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}|"
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) moreoverhave"inj_on ?f ?Y" by (metis (mono_tags, lifting) assms inj_onI mem_Collect_eq) ultimatelyshow"|?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
lemma internalize_card_of_ordLess2: "( |A| B < C. |A| =o |B| \ |B| using internalize_card_of_ordLess[of "A""|C|"] Field_card_of[of C] by auto
lemma Card_order_omax: 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})"
proof- let ?R = "{|A i| | i. i \ I}" have"finite ?R"and"?R \ {}" using assms by auto moreoverhave"\r\?R. Card_order r" using card_of_Card_order by auto ultimatelyshow ?thesis by(rule Card_order_omax) qed
subsection \<open>Cardinals versus set operations on arbitrary sets\<close>
lemma card_of_set_type[simp]: "|UNIV::'a set| using card_of_Pow[of "UNIV::'a set"] by simp
lemma card_of_Un1[simp]: "|A| \o |A \ B| " by fastforce
lemma card_of_diff[simp]: "|A - B| \o |A|" by fastforce
lemma subset_ordLeq_strict: assumes"A \ B" and "|A| shows"A < B" using assms ordLess_irreflexive by blast
corollary subset_ordLeq_diff: assumes"A \ B" and "|A| shows"B - A \ {}" using assms subset_ordLeq_strict by blast
lemma card_of_empty5: "|A| B \ {}" using card_of_empty not_ordLess_ordLeq by blast
lemma Well_order_card_of_empty: "Well_order r \ |{}| \o r" by simp
lemma card_of_UNIV[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
lemma card_of_Pow_mono[simp]: 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 hence"inj_on (image f) (Pow A) \ (image f) ` (Pow A) \ (Pow B)" 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
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
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
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_of_Un2[simp]: 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)"
proof- 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|" 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
lemma card_of_Un_Plus_ordIso2: "|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- have"bij_betw fst (A \ {b}) 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_singl1: "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 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
lemma card_of_Times_assoc: "|(A \ B) \ C| =o |A \ B \ C|" proof - let ?f = "\((a,b),c). (a,(b,c))" have"A \ B \ C \ ?f ` ((A \ B) \ C)" proof fix x assume"x \ A \ B \ C" thenobtain a b c where *: "a \ A" "b \ B" "c \ C" "x = (a, b, c)" by blast let ?x = "((a, b), c)" from * have"?x \ (A \ B) \ C" "x = ?f ?x" by auto 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 thus ?thesis using card_of_ordIso by blast qed
lemma card_of_Times_cong1[simp]: 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)
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
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
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
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
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: 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
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|"
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 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|"
proof- have"\i \ I. |A(f i)| \o |B(f i)|" 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 moreoverhave"|SIGMA i : I. B (f i)| \o |SIGMA j : J. B j|" using INJ IM card_of_Sigma_mono2 by blast ultimatelyshow ?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: 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)"] 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: 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
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|"
proof- let ?L = "\i\I. A i" let ?R = "Sigma I A" have"|?L| <=o |?R|"using card_of_UNION_Sigma . moreoverhave"|?R| <=o |?L|"
proof- have"inj_on snd ?R" unfolding inj_on_def using assms by auto moreoverhave"snd ` ?R <= ?L"by auto ultimatelyshow ?thesis using card_of_ordLeq by blast qed ultimatelyshow ?thesis by(simp add: ordIso_iff_ordLeq) 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: 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
corollary Times_same_infinite_bij_betw: 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
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)"
proof- have"|B| \o |A|" using INJ card_of_ordLeq by blast thus ?thesis using INF NE by (auto simp: card_of_ordIso card_of_Times_infinite) qed
corollary Times_infinite_bij_betw_types: 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
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)"
proof- have"|B| \o |A|" using INJ card_of_ordLeq by blast thus ?thesis using INF by (auto simp: card_of_ordIso) qed
corollary Plus_infinite_bij_betw_types: 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_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
lemma card_of_Un_diff_infinite: assumes INF: "\finite A" and LESS: "|B| shows"|A - B| =o |A|"
proof- obtain C where C_def: "C = A - B"by blast have"|A \ B| =o |A|" using assms ordLeq_iff_ordLess_or_ordIso card_of_Un_infinite by blast moreoverhave"C \ B = A \ B" unfolding C_def by auto ultimatelyhave 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 ultimatelyhave 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" hence"finite B"using card_of_ordLeq_finite 2 by blast hence False using * INF card_of_ordIso_finite 1 by blast
} hence"\finite C" by auto hence"|C| =o |A|" 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"
proof- have"| Field r \ Field p | =o | Field r | \
| Field p \<union> Field r | =o | Field r |" 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 qed
corollary subset_ordLeq_diff_infinite: assumes INF: "\finite B" and SUB: "A \ B" and LESS: "|A| shows"\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| and LESS2: "|B| shows"|A \ B| proof(cases "A = {} \ B = {}") assume Case1: "A = {} \ B = {}" hence"A \ B = {}" by blast moreoverhave"C \ {}" using
LESS1 card_of_empty5 by blast ultimatelyshow ?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: 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
} ultimatelyhave 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 qed
lemma card_of_Times_ordLess_infinite_Field[simp]: assumes INF: "\finite (Field r)" and r: "Card_order r" and
LESS1: "|A| and LESS2: "|B| shows"|A \ B|
proof- let ?C = "Field r" have 1: "r =o |?C| \ |?C| =o r" using r card_of_Field_ordIso
ordIso_symmetric by blast hence"|A| "|B| using LESS1 LESS2 ordLess_ordIso_trans by blast+ hence"|A \ B|
card_of_Times_ordLess_infinite by blast thus ?thesis using 1 ordLess_ordIso_trans by blast qed
lemma ordLeq_finite_Field: assumes"r \o s" and "finite (Field s)" shows"finite (Field r)" by (metis assms card_of_mono2 card_of_ordLeq_infinite)
lemma infinite_card_of_insert: 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) qed
lemma card_of_Un_singl_ordLess_infinite1: assumes"\finite B" and "|A| shows"|{a} Un A| by (metis assms card_of_Un_ordLess_infinite finite.emptyI finite_insert finite_ordLess_infinite2)
lemma card_of_Un_singl_ordLess_infinite: assumes"\finite B" shows"|A| |{a} Un A| using assms card_of_Un_singl_ordLess_infinite1[of B A] using card_of_Un2 ordLeq_ordLess_trans by blast
subsection \<open>Cardinals versus lists\<close>
text\<open>The next is an auxiliary operator, which shall be used for inductive
proofs of facts concerning the cardinality of \<open>List\<close> :\<close>
definition nlists :: "'a set \ nat \ 'a list set" where"nlists A n \ {l. set l \ A \ length l = n}"
lemma lists_UNION_nlists: "lists A = (\n. nlists A n)" 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_eq_set by auto thus ?thesis by (metis card_of_ordLeq) qed
lemma nlists_0: "nlists A 0 = {[]}" unfolding nlists_def by auto
lemma nlists_not_empty: assumes"A \ {}" shows"nlists A n \ {}" proof (induction n) case (Suc n) thenobtain 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 thenshow ?caseby 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 moreoverhave"nlists A (Suc n) \ ?h ` ?B" proof clarify fix l assume"l \ nlists A (Suc n)" hence 1: "length l = Suc n \ set l \ A" unfolding nlists_def by auto thenobtain a and l' where 2: "l = a # l'" by (auto simp: length_Suc_conv) hence"a \ A \ set l' \ A \ length l' = n" using 1 by auto thus"l \ ?h ` ?B" using 2 unfolding nlists_def by auto qed ultimatelyhave"bij_betw ?h ?B (nlists A (Suc n))" 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(induction n) case 0 have"A \ {}" using assms by auto thenshow ?case by (simp add: nlists_0) next case (Suc n) have"|nlists A (Suc n)| =o |A \ (nlists A n)|" 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 Suc assms by auto ultimatelyshow ?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
lemma Union_set_lists: "\(set ` (lists A)) = A" proof -
{ fix a assume"a \ A" hence"set [a] \ A \ a \ set [a]" by auto hence"\l. set l \ A \ a \ set l" by blast } thenshow ?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
lemma map_lists_mono: 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" 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: inj_on_map_lists map_lists_surjective)
lemma card_of_lists_mono[simp]: 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 hence"inj_on (map f) (lists A) \ (map f) ` (lists A) \ (lists B)" 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
lemma card_of_lists_infinite[simp]: 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) 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
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
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
corollary lists_infinite_bij_betw_types: assumes"\finite(UNIV :: 'a set)" shows"\(f::'a list \ 'a). bij f" using assms lists_infinite_bij_betw by fastforce
subsection \<open>Cardinals versus the finite powerset operator\<close>
lemma card_of_Fpow[simp]: "|A| \o |Fpow A|"
proof- let ?h = "\ a. {a}" have"inj_on ?h A \ ?h ` A \ Fpow A" 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
lemma image_Fpow_surjective: 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) thenshow ?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: inj_on_image_Fpow image_Fpow_surjective)
lemma card_of_Fpow_mono[simp]: 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 hence"inj_on (image f) (Fpow A) \ (image f) ` (Fpow A) \ (Fpow B)" 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
lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV" 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})"
proof-
{assume"A \ UNIV" hence "\n. n \ A" by blast moreoverobtain n where n_def: "n = (LEAST n. n \ A)" by blast ultimatelyhave 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 thenhave"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}))" proof(rule iffI) assume"ofilter natLeq A" hence"\m n. n \ A \ m \ n \ m \ A" using natLeq_wo_rel 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: natLeq_ofilter_less natLeq_UNIV_ofilter) qed
lemma natLeq_under_leq: "under natLeq n = {0 .. n}" unfolding under_def natLeq_def by auto
lemma natLeq_on_ofilter_less_eq: "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})" proof(rule iffI) assume *: "wo_rel.ofilter (natLeq_on m) A" hence 1: "A \ {0.. by (auto simp: natLeq_on_wo_rel wo_rel.ofilter_def under_def Field_natLeq_on) hence"\n1 n2. n2 \ A \ n1 \ n2 \ n1 \ A" 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: natLeq_on_ofilter_less_eq) qed
lemma natLeq_on_ofilter_less: assumes"n < m"shows"ofilter (natLeq_on m) {0 .. n}" proof - have"Suc n \ m" using assms by simp thenshow ?thesis using natLeq_on_ofilter_iff by auto qed
lemma natLeq_on_ordLess_natLeq: "natLeq_on n proof - have"well_order natLeq" using Field_natLeq natLeq_Well_order by auto moreoverhave"\n. well_order_on {na. na < n} (natLeq_on n)" using Field_natLeq_on natLeq_on_Well_order by presburger ultimatelyshow ?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
lemma natLeq_on_injective_ordIso: "(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" thenobtain f where"bij_betw f {x. x using Field_natLeq_on unfolding ordIso_def iso_def[abs_def] by auto thus"m = n"using atLeastLessThan_injective2[of f m n] unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast qed
lemma ordIso_natLeq_infinite2: "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)
lemma natLeq_on_Card_order: "Card_order (natLeq_on n)" 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
} thenshow ?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
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
lemma natLeq_on_ordLeq_less_eq: "((natLeq_on m) \o (natLeq_on n)) = (m \ n)" proof assume"natLeq_on m \o natLeq_on n" thenobtain 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 thus"m \ n" using atLeastLessThan_less_eq2 unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast next assume"m \ n" hence"inj_on id {0.. id ` {0.. {0.. hence"|{0..o |{0.. thus"natLeq_on m \o natLeq_on n" using card_of_less ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast qed
lemma natLeq_on_ordLeq_less: "((natLeq_on m) using not_ordLeq_iff_ordLess[OF natLeq_on_Well_order natLeq_on_Well_order, of n m]
natLeq_on_ordLeq_less_eq[of n m] by linarith
lemma ordLeq_natLeq_on_imp_finite: 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: card_of_ordLeq_finite) qed
subsubsection \<open>"Backward compatibility" with the numeric cardinal operator for finite sets\<close>
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
lemma finite_imp_card_of_natLeq_on: 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 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: 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
lemma finite_card_of_iff_card3: assumes FIN: "finite A"and FIN': "finite B" shows"( |A|
proof- have"( |A| o |A| ))" by simp alsohave"\ = (~ (card B \ card A))" using assms by(simp add: finite_card_of_iff_card2) alsohave"\ = (card A < card B)" by auto finallyshow ?thesis . qed
lemma card_Field_natLeq_on: "card(Field(natLeq_on n)) = n" using Field_natLeq_on card_atLeastLessThan by auto
subsection \<open>The successor of a cardinal\<close>
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_mono_ordLess[simp]: assumes CARD: "Card_order r"and CARD': "Card_order r'" shows"(cardSuc r
proof- have 0: "Well_order r \ Well_order r' \ Well_order(cardSuc r) \ Well_order(cardSuc r')" 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 qed
lemma cardSuc_natLeq_on_Suc: "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: *) 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 hence WELL: "Well_order r \ Well_order r' \ Well_order p" 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 hence FIN: "finite (Field r)"by force have"r using CARD unfolding r_def r'_def using cardSuc_greater by blast hence"|Field r| using CARD card_of_Field_ordIso ordIso_ordLess_trans by blast hence LESS: "|Field r| using CARD card_of_Field_ordIso ordLess_ordIso_trans ordIso_symmetric by blast (* Main proof: *) have"r' \o p" using CARD unfolding r_def r'_def p_def using natLeq_on_ordLeq_less cardSuc_ordLess_ordLeq by blast moreoverhave"p \o r'"
proof-
{assume"r' thenobtain 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 thenobtain m where"m \ Suc n" and 3: "f ` (Field r') = {0.. unfolding p_def by (auto simp: natLeq_on_ofilter_iff) hence 4: "m \ 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 moreoverhave"finite(f ` (Field r'))"using 3 finite_atLeastLessThan[of 0 m] by force ultimatelyhave 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 ultimatelyshow ?thesis using ordIso_iff_ordLeq unfolding r'_def p_def by blast qed
lemma card_of_Plus_ordLeq_infinite[simp]: assumes"\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"\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 \<open>Others\<close>
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
lemma underS_under: 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
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)
(* bounded powerset *) definition Bpow where "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
lemma singl_in_Bpow: 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|"
proof- have"inj_on (\ a. {a}) A" unfolding inj_on_def by auto moreoverhave"(\ a. {a}) ` A \ Bpow r A" using singl_in_Bpow[OF assms] by auto ultimatelyshow ?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)
definition Func_option where "Func_option A B \
{f. (\<forall> a. f a \<noteq> None \<longleftrightarrow> a \<in> A) \<and> (\<forall> a \<in> A. case f a of Some b \<Rightarrow> b \<in> B |None \<Rightarrow> True)}"
lemma card_of_Func_option_Func: "|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) 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" by (smt (verit) Func_def eq f g mem_Collect_eq option.inject) qed next show"?F ` Func A B = Func_option A B" proof safe 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+ moreoverhave"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+ qed ultimatelyshow"f \ ?F ` (Func A B)" by blast qed(unfold Func_def Func_option_def, auto) qed qed
(* partial-function space: *) definition Pfunc where "Pfunc A B \
{f. (\<forall>a. f a \<noteq> None \<longrightarrow> a \<in> A) \<and>
(\<forall>a. case f a of None \<Rightarrow> True | Some b \<Rightarrow> b \<in> B)}"
lemma Func_Pfunc: "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)" proof safe fix f assume f: "f \ Pfunc A B" show"f \ (\A'\Pow A. Func_option A' B)" proof (intro UN_I) let ?A' = "{a. f a \ None}" show"?A' \ Pow A" using f unfolding Pow_def Pfunc_def by auto show"f \ Func_option ?A' B" using f unfolding Func_option_def Pfunc_def by auto qed next fix f A' assume "f \ Func_option A' B" and "A' \ A" thus"f \ Pfunc A B" unfolding Func_option_def Pfunc_def by auto 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|"
proof- obtain bb where bb: "bb \ B" using B by auto
define F where [abs_def]: "F f1 a =
(if a \<in> A2 then (if a \<in> A1 then f1 a else bb) else undefined)" for f1 :: "'a \<Rightarrow> '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 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" 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_Pfunc_Pow_Func_option: 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) alsohave"?K \o |Sigma (Pow A) (\ A'. Func_option A' B)|" using card_of_UNION_Sigma . alsohave"|Sigma (Pow A) (\ A'. Func_option A' B)| \o |Pow A \ Func_option A B|" by (simp add: assms card_of_Func_option_mono card_of_Sigma_mono1) finallyshow ?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|"
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) thenobtain 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) 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)
} ultimatelyshow ?thesis by (metis ordIso_ordLeq_trans) qed
lemma Func_mono[simp]: 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 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
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 = "\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)
subsection \<open>Infinite cardinals are limit ordinals\<close>
lemma card_order_infinite_isLimOrd: 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 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 \ Field r" and "\i\Field r. (i, j) \ r" thenshow 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)
lemma Field_init_seg_of[simp]: "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
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| shows"\ 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 thus ?thesis by auto qed
lemma relChain_stabilize: assumes rc: "relChain r As"and AsB: "(\i \ Field r. As i) \ B" and Br: "|B| and ir: "\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)+ 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 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 fix i j assume 1: "(i, j) \ r" "i \ j" and Asij: "As i = As j" 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" 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
} ultimatelyshow 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) thenobtain 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 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) assume"(i, j) \ r" and ijd: "i \ j" 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 thus"i = j"using ij ijd fij f by auto next assume"(j, i) \ r" and ijd: "i \ j" hence rij: "(succ r j, i) \ r" by (metis "0" wo_rel.succ_smallest) hence"As (succ r j) \ As i" using rc unfolding relChain_def by auto thus"j = i"using ij ijd fij f by fastforce qed(insert ij, auto) qed moreoverhave"f ` (Field r) \ B" using f AsBs by auto moreoverhave"|B| using Br cr by (metis card_of_unique ordLess_ordIso_trans) ultimatelyshow False unfolding card_of_ordLess[symmetric] by auto qed
subsection \<open>Regular vs. stable cardinals\<close>
lemma stable_ordIso: 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
text\<open>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.\<close>
lemma infinite_stable_exists: assumes CARD: "\r \ R. Card_order (r::'a rel)" shows"\(A :: (nat + 'a set)set). \<not>finite A \<and> stable |A| \<and> (\<forall>r \<in> R. r <o |A| )"
proof- have"\(A :: (nat + 'a set)set). \<not>finite A \<and> stable |A| \<and> |UNIV::'a set| <o |A|" proof(cases "finite (UNIV::'a set)") case True let ?B = "UNIV::nat set" have"\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 True by simp hence"|UNIV::'a set| by (simp add: finite_ordLess_infinite) hence"|UNIV::'a set| {}|"using card_of_Plus_empty1 ordLess_ordIso_trans by blast ultimatelyshow ?thesis by blast next 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 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 moreoverhave"stable(cardSuc |UNIV::'a set| )" using stable_cardSuc * card_of_Card_order by blast ultimatelyhave"stable |?B|"using stable_ordIso by blast hence 3: "stable |{} <+> ?B|"using stable_ordIso 0 by blast have"|UNIV::'a set| using card_of_Card_order cardSuc_greater by blast moreoverhave"|?B| =o cardSuc |UNIV::'a set|" using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast ultimatelyhave"|UNIV::'a set| using ordIso_symmetric ordLess_ordIso_trans by blast hence"|UNIV::'a set| ?B|"using 0 ordLess_ordIso_trans by blast thus ?thesis using 2 3 by blast qed thus ?thesis using CARD card_of_UNIV2 ordLeq_ordLess_trans by blast qed
corollary infinite_regularCard_exists: assumes CARD: "\r \ R. Card_order (r::'a rel)" shows"\(A :: (nat + 'a set)set). \<not>finite A \<and> regularCard |A| \<and> (\<forall>r \<in> R. r <o |A| )" using infinite_stable_exists[OF CARD] stable_regularCard by (metis Field_card_of card_of_card_order_on)
end
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.52Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
