9

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
Joachim Breitner
  • 25,395
  • 6
  • 78
  • 139

3 Answers3

7

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
Joachim Breitner
  • 25,395
  • 6
  • 78
  • 139
6

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
chris
  • 4,988
  • 20
  • 36
  • 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. – Joachim Breitner Apr 10 '13 at 10:42
  • @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). – chris Apr 10 '13 at 11:19
  • 2
    @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. – Lars Noschinski Apr 18 '13 at 06:39
2

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.