Library/card.ml

   1 (* ========================================================================= *)
   2 (* Basic notions of cardinal arithmetic.                                     *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/wo.ml";;
   6
   7 let TRANS_CHAIN_TAC th =
   8   MAP_EVERY (fun t -> TRANS_TAC th t THEN ASM_REWRITE_TAC[]);;
   9
  10 (* ------------------------------------------------------------------------- *)
  11 (* We need these a few times, so give them names.                            *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 let sum_DISTINCT = distinctness "sum";;
  15
  16 let sum_INJECTIVE = injectivity "sum";;
  17
  18 let sum_CASES = prove_cases_thm sum_INDUCT;;
  19
  20 let FORALL_SUM_THM = prove
  21  (`(!z. P z) <=> (!x. P(INL x)) /\ (!x. P(INR x))`,
  22   MESON_TAC[sum_CASES]);;
  23
  24 let EXISTS_SUM_THM = prove
  25  (`(?z. P z) <=> (?x. P(INL x)) \/ (?x. P(INR x))`,
  26   MESON_TAC[sum_CASES]);;
  27
  28 (* ------------------------------------------------------------------------- *)
  29 (* Special case of Zorn's Lemma for restriction of subset lattice.           *)
  30 (* ------------------------------------------------------------------------- *)
  31
  32 let POSET_RESTRICTED_SUBSET = prove
  33  (`!P. poset(\(x,y). P(x) /\ P(y) /\ x SUBSET y)`,
  34   GEN_TAC THEN REWRITE_TAC[poset; fl] THEN
  35   CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
  36   REWRITE_TAC[SUBSET; EXTENSION] THEN MESON_TAC[]);;
  37
  38 let FL_RESTRICTED_SUBSET = prove
  39  (`!P. fl(\(x,y). P(x) /\ P(y) /\ x SUBSET y) = P`,
  40   REWRITE_TAC[fl; FORALL_PAIR_THM; FUN_EQ_THM] THEN
  41   CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN MESON_TAC[SUBSET_REFL]);;
  42
  43 let ZL_SUBSETS = prove
  44  (`!P. (!c. (!x. x IN c ==> P x) /\
  45             (!x y. x IN c /\ y IN c ==> x SUBSET y \/ y SUBSET x)
  46             ==> ?z. P z /\ (!x. x IN c ==> x SUBSET z))
  47        ==> ?a:A->bool. P a /\ (!x. P x /\ a SUBSET x ==> (a = x))`,
  48   GEN_TAC THEN
  49   MP_TAC(ISPEC `\(x,y). P(x:A->bool) /\ P(y) /\ x SUBSET y` ZL) THEN
  50   REWRITE_TAC[POSET_RESTRICTED_SUBSET; FL_RESTRICTED_SUBSET] THEN
  51   REWRITE_TAC[chain] THEN
  52   CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
  53   REWRITE_TAC[IN] THEN MATCH_MP_TAC MONO_IMP THEN CONJ_TAC THENL
  54    [MATCH_MP_TAC MONO_FORALL; ALL_TAC] THEN
  55   MESON_TAC[]);;
  56
  57 let ZL_SUBSETS_UNIONS = prove
  58  (`!P. (!c. (!x. x IN c ==> P x) /\
  59             (!x y. x IN c /\ y IN c ==> x SUBSET y \/ y SUBSET x)
  60             ==> P(UNIONS c))
  61        ==> ?a:A->bool. P a /\ (!x. P x /\ a SUBSET x ==> (a = x))`,
  62   REPEAT STRIP_TAC THEN MATCH_MP_TAC ZL_SUBSETS THEN
  63   REPEAT STRIP_TAC THEN EXISTS_TAC `UNIONS(c:(A->bool)->bool)` THEN
  64   ASM_MESON_TAC[SUBSET; IN_UNIONS]);;
  65
  66 let ZL_SUBSETS_UNIONS_NONEMPTY = prove
  67  (`!P. (?x. P x) /\
  68        (!c. (?x. x IN c) /\
  69             (!x. x IN c ==> P x) /\
  70             (!x y. x IN c /\ y IN c ==> x SUBSET y \/ y SUBSET x)
  71             ==> P(UNIONS c))
  72        ==> ?a:A->bool. P a /\ (!x. P x /\ a SUBSET x ==> (a = x))`,
  73   REPEAT STRIP_TAC THEN MATCH_MP_TAC ZL_SUBSETS THEN
  74   REPEAT STRIP_TAC THEN ASM_CASES_TAC `?x:A->bool. x IN c` THENL
  75    [EXISTS_TAC `UNIONS(c:(A->bool)->bool)` THEN
  76     ASM_SIMP_TAC[] THEN MESON_TAC[SUBSET; IN_UNIONS];
  77     ASM_MESON_TAC[]]);;
  78
  79 (* ------------------------------------------------------------------------- *)
  80 (* Useful lemma to reduce some higher order stuff to first order.            *)
  81 (* ------------------------------------------------------------------------- *)
  82
  83 let FLATTEN_LEMMA = prove
  84  (`(!x. x IN s ==> (g(f(x)) = x)) <=> !y x. x IN s /\ (y = f x) ==> (g y = x)`,
  85   MESON_TAC[]);;
  86
  87 (* ------------------------------------------------------------------------- *)
  88 (* Knaster-Tarski fixpoint theorem (used in Schroeder-Bernstein below).      *)
  89 (* ------------------------------------------------------------------------- *)
  90
  91 let TARSKI_SET = prove
  92  (`!f. (!s t. s SUBSET t ==> f(s) SUBSET f(t)) ==> ?s:A->bool. f(s) = s`,
  93   REPEAT STRIP_TAC THEN MAP_EVERY ABBREV_TAC
  94    [`Y = {b:A->bool | f(b) SUBSET b}`; `a:A->bool = INTERS Y`] THEN
  95   SUBGOAL_THEN `!b:A->bool. b IN Y <=> f(b) SUBSET b` ASSUME_TAC THENL
  96    [EXPAND_TAC "Y" THEN REWRITE_TAC[IN_ELIM_THM]; ALL_TAC] THEN
  97   SUBGOAL_THEN `!b:A->bool. b IN Y ==> f(a:A->bool) SUBSET b` ASSUME_TAC THENL
  98    [ASM_MESON_TAC[SUBSET_TRANS; IN_INTERS; SUBSET]; ALL_TAC] THEN
  99   SUBGOAL_THEN `f(a:A->bool) SUBSET a`
 100    (fun th -> ASM_MESON_TAC[SUBSET_ANTISYM; IN_INTERS; th]) THEN
 101   ASM_MESON_TAC[IN_INTERS; SUBSET]);;
 102
 103 (* ------------------------------------------------------------------------- *)
 104 (* We need a nonemptiness hypothesis for the nicest total function form.     *)
 105 (* ------------------------------------------------------------------------- *)
 106
 107 let INJECTIVE_LEFT_INVERSE_NONEMPTY = prove
 108  (`(?x. x IN s)
 109    ==> ((!x y. x IN s /\ y IN s /\ (f(x) = f(y)) ==> (x = y)) <=>
 110         ?g. (!y. y IN t ==> g(y) IN s) /\
 111             (!x. x IN s ==> (g(f(x)) = x)))`,
 112   REWRITE_TAC[FLATTEN_LEMMA; GSYM SKOLEM_THM; AND_FORALL_THM] THEN
 113   MESON_TAC[]);;
 114
 115 (* ------------------------------------------------------------------------- *)
 116 (* Now bijectivity.                                                          *)
 117 (* ------------------------------------------------------------------------- *)
 118
 119 let BIJECTIVE_INJECTIVE_SURJECTIVE = prove
 120  (`(!x. x IN s ==> f(x) IN t) /\
 121    (!y. y IN t ==> ?!x. x IN s /\ (f x = y)) <=>
 122    (!x. x IN s ==> f(x) IN t) /\
 123    (!x y. x IN s /\ y IN s /\ (f(x) = f(y)) ==> (x = y)) /\
 124    (!y. y IN t ==> ?x. x IN s /\ (f x = y))`,
 125   MESON_TAC[]);;
 126
 127 let BIJECTIVE_INVERSES = prove
 128  (`(!x. x IN s ==> f(x) IN t) /\
 129    (!y. y IN t ==> ?!x. x IN s /\ (f x = y)) <=>
 130    (!x. x IN s ==> f(x) IN t) /\
 131    ?g. (!y. y IN t ==> g(y) IN s) /\
 132        (!y. y IN t ==> (f(g(y)) = y)) /\
 133        (!x. x IN s ==> (g(f(x)) = x))`,
 134   REWRITE_TAC[BIJECTIVE_INJECTIVE_SURJECTIVE;
 135               INJECTIVE_ON_LEFT_INVERSE;
 136               SURJECTIVE_ON_RIGHT_INVERSE] THEN
 137   MATCH_MP_TAC(TAUT `(a ==> (b <=> c)) ==> (a /\ b <=> a /\ c)`) THEN
 138   DISCH_TAC THEN REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN
 139   AP_TERM_TAC THEN ABS_TAC THEN EQ_TAC THEN ASM_MESON_TAC[]);;
 140
 141 (* ------------------------------------------------------------------------- *)
 142 (* Other variants of cardinal equality.                                      *)
 143 (* ------------------------------------------------------------------------- *)
 144
 145 let EQ_C_BIJECTIONS = prove
 146  (`!s:A->bool t:B->bool.
 147         s =_c t <=> ?f g. (!x. x IN s ==> f x IN t /\ g(f x) = x) /\
 148                           (!y. y IN t ==> g y IN s /\ f(g y) = y)`,
 149   REPEAT GEN_TAC THEN REWRITE_TAC[eq_c] THEN
 150   AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
 151   X_GEN_TAC `f:A->B` THEN REWRITE_TAC[] THEN
 152   EQ_TAC THENL [STRIP_TAC; MESON_TAC[]] THEN
 153   EXISTS_TAC `(\y. @x. x IN s /\ f x = y):B->A` THEN
 154   ASM_MESON_TAC[]);;
 155
 156 let EQ_C = prove
 157  (`s =_c t <=>
 158    ?R:A#B->bool. (!x y. R(x,y) ==> x IN s /\ y IN t) /\
 159                  (!x. x IN s ==> ?!y. y IN t /\ R(x,y)) /\
 160                  (!y. y IN t ==> ?!x. x IN s /\ R(x,y))`,
 161   REWRITE_TAC[eq_c] THEN EQ_TAC THENL
 162    [DISCH_THEN(X_CHOOSE_THEN `f:A->B` STRIP_ASSUME_TAC) THEN
 163     EXISTS_TAC `\(x:A,y:B). x IN s /\ y IN t /\ (y = f x)` THEN
 164     CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN ASM_MESON_TAC[];
 165     DISCH_THEN(CHOOSE_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 166     DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 167     GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV)
 168      [EXISTS_UNIQUE_ALT; RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN
 169     MATCH_MP_TAC MONO_EXISTS THEN ASM_MESON_TAC[]]);;
 170
 171 (* ------------------------------------------------------------------------- *)
 172 (* The "easy" ordering properties.                                           *)
 173 (* ------------------------------------------------------------------------- *)
 174
 175 let CARD_LE_REFL = prove
 176  (`!s:A->bool. s <=_c s`,
 177   GEN_TAC THEN REWRITE_TAC[le_c] THEN EXISTS_TAC `\x:A. x` THEN SIMP_TAC[]);;
 178
 179 let CARD_LE_TRANS = prove
 180  (`!s:A->bool t:B->bool u:C->bool.
 181        s <=_c t /\ t <=_c u ==> s <=_c u`,
 182   REPEAT GEN_TAC THEN REWRITE_TAC[le_c] THEN
 183   DISCH_THEN(CONJUNCTS_THEN2
 184    (X_CHOOSE_TAC `f:A->B`) (X_CHOOSE_TAC `g:B->C`)) THEN
 185   EXISTS_TAC `(g:B->C) o (f:A->B)` THEN REWRITE_TAC[o_THM] THEN
 186   ASM_MESON_TAC[]);;
 187
 188 let CARD_LT_REFL = prove
 189  (`!s:A->bool. ~(s <_c s)`,
 190   MESON_TAC[lt_c; CARD_LE_REFL]);;
 191
 192 let CARD_LET_TRANS = prove
 193  (`!s:A->bool t:B->bool u:C->bool.
 194        s <=_c t /\ t <_c u ==> s <_c u`,
 195   REPEAT GEN_TAC THEN REWRITE_TAC[lt_c] THEN
 196   MATCH_MP_TAC(TAUT `(a /\ b ==> c) /\ (c' /\ a ==> b')
 197                      ==> a /\ b /\ ~b' ==> c /\ ~c'`) THEN
 198   REWRITE_TAC[CARD_LE_TRANS]);;
 199
 200 let CARD_LTE_TRANS = prove
 201  (`!s:A->bool t:B->bool u:C->bool.
 202        s <_c t /\ t <=_c u ==> s <_c u`,
 203   REPEAT GEN_TAC THEN REWRITE_TAC[lt_c] THEN
 204   MATCH_MP_TAC(TAUT `(a /\ b ==> c) /\ (b /\ c' ==> a')
 205                      ==> (a /\ ~a') /\ b ==> c /\ ~c'`) THEN
 206   REWRITE_TAC[CARD_LE_TRANS]);;
 207
 208 let CARD_LT_TRANS = prove
 209  (`!s:A->bool t:B->bool u:C->bool.
 210        s <_c t /\ t <_c u ==> s <_c u`,
 211   MESON_TAC[lt_c; CARD_LTE_TRANS]);;
 212
 213 let CARD_EQ_REFL = prove
 214  (`!s:A->bool. s =_c s`,
 215   GEN_TAC THEN REWRITE_TAC[eq_c] THEN EXISTS_TAC `\x:A. x` THEN
 216   SIMP_TAC[] THEN MESON_TAC[]);;
 217
 218 let CARD_EQ_SYM = prove
 219  (`!s t. s =_c t <=> t =_c s`,
 220   REPEAT GEN_TAC THEN REWRITE_TAC[eq_c; BIJECTIVE_INVERSES] THEN
 221   REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN
 222   GEN_REWRITE_TAC RAND_CONV [SWAP_EXISTS_THM] THEN
 223   REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN REWRITE_TAC[CONJ_ACI]);;
 224
 225 let CARD_EQ_IMP_LE = prove
 226  (`!s t. s =_c t ==> s <=_c t`,
 227   REWRITE_TAC[le_c; eq_c] THEN MESON_TAC[]);;
 228
 229 let CARD_LT_IMP_LE = prove
 230  (`!s t. s <_c t ==> s <=_c t`,
 231   SIMP_TAC[lt_c]);;
 232
 233 let CARD_LE_RELATIONAL = prove
 234  (`!R:A->B->bool.
 235         (!x y y'. x IN s /\ R x y /\ R x y' ==> y = y')
 236         ==> {y | ?x. x IN s /\ R x y} <=_c s`,
 237   REPEAT STRIP_TAC THEN REWRITE_TAC[le_c] THEN
 238   EXISTS_TAC `\y:B. @x:A. x IN s /\ R x y` THEN
 239   REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[]);;
 240
 241 let CARD_LE_RELATIONAL_FULL = prove
 242  (`!R:A->B->bool s t.
 243         (!y. y IN t ==> ?x. x IN s /\ R x y) /\
 244         (!x y y'. x IN s /\ y IN t /\ y' IN t /\ R x y /\ R x y' ==> y = y')
 245         ==> t <=_c s`,
 246   REPEAT STRIP_TAC THEN REWRITE_TAC[le_c] THEN
 247   EXISTS_TAC `\y:B. @x:A. x IN s /\ R x y` THEN
 248   REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[]);;
 249
 250 (* ------------------------------------------------------------------------- *)
 251 (* Two trivial lemmas.                                                       *)
 252 (* ------------------------------------------------------------------------- *)
 253
 254 let CARD_LE_EMPTY = prove
 255  (`!s. s <=_c {} <=> s = {}`,
 256   REWRITE_TAC[le_c; EXTENSION; NOT_IN_EMPTY] THEN MESON_TAC[]);;
 257
 258 let CARD_EQ_EMPTY = prove
 259  (`!s. s =_c {} <=> s = {}`,
 260   REWRITE_TAC[eq_c; EXTENSION; NOT_IN_EMPTY] THEN MESON_TAC[]);;
 261
 262 (* ------------------------------------------------------------------------- *)
 263 (* Antisymmetry (the Schroeder-Bernstein theorem).                           *)
 264 (* ------------------------------------------------------------------------- *)
 265
 266 let CARD_LE_ANTISYM = prove
 267  (`!s:A->bool t:B->bool. s <=_c t /\ t <=_c s <=> (s =_c t)`,
 268   REPEAT GEN_TAC THEN EQ_TAC THENL
 269    [ALL_TAC;
 270     SIMP_TAC[CARD_EQ_IMP_LE] THEN ONCE_REWRITE_TAC[CARD_EQ_SYM] THEN
 271     SIMP_TAC[CARD_EQ_IMP_LE]] THEN
 272   ASM_CASES_TAC `s:A->bool = {}` THEN ASM_CASES_TAC `t:B->bool = {}` THEN
 273   ASM_SIMP_TAC[CARD_LE_EMPTY; CARD_EQ_EMPTY] THEN
 274   RULE_ASSUM_TAC(REWRITE_RULE[EXTENSION; NOT_IN_EMPTY; NOT_FORALL_THM]) THEN
 275   ASM_SIMP_TAC[le_c; eq_c; INJECTIVE_LEFT_INVERSE_NONEMPTY] THEN
 276   DISCH_THEN(CONJUNCTS_THEN2
 277    (X_CHOOSE_THEN `i:A->B`
 278      (CONJUNCTS_THEN2 ASSUME_TAC (X_CHOOSE_THEN `i':B->A` STRIP_ASSUME_TAC)))
 279    (X_CHOOSE_THEN `j:B->A`
 280      (CONJUNCTS_THEN2 ASSUME_TAC
 281        (X_CHOOSE_THEN `j':A->B` STRIP_ASSUME_TAC)))) THEN
 282   MP_TAC(ISPEC
 283     `\a. s DIFF (IMAGE (j:B->A) (t DIFF (IMAGE (i:A->B) a)))`
 284     TARSKI_SET) THEN
 285   REWRITE_TAC[] THEN ANTS_TAC THENL
 286    [REWRITE_TAC[SUBSET; IN_DIFF; IN_IMAGE] THEN MESON_TAC[];
 287     ALL_TAC] THEN
 288   DISCH_THEN(X_CHOOSE_THEN `a:A->bool` ASSUME_TAC) THEN
 289   REWRITE_TAC[BIJECTIVE_INVERSES] THEN REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN
 290   EXISTS_TAC `\x. if x IN a then (i:A->B)(x) else j'(x)` THEN
 291   EXISTS_TAC `\y. if y IN (IMAGE (i:A->B) a) then i'(y) else (j:B->A)(y)` THEN
 292   REWRITE_TAC[FUN_EQ_THM; o_THM; I_DEF] THEN
 293   ONCE_REWRITE_TAC[TAUT `a /\ b /\ c /\ d <=> (a /\ d) /\ (b /\ c)`] THEN
 294   REWRITE_TAC[AND_FORALL_THM] THEN
 295   REWRITE_TAC[TAUT `(a ==> b) /\ (a ==> c) <=> a ==> b /\ c`] THEN
 296   CONJ_TAC THENL
 297    [X_GEN_TAC `x:A` THEN ASM_CASES_TAC `x:A IN a`;
 298     X_GEN_TAC `y:B` THEN ASM_CASES_TAC `y IN IMAGE (i:A->B) a`] THEN
 299   ASM_REWRITE_TAC[] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 300   RULE_ASSUM_TAC(REWRITE_RULE[EXTENSION; IN_UNIV; IN_DIFF; IN_IMAGE]) THEN
 301   TRY(FIRST_X_ASSUM(X_CHOOSE_THEN `x:A` STRIP_ASSUME_TAC)) THEN
 302   TRY(FIRST_X_ASSUM(fun th -> MP_TAC(SPEC `x:A` th) THEN
 303       ASM_REWRITE_TAC[] THEN ASSUME_TAC th)) THEN
 304   ASM_MESON_TAC[]);;
 305
 306 (* ------------------------------------------------------------------------- *)
 307 (* Totality (cardinal comparability).                                        *)
 308 (* ------------------------------------------------------------------------- *)
 309
 310 let CARD_LE_TOTAL = prove
 311  (`!s:A->bool t:B->bool. s <=_c t \/ t <=_c s`,
 312   REPEAT GEN_TAC THEN
 313   ABBREV_TAC
 314    `P = \R. (!x:A y:B. R(x,y) ==> x IN s /\ y IN t) /\
 315             (!x y y'. R(x,y) /\ R(x,y') ==> (y = y')) /\
 316             (!x x' y. R(x,y) /\ R(x',y) ==> (x = x'))` THEN
 317   MP_TAC(ISPEC `P:((A#B)->bool)->bool` ZL_SUBSETS_UNIONS) THEN ANTS_TAC THENL
 318    [GEN_TAC THEN EXPAND_TAC "P" THEN
 319     REWRITE_TAC[UNIONS; IN_ELIM_THM] THEN
 320     REWRITE_TAC[SUBSET; IN] THEN MESON_TAC[];
 321     ALL_TAC] THEN
 322   FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[] THEN
 323   DISCH_THEN(X_CHOOSE_THEN `R:A#B->bool` STRIP_ASSUME_TAC) THEN
 324   ASM_CASES_TAC `(!x:A. x IN s ==> ?y:B. y IN t /\ R(x,y)) \/
 325                  (!y:B. y IN t ==> ?x:A. x IN s /\ R(x,y))`
 326   THENL
 327    [FIRST_X_ASSUM(K ALL_TAC o SPEC `\(x:A,y:B). T`) THEN
 328     FIRST_X_ASSUM(DISJ_CASES_THEN MP_TAC) THEN
 329     REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM; le_c] THEN ASM_MESON_TAC[];
 330     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [DE_MORGAN_THM]) THEN
 331     REWRITE_TAC[NOT_FORALL_THM; NOT_IMP] THEN
 332     DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `a:A`) (X_CHOOSE_TAC `b:B`)) THEN
 333     FIRST_X_ASSUM(MP_TAC o SPEC
 334       `\(x:A,y:B). (x = a) /\ (y = b) \/ R(x,y)`) THEN
 335     REWRITE_TAC[SUBSET; FORALL_PAIR_THM; IN; EXTENSION] THEN
 336     CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
 337     RULE_ASSUM_TAC(REWRITE_RULE[IN]) THEN ASM_MESON_TAC[]]);;
 338
 339 (* ------------------------------------------------------------------------- *)
 340 (* Other variants like "trichotomy of cardinals" now follow easily.          *)
 341 (* ------------------------------------------------------------------------- *)
 342
 343 let CARD_LET_TOTAL = prove
 344  (`!s:A->bool t:B->bool. s <=_c t \/ t <_c s`,
 345   REWRITE_TAC[lt_c] THEN MESON_TAC[CARD_LE_TOTAL]);;
 346
 347 let CARD_LTE_TOTAL = prove
 348  (`!s:A->bool t:B->bool. s <_c t \/ t <=_c s`,
 349   REWRITE_TAC[lt_c] THEN MESON_TAC[CARD_LE_TOTAL]);;
 350
 351 let CARD_LT_TOTAL = prove
 352  (`!s:A->bool t:B->bool. s =_c t \/ s <_c t \/ t <_c s`,
 353   REWRITE_TAC[lt_c; GSYM CARD_LE_ANTISYM] THEN MESON_TAC[CARD_LE_TOTAL]);;
 354
 355 let CARD_NOT_LE = prove
 356  (`!s:A->bool t:B->bool. ~(s <=_c t) <=> t <_c s`,
 357   REWRITE_TAC[lt_c] THEN MESON_TAC[CARD_LE_TOTAL]);;
 358
 359 let CARD_NOT_LT = prove
 360  (`!s:A->bool t:B->bool. ~(s <_c t) <=> t <=_c s`,
 361   REWRITE_TAC[lt_c] THEN MESON_TAC[CARD_LE_TOTAL]);;
 362
 363 let CARD_LT_LE = prove
 364  (`!s t. s <_c t <=> s <=_c t /\ ~(s =_c t)`,
 365   REWRITE_TAC[lt_c; GSYM CARD_LE_ANTISYM] THEN CONV_TAC TAUT);;
 366
 367 let CARD_LE_LT = prove
 368  (`!s t. s <=_c t <=> s <_c t \/ s =_c t`,
 369   REPEAT GEN_TAC THEN REWRITE_TAC[GSYM CARD_NOT_LT] THEN
 370   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [CARD_LT_LE] THEN
 371   REWRITE_TAC[DE_MORGAN_THM; CARD_NOT_LE; CARD_EQ_SYM]);;
 372
 373 let CARD_LE_CONG = prove
 374  (`!s:A->bool s':B->bool t:C->bool t':D->bool.
 375       s =_c s' /\ t =_c t' ==> (s <=_c t <=> s' <=_c t')`,
 376   REPEAT GEN_TAC THEN REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN
 377   MATCH_MP_TAC(TAUT
 378    `!x y. (b /\ e ==> x) /\ (x /\ c ==> f) /\ (a /\ f ==> y) /\ (y /\ d ==> e)
 379           ==> (a /\ b) /\ (c /\ d) ==> (e <=> f)`) THEN
 380   MAP_EVERY EXISTS_TAC
 381    [`(s':B->bool) <=_c (t:C->bool)`;
 382     `(s:A->bool) <=_c (t':D->bool)`] THEN
 383   REWRITE_TAC[CARD_LE_TRANS]);;
 384
 385 let CARD_LT_CONG = prove
 386  (`!s:A->bool s':B->bool t:C->bool t':D->bool.
 387       s =_c s' /\ t =_c t' ==> (s <_c t <=> s' <_c t')`,
 388   REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM CARD_NOT_LE] THEN
 389   AP_TERM_TAC THEN MATCH_MP_TAC CARD_LE_CONG THEN
 390   ASM_REWRITE_TAC[]);;
 391
 392 let CARD_EQ_TRANS = prove
 393  (`!s:A->bool t:B->bool u:C->bool.
 394        s =_c t /\ t =_c u ==> s =_c u`,
 395   REPEAT GEN_TAC THEN REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN
 396   REPEAT STRIP_TAC THEN ASM_MESON_TAC[CARD_LE_TRANS]);;
 397
 398 let CARD_EQ_CONG = prove
 399  (`!s:A->bool s':B->bool t:C->bool t':D->bool.
 400       s =_c s' /\ t =_c t' ==> (s =_c t <=> s' =_c t')`,
 401   REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THENL
 402    [TRANS_CHAIN_TAC CARD_EQ_TRANS [`t:C->bool`; `s:A->bool`];
 403     TRANS_CHAIN_TAC CARD_EQ_TRANS [`s':B->bool`; `t':D->bool`]] THEN
 404   ASM_MESON_TAC[CARD_EQ_SYM]);;
 405
 406 (* ------------------------------------------------------------------------- *)
 407 (* Finiteness and infiniteness in terms of cardinality of N.                 *)
 408 (* ------------------------------------------------------------------------- *)
 409
 410 let INFINITE_CARD_LE = prove
 411  (`!s:A->bool. INFINITE s <=> (UNIV:num->bool) <=_c s`,
 412   REPEAT STRIP_TAC THEN EQ_TAC THENL
 413    [ALL_TAC;
 414     ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 415     REWRITE_TAC[INFINITE; le_c; IN_UNIV] THEN REPEAT STRIP_TAC THEN
 416     FIRST_ASSUM(MP_TAC o MATCH_MP INFINITE_IMAGE_INJ) THEN
 417     DISCH_THEN(MP_TAC o C MATCH_MP num_INFINITE) THEN
 418     REWRITE_TAC[INFINITE] THEN
 419     MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `s:A->bool` THEN
 420     ASM_SIMP_TAC[SUBSET; IN_IMAGE; IN_UNIV; LEFT_IMP_EXISTS_THM]] THEN
 421   DISCH_TAC THEN
 422   SUBGOAL_THEN `?f:num->A. !n. f(n) = @x. x IN (s DIFF IMAGE f {m | m < n})`
 423   MP_TAC THENL
 424    [MATCH_MP_TAC(MATCH_MP WF_REC WF_num) THEN
 425     REWRITE_TAC[IN_IMAGE; IN_ELIM_THM; IN_DIFF] THEN REPEAT STRIP_TAC THEN
 426     AP_TERM_TAC THEN ABS_TAC THEN ASM_MESON_TAC[];
 427     ALL_TAC] THEN
 428   REWRITE_TAC[le_c] THEN MATCH_MP_TAC MONO_EXISTS THEN
 429   X_GEN_TAC `f:num->A` THEN REWRITE_TAC[IN_UNIV] THEN DISCH_TAC THEN
 430   SUBGOAL_THEN `!n. (f:num->A)(n) IN (s DIFF IMAGE f {m | m < n})` MP_TAC THENL
 431    [GEN_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN CONV_TAC SELECT_CONV THEN
 432     REWRITE_TAC[MEMBER_NOT_EMPTY] THEN
 433     MATCH_MP_TAC INFINITE_NONEMPTY THEN MATCH_MP_TAC INFINITE_DIFF_FINITE THEN
 434     ASM_SIMP_TAC[FINITE_IMAGE; FINITE_NUMSEG_LT];
 435     ALL_TAC] THEN
 436   REWRITE_TAC[IN_IMAGE; IN_ELIM_THM; IN_DIFF] THEN MESON_TAC[LT_CASES]);;
 437
 438 let FINITE_CARD_LT = prove
 439  (`!s:A->bool. FINITE s <=> s <_c (UNIV:num->bool)`,
 440   ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN
 441   REWRITE_TAC[GSYM INFINITE; CARD_NOT_LT; INFINITE_CARD_LE]);;
 442
 443 let CARD_LE_SUBSET = prove
 444  (`!s:A->bool t. s SUBSET t ==> s <=_c t`,
 445   REWRITE_TAC[SUBSET; le_c] THEN MESON_TAC[I_THM]);;
 446
 447 let CARD_LE_UNIV = prove
 448  (`!s:A->bool. s <=_c (:A)`,
 449   GEN_TAC THEN MATCH_MP_TAC CARD_LE_SUBSET THEN REWRITE_TAC[SUBSET_UNIV]);;
 450
 451 let CARD_LE_EQ_SUBSET = prove
 452  (`!s:A->bool t:B->bool. s <=_c t <=> ?u. u SUBSET t /\ (s =_c u)`,
 453   REPEAT GEN_TAC THEN EQ_TAC THENL
 454    [ALL_TAC;
 455     REPEAT STRIP_TAC THEN
 456     FIRST_ASSUM(MP_TAC o MATCH_MP CARD_LE_SUBSET) THEN
 457     MATCH_MP_TAC(TAUT `(a <=> b) ==> b ==> a`) THEN
 458     MATCH_MP_TAC CARD_LE_CONG THEN
 459     ASM_REWRITE_TAC[CARD_LE_CONG; CARD_EQ_REFL]] THEN
 460   REWRITE_TAC[le_c; eq_c] THEN
 461   DISCH_THEN(X_CHOOSE_THEN `f:A->B` STRIP_ASSUME_TAC) THEN
 462   REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN EXISTS_TAC `IMAGE (f:A->B) s` THEN
 463   EXISTS_TAC `f:A->B` THEN REWRITE_TAC[IN_IMAGE; SUBSET] THEN
 464   ASM_MESON_TAC[]);;
 465
 466 let CARD_INFINITE_CONG = prove
 467  (`!s:A->bool t:B->bool. s =_c t ==> (INFINITE s <=> INFINITE t)`,
 468   REWRITE_TAC[INFINITE_CARD_LE] THEN REPEAT STRIP_TAC THEN
 469   MATCH_MP_TAC CARD_LE_CONG THEN ASM_REWRITE_TAC[CARD_EQ_REFL]);;
 470
 471 let CARD_FINITE_CONG = prove
 472  (`!s:A->bool t:B->bool. s =_c t ==> (FINITE s <=> FINITE t)`,
 473   ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN
 474   REWRITE_TAC[GSYM INFINITE; CARD_INFINITE_CONG]);;
 475
 476 let CARD_LE_FINITE = prove
 477  (`!s:A->bool t:B->bool. FINITE t /\ s <=_c t ==> FINITE s`,
 478   ASM_MESON_TAC[CARD_LE_EQ_SUBSET; FINITE_SUBSET; CARD_FINITE_CONG]);;
 479
 480 let CARD_EQ_FINITE = prove
 481  (`!s t:A->bool. FINITE t /\ s =_c t ==> FINITE s`,
 482   REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN MESON_TAC[CARD_LE_FINITE]);;
 483
 484 let CARD_LE_INFINITE = prove
 485  (`!s:A->bool t:B->bool. INFINITE s /\ s <=_c t ==> INFINITE t`,
 486   MESON_TAC[CARD_LE_FINITE; INFINITE]);;
 487
 488 let CARD_LT_FINITE_INFINITE = prove
 489  (`!s:A->bool t:B->bool. FINITE s /\ INFINITE t ==> s <_c t`,
 490   REWRITE_TAC[GSYM CARD_NOT_LE; INFINITE] THEN MESON_TAC[CARD_LE_FINITE]);;
 491
 492 let CARD_LE_CARD_IMP = prove
 493  (`!s:A->bool t:B->bool. FINITE t /\ s <=_c t ==> CARD s <= CARD t`,
 494   REPEAT STRIP_TAC THEN
 495   SUBGOAL_THEN `FINITE(s:A->bool)` ASSUME_TAC THENL
 496    [ASM_MESON_TAC[CARD_LE_FINITE]; ALL_TAC] THEN
 497   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [le_c]) THEN
 498   DISCH_THEN(X_CHOOSE_THEN `f:A->B` STRIP_ASSUME_TAC) THEN
 499   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `CARD(IMAGE (f:A->B) s)` THEN
 500   CONJ_TAC THENL
 501    [MATCH_MP_TAC(ARITH_RULE `(m = n:num) ==> n <= m`) THEN
 502     MATCH_MP_TAC CARD_IMAGE_INJ THEN ASM_REWRITE_TAC[];
 503     MATCH_MP_TAC CARD_SUBSET THEN ASM_REWRITE_TAC[] THEN
 504     ASM_MESON_TAC[SUBSET; IN_IMAGE]]);;
 505
 506 let CARD_EQ_CARD_IMP = prove
 507  (`!s:A->bool t:B->bool. FINITE t /\ s =_c t ==> (CARD s = CARD t)`,
 508   MESON_TAC[CARD_FINITE_CONG; LE_ANTISYM; CARD_LE_ANTISYM; CARD_LE_CARD_IMP]);;
 509
 510 let CARD_LE_CARD = prove
 511  (`!s:A->bool t:B->bool.
 512         FINITE s /\ FINITE t ==> (s <=_c t <=> CARD s <= CARD t)`,
 513   REPEAT STRIP_TAC THEN
 514   MATCH_MP_TAC(TAUT `(a ==> b) /\ (~a ==> ~b) ==> (a <=> b)`) THEN
 515   ASM_SIMP_TAC[CARD_LE_CARD_IMP] THEN
 516   REWRITE_TAC[CARD_NOT_LE; NOT_LE] THEN REWRITE_TAC[lt_c; LT_LE] THEN
 517   ASM_SIMP_TAC[CARD_LE_CARD_IMP] THEN
 518   MATCH_MP_TAC(TAUT `(c ==> a ==> b) ==> a /\ ~b ==> ~c`) THEN
 519   DISCH_TAC THEN GEN_REWRITE_TAC LAND_CONV [CARD_LE_EQ_SUBSET] THEN
 520   DISCH_THEN(X_CHOOSE_THEN `u:A->bool` STRIP_ASSUME_TAC) THEN
 521   MATCH_MP_TAC CARD_EQ_IMP_LE THEN
 522   SUBGOAL_THEN `u:A->bool = s` (fun th -> ASM_MESON_TAC[th; CARD_EQ_SYM]) THEN
 523   ASM_MESON_TAC[CARD_SUBSET_EQ; CARD_EQ_CARD_IMP; CARD_EQ_SYM]);;
 524
 525 let CARD_EQ_CARD = prove
 526  (`!s:A->bool t:B->bool.
 527         FINITE s /\ FINITE t ==> (s =_c t <=> (CARD s = CARD t))`,
 528   MESON_TAC[CARD_FINITE_CONG; LE_ANTISYM; CARD_LE_ANTISYM; CARD_LE_CARD]);;
 529
 530 let CARD_LT_CARD = prove
 531  (`!s:A->bool t:B->bool.
 532         FINITE s /\ FINITE t ==> (s <_c t <=> CARD s < CARD t)`,
 533   SIMP_TAC[CARD_LE_CARD; GSYM NOT_LE; GSYM CARD_NOT_LE]);;
 534
 535 let CARD_HAS_SIZE_CONG = prove
 536  (`!s:A->bool t:B->bool n. s HAS_SIZE n /\ s =_c t ==> t HAS_SIZE n`,
 537   REWRITE_TAC[HAS_SIZE] THEN
 538   MESON_TAC[CARD_EQ_CARD; CARD_FINITE_CONG]);;
 539
 540 let CARD_LE_IMAGE = prove
 541  (`!f s. IMAGE f s <=_c s`,
 542   REWRITE_TAC[LE_C; FORALL_IN_IMAGE] THEN MESON_TAC[]);;
 543
 544 let CARD_LE_IMAGE_GEN = prove
 545  (`!f:A->B s t. t SUBSET IMAGE f s ==> t <=_c s`,
 546   REPEAT STRIP_TAC THEN TRANS_TAC CARD_LE_TRANS `IMAGE (f:A->B) s` THEN
 547   ASM_SIMP_TAC[CARD_LE_IMAGE; CARD_LE_SUBSET]);;
 548
 549 let CARD_EQ_IMAGE = prove
 550  (`!f:A->B s.
 551         (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y)
 552         ==> IMAGE f s =_c s`,
 553   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[CARD_EQ_SYM] THEN
 554   REWRITE_TAC[eq_c] THEN EXISTS_TAC `f:A->B` THEN ASM SET_TAC[]);;
 555
 556 (* ------------------------------------------------------------------------- *)
 557 (* Cardinal arithmetic operations.                                           *)
 558 (* ------------------------------------------------------------------------- *)
 559
 560 parse_as_infix("+_c",(16,"right"));;
 561 parse_as_infix("*_c",(20,"right"));;
 562
 563 let add_c = new_definition
 564   `s +_c t = {INL x | x IN s} UNION {INR y | y IN t}`;;
 565
 566 let mul_c = new_definition
 567   `s *_c t = {(x,y) | x IN s /\ y IN t}`;;
 568
 569 (* ------------------------------------------------------------------------- *)
 570 (* Congruence properties for the arithmetic operators.                       *)
 571 (* ------------------------------------------------------------------------- *)
 572
 573 let CARD_LE_ADD = prove
 574  (`!s:A->bool s':B->bool t:C->bool t':D->bool.
 575       s <=_c s' /\ t <=_c t' ==> s +_c t <=_c s' +_c t'`,
 576   REPEAT GEN_TAC THEN REWRITE_TAC[le_c; add_c] THEN
 577   DISCH_THEN(CONJUNCTS_THEN2
 578    (X_CHOOSE_THEN `f:A->B` STRIP_ASSUME_TAC)
 579    (X_CHOOSE_THEN `g:C->D` STRIP_ASSUME_TAC)) THEN
 580   MP_TAC(prove_recursive_functions_exist sum_RECURSION
 581    `(!x. h(INL x) = INL((f:A->B) x)) /\ (!y. h(INR y) = INR((g:C->D) y))`) THEN
 582   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `h:(A+C)->(B+D)` THEN STRIP_TAC THEN
 583   REWRITE_TAC[IN_UNION; IN_ELIM_THM] THEN
 584   CONJ_TAC THEN REPEAT GEN_TAC THEN
 585   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
 586          ASM_REWRITE_TAC[]) THEN
 587   ASM_REWRITE_TAC[sum_DISTINCT;
 588                   sum_INJECTIVE] THEN
 589   ASM_MESON_TAC[]);;
 590
 591 let CARD_LE_MUL = prove
 592  (`!s:A->bool s':B->bool t:C->bool t':D->bool.
 593       s <=_c s' /\ t <=_c t' ==> s *_c t <=_c s' *_c t'`,
 594   REPEAT GEN_TAC THEN REWRITE_TAC[le_c; mul_c] THEN
 595   DISCH_THEN(CONJUNCTS_THEN2
 596    (X_CHOOSE_THEN `f:A->B` STRIP_ASSUME_TAC)
 597    (X_CHOOSE_THEN `g:C->D` STRIP_ASSUME_TAC)) THEN
 598   EXISTS_TAC `\(x,y). (f:A->B) x,(g:C->D) y` THEN
 599   REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_THM] THEN
 600   CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
 601   REWRITE_TAC[PAIR_EQ] THEN ASM_MESON_TAC[]);;
 602
 603 let CARD_FUNSPACE_LE = prove
 604  (`(:A) <=_c (:A') /\ (:B) <=_c (:B') ==> (:A->B) <=_c (:A'->B')`,
 605   REWRITE_TAC[le_c; IN_UNIV] THEN DISCH_THEN(CONJUNCTS_THEN2
 606    (X_CHOOSE_TAC `f:A->A'`) (X_CHOOSE_TAC `g:B->B'`)) THEN
 607   SUBGOAL_THEN `?f':A'->A. !x. f'(f x) = x` STRIP_ASSUME_TAC THENL
 608    [ASM_REWRITE_TAC[GSYM INJECTIVE_LEFT_INVERSE]; ALL_TAC] THEN
 609   EXISTS_TAC `\h. (g:B->B') o (h:A->B) o (f':A'->A)` THEN
 610   ASM_REWRITE_TAC[o_DEF; FUN_EQ_THM] THEN ASM_MESON_TAC[]);;
 611
 612 let CARD_ADD_CONG = prove
 613  (`!s:A->bool s':B->bool t:C->bool t':D->bool.
 614       s =_c s' /\ t =_c t' ==> s +_c t =_c s' +_c t'`,
 615   SIMP_TAC[CARD_LE_ADD; GSYM CARD_LE_ANTISYM]);;
 616
 617 let CARD_MUL_CONG = prove
 618  (`!s:A->bool s':B->bool t:C->bool t':D->bool.
 619       s =_c s' /\ t =_c t' ==> s *_c t =_c s' *_c t'`,
 620   SIMP_TAC[CARD_LE_MUL; GSYM CARD_LE_ANTISYM]);;
 621
 622 let CARD_FUNSPACE_CONG = prove
 623  (`(:A) =_c (:A') /\ (:B) =_c (:B') ==> (:A->B) =_c (:A'->B')`,
 624   SIMP_TAC[GSYM CARD_LE_ANTISYM; CARD_FUNSPACE_LE]);;
 625
 626 (* ------------------------------------------------------------------------- *)
 627 (* Misc lemmas.                                                              *)
 628 (* ------------------------------------------------------------------------- *)
 629
 630 let MUL_C_UNIV = prove
 631  (`(:A) *_c (:B) = (:A#B)`,
 632   REWRITE_TAC[EXTENSION; FORALL_PAIR_THM; mul_c; IN_ELIM_PAIR_THM; IN_UNIV]);;
 633
 634 let CARD_FUNSPACE_CURRY = prove
 635  (`(:A->B->C) =_c (:A#B->C)`,
 636   REWRITE_TAC[EQ_C_BIJECTIONS] THEN
 637   EXISTS_TAC `\(f:A->B->C) (x,y). f x y` THEN
 638   EXISTS_TAC `\(g:A#B->C) x y. g(x,y)` THEN
 639   REWRITE_TAC[IN_UNIV] THEN
 640   REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM]);;
 641
 642 let IN_CARD_ADD = prove
 643  (`(!x. INL(x) IN (s +_c t) <=> x IN s) /\
 644    (!y. INR(y) IN (s +_c t) <=> y IN t)`,
 645   REWRITE_TAC[add_c; IN_UNION; IN_ELIM_THM] THEN
 646   REWRITE_TAC[sum_DISTINCT; sum_INJECTIVE] THEN MESON_TAC[]);;
 647
 648 let IN_CARD_MUL = prove
 649  (`!s t x y. (x,y) IN (s *_c t) <=> x IN s /\ y IN t`,
 650   REWRITE_TAC[mul_c; IN_ELIM_THM; PAIR_EQ] THEN MESON_TAC[]);;
 651
 652 let CARD_LE_SQUARE = prove
 653  (`!s:A->bool. s <=_c s *_c s`,
 654   GEN_TAC THEN REWRITE_TAC[le_c] THEN EXISTS_TAC `\x:A. x,(@z:A. z IN s)` THEN
 655   SIMP_TAC[IN_CARD_MUL; PAIR_EQ] THEN
 656   CONV_TAC(ONCE_DEPTH_CONV SELECT_CONV) THEN MESON_TAC[]);;
 657
 658 let CARD_SQUARE_NUM = prove
 659  (`(UNIV:num->bool) *_c (UNIV:num->bool) =_c (UNIV:num->bool)`,
 660   REWRITE_TAC[GSYM CARD_LE_ANTISYM; CARD_LE_SQUARE] THEN
 661   REWRITE_TAC[le_c; IN_UNIV; mul_c; IN_ELIM_THM] THEN
 662   EXISTS_TAC `\(x,y). NUMPAIR x y` THEN
 663   REWRITE_TAC[FORALL_PAIR_THM] THEN
 664   CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN MESON_TAC[NUMPAIR_INJ]);;
 665
 666 let UNION_LE_ADD_C = prove
 667  (`!s t:A->bool. (s UNION t) <=_c s +_c t`,
 668   REPEAT GEN_TAC THEN MATCH_MP_TAC CARD_LE_IMAGE_GEN THEN
 669   EXISTS_TAC `function INL x -> (x:A) | INR x -> x` THEN
 670   REWRITE_TAC[add_c; IMAGE_UNION] THEN ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN
 671   REWRITE_TAC[GSYM IMAGE_o; o_DEF] THEN SET_TAC[]);;
 672
 673 let CARD_ADD_C = prove
 674  (`!s t. FINITE s /\ FINITE t ==> CARD(s +_c t) = CARD s + CARD t`,
 675   REPEAT STRIP_TAC THEN REWRITE_TAC[add_c] THEN
 676   W(MP_TAC o PART_MATCH (lhs o rand) CARD_UNION o lhand o snd) THEN
 677   ASM_SIMP_TAC[SIMPLE_IMAGE; FINITE_IMAGE] THEN
 678   REWRITE_TAC[SET_RULE `IMAGE f s INTER IMAGE g t = {} <=>
 679                         !x y. x IN s /\ y IN t ==> ~(f x = g y)`] THEN
 680   REWRITE_TAC[sum_DISTINCT] THEN DISCH_THEN SUBST1_TAC THEN
 681   BINOP_TAC THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN
 682   ASM_SIMP_TAC[sum_INJECTIVE]);;
 683
 684 (* ------------------------------------------------------------------------- *)
 685 (* Various "arithmetical" lemmas.                                            *)
 686 (* ------------------------------------------------------------------------- *)
 687
 688 let CARD_ADD_SYM = prove
 689  (`!s:A->bool t:B->bool. s +_c t =_c t +_c s`,
 690   REPEAT GEN_TAC THEN REWRITE_TAC[eq_c] THEN
 691   MP_TAC(prove_recursive_functions_exist sum_RECURSION
 692     `(!x. (h:A+B->B+A) (INL x) = INR x) /\ (!y. h(INR y) = INL y)`) THEN
 693   MATCH_MP_TAC MONO_EXISTS THEN
 694   SIMP_TAC[FORALL_SUM_THM; EXISTS_SUM_THM; EXISTS_UNIQUE_THM] THEN
 695   REWRITE_TAC[sum_DISTINCT; sum_INJECTIVE; IN_CARD_ADD] THEN MESON_TAC[]);;
 696
 697 let CARD_ADD_ASSOC = prove
 698  (`!s:A->bool t:B->bool u:C->bool. s +_c (t +_c u) =_c (s +_c t) +_c u`,
 699   REPEAT GEN_TAC THEN REWRITE_TAC[eq_c] THEN
 700   CHOOSE_TAC(prove_recursive_functions_exist sum_RECURSION
 701     `(!u. (i:B+C->(A+B)+C) (INL u) = INL(INR u)) /\
 702      (!v. i(INR v) = INR v)`) THEN
 703   MP_TAC(prove_recursive_functions_exist sum_RECURSION
 704     `(!x. (h:A+B+C->(A+B)+C) (INL x) = INL(INL x)) /\
 705      (!z. h(INR z) = i(z))`) THEN
 706   MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN STRIP_TAC THEN
 707   ASM_REWRITE_TAC[FORALL_SUM_THM; EXISTS_SUM_THM; EXISTS_UNIQUE_THM;
 708                   sum_DISTINCT; sum_INJECTIVE; IN_CARD_ADD] THEN
 709   MESON_TAC[]);;
 710
 711 let CARD_MUL_SYM = prove
 712  (`!s:A->bool t:B->bool. s *_c t =_c t *_c s`,
 713   REPEAT GEN_TAC THEN REWRITE_TAC[eq_c] THEN
 714   MP_TAC(prove_recursive_functions_exist pair_RECURSION
 715     `(!x:A y:B. h(x,y) = (y,x))`) THEN
 716   MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN STRIP_TAC THEN
 717   REWRITE_TAC[EXISTS_UNIQUE_THM; FORALL_PAIR_THM; EXISTS_PAIR_THM] THEN
 718   ASM_REWRITE_TAC[FORALL_PAIR_THM; IN_CARD_MUL; PAIR_EQ] THEN
 719   MESON_TAC[]);;
 720
 721 let CARD_MUL_ASSOC = prove
 722  (`!s:A->bool t:B->bool u:C->bool. s *_c (t *_c u) =_c (s *_c t) *_c u`,
 723   REPEAT GEN_TAC THEN REWRITE_TAC[eq_c] THEN
 724   CHOOSE_TAC(prove_recursive_functions_exist pair_RECURSION
 725     `(!x y z. (i:A->B#C->(A#B)#C) x (y,z) = (x,y),z)`) THEN
 726   MP_TAC(prove_recursive_functions_exist pair_RECURSION
 727     `(!x p. (h:A#B#C->(A#B)#C) (x,p) = i x p)`) THEN
 728   MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN STRIP_TAC THEN
 729   REWRITE_TAC[EXISTS_UNIQUE_THM; FORALL_PAIR_THM; EXISTS_PAIR_THM] THEN
 730   ASM_REWRITE_TAC[FORALL_PAIR_THM; IN_CARD_MUL; PAIR_EQ] THEN
 731   MESON_TAC[]);;
 732
 733 let CARD_LDISTRIB = prove
 734  (`!s:A->bool t:B->bool u:C->bool.
 735         s *_c (t +_c u) =_c (s *_c t) +_c (s *_c u)`,
 736   REPEAT GEN_TAC THEN REWRITE_TAC[eq_c] THEN
 737   CHOOSE_TAC(prove_recursive_functions_exist sum_RECURSION
 738     `(!x y. (i:A->(B+C)->A#B+A#C) x (INL y) = INL(x,y)) /\
 739      (!x z. (i:A->(B+C)->A#B+A#C) x (INR z) = INR(x,z))`) THEN
 740   MP_TAC(prove_recursive_functions_exist pair_RECURSION
 741     `(!x s. (h:A#(B+C)->(A#B)+(A#C)) (x,s) = i x s)`) THEN
 742   MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN STRIP_TAC THEN
 743   ASM_REWRITE_TAC[EXISTS_UNIQUE_THM; FORALL_PAIR_THM; EXISTS_PAIR_THM;
 744                   FORALL_SUM_THM; EXISTS_SUM_THM; PAIR_EQ; IN_CARD_MUL;
 745                   sum_DISTINCT; sum_INJECTIVE; IN_CARD_ADD] THEN
 746   MESON_TAC[]);;
 747
 748 let CARD_RDISTRIB = prove
 749  (`!s:A->bool t:B->bool u:C->bool.
 750         (s +_c t) *_c u =_c (s *_c u) +_c (t *_c u)`,
 751   REPEAT GEN_TAC THEN
 752   TRANS_TAC CARD_EQ_TRANS
 753    `(u:C->bool) *_c ((s:A->bool) +_c (t:B->bool))` THEN
 754   REWRITE_TAC[CARD_MUL_SYM] THEN
 755   TRANS_TAC CARD_EQ_TRANS
 756    `(u:C->bool) *_c (s:A->bool) +_c (u:C->bool) *_c (t:B->bool)` THEN
 757   REWRITE_TAC[CARD_LDISTRIB] THEN
 758   MATCH_MP_TAC CARD_ADD_CONG THEN REWRITE_TAC[CARD_MUL_SYM]);;
 759
 760 let CARD_LE_ADDR = prove
 761  (`!s:A->bool t:B->bool. s <=_c s +_c t`,
 762   REPEAT GEN_TAC THEN REWRITE_TAC[le_c] THEN
 763   EXISTS_TAC `INL:A->A+B` THEN SIMP_TAC[IN_CARD_ADD; sum_INJECTIVE]);;
 764
 765 let CARD_LE_ADDL = prove
 766  (`!s:A->bool t:B->bool. t <=_c s +_c t`,
 767   REPEAT GEN_TAC THEN REWRITE_TAC[le_c] THEN
 768   EXISTS_TAC `INR:B->A+B` THEN SIMP_TAC[IN_CARD_ADD; sum_INJECTIVE]);;
 769
 770 (* ------------------------------------------------------------------------- *)
 771 (* A rather special lemma but temporarily useful.                            *)
 772 (* ------------------------------------------------------------------------- *)
 773
 774 let CARD_ADD_LE_MUL_INFINITE = prove
 775  (`!s:A->bool. INFINITE s ==> s +_c s <=_c s *_c s`,
 776   GEN_TAC THEN REWRITE_TAC[INFINITE_CARD_LE; le_c; IN_UNIV] THEN
 777   DISCH_THEN(X_CHOOSE_THEN `f:num->A` STRIP_ASSUME_TAC) THEN
 778   MP_TAC(prove_recursive_functions_exist sum_RECURSION
 779     `(!x. h(INL x) = (f(0),x):A#A) /\ (!x. h(INR x) = (f(1),x))`) THEN
 780   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `h:A+A->A#A` THEN
 781   STRIP_TAC THEN
 782   REPEAT((MATCH_MP_TAC sum_INDUCT THEN
 783           ASM_REWRITE_TAC[IN_CARD_ADD; IN_CARD_MUL; PAIR_EQ])
 784          ORELSE STRIP_TAC) THEN
 785   ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[NUM_REDUCE_CONV `1 = 0`]);;
 786
 787 (* ------------------------------------------------------------------------- *)
 788 (* Relate cardinal addition to the simple union operation.                   *)
 789 (* ------------------------------------------------------------------------- *)
 790
 791 let CARD_DISJOINT_UNION = prove
 792  (`!s:A->bool t. (s INTER t = {}) ==> (s UNION t =_c s +_c t)`,
 793   REPEAT GEN_TAC THEN REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
 794   STRIP_TAC THEN REWRITE_TAC[eq_c; IN_UNION] THEN
 795   EXISTS_TAC `\x:A. if x IN s then INL x else INR x` THEN
 796   REWRITE_TAC[FORALL_SUM_THM; IN_CARD_ADD] THEN
 797   REWRITE_TAC[COND_RAND; COND_RATOR] THEN
 798   REWRITE_TAC[TAUT `(if b then x else y) <=> b /\ x \/ ~b /\ y`] THEN
 799   REWRITE_TAC[sum_DISTINCT; sum_INJECTIVE; IN_CARD_ADD] THEN
 800   ASM_MESON_TAC[]);;
 801
 802 (* ------------------------------------------------------------------------- *)
 803 (* The key to arithmetic on infinite cardinals: k^2 = k.                     *)
 804 (* ------------------------------------------------------------------------- *)
 805
 806 let CARD_SQUARE_INFINITE = prove
 807  (`!k:A->bool. INFINITE k ==> (k *_c k =_c k)`,
 808   let lemma = prove
 809    (`INFINITE(s:A->bool) /\ s SUBSET k /\
 810      (!x y. R(x,y) ==> x IN (s *_c s) /\ y IN s) /\
 811      (!x. x IN (s *_c s) ==> ?!y. y IN s /\ R(x,y)) /\
 812      (!y:A. y IN s ==> ?!x. x IN (s *_c s) /\ R(x,y))
 813      ==> (s = {z | ?p. R(p,z)})`,
 814     REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN MESON_TAC[]) in
 815   REPEAT STRIP_TAC THEN
 816   ABBREV_TAC
 817     `P = \R. ?s. INFINITE(s:A->bool) /\ s SUBSET k /\
 818                  (!x y. R(x,y) ==> x IN (s *_c s) /\ y IN s) /\
 819                  (!x. x IN (s *_c s) ==> ?!y. y IN s /\ R(x,y)) /\
 820                  (!y. y IN s ==> ?!x. x IN (s *_c s) /\ R(x,y))` THEN
 821   MP_TAC(ISPEC `P:((A#A)#A->bool)->bool` ZL_SUBSETS_UNIONS_NONEMPTY) THEN
 822   ANTS_TAC THENL
 823    [CONJ_TAC THENL
 824      [FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[] THEN
 825       ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
 826       REWRITE_TAC[RIGHT_EXISTS_AND_THM; GSYM EQ_C] THEN
 827       FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INFINITE_CARD_LE]) THEN
 828       REWRITE_TAC[CARD_LE_EQ_SUBSET] THEN
 829       MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `s:A->bool` THEN
 830       STRIP_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
 831        [ASM_MESON_TAC[num_INFINITE; CARD_INFINITE_CONG]; ALL_TAC] THEN
 832       FIRST_ASSUM(fun th ->
 833        MP_TAC(MATCH_MP CARD_MUL_CONG (CONJ th th))) THEN
 834       GEN_REWRITE_TAC LAND_CONV [CARD_EQ_SYM] THEN
 835       DISCH_THEN(MP_TAC o C CONJ CARD_SQUARE_NUM) THEN
 836       DISCH_THEN(MP_TAC o MATCH_MP CARD_EQ_TRANS) THEN
 837       FIRST_ASSUM(fun th ->
 838         DISCH_THEN(ACCEPT_TAC o MATCH_MP CARD_EQ_TRANS o C CONJ th));
 839       ALL_TAC] THEN
 840     SUBGOAL_THEN
 841      `P = \R. INFINITE {z | ?x y. R((x,y),z)} /\
 842               (!x:A y z. R((x,y),z) ==> x IN k /\ y IN k /\ z IN k) /\
 843               (!x y. (?u v. R((u,v),x)) /\ (?u v. R((u,v),y))
 844                      ==> ?z. R((x,y),z)) /\
 845               (!x y. (?z. R((x,y),z))
 846                      ==> (?u v. R((u,v),x)) /\ (?u v. R((u,v),y))) /\
 847               (!x y z1 z2. R((x,y),z1) /\ R((x,y),z2) ==> (z1 = z2)) /\
 848               (!x1 y1 x2 y2 z. R((x1,y1),z) /\ R((x2,y2),z)
 849                                ==> (x1 = x2) /\ (y1 = y2))`
 850     SUBST1_TAC THENL
 851      [FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[] THEN
 852       ONCE_REWRITE_TAC[MATCH_MP(TAUT `(a ==> b) ==> (a <=> b /\ a)`) lemma] THEN
 853       REWRITE_TAC[UNWIND_THM2] THEN REWRITE_TAC[FUN_EQ_THM] THEN
 854       REWRITE_TAC[IN_CARD_MUL; EXISTS_PAIR_THM; SUBSET; FUN_EQ_THM;
 855                   IN_ELIM_THM; FORALL_PAIR_THM; EXISTS_UNIQUE_THM;
 856                   UNIONS; PAIR_EQ] THEN
 857       GEN_TAC THEN AP_TERM_TAC THEN MESON_TAC[];
 858       ALL_TAC] THEN
 859     FIRST_X_ASSUM(K ALL_TAC o SYM) THEN REWRITE_TAC[] THEN GEN_TAC THEN
 860     GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
 861      [TAUT `a ==> b /\ c <=> (a ==> b) /\ (a ==> c)`] THEN
 862     GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [FORALL_AND_THM] THEN
 863     MATCH_MP_TAC(TAUT
 864      `(c /\ d ==> f) /\ (a /\ b ==> e)
 865       ==> (a /\ (b /\ c) /\ d ==> e /\ f)`) THEN
 866     CONJ_TAC THENL
 867      [REWRITE_TAC[UNIONS; IN_ELIM_THM] THEN
 868       REWRITE_TAC[SUBSET; IN] THEN MESON_TAC[];
 869       ALL_TAC] THEN
 870     DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `s:(A#A)#A->bool`) MP_TAC) THEN
 871     DISCH_THEN(MP_TAC o SPEC `s:(A#A)#A->bool`) THEN
 872     ASM_REWRITE_TAC[INFINITE; CONTRAPOS_THM] THEN
 873     MATCH_MP_TAC(ONCE_REWRITE_RULE[TAUT `a /\ b ==> c <=> b ==> a ==> c`]
 874                       FINITE_SUBSET) THEN
 875     REWRITE_TAC[SUBSET; IN_ELIM_THM; UNIONS] THEN ASM_MESON_TAC[IN];
 876     ALL_TAC] THEN
 877   FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[] THEN
 878   DISCH_THEN(X_CHOOSE_THEN `R:(A#A)#A->bool`
 879    (CONJUNCTS_THEN2 (X_CHOOSE_TAC `s:A->bool`) ASSUME_TAC)) THEN
 880   SUBGOAL_THEN `(s:A->bool) *_c s =_c s` ASSUME_TAC THENL
 881    [REWRITE_TAC[EQ_C] THEN EXISTS_TAC `R:(A#A)#A->bool` THEN ASM_REWRITE_TAC[];
 882     ALL_TAC] THEN
 883   SUBGOAL_THEN `s +_c s <=_c (s:A->bool)` ASSUME_TAC THENL
 884    [TRANS_TAC CARD_LE_TRANS `(s:A->bool) *_c s` THEN
 885     ASM_SIMP_TAC[CARD_EQ_IMP_LE; CARD_ADD_LE_MUL_INFINITE];
 886     ALL_TAC] THEN
 887   SUBGOAL_THEN `(s:A->bool) INTER (k DIFF s) = {}` ASSUME_TAC THENL
 888    [REWRITE_TAC[EXTENSION; IN_INTER; IN_DIFF; NOT_IN_EMPTY] THEN MESON_TAC[];
 889     ALL_TAC] THEN
 890   DISJ_CASES_TAC(ISPECL [`k DIFF (s:A->bool)`; `s:A->bool`] CARD_LE_TOTAL)
 891   THENL
 892    [SUBGOAL_THEN `k = (s:A->bool) UNION (k DIFF s)` SUBST1_TAC THENL
 893      [FIRST_ASSUM(MP_TAC o CONJUNCT1 o CONJUNCT2) THEN
 894       REWRITE_TAC[SUBSET; EXTENSION; IN_INTER; NOT_IN_EMPTY;
 895                   IN_UNION; IN_DIFF] THEN
 896       MESON_TAC[];
 897       ALL_TAC] THEN
 898     REWRITE_TAC[GSYM CARD_LE_ANTISYM; CARD_LE_SQUARE] THEN
 899     TRANS_TAC CARD_LE_TRANS
 900      `((s:A->bool) +_c (k DIFF s:A->bool)) *_c (s +_c k DIFF s)` THEN
 901     ASM_SIMP_TAC[CARD_DISJOINT_UNION; CARD_EQ_IMP_LE; CARD_MUL_CONG] THEN
 902     TRANS_TAC CARD_LE_TRANS `((s:A->bool) +_c s) *_c (s +_c s)` THEN
 903     ASM_SIMP_TAC[CARD_LE_ADD; CARD_LE_MUL; CARD_LE_REFL] THEN
 904     TRANS_TAC CARD_LE_TRANS `(s:A->bool) *_c s` THEN
 905     ASM_SIMP_TAC[CARD_LE_MUL] THEN
 906     TRANS_TAC CARD_LE_TRANS `s:A->bool` THEN ASM_SIMP_TAC[CARD_EQ_IMP_LE] THEN
 907     REWRITE_TAC[CARD_LE_EQ_SUBSET] THEN EXISTS_TAC `s:A->bool` THEN
 908     SIMP_TAC[CARD_EQ_REFL; SUBSET; IN_UNION];
 909     ALL_TAC] THEN
 910   UNDISCH_TAC `s:A->bool <=_c k DIFF s` THEN
 911   REWRITE_TAC[CARD_LE_EQ_SUBSET] THEN
 912   DISCH_THEN(X_CHOOSE_THEN `d:A->bool` STRIP_ASSUME_TAC) THEN
 913   SUBGOAL_THEN `(s:A->bool *_c d) UNION (d *_c s) UNION (d *_c d) =_c d`
 914   MP_TAC THENL
 915    [TRANS_TAC CARD_EQ_TRANS
 916        `((s:A->bool) *_c (d:A->bool)) +_c ((d *_c s) +_c (d *_c d))` THEN
 917     CONJ_TAC THENL
 918      [TRANS_TAC CARD_EQ_TRANS
 919        `((s:A->bool) *_c d) +_c ((d *_c s) UNION (d *_c d))` THEN
 920       CONJ_TAC THENL
 921        [ALL_TAC;
 922         MATCH_MP_TAC CARD_ADD_CONG THEN REWRITE_TAC[CARD_EQ_REFL]] THEN
 923       MATCH_MP_TAC CARD_DISJOINT_UNION THEN
 924       UNDISCH_TAC `s INTER (k DIFF s:A->bool) = {}` THEN
 925       UNDISCH_TAC `d SUBSET (k DIFF s:A->bool)` THEN
 926       REWRITE_TAC[EXTENSION; SUBSET; FORALL_PAIR_THM; NOT_IN_EMPTY;
 927                   IN_INTER; IN_UNION; IN_CARD_MUL; IN_DIFF] THEN MESON_TAC[];
 928       ALL_TAC] THEN
 929     TRANS_TAC CARD_EQ_TRANS `s:A->bool` THEN ASM_REWRITE_TAC[] THEN
 930     TRANS_TAC CARD_EQ_TRANS
 931       `(s:A->bool *_c s) +_c (s *_c s) +_c (s *_c s)` THEN
 932     CONJ_TAC THENL
 933      [REPEAT(MATCH_MP_TAC CARD_ADD_CONG THEN CONJ_TAC) THEN
 934       MATCH_MP_TAC CARD_MUL_CONG THEN ASM_REWRITE_TAC[CARD_EQ_REFL] THEN
 935       ONCE_REWRITE_TAC[CARD_EQ_SYM] THEN ASM_REWRITE_TAC[];
 936       ALL_TAC] THEN
 937     TRANS_TAC CARD_EQ_TRANS `(s:A->bool) +_c s +_c s` THEN CONJ_TAC THENL
 938      [REPEAT(MATCH_MP_TAC CARD_ADD_CONG THEN ASM_REWRITE_TAC[]);
 939       ALL_TAC] THEN
 940     REWRITE_TAC[GSYM CARD_LE_ANTISYM; CARD_LE_ADDR] THEN
 941     TRANS_TAC CARD_LE_TRANS `(s:A->bool) +_c s` THEN
 942     ASM_SIMP_TAC[CARD_LE_ADD; CARD_LE_REFL];
 943     ALL_TAC] THEN
 944   FIRST_X_ASSUM(CONJUNCTS_THEN ASSUME_TAC) THEN
 945   FIRST_X_ASSUM(CONJUNCTS_THEN ASSUME_TAC) THEN
 946   REWRITE_TAC[EQ_C; IN_UNION] THEN
 947   DISCH_THEN(X_CHOOSE_TAC `S:(A#A)#A->bool`) THEN
 948   FIRST_X_ASSUM(MP_TAC o SPEC `\x:(A#A)#A. R(x) \/ S(x)`) THEN
 949   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN DISCH_THEN(K ALL_TAC) THEN
 950   REWRITE_TAC[NOT_IMP] THEN REPEAT CONJ_TAC THENL
 951    [EXISTS_TAC `(s:A->bool) UNION d`;
 952     SIMP_TAC[SUBSET; IN];
 953     SUBGOAL_THEN `~(d:A->bool = {})` MP_TAC THENL
 954      [DISCH_THEN(MP_TAC o AP_TERM `FINITE:(A->bool)->bool`) THEN
 955       REWRITE_TAC[FINITE_RULES; GSYM INFINITE] THEN
 956       ASM_MESON_TAC[CARD_INFINITE_CONG];
 957       ALL_TAC] THEN
 958     REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN DISCH_THEN(X_CHOOSE_TAC `a:A`) THEN
 959     FIRST_ASSUM(MP_TAC o C MATCH_MP
 960      (ASSUME `a:A IN d`) o last o CONJUNCTS) THEN
 961     DISCH_THEN(MP_TAC o EXISTENCE) THEN
 962     DISCH_THEN(X_CHOOSE_THEN `b:A#A` (CONJUNCTS_THEN ASSUME_TAC)) THEN
 963     REWRITE_TAC[EXTENSION; NOT_FORALL_THM] THEN
 964     EXISTS_TAC `(b:A#A,a:A)` THEN ASM_REWRITE_TAC[IN] THEN
 965     DISCH_THEN(fun th -> FIRST_ASSUM
 966      (MP_TAC o CONJUNCT2 o C MATCH_MP th o CONJUNCT1)) THEN
 967     MAP_EVERY UNDISCH_TAC
 968      [`a:A IN d`; `(d:A->bool) SUBSET (k DIFF s)`] THEN
 969     REWRITE_TAC[SUBSET; IN_DIFF] THEN MESON_TAC[]] THEN
 970   REWRITE_TAC[INFINITE; FINITE_UNION; DE_MORGAN_THM] THEN
 971   ASM_REWRITE_TAC[GSYM INFINITE] THEN CONJ_TAC THENL
 972    [MAP_EVERY UNDISCH_TAC
 973      [`(d:A->bool) SUBSET (k DIFF s)`; `(s:A->bool) SUBSET k`] THEN
 974     REWRITE_TAC[SUBSET; IN_UNION; IN_DIFF] THEN MESON_TAC[];
 975     ALL_TAC] THEN
 976   REPEAT(FIRST_ASSUM(UNDISCH_TAC o check is_conj o concl)) THEN
 977   REWRITE_TAC[FORALL_PAIR_THM; EXISTS_UNIQUE_THM; EXISTS_PAIR_THM;
 978               IN_CARD_MUL; IN_UNION; PAIR_EQ] THEN
 979   MAP_EVERY UNDISCH_TAC
 980    [`(s:A->bool) SUBSET k`;
 981     `(d:A->bool) SUBSET (k DIFF s)`] THEN
 982   REWRITE_TAC[SUBSET; EXTENSION; NOT_IN_EMPTY; IN_INTER; IN_DIFF] THEN
 983   POP_ASSUM_LIST(K ALL_TAC) THEN
 984   REPEAT DISCH_TAC THEN REPEAT CONJ_TAC THENL
 985    [ASM_MESON_TAC[]; ASM_MESON_TAC[]; ALL_TAC] THEN
 986   GEN_TAC THEN DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
 987    [ASM_MESON_TAC[]; ALL_TAC] THEN
 988   DISCH_THEN(fun th -> CONJ_TAC THEN MP_TAC th) THENL
 989    [ALL_TAC; ASM_MESON_TAC[]] THEN
 990   DISCH_THEN(fun th ->
 991    FIRST_ASSUM(MP_TAC o C MATCH_MP th o last o CONJUNCTS)) THEN
 992   MESON_TAC[]);;
 993
 994 (* ------------------------------------------------------------------------- *)
 995 (* Preservation of finiteness.                                               *)
 996 (* ------------------------------------------------------------------------- *)
 997
 998 let CARD_ADD_FINITE = prove
 999  (`!s t. FINITE s /\ FINITE t ==> FINITE(s +_c t)`,
1000   SIMP_TAC[add_c; FINITE_UNION; SIMPLE_IMAGE; FINITE_IMAGE]);;
1001
1002 let CARD_ADD_FINITE_EQ = prove
1003  (`!s:A->bool t:B->bool. FINITE(s +_c t) <=> FINITE s /\ FINITE t`,
1004   REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[CARD_ADD_FINITE] THEN
1005   DISCH_THEN(fun th -> CONJ_TAC THEN MP_TAC th) THEN
1006   MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] CARD_LE_FINITE) THEN
1007   REWRITE_TAC[CARD_LE_ADDL; CARD_LE_ADDR]);;
1008
1009 let CARD_MUL_FINITE = prove
1010  (`!s t. FINITE s /\ FINITE t ==> FINITE(s *_c t)`,
1011   SIMP_TAC[mul_c; FINITE_PRODUCT]);;
1012
1013 (* ------------------------------------------------------------------------- *)
1014 (* Hence the "absorption laws" for arithmetic with an infinite cardinal.     *)
1015 (* ------------------------------------------------------------------------- *)
1016
1017 let CARD_MUL_ABSORB_LE = prove
1018  (`!s:A->bool t:B->bool. INFINITE(t) /\ s <=_c t ==> s *_c t <=_c t`,
1019   REPEAT STRIP_TAC THEN
1020   TRANS_TAC CARD_LE_TRANS `(t:B->bool) *_c t` THEN
1021   ASM_SIMP_TAC[CARD_LE_MUL; CARD_LE_REFL;
1022                CARD_SQUARE_INFINITE; CARD_EQ_IMP_LE]);;
1023
1024 let CARD_MUL2_ABSORB_LE = prove
1025  (`!s:A->bool t:B->bool u:C->bool.
1026      INFINITE(u) /\ s <=_c u /\ t <=_c u ==> s *_c t <=_c u`,
1027   REPEAT STRIP_TAC THEN
1028   TRANS_TAC CARD_LE_TRANS `(s:A->bool) *_c (u:C->bool)` THEN
1029   ASM_SIMP_TAC[CARD_MUL_ABSORB_LE] THEN MATCH_MP_TAC CARD_LE_MUL THEN
1030   ASM_REWRITE_TAC[CARD_LE_REFL]);;
1031
1032 let CARD_ADD_ABSORB_LE = prove
1033  (`!s:A->bool t:B->bool. INFINITE(t) /\ s <=_c t ==> s +_c t <=_c t`,
1034   REPEAT STRIP_TAC THEN
1035   TRANS_TAC CARD_LE_TRANS `(t:B->bool) *_c t` THEN
1036   ASM_SIMP_TAC[CARD_SQUARE_INFINITE; CARD_EQ_IMP_LE] THEN
1037   TRANS_TAC CARD_LE_TRANS `(t:B->bool) +_c t` THEN
1038   ASM_SIMP_TAC[CARD_ADD_LE_MUL_INFINITE; CARD_LE_ADD; CARD_LE_REFL]);;
1039
1040 let CARD_ADD2_ABSORB_LE = prove
1041  (`!s:A->bool t:B->bool u:C->bool.
1042      INFINITE(u) /\ s <=_c u /\ t <=_c u ==> s +_c t <=_c u`,
1043   REPEAT STRIP_TAC THEN
1044   TRANS_TAC CARD_LE_TRANS `(s:A->bool) +_c (u:C->bool)` THEN
1045   ASM_SIMP_TAC[CARD_ADD_ABSORB_LE] THEN MATCH_MP_TAC CARD_LE_ADD THEN
1046   ASM_REWRITE_TAC[CARD_LE_REFL]);;
1047
1048 let CARD_MUL_ABSORB = prove
1049  (`!s:A->bool t:B->bool.
1050      INFINITE(t) /\ ~(s = {}) /\ s <=_c t ==> s *_c t =_c t`,
1051   SIMP_TAC[GSYM CARD_LE_ANTISYM; CARD_MUL_ABSORB_LE] THEN REPEAT STRIP_TAC THEN
1052   FIRST_X_ASSUM(X_CHOOSE_TAC `a:A` o
1053    GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
1054   REWRITE_TAC[le_c] THEN EXISTS_TAC `\x:B. (a:A,x)` THEN
1055   ASM_SIMP_TAC[IN_CARD_MUL; PAIR_EQ]);;
1056
1057 let CARD_ADD_ABSORB = prove
1058  (`!s:A->bool t:B->bool. INFINITE(t) /\ s <=_c t ==> s +_c t =_c t`,
1059   SIMP_TAC[GSYM CARD_LE_ANTISYM; CARD_LE_ADDL; CARD_ADD_ABSORB_LE]);;
1060
1061 let CARD_ADD2_ABSORB_LT = prove
1062  (`!s:A->bool t:B->bool u:C->bool.
1063         INFINITE u /\ s <_c u /\ t <_c u ==> s +_c t <_c u`,
1064   REPEAT STRIP_TAC THEN
1065   ASM_CASES_TAC `FINITE((s:A->bool) +_c (t:B->bool))` THEN
1066   ASM_SIMP_TAC[CARD_LT_FINITE_INFINITE] THEN
1067   DISJ_CASES_TAC(ISPECL [`s:A->bool`; `t:B->bool`] CARD_LE_TOTAL) THENL
1068    [ASM_CASES_TAC `FINITE(t:B->bool)` THENL
1069      [ASM_MESON_TAC[CARD_LE_FINITE; CARD_ADD_FINITE];
1070       TRANS_TAC CARD_LET_TRANS `t:B->bool`];
1071     ASM_CASES_TAC `FINITE(s:A->bool)` THENL
1072      [ASM_MESON_TAC[CARD_LE_FINITE; CARD_ADD_FINITE];
1073       TRANS_TAC CARD_LET_TRANS `s:A->bool`]] THEN
1074   ASM_REWRITE_TAC[] THEN
1075   MATCH_MP_TAC CARD_ADD2_ABSORB_LE THEN
1076   ASM_REWRITE_TAC[INFINITE; CARD_LE_REFL]);;
1077
1078 let CARD_LT_ADD = prove
1079  (`!s:A->bool s':B->bool t:C->bool t':D->bool.
1080         s <_c s' /\ t <_c t' ==> s +_c t <_c s' +_c t'`,
1081   REPEAT STRIP_TAC THEN
1082   ASM_CASES_TAC `FINITE((s':B->bool) +_c (t':D->bool))` THENL
1083    [FIRST_X_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I
1084       [CARD_ADD_FINITE_EQ]) THEN
1085     SUBGOAL_THEN `FINITE(s:A->bool) /\ FINITE(t:C->bool)`
1086     STRIP_ASSUME_TAC THENL
1087      [CONJ_TAC THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
1088         (REWRITE_RULE[IMP_CONJ_ALT] CARD_LE_FINITE) o
1089         MATCH_MP CARD_LT_IMP_LE) THEN
1090       ASM_REWRITE_TAC[];
1091       MAP_EVERY UNDISCH_TAC
1092        [`(s:A->bool) <_c (s':B->bool)`;
1093         `(t:C->bool) <_c (t':D->bool)`] THEN
1094       ASM_SIMP_TAC[CARD_LT_CARD; CARD_ADD_FINITE; CARD_ADD_C] THEN
1095       ARITH_TAC];
1096     MATCH_MP_TAC CARD_ADD2_ABSORB_LT THEN ASM_REWRITE_TAC[INFINITE] THEN
1097     CONJ_TAC THENL
1098      [TRANS_TAC CARD_LTE_TRANS `s':B->bool` THEN
1099       ASM_REWRITE_TAC[CARD_LE_ADDR];
1100       TRANS_TAC CARD_LTE_TRANS `t':D->bool` THEN
1101       ASM_REWRITE_TAC[CARD_LE_ADDL]]]);;
1102
1103 (* ------------------------------------------------------------------------- *)
1104 (* Some more ad-hoc but useful theorems.                                     *)
1105 (* ------------------------------------------------------------------------- *)
1106
1107 let CARD_MUL_LT_LEMMA = prove
1108  (`!s t:B->bool u. s <=_c t /\ t <_c u /\ INFINITE u ==> s *_c t <_c u`,
1109   REPEAT GEN_TAC THEN ASM_CASES_TAC `FINITE(t:B->bool)` THENL
1110    [REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1111     ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
1112     REWRITE_TAC[CARD_NOT_LT; INFINITE] THEN
1113     ASM_MESON_TAC[CARD_LE_FINITE; CARD_MUL_FINITE];
1114     ASM_MESON_TAC[INFINITE; CARD_MUL_ABSORB_LE; CARD_LET_TRANS]]);;
1115
1116 let CARD_MUL_LT_INFINITE = prove
1117  (`!s:A->bool t:B->bool u. s <_c u /\ t <_c u /\ INFINITE u ==> s *_c t <_c u`,
1118   REPEAT GEN_TAC THEN
1119   DISJ_CASES_TAC(ISPECL [`s:A->bool`; `t:B->bool`] CARD_LE_TOTAL) THENL
1120    [ASM_MESON_TAC[CARD_MUL_SYM; CARD_MUL_LT_LEMMA];
1121     STRIP_TAC THEN TRANS_TAC CARD_LET_TRANS `t:B->bool *_c s:A->bool` THEN
1122     ASM_MESON_TAC[CARD_EQ_IMP_LE; CARD_MUL_SYM; CARD_MUL_LT_LEMMA]]);;
1123
1124 (* ------------------------------------------------------------------------- *)
1125 (* Cantor's theorem.                                                         *)
1126 (* ------------------------------------------------------------------------- *)
1127
1128 let CANTOR_THM = prove
1129  (`!s:A->bool. s <_c {t | t SUBSET s}`,
1130   GEN_TAC THEN REWRITE_TAC[lt_c] THEN CONJ_TAC THENL
1131    [REWRITE_TAC[le_c] THEN EXISTS_TAC `(=):A->A->bool` THEN
1132     REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM; SUBSET; IN] THEN MESON_TAC[];
1133     REWRITE_TAC[LE_C; IN_ELIM_THM; SURJECTIVE_RIGHT_INVERSE] THEN
1134     REWRITE_TAC[NOT_EXISTS_THM] THEN X_GEN_TAC `g:A->(A->bool)` THEN
1135     DISCH_THEN(MP_TAC o SPEC `\x:A. s(x) /\ ~(g x x)`) THEN
1136     REWRITE_TAC[SUBSET; IN; FUN_EQ_THM] THEN MESON_TAC[]]);;
1137
1138 let CANTOR_THM_UNIV = prove
1139  (`(UNIV:A->bool) <_c (UNIV:(A->bool)->bool)`,
1140   MP_TAC(ISPEC `UNIV:A->bool` CANTOR_THM) THEN
1141   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
1142   REWRITE_TAC[EXTENSION; SUBSET; IN_UNIV; IN_ELIM_THM]);;
1143
1144 (* ------------------------------------------------------------------------- *)
1145 (* Lemmas about countability.                                                *)
1146 (* ------------------------------------------------------------------------- *)
1147
1148 let NUM_COUNTABLE = prove
1149  (`COUNTABLE(:num)`,
1150   REWRITE_TAC[COUNTABLE; ge_c; CARD_LE_REFL]);;
1151
1152 let COUNTABLE_ALT = prove
1153  (`!s. COUNTABLE s <=> s <=_c (:num)`,
1154   REWRITE_TAC[COUNTABLE; ge_c]);;
1155
1156 let COUNTABLE_CASES = prove
1157  (`!s. COUNTABLE s <=> FINITE s \/ s =_c (:num)`,
1158   REWRITE_TAC[COUNTABLE_ALT; FINITE_CARD_LT; CARD_LE_LT]);;
1159
1160 let CARD_LE_COUNTABLE = prove
1161  (`!s t:A->bool. COUNTABLE t /\ s <=_c t ==> COUNTABLE s`,
1162   REWRITE_TAC[COUNTABLE; ge_c] THEN REPEAT STRIP_TAC THEN
1163   TRANS_TAC CARD_LE_TRANS `t:A->bool` THEN ASM_REWRITE_TAC[]);;
1164
1165 let CARD_EQ_COUNTABLE = prove
1166  (`!s t:A->bool. COUNTABLE t /\ s =_c t ==> COUNTABLE s`,
1167   REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN MESON_TAC[CARD_LE_COUNTABLE]);;
1168
1169 let CARD_COUNTABLE_CONG = prove
1170  (`!s t. s =_c t ==> (COUNTABLE s <=> COUNTABLE t)`,
1171   REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN MESON_TAC[CARD_LE_COUNTABLE]);;
1172
1173 let COUNTABLE_SUBSET = prove
1174  (`!s t:A->bool. COUNTABLE t /\ s SUBSET t ==> COUNTABLE s`,
1175   REWRITE_TAC[COUNTABLE; ge_c] THEN REPEAT STRIP_TAC THEN
1176   TRANS_TAC CARD_LE_TRANS `t:A->bool` THEN
1177   ASM_SIMP_TAC[CARD_LE_SUBSET]);;
1178
1179 let COUNTABLE_RESTRICT = prove
1180  (`!s P. COUNTABLE s ==> COUNTABLE {x | x IN s /\ P x}`,
1181   REPEAT GEN_TAC THEN
1182   MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] COUNTABLE_SUBSET) THEN
1183   SET_TAC[]);;
1184
1185 let COUNTABLE_SUBSET_NUM = prove
1186  (`!s:num->bool. COUNTABLE s`,
1187   MESON_TAC[NUM_COUNTABLE; COUNTABLE_SUBSET; SUBSET_UNIV]);;
1188
1189 let FINITE_IMP_COUNTABLE = prove
1190  (`!s. FINITE s ==> COUNTABLE s`,
1191   SIMP_TAC[FINITE_CARD_LT; lt_c; COUNTABLE; ge_c]);;
1192
1193 let COUNTABLE_IMAGE = prove
1194  (`!f:A->B s. COUNTABLE s ==> COUNTABLE (IMAGE f s)`,
1195   REWRITE_TAC[COUNTABLE; ge_c] THEN REPEAT STRIP_TAC THEN
1196   TRANS_TAC CARD_LE_TRANS `s:A->bool` THEN
1197   ASM_SIMP_TAC[CARD_LE_IMAGE]);;
1198
1199 let COUNTABLE_IMAGE_INJ_GENERAL = prove
1200  (`!(f:A->B) A s.
1201         (!x y. x IN s /\ y IN s /\ f(x) = f(y) ==> x = y) /\
1202         COUNTABLE A
1203         ==> COUNTABLE {x | x IN s /\ f(x) IN A}`,
1204   REPEAT STRIP_TAC THEN
1205   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INJECTIVE_ON_LEFT_INVERSE]) THEN
1206   DISCH_THEN(X_CHOOSE_TAC `g:B->A`) THEN
1207   MATCH_MP_TAC COUNTABLE_SUBSET THEN EXISTS_TAC `IMAGE (g:B->A) A` THEN
1208   ASM_SIMP_TAC[COUNTABLE_IMAGE] THEN ASM SET_TAC[]);;
1209
1210 let COUNTABLE_IMAGE_INJ_EQ = prove
1211  (`!(f:A->B) s.
1212         (!x y. x IN s /\ y IN s /\ (f(x) = f(y)) ==> (x = y))
1213         ==> (COUNTABLE(IMAGE f s) <=> COUNTABLE s)`,
1214   REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC[COUNTABLE_IMAGE] THEN
1215   POP_ASSUM MP_TAC THEN REWRITE_TAC[IMP_IMP] THEN
1216   DISCH_THEN(MP_TAC o MATCH_MP COUNTABLE_IMAGE_INJ_GENERAL) THEN
1217   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN SET_TAC[]);;
1218
1219 let COUNTABLE_IMAGE_INJ = prove
1220  (`!(f:A->B) A.
1221         (!x y. (f(x) = f(y)) ==> (x = y)) /\
1222          COUNTABLE A
1223          ==> COUNTABLE {x | f(x) IN A}`,
1224   REPEAT GEN_TAC THEN
1225   MP_TAC(SPECL [`f:A->B`; `A:B->bool`; `UNIV:A->bool`]
1226     COUNTABLE_IMAGE_INJ_GENERAL) THEN REWRITE_TAC[IN_UNIV]);;
1227
1228 let COUNTABLE_EMPTY = prove
1229  (`COUNTABLE {}`,
1230   SIMP_TAC[FINITE_IMP_COUNTABLE; FINITE_RULES]);;
1231
1232 let COUNTABLE_INTER = prove
1233  (`!s t. COUNTABLE s \/ COUNTABLE t ==> COUNTABLE (s INTER t)`,
1234   REWRITE_TAC[TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`] THEN
1235   REPEAT GEN_TAC THEN CONJ_TAC THEN
1236   MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] COUNTABLE_SUBSET) THEN
1237   SET_TAC[]);;
1238
1239 let COUNTABLE_UNION_IMP = prove
1240  (`!s t:A->bool. COUNTABLE s /\ COUNTABLE t ==> COUNTABLE(s UNION t)`,
1241   REWRITE_TAC[COUNTABLE; ge_c] THEN REPEAT STRIP_TAC THEN
1242   TRANS_TAC CARD_LE_TRANS `(s:A->bool) +_c (t:A->bool)` THEN
1243   ASM_SIMP_TAC[CARD_ADD2_ABSORB_LE; num_INFINITE; UNION_LE_ADD_C]);;
1244
1245 let COUNTABLE_UNION = prove
1246  (`!s t:A->bool. COUNTABLE(s UNION t) <=> COUNTABLE s /\ COUNTABLE t`,
1247   REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[COUNTABLE_UNION_IMP] THEN
1248   DISCH_THEN(fun th -> CONJ_TAC THEN MP_TAC th) THEN
1249   MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] COUNTABLE_SUBSET) THEN
1250   SET_TAC[]);;
1251
1252 let COUNTABLE_SING = prove
1253  (`!x. COUNTABLE {x}`,
1254   SIMP_TAC[FINITE_IMP_COUNTABLE; FINITE_SING]);;
1255
1256 let COUNTABLE_INSERT = prove
1257  (`!x s. COUNTABLE(x INSERT s) <=> COUNTABLE s`,
1258   ONCE_REWRITE_TAC[SET_RULE `x INSERT s = {x} UNION s`] THEN
1259   REWRITE_TAC[COUNTABLE_UNION; COUNTABLE_SING]);;
1260
1261 let COUNTABLE_DELETE = prove
1262  (`!x:A s. COUNTABLE(s DELETE x) <=> COUNTABLE s`,
1263   REPEAT GEN_TAC THEN ASM_CASES_TAC `(x:A) IN s` THEN
1264   ASM_SIMP_TAC[SET_RULE `~(x IN s) ==> s DELETE x = s`] THEN
1265   MATCH_MP_TAC EQ_TRANS THEN
1266   EXISTS_TAC `COUNTABLE((x:A) INSERT (s DELETE x))` THEN CONJ_TAC THENL
1267    [REWRITE_TAC[COUNTABLE_INSERT]; AP_TERM_TAC THEN ASM SET_TAC[]]);;
1268
1269 let COUNTABLE_DIFF_FINITE = prove
1270  (`!s t. FINITE s ==> (COUNTABLE(t DIFF s) <=> COUNTABLE t)`,
1271   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
1272   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1273   SIMP_TAC[DIFF_EMPTY; SET_RULE `s DIFF (x INSERT t) = (s DIFF t) DELETE x`;
1274            COUNTABLE_DELETE]);;
1275
1276 let COUNTABLE_CROSS = prove
1277  (`!s t. COUNTABLE s /\ COUNTABLE t ==> COUNTABLE(s CROSS t)`,
1278   REWRITE_TAC[COUNTABLE; ge_c; CROSS; GSYM mul_c] THEN
1279   SIMP_TAC[CARD_MUL2_ABSORB_LE; num_INFINITE]);;
1280
1281 let COUNTABLE_AS_IMAGE_SUBSET = prove
1282  (`!s. COUNTABLE s ==> ?f. s SUBSET (IMAGE f (:num))`,
1283   REWRITE_TAC[COUNTABLE; ge_c; LE_C; SUBSET; IN_IMAGE] THEN MESON_TAC[]);;
1284
1285 let COUNTABLE_AS_IMAGE_SUBSET_EQ = prove
1286  (`!s:A->bool. COUNTABLE s <=> ?f. s SUBSET (IMAGE f (:num))`,
1287   REWRITE_TAC[COUNTABLE; ge_c; LE_C; SUBSET; IN_IMAGE] THEN MESON_TAC[]);;
1288
1289 let COUNTABLE_AS_IMAGE = prove
1290  (`!s:A->bool. COUNTABLE s /\ ~(s = {}) ==> ?f. s = IMAGE f (:num)`,
1291   REPEAT STRIP_TAC THEN FIRST_X_ASSUM(X_CHOOSE_TAC `a:A` o
1292     GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
1293   FIRST_X_ASSUM(MP_TAC o MATCH_MP COUNTABLE_AS_IMAGE_SUBSET) THEN
1294   DISCH_THEN(X_CHOOSE_TAC `f:num->A`) THEN
1295   EXISTS_TAC `\n. if (f:num->A) n IN s then f n else a` THEN
1296   ASM SET_TAC[]);;
1297
1298 let FORALL_COUNTABLE_AS_IMAGE = prove
1299  (`(!d. COUNTABLE d ==> P d) <=> P {} /\ (!f. P(IMAGE f (:num)))`,
1300   MESON_TAC[COUNTABLE_AS_IMAGE; COUNTABLE_IMAGE; NUM_COUNTABLE;
1301             COUNTABLE_EMPTY]);;
1302
1303 let COUNTABLE_AS_INJECTIVE_IMAGE = prove
1304  (`!s. COUNTABLE s /\ INFINITE s
1305        ==> ?f. s = IMAGE f (:num) /\ (!m n. f(m) = f(n) ==> m = n)`,
1306   GEN_TAC THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN
1307   REWRITE_TAC[INFINITE_CARD_LE; COUNTABLE; ge_c] THEN
1308   REWRITE_TAC[CARD_LE_ANTISYM; eq_c] THEN
1309   MATCH_MP_TAC MONO_EXISTS THEN SET_TAC[]);;
1310
1311 let COUNTABLE_UNIONS = prove
1312  (`!A:(A->bool)->bool.
1313         COUNTABLE A /\ (!s. s IN A ==> COUNTABLE s)
1314         ==> COUNTABLE (UNIONS A)`,
1315   GEN_TAC THEN
1316   GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV)
1317    [COUNTABLE_AS_IMAGE_SUBSET_EQ] THEN
1318   DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `f:num->A->bool`) MP_TAC) THEN
1319   GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV) [RIGHT_IMP_EXISTS_THM] THEN
1320   REWRITE_TAC[SKOLEM_THM] THEN
1321   DISCH_THEN(X_CHOOSE_TAC `g:(A->bool)->num->A`) THEN
1322   MATCH_MP_TAC COUNTABLE_SUBSET THEN
1323   EXISTS_TAC `IMAGE (\(m,n). (g:(A->bool)->num->A) ((f:num->A->bool) m) n)
1324                     ((:num) CROSS (:num))` THEN
1325   ASM_SIMP_TAC[COUNTABLE_IMAGE; COUNTABLE_CROSS; NUM_COUNTABLE] THEN
1326   REWRITE_TAC[SUBSET; FORALL_IN_UNIONS] THEN
1327   REWRITE_TAC[IN_IMAGE; EXISTS_PAIR_THM; IN_CROSS; IN_UNIV] THEN
1328   ASM SET_TAC[]);;
1329
1330 let COUNTABLE_PRODUCT_DEPENDENT = prove
1331  (`!f:A->B->C s t.
1332         COUNTABLE s /\ (!x. x IN s ==> COUNTABLE(t x))
1333         ==> COUNTABLE {f x y | x IN s /\ y IN (t x)}`,
1334   REPEAT GEN_TAC THEN DISCH_TAC THEN
1335   SUBGOAL_THEN `{(f:A->B->C) x y | x IN s /\ y IN (t x)} =
1336                 IMAGE (\(x,y). f x y) {(x,y) | x IN s /\ y IN (t x)}`
1337   SUBST1_TAC THENL
1338    [REWRITE_TAC[EXTENSION; IN_IMAGE; EXISTS_PAIR_THM; IN_ELIM_PAIR_THM] THEN
1339     SET_TAC[];
1340     MATCH_MP_TAC COUNTABLE_IMAGE THEN POP_ASSUM MP_TAC] THEN
1341   GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV)
1342    [COUNTABLE_AS_IMAGE_SUBSET_EQ] THEN
1343   DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `f:num->A`) MP_TAC) THEN
1344   GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV) [RIGHT_IMP_EXISTS_THM] THEN
1345   REWRITE_TAC[SKOLEM_THM] THEN
1346   DISCH_THEN(X_CHOOSE_TAC `g:A->num->B`) THEN
1347   MATCH_MP_TAC COUNTABLE_SUBSET THEN
1348   EXISTS_TAC `IMAGE (\(m,n). (f:num->A) m,(g:A->num->B)(f m) n)
1349                     ((:num) CROSS (:num))` THEN
1350   ASM_SIMP_TAC[COUNTABLE_IMAGE; COUNTABLE_CROSS; NUM_COUNTABLE] THEN
1351   REWRITE_TAC[SUBSET; FORALL_IN_UNIONS] THEN
1352   REWRITE_TAC[IN_IMAGE; FORALL_PAIR_THM; IN_ELIM_PAIR_THM;
1353               EXISTS_PAIR_THM; IN_CROSS; IN_UNIV] THEN
1354   ASM SET_TAC[]);;
1355
1356 let COUNTABLE_CARD_MUL = prove
1357  (`!s:A->bool t:B->bool. COUNTABLE s /\ COUNTABLE t ==> COUNTABLE(s *_c t)`,
1358   REPEAT STRIP_TAC THEN REWRITE_TAC[mul_c] THEN
1359   ASM_SIMP_TAC[COUNTABLE_PRODUCT_DEPENDENT]);;
1360
1361 let COUNTABLE_CARD_MUL_EQ = prove
1362  (`!s:A->bool t:B->bool.
1363         COUNTABLE(s *_c t) <=> s = {} \/ t = {} \/ COUNTABLE s /\ COUNTABLE t`,
1364   REPEAT GEN_TAC THEN REWRITE_TAC[mul_c] THEN
1365   MAP_EVERY ASM_CASES_TAC [`s:A->bool = {}`; `t:B->bool = {}`] THEN
1366   ASM_REWRITE_TAC[COUNTABLE_EMPTY; EMPTY_GSPEC; NOT_IN_EMPTY;
1367                   SET_RULE `{x,y | F} = {}`] THEN
1368   EQ_TAC THEN SIMP_TAC[REWRITE_RULE[mul_c] COUNTABLE_CARD_MUL] THEN
1369   REPEAT STRIP_TAC THEN MATCH_MP_TAC COUNTABLE_SUBSET THENL
1370    [EXISTS_TAC `IMAGE FST ((s:A->bool) *_c (t:B->bool))`;
1371     EXISTS_TAC `IMAGE SND ((s:A->bool) *_c (t:B->bool))`] THEN
1372   ASM_SIMP_TAC[COUNTABLE_IMAGE; mul_c; SUBSET; IN_IMAGE; EXISTS_PAIR_THM] THEN
1373   REWRITE_TAC[IN_ELIM_PAIR_THM] THEN ASM SET_TAC[]);;
1374
1375 let CARD_EQ_PCROSS = prove
1376  (`!s:A^M->bool t:A^N->bool. s PCROSS t =_c s *_c t`,
1377   REPEAT GEN_TAC THEN REWRITE_TAC[EQ_C_BIJECTIONS; mul_c] THEN
1378   EXISTS_TAC `\z:A^(M,N)finite_sum. fstcart z,sndcart z` THEN
1379   EXISTS_TAC `\(x:A^M,y:A^N). pastecart x y` THEN
1380   REWRITE_TAC[FORALL_IN_GSPEC; PASTECART_IN_PCROSS] THEN
1381   REWRITE_TAC[IN_ELIM_PAIR_THM; PASTECART_FST_SND] THEN
1382   REWRITE_TAC[FORALL_IN_PCROSS; FSTCART_PASTECART; SNDCART_PASTECART]);;
1383
1384 let COUNTABLE_PCROSS_EQ = prove
1385  (`!s:A^M->bool t:A^N->bool.
1386         COUNTABLE(s PCROSS t) <=>
1387         s = {} \/ t = {} \/ COUNTABLE s /\ COUNTABLE t`,
1388   REPEAT GEN_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
1389   EXISTS_TAC `COUNTABLE((s:A^M->bool) *_c (t:A^N->bool))` THEN CONJ_TAC THENL
1390    [MATCH_MP_TAC CARD_COUNTABLE_CONG THEN REWRITE_TAC[CARD_EQ_PCROSS];
1391     REWRITE_TAC[COUNTABLE_CARD_MUL_EQ]]);;
1392
1393 let COUNTABLE_PCROSS = prove
1394  (`!s:A^M->bool t:A^N->bool.
1395         COUNTABLE s /\ COUNTABLE t ==> COUNTABLE(s PCROSS t)`,
1396   SIMP_TAC[COUNTABLE_PCROSS_EQ]);;
1397
1398 let COUNTABLE_CART = prove
1399  (`!P. (!i. 1 <= i /\ i <= dimindex(:N) ==> COUNTABLE {x | P i x})
1400        ==> COUNTABLE {v:A^N | !i. 1 <= i /\ i <= dimindex(:N) ==> P i (v$i)}`,
1401   GEN_TAC THEN DISCH_TAC THEN
1402   SUBGOAL_THEN
1403    `!n. n <= dimindex(:N)
1404         ==> COUNTABLE {v:A^N | (!i. 1 <= i /\ i <= dimindex(:N) /\ i <= n
1405                                  ==> P i (v$i)) /\
1406                             (!i. 1 <= i /\ i <= dimindex(:N) /\ n < i
1407                                  ==> v$i = @x. F)}`
1408    (MP_TAC o SPEC `dimindex(:N)`) THEN REWRITE_TAC[LE_REFL; LET_ANTISYM] THEN
1409   INDUCT_TAC THENL
1410    [REWRITE_TAC[ARITH_RULE `1 <= i /\ i <= n /\ i <= 0 <=> F`] THEN
1411     SIMP_TAC[ARITH_RULE `1 <= i /\ i <= n /\ 0 < i <=> 1 <= i /\ i <= n`] THEN
1412     SUBGOAL_THEN
1413      `{v | !i. 1 <= i /\ i <= dimindex (:N) ==> v$i = (@x. F)} =
1414       {(lambda i. @x. F):A^N}`
1415      (fun th -> SIMP_TAC[COUNTABLE_SING;th]) THEN
1416     SIMP_TAC[EXTENSION; IN_SING; IN_ELIM_THM; CART_EQ; LAMBDA_BETA];
1417     ALL_TAC] THEN
1418   DISCH_TAC THEN
1419   MATCH_MP_TAC COUNTABLE_SUBSET THEN EXISTS_TAC
1420    `IMAGE (\(x:A,v:A^N). (lambda i. if i = SUC n then x else v$i):A^N)
1421           {x,v | x IN {x:A | P (SUC n) x} /\
1422                  v IN {v:A^N | (!i. 1 <= i /\ i <= dimindex(:N) /\ i <= n
1423                                 ==> P i (v$i)) /\
1424                            (!i. 1 <= i /\ i <= dimindex (:N) /\ n < i
1425                                 ==> v$i = (@x. F))}}` THEN
1426   CONJ_TAC THENL
1427    [MATCH_MP_TAC COUNTABLE_IMAGE THEN
1428     ASM_SIMP_TAC[REWRITE_RULE[CROSS] COUNTABLE_CROSS; ARITH_RULE `1 <= SUC n`;
1429                  ARITH_RULE `SUC n <= m ==> n <= m`];
1430     ALL_TAC] THEN
1431   REWRITE_TAC[SUBSET; IN_IMAGE; IN_ELIM_PAIR_THM; EXISTS_PAIR_THM] THEN
1432   X_GEN_TAC `v:A^N` THEN REWRITE_TAC[IN_ELIM_THM] THEN
1433   STRIP_TAC THEN EXISTS_TAC `(v:A^N)$(SUC n)` THEN
1434   EXISTS_TAC `(lambda i. if i = SUC n then @x. F else (v:A^N)$i):A^N` THEN
1435   SIMP_TAC[CART_EQ; LAMBDA_BETA; ARITH_RULE `i <= n ==> ~(i = SUC n)`] THEN
1436   ASM_MESON_TAC[LE; ARITH_RULE `1 <= SUC n`;
1437                 ARITH_RULE `n < i /\ ~(i = SUC n) ==> SUC n < i`]);;
1438
1439 let COUNTABLE_SUBSET_IMAGE = prove
1440  (`!f:A->B s t.
1441         COUNTABLE(t) /\ t SUBSET (IMAGE f s) <=>
1442         ?s'. COUNTABLE s' /\ s' SUBSET s /\ (t = IMAGE f s')`,
1443   REPEAT GEN_TAC THEN EQ_TAC THENL
1444    [ALL_TAC; ASM_MESON_TAC[COUNTABLE_IMAGE; IMAGE_SUBSET]] THEN
1445   STRIP_TAC THEN
1446   EXISTS_TAC `IMAGE (\y. @x. x IN s /\ ((f:A->B)(x) = y)) t` THEN
1447   ASM_SIMP_TAC[COUNTABLE_IMAGE] THEN
1448   REWRITE_TAC[EXTENSION; SUBSET; FORALL_IN_IMAGE] THEN CONJ_TAC THENL
1449    [ASM_MESON_TAC[SUBSET; IN_IMAGE]; ALL_TAC] THEN
1450   REWRITE_TAC[IN_IMAGE] THEN X_GEN_TAC `y:B` THEN
1451   REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN
1452   ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN
1453   REWRITE_TAC[UNWIND_THM2; GSYM CONJ_ASSOC] THEN
1454   ASM_MESON_TAC[SUBSET; IN_IMAGE]);;
1455
1456 let EXISTS_COUNTABLE_SUBSET_IMAGE = prove
1457  (`!P f s.
1458     (?t. COUNTABLE t /\ t SUBSET IMAGE f s /\ P t) <=>
1459     (?t. COUNTABLE t /\ t SUBSET s /\ P (IMAGE f t))`,
1460   REWRITE_TAC[COUNTABLE_SUBSET_IMAGE; CONJ_ASSOC] THEN MESON_TAC[]);;
1461
1462 let FORALL_COUNTABLE_SUBSET_IMAGE = prove
1463  (`!P f s. (!t. COUNTABLE t /\ t SUBSET IMAGE f s ==> P t) <=>
1464            (!t. COUNTABLE t /\ t SUBSET s ==> P(IMAGE f t))`,
1465   REPEAT GEN_TAC THEN
1466   ONCE_REWRITE_TAC[MESON[] `(!x. P x) <=> ~(?x. ~P x)`] THEN
1467   REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC; EXISTS_COUNTABLE_SUBSET_IMAGE]);;
1468
1469 (* ------------------------------------------------------------------------- *)
1470 (* Cardinality of infinite list and cartesian product types.                 *)
1471 (* ------------------------------------------------------------------------- *)
1472
1473 let CARD_EQ_LIST_GEN = prove
1474  (`!s:A->bool. INFINITE(s) ==> {l | !x. MEM x l ==> x IN s} =_c s`,
1475   GEN_TAC THEN DISCH_TAC THEN
1476   REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN CONJ_TAC THENL
1477    [ALL_TAC;
1478     REWRITE_TAC[le_c; IN_UNIV] THEN
1479     EXISTS_TAC `\x:A. [x]` THEN SIMP_TAC[CONS_11; IN_ELIM_THM; MEM]] THEN
1480   TRANS_TAC CARD_LE_TRANS `(:num) *_c (s:A->bool)` THEN CONJ_TAC THENL
1481    [ALL_TAC;
1482     MATCH_MP_TAC CARD_MUL2_ABSORB_LE THEN
1483     ASM_REWRITE_TAC[GSYM INFINITE_CARD_LE; CARD_LE_REFL]] THEN
1484   SUBGOAL_THEN `s *_c s <=_c (s:A->bool)` MP_TAC THENL
1485    [MATCH_MP_TAC CARD_MUL2_ABSORB_LE THEN ASM_REWRITE_TAC[CARD_LE_REFL];
1486     ALL_TAC] THEN
1487   REWRITE_TAC[le_c; mul_c; FORALL_PAIR_THM; IN_ELIM_PAIR_THM; PAIR_EQ] THEN
1488   REWRITE_TAC[IN_UNIV; LEFT_IMP_EXISTS_THM] THEN
1489   GEN_REWRITE_TAC I [FORALL_CURRY] THEN
1490   X_GEN_TAC `pair:A->A->A` THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
1491   SUBGOAL_THEN `?b:A. b IN s` CHOOSE_TAC THENL
1492    [ASM_MESON_TAC[INFINITE; FINITE_EMPTY; MEMBER_NOT_EMPTY]; ALL_TAC] THEN
1493   EXISTS_TAC `\l. LENGTH l,ITLIST (pair:A->A->A) l b` THEN
1494   REWRITE_TAC[PAIR_EQ; RIGHT_EXISTS_AND_THM; GSYM EXISTS_REFL] THEN
1495   SUBGOAL_THEN
1496    `!l:A list. (!x. MEM x l ==> x IN s) ==> (ITLIST pair l b) IN s`
1497   ASSUME_TAC THENL
1498    [LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[MEM; ITLIST] THEN ASM_MESON_TAC[];
1499     CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC]] THEN
1500   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
1501   LIST_INDUCT_TAC THEN SIMP_TAC[LENGTH_EQ_NIL; LENGTH] THEN
1502   LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; NOT_SUC] THEN
1503   REWRITE_TAC[ITLIST; SUC_INJ; MEM; CONS_11] THEN
1504   REPEAT STRIP_TAC THENL [ALL_TAC; FIRST_X_ASSUM MATCH_MP_TAC] THEN
1505   ASM_MESON_TAC[]);;
1506
1507 let CARD_EQ_LIST = prove
1508  (`INFINITE(:A) ==> (:A list) =_c (:A)`,
1509   DISCH_THEN(MP_TAC o MATCH_MP CARD_EQ_LIST_GEN) THEN
1510   REWRITE_TAC[IN_UNIV; SET_RULE `{x | T} = UNIV`]);;
1511
1512 let CARD_EQ_CART = prove
1513  (`INFINITE(:A) ==> (:A^N) =_c (:A)`,
1514   DISCH_TAC THEN REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN CONJ_TAC THENL
1515    [ALL_TAC;
1516     REWRITE_TAC[le_c; IN_UNIV] THEN
1517     EXISTS_TAC `(\x. lambda i. x):A->A^N` THEN
1518     SIMP_TAC[CART_EQ; LAMBDA_BETA] THEN
1519     MESON_TAC[LE_REFL; DIMINDEX_GE_1]] THEN
1520   TRANS_TAC CARD_LE_TRANS `(:A list)` THEN
1521   ASM_SIMP_TAC[CARD_EQ_LIST; CARD_EQ_IMP_LE] THEN REWRITE_TAC[LE_C] THEN
1522   EXISTS_TAC `(\l. lambda i. EL i l):(A)list->A^N` THEN
1523   ASM_SIMP_TAC[CART_EQ; IN_UNIV; LAMBDA_BETA] THEN X_GEN_TAC `x:A^N` THEN
1524   SUBGOAL_THEN `!n f. ?l. !i. i < n ==> EL i l:A = f i` MP_TAC THENL
1525    [INDUCT_TAC THEN REWRITE_TAC[CONJUNCT1 LT] THEN X_GEN_TAC `f:num->A` THEN
1526     FIRST_X_ASSUM(MP_TAC o SPEC `\i. (f:num->A)(SUC i)`) THEN
1527     REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `l:A list` THEN
1528     DISCH_TAC THEN EXISTS_TAC `CONS ((f:num->A) 0) l` THEN
1529     INDUCT_TAC THEN ASM_SIMP_TAC[EL; HD; TL; LT_SUC];
1530     DISCH_THEN(MP_TAC o SPECL [`dimindex(:N)+1`; `\i. (x:A^N)$i`]) THEN
1531     REWRITE_TAC[LEFT_IMP_EXISTS_THM; ARITH_RULE `i < n + 1 <=> i <= n`] THEN
1532     MESON_TAC[]]);;
1533
1534 (* ------------------------------------------------------------------------- *)
1535 (* Cardinality of the reals. This is done in a rather laborious way to avoid *)
1536 (* any dependence on the theories of analysis.                               *)
1537 (* ------------------------------------------------------------------------- *)
1538
1539 let CARD_EQ_REAL = prove
1540  (`(:real) =_c (:num->bool)`,
1541   let lemma = prove
1542    (`!s m n. sum (s INTER (m..n)) (\i. inv(&3 pow i)) < &3 / &2 / &3 pow m`,
1543     REPEAT GEN_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
1544     EXISTS_TAC `sum (m..n) (\i. inv(&3 pow i))` THEN CONJ_TAC THENL
1545      [MATCH_MP_TAC SUM_SUBSET_SIMPLE THEN
1546       SIMP_TAC[FINITE_NUMSEG; INTER_SUBSET; REAL_LE_INV_EQ;
1547                REAL_POW_LE; REAL_POS];
1548       WF_INDUCT_TAC `n - m:num` THEN
1549       ASM_CASES_TAC `m:num <= n` THENL
1550        [ASM_SIMP_TAC[SUM_CLAUSES_LEFT] THEN ASM_CASES_TAC `m + 1 <= n` THENL
1551          [FIRST_X_ASSUM(MP_TAC o SPECL [`n:num`; `SUC m`]) THEN
1552           ANTS_TAC THENL [ASM_ARITH_TAC; REWRITE_TAC[ADD1; REAL_POW_ADD]] THEN
1553           MATCH_MP_TAC(REAL_ARITH
1554            `a + j:real <= k ==> x < j ==> a + x < k`) THEN
1555           REWRITE_TAC[real_div; REAL_INV_MUL; REAL_POW_1] THEN REAL_ARITH_TAC;
1556           ALL_TAC];
1557         ALL_TAC] THEN
1558       RULE_ASSUM_TAC(REWRITE_RULE[NOT_LE; GSYM NUMSEG_EMPTY]) THEN
1559       ASM_REWRITE_TAC[SUM_CLAUSES; REAL_ADD_RID] THEN
1560       REWRITE_TAC[REAL_ARITH `inv x < &3 / &2 / x <=> &0 < inv x`] THEN
1561       SIMP_TAC[REAL_LT_INV_EQ; REAL_LT_DIV; REAL_POW_LT; REAL_OF_NUM_LT;
1562                ARITH]]) in
1563   REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN CONJ_TAC THENL
1564    [TRANS_TAC CARD_LE_TRANS `(:num) *_c (:num->bool)` THEN CONJ_TAC THENL
1565      [ALL_TAC;
1566       MATCH_MP_TAC CARD_MUL2_ABSORB_LE THEN REWRITE_TAC[INFINITE_CARD_LE] THEN
1567       SIMP_TAC[CANTOR_THM_UNIV; CARD_LT_IMP_LE; CARD_LE_REFL]] THEN
1568     TRANS_TAC CARD_LE_TRANS `(:num) *_c {x:real | &0 <= x}` THEN CONJ_TAC THENL
1569      [REWRITE_TAC[LE_C; mul_c; EXISTS_PAIR_THM; IN_ELIM_PAIR_THM; IN_UNIV] THEN
1570       EXISTS_TAC `\(n,x:real). --(&1) pow n * x` THEN X_GEN_TAC `x:real` THEN
1571       MATCH_MP_TAC(MESON[] `P 0 \/ P 1 ==> ?n. P n`) THEN
1572       REWRITE_TAC[OR_EXISTS_THM] THEN EXISTS_TAC `abs x` THEN
1573       REWRITE_TAC[IN_ELIM_THM] THEN REAL_ARITH_TAC;
1574       ALL_TAC] THEN
1575     MATCH_MP_TAC CARD_LE_MUL THEN REWRITE_TAC[CARD_LE_REFL] THEN
1576     MP_TAC(ISPECL [`(:num)`; `(:num)`] CARD_MUL_ABSORB_LE) THEN
1577     REWRITE_TAC[CARD_LE_REFL; num_INFINITE] THEN
1578     REWRITE_TAC[le_c; mul_c; IN_UNIV; FORALL_PAIR_THM; IN_ELIM_PAIR_THM] THEN
1579     REWRITE_TAC[GSYM FORALL_PAIR_THM; INJECTIVE_LEFT_INVERSE] THEN
1580     REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
1581     MAP_EVERY X_GEN_TAC [`pair:num#num->num`; `unpair:num->num#num`] THEN
1582     DISCH_TAC THEN
1583     EXISTS_TAC `\x:real n:num. &(FST(unpair n)) * x <= &(SND(unpair n))` THEN
1584     MATCH_MP_TAC REAL_WLOG_LT THEN REWRITE_TAC[IN_ELIM_THM; FUN_EQ_THM] THEN
1585     CONJ_TAC THENL [REWRITE_TAC[EQ_SYM_EQ; CONJ_ACI]; ALL_TAC] THEN
1586     MAP_EVERY X_GEN_TAC [`x:real`; `y:real`] THEN REPEAT STRIP_TAC THEN
1587     FIRST_X_ASSUM(MP_TAC o GENL [`p:num`; `q:num`] o
1588       SPEC `(pair:num#num->num) (p,q)`) THEN
1589     ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN
1590     MP_TAC(SPEC `y - x:real` REAL_ARCH) THEN
1591     ASM_REWRITE_TAC[REAL_SUB_LT; NOT_FORALL_THM] THEN
1592     DISCH_THEN(MP_TAC o SPEC `&2`) THEN MATCH_MP_TAC MONO_EXISTS THEN
1593     X_GEN_TAC `p:num` THEN DISCH_TAC THEN
1594     MP_TAC(ISPEC `&p * x:real` REAL_ARCH_LT) THEN
1595     GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN MATCH_MP_TAC MONO_EXISTS THEN
1596     MATCH_MP_TAC num_INDUCTION THEN
1597     ASM_SIMP_TAC[REAL_LE_MUL; REAL_POS;
1598       REAL_ARITH `x:real < &0 <=> ~(&0 <= x)`] THEN
1599     X_GEN_TAC `q:num` THEN REWRITE_TAC[GSYM REAL_OF_NUM_SUC] THEN
1600     DISCH_THEN(K ALL_TAC) THEN STRIP_TAC THEN
1601     FIRST_X_ASSUM(MP_TAC o SPEC `q:num`) THEN
1602     REWRITE_TAC[LT] THEN ASM_REAL_ARITH_TAC;
1603     REWRITE_TAC[le_c; IN_UNIV] THEN
1604     EXISTS_TAC `\s:num->bool. sup { sum (s INTER (0..n)) (\i. inv(&3 pow i)) |
1605                                     n IN (:num) }` THEN
1606     MAP_EVERY X_GEN_TAC [`x:num->bool`; `y:num->bool`] THEN
1607     ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
1608     REWRITE_TAC[EXTENSION; NOT_FORALL_THM] THEN
1609     GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN
1610     MAP_EVERY (fun w -> SPEC_TAC(w,w)) [`y:num->bool`; `x:num->bool`] THEN
1611     MATCH_MP_TAC(MESON[IN]
1612      `((!P Q n. R P Q n <=> R Q P n) /\ (!P Q. S P Q <=> S Q P)) /\
1613       (!P Q. (?n. n IN P /\ ~(n IN Q) /\ R P Q n) ==> S P Q)
1614       ==> !P Q. (?n:num. ~(n IN P <=> n IN Q) /\ R P Q n) ==> S P Q`) THEN
1615     CONJ_TAC THENL [REWRITE_TAC[EQ_SYM_EQ]; REWRITE_TAC[]] THEN
1616     MAP_EVERY X_GEN_TAC [`x:num->bool`; `y:num->bool`] THEN
1617     DISCH_THEN(X_CHOOSE_THEN `n:num` STRIP_ASSUME_TAC) THEN
1618     MATCH_MP_TAC(REAL_ARITH `!z:real. y < z /\ z <= x ==> ~(x = y)`) THEN
1619     EXISTS_TAC `sum (x INTER (0..n)) (\i. inv(&3 pow i))` THEN CONJ_TAC THENL
1620      [MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC
1621        `sum (y INTER (0..n)) (\i. inv(&3 pow i)) +
1622         &3 / &2 / &3 pow (SUC n)` THEN
1623       CONJ_TAC THENL
1624        [MATCH_MP_TAC REAL_SUP_LE THEN
1625         CONJ_TAC THENL [SET_TAC[]; REWRITE_TAC[FORALL_IN_GSPEC; IN_UNIV]] THEN
1626         X_GEN_TAC `p:num` THEN ASM_CASES_TAC `n:num <= p` THENL
1627          [MATCH_MP_TAC(REAL_ARITH
1628            `!d. s:real = t + d /\ d <= e ==> s <= t + e`) THEN
1629           EXISTS_TAC `sum(y INTER (n+1..p)) (\i. inv (&3 pow i))` THEN
1630           CONJ_TAC THENL
1631            [ONCE_REWRITE_TAC[INTER_COMM] THEN
1632             REWRITE_TAC[INTER; SUM_RESTRICT_SET] THEN
1633             ASM_SIMP_TAC[SUM_COMBINE_R; LE_0];
1634             SIMP_TAC[ADD1; lemma; REAL_LT_IMP_LE]];
1635           MATCH_MP_TAC(REAL_ARITH `y:real <= x /\ &0 <= d ==> y <= x + d`) THEN
1636           SIMP_TAC[REAL_LE_DIV; REAL_POS; REAL_POW_LE] THEN
1637           MATCH_MP_TAC SUM_SUBSET_SIMPLE THEN
1638           SIMP_TAC[REAL_LE_INV_EQ; REAL_POW_LE; REAL_POS] THEN
1639           SIMP_TAC[FINITE_INTER; FINITE_NUMSEG] THEN MATCH_MP_TAC
1640            (SET_RULE `s SUBSET t ==> u INTER s SUBSET u INTER t`) THEN
1641           REWRITE_TAC[SUBSET_NUMSEG] THEN ASM_ARITH_TAC];
1642         ONCE_REWRITE_TAC[INTER_COMM] THEN
1643         REWRITE_TAC[INTER; SUM_RESTRICT_SET] THEN ASM_CASES_TAC `n = 0` THENL
1644          [FIRST_X_ASSUM SUBST_ALL_TAC THEN
1645           ASM_REWRITE_TAC[SUM_SING; NUMSEG_SING; real_pow] THEN REAL_ARITH_TAC;
1646           ASM_SIMP_TAC[SUM_CLAUSES_RIGHT; LE_1; LE_0; REAL_ADD_RID] THEN
1647           MATCH_MP_TAC(REAL_ARITH `s:real = t /\ d < e ==> s + d < t + e`) THEN
1648           CONJ_TAC THENL
1649            [MATCH_MP_TAC SUM_EQ_NUMSEG THEN
1650             ASM_SIMP_TAC[ARITH_RULE `~(n = 0) /\ m <= n - 1 ==> m < n`];
1651             REWRITE_TAC[real_pow; real_div; REAL_INV_MUL; REAL_MUL_ASSOC] THEN
1652             CONV_TAC REAL_RAT_REDUCE_CONV THEN
1653             REWRITE_TAC[REAL_ARITH `&1 / &2 * x < x <=> &0 < x`] THEN
1654             SIMP_TAC[REAL_LT_INV_EQ; REAL_POW_LT; REAL_OF_NUM_LT; ARITH]]]];
1655       MP_TAC(ISPEC `{ sum (x INTER (0..n)) (\i. inv(&3 pow i)) | n IN (:num) }`
1656           SUP) THEN REWRITE_TAC[FORALL_IN_GSPEC; IN_UNIV] THEN
1657       ANTS_TAC THENL [ALL_TAC; SIMP_TAC[]] THEN
1658       CONJ_TAC THENL [SET_TAC[]; ALL_TAC] THEN
1659       EXISTS_TAC `&3 / &2 / &3 pow 0` THEN
1660       SIMP_TAC[lemma; REAL_LT_IMP_LE]]]);;
1661
1662 let UNCOUNTABLE_REAL = prove
1663  (`~COUNTABLE(:real)`,
1664   REWRITE_TAC[COUNTABLE; CARD_NOT_LE; ge_c] THEN
1665   TRANS_TAC CARD_LTE_TRANS `(:num->bool)` THEN
1666   REWRITE_TAC[CANTOR_THM_UNIV] THEN MATCH_MP_TAC CARD_EQ_IMP_LE THEN
1667   ONCE_REWRITE_TAC[CARD_EQ_SYM] THEN REWRITE_TAC[CARD_EQ_REAL]);;
1668
1669 let CARD_EQ_REAL_IMP_UNCOUNTABLE = prove
1670  (`!(s : A -> bool). s =_c (:real) ==> ~COUNTABLE s`,
1671   GEN_TAC THEN STRIP_TAC THEN
1672   DISCH_THEN(MP_TAC o ISPEC `(:real)` o MATCH_MP
1673     (REWRITE_RULE[IMP_CONJ] CARD_EQ_COUNTABLE)) THEN
1674   REWRITE_TAC[UNCOUNTABLE_REAL] THEN ASM_MESON_TAC[CARD_EQ_SYM]);;
1675
1676 let COUNTABLE_IMP_CARD_LT_REAL = prove
1677  (`!s:A->bool. COUNTABLE s ==> s <_c (:real)`,
1678   REWRITE_TAC[GSYM CARD_NOT_LE] THEN
1679   ASM_MESON_TAC[CARD_LE_COUNTABLE; UNCOUNTABLE_REAL]);;
1680
1681 (* ------------------------------------------------------------------------- *)
1682 (* More about cardinality of lists and restricted powersets etc.             *)
1683 (* ------------------------------------------------------------------------- *)
1684
1685 let CARD_EQ_FINITE_SUBSETS = prove
1686  (`!s:A->bool. INFINITE(s) ==> {t | t SUBSET s /\ FINITE t} =_c s`,
1687   GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN
1688   CONJ_TAC THENL
1689    [TRANS_TAC CARD_LE_TRANS `{l:A list | !x. MEM x l ==> x IN s}` THEN
1690     CONJ_TAC THENL
1691      [REWRITE_TAC[LE_C; IN_ELIM_THM] THEN
1692       EXISTS_TAC `set_of_list:A list->(A->bool)` THEN
1693       X_GEN_TAC `t:A->bool` THEN STRIP_TAC THEN
1694       EXISTS_TAC `list_of_set(t:A->bool)` THEN
1695       ASM_SIMP_TAC[MEM_LIST_OF_SET; GSYM SUBSET; SET_OF_LIST_OF_SET];
1696       MATCH_MP_TAC CARD_EQ_IMP_LE THEN
1697       MATCH_MP_TAC CARD_EQ_LIST_GEN THEN ASM_REWRITE_TAC[]];
1698    REWRITE_TAC[le_c] THEN EXISTS_TAC `\x:A. {x}` THEN
1699    REWRITE_TAC[IN_ELIM_THM; FINITE_SING] THEN SET_TAC[]]);;
1700
1701 let CARD_LE_LIST = prove
1702  (`!s:A->bool t:B->bool.
1703         s <=_c t
1704         ==> {l | !x. MEM x l ==> x IN s} <=_c {l | !x. MEM x l ==> x IN t}`,
1705   GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[le_c; IN_ELIM_THM] THEN
1706   DISCH_THEN(X_CHOOSE_THEN `f:A->B` STRIP_ASSUME_TAC) THEN
1707   EXISTS_TAC `MAP (f:A->B)` THEN
1708   MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN CONJ_TAC THENL
1709    [REWRITE_TAC[MEM_MAP] THEN ASM_MESON_TAC[]; DISCH_TAC] THEN
1710   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
1711   LIST_INDUCT_TAC THEN SIMP_TAC[MAP_EQ_NIL; MAP] THEN
1712   LIST_INDUCT_TAC THEN REWRITE_TAC[MAP; NOT_CONS_NIL; MEM; CONS_11] THEN
1713   ASM_MESON_TAC[]);;
1714
1715 let CARD_LE_SUBPOWERSET = prove
1716  (`!s:A->bool t:B->bool.
1717         s <=_c t /\ (!f s. P s ==> Q(IMAGE f s))
1718         ==> {u | u SUBSET s /\ P u} <=_c {v | v SUBSET t /\ Q v}`,
1719   REPEAT GEN_TAC THEN REWRITE_TAC[le_c; IN_ELIM_THM] THEN DISCH_THEN
1720    (CONJUNCTS_THEN2 (X_CHOOSE_THEN `f:A->B` STRIP_ASSUME_TAC) ASSUME_TAC) THEN
1721   EXISTS_TAC `IMAGE (f:A->B)` THEN ASM_SIMP_TAC[] THEN ASM SET_TAC[]);;
1722
1723 let CARD_LE_FINITE_SUBSETS = prove
1724  (`!s:A->bool t:B->bool.
1725     s <=_c t
1726     ==> {u | u SUBSET s /\ FINITE u} <=_c {v | v SUBSET t /\ FINITE v}`,
1727   REPEAT STRIP_TAC THEN MATCH_MP_TAC CARD_LE_SUBPOWERSET THEN
1728   ASM_SIMP_TAC[FINITE_IMAGE]);;
1729
1730 let CARD_LE_COUNTABLE_SUBSETS = prove
1731  (`!s:A->bool t:B->bool.
1732     s <=_c t
1733     ==> {u | u SUBSET s /\ COUNTABLE u} <=_c {v | v SUBSET t /\ COUNTABLE v}`,
1734   REPEAT STRIP_TAC THEN MATCH_MP_TAC CARD_LE_SUBPOWERSET THEN
1735   ASM_SIMP_TAC[COUNTABLE_IMAGE]);;
1736
1737 let CARD_LE_POWERSET = prove
1738  (`!s:A->bool t:B->bool.
1739     s <=_c t ==> {u | u SUBSET s} <=_c {v | v SUBSET t}`,
1740   REPEAT STRIP_TAC THEN PURE_ONCE_REWRITE_TAC[SET_RULE
1741     `{x | x SUBSET y} = {x | x SUBSET y /\ T}`] THEN
1742   MATCH_MP_TAC CARD_LE_SUBPOWERSET THEN
1743   ASM_SIMP_TAC[]);;
1744
1745 let COUNTABLE_LIST_GEN = prove
1746  (`!s:A->bool. COUNTABLE s ==> COUNTABLE {l | !x. MEM x l ==> x IN s}`,
1747   GEN_TAC THEN REWRITE_TAC[COUNTABLE; ge_c] THEN
1748   DISCH_THEN(MP_TAC o MATCH_MP CARD_LE_LIST) THEN
1749   MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] CARD_LE_TRANS) THEN
1750   MATCH_MP_TAC CARD_EQ_IMP_LE THEN
1751   REWRITE_TAC[IN_UNIV; SET_RULE `{x | T} = UNIV`] THEN
1752   SIMP_TAC[CARD_EQ_LIST; num_INFINITE]);;
1753
1754 let COUNTABLE_LIST = prove
1755  (`COUNTABLE(:A) ==> COUNTABLE(:A list)`,
1756   MP_TAC(ISPEC `(:A)` COUNTABLE_LIST_GEN) THEN
1757   REWRITE_TAC[IN_UNIV; SET_RULE `{x | T} = UNIV`]);;
1758
1759 let COUNTABLE_FINITE_SUBSETS = prove
1760  (`!s:A->bool. COUNTABLE(s) ==> COUNTABLE {t | t SUBSET s /\ FINITE t}`,
1761   GEN_TAC THEN REWRITE_TAC[COUNTABLE; ge_c] THEN
1762   DISCH_THEN(MP_TAC o MATCH_MP CARD_LE_FINITE_SUBSETS) THEN
1763   MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] CARD_LE_TRANS) THEN
1764   MATCH_MP_TAC CARD_EQ_IMP_LE THEN
1765   REWRITE_TAC[IN_UNIV; SET_RULE `{x | T} = UNIV`] THEN
1766   SIMP_TAC[CARD_EQ_FINITE_SUBSETS; num_INFINITE]);;
1767
1768 let CARD_EQ_REAL_SEQUENCES = prove
1769  (`(:num->real) =_c (:real)`,
1770   TRANS_TAC CARD_EQ_TRANS `(:num->num->bool)` THEN
1771   ASM_SIMP_TAC[CARD_FUNSPACE_CONG; CARD_EQ_REFL; CARD_EQ_REAL] THEN
1772   TRANS_TAC CARD_EQ_TRANS `(:num#num->bool)` THEN
1773   ASM_SIMP_TAC[CARD_FUNSPACE_CURRY] THEN
1774   TRANS_TAC CARD_EQ_TRANS `(:num->bool)` THEN
1775   ASM_SIMP_TAC[CARD_FUNSPACE_CONG; CARD_EQ_REFL;
1776                ONCE_REWRITE_RULE[CARD_EQ_SYM] CARD_EQ_REAL;
1777                REWRITE_RULE[MUL_C_UNIV] CARD_SQUARE_NUM]);;
1778
1779 let CARD_EQ_COUNTABLE_SUBSETS_REAL = prove
1780  (`{s:real->bool | COUNTABLE s} =_c (:real)`,
1781   REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN CONJ_TAC THENL
1782    [TRANS_TAC CARD_LE_TRANS
1783      `{{}:real->bool} +_c {s:real->bool | COUNTABLE s /\ ~(s = {})}` THEN
1784     CONJ_TAC THENL
1785      [W(MP_TAC o PART_MATCH rand UNION_LE_ADD_C o rand o snd) THEN
1786       MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] CARD_LE_TRANS) THEN
1787       MATCH_MP_TAC(MESON[CARD_LE_REFL] `s = t ==> s <=_c t`) THEN
1788       ONCE_REWRITE_TAC[EXTENSION] THEN
1789       REWRITE_TAC[IN_ELIM_THM; IN_UNION; IN_SING] THEN
1790       MESON_TAC[COUNTABLE_EMPTY];
1791       ALL_TAC] THEN
1792     TRANS_TAC CARD_LE_TRANS `{{}:real->bool} +_c (:real)` THEN CONJ_TAC THENL
1793      [MATCH_MP_TAC CARD_LE_ADD THEN
1794       REWRITE_TAC[CARD_LE_REFL] THEN
1795       TRANS_TAC CARD_LE_TRANS `(:num->real)` THEN
1796       ASM_SIMP_TAC[CARD_EQ_REAL_SEQUENCES; CARD_EQ_IMP_LE] THEN
1797       REWRITE_TAC[LE_C] THEN EXISTS_TAC `\f:num->real. IMAGE f (:num)` THEN
1798       REWRITE_TAC[IN_UNIV; IN_ELIM_THM] THEN
1799       MESON_TAC[COUNTABLE_AS_IMAGE];
1800       MATCH_MP_TAC CARD_ADD_ABSORB_LE THEN
1801       SIMP_TAC[real_INFINITE; le_c; IN_UNIV; IN_SING]];
1802      REWRITE_TAC[le_c] THEN EXISTS_TAC `\x:real. {x}` THEN
1803      REWRITE_TAC[IN_UNIV; COUNTABLE_SING; IN_ELIM_THM] THEN SET_TAC[]]);;