Gergely Buday (Jul 26 2023 at 07:43): Gergely Buday (Jul 26 2023 at 07:43):lemma imp_uncurry2: "(P ⟶ (Q ⟶ R)) ⟶ P ∧ Q ⟶ R"
proof (rule impI)
assume pqr: "P ⟶ (Q ⟶ R)"
show pandqr: "P ∧ Q ⟶ R"
proof
assume pq: "P ∧ Q"
then have p: P by (rule conjE)
from pq have q: Q by (rule conjE)
show R
proof -
from pqr and p have qr: "Q ⟶R" by (rule impE)
from qr and q show ?thesis by (rule HOL.mp)
qed
qed
qed
I wonder how showing R solves pandqr and in turn the main proof. Can you give an explanation?
Mathias Fleury (Jul 26 2023 at 07:55):instead of proof, you should always write proof standard or proof -
Mathias Fleury (Jul 26 2023 at 07:55):in your case the standard is implicit
Mathias Fleury (Jul 26 2023 at 07:56):but it does the obvious transformation
Mathias Fleury (Jul 26 2023 at 10:01):kann auch einfach ein Beweis sein…
Last updated: Dec 21 2024 at 16:20 UTC