如何在Isabelle中定义一个函数,该函数具有不同的定义,具体取决于其参数的类型或它所使用的上下文的类型？
例如,我可能想要定义一个is_default带有类型的函数'a ? bool,其中每个不同的类型'a都有一个可能不同的"默认值".(为了论证,我也假设现有的概念zero不合适.)
我是vim粉丝,但只有emacs才有这个Isabelle/HOL环境.jEdit很棒,但我不能使用
using [[simp_trace=true]]
就像在emacs中一样.
如何在jEdit中启用"跟踪" ？
我想A /\ B /\ C /\ D /\ E /\ F在伊莎贝尔证明.如何将子目标自动拆分为6个单独的子目标proof(rule ...),以便之后我可以单独证明它们？
当然,我可以写proof(rule conjI)5次,但也许有一种更优雅的方式可以一步完成分割？
我正在阅读Isabelle教程，并试图阐明我对使用Primrec和乐趣的概念。到目前为止，我已经搜索了所有内容，包括此处的答案；我知道primrec内部的构造函数默认只能有一个方程式，而primrec默认具有[simp]，而fun可以具有多个方程式，并且需要明确指定自动化策略。但是，我仍然很难清楚地理解它。
任何人都足以举例说明吗？
问题
我想知道在 Isabelle 中是否有一种自然的编码方式是这样的语法：
type_synonym Var = string
datatype Value = VInt int | ...
datatype Cmd = Skip | NonDeterministicChoice "Cmd set" | ...
动机是根据非确定性选择定义一些规范命令，例如：
Magic == NonDeterministicChoice {}
Rely c r z = Defined using set compreehension and NonDeterministicChoice
Isabelle 抱怨“Cmd set”中类型“Cmd”的递归出现，即：
不支持通过类型表达式“Cmd set”中的类型构造函数“Set.set”递归出现类型“Cmd”。使用“bnf”命令将“Set.set”注册为有界自然函子以允许嵌套（共）递归通过它
在我使用 set 时查看 Isabelle 错误消息，我无法弄清楚如何在这种情况下为“set”类型注册有界自然函子，因此我决定尝试一种推测性解决方案。
投机解决方案
相反，如果我使用归纳定义的数据类型，例如列表，伊莎贝尔不会抱怨，例如
datatype Cmd = Skip | NonDeterministicChoice "Cmd list" | ...
列表在这里不是正确的抽象，但我试一试看看它是否有效。使用列表的直接效果是，我需要使用序列过滤而不是使用集合理解，然后问题就变成了假设存在两个列表：一个包含Cmd 的所有元素，另一个包含Value 的所有元素。
我声明了两个未解释的常量：
consts Values :: "Value list"
consts Programs :: "Cmd …我正在尝试官方Isabelle教程中的列表示例.我将#with :和@with 替换为与++Haskell具有相同的语法.现在我收到有关AST中含糊不清的警告.我知道我可以隐藏函数,hide_const但这对于中缀表示法的运算符不起作用.我怎样才能隐藏Isabelle的操作员？
确切的警告信息是:
Ambiguous input? produces 2 parse trees:
("\<^const>HOL.Trueprop"
("\<^const>HOL.eq" ("\<^const>Map.map_add" ("/<^const>toylist.list.Nil") ("_position" ys))
("_position" ys)))
("\<^const>HOL.Trueprop"
("\<^const>HOL.eq" ("\<^fixed>app" ("\<^const>toylist.list.Nil") ("_position" ys)) ("_position" ys)))
Fortunately, only one parse tree is well-formed and type-correct,
but you may still want to disambiguate your grammar or your input.
我注意到,在与Isabelle/HOL Isar合作时,有几种方法可以处理通用量化问题.我正在尝试以适合本科生理解和复制的风格写出一些证据(这就是我使用Isar的原因!)而且我对如何以一种很好的方式表达普遍量化感到困惑.
例如,在Coq中,我可以写forall x, P(x),然后我可以说"感应x",它将根据相应的归纳原理自动生成目标.然而,在Isabelle/HOL Isar中,如果我想直接应用归纳原理,我必须在没有任何量化的情况下陈述该定理,如下所示:
lemma foo: P(x)
proof (induct x)
这样可以正常工作,因为x被视为一个原理图变量,就像它被普遍量化一样.但是,它在声明中缺乏普遍的量化,而这种量化并不是很有教育意义.我资助的另一种方式是使用\<And>和\<forall>.但是,如果我以这种方式陈述引理,我不能直接应用归纳原理,我必须首先修复普遍量化的变量......从教育的角度来看,这似乎很不方便:
lemma foo: \<And>x. P(x)
proof -
fix x
show "P(x)"
proof (induct x)
什么是表达通用量化的一个很好的证明模式,不需要我在归纳之前明确地修复变量？
如何更改规则中的前提顺序？例如,在伊莎贝尔的自然演绎规则中:
mp: ?P ? ?Q ? ?P ? ?Q
我们可以将订单更改为:
?P ? ?P ? ?Q ? ?Q
我可以使用rev_mp或定义一个新的引理,但我要找的是是否有一个定理修饰符改变了前提的顺序.
我刚开始使用Isabelle/HOL并试图用自然演绎规则证明一个简单的HOL语句"P(t)⟶(∃x.P(x))".我从一个仅包含该定理的理论文件开始:
theory simple imports Main
begin
lemma T: shows "P(t) ? (?x . P(x))"
proof
(* x *)
qed
end
在注释中标记为x的位置处,当前目标已经是"P(t)⟹(∃x.P(x))",即逻辑蕴涵已经简化为元逻辑蕴涵.
通过反复试验,我得出以下证据:
proof
assume "P(t)" then
have "? x . P(x)" by (rule exI) then
have "P(t) ? (?x . P(x))" by (rule impI)
then show "P(t) ? (?x . P(x))" by (rule impE)
qed
这看起来有些奇怪:我正在介绍这个含义,只是为了在下一步中消除它.
我现在的问题是:
我一直在尝试使用Concrete Semantics(为Coq Isabelle/HOL 编写)作为参考点来编写和验证Agda中的编译器.我正在为该文本中使用的相同语言定义编译.
对于上下文,我已经完成了编译器的编写,现在我处于验证阶段,但是我必须在机器指令执行的定义中对Concrete Semantics做出重大改变.这种差异似乎在Agda中是必要的,但现在使验证阶段非常复杂.
在尝试使用Concrete Semantics中给出的更简单的指令执行版本时,我遇到了这一行,这可以解释为什么我无法直接将其转换为Agda:
列表的头部,第一个元素和尾部,列表的其余部分也很有用:
Run Code Online (Sandbox Code Playgroud)fun hd :: 'a list ? 'a hd (x # xs) = x请注意,由于HOL是总函数的逻辑,
hd []因此定义了,但我们不知道结果是什么.也就是说,hd []未定义但未定义.
hd []欠定义是什么意思？这相当于在Agda中使用不完整的模式吗？
汇编指令执行函数在很大程度上依赖于hd.在我在Agda中的实现中,我给了多个类型的索引,以允许我构建堆栈总是具有最小元素数量的证明,以避免不完整的模式匹配问题.现在我正在尝试验证编译器,证明的大小比具体语义中的证明更复杂,因为我必须使用这些索引.
我是否遗漏了某些东西,或者具体语义中的证据是不完整的,hd []未被定义？