isabelle - 嵌套析取的证明（规则 disjE）

Question

在 Isar 风格的 Isabelle 证明中，这很有效：

from `a ∨ b` have foo
proof
  assume a
  show foo sorry
next
  assume b
  show foo sorry
qed

这里调用的隐含规则proof是rule conjE。但是我应该放什么让它不仅仅适用于一个析取：

from `a ∨ b ∨ c` have foo
proof(?)
  assume a
  show foo sorry
next
  assume b
  show foo sorry
next
  assume c
  show foo sorry
qed

Answer 1

在写这个问题的时候，我有了一个想法，结果就是我想要的：

from `a ∨ b ∨ c` have foo
proof(elim disjE)
  assume a
  show foo sorry
next
  assume b
  show foo sorry
next
  assume c
  show foo sorry
qed

Answer 2

进行这种案例分析的另一种规范方法如下：

{ assume a
  have foo sorry }
moreover
{ assume b
  have foo sorry }
moreover
{ assume c
  have foo sorry }
ultimately
have foo using `a ∨ b ∨ c` by blast

也就是说，让一个自动工具在最后“弄清楚”细节。这在考虑算术情况时特别有效（by arith作为最后一步）。

更新：使用 newconsider语句可以如下完成：

notepad
begin
  fix A B C assume "A ∨ B ∨ C"
  then consider A | B | C by blast
  then have "something"
  proof (cases)
    case 1
    show ?thesis sorry
  next
    case 2
    show ?thesis sorry
  next
    case 3
    show ?thesis sorry
  qed
end

Answer 3

或者，为了区分大小写，您似乎可以采用更通用的induct方法来进行竞标。对于三种情况，这将像这样工作：证明一个引理disjCases3：

lemma disjCases3[consumes 1, case_names 1 2 3]:
  assumes ABC: "A ∨ B ∨ C"
  and AP: "A ⟹ P"
  and BP: "B ⟹ P"
  and CP: "C ⟹ P"
  shows "P"
proof -
  from ABC AP BP CP show ?thesis by blast
qed

您可以按如下方式使用此引理：

from `a ∨ b ∨ c` have foo
proof(induct rule: disjCases3)
  case 1 thus ?case 
     sorry
next
  case 2 thus ?case 
     sorry
next
  case 3 thus ?case 
     sorry
qed

缺点是你需要一堆引理来涵盖任意数量的情况，disjCases2, disjCases3,disjCases4等disjCases5，但除此之外它似乎工作得很好。