Re: [isabelle] elementary proofs
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
lemma facile2 : "(P â Q) â (Q â R) â (P â R)"
assume 1: "(P âQ)â (Q â R)"
show "P â R"
proof (rule impI)
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)
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)"
> assume 1:"P"
> note 1
> show "Q â P"
> assume 2:"Q"
> from 1 show "P".
> Then I have started another proof
> lemma facile2 : "(P â Q) â (Q â R) â (P â R)"
> assume 1: "(P âQ)â (Q â R)"
> note 1
> show "P â R"
> assume 2:"P"
> note 2
> show "R"
> 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
> Thank you in advance for an answer.
> email : michel.levy at imag.fr
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
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