# Theory Disjoint_Sets

(*  Author:     Johannes Hölzl, TU München
*)

section ‹Partitions and Disjoint Sets›

theory Disjoint_Sets
imports FuncSet
begin

lemma mono_imp_UN_eq_last: "mono A  (in. A i) = A n"
unfolding mono_def by auto

subsection ‹Set of Disjoint Sets›

abbreviation disjoint :: "'a set set  bool" where "disjoint  pairwise disjnt"

lemma disjoint_def: "disjoint A  (aA. bA. a  b  a  b = {})"
unfolding pairwise_def disjnt_def by auto

lemma disjointI:
"(a b. a  A  b  A  a  b  a  b = {})  disjoint A"
unfolding disjoint_def by auto

lemma disjointD:
"disjoint A  a  A  b  A  a  b  a  b = {}"
unfolding disjoint_def by auto

lemma disjoint_image: "inj_on f (A)  disjoint A  disjoint ((`) f ` A)"
unfolding inj_on_def disjoint_def by blast

lemma assumes "disjoint (A  B)"
shows   disjoint_unionD1: "disjoint A" and disjoint_unionD2: "disjoint B"
using assms by (simp_all add: disjoint_def)

lemma disjoint_INT:
assumes *: "i. i  I  disjoint (F i)"
shows "disjoint {iI. X i | X. iI. X i  F i}"
proof (safe intro!: disjointI del: equalityI)
fix A B :: "'a  'b set" assume "(iI. A i)  (iI. B i)"
then obtain i where "A i  B i" "i  I"
by auto
moreover assume "iI. A i  F i" "iI. B i  F i"
ultimately show "(iI. A i)  (iI. B i) = {}"
using *[OF iI, THEN disjointD, of "A i" "B i"]
by (auto simp flip: INT_Int_distrib)
qed

lemma diff_Union_pairwise_disjoint:
assumes  "  𝒜"
shows "𝒜 -  = (𝒜 - )"
proof -
have "False"
if x: "x  A" "x  B" and AB: "A  𝒜" "A  " "B  " for x A B
proof -
have "A  B = {}"
using assms disjointD AB by blast
with x show ?thesis
by blast
qed
then show ?thesis by auto
qed

lemma Int_Union_pairwise_disjoint:
assumes "pairwise disjnt (𝒜  )"
shows "𝒜   = (𝒜  )"
proof -
have "False"
if x: "x  A" "x  B" and AB: "A  𝒜" "A  " "B  " for x A B
proof -
have "A  B = {}"
using assms disjointD AB by blast
with x show ?thesis
by blast
qed
then show ?thesis by auto
qed

lemma psubset_Union_pairwise_disjoint:
assumes :  and "𝒜   - {{}}"
shows "𝒜  "
unfolding psubset_eq
proof
show "𝒜  "
using assms by blast
have "𝒜  " "( - 𝒜  ( - {{}}))  {}"
using assms by blast+
then show "𝒜  "
using diff_Union_pairwise_disjoint [OF ] by blast
qed

subsubsection "Family of Disjoint Sets"

definition disjoint_family_on :: "('i  'a set)  'i set  bool" where
"disjoint_family_on A S  (mS. nS. m  n  A m  A n = {})"

abbreviation "disjoint_family A  disjoint_family_on A UNIV"

lemma disjoint_family_elem_disjnt:
assumes "infinite A" "finite C"
and df:
obtains x where "x  A" "disjnt C (B x)"
proof -
have "False" if *: "x  A. y. y  C  y  B x"
proof -
obtain g where g: "x  A. g x  C  g x  B x"
using * by metis
with df have "inj_on g A"
by (fastforce simp add: inj_on_def disjoint_family_on_def)
then have "infinite (g ` A)"
using infinite A finite_image_iff by blast
then show False
by (meson finite C finite_subset g image_subset_iff)
qed
then show ?thesis
by (force simp: disjnt_iff intro: that)
qed

lemma disjoint_family_onD:
"disjoint_family_on A I  i  I  j  I  i  j  A i  A j = {}"
by (auto simp: disjoint_family_on_def)

lemma disjoint_family_subset: "disjoint_family A  (x. B x  A x)  disjoint_family B"

lemma disjoint_family_on_insert:
"i  I  disjoint_family_on A (insert i I)  A i  (iI. A i) = {}  disjoint_family_on A I"
by (fastforce simp: disjoint_family_on_def)

lemma disjoint_family_on_bisimulation:
assumes
and "n m. n  S  m  S  n  m  f n  f m = {}  g n  g m = {}"
shows
using assms unfolding disjoint_family_on_def by auto

lemma disjoint_family_on_mono:
"A  B  disjoint_family_on f B  disjoint_family_on f A"
unfolding disjoint_family_on_def by auto

lemma disjoint_family_Suc:
"(n. A n  A (Suc n))  disjoint_family (λi. A (Suc i) - A i)"
using lift_Suc_mono_le[of A]
(metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less less_imp_le)

lemma disjoint_family_on_disjoint_image:
"disjoint_family_on A I  disjoint (A ` I)"
unfolding disjoint_family_on_def disjoint_def by force

lemma disjoint_family_on_vimageI: "disjoint_family_on F I  disjoint_family_on (λi. f -` F i) I"
by (auto simp: disjoint_family_on_def)

lemma disjoint_image_disjoint_family_on:
assumes d: "disjoint (A ` I)" and i: "inj_on A I"
shows
unfolding disjoint_family_on_def
proof (intro ballI impI)
fix n m assume nm: "m  I" "n  I" and "n  m"
with i[THEN inj_onD, of n m] show "A n  A m = {}"
by (intro disjointD[OF d]) auto
qed

lemma disjoint_family_on_iff_disjoint_image:
assumes "i. i  I  A i  {}"
shows "disjoint_family_on A I  disjoint (A ` I)  inj_on A I"
proof
assume
then show "disjoint (A ` I)  inj_on A I"
by (metis (mono_tags, lifting) assms disjoint_family_onD disjoint_family_on_disjoint_image inf.idem inj_onI)
qed (use disjoint_image_disjoint_family_on in metis)

lemma card_UN_disjoint':
assumes  "i. i  I  finite (A i)" "finite I"
shows "card (iI. A i) = (iI. card (A i))"
using assms   by (simp add: card_UN_disjoint disjoint_family_on_def)

lemma disjoint_UN:
assumes F: "i. i  I  disjoint (F i)" and *: "disjoint_family_on (λi. (F i)) I"
shows "disjoint (iI. F i)"
proof (safe intro!: disjointI del: equalityI)
fix A B i j assume "A  B" "A  F i" "i  I" "B  F j" "j  I"
show "A  B = {}"
proof cases
assume "i = j" with F[of i] i  I A  F i B  F j A  B show "A  B = {}"
by (auto dest: disjointD)
next
assume "i  j"
with * iI jI have "((F i))  ((F j)) = {}"
by (rule disjoint_family_onD)
with AF i iI BF j jI
show "A  B = {}"
by auto
qed
qed

lemma distinct_list_bind:
assumes "distinct xs" "x. x  set xs  distinct (f x)"
"disjoint_family_on (set  f) (set xs)"
shows   "distinct (List.bind xs f)"
using assms
by (induction xs)
(auto simp: disjoint_family_on_def distinct_map inj_on_def set_list_bind)

lemma bij_betw_UNION_disjoint:
assumes disj: "disjoint_family_on A' I"
assumes bij: "i. i  I  bij_betw f (A i) (A' i)"
shows   "bij_betw f (iI. A i) (iI. A' i)"
unfolding bij_betw_def
proof
from bij show eq: "f ` (A ` I) = (A' ` I)"
by (auto simp: bij_betw_def image_UN)
show "inj_on f ((A ` I))"
proof (rule inj_onI, clarify)
fix i j x y assume A: "i  I" "j  I" "x  A i" "y  A j" and B: "f x = f y"
from A bij[of i] bij[of j] have "f x  A' i" "f y  A' j"
by (auto simp: bij_betw_def)
with B have "A' i  A' j  {}" by auto
with disj A have "i = j" unfolding disjoint_family_on_def by blast
with A B bij[of i] show "x = y" by (auto simp: bij_betw_def dest: inj_onD)
qed
qed

lemma disjoint_union: "disjoint C  disjoint B  C  B = {}  disjoint (C  B)"
using disjoint_UN[of "{C, B}" "λx. x"] by (auto simp add: disjoint_family_on_def)

text ‹
Sum/product of the union of a finite disjoint family
›
context comm_monoid_set
begin

lemma UNION_disjoint_family:
assumes "finite I" and "iI. finite (A i)"
and
shows "F g ((A ` I)) = F (λx. F g (A x)) I"
using assms unfolding disjoint_family_on_def  by (rule UNION_disjoint)

lemma Union_disjoint_sets:
assumes "AC. finite A" and "disjoint C"
shows "F g (C) = (F  F) g C"
using assms unfolding disjoint_def  by (rule Union_disjoint)

end

text ‹
The union of an infinite disjoint family of non-empty sets is infinite.
›
lemma infinite_disjoint_family_imp_infinite_UNION:
assumes "¬finite A" "x. x  A  f x  {}"
shows   "¬finite ((f ` A))"
proof -
define g where "g x = (SOME y. y  f x)" for x
have g: "g x  f x" if "x  A" for x
unfolding g_def by (rule someI_ex, insert assms(2) that) blast
have inj_on_g: "inj_on g A"
proof (rule inj_onI, rule ccontr)
fix x y assume A: "x  A" "y  A" "g x = g y" "x  y"
with g[of x] g[of y] have "g x  f x" "g x  f y" by auto
with A x  y assms show False
by (auto simp: disjoint_family_on_def inj_on_def)
qed
from g have "g ` A  (f ` A)" by blast
moreover from inj_on_g ¬finite A have "¬finite (g ` A)"
using finite_imageD by blast
ultimately show ?thesis using finite_subset by blast
qed

subsection ‹Construct Disjoint Sequences›

definition disjointed :: "(nat  'a set)  nat  'a set" where
"disjointed A n = A n - (i{0..<n}. A i)"

lemma finite_UN_disjointed_eq: "(i{0..<n}. disjointed A i) = (i{0..<n}. A i)"
proof (induct n)
case 0 show ?case by simp
next
case (Suc n)
thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
qed

lemma UN_disjointed_eq: "(i. disjointed A i) = (i. A i)"
by (rule UN_finite2_eq [where k=])

lemma less_disjoint_disjointed: "m < n  disjointed A m  disjointed A n = {}"

lemma disjoint_family_disjointed:
(metis neq_iff Int_commute less_disjoint_disjointed)

lemma disjointed_subset: "disjointed A n  A n"

lemma disjointed_0[simp]: "disjointed A 0 = A 0"

lemma disjointed_mono: "mono A  disjointed A (Suc n) = A (Suc n) - A n"
using mono_imp_UN_eq_last[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)

subsection ‹Partitions›

text ‹
Partitions termP of a set termA. We explicitly disallow empty sets.
›

definition partition_on :: "'a set  'a set set  bool"
where
"partition_on A P  P = A  disjoint P  {}  P"

lemma partition_onI:
"P = A  (p q. p  P  q  P  p  q  disjnt p q)  {}  P  partition_on A P"
by (auto simp: partition_on_def pairwise_def)

lemma partition_onD1: "partition_on A P  A = P"
by (auto simp: partition_on_def)

lemma partition_onD2: "partition_on A P  disjoint P"
by (auto simp: partition_on_def)

lemma partition_onD3: "partition_on A P  {}  P"
by (auto simp: partition_on_def)

subsection ‹Constructions of partitions›

lemma partition_on_empty:
unfolding partition_on_def by fastforce

lemma partition_on_space: "A  {}  partition_on A {A}"
by (auto simp: partition_on_def disjoint_def)

lemma partition_on_singletons: "partition_on A ((λx. {x}) ` A)"
by (auto simp: partition_on_def disjoint_def)

lemma partition_on_transform:
assumes P: "partition_on A P"
assumes F_UN: "(F ` P) = F (P)" and F_disjnt: "p q. p  P  q  P  disjnt p q  disjnt (F p) (F q)"
shows "partition_on (F A) (F ` P - {{}})"
proof -
have "(F ` P - {{}}) = F A"
unfolding P[THEN partition_onD1] F_UN[symmetric] by auto
with P show ?thesis
by (auto simp add: partition_on_def pairwise_def intro!: F_disjnt)
qed

lemma partition_on_restrict: "partition_on A P  partition_on (B  A) ((∩) B ` P - {{}})"
by (intro partition_on_transform) (auto simp: disjnt_def)

lemma partition_on_vimage: "partition_on A P  partition_on (f -` A) ((-`) f ` P - {{}})"
by (intro partition_on_transform) (auto simp: disjnt_def)

lemma partition_on_inj_image:
assumes P: "partition_on A P" and f: "inj_on f A"
shows "partition_on (f ` A) ((`) f ` P - {{}})"
proof (rule partition_on_transform[OF P])
show "p  P  q  P  disjnt p q  disjnt (f ` p) (f ` q)" for p q
using f[THEN inj_onD] P[THEN partition_onD1] by (auto simp: disjnt_def)
qed auto

lemma partition_on_insert:
assumes "disjnt p (P)"
shows "partition_on A (insert p P)  partition_on (A-p) P  p  A  p  {}"
using assms
by (auto simp: partition_on_def disjnt_iff pairwise_insert)

subsection ‹Finiteness of partitions›

lemma finitely_many_partition_on:
assumes "finite A"
shows "finite {P. partition_on A P}"
proof (rule finite_subset)
show "{P. partition_on A P}  Pow (Pow A)"
unfolding partition_on_def by auto
show "finite (Pow (Pow A))"
using assms by simp
qed

lemma finite_elements: "finite A  partition_on A P  finite P"
using partition_onD1[of A P] by (simp add: finite_UnionD)

lemma product_partition:
assumes "partition_on A P" and "p. p  P  finite p"
shows "card A = (pP. card p)"
using assms unfolding partition_on_def  by (meson card_Union_disjoint)

subsection ‹Equivalence of partitions and equivalence classes›

lemma partition_on_quotient:
assumes r: "equiv A r"
shows "partition_on A (A // r)"
proof (rule partition_onI)
from r have "refl_on A r"
by (auto elim: equivE)
then show "(A // r) = A" "{}  A // r"
by (auto simp: refl_on_def quotient_def)

fix p q assume "p  A // r" "q  A // r" "p  q"
then obtain x y where "x  A" "y  A" "p = r `` {x}" "q = r `` {y}"
by (auto simp: quotient_def)
with r equiv_class_eq_iff[OF r, of x y] p  q show "disjnt p q"
by (auto simp: disjnt_equiv_class)
qed

lemma equiv_partition_on:
assumes P: "partition_on A P"
shows "equiv A {(x, y). p  P. x  p  y  p}"
proof (rule equivI)
have "A = P"
using P by (auto simp: partition_on_def)

have "{(x, y). p  P. x  p  y  p}  A × A"
unfolding A = P by blast
then show "refl_on A {(x, y). pP. x  p  y  p}"
unfolding refl_on_def A = P by auto
next
show "trans {(x, y). pP. x  p  y  p}"
using P by (auto simp only: trans_def disjoint_def partition_on_def)
next
show "sym {(x, y). pP. x  p  y  p}"
by (auto simp only: sym_def)
qed

lemma partition_on_eq_quotient:
assumes P: "partition_on A P"
shows "A // {(x, y). p  P. x  p  y  p} = P"
unfolding quotient_def
proof safe
fix x assume "x  A"
then obtain p where "p  P" "x  p" "q. q  P  x  q  p = q"
using P by (auto simp: partition_on_def disjoint_def)
then have "{y. pP. x  p  y  p} = p"
by (safe intro!: bexI[of _ p]) simp
then show "{(x, y). pP. x  p  y  p} `` {x}  P"
next
fix p assume "p  P"
then have "p  {}"
using P by (auto simp: partition_on_def)
then obtain x where "x  p"
by auto
then have "x  A" "q. q  P  x  q  p = q"
using P p  P by (auto simp: partition_on_def disjoint_def)
with pP x  p have "{y. pP. x  p  y  p} = p"
by (safe intro!: bexI[of _ p]) simp
then show "p  (xA. {{(x, y). pP. x  p  y  p} `` {x}})"
by (auto intro: x  A)
qed

lemma partition_on_alt: "partition_on A P  (r. equiv A r  P = A // r)"
by (auto simp: partition_on_eq_quotient intro!: partition_on_quotient intro: equiv_partition_on)

subsection ‹Refinement of partitions›

definition refines :: "'a set  'a set set  'a set set  bool"
where "refines A P Q
partition_on A P  partition_on A Q  (XP. YQ. X  Y)"

lemma refines_refl: "partition_on A P  refines A P P"
using refines_def by blast

lemma refines_asym1:
assumes "refines A P Q" "refines A Q P"
shows "P  Q"
proof
fix X
assume "X  P"
then obtain Y X' where "Y  Q" "X  Y" "X'  P" "Y  X'"
by (meson assms refines_def)
then have "X' = X"
using assms(2) unfolding partition_on_def refines_def
by (metis X  P X  Y disjnt_self_iff_empty disjnt_subset1 pairwiseD)
then show "X  Q"
using X  Y Y  Q Y  X' by force
qed

lemma refines_asym: "refines A P Q; refines A Q P  P=Q"
by (meson antisym_conv refines_asym1)

lemma refines_trans: "refines A P Q; refines A Q R  refines A P R"
by (meson order.trans refines_def)

lemma refines_obtains_subset:
assumes "refines A P Q" "q  Q"
shows "partition_on q {p  P. p  q}"
proof -
have "p  q  disjnt p q" if "p  P" for p
using that assms unfolding refines_def partition_on_def disjoint_def
by (metis disjnt_def disjnt_subset1)
with assms have "q  Union {p  P. p  q}"
using assms
by (clarsimp simp: refines_def disjnt_iff partition_on_def) (metis Union_iff)
with assms have "q = Union {p  P. p  q}"
by auto
then show ?thesis
using assms by (auto simp: refines_def disjoint_def partition_on_def)
qed

subsection ‹The coarsest common refinement of a set of partitions›

definition common_refinement :: "'a set set set  'a set set"
where "common_refinement 𝒫  (f  (ΠE P𝒫. P). { (f ` 𝒫)}) - {{}}"

text ‹With non-extensional function space›
lemma common_refinement: "common_refinement 𝒫 = (f  (Π P𝒫. P). { (f ` 𝒫)}) - {{}}"
(is "?lhs = ?rhs")
proof
show "?rhs  ?lhs"
apply (clarsimp simp add: common_refinement_def PiE_def Ball_def)
by (metis restrict_Pi_cancel image_restrict_eq restrict_extensional)
qed (auto simp add: common_refinement_def PiE_def)

lemma common_refinement_exists: "X  common_refinement 𝒫; P  𝒫  RP. X  R"

lemma Union_common_refinement: " (common_refinement 𝒫) = ( P𝒫. P)"
proof
show "( P𝒫. P)   (common_refinement 𝒫)"
proof (clarsimp simp: common_refinement)
fix x
assume "P𝒫. XP. x  X"
then obtain F where F: "P. P𝒫  F P  P  x  F P"
by metis
then have "x   (F ` 𝒫)"
by force
with F show "X(xΠ P𝒫. P. { (x ` 𝒫)}) - {{}}. x  X"
by (auto simp add: Pi_iff Bex_def)
qed
qed (auto simp: common_refinement_def)

lemma partition_on_common_refinement:
assumes A: "P. P  𝒫  partition_on A P" and "𝒫  {}"
shows
proof (rule partition_onI)
show " (common_refinement 𝒫) = A"
using assms by (simp add: partition_on_def Union_common_refinement)
fix P Q
assume  and  and "P  Q"
then obtain f g where f: "f  (ΠE P𝒫. P)" and P: "P =  (f ` 𝒫)" and "P  {}"
and   g: "g  (ΠE P𝒫. P)" and Q: "Q =  (g ` 𝒫)" and "Q  {}"
have "f=g" if "x  P" "x  Q" for x
proof (rule extensionalityI [of _ 𝒫])
fix R
assume "R  𝒫"
with that P Q f g A [unfolded partition_on_def, OF R  𝒫]
show "f R = g R"
by (metis INT_E Int_iff PiE_iff disjointD emptyE)
qed (use PiE_iff f g in auto)
then show "disjnt P Q"
by (metis P Q P  Q disjnt_iff)

lemma refines_common_refinement:
assumes "P. P  𝒫  partition_on A P" "P  𝒫"
shows "refines A (common_refinement 𝒫) P"
unfolding refines_def
proof (intro conjI strip)
fix X
assume
with assms show "YP. X  Y"
by (auto simp: common_refinement_def)
qed (use assms partition_on_common_refinement in auto)

text ‹The common refinement is itself refined by any other›
lemma common_refinement_coarsest:
assumes "P. P  𝒫  partition_on A P" "partition_on A R" "P. P  𝒫  refines A R P" "𝒫  {}"
shows "refines A R (common_refinement 𝒫)"
unfolding refines_def
proof (intro conjI ballI partition_on_common_refinement)
fix X
assume "X  R"
have "p  P. X  p" if "P  𝒫" for P
by (meson X  R assms(3) refines_def that)
then obtain F where f: "P. P  𝒫  F P  P  X  F P"
by metis
with partition_on A R X  R 𝒫  {}
have " (F ` 𝒫)  common_refinement 𝒫"
apply (simp add: partition_on_def common_refinement Pi_iff Bex_def)
by (metis (no_types, lifting) cINF_greatest subset_empty)
with f show "Ycommon_refinement 𝒫. X  Y"
by (metis 𝒫  {} cINF_greatest)
qed (use assms in auto)

lemma finite_common_refinement:
assumes "finite 𝒫" "P. P  𝒫  finite P"
shows
proof -
have "finite (ΠE P𝒫. P)"
then show ?thesis
by (auto simp: common_refinement_def)
qed

lemma card_common_refinement:
assumes "finite 𝒫" "P. P  𝒫  finite P"
shows "card (common_refinement 𝒫)  (P  𝒫. card P)"
proof -
have "card (common_refinement 𝒫)  card (f  (ΠE P𝒫. P). { (f ` 𝒫)})"
unfolding common_refinement_def by (meson card_Diff1_le)
also have "  (f(ΠE P𝒫. P). card{ (f ` 𝒫)})"
by (metis assms finite_PiE card_UN_le)
also have " = card(ΠE P𝒫. P)"
by simp
also have " = (P  𝒫. card P)"
by (simp add: assms(1) card_PiE dual_order.eq_iff)
finally show ?thesis .
qed

end