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?

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]]›)
```

and `THEN (conjunct1,conjunct2)`

does not exist

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]])+
```

(rule applies one of the theorems that matches)

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

Last updated: Oct 12 2024 at 20:18 UTC