Stream: Beginner Questions

Topic: ✔ Apply iff theorem in one direction?

Jiahong Lee (Dec 15 2022 at 14:54):

That helps a lot, thank you very much!

Jiahong Lee (Dec 15 2022 at 14:55):

With the given hint, I can complete my proof as follow:

lemma "~ (p ∧ q) ⟶ ~ p ∨ ~ q"
  apply(rule impI)
  apply(rule de_Morgan_conj[THEN iffD1])
  apply assumption
  done

lemma "~ (p ∧ q) ⟹ ~ p ∨ ~ q"
  by(rule de_Morgan_conj[THEN iffD1])

Hope that it helps!

Notification Bot (Dec 15 2022 at 14:56):

Jiahong Lee has marked this topic as resolved.

Mathias Fleury (Dec 15 2022 at 15:03):

de_Morgan_conj[THEN iffD1, THEN impI] works too

Wolfgang Jeltsch (Dec 16 2022 at 21:19):

Let me add that ⟷ is just an “abbreviation” of =, with the type restricted to bool ⇒ bool ⇒ bool. Therefore, you can use logical equivalence statements (those phrased with ⟷) as rewrite rules with all the tools that provide rewriting: unfolding constructs and the proof methods subst, unfold, simp, auto, fastforce, slowsimp, bestsimp, and force.

Wolfgang Jeltsch (Dec 16 2022 at 21:23):

For example, if you would phrase your second lemma as an Isabelle/Pure implication, where trivial implications P ⟹ P are automatically discharged by Isar, you could prove it via unfolding:

lemma "~ (p ∧ q) ⟹ ~ p ∨ ~ q"
  unfolding de_Morgan_conj .

Wolfgang Jeltsch (Dec 16 2022 at 21:25):

If you want to use Isabelle/HOL’s implication operator, you could write the following:

lemma "~ (p ∧ q) ⟶ ~ p ∨ ~ q"
  unfolding de_Morgan_conj using imp_refl .

Last updated: Apr 16 2024 at 08:18 UTC