isabelle - 如何提交关键字证明的参数？

Question

我想了解关键字 proof 在 Isar 证明中的工作原理。我咨询了the Isabelle/Isar reference, section 6.3.2和 Programming and Proving in Isabelle/HOL, section 4.1 .

总结一下我所学到的，可以通过三种方式通过关键字 proof 开始证明:

• 在没有任何论证的情况下，Isabelle 为所证明的引理找到了合适的引入规则，并将其应用于正向模式

• 如果提供连字符:- 作为参数，则 proof 对目标不会执行任何操作，避免在会导致以下情况时应用任何自动规则:死胡同

• 如果是特定规则，例如规则名称、unfold true_def、clarify或induct n提供，然后以转发模式应用于目标

第三种情况就像使用 apply 并提供参数，我说得对吗？

系统如何挑选第一个案例的自动引入规则？

而且，上面是否完整地描述了proof的用法？

Answer 1

没有方法规范的命令proof应用方法default。方法 default 几乎类似于 rule，但如果 rule 失败，则会尝试下一个 intro_classes，然后尝试 >unfold_locales。在没有给出定理列表的情况下，方法 rule 会尝试向经典推理器声明的所有规则(intro、elim 和 目标)。如果没有链接任何事实，则仅考虑 intro 规则。否则，将尝试所有类型的规则。所有束缚的事实必须与规则相统一。 dest 规则在应用之前会转换为 elim 规则。

您可以使用 print_rules 打印所有声明的规则。安全规则(intro!、elim!、...)优先于普通规则(intro、elim) , ...) 和额外规则 (intro?, elim?) 最后。

您还可以使用rule而不给出任何规则。然后，它的行为类似于 default，但没有后备 intro_classes 和 unfold_locales。