# HG changeset patch # User paulson # Date 1673543556 0 # Node ID 5df58a471d9e55f5d39cacad98d8f25f3887121f # Parent 7ed303c024187025d7c89dd9d27a42284c1a34b4 Trying to clean up HOL/Cardinals diff -r 7ed303c02418 -r 5df58a471d9e src/HOL/Cardinals/Cardinal_Arithmetic.thy --- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Wed Jan 11 17:02:52 2023 +0000 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Thu Jan 12 17:12:36 2023 +0000 @@ -8,15 +8,15 @@ section \Cardinal Arithmetic\ theory Cardinal_Arithmetic -imports Cardinal_Order_Relation + imports Cardinal_Order_Relation begin subsection \Binary sum\ lemma csum_Cnotzero2: "Cnotzero r2 \ Cnotzero (r1 +c r2)" -unfolding csum_def -by (metis Cnotzero_imp_not_empty Field_card_of Plus_eq_empty_conv card_of_card_order_on czeroE) + unfolding csum_def + by (metis Cnotzero_imp_not_empty Field_card_of Plus_eq_empty_conv card_of_card_order_on czeroE) lemma single_cone: "|{x}| =o cone" @@ -27,10 +27,10 @@ qed lemma cone_Cnotzero: "Cnotzero cone" -by (simp add: cone_not_czero Card_order_cone) + by (simp add: cone_not_czero Card_order_cone) lemma cone_ordLeq_ctwo: "cone \o ctwo" -unfolding cone_def ctwo_def card_of_ordLeq[symmetric] by auto + unfolding cone_def ctwo_def card_of_ordLeq[symmetric] by auto lemma csum_czero1: "Card_order r \ r +c czero =o r" unfolding czero_def csum_def Field_card_of @@ -44,7 +44,7 @@ subsection \Product\ lemma Times_cprod: "|A \ B| =o |A| *c |B|" -by (simp only: cprod_def Field_card_of card_of_refl) + by (simp only: cprod_def Field_card_of card_of_refl) lemma card_of_Times_singleton: fixes A :: "'a set" @@ -64,21 +64,20 @@ lemma cprod_cone: "Card_order r \ r *c cone =o r" unfolding cprod_def cone_def Field_card_of - by (drule card_of_Field_ordIso) (erule ordIso_transitive[OF card_of_Times_singleton]) - + by (metis (no_types) card_of_Field_ordIso card_of_Times_singleton ordIso_transitive) lemma ordLeq_cprod1: "\Card_order p1; Cnotzero p2\ \ p1 \o p1 *c p2" -unfolding cprod_def by (metis Card_order_Times1 czeroI) + unfolding cprod_def by (metis Card_order_Times1 czeroI) subsection \Exponentiation\ lemma cexp_czero: "r ^c czero =o cone" -unfolding cexp_def czero_def Field_card_of Func_empty by (rule single_cone) + unfolding cexp_def czero_def Field_card_of Func_empty by (rule single_cone) lemma Pow_cexp_ctwo: "|Pow A| =o ctwo ^c |A|" -unfolding ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func) + by (simp add: card_of_Pow_Func cexp_def ctwo_def) lemma Cnotzero_cexp: assumes "Cnotzero q" @@ -92,29 +91,24 @@ lemma Cinfinite_ctwo_cexp: "Cinfinite r \ Cinfinite (ctwo ^c r)" -unfolding ctwo_def cexp_def cinfinite_def Field_card_of -by (rule conjI, rule infinite_Func, auto) + unfolding ctwo_def cexp_def cinfinite_def Field_card_of + by (rule conjI, rule infinite_Func, auto) lemma cone_ordLeq_iff_Field: assumes "cone \o r" shows "Field r \ {}" -proof (rule ccontr) - assume "\ Field r \ {}" - hence "Field r = {}" by simp - thus False using card_of_empty3 - card_of_mono2[OF assms] Cnotzero_imp_not_empty[OF cone_Cnotzero] by auto -qed + by (metis assms card_of_empty3 card_of_mono2 cone_Cnotzero czeroI) lemma cone_ordLeq_cexp: "cone \o r1 \ cone \o r1 ^c r2" -by (simp add: cexp_def cone_def Func_non_emp cone_ordLeq_iff_Field) + by (simp add: cexp_def cone_def Func_non_emp cone_ordLeq_iff_Field) lemma Card_order_czero: "Card_order czero" -by (simp only: card_of_Card_order czero_def) + by (simp only: card_of_Card_order czero_def) lemma cexp_mono2'': assumes 2: "p2 \o r2" - and n1: "Cnotzero q" - and n2: "Card_order p2" + and n1: "Cnotzero q" + and n2: "Card_order p2" shows "q ^c p2 \o q ^c r2" proof (cases "p2 =o (czero :: 'a rel)") case True @@ -129,28 +123,20 @@ lemma csum_cexp: "\Cinfinite r1; Cinfinite r2; Card_order q; ctwo \o q\ \ q ^c r1 +c q ^c r2 \o q ^c (r1 +c r2)" apply (rule csum_cinfinite_bound) - apply (metis cexp_mono2' cinfinite_def finite.emptyI ordLeq_csum1) - apply (metis cexp_mono2' cinfinite_def finite.emptyI ordLeq_csum2) + apply (metis cexp_mono2' cinfinite_def finite.emptyI ordLeq_csum1) + apply (metis cexp_mono2' cinfinite_def finite.emptyI ordLeq_csum2) by (simp_all add: Card_order_cexp Cinfinite_csum1 Cinfinite_cexp cinfinite_cexp) lemma csum_cexp': "\Cinfinite r; Card_order q; ctwo \o q\ \ q +c r \o q ^c r" -apply (rule csum_cinfinite_bound) - apply (metis Cinfinite_Cnotzero ordLeq_cexp1) - apply (metis ordLeq_cexp2) - apply blast+ -by (metis Cinfinite_cexp) + apply (rule csum_cinfinite_bound) + apply (metis Cinfinite_Cnotzero ordLeq_cexp1) + apply (metis ordLeq_cexp2) + apply blast+ + by (metis Cinfinite_cexp) lemma card_of_Sigma_ordLeq_Cinfinite: "\Cinfinite r; |I| \o r; \i \ I. |A i| \o r\ \ |SIGMA i : I. A i| \o r" -unfolding cinfinite_def by (blast intro: card_of_Sigma_ordLeq_infinite_Field) - -lemma card_order_cexp: - assumes "card_order r1" "card_order r2" - shows "card_order (r1 ^c r2)" -proof - - have "Field r1 = UNIV" "Field r2 = UNIV" using assms card_order_on_Card_order by auto - thus ?thesis unfolding cexp_def Func_def by simp -qed + unfolding cinfinite_def by (blast intro: card_of_Sigma_ordLeq_infinite_Field) lemma Cinfinite_ordLess_cexp: assumes r: "Cinfinite r" @@ -165,19 +151,19 @@ lemma infinite_ordLeq_cexp: assumes "Cinfinite r" shows "r \o r ^c r" -by (rule ordLess_imp_ordLeq[OF Cinfinite_ordLess_cexp[OF assms]]) + by (rule ordLess_imp_ordLeq[OF Cinfinite_ordLess_cexp[OF assms]]) lemma czero_cexp: "Cnotzero r \ czero ^c r =o czero" - by (drule Cnotzero_imp_not_empty) (simp add: cexp_def czero_def card_of_empty_ordIso) + by (metis Cnotzero_imp_not_empty cexp_def czero_def card_of_empty_ordIso Field_card_of Func_is_emp) lemma Func_singleton: -fixes x :: 'b and A :: "'a set" -shows "|Func A {x}| =o |{x}|" + fixes x :: 'b and A :: "'a set" + shows "|Func A {x}| =o |{x}|" proof (rule ordIso_symmetric) define f where [abs_def]: "f y a = (if y = x \ a \ A then x else undefined)" for y a have "Func A {x} \ f ` {x}" unfolding f_def Func_def by (force simp: fun_eq_iff) - hence "bij_betw f {x} (Func A {x})" unfolding bij_betw_def inj_on_def f_def Func_def - by (auto split: if_split_asm) + hence "bij_betw f {x} (Func A {x})" + unfolding bij_betw_def inj_on_def f_def Func_def by (auto split: if_split_asm) thus "|{x}| =o |Func A {x}|" using card_of_ordIso by blast qed @@ -225,32 +211,32 @@ definition cpow where "cpow r = |Pow (Field r)|" lemma card_order_cpow: "card_order r \ card_order (cpow r)" -by (simp only: cpow_def Field_card_order Pow_UNIV card_of_card_order_on) + by (simp only: cpow_def Field_card_order Pow_UNIV card_of_card_order_on) lemma cpow_greater_eq: "Card_order r \ r \o cpow r" -by (rule ordLess_imp_ordLeq) (simp only: cpow_def Card_order_Pow) + by (rule ordLess_imp_ordLeq) (simp only: cpow_def Card_order_Pow) lemma Cinfinite_cpow: "Cinfinite r \ Cinfinite (cpow r)" -unfolding cpow_def cinfinite_def by (metis Field_card_of card_of_Card_order infinite_Pow) + unfolding cpow_def cinfinite_def by simp lemma Card_order_cpow: "Card_order (cpow r)" -unfolding cpow_def by (rule card_of_Card_order) + unfolding cpow_def by (rule card_of_Card_order) lemma cardSuc_ordLeq_cpow: "Card_order r \ cardSuc r \o cpow r" -unfolding cpow_def by (metis Card_order_Pow cardSuc_ordLess_ordLeq card_of_Card_order) + unfolding cpow_def by (metis Card_order_Pow cardSuc_ordLess_ordLeq card_of_Card_order) lemma cpow_cexp_ctwo: "cpow r =o ctwo ^c r" -unfolding cpow_def ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func) + unfolding cpow_def ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func) subsection \Inverse image\ lemma vimage_ordLeq: -assumes "|A| \o k" and "\ a \ A. |vimage f {a}| \o k" and "Cinfinite k" -shows "|vimage f A| \o k" + assumes "|A| \o k" and "\ a \ A. |vimage f {a}| \o k" and "Cinfinite k" + shows "|vimage f A| \o k" proof- have "vimage f A = (\a \ A. vimage f {a})" by auto also have "|\a \ A. vimage f {a}| \o k" - using UNION_Cinfinite_bound[OF assms] . + using UNION_Cinfinite_bound[OF assms] . finally show ?thesis . qed @@ -268,7 +254,8 @@ lemma cmax1: assumes "Card_order r" "Card_order s" "s \o r" shows "cmax r s =o r" -unfolding cmax_def proof (split if_splits, intro conjI impI) + unfolding cmax_def +proof (split if_splits, intro conjI impI) assume "cinfinite r \ cinfinite s" hence Cinf: "Cinfinite r" using assms(1,3) by (metis cinfinite_mono) have "czero +c r +c s =o r +c s" by (rule csum_czero2[OF Card_order_csum]) @@ -299,33 +286,14 @@ shows "cmax r s =o s" by (metis assms cmax1 cmax_com ordIso_transitive) -lemma csum_absorb2: "Cinfinite r2 \ r1 \o r2 \ r1 +c r2 =o r2" - by (metis csum_absorb2') - -lemma cprod_infinite2': "\Cnotzero r1; Cinfinite r2; r1 \o r2\ \ r1 *c r2 =o r2" - unfolding ordIso_iff_ordLeq - by (intro conjI cprod_cinfinite_bound ordLeq_cprod2 ordLeq_refl) - (auto dest!: ordIso_imp_ordLeq not_ordLeq_ordLess simp: czero_def Card_order_empty) - context fixes r s assumes r: "Cinfinite r" - and s: "Cinfinite s" + and s: "Cinfinite s" begin lemma cmax_csum: "cmax r s =o r +c s" -proof (cases "r \o s") - case True - hence "cmax r s =o s" by (metis cmax2 r s) - also have "s =o r +c s" by (metis True csum_absorb2 ordIso_symmetric s) - finally show ?thesis . -next - case False - hence "s \o r" by (metis ordLeq_total r s card_order_on_def) - hence "cmax r s =o r" by (metis cmax1 r s) - also have "r =o r +c s" by (metis \s \o r\ csum_absorb1 ordIso_symmetric r) - finally show ?thesis . -qed + by (simp add: Card_order_csum cmax_def csum_czero2 r) lemma cmax_cprod: "cmax r s =o r *c s" proof (cases "r \o s") @@ -344,39 +312,21 @@ end lemma Card_order_cmax: -assumes r: "Card_order r" and s: "Card_order s" -shows "Card_order (cmax r s)" -unfolding cmax_def by (auto simp: Card_order_csum) + assumes r: "Card_order r" and s: "Card_order s" + shows "Card_order (cmax r s)" + unfolding cmax_def by (auto simp: Card_order_csum) lemma ordLeq_cmax: -assumes r: "Card_order r" and s: "Card_order s" -shows "r \o cmax r s \ s \o cmax r s" -proof- - {assume "r \o s" - hence ?thesis by (metis cmax2 ordIso_iff_ordLeq ordLeq_transitive r s) - } - moreover - {assume "s \o r" - hence ?thesis using cmax_com by (metis cmax2 ordIso_iff_ordLeq ordLeq_transitive r s) - } - ultimately show ?thesis using r s ordLeq_total unfolding card_order_on_def by auto -qed + assumes r: "Card_order r" and s: "Card_order s" + shows "r \o cmax r s \ s \o cmax r s" + by (meson card_order_on_def cmax1 cmax2 ordIso_iff_ordLeq ordLeq_total ordLeq_transitive r s) lemmas ordLeq_cmax1 = ordLeq_cmax[THEN conjunct1] and - ordLeq_cmax2 = ordLeq_cmax[THEN conjunct2] + ordLeq_cmax2 = ordLeq_cmax[THEN conjunct2] lemma finite_cmax: -assumes r: "Card_order r" and s: "Card_order s" -shows "finite (Field (cmax r s)) \ finite (Field r) \ finite (Field s)" -proof- - {assume "r \o s" - hence ?thesis by (metis cmax2 ordIso_finite_Field ordLeq_finite_Field r s) - } - moreover - {assume "s \o r" - hence ?thesis by (metis cmax1 ordIso_finite_Field ordLeq_finite_Field r s) - } - ultimately show ?thesis using r s ordLeq_total unfolding card_order_on_def by auto -qed + assumes r: "Card_order r" and s: "Card_order s" + shows "finite (Field (cmax r s)) \ finite (Field r) \ finite (Field s)" + by (meson card_order_on_def cmax1 cmax2 ordIso_finite_Field ordLeq_finite_Field ordLeq_total r s) end diff -r 7ed303c02418 -r 5df58a471d9e src/HOL/Cardinals/Cardinal_Order_Relation.thy --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Wed Jan 11 17:02:52 2023 +0000 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Thu Jan 12 17:12:36 2023 +0000 @@ -8,7 +8,7 @@ section \Cardinal-Order Relations\ theory Cardinal_Order_Relation -imports Wellorder_Constructions + imports Wellorder_Constructions begin declare @@ -72,46 +72,36 @@ subsection \Cardinal of a set\ lemma card_of_inj_rel: assumes INJ: "\x y y'. \(x,y) \ R; (x,y') \ R\ \ y = y'" -shows "|{y. \x. (x,y) \ R}| <=o |{x. \y. (x,y) \ R}|" + shows "|{y. \x. (x,y) \ R}| <=o |{x. \y. (x,y) \ R}|" proof- let ?Y = "{y. \x. (x,y) \ R}" let ?X = "{x. \y. (x,y) \ R}" let ?f = "\y. SOME x. (x,y) \ R" have "?f ` ?Y <= ?X" by (auto dest: someI) moreover have "inj_on ?f ?Y" - unfolding inj_on_def proof(auto) - fix y1 x1 y2 x2 - assume *: "(x1, y1) \ R" "(x2, y2) \ R" and **: "?f y1 = ?f y2" - hence "(?f y1,y1) \ R" using someI[of "\x. (x,y1) \ R"] by auto - moreover have "(?f y2,y2) \ R" using * someI[of "\x. (x,y2) \ R"] by auto - ultimately show "y1 = y2" using ** INJ by auto - qed + by (metis (mono_tags, lifting) assms inj_onI mem_Collect_eq) ultimately show "|?Y| <=o |?X|" using card_of_ordLeq by blast qed lemma card_of_unique2: "\card_order_on B r; bij_betw f A B\ \ r =o |A|" -using card_of_ordIso card_of_unique ordIso_equivalence by blast + using card_of_ordIso card_of_unique ordIso_equivalence by blast lemma internalize_card_of_ordLess2: -"( |A| B < C. |A| =o |B| \ |B| B < C. |A| =o |B| \ |B| {}" and "\r\R. Card_order r" -shows "Card_order (omax R)" -proof- - have "\r\R. Well_order r" - using assms unfolding card_order_on_def by simp - thus ?thesis using assms apply - apply(drule omax_in) by auto -qed + assumes "finite R" and "R \ {}" and "\r\R. Card_order r" + shows "Card_order (omax R)" + by (simp add: assms omax_in) lemma Card_order_omax2: -assumes "finite I" and "I \ {}" -shows "Card_order (omax {|A i| | i. i \ I})" + assumes "finite I" and "I \ {}" + shows "Card_order (omax {|A i| | i. i \ I})" proof- let ?R = "{|A i| | i. i \ I}" have "finite ?R" and "?R \ {}" using assms by auto moreover have "\r\?R. Card_order r" - using card_of_Card_order by auto + using card_of_Card_order by auto ultimately show ?thesis by(rule Card_order_omax) qed @@ -119,138 +109,104 @@ subsection \Cardinals versus set operations on arbitrary sets\ lemma card_of_set_type[simp]: "|UNIV::'a set| o |A \ B| " -using inj_on_id[of A] card_of_ordLeq[of A _] by fastforce +lemma card_of_Un1[simp]: "|A| \o |A \ B| " + by fastforce -lemma card_of_diff[simp]: -shows "|A - B| \o |A|" -using inj_on_id[of "A - B"] card_of_ordLeq[of "A - B" _] by fastforce +lemma card_of_diff[simp]: "|A - B| \o |A|" + by fastforce lemma subset_ordLeq_strict: -assumes "A \ B" and "|A| (A < B)" - hence "A = B" using assms(1) by blast - hence False using assms(2) not_ordLess_ordIso card_of_refl by blast - } - thus ?thesis by blast -qed + assumes "A \ B" and "|A| B" and "|A| {}" -using assms subset_ordLeq_strict by blast + assumes "A \ B" and "|A| {}" + using assms subset_ordLeq_strict by blast lemma card_of_empty4: -"|{}::'b set| {})" -proof(intro iffI notI) - assume *: "|{}::'b set| {}" - hence "(\ (\f. inj_on f A \ f ` A \ {}))" - unfolding inj_on_def by blast - thus "| {} | {})" + by (metis card_of_empty card_of_ordLess2 image_is_empty not_ordLess_ordLeq) lemma card_of_empty5: -"|A| B \ {}" -using card_of_empty not_ordLess_ordLeq by blast + "|A| B \ {}" + using card_of_empty not_ordLess_ordLeq by blast lemma Well_order_card_of_empty: -"Well_order r \ |{}| \o r" by simp + "Well_order r \ |{}| \o r" + by simp lemma card_of_UNIV[simp]: -"|A :: 'a set| \o |UNIV :: 'a set|" -using card_of_mono1[of A] by simp + "|A :: 'a set| \o |UNIV :: 'a set|" + by simp lemma card_of_UNIV2[simp]: -"Card_order r \ (r :: 'a rel) \o |UNIV :: 'a set|" -using card_of_UNIV[of "Field r"] card_of_Field_ordIso - ordIso_symmetric ordIso_ordLeq_trans by blast + "Card_order r \ (r :: 'a rel) \o |UNIV :: 'a set|" + using card_of_UNIV[of "Field r"] card_of_Field_ordIso + ordIso_symmetric ordIso_ordLeq_trans by blast lemma card_of_Pow_mono[simp]: -assumes "|A| \o |B|" -shows "|Pow A| \o |Pow B|" + assumes "|A| \o |B|" + shows "|Pow A| \o |Pow B|" proof- obtain f where "inj_on f A \ f ` A \ B" - using assms card_of_ordLeq[of A B] by auto + using assms card_of_ordLeq[of A B] by auto hence "inj_on (image f) (Pow A) \ (image f) ` (Pow A) \ (Pow B)" - by (auto simp add: inj_on_image_Pow image_Pow_mono) + by (auto simp: inj_on_image_Pow image_Pow_mono) thus ?thesis using card_of_ordLeq[of "Pow A"] by metis qed lemma ordIso_Pow_mono[simp]: -assumes "r \o r'" -shows "|Pow(Field r)| \o |Pow(Field r')|" -using assms card_of_mono2 card_of_Pow_mono by blast + assumes "r \o r'" + shows "|Pow(Field r)| \o |Pow(Field r')|" + using assms card_of_mono2 card_of_Pow_mono by blast lemma card_of_Pow_cong[simp]: -assumes "|A| =o |B|" -shows "|Pow A| =o |Pow B|" -proof- - obtain f where "bij_betw f A B" - using assms card_of_ordIso[of A B] by auto - hence "bij_betw (image f) (Pow A) (Pow B)" - by (auto simp add: bij_betw_image_Pow) - thus ?thesis using card_of_ordIso[of "Pow A"] by auto -qed + assumes "|A| =o |B|" + shows "|Pow A| =o |Pow B|" + by (meson assms card_of_Pow_mono ordIso_iff_ordLeq) lemma ordIso_Pow_cong[simp]: -assumes "r =o r'" -shows "|Pow(Field r)| =o |Pow(Field r')|" -using assms card_of_cong card_of_Pow_cong by blast + assumes "r =o r'" + shows "|Pow(Field r)| =o |Pow(Field r')|" + using assms card_of_cong card_of_Pow_cong by blast corollary Card_order_Plus_empty1: -"Card_order r \ r =o |(Field r) <+> {}|" -using card_of_Plus_empty1 card_of_Field_ordIso ordIso_equivalence by blast + "Card_order r \ r =o |(Field r) <+> {}|" + using card_of_Plus_empty1 card_of_Field_ordIso ordIso_equivalence by blast corollary Card_order_Plus_empty2: -"Card_order r \ r =o |{} <+> (Field r)|" -using card_of_Plus_empty2 card_of_Field_ordIso ordIso_equivalence by blast - -lemma Card_order_Un1: -shows "Card_order r \ |Field r| \o |(Field r) \ B| " -using card_of_Un1 card_of_Field_ordIso ordIso_symmetric ordIso_ordLeq_trans by auto + "Card_order r \ r =o |{} <+> (Field r)|" + using card_of_Plus_empty2 card_of_Field_ordIso ordIso_equivalence by blast lemma card_of_Un2[simp]: -shows "|A| \o |B \ A|" -using inj_on_id[of A] card_of_ordLeq[of A _] by fastforce - -lemma Card_order_Un2: -shows "Card_order r \ |Field r| \o |A \ (Field r)| " -using card_of_Un2 card_of_Field_ordIso ordIso_symmetric ordIso_ordLeq_trans by auto + shows "|A| \o |B \ A|" + by fastforce lemma Un_Plus_bij_betw: -assumes "A Int B = {}" -shows "\f. bij_betw f (A \ B) (A <+> B)" + assumes "A Int B = {}" + shows "\f. bij_betw f (A \ B) (A <+> B)" proof- - let ?f = "\ c. if c \ A then Inl c else Inr c" - have "bij_betw ?f (A \ B) (A <+> B)" - using assms by(unfold bij_betw_def inj_on_def, auto) + have "bij_betw (\ c. if c \ A then Inl c else Inr c) (A \ B) (A <+> B)" + using assms unfolding bij_betw_def inj_on_def by auto thus ?thesis by blast qed lemma card_of_Un_Plus_ordIso: -assumes "A Int B = {}" -shows "|A \ B| =o |A <+> B|" -using assms card_of_ordIso[of "A \ B"] Un_Plus_bij_betw[of A B] by auto + assumes "A Int B = {}" + shows "|A \ B| =o |A <+> B|" + by (meson Un_Plus_bij_betw assms card_of_ordIso) lemma card_of_Un_Plus_ordIso1: -"|A \ B| =o |A <+> (B - A)|" -using card_of_Un_Plus_ordIso[of A "B - A"] by auto + "|A \ B| =o |A <+> (B - A)|" + using card_of_Un_Plus_ordIso[of A "B - A"] by auto lemma card_of_Un_Plus_ordIso2: -"|A \ B| =o |(A - B) <+> B|" -using card_of_Un_Plus_ordIso[of "A - B" B] by auto + "|A \ B| =o |(A - B) <+> B|" + using card_of_Un_Plus_ordIso[of "A - B" B] by auto lemma card_of_Times_singl1: "|A| =o |A \ {b}|" proof- @@ -259,18 +215,19 @@ qed corollary Card_order_Times_singl1: -"Card_order r \ r =o |(Field r) \ {b}|" -using card_of_Times_singl1[of _ b] card_of_Field_ordIso ordIso_equivalence by blast + "Card_order r \ r =o |(Field r) \ {b}|" + using card_of_Times_singl1[of _ b] card_of_Field_ordIso ordIso_equivalence by blast lemma card_of_Times_singl2: "|A| =o |{b} \ A|" proof- - have "bij_betw snd ({b} \ A) A" unfolding bij_betw_def inj_on_def by force + have "bij_betw snd ({b} \ A) A" + unfolding bij_betw_def inj_on_def by force thus ?thesis using card_of_ordIso ordIso_symmetric by blast qed corollary Card_order_Times_singl2: -"Card_order r \ r =o |{a} \ (Field r)|" -using card_of_Times_singl2[of _ a] card_of_Field_ordIso ordIso_equivalence by blast + "Card_order r \ r =o |{a} \ (Field r)|" + using card_of_Times_singl2[of _ a] card_of_Field_ordIso ordIso_equivalence by blast lemma card_of_Times_assoc: "|(A \ B) \ C| =o |A \ B \ C|" proof - @@ -284,118 +241,111 @@ thus "x \ ?f ` ((A \ B) \ C)" by blast qed hence "bij_betw ?f ((A \ B) \ C) (A \ B \ C)" - unfolding bij_betw_def inj_on_def by auto + unfolding bij_betw_def inj_on_def by auto thus ?thesis using card_of_ordIso by blast qed -corollary Card_order_Times3: -"Card_order r \ |Field r| \o |(Field r) \ (Field r)|" - by (rule card_of_Times3) - lemma card_of_Times_cong1[simp]: -assumes "|A| =o |B|" -shows "|A \ C| =o |B \ C|" -using assms by (simp add: ordIso_iff_ordLeq) + assumes "|A| =o |B|" + shows "|A \ C| =o |B \ C|" + using assms by (simp add: ordIso_iff_ordLeq) lemma card_of_Times_cong2[simp]: -assumes "|A| =o |B|" -shows "|C \ A| =o |C \ B|" -using assms by (simp add: ordIso_iff_ordLeq) + assumes "|A| =o |B|" + shows "|C \ A| =o |C \ B|" + using assms by (simp add: ordIso_iff_ordLeq) lemma card_of_Times_mono[simp]: -assumes "|A| \o |B|" and "|C| \o |D|" -shows "|A \ C| \o |B \ D|" -using assms card_of_Times_mono1[of A B C] card_of_Times_mono2[of C D B] - ordLeq_transitive[of "|A \ C|"] by blast + assumes "|A| \o |B|" and "|C| \o |D|" + shows "|A \ C| \o |B \ D|" + using assms card_of_Times_mono1[of A B C] card_of_Times_mono2[of C D B] + ordLeq_transitive[of "|A \ C|"] by blast corollary ordLeq_Times_mono: -assumes "r \o r'" and "p \o p'" -shows "|(Field r) \ (Field p)| \o |(Field r') \ (Field p')|" -using assms card_of_mono2[of r r'] card_of_mono2[of p p'] card_of_Times_mono by blast + assumes "r \o r'" and "p \o p'" + shows "|(Field r) \ (Field p)| \o |(Field r') \ (Field p')|" + using assms card_of_mono2[of r r'] card_of_mono2[of p p'] card_of_Times_mono by blast corollary ordIso_Times_cong1[simp]: -assumes "r =o r'" -shows "|(Field r) \ C| =o |(Field r') \ C|" -using assms card_of_cong card_of_Times_cong1 by blast + assumes "r =o r'" + shows "|(Field r) \ C| =o |(Field r') \ C|" + using assms card_of_cong card_of_Times_cong1 by blast corollary ordIso_Times_cong2: -assumes "r =o r'" -shows "|A \ (Field r)| =o |A \ (Field r')|" -using assms card_of_cong card_of_Times_cong2 by blast + assumes "r =o r'" + shows "|A \ (Field r)| =o |A \ (Field r')|" + using assms card_of_cong card_of_Times_cong2 by blast lemma card_of_Times_cong[simp]: -assumes "|A| =o |B|" and "|C| =o |D|" -shows "|A \ C| =o |B \ D|" -using assms -by (auto simp add: ordIso_iff_ordLeq) + assumes "|A| =o |B|" and "|C| =o |D|" + shows "|A \ C| =o |B \ D|" + using assms + by (auto simp: ordIso_iff_ordLeq) corollary ordIso_Times_cong: -assumes "r =o r'" and "p =o p'" -shows "|(Field r) \ (Field p)| =o |(Field r') \ (Field p')|" -using assms card_of_cong[of r r'] card_of_cong[of p p'] card_of_Times_cong by blast + assumes "r =o r'" and "p =o p'" + shows "|(Field r) \ (Field p)| =o |(Field r') \ (Field p')|" + using assms card_of_cong[of r r'] card_of_cong[of p p'] card_of_Times_cong by blast lemma card_of_Sigma_mono2: -assumes "inj_on f (I::'i set)" and "f ` I \ (J::'j set)" -shows "|SIGMA i : I. (A::'j \ 'a set) (f i)| \o |SIGMA j : J. A j|" + assumes "inj_on f (I::'i set)" and "f ` I \ (J::'j set)" + shows "|SIGMA i : I. (A::'j \ 'a set) (f i)| \o |SIGMA j : J. A j|" proof- let ?LEFT = "SIGMA i : I. A (f i)" let ?RIGHT = "SIGMA j : J. A j" obtain u where u_def: "u = (\(i::'i,a::'a). (f i,a))" by blast have "inj_on u ?LEFT \ u `?LEFT \ ?RIGHT" - using assms unfolding u_def inj_on_def by auto + using assms unfolding u_def inj_on_def by auto thus ?thesis using card_of_ordLeq by blast qed lemma card_of_Sigma_mono: -assumes INJ: "inj_on f I" and IM: "f ` I \ J" and - LEQ: "\j \ J. |A j| \o |B j|" -shows "|SIGMA i : I. A (f i)| \o |SIGMA j : J. B j|" + assumes INJ: "inj_on f I" and IM: "f ` I \ J" and + LEQ: "\j \ J. |A j| \o |B j|" + shows "|SIGMA i : I. A (f i)| \o |SIGMA j : J. B j|" proof- have "\i \ I. |A(f i)| \o |B(f i)|" - using IM LEQ by blast + using IM LEQ by blast hence "|SIGMA i : I. A (f i)| \o |SIGMA i : I. B (f i)|" - using card_of_Sigma_mono1[of I] by metis + using card_of_Sigma_mono1[of I] by metis moreover have "|SIGMA i : I. B (f i)| \o |SIGMA j : J. B j|" - using INJ IM card_of_Sigma_mono2 by blast + using INJ IM card_of_Sigma_mono2 by blast ultimately show ?thesis using ordLeq_transitive by blast qed lemma ordLeq_Sigma_mono1: -assumes "\i \ I. p i \o r i" -shows "|SIGMA i : I. Field(p i)| \o |SIGMA i : I. Field(r i)|" -using assms by (auto simp add: card_of_Sigma_mono1) + assumes "\i \ I. p i \o r i" + shows "|SIGMA i : I. Field(p i)| \o |SIGMA i : I. Field(r i)|" + using assms by (auto simp: card_of_Sigma_mono1) lemma ordLeq_Sigma_mono: -assumes "inj_on f I" and "f ` I \ J" and - "\j \ J. p j \o r j" -shows "|SIGMA i : I. Field(p(f i))| \o |SIGMA j : J. Field(r j)|" -using assms card_of_mono2 card_of_Sigma_mono - [of f I J "\ i. Field(p i)" "\ j. Field(r j)"] by metis + assumes "inj_on f I" and "f ` I \ J" and + "\j \ J. p j \o r j" + shows "|SIGMA i : I. Field(p(f i))| \o |SIGMA j : J. Field(r j)|" + using assms card_of_mono2 card_of_Sigma_mono [of f I J "\ i. Field(p i)"] by metis lemma ordIso_Sigma_cong1: -assumes "\i \ I. p i =o r i" -shows "|SIGMA i : I. Field(p i)| =o |SIGMA i : I. Field(r i)|" -using assms by (auto simp add: card_of_Sigma_cong1) + assumes "\i \ I. p i =o r i" + shows "|SIGMA i : I. Field(p i)| =o |SIGMA i : I. Field(r i)|" + using assms by (auto simp: card_of_Sigma_cong1) lemma ordLeq_Sigma_cong: -assumes "bij_betw f I J" and - "\j \ J. p j =o r j" -shows "|SIGMA i : I. Field(p(f i))| =o |SIGMA j : J. Field(r j)|" -using assms card_of_cong card_of_Sigma_cong - [of f I J "\ j. Field(p j)" "\ j. Field(r j)"] by blast + assumes "bij_betw f I J" and + "\j \ J. p j =o r j" + shows "|SIGMA i : I. Field(p(f i))| =o |SIGMA j : J. Field(r j)|" + using assms card_of_cong card_of_Sigma_cong + [of f I J "\ j. Field(p j)" "\ j. Field(r j)"] by blast lemma card_of_UNION_Sigma2: -assumes -"!! i j. \{i,j} <= I; i ~= j\ \ A i Int A j = {}" -shows -"|\i\I. A i| =o |Sigma I A|" + assumes "\i j. \{i,j} <= I; i \ j\ \ A i Int A j = {}" + shows "|\i\I. A i| =o |Sigma I A|" proof- let ?L = "\i\I. A i" let ?R = "Sigma I A" have "|?L| <=o |?R|" using card_of_UNION_Sigma . moreover have "|?R| <=o |?L|" proof- have "inj_on snd ?R" - unfolding inj_on_def using assms by auto + unfolding inj_on_def using assms by auto moreover have "snd ` ?R <= ?L" by auto ultimately show ?thesis using card_of_ordLeq by blast qed @@ -403,102 +353,91 @@ qed corollary Plus_into_Times: -assumes A2: "a1 \ a2 \ {a1,a2} \ A" and - B2: "b1 \ b2 \ {b1,b2} \ B" -shows "\f. inj_on f (A <+> B) \ f ` (A <+> B) \ A \ B" -using assms by (auto simp add: card_of_Plus_Times card_of_ordLeq) + assumes A2: "a1 \ a2 \ {a1,a2} \ A" and B2: "b1 \ b2 \ {b1,b2} \ B" + shows "\f. inj_on f (A <+> B) \ f ` (A <+> B) \ A \ B" + using assms by (auto simp: card_of_Plus_Times card_of_ordLeq) corollary Plus_into_Times_types: -assumes A2: "(a1::'a) \ a2" and B2: "(b1::'b) \ b2" -shows "\(f::'a + 'b \ 'a * 'b). inj f" -using assms Plus_into_Times[of a1 a2 UNIV b1 b2 UNIV] -by auto + assumes A2: "(a1::'a) \ a2" and B2: "(b1::'b) \ b2" + shows "\(f::'a + 'b \ 'a * 'b). inj f" + using assms Plus_into_Times[of a1 a2 UNIV b1 b2 UNIV] + by auto corollary Times_same_infinite_bij_betw: -assumes "\finite A" -shows "\f. bij_betw f (A \ A) A" -using assms by (auto simp add: card_of_ordIso) + assumes "\finite A" + shows "\f. bij_betw f (A \ A) A" + using assms by (auto simp: card_of_ordIso) corollary Times_same_infinite_bij_betw_types: -assumes INF: "\finite(UNIV::'a set)" -shows "\(f::('a * 'a) => 'a). bij f" -using assms Times_same_infinite_bij_betw[of "UNIV::'a set"] -by auto + assumes INF: "\finite(UNIV::'a set)" + shows "\(f::('a * 'a) => 'a). bij f" + using assms Times_same_infinite_bij_betw[of "UNIV::'a set"] + by auto corollary Times_infinite_bij_betw: -assumes INF: "\finite A" and NE: "B \ {}" and INJ: "inj_on g B \ g ` B \ A" -shows "(\f. bij_betw f (A \ B) A) \ (\h. bij_betw h (B \ A) A)" + assumes INF: "\finite A" and NE: "B \ {}" and INJ: "inj_on g B \ g ` B \ A" + shows "(\f. bij_betw f (A \ B) A) \ (\h. bij_betw h (B \ A) A)" proof- have "|B| \o |A|" using INJ card_of_ordLeq by blast thus ?thesis using INF NE - by (auto simp add: card_of_ordIso card_of_Times_infinite) + by (auto simp: card_of_ordIso card_of_Times_infinite) qed corollary Times_infinite_bij_betw_types: -assumes INF: "\finite(UNIV::'a set)" and - BIJ: "inj(g::'b \ 'a)" -shows "(\(f::('b * 'a) => 'a). bij f) \ (\(h::('a * 'b) => 'a). bij h)" -using assms Times_infinite_bij_betw[of "UNIV::'a set" "UNIV::'b set" g] -by auto + assumes "\finite(UNIV::'a set)" and "inj(g::'b \ 'a)" + shows "(\(f::('b * 'a) => 'a). bij f) \ (\(h::('a * 'b) => 'a). bij h)" + using assms Times_infinite_bij_betw[of "UNIV::'a set" "UNIV::'b set" g] + by auto lemma card_of_Times_ordLeq_infinite: -"\\finite C; |A| \o |C|; |B| \o |C|\ - \ |A \ B| \o |C|" -by(simp add: card_of_Sigma_ordLeq_infinite) + "\\finite C; |A| \o |C|; |B| \o |C|\ \ |A \ B| \o |C|" + by(simp add: card_of_Sigma_ordLeq_infinite) corollary Plus_infinite_bij_betw: -assumes INF: "\finite A" and INJ: "inj_on g B \ g ` B \ A" -shows "(\f. bij_betw f (A <+> B) A) \ (\h. bij_betw h (B <+> A) A)" + assumes INF: "\finite A" and INJ: "inj_on g B \ g ` B \ A" + shows "(\f. bij_betw f (A <+> B) A) \ (\h. bij_betw h (B <+> A) A)" proof- have "|B| \o |A|" using INJ card_of_ordLeq by blast thus ?thesis using INF - by (auto simp add: card_of_ordIso) + by (auto simp: card_of_ordIso) qed corollary Plus_infinite_bij_betw_types: -assumes INF: "\finite(UNIV::'a set)" and - BIJ: "inj(g::'b \ 'a)" -shows "(\(f::('b + 'a) => 'a). bij f) \ (\(h::('a + 'b) => 'a). bij h)" -using assms Plus_infinite_bij_betw[of "UNIV::'a set" g "UNIV::'b set"] -by auto + assumes "\finite(UNIV::'a set)" and "inj(g::'b \ 'a)" + shows "(\(f::('b + 'a) => 'a). bij f) \ (\(h::('a + 'b) => 'a). bij h)" + using assms Plus_infinite_bij_betw[of "UNIV::'a set" g "UNIV::'b set"] + by auto lemma card_of_Un_infinite: -assumes INF: "\finite A" and LEQ: "|B| \o |A|" -shows "|A \ B| =o |A| \ |B \ A| =o |A|" -proof- - have "|A \ B| \o |A <+> B|" by (rule card_of_Un_Plus_ordLeq) - moreover have "|A <+> B| =o |A|" - using assms by (metis card_of_Plus_infinite) - ultimately have "|A \ B| \o |A|" using ordLeq_ordIso_trans by blast - hence "|A \ B| =o |A|" using card_of_Un1 ordIso_iff_ordLeq by blast - thus ?thesis using Un_commute[of B A] by auto -qed + assumes INF: "\finite A" and LEQ: "|B| \o |A|" + shows "|A \ B| =o |A| \ |B \ A| =o |A|" + by (simp add: INF LEQ card_of_Un_ordLeq_infinite_Field ordIso_iff_ordLeq) lemma card_of_Un_infinite_simps[simp]: -"\\finite A; |B| \o |A| \ \ |A \ B| =o |A|" -"\\finite A; |B| \o |A| \ \ |B \ A| =o |A|" -using card_of_Un_infinite by auto + "\\finite A; |B| \o |A| \ \ |A \ B| =o |A|" + "\\finite A; |B| \o |A| \ \ |B \ A| =o |A|" + using card_of_Un_infinite by auto lemma card_of_Un_diff_infinite: -assumes INF: "\finite A" and LESS: "|B| finite A" and LESS: "|B| B| =o |A|" - using assms ordLeq_iff_ordLess_or_ordIso card_of_Un_infinite by blast + using assms ordLeq_iff_ordLess_or_ordIso card_of_Un_infinite by blast moreover have "C \ B = A \ B" unfolding C_def by auto ultimately have 1: "|C \ B| =o |A|" by auto - (* *) + (* *) {assume *: "|C| \o |B|" - moreover - {assume **: "finite B" - hence "finite C" - using card_of_ordLeq_finite * by blast - hence False using ** INF card_of_ordIso_finite 1 by blast - } - hence "\finite B" by auto - ultimately have False - using card_of_Un_infinite 1 ordIso_equivalence(1,3) LESS not_ordLess_ordIso by metis + moreover + {assume **: "finite B" + hence "finite C" + using card_of_ordLeq_finite * by blast + hence False using ** INF card_of_ordIso_finite 1 by blast + } + hence "\finite B" by auto + ultimately have False + using card_of_Un_infinite 1 ordIso_equivalence(1,3) LESS not_ordLess_ordIso by metis } hence 2: "|B| \o |C|" using card_of_Well_order ordLeq_total by blast {assume *: "finite C" @@ -507,155 +446,121 @@ } hence "\finite C" by auto hence "|C| =o |A|" - using card_of_Un_infinite 1 2 ordIso_equivalence(1,3) by metis + using card_of_Un_infinite 1 2 ordIso_equivalence(1,3) by metis thus ?thesis unfolding C_def . qed corollary Card_order_Un_infinite: -assumes INF: "\finite(Field r)" and CARD: "Card_order r" and - LEQ: "p \o r" -shows "| (Field r) \ (Field p) | =o r \ | (Field p) \ (Field r) | =o r" + assumes INF: "\finite(Field r)" and CARD: "Card_order r" and + LEQ: "p \o r" + shows "| (Field r) \ (Field p) | =o r \ | (Field p) \ (Field r) | =o r" proof- have "| Field r \ Field p | =o | Field r | \ | Field p \ Field r | =o | Field r |" - using assms by (auto simp add: card_of_Un_infinite) + using assms by (auto simp: card_of_Un_infinite) thus ?thesis - using assms card_of_Field_ordIso[of r] - ordIso_transitive[of "|Field r \ Field p|"] - ordIso_transitive[of _ "|Field r|"] by blast + using assms card_of_Field_ordIso[of r] + ordIso_transitive[of "|Field r \ Field p|"] + ordIso_transitive[of _ "|Field r|"] by blast qed corollary subset_ordLeq_diff_infinite: -assumes INF: "\finite B" and SUB: "A \ B" and LESS: "|A| finite (B - A)" -using assms card_of_Un_diff_infinite card_of_ordIso_finite by blast + assumes INF: "\finite B" and SUB: "A \ B" and LESS: "|A| finite (B - A)" + using assms card_of_Un_diff_infinite card_of_ordIso_finite by blast lemma card_of_Times_ordLess_infinite[simp]: -assumes INF: "\finite C" and - LESS1: "|A| B| finite C" and + LESS1: "|A| B| B = {}") assume Case1: "A = {} \ B = {}" hence "A \ B = {}" by blast moreover have "C \ {}" using - LESS1 card_of_empty5 by blast - ultimately show ?thesis by(auto simp add: card_of_empty4) + LESS1 card_of_empty5 by blast + ultimately show ?thesis by(auto simp: card_of_empty4) next assume Case2: "\(A = {} \ B = {})" {assume *: "|C| \o |A \ B|" - hence "\finite (A \ B)" using INF card_of_ordLeq_finite by blast - hence 1: "\finite A \ \finite B" using finite_cartesian_product by blast - {assume Case21: "|A| \o |B|" - hence "\finite B" using 1 card_of_ordLeq_finite by blast - hence "|A \ B| =o |B|" using Case2 Case21 - by (auto simp add: card_of_Times_infinite) - hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast - } - moreover - {assume Case22: "|B| \o |A|" - hence "\finite A" using 1 card_of_ordLeq_finite by blast - hence "|A \ B| =o |A|" using Case2 Case22 - by (auto simp add: card_of_Times_infinite) - hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast - } - ultimately have False using ordLeq_total card_of_Well_order[of A] - card_of_Well_order[of B] by blast + hence "\finite (A \ B)" using INF card_of_ordLeq_finite by blast + hence 1: "\finite A \ \finite B" using finite_cartesian_product by blast + {assume Case21: "|A| \o |B|" + hence "\finite B" using 1 card_of_ordLeq_finite by blast + hence "|A \ B| =o |B|" using Case2 Case21 + by (auto simp: card_of_Times_infinite) + hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast + } + moreover + {assume Case22: "|B| \o |A|" + hence "\finite A" using 1 card_of_ordLeq_finite by blast + hence "|A \ B| =o |A|" using Case2 Case22 + by (auto simp: card_of_Times_infinite) + hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast + } + ultimately have False using ordLeq_total card_of_Well_order[of A] + card_of_Well_order[of B] by blast } thus ?thesis using ordLess_or_ordLeq[of "|A \ B|" "|C|"] - card_of_Well_order[of "A \ B"] card_of_Well_order[of "C"] by auto + card_of_Well_order[of "A \ B"] card_of_Well_order[of "C"] by auto qed lemma card_of_Times_ordLess_infinite_Field[simp]: -assumes INF: "\finite (Field r)" and r: "Card_order r" and - LESS1: "|A| B| finite (Field r)" and r: "Card_order r" and + LESS1: "|A| B| |?C| =o r" using r card_of_Field_ordIso - ordIso_symmetric by blast + ordIso_symmetric by blast hence "|A| B| finite C" and - LESS1: "|A| B| finite (Field r)" and r: "Card_order r" and - LESS1: "|A| |?C| =o r" using r card_of_Field_ordIso - ordIso_symmetric by blast - hence "|A| o s" and "finite (Field s)" -shows "finite (Field r)" -by (metis assms card_of_mono2 card_of_ordLeq_infinite) + assumes "r \o s" and "finite (Field s)" + shows "finite (Field r)" + by (metis assms card_of_mono2 card_of_ordLeq_infinite) lemma ordIso_finite_Field: -assumes "r =o s" -shows "finite (Field r) \ finite (Field s)" -by (metis assms ordIso_iff_ordLeq ordLeq_finite_Field) + assumes "r =o s" + shows "finite (Field r) \ finite (Field s)" + by (metis assms ordIso_iff_ordLeq ordLeq_finite_Field) subsection \Cardinals versus set operations involving infinite sets\ lemma finite_iff_cardOf_nat: -"finite A = ( |A| finite B" -shows "|A| finite B" + shows "|A| finite A" -shows "|insert a A| =o |A|" + assumes "\finite A" + shows "|insert a A| =o |A|" proof- have iA: "insert a A = A \ {a}" by simp show ?thesis - using infinite_imp_bij_betw2[OF assms] unfolding iA - by (metis bij_betw_inv card_of_ordIso) + using infinite_imp_bij_betw2[OF assms] unfolding iA + by (metis bij_betw_inv card_of_ordIso) qed lemma card_of_Un_singl_ordLess_infinite1: -assumes "\finite B" and "|A| finite B" and "|A| finite B" -shows "( |A| finite B" + shows "|A| |{a} Un A| Cardinals versus lists\ @@ -664,48 +569,39 @@ proofs of facts concerning the cardinality of \List\ :\ definition nlists :: "'a set \ nat \ 'a list set" -where "nlists A n \ {l. set l \ A \ length l = n}" - -lemma lists_def2: "lists A = {l. set l \ A}" -using in_listsI by blast + where "nlists A n \ {l. set l \ A \ length l = n}" lemma lists_UNION_nlists: "lists A = (\n. nlists A n)" -unfolding lists_def2 nlists_def by blast + unfolding lists_eq_set nlists_def by blast lemma card_of_lists: "|A| \o |lists A|" proof- let ?h = "\ a. [a]" have "inj_on ?h A \ ?h ` A \ lists A" - unfolding inj_on_def lists_def2 by auto + unfolding inj_on_def lists_eq_set by auto thus ?thesis by (metis card_of_ordLeq) qed lemma nlists_0: "nlists A 0 = {[]}" -unfolding nlists_def by auto + unfolding nlists_def by auto lemma nlists_not_empty: -assumes "A \ {}" -shows "nlists A n \ {}" -proof(induct n, simp add: nlists_0) - fix n assume "nlists A n \ {}" + assumes "A \ {}" + shows "nlists A n \ {}" +proof (induction n) + case (Suc n) then obtain a and l where "a \ A \ l \ nlists A n" using assms by auto hence "a # l \ nlists A (Suc n)" unfolding nlists_def by auto - thus "nlists A (Suc n) \ {}" by auto -qed - -lemma Nil_in_lists: "[] \ lists A" -unfolding lists_def2 by auto - -lemma lists_not_empty: "lists A \ {}" -using Nil_in_lists by blast + then show ?case by auto +qed (simp add: nlists_0) lemma card_of_nlists_Succ: "|nlists A (Suc n)| =o |A \ (nlists A n)|" proof- let ?B = "A \ (nlists A n)" let ?h = "\(a,l). a # l" have "inj_on ?h ?B \ ?h ` ?B \ nlists A (Suc n)" - unfolding inj_on_def nlists_def by auto + unfolding inj_on_def nlists_def by auto moreover have "nlists A (Suc n) \ ?h ` ?B" - proof(auto) + proof clarify fix l assume "l \ nlists A (Suc n)" hence 1: "length l = Suc n \ set l \ A" unfolding nlists_def by auto then obtain a and l' where 2: "l = a # l'" by (auto simp: length_Suc_conv) @@ -713,131 +609,113 @@ thus "l \ ?h ` ?B" using 2 unfolding nlists_def by auto qed ultimately have "bij_betw ?h ?B (nlists A (Suc n))" - unfolding bij_betw_def by auto + unfolding bij_betw_def by auto thus ?thesis using card_of_ordIso ordIso_symmetric by blast qed lemma card_of_nlists_infinite: -assumes "\finite A" -shows "|nlists A n| \o |A|" -proof(induct n) + assumes "\finite A" + shows "|nlists A n| \o |A|" +proof(induction n) + case 0 have "A \ {}" using assms by auto - thus "|nlists A 0| \o |A|" by (simp add: nlists_0) + then show ?case + by (simp add: nlists_0) next - fix n assume IH: "|nlists A n| \o |A|" + case (Suc n) have "|nlists A (Suc n)| =o |A \ (nlists A n)|" - using card_of_nlists_Succ by blast + using card_of_nlists_Succ by blast moreover - {have "nlists A n \ {}" using assms nlists_not_empty[of A] by blast - hence "|A \ (nlists A n)| =o |A|" - using assms IH by (auto simp add: card_of_Times_infinite) - } - ultimately show "|nlists A (Suc n)| \o |A|" - using ordIso_transitive ordIso_iff_ordLeq by blast + have "nlists A n \ {}" using assms nlists_not_empty[of A] by blast + hence "|A \ (nlists A n)| =o |A|" + using Suc assms by auto + ultimately show ?case + using ordIso_transitive ordIso_iff_ordLeq by blast qed + lemma Card_order_lists: "Card_order r \ r \o |lists(Field r) |" -using card_of_lists card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast + using card_of_lists card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast lemma Union_set_lists: "\(set ` (lists A)) = A" - unfolding lists_def2 -proof(auto) - fix a assume "a \ A" +proof - + { fix a assume "a \ A" hence "set [a] \ A \ a \ set [a]" by auto - thus "\l. set l \ A \ a \ set l" by blast + hence "\l. set l \ A \ a \ set l" by blast } + then show ?thesis by force qed lemma inj_on_map_lists: -assumes "inj_on f A" -shows "inj_on (map f) (lists A)" -using assms Union_set_lists[of A] inj_on_mapI[of f "lists A"] by auto + assumes "inj_on f A" + shows "inj_on (map f) (lists A)" + using assms Union_set_lists[of A] inj_on_mapI[of f "lists A"] by auto lemma map_lists_mono: -assumes "f ` A \ B" -shows "(map f) ` (lists A) \ lists B" -using assms unfolding lists_def2 by (auto, blast) (* lethal combination of methods :) *) + assumes "f ` A \ B" + shows "(map f) ` (lists A) \ lists B" + using assms by force lemma map_lists_surjective: -assumes "f ` A = B" -shows "(map f) ` (lists A) = lists B" -using assms unfolding lists_def2 -proof (auto, blast) - fix l' assume *: "set l' \ f ` A" - have "set l' \ f ` A \ l' \ map f ` {l. set l \ A}" - proof(induct l', auto) - fix l a - assume "a \ A" and "set l \ A" and - IH: "f ` (set l) \ f ` A" - hence "set (a # l) \ A" by auto - hence "map f (a # l) \ map f ` {l. set l \ A}" by blast - thus "f a # map f l \ map f ` {l. set l \ A}" by auto - qed - thus "l' \ map f ` {l. set l \ A}" using * by auto -qed + assumes "f ` A = B" + shows "(map f) ` (lists A) = lists B" + by (metis assms lists_image) lemma bij_betw_map_lists: -assumes "bij_betw f A B" -shows "bij_betw (map f) (lists A) (lists B)" -using assms unfolding bij_betw_def -by(auto simp add: inj_on_map_lists map_lists_surjective) + assumes "bij_betw f A B" + shows "bij_betw (map f) (lists A) (lists B)" + using assms unfolding bij_betw_def + by(auto simp: inj_on_map_lists map_lists_surjective) lemma card_of_lists_mono[simp]: -assumes "|A| \o |B|" -shows "|lists A| \o |lists B|" + assumes "|A| \o |B|" + shows "|lists A| \o |lists B|" proof- obtain f where "inj_on f A \ f ` A \ B" - using assms card_of_ordLeq[of A B] by auto + using assms card_of_ordLeq[of A B] by auto hence "inj_on (map f) (lists A) \ (map f) ` (lists A) \ (lists B)" - by (auto simp add: inj_on_map_lists map_lists_mono) + by (auto simp: inj_on_map_lists map_lists_mono) thus ?thesis using card_of_ordLeq[of "lists A"] by metis qed lemma ordIso_lists_mono: -assumes "r \o r'" -shows "|lists(Field r)| \o |lists(Field r')|" -using assms card_of_mono2 card_of_lists_mono by blast + assumes "r \o r'" + shows "|lists(Field r)| \o |lists(Field r')|" + using assms card_of_mono2 card_of_lists_mono by blast lemma card_of_lists_cong[simp]: -assumes "|A| =o |B|" -shows "|lists A| =o |lists B|" -proof- - obtain f where "bij_betw f A B" - using assms card_of_ordIso[of A B] by auto - hence "bij_betw (map f) (lists A) (lists B)" - by (auto simp add: bij_betw_map_lists) - thus ?thesis using card_of_ordIso[of "lists A"] by auto -qed + assumes "|A| =o |B|" + shows "|lists A| =o |lists B|" + by (meson assms card_of_lists_mono ordIso_iff_ordLeq) lemma card_of_lists_infinite[simp]: -assumes "\finite A" -shows "|lists A| =o |A|" + assumes "\finite A" + shows "|lists A| =o |A|" proof- have "|lists A| \o |A|" unfolding lists_UNION_nlists - by (rule card_of_UNION_ordLeq_infinite[OF assms _ ballI[OF card_of_nlists_infinite[OF assms]]]) - (metis infinite_iff_card_of_nat assms) + by (rule card_of_UNION_ordLeq_infinite[OF assms _ ballI[OF card_of_nlists_infinite[OF assms]]]) + (metis infinite_iff_card_of_nat assms) thus ?thesis using card_of_lists ordIso_iff_ordLeq by blast qed lemma Card_order_lists_infinite: -assumes "Card_order r" and "\finite(Field r)" -shows "|lists(Field r)| =o r" -using assms card_of_lists_infinite card_of_Field_ordIso ordIso_transitive by blast + assumes "Card_order r" and "\finite(Field r)" + shows "|lists(Field r)| =o r" + using assms card_of_lists_infinite card_of_Field_ordIso ordIso_transitive by blast lemma ordIso_lists_cong: -assumes "r =o r'" -shows "|lists(Field r)| =o |lists(Field r')|" -using assms card_of_cong card_of_lists_cong by blast + assumes "r =o r'" + shows "|lists(Field r)| =o |lists(Field r')|" + using assms card_of_cong card_of_lists_cong by blast corollary lists_infinite_bij_betw: -assumes "\finite A" -shows "\f. bij_betw f (lists A) A" -using assms card_of_lists_infinite card_of_ordIso by blast + assumes "\finite A" + shows "\f. bij_betw f (lists A) A" + using assms card_of_lists_infinite card_of_ordIso by blast corollary lists_infinite_bij_betw_types: -assumes "\finite(UNIV :: 'a set)" -shows "\(f::'a list \ 'a). bij f" -using assms assms lists_infinite_bij_betw[of "UNIV::'a set"] -using lists_UNIV by auto + assumes "\finite(UNIV :: 'a set)" + shows "\(f::'a list \ 'a). bij f" + using assms lists_infinite_bij_betw by fastforce subsection \Cardinals versus the finite powerset operator\ @@ -846,82 +724,72 @@ proof- let ?h = "\ a. {a}" have "inj_on ?h A \ ?h ` A \ Fpow A" - unfolding inj_on_def Fpow_def by auto + unfolding inj_on_def Fpow_def by auto thus ?thesis using card_of_ordLeq by metis qed lemma Card_order_Fpow: "Card_order r \ r \o |Fpow(Field r) |" -using card_of_Fpow card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast + using card_of_Fpow card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast lemma image_Fpow_surjective: -assumes "f ` A = B" -shows "(image f) ` (Fpow A) = Fpow B" -using assms proof(unfold Fpow_def, auto) - fix Y assume *: "Y \ f ` A" and **: "finite Y" - hence "\b \ Y. \a. a \ A \ f a = b" by auto - with bchoice[of Y "\b a. a \ A \ f a = b"] - obtain g where 1: "\b \ Y. g b \ A \ f(g b) = b" by blast - obtain X where X_def: "X = g ` Y" by blast - have "f ` X = Y \ X \ A \ finite X" - by(unfold X_def, force simp add: ** 1) - thus "Y \ (image f) ` {X. X \ A \ finite X}" by auto + assumes "f ` A = B" + shows "(image f) ` (Fpow A) = Fpow B" +proof - + have "\C. \C \ f ` A; finite C\ \ C \ (`) f ` {X. X \ A \ finite X}" + by (simp add: finite_subset_image image_iff) + then show ?thesis + using assms by (force simp add: Fpow_def) qed lemma bij_betw_image_Fpow: -assumes "bij_betw f A B" -shows "bij_betw (image f) (Fpow A) (Fpow B)" -using assms unfolding bij_betw_def -by (auto simp add: inj_on_image_Fpow image_Fpow_surjective) + assumes "bij_betw f A B" + shows "bij_betw (image f) (Fpow A) (Fpow B)" + using assms unfolding bij_betw_def + by (auto simp: inj_on_image_Fpow image_Fpow_surjective) lemma card_of_Fpow_mono[simp]: -assumes "|A| \o |B|" -shows "|Fpow A| \o |Fpow B|" + assumes "|A| \o |B|" + shows "|Fpow A| \o |Fpow B|" proof- obtain f where "inj_on f A \ f ` A \ B" - using assms card_of_ordLeq[of A B] by auto + using assms card_of_ordLeq[of A B] by auto hence "inj_on (image f) (Fpow A) \ (image f) ` (Fpow A) \ (Fpow B)" - by (auto simp add: inj_on_image_Fpow image_Fpow_mono) + by (auto simp: inj_on_image_Fpow image_Fpow_mono) thus ?thesis using card_of_ordLeq[of "Fpow A"] by auto qed lemma ordIso_Fpow_mono: -assumes "r \o r'" -shows "|Fpow(Field r)| \o |Fpow(Field r')|" -using assms card_of_mono2 card_of_Fpow_mono by blast + assumes "r \o r'" + shows "|Fpow(Field r)| \o |Fpow(Field r')|" + using assms card_of_mono2 card_of_Fpow_mono by blast lemma card_of_Fpow_cong[simp]: -assumes "|A| =o |B|" -shows "|Fpow A| =o |Fpow B|" -proof- - obtain f where "bij_betw f A B" - using assms card_of_ordIso[of A B] by auto - hence "bij_betw (image f) (Fpow A) (Fpow B)" - by (auto simp add: bij_betw_image_Fpow) - thus ?thesis using card_of_ordIso[of "Fpow A"] by auto -qed + assumes "|A| =o |B|" + shows "|Fpow A| =o |Fpow B|" + by (meson assms card_of_Fpow_mono ordIso_iff_ordLeq) lemma ordIso_Fpow_cong: -assumes "r =o r'" -shows "|Fpow(Field r)| =o |Fpow(Field r')|" -using assms card_of_cong card_of_Fpow_cong by blast + assumes "r =o r'" + shows "|Fpow(Field r)| =o |Fpow(Field r')|" + using assms card_of_cong card_of_Fpow_cong by blast lemma card_of_Fpow_lists: "|Fpow A| \o |lists A|" proof- have "set ` (lists A) = Fpow A" - unfolding lists_def2 Fpow_def using finite_list finite_set by blast + unfolding lists_eq_set Fpow_def using finite_list finite_set by blast thus ?thesis using card_of_ordLeq2[of "Fpow A"] Fpow_not_empty[of A] by blast qed lemma card_of_Fpow_infinite[simp]: -assumes "\finite A" -shows "|Fpow A| =o |A|" -using assms card_of_Fpow_lists card_of_lists_infinite card_of_Fpow - ordLeq_ordIso_trans ordIso_iff_ordLeq by blast + assumes "\finite A" + shows "|Fpow A| =o |A|" + using assms card_of_Fpow_lists card_of_lists_infinite card_of_Fpow + ordLeq_ordIso_trans ordIso_iff_ordLeq by blast corollary Fpow_infinite_bij_betw: -assumes "\finite A" -shows "\f. bij_betw f (Fpow A) A" -using assms card_of_Fpow_infinite card_of_ordIso by blast + assumes "\finite A" + shows "\f. bij_betw f (Fpow A) A" + using assms card_of_Fpow_infinite card_of_ordIso by blast subsection \The cardinal $\omega$ and the finite cardinals\ @@ -929,108 +797,120 @@ subsubsection \First as well-orders\ lemma Field_natLess: "Field natLess = (UNIV::nat set)" -by(unfold Field_def natLess_def, auto) + by (auto simp: Field_def natLess_def) lemma natLeq_well_order_on: "well_order_on UNIV natLeq" -using natLeq_Well_order Field_natLeq by auto + using natLeq_Well_order Field_natLeq by auto lemma natLeq_wo_rel: "wo_rel natLeq" -unfolding wo_rel_def using natLeq_Well_order . + unfolding wo_rel_def using natLeq_Well_order . lemma natLeq_ofilter_less: "ofilter natLeq {0 ..< n}" -by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def, - simp add: Field_natLeq, unfold under_def natLeq_def, auto) +proof - + have "\t Field natLeq" + by (simp add: Field_natLeq) + moreover have "\xt. (t, x) \ natLeq \ t < n" + by (simp add: natLeq_def) + ultimately show ?thesis + by (auto simp: natLeq_wo_rel wo_rel.ofilter_def under_def) +qed lemma natLeq_ofilter_leq: "ofilter natLeq {0 .. n}" -by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def, - simp add: Field_natLeq, unfold under_def natLeq_def, auto) + by (metis (no_types) atLeastLessThanSuc_atLeastAtMost natLeq_ofilter_less) lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV" -using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto + using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto lemma closed_nat_set_iff: -assumes "\(m::nat) n. n \ A \ m \ n \ m \ A" -shows "A = UNIV \ (\n. A = {0 ..< n})" + assumes "\(m::nat) n. n \ A \ m \ n \ m \ A" + shows "A = UNIV \ (\n. A = {0 ..< n})" proof- {assume "A \ UNIV" hence "\n. n \ A" by blast - moreover obtain n where n_def: "n = (LEAST n. n \ A)" by blast - ultimately have 1: "n \ A \ (\m. m < n \ m \ A)" - using LeastI_ex[of "\ n. n \ A"] n_def Least_le[of "\ n. n \ A"] by fastforce - have "A = {0 ..< n}" - proof(auto simp add: 1) - fix m assume *: "m \ A" - {assume "n \ m" with assms * have "n \ A" by blast - hence False using 1 by auto - } - thus "m < n" by fastforce - qed - hence "\n. A = {0 ..< n}" by blast + moreover obtain n where n_def: "n = (LEAST n. n \ A)" by blast + ultimately have 1: "n \ A \ (\m. m < n \ m \ A)" + using LeastI_ex[of "\ n. n \ A"] n_def Least_le[of "\ n. n \ A"] by fastforce + then have "A = {0 ..< n}" + proof(auto simp: 1) + fix m assume *: "m \ A" + {assume "n \ m" with assms * have "n \ A" by blast + hence False using 1 by auto + } + thus "m < n" by fastforce + qed + hence "\n. A = {0 ..< n}" by blast } thus ?thesis by blast qed lemma natLeq_ofilter_iff: -"ofilter natLeq A = (A = UNIV \ (\n. A = {0 ..< n}))" + "ofilter natLeq A = (A = UNIV \ (\n. A = {0 ..< n}))" proof(rule iffI) assume "ofilter natLeq A" hence "\m n. n \ A \ m \ n \ m \ A" using natLeq_wo_rel - by(auto simp add: natLeq_def wo_rel.ofilter_def under_def) + by(auto simp: natLeq_def wo_rel.ofilter_def under_def) thus "A = UNIV \ (\n. A = {0 ..< n})" using closed_nat_set_iff by blast next assume "A = UNIV \ (\n. A = {0 ..< n})" thus "ofilter natLeq A" - by(auto simp add: natLeq_ofilter_less natLeq_UNIV_ofilter) + by(auto simp: natLeq_ofilter_less natLeq_UNIV_ofilter) qed lemma natLeq_under_leq: "under natLeq n = {0 .. n}" -unfolding under_def natLeq_def by auto + unfolding under_def natLeq_def by auto lemma natLeq_on_ofilter_less_eq: -"n \ m \ wo_rel.ofilter (natLeq_on m) {0 ..< n}" -apply (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def) -apply (simp add: Field_natLeq_on) -by (auto simp add: under_def) + "n \ m \ wo_rel.ofilter (natLeq_on m) {0 ..< n}" + by (auto simp: natLeq_on_wo_rel wo_rel.ofilter_def Field_natLeq_on under_def) lemma natLeq_on_ofilter_iff: -"wo_rel.ofilter (natLeq_on m) A = (\n \ m. A = {0 ..< n})" + "wo_rel.ofilter (natLeq_on m) A = (\n \ m. A = {0 ..< n})" proof(rule iffI) assume *: "wo_rel.ofilter (natLeq_on m) A" hence 1: "A \ {0..n1 n2. n2 \ A \ n1 \ n2 \ n1 \ A" - using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def under_def) + using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def under_def) hence "A = UNIV \ (\n. A = {0 ..< n})" using closed_nat_set_iff by blast thus "\n \ m. A = {0 ..< n}" using 1 atLeastLessThan_less_eq by blast next assume "(\n\m. A = {0 ..< n})" - thus "wo_rel.ofilter (natLeq_on m) A" by (auto simp add: natLeq_on_ofilter_less_eq) + thus "wo_rel.ofilter (natLeq_on m) A" by (auto simp: natLeq_on_ofilter_less_eq) qed corollary natLeq_on_ofilter: -"ofilter(natLeq_on n) {0 ..< n}" -by (auto simp add: natLeq_on_ofilter_less_eq) + "ofilter(natLeq_on n) {0 ..< n}" + by (auto simp: natLeq_on_ofilter_less_eq) lemma natLeq_on_ofilter_less: -"n < m \ ofilter (natLeq_on m) {0 .. n}" -by(auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def, - simp add: Field_natLeq_on, unfold under_def, auto) + assumes "n < m" shows "ofilter (natLeq_on m) {0 .. n}" +proof - + have "Suc n \ m" + using assms by simp + then show ?thesis + using natLeq_on_ofilter_iff by auto +qed lemma natLeq_on_ordLess_natLeq: "natLeq_on n n. well_order_on {na. na < n} (natLeq_on n)" + using Field_natLeq_on natLeq_on_Well_order by presburger + ultimately show ?thesis + by (simp add: Field_natLeq Field_natLeq_on finite_ordLess_infinite) +qed lemma natLeq_on_injective: -"natLeq_on m = natLeq_on n \ m = n" -using Field_natLeq_on[of m] Field_natLeq_on[of n] - atLeastLessThan_injective[of m n, unfolded atLeastLessThan_def] by blast + "natLeq_on m = natLeq_on n \ m = n" + using Field_natLeq_on[of m] Field_natLeq_on[of n] + atLeastLessThan_injective[of m n, unfolded atLeastLessThan_def] by blast lemma natLeq_on_injective_ordIso: -"(natLeq_on m =o natLeq_on n) = (m = n)" -proof(auto simp add: natLeq_on_Well_order ordIso_reflexive) + "(natLeq_on m =o natLeq_on n) = (m = n)" +proof(auto simp: natLeq_on_Well_order ordIso_reflexive) assume "natLeq_on m =o natLeq_on n" then obtain f where "bij_betw f {x. xThen as cardinals\ lemma ordIso_natLeq_infinite1: -"|A| =o natLeq \ \finite A" -using ordIso_symmetric ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast + "|A| =o natLeq \ \finite A" + by (meson finite_iff_ordLess_natLeq not_ordLess_ordIso) lemma ordIso_natLeq_infinite2: -"natLeq =o |A| \ \finite A" -using ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast + "natLeq =o |A| \ \finite A" + using ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast lemma ordIso_natLeq_on_imp_finite: -"|A| =o natLeq_on n \ finite A" -unfolding ordIso_def iso_def[abs_def] -by (auto simp: Field_natLeq_on bij_betw_finite) + "|A| =o natLeq_on n \ finite A" + unfolding ordIso_def iso_def[abs_def] + by (auto simp: Field_natLeq_on bij_betw_finite) lemma natLeq_on_Card_order: "Card_order (natLeq_on n)" -proof(unfold card_order_on_def, - auto simp add: natLeq_on_Well_order, simp add: Field_natLeq_on) - fix r assume "well_order_on {x. x < n} r" - thus "natLeq_on n \o r" - using finite_atLeastLessThan natLeq_on_well_order_on +proof - + { fix r assume "well_order_on {x. x < n} r" + hence "natLeq_on n \o r" + using finite_atLeastLessThan natLeq_on_well_order_on finite_well_order_on_ordIso ordIso_iff_ordLeq by blast + } + then show ?thesis + unfolding card_order_on_def using Field_natLeq_on natLeq_on_Well_order by presburger qed corollary card_of_Field_natLeq_on: -"|Field (natLeq_on n)| =o natLeq_on n" -using Field_natLeq_on natLeq_on_Card_order - Card_order_iff_ordIso_card_of[of "natLeq_on n"] - ordIso_symmetric[of "natLeq_on n"] by blast + "|Field (natLeq_on n)| =o natLeq_on n" + using Field_natLeq_on natLeq_on_Card_order + Card_order_iff_ordIso_card_of[of "natLeq_on n"] + ordIso_symmetric[of "natLeq_on n"] by blast corollary card_of_less: -"|{0 ..< n}| =o natLeq_on n" -using Field_natLeq_on card_of_Field_natLeq_on -unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by auto + "|{0 ..< n}| =o natLeq_on n" + using Field_natLeq_on card_of_Field_natLeq_on + unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by auto lemma natLeq_on_ordLeq_less_eq: -"((natLeq_on m) \o (natLeq_on n)) = (m \ n)" + "((natLeq_on m) \o (natLeq_on n)) = (m \ n)" proof assume "natLeq_on m \o natLeq_on n" then obtain f where "inj_on f {x. x < m} \ f ` {x. x < m} \ {x. x < n}" - unfolding ordLeq_def using - embed_inj_on[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on] - embed_Field Field_natLeq_on by blast + unfolding ordLeq_def using + embed_inj_on[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on] + embed_Field Field_natLeq_on by blast thus "m \ n" using atLeastLessThan_less_eq2 unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast next @@ -1086,141 +968,126 @@ hence "inj_on id {0.. id ` {0.. {0..o |{0..o natLeq_on n" - using card_of_less ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast + using card_of_less ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast qed lemma natLeq_on_ordLeq_less: -"((natLeq_on m) o natLeq_on n" -shows "finite A" + assumes "|A| \o natLeq_on n" + shows "finite A" proof- have "|A| \o |{0 ..< n}|" - using assms card_of_less ordIso_symmetric ordLeq_ordIso_trans by blast - thus ?thesis by (auto simp add: card_of_ordLeq_finite) + using assms card_of_less ordIso_symmetric ordLeq_ordIso_trans by blast + thus ?thesis by (auto simp: card_of_ordLeq_finite) qed subsubsection \"Backward compatibility" with the numeric cardinal operator for finite sets\ lemma finite_card_of_iff_card2: -assumes FIN: "finite A" and FIN': "finite B" -shows "( |A| \o |B| ) = (card A \ card B)" -using assms card_of_ordLeq[of A B] inj_on_iff_card_le[of A B] by blast + assumes FIN: "finite A" and FIN': "finite B" + shows "( |A| \o |B| ) = (card A \ card B)" + using assms card_of_ordLeq[of A B] inj_on_iff_card_le[of A B] by blast lemma finite_imp_card_of_natLeq_on: -assumes "finite A" -shows "|A| =o natLeq_on (card A)" + assumes "finite A" + shows "|A| =o natLeq_on (card A)" proof- obtain h where "bij_betw h A {0 ..< card A}" - using assms ex_bij_betw_finite_nat by blast + using assms ex_bij_betw_finite_nat by blast thus ?thesis using card_of_ordIso card_of_less ordIso_equivalence by blast qed lemma finite_iff_card_of_natLeq_on: -"finite A = (\n. |A| =o natLeq_on n)" -using finite_imp_card_of_natLeq_on[of A] -by(auto simp add: ordIso_natLeq_on_imp_finite) + "finite A = (\n. |A| =o natLeq_on n)" + using finite_imp_card_of_natLeq_on[of A] + by(auto simp: ordIso_natLeq_on_imp_finite) lemma finite_card_of_iff_card: -assumes FIN: "finite A" and FIN': "finite B" -shows "( |A| =o |B| ) = (card A = card B)" -using assms card_of_ordIso[of A B] bij_betw_iff_card[of A B] by blast + assumes FIN: "finite A" and FIN': "finite B" + shows "( |A| =o |B| ) = (card A = card B)" + using assms card_of_ordIso[of A B] bij_betw_iff_card[of A B] by blast lemma finite_card_of_iff_card3: -assumes FIN: "finite A" and FIN': "finite B" -shows "( |A| o |A| ))" by simp - also have "... = (~ (card B \ card A))" - using assms by(simp add: finite_card_of_iff_card2) - also have "... = (card A < card B)" by auto + also have "\ = (~ (card B \ card A))" + using assms by(simp add: finite_card_of_iff_card2) + also have "\ = (card A < card B)" by auto finally show ?thesis . qed lemma card_Field_natLeq_on: -"card(Field(natLeq_on n)) = n" -using Field_natLeq_on card_atLeastLessThan by auto + "card(Field(natLeq_on n)) = n" + using Field_natLeq_on card_atLeastLessThan by auto subsection \The successor of a cardinal\ lemma embed_implies_ordIso_Restr: -assumes WELL: "Well_order r" and WELL': "Well_order r'" and EMB: "embed r' r f" -shows "r' =o Restr r (f ` (Field r'))" -using assms embed_implies_iso_Restr Well_order_Restr unfolding ordIso_def by blast - -lemma cardSuc_Well_order[simp]: -"Card_order r \ Well_order(cardSuc r)" -using cardSuc_Card_order unfolding card_order_on_def by blast - -lemma Field_cardSuc_not_empty: -assumes "Card_order r" -shows "Field (cardSuc r) \ {}" -proof - assume "Field(cardSuc r) = {}" - hence "|Field(cardSuc r)| \o r" using assms Card_order_empty[of r] by auto - hence "cardSuc r \o r" using assms card_of_Field_ordIso - cardSuc_Card_order ordIso_symmetric ordIso_ordLeq_trans by blast - thus False using cardSuc_greater not_ordLess_ordLeq assms by blast -qed + assumes WELL: "Well_order r" and WELL': "Well_order r'" and EMB: "embed r' r f" + shows "r' =o Restr r (f ` (Field r'))" + using assms embed_implies_iso_Restr Well_order_Restr unfolding ordIso_def by blast lemma cardSuc_mono_ordLess[simp]: -assumes CARD: "Card_order r" and CARD': "Card_order r'" -shows "(cardSuc r Well_order r' \ Well_order(cardSuc r) \ Well_order(cardSuc r')" - using assms by auto + using assms by auto thus ?thesis - using not_ordLeq_iff_ordLess not_ordLeq_iff_ordLess[of r r'] - using cardSuc_mono_ordLeq[of r' r] assms by blast + using not_ordLeq_iff_ordLess not_ordLeq_iff_ordLess[of r r'] + using cardSuc_mono_ordLeq[of r' r] assms by blast qed lemma cardSuc_natLeq_on_Suc: -"cardSuc(natLeq_on n) =o natLeq_on(Suc n)" + "cardSuc(natLeq_on n) =o natLeq_on(Suc n)" proof- obtain r r' p where r_def: "r = natLeq_on n" and - r'_def: "r' = cardSuc(natLeq_on n)" and - p_def: "p = natLeq_on(Suc n)" by blast - (* Preliminary facts: *) + r'_def: "r' = cardSuc(natLeq_on n)" and + p_def: "p = natLeq_on(Suc n)" by blast + (* Preliminary facts: *) have CARD: "Card_order r \ Card_order r' \ Card_order p" unfolding r_def r'_def p_def - using cardSuc_ordLess_ordLeq natLeq_on_Card_order cardSuc_Card_order by blast + using cardSuc_ordLess_ordLeq natLeq_on_Card_order cardSuc_Card_order by blast hence WELL: "Well_order r \ Well_order r' \ Well_order p" - unfolding card_order_on_def by force + unfolding card_order_on_def by force have FIELD: "Field r = {0.. Field p = {0..<(Suc n)}" - unfolding r_def p_def Field_natLeq_on atLeast_0 atLeastLessThan_def lessThan_def by simp + unfolding r_def p_def Field_natLeq_on atLeast_0 atLeastLessThan_def lessThan_def by simp hence FIN: "finite (Field r)" by force have "r o p" using CARD unfolding r_def r'_def p_def - using natLeq_on_ordLeq_less cardSuc_ordLess_ordLeq by blast + using natLeq_on_ordLeq_less cardSuc_ordLess_ordLeq by blast moreover have "p \o r'" proof- {assume "r' Suc n" and 3: "f ` (Field r') = {0.. n" using 2 by force - (* *) - have "bij_betw f (Field r') (f ` (Field r'))" - using WELL embed_inj_on[OF _ 1] unfolding bij_betw_def by blast - moreover have "finite(f ` (Field r'))" using 3 finite_atLeastLessThan[of 0 m] by force - ultimately have 5: "finite (Field r') \ card(Field r') = card (f ` (Field r'))" - using bij_betw_same_card bij_betw_finite by metis - hence "card(Field r') \ card(Field r)" using 3 4 FIELD by force - hence "|Field r'| \o |Field r|" using FIN 5 finite_card_of_iff_card2 by blast - hence False using LESS not_ordLess_ordLeq by auto + then obtain f where 0: "embedS r' p f" unfolding ordLess_def by force + let ?q = "Restr p (f ` Field r')" + have 1: "embed r' p f" using 0 unfolding embedS_def by force + hence 2: "f ` Field r' < {0..<(Suc n)}" + using WELL FIELD 0 by (auto simp: embedS_iff) + have "wo_rel.ofilter p (f ` Field r')" using embed_Field_ofilter 1 WELL by blast + then obtain m where "m \ Suc n" and 3: "f ` (Field r') = {0.. n" using 2 by force + (* *) + have "bij_betw f (Field r') (f ` (Field r'))" + using WELL embed_inj_on[OF _ 1] unfolding bij_betw_def by blast + moreover have "finite(f ` (Field r'))" using 3 finite_atLeastLessThan[of 0 m] by force + ultimately have 5: "finite (Field r') \ card(Field r') = card (f ` (Field r'))" + using bij_betw_same_card bij_betw_finite by metis + hence "card(Field r') \ card(Field r)" using 3 4 FIELD by force + hence "|Field r'| \o |Field r|" using FIN 5 finite_card_of_iff_card2 by blast + hence False using LESS not_ordLess_ordLeq by auto } thus ?thesis using WELL CARD by fastforce qed @@ -1228,129 +1095,104 @@ qed lemma card_of_Plus_ordLeq_infinite[simp]: -assumes C: "\finite C" and A: "|A| \o |C|" and B: "|B| \o |C|" -shows "|A <+> B| \o |C|" -proof- - let ?r = "cardSuc |C|" - have "Card_order ?r \ \finite (Field ?r)" using assms by simp - moreover have "|A| B| finite C" and "|A| \o |C|" and "|B| \o |C|" + shows "|A <+> B| \o |C|" + by (simp add: assms) lemma card_of_Un_ordLeq_infinite[simp]: -assumes C: "\finite C" and A: "|A| \o |C|" and B: "|B| \o |C|" -shows "|A Un B| \o |C|" -using assms card_of_Plus_ordLeq_infinite card_of_Un_Plus_ordLeq -ordLeq_transitive by metis + assumes "\finite C" and "|A| \o |C|" and "|B| \o |C|" + shows "|A Un B| \o |C|" + using assms card_of_Plus_ordLeq_infinite card_of_Un_Plus_ordLeq ordLeq_transitive by metis subsection \Others\ lemma under_mono[simp]: -assumes "Well_order r" and "(i,j) \ r" -shows "under r i \ under r j" -using assms unfolding under_def order_on_defs -trans_def by blast + assumes "Well_order r" and "(i,j) \ r" + shows "under r i \ under r j" + using assms unfolding under_def order_on_defs trans_def by blast lemma underS_under: -assumes "i \ Field r" -shows "underS r i = under r i - {i}" -using assms unfolding underS_def under_def by auto + assumes "i \ Field r" + shows "underS r i = under r i - {i}" + using assms unfolding underS_def under_def by auto lemma relChain_under: -assumes "Well_order r" -shows "relChain r (\ i. under r i)" -using assms unfolding relChain_def by auto + assumes "Well_order r" + shows "relChain r (\ i. under r i)" + using assms unfolding relChain_def by auto lemma card_of_infinite_diff_finite: -assumes "\finite A" and "finite B" -shows "|A - B| =o |A|" -by (metis assms card_of_Un_diff_infinite finite_ordLess_infinite2) + assumes "\finite A" and "finite B" + shows "|A - B| =o |A|" + by (metis assms card_of_Un_diff_infinite finite_ordLess_infinite2) lemma infinite_card_of_diff_singl: -assumes "\finite A" -shows "|A - {a}| =o |A|" -by (metis assms card_of_infinite_diff_finite finite.emptyI finite_insert) + assumes "\finite A" + shows "|A - {a}| =o |A|" + by (metis assms card_of_infinite_diff_finite finite.emptyI finite_insert) lemma card_of_vimage: -assumes "B \ range f" -shows "|B| \o |f -` B|" -apply(rule surj_imp_ordLeq[of _ f]) -using assms by (metis Int_absorb2 image_vimage_eq order_refl) + assumes "B \ range f" + shows "|B| \o |f -` B|" + by (metis Int_absorb2 assms image_vimage_eq order_refl surj_imp_ordLeq) lemma surj_card_of_vimage: -assumes "surj f" -shows "|B| \o |f -` B|" -by (metis assms card_of_vimage subset_UNIV) - -lemma infinite_Pow: -assumes "\ finite A" -shows "\ finite (Pow A)" -proof- - have "|A| \o |Pow A|" by (metis card_of_Pow ordLess_imp_ordLeq) - thus ?thesis by (metis assms finite_Pow_iff) -qed + assumes "surj f" + shows "|B| \o |f -` B|" + by (metis assms card_of_vimage subset_UNIV) (* bounded powerset *) definition Bpow where -"Bpow r A \ {X . X \ A \ |X| \o r}" + "Bpow r A \ {X . X \ A \ |X| \o r}" lemma Bpow_empty[simp]: -assumes "Card_order r" -shows "Bpow r {} = {{}}" -using assms unfolding Bpow_def by auto + assumes "Card_order r" + shows "Bpow r {} = {{}}" + using assms unfolding Bpow_def by auto lemma singl_in_Bpow: -assumes rc: "Card_order r" -and r: "Field r \ {}" and a: "a \ A" -shows "{a} \ Bpow r A" + assumes rc: "Card_order r" + and r: "Field r \ {}" and a: "a \ A" + shows "{a} \ Bpow r A" proof- have "|{a}| \o r" using r rc by auto thus ?thesis unfolding Bpow_def using a by auto qed lemma ordLeq_card_Bpow: -assumes rc: "Card_order r" and r: "Field r \ {}" -shows "|A| \o |Bpow r A|" + assumes rc: "Card_order r" and r: "Field r \ {}" + shows "|A| \o |Bpow r A|" proof- have "inj_on (\ a. {a}) A" unfolding inj_on_def by auto moreover have "(\ a. {a}) ` A \ Bpow r A" - using singl_in_Bpow[OF assms] by auto + using singl_in_Bpow[OF assms] by auto ultimately show ?thesis unfolding card_of_ordLeq[symmetric] by blast qed lemma infinite_Bpow: -assumes rc: "Card_order r" and r: "Field r \ {}" -and A: "\finite A" -shows "\finite (Bpow r A)" -using ordLeq_card_Bpow[OF rc r] -by (metis A card_of_ordLeq_infinite) + assumes rc: "Card_order r" and r: "Field r \ {}" + and A: "\finite A" + shows "\finite (Bpow r A)" + using ordLeq_card_Bpow[OF rc r] + by (metis A card_of_ordLeq_infinite) definition Func_option where - "Func_option A B \ + "Func_option A B \ {f. (\ a. f a \ None \ a \ A) \ (\ a \ A. case f a of Some b \ b \ B |None \ True)}" lemma card_of_Func_option_Func: -"|Func_option A B| =o |Func A B|" + "|Func_option A B| =o |Func A B|" proof (rule ordIso_symmetric, unfold card_of_ordIso[symmetric], intro exI) let ?F = "\ f a. if a \ A then Some (f a) else None" show "bij_betw ?F (Func A B) (Func_option A B)" - unfolding bij_betw_def unfolding inj_on_def proof(intro conjI ballI impI) + unfolding bij_betw_def unfolding inj_on_def proof(intro conjI ballI impI) fix f g assume f: "f \ Func A B" and g: "g \ Func A B" and eq: "?F f = ?F g" show "f = g" proof(rule ext) fix a show "f a = g a" - proof(cases "a \ A") - case True - have "Some (f a) = ?F f a" using True by auto - also have "... = ?F g a" using eq unfolding fun_eq_iff by(rule allE) - also have "... = Some (g a)" using True by auto - finally have "Some (f a) = Some (g a)" . - thus ?thesis by simp - qed(insert f g, unfold Func_def, auto) + by (smt (verit) Func_def eq f g mem_Collect_eq option.inject) qed next show "?F ` Func A B = Func_option A B" @@ -1358,11 +1200,11 @@ fix f assume f: "f \ Func_option A B" define g where [abs_def]: "g a = (case f a of Some b \ b | None \ undefined)" for a have "g \ Func A B" - using f unfolding g_def Func_def Func_option_def by force+ + using f unfolding g_def Func_def Func_option_def by force+ moreover have "f = ?F g" proof(rule ext) fix a show "f a = ?F g a" - using f unfolding Func_option_def g_def by (cases "a \ A") force+ + using f unfolding Func_option_def g_def by (cases "a \ A") force+ qed ultimately show "f \ ?F ` (Func A B)" by blast qed(unfold Func_def Func_option_def, auto) @@ -1371,16 +1213,16 @@ (* partial-function space: *) definition Pfunc where -"Pfunc A B \ + "Pfunc A B \ {f. (\a. f a \ None \ a \ A) \ (\a. case f a of None \ True | Some b \ b \ B)}" lemma Func_Pfunc: -"Func_option A B \ Pfunc A B" -unfolding Func_option_def Pfunc_def by auto + "Func_option A B \ Pfunc A B" + unfolding Func_option_def Pfunc_def by auto lemma Pfunc_Func_option: -"Pfunc A B = (\A' \ Pow A. Func_option A' B)" + "Pfunc A B = (\A' \ Pow A. Func_option A' B)" proof safe fix f assume f: "f \ Pfunc A B" show "f \ (\A'\Pow A. Func_option A' B)" @@ -1395,180 +1237,161 @@ qed lemma card_of_Func_mono: -fixes A1 A2 :: "'a set" and B :: "'b set" -assumes A12: "A1 \ A2" and B: "B \ {}" -shows "|Func A1 B| \o |Func A2 B|" + fixes A1 A2 :: "'a set" and B :: "'b set" + assumes A12: "A1 \ A2" and B: "B \ {}" + shows "|Func A1 B| \o |Func A2 B|" proof- obtain bb where bb: "bb \ B" using B by auto define F where [abs_def]: "F f1 a = (if a \ A2 then (if a \ A1 then f1 a else bb) else undefined)" for f1 :: "'a \ 'b" and a - show ?thesis unfolding card_of_ordLeq[symmetric] proof(intro exI[of _ F] conjI) - show "inj_on F (Func A1 B)" unfolding inj_on_def proof safe + show ?thesis unfolding card_of_ordLeq[symmetric] + proof(intro exI[of _ F] conjI) + show "inj_on F (Func A1 B)" unfolding inj_on_def + proof safe fix f g assume f: "f \ Func A1 B" and g: "g \ Func A1 B" and eq: "F f = F g" show "f = g" proof(rule ext) fix a show "f a = g a" - proof(cases "a \ A1") - case True - thus ?thesis using eq A12 unfolding F_def fun_eq_iff - by (elim allE[of _ a]) auto - qed(insert f g, unfold Func_def, fastforce) + by (smt (verit) A12 F_def Func_def eq f g mem_Collect_eq subsetD) qed qed qed(insert bb, unfold Func_def F_def, force) qed lemma card_of_Func_option_mono: -fixes A1 A2 :: "'a set" and B :: "'b set" -assumes A12: "A1 \ A2" and B: "B \ {}" -shows "|Func_option A1 B| \o |Func_option A2 B|" -by (metis card_of_Func_mono[OF A12 B] card_of_Func_option_Func - ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric) + fixes A1 A2 :: "'a set" and B :: "'b set" + assumes A12: "A1 \ A2" and B: "B \ {}" + shows "|Func_option A1 B| \o |Func_option A2 B|" + by (metis card_of_Func_mono[OF A12 B] card_of_Func_option_Func + ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric) lemma card_of_Pfunc_Pow_Func_option: -assumes "B \ {}" -shows "|Pfunc A B| \o |Pow A \ Func_option A B|" + assumes "B \ {}" + shows "|Pfunc A B| \o |Pow A \ Func_option A B|" proof- have "|Pfunc A B| =o |\A' \ Pow A. Func_option A' B|" (is "_ =o ?K") unfolding Pfunc_Func_option by(rule card_of_refl) also have "?K \o |Sigma (Pow A) (\ A'. Func_option A' B)|" using card_of_UNION_Sigma . also have "|Sigma (Pow A) (\ A'. Func_option A' B)| \o |Pow A \ Func_option A B|" - apply(rule card_of_Sigma_mono1) using card_of_Func_option_mono[OF _ assms] by auto + by (simp add: assms card_of_Func_option_mono card_of_Sigma_mono1) finally show ?thesis . qed lemma Bpow_ordLeq_Func_Field: -assumes rc: "Card_order r" and r: "Field r \ {}" and A: "\finite A" -shows "|Bpow r A| \o |Func (Field r) A|" + assumes rc: "Card_order r" and r: "Field r \ {}" and A: "\finite A" + shows "|Bpow r A| \o |Func (Field r) A|" proof- let ?F = "\ f. {x | x a. f a = x \ a \ Field r}" {fix X assume "X \ Bpow r A - {{}}" - hence XA: "X \ A" and "|X| \o r" - and X: "X \ {}" unfolding Bpow_def by auto - hence "|X| \o |Field r|" by (metis Field_card_of card_of_mono2) - then obtain F where 1: "X = F ` (Field r)" - using card_of_ordLeq2[OF X] by metis - define f where [abs_def]: "f i = (if i \ Field r then F i else undefined)" for i - have "\ f \ Func (Field r) A. X = ?F f" - apply (intro bexI[of _ f]) using 1 XA unfolding Func_def f_def by auto + hence XA: "X \ A" and "|X| \o r" + and X: "X \ {}" unfolding Bpow_def by auto + hence "|X| \o |Field r|" by (metis Field_card_of card_of_mono2) + then obtain F where 1: "X = F ` (Field r)" + using card_of_ordLeq2[OF X] by metis + define f where [abs_def]: "f i = (if i \ Field r then F i else undefined)" for i + have "\ f \ Func (Field r) A. X = ?F f" + apply (intro bexI[of _ f]) using 1 XA unfolding Func_def f_def by auto } hence "Bpow r A - {{}} \ ?F ` (Func (Field r) A)" by auto hence "|Bpow r A - {{}}| \o |Func (Field r) A|" - by (rule surj_imp_ordLeq) + by (rule surj_imp_ordLeq) moreover {have 2: "\finite (Bpow r A)" using infinite_Bpow[OF rc r A] . - have "|Bpow r A| =o |Bpow r A - {{}}|" - by (metis 2 infinite_card_of_diff_singl ordIso_symmetric) + have "|Bpow r A| =o |Bpow r A - {{}}|" + by (metis 2 infinite_card_of_diff_singl ordIso_symmetric) } ultimately show ?thesis by (metis ordIso_ordLeq_trans) qed lemma empty_in_Func[simp]: -"B \ {} \ (\x. undefined) \ Func {} B" -unfolding Func_def by auto + "B \ {} \ (\x. undefined) \ Func {} B" + by simp lemma Func_mono[simp]: -assumes "B1 \ B2" -shows "Func A B1 \ Func A B2" -using assms unfolding Func_def by force + assumes "B1 \ B2" + shows "Func A B1 \ Func A B2" + using assms unfolding Func_def by force lemma Pfunc_mono[simp]: -assumes "A1 \ A2" and "B1 \ B2" -shows "Pfunc A B1 \ Pfunc A B2" -using assms unfolding Pfunc_def -apply safe -apply (case_tac "x a", auto) -apply (metis in_mono option.simps(5)) -done + assumes "A1 \ A2" and "B1 \ B2" + shows "Pfunc A B1 \ Pfunc A B2" + using assms unfolding Pfunc_def + by (force split: option.split_asm option.split) lemma card_of_Func_UNIV_UNIV: -"|Func (UNIV::'a set) (UNIV::'b set)| =o |UNIV::('a \ 'b) set|" -using card_of_Func_UNIV[of "UNIV::'b set"] by auto + "|Func (UNIV::'a set) (UNIV::'b set)| =o |UNIV::('a \ 'b) set|" + using card_of_Func_UNIV[of "UNIV::'b set"] by auto lemma ordLeq_Func: -assumes "{b1,b2} \ B" "b1 \ b2" -shows "|A| \o |Func A B|" -unfolding card_of_ordLeq[symmetric] proof(intro exI conjI) - let ?F = "\ aa a. if a \ A then (if a = aa then b1 else b2) else undefined" + assumes "{b1,b2} \ B" "b1 \ b2" + shows "|A| \o |Func A B|" + unfolding card_of_ordLeq[symmetric] proof(intro exI conjI) + let ?F = "\x a. if a \ A then (if a = x then b1 else b2) else undefined" show "inj_on ?F A" using assms unfolding inj_on_def fun_eq_iff by auto show "?F ` A \ Func A B" using assms unfolding Func_def by auto qed lemma infinite_Func: -assumes A: "\finite A" and B: "{b1,b2} \ B" "b1 \ b2" -shows "\finite (Func A B)" -using ordLeq_Func[OF B] by (metis A card_of_ordLeq_finite) + assumes A: "\finite A" and B: "{b1,b2} \ B" "b1 \ b2" + shows "\finite (Func A B)" + using ordLeq_Func[OF B] by (metis A card_of_ordLeq_finite) subsection \Infinite cardinals are limit ordinals\ lemma card_order_infinite_isLimOrd: -assumes c: "Card_order r" and i: "\finite (Field r)" -shows "isLimOrd r" + assumes c: "Card_order r" and i: "\finite (Field r)" + shows "isLimOrd r" proof- have 0: "wo_rel r" and 00: "Well_order r" - using c unfolding card_order_on_def wo_rel_def by auto + using c unfolding card_order_on_def wo_rel_def by auto hence rr: "Refl r" by (metis wo_rel.REFL) - show ?thesis unfolding wo_rel.isLimOrd_def[OF 0] wo_rel.isSuccOrd_def[OF 0] proof safe - fix j assume j: "j \ Field r" and jm: "\i\Field r. (i, j) \ r" - define p where "p = Restr r (Field r - {j})" - have fp: "Field p = Field r - {j}" - unfolding p_def apply(rule Refl_Field_Restr2[OF rr]) by auto - have of: "ofilter r (Field p)" unfolding wo_rel.ofilter_def[OF 0] proof safe - fix a x assume a: "a \ Field p" and "x \ under r a" - hence x: "(x,a) \ r" "x \ Field r" unfolding under_def Field_def by auto - moreover have a: "a \ j" "a \ Field r" "(a,j) \ r" using a jm unfolding fp by auto - ultimately have "x \ j" using j jm by (metis 0 wo_rel.max2_def wo_rel.max2_equals1) - thus "x \ Field p" using x unfolding fp by auto - qed(unfold p_def Field_def, auto) - have "p Field r" and "\i\Field r. (i, j) \ r" + then show False + by (metis Card_order_trans c i infinite_Card_order_limit) qed qed lemma insert_Chain: -assumes "Refl r" "C \ Chains r" and "i \ Field r" and "\j. j \ C \ (j,i) \ r \ (i,j) \ r" -shows "insert i C \ Chains r" -using assms unfolding Chains_def by (auto dest: refl_onD) + assumes "Refl r" "C \ Chains r" and "i \ Field r" and "\j. j \ C \ (j,i) \ r \ (i,j) \ r" + shows "insert i C \ Chains r" + using assms unfolding Chains_def by (auto dest: refl_onD) lemma Collect_insert: "{R j |j. j \ insert j1 J} = insert (R j1) {R j |j. j \ J}" -by auto + by auto lemma Field_init_seg_of[simp]: -"Field init_seg_of = UNIV" -unfolding Field_def init_seg_of_def by auto + "Field init_seg_of = UNIV" + unfolding Field_def init_seg_of_def by auto lemma refl_init_seg_of[intro, simp]: "refl init_seg_of" -unfolding refl_on_def Field_def by auto + unfolding refl_on_def Field_def by auto lemma regularCard_all_ex: -assumes r: "Card_order r" "regularCard r" -and As: "\ i j b. b \ B \ (i,j) \ r \ P i b \ P j b" -and Bsub: "\ b \ B. \ i \ Field r. P i b" -and cardB: "|B| i \ Field r. \ b \ B. P i b" + assumes r: "Card_order r" "regularCard r" + and As: "\ i j b. b \ B \ (i,j) \ r \ P i b \ P j b" + and Bsub: "\ b \ B. \ i \ Field r. P i b" + and cardB: "|B| i \ Field r. \ b \ B. P i b" proof- let ?As = "\i. {b \ B. P i b}" have "\i \ Field r. B \ ?As i" - apply(rule regularCard_UNION) using assms unfolding relChain_def by auto + apply(rule regularCard_UNION) using assms unfolding relChain_def by auto thus ?thesis by auto qed lemma relChain_stabilize: -assumes rc: "relChain r As" and AsB: "(\i \ Field r. As i) \ B" and Br: "|B| finite (Field r)" and cr: "Card_order r" -shows "\ i \ Field r. As (succ r i) = As i" + assumes rc: "relChain r As" and AsB: "(\i \ Field r. As i) \ B" and Br: "|B| finite (Field r)" and cr: "Card_order r" + shows "\ i \ Field r. As (succ r i) = As i" proof(rule ccontr, auto) have 0: "wo_rel r" and 00: "Well_order r" - unfolding wo_rel_def by (metis card_order_on_well_order_on cr)+ + unfolding wo_rel_def by (metis card_order_on_well_order_on cr)+ have L: "isLimOrd r" using ir cr by (metis card_order_infinite_isLimOrd) have AsBs: "(\i \ Field r. As (succ r i)) \ B" - using AsB L apply safe by (metis "0" UN_I subsetD wo_rel.isLimOrd_succ) + using AsB L by (simp add: "0" Sup_le_iff wo_rel.isLimOrd_succ) assume As_s: "\i\Field r. As (succ r i) \ As i" have 1: "\i j. (i,j) \ r \ i \ j \ As i \ As j" proof safe @@ -1576,18 +1399,19 @@ hence rij: "(succ r i, j) \ r" by (metis "0" wo_rel.succ_smallest) hence "As (succ r i) \ As j" using rc unfolding relChain_def by auto moreover - {have "(i,succ r i) \ r" apply(rule wo_rel.succ_in[OF 0]) - using 1 unfolding aboveS_def by auto - hence "As i \ As (succ r i)" using As_s rc rij unfolding relChain_def Field_def by auto + { have "(i,succ r i) \ r" + by (meson "0" "1"(1) FieldI1 L wo_rel.isLimOrd_aboveS wo_rel.succ_in) + hence "As i \ As (succ r i)" using As_s rc rij unfolding relChain_def Field_def by auto } ultimately show False unfolding Asij by auto qed (insert rc, unfold relChain_def, auto) hence "\ i \ Field r. \ a. a \ As (succ r i) - As i" - using wo_rel.succ_in[OF 0] AsB - by(metis 0 card_order_infinite_isLimOrd cr ir psubset_imp_ex_mem - wo_rel.isLimOrd_aboveS wo_rel.succ_diff) + using wo_rel.succ_in[OF 0] AsB + by(metis 0 card_order_infinite_isLimOrd cr ir psubset_imp_ex_mem + wo_rel.isLimOrd_aboveS wo_rel.succ_diff) then obtain f where f: "\ i \ Field r. f i \ As (succ r i) - As i" by metis - have "inj_on f (Field r)" unfolding inj_on_def proof safe + have "inj_on f (Field r)" unfolding inj_on_def + proof safe fix i j assume ij: "i \ Field r" "j \ Field r" and fij: "f i = f j" show "i = j" proof(cases rule: wo_rel.cases_Total3[OF 0], safe) @@ -1610,118 +1434,62 @@ subsection \Regular vs. stable cardinals\ -lemma stable_regularCard: -assumes cr: "Card_order r" and ir: "\finite (Field r)" and st: "stable r" -shows "regularCard r" -unfolding regularCard_def proof safe - fix K assume K: "K \ Field r" and cof: "cofinal K r" - have "|K| \o r" using K by (metis card_of_Field_ordIso card_of_mono1 cr ordLeq_ordIso_trans) - moreover - {assume Kr: "|K| a \ Field r. f a \ K \ a \ f a \ (a, f a) \ r" - using cof unfolding cofinal_def by metis - hence "Field r \ (\a \ K. underS r a)" unfolding underS_def by auto - hence "r \o |\a \ K. underS r a|" using cr - by (metis Card_order_iff_ordLeq_card_of card_of_mono1 ordLeq_transitive) - also have "|\a \ K. underS r a| \o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma) - also - {have "\ a \ K. |underS r a| 'a set" - assume "|A| a\A. |F a| (\a \ A. finite(F a))" - by (auto simp add: finite_iff_ordLess_natLeq) - hence "finite(Sigma A F)" by (simp only: finite_SigmaI[of A F]) - thus "|Sigma A F | finite (Field r)" -shows "stable(cardSuc r)" -using infinite_cardSuc_regularCard regularCard_stable -by (metis CARD INF cardSuc_Card_order cardSuc_finite) - -lemma stable_ordIso1: -assumes ST: "stable r" and ISO: "r' =o r" -shows "stable r'" -proof(unfold stable_def, auto) - fix A::"'b set" and F::"'b \ 'b set" - assume "|A| a \ A. |F a| (\a \ A. |F a| finite (Field r)" + shows "stable(cardSuc r)" + using infinite_cardSuc_regularCard regularCard_stable + by (metis CARD INF cardSuc_Card_order cardSuc_finite) lemma stable_ordIso: -assumes "r =o r'" -shows "stable r = stable r'" -using assms stable_ordIso1 stable_ordIso2 by blast + assumes "r =o r'" + shows "stable r = stable r'" + by (metis assms ordIso_symmetric stable_ordIso1) lemma stable_nat: "stable |UNIV::nat set|" -using stable_natLeq card_of_nat stable_ordIso by auto + using stable_natLeq card_of_nat stable_ordIso by auto text\Below, the type of "A" is not important -- we just had to choose an appropriate type to make "A" possible. What is important is that arbitrarily large infinite sets of stable cardinality exist.\ lemma infinite_stable_exists: -assumes CARD: "\r \ R. Card_order (r::'a rel)" -shows "\(A :: (nat + 'a set)set). + assumes CARD: "\r \ R. Card_order (r::'a rel)" + shows "\(A :: (nat + 'a set)set). \finite A \ stable |A| \ (\r \ R. r (A :: (nat + 'a set)set). \finite A \ stable |A| \ |UNIV::'a set| finite(?B <+> {})" using finite_Plus_iff by blast moreover have "stable |?B|" using stable_natLeq card_of_nat stable_ordIso1 by blast hence "stable |?B <+> {}|" using stable_ordIso card_of_Plus_empty1 by blast moreover - have "\finite(Field |?B| ) \ finite(Field |UNIV::'a set| )" using Case1 by simp + have "\finite(Field |?B| ) \ finite(Field |UNIV::'a set| )" using True by simp hence "|UNIV::'a set| {}|" using card_of_Plus_empty1 ordLess_ordIso_trans by blast ultimately show ?thesis by blast next - assume Case1: "\finite (UNIV::'a set)" + case False hence *: "\finite(Field |UNIV::'a set| )" by simp let ?B = "Field(cardSuc |UNIV::'a set| )" have 0: "|?B| =o |{} <+> ?B|" using card_of_Plus_empty2 by blast - have 1: "\finite ?B" using Case1 card_of_cardSuc_finite by blast + have 1: "\finite ?B" using False card_of_cardSuc_finite by blast hence 2: "\finite({} <+> ?B)" using 0 card_of_ordIso_finite by blast have "|?B| =o cardSuc |UNIV::'a set|" - using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast + using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast moreover have "stable(cardSuc |UNIV::'a set| )" - using stable_cardSuc * card_of_Card_order by blast + using stable_cardSuc * card_of_Card_order by blast ultimately have "stable |?B|" using stable_ordIso by blast hence 3: "stable |{} <+> ?B|" using stable_ordIso 0 by blast have "|UNIV::'a set| ?B|" using 0 ordLess_ordIso_trans by blast thus ?thesis using 2 3 by blast qed @@ -1729,9 +1497,9 @@ qed corollary infinite_regularCard_exists: -assumes CARD: "\r \ R. Card_order (r::'a rel)" -shows "\(A :: (nat + 'a set)set). + assumes CARD: "\r \ R. Card_order (r::'a rel)" + shows "\(A :: (nat + 'a set)set). \finite A \ regularCard |A| \ (\r \ R. r More on Injections, Bijections and Inverses\ theory Fun_More -imports Main + imports Main begin subsection \Purely functional properties\ (* unused *) -(*1*)lemma notIn_Un_bij_betw2: -assumes NIN: "b \ A" and NIN': "b' \ A'" and - BIJ: "bij_betw f A A'" -shows "bij_betw f (A \ {b}) (A' \ {b'}) = (f b = b')" -proof - assume "f b = b'" - thus "bij_betw f (A \ {b}) (A' \ {b'})" - using assms notIn_Un_bij_betw[of b A f A'] by auto -next - assume *: "bij_betw f (A \ {b}) (A' \ {b'})" - hence "f b \ A' \ {b'}" - unfolding bij_betw_def by auto - moreover - {assume "f b \ A'" - then obtain b1 where 1: "b1 \ A" and 2: "f b1 = f b" using BIJ - by (auto simp add: bij_betw_def) - hence "b = b1" using * - by (auto simp add: bij_betw_def inj_on_def) - with 1 NIN have False by auto - } - ultimately show "f b = b'" by blast -qed - -(* unused *) (*1*)lemma bij_betw_diff_singl: -assumes BIJ: "bij_betw f A A'" and IN: "a \ A" -shows "bij_betw f (A - {a}) (A' - {f a})" + assumes BIJ: "bij_betw f A A'" and IN: "a \ A" + shows "bij_betw f (A - {a}) (A' - {f a})" proof- let ?B = "A - {a}" let ?B' = "A' - {f a}" have "f a \ A'" using IN BIJ unfolding bij_betw_def by blast hence "a \ ?B \ f a \ ?B' \ A = ?B \ {a} \ A' = ?B' \ {f a}" - using IN by blast + using IN by blast thus ?thesis using notIn_Un_bij_betw3[of a ?B f ?B'] BIJ by simp qed @@ -54,120 +30,62 @@ (* unused *) (*1*)lemma bij_betw_inv_into_RIGHT: -assumes BIJ: "bij_betw f A A'" and SUB: "B' \ A'" -shows "f `((inv_into A f)`B') = B'" -using assms -proof(auto simp add: bij_betw_inv_into_right) - let ?f' = "(inv_into A f)" - fix a' assume *: "a' \ B'" - hence "a' \ A'" using SUB by auto - hence "a' = f (?f' a')" - using BIJ by (auto simp add: bij_betw_inv_into_right) - thus "a' \ f ` (?f' ` B')" using * by blast -qed + assumes BIJ: "bij_betw f A A'" and SUB: "B' \ A'" + shows "f `((inv_into A f)`B') = B'" + by (metis BIJ SUB bij_betw_imp_surj_on image_inv_into_cancel) + (* unused *) (*1*)lemma bij_betw_inv_into_RIGHT_LEFT: -assumes BIJ: "bij_betw f A A'" and SUB: "B' \ A'" and - IM: "(inv_into A f) ` B' = B" -shows "f ` B = B'" -proof- - have "f`((inv_into A f)` B') = B'" - using assms bij_betw_inv_into_RIGHT[of f A A' B'] by auto - thus ?thesis using IM by auto -qed + assumes BIJ: "bij_betw f A A'" and SUB: "B' \ A'" and + IM: "(inv_into A f) ` B' = B" + shows "f ` B = B'" + by (metis BIJ IM SUB bij_betw_inv_into_RIGHT) (* unused *) (*2*)lemma bij_betw_inv_into_twice: -assumes "bij_betw f A A'" -shows "\a \ A. inv_into A' (inv_into A f) a = f a" -proof - let ?f' = "inv_into A f" let ?f'' = "inv_into A' ?f'" - have 1: "bij_betw ?f' A' A" using assms - by (auto simp add: bij_betw_inv_into) - fix a assume *: "a \ A" - then obtain a' where 2: "a' \ A'" and 3: "?f' a' = a" - using 1 unfolding bij_betw_def by force - hence "?f'' a = a'" - using * 1 3 by (auto simp add: bij_betw_inv_into_left) - moreover have "f a = a'" using assms 2 3 - by (auto simp add: bij_betw_inv_into_right) - ultimately show "?f'' a = f a" by simp -qed + assumes "bij_betw f A A'" + shows "\a \ A. inv_into A' (inv_into A f) a = f a" + by (simp add: assms inv_into_inv_into_eq) subsection \Properties involving Hilbert choice\ (*1*)lemma bij_betw_inv_into_LEFT: -assumes BIJ: "bij_betw f A A'" and SUB: "B \ A" -shows "(inv_into A f)`(f ` B) = B" -using assms unfolding bij_betw_def using inv_into_image_cancel by force + assumes BIJ: "bij_betw f A A'" and SUB: "B \ A" + shows "(inv_into A f)`(f ` B) = B" + using assms unfolding bij_betw_def using inv_into_image_cancel by force (*1*)lemma bij_betw_inv_into_LEFT_RIGHT: -assumes BIJ: "bij_betw f A A'" and SUB: "B \ A" and - IM: "f ` B = B'" -shows "(inv_into A f) ` B' = B" -using assms bij_betw_inv_into_LEFT[of f A A' B] by fast + assumes BIJ: "bij_betw f A A'" and SUB: "B \ A" and + IM: "f ` B = B'" + shows "(inv_into A f) ` B' = B" + using assms bij_betw_inv_into_LEFT[of f A A' B] by fast subsection \Other facts\ (*3*)lemma atLeastLessThan_injective: -assumes "{0 ..< m::nat} = {0 ..< n}" -shows "m = n" -proof- - {assume "m < n" - hence "m \ {0 ..< n}" by auto - hence "{0 ..< m} < {0 ..< n}" by auto - hence False using assms by blast - } - moreover - {assume "n < m" - hence "n \ {0 ..< m}" by auto - hence "{0 ..< n} < {0 ..< m}" by auto - hence False using assms by blast - } - ultimately show ?thesis by force -qed + assumes "{0 ..< m::nat} = {0 ..< n}" + shows "m = n" + using assms atLeast0LessThan by force (*2*)lemma atLeastLessThan_injective2: -"bij_betw f {0 ..< m::nat} {0 ..< n} \ m = n" -using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n] - card_atLeastLessThan[of m] card_atLeastLessThan[of n] - bij_betw_iff_card[of "{0 ..< m}" "{0 ..< n}"] by auto + "bij_betw f {0 ..< m::nat} {0 ..< n} \ m = n" + using bij_betw_same_card by fastforce (*2*)lemma atLeastLessThan_less_eq: -"({0.. {0.. n)" -unfolding ivl_subset by arith + "({0.. {0.. n)" + by auto (*2*)lemma atLeastLessThan_less_eq2: -assumes "inj_on f {0..<(m::nat)} \ f ` {0.. {0.. n" -using assms -using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n] - card_atLeastLessThan[of m] card_atLeastLessThan[of n] - card_inj_on_le[of f "{0 ..< m}" "{0 ..< n}"] by fastforce - -(* unused *) -(*2*)lemma atLeastLessThan_less_eq3: -"(\f. inj_on f {0..<(m::nat)} \ f ` {0.. {0.. n)" -using atLeastLessThan_less_eq2 -proof(auto) - assume "m \ n" - hence "inj_on id {0.. id ` {0.. {0..f. inj_on f {0.. f ` {0.. {0.. {0.. n" + by (metis assms card_inj_on_le card_lessThan finite_lessThan lessThan_atLeast0) (* unused *) (*3*)lemma atLeastLessThan_less: -"({0.. {0.. {0.. = (m \ n \ m ~= n)" - using atLeastLessThan_less_eq atLeastLessThan_injective by blast - also have "\ = (m < n)" by auto - finally show ?thesis . -qed + "({0..Basics on Order-Like Relations\ theory Order_Relation_More -imports Main + imports Main begin subsection \The upper and lower bounds operators\ lemma aboveS_subset_above: "aboveS r a \ above r a" -by(auto simp add: aboveS_def above_def) + by(auto simp add: aboveS_def above_def) lemma AboveS_subset_Above: "AboveS r A \ Above r A" -by(auto simp add: AboveS_def Above_def) + by(auto simp add: AboveS_def Above_def) lemma UnderS_disjoint: "A Int (UnderS r A) = {}" -by(auto simp add: UnderS_def) + by(auto simp add: UnderS_def) lemma aboveS_notIn: "a \ aboveS r a" -by(auto simp add: aboveS_def) + by(auto simp add: aboveS_def) lemma Refl_above_in: "\Refl r; a \ Field r\ \ a \ above r a" -by(auto simp add: refl_on_def above_def) + by(auto simp add: refl_on_def above_def) lemma in_Above_under: "a \ Field r \ a \ Above r (under r a)" -by(auto simp add: Above_def under_def) + by(auto simp add: Above_def under_def) lemma in_Under_above: "a \ Field r \ a \ Under r (above r a)" -by(auto simp add: Under_def above_def) + by(auto simp add: Under_def above_def) lemma in_UnderS_aboveS: "a \ Field r \ a \ UnderS r (aboveS r a)" -by(auto simp add: UnderS_def aboveS_def) + by(auto simp add: UnderS_def aboveS_def) lemma UnderS_subset_Under: "UnderS r A \ Under r A" -by(auto simp add: UnderS_def Under_def) + by(auto simp add: UnderS_def Under_def) lemma subset_Above_Under: "B \ Field r \ B \ Above r (Under r B)" -by(auto simp add: Above_def Under_def) + by(auto simp add: Above_def Under_def) lemma subset_Under_Above: "B \ Field r \ B \ Under r (Above r B)" -by(auto simp add: Under_def Above_def) + by(auto simp add: Under_def Above_def) lemma subset_AboveS_UnderS: "B \ Field r \ B \ AboveS r (UnderS r B)" -by(auto simp add: AboveS_def UnderS_def) + by(auto simp add: AboveS_def UnderS_def) lemma subset_UnderS_AboveS: "B \ Field r \ B \ UnderS r (AboveS r B)" -by(auto simp add: UnderS_def AboveS_def) + by(auto simp add: UnderS_def AboveS_def) lemma Under_Above_Galois: -"\B \ Field r; C \ Field r\ \ (B \ Above r C) = (C \ Under r B)" -by(unfold Above_def Under_def, blast) + "\B \ Field r; C \ Field r\ \ (B \ Above r C) = (C \ Under r B)" + by(unfold Above_def Under_def, blast) lemma UnderS_AboveS_Galois: -"\B \ Field r; C \ Field r\ \ (B \ AboveS r C) = (C \ UnderS r B)" -by(unfold AboveS_def UnderS_def, blast) + "\B \ Field r; C \ Field r\ \ (B \ AboveS r C) = (C \ UnderS r B)" + by(unfold AboveS_def UnderS_def, blast) lemma Refl_above_aboveS: assumes REFL: "Refl r" and IN: "a \ Field r" @@ -79,20 +79,20 @@ with LIN IN order_on_defs[of "Field r" r] total_on_def[of "Field r" r] have "(a,b) \ r \ a = b" by blast thus "(a,b) \ r" - using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto + using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto next fix b assume "(b, a) \ r" thus "b \ Field r" - using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast + using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast next fix b assume "b \ a" "(a, b) \ r" thus "b \ Field r" - using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast + using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast qed lemma Linear_order_underS_above_Field: -assumes LIN: "Linear_order r" and IN: "a \ Field r" -shows "Field r = underS r a \ above r a" + assumes LIN: "Linear_order r" and IN: "a \ Field r" + shows "Field r = underS r a \ above r a" proof(unfold underS_def above_def, auto) assume "a \ Field r" "(a, a) \ r" with LIN IN order_on_defs[of _ r] refl_on_def[of _ r] @@ -102,174 +102,174 @@ with LIN IN order_on_defs[of "Field r" r] total_on_def[of "Field r" r] have "(b,a) \ r \ b = a" by blast thus "(b,a) \ r" - using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto + using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto next fix b assume "b \ a" "(b, a) \ r" thus "b \ Field r" - using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast + using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast next fix b assume "(a, b) \ r" thus "b \ Field r" - using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast + using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast qed lemma under_empty: "a \ Field r \ under r a = {}" -unfolding Field_def under_def by auto + unfolding Field_def under_def by auto lemma Under_Field: "Under r A \ Field r" -by(unfold Under_def Field_def, auto) + by(unfold Under_def Field_def, auto) lemma UnderS_Field: "UnderS r A \ Field r" -by(unfold UnderS_def Field_def, auto) + by(unfold UnderS_def Field_def, auto) lemma above_Field: "above r a \ Field r" -by(unfold above_def Field_def, auto) + by(unfold above_def Field_def, auto) lemma aboveS_Field: "aboveS r a \ Field r" -by(unfold aboveS_def Field_def, auto) + by(unfold aboveS_def Field_def, auto) lemma Above_Field: "Above r A \ Field r" -by(unfold Above_def Field_def, auto) + by(unfold Above_def Field_def, auto) lemma Refl_under_Under: -assumes REFL: "Refl r" and NE: "A \ {}" -shows "Under r A = (\a \ A. under r a)" + assumes REFL: "Refl r" and NE: "A \ {}" + shows "Under r A = (\a \ A. under r a)" proof show "Under r A \ (\a \ A. under r a)" - by(unfold Under_def under_def, auto) + by(unfold Under_def under_def, auto) next show "(\a \ A. under r a) \ Under r A" proof(auto) fix x assume *: "\xa \ A. x \ under r xa" hence "\xa \ A. (x,xa) \ r" - by (simp add: under_def) + by (simp add: under_def) moreover {from NE obtain a where "a \ A" by blast - with * have "x \ under r a" by simp - hence "x \ Field r" - using under_Field[of r a] by auto + with * have "x \ under r a" by simp + hence "x \ Field r" + using under_Field[of r a] by auto } ultimately show "x \ Under r A" - unfolding Under_def by auto + unfolding Under_def by auto qed qed lemma Refl_underS_UnderS: -assumes REFL: "Refl r" and NE: "A \ {}" -shows "UnderS r A = (\a \ A. underS r a)" + assumes REFL: "Refl r" and NE: "A \ {}" + shows "UnderS r A = (\a \ A. underS r a)" proof show "UnderS r A \ (\a \ A. underS r a)" - by(unfold UnderS_def underS_def, auto) + by(unfold UnderS_def underS_def, auto) next show "(\a \ A. underS r a) \ UnderS r A" proof(auto) fix x assume *: "\xa \ A. x \ underS r xa" hence "\xa \ A. x \ xa \ (x,xa) \ r" - by (auto simp add: underS_def) + by (auto simp add: underS_def) moreover {from NE obtain a where "a \ A" by blast - with * have "x \ underS r a" by simp - hence "x \ Field r" - using underS_Field[of _ r a] by auto + with * have "x \ underS r a" by simp + hence "x \ Field r" + using underS_Field[of _ r a] by auto } ultimately show "x \ UnderS r A" - unfolding UnderS_def by auto + unfolding UnderS_def by auto qed qed lemma Refl_above_Above: -assumes REFL: "Refl r" and NE: "A \ {}" -shows "Above r A = (\a \ A. above r a)" + assumes REFL: "Refl r" and NE: "A \ {}" + shows "Above r A = (\a \ A. above r a)" proof show "Above r A \ (\a \ A. above r a)" - by(unfold Above_def above_def, auto) + by(unfold Above_def above_def, auto) next show "(\a \ A. above r a) \ Above r A" proof(auto) fix x assume *: "\xa \ A. x \ above r xa" hence "\xa \ A. (xa,x) \ r" - by (simp add: above_def) + by (simp add: above_def) moreover {from NE obtain a where "a \ A" by blast - with * have "x \ above r a" by simp - hence "x \ Field r" - using above_Field[of r a] by auto + with * have "x \ above r a" by simp + hence "x \ Field r" + using above_Field[of r a] by auto } ultimately show "x \ Above r A" - unfolding Above_def by auto + unfolding Above_def by auto qed qed lemma Refl_aboveS_AboveS: -assumes REFL: "Refl r" and NE: "A \ {}" -shows "AboveS r A = (\a \ A. aboveS r a)" + assumes REFL: "Refl r" and NE: "A \ {}" + shows "AboveS r A = (\a \ A. aboveS r a)" proof show "AboveS r A \ (\a \ A. aboveS r a)" - by(unfold AboveS_def aboveS_def, auto) + by(unfold AboveS_def aboveS_def, auto) next show "(\a \ A. aboveS r a) \ AboveS r A" proof(auto) fix x assume *: "\xa \ A. x \ aboveS r xa" hence "\xa \ A. xa \ x \ (xa,x) \ r" - by (auto simp add: aboveS_def) + by (auto simp add: aboveS_def) moreover {from NE obtain a where "a \ A" by blast - with * have "x \ aboveS r a" by simp - hence "x \ Field r" - using aboveS_Field[of r a] by auto + with * have "x \ aboveS r a" by simp + hence "x \ Field r" + using aboveS_Field[of r a] by auto } ultimately show "x \ AboveS r A" - unfolding AboveS_def by auto + unfolding AboveS_def by auto qed qed lemma under_Under_singl: "under r a = Under r {a}" -by(unfold Under_def under_def, auto simp add: Field_def) + by(unfold Under_def under_def, auto simp add: Field_def) lemma underS_UnderS_singl: "underS r a = UnderS r {a}" -by(unfold UnderS_def underS_def, auto simp add: Field_def) + by(unfold UnderS_def underS_def, auto simp add: Field_def) lemma above_Above_singl: "above r a = Above r {a}" -by(unfold Above_def above_def, auto simp add: Field_def) + by(unfold Above_def above_def, auto simp add: Field_def) lemma aboveS_AboveS_singl: "aboveS r a = AboveS r {a}" -by(unfold AboveS_def aboveS_def, auto simp add: Field_def) + by(unfold AboveS_def aboveS_def, auto simp add: Field_def) lemma Under_decr: "A \ B \ Under r B \ Under r A" -by(unfold Under_def, auto) + by(unfold Under_def, auto) lemma UnderS_decr: "A \ B \ UnderS r B \ UnderS r A" -by(unfold UnderS_def, auto) + by(unfold UnderS_def, auto) lemma Above_decr: "A \ B \ Above r B \ Above r A" -by(unfold Above_def, auto) + by(unfold Above_def, auto) lemma AboveS_decr: "A \ B \ AboveS r B \ AboveS r A" -by(unfold AboveS_def, auto) + by(unfold AboveS_def, auto) lemma under_incl_iff: -assumes TRANS: "trans r" and REFL: "Refl r" and IN: "a \ Field r" -shows "(under r a \ under r b) = ((a,b) \ r)" + assumes TRANS: "trans r" and REFL: "Refl r" and IN: "a \ Field r" + shows "(under r a \ under r b) = ((a,b) \ r)" proof assume "(a,b) \ r" thus "under r a \ under r b" using TRANS - by (auto simp add: under_incr) + by (auto simp add: under_incr) next assume "under r a \ under r b" moreover have "a \ under r a" using REFL IN - by (auto simp add: Refl_under_in) + by (auto simp add: Refl_under_in) ultimately show "(a,b) \ r" - by (auto simp add: under_def) + by (auto simp add: under_def) qed lemma above_decr: -assumes TRANS: "trans r" and REL: "(a,b) \ r" -shows "above r b \ above r a" + assumes TRANS: "trans r" and REL: "(a,b) \ r" + shows "above r b \ above r a" proof(unfold above_def, auto) fix x assume "(b,x) \ r" with REL TRANS trans_def[of r] @@ -277,9 +277,9 @@ qed lemma aboveS_decr: -assumes TRANS: "trans r" and ANTISYM: "antisym r" and - REL: "(a,b) \ r" -shows "aboveS r b \ aboveS r a" + assumes TRANS: "trans r" and ANTISYM: "antisym r" and + REL: "(a,b) \ r" + shows "aboveS r b \ aboveS r a" proof(unfold aboveS_def, auto) assume *: "a \ b" and **: "(b,a) \ r" with ANTISYM antisym_def[of r] REL @@ -291,26 +291,26 @@ qed lemma under_trans: -assumes TRANS: "trans r" and - IN1: "a \ under r b" and IN2: "b \ under r c" -shows "a \ under r c" + assumes TRANS: "trans r" and + IN1: "a \ under r b" and IN2: "b \ under r c" + shows "a \ under r c" proof- have "(a,b) \ r \ (b,c) \ r" - using IN1 IN2 under_def by fastforce + using IN1 IN2 under_def by fastforce hence "(a,c) \ r" - using TRANS trans_def[of r] by blast + using TRANS trans_def[of r] by blast thus ?thesis unfolding under_def by simp qed lemma under_underS_trans: -assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ under r b" and IN2: "b \ underS r c" -shows "a \ underS r c" + assumes TRANS: "trans r" and ANTISYM: "antisym r" and + IN1: "a \ under r b" and IN2: "b \ underS r c" + shows "a \ underS r c" proof- have 0: "(a,b) \ r \ (b,c) \ r" - using IN1 IN2 under_def underS_def by fastforce + using IN1 IN2 under_def underS_def by fastforce hence 1: "(a,c) \ r" - using TRANS trans_def[of r] by blast + using TRANS trans_def[of r] by blast have 2: "b \ c" using IN2 underS_def by force have 3: "a \ c" proof @@ -321,14 +321,14 @@ qed lemma underS_under_trans: -assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ underS r b" and IN2: "b \ under r c" -shows "a \ underS r c" + assumes TRANS: "trans r" and ANTISYM: "antisym r" and + IN1: "a \ underS r b" and IN2: "b \ under r c" + shows "a \ underS r c" proof- have 0: "(a,b) \ r \ (b,c) \ r" - using IN1 IN2 under_def underS_def by fast + using IN1 IN2 under_def underS_def by fast hence 1: "(a,c) \ r" - using TRANS trans_def[of r] by fast + using TRANS trans_def[of r] by fast have 2: "a \ b" using IN1 underS_def by force have 3: "a \ c" proof @@ -339,36 +339,36 @@ qed lemma underS_underS_trans: -assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ underS r b" and IN2: "b \ underS r c" -shows "a \ underS r c" + assumes TRANS: "trans r" and ANTISYM: "antisym r" and + IN1: "a \ underS r b" and IN2: "b \ underS r c" + shows "a \ underS r c" proof- have "a \ under r b" - using IN1 underS_subset_under by fast + using IN1 underS_subset_under by fast with assms under_underS_trans show ?thesis by fast qed lemma above_trans: -assumes TRANS: "trans r" and - IN1: "b \ above r a" and IN2: "c \ above r b" -shows "c \ above r a" + assumes TRANS: "trans r" and + IN1: "b \ above r a" and IN2: "c \ above r b" + shows "c \ above r a" proof- have "(a,b) \ r \ (b,c) \ r" - using IN1 IN2 above_def by fast + using IN1 IN2 above_def by fast hence "(a,c) \ r" - using TRANS trans_def[of r] by blast + using TRANS trans_def[of r] by blast thus ?thesis unfolding above_def by simp qed lemma above_aboveS_trans: -assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "b \ above r a" and IN2: "c \ aboveS r b" -shows "c \ aboveS r a" + assumes TRANS: "trans r" and ANTISYM: "antisym r" and + IN1: "b \ above r a" and IN2: "c \ aboveS r b" + shows "c \ aboveS r a" proof- have 0: "(a,b) \ r \ (b,c) \ r" - using IN1 IN2 above_def aboveS_def by fast + using IN1 IN2 above_def aboveS_def by fast hence 1: "(a,c) \ r" - using TRANS trans_def[of r] by blast + using TRANS trans_def[of r] by blast have 2: "b \ c" using IN2 aboveS_def by force have 3: "a \ c" proof @@ -379,14 +379,14 @@ qed lemma aboveS_above_trans: -assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "b \ aboveS r a" and IN2: "c \ above r b" -shows "c \ aboveS r a" + assumes TRANS: "trans r" and ANTISYM: "antisym r" and + IN1: "b \ aboveS r a" and IN2: "c \ above r b" + shows "c \ aboveS r a" proof- have 0: "(a,b) \ r \ (b,c) \ r" - using IN1 IN2 above_def aboveS_def by fast + using IN1 IN2 above_def aboveS_def by fast hence 1: "(a,c) \ r" - using TRANS trans_def[of r] by blast + using TRANS trans_def[of r] by blast have 2: "a \ b" using IN1 aboveS_def by force have 3: "a \ c" proof @@ -397,26 +397,26 @@ qed lemma aboveS_aboveS_trans: -assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "b \ aboveS r a" and IN2: "c \ aboveS r b" -shows "c \ aboveS r a" + assumes TRANS: "trans r" and ANTISYM: "antisym r" and + IN1: "b \ aboveS r a" and IN2: "c \ aboveS r b" + shows "c \ aboveS r a" proof- have "b \ above r a" - using IN1 aboveS_subset_above by fast + using IN1 aboveS_subset_above by fast with assms above_aboveS_trans show ?thesis by fast qed lemma under_Under_trans: -assumes TRANS: "trans r" and - IN1: "a \ under r b" and IN2: "b \ Under r C" -shows "a \ Under r C" + assumes TRANS: "trans r" and + IN1: "a \ under r b" and IN2: "b \ Under r C" + shows "a \ Under r C" proof- have "b \ {u \ Field r. \x. x \ C \ (u, x) \ r}" using IN2 Under_def by force hence "(a,b) \ r \ (\c \ C. (b,c) \ r)" using IN1 under_def by fast hence "\c \ C. (a,c) \ r" - using TRANS trans_def[of r] by blast + using TRANS trans_def[of r] by blast moreover have "a \ Field r" using IN1 unfolding Field_def under_def by blast ultimately @@ -424,53 +424,53 @@ qed lemma underS_Under_trans: -assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ underS r b" and IN2: "b \ Under r C" -shows "a \ UnderS r C" + assumes TRANS: "trans r" and ANTISYM: "antisym r" and + IN1: "a \ underS r b" and IN2: "b \ Under r C" + shows "a \ UnderS r C" proof- from IN1 have "a \ under r b" - using underS_subset_under[of r b] by fast + using underS_subset_under[of r b] by fast with assms under_Under_trans have "a \ Under r C" by fast - (* *) + (* *) moreover have "a \ C" proof assume *: "a \ C" have 1: "b \ a \ (a,b) \ r" - using IN1 underS_def[of r b] by auto + using IN1 underS_def[of r b] by auto have "\c \ C. (b,c) \ r" - using IN2 Under_def[of r C] by auto + using IN2 Under_def[of r C] by auto with * have "(b,a) \ r" by simp with 1 ANTISYM antisym_def[of r] show False by blast qed - (* *) + (* *) ultimately show ?thesis unfolding UnderS_def - using Under_def by force + using Under_def by force qed lemma underS_UnderS_trans: -assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ underS r b" and IN2: "b \ UnderS r C" -shows "a \ UnderS r C" + assumes TRANS: "trans r" and ANTISYM: "antisym r" and + IN1: "a \ underS r b" and IN2: "b \ UnderS r C" + shows "a \ UnderS r C" proof- from IN2 have "b \ Under r C" - using UnderS_subset_Under[of r C] by blast + using UnderS_subset_Under[of r C] by blast with underS_Under_trans assms show ?thesis by force qed lemma above_Above_trans: -assumes TRANS: "trans r" and - IN1: "a \ above r b" and IN2: "b \ Above r C" -shows "a \ Above r C" + assumes TRANS: "trans r" and + IN1: "a \ above r b" and IN2: "b \ Above r C" + shows "a \ Above r C" proof- have "(b,a) \ r \ (\c \ C. (c,b) \ r)" using IN1[unfolded above_def] IN2[unfolded Above_def] by simp hence "\c \ C. (c,a) \ r" - using TRANS trans_def[of r] by blast + using TRANS trans_def[of r] by blast moreover have "a \ Field r" using IN1[unfolded above_def] Field_def by fast ultimately @@ -478,95 +478,95 @@ qed lemma aboveS_Above_trans: -assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ aboveS r b" and IN2: "b \ Above r C" -shows "a \ AboveS r C" + assumes TRANS: "trans r" and ANTISYM: "antisym r" and + IN1: "a \ aboveS r b" and IN2: "b \ Above r C" + shows "a \ AboveS r C" proof- from IN1 have "a \ above r b" - using aboveS_subset_above[of r b] by blast + using aboveS_subset_above[of r b] by blast with assms above_Above_trans have "a \ Above r C" by fast - (* *) + (* *) moreover have "a \ C" proof assume *: "a \ C" have 1: "b \ a \ (b,a) \ r" - using IN1 aboveS_def[of r b] by auto + using IN1 aboveS_def[of r b] by auto have "\c \ C. (c,b) \ r" - using IN2 Above_def[of r C] by auto + using IN2 Above_def[of r C] by auto with * have "(a,b) \ r" by simp with 1 ANTISYM antisym_def[of r] show False by blast qed - (* *) + (* *) ultimately show ?thesis unfolding AboveS_def - using Above_def by force + using Above_def by force qed lemma above_AboveS_trans: -assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ above r b" and IN2: "b \ AboveS r C" -shows "a \ AboveS r C" + assumes TRANS: "trans r" and ANTISYM: "antisym r" and + IN1: "a \ above r b" and IN2: "b \ AboveS r C" + shows "a \ AboveS r C" proof- from IN2 have "b \ Above r C" - using AboveS_subset_Above[of r C] by blast + using AboveS_subset_Above[of r C] by blast with assms above_Above_trans have "a \ Above r C" by force - (* *) + (* *) moreover have "a \ C" proof assume *: "a \ C" have 1: "(b,a) \ r" - using IN1 above_def[of r b] by auto + using IN1 above_def[of r b] by auto have "\c \ C. b \ c \ (c,b) \ r" - using IN2 AboveS_def[of r C] by auto + using IN2 AboveS_def[of r C] by auto with * have "b \ a \ (a,b) \ r" by simp with 1 ANTISYM antisym_def[of r] show False by blast qed - (* *) + (* *) ultimately show ?thesis unfolding AboveS_def - using Above_def by force + using Above_def by force qed lemma aboveS_AboveS_trans: -assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ aboveS r b" and IN2: "b \ AboveS r C" -shows "a \ AboveS r C" + assumes TRANS: "trans r" and ANTISYM: "antisym r" and + IN1: "a \ aboveS r b" and IN2: "b \ AboveS r C" + shows "a \ AboveS r C" proof- from IN2 have "b \ Above r C" - using AboveS_subset_Above[of r C] by blast + using AboveS_subset_Above[of r C] by blast with aboveS_Above_trans assms show ?thesis by force qed lemma under_UnderS_trans: -assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ under r b" and IN2: "b \ UnderS r C" -shows "a \ UnderS r C" + assumes TRANS: "trans r" and ANTISYM: "antisym r" and + IN1: "a \ under r b" and IN2: "b \ UnderS r C" + shows "a \ UnderS r C" proof- from IN2 have "b \ Under r C" - using UnderS_subset_Under[of r C] by blast + using UnderS_subset_Under[of r C] by blast with assms under_Under_trans have "a \ Under r C" by force - (* *) + (* *) moreover have "a \ C" proof assume *: "a \ C" have 1: "(a,b) \ r" - using IN1 under_def[of r b] by auto + using IN1 under_def[of r b] by auto have "\c \ C. b \ c \ (b,c) \ r" - using IN2 UnderS_def[of r C] by blast + using IN2 UnderS_def[of r C] by blast with * have "b \ a \ (b,a) \ r" by blast with 1 ANTISYM antisym_def[of r] show False by blast qed - (* *) + (* *) ultimately show ?thesis unfolding UnderS_def Under_def by fast qed @@ -575,12 +575,12 @@ subsection \Properties depending on more than one relation\ lemma under_incr2: -"r \ r' \ under r a \ under r' a" -unfolding under_def by blast + "r \ r' \ under r a \ under r' a" + unfolding under_def by blast lemma underS_incr2: -"r \ r' \ underS r a \ underS r' a" -unfolding underS_def by blast + "r \ r' \ underS r a \ underS r' a" + unfolding underS_def by blast (* FIXME: r \ r' lemma Under_incr: @@ -601,12 +601,12 @@ *) lemma above_incr2: -"r \ r' \ above r a \ above r' a" -unfolding above_def by blast + "r \ r' \ above r a \ above r' a" + unfolding above_def by blast lemma aboveS_incr2: -"r \ r' \ aboveS r a \ aboveS r' a" -unfolding aboveS_def by blast + "r \ r' \ aboveS r a \ aboveS r' a" + unfolding aboveS_def by blast (* FIXME lemma Above_incr: diff -r 7ed303c02418 -r 5df58a471d9e src/HOL/Cardinals/Order_Union.thy --- a/src/HOL/Cardinals/Order_Union.thy Wed Jan 11 17:02:52 2023 +0000 +++ b/src/HOL/Cardinals/Order_Union.thy Thu Jan 12 17:12:36 2023 +0000 @@ -7,7 +7,7 @@ section \Order Union\ theory Order_Union -imports Main + imports Main begin definition Osum :: "'a rel \ 'a rel \ 'a rel" (infix "Osum" 60) where @@ -19,10 +19,10 @@ unfolding Osum_def Field_def by blast lemma Osum_wf: -assumes FLD: "Field r Int Field r' = {}" and - WF: "wf r" and WF': "wf r'" -shows "wf (r Osum r')" -unfolding wf_eq_minimal2 unfolding Field_Osum + assumes FLD: "Field r Int Field r' = {}" and + WF: "wf r" and WF': "wf r'" + shows "wf (r Osum r')" + unfolding wf_eq_minimal2 unfolding Field_Osum proof(intro allI impI, elim conjE) fix A assume *: "A \ Field r \ Field r'" and **: "A \ {}" obtain B where B_def: "B = A Int Field r" by blast @@ -31,26 +31,26 @@ assume Case1: "B \ {}" hence "B \ {} \ B \ Field r" using B_def by auto then obtain a where 1: "a \ B" and 2: "\a1 \ B. (a1,a) \ r" - using WF unfolding wf_eq_minimal2 by blast + using WF unfolding wf_eq_minimal2 by blast hence 3: "a \ Field r \ a \ Field r'" using B_def FLD by auto - (* *) + (* *) have "\a1 \ A. (a1,a) \ r Osum r'" proof(intro ballI) fix a1 assume **: "a1 \ A" {assume Case11: "a1 \ Field r" - hence "(a1,a) \ r" using B_def ** 2 by auto - moreover - have "(a1,a) \ r'" using 3 by (auto simp add: Field_def) - ultimately have "(a1,a) \ r Osum r'" - using 3 unfolding Osum_def by auto + hence "(a1,a) \ r" using B_def ** 2 by auto + moreover + have "(a1,a) \ r'" using 3 by (auto simp add: Field_def) + ultimately have "(a1,a) \ r Osum r'" + using 3 unfolding Osum_def by auto } moreover {assume Case12: "a1 \ Field r" - hence "(a1,a) \ r" unfolding Field_def by auto - moreover - have "(a1,a) \ r'" using 3 unfolding Field_def by auto - ultimately have "(a1,a) \ r Osum r'" - using 3 unfolding Osum_def by auto + hence "(a1,a) \ r" unfolding Field_def by auto + moreover + have "(a1,a) \ r'" using 3 unfolding Field_def by auto + ultimately have "(a1,a) \ r Osum r'" + using 3 unfolding Osum_def by auto } ultimately show "(a1,a) \ r Osum r'" by blast qed @@ -59,9 +59,9 @@ assume Case2: "B = {}" hence 1: "A \ {} \ A \ Field r'" using * ** B_def by auto then obtain a' where 2: "a' \ A" and 3: "\a1' \ A. (a1',a') \ r'" - using WF' unfolding wf_eq_minimal2 by blast + using WF' unfolding wf_eq_minimal2 by blast hence 4: "a' \ Field r' \ a' \ Field r" using 1 FLD by blast - (* *) + (* *) have "\a1' \ A. (a1',a') \ r Osum r'" proof(unfold Osum_def, auto simp add: 3) fix a1' assume "(a1', a') \ r" @@ -75,296 +75,231 @@ qed lemma Osum_Refl: -assumes FLD: "Field r Int Field r' = {}" and - REFL: "Refl r" and REFL': "Refl r'" -shows "Refl (r Osum r')" -using assms -unfolding refl_on_def Field_Osum unfolding Osum_def by blast + assumes FLD: "Field r Int Field r' = {}" and + REFL: "Refl r" and REFL': "Refl r'" + shows "Refl (r Osum r')" + using assms + unfolding refl_on_def Field_Osum unfolding Osum_def by blast lemma Osum_trans: -assumes FLD: "Field r Int Field r' = {}" and - TRANS: "trans r" and TRANS': "trans r'" -shows "trans (r Osum r')" -proof(unfold trans_def, auto) - fix x y z assume *: "(x, y) \ r \o r'" and **: "(y, z) \ r \o r'" - show "(x, z) \ r \o r'" - proof- - {assume Case1: "(x,y) \ r" - hence 1: "x \ Field r \ y \ Field r" unfolding Field_def by auto - have ?thesis - proof- - {assume Case11: "(y,z) \ r" - hence "(x,z) \ r" using Case1 TRANS trans_def[of r] by blast - hence ?thesis unfolding Osum_def by auto - } - moreover - {assume Case12: "(y,z) \ r'" - hence "y \ Field r'" unfolding Field_def by auto - hence False using FLD 1 by auto - } - moreover - {assume Case13: "z \ Field r'" - hence ?thesis using 1 unfolding Osum_def by auto - } - ultimately show ?thesis using ** unfolding Osum_def by blast - qed - } - moreover - {assume Case2: "(x,y) \ r'" - hence 2: "x \ Field r' \ y \ Field r'" unfolding Field_def by auto - have ?thesis - proof- - {assume Case21: "(y,z) \ r" - hence "y \ Field r" unfolding Field_def by auto - hence False using FLD 2 by auto - } - moreover - {assume Case22: "(y,z) \ r'" - hence "(x,z) \ r'" using Case2 TRANS' trans_def[of r'] by blast - hence ?thesis unfolding Osum_def by auto - } - moreover - {assume Case23: "y \ Field r" - hence False using FLD 2 by auto - } - ultimately show ?thesis using ** unfolding Osum_def by blast - qed - } - moreover - {assume Case3: "x \ Field r \ y \ Field r'" - have ?thesis - proof- - {assume Case31: "(y,z) \ r" - hence "y \ Field r" unfolding Field_def by auto - hence False using FLD Case3 by auto - } - moreover - {assume Case32: "(y,z) \ r'" - hence "z \ Field r'" unfolding Field_def by blast - hence ?thesis unfolding Osum_def using Case3 by auto - } - moreover - {assume Case33: "y \ Field r" - hence False using FLD Case3 by auto - } - ultimately show ?thesis using ** unfolding Osum_def by blast - qed - } - ultimately show ?thesis using * unfolding Osum_def by blast - qed -qed + assumes FLD: "Field r Int Field r' = {}" and + TRANS: "trans r" and TRANS': "trans r'" + shows "trans (r Osum r')" + using assms + apply (clarsimp simp: trans_def disjoint_iff) + by (smt (verit) Domain.DomainI Field_def Osum_def Pair_inject Range.intros Un_iff case_prodE case_prodI mem_Collect_eq) lemma Osum_Preorder: -"\Field r Int Field r' = {}; Preorder r; Preorder r'\ \ Preorder (r Osum r')" -unfolding preorder_on_def using Osum_Refl Osum_trans by blast + "\Field r Int Field r' = {}; Preorder r; Preorder r'\ \ Preorder (r Osum r')" + unfolding preorder_on_def using Osum_Refl Osum_trans by blast lemma Osum_antisym: -assumes FLD: "Field r Int Field r' = {}" and - AN: "antisym r" and AN': "antisym r'" -shows "antisym (r Osum r')" + assumes FLD: "Field r Int Field r' = {}" and + AN: "antisym r" and AN': "antisym r'" + shows "antisym (r Osum r')" proof(unfold antisym_def, auto) fix x y assume *: "(x, y) \ r \o r'" and **: "(y, x) \ r \o r'" show "x = y" proof- {assume Case1: "(x,y) \ r" - hence 1: "x \ Field r \ y \ Field r" unfolding Field_def by auto - have ?thesis - proof- - have "(y,x) \ r \ ?thesis" - using Case1 AN antisym_def[of r] by blast - moreover - {assume "(y,x) \ r'" - hence "y \ Field r'" unfolding Field_def by auto - hence False using FLD 1 by auto - } - moreover - have "x \ Field r' \ False" using FLD 1 by auto - ultimately show ?thesis using ** unfolding Osum_def by blast - qed + hence 1: "x \ Field r \ y \ Field r" unfolding Field_def by auto + have ?thesis + proof- + have "(y,x) \ r \ ?thesis" + using Case1 AN antisym_def[of r] by blast + moreover + {assume "(y,x) \ r'" + hence "y \ Field r'" unfolding Field_def by auto + hence False using FLD 1 by auto + } + moreover + have "x \ Field r' \ False" using FLD 1 by auto + ultimately show ?thesis using ** unfolding Osum_def by blast + qed } moreover {assume Case2: "(x,y) \ r'" - hence 2: "x \ Field r' \ y \ Field r'" unfolding Field_def by auto - have ?thesis - proof- - {assume "(y,x) \ r" - hence "y \ Field r" unfolding Field_def by auto - hence False using FLD 2 by auto - } - moreover - have "(y,x) \ r' \ ?thesis" - using Case2 AN' antisym_def[of r'] by blast - moreover - {assume "y \ Field r" - hence False using FLD 2 by auto - } - ultimately show ?thesis using ** unfolding Osum_def by blast - qed + hence 2: "x \ Field r' \ y \ Field r'" unfolding Field_def by auto + have ?thesis + proof- + {assume "(y,x) \ r" + hence "y \ Field r" unfolding Field_def by auto + hence False using FLD 2 by auto + } + moreover + have "(y,x) \ r' \ ?thesis" + using Case2 AN' antisym_def[of r'] by blast + moreover + {assume "y \ Field r" + hence False using FLD 2 by auto + } + ultimately show ?thesis using ** unfolding Osum_def by blast + qed } moreover {assume Case3: "x \ Field r \ y \ Field r'" - have ?thesis - proof- - {assume "(y,x) \ r" - hence "y \ Field r" unfolding Field_def by auto - hence False using FLD Case3 by auto - } - moreover - {assume Case32: "(y,x) \ r'" - hence "x \ Field r'" unfolding Field_def by blast - hence False using FLD Case3 by auto - } - moreover - have "\ y \ Field r" using FLD Case3 by auto - ultimately show ?thesis using ** unfolding Osum_def by blast - qed + have ?thesis + proof- + {assume "(y,x) \ r" + hence "y \ Field r" unfolding Field_def by auto + hence False using FLD Case3 by auto + } + moreover + {assume Case32: "(y,x) \ r'" + hence "x \ Field r'" unfolding Field_def by blast + hence False using FLD Case3 by auto + } + moreover + have "\ y \ Field r" using FLD Case3 by auto + ultimately show ?thesis using ** unfolding Osum_def by blast + qed } ultimately show ?thesis using * unfolding Osum_def by blast qed qed lemma Osum_Partial_order: -"\Field r Int Field r' = {}; Partial_order r; Partial_order r'\ \ + "\Field r Int Field r' = {}; Partial_order r; Partial_order r'\ \ Partial_order (r Osum r')" -unfolding partial_order_on_def using Osum_Preorder Osum_antisym by blast + unfolding partial_order_on_def using Osum_Preorder Osum_antisym by blast lemma Osum_Total: -assumes FLD: "Field r Int Field r' = {}" and - TOT: "Total r" and TOT': "Total r'" -shows "Total (r Osum r')" -using assms -unfolding total_on_def Field_Osum unfolding Osum_def by blast + assumes FLD: "Field r Int Field r' = {}" and + TOT: "Total r" and TOT': "Total r'" + shows "Total (r Osum r')" + using assms + unfolding total_on_def Field_Osum unfolding Osum_def by blast lemma Osum_Linear_order: -"\Field r Int Field r' = {}; Linear_order r; Linear_order r'\ \ + "\Field r Int Field r' = {}; Linear_order r; Linear_order r'\ \ Linear_order (r Osum r')" -unfolding linear_order_on_def using Osum_Partial_order Osum_Total by blast + unfolding linear_order_on_def using Osum_Partial_order Osum_Total by blast lemma Osum_minus_Id1: -assumes "r \ Id" -shows "(r Osum r') - Id \ (r' - Id) \ (Field r \ Field r')" + assumes "r \ Id" + shows "(r Osum r') - Id \ (r' - Id) \ (Field r \ Field r')" proof- let ?Left = "(r Osum r') - Id" let ?Right = "(r' - Id) \ (Field r \ Field r')" {fix a::'a and b assume *: "(a,b) \ Id" - {assume "(a,b) \ r" - with * have False using assms by auto - } - moreover - {assume "(a,b) \ r'" - with * have "(a,b) \ r' - Id" by auto - } - ultimately - have "(a,b) \ ?Left \ (a,b) \ ?Right" - unfolding Osum_def by auto + {assume "(a,b) \ r" + with * have False using assms by auto + } + moreover + {assume "(a,b) \ r'" + with * have "(a,b) \ r' - Id" by auto + } + ultimately + have "(a,b) \ ?Left \ (a,b) \ ?Right" + unfolding Osum_def by auto } thus ?thesis by auto qed lemma Osum_minus_Id2: -assumes "r' \ Id" -shows "(r Osum r') - Id \ (r - Id) \ (Field r \ Field r')" + assumes "r' \ Id" + shows "(r Osum r') - Id \ (r - Id) \ (Field r \ Field r')" proof- let ?Left = "(r Osum r') - Id" let ?Right = "(r - Id) \ (Field r \ Field r')" {fix a::'a and b assume *: "(a,b) \ Id" - {assume "(a,b) \ r'" - with * have False using assms by auto - } - moreover - {assume "(a,b) \ r" - with * have "(a,b) \ r - Id" by auto - } - ultimately - have "(a,b) \ ?Left \ (a,b) \ ?Right" - unfolding Osum_def by auto + {assume "(a,b) \ r'" + with * have False using assms by auto + } + moreover + {assume "(a,b) \ r" + with * have "(a,b) \ r - Id" by auto + } + ultimately + have "(a,b) \ ?Left \ (a,b) \ ?Right" + unfolding Osum_def by auto } thus ?thesis by auto qed lemma Osum_minus_Id: -assumes TOT: "Total r" and TOT': "Total r'" and - NID: "\ (r \ Id)" and NID': "\ (r' \ Id)" -shows "(r Osum r') - Id \ (r - Id) Osum (r' - Id)" + assumes TOT: "Total r" and TOT': "Total r'" and + NID: "\ (r \ Id)" and NID': "\ (r' \ Id)" + shows "(r Osum r') - Id \ (r - Id) Osum (r' - Id)" proof- {fix a a' assume *: "(a,a') \ (r Osum r')" and **: "a \ a'" - have "(a,a') \ (r - Id) Osum (r' - Id)" - proof- - {assume "(a,a') \ r \ (a,a') \ r'" - with ** have ?thesis unfolding Osum_def by auto - } - moreover - {assume "a \ Field r \ a' \ Field r'" - hence "a \ Field(r - Id) \ a' \ Field (r' - Id)" - using assms Total_Id_Field by blast - hence ?thesis unfolding Osum_def by auto - } - ultimately show ?thesis using * unfolding Osum_def by fast - qed + have "(a,a') \ (r - Id) Osum (r' - Id)" + proof- + {assume "(a,a') \ r \ (a,a') \ r'" + with ** have ?thesis unfolding Osum_def by auto + } + moreover + {assume "a \ Field r \ a' \ Field r'" + hence "a \ Field(r - Id) \ a' \ Field (r' - Id)" + using assms Total_Id_Field by blast + hence ?thesis unfolding Osum_def by auto + } + ultimately show ?thesis using * unfolding Osum_def by fast + qed } thus ?thesis by(auto simp add: Osum_def) qed lemma wf_Int_Times: -assumes "A Int B = {}" -shows "wf(A \ B)" -unfolding wf_def using assms by blast + assumes "A Int B = {}" + shows "wf(A \ B)" + unfolding wf_def using assms by blast lemma Osum_wf_Id: -assumes TOT: "Total r" and TOT': "Total r'" and - FLD: "Field r Int Field r' = {}" and - WF: "wf(r - Id)" and WF': "wf(r' - Id)" -shows "wf ((r Osum r') - Id)" + assumes TOT: "Total r" and TOT': "Total r'" and + FLD: "Field r Int Field r' = {}" and + WF: "wf(r - Id)" and WF': "wf(r' - Id)" + shows "wf ((r Osum r') - Id)" proof(cases "r \ Id \ r' \ Id") assume Case1: "\(r \ Id \ r' \ Id)" have "Field(r - Id) Int Field(r' - Id) = {}" - using FLD mono_Field[of "r - Id" r] mono_Field[of "r' - Id" r'] - Diff_subset[of r Id] Diff_subset[of r' Id] by blast + using FLD mono_Field[of "r - Id" r] mono_Field[of "r' - Id" r'] + Diff_subset[of r Id] Diff_subset[of r' Id] by blast thus ?thesis - using Case1 Osum_minus_Id[of r r'] assms Osum_wf[of "r - Id" "r' - Id"] - wf_subset[of "(r - Id) \o (r' - Id)" "(r Osum r') - Id"] by auto + using Case1 Osum_minus_Id[of r r'] assms Osum_wf[of "r - Id" "r' - Id"] + wf_subset[of "(r - Id) \o (r' - Id)" "(r Osum r') - Id"] by auto next have 1: "wf(Field r \ Field r')" - using FLD by (auto simp add: wf_Int_Times) + using FLD by (auto simp add: wf_Int_Times) assume Case2: "r \ Id \ r' \ Id" moreover {assume Case21: "r \ Id" - hence "(r Osum r') - Id \ (r' - Id) \ (Field r \ Field r')" - using Osum_minus_Id1[of r r'] by simp - moreover - {have "Domain(Field r \ Field r') Int Range(r' - Id) = {}" - using FLD unfolding Field_def by blast - hence "wf((r' - Id) \ (Field r \ Field r'))" - using 1 WF' wf_Un[of "Field r \ Field r'" "r' - Id"] - by (auto simp add: Un_commute) - } - ultimately have ?thesis using wf_subset by blast + hence "(r Osum r') - Id \ (r' - Id) \ (Field r \ Field r')" + using Osum_minus_Id1[of r r'] by simp + moreover + {have "Domain(Field r \ Field r') Int Range(r' - Id) = {}" + using FLD unfolding Field_def by blast + hence "wf((r' - Id) \ (Field r \ Field r'))" + using 1 WF' wf_Un[of "Field r \ Field r'" "r' - Id"] + by (auto simp add: Un_commute) + } + ultimately have ?thesis using wf_subset by blast } moreover {assume Case22: "r' \ Id" - hence "(r Osum r') - Id \ (r - Id) \ (Field r \ Field r')" - using Osum_minus_Id2[of r' r] by simp - moreover - {have "Range(Field r \ Field r') Int Domain(r - Id) = {}" - using FLD unfolding Field_def by blast - hence "wf((r - Id) \ (Field r \ Field r'))" - using 1 WF wf_Un[of "r - Id" "Field r \ Field r'"] - by (auto simp add: Un_commute) - } - ultimately have ?thesis using wf_subset by blast + hence "(r Osum r') - Id \ (r - Id) \ (Field r \ Field r')" + using Osum_minus_Id2[of r' r] by simp + moreover + {have "Range(Field r \ Field r') Int Domain(r - Id) = {}" + using FLD unfolding Field_def by blast + hence "wf((r - Id) \ (Field r \ Field r'))" + using 1 WF wf_Un[of "r - Id" "Field r \ Field r'"] + by (auto simp add: Un_commute) + } + ultimately have ?thesis using wf_subset by blast } ultimately show ?thesis by blast qed lemma Osum_Well_order: -assumes FLD: "Field r Int Field r' = {}" and - WELL: "Well_order r" and WELL': "Well_order r'" -shows "Well_order (r Osum r')" + assumes FLD: "Field r Int Field r' = {}" and + WELL: "Well_order r" and WELL': "Well_order r'" + shows "Well_order (r Osum r')" proof- have "Total r \ Total r'" using WELL WELL' - by (auto simp add: order_on_defs) + by (auto simp add: order_on_defs) thus ?thesis using assms unfolding well_order_on_def - using Osum_Linear_order Osum_wf_Id by blast + using Osum_Linear_order Osum_wf_Id by blast qed end diff -r 7ed303c02418 -r 5df58a471d9e src/HOL/Cardinals/Wellorder_Constructions.thy --- a/src/HOL/Cardinals/Wellorder_Constructions.thy Wed Jan 11 17:02:52 2023 +0000 +++ b/src/HOL/Cardinals/Wellorder_Constructions.thy Thu Jan 12 17:12:36 2023 +0000 @@ -8,8 +8,8 @@ section \Constructions on Wellorders\ theory Wellorder_Constructions -imports - Wellorder_Embedding Order_Union + imports + Wellorder_Embedding Order_Union begin unbundle cardinal_syntax @@ -21,254 +21,189 @@ Func_empty[simp] Func_is_emp[simp] -lemma Func_emp2[simp]: "A \ {} \ Func A {} = {}" by auto - - -subsection \Restriction to a set\ - -lemma Restr_incr2: -"r <= r' \ Restr r A <= Restr r' A" -by blast - -lemma Restr_incr: -"\r \ r'; A \ A'\ \ Restr r A \ Restr r' A'" -by blast - -lemma Restr_Int: -"Restr (Restr r A) B = Restr r (A Int B)" -by blast - -lemma Restr_iff: "(a,b) \ Restr r A = (a \ A \ b \ A \ (a,b) \ r)" -by (auto simp add: Field_def) - -lemma Restr_subset1: "Restr r A \ r" -by auto - -lemma Restr_subset2: "Restr r A \ A \ A" -by auto - -lemma wf_Restr: -"wf r \ wf(Restr r A)" -using Restr_subset by (elim wf_subset) simp - -lemma Restr_incr1: -"A \ B \ Restr r A \ Restr r B" -by blast subsection \Order filters versus restrictions and embeddings\ -lemma ofilter_Restr: -assumes WELL: "Well_order r" and - OFA: "ofilter r A" and OFB: "ofilter r B" and SUB: "A \ B" -shows "ofilter (Restr r B) A" -proof- - let ?rB = "Restr r B" - have Well: "wo_rel r" unfolding wo_rel_def using WELL . - hence Refl: "Refl r" by (auto simp add: wo_rel.REFL) - hence Field: "Field ?rB = Field r Int B" - using Refl_Field_Restr by blast - have WellB: "wo_rel ?rB \ Well_order ?rB" using WELL - by (auto simp add: Well_order_Restr wo_rel_def) - (* Main proof *) - show ?thesis - proof(auto simp add: WellB wo_rel.ofilter_def) - fix a assume "a \ A" - hence "a \ Field r \ a \ B" using assms Well - by (auto simp add: wo_rel.ofilter_def) - with Field show "a \ Field(Restr r B)" by auto - next - fix a b assume *: "a \ A" and "b \ under (Restr r B) a" - hence "b \ under r a" - using WELL OFB SUB ofilter_Restr_under[of r B a] by auto - thus "b \ A" using * Well OFA by(auto simp add: wo_rel.ofilter_def) - qed -qed - lemma ofilter_subset_iso: -assumes WELL: "Well_order r" and - OFA: "ofilter r A" and OFB: "ofilter r B" -shows "(A = B) = iso (Restr r A) (Restr r B) id" -using assms -by (auto simp add: ofilter_subset_embedS_iso) + assumes WELL: "Well_order r" and + OFA: "ofilter r A" and OFB: "ofilter r B" + shows "(A = B) = iso (Restr r A) (Restr r B) id" + using assms by (auto simp add: ofilter_subset_embedS_iso) subsection \Ordering the well-orders by existence of embeddings\ corollary ordLeq_refl_on: "refl_on {r. Well_order r} ordLeq" -using ordLeq_reflexive unfolding ordLeq_def refl_on_def -by blast + using ordLeq_reflexive unfolding ordLeq_def refl_on_def + by blast corollary ordLeq_trans: "trans ordLeq" -using trans_def[of ordLeq] ordLeq_transitive by blast + using trans_def[of ordLeq] ordLeq_transitive by blast corollary ordLeq_preorder_on: "preorder_on {r. Well_order r} ordLeq" -by(auto simp add: preorder_on_def ordLeq_refl_on ordLeq_trans) + by(auto simp add: preorder_on_def ordLeq_refl_on ordLeq_trans) corollary ordIso_refl_on: "refl_on {r. Well_order r} ordIso" -using ordIso_reflexive unfolding refl_on_def ordIso_def -by blast + using ordIso_reflexive unfolding refl_on_def ordIso_def + by blast corollary ordIso_trans: "trans ordIso" -using trans_def[of ordIso] ordIso_transitive by blast + using trans_def[of ordIso] ordIso_transitive by blast corollary ordIso_sym: "sym ordIso" -by (auto simp add: sym_def ordIso_symmetric) + by (auto simp add: sym_def ordIso_symmetric) corollary ordIso_equiv: "equiv {r. Well_order r} ordIso" -by (auto simp add: equiv_def ordIso_sym ordIso_refl_on ordIso_trans) + by (auto simp add: equiv_def ordIso_sym ordIso_refl_on ordIso_trans) lemma ordLess_Well_order_simp[simp]: -assumes "r Well_order r'" -using assms unfolding ordLess_def by simp + assumes "r Well_order r'" + using assms unfolding ordLess_def by simp lemma ordIso_Well_order_simp[simp]: -assumes "r =o r'" -shows "Well_order r \ Well_order r'" -using assms unfolding ordIso_def by simp + assumes "r =o r'" + shows "Well_order r \ Well_order r'" + using assms unfolding ordIso_def by simp lemma ordLess_irrefl: "irrefl ordLess" -by(unfold irrefl_def, auto simp add: ordLess_irreflexive) + by(unfold irrefl_def, auto simp add: ordLess_irreflexive) lemma ordLess_or_ordIso: -assumes WELL: "Well_order r" and WELL': "Well_order r'" -shows "r r' r =o r'" -unfolding ordLess_def ordIso_def -using assms embedS_or_iso[of r r'] by auto + assumes WELL: "Well_order r" and WELL': "Well_order r'" + shows "r r' r =o r'" + unfolding ordLess_def ordIso_def + using assms embedS_or_iso[of r r'] by auto corollary ordLeq_ordLess_Un_ordIso: -"ordLeq = ordLess \ ordIso" -by (auto simp add: ordLeq_iff_ordLess_or_ordIso) - -lemma not_ordLeq_ordLess: -"r \o r' \ \ r' ordIso" + by (auto simp add: ordLeq_iff_ordLess_or_ordIso) lemma ordIso_or_ordLess: -assumes WELL: "Well_order r" and WELL': "Well_order r'" -shows "r =o r' \ r r' r r' o r" + assumes "Well_order r" and "ofilter r A" + shows "Restr r A \o r" proof- have "A \ Field r" using assms by (auto simp add: wo_rel_def wo_rel.ofilter_def) thus ?thesis using assms - by (simp add: ofilter_subset_ordLeq wo_rel.Field_ofilter - wo_rel_def Restr_Field) + by (simp add: ofilter_subset_ordLeq wo_rel.Field_ofilter + wo_rel_def Restr_Field) qed corollary under_Restr_ordLeq: -"Well_order r \ Restr r (under r a) \o r" -by (auto simp add: ofilter_ordLeq wo_rel.under_ofilter wo_rel_def) + "Well_order r \ Restr r (under r a) \o r" + by (auto simp add: ofilter_ordLeq wo_rel.under_ofilter wo_rel_def) subsection \Copy via direct images\ lemma Id_dir_image: "dir_image Id f \ Id" -unfolding dir_image_def by auto + unfolding dir_image_def by auto lemma Un_dir_image: -"dir_image (r1 \ r2) f = (dir_image r1 f) \ (dir_image r2 f)" -unfolding dir_image_def by auto + "dir_image (r1 \ r2) f = (dir_image r1 f) \ (dir_image r2 f)" + unfolding dir_image_def by auto lemma Int_dir_image: -assumes "inj_on f (Field r1 \ Field r2)" -shows "dir_image (r1 Int r2) f = (dir_image r1 f) Int (dir_image r2 f)" + assumes "inj_on f (Field r1 \ Field r2)" + shows "dir_image (r1 Int r2) f = (dir_image r1 f) Int (dir_image r2 f)" proof show "dir_image (r1 Int r2) f \ (dir_image r1 f) Int (dir_image r2 f)" - using assms unfolding dir_image_def inj_on_def by auto + using assms unfolding dir_image_def inj_on_def by auto next show "(dir_image r1 f) Int (dir_image r2 f) \ dir_image (r1 Int r2) f" proof(clarify) fix a' b' assume "(a',b') \ dir_image r1 f" "(a',b') \ dir_image r2 f" then obtain a1 b1 a2 b2 - where 1: "a' = f a1 \ b' = f b1 \ a' = f a2 \ b' = f b2" and - 2: "(a1,b1) \ r1 \ (a2,b2) \ r2" and - 3: "{a1,b1} \ Field r1 \ {a2,b2} \ Field r2" - unfolding dir_image_def Field_def by blast + where 1: "a' = f a1 \ b' = f b1 \ a' = f a2 \ b' = f b2" and + 2: "(a1,b1) \ r1 \ (a2,b2) \ r2" and + 3: "{a1,b1} \ Field r1 \ {a2,b2} \ Field r2" + unfolding dir_image_def Field_def by blast hence "a1 = a2 \ b1 = b2" using assms unfolding inj_on_def by auto hence "a' = f a1 \ b' = f b1 \ (a1,b1) \ r1 Int r2 \ (a2,b2) \ r1 Int r2" - using 1 2 by auto + using 1 2 by auto thus "(a',b') \ dir_image (r1 \ r2) f" - unfolding dir_image_def by blast + unfolding dir_image_def by blast qed qed (* More facts on ordinal sum: *) lemma Osum_embed: -assumes FLD: "Field r Int Field r' = {}" and - WELL: "Well_order r" and WELL': "Well_order r'" -shows "embed r (r Osum r') id" + assumes FLD: "Field r Int Field r' = {}" and + WELL: "Well_order r" and WELL': "Well_order r'" + shows "embed r (r Osum r') id" proof- have 1: "Well_order (r Osum r')" - using assms by (auto simp add: Osum_Well_order) + using assms by (auto simp add: Osum_Well_order) moreover have "compat r (r Osum r') id" - unfolding compat_def Osum_def by auto + unfolding compat_def Osum_def by auto moreover have "inj_on id (Field r)" by simp moreover have "ofilter (r Osum r') (Field r)" - using 1 proof(auto simp add: wo_rel_def wo_rel.ofilter_def - Field_Osum under_def) + using 1 proof(auto simp add: wo_rel_def wo_rel.ofilter_def + Field_Osum under_def) fix a b assume 2: "a \ Field r" and 3: "(b,a) \ r Osum r'" moreover {assume "(b,a) \ r'" - hence "a \ Field r'" using Field_def[of r'] by blast - hence False using 2 FLD by blast + hence "a \ Field r'" using Field_def[of r'] by blast + hence False using 2 FLD by blast } moreover {assume "a \ Field r'" - hence False using 2 FLD by blast + hence False using 2 FLD by blast } ultimately show "b \ Field r" by (auto simp add: Osum_def Field_def) qed ultimately show ?thesis - using assms by (auto simp add: embed_iff_compat_inj_on_ofilter) + using assms by (auto simp add: embed_iff_compat_inj_on_ofilter) qed corollary Osum_ordLeq: -assumes FLD: "Field r Int Field r' = {}" and - WELL: "Well_order r" and WELL': "Well_order r'" -shows "r \o r Osum r'" -using assms Osum_embed Osum_Well_order -unfolding ordLeq_def by blast + assumes FLD: "Field r Int Field r' = {}" and + WELL: "Well_order r" and WELL': "Well_order r'" + shows "r \o r Osum r'" + using assms Osum_embed Osum_Well_order + unfolding ordLeq_def by blast lemma Well_order_embed_copy: -assumes WELL: "well_order_on A r" and - INJ: "inj_on f A" and SUB: "f ` A \ B" -shows "\r'. well_order_on B r' \ r \o r'" + assumes WELL: "well_order_on A r" and + INJ: "inj_on f A" and SUB: "f ` A \ B" + shows "\r'. well_order_on B r' \ r \o r'" proof- have "bij_betw f A (f ` A)" - using INJ inj_on_imp_bij_betw by blast + using INJ inj_on_imp_bij_betw by blast then obtain r'' where "well_order_on (f ` A) r''" and 1: "r =o r''" - using WELL Well_order_iso_copy by blast + using WELL Well_order_iso_copy by blast hence 2: "Well_order r'' \ Field r'' = (f ` A)" - using well_order_on_Well_order by blast - (* *) + using well_order_on_Well_order by blast + (* *) let ?C = "B - (f ` A)" obtain r''' where "well_order_on ?C r'''" - using well_order_on by blast + using well_order_on by blast hence 3: "Well_order r''' \ Field r''' = ?C" - using well_order_on_Well_order by blast - (* *) + using well_order_on_Well_order by blast + (* *) let ?r' = "r'' Osum r'''" have "Field r'' Int Field r''' = {}" - using 2 3 by auto + using 2 3 by auto hence "r'' \o ?r'" using Osum_ordLeq[of r'' r'''] 2 3 by blast hence 4: "r \o ?r'" using 1 ordIso_ordLeq_trans by blast - (* *) + (* *) hence "Well_order ?r'" unfolding ordLeq_def by auto moreover have "Field ?r' = B" using 2 3 SUB by (auto simp add: Field_Osum) @@ -278,56 +213,56 @@ subsection \The maxim among a finite set of ordinals\ -text \The correct phrasing would be ``a maxim of ...", as \\o\ is only a preorder.\ +text \The correct phrasing would be ``a maxim of \", as \\o\ is only a preorder.\ definition isOmax :: "'a rel set \ 'a rel \ bool" -where -"isOmax R r \ r \ R \ (\r' \ R. r' \o r)" + where + "isOmax R r \ r \ R \ (\r' \ R. r' \o r)" definition omax :: "'a rel set \ 'a rel" -where -"omax R == SOME r. isOmax R r" + where + "omax R == SOME r. isOmax R r" lemma exists_isOmax: -assumes "finite R" and "R \ {}" and "\ r \ R. Well_order r" -shows "\ r. isOmax R r" + assumes "finite R" and "R \ {}" and "\ r \ R. Well_order r" + shows "\ r. isOmax R r" proof- have "finite R \ R \ {} \ (\ r \ R. Well_order r) \ (\ r. isOmax R r)" - apply(erule finite_induct) apply(simp add: isOmax_def) + apply(erule finite_induct) apply(simp add: isOmax_def) proof(clarsimp) fix r :: "('a \ 'a) set" and R assume *: "finite R" and **: "r \ R" - and ***: "Well_order r" and ****: "\r\R. Well_order r" - and IH: "R \ {} \ (\p. isOmax R p)" + and ***: "Well_order r" and ****: "\r\R. Well_order r" + and IH: "R \ {} \ (\p. isOmax R p)" let ?R' = "insert r R" show "\p'. (isOmax ?R' p')" proof(cases "R = {}") - assume Case1: "R = {}" + case True thus ?thesis unfolding isOmax_def using *** - by (simp add: ordLeq_reflexive) + by (simp add: ordLeq_reflexive) next - assume Case2: "R \ {}" + case False then obtain p where p: "isOmax R p" using IH by auto hence 1: "Well_order p" using **** unfolding isOmax_def by simp {assume Case21: "r \o p" - hence "isOmax ?R' p" using p unfolding isOmax_def by simp - hence ?thesis by auto + hence "isOmax ?R' p" using p unfolding isOmax_def by simp + hence ?thesis by auto } moreover {assume Case22: "p \o r" - {fix r' assume "r' \ ?R'" - moreover - {assume "r' \ R" - hence "r' \o p" using p unfolding isOmax_def by simp - hence "r' \o r" using Case22 by(rule ordLeq_transitive) + {fix r' assume "r' \ ?R'" + moreover + {assume "r' \ R" + hence "r' \o p" using p unfolding isOmax_def by simp + hence "r' \o r" using Case22 by(rule ordLeq_transitive) + } + moreover have "r \o r" using *** by(rule ordLeq_reflexive) + ultimately have "r' \o r" by auto } - moreover have "r \o r" using *** by(rule ordLeq_reflexive) - ultimately have "r' \o r" by auto - } - hence "isOmax ?R' r" unfolding isOmax_def by simp - hence ?thesis by auto + hence "isOmax ?R' r" unfolding isOmax_def by simp + hence ?thesis by auto } moreover have "r \o p \ p \o r" - using 1 *** ordLeq_total by auto + using 1 *** ordLeq_total by auto ultimately show ?thesis by blast qed qed @@ -335,120 +270,86 @@ qed lemma omax_isOmax: -assumes "finite R" and "R \ {}" and "\ r \ R. Well_order r" -shows "isOmax R (omax R)" -unfolding omax_def using assms -by(simp add: exists_isOmax someI_ex) + assumes "finite R" and "R \ {}" and "\ r \ R. Well_order r" + shows "isOmax R (omax R)" + unfolding omax_def using assms + by(simp add: exists_isOmax someI_ex) lemma omax_in: -assumes "finite R" and "R \ {}" and "\ r \ R. Well_order r" -shows "omax R \ R" -using assms omax_isOmax unfolding isOmax_def by blast + assumes "finite R" and "R \ {}" and "\ r \ R. Well_order r" + shows "omax R \ R" + using assms omax_isOmax unfolding isOmax_def by blast lemma Well_order_omax: -assumes "finite R" and "R \ {}" and "\r\R. Well_order r" -shows "Well_order (omax R)" -using assms apply - apply(drule omax_in) by auto + assumes "finite R" and "R \ {}" and "\r\R. Well_order r" + shows "Well_order (omax R)" + using assms omax_in by blast lemma omax_maxim: -assumes "finite R" and "\ r \ R. Well_order r" and "r \ R" -shows "r \o omax R" -using assms omax_isOmax unfolding isOmax_def by blast + assumes "finite R" and "\ r \ R. Well_order r" and "r \ R" + shows "r \o omax R" + using assms omax_isOmax unfolding isOmax_def by blast lemma omax_ordLeq: -assumes "finite R" and "R \ {}" and *: "\ r \ R. r \o p" -shows "omax R \o p" -proof- - have "\ r \ R. Well_order r" using * unfolding ordLeq_def by simp - thus ?thesis using assms omax_in by auto -qed + assumes "finite R" and "R \ {}" and "\ r \ R. r \o p" + shows "omax R \o p" + by (meson assms omax_in ordLeq_Well_order_simp) lemma omax_ordLess: -assumes "finite R" and "R \ {}" and *: "\ r \ R. r r \ R. Well_order r" using * unfolding ordLess_def by simp - thus ?thesis using assms omax_in by auto -qed + assumes "finite R" and "R \ {}" and "\ r \ R. r r \ R. Well_order r" -and "omax R \o p" and "r \ R" -shows "r \o p" -using assms omax_maxim[of R r] apply simp -using ordLeq_transitive by blast + assumes "finite R" and "\ r \ R. Well_order r" + and "omax R \o p" and "r \ R" + shows "r \o p" + by (meson assms omax_maxim ordLeq_transitive) lemma omax_ordLess_elim: -assumes "finite R" and "\ r \ R. Well_order r" -and "omax R R" -shows "r r \ R. Well_order r" + and "omax R R" + shows "r r \ R. Well_order r" -and "r \ R" and "p \o r" -shows "p \o omax R" -using assms omax_maxim[of R r] apply simp -using ordLeq_transitive by blast + assumes "finite R" and "\ r \ R. Well_order r" + and "r \ R" and "p \o r" + shows "p \o omax R" + by (meson assms omax_maxim ordLeq_transitive) lemma ordLess_omax: -assumes "finite R" and "\ r \ R. Well_order r" -and "r \ R" and "p r \ R. Well_order r" + and "r \ R" and "p {}" and Well_R: "\ r \ R. Well_order r" -and LEQ: "\ p \ P. \ r \ R. p \o r" -shows "omax P \o omax R" -proof- - let ?mp = "omax P" let ?mr = "omax R" - {fix p assume "p \ P" - then obtain r where r: "r \ R" and "p \o r" - using LEQ by blast - moreover have "r <=o ?mr" - using r R Well_R omax_maxim by blast - ultimately have "p <=o ?mr" - using ordLeq_transitive by blast - } - thus "?mp <=o ?mr" - using NE_P P using omax_ordLeq by blast -qed + assumes P: "finite P" and R: "finite R" + and NE_P: "P \ {}" and Well_R: "\ r \ R. Well_order r" + and LEQ: "\ p \ P. \ r \ R. p \o r" + shows "omax P \o omax R" + by (meson LEQ NE_P P R Well_R omax_ordLeq ordLeq_omax) lemma omax_ordLess_mono: -assumes P: "finite P" and R: "finite R" -and NE_P: "P \ {}" and Well_R: "\ r \ R. Well_order r" -and LEQ: "\ p \ P. \ r \ R. p P" - then obtain r where r: "r \ R" and "p {}" and Well_R: "\ r \ R. Well_order r" + and LEQ: "\ p \ P. \ r \ R. p Limit and succesor ordinals\ lemma embed_underS2: -assumes r: "Well_order r" and g: "embed r s g" and a: "a \ Field r" -shows "g ` underS r a = underS s (g a)" + assumes r: "Well_order r" and g: "embed r s g" and a: "a \ Field r" + shows "g ` underS r a = underS s (g a)" by (meson a bij_betw_def embed_underS g r) lemma bij_betw_insert: -assumes "b \ A" and "f b \ A'" and "bij_betw f A A'" -shows "bij_betw f (insert b A) (insert (f b) A')" -using notIn_Un_bij_betw[OF assms] by auto + assumes "b \ A" and "f b \ A'" and "bij_betw f A A'" + shows "bij_betw f (insert b A) (insert (f b) A')" + using notIn_Un_bij_betw[OF assms] by auto context wo_rel begin @@ -459,90 +360,80 @@ by (induct rule: well_order_induct) (rule assms, simp add: underS_def) lemma suc_underS: -assumes B: "B \ Field r" and A: "AboveS B \ {}" and b: "b \ B" -shows "b \ underS (suc B)" -using suc_AboveS[OF B A] b unfolding underS_def AboveS_def by auto + assumes B: "B \ Field r" and A: "AboveS B \ {}" and b: "b \ B" + shows "b \ underS (suc B)" + using suc_AboveS[OF B A] b unfolding underS_def AboveS_def by auto lemma underS_supr: -assumes bA: "b \ underS (supr A)" and A: "A \ Field r" -shows "\ a \ A. b \ underS a" -proof(rule ccontr, auto) + assumes bA: "b \ underS (supr A)" and A: "A \ Field r" + shows "\ a \ A. b \ underS a" +proof(rule ccontr, simp) have bb: "b \ Field r" using bA unfolding underS_def Field_def by auto assume "\a\A. b \ underS a" hence 0: "\a \ A. (a,b) \ r" using A bA unfolding underS_def - by simp (metis REFL in_mono max2_def max2_greater refl_on_domain) - have "(supr A, b) \ r" apply(rule supr_least[OF A bb]) using 0 by auto + by simp (metis REFL in_mono max2_def max2_greater refl_on_domain) + have "(supr A, b) \ r" + by (simp add: "0" A bb supr_least) thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD) qed lemma underS_suc: -assumes bA: "b \ underS (suc A)" and A: "A \ Field r" -shows "\ a \ A. b \ under a" -proof(rule ccontr, auto) + assumes bA: "b \ underS (suc A)" and A: "A \ Field r" + shows "\ a \ A. b \ under a" +proof(rule ccontr, simp) have bb: "b \ Field r" using bA unfolding underS_def Field_def by auto assume "\a\A. b \ under a" - hence 0: "\a \ A. a \ underS b" using A bA unfolding underS_def - by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq under_def rev_subsetD) - have "(suc A, b) \ r" apply(rule suc_least[OF A bb]) using 0 unfolding underS_def by auto + hence 0: "\a \ A. a \ underS b" using A bA + by (metis bb in_mono max2_def max2_greater mem_Collect_eq underS_I under_def) + have "(suc A, b) \ r" + by (metis "0" A bb suc_least underS_E) thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD) qed lemma (in wo_rel) in_underS_supr: -assumes j: "j \ underS i" and i: "i \ A" and A: "A \ Field r" and AA: "Above A \ {}" -shows "j \ underS (supr A)" + assumes j: "j \ underS i" and i: "i \ A" and A: "A \ Field r" and AA: "Above A \ {}" + shows "j \ underS (supr A)" proof- have "(i,supr A) \ r" using supr_greater[OF A AA i] . thus ?thesis using j unfolding underS_def - by simp (metis REFL TRANS max2_def max2_equals1 refl_on_domain transD) + by simp (metis REFL TRANS max2_def max2_equals1 refl_on_domain transD) qed lemma inj_on_Field: -assumes A: "A \ Field r" and f: "\ a b. \a \ A; b \ A; a \ underS b\ \ f a \ f b" -shows "inj_on f A" -unfolding inj_on_def proof safe - fix a b assume a: "a \ A" and b: "b \ A" and fab: "f a = f b" - {assume "a \ underS b" - hence False using f[OF a b] fab by auto - } - moreover - {assume "b \ underS a" - hence False using f[OF b a] fab by auto - } - ultimately show "a = b" using TOTALS A a b unfolding underS_def by auto -qed + assumes A: "A \ Field r" and f: "\ a b. \a \ A; b \ A; a \ underS b\ \ f a \ f b" + shows "inj_on f A" + by (smt (verit) A f in_notinI inj_on_def subsetD underS_I) lemma ofilter_init_seg_of: -assumes "ofilter F" -shows "Restr r F initial_segment_of r" -using assms unfolding ofilter_def init_seg_of_def under_def by auto + assumes "ofilter F" + shows "Restr r F initial_segment_of r" + using assms unfolding ofilter_def init_seg_of_def under_def by auto lemma underS_init_seg_of_Collect: -assumes "\j1 j2. \j2 \ underS i; (j1, j2) \ r\ \ R j1 initial_segment_of R j2" -shows "{R j |j. j \ underS i} \ Chains init_seg_of" -unfolding Chains_def proof safe + assumes "\j1 j2. \j2 \ underS i; (j1, j2) \ r\ \ R j1 initial_segment_of R j2" + shows "{R j |j. j \ underS i} \ Chains init_seg_of" + unfolding Chains_def proof safe fix j ja assume jS: "j \ underS i" and jaS: "ja \ underS i" - and init: "(R ja, R j) \ init_seg_of" + and init: "(R ja, R j) \ init_seg_of" hence jja: "{j,ja} \ Field r" and j: "j \ Field r" and ja: "ja \ Field r" - and jjai: "(j,i) \ r" "(ja,i) \ r" - and i: "i \ {j,ja}" unfolding Field_def underS_def by auto + and jjai: "(j,i) \ r" "(ja,i) \ r" + and i: "i \ {j,ja}" unfolding Field_def underS_def by auto have jj: "(j,j) \ r" and jaja: "(ja,ja) \ r" using j ja by (metis in_notinI)+ show "R j initial_segment_of R ja" - using jja init jjai i - by (elim cases_Total3 disjE) (auto elim: cases_Total3 intro!: assms simp: underS_def) + using jja init TOTALS assms jS jaS by auto qed lemma (in wo_rel) Field_init_seg_of_Collect: -assumes "\j1 j2. \j2 \ Field r; (j1, j2) \ r\ \ R j1 initial_segment_of R j2" -shows "{R j |j. j \ Field r} \ Chains init_seg_of" -unfolding Chains_def proof safe + assumes "\j1 j2. \j2 \ Field r; (j1, j2) \ r\ \ R j1 initial_segment_of R j2" + shows "{R j |j. j \ Field r} \ Chains init_seg_of" + unfolding Chains_def proof safe fix j ja assume jS: "j \ Field r" and jaS: "ja \ Field r" - and init: "(R ja, R j) \ init_seg_of" + and init: "(R ja, R j) \ init_seg_of" hence jja: "{j,ja} \ Field r" and j: "j \ Field r" and ja: "ja \ Field r" - unfolding Field_def underS_def by auto + unfolding Field_def underS_def by auto have jj: "(j,j) \ r" and jaja: "(ja,ja) \ r" using j ja by (metis in_notinI)+ show "R j initial_segment_of R ja" - using jja init - by (elim cases_Total3 disjE) (auto elim: cases_Total3 intro!: assms simp: Field_def) + using TOTALS assms init jS jaS by blast qed subsubsection \Successor and limit elements of an ordinal\ @@ -556,77 +447,65 @@ definition "isLim i \ \ isSucc i" lemma zero_smallest[simp]: -assumes "j \ Field r" shows "(zero, j) \ r" -unfolding zero_def -by (metis AboveS_Field assms subset_AboveS_UnderS subset_antisym subset_refl suc_def suc_least_AboveS) + assumes "j \ Field r" shows "(zero, j) \ r" + unfolding zero_def + by (metis AboveS_Field assms subset_AboveS_UnderS subset_antisym subset_refl suc_def suc_least_AboveS) lemma zero_in_Field: assumes "Field r \ {}" shows "zero \ Field r" -using assms unfolding zero_def by (metis Field_ofilter minim_in ofilter_def) + using assms unfolding zero_def by (metis Field_ofilter minim_in ofilter_def) lemma leq_zero_imp[simp]: -"(x, zero) \ r \ x = zero" -by (metis ANTISYM WELL antisymD well_order_on_domain zero_smallest) + "(x, zero) \ r \ x = zero" + by (metis ANTISYM WELL antisymD well_order_on_domain zero_smallest) lemma leq_zero[simp]: -assumes "Field r \ {}" shows "(x, zero) \ r \ x = zero" -using zero_in_Field[OF assms] in_notinI[of x zero] by auto + assumes "Field r \ {}" shows "(x, zero) \ r \ x = zero" + using zero_in_Field[OF assms] in_notinI[of x zero] by auto lemma under_zero[simp]: -assumes "Field r \ {}" shows "under zero = {zero}" -using assms unfolding under_def by auto + assumes "Field r \ {}" shows "under zero = {zero}" + using assms unfolding under_def by auto lemma underS_zero[simp,intro]: "underS zero = {}" -unfolding underS_def by auto + unfolding underS_def by auto lemma isSucc_succ: "aboveS i \ {} \ isSucc (succ i)" -unfolding isSucc_def succ_def by auto + unfolding isSucc_def succ_def by auto lemma succ_in_diff: -assumes "aboveS i \ {}" shows "(i,succ i) \ r \ succ i \ i" -using assms suc_greater[of "{i}"] unfolding succ_def AboveS_def aboveS_def Field_def by auto + assumes "aboveS i \ {}" shows "(i,succ i) \ r \ succ i \ i" + using assms suc_greater[of "{i}"] unfolding succ_def AboveS_def aboveS_def Field_def by auto lemmas succ_in[simp] = succ_in_diff[THEN conjunct1] lemmas succ_diff[simp] = succ_in_diff[THEN conjunct2] lemma succ_in_Field[simp]: -assumes "aboveS i \ {}" shows "succ i \ Field r" -using succ_in[OF assms] unfolding Field_def by auto + assumes "aboveS i \ {}" shows "succ i \ Field r" + using succ_in[OF assms] unfolding Field_def by auto lemma succ_not_in: -assumes "aboveS i \ {}" shows "(succ i, i) \ r" -proof - assume 1: "(succ i, i) \ r" - hence "succ i \ Field r \ i \ Field r" unfolding Field_def by auto - hence "(i, succ i) \ r \ succ i \ i" using assms by auto - thus False using 1 by (metis ANTISYM antisymD) -qed + assumes "aboveS i \ {}" shows "(succ i, i) \ r" + by (metis FieldI2 assms max2_equals1 max2_equals2 succ_diff succ_in) lemma not_isSucc_zero: "\ isSucc zero" -proof - assume *: "isSucc zero" - then obtain i where "aboveS i \ {}" and 1: "minim (Field r) = succ i" - unfolding isSucc_def zero_def by auto - hence "succ i \ Field r" by auto - with * show False - by (metis REFL isSucc_def minim_least refl_on_domain - subset_refl succ_in succ_not_in zero_def) -qed + by (metis isSucc_def leq_zero_imp succ_in_diff) lemma isLim_zero[simp]: "isLim zero" by (metis isLim_def not_isSucc_zero) lemma succ_smallest: -assumes "(i,j) \ r" and "i \ j" -shows "(succ i, j) \ r" -unfolding succ_def apply(rule suc_least) -using assms unfolding Field_def by auto + assumes "(i,j) \ r" and "i \ j" + shows "(succ i, j) \ r" + unfolding succ_def apply(rule suc_least) + using assms unfolding Field_def by auto lemma isLim_supr: -assumes f: "i \ Field r" and l: "isLim i" -shows "i = supr (underS i)" + assumes f: "i \ Field r" and l: "isLim i" + shows "i = supr (underS i)" proof(rule equals_supr) fix j assume j: "j \ Field r" and 1: "\ j'. j' \ underS i \ (j',j) \ r" - show "(i,j) \ r" proof(intro in_notinI[OF _ f j], safe) + show "(i,j) \ r" + proof(intro in_notinI[OF _ f j], safe) assume ji: "(j,i) \ r" "j \ i" hence a: "aboveS j \ {}" unfolding aboveS_def by auto hence "i \ succ j" using l unfolding isLim_def isSucc_def by auto @@ -635,17 +514,19 @@ hence "(succ j, j) \ r" using 1 by auto thus False using succ_not_in[OF a] by simp qed -qed(insert f, unfold underS_def Field_def, auto) +qed(use f underS_def Field_def in fastforce)+ definition "pred i \ SOME j. j \ Field r \ aboveS j \ {} \ succ j = i" lemma pred_Field_succ: -assumes "isSucc i" shows "pred i \ Field r \ aboveS (pred i) \ {} \ succ (pred i) = i" + assumes "isSucc i" shows "pred i \ Field r \ aboveS (pred i) \ {} \ succ (pred i) = i" proof- - obtain j where a: "aboveS j \ {}" and i: "i = succ j" using assms unfolding isSucc_def by auto - have 1: "j \ Field r" "j \ i" unfolding Field_def i - using succ_diff[OF a] a unfolding aboveS_def by auto - show ?thesis unfolding pred_def apply(rule someI_ex) using 1 i a by auto + obtain j where j: "aboveS j \ {}" "i = succ j" + using assms unfolding isSucc_def by auto + then obtain "j \ Field r" "j \ i" + by (metis FieldI1 succ_diff succ_in) + then show ?thesis unfolding pred_def + by (metis (mono_tags, lifting) j someI_ex) qed lemmas pred_Field[simp] = pred_Field_succ[THEN conjunct1] @@ -653,165 +534,100 @@ lemmas succ_pred[simp] = pred_Field_succ[THEN conjunct2, THEN conjunct2] lemma isSucc_pred_in: -assumes "isSucc i" shows "(pred i, i) \ r" -proof- - define j where "j = pred i" - have i: "i = succ j" using assms unfolding j_def by simp - have a: "aboveS j \ {}" unfolding j_def using assms by auto - show ?thesis unfolding j_def[symmetric] unfolding i using succ_in[OF a] . -qed + assumes "isSucc i" shows "(pred i, i) \ r" + by (metis assms pred_Field_succ succ_in) lemma isSucc_pred_diff: -assumes "isSucc i" shows "pred i \ i" -by (metis aboveS_pred assms succ_diff succ_pred) + assumes "isSucc i" shows "pred i \ i" + by (metis aboveS_pred assms succ_diff succ_pred) (* todo: pred maximal, pred injective? *) lemma succ_inj[simp]: -assumes "aboveS i \ {}" and "aboveS j \ {}" -shows "succ i = succ j \ i = j" -proof safe - assume s: "succ i = succ j" - {assume "i \ j" and "(i,j) \ r" - hence "(succ i, j) \ r" using assms by (metis succ_smallest) - hence False using s assms by (metis succ_not_in) - } - moreover - {assume "i \ j" and "(j,i) \ r" - hence "(succ j, i) \ r" using assms by (metis succ_smallest) - hence False using s assms by (metis succ_not_in) - } - ultimately show "i = j" by (metis TOTALS WELL assms(1) assms(2) succ_in_diff well_order_on_domain) -qed + assumes "aboveS i \ {}" and "aboveS j \ {}" + shows "succ i = succ j \ i = j" + by (metis FieldI1 assms succ_def succ_in supr_under under_underS_suc) lemma pred_succ[simp]: -assumes "aboveS j \ {}" shows "pred (succ j) = j" -unfolding pred_def apply(rule some_equality) -using assms apply(force simp: Field_def aboveS_def) -by (metis assms succ_inj) + assumes "aboveS j \ {}" shows "pred (succ j) = j" + using assms isSucc_def pred_Field_succ succ_inj by blast lemma less_succ[simp]: -assumes "aboveS i \ {}" -shows "(j, succ i) \ r \ (j,i) \ r \ j = succ i" -apply safe - apply (metis WELL assms in_notinI well_order_on_domain suc_singl_pred succ_def succ_in_diff) - apply (metis (opaque_lifting, full_types) REFL TRANS assms max2_def max2_equals1 refl_on_domain succ_in_Field succ_not_in transD) - apply (metis assms in_notinI succ_in_Field) -done + assumes "aboveS i \ {}" + shows "(j, succ i) \ r \ (j,i) \ r \ j = succ i" + by (metis FieldI1 assms in_notinI max2_equals1 max2_equals2 max2_iff succ_in succ_smallest) lemma underS_succ[simp]: -assumes "aboveS i \ {}" -shows "underS (succ i) = under i" -unfolding underS_def under_def by (auto simp: assms succ_not_in) + assumes "aboveS i \ {}" + shows "underS (succ i) = under i" + unfolding underS_def under_def by (auto simp: assms succ_not_in) lemma succ_mono: -assumes "aboveS j \ {}" and "(i,j) \ r" -shows "(succ i, succ j) \ r" -by (metis (full_types) assms less_succ succ_smallest) + assumes "aboveS j \ {}" and "(i,j) \ r" + shows "(succ i, succ j) \ r" + by (metis (full_types) assms less_succ succ_smallest) lemma under_succ[simp]: -assumes "aboveS i \ {}" -shows "under (succ i) = insert (succ i) (under i)" -using less_succ[OF assms] unfolding under_def by auto + assumes "aboveS i \ {}" + shows "under (succ i) = insert (succ i) (under i)" + using less_succ[OF assms] unfolding under_def by auto definition mergeSL :: "('a \ 'b \ 'b) \ (('a \ 'b) \ 'a \ 'b) \ ('a \ 'b) \ 'a \ 'b" -where -"mergeSL S L f i \ - if isSucc i then S (pred i) (f (pred i)) - else L f i" + where + "mergeSL S L f i \ if isSucc i then S (pred i) (f (pred i)) else L f i" subsubsection \Well-order recursion with (zero), succesor, and limit\ definition worecSL :: "('a \ 'b \ 'b) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" -where "worecSL S L \ worec (mergeSL S L)" + where "worecSL S L \ worec (mergeSL S L)" definition "adm_woL L \ \f g i. isLim i \ (\j\underS i. f j = g j) \ L f i = L g i" -lemma mergeSL: -assumes "adm_woL L" shows "adm_wo (mergeSL S L)" -unfolding adm_wo_def proof safe - fix f g :: "'a => 'b" and i :: 'a - assume 1: "\j\underS i. f j = g j" - show "mergeSL S L f i = mergeSL S L g i" - proof(cases "isSucc i") - case True - hence "pred i \ underS i" unfolding underS_def using isSucc_pred_in isSucc_pred_diff by auto - thus ?thesis using True 1 unfolding mergeSL_def by auto - next - case False hence "isLim i" unfolding isLim_def by auto - thus ?thesis using assms False 1 unfolding mergeSL_def adm_woL_def by auto - qed -qed +lemma mergeSL: "adm_woL L \adm_wo (mergeSL S L)" + unfolding adm_wo_def adm_woL_def isLim_def + by (smt (verit, ccfv_threshold) isSucc_pred_diff isSucc_pred_in mergeSL_def underS_I) lemma worec_fixpoint1: "adm_wo H \ worec H i = H (worec H) i" -by (metis worec_fixpoint) + by (metis worec_fixpoint) lemma worecSL_isSucc: -assumes a: "adm_woL L" and i: "isSucc i" -shows "worecSL S L i = S (pred i) (worecSL S L (pred i))" -proof- - let ?H = "mergeSL S L" - have "worecSL S L i = ?H (worec ?H) i" - unfolding worecSL_def using worec_fixpoint1[OF mergeSL[OF a]] . - also have "... = S (pred i) (worecSL S L (pred i))" - unfolding worecSL_def mergeSL_def using i by simp - finally show ?thesis . -qed + assumes a: "adm_woL L" and i: "isSucc i" + shows "worecSL S L i = S (pred i) (worecSL S L (pred i))" + by (metis a i mergeSL mergeSL_def worecSL_def worec_fixpoint) lemma worecSL_succ: -assumes a: "adm_woL L" and i: "aboveS j \ {}" -shows "worecSL S L (succ j) = S j (worecSL S L j)" -proof- - define i where "i = succ j" - have i: "isSucc i" by (metis i i_def isSucc_succ) - have ij: "j = pred i" unfolding i_def using assms by simp - have 0: "succ (pred i) = i" using i by simp - show ?thesis unfolding ij using worecSL_isSucc[OF a i] unfolding 0 . -qed + assumes a: "adm_woL L" and i: "aboveS j \ {}" + shows "worecSL S L (succ j) = S j (worecSL S L j)" + by (simp add: a i isSucc_succ worecSL_isSucc) lemma worecSL_isLim: -assumes a: "adm_woL L" and i: "isLim i" -shows "worecSL S L i = L (worecSL S L) i" -proof- - let ?H = "mergeSL S L" - have "worecSL S L i = ?H (worec ?H) i" - unfolding worecSL_def using worec_fixpoint1[OF mergeSL[OF a]] . - also have "... = L (worecSL S L) i" - using i unfolding worecSL_def mergeSL_def isLim_def by simp - finally show ?thesis . -qed + assumes a: "adm_woL L" and i: "isLim i" + shows "worecSL S L i = L (worecSL S L) i" + by (metis a i isLim_def mergeSL mergeSL_def worecSL_def worec_fixpoint) definition worecZSL :: "'b \ ('a \ 'b \ 'b) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" -where "worecZSL Z S L \ worecSL S (\ f a. if a = zero then Z else L f a)" + where "worecZSL Z S L \ worecSL S (\ f a. if a = zero then Z else L f a)" lemma worecZSL_zero: -assumes a: "adm_woL L" -shows "worecZSL Z S L zero = Z" -proof- - let ?L = "\ f a. if a = zero then Z else L f a" - have "worecZSL Z S L zero = ?L (worecZSL Z S L) zero" - unfolding worecZSL_def apply(rule worecSL_isLim) - using assms unfolding adm_woL_def by auto - also have "... = Z" by simp - finally show ?thesis . -qed + assumes a: "adm_woL L" + shows "worecZSL Z S L zero = Z" + by (smt (verit, best) adm_woL_def assms isLim_zero worecSL_isLim worecZSL_def) lemma worecZSL_succ: -assumes a: "adm_woL L" and i: "aboveS j \ {}" -shows "worecZSL Z S L (succ j) = S j (worecZSL Z S L j)" -unfolding worecZSL_def apply(rule worecSL_succ) -using assms unfolding adm_woL_def by auto + assumes a: "adm_woL L" and i: "aboveS j \ {}" + shows "worecZSL Z S L (succ j) = S j (worecZSL Z S L j)" + unfolding worecZSL_def + by (smt (verit, best) a adm_woL_def i worecSL_succ) lemma worecZSL_isLim: -assumes a: "adm_woL L" and "isLim i" and "i \ zero" -shows "worecZSL Z S L i = L (worecZSL Z S L) i" + assumes a: "adm_woL L" and "isLim i" and "i \ zero" + shows "worecZSL Z S L i = L (worecZSL Z S L) i" proof- let ?L = "\ f a. if a = zero then Z else L f a" have "worecZSL Z S L i = ?L (worecZSL Z S L) i" - unfolding worecZSL_def apply(rule worecSL_isLim) - using assms unfolding adm_woL_def by auto - also have "... = L (worecZSL Z S L) i" using assms by simp + unfolding worecZSL_def by (smt (verit, best) adm_woL_def assms worecSL_isLim) + also have "\ = L (worecZSL Z S L) i" using assms by simp finally show ?thesis . qed @@ -819,70 +635,54 @@ subsubsection \Well-order succ-lim induction\ lemma ord_cases: -obtains j where "i = succ j" and "aboveS j \ {}" | "isLim i" -by (metis isLim_def isSucc_def) + obtains j where "i = succ j" and "aboveS j \ {}" | "isLim i" + by (metis isLim_def isSucc_def) lemma well_order_inductSL[case_names Suc Lim]: -assumes SUCC: "\i. \aboveS i \ {}; P i\ \ P (succ i)" and -LIM: "\i. \isLim i; \j. j \ underS i \ P j\ \ P i" -shows "P i" + assumes "\i. \aboveS i \ {}; P i\ \ P (succ i)" "\i. \isLim i; \j. j \ underS i \ P j\ \ P i" + shows "P i" proof(induction rule: well_order_induct) - fix i assume 0: "\j. j \ i \ (j, i) \ r \ P j" - show "P i" proof(cases i rule: ord_cases) - fix j assume i: "i = succ j" and j: "aboveS j \ {}" - hence "j \ i \ (j, i) \ r" by (metis succ_diff succ_in) - hence 1: "P j" using 0 by simp - show "P i" unfolding i apply(rule SUCC) using 1 j by auto - qed(insert 0 LIM, unfold underS_def, auto) + case (1 x) + then show ?case + by (metis assms ord_cases succ_diff succ_in underS_E) qed lemma well_order_inductZSL[case_names Zero Suc Lim]: -assumes ZERO: "P zero" -and SUCC: "\i. \aboveS i \ {}; P i\ \ P (succ i)" and -LIM: "\i. \isLim i; i \ zero; \j. j \ underS i \ P j\ \ P i" -shows "P i" -apply(induction rule: well_order_inductSL) using assms by auto + assumes "P zero" + and "\i. \aboveS i \ {}; P i\ \ P (succ i)" and + "\i. \isLim i; i \ zero; \j. j \ underS i \ P j\ \ P i" + shows "P i" + by (metis assms well_order_inductSL) (* Succesor and limit ordinals *) definition "isSuccOrd \ \ j \ Field r. \ i \ Field r. (i,j) \ r" definition "isLimOrd \ \ isSuccOrd" lemma isLimOrd_succ: -assumes isLimOrd and "i \ Field r" -shows "succ i \ Field r" -using assms unfolding isLimOrd_def isSuccOrd_def -by (metis REFL in_notinI refl_on_domain succ_smallest) + assumes isLimOrd and "i \ Field r" + shows "succ i \ Field r" + using assms unfolding isLimOrd_def isSuccOrd_def + by (metis REFL in_notinI refl_on_domain succ_smallest) lemma isLimOrd_aboveS: -assumes l: isLimOrd and i: "i \ Field r" -shows "aboveS i \ {}" + assumes l: isLimOrd and i: "i \ Field r" + shows "aboveS i \ {}" proof- obtain j where "j \ Field r" and "(j,i) \ r" - using assms unfolding isLimOrd_def isSuccOrd_def by auto + using assms unfolding isLimOrd_def isSuccOrd_def by auto hence "(i,j) \ r \ j \ i" by (metis i max2_def max2_greater) thus ?thesis unfolding aboveS_def by auto qed lemma succ_aboveS_isLimOrd: -assumes "\ i \ Field r. aboveS i \ {} \ succ i \ Field r" -shows isLimOrd -unfolding isLimOrd_def isSuccOrd_def proof safe - fix j assume j: "j \ Field r" "\i\Field r. (i, j) \ r" - hence "(succ j, j) \ r" using assms by auto - moreover have "aboveS j \ {}" using assms j unfolding aboveS_def by auto - ultimately show False by (metis succ_not_in) -qed + assumes "\ i \ Field r. aboveS i \ {} \ succ i \ Field r" + shows isLimOrd + using assms isLimOrd_def isSuccOrd_def succ_not_in by blast lemma isLim_iff: -assumes l: "isLim i" and j: "j \ underS i" -shows "\ k. k \ underS i \ j \ underS k" -proof- - have a: "aboveS j \ {}" using j unfolding underS_def aboveS_def by auto - show ?thesis apply(rule exI[of _ "succ j"]) apply safe - using assms a unfolding underS_def isLim_def - apply (metis (lifting, full_types) isSucc_def mem_Collect_eq succ_smallest) - by (metis (lifting, full_types) a mem_Collect_eq succ_diff succ_in) -qed + assumes l: "isLim i" and j: "j \ underS i" + shows "\ k. k \ underS i \ j \ underS k" + by (metis Order_Relation.underS_Field empty_iff isLim_supr j l underS_empty underS_supr) end (* context wo_rel *) @@ -903,124 +703,98 @@ definition "oproj r s f \ Field s \ f ` (Field r) \ compat r s f" lemma oproj_in: -assumes "oproj r s f" and "(a,a') \ r" -shows "(f a, f a') \ s" -using assms unfolding oproj_def compat_def by auto + assumes "oproj r s f" and "(a,a') \ r" + shows "(f a, f a') \ s" + using assms unfolding oproj_def compat_def by auto lemma oproj_Field: -assumes f: "oproj r s f" and a: "a \ Field r" -shows "f a \ Field s" -using oproj_in[OF f] a unfolding Field_def by auto + assumes f: "oproj r s f" and a: "a \ Field r" + shows "f a \ Field s" + using oproj_in[OF f] a unfolding Field_def by auto lemma oproj_Field2: -assumes f: "oproj r s f" and a: "b \ Field s" -shows "\ a \ Field r. f a = b" -using assms unfolding oproj_def by auto + assumes f: "oproj r s f" and a: "b \ Field s" + shows "\ a \ Field r. f a = b" + using assms unfolding oproj_def by auto lemma oproj_under: -assumes f: "oproj r s f" and a: "a \ under r a'" -shows "f a \ under s (f a')" -using oproj_in[OF f] a unfolding under_def by auto + assumes f: "oproj r s f" and a: "a \ under r a'" + shows "f a \ under s (f a')" + using oproj_in[OF f] a unfolding under_def by auto (* An ordinal is embedded in another whenever it is embedded as an order (not necessarily as initial segment):*) theorem embedI: -assumes r: "Well_order r" and s: "Well_order s" -and f: "\ a. a \ Field r \ f a \ Field s \ f ` underS r a \ underS s (f a)" -shows "\ g. embed r s g" + assumes r: "Well_order r" and s: "Well_order s" + and f: "\ a. a \ Field r \ f a \ Field s \ f ` underS r a \ underS s (f a)" + shows "\ g. embed r s g" proof- interpret r: wo_rel r by unfold_locales (rule r) interpret s: wo_rel s by unfold_locales (rule s) let ?G = "\ g a. suc s (g ` underS r a)" define g where "g = worec r ?G" have adm: "adm_wo r ?G" unfolding r.adm_wo_def image_def by auto - (* *) + (* *) {fix a assume "a \ Field r" - hence "bij_betw g (under r a) (under s (g a)) \ + hence "bij_betw g (under r a) (under s (g a)) \ g a \ under s (f a)" - proof(induction a rule: r.underS_induct) - case (1 a) - hence a: "a \ Field r" - and IH1a: "\ a1. a1 \ underS r a \ inj_on g (under r a1)" - and IH1b: "\ a1. a1 \ underS r a \ g ` under r a1 = under s (g a1)" - and IH2: "\ a1. a1 \ underS r a \ g a1 \ under s (f a1)" - unfolding underS_def Field_def bij_betw_def by auto - have fa: "f a \ Field s" using f[OF a] by auto - have g: "g a = suc s (g ` underS r a)" - using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by blast - have A0: "g ` underS r a \ Field s" - using IH1b by (metis IH2 image_subsetI in_mono under_Field) - {fix a1 assume a1: "a1 \ underS r a" - from IH2[OF this] have "g a1 \ under s (f a1)" . - moreover have "f a1 \ underS s (f a)" using f[OF a] a1 by auto - ultimately have "g a1 \ underS s (f a)" by (metis s.ANTISYM s.TRANS under_underS_trans) - } - hence "f a \ AboveS s (g ` underS r a)" unfolding AboveS_def - using fa by simp (metis (lifting, full_types) mem_Collect_eq underS_def) - hence A: "AboveS s (g ` underS r a) \ {}" by auto - have B: "\ a1. a1 \ underS r a \ g a1 \ underS s (g a)" - unfolding g apply(rule s.suc_underS[OF A0 A]) by auto - {fix a1 a2 assume a2: "a2 \ underS r a" and 1: "a1 \ underS r a2" - hence a12: "{a1,a2} \ under r a2" and "a1 \ a2" using r.REFL a - unfolding underS_def under_def refl_on_def Field_def by auto - hence "g a1 \ g a2" using IH1a[OF a2] unfolding inj_on_def by auto - hence "g a1 \ underS s (g a2)" using IH1b[OF a2] a12 - unfolding underS_def under_def by auto - } note C = this - have ga: "g a \ Field s" unfolding g using s.suc_inField[OF A0 A] . - have aa: "a \ under r a" - using a r.REFL unfolding under_def underS_def refl_on_def by auto - show ?case proof safe - show "bij_betw g (under r a) (under s (g a))" unfolding bij_betw_def proof safe - show "inj_on g (under r a)" proof(rule r.inj_on_Field) - fix a1 a2 assume "a1 \ under r a" and a2: "a2 \ under r a" and a1: "a1 \ underS r a2" - hence a22: "a2 \ under r a2" and a12: "a1 \ under r a2" "a1 \ a2" - using a r.REFL unfolding under_def underS_def refl_on_def by auto - show "g a1 \ g a2" - proof(cases "a2 = a") - case False hence "a2 \ underS r a" - using a2 unfolding underS_def under_def by auto - from IH1a[OF this] show ?thesis using a12 a22 unfolding inj_on_def by auto - qed(insert B a1, unfold underS_def, auto) - qed(unfold under_def Field_def, auto) - next - fix a1 assume a1: "a1 \ under r a" - show "g a1 \ under s (g a)" - proof(cases "a1 = a") - case True thus ?thesis - using ga s.REFL unfolding refl_on_def under_def by auto - next - case False - hence a1: "a1 \ underS r a" using a1 unfolding underS_def under_def by auto - thus ?thesis using B unfolding underS_def under_def by auto - qed - next - fix b1 assume b1: "b1 \ under s (g a)" - show "b1 \ g ` under r a" - proof(cases "b1 = g a") - case True thus ?thesis using aa by auto - next - case False - hence "b1 \ underS s (g a)" using b1 unfolding underS_def under_def by auto - from s.underS_suc[OF this[unfolded g] A0] - obtain a1 where a1: "a1 \ underS r a" and b1: "b1 \ under s (g a1)" by auto - obtain a2 where "a2 \ under r a1" and b1: "b1 = g a2" using IH1b[OF a1] b1 by auto - hence "a2 \ under r a" using a1 - by (metis r.ANTISYM r.TRANS in_mono underS_subset_under under_underS_trans) - thus ?thesis using b1 by auto - qed - qed - next - have "(g a, f a) \ s" unfolding g proof(rule s.suc_least[OF A0]) - fix b1 assume "b1 \ g ` underS r a" - then obtain a1 where a1: "b1 = g a1" and a1: "a1 \ underS r a" by auto - hence "b1 \ underS s (f a)" - using a by (metis \\a1. a1 \ underS r a \ g a1 \ underS s (f a)\) - thus "f a \ b1 \ (b1, f a) \ s" unfolding underS_def by auto - qed(insert fa, auto) - thus "g a \ under s (f a)" unfolding under_def by auto - qed - qed + proof(induction a rule: r.underS_induct) + case (1 a) + hence a: "a \ Field r" + and IH1a: "\ a1. a1 \ underS r a \ inj_on g (under r a1)" + and IH1b: "\ a1. a1 \ underS r a \ g ` under r a1 = under s (g a1)" + and IH2: "\ a1. a1 \ underS r a \ g a1 \ under s (f a1)" + unfolding underS_def Field_def bij_betw_def by auto + have fa: "f a \ Field s" using f[OF a] by auto + have g: "g a = suc s (g ` underS r a)" + using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by blast + have A0: "g ` underS r a \ Field s" + using IH1b by (metis IH2 image_subsetI in_mono under_Field) + {fix a1 assume a1: "a1 \ underS r a" + from IH2[OF this] have "g a1 \ under s (f a1)" . + moreover have "f a1 \ underS s (f a)" using f[OF a] a1 by auto + ultimately have "g a1 \ underS s (f a)" by (metis s.ANTISYM s.TRANS under_underS_trans) + } + hence "f a \ AboveS s (g ` underS r a)" unfolding AboveS_def + using fa by simp (metis (lifting, full_types) mem_Collect_eq underS_def) + hence A: "AboveS s (g ` underS r a) \ {}" by auto + have B: "\ a1. a1 \ underS r a \ g a1 \ underS s (g a)" + unfolding g apply(rule s.suc_underS[OF A0 A]) by auto + {fix a1 a2 assume a2: "a2 \ underS r a" and 1: "a1 \ underS r a2" + hence a12: "{a1,a2} \ under r a2" and "a1 \ a2" using r.REFL a + unfolding underS_def under_def refl_on_def Field_def by auto + hence "g a1 \ g a2" using IH1a[OF a2] unfolding inj_on_def by auto + hence "g a1 \ underS s (g a2)" using IH1b[OF a2] a12 + unfolding underS_def under_def by auto + } note C = this + have ga: "g a \ Field s" unfolding g using s.suc_inField[OF A0 A] . + have aa: "a \ under r a" + using a r.REFL unfolding under_def underS_def refl_on_def by auto + show ?case proof safe + show "bij_betw g (under r a) (under s (g a))" unfolding bij_betw_def proof safe + show "inj_on g (under r a)" + by (metis A IH1a IH1b a bij_betw_def g ga r s s.suc_greater subsetI wellorders_totally_ordered_aux) + next + fix a1 assume a1: "a1 \ under r a" + show "g a1 \ under s (g a)" + by (metis (mono_tags, lifting) B a1 ga mem_Collect_eq s.in_notinI underS_def under_def) + next + fix b1 assume b1: "b1 \ under s (g a)" + show "b1 \ g ` under r a" + proof(cases "b1 = g a") + case True thus ?thesis using aa by auto + next + case False + show ?thesis + by (metis b1 A IH1a IH1b a bij_betw_def g ga r s s.suc_greater subsetI wellorders_totally_ordered_aux) + qed + qed + next + have "(g a, f a) \ s" unfolding g + using \f a \ s.AboveS (g ` r.underS a)\ s.suc_least_AboveS by blast + thus "g a \ under s (f a)" unfolding under_def by auto + qed + qed } thus ?thesis unfolding embed_def by auto qed @@ -1028,39 +802,39 @@ corollary ordLeq_def2: "r \o s \ Well_order r \ Well_order s \ (\ f. \ a \ Field r. f a \ Field s \ f ` underS r a \ underS s (f a))" -using embed_in_Field[of r s] embed_underS2[of r s] embedI[of r s] -unfolding ordLeq_def by fast + using embed_in_Field[of r s] embed_underS2[of r s] embedI[of r s] + unfolding ordLeq_def by fast lemma iso_oproj: assumes r: "Well_order r" and s: "Well_order s" and f: "iso r s f" shows "oproj r s f" -using assms unfolding oproj_def -by (subst (asm) iso_iff3) (auto simp: bij_betw_def) + using assms unfolding oproj_def + by (metis iso_Field iso_iff3 order_refl) theorem oproj_embed: -assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f" -shows "\ g. embed s r g" + assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f" + shows "\ g. embed s r g" proof (rule embedI[OF s r, of "inv_into (Field r) f"], unfold underS_def, safe) fix b assume "b \ Field s" - thus "inv_into (Field r) f b \ Field r" using oproj_Field2[OF f] by (metis imageI inv_into_into) + thus "inv_into (Field r) f b \ Field r" + using oproj_Field2[OF f] by (metis imageI inv_into_into) next fix a b assume "b \ Field s" "a \ b" "(a, b) \ s" "inv_into (Field r) f a = inv_into (Field r) f b" - with f show False by (auto dest!: inv_into_injective simp: Field_def oproj_def) + with f show False + by (meson FieldI1 in_mono inv_into_injective oproj_def) next fix a b assume *: "b \ Field s" "a \ b" "(a, b) \ s" - { assume "(inv_into (Field r) f a, inv_into (Field r) f b) \ r" + { assume notin: "(inv_into (Field r) f a, inv_into (Field r) f b) \ r" moreover from *(3) have "a \ Field s" unfolding Field_def by auto - with *(1,2) have - "inv_into (Field r) f a \ Field r" "inv_into (Field r) f b \ Field r" - "inv_into (Field r) f a \ inv_into (Field r) f b" - by (auto dest!: oproj_Field2[OF f] inv_into_injective intro!: inv_into_into) + then have "(inv_into (Field r) f b, inv_into (Field r) f a) \ r" + by (meson "*"(1) notin f in_mono inv_into_into oproj_def r wo_rel.in_notinI wo_rel.intro) ultimately have "(inv_into (Field r) f b, inv_into (Field r) f a) \ r" using r by (auto simp: well_order_on_def linear_order_on_def total_on_def) with f[unfolded oproj_def compat_def] *(1) \a \ Field s\ f_inv_into_f[of b f "Field r"] f_inv_into_f[of a f "Field r"] - have "(b, a) \ s" by (metis in_mono) + have "(b, a) \ s" by (metis in_mono) with *(2,3) s have False by (auto simp: well_order_on_def linear_order_on_def partial_order_on_def antisym_def) } thus "(inv_into (Field r) f a, inv_into (Field r) f b) \ r" by blast