我已经看过很多关于Isabelle的语法和证明策略的文档.然而,我几乎找不到它的基础.我有几个问题,如果有人能抽出时间回答,我将非常感激:
为什么Isabelle/HOL不接受不终止的功能？许多其他语言(如Haskell)都承认非终止函数.
什么符号是伊莎贝尔的元语言的一部分？我读到在通用量化(/\)和暗示(==>)的元语言中有符号.但是,这些符号在对象级语言(∀和-->)中具有对应的符号.我知道这-->是一个类型的对象级函数bool => bool => bool.但是,∀和how是如何定义的？它们是对象级布尔函数吗？如果是这样,它们是不可计算的(考虑无限域).我注意到我能够在∀和ther中编写布尔函数,但它们不可计算.那么∀和what是什么？它们是对象级别的一部分吗？如果是这样,他们是如何定义的？
Isabelle定理只是布尔表达式吗？然后布尔是元语言的一部分？
据我所知,Isabelle是一种严格的编程语言.我怎样才能使用无限对象？比方说,无限列表.Isabelle/HOL有可能吗？
对不起,如果这些问题非常基础.我似乎没有找到关于伊莎贝尔元理论的好教程.我很乐意,如果有人可以推荐我这些主题的好教程.
非常感谢你.
我注意到,在与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)
什么是表达通用量化的一个很好的证明模式,不需要我在归纳之前明确地修复变量？
我想在 Isabelle 中使用 nat 类型，但我想重载一些现有的定义，例如加法。我写了以下代码：
theory Prueba
imports Main HOL
begin
primrec suma::"nat ? nat ? nat" where
"suma 0 n = 0" |
"suma (Suc x) n = 0"
no_notation suma (infix "+" 65)
value "2 + (1 :: nat)"
我试图用一个总是输出 0 的新定义来重载加法。但是，当我评估2 + (1 :: nat)I get 时"Suc (Suc (Suc 0))" :: "nat"，这意味着 Isabelle 仍在使用来自 Nat 的加号定义。我怎样才能让它使用我对 + 的新定义？
谢谢
我正在尝试编写一个函数来计算Coq中的自然除法,我在定义它时遇到了一些麻烦,因为它不是结构递归.
我的代码是:
Inductive N : Set :=
| O : N
| S : N -> N.
Inductive Bool : Set :=
| True : Bool
| False : Bool.
Fixpoint sum (m :N) (n : N) : N :=
match m with
| O => n
| S x => S ( sum x n)
end.
Notation "m + n" := (sum m n) (at level 50, left associativity).
Fixpoint mult (m :N) (n : N) : N := …我试图在 Coq 中证明以下引理：
Lemma not_eq_S2: forall m n, S m <> S n -> m <> n.
这似乎很容易，但我不知道如何完成证明。有人可以帮我吗？
谢谢你。
我试图证明一个引理,它在某个部分有一个错误的假设.在Coq,我曾经写过"一致",它会摆脱目标.但是,我不知道如何继续Isabelle Isar.我试图证明我的le功能的一个引理:
primrec le::"nat ? nat ? bool" where
"le 0 n = True" |
"le (Suc k) n = (case n of 0 ? False | Suc j ? le k j)"
lemma def_le: "le a b = True ? (?k. a + k = b)"
proof
assume H:"le a b = True"
show "?k. a + k = b"
proof (induct a)
case 0
show "?k. 0 + k = b"
proof -
have "0 + …