src/HOL/Library/Disjoint_Sets.thy
 author wenzelm Tue May 15 13:57:39 2018 +0200 (16 months ago) changeset 68189 6163c90694ef parent 67399 eab6ce8368fa child 68406 6beb45f6cf67 permissions -rw-r--r--
1 (*  Title:      HOL/Library/Disjoint_Sets.thy
2     Author:     Johannes Hölzl, TU München
3 *)
5 section \<open>Partitions and Disjoint Sets\<close>
7 theory Disjoint_Sets
8   imports Main
9 begin
11 lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
12   by blast
14 lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
15   by blast
17 lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
18   by blast
20 lemma mono_Un: "mono A \<Longrightarrow> (\<Union>i\<le>n. A i) = A n"
21   unfolding mono_def by auto
23 lemma disjnt_equiv_class: "equiv A r \<Longrightarrow> disjnt (r``{a}) (r``{b}) \<longleftrightarrow> (a, b) \<notin> r"
24   by (auto dest: equiv_class_self simp: equiv_class_eq_iff disjnt_def)
26 subsection \<open>Set of Disjoint Sets\<close>
28 abbreviation disjoint :: "'a set set \<Rightarrow> bool" where "disjoint \<equiv> pairwise disjnt"
30 lemma disjoint_def: "disjoint A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. a \<noteq> b \<longrightarrow> a \<inter> b = {})"
31   unfolding pairwise_def disjnt_def by auto
33 lemma disjointI:
34   "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}) \<Longrightarrow> disjoint A"
35   unfolding disjoint_def by auto
37 lemma disjointD:
38   "disjoint A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}"
39   unfolding disjoint_def by auto
41 lemma disjoint_image: "inj_on f (\<Union>A) \<Longrightarrow> disjoint A \<Longrightarrow> disjoint ((`) f ` A)"
42   unfolding inj_on_def disjoint_def by blast
44 lemma assumes "disjoint (A \<union> B)"
45       shows   disjoint_unionD1: "disjoint A" and disjoint_unionD2: "disjoint B"
46   using assms by (simp_all add: disjoint_def)
48 lemma disjoint_INT:
49   assumes *: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)"
50   shows "disjoint {\<Inter>i\<in>I. X i | X. \<forall>i\<in>I. X i \<in> F i}"
51 proof (safe intro!: disjointI del: equalityI)
52   fix A B :: "'a \<Rightarrow> 'b set" assume "(\<Inter>i\<in>I. A i) \<noteq> (\<Inter>i\<in>I. B i)"
53   then obtain i where "A i \<noteq> B i" "i \<in> I"
54     by auto
55   moreover assume "\<forall>i\<in>I. A i \<in> F i" "\<forall>i\<in>I. B i \<in> F i"
56   ultimately show "(\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i) = {}"
57     using *[OF \<open>i\<in>I\<close>, THEN disjointD, of "A i" "B i"]
58     by (auto simp: INT_Int_distrib[symmetric])
59 qed
61 subsubsection "Family of Disjoint Sets"
63 definition disjoint_family_on :: "('i \<Rightarrow> 'a set) \<Rightarrow> 'i set \<Rightarrow> bool" where
64   "disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
66 abbreviation "disjoint_family A \<equiv> disjoint_family_on A UNIV"
68 lemma disjoint_family_elem_disjnt:
69   assumes "infinite A" "finite C"
70       and df: "disjoint_family_on B A"
71   obtains x where "x \<in> A" "disjnt C (B x)"
72 proof -
73   have "False" if *: "\<forall>x \<in> A. \<exists>y. y \<in> C \<and> y \<in> B x"
74   proof -
75     obtain g where g: "\<forall>x \<in> A. g x \<in> C \<and> g x \<in> B x"
76       using * by metis
77     with df have "inj_on g A"
78       by (fastforce simp add: inj_on_def disjoint_family_on_def)
79     then have "infinite (g ` A)"
80       using \<open>infinite A\<close> finite_image_iff by blast
81     then show False
82       by (meson \<open>finite C\<close> finite_subset g image_subset_iff)
83   qed
84   then show ?thesis
85     by (force simp: disjnt_iff intro: that)
86 qed
88 lemma disjoint_family_onD:
89   "disjoint_family_on A I \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
90   by (auto simp: disjoint_family_on_def)
92 lemma disjoint_family_subset: "disjoint_family A \<Longrightarrow> (\<And>x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
93   by (force simp add: disjoint_family_on_def)
95 lemma disjoint_family_on_bisimulation:
96   assumes "disjoint_family_on f S"
97   and "\<And>n m. n \<in> S \<Longrightarrow> m \<in> S \<Longrightarrow> n \<noteq> m \<Longrightarrow> f n \<inter> f m = {} \<Longrightarrow> g n \<inter> g m = {}"
98   shows "disjoint_family_on g S"
99   using assms unfolding disjoint_family_on_def by auto
101 lemma disjoint_family_on_mono:
102   "A \<subseteq> B \<Longrightarrow> disjoint_family_on f B \<Longrightarrow> disjoint_family_on f A"
103   unfolding disjoint_family_on_def by auto
105 lemma disjoint_family_Suc:
106   "(\<And>n. A n \<subseteq> A (Suc n)) \<Longrightarrow> disjoint_family (\<lambda>i. A (Suc i) - A i)"
107   using lift_Suc_mono_le[of A]
108   by (auto simp add: disjoint_family_on_def)
109      (metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less less_imp_le)
111 lemma disjoint_family_on_disjoint_image:
112   "disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)"
113   unfolding disjoint_family_on_def disjoint_def by force
115 lemma disjoint_family_on_vimageI: "disjoint_family_on F I \<Longrightarrow> disjoint_family_on (\<lambda>i. f -` F i) I"
116   by (auto simp: disjoint_family_on_def)
118 lemma disjoint_image_disjoint_family_on:
119   assumes d: "disjoint (A ` I)" and i: "inj_on A I"
120   shows "disjoint_family_on A I"
121   unfolding disjoint_family_on_def
122 proof (intro ballI impI)
123   fix n m assume nm: "m \<in> I" "n \<in> I" and "n \<noteq> m"
124   with i[THEN inj_onD, of n m] show "A n \<inter> A m = {}"
125     by (intro disjointD[OF d]) auto
126 qed
128 lemma disjoint_UN:
129   assumes F: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)" and *: "disjoint_family_on (\<lambda>i. \<Union>F i) I"
130   shows "disjoint (\<Union>i\<in>I. F i)"
131 proof (safe intro!: disjointI del: equalityI)
132   fix A B i j assume "A \<noteq> B" "A \<in> F i" "i \<in> I" "B \<in> F j" "j \<in> I"
133   show "A \<inter> B = {}"
134   proof cases
135     assume "i = j" with F[of i] \<open>i \<in> I\<close> \<open>A \<in> F i\<close> \<open>B \<in> F j\<close> \<open>A \<noteq> B\<close> show "A \<inter> B = {}"
136       by (auto dest: disjointD)
137   next
138     assume "i \<noteq> j"
139     with * \<open>i\<in>I\<close> \<open>j\<in>I\<close> have "(\<Union>F i) \<inter> (\<Union>F j) = {}"
140       by (rule disjoint_family_onD)
141     with \<open>A\<in>F i\<close> \<open>i\<in>I\<close> \<open>B\<in>F j\<close> \<open>j\<in>I\<close>
142     show "A \<inter> B = {}"
143       by auto
144   qed
145 qed
147 lemma distinct_list_bind:
148   assumes "distinct xs" "\<And>x. x \<in> set xs \<Longrightarrow> distinct (f x)"
149           "disjoint_family_on (set \<circ> f) (set xs)"
150   shows   "distinct (List.bind xs f)"
151   using assms
152   by (induction xs)
153      (auto simp: disjoint_family_on_def distinct_map inj_on_def set_list_bind)
155 lemma bij_betw_UNION_disjoint:
156   assumes disj: "disjoint_family_on A' I"
157   assumes bij: "\<And>i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
158   shows   "bij_betw f (\<Union>i\<in>I. A i) (\<Union>i\<in>I. A' i)"
159 unfolding bij_betw_def
160 proof
161   from bij show eq: "f ` UNION I A = UNION I A'"
162     by (auto simp: bij_betw_def image_UN)
163   show "inj_on f (UNION I A)"
164   proof (rule inj_onI, clarify)
165     fix i j x y assume A: "i \<in> I" "j \<in> I" "x \<in> A i" "y \<in> A j" and B: "f x = f y"
166     from A bij[of i] bij[of j] have "f x \<in> A' i" "f y \<in> A' j"
167       by (auto simp: bij_betw_def)
168     with B have "A' i \<inter> A' j \<noteq> {}" by auto
169     with disj A have "i = j" unfolding disjoint_family_on_def by blast
170     with A B bij[of i] show "x = y" by (auto simp: bij_betw_def dest: inj_onD)
171   qed
172 qed
174 lemma disjoint_union: "disjoint C \<Longrightarrow> disjoint B \<Longrightarrow> \<Union>C \<inter> \<Union>B = {} \<Longrightarrow> disjoint (C \<union> B)"
175   using disjoint_UN[of "{C, B}" "\<lambda>x. x"] by (auto simp add: disjoint_family_on_def)
177 text \<open>
178   The union of an infinite disjoint family of non-empty sets is infinite.
179 \<close>
180 lemma infinite_disjoint_family_imp_infinite_UNION:
181   assumes "\<not>finite A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}" "disjoint_family_on f A"
182   shows   "\<not>finite (UNION A f)"
183 proof -
184   define g where "g x = (SOME y. y \<in> f x)" for x
185   have g: "g x \<in> f x" if "x \<in> A" for x
186     unfolding g_def by (rule someI_ex, insert assms(2) that) blast
187   have inj_on_g: "inj_on g A"
188   proof (rule inj_onI, rule ccontr)
189     fix x y assume A: "x \<in> A" "y \<in> A" "g x = g y" "x \<noteq> y"
190     with g[of x] g[of y] have "g x \<in> f x" "g x \<in> f y" by auto
191     with A \<open>x \<noteq> y\<close> assms show False
192       by (auto simp: disjoint_family_on_def inj_on_def)
193   qed
194   from g have "g ` A \<subseteq> UNION A f" by blast
195   moreover from inj_on_g \<open>\<not>finite A\<close> have "\<not>finite (g ` A)"
196     using finite_imageD by blast
197   ultimately show ?thesis using finite_subset by blast
198 qed
201 subsection \<open>Construct Disjoint Sequences\<close>
203 definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set" where
204   "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
206 lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
207 proof (induct n)
208   case 0 show ?case by simp
209 next
210   case (Suc n)
211   thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
212 qed
214 lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
215   by (rule UN_finite2_eq [where k=0])
218 lemma less_disjoint_disjointed: "m < n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
219   by (auto simp add: disjointed_def)
221 lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
223      (metis neq_iff Int_commute less_disjoint_disjointed)
225 lemma disjointed_subset: "disjointed A n \<subseteq> A n"
226   by (auto simp add: disjointed_def)
228 lemma disjointed_0[simp]: "disjointed A 0 = A 0"
231 lemma disjointed_mono: "mono A \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n"
232   using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
234 subsection \<open>Partitions\<close>
236 text \<open>
237   Partitions @{term P} of a set @{term A}. We explicitly disallow empty sets.
238 \<close>
240 definition partition_on :: "'a set \<Rightarrow> 'a set set \<Rightarrow> bool"
241 where
242   "partition_on A P \<longleftrightarrow> \<Union>P = A \<and> disjoint P \<and> {} \<notin> P"
244 lemma partition_onI:
245   "\<Union>P = A \<Longrightarrow> (\<And>p q. p \<in> P \<Longrightarrow> q \<in> P \<Longrightarrow> p \<noteq> q \<Longrightarrow> disjnt p q) \<Longrightarrow> {} \<notin> P \<Longrightarrow> partition_on A P"
246   by (auto simp: partition_on_def pairwise_def)
248 lemma partition_onD1: "partition_on A P \<Longrightarrow> A = \<Union>P"
249   by (auto simp: partition_on_def)
251 lemma partition_onD2: "partition_on A P \<Longrightarrow> disjoint P"
252   by (auto simp: partition_on_def)
254 lemma partition_onD3: "partition_on A P \<Longrightarrow> {} \<notin> P"
255   by (auto simp: partition_on_def)
257 subsection \<open>Constructions of partitions\<close>
259 lemma partition_on_empty: "partition_on {} P \<longleftrightarrow> P = {}"
260   unfolding partition_on_def by fastforce
262 lemma partition_on_space: "A \<noteq> {} \<Longrightarrow> partition_on A {A}"
263   by (auto simp: partition_on_def disjoint_def)
265 lemma partition_on_singletons: "partition_on A ((\<lambda>x. {x}) ` A)"
266   by (auto simp: partition_on_def disjoint_def)
268 lemma partition_on_transform:
269   assumes P: "partition_on A P"
270   assumes F_UN: "\<Union>(F ` P) = F (\<Union>P)" and F_disjnt: "\<And>p q. p \<in> P \<Longrightarrow> q \<in> P \<Longrightarrow> disjnt p q \<Longrightarrow> disjnt (F p) (F q)"
271   shows "partition_on (F A) (F ` P - {{}})"
272 proof -
273   have "\<Union>(F ` P - {{}}) = F A"
274     unfolding P[THEN partition_onD1] F_UN[symmetric] by auto
275   with P show ?thesis
276     by (auto simp add: partition_on_def pairwise_def intro!: F_disjnt)
277 qed
279 lemma partition_on_restrict: "partition_on A P \<Longrightarrow> partition_on (B \<inter> A) ((\<inter>) B ` P - {{}})"
280   by (intro partition_on_transform) (auto simp: disjnt_def)
282 lemma partition_on_vimage: "partition_on A P \<Longrightarrow> partition_on (f -` A) ((-`) f ` P - {{}})"
283   by (intro partition_on_transform) (auto simp: disjnt_def)
285 lemma partition_on_inj_image:
286   assumes P: "partition_on A P" and f: "inj_on f A"
287   shows "partition_on (f ` A) ((`) f ` P - {{}})"
288 proof (rule partition_on_transform[OF P])
289   show "p \<in> P \<Longrightarrow> q \<in> P \<Longrightarrow> disjnt p q \<Longrightarrow> disjnt (f ` p) (f ` q)" for p q
290     using f[THEN inj_onD] P[THEN partition_onD1] by (auto simp: disjnt_def)
291 qed auto
293 subsection \<open>Finiteness of partitions\<close>
295 lemma finitely_many_partition_on:
296   assumes "finite A"
297   shows "finite {P. partition_on A P}"
298 proof (rule finite_subset)
299   show "{P. partition_on A P} \<subseteq> Pow (Pow A)"
300     unfolding partition_on_def by auto
301   show "finite (Pow (Pow A))"
302     using assms by simp
303 qed
305 lemma finite_elements: "finite A \<Longrightarrow> partition_on A P \<Longrightarrow> finite P"
306   using partition_onD1[of A P] by (simp add: finite_UnionD)
308 subsection \<open>Equivalence of partitions and equivalence classes\<close>
310 lemma partition_on_quotient:
311   assumes r: "equiv A r"
312   shows "partition_on A (A // r)"
313 proof (rule partition_onI)
314   from r have "refl_on A r"
315     by (auto elim: equivE)
316   then show "\<Union>(A // r) = A" "{} \<notin> A // r"
317     by (auto simp: refl_on_def quotient_def)
319   fix p q assume "p \<in> A // r" "q \<in> A // r" "p \<noteq> q"
320   then obtain x y where "x \<in> A" "y \<in> A" "p = r `` {x}" "q = r `` {y}"
321     by (auto simp: quotient_def)
322   with r equiv_class_eq_iff[OF r, of x y] \<open>p \<noteq> q\<close> show "disjnt p q"
323     by (auto simp: disjnt_equiv_class)
324 qed
326 lemma equiv_partition_on:
327   assumes P: "partition_on A P"
328   shows "equiv A {(x, y). \<exists>p \<in> P. x \<in> p \<and> y \<in> p}"
329 proof (rule equivI)
330   have "A = \<Union>P" "disjoint P" "{} \<notin> P"
331     using P by (auto simp: partition_on_def)
332   then show "refl_on A {(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p}"
333     unfolding refl_on_def by auto
334   show "trans {(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p}"
335     using \<open>disjoint P\<close> by (auto simp: trans_def disjoint_def)
336 qed (auto simp: sym_def)
338 lemma partition_on_eq_quotient:
339   assumes P: "partition_on A P"
340   shows "A // {(x, y). \<exists>p \<in> P. x \<in> p \<and> y \<in> p} = P"
341   unfolding quotient_def
342 proof safe
343   fix x assume "x \<in> A"
344   then obtain p where "p \<in> P" "x \<in> p" "\<And>q. q \<in> P \<Longrightarrow> x \<in> q \<Longrightarrow> p = q"
345     using P by (auto simp: partition_on_def disjoint_def)
346   then have "{y. \<exists>p\<in>P. x \<in> p \<and> y \<in> p} = p"
347     by (safe intro!: bexI[of _ p]) simp
348   then show "{(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p} `` {x} \<in> P"
349     by (simp add: \<open>p \<in> P\<close>)
350 next
351   fix p assume "p \<in> P"
352   then have "p \<noteq> {}"
353     using P by (auto simp: partition_on_def)
354   then obtain x where "x \<in> p"
355     by auto
356   then have "x \<in> A" "\<And>q. q \<in> P \<Longrightarrow> x \<in> q \<Longrightarrow> p = q"
357     using P \<open>p \<in> P\<close> by (auto simp: partition_on_def disjoint_def)
358   with \<open>p\<in>P\<close> \<open>x \<in> p\<close> have "{y. \<exists>p\<in>P. x \<in> p \<and> y \<in> p} = p"
359     by (safe intro!: bexI[of _ p]) simp
360   then show "p \<in> (\<Union>x\<in>A. {{(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p} `` {x}})"
361     by (auto intro: \<open>x \<in> A\<close>)
362 qed
364 lemma partition_on_alt: "partition_on A P \<longleftrightarrow> (\<exists>r. equiv A r \<and> P = A // r)"
365   by (auto simp: partition_on_eq_quotient intro!: partition_on_quotient intro: equiv_partition_on)
367 end