伊莎贝尔/HOL规则反演证明

Question

我从Isabelle/HOL开始，学习发行版中包含的prog-prove.pdf教程。我在4.4.5节“规则倒置”中遇到了困难。本教程(本质上)给出了以下示例：

theory Structured
imports Main
begin

inductive ev :: "nat ⇒ bool" where
ev0:  "ev 0" |
evSS: "ev n ⟹ ev (Suc (Suc n))"

notepad
begin
  assume "ev n"
  from this have "ev (n - 2)"
  proof cases
    case ev0 thus "ev (n - 2)" by (simp add: ev.ev0)
  next
    case (evSS k) thus "ev (n - 2)" by (simp add: ev.evSS)
  qed
end

这是可行的，尽管我不得不把notepad放在证据的周围，因为伊莎贝尔不喜欢顶级的assume。但是现在我想用同样的证明方法，把同样的事实和引理说出来，这是行不通的：

lemma "ev n ⟹ ev (n - 2)"
proof cases
  case ev0 thus "ev (n - 2)" by (simp add: ev.ev0)
  (* ... *)

伊莎贝尔在ev0停留，抱怨Undefined case: "ev0"，然后Illegal application of proof command in "state" mode在by。

这两种表述这个目标的方法有什么不同？如何在引理语句中使用上述证明技巧？(我知道我可以用sledgehammer证明引理，但我试图理解Isar证明。)

Answer 1

cases方法试图根据“给定的事实”选择正确的案例分析规则。给定的事实是使用then、from或using提供的事实。

如果将光标放在have "ev (n - 2)"上，就会看到目标状态。

proof (prove): depth 1

using this:
  ev n

goal (1 subgoal):
 1. ev (n - 2)

当你在lemma "ev n ⟹ ev (n - 2)"上的时候

proof (prove): depth 0

goal (1 subgoal):
 1. ev n ⟹ ev (n - 2)

解决方案是，当您可以使用适当的Isar命令分别指定引理的假设时，避免元蕴涵(==>)，并将它们提供给使用using的证明。

lemma 
  assumes "ev n"
  shows "ev (n - 2)"
using assms