# HG changeset patch
# User paulson
# Date 1635261723 -3600
# Node ID a0ab0dc28d3c19029fa8b7c89ed4a71df8dcc2a5
# Parent  ee92a47b47cbf214c319128bb14e472491712f7c# Parent  00ffae972fc0625bdd9939399254751b02367824
merged

diff -r ee92a47b47cb -r a0ab0dc28d3c src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Tue Oct 26 15:11:40 2021 +0200
+++ b/src/HOL/Equiv_Relations.thy	Tue Oct 26 16:22:03 2021 +0100
@@ -82,6 +82,9 @@
 lemma eq_equiv_class_iff: "equiv A r \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> r``{x} = r``{y} \<longleftrightarrow> (x, y) \<in> r"
   by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)
 
+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>Quotients\<close>
 
diff -r ee92a47b47cb -r a0ab0dc28d3c src/HOL/Library/Disjoint_Sets.thy
--- a/src/HOL/Library/Disjoint_Sets.thy	Tue Oct 26 15:11:40 2021 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy	Tue Oct 26 16:22:03 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
diff -r ee92a47b47cb -r a0ab0dc28d3c src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Oct 26 15:11:40 2021 +0200
+++ b/src/HOL/Set.thy	Tue Oct 26 16:22:03 2021 +0100
@@ -973,6 +973,9 @@
 lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) \<Longrightarrow> (\<And>x. b = f x \<Longrightarrow> P) \<Longrightarrow> P"
   by (rule imageE)
 
+lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
+  by blast
+
 lemma full_SetCompr_eq: "{u. \<exists>x. u = f x} = range f"
   by auto
 
@@ -1570,6 +1573,12 @@
 
 text \<open>\<^medskip> Miscellany.\<close>
 
+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 set_eq_subset: "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
   by blast