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