Isabelle/HOL中的对象层次含义

Question

我发现Isabelle/HOL中的许多定理更倾向于元级蕴涵：

==>

而不是

-->

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

伊莎贝尔维基说，粗略地说，应该使用元级含义来将假设与规则语句中的结论分开。

除此之外，关于对象和元级含义的使用，我应该知道些什么呢？我认为后者主要是被使用。什么时候和什么时候我应该使用HOL的含义？

Answer 1

我认为简单的答案是:尽可能使用==>，因为它比-->更容易使用。

尽管如此，您不应该在编写的代码中经常看到==>。

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