Search code examples
isabelleisar

proof (rule disjE) for nested disjunction


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

Solution

  • 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