Jiahong Lee (Dec 18 2022 at 13:55): 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]]›)
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]])+
(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: Apr 26 2024 at 20:16 UTC