proof (rule disjE) for nested disjunction

Question

In Isar-style Isabelle proofs, this works nicely:

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

The implicit rule called by proof here is rule conjE. But what should I put there to make it work for more than just one disjunction:

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

Warford

Answer 1

While writing the question, I had an idea, and it turns out to be what I want:

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

Warford

Answer 2

Another canonical way to do this kind of case analysis is as follows:

{ 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

That is, let an automatic tool "figure out" the details at the end. This works especially well when considering arithmetical cases (with by arith as final step).

Update: Using the new consider statement it can be done as follows:

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

Wina

I’ve done that as well. One problem is that it lacks the automatisms of proof, e.g. setting up cases, ?thesis and the like. – Warford

@JoachimBreitner: True. It works best when the proof is made more readable by explicitly writing an assumption instead of using case anyway (which is mostly true for rather short assumptions). – Wina

@JoachimBreitner: proof does not set up ?thesis, lemma (or have) does. So you can use ?thesis in the rule/intro/elim-approach only if you could use it in the moreover-approach. – Miscarry

Answer 3

Alternatively to do case distinction, it seems you can bend the more general induct method to do your bidding. For three cases, this would work like this: Prove a lemma 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

You can use this lemma as follows:

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

The disadvantage is you need a bunch of lemmas to cover any number of cases, disjCases2, disjCases3, disjCases4, disjCases5 etc., but otherwise it seems to work nicely.

Shafting