--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Sat Jun 25 09:50:40 2022 +0000
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Mon Jun 27 15:54:18 2022 +0200
@@ -1,6 +1,7 @@
(* Title: HOL/BNF_Cardinal_Order_Relation.thy
Author: Andrei Popescu, TU Muenchen
- Copyright 2012
+ Author: Jan van Brügge, TU Muenchen
+ Copyright 2012, 2022
Cardinal-order relations as needed by bounded natural functors.
*)
@@ -1425,6 +1426,66 @@
thus ?thesis by (simp only: card_of_cardSuc_finite)
qed
+lemma Field_cardSuc_not_empty:
+assumes "Card_order r"
+shows "Field (cardSuc r) \<noteq> {}"
+proof
+ assume "Field(cardSuc r) = {}"
+ then have "|Field(cardSuc r)| \<le>o r" using assms Card_order_empty[of r] by auto
+ then have "cardSuc r \<le>o r" using assms card_of_Field_ordIso
+ cardSuc_Card_order ordIso_symmetric ordIso_ordLeq_trans by blast
+ then show False using cardSuc_greater not_ordLess_ordLeq assms by blast
+qed
+
+typedef 'a suc = "Field (cardSuc |UNIV :: 'a set| )"
+ using Field_cardSuc_not_empty card_of_Card_order by blast
+
+definition card_suc :: "'a rel \<Rightarrow> 'a suc rel" where
+ "card_suc \<equiv> \<lambda>_. map_prod Abs_suc Abs_suc ` cardSuc |UNIV :: 'a set|"
+
+lemma Field_card_suc: "Field (card_suc r) = UNIV"
+proof -
+ let ?r = "cardSuc |UNIV|"
+ let ?ar = "\<lambda>x. Abs_suc (Rep_suc x)"
+ have 1: "\<And>P. (\<forall>x\<in>Field ?r. P x) = (\<forall>x. P (Rep_suc x))" using Rep_suc_induct Rep_suc by blast
+ have 2: "\<And>P. (\<exists>x\<in>Field ?r. P x) = (\<exists>x. P (Rep_suc x))" using Rep_suc_cases Rep_suc by blast
+ have 3: "\<And>A a b. (a, b) \<in> A \<Longrightarrow> (Abs_suc a, Abs_suc b) \<in> map_prod Abs_suc Abs_suc ` A" unfolding map_prod_def by auto
+ have "\<forall>x\<in>Field ?r. (\<exists>b\<in>Field ?r. (x, b) \<in> ?r) \<or> (\<exists>a\<in>Field ?r. (a, x) \<in> ?r)"
+ unfolding Field_def Range.simps Domain.simps Un_iff by blast
+ then have "\<forall>x. (\<exists>b. (Rep_suc x, Rep_suc b) \<in> ?r) \<or> (\<exists>a. (Rep_suc a, Rep_suc x) \<in> ?r)" unfolding 1 2 .
+ then have "\<forall>x. (\<exists>b. (?ar x, ?ar b) \<in> map_prod Abs_suc Abs_suc ` ?r) \<or> (\<exists>a. (?ar a, ?ar x) \<in> map_prod Abs_suc Abs_suc ` ?r)" using 3 by fast
+ then have "\<forall>x. (\<exists>b. (x, b) \<in> card_suc r) \<or> (\<exists>a. (a, x) \<in> card_suc r)" unfolding card_suc_def Rep_suc_inverse .
+ then show ?thesis unfolding Field_def Domain.simps Range.simps set_eq_iff Un_iff eqTrueI[OF UNIV_I] ex_simps simp_thms .
+qed
+
+lemma card_suc_alt: "card_suc r = dir_image (cardSuc |UNIV :: 'a set| ) Abs_suc"
+ unfolding card_suc_def dir_image_def by auto
+
+lemma cardSuc_Well_order: "Card_order r \<Longrightarrow> Well_order(cardSuc r)"
+ using cardSuc_Card_order unfolding card_order_on_def by blast
+
+lemma cardSuc_ordIso_card_suc:
+ assumes "card_order r"
+ shows "cardSuc r =o card_suc (r :: 'a rel)"
+proof -
+ have "cardSuc (r :: 'a rel) =o cardSuc |UNIV :: 'a set|"
+ using cardSuc_invar_ordIso[THEN iffD2, OF _ card_of_Card_order card_of_unique[OF assms]] assms
+ by (simp add: card_order_on_Card_order)
+ also have "cardSuc |UNIV :: 'a set| =o card_suc (r :: 'a rel)"
+ unfolding card_suc_alt
+ by (rule dir_image_ordIso) (simp_all add: inj_on_def Abs_suc_inject cardSuc_Well_order card_of_Card_order)
+ finally show ?thesis .
+qed
+
+lemma Card_order_card_suc: "card_order r \<Longrightarrow> Card_order (card_suc r)"
+ using cardSuc_Card_order[THEN Card_order_ordIso2[OF _ cardSuc_ordIso_card_suc]] card_order_on_Card_order by blast
+
+lemma card_order_card_suc: "card_order r \<Longrightarrow> card_order (card_suc r)"
+ using Card_order_card_suc arg_cong2[OF Field_card_suc refl, of "card_order_on"] by blast
+
+lemma card_suc_greater: "card_order r \<Longrightarrow> r <o card_suc r"
+ using ordLess_ordIso_trans[OF cardSuc_greater cardSuc_ordIso_card_suc] card_order_on_Card_order by blast
+
lemma card_of_Plus_ordLess_infinite:
assumes INF: "\<not>finite C" and
LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
@@ -1501,6 +1562,27 @@
using assms card_of_Plus_ordLeq_infinite_Field card_of_Un_Plus_ordLeq
ordLeq_transitive by fast
+lemma card_of_Un_ordLess_infinite:
+assumes INF: "\<not>finite C" and
+ LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
+shows "|A \<union> B| <o |C|"
+using assms card_of_Plus_ordLess_infinite card_of_Un_Plus_ordLeq
+ ordLeq_ordLess_trans by blast
+
+lemma card_of_Un_ordLess_infinite_Field:
+assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
+ LESS1: "|A| <o r" and LESS2: "|B| <o r"
+shows "|A Un B| <o r"
+proof-
+ let ?C = "Field r"
+ have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso
+ ordIso_symmetric by blast
+ hence "|A| <o |?C|" "|B| <o |?C|"
+ using LESS1 LESS2 ordLess_ordIso_trans by blast+
+ hence "|A Un B| <o |?C|" using INF
+ card_of_Un_ordLess_infinite by blast
+ thus ?thesis using 1 ordLess_ordIso_trans by blast
+qed
subsection \<open>Regular cardinals\<close>
@@ -1689,4 +1771,228 @@
thus ?thesis using card_of_ordIso by blast
qed
+subsection \<open>Regular vs. stable cardinals\<close>
+
+definition stable :: "'a rel \<Rightarrow> bool"
+where
+"stable r \<equiv> \<forall>(A::'a set) (F :: 'a \<Rightarrow> 'a set).
+ |A| <o r \<and> (\<forall>a \<in> A. |F a| <o r)
+ \<longrightarrow> |SIGMA a : A. F a| <o r"
+
+lemma regularCard_stable:
+ assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and reg: "regularCard r"
+ shows "stable r"
+ unfolding stable_def proof safe
+ fix A :: "'a set" and F :: "'a \<Rightarrow> 'a set" assume A: "|A| <o r" and F: "\<forall>a\<in>A. |F a| <o r"
+ {assume "r \<le>o |Sigma A F|"
+ hence "|Field r| \<le>o |Sigma A F|" using card_of_Field_ordIso[OF cr] ordIso_ordLeq_trans by blast
+ moreover have Fi: "Field r \<noteq> {}" using ir by auto
+ ultimately have "\<exists>f. f ` Sigma A F = Field r" using card_of_ordLeq2[OF Fi] by blast
+ then obtain f where f: "f ` Sigma A F = Field r" by blast
+ have r: "wo_rel r" using cr unfolding card_order_on_def wo_rel_def by auto
+ {fix a assume a: "a \<in> A"
+ define L where "L = {(a,u) | u. u \<in> F a}"
+ have fL: "f ` L \<subseteq> Field r" using f a unfolding L_def by auto
+ have "|L| =o |F a|" unfolding L_def card_of_ordIso[symmetric]
+ apply(rule exI[of _ snd]) unfolding bij_betw_def inj_on_def by (auto simp: image_def)
+ hence "|L| <o r" using F a ordIso_ordLess_trans[of "|L|" "|F a|"] unfolding L_def by auto
+ hence "|f ` L| <o r" using ordLeq_ordLess_trans[OF card_of_image, of "L"] unfolding L_def by auto
+ hence "\<not> cofinal (f ` L) r" using reg fL unfolding regularCard_def
+ apply simp
+ apply (drule not_ordLess_ordIso)
+ by auto
+ then obtain k where k: "k \<in> Field r" and "\<forall> l \<in> L. \<not> (f l \<noteq> k \<and> (k, f l) \<in> r)"
+ unfolding cofinal_def image_def by auto
+ hence "\<exists> k \<in> Field r. \<forall> l \<in> L. (f l, k) \<in> r"
+ using wo_rel.in_notinI[OF r _ _ \<open>k \<in> Field r\<close>] fL unfolding image_subset_iff by fast
+ hence "\<exists> k \<in> Field r. \<forall> u \<in> F a. (f (a,u), k) \<in> r" unfolding L_def by auto
+ }
+ then have x: "\<And>a. a\<in>A \<Longrightarrow> \<exists>k. k \<in> Field r \<and> (\<forall>u\<in>F a. (f (a, u), k) \<in> r)" by blast
+ obtain gg where "\<And>a. a\<in>A \<Longrightarrow> gg a = (SOME k. k \<in> Field r \<and> (\<forall>u\<in>F a. (f (a, u), k) \<in> r))" by simp
+ then have gg: "\<forall>a\<in>A. \<forall>u\<in>F a. (f (a, u), gg a) \<in> r" using someI_ex[OF x] by auto
+ obtain j0 where j0: "j0 \<in> Field r" using Fi by auto
+ define g where [abs_def]: "g a = (if F a \<noteq> {} then gg a else j0)" for a
+ have g: "\<forall> a \<in> A. \<forall> u \<in> F a. (f (a,u),g a) \<in> r" using gg unfolding g_def by auto
+ hence 1: "Field r \<subseteq> (\<Union>a \<in> A. under r (g a))"
+ using f[symmetric] unfolding under_def image_def by auto
+ have gA: "g ` A \<subseteq> Field r" using gg j0 unfolding Field_def g_def by auto
+ moreover have "cofinal (g ` A) r" unfolding cofinal_def proof safe
+ fix i assume "i \<in> Field r"
+ then obtain j where ij: "(i,j) \<in> r" "i \<noteq> j" using cr ir infinite_Card_order_limit by fast
+ hence "j \<in> Field r" using card_order_on_def cr well_order_on_domain by fast
+ then obtain a where a: "a \<in> A" and j: "(j, g a) \<in> r" using 1 unfolding under_def by auto
+ hence "(i, g a) \<in> r" using ij wo_rel.TRANS[OF r] unfolding trans_def by blast
+ moreover have "i \<noteq> g a"
+ using ij j r unfolding wo_rel_def unfolding well_order_on_def linear_order_on_def
+ partial_order_on_def antisym_def by auto
+ ultimately show "\<exists>j\<in>g ` A. i \<noteq> j \<and> (i, j) \<in> r" using a by auto
+ qed
+ ultimately have "|g ` A| =o r" using reg unfolding regularCard_def by auto
+ moreover have "|g ` A| \<le>o |A|" using card_of_image by blast
+ ultimately have False using A using not_ordLess_ordIso ordLeq_ordLess_trans by blast
+ }
+ thus "|Sigma A F| <o r"
+ using cr not_ordLess_iff_ordLeq using card_of_Well_order card_order_on_well_order_on by blast
+qed
+
+lemma stable_regularCard:
+assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and st: "stable r"
+shows "regularCard r"
+unfolding regularCard_def proof safe
+ fix K assume K: "K \<subseteq> Field r" and cof: "cofinal K r"
+ have "|K| \<le>o r" using K card_of_Field_ordIso card_of_mono1 cr ordLeq_ordIso_trans by blast
+ moreover
+ {assume Kr: "|K| <o r"
+ have x: "\<And>a. a \<in> Field r \<Longrightarrow> \<exists>b. b \<in> K \<and> a \<noteq> b \<and> (a, b) \<in> r" using cof unfolding cofinal_def by blast
+ then obtain f where "\<And>a. a \<in> Field r \<Longrightarrow> f a = (SOME b. b \<in> K \<and> a \<noteq> b \<and> (a, b) \<in> r)" by simp
+ then have "\<forall>a\<in>Field r. f a \<in> K \<and> a \<noteq> f a \<and> (a, f a) \<in> r" using someI_ex[OF x] by simp
+ hence "Field r \<subseteq> (\<Union>a \<in> K. underS r a)" unfolding underS_def by auto
+ hence "r \<le>o |\<Union>a \<in> K. underS r a|"
+ using cr Card_order_iff_ordLeq_card_of card_of_mono1 ordLeq_transitive by blast
+ also have "|\<Union>a \<in> K. underS r a| \<le>o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma)
+ also
+ {have "\<forall> a \<in> K. |underS r a| <o r" using K card_of_underS[OF cr] subsetD by auto
+ hence "|SIGMA a: K. underS r a| <o r" using st Kr unfolding stable_def by auto
+ }
+ finally have "r <o r" .
+ hence False using ordLess_irreflexive by blast
+ }
+ ultimately show "|K| =o r" using ordLeq_iff_ordLess_or_ordIso by blast
+qed
+
+lemma internalize_card_of_ordLess:
+"( |A| <o r) = (\<exists>B < Field r. |A| =o |B| \<and> |B| <o r)"
+proof
+ assume "|A| <o r"
+ then obtain p where 1: "Field p < Field r \<and> |A| =o p \<and> p <o r"
+ using internalize_ordLess[of "|A|" r] by blast
+ hence "Card_order p" using card_of_Card_order Card_order_ordIso2 by blast
+ hence "|Field p| =o p" using card_of_Field_ordIso by blast
+ hence "|A| =o |Field p| \<and> |Field p| <o r"
+ using 1 ordIso_equivalence ordIso_ordLess_trans by blast
+ thus "\<exists>B < Field r. |A| =o |B| \<and> |B| <o r" using 1 by blast
+next
+ assume "\<exists>B < Field r. |A| =o |B| \<and> |B| <o r"
+ thus "|A| <o r" using ordIso_ordLess_trans by blast
+qed
+
+lemma card_of_Sigma_cong1:
+assumes "\<forall>i \<in> I. |A i| =o |B i|"
+shows "|SIGMA i : I. A i| =o |SIGMA i : I. B i|"
+using assms by (auto simp add: card_of_Sigma_mono1 ordIso_iff_ordLeq)
+
+lemma card_of_Sigma_cong2:
+assumes "bij_betw f (I::'i set) (J::'j set)"
+shows "|SIGMA i : I. (A::'j \<Rightarrow> '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 = (\<lambda>(i::'i,a::'a). (f i,a))" by blast
+ have "bij_betw u ?LEFT ?RIGHT"
+ using assms unfolding u_def bij_betw_def inj_on_def by auto
+ thus ?thesis using card_of_ordIso by blast
+qed
+
+lemma card_of_Sigma_cong:
+assumes BIJ: "bij_betw f I J" and
+ ISO: "\<forall>j \<in> J. |A j| =o |B j|"
+shows "|SIGMA i : I. A (f i)| =o |SIGMA j : J. B j|"
+proof-
+ have "\<forall>i \<in> I. |A(f i)| =o |B(f i)|"
+ using ISO BIJ unfolding bij_betw_def by blast
+ hence "|SIGMA i : I. A (f i)| =o |SIGMA i : I. B (f i)|" by (rule card_of_Sigma_cong1)
+ moreover have "|SIGMA i : I. B (f i)| =o |SIGMA j : J. B j|"
+ using BIJ card_of_Sigma_cong2 by blast
+ ultimately show ?thesis using ordIso_transitive by blast
+qed
+
+(* Note that below the types of A and F are now unconstrained: *)
+lemma stable_elim:
+assumes ST: "stable r" and A_LESS: "|A| <o r" and
+ F_LESS: "\<And> a. a \<in> A \<Longrightarrow> |F a| <o r"
+shows "|SIGMA a : A. F a| <o r"
+proof-
+ obtain A' where 1: "A' < Field r \<and> |A'| <o r" and 2: " |A| =o |A'|"
+ using internalize_card_of_ordLess[of A r] A_LESS by blast
+ then obtain G where 3: "bij_betw G A' A"
+ using card_of_ordIso ordIso_symmetric by blast
+ (* *)
+ {fix a assume "a \<in> A"
+ hence "\<exists>B'. B' \<le> Field r \<and> |F a| =o |B'| \<and> |B'| <o r"
+ using internalize_card_of_ordLess[of "F a" r] F_LESS by blast
+ }
+ then obtain F' where
+ temp: "\<forall>a \<in> A. F' a \<le> Field r \<and> |F a| =o |F' a| \<and> |F' a| <o r"
+ using bchoice[of A "\<lambda> a B'. B' \<le> Field r \<and> |F a| =o |B'| \<and> |B'| <o r"] by blast
+ hence 4: "\<forall>a \<in> A. F' a \<le> Field r \<and> |F' a| <o r" by auto
+ have 5: "\<forall>a \<in> A. |F' a| =o |F a|" using temp ordIso_symmetric by auto
+ (* *)
+ have "\<forall>a' \<in> A'. F'(G a') \<le> Field r \<and> |F'(G a')| <o r"
+ using 3 4 bij_betw_ball[of G A' A] by auto
+ hence "|SIGMA a' : A'. F'(G a')| <o r"
+ using ST 1 unfolding stable_def by auto
+ moreover have "|SIGMA a' : A'. F'(G a')| =o |SIGMA a : A. F a|"
+ using card_of_Sigma_cong[of G A' A F' F] 5 3 by blast
+ ultimately show ?thesis using ordIso_symmetric ordIso_ordLess_trans by blast
+qed
+
+lemma stable_natLeq: "stable natLeq"
+proof(unfold stable_def, safe)
+ fix A :: "'a set" and F :: "'a \<Rightarrow> 'a set"
+ assume "|A| <o natLeq" and "\<forall>a\<in>A. |F a| <o natLeq"
+ hence "finite A \<and> (\<forall>a \<in> 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 | <o natLeq"
+ by (auto simp add: finite_iff_ordLess_natLeq)
+qed
+
+corollary regularCard_natLeq: "regularCard natLeq"
+using stable_regularCard[OF natLeq_Card_order _ stable_natLeq] Field_natLeq by simp
+
+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 \<Rightarrow> 'b set"
+ assume "|A| <o r'" and "\<forall>a \<in> A. |F a| <o r'"
+ hence "( |A| <o r) \<and> (\<forall>a \<in> A. |F a| <o r)"
+ using ISO ordLess_ordIso_trans by blast
+ hence "|SIGMA a : A. F a| <o r" using assms stable_elim by blast
+ thus "|SIGMA a : A. F a| <o r'"
+ using ISO ordIso_symmetric ordLess_ordIso_trans by blast
+qed
+
+lemma stable_UNION:
+assumes ST: "stable r" and A_LESS: "|A| <o r" and
+ F_LESS: "\<And> a. a \<in> A \<Longrightarrow> |F a| <o r"
+shows "|\<Union>a \<in> A. F a| <o r"
+proof-
+ have "|\<Union>a \<in> A. F a| \<le>o |SIGMA a : A. F a|"
+ using card_of_UNION_Sigma by blast
+ thus ?thesis using assms stable_elim ordLeq_ordLess_trans by blast
+qed
+
+corollary card_of_UNION_ordLess_infinite:
+assumes INF: "stable |B|" and
+ LEQ_I: "|I| <o |B|" and LEQ: "\<forall>i \<in> I. |A i| <o |B|"
+shows "|\<Union>i \<in> I. A i| <o |B|"
+ using assms stable_UNION by blast
+
+corollary card_of_UNION_ordLess_infinite_Field:
+assumes ST: "stable r" and r: "Card_order r" and
+ LEQ_I: "|I| <o r" and LEQ: "\<forall>i \<in> I. |A i| <o r"
+shows "|\<Union>i \<in> I. A i| <o r"
+proof-
+ let ?B = "Field r"
+ have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso
+ ordIso_symmetric by blast
+ hence "|I| <o |?B|" "\<forall>i \<in> I. |A i| <o |?B|"
+ using LEQ_I LEQ ordLess_ordIso_trans by blast+
+ moreover have "stable |?B|" using stable_ordIso1 ST 1 by blast
+ ultimately have "|\<Union>i \<in> I. A i| <o |?B|" using LEQ
+ card_of_UNION_ordLess_infinite by blast
+ thus ?thesis using 1 ordLess_ordIso_trans by blast
+qed
+
end