# Theory Disjoint_Sets

theory Disjoint_Sets
imports Main
```(*  Title:      HOL/Library/Disjoint_Sets.thy
Author:     Johannes Hölzl, TU München
*)

section ‹Partitions and Disjoint Sets›

theory Disjoint_Sets
imports Main
begin

lemma range_subsetD: "range f ⊆ B ⟹ f i ∈ B"
by blast

lemma Int_Diff_disjoint: "A ∩ B ∩ (A - B) = {}"
by blast

lemma Int_Diff_Un: "A ∩ B ∪ (A - B) = A"
by blast

lemma mono_Un: "mono A ⟹ (⋃i≤n. A i) = A n"
unfolding mono_def by auto

lemma disjnt_equiv_class: "equiv A r ⟹ disjnt (r``{a}) (r``{b}) ⟷ (a, b) ∉ r"
by (auto dest: equiv_class_self simp: equiv_class_eq_iff disjnt_def)

subsection ‹Set of Disjoint Sets›

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

lemma disjoint_def: "disjoint A ⟷ (∀a∈A. ∀b∈A. 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 {⋂i∈I. X i | X. ∀i∈I. X i ∈ F i}"
proof (safe intro!: disjointI del: equalityI)
fix A B :: "'a ⇒ 'b set" assume "(⋂i∈I. A i) ≠ (⋂i∈I. B i)"
then obtain i where "A i ≠ B i" "i ∈ I"
by auto
moreover assume "∀i∈I. A i ∈ F i" "∀i∈I. B i ∈ F i"
ultimately show "(⋂i∈I. A i) ∩ (⋂i∈I. B i) = {}"
using *[OF ‹i∈I›, THEN disjointD, of "A i" "B i"]
by (auto simp flip: INT_Int_distrib)
qed

subsubsection "Family of Disjoint Sets"

definition disjoint_family_on :: "('i ⇒ 'a set) ⇒ 'i set ⇒ bool" where
"disjoint_family_on A S ⟷ (∀m∈S. ∀n∈S. 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: "disjoint_family_on B A"
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_bisimulation:
assumes "disjoint_family_on f S"
and "⋀n m. n ∈ S ⟹ m ∈ S ⟹ n ≠ m ⟹ f n ∩ f m = {} ⟹ g n ∩ g m = {}"
shows "disjoint_family_on g S"
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 "disjoint_family_on A I"
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_UN:
assumes F: "⋀i. i ∈ I ⟹ disjoint (F i)" and *: "disjoint_family_on (λi. ⋃F i) I"
shows "disjoint (⋃i∈I. 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 * ‹i∈I› ‹j∈I› have "(⋃F i) ∩ (⋃F j) = {}"
by (rule disjoint_family_onD)
with ‹A∈F i› ‹i∈I› ‹B∈F j› ‹j∈I›
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 (⋃i∈I. A i) (⋃i∈I. A' i)"
unfolding bij_betw_def
proof
from bij show eq: "f ` UNION I A = UNION I A'"
by (auto simp: bij_betw_def image_UN)
show "inj_on f (UNION I A)"
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 ‹
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 ≠ {}" "disjoint_family_on f A"
shows   "¬finite (UNION A f)"
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 ⊆ UNION A f" 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=0])

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

lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
(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_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)

subsection ‹Partitions›

text ‹
Partitions @{term P} of a set @{term A}. 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: "partition_on {} P ⟷ P = {}"
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

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)

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" "disjoint P" "{} ∉ P"
using P by (auto simp: partition_on_def)
then show "refl_on A {(x, y). ∃p∈P. x ∈ p ∧ y ∈ p}"
unfolding refl_on_def by auto
show "trans {(x, y). ∃p∈P. x ∈ p ∧ y ∈ p}"
using ‹disjoint P› by (auto simp: trans_def disjoint_def)
qed (auto simp: sym_def)

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. ∃p∈P. x ∈ p ∧ y ∈ p} = p"
by (safe intro!: bexI[of _ p]) simp
then show "{(x, y). ∃p∈P. x ∈ p ∧ y ∈ p} `` {x} ∈ P"
by (simp add: ‹p ∈ 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 ‹p∈P› ‹x ∈ p› have "{y. ∃p∈P. x ∈ p ∧ y ∈ p} = p"
by (safe intro!: bexI[of _ p]) simp
then show "p ∈ (⋃x∈A. {{(x, y). ∃p∈P. 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)

end
```