Suppose I have a premise such as A ∨ B ∨ C
, and want to prove P
. The natural way to prove it is by proving that A ⟹ P
, B ⟹ P
and C ⟹ P
. However, disjE
is made for 2 cases, so I have to apply it twice:
lemma foo:
assumes "A ∨ B ∨ C"
shows "P"
proof (rule disjE)
assume "A"
...
then show "P"
next
assume "B ∨ C"
then show "P"
proof (rule disjE)
assume "B"
...
then show "P"
next
assume "C"
...
then show "P"
qed
qed
Now of course, I could prove my own lemma disjE_3 [rulify]: assumes "P ∨ Q ∨ R" "P ⟹ A" "Q ⟹ A" "R ⟹ A" shows "A"
and use it instead, which would result in a much more readable proof:
lemma foo:
assumes "A ∨ B ∨ C"
shows "P"
proof (rule disjE_3)
assume "A"
...
then show "P"
next
assume "B"
...
then show "P"
next
assume "C"
...
then show "P"
qed
On the other hand, what if I have 4 cases, or 5, or 10? It seems very inconvenient to create rules for every case you might need. Although you can apply multiple rules at once, proof (rule disjE disjE)
doesn't seem to cut it in this case.
So, is there a way to reduce the subgoals to a "minimal form" by applying a rule as many times as possible?