(* Author: Johannes Hölzl, TU München
*)
section ‹Partitions
and Disjoint Sets
›
theory Disjoint_Sets
imports FuncSet
begin
lemma mono_imp_UN_eq_last:
"mono A \ (\i\n. A i) = A n"
unfolding mono_def
by auto
subsection ‹Set of Disjoint Sets
›
abbreviation disjoint ::
"'a set set \ bool" where "disjoint \ pairwise disjnt"
lemma disjoint_def:
"disjoint A \ (\a\A. \b\A. a \ b \ a \ b = {})"
unfolding pairwise_def disjnt_def
by auto
lemma disjointI:
"(\a b. a \ A \ b \ A \ a \ b \ a \ b = {}) \ disjoint A"
unfolding disjoint_def
by auto
lemma disjointD:
"disjoint A \ a \ A \ b \ A \ a \ b \ a \ b = {}"
unfolding disjoint_def
by auto
lemma disjoint_image:
"inj_on f (\A) \ disjoint A \ disjoint ((`) f ` A)"
unfolding inj_on_def disjoint_def
by blast
lemma assumes "disjoint (A \ B)"
shows disjoint_unionD1:
"disjoint A" and disjoint_unionD2:
"disjoint B"
using assms
by (simp_all add: disjoint_def)
lemma disjoint_INT:
assumes *:
"\i. i \ I \ disjoint (F i)"
shows "disjoint {\i\I. X i | X. \i\I. X i \ F i}"
proof (safe intro!: disjointI del: equalityI)
fix A B ::
"'a \ 'b set" assume "(\i\I. A i) \ (\i\I. B i)"
then obtain i
where "A i \ B i" "i \ I"
by auto
moreover assume "\i\I. A i \ F i" "\i\I. B i \ F i"
ultimately show "(\i\I. A i) \ (\i\I. B i) = {}"
using *[OF
‹i
∈I
›,
THEN disjointD, of
"A i" "B i"]
by (auto simp flip: INT_Int_distrib)
qed
lemma diff_Union_pairwise_disjoint:
assumes "pairwise disjnt \" "\ \ \"
shows "\\ - \\ = \(\ - \)"
proof -
have "False"
if x:
"x \ A" "x \ B" and AB:
"A \ \" "A \ \" "B \ \" for x A B
proof -
have "A \ B = {}"
using assms disjointD AB
by blast
with x
show ?thesis
by blast
qed
then show ?thesis
by auto
qed
lemma Int_Union_pairwise_disjoint:
assumes "pairwise disjnt (\ \ \)"
shows "\\ \ \\ = \(\ \ \)"
proof -
have "False"
if x:
"x \ A" "x \ B" and AB:
"A \ \" "A \ \" "B \ \" for x A B
proof -
have "A \ B = {}"
using assms disjointD AB
by blast
with x
show ?thesis
by blast
qed
then show ?thesis
by auto
qed
lemma psubset_Union_pairwise_disjoint:
assumes B:
"pairwise disjnt \" and "\ \ \ - {{}}"
shows "\\ \ \\"
unfolding psubset_eq
proof
show "\\ \ \\"
using assms
by blast
have "\ \ \" "\(\ - \ \ (\ - {{}})) \ {}"
using assms
by blast+
then show "\\ \ \\"
using diff_Union_pairwise_disjoint [OF
B]
by blast
qed
subsubsection
"Family of Disjoint Sets"
definition disjoint_family_on ::
"('i \ 'a set) \ 'i set \ bool" where
"disjoint_family_on A S \ (\m\S. \n\S. m \ n \ A m \ A n = {})"
abbreviation "disjoint_family A \ disjoint_family_on A UNIV"
lemma disjoint_family_elem_disjnt:
assumes "infinite A" "finite C"
and df:
"disjoint_family_on B A"
obtains x
where "x \ A" "disjnt C (B x)"
proof -
have "False" if *:
"\x \ A. \y. y \ C \ y \ B x"
proof -
obtain g
where g:
"\x \ A. g x \ C \ g x \ B x"
using *
by metis
with df
have "inj_on g A"
by (fastforce simp add: inj_on_def disjoint_family_on_def)
then have "infinite (g ` A)"
using ‹infinite A
› finite_image_iff
by blast
then show False
by (meson
‹finite C
› finite_subset g image_subset_iff)
qed
then show ?thesis
by (force simp: disjnt_iff intro: that)
qed
lemma disjoint_family_onD:
"disjoint_family_on A I \ i \ I \ j \ I \ i \ j \ A i \ A j = {}"
by (auto simp: disjoint_family_on_def)
lemma disjoint_family_subset:
"disjoint_family A \ (\x. B x \ A x) \ disjoint_family B"
by (force simp add: disjoint_family_on_def)
lemma disjoint_family_on_insert:
"i \ I \ disjoint_family_on A (insert i I) \ A i \ (\i\I. A i) = {} \ disjoint_family_on A I"
by (fastforce simp: disjoint_family_on_def)
lemma disjoint_family_on_bisimulation:
assumes "disjoint_family_on f S"
and "\n m. n \ S \ m \ S \ n \ m \ f n \ f m = {} \ g n \ g m = {}"
shows "disjoint_family_on g S"
using assms
unfolding disjoint_family_on_def
by auto
lemma disjoint_family_on_mono:
"A \ B \ disjoint_family_on f B \ disjoint_family_on f A"
unfolding disjoint_family_on_def
by auto
lemma disjoint_family_Suc:
"(\n. A n \ A (Suc n)) \ disjoint_family (\i. A (Suc i) - A i)"
using lift_Suc_mono_le[of A]
by (auto simp add: disjoint_family_on_def)
(metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less less_imp_le)
lemma disjoint_family_on_disjoint_image:
"disjoint_family_on A I \ disjoint (A ` I)"
unfolding disjoint_family_on_def disjoint_def
by force
lemma disjoint_family_on_vimageI:
"disjoint_family_on F I \ disjoint_family_on (\i. f -` F i) I"
by (auto simp: disjoint_family_on_def)
lemma disjoint_image_disjoint_family_on:
assumes d:
"disjoint (A ` I)" and i:
"inj_on A I"
shows "disjoint_family_on A I"
unfolding disjoint_family_on_def
proof (intro ballI impI)
fix n m
assume nm:
"m \ I" "n \ I" and "n \ m"
with i[
THEN inj_onD, of n m]
show "A n \ A m = {}"
by (intro disjointD[OF d]) auto
qed
lemma disjoint_family_on_iff_disjoint_image:
assumes "\i. i \ I \ A i \ {}"
shows "disjoint_family_on A I \ disjoint (A ` I) \ inj_on A I"
proof
assume "disjoint_family_on A I"
then show "disjoint (A ` I) \ inj_on A I"
by (metis (mono_tags, lifting) assms disjoint_family_onD disjoint_family_on_disjoint_i
mage inf.idem inj_onI)
qed (use disjoint_image_disjoint_family_on in metis)
lemma card_UN_disjoint':
assumes "disjoint_family_on A I" "\i. i \ I \ finite (A i)" "finite I"
shows "card (\i\I. A i) = (\i\I. card (A i))"
using assms by (simp add: card_UN_disjoint disjoint_family_on_def)
lemma disjoint_UN:
assumes F: "\i. i \ I \ disjoint (F i)" and *: "disjoint_family_on (\i. \(F i)) I"
shows "disjoint (\i\I. F i)"
proof (safe intro!: disjointI del: equalityI)
fix A B i j assume "A \ B" "A \ F i" "i \ I" "B \ F j" "j \ I"
show "A \ B = {}"
proof cases
assume "i = j" with F[of i] ‹i ∈ I› ‹A ∈ F i› ‹B ∈ F j› ‹A ≠ B› show "A \ B = {}"
by (auto dest: disjointD)
next
assume "i \ j"
with * ‹i∈I› ‹j∈I› have "(\(F i)) \ (\(F j)) = {}"
by (rule disjoint_family_onD)
with ‹A∈F i› ‹i∈I› ‹B∈F j› ‹j∈I›
show "A \ B = {}"
by auto
qed
qed
lemma distinct_list_bind:
assumes "distinct xs" "\x. x \ set xs \ distinct (f x)"
"disjoint_family_on (set \ f) (set xs)"
shows "distinct (List.bind xs f)"
using assms
by (induction xs)
(auto simp: disjoint_family_on_def distinct_map inj_on_def set_list_bind)
lemma bij_betw_UNION_disjoint:
assumes disj: "disjoint_family_on A' I"
assumes bij: "\i. i \ I \ bij_betw f (A i) (A' i)"
shows "bij_betw f (\i\I. A i) (\i\I. A' i)"
unfolding bij_betw_def
proof
from bij show eq: "f ` \(A ` I) = \(A' ` I)"
by (auto simp: bij_betw_def image_UN)
show "inj_on f (\(A ` I))"
proof (rule inj_onI, clarify)
fix i j x y assume A: "i \ I" "j \ I" "x \ A i" "y \ A j" and B: "f x = f y"
from A bij[of i] bij[of j] have "f x \ A' i" "f y \ A' j"
by (auto simp: bij_betw_def)
with B have "A' i \ A' j \ {}" by auto
with disj A have "i = j" unfolding disjoint_family_on_def by blast
with A B bij[of i] show "x = y" by (auto simp: bij_betw_def dest: inj_onD)
qed
qed
lemma disjoint_union: "disjoint C \ disjoint B \ \C \ \B = {} \ disjoint (C \ B)"
using disjoint_UN[of "{C, B}" "\x. x"] by (auto simp add: disjoint_family_on_def)
text ‹
Sum/product of the union of a finite disjoint family
›
context comm_monoid_set
begin
lemma UNION_disjoint_family:
assumes "finite I" and "\i\I. finite (A i)"
and "disjoint_family_on A I"
shows "F g (\(A ` I)) = F (\x. F g (A x)) I"
using assms unfolding disjoint_family_on_def by (rule UNION_disjoint)
lemma Union_disjoint_sets:
assumes "\A\C. finite A" and "disjoint C"
shows "F g (\C) = (F \ F) g C"
using assms unfolding disjoint_def by (rule Union_disjoint)
end
text ‹
The union of an infinite disjoint family of non-empty sets is infinite.
›
lemma infinite_disjoint_family_imp_infinite_UNION:
assumes "\finite A" "\x. x \ A \ f x \ {}" "disjoint_family_on f A"
shows "\finite (\(f ` A))"
proof -
define g where "g x = (SOME y. y \ f x)" for x
have g: "g x \ f x" if "x \ A" for x
unfolding g_def by (rule someI_ex, insert assms(2) that) blast
have inj_on_g: "inj_on g A"
proof (rule inj_onI, rule ccontr)
fix x y assume A: "x \ A" "y \ A" "g x = g y" "x \ y"
with g[of x] g[of y] have "g x \ f x" "g x \ f y" by auto
with A ‹x ≠ y› assms show False
by (auto simp: disjoint_family_on_def inj_on_def)
qed
from g have "g ` A \ \(f ` A)" by blast
moreover from inj_on_g ‹¬finite A› have "\finite (g ` A)"
using finite_imageD by blast
ultimately show ?thesis using finite_subset by blast
qed
subsection ‹Construct Disjoint Sequences›
definition disjointed :: "(nat \ 'a set) \ nat \ 'a set" where
"disjointed A n = A n - (\i\{0..
lemma finite_UN_disjointed_eq: "(\i\{0..i\{0..
proof (induct n)
case 0 show ?case by simp
next
case (Suc n)
thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
qed
lemma UN_disjointed_eq: "(\i. disjointed A i) = (\i. A i)"
by (rule UN_finite2_eq [where k=0])
(simp add: finite_UN_disjointed_eq)
lemma less_disjoint_disjointed: "m < n \ disjointed A m \ disjointed A n = {}"
by (auto simp add: disjointed_def)
lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
by (simp add: disjoint_family_on_def)
(metis neq_iff Int_commute less_disjoint_disjointed)
lemma disjointed_subset: "disjointed A n \ A n"
by (auto simp add: disjointed_def)
lemma disjointed_0[simp]: "disjointed A 0 = A 0"
by (simp add: disjointed_def)
lemma disjointed_mono: "mono A \ disjointed A (Suc n) = A (Suc n) - A n"
using mono_imp_UN_eq_last[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
subsection ‹Partitions›
text ‹
Partitions 🍋‹P› of a set 🍋‹A›. We explicitly disallow empty sets.
›
definition partition_on :: "'a set \ 'a set set \ bool"
where
"partition_on A P \ \P = A \ disjoint P \ {} \ P"
lemma partition_onI:
"\P = A \ (\p q. p \ P \ q \ P \ p \ q \ disjnt p q) \ {} \ P \ partition_on A P"
by (auto simp: partition_on_def pairwise_def)
lemma partition_onD1: "partition_on A P \ A = \P"
by (auto simp: partition_on_def)
lemma partition_onD2: "partition_on A P \ disjoint P"
by (auto simp: partition_on_def)
lemma partition_onD3: "partition_on A P \ {} \ P"
by (auto simp: partition_on_def)
subsection ‹Constructions of partitions›
lemma partition_on_empty: "partition_on {} P \ P = {}"
unfolding partition_on_def by fastforce
lemma partition_on_space: "A \ {} \ partition_on A {A}"
by (auto simp: partition_on_def disjoint_def)
lemma partition_on_singletons: "partition_on A ((\x. {x}) ` A)"
by (auto simp: partition_on_def disjoint_def)
lemma partition_on_transform:
assumes P: "partition_on A P"
assumes F_UN: "\(F ` P) = F (\P)" and F_disjnt: "\p q. p \ P \ q \ P \ disjnt p q \ disjnt (F p) (F q)"
shows "partition_on (F A) (F ` P - {{}})"
proof -
have "\(F ` P - {{}}) = F A"
unfolding P[THEN partition_onD1] F_UN[symmetric] by auto
with P show ?thesis
by (auto simp add: partition_on_def pairwise_def intro!: F_disjnt)
qed
lemma partition_on_restrict: "partition_on A P \ partition_on (B \ A) ((\) B ` P - {{}})"
by (intro partition_on_transform) (auto simp: disjnt_def)
lemma partition_on_vimage: "partition_on A P \ partition_on (f -` A) ((-`) f ` P - {{}})"
by (intro partition_on_transform) (auto simp: disjnt_def)
lemma partition_on_inj_image:
assumes P: "partition_on A P" and f: "inj_on f A"
shows "partition_on (f ` A) ((`) f ` P - {{}})"
proof (rule partition_on_transform[OF P])
show "p \ P \ q \ P \ disjnt p q \ disjnt (f ` p) (f ` q)" for p q
using f[THEN inj_onD] P[THEN partition_onD1] by (auto simp: disjnt_def)
qed auto
lemma partition_on_insert:
assumes "disjnt p (\P)"
shows "partition_on A (insert p P) \ partition_on (A-p) P \ p \ A \ p \ {}"
using assms
by (auto simp: partition_on_def disjnt_iff pairwise_insert)
subsection ‹Finiteness of partitions›
lemma finitely_many_partition_on:
assumes "finite A"
shows "finite {P. partition_on A P}"
proof (rule finite_subset)
show "{P. partition_on A P} \ Pow (Pow A)"
unfolding partition_on_def by auto
show "finite (Pow (Pow A))"
using assms by simp
qed
lemma finite_elements: "finite A \ partition_on A P \ finite P"
using partition_onD1[of A P] by (simp add: finite_UnionD)
lemma product_partition:
assumes "partition_on A P" and "\p. p \ P \ finite p"
shows "card A = (\p\P. card p)"
using assms unfolding partition_on_def by (meson card_Union_disjoint)
subsection ‹Equivalence of partitions and equivalence classes›
lemma partition_on_quotient:
assumes r: "equiv A r"
shows "partition_on A (A // r)"
proof (rule partition_onI)
from r have "r \ A \ A" and "refl_on A r"
by (auto elim: equivE)
then show "\(A // r) = A" "{} \ A // r"
by (auto simp: refl_on_def quotient_def)
fix p q assume "p \ A // r" "q \ A // r" "p \ q"
then obtain x y where "x \ A" "y \ A" "p = r `` {x}" "q = r `` {y}"
by (auto simp: quotient_def)
with r equiv_class_eq_iff[OF r, of x y] ‹p ≠ q› show "disjnt p q"
by (auto simp: disjnt_equiv_class)
qed
lemma equiv_partition_on:
assumes P: "partition_on A P"
shows "equiv A {(x, y). \p \ P. x \ p \ y \ p}"
proof (rule equivI)
have "A = \P"
using P by (auto simp: partition_on_def)
show "{(x, y). \p \ P. x \ p \ y \ p} \ A \ A"
unfolding ‹A = ∪P› by blast
show "refl_on A {(x, y). \p\P. x \ p \ y \ p}"
unfolding refl_on_def ‹A = ∪P› by auto
next
show "trans {(x, y). \p\P. x \ p \ y \ p}"
using P by (auto simp only: trans_def disjoint_def partition_on_def)
next
show "sym {(x, y). \p\P. x \ p \ y \ p}"
by (auto simp only: sym_def)
qed
lemma partition_on_eq_quotient:
assumes P: "partition_on A P"
shows "A // {(x, y). \p \ P. x \ p \ y \ p} = P"
unfolding quotient_def
proof safe
fix x assume "x \ A"
then obtain p where "p \ P" "x \ p" "\q. q \ P \ x \ q \ p = q"
using P by (auto simp: partition_on_def disjoint_def)
then have "{y. \p\P. x \ p \ y \ p} = p"
by (safe intro!: bexI[of _ p]) simp
then show "{(x, y). \p\P. x \ p \ y \ p} `` {x} \ P"
by (simp add: ‹p ∈ P›)
next
fix p assume "p \ P"
then have "p \ {}"
using P by (auto simp: partition_on_def)
then obtain x where "x \ p"
by auto
then have "x \ A" "\q. q \ P \ x \ q \ p = q"
using P ‹p ∈ P› by (auto simp: partition_on_def disjoint_def)
with ‹p∈P› ‹x ∈ p› have "{y. \p\P. x \ p \ y \ p} = p"
by (safe intro!: bexI[of _ p]) simp
then show "p \ (\x\A. {{(x, y). \p\P. x \ p \ y \ p} `` {x}})"
by (auto intro: ‹x ∈ A›)
qed
lemma partition_on_alt: "partition_on A P \ (\r. equiv A r \ P = A // r)"
by (auto simp: partition_on_eq_quotient intro!: partition_on_quotient intro: equiv_partition_on)
lemma (in comm_monoid_set) partition:
assumes "finite X" "partition_on X A"
shows "F g X = F (\B. F g B) A"
proof -
have "finite A"
using assms finite_UnionD partition_onD1 by auto
have [intro]: "finite B" if "B \ A" for B
by (rule finite_subset[OF _ assms(1)])
(use assms that in ‹auto simp: partition_on_def›)
have "F g X = F g (\A)"
using assms by (simp add: partition_on_def)
also have "\ = (F \ F) g A"
by (rule Union_disjoint) (use assms ‹finite A› in ‹auto simp: partition_on_def disjoint_def›)
finally show ?thesis
by simp
qed
text ‹
If $h$ is an involution on $X$ with no fixed points in $X$ and
$f(h(x)) = -f(x)$ then $\sum_{x\in X} f(x) = 0$.
This is easy to show in a ring with characteristic not equal to $2$, since then we can do
\[\sum_{x\in X} f(x) = \sum_{x\in X} f(h(x)) = -\sum_{x\in X} f(x)\]
and therefore $2 \sum_{x\in X} f(x) = 0$.
However, the following proof also works in rings of characteristic 2.
The idea is to simply partition $X$ into a disjoint union of doubleton sets of the form
$\{x, h(x)\}$.
›
lemma sum_involution_eq_0:
assumes f_h: "\x. x \ X \ f (h x) + f x = 0"
assumes h: "\x. x \ X \ h x \ X" "\x. x \ X \ h (h x) = x" "\x. x \ X \ h x \ x"
shows "(\x\X. f x) = 0"
proof (cases "finite X")
assume fin: "finite X"
define R where "R = {(x,y). x \ X \ y \ X \ (x = y \ h x = y)}"
have R: "equiv X R"
unfolding equiv_def R_def using h(2,3)
by (auto simp: refl_on_def sym_def trans_def)
define A where "A = X // R"
have partition: "partition_on X A"
unfolding A_def using R by (rule partition_on_quotient)
have "(\x\X. f x) = (\B\A. \x\B. f x)"
by (subst sum.partition[OF fin partition]) auto
also have "\ = (\B\A. 0)"
proof (rule sum.cong)
fix B assume B: "B \ A"
then obtain x where x: "x \ X" and [simp]: "B = R `` {x}"
using R by (metis A_def quotientE)
have "R `` {x} = {x, h x}" "h x \ x"
using h x(1) by (auto simp: R_def)
thus "(\x\B. f x) = 0"
using x f_h[of x] by (simp add: add.commute)
qed auto
finally show ?thesis
by simp
qed auto
subsection ‹Refinement of partitions›
definition refines :: "'a set \ 'a set set \ 'a set set \ bool"
where "refines A P Q \
partition_on A P ∧ partition_on A Q ∧ (∀X∈P. ∃Y∈Q. X ⊆ Y)"
lemma refines_refl: "partition_on A P \ refines A P P"
using refines_def by blast
lemma refines_asym1:
assumes "refines A P Q" "refines A Q P"
shows "P \ Q"
proof
fix X
assume "X \ P"
then obtain Y X' where "Y \ Q" "X \ Y" "X' ∈ P" "Y ⊆ X'"
by (meson assms refines_def)
then have "X' = X"
using assms(2) unfolding partition_on_def refines_def
by (metis ‹X ∈ P› ‹X ⊆ Y› disjnt_self_iff_empty disjnt_subset1 pairwiseD)
then show "X \ Q"
using ‹X ⊆ Y› ‹Y ∈ Q› ‹Y ⊆ X'\ by force
qed
lemma refines_asym: "\refines A P Q; refines A Q P\ \ P=Q"
by (meson antisym_conv refines_asym1)
lemma refines_trans: "\refines A P Q; refines A Q R\ \ refines A P R"
by (meson order.trans refines_def)
lemma refines_obtains_subset:
assumes "refines A P Q" "q \ Q"
shows "partition_on q {p \ P. p \ q}"
proof -
have "p \ q \ disjnt p q" if "p \ P" for p
using that assms unfolding refines_def partition_on_def disjoint_def
by (metis disjnt_def disjnt_subset1)
with assms have "q \ Union {p \ P. p \ q}"
using assms
by (clarsimp simp: refines_def disjnt_iff partition_on_def) (metis Union_iff)
with assms have "q = Union {p \ P. p \ q}"
by auto
then show ?thesis
using assms by (auto simp: refines_def disjoint_def partition_on_def)
qed
subsection ‹The coarsest common refinement of a set of partitions›
definition common_refinement :: "'a set set set \ 'a set set"
where "common_refinement \ \ (\f \ (\\<^sub>E P\\. P). {\ (f ` \)}) - {{}}"
text ‹With non-extensional function space›
lemma common_refinement: "common_refinement \ = (\f \ (\ P\\. P). {\ (f ` \)}) - {{}}"
(is "?lhs = ?rhs")
proof
show "?rhs \ ?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: "\X \ common_refinement \; P \ \\ \ \R\P. X \ R"
by (auto simp add: common_refinement)
lemma Union_common_refinement: "\ (common_refinement \) = (\ P\\. \P)"
proof
show "(\ P\\. \P) \ \ (common_refinement \)"
proof (clarsimp simp: common_refinement)
fix x
assume "\P\\. \X\P. x \ X"
then obtain F where F: "\P. P\\ \ F P \ P \ x \ F P"
by metis
then have "x \ \ (F ` \)"
by force
with F show "\X\(\x\\ P\\. P. {\ (x ` \)}) - {{}}. x \ X"
by (auto simp add: Pi_iff Bex_def)
qed
qed (auto simp: common_refinement_def)
lemma partition_on_common_refinement:
assumes A: "\P. P \ \ \ partition_on A P"
and "\ \ {}"
shows "partition_on A (common_refinement \)"
proof (rule partition_onI)
show "\ (common_refinement \) = A"
using assms by (simp add: partition_on_def Union_common_refinement)
fix P Q
assume "P \ common_refinement \"
and "Q \ common_refinement \"
and "P \ Q"
then obtain f g where f: "f \ (\\<^sub>E P\\. P)"
and P: "P = \ (f ` \)"
and "P \ {}"
and g: "g \ (\\<^sub>E P\\. P)"
and Q: "Q = \ (g ` \)"
and "Q \ {}"
by (auto simp add: common_refinement_def)
have "f=g" if "x \ P" "x \ Q" for x
proof (rule extensionalityI [of _ P])
fix R
assume "R \ \"
with that P Q f g A [unfolded partition_on_def, OF ‹R ∈ P›]
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 ‹P ≠ Q› disjnt_iff)
qed (simp add: common_refinement_def)
lemma refines_common_refinement:
assumes "\P. P \ \ \ partition_on A P"
"P \ \"
shows "refines A (common_refinement \) P"
unfolding refines_def
proof (intro conjI strip)
fix X
assume "X \ common_refinement \"
with assms show "\Y\P. X \ Y"
by (auto simp: common_refinement_def)
qed (use assms partition_on_common_refinement in auto)
text ‹The common refinement is itself refined by any other›
lemma common_refinement_coarsest:
assumes "\P. P \ \ \ partition_on A P"
"partition_on A R" "\P. P \ \ \ refines A R P"
"\ \ {}"
shows "refines A R (common_refinement \)"
unfolding refines_def
proof (intro conjI ballI partition_on_common_refinement)
fix X
assume "X \ R"
have "\p \ P. X \ p" if "P \ \"
for P
by (meson ‹X ∈ R› assms(3) refines_def that)
then obtain F where f: "\P. P \ \ \ F P \ P \ X \ F P"
by metis
with ‹partition_on A R› ‹X ∈ R› ‹P ≠ {}›
have "\ (F ` \) \ common_refinement \"
apply (simp add: partition_on_def common_refinement Pi_iff Bex_def)
by (metis (no_types, lifting) cINF_greatest subset_empty)
with f show "\Y\common_refinement \. X \ Y"
by (metis ‹P ≠ {}› cINF_greatest)
qed (use assms in auto)
lemma finite_common_refinement:
assumes "finite \"
"\P. P \ \ \ finite P"
shows "finite (common_refinement \)"
proof -
have "finite (\\<^sub>E 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. P \ \ \ finite P"
shows "card (common_refinement \) \ (\P \ \. card P)"
proof -
have "card (common_refinement \) \ card (\f \ (\\<^sub>E P\\. P). {\ (f ` \)})"
unfolding common_refinement_def by (meson card_Diff1_le)
also have "\ \ (\f\(\\<^sub>E P\\. P). card{\ (f ` \)})"
by (metis assms finite_PiE card_UN_le)
also have "\ = card(\\<^sub>E P\\. P)"
by simp
also have "\ = (\P \ \. card P)"
by (simp add: assms(1) card_PiE dual_order.eq_iff)
finally show ?thesis .
qed
end
