我已经看过很多关于Isabelle的语法和证明策略的文档.然而,我几乎找不到它的基础.我有几个问题,如果有人能抽出时间回答,我将非常感激:
为什么Isabelle/HOL不接受不终止的功能？许多其他语言(如Haskell)都承认非终止函数.
什么符号是伊莎贝尔的元语言的一部分？我读到在通用量化(/\)和暗示(==>)的元语言中有符号.但是,这些符号在对象级语言(∀和-->)中具有对应的符号.我知道这-->是一个类型的对象级函数bool => bool => bool.但是,∀和how是如何定义的？它们是对象级布尔函数吗？如果是这样,它们是不可计算的(考虑无限域).我注意到我能够在∀和ther中编写布尔函数,但它们不可计算.那么∀和what是什么？它们是对象级别的一部分吗？如果是这样,他们是如何定义的？
Isabelle定理只是布尔表达式吗？然后布尔是元语言的一部分？
据我所知,Isabelle是一种严格的编程语言.我怎样才能使用无限对象？比方说,无限列表.Isabelle/HOL有可能吗？
对不起,如果这些问题非常基础.我似乎没有找到关于伊莎贝尔元理论的好教程.我很乐意,如果有人可以推荐我这些主题的好教程.
非常感谢你.
我发现自己经常想通过类型而不是名称来引用假设。尤其是在语义规则倒置的证明中，即具有几种情况的规则，每种情况可能都有多个先例。
我知道如何使用来完成此操作match goal with ...，如以下简单示例所示。
Lemma l0:
forall P1 P2,
P1 \/ (P1 = P2) ->
P2 ->
P1.
Proof.
intros.
match goal with H:_ \/ _ |- _ => destruct H as [H1|H2] end.
assumption.
match goal with H: _ = _ |- _ => rewrite H end.
assumption.
Qed.
有没有更简洁的方法？还是更好的方法？
（诸如的引入模式intros [???? HA HB|??? HA|????? HA HB HC HD]不是一个选择，我已经厌倦了找到正确数量的?s！）
例如，是否可以编写grab将模式和策略结合起来的策略，如
grab [H:P1 \/ _] => rename H into HH.
grab …