Jiahong Lee (Dec 19 2022 at 01:57): Jiahong Lee (Dec 19 2022 at 01:57):Hi, suppose I have a proven theorem:
theorem notnotI: "p ⟹ ¬ ¬ p"
by(rule cnf.clause2raw_not_not)
can I use it to rewrite a term in a formula?
lemma "p ∨ q ⟹ p ∨ ¬ ¬ q"
proof -
assume "p ∨ q"
thus "p ∨ ¬ ¬ q" by (* rewrite term q with notnotI *)
qed
EDIT:
To put it into context, I'm looking for an explicit step for the following proof:
lemma "(P ⟶ Q) ⟷ ¬ (P ∧ ¬ Q)"
proof -
have "(P ⟶ Q) = (¬ P ∨ Q)" by(rule imp_conv_disj)
also have "... = (¬ P ∨ ¬ ¬ Q)" by auto (* <== Replace this with an explicit step *)
also have "... = (¬ (P ∧ ¬ Q))" by(rule de_Morgan_conj[symmetric])
finally show "(P ⟶ Q) = (¬ (P ∧ ¬ Q))" .
qed
I would for subsutituing (tactic subst) the theorem that says that ¬ ¬ Q by Q (you know how to use the query panel to find it right?)
Last updated: Dec 21 2024 at 16:20 UTC