## Stream: Beginner Questions

### Topic: How to break down these conjuncts directly?

#### Jiahong Lee (Dec 18 2022 at 13:55):

Hi, in my structured proof, I have `"P /\ Q"` as my intermediate state, but I'd like to have `"P" and "Q"` directly. E.g.

``````theorem "(A ∪ B) - B ⊆ A"
proof (rule subsetI)
fix x assume 1: "x ∈ (A ∪ B) - B"
hence "x ∈ A ∪ B ∧ x ∉ B" by(rule Diff_iff[THEN iffD1]) (* <=== This line is redundant *)
hence 2: "x ∈ A ∪ B" and 3: "x ∉ B" by(rule conjunct1, rule conjunct2)
oops
``````

I want to simplify it into:

``````theorem "(A ∪ B) - B ⊆ A"
proof (rule subsetI)
fix x assume 1: "x ∈ (A ∪ B) - B"
hence 2: "x ∈ A ∪ B" and 3: "x ∉ B" by(rule Diff_iff[THEN iffD1[THEN (conjunct1,conjunct2)]]) (* Error, doesn't work! *)
oops
``````

What is the correct proof method composition for my case?

#### Mathias Fleury (Dec 19 2022 at 09:08):

the hence only threads the fact to the first rule, not the second:

``````  hence 2: "x ∈ A ∪ B" and 3: "x ∉ B"
by (rule Diff_iff[THEN iffD1[THEN conjunct1]])
(use 1 in ‹rule Diff_iff[THEN iffD1[THEN conjunct2]]›)
``````

#### Mathias Fleury (Dec 19 2022 at 09:08):

and `THEN (conjunct1,conjunct2)` does not exist

#### Mathias Fleury (Dec 19 2022 at 09:09):

but you could go for

``````  hence 2: "x ∈ A ∪ B" and 3: "x ∉ B"
by (rule Diff_iff[THEN iffD1[THEN conjunct1]] Diff_iff[THEN iffD1[THEN conjunct2]])+
``````

#### Mathias Fleury (Dec 19 2022 at 09:09):

(rule applies one of the theorems that matches)

#### Mathias Fleury (Dec 19 2022 at 09:09):

that being said, you should not do that and use auto instead

Last updated: Sep 11 2024 at 16:22 UTC