# [isabelle] finishing a proof

Hi,
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
begin
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.*