Re: [isabelle] finishing a proof



Hi,

My non-expert view:

You have made too many assumptions - namely your assumptions p and q.

Try starting your proof with

proof(rule impI)+

Cheers

Mark

On 13 October 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.