Stream: Beginner Questions

Topic: Apply iff theorem in one direction?

Jiahong Lee (Dec 15 2022 at 08:12):

HI, suppose I have a theorem like de_Morgan_conj, how to apply it in a single direction? E.g.

thm de_Morgan_conj

lemma "~ (p ∧ q) ⟷ ~ p ∨ ~ q"
  by(rule de_Morgan_conj) (* Ok *)

lemma "~ (p ∧ q) ⟶ ~ p ∨ ~ q"
  by(rule de_Morgan_conj) (* Error. How to make this work?  *)

Mathias Fleury (Dec 15 2022 at 08:23):

You need to combine the theorem to make it one-sided. So typically de_Morgan_conj[THEN iffD1]

Mathias Fleury (Dec 15 2022 at 08:24):

(in your case you are using ⟶ instead of ⟹ as in de_Morgan_conj[THEN iffD1], so you have to use impI too)

Last updated: Nov 13 2025 at 04:27 UTC