Library: add partition_on
authorhoelzl
Tue May 17 11:16:39 2016 +0200 (2016-05-17 ago)
changeset 6309956f03591898b
parent 63097 ee8edbcbb4ad
child 63100 aa5cffd8a606
Library: add partition_on
src/HOL/Library/Disjoint_Sets.thy
     1.1 --- a/src/HOL/Library/Disjoint_Sets.thy	Tue May 17 08:40:24 2016 +0200
     1.2 +++ b/src/HOL/Library/Disjoint_Sets.thy	Tue May 17 11:16:39 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 @@ -39,7 +42,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 @@ -150,4 +153,137 @@
    1.32  lemma disjointed_mono: "mono A \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n"
    1.33    using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
    1.34  
    1.35 +subsection \<open>Partitions\<close>
    1.36 +
    1.37 +text \<open>
    1.38 +  Partitions @{term P} of a set @{term A}. We explicitly disallow empty sets.
    1.39 +\<close>
    1.40 +
    1.41 +definition partition_on :: "'a set \<Rightarrow> 'a set set \<Rightarrow> bool"
    1.42 +where
    1.43 +  "partition_on A P \<longleftrightarrow> \<Union>P = A \<and> disjoint P \<and> {} \<notin> P"
    1.44 +
    1.45 +lemma partition_onI:
    1.46 +  "\<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.47 +  by (auto simp: partition_on_def pairwise_def)
    1.48 +
    1.49 +lemma partition_onD1: "partition_on A P \<Longrightarrow> A = \<Union>P"
    1.50 +  by (auto simp: partition_on_def)
    1.51 +
    1.52 +lemma partition_onD2: "partition_on A P \<Longrightarrow> disjoint P"
    1.53 +  by (auto simp: partition_on_def)
    1.54 +
    1.55 +lemma partition_onD3: "partition_on A P \<Longrightarrow> {} \<notin> P"
    1.56 +  by (auto simp: partition_on_def)
    1.57 +
    1.58 +subsection \<open>Constructions of partitions\<close>
    1.59 +
    1.60 +lemma partition_on_empty: "partition_on {} P \<longleftrightarrow> P = {}"
    1.61 +  unfolding partition_on_def by fastforce
    1.62 +
    1.63 +lemma partition_on_space: "A \<noteq> {} \<Longrightarrow> partition_on A {A}"
    1.64 +  by (auto simp: partition_on_def disjoint_def)
    1.65 +
    1.66 +lemma partition_on_singletons: "partition_on A ((\<lambda>x. {x}) ` A)"
    1.67 +  by (auto simp: partition_on_def disjoint_def)
    1.68 +
    1.69 +lemma partition_on_transform:
    1.70 +  assumes P: "partition_on A P"
    1.71 +  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.72 +  shows "partition_on (F A) (F ` P - {{}})"
    1.73 +proof -
    1.74 +  have "\<Union>(F ` P - {{}}) = F A"
    1.75 +    unfolding P[THEN partition_onD1] F_UN[symmetric] by auto
    1.76 +  with P show ?thesis
    1.77 +    by (auto simp add: partition_on_def pairwise_def intro!: F_disjnt)
    1.78 +qed
    1.79 +
    1.80 +lemma partition_on_restrict: "partition_on A P \<Longrightarrow> partition_on (B \<inter> A) (op \<inter> B ` P - {{}})"
    1.81 +  by (intro partition_on_transform) (auto simp: disjnt_def)
    1.82 +
    1.83 +lemma partition_on_vimage: "partition_on A P \<Longrightarrow> partition_on (f -` A) (op -` f ` P - {{}})"
    1.84 +  by (intro partition_on_transform) (auto simp: disjnt_def)
    1.85 +
    1.86 +lemma partition_on_inj_image:
    1.87 +  assumes P: "partition_on A P" and f: "inj_on f A"
    1.88 +  shows "partition_on (f ` A) (op ` f ` P - {{}})"
    1.89 +proof (rule partition_on_transform[OF P])
    1.90 +  show "p \<in> P \<Longrightarrow> q \<in> P \<Longrightarrow> disjnt p q \<Longrightarrow> disjnt (f ` p) (f ` q)" for p q
    1.91 +    using f[THEN inj_onD] P[THEN partition_onD1] by (auto simp: disjnt_def)
    1.92 +qed auto
    1.93 +
    1.94 +subsection \<open>Finiteness of partitions\<close>
    1.95 +
    1.96 +lemma finitely_many_partition_on:
    1.97 +  assumes "finite A"
    1.98 +  shows "finite {P. partition_on A P}"
    1.99 +proof (rule finite_subset)
   1.100 +  show "{P. partition_on A P} \<subseteq> Pow (Pow A)"
   1.101 +    unfolding partition_on_def by auto
   1.102 +  show "finite (Pow (Pow A))"
   1.103 +    using assms by simp
   1.104 +qed
   1.105 +
   1.106 +lemma finite_elements: "finite A \<Longrightarrow> partition_on A P \<Longrightarrow> finite P"
   1.107 +  using partition_onD1[of A P] by (simp add: finite_UnionD)
   1.108 +
   1.109 +subsection \<open>Equivalence of partitions and equivalence classes\<close>
   1.110 +
   1.111 +lemma partition_on_quotient:
   1.112 +  assumes r: "equiv A r"
   1.113 +  shows "partition_on A (A // r)"
   1.114 +proof (rule partition_onI)
   1.115 +  from r have "refl_on A r"
   1.116 +    by (auto elim: equivE)
   1.117 +  then show "\<Union>(A // r) = A" "{} \<notin> A // r"
   1.118 +    by (auto simp: refl_on_def quotient_def)
   1.119 +
   1.120 +  fix p q assume "p \<in> A // r" "q \<in> A // r" "p \<noteq> q"
   1.121 +  then obtain x y where "x \<in> A" "y \<in> A" "p = r `` {x}" "q = r `` {y}"
   1.122 +    by (auto simp: quotient_def)
   1.123 +  with r equiv_class_eq_iff[OF r, of x y] \<open>p \<noteq> q\<close> show "disjnt p q"
   1.124 +    by (auto simp: disjnt_equiv_class)
   1.125 +qed
   1.126 +
   1.127 +lemma equiv_partition_on:
   1.128 +  assumes P: "partition_on A P"
   1.129 +  shows "equiv A {(x, y). \<exists>p \<in> P. x \<in> p \<and> y \<in> p}"
   1.130 +proof (rule equivI)
   1.131 +  have "A = \<Union>P" "disjoint P" "{} \<notin> P"
   1.132 +    using P by (auto simp: partition_on_def)
   1.133 +  then show "refl_on A {(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p}"
   1.134 +    unfolding refl_on_def by auto
   1.135 +  show "trans {(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p}"
   1.136 +    using \<open>disjoint P\<close> by (auto simp: trans_def disjoint_def)
   1.137 +qed (auto simp: sym_def)
   1.138 +
   1.139 +lemma partition_on_eq_quotient:
   1.140 +  assumes P: "partition_on A P"
   1.141 +  shows "A // {(x, y). \<exists>p \<in> P. x \<in> p \<and> y \<in> p} = P"
   1.142 +  unfolding quotient_def
   1.143 +proof safe
   1.144 +  fix x assume "x \<in> A"
   1.145 +  then obtain p where "p \<in> P" "x \<in> p" "\<And>q. q \<in> P \<Longrightarrow> x \<in> q \<Longrightarrow> p = q"
   1.146 +    using P by (auto simp: partition_on_def disjoint_def)
   1.147 +  then have "{y. \<exists>p\<in>P. x \<in> p \<and> y \<in> p} = p"
   1.148 +    by (safe intro!: bexI[of _ p]) simp
   1.149 +  then show "{(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p} `` {x} \<in> P"
   1.150 +    by (simp add: \<open>p \<in> P\<close>)
   1.151 +next
   1.152 +  fix p assume "p \<in> P"
   1.153 +  then have "p \<noteq> {}"
   1.154 +    using P by (auto simp: partition_on_def)
   1.155 +  then obtain x where "x \<in> p"
   1.156 +    by auto
   1.157 +  then have "x \<in> A" "\<And>q. q \<in> P \<Longrightarrow> x \<in> q \<Longrightarrow> p = q"
   1.158 +    using P \<open>p \<in> P\<close> by (auto simp: partition_on_def disjoint_def)
   1.159 +  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.160 +    by (safe intro!: bexI[of _ p]) simp
   1.161 +  then show "p \<in> (\<Union>x\<in>A. {{(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p} `` {x}})"
   1.162 +    by (auto intro: \<open>x \<in> A\<close>)
   1.163 +qed
   1.164 +
   1.165 +lemma partition_on_alt: "partition_on A P \<longleftrightarrow> (\<exists>r. equiv A r \<and> P = A // r)"
   1.166 +  by (auto simp: partition_on_eq_quotient intro!: partition_on_quotient intro: equiv_partition_on)
   1.167 +
   1.168  end