
diff -r 42fb56041c11 -r 00ffae972fc0 src/HOL/Library/Disjoint_Sets.thy
--- a/src/HOL/Library/Disjoint_Sets.thy	Mon Oct 25 23:10:06 2021 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy	Tue Oct 26 11:15:40 2021 +0100
@@ -4,24 +4,12 @@
 section \<open>Partitions and Disjoint Sets\<close>
 
 theory Disjoint_Sets
-  imports Main
+  imports FuncSet
 begin
 
-lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
-  by blast
-
-lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
-  by blast
-
-lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
-  by blast
-
-lemma mono_Un: "mono A \<Longrightarrow> (\<Union>i\<le>n. A i) = A n"
+lemma mono_imp_UN_eq_last: "mono A \<Longrightarrow> (\<Union>i\<le>n. A i) = A n"
   unfolding mono_def by auto
 
-lemma disjnt_equiv_class: "equiv A r \<Longrightarrow> disjnt (r``{a}) (r``{b}) \<longleftrightarrow> (a, b) \<notin> r"
-  by (auto dest: equiv_class_self simp: equiv_class_eq_iff disjnt_def)
-
 subsection \<open>Set of Disjoint Sets\<close>
 
 abbreviation disjoint :: "'a set set \<Rightarrow> bool" where "disjoint \<equiv> pairwise disjnt"
@@ -304,7 +292,7 @@
   by (simp add: disjointed_def)
 
 lemma disjointed_mono: "mono A \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n"
-  using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
+  using mono_imp_UN_eq_last[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
 
 subsection \<open>Partitions\<close>
 
@@ -496,4 +484,115 @@
     using assms by (auto simp: refines_def disjoint_def partition_on_def)
 qed 
 
+subsection \<open>The coarsest common refinement of a set of partitions\<close>
+
+definition common_refinement :: "'a set set set \<Rightarrow> 'a set set"
+  where "common_refinement \<P> \<equiv> (\<Union>f \<in> (\<Pi>\<^sub>E P\<in>\<P>. P). {\<Inter> (f ` \<P>)}) - {{}}" 
+
+text \<open>With non-extensional function space\<close>
+lemma common_refinement: "common_refinement \<P> = (\<Union>f \<in> (\<Pi> P\<in>\<P>. P). {\<Inter> (f ` \<P>)}) - {{}}" 
+  (is "?lhs = ?rhs")
+proof
+  show "?rhs \<subseteq> ?lhs"
+    apply (clarsimp simp add: common_refinement_def PiE_def Ball_def)
+    by (metis restrict_Pi_cancel image_restrict_eq restrict_extensional)
+qed (auto simp add: common_refinement_def PiE_def)
+
+lemma common_refinement_exists: "\<lbrakk>X \<in> common_refinement \<P>; P \<in> \<P>\<rbrakk> \<Longrightarrow> \<exists>R\<in>P. X \<subseteq> R"
+  by (auto simp add: common_refinement)
+
+lemma Union_common_refinement: "\<Union> (common_refinement \<P>) = (\<Inter> P\<in>\<P>. \<Union>P)"
+proof
+  show "(\<Inter> P\<in>\<P>. \<Union>P) \<subseteq> \<Union> (common_refinement \<P>)"
+  proof (clarsimp simp: common_refinement)
+    fix x
+    assume "\<forall>P\<in>\<P>. \<exists>X\<in>P. x \<in> X"
+    then obtain F where F: "\<And>P. P\<in>\<P> \<Longrightarrow> F P \<in> P \<and> x \<in> F P"
+      by metis
+    then have "x \<in> \<Inter> (F ` \<P>)"
+      by force
+    with F show "\<exists>X\<in>(\<Union>x\<in>\<Pi> P\<in>\<P>. P. {\<Inter> (x ` \<P>)}) - {{}}. x \<in> X"
+      by (auto simp add: Pi_iff Bex_def)
+  qed
+qed (auto simp: common_refinement_def)
+
+lemma partition_on_common_refinement:
+  assumes A: "\<And>P. P \<in> \<P> \<Longrightarrow> partition_on A P" and "\<P> \<noteq> {}"
+  shows "partition_on A (common_refinement \<P>)"
+proof (rule partition_onI)
+  show "\<Union> (common_refinement \<P>) = A"
+    using assms by (simp add: partition_on_def Union_common_refinement)
+  fix P Q
+  assume "P \<in> common_refinement \<P>" and "Q \<in> common_refinement \<P>" and "P \<noteq> Q"
+  then obtain f g where f: "f \<in> (\<Pi>\<^sub>E P\<in>\<P>. P)" and P: "P = \<Inter> (f ` \<P>)" and "P \<noteq> {}"
+                  and   g: "g \<in> (\<Pi>\<^sub>E P\<in>\<P>. P)" and Q: "Q = \<Inter> (g ` \<P>)" and "Q \<noteq> {}"
+    by (auto simp add: common_refinement_def)
+  have "f=g" if "x \<in> P" "x \<in> Q" for x
+  proof (rule extensionalityI [of _ \<P>])
+    fix R
+    assume "R \<in> \<P>"
+    with that P Q f g A [unfolded partition_on_def, OF \<open>R \<in> \<P>\<close>]
+    show "f R = g R"
+      by (metis INT_E Int_iff PiE_iff disjointD emptyE)
+  qed (use PiE_iff f g in auto)
+  then show "disjnt P Q"
+    by (metis P Q \<open>P \<noteq> Q\<close> disjnt_iff) 
+qed (simp add: common_refinement_def)
+
+lemma refines_common_refinement:
+  assumes "\<And>P. P \<in> \<P> \<Longrightarrow> partition_on A P" "P \<in> \<P>"
+  shows "refines A (common_refinement \<P>) P"
+  unfolding refines_def
+proof (intro conjI strip)
+  fix X
+  assume "X \<in> common_refinement \<P>"
+  with assms show "\<exists>Y\<in>P. X \<subseteq> Y"
+    by (auto simp: common_refinement_def)
+qed (use assms partition_on_common_refinement in auto)
+
+text \<open>The common refinement is itself refined by any other\<close>
+lemma common_refinement_coarsest:
+  assumes "\<And>P. P \<in> \<P> \<Longrightarrow> partition_on A P" "partition_on A R" "\<And>P. P \<in> \<P> \<Longrightarrow> refines A R P" "\<P> \<noteq> {}"
+  shows "refines A R (common_refinement \<P>)"
+  unfolding refines_def
+proof (intro conjI ballI partition_on_common_refinement)
+  fix X
+  assume "X \<in> R"
+  have "\<exists>p \<in> P. X \<subseteq> p" if "P \<in> \<P>" for P
+    by (meson \<open>X \<in> R\<close> assms(3) refines_def that)
+  then obtain F where f: "\<And>P. P \<in> \<P> \<Longrightarrow> F P \<in> P \<and> X \<subseteq> F P"
+    by metis
+  with \<open>partition_on A R\<close> \<open>X \<in> R\<close> \<open>\<P> \<noteq> {}\<close>
+  have "\<Inter> (F ` \<P>) \<in> common_refinement \<P>"
+    apply (simp add: partition_on_def common_refinement Pi_iff Bex_def)
+    by (metis (no_types, lifting) cINF_greatest subset_empty)
+  with f show "\<exists>Y\<in>common_refinement \<P>. X \<subseteq> Y"
+    by (metis \<open>\<P> \<noteq> {}\<close> cINF_greatest)
+qed (use assms in auto)
+
+lemma finite_common_refinement:
+  assumes "finite \<P>" "\<And>P. P \<in> \<P> \<Longrightarrow> finite P"
+  shows "finite (common_refinement \<P>)"
+proof -
+  have "finite (\<Pi>\<^sub>E P\<in>\<P>. P)"
+    by (simp add: assms finite_PiE)
+  then show ?thesis
+    by (auto simp: common_refinement_def)
+qed
+
+lemma card_common_refinement:
+  assumes "finite \<P>" "\<And>P. P \<in> \<P> \<Longrightarrow> finite P"
+  shows "card (common_refinement \<P>) \<le> (\<Prod>P \<in> \<P>. card P)"
+proof -
+  have "card (common_refinement \<P>) \<le> card (\<Union>f \<in> (\<Pi>\<^sub>E P\<in>\<P>. P). {\<Inter> (f ` \<P>)})"
+    unfolding common_refinement_def by (meson card_Diff1_le)
+  also have "\<dots> \<le> (\<Sum>f\<in>(\<Pi>\<^sub>E P\<in>\<P>. P). card{\<Inter> (f ` \<P>)})"
+    by (metis assms finite_PiE card_UN_le)
+  also have "\<dots> = card(\<Pi>\<^sub>E P\<in>\<P>. P)"
+    by simp
+  also have "\<dots> = (\<Prod>P \<in> \<P>. card P)"
+    by (simp add: assms(1) card_PiE dual_order.eq_iff)
+  finally show ?thesis .
+qed
+
 end




