2

我试图证明：

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 中自动执行的（介绍？）规则？

4

1 回答 1

2

正如对您问题的评论中所述，在您的情况下，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命令，您会发现这是 theorem ev.cases，这也是该cases方法使用的那个（除了该cases方法还对目标进行了一些后处​​理简化，如此处所述）。

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

于 2020-05-21T08:13:35.213 回答