Email Gateway (Aug 22 2022 at 13:03): Email Gateway (Aug 22 2022 at 13:03):From: michel levy <michel.levy@imag.fr>
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 Gateway (Aug 22 2022 at 13:03):From: Alfio Martini <alfio.martini@acm.org>
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!
Email Gateway (Aug 22 2022 at 13:03):From: Alfio Martini <alfio.martini@acm.org>
Hi,
It should be in the reference manual and in the programming and proving
tutorial.
Best
Email Gateway (Aug 22 2022 at 13:03):From: Alfio Martini <alfio.martini@acm.org>
Hi Michel,
Here goes one way to do it:
theorem "P ∨ Q --> Q ∨ P"
proof (rule impI)
assume 1: "P \/ Q"
show "Q \/ P"
proof (rule disjE[OF 1])
assume "P"
then show "Q \/ P" by (rule disj2)
next
assume "Q"
then show "Q \/ P" by (rule disjI1)
qed
qed
Best
Last updated: Apr 26 2024 at 16:20 UTC