src/HOL/Ordinals_and_Cardinals/Cardinal_Order_Relation_Base.thy
author blanchet
Tue Aug 28 17:16:00 2012 +0200 (2012-08-28)
changeset 48975 7f79f94a432c
permissions -rw-r--r--
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet@48975
     1
(*  Title:      HOL/Ordinals_and_Cardinals/Cardinal_Order_Relation_Base.thy
blanchet@48975
     2
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     3
    Copyright   2012
blanchet@48975
     4
blanchet@48975
     5
Cardinal-order relations (base).
blanchet@48975
     6
*)
blanchet@48975
     7
blanchet@48975
     8
header {* Cardinal-Order Relations (Base)  *}
blanchet@48975
     9
blanchet@48975
    10
theory Cardinal_Order_Relation_Base
blanchet@48975
    11
imports Constructions_on_Wellorders_Base
blanchet@48975
    12
begin
blanchet@48975
    13
blanchet@48975
    14
blanchet@48975
    15
text{* In this section, we define cardinal-order relations to be minim well-orders
blanchet@48975
    16
on their field.  Then we define the cardinal of a set to be {\em some} cardinal-order
blanchet@48975
    17
relation on that set, which will be unique up to order isomorphism.  Then we study
blanchet@48975
    18
the connection between cardinals and:
blanchet@48975
    19
\begin{itemize}
blanchet@48975
    20
\item standard set-theoretic constructions: products,
blanchet@48975
    21
sums, unions, lists, powersets, set-of finite sets operator;
blanchet@48975
    22
\item finiteness and infiniteness (in particular, with the numeric cardinal operator
blanchet@48975
    23
for finite sets, @{text "card"}, from the theory @{text "Finite_Sets.thy"}).
blanchet@48975
    24
\end{itemize}
blanchet@48975
    25
%
blanchet@48975
    26
On the way, we define the canonical $\omega$ cardinal and finite cardinals.  We also
blanchet@48975
    27
define (again, up to order isomorphism) the successor of a cardinal, and show that
blanchet@48975
    28
any cardinal admits a successor.
blanchet@48975
    29
blanchet@48975
    30
Main results of this section are the existence of cardinal relations and the
blanchet@48975
    31
facts that, in the presence of infiniteness,
blanchet@48975
    32
most of the standard set-theoretic constructions (except for the powerset)
blanchet@48975
    33
{\em do not increase cardinality}.  In particular, e.g., the set of words/lists over
blanchet@48975
    34
any infinite set has the same cardinality (hence, is in bijection) with that set.
blanchet@48975
    35
*}
blanchet@48975
    36
blanchet@48975
    37
blanchet@48975
    38
subsection {* Cardinal orders *}
blanchet@48975
    39
blanchet@48975
    40
blanchet@48975
    41
text{* A cardinal order in our setting shall be a well-order {\em minim} w.r.t. the
blanchet@48975
    42
order-embedding relation, @{text "\<le>o"} (which is the same as being {\em minimal} w.r.t. the
blanchet@48975
    43
strict order-embedding relation, @{text "<o"}), among all the well-orders on its field.  *}
blanchet@48975
    44
blanchet@48975
    45
definition card_order_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
blanchet@48975
    46
where
blanchet@48975
    47
"card_order_on A r \<equiv> well_order_on A r \<and> (\<forall>r'. well_order_on A r' \<longrightarrow> r \<le>o r')"
blanchet@48975
    48
blanchet@48975
    49
blanchet@48975
    50
abbreviation "Card_order r \<equiv> card_order_on (Field r) r"
blanchet@48975
    51
abbreviation "card_order r \<equiv> card_order_on UNIV r"
blanchet@48975
    52
blanchet@48975
    53
blanchet@48975
    54
lemma card_order_on_well_order_on:
blanchet@48975
    55
assumes "card_order_on A r"
blanchet@48975
    56
shows "well_order_on A r"
blanchet@48975
    57
using assms unfolding card_order_on_def by simp
blanchet@48975
    58
blanchet@48975
    59
blanchet@48975
    60
lemma card_order_on_Card_order:
blanchet@48975
    61
"card_order_on A r \<Longrightarrow> A = Field r \<and> Card_order r"
blanchet@48975
    62
unfolding card_order_on_def using rel.well_order_on_Field by blast
blanchet@48975
    63
blanchet@48975
    64
blanchet@48975
    65
text{* The existence of a cardinal relation on any given set (which will mean
blanchet@48975
    66
that any set has a cardinal) follows from two facts:
blanchet@48975
    67
\begin{itemize}
blanchet@48975
    68
\item Zermelo's theorem (proved in @{text "Zorn.thy"} as theorem @{text "well_order_on"}),
blanchet@48975
    69
which states that on any given set there exists a well-order;
blanchet@48975
    70
\item The well-founded-ness of @{text "<o"}, ensuring that then there exists a minimal
blanchet@48975
    71
such well-order, i.e., a cardinal order.
blanchet@48975
    72
\end{itemize}
blanchet@48975
    73
*}
blanchet@48975
    74
blanchet@48975
    75
blanchet@48975
    76
theorem card_order_on: "\<exists>r. card_order_on A r"
blanchet@48975
    77
proof-
blanchet@48975
    78
  obtain R where R_def: "R = {r. well_order_on A r}" by blast
blanchet@48975
    79
  have 1: "R \<noteq> {} \<and> (\<forall>r \<in> R. Well_order r)"
blanchet@48975
    80
  using well_order_on[of A] R_def rel.well_order_on_Well_order by blast
blanchet@48975
    81
  hence "\<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"
blanchet@48975
    82
  using  exists_minim_Well_order[of R] by auto
blanchet@48975
    83
  thus ?thesis using R_def unfolding card_order_on_def by auto
blanchet@48975
    84
qed
blanchet@48975
    85
blanchet@48975
    86
blanchet@48975
    87
lemma card_order_on_ordIso:
blanchet@48975
    88
assumes CO: "card_order_on A r" and CO': "card_order_on A r'"
blanchet@48975
    89
shows "r =o r'"
blanchet@48975
    90
using assms unfolding card_order_on_def
blanchet@48975
    91
using ordIso_iff_ordLeq by blast
blanchet@48975
    92
blanchet@48975
    93
blanchet@48975
    94
lemma Card_order_ordIso:
blanchet@48975
    95
assumes CO: "Card_order r" and ISO: "r' =o r"
blanchet@48975
    96
shows "Card_order r'"
blanchet@48975
    97
using ISO unfolding ordIso_def
blanchet@48975
    98
proof(unfold card_order_on_def, auto)
blanchet@48975
    99
  fix p' assume "well_order_on (Field r') p'"
blanchet@48975
   100
  hence 0: "Well_order p' \<and> Field p' = Field r'"
blanchet@48975
   101
  using rel.well_order_on_Well_order by blast
blanchet@48975
   102
  obtain f where 1: "iso r' r f" and 2: "Well_order r \<and> Well_order r'"
blanchet@48975
   103
  using ISO unfolding ordIso_def by auto
blanchet@48975
   104
  hence 3: "inj_on f (Field r') \<and> f ` (Field r') = Field r"
blanchet@48975
   105
  by (auto simp add: iso_iff embed_inj_on)
blanchet@48975
   106
  let ?p = "dir_image p' f"
blanchet@48975
   107
  have 4: "p' =o ?p \<and> Well_order ?p"
blanchet@48975
   108
  using 0 2 3 by (auto simp add: dir_image_ordIso Well_order_dir_image)
blanchet@48975
   109
  moreover have "Field ?p =  Field r"
blanchet@48975
   110
  using 0 3 by (auto simp add: dir_image_Field2 order_on_defs)
blanchet@48975
   111
  ultimately have "well_order_on (Field r) ?p" by auto
blanchet@48975
   112
  hence "r \<le>o ?p" using CO unfolding card_order_on_def by auto
blanchet@48975
   113
  thus "r' \<le>o p'"
blanchet@48975
   114
  using ISO 4 ordLeq_ordIso_trans ordIso_ordLeq_trans ordIso_symmetric by blast
blanchet@48975
   115
qed
blanchet@48975
   116
blanchet@48975
   117
blanchet@48975
   118
lemma Card_order_ordIso2:
blanchet@48975
   119
assumes CO: "Card_order r" and ISO: "r =o r'"
blanchet@48975
   120
shows "Card_order r'"
blanchet@48975
   121
using assms Card_order_ordIso ordIso_symmetric by blast
blanchet@48975
   122
blanchet@48975
   123
blanchet@48975
   124
subsection {* Cardinal of a set *}
blanchet@48975
   125
blanchet@48975
   126
blanchet@48975
   127
text{* We define the cardinal of set to be {\em some} cardinal order on that set.
blanchet@48975
   128
We shall prove that this notion is unique up to order isomorphism, meaning
blanchet@48975
   129
that order isomorphism shall be the true identity of cardinals.  *}
blanchet@48975
   130
blanchet@48975
   131
blanchet@48975
   132
definition card_of :: "'a set \<Rightarrow> 'a rel" ("|_|" )
blanchet@48975
   133
where "card_of A = (SOME r. card_order_on A r)"
blanchet@48975
   134
blanchet@48975
   135
blanchet@48975
   136
lemma card_of_card_order_on: "card_order_on A |A|"
blanchet@48975
   137
unfolding card_of_def by (auto simp add: card_order_on someI_ex)
blanchet@48975
   138
blanchet@48975
   139
blanchet@48975
   140
lemma card_of_well_order_on: "well_order_on A |A|"
blanchet@48975
   141
using card_of_card_order_on card_order_on_def by blast
blanchet@48975
   142
blanchet@48975
   143
blanchet@48975
   144
lemma Field_card_of: "Field |A| = A"
blanchet@48975
   145
using card_of_card_order_on[of A] unfolding card_order_on_def
blanchet@48975
   146
using rel.well_order_on_Field by blast
blanchet@48975
   147
blanchet@48975
   148
blanchet@48975
   149
lemma card_of_Card_order: "Card_order |A|"
blanchet@48975
   150
by (simp only: card_of_card_order_on Field_card_of)
blanchet@48975
   151
blanchet@48975
   152
blanchet@48975
   153
corollary ordIso_card_of_imp_Card_order:
blanchet@48975
   154
"r =o |A| \<Longrightarrow> Card_order r"
blanchet@48975
   155
using card_of_Card_order Card_order_ordIso by blast
blanchet@48975
   156
blanchet@48975
   157
blanchet@48975
   158
lemma card_of_Well_order: "Well_order |A|"
blanchet@48975
   159
using card_of_Card_order unfolding  card_order_on_def by auto
blanchet@48975
   160
blanchet@48975
   161
blanchet@48975
   162
lemma card_of_refl: "|A| =o |A|"
blanchet@48975
   163
using card_of_Well_order ordIso_reflexive by blast
blanchet@48975
   164
blanchet@48975
   165
blanchet@48975
   166
lemma card_of_least: "well_order_on A r \<Longrightarrow> |A| \<le>o r"
blanchet@48975
   167
using card_of_card_order_on unfolding card_order_on_def by blast
blanchet@48975
   168
blanchet@48975
   169
blanchet@48975
   170
lemma card_of_ordIso:
blanchet@48975
   171
"(\<exists>f. bij_betw f A B) = ( |A| =o |B| )"
blanchet@48975
   172
proof(auto)
blanchet@48975
   173
  fix f assume *: "bij_betw f A B"
blanchet@48975
   174
  then obtain r where "well_order_on B r \<and> |A| =o r"
blanchet@48975
   175
  using Well_order_iso_copy card_of_well_order_on by blast
blanchet@48975
   176
  hence "|B| \<le>o |A|" using card_of_least
blanchet@48975
   177
  ordLeq_ordIso_trans ordIso_symmetric by blast
blanchet@48975
   178
  moreover
blanchet@48975
   179
  {let ?g = "inv_into A f"
blanchet@48975
   180
   have "bij_betw ?g B A" using * bij_betw_inv_into by blast
blanchet@48975
   181
   then obtain r where "well_order_on A r \<and> |B| =o r"
blanchet@48975
   182
   using Well_order_iso_copy card_of_well_order_on by blast
blanchet@48975
   183
   hence "|A| \<le>o |B|" using card_of_least
blanchet@48975
   184
   ordLeq_ordIso_trans ordIso_symmetric by blast
blanchet@48975
   185
  }
blanchet@48975
   186
  ultimately show "|A| =o |B|" using ordIso_iff_ordLeq by blast
blanchet@48975
   187
next
blanchet@48975
   188
  assume "|A| =o |B|"
blanchet@48975
   189
  then obtain f where "iso ( |A| ) ( |B| ) f"
blanchet@48975
   190
  unfolding ordIso_def by auto
blanchet@48975
   191
  hence "bij_betw f A B" unfolding iso_def Field_card_of by simp
blanchet@48975
   192
  thus "\<exists>f. bij_betw f A B" by auto
blanchet@48975
   193
qed
blanchet@48975
   194
blanchet@48975
   195
blanchet@48975
   196
lemma card_of_ordLeq:
blanchet@48975
   197
"(\<exists>f. inj_on f A \<and> f ` A \<le> B) = ( |A| \<le>o |B| )"
blanchet@48975
   198
proof(auto)
blanchet@48975
   199
  fix f assume *: "inj_on f A" and **: "f ` A \<le> B"
blanchet@48975
   200
  {assume "|B| <o |A|"
blanchet@48975
   201
   hence "|B| \<le>o |A|" using ordLeq_iff_ordLess_or_ordIso by blast
blanchet@48975
   202
   then obtain g where "embed ( |B| ) ( |A| ) g"
blanchet@48975
   203
   unfolding ordLeq_def by auto
blanchet@48975
   204
   hence 1: "inj_on g B \<and> g ` B \<le> A" using embed_inj_on[of "|B|" "|A|" "g"]
blanchet@48975
   205
   card_of_Well_order[of "B"] Field_card_of[of "B"] Field_card_of[of "A"]
blanchet@48975
   206
   embed_Field[of "|B|" "|A|" g] by auto
blanchet@48975
   207
   obtain h where "bij_betw h A B"
blanchet@48975
   208
   using * ** 1 Cantor_Bernstein[of f] by fastforce
blanchet@48975
   209
   hence "|A| =o |B|" using card_of_ordIso by blast
blanchet@48975
   210
   hence "|A| \<le>o |B|" using ordIso_iff_ordLeq by auto
blanchet@48975
   211
  }
blanchet@48975
   212
  thus "|A| \<le>o |B|" using ordLess_or_ordLeq[of "|B|" "|A|"]
blanchet@48975
   213
  by (auto simp: card_of_Well_order)
blanchet@48975
   214
next
blanchet@48975
   215
  assume *: "|A| \<le>o |B|"
blanchet@48975
   216
  obtain f where "embed ( |A| ) ( |B| ) f"
blanchet@48975
   217
  using * unfolding ordLeq_def by auto
blanchet@48975
   218
  hence "inj_on f A \<and> f ` A \<le> B" using embed_inj_on[of "|A|" "|B|" f]
blanchet@48975
   219
  card_of_Well_order[of "A"] Field_card_of[of "A"] Field_card_of[of "B"]
blanchet@48975
   220
  embed_Field[of "|A|" "|B|" f] by auto
blanchet@48975
   221
  thus "\<exists>f. inj_on f A \<and> f ` A \<le> B" by auto
blanchet@48975
   222
qed
blanchet@48975
   223
blanchet@48975
   224
blanchet@48975
   225
lemma card_of_ordLeq2:
blanchet@48975
   226
"A \<noteq> {} \<Longrightarrow> (\<exists>g. g ` B = A) = ( |A| \<le>o |B| )"
blanchet@48975
   227
using card_of_ordLeq[of A B] inj_on_iff_surj[of A B] by auto
blanchet@48975
   228
blanchet@48975
   229
blanchet@48975
   230
lemma card_of_ordLess:
blanchet@48975
   231
"(\<not>(\<exists>f. inj_on f A \<and> f ` A \<le> B)) = ( |B| <o |A| )"
blanchet@48975
   232
proof-
blanchet@48975
   233
  have "(\<not>(\<exists>f. inj_on f A \<and> f ` A \<le> B)) = (\<not> |A| \<le>o |B| )"
blanchet@48975
   234
  using card_of_ordLeq by blast
blanchet@48975
   235
  also have "\<dots> = ( |B| <o |A| )"
blanchet@48975
   236
  using card_of_Well_order[of A] card_of_Well_order[of B]
blanchet@48975
   237
        not_ordLeq_iff_ordLess by blast
blanchet@48975
   238
  finally show ?thesis .
blanchet@48975
   239
qed
blanchet@48975
   240
blanchet@48975
   241
blanchet@48975
   242
lemma card_of_ordLess2:
blanchet@48975
   243
"B \<noteq> {} \<Longrightarrow> (\<not>(\<exists>f. f ` A = B)) = ( |A| <o |B| )"
blanchet@48975
   244
using card_of_ordLess[of B A] inj_on_iff_surj[of B A] by auto
blanchet@48975
   245
blanchet@48975
   246
blanchet@48975
   247
lemma card_of_ordIsoI:
blanchet@48975
   248
assumes "bij_betw f A B"
blanchet@48975
   249
shows "|A| =o |B|"
blanchet@48975
   250
using assms unfolding card_of_ordIso[symmetric] by auto
blanchet@48975
   251
blanchet@48975
   252
blanchet@48975
   253
lemma card_of_ordLeqI:
blanchet@48975
   254
assumes "inj_on f A" and "\<And> a. a \<in> A \<Longrightarrow> f a \<in> B"
blanchet@48975
   255
shows "|A| \<le>o |B|"
blanchet@48975
   256
using assms unfolding card_of_ordLeq[symmetric] by auto
blanchet@48975
   257
blanchet@48975
   258
blanchet@48975
   259
lemma card_of_unique:
blanchet@48975
   260
"card_order_on A r \<Longrightarrow> r =o |A|"
blanchet@48975
   261
by (simp only: card_order_on_ordIso card_of_card_order_on)
blanchet@48975
   262
blanchet@48975
   263
blanchet@48975
   264
lemma card_of_mono1:
blanchet@48975
   265
"A \<le> B \<Longrightarrow> |A| \<le>o |B|"
blanchet@48975
   266
using inj_on_id[of A] card_of_ordLeq[of A B] by fastforce
blanchet@48975
   267
blanchet@48975
   268
blanchet@48975
   269
lemma card_of_mono2:
blanchet@48975
   270
assumes "r \<le>o r'"
blanchet@48975
   271
shows "|Field r| \<le>o |Field r'|"
blanchet@48975
   272
proof-
blanchet@48975
   273
  obtain f where
blanchet@48975
   274
  1: "well_order_on (Field r) r \<and> well_order_on (Field r) r \<and> embed r r' f"
blanchet@48975
   275
  using assms unfolding ordLeq_def
blanchet@48975
   276
  by (auto simp add: rel.well_order_on_Well_order)
blanchet@48975
   277
  hence "inj_on f (Field r) \<and> f ` (Field r) \<le> Field r'"
blanchet@48975
   278
  by (auto simp add: embed_inj_on embed_Field)
blanchet@48975
   279
  thus "|Field r| \<le>o |Field r'|" using card_of_ordLeq by blast
blanchet@48975
   280
qed
blanchet@48975
   281
blanchet@48975
   282
blanchet@48975
   283
lemma card_of_cong: "r =o r' \<Longrightarrow> |Field r| =o |Field r'|"
blanchet@48975
   284
by (simp add: ordIso_iff_ordLeq card_of_mono2)
blanchet@48975
   285
blanchet@48975
   286
blanchet@48975
   287
lemma card_of_Field_ordLess: "Well_order r \<Longrightarrow> |Field r| \<le>o r"
blanchet@48975
   288
using card_of_least card_of_well_order_on rel.well_order_on_Well_order by blast
blanchet@48975
   289
blanchet@48975
   290
blanchet@48975
   291
lemma card_of_Field_ordIso:
blanchet@48975
   292
assumes "Card_order r"
blanchet@48975
   293
shows "|Field r| =o r"
blanchet@48975
   294
proof-
blanchet@48975
   295
  have "card_order_on (Field r) r"
blanchet@48975
   296
  using assms card_order_on_Card_order by blast
blanchet@48975
   297
  moreover have "card_order_on (Field r) |Field r|"
blanchet@48975
   298
  using card_of_card_order_on by blast
blanchet@48975
   299
  ultimately show ?thesis using card_order_on_ordIso by blast
blanchet@48975
   300
qed
blanchet@48975
   301
blanchet@48975
   302
blanchet@48975
   303
lemma Card_order_iff_ordIso_card_of:
blanchet@48975
   304
"Card_order r = (r =o |Field r| )"
blanchet@48975
   305
using ordIso_card_of_imp_Card_order card_of_Field_ordIso ordIso_symmetric by blast
blanchet@48975
   306
blanchet@48975
   307
blanchet@48975
   308
lemma Card_order_iff_ordLeq_card_of:
blanchet@48975
   309
"Card_order r = (r \<le>o |Field r| )"
blanchet@48975
   310
proof-
blanchet@48975
   311
  have "Card_order r = (r =o |Field r| )"
blanchet@48975
   312
  unfolding Card_order_iff_ordIso_card_of by simp
blanchet@48975
   313
  also have "... = (r \<le>o |Field r| \<and> |Field r| \<le>o r)"
blanchet@48975
   314
  unfolding ordIso_iff_ordLeq by simp
blanchet@48975
   315
  also have "... = (r \<le>o |Field r| )"
blanchet@48975
   316
  using card_of_Field_ordLess
blanchet@48975
   317
  by (auto simp: card_of_Field_ordLess ordLeq_Well_order_simp)
blanchet@48975
   318
  finally show ?thesis .
blanchet@48975
   319
qed
blanchet@48975
   320
blanchet@48975
   321
blanchet@48975
   322
lemma Card_order_iff_Restr_underS:
blanchet@48975
   323
assumes "Well_order r"
blanchet@48975
   324
shows "Card_order r = (\<forall>a \<in> Field r. Restr r (rel.underS r a) <o |Field r| )"
blanchet@48975
   325
using assms unfolding Card_order_iff_ordLeq_card_of
blanchet@48975
   326
using ordLeq_iff_ordLess_Restr card_of_Well_order by blast
blanchet@48975
   327
blanchet@48975
   328
blanchet@48975
   329
lemma card_of_underS:
blanchet@48975
   330
assumes r: "Card_order r" and a: "a : Field r"
blanchet@48975
   331
shows "|rel.underS r a| <o r"
blanchet@48975
   332
proof-
blanchet@48975
   333
  let ?A = "rel.underS r a"  let ?r' = "Restr r ?A"
blanchet@48975
   334
  have 1: "Well_order r"
blanchet@48975
   335
  using r unfolding card_order_on_def by simp
blanchet@48975
   336
  have "Well_order ?r'" using 1 Well_order_Restr by auto
blanchet@48975
   337
  moreover have "card_order_on (Field ?r') |Field ?r'|"
blanchet@48975
   338
  using card_of_card_order_on .
blanchet@48975
   339
  ultimately have "|Field ?r'| \<le>o ?r'"
blanchet@48975
   340
  unfolding card_order_on_def by simp
blanchet@48975
   341
  moreover have "Field ?r' = ?A"
blanchet@48975
   342
  using 1 wo_rel.underS_ofilter Field_Restr_ofilter
blanchet@48975
   343
  unfolding wo_rel_def by fastforce
blanchet@48975
   344
  ultimately have "|?A| \<le>o ?r'" by simp
blanchet@48975
   345
  also have "?r' <o |Field r|"
blanchet@48975
   346
  using 1 a r Card_order_iff_Restr_underS by blast
blanchet@48975
   347
  also have "|Field r| =o r"
blanchet@48975
   348
  using r ordIso_symmetric unfolding Card_order_iff_ordIso_card_of by auto
blanchet@48975
   349
  finally show ?thesis .
blanchet@48975
   350
qed
blanchet@48975
   351
blanchet@48975
   352
blanchet@48975
   353
lemma ordLess_Field:
blanchet@48975
   354
assumes "r <o r'"
blanchet@48975
   355
shows "|Field r| <o r'"
blanchet@48975
   356
proof-
blanchet@48975
   357
  have "well_order_on (Field r) r" using assms unfolding ordLess_def
blanchet@48975
   358
  by (auto simp add: rel.well_order_on_Well_order)
blanchet@48975
   359
  hence "|Field r| \<le>o r" using card_of_least by blast
blanchet@48975
   360
  thus ?thesis using assms ordLeq_ordLess_trans by blast
blanchet@48975
   361
qed
blanchet@48975
   362
blanchet@48975
   363
blanchet@48975
   364
lemma internalize_card_of_ordLeq:
blanchet@48975
   365
"( |A| \<le>o r) = (\<exists>B \<le> Field r. |A| =o |B| \<and> |B| \<le>o r)"
blanchet@48975
   366
proof
blanchet@48975
   367
  assume "|A| \<le>o r"
blanchet@48975
   368
  then obtain p where 1: "Field p \<le> Field r \<and> |A| =o p \<and> p \<le>o r"
blanchet@48975
   369
  using internalize_ordLeq[of "|A|" r] by blast
blanchet@48975
   370
  hence "Card_order p" using card_of_Card_order Card_order_ordIso2 by blast
blanchet@48975
   371
  hence "|Field p| =o p" using card_of_Field_ordIso by blast
blanchet@48975
   372
  hence "|A| =o |Field p| \<and> |Field p| \<le>o r"
blanchet@48975
   373
  using 1 ordIso_equivalence ordIso_ordLeq_trans by blast
blanchet@48975
   374
  thus "\<exists>B \<le> Field r. |A| =o |B| \<and> |B| \<le>o r" using 1 by blast
blanchet@48975
   375
next
blanchet@48975
   376
  assume "\<exists>B \<le> Field r. |A| =o |B| \<and> |B| \<le>o r"
blanchet@48975
   377
  thus "|A| \<le>o r" using ordIso_ordLeq_trans by blast
blanchet@48975
   378
qed
blanchet@48975
   379
blanchet@48975
   380
blanchet@48975
   381
lemma internalize_card_of_ordLeq2:
blanchet@48975
   382
"( |A| \<le>o |C| ) = (\<exists>B \<le> C. |A| =o |B| \<and> |B| \<le>o |C| )"
blanchet@48975
   383
using internalize_card_of_ordLeq[of "A" "|C|"] Field_card_of[of C] by auto
blanchet@48975
   384
blanchet@48975
   385
blanchet@48975
   386
blanchet@48975
   387
subsection {* Cardinals versus set operations on arbitrary sets *}
blanchet@48975
   388
blanchet@48975
   389
blanchet@48975
   390
text{* Here we embark in a long journey of simple results showing
blanchet@48975
   391
that the standard set-theoretic operations are well-behaved w.r.t. the notion of
blanchet@48975
   392
cardinal -- essentially, this means that they preserve the ``cardinal identity"
blanchet@48975
   393
@{text "=o"} and are monotonic w.r.t. @{text "\<le>o"}.
blanchet@48975
   394
*}
blanchet@48975
   395
blanchet@48975
   396
blanchet@48975
   397
lemma card_of_empty: "|{}| \<le>o |A|"
blanchet@48975
   398
using card_of_ordLeq inj_on_id by blast
blanchet@48975
   399
blanchet@48975
   400
blanchet@48975
   401
lemma card_of_empty1:
blanchet@48975
   402
assumes "Well_order r \<or> Card_order r"
blanchet@48975
   403
shows "|{}| \<le>o r"
blanchet@48975
   404
proof-
blanchet@48975
   405
  have "Well_order r" using assms unfolding card_order_on_def by auto
blanchet@48975
   406
  hence "|Field r| <=o r"
blanchet@48975
   407
  using assms card_of_Field_ordLess by blast
blanchet@48975
   408
  moreover have "|{}| \<le>o |Field r|" by (simp add: card_of_empty)
blanchet@48975
   409
  ultimately show ?thesis using ordLeq_transitive by blast
blanchet@48975
   410
qed
blanchet@48975
   411
blanchet@48975
   412
blanchet@48975
   413
corollary Card_order_empty:
blanchet@48975
   414
"Card_order r \<Longrightarrow> |{}| \<le>o r" by (simp add: card_of_empty1)
blanchet@48975
   415
blanchet@48975
   416
blanchet@48975
   417
lemma card_of_empty2:
blanchet@48975
   418
assumes LEQ: "|A| =o |{}|"
blanchet@48975
   419
shows "A = {}"
blanchet@48975
   420
using assms card_of_ordIso[of A] bij_betw_empty2 by blast
blanchet@48975
   421
blanchet@48975
   422
blanchet@48975
   423
lemma card_of_empty3:
blanchet@48975
   424
assumes LEQ: "|A| \<le>o |{}|"
blanchet@48975
   425
shows "A = {}"
blanchet@48975
   426
using assms
blanchet@48975
   427
by (simp add: ordIso_iff_ordLeq card_of_empty1 card_of_empty2
blanchet@48975
   428
              ordLeq_Well_order_simp)
blanchet@48975
   429
blanchet@48975
   430
blanchet@48975
   431
lemma card_of_empty_ordIso:
blanchet@48975
   432
"|{}::'a set| =o |{}::'b set|"
blanchet@48975
   433
using card_of_ordIso unfolding bij_betw_def inj_on_def by blast
blanchet@48975
   434
blanchet@48975
   435
blanchet@48975
   436
lemma card_of_image:
blanchet@48975
   437
"|f ` A| <=o |A|"
blanchet@48975
   438
proof(cases "A = {}", simp add: card_of_empty)
blanchet@48975
   439
  assume "A ~= {}"
blanchet@48975
   440
  hence "f ` A ~= {}" by auto
blanchet@48975
   441
  thus "|f ` A| \<le>o |A|"
blanchet@48975
   442
  using card_of_ordLeq2[of "f ` A" A] by auto
blanchet@48975
   443
qed
blanchet@48975
   444
blanchet@48975
   445
blanchet@48975
   446
lemma surj_imp_ordLeq:
blanchet@48975
   447
assumes "B <= f ` A"
blanchet@48975
   448
shows "|B| <=o |A|"
blanchet@48975
   449
proof-
blanchet@48975
   450
  have "|B| <=o |f ` A|" using assms card_of_mono1 by auto
blanchet@48975
   451
  thus ?thesis using card_of_image ordLeq_transitive by blast
blanchet@48975
   452
qed
blanchet@48975
   453
blanchet@48975
   454
blanchet@48975
   455
lemma card_of_ordLeqI2:
blanchet@48975
   456
assumes "B \<subseteq> f ` A"
blanchet@48975
   457
shows "|B| \<le>o |A|"
blanchet@48975
   458
using assms by (metis surj_imp_ordLeq)
blanchet@48975
   459
blanchet@48975
   460
blanchet@48975
   461
lemma card_of_singl_ordLeq:
blanchet@48975
   462
assumes "A \<noteq> {}"
blanchet@48975
   463
shows "|{b}| \<le>o |A|"
blanchet@48975
   464
proof-
blanchet@48975
   465
  obtain a where *: "a \<in> A" using assms by auto
blanchet@48975
   466
  let ?h = "\<lambda> b'::'b. if b' = b then a else undefined"
blanchet@48975
   467
  have "inj_on ?h {b} \<and> ?h ` {b} \<le> A"
blanchet@48975
   468
  using * unfolding inj_on_def by auto
blanchet@48975
   469
  thus ?thesis using card_of_ordLeq by blast
blanchet@48975
   470
qed
blanchet@48975
   471
blanchet@48975
   472
blanchet@48975
   473
corollary Card_order_singl_ordLeq:
blanchet@48975
   474
"\<lbrakk>Card_order r; Field r \<noteq> {}\<rbrakk> \<Longrightarrow> |{b}| \<le>o r"
blanchet@48975
   475
using card_of_singl_ordLeq[of "Field r" b]
blanchet@48975
   476
      card_of_Field_ordIso[of r] ordLeq_ordIso_trans by blast
blanchet@48975
   477
blanchet@48975
   478
blanchet@48975
   479
lemma card_of_Pow: "|A| <o |Pow A|"
blanchet@48975
   480
using card_of_ordLess2[of "Pow A" A]  Cantors_paradox[of A]
blanchet@48975
   481
      Pow_not_empty[of A] by auto
blanchet@48975
   482
blanchet@48975
   483
blanchet@48975
   484
lemma infinite_Pow:
blanchet@48975
   485
assumes "infinite A"
blanchet@48975
   486
shows "infinite (Pow A)"
blanchet@48975
   487
proof-
blanchet@48975
   488
  have "|A| \<le>o |Pow A|" by (metis card_of_Pow ordLess_imp_ordLeq)
blanchet@48975
   489
  thus ?thesis by (metis assms finite_Pow_iff)
blanchet@48975
   490
qed
blanchet@48975
   491
blanchet@48975
   492
blanchet@48975
   493
corollary Card_order_Pow:
blanchet@48975
   494
"Card_order r \<Longrightarrow> r <o |Pow(Field r)|"
blanchet@48975
   495
using card_of_Pow card_of_Field_ordIso ordIso_ordLess_trans ordIso_symmetric by blast
blanchet@48975
   496
blanchet@48975
   497
blanchet@48975
   498
corollary card_of_set_type: "|UNIV::'a set| <o |UNIV::'a set set|"
blanchet@48975
   499
using card_of_Pow[of "UNIV::'a set"] by simp
blanchet@48975
   500
blanchet@48975
   501
blanchet@48975
   502
lemma card_of_Plus1: "|A| \<le>o |A <+> B|"
blanchet@48975
   503
proof-
blanchet@48975
   504
  have "Inl ` A \<le> A <+> B" by auto
blanchet@48975
   505
  thus ?thesis using inj_Inl[of A] card_of_ordLeq by blast
blanchet@48975
   506
qed
blanchet@48975
   507
blanchet@48975
   508
blanchet@48975
   509
corollary Card_order_Plus1:
blanchet@48975
   510
"Card_order r \<Longrightarrow> r \<le>o |(Field r) <+> B|"
blanchet@48975
   511
using card_of_Plus1 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
blanchet@48975
   512
blanchet@48975
   513
blanchet@48975
   514
lemma card_of_Plus2: "|B| \<le>o |A <+> B|"
blanchet@48975
   515
proof-
blanchet@48975
   516
  have "Inr ` B \<le> A <+> B" by auto
blanchet@48975
   517
  thus ?thesis using inj_Inr[of B] card_of_ordLeq by blast
blanchet@48975
   518
qed
blanchet@48975
   519
blanchet@48975
   520
blanchet@48975
   521
corollary Card_order_Plus2:
blanchet@48975
   522
"Card_order r \<Longrightarrow> r \<le>o |A <+> (Field r)|"
blanchet@48975
   523
using card_of_Plus2 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
blanchet@48975
   524
blanchet@48975
   525
blanchet@48975
   526
lemma card_of_Plus_empty1: "|A| =o |A <+> {}|"
blanchet@48975
   527
proof-
blanchet@48975
   528
  have "bij_betw Inl A (A <+> {})" unfolding bij_betw_def inj_on_def by auto
blanchet@48975
   529
  thus ?thesis using card_of_ordIso by auto
blanchet@48975
   530
qed
blanchet@48975
   531
blanchet@48975
   532
blanchet@48975
   533
lemma card_of_Plus_empty2: "|A| =o |{} <+> A|"
blanchet@48975
   534
proof-
blanchet@48975
   535
  have "bij_betw Inr A ({} <+> A)" unfolding bij_betw_def inj_on_def by auto
blanchet@48975
   536
  thus ?thesis using card_of_ordIso by auto
blanchet@48975
   537
qed
blanchet@48975
   538
blanchet@48975
   539
blanchet@48975
   540
lemma card_of_Plus_commute: "|A <+> B| =o |B <+> A|"
blanchet@48975
   541
proof-
blanchet@48975
   542
  let ?f = "\<lambda>(c::'a + 'b). case c of Inl a \<Rightarrow> Inr a
blanchet@48975
   543
                                   | Inr b \<Rightarrow> Inl b"
blanchet@48975
   544
  have "bij_betw ?f (A <+> B) (B <+> A)"
blanchet@48975
   545
  unfolding bij_betw_def inj_on_def by force
blanchet@48975
   546
  thus ?thesis using card_of_ordIso by blast
blanchet@48975
   547
qed
blanchet@48975
   548
blanchet@48975
   549
blanchet@48975
   550
lemma card_of_Plus_assoc:
blanchet@48975
   551
fixes A :: "'a set" and B :: "'b set" and C :: "'c set"
blanchet@48975
   552
shows "|(A <+> B) <+> C| =o |A <+> B <+> C|"
blanchet@48975
   553
proof -
blanchet@48975
   554
  def f \<equiv> "\<lambda>(k::('a + 'b) + 'c).
blanchet@48975
   555
  case k of Inl ab \<Rightarrow> (case ab of Inl a \<Rightarrow> Inl a
blanchet@48975
   556
                                 |Inr b \<Rightarrow> Inr (Inl b))
blanchet@48975
   557
           |Inr c \<Rightarrow> Inr (Inr c)"
blanchet@48975
   558
  have "A <+> B <+> C \<subseteq> f ` ((A <+> B) <+> C)"
blanchet@48975
   559
  proof
blanchet@48975
   560
    fix x assume x: "x \<in> A <+> B <+> C"
blanchet@48975
   561
    show "x \<in> f ` ((A <+> B) <+> C)"
blanchet@48975
   562
    proof(cases x)
blanchet@48975
   563
      case (Inl a)
blanchet@48975
   564
      hence "a \<in> A" "x = f (Inl (Inl a))"
blanchet@48975
   565
      using x unfolding f_def by auto
blanchet@48975
   566
      thus ?thesis by auto
blanchet@48975
   567
    next
blanchet@48975
   568
      case (Inr bc) note 1 = Inr show ?thesis
blanchet@48975
   569
      proof(cases bc)
blanchet@48975
   570
        case (Inl b)
blanchet@48975
   571
        hence "b \<in> B" "x = f (Inl (Inr b))"
blanchet@48975
   572
        using x 1 unfolding f_def by auto
blanchet@48975
   573
        thus ?thesis by auto
blanchet@48975
   574
      next
blanchet@48975
   575
        case (Inr c)
blanchet@48975
   576
        hence "c \<in> C" "x = f (Inr c)"
blanchet@48975
   577
        using x 1 unfolding f_def by auto
blanchet@48975
   578
        thus ?thesis by auto
blanchet@48975
   579
      qed
blanchet@48975
   580
    qed
blanchet@48975
   581
  qed
blanchet@48975
   582
  hence "bij_betw f ((A <+> B) <+> C) (A <+> B <+> C)"
blanchet@48975
   583
  unfolding bij_betw_def inj_on_def f_def by auto
blanchet@48975
   584
  thus ?thesis using card_of_ordIso by blast
blanchet@48975
   585
qed
blanchet@48975
   586
blanchet@48975
   587
blanchet@48975
   588
lemma card_of_Plus_mono1:
blanchet@48975
   589
assumes "|A| \<le>o |B|"
blanchet@48975
   590
shows "|A <+> C| \<le>o |B <+> C|"
blanchet@48975
   591
proof-
blanchet@48975
   592
  obtain f where 1: "inj_on f A \<and> f ` A \<le> B"
blanchet@48975
   593
  using assms card_of_ordLeq[of A] by fastforce
blanchet@48975
   594
  obtain g where g_def:
blanchet@48975
   595
  "g = (\<lambda>d. case d of Inl a \<Rightarrow> Inl(f a) | Inr (c::'c) \<Rightarrow> Inr c)" by blast
blanchet@48975
   596
  have "inj_on g (A <+> C) \<and> g ` (A <+> C) \<le> (B <+> C)"
blanchet@48975
   597
  proof-
blanchet@48975
   598
    {fix d1 and d2 assume "d1 \<in> A <+> C \<and> d2 \<in> A <+> C" and
blanchet@48975
   599
                          "g d1 = g d2"
blanchet@48975
   600
     hence "d1 = d2" using 1 unfolding inj_on_def
blanchet@48975
   601
     by(case_tac d1, case_tac d2, auto simp add: g_def)
blanchet@48975
   602
    }
blanchet@48975
   603
    moreover
blanchet@48975
   604
    {fix d assume "d \<in> A <+> C"
blanchet@48975
   605
     hence "g d \<in> B <+> C"  using 1
blanchet@48975
   606
     by(case_tac d, auto simp add: g_def)
blanchet@48975
   607
    }
blanchet@48975
   608
    ultimately show ?thesis unfolding inj_on_def by auto
blanchet@48975
   609
  qed
blanchet@48975
   610
  thus ?thesis using card_of_ordLeq by metis
blanchet@48975
   611
qed
blanchet@48975
   612
blanchet@48975
   613
blanchet@48975
   614
corollary ordLeq_Plus_mono1:
blanchet@48975
   615
assumes "r \<le>o r'"
blanchet@48975
   616
shows "|(Field r) <+> C| \<le>o |(Field r') <+> C|"
blanchet@48975
   617
using assms card_of_mono2 card_of_Plus_mono1 by blast
blanchet@48975
   618
blanchet@48975
   619
blanchet@48975
   620
lemma card_of_Plus_mono2:
blanchet@48975
   621
assumes "|A| \<le>o |B|"
blanchet@48975
   622
shows "|C <+> A| \<le>o |C <+> B|"
blanchet@48975
   623
using assms card_of_Plus_mono1[of A B C]
blanchet@48975
   624
      card_of_Plus_commute[of C A]  card_of_Plus_commute[of B C]
blanchet@48975
   625
      ordIso_ordLeq_trans[of "|C <+> A|"] ordLeq_ordIso_trans[of "|C <+> A|"]
blanchet@48975
   626
by blast
blanchet@48975
   627
blanchet@48975
   628
blanchet@48975
   629
corollary ordLeq_Plus_mono2:
blanchet@48975
   630
assumes "r \<le>o r'"
blanchet@48975
   631
shows "|A <+> (Field r)| \<le>o |A <+> (Field r')|"
blanchet@48975
   632
using assms card_of_mono2 card_of_Plus_mono2 by blast
blanchet@48975
   633
blanchet@48975
   634
blanchet@48975
   635
lemma card_of_Plus_mono:
blanchet@48975
   636
assumes "|A| \<le>o |B|" and "|C| \<le>o |D|"
blanchet@48975
   637
shows "|A <+> C| \<le>o |B <+> D|"
blanchet@48975
   638
using assms card_of_Plus_mono1[of A B C] card_of_Plus_mono2[of C D B]
blanchet@48975
   639
      ordLeq_transitive[of "|A <+> C|"] by blast
blanchet@48975
   640
blanchet@48975
   641
blanchet@48975
   642
corollary ordLeq_Plus_mono:
blanchet@48975
   643
assumes "r \<le>o r'" and "p \<le>o p'"
blanchet@48975
   644
shows "|(Field r) <+> (Field p)| \<le>o |(Field r') <+> (Field p')|"
blanchet@48975
   645
using assms card_of_mono2[of r r'] card_of_mono2[of p p'] card_of_Plus_mono by blast
blanchet@48975
   646
blanchet@48975
   647
blanchet@48975
   648
lemma card_of_Plus_cong1:
blanchet@48975
   649
assumes "|A| =o |B|"
blanchet@48975
   650
shows "|A <+> C| =o |B <+> C|"
blanchet@48975
   651
using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono1)
blanchet@48975
   652
blanchet@48975
   653
blanchet@48975
   654
corollary ordIso_Plus_cong1:
blanchet@48975
   655
assumes "r =o r'"
blanchet@48975
   656
shows "|(Field r) <+> C| =o |(Field r') <+> C|"
blanchet@48975
   657
using assms card_of_cong card_of_Plus_cong1 by blast
blanchet@48975
   658
blanchet@48975
   659
blanchet@48975
   660
lemma card_of_Plus_cong2:
blanchet@48975
   661
assumes "|A| =o |B|"
blanchet@48975
   662
shows "|C <+> A| =o |C <+> B|"
blanchet@48975
   663
using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono2)
blanchet@48975
   664
blanchet@48975
   665
blanchet@48975
   666
corollary ordIso_Plus_cong2:
blanchet@48975
   667
assumes "r =o r'"
blanchet@48975
   668
shows "|A <+> (Field r)| =o |A <+> (Field r')|"
blanchet@48975
   669
using assms card_of_cong card_of_Plus_cong2 by blast
blanchet@48975
   670
blanchet@48975
   671
blanchet@48975
   672
lemma card_of_Plus_cong:
blanchet@48975
   673
assumes "|A| =o |B|" and "|C| =o |D|"
blanchet@48975
   674
shows "|A <+> C| =o |B <+> D|"
blanchet@48975
   675
using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono)
blanchet@48975
   676
blanchet@48975
   677
blanchet@48975
   678
corollary ordIso_Plus_cong:
blanchet@48975
   679
assumes "r =o r'" and "p =o p'"
blanchet@48975
   680
shows "|(Field r) <+> (Field p)| =o |(Field r') <+> (Field p')|"
blanchet@48975
   681
using assms card_of_cong[of r r'] card_of_cong[of p p'] card_of_Plus_cong by blast
blanchet@48975
   682
blanchet@48975
   683
blanchet@48975
   684
lemma card_of_Un1:
blanchet@48975
   685
shows "|A| \<le>o |A \<union> B| "
blanchet@48975
   686
using inj_on_id[of A] card_of_ordLeq[of A _] by fastforce
blanchet@48975
   687
blanchet@48975
   688
blanchet@48975
   689
lemma card_of_diff:
blanchet@48975
   690
shows "|A - B| \<le>o |A|"
blanchet@48975
   691
using inj_on_id[of "A - B"] card_of_ordLeq[of "A - B" _] by fastforce
blanchet@48975
   692
blanchet@48975
   693
blanchet@48975
   694
lemma card_of_Un_Plus_ordLeq:
blanchet@48975
   695
"|A \<union> B| \<le>o |A <+> B|"
blanchet@48975
   696
proof-
blanchet@48975
   697
   let ?f = "\<lambda> c. if c \<in> A then Inl c else Inr c"
blanchet@48975
   698
   have "inj_on ?f (A \<union> B) \<and> ?f ` (A \<union> B) \<le> A <+> B"
blanchet@48975
   699
   unfolding inj_on_def by auto
blanchet@48975
   700
   thus ?thesis using card_of_ordLeq by blast
blanchet@48975
   701
qed
blanchet@48975
   702
blanchet@48975
   703
blanchet@48975
   704
lemma card_of_Times1:
blanchet@48975
   705
assumes "A \<noteq> {}"
blanchet@48975
   706
shows "|B| \<le>o |B \<times> A|"
blanchet@48975
   707
proof(cases "B = {}", simp add: card_of_empty)
blanchet@48975
   708
  assume *: "B \<noteq> {}"
blanchet@48975
   709
  have "fst `(B \<times> A) = B" unfolding image_def using assms by auto
blanchet@48975
   710
  thus ?thesis using inj_on_iff_surj[of B "B \<times> A"]
blanchet@48975
   711
                     card_of_ordLeq[of B "B \<times> A"] * by blast
blanchet@48975
   712
qed
blanchet@48975
   713
blanchet@48975
   714
blanchet@48975
   715
corollary Card_order_Times1:
blanchet@48975
   716
"\<lbrakk>Card_order r; B \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |(Field r) \<times> B|"
blanchet@48975
   717
using card_of_Times1[of B] card_of_Field_ordIso
blanchet@48975
   718
      ordIso_ordLeq_trans ordIso_symmetric by blast
blanchet@48975
   719
blanchet@48975
   720
blanchet@48975
   721
lemma card_of_Times_commute: "|A \<times> B| =o |B \<times> A|"
blanchet@48975
   722
proof-
blanchet@48975
   723
  let ?f = "\<lambda>(a::'a,b::'b). (b,a)"
blanchet@48975
   724
  have "bij_betw ?f (A \<times> B) (B \<times> A)"
blanchet@48975
   725
  unfolding bij_betw_def inj_on_def by auto
blanchet@48975
   726
  thus ?thesis using card_of_ordIso by blast
blanchet@48975
   727
qed
blanchet@48975
   728
blanchet@48975
   729
blanchet@48975
   730
lemma card_of_Times2:
blanchet@48975
   731
assumes "A \<noteq> {}"   shows "|B| \<le>o |A \<times> B|"
blanchet@48975
   732
using assms card_of_Times1[of A B] card_of_Times_commute[of B A]
blanchet@48975
   733
      ordLeq_ordIso_trans by blast
blanchet@48975
   734
blanchet@48975
   735
blanchet@48975
   736
corollary Card_order_Times2:
blanchet@48975
   737
"\<lbrakk>Card_order r; A \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |A \<times> (Field r)|"
blanchet@48975
   738
using card_of_Times2[of A] card_of_Field_ordIso
blanchet@48975
   739
      ordIso_ordLeq_trans ordIso_symmetric by blast
blanchet@48975
   740
blanchet@48975
   741
blanchet@48975
   742
lemma card_of_Times3: "|A| \<le>o |A \<times> A|"
blanchet@48975
   743
using card_of_Times1[of A]
blanchet@48975
   744
by(cases "A = {}", simp add: card_of_empty, blast)
blanchet@48975
   745
blanchet@48975
   746
blanchet@48975
   747
lemma card_of_Plus_Times_bool: "|A <+> A| =o |A \<times> (UNIV::bool set)|"
blanchet@48975
   748
proof-
blanchet@48975
   749
  let ?f = "\<lambda>c::'a + 'a. case c of Inl a \<Rightarrow> (a,True)
blanchet@48975
   750
                                  |Inr a \<Rightarrow> (a,False)"
blanchet@48975
   751
  have "bij_betw ?f (A <+> A) (A \<times> (UNIV::bool set))"
blanchet@48975
   752
  proof-
blanchet@48975
   753
    {fix  c1 and c2 assume "?f c1 = ?f c2"
blanchet@48975
   754
     hence "c1 = c2"
blanchet@48975
   755
     by(case_tac "c1", case_tac "c2", auto, case_tac "c2", auto)
blanchet@48975
   756
    }
blanchet@48975
   757
    moreover
blanchet@48975
   758
    {fix c assume "c \<in> A <+> A"
blanchet@48975
   759
     hence "?f c \<in> A \<times> (UNIV::bool set)"
blanchet@48975
   760
     by(case_tac c, auto)
blanchet@48975
   761
    }
blanchet@48975
   762
    moreover
blanchet@48975
   763
    {fix a bl assume *: "(a,bl) \<in> A \<times> (UNIV::bool set)"
blanchet@48975
   764
     have "(a,bl) \<in> ?f ` ( A <+> A)"
blanchet@48975
   765
     proof(cases bl)
blanchet@48975
   766
       assume bl hence "?f(Inl a) = (a,bl)" by auto
blanchet@48975
   767
       thus ?thesis using * by force
blanchet@48975
   768
     next
blanchet@48975
   769
       assume "\<not> bl" hence "?f(Inr a) = (a,bl)" by auto
blanchet@48975
   770
       thus ?thesis using * by force
blanchet@48975
   771
     qed
blanchet@48975
   772
    }
blanchet@48975
   773
    ultimately show ?thesis unfolding bij_betw_def inj_on_def by auto
blanchet@48975
   774
  qed
blanchet@48975
   775
  thus ?thesis using card_of_ordIso by blast
blanchet@48975
   776
qed
blanchet@48975
   777
blanchet@48975
   778
blanchet@48975
   779
lemma card_of_Times_mono1:
blanchet@48975
   780
assumes "|A| \<le>o |B|"
blanchet@48975
   781
shows "|A \<times> C| \<le>o |B \<times> C|"
blanchet@48975
   782
proof-
blanchet@48975
   783
  obtain f where 1: "inj_on f A \<and> f ` A \<le> B"
blanchet@48975
   784
  using assms card_of_ordLeq[of A] by fastforce
blanchet@48975
   785
  obtain g where g_def:
blanchet@48975
   786
  "g = (\<lambda>(a,c::'c). (f a,c))" by blast
blanchet@48975
   787
  have "inj_on g (A \<times> C) \<and> g ` (A \<times> C) \<le> (B \<times> C)"
blanchet@48975
   788
  using 1 unfolding inj_on_def using g_def by auto
blanchet@48975
   789
  thus ?thesis using card_of_ordLeq by metis
blanchet@48975
   790
qed
blanchet@48975
   791
blanchet@48975
   792
blanchet@48975
   793
corollary ordLeq_Times_mono1:
blanchet@48975
   794
assumes "r \<le>o r'"
blanchet@48975
   795
shows "|(Field r) \<times> C| \<le>o |(Field r') \<times> C|"
blanchet@48975
   796
using assms card_of_mono2 card_of_Times_mono1 by blast
blanchet@48975
   797
blanchet@48975
   798
blanchet@48975
   799
lemma card_of_Times_mono2:
blanchet@48975
   800
assumes "|A| \<le>o |B|"
blanchet@48975
   801
shows "|C \<times> A| \<le>o |C \<times> B|"
blanchet@48975
   802
using assms card_of_Times_mono1[of A B C]
blanchet@48975
   803
      card_of_Times_commute[of C A]  card_of_Times_commute[of B C]
blanchet@48975
   804
      ordIso_ordLeq_trans[of "|C \<times> A|"] ordLeq_ordIso_trans[of "|C \<times> A|"]
blanchet@48975
   805
by blast
blanchet@48975
   806
blanchet@48975
   807
blanchet@48975
   808
corollary ordLeq_Times_mono2:
blanchet@48975
   809
assumes "r \<le>o r'"
blanchet@48975
   810
shows "|A \<times> (Field r)| \<le>o |A \<times> (Field r')|"
blanchet@48975
   811
using assms card_of_mono2 card_of_Times_mono2 by blast
blanchet@48975
   812
blanchet@48975
   813
blanchet@48975
   814
lemma card_of_Times_cong1:
blanchet@48975
   815
assumes "|A| =o |B|"
blanchet@48975
   816
shows "|A \<times> C| =o |B \<times> C|"
blanchet@48975
   817
using assms by (simp add: ordIso_iff_ordLeq card_of_Times_mono1)
blanchet@48975
   818
blanchet@48975
   819
blanchet@48975
   820
lemma card_of_Times_cong2:
blanchet@48975
   821
assumes "|A| =o |B|"
blanchet@48975
   822
shows "|C \<times> A| =o |C \<times> B|"
blanchet@48975
   823
using assms by (simp add: ordIso_iff_ordLeq card_of_Times_mono2)
blanchet@48975
   824
blanchet@48975
   825
blanchet@48975
   826
corollary ordIso_Times_cong2:
blanchet@48975
   827
assumes "r =o r'"
blanchet@48975
   828
shows "|A \<times> (Field r)| =o |A \<times> (Field r')|"
blanchet@48975
   829
using assms card_of_cong card_of_Times_cong2 by blast
blanchet@48975
   830
blanchet@48975
   831
blanchet@48975
   832
lemma card_of_Sigma_mono1:
blanchet@48975
   833
assumes "\<forall>i \<in> I. |A i| \<le>o |B i|"
blanchet@48975
   834
shows "|SIGMA i : I. A i| \<le>o |SIGMA i : I. B i|"
blanchet@48975
   835
proof-
blanchet@48975
   836
  have "\<forall>i. i \<in> I \<longrightarrow> (\<exists>f. inj_on f (A i) \<and> f ` (A i) \<le> B i)"
blanchet@48975
   837
  using assms by (auto simp add: card_of_ordLeq)
blanchet@48975
   838
  with choice[of "\<lambda> i f. i \<in> I \<longrightarrow> inj_on f (A i) \<and> f ` (A i) \<le> B i"]
blanchet@48975
   839
  obtain F where 1: "\<forall>i \<in> I. inj_on (F i) (A i) \<and> (F i) ` (A i) \<le> B i" by fastforce
blanchet@48975
   840
  obtain g where g_def: "g = (\<lambda>(i,a::'b). (i,F i a))" by blast
blanchet@48975
   841
  have "inj_on g (Sigma I A) \<and> g ` (Sigma I A) \<le> (Sigma I B)"
blanchet@48975
   842
  using 1 unfolding inj_on_def using g_def by force
blanchet@48975
   843
  thus ?thesis using card_of_ordLeq by metis
blanchet@48975
   844
qed
blanchet@48975
   845
blanchet@48975
   846
blanchet@48975
   847
corollary card_of_Sigma_Times:
blanchet@48975
   848
"\<forall>i \<in> I. |A i| \<le>o |B| \<Longrightarrow> |SIGMA i : I. A i| \<le>o |I \<times> B|"
blanchet@48975
   849
using card_of_Sigma_mono1[of I A "\<lambda>i. B"] .
blanchet@48975
   850
blanchet@48975
   851
blanchet@48975
   852
lemma card_of_UNION_Sigma:
blanchet@48975
   853
"|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
blanchet@48975
   854
using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by metis
blanchet@48975
   855
blanchet@48975
   856
blanchet@48975
   857
lemma card_of_bool:
blanchet@48975
   858
assumes "a1 \<noteq> a2"
blanchet@48975
   859
shows "|UNIV::bool set| =o |{a1,a2}|"
blanchet@48975
   860
proof-
blanchet@48975
   861
  let ?f = "\<lambda> bl. case bl of True \<Rightarrow> a1 | False \<Rightarrow> a2"
blanchet@48975
   862
  have "bij_betw ?f UNIV {a1,a2}"
blanchet@48975
   863
  proof-
blanchet@48975
   864
    {fix bl1 and bl2 assume "?f  bl1 = ?f bl2"
blanchet@48975
   865
     hence "bl1 = bl2" using assms by (case_tac bl1, case_tac bl2, auto)
blanchet@48975
   866
    }
blanchet@48975
   867
    moreover
blanchet@48975
   868
    {fix bl have "?f bl \<in> {a1,a2}" by (case_tac bl, auto)
blanchet@48975
   869
    }
blanchet@48975
   870
    moreover
blanchet@48975
   871
    {fix a assume *: "a \<in> {a1,a2}"
blanchet@48975
   872
     have "a \<in> ?f ` UNIV"
blanchet@48975
   873
     proof(cases "a = a1")
blanchet@48975
   874
       assume "a = a1"
blanchet@48975
   875
       hence "?f True = a" by auto  thus ?thesis by blast
blanchet@48975
   876
     next
blanchet@48975
   877
       assume "a \<noteq> a1" hence "a = a2" using * by auto
blanchet@48975
   878
       hence "?f False = a" by auto  thus ?thesis by blast
blanchet@48975
   879
     qed
blanchet@48975
   880
    }
blanchet@48975
   881
    ultimately show ?thesis unfolding bij_betw_def inj_on_def
blanchet@48975
   882
    by (metis image_subsetI order_eq_iff subsetI)
blanchet@48975
   883
  qed
blanchet@48975
   884
  thus ?thesis using card_of_ordIso by blast
blanchet@48975
   885
qed
blanchet@48975
   886
blanchet@48975
   887
blanchet@48975
   888
lemma card_of_Plus_Times_aux:
blanchet@48975
   889
assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and
blanchet@48975
   890
        LEQ: "|A| \<le>o |B|"
blanchet@48975
   891
shows "|A <+> B| \<le>o |A \<times> B|"
blanchet@48975
   892
proof-
blanchet@48975
   893
  have 1: "|UNIV::bool set| \<le>o |A|"
blanchet@48975
   894
  using A2 card_of_mono1[of "{a1,a2}"] card_of_bool[of a1 a2]
blanchet@48975
   895
        ordIso_ordLeq_trans[of "|UNIV::bool set|"] by metis
blanchet@48975
   896
  (*  *)
blanchet@48975
   897
  have "|A <+> B| \<le>o |B <+> B|"
blanchet@48975
   898
  using LEQ card_of_Plus_mono1 by blast
blanchet@48975
   899
  moreover have "|B <+> B| =o |B \<times> (UNIV::bool set)|"
blanchet@48975
   900
  using card_of_Plus_Times_bool by blast
blanchet@48975
   901
  moreover have "|B \<times> (UNIV::bool set)| \<le>o |B \<times> A|"
blanchet@48975
   902
  using 1 by (simp add: card_of_Times_mono2)
blanchet@48975
   903
  moreover have " |B \<times> A| =o |A \<times> B|"
blanchet@48975
   904
  using card_of_Times_commute by blast
blanchet@48975
   905
  ultimately show "|A <+> B| \<le>o |A \<times> B|"
blanchet@48975
   906
  using ordLeq_ordIso_trans[of "|A <+> B|" "|B <+> B|" "|B \<times> (UNIV::bool set)|"]
blanchet@48975
   907
        ordLeq_transitive[of "|A <+> B|" "|B \<times> (UNIV::bool set)|" "|B \<times> A|"]
blanchet@48975
   908
        ordLeq_ordIso_trans[of "|A <+> B|" "|B \<times> A|" "|A \<times> B|"]
blanchet@48975
   909
  by blast
blanchet@48975
   910
qed
blanchet@48975
   911
blanchet@48975
   912
blanchet@48975
   913
lemma card_of_Plus_Times:
blanchet@48975
   914
assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and
blanchet@48975
   915
        B2: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B"
blanchet@48975
   916
shows "|A <+> B| \<le>o |A \<times> B|"
blanchet@48975
   917
proof-
blanchet@48975
   918
  {assume "|A| \<le>o |B|"
blanchet@48975
   919
   hence ?thesis using assms by (auto simp add: card_of_Plus_Times_aux)
blanchet@48975
   920
  }
blanchet@48975
   921
  moreover
blanchet@48975
   922
  {assume "|B| \<le>o |A|"
blanchet@48975
   923
   hence "|B <+> A| \<le>o |B \<times> A|"
blanchet@48975
   924
   using assms by (auto simp add: card_of_Plus_Times_aux)
blanchet@48975
   925
   hence ?thesis
blanchet@48975
   926
   using card_of_Plus_commute card_of_Times_commute
blanchet@48975
   927
         ordIso_ordLeq_trans ordLeq_ordIso_trans by metis
blanchet@48975
   928
  }
blanchet@48975
   929
  ultimately show ?thesis
blanchet@48975
   930
  using card_of_Well_order[of A] card_of_Well_order[of B]
blanchet@48975
   931
        ordLeq_total[of "|A|"] by metis
blanchet@48975
   932
qed
blanchet@48975
   933
blanchet@48975
   934
blanchet@48975
   935
lemma card_of_ordLeq_finite:
blanchet@48975
   936
assumes "|A| \<le>o |B|" and "finite B"
blanchet@48975
   937
shows "finite A"
blanchet@48975
   938
using assms unfolding ordLeq_def
blanchet@48975
   939
using embed_inj_on[of "|A|" "|B|"]  embed_Field[of "|A|" "|B|"]
blanchet@48975
   940
      Field_card_of[of "A"] Field_card_of[of "B"] inj_on_finite[of _ "A" "B"] by fastforce
blanchet@48975
   941
blanchet@48975
   942
blanchet@48975
   943
lemma card_of_ordLeq_infinite:
blanchet@48975
   944
assumes "|A| \<le>o |B|" and "infinite A"
blanchet@48975
   945
shows "infinite B"
blanchet@48975
   946
using assms card_of_ordLeq_finite by auto
blanchet@48975
   947
blanchet@48975
   948
blanchet@48975
   949
lemma card_of_ordIso_finite:
blanchet@48975
   950
assumes "|A| =o |B|"
blanchet@48975
   951
shows "finite A = finite B"
blanchet@48975
   952
using assms unfolding ordIso_def iso_def[abs_def]
blanchet@48975
   953
by (auto simp: bij_betw_finite Field_card_of)
blanchet@48975
   954
blanchet@48975
   955
blanchet@48975
   956
lemma card_of_ordIso_finite_Field:
blanchet@48975
   957
assumes "Card_order r" and "r =o |A|"
blanchet@48975
   958
shows "finite(Field r) = finite A"
blanchet@48975
   959
using assms card_of_Field_ordIso card_of_ordIso_finite ordIso_equivalence by blast
blanchet@48975
   960
blanchet@48975
   961
blanchet@48975
   962
subsection {* Cardinals versus set operations involving infinite sets *}
blanchet@48975
   963
blanchet@48975
   964
blanchet@48975
   965
text{* Here we show that, for infinite sets, most set-theoretic constructions
blanchet@48975
   966
do not increase the cardinality.  The cornerstone for this is
blanchet@48975
   967
theorem @{text "Card_order_Times_same_infinite"}, which states that self-product
blanchet@48975
   968
does not increase cardinality -- the proof of this fact adapts a standard
blanchet@48975
   969
set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
blanchet@48975
   970
at page 47 in \cite{card-book}. Then everything else follows fairly easily.  *}
blanchet@48975
   971
blanchet@48975
   972
blanchet@48975
   973
lemma infinite_iff_card_of_nat:
blanchet@48975
   974
"infinite A = ( |UNIV::nat set| \<le>o |A| )"
blanchet@48975
   975
by (auto simp add: infinite_iff_countable_subset card_of_ordLeq)
blanchet@48975
   976
blanchet@48975
   977
blanchet@48975
   978
lemma finite_iff_cardOf_nat:
blanchet@48975
   979
"finite A = ( |A| <o |UNIV :: nat set| )"
blanchet@48975
   980
using infinite_iff_card_of_nat[of A]
blanchet@48975
   981
not_ordLeq_iff_ordLess[of "|A|" "|UNIV :: nat set|"]
blanchet@48975
   982
by (fastforce simp: card_of_Well_order)
blanchet@48975
   983
blanchet@48975
   984
lemma finite_ordLess_infinite2:
blanchet@48975
   985
assumes "finite A" and "infinite B"
blanchet@48975
   986
shows "|A| <o |B|"
blanchet@48975
   987
using assms
blanchet@48975
   988
finite_ordLess_infinite[of "|A|" "|B|"]
blanchet@48975
   989
card_of_Well_order[of A] card_of_Well_order[of B]
blanchet@48975
   990
Field_card_of[of A] Field_card_of[of B] by auto
blanchet@48975
   991
blanchet@48975
   992
blanchet@48975
   993
text{* The next two results correspond to the ZF fact that all infinite cardinals are
blanchet@48975
   994
limit ordinals: *}
blanchet@48975
   995
blanchet@48975
   996
lemma Card_order_infinite_not_under:
blanchet@48975
   997
assumes CARD: "Card_order r" and INF: "infinite (Field r)"
blanchet@48975
   998
shows "\<not> (\<exists>a. Field r = rel.under r a)"
blanchet@48975
   999
proof(auto)
blanchet@48975
  1000
  have 0: "Well_order r \<and> wo_rel r \<and> Refl r"
blanchet@48975
  1001
  using CARD unfolding wo_rel_def card_order_on_def order_on_defs by auto
blanchet@48975
  1002
  fix a assume *: "Field r = rel.under r a"
blanchet@48975
  1003
  show False
blanchet@48975
  1004
  proof(cases "a \<in> Field r")
blanchet@48975
  1005
    assume Case1: "a \<notin> Field r"
blanchet@48975
  1006
    hence "rel.under r a = {}" unfolding Field_def rel.under_def by auto
blanchet@48975
  1007
    thus False using INF *  by auto
blanchet@48975
  1008
  next
blanchet@48975
  1009
    let ?r' = "Restr r (rel.underS r a)"
blanchet@48975
  1010
    assume Case2: "a \<in> Field r"
blanchet@48975
  1011
    hence 1: "rel.under r a = rel.underS r a \<union> {a} \<and> a \<notin> rel.underS r a"
blanchet@48975
  1012
    using 0 rel.Refl_under_underS rel.underS_notIn by fastforce
blanchet@48975
  1013
    have 2: "wo_rel.ofilter r (rel.underS r a) \<and> rel.underS r a < Field r"
blanchet@48975
  1014
    using 0 wo_rel.underS_ofilter * 1 Case2 by auto
blanchet@48975
  1015
    hence "?r' <o r" using 0 using ofilter_ordLess by blast
blanchet@48975
  1016
    moreover
blanchet@48975
  1017
    have "Field ?r' = rel.underS r a \<and> Well_order ?r'"
blanchet@48975
  1018
    using  2 0 Field_Restr_ofilter[of r] Well_order_Restr[of r] by blast
blanchet@48975
  1019
    ultimately have "|rel.underS r a| <o r" using ordLess_Field[of ?r'] by auto
blanchet@48975
  1020
    moreover have "|rel.under r a| =o r" using * CARD card_of_Field_ordIso[of r] by auto
blanchet@48975
  1021
    ultimately have "|rel.underS r a| <o |rel.under r a|"
blanchet@48975
  1022
    using ordIso_symmetric ordLess_ordIso_trans by blast
blanchet@48975
  1023
    moreover
blanchet@48975
  1024
    {have "\<exists>f. bij_betw f (rel.under r a) (rel.underS r a)"
blanchet@48975
  1025
     using infinite_imp_bij_betw[of "Field r" a] INF * 1 by auto
blanchet@48975
  1026
     hence "|rel.under r a| =o |rel.underS r a|" using card_of_ordIso by blast
blanchet@48975
  1027
    }
blanchet@48975
  1028
    ultimately show False using not_ordLess_ordIso ordIso_symmetric by blast
blanchet@48975
  1029
  qed
blanchet@48975
  1030
qed
blanchet@48975
  1031
blanchet@48975
  1032
blanchet@48975
  1033
lemma infinite_Card_order_limit:
blanchet@48975
  1034
assumes r: "Card_order r" and "infinite (Field r)"
blanchet@48975
  1035
and a: "a : Field r"
blanchet@48975
  1036
shows "EX b : Field r. a \<noteq> b \<and> (a,b) : r"
blanchet@48975
  1037
proof-
blanchet@48975
  1038
  have "Field r \<noteq> rel.under r a"
blanchet@48975
  1039
  using assms Card_order_infinite_not_under by blast
blanchet@48975
  1040
  moreover have "rel.under r a \<le> Field r"
blanchet@48975
  1041
  using rel.under_Field .
blanchet@48975
  1042
  ultimately have "rel.under r a < Field r" by blast
blanchet@48975
  1043
  then obtain b where 1: "b : Field r \<and> ~ (b,a) : r"
blanchet@48975
  1044
  unfolding rel.under_def by blast
blanchet@48975
  1045
  moreover have ba: "b \<noteq> a"
blanchet@48975
  1046
  using 1 r unfolding card_order_on_def well_order_on_def
blanchet@48975
  1047
  linear_order_on_def partial_order_on_def preorder_on_def refl_on_def by auto
blanchet@48975
  1048
  ultimately have "(a,b) : r"
blanchet@48975
  1049
  using a r unfolding card_order_on_def well_order_on_def linear_order_on_def
blanchet@48975
  1050
  total_on_def by blast
blanchet@48975
  1051
  thus ?thesis using 1 ba by auto
blanchet@48975
  1052
qed
blanchet@48975
  1053
blanchet@48975
  1054
blanchet@48975
  1055
theorem Card_order_Times_same_infinite:
blanchet@48975
  1056
assumes CO: "Card_order r" and INF: "infinite(Field r)"
blanchet@48975
  1057
shows "|Field r \<times> Field r| \<le>o r"
blanchet@48975
  1058
proof-
blanchet@48975
  1059
  obtain phi where phi_def:
blanchet@48975
  1060
  "phi = (\<lambda>r::'a rel. Card_order r \<and> infinite(Field r) \<and>
blanchet@48975
  1061
                      \<not> |Field r \<times> Field r| \<le>o r )" by blast
blanchet@48975
  1062
  have temp1: "\<forall>r. phi r \<longrightarrow> Well_order r"
blanchet@48975
  1063
  unfolding phi_def card_order_on_def by auto
blanchet@48975
  1064
  have Ft: "\<not>(\<exists>r. phi r)"
blanchet@48975
  1065
  proof
blanchet@48975
  1066
    assume "\<exists>r. phi r"
blanchet@48975
  1067
    hence "{r. phi r} \<noteq> {} \<and> {r. phi r} \<le> {r. Well_order r}"
blanchet@48975
  1068
    using temp1 by auto
blanchet@48975
  1069
    then obtain r where 1: "phi r" and 2: "\<forall>r'. phi r' \<longrightarrow> r \<le>o r'" and
blanchet@48975
  1070
                   3: "Card_order r \<and> Well_order r"
blanchet@48975
  1071
    using exists_minim_Well_order[of "{r. phi r}"] temp1 phi_def by blast
blanchet@48975
  1072
    let ?A = "Field r"  let ?r' = "bsqr r"
blanchet@48975
  1073
    have 4: "Well_order ?r' \<and> Field ?r' = ?A \<times> ?A \<and> |?A| =o r"
blanchet@48975
  1074
    using 3 bsqr_Well_order Field_bsqr card_of_Field_ordIso by blast
blanchet@48975
  1075
    have 5: "Card_order |?A \<times> ?A| \<and> Well_order |?A \<times> ?A|"
blanchet@48975
  1076
    using card_of_Card_order card_of_Well_order by blast
blanchet@48975
  1077
    (*  *)
blanchet@48975
  1078
    have "r <o |?A \<times> ?A|"
blanchet@48975
  1079
    using 1 3 5 ordLess_or_ordLeq unfolding phi_def by blast
blanchet@48975
  1080
    moreover have "|?A \<times> ?A| \<le>o ?r'"
blanchet@48975
  1081
    using card_of_least[of "?A \<times> ?A"] 4 by auto
blanchet@48975
  1082
    ultimately have "r <o ?r'" using ordLess_ordLeq_trans by auto
blanchet@48975
  1083
    then obtain f where 6: "embed r ?r' f" and 7: "\<not> bij_betw f ?A (?A \<times> ?A)"
blanchet@48975
  1084
    unfolding ordLess_def embedS_def[abs_def]
blanchet@48975
  1085
    by (auto simp add: Field_bsqr)
blanchet@48975
  1086
    let ?B = "f ` ?A"
blanchet@48975
  1087
    have "|?A| =o |?B|"
blanchet@48975
  1088
    using 3 6 embed_inj_on inj_on_imp_bij_betw card_of_ordIso by blast
blanchet@48975
  1089
    hence 8: "r =o |?B|" using 4 ordIso_transitive ordIso_symmetric by blast
blanchet@48975
  1090
    (*  *)
blanchet@48975
  1091
    have "wo_rel.ofilter ?r' ?B"
blanchet@48975
  1092
    using 6 embed_Field_ofilter 3 4 by blast
blanchet@48975
  1093
    hence "wo_rel.ofilter ?r' ?B \<and> ?B \<noteq> ?A \<times> ?A \<and> ?B \<noteq> Field ?r'"
blanchet@48975
  1094
    using 7 unfolding bij_betw_def using 6 3 embed_inj_on 4 by auto
blanchet@48975
  1095
    hence temp2: "wo_rel.ofilter ?r' ?B \<and> ?B < ?A \<times> ?A"
blanchet@48975
  1096
    using 4 wo_rel_def[of ?r'] wo_rel.ofilter_def[of ?r' ?B] by blast
blanchet@48975
  1097
    have "\<not> (\<exists>a. Field r = rel.under r a)"
blanchet@48975
  1098
    using 1 unfolding phi_def using Card_order_infinite_not_under[of r] by auto
blanchet@48975
  1099
    then obtain A1 where temp3: "wo_rel.ofilter r A1 \<and> A1 < ?A" and 9: "?B \<le> A1 \<times> A1"
blanchet@48975
  1100
    using temp2 3 bsqr_ofilter[of r ?B] by blast
blanchet@48975
  1101
    hence "|?B| \<le>o |A1 \<times> A1|" using card_of_mono1 by blast
blanchet@48975
  1102
    hence 10: "r \<le>o |A1 \<times> A1|" using 8 ordIso_ordLeq_trans by blast
blanchet@48975
  1103
    let ?r1 = "Restr r A1"
blanchet@48975
  1104
    have "?r1 <o r" using temp3 ofilter_ordLess 3 by blast
blanchet@48975
  1105
    moreover
blanchet@48975
  1106
    {have "well_order_on A1 ?r1" using 3 temp3 well_order_on_Restr by blast
blanchet@48975
  1107
     hence "|A1| \<le>o ?r1" using 3 Well_order_Restr card_of_least by blast
blanchet@48975
  1108
    }
blanchet@48975
  1109
    ultimately have 11: "|A1| <o r" using ordLeq_ordLess_trans by blast
blanchet@48975
  1110
    (*  *)
blanchet@48975
  1111
    have "infinite (Field r)" using 1 unfolding phi_def by simp
blanchet@48975
  1112
    hence "infinite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast
blanchet@48975
  1113
    hence "infinite A1" using 9 infinite_super finite_cartesian_product by blast
blanchet@48975
  1114
    moreover have temp4: "Field |A1| = A1 \<and> Well_order |A1| \<and> Card_order |A1|"
blanchet@48975
  1115
    using card_of_Card_order[of A1] card_of_Well_order[of A1]
blanchet@48975
  1116
    by (simp add: Field_card_of)
blanchet@48975
  1117
    moreover have "\<not> r \<le>o | A1 |"
blanchet@48975
  1118
    using temp4 11 3 using not_ordLeq_iff_ordLess by blast
blanchet@48975
  1119
    ultimately have "infinite(Field |A1| ) \<and> Card_order |A1| \<and> \<not> r \<le>o | A1 |"
blanchet@48975
  1120
    by (simp add: card_of_card_order_on)
blanchet@48975
  1121
    hence "|Field |A1| \<times> Field |A1| | \<le>o |A1|"
blanchet@48975
  1122
    using 2 unfolding phi_def by blast
blanchet@48975
  1123
    hence "|A1 \<times> A1 | \<le>o |A1|" using temp4 by auto
blanchet@48975
  1124
    hence "r \<le>o |A1|" using 10 ordLeq_transitive by blast
blanchet@48975
  1125
    thus False using 11 not_ordLess_ordLeq by auto
blanchet@48975
  1126
  qed
blanchet@48975
  1127
  thus ?thesis using assms unfolding phi_def by blast
blanchet@48975
  1128
qed
blanchet@48975
  1129
blanchet@48975
  1130
blanchet@48975
  1131
corollary card_of_Times_same_infinite:
blanchet@48975
  1132
assumes "infinite A"
blanchet@48975
  1133
shows "|A \<times> A| =o |A|"
blanchet@48975
  1134
proof-
blanchet@48975
  1135
  let ?r = "|A|"
blanchet@48975
  1136
  have "Field ?r = A \<and> Card_order ?r"
blanchet@48975
  1137
  using Field_card_of card_of_Card_order[of A] by fastforce
blanchet@48975
  1138
  hence "|A \<times> A| \<le>o |A|"
blanchet@48975
  1139
  using Card_order_Times_same_infinite[of ?r] assms by auto
blanchet@48975
  1140
  thus ?thesis using card_of_Times3 ordIso_iff_ordLeq by blast
blanchet@48975
  1141
qed
blanchet@48975
  1142
blanchet@48975
  1143
blanchet@48975
  1144
lemma card_of_Times_infinite:
blanchet@48975
  1145
assumes INF: "infinite A" and NE: "B \<noteq> {}" and LEQ: "|B| \<le>o |A|"
blanchet@48975
  1146
shows "|A \<times> B| =o |A| \<and> |B \<times> A| =o |A|"
blanchet@48975
  1147
proof-
blanchet@48975
  1148
  have "|A| \<le>o |A \<times> B| \<and> |A| \<le>o |B \<times> A|"
blanchet@48975
  1149
  using assms by (simp add: card_of_Times1 card_of_Times2)
blanchet@48975
  1150
  moreover
blanchet@48975
  1151
  {have "|A \<times> B| \<le>o |A \<times> A| \<and> |B \<times> A| \<le>o |A \<times> A|"
blanchet@48975
  1152
   using LEQ card_of_Times_mono1 card_of_Times_mono2 by blast
blanchet@48975
  1153
   moreover have "|A \<times> A| =o |A|" using INF card_of_Times_same_infinite by blast
blanchet@48975
  1154
   ultimately have "|A \<times> B| \<le>o |A| \<and> |B \<times> A| \<le>o |A|"
blanchet@48975
  1155
   using ordLeq_ordIso_trans[of "|A \<times> B|"] ordLeq_ordIso_trans[of "|B \<times> A|"] by auto
blanchet@48975
  1156
  }
blanchet@48975
  1157
  ultimately show ?thesis by (simp add: ordIso_iff_ordLeq)
blanchet@48975
  1158
qed
blanchet@48975
  1159
blanchet@48975
  1160
blanchet@48975
  1161
corollary card_of_Times_infinite_simps:
blanchet@48975
  1162
"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A \<times> B| =o |A|"
blanchet@48975
  1163
"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |A \<times> B|"
blanchet@48975
  1164
"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |B \<times> A| =o |A|"
blanchet@48975
  1165
"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |B \<times> A|"
blanchet@48975
  1166
by (auto simp add: card_of_Times_infinite ordIso_symmetric)
blanchet@48975
  1167
blanchet@48975
  1168
blanchet@48975
  1169
corollary Card_order_Times_infinite:
blanchet@48975
  1170
assumes INF: "infinite(Field r)" and CARD: "Card_order r" and
blanchet@48975
  1171
        NE: "Field p \<noteq> {}" and LEQ: "p \<le>o r"
blanchet@48975
  1172
shows "| (Field r) \<times> (Field p) | =o r \<and> | (Field p) \<times> (Field r) | =o r"
blanchet@48975
  1173
proof-
blanchet@48975
  1174
  have "|Field r \<times> Field p| =o |Field r| \<and> |Field p \<times> Field r| =o |Field r|"
blanchet@48975
  1175
  using assms by (simp add: card_of_Times_infinite card_of_mono2)
blanchet@48975
  1176
  thus ?thesis
blanchet@48975
  1177
  using assms card_of_Field_ordIso[of r]
blanchet@48975
  1178
        ordIso_transitive[of "|Field r \<times> Field p|"]
blanchet@48975
  1179
        ordIso_transitive[of _ "|Field r|"] by blast
blanchet@48975
  1180
qed
blanchet@48975
  1181
blanchet@48975
  1182
blanchet@48975
  1183
lemma card_of_Sigma_ordLeq_infinite:
blanchet@48975
  1184
assumes INF: "infinite B" and
blanchet@48975
  1185
        LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
blanchet@48975
  1186
shows "|SIGMA i : I. A i| \<le>o |B|"
blanchet@48975
  1187
proof(cases "I = {}", simp add: card_of_empty)
blanchet@48975
  1188
  assume *: "I \<noteq> {}"
blanchet@48975
  1189
  have "|SIGMA i : I. A i| \<le>o |I \<times> B|"
blanchet@48975
  1190
  using LEQ card_of_Sigma_Times by blast
blanchet@48975
  1191
  moreover have "|I \<times> B| =o |B|"
blanchet@48975
  1192
  using INF * LEQ_I by (auto simp add: card_of_Times_infinite)
blanchet@48975
  1193
  ultimately show ?thesis using ordLeq_ordIso_trans by blast
blanchet@48975
  1194
qed
blanchet@48975
  1195
blanchet@48975
  1196
blanchet@48975
  1197
lemma card_of_Sigma_ordLeq_infinite_Field:
blanchet@48975
  1198
assumes INF: "infinite (Field r)" and r: "Card_order r" and
blanchet@48975
  1199
        LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
blanchet@48975
  1200
shows "|SIGMA i : I. A i| \<le>o r"
blanchet@48975
  1201
proof-
blanchet@48975
  1202
  let ?B  = "Field r"
blanchet@48975
  1203
  have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso
blanchet@48975
  1204
  ordIso_symmetric by blast
blanchet@48975
  1205
  hence "|I| \<le>o |?B|"  "\<forall>i \<in> I. |A i| \<le>o |?B|"
blanchet@48975
  1206
  using LEQ_I LEQ ordLeq_ordIso_trans by blast+
blanchet@48975
  1207
  hence  "|SIGMA i : I. A i| \<le>o |?B|" using INF LEQ
blanchet@48975
  1208
  card_of_Sigma_ordLeq_infinite by blast
blanchet@48975
  1209
  thus ?thesis using 1 ordLeq_ordIso_trans by blast
blanchet@48975
  1210
qed
blanchet@48975
  1211
blanchet@48975
  1212
blanchet@48975
  1213
lemma card_of_Times_ordLeq_infinite_Field:
blanchet@48975
  1214
"\<lbrakk>infinite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk>
blanchet@48975
  1215
 \<Longrightarrow> |A <*> B| \<le>o r"
blanchet@48975
  1216
by(simp add: card_of_Sigma_ordLeq_infinite_Field)
blanchet@48975
  1217
blanchet@48975
  1218
blanchet@48975
  1219
lemma card_of_UNION_ordLeq_infinite:
blanchet@48975
  1220
assumes INF: "infinite B" and
blanchet@48975
  1221
        LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
blanchet@48975
  1222
shows "|\<Union> i \<in> I. A i| \<le>o |B|"
blanchet@48975
  1223
proof(cases "I = {}", simp add: card_of_empty)
blanchet@48975
  1224
  assume *: "I \<noteq> {}"
blanchet@48975
  1225
  have "|\<Union> i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
blanchet@48975
  1226
  using card_of_UNION_Sigma by blast
blanchet@48975
  1227
  moreover have "|SIGMA i : I. A i| \<le>o |B|"
blanchet@48975
  1228
  using assms card_of_Sigma_ordLeq_infinite by blast
blanchet@48975
  1229
  ultimately show ?thesis using ordLeq_transitive by blast
blanchet@48975
  1230
qed
blanchet@48975
  1231
blanchet@48975
  1232
blanchet@48975
  1233
corollary card_of_UNION_ordLeq_infinite_Field:
blanchet@48975
  1234
assumes INF: "infinite (Field r)" and r: "Card_order r" and
blanchet@48975
  1235
        LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
blanchet@48975
  1236
shows "|\<Union> i \<in> I. A i| \<le>o r"
blanchet@48975
  1237
proof-
blanchet@48975
  1238
  let ?B  = "Field r"
blanchet@48975
  1239
  have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso
blanchet@48975
  1240
  ordIso_symmetric by blast
blanchet@48975
  1241
  hence "|I| \<le>o |?B|"  "\<forall>i \<in> I. |A i| \<le>o |?B|"
blanchet@48975
  1242
  using LEQ_I LEQ ordLeq_ordIso_trans by blast+
blanchet@48975
  1243
  hence  "|\<Union> i \<in> I. A i| \<le>o |?B|" using INF LEQ
blanchet@48975
  1244
  card_of_UNION_ordLeq_infinite by blast
blanchet@48975
  1245
  thus ?thesis using 1 ordLeq_ordIso_trans by blast
blanchet@48975
  1246
qed
blanchet@48975
  1247
blanchet@48975
  1248
blanchet@48975
  1249
lemma card_of_Plus_infinite1:
blanchet@48975
  1250
assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
blanchet@48975
  1251
shows "|A <+> B| =o |A|"
blanchet@48975
  1252
proof(cases "B = {}", simp add: card_of_Plus_empty1 card_of_Plus_empty2 ordIso_symmetric)
blanchet@48975
  1253
  let ?Inl = "Inl::'a \<Rightarrow> 'a + 'b"  let ?Inr = "Inr::'b \<Rightarrow> 'a + 'b"
blanchet@48975
  1254
  assume *: "B \<noteq> {}"
blanchet@48975
  1255
  then obtain b1 where 1: "b1 \<in> B" by blast
blanchet@48975
  1256
  show ?thesis
blanchet@48975
  1257
  proof(cases "B = {b1}")
blanchet@48975
  1258
    assume Case1: "B = {b1}"
blanchet@48975
  1259
    have 2: "bij_betw ?Inl A ((?Inl ` A))"
blanchet@48975
  1260
    unfolding bij_betw_def inj_on_def by auto
blanchet@48975
  1261
    hence 3: "infinite (?Inl ` A)"
blanchet@48975
  1262
    using INF bij_betw_finite[of ?Inl A] by blast
blanchet@48975
  1263
    let ?A' = "?Inl ` A \<union> {?Inr b1}"
blanchet@48975
  1264
    obtain g where "bij_betw g (?Inl ` A) ?A'"
blanchet@48975
  1265
    using 3 infinite_imp_bij_betw2[of "?Inl ` A"] by auto
blanchet@48975
  1266
    moreover have "?A' = A <+> B" using Case1 by blast
blanchet@48975
  1267
    ultimately have "bij_betw g (?Inl ` A) (A <+> B)" by simp
blanchet@48975
  1268
    hence "bij_betw (g o ?Inl) A (A <+> B)"
blanchet@48975
  1269
    using 2 by (auto simp add: bij_betw_trans)
blanchet@48975
  1270
    thus ?thesis using card_of_ordIso ordIso_symmetric by blast
blanchet@48975
  1271
  next
blanchet@48975
  1272
    assume Case2: "B \<noteq> {b1}"
blanchet@48975
  1273
    with * 1 obtain b2 where 3: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B" by fastforce
blanchet@48975
  1274
    obtain f where "inj_on f B \<and> f ` B \<le> A"
blanchet@48975
  1275
    using LEQ card_of_ordLeq[of B] by fastforce
blanchet@48975
  1276
    with 3 have "f b1 \<noteq> f b2 \<and> {f b1, f b2} \<le> A"
blanchet@48975
  1277
    unfolding inj_on_def by auto
blanchet@48975
  1278
    with 3 have "|A <+> B| \<le>o |A \<times> B|"
blanchet@48975
  1279
    by (auto simp add: card_of_Plus_Times)
blanchet@48975
  1280
    moreover have "|A \<times> B| =o |A|"
blanchet@48975
  1281
    using assms * by (simp add: card_of_Times_infinite_simps)
blanchet@48975
  1282
    ultimately have "|A <+> B| \<le>o |A|" using ordLeq_ordIso_trans by metis
blanchet@48975
  1283
    thus ?thesis using card_of_Plus1 ordIso_iff_ordLeq by blast
blanchet@48975
  1284
  qed
blanchet@48975
  1285
qed
blanchet@48975
  1286
blanchet@48975
  1287
blanchet@48975
  1288
lemma card_of_Plus_infinite2:
blanchet@48975
  1289
assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
blanchet@48975
  1290
shows "|B <+> A| =o |A|"
blanchet@48975
  1291
using assms card_of_Plus_commute card_of_Plus_infinite1
blanchet@48975
  1292
ordIso_equivalence by blast
blanchet@48975
  1293
blanchet@48975
  1294
blanchet@48975
  1295
lemma card_of_Plus_infinite:
blanchet@48975
  1296
assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
blanchet@48975
  1297
shows "|A <+> B| =o |A| \<and> |B <+> A| =o |A|"
blanchet@48975
  1298
using assms by (auto simp: card_of_Plus_infinite1 card_of_Plus_infinite2)
blanchet@48975
  1299
blanchet@48975
  1300
blanchet@48975
  1301
corollary Card_order_Plus_infinite:
blanchet@48975
  1302
assumes INF: "infinite(Field r)" and CARD: "Card_order r" and
blanchet@48975
  1303
        LEQ: "p \<le>o r"
blanchet@48975
  1304
shows "| (Field r) <+> (Field p) | =o r \<and> | (Field p) <+> (Field r) | =o r"
blanchet@48975
  1305
proof-
blanchet@48975
  1306
  have "| Field r <+> Field p | =o | Field r | \<and>
blanchet@48975
  1307
        | Field p <+> Field r | =o | Field r |"
blanchet@48975
  1308
  using assms by (simp add: card_of_Plus_infinite card_of_mono2)
blanchet@48975
  1309
  thus ?thesis
blanchet@48975
  1310
  using assms card_of_Field_ordIso[of r]
blanchet@48975
  1311
        ordIso_transitive[of "|Field r <+> Field p|"]
blanchet@48975
  1312
        ordIso_transitive[of _ "|Field r|"] by blast
blanchet@48975
  1313
qed
blanchet@48975
  1314
blanchet@48975
  1315
blanchet@48975
  1316
lemma card_of_Un_infinite:
blanchet@48975
  1317
assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
blanchet@48975
  1318
shows "|A \<union> B| =o |A| \<and> |B \<union> A| =o |A|"
blanchet@48975
  1319
proof-
blanchet@48975
  1320
  have "|A \<union> B| \<le>o |A <+> B|" by (rule card_of_Un_Plus_ordLeq)
blanchet@48975
  1321
  moreover have "|A <+> B| =o |A|"
blanchet@48975
  1322
  using assms by (metis card_of_Plus_infinite)
blanchet@48975
  1323
  ultimately have "|A \<union> B| \<le>o |A|" using ordLeq_ordIso_trans by blast
blanchet@48975
  1324
  hence "|A \<union> B| =o |A|" using card_of_Un1 ordIso_iff_ordLeq by blast
blanchet@48975
  1325
  thus ?thesis using Un_commute[of B A] by auto
blanchet@48975
  1326
qed
blanchet@48975
  1327
blanchet@48975
  1328
blanchet@48975
  1329
lemma card_of_Un_diff_infinite:
blanchet@48975
  1330
assumes INF: "infinite A" and LESS: "|B| <o |A|"
blanchet@48975
  1331
shows "|A - B| =o |A|"
blanchet@48975
  1332
proof-
blanchet@48975
  1333
  obtain C where C_def: "C = A - B" by blast
blanchet@48975
  1334
  have "|A \<union> B| =o |A|"
blanchet@48975
  1335
  using assms ordLeq_iff_ordLess_or_ordIso card_of_Un_infinite by blast
blanchet@48975
  1336
  moreover have "C \<union> B = A \<union> B" unfolding C_def by auto
blanchet@48975
  1337
  ultimately have 1: "|C \<union> B| =o |A|" by auto
blanchet@48975
  1338
  (*  *)
blanchet@48975
  1339
  {assume *: "|C| \<le>o |B|"
blanchet@48975
  1340
   moreover
blanchet@48975
  1341
   {assume **: "finite B"
blanchet@48975
  1342
    hence "finite C"
blanchet@48975
  1343
    using card_of_ordLeq_finite * by blast
blanchet@48975
  1344
    hence False using ** INF card_of_ordIso_finite 1 by blast
blanchet@48975
  1345
   }
blanchet@48975
  1346
   hence "infinite B" by auto
blanchet@48975
  1347
   ultimately have False
blanchet@48975
  1348
   using card_of_Un_infinite 1 ordIso_equivalence(1,3) LESS not_ordLess_ordIso by metis
blanchet@48975
  1349
  }
blanchet@48975
  1350
  hence 2: "|B| \<le>o |C|" using card_of_Well_order ordLeq_total by blast
blanchet@48975
  1351
  {assume *: "finite C"
blanchet@48975
  1352
    hence "finite B" using card_of_ordLeq_finite 2 by blast
blanchet@48975
  1353
    hence False using * INF card_of_ordIso_finite 1 by blast
blanchet@48975
  1354
  }
blanchet@48975
  1355
  hence "infinite C" by auto
blanchet@48975
  1356
  hence "|C| =o |A|"
blanchet@48975
  1357
  using  card_of_Un_infinite 1 2 ordIso_equivalence(1,3) by metis
blanchet@48975
  1358
  thus ?thesis unfolding C_def .
blanchet@48975
  1359
qed
blanchet@48975
  1360
blanchet@48975
  1361
blanchet@48975
  1362
lemma card_of_Plus_ordLess_infinite:
blanchet@48975
  1363
assumes INF: "infinite C" and
blanchet@48975
  1364
        LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
blanchet@48975
  1365
shows "|A <+> B| <o |C|"
blanchet@48975
  1366
proof(cases "A = {} \<or> B = {}")
blanchet@48975
  1367
  assume Case1: "A = {} \<or> B = {}"
blanchet@48975
  1368
  hence "|A| =o |A <+> B| \<or> |B| =o |A <+> B|"
blanchet@48975
  1369
  using card_of_Plus_empty1 card_of_Plus_empty2 by blast
blanchet@48975
  1370
  hence "|A <+> B| =o |A| \<or> |A <+> B| =o |B|"
blanchet@48975
  1371
  using ordIso_symmetric[of "|A|"] ordIso_symmetric[of "|B|"] by blast
blanchet@48975
  1372
  thus ?thesis using LESS1 LESS2
blanchet@48975
  1373
       ordIso_ordLess_trans[of "|A <+> B|" "|A|"]
blanchet@48975
  1374
       ordIso_ordLess_trans[of "|A <+> B|" "|B|"] by blast
blanchet@48975
  1375
next
blanchet@48975
  1376
  assume Case2: "\<not>(A = {} \<or> B = {})"
blanchet@48975
  1377
  {assume *: "|C| \<le>o |A <+> B|"
blanchet@48975
  1378
   hence "infinite (A <+> B)" using INF card_of_ordLeq_finite by blast
blanchet@48975
  1379
   hence 1: "infinite A \<or> infinite B" using finite_Plus by blast
blanchet@48975
  1380
   {assume Case21: "|A| \<le>o |B|"
blanchet@48975
  1381
    hence "infinite B" using 1 card_of_ordLeq_finite by blast
blanchet@48975
  1382
    hence "|A <+> B| =o |B|" using Case2 Case21
blanchet@48975
  1383
    by (auto simp add: card_of_Plus_infinite)
blanchet@48975
  1384
    hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
blanchet@48975
  1385
   }
blanchet@48975
  1386
   moreover
blanchet@48975
  1387
   {assume Case22: "|B| \<le>o |A|"
blanchet@48975
  1388
    hence "infinite A" using 1 card_of_ordLeq_finite by blast
blanchet@48975
  1389
    hence "|A <+> B| =o |A|" using Case2 Case22
blanchet@48975
  1390
    by (auto simp add: card_of_Plus_infinite)
blanchet@48975
  1391
    hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
blanchet@48975
  1392
   }
blanchet@48975
  1393
   ultimately have False using ordLeq_total card_of_Well_order[of A]
blanchet@48975
  1394
   card_of_Well_order[of B] by blast
blanchet@48975
  1395
  }
blanchet@48975
  1396
  thus ?thesis using ordLess_or_ordLeq[of "|A <+> B|" "|C|"]
blanchet@48975
  1397
  card_of_Well_order[of "A <+> B"] card_of_Well_order[of "C"] by auto
blanchet@48975
  1398
qed
blanchet@48975
  1399
blanchet@48975
  1400
blanchet@48975
  1401
lemma card_of_Plus_ordLess_infinite_Field:
blanchet@48975
  1402
assumes INF: "infinite (Field r)" and r: "Card_order r" and
blanchet@48975
  1403
        LESS1: "|A| <o r" and LESS2: "|B| <o r"
blanchet@48975
  1404
shows "|A <+> B| <o r"
blanchet@48975
  1405
proof-
blanchet@48975
  1406
  let ?C  = "Field r"
blanchet@48975
  1407
  have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso
blanchet@48975
  1408
  ordIso_symmetric by blast
blanchet@48975
  1409
  hence "|A| <o |?C|"  "|B| <o |?C|"
blanchet@48975
  1410
  using LESS1 LESS2 ordLess_ordIso_trans by blast+
blanchet@48975
  1411
  hence  "|A <+> B| <o |?C|" using INF
blanchet@48975
  1412
  card_of_Plus_ordLess_infinite by blast
blanchet@48975
  1413
  thus ?thesis using 1 ordLess_ordIso_trans by blast
blanchet@48975
  1414
qed
blanchet@48975
  1415
blanchet@48975
  1416
blanchet@48975
  1417
lemma infinite_card_of_insert:
blanchet@48975
  1418
assumes "infinite A"
blanchet@48975
  1419
shows "|insert a A| =o |A|"
blanchet@48975
  1420
proof-
blanchet@48975
  1421
  have iA: "insert a A = A \<union> {a}" by simp
blanchet@48975
  1422
  show ?thesis
blanchet@48975
  1423
  using infinite_imp_bij_betw2[OF assms] unfolding iA
blanchet@48975
  1424
  by (metis bij_betw_inv card_of_ordIso)
blanchet@48975
  1425
qed
blanchet@48975
  1426
blanchet@48975
  1427
blanchet@48975
  1428
subsection {* Cardinals versus lists  *}
blanchet@48975
  1429
blanchet@48975
  1430
blanchet@48975
  1431
text{* The next is an auxiliary operator, which shall be used for inductive
blanchet@48975
  1432
proofs of facts concerning the cardinality of @{text "List"} : *}
blanchet@48975
  1433
blanchet@48975
  1434
definition nlists :: "'a set \<Rightarrow> nat \<Rightarrow> 'a list set"
blanchet@48975
  1435
where "nlists A n \<equiv> {l. set l \<le> A \<and> length l = n}"
blanchet@48975
  1436
blanchet@48975
  1437
blanchet@48975
  1438
lemma lists_def2: "lists A = {l. set l \<le> A}"
blanchet@48975
  1439
using in_listsI by blast
blanchet@48975
  1440
blanchet@48975
  1441
blanchet@48975
  1442
lemma lists_UNION_nlists: "lists A = (\<Union> n. nlists A n)"
blanchet@48975
  1443
unfolding lists_def2 nlists_def by blast
blanchet@48975
  1444
blanchet@48975
  1445
blanchet@48975
  1446
lemma card_of_lists: "|A| \<le>o |lists A|"
blanchet@48975
  1447
proof-
blanchet@48975
  1448
  let ?h = "\<lambda> a. [a]"
blanchet@48975
  1449
  have "inj_on ?h A \<and> ?h ` A \<le> lists A"
blanchet@48975
  1450
  unfolding inj_on_def lists_def2 by auto
blanchet@48975
  1451
  thus ?thesis by (metis card_of_ordLeq)
blanchet@48975
  1452
qed
blanchet@48975
  1453
blanchet@48975
  1454
blanchet@48975
  1455
lemma nlists_0: "nlists A 0 = {[]}"
blanchet@48975
  1456
unfolding nlists_def by auto
blanchet@48975
  1457
blanchet@48975
  1458
blanchet@48975
  1459
lemma nlists_not_empty:
blanchet@48975
  1460
assumes "A \<noteq> {}"
blanchet@48975
  1461
shows "nlists A n \<noteq> {}"
blanchet@48975
  1462
proof(induct n, simp add: nlists_0)
blanchet@48975
  1463
  fix n assume "nlists A n \<noteq> {}"
blanchet@48975
  1464
  then obtain a and l where "a \<in> A \<and> l \<in> nlists A n" using assms by auto
blanchet@48975
  1465
  hence "a # l \<in> nlists A (Suc n)" unfolding nlists_def by auto
blanchet@48975
  1466
  thus "nlists A (Suc n) \<noteq> {}" by auto
blanchet@48975
  1467
qed
blanchet@48975
  1468
blanchet@48975
  1469
blanchet@48975
  1470
lemma Nil_in_lists: "[] \<in> lists A"
blanchet@48975
  1471
unfolding lists_def2 by auto
blanchet@48975
  1472
blanchet@48975
  1473
blanchet@48975
  1474
lemma lists_not_empty: "lists A \<noteq> {}"
blanchet@48975
  1475
using Nil_in_lists by blast
blanchet@48975
  1476
blanchet@48975
  1477
blanchet@48975
  1478
lemma card_of_nlists_Succ: "|nlists A (Suc n)| =o |A \<times> (nlists A n)|"
blanchet@48975
  1479
proof-
blanchet@48975
  1480
  let ?B = "A \<times> (nlists A n)"   let ?h = "\<lambda>(a,l). a # l"
blanchet@48975
  1481
  have "inj_on ?h ?B \<and> ?h ` ?B \<le> nlists A (Suc n)"
blanchet@48975
  1482
  unfolding inj_on_def nlists_def by auto
blanchet@48975
  1483
  moreover have "nlists A (Suc n) \<le> ?h ` ?B"
blanchet@48975
  1484
  proof(auto)
blanchet@48975
  1485
    fix l assume "l \<in> nlists A (Suc n)"
blanchet@48975
  1486
    hence 1: "length l = Suc n \<and> set l \<le> A" unfolding nlists_def by auto
blanchet@48975
  1487
    then obtain a and l' where 2: "l = a # l'" by (auto simp: length_Suc_conv)
blanchet@48975
  1488
    hence "a \<in> A \<and> set l' \<le> A \<and> length l' = n" using 1 by auto
blanchet@48975
  1489
    thus "l \<in> ?h ` ?B"  using 2 unfolding nlists_def by auto
blanchet@48975
  1490
  qed
blanchet@48975
  1491
  ultimately have "bij_betw ?h ?B (nlists A (Suc n))"
blanchet@48975
  1492
  unfolding bij_betw_def by auto
blanchet@48975
  1493
  thus ?thesis using card_of_ordIso ordIso_symmetric by blast
blanchet@48975
  1494
qed
blanchet@48975
  1495
blanchet@48975
  1496
blanchet@48975
  1497
lemma card_of_nlists_infinite:
blanchet@48975
  1498
assumes "infinite A"
blanchet@48975
  1499
shows "|nlists A n| \<le>o |A|"
blanchet@48975
  1500
proof(induct n)
blanchet@48975
  1501
  have "A \<noteq> {}" using assms by auto
blanchet@48975
  1502
  thus "|nlists A 0| \<le>o |A|" by (simp add: nlists_0 card_of_singl_ordLeq)
blanchet@48975
  1503
next
blanchet@48975
  1504
  fix n assume IH: "|nlists A n| \<le>o |A|"
blanchet@48975
  1505
  have "|nlists A (Suc n)| =o |A \<times> (nlists A n)|"
blanchet@48975
  1506
  using card_of_nlists_Succ by blast
blanchet@48975
  1507
  moreover
blanchet@48975
  1508
  {have "nlists A n \<noteq> {}" using assms nlists_not_empty[of A] by blast
blanchet@48975
  1509
   hence "|A \<times> (nlists A n)| =o |A|"
blanchet@48975
  1510
   using assms IH by (auto simp add: card_of_Times_infinite)
blanchet@48975
  1511
  }
blanchet@48975
  1512
  ultimately show "|nlists A (Suc n)| \<le>o |A|"
blanchet@48975
  1513
  using ordIso_transitive ordIso_iff_ordLeq by blast
blanchet@48975
  1514
qed
blanchet@48975
  1515
blanchet@48975
  1516
blanchet@48975
  1517
lemma card_of_lists_infinite:
blanchet@48975
  1518
assumes "infinite A"
blanchet@48975
  1519
shows "|lists A| =o |A|"
blanchet@48975
  1520
proof-
blanchet@48975
  1521
  have "|lists A| \<le>o |A|"
blanchet@48975
  1522
  using assms
blanchet@48975
  1523
  by (auto simp add: lists_UNION_nlists card_of_UNION_ordLeq_infinite
blanchet@48975
  1524
                     infinite_iff_card_of_nat card_of_nlists_infinite)
blanchet@48975
  1525
  thus ?thesis using card_of_lists ordIso_iff_ordLeq by blast
blanchet@48975
  1526
qed
blanchet@48975
  1527
blanchet@48975
  1528
blanchet@48975
  1529
lemma Card_order_lists_infinite:
blanchet@48975
  1530
assumes "Card_order r" and "infinite(Field r)"
blanchet@48975
  1531
shows "|lists(Field r)| =o r"
blanchet@48975
  1532
using assms card_of_lists_infinite card_of_Field_ordIso ordIso_transitive by blast
blanchet@48975
  1533
blanchet@48975
  1534
blanchet@48975
  1535
blanchet@48975
  1536
subsection {* The cardinal $\omega$ and the finite cardinals  *}
blanchet@48975
  1537
blanchet@48975
  1538
blanchet@48975
  1539
text{* The cardinal $\omega$, of natural numbers, shall be the standard non-strict
blanchet@48975
  1540
order relation on
blanchet@48975
  1541
@{text "nat"}, that we abbreviate by @{text "natLeq"}.  The finite cardinals
blanchet@48975
  1542
shall be the restrictions of these relations to the numbers smaller than
blanchet@48975
  1543
fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}.  *}
blanchet@48975
  1544
blanchet@48975
  1545
abbreviation "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}"
blanchet@48975
  1546
abbreviation "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}"
blanchet@48975
  1547
blanchet@48975
  1548
abbreviation natLeq_on :: "nat \<Rightarrow> (nat * nat) set"
blanchet@48975
  1549
where "natLeq_on n \<equiv> {(x,y). x < n \<and> y < n \<and> x \<le> y}"
blanchet@48975
  1550
blanchet@48975
  1551
lemma infinite_cartesian_product:
blanchet@48975
  1552
assumes "infinite A" "infinite B"
blanchet@48975
  1553
shows "infinite (A \<times> B)"
blanchet@48975
  1554
proof
blanchet@48975
  1555
  assume "finite (A \<times> B)"
blanchet@48975
  1556
  from assms(1) have "A \<noteq> {}" by auto
blanchet@48975
  1557
  with `finite (A \<times> B)` have "finite B" using finite_cartesian_productD2 by auto
blanchet@48975
  1558
  with assms(2) show False by simp
blanchet@48975
  1559
qed
blanchet@48975
  1560
blanchet@48975
  1561
blanchet@48975
  1562
blanchet@48975
  1563
subsubsection {* First as well-orders *}
blanchet@48975
  1564
blanchet@48975
  1565
blanchet@48975
  1566
lemma Field_natLeq: "Field natLeq = (UNIV::nat set)"
blanchet@48975
  1567
by(unfold Field_def, auto)
blanchet@48975
  1568
blanchet@48975
  1569
blanchet@48975
  1570
lemma natLeq_Refl: "Refl natLeq"
blanchet@48975
  1571
unfolding refl_on_def Field_def by auto
blanchet@48975
  1572
blanchet@48975
  1573
blanchet@48975
  1574
lemma natLeq_trans: "trans natLeq"
blanchet@48975
  1575
unfolding trans_def by auto
blanchet@48975
  1576
blanchet@48975
  1577
blanchet@48975
  1578
lemma natLeq_Preorder: "Preorder natLeq"
blanchet@48975
  1579
unfolding preorder_on_def
blanchet@48975
  1580
by (auto simp add: natLeq_Refl natLeq_trans)
blanchet@48975
  1581
blanchet@48975
  1582
blanchet@48975
  1583
lemma natLeq_antisym: "antisym natLeq"
blanchet@48975
  1584
unfolding antisym_def by auto
blanchet@48975
  1585
blanchet@48975
  1586
blanchet@48975
  1587
lemma natLeq_Partial_order: "Partial_order natLeq"
blanchet@48975
  1588
unfolding partial_order_on_def
blanchet@48975
  1589
by (auto simp add: natLeq_Preorder natLeq_antisym)
blanchet@48975
  1590
blanchet@48975
  1591
blanchet@48975
  1592
lemma natLeq_Total: "Total natLeq"
blanchet@48975
  1593
unfolding total_on_def by auto
blanchet@48975
  1594
blanchet@48975
  1595
blanchet@48975
  1596
lemma natLeq_Linear_order: "Linear_order natLeq"
blanchet@48975
  1597
unfolding linear_order_on_def
blanchet@48975
  1598
by (auto simp add: natLeq_Partial_order natLeq_Total)
blanchet@48975
  1599
blanchet@48975
  1600
blanchet@48975
  1601
lemma natLeq_natLess_Id: "natLess = natLeq - Id"
blanchet@48975
  1602
by auto
blanchet@48975
  1603
blanchet@48975
  1604
blanchet@48975
  1605
lemma natLeq_Well_order: "Well_order natLeq"
blanchet@48975
  1606
unfolding well_order_on_def
blanchet@48975
  1607
using natLeq_Linear_order wf_less natLeq_natLess_Id by auto
blanchet@48975
  1608
blanchet@48975
  1609
blanchet@48975
  1610
corollary natLeq_well_order_on: "well_order_on UNIV natLeq"
blanchet@48975
  1611
using natLeq_Well_order Field_natLeq by auto
blanchet@48975
  1612
blanchet@48975
  1613
blanchet@48975
  1614
lemma natLeq_wo_rel: "wo_rel natLeq"
blanchet@48975
  1615
unfolding wo_rel_def using natLeq_Well_order .
blanchet@48975
  1616
blanchet@48975
  1617
blanchet@48975
  1618
lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV"
blanchet@48975
  1619
using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto
blanchet@48975
  1620
blanchet@48975
  1621
blanchet@48975
  1622
lemma closed_nat_set_iff:
blanchet@48975
  1623
assumes "\<forall>(m::nat) n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
blanchet@48975
  1624
shows "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
blanchet@48975
  1625
proof-
blanchet@48975
  1626
  {assume "A \<noteq> UNIV" hence "\<exists>n. n \<notin> A" by blast
blanchet@48975
  1627
   moreover obtain n where n_def: "n = (LEAST n. n \<notin> A)" by blast
blanchet@48975
  1628
   ultimately have 1: "n \<notin> A \<and> (\<forall>m. m < n \<longrightarrow> m \<in> A)"
blanchet@48975
  1629
   using LeastI_ex[of "\<lambda> n. n \<notin> A"] n_def Least_le[of "\<lambda> n. n \<notin> A"] by fastforce
blanchet@48975
  1630
   have "A = {0 ..< n}"
blanchet@48975
  1631
   proof(auto simp add: 1)
blanchet@48975
  1632
     fix m assume *: "m \<in> A"
blanchet@48975
  1633
     {assume "n \<le> m" with assms * have "n \<in> A" by blast
blanchet@48975
  1634
      hence False using 1 by auto
blanchet@48975
  1635
     }
blanchet@48975
  1636
     thus "m < n" by fastforce
blanchet@48975
  1637
   qed
blanchet@48975
  1638
   hence "\<exists>n. A = {0 ..< n}" by blast
blanchet@48975
  1639
  }
blanchet@48975
  1640
  thus ?thesis by blast
blanchet@48975
  1641
qed
blanchet@48975
  1642
blanchet@48975
  1643
blanchet@48975
  1644
lemma Field_natLeq_on: "Field (natLeq_on n) = {0 ..< n}"
blanchet@48975
  1645
unfolding Field_def by auto
blanchet@48975
  1646
blanchet@48975
  1647
blanchet@48975
  1648
lemma natLeq_underS_less: "rel.underS natLeq n = {0 ..< n}"
blanchet@48975
  1649
unfolding rel.underS_def by auto
blanchet@48975
  1650
blanchet@48975
  1651
blanchet@48975
  1652
lemma Restr_natLeq: "Restr natLeq {0 ..< n} = natLeq_on n"
blanchet@48975
  1653
by auto
blanchet@48975
  1654
blanchet@48975
  1655
blanchet@48975
  1656
lemma Restr_natLeq2:
blanchet@48975
  1657
"Restr natLeq (rel.underS natLeq n) = natLeq_on n"
blanchet@48975
  1658
by (auto simp add: Restr_natLeq natLeq_underS_less)
blanchet@48975
  1659
blanchet@48975
  1660
blanchet@48975
  1661
lemma natLeq_on_Well_order: "Well_order(natLeq_on n)"
blanchet@48975
  1662
using Restr_natLeq[of n] natLeq_Well_order
blanchet@48975
  1663
      Well_order_Restr[of natLeq "{0..<n}"] by auto
blanchet@48975
  1664
blanchet@48975
  1665
blanchet@48975
  1666
corollary natLeq_on_well_order_on: "well_order_on {0 ..< n} (natLeq_on n)"
blanchet@48975
  1667
using natLeq_on_Well_order Field_natLeq_on by auto
blanchet@48975
  1668
blanchet@48975
  1669
blanchet@48975
  1670
lemma natLeq_on_wo_rel: "wo_rel(natLeq_on n)"
blanchet@48975
  1671
unfolding wo_rel_def using natLeq_on_Well_order .
blanchet@48975
  1672
blanchet@48975
  1673
blanchet@48975
  1674
lemma natLeq_on_ofilter_less_eq:
blanchet@48975
  1675
"n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}"
blanchet@48975
  1676
by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def,
blanchet@48975
  1677
    simp add: Field_natLeq_on, unfold rel.under_def, auto)
blanchet@48975
  1678
blanchet@48975
  1679
blanchet@48975
  1680
lemma natLeq_on_ofilter_iff:
blanchet@48975
  1681
"wo_rel.ofilter (natLeq_on m) A = (\<exists>n \<le> m. A = {0 ..< n})"
blanchet@48975
  1682
proof(rule iffI)
blanchet@48975
  1683
  assume *: "wo_rel.ofilter (natLeq_on m) A"
blanchet@48975
  1684
  hence 1: "A \<le> {0..<m}"
blanchet@48975
  1685
  by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def Field_natLeq_on)
blanchet@48975
  1686
  hence "\<forall>n1 n2. n2 \<in> A \<and> n1 \<le> n2 \<longrightarrow> n1 \<in> A"
blanchet@48975
  1687
  using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def)
blanchet@48975
  1688
  hence "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
blanchet@48975
  1689
  thus "\<exists>n \<le> m. A = {0 ..< n}" using 1 atLeastLessThan_less_eq by blast
blanchet@48975
  1690
next
blanchet@48975
  1691
  assume "(\<exists>n\<le>m. A = {0 ..< n})"
blanchet@48975
  1692
  thus "wo_rel.ofilter (natLeq_on m) A" by (auto simp add: natLeq_on_ofilter_less_eq)
blanchet@48975
  1693
qed
blanchet@48975
  1694
blanchet@48975
  1695
blanchet@48975
  1696
blanchet@48975
  1697
subsubsection {* Then as cardinals *}
blanchet@48975
  1698
blanchet@48975
  1699
blanchet@48975
  1700
lemma natLeq_Card_order: "Card_order natLeq"
blanchet@48975
  1701
proof(auto simp add: natLeq_Well_order
blanchet@48975
  1702
      Card_order_iff_Restr_underS Restr_natLeq2, simp add:  Field_natLeq)
blanchet@48975
  1703
  fix n have "finite(Field (natLeq_on n))"
blanchet@48975
  1704
  unfolding Field_natLeq_on by auto
blanchet@48975
  1705
  moreover have "infinite(UNIV::nat set)" by auto
blanchet@48975
  1706
  ultimately show "natLeq_on n <o |UNIV::nat set|"
blanchet@48975
  1707
  using finite_ordLess_infinite[of "natLeq_on n" "|UNIV::nat set|"]
blanchet@48975
  1708
        Field_card_of[of "UNIV::nat set"]
blanchet@48975
  1709
        card_of_Well_order[of "UNIV::nat set"] natLeq_on_Well_order[of n] by auto
blanchet@48975
  1710
qed
blanchet@48975
  1711
blanchet@48975
  1712
blanchet@48975
  1713
corollary card_of_Field_natLeq:
blanchet@48975
  1714
"|Field natLeq| =o natLeq"
blanchet@48975
  1715
using Field_natLeq natLeq_Card_order Card_order_iff_ordIso_card_of[of natLeq]
blanchet@48975
  1716
      ordIso_symmetric[of natLeq] by blast
blanchet@48975
  1717
blanchet@48975
  1718
blanchet@48975
  1719
corollary card_of_nat:
blanchet@48975
  1720
"|UNIV::nat set| =o natLeq"
blanchet@48975
  1721
using Field_natLeq card_of_Field_natLeq by auto
blanchet@48975
  1722
blanchet@48975
  1723
blanchet@48975
  1724
corollary infinite_iff_natLeq_ordLeq:
blanchet@48975
  1725
"infinite A = ( natLeq \<le>o |A| )"
blanchet@48975
  1726
using infinite_iff_card_of_nat[of A] card_of_nat
blanchet@48975
  1727
      ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
blanchet@48975
  1728
blanchet@48975
  1729
blanchet@48975
  1730
corollary finite_iff_ordLess_natLeq:
blanchet@48975
  1731
"finite A = ( |A| <o natLeq)"
blanchet@48975
  1732
using infinite_iff_natLeq_ordLeq not_ordLeq_iff_ordLess
blanchet@48975
  1733
      card_of_Well_order natLeq_Well_order by blast
blanchet@48975
  1734
blanchet@48975
  1735
blanchet@48975
  1736
lemma ordIso_natLeq_on_imp_finite:
blanchet@48975
  1737
"|A| =o natLeq_on n \<Longrightarrow> finite A"
blanchet@48975
  1738
unfolding ordIso_def iso_def[abs_def]
blanchet@48975
  1739
by (auto simp: Field_natLeq_on bij_betw_finite Field_card_of)
blanchet@48975
  1740
blanchet@48975
  1741
blanchet@48975
  1742
lemma natLeq_on_Card_order: "Card_order (natLeq_on n)"
blanchet@48975
  1743
proof(unfold card_order_on_def,
blanchet@48975
  1744
      auto simp add: natLeq_on_Well_order, simp add: Field_natLeq_on)
blanchet@48975
  1745
  fix r assume "well_order_on {0..<n} r"
blanchet@48975
  1746
  thus "natLeq_on n \<le>o r"
blanchet@48975
  1747
  using finite_atLeastLessThan natLeq_on_well_order_on
blanchet@48975
  1748
        finite_well_order_on_ordIso ordIso_iff_ordLeq by blast
blanchet@48975
  1749
qed
blanchet@48975
  1750
blanchet@48975
  1751
blanchet@48975
  1752
corollary card_of_Field_natLeq_on:
blanchet@48975
  1753
"|Field (natLeq_on n)| =o natLeq_on n"
blanchet@48975
  1754
using Field_natLeq_on natLeq_on_Card_order
blanchet@48975
  1755
      Card_order_iff_ordIso_card_of[of "natLeq_on n"]
blanchet@48975
  1756
      ordIso_symmetric[of "natLeq_on n"] by blast
blanchet@48975
  1757
blanchet@48975
  1758
blanchet@48975
  1759
corollary card_of_less:
blanchet@48975
  1760
"|{0 ..< n}| =o natLeq_on n"
blanchet@48975
  1761
using Field_natLeq_on card_of_Field_natLeq_on by auto
blanchet@48975
  1762
blanchet@48975
  1763
blanchet@48975
  1764
lemma natLeq_on_ordLeq_less_eq:
blanchet@48975
  1765
"((natLeq_on m) \<le>o (natLeq_on n)) = (m \<le> n)"
blanchet@48975
  1766
proof
blanchet@48975
  1767
  assume "natLeq_on m \<le>o natLeq_on n"
blanchet@48975
  1768
  then obtain f where "inj_on f {0..<m} \<and> f ` {0..<m} \<le> {0..<n}"
blanchet@48975
  1769
  using Field_natLeq_on[of m] Field_natLeq_on[of n]
blanchet@48975
  1770
  unfolding ordLeq_def using embed_inj_on[of "natLeq_on m"  "natLeq_on n"]
blanchet@48975
  1771
  embed_Field[of "natLeq_on m" "natLeq_on n"] using natLeq_on_Well_order[of m] by fastforce
blanchet@48975
  1772
  thus "m \<le> n" using atLeastLessThan_less_eq2 by blast
blanchet@48975
  1773
next
blanchet@48975
  1774
  assume "m \<le> n"
blanchet@48975
  1775
  hence "inj_on id {0..<m} \<and> id ` {0..<m} \<le> {0..<n}" unfolding inj_on_def by auto
blanchet@48975
  1776
  hence "|{0..<m}| \<le>o |{0..<n}|" using card_of_ordLeq by blast
blanchet@48975
  1777
  thus "natLeq_on m \<le>o natLeq_on n"
blanchet@48975
  1778
  using card_of_less ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
blanchet@48975
  1779
qed
blanchet@48975
  1780
blanchet@48975
  1781
blanchet@48975
  1782
lemma natLeq_on_ordLeq_less:
blanchet@48975
  1783
"((natLeq_on m) <o (natLeq_on n)) = (m < n)"
blanchet@48975
  1784
using not_ordLeq_iff_ordLess[of "natLeq_on m" "natLeq_on n"]
blanchet@48975
  1785
natLeq_on_Well_order natLeq_on_ordLeq_less_eq by auto
blanchet@48975
  1786
blanchet@48975
  1787
blanchet@48975
  1788
blanchet@48975
  1789
subsubsection {* "Backwards compatibility" with the numeric cardinal operator for finite sets *}
blanchet@48975
  1790
blanchet@48975
  1791
blanchet@48975
  1792
lemma finite_card_of_iff_card2:
blanchet@48975
  1793
assumes FIN: "finite A" and FIN': "finite B"
blanchet@48975
  1794
shows "( |A| \<le>o |B| ) = (card A \<le> card B)"
blanchet@48975
  1795
using assms card_of_ordLeq[of A B] inj_on_iff_card_le[of A B] by blast
blanchet@48975
  1796
blanchet@48975
  1797
blanchet@48975
  1798
lemma finite_imp_card_of_natLeq_on:
blanchet@48975
  1799
assumes "finite A"
blanchet@48975
  1800
shows "|A| =o natLeq_on (card A)"
blanchet@48975
  1801
proof-
blanchet@48975
  1802
  obtain h where "bij_betw h A {0 ..< card A}"
blanchet@48975
  1803
  using assms ex_bij_betw_finite_nat by blast
blanchet@48975
  1804
  thus ?thesis using card_of_ordIso card_of_less ordIso_equivalence by blast
blanchet@48975
  1805
qed
blanchet@48975
  1806
blanchet@48975
  1807
blanchet@48975
  1808
lemma finite_iff_card_of_natLeq_on:
blanchet@48975
  1809
"finite A = (\<exists>n. |A| =o natLeq_on n)"
blanchet@48975
  1810
using finite_imp_card_of_natLeq_on[of A]
blanchet@48975
  1811
by(auto simp add: ordIso_natLeq_on_imp_finite)
blanchet@48975
  1812
blanchet@48975
  1813
blanchet@48975
  1814
blanchet@48975
  1815
subsection {* The successor of a cardinal *}
blanchet@48975
  1816
blanchet@48975
  1817
blanchet@48975
  1818
text{* First we define @{text "isCardSuc r r'"}, the notion of @{text "r'"}
blanchet@48975
  1819
being a successor cardinal of @{text "r"}. Although the definition does
blanchet@48975
  1820
not require @{text "r"} to be a cardinal, only this case will be meaningful.  *}
blanchet@48975
  1821
blanchet@48975
  1822
blanchet@48975
  1823
definition isCardSuc :: "'a rel \<Rightarrow> 'a set rel \<Rightarrow> bool"
blanchet@48975
  1824
where
blanchet@48975
  1825
"isCardSuc r r' \<equiv>
blanchet@48975
  1826
 Card_order r' \<and> r <o r' \<and>
blanchet@48975
  1827
 (\<forall>(r''::'a set rel). Card_order r'' \<and> r <o r'' \<longrightarrow> r' \<le>o r'')"
blanchet@48975
  1828
blanchet@48975
  1829
blanchet@48975
  1830
text{* Now we introduce the cardinal-successor operator @{text "cardSuc"},
blanchet@48975
  1831
by picking {\em some} cardinal-order relation fulfilling @{text "isCardSuc"}.
blanchet@48975
  1832
Again, the picked item shall be proved unique up to order-isomorphism. *}
blanchet@48975
  1833
blanchet@48975
  1834
blanchet@48975
  1835
definition cardSuc :: "'a rel \<Rightarrow> 'a set rel"
blanchet@48975
  1836
where
blanchet@48975
  1837
"cardSuc r \<equiv> SOME r'. isCardSuc r r'"
blanchet@48975
  1838
blanchet@48975
  1839
blanchet@48975
  1840
lemma exists_minim_Card_order:
blanchet@48975
  1841
"\<lbrakk>R \<noteq> {}; \<forall>r \<in> R. Card_order r\<rbrakk> \<Longrightarrow> \<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"
blanchet@48975
  1842
unfolding card_order_on_def using exists_minim_Well_order by blast
blanchet@48975
  1843
blanchet@48975
  1844
blanchet@48975
  1845
lemma exists_isCardSuc:
blanchet@48975
  1846
assumes "Card_order r"
blanchet@48975
  1847
shows "\<exists>r'. isCardSuc r r'"
blanchet@48975
  1848
proof-
blanchet@48975
  1849
  let ?R = "{(r'::'a set rel). Card_order r' \<and> r <o r'}"
blanchet@48975
  1850
  have "|Pow(Field r)| \<in> ?R \<and> (\<forall>r \<in> ?R. Card_order r)" using assms
blanchet@48975
  1851
  by (simp add: card_of_Card_order Card_order_Pow)
blanchet@48975
  1852
  then obtain r where "r \<in> ?R \<and> (\<forall>r' \<in> ?R. r \<le>o r')"
blanchet@48975
  1853
  using exists_minim_Card_order[of ?R] by blast
blanchet@48975
  1854
  thus ?thesis unfolding isCardSuc_def by auto
blanchet@48975
  1855
qed
blanchet@48975
  1856
blanchet@48975
  1857
blanchet@48975
  1858
lemma cardSuc_isCardSuc:
blanchet@48975
  1859
assumes "Card_order r"
blanchet@48975
  1860
shows "isCardSuc r (cardSuc r)"
blanchet@48975
  1861
unfolding cardSuc_def using assms
blanchet@48975
  1862
by (simp add: exists_isCardSuc someI_ex)
blanchet@48975
  1863
blanchet@48975
  1864
blanchet@48975
  1865
lemma cardSuc_Card_order:
blanchet@48975
  1866
"Card_order r \<Longrightarrow> Card_order(cardSuc r)"
blanchet@48975
  1867
using cardSuc_isCardSuc unfolding isCardSuc_def by blast
blanchet@48975
  1868
blanchet@48975
  1869
blanchet@48975
  1870
lemma cardSuc_greater:
blanchet@48975
  1871
"Card_order r \<Longrightarrow> r <o cardSuc r"
blanchet@48975
  1872
using cardSuc_isCardSuc unfolding isCardSuc_def by blast
blanchet@48975
  1873
blanchet@48975
  1874
blanchet@48975
  1875
lemma cardSuc_ordLeq:
blanchet@48975
  1876
"Card_order r \<Longrightarrow> r \<le>o cardSuc r"
blanchet@48975
  1877
using cardSuc_greater ordLeq_iff_ordLess_or_ordIso by blast
blanchet@48975
  1878
blanchet@48975
  1879
blanchet@48975
  1880
text{* The minimality property of @{text "cardSuc"} originally present in its definition
blanchet@48975
  1881
is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}:  *}
blanchet@48975
  1882
blanchet@48975
  1883
lemma cardSuc_least_aux:
blanchet@48975
  1884
"\<lbrakk>Card_order (r::'a rel); Card_order (r'::'a set rel); r <o r'\<rbrakk> \<Longrightarrow> cardSuc r \<le>o r'"
blanchet@48975
  1885
using cardSuc_isCardSuc unfolding isCardSuc_def by blast
blanchet@48975
  1886
blanchet@48975
  1887
blanchet@48975
  1888
text{* But from this we can infer general minimality: *}
blanchet@48975
  1889
blanchet@48975
  1890
lemma cardSuc_least:
blanchet@48975
  1891
assumes CARD: "Card_order r" and CARD': "Card_order r'" and LESS: "r <o r'"
blanchet@48975
  1892
shows "cardSuc r \<le>o r'"
blanchet@48975
  1893
proof-
blanchet@48975
  1894
  let ?p = "cardSuc r"
blanchet@48975
  1895
  have 0: "Well_order ?p \<and> Well_order r'"
blanchet@48975
  1896
  using assms cardSuc_Card_order unfolding card_order_on_def by blast
blanchet@48975
  1897
  {assume "r' <o ?p"
blanchet@48975
  1898
   then obtain r'' where 1: "Field r'' < Field ?p" and 2: "r' =o r'' \<and> r'' <o ?p"
blanchet@48975
  1899
   using internalize_ordLess[of r' ?p] by blast
blanchet@48975
  1900
   (*  *)
blanchet@48975
  1901
   have "Card_order r''" using CARD' Card_order_ordIso2 2 by blast
blanchet@48975
  1902
   moreover have "r <o r''" using LESS 2 ordLess_ordIso_trans by blast
blanchet@48975
  1903
   ultimately have "?p \<le>o r''" using cardSuc_least_aux CARD by blast
blanchet@48975
  1904
   hence False using 2 not_ordLess_ordLeq by blast
blanchet@48975
  1905
  }
blanchet@48975
  1906
  thus ?thesis using 0 ordLess_or_ordLeq by blast
blanchet@48975
  1907
qed
blanchet@48975
  1908
blanchet@48975
  1909
blanchet@48975
  1910
lemma cardSuc_ordLess_ordLeq:
blanchet@48975
  1911
assumes CARD: "Card_order r" and CARD': "Card_order r'"
blanchet@48975
  1912
shows "(r <o r') = (cardSuc r \<le>o r')"
blanchet@48975
  1913
proof(auto simp add: assms cardSuc_least)
blanchet@48975
  1914
  assume "cardSuc r \<le>o r'"
blanchet@48975
  1915
  thus "r <o r'" using assms cardSuc_greater ordLess_ordLeq_trans by blast
blanchet@48975
  1916
qed
blanchet@48975
  1917
blanchet@48975
  1918
blanchet@48975
  1919
lemma cardSuc_ordLeq_ordLess:
blanchet@48975
  1920
assumes CARD: "Card_order r" and CARD': "Card_order r'"
blanchet@48975
  1921
shows "(r' <o cardSuc r) = (r' \<le>o r)"
blanchet@48975
  1922
proof-
blanchet@48975
  1923
  have "Well_order r \<and> Well_order r'"
blanchet@48975
  1924
  using assms unfolding card_order_on_def by auto
blanchet@48975
  1925
  moreover have "Well_order(cardSuc r)"
blanchet@48975
  1926
  using assms cardSuc_Card_order card_order_on_def by blast
blanchet@48975
  1927
  ultimately show ?thesis
blanchet@48975
  1928
  using assms cardSuc_ordLess_ordLeq[of r r']
blanchet@48975
  1929
  not_ordLeq_iff_ordLess[of r r'] not_ordLeq_iff_ordLess[of r' "cardSuc r"] by blast
blanchet@48975
  1930
qed
blanchet@48975
  1931
blanchet@48975
  1932
blanchet@48975
  1933
lemma cardSuc_mono_ordLeq:
blanchet@48975
  1934
assumes CARD: "Card_order r" and CARD': "Card_order r'"
blanchet@48975
  1935
shows "(cardSuc r \<le>o cardSuc r') = (r \<le>o r')"
blanchet@48975
  1936
using assms cardSuc_ordLeq_ordLess cardSuc_ordLess_ordLeq cardSuc_Card_order by blast
blanchet@48975
  1937
blanchet@48975
  1938
blanchet@48975
  1939
lemma cardSuc_invar_ordIso:
blanchet@48975
  1940
assumes CARD: "Card_order r" and CARD': "Card_order r'"
blanchet@48975
  1941
shows "(cardSuc r =o cardSuc r') = (r =o r')"
blanchet@48975
  1942
proof-
blanchet@48975
  1943
  have 0: "Well_order r \<and> Well_order r' \<and> Well_order(cardSuc r) \<and> Well_order(cardSuc r')"
blanchet@48975
  1944
  using assms by (simp add: card_order_on_well_order_on cardSuc_Card_order)
blanchet@48975
  1945
  thus ?thesis
blanchet@48975
  1946
  using ordIso_iff_ordLeq[of r r'] ordIso_iff_ordLeq
blanchet@48975
  1947
  using cardSuc_mono_ordLeq[of r r'] cardSuc_mono_ordLeq[of r' r] assms by blast
blanchet@48975
  1948
qed
blanchet@48975
  1949
blanchet@48975
  1950
blanchet@48975
  1951
lemma cardSuc_natLeq_on_Suc:
blanchet@48975
  1952
"cardSuc(natLeq_on n) =o natLeq_on(Suc n)"
blanchet@48975
  1953
proof-
blanchet@48975
  1954
  obtain r r' p where r_def: "r = natLeq_on n" and
blanchet@48975
  1955
                      r'_def: "r' = cardSuc(natLeq_on n)"  and
blanchet@48975
  1956
                      p_def: "p = natLeq_on(Suc n)" by blast
blanchet@48975
  1957
  (* Preliminary facts:  *)
blanchet@48975
  1958
  have CARD: "Card_order r \<and> Card_order r' \<and> Card_order p" unfolding r_def r'_def p_def
blanchet@48975
  1959
  using cardSuc_ordLess_ordLeq natLeq_on_Card_order cardSuc_Card_order by blast
blanchet@48975
  1960
  hence WELL: "Well_order r \<and> Well_order r' \<and>  Well_order p"
blanchet@48975
  1961
  unfolding card_order_on_def by force
blanchet@48975
  1962
  have FIELD: "Field r = {0..<n} \<and> Field p = {0..<(Suc n)}"
blanchet@48975
  1963
  unfolding r_def p_def Field_natLeq_on by simp
blanchet@48975
  1964
  hence FIN: "finite (Field r)" by force
blanchet@48975
  1965
  have "r <o r'" using CARD unfolding r_def r'_def using cardSuc_greater by blast
blanchet@48975
  1966
  hence "|Field r| <o r'" using CARD card_of_Field_ordIso ordIso_ordLess_trans by blast
blanchet@48975
  1967
  hence LESS: "|Field r| <o |Field r'|"
blanchet@48975
  1968
  using CARD card_of_Field_ordIso ordLess_ordIso_trans ordIso_symmetric by blast
blanchet@48975
  1969
  (* Main proof: *)
blanchet@48975
  1970
  have "r' \<le>o p" using CARD unfolding r_def r'_def p_def
blanchet@48975
  1971
  using natLeq_on_ordLeq_less cardSuc_ordLess_ordLeq by blast
blanchet@48975
  1972
  moreover have "p \<le>o r'"
blanchet@48975
  1973
  proof-
blanchet@48975
  1974
    {assume "r' <o p"
blanchet@48975
  1975
     then obtain f where 0: "embedS r' p f" unfolding ordLess_def by force
blanchet@48975
  1976
     let ?q = "Restr p (f ` Field r')"
blanchet@48975
  1977
     have 1: "embed r' p f" using 0 unfolding embedS_def by force
blanchet@48975
  1978
     hence 2: "f ` Field r' < {0..<(Suc n)}"
blanchet@48975
  1979
     using WELL FIELD 0 by (auto simp add: embedS_iff)
blanchet@48975
  1980
     have "wo_rel.ofilter p (f ` Field r')" using embed_Field_ofilter 1 WELL by blast
blanchet@48975
  1981
     then obtain m where "m \<le> Suc n" and 3: "f ` (Field r') = {0..<m}"
blanchet@48975
  1982
     unfolding p_def by (auto simp add: natLeq_on_ofilter_iff)
blanchet@48975
  1983
     hence 4: "m \<le> n" using 2 by force
blanchet@48975
  1984
     (*  *)
blanchet@48975
  1985
     have "bij_betw f (Field r') (f ` (Field r'))"
blanchet@48975
  1986
     using 1 WELL embed_inj_on unfolding bij_betw_def by force
blanchet@48975
  1987
     moreover have "finite(f ` (Field r'))" using 3 finite_atLeastLessThan[of 0 m] by force
blanchet@48975
  1988
     ultimately have 5: "finite (Field r') \<and> card(Field r') = card (f ` (Field r'))"
blanchet@48975
  1989
     using bij_betw_same_card bij_betw_finite by metis
blanchet@48975
  1990
     hence "card(Field r') \<le> card(Field r)" using 3 4 FIELD by force
blanchet@48975
  1991
     hence "|Field r'| \<le>o |Field r|" using FIN 5 finite_card_of_iff_card2 by blast
blanchet@48975
  1992
     hence False using LESS not_ordLess_ordLeq by auto
blanchet@48975
  1993
    }
blanchet@48975
  1994
    thus ?thesis using WELL CARD by (fastforce simp: not_ordLess_iff_ordLeq)
blanchet@48975
  1995
  qed
blanchet@48975
  1996
  ultimately show ?thesis using ordIso_iff_ordLeq unfolding r'_def p_def by blast
blanchet@48975
  1997
qed
blanchet@48975
  1998
blanchet@48975
  1999
blanchet@48975
  2000
lemma card_of_cardSuc_finite:
blanchet@48975
  2001
"finite(Field(cardSuc |A| )) = finite A"
blanchet@48975
  2002
proof
blanchet@48975
  2003
  assume *: "finite (Field (cardSuc |A| ))"
blanchet@48975
  2004
  have 0: "|Field(cardSuc |A| )| =o cardSuc |A|"
blanchet@48975
  2005
  using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast
blanchet@48975
  2006
  hence "|A| \<le>o |Field(cardSuc |A| )|"
blanchet@48975
  2007
  using card_of_Card_order[of A] cardSuc_ordLeq[of "|A|"] ordIso_symmetric
blanchet@48975
  2008
  ordLeq_ordIso_trans by blast
blanchet@48975
  2009
  thus "finite A" using * card_of_ordLeq_finite by blast
blanchet@48975
  2010
next
blanchet@48975
  2011
  assume "finite A"
blanchet@48975
  2012
  then obtain n where "|A| =o natLeq_on n" using finite_iff_card_of_natLeq_on by blast
blanchet@48975
  2013
  hence "cardSuc |A| =o cardSuc(natLeq_on n)"
blanchet@48975
  2014
  using card_of_Card_order cardSuc_invar_ordIso natLeq_on_Card_order by blast
blanchet@48975
  2015
  hence "cardSuc |A| =o natLeq_on(Suc n)"
blanchet@48975
  2016
  using cardSuc_natLeq_on_Suc ordIso_transitive by blast
blanchet@48975
  2017
  hence "cardSuc |A| =o |{0..<(Suc n)}|" using card_of_less ordIso_equivalence by blast
blanchet@48975
  2018
  moreover have "|Field (cardSuc |A| ) | =o cardSuc |A|"
blanchet@48975
  2019
  using card_of_Field_ordIso cardSuc_Card_order card_of_Card_order by blast
blanchet@48975
  2020
  ultimately have "|Field (cardSuc |A| ) | =o |{0..<(Suc n)}|"
blanchet@48975
  2021
  using ordIso_equivalence by blast
blanchet@48975
  2022
  thus "finite (Field (cardSuc |A| ))"
blanchet@48975
  2023
  using card_of_ordIso_finite finite_atLeastLessThan by blast
blanchet@48975
  2024
qed
blanchet@48975
  2025
blanchet@48975
  2026
blanchet@48975
  2027
lemma cardSuc_finite:
blanchet@48975
  2028
assumes "Card_order r"
blanchet@48975
  2029
shows "finite (Field (cardSuc r)) = finite (Field r)"
blanchet@48975
  2030
proof-
blanchet@48975
  2031
  let ?A = "Field r"
blanchet@48975
  2032
  have "|?A| =o r" using assms by (simp add: card_of_Field_ordIso)
blanchet@48975
  2033
  hence "cardSuc |?A| =o cardSuc r" using assms
blanchet@48975
  2034
  by (simp add: card_of_Card_order cardSuc_invar_ordIso)
blanchet@48975
  2035
  moreover have "|Field (cardSuc |?A| ) | =o cardSuc |?A|"
blanchet@48975
  2036
  by (simp add: card_of_card_order_on Field_card_of card_of_Field_ordIso cardSuc_Card_order)
blanchet@48975
  2037
  moreover
blanchet@48975
  2038
  {have "|Field (cardSuc r) | =o cardSuc r"
blanchet@48975
  2039
   using assms by (simp add: card_of_Field_ordIso cardSuc_Card_order)
blanchet@48975
  2040
   hence "cardSuc r =o |Field (cardSuc r) |"
blanchet@48975
  2041
   using ordIso_symmetric by blast
blanchet@48975
  2042
  }
blanchet@48975
  2043
  ultimately have "|Field (cardSuc |?A| ) | =o |Field (cardSuc r) |"
blanchet@48975
  2044
  using ordIso_transitive by blast
blanchet@48975
  2045
  hence "finite (Field (cardSuc |?A| )) = finite (Field (cardSuc r))"
blanchet@48975
  2046
  using card_of_ordIso_finite by blast
blanchet@48975
  2047
  thus ?thesis by (simp only: card_of_cardSuc_finite)
blanchet@48975
  2048
qed
blanchet@48975
  2049
blanchet@48975
  2050
blanchet@48975
  2051
lemma card_of_Plus_ordLeq_infinite_Field:
blanchet@48975
  2052
assumes r: "infinite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
blanchet@48975
  2053
and c: "Card_order r"
blanchet@48975
  2054
shows "|A <+> B| \<le>o r"
blanchet@48975
  2055
proof-
blanchet@48975
  2056
  let ?r' = "cardSuc r"
blanchet@48975
  2057
  have "Card_order ?r' \<and> infinite (Field ?r')" using assms
blanchet@48975
  2058
  by (simp add: cardSuc_Card_order cardSuc_finite)
blanchet@48975
  2059
  moreover have "|A| <o ?r'" and "|B| <o ?r'" using A B c
blanchet@48975
  2060
  by (auto simp: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
blanchet@48975
  2061
  ultimately have "|A <+> B| <o ?r'"
blanchet@48975
  2062
  using card_of_Plus_ordLess_infinite_Field by blast
blanchet@48975
  2063
  thus ?thesis using c r
blanchet@48975
  2064
  by (simp add: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
blanchet@48975
  2065
qed
blanchet@48975
  2066
blanchet@48975
  2067
blanchet@48975
  2068
lemma card_of_Un_ordLeq_infinite_Field:
blanchet@48975
  2069
assumes C: "infinite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
blanchet@48975
  2070
and "Card_order r"
blanchet@48975
  2071
shows "|A Un B| \<le>o r"
blanchet@48975
  2072
using assms card_of_Plus_ordLeq_infinite_Field card_of_Un_Plus_ordLeq
blanchet@48975
  2073
ordLeq_transitive by blast
blanchet@48975
  2074
blanchet@48975
  2075
blanchet@48975
  2076
blanchet@48975
  2077
subsection {* Regular cardinals *}
blanchet@48975
  2078
blanchet@48975
  2079
blanchet@48975
  2080
definition cofinal where
blanchet@48975
  2081
"cofinal A r \<equiv>
blanchet@48975
  2082
 ALL a : Field r. EX b : A. a \<noteq> b \<and> (a,b) : r"
blanchet@48975
  2083
blanchet@48975
  2084
blanchet@48975
  2085
definition regular where
blanchet@48975
  2086
"regular r \<equiv>
blanchet@48975
  2087
 ALL K. K \<le> Field r \<and> cofinal K r \<longrightarrow> |K| =o r"
blanchet@48975
  2088
blanchet@48975
  2089
blanchet@48975
  2090
definition relChain where
blanchet@48975
  2091
"relChain r As \<equiv>
blanchet@48975
  2092
 ALL i j. (i,j) \<in> r \<longrightarrow> As i \<le> As j"
blanchet@48975
  2093
blanchet@48975
  2094
lemma regular_UNION:
blanchet@48975
  2095
assumes r: "Card_order r"   "regular r"
blanchet@48975
  2096
and As: "relChain r As"
blanchet@48975
  2097
and Bsub: "B \<le> (UN i : Field r. As i)"
blanchet@48975
  2098
and cardB: "|B| <o r"