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