src/HOL/Library/Disjoint_Sets.thy
author wenzelm
Wed Mar 08 10:50:59 2017 +0100 (2017-03-08)
changeset 65151 a7394aa4d21c
parent 63928 d81fb5b46a5c
child 67399 eab6ce8368fa
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/Library/Disjoint_Sets.thy
     2     Author:     Johannes Hölzl, TU München
     3 *)
     4 
     5 section \<open>Partitions and Disjoint Sets\<close>
     6 
     7 theory Disjoint_Sets
     8   imports Main
     9 begin
    10 
    11 lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
    12   by blast
    13 
    14 lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
    15   by blast
    16 
    17 lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
    18   by blast
    19 
    20 lemma mono_Un: "mono A \<Longrightarrow> (\<Union>i\<le>n. A i) = A n"
    21   unfolding mono_def by auto
    22 
    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)
    25 
    26 subsection \<open>Set of Disjoint Sets\<close>
    27 
    28 abbreviation disjoint :: "'a set set \<Rightarrow> bool" where "disjoint \<equiv> pairwise disjnt"
    29 
    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
    32 
    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
    36 
    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
    40 
    41 lemma disjoint_image: "inj_on f (\<Union>A) \<Longrightarrow> disjoint A \<Longrightarrow> disjoint (op ` f ` A)"
    42   unfolding inj_on_def disjoint_def by blast
    43 
    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)
    47   
    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
    60 
    61 subsubsection "Family of Disjoint Sets"
    62 
    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 = {})"
    65 
    66 abbreviation "disjoint_family A \<equiv> disjoint_family_on A UNIV"
    67 
    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
    87 
    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)
    91 
    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)
    94 
    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
   100 
   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
   104 
   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)
   110 
   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
   114  
   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)
   117 
   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
   127 
   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
   146 
   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)
   154 
   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
   173 
   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)
   176 
   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  
   199   
   200 
   201 subsection \<open>Construct Disjoint Sequences\<close>
   202 
   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)"
   205 
   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
   213 
   214 lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
   215   by (rule UN_finite2_eq [where k=0])
   216      (simp add: finite_UN_disjointed_eq)
   217 
   218 lemma less_disjoint_disjointed: "m < n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
   219   by (auto simp add: disjointed_def)
   220 
   221 lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
   222   by (simp add: disjoint_family_on_def)
   223      (metis neq_iff Int_commute less_disjoint_disjointed)
   224 
   225 lemma disjointed_subset: "disjointed A n \<subseteq> A n"
   226   by (auto simp add: disjointed_def)
   227 
   228 lemma disjointed_0[simp]: "disjointed A 0 = A 0"
   229   by (simp add: disjointed_def)
   230 
   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)
   233 
   234 subsection \<open>Partitions\<close>
   235 
   236 text \<open>
   237   Partitions @{term P} of a set @{term A}. We explicitly disallow empty sets.
   238 \<close>
   239 
   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"
   243 
   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)
   247 
   248 lemma partition_onD1: "partition_on A P \<Longrightarrow> A = \<Union>P"
   249   by (auto simp: partition_on_def)
   250 
   251 lemma partition_onD2: "partition_on A P \<Longrightarrow> disjoint P"
   252   by (auto simp: partition_on_def)
   253 
   254 lemma partition_onD3: "partition_on A P \<Longrightarrow> {} \<notin> P"
   255   by (auto simp: partition_on_def)
   256 
   257 subsection \<open>Constructions of partitions\<close>
   258 
   259 lemma partition_on_empty: "partition_on {} P \<longleftrightarrow> P = {}"
   260   unfolding partition_on_def by fastforce
   261 
   262 lemma partition_on_space: "A \<noteq> {} \<Longrightarrow> partition_on A {A}"
   263   by (auto simp: partition_on_def disjoint_def)
   264 
   265 lemma partition_on_singletons: "partition_on A ((\<lambda>x. {x}) ` A)"
   266   by (auto simp: partition_on_def disjoint_def)
   267 
   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
   278 
   279 lemma partition_on_restrict: "partition_on A P \<Longrightarrow> partition_on (B \<inter> A) (op \<inter> B ` P - {{}})"
   280   by (intro partition_on_transform) (auto simp: disjnt_def)
   281 
   282 lemma partition_on_vimage: "partition_on A P \<Longrightarrow> partition_on (f -` A) (op -` f ` P - {{}})"
   283   by (intro partition_on_transform) (auto simp: disjnt_def)
   284 
   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) (op ` 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
   292 
   293 subsection \<open>Finiteness of partitions\<close>
   294 
   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
   304 
   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)
   307 
   308 subsection \<open>Equivalence of partitions and equivalence classes\<close>
   309 
   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)
   318 
   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
   325 
   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)
   337 
   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
   363 
   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)
   366 
   367 end