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