theory Lib

lemma Diff_Un2:
  assumes emptyad: "A \<inter> D = {}"
  and     emptybc: "B \<inter> C = {}"
  shows   "(A \<union> B) - (C \<union> D) = (A - C) \<union> (B - D)" proof - have "(A \<union> B) - (C \<union> D) = (A \<union> B - C) \<inter> (A \<union> B - D)" by (rule Diff_Un) also have "\<dots> = ((A - C) \<union> B) \<inter> (A \<union> (B - D))" using emptyad emptybc by (simp add: Un_Diff Diff_triv) also have "\<dots> = (A - C) \<union> (B - D)" proof - have "(A - C) \<inter> (A \<union> (B - D)) = A - C" using  emptyad emptybc by (metis Diff_Int2 Diff_Int_distrib2 inf_sup_absorb) moreover have "B \<inter> (A \<union> (B - D)) = B - D" using emptyad emptybc by (metis Int_Diff Un_Diff Un_Diff_Int Un_commute Un_empty_left inf_sup_absorb) ultimately show ?thesis by (simp add: Int_Un_distrib2) qed finally show ?thesis . qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<union> B - (C \<union> D) = A - C \<union> (B - D) proof (state)
goal (1 subgoal):
 1. A \<union> B - (C \<union> D) = A - C \<union> (B - D) proof (prove)
goal (1 subgoal):
 1. A \<union> B - (C \<union> D) = (A \<union> B - C) \<inter> (A \<union> B - D) proof (state)
this:
A \<union> B - (C \<union> D) = (A \<union> B - C) \<inter> (A \<union> B - D)

goal (1 subgoal):
 1. A \<union> B - (C \<union> D) = A - C \<union> (B - D) proof (state)
this:
A \<union> B - (C \<union> D) = (A \<union> B - C) \<inter> (A \<union> B - D)

goal (1 subgoal):
 1. A \<union> B - (C \<union> D) = A - C \<union> (B - D) proof (prove)
goal (1 subgoal):
 1. (A \<union> B - C) \<inter> (A \<union> B - D) = (A - C \<union> B) \<inter> (A \<union> (B - D)) proof (prove)
using this:
A \<inter> D = {}
B \<inter> C = {}

goal (1 subgoal):
 1. (A \<union> B - C) \<inter> (A \<union> B - D) = (A - C \<union> B) \<inter> (A \<union> (B - D)) proof (state)
this:
(A \<union> B - C) \<inter> (A \<union> B - D) = (A - C \<union> B) \<inter> (A \<union> (B - D))

goal (1 subgoal):
 1. A \<union> B - (C \<union> D) = A - C \<union> (B - D) proof (state)
this:
(A \<union> B - C) \<inter> (A \<union> B - D) = (A - C \<union> B) \<inter> (A \<union> (B - D))

goal (1 subgoal):
 1. A \<union> B - (C \<union> D) = A - C \<union> (B - D) proof (prove)
goal (1 subgoal):
 1. (A - C \<union> B) \<inter> (A \<union> (B - D)) = A - C \<union> (B - D) proof (state)
goal (1 subgoal):
 1. (A - C \<union> B) \<inter> (A \<union> (B - D)) = A - C \<union> (B - D) proof (prove)
goal (1 subgoal):
 1. (A - C) \<inter> (A \<union> (B - D)) = A - C proof (prove)
using this:
A \<inter> D = {}
B \<inter> C = {}

goal (1 subgoal):
 1. (A - C) \<inter> (A \<union> (B - D)) = A - C proof (state)
this:
(A - C) \<inter> (A \<union> (B - D)) = A - C

goal (1 subgoal):
 1. (A - C \<union> B) \<inter> (A \<union> (B - D)) = A - C \<union> (B - D) proof (state)
this:
(A - C) \<inter> (A \<union> (B - D)) = A - C

goal (1 subgoal):
 1. (A - C \<union> B) \<inter> (A \<union> (B - D)) = A - C \<union> (B - D) proof (prove)
goal (1 subgoal):
 1. B \<inter> (A \<union> (B - D)) = B - D proof (prove)
using this:
A \<inter> D = {}
B \<inter> C = {}

goal (1 subgoal):
 1. B \<inter> (A \<union> (B - D)) = B - D proof (state)
this:
B \<inter> (A \<union> (B - D)) = B - D

goal (1 subgoal):
 1. (A - C \<union> B) \<inter> (A \<union> (B - D)) = A - C \<union> (B - D) proof (chain)
picking this:
(A - C) \<inter> (A \<union> (B - D)) = A - C
B \<inter> (A \<union> (B - D)) = B - D proof (prove)
using this:
(A - C) \<inter> (A \<union> (B - D)) = A - C
B \<inter> (A \<union> (B - D)) = B - D

goal (1 subgoal):
 1. (A - C \<union> B) \<inter> (A \<union> (B - D)) = A - C \<union> (B - D) proof (state)
this:
(A - C \<union> B) \<inter> (A \<union> (B - D)) = A - C \<union> (B - D)

goal:
No subgoals! proof (state)
this:
(A - C \<union> B) \<inter> (A \<union> (B - D)) = A - C \<union> (B - D)

goal (1 subgoal):
 1. A \<union> B - (C \<union> D) = A - C \<union> (B - D) proof (chain)
picking this:
A \<union> B - (C \<union> D) = A - C \<union> (B - D) proof (prove)
using this:
A \<union> B - (C \<union> D) = A - C \<union> (B - D)

goal (1 subgoal):
 1. A \<union> B - (C \<union> D) = A - C \<union> (B - D) proof (state)
this:
A \<union> B - (C \<union> D) = A - C \<union> (B - D)

goal:
No subgoals!