Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

proof (rule disjE) for nested disjunction

Tags:

isabelle

isar

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
like image 520
Joachim Breitner Avatar asked Apr 09 '13 12:04

Joachim Breitner


1 Answers

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
like image 104
Joachim Breitner Avatar answered Sep 19 '22 14:09

Joachim Breitner