Search code examples
isabelleproof

Proof implication with exist in the premises without using Isar

I have the following goal extracted from one of the theorems I have to prove:

∃ys zs. [x] = ys @ zs ∧ P ys zs ⟹ P [] [x] ∨ P [x] []

Here I wanted to apply the existential elimination rule but it produces two strange subgoals:

 1. ∃ys zs. [x] = ys @ zs ∧ P ys zs ⟹ ∃x. ?P25 x
 2. ⋀xa. ∃ys zs. [x] = ys @ zs ∧ P ys zs ⟹ ?P25 xa ⟹ P [] [x] ∨ P [x] []

The idea is that if I could remove the quantifiers the proof is indeed quite easy. If [x]= ys @ zs then there are two possibilities. Either ys = [x], zs = [] or the opposite. Thus, we would P [x] [] or P [] [x].

How can I prove this without using Isar, only using apply commands?

Solution

  • I don't know why the exists elimination tactic fails in your case, but the following line succeeds.

    by (elim exE, rename_tac ys zs, case_tac ys, auto)

    Here, the rename_tac renames the newly obtained lists to the user-chosen names ys and zs, so that afterwards a case-analysis on ys (empty or not) is possible.