[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.