[isabelle] finishing a proof



I would like to write a forward proof in Isar to have 


   P â (Q â R) â Q â (P â R)


by hand it can be done through two implication eliminations using P and Q as assumptions, and then re-introducing implications but in the reverse order.


I wrote the following to formalise this:


theory Logic

imports Main



lemma "P â (Q â R) â Q â (P â R)" 

proof -

assume premise : "P â (Q â R)"

assume p: "P"

have qr: "Q â R" by (simp add: p premise)

assume q: "Q"

have r: "R" by (simp add: q qr)

from this have "P â R" by (simp add: p)

from this have "Q â (P â R)" by (simp add: q)

thus "P â (Q â R) â Q â (P â R)" by assumption


Failed to refine any pending goal 

Local statement fails to refine any pending goal

Failed attempt to solve goal by exported rule:

  (P â Q â R) â (P) â (Q) â (P â Q â R) â Q â P â R


It fails at the last line, it is not really clear why. Can you give a clue?


- Gergely

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.