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
```