Quelle Disjoint_Sets.thy Sprache: Isabelle

(* Author: Johannes Hölzl, TU München
*)

section \<open>Partitions and Disjoint Sets\<close>

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 \<open>Set of Disjoint Sets\<close>

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 \<open>i\<in>I\<close>, 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 \: "pairwise disjnt \" and "\<A> \<subset> \ - {{}}"
 shows "\\ \ \\"
 unfolding psubset_eq
proof
 show "\\ \ \\"
 using assms by blast
 have "\ \ \" "\(\ - \ \ (\ - {{}})) \ {}"
 using assms by blast+
 then show "\\ \ \\"
 using diff_Union_pairwise_disjoint [OF \] 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 \<open>infinite A\<close> finite_image_iff by blast
 then show False
 by (meson \<open>finite C\<close> 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_image 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] \<open>i \<in> I\<close> \<open>A \<in> F i\<close> \<open>B \<in> F j\<close> \<open>A \<noteq> B\<close> show "A \<inter> B = {}"
 by (auto dest: disjointD)
 next
 assume "i \ j"
 with * \<open>i\<in>I\<close> \<open>j\<in>I\<close> have "(\<Union>(F i)) \<inter> (\<Union>(F j)) = {}"
 by (rule disjoint_family_onD)
 with \<open>A\<in>F i\<close> \<open>i\<in>I\<close> \<open>B\<in>F j\<close> \<open>j\<in>I\<close>
 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 \<open>
 Sum/product of the union of a finite disjoint family
\<close>
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 \<open>
 The union of an infinite disjoint family of non-empty sets is infinite.
\<close>
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 \<open>x \<noteq> y\<close> 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 \<open>\<not>finite A\<close> have "\<not>finite (g ` A)"
 using finite_imageD by blast
 ultimately show ?thesis using finite_subset by blast
qed


subsection \<open>Construct Disjoint Sequences\<close>

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 \<open>Partitions\<close>

text \<open>
 Partitions \<^term>\<open>P\<close> of a set \<^term>\<open>A\<close>. We explicitly disallow empty sets.
\<close>

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 \<open>Constructions of partitions\<close>

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 \<open>Finiteness of partitions\<close>

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 \<open>Equivalence of partitions and equivalence classes\<close>

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] \<open>p \<noteq> q\<close> 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 \<open>A = \<Union>P\<close> by blast

 show "refl_on A {(x, y). \p\P. x \ p \ y \ p}"
 unfolding refl_on_def \<open>A = \<Union>P\<close> 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: \<open>p \<in> P\<close>)
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 \<open>p \<in> P\<close> by (auto simp: partition_on_def disjoint_def)
 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"
 by (safe intro!: bexI[of _ p]) simp
 then show "p \ (\x\A. {{(x, y). \p\P. x \ p \ y \ p} `` {x}})"
 by (auto intro: \<open>x \<in> A\<close>)
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 \<open>auto simp: partition_on_def\<close>)
 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 \<open>finite A\<close> in \<open>auto simp: partition_on_def disjoint_def\<close>)
 finally show ?thesis
 by simp
qed

text \<open>
 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)\}$.
\<close>
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 \<open>Refinement of partitions\<close>

definition refines :: "'a set \ 'a set set \ 'a set set \ bool"
 where "refines A P Q \
 partition_on A P \<and> partition_on A Q \<and> (\<forall>X\<in>P. \<exists>Y\<in>Q. X \<subseteq> 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 \<open>X \<in> P\<close> \<open>X \<subseteq> Y\<close> disjnt_self_iff_empty disjnt_subset1 pairwiseD)
 then show "X \ Q"
 using \<open>X \<subseteq> Y\<close> \<open>Y \<in> Q\<close> \<open>Y \<subseteq> X'\<close> 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 \<open>The coarsest common refinement of a set of partitions\<close>

definition common_refinement :: "'a set set set \ 'a set set"
 where "common_refinement \
\ (\f \ (\\<^sub>E P\\
. P). {\ (f ` \
)}) - {{}}"

text \<open>With non-extensional function space\<close>
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 _ \])
 fix R
 assume "R \ \
"
 with that P Q f g A [unfolded partition_on_def, OF \<open>R \<in> \\<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 "\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 \<open>The common refinement is itself refined by any other\<close>
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 \<open>X \<in> R\<close> assms(3) refines_def that)
 then obtain F where f: "\P. P \ \
\ F P \ P \ X \ F P"
 by metis
 with \<open>partition_on A R\<close> \<open>X \<in> R\<close> \<open>\ \<noteq> {}\<close>
 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 \<open>\ \<noteq> {}\<close> 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

quality97%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.