Applying elimination rule as many times as possible in Isabelle/Isar

65 Views Asked by At

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?

0

There are 0 best solutions below