--- 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>
--- 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
--- 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