Isabelle/HOL 中的对象级别含义

Question

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

==>

而不是

-->

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

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

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

Answer 1

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

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

1. 在编写引理时，使用assumes 和shows 语法通常会更好。
2. 对于带有have 的中间步骤，有一个带有if 的语法： have "B" if "A" 而不是 have "B ==> A"
3. 元暗示只能在顶层使用，因此如果您有一个谓词作为函数的参数，则不能在该谓词中使用==>。