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