src/ZF/Cardinal.thy
author wenzelm
Mon Dec 04 22:54:31 2017 +0100 (20 months ago)
changeset 67131 85d10959c2e4
parent 61798 27f3c10b0b50
child 67443 3abf6a722518
permissions -rw-r--r--
tuned signature;
clasohm@1478
     1
(*  Title:      ZF/Cardinal.thy
clasohm@1478
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@435
     3
    Copyright   1994  University of Cambridge
paulson@13328
     4
*)
paulson@13221
     5
wenzelm@60770
     6
section\<open>Cardinal Numbers Without the Axiom of Choice\<close>
lcp@435
     7
krauss@26056
     8
theory Cardinal imports OrderType Finite Nat_ZF Sum begin
paulson@13221
     9
wenzelm@24893
    10
definition
lcp@435
    11
  (*least ordinal operator*)
wenzelm@61394
    12
   Least    :: "(i=>o) => i"    (binder "\<mu> " 10)  where
paulson@46820
    13
     "Least(P) == THE i. Ord(i) & P(i) & (\<forall>j. j<i \<longrightarrow> ~P(j))"
lcp@435
    14
wenzelm@24893
    15
definition
wenzelm@61394
    16
  eqpoll   :: "[i,i] => o"     (infixl "\<approx>" 50)  where
wenzelm@61394
    17
    "A \<approx> B == \<exists>f. f \<in> bij(A,B)"
lcp@435
    18
wenzelm@24893
    19
definition
wenzelm@61394
    20
  lepoll   :: "[i,i] => o"     (infixl "\<lesssim>" 50)  where
wenzelm@61394
    21
    "A \<lesssim> B == \<exists>f. f \<in> inj(A,B)"
lcp@435
    22
wenzelm@24893
    23
definition
wenzelm@61394
    24
  lesspoll :: "[i,i] => o"     (infixl "\<prec>" 50)  where
wenzelm@61394
    25
    "A \<prec> B == A \<lesssim> B & ~(A \<approx> B)"
lcp@832
    26
wenzelm@24893
    27
definition
wenzelm@24893
    28
  cardinal :: "i=>i"           ("|_|")  where
wenzelm@61394
    29
    "|A| == (\<mu> i. i \<approx> A)"
lcp@435
    30
wenzelm@24893
    31
definition
wenzelm@24893
    32
  Finite   :: "i=>o"  where
wenzelm@61394
    33
    "Finite(A) == \<exists>n\<in>nat. A \<approx> n"
lcp@435
    34
wenzelm@24893
    35
definition
wenzelm@24893
    36
  Card     :: "i=>o"  where
paulson@13221
    37
    "Card(i) == (i = |i|)"
lcp@435
    38
kleing@14565
    39
wenzelm@60770
    40
subsection\<open>The Schroeder-Bernstein Theorem\<close>
wenzelm@60770
    41
text\<open>See Davey and Priestly, page 106\<close>
paulson@13221
    42
paulson@13221
    43
(** Lemma: Banach's Decomposition Theorem **)
paulson@13221
    44
paulson@13221
    45
lemma decomp_bnd_mono: "bnd_mono(X, %W. X - g``(Y - f``W))"
paulson@13221
    46
by (rule bnd_monoI, blast+)
paulson@13221
    47
paulson@13221
    48
lemma Banach_last_equation:
paulson@46953
    49
    "g \<in> Y->X
paulson@46820
    50
     ==> g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) =
paulson@46820
    51
         X - lfp(X, %W. X - g``(Y - f``W))"
wenzelm@59788
    52
apply (rule_tac P = "%u. v = X-u" for v
paulson@13221
    53
       in decomp_bnd_mono [THEN lfp_unfold, THEN ssubst])
paulson@13221
    54
apply (simp add: double_complement  fun_is_rel [THEN image_subset])
paulson@13221
    55
done
paulson@13221
    56
paulson@13221
    57
lemma decomposition:
paulson@46953
    58
     "[| f \<in> X->Y;  g \<in> Y->X |] ==>
paulson@46820
    59
      \<exists>XA XB YA YB. (XA \<inter> XB = 0) & (XA \<union> XB = X) &
paulson@46820
    60
                      (YA \<inter> YB = 0) & (YA \<union> YB = Y) &
paulson@13221
    61
                      f``XA=YA & g``YB=XB"
paulson@13221
    62
apply (intro exI conjI)
paulson@13221
    63
apply (rule_tac [6] Banach_last_equation)
paulson@13221
    64
apply (rule_tac [5] refl)
paulson@46820
    65
apply (assumption |
paulson@13221
    66
       rule  Diff_disjoint Diff_partition fun_is_rel image_subset lfp_subset)+
paulson@13221
    67
done
paulson@13221
    68
paulson@13221
    69
lemma schroeder_bernstein:
paulson@46953
    70
    "[| f \<in> inj(X,Y);  g \<in> inj(Y,X) |] ==> \<exists>h. h \<in> bij(X,Y)"
paulson@46820
    71
apply (insert decomposition [of f X Y g])
paulson@13221
    72
apply (simp add: inj_is_fun)
paulson@13221
    73
apply (blast intro!: restrict_bij bij_disjoint_Un intro: bij_converse_bij)
paulson@46820
    74
(* The instantiation of exI to @{term"restrict(f,XA) \<union> converse(restrict(g,YB))"}
paulson@13221
    75
   is forced by the context!! *)
paulson@13221
    76
done
paulson@13221
    77
paulson@13221
    78
paulson@13221
    79
(** Equipollence is an equivalence relation **)
paulson@13221
    80
paulson@46953
    81
lemma bij_imp_eqpoll: "f \<in> bij(A,B) ==> A \<approx> B"
paulson@13221
    82
apply (unfold eqpoll_def)
paulson@13221
    83
apply (erule exI)
paulson@13221
    84
done
paulson@13221
    85
wenzelm@61394
    86
(*A \<approx> A*)
wenzelm@45602
    87
lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, simp]
paulson@13221
    88
paulson@13221
    89
lemma eqpoll_sym: "X \<approx> Y ==> Y \<approx> X"
paulson@13221
    90
apply (unfold eqpoll_def)
paulson@13221
    91
apply (blast intro: bij_converse_bij)
paulson@13221
    92
done
paulson@13221
    93
paulson@46841
    94
lemma eqpoll_trans [trans]:
paulson@13221
    95
    "[| X \<approx> Y;  Y \<approx> Z |] ==> X \<approx> Z"
paulson@13221
    96
apply (unfold eqpoll_def)
paulson@13221
    97
apply (blast intro: comp_bij)
paulson@13221
    98
done
paulson@13221
    99
paulson@13221
   100
(** Le-pollence is a partial ordering **)
paulson@13221
   101
paulson@13221
   102
lemma subset_imp_lepoll: "X<=Y ==> X \<lesssim> Y"
paulson@13221
   103
apply (unfold lepoll_def)
paulson@13221
   104
apply (rule exI)
paulson@13221
   105
apply (erule id_subset_inj)
paulson@13221
   106
done
paulson@13221
   107
wenzelm@45602
   108
lemmas lepoll_refl = subset_refl [THEN subset_imp_lepoll, simp]
paulson@13221
   109
wenzelm@45602
   110
lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll]
paulson@13221
   111
paulson@13221
   112
lemma eqpoll_imp_lepoll: "X \<approx> Y ==> X \<lesssim> Y"
paulson@13221
   113
by (unfold eqpoll_def bij_def lepoll_def, blast)
paulson@13221
   114
paulson@46841
   115
lemma lepoll_trans [trans]: "[| X \<lesssim> Y;  Y \<lesssim> Z |] ==> X \<lesssim> Z"
paulson@13221
   116
apply (unfold lepoll_def)
paulson@13221
   117
apply (blast intro: comp_inj)
paulson@13221
   118
done
paulson@13221
   119
paulson@46841
   120
lemma eq_lepoll_trans [trans]: "[| X \<approx> Y;  Y \<lesssim> Z |] ==> X \<lesssim> Z"
paulson@46953
   121
 by (blast intro: eqpoll_imp_lepoll lepoll_trans)
paulson@46841
   122
paulson@46841
   123
lemma lepoll_eq_trans [trans]: "[| X \<lesssim> Y;  Y \<approx> Z |] ==> X \<lesssim> Z"
paulson@46953
   124
 by (blast intro: eqpoll_imp_lepoll lepoll_trans)
paulson@46841
   125
paulson@13221
   126
(*Asymmetry law*)
paulson@13221
   127
lemma eqpollI: "[| X \<lesssim> Y;  Y \<lesssim> X |] ==> X \<approx> Y"
paulson@13221
   128
apply (unfold lepoll_def eqpoll_def)
paulson@13221
   129
apply (elim exE)
paulson@13221
   130
apply (rule schroeder_bernstein, assumption+)
paulson@13221
   131
done
paulson@13221
   132
paulson@13221
   133
lemma eqpollE:
paulson@13221
   134
    "[| X \<approx> Y; [| X \<lesssim> Y; Y \<lesssim> X |] ==> P |] ==> P"
paulson@46820
   135
by (blast intro: eqpoll_imp_lepoll eqpoll_sym)
paulson@13221
   136
paulson@46821
   137
lemma eqpoll_iff: "X \<approx> Y \<longleftrightarrow> X \<lesssim> Y & Y \<lesssim> X"
paulson@13221
   138
by (blast intro: eqpollI elim!: eqpollE)
paulson@13221
   139
paulson@13221
   140
lemma lepoll_0_is_0: "A \<lesssim> 0 ==> A = 0"
paulson@13221
   141
apply (unfold lepoll_def inj_def)
paulson@13221
   142
apply (blast dest: apply_type)
paulson@13221
   143
done
paulson@13221
   144
paulson@46820
   145
(*@{term"0 \<lesssim> Y"}*)
wenzelm@45602
   146
lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll]
paulson@13221
   147
paulson@46821
   148
lemma lepoll_0_iff: "A \<lesssim> 0 \<longleftrightarrow> A=0"
paulson@13221
   149
by (blast intro: lepoll_0_is_0 lepoll_refl)
paulson@13221
   150
paulson@46820
   151
lemma Un_lepoll_Un:
paulson@46820
   152
    "[| A \<lesssim> B; C \<lesssim> D; B \<inter> D = 0 |] ==> A \<union> C \<lesssim> B \<union> D"
paulson@13221
   153
apply (unfold lepoll_def)
paulson@13221
   154
apply (blast intro: inj_disjoint_Un)
paulson@13221
   155
done
paulson@13221
   156
wenzelm@61394
   157
(*A \<approx> 0 ==> A=0*)
wenzelm@45602
   158
lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0]
paulson@13221
   159
paulson@46821
   160
lemma eqpoll_0_iff: "A \<approx> 0 \<longleftrightarrow> A=0"
paulson@13221
   161
by (blast intro: eqpoll_0_is_0 eqpoll_refl)
paulson@13221
   162
paulson@46820
   163
lemma eqpoll_disjoint_Un:
paulson@46820
   164
    "[| A \<approx> B;  C \<approx> D;  A \<inter> C = 0;  B \<inter> D = 0 |]
paulson@46820
   165
     ==> A \<union> C \<approx> B \<union> D"
paulson@13221
   166
apply (unfold eqpoll_def)
paulson@13221
   167
apply (blast intro: bij_disjoint_Un)
paulson@13221
   168
done
paulson@13221
   169
paulson@13221
   170
wenzelm@60770
   171
subsection\<open>lesspoll: contributions by Krzysztof Grabczewski\<close>
paulson@13221
   172
paulson@13221
   173
lemma lesspoll_not_refl: "~ (i \<prec> i)"
paulson@46820
   174
by (simp add: lesspoll_def)
paulson@13221
   175
paulson@13221
   176
lemma lesspoll_irrefl [elim!]: "i \<prec> i ==> P"
paulson@46820
   177
by (simp add: lesspoll_def)
paulson@13221
   178
paulson@13221
   179
lemma lesspoll_imp_lepoll: "A \<prec> B ==> A \<lesssim> B"
paulson@13221
   180
by (unfold lesspoll_def, blast)
paulson@13221
   181
paulson@46820
   182
lemma lepoll_well_ord: "[| A \<lesssim> B; well_ord(B,r) |] ==> \<exists>s. well_ord(A,s)"
paulson@13221
   183
apply (unfold lepoll_def)
paulson@13221
   184
apply (blast intro: well_ord_rvimage)
paulson@13221
   185
done
paulson@13221
   186
paulson@46821
   187
lemma lepoll_iff_leqpoll: "A \<lesssim> B \<longleftrightarrow> A \<prec> B | A \<approx> B"
paulson@13221
   188
apply (unfold lesspoll_def)
paulson@13221
   189
apply (blast intro!: eqpollI elim!: eqpollE)
paulson@13221
   190
done
paulson@13221
   191
paulson@46820
   192
lemma inj_not_surj_succ:
paulson@47042
   193
  assumes fi: "f \<in> inj(A, succ(m))" and fns: "f \<notin> surj(A, succ(m))" 
paulson@47042
   194
  shows "\<exists>f. f \<in> inj(A,m)"
paulson@47042
   195
proof -
paulson@47042
   196
  from fi [THEN inj_is_fun] fns 
paulson@47042
   197
  obtain y where y: "y \<in> succ(m)" "\<And>x. x\<in>A \<Longrightarrow> f ` x \<noteq> y"
paulson@47042
   198
    by (auto simp add: surj_def)
paulson@47042
   199
  show ?thesis
paulson@47042
   200
    proof 
paulson@47042
   201
      show "(\<lambda>z\<in>A. if f`z = m then y else f`z) \<in> inj(A, m)" using y fi
paulson@47042
   202
        by (simp add: inj_def) 
paulson@47042
   203
           (auto intro!: if_type [THEN lam_type] intro: Pi_type dest: apply_funtype)
paulson@47042
   204
      qed
paulson@47042
   205
qed
paulson@13221
   206
paulson@13221
   207
(** Variations on transitivity **)
paulson@13221
   208
paulson@46841
   209
lemma lesspoll_trans [trans]:
paulson@13221
   210
      "[| X \<prec> Y; Y \<prec> Z |] ==> X \<prec> Z"
paulson@13221
   211
apply (unfold lesspoll_def)
paulson@13221
   212
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
paulson@13221
   213
done
paulson@13221
   214
paulson@46841
   215
lemma lesspoll_trans1 [trans]:
paulson@13221
   216
      "[| X \<lesssim> Y; Y \<prec> Z |] ==> X \<prec> Z"
paulson@13221
   217
apply (unfold lesspoll_def)
paulson@13221
   218
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
paulson@13221
   219
done
paulson@13221
   220
paulson@46841
   221
lemma lesspoll_trans2 [trans]:
paulson@13221
   222
      "[| X \<prec> Y; Y \<lesssim> Z |] ==> X \<prec> Z"
paulson@13221
   223
apply (unfold lesspoll_def)
paulson@13221
   224
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
paulson@13221
   225
done
paulson@13221
   226
paulson@46841
   227
lemma eq_lesspoll_trans [trans]:
paulson@46841
   228
      "[| X \<approx> Y; Y \<prec> Z |] ==> X \<prec> Z"
paulson@46953
   229
  by (blast intro: eqpoll_imp_lepoll lesspoll_trans1)
paulson@46841
   230
paulson@46841
   231
lemma lesspoll_eq_trans [trans]:
paulson@46841
   232
      "[| X \<prec> Y; Y \<approx> Z |] ==> X \<prec> Z"
paulson@46953
   233
  by (blast intro: eqpoll_imp_lepoll lesspoll_trans2)
paulson@46841
   234
paulson@13221
   235
wenzelm@61394
   236
(** \<mu> -- the least number operator [from HOL/Univ.ML] **)
paulson@13221
   237
paulson@46820
   238
lemma Least_equality:
paulson@46847
   239
    "[| P(i);  Ord(i);  !!x. x<i ==> ~P(x) |] ==> (\<mu> x. P(x)) = i"
paulson@46820
   240
apply (unfold Least_def)
paulson@13221
   241
apply (rule the_equality, blast)
paulson@13221
   242
apply (elim conjE)
paulson@13221
   243
apply (erule Ord_linear_lt, assumption, blast+)
paulson@13221
   244
done
paulson@13221
   245
paulson@47016
   246
lemma LeastI: 
paulson@47016
   247
  assumes P: "P(i)" and i: "Ord(i)" shows "P(\<mu> x. P(x))"
paulson@47016
   248
proof -
paulson@47016
   249
  { from i have "P(i) \<Longrightarrow> P(\<mu> x. P(x))"
paulson@47016
   250
      proof (induct i rule: trans_induct)
paulson@47016
   251
        case (step i) 
paulson@47016
   252
        show ?case
paulson@47016
   253
          proof (cases "P(\<mu> a. P(a))")
paulson@47016
   254
            case True thus ?thesis .
paulson@47016
   255
          next
paulson@47016
   256
            case False
paulson@47016
   257
            hence "\<And>x. x \<in> i \<Longrightarrow> ~P(x)" using step
paulson@47016
   258
              by blast
paulson@47018
   259
            hence "(\<mu> a. P(a)) = i" using step
paulson@47018
   260
              by (blast intro: Least_equality ltD) 
paulson@47018
   261
            thus ?thesis using step.prems
paulson@47016
   262
              by simp 
paulson@47016
   263
          qed
paulson@47016
   264
      qed
paulson@47016
   265
  }
paulson@47016
   266
  thus ?thesis using P .
paulson@47016
   267
qed
paulson@13221
   268
wenzelm@60770
   269
text\<open>The proof is almost identical to the one above!\<close>
paulson@47018
   270
lemma Least_le: 
paulson@47018
   271
  assumes P: "P(i)" and i: "Ord(i)" shows "(\<mu> x. P(x)) \<le> i"
paulson@47018
   272
proof -
paulson@47018
   273
  { from i have "P(i) \<Longrightarrow> (\<mu> x. P(x)) \<le> i"
paulson@47018
   274
      proof (induct i rule: trans_induct)
paulson@47018
   275
        case (step i) 
paulson@47018
   276
        show ?case
paulson@47018
   277
          proof (cases "(\<mu> a. P(a)) \<le> i")
paulson@47018
   278
            case True thus ?thesis .
paulson@47018
   279
          next
paulson@47018
   280
            case False
paulson@47018
   281
            hence "\<And>x. x \<in> i \<Longrightarrow> ~ (\<mu> a. P(a)) \<le> i" using step
paulson@47018
   282
              by blast
paulson@47018
   283
            hence "(\<mu> a. P(a)) = i" using step
paulson@47018
   284
              by (blast elim: ltE intro: ltI Least_equality lt_trans1)
paulson@47018
   285
            thus ?thesis using step
paulson@47018
   286
              by simp 
paulson@47018
   287
          qed
paulson@47018
   288
      qed
paulson@47018
   289
  }
paulson@47018
   290
  thus ?thesis using P .
paulson@47018
   291
qed
paulson@13221
   292
wenzelm@61394
   293
(*\<mu> really is the smallest*)
paulson@46847
   294
lemma less_LeastE: "[| P(i);  i < (\<mu> x. P(x)) |] ==> Q"
paulson@13221
   295
apply (rule Least_le [THEN [2] lt_trans2, THEN lt_irrefl], assumption+)
paulson@46820
   296
apply (simp add: lt_Ord)
paulson@13221
   297
done
paulson@13221
   298
paulson@13221
   299
(*Easier to apply than LeastI: conclusion has only one occurrence of P*)
paulson@13221
   300
lemma LeastI2:
paulson@46847
   301
    "[| P(i);  Ord(i);  !!j. P(j) ==> Q(j) |] ==> Q(\<mu> j. P(j))"
paulson@46820
   302
by (blast intro: LeastI )
paulson@13221
   303
wenzelm@61394
   304
(*If there is no such P then \<mu> is vacuously 0*)
paulson@46820
   305
lemma Least_0:
paulson@46847
   306
    "[| ~ (\<exists>i. Ord(i) & P(i)) |] ==> (\<mu> x. P(x)) = 0"
paulson@13221
   307
apply (unfold Least_def)
paulson@13221
   308
apply (rule the_0, blast)
paulson@13221
   309
done
paulson@13221
   310
paulson@46847
   311
lemma Ord_Least [intro,simp,TC]: "Ord(\<mu> x. P(x))"
paulson@47042
   312
proof (cases "\<exists>i. Ord(i) & P(i)")
paulson@47042
   313
  case True 
paulson@47042
   314
  then obtain i where "P(i)" "Ord(i)"  by auto
paulson@47042
   315
  hence " (\<mu> x. P(x)) \<le> i"  by (rule Least_le) 
paulson@47042
   316
  thus ?thesis
paulson@47042
   317
    by (elim ltE)
paulson@47042
   318
next
paulson@47042
   319
  case False
paulson@47042
   320
  hence "(\<mu> x. P(x)) = 0"  by (rule Least_0)
paulson@47042
   321
  thus ?thesis
paulson@47042
   322
    by auto
paulson@47042
   323
qed
paulson@13221
   324
paulson@13221
   325
wenzelm@60770
   326
subsection\<open>Basic Properties of Cardinals\<close>
paulson@13221
   327
paulson@13221
   328
(*Not needed for simplification, but helpful below*)
paulson@46847
   329
lemma Least_cong: "(!!y. P(y) \<longleftrightarrow> Q(y)) ==> (\<mu> x. P(x)) = (\<mu> x. Q(x))"
paulson@13221
   330
by simp
paulson@13221
   331
paulson@46820
   332
(*Need AC to get @{term"X \<lesssim> Y ==> |X| \<le> |Y|"};  see well_ord_lepoll_imp_Card_le
paulson@13221
   333
  Converse also requires AC, but see well_ord_cardinal_eqE*)
paulson@13221
   334
lemma cardinal_cong: "X \<approx> Y ==> |X| = |Y|"
paulson@13221
   335
apply (unfold eqpoll_def cardinal_def)
paulson@13221
   336
apply (rule Least_cong)
paulson@13221
   337
apply (blast intro: comp_bij bij_converse_bij)
paulson@13221
   338
done
paulson@13221
   339
paulson@13221
   340
(*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*)
paulson@46820
   341
lemma well_ord_cardinal_eqpoll:
paulson@47018
   342
  assumes r: "well_ord(A,r)" shows "|A| \<approx> A"
paulson@47018
   343
proof (unfold cardinal_def)
paulson@47018
   344
  show "(\<mu> i. i \<approx> A) \<approx> A"
paulson@47018
   345
    by (best intro: LeastI Ord_ordertype ordermap_bij bij_converse_bij bij_imp_eqpoll r) 
paulson@47018
   346
qed
paulson@13221
   347
paulson@46820
   348
(* @{term"Ord(A) ==> |A| \<approx> A"} *)
paulson@13221
   349
lemmas Ord_cardinal_eqpoll = well_ord_Memrel [THEN well_ord_cardinal_eqpoll]
paulson@13221
   350
paulson@46841
   351
lemma Ord_cardinal_idem: "Ord(A) \<Longrightarrow> ||A|| = |A|"
paulson@46841
   352
 by (rule Ord_cardinal_eqpoll [THEN cardinal_cong])
paulson@46841
   353
paulson@13221
   354
lemma well_ord_cardinal_eqE:
paulson@46953
   355
  assumes woX: "well_ord(X,r)" and woY: "well_ord(Y,s)" and eq: "|X| = |Y|"
paulson@46847
   356
shows "X \<approx> Y"
paulson@46847
   357
proof -
paulson@46953
   358
  have "X \<approx> |X|" by (blast intro: well_ord_cardinal_eqpoll [OF woX] eqpoll_sym)
paulson@46847
   359
  also have "... = |Y|" by (rule eq)
paulson@46953
   360
  also have "... \<approx> Y" by (rule well_ord_cardinal_eqpoll [OF woY])
paulson@46847
   361
  finally show ?thesis .
paulson@46847
   362
qed
paulson@13221
   363
paulson@13221
   364
lemma well_ord_cardinal_eqpoll_iff:
paulson@46821
   365
     "[| well_ord(X,r);  well_ord(Y,s) |] ==> |X| = |Y| \<longleftrightarrow> X \<approx> Y"
paulson@13221
   366
by (blast intro: cardinal_cong well_ord_cardinal_eqE)
paulson@13221
   367
paulson@13221
   368
paulson@13221
   369
(** Observations from Kunen, page 28 **)
paulson@13221
   370
paulson@46820
   371
lemma Ord_cardinal_le: "Ord(i) ==> |i| \<le> i"
paulson@13221
   372
apply (unfold cardinal_def)
paulson@13221
   373
apply (erule eqpoll_refl [THEN Least_le])
paulson@13221
   374
done
paulson@13221
   375
paulson@13221
   376
lemma Card_cardinal_eq: "Card(K) ==> |K| = K"
paulson@13221
   377
apply (unfold Card_def)
paulson@13221
   378
apply (erule sym)
paulson@13221
   379
done
paulson@13221
   380
paulson@46841
   381
(* Could replace the  @{term"~(j \<approx> i)"}  by  @{term"~(i \<preceq> j)"}. *)
paulson@13221
   382
lemma CardI: "[| Ord(i);  !!j. j<i ==> ~(j \<approx> i) |] ==> Card(i)"
paulson@46820
   383
apply (unfold Card_def cardinal_def)
paulson@13221
   384
apply (subst Least_equality)
paulson@47018
   385
apply (blast intro: eqpoll_refl)+
paulson@13221
   386
done
paulson@13221
   387
paulson@13221
   388
lemma Card_is_Ord: "Card(i) ==> Ord(i)"
paulson@13221
   389
apply (unfold Card_def cardinal_def)
paulson@13221
   390
apply (erule ssubst)
paulson@13221
   391
apply (rule Ord_Least)
paulson@13221
   392
done
paulson@13221
   393
paulson@46820
   394
lemma Card_cardinal_le: "Card(K) ==> K \<le> |K|"
paulson@13221
   395
apply (simp (no_asm_simp) add: Card_is_Ord Card_cardinal_eq)
paulson@13221
   396
done
paulson@13221
   397
paulson@13221
   398
lemma Ord_cardinal [simp,intro!]: "Ord(|A|)"
paulson@13221
   399
apply (unfold cardinal_def)
paulson@13221
   400
apply (rule Ord_Least)
paulson@13221
   401
done
paulson@13221
   402
wenzelm@60770
   403
text\<open>The cardinals are the initial ordinals.\<close>
paulson@46821
   404
lemma Card_iff_initial: "Card(K) \<longleftrightarrow> Ord(K) & (\<forall>j. j<K \<longrightarrow> ~ j \<approx> K)"
paulson@47018
   405
proof -
paulson@47018
   406
  { fix j
paulson@47018
   407
    assume K: "Card(K)" "j \<approx> K"
paulson@47018
   408
    assume "j < K"
paulson@47018
   409
    also have "... = (\<mu> i. i \<approx> K)" using K
paulson@47018
   410
      by (simp add: Card_def cardinal_def)
paulson@47018
   411
    finally have "j < (\<mu> i. i \<approx> K)" .
paulson@47018
   412
    hence "False" using K
paulson@47018
   413
      by (best dest: less_LeastE) 
paulson@47018
   414
  }
paulson@47018
   415
  then show ?thesis
paulson@47042
   416
    by (blast intro: CardI Card_is_Ord) 
paulson@47018
   417
qed
paulson@13221
   418
paulson@13221
   419
lemma lt_Card_imp_lesspoll: "[| Card(a); i<a |] ==> i \<prec> a"
paulson@13221
   420
apply (unfold lesspoll_def)
paulson@13221
   421
apply (drule Card_iff_initial [THEN iffD1])
paulson@13221
   422
apply (blast intro!: leI [THEN le_imp_lepoll])
paulson@13221
   423
done
paulson@13221
   424
paulson@13221
   425
lemma Card_0: "Card(0)"
paulson@13221
   426
apply (rule Ord_0 [THEN CardI])
paulson@13221
   427
apply (blast elim!: ltE)
paulson@13221
   428
done
paulson@13221
   429
paulson@46820
   430
lemma Card_Un: "[| Card(K);  Card(L) |] ==> Card(K \<union> L)"
paulson@13221
   431
apply (rule Ord_linear_le [of K L])
paulson@13221
   432
apply (simp_all add: subset_Un_iff [THEN iffD1]  Card_is_Ord le_imp_subset
paulson@13221
   433
                     subset_Un_iff2 [THEN iffD1])
paulson@13221
   434
done
paulson@13221
   435
paulson@13221
   436
(*Infinite unions of cardinals?  See Devlin, Lemma 6.7, page 98*)
paulson@13221
   437
paulson@47101
   438
lemma Card_cardinal [iff]: "Card(|A|)"
paulson@46847
   439
proof (unfold cardinal_def)
paulson@46847
   440
  show "Card(\<mu> i. i \<approx> A)"
paulson@46847
   441
    proof (cases "\<exists>i. Ord (i) & i \<approx> A")
wenzelm@61798
   442
      case False thus ?thesis           \<comment>\<open>degenerate case\<close>
paulson@46847
   443
        by (simp add: Least_0 Card_0)
paulson@46847
   444
    next
wenzelm@61798
   445
      case True                         \<comment>\<open>real case: @{term A} is isomorphic to some ordinal\<close>
paulson@46847
   446
      then obtain i where i: "Ord(i)" "i \<approx> A" by blast
paulson@46953
   447
      show ?thesis
paulson@46847
   448
        proof (rule CardI [OF Ord_Least], rule notI)
paulson@46847
   449
          fix j
paulson@46953
   450
          assume j: "j < (\<mu> i. i \<approx> A)"
paulson@46847
   451
          assume "j \<approx> (\<mu> i. i \<approx> A)"
paulson@46847
   452
          also have "... \<approx> A" using i by (auto intro: LeastI)
paulson@46847
   453
          finally have "j \<approx> A" .
paulson@46953
   454
          thus False
paulson@46847
   455
            by (rule less_LeastE [OF _ j])
paulson@46847
   456
        qed
paulson@46847
   457
    qed
paulson@46847
   458
qed
paulson@13221
   459
paulson@13221
   460
(*Kunen's Lemma 10.5*)
paulson@46953
   461
lemma cardinal_eq_lemma:
paulson@46841
   462
  assumes i:"|i| \<le> j" and j: "j \<le> i" shows "|j| = |i|"
paulson@46841
   463
proof (rule eqpollI [THEN cardinal_cong])
paulson@46841
   464
  show "j \<lesssim> i" by (rule le_imp_lepoll [OF j])
paulson@46841
   465
next
paulson@46841
   466
  have Oi: "Ord(i)" using j by (rule le_Ord2)
paulson@46953
   467
  hence "i \<approx> |i|"
paulson@46953
   468
    by (blast intro: Ord_cardinal_eqpoll eqpoll_sym)
paulson@46953
   469
  also have "... \<lesssim> j"
paulson@46953
   470
    by (blast intro: le_imp_lepoll i)
paulson@46841
   471
  finally show "i \<lesssim> j" .
paulson@46841
   472
qed
paulson@13221
   473
paulson@46953
   474
lemma cardinal_mono:
paulson@46877
   475
  assumes ij: "i \<le> j" shows "|i| \<le> |j|"
paulson@47016
   476
using Ord_cardinal [of i] Ord_cardinal [of j]
paulson@47016
   477
proof (cases rule: Ord_linear_le)
paulson@47016
   478
  case le thus ?thesis .
paulson@46877
   479
next
paulson@47016
   480
  case ge
paulson@46877
   481
  have i: "Ord(i)" using ij
paulson@46953
   482
    by (simp add: lt_Ord)
paulson@46953
   483
  have ci: "|i| \<le> j"
paulson@46953
   484
    by (blast intro: Ord_cardinal_le ij le_trans i)
paulson@46953
   485
  have "|i| = ||i||"
paulson@46953
   486
    by (auto simp add: Ord_cardinal_idem i)
paulson@46877
   487
  also have "... = |j|"
paulson@47016
   488
    by (rule cardinal_eq_lemma [OF ge ci])
paulson@46877
   489
  finally have "|i| = |j|" .
paulson@46877
   490
  thus ?thesis by simp
paulson@46877
   491
qed
paulson@13221
   492
wenzelm@61798
   493
text\<open>Since we have @{term"|succ(nat)| \<le> |nat|"}, the converse of \<open>cardinal_mono\<close> fails!\<close>
paulson@13221
   494
lemma cardinal_lt_imp_lt: "[| |i| < |j|;  Ord(i);  Ord(j) |] ==> i < j"
paulson@13221
   495
apply (rule Ord_linear2 [of i j], assumption+)
paulson@13221
   496
apply (erule lt_trans2 [THEN lt_irrefl])
paulson@13221
   497
apply (erule cardinal_mono)
paulson@13221
   498
done
paulson@13221
   499
paulson@13221
   500
lemma Card_lt_imp_lt: "[| |i| < K;  Ord(i);  Card(K) |] ==> i < K"
paulson@46877
   501
  by (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq)
paulson@13221
   502
paulson@46821
   503
lemma Card_lt_iff: "[| Ord(i);  Card(K) |] ==> (|i| < K) \<longleftrightarrow> (i < K)"
paulson@13221
   504
by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1])
paulson@13221
   505
paulson@46821
   506
lemma Card_le_iff: "[| Ord(i);  Card(K) |] ==> (K \<le> |i|) \<longleftrightarrow> (K \<le> i)"
paulson@13269
   507
by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
paulson@13221
   508
paulson@13221
   509
(*Can use AC or finiteness to discharge first premise*)
paulson@13221
   510
lemma well_ord_lepoll_imp_Card_le:
paulson@46841
   511
  assumes wB: "well_ord(B,r)" and AB: "A \<lesssim> B"
paulson@46841
   512
  shows "|A| \<le> |B|"
paulson@47016
   513
using Ord_cardinal [of A] Ord_cardinal [of B]
paulson@47016
   514
proof (cases rule: Ord_linear_le)
paulson@47016
   515
  case le thus ?thesis .
paulson@47016
   516
next
paulson@47016
   517
  case ge
paulson@46841
   518
  from lepoll_well_ord [OF AB wB]
paulson@46841
   519
  obtain s where s: "well_ord(A, s)" by blast
paulson@46953
   520
  have "B  \<approx> |B|" by (blast intro: wB eqpoll_sym well_ord_cardinal_eqpoll)
paulson@47016
   521
  also have "... \<lesssim> |A|" by (rule le_imp_lepoll [OF ge])
paulson@46841
   522
  also have "... \<approx> A" by (rule well_ord_cardinal_eqpoll [OF s])
paulson@46841
   523
  finally have "B \<lesssim> A" .
paulson@46953
   524
  hence "A \<approx> B" by (blast intro: eqpollI AB)
paulson@46841
   525
  hence "|A| = |B|" by (rule cardinal_cong)
paulson@46841
   526
  thus ?thesis by simp
paulson@46841
   527
qed
paulson@13221
   528
paulson@46820
   529
lemma lepoll_cardinal_le: "[| A \<lesssim> i; Ord(i) |] ==> |A| \<le> i"
paulson@13221
   530
apply (rule le_trans)
paulson@13221
   531
apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption)
paulson@13221
   532
apply (erule Ord_cardinal_le)
paulson@13221
   533
done
paulson@13221
   534
paulson@13221
   535
lemma lepoll_Ord_imp_eqpoll: "[| A \<lesssim> i; Ord(i) |] ==> |A| \<approx> A"
paulson@13221
   536
by (blast intro: lepoll_cardinal_le well_ord_Memrel well_ord_cardinal_eqpoll dest!: lepoll_well_ord)
paulson@13221
   537
paulson@14046
   538
lemma lesspoll_imp_eqpoll: "[| A \<prec> i; Ord(i) |] ==> |A| \<approx> A"
paulson@13221
   539
apply (unfold lesspoll_def)
paulson@13221
   540
apply (blast intro: lepoll_Ord_imp_eqpoll)
paulson@13221
   541
done
paulson@13221
   542
paulson@46820
   543
lemma cardinal_subset_Ord: "[|A<=i; Ord(i)|] ==> |A| \<subseteq> i"
paulson@14046
   544
apply (drule subset_imp_lepoll [THEN lepoll_cardinal_le])
paulson@14046
   545
apply (auto simp add: lt_def)
paulson@14046
   546
apply (blast intro: Ord_trans)
paulson@14046
   547
done
paulson@13221
   548
wenzelm@60770
   549
subsection\<open>The finite cardinals\<close>
paulson@13221
   550
paulson@46820
   551
lemma cons_lepoll_consD:
paulson@46820
   552
 "[| cons(u,A) \<lesssim> cons(v,B);  u\<notin>A;  v\<notin>B |] ==> A \<lesssim> B"
paulson@13221
   553
apply (unfold lepoll_def inj_def, safe)
paulson@46820
   554
apply (rule_tac x = "\<lambda>x\<in>A. if f`x=v then f`u else f`x" in exI)
paulson@13221
   555
apply (rule CollectI)
paulson@13221
   556
(*Proving it's in the function space A->B*)
paulson@13221
   557
apply (rule if_type [THEN lam_type])
paulson@13221
   558
apply (blast dest: apply_funtype)
paulson@13221
   559
apply (blast elim!: mem_irrefl dest: apply_funtype)
paulson@13221
   560
(*Proving it's injective*)
paulson@13221
   561
apply (simp (no_asm_simp))
paulson@13221
   562
apply blast
paulson@13221
   563
done
paulson@13221
   564
paulson@46820
   565
lemma cons_eqpoll_consD: "[| cons(u,A) \<approx> cons(v,B);  u\<notin>A;  v\<notin>B |] ==> A \<approx> B"
paulson@13221
   566
apply (simp add: eqpoll_iff)
paulson@13221
   567
apply (blast intro: cons_lepoll_consD)
paulson@13221
   568
done
paulson@13221
   569
paulson@13221
   570
(*Lemma suggested by Mike Fourman*)
paulson@13221
   571
lemma succ_lepoll_succD: "succ(m) \<lesssim> succ(n) ==> m \<lesssim> n"
paulson@13221
   572
apply (unfold succ_def)
paulson@13221
   573
apply (erule cons_lepoll_consD)
paulson@13221
   574
apply (rule mem_not_refl)+
paulson@13221
   575
done
paulson@13221
   576
paulson@46877
   577
paulson@46935
   578
lemma nat_lepoll_imp_le:
paulson@46935
   579
     "m \<in> nat ==> n \<in> nat \<Longrightarrow> m \<lesssim> n \<Longrightarrow> m \<le> n"
paulson@46935
   580
proof (induct m arbitrary: n rule: nat_induct)
paulson@46935
   581
  case 0 thus ?case by (blast intro!: nat_0_le)
paulson@46935
   582
next
paulson@46935
   583
  case (succ m)
wenzelm@60770
   584
  show ?case  using \<open>n \<in> nat\<close>
paulson@46935
   585
    proof (cases rule: natE)
paulson@46935
   586
      case 0 thus ?thesis using succ
paulson@46935
   587
        by (simp add: lepoll_def inj_def)
paulson@46935
   588
    next
wenzelm@60770
   589
      case (succ n') thus ?thesis using succ.hyps \<open> succ(m) \<lesssim> n\<close>
paulson@46935
   590
        by (blast intro!: succ_leI dest!: succ_lepoll_succD)
paulson@46935
   591
    qed
paulson@46935
   592
qed
paulson@13221
   593
paulson@46953
   594
lemma nat_eqpoll_iff: "[| m \<in> nat; n \<in> nat |] ==> m \<approx> n \<longleftrightarrow> m = n"
paulson@13221
   595
apply (rule iffI)
paulson@13221
   596
apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE)
paulson@13221
   597
apply (simp add: eqpoll_refl)
paulson@13221
   598
done
paulson@13221
   599
paulson@13221
   600
(*The object of all this work: every natural number is a (finite) cardinal*)
paulson@46820
   601
lemma nat_into_Card:
paulson@47042
   602
  assumes n: "n \<in> nat" shows "Card(n)"
paulson@47042
   603
proof (unfold Card_def cardinal_def, rule sym)
paulson@47042
   604
  have "Ord(n)" using n  by auto
paulson@47042
   605
  moreover
paulson@47042
   606
  { fix i
paulson@47042
   607
    assume "i < n" "i \<approx> n"
paulson@47042
   608
    hence False using n
paulson@47042
   609
      by (auto simp add: lt_nat_in_nat [THEN nat_eqpoll_iff])
paulson@47042
   610
  }
paulson@47042
   611
  ultimately show "(\<mu> i. i \<approx> n) = n" by (auto intro!: Least_equality) 
paulson@47042
   612
qed
paulson@13221
   613
paulson@13221
   614
lemmas cardinal_0 = nat_0I [THEN nat_into_Card, THEN Card_cardinal_eq, iff]
paulson@13221
   615
lemmas cardinal_1 = nat_1I [THEN nat_into_Card, THEN Card_cardinal_eq, iff]
paulson@13221
   616
paulson@13221
   617
paulson@13221
   618
(*Part of Kunen's Lemma 10.6*)
paulson@46877
   619
lemma succ_lepoll_natE: "[| succ(n) \<lesssim> n;  n \<in> nat |] ==> P"
paulson@13221
   620
by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto)
paulson@13221
   621
paulson@46820
   622
lemma nat_lepoll_imp_ex_eqpoll_n:
paulson@13221
   623
     "[| n \<in> nat;  nat \<lesssim> X |] ==> \<exists>Y. Y \<subseteq> X & n \<approx> Y"
paulson@13221
   624
apply (unfold lepoll_def eqpoll_def)
paulson@13221
   625
apply (fast del: subsetI subsetCE
paulson@13221
   626
            intro!: subset_SIs
paulson@13221
   627
            dest!: Ord_nat [THEN [2] OrdmemD, THEN [2] restrict_inj]
paulson@46820
   628
            elim!: restrict_bij
paulson@13221
   629
                   inj_is_fun [THEN fun_is_rel, THEN image_subset])
paulson@13221
   630
done
paulson@13221
   631
paulson@13221
   632
wenzelm@61394
   633
(** \<lesssim>, \<prec> and natural numbers **)
paulson@13221
   634
paulson@46877
   635
lemma lepoll_succ: "i \<lesssim> succ(i)"
paulson@46877
   636
  by (blast intro: subset_imp_lepoll)
paulson@46877
   637
paulson@46820
   638
lemma lepoll_imp_lesspoll_succ:
paulson@46877
   639
  assumes A: "A \<lesssim> m" and m: "m \<in> nat"
paulson@46877
   640
  shows "A \<prec> succ(m)"
paulson@46877
   641
proof -
paulson@46953
   642
  { assume "A \<approx> succ(m)"
paulson@46877
   643
    hence "succ(m) \<approx> A" by (rule eqpoll_sym)
paulson@46877
   644
    also have "... \<lesssim> m" by (rule A)
paulson@46877
   645
    finally have "succ(m) \<lesssim> m" .
paulson@46877
   646
    hence False by (rule succ_lepoll_natE) (rule m) }
paulson@46877
   647
  moreover have "A \<lesssim> succ(m)" by (blast intro: lepoll_trans A lepoll_succ)
paulson@46953
   648
  ultimately show ?thesis by (auto simp add: lesspoll_def)
paulson@46877
   649
qed
paulson@46877
   650
paulson@46877
   651
lemma lesspoll_succ_imp_lepoll:
paulson@46877
   652
     "[| A \<prec> succ(m); m \<in> nat |] ==> A \<lesssim> m"
paulson@46877
   653
apply (unfold lesspoll_def lepoll_def eqpoll_def bij_def)
paulson@46877
   654
apply (auto dest: inj_not_surj_succ)
paulson@13221
   655
done
paulson@13221
   656
paulson@46877
   657
lemma lesspoll_succ_iff: "m \<in> nat ==> A \<prec> succ(m) \<longleftrightarrow> A \<lesssim> m"
paulson@13221
   658
by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll)
paulson@13221
   659
paulson@46877
   660
lemma lepoll_succ_disj: "[| A \<lesssim> succ(m);  m \<in> nat |] ==> A \<lesssim> m | A \<approx> succ(m)"
paulson@13221
   661
apply (rule disjCI)
paulson@13221
   662
apply (rule lesspoll_succ_imp_lepoll)
paulson@13221
   663
prefer 2 apply assumption
paulson@13221
   664
apply (simp (no_asm_simp) add: lesspoll_def)
paulson@13221
   665
done
paulson@13221
   666
paulson@13221
   667
lemma lesspoll_cardinal_lt: "[| A \<prec> i; Ord(i) |] ==> |A| < i"
paulson@13221
   668
apply (unfold lesspoll_def, clarify)
paulson@13221
   669
apply (frule lepoll_cardinal_le, assumption)
paulson@13221
   670
apply (blast intro: well_ord_Memrel well_ord_cardinal_eqpoll [THEN eqpoll_sym]
paulson@13221
   671
             dest: lepoll_well_ord  elim!: leE)
paulson@13221
   672
done
paulson@13221
   673
paulson@13221
   674
wenzelm@60770
   675
subsection\<open>The first infinite cardinal: Omega, or nat\<close>
paulson@13221
   676
paulson@13221
   677
(*This implies Kunen's Lemma 10.6*)
paulson@46877
   678
lemma lt_not_lepoll:
paulson@46877
   679
  assumes n: "n<i" "n \<in> nat" shows "~ i \<lesssim> n"
paulson@46877
   680
proof -
paulson@46877
   681
  { assume i: "i \<lesssim> n"
paulson@46877
   682
    have "succ(n) \<lesssim> i" using n
paulson@46953
   683
      by (elim ltE, blast intro: Ord_succ_subsetI [THEN subset_imp_lepoll])
paulson@46877
   684
    also have "... \<lesssim> n" by (rule i)
paulson@46877
   685
    finally have "succ(n) \<lesssim> n" .
paulson@46877
   686
    hence False  by (rule succ_lepoll_natE) (rule n) }
paulson@46877
   687
  thus ?thesis by auto
paulson@46877
   688
qed
paulson@13221
   689
wenzelm@61798
   690
text\<open>A slightly weaker version of \<open>nat_eqpoll_iff\<close>\<close>
paulson@46877
   691
lemma Ord_nat_eqpoll_iff:
paulson@46877
   692
  assumes i: "Ord(i)" and n: "n \<in> nat" shows "i \<approx> n \<longleftrightarrow> i=n"
paulson@47016
   693
using i nat_into_Ord [OF n]
paulson@47016
   694
proof (cases rule: Ord_linear_lt)
paulson@47016
   695
  case lt
paulson@46877
   696
  hence  "i \<in> nat" by (rule lt_nat_in_nat) (rule n)
paulson@46953
   697
  thus ?thesis by (simp add: nat_eqpoll_iff n)
paulson@46877
   698
next
paulson@47016
   699
  case eq
paulson@46953
   700
  thus ?thesis by (simp add: eqpoll_refl)
paulson@46877
   701
next
paulson@47016
   702
  case gt
paulson@46953
   703
  hence  "~ i \<lesssim> n" using n  by (rule lt_not_lepoll)
paulson@46877
   704
  hence  "~ i \<approx> n" using n  by (blast intro: eqpoll_imp_lepoll)
wenzelm@60770
   705
  moreover have "i \<noteq> n" using \<open>n<i\<close> by auto
paulson@46877
   706
  ultimately show ?thesis by blast
paulson@46877
   707
qed
paulson@13221
   708
paulson@13221
   709
lemma Card_nat: "Card(nat)"
paulson@46877
   710
proof -
paulson@46877
   711
  { fix i
paulson@46953
   712
    assume i: "i < nat" "i \<approx> nat"
paulson@46953
   713
    hence "~ nat \<lesssim> i"
paulson@46953
   714
      by (simp add: lt_def lt_not_lepoll)
paulson@46953
   715
    hence False using i
paulson@46877
   716
      by (simp add: eqpoll_iff)
paulson@46877
   717
  }
paulson@46953
   718
  hence "(\<mu> i. i \<approx> nat) = nat" by (blast intro: Least_equality eqpoll_refl)
paulson@46877
   719
  thus ?thesis
paulson@46953
   720
    by (auto simp add: Card_def cardinal_def)
paulson@46877
   721
qed
paulson@13221
   722
paulson@13221
   723
(*Allows showing that |i| is a limit cardinal*)
paulson@46820
   724
lemma nat_le_cardinal: "nat \<le> i ==> nat \<le> |i|"
paulson@13221
   725
apply (rule Card_nat [THEN Card_cardinal_eq, THEN subst])
paulson@13221
   726
apply (erule cardinal_mono)
paulson@13221
   727
done
paulson@13221
   728
paulson@46841
   729
lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
paulson@46841
   730
  by (blast intro: Ord_nat Card_nat ltI lt_Card_imp_lesspoll)
paulson@46841
   731
paulson@13221
   732
wenzelm@60770
   733
subsection\<open>Towards Cardinal Arithmetic\<close>
paulson@13221
   734
(** Congruence laws for successor, cardinal addition and multiplication **)
paulson@13221
   735
paulson@13221
   736
(*Congruence law for  cons  under equipollence*)
paulson@46820
   737
lemma cons_lepoll_cong:
paulson@46820
   738
    "[| A \<lesssim> B;  b \<notin> B |] ==> cons(a,A) \<lesssim> cons(b,B)"
paulson@13221
   739
apply (unfold lepoll_def, safe)
paulson@46820
   740
apply (rule_tac x = "\<lambda>y\<in>cons (a,A) . if y=a then b else f`y" in exI)
paulson@46953
   741
apply (rule_tac d = "%z. if z \<in> B then converse (f) `z else a" in lam_injective)
paulson@46820
   742
apply (safe elim!: consE')
paulson@13221
   743
   apply simp_all
paulson@46820
   744
apply (blast intro: inj_is_fun [THEN apply_type])+
paulson@13221
   745
done
paulson@13221
   746
paulson@13221
   747
lemma cons_eqpoll_cong:
paulson@46820
   748
     "[| A \<approx> B;  a \<notin> A;  b \<notin> B |] ==> cons(a,A) \<approx> cons(b,B)"
paulson@13221
   749
by (simp add: eqpoll_iff cons_lepoll_cong)
paulson@13221
   750
paulson@13221
   751
lemma cons_lepoll_cons_iff:
paulson@46821
   752
     "[| a \<notin> A;  b \<notin> B |] ==> cons(a,A) \<lesssim> cons(b,B)  \<longleftrightarrow>  A \<lesssim> B"
paulson@13221
   753
by (blast intro: cons_lepoll_cong cons_lepoll_consD)
paulson@13221
   754
paulson@13221
   755
lemma cons_eqpoll_cons_iff:
paulson@46821
   756
     "[| a \<notin> A;  b \<notin> B |] ==> cons(a,A) \<approx> cons(b,B)  \<longleftrightarrow>  A \<approx> B"
paulson@13221
   757
by (blast intro: cons_eqpoll_cong cons_eqpoll_consD)
paulson@13221
   758
paulson@13221
   759
lemma singleton_eqpoll_1: "{a} \<approx> 1"
paulson@13221
   760
apply (unfold succ_def)
paulson@13221
   761
apply (blast intro!: eqpoll_refl [THEN cons_eqpoll_cong])
paulson@13221
   762
done
paulson@13221
   763
paulson@13221
   764
lemma cardinal_singleton: "|{a}| = 1"
paulson@13221
   765
apply (rule singleton_eqpoll_1 [THEN cardinal_cong, THEN trans])
paulson@13221
   766
apply (simp (no_asm) add: nat_into_Card [THEN Card_cardinal_eq])
paulson@13221
   767
done
paulson@13221
   768
paulson@46820
   769
lemma not_0_is_lepoll_1: "A \<noteq> 0 ==> 1 \<lesssim> A"
paulson@13221
   770
apply (erule not_emptyE)
paulson@13221
   771
apply (rule_tac a = "cons (x, A-{x}) " in subst)
paulson@13221
   772
apply (rule_tac [2] a = "cons(0,0)" and P= "%y. y \<lesssim> cons (x, A-{x})" in subst)
paulson@13221
   773
prefer 3 apply (blast intro: cons_lepoll_cong subset_imp_lepoll, auto)
paulson@13221
   774
done
paulson@13221
   775
paulson@13221
   776
(*Congruence law for  succ  under equipollence*)
paulson@13221
   777
lemma succ_eqpoll_cong: "A \<approx> B ==> succ(A) \<approx> succ(B)"
paulson@13221
   778
apply (unfold succ_def)
paulson@13221
   779
apply (simp add: cons_eqpoll_cong mem_not_refl)
paulson@13221
   780
done
paulson@13221
   781
paulson@13221
   782
(*Congruence law for + under equipollence*)
paulson@13221
   783
lemma sum_eqpoll_cong: "[| A \<approx> C;  B \<approx> D |] ==> A+B \<approx> C+D"
paulson@13221
   784
apply (unfold eqpoll_def)
paulson@13221
   785
apply (blast intro!: sum_bij)
paulson@13221
   786
done
paulson@13221
   787
paulson@13221
   788
(*Congruence law for * under equipollence*)
paulson@46820
   789
lemma prod_eqpoll_cong:
paulson@13221
   790
    "[| A \<approx> C;  B \<approx> D |] ==> A*B \<approx> C*D"
paulson@13221
   791
apply (unfold eqpoll_def)
paulson@13221
   792
apply (blast intro!: prod_bij)
paulson@13221
   793
done
paulson@13221
   794
paulson@46820
   795
lemma inj_disjoint_eqpoll:
paulson@46953
   796
    "[| f \<in> inj(A,B);  A \<inter> B = 0 |] ==> A \<union> (B - range(f)) \<approx> B"
paulson@13221
   797
apply (unfold eqpoll_def)
paulson@13221
   798
apply (rule exI)
paulson@46953
   799
apply (rule_tac c = "%x. if x \<in> A then f`x else x"
paulson@46953
   800
            and d = "%y. if y \<in> range (f) then converse (f) `y else y"
paulson@13221
   801
       in lam_bijective)
paulson@13221
   802
apply (blast intro!: if_type inj_is_fun [THEN apply_type])
paulson@13221
   803
apply (simp (no_asm_simp) add: inj_converse_fun [THEN apply_funtype])
paulson@46820
   804
apply (safe elim!: UnE')
paulson@13221
   805
   apply (simp_all add: inj_is_fun [THEN apply_rangeI])
paulson@46820
   806
apply (blast intro: inj_converse_fun [THEN apply_type])+
paulson@13221
   807
done
paulson@13221
   808
paulson@13221
   809
wenzelm@60770
   810
subsection\<open>Lemmas by Krzysztof Grabczewski\<close>
paulson@13356
   811
paulson@13356
   812
(*New proofs using cons_lepoll_cons. Could generalise from succ to cons.*)
paulson@13221
   813
wenzelm@60770
   814
text\<open>If @{term A} has at most @{term"n+1"} elements and @{term"a \<in> A"}
wenzelm@60770
   815
      then @{term"A-{a}"} has at most @{term n}.\<close>
paulson@46820
   816
lemma Diff_sing_lepoll:
paulson@46877
   817
      "[| a \<in> A;  A \<lesssim> succ(n) |] ==> A - {a} \<lesssim> n"
paulson@13221
   818
apply (unfold succ_def)
paulson@13221
   819
apply (rule cons_lepoll_consD)
paulson@13221
   820
apply (rule_tac [3] mem_not_refl)
paulson@13221
   821
apply (erule cons_Diff [THEN ssubst], safe)
paulson@13221
   822
done
paulson@13221
   823
wenzelm@60770
   824
text\<open>If @{term A} has at least @{term"n+1"} elements then @{term"A-{a}"} has at least @{term n}.\<close>
paulson@46820
   825
lemma lepoll_Diff_sing:
paulson@46877
   826
  assumes A: "succ(n) \<lesssim> A" shows "n \<lesssim> A - {a}"
paulson@46877
   827
proof -
paulson@46877
   828
  have "cons(n,n) \<lesssim> A" using A
paulson@46877
   829
    by (unfold succ_def)
paulson@46953
   830
  also have "... \<lesssim> cons(a, A-{a})"
paulson@46877
   831
    by (blast intro: subset_imp_lepoll)
paulson@46877
   832
  finally have "cons(n,n) \<lesssim> cons(a, A-{a})" .
paulson@46877
   833
  thus ?thesis
paulson@46953
   834
    by (blast intro: cons_lepoll_consD mem_irrefl)
paulson@46877
   835
qed
paulson@13221
   836
paulson@46877
   837
lemma Diff_sing_eqpoll: "[| a \<in> A; A \<approx> succ(n) |] ==> A - {a} \<approx> n"
paulson@46820
   838
by (blast intro!: eqpollI
paulson@46820
   839
          elim!: eqpollE
paulson@13221
   840
          intro: Diff_sing_lepoll lepoll_Diff_sing)
paulson@13221
   841
paulson@46877
   842
lemma lepoll_1_is_sing: "[| A \<lesssim> 1; a \<in> A |] ==> A = {a}"
paulson@13221
   843
apply (frule Diff_sing_lepoll, assumption)
paulson@13221
   844
apply (drule lepoll_0_is_0)
paulson@13221
   845
apply (blast elim: equalityE)
paulson@13221
   846
done
paulson@13221
   847
paulson@46820
   848
lemma Un_lepoll_sum: "A \<union> B \<lesssim> A+B"
paulson@13221
   849
apply (unfold lepoll_def)
paulson@46877
   850
apply (rule_tac x = "\<lambda>x\<in>A \<union> B. if x\<in>A then Inl (x) else Inr (x)" in exI)
paulson@46877
   851
apply (rule_tac d = "%z. snd (z)" in lam_injective)
paulson@46820
   852
apply force
paulson@13221
   853
apply (simp add: Inl_def Inr_def)
paulson@13221
   854
done
paulson@13221
   855
paulson@13221
   856
lemma well_ord_Un:
paulson@46820
   857
     "[| well_ord(X,R); well_ord(Y,S) |] ==> \<exists>T. well_ord(X \<union> Y, T)"
paulson@46820
   858
by (erule well_ord_radd [THEN Un_lepoll_sum [THEN lepoll_well_ord]],
paulson@13221
   859
    assumption)
paulson@13221
   860
paulson@13221
   861
(*Krzysztof Grabczewski*)
paulson@46820
   862
lemma disj_Un_eqpoll_sum: "A \<inter> B = 0 ==> A \<union> B \<approx> A + B"
paulson@13221
   863
apply (unfold eqpoll_def)
paulson@46877
   864
apply (rule_tac x = "\<lambda>a\<in>A \<union> B. if a \<in> A then Inl (a) else Inr (a)" in exI)
paulson@46877
   865
apply (rule_tac d = "%z. case (%x. x, %x. x, z)" in lam_bijective)
paulson@13221
   866
apply auto
paulson@13221
   867
done
paulson@13221
   868
paulson@13221
   869
wenzelm@60770
   870
subsection \<open>Finite and infinite sets\<close>
paulson@13221
   871
paulson@47018
   872
lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) \<longleftrightarrow> Finite(B)"
paulson@47018
   873
apply (unfold Finite_def)
paulson@47018
   874
apply (blast intro: eqpoll_trans eqpoll_sym)
paulson@47018
   875
done
paulson@47018
   876
paulson@13244
   877
lemma Finite_0 [simp]: "Finite(0)"
paulson@13221
   878
apply (unfold Finite_def)
paulson@13221
   879
apply (blast intro!: eqpoll_refl nat_0I)
paulson@13221
   880
done
paulson@13221
   881
paulson@47018
   882
lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))"
paulson@13221
   883
apply (unfold Finite_def)
paulson@47018
   884
apply (case_tac "y \<in> x")
paulson@47018
   885
apply (simp add: cons_absorb)
paulson@47018
   886
apply (erule bexE)
paulson@47018
   887
apply (rule bexI)
paulson@47018
   888
apply (erule_tac [2] nat_succI)
paulson@47018
   889
apply (simp (no_asm_simp) add: succ_def cons_eqpoll_cong mem_not_refl)
paulson@47018
   890
done
paulson@47018
   891
paulson@47018
   892
lemma Finite_succ: "Finite(x) ==> Finite(succ(x))"
paulson@47018
   893
apply (unfold succ_def)
paulson@47018
   894
apply (erule Finite_cons)
paulson@13221
   895
done
paulson@13221
   896
paulson@47018
   897
lemma lepoll_nat_imp_Finite:
paulson@47018
   898
  assumes A: "A \<lesssim> n" and n: "n \<in> nat" shows "Finite(A)"
paulson@47018
   899
proof -
paulson@47018
   900
  have "A \<lesssim> n \<Longrightarrow> Finite(A)" using n
paulson@47018
   901
    proof (induct n)
paulson@47018
   902
      case 0
paulson@47018
   903
      hence "A = 0" by (rule lepoll_0_is_0) 
paulson@47018
   904
      thus ?case by simp
paulson@47018
   905
    next
paulson@47018
   906
      case (succ n)
paulson@47018
   907
      hence "A \<lesssim> n \<or> A \<approx> succ(n)" by (blast dest: lepoll_succ_disj)
paulson@47018
   908
      thus ?case using succ by (auto simp add: Finite_def) 
paulson@47018
   909
    qed
paulson@47018
   910
  thus ?thesis using A .
paulson@47018
   911
qed
paulson@47018
   912
paulson@46820
   913
lemma lesspoll_nat_is_Finite:
paulson@13221
   914
     "A \<prec> nat ==> Finite(A)"
paulson@13221
   915
apply (unfold Finite_def)
paulson@46820
   916
apply (blast dest: ltD lesspoll_cardinal_lt
paulson@13221
   917
                   lesspoll_imp_eqpoll [THEN eqpoll_sym])
paulson@13221
   918
done
paulson@13221
   919
paulson@46820
   920
lemma lepoll_Finite:
paulson@46877
   921
  assumes Y: "Y \<lesssim> X" and X: "Finite(X)" shows "Finite(Y)"
paulson@46877
   922
proof -
paulson@46953
   923
  obtain n where n: "n \<in> nat" "X \<approx> n" using X
paulson@46953
   924
    by (auto simp add: Finite_def)
paulson@46877
   925
  have "Y \<lesssim> X"         by (rule Y)
paulson@46877
   926
  also have "... \<approx> n"  by (rule n)
paulson@46877
   927
  finally have "Y \<lesssim> n" .
paulson@46877
   928
  thus ?thesis using n by (simp add: lepoll_nat_imp_Finite)
paulson@46877
   929
qed
paulson@13221
   930
wenzelm@45602
   931
lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite]
paulson@13221
   932
paulson@46821
   933
lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) \<longleftrightarrow> Finite(x)"
paulson@13244
   934
by (blast intro: Finite_cons subset_Finite)
paulson@13244
   935
paulson@46821
   936
lemma Finite_succ_iff [iff]: "Finite(succ(x)) \<longleftrightarrow> Finite(x)"
paulson@13244
   937
by (simp add: succ_def)
paulson@13244
   938
paulson@47018
   939
lemma Finite_Int: "Finite(A) | Finite(B) ==> Finite(A \<inter> B)"
paulson@47018
   940
by (blast intro: subset_Finite)
paulson@47018
   941
paulson@47018
   942
lemmas Finite_Diff = Diff_subset [THEN subset_Finite]
paulson@47018
   943
paulson@46820
   944
lemma nat_le_infinite_Ord:
paulson@46820
   945
      "[| Ord(i);  ~ Finite(i) |] ==> nat \<le> i"
paulson@13221
   946
apply (unfold Finite_def)
paulson@13221
   947
apply (erule Ord_nat [THEN [2] Ord_linear2])
paulson@13221
   948
prefer 2 apply assumption
paulson@13221
   949
apply (blast intro!: eqpoll_refl elim!: ltE)
paulson@13221
   950
done
paulson@13221
   951
paulson@46820
   952
lemma Finite_imp_well_ord:
paulson@46820
   953
    "Finite(A) ==> \<exists>r. well_ord(A,r)"
paulson@13221
   954
apply (unfold Finite_def eqpoll_def)
paulson@13221
   955
apply (blast intro: well_ord_rvimage bij_is_inj well_ord_Memrel nat_into_Ord)
paulson@13221
   956
done
paulson@13221
   957
paulson@13244
   958
lemma succ_lepoll_imp_not_empty: "succ(x) \<lesssim> y ==> y \<noteq> 0"
paulson@13244
   959
by (fast dest!: lepoll_0_is_0)
paulson@13244
   960
paulson@13244
   961
lemma eqpoll_succ_imp_not_empty: "x \<approx> succ(n) ==> x \<noteq> 0"
paulson@13244
   962
by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0])
paulson@13244
   963
paulson@13244
   964
lemma Finite_Fin_lemma [rule_format]:
paulson@46820
   965
     "n \<in> nat ==> \<forall>A. (A\<approx>n & A \<subseteq> X) \<longrightarrow> A \<in> Fin(X)"
paulson@13244
   966
apply (induct_tac n)
paulson@13244
   967
apply (rule allI)
paulson@13244
   968
apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
paulson@13244
   969
apply (rule allI)
paulson@13244
   970
apply (rule impI)
paulson@13244
   971
apply (erule conjE)
paulson@13244
   972
apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption)
paulson@13244
   973
apply (frule Diff_sing_eqpoll, assumption)
paulson@13244
   974
apply (erule allE)
paulson@13244
   975
apply (erule impE, fast)
paulson@13244
   976
apply (drule subsetD, assumption)
paulson@13244
   977
apply (drule Fin.consI, assumption)
paulson@13244
   978
apply (simp add: cons_Diff)
paulson@13244
   979
done
paulson@13244
   980
paulson@13244
   981
lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)"
paulson@46820
   982
by (unfold Finite_def, blast intro: Finite_Fin_lemma)
paulson@13244
   983
paulson@46953
   984
lemma Fin_lemma [rule_format]: "n \<in> nat ==> \<forall>A. A \<approx> n \<longrightarrow> A \<in> Fin(A)"
paulson@13244
   985
apply (induct_tac n)
paulson@13244
   986
apply (simp add: eqpoll_0_iff, clarify)
paulson@46953
   987
apply (subgoal_tac "\<exists>u. u \<in> A")
paulson@13244
   988
apply (erule exE)
wenzelm@46471
   989
apply (rule Diff_sing_eqpoll [elim_format])
paulson@13244
   990
prefer 2 apply assumption
paulson@13244
   991
apply assumption
paulson@13784
   992
apply (rule_tac b = A in cons_Diff [THEN subst], assumption)
paulson@13244
   993
apply (rule Fin.consI, blast)
paulson@13244
   994
apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
paulson@13244
   995
(*Now for the lemma assumed above*)
paulson@13244
   996
apply (unfold eqpoll_def)
paulson@13244
   997
apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type])
paulson@13244
   998
done
paulson@13244
   999
paulson@46820
  1000
lemma Finite_into_Fin: "Finite(A) ==> A \<in> Fin(A)"
paulson@13244
  1001
apply (unfold Finite_def)
paulson@13244
  1002
apply (blast intro: Fin_lemma)
paulson@13244
  1003
done
paulson@13244
  1004
paulson@46820
  1005
lemma Fin_into_Finite: "A \<in> Fin(U) ==> Finite(A)"
paulson@13244
  1006
by (fast intro!: Finite_0 Finite_cons elim: Fin_induct)
paulson@13244
  1007
paulson@46821
  1008
lemma Finite_Fin_iff: "Finite(A) \<longleftrightarrow> A \<in> Fin(A)"
paulson@13244
  1009
by (blast intro: Finite_into_Fin Fin_into_Finite)
paulson@13244
  1010
paulson@46820
  1011
lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A \<union> B)"
paulson@46820
  1012
by (blast intro!: Fin_into_Finite Fin_UnI
paulson@13244
  1013
          dest!: Finite_into_Fin
paulson@46820
  1014
          intro: Un_upper1 [THEN Fin_mono, THEN subsetD]
paulson@13244
  1015
                 Un_upper2 [THEN Fin_mono, THEN subsetD])
paulson@13244
  1016
paulson@46821
  1017
lemma Finite_Un_iff [simp]: "Finite(A \<union> B) \<longleftrightarrow> (Finite(A) & Finite(B))"
paulson@46820
  1018
by (blast intro: subset_Finite Finite_Un)
paulson@14883
  1019
wenzelm@60770
  1020
text\<open>The converse must hold too.\<close>
paulson@46820
  1021
lemma Finite_Union: "[| \<forall>y\<in>X. Finite(y);  Finite(X) |] ==> Finite(\<Union>(X))"
paulson@13244
  1022
apply (simp add: Finite_Fin_iff)
paulson@13244
  1023
apply (rule Fin_UnionI)
paulson@13244
  1024
apply (erule Fin_induct, simp)
paulson@13244
  1025
apply (blast intro: Fin.consI Fin_mono [THEN [2] rev_subsetD])
paulson@13244
  1026
done
paulson@13244
  1027
paulson@13244
  1028
(* Induction principle for Finite(A), by Sidi Ehmety *)
wenzelm@13524
  1029
lemma Finite_induct [case_names 0 cons, induct set: Finite]:
paulson@13244
  1030
"[| Finite(A); P(0);
paulson@46820
  1031
    !! x B.   [| Finite(B); x \<notin> B; P(B) |] ==> P(cons(x, B)) |]
paulson@13244
  1032
 ==> P(A)"
paulson@46820
  1033
apply (erule Finite_into_Fin [THEN Fin_induct])
paulson@13244
  1034
apply (blast intro: Fin_into_Finite)+
paulson@13244
  1035
done
paulson@13244
  1036
paulson@13244
  1037
(*Sidi Ehmety.  The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *)
paulson@13244
  1038
lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)"
paulson@13244
  1039
apply (unfold Finite_def)
paulson@46877
  1040
apply (case_tac "a \<in> A")
paulson@13244
  1041
apply (subgoal_tac [2] "A-{a}=A", auto)
paulson@13244
  1042
apply (rule_tac x = "succ (n) " in bexI)
paulson@13244
  1043
apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ")
paulson@13784
  1044
apply (drule_tac a = a and b = n in cons_eqpoll_cong)
paulson@13244
  1045
apply (auto dest: mem_irrefl)
paulson@13244
  1046
done
paulson@13244
  1047
paulson@13244
  1048
(*Sidi Ehmety.  And the contrapositive of this says
paulson@13244
  1049
   [| ~Finite(A); Finite(B) |] ==> ~Finite(A-B) *)
paulson@46820
  1050
lemma Diff_Finite [rule_format]: "Finite(B) ==> Finite(A-B) \<longrightarrow> Finite(A)"
paulson@13244
  1051
apply (erule Finite_induct, auto)
paulson@46953
  1052
apply (case_tac "x \<in> A")
paulson@13244
  1053
 apply (subgoal_tac [2] "A-cons (x, B) = A - B")
paulson@13615
  1054
apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}", simp)
paulson@13244
  1055
apply (drule Diff_sing_Finite, auto)
paulson@13244
  1056
done
paulson@13244
  1057
paulson@13244
  1058
lemma Finite_RepFun: "Finite(A) ==> Finite(RepFun(A,f))"
paulson@13244
  1059
by (erule Finite_induct, simp_all)
paulson@13244
  1060
paulson@13244
  1061
lemma Finite_RepFun_iff_lemma [rule_format]:
paulson@46820
  1062
     "[|Finite(x); !!x y. f(x)=f(y) ==> x=y|]
paulson@46820
  1063
      ==> \<forall>A. x = RepFun(A,f) \<longrightarrow> Finite(A)"
paulson@13244
  1064
apply (erule Finite_induct)
paulson@46820
  1065
 apply clarify
paulson@13244
  1066
 apply (case_tac "A=0", simp)
paulson@46820
  1067
 apply (blast del: allE, clarify)
paulson@46820
  1068
apply (subgoal_tac "\<exists>z\<in>A. x = f(z)")
paulson@46820
  1069
 prefer 2 apply (blast del: allE elim: equalityE, clarify)
paulson@13244
  1070
apply (subgoal_tac "B = {f(u) . u \<in> A - {z}}")
paulson@46820
  1071
 apply (blast intro: Diff_sing_Finite)
wenzelm@59788
  1072
apply (thin_tac "\<forall>A. P(A) \<longrightarrow> Finite(A)" for P)
paulson@46820
  1073
apply (rule equalityI)
paulson@46820
  1074
 apply (blast intro: elim: equalityE)
paulson@46820
  1075
apply (blast intro: elim: equalityCE)
paulson@13244
  1076
done
paulson@13244
  1077
wenzelm@60770
  1078
text\<open>I don't know why, but if the premise is expressed using meta-connectives
wenzelm@60770
  1079
then  the simplifier cannot prove it automatically in conditional rewriting.\<close>
paulson@13244
  1080
lemma Finite_RepFun_iff:
paulson@46821
  1081
     "(\<forall>x y. f(x)=f(y) \<longrightarrow> x=y) ==> Finite(RepFun(A,f)) \<longleftrightarrow> Finite(A)"
paulson@46820
  1082
by (blast intro: Finite_RepFun Finite_RepFun_iff_lemma [of _ f])
paulson@13244
  1083
paulson@13244
  1084
lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))"
paulson@46820
  1085
apply (erule Finite_induct)
paulson@46820
  1086
apply (simp_all add: Pow_insert Finite_Un Finite_RepFun)
paulson@13244
  1087
done
paulson@13244
  1088
paulson@13244
  1089
lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ==> Finite(A)"
paulson@13244
  1090
apply (subgoal_tac "Finite({{x} . x \<in> A})")
paulson@46820
  1091
 apply (simp add: Finite_RepFun_iff )
paulson@46820
  1092
apply (blast intro: subset_Finite)
paulson@13244
  1093
done
paulson@13244
  1094
paulson@46821
  1095
lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) \<longleftrightarrow> Finite(A)"
paulson@13244
  1096
by (blast intro: Finite_Pow Finite_Pow_imp_Finite)
paulson@13244
  1097
paulson@47101
  1098
lemma Finite_cardinal_iff:
paulson@47101
  1099
  assumes i: "Ord(i)" shows "Finite(|i|) \<longleftrightarrow> Finite(i)"
paulson@47101
  1100
  by (auto simp add: Finite_def) (blast intro: eqpoll_trans eqpoll_sym Ord_cardinal_eqpoll [OF i])+
paulson@13244
  1101
paulson@13221
  1102
paulson@13221
  1103
(*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
paulson@13221
  1104
  set is well-ordered.  Proofs simplified by lcp. *)
paulson@13221
  1105
paulson@46877
  1106
lemma nat_wf_on_converse_Memrel: "n \<in> nat ==> wf[n](converse(Memrel(n)))"
paulson@47018
  1107
proof (induct n rule: nat_induct)
paulson@47018
  1108
  case 0 thus ?case by (blast intro: wf_onI)
paulson@47018
  1109
next
paulson@47018
  1110
  case (succ x)
paulson@47018
  1111
  hence wfx: "\<And>Z. Z = 0 \<or> (\<exists>z\<in>Z. \<forall>y. z \<in> y \<and> z \<in> x \<and> y \<in> x \<and> z \<in> x \<longrightarrow> y \<notin> Z)"
wenzelm@61798
  1112
    by (simp add: wf_on_def wf_def)  \<comment>\<open>not easy to erase the duplicate @{term"z \<in> x"}!\<close>
paulson@47018
  1113
  show ?case
paulson@47018
  1114
    proof (rule wf_onI)
paulson@47018
  1115
      fix Z u
paulson@47018
  1116
      assume Z: "u \<in> Z" "\<forall>z\<in>Z. \<exists>y\<in>Z. \<langle>y, z\<rangle> \<in> converse(Memrel(succ(x)))"
paulson@47018
  1117
      show False 
paulson@47018
  1118
        proof (cases "x \<in> Z")
paulson@47018
  1119
          case True thus False using Z
paulson@47018
  1120
            by (blast elim: mem_irrefl mem_asym)
paulson@47018
  1121
          next
paulson@47018
  1122
          case False thus False using wfx [of Z] Z
paulson@47018
  1123
            by blast
paulson@47018
  1124
        qed
paulson@47018
  1125
    qed
paulson@47018
  1126
qed
paulson@13221
  1127
paulson@46877
  1128
lemma nat_well_ord_converse_Memrel: "n \<in> nat ==> well_ord(n,converse(Memrel(n)))"
paulson@13221
  1129
apply (frule Ord_nat [THEN Ord_in_Ord, THEN well_ord_Memrel])
paulson@47018
  1130
apply (simp add: well_ord_def tot_ord_converse nat_wf_on_converse_Memrel) 
paulson@13221
  1131
done
paulson@13221
  1132
paulson@13221
  1133
lemma well_ord_converse:
paulson@46820
  1134
     "[|well_ord(A,r);
paulson@13221
  1135
        well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r)))) |]
paulson@13221
  1136
      ==> well_ord(A,converse(r))"
paulson@13221
  1137
apply (rule well_ord_Int_iff [THEN iffD1])
paulson@13221
  1138
apply (frule ordermap_bij [THEN bij_is_inj, THEN well_ord_rvimage], assumption)
paulson@13221
  1139
apply (simp add: rvimage_converse converse_Int converse_prod
paulson@13221
  1140
                 ordertype_ord_iso [THEN ord_iso_rvimage_eq])
paulson@13221
  1141
done
paulson@13221
  1142
paulson@13221
  1143
lemma ordertype_eq_n:
paulson@46953
  1144
  assumes r: "well_ord(A,r)" and A: "A \<approx> n" and n: "n \<in> nat"
paulson@46877
  1145
  shows "ordertype(A,r) = n"
paulson@46877
  1146
proof -
paulson@46953
  1147
  have "ordertype(A,r) \<approx> A"
paulson@46953
  1148
    by (blast intro: bij_imp_eqpoll bij_converse_bij ordermap_bij r)
paulson@46877
  1149
  also have "... \<approx> n" by (rule A)
paulson@46877
  1150
  finally have "ordertype(A,r) \<approx> n" .
paulson@46877
  1151
  thus ?thesis
paulson@46953
  1152
    by (simp add: Ord_nat_eqpoll_iff Ord_ordertype n r)
paulson@46877
  1153
qed
paulson@13221
  1154
paulson@46820
  1155
lemma Finite_well_ord_converse:
paulson@13221
  1156
    "[| Finite(A);  well_ord(A,r) |] ==> well_ord(A,converse(r))"
paulson@13221
  1157
apply (unfold Finite_def)
paulson@13221
  1158
apply (rule well_ord_converse, assumption)
paulson@13221
  1159
apply (blast dest: ordertype_eq_n intro!: nat_well_ord_converse_Memrel)
paulson@13221
  1160
done
paulson@13221
  1161
paulson@46877
  1162
lemma nat_into_Finite: "n \<in> nat ==> Finite(n)"
paulson@47018
  1163
  by (auto simp add: Finite_def intro: eqpoll_refl) 
paulson@13221
  1164
paulson@46877
  1165
lemma nat_not_Finite: "~ Finite(nat)"
paulson@46877
  1166
proof -
paulson@46877
  1167
  { fix n
paulson@46877
  1168
    assume n: "n \<in> nat" "nat \<approx> n"
paulson@46953
  1169
    have "n \<in> nat"    by (rule n)
paulson@46877
  1170
    also have "... = n" using n
paulson@46953
  1171
      by (simp add: Ord_nat_eqpoll_iff Ord_nat)
paulson@46877
  1172
    finally have "n \<in> n" .
paulson@46953
  1173
    hence False
paulson@46953
  1174
      by (blast elim: mem_irrefl)
paulson@46877
  1175
  }
paulson@46877
  1176
  thus ?thesis
paulson@46953
  1177
    by (auto simp add: Finite_def)
paulson@46877
  1178
qed
paulson@14076
  1179
lcp@435
  1180
end