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
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
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With