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