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
See Question&Answers more detail:
os 与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…