author eberlm Tue May 17 19:27:42 2016 +0200 (2016-05-17 ago) changeset 63100 aa5cffd8a606 parent 63098 af0e964aad7b parent 63099 56f03591898b child 63101 65f1d7829463
Merged
```     1.1 --- a/src/HOL/Library/Disjoint_Sets.thy	Tue May 17 17:05:35 2016 +0200
1.2 +++ b/src/HOL/Library/Disjoint_Sets.thy	Tue May 17 19:27:42 2016 +0200
1.3 @@ -2,7 +2,7 @@
1.4      Author:     Johannes Hölzl, TU München
1.5  *)
1.6
1.7 -section \<open>Handling Disjoint Sets\<close>
1.8 +section \<open>Partitions and Disjoint Sets\<close>
1.9
1.10  theory Disjoint_Sets
1.11    imports Main
1.12 @@ -20,6 +20,9 @@
1.13  lemma mono_Un: "mono A \<Longrightarrow> (\<Union>i\<le>n. A i) = A n"
1.14    unfolding mono_def by auto
1.15
1.16 +lemma disjnt_equiv_class: "equiv A r \<Longrightarrow> disjnt (r``{a}) (r``{b}) \<longleftrightarrow> (a, b) \<notin> r"
1.17 +  by (auto dest: equiv_class_self simp: equiv_class_eq_iff disjnt_def)
1.18 +
1.19  subsection \<open>Set of Disjoint Sets\<close>
1.20
1.21  abbreviation disjoint :: "'a set set \<Rightarrow> bool" where "disjoint \<equiv> pairwise disjnt"
1.22 @@ -46,7 +49,7 @@
1.23    assumes *: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)"
1.24    shows "disjoint {\<Inter>i\<in>I. X i | X. \<forall>i\<in>I. X i \<in> F i}"
1.25  proof (safe intro!: disjointI del: equalityI)
1.26 -  fix A B :: "'a \<Rightarrow> 'b set" assume "(\<Inter>i\<in>I. A i) \<noteq> (\<Inter>i\<in>I. B i)"
1.27 +  fix A B :: "'a \<Rightarrow> 'b set" assume "(\<Inter>i\<in>I. A i) \<noteq> (\<Inter>i\<in>I. B i)"
1.28    then obtain i where "A i \<noteq> B i" "i \<in> I"
1.29      by auto
1.30    moreover assume "\<forall>i\<in>I. A i \<in> F i" "\<forall>i\<in>I. B i \<in> F i"
1.31 @@ -207,5 +210,138 @@
1.32
1.33  lemma disjointed_mono: "mono A \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n"
1.34    using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
1.35 -
1.36 +
1.37 +subsection \<open>Partitions\<close>
1.38 +
1.39 +text \<open>
1.40 +  Partitions @{term P} of a set @{term A}. We explicitly disallow empty sets.
1.41 +\<close>
1.42 +
1.43 +definition partition_on :: "'a set \<Rightarrow> 'a set set \<Rightarrow> bool"
1.44 +where
1.45 +  "partition_on A P \<longleftrightarrow> \<Union>P = A \<and> disjoint P \<and> {} \<notin> P"
1.46 +
1.47 +lemma partition_onI:
1.48 +  "\<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"
1.49 +  by (auto simp: partition_on_def pairwise_def)
1.50 +
1.51 +lemma partition_onD1: "partition_on A P \<Longrightarrow> A = \<Union>P"
1.52 +  by (auto simp: partition_on_def)
1.53 +
1.54 +lemma partition_onD2: "partition_on A P \<Longrightarrow> disjoint P"
1.55 +  by (auto simp: partition_on_def)
1.56 +
1.57 +lemma partition_onD3: "partition_on A P \<Longrightarrow> {} \<notin> P"
1.58 +  by (auto simp: partition_on_def)
1.59 +
1.60 +subsection \<open>Constructions of partitions\<close>
1.61 +
1.62 +lemma partition_on_empty: "partition_on {} P \<longleftrightarrow> P = {}"
1.63 +  unfolding partition_on_def by fastforce
1.64 +
1.65 +lemma partition_on_space: "A \<noteq> {} \<Longrightarrow> partition_on A {A}"
1.66 +  by (auto simp: partition_on_def disjoint_def)
1.67 +
1.68 +lemma partition_on_singletons: "partition_on A ((\<lambda>x. {x}) ` A)"
1.69 +  by (auto simp: partition_on_def disjoint_def)
1.70 +
1.71 +lemma partition_on_transform:
1.72 +  assumes P: "partition_on A P"
1.73 +  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)"
1.74 +  shows "partition_on (F A) (F ` P - {{}})"
1.75 +proof -
1.76 +  have "\<Union>(F ` P - {{}}) = F A"
1.77 +    unfolding P[THEN partition_onD1] F_UN[symmetric] by auto
1.78 +  with P show ?thesis
1.79 +    by (auto simp add: partition_on_def pairwise_def intro!: F_disjnt)
1.80 +qed
1.81 +
1.82 +lemma partition_on_restrict: "partition_on A P \<Longrightarrow> partition_on (B \<inter> A) (op \<inter> B ` P - {{}})"
1.83 +  by (intro partition_on_transform) (auto simp: disjnt_def)
1.84 +
1.85 +lemma partition_on_vimage: "partition_on A P \<Longrightarrow> partition_on (f -` A) (op -` f ` P - {{}})"
1.86 +  by (intro partition_on_transform) (auto simp: disjnt_def)
1.87 +
1.88 +lemma partition_on_inj_image:
1.89 +  assumes P: "partition_on A P" and f: "inj_on f A"
1.90 +  shows "partition_on (f ` A) (op ` f ` P - {{}})"
1.91 +proof (rule partition_on_transform[OF P])
1.92 +  show "p \<in> P \<Longrightarrow> q \<in> P \<Longrightarrow> disjnt p q \<Longrightarrow> disjnt (f ` p) (f ` q)" for p q
1.93 +    using f[THEN inj_onD] P[THEN partition_onD1] by (auto simp: disjnt_def)
1.94 +qed auto
1.95 +
1.96 +subsection \<open>Finiteness of partitions\<close>
1.97 +
1.98 +lemma finitely_many_partition_on:
1.99 +  assumes "finite A"
1.100 +  shows "finite {P. partition_on A P}"
1.101 +proof (rule finite_subset)
1.102 +  show "{P. partition_on A P} \<subseteq> Pow (Pow A)"
1.103 +    unfolding partition_on_def by auto
1.104 +  show "finite (Pow (Pow A))"
1.105 +    using assms by simp
1.106 +qed
1.107 +
1.108 +lemma finite_elements: "finite A \<Longrightarrow> partition_on A P \<Longrightarrow> finite P"
1.109 +  using partition_onD1[of A P] by (simp add: finite_UnionD)
1.110 +
1.111 +subsection \<open>Equivalence of partitions and equivalence classes\<close>
1.112 +
1.113 +lemma partition_on_quotient:
1.114 +  assumes r: "equiv A r"
1.115 +  shows "partition_on A (A // r)"
1.116 +proof (rule partition_onI)
1.117 +  from r have "refl_on A r"
1.118 +    by (auto elim: equivE)
1.119 +  then show "\<Union>(A // r) = A" "{} \<notin> A // r"
1.120 +    by (auto simp: refl_on_def quotient_def)
1.121 +
1.122 +  fix p q assume "p \<in> A // r" "q \<in> A // r" "p \<noteq> q"
1.123 +  then obtain x y where "x \<in> A" "y \<in> A" "p = r `` {x}" "q = r `` {y}"
1.124 +    by (auto simp: quotient_def)
1.125 +  with r equiv_class_eq_iff[OF r, of x y] \<open>p \<noteq> q\<close> show "disjnt p q"
1.126 +    by (auto simp: disjnt_equiv_class)
1.127 +qed
1.128 +
1.129 +lemma equiv_partition_on:
1.130 +  assumes P: "partition_on A P"
1.131 +  shows "equiv A {(x, y). \<exists>p \<in> P. x \<in> p \<and> y \<in> p}"
1.132 +proof (rule equivI)
1.133 +  have "A = \<Union>P" "disjoint P" "{} \<notin> P"
1.134 +    using P by (auto simp: partition_on_def)
1.135 +  then show "refl_on A {(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p}"
1.136 +    unfolding refl_on_def by auto
1.137 +  show "trans {(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p}"
1.138 +    using \<open>disjoint P\<close> by (auto simp: trans_def disjoint_def)
1.139 +qed (auto simp: sym_def)
1.140 +
1.141 +lemma partition_on_eq_quotient:
1.142 +  assumes P: "partition_on A P"
1.143 +  shows "A // {(x, y). \<exists>p \<in> P. x \<in> p \<and> y \<in> p} = P"
1.144 +  unfolding quotient_def
1.145 +proof safe
1.146 +  fix x assume "x \<in> A"
1.147 +  then obtain p where "p \<in> P" "x \<in> p" "\<And>q. q \<in> P \<Longrightarrow> x \<in> q \<Longrightarrow> p = q"
1.148 +    using P by (auto simp: partition_on_def disjoint_def)
1.149 +  then have "{y. \<exists>p\<in>P. x \<in> p \<and> y \<in> p} = p"
1.150 +    by (safe intro!: bexI[of _ p]) simp
1.151 +  then show "{(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p} `` {x} \<in> P"
1.152 +    by (simp add: \<open>p \<in> P\<close>)
1.153 +next
1.154 +  fix p assume "p \<in> P"
1.155 +  then have "p \<noteq> {}"
1.156 +    using P by (auto simp: partition_on_def)
1.157 +  then obtain x where "x \<in> p"
1.158 +    by auto
1.159 +  then have "x \<in> A" "\<And>q. q \<in> P \<Longrightarrow> x \<in> q \<Longrightarrow> p = q"
1.160 +    using P \<open>p \<in> P\<close> by (auto simp: partition_on_def disjoint_def)
1.161 +  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"
1.162 +    by (safe intro!: bexI[of _ p]) simp
1.163 +  then show "p \<in> (\<Union>x\<in>A. {{(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p} `` {x}})"
1.164 +    by (auto intro: \<open>x \<in> A\<close>)
1.165 +qed
1.166 +
1.167 +lemma partition_on_alt: "partition_on A P \<longleftrightarrow> (\<exists>r. equiv A r \<and> P = A // r)"
1.168 +  by (auto simp: partition_on_eq_quotient intro!: partition_on_quotient intro: equiv_partition_on)
1.169 +
1.170  end
```