isabelle - 当证明开始时，我们如何才能迫使 Isabelle 向我们透露它在 Isar 的后台应用的规则是什么？

Question

我试图证明:

lemma
  shows "¬ ev (Suc 0)"

我做到了:

lemma
  shows "¬ ev (Suc 0)"
proof (rule notI)
  assume "ev (Suc 0)"
  then show False 
  proof

它给了我非常漂亮的目标:

proof (state)
goal (2 subgoals):
 1. Suc 0 = 0 ⟹ False
 2. ⋀n. ⟦Suc 0 = Suc (Suc n); ev n⟧ ⟹ False

这可能会使我的证明具有可读性。

它似乎在后台应用了某种情况。但是当我写案例时，证明立即完成，而不是明确地显示上述规则反转案例。请参阅:

lemma
  shows "¬ ev (Suc 0)"
proof (rule notI)
  assume "ev (Suc 0)"
  then show False 
  proof (cases)

显示:

proof (state)
goal:
No subgoals!

这意味着我可以只放置一个qed。

我怎样才能准确地弄清楚 Isar 在 Isabelle 中自动执行的(介绍？)规则？

Answer 1

正如对您问题的评论中所述，就您而言，proof归结为proof rule 。 rule方法(不带任何参数)应用一些拟合引入/消除规则。您可以使用 rule_trace 找出它是哪一个。属性:

    using [[rule_trace]] apply rule

(或者你可以在上面的全局范围内完成 declare [[rule_trace]] 或在你的 Isar 证明中完成 note [[rule_trace]])

这说的是

    proof (prove)
    goal (2 subgoals):
     1. Suc 0 = 0 ⟹ False
     2. ⋀n. Suc 0 = Suc (Suc n) ⟹ ev n ⟹ False 
    rules:
        ev ?a ⟹ (?a = 0 ⟹ ?P) ⟹ (⋀n. ?a = Suc (Suc n) ⟹ ev n ⟹ ?P) ⟹ ?P

不幸的是，它没有给你名字。但很显然，这个规则一定来自inductive命令，因为你自己没有证明这一点。如果您执行 print_theorems inductive 之后的命令命令，你发现这是定理ev.cases ，这也是cases方法使用(除了 cases 方法还对目标进行一些后处理简化，如前面提到的 here )。

inductive命令注册ev.cases规则为elim?规则，这意味着自动化不会使用它，但是如果您执行类似 apply rule 的操作，会考虑的。