Stream: Beginner Questions

Topic: ✔ How to break down these conjuncts directly?

Jiahong Lee (Dec 20 2022 at 01:57):

Hmm, this is more convoluted than what I expected

Jiahong Lee (Dec 20 2022 at 02:04):

Still, I prefer an explicit step/proof method over auto. Using HOL-Eisbach.Eisbach, this is good enough for me:

method splitconj uses rule =
 (rule conjunct1[OF rule], rule conjunct2[OF rule])

hence 2: "x ∈ A ∪ B" and 3: "x ∉ B"
  by(splitconj rule: Diff_iff[THEN iffD1]) (* Ok! *)

Jiahong Lee (Dec 20 2022 at 02:04):

Thanks!

Notification Bot (Dec 20 2022 at 02:04):

Jiahong Lee has marked this topic as resolved.

Last updated: Dec 21 2024 at 16:20 UTC