John Hughes (May 06 2025 at 13:53): John Hughes (May 06 2025 at 13:53):In programming-and-proving, page 45, there's a nice example of how to do a proof where there are two cases:
have "P \/ Q" <proof>
then show "R"
proof
assume "P"
...
show "R" <proof>
next
assume "Q"
...
show "R" <proof>
qed
Is there something similar for a 3-way disjunction? I tried the natural thing:
lemma example:
assumes "A ∨ B ∨ C"
shows "R"
proof -
have "A ∨ B ∨ C" using assms by blast
then show "R"
proof
assume "A"
show "R" sorry
next
assume "B"
show "R" sorry
next
assume "C"
show "R" sorry
qed
qed
but Isabelle very reasonably complained, because the A \/ B \/ C was treated as a two-term disjunction, A \/ (B \/ C). And I can obviously split that, and nest one level deeper, etc., but I'm wondering if there's something more naturally structured that I might use when working with something like trichotomy, where three disjoint cases arise very naturally.
Mathias Fleury (May 06 2025 at 14:12):begin
have "P ∨ Q ∨ Q'" sorry
then have "R"
proof (elim disjE)
The consider keyword is also very powerful for such use cases
Last updated: May 31 2025 at 04:25 UTC