src/HOL/Cardinals/Cardinal_Order_Relation.thy
author traytel
Fri Jul 05 18:10:07 2013 +0200 (2013-07-05)
changeset 52544 0c4b140cff00
parent 51764 67f05cb13e08
child 52545 d2ad6eae514f
permissions -rw-r--r--
tuned spelling
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@48979
    11
imports Cardinal_Order_Relation_Base 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_set_type[simp]
blanchet@48975
    38
  card_of_Plus1[simp]
blanchet@48975
    39
  Card_order_Plus1[simp]
blanchet@48975
    40
  card_of_Plus2[simp]
blanchet@48975
    41
  Card_order_Plus2[simp]
blanchet@48975
    42
  card_of_Plus_mono1[simp]
blanchet@48975
    43
  card_of_Plus_mono2[simp]
blanchet@48975
    44
  card_of_Plus_mono[simp]
blanchet@48975
    45
  card_of_Plus_cong2[simp]
blanchet@48975
    46
  card_of_Plus_cong[simp]
blanchet@48975
    47
  card_of_Un1[simp]
blanchet@48975
    48
  card_of_diff[simp]
blanchet@48975
    49
  card_of_Un_Plus_ordLeq[simp]
blanchet@48975
    50
  card_of_Times1[simp]
blanchet@48975
    51
  card_of_Times2[simp]
blanchet@48975
    52
  card_of_Times3[simp]
blanchet@48975
    53
  card_of_Times_mono1[simp]
blanchet@48975
    54
  card_of_Times_mono2[simp]
blanchet@48975
    55
  card_of_Times_cong1[simp]
blanchet@48975
    56
  card_of_Times_cong2[simp]
blanchet@48975
    57
  card_of_ordIso_finite[simp]
blanchet@48975
    58
  finite_ordLess_infinite2[simp]
blanchet@48975
    59
  card_of_Times_same_infinite[simp]
blanchet@48975
    60
  card_of_Times_infinite_simps[simp]
blanchet@48975
    61
  card_of_Plus_infinite1[simp]
blanchet@48975
    62
  card_of_Plus_infinite2[simp]
blanchet@48975
    63
  card_of_Plus_ordLess_infinite[simp]
blanchet@48975
    64
  card_of_Plus_ordLess_infinite_Field[simp]
blanchet@48975
    65
  card_of_lists_infinite[simp]
blanchet@48975
    66
  infinite_cartesian_product[simp]
blanchet@48975
    67
  cardSuc_Card_order[simp]
blanchet@48975
    68
  cardSuc_greater[simp]
blanchet@48975
    69
  cardSuc_ordLeq[simp]
blanchet@48975
    70
  cardSuc_ordLeq_ordLess[simp]
blanchet@48975
    71
  cardSuc_mono_ordLeq[simp]
blanchet@48975
    72
  cardSuc_invar_ordIso[simp]
blanchet@48975
    73
  card_of_cardSuc_finite[simp]
blanchet@48975
    74
  cardSuc_finite[simp]
blanchet@48975
    75
  card_of_Plus_ordLeq_infinite_Field[simp]
blanchet@48975
    76
  curr_in[intro, simp]
blanchet@48975
    77
  Func_empty[simp]
blanchet@48975
    78
  Func_map_empty[simp]
blanchet@48975
    79
  Func_is_emp[simp]
blanchet@48975
    80
blanchet@48975
    81
blanchet@48975
    82
subsection {* Cardinal of a set *}
blanchet@48975
    83
blanchet@48975
    84
lemma card_of_inj_rel: assumes INJ: "!! x y y'. \<lbrakk>(x,y) : R; (x,y') : R\<rbrakk> \<Longrightarrow> y = y'"
blanchet@48975
    85
shows "|{y. EX x. (x,y) : R}| <=o |{x. EX y. (x,y) : R}|"
blanchet@48975
    86
proof-
blanchet@48975
    87
  let ?Y = "{y. EX x. (x,y) : R}"  let ?X = "{x. EX y. (x,y) : R}"
blanchet@48975
    88
  let ?f = "% y. SOME x. (x,y) : R"
traytel@51764
    89
  have "?f ` ?Y <= ?X" by (auto dest: someI)
blanchet@48975
    90
  moreover have "inj_on ?f ?Y"
blanchet@48975
    91
  unfolding inj_on_def proof(auto)
blanchet@48975
    92
    fix y1 x1 y2 x2
blanchet@48975
    93
    assume *: "(x1, y1) \<in> R" "(x2, y2) \<in> R" and **: "?f y1 = ?f y2"
blanchet@48975
    94
    hence "(?f y1,y1) : R" using someI[of "% x. (x,y1) : R"] by auto
blanchet@48975
    95
    moreover have "(?f y2,y2) : R" using * someI[of "% x. (x,y2) : R"] by auto
blanchet@48975
    96
    ultimately show "y1 = y2" using ** INJ by auto
blanchet@48975
    97
  qed
blanchet@48975
    98
  ultimately show "|?Y| <=o |?X|" using card_of_ordLeq by blast
blanchet@48975
    99
qed
blanchet@48975
   100
blanchet@48975
   101
lemma card_of_unique2: "\<lbrakk>card_order_on B r; bij_betw f A B\<rbrakk> \<Longrightarrow> r =o |A|"
blanchet@48975
   102
using card_of_ordIso card_of_unique ordIso_equivalence by blast
blanchet@48975
   103
blanchet@48975
   104
lemma internalize_card_of_ordLess:
blanchet@48975
   105
"( |A| <o r) = (\<exists>B < Field r. |A| =o |B| \<and> |B| <o r)"
blanchet@48975
   106
proof
blanchet@48975
   107
  assume "|A| <o r"
blanchet@48975
   108
  then obtain p where 1: "Field p < Field r \<and> |A| =o p \<and> p <o r"
blanchet@48975
   109
  using internalize_ordLess[of "|A|" r] by blast
blanchet@48975
   110
  hence "Card_order p" using card_of_Card_order Card_order_ordIso2 by blast
blanchet@48975
   111
  hence "|Field p| =o p" using card_of_Field_ordIso by blast
blanchet@48975
   112
  hence "|A| =o |Field p| \<and> |Field p| <o r"
blanchet@48975
   113
  using 1 ordIso_equivalence ordIso_ordLess_trans by blast
blanchet@48975
   114
  thus "\<exists>B < Field r. |A| =o |B| \<and> |B| <o r" using 1 by blast
blanchet@48975
   115
next
blanchet@48975
   116
  assume "\<exists>B < Field r. |A| =o |B| \<and> |B| <o r"
blanchet@48975
   117
  thus "|A| <o r" using ordIso_ordLess_trans by blast
blanchet@48975
   118
qed
blanchet@48975
   119
blanchet@48975
   120
lemma internalize_card_of_ordLess2:
blanchet@48975
   121
"( |A| <o |C| ) = (\<exists>B < C. |A| =o |B| \<and> |B| <o |C| )"
blanchet@48975
   122
using internalize_card_of_ordLess[of "A" "|C|"] Field_card_of[of C] by auto
blanchet@48975
   123
blanchet@48975
   124
lemma Card_order_omax:
blanchet@48975
   125
assumes "finite R" and "R \<noteq> {}" and "\<forall>r\<in>R. Card_order r"
blanchet@48975
   126
shows "Card_order (omax R)"
blanchet@48975
   127
proof-
blanchet@48975
   128
  have "\<forall>r\<in>R. Well_order r"
blanchet@48975
   129
  using assms unfolding card_order_on_def by simp
blanchet@48975
   130
  thus ?thesis using assms apply - apply(drule omax_in) by auto
blanchet@48975
   131
qed
blanchet@48975
   132
blanchet@48975
   133
lemma Card_order_omax2:
blanchet@48975
   134
assumes "finite I" and "I \<noteq> {}"
blanchet@48975
   135
shows "Card_order (omax {|A i| | i. i \<in> I})"
blanchet@48975
   136
proof-
blanchet@48975
   137
  let ?R = "{|A i| | i. i \<in> I}"
blanchet@48975
   138
  have "finite ?R" and "?R \<noteq> {}" using assms by auto
blanchet@48975
   139
  moreover have "\<forall>r\<in>?R. Card_order r"
blanchet@48975
   140
  using card_of_Card_order by auto
blanchet@48975
   141
  ultimately show ?thesis by(rule Card_order_omax)
blanchet@48975
   142
qed
blanchet@48975
   143
blanchet@48975
   144
blanchet@48975
   145
subsection {* Cardinals versus set operations on arbitrary sets *}
blanchet@48975
   146
blanchet@48975
   147
lemma subset_ordLeq_strict:
blanchet@48975
   148
assumes "A \<le> B" and "|A| <o |B|"
blanchet@48975
   149
shows "A < B"
blanchet@48975
   150
proof-
blanchet@48975
   151
  {assume "\<not>(A < B)"
blanchet@48975
   152
   hence "A = B" using assms(1) by blast
blanchet@48975
   153
   hence False using assms(2) not_ordLess_ordIso card_of_refl by blast
blanchet@48975
   154
  }
blanchet@48975
   155
  thus ?thesis by blast
blanchet@48975
   156
qed
blanchet@48975
   157
blanchet@48975
   158
corollary subset_ordLeq_diff:
blanchet@48975
   159
assumes "A \<le> B" and "|A| <o |B|"
blanchet@48975
   160
shows "B - A \<noteq> {}"
blanchet@48975
   161
using assms subset_ordLeq_strict by blast
blanchet@48975
   162
blanchet@48975
   163
lemma card_of_empty4:
blanchet@48975
   164
"|{}::'b set| <o |A::'a set| = (A \<noteq> {})"
blanchet@48975
   165
proof(intro iffI notI)
blanchet@48975
   166
  assume *: "|{}::'b set| <o |A|" and "A = {}"
blanchet@48975
   167
  hence "|A| =o |{}::'b set|"
blanchet@48975
   168
  using card_of_ordIso unfolding bij_betw_def inj_on_def by blast
blanchet@48975
   169
  hence "|{}::'b set| =o |A|" using ordIso_symmetric by blast
blanchet@48975
   170
  with * show False using not_ordLess_ordIso[of "|{}::'b set|" "|A|"] by blast
blanchet@48975
   171
next
blanchet@48975
   172
  assume "A \<noteq> {}"
blanchet@48975
   173
  hence "(\<not> (\<exists>f. inj_on f A \<and> f ` A \<subseteq> {}))"
blanchet@48975
   174
  unfolding inj_on_def by blast
blanchet@48975
   175
  thus "| {} | <o | A |"
blanchet@48975
   176
  using card_of_ordLess by blast
blanchet@48975
   177
qed
blanchet@48975
   178
blanchet@48975
   179
lemma card_of_empty5:
blanchet@48975
   180
"|A| <o |B| \<Longrightarrow> B \<noteq> {}"
blanchet@48975
   181
using card_of_empty not_ordLess_ordLeq by blast
blanchet@48975
   182
blanchet@48975
   183
lemma Well_order_card_of_empty:
blanchet@48975
   184
"Well_order r \<Longrightarrow> |{}| \<le>o r" by simp
blanchet@48975
   185
blanchet@48975
   186
lemma card_of_UNIV[simp]:
blanchet@48975
   187
"|A :: 'a set| \<le>o |UNIV :: 'a set|"
blanchet@48975
   188
using card_of_mono1[of A] by simp
blanchet@48975
   189
blanchet@48975
   190
lemma card_of_UNIV2[simp]:
blanchet@48975
   191
"Card_order r \<Longrightarrow> (r :: 'a rel) \<le>o |UNIV :: 'a set|"
blanchet@48975
   192
using card_of_UNIV[of "Field r"] card_of_Field_ordIso
blanchet@48975
   193
      ordIso_symmetric ordIso_ordLeq_trans by blast
blanchet@48975
   194
blanchet@48975
   195
lemma card_of_Pow_mono[simp]:
blanchet@48975
   196
assumes "|A| \<le>o |B|"
blanchet@48975
   197
shows "|Pow A| \<le>o |Pow B|"
blanchet@48975
   198
proof-
blanchet@48975
   199
  obtain f where "inj_on f A \<and> f ` A \<le> B"
blanchet@48975
   200
  using assms card_of_ordLeq[of A B] by auto
blanchet@48975
   201
  hence "inj_on (image f) (Pow A) \<and> (image f) ` (Pow A) \<le> (Pow B)"
blanchet@48975
   202
  by (auto simp add: inj_on_image_Pow image_Pow_mono)
blanchet@48975
   203
  thus ?thesis using card_of_ordLeq[of "Pow A"] by metis
blanchet@48975
   204
qed
blanchet@48975
   205
blanchet@48975
   206
lemma ordIso_Pow_mono[simp]:
blanchet@48975
   207
assumes "r \<le>o r'"
blanchet@48975
   208
shows "|Pow(Field r)| \<le>o |Pow(Field r')|"
blanchet@48975
   209
using assms card_of_mono2 card_of_Pow_mono by blast
blanchet@48975
   210
blanchet@48975
   211
lemma card_of_Pow_cong[simp]:
blanchet@48975
   212
assumes "|A| =o |B|"
blanchet@48975
   213
shows "|Pow A| =o |Pow B|"
blanchet@48975
   214
proof-
blanchet@48975
   215
  obtain f where "bij_betw f A B"
blanchet@48975
   216
  using assms card_of_ordIso[of A B] by auto
blanchet@48975
   217
  hence "bij_betw (image f) (Pow A) (Pow B)"
blanchet@48975
   218
  by (auto simp add: bij_betw_image_Pow)
blanchet@48975
   219
  thus ?thesis using card_of_ordIso[of "Pow A"] by auto
blanchet@48975
   220
qed
blanchet@48975
   221
blanchet@48975
   222
lemma ordIso_Pow_cong[simp]:
blanchet@48975
   223
assumes "r =o r'"
blanchet@48975
   224
shows "|Pow(Field r)| =o |Pow(Field r')|"
blanchet@48975
   225
using assms card_of_cong card_of_Pow_cong by blast
blanchet@48975
   226
blanchet@48975
   227
corollary Card_order_Plus_empty1:
blanchet@48975
   228
"Card_order r \<Longrightarrow> r =o |(Field r) <+> {}|"
blanchet@48975
   229
using card_of_Plus_empty1 card_of_Field_ordIso ordIso_equivalence by blast
blanchet@48975
   230
blanchet@48975
   231
corollary Card_order_Plus_empty2:
blanchet@48975
   232
"Card_order r \<Longrightarrow> r =o |{} <+> (Field r)|"
blanchet@48975
   233
using card_of_Plus_empty2 card_of_Field_ordIso ordIso_equivalence by blast
blanchet@48975
   234
blanchet@48975
   235
lemma Card_order_Un1:
blanchet@48975
   236
shows "Card_order r \<Longrightarrow> |Field r| \<le>o |(Field r) \<union> B| "
blanchet@48975
   237
using card_of_Un1 card_of_Field_ordIso ordIso_symmetric ordIso_ordLeq_trans by auto
blanchet@48975
   238
blanchet@48975
   239
lemma card_of_Un2[simp]:
blanchet@48975
   240
shows "|A| \<le>o |B \<union> A|"
blanchet@48975
   241
using inj_on_id[of A] card_of_ordLeq[of A _] by fastforce
blanchet@48975
   242
blanchet@48975
   243
lemma Card_order_Un2:
blanchet@48975
   244
shows "Card_order r \<Longrightarrow> |Field r| \<le>o |A \<union> (Field r)| "
blanchet@48975
   245
using card_of_Un2 card_of_Field_ordIso ordIso_symmetric ordIso_ordLeq_trans by auto
blanchet@48975
   246
blanchet@48975
   247
lemma Un_Plus_bij_betw:
blanchet@48975
   248
assumes "A Int B = {}"
blanchet@48975
   249
shows "\<exists>f. bij_betw f (A \<union> B) (A <+> B)"
blanchet@48975
   250
proof-
blanchet@48975
   251
  let ?f = "\<lambda> c. if c \<in> A then Inl c else Inr c"
blanchet@48975
   252
  have "bij_betw ?f (A \<union> B) (A <+> B)"
blanchet@48975
   253
  using assms by(unfold bij_betw_def inj_on_def, auto)
blanchet@48975
   254
  thus ?thesis by blast
blanchet@48975
   255
qed
blanchet@48975
   256
blanchet@48975
   257
lemma card_of_Un_Plus_ordIso:
blanchet@48975
   258
assumes "A Int B = {}"
blanchet@48975
   259
shows "|A \<union> B| =o |A <+> B|"
blanchet@48975
   260
using assms card_of_ordIso[of "A \<union> B"] Un_Plus_bij_betw[of A B] by auto
blanchet@48975
   261
blanchet@48975
   262
lemma card_of_Un_Plus_ordIso1:
blanchet@48975
   263
"|A \<union> B| =o |A <+> (B - A)|"
blanchet@48975
   264
using card_of_Un_Plus_ordIso[of A "B - A"] by auto
blanchet@48975
   265
blanchet@48975
   266
lemma card_of_Un_Plus_ordIso2:
blanchet@48975
   267
"|A \<union> B| =o |(A - B) <+> B|"
blanchet@48975
   268
using card_of_Un_Plus_ordIso[of "A - B" B] by auto
blanchet@48975
   269
blanchet@48975
   270
lemma card_of_Times_singl1: "|A| =o |A \<times> {b}|"
blanchet@48975
   271
proof-
blanchet@48975
   272
  have "bij_betw fst (A \<times> {b}) A" unfolding bij_betw_def inj_on_def by force
blanchet@48975
   273
  thus ?thesis using card_of_ordIso ordIso_symmetric by blast
blanchet@48975
   274
qed
blanchet@48975
   275
blanchet@48975
   276
corollary Card_order_Times_singl1:
blanchet@48975
   277
"Card_order r \<Longrightarrow> r =o |(Field r) \<times> {b}|"
blanchet@48975
   278
using card_of_Times_singl1[of _ b] card_of_Field_ordIso ordIso_equivalence by blast
blanchet@48975
   279
blanchet@48975
   280
lemma card_of_Times_singl2: "|A| =o |{b} \<times> A|"
blanchet@48975
   281
proof-
blanchet@48975
   282
  have "bij_betw snd ({b} \<times> A) A" unfolding bij_betw_def inj_on_def by force
blanchet@48975
   283
  thus ?thesis using card_of_ordIso ordIso_symmetric by blast
blanchet@48975
   284
qed
blanchet@48975
   285
blanchet@48975
   286
corollary Card_order_Times_singl2:
blanchet@48975
   287
"Card_order r \<Longrightarrow> r =o |{a} \<times> (Field r)|"
blanchet@48975
   288
using card_of_Times_singl2[of _ a] card_of_Field_ordIso ordIso_equivalence by blast
blanchet@48975
   289
blanchet@48975
   290
lemma card_of_Times_assoc: "|(A \<times> B) \<times> C| =o |A \<times> B \<times> C|"
blanchet@48975
   291
proof -
blanchet@48975
   292
  let ?f = "\<lambda>((a,b),c). (a,(b,c))"
blanchet@48975
   293
  have "A \<times> B \<times> C \<subseteq> ?f ` ((A \<times> B) \<times> C)"
blanchet@48975
   294
  proof
blanchet@48975
   295
    fix x assume "x \<in> A \<times> B \<times> C"
blanchet@48975
   296
    then obtain a b c where *: "a \<in> A" "b \<in> B" "c \<in> C" "x = (a, b, c)" by blast
blanchet@48975
   297
    let ?x = "((a, b), c)"
blanchet@48975
   298
    from * have "?x \<in> (A \<times> B) \<times> C" "x = ?f ?x" by auto
blanchet@48975
   299
    thus "x \<in> ?f ` ((A \<times> B) \<times> C)" by blast
blanchet@48975
   300
  qed
blanchet@48975
   301
  hence "bij_betw ?f ((A \<times> B) \<times> C) (A \<times> B \<times> C)"
blanchet@48975
   302
  unfolding bij_betw_def inj_on_def by auto
blanchet@48975
   303
  thus ?thesis using card_of_ordIso by blast
blanchet@48975
   304
qed
blanchet@48975
   305
blanchet@48975
   306
corollary Card_order_Times3:
blanchet@48975
   307
"Card_order r \<Longrightarrow> |Field r| \<le>o |(Field r) \<times> (Field r)|"
blanchet@48975
   308
using card_of_Times3 card_of_Field_ordIso
blanchet@48975
   309
      ordIso_ordLeq_trans ordIso_symmetric by blast
blanchet@48975
   310
blanchet@48975
   311
lemma card_of_Times_mono[simp]:
blanchet@48975
   312
assumes "|A| \<le>o |B|" and "|C| \<le>o |D|"
blanchet@48975
   313
shows "|A \<times> C| \<le>o |B \<times> D|"
blanchet@48975
   314
using assms card_of_Times_mono1[of A B C] card_of_Times_mono2[of C D B]
blanchet@48975
   315
      ordLeq_transitive[of "|A \<times> C|"] by blast
blanchet@48975
   316
blanchet@48975
   317
corollary ordLeq_Times_mono:
blanchet@48975
   318
assumes "r \<le>o r'" and "p \<le>o p'"
blanchet@48975
   319
shows "|(Field r) \<times> (Field p)| \<le>o |(Field r') \<times> (Field p')|"
blanchet@48975
   320
using assms card_of_mono2[of r r'] card_of_mono2[of p p'] card_of_Times_mono by blast
blanchet@48975
   321
blanchet@48975
   322
corollary ordIso_Times_cong1[simp]:
blanchet@48975
   323
assumes "r =o r'"
blanchet@48975
   324
shows "|(Field r) \<times> C| =o |(Field r') \<times> C|"
blanchet@48975
   325
using assms card_of_cong card_of_Times_cong1 by blast
blanchet@48975
   326
blanchet@48975
   327
lemma card_of_Times_cong[simp]:
blanchet@48975
   328
assumes "|A| =o |B|" and "|C| =o |D|"
blanchet@48975
   329
shows "|A \<times> C| =o |B \<times> D|"
blanchet@48975
   330
using assms
blanchet@48975
   331
by (auto simp add: ordIso_iff_ordLeq)
blanchet@48975
   332
blanchet@48975
   333
corollary ordIso_Times_cong:
blanchet@48975
   334
assumes "r =o r'" and "p =o p'"
blanchet@48975
   335
shows "|(Field r) \<times> (Field p)| =o |(Field r') \<times> (Field p')|"
blanchet@48975
   336
using assms card_of_cong[of r r'] card_of_cong[of p p'] card_of_Times_cong by blast
blanchet@48975
   337
blanchet@48975
   338
lemma card_of_Sigma_mono2:
blanchet@48975
   339
assumes "inj_on f (I::'i set)" and "f ` I \<le> (J::'j set)"
blanchet@48975
   340
shows "|SIGMA i : I. (A::'j \<Rightarrow> 'a set) (f i)| \<le>o |SIGMA j : J. A j|"
blanchet@48975
   341
proof-
blanchet@48975
   342
  let ?LEFT = "SIGMA i : I. A (f i)"
blanchet@48975
   343
  let ?RIGHT = "SIGMA j : J. A j"
blanchet@48975
   344
  obtain u where u_def: "u = (\<lambda>(i::'i,a::'a). (f i,a))" by blast
blanchet@48975
   345
  have "inj_on u ?LEFT \<and> u `?LEFT \<le> ?RIGHT"
blanchet@48975
   346
  using assms unfolding u_def inj_on_def by auto
blanchet@48975
   347
  thus ?thesis using card_of_ordLeq by blast
blanchet@48975
   348
qed
blanchet@48975
   349
blanchet@48975
   350
lemma card_of_Sigma_mono:
blanchet@48975
   351
assumes INJ: "inj_on f I" and IM: "f ` I \<le> J" and
blanchet@48975
   352
        LEQ: "\<forall>j \<in> J. |A j| \<le>o |B j|"
blanchet@48975
   353
shows "|SIGMA i : I. A (f i)| \<le>o |SIGMA j : J. B j|"
blanchet@48975
   354
proof-
blanchet@48975
   355
  have "\<forall>i \<in> I. |A(f i)| \<le>o |B(f i)|"
blanchet@48975
   356
  using IM LEQ by blast
blanchet@48975
   357
  hence "|SIGMA i : I. A (f i)| \<le>o |SIGMA i : I. B (f i)|"
blanchet@48975
   358
  using card_of_Sigma_mono1[of I] by metis
blanchet@48975
   359
  moreover have "|SIGMA i : I. B (f i)| \<le>o |SIGMA j : J. B j|"
blanchet@48975
   360
  using INJ IM card_of_Sigma_mono2 by blast
blanchet@48975
   361
  ultimately show ?thesis using ordLeq_transitive by blast
blanchet@48975
   362
qed
blanchet@48975
   363
blanchet@48975
   364
blanchet@48975
   365
lemma ordLeq_Sigma_mono1:
blanchet@48975
   366
assumes "\<forall>i \<in> I. p i \<le>o r i"
blanchet@48975
   367
shows "|SIGMA i : I. Field(p i)| \<le>o |SIGMA i : I. Field(r i)|"
blanchet@48975
   368
using assms by (auto simp add: card_of_Sigma_mono1)
blanchet@48975
   369
blanchet@48975
   370
blanchet@48975
   371
lemma ordLeq_Sigma_mono:
blanchet@48975
   372
assumes "inj_on f I" and "f ` I \<le> J" and
blanchet@48975
   373
        "\<forall>j \<in> J. p j \<le>o r j"
blanchet@48975
   374
shows "|SIGMA i : I. Field(p(f i))| \<le>o |SIGMA j : J. Field(r j)|"
blanchet@48975
   375
using assms card_of_mono2 card_of_Sigma_mono
blanchet@48975
   376
      [of f I J "\<lambda> i. Field(p i)" "\<lambda> j. Field(r j)"] by metis
blanchet@48975
   377
blanchet@48975
   378
blanchet@48975
   379
lemma card_of_Sigma_cong1:
blanchet@48975
   380
assumes "\<forall>i \<in> I. |A i| =o |B i|"
blanchet@48975
   381
shows "|SIGMA i : I. A i| =o |SIGMA i : I. B i|"
blanchet@48975
   382
using assms by (auto simp add: card_of_Sigma_mono1 ordIso_iff_ordLeq)
blanchet@48975
   383
blanchet@48975
   384
blanchet@48975
   385
lemma card_of_Sigma_cong2:
blanchet@48975
   386
assumes "bij_betw f (I::'i set) (J::'j set)"
blanchet@48975
   387
shows "|SIGMA i : I. (A::'j \<Rightarrow> 'a set) (f i)| =o |SIGMA j : J. A j|"
blanchet@48975
   388
proof-
blanchet@48975
   389
  let ?LEFT = "SIGMA i : I. A (f i)"
blanchet@48975
   390
  let ?RIGHT = "SIGMA j : J. A j"
blanchet@48975
   391
  obtain u where u_def: "u = (\<lambda>(i::'i,a::'a). (f i,a))" by blast
blanchet@48975
   392
  have "bij_betw u ?LEFT ?RIGHT"
blanchet@48975
   393
  using assms unfolding u_def bij_betw_def inj_on_def by auto
blanchet@48975
   394
  thus ?thesis using card_of_ordIso by blast
blanchet@48975
   395
qed
blanchet@48975
   396
blanchet@48975
   397
lemma card_of_Sigma_cong:
blanchet@48975
   398
assumes BIJ: "bij_betw f I J" and
blanchet@48975
   399
        ISO: "\<forall>j \<in> J. |A j| =o |B j|"
blanchet@48975
   400
shows "|SIGMA i : I. A (f i)| =o |SIGMA j : J. B j|"
blanchet@48975
   401
proof-
blanchet@48975
   402
  have "\<forall>i \<in> I. |A(f i)| =o |B(f i)|"
blanchet@48975
   403
  using ISO BIJ unfolding bij_betw_def by blast
blanchet@48975
   404
  hence "|SIGMA i : I. A (f i)| =o |SIGMA i : I. B (f i)|"
blanchet@48975
   405
  using card_of_Sigma_cong1 by metis
blanchet@48975
   406
  moreover have "|SIGMA i : I. B (f i)| =o |SIGMA j : J. B j|"
blanchet@48975
   407
  using BIJ card_of_Sigma_cong2 by blast
blanchet@48975
   408
  ultimately show ?thesis using ordIso_transitive by blast
blanchet@48975
   409
qed
blanchet@48975
   410
blanchet@48975
   411
lemma ordIso_Sigma_cong1:
blanchet@48975
   412
assumes "\<forall>i \<in> I. p i =o r i"
blanchet@48975
   413
shows "|SIGMA i : I. Field(p i)| =o |SIGMA i : I. Field(r i)|"
blanchet@48975
   414
using assms by (auto simp add: card_of_Sigma_cong1)
blanchet@48975
   415
blanchet@48975
   416
lemma ordLeq_Sigma_cong:
blanchet@48975
   417
assumes "bij_betw f I J" and
blanchet@48975
   418
        "\<forall>j \<in> J. p j =o r j"
blanchet@48975
   419
shows "|SIGMA i : I. Field(p(f i))| =o |SIGMA j : J. Field(r j)|"
blanchet@48975
   420
using assms card_of_cong card_of_Sigma_cong
blanchet@48975
   421
      [of f I J "\<lambda> j. Field(p j)" "\<lambda> j. Field(r j)"] by blast
blanchet@48975
   422
blanchet@48975
   423
corollary ordLeq_Sigma_Times:
blanchet@48975
   424
"\<forall>i \<in> I. p i \<le>o r \<Longrightarrow> |SIGMA i : I. Field (p i)| \<le>o |I \<times> (Field r)|"
blanchet@48975
   425
by (auto simp add: card_of_Sigma_Times)
blanchet@48975
   426
blanchet@48975
   427
lemma card_of_UNION_Sigma2:
blanchet@48975
   428
assumes
blanchet@48975
   429
"!! i j. \<lbrakk>{i,j} <= I; i ~= j\<rbrakk> \<Longrightarrow> A i Int A j = {}"
blanchet@48975
   430
shows
blanchet@48975
   431
"|\<Union>i\<in>I. A i| =o |Sigma I A|"
blanchet@48975
   432
proof-
blanchet@48975
   433
  let ?L = "\<Union>i\<in>I. A i"  let ?R = "Sigma I A"
blanchet@48975
   434
  have "|?L| <=o |?R|" using card_of_UNION_Sigma .
blanchet@48975
   435
  moreover have "|?R| <=o |?L|"
blanchet@48975
   436
  proof-
blanchet@48975
   437
    have "inj_on snd ?R"
blanchet@48975
   438
    unfolding inj_on_def using assms by auto
blanchet@48975
   439
    moreover have "snd ` ?R <= ?L" by auto
blanchet@48975
   440
    ultimately show ?thesis using card_of_ordLeq by blast
blanchet@48975
   441
  qed
blanchet@48975
   442
  ultimately show ?thesis by(simp add: ordIso_iff_ordLeq)
blanchet@48975
   443
qed
blanchet@48975
   444
blanchet@48975
   445
corollary Plus_into_Times:
blanchet@48975
   446
assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and
blanchet@48975
   447
        B2: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B"
blanchet@48975
   448
shows "\<exists>f. inj_on f (A <+> B) \<and> f ` (A <+> B) \<le> A \<times> B"
blanchet@48975
   449
using assms by (auto simp add: card_of_Plus_Times card_of_ordLeq)
blanchet@48975
   450
blanchet@48975
   451
corollary Plus_into_Times_types:
blanchet@48975
   452
assumes A2: "(a1::'a) \<noteq> a2" and  B2: "(b1::'b) \<noteq> b2"
blanchet@48975
   453
shows "\<exists>(f::'a + 'b \<Rightarrow> 'a * 'b). inj f"
blanchet@48975
   454
using assms Plus_into_Times[of a1 a2 UNIV b1 b2 UNIV]
blanchet@48975
   455
by auto
blanchet@48975
   456
blanchet@48975
   457
corollary Times_same_infinite_bij_betw:
blanchet@48975
   458
assumes "infinite A"
blanchet@48975
   459
shows "\<exists>f. bij_betw f (A \<times> A) A"
blanchet@48975
   460
using assms by (auto simp add: card_of_ordIso)
blanchet@48975
   461
blanchet@48975
   462
corollary Times_same_infinite_bij_betw_types:
blanchet@48975
   463
assumes INF: "infinite(UNIV::'a set)"
blanchet@48975
   464
shows "\<exists>(f::('a * 'a) => 'a). bij f"
blanchet@48975
   465
using assms Times_same_infinite_bij_betw[of "UNIV::'a set"]
blanchet@48975
   466
by auto
blanchet@48975
   467
blanchet@48975
   468
corollary Times_infinite_bij_betw:
blanchet@48975
   469
assumes INF: "infinite A" and NE: "B \<noteq> {}" and INJ: "inj_on g B \<and> g ` B \<le> A"
blanchet@48975
   470
shows "(\<exists>f. bij_betw f (A \<times> B) A) \<and> (\<exists>h. bij_betw h (B \<times> A) A)"
blanchet@48975
   471
proof-
blanchet@48975
   472
  have "|B| \<le>o |A|" using INJ card_of_ordLeq by blast
blanchet@48975
   473
  thus ?thesis using INF NE
blanchet@48975
   474
  by (auto simp add: card_of_ordIso card_of_Times_infinite)
blanchet@48975
   475
qed
blanchet@48975
   476
blanchet@48975
   477
corollary Times_infinite_bij_betw_types:
blanchet@48975
   478
assumes INF: "infinite(UNIV::'a set)" and
blanchet@48975
   479
        BIJ: "inj(g::'b \<Rightarrow> 'a)"
blanchet@48975
   480
shows "(\<exists>(f::('b * 'a) => 'a). bij f) \<and> (\<exists>(h::('a * 'b) => 'a). bij h)"
blanchet@48975
   481
using assms Times_infinite_bij_betw[of "UNIV::'a set" "UNIV::'b set" g]
blanchet@48975
   482
by auto
blanchet@48975
   483
blanchet@48975
   484
lemma card_of_Times_ordLeq_infinite:
blanchet@48975
   485
"\<lbrakk>infinite C; |A| \<le>o |C|; |B| \<le>o |C|\<rbrakk>
blanchet@48975
   486
 \<Longrightarrow> |A <*> B| \<le>o |C|"
blanchet@48975
   487
by(simp add: card_of_Sigma_ordLeq_infinite)
blanchet@48975
   488
blanchet@48975
   489
corollary Plus_infinite_bij_betw:
blanchet@48975
   490
assumes INF: "infinite A" and INJ: "inj_on g B \<and> g ` B \<le> A"
blanchet@48975
   491
shows "(\<exists>f. bij_betw f (A <+> B) A) \<and> (\<exists>h. bij_betw h (B <+> A) A)"
blanchet@48975
   492
proof-
blanchet@48975
   493
  have "|B| \<le>o |A|" using INJ card_of_ordLeq by blast
blanchet@48975
   494
  thus ?thesis using INF
blanchet@48975
   495
  by (auto simp add: card_of_ordIso)
blanchet@48975
   496
qed
blanchet@48975
   497
blanchet@48975
   498
corollary Plus_infinite_bij_betw_types:
blanchet@48975
   499
assumes INF: "infinite(UNIV::'a set)" and
blanchet@48975
   500
        BIJ: "inj(g::'b \<Rightarrow> 'a)"
blanchet@48975
   501
shows "(\<exists>(f::('b + 'a) => 'a). bij f) \<and> (\<exists>(h::('a + 'b) => 'a). bij h)"
blanchet@48975
   502
using assms Plus_infinite_bij_betw[of "UNIV::'a set" g "UNIV::'b set"]
blanchet@48975
   503
by auto
blanchet@48975
   504
blanchet@48975
   505
lemma card_of_Un_infinite_simps[simp]:
blanchet@48975
   506
"\<lbrakk>infinite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |A \<union> B| =o |A|"
blanchet@48975
   507
"\<lbrakk>infinite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |B \<union> A| =o |A|"
blanchet@48975
   508
using card_of_Un_infinite by auto
blanchet@48975
   509
blanchet@48975
   510
corollary Card_order_Un_infinite:
blanchet@48975
   511
assumes INF: "infinite(Field r)" and CARD: "Card_order r" and
blanchet@48975
   512
        LEQ: "p \<le>o r"
blanchet@48975
   513
shows "| (Field r) \<union> (Field p) | =o r \<and> | (Field p) \<union> (Field r) | =o r"
blanchet@48975
   514
proof-
blanchet@48975
   515
  have "| Field r \<union> Field p | =o | Field r | \<and>
blanchet@48975
   516
        | Field p \<union> Field r | =o | Field r |"
blanchet@48975
   517
  using assms by (auto simp add: card_of_Un_infinite)
blanchet@48975
   518
  thus ?thesis
blanchet@48975
   519
  using assms card_of_Field_ordIso[of r]
blanchet@48975
   520
        ordIso_transitive[of "|Field r \<union> Field p|"]
blanchet@48975
   521
        ordIso_transitive[of _ "|Field r|"] by blast
blanchet@48975
   522
qed
blanchet@48975
   523
blanchet@48975
   524
corollary subset_ordLeq_diff_infinite:
blanchet@48975
   525
assumes INF: "infinite B" and SUB: "A \<le> B" and LESS: "|A| <o |B|"
blanchet@48975
   526
shows "infinite (B - A)"
blanchet@48975
   527
using assms card_of_Un_diff_infinite card_of_ordIso_finite by blast
blanchet@48975
   528
blanchet@48975
   529
lemma card_of_Times_ordLess_infinite[simp]:
blanchet@48975
   530
assumes INF: "infinite C" and
blanchet@48975
   531
        LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
blanchet@48975
   532
shows "|A \<times> B| <o |C|"
blanchet@48975
   533
proof(cases "A = {} \<or> B = {}")
blanchet@48975
   534
  assume Case1: "A = {} \<or> B = {}"
blanchet@48975
   535
  hence "A \<times> B = {}" by blast
blanchet@48975
   536
  moreover have "C \<noteq> {}" using
blanchet@48975
   537
  LESS1 card_of_empty5 by blast
blanchet@48975
   538
  ultimately show ?thesis by(auto simp add:  card_of_empty4)
blanchet@48975
   539
next
blanchet@48975
   540
  assume Case2: "\<not>(A = {} \<or> B = {})"
blanchet@48975
   541
  {assume *: "|C| \<le>o |A \<times> B|"
blanchet@48975
   542
   hence "infinite (A \<times> B)" using INF card_of_ordLeq_finite by blast
blanchet@48975
   543
   hence 1: "infinite A \<or> infinite B" using finite_cartesian_product by blast
blanchet@48975
   544
   {assume Case21: "|A| \<le>o |B|"
blanchet@48975
   545
    hence "infinite B" using 1 card_of_ordLeq_finite by blast
blanchet@48975
   546
    hence "|A \<times> B| =o |B|" using Case2 Case21
blanchet@48975
   547
    by (auto simp add: card_of_Times_infinite)
blanchet@48975
   548
    hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
blanchet@48975
   549
   }
blanchet@48975
   550
   moreover
blanchet@48975
   551
   {assume Case22: "|B| \<le>o |A|"
blanchet@48975
   552
    hence "infinite A" using 1 card_of_ordLeq_finite by blast
blanchet@48975
   553
    hence "|A \<times> B| =o |A|" using Case2 Case22
blanchet@48975
   554
    by (auto simp add: card_of_Times_infinite)
blanchet@48975
   555
    hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
blanchet@48975
   556
   }
blanchet@48975
   557
   ultimately have False using ordLeq_total card_of_Well_order[of A]
blanchet@48975
   558
   card_of_Well_order[of B] by blast
blanchet@48975
   559
  }
blanchet@48975
   560
  thus ?thesis using ordLess_or_ordLeq[of "|A \<times> B|" "|C|"]
blanchet@48975
   561
  card_of_Well_order[of "A \<times> B"] card_of_Well_order[of "C"] by auto
blanchet@48975
   562
qed
blanchet@48975
   563
blanchet@48975
   564
lemma card_of_Times_ordLess_infinite_Field[simp]:
blanchet@48975
   565
assumes INF: "infinite (Field r)" and r: "Card_order r" and
blanchet@48975
   566
        LESS1: "|A| <o r" and LESS2: "|B| <o r"
blanchet@48975
   567
shows "|A \<times> B| <o r"
blanchet@48975
   568
proof-
blanchet@48975
   569
  let ?C  = "Field r"
blanchet@48975
   570
  have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso
blanchet@48975
   571
  ordIso_symmetric by blast
blanchet@48975
   572
  hence "|A| <o |?C|"  "|B| <o |?C|"
blanchet@48975
   573
  using LESS1 LESS2 ordLess_ordIso_trans by blast+
blanchet@48975
   574
  hence  "|A <*> B| <o |?C|" using INF
blanchet@48975
   575
  card_of_Times_ordLess_infinite by blast
blanchet@48975
   576
  thus ?thesis using 1 ordLess_ordIso_trans by blast
blanchet@48975
   577
qed
blanchet@48975
   578
blanchet@48975
   579
lemma card_of_Un_ordLess_infinite[simp]:
blanchet@48975
   580
assumes INF: "infinite C" and
blanchet@48975
   581
        LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
blanchet@48975
   582
shows "|A \<union> B| <o |C|"
blanchet@48975
   583
using assms card_of_Plus_ordLess_infinite card_of_Un_Plus_ordLeq
blanchet@48975
   584
      ordLeq_ordLess_trans by blast
blanchet@48975
   585
blanchet@48975
   586
lemma card_of_Un_ordLess_infinite_Field[simp]:
blanchet@48975
   587
assumes INF: "infinite (Field r)" and r: "Card_order r" and
blanchet@48975
   588
        LESS1: "|A| <o r" and LESS2: "|B| <o r"
blanchet@48975
   589
shows "|A Un B| <o r"
blanchet@48975
   590
proof-
blanchet@48975
   591
  let ?C  = "Field r"
blanchet@48975
   592
  have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso
blanchet@48975
   593
  ordIso_symmetric by blast
blanchet@48975
   594
  hence "|A| <o |?C|"  "|B| <o |?C|"
blanchet@48975
   595
  using LESS1 LESS2 ordLess_ordIso_trans by blast+
blanchet@48975
   596
  hence  "|A Un B| <o |?C|" using INF
blanchet@48975
   597
  card_of_Un_ordLess_infinite by blast
blanchet@48975
   598
  thus ?thesis using 1 ordLess_ordIso_trans by blast
blanchet@48975
   599
qed
blanchet@48975
   600
blanchet@48975
   601
lemma card_of_Un_singl_ordLess_infinite1:
blanchet@48975
   602
assumes "infinite B" and "|A| <o |B|"
blanchet@48975
   603
shows "|{a} Un A| <o |B|"
blanchet@48975
   604
proof-
blanchet@48975
   605
  have "|{a}| <o |B|" using assms by auto
traytel@51764
   606
  thus ?thesis using assms card_of_Un_ordLess_infinite[of B] by blast
blanchet@48975
   607
qed
blanchet@48975
   608
blanchet@48975
   609
lemma card_of_Un_singl_ordLess_infinite:
blanchet@48975
   610
assumes "infinite B"
blanchet@48975
   611
shows "( |A| <o |B| ) = ( |{a} Un A| <o |B| )"
blanchet@48975
   612
using assms card_of_Un_singl_ordLess_infinite1[of B A]
blanchet@48975
   613
proof(auto)
blanchet@48975
   614
  assume "|insert a A| <o |B|"
traytel@51764
   615
  moreover have "|A| <=o |insert a A|" using card_of_mono1[of A "insert a A"] by blast
blanchet@48975
   616
  ultimately show "|A| <o |B|" using ordLeq_ordLess_trans by blast
blanchet@48975
   617
qed
blanchet@48975
   618
blanchet@48975
   619
blanchet@48975
   620
subsection {* Cardinals versus lists  *}
blanchet@48975
   621
blanchet@48975
   622
lemma Card_order_lists: "Card_order r \<Longrightarrow> r \<le>o |lists(Field r) |"
blanchet@48975
   623
using card_of_lists card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
blanchet@48975
   624
blanchet@48975
   625
lemma Union_set_lists:
blanchet@48975
   626
"Union(set ` (lists A)) = A"
blanchet@48975
   627
unfolding lists_def2 proof(auto)
blanchet@48975
   628
  fix a assume "a \<in> A"
blanchet@48975
   629
  hence "set [a] \<le> A \<and> a \<in> set [a]" by auto
blanchet@48975
   630
  thus "\<exists>l. set l \<le> A \<and> a \<in> set l" by blast
blanchet@48975
   631
qed
blanchet@48975
   632
blanchet@48975
   633
lemma inj_on_map_lists:
blanchet@48975
   634
assumes "inj_on f A"
blanchet@48975
   635
shows "inj_on (map f) (lists A)"
blanchet@48975
   636
using assms Union_set_lists[of A] inj_on_mapI[of f "lists A"] by auto
blanchet@48975
   637
blanchet@48975
   638
lemma map_lists_mono:
blanchet@48975
   639
assumes "f ` A \<le> B"
blanchet@48975
   640
shows "(map f) ` (lists A) \<le> lists B"
blanchet@48975
   641
using assms unfolding lists_def2 by (auto, blast) (* lethal combination of methods :)  *)
blanchet@48975
   642
blanchet@48975
   643
lemma map_lists_surjective:
blanchet@48975
   644
assumes "f ` A = B"
blanchet@48975
   645
shows "(map f) ` (lists A) = lists B"
blanchet@48975
   646
using assms unfolding lists_def2
blanchet@48975
   647
proof (auto, blast)
blanchet@48975
   648
  fix l' assume *: "set l' \<le> f ` A"
blanchet@48975
   649
  have "set l' \<le> f ` A \<longrightarrow> l' \<in> map f ` {l. set l \<le> A}"
blanchet@48975
   650
  proof(induct l', auto)
blanchet@48975
   651
    fix l a
blanchet@48975
   652
    assume "a \<in> A" and "set l \<le> A" and
blanchet@48975
   653
           IH: "f ` (set l) \<le> f ` A"
blanchet@48975
   654
    hence "set (a # l) \<le> A" by auto
blanchet@48975
   655
    hence "map f (a # l) \<in> map f ` {l. set l \<le> A}" by blast
blanchet@48975
   656
    thus "f a # map f l \<in> map f ` {l. set l \<le> A}" by auto
blanchet@48975
   657
  qed
blanchet@48975
   658
  thus "l' \<in> map f ` {l. set l \<le> A}" using * by auto
blanchet@48975
   659
qed
blanchet@48975
   660
blanchet@48975
   661
lemma bij_betw_map_lists:
blanchet@48975
   662
assumes "bij_betw f A B"
blanchet@48975
   663
shows "bij_betw (map f) (lists A) (lists B)"
blanchet@48975
   664
using assms unfolding bij_betw_def
blanchet@48975
   665
by(auto simp add: inj_on_map_lists map_lists_surjective)
blanchet@48975
   666
blanchet@48975
   667
lemma card_of_lists_mono[simp]:
blanchet@48975
   668
assumes "|A| \<le>o |B|"
blanchet@48975
   669
shows "|lists A| \<le>o |lists B|"
blanchet@48975
   670
proof-
blanchet@48975
   671
  obtain f where "inj_on f A \<and> f ` A \<le> B"
blanchet@48975
   672
  using assms card_of_ordLeq[of A B] by auto
blanchet@48975
   673
  hence "inj_on (map f) (lists A) \<and> (map f) ` (lists A) \<le> (lists B)"
blanchet@48975
   674
  by (auto simp add: inj_on_map_lists map_lists_mono)
blanchet@48975
   675
  thus ?thesis using card_of_ordLeq[of "lists A"] by metis
blanchet@48975
   676
qed
blanchet@48975
   677
blanchet@48975
   678
lemma ordIso_lists_mono:
blanchet@48975
   679
assumes "r \<le>o r'"
blanchet@48975
   680
shows "|lists(Field r)| \<le>o |lists(Field r')|"
blanchet@48975
   681
using assms card_of_mono2 card_of_lists_mono by blast
blanchet@48975
   682
blanchet@48975
   683
lemma card_of_lists_cong[simp]:
blanchet@48975
   684
assumes "|A| =o |B|"
blanchet@48975
   685
shows "|lists A| =o |lists B|"
blanchet@48975
   686
proof-
blanchet@48975
   687
  obtain f where "bij_betw f A B"
blanchet@48975
   688
  using assms card_of_ordIso[of A B] by auto
blanchet@48975
   689
  hence "bij_betw (map f) (lists A) (lists B)"
blanchet@48975
   690
  by (auto simp add: bij_betw_map_lists)
blanchet@48975
   691
  thus ?thesis using card_of_ordIso[of "lists A"] by auto
blanchet@48975
   692
qed
blanchet@48975
   693
blanchet@48975
   694
lemma ordIso_lists_cong:
blanchet@48975
   695
assumes "r =o r'"
blanchet@48975
   696
shows "|lists(Field r)| =o |lists(Field r')|"
blanchet@48975
   697
using assms card_of_cong card_of_lists_cong by blast
blanchet@48975
   698
blanchet@48975
   699
corollary lists_infinite_bij_betw:
blanchet@48975
   700
assumes "infinite A"
blanchet@48975
   701
shows "\<exists>f. bij_betw f (lists A) A"
blanchet@48975
   702
using assms card_of_lists_infinite card_of_ordIso by blast
blanchet@48975
   703
blanchet@48975
   704
corollary lists_infinite_bij_betw_types:
blanchet@48975
   705
assumes "infinite(UNIV :: 'a set)"
blanchet@48975
   706
shows "\<exists>(f::'a list \<Rightarrow> 'a). bij f"
blanchet@48975
   707
using assms assms lists_infinite_bij_betw[of "UNIV::'a set"]
blanchet@48975
   708
using lists_UNIV by auto
blanchet@48975
   709
blanchet@48975
   710
blanchet@48975
   711
subsection {* Cardinals versus the set-of-finite-sets operator  *}
blanchet@48975
   712
blanchet@48975
   713
definition Fpow :: "'a set \<Rightarrow> 'a set set"
blanchet@48975
   714
where "Fpow A \<equiv> {X. X \<le> A \<and> finite X}"
blanchet@48975
   715
blanchet@48975
   716
lemma Fpow_mono: "A \<le> B \<Longrightarrow> Fpow A \<le> Fpow B"
blanchet@48975
   717
unfolding Fpow_def by auto
blanchet@48975
   718
blanchet@48975
   719
lemma empty_in_Fpow: "{} \<in> Fpow A"
blanchet@48975
   720
unfolding Fpow_def by auto
blanchet@48975
   721
blanchet@48975
   722
lemma Fpow_not_empty: "Fpow A \<noteq> {}"
blanchet@48975
   723
using empty_in_Fpow by blast
blanchet@48975
   724
blanchet@48975
   725
lemma Fpow_subset_Pow: "Fpow A \<le> Pow A"
blanchet@48975
   726
unfolding Fpow_def by auto
blanchet@48975
   727
blanchet@48975
   728
lemma card_of_Fpow[simp]: "|A| \<le>o |Fpow A|"
blanchet@48975
   729
proof-
blanchet@48975
   730
  let ?h = "\<lambda> a. {a}"
blanchet@48975
   731
  have "inj_on ?h A \<and> ?h ` A \<le> Fpow A"
blanchet@48975
   732
  unfolding inj_on_def Fpow_def by auto
blanchet@48975
   733
  thus ?thesis using card_of_ordLeq by metis
blanchet@48975
   734
qed
blanchet@48975
   735
blanchet@48975
   736
lemma Card_order_Fpow: "Card_order r \<Longrightarrow> r \<le>o |Fpow(Field r) |"
blanchet@48975
   737
using card_of_Fpow card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
blanchet@48975
   738
blanchet@48975
   739
lemma Fpow_Pow_finite: "Fpow A = Pow A Int {A. finite A}"
blanchet@48975
   740
unfolding Fpow_def Pow_def by blast
blanchet@48975
   741
blanchet@48975
   742
lemma inj_on_image_Fpow:
blanchet@48975
   743
assumes "inj_on f A"
blanchet@48975
   744
shows "inj_on (image f) (Fpow A)"
blanchet@48975
   745
using assms Fpow_subset_Pow[of A] subset_inj_on[of "image f" "Pow A"]
blanchet@48975
   746
      inj_on_image_Pow by blast
blanchet@48975
   747
blanchet@48975
   748
lemma image_Fpow_mono:
blanchet@48975
   749
assumes "f ` A \<le> B"
blanchet@48975
   750
shows "(image f) ` (Fpow A) \<le> Fpow B"
blanchet@48975
   751
using assms by(unfold Fpow_def, auto)
blanchet@48975
   752
blanchet@48975
   753
lemma image_Fpow_surjective:
blanchet@48975
   754
assumes "f ` A = B"
blanchet@48975
   755
shows "(image f) ` (Fpow A) = Fpow B"
blanchet@48975
   756
using assms proof(unfold Fpow_def, auto)
blanchet@48975
   757
  fix Y assume *: "Y \<le> f ` A" and **: "finite Y"
blanchet@48975
   758
  hence "\<forall>b \<in> Y. \<exists>a. a \<in> A \<and> f a = b" by auto
blanchet@48975
   759
  with bchoice[of Y "\<lambda>b a. a \<in> A \<and> f a = b"]
blanchet@48975
   760
  obtain g where 1: "\<forall>b \<in> Y. g b \<in> A \<and> f(g b) = b" by blast
blanchet@48975
   761
  obtain X where X_def: "X = g ` Y" by blast
blanchet@48975
   762
  have "f ` X = Y \<and> X \<le> A \<and> finite X"
blanchet@48975
   763
  by(unfold X_def, force simp add: ** 1)
blanchet@48975
   764
  thus "Y \<in> (image f) ` {X. X \<le> A \<and> finite X}" by auto
blanchet@48975
   765
qed
blanchet@48975
   766
blanchet@48975
   767
lemma bij_betw_image_Fpow:
blanchet@48975
   768
assumes "bij_betw f A B"
blanchet@48975
   769
shows "bij_betw (image f) (Fpow A) (Fpow B)"
blanchet@48975
   770
using assms unfolding bij_betw_def
blanchet@48975
   771
by (auto simp add: inj_on_image_Fpow image_Fpow_surjective)
blanchet@48975
   772
blanchet@48975
   773
lemma card_of_Fpow_mono[simp]:
blanchet@48975
   774
assumes "|A| \<le>o |B|"
blanchet@48975
   775
shows "|Fpow A| \<le>o |Fpow B|"
blanchet@48975
   776
proof-
blanchet@48975
   777
  obtain f where "inj_on f A \<and> f ` A \<le> B"
blanchet@48975
   778
  using assms card_of_ordLeq[of A B] by auto
blanchet@48975
   779
  hence "inj_on (image f) (Fpow A) \<and> (image f) ` (Fpow A) \<le> (Fpow B)"
blanchet@48975
   780
  by (auto simp add: inj_on_image_Fpow image_Fpow_mono)
blanchet@48975
   781
  thus ?thesis using card_of_ordLeq[of "Fpow A"] by auto
blanchet@48975
   782
qed
blanchet@48975
   783
blanchet@48975
   784
lemma ordIso_Fpow_mono:
blanchet@48975
   785
assumes "r \<le>o r'"
blanchet@48975
   786
shows "|Fpow(Field r)| \<le>o |Fpow(Field r')|"
blanchet@48975
   787
using assms card_of_mono2 card_of_Fpow_mono by blast
blanchet@48975
   788
blanchet@48975
   789
lemma card_of_Fpow_cong[simp]:
blanchet@48975
   790
assumes "|A| =o |B|"
blanchet@48975
   791
shows "|Fpow A| =o |Fpow B|"
blanchet@48975
   792
proof-
blanchet@48975
   793
  obtain f where "bij_betw f A B"
blanchet@48975
   794
  using assms card_of_ordIso[of A B] by auto
blanchet@48975
   795
  hence "bij_betw (image f) (Fpow A) (Fpow B)"
blanchet@48975
   796
  by (auto simp add: bij_betw_image_Fpow)
blanchet@48975
   797
  thus ?thesis using card_of_ordIso[of "Fpow A"] by auto
blanchet@48975
   798
qed
blanchet@48975
   799
blanchet@48975
   800
lemma ordIso_Fpow_cong:
blanchet@48975
   801
assumes "r =o r'"
blanchet@48975
   802
shows "|Fpow(Field r)| =o |Fpow(Field r')|"
blanchet@48975
   803
using assms card_of_cong card_of_Fpow_cong by blast
blanchet@48975
   804
blanchet@48975
   805
lemma card_of_Fpow_lists: "|Fpow A| \<le>o |lists A|"
blanchet@48975
   806
proof-
blanchet@48975
   807
  have "set ` (lists A) = Fpow A"
blanchet@48975
   808
  unfolding lists_def2 Fpow_def using finite_list finite_set by blast
blanchet@48975
   809
  thus ?thesis using card_of_ordLeq2[of "Fpow A"] Fpow_not_empty[of A] by blast
blanchet@48975
   810
qed
blanchet@48975
   811
blanchet@48975
   812
lemma card_of_Fpow_infinite[simp]:
blanchet@48975
   813
assumes "infinite A"
blanchet@48975
   814
shows "|Fpow A| =o |A|"
blanchet@48975
   815
using assms card_of_Fpow_lists card_of_lists_infinite card_of_Fpow
blanchet@48975
   816
      ordLeq_ordIso_trans ordIso_iff_ordLeq by blast
blanchet@48975
   817
blanchet@48975
   818
corollary Fpow_infinite_bij_betw:
blanchet@48975
   819
assumes "infinite A"
blanchet@48975
   820
shows "\<exists>f. bij_betw f (Fpow A) A"
blanchet@48975
   821
using assms card_of_Fpow_infinite card_of_ordIso by blast
blanchet@48975
   822
blanchet@48975
   823
blanchet@48975
   824
subsection {* The cardinal $\omega$ and the finite cardinals  *}
blanchet@48975
   825
blanchet@48975
   826
subsubsection {* First as well-orders *}
blanchet@48975
   827
blanchet@48975
   828
lemma Field_natLess: "Field natLess = (UNIV::nat set)"
blanchet@48975
   829
by(unfold Field_def, auto)
blanchet@48975
   830
blanchet@48975
   831
lemma natLeq_ofilter_less: "ofilter natLeq {0 ..< n}"
blanchet@48975
   832
by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
blanchet@48975
   833
   simp add:  Field_natLeq, unfold rel.under_def, auto)
blanchet@48975
   834
blanchet@48975
   835
lemma natLeq_ofilter_leq: "ofilter natLeq {0 .. n}"
blanchet@48975
   836
by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
blanchet@48975
   837
   simp add:  Field_natLeq, unfold rel.under_def, auto)
blanchet@48975
   838
blanchet@48975
   839
lemma natLeq_ofilter_iff:
blanchet@48975
   840
"ofilter natLeq A = (A = UNIV \<or> (\<exists>n. A = {0 ..< n}))"
blanchet@48975
   841
proof(rule iffI)
blanchet@48975
   842
  assume "ofilter natLeq A"
blanchet@48975
   843
  hence "\<forall>m n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
blanchet@48975
   844
  by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def rel.under_def)
blanchet@48975
   845
  thus "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
blanchet@48975
   846
next
blanchet@48975
   847
  assume "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
blanchet@48975
   848
  thus "ofilter natLeq A"
blanchet@48975
   849
  by(auto simp add: natLeq_ofilter_less natLeq_UNIV_ofilter)
blanchet@48975
   850
qed
blanchet@48975
   851
blanchet@48975
   852
lemma natLeq_under_leq: "under natLeq n = {0 .. n}"
blanchet@48975
   853
unfolding rel.under_def by auto
blanchet@48975
   854
blanchet@48975
   855
corollary natLeq_on_ofilter:
blanchet@48975
   856
"ofilter(natLeq_on n) {0 ..< n}"
blanchet@48975
   857
by (auto simp add: natLeq_on_ofilter_less_eq)
blanchet@48975
   858
blanchet@48975
   859
lemma natLeq_on_ofilter_less:
blanchet@48975
   860
"n < m \<Longrightarrow> ofilter (natLeq_on m) {0 .. n}"
blanchet@48975
   861
by(auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def,
blanchet@48975
   862
   simp add: Field_natLeq_on, unfold rel.under_def, auto)
blanchet@48975
   863
blanchet@48975
   864
lemma natLeq_on_ordLess_natLeq: "natLeq_on n <o natLeq"
blanchet@48975
   865
using Field_natLeq Field_natLeq_on[of n] nat_infinite
blanchet@48975
   866
      finite_ordLess_infinite[of "natLeq_on n" natLeq]
blanchet@48975
   867
      natLeq_Well_order natLeq_on_Well_order[of n] by auto
blanchet@48975
   868
blanchet@48975
   869
lemma natLeq_on_injective:
blanchet@48975
   870
"natLeq_on m = natLeq_on n \<Longrightarrow> m = n"
blanchet@48975
   871
using Field_natLeq_on[of m] Field_natLeq_on[of n]
blanchet@48975
   872
      atLeastLessThan_injective[of m n] by auto
blanchet@48975
   873
blanchet@48975
   874
lemma natLeq_on_injective_ordIso:
blanchet@48975
   875
"(natLeq_on m =o natLeq_on n) = (m = n)"
blanchet@48975
   876
proof(auto simp add: natLeq_on_Well_order ordIso_reflexive)
blanchet@48975
   877
  assume "natLeq_on m =o natLeq_on n"
blanchet@48975
   878
  then obtain f where "bij_betw f {0..<m} {0..<n}"
blanchet@48975
   879
  using Field_natLeq_on assms unfolding ordIso_def iso_def[abs_def] by auto
blanchet@48975
   880
  thus "m = n" using atLeastLessThan_injective2 by blast
blanchet@48975
   881
qed
blanchet@48975
   882
blanchet@48975
   883
blanchet@48975
   884
subsubsection {* Then as cardinals *}
blanchet@48975
   885
blanchet@48975
   886
lemma ordIso_natLeq_infinite1:
blanchet@48975
   887
"|A| =o natLeq \<Longrightarrow> infinite A"
blanchet@48975
   888
using ordIso_symmetric ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
blanchet@48975
   889
blanchet@48975
   890
lemma ordIso_natLeq_infinite2:
blanchet@48975
   891
"natLeq =o |A| \<Longrightarrow> infinite A"
blanchet@48975
   892
using ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
blanchet@48975
   893
blanchet@48975
   894
lemma ordLeq_natLeq_on_imp_finite:
blanchet@48975
   895
assumes "|A| \<le>o natLeq_on n"
blanchet@48975
   896
shows "finite A"
blanchet@48975
   897
proof-
blanchet@48975
   898
  have "|A| \<le>o |{0 ..< n}|"
blanchet@48975
   899
  using assms card_of_less ordIso_symmetric ordLeq_ordIso_trans by blast
blanchet@48975
   900
  thus ?thesis by (auto simp add: card_of_ordLeq_finite)
blanchet@48975
   901
qed
blanchet@48975
   902
blanchet@48975
   903
blanchet@48975
   904
subsubsection {* "Backwards compatibility" with the numeric cardinal operator for finite sets *}
blanchet@48975
   905
blanchet@48975
   906
lemma finite_card_of_iff_card:
blanchet@48975
   907
assumes FIN: "finite A" and FIN': "finite B"
blanchet@48975
   908
shows "( |A| =o |B| ) = (card A = card B)"
blanchet@48975
   909
using assms card_of_ordIso[of A B] bij_betw_iff_card[of A B] by blast
blanchet@48975
   910
blanchet@48975
   911
lemma finite_card_of_iff_card3:
blanchet@48975
   912
assumes FIN: "finite A" and FIN': "finite B"
blanchet@48975
   913
shows "( |A| <o |B| ) = (card A < card B)"
blanchet@48975
   914
proof-
blanchet@48975
   915
  have "( |A| <o |B| ) = (~ ( |B| \<le>o |A| ))" by simp
blanchet@48975
   916
  also have "... = (~ (card B \<le> card A))"
blanchet@48975
   917
  using assms by(simp add: finite_card_of_iff_card2)
blanchet@48975
   918
  also have "... = (card A < card B)" by auto
blanchet@48975
   919
  finally show ?thesis .
blanchet@48975
   920
qed
blanchet@48975
   921
blanchet@48975
   922
lemma card_Field_natLeq_on:
blanchet@48975
   923
"card(Field(natLeq_on n)) = n"
blanchet@48975
   924
using Field_natLeq_on card_atLeastLessThan by auto
blanchet@48975
   925
blanchet@48975
   926
blanchet@48975
   927
subsection {* The successor of a cardinal *}
blanchet@48975
   928
blanchet@48975
   929
lemma embed_implies_ordIso_Restr:
blanchet@48975
   930
assumes WELL: "Well_order r" and WELL': "Well_order r'" and EMB: "embed r' r f"
blanchet@48975
   931
shows "r' =o Restr r (f ` (Field r'))"
blanchet@48975
   932
using assms embed_implies_iso_Restr Well_order_Restr unfolding ordIso_def by blast
blanchet@48975
   933
blanchet@48975
   934
lemma cardSuc_Well_order[simp]:
blanchet@48975
   935
"Card_order r \<Longrightarrow> Well_order(cardSuc r)"
blanchet@48975
   936
using cardSuc_Card_order unfolding card_order_on_def by blast
blanchet@48975
   937
blanchet@48975
   938
lemma Field_cardSuc_not_empty:
blanchet@48975
   939
assumes "Card_order r"
blanchet@48975
   940
shows "Field (cardSuc r) \<noteq> {}"
blanchet@48975
   941
proof
blanchet@48975
   942
  assume "Field(cardSuc r) = {}"
blanchet@48975
   943
  hence "|Field(cardSuc r)| \<le>o r" using assms Card_order_empty[of r] by auto
blanchet@48975
   944
  hence "cardSuc r \<le>o r" using assms card_of_Field_ordIso
blanchet@48975
   945
  cardSuc_Card_order ordIso_symmetric ordIso_ordLeq_trans by blast
blanchet@48975
   946
  thus False using cardSuc_greater not_ordLess_ordLeq assms by blast
blanchet@48975
   947
qed
blanchet@48975
   948
blanchet@48975
   949
lemma cardSuc_mono_ordLess[simp]:
blanchet@48975
   950
assumes CARD: "Card_order r" and CARD': "Card_order r'"
blanchet@48975
   951
shows "(cardSuc r <o cardSuc r') = (r <o r')"
blanchet@48975
   952
proof-
blanchet@48975
   953
  have 0: "Well_order r \<and> Well_order r' \<and> Well_order(cardSuc r) \<and> Well_order(cardSuc r')"
blanchet@48975
   954
  using assms by auto
blanchet@48975
   955
  thus ?thesis
blanchet@48975
   956
  using not_ordLeq_iff_ordLess not_ordLeq_iff_ordLess[of r r']
blanchet@48975
   957
  using cardSuc_mono_ordLeq[of r' r] assms by blast
blanchet@48975
   958
qed
blanchet@48975
   959
blanchet@48975
   960
lemma card_of_Plus_ordLeq_infinite[simp]:
blanchet@48975
   961
assumes C: "infinite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
blanchet@48975
   962
shows "|A <+> B| \<le>o |C|"
blanchet@48975
   963
proof-
blanchet@48975
   964
  let ?r = "cardSuc |C|"
blanchet@48975
   965
  have "Card_order ?r \<and> infinite (Field ?r)" using assms by simp
blanchet@48975
   966
  moreover have "|A| <o ?r" and "|B| <o ?r" using A B by auto
blanchet@48975
   967
  ultimately have "|A <+> B| <o ?r"
blanchet@48975
   968
  using card_of_Plus_ordLess_infinite_Field by blast
blanchet@48975
   969
  thus ?thesis using C by simp
blanchet@48975
   970
qed
blanchet@48975
   971
blanchet@48975
   972
lemma card_of_Un_ordLeq_infinite[simp]:
blanchet@48975
   973
assumes C: "infinite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
blanchet@48975
   974
shows "|A Un B| \<le>o |C|"
blanchet@48975
   975
using assms card_of_Plus_ordLeq_infinite card_of_Un_Plus_ordLeq
blanchet@48975
   976
ordLeq_transitive by metis
blanchet@48975
   977
blanchet@48975
   978
blanchet@48975
   979
subsection {* Others *}
blanchet@48975
   980
blanchet@48975
   981
lemma under_mono[simp]:
blanchet@48975
   982
assumes "Well_order r" and "(i,j) \<in> r"
blanchet@48975
   983
shows "under r i \<subseteq> under r j"
blanchet@48975
   984
using assms unfolding rel.under_def order_on_defs
blanchet@48975
   985
trans_def by blast
blanchet@48975
   986
blanchet@48975
   987
lemma underS_under:
blanchet@48975
   988
assumes "i \<in> Field r"
blanchet@48975
   989
shows "underS r i = under r i - {i}"
blanchet@48975
   990
using assms unfolding rel.underS_def rel.under_def by auto
blanchet@48975
   991
blanchet@48975
   992
lemma relChain_under:
blanchet@48975
   993
assumes "Well_order r"
blanchet@48975
   994
shows "relChain r (\<lambda> i. under r i)"
blanchet@48975
   995
using assms unfolding relChain_def by auto
blanchet@48975
   996
blanchet@48975
   997
lemma infinite_card_of_diff_singl:
blanchet@48975
   998
assumes "infinite A"
blanchet@48975
   999
shows "|A - {a}| =o |A|"
traytel@52544
  1000
by (metis assms card_of_infinite_diff_finite finite.emptyI finite_insert)
blanchet@48975
  1001
blanchet@48975
  1002
lemma card_of_vimage:
blanchet@48975
  1003
assumes "B \<subseteq> range f"
blanchet@48975
  1004
shows "|B| \<le>o |f -` B|"
blanchet@48975
  1005
apply(rule surj_imp_ordLeq[of _ f])
blanchet@48975
  1006
using assms by (metis Int_absorb2 image_vimage_eq order_refl)
blanchet@48975
  1007
blanchet@48975
  1008
lemma surj_card_of_vimage:
blanchet@48975
  1009
assumes "surj f"
blanchet@48975
  1010
shows "|B| \<le>o |f -` B|"
blanchet@48975
  1011
by (metis assms card_of_vimage subset_UNIV)
blanchet@48975
  1012
blanchet@48975
  1013
(* bounded powerset *)
blanchet@48975
  1014
definition Bpow where
blanchet@48975
  1015
"Bpow r A \<equiv> {X . X \<subseteq> A \<and> |X| \<le>o r}"
blanchet@48975
  1016
blanchet@48975
  1017
lemma Bpow_empty[simp]:
blanchet@48975
  1018
assumes "Card_order r"
blanchet@48975
  1019
shows "Bpow r {} = {{}}"
blanchet@48975
  1020
using assms unfolding Bpow_def by auto
blanchet@48975
  1021
blanchet@48975
  1022
lemma singl_in_Bpow:
blanchet@48975
  1023
assumes rc: "Card_order r"
blanchet@48975
  1024
and r: "Field r \<noteq> {}" and a: "a \<in> A"
blanchet@48975
  1025
shows "{a} \<in> Bpow r A"
blanchet@48975
  1026
proof-
blanchet@48975
  1027
  have "|{a}| \<le>o r" using r rc by auto
blanchet@48975
  1028
  thus ?thesis unfolding Bpow_def using a by auto
blanchet@48975
  1029
qed
blanchet@48975
  1030
blanchet@48975
  1031
lemma ordLeq_card_Bpow:
blanchet@48975
  1032
assumes rc: "Card_order r" and r: "Field r \<noteq> {}"
blanchet@48975
  1033
shows "|A| \<le>o |Bpow r A|"
blanchet@48975
  1034
proof-
blanchet@48975
  1035
  have "inj_on (\<lambda> a. {a}) A" unfolding inj_on_def by auto
blanchet@48975
  1036
  moreover have "(\<lambda> a. {a}) ` A \<subseteq> Bpow r A"
blanchet@48975
  1037
  using singl_in_Bpow[OF assms] by auto
blanchet@48975
  1038
  ultimately show ?thesis unfolding card_of_ordLeq[symmetric] by blast
blanchet@48975
  1039
qed
blanchet@48975
  1040
blanchet@48975
  1041
lemma infinite_Bpow:
blanchet@48975
  1042
assumes rc: "Card_order r" and r: "Field r \<noteq> {}"
blanchet@48975
  1043
and A: "infinite A"
blanchet@48975
  1044
shows "infinite (Bpow r A)"
blanchet@48975
  1045
using ordLeq_card_Bpow[OF rc r]
blanchet@48975
  1046
by (metis A card_of_ordLeq_infinite)
blanchet@48975
  1047
blanchet@48975
  1048
lemma Bpow_ordLeq_Func_Field:
blanchet@48975
  1049
assumes rc: "Card_order r" and r: "Field r \<noteq> {}" and A: "infinite A"
blanchet@48975
  1050
shows "|Bpow r A| \<le>o |Func (Field r) A|"
blanchet@48975
  1051
proof-
blanchet@48975
  1052
  let ?F = "\<lambda> f. {x | x a. f a = Some x}"
blanchet@48975
  1053
  {fix X assume "X \<in> Bpow r A - {{}}"
blanchet@48975
  1054
   hence XA: "X \<subseteq> A" and "|X| \<le>o r"
blanchet@48975
  1055
   and X: "X \<noteq> {}" unfolding Bpow_def by auto
blanchet@48975
  1056
   hence "|X| \<le>o |Field r|" by (metis Field_card_of card_of_mono2)
blanchet@48975
  1057
   then obtain F where 1: "X = F ` (Field r)"
blanchet@48975
  1058
   using card_of_ordLeq2[OF X] by metis
blanchet@48975
  1059
   def f \<equiv> "\<lambda> i. if i \<in> Field r then Some (F i) else None"
blanchet@48975
  1060
   have "\<exists> f \<in> Func (Field r) A. X = ?F f"
blanchet@48975
  1061
   apply (intro bexI[of _ f]) using 1 XA unfolding Func_def f_def by auto
blanchet@48975
  1062
  }
blanchet@48975
  1063
  hence "Bpow r A - {{}} \<subseteq> ?F ` (Func (Field r) A)" by auto
blanchet@48975
  1064
  hence "|Bpow r A - {{}}| \<le>o |Func (Field r) A|"
blanchet@48975
  1065
  by (rule surj_imp_ordLeq)
blanchet@48975
  1066
  moreover
blanchet@48975
  1067
  {have 2: "infinite (Bpow r A)" using infinite_Bpow[OF rc r A] .
blanchet@48975
  1068
   have "|Bpow r A| =o |Bpow r A - {{}}|"
traytel@52544
  1069
   using card_of_infinite_diff_finite
blanchet@48975
  1070
   by (metis Pow_empty 2 finite_Pow_iff infinite_imp_nonempty ordIso_symmetric)
blanchet@48975
  1071
  }
blanchet@48975
  1072
  ultimately show ?thesis by (metis ordIso_ordLeq_trans)
blanchet@48975
  1073
qed
blanchet@48975
  1074
blanchet@48975
  1075
lemma Func_emp2[simp]: "A \<noteq> {} \<Longrightarrow> Func A {} = {}" by auto
blanchet@48975
  1076
blanchet@48975
  1077
lemma empty_in_Func[simp]:
blanchet@48975
  1078
"B \<noteq> {} \<Longrightarrow> empty \<in> Func {} B"
blanchet@48975
  1079
unfolding Func_def by auto
blanchet@48975
  1080
blanchet@48975
  1081
lemma Func_mono[simp]:
blanchet@48975
  1082
assumes "B1 \<subseteq> B2"
blanchet@48975
  1083
shows "Func A B1 \<subseteq> Func A B2"
blanchet@48975
  1084
using assms unfolding Func_def by force
blanchet@48975
  1085
blanchet@48975
  1086
lemma Pfunc_mono[simp]:
blanchet@48975
  1087
assumes "A1 \<subseteq> A2" and "B1 \<subseteq> B2"
blanchet@48975
  1088
shows "Pfunc A B1 \<subseteq> Pfunc A B2"
blanchet@48975
  1089
using assms in_mono unfolding Pfunc_def apply safe
blanchet@48975
  1090
apply(case_tac "x a", auto)
blanchet@48975
  1091
by (metis in_mono option.simps(5))
blanchet@48975
  1092
blanchet@48975
  1093
lemma card_of_Func_UNIV_UNIV:
blanchet@48975
  1094
"|Func (UNIV::'a set) (UNIV::'b set)| =o |UNIV::('a \<Rightarrow> 'b) set|"
blanchet@48975
  1095
using card_of_Func_UNIV[of "UNIV::'b set"] by auto
blanchet@48975
  1096
blanchet@48975
  1097
end