Isabelle/HOL中的对象级含义

Question

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

==>

而不是

-->

对象逻辑级别，即高阶逻辑含义。

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

除此之外，关于对象和元级别含义的使用，我应该知道什么？我看到后者被广泛使用。我应该在什么时候以及为了什么使用HOL含义？

Answer 1

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

也就是说，您不应该在编写的代码中经常看到==>。

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