isabelle - Isabelle/HOL 中的对象级别含义

Question

我看到 Isabelle/HOL 中的许多定理更喜欢元级含义：

==>

代替

-->

对象逻辑层，即高阶逻辑蕴涵。

Isabelle wiki说，粗略地说，应该使用元级别的含义将规则陈述中的假设与结论分开。

除此之外，关于对象和元级别含义的使用我应该知道什么？我看到后者主要被使用。我应该在什么时候使用 HOL 蕴涵？

Answer 1

我认为简短的回答是：==>尽可能使用，因为它比-->.

话虽==>如此，你不应该在你编写的代码中经常看到。

1. assumes在编写引理时，使用andshows语法通常更好。
2. 对于中间步骤，have有一个语法if： have "B" if "A"而不是have "B ==> A"
3. 元暗示只能在顶层使用，所以如果你有一个谓词作为函数的参数，你就不能==>在那个谓词中使用。