嵌套析取的证明（规则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

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

{ 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 2

在写问题时，我有了一个主意，结果就是我想要的：

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