Re: [isabelle] finishing a proof



If you look at the State with the cursor after the proof keyword, you will see displayed what you are allowed to assume, which variables you must fix, and which conclusion you must show. Here you may assume "P â (Q â R)â and must show "Q â (P â R)â; to do that in single steps requires a nested proof. Or else do it as Mark suggested.

Larry

> On 13 Oct 2016, at 10:15, Gergely Buday <buday.gergely at uni-eszterhazy.hu> wrote:
> 
> 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.