text_formalization/jordan/misc_defs_and_lemmas.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Jordan                                                               *)
   5 (* Copied from HOL Light jordan directory *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-07-08                                                           *)
   8 (* ========================================================================== *)
   9
  10 (*
  11 The file in the HOL Light distribution is longer, with results about
  12 Euclidan space that are not relevant here.
  13
  14 May 7, 2011, renamed INV -> INVERSE to avoid clash with HOL Library/rstc.ml
  15 *)
  16
  17 module Misc_defs_and_lemmas = struct
  18
  19 open Tactics_jordan;;
  20 open Tactics_jordan;;
  21 open Parse_ext_override_interface;;
  22 (* open Refinement;; *)
  23 open Real_ext;;
  24 open Float;;
  25
  26 (* labels_flag:= true;; *)
  27
  28 let prove_by_refinement = Refinement.enhanced_prove_by_refinement true ALL_TAC;;
  29
  30 let LABEL_ALL_TAC = Refinement.LABEL_ALL_TAC;;
  31
  32 unambiguous_interface();;
  33
  34
  35 let dirac_delta = new_definition `dirac_delta i =
  36    \j. if (i=j) then &1  else &0`;;
  37
  38 (*
  39 let dirac_delta = new_definition `dirac_delta (i:num) j =
  40       if (i=j) then &. 1  else &. 0`;;
  41 *)
  42
  43 (*
  44 let dirac_delta = prove_by_refinement(`!i. dirac_delta i =
  45       (\j. if (i=j) then &. 1  else &. 0)`,
  46    [
  47      GEN_TAC;
  48      ONCE_REWRITE_TAC[FUN_EQ_THM];
  49      REWRITE_TAC[dirac_delta_thm];
  50      BETA_TAC;
  51    ]                   );;
  52 *)
  53
  54 let min_num = new_definition
  55   `min_num (X:num->bool) = @m. (m IN X) /\ (!n. (n IN X) ==> (m <= n))`;;
  56
  57 let min_least = prove_by_refinement (
  58   `!(X:num->bool) c. (X c) ==> (X (min_num X) /\ (min_num X <=| c))`,
  59   (* {{{ proof *)
  60
  61   [
  62   REWRITE_TAC[min_num;IN];
  63   REPEAT GEN_TAC;
  64   DISCH_TAC;
  65   SUBGOAL_THEN `?n. (X:num->bool) n /\ (!m. m <| n ==> ~X m)` MP_TAC;
  66     REWRITE_TAC[(GSYM (ISPEC `X:num->bool` num_WOP))];
  67     ASM_MESON_TAC[];
  68   DISCH_THEN CHOOSE_TAC;
  69   ASSUME_TAC (select_thm `\m. (X:num->bool) m /\ (!n. X n ==> m <=| n)` `n:num`);
  70   ABBREV_TAC `r = @m. (X:num->bool) m /\ (!n. X n ==> m <=| n)`;
  71   ASM_MESON_TAC[ ARITH_RULE `~(n' < n) ==> (n <=| n') `]
  72   ]);;
  73
  74   (* }}} *)
  75
  76 let max_real = new_definition(`max_real x y =
  77         if (y <. x) then x else y`);;
  78
  79 let min_real = new_definition(`min_real x y =
  80         if (x <. y) then x else y`);;
  81
  82 (* let deriv = new_definition(`deriv f x = @d. (f diffl d)(x)`);;
  83 let deriv2 = new_definition(`deriv2 f = (deriv (deriv f))`);; *)
  84
  85 let square_le = prove_by_refinement(
  86   `!x y. (&.0 <=. x) /\ (&.0 <=. y) /\ (x*.x <=. y*.y) ==> (x <=. y)`,
  87   (* {{{ proof *)
  88
  89   [
  90   DISCH_ALL_TAC;
  91   UNDISCH_FIND_TAC `( *. )` ;
  92   ONCE_REWRITE_TAC[REAL_ARITH `(a <=. b) <=> (&.0 <= (b - a))`];
  93   REWRITE_TAC[GSYM REAL_DIFFSQ];
  94   DISCH_TAC;
  95   DISJ_CASES_TAC (REAL_ARITH `&.0 < (y+x) \/ (y+x <=. (&.0))`);
  96   MATCH_MP_TAC (SPEC `(y+x):real` REAL_LE_LCANCEL_IMP);
  97   ASM_REWRITE_TAC [REAL_ARITH `x * (&.0) = (&.0)`];
  98   CLEAN_ASSUME_TAC (REAL_ARITH `(&.0 <= y) /\ (&.0 <=. x) /\ (y+x <= (&.0)) ==> ((x= &.0) /\ (y= &.0))`);
  99   ASM_REWRITE_TAC[REAL_ARITH `&.0 <=. (&.0 -. (&.0))`];
 100   ]);;
 101
 102   (* }}} *)
 103
 104 let max_num_sequence = prove_by_refinement(
 105   `!(t:num->num). (?n. !m. (n <=| m) ==> (t m = 0)) ==>
 106       (?M. !i. (t i <=| M))`,
 107   (* {{{ proof *)
 108   [
 109   GEN_TAC;
 110   REWRITE_TAC[GSYM LEFT_FORALL_IMP_THM];
 111   GEN_TAC;
 112   SPEC_TAC (`t:num->num`,`t:num->num`);
 113   SPEC_TAC (`n:num`,`n:num`);
 114   INDUCT_TAC;
 115   GEN_TAC;
 116   REWRITE_TAC[ARITH_RULE `0<=|m`];
 117   DISCH_TAC;
 118   EXISTS_TAC `0`;
 119   ASM_MESON_TAC[ARITH_RULE`(a=0) ==> (a <=|0)`];
 120   DISCH_ALL_TAC;
 121   ABBREV_TAC `b = \m. (if (m=n) then 0 else (t (m:num)) )`;
 122   FIRST_ASSUM (fun t-> ASSUME_TAC (SPEC `b:num->num` t));
 123   SUBGOAL_MP_TAC `((b:num->num) (n) = 0) /\ (!m. ~(m=n) ==> (b m = t m))`;
 124   EXPAND_TAC "b";
 125   CONJ_TAC;
 126   COND_CASES_TAC;
 127   REWRITE_TAC[];
 128   ASM_MESON_TAC[];
 129   GEN_TAC;
 130   COND_CASES_TAC;
 131   REWRITE_TAC[];
 132   REWRITE_TAC[];
 133   DISCH_ALL_TAC;
 134   FIRST_ASSUM (fun t-> MP_TAC(SPEC `b:num->num` t));
 135   SUBGOAL_MP_TAC `!m. (n<=|m) ==> (b m =0)`;
 136   GEN_TAC;
 137   ASM_CASES_TAC `m = (n:num)`;
 138   ASM_REWRITE_TAC[];
 139   SUBGOAL_MP_TAC ( `(n <=| m) /\ (~(m = n)) ==> (SUC n <=| m)`);
 140   ARITH_TAC;
 141   ASM_REWRITE_TAC[];
 142   DISCH_ALL_TAC;
 143   ASM_MESON_TAC[]; (* good *)
 144   DISCH_THEN (fun t-> REWRITE_TAC[t]);
 145   DISCH_THEN CHOOSE_TAC;
 146   EXISTS_TAC `(M:num) + (t:num->num) n`;
 147   GEN_TAC;
 148   ASM_CASES_TAC `(i:num) = n`;
 149   ASM_REWRITE_TAC[];
 150   ARITH_TAC;
 151   MATCH_MP_TAC (ARITH_RULE `x <=| M ==> (x <=| M+ u)`);
 152   ASM_MESON_TAC[];
 153   ]);;
 154   (* }}} *)
 155
 156 let REAL_INV_LT = prove_by_refinement(
 157   `!x y z. (&.0 <. x) ==> ((inv(x)*y < z) <=> (y <. x*z))`,
 158   (* {{{ proof *)
 159   [
 160   REPEAT GEN_TAC;
 161   DISCH_TAC;
 162   REWRITE_TAC[REAL_ARITH `inv x * y = y* inv x`];
 163   REWRITE_TAC[GSYM real_div];
 164   ASM_SIMP_TAC[REAL_LT_LDIV_EQ];
 165   REAL_ARITH_TAC;
 166   ]);;
 167   (* }}} *)
 168
 169 let REAL_MUL_NN = prove_by_refinement(
 170   `!x y. (&.0 <= x*y) <=>
 171     ((&.0 <= x /\ (&.0 <=. y)) \/ ((x <= &.0) /\ (y <= &.0) ))`,
 172   (* {{{ proof *)
 173   [
 174   DISCH_ALL_TAC;
 175   SUBGOAL_MP_TAC `! x y. ((&.0 < x) ==> ((&.0 <= x*y) <=> ((&.0 <= x /\ (&.0 <=. y)) \/ ((x <= &.0) /\ (y <= &.0) ))))`;
 176   DISCH_ALL_TAC;
 177   ASM_SIMP_TAC[REAL_ARITH `((&.0 <. x) ==> (&.0 <=. x))`;REAL_ARITH `(&.0 <. x) ==> ~(x <=. &.0)`];
 178   EQ_TAC;
 179   ASM_MESON_TAC[REAL_PROP_NN_LCANCEL];
 180   ASM_MESON_TAC[REAL_LE_MUL;REAL_LT_IMP_LE];
 181   DISCH_TAC;
 182   DISJ_CASES_TAC (REAL_ARITH `(&.0 < x) \/ (x = &.0) \/ (x < &.0)`);
 183   ASM_MESON_TAC[];
 184   UND 1 THEN DISCH_THEN  DISJ_CASES_TAC;
 185   ASM_REWRITE_TAC[];
 186   REAL_ARITH_TAC;
 187   ASM_SIMP_TAC[REAL_ARITH `((x <. &.0) ==> ~(&.0 <=. x))`;REAL_ARITH `(x <. &.0) ==> (x <=. &.0)`];
 188   USE 0 (SPECL [`--. (x:real)`;`--. (y:real)`]);
 189   UND 0;
 190   REDUCE_TAC;
 191   ASM_REWRITE_TAC[];
 192   ASM_SIMP_TAC[REAL_ARITH `((x <. &.0) ==> ~(&.0 <=. x))`;REAL_ARITH `(x <. &.0) ==> (x <=. &.0)`];
 193   ]);;
 194   (* }}} *)
 195
 196 let ABS_SQUARE = prove_by_refinement(
 197   `!t u. abs(t) <. u ==> t*t <. u*u`,
 198   (* {{{ proof *)
 199
 200   [
 201   REP_GEN_TAC;
 202   CONV_TAC (SUBS_CONV[SPEC `t:real` (REWRITE_RULE[POW_2] (GSYM REAL_POW2_ABS))]);
 203   ASSUME_TAC REAL_ABS_POS;
 204   USE 0 (SPEC `t:real`);
 205   ABBREV_TAC `(b:real) = (abs t)`;
 206   KILL 1;
 207   DISCH_ALL_TAC;
 208   MATCH_MP_TAC REAL_PROP_LT_LRMUL;
 209   ASM_REWRITE_TAC[];
 210   ]);;
 211
 212   (* }}} *)
 213
 214 let ABS_SQUARE_LE = prove_by_refinement(
 215   `!t u. abs(t) <=. u ==> t*t <=. u*u`,
 216   (* {{{ proof *)
 217
 218   [
 219   REP_GEN_TAC;
 220   CONV_TAC (SUBS_CONV[SPEC `t:real` (REWRITE_RULE[POW_2] (GSYM REAL_POW2_ABS))]);
 221   ASSUME_TAC REAL_ABS_POS;
 222   USE 0 (SPEC `t:real`);
 223   ABBREV_TAC `(b:real) = (abs t)`;
 224   KILL 1;
 225   DISCH_ALL_TAC;
 226   MATCH_MP_TAC REAL_PROP_LE_LRMUL;
 227   ASM_REWRITE_TAC[];
 228   ]);;
 229
 230   (* }}} *)
 231
 232 let POW_2_LE1 = REAL_LE_POW2;;
 233
 234 let REAL_ADD = REAL_OF_NUM_ADD;;
 235
 236 let POW_2_LT = prove_by_refinement(
 237   `!n. &n < &2 pow n`,
 238   [
 239   INDUCT_TAC;
 240   REWRITE_TAC[pow; REAL_LT_01] ;
 241   REWRITE_TAC[pow;ADD1; GSYM REAL_ADD; GSYM REAL_DOUBLE];
 242   MATCH_MP_TAC REAL_LTE_ADD2;
 243   ASM_REWRITE_TAC[POW_2_LE1];
 244   ]);;
 245
 246
 247 let twopow_eps = prove_by_refinement(
 248   `!R e. ?n. (&.0 <. R)/\ (&.0 <. e) ==> R*(twopow(--: (&:n))) <. e`,
 249   (* {{{ proof *)
 250
 251   [
 252   DISCH_ALL_TAC;
 253   REWRITE_TAC[TWOPOW_NEG]; (* cs6b *)
 254   ASSUME_TAC (prove(`!n. &.0 < &.2 pow n`,REDUCE_TAC THEN ARITH_TAC));
 255   ONCE_REWRITE_TAC[REAL_MUL_AC];
 256   ASM_SIMP_TAC[REAL_INV_LT];
 257   ASM_SIMP_TAC[GSYM REAL_LT_LDIV_EQ];
 258   CONV_TAC (quant_right_CONV "n");
 259   DISCH_ALL_TAC;
 260   ASSUME_TAC (SPEC `R/e` REAL_ARCH_SIMPLE);
 261   CHO 3;
 262   EXISTS_TAC `n:num`;
 263   UND 3;
 264   MESON_TAC[POW_2_LT;REAL_LET_TRANS];
 265   ]);;
 266
 267   (* }}} *)
 268
 269
 270 (* ------------------------------------------------------------------ *)
 271 (* finite products, in imitation of finite sums *)
 272 (* ------------------------------------------------------------------ *)
 273
 274 let prod_EXISTS = prove_by_refinement(
 275   `?prod. (!f n.  prod(n,0) f = &1) /\
 276          (!f m n. prod(n,SUC m) f = prod(n,m) f * f(n + m))`,
 277 (* {{{ proof *)
 278   [
 279   (CHOOSE_TAC o prove_recursive_functions_exist num_RECURSION) `(!f n. sm n 0 f = &1) /\ (!f m n. sm  n (SUC m) f = sm n m f * f(n + m))` ;
 280   EXISTS_TAC `\(n,m) f. (sm:num->num->(num->real)->real) n m f`;
 281   CONV_TAC(DEPTH_CONV GEN_BETA_CONV) THEN ASM_REWRITE_TAC[]
 282   ]);;
 283 (* }}} *)
 284
 285 let prod_DEF = new_specification ["prod"] prod_EXISTS;;
 286
 287 let prod = prove
 288  (`!n m. (prod(n,0) f = &1) /\
 289    (prod(n,SUC m) f = prod(n,m) f * f(n + m))`,
 290 (* {{{ proof *)
 291   REWRITE_TAC[prod_DEF]);;
 292 (* }}} *)
 293
 294 let PROD_TWO = prove_by_refinement(
 295  `!f n p. prod(0,n) f * prod(n,p) f = prod(0,n + p) f`,
 296 (* {{{ proof *)
 297   [
 298   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[prod; REAL_MUL_RID; MULT_CLAUSES;ADD_0];
 299   REWRITE_TAC[ARITH_RULE `n+| (SUC p) = (SUC (n+|p))`;prod;ARITH_RULE `0+|n = n`];
 300   ASM_REWRITE_TAC[REAL_MUL_ASSOC];
 301 ]);;
 302 (* }}} *)
 303
 304
 305 let ABS_PROD = prove_by_refinement(
 306  `!f m n. abs(prod(m,n) f) = prod(m,n) (\n. abs(f n))`,
 307 (* {{{ proof *)
 308   [
 309   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC;
 310   REWRITE_TAC[prod];
 311   REAL_ARITH_TAC;
 312   ASM_REWRITE_TAC[prod;ABS_MUL]
 313   ]);;
 314 (* }}} *)
 315
 316 let PROD_EQ = prove_by_refinement
 317  (`!f g m n. (!r. m <= r /\ r < (n + m) ==> (f(r) = g(r)))
 318         ==> (prod(m,n) f = prod(m,n) g)`,
 319 (* {{{ proof *)
 320
 321   [
 322   GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[prod];
 323   REWRITE_TAC[prod];
 324   DISCH_THEN (fun th -> MP_TAC th THEN (MP_TAC (SPEC `m+|n` th)));
 325   REWRITE_TAC[ARITH_RULE `(m<=| (m+|n))/\ (m +| n <| (SUC n +| m))`];
 326   DISCH_ALL_TAC;
 327   ASM_REWRITE_TAC[];
 328   AP_THM_TAC THEN AP_TERM_TAC;
 329   FIRST_X_ASSUM MATCH_MP_TAC;
 330   GEN_TAC THEN DISCH_TAC;
 331   FIRST_X_ASSUM MATCH_MP_TAC;
 332   ASM_MESON_TAC[ARITH_RULE `r <| (n+| m) ==> (r <| (SUC n +| m))`]
 333   ]);;
 334
 335 (* }}} *)
 336
 337 let PROD_POS = prove_by_refinement
 338  (`!f. (!n. &0 <= f(n)) ==> !m n. &0 <= prod(m,n) f`,
 339 (* {{{ proof *)
 340
 341   [
 342   GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[prod];
 343   REAL_ARITH_TAC;
 344   ASM_MESON_TAC[REAL_LE_MUL]
 345   ]);;
 346 (* }}} *)
 347
 348 let PROD_POS_GEN = prove_by_refinement
 349  (`!f m n.
 350      (!n. m <= n ==> &0 <= f(n))
 351      ==> &0 <= prod(m,n) f`,
 352 (* {{{ proof *)
 353
 354   [
 355   REPEAT STRIP_TAC THEN SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN REWRITE_TAC[prod];
 356   REAL_ARITH_TAC;
 357   ASM_MESON_TAC[REAL_LE_MUL;ARITH_RULE `m <=| (m +| n)`]
 358   ]);;
 359 (* }}} *)
 360
 361
 362 let PROD_ABS = prove
 363  (`!f m n. abs(prod(m,n) (\m. abs(f m))) = prod(m,n) (\m. abs(f m))`,
 364 (* {{{ proof *)
 365   REWRITE_TAC[ABS_PROD;REAL_ARITH `||. (||. x) = (||. x)`]);;
 366 (* }}} *)
 367
 368 let PROD_ZERO = prove_by_refinement
 369  (`!f m n. (?p. (m <= p /\ (p < (n+| m)) /\ (f p = (&.0)))) ==>
 370          (prod(m,n) f = &0)`,
 371 (* {{{ proof *)
 372   [
 373   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN (REWRITE_TAC[prod]);
 374   ARITH_TAC;
 375   DISCH_THEN CHOOSE_TAC;
 376   ASM_CASES_TAC `p <| (n+| m)`;
 377   MATCH_MP_TAC (prove (`(x = (&.0)) ==> (x *. y = (&.0))`,(DISCH_THEN (fun th -> (REWRITE_TAC[th]))) THEN REAL_ARITH_TAC));
 378   FIRST_X_ASSUM MATCH_MP_TAC;
 379   ASM_MESON_TAC[];
 380   POP_ASSUM (fun th -> ASSUME_TAC (MATCH_MP (ARITH_RULE `(~(p <| (n+|m)) ==> ((p <| ((SUC n) +| m)) ==> (p = ((m +| n)))))`) th));
 381   MATCH_MP_TAC (prove (`(x = (&.0)) ==> (y *. x = (&.0))`,(DISCH_THEN (fun th -> (REWRITE_TAC[th]))) THEN REAL_ARITH_TAC));
 382   ASM_MESON_TAC[]
 383  ]);;
 384 (* }}} *)
 385
 386 let PROD_MUL = prove_by_refinement(
 387   `!f g m n. prod(m,n) (\n. f(n) * g(n)) = prod(m,n) f * prod(m,n) g`,
 388   (* {{{ proof *)
 389   [
 390   EVERY(replicate GEN_TAC 3) THEN INDUCT_TAC THEN ASM_REWRITE_TAC[prod];
 391   REAL_ARITH_TAC;
 392   REWRITE_TAC[REAL_MUL_AC];
 393   ]);;
 394   (* }}} *)
 395
 396 let PROD_CMUL = prove_by_refinement(
 397   `!f c m n. prod(m,n) (\n. c * f(n)) = (c **. n) * prod(m,n) f`,
 398   (* {{{ proof *)
 399   [
 400   EVERY(replicate GEN_TAC 3) THEN INDUCT_TAC THEN ASM_REWRITE_TAC[prod;pow];
 401   REAL_ARITH_TAC;
 402   REWRITE_TAC[REAL_MUL_AC];
 403   ]);;
 404   (* }}} *)
 405
 406 (* ------------------------------------------------------------------ *)
 407 (*  LEMMAS ABOUT SETS                                                 *)
 408 (* ------------------------------------------------------------------ *)
 409
 410 (* IN_ELIM_THM produces garbled results at times. I like this better: *)
 411
 412 (*** JRH replaced this with the "new" IN_ELIM_THM; see how it works.
 413
 414 let IN_ELIM_THM' = prove_by_refinement(
 415  `(!P. !x:A. x IN (GSPEC P) <=> P x) /\
 416    (!P. !x:A. x IN (\x. P x) <=> P x) /\
 417    (!P. !x:A. (GSPEC P) x <=> P x) /\
 418    (!P (x:A) (t:A). (\t. (?y:A. P y /\ (t = y))) x <=> P x)`,
 419   (* {{{ proof *)
 420   [
 421   REWRITE_TAC[IN; GSPEC];
 422   MESON_TAC[];
 423   ]);;
 424   (* }}} *)
 425
 426  ****)
 427
 428 let IN_ELIM_THM' = IN_ELIM_THM;;
 429
 430 let SURJ_IMAGE = prove_by_refinement(
 431   `!(f:A->B) a b. SURJ f a b ==> (b = (IMAGE f a))`,
 432 (* {{{ proof *)
 433
 434   [
 435   REPEAT GEN_TAC;
 436   REWRITE_TAC[SURJ;IMAGE];
 437   DISCH_ALL_TAC;
 438   REWRITE_TAC[EXTENSION];
 439   GEN_TAC;
 440   REWRITE_TAC[IN_ELIM_THM];
 441   ASM_MESON_TAC[]]
 442
 443 (* }}} *)
 444 );;
 445
 446
 447 let SURJ_FINITE = prove_by_refinement(
 448   `!a b (f:A->B). FINITE a /\ (SURJ f a b) ==> FINITE b`,
 449 (* {{{ *)
 450
 451   [
 452   ASM_MESON_TAC[SURJ_IMAGE;FINITE_IMAGE]
 453   ]);;
 454
 455 (* }}} *)
 456
 457 let BIJ_INVERSE = prove_by_refinement(
 458   `!a b (f:A->B). (SURJ f a b) ==> (?(g:B->A). (INJ g b a))`,
 459 (* {{{ proof *)
 460
 461   [
 462   REPEAT GEN_TAC;
 463   DISCH_ALL_TAC;
 464   SUBGOAL_THEN `!y. ?u. ((y IN b) ==> ((u IN a) /\ ((f:A->B) u = y)))` ASSUME_TAC;
 465   ASM_MESON_TAC[SURJ];
 466   LABEL_ALL_TAC;
 467   H_REWRITE_RULE[THM SKOLEM_THM] (HYP "1");
 468   LABEL_ALL_TAC;
 469   H_UNDISCH_TAC (HYP"2");
 470   DISCH_THEN CHOOSE_TAC;
 471   EXISTS_TAC `u:B->A`;
 472   REWRITE_TAC[INJ] THEN  CONJ_TAC THEN (ASM_MESON_TAC[])
 473   ]
 474
 475 (* }}} *)
 476 );;
 477
 478 (* complement of an intersection is a union of complements *)
 479 let UNIONS_INTERS = prove_by_refinement(
 480   `!(X:A->bool)  V.
 481      (X DIFF (INTERS V) = UNIONS (IMAGE ((DIFF) X) V))`,
 482 (* {{{ proof *)
 483
 484   [
 485   REPEAT GEN_TAC;
 486   MATCH_MP_TAC SUBSET_ANTISYM;
 487   CONJ_TAC;
 488   REWRITE_TAC[SUBSET;IMAGE;IN_ELIM_THM];
 489   X_GEN_TAC `c:A`;
 490   REWRITE_TAC[IN_DIFF;IN_INTERS;IN_UNIONS;NOT_FORALL_THM];
 491   DISCH_ALL_TAC;
 492   UNDISCH_FIND_THEN `(?)` CHOOSE_TAC;
 493   EXISTS_TAC `(X DIFF t):A->bool`;
 494   REWRITE_TAC[IN_ELIM_THM];
 495   CONJ_TAC;
 496   EXISTS_TAC `t:A->bool`;
 497   ASM_MESON_TAC[];
 498   REWRITE_TAC[IN_DIFF];
 499   ASM_MESON_TAC[];
 500   REWRITE_TAC[SUBSET;IMAGE;IN_ELIM_THM];
 501   X_GEN_TAC `c:A`;
 502   REWRITE_TAC[IN_DIFF;IN_UNIONS];
 503   DISCH_THEN CHOOSE_TAC;
 504   UNDISCH_FIND_TAC `(IN)`;
 505   REWRITE_TAC[IN_INTERS;IN_ELIM_THM];
 506   DISCH_ALL_TAC;
 507   UNDISCH_FIND_THEN `(?)` CHOOSE_TAC;
 508   CONJ_TAC;
 509   ASM_MESON_TAC[SUBSET_DIFF;SUBSET];
 510   REWRITE_TAC[NOT_FORALL_THM];
 511   EXISTS_TAC `x:A->bool`;
 512   ASM_MESON_TAC[IN_DIFF];
 513   ]);;
 514
 515 (* }}} *)
 516
 517 let INTERS_SUBSET = prove_by_refinement (
 518    `!X (A:A->bool).  (A IN X) ==> (INTERS X SUBSET A)`,
 519 (* {{{ *)
 520   [
 521   REPEAT GEN_TAC;
 522   REWRITE_TAC[SUBSET;IN_INTERS];
 523   MESON_TAC[IN];
 524   ]);;
 525 (* }}} *)
 526
 527 let sub_union = prove_by_refinement(
 528   `!X (U:(A->bool)->bool). (U X) ==> (X SUBSET (UNIONS U))`,
 529 (* {{{ *)
 530  [
 531  DISCH_ALL_TAC;
 532  REWRITE_TAC[SUBSET;IN_ELIM_THM;UNIONS];
 533  REWRITE_TAC[IN];
 534  DISCH_ALL_TAC;
 535  EXISTS_TAC `X:A->bool`;
 536  ASM_REWRITE_TAC[];
 537  ]);;
 538 (* }}} *)
 539
 540 let IMAGE_SURJ = prove_by_refinement(
 541  `!(f:A->B) a. SURJ f a (IMAGE f a)`,
 542 (* {{{ *)
 543  [
 544  REWRITE_TAC[SURJ;IMAGE;IN_ELIM_THM];
 545  MESON_TAC[IN];
 546  ]);;
 547 (* }}} *)
 548
 549 let SUBSET_PREIMAGE = prove_by_refinement(
 550   `!(f:A->B) X Y. (Y SUBSET (IMAGE f X)) ==>
 551     (?Z. (Z SUBSET X) /\ (Y = IMAGE f Z))`,
 552 (* {{{ proof *)
 553  [
 554  DISCH_ALL_TAC;
 555  EXISTS_TAC `{x | (x IN (X:A->bool))/\ (f x IN (Y:B->bool)) }`;
 556  CONJ_TAC;
 557  REWRITE_TAC[SUBSET;IN_ELIM_THM];
 558  MESON_TAC[];
 559  REWRITE_TAC[EXTENSION];
 560  X_GEN_TAC `y:B`;
 561  UNDISCH_FIND_TAC `(SUBSET)`;
 562  REWRITE_TAC[SUBSET;IN_IMAGE];
 563  REWRITE_TAC[IN_ELIM_THM];
 564  DISCH_THEN (fun t-> MP_TAC (SPEC `y:B` t));
 565  MESON_TAC[];
 566  ]);;
 567 (* }}} *)
 568
 569 let UNIONS_INTER = prove_by_refinement(
 570   `!(U:(A->bool)->bool) A. (((UNIONS U) INTER A) =
 571        (UNIONS (IMAGE ((INTER) A) U)))`,
 572  (* {{{ proof *)
 573  [
 574  REPEAT GEN_TAC;
 575  MATCH_MP_TAC (prove(`((C SUBSET (B:A->bool)) /\ (C SUBSET A) /\ ((A INTER B) SUBSET C)) ==> ((B INTER A) = C)`,SET_TAC[]));
 576  CONJ_TAC;
 577  REWRITE_TAC[SUBSET;UNIONS;IN_ELIM_THM];
 578  REWRITE_TAC[IN_IMAGE];
 579  SET_TAC[];
 580  REWRITE_TAC[SUBSET;UNIONS;IN_IMAGE];
 581  CONJ_TAC;
 582  REWRITE_TAC[IN_ELIM_THM];
 583  X_GEN_TAC `y:A`;
 584  DISCH_THEN CHOOSE_TAC;
 585  ASM_MESON_TAC[IN_INTER];
 586  REWRITE_TAC[IN_INTER];
 587  REWRITE_TAC[IN_ELIM_THM];
 588  X_GEN_TAC `y:A`;
 589  DISCH_ALL_TAC;
 590  UNDISCH_FIND_THEN `(?)` CHOOSE_TAC;
 591  EXISTS_TAC `A INTER (u:A->bool)`;
 592  ASM SET_TAC[];
 593  ]);;
 594 (* }}} *)
 595
 596 let UNIONS_SUBSET = prove_by_refinement(
 597  `!U (X:A->bool). (!A. (A IN U) ==> (A SUBSET X))  ==> (UNIONS U SUBSET X)`,
 598 (* {{{ *)
 599  [
 600  REPEAT GEN_TAC;
 601  SET_TAC[];
 602  ]);;
 603 (* }}} *)
 604
 605 let SUBSET_INTER = prove_by_refinement(
 606  `!X A (B:A->bool). (X SUBSET (A INTER B)) <=> (X SUBSET A) /\ (X SUBSET B)`,
 607 (* {{{ *)
 608  [
 609  REWRITE_TAC[SUBSET;INTER;IN_ELIM_THM];
 610  MESON_TAC[IN];
 611  ]);;
 612 (* }}} *)
 613
 614 let EMPTY_EXISTS = prove_by_refinement(
 615  `!X. ~(X = {}) <=> (? (u:A). (u IN X))`,
 616 (* {{{ *)
 617  [
 618  REWRITE_TAC[EXTENSION];
 619  REWRITE_TAC[IN;EMPTY];
 620  MESON_TAC[];
 621  ]);;
 622 (* }}} *)
 623
 624 let UNIONS_UNIONS = prove_by_refinement(
 625  `!A B. (A SUBSET B) ==>(UNIONS (A:(A->bool)->bool) SUBSET (UNIONS B))`,
 626 (* {{{ *)
 627  [
 628  REWRITE_TAC[SUBSET;UNIONS;IN_ELIM_THM];
 629  MESON_TAC[IN];
 630  ]);;
 631 (* }}} *)
 632
 633
 634 (* nested union can flatten from outside in, or inside out *)
 635 let UNIONS_IMAGE_UNIONS = prove_by_refinement(
 636   `!(X:((A->bool)->bool)->bool).
 637     UNIONS (UNIONS X) = (UNIONS (IMAGE UNIONS X))`,
 638  (* {{{ proof *)
 639   [
 640   GEN_TAC;
 641   REWRITE_TAC[EXTENSION;IN_UNIONS];
 642   GEN_TAC;
 643   REWRITE_TAC[EXTENSION;IN_UNIONS];
 644   EQ_TAC;
 645   DISCH_THEN (CHOOSE_THEN MP_TAC);
 646   DISCH_ALL_TAC;
 647   FIRST_ASSUM MP_TAC;
 648   DISCH_THEN CHOOSE_TAC;
 649   EXISTS_TAC `UNIONS (t':(A->bool)->bool)`;
 650   REWRITE_TAC[IN_UNIONS;IN_IMAGE];
 651   CONJ_TAC;
 652   EXISTS_TAC `(t':(A->bool)->bool)`;
 653   ASM_REWRITE_TAC[];
 654   ASM_MESON_TAC[];
 655   DISCH_THEN CHOOSE_TAC;
 656   FIRST_ASSUM MP_TAC;
 657   REWRITE_TAC[IN_IMAGE];
 658   DISCH_ALL_TAC;
 659   FIRST_ASSUM MP_TAC;
 660   DISCH_THEN CHOOSE_TAC;
 661   UNDISCH_TAC `(x:A) IN t`;
 662   FIRST_ASSUM (fun t-> REWRITE_TAC[t]);
 663   REWRITE_TAC[IN_UNIONS];
 664   DISCH_THEN (CHOOSE_TAC);
 665   EXISTS_TAC `t':(A->bool)`;
 666   CONJ_TAC;
 667   EXISTS_TAC `x':(A->bool)->bool`;
 668   ASM_REWRITE_TAC[];
 669   ASM_REWRITE_TAC[];
 670   ]);;
 671 (* }}} *)
 672
 673
 674 let INTERS_SUBSET2 = prove_by_refinement(
 675   `!X A. (?(x:A->bool). (A x /\ (x SUBSET X))) ==> ((INTERS A) SUBSET X)`,
 676   (* {{{ proof *)
 677   [
 678   REWRITE_TAC[SUBSET;INTERS;IN_ELIM_THM'];
 679   REWRITE_TAC[IN];
 680   MESON_TAC[];
 681   ]);;
 682   (* }}} *)
 683
 684 (**** New proof by JRH; old one breaks because of new set comprehensions
 685
 686 let INTERS_EMPTY = prove_by_refinement(
 687   `INTERS EMPTY = (UNIV:A->bool)`,
 688   (* {{{ proof *)
 689   [
 690   REWRITE_TAC[INTERS;NOT_IN_EMPTY;IN_ELIM_THM';];
 691   REWRITE_TAC[UNIV;GSPEC];
 692   MATCH_MP_TAC  EQ_EXT;
 693   GEN_TAC;
 694   REWRITE_TAC[IN_ELIM_THM'];
 695   MESON_TAC[];
 696   ]);;
 697   (* }}} *)
 698
 699  ****)
 700
 701 let INTERS_EMPTY = prove_by_refinement(
 702   `INTERS EMPTY = (UNIV:A->bool)`,
 703   [SET_TAC[]]);;
 704
 705 let preimage = new_definition `preimage dom (f:A->B)
 706   Z = {x | (x IN dom) /\ (f x IN Z)}`;;
 707
 708 let in_preimage = prove_by_refinement(
 709   `!f x Z dom. x IN (preimage dom (f:A->B) Z) <=> (x IN dom) /\ (f x IN Z)`,
 710 (* {{{ *)
 711   [
 712   REWRITE_TAC[preimage];
 713   REWRITE_TAC[IN_ELIM_THM']
 714   ]);;
 715 (* }}} *)
 716
 717 (* Partial functions, which we identify with functions that
 718    take the canonical choice of element outside the domain. *)
 719
 720 let supp = new_definition
 721   `supp (f:A->B) = \ x.  ~(f x = (CHOICE (UNIV:B ->bool)) )`;;
 722
 723 let func = new_definition
 724   `func a b = (\ (f:A->B). ((!x. (x IN a) ==> (f x IN b)) /\
 725               ((supp f) SUBSET a))) `;;
 726
 727
 728 (* relations *)
 729 let reflexive = new_definition
 730   `reflexive (f:A->A->bool) <=> (!x. f x x)`;;
 731
 732 let symmetric = new_definition
 733   `symmetric (f:A->A->bool) <=> (!x y. f x y ==> f y x)`;;
 734
 735 let transitive = new_definition
 736   `transitive (f:A->A->bool) <=> (!x y z. f x y /\ f y z ==> f x z)`;;
 737
 738 let equivalence_relation = new_definition
 739   `equivalence_relation (f:A->A->bool) <=>
 740     (reflexive f) /\ (symmetric f) /\ (transitive f)`;;
 741
 742 (* We do not introduce the equivalence class of f explicitly, because
 743    it is represented directly in HOL by (f a) *)
 744
 745 let partition_DEF = new_definition
 746   `partition (A:A->bool) SA <=> (UNIONS SA = A) /\
 747    (!a b. ((a IN SA) /\ (b IN SA) /\ (~(a = b)) ==> ({} = (a INTER b))))`;;
 748
 749 let DIFF_DIFF2 = prove_by_refinement(
 750   `!X (A:A->bool). (A SUBSET X) ==> ((X DIFF (X DIFF A)) = A)`,
 751   [
 752   SET_TAC[]
 753   ]);;
 754
 755 (*** Old proof replaced by JRH: no longer UNWIND_THM[12] clause in IN_ELIM_THM
 756
 757 let GSPEC_THM = prove_by_refinement(
 758   `!P (x:A). (?y. P y /\ (x = y)) <=> P x`,
 759   [REWRITE_TAC[IN_ELIM_THM]]);;
 760
 761 ***)
 762
 763 let GSPEC_THM = prove_by_refinement(
 764   `!P (x:A). (?y. P y /\ (x = y)) <=> P x`,
 765   [MESON_TAC[]]);;
 766
 767 let CARD_GE_REFL = prove
 768  (`!s:A->bool. s >=_c s`,
 769   GEN_TAC THEN REWRITE_TAC[GE_C] THEN
 770   EXISTS_TAC `\x:A. x` THEN MESON_TAC[]);;
 771
 772 let FINITE_HAS_SIZE_LEMMA = prove
 773  (`!s:A->bool. FINITE s ==> ?n:num. {x | x < n} >=_c s`,
 774   MATCH_MP_TAC FINITE_INDUCT THEN CONJ_TAC THENL
 775    [EXISTS_TAC `0` THEN REWRITE_TAC[NOT_IN_EMPTY; GE_C; IN_ELIM_THM];
 776     REPEAT GEN_TAC THEN DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN
 777     EXISTS_TAC `SUC N` THEN POP_ASSUM MP_TAC THEN PURE_REWRITE_TAC[GE_C] THEN
 778     DISCH_THEN(X_CHOOSE_TAC `f:num->A`) THEN
 779     EXISTS_TAC `\n:num. if n = N then x:A else f n` THEN
 780     X_GEN_TAC `y:A` THEN PURE_REWRITE_TAC[IN_INSERT] THEN
 781     DISCH_THEN(DISJ_CASES_THEN2 SUBST_ALL_TAC (ANTE_RES_THEN MP_TAC)) THENL
 782      [EXISTS_TAC `N:num` THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN ARITH_TAC;
 783       DISCH_THEN(X_CHOOSE_THEN `n:num` MP_TAC) THEN
 784       REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
 785       EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[] THEN
 786       UNDISCH_TAC `n:num < N` THEN COND_CASES_TAC THEN
 787       ASM_REWRITE_TAC[LT_REFL] THEN ARITH_TAC]]);;
 788
 789 let NUM_COUNTABLE = prove_by_refinement(
 790   `COUNTABLE (UNIV:num->bool)`,
 791   (* {{{ proof *)
 792
 793   [
 794   REWRITE_TAC[COUNTABLE;CARD_GE_REFL];
 795   ]);;
 796
 797   (* }}} *)
 798
 799 let NUM2_COUNTABLE = prove_by_refinement(
 800   `COUNTABLE {((x:num),(y:num)) | T}`,
 801   (* {{{ proof *)
 802   [
 803   CHOOSE_TAC (ISPECL[`(0,0)`;`(\ (a:num,b:num) (n:num) . if (b=0) then (0,a+b+1) else (a+1,b-1))`] num_RECURSION);
 804   REWRITE_TAC[COUNTABLE;GE_C;IN_ELIM_THM'];
 805   NAME_CONFLICT_TAC;
 806   EXISTS_TAC `fn:num -> (num#num)`;
 807   X_GEN_TAC `p:num#num`;
 808   REPEAT (DISCH_THEN (CHOOSE_THEN MP_TAC));
 809   DISCH_THEN (fun t->REWRITE_TAC[t]);
 810   REWRITE_TAC[IN_UNIV];
 811   SUBGOAL_MP_TAC `?t. t = x'+|y'`;
 812   MESON_TAC[];
 813   SPEC_TAC (`x':num`,`a:num`);
 814   SPEC_TAC (`y':num`,`b:num`);
 815   CONV_TAC (quant_left_CONV "t");
 816   CONV_TAC (quant_left_CONV "t");
 817   CONV_TAC (quant_left_CONV "t");
 818   INDUCT_TAC;
 819   REDUCE_TAC;
 820   REP_GEN_TAC;
 821   DISCH_THEN (fun t -> REWRITE_TAC[t]);
 822   EXISTS_TAC `0`;
 823   ASM_REWRITE_TAC[];
 824   CONV_TAC (quant_left_CONV "a");
 825   INDUCT_TAC;
 826   REDUCE_TAC;
 827   GEN_TAC;
 828   USE 1 (SPECL [`0`;`t:num`]);
 829   UND 1 THEN REDUCE_TAC;
 830   DISCH_THEN (X_CHOOSE_TAC `n:num`);
 831   AND 0;
 832   USE 0 (SPEC `n:num`);
 833   UND 0;
 834   UND 1;
 835   DISCH_THEN (fun t-> REWRITE_TAC[GSYM t]);
 836   CONV_TAC (ONCE_DEPTH_CONV GEN_BETA_CONV);
 837   BETA_TAC;
 838   REDUCE_TAC;
 839   DISCH_ALL_TAC;
 840   EXISTS_TAC `SUC n`;
 841   EXPAND_TAC "b";
 842   KILL 0;
 843   ASM_REWRITE_TAC[];
 844   REWRITE_TAC [ARITH_RULE `SUC t = t+|1`];
 845   GEN_TAC;
 846   ABBREV_TAC `t'  = SUC t`;
 847   USE 2 (SPEC `SUC b`);
 848   DISCH_TAC;
 849   UND 2;
 850   ASM_REWRITE_TAC[];
 851   REWRITE_TAC[ARITH_RULE `SUC a +| b = a +| SUC b`];
 852   DISCH_THEN (X_CHOOSE_TAC `n:num`);
 853   EXISTS_TAC `SUC n`;
 854   AND 0;
 855   USE 0 (SPEC `n:num`);
 856   UND 0;
 857   UND 2;
 858   DISCH_THEN (fun t->REWRITE_TAC[GSYM t]);
 859   CONV_TAC (ONCE_DEPTH_CONV GEN_BETA_CONV);
 860   BETA_TAC;
 861   REDUCE_TAC;
 862   DISCH_THEN (fun t->REWRITE_TAC[t]);
 863   REWRITE_TAC[ARITH_RULE `SUC a = a+| 1`];
 864   ]);;
 865   (* }}} *)
 866
 867 let COUNTABLE_UNIONS = prove_by_refinement(
 868   `!A:(A->bool)->bool. (COUNTABLE A) /\
 869       (!a. (a IN A) ==> (COUNTABLE a)) ==> (COUNTABLE (UNIONS A))`,
 870   (* {{{ proof *)
 871   [
 872   GEN_TAC;
 873   DISCH_ALL_TAC;
 874   USE 0 (REWRITE_RULE[COUNTABLE;GE_C;IN_UNIV]);
 875   CHO 0;
 876   USE 0 (CONV_RULE (quant_left_CONV "x"));
 877   USE 0 (CONV_RULE (quant_left_CONV "x"));
 878   CHO 0;
 879   USE 1 (REWRITE_RULE[COUNTABLE;GE_C;IN_UNIV]);
 880   USE 1 (CONV_RULE (quant_left_CONV "f"));
 881   USE 1 (CONV_RULE (quant_left_CONV "f"));
 882   UND 1;
 883   DISCH_THEN (X_CHOOSE_TAC `g:(A->bool)->num->A`);
 884   SUBGOAL_MP_TAC `!a y. (a IN (A:(A->bool)->bool)) /\ (y IN a) ==> (? (u:num) (v:num). ( a = f u) /\ (y = g a v))`;
 885   REP_GEN_TAC;
 886   DISCH_ALL_TAC;
 887   USE 1 (SPEC `a:A->bool`);
 888   USE 0 (SPEC `a:A->bool`);
 889   EXISTS_TAC `(x:(A->bool)->num) a`;
 890   ASM_SIMP_TAC[];
 891   ASSUME_TAC NUM2_COUNTABLE;
 892   USE 2 (REWRITE_RULE[COUNTABLE;GE_C;IN_ELIM_THM';IN_UNIV]);
 893   USE 2 (CONV_RULE NAME_CONFLICT_CONV);
 894   UND 2 THEN (DISCH_THEN (X_CHOOSE_TAC `h:num->(num#num)`));
 895   DISCH_TAC;
 896   REWRITE_TAC[COUNTABLE;GE_C;IN_ELIM_THM';IN_UNIV;IN_UNIONS];
 897   EXISTS_TAC `(\p. (g:(A->bool)->num->A) ((f:num->(A->bool)) (FST ((h:num->(num#num)) p))) (SND (h p)))`;
 898   BETA_TAC;
 899   GEN_TAC;
 900   DISCH_THEN (CHOOSE_THEN MP_TAC);
 901   DISCH_ALL_TAC;
 902   USE 3 (SPEC `t:A->bool`);
 903   USE 3 (SPEC `y:A`);
 904   UND 3 THEN (ASM_REWRITE_TAC[]);
 905   REPEAT (DISCH_THEN(CHOOSE_THEN (MP_TAC)));
 906   DISCH_ALL_TAC;
 907   USE 2 (SPEC `(u:num,v:num)`);
 908   SUBGOAL_MP_TAC `?x' y'. (u:num,v:num) = (x',y')`;
 909   MESON_TAC[];
 910   DISCH_TAC;
 911   UND 2;
 912   ASM_REWRITE_TAC[];
 913   DISCH_THEN (CHOOSE_THEN (ASSUME_TAC o GSYM));
 914   EXISTS_TAC `x':num`;
 915   ASM_REWRITE_TAC[];
 916   ]);;
 917   (* }}} *)
 918
 919 let COUNTABLE_IMAGE = prove_by_refinement(
 920   `!(A:A->bool) (B:B->bool) . (COUNTABLE A) /\ (?f. (B SUBSET IMAGE f A)) ==>
 921         (COUNTABLE B)`,
 922   (* {{{ proof *)
 923   [
 924   REWRITE_TAC[COUNTABLE;GE_C;IN_UNIV;IN_ELIM_THM';SUBSET];
 925   DISCH_ALL_TAC;
 926   CHO 0;
 927   USE 1 (REWRITE_RULE[IMAGE;IN_ELIM_THM']);
 928   CHO 1;
 929   USE 1 (REWRITE_RULE[IN_ELIM_THM']);
 930   USE 1 (CONV_RULE NAME_CONFLICT_CONV);
 931   EXISTS_TAC `(f':A->B) o (f:num->A)`;
 932   REWRITE_TAC[o_DEF];
 933   DISCH_ALL_TAC;
 934   USE 1 (SPEC `y:B`);
 935   UND 1;
 936   ASM_REWRITE_TAC[];
 937   DISCH_THEN CHOOSE_TAC;
 938   USE 0 (SPEC `x':A`);
 939   UND 0 THEN (ASM_REWRITE_TAC[]) THEN DISCH_TAC;
 940   ASM_MESON_TAC[];
 941   ]);;
 942   (* }}} *)
 943
 944 let COUNTABLE_CARD = prove_by_refinement(
 945   `!(A:A->bool) (B:B->bool). (COUNTABLE A) /\ (A >=_c B) ==>
 946      (COUNTABLE B)`,
 947   (* {{{ proof *)
 948
 949   [
 950   DISCH_ALL_TAC;
 951   MATCH_MP_TAC COUNTABLE_IMAGE;
 952   EXISTS_TAC `A:A->bool`;
 953   ASM_REWRITE_TAC[];
 954   REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM'];
 955   USE 1 (REWRITE_RULE[GE_C]);
 956   CHO 1;
 957   EXISTS_TAC `f:A->B`;
 958   ASM_REWRITE_TAC[];
 959   ]);;
 960
 961   (* }}} *)
 962
 963 let COUNTABLE_NUMSEG = prove_by_refinement(
 964   `!n. COUNTABLE {x | x <| n}`,
 965   (* {{{ proof *)
 966   [
 967   GEN_TAC;
 968   REWRITE_TAC[COUNTABLE;GE_C;IN_UNIV];
 969   EXISTS_TAC `I:num->num`;
 970   REDUCE_TAC;
 971   REWRITE_TAC[IN_ELIM_THM'];
 972   MESON_TAC[];
 973   ]);;
 974   (* }}} *)
 975
 976 let FINITE_COUNTABLE = prove_by_refinement(
 977   `!(A:A->bool). (FINITE A) ==> (COUNTABLE A)`,
 978   (* {{{ proof *)
 979   [
 980   DISCH_ALL_TAC;
 981   USE 0 (MATCH_MP FINITE_HAS_SIZE_LEMMA);
 982   CHO 0;
 983   ASSUME_TAC(SPEC `n:num` COUNTABLE_NUMSEG);
 984   JOIN 1 0;
 985   USE 0 (MATCH_MP COUNTABLE_CARD);
 986   ASM_REWRITE_TAC[];
 987   ]);;
 988   (* }}} *)
 989
 990 let num_infinite = prove_by_refinement(
 991   `~ (FINITE (UNIV:num->bool))`,
 992   (* {{{ proof *)
 993   [
 994   PROOF_BY_CONTR_TAC;
 995   USE 0 (REWRITE_RULE[]);
 996   USE 0 (MATCH_MP num_FINITE_AVOID);
 997   USE 0 (REWRITE_RULE[IN_UNIV]);
 998   ASM_REWRITE_TAC[];
 999   ]);;
1000   (* }}} *)
1001
1002 let num_SEG_UNION = prove_by_refinement(
1003   `!i. ({u | i <| u} UNION {m | m <=| i}) = UNIV`,
1004   (* {{{ proof *)
1005   [
1006   REP_BASIC_TAC;
1007   SUBGOAL_MP_TAC `({u | i <| u} UNION {m | m <=| i}) = UNIV`;
1008   MATCH_MP_TAC EQ_EXT;
1009   GEN_TAC;
1010   REWRITE_TAC[UNIV;UNION;IN_ELIM_THM'];
1011   ARITH_TAC;
1012   REWRITE_TAC[];
1013   ]);;
1014   (* }}} *)
1015
1016 let num_above_infinite = prove_by_refinement(
1017   `!i. ~ (FINITE {u | i <| u})`,
1018   (* {{{ proof *)
1019   [
1020   GEN_TAC;
1021   PROOF_BY_CONTR_TAC;
1022   USE 0 (REWRITE_RULE[]);
1023   ASSUME_TAC(SPEC `i:num` FINITE_NUMSEG_LE);
1024   JOIN 0 1;
1025   USE 0 (MATCH_MP FINITE_UNION_IMP);
1026   SUBGOAL_MP_TAC `({u | i <| u} UNION {m | m <=| i}) = UNIV`;
1027   REWRITE_TAC[num_SEG_UNION];
1028   DISCH_TAC;
1029   UND 0;
1030   ASM_REWRITE_TAC[];
1031   REWRITE_TAC[num_infinite];
1032   ]);;
1033   (* }}} *)
1034
1035 let INTER_FINITE = prove_by_refinement(
1036   `!s (t:A->bool). (FINITE s ==> FINITE(s INTER t)) /\ (FINITE t ==> FINITE (s INTER t))`,
1037   (* {{{ proof *)
1038
1039   [
1040   CONV_TAC (quant_right_CONV "t");
1041   CONV_TAC (quant_right_CONV "s");
1042   SUBCONJ_TAC;
1043   DISCH_ALL_TAC;
1044   SUBGOAL_MP_TAC `s INTER t SUBSET (s:A->bool)`;
1045   SET_TAC[];
1046   ASM_MESON_TAC[FINITE_SUBSET];
1047   MESON_TAC[INTER_COMM];
1048   ]);;
1049
1050   (* }}} *)
1051
1052 let num_above_finite = prove_by_refinement(
1053   `!i J. (FINITE (J INTER {u | (i <| u)})) ==> (FINITE J)`,
1054   (* {{{ proof *)
1055   [
1056   DISCH_ALL_TAC;
1057   SUBGOAL_MP_TAC `J = (J INTER {u | (i <| u)}) UNION (J INTER {m | m <=| i})`;
1058   REWRITE_TAC[GSYM UNION_OVER_INTER;num_SEG_UNION;INTER_UNIV];
1059   DISCH_TAC;
1060   ASM (ONCE_REWRITE_TAC)[];
1061   REWRITE_TAC[FINITE_UNION];
1062   ASM_REWRITE_TAC[];
1063   MP_TAC (SPEC `i:num` FINITE_NUMSEG_LE);
1064   REWRITE_TAC[INTER_FINITE];
1065   ]);;
1066   (* }}} *)
1067
1068 let SUBSET_SUC = prove_by_refinement(
1069   `!(f:num->A->bool). (!i. f i SUBSET f (SUC i)) ==> (! i j. ( i <=| j) ==> (f i SUBSET f j))`,
1070   (* {{{ proof *)
1071   [
1072   GEN_TAC;
1073   DISCH_TAC;
1074   REP_GEN_TAC;
1075   MP_TAC (prove( `?n. n = j -| i`,MESON_TAC[]));
1076   CONV_TAC (quant_left_CONV "n");
1077   SPEC_TAC (`i:num`,`i:num`);
1078   SPEC_TAC (`j:num`,`j:num`);
1079   REP 2(  CONV_TAC (quant_left_CONV "n"));
1080   INDUCT_TAC;
1081   REP_GEN_TAC;
1082   DISCH_ALL_TAC;
1083   JOIN 1 2;
1084   USE 1 (CONV_RULE REDUCE_CONV);
1085   ASM_REWRITE_TAC[SUBSET];
1086   REP_GEN_TAC;
1087   DISCH_TAC;
1088   SUBGOAL_MP_TAC `?j'. j = SUC j'`;
1089   DISJ_CASES_TAC (SPEC `j:num` num_CASES);
1090   UND 2;
1091   ASM_REWRITE_TAC[];
1092   REDUCE_TAC;
1093   ASM_REWRITE_TAC[];
1094   DISCH_THEN CHOOSE_TAC;
1095   ASM_REWRITE_TAC[];
1096   USE 0 (SPEC `j':num`);
1097   USE 1(SPECL [`j':num`;`i:num`]);
1098   DISCH_TAC;
1099   SUBGOAL_MP_TAC `(n = j'-|i)`;
1100   UND 2;
1101   ASM_REWRITE_TAC[];
1102   ARITH_TAC;
1103   DISCH_TAC;
1104   SUBGOAL_MP_TAC `(i<=| j')`;
1105   USE 2 (MATCH_MP(ARITH_RULE `(SUC n = j -| i) ==> (0 < j -| i)`));
1106   UND 2;
1107   ASM_REWRITE_TAC[];
1108   ARITH_TAC;
1109   UND 1;
1110   ASM_REWRITE_TAC [];
1111   DISCH_ALL_TAC;
1112   REWR 6;
1113   ASM_MESON_TAC[SUBSET_TRANS];
1114   ]);;
1115   (* }}} *)
1116
1117 let SUBSET_SUC2 = prove_by_refinement(
1118   `!(f:num->A->bool). (!i. f (SUC i) SUBSET (f i)) ==> (! i j. ( i <=| j) ==> (f j SUBSET f i))`,
1119   (* {{{ proof *)
1120   [
1121   GEN_TAC;
1122   DISCH_TAC;
1123   REP_GEN_TAC;
1124   MP_TAC (prove( `?n. n = j -| i`,MESON_TAC[]));
1125   CONV_TAC (quant_left_CONV "n");
1126   SPEC_TAC (`i:num`,`i:num`);
1127   SPEC_TAC (`j:num`,`j:num`);
1128   REP 2(  CONV_TAC (quant_left_CONV "n"));
1129   INDUCT_TAC;
1130   REP_GEN_TAC;
1131   DISCH_ALL_TAC;
1132   JOIN 1 2;
1133   USE 1 (CONV_RULE REDUCE_CONV);
1134   ASM_REWRITE_TAC[SUBSET];
1135   REP_GEN_TAC;
1136   DISCH_TAC;
1137   SUBGOAL_MP_TAC `?j'. j = SUC j'`;
1138   DISJ_CASES_TAC (SPEC `j:num` num_CASES);
1139   UND 2;
1140   ASM_REWRITE_TAC[];
1141   REDUCE_TAC;
1142   ASM_REWRITE_TAC[];
1143   DISCH_THEN CHOOSE_TAC;
1144   ASM_REWRITE_TAC[];
1145   USE 0 (SPEC `j':num`);
1146   USE 1(SPECL [`j':num`;`i:num`]);
1147   DISCH_TAC;
1148   SUBGOAL_MP_TAC `(n = j'-|i)`;
1149   UND 2;
1150   ASM_REWRITE_TAC[];
1151   ARITH_TAC;
1152   DISCH_TAC;
1153   SUBGOAL_MP_TAC `(i<=| j')`;
1154   USE 2 (MATCH_MP(ARITH_RULE `(SUC n = j -| i) ==> (0 < j -| i)`));
1155   UND 2;
1156   ASM_REWRITE_TAC[];
1157   ARITH_TAC;
1158   UND 1;
1159   ASM_REWRITE_TAC [];
1160   DISCH_ALL_TAC;
1161   REWR 6;
1162   ASM_MESON_TAC[SUBSET_TRANS];
1163   ]);;
1164   (* }}} *)
1165
1166 let INFINITE_PIGEONHOLE = prove_by_refinement(
1167   `!I (f:A->B) B C. (~(FINITE {i | (I i) /\ (C (f i))})) /\ (FINITE B) /\
1168     (C SUBSET (UNIONS B)) ==>
1169     (?b. (B b) /\ ~(FINITE {i | (I i) /\ (C INTER b) (f i) }))`,
1170   (* {{{ proof *)
1171   [
1172   DISCH_ALL_TAC;
1173   PROOF_BY_CONTR_TAC;
1174   USE 3 (  CONV_RULE (quant_left_CONV "b"));
1175   UND 0;
1176   TAUT_TAC `P ==> (~P ==> F)`;
1177   SUBGOAL_MP_TAC `{i | I' i /\ (C ((f:A->B) i))} = UNIONS (IMAGE (\b. {i | I' i /\ ((C INTER b) (f i))}) B)`;
1178   REWRITE_TAC[UNIONS;IN_IMAGE];
1179   MATCH_MP_TAC EQ_EXT;
1180   GEN_TAC;
1181   REWRITE_TAC[IN_ELIM_THM'];
1182   ABBREV_TAC `j = (x:A)`;
1183   EQ_TAC;
1184   DISCH_ALL_TAC;
1185   USE 2 (REWRITE_RULE [SUBSET;UNIONS]);
1186   USE 2 (REWRITE_RULE[IN_ELIM_THM']);
1187   USE 2 (SPEC `(f:A->B) j`);
1188   USE 2 (REWRITE_RULE[IN]);
1189   REWR 2;
1190   CHO 2;
1191   CONV_TAC (quant_left_CONV "x");
1192   CONV_TAC (quant_left_CONV "x");
1193   EXISTS_TAC (`u:B->bool`);
1194   NAME_CONFLICT_TAC;
1195   EXISTS_TAC (`{i' | I' i' /\ (C INTER u) ((f:A->B) i')}`);
1196   ASM_REWRITE_TAC[];
1197   REWRITE_TAC[IN_ELIM_THM';INTER];
1198   REWRITE_TAC[IN];
1199   ASM_REWRITE_TAC[];
1200   DISCH_TAC;
1201   CHO 4;
1202   AND 4;
1203   CHO 5;
1204   REWR 4;
1205   USE 4 (REWRITE_RULE[IN_ELIM_THM';INTER]);
1206   USE 4 (REWRITE_RULE[IN]);
1207   ASM_REWRITE_TAC[];
1208   DISCH_TAC;
1209   ASM_REWRITE_TAC[];
1210   SUBGOAL_MP_TAC `FINITE (IMAGE (\b. {i | I' i /\ (C INTER b) ((f:A->B) i)}) B)`;
1211   MATCH_MP_TAC FINITE_IMAGE;
1212   ASM_REWRITE_TAC[];
1213   SIMP_TAC[FINITE_UNIONS];
1214   DISCH_TAC;
1215   GEN_TAC;
1216   REWRITE_TAC[IN_IMAGE];
1217   DISCH_THEN (X_CHOOSE_TAC `b:B->bool`);
1218   ASM_REWRITE_TAC[];
1219   USE 3 (SPEC `b:B->bool`);
1220   UND 3;
1221   AND 5;
1222   UND 3;
1223   ABBREV_TAC `r = {i | I' i /\ (C INTER b) ((f:A->B) i)}`;
1224   MESON_TAC[IN];
1225   ]);;
1226   (* }}} *)
1227
1228 let real_FINITE = prove_by_refinement(
1229   `!(s:real->bool). FINITE s ==> (?a. !x. x IN s ==> (x <=. a))`,
1230   (* {{{ proof *)
1231   [
1232   DISCH_ALL_TAC;
1233   ASSUME_TAC REAL_ARCH_SIMPLE;
1234   USE 1 (CONV_RULE (quant_left_CONV "n"));
1235   CHO 1;
1236   SUBGOAL_MP_TAC `FINITE (IMAGE (n:real->num) s)`;
1237   ASM_MESON_TAC[FINITE_IMAGE];
1238 (*** JRH -- num_FINITE is now an equivalence not an implication
1239   ASSUME_TAC (SPEC `IMAGE (n:real->num) s` num_FINITE);
1240  ***)
1241   ASSUME_TAC(fst(EQ_IMP_RULE(SPEC `IMAGE (n:real->num) s` num_FINITE)));
1242   DISCH_TAC;
1243   REWR 2;
1244   CHO 2;
1245   USE 2 (REWRITE_RULE[IN_IMAGE]);
1246   USE 2 (CONV_RULE NAME_CONFLICT_CONV);
1247   EXISTS_TAC `&.a`;
1248   GEN_TAC;
1249   USE 2 (CONV_RULE (quant_left_CONV "x'"));
1250   USE 2 (CONV_RULE (quant_left_CONV "x'"));
1251   USE 2 (SPEC `x:real`);
1252   USE 2 (SPEC `(n:real->num) x`);
1253   DISCH_TAC;
1254   REWR 2;
1255   USE 1 (SPEC `x:real`);
1256   UND 1;
1257   MATCH_MP_TAC (REAL_ARITH `a<=b ==> ((x <= a) ==> (x <=. b))`);
1258   REDUCE_TAC;
1259   ASM_REWRITE_TAC [];
1260   ]);;
1261   (* }}} *)
1262
1263 let UNIONS_DELETE = prove_by_refinement(
1264   `!s. (UNIONS (s:(A->bool)->bool)) = (UNIONS (s DELETE (EMPTY)))`,
1265   (* {{{ proof *)
1266   [
1267   REWRITE_TAC[UNIONS;DELETE;EMPTY];
1268   GEN_TAC;
1269   MATCH_MP_TAC EQ_EXT;
1270   REWRITE_TAC[IN_ELIM_THM'];
1271   GEN_TAC;
1272   REWRITE_TAC[IN];
1273   MESON_TAC[];
1274   ]);;
1275   (* }}} *)
1276
1277
1278 (* ------------------------------------------------------------------ *)
1279 (* Partial functions, which we identify with functions that
1280    take the canonical choice of element outside the domain. *)
1281 (* ------------------------------------------------------------------ *)
1282
1283 let SUPP = new_definition
1284   `SUPP (f:A->B) = \ x.  ~(f x = (CHOICE (UNIV:B ->bool)) )`;;
1285
1286 let FUN = new_definition
1287   `FUN a b = (\ (f:A->B). ((!x. (x IN a) ==> (f x IN b)) /\
1288               ((SUPP f) SUBSET a))) `;;
1289
1290 (* ------------------------------------------------------------------ *)
1291 (* compositions *)
1292 (* ------------------------------------------------------------------ *)
1293
1294 let compose = new_definition
1295   `compose f g = \x. (f (g x))`;;
1296
1297 let COMP_ASSOC = prove_by_refinement(
1298    `!(f:num ->num) (g:num->num) (h:num->num).
1299       (compose f (compose g h)) = (compose (compose f g) h)`,
1300 (* {{{ proof *)
1301
1302    [
1303    REPEAT GEN_TAC THEN REWRITE_TAC[compose];
1304    ]);;
1305 (* }}} *)
1306
1307 let COMP_INJ = prove (`!(f:A->B) (g:B->C) s t u.
1308       INJ f s t /\ (INJ g t u) ==>
1309   (INJ (compose g f) s u)`,
1310 (* {{{ proof *)
1311
1312    EVERY[REPEAT GEN_TAC;
1313    REWRITE_TAC[INJ;compose];
1314    DISCH_ALL_TAC;
1315    ASM_MESON_TAC[]]);;
1316 (* }}} *)
1317
1318 let COMP_SURJ = prove (`!(f:A->B) (g:B->C) s t u.
1319    SURJ f s t /\ (SURJ g t u) ==> (SURJ (compose g f) s u)`,
1320 (* {{{ proof *)
1321
1322    EVERY[REWRITE_TAC[SURJ;compose];
1323    DISCH_ALL_TAC;
1324    ASM_MESON_TAC[]]);;
1325 (* }}} *)
1326
1327 let COMP_BIJ = prove (`!(f:A->B) s t (g:B->C) u.
1328     BIJ f s t /\ (BIJ g t u) ==> (BIJ (compose g f) s u)`,
1329 (* {{{ proof *)
1330
1331    EVERY[
1332    REPEAT GEN_TAC;
1333    REWRITE_TAC[BIJ];
1334    DISCH_ALL_TAC;
1335    ASM_MESON_TAC[COMP_INJ;COMP_SURJ]]);;
1336
1337 (* }}} *)
1338
1339
1340 (* ------------------------------------------------------------------ *)
1341 (* general construction of an inverse function on a domain *)
1342 (* ------------------------------------------------------------------ *)
1343
1344 let INVERSE_FN = prove_by_refinement(
1345   `?INVERSE. (! (f:A->B) a b. (SURJ f a b) ==> ((INJ (INVERSE f a b) b a) /\
1346        (!(x:B). (x IN b) ==> (f ((INVERSE f a b) x) = x))))`,
1347 (* {{{ proof *)
1348
1349   [
1350   REWRITE_TAC[GSYM SKOLEM_THM];
1351   REPEAT GEN_TAC;
1352   MATCH_MP_TAC (prove_by_refinement( `!A B. (A ==> (?x. (B x))) ==> (?(x:B->A). (A ==> (B x)))`,[MESON_TAC[]])) ;
1353   REWRITE_TAC[SURJ;INJ];
1354   DISCH_ALL_TAC;
1355   SUBGOAL_MP_TAC `?u. !y. ((y IN b)==> ((u y IN a) /\ ((f:A->B) (u y) = y)))`;
1356   REWRITE_TAC[GSYM SKOLEM_THM];
1357   GEN_TAC;
1358   ASM_MESON_TAC[];
1359   DISCH_THEN CHOOSE_TAC;
1360   EXISTS_TAC `u:B->A`;
1361   REPEAT CONJ_TAC;
1362   ASM_MESON_TAC[];
1363   REPEAT GEN_TAC;
1364   DISCH_ALL_TAC;
1365   FIRST_X_ASSUM (fun th -> ASSUME_TAC (AP_TERM `f:A->B` th));
1366   ASM_MESON_TAC[];
1367   ASM_MESON_TAC[]
1368   ]);;
1369
1370 (* }}} *)
1371
1372 let INVERSE_DEF = new_specification ["INVERSE"] INVERSE_FN;;
1373
1374 let INVERSE_BIJ = prove_by_refinement(
1375   `!(f:A->B) a b. (BIJ f a b) ==> ((BIJ (INVERSE f a b) b a))`,
1376 (* {{{ proof *)
1377   [
1378   REPEAT GEN_TAC;
1379   REWRITE_TAC[BIJ];
1380   DISCH_ALL_TAC;
1381   ASM_SIMP_TAC[INVERSE_DEF];
1382   REWRITE_TAC[SURJ];
1383   CONJ_TAC;
1384   ASM_MESON_TAC[INVERSE_DEF;INJ];
1385   GEN_TAC THEN DISCH_TAC;
1386   EXISTS_TAC `(f:A->B) x`;
1387   CONJ_TAC;
1388   ASM_MESON_TAC[INJ];
1389   SUBGOAL_THEN `((f:A->B) x) IN b` ASSUME_TAC;
1390   ASM_MESON_TAC[INJ];
1391   SUBGOAL_THEN `(f:A->B) (INVERSE f a b (f x)) = (f x)` ASSUME_TAC;
1392   ASM_MESON_TAC[INVERSE_DEF];
1393   H_UNDISCH_TAC (HYP "0");
1394   REWRITE_TAC[INJ];
1395   DISCH_ALL_TAC;
1396   FIRST_X_ASSUM (fun th -> MP_TAC (SPECL [`INVERSE (f:A->B) a b (f x)`;`x:A`] th));
1397   ASM_REWRITE_TAC[];
1398   DISCH_ALL_TAC;
1399   SUBGOAL_THEN `INVERSE (f:A->B) a b (f x) IN a` ASSUME_TAC;
1400   ASM_MESON_TAC[INVERSE_DEF;INJ];
1401   ASM_MESON_TAC[];
1402   ]);;
1403 (* }}} *)
1404
1405 let INVERSE_XY = prove_by_refinement(
1406   `!(f:A->B) a b x y. (BIJ f a b) /\ (x IN a) /\ (y IN b) ==> ((INVERSE f a b y = x) <=> (f x = y))`,
1407 (* {{{ proof *)
1408   [
1409   REPEAT GEN_TAC;
1410   DISCH_ALL_TAC;
1411   EQ_TAC;
1412   FIRST_X_ASSUM (fun th -> (ASSUME_TAC th THEN (ASSUME_TAC (MATCH_MP INVERSE_DEF (CONJUNCT2 (REWRITE_RULE[BIJ] th))))));
1413   ASM_MESON_TAC[];
1414   POP_ASSUM (fun th -> (ASSUME_TAC th THEN (ASSUME_TAC (CONJUNCT2 (REWRITE_RULE[INJ] (CONJUNCT1 (REWRITE_RULE[BIJ] th)))))));
1415   DISCH_THEN (fun th -> ASSUME_TAC th THEN (REWRITE_TAC[GSYM th]));
1416   FIRST_X_ASSUM  MATCH_MP_TAC;
1417   REPEAT CONJ_TAC;
1418   ASM_REWRITE_TAC[];
1419   IMP_RES_THEN ASSUME_TAC INVERSE_BIJ;
1420   ASM_MESON_TAC[BIJ;INJ];
1421   ASM_REWRITE_TAC[];
1422   FIRST_X_ASSUM (fun th -> (ASSUME_TAC (CONJUNCT2 (REWRITE_RULE[BIJ] th))));
1423   IMP_RES_THEN (fun th -> ASSUME_TAC (CONJUNCT2 th)) INVERSE_DEF;
1424   ASM_MESON_TAC[];
1425   ]);;
1426 (* }}} *)
1427
1428 let FINITE_BIJ = prove(
1429   `!a b (f:A->B). FINITE a /\ (BIJ f a b) ==> (FINITE b)`,
1430 (* {{{ proof *)
1431
1432   MESON_TAC[SURJ_IMAGE;BIJ;INJ;FINITE_IMAGE]
1433 );;
1434
1435 (* }}} *)
1436
1437 let FINITE_INJ = prove_by_refinement(
1438   `!a b (f:A->B). FINITE b /\ (INJ f a b) ==> (FINITE a)`,
1439 (* {{{ proof *)
1440
1441   [
1442   REPEAT GEN_TAC;
1443   DISCH_ALL_TAC;
1444   MP_TAC (SPECL [`f:A->B`;`b:B->bool`;`a:A->bool`] FINITE_IMAGE_INJ_GENERAL);
1445   DISCH_ALL_TAC;
1446   SUBGOAL_THEN `(a:A->bool) SUBSET ({x | (x IN a) /\ ((f:A->B) x IN b)})` ASSUME_TAC;
1447   REWRITE_TAC[SUBSET];
1448   GEN_TAC ;
1449   REWRITE_TAC[IN_ELIM_THM];
1450   POPL_TAC[0;1];
1451   ASM_MESON_TAC[BIJ;INJ];
1452   MATCH_MP_TAC FINITE_SUBSET;
1453   EXISTS_TAC `({x | (x IN a) /\ ((f:A->B) x IN b)})` ;
1454   CONJ_TAC;
1455   FIRST_X_ASSUM (fun th -> MATCH_MP_TAC th);
1456   CONJ_TAC;
1457   ASM_MESON_TAC[BIJ;INJ];
1458   ASM_REWRITE_TAC[];
1459   ASM_REWRITE_TAC[];
1460   ]
1461 );;
1462
1463 (* }}} *)
1464
1465 let FINITE_BIJ2 = prove_by_refinement(
1466   `!a b (f:A->B). FINITE b /\ (BIJ f a b) ==> (FINITE a)`,
1467 (* {{{ proof *)
1468
1469   [
1470   MESON_TAC[BIJ;FINITE_INJ]
1471   ]);;
1472 (* }}} *)
1473
1474 let BIJ_CARD = prove_by_refinement(
1475   `!a b (f:A->B). FINITE a /\ (BIJ f a b) ==> (CARD a = (CARD b))`,
1476 (* {{{ proof *)
1477
1478   [
1479   ASM_MESON_TAC[SURJ_IMAGE;BIJ;INJ;CARD_IMAGE_INJ];
1480   ]);;
1481
1482 (* }}} *)
1483
1484 let PAIR_LEMMA = prove_by_refinement(
1485    `!(x:num#num) i j. ((FST x = i) /\ (SND x = j)) <=> (x = (i,j))` ,
1486 (* {{{ proof *)
1487
1488    [
1489    MESON_TAC[FST;SND;PAIR];
1490    ]);;
1491 (* }}} *)
1492
1493 let CARD_SING = prove_by_refinement(
1494       `!(u:A->bool). (SING u ) ==> (CARD u = 1)`,
1495 (* {{{ proof *)
1496    [
1497    REWRITE_TAC[SING];
1498    GEN_TAC;
1499    DISCH_THEN (CHOOSE_TAC);
1500    ASM_REWRITE_TAC[];
1501    ASSUME_TAC FINITE_RULES;
1502    ASM_SIMP_TAC[CARD_CLAUSES;NOT_IN_EMPTY];
1503    ACCEPT_TAC (NUM_RED_CONV `SUC 0`)
1504    ]);;
1505 (* }}} *)
1506
1507 let FINITE_SING = prove_by_refinement(
1508     `!(x:A). FINITE ({x})`,
1509 (* {{{ proof *)
1510
1511     [
1512     MESON_TAC[FINITE_RULES]
1513     ]);;
1514 (* }}} *)
1515
1516 let NUM_INTRO = prove_by_refinement(
1517   `!f P.((!(n:num). !(g:A). (f g = n) ==> (P g)) ==> (!g. (P g)))`,
1518 (* {{{ proof *)
1519
1520   [
1521   REPEAT GEN_TAC;
1522   DISCH_ALL_TAC;
1523   GEN_TAC;
1524   H_VAL (SPECL [`(f:A->num) (g:A)`; `g:A`]) (HYP "0");
1525   ASM_MESON_TAC[];
1526   ]);;
1527 (* }}} *)
1528
1529
1530
1531 (* ------------------------------------------------------------------ *)
1532 (* Lemmas about the support of a function *)
1533 (* ------------------------------------------------------------------ *)
1534
1535
1536 (* Law of cardinal exponents B^0 = 1 *)
1537 let DOMAIN_EMPTY = prove_by_refinement(
1538   `!b. FUN (EMPTY:A->bool) b = { (\ (u:A). (CHOICE (UNIV:B->bool))) }`,
1539 (* {{{ proof *)
1540   [
1541   GEN_TAC;
1542   REWRITE_TAC[EXTENSION;FUN];
1543   X_GEN_TAC `f:A->B`;
1544   REWRITE_TAC[IN_ELIM_THM;INSERT;NOT_IN_EMPTY;SUBSET_EMPTY;SUPP];
1545   REWRITE_TAC[EMPTY];
1546   ONCE_REWRITE_TAC[EXTENSION];
1547   REWRITE_TAC[IN];
1548   EQ_TAC;
1549   DISCH_TAC THEN (MATCH_MP_TAC EQ_EXT);
1550   BETA_TAC;
1551   ASM_REWRITE_TAC[];
1552   DISCH_TAC THEN (ASM_REWRITE_TAC[]) THEN BETA_TAC;
1553   ]);;
1554 (* }}} *)
1555
1556 (* Law of cardinal exponents B^A * B = B^(A+1) *)
1557 let DOMAIN_INSERT = prove_by_refinement(
1558   `!a b s. (~((s:A) IN a) ==>
1559       (?F.   (BIJ F (FUN (s INSERT a) b)
1560            { (u,v) | (u IN (FUN a b)) /\ ((v:B) IN b) }
1561            )))`,
1562 (* {{{ proof *)
1563   [
1564   REPEAT GEN_TAC;
1565   DISCH_TAC;
1566   EXISTS_TAC  `\ f. ((\ x. (if (x=(s:A)) then (CHOICE (UNIV:B->bool)) else (f x))),(f s))`;
1567   REWRITE_TAC[BIJ;INJ;SURJ];
1568   TAUT_TAC `(A /\ (A ==> B) /\ (A ==>C))  ==> ((A/\ B) /\ (A /\ C))`;
1569   REPEAT CONJ_TAC;
1570   X_GEN_TAC `(f:A->B)`;
1571   REWRITE_TAC[FUN;IN_ELIM_THM];
1572   REWRITE_TAC[INSERT;SUBSET];
1573   REWRITE_TAC[IN_ELIM_THM;SUPP];
1574   STRIP_TAC;
1575   ABBREV_TAC `g = \ x. (if (x=(s:A)) then (CHOICE (UNIV:B->bool)) else (f x)) `;
1576   EXISTS_TAC `g:A->B`;
1577   EXISTS_TAC `(f:A->B) s`;
1578   REWRITE_TAC[];
1579   REPEAT CONJ_TAC;
1580   EXPAND_TAC "g" THEN BETA_TAC;
1581   GEN_TAC;
1582   REWRITE_TAC[IN;COND_ELIM_THM];
1583   ASM_MESON_TAC[IN];
1584   (* next *) ALL_TAC;
1585   EXPAND_TAC "g" THEN BETA_TAC;
1586   GEN_TAC;
1587   ASM_CASES_TAC `(x:A) = s`;
1588   ASM_REWRITE_TAC[];
1589   ASM_REWRITE_TAC[];
1590   ASM_MESON_TAC[];
1591   (* next *) ALL_TAC;
1592   ASM_MESON_TAC[];
1593   (* INJ *)  ALL_TAC;
1594   REWRITE_TAC[FUN;SUPP];
1595   DISCH_TAC;
1596   X_GEN_TAC `f1:A->B`;
1597   X_GEN_TAC `f2:A->B`;
1598   REWRITE_TAC[IN];
1599   DISCH_ALL_TAC;
1600   MATCH_MP_TAC EQ_EXT;
1601   GEN_TAC;
1602   ASM_CASES_TAC `(x:A) = s`;
1603   POPL_TAC[1;2;3;4;6;7];
1604   ASM_REWRITE_TAC[];
1605   ASM_MESON_TAC[PAIR;FST;SND];
1606   POPL_TAC[1;2;3;4;6;7];
1607   FIRST_X_ASSUM (fun th -> ASSUME_TAC (REWRITE_RULE[FST] (AP_TERM `FST:((A->B)#B)->(A->B)` th))) ;
1608   FIRST_X_ASSUM (fun th -> ASSUME_TAC (REWRITE_RULE[COND_ELIM_THM] (BETA_RULE (AP_THM th `x:A`))));
1609   LABEL_ALL_TAC;
1610   H_UNDISCH_TAC (HYP "0");
1611   COND_CASES_TAC;
1612   ASM_MESON_TAC[];
1613   ASM_MESON_TAC[];
1614   (* SURJ *) ALL_TAC;
1615   REWRITE_TAC[FUN;SUPP;IN_ELIM_THM];
1616   REWRITE_TAC[IN;INSERT;SUBSET];
1617   DISCH_ALL_TAC;
1618   X_GEN_TAC `p:(A->B)#B`;
1619   DISCH_THEN CHOOSE_TAC;
1620   FIRST_X_ASSUM (fun th -> MP_TAC th);
1621   DISCH_THEN CHOOSE_TAC;
1622   FIRST_X_ASSUM MP_TAC;
1623   DISCH_ALL_TAC;
1624   ASM_REWRITE_TAC[];
1625   EXISTS_TAC `\ (x:A). if (x = s) then (v:B) else (u x)`;
1626   REPEAT CONJ_TAC;
1627   X_GEN_TAC `t:A`;
1628   BETA_TAC;
1629   REWRITE_TAC[IN_ELIM_THM;COND_ELIM_THM];
1630   POPL_TAC[1;3;4;5];
1631   ASM_MESON_TAC[];
1632   X_GEN_TAC `t:A`;
1633   BETA_TAC;
1634   REWRITE_TAC[IN_ELIM_THM;COND_ELIM_THM];
1635   ASM_CASES_TAC `(t:A) = s`;
1636   POPL_TAC[1;3;4;5;6];
1637   ASM_REWRITE_TAC[];
1638   POPL_TAC[1;3;4;5;6];
1639   FIRST_X_ASSUM (fun th -> ASSUME_TAC (SPEC `t:A` th));
1640   ASM_SIMP_TAC[prove(`~((t:A)=s) ==> ((t=s)=F)`,MESON_TAC[])];
1641   BETA_TAC;
1642   REWRITE_TAC[];
1643   POPL_TAC[0;2;3;4];
1644   AP_THM_TAC;
1645   AP_TERM_TAC;
1646   MATCH_MP_TAC EQ_EXT;
1647   X_GEN_TAC `t:A`;
1648   BETA_TAC;
1649   DISJ_CASES_TAC (prove(`(((t:A)=s) <=> T) \/ ((t=s) <=> F)`,MESON_TAC[]));
1650   ASM_REWRITE_TAC[];
1651   ASM_MESON_TAC[IN];
1652   ASM_REWRITE_TAC[]
1653   ]);;
1654 (* }}} *)
1655
1656 let CARD_DELETE_CHOICE = prove_by_refinement(
1657   `!(a:(A->bool)). ((FINITE a) /\ (~(a=EMPTY))) ==>
1658    (SUC (CARD (a DELETE (CHOICE a))) = (CARD a))`,
1659 (* {{{ proof *)
1660   [
1661   REPEAT GEN_TAC;
1662   DISCH_ALL_TAC;
1663   ASM_SIMP_TAC[CARD_DELETE];
1664   ASM_SIMP_TAC[CHOICE_DEF];
1665   MATCH_MP_TAC (ARITH_RULE `~(x=0) ==> (SUC (x -| 1) = x)`);
1666   ASM_MESON_TAC[HAS_SIZE_0;HAS_SIZE];
1667   ]);;
1668 (* }}} *)
1669
1670
1671 (*
1672 let dets_flag = ref true;;
1673 dets_flag:= !labels_flag;;
1674 *)
1675
1676
1677 (* labels_flag:=false;; *)
1678
1679 (* Law of cardinals |B^A| = |B|^|A| *)
1680 let FUN_SIZE =
1681  Refinement.enhanced_prove_by_refinement false ALL_TAC (
1682   `!b a. (FINITE (a:A->bool)) /\ (FINITE (b:B->bool))
1683           ==> ((FUN a b) HAS_SIZE ((CARD b) EXP (CARD a)))`,
1684 (* {{{ proof *)
1685   [
1686   GEN_TAC;
1687   MATCH_MP_TAC (SPEC `CARD:(A->bool)->num` ((INST_TYPE) [`:A->bool`,`:A`]  NUM_INTRO));
1688   INDUCT_TAC;
1689   GEN_TAC;
1690   DISCH_ALL_TAC;
1691   ASM_REWRITE_TAC[];
1692   REWRITE_TAC [EXP];
1693   SUBGOAL_THEN `(a:A->bool) = EMPTY` ASSUME_TAC;
1694   ASM_REWRITE_TAC[GSYM HAS_SIZE_0;HAS_SIZE];
1695   ASM_REWRITE_TAC[HAS_SIZE;DOMAIN_EMPTY];
1696   CONJ_TAC;
1697   REWRITE_TAC[FINITE_SING];
1698   MATCH_MP_TAC CARD_SING;
1699   REWRITE_TAC[SING];
1700   MESON_TAC[];
1701   GEN_TAC;
1702   FIRST_X_ASSUM (fun th -> ASSUME_TAC (SPEC `(a:A->bool) DELETE (CHOICE a)` th)) ;
1703   DISCH_ALL_TAC;
1704   SUBGOAL_THEN `CARD ((a:A->bool) DELETE (CHOICE a)) = n` ASSUME_TAC;
1705   ASM_SIMP_TAC[CARD_DELETE];
1706   SUBGOAL_THEN `CHOICE (a:A->bool) IN a` ASSUME_TAC;
1707   MATCH_MP_TAC CHOICE_DEF;
1708   ASSUME_TAC( ARITH_RULE `!x. (x = (SUC n)) ==> (~(x = 0))`);
1709   REWRITE_TAC[GSYM HAS_SIZE_0;HAS_SIZE];
1710   ASM_MESON_TAC[];
1711   ASM_REWRITE_TAC[];
1712   MESON_TAC[ ( ARITH_RULE `!n. (SUC n -| 1) = n`)];
1713   LABEL_ALL_TAC;
1714   H_MATCH_MP (HYP "3") (HYP "4");
1715   SUBGOAL_THEN `FUN ((a:A->bool) DELETE CHOICE a) (b:B->bool) HAS_SIZE CARD b **| CARD (a DELETE CHOICE a)` ASSUME_TAC;
1716   ASM_MESON_TAC[FINITE_DELETE];
1717   ASSUME_TAC (SPECL [`((a:A->bool) DELETE (CHOICE a))`;`b:B->bool`;`(CHOICE (a:A->bool))` ] DOMAIN_INSERT);
1718   LABEL_ALL_TAC;
1719   H_UNDISCH_TAC (HYP "5");
1720   REWRITE_TAC[IN_DELETE];
1721   SUBGOAL_THEN `~((a:A->bool) = EMPTY)` ASSUME_TAC;
1722   REWRITE_TAC[GSYM HAS_SIZE_0;HAS_SIZE];
1723   ASSUME_TAC( ARITH_RULE `!x. (x = (SUC n)) ==> (~(x = 0))`);
1724   ASM_MESON_TAC[];
1725   ASM_SIMP_TAC[INSERT_DELETE;CHOICE_DEF];
1726   DISCH_THEN CHOOSE_TAC;
1727   REWRITE_TAC[HAS_SIZE];
1728   SUBGOAL_THEN `FINITE (FUN (a:A->bool) (b:B->bool))` ASSUME_TAC;
1729   (* CONJ_TAC; *) ALL_TAC;
1730   MATCH_MP_TAC (SPEC `FUN (a:A->bool) (b:B->bool)` (PINST[(`:A->B`,`:A`);(`:(A->B)#B`,`:B`)] [] FINITE_BIJ2));
1731   EXISTS_TAC `{u,v | (u:A->B) IN FUN (a DELETE CHOICE a) b /\ (v:B) IN b}`;
1732   EXISTS_TAC `F':(A->B)->((A->B)#B)`;
1733   ASM_REWRITE_TAC[];
1734   MATCH_MP_TAC FINITE_PRODUCT;
1735   ASM_REWRITE_TAC[];
1736   ASM_MESON_TAC[HAS_SIZE];
1737   ASM_REWRITE_TAC[];
1738   SUBGOAL_THEN `CARD (FUN (a:A->bool) (b:B->bool)) = (CARD {u,v | (u:A->B) IN FUN (a DELETE CHOICE a) b /\ (v:B) IN b})` ASSUME_TAC;
1739   MATCH_MP_TAC BIJ_CARD;
1740   EXISTS_TAC `F':(A->B)->((A->B)#B)`;
1741   ASM_REWRITE_TAC[];
1742   (* *) ALL_TAC;
1743   ASM_REWRITE_TAC[];
1744   SUBGOAL_THEN `FINITE (a DELETE CHOICE (a:A->bool))` ASSUME_TAC;
1745   ASM_MESON_TAC[FINITE_DELETE];
1746   SUBGOAL_THEN `(FUN ((a:A->bool) DELETE CHOICE a) (b:B->bool)) HAS_SIZE (CARD b **| (CARD (a DELETE CHOICE a)))` ASSUME_TAC;
1747   POPL_TAC[1;2;3;4;5;10;11];
1748   ASM_MESON_TAC[CARD_DELETE];
1749   POP_ASSUM (fun th -> ASSUME_TAC (REWRITE_RULE[HAS_SIZE] th) THEN (ASSUME_TAC th));
1750   ASM_SIMP_TAC[CARD_PRODUCT];
1751   REWRITE_TAC[EXP;MULT_AC]
1752   ]);;
1753 (* }}} *)
1754
1755 (* labels_flag:= true;; *)
1756
1757
1758 (* ------------------------------------------------------------------ *)
1759 (* ------------------------------------------------------------------ *)
1760
1761
1762
1763 (* Definitions in math tend to be n-tuples of data.  Let's make it
1764    easy to pick out the individual components of a definition *)
1765
1766 (* pick out the rest of n-tuples. Indexing consistent with lib.drop *)
1767 let drop0 = new_definition(`drop0 (u:A#B) = SND u`);;
1768 let drop1 = new_definition(`drop1 (u:A#B#C) = SND (SND u)`);;
1769 let drop2 = new_definition(`drop2 (u:A#B#C#D) = SND (SND (SND u))`);;
1770 let drop3 = new_definition(`drop3 (u:A#B#C#D#E) = SND (SND (SND (SND u)))`);;
1771
1772 (* pick out parts of n-tuples *)
1773
1774 let part0 = new_definition(`part0 (u:A#B) = FST u`);;
1775 let part1 = new_definition(`part1 (u:A#B#C) = FST (drop0 u)`);;
1776 let part2 = new_definition(`part2 (u:A#B#C#D) = FST (drop1 u)`);;
1777 let part3 = new_definition(`part3 (u:A#B#C#D#E) = FST (drop2 u)`);;
1778 let part4 = new_definition(`part4 (u:A#B#C#D#E#F) = FST (drop3 u)`);;
1779 let part5 = new_definition(`part5 (u:A#B#C#D#E#F#G) =
1780    FST (SND (SND (SND (SND (SND u)))))`);;
1781 let part6 = new_definition(`part6 (u:A#B#C#D#E#F#G#H) =
1782    FST (SND (SND (SND (SND (SND (SND u))))))`);;
1783 let part7 = new_definition(`part7 (u:A#B#C#D#E#F#G#H#I) =
1784    FST (SND (SND (SND (SND (SND (SND (SND u)))))))`);;
1785 let part8 = new_definition(`part8 (u:A#B#C#D#E#F#G#H#I#J) =
1786    FST (SND (SND (SND (SND (SND (SND (SND (SND u))))))))`);;
1787
1788
1789
1790 pop_priority();;
1791
1792 end;;