我想了解关键字 proof 在 Isar 证明中的工作原理。我咨询了the Isabelle/Isar reference, section 6.3.2和Programming and Proving in Isabelle/HOL, section 4.1。
总结一下我所学到的，用关键字proof开始证明有三种方式：
没有任何论据，Isabelle 为被证明的引理找到了一个合适的引入规则，并将其应用于前向模式
如果提供了特定规则，例如 rule name、unfold true_def、clarify 或 induct n，则它会以前进模式应用于目标
我对第三种情况就像使用 apply 并提供参数一样吗？
系统选取的第一个案例的自动引入规则是怎样的？
而且，上面是否完整描述了proof的用法？
【问题讨论】：
标签： isabelle
没有方法说明的命令proof 应用方法default。方法default 几乎就像rule，但是如果rule 失败，那么它会尝试下一个intro_classes，然后是unfold_locales。没有给出定理列表的方法rule 会尝试向经典推理器（intro、elim 和dest）声明的所有规则。如果没有链接任何事实，则仅考虑 intro 规则。否则，将尝试所有类型的规则。所有链入的事实都必须与规则相统一。 dest 规则在应用之前会转换为 elim 规则。
您可以使用print_rules 打印所有声明的规则。安全规则（intro!、elim!、...）优先于普通规则（intro、elim、...），额外规则（intro?、elim?）排在最后。
您也可以使用rule 而不给出任何规则。然后，它的行为类似于default，但没有备用intro_classes 和unfold_locales。
【讨论】：
Andreas 很好地描述了 proof 在没有方法参数的情况下是如何工作的；我将仅介绍问题的其他部分。
首先，proof (method) 类似于 apply (method)，除了一件事：apply 让您处于“证明”模式，您可以在其中继续更多 apply 语句，proof 转换为“状态”模式，您必须使用have 或show 语句才能继续证明。否则对目标状态的影响是一样的。
我还要指出，case 2 (proof -) 实际上是case 3 的一个实例，因为- 实际上是一个普通的证明方法，就像rule name 或induct 一样（你也可以写apply -，例如）。连字符- proof 方法什么都不做，除了它会将链式事实插入到当前目标中，如果给定了任何链式事实。
【讨论】：