src/HOL/Cardinals/Cardinal_Arithmetic.thy
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (23 months ago)
changeset 66924 b4d4027f743b
parent 66453 cc19f7ca2ed6
child 68652 1e37b45ce3fb
permissions -rw-r--r--
more permissive;
     1 (*  Title:      HOL/Cardinals/Cardinal_Arithmetic.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Copyright   2012
     4 
     5 Cardinal arithmetic.
     6 *)
     7 
     8 section \<open>Cardinal Arithmetic\<close>
     9 
    10 theory Cardinal_Arithmetic
    11 imports HOL.BNF_Cardinal_Arithmetic Cardinal_Order_Relation
    12 begin
    13 
    14 subsection \<open>Binary sum\<close>
    15 
    16 lemma csum_Cnotzero2:
    17   "Cnotzero r2 \<Longrightarrow> Cnotzero (r1 +c r2)"
    18 unfolding csum_def
    19 by (metis Cnotzero_imp_not_empty Field_card_of Plus_eq_empty_conv card_of_card_order_on czeroE)
    20 
    21 lemma single_cone:
    22   "|{x}| =o cone"
    23 proof -
    24   let ?f = "\<lambda>x. ()"
    25   have "bij_betw ?f {x} {()}" unfolding bij_betw_def by auto
    26   thus ?thesis unfolding cone_def using card_of_ordIso by blast
    27 qed
    28 
    29 lemma cone_Cnotzero: "Cnotzero cone"
    30 by (simp add: cone_not_czero Card_order_cone)
    31 
    32 lemma cone_ordLeq_ctwo: "cone \<le>o ctwo"
    33 unfolding cone_def ctwo_def card_of_ordLeq[symmetric] by auto
    34 
    35 lemma csum_czero1: "Card_order r \<Longrightarrow> r +c czero =o r"
    36   unfolding czero_def csum_def Field_card_of
    37   by (rule ordIso_transitive[OF ordIso_symmetric[OF card_of_Plus_empty1] card_of_Field_ordIso])
    38 
    39 lemma csum_czero2: "Card_order r \<Longrightarrow> czero +c r =o r"
    40   unfolding czero_def csum_def Field_card_of
    41   by (rule ordIso_transitive[OF ordIso_symmetric[OF card_of_Plus_empty2] card_of_Field_ordIso])
    42 
    43 
    44 subsection \<open>Product\<close>
    45 
    46 lemma Times_cprod: "|A \<times> B| =o |A| *c |B|"
    47 by (simp only: cprod_def Field_card_of card_of_refl)
    48 
    49 lemma card_of_Times_singleton:
    50   fixes A :: "'a set"
    51   shows "|A \<times> {x}| =o |A|"
    52 proof -
    53   define f :: "'a \<times> 'b \<Rightarrow> 'a" where "f = (\<lambda>(a, b). a)"
    54   have "A \<subseteq> f ` (A \<times> {x})" unfolding f_def by (auto simp: image_iff)
    55   hence "bij_betw f (A \<times> {x}) A"  unfolding bij_betw_def inj_on_def f_def by fastforce
    56   thus ?thesis using card_of_ordIso by blast
    57 qed
    58 
    59 lemma cprod_assoc: "(r *c s) *c t =o r *c s *c t"
    60   unfolding cprod_def Field_card_of by (rule card_of_Times_assoc)
    61 
    62 lemma cprod_czero: "r *c czero =o czero"
    63   unfolding cprod_def czero_def Field_card_of by (simp add: card_of_empty_ordIso)
    64 
    65 lemma cprod_cone: "Card_order r \<Longrightarrow> r *c cone =o r"
    66   unfolding cprod_def cone_def Field_card_of
    67   by (drule card_of_Field_ordIso) (erule ordIso_transitive[OF card_of_Times_singleton])
    68 
    69 
    70 lemma ordLeq_cprod1: "\<lbrakk>Card_order p1; Cnotzero p2\<rbrakk> \<Longrightarrow> p1 \<le>o p1 *c p2"
    71 unfolding cprod_def by (metis Card_order_Times1 czeroI)
    72 
    73 
    74 subsection \<open>Exponentiation\<close>
    75 
    76 lemma cexp_czero: "r ^c czero =o cone"
    77 unfolding cexp_def czero_def Field_card_of Func_empty by (rule single_cone)
    78 
    79 lemma Pow_cexp_ctwo:
    80   "|Pow A| =o ctwo ^c |A|"
    81 unfolding ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func)
    82 
    83 lemma Cnotzero_cexp:
    84   assumes "Cnotzero q" "Card_order r"
    85   shows "Cnotzero (q ^c r)"
    86 proof (cases "r =o czero")
    87   case False thus ?thesis
    88     apply -
    89     apply (rule Cnotzero_mono)
    90     apply (rule assms(1))
    91     apply (rule Card_order_cexp)
    92     apply (rule ordLeq_cexp1)
    93     apply (rule conjI)
    94     apply (rule notI)
    95     apply (erule notE)
    96     apply (rule ordIso_transitive)
    97     apply assumption
    98     apply (rule czero_ordIso)
    99     apply (rule assms(2))
   100     apply (rule conjunct2)
   101     apply (rule assms(1))
   102   done
   103 next
   104   case True thus ?thesis
   105     apply -
   106     apply (rule Cnotzero_mono)
   107     apply (rule cone_Cnotzero)
   108     apply (rule Card_order_cexp)
   109     apply (rule ordIso_imp_ordLeq)
   110     apply (rule ordIso_symmetric)
   111     apply (rule ordIso_transitive)
   112     apply (rule cexp_cong2)
   113     apply assumption
   114     apply (rule conjunct2)
   115     apply (rule assms(1))
   116     apply (rule assms(2))
   117     apply (rule cexp_czero)
   118   done
   119 qed
   120 
   121 lemma Cinfinite_ctwo_cexp:
   122   "Cinfinite r \<Longrightarrow> Cinfinite (ctwo ^c r)"
   123 unfolding ctwo_def cexp_def cinfinite_def Field_card_of
   124 by (rule conjI, rule infinite_Func, auto)
   125 
   126 lemma cone_ordLeq_iff_Field:
   127   assumes "cone \<le>o r"
   128   shows "Field r \<noteq> {}"
   129 proof (rule ccontr)
   130   assume "\<not> Field r \<noteq> {}"
   131   hence "Field r = {}" by simp
   132   thus False using card_of_empty3
   133     card_of_mono2[OF assms] Cnotzero_imp_not_empty[OF cone_Cnotzero] by auto
   134 qed
   135 
   136 lemma cone_ordLeq_cexp: "cone \<le>o r1 \<Longrightarrow> cone \<le>o r1 ^c r2"
   137 by (simp add: cexp_def cone_def Func_non_emp cone_ordLeq_iff_Field)
   138 
   139 lemma Card_order_czero: "Card_order czero"
   140 by (simp only: card_of_Card_order czero_def)
   141 
   142 lemma cexp_mono2'':
   143   assumes 2: "p2 \<le>o r2"
   144   and n1: "Cnotzero q"
   145   and n2: "Card_order p2"
   146   shows "q ^c p2 \<le>o q ^c r2"
   147 proof (cases "p2 =o (czero :: 'a rel)")
   148   case True
   149   hence "q ^c p2 =o q ^c (czero :: 'a rel)" using n1 n2 cexp_cong2 Card_order_czero by blast
   150   also have "q ^c (czero :: 'a rel) =o cone" using cexp_czero by blast
   151   also have "cone \<le>o q ^c r2" using cone_ordLeq_cexp cone_ordLeq_Cnotzero n1 by blast
   152   finally show ?thesis .
   153 next
   154   case False thus ?thesis using assms cexp_mono2' czeroI by metis
   155 qed
   156 
   157 lemma csum_cexp: "\<lbrakk>Cinfinite r1; Cinfinite r2; Card_order q; ctwo \<le>o q\<rbrakk> \<Longrightarrow>
   158   q ^c r1 +c q ^c r2 \<le>o q ^c (r1 +c r2)"
   159 apply (rule csum_cinfinite_bound)
   160 apply (rule cexp_mono2)
   161 apply (rule ordLeq_csum1)
   162 apply (erule conjunct2)
   163 apply assumption
   164 apply (rule notE)
   165 apply (rule cinfinite_not_czero[of r1])
   166 apply (erule conjunct1)
   167 apply assumption
   168 apply (erule conjunct2)
   169 apply (rule cexp_mono2)
   170 apply (rule ordLeq_csum2)
   171 apply (erule conjunct2)
   172 apply assumption
   173 apply (rule notE)
   174 apply (rule cinfinite_not_czero[of r2])
   175 apply (erule conjunct1)
   176 apply assumption
   177 apply (erule conjunct2)
   178 apply (rule Card_order_cexp)
   179 apply (rule Card_order_cexp)
   180 apply (rule Cinfinite_cexp)
   181 apply assumption
   182 apply (rule Cinfinite_csum)
   183 by (rule disjI1)
   184 
   185 lemma csum_cexp': "\<lbrakk>Cinfinite r; Card_order q; ctwo \<le>o q\<rbrakk> \<Longrightarrow> q +c r \<le>o q ^c r"
   186 apply (rule csum_cinfinite_bound)
   187     apply (metis Cinfinite_Cnotzero ordLeq_cexp1)
   188    apply (metis ordLeq_cexp2)
   189   apply blast+
   190 by (metis Cinfinite_cexp)
   191 
   192 lemma card_of_Sigma_ordLeq_Cinfinite:
   193   "\<lbrakk>Cinfinite r; |I| \<le>o r; \<forall>i \<in> I. |A i| \<le>o r\<rbrakk> \<Longrightarrow> |SIGMA i : I. A i| \<le>o r"
   194 unfolding cinfinite_def by (blast intro: card_of_Sigma_ordLeq_infinite_Field)
   195 
   196 lemma card_order_cexp:
   197   assumes "card_order r1" "card_order r2"
   198   shows "card_order (r1 ^c r2)"
   199 proof -
   200   have "Field r1 = UNIV" "Field r2 = UNIV" using assms card_order_on_Card_order by auto
   201   thus ?thesis unfolding cexp_def Func_def by simp
   202 qed
   203 
   204 lemma Cinfinite_ordLess_cexp:
   205   assumes r: "Cinfinite r"
   206   shows "r <o r ^c r"
   207 proof -
   208   have "r <o ctwo ^c r" using r by (simp only: ordLess_ctwo_cexp)
   209   also have "ctwo ^c r \<le>o r ^c r"
   210     by (rule cexp_mono1[OF ctwo_ordLeq_Cinfinite]) (auto simp: r ctwo_not_czero Card_order_ctwo)
   211   finally show ?thesis .
   212 qed
   213 
   214 lemma infinite_ordLeq_cexp:
   215   assumes "Cinfinite r"
   216   shows "r \<le>o r ^c r"
   217 by (rule ordLess_imp_ordLeq[OF Cinfinite_ordLess_cexp[OF assms]])
   218 
   219 lemma czero_cexp: "Cnotzero r \<Longrightarrow> czero ^c r =o czero"
   220   by (drule Cnotzero_imp_not_empty) (simp add: cexp_def czero_def card_of_empty_ordIso)
   221 
   222 lemma Func_singleton:
   223 fixes x :: 'b and A :: "'a set"
   224 shows "|Func A {x}| =o |{x}|"
   225 proof (rule ordIso_symmetric)
   226   define f where [abs_def]: "f y a = (if y = x \<and> a \<in> A then x else undefined)" for y a
   227   have "Func A {x} \<subseteq> f ` {x}" unfolding f_def Func_def by (force simp: fun_eq_iff)
   228   hence "bij_betw f {x} (Func A {x})" unfolding bij_betw_def inj_on_def f_def Func_def
   229     by (auto split: if_split_asm)
   230   thus "|{x}| =o |Func A {x}|" using card_of_ordIso by blast
   231 qed
   232 
   233 lemma cone_cexp: "cone ^c r =o cone"
   234   unfolding cexp_def cone_def Field_card_of by (rule Func_singleton)
   235 
   236 lemma card_of_Func_squared:
   237   fixes A :: "'a set"
   238   shows "|Func (UNIV :: bool set) A| =o |A \<times> A|"
   239 proof (rule ordIso_symmetric)
   240   define f where "f = (\<lambda>(x::'a,y) b. if A = {} then undefined else if b then x else y)"
   241   have "Func (UNIV :: bool set) A \<subseteq> f ` (A \<times> A)" unfolding f_def Func_def
   242     by (auto simp: image_iff fun_eq_iff split: option.splits if_split_asm) blast
   243   hence "bij_betw f (A \<times> A) (Func (UNIV :: bool set) A)"
   244     unfolding bij_betw_def inj_on_def f_def Func_def by (auto simp: fun_eq_iff)
   245   thus "|A \<times> A| =o |Func (UNIV :: bool set) A|" using card_of_ordIso by blast
   246 qed
   247 
   248 lemma cexp_ctwo: "r ^c ctwo =o r *c r"
   249   unfolding cexp_def ctwo_def cprod_def Field_card_of by (rule card_of_Func_squared)
   250 
   251 lemma card_of_Func_Plus:
   252   fixes A :: "'a set" and B :: "'b set" and C :: "'c set"
   253   shows "|Func (A <+> B) C| =o |Func A C \<times> Func B C|"
   254 proof (rule ordIso_symmetric)
   255   define f where "f = (\<lambda>(g :: 'a => 'c, h::'b \<Rightarrow> 'c) ab. case ab of Inl a \<Rightarrow> g a | Inr b \<Rightarrow> h b)"
   256   define f' where "f' = (\<lambda>(f :: ('a + 'b) \<Rightarrow> 'c). (\<lambda>a. f (Inl a), \<lambda>b. f (Inr b)))"
   257   have "f ` (Func A C \<times> Func B C) \<subseteq> Func (A <+> B) C"
   258     unfolding Func_def f_def by (force split: sum.splits)
   259   moreover have "f' ` Func (A <+> B) C \<subseteq> Func A C \<times> Func B C" unfolding Func_def f'_def by force
   260   moreover have "\<forall>a \<in> Func A C \<times> Func B C. f' (f a) = a" unfolding f'_def f_def Func_def by auto
   261   moreover have "\<forall>a' \<in> Func (A <+> B) C. f (f' a') = a'" unfolding f'_def f_def Func_def
   262     by (auto split: sum.splits)
   263   ultimately have "bij_betw f (Func A C \<times> Func B C) (Func (A <+> B) C)"
   264     by (intro bij_betw_byWitness[of _ f' f])
   265   thus "|Func A C \<times> Func B C| =o |Func (A <+> B) C|" using card_of_ordIso by blast
   266 qed
   267 
   268 lemma cexp_csum: "r ^c (s +c t) =o r ^c s *c r ^c t"
   269   unfolding cexp_def cprod_def csum_def Field_card_of by (rule card_of_Func_Plus)
   270 
   271 
   272 subsection \<open>Powerset\<close>
   273 
   274 definition cpow where "cpow r = |Pow (Field r)|"
   275 
   276 lemma card_order_cpow: "card_order r \<Longrightarrow> card_order (cpow r)"
   277 by (simp only: cpow_def Field_card_order Pow_UNIV card_of_card_order_on)
   278 
   279 lemma cpow_greater_eq: "Card_order r \<Longrightarrow> r \<le>o cpow r"
   280 by (rule ordLess_imp_ordLeq) (simp only: cpow_def Card_order_Pow)
   281 
   282 lemma Cinfinite_cpow: "Cinfinite r \<Longrightarrow> Cinfinite (cpow r)"
   283 unfolding cpow_def cinfinite_def by (metis Field_card_of card_of_Card_order infinite_Pow)
   284 
   285 lemma Card_order_cpow: "Card_order (cpow r)"
   286 unfolding cpow_def by (rule card_of_Card_order)
   287 
   288 lemma cardSuc_ordLeq_cpow: "Card_order r \<Longrightarrow> cardSuc r \<le>o cpow r"
   289 unfolding cpow_def by (metis Card_order_Pow cardSuc_ordLess_ordLeq card_of_Card_order)
   290 
   291 lemma cpow_cexp_ctwo: "cpow r =o ctwo ^c r"
   292 unfolding cpow_def ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func)
   293 
   294 subsection \<open>Inverse image\<close>
   295 
   296 lemma vimage_ordLeq:
   297 assumes "|A| \<le>o k" and "\<forall> a \<in> A. |vimage f {a}| \<le>o k" and "Cinfinite k"
   298 shows "|vimage f A| \<le>o k"
   299 proof-
   300   have "vimage f A = (\<Union>a \<in> A. vimage f {a})" by auto
   301   also have "|\<Union>a \<in> A. vimage f {a}| \<le>o k"
   302   using UNION_Cinfinite_bound[OF assms] .
   303   finally show ?thesis .
   304 qed
   305 
   306 subsection \<open>Maximum\<close>
   307 
   308 definition cmax where
   309   "cmax r s =
   310     (if cinfinite r \<or> cinfinite s then czero +c r +c s
   311      else natLeq_on (max (card (Field r)) (card (Field s))) +c czero)"
   312 
   313 lemma cmax_com: "cmax r s =o cmax s r"
   314   unfolding cmax_def
   315   by (auto simp: max.commute intro: csum_cong2[OF csum_com] csum_cong2[OF czero_ordIso])
   316 
   317 lemma cmax1:
   318   assumes "Card_order r" "Card_order s" "s \<le>o r"
   319   shows "cmax r s =o r"
   320 unfolding cmax_def proof (split if_splits, intro conjI impI)
   321   assume "cinfinite r \<or> cinfinite s"
   322   hence Cinf: "Cinfinite r" using assms(1,3) by (metis cinfinite_mono)
   323   have "czero +c r +c s =o r +c s" by (rule csum_czero2[OF Card_order_csum])
   324   also have "r +c s =o r" by (rule csum_absorb1[OF Cinf assms(3)])
   325   finally show "czero +c r +c s =o r" .
   326 next
   327   assume "\<not> (cinfinite r \<or> cinfinite s)"
   328   hence fin: "finite (Field r)" and "finite (Field s)" unfolding cinfinite_def by simp_all
   329   moreover
   330   { from assms(2) have "|Field s| =o s" by (rule card_of_Field_ordIso)
   331     also from assms(3) have "s \<le>o r" .
   332     also from assms(1) have "r =o |Field r|" by (rule ordIso_symmetric[OF card_of_Field_ordIso])
   333     finally have "|Field s| \<le>o |Field r|" .
   334   }
   335   ultimately have "card (Field s) \<le> card (Field r)" by (subst sym[OF finite_card_of_iff_card2])
   336   hence "max (card (Field r)) (card (Field s)) = card (Field r)" by (rule max_absorb1)
   337   hence "natLeq_on (max (card (Field r)) (card (Field s))) +c czero =
   338     natLeq_on (card (Field r)) +c czero" by simp
   339   also have "\<dots> =o natLeq_on (card (Field r))" by (rule csum_czero1[OF natLeq_on_Card_order])
   340   also have "natLeq_on (card (Field r)) =o |Field r|"
   341     by (rule ordIso_symmetric[OF finite_imp_card_of_natLeq_on[OF fin]])
   342   also from assms(1) have "|Field r| =o r" by (rule card_of_Field_ordIso)
   343   finally show "natLeq_on (max (card (Field r)) (card (Field s))) +c czero =o r" .
   344 qed
   345 
   346 lemma cmax2:
   347   assumes "Card_order r" "Card_order s" "r \<le>o s"
   348   shows "cmax r s =o s"
   349   by (metis assms cmax1 cmax_com ordIso_transitive)
   350 
   351 lemma csum_absorb2: "Cinfinite r2 \<Longrightarrow> r1 \<le>o r2 \<Longrightarrow> r1 +c r2 =o r2"
   352   by (metis csum_absorb2')
   353 
   354 lemma cprod_infinite2': "\<lbrakk>Cnotzero r1; Cinfinite r2; r1 \<le>o r2\<rbrakk> \<Longrightarrow> r1 *c r2 =o r2"
   355   unfolding ordIso_iff_ordLeq
   356   by (intro conjI cprod_cinfinite_bound ordLeq_cprod2 ordLeq_refl)
   357     (auto dest!: ordIso_imp_ordLeq not_ordLeq_ordLess simp: czero_def Card_order_empty)
   358 
   359 context
   360   fixes r s
   361   assumes r: "Cinfinite r"
   362   and     s: "Cinfinite s"
   363 begin
   364 
   365 lemma cmax_csum: "cmax r s =o r +c s"
   366 proof (cases "r \<le>o s")
   367   case True
   368   hence "cmax r s =o s" by (metis cmax2 r s)
   369   also have "s =o r +c s" by (metis True csum_absorb2 ordIso_symmetric s)
   370   finally show ?thesis .
   371 next
   372   case False
   373   hence "s \<le>o r" by (metis ordLeq_total r s card_order_on_def)
   374   hence "cmax r s =o r" by (metis cmax1 r s)
   375   also have "r =o r +c s" by (metis \<open>s \<le>o r\<close> csum_absorb1 ordIso_symmetric r)
   376   finally show ?thesis .
   377 qed
   378 
   379 lemma cmax_cprod: "cmax r s =o r *c s"
   380 proof (cases "r \<le>o s")
   381   case True
   382   hence "cmax r s =o s" by (metis cmax2 r s)
   383   also have "s =o r *c s" by (metis Cinfinite_Cnotzero True cprod_infinite2' ordIso_symmetric r s)
   384   finally show ?thesis .
   385 next
   386   case False
   387   hence "s \<le>o r" by (metis ordLeq_total r s card_order_on_def)
   388   hence "cmax r s =o r" by (metis cmax1 r s)
   389   also have "r =o r *c s" by (metis Cinfinite_Cnotzero \<open>s \<le>o r\<close> cprod_infinite1' ordIso_symmetric r s)
   390   finally show ?thesis .
   391 qed
   392 
   393 end
   394 
   395 lemma Card_order_cmax:
   396 assumes r: "Card_order r" and s: "Card_order s"
   397 shows "Card_order (cmax r s)"
   398 unfolding cmax_def by (auto simp: Card_order_csum)
   399 
   400 lemma ordLeq_cmax:
   401 assumes r: "Card_order r" and s: "Card_order s"
   402 shows "r \<le>o cmax r s \<and> s \<le>o cmax r s"
   403 proof-
   404   {assume "r \<le>o s"
   405    hence ?thesis by (metis cmax2 ordIso_iff_ordLeq ordLeq_transitive r s)
   406   }
   407   moreover
   408   {assume "s \<le>o r"
   409    hence ?thesis using cmax_com by (metis cmax2 ordIso_iff_ordLeq ordLeq_transitive r s)
   410   }
   411   ultimately show ?thesis using r s ordLeq_total unfolding card_order_on_def by auto
   412 qed
   413 
   414 lemmas ordLeq_cmax1 = ordLeq_cmax[THEN conjunct1] and
   415        ordLeq_cmax2 = ordLeq_cmax[THEN conjunct2]
   416 
   417 lemma finite_cmax:
   418 assumes r: "Card_order r" and s: "Card_order s"
   419 shows "finite (Field (cmax r s)) \<longleftrightarrow> finite (Field r) \<and> finite (Field s)"
   420 proof-
   421   {assume "r \<le>o s"
   422    hence ?thesis by (metis cmax2 ordIso_finite_Field ordLeq_finite_Field r s)
   423   }
   424   moreover
   425   {assume "s \<le>o r"
   426    hence ?thesis by (metis cmax1 ordIso_finite_Field ordLeq_finite_Field r s)
   427   }
   428   ultimately show ?thesis using r s ordLeq_total unfolding card_order_on_def by auto
   429 qed
   430 
   431 end