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

(或者你可以在你的 Isar 证明中在全局某处完成 declare [[rule_trace]] 或 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 的操作，会考虑。