src/HOL/Cardinals/Cardinal_Order_Relation.thy
author haftmann
Sat Jan 11 21:03:11 2014 +0100 (2014-01-11)
changeset 54989 0fd6b0660242
parent 54980 7e0573a490ee
child 55023 38db7814481d
permissions -rw-r--r--
shot in the dark to make LaTeX happy again
blanchet@49310
     1
(*  Title:      HOL/Cardinals/Cardinal_Order_Relation.thy
blanchet@48975
     2
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     3
    Copyright   2012
blanchet@48975
     4
blanchet@48975
     5
Cardinal-order relations.
blanchet@48975
     6
*)
blanchet@48975
     7
blanchet@48975
     8
header {* Cardinal-Order Relations *}
blanchet@48975
     9
blanchet@48975
    10
theory Cardinal_Order_Relation
blanchet@54481
    11
imports Cardinal_Order_Relation_FP Constructions_on_Wellorders
blanchet@48975
    12
begin
blanchet@48975
    13
blanchet@48975
    14
declare
blanchet@48975
    15
  card_order_on_well_order_on[simp]
blanchet@48975
    16
  card_of_card_order_on[simp]
blanchet@48975
    17
  card_of_well_order_on[simp]
blanchet@48975
    18
  Field_card_of[simp]
blanchet@48975
    19
  card_of_Card_order[simp]
blanchet@48975
    20
  card_of_Well_order[simp]
blanchet@48975
    21
  card_of_least[simp]
blanchet@48975
    22
  card_of_unique[simp]
blanchet@48975
    23
  card_of_mono1[simp]
blanchet@48975
    24
  card_of_mono2[simp]
blanchet@48975
    25
  card_of_cong[simp]
blanchet@48975
    26
  card_of_Field_ordLess[simp]
blanchet@48975
    27
  card_of_Field_ordIso[simp]
blanchet@48975
    28
  card_of_underS[simp]
blanchet@48975
    29
  ordLess_Field[simp]
blanchet@48975
    30
  card_of_empty[simp]
blanchet@48975
    31
  card_of_empty1[simp]
blanchet@48975
    32
  card_of_image[simp]
blanchet@48975
    33
  card_of_singl_ordLeq[simp]
blanchet@48975
    34
  Card_order_singl_ordLeq[simp]
blanchet@48975
    35
  card_of_Pow[simp]
blanchet@48975
    36
  Card_order_Pow[simp]
blanchet@48975
    37
  card_of_Plus1[simp]
blanchet@48975
    38
  Card_order_Plus1[simp]
blanchet@48975
    39
  card_of_Plus2[simp]
blanchet@48975
    40
  Card_order_Plus2[simp]
blanchet@48975
    41
  card_of_Plus_mono1[simp]
blanchet@48975
    42
  card_of_Plus_mono2[simp]
blanchet@48975
    43
  card_of_Plus_mono[simp]
blanchet@48975
    44
  card_of_Plus_cong2[simp]
blanchet@48975
    45
  card_of_Plus_cong[simp]
blanchet@48975
    46
  card_of_Un_Plus_ordLeq[simp]
blanchet@48975
    47
  card_of_Times1[simp]
blanchet@48975
    48
  card_of_Times2[simp]
blanchet@48975
    49
  card_of_Times3[simp]
blanchet@48975
    50
  card_of_Times_mono1[simp]
blanchet@48975
    51
  card_of_Times_mono2[simp]
blanchet@48975
    52
  card_of_ordIso_finite[simp]
blanchet@48975
    53
  card_of_Times_same_infinite[simp]
blanchet@48975
    54
  card_of_Times_infinite_simps[simp]
blanchet@48975
    55
  card_of_Plus_infinite1[simp]
blanchet@48975
    56
  card_of_Plus_infinite2[simp]
blanchet@48975
    57
  card_of_Plus_ordLess_infinite[simp]
blanchet@48975
    58
  card_of_Plus_ordLess_infinite_Field[simp]
blanchet@48975
    59
  infinite_cartesian_product[simp]
blanchet@48975
    60
  cardSuc_Card_order[simp]
blanchet@48975
    61
  cardSuc_greater[simp]
blanchet@48975
    62
  cardSuc_ordLeq[simp]
blanchet@48975
    63
  cardSuc_ordLeq_ordLess[simp]
blanchet@48975
    64
  cardSuc_mono_ordLeq[simp]
blanchet@48975
    65
  cardSuc_invar_ordIso[simp]
blanchet@48975
    66
  card_of_cardSuc_finite[simp]
blanchet@48975
    67
  cardSuc_finite[simp]
blanchet@48975
    68
  card_of_Plus_ordLeq_infinite_Field[simp]
blanchet@48975
    69
  curr_in[intro, simp]
blanchet@48975
    70
blanchet@48975
    71
blanchet@48975
    72
subsection {* Cardinal of a set *}
blanchet@48975
    73
blanchet@48975
    74
lemma card_of_inj_rel: assumes INJ: "!! x y y'. \<lbrakk>(x,y) : R; (x,y') : R\<rbrakk> \<Longrightarrow> y = y'"
blanchet@48975
    75
shows "|{y. EX x. (x,y) : R}| <=o |{x. EX y. (x,y) : R}|"
blanchet@48975
    76
proof-
blanchet@48975
    77
  let ?Y = "{y. EX x. (x,y) : R}"  let ?X = "{x. EX y. (x,y) : R}"
blanchet@48975
    78
  let ?f = "% y. SOME x. (x,y) : R"
traytel@51764
    79
  have "?f ` ?Y <= ?X" by (auto dest: someI)
blanchet@48975
    80
  moreover have "inj_on ?f ?Y"
blanchet@48975
    81
  unfolding inj_on_def proof(auto)
blanchet@48975
    82
    fix y1 x1 y2 x2
blanchet@48975
    83
    assume *: "(x1, y1) \<in> R" "(x2, y2) \<in> R" and **: "?f y1 = ?f y2"
blanchet@48975
    84
    hence "(?f y1,y1) : R" using someI[of "% x. (x,y1) : R"] by auto
blanchet@48975
    85
    moreover have "(?f y2,y2) : R" using * someI[of "% x. (x,y2) : R"] by auto
blanchet@48975
    86
    ultimately show "y1 = y2" using ** INJ by auto
blanchet@48975
    87
  qed
blanchet@48975
    88
  ultimately show "|?Y| <=o |?X|" using card_of_ordLeq by blast
blanchet@48975
    89
qed
blanchet@48975
    90
blanchet@48975
    91
lemma card_of_unique2: "\<lbrakk>card_order_on B r; bij_betw f A B\<rbrakk> \<Longrightarrow> r =o |A|"
blanchet@48975
    92
using card_of_ordIso card_of_unique ordIso_equivalence by blast
blanchet@48975
    93
blanchet@48975
    94
lemma internalize_card_of_ordLess:
blanchet@48975
    95
"( |A| <o r) = (\<exists>B < Field r. |A| =o |B| \<and> |B| <o r)"
blanchet@48975
    96
proof
blanchet@48975
    97
  assume "|A| <o r"
blanchet@48975
    98
  then obtain p where 1: "Field p < Field r \<and> |A| =o p \<and> p <o r"
blanchet@48975
    99
  using internalize_ordLess[of "|A|" r] by blast
blanchet@48975
   100
  hence "Card_order p" using card_of_Card_order Card_order_ordIso2 by blast
blanchet@48975
   101
  hence "|Field p| =o p" using card_of_Field_ordIso by blast
blanchet@48975
   102
  hence "|A| =o |Field p| \<and> |Field p| <o r"
blanchet@48975
   103
  using 1 ordIso_equivalence ordIso_ordLess_trans by blast
blanchet@48975
   104
  thus "\<exists>B < Field r. |A| =o |B| \<and> |B| <o r" using 1 by blast
blanchet@48975
   105
next
blanchet@48975
   106
  assume "\<exists>B < Field r. |A| =o |B| \<and> |B| <o r"
blanchet@48975
   107
  thus "|A| <o r" using ordIso_ordLess_trans by blast
blanchet@48975
   108
qed
blanchet@48975
   109
blanchet@48975
   110
lemma internalize_card_of_ordLess2:
blanchet@48975
   111
"( |A| <o |C| ) = (\<exists>B < C. |A| =o |B| \<and> |B| <o |C| )"
blanchet@48975
   112
using internalize_card_of_ordLess[of "A" "|C|"] Field_card_of[of C] by auto
blanchet@48975
   113
blanchet@48975
   114
lemma Card_order_omax:
blanchet@48975
   115
assumes "finite R" and "R \<noteq> {}" and "\<forall>r\<in>R. Card_order r"
blanchet@48975
   116
shows "Card_order (omax R)"
blanchet@48975
   117
proof-
blanchet@48975
   118
  have "\<forall>r\<in>R. Well_order r"
blanchet@48975
   119
  using assms unfolding card_order_on_def by simp
blanchet@48975
   120
  thus ?thesis using assms apply - apply(drule omax_in) by auto
blanchet@48975
   121
qed
blanchet@48975
   122
blanchet@48975
   123
lemma Card_order_omax2:
blanchet@48975
   124
assumes "finite I" and "I \<noteq> {}"
blanchet@48975
   125
shows "Card_order (omax {|A i| | i. i \<in> I})"
blanchet@48975
   126
proof-
blanchet@48975
   127
  let ?R = "{|A i| | i. i \<in> I}"
blanchet@48975
   128
  have "finite ?R" and "?R \<noteq> {}" using assms by auto
blanchet@48975
   129
  moreover have "\<forall>r\<in>?R. Card_order r"
blanchet@48975
   130
  using card_of_Card_order by auto
blanchet@48975
   131
  ultimately show ?thesis by(rule Card_order_omax)
blanchet@48975
   132
qed
blanchet@48975
   133
blanchet@48975
   134
blanchet@48975
   135
subsection {* Cardinals versus set operations on arbitrary sets *}
blanchet@48975
   136
blanchet@54481
   137
lemma card_of_set_type[simp]: "|UNIV::'a set| <o |UNIV::'a set set|"
blanchet@54475
   138
using card_of_Pow[of "UNIV::'a set"] by simp
blanchet@54475
   139
blanchet@54475
   140
lemma card_of_Un1[simp]:
blanchet@54475
   141
shows "|A| \<le>o |A \<union> B| "
blanchet@54475
   142
using inj_on_id[of A] card_of_ordLeq[of A _] by fastforce
blanchet@54475
   143
blanchet@54475
   144
lemma card_of_diff[simp]:
blanchet@54475
   145
shows "|A - B| \<le>o |A|"
blanchet@54475
   146
using inj_on_id[of "A - B"] card_of_ordLeq[of "A - B" _] by fastforce
blanchet@54475
   147
blanchet@48975
   148
lemma subset_ordLeq_strict:
blanchet@48975
   149
assumes "A \<le> B" and "|A| <o |B|"
blanchet@48975
   150
shows "A < B"
blanchet@48975
   151
proof-
blanchet@48975
   152
  {assume "\<not>(A < B)"
blanchet@48975
   153
   hence "A = B" using assms(1) by blast
blanchet@48975
   154
   hence False using assms(2) not_ordLess_ordIso card_of_refl by blast
blanchet@48975
   155
  }
blanchet@48975
   156
  thus ?thesis by blast
blanchet@48975
   157
qed
blanchet@48975
   158
blanchet@48975
   159
corollary subset_ordLeq_diff:
blanchet@48975
   160
assumes "A \<le> B" and "|A| <o |B|"
blanchet@48975
   161
shows "B - A \<noteq> {}"
blanchet@48975
   162
using assms subset_ordLeq_strict by blast
blanchet@48975
   163
blanchet@48975
   164
lemma card_of_empty4:
blanchet@48975
   165
"|{}::'b set| <o |A::'a set| = (A \<noteq> {})"
blanchet@48975
   166
proof(intro iffI notI)
blanchet@48975
   167
  assume *: "|{}::'b set| <o |A|" and "A = {}"
blanchet@48975
   168
  hence "|A| =o |{}::'b set|"
blanchet@48975
   169
  using card_of_ordIso unfolding bij_betw_def inj_on_def by blast
blanchet@48975
   170
  hence "|{}::'b set| =o |A|" using ordIso_symmetric by blast
blanchet@48975
   171
  with * show False using not_ordLess_ordIso[of "|{}::'b set|" "|A|"] by blast
blanchet@48975
   172
next
blanchet@48975
   173
  assume "A \<noteq> {}"
blanchet@48975
   174
  hence "(\<not> (\<exists>f. inj_on f A \<and> f ` A \<subseteq> {}))"
blanchet@48975
   175
  unfolding inj_on_def by blast
blanchet@48975
   176
  thus "| {} | <o | A |"
blanchet@48975
   177
  using card_of_ordLess by blast
blanchet@48975
   178
qed
blanchet@48975
   179
blanchet@48975
   180
lemma card_of_empty5:
blanchet@48975
   181
"|A| <o |B| \<Longrightarrow> B \<noteq> {}"
blanchet@48975
   182
using card_of_empty not_ordLess_ordLeq by blast
blanchet@48975
   183
blanchet@48975
   184
lemma Well_order_card_of_empty:
blanchet@48975
   185
"Well_order r \<Longrightarrow> |{}| \<le>o r" by simp
blanchet@48975
   186
blanchet@48975
   187
lemma card_of_UNIV[simp]:
blanchet@48975
   188
"|A :: 'a set| \<le>o |UNIV :: 'a set|"
blanchet@48975
   189
using card_of_mono1[of A] by simp
blanchet@48975
   190
blanchet@48975
   191
lemma card_of_UNIV2[simp]:
blanchet@48975
   192
"Card_order r \<Longrightarrow> (r :: 'a rel) \<le>o |UNIV :: 'a set|"
blanchet@48975
   193
using card_of_UNIV[of "Field r"] card_of_Field_ordIso
blanchet@48975
   194
      ordIso_symmetric ordIso_ordLeq_trans by blast
blanchet@48975
   195
blanchet@48975
   196
lemma card_of_Pow_mono[simp]:
blanchet@48975
   197
assumes "|A| \<le>o |B|"
blanchet@48975
   198
shows "|Pow A| \<le>o |Pow B|"
blanchet@48975
   199
proof-
blanchet@48975
   200
  obtain f where "inj_on f A \<and> f ` A \<le> B"
blanchet@48975
   201
  using assms card_of_ordLeq[of A B] by auto
blanchet@48975
   202
  hence "inj_on (image f) (Pow A) \<and> (image f) ` (Pow A) \<le> (Pow B)"
blanchet@48975
   203
  by (auto simp add: inj_on_image_Pow image_Pow_mono)
blanchet@48975
   204
  thus ?thesis using card_of_ordLeq[of "Pow A"] by metis
blanchet@48975
   205
qed
blanchet@48975
   206
blanchet@48975
   207
lemma ordIso_Pow_mono[simp]:
blanchet@48975
   208
assumes "r \<le>o r'"
blanchet@48975
   209
shows "|Pow(Field r)| \<le>o |Pow(Field r')|"
blanchet@48975
   210
using assms card_of_mono2 card_of_Pow_mono by blast
blanchet@48975
   211
blanchet@48975
   212
lemma card_of_Pow_cong[simp]:
blanchet@48975
   213
assumes "|A| =o |B|"
blanchet@48975
   214
shows "|Pow A| =o |Pow B|"
blanchet@48975
   215
proof-
blanchet@48975
   216
  obtain f where "bij_betw f A B"
blanchet@48975
   217
  using assms card_of_ordIso[of A B] by auto
blanchet@48975
   218
  hence "bij_betw (image f) (Pow A) (Pow B)"
blanchet@48975
   219
  by (auto simp add: bij_betw_image_Pow)
blanchet@48975
   220
  thus ?thesis using card_of_ordIso[of "Pow A"] by auto
blanchet@48975
   221
qed
blanchet@48975
   222
blanchet@48975
   223
lemma ordIso_Pow_cong[simp]:
blanchet@48975
   224
assumes "r =o r'"
blanchet@48975
   225
shows "|Pow(Field r)| =o |Pow(Field r')|"
blanchet@48975
   226
using assms card_of_cong card_of_Pow_cong by blast
blanchet@48975
   227
blanchet@48975
   228
corollary Card_order_Plus_empty1:
blanchet@48975
   229
"Card_order r \<Longrightarrow> r =o |(Field r) <+> {}|"
blanchet@48975
   230
using card_of_Plus_empty1 card_of_Field_ordIso ordIso_equivalence by blast
blanchet@48975
   231
blanchet@48975
   232
corollary Card_order_Plus_empty2:
blanchet@48975
   233
"Card_order r \<Longrightarrow> r =o |{} <+> (Field r)|"
blanchet@48975
   234
using card_of_Plus_empty2 card_of_Field_ordIso ordIso_equivalence by blast
blanchet@48975
   235
blanchet@48975
   236
lemma Card_order_Un1:
blanchet@48975
   237
shows "Card_order r \<Longrightarrow> |Field r| \<le>o |(Field r) \<union> B| "
blanchet@48975
   238
using card_of_Un1 card_of_Field_ordIso ordIso_symmetric ordIso_ordLeq_trans by auto
blanchet@48975
   239
blanchet@48975
   240
lemma card_of_Un2[simp]:
blanchet@48975
   241
shows "|A| \<le>o |B \<union> A|"
blanchet@48975
   242
using inj_on_id[of A] card_of_ordLeq[of A _] by fastforce
blanchet@48975
   243
blanchet@48975
   244
lemma Card_order_Un2:
blanchet@48975
   245
shows "Card_order r \<Longrightarrow> |Field r| \<le>o |A \<union> (Field r)| "
blanchet@48975
   246
using card_of_Un2 card_of_Field_ordIso ordIso_symmetric ordIso_ordLeq_trans by auto
blanchet@48975
   247
blanchet@48975
   248
lemma Un_Plus_bij_betw:
blanchet@48975
   249
assumes "A Int B = {}"
blanchet@48975
   250
shows "\<exists>f. bij_betw f (A \<union> B) (A <+> B)"
blanchet@48975
   251
proof-
blanchet@48975
   252
  let ?f = "\<lambda> c. if c \<in> A then Inl c else Inr c"
blanchet@48975
   253
  have "bij_betw ?f (A \<union> B) (A <+> B)"
blanchet@48975
   254
  using assms by(unfold bij_betw_def inj_on_def, auto)
blanchet@48975
   255
  thus ?thesis by blast
blanchet@48975
   256
qed
blanchet@48975
   257
blanchet@48975
   258
lemma card_of_Un_Plus_ordIso:
blanchet@48975
   259
assumes "A Int B = {}"
blanchet@48975
   260
shows "|A \<union> B| =o |A <+> B|"
blanchet@48975
   261
using assms card_of_ordIso[of "A \<union> B"] Un_Plus_bij_betw[of A B] by auto
blanchet@48975
   262
blanchet@48975
   263
lemma card_of_Un_Plus_ordIso1:
blanchet@48975
   264
"|A \<union> B| =o |A <+> (B - A)|"
blanchet@48975
   265
using card_of_Un_Plus_ordIso[of A "B - A"] by auto
blanchet@48975
   266
blanchet@48975
   267
lemma card_of_Un_Plus_ordIso2:
blanchet@48975
   268
"|A \<union> B| =o |(A - B) <+> B|"
blanchet@48975
   269
using card_of_Un_Plus_ordIso[of "A - B" B] by auto
blanchet@48975
   270
blanchet@48975
   271
lemma card_of_Times_singl1: "|A| =o |A \<times> {b}|"
blanchet@48975
   272
proof-
blanchet@48975
   273
  have "bij_betw fst (A \<times> {b}) A" unfolding bij_betw_def inj_on_def by force
blanchet@48975
   274
  thus ?thesis using card_of_ordIso ordIso_symmetric by blast
blanchet@48975
   275
qed
blanchet@48975
   276
blanchet@48975
   277
corollary Card_order_Times_singl1:
blanchet@48975
   278
"Card_order r \<Longrightarrow> r =o |(Field r) \<times> {b}|"
blanchet@48975
   279
using card_of_Times_singl1[of _ b] card_of_Field_ordIso ordIso_equivalence by blast
blanchet@48975
   280
blanchet@48975
   281
lemma card_of_Times_singl2: "|A| =o |{b} \<times> A|"
blanchet@48975
   282
proof-
blanchet@48975
   283
  have "bij_betw snd ({b} \<times> A) A" unfolding bij_betw_def inj_on_def by force
blanchet@48975
   284
  thus ?thesis using card_of_ordIso ordIso_symmetric by blast
blanchet@48975
   285
qed
blanchet@48975
   286
blanchet@48975
   287
corollary Card_order_Times_singl2:
blanchet@48975
   288
"Card_order r \<Longrightarrow> r =o |{a} \<times> (Field r)|"
blanchet@48975
   289
using card_of_Times_singl2[of _ a] card_of_Field_ordIso ordIso_equivalence by blast
blanchet@48975
   290
blanchet@48975
   291
lemma card_of_Times_assoc: "|(A \<times> B) \<times> C| =o |A \<times> B \<times> C|"
blanchet@48975
   292
proof -
blanchet@48975
   293
  let ?f = "\<lambda>((a,b),c). (a,(b,c))"
blanchet@48975
   294
  have "A \<times> B \<times> C \<subseteq> ?f ` ((A \<times> B) \<times> C)"
blanchet@48975
   295
  proof
blanchet@48975
   296
    fix x assume "x \<in> A \<times> B \<times> C"
blanchet@48975
   297
    then obtain a b c where *: "a \<in> A" "b \<in> B" "c \<in> C" "x = (a, b, c)" by blast
blanchet@48975
   298
    let ?x = "((a, b), c)"
blanchet@48975
   299
    from * have "?x \<in> (A \<times> B) \<times> C" "x = ?f ?x" by auto
blanchet@48975
   300
    thus "x \<in> ?f ` ((A \<times> B) \<times> C)" by blast
blanchet@48975
   301
  qed
blanchet@48975
   302
  hence "bij_betw ?f ((A \<times> B) \<times> C) (A \<times> B \<times> C)"
blanchet@48975
   303
  unfolding bij_betw_def inj_on_def by auto
blanchet@48975
   304
  thus ?thesis using card_of_ordIso by blast
blanchet@48975
   305
qed
blanchet@48975
   306
blanchet@48975
   307
corollary Card_order_Times3:
blanchet@48975
   308
"Card_order r \<Longrightarrow> |Field r| \<le>o |(Field r) \<times> (Field r)|"
traytel@54578
   309
  by (rule card_of_Times3)
blanchet@48975
   310
blanchet@54475
   311
lemma card_of_Times_cong1[simp]:
blanchet@54475
   312
assumes "|A| =o |B|"
blanchet@54475
   313
shows "|A \<times> C| =o |B \<times> C|"
traytel@54578
   314
using assms by (simp add: ordIso_iff_ordLeq)
blanchet@54475
   315
blanchet@54475
   316
lemma card_of_Times_cong2[simp]:
blanchet@54475
   317
assumes "|A| =o |B|"
blanchet@54475
   318
shows "|C \<times> A| =o |C \<times> B|"
traytel@54578
   319
using assms by (simp add: ordIso_iff_ordLeq)
blanchet@54475
   320
blanchet@48975
   321
lemma card_of_Times_mono[simp]:
blanchet@48975
   322
assumes "|A| \<le>o |B|" and "|C| \<le>o |D|"
blanchet@48975
   323
shows "|A \<times> C| \<le>o |B \<times> D|"
blanchet@48975
   324
using assms card_of_Times_mono1[of A B C] card_of_Times_mono2[of C D B]
blanchet@48975
   325
      ordLeq_transitive[of "|A \<times> C|"] by blast
blanchet@48975
   326
blanchet@48975
   327
corollary ordLeq_Times_mono:
blanchet@48975
   328
assumes "r \<le>o r'" and "p \<le>o p'"
blanchet@48975
   329
shows "|(Field r) \<times> (Field p)| \<le>o |(Field r') \<times> (Field p')|"
blanchet@48975
   330
using assms card_of_mono2[of r r'] card_of_mono2[of p p'] card_of_Times_mono by blast
blanchet@48975
   331
blanchet@48975
   332
corollary ordIso_Times_cong1[simp]:
blanchet@48975
   333
assumes "r =o r'"
blanchet@48975
   334
shows "|(Field r) \<times> C| =o |(Field r') \<times> C|"
blanchet@48975
   335
using assms card_of_cong card_of_Times_cong1 by blast
blanchet@48975
   336
blanchet@54475
   337
corollary ordIso_Times_cong2:
blanchet@54475
   338
assumes "r =o r'"
blanchet@54475
   339
shows "|A \<times> (Field r)| =o |A \<times> (Field r')|"
blanchet@54475
   340
using assms card_of_cong card_of_Times_cong2 by blast
blanchet@54475
   341
blanchet@48975
   342
lemma card_of_Times_cong[simp]:
blanchet@48975
   343
assumes "|A| =o |B|" and "|C| =o |D|"
blanchet@48975
   344
shows "|A \<times> C| =o |B \<times> D|"
blanchet@48975
   345
using assms
blanchet@48975
   346
by (auto simp add: ordIso_iff_ordLeq)
blanchet@48975
   347
blanchet@48975
   348
corollary ordIso_Times_cong:
blanchet@48975
   349
assumes "r =o r'" and "p =o p'"
blanchet@48975
   350
shows "|(Field r) \<times> (Field p)| =o |(Field r') \<times> (Field p')|"
blanchet@48975
   351
using assms card_of_cong[of r r'] card_of_cong[of p p'] card_of_Times_cong by blast
blanchet@48975
   352
blanchet@48975
   353
lemma card_of_Sigma_mono2:
blanchet@48975
   354
assumes "inj_on f (I::'i set)" and "f ` I \<le> (J::'j set)"
blanchet@48975
   355
shows "|SIGMA i : I. (A::'j \<Rightarrow> 'a set) (f i)| \<le>o |SIGMA j : J. A j|"
blanchet@48975
   356
proof-
blanchet@48975
   357
  let ?LEFT = "SIGMA i : I. A (f i)"
blanchet@48975
   358
  let ?RIGHT = "SIGMA j : J. A j"
blanchet@48975
   359
  obtain u where u_def: "u = (\<lambda>(i::'i,a::'a). (f i,a))" by blast
blanchet@48975
   360
  have "inj_on u ?LEFT \<and> u `?LEFT \<le> ?RIGHT"
blanchet@48975
   361
  using assms unfolding u_def inj_on_def by auto
blanchet@48975
   362
  thus ?thesis using card_of_ordLeq by blast
blanchet@48975
   363
qed
blanchet@48975
   364
blanchet@48975
   365
lemma card_of_Sigma_mono:
blanchet@48975
   366
assumes INJ: "inj_on f I" and IM: "f ` I \<le> J" and
blanchet@48975
   367
        LEQ: "\<forall>j \<in> J. |A j| \<le>o |B j|"
blanchet@48975
   368
shows "|SIGMA i : I. A (f i)| \<le>o |SIGMA j : J. B j|"
blanchet@48975
   369
proof-
blanchet@48975
   370
  have "\<forall>i \<in> I. |A(f i)| \<le>o |B(f i)|"
blanchet@48975
   371
  using IM LEQ by blast
blanchet@48975
   372
  hence "|SIGMA i : I. A (f i)| \<le>o |SIGMA i : I. B (f i)|"
blanchet@48975
   373
  using card_of_Sigma_mono1[of I] by metis
blanchet@48975
   374
  moreover have "|SIGMA i : I. B (f i)| \<le>o |SIGMA j : J. B j|"
blanchet@48975
   375
  using INJ IM card_of_Sigma_mono2 by blast
blanchet@48975
   376
  ultimately show ?thesis using ordLeq_transitive by blast
blanchet@48975
   377
qed
blanchet@48975
   378
blanchet@48975
   379
blanchet@48975
   380
lemma ordLeq_Sigma_mono1:
blanchet@48975
   381
assumes "\<forall>i \<in> I. p i \<le>o r i"
blanchet@48975
   382
shows "|SIGMA i : I. Field(p i)| \<le>o |SIGMA i : I. Field(r i)|"
blanchet@48975
   383
using assms by (auto simp add: card_of_Sigma_mono1)
blanchet@48975
   384
blanchet@48975
   385
blanchet@48975
   386
lemma ordLeq_Sigma_mono:
blanchet@48975
   387
assumes "inj_on f I" and "f ` I \<le> J" and
blanchet@48975
   388
        "\<forall>j \<in> J. p j \<le>o r j"
blanchet@48975
   389
shows "|SIGMA i : I. Field(p(f i))| \<le>o |SIGMA j : J. Field(r j)|"
blanchet@48975
   390
using assms card_of_mono2 card_of_Sigma_mono
blanchet@48975
   391
      [of f I J "\<lambda> i. Field(p i)" "\<lambda> j. Field(r j)"] by metis
blanchet@48975
   392
blanchet@48975
   393
blanchet@48975
   394
lemma card_of_Sigma_cong1:
blanchet@48975
   395
assumes "\<forall>i \<in> I. |A i| =o |B i|"
blanchet@48975
   396
shows "|SIGMA i : I. A i| =o |SIGMA i : I. B i|"
blanchet@48975
   397
using assms by (auto simp add: card_of_Sigma_mono1 ordIso_iff_ordLeq)
blanchet@48975
   398
blanchet@48975
   399
blanchet@48975
   400
lemma card_of_Sigma_cong2:
blanchet@48975
   401
assumes "bij_betw f (I::'i set) (J::'j set)"
blanchet@48975
   402
shows "|SIGMA i : I. (A::'j \<Rightarrow> 'a set) (f i)| =o |SIGMA j : J. A j|"
blanchet@48975
   403
proof-
blanchet@48975
   404
  let ?LEFT = "SIGMA i : I. A (f i)"
blanchet@48975
   405
  let ?RIGHT = "SIGMA j : J. A j"
blanchet@48975
   406
  obtain u where u_def: "u = (\<lambda>(i::'i,a::'a). (f i,a))" by blast
blanchet@48975
   407
  have "bij_betw u ?LEFT ?RIGHT"
blanchet@48975
   408
  using assms unfolding u_def bij_betw_def inj_on_def by auto
blanchet@48975
   409
  thus ?thesis using card_of_ordIso by blast
blanchet@48975
   410
qed
blanchet@48975
   411
blanchet@48975
   412
lemma card_of_Sigma_cong:
blanchet@48975
   413
assumes BIJ: "bij_betw f I J" and
blanchet@48975
   414
        ISO: "\<forall>j \<in> J. |A j| =o |B j|"
blanchet@48975
   415
shows "|SIGMA i : I. A (f i)| =o |SIGMA j : J. B j|"
blanchet@48975
   416
proof-
blanchet@48975
   417
  have "\<forall>i \<in> I. |A(f i)| =o |B(f i)|"
blanchet@48975
   418
  using ISO BIJ unfolding bij_betw_def by blast
traytel@54980
   419
  hence "|SIGMA i : I. A (f i)| =o |SIGMA i : I. B (f i)|" by (rule card_of_Sigma_cong1)
blanchet@48975
   420
  moreover have "|SIGMA i : I. B (f i)| =o |SIGMA j : J. B j|"
blanchet@48975
   421
  using BIJ card_of_Sigma_cong2 by blast
blanchet@48975
   422
  ultimately show ?thesis using ordIso_transitive by blast
blanchet@48975
   423
qed
blanchet@48975
   424
blanchet@48975
   425
lemma ordIso_Sigma_cong1:
blanchet@48975
   426
assumes "\<forall>i \<in> I. p i =o r i"
blanchet@48975
   427
shows "|SIGMA i : I. Field(p i)| =o |SIGMA i : I. Field(r i)|"
blanchet@48975
   428
using assms by (auto simp add: card_of_Sigma_cong1)
blanchet@48975
   429
blanchet@48975
   430
lemma ordLeq_Sigma_cong:
blanchet@48975
   431
assumes "bij_betw f I J" and
blanchet@48975
   432
        "\<forall>j \<in> J. p j =o r j"
blanchet@48975
   433
shows "|SIGMA i : I. Field(p(f i))| =o |SIGMA j : J. Field(r j)|"
blanchet@48975
   434
using assms card_of_cong card_of_Sigma_cong
blanchet@48975
   435
      [of f I J "\<lambda> j. Field(p j)" "\<lambda> j. Field(r j)"] by blast
blanchet@48975
   436
blanchet@48975
   437
corollary ordLeq_Sigma_Times:
blanchet@48975
   438
"\<forall>i \<in> I. p i \<le>o r \<Longrightarrow> |SIGMA i : I. Field (p i)| \<le>o |I \<times> (Field r)|"
blanchet@48975
   439
by (auto simp add: card_of_Sigma_Times)
blanchet@48975
   440
blanchet@48975
   441
lemma card_of_UNION_Sigma2:
blanchet@48975
   442
assumes
blanchet@48975
   443
"!! i j. \<lbrakk>{i,j} <= I; i ~= j\<rbrakk> \<Longrightarrow> A i Int A j = {}"
blanchet@48975
   444
shows
blanchet@48975
   445
"|\<Union>i\<in>I. A i| =o |Sigma I A|"
blanchet@48975
   446
proof-
blanchet@48975
   447
  let ?L = "\<Union>i\<in>I. A i"  let ?R = "Sigma I A"
blanchet@48975
   448
  have "|?L| <=o |?R|" using card_of_UNION_Sigma .
blanchet@48975
   449
  moreover have "|?R| <=o |?L|"
blanchet@48975
   450
  proof-
blanchet@48975
   451
    have "inj_on snd ?R"
blanchet@48975
   452
    unfolding inj_on_def using assms by auto
blanchet@48975
   453
    moreover have "snd ` ?R <= ?L" by auto
blanchet@48975
   454
    ultimately show ?thesis using card_of_ordLeq by blast
blanchet@48975
   455
  qed
blanchet@48975
   456
  ultimately show ?thesis by(simp add: ordIso_iff_ordLeq)
blanchet@48975
   457
qed
blanchet@48975
   458
blanchet@48975
   459
corollary Plus_into_Times:
blanchet@48975
   460
assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and
blanchet@48975
   461
        B2: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B"
blanchet@48975
   462
shows "\<exists>f. inj_on f (A <+> B) \<and> f ` (A <+> B) \<le> A \<times> B"
blanchet@48975
   463
using assms by (auto simp add: card_of_Plus_Times card_of_ordLeq)
blanchet@48975
   464
blanchet@48975
   465
corollary Plus_into_Times_types:
blanchet@48975
   466
assumes A2: "(a1::'a) \<noteq> a2" and  B2: "(b1::'b) \<noteq> b2"
blanchet@48975
   467
shows "\<exists>(f::'a + 'b \<Rightarrow> 'a * 'b). inj f"
blanchet@48975
   468
using assms Plus_into_Times[of a1 a2 UNIV b1 b2 UNIV]
blanchet@48975
   469
by auto
blanchet@48975
   470
blanchet@48975
   471
corollary Times_same_infinite_bij_betw:
traytel@54578
   472
assumes "\<not>finite A"
blanchet@48975
   473
shows "\<exists>f. bij_betw f (A \<times> A) A"
blanchet@48975
   474
using assms by (auto simp add: card_of_ordIso)
blanchet@48975
   475
blanchet@48975
   476
corollary Times_same_infinite_bij_betw_types:
traytel@54578
   477
assumes INF: "\<not>finite(UNIV::'a set)"
blanchet@48975
   478
shows "\<exists>(f::('a * 'a) => 'a). bij f"
blanchet@48975
   479
using assms Times_same_infinite_bij_betw[of "UNIV::'a set"]
blanchet@48975
   480
by auto
blanchet@48975
   481
blanchet@48975
   482
corollary Times_infinite_bij_betw:
traytel@54578
   483
assumes INF: "\<not>finite A" and NE: "B \<noteq> {}" and INJ: "inj_on g B \<and> g ` B \<le> A"
blanchet@48975
   484
shows "(\<exists>f. bij_betw f (A \<times> B) A) \<and> (\<exists>h. bij_betw h (B \<times> A) A)"
blanchet@48975
   485
proof-
blanchet@48975
   486
  have "|B| \<le>o |A|" using INJ card_of_ordLeq by blast
blanchet@48975
   487
  thus ?thesis using INF NE
blanchet@48975
   488
  by (auto simp add: card_of_ordIso card_of_Times_infinite)
blanchet@48975
   489
qed
blanchet@48975
   490
blanchet@48975
   491
corollary Times_infinite_bij_betw_types:
traytel@54578
   492
assumes INF: "\<not>finite(UNIV::'a set)" and
blanchet@48975
   493
        BIJ: "inj(g::'b \<Rightarrow> 'a)"
blanchet@48975
   494
shows "(\<exists>(f::('b * 'a) => 'a). bij f) \<and> (\<exists>(h::('a * 'b) => 'a). bij h)"
blanchet@48975
   495
using assms Times_infinite_bij_betw[of "UNIV::'a set" "UNIV::'b set" g]
blanchet@48975
   496
by auto
blanchet@48975
   497
blanchet@48975
   498
lemma card_of_Times_ordLeq_infinite:
traytel@54578
   499
"\<lbrakk>\<not>finite C; |A| \<le>o |C|; |B| \<le>o |C|\<rbrakk>
blanchet@48975
   500
 \<Longrightarrow> |A <*> B| \<le>o |C|"
blanchet@48975
   501
by(simp add: card_of_Sigma_ordLeq_infinite)
blanchet@48975
   502
blanchet@48975
   503
corollary Plus_infinite_bij_betw:
traytel@54578
   504
assumes INF: "\<not>finite A" and INJ: "inj_on g B \<and> g ` B \<le> A"
blanchet@48975
   505
shows "(\<exists>f. bij_betw f (A <+> B) A) \<and> (\<exists>h. bij_betw h (B <+> A) A)"
blanchet@48975
   506
proof-
blanchet@48975
   507
  have "|B| \<le>o |A|" using INJ card_of_ordLeq by blast
blanchet@48975
   508
  thus ?thesis using INF
blanchet@48975
   509
  by (auto simp add: card_of_ordIso)
blanchet@48975
   510
qed
blanchet@48975
   511
blanchet@48975
   512
corollary Plus_infinite_bij_betw_types:
traytel@54578
   513
assumes INF: "\<not>finite(UNIV::'a set)" and
blanchet@48975
   514
        BIJ: "inj(g::'b \<Rightarrow> 'a)"
blanchet@48975
   515
shows "(\<exists>(f::('b + 'a) => 'a). bij f) \<and> (\<exists>(h::('a + 'b) => 'a). bij h)"
blanchet@48975
   516
using assms Plus_infinite_bij_betw[of "UNIV::'a set" g "UNIV::'b set"]
blanchet@48975
   517
by auto
blanchet@48975
   518
blanchet@54475
   519
lemma card_of_Un_infinite:
traytel@54578
   520
assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
blanchet@54475
   521
shows "|A \<union> B| =o |A| \<and> |B \<union> A| =o |A|"
blanchet@54475
   522
proof-
blanchet@54475
   523
  have "|A \<union> B| \<le>o |A <+> B|" by (rule card_of_Un_Plus_ordLeq)
blanchet@54475
   524
  moreover have "|A <+> B| =o |A|"
blanchet@54475
   525
  using assms by (metis card_of_Plus_infinite)
blanchet@54475
   526
  ultimately have "|A \<union> B| \<le>o |A|" using ordLeq_ordIso_trans by blast
blanchet@54475
   527
  hence "|A \<union> B| =o |A|" using card_of_Un1 ordIso_iff_ordLeq by blast
blanchet@54475
   528
  thus ?thesis using Un_commute[of B A] by auto
blanchet@54475
   529
qed
blanchet@54475
   530
blanchet@48975
   531
lemma card_of_Un_infinite_simps[simp]:
traytel@54578
   532
"\<lbrakk>\<not>finite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |A \<union> B| =o |A|"
traytel@54578
   533
"\<lbrakk>\<not>finite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |B \<union> A| =o |A|"
blanchet@48975
   534
using card_of_Un_infinite by auto
blanchet@48975
   535
blanchet@54475
   536
lemma card_of_Un_diff_infinite:
traytel@54578
   537
assumes INF: "\<not>finite A" and LESS: "|B| <o |A|"
blanchet@54475
   538
shows "|A - B| =o |A|"
blanchet@54475
   539
proof-
blanchet@54475
   540
  obtain C where C_def: "C = A - B" by blast
blanchet@54475
   541
  have "|A \<union> B| =o |A|"
blanchet@54475
   542
  using assms ordLeq_iff_ordLess_or_ordIso card_of_Un_infinite by blast
blanchet@54475
   543
  moreover have "C \<union> B = A \<union> B" unfolding C_def by auto
blanchet@54475
   544
  ultimately have 1: "|C \<union> B| =o |A|" by auto
blanchet@54475
   545
  (*  *)
blanchet@54475
   546
  {assume *: "|C| \<le>o |B|"
blanchet@54475
   547
   moreover
blanchet@54475
   548
   {assume **: "finite B"
blanchet@54475
   549
    hence "finite C"
blanchet@54475
   550
    using card_of_ordLeq_finite * by blast
blanchet@54475
   551
    hence False using ** INF card_of_ordIso_finite 1 by blast
blanchet@54475
   552
   }
traytel@54578
   553
   hence "\<not>finite B" by auto
blanchet@54475
   554
   ultimately have False
blanchet@54475
   555
   using card_of_Un_infinite 1 ordIso_equivalence(1,3) LESS not_ordLess_ordIso by metis
blanchet@54475
   556
  }
blanchet@54475
   557
  hence 2: "|B| \<le>o |C|" using card_of_Well_order ordLeq_total by blast
blanchet@54475
   558
  {assume *: "finite C"
blanchet@54475
   559
    hence "finite B" using card_of_ordLeq_finite 2 by blast
blanchet@54475
   560
    hence False using * INF card_of_ordIso_finite 1 by blast
blanchet@54475
   561
  }
traytel@54578
   562
  hence "\<not>finite C" by auto
blanchet@54475
   563
  hence "|C| =o |A|"
blanchet@54475
   564
  using  card_of_Un_infinite 1 2 ordIso_equivalence(1,3) by metis
blanchet@54475
   565
  thus ?thesis unfolding C_def .
blanchet@54475
   566
qed
blanchet@54475
   567
blanchet@48975
   568
corollary Card_order_Un_infinite:
traytel@54578
   569
assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
blanchet@48975
   570
        LEQ: "p \<le>o r"
blanchet@48975
   571
shows "| (Field r) \<union> (Field p) | =o r \<and> | (Field p) \<union> (Field r) | =o r"
blanchet@48975
   572
proof-
blanchet@48975
   573
  have "| Field r \<union> Field p | =o | Field r | \<and>
blanchet@48975
   574
        | Field p \<union> Field r | =o | Field r |"
blanchet@48975
   575
  using assms by (auto simp add: card_of_Un_infinite)
blanchet@48975
   576
  thus ?thesis
blanchet@48975
   577
  using assms card_of_Field_ordIso[of r]
blanchet@48975
   578
        ordIso_transitive[of "|Field r \<union> Field p|"]
blanchet@48975
   579
        ordIso_transitive[of _ "|Field r|"] by blast
blanchet@48975
   580
qed
blanchet@48975
   581
blanchet@48975
   582
corollary subset_ordLeq_diff_infinite:
traytel@54578
   583
assumes INF: "\<not>finite B" and SUB: "A \<le> B" and LESS: "|A| <o |B|"
traytel@54578
   584
shows "\<not>finite (B - A)"
blanchet@48975
   585
using assms card_of_Un_diff_infinite card_of_ordIso_finite by blast
blanchet@48975
   586
blanchet@48975
   587
lemma card_of_Times_ordLess_infinite[simp]:
traytel@54578
   588
assumes INF: "\<not>finite C" and
blanchet@48975
   589
        LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
blanchet@48975
   590
shows "|A \<times> B| <o |C|"
blanchet@48975
   591
proof(cases "A = {} \<or> B = {}")
blanchet@48975
   592
  assume Case1: "A = {} \<or> B = {}"
blanchet@48975
   593
  hence "A \<times> B = {}" by blast
blanchet@48975
   594
  moreover have "C \<noteq> {}" using
blanchet@48975
   595
  LESS1 card_of_empty5 by blast
blanchet@48975
   596
  ultimately show ?thesis by(auto simp add:  card_of_empty4)
blanchet@48975
   597
next
blanchet@48975
   598
  assume Case2: "\<not>(A = {} \<or> B = {})"
blanchet@48975
   599
  {assume *: "|C| \<le>o |A \<times> B|"
traytel@54578
   600
   hence "\<not>finite (A \<times> B)" using INF card_of_ordLeq_finite by blast
traytel@54578
   601
   hence 1: "\<not>finite A \<or> \<not>finite B" using finite_cartesian_product by blast
blanchet@48975
   602
   {assume Case21: "|A| \<le>o |B|"
traytel@54578
   603
    hence "\<not>finite B" using 1 card_of_ordLeq_finite by blast
blanchet@48975
   604
    hence "|A \<times> B| =o |B|" using Case2 Case21
blanchet@48975
   605
    by (auto simp add: card_of_Times_infinite)
blanchet@48975
   606
    hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
blanchet@48975
   607
   }
blanchet@48975
   608
   moreover
blanchet@48975
   609
   {assume Case22: "|B| \<le>o |A|"
traytel@54578
   610
    hence "\<not>finite A" using 1 card_of_ordLeq_finite by blast
blanchet@48975
   611
    hence "|A \<times> B| =o |A|" using Case2 Case22
blanchet@48975
   612
    by (auto simp add: card_of_Times_infinite)
blanchet@48975
   613
    hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
blanchet@48975
   614
   }
blanchet@48975
   615
   ultimately have False using ordLeq_total card_of_Well_order[of A]
blanchet@48975
   616
   card_of_Well_order[of B] by blast
blanchet@48975
   617
  }
blanchet@48975
   618
  thus ?thesis using ordLess_or_ordLeq[of "|A \<times> B|" "|C|"]
blanchet@48975
   619
  card_of_Well_order[of "A \<times> B"] card_of_Well_order[of "C"] by auto
blanchet@48975
   620
qed
blanchet@48975
   621
blanchet@48975
   622
lemma card_of_Times_ordLess_infinite_Field[simp]:
traytel@54578
   623
assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
blanchet@48975
   624
        LESS1: "|A| <o r" and LESS2: "|B| <o r"
blanchet@48975
   625
shows "|A \<times> B| <o r"
blanchet@48975
   626
proof-
blanchet@48975
   627
  let ?C  = "Field r"
blanchet@48975
   628
  have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso
blanchet@48975
   629
  ordIso_symmetric by blast
blanchet@48975
   630
  hence "|A| <o |?C|"  "|B| <o |?C|"
blanchet@48975
   631
  using LESS1 LESS2 ordLess_ordIso_trans by blast+
blanchet@48975
   632
  hence  "|A <*> B| <o |?C|" using INF
blanchet@48975
   633
  card_of_Times_ordLess_infinite by blast
blanchet@48975
   634
  thus ?thesis using 1 ordLess_ordIso_trans by blast
blanchet@48975
   635
qed
blanchet@48975
   636
blanchet@48975
   637
lemma card_of_Un_ordLess_infinite[simp]:
traytel@54578
   638
assumes INF: "\<not>finite C" and
blanchet@48975
   639
        LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
blanchet@48975
   640
shows "|A \<union> B| <o |C|"
blanchet@48975
   641
using assms card_of_Plus_ordLess_infinite card_of_Un_Plus_ordLeq
blanchet@48975
   642
      ordLeq_ordLess_trans by blast
blanchet@48975
   643
blanchet@48975
   644
lemma card_of_Un_ordLess_infinite_Field[simp]:
traytel@54578
   645
assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
blanchet@48975
   646
        LESS1: "|A| <o r" and LESS2: "|B| <o r"
blanchet@48975
   647
shows "|A Un B| <o r"
blanchet@48975
   648
proof-
blanchet@48975
   649
  let ?C  = "Field r"
blanchet@48975
   650
  have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso
blanchet@48975
   651
  ordIso_symmetric by blast
blanchet@48975
   652
  hence "|A| <o |?C|"  "|B| <o |?C|"
blanchet@48975
   653
  using LESS1 LESS2 ordLess_ordIso_trans by blast+
blanchet@48975
   654
  hence  "|A Un B| <o |?C|" using INF
blanchet@48975
   655
  card_of_Un_ordLess_infinite by blast
blanchet@48975
   656
  thus ?thesis using 1 ordLess_ordIso_trans by blast
blanchet@48975
   657
qed
blanchet@48975
   658
blanchet@54475
   659
blanchet@54475
   660
subsection {* Cardinals versus set operations involving infinite sets *}
blanchet@54475
   661
blanchet@54475
   662
lemma finite_iff_cardOf_nat:
blanchet@54475
   663
"finite A = ( |A| <o |UNIV :: nat set| )"
blanchet@54475
   664
using infinite_iff_card_of_nat[of A]
blanchet@54475
   665
not_ordLeq_iff_ordLess[of "|A|" "|UNIV :: nat set|"]
traytel@54578
   666
by fastforce
blanchet@54475
   667
blanchet@54475
   668
lemma finite_ordLess_infinite2[simp]:
traytel@54578
   669
assumes "finite A" and "\<not>finite B"
blanchet@54475
   670
shows "|A| <o |B|"
blanchet@54475
   671
using assms
blanchet@54475
   672
finite_ordLess_infinite[of "|A|" "|B|"]
blanchet@54475
   673
card_of_Well_order[of A] card_of_Well_order[of B]
blanchet@54475
   674
Field_card_of[of A] Field_card_of[of B] by auto
blanchet@54475
   675
blanchet@54475
   676
lemma infinite_card_of_insert:
traytel@54578
   677
assumes "\<not>finite A"
blanchet@54475
   678
shows "|insert a A| =o |A|"
blanchet@54475
   679
proof-
blanchet@54475
   680
  have iA: "insert a A = A \<union> {a}" by simp
blanchet@54475
   681
  show ?thesis
blanchet@54475
   682
  using infinite_imp_bij_betw2[OF assms] unfolding iA
blanchet@54475
   683
  by (metis bij_betw_inv card_of_ordIso)
blanchet@54475
   684
qed
blanchet@54475
   685
blanchet@48975
   686
lemma card_of_Un_singl_ordLess_infinite1:
traytel@54578
   687
assumes "\<not>finite B" and "|A| <o |B|"
blanchet@48975
   688
shows "|{a} Un A| <o |B|"
blanchet@48975
   689
proof-
blanchet@48975
   690
  have "|{a}| <o |B|" using assms by auto
traytel@51764
   691
  thus ?thesis using assms card_of_Un_ordLess_infinite[of B] by blast
blanchet@48975
   692
qed
blanchet@48975
   693
blanchet@48975
   694
lemma card_of_Un_singl_ordLess_infinite:
traytel@54578
   695
assumes "\<not>finite B"
blanchet@48975
   696
shows "( |A| <o |B| ) = ( |{a} Un A| <o |B| )"
blanchet@48975
   697
using assms card_of_Un_singl_ordLess_infinite1[of B A]
blanchet@48975
   698
proof(auto)
blanchet@48975
   699
  assume "|insert a A| <o |B|"
traytel@51764
   700
  moreover have "|A| <=o |insert a A|" using card_of_mono1[of A "insert a A"] by blast
blanchet@48975
   701
  ultimately show "|A| <o |B|" using ordLeq_ordLess_trans by blast
blanchet@48975
   702
qed
blanchet@48975
   703
blanchet@48975
   704
blanchet@54475
   705
subsection {* Cardinals versus lists *}
blanchet@54475
   706
blanchet@54475
   707
text{* The next is an auxiliary operator, which shall be used for inductive
blanchet@54475
   708
proofs of facts concerning the cardinality of @{text "List"} : *}
blanchet@54475
   709
blanchet@54475
   710
definition nlists :: "'a set \<Rightarrow> nat \<Rightarrow> 'a list set"
blanchet@54475
   711
where "nlists A n \<equiv> {l. set l \<le> A \<and> length l = n}"
blanchet@54475
   712
blanchet@54475
   713
lemma lists_def2: "lists A = {l. set l \<le> A}"
blanchet@54475
   714
using in_listsI by blast
blanchet@54475
   715
blanchet@54475
   716
lemma lists_UNION_nlists: "lists A = (\<Union> n. nlists A n)"
blanchet@54475
   717
unfolding lists_def2 nlists_def by blast
blanchet@54475
   718
blanchet@54475
   719
lemma card_of_lists: "|A| \<le>o |lists A|"
blanchet@54475
   720
proof-
blanchet@54475
   721
  let ?h = "\<lambda> a. [a]"
blanchet@54475
   722
  have "inj_on ?h A \<and> ?h ` A \<le> lists A"
blanchet@54475
   723
  unfolding inj_on_def lists_def2 by auto
blanchet@54475
   724
  thus ?thesis by (metis card_of_ordLeq)
blanchet@54475
   725
qed
blanchet@54475
   726
blanchet@54475
   727
lemma nlists_0: "nlists A 0 = {[]}"
blanchet@54475
   728
unfolding nlists_def by auto
blanchet@54475
   729
blanchet@54475
   730
lemma nlists_not_empty:
blanchet@54475
   731
assumes "A \<noteq> {}"
blanchet@54475
   732
shows "nlists A n \<noteq> {}"
blanchet@54475
   733
proof(induct n, simp add: nlists_0)
blanchet@54475
   734
  fix n assume "nlists A n \<noteq> {}"
blanchet@54475
   735
  then obtain a and l where "a \<in> A \<and> l \<in> nlists A n" using assms by auto
blanchet@54475
   736
  hence "a # l \<in> nlists A (Suc n)" unfolding nlists_def by auto
blanchet@54475
   737
  thus "nlists A (Suc n) \<noteq> {}" by auto
blanchet@54475
   738
qed
blanchet@54475
   739
blanchet@54475
   740
lemma Nil_in_lists: "[] \<in> lists A"
blanchet@54475
   741
unfolding lists_def2 by auto
blanchet@54475
   742
blanchet@54475
   743
lemma lists_not_empty: "lists A \<noteq> {}"
blanchet@54475
   744
using Nil_in_lists by blast
blanchet@54475
   745
blanchet@54475
   746
lemma card_of_nlists_Succ: "|nlists A (Suc n)| =o |A \<times> (nlists A n)|"
blanchet@54475
   747
proof-
blanchet@54475
   748
  let ?B = "A \<times> (nlists A n)"   let ?h = "\<lambda>(a,l). a # l"
blanchet@54475
   749
  have "inj_on ?h ?B \<and> ?h ` ?B \<le> nlists A (Suc n)"
blanchet@54475
   750
  unfolding inj_on_def nlists_def by auto
blanchet@54475
   751
  moreover have "nlists A (Suc n) \<le> ?h ` ?B"
blanchet@54475
   752
  proof(auto)
blanchet@54475
   753
    fix l assume "l \<in> nlists A (Suc n)"
blanchet@54475
   754
    hence 1: "length l = Suc n \<and> set l \<le> A" unfolding nlists_def by auto
blanchet@54475
   755
    then obtain a and l' where 2: "l = a # l'" by (auto simp: length_Suc_conv)
blanchet@54475
   756
    hence "a \<in> A \<and> set l' \<le> A \<and> length l' = n" using 1 by auto
blanchet@54475
   757
    thus "l \<in> ?h ` ?B"  using 2 unfolding nlists_def by auto
blanchet@54475
   758
  qed
blanchet@54475
   759
  ultimately have "bij_betw ?h ?B (nlists A (Suc n))"
blanchet@54475
   760
  unfolding bij_betw_def by auto
blanchet@54475
   761
  thus ?thesis using card_of_ordIso ordIso_symmetric by blast
blanchet@54475
   762
qed
blanchet@54475
   763
blanchet@54475
   764
lemma card_of_nlists_infinite:
traytel@54578
   765
assumes "\<not>finite A"
blanchet@54475
   766
shows "|nlists A n| \<le>o |A|"
blanchet@54475
   767
proof(induct n)
blanchet@54475
   768
  have "A \<noteq> {}" using assms by auto
traytel@54578
   769
  thus "|nlists A 0| \<le>o |A|" by (simp add: nlists_0)
blanchet@54475
   770
next
blanchet@54475
   771
  fix n assume IH: "|nlists A n| \<le>o |A|"
blanchet@54475
   772
  have "|nlists A (Suc n)| =o |A \<times> (nlists A n)|"
blanchet@54475
   773
  using card_of_nlists_Succ by blast
blanchet@54475
   774
  moreover
blanchet@54475
   775
  {have "nlists A n \<noteq> {}" using assms nlists_not_empty[of A] by blast
blanchet@54475
   776
   hence "|A \<times> (nlists A n)| =o |A|"
blanchet@54475
   777
   using assms IH by (auto simp add: card_of_Times_infinite)
blanchet@54475
   778
  }
blanchet@54475
   779
  ultimately show "|nlists A (Suc n)| \<le>o |A|"
blanchet@54475
   780
  using ordIso_transitive ordIso_iff_ordLeq by blast
blanchet@54475
   781
qed
blanchet@48975
   782
blanchet@48975
   783
lemma Card_order_lists: "Card_order r \<Longrightarrow> r \<le>o |lists(Field r) |"
blanchet@48975
   784
using card_of_lists card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
blanchet@48975
   785
blanchet@48975
   786
lemma Union_set_lists:
blanchet@48975
   787
"Union(set ` (lists A)) = A"
blanchet@48975
   788
unfolding lists_def2 proof(auto)
blanchet@48975
   789
  fix a assume "a \<in> A"
blanchet@48975
   790
  hence "set [a] \<le> A \<and> a \<in> set [a]" by auto
blanchet@48975
   791
  thus "\<exists>l. set l \<le> A \<and> a \<in> set l" by blast
blanchet@48975
   792
qed
blanchet@48975
   793
blanchet@48975
   794
lemma inj_on_map_lists:
blanchet@48975
   795
assumes "inj_on f A"
blanchet@48975
   796
shows "inj_on (map f) (lists A)"
blanchet@48975
   797
using assms Union_set_lists[of A] inj_on_mapI[of f "lists A"] by auto
blanchet@48975
   798
blanchet@48975
   799
lemma map_lists_mono:
blanchet@48975
   800
assumes "f ` A \<le> B"
blanchet@48975
   801
shows "(map f) ` (lists A) \<le> lists B"
blanchet@48975
   802
using assms unfolding lists_def2 by (auto, blast) (* lethal combination of methods :)  *)
blanchet@48975
   803
blanchet@48975
   804
lemma map_lists_surjective:
blanchet@48975
   805
assumes "f ` A = B"
blanchet@48975
   806
shows "(map f) ` (lists A) = lists B"
blanchet@48975
   807
using assms unfolding lists_def2
blanchet@48975
   808
proof (auto, blast)
blanchet@48975
   809
  fix l' assume *: "set l' \<le> f ` A"
blanchet@48975
   810
  have "set l' \<le> f ` A \<longrightarrow> l' \<in> map f ` {l. set l \<le> A}"
blanchet@48975
   811
  proof(induct l', auto)
blanchet@48975
   812
    fix l a
blanchet@48975
   813
    assume "a \<in> A" and "set l \<le> A" and
blanchet@48975
   814
           IH: "f ` (set l) \<le> f ` A"
blanchet@48975
   815
    hence "set (a # l) \<le> A" by auto
blanchet@48975
   816
    hence "map f (a # l) \<in> map f ` {l. set l \<le> A}" by blast
blanchet@48975
   817
    thus "f a # map f l \<in> map f ` {l. set l \<le> A}" by auto
blanchet@48975
   818
  qed
blanchet@48975
   819
  thus "l' \<in> map f ` {l. set l \<le> A}" using * by auto
blanchet@48975
   820
qed
blanchet@48975
   821
blanchet@48975
   822
lemma bij_betw_map_lists:
blanchet@48975
   823
assumes "bij_betw f A B"
blanchet@48975
   824
shows "bij_betw (map f) (lists A) (lists B)"
blanchet@48975
   825
using assms unfolding bij_betw_def
blanchet@48975
   826
by(auto simp add: inj_on_map_lists map_lists_surjective)
blanchet@48975
   827
blanchet@48975
   828
lemma card_of_lists_mono[simp]:
blanchet@48975
   829
assumes "|A| \<le>o |B|"
blanchet@48975
   830
shows "|lists A| \<le>o |lists B|"
blanchet@48975
   831
proof-
blanchet@48975
   832
  obtain f where "inj_on f A \<and> f ` A \<le> B"
blanchet@48975
   833
  using assms card_of_ordLeq[of A B] by auto
blanchet@48975
   834
  hence "inj_on (map f) (lists A) \<and> (map f) ` (lists A) \<le> (lists B)"
blanchet@48975
   835
  by (auto simp add: inj_on_map_lists map_lists_mono)
blanchet@48975
   836
  thus ?thesis using card_of_ordLeq[of "lists A"] by metis
blanchet@48975
   837
qed
blanchet@48975
   838
blanchet@48975
   839
lemma ordIso_lists_mono:
blanchet@48975
   840
assumes "r \<le>o r'"
blanchet@48975
   841
shows "|lists(Field r)| \<le>o |lists(Field r')|"
blanchet@48975
   842
using assms card_of_mono2 card_of_lists_mono by blast
blanchet@48975
   843
blanchet@48975
   844
lemma card_of_lists_cong[simp]:
blanchet@48975
   845
assumes "|A| =o |B|"
blanchet@48975
   846
shows "|lists A| =o |lists B|"
blanchet@48975
   847
proof-
blanchet@48975
   848
  obtain f where "bij_betw f A B"
blanchet@48975
   849
  using assms card_of_ordIso[of A B] by auto
blanchet@48975
   850
  hence "bij_betw (map f) (lists A) (lists B)"
blanchet@48975
   851
  by (auto simp add: bij_betw_map_lists)
blanchet@48975
   852
  thus ?thesis using card_of_ordIso[of "lists A"] by auto
blanchet@48975
   853
qed
blanchet@48975
   854
blanchet@54475
   855
lemma card_of_lists_infinite[simp]:
traytel@54578
   856
assumes "\<not>finite A"
blanchet@54475
   857
shows "|lists A| =o |A|"
blanchet@54475
   858
proof-
traytel@54578
   859
  have "|lists A| \<le>o |A|" unfolding lists_UNION_nlists
traytel@54578
   860
  by (rule card_of_UNION_ordLeq_infinite[OF assms _ ballI[OF card_of_nlists_infinite[OF assms]]])
traytel@54578
   861
    (metis infinite_iff_card_of_nat assms)
blanchet@54475
   862
  thus ?thesis using card_of_lists ordIso_iff_ordLeq by blast
blanchet@54475
   863
qed
blanchet@54475
   864
blanchet@54475
   865
lemma Card_order_lists_infinite:
traytel@54578
   866
assumes "Card_order r" and "\<not>finite(Field r)"
blanchet@54475
   867
shows "|lists(Field r)| =o r"
blanchet@54475
   868
using assms card_of_lists_infinite card_of_Field_ordIso ordIso_transitive by blast
blanchet@54475
   869
blanchet@48975
   870
lemma ordIso_lists_cong:
blanchet@48975
   871
assumes "r =o r'"
blanchet@48975
   872
shows "|lists(Field r)| =o |lists(Field r')|"
blanchet@48975
   873
using assms card_of_cong card_of_lists_cong by blast
blanchet@48975
   874
blanchet@48975
   875
corollary lists_infinite_bij_betw:
traytel@54578
   876
assumes "\<not>finite A"
blanchet@48975
   877
shows "\<exists>f. bij_betw f (lists A) A"
blanchet@48975
   878
using assms card_of_lists_infinite card_of_ordIso by blast
blanchet@48975
   879
blanchet@48975
   880
corollary lists_infinite_bij_betw_types:
traytel@54578
   881
assumes "\<not>finite(UNIV :: 'a set)"
blanchet@48975
   882
shows "\<exists>(f::'a list \<Rightarrow> 'a). bij f"
blanchet@48975
   883
using assms assms lists_infinite_bij_betw[of "UNIV::'a set"]
blanchet@48975
   884
using lists_UNIV by auto
blanchet@48975
   885
blanchet@48975
   886
blanchet@48975
   887
subsection {* Cardinals versus the set-of-finite-sets operator  *}
blanchet@48975
   888
blanchet@48975
   889
definition Fpow :: "'a set \<Rightarrow> 'a set set"
blanchet@48975
   890
where "Fpow A \<equiv> {X. X \<le> A \<and> finite X}"
blanchet@48975
   891
blanchet@48975
   892
lemma Fpow_mono: "A \<le> B \<Longrightarrow> Fpow A \<le> Fpow B"
blanchet@48975
   893
unfolding Fpow_def by auto
blanchet@48975
   894
blanchet@48975
   895
lemma empty_in_Fpow: "{} \<in> Fpow A"
blanchet@48975
   896
unfolding Fpow_def by auto
blanchet@48975
   897
blanchet@48975
   898
lemma Fpow_not_empty: "Fpow A \<noteq> {}"
blanchet@48975
   899
using empty_in_Fpow by blast
blanchet@48975
   900
blanchet@48975
   901
lemma Fpow_subset_Pow: "Fpow A \<le> Pow A"
blanchet@48975
   902
unfolding Fpow_def by auto
blanchet@48975
   903
blanchet@48975
   904
lemma card_of_Fpow[simp]: "|A| \<le>o |Fpow A|"
blanchet@48975
   905
proof-
blanchet@48975
   906
  let ?h = "\<lambda> a. {a}"
blanchet@48975
   907
  have "inj_on ?h A \<and> ?h ` A \<le> Fpow A"
blanchet@48975
   908
  unfolding inj_on_def Fpow_def by auto
blanchet@48975
   909
  thus ?thesis using card_of_ordLeq by metis
blanchet@48975
   910
qed
blanchet@48975
   911
blanchet@48975
   912
lemma Card_order_Fpow: "Card_order r \<Longrightarrow> r \<le>o |Fpow(Field r) |"
blanchet@48975
   913
using card_of_Fpow card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
blanchet@48975
   914
blanchet@48975
   915
lemma Fpow_Pow_finite: "Fpow A = Pow A Int {A. finite A}"
blanchet@48975
   916
unfolding Fpow_def Pow_def by blast
blanchet@48975
   917
blanchet@48975
   918
lemma inj_on_image_Fpow:
blanchet@48975
   919
assumes "inj_on f A"
blanchet@48975
   920
shows "inj_on (image f) (Fpow A)"
blanchet@48975
   921
using assms Fpow_subset_Pow[of A] subset_inj_on[of "image f" "Pow A"]
blanchet@48975
   922
      inj_on_image_Pow by blast
blanchet@48975
   923
blanchet@48975
   924
lemma image_Fpow_mono:
blanchet@48975
   925
assumes "f ` A \<le> B"
blanchet@48975
   926
shows "(image f) ` (Fpow A) \<le> Fpow B"
blanchet@48975
   927
using assms by(unfold Fpow_def, auto)
blanchet@48975
   928
blanchet@48975
   929
lemma image_Fpow_surjective:
blanchet@48975
   930
assumes "f ` A = B"
blanchet@48975
   931
shows "(image f) ` (Fpow A) = Fpow B"
blanchet@48975
   932
using assms proof(unfold Fpow_def, auto)
blanchet@48975
   933
  fix Y assume *: "Y \<le> f ` A" and **: "finite Y"
blanchet@48975
   934
  hence "\<forall>b \<in> Y. \<exists>a. a \<in> A \<and> f a = b" by auto
blanchet@48975
   935
  with bchoice[of Y "\<lambda>b a. a \<in> A \<and> f a = b"]
blanchet@48975
   936
  obtain g where 1: "\<forall>b \<in> Y. g b \<in> A \<and> f(g b) = b" by blast
blanchet@48975
   937
  obtain X where X_def: "X = g ` Y" by blast
blanchet@48975
   938
  have "f ` X = Y \<and> X \<le> A \<and> finite X"
blanchet@48975
   939
  by(unfold X_def, force simp add: ** 1)
blanchet@48975
   940
  thus "Y \<in> (image f) ` {X. X \<le> A \<and> finite X}" by auto
blanchet@48975
   941
qed
blanchet@48975
   942
blanchet@48975
   943
lemma bij_betw_image_Fpow:
blanchet@48975
   944
assumes "bij_betw f A B"
blanchet@48975
   945
shows "bij_betw (image f) (Fpow A) (Fpow B)"
blanchet@48975
   946
using assms unfolding bij_betw_def
blanchet@48975
   947
by (auto simp add: inj_on_image_Fpow image_Fpow_surjective)
blanchet@48975
   948
blanchet@48975
   949
lemma card_of_Fpow_mono[simp]:
blanchet@48975
   950
assumes "|A| \<le>o |B|"
blanchet@48975
   951
shows "|Fpow A| \<le>o |Fpow B|"
blanchet@48975
   952
proof-
blanchet@48975
   953
  obtain f where "inj_on f A \<and> f ` A \<le> B"
blanchet@48975
   954
  using assms card_of_ordLeq[of A B] by auto
blanchet@48975
   955
  hence "inj_on (image f) (Fpow A) \<and> (image f) ` (Fpow A) \<le> (Fpow B)"
blanchet@48975
   956
  by (auto simp add: inj_on_image_Fpow image_Fpow_mono)
blanchet@48975
   957
  thus ?thesis using card_of_ordLeq[of "Fpow A"] by auto
blanchet@48975
   958
qed
blanchet@48975
   959
blanchet@48975
   960
lemma ordIso_Fpow_mono:
blanchet@48975
   961
assumes "r \<le>o r'"
blanchet@48975
   962
shows "|Fpow(Field r)| \<le>o |Fpow(Field r')|"
blanchet@48975
   963
using assms card_of_mono2 card_of_Fpow_mono by blast
blanchet@48975
   964
blanchet@48975
   965
lemma card_of_Fpow_cong[simp]:
blanchet@48975
   966
assumes "|A| =o |B|"
blanchet@48975
   967
shows "|Fpow A| =o |Fpow B|"
blanchet@48975
   968
proof-
blanchet@48975
   969
  obtain f where "bij_betw f A B"
blanchet@48975
   970
  using assms card_of_ordIso[of A B] by auto
blanchet@48975
   971
  hence "bij_betw (image f) (Fpow A) (Fpow B)"
blanchet@48975
   972
  by (auto simp add: bij_betw_image_Fpow)
blanchet@48975
   973
  thus ?thesis using card_of_ordIso[of "Fpow A"] by auto
blanchet@48975
   974
qed
blanchet@48975
   975
blanchet@48975
   976
lemma ordIso_Fpow_cong:
blanchet@48975
   977
assumes "r =o r'"
blanchet@48975
   978
shows "|Fpow(Field r)| =o |Fpow(Field r')|"
blanchet@48975
   979
using assms card_of_cong card_of_Fpow_cong by blast
blanchet@48975
   980
blanchet@48975
   981
lemma card_of_Fpow_lists: "|Fpow A| \<le>o |lists A|"
blanchet@48975
   982
proof-
blanchet@48975
   983
  have "set ` (lists A) = Fpow A"
blanchet@48975
   984
  unfolding lists_def2 Fpow_def using finite_list finite_set by blast
blanchet@48975
   985
  thus ?thesis using card_of_ordLeq2[of "Fpow A"] Fpow_not_empty[of A] by blast
blanchet@48975
   986
qed
blanchet@48975
   987
blanchet@48975
   988
lemma card_of_Fpow_infinite[simp]:
traytel@54578
   989
assumes "\<not>finite A"
blanchet@48975
   990
shows "|Fpow A| =o |A|"
blanchet@48975
   991
using assms card_of_Fpow_lists card_of_lists_infinite card_of_Fpow
blanchet@48975
   992
      ordLeq_ordIso_trans ordIso_iff_ordLeq by blast
blanchet@48975
   993
blanchet@48975
   994
corollary Fpow_infinite_bij_betw:
traytel@54578
   995
assumes "\<not>finite A"
blanchet@48975
   996
shows "\<exists>f. bij_betw f (Fpow A) A"
blanchet@48975
   997
using assms card_of_Fpow_infinite card_of_ordIso by blast
blanchet@48975
   998
blanchet@48975
   999
blanchet@48975
  1000
subsection {* The cardinal $\omega$ and the finite cardinals  *}
blanchet@48975
  1001
blanchet@48975
  1002
subsubsection {* First as well-orders *}
blanchet@48975
  1003
blanchet@48975
  1004
lemma Field_natLess: "Field natLess = (UNIV::nat set)"
blanchet@48975
  1005
by(unfold Field_def, auto)
blanchet@48975
  1006
blanchet@54475
  1007
lemma natLeq_well_order_on: "well_order_on UNIV natLeq"
blanchet@54475
  1008
using natLeq_Well_order Field_natLeq by auto
blanchet@54475
  1009
blanchet@54475
  1010
lemma natLeq_wo_rel: "wo_rel natLeq"
blanchet@54475
  1011
unfolding wo_rel_def using natLeq_Well_order .
blanchet@54475
  1012
blanchet@48975
  1013
lemma natLeq_ofilter_less: "ofilter natLeq {0 ..< n}"
blanchet@48975
  1014
by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
blanchet@54475
  1015
   simp add: Field_natLeq, unfold rel.under_def, auto)
blanchet@48975
  1016
blanchet@48975
  1017
lemma natLeq_ofilter_leq: "ofilter natLeq {0 .. n}"
blanchet@48975
  1018
by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
blanchet@54475
  1019
   simp add: Field_natLeq, unfold rel.under_def, auto)
blanchet@54475
  1020
blanchet@54475
  1021
lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV"
blanchet@54475
  1022
using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto
blanchet@48975
  1023
traytel@54581
  1024
lemma closed_nat_set_iff:
traytel@54581
  1025
assumes "\<forall>(m::nat) n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
traytel@54581
  1026
shows "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
traytel@54581
  1027
proof-
traytel@54581
  1028
  {assume "A \<noteq> UNIV" hence "\<exists>n. n \<notin> A" by blast
traytel@54581
  1029
   moreover obtain n where n_def: "n = (LEAST n. n \<notin> A)" by blast
traytel@54581
  1030
   ultimately have 1: "n \<notin> A \<and> (\<forall>m. m < n \<longrightarrow> m \<in> A)"
traytel@54581
  1031
   using LeastI_ex[of "\<lambda> n. n \<notin> A"] n_def Least_le[of "\<lambda> n. n \<notin> A"] by fastforce
traytel@54581
  1032
   have "A = {0 ..< n}"
traytel@54581
  1033
   proof(auto simp add: 1)
traytel@54581
  1034
     fix m assume *: "m \<in> A"
traytel@54581
  1035
     {assume "n \<le> m" with assms * have "n \<in> A" by blast
traytel@54581
  1036
      hence False using 1 by auto
traytel@54581
  1037
     }
traytel@54581
  1038
     thus "m < n" by fastforce
traytel@54581
  1039
   qed
traytel@54581
  1040
   hence "\<exists>n. A = {0 ..< n}" by blast
traytel@54581
  1041
  }
traytel@54581
  1042
  thus ?thesis by blast
traytel@54581
  1043
qed
traytel@54581
  1044
blanchet@48975
  1045
lemma natLeq_ofilter_iff:
blanchet@48975
  1046
"ofilter natLeq A = (A = UNIV \<or> (\<exists>n. A = {0 ..< n}))"
blanchet@48975
  1047
proof(rule iffI)
blanchet@48975
  1048
  assume "ofilter natLeq A"
blanchet@48975
  1049
  hence "\<forall>m n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
blanchet@48975
  1050
  by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def rel.under_def)
blanchet@48975
  1051
  thus "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
blanchet@48975
  1052
next
blanchet@48975
  1053
  assume "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
blanchet@48975
  1054
  thus "ofilter natLeq A"
blanchet@48975
  1055
  by(auto simp add: natLeq_ofilter_less natLeq_UNIV_ofilter)
blanchet@48975
  1056
qed
blanchet@48975
  1057
blanchet@48975
  1058
lemma natLeq_under_leq: "under natLeq n = {0 .. n}"
blanchet@48975
  1059
unfolding rel.under_def by auto
blanchet@48975
  1060
traytel@54581
  1061
lemma natLeq_on_ofilter_less_eq:
traytel@54581
  1062
"n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}"
traytel@54581
  1063
apply (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def)
traytel@54581
  1064
apply (simp add: Field_natLeq_on)
traytel@54581
  1065
by (auto simp add: rel.under_def)
traytel@54581
  1066
traytel@54581
  1067
lemma natLeq_on_ofilter_iff:
traytel@54581
  1068
"wo_rel.ofilter (natLeq_on m) A = (\<exists>n \<le> m. A = {0 ..< n})"
traytel@54581
  1069
proof(rule iffI)
traytel@54581
  1070
  assume *: "wo_rel.ofilter (natLeq_on m) A"
traytel@54581
  1071
  hence 1: "A \<le> {0..<m}"
traytel@54581
  1072
  by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def Field_natLeq_on)
traytel@54581
  1073
  hence "\<forall>n1 n2. n2 \<in> A \<and> n1 \<le> n2 \<longrightarrow> n1 \<in> A"
traytel@54581
  1074
  using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def)
traytel@54581
  1075
  hence "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
traytel@54581
  1076
  thus "\<exists>n \<le> m. A = {0 ..< n}" using 1 atLeastLessThan_less_eq by blast
traytel@54581
  1077
next
traytel@54581
  1078
  assume "(\<exists>n\<le>m. A = {0 ..< n})"
traytel@54581
  1079
  thus "wo_rel.ofilter (natLeq_on m) A" by (auto simp add: natLeq_on_ofilter_less_eq)
traytel@54581
  1080
qed
traytel@54581
  1081
blanchet@48975
  1082
corollary natLeq_on_ofilter:
blanchet@48975
  1083
"ofilter(natLeq_on n) {0 ..< n}"
blanchet@48975
  1084
by (auto simp add: natLeq_on_ofilter_less_eq)
blanchet@48975
  1085
blanchet@48975
  1086
lemma natLeq_on_ofilter_less:
blanchet@48975
  1087
"n < m \<Longrightarrow> ofilter (natLeq_on m) {0 .. n}"
blanchet@48975
  1088
by(auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def,
blanchet@48975
  1089
   simp add: Field_natLeq_on, unfold rel.under_def, auto)
blanchet@48975
  1090
blanchet@48975
  1091
lemma natLeq_on_ordLess_natLeq: "natLeq_on n <o natLeq"
traytel@54578
  1092
using Field_natLeq Field_natLeq_on[of n]
blanchet@48975
  1093
      finite_ordLess_infinite[of "natLeq_on n" natLeq]
blanchet@48975
  1094
      natLeq_Well_order natLeq_on_Well_order[of n] by auto
blanchet@48975
  1095
blanchet@48975
  1096
lemma natLeq_on_injective:
blanchet@48975
  1097
"natLeq_on m = natLeq_on n \<Longrightarrow> m = n"
blanchet@48975
  1098
using Field_natLeq_on[of m] Field_natLeq_on[of n]
traytel@54581
  1099
      atLeastLessThan_injective[of m n, unfolded atLeastLessThan_def] by blast
blanchet@48975
  1100
blanchet@48975
  1101
lemma natLeq_on_injective_ordIso:
blanchet@48975
  1102
"(natLeq_on m =o natLeq_on n) = (m = n)"
blanchet@48975
  1103
proof(auto simp add: natLeq_on_Well_order ordIso_reflexive)
blanchet@48975
  1104
  assume "natLeq_on m =o natLeq_on n"
traytel@54581
  1105
  then obtain f where "bij_betw f {x. x<m} {x. x<n}"
blanchet@48975
  1106
  using Field_natLeq_on assms unfolding ordIso_def iso_def[abs_def] by auto
traytel@54581
  1107
  thus "m = n" using atLeastLessThan_injective2[of f m n]
traytel@54581
  1108
    unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast
blanchet@48975
  1109
qed
blanchet@48975
  1110
blanchet@48975
  1111
blanchet@48975
  1112
subsubsection {* Then as cardinals *}
blanchet@48975
  1113
blanchet@48975
  1114
lemma ordIso_natLeq_infinite1:
traytel@54578
  1115
"|A| =o natLeq \<Longrightarrow> \<not>finite A"
blanchet@48975
  1116
using ordIso_symmetric ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
blanchet@48975
  1117
blanchet@48975
  1118
lemma ordIso_natLeq_infinite2:
traytel@54578
  1119
"natLeq =o |A| \<Longrightarrow> \<not>finite A"
blanchet@48975
  1120
using ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
blanchet@48975
  1121
traytel@54581
  1122
traytel@54581
  1123
lemma ordIso_natLeq_on_imp_finite:
traytel@54581
  1124
"|A| =o natLeq_on n \<Longrightarrow> finite A"
traytel@54581
  1125
unfolding ordIso_def iso_def[abs_def]
traytel@54581
  1126
by (auto simp: Field_natLeq_on bij_betw_finite)
traytel@54581
  1127
traytel@54581
  1128
traytel@54581
  1129
lemma natLeq_on_Card_order: "Card_order (natLeq_on n)"
traytel@54581
  1130
proof(unfold card_order_on_def,
traytel@54581
  1131
      auto simp add: natLeq_on_Well_order, simp add: Field_natLeq_on)
traytel@54581
  1132
  fix r assume "well_order_on {x. x < n} r"
traytel@54581
  1133
  thus "natLeq_on n \<le>o r"
traytel@54581
  1134
  using finite_atLeastLessThan natLeq_on_well_order_on
traytel@54581
  1135
        finite_well_order_on_ordIso ordIso_iff_ordLeq by blast
traytel@54581
  1136
qed
traytel@54581
  1137
traytel@54581
  1138
traytel@54581
  1139
corollary card_of_Field_natLeq_on:
traytel@54581
  1140
"|Field (natLeq_on n)| =o natLeq_on n"
traytel@54581
  1141
using Field_natLeq_on natLeq_on_Card_order
traytel@54581
  1142
      Card_order_iff_ordIso_card_of[of "natLeq_on n"]
traytel@54581
  1143
      ordIso_symmetric[of "natLeq_on n"] by blast
traytel@54581
  1144
traytel@54581
  1145
traytel@54581
  1146
corollary card_of_less:
traytel@54581
  1147
"|{0 ..< n}| =o natLeq_on n"
traytel@54581
  1148
using Field_natLeq_on card_of_Field_natLeq_on
traytel@54581
  1149
unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by auto
traytel@54581
  1150
traytel@54581
  1151
traytel@54581
  1152
lemma natLeq_on_ordLeq_less_eq:
traytel@54581
  1153
"((natLeq_on m) \<le>o (natLeq_on n)) = (m \<le> n)"
traytel@54581
  1154
proof
traytel@54581
  1155
  assume "natLeq_on m \<le>o natLeq_on n"
traytel@54581
  1156
  then obtain f where "inj_on f {x. x < m} \<and> f ` {x. x < m} \<le> {x. x < n}"
traytel@54581
  1157
  unfolding ordLeq_def using
traytel@54581
  1158
    embed_inj_on[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on]
traytel@54581
  1159
     embed_Field[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on] by blast
traytel@54581
  1160
  thus "m \<le> n" using atLeastLessThan_less_eq2
traytel@54581
  1161
    unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast
traytel@54581
  1162
next
traytel@54581
  1163
  assume "m \<le> n"
traytel@54581
  1164
  hence "inj_on id {0..<m} \<and> id ` {0..<m} \<le> {0..<n}" unfolding inj_on_def by auto
traytel@54581
  1165
  hence "|{0..<m}| \<le>o |{0..<n}|" using card_of_ordLeq by blast
traytel@54581
  1166
  thus "natLeq_on m \<le>o natLeq_on n"
traytel@54581
  1167
  using card_of_less ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
traytel@54581
  1168
qed
traytel@54581
  1169
traytel@54581
  1170
traytel@54581
  1171
lemma natLeq_on_ordLeq_less:
traytel@54581
  1172
"((natLeq_on m) <o (natLeq_on n)) = (m < n)"
traytel@54980
  1173
using not_ordLeq_iff_ordLess[OF natLeq_on_Well_order natLeq_on_Well_order, of n m]
traytel@54980
  1174
   natLeq_on_ordLeq_less_eq[of n m] by linarith
traytel@54581
  1175
blanchet@48975
  1176
lemma ordLeq_natLeq_on_imp_finite:
blanchet@48975
  1177
assumes "|A| \<le>o natLeq_on n"
blanchet@48975
  1178
shows "finite A"
blanchet@48975
  1179
proof-
blanchet@48975
  1180
  have "|A| \<le>o |{0 ..< n}|"
blanchet@48975
  1181
  using assms card_of_less ordIso_symmetric ordLeq_ordIso_trans by blast
blanchet@48975
  1182
  thus ?thesis by (auto simp add: card_of_ordLeq_finite)
blanchet@48975
  1183
qed
blanchet@48975
  1184
blanchet@48975
  1185
blanchet@54475
  1186
subsubsection {* "Backward compatibility" with the numeric cardinal operator for finite sets *}
blanchet@48975
  1187
traytel@54581
  1188
lemma finite_card_of_iff_card2:
traytel@54581
  1189
assumes FIN: "finite A" and FIN': "finite B"
traytel@54581
  1190
shows "( |A| \<le>o |B| ) = (card A \<le> card B)"
traytel@54581
  1191
using assms card_of_ordLeq[of A B] inj_on_iff_card_le[of A B] by blast
traytel@54581
  1192
traytel@54581
  1193
lemma finite_imp_card_of_natLeq_on:
traytel@54581
  1194
assumes "finite A"
traytel@54581
  1195
shows "|A| =o natLeq_on (card A)"
traytel@54581
  1196
proof-
traytel@54581
  1197
  obtain h where "bij_betw h A {0 ..< card A}"
traytel@54581
  1198
  using assms ex_bij_betw_finite_nat by blast
traytel@54581
  1199
  thus ?thesis using card_of_ordIso card_of_less ordIso_equivalence by blast
traytel@54581
  1200
qed
traytel@54581
  1201
traytel@54581
  1202
lemma finite_iff_card_of_natLeq_on:
traytel@54581
  1203
"finite A = (\<exists>n. |A| =o natLeq_on n)"
traytel@54581
  1204
using finite_imp_card_of_natLeq_on[of A]
traytel@54581
  1205
by(auto simp add: ordIso_natLeq_on_imp_finite)
traytel@54581
  1206
traytel@54581
  1207
blanchet@48975
  1208
lemma finite_card_of_iff_card:
blanchet@48975
  1209
assumes FIN: "finite A" and FIN': "finite B"
blanchet@48975
  1210
shows "( |A| =o |B| ) = (card A = card B)"
blanchet@48975
  1211
using assms card_of_ordIso[of A B] bij_betw_iff_card[of A B] by blast
blanchet@48975
  1212
blanchet@48975
  1213
lemma finite_card_of_iff_card3:
blanchet@48975
  1214
assumes FIN: "finite A" and FIN': "finite B"
blanchet@48975
  1215
shows "( |A| <o |B| ) = (card A < card B)"
blanchet@48975
  1216
proof-
blanchet@48975
  1217
  have "( |A| <o |B| ) = (~ ( |B| \<le>o |A| ))" by simp
blanchet@48975
  1218
  also have "... = (~ (card B \<le> card A))"
blanchet@48975
  1219
  using assms by(simp add: finite_card_of_iff_card2)
blanchet@48975
  1220
  also have "... = (card A < card B)" by auto
blanchet@48975
  1221
  finally show ?thesis .
blanchet@48975
  1222
qed
blanchet@48975
  1223
blanchet@48975
  1224
lemma card_Field_natLeq_on:
blanchet@48975
  1225
"card(Field(natLeq_on n)) = n"
blanchet@48975
  1226
using Field_natLeq_on card_atLeastLessThan by auto
blanchet@48975
  1227
blanchet@48975
  1228
blanchet@48975
  1229
subsection {* The successor of a cardinal *}
blanchet@48975
  1230
blanchet@48975
  1231
lemma embed_implies_ordIso_Restr:
blanchet@48975
  1232
assumes WELL: "Well_order r" and WELL': "Well_order r'" and EMB: "embed r' r f"
blanchet@48975
  1233
shows "r' =o Restr r (f ` (Field r'))"
blanchet@48975
  1234
using assms embed_implies_iso_Restr Well_order_Restr unfolding ordIso_def by blast
blanchet@48975
  1235
blanchet@48975
  1236
lemma cardSuc_Well_order[simp]:
blanchet@48975
  1237
"Card_order r \<Longrightarrow> Well_order(cardSuc r)"
blanchet@48975
  1238
using cardSuc_Card_order unfolding card_order_on_def by blast
blanchet@48975
  1239
blanchet@48975
  1240
lemma Field_cardSuc_not_empty:
blanchet@48975
  1241
assumes "Card_order r"
blanchet@48975
  1242
shows "Field (cardSuc r) \<noteq> {}"
blanchet@48975
  1243
proof
blanchet@48975
  1244
  assume "Field(cardSuc r) = {}"
blanchet@48975
  1245
  hence "|Field(cardSuc r)| \<le>o r" using assms Card_order_empty[of r] by auto
blanchet@48975
  1246
  hence "cardSuc r \<le>o r" using assms card_of_Field_ordIso
blanchet@48975
  1247
  cardSuc_Card_order ordIso_symmetric ordIso_ordLeq_trans by blast
blanchet@48975
  1248
  thus False using cardSuc_greater not_ordLess_ordLeq assms by blast
blanchet@48975
  1249
qed
blanchet@48975
  1250
blanchet@48975
  1251
lemma cardSuc_mono_ordLess[simp]:
blanchet@48975
  1252
assumes CARD: "Card_order r" and CARD': "Card_order r'"
blanchet@48975
  1253
shows "(cardSuc r <o cardSuc r') = (r <o r')"
blanchet@48975
  1254
proof-
blanchet@48975
  1255
  have 0: "Well_order r \<and> Well_order r' \<and> Well_order(cardSuc r) \<and> Well_order(cardSuc r')"
blanchet@48975
  1256
  using assms by auto
blanchet@48975
  1257
  thus ?thesis
blanchet@48975
  1258
  using not_ordLeq_iff_ordLess not_ordLeq_iff_ordLess[of r r']
blanchet@48975
  1259
  using cardSuc_mono_ordLeq[of r' r] assms by blast
blanchet@48975
  1260
qed
blanchet@48975
  1261
traytel@54581
  1262
lemma cardSuc_natLeq_on_Suc:
traytel@54581
  1263
"cardSuc(natLeq_on n) =o natLeq_on(Suc n)"
traytel@54581
  1264
proof-
traytel@54581
  1265
  obtain r r' p where r_def: "r = natLeq_on n" and
traytel@54581
  1266
                      r'_def: "r' = cardSuc(natLeq_on n)"  and
traytel@54581
  1267
                      p_def: "p = natLeq_on(Suc n)" by blast
traytel@54581
  1268
  (* Preliminary facts:  *)
traytel@54581
  1269
  have CARD: "Card_order r \<and> Card_order r' \<and> Card_order p" unfolding r_def r'_def p_def
traytel@54581
  1270
  using cardSuc_ordLess_ordLeq natLeq_on_Card_order cardSuc_Card_order by blast
traytel@54581
  1271
  hence WELL: "Well_order r \<and> Well_order r' \<and>  Well_order p"
traytel@54581
  1272
  unfolding card_order_on_def by force
traytel@54581
  1273
  have FIELD: "Field r = {0..<n} \<and> Field p = {0..<(Suc n)}"
traytel@54581
  1274
  unfolding r_def p_def Field_natLeq_on atLeast_0 atLeastLessThan_def lessThan_def by simp
traytel@54581
  1275
  hence FIN: "finite (Field r)" by force
traytel@54581
  1276
  have "r <o r'" using CARD unfolding r_def r'_def using cardSuc_greater by blast
traytel@54581
  1277
  hence "|Field r| <o r'" using CARD card_of_Field_ordIso ordIso_ordLess_trans by blast
traytel@54581
  1278
  hence LESS: "|Field r| <o |Field r'|"
traytel@54581
  1279
  using CARD card_of_Field_ordIso ordLess_ordIso_trans ordIso_symmetric by blast
traytel@54581
  1280
  (* Main proof: *)
traytel@54581
  1281
  have "r' \<le>o p" using CARD unfolding r_def r'_def p_def
traytel@54581
  1282
  using natLeq_on_ordLeq_less cardSuc_ordLess_ordLeq by blast
traytel@54581
  1283
  moreover have "p \<le>o r'"
traytel@54581
  1284
  proof-
traytel@54581
  1285
    {assume "r' <o p"
traytel@54581
  1286
     then obtain f where 0: "embedS r' p f" unfolding ordLess_def by force
traytel@54581
  1287
     let ?q = "Restr p (f ` Field r')"
traytel@54581
  1288
     have 1: "embed r' p f" using 0 unfolding embedS_def by force
traytel@54581
  1289
     hence 2: "f ` Field r' < {0..<(Suc n)}"
traytel@54581
  1290
     using WELL FIELD 0 by (auto simp add: embedS_iff)
traytel@54581
  1291
     have "wo_rel.ofilter p (f ` Field r')" using embed_Field_ofilter 1 WELL by blast
traytel@54581
  1292
     then obtain m where "m \<le> Suc n" and 3: "f ` (Field r') = {0..<m}"
traytel@54581
  1293
     unfolding p_def by (auto simp add: natLeq_on_ofilter_iff)
traytel@54581
  1294
     hence 4: "m \<le> n" using 2 by force
traytel@54581
  1295
     (*  *)
traytel@54581
  1296
     have "bij_betw f (Field r') (f ` (Field r'))"
traytel@54980
  1297
     using WELL embed_inj_on[OF _ 1] unfolding bij_betw_def by blast
traytel@54581
  1298
     moreover have "finite(f ` (Field r'))" using 3 finite_atLeastLessThan[of 0 m] by force
traytel@54581
  1299
     ultimately have 5: "finite (Field r') \<and> card(Field r') = card (f ` (Field r'))"
traytel@54581
  1300
     using bij_betw_same_card bij_betw_finite by metis
traytel@54581
  1301
     hence "card(Field r') \<le> card(Field r)" using 3 4 FIELD by force
traytel@54581
  1302
     hence "|Field r'| \<le>o |Field r|" using FIN 5 finite_card_of_iff_card2 by blast
traytel@54581
  1303
     hence False using LESS not_ordLess_ordLeq by auto
traytel@54581
  1304
    }
traytel@54581
  1305
    thus ?thesis using WELL CARD by fastforce
traytel@54581
  1306
  qed
traytel@54581
  1307
  ultimately show ?thesis using ordIso_iff_ordLeq unfolding r'_def p_def by blast
traytel@54581
  1308
qed
traytel@54581
  1309
blanchet@48975
  1310
lemma card_of_Plus_ordLeq_infinite[simp]:
traytel@54578
  1311
assumes C: "\<not>finite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
blanchet@48975
  1312
shows "|A <+> B| \<le>o |C|"
blanchet@48975
  1313
proof-
blanchet@48975
  1314
  let ?r = "cardSuc |C|"
traytel@54578
  1315
  have "Card_order ?r \<and> \<not>finite (Field ?r)" using assms by simp
blanchet@48975
  1316
  moreover have "|A| <o ?r" and "|B| <o ?r" using A B by auto
blanchet@48975
  1317
  ultimately have "|A <+> B| <o ?r"
blanchet@48975
  1318
  using card_of_Plus_ordLess_infinite_Field by blast
blanchet@48975
  1319
  thus ?thesis using C by simp
blanchet@48975
  1320
qed
blanchet@48975
  1321
blanchet@48975
  1322
lemma card_of_Un_ordLeq_infinite[simp]:
traytel@54578
  1323
assumes C: "\<not>finite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
blanchet@48975
  1324
shows "|A Un B| \<le>o |C|"
blanchet@48975
  1325
using assms card_of_Plus_ordLeq_infinite card_of_Un_Plus_ordLeq
blanchet@48975
  1326
ordLeq_transitive by metis
blanchet@48975
  1327
blanchet@48975
  1328
blanchet@48975
  1329
subsection {* Others *}
blanchet@48975
  1330
blanchet@48975
  1331
lemma under_mono[simp]:
blanchet@48975
  1332
assumes "Well_order r" and "(i,j) \<in> r"
blanchet@48975
  1333
shows "under r i \<subseteq> under r j"
blanchet@48975
  1334
using assms unfolding rel.under_def order_on_defs
blanchet@48975
  1335
trans_def by blast
blanchet@48975
  1336
blanchet@48975
  1337
lemma underS_under:
blanchet@48975
  1338
assumes "i \<in> Field r"
blanchet@48975
  1339
shows "underS r i = under r i - {i}"
blanchet@48975
  1340
using assms unfolding rel.underS_def rel.under_def by auto
blanchet@48975
  1341
blanchet@48975
  1342
lemma relChain_under:
blanchet@48975
  1343
assumes "Well_order r"
blanchet@48975
  1344
shows "relChain r (\<lambda> i. under r i)"
blanchet@48975
  1345
using assms unfolding relChain_def by auto
blanchet@48975
  1346
blanchet@54475
  1347
lemma card_of_infinite_diff_finite:
traytel@54578
  1348
assumes "\<not>finite A" and "finite B"
blanchet@54475
  1349
shows "|A - B| =o |A|"
blanchet@54475
  1350
by (metis assms card_of_Un_diff_infinite finite_ordLess_infinite2)
blanchet@54475
  1351
blanchet@48975
  1352
lemma infinite_card_of_diff_singl:
traytel@54578
  1353
assumes "\<not>finite A"
blanchet@48975
  1354
shows "|A - {a}| =o |A|"
traytel@52544
  1355
by (metis assms card_of_infinite_diff_finite finite.emptyI finite_insert)
blanchet@48975
  1356
blanchet@48975
  1357
lemma card_of_vimage:
blanchet@48975
  1358
assumes "B \<subseteq> range f"
blanchet@48975
  1359
shows "|B| \<le>o |f -` B|"
blanchet@48975
  1360
apply(rule surj_imp_ordLeq[of _ f])
blanchet@48975
  1361
using assms by (metis Int_absorb2 image_vimage_eq order_refl)
blanchet@48975
  1362
blanchet@48975
  1363
lemma surj_card_of_vimage:
blanchet@48975
  1364
assumes "surj f"
blanchet@48975
  1365
shows "|B| \<le>o |f -` B|"
blanchet@48975
  1366
by (metis assms card_of_vimage subset_UNIV)
blanchet@48975
  1367
traytel@54794
  1368
lemma infinite_Pow:
traytel@54794
  1369
assumes "\<not> finite A"
traytel@54794
  1370
shows "\<not> finite (Pow A)"
traytel@54794
  1371
proof-
traytel@54794
  1372
  have "|A| \<le>o |Pow A|" by (metis card_of_Pow ordLess_imp_ordLeq)
traytel@54794
  1373
  thus ?thesis by (metis assms finite_Pow_iff)
traytel@54794
  1374
qed
traytel@54794
  1375
blanchet@48975
  1376
(* bounded powerset *)
blanchet@48975
  1377
definition Bpow where
blanchet@48975
  1378
"Bpow r A \<equiv> {X . X \<subseteq> A \<and> |X| \<le>o r}"
blanchet@48975
  1379
blanchet@48975
  1380
lemma Bpow_empty[simp]:
blanchet@48975
  1381
assumes "Card_order r"
blanchet@48975
  1382
shows "Bpow r {} = {{}}"
blanchet@48975
  1383
using assms unfolding Bpow_def by auto
blanchet@48975
  1384
blanchet@48975
  1385
lemma singl_in_Bpow:
blanchet@48975
  1386
assumes rc: "Card_order r"
blanchet@48975
  1387
and r: "Field r \<noteq> {}" and a: "a \<in> A"
blanchet@48975
  1388
shows "{a} \<in> Bpow r A"
blanchet@48975
  1389
proof-
blanchet@48975
  1390
  have "|{a}| \<le>o r" using r rc by auto
blanchet@48975
  1391
  thus ?thesis unfolding Bpow_def using a by auto
blanchet@48975
  1392
qed
blanchet@48975
  1393
blanchet@48975
  1394
lemma ordLeq_card_Bpow:
blanchet@48975
  1395
assumes rc: "Card_order r" and r: "Field r \<noteq> {}"
blanchet@48975
  1396
shows "|A| \<le>o |Bpow r A|"
blanchet@48975
  1397
proof-
blanchet@48975
  1398
  have "inj_on (\<lambda> a. {a}) A" unfolding inj_on_def by auto
blanchet@48975
  1399
  moreover have "(\<lambda> a. {a}) ` A \<subseteq> Bpow r A"
blanchet@48975
  1400
  using singl_in_Bpow[OF assms] by auto
blanchet@48975
  1401
  ultimately show ?thesis unfolding card_of_ordLeq[symmetric] by blast
blanchet@48975
  1402
qed
blanchet@48975
  1403
blanchet@48975
  1404
lemma infinite_Bpow:
blanchet@48975
  1405
assumes rc: "Card_order r" and r: "Field r \<noteq> {}"
traytel@54578
  1406
and A: "\<not>finite A"
traytel@54578
  1407
shows "\<not>finite (Bpow r A)"
blanchet@48975
  1408
using ordLeq_card_Bpow[OF rc r]
blanchet@48975
  1409
by (metis A card_of_ordLeq_infinite)
blanchet@48975
  1410
traytel@52545
  1411
definition Func_option where
traytel@52545
  1412
 "Func_option A B \<equiv>
traytel@52545
  1413
  {f. (\<forall> a. f a \<noteq> None \<longleftrightarrow> a \<in> A) \<and> (\<forall> a \<in> A. case f a of Some b \<Rightarrow> b \<in> B |None \<Rightarrow> True)}"
traytel@52545
  1414
traytel@52545
  1415
lemma card_of_Func_option_Func:
traytel@52545
  1416
"|Func_option A B| =o |Func A B|"
traytel@52545
  1417
proof (rule ordIso_symmetric, unfold card_of_ordIso[symmetric], intro exI)
traytel@52545
  1418
  let ?F = "\<lambda> f a. if a \<in> A then Some (f a) else None"
traytel@52545
  1419
  show "bij_betw ?F (Func A B) (Func_option A B)"
traytel@52545
  1420
  unfolding bij_betw_def unfolding inj_on_def proof(intro conjI ballI impI)
traytel@52545
  1421
    fix f g assume f: "f \<in> Func A B" and g: "g \<in> Func A B" and eq: "?F f = ?F g"
traytel@52545
  1422
    show "f = g"
traytel@52545
  1423
    proof(rule ext)
traytel@52545
  1424
      fix a
traytel@52545
  1425
      show "f a = g a"
traytel@52545
  1426
      proof(cases "a \<in> A")
traytel@52545
  1427
        case True
traytel@52545
  1428
        have "Some (f a) = ?F f a" using True by auto
traytel@52545
  1429
        also have "... = ?F g a" using eq unfolding fun_eq_iff by(rule allE)
traytel@52545
  1430
        also have "... = Some (g a)" using True by auto
traytel@52545
  1431
        finally have "Some (f a) = Some (g a)" .
traytel@52545
  1432
        thus ?thesis by simp
traytel@52545
  1433
      qed(insert f g, unfold Func_def, auto)
traytel@52545
  1434
    qed
traytel@52545
  1435
  next
traytel@52545
  1436
    show "?F ` Func A B = Func_option A B"
traytel@52545
  1437
    proof safe
traytel@52545
  1438
      fix f assume f: "f \<in> Func_option A B"
traytel@52545
  1439
      def g \<equiv> "\<lambda> a. case f a of Some b \<Rightarrow> b | None \<Rightarrow> undefined"
traytel@52545
  1440
      have "g \<in> Func A B"
traytel@52545
  1441
      using f unfolding g_def Func_def Func_option_def by force+
traytel@52545
  1442
      moreover have "f = ?F g"
traytel@52545
  1443
      proof(rule ext)
traytel@52545
  1444
        fix a show "f a = ?F g a"
traytel@52545
  1445
        using f unfolding Func_option_def g_def by (cases "a \<in> A") force+
traytel@52545
  1446
      qed
traytel@52545
  1447
      ultimately show "f \<in> ?F ` (Func A B)" by blast
traytel@52545
  1448
    qed(unfold Func_def Func_option_def, auto)
traytel@52545
  1449
  qed
traytel@52545
  1450
qed
traytel@52545
  1451
traytel@52545
  1452
(* partial-function space: *)
traytel@52545
  1453
definition Pfunc where
traytel@52545
  1454
"Pfunc A B \<equiv>
traytel@52545
  1455
 {f. (\<forall>a. f a \<noteq> None \<longrightarrow> a \<in> A) \<and>
traytel@52545
  1456
     (\<forall>a. case f a of None \<Rightarrow> True | Some b \<Rightarrow> b \<in> B)}"
traytel@52545
  1457
traytel@52545
  1458
lemma Func_Pfunc:
traytel@52545
  1459
"Func_option A B \<subseteq> Pfunc A B"
traytel@52545
  1460
unfolding Func_option_def Pfunc_def by auto
traytel@52545
  1461
traytel@52545
  1462
lemma Pfunc_Func_option:
traytel@52545
  1463
"Pfunc A B = (\<Union> A' \<in> Pow A. Func_option A' B)"
traytel@52545
  1464
proof safe
traytel@52545
  1465
  fix f assume f: "f \<in> Pfunc A B"
traytel@52545
  1466
  show "f \<in> (\<Union>A'\<in>Pow A. Func_option A' B)"
traytel@52545
  1467
  proof (intro UN_I)
traytel@52545
  1468
    let ?A' = "{a. f a \<noteq> None}"
traytel@52545
  1469
    show "?A' \<in> Pow A" using f unfolding Pow_def Pfunc_def by auto
traytel@52545
  1470
    show "f \<in> Func_option ?A' B" using f unfolding Func_option_def Pfunc_def by auto
traytel@52545
  1471
  qed
traytel@52545
  1472
next
traytel@52545
  1473
  fix f A' assume "f \<in> Func_option A' B" and "A' \<subseteq> A"
traytel@52545
  1474
  thus "f \<in> Pfunc A B" unfolding Func_option_def Pfunc_def by auto
traytel@52545
  1475
qed
traytel@52545
  1476
blanchet@54475
  1477
lemma card_of_Func_mono:
blanchet@54475
  1478
fixes A1 A2 :: "'a set" and B :: "'b set"
blanchet@54475
  1479
assumes A12: "A1 \<subseteq> A2" and B: "B \<noteq> {}"
blanchet@54475
  1480
shows "|Func A1 B| \<le>o |Func A2 B|"
blanchet@54475
  1481
proof-
blanchet@54475
  1482
  obtain bb where bb: "bb \<in> B" using B by auto
blanchet@54475
  1483
  def F \<equiv> "\<lambda> (f1::'a \<Rightarrow> 'b) a. if a \<in> A2 then (if a \<in> A1 then f1 a else bb)
blanchet@54475
  1484
                                                else undefined"
blanchet@54475
  1485
  show ?thesis unfolding card_of_ordLeq[symmetric] proof(intro exI[of _ F] conjI)
blanchet@54475
  1486
    show "inj_on F (Func A1 B)" unfolding inj_on_def proof safe
blanchet@54475
  1487
      fix f g assume f: "f \<in> Func A1 B" and g: "g \<in> Func A1 B" and eq: "F f = F g"
blanchet@54475
  1488
      show "f = g"
blanchet@54475
  1489
      proof(rule ext)
blanchet@54475
  1490
        fix a show "f a = g a"
blanchet@54475
  1491
        proof(cases "a \<in> A1")
blanchet@54475
  1492
          case True
blanchet@54475
  1493
          thus ?thesis using eq A12 unfolding F_def fun_eq_iff
blanchet@54475
  1494
          by (elim allE[of _ a]) auto
blanchet@54475
  1495
        qed(insert f g, unfold Func_def, fastforce)
blanchet@54475
  1496
      qed
blanchet@54475
  1497
    qed
blanchet@54475
  1498
  qed(insert bb, unfold Func_def F_def, force)
blanchet@54475
  1499
qed
blanchet@54475
  1500
traytel@52545
  1501
lemma card_of_Func_option_mono:
traytel@52545
  1502
fixes A1 A2 :: "'a set" and B :: "'b set"
traytel@52545
  1503
assumes A12: "A1 \<subseteq> A2" and B: "B \<noteq> {}"
traytel@52545
  1504
shows "|Func_option A1 B| \<le>o |Func_option A2 B|"
traytel@52545
  1505
by (metis card_of_Func_mono[OF A12 B] card_of_Func_option_Func
traytel@52545
  1506
  ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric)
traytel@52545
  1507
traytel@52545
  1508
lemma card_of_Pfunc_Pow_Func_option:
traytel@52545
  1509
assumes "B \<noteq> {}"
traytel@52545
  1510
shows "|Pfunc A B| \<le>o |Pow A <*> Func_option A B|"
traytel@52545
  1511
proof-
traytel@52545
  1512
  have "|Pfunc A B| =o |\<Union> A' \<in> Pow A. Func_option A' B|" (is "_ =o ?K")
traytel@52545
  1513
    unfolding Pfunc_Func_option by(rule card_of_refl)
traytel@52545
  1514
  also have "?K \<le>o |Sigma (Pow A) (\<lambda> A'. Func_option A' B)|" using card_of_UNION_Sigma .
traytel@52545
  1515
  also have "|Sigma (Pow A) (\<lambda> A'. Func_option A' B)| \<le>o |Pow A <*> Func_option A B|"
traytel@52545
  1516
    apply(rule card_of_Sigma_mono1) using card_of_Func_option_mono[OF _ assms] by auto
traytel@52545
  1517
  finally show ?thesis .
traytel@52545
  1518
qed
traytel@52545
  1519
blanchet@48975
  1520
lemma Bpow_ordLeq_Func_Field:
traytel@54578
  1521
assumes rc: "Card_order r" and r: "Field r \<noteq> {}" and A: "\<not>finite A"
blanchet@48975
  1522
shows "|Bpow r A| \<le>o |Func (Field r) A|"
blanchet@48975
  1523
proof-
traytel@52545
  1524
  let ?F = "\<lambda> f. {x | x a. f a = x \<and> a \<in> Field r}"
blanchet@48975
  1525
  {fix X assume "X \<in> Bpow r A - {{}}"
blanchet@48975
  1526
   hence XA: "X \<subseteq> A" and "|X| \<le>o r"
blanchet@48975
  1527
   and X: "X \<noteq> {}" unfolding Bpow_def by auto
blanchet@48975
  1528
   hence "|X| \<le>o |Field r|" by (metis Field_card_of card_of_mono2)
blanchet@48975
  1529
   then obtain F where 1: "X = F ` (Field r)"
blanchet@48975
  1530
   using card_of_ordLeq2[OF X] by metis
traytel@52545
  1531
   def f \<equiv> "\<lambda> i. if i \<in> Field r then F i else undefined"
blanchet@48975
  1532
   have "\<exists> f \<in> Func (Field r) A. X = ?F f"
blanchet@48975
  1533
   apply (intro bexI[of _ f]) using 1 XA unfolding Func_def f_def by auto
blanchet@48975
  1534
  }
blanchet@48975
  1535
  hence "Bpow r A - {{}} \<subseteq> ?F ` (Func (Field r) A)" by auto
blanchet@48975
  1536
  hence "|Bpow r A - {{}}| \<le>o |Func (Field r) A|"
blanchet@48975
  1537
  by (rule surj_imp_ordLeq)
blanchet@48975
  1538
  moreover
traytel@54578
  1539
  {have 2: "\<not>finite (Bpow r A)" using infinite_Bpow[OF rc r A] .
blanchet@48975
  1540
   have "|Bpow r A| =o |Bpow r A - {{}}|"
traytel@54578
  1541
     by (metis 2 infinite_card_of_diff_singl ordIso_symmetric)
blanchet@48975
  1542
  }
blanchet@48975
  1543
  ultimately show ?thesis by (metis ordIso_ordLeq_trans)
blanchet@48975
  1544
qed
blanchet@48975
  1545
blanchet@48975
  1546
lemma empty_in_Func[simp]:
traytel@52545
  1547
"B \<noteq> {} \<Longrightarrow> (\<lambda>x. undefined) \<in> Func {} B"
blanchet@48975
  1548
unfolding Func_def by auto
blanchet@48975
  1549
blanchet@48975
  1550
lemma Func_mono[simp]:
blanchet@48975
  1551
assumes "B1 \<subseteq> B2"
blanchet@48975
  1552
shows "Func A B1 \<subseteq> Func A B2"
blanchet@48975
  1553
using assms unfolding Func_def by force
blanchet@48975
  1554
blanchet@48975
  1555
lemma Pfunc_mono[simp]:
blanchet@48975
  1556
assumes "A1 \<subseteq> A2" and "B1 \<subseteq> B2"
blanchet@48975
  1557
shows "Pfunc A B1 \<subseteq> Pfunc A B2"
blanchet@48975
  1558
using assms in_mono unfolding Pfunc_def apply safe
blanchet@48975
  1559
apply(case_tac "x a", auto)
blanchet@48975
  1560
by (metis in_mono option.simps(5))
blanchet@48975
  1561
blanchet@48975
  1562
lemma card_of_Func_UNIV_UNIV:
blanchet@48975
  1563
"|Func (UNIV::'a set) (UNIV::'b set)| =o |UNIV::('a \<Rightarrow> 'b) set|"
blanchet@48975
  1564
using card_of_Func_UNIV[of "UNIV::'b set"] by auto
blanchet@48975
  1565
blanchet@54475
  1566
lemma ordLeq_Func:
blanchet@54475
  1567
assumes "{b1,b2} \<subseteq> B" "b1 \<noteq> b2"
blanchet@54475
  1568
shows "|A| \<le>o |Func A B|"
blanchet@54475
  1569
unfolding card_of_ordLeq[symmetric] proof(intro exI conjI)
blanchet@54475
  1570
  let ?F = "\<lambda> aa a. if a \<in> A then (if a = aa then b1 else b2) else undefined"
blanchet@54475
  1571
  show "inj_on ?F A" using assms unfolding inj_on_def fun_eq_iff by auto
blanchet@54475
  1572
  show "?F ` A \<subseteq> Func A B" using assms unfolding Func_def by auto
blanchet@54475
  1573
qed
blanchet@54475
  1574
blanchet@54475
  1575
lemma infinite_Func:
traytel@54578
  1576
assumes A: "\<not>finite A" and B: "{b1,b2} \<subseteq> B" "b1 \<noteq> b2"
traytel@54578
  1577
shows "\<not>finite (Func A B)"
blanchet@54475
  1578
using ordLeq_Func[OF B] by (metis A card_of_ordLeq_finite)
blanchet@54475
  1579
traytel@54980
  1580
section {* Infinite cardinals are limit ordinals *}
traytel@54980
  1581
traytel@54980
  1582
lemma card_order_infinite_isLimOrd:
traytel@54980
  1583
assumes c: "Card_order r" and i: "\<not>finite (Field r)"
traytel@54980
  1584
shows "isLimOrd r"
traytel@54980
  1585
proof-
traytel@54980
  1586
  have 0: "wo_rel r" and 00: "Well_order r"
traytel@54980
  1587
  using c unfolding card_order_on_def wo_rel_def by auto
traytel@54980
  1588
  hence rr: "Refl r" by (metis wo_rel.REFL)
traytel@54980
  1589
  show ?thesis unfolding wo_rel.isLimOrd_def[OF 0] wo_rel.isSuccOrd_def[OF 0] proof safe
traytel@54980
  1590
    fix j assume j: "j \<in> Field r" and jm: "\<forall>i\<in>Field r. (i, j) \<in> r"
traytel@54980
  1591
    def p \<equiv> "Restr r (Field r - {j})"
traytel@54980
  1592
    have fp: "Field p = Field r - {j}"
traytel@54980
  1593
    unfolding p_def apply(rule Refl_Field_Restr2[OF rr]) by auto
traytel@54980
  1594
    have of: "ofilter r (Field p)" unfolding wo_rel.ofilter_def[OF 0] proof safe
traytel@54980
  1595
      fix a x assume a: "a \<in> Field p" and "x \<in> under r a"
traytel@54980
  1596
      hence x: "(x,a) \<in> r" "x \<in> Field r" unfolding rel.under_def Field_def by auto
traytel@54980
  1597
      moreover have a: "a \<noteq> j" "a \<in> Field r" "(a,j) \<in> r" using a jm  unfolding fp by auto
traytel@54980
  1598
      ultimately have "x \<noteq> j" using j jm  by (metis 0 wo_rel.max2_def wo_rel.max2_equals1)
traytel@54980
  1599
      thus "x \<in> Field p" using x unfolding fp by auto
traytel@54980
  1600
    qed(unfold p_def Field_def, auto)
traytel@54980
  1601
    have "p <o r" using j ofilter_ordLess[OF 00 of] unfolding fp p_def[symmetric] by auto
traytel@54980
  1602
    hence 2: "|Field p| <o r" using c by (metis Cardinal_Order_Relation_FP.ordLess_Field)
traytel@54980
  1603
    have "|Field p| =o |Field r|" unfolding fp using i by (metis infinite_card_of_diff_singl)
traytel@54980
  1604
    also have "|Field r| =o r"
traytel@54980
  1605
    using c by (metis card_of_unique ordIso_symmetric)
traytel@54980
  1606
    finally have "|Field p| =o r" .
traytel@54980
  1607
    with 2 show False by (metis not_ordLess_ordIso)
traytel@54980
  1608
  qed
traytel@54980
  1609
qed
traytel@54980
  1610
traytel@54980
  1611
lemma insert_Chain:
traytel@54980
  1612
assumes "Refl r" "C \<in> Chains r" and "i \<in> Field r" and "\<And>j. j \<in> C \<Longrightarrow> (j,i) \<in> r \<or> (i,j) \<in> r"
traytel@54980
  1613
shows "insert i C \<in> Chains r"
traytel@54980
  1614
using assms unfolding Chains_def by (auto dest: refl_onD)
traytel@54980
  1615
traytel@54980
  1616
lemma Collect_insert: "{R j |j. j \<in> insert j1 J} = insert (R j1) {R j |j. j \<in> J}"
traytel@54980
  1617
by auto
traytel@54980
  1618
traytel@54980
  1619
lemma Field_init_seg_of[simp]:
traytel@54980
  1620
"Field init_seg_of = UNIV"
traytel@54980
  1621
unfolding Field_def init_seg_of_def by auto
traytel@54980
  1622
traytel@54980
  1623
lemma refl_init_seg_of[intro, simp]: "refl init_seg_of"
traytel@54980
  1624
unfolding refl_on_def Field_def by auto
traytel@54980
  1625
traytel@54980
  1626
lemma regular_all_ex:
traytel@54980
  1627
assumes r: "Card_order r"   "regular r"
traytel@54980
  1628
and As: "\<And> i j b. b \<in> B \<Longrightarrow> (i,j) \<in> r \<Longrightarrow> P i b \<Longrightarrow> P j b"
traytel@54980
  1629
and Bsub: "\<forall> b \<in> B. \<exists> i \<in> Field r. P i b"
traytel@54980
  1630
and cardB: "|B| <o r"
traytel@54980
  1631
shows "\<exists> i \<in> Field r. \<forall> b \<in> B. P i b"
traytel@54980
  1632
proof-
traytel@54980
  1633
  let ?As = "\<lambda>i. {b \<in> B. P i b}"
traytel@54980
  1634
  have "EX i : Field r. B \<le> ?As i"
traytel@54980
  1635
  apply(rule regular_UNION) using assms unfolding relChain_def by auto
traytel@54980
  1636
  thus ?thesis by auto
traytel@54980
  1637
qed
traytel@54980
  1638
traytel@54980
  1639
lemma relChain_stabilize:
traytel@54980
  1640
assumes rc: "relChain r As" and AsB: "(\<Union> i \<in> Field r. As i) \<subseteq> B" and Br: "|B| <o r"
traytel@54980
  1641
and ir: "\<not>finite (Field r)" and cr: "Card_order r"
traytel@54980
  1642
shows "\<exists> i \<in> Field r. As (succ r i) = As i"
traytel@54980
  1643
proof(rule ccontr, auto)
traytel@54980
  1644
  have 0: "wo_rel r" and 00: "Well_order r"
traytel@54980
  1645
  unfolding wo_rel_def by (metis card_order_on_well_order_on cr)+
traytel@54980
  1646
  have L: "isLimOrd r" using ir cr by (metis card_order_infinite_isLimOrd)
traytel@54980
  1647
  have AsBs: "(\<Union> i \<in> Field r. As (succ r i)) \<subseteq> B"
traytel@54980
  1648
  using AsB L apply safe by (metis "0" UN_I set_mp wo_rel.isLimOrd_succ)
traytel@54980
  1649
  assume As_s: "\<forall>i\<in>Field r. As (succ r i) \<noteq> As i"
traytel@54980
  1650
  have 1: "\<forall>i j. (i,j) \<in> r \<and> i \<noteq> j \<longrightarrow> As i \<subset> As j"
traytel@54980
  1651
  proof safe
traytel@54980
  1652
    fix i j assume 1: "(i, j) \<in> r" "i \<noteq> j" and Asij: "As i = As j"
traytel@54980
  1653
    hence rij: "(succ r i, j) \<in> r" by (metis "0" wo_rel.succ_smallest)
traytel@54980
  1654
    hence "As (succ r i) \<subseteq> As j" using rc unfolding relChain_def by auto
traytel@54980
  1655
    moreover
traytel@54980
  1656
    {have "(i,succ r i) \<in> r" apply(rule wo_rel.succ_in[OF 0])
traytel@54980
  1657
     using 1 unfolding rel.aboveS_def by auto
traytel@54980
  1658
     hence "As i \<subset> As (succ r i)" using As_s rc rij unfolding relChain_def Field_def by auto
traytel@54980
  1659
    }
traytel@54980
  1660
    ultimately show False unfolding Asij by auto
traytel@54980
  1661
  qed (insert rc, unfold relChain_def, auto)
traytel@54980
  1662
  hence "\<forall> i \<in> Field r. \<exists> a. a \<in> As (succ r i) - As i"
traytel@54980
  1663
  using wo_rel.succ_in[OF 0] AsB
traytel@54980
  1664
  by(metis 0 card_order_infinite_isLimOrd cr ir psubset_imp_ex_mem
traytel@54980
  1665
            wo_rel.isLimOrd_aboveS wo_rel.succ_diff)
traytel@54980
  1666
  then obtain f where f: "\<forall> i \<in> Field r. f i \<in> As (succ r i) - As i" by metis
traytel@54980
  1667
  have "inj_on f (Field r)" unfolding inj_on_def proof safe
traytel@54980
  1668
    fix i j assume ij: "i \<in> Field r" "j \<in> Field r" and fij: "f i = f j"
traytel@54980
  1669
    show "i = j"
traytel@54980
  1670
    proof(cases rule: wo_rel.cases_Total3[OF 0], safe)
traytel@54980
  1671
      assume "(i, j) \<in> r" and ijd: "i \<noteq> j"
traytel@54980
  1672
      hence rij: "(succ r i, j) \<in> r" by (metis "0" wo_rel.succ_smallest)
traytel@54980
  1673
      hence "As (succ r i) \<subseteq> As j" using rc unfolding relChain_def by auto
traytel@54980
  1674
      thus "i = j" using ij ijd fij f by auto
traytel@54980
  1675
    next
traytel@54980
  1676
      assume "(j, i) \<in> r" and ijd: "i \<noteq> j"
traytel@54980
  1677
      hence rij: "(succ r j, i) \<in> r" by (metis "0" wo_rel.succ_smallest)
traytel@54980
  1678
      hence "As (succ r j) \<subseteq> As i" using rc unfolding relChain_def by auto
traytel@54980
  1679
      thus "j = i" using ij ijd fij f by fastforce
traytel@54980
  1680
    qed(insert ij, auto)
traytel@54980
  1681
  qed
traytel@54980
  1682
  moreover have "f ` (Field r) \<subseteq> B" using f AsBs by auto
traytel@54980
  1683
  moreover have "|B| <o |Field r|" using Br cr by (metis card_of_unique ordLess_ordIso_trans)
traytel@54980
  1684
  ultimately show False unfolding card_of_ordLess[symmetric] by auto
traytel@54980
  1685
qed
traytel@54980
  1686
traytel@54980
  1687
section {* Regular vs. Stable Cardinals *}
traytel@54980
  1688
traytel@54980
  1689
definition stable :: "'a rel \<Rightarrow> bool"
traytel@54980
  1690
where
traytel@54980
  1691
"stable r \<equiv> \<forall>(A::'a set) (F :: 'a \<Rightarrow> 'a set).
traytel@54980
  1692
               |A| <o r \<and> (\<forall>a \<in> A. |F a| <o r)
traytel@54980
  1693
               \<longrightarrow> |SIGMA a : A. F a| <o r"
traytel@54980
  1694
traytel@54980
  1695
lemma regular_stable:
traytel@54980
  1696
assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and reg: "regular r"
traytel@54980
  1697
shows "stable r"
traytel@54980
  1698
unfolding stable_def proof safe
traytel@54980
  1699
  fix A :: "'a set" and F :: "'a \<Rightarrow> 'a set" assume A: "|A| <o r" and F: "\<forall>a\<in>A. |F a| <o r"
traytel@54980
  1700
  {assume "r \<le>o |Sigma A F|"
traytel@54980
  1701
   hence "|Field r| \<le>o |Sigma A F|" using card_of_Field_ordIso[OF cr]
traytel@54980
  1702
   by (metis Field_card_of card_of_cong ordLeq_iff_ordLess_or_ordIso ordLeq_ordLess_trans)
traytel@54980
  1703
   moreover have Fi: "Field r \<noteq> {}" using ir by auto
traytel@54980
  1704
   ultimately obtain f where f: "f ` Sigma A F = Field r" using card_of_ordLeq2 by metis
traytel@54980
  1705
   have r: "wo_rel r" using cr unfolding card_order_on_def wo_rel_def by auto
traytel@54980
  1706
   {fix a assume a: "a \<in> A"
traytel@54980
  1707
    def L \<equiv> "{(a,u) | u. u \<in> F a}"
traytel@54980
  1708
    have fL: "f ` L \<subseteq> Field r" using f a unfolding L_def by auto
traytel@54980
  1709
    have "|L| =o |F a|" unfolding L_def card_of_ordIso[symmetric]
traytel@54980
  1710
    apply(rule exI[of _ snd]) unfolding bij_betw_def inj_on_def by (auto simp: image_def)
traytel@54980
  1711
    hence "|L| <o r" using F a ordIso_ordLess_trans[of "|L|" "|F a|"] unfolding L_def by auto
traytel@54980
  1712
    hence "|f ` L| <o r" using ordLeq_ordLess_trans[OF card_of_image, of "L"] unfolding L_def by auto
traytel@54980
  1713
    hence "\<not> cofinal (f ` L) r" using reg fL unfolding regular_def by (metis not_ordLess_ordIso)
traytel@54980
  1714
    then obtain k where k: "k \<in> Field r" and "\<forall> l \<in> L. \<not> (f l \<noteq> k \<and> (k, f l) \<in> r)"
traytel@54980
  1715
    unfolding cofinal_def image_def by auto
traytel@54980
  1716
    hence "\<exists> k \<in> Field r. \<forall> l \<in> L. (f l, k) \<in> r" using r by (metis fL image_subset_iff wo_rel.in_notinI)
traytel@54980
  1717
    hence "\<exists> k \<in> Field r. \<forall> u \<in> F a. (f (a,u), k) \<in> r" unfolding L_def by auto
traytel@54980
  1718
   }
traytel@54980
  1719
   then obtain gg where gg: "\<forall> a \<in> A. \<forall> u \<in> F a. (f (a,u), gg a) \<in> r" by metis
traytel@54980
  1720
   obtain j0 where j0: "j0 \<in> Field r" using Fi by auto
traytel@54980
  1721
   def g \<equiv> "\<lambda> a. if F a \<noteq> {} then gg a else j0"
traytel@54980
  1722
   have g: "\<forall> a \<in> A. \<forall> u \<in> F a. (f (a,u),g a) \<in> r" using gg unfolding g_def by auto
traytel@54980
  1723
   hence 1: "Field r \<subseteq> (\<Union> a \<in> A. under r (g a))"
traytel@54980
  1724
   using f[symmetric] unfolding rel.under_def image_def by auto
traytel@54980
  1725
   have gA: "g ` A \<subseteq> Field r" using gg j0 unfolding Field_def g_def by auto
traytel@54980
  1726
   moreover have "cofinal (g ` A) r" unfolding cofinal_def proof safe
traytel@54980
  1727
     fix i assume "i \<in> Field r"
traytel@54980
  1728
     then obtain j where ij: "(i,j) \<in> r" "i \<noteq> j" using cr ir by (metis infinite_Card_order_limit)
traytel@54980
  1729
     hence "j \<in> Field r" by (metis card_order_on_def cr rel.well_order_on_domain)
traytel@54980
  1730
     then obtain a where a: "a \<in> A" and j: "(j, g a) \<in> r" using 1 unfolding rel.under_def by auto
traytel@54980
  1731
     hence "(i, g a) \<in> r" using ij wo_rel.TRANS[OF r] unfolding trans_def by blast
traytel@54980
  1732
     moreover have "i \<noteq> g a"
traytel@54980
  1733
     using ij j r unfolding wo_rel_def unfolding well_order_on_def linear_order_on_def
traytel@54980
  1734
     partial_order_on_def antisym_def by auto
traytel@54980
  1735
     ultimately show "\<exists>j\<in>g ` A. i \<noteq> j \<and> (i, j) \<in> r" using a by auto
traytel@54980
  1736
   qed
traytel@54980
  1737
   ultimately have "|g ` A| =o r" using reg unfolding regular_def by auto
traytel@54980
  1738
   moreover have "|g ` A| \<le>o |A|" by (metis card_of_image)
traytel@54980
  1739
   ultimately have False using A by (metis not_ordLess_ordIso ordLeq_ordLess_trans)
traytel@54980
  1740
  }
traytel@54980
  1741
  thus "|Sigma A F| <o r"
traytel@54980
  1742
  using cr not_ordLess_iff_ordLeq by (metis card_of_Well_order card_order_on_well_order_on)
traytel@54980
  1743
qed
traytel@54980
  1744
traytel@54980
  1745
lemma stable_regular:
traytel@54980
  1746
assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and st: "stable r"
traytel@54980
  1747
shows "regular r"
traytel@54980
  1748
unfolding regular_def proof safe
traytel@54980
  1749
  fix K assume K: "K \<subseteq> Field r" and cof: "cofinal K r"
traytel@54980
  1750
  have "|K| \<le>o r" using K by (metis card_of_Field_ordIso card_of_mono1 cr ordLeq_ordIso_trans)
traytel@54980
  1751
  moreover
traytel@54980
  1752
  {assume Kr: "|K| <o r"
traytel@54980
  1753
   then obtain f where "\<forall> a \<in> Field r. f a \<in> K \<and> a \<noteq> f a \<and> (a, f a) \<in> r"
traytel@54980
  1754
   using cof unfolding cofinal_def by metis
traytel@54980
  1755
   hence "Field r \<subseteq> (\<Union> a \<in> K. underS r a)" unfolding rel.underS_def by auto
traytel@54980
  1756
   hence "r \<le>o |\<Union> a \<in> K. underS r a|" using cr
traytel@54980
  1757
   by (metis Card_order_iff_ordLeq_card_of card_of_mono1 ordLeq_transitive)
traytel@54980
  1758
   also have "|\<Union> a \<in> K. underS r a| \<le>o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma)
traytel@54980
  1759
   also
traytel@54980
  1760
   {have "\<forall> a \<in> K. |underS r a| <o r" using K by (metis card_of_underS cr subsetD)
traytel@54980
  1761
    hence "|SIGMA a: K. underS r a| <o r" using st Kr unfolding stable_def by auto
traytel@54980
  1762
   }
traytel@54980
  1763
   finally have "r <o r" .
traytel@54980
  1764
   hence False by (metis ordLess_irreflexive)
traytel@54980
  1765
  }
traytel@54980
  1766
  ultimately show "|K| =o r" by (metis ordLeq_iff_ordLess_or_ordIso)
traytel@54980
  1767
qed
traytel@54980
  1768
traytel@54980
  1769
(* Note that below the types of A and F are now unconstrained: *)
traytel@54980
  1770
lemma stable_elim:
traytel@54980
  1771
assumes ST: "stable r" and A_LESS: "|A| <o r" and
traytel@54980
  1772
        F_LESS: "\<And> a. a \<in> A \<Longrightarrow> |F a| <o r"
traytel@54980
  1773
shows "|SIGMA a : A. F a| <o r"
traytel@54980
  1774
proof-
traytel@54980
  1775
  obtain A' where 1: "A' < Field r \<and> |A'| <o r" and 2: " |A| =o |A'|"
traytel@54980
  1776
  using internalize_card_of_ordLess[of A r] A_LESS by blast
traytel@54980
  1777
  then obtain G where 3: "bij_betw G A' A"
traytel@54980
  1778
  using card_of_ordIso  ordIso_symmetric by blast
traytel@54980
  1779
  (*  *)
traytel@54980
  1780
  {fix a assume "a \<in> A"
traytel@54980
  1781
   hence "\<exists>B'. B' \<le> Field r \<and> |F a| =o |B'| \<and> |B'| <o r"
traytel@54980
  1782
   using internalize_card_of_ordLess[of "F a" r] F_LESS by blast
traytel@54980
  1783
  }
traytel@54980
  1784
  then obtain F' where
traytel@54980
  1785
  temp: "\<forall>a \<in> A. F' a \<le> Field r \<and> |F a| =o |F' a| \<and> |F' a| <o r"
traytel@54980
  1786
  using bchoice[of A "\<lambda> a B'. B' \<le> Field r \<and> |F a| =o |B'| \<and> |B'| <o r"] by blast
traytel@54980
  1787
  hence 4: "\<forall>a \<in> A. F' a \<le> Field r \<and> |F' a| <o r" by auto
traytel@54980
  1788
  have 5: "\<forall>a \<in> A. |F' a| =o |F a|" using temp ordIso_symmetric by auto
traytel@54980
  1789
  (*  *)
traytel@54980
  1790
  have "\<forall>a' \<in> A'. F'(G a') \<le> Field r \<and> |F'(G a')| <o r"
traytel@54980
  1791
  using 3 4 bij_betw_ball[of G A' A] by auto
traytel@54980
  1792
  hence "|SIGMA a' : A'. F'(G a')| <o r"
traytel@54980
  1793
  using ST 1 unfolding stable_def by auto
traytel@54980
  1794
  moreover have "|SIGMA a' : A'. F'(G a')| =o |SIGMA a : A. F a|"
traytel@54980
  1795
  using card_of_Sigma_cong[of G A' A F' F] 5 3 by blast
traytel@54980
  1796
  ultimately show ?thesis using ordIso_symmetric ordIso_ordLess_trans by blast
traytel@54980
  1797
qed
traytel@54980
  1798
traytel@54980
  1799
lemma stable_natLeq: "stable natLeq"
traytel@54980
  1800
proof(unfold stable_def, safe)
traytel@54980
  1801
  fix A :: "'a set" and F :: "'a \<Rightarrow> 'a set"
traytel@54980
  1802
  assume "|A| <o natLeq" and "\<forall>a\<in>A. |F a| <o natLeq"
traytel@54980
  1803
  hence "finite A \<and> (\<forall>a \<in> A. finite(F a))"
traytel@54980
  1804
  by (auto simp add: finite_iff_ordLess_natLeq)
traytel@54980
  1805
  hence "finite(Sigma A F)" by (simp only: finite_SigmaI[of A F])
traytel@54980
  1806
  thus "|Sigma A F | <o natLeq"
traytel@54980
  1807
  by (auto simp add: finite_iff_ordLess_natLeq)
traytel@54980
  1808
qed
traytel@54980
  1809
traytel@54980
  1810
corollary regular_natLeq: "regular natLeq"
traytel@54980
  1811
using stable_regular[OF natLeq_Card_order _ stable_natLeq] Field_natLeq by simp
traytel@54980
  1812
traytel@54980
  1813
lemma stable_cardSuc:
traytel@54980
  1814
assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"
traytel@54980
  1815
shows "stable(cardSuc r)"
traytel@54980
  1816
using infinite_cardSuc_regular regular_stable
traytel@54980
  1817
by (metis CARD INF cardSuc_Card_order cardSuc_finite)
traytel@54980
  1818
traytel@54980
  1819
lemma stable_UNION:
traytel@54980
  1820
assumes ST: "stable r" and A_LESS: "|A| <o r" and
traytel@54980
  1821
        F_LESS: "\<And> a. a \<in> A \<Longrightarrow> |F a| <o r"
traytel@54980
  1822
shows "|\<Union> a \<in> A. F a| <o r"
traytel@54980
  1823
proof-
traytel@54980
  1824
  have "|\<Union> a \<in> A. F a| \<le>o |SIGMA a : A. F a|"
traytel@54980
  1825
  using card_of_UNION_Sigma by blast
traytel@54980
  1826
  thus ?thesis using assms stable_elim ordLeq_ordLess_trans by blast
traytel@54980
  1827
qed
traytel@54980
  1828
traytel@54980
  1829
lemma stable_ordIso1:
traytel@54980
  1830
assumes ST: "stable r" and ISO: "r' =o r"
traytel@54980
  1831
shows "stable r'"
traytel@54980
  1832
proof(unfold stable_def, auto)
traytel@54980
  1833
  fix A::"'b set" and F::"'b \<Rightarrow> 'b set"
traytel@54980
  1834
  assume "|A| <o r'" and "\<forall>a \<in> A. |F a| <o r'"
traytel@54980
  1835
  hence "( |A| <o r) \<and> (\<forall>a \<in> A. |F a| <o r)"
traytel@54980
  1836
  using ISO ordLess_ordIso_trans by blast
traytel@54980
  1837
  hence "|SIGMA a : A. F a| <o r" using assms stable_elim by blast
traytel@54980
  1838
  thus "|SIGMA a : A. F a| <o r'"
traytel@54980
  1839
  using ISO ordIso_symmetric ordLess_ordIso_trans by blast
traytel@54980
  1840
qed
traytel@54980
  1841
traytel@54980
  1842
lemma stable_ordIso2:
traytel@54980
  1843
assumes ST: "stable r" and ISO: "r =o r'"
traytel@54980
  1844
shows "stable r'"
traytel@54980
  1845
using assms stable_ordIso1 ordIso_symmetric by blast
traytel@54980
  1846
traytel@54980
  1847
lemma stable_ordIso:
traytel@54980
  1848
assumes "r =o r'"
traytel@54980
  1849
shows "stable r = stable r'"
traytel@54980
  1850
using assms stable_ordIso1 stable_ordIso2 by blast
traytel@54980
  1851
traytel@54980
  1852
lemma stable_nat: "stable |UNIV::nat set|"
traytel@54980
  1853
using stable_natLeq card_of_nat stable_ordIso by auto
traytel@54980
  1854
traytel@54980
  1855
text{* Below, the type of "A" is not important -- we just had to choose an appropriate
traytel@54980
  1856
   type to make "A" possible. What is important is that arbitrarily large
haftmann@54989
  1857
   infinite sets of stable cardinality exist. *}
traytel@54980
  1858
traytel@54980
  1859
lemma infinite_stable_exists:
traytel@54980
  1860
assumes CARD: "\<forall>r \<in> R. Card_order (r::'a rel)"
traytel@54980
  1861
shows "\<exists>(A :: (nat + 'a set)set).
traytel@54980
  1862
          \<not>finite A \<and> stable |A| \<and> (\<forall>r \<in> R. r <o |A| )"
traytel@54980
  1863
proof-
traytel@54980
  1864
  have "\<exists>(A :: (nat + 'a set)set).
traytel@54980
  1865
          \<not>finite A \<and> stable |A| \<and> |UNIV::'a set| <o |A|"
traytel@54980
  1866
  proof(cases "finite (UNIV::'a set)")
traytel@54980
  1867
    assume Case1: "finite (UNIV::'a set)"
traytel@54980
  1868
    let ?B = "UNIV::nat set"
traytel@54980
  1869
    have "\<not>finite(?B <+> {})" using finite_Plus_iff by blast
traytel@54980
  1870
    moreover
traytel@54980
  1871
    have "stable |?B|" using stable_natLeq card_of_nat stable_ordIso1 by blast
traytel@54980
  1872
    hence "stable |?B <+> {}|" using stable_ordIso card_of_Plus_empty1 by blast
traytel@54980
  1873
    moreover
traytel@54980
  1874
    have "\<not>finite(Field |?B| ) \<and> finite(Field |UNIV::'a set| )" using Case1 by simp
traytel@54980
  1875
    hence "|UNIV::'a set| <o |?B|" by (simp add: finite_ordLess_infinite)
traytel@54980
  1876
    hence "|UNIV::'a set| <o |?B <+> {}|" using card_of_Plus_empty1 ordLess_ordIso_trans by blast
traytel@54980
  1877
    ultimately show ?thesis by blast
traytel@54980
  1878
  next
traytel@54980
  1879
    assume Case1: "\<not>finite (UNIV::'a set)"
traytel@54980
  1880
    hence *: "\<not>finite(Field |UNIV::'a set| )" by simp
traytel@54980
  1881
    let ?B = "Field(cardSuc |UNIV::'a set| )"
traytel@54980
  1882
    have 0: "|?B| =o |{} <+> ?B|" using card_of_Plus_empty2 by blast
traytel@54980
  1883
    have 1: "\<not>finite ?B" using Case1 card_of_cardSuc_finite by blast
traytel@54980
  1884
    hence 2: "\<not>finite({} <+> ?B)" using 0 card_of_ordIso_finite by blast
traytel@54980
  1885
    have "|?B| =o cardSuc |UNIV::'a set|"
traytel@54980
  1886
    using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast
traytel@54980
  1887
    moreover have "stable(cardSuc |UNIV::'a set| )"
traytel@54980
  1888
    using stable_cardSuc * card_of_Card_order by blast
traytel@54980
  1889
    ultimately have "stable |?B|" using stable_ordIso by blast
traytel@54980
  1890
    hence 3: "stable |{} <+> ?B|" using stable_ordIso 0 by blast
traytel@54980
  1891
    have "|UNIV::'a set| <o cardSuc |UNIV::'a set|"
traytel@54980
  1892
    using card_of_Card_order cardSuc_greater by blast
traytel@54980
  1893
    moreover have "|?B| =o  cardSuc |UNIV::'a set|"
traytel@54980
  1894
    using card_of_Card_order cardSuc_Card_order  card_of_Field_ordIso by blast
traytel@54980
  1895
    ultimately have "|UNIV::'a set| <o |?B|"
traytel@54980
  1896
    using ordIso_symmetric ordLess_ordIso_trans by blast
traytel@54980
  1897
    hence "|UNIV::'a set| <o |{} <+> ?B|" using 0 ordLess_ordIso_trans by blast
traytel@54980
  1898
    thus ?thesis using 2 3 by blast
traytel@54980
  1899
  qed
traytel@54980
  1900
  thus ?thesis using CARD card_of_UNIV2 ordLeq_ordLess_trans by blast
traytel@54980
  1901
qed
traytel@54980
  1902
traytel@54980
  1903
corollary infinite_regular_exists:
traytel@54980
  1904
assumes CARD: "\<forall>r \<in> R. Card_order (r::'a rel)"
traytel@54980
  1905
shows "\<exists>(A :: (nat + 'a set)set).
traytel@54980
  1906
          \<not>finite A \<and> regular |A| \<and> (\<forall>r \<in> R. r <o |A| )"
traytel@54980
  1907
using infinite_stable_exists[OF CARD] stable_regular by (metis Field_card_of card_of_card_order_on)
traytel@54980
  1908
blanchet@48975
  1909
end