Isabelle/HOL 规则反转证明

Question

我从 Isabelle/HOL 开始，然后学习发行版中包含的 prog-prove.pdf 教程。我被第 4.4.5 节难住了，"Rule Inversion"。本教程（基本上）给出了以下示例：

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，因为 Isabelle 不喜欢顶层的 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

Isabelle/HOL 规则反转证明

Isabelle/HOL proof by rule inversion

isabelle