diff --git a/thys/Delta_System_Lemma/Cardinal_Library.thy b/thys/Delta_System_Lemma/Cardinal_Library.thy --- a/thys/Delta_System_Lemma/Cardinal_Library.thy +++ b/thys/Delta_System_Lemma/Cardinal_Library.thy @@ -1,708 +1,708 @@ section\Cardinal Arithmetic under Choice\label{sec:cardinal-lib}\ theory Cardinal_Library imports ZF_Library ZF.Cardinal_AC begin text\This theory includes results on cardinalities that depend on $\AC$\ subsection\Results on cardinal exponentiation\ text\Non trivial instances of cardinal exponentiation require that the relevant function spaces are well-ordered, hence this implies a strong use of choice.\ lemma cexp_eqpoll_cong: assumes "A \ A'" "B \ B'" shows "A\<^bsup>\B\<^esup> = A'\<^bsup>\B'\<^esup>" unfolding cexp_def using cardinal_eqpoll_iff function_space_eqpoll_cong assms by simp lemma cexp_cexp_cmult: "(\\<^bsup>\\1\<^esup>)\<^bsup>\\2\<^esup> = \\<^bsup>\\2 \ \1\<^esup>" proof - have "(\\<^bsup>\\1\<^esup>)\<^bsup>\\2\<^esup> = (\1 \ \)\<^bsup>\\2\<^esup>" using cardinal_eqpoll by (intro cexp_eqpoll_cong) (simp_all add:cexp_def) also have " \ = \\<^bsup>\\2 \ \1\<^esup>" unfolding cexp_def using curry_eqpoll cardinal_cong by blast also have " \ = \\<^bsup>\\2 \ \1\<^esup>" using cardinal_eqpoll[THEN eqpoll_sym] unfolding cmult_def by (intro cexp_eqpoll_cong) (simp) finally show ?thesis . qed lemma cardinal_Pow: "|Pow(X)| = 2\<^bsup>\X\<^esup>" \ \Perhaps it's better with |X|\ using cardinal_eqpoll_iff[THEN iffD2, OF Pow_eqpoll_function_space] unfolding cexp_def by simp lemma cantor_cexp: assumes "Card(\)" shows "\ < 2\<^bsup>\\\<^esup>" using assms Card_is_Ord Card_cexp proof (intro not_le_iff_lt[THEN iffD1] notI) assume "2\<^bsup>\\\<^esup> \ \" then have "|Pow(\)| \ \" using cardinal_Pow by simp with assms have "Pow(\) \ \" using cardinal_eqpoll_iff Card_le_imp_lepoll Card_cardinal_eq by auto then obtain g where "g \ inj(Pow(\), \)" by blast then show "False" using cantor_inj by simp qed simp lemma cexp_left_mono: assumes "\1 \ \2" shows "\1\<^bsup>\\\<^esup> \ \2\<^bsup>\\\<^esup>" (* \ \short, unreadable proof: \ unfolding cexp_def - using subset_imp_lepoll[THEN lepoll_imp_Card_le] + using subset_imp_lepoll[THEN lepoll_imp_cardinal_le] assms le_subset_iff[THEN iffD1, OF assms] Pi_weaken_type[of _ _ "\_. \1" "\_. \2"] by auto *) proof - from assms have "\1 \ \2" using le_subset_iff by simp then have "\ \ \1 \ \ \ \2" using Pi_weaken_type by auto then show ?thesis unfolding cexp_def - using lepoll_imp_Card_le subset_imp_lepoll by simp + using lepoll_imp_cardinal_le subset_imp_lepoll by simp qed lemma cantor_cexp': assumes "2 \ \" "Card(\)" shows "\ < \\<^bsup>\\\<^esup>" using cexp_left_mono assms cantor_cexp lt_trans2 by blast lemma InfCard_cexp: assumes "2 \ \" "InfCard(\)" shows "InfCard(\\<^bsup>\\\<^esup>)" using assms cantor_cexp'[THEN leI] le_trans Card_cexp unfolding InfCard_def by auto lemmas InfCard_cexp' = InfCard_cexp[OF nats_le_InfCard, simplified] \ \\<^term>\InfCard(\) \ InfCard(\) \ InfCard(\\<^bsup>\\\<^esup>)\\ subsection\Miscellaneous\ lemma cardinal_RepFun_le: "|{f(a) . a\A}| \ |A|" proof - have "(\x\A. f(x)) \ surj(A, {f(a) . a\A})" unfolding surj_def using lam_funtype by auto then show ?thesis using surj_implies_cardinal_le by blast qed lemma subset_imp_le_cardinal: "A \ B \ |A| \ |B|" - using subset_imp_lepoll[THEN lepoll_imp_Card_le] . + using subset_imp_lepoll[THEN lepoll_imp_cardinal_le] . lemma lt_cardinal_imp_not_subset: "|A| < |B| \ \ B \ A" using subset_imp_le_cardinal le_imp_not_lt by blast lemma cardinal_lt_csucc_iff: "Card(K) \ |K'| < K\<^sup>+ \ |K'| \ K" by (simp add: Card_lt_csucc_iff) lemma cardinal_UN_le_nat: "(\i. i\\ \ |X(i)| \ \) \ |\i\\. X(i)| \ \" by (simp add: cardinal_UN_le InfCard_nat) lemma leqpoll_imp_cardinal_UN_le: notes [dest] = InfCard_is_Card Card_is_Ord assumes "InfCard(K)" "J \ K" "\i. i\J \ |X(i)| \ K" shows "|\i\J. X(i)| \ K" proof - from \J \ K\ obtain f where "f \ inj(J,K)" by blast define Y where "Y(k) \ if k\range(f) then X(converse(f)k) else 0" for k have "i\J \ fi \ K" for i using inj_is_fun[OF \f \ inj(J,K)\] by auto have "(\i\J. X(i)) \ (\i\K. Y(i))" proof (standard, elim UN_E) fix x i assume "i\J" "x\X(i)" with \f \ inj(J,K)\ \i\J \ fi \ K\ have "x \ Y(fi)" "fi \ K" unfolding Y_def using inj_is_fun[OF \f \ inj(J,K)\] right_inverse apply_rangeI by auto then show "x \ (\i\K. Y(i))" by auto qed then have "|\i\J. X(i)| \ |\i\K. Y(i)|" unfolding Y_def using subset_imp_le_cardinal by simp with assms \\i. i\J \ fi \ K\ show "|\i\J. X(i)| \ K" using inj_converse_fun[OF \f \ inj(J,K)\] unfolding Y_def by (rule_tac le_trans[OF _ cardinal_UN_le]) (auto intro:Ord_0_le)+ qed lemma cardinal_lt_csucc_iff': includes Ord_dests assumes "Card(\)" shows "\ < |X| \ \\<^sup>+ \ |X|" using assms cardinal_lt_csucc_iff[of \ X] Card_csucc[of \] not_le_iff_lt[of "\\<^sup>+" "|X|"] not_le_iff_lt[of "|X|" \] by blast lemma lepoll_imp_subset_bij: "X \ Y \ (\Z. Z \ Y \ Z \ X)" proof assume "X \ Y" then obtain j where "j \ inj(X,Y)" by blast then have "range(j) \ Y" "j \ bij(X,range(j))" using inj_bij_range inj_is_fun range_fun_subset_codomain by blast+ then show "\Z. Z \ Y \ Z \ X" using eqpoll_sym unfolding eqpoll_def by force next assume "\Z. Z \ Y \ Z \ X" then obtain Z f where "f \ bij(Z,X)" "Z \ Y" unfolding eqpoll_def by force then have "converse(f) \ inj(X,Y)" using bij_is_inj inj_weaken_type bij_converse_bij by blast then show "X \ Y" by blast qed text\The following result proves to be very useful when combining \<^term>\cardinal\ and \<^term>\eqpoll\ in a calculation.\ lemma cardinal_Card_eqpoll_iff: "Card(\) \ |X| = \ \ X \ \" using Card_cardinal_eq[of \] cardinal_eqpoll_iff[of X \] by auto \ \Compare @{thm "le_Card_iff"}\ lemma lepoll_imp_lepoll_cardinal: assumes "X \ Y" shows "X \ |Y|" using assms cardinal_Card_eqpoll_iff[of "|Y|" Y] lepoll_eq_trans[of _ _ "|Y|"] by simp lemma lepoll_Un: assumes "InfCard(\)" "A \ \" "B \ \" shows "A \ B \ \" proof - have "A \ B \ sum(A,B)" using Un_lepoll_sum . moreover note assms moreover from this have "|sum(A,B)| \ \ \ \" - using sum_lepoll_mono[of A \ B \] lepoll_imp_Card_le + using sum_lepoll_mono[of A \ B \] lepoll_imp_cardinal_le unfolding cadd_def by auto ultimately show ?thesis using InfCard_cdouble_eq Card_cardinal_eq InfCard_is_Card Card_le_imp_lepoll[of "sum(A,B)" \] lepoll_trans[of "A\B"] by auto qed lemma cardinal_Un_le: assumes "InfCard(\)" "|A| \ \" "|B| \ \" shows "|A \ B| \ \" using assms lepoll_Un le_Card_iff InfCard_is_Card by auto text\This is the unconditional version under choice of @{thm Cardinal.Finite_cardinal_iff}.\ lemma Finite_cardinal_iff': "Finite(|i|) \ Finite(i)" using cardinal_eqpoll_iff eqpoll_imp_Finite_iff by fastforce lemma cardinal_subset_of_Card: assumes "Card(\)" "a \ \" shows "|a| < \ \ |a| = \" proof - from assms have "|a| < |\| \ |a| = |\|" using subset_imp_le_cardinal le_iff by simp with assms show ?thesis using Card_cardinal_eq by simp qed lemma cardinal_cases: includes Ord_dests shows "Card(\) \ |X| < \ \ \ |X| \ \" using not_le_iff_lt by auto subsection\Countable and uncountable sets\ \ \Kunen's Definition I.10.5\ definition countable :: "i\o" where "countable(X) \ X \ \" lemma countableI[intro]: "X \ \ \ countable(X)" unfolding countable_def by simp lemma countableD[dest]: "countable(X) \ X \ \" unfolding countable_def by simp lemma countable_iff_cardinal_le_nat: "countable(X) \ |X| \ \" using le_Card_iff[of \ X] Card_nat unfolding countable_def by simp lemma lepoll_countable: "X \ Y \ countable(Y) \ countable(X)" using lepoll_trans[of X Y] by blast \ \Next lemma can be proved without using AC\ lemma surj_countable: "countable(X) \ f \ surj(X,Y) \ countable(Y)" using surj_implies_cardinal_le[of f X Y, THEN le_trans] countable_iff_cardinal_le_nat by simp lemma Finite_imp_countable: "Finite(X) \ countable(X)" unfolding Finite_def by (auto intro:InfCard_nat nats_le_InfCard[of _ \, THEN le_imp_lepoll] dest!:eq_lepoll_trans[of X _ \]) lemma countable_imp_countable_UN: assumes "countable(J)" "\i. i\J \ countable(X(i))" shows "countable(\i\J. X(i))" using assms leqpoll_imp_cardinal_UN_le[of \ J X] InfCard_nat countable_iff_cardinal_le_nat by auto lemma countable_union_countable: assumes "\x. x \ C \ countable(x)" "countable(C)" shows "countable(\C)" using assms countable_imp_countable_UN[of C "\x. x"] by simp abbreviation uncountable :: "i\o" where "uncountable(X) \ \ countable(X)" lemma uncountable_iff_nat_lt_cardinal: "uncountable(X) \ \ < |X|" using countable_iff_cardinal_le_nat not_le_iff_lt by simp lemma uncountable_not_empty: "uncountable(X) \ X \ 0" using empty_lepollI by auto lemma uncountable_imp_Infinite: "uncountable(X) \ Infinite(X)" using uncountable_iff_nat_lt_cardinal[of X] lepoll_nat_imp_Infinite[of X] cardinal_le_imp_lepoll[of \ X] leI by simp lemma uncountable_not_subset_countable: assumes "countable(X)" "uncountable(Y)" shows "\ (Y \ X)" using assms lepoll_trans subset_imp_lepoll[of Y X] by blast subsection\Results on Alephs\ lemma nat_lt_Aleph1: "\ < \\<^bsub>1\<^esub>" by (simp add: Aleph_def lt_csucc) lemma zero_lt_Aleph1: "0 < \\<^bsub>1\<^esub>" by (rule lt_trans[of _ "\"], auto simp add: ltI nat_lt_Aleph1) lemma le_aleph1_nat: "Card(k) \ k<\\<^bsub>1\<^esub> \ k \ \" by (simp add: Aleph_def Card_lt_csucc_iff Card_nat) lemma Aleph_succ: "\\<^bsub>succ(\)\<^esub> = \\<^bsub>\\<^esub>\<^sup>+" unfolding Aleph_def by simp lemma lesspoll_aleph_plus_one: assumes "Ord(\)" shows "d \ \\<^bsub>succ(\)\<^esub> \ d \ \\<^bsub>\\<^esub>" using assms lesspoll_csucc Aleph_succ Card_is_Ord by simp lemma cardinal_Aleph [simp]: "Ord(\) \ |\\<^bsub>\\<^esub>| = \\<^bsub>\\<^esub>" using Card_cardinal_eq by simp \ \Could be proved without using AC\ lemma Aleph_lesspoll_increasing: includes Aleph_intros shows "a < b \ \\<^bsub>a\<^esub> \ \\<^bsub>b\<^esub>" using cardinal_lt_iff_lesspoll[of "\\<^bsub>a\<^esub>" "\\<^bsub>b\<^esub>"] Card_cardinal_eq[of "\\<^bsub>b\<^esub>"] lt_Ord lt_Ord2 Card_Aleph[THEN Card_is_Ord] by auto lemma uncountable_iff_subset_eqpoll_Aleph1: includes Ord_dests notes Aleph_zero_eq_nat[simp] Card_nat[simp] Aleph_succ[simp] shows "uncountable(X) \ (\S. S \ X \ S \ \\<^bsub>1\<^esub>)" proof assume "uncountable(X)" then have "\\<^bsub>1\<^esub> \ X" using uncountable_iff_nat_lt_cardinal cardinal_lt_csucc_iff' cardinal_le_imp_lepoll by force then obtain S where "S \ X" "S \ \\<^bsub>1\<^esub>" using lepoll_imp_subset_bij by auto then show "\S. S \ X \ S \ \\<^bsub>1\<^esub>" using cardinal_cong Card_csucc[of \] Card_cardinal_eq by auto next assume "\S. S \ X \ S \ \\<^bsub>1\<^esub>" then have "\\<^bsub>1\<^esub> \ X" using subset_imp_lepoll[THEN [2] eq_lepoll_trans, of "\\<^bsub>1\<^esub>" _ X, OF eqpoll_sym] by auto then show "uncountable(X)" using Aleph_lesspoll_increasing[of 0 1, THEN [2] lesspoll_trans1, of "\\<^bsub>1\<^esub>"] lepoll_trans[of "\\<^bsub>1\<^esub>" X \] by auto qed lemma lt_Aleph_imp_cardinal_UN_le_nat: "function(G) \ domain(G) \ \ \ \n\domain(G). |Gn|<\\<^bsub>1\<^esub> \ |\n\domain(G). Gn|\\" proof - assume "function(G)" let ?N="domain(G)" and ?R="\n\domain(G). Gn" assume "?N \ \" assume Eq1: "\n\?N. |Gn|<\\<^bsub>1\<^esub>" { fix n assume "n\?N" with Eq1 have "|Gn| \ \" using le_aleph1_nat by simp } then have "n\?N \ |Gn| \ \" for n . with \?N \ \\ show ?thesis using InfCard_nat leqpoll_imp_cardinal_UN_le by simp qed lemma Aleph1_eq_cardinal_vimage: "f:\\<^bsub>1\<^esub>\\ \ \n\\. |f-{n}| = \\<^bsub>1\<^esub>" proof - assume "f:\\<^bsub>1\<^esub>\\" then have "function(f)" "domain(f) = \\<^bsub>1\<^esub>" "range(f)\\" by (simp_all add: domain_of_fun fun_is_function range_fun_subset_codomain) let ?G="\n\range(f). f-{n}" from \f:\\<^bsub>1\<^esub>\\\ have "range(f) \ \" by (simp add: range_fun_subset_codomain) then have "domain(?G) \ \" using subset_imp_lepoll by simp have "function(?G)" by (simp add:function_lam) from \f:\\<^bsub>1\<^esub>\\\ have "n\\ \ f-{n} \ \\<^bsub>1\<^esub>" for n using Pi_vimage_subset by simp with \range(f) \ \\ have "\\<^bsub>1\<^esub> = (\n\range(f). f-{n})" proof (intro equalityI, intro subsetI) fix x assume "x \ \\<^bsub>1\<^esub>" with \f:\\<^bsub>1\<^esub>\\\ \function(f)\ \domain(f) = \\<^bsub>1\<^esub>\ have "x \ f-{fx}" "fx \ range(f)" using function_apply_Pair vimage_iff apply_rangeI by simp_all then show "x \ (\n\range(f). f-{n})" by auto qed auto { assume "\n\range(f). |f-{n}| < \\<^bsub>1\<^esub>" then have "\n\domain(?G). |?Gn| < \\<^bsub>1\<^esub>" using zero_lt_Aleph1 by (auto) with \function(?G)\ \domain(?G) \ \\ have "|\n\domain(?G). ?Gn|\\" using lt_Aleph_imp_cardinal_UN_le_nat by blast then have "|\n\range(f). f-{n}|\\" by simp with \\\<^bsub>1\<^esub> = _\ have "|\\<^bsub>1\<^esub>| \ \" by simp then have "\\<^bsub>1\<^esub> \ \" using Card_Aleph Card_cardinal_eq by simp then have "False" using nat_lt_Aleph1 by (blast dest:lt_trans2) } with \range(f)\\\ obtain n where "n\\" "$$|f - {n}| < \\<^bsub>1\<^esub>)" by blast moreover from this have "\\<^bsub>1\<^esub> \ |f-{n}|" using not_lt_iff_le Card_is_Ord by auto moreover note \n\\ \ f-{n} \ \\<^bsub>1\<^esub>\ ultimately show ?thesis using subset_imp_le_cardinal[THEN le_anti_sym, of _ "\\<^bsub>1\<^esub>"] Card_Aleph Card_cardinal_eq by auto qed \ \There is some asymmetry between assumptions and conclusion (\<^term>\($$\ versus \<^term>\cardinal\)\ lemma eqpoll_Aleph1_cardinal_vimage: assumes "X \ \\<^bsub>1\<^esub>" "f : X \ \" shows "\n\\. |f-{n}| = \\<^bsub>1\<^esub>" proof - from assms obtain g where "g\bij(\\<^bsub>1\<^esub>,X)" using eqpoll_sym by blast with \f : X \ \\ have "f O g : \\<^bsub>1\<^esub> \ \" "converse(g) \ bij(X, \\<^bsub>1\<^esub>)" using bij_is_fun comp_fun bij_converse_bij by blast+ then obtain n where "n\\" "|(f O g)-{n}| = \\<^bsub>1\<^esub>" using Aleph1_eq_cardinal_vimage by auto then have "\\<^bsub>1\<^esub> = |converse(g)  (f -{n})|" using image_comp converse_comp unfolding vimage_def by simp also from \converse(g) \ bij(X, \\<^bsub>1\<^esub>)\ \f: X\ \\ have "\ = |f -{n}|" using range_of_subset_eqpoll[of "converse(g)" X _ "f -{n}"] bij_is_inj cardinal_cong bij_is_fun eqpoll_sym Pi_vimage_subset by fastforce finally show ?thesis using \n\\\ by auto qed subsection\Applications of transfinite recursive constructions\ definition rec_constr :: "[i,i] \ i" where "rec_constr(f,\) \ transrec(\,\a g. f(ga))" text\The function \<^term>\rec_constr\ allows to perform \<^emph>\recursive constructions\: given a choice function on the powerset of some set, a transfinite sequence is created by successively choosing some new element. The next result explains its use.\ lemma rec_constr_unfold: "rec_constr(f,\) = f({rec_constr(f,\). \\\})" using def_transrec[OF rec_constr_def, of f \] image_lam by simp lemma rec_constr_type: assumes "f:Pow(G)\ G" "Ord(\)" shows "rec_constr(f,\) \ G" using assms(2,1) by (induct rule:trans_induct) (subst rec_constr_unfold, rule apply_type[of f "Pow(G)" "\_. G"], auto) text\The next lemma is an application of recursive constructions. It works under the assumption that whenever the already constructed subsequence is small enough, another element can be added.\ lemma bounded_cardinal_selection: includes Ord_dests assumes "\X. |X| < \ \ X \ G \ \a\G. \s\X. Q(s,a)" "b\G" "Card(\)" shows "\S. S : \ \ G \ (\\ \ \. \\ \ \. \<\ \ Q(S\,S\))" proof - let ?cdlt\="{X\Pow(G) . |X|<\}" \ \“cardinal less than \<^term>\\\”\ and ?inQ="\Y.{a\G. \s\Y. Q(s,a)}" from assms have "\Y \ ?cdlt\. \a. a \ ?inQ(Y)" by blast then have "\f. f \ Pi(?cdlt\,?inQ)" using AC_ball_Pi[of ?cdlt\ ?inQ] by simp then obtain f where f_type:"f \ Pi(?cdlt\,?inQ)" by auto moreover define Cb where "Cb \ \_\Pow(G)-?cdlt\. b" moreover from \b\G\ have "Cb \ Pow(G)-?cdlt\ \ G" unfolding Cb_def by simp moreover note \Card(\)\ ultimately have "f \ Cb : (\x\Pow(G). ?inQ(x) \ G)" using fun_Pi_disjoint_Un[ of f ?cdlt\ ?inQ Cb "Pow(G)-?cdlt\" "\_.G"] Diff_partition[of "{X\Pow(G). |X|<\}" "Pow(G)", OF Collect_subset] by auto moreover have "?inQ(x) \ G = G" for x by auto ultimately have "f \ Cb : Pow(G) \ G" by simp define S where "S\\\\\. rec_constr(f \ Cb, \)" from \f \ Cb: Pow(G) \ G\ \Card(\)\ have "S : \ \ G" using Ord_in_Ord unfolding S_def by (intro lam_type rec_constr_type) auto moreover have "\\\\. \\\\. \ < \ \ Q(S  \, S  \)" proof (intro ballI impI) fix \ \ assume "\\\" with \Card(\)\ have "{rec_constr(f \ Cb, x) . x\\} = {Sx . x \ \}" using Ord_trans[OF _ _ Card_is_Ord, of _ \ \] unfolding S_def by auto moreover from \\\\\ \S : \ \ G\ \Card(\)\ have "{Sx . x \ \} \ G" using Ord_trans[OF _ _ Card_is_Ord, of _ \ \] apply_type[of S \ "\_. G"] by auto moreover from \Card(\)\ \\\\\ have "|{Sx . x \ \}| < \" using cardinal_RepFun_le[of \] Ord_in_Ord lt_trans1[of "|{Sx . x \ \}|" "|\|" \] Card_lt_iff[THEN iffD2, of \ \, OF _ _ ltI] by force moreover have "\x\\. Q(Sx, f  {Sx . x \ \})" proof - from calculation and f_type have "f  {Sx . x \ \} \ {a\G. \x\\. Q(Sx,a)}" using apply_type[of f ?cdlt\ ?inQ "{Sx . x \ \}"] by blast then show ?thesis by simp qed moreover assume "\\\" "\ < \" moreover note \\\\\ \Cb \ Pow(G)-?cdlt\ \ G\ ultimately show "Q(S  \, S  \)" using fun_disjoint_apply1[of "{Sx . x \ \}" Cb f] domain_of_fun[of Cb] ltD[of \ \] by (subst (2) S_def, auto) (subst rec_constr_unfold, auto) qed ultimately show ?thesis by blast qed text\The following basic result can, in turn, be proved by a bounded-cardinal selection.\ lemma Infinite_iff_lepoll_nat: "Infinite(X) \ \ \ X" proof assume "Infinite(X)" then obtain b where "b\X" using Infinite_not_empty by auto { fix Y assume "|Y| < \" then have "Finite(Y)" using Finite_cardinal_iff' ltD nat_into_Finite by blast with \Infinite(X)\ have "X \ Y" by auto } with \b\X\ obtain S where "S : \ \ X" "\\\\. \\\\. \ < \ \ S\ \ S\" using bounded_cardinal_selection[of \ X "\x y. x\y"] Card_nat by blast moreover from this have "\ \ \ \ \ \ \ \ \\\ \ S\ \ S\" for \ \ by (rule_tac lt_neq_symmetry[of "\" "\\ \. S\ \ S\"]) auto ultimately show "\ \ X" unfolding lepoll_def inj_def by blast qed (intro lepoll_nat_imp_Infinite) lemma Infinite_InfCard_cardinal: "Infinite(X) \ InfCard(|X|)" using lepoll_eq_trans eqpoll_sym lepoll_nat_imp_Infinite Infinite_iff_lepoll_nat Inf_Card_is_InfCard cardinal_eqpoll by simp lemma Finite_to_one_surj_imp_cardinal_eq: assumes "F \ Finite_to_one(X,Y) \ surj(X,Y)" "Infinite(X)" shows "|Y| = |X|" proof - from \F \ Finite_to_one(X,Y) \ surj(X,Y)\ have "X = (\y\Y. {x\X . Fx = y})" using apply_type by fastforce show ?thesis proof (cases "Finite(Y)") case True with \X = (\y\Y. {x\X . Fx = y})\ and assms show ?thesis using Finite_RepFun[THEN [2] Finite_Union, of Y "\y. {x\X . Fx = y}"] by auto next case False moreover from this have "Y \ |Y|" using cardinal_eqpoll eqpoll_sym eqpoll_imp_lepoll by simp moreover note assms moreover from calculation have "y \ Y \ |{x\X . Fx = y}| \ |Y|" for y - using Infinite_imp_nats_lepoll[THEN lepoll_imp_Card_le, of Y + using Infinite_imp_nats_lepoll[THEN lepoll_imp_cardinal_le, of Y "|{x\X . Fx = y}|"] cardinal_idem by auto ultimately have "|\y\Y. {x\X . Fx = y}| \ |Y|" using leqpoll_imp_cardinal_UN_le[of "|Y|" Y] Infinite_InfCard_cardinal[of Y] by simp moreover from \F \ Finite_to_one(X,Y) \ surj(X,Y)\ have "|Y| \ |X|" using surj_implies_cardinal_le by auto moreover note \X = (\y\Y. {x\X . Fx = y})\ ultimately show ?thesis using le_anti_sym by auto qed qed lemma cardinal_map_Un: assumes "Infinite(X)" "Finite(b)" shows "|{a \ b . a \ X}| = |X|" proof - have "(\a\X. a \ b) \ Finite_to_one(X,{a \ b . a \ X})" "(\a\X. a \ b) \ surj(X,{a \ b . a \ X})" unfolding surj_def proof fix d have "Finite({a \ X . a \ b = d})" (is "Finite(?Y(b,d))") using \Finite(b)\ proof (induct arbitrary:d) case 0 have "{a \ X . a \ 0 = d} = (if d\X then {d} else 0)" by auto then show ?case by simp next case (cons c b) from \c \ b\ have "?Y(cons(c,b),d) \ (if c\d then ?Y(b,d) \ ?Y(b,d-{c}) else 0)" by auto with cons show ?case using subset_Finite by simp qed moreover assume "d \ {x \ b . x \ X}" ultimately show "Finite({a \ X . (\x\X. x \ b)  a = d})" by simp qed (auto intro:lam_funtype) with assms show ?thesis using Finite_to_one_surj_imp_cardinal_eq by fast qed end \ No newline at end of file diff --git a/thys/Delta_System_Lemma/Cohen_Posets.thy b/thys/Delta_System_Lemma/Cohen_Posets.thy --- a/thys/Delta_System_Lemma/Cohen_Posets.thy +++ b/thys/Delta_System_Lemma/Cohen_Posets.thy @@ -1,248 +1,248 @@ subsection\Application to Cohen posets\label{sec:cohen}\ theory Cohen_Posets imports Delta_System begin text\We end this session by applying DSL to the combinatorics of finite function posets. We first define some basic concepts; we take a different approach from \cite{2020arXiv200109715G}, in that the order relation is presented as a predicate (of type @{typ $i,i] \ o\}). Two elements of a poset are \<^emph>\compatible\ if they have a common lower bound.\ definition compat_in :: "[i,[i,i]\o,i,i]\o" where "compat_in(A,r,p,q) \ \d\A . r(d,p) \ r(d,q)" text\An \<^emph>\antichain\ is a subset of pairwise incompatible members.\ definition antichain :: "[i,[i,i]\o,i]\o" where "antichain(P,leq,A) \ A\P \ (\p\A. \q\A. p\q \ \compat_in(P,leq,p,q))" text\A poset has the \<^emph>\countable chain condition\ (ccc) if all of its antichains are countable.\ definition ccc :: "[i,[i,i]\o]\o" where "ccc(P,leq) \ \A. antichain(P,leq,A) \ countable(A)" text\Finally, the \<^emph>\Cohen poset\ is the set of finite partial functions between two sets with the order of reverse inclusion.\ definition Fn :: "[i,i] \ i" where "Fn(I,J) \ \{(d\J) . d \ {x \ Pow(I). Finite(x)}}" abbreviation Supset :: "i \ i \ o" (infixl \\\ 50) where "f \ g \ g \ f" lemma FnI[intro]: assumes "p : d \ J" "d \ I" "Finite(d)" shows "p \ Fn(I,J)" using assms unfolding Fn_def by auto lemma FnD[dest]: assumes "p \ Fn(I,J)" shows "\d. p : d \ J \ d \ I \ Finite(d)" using assms unfolding Fn_def by auto lemma Fn_is_function: "p \ Fn(I,J) \ function(p)" unfolding Fn_def using fun_is_function by auto lemma restrict_eq_imp_compat: assumes "f \ Fn(I, J)" "g \ Fn(I, J)" "restrict(f, domain(f) \ domain(g)) = restrict(g, domain(f) \ domain(g))" shows "f \ g \ Fn(I, J)" proof - from assms obtain d1 d2 where "f : d1 \ J" "d1 \ Pow(I)" "Finite(d1)" "g : d2 \ J" "d2 \ Pow(I)" "Finite(d2)" by blast with assms show ?thesis using domain_of_fun restrict_eq_imp_Un_into_Pi[of f d1 "\_. J" g d2 "\_. J"] by auto qed text\We finally arrive to our application of DSL.\ -lemma ccc_Fn_nat: "ccc(Fn(I,2), (\))" +lemma ccc_Fn_2: "ccc(Fn(I,2), (\))" proof - { fix A assume "\ countable(A)" assume "A \ Fn(I, 2)" moreover from this have "countable({p\A. domain(p) = d})" for d proof (cases "Finite(d) \ d \ I") case True with \A \ Fn(I, 2)\ have "{p \ A . domain(p) = d} \ d \ 2" using domain_of_fun by fastforce moreover from True have "Finite(d \ 2)" using Finite_Pi lesspoll_nat_is_Finite by auto ultimately show ?thesis using subset_Finite[of _ "d\2" ] Finite_imp_countable by auto next case False with \A \ Fn(I, 2)\ have "{p \ A . domain(p) = d} = 0" by (intro equalityI) (auto dest!: domain_of_fun) then show ?thesis using empty_lepollI by auto qed moreover have "uncountable({domain(p) . p \ A})" proof from \A \ Fn(I, 2)\ have "A = (\d\{domain(p) . p \ A}. {p\A. domain(p) = d})" by auto moreover assume "countable({domain(p) . p \ A})" moreover note \\d. countable({p\A. domain(p) = d})\ \\countable(A)\ ultimately show "False" using countable_imp_countable_UN[of "{domain(p). p\A}" "\d. {p \ A. domain(p) = d }"] by auto qed moreover from \A \ Fn(I, 2)\ have "p \ A \ Finite(domain(p))" for p using lesspoll_nat_is_Finite[of "domain(p)"] domain_of_fun[of p _ "\_. 2"] by auto ultimately obtain D where "delta_system(D)" "D \ {domain(p) . p \ A}" "D \ \\<^bsub>1\<^esub>" using delta_system_uncountable[of "{domain(p) . p \ A}"] by auto then have delta:"\d1\D. \d2\D. d1 \ d2 \ d1 \ d2 = \D" using delta_system_root_eq_Inter by simp moreover from \D \ \\<^bsub>1\<^esub>\ have "uncountable(D)" using uncountable_iff_subset_eqpoll_Aleph1 by auto moreover from this and \D \ {domain(p) . p \ A}\ obtain p1 where "p1 \ A" "domain(p1) \ D" using uncountable_not_empty[of D] by blast moreover from this and \p1 \ A \ Finite(domain(p1))\ have "Finite(domain(p1))" using Finite_domain by simp moreover define r where "r \ \D" ultimately have "Finite(r)" using subset_Finite[of "r" "domain(p1)"] by auto have "countable({restrict(p,r) . p\A})" proof - have "f \ Fn(I, 2) \ restrict(f,r) \ Pow(r \ 2)" for f using restrict_subset_Sigma[of f _ "\_. 2" r] by (auto dest!:FnD simp: Pi_def) auto with \A \ Fn(I, 2)\ have "{restrict(f,r) . f \ A } \ Pow(r \ 2)" by fast with \Finite(r)\ show ?thesis using Finite_Sigma[THEN Finite_Pow, of r "\_. 2"] by (intro Finite_imp_countable) (auto intro:subset_Finite) qed moreover have "uncountable({p\A. domain(p) \ D})" (is "uncountable(?X)") proof from \D \ {domain(p) . p \ A}\ have "(\p\?X. domain(p)) \ surj(?X, D)" using lam_type unfolding surj_def by auto moreover assume "countable(?X)" moreover note \uncountable(D)\ ultimately show False using surj_countable by auto qed moreover have "D = (\f\Pow(r\2) . {domain(p) . p\{ x\A. restrict(x,r) = f \ domain(x) \ D}})" proof - { fix z assume "z \ D" with \D \ _\ obtain p where "domain(p) = z" "p \ A" by auto moreover from \A \ Fn(I, 2)\ and this have "p : z \ 2" using domain_of_fun by (auto dest!:FnD) moreover from this have "restrict(p,r) \ r \ 2" using function_restrictI[of p r] fun_is_function[of p z "\_. 2"] restrict_subset_Sigma[of p z "\_. 2" r] by (auto simp:Pi_def) ultimately have "\p\A. restrict(p,r) \ Pow(r\2) \ domain(p) = z" by auto } then show ?thesis by (intro equalityI) (force)+ qed obtain f where "uncountable({domain(p) . p\{x\A. restrict(x,r) = f \ domain(x) \ D}})" (is "uncountable(?Y(f))") proof - { from \Finite(r)\ have "countable(Pow(r\2))" using Finite_Sigma[THEN Finite_Pow, THEN Finite_imp_countable] by simp moreover assume "countable(?Y(f))" for f moreover note \D = (\f\Pow(r\2) .?Y(f))\ moreover note \uncountable(D)\ ultimately have "False" using countable_imp_countable_UN[of "Pow(r\2)" ?Y] by auto } with that show ?thesis by auto qed then obtain j where "j \ inj(nat, ?Y(f))" using uncountable_iff_nat_lt_cardinal[THEN iffD1, THEN leI, THEN cardinal_le_imp_lepoll, THEN lepollD] by auto then have "j0 \ j1" "j0 \ ?Y(f)" "j1 \ ?Y(f)" using inj_is_fun[THEN apply_type, of j nat "?Y(f)"] unfolding inj_def by auto then obtain p q where "domain(p) \ domain(q)" "p \ A" "q \ A" "domain(p) \ D" "domain(q) \ D" "restrict(p,r) = restrict(q,r)" by auto moreover from this and delta have "domain(p) \ domain(q) = r" unfolding r_def by simp moreover note \A \ Fn(I, 2)\ moreover from calculation have "p \ q \ Fn(I, 2)" by (rule_tac restrict_eq_imp_compat) auto ultimately have "\p\A. \q\A. p \ q \ compat_in(Fn(I, 2), (\), p, q)" unfolding compat_in_def by (rule_tac bexI[of _ p], rule_tac bexI[of _ q]) blast } then show ?thesis unfolding ccc_def antichain_def by auto qed text\The fact that a poset P has the ccc has useful consequences for the theory of forcing, since it implies that cardinals from the original model are exactly the cardinals in any generic extension by P \cite[Chap.~IV]{kunen2011set}.\ end \ No newline at end of file diff --git a/thys/Delta_System_Lemma/Konig.thy b/thys/Delta_System_Lemma/Konig.thy --- a/thys/Delta_System_Lemma/Konig.thy +++ b/thys/Delta_System_Lemma/Konig.thy @@ -1,187 +1,187 @@ theory Konig imports Cofinality Cardinal_Library begin text\Now, using the Axiom of choice, we can show that all successor cardinals are regular.\ lemma cf_csucc: assumes "InfCard(z)" shows "cf(z\<^sup>+) = z\<^sup>+" proof (rule ccontr) assume "cf(z\<^sup>+) \ z\<^sup>+" moreover from \InfCard(z)\ have "Ord(z\<^sup>+)" "Ord(z)" "Limit(z)" "Limit(z\<^sup>+)" "Card(z\<^sup>+)" "Card(z)" using InfCard_csucc Card_is_Ord InfCard_is_Card InfCard_is_Limit by fastforce+ moreover from calculation have "cf(z\<^sup>+) < z\<^sup>+" using cf_le_cardinal[of "z\<^sup>+", THEN le_iff[THEN iffD1]] Card_cardinal_eq by simp ultimately obtain G where "G:cf(z\<^sup>+)\ z\<^sup>+" "\\\z\<^sup>+. \y\cf(z\<^sup>+). \ < Gy" using Limit_cofinal_fun_lt[of "z\<^sup>+" _ "cf(z\<^sup>+)"] Ord_cf cf_le_cf_fun[of "z\<^sup>+" "cf(z\<^sup>+)"] le_refl[of "cf(z\<^sup>+)"] by auto with \Card(z)\ \Card(z\<^sup>+)\ \Ord(z\<^sup>+)\ have "\\\cf(z\<^sup>+). |G\| \ z" using apply_type[of G "cf(z\<^sup>+)" "\_. z\<^sup>+", THEN ltI] Card_lt_iff[THEN iffD2] Ord_in_Ord[OF Card_is_Ord, of "z\<^sup>+"] cardinal_lt_csucc_iff[THEN iffD1] by auto from \cf(z\<^sup>+) < z\<^sup>+\ \InfCard(z)\ \Ord(z)\ have "cf(z\<^sup>+) \ z" using cardinal_lt_csucc_iff[of "z" "cf(z\<^sup>+)"] Card_csucc[of "z"] le_Card_iff[of "z" "cf(z\<^sup>+)"] InfCard_is_Card Card_lt_iff[of "cf(z\<^sup>+)" "z\<^sup>+"] lt_Ord[of "cf(z\<^sup>+)" "z\<^sup>+"] by simp with \cf(z\<^sup>+) < z\<^sup>+\ \\\\cf(z\<^sup>+). |G\| \ _\ \InfCard(z)\ have "|\\\cf(z\<^sup>+). G\| \ z" using InfCard_csucc[of z] - subset_imp_lepoll[THEN lepoll_imp_Card_le, of "\\\cf(z\<^sup>+). G\" "z"] + subset_imp_lepoll[THEN lepoll_imp_cardinal_le, of "\\\cf(z\<^sup>+). G\" "z"] by (rule_tac leqpoll_imp_cardinal_UN_le) auto moreover note \Ord(z)\ moreover from \\\\z\<^sup>+. \y\cf(z\<^sup>+). \ < Gy\ and this have "z\<^sup>+ \ (\\\cf(z\<^sup>+). G\)" by (blast dest:ltD) ultimately have "z\<^sup>+ \ z" using subset_imp_le_cardinal[of "z\<^sup>+" "\\\cf(z\<^sup>+). G\"] le_trans InfCard_is_Card Card_csucc[of z] Card_cardinal_eq by auto with \Ord(z)\ show "False" using lt_csucc[of z] not_lt_iff_le[THEN iffD2, of z "z\<^sup>+"] Card_csucc[THEN Card_is_Ord] by auto qed text\And this finishes the calculation of cofinality of Alephs.\ lemma cf_Aleph_succ: "Ord(z) \ cf(\\<^bsub>succ(z)\<^esub>) = \\<^bsub>succ(z)\<^esub>" using Aleph_succ cf_csucc InfCard_Aleph by simp subsection\König's Theorem\label{sec:konig}\ text\We end this section by proving König's Theorem on the cofinality of cardinal exponentiation. This is a strengthening of Cantor's theorem and it is essentially the only basic way to prove strict cardinal inequalities. It is proved rather straightforwardly with the tools already developed.\ lemma konigs_theorem: notes [dest] = InfCard_is_Card Card_is_Ord and [trans] = lt_trans1 lt_trans2 assumes "InfCard(\)" "InfCard(\)" "cf(\) \ \" shows "\ < \\<^bsup>\\\<^esup>" using assms(1,2) Card_cexp proof (intro not_le_iff_lt[THEN iffD1] notI) assume "\\<^bsup>\\\<^esup> \ \" moreover note \InfCard(\)\ moreover from calculation have "\ \ \ \ \" using Card_cardinal_eq[OF InfCard_is_Card, symmetric] Card_le_imp_lepoll unfolding cexp_def by simp ultimately obtain G where "G \ surj(\, \ \ \)" using inj_imp_surj[OF _ function_space_nonempty, OF _ nat_into_InfCard] by blast from assms obtain f where "f:\ \ \" "cf_fun(f,\)" using cf_le_cf_fun[OF _ InfCard_is_Limit] by blast define H where "H(\) \ \ x. x\\ \ (\m. Gm\ \ x)" (is "_ \ \ x. ?P(\,x)") for \ have H_satisfies: "?P(\,H(\))" if "\ \ \" for \ proof - obtain h where "?P(\,h)" proof - from \\\\\ \f:\ \ \\ \InfCard(\)\ have "f\ < \" using apply_type[of _ _ "\_ . \"] by (auto intro:ltI) have "|{Gm\ . m \ {x\\ . x < f\}}| \ |{x\\ . x < f\}|" using cardinal_RepFun_le by simp also from \f\ < \\ \InfCard(\)\ have "|{x\\ . x < f\}| < |\|" using Card_lt_iff[OF lt_Ord, THEN iffD2, of "f\" \$ Ord_eq_Collect_lt[of "f\" \] Card_cardinal_eq by force finally have "|{Gm\ . m \ {x\\ . x < f\}}| < |\|" . moreover from \f\ < \\ \InfCard(\)\ have "m \ m\\" for m using Ord_trans[of m "f\" \] by (auto dest:ltD) ultimately have "\h. ?P(\,h)" using lt_cardinal_imp_not_subset by blast with that show ?thesis by blast qed with assms show "?P(\,H(\))" using LeastI[of "?P(\)" h] lt_Ord Ord_in_Ord unfolding H_def by fastforce qed then have "(\\\\. H(\)): \ \ \" using lam_type by auto with \G \ surj(\, \ \ \)\ obtain n where "n\\" "Gn = (\\\\. H(\))" unfolding surj_def by blast moreover note \InfCard(\)\ \f: \ \ \\ \cf_fun(f,_)\ ultimately obtain \ where "n < f\" "\\\" using Limit_cofinal_fun_lt[OF InfCard_is_Limit] by blast moreover from calculation and \Gn = (\\\\. H(\))\ have "Gn\ = H(\)" using ltD by simp moreover from calculation and H_satisfies have "\m. Gm\ \ H(\)" by simp ultimately show "False" by blast qed blast+ lemma cf_cexp: assumes "Card(\)" "InfCard(\)" "2 \ \" shows "\ < cf(\\<^bsup>\\\<^esup>)" proof (rule ccontr) assume "\ \ < cf(\\<^bsup>\\\<^esup>)" with \InfCard(\)\ have "cf(\\<^bsup>\\\<^esup>) \ \" using not_lt_iff_le Ord_cf InfCard_is_Card Card_is_Ord by simp moreover note assms moreover from calculation have "InfCard(\\<^bsup>\\\<^esup>)" using InfCard_cexp by simp moreover from calculation have "\\<^bsup>\\\<^esup> < (\\<^bsup>\\\<^esup>)\<^bsup>\\\<^esup>" using konigs_theorem by simp ultimately show "False" using cexp_cexp_cmult InfCard_csquare_eq by auto qed text\Finally, the next two corollaries illustrate the only possible exceptions to the value of the cardinality of the continuum: The limit cardinals of countable cofinality. That these are the only exceptions is a consequence of Easton's Theorem~\cite[Thm 15.18]{Jech_Millennium}.\ corollary cf_continuum: "\\<^bsub>0\<^esub> < cf(2\<^bsup>\\\<^bsub>0\<^esub>\<^esup>)" using cf_cexp InfCard_Aleph nat_into_Card by simp corollary continuum_not_eq_Aleph_nat: "2\<^bsup>\\\<^bsub>0\<^esub>\<^esup> \ \\<^bsub>\\<^esub>" using cf_continuum cf_Aleph_Limit[OF Limit_nat] cf_nat Aleph_zero_eq_nat by auto end \ No newline at end of file