[当证明开始时，我们如何迫使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中自动执行的规则（简介？）>

[我正试图证明：引理显示“¬ev（Suc 0）”我做了：引理显示“¬ev（Suc 0）”证明（规则notI）假设为“ ev（Suc 0）”然后显示了虚假证明，给了我非常漂亮的目标：...

Answer 1

如您对问题的评论所指出，在您的情况下，proof可以归结为proof rule。 rule方法（不带任何参数）应用一些拟合引入/消除规则。您可以使用rule_trace属性找出是哪一个：