Re: [isabelle] elementary proofs



Hi Michel,

I think you have to use the hyphen method "-" as an argument for
the command proof, because there is no introduction rule for proving
an atomic statement like R. There are a lot of ways to prove this
conjecture. One way possible (using more or less your style) goes
as follows:

lemma facile2 : "(P â Q) â (Q â R) â (P â R)"
  proof
    assume 1: "(P âQ)â (Q â R)"
    show "P â R"
    proof (rule impI)
      assume 2:"P"
      show "R"
      proof -
        from 1 have "PâQ" by (rule conjE)
        then have q: Q using 2 by (rule mp)
        from 1 have "QâR" by  (rule conjE)
        from this and q show ?thesis by (rule mp)
      qed
    qed
  qed

Best!

On Sat, Mar 26, 2016 at 7:48 PM, michel levy <michel.levy at imag.fr> wrote:

> I have tried (with success) a proof elementary
> lemma facile1 : "P â (Q â P)"
>   proof
>     assume 1:"P"
>     note 1
>     show "Q â P"
>     proof
>       assume 2:"Q"
>       from 1 show "P".
>     qed
>   qed
>
> Then I have started another proof
> lemma facile2 : "(P â Q) â (Q â R) â (P â R)"
>   proof
>     assume 1: "(P âQ)â (Q â R)"
>     note 1
>     show "P â R"
>     proof
>       assume 2:"P"
>       note 2
>       show "R"
>       proof
> But on the last line, on the word proof, I have the error "Failed to
> apply initial proof method."
> I don't see the difference between my both examples and why I have this
> error.
>
> Thank you in advance for an answer.
>
> --
> email : michel.levy at imag.fr
> http://membres-liglab.imag.fr/michel.levy
>
>


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica
90619-900 -Porto Alegre - RS - Brasil



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