Jordan/misc_defs_and_lemmas.ml

   1
   2 labels_flag:= true;;
   3
   4 let dirac_delta = new_definition `dirac_delta (i:num) =
   5      (\j. if (i=j) then (&.1) else (&.0))`;;
   6
   7 let min_num = new_definition
   8   `min_num (X:num->bool) = @m. (m IN X) /\ (!n. (n IN X) ==> (m <= n))`;;
   9
  10 let min_least = prove_by_refinement (
  11   `!(X:num->bool) c. (X c) ==> (X (min_num X) /\ (min_num X <=| c))`,
  12   (* {{{ proof *)
  13
  14   [
  15   REWRITE_TAC[min_num;IN];
  16   REPEAT GEN_TAC;
  17   DISCH_TAC;
  18   SUBGOAL_THEN `?n. (X:num->bool) n /\ (!m. m <| n ==> ~X m)` MP_TAC;
  19     REWRITE_TAC[(GSYM (ISPEC `X:num->bool` num_WOP))];
  20     ASM_MESON_TAC[];
  21   DISCH_THEN CHOOSE_TAC;
  22   ASSUME_TAC (select_thm `\m. (X:num->bool) m /\ (!n. X n ==> m <=| n)` `n:num`);
  23   ABBREV_TAC `r = @m. (X:num->bool) m /\ (!n. X n ==> m <=| n)`;
  24   ASM_MESON_TAC[ ARITH_RULE `~(n' < n) ==> (n <=| n') `]
  25   ]);;
  26
  27   (* }}} *)
  28
  29 let max_real = new_definition(`max_real x y =
  30         if (y <. x) then x else y`);;
  31
  32 let min_real = new_definition(`min_real x y =
  33         if (x <. y) then x else y`);;
  34
  35 let deriv = new_definition(`deriv f x = @d. (f diffl d)(x)`);;
  36 let deriv2 = new_definition(`deriv2 f = (deriv (deriv f))`);;
  37
  38 let square_le = prove_by_refinement(
  39   `!x y. (&.0 <=. x) /\ (&.0 <=. y) /\ (x*.x <=. y*.y) ==> (x <=. y)`,
  40   (* {{{ proof *)
  41
  42   [
  43   DISCH_ALL_TAC;
  44   UNDISCH_FIND_TAC `( *. )` ;
  45   ONCE_REWRITE_TAC[REAL_ARITH `(a <=. b) <=> (&.0 <= (b - a))`];
  46   REWRITE_TAC[GSYM REAL_DIFFSQ];
  47   DISCH_TAC;
  48   DISJ_CASES_TAC (REAL_ARITH `&.0 < (y+x) \/ (y+x <=. (&.0))`);
  49   MATCH_MP_TAC (SPEC `(y+x):real` REAL_LE_LCANCEL_IMP);
  50   ASM_REWRITE_TAC [REAL_ARITH `x * (&.0) = (&.0)`];
  51   CLEAN_ASSUME_TAC (REAL_ARITH `(&.0 <= y) /\ (&.0 <=. x) /\ (y+x <= (&.0)) ==> ((x= &.0) /\ (y= &.0))`);
  52   ASM_REWRITE_TAC[REAL_ARITH `&.0 <=. (&.0 -. (&.0))`];
  53   ]);;
  54
  55   (* }}} *)
  56
  57 let max_num_sequence = prove_by_refinement(
  58   `!(t:num->num). (?n. !m. (n <=| m) ==> (t m = 0)) ==>
  59       (?M. !i. (t i <=| M))`,
  60   (* {{{ proof *)
  61   [
  62   GEN_TAC;
  63   REWRITE_TAC[GSYM LEFT_FORALL_IMP_THM];
  64   GEN_TAC;
  65   SPEC_TAC (`t:num->num`,`t:num->num`);
  66   SPEC_TAC (`n:num`,`n:num`);
  67   INDUCT_TAC;
  68   GEN_TAC;
  69   REWRITE_TAC[ARITH_RULE `0<=|m`];
  70   DISCH_TAC;
  71   EXISTS_TAC `0`;
  72   ASM_MESON_TAC[ARITH_RULE`(a=0) ==> (a <=|0)`];
  73   DISCH_ALL_TAC;
  74   ABBREV_TAC `b = \m. (if (m=n) then 0 else (t (m:num)) )`;
  75   FIRST_ASSUM (fun t-> ASSUME_TAC (SPEC `b:num->num` t));
  76   SUBGOAL_TAC `((b:num->num) (n) = 0) /\ (!m. ~(m=n) ==> (b m = t m))`;
  77   EXPAND_TAC "b";
  78   CONJ_TAC;
  79   COND_CASES_TAC;
  80   REWRITE_TAC[];
  81   ASM_MESON_TAC[];
  82   GEN_TAC;
  83   COND_CASES_TAC;
  84   REWRITE_TAC[];
  85   REWRITE_TAC[];
  86   DISCH_ALL_TAC;
  87   FIRST_ASSUM (fun t-> MP_TAC(SPEC `b:num->num` t));
  88   SUBGOAL_TAC `!m. (n<=|m) ==> (b m =0)`;
  89   GEN_TAC;
  90   ASM_CASES_TAC `m = (n:num)`;
  91   ASM_REWRITE_TAC[];
  92   SUBGOAL_TAC ( `(n <=| m) /\ (~(m = n)) ==> (SUC n <=| m)`);
  93   ARITH_TAC;
  94   ASM_REWRITE_TAC[];
  95   DISCH_ALL_TAC;
  96   ASM_MESON_TAC[]; (* good *)
  97   DISCH_THEN (fun t-> REWRITE_TAC[t]);
  98   DISCH_THEN CHOOSE_TAC;
  99   EXISTS_TAC `(M:num) + (t:num->num) n`;
 100   GEN_TAC;
 101   ASM_CASES_TAC `(i:num) = n`;
 102   ASM_REWRITE_TAC[];
 103   ARITH_TAC;
 104   MATCH_MP_TAC (ARITH_RULE `x <=| M ==> (x <=| M+ u)`);
 105   ASM_MESON_TAC[];
 106   ]);;
 107   (* }}} *)
 108
 109 let REAL_INV_LT = prove_by_refinement(
 110   `!x y z. (&.0 <. x) ==> ((inv(x)*y < z) <=> (y <. x*z))`,
 111   (* {{{ proof *)
 112   [
 113   REPEAT GEN_TAC;
 114   DISCH_TAC;
 115   REWRITE_TAC[REAL_ARITH `inv x * y = y* inv x`];
 116   REWRITE_TAC[GSYM real_div];
 117   ASM_SIMP_TAC[REAL_LT_LDIV_EQ];
 118   REAL_ARITH_TAC;
 119   ]);;
 120   (* }}} *)
 121
 122 let REAL_MUL_NN = prove_by_refinement(
 123   `!x y. (&.0 <= x*y) <=>
 124     ((&.0 <= x /\ (&.0 <=. y)) \/ ((x <= &.0) /\ (y <= &.0) ))`,
 125   (* {{{ proof *)
 126   [
 127   DISCH_ALL_TAC;
 128   SUBGOAL_TAC `! x y. ((&.0 < x) ==> ((&.0 <= x*y) <=> ((&.0 <= x /\ (&.0 <=. y)) \/ ((x <= &.0) /\ (y <= &.0) ))))`;
 129   DISCH_ALL_TAC;
 130   ASM_SIMP_TAC[REAL_ARITH `((&.0 <. x) ==> (&.0 <=. x))`;REAL_ARITH `(&.0 <. x) ==> ~(x <=. &.0)`];
 131   EQ_TAC;
 132   ASM_MESON_TAC[REAL_PROP_NN_LCANCEL];
 133   ASM_MESON_TAC[REAL_LE_MUL;REAL_LT_IMP_LE];
 134   DISCH_TAC;
 135   DISJ_CASES_TAC (REAL_ARITH `(&.0 < x) \/ (x = &.0) \/ (x < &.0)`);
 136   ASM_MESON_TAC[];
 137   UND 1 THEN DISCH_THEN  DISJ_CASES_TAC;
 138   ASM_REWRITE_TAC[];
 139   REAL_ARITH_TAC;
 140   ASM_SIMP_TAC[REAL_ARITH `((x <. &.0) ==> ~(&.0 <=. x))`;REAL_ARITH `(x <. &.0) ==> (x <=. &.0)`];
 141   USE 0 (SPECL [`--. (x:real)`;`--. (y:real)`]);
 142   UND 0;
 143   REDUCE_TAC;
 144   ASM_REWRITE_TAC[];
 145   ASM_SIMP_TAC[REAL_ARITH `((x <. &.0) ==> ~(&.0 <=. x))`;REAL_ARITH `(x <. &.0) ==> (x <=. &.0)`];
 146   ]);;
 147   (* }}} *)
 148
 149 let ABS_SQUARE = prove_by_refinement(
 150   `!t u. abs(t) <. u ==> t*t <. u*u`,
 151   (* {{{ proof *)
 152
 153   [
 154   REP_GEN_TAC;
 155   CONV_TAC (SUBS_CONV[SPEC `t:real` (REWRITE_RULE[POW_2] (GSYM REAL_POW2_ABS))]);
 156   ASSUME_TAC REAL_ABS_POS;
 157   USE 0 (SPEC `t:real`);
 158   ABBREV_TAC `(b:real) = (abs t)`;
 159   KILL 1;
 160   DISCH_ALL_TAC;
 161   MATCH_MP_TAC REAL_PROP_LT_LRMUL;
 162   ASM_REWRITE_TAC[];
 163   ]);;
 164
 165   (* }}} *)
 166
 167 let ABS_SQUARE_LE = prove_by_refinement(
 168   `!t u. abs(t) <=. u ==> t*t <=. u*u`,
 169   (* {{{ proof *)
 170
 171   [
 172   REP_GEN_TAC;
 173   CONV_TAC (SUBS_CONV[SPEC `t:real` (REWRITE_RULE[POW_2] (GSYM REAL_POW2_ABS))]);
 174   ASSUME_TAC REAL_ABS_POS;
 175   USE 0 (SPEC `t:real`);
 176   ABBREV_TAC `(b:real) = (abs t)`;
 177   KILL 1;
 178   DISCH_ALL_TAC;
 179   MATCH_MP_TAC REAL_PROP_LE_LRMUL;
 180   ASM_REWRITE_TAC[];
 181   ]);;
 182
 183   (* }}} *)
 184
 185 let twopow_eps = prove_by_refinement(
 186   `!R e. ?n. (&.0 <. R)/\ (&.0 <. e) ==> R*(twopow(--: (&:n))) <. e`,
 187   (* {{{ proof *)
 188
 189   [
 190   DISCH_ALL_TAC;
 191   REWRITE_TAC[TWOPOW_NEG]; (* cs6b *)
 192   ASSUME_TAC (prove(`!n. &.0 < &.2 pow n`,REDUCE_TAC THEN ARITH_TAC));
 193   ONCE_REWRITE_TAC[REAL_MUL_AC];
 194   ASM_SIMP_TAC[REAL_INV_LT];
 195   ASM_SIMP_TAC[GSYM REAL_LT_LDIV_EQ];
 196   CONV_TAC (quant_right_CONV "n");
 197   DISCH_ALL_TAC;
 198   ASSUME_TAC (SPEC `R/e` REAL_ARCH_SIMPLE);
 199   CHO 3;
 200   EXISTS_TAC `n:num`;
 201   UND 3;
 202   MESON_TAC[POW_2_LT;REAL_LET_TRANS];
 203   ]);;
 204
 205   (* }}} *)
 206
 207
 208 (* ------------------------------------------------------------------ *)
 209 (* finite products, in imitation of finite sums *)
 210 (* ------------------------------------------------------------------ *)
 211
 212 let prod_EXISTS = prove_by_refinement(
 213   `?prod. (!f n.  prod(n,0) f = &1) /\
 214          (!f m n. prod(n,SUC m) f = prod(n,m) f * f(n + m))`,
 215 (* {{{ proof *)
 216   [
 217   (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))` ;
 218   EXISTS_TAC `\(n,m) f. (sm:num->num->(num->real)->real) n m f`;
 219   CONV_TAC(DEPTH_CONV GEN_BETA_CONV) THEN ASM_REWRITE_TAC[]
 220   ]);;
 221 (* }}} *)
 222
 223 let prod_DEF = new_specification ["prod"] prod_EXISTS;;
 224
 225 let prod = prove
 226  (`!n m. (prod(n,0) f = &1) /\
 227    (prod(n,SUC m) f = prod(n,m) f * f(n + m))`,
 228 (* {{{ proof *)
 229   REWRITE_TAC[prod_DEF]);;
 230 (* }}} *)
 231
 232 let PROD_TWO = prove_by_refinement(
 233  `!f n p. prod(0,n) f * prod(n,p) f = prod(0,n + p) f`,
 234 (* {{{ proof *)
 235   [
 236   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[prod; REAL_MUL_RID; MULT_CLAUSES;ADD_0];
 237   REWRITE_TAC[ARITH_RULE `n+| (SUC p) = (SUC (n+|p))`;prod;ARITH_RULE `0+|n = n`];
 238   ASM_REWRITE_TAC[REAL_MUL_ASSOC];
 239 ]);;
 240 (* }}} *)
 241
 242
 243 let ABS_PROD = prove_by_refinement(
 244  `!f m n. abs(prod(m,n) f) = prod(m,n) (\n. abs(f n))`,
 245 (* {{{ proof *)
 246   [
 247   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC;
 248   REWRITE_TAC[prod];
 249   REAL_ARITH_TAC;
 250   ASM_REWRITE_TAC[prod;ABS_MUL]
 251   ]);;
 252 (* }}} *)
 253
 254 let PROD_EQ = prove_by_refinement
 255  (`!f g m n. (!r. m <= r /\ r < (n + m) ==> (f(r) = g(r)))
 256         ==> (prod(m,n) f = prod(m,n) g)`,
 257 (* {{{ proof *)
 258
 259   [
 260   GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[prod];
 261   REWRITE_TAC[prod];
 262   DISCH_THEN (fun th -> MP_TAC th THEN (MP_TAC (SPEC `m+|n` th)));
 263   REWRITE_TAC[ARITH_RULE `(m<=| (m+|n))/\ (m +| n <| (SUC n +| m))`];
 264   DISCH_ALL_TAC;
 265   ASM_REWRITE_TAC[];
 266   AP_THM_TAC THEN AP_TERM_TAC;
 267   FIRST_X_ASSUM MATCH_MP_TAC;
 268   GEN_TAC THEN DISCH_TAC;
 269   FIRST_X_ASSUM MATCH_MP_TAC;
 270   ASM_MESON_TAC[ARITH_RULE `r <| (n+| m) ==> (r <| (SUC n +| m))`]
 271   ]);;
 272
 273 (* }}} *)
 274
 275 let PROD_POS = prove_by_refinement
 276  (`!f. (!n. &0 <= f(n)) ==> !m n. &0 <= prod(m,n) f`,
 277 (* {{{ proof *)
 278
 279   [
 280   GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[prod];
 281   REAL_ARITH_TAC;
 282   ASM_MESON_TAC[REAL_LE_MUL]
 283   ]);;
 284 (* }}} *)
 285
 286 let PROD_POS_GEN = prove_by_refinement
 287  (`!f m n.
 288      (!n. m <= n ==> &0 <= f(n))
 289      ==> &0 <= prod(m,n) f`,
 290 (* {{{ proof *)
 291
 292   [
 293   REPEAT STRIP_TAC THEN SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN REWRITE_TAC[prod];
 294   REAL_ARITH_TAC;
 295   ASM_MESON_TAC[REAL_LE_MUL;ARITH_RULE `m <=| (m +| n)`]
 296   ]);;
 297 (* }}} *)
 298
 299
 300 let PROD_ABS = prove
 301  (`!f m n. abs(prod(m,n) (\m. abs(f m))) = prod(m,n) (\m. abs(f m))`,
 302 (* {{{ proof *)
 303   REWRITE_TAC[ABS_PROD;REAL_ARITH `||. (||. x) = (||. x)`]);;
 304 (* }}} *)
 305
 306 let PROD_ZERO = prove_by_refinement
 307  (`!f m n. (?p. (m <= p /\ (p < (n+| m)) /\ (f p = (&.0)))) ==>
 308          (prod(m,n) f = &0)`,
 309 (* {{{ proof *)
 310   [
 311   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN (REWRITE_TAC[prod]);
 312   ARITH_TAC;
 313   DISCH_THEN CHOOSE_TAC;
 314   ASM_CASES_TAC `p <| (n+| m)`;
 315   MATCH_MP_TAC (prove (`(x = (&.0)) ==> (x *. y = (&.0))`,(DISCH_THEN (fun th -> (REWRITE_TAC[th]))) THEN REAL_ARITH_TAC));
 316   FIRST_X_ASSUM MATCH_MP_TAC;
 317   ASM_MESON_TAC[];
 318   POP_ASSUM (fun th -> ASSUME_TAC (MATCH_MP (ARITH_RULE `(~(p <| (n+|m)) ==> ((p <| ((SUC n) +| m)) ==> (p = ((m +| n)))))`) th));
 319   MATCH_MP_TAC (prove (`(x = (&.0)) ==> (y *. x = (&.0))`,(DISCH_THEN (fun th -> (REWRITE_TAC[th]))) THEN REAL_ARITH_TAC));
 320   ASM_MESON_TAC[]
 321  ]);;
 322 (* }}} *)
 323
 324 let PROD_MUL = prove_by_refinement(
 325   `!f g m n. prod(m,n) (\n. f(n) * g(n)) = prod(m,n) f * prod(m,n) g`,
 326   (* {{{ proof *)
 327   [
 328   EVERY(replicate GEN_TAC 3) THEN INDUCT_TAC THEN ASM_REWRITE_TAC[prod];
 329   REAL_ARITH_TAC;
 330   REWRITE_TAC[REAL_MUL_AC];
 331   ]);;
 332   (* }}} *)
 333
 334 let PROD_CMUL = prove_by_refinement(
 335   `!f c m n. prod(m,n) (\n. c * f(n)) = (c **. n) * prod(m,n) f`,
 336   (* {{{ proof *)
 337   [
 338   EVERY(replicate GEN_TAC 3) THEN INDUCT_TAC THEN ASM_REWRITE_TAC[prod;pow];
 339   REAL_ARITH_TAC;
 340   REWRITE_TAC[REAL_MUL_AC];
 341   ]);;
 342   (* }}} *)
 343
 344 (* ------------------------------------------------------------------ *)
 345 (*  LEMMAS ABOUT SETS                                                 *)
 346 (* ------------------------------------------------------------------ *)
 347
 348 (* IN_ELIM_THM produces garbled results at times. I like this better: *)
 349
 350 (*** JRH replaced this with the "new" IN_ELIM_THM; see how it works.
 351
 352 let IN_ELIM_THM' = prove_by_refinement(
 353  `(!P. !x:A. x IN (GSPEC P) <=> P x) /\
 354    (!P. !x:A. x IN (\x. P x) <=> P x) /\
 355    (!P. !x:A. (GSPEC P) x <=> P x) /\
 356    (!P (x:A) (t:A). (\t. (?y:A. P y /\ (t = y))) x <=> P x)`,
 357   (* {{{ proof *)
 358   [
 359   REWRITE_TAC[IN; GSPEC];
 360   MESON_TAC[];
 361   ]);;
 362   (* }}} *)
 363
 364  ****)
 365
 366 let IN_ELIM_THM' = IN_ELIM_THM;;
 367
 368 let SURJ_IMAGE = prove_by_refinement(
 369   `!(f:A->B) a b. SURJ f a b ==> (b = (IMAGE f a))`,
 370 (* {{{ proof *)
 371
 372   [
 373   REPEAT GEN_TAC;
 374   REWRITE_TAC[SURJ;IMAGE];
 375   DISCH_ALL_TAC;
 376   REWRITE_TAC[EXTENSION];
 377   GEN_TAC;
 378   REWRITE_TAC[IN_ELIM_THM];
 379   ASM_MESON_TAC[]]
 380
 381 (* }}} *)
 382 );;
 383
 384
 385 let SURJ_FINITE = prove_by_refinement(
 386   `!a b (f:A->B). FINITE a /\ (SURJ f a b) ==> FINITE b`,
 387 (* {{{ *)
 388
 389   [
 390   ASM_MESON_TAC[SURJ_IMAGE;FINITE_IMAGE]
 391   ]);;
 392
 393 (* }}} *)
 394
 395 let BIJ_INVERSE = prove_by_refinement(
 396   `!a b (f:A->B). (SURJ f a b) ==> (?(g:B->A). (INJ g b a))`,
 397 (* {{{ proof *)
 398
 399   [
 400   REPEAT GEN_TAC;
 401   DISCH_ALL_TAC;
 402   SUBGOAL_THEN `!y. ?u. ((y IN b) ==> ((u IN a) /\ ((f:A->B) u = y)))` ASSUME_TAC;
 403   ASM_MESON_TAC[SURJ];
 404   LABEL_ALL_TAC;
 405   H_REWRITE_RULE[THM SKOLEM_THM] (HYP "1");
 406   LABEL_ALL_TAC;
 407   H_UNDISCH_TAC (HYP"2");
 408   DISCH_THEN CHOOSE_TAC;
 409   EXISTS_TAC `u:B->A`;
 410   REWRITE_TAC[INJ] THEN  CONJ_TAC THEN (ASM_MESON_TAC[])
 411   ]
 412
 413 (* }}} *)
 414 );;
 415
 416 (* complement of an intersection is a union of complements *)
 417 let UNIONS_INTERS = prove_by_refinement(
 418   `!(X:A->bool)  V.
 419      (X DIFF (INTERS V) = UNIONS (IMAGE ((DIFF) X) V))`,
 420 (* {{{ proof *)
 421
 422   [
 423   REPEAT GEN_TAC;
 424   MATCH_MP_TAC SUBSET_ANTISYM;
 425   CONJ_TAC;
 426   REWRITE_TAC[SUBSET;IMAGE;IN_ELIM_THM];
 427   X_GEN_TAC `c:A`;
 428   REWRITE_TAC[IN_DIFF;IN_INTERS;IN_UNIONS;NOT_FORALL_THM];
 429   DISCH_ALL_TAC;
 430   UNDISCH_FIND_THEN `(?)` CHOOSE_TAC;
 431   EXISTS_TAC `(X DIFF t):A->bool`;
 432   REWRITE_TAC[IN_ELIM_THM];
 433   CONJ_TAC;
 434   EXISTS_TAC `t:A->bool`;
 435   ASM_MESON_TAC[];
 436   REWRITE_TAC[IN_DIFF];
 437   ASM_MESON_TAC[];
 438   REWRITE_TAC[SUBSET;IMAGE;IN_ELIM_THM];
 439   X_GEN_TAC `c:A`;
 440   REWRITE_TAC[IN_DIFF;IN_UNIONS];
 441   DISCH_THEN CHOOSE_TAC;
 442   UNDISCH_FIND_TAC `(IN)`;
 443   REWRITE_TAC[IN_INTERS;IN_ELIM_THM];
 444   DISCH_ALL_TAC;
 445   UNDISCH_FIND_THEN `(?)` CHOOSE_TAC;
 446   CONJ_TAC;
 447   ASM_MESON_TAC[SUBSET_DIFF;SUBSET];
 448   REWRITE_TAC[NOT_FORALL_THM];
 449   EXISTS_TAC `x:A->bool`;
 450   ASM_MESON_TAC[IN_DIFF];
 451   ]);;
 452
 453 (* }}} *)
 454
 455 let INTERS_SUBSET = prove_by_refinement (
 456    `!X (A:A->bool).  (A IN X) ==> (INTERS X SUBSET A)`,
 457 (* {{{ *)
 458   [
 459   REPEAT GEN_TAC;
 460   REWRITE_TAC[SUBSET;IN_INTERS];
 461   MESON_TAC[IN];
 462   ]);;
 463 (* }}} *)
 464
 465 let sub_union = prove_by_refinement(
 466   `!X (U:(A->bool)->bool). (U X) ==> (X SUBSET (UNIONS U))`,
 467 (* {{{ *)
 468  [
 469  DISCH_ALL_TAC;
 470  REWRITE_TAC[SUBSET;IN_ELIM_THM;UNIONS];
 471  REWRITE_TAC[IN];
 472  DISCH_ALL_TAC;
 473  EXISTS_TAC `X:A->bool`;
 474  ASM_REWRITE_TAC[];
 475  ]);;
 476 (* }}} *)
 477
 478 let IMAGE_SURJ = prove_by_refinement(
 479  `!(f:A->B) a. SURJ f a (IMAGE f a)`,
 480 (* {{{ *)
 481  [
 482  REWRITE_TAC[SURJ;IMAGE;IN_ELIM_THM];
 483  MESON_TAC[IN];
 484  ]);;
 485 (* }}} *)
 486
 487 let SUBSET_PREIMAGE = prove_by_refinement(
 488   `!(f:A->B) X Y. (Y SUBSET (IMAGE f X)) ==>
 489     (?Z. (Z SUBSET X) /\ (Y = IMAGE f Z))`,
 490 (* {{{ proof *)
 491  [
 492  DISCH_ALL_TAC;
 493  EXISTS_TAC `{x | (x IN (X:A->bool))/\ (f x IN (Y:B->bool)) }`;
 494  CONJ_TAC;
 495  REWRITE_TAC[SUBSET;IN_ELIM_THM];
 496  MESON_TAC[];
 497  REWRITE_TAC[EXTENSION];
 498  X_GEN_TAC `y:B`;
 499  UNDISCH_FIND_TAC `(SUBSET)`;
 500  REWRITE_TAC[SUBSET;IN_IMAGE];
 501  REWRITE_TAC[IN_ELIM_THM];
 502  DISCH_THEN (fun t-> MP_TAC (SPEC `y:B` t));
 503  MESON_TAC[];
 504  ]);;
 505 (* }}} *)
 506
 507 let UNIONS_INTER = prove_by_refinement(
 508   `!(U:(A->bool)->bool) A. (((UNIONS U) INTER A) =
 509        (UNIONS (IMAGE ((INTER) A) U)))`,
 510  (* {{{ proof *)
 511  [
 512  REPEAT GEN_TAC;
 513  MATCH_MP_TAC (prove(`((C SUBSET (B:A->bool)) /\ (C SUBSET A) /\ ((A INTER B) SUBSET C)) ==> ((B INTER A) = C)`,SET_TAC[]));
 514  CONJ_TAC;
 515  REWRITE_TAC[SUBSET;UNIONS;IN_ELIM_THM];
 516  REWRITE_TAC[IN_IMAGE];
 517  SET_TAC[];
 518  REWRITE_TAC[SUBSET;UNIONS;IN_IMAGE];
 519  CONJ_TAC;
 520  REWRITE_TAC[IN_ELIM_THM];
 521  X_GEN_TAC `y:A`;
 522  DISCH_THEN CHOOSE_TAC;
 523  ASM_MESON_TAC[IN_INTER];
 524  REWRITE_TAC[IN_INTER];
 525  REWRITE_TAC[IN_ELIM_THM];
 526  X_GEN_TAC `y:A`;
 527  DISCH_ALL_TAC;
 528  UNDISCH_FIND_THEN `(?)` CHOOSE_TAC;
 529  EXISTS_TAC `A INTER (u:A->bool)`;
 530  ASM SET_TAC[];
 531  ]);;
 532 (* }}} *)
 533
 534 let UNIONS_SUBSET = prove_by_refinement(
 535  `!U (X:A->bool). (!A. (A IN U) ==> (A SUBSET X))  ==> (UNIONS U SUBSET X)`,
 536 (* {{{ *)
 537  [
 538  REPEAT GEN_TAC;
 539  SET_TAC[];
 540  ]);;
 541 (* }}} *)
 542
 543 let SUBSET_INTER = prove_by_refinement(
 544  `!X A (B:A->bool). (X SUBSET (A INTER B)) <=> (X SUBSET A) /\ (X SUBSET B)`,
 545 (* {{{ *)
 546  [
 547  REWRITE_TAC[SUBSET;INTER;IN_ELIM_THM];
 548  MESON_TAC[IN];
 549  ]);;
 550 (* }}} *)
 551
 552 let EMPTY_EXISTS = prove_by_refinement(
 553  `!X. ~(X = {}) <=> (? (u:A). (u IN X))`,
 554 (* {{{ *)
 555  [
 556  REWRITE_TAC[EXTENSION];
 557  REWRITE_TAC[IN;EMPTY];
 558  MESON_TAC[];
 559  ]);;
 560 (* }}} *)
 561
 562 let UNIONS_UNIONS = prove_by_refinement(
 563  `!A B. (A SUBSET B) ==>(UNIONS (A:(A->bool)->bool) SUBSET (UNIONS B))`,
 564 (* {{{ *)
 565  [
 566  REWRITE_TAC[SUBSET;UNIONS;IN_ELIM_THM];
 567  MESON_TAC[IN];
 568  ]);;
 569 (* }}} *)
 570
 571
 572 (* nested union can flatten from outside in, or inside out *)
 573 let UNIONS_IMAGE_UNIONS = prove_by_refinement(
 574   `!(X:((A->bool)->bool)->bool).
 575     UNIONS (UNIONS X) = (UNIONS (IMAGE UNIONS X))`,
 576  (* {{{ proof *)
 577   [
 578   GEN_TAC;
 579   REWRITE_TAC[EXTENSION;IN_UNIONS];
 580   GEN_TAC;
 581   REWRITE_TAC[EXTENSION;IN_UNIONS];
 582   EQ_TAC;
 583   DISCH_THEN (CHOOSE_THEN MP_TAC);
 584   DISCH_ALL_TAC;
 585   FIRST_ASSUM MP_TAC;
 586   DISCH_THEN CHOOSE_TAC;
 587   EXISTS_TAC `UNIONS (t':(A->bool)->bool)`;
 588   REWRITE_TAC[IN_UNIONS;IN_IMAGE];
 589   CONJ_TAC;
 590   EXISTS_TAC `(t':(A->bool)->bool)`;
 591   ASM_REWRITE_TAC[];
 592   ASM_MESON_TAC[];
 593   DISCH_THEN CHOOSE_TAC;
 594   FIRST_ASSUM MP_TAC;
 595   REWRITE_TAC[IN_IMAGE];
 596   DISCH_ALL_TAC;
 597   FIRST_ASSUM MP_TAC;
 598   DISCH_THEN CHOOSE_TAC;
 599   UNDISCH_TAC `(x:A) IN t`;
 600   FIRST_ASSUM (fun t-> REWRITE_TAC[t]);
 601   REWRITE_TAC[IN_UNIONS];
 602   DISCH_THEN (CHOOSE_TAC);
 603   EXISTS_TAC `t':(A->bool)`;
 604   CONJ_TAC;
 605   EXISTS_TAC `x':(A->bool)->bool`;
 606   ASM_REWRITE_TAC[];
 607   ASM_REWRITE_TAC[];
 608   ]);;
 609 (* }}} *)
 610
 611
 612 let INTERS_SUBSET2 = prove_by_refinement(
 613   `!X A. (?(x:A->bool). (A x /\ (x SUBSET X))) ==> ((INTERS A) SUBSET X)`,
 614   (* {{{ proof *)
 615   [
 616   REWRITE_TAC[SUBSET;INTERS;IN_ELIM_THM'];
 617   REWRITE_TAC[IN];
 618   MESON_TAC[];
 619   ]);;
 620   (* }}} *)
 621
 622 (**** New proof by JRH; old one breaks because of new set comprehensions
 623
 624 let INTERS_EMPTY = prove_by_refinement(
 625   `INTERS EMPTY = (UNIV:A->bool)`,
 626   (* {{{ proof *)
 627   [
 628   REWRITE_TAC[INTERS;NOT_IN_EMPTY;IN_ELIM_THM';];
 629   REWRITE_TAC[UNIV;GSPEC];
 630   MATCH_MP_TAC  EQ_EXT;
 631   GEN_TAC;
 632   REWRITE_TAC[IN_ELIM_THM'];
 633   MESON_TAC[];
 634   ]);;
 635   (* }}} *)
 636
 637  ****)
 638
 639 let INTERS_EMPTY = prove_by_refinement(
 640   `INTERS EMPTY = (UNIV:A->bool)`,
 641   [SET_TAC[]]);;
 642
 643 let preimage = new_definition `preimage dom (f:A->B)
 644   Z = {x | (x IN dom) /\ (f x IN Z)}`;;
 645
 646 let in_preimage = prove_by_refinement(
 647   `!f x Z dom. x IN (preimage dom (f:A->B) Z) <=> (x IN dom) /\ (f x IN Z)`,
 648 (* {{{ *)
 649   [
 650   REWRITE_TAC[preimage];
 651   REWRITE_TAC[IN_ELIM_THM']
 652   ]);;
 653 (* }}} *)
 654
 655 (* Partial functions, which we identify with functions that
 656    take the canonical choice of element outside the domain. *)
 657
 658 let supp = new_definition
 659   `supp (f:A->B) = \ x.  ~(f x = (CHOICE (UNIV:B ->bool)) )`;;
 660
 661 let func = new_definition
 662   `func a b = (\ (f:A->B). ((!x. (x IN a) ==> (f x IN b)) /\
 663               ((supp f) SUBSET a))) `;;
 664
 665
 666 (* relations *)
 667 let reflexive = new_definition
 668   `reflexive (f:A->A->bool) <=> (!x. f x x)`;;
 669
 670 let symmetric = new_definition
 671   `symmetric (f:A->A->bool) <=> (!x y. f x y ==> f y x)`;;
 672
 673 let transitive = new_definition
 674   `transitive (f:A->A->bool) <=> (!x y z. f x y /\ f y z ==> f x z)`;;
 675
 676 let equivalence_relation = new_definition
 677   `equivalence_relation (f:A->A->bool) <=>
 678     (reflexive f) /\ (symmetric f) /\ (transitive f)`;;
 679
 680 (* We do not introduce the equivalence class of f explicitly, because
 681    it is represented directly in HOL by (f a) *)
 682
 683 let partition_DEF = new_definition
 684   `partition (A:A->bool) SA <=> (UNIONS SA = A) /\
 685    (!a b. ((a IN SA) /\ (b IN SA) /\ (~(a = b)) ==> ({} = (a INTER b))))`;;
 686
 687 let DIFF_DIFF2 = prove_by_refinement(
 688   `!X (A:A->bool). (A SUBSET X) ==> ((X DIFF (X DIFF A)) = A)`,
 689   [
 690   SET_TAC[]
 691   ]);;
 692
 693 (*** Old proof replaced by JRH: no longer UNWIND_THM[12] clause in IN_ELIM_THM
 694
 695 let GSPEC_THM = prove_by_refinement(
 696   `!P (x:A). (?y. P y /\ (x = y)) <=> P x`,
 697   [REWRITE_TAC[IN_ELIM_THM]]);;
 698
 699 ***)
 700
 701 let GSPEC_THM = prove_by_refinement(
 702   `!P (x:A). (?y. P y /\ (x = y)) <=> P x`,
 703   [MESON_TAC[]]);;
 704
 705 let CARD_GE_REFL = prove
 706  (`!s:A->bool. s >=_c s`,
 707   GEN_TAC THEN REWRITE_TAC[GE_C] THEN
 708   EXISTS_TAC `\x:A. x` THEN MESON_TAC[]);;
 709
 710 let FINITE_HAS_SIZE_LEMMA = prove
 711  (`!s:A->bool. FINITE s ==> ?n:num. {x | x < n} >=_c s`,
 712   MATCH_MP_TAC FINITE_INDUCT THEN CONJ_TAC THENL
 713    [EXISTS_TAC `0` THEN REWRITE_TAC[NOT_IN_EMPTY; GE_C; IN_ELIM_THM];
 714     REPEAT GEN_TAC THEN DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN
 715     EXISTS_TAC `SUC N` THEN POP_ASSUM MP_TAC THEN PURE_REWRITE_TAC[GE_C] THEN
 716     DISCH_THEN(X_CHOOSE_TAC `f:num->A`) THEN
 717     EXISTS_TAC `\n:num. if n = N then x:A else f n` THEN
 718     X_GEN_TAC `y:A` THEN PURE_REWRITE_TAC[IN_INSERT] THEN
 719     DISCH_THEN(DISJ_CASES_THEN2 SUBST_ALL_TAC (ANTE_RES_THEN MP_TAC)) THENL
 720      [EXISTS_TAC `N:num` THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN ARITH_TAC;
 721       DISCH_THEN(X_CHOOSE_THEN `n:num` MP_TAC) THEN
 722       REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
 723       EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[] THEN
 724       UNDISCH_TAC `n:num < N` THEN COND_CASES_TAC THEN
 725       ASM_REWRITE_TAC[LT_REFL] THEN ARITH_TAC]]);;
 726
 727 let NUM_COUNTABLE = prove_by_refinement(
 728   `COUNTABLE (UNIV:num->bool)`,
 729   (* {{{ proof *)
 730
 731   [
 732   REWRITE_TAC[COUNTABLE;CARD_GE_REFL];
 733   ]);;
 734
 735   (* }}} *)
 736
 737 let NUM2_COUNTABLE = prove_by_refinement(
 738   `COUNTABLE {((x:num),(y:num)) | T}`,
 739   (* {{{ proof *)
 740   [
 741   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);
 742   REWRITE_TAC[COUNTABLE;GE_C;IN_ELIM_THM'];
 743   NAME_CONFLICT_TAC;
 744   EXISTS_TAC `fn:num -> (num#num)`;
 745   X_GEN_TAC `p:num#num`;
 746   REPEAT (DISCH_THEN (CHOOSE_THEN MP_TAC));
 747   DISCH_THEN (fun t->REWRITE_TAC[t]);
 748   REWRITE_TAC[IN_UNIV];
 749   SUBGOAL_TAC `?t. t = x'+|y'`;
 750   MESON_TAC[];
 751   SPEC_TAC (`x':num`,`a:num`);
 752   SPEC_TAC (`y':num`,`b:num`);
 753   CONV_TAC (quant_left_CONV "t");
 754   CONV_TAC (quant_left_CONV "t");
 755   CONV_TAC (quant_left_CONV "t");
 756   INDUCT_TAC;
 757   REDUCE_TAC;
 758   REP_GEN_TAC;
 759   DISCH_THEN (fun t -> REWRITE_TAC[t]);
 760   EXISTS_TAC `0`;
 761   ASM_REWRITE_TAC[];
 762   CONV_TAC (quant_left_CONV "a");
 763   INDUCT_TAC;
 764   REDUCE_TAC;
 765   GEN_TAC;
 766   USE 1 (SPECL [`0`;`t:num`]);
 767   UND 1 THEN REDUCE_TAC;
 768   DISCH_THEN (X_CHOOSE_TAC `n:num`);
 769   AND 0;
 770   USE 0 (SPEC `n:num`);
 771   UND 0;
 772   UND 1;
 773   DISCH_THEN (fun t-> REWRITE_TAC[GSYM t]);
 774   CONV_TAC (ONCE_DEPTH_CONV GEN_BETA_CONV);
 775   BETA_TAC;
 776   REDUCE_TAC;
 777   DISCH_ALL_TAC;
 778   EXISTS_TAC `SUC n`;
 779   EXPAND_TAC "b";
 780   KILL 0;
 781   ASM_REWRITE_TAC[];
 782   REWRITE_TAC [ARITH_RULE `SUC t = t+|1`];
 783   GEN_TAC;
 784   ABBREV_TAC `t'  = SUC t`;
 785   USE 2 (SPEC `SUC b`);
 786   DISCH_TAC;
 787   UND 2;
 788   ASM_REWRITE_TAC[];
 789   REWRITE_TAC[ARITH_RULE `SUC a +| b = a +| SUC b`];
 790   DISCH_THEN (X_CHOOSE_TAC `n:num`);
 791   EXISTS_TAC `SUC n`;
 792   AND 0;
 793   USE 0 (SPEC `n:num`);
 794   UND 0;
 795   UND 2;
 796   DISCH_THEN (fun t->REWRITE_TAC[GSYM t]);
 797   CONV_TAC (ONCE_DEPTH_CONV GEN_BETA_CONV);
 798   BETA_TAC;
 799   REDUCE_TAC;
 800   DISCH_THEN (fun t->REWRITE_TAC[t]);
 801   REWRITE_TAC[ARITH_RULE `SUC a = a+| 1`];
 802   ]);;
 803   (* }}} *)
 804
 805 let COUNTABLE_UNIONS = prove_by_refinement(
 806   `!A:(A->bool)->bool. (COUNTABLE A) /\
 807       (!a. (a IN A) ==> (COUNTABLE a)) ==> (COUNTABLE (UNIONS A))`,
 808   (* {{{ proof *)
 809   [
 810   GEN_TAC;
 811   DISCH_ALL_TAC;
 812   USE 0 (REWRITE_RULE[COUNTABLE;GE_C;IN_UNIV]);
 813   CHO 0;
 814   USE 0 (CONV_RULE (quant_left_CONV "x"));
 815   USE 0 (CONV_RULE (quant_left_CONV "x"));
 816   CHO 0;
 817   USE 1 (REWRITE_RULE[COUNTABLE;GE_C;IN_UNIV]);
 818   USE 1 (CONV_RULE (quant_left_CONV "f"));
 819   USE 1 (CONV_RULE (quant_left_CONV "f"));
 820   UND 1;
 821   DISCH_THEN (X_CHOOSE_TAC `g:(A->bool)->num->A`);
 822   SUBGOAL_TAC `!a y. (a IN (A:(A->bool)->bool)) /\ (y IN a) ==> (? (u:num) (v:num). ( a = f u) /\ (y = g a v))`;
 823   REP_GEN_TAC;
 824   DISCH_ALL_TAC;
 825   USE 1 (SPEC `a:A->bool`);
 826   USE 0 (SPEC `a:A->bool`);
 827   EXISTS_TAC `(x:(A->bool)->num) a`;
 828   ASM_SIMP_TAC[];
 829   ASSUME_TAC NUM2_COUNTABLE;
 830   USE 2 (REWRITE_RULE[COUNTABLE;GE_C;IN_ELIM_THM';IN_UNIV]);
 831   USE 2 (CONV_RULE NAME_CONFLICT_CONV);
 832   UND 2 THEN (DISCH_THEN (X_CHOOSE_TAC `h:num->(num#num)`));
 833   DISCH_TAC;
 834   REWRITE_TAC[COUNTABLE;GE_C;IN_ELIM_THM';IN_UNIV;IN_UNIONS];
 835   EXISTS_TAC `(\p. (g:(A->bool)->num->A) ((f:num->(A->bool)) (FST ((h:num->(num#num)) p))) (SND (h p)))`;
 836   BETA_TAC;
 837   GEN_TAC;
 838   DISCH_THEN (CHOOSE_THEN MP_TAC);
 839   DISCH_ALL_TAC;
 840   USE 3 (SPEC `t:A->bool`);
 841   USE 3 (SPEC `y:A`);
 842   UND 3 THEN (ASM_REWRITE_TAC[]);
 843   REPEAT (DISCH_THEN(CHOOSE_THEN (MP_TAC)));
 844   DISCH_ALL_TAC;
 845   USE 2 (SPEC `(u:num,v:num)`);
 846   SUBGOAL_TAC `?x' y'. (u:num,v:num) = (x',y')`;
 847   MESON_TAC[];
 848   DISCH_TAC;
 849   UND 2;
 850   ASM_REWRITE_TAC[];
 851   DISCH_THEN (CHOOSE_THEN (ASSUME_TAC o GSYM));
 852   EXISTS_TAC `x':num`;
 853   ASM_REWRITE_TAC[];
 854   ]);;
 855   (* }}} *)
 856
 857 let COUNTABLE_IMAGE = prove_by_refinement(
 858   `!(A:A->bool) (B:B->bool) . (COUNTABLE A) /\ (?f. (B SUBSET IMAGE f A)) ==>
 859         (COUNTABLE B)`,
 860   (* {{{ proof *)
 861   [
 862   REWRITE_TAC[COUNTABLE;GE_C;IN_UNIV;IN_ELIM_THM';SUBSET];
 863   DISCH_ALL_TAC;
 864   CHO 0;
 865   USE 1 (REWRITE_RULE[IMAGE;IN_ELIM_THM']);
 866   CHO 1;
 867   USE 1 (REWRITE_RULE[IN_ELIM_THM']);
 868   USE 1 (CONV_RULE NAME_CONFLICT_CONV);
 869   EXISTS_TAC `(f':A->B) o (f:num->A)`;
 870   REWRITE_TAC[o_DEF];
 871   DISCH_ALL_TAC;
 872   USE 1 (SPEC `y:B`);
 873   UND 1;
 874   ASM_REWRITE_TAC[];
 875   DISCH_THEN CHOOSE_TAC;
 876   USE 0 (SPEC `x':A`);
 877   UND 0 THEN (ASM_REWRITE_TAC[]) THEN DISCH_TAC;
 878   ASM_MESON_TAC[];
 879   ]);;
 880   (* }}} *)
 881
 882 let COUNTABLE_CARD = prove_by_refinement(
 883   `!(A:A->bool) (B:B->bool). (COUNTABLE A) /\ (A >=_c B) ==>
 884      (COUNTABLE B)`,
 885   (* {{{ proof *)
 886
 887   [
 888   DISCH_ALL_TAC;
 889   MATCH_MP_TAC COUNTABLE_IMAGE;
 890   EXISTS_TAC `A:A->bool`;
 891   ASM_REWRITE_TAC[];
 892   REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM'];
 893   USE 1 (REWRITE_RULE[GE_C]);
 894   CHO 1;
 895   EXISTS_TAC `f:A->B`;
 896   ASM_REWRITE_TAC[];
 897   ]);;
 898
 899   (* }}} *)
 900
 901 let COUNTABLE_NUMSEG = prove_by_refinement(
 902   `!n. COUNTABLE {x | x <| n}`,
 903   (* {{{ proof *)
 904   [
 905   GEN_TAC;
 906   REWRITE_TAC[COUNTABLE;GE_C;IN_UNIV];
 907   EXISTS_TAC `I:num->num`;
 908   REDUCE_TAC;
 909   REWRITE_TAC[IN_ELIM_THM'];
 910   MESON_TAC[];
 911   ]);;
 912   (* }}} *)
 913
 914 let FINITE_COUNTABLE = prove_by_refinement(
 915   `!(A:A->bool). (FINITE A) ==> (COUNTABLE A)`,
 916   (* {{{ proof *)
 917   [
 918   DISCH_ALL_TAC;
 919   USE 0 (MATCH_MP FINITE_HAS_SIZE_LEMMA);
 920   CHO 0;
 921   ASSUME_TAC(SPEC `n:num` COUNTABLE_NUMSEG);
 922   JOIN 1 0;
 923   USE 0 (MATCH_MP COUNTABLE_CARD);
 924   ASM_REWRITE_TAC[];
 925   ]);;
 926   (* }}} *)
 927
 928 let num_infinite = prove_by_refinement(
 929   `~ (FINITE (UNIV:num->bool))`,
 930   (* {{{ proof *)
 931   [
 932   PROOF_BY_CONTR_TAC;
 933   USE 0 (REWRITE_RULE[]);
 934   USE 0 (MATCH_MP num_FINITE_AVOID);
 935   USE 0 (REWRITE_RULE[IN_UNIV]);
 936   ASM_REWRITE_TAC[];
 937   ]);;
 938   (* }}} *)
 939
 940 let num_SEG_UNION = prove_by_refinement(
 941   `!i. ({u | i <| u} UNION {m | m <=| i}) = UNIV`,
 942   (* {{{ proof *)
 943   [
 944   REP_BASIC_TAC;
 945   SUBGOAL_TAC `({u | i <| u} UNION {m | m <=| i}) = UNIV`;
 946   MATCH_MP_TAC EQ_EXT;
 947   GEN_TAC;
 948   REWRITE_TAC[UNIV;UNION;IN_ELIM_THM'];
 949   ARITH_TAC;
 950   REWRITE_TAC[];
 951   ]);;
 952   (* }}} *)
 953
 954 let num_above_infinite = prove_by_refinement(
 955   `!i. ~ (FINITE {u | i <| u})`,
 956   (* {{{ proof *)
 957   [
 958   GEN_TAC;
 959   PROOF_BY_CONTR_TAC;
 960   USE 0 (REWRITE_RULE[]);
 961   ASSUME_TAC(SPEC `i:num` FINITE_NUMSEG_LE);
 962   JOIN 0 1;
 963   USE 0 (MATCH_MP FINITE_UNION_IMP);
 964   SUBGOAL_TAC `({u | i <| u} UNION {m | m <=| i}) = UNIV`;
 965   REWRITE_TAC[num_SEG_UNION];
 966   DISCH_TAC;
 967   UND 0;
 968   ASM_REWRITE_TAC[];
 969   REWRITE_TAC[num_infinite];
 970   ]);;
 971   (* }}} *)
 972
 973 let INTER_FINITE = prove_by_refinement(
 974   `!s (t:A->bool). (FINITE s ==> FINITE(s INTER t)) /\ (FINITE t ==> FINITE (s INTER t))`,
 975   (* {{{ proof *)
 976
 977   [
 978   CONV_TAC (quant_right_CONV "t");
 979   CONV_TAC (quant_right_CONV "s");
 980   SUBCONJ_TAC;
 981   DISCH_ALL_TAC;
 982   SUBGOAL_TAC `s INTER t SUBSET (s:A->bool)`;
 983   SET_TAC[];
 984   ASM_MESON_TAC[FINITE_SUBSET];
 985   MESON_TAC[INTER_COMM];
 986   ]);;
 987
 988   (* }}} *)
 989
 990 let num_above_finite = prove_by_refinement(
 991   `!i J. (FINITE (J INTER {u | (i <| u)})) ==> (FINITE J)`,
 992   (* {{{ proof *)
 993   [
 994   DISCH_ALL_TAC;
 995   SUBGOAL_TAC `J = (J INTER {u | (i <| u)}) UNION (J INTER {m | m <=| i})`;
 996   REWRITE_TAC[GSYM UNION_OVER_INTER;num_SEG_UNION;INTER_UNIV];
 997   DISCH_TAC;
 998   ASM (ONCE_REWRITE_TAC)[];
 999   REWRITE_TAC[FINITE_UNION];
1000   ASM_REWRITE_TAC[];
1001   MP_TAC (SPEC `i:num` FINITE_NUMSEG_LE);
1002   REWRITE_TAC[INTER_FINITE];
1003   ]);;
1004   (* }}} *)
1005
1006 let SUBSET_SUC = prove_by_refinement(
1007   `!(f:num->A->bool). (!i. f i SUBSET f (SUC i)) ==> (! i j. ( i <=| j) ==> (f i SUBSET f j))`,
1008   (* {{{ proof *)
1009   [
1010   GEN_TAC;
1011   DISCH_TAC;
1012   REP_GEN_TAC;
1013   MP_TAC (prove( `?n. n = j -| i`,MESON_TAC[]));
1014   CONV_TAC (quant_left_CONV "n");
1015   SPEC_TAC (`i:num`,`i:num`);
1016   SPEC_TAC (`j:num`,`j:num`);
1017   REP 2(  CONV_TAC (quant_left_CONV "n"));
1018   INDUCT_TAC;
1019   REP_GEN_TAC;
1020   DISCH_ALL_TAC;
1021   JOIN 1 2;
1022   USE 1 (CONV_RULE REDUCE_CONV);
1023   ASM_REWRITE_TAC[SUBSET];
1024   REP_GEN_TAC;
1025   DISCH_TAC;
1026   SUBGOAL_TAC `?j'. j = SUC j'`;
1027   DISJ_CASES_TAC (SPEC `j:num` num_CASES);
1028   UND 2;
1029   ASM_REWRITE_TAC[];
1030   REDUCE_TAC;
1031   ASM_REWRITE_TAC[];
1032   DISCH_THEN CHOOSE_TAC;
1033   ASM_REWRITE_TAC[];
1034   USE 0 (SPEC `j':num`);
1035   USE 1(SPECL [`j':num`;`i:num`]);
1036   DISCH_TAC;
1037   SUBGOAL_TAC `(n = j'-|i)`;
1038   UND 2;
1039   ASM_REWRITE_TAC[];
1040   ARITH_TAC;
1041   DISCH_TAC;
1042   SUBGOAL_TAC `(i<=| j')`;
1043   USE 2 (MATCH_MP(ARITH_RULE `(SUC n = j -| i) ==> (0 < j -| i)`));
1044   UND 2;
1045   ASM_REWRITE_TAC[];
1046   ARITH_TAC;
1047   UND 1;
1048   ASM_REWRITE_TAC [];
1049   DISCH_ALL_TAC;
1050   REWR 6;
1051   ASM_MESON_TAC[SUBSET_TRANS];
1052   ]);;
1053   (* }}} *)
1054
1055 let SUBSET_SUC2 = prove_by_refinement(
1056   `!(f:num->A->bool). (!i. f (SUC i) SUBSET (f i)) ==> (! i j. ( i <=| j) ==> (f j SUBSET f i))`,
1057   (* {{{ proof *)
1058   [
1059   GEN_TAC;
1060   DISCH_TAC;
1061   REP_GEN_TAC;
1062   MP_TAC (prove( `?n. n = j -| i`,MESON_TAC[]));
1063   CONV_TAC (quant_left_CONV "n");
1064   SPEC_TAC (`i:num`,`i:num`);
1065   SPEC_TAC (`j:num`,`j:num`);
1066   REP 2(  CONV_TAC (quant_left_CONV "n"));
1067   INDUCT_TAC;
1068   REP_GEN_TAC;
1069   DISCH_ALL_TAC;
1070   JOIN 1 2;
1071   USE 1 (CONV_RULE REDUCE_CONV);
1072   ASM_REWRITE_TAC[SUBSET];
1073   REP_GEN_TAC;
1074   DISCH_TAC;
1075   SUBGOAL_TAC `?j'. j = SUC j'`;
1076   DISJ_CASES_TAC (SPEC `j:num` num_CASES);
1077   UND 2;
1078   ASM_REWRITE_TAC[];
1079   REDUCE_TAC;
1080   ASM_REWRITE_TAC[];
1081   DISCH_THEN CHOOSE_TAC;
1082   ASM_REWRITE_TAC[];
1083   USE 0 (SPEC `j':num`);
1084   USE 1(SPECL [`j':num`;`i:num`]);
1085   DISCH_TAC;
1086   SUBGOAL_TAC `(n = j'-|i)`;
1087   UND 2;
1088   ASM_REWRITE_TAC[];
1089   ARITH_TAC;
1090   DISCH_TAC;
1091   SUBGOAL_TAC `(i<=| j')`;
1092   USE 2 (MATCH_MP(ARITH_RULE `(SUC n = j -| i) ==> (0 < j -| i)`));
1093   UND 2;
1094   ASM_REWRITE_TAC[];
1095   ARITH_TAC;
1096   UND 1;
1097   ASM_REWRITE_TAC [];
1098   DISCH_ALL_TAC;
1099   REWR 6;
1100   ASM_MESON_TAC[SUBSET_TRANS];
1101   ]);;
1102   (* }}} *)
1103
1104 let INFINITE_PIGEONHOLE = prove_by_refinement(
1105   `!I (f:A->B) B C. (~(FINITE {i | (I i) /\ (C (f i))})) /\ (FINITE B) /\
1106     (C SUBSET (UNIONS B)) ==>
1107     (?b. (B b) /\ ~(FINITE {i | (I i) /\ (C INTER b) (f i) }))`,
1108   (* {{{ proof *)
1109   [
1110   DISCH_ALL_TAC;
1111   PROOF_BY_CONTR_TAC;
1112   USE 3 (  CONV_RULE (quant_left_CONV "b"));
1113   UND 0;
1114   TAUT_TAC `P ==> (~P ==> F)`;
1115   SUBGOAL_TAC `{i | I' i /\ (C ((f:A->B) i))} = UNIONS (IMAGE (\b. {i | I' i /\ ((C INTER b) (f i))}) B)`;
1116   REWRITE_TAC[UNIONS;IN_IMAGE];
1117   MATCH_MP_TAC EQ_EXT;
1118   GEN_TAC;
1119   REWRITE_TAC[IN_ELIM_THM'];
1120   ABBREV_TAC `j = (x:A)`;
1121   EQ_TAC;
1122   DISCH_ALL_TAC;
1123   USE 2 (REWRITE_RULE [SUBSET;UNIONS]);
1124   USE 2 (REWRITE_RULE[IN_ELIM_THM']);
1125   USE 2 (SPEC `(f:A->B) j`);
1126   USE 2 (REWRITE_RULE[IN]);
1127   REWR 2;
1128   CHO 2;
1129   CONV_TAC (quant_left_CONV "x");
1130   CONV_TAC (quant_left_CONV "x");
1131   EXISTS_TAC (`u:B->bool`);
1132   NAME_CONFLICT_TAC;
1133   EXISTS_TAC (`{i' | I' i' /\ (C INTER u) ((f:A->B) i')}`);
1134   ASM_REWRITE_TAC[];
1135   REWRITE_TAC[IN_ELIM_THM';INTER];
1136   REWRITE_TAC[IN];
1137   ASM_REWRITE_TAC[];
1138   DISCH_TAC;
1139   CHO 4;
1140   AND 4;
1141   CHO 5;
1142   REWR 4;
1143   USE 4 (REWRITE_RULE[IN_ELIM_THM';INTER]);
1144   USE 4 (REWRITE_RULE[IN]);
1145   ASM_REWRITE_TAC[];
1146   DISCH_TAC;
1147   ASM_REWRITE_TAC[];
1148   SUBGOAL_TAC `FINITE (IMAGE (\b. {i | I' i /\ (C INTER b) ((f:A->B) i)}) B)`;
1149   MATCH_MP_TAC FINITE_IMAGE;
1150   ASM_REWRITE_TAC[];
1151   SIMP_TAC[FINITE_UNIONS];
1152   DISCH_TAC;
1153   GEN_TAC;
1154   REWRITE_TAC[IN_IMAGE];
1155   DISCH_THEN (X_CHOOSE_TAC `b:B->bool`);
1156   ASM_REWRITE_TAC[];
1157   USE 3 (SPEC `b:B->bool`);
1158   UND 3;
1159   AND 5;
1160   UND 3;
1161   ABBREV_TAC `r = {i | I' i /\ (C INTER b) ((f:A->B) i)}`;
1162   MESON_TAC[IN];
1163   ]);;
1164   (* }}} *)
1165
1166 let real_FINITE = prove_by_refinement(
1167   `!(s:real->bool). FINITE s ==> (?a. !x. x IN s ==> (x <=. a))`,
1168   (* {{{ proof *)
1169   [
1170   DISCH_ALL_TAC;
1171   ASSUME_TAC REAL_ARCH_SIMPLE;
1172   USE 1 (CONV_RULE (quant_left_CONV "n"));
1173   CHO 1;
1174   SUBGOAL_TAC `FINITE (IMAGE (n:real->num) s)`;
1175   ASM_MESON_TAC[FINITE_IMAGE];
1176 (*** JRH -- num_FINITE is now an equivalence not an implication
1177   ASSUME_TAC (SPEC `IMAGE (n:real->num) s` num_FINITE);
1178  ***)
1179   ASSUME_TAC(fst(EQ_IMP_RULE(SPEC `IMAGE (n:real->num) s` num_FINITE)));
1180   DISCH_TAC;
1181   REWR 2;
1182   CHO 2;
1183   USE 2 (REWRITE_RULE[IN_IMAGE]);
1184   USE 2 (CONV_RULE NAME_CONFLICT_CONV);
1185   EXISTS_TAC `&.a`;
1186   GEN_TAC;
1187   USE 2 (CONV_RULE (quant_left_CONV "x'"));
1188   USE 2 (CONV_RULE (quant_left_CONV "x'"));
1189   USE 2 (SPEC `x:real`);
1190   USE 2 (SPEC `(n:real->num) x`);
1191   DISCH_TAC;
1192   REWR 2;
1193   USE 1 (SPEC `x:real`);
1194   UND 1;
1195   MATCH_MP_TAC (REAL_ARITH `a<=b ==> ((x <= a) ==> (x <=. b))`);
1196   REDUCE_TAC;
1197   ASM_REWRITE_TAC [];
1198   ]);;
1199   (* }}} *)
1200
1201 let UNIONS_DELETE = prove_by_refinement(
1202   `!s. (UNIONS (s:(A->bool)->bool)) = (UNIONS (s DELETE (EMPTY)))`,
1203   (* {{{ proof *)
1204   [
1205   REWRITE_TAC[UNIONS;DELETE;EMPTY];
1206   GEN_TAC;
1207   MATCH_MP_TAC EQ_EXT;
1208   REWRITE_TAC[IN_ELIM_THM'];
1209   GEN_TAC;
1210   REWRITE_TAC[IN];
1211   MESON_TAC[];
1212   ]);;
1213   (* }}} *)
1214
1215
1216 (* ------------------------------------------------------------------ *)
1217 (* Partial functions, which we identify with functions that
1218    take the canonical choice of element outside the domain. *)
1219 (* ------------------------------------------------------------------ *)
1220
1221 let SUPP = new_definition
1222   `SUPP (f:A->B) = \ x.  ~(f x = (CHOICE (UNIV:B ->bool)) )`;;
1223
1224 let FUN = new_definition
1225   `FUN a b = (\ (f:A->B). ((!x. (x IN a) ==> (f x IN b)) /\
1226               ((SUPP f) SUBSET a))) `;;
1227
1228 (* ------------------------------------------------------------------ *)
1229 (* compositions *)
1230 (* ------------------------------------------------------------------ *)
1231
1232 let compose = new_definition
1233   `compose f g = \x. (f (g x))`;;
1234
1235 let COMP_ASSOC = prove_by_refinement(
1236    `!(f:num ->num) (g:num->num) (h:num->num).
1237       (compose f (compose g h)) = (compose (compose f g) h)`,
1238 (* {{{ proof *)
1239
1240    [
1241    REPEAT GEN_TAC THEN REWRITE_TAC[compose];
1242    ]);;
1243 (* }}} *)
1244
1245 let COMP_INJ = prove (`!(f:A->B) (g:B->C) s t u.
1246       INJ f s t /\ (INJ g t u) ==>
1247   (INJ (compose g f) s u)`,
1248 (* {{{ proof *)
1249
1250    EVERY[REPEAT GEN_TAC;
1251    REWRITE_TAC[INJ;compose];
1252    DISCH_ALL_TAC;
1253    ASM_MESON_TAC[]]);;
1254 (* }}} *)
1255
1256 let COMP_SURJ = prove (`!(f:A->B) (g:B->C) s t u.
1257    SURJ f s t /\ (SURJ g t u) ==> (SURJ (compose g f) s u)`,
1258 (* {{{ proof *)
1259
1260    EVERY[REWRITE_TAC[SURJ;compose];
1261    DISCH_ALL_TAC;
1262    ASM_MESON_TAC[]]);;
1263 (* }}} *)
1264
1265 let COMP_BIJ = prove (`!(f:A->B) s t (g:B->C) u.
1266     BIJ f s t /\ (BIJ g t u) ==> (BIJ (compose g f) s u)`,
1267 (* {{{ proof *)
1268
1269    EVERY[
1270    REPEAT GEN_TAC;
1271    REWRITE_TAC[BIJ];
1272    DISCH_ALL_TAC;
1273    ASM_MESON_TAC[COMP_INJ;COMP_SURJ]]);;
1274
1275 (* }}} *)
1276
1277
1278 (* ------------------------------------------------------------------ *)
1279 (* general construction of an inverse function on a domain *)
1280 (* ------------------------------------------------------------------ *)
1281
1282 let INVERSE_FN = prove_by_refinement(
1283   `?INV. (! (f:A->B) a b. (SURJ f a b) ==> ((INJ (INV f a b) b a) /\
1284        (!(x:B). (x IN b) ==> (f ((INV f a b) x) = x))))`,
1285 (* {{{ proof *)
1286
1287   [
1288   REWRITE_TAC[GSYM SKOLEM_THM];
1289   REPEAT GEN_TAC;
1290   MATCH_MP_TAC (prove_by_refinement( `!A B. (A ==> (?x. (B x))) ==> (?(x:B->A). (A ==> (B x)))`,[MESON_TAC[]])) ;
1291   REWRITE_TAC[SURJ;INJ];
1292   DISCH_ALL_TAC;
1293   SUBGOAL_TAC `?u. !y. ((y IN b)==> ((u y IN a) /\ ((f:A->B) (u y) = y)))`;
1294   REWRITE_TAC[GSYM SKOLEM_THM];
1295   GEN_TAC;
1296   ASM_MESON_TAC[];
1297   DISCH_THEN CHOOSE_TAC;
1298   EXISTS_TAC `u:B->A`;
1299   REPEAT CONJ_TAC;
1300   ASM_MESON_TAC[];
1301   REPEAT GEN_TAC;
1302   DISCH_ALL_TAC;
1303   FIRST_X_ASSUM (fun th -> ASSUME_TAC (AP_TERM `f:A->B` th));
1304   ASM_MESON_TAC[];
1305   ASM_MESON_TAC[]
1306   ]);;
1307
1308 (* }}} *)
1309
1310 let INVERSE_DEF = new_specification ["INV"] INVERSE_FN;;
1311
1312 let INVERSE_BIJ = prove_by_refinement(
1313   `!(f:A->B) a b. (BIJ f a b) ==> ((BIJ (INV f a b) b a))`,
1314 (* {{{ proof *)
1315   [
1316   REPEAT GEN_TAC;
1317   REWRITE_TAC[BIJ];
1318   DISCH_ALL_TAC;
1319   ASM_SIMP_TAC[INVERSE_DEF];
1320   REWRITE_TAC[SURJ];
1321   CONJ_TAC;
1322   ASM_MESON_TAC[INVERSE_DEF;INJ];
1323   GEN_TAC THEN DISCH_TAC;
1324   EXISTS_TAC `(f:A->B) x`;
1325   CONJ_TAC;
1326   ASM_MESON_TAC[INJ];
1327   SUBGOAL_THEN `((f:A->B) x) IN b` ASSUME_TAC;
1328   ASM_MESON_TAC[INJ];
1329   SUBGOAL_THEN `(f:A->B) (INV f a b (f x)) = (f x)` ASSUME_TAC;
1330   ASM_MESON_TAC[INVERSE_DEF];
1331   H_UNDISCH_TAC (HYP "0");
1332   REWRITE_TAC[INJ];
1333   DISCH_ALL_TAC;
1334   FIRST_X_ASSUM (fun th -> MP_TAC (SPECL [`INV (f:A->B) a b (f x)`;`x:A`] th));
1335   ASM_REWRITE_TAC[];
1336   DISCH_ALL_TAC;
1337   SUBGOAL_THEN `INV (f:A->B) a b (f x) IN a` ASSUME_TAC;
1338   ASM_MESON_TAC[INVERSE_DEF;INJ];
1339   ASM_MESON_TAC[];
1340   ]);;
1341 (* }}} *)
1342
1343 let INVERSE_XY = prove_by_refinement(
1344   `!(f:A->B) a b x y. (BIJ f a b) /\ (x IN a) /\ (y IN b) ==> ((INV f a b y = x) <=> (f x = y))`,
1345 (* {{{ proof *)
1346   [
1347   REPEAT GEN_TAC;
1348   DISCH_ALL_TAC;
1349   EQ_TAC;
1350   FIRST_X_ASSUM (fun th -> (ASSUME_TAC th THEN (ASSUME_TAC (MATCH_MP INVERSE_DEF (CONJUNCT2 (REWRITE_RULE[BIJ] th))))));
1351   ASM_MESON_TAC[];
1352   POP_ASSUM (fun th -> (ASSUME_TAC th THEN (ASSUME_TAC (CONJUNCT2 (REWRITE_RULE[INJ] (CONJUNCT1 (REWRITE_RULE[BIJ] th)))))));
1353   DISCH_THEN (fun th -> ASSUME_TAC th THEN (REWRITE_TAC[GSYM th]));
1354   FIRST_X_ASSUM  MATCH_MP_TAC;
1355   REPEAT CONJ_TAC;
1356   ASM_REWRITE_TAC[];
1357   IMP_RES_THEN ASSUME_TAC INVERSE_BIJ;
1358   ASM_MESON_TAC[BIJ;INJ];
1359   ASM_REWRITE_TAC[];
1360   FIRST_X_ASSUM (fun th -> (ASSUME_TAC (CONJUNCT2 (REWRITE_RULE[BIJ] th))));
1361   IMP_RES_THEN (fun th -> ASSUME_TAC (CONJUNCT2 th)) INVERSE_DEF;
1362   ASM_MESON_TAC[];
1363   ]);;
1364 (* }}} *)
1365
1366 let FINITE_BIJ = prove(
1367   `!a b (f:A->B). FINITE a /\ (BIJ f a b) ==> (FINITE b)`,
1368 (* {{{ proof *)
1369
1370   MESON_TAC[SURJ_IMAGE;BIJ;INJ;FINITE_IMAGE]
1371 );;
1372
1373 (* }}} *)
1374
1375 let FINITE_INJ = prove_by_refinement(
1376   `!a b (f:A->B). FINITE b /\ (INJ f a b) ==> (FINITE a)`,
1377 (* {{{ proof *)
1378
1379   [
1380   REPEAT GEN_TAC;
1381   DISCH_ALL_TAC;
1382   MP_TAC (SPECL [`f:A->B`;`b:B->bool`;`a:A->bool`] FINITE_IMAGE_INJ_GENERAL);
1383   DISCH_ALL_TAC;
1384   SUBGOAL_THEN `(a:A->bool) SUBSET ({x | (x IN a) /\ ((f:A->B) x IN b)})` ASSUME_TAC;
1385   REWRITE_TAC[SUBSET];
1386   GEN_TAC ;
1387   REWRITE_TAC[IN_ELIM_THM];
1388   POPL_TAC[0;1];
1389   ASM_MESON_TAC[BIJ;INJ];
1390   MATCH_MP_TAC FINITE_SUBSET;
1391   EXISTS_TAC `({x | (x IN a) /\ ((f:A->B) x IN b)})` ;
1392   CONJ_TAC;
1393   FIRST_X_ASSUM (fun th -> MATCH_MP_TAC th);
1394   CONJ_TAC;
1395   ASM_MESON_TAC[BIJ;INJ];
1396   ASM_REWRITE_TAC[];
1397   ASM_REWRITE_TAC[];
1398   ]
1399 );;
1400
1401 (* }}} *)
1402
1403 let FINITE_BIJ2 = prove_by_refinement(
1404   `!a b (f:A->B). FINITE b /\ (BIJ f a b) ==> (FINITE a)`,
1405 (* {{{ proof *)
1406
1407   [
1408   MESON_TAC[BIJ;FINITE_INJ]
1409   ]);;
1410 (* }}} *)
1411
1412 let BIJ_CARD = prove_by_refinement(
1413   `!a b (f:A->B). FINITE a /\ (BIJ f a b) ==> (CARD a = (CARD b))`,
1414 (* {{{ proof *)
1415
1416   [
1417   ASM_MESON_TAC[SURJ_IMAGE;BIJ;INJ;CARD_IMAGE_INJ];
1418   ]);;
1419
1420 (* }}} *)
1421
1422 let PAIR_LEMMA = prove_by_refinement(
1423    `!(x:num#num) i j. ((FST x = i) /\ (SND x = j)) <=> (x = (i,j))` ,
1424 (* {{{ proof *)
1425
1426    [
1427    MESON_TAC[FST;SND;PAIR];
1428    ]);;
1429 (* }}} *)
1430
1431 let CARD_SING = prove_by_refinement(
1432       `!(u:A->bool). (SING u ) ==> (CARD u = 1)`,
1433 (* {{{ proof *)
1434    [
1435    REWRITE_TAC[SING];
1436    GEN_TAC;
1437    DISCH_THEN (CHOOSE_TAC);
1438    ASM_REWRITE_TAC[];
1439    ASSUME_TAC FINITE_RULES;
1440    ASM_SIMP_TAC[CARD_CLAUSES;NOT_IN_EMPTY];
1441    ACCEPT_TAC (NUM_RED_CONV `SUC 0`)
1442    ]);;
1443 (* }}} *)
1444
1445 let FINITE_SING = prove_by_refinement(
1446     `!(x:A). FINITE ({x})`,
1447 (* {{{ proof *)
1448
1449     [
1450     MESON_TAC[FINITE_RULES]
1451     ]);;
1452 (* }}} *)
1453
1454 let NUM_INTRO = prove_by_refinement(
1455   `!f P.((!(n:num). !(g:A). (f g = n) ==> (P g)) ==> (!g. (P g)))`,
1456 (* {{{ proof *)
1457
1458   [
1459   REPEAT GEN_TAC;
1460   DISCH_ALL_TAC;
1461   GEN_TAC;
1462   H_VAL (SPECL [`(f:A->num) (g:A)`; `g:A`]) (HYP "0");
1463   ASM_MESON_TAC[];
1464   ]);;
1465 (* }}} *)
1466
1467
1468
1469 (* ------------------------------------------------------------------ *)
1470 (* Lemmas about the support of a function *)
1471 (* ------------------------------------------------------------------ *)
1472
1473
1474 (* Law of cardinal exponents B^0 = 1 *)
1475 let DOMAIN_EMPTY = prove_by_refinement(
1476   `!b. FUN (EMPTY:A->bool) b = { (\ (u:A). (CHOICE (UNIV:B->bool))) }`,
1477 (* {{{ proof *)
1478   [
1479   GEN_TAC;
1480   REWRITE_TAC[EXTENSION;FUN];
1481   X_GEN_TAC `f:A->B`;
1482   REWRITE_TAC[IN_ELIM_THM;INSERT;NOT_IN_EMPTY;SUBSET_EMPTY;SUPP];
1483   REWRITE_TAC[EMPTY];
1484   ONCE_REWRITE_TAC[EXTENSION];
1485   REWRITE_TAC[IN];
1486   EQ_TAC;
1487   DISCH_TAC THEN (MATCH_MP_TAC EQ_EXT);
1488   BETA_TAC;
1489   ASM_REWRITE_TAC[];
1490   DISCH_TAC THEN (ASM_REWRITE_TAC[]) THEN BETA_TAC;
1491   ]);;
1492 (* }}} *)
1493
1494 (* Law of cardinal exponents B^A * B = B^(A+1) *)
1495 let DOMAIN_INSERT = prove_by_refinement(
1496   `!a b s. (~((s:A) IN a) ==>
1497       (?F.   (BIJ F (FUN (s INSERT a) b)
1498            { (u,v) | (u IN (FUN a b)) /\ ((v:B) IN b) }
1499            )))`,
1500 (* {{{ proof *)
1501   [
1502   REPEAT GEN_TAC;
1503   DISCH_TAC;
1504   EXISTS_TAC  `\ f. ((\ x. (if (x=(s:A)) then (CHOICE (UNIV:B->bool)) else (f x))),(f s))`;
1505   REWRITE_TAC[BIJ;INJ;SURJ];
1506   TAUT_TAC `(A /\ (A ==> B) /\ (A ==>C))  ==> ((A/\ B) /\ (A /\ C))`;
1507   REPEAT CONJ_TAC;
1508   X_GEN_TAC `(f:A->B)`;
1509   REWRITE_TAC[FUN;IN_ELIM_THM];
1510   REWRITE_TAC[INSERT;SUBSET];
1511   REWRITE_TAC[IN_ELIM_THM;SUPP];
1512   STRIP_TAC;
1513   ABBREV_TAC `g = \ x. (if (x=(s:A)) then (CHOICE (UNIV:B->bool)) else (f x)) `;
1514   EXISTS_TAC `g:A->B`;
1515   EXISTS_TAC `(f:A->B) s`;
1516   REWRITE_TAC[];
1517   REPEAT CONJ_TAC;
1518   EXPAND_TAC "g" THEN BETA_TAC;
1519   GEN_TAC;
1520   REWRITE_TAC[IN;COND_ELIM_THM];
1521   ASM_MESON_TAC[IN];
1522   (* next *) ALL_TAC;
1523   EXPAND_TAC "g" THEN BETA_TAC;
1524   GEN_TAC;
1525   ASM_CASES_TAC `(x:A) = s`;
1526   ASM_REWRITE_TAC[];
1527   ASM_REWRITE_TAC[];
1528   ASM_MESON_TAC[];
1529   (* next *) ALL_TAC;
1530   ASM_MESON_TAC[];
1531   (* INJ *)  ALL_TAC;
1532   REWRITE_TAC[FUN;SUPP];
1533   DISCH_TAC;
1534   X_GEN_TAC `f1:A->B`;
1535   X_GEN_TAC `f2:A->B`;
1536   REWRITE_TAC[IN];
1537   DISCH_ALL_TAC;
1538   MATCH_MP_TAC EQ_EXT;
1539   GEN_TAC;
1540   ASM_CASES_TAC `(x:A) = s`;
1541   POPL_TAC[1;2;3;4;6;7];
1542   ASM_REWRITE_TAC[];
1543   ASM_MESON_TAC[PAIR;FST;SND];
1544   POPL_TAC[1;2;3;4;6;7];
1545   FIRST_X_ASSUM (fun th -> ASSUME_TAC (REWRITE_RULE[FST] (AP_TERM `FST:((A->B)#B)->(A->B)` th))) ;
1546   FIRST_X_ASSUM (fun th -> ASSUME_TAC (REWRITE_RULE[COND_ELIM_THM] (BETA_RULE (AP_THM th `x:A`))));
1547   LABEL_ALL_TAC;
1548   H_UNDISCH_TAC (HYP "0");
1549   COND_CASES_TAC;
1550   ASM_MESON_TAC[];
1551   ASM_MESON_TAC[];
1552   (* SURJ *) ALL_TAC;
1553   REWRITE_TAC[FUN;SUPP;IN_ELIM_THM];
1554   REWRITE_TAC[IN;INSERT;SUBSET];
1555   DISCH_ALL_TAC;
1556   X_GEN_TAC `p:(A->B)#B`;
1557   DISCH_THEN CHOOSE_TAC;
1558   FIRST_X_ASSUM (fun th -> MP_TAC th);
1559   DISCH_THEN CHOOSE_TAC;
1560   FIRST_X_ASSUM MP_TAC;
1561   DISCH_ALL_TAC;
1562   ASM_REWRITE_TAC[];
1563   EXISTS_TAC `\ (x:A). if (x = s) then (v:B) else (u x)`;
1564   REPEAT CONJ_TAC;
1565   X_GEN_TAC `t:A`;
1566   BETA_TAC;
1567   REWRITE_TAC[IN_ELIM_THM;COND_ELIM_THM];
1568   POPL_TAC[1;3;4;5];
1569   ASM_MESON_TAC[];
1570   X_GEN_TAC `t:A`;
1571   BETA_TAC;
1572   REWRITE_TAC[IN_ELIM_THM;COND_ELIM_THM];
1573   ASM_CASES_TAC `(t:A) = s`;
1574   POPL_TAC[1;3;4;5;6];
1575   ASM_REWRITE_TAC[];
1576   POPL_TAC[1;3;4;5;6];
1577   FIRST_X_ASSUM (fun th -> ASSUME_TAC (SPEC `t:A` th));
1578   ASM_SIMP_TAC[prove(`~((t:A)=s) ==> ((t=s)=F)`,MESON_TAC[])];
1579   BETA_TAC;
1580   REWRITE_TAC[];
1581   POPL_TAC[0;2;3;4];
1582   AP_THM_TAC;
1583   AP_TERM_TAC;
1584   MATCH_MP_TAC EQ_EXT;
1585   X_GEN_TAC `t:A`;
1586   BETA_TAC;
1587   DISJ_CASES_TAC (prove(`(((t:A)=s) <=> T) \/ ((t=s) <=> F)`,MESON_TAC[]));
1588   ASM_REWRITE_TAC[];
1589   ASM_MESON_TAC[IN];
1590   ASM_REWRITE_TAC[]
1591   ]);;
1592 (* }}} *)
1593
1594 let CARD_DELETE_CHOICE = prove_by_refinement(
1595   `!(a:(A->bool)). ((FINITE a) /\ (~(a=EMPTY))) ==>
1596    (SUC (CARD (a DELETE (CHOICE a))) = (CARD a))`,
1597 (* {{{ proof *)
1598   [
1599   REPEAT GEN_TAC;
1600   DISCH_ALL_TAC;
1601   ASM_SIMP_TAC[CARD_DELETE];
1602   ASM_SIMP_TAC[CHOICE_DEF];
1603   MATCH_MP_TAC (ARITH_RULE `~(x=0) ==> (SUC (x -| 1) = x)`);
1604   ASM_MESON_TAC[HAS_SIZE_0;HAS_SIZE];
1605   ]);;
1606 (* }}} *)
1607
1608
1609 (*
1610 let dets_flag = ref true;;
1611 dets_flag:= !labels_flag;;
1612 *)
1613
1614
1615 labels_flag:=false;;
1616
1617 (* Law of cardinals |B^A| = |B|^|A| *)
1618 let FUN_SIZE = prove_by_refinement(
1619   `!b a. (FINITE (a:A->bool)) /\ (FINITE (b:B->bool))
1620           ==> ((FUN a b) HAS_SIZE ((CARD b) EXP (CARD a)))`,
1621 (* {{{ proof *)
1622   [
1623   GEN_TAC;
1624   MATCH_MP_TAC (SPEC `CARD:(A->bool)->num` ((INST_TYPE) [`:A->bool`,`:A`]  NUM_INTRO));
1625   INDUCT_TAC;
1626   GEN_TAC;
1627   DISCH_ALL_TAC;
1628   ASM_REWRITE_TAC[];
1629   REWRITE_TAC [EXP];
1630   SUBGOAL_THEN `(a:A->bool) = EMPTY` ASSUME_TAC;
1631   ASM_REWRITE_TAC[GSYM HAS_SIZE_0;HAS_SIZE];
1632   ASM_REWRITE_TAC[HAS_SIZE;DOMAIN_EMPTY];
1633   CONJ_TAC;
1634   REWRITE_TAC[FINITE_SING];
1635   MATCH_MP_TAC CARD_SING;
1636   REWRITE_TAC[SING];
1637   MESON_TAC[];
1638   GEN_TAC;
1639   FIRST_X_ASSUM (fun th -> ASSUME_TAC (SPEC `(a:A->bool) DELETE (CHOICE a)` th)) ;
1640   DISCH_ALL_TAC;
1641   SUBGOAL_THEN `CARD ((a:A->bool) DELETE (CHOICE a)) = n` ASSUME_TAC;
1642   ASM_SIMP_TAC[CARD_DELETE];
1643   SUBGOAL_THEN `CHOICE (a:A->bool) IN a` ASSUME_TAC;
1644   MATCH_MP_TAC CHOICE_DEF;
1645   ASSUME_TAC( ARITH_RULE `!x. (x = (SUC n)) ==> (~(x = 0))`);
1646   REWRITE_TAC[GSYM HAS_SIZE_0;HAS_SIZE];
1647   ASM_MESON_TAC[];
1648   ASM_REWRITE_TAC[];
1649   MESON_TAC[ ( ARITH_RULE `!n. (SUC n -| 1) = n`)];
1650   LABEL_ALL_TAC;
1651   H_MATCH_MP (HYP "3") (HYP "4");
1652   SUBGOAL_THEN `FUN ((a:A->bool) DELETE CHOICE a) (b:B->bool) HAS_SIZE CARD b **| CARD (a DELETE CHOICE a)` ASSUME_TAC;
1653   ASM_MESON_TAC[FINITE_DELETE];
1654   ASSUME_TAC (SPECL [`((a:A->bool) DELETE (CHOICE a))`;`b:B->bool`;`(CHOICE (a:A->bool))` ] DOMAIN_INSERT);
1655   LABEL_ALL_TAC;
1656   H_UNDISCH_TAC (HYP "5");
1657   REWRITE_TAC[IN_DELETE];
1658   SUBGOAL_THEN `~((a:A->bool) = EMPTY)` ASSUME_TAC;
1659   REWRITE_TAC[GSYM HAS_SIZE_0;HAS_SIZE];
1660   ASSUME_TAC( ARITH_RULE `!x. (x = (SUC n)) ==> (~(x = 0))`);
1661   ASM_MESON_TAC[];
1662   ASM_SIMP_TAC[INSERT_DELETE;CHOICE_DEF];
1663   DISCH_THEN CHOOSE_TAC;
1664   REWRITE_TAC[HAS_SIZE];
1665   SUBGOAL_THEN `FINITE (FUN (a:A->bool) (b:B->bool))` ASSUME_TAC;
1666   (* CONJ_TAC; *) ALL_TAC;
1667   MATCH_MP_TAC (SPEC `FUN (a:A->bool) (b:B->bool)` (PINST[(`:A->B`,`:A`);(`:(A->B)#B`,`:B`)] [] FINITE_BIJ2));
1668   EXISTS_TAC `{u,v | (u:A->B) IN FUN (a DELETE CHOICE a) b /\ (v:B) IN b}`;
1669   EXISTS_TAC `F':(A->B)->((A->B)#B)`;
1670   ASM_REWRITE_TAC[];
1671   MATCH_MP_TAC FINITE_PRODUCT;
1672   ASM_REWRITE_TAC[];
1673   ASM_MESON_TAC[HAS_SIZE];
1674   ASM_REWRITE_TAC[];
1675   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;
1676   MATCH_MP_TAC BIJ_CARD;
1677   EXISTS_TAC `F':(A->B)->((A->B)#B)`;
1678   ASM_REWRITE_TAC[];
1679   (* *) ALL_TAC;
1680   ASM_REWRITE_TAC[];
1681   SUBGOAL_THEN `FINITE (a DELETE CHOICE (a:A->bool))` ASSUME_TAC;
1682   ASM_MESON_TAC[FINITE_DELETE];
1683   SUBGOAL_THEN `(FUN ((a:A->bool) DELETE CHOICE a) (b:B->bool)) HAS_SIZE (CARD b **| (CARD (a DELETE CHOICE a)))` ASSUME_TAC;
1684   POPL_TAC[1;2;3;4;5;10;11];
1685   ASM_MESON_TAC[CARD_DELETE];
1686   POP_ASSUM (fun th -> ASSUME_TAC (REWRITE_RULE[HAS_SIZE] th) THEN (ASSUME_TAC th));
1687   ASM_SIMP_TAC[CARD_PRODUCT];
1688   REWRITE_TAC[EXP;MULT_AC]
1689   ]);;
1690 (* }}} *)
1691
1692 labels_flag:= true;;
1693
1694
1695 (* ------------------------------------------------------------------ *)
1696 (* ------------------------------------------------------------------ *)
1697
1698
1699
1700 (* Definitions in math tend to be n-tuples of data.  Let's make it
1701    easy to pick out the individual components of a definition *)
1702
1703 (* pick out the rest of n-tuples. Indexing consistent with lib.drop *)
1704 let drop0 = new_definition(`drop0 (u:A#B) = SND u`);;
1705 let drop1 = new_definition(`drop1 (u:A#B#C) = SND (SND u)`);;
1706 let drop2 = new_definition(`drop2 (u:A#B#C#D) = SND (SND (SND u))`);;
1707 let drop3 = new_definition(`drop3 (u:A#B#C#D#E) = SND (SND (SND (SND u)))`);;
1708
1709 (* pick out parts of n-tuples *)
1710
1711 let part0 = new_definition(`part0 (u:A#B) = FST u`);;
1712 let part1 = new_definition(`part1 (u:A#B#C) = FST (drop0 u)`);;
1713 let part2 = new_definition(`part2 (u:A#B#C#D) = FST (drop1 u)`);;
1714 let part3 = new_definition(`part3 (u:A#B#C#D#E) = FST (drop2 u)`);;
1715 let part4 = new_definition(`part4 (u:A#B#C#D#E#F) = FST (drop3 u)`);;
1716 let part5 = new_definition(`part5 (u:A#B#C#D#E#F#G) =
1717    FST (SND (SND (SND (SND (SND u)))))`);;
1718 let part6 = new_definition(`part6 (u:A#B#C#D#E#F#G#H) =
1719    FST (SND (SND (SND (SND (SND (SND u))))))`);;
1720 let part7 = new_definition(`part7 (u:A#B#C#D#E#F#G#H#I) =
1721    FST (SND (SND (SND (SND (SND (SND (SND u)))))))`);;
1722
1723
1724 (* ------------------------------------------------------------------ *)
1725 (* Basic Definitions of Euclidean Space, Metric Spaces, and Topology *)
1726 (* ------------------------------------------------------------------ *)
1727
1728 (* ------------------------------------------------------------------ *)
1729 (* Interface *)
1730 (* ------------------------------------------------------------------ *)
1731
1732 let euclid_def = local_definition "euclid";;
1733 mk_local_interface "euclid";;
1734
1735 overload_interface
1736  ("+", `euclid'euclid_plus:(num->real)->(num->real)->(num->real)`);;
1737
1738 make_overloadable "*#" `:A -> B -> B`;;
1739
1740 let euclid_scale = euclid_def
1741   `euclid_scale t f = \ (i:num). (t*. (f i))`;;
1742
1743 overload_interface ("*#",`euclid'euclid_scale`);;
1744
1745 parse_as_infix("*#",(20,"right"));;
1746
1747 let euclid_neg = euclid_def `euclid_neg f = \ (i:num). (--. (f i))`;;
1748
1749 (* This is highly ambiguous: -- f x can be read as
1750    (-- f) x or as -- (f x).  *)
1751 overload_interface ("--",`euclid'euclid_neg`);;
1752
1753 overload_interface
1754   ("-", `euclid'euclid_minus:(num->real)->(num->real)->(num->real)`);;
1755
1756 (* ------------------------------------------------------------------ *)
1757 (* Euclidean Space *)
1758 (* ------------------------------------------------------------------ *)
1759
1760 let euclid_plus = euclid_def
1761   `euclid_plus f g = \ (i:num). (f i) +. (g i)`;;
1762
1763 let euclid = euclid_def `euclid n v <=> !m. (n <=| m) ==> (v m = &.0)`;;
1764
1765 let euclidean = euclid_def `euclidean v <=> ?n. euclid n v`;;
1766
1767 let euclid_minus = euclid_def
1768   `euclid_minus f g = \(i:num). (f i) -. (g i)`;;
1769
1770 let euclid0 = euclid_def `euclid0 = \(i:num). &.0`;;
1771
1772 let coord = euclid_def `coord i (f:num->real) = f i`;;
1773
1774 let dot = euclid_def `dot f g =
1775   let (n = (min_num (\m. (euclid m f) /\ (euclid m g)))) in
1776   sum (0,n) (\i. (f i)*(g i))`;;
1777
1778 let norm = euclid_def `norm f = sqrt(dot f f)`;;
1779
1780 let d_euclid = euclid_def `d_euclid f g = norm (f - g)`;;
1781
1782
1783
1784 (* ------------------------------------------------------------------ *)
1785 (* Euclidean and Convex geometry *)
1786 (* ------------------------------------------------------------------ *)
1787
1788
1789 let sum_vector_EXISTS = prove_by_refinement(
1790   `?sum_vector. (!f n. sum_vector(n,0) f = (\n. &.0)) /\
1791     (!f m n. sum_vector(n,SUC m) f = sum_vector(n,m) f + f(n + m))`,
1792   (* {{{ proof *)
1793   [
1794   (CHOOSE_TAC o prove_recursive_functions_exist num_RECURSION) `(!f n. sm n 0 f = (\n. &0)) /\ (!f m n. sm  n (SUC m) f = sm n m f + f(n + m))`;
1795   EXISTS_TAC `\(n,m) f. (sm:num->num->(num->(num->real))->(num->real)) n m f`;
1796   CONV_TAC(DEPTH_CONV GEN_BETA_CONV);
1797   ASM_REWRITE_TAC[];
1798   ]);;
1799   (* }}} *)
1800
1801 let sum_vector = new_specification ["sum_vector"] sum_vector_EXISTS;;
1802
1803 let mk_segment = euclid_def
1804   `mk_segment x y = { u | ?a. (&.0 <=. a) /\ (a <=. &.1) /\
1805         (u = a *# x + (&.1 - a) *# y) }`;;
1806
1807 let mk_open_segment = euclid_def
1808   `mk_open_segment x y = { u | ?a. (&.0 <. a) /\ (a <. &.1) /\
1809         (u = a *# x + (&.1 - a) *# y) }`;;
1810
1811 let convex = euclid_def
1812   `convex S <=> !x y. (S x) /\ (S y) ==> (mk_segment x y SUBSET S)`;;
1813
1814 let convex_hull = euclid_def
1815   `convex_hull S = { u | ?f alpha m. (!n. (n< m) ==> (S (f n))) /\
1816     (sum(0,m) alpha = &.1) /\ (!n. (n< m) ==> (&.0 <=. (alpha n))) /\
1817     (u = sum_vector(0,m) (\n. (alpha n) *# (f n)))}`;;
1818
1819 let affine_hull = euclid_def
1820   `affine_hull S = { u | ?f alpha m. (!n. (n< m) ==> (S (f n))) /\
1821     (sum(0,m) alpha = &.1) /\
1822     (u = sum_vector(0,m) (\n. (alpha n) *# (f n)))}`;;
1823
1824 let mk_line = euclid_def `mk_line x y =
1825    {z| ?t. (z = (t *# x) + ((&.1 - t) *# y)) }`;;
1826
1827 let affine = euclid_def
1828   `affine S <=> !x y. (S x ) /\ (S y) ==> (mk_line x y SUBSET S)`;;
1829
1830 let affine_dim = euclid_def
1831   `affine_dim n S <=>
1832     (?T. (T HAS_SIZE (SUC n)) /\ (affine_hull T = affine_hull S)) /\
1833     (!T m. (T HAS_SIZE (SUC m)) /\ (m < n) ==> ~(affine_hull T = affine_hull S))`;;
1834
1835 let collinear = euclid_def
1836   `collinear S <=> (?n. affine_dim n S /\ (n < 2))`;;
1837
1838 let coplanar = euclid_def
1839   `coplanar S <=> (?n. affine_dim n S /\ (n < 3))`;;
1840
1841 let line = euclid_def
1842   `line L <=> (affine L) /\ (affine_dim 1 L)`;;
1843
1844 let plane = euclid_def
1845   `plane P <=> (affine P) /\ (affine_dim 2 P)`;;
1846
1847 let space = euclid_def
1848   `space R <=> (affine R) /\ (affine_dim 3 R)`;;
1849
1850 (*
1851
1852 General constructor of conical objects, including
1853   rays, cones, half-planes, etc.
1854
1855 L is the edge.  C is the set of generators in the positive
1856 direction.
1857
1858 If L is a line, and C = {c}, we get the half-plane bounded by
1859 L and containing c.
1860
1861 If L is a point, and C is general, we get the cone at L generated
1862 by C.
1863
1864 If L and C are both singletons, we get the ray ending at L.
1865
1866   *)
1867
1868 let mk_open_half_set = euclid_def
1869   `mk_open_half_set L S  =
1870    { u | ?t v c. (L v) /\ (S c) /\ (&.0 < t) /\
1871       (u = (t *# (c - v) + (&.1 - t) *# v)) }`;;
1872
1873 let mk_half_set = euclid_def
1874   `mk_half_set L S  =
1875    { u | ?t v c. (L v) /\ (S c) /\ (&.0 <=. t) /\
1876       (u = (t *# (c - v) + (&.1 - t) *# v)) }`;;
1877
1878
1879 let mk_angle = euclid_def `mk_angle x y z =
1880    (mk_half_set {x} {y}) UNION (mk_half_set {x} {z})`;;
1881
1882 let mk_signed_angle = euclid_def `mk_signed_angle x y z =
1883    (mk_half_set {x} {y} , mk_half_set {x} {z})`;;
1884
1885 let mk_convex_cone = euclid_def
1886   `mk_convex_cone v (S:(num->real)->bool) =
1887     mk_half_set {v} (convex_hull S)`;;
1888
1889 (* we always normalize the radius of balls in a packing to 1 *)
1890 let packing = euclid_def(`packing (S:(num->real)->bool) <=>
1891         !x y. ( ((S x) /\ (S y) /\ ((d_euclid x y) < (&.2))) ==>
1892                 (x = y))`);;
1893
1894 let saturated_packing = euclid_def(`saturated_packing S <=>
1895         (( packing S) /\
1896         (!z. (affine_hull S z)  ==>
1897                (?x. ((S x) /\ ((d_euclid x z) < (&.2))))))`);;
1898
1899
1900 (* 3 dimensions specific:  *)
1901 let cross_product3 = euclid_def(`cross_product3 v1 v2 =
1902         let (x1 = v1 0) and (x2 = v1 1) and (x3 = v1 2) in
1903         let (y1 = v2 0) and (y2 = v2 1) and (y3 = v2 2) in
1904         (\k.
1905                 (if (k=0) then (x2*y3-x3*y2)
1906                 else if (k=1) then (x3*y1-x1*y3)
1907                 else if (k=2) then (x1*y2-x2*y1)
1908                 else (&0)))`);;
1909
1910 let triple_product = euclid_def(`triple_product v1 v2 v3 =
1911         dot v1 (cross_product3 v2 v3)`);;
1912
1913 (* the bounding edge *)
1914 let mk_triangle = euclid_def `mk_triangle v1 v2 v3 =
1915   (mk_segment v1 v2) UNION (mk_segment v2 v3) UNION (mk_segment v3 v1)`;;
1916
1917 (* the interior *)
1918 let mk_interior_triangle = euclid_def
1919   `mk_interior_triangle v1 v2 v3 =
1920      mk_open_half_set (mk_line v1 v2) {v3} INTER
1921        (mk_open_half_set (mk_line v2 v3) {v1}) INTER
1922        (mk_open_half_set (mk_line v3 v1) {v2})`;;
1923
1924 let mk_triangular_region = euclid_def
1925   `mk_triangular_region v1 v2 v3 =
1926     (mk_triangle v1 v2 v3) UNION (mk_interior_triangle v1 v2 v3)`;;
1927
1928
1929 (* ------------------------------------------------------------------ *)
1930 (* Statements of Theorems in Euclidean Geometry (no proofs *)
1931 (* ------------------------------------------------------------------ *)
1932
1933 let half_set_convex = `!L S. convex (mk_half_set L S)`;;
1934
1935 let open_half_set_convex = `!L S . convex (mk_open_half_set L S )`;;
1936
1937 let affine_dim0 = `!S. (affine_dim 0 S) = (SING S)`;;
1938
1939 let hull_convex = `!S. (convex (convex_hull S))`;;
1940
1941 let hull_minimal = `!S T. (convex T) /\ (S SUBSET T) ==>
1942      (convex_hull S) SUBSET T`;;
1943
1944 let affine_hull_affine = `!S. (affine (affine_hull S))`;;
1945
1946 let affine_hull_minimal = `!S T. (affine T) /\ (S SUBSET T) ==>
1947      (affine_hull S) SUBSET T`;;
1948
1949 let mk_line_dim = `!x y. ~(x = y) ==> affine_dim 1 (mk_line x y)`;;
1950
1951 let affine_convex_hull = `!S. (affine_hull S) = (affine_hull (convex_hull S))`;;
1952
1953 let convex_hull_hull = `!S. (convex_hull S) = (convex_hull (convex_hull S))`;;
1954
1955 let euclid_affine_dim = `!n. affine_dim n (euclid n)`;;
1956
1957 let affine_dim_subset = `!m n T S.
1958   (affine_dim m T) /\ (affine_dim n S) /\ (T SUBSET S) ==> (m <= n)`;;
1959
1960 (* A few of the Birkhoff postulates of Geometry (incomplete) *)
1961
1962 let line_postulate = `!x y. ~(x = y) ==>
1963    (?!L. (L x) /\ (L y) /\ (line L))`;;
1964
1965 let ruler_postulate = `!L. (line L) ==>
1966   (?f. (BIJ f L UNIV) /\
1967   (!x y. (L x /\ L y ==> (d_euclid x y = abs(f x -. f y)))))`;;
1968
1969 let affine_postulate = `!n. (affine_dim n P) ==> (?S.
1970   (S SUBSET P) /\ (S HAS_SIZE n) /\ (affine_dim n S))`;;
1971
1972 let line_plane = `!P x y. (plane P) /\ (P x) /\ (P y) ==>
1973   (mk_line x y SUBSET P)`;;
1974
1975 let plane_of_pt = `!S. (S HAS_SIZE 3) ==> (?P. (plane P) /\
1976    (S SUBSET P))`;;
1977
1978 let plane_of_pt_unique = `!S. (S HAS_SIZE 3) ==> (collinear S) \/
1979   (?! P. (plane P) /\ (S SUBSET P))`;;
1980
1981 let plane_inter = `!P Q. (plane P) /\ (plane Q) ==>
1982   (P INTER Q = EMPTY) \/ (line (P INTER Q)) \/ (P = Q)`;;
1983
1984 (* each line separates a plane into two half-planes *)
1985 let plane_separation =
1986   `!P L. (plane P) /\ (line L) /\ (L SUBSET P) ==>
1987   (?A B. (A INTER B = EMPTY) /\ (A INTER L = EMPTY) /\
1988     (B INTER L = EMPTY) /\ (L UNION A UNION B = P) /\
1989    (!c u. (P c) /\ (u = mk_open_half_set L {c}) ==>
1990       (u = A) \/ (u = B) \/ (u = L)) /\
1991    (!a b. (A a) /\ (B b) ==> ~(segment a b INTER L = EMPTY)))`;;
1992
1993 let space_separation =
1994   `!R P. (space R) /\ (plane P) /\ (P SUBSET R) ==>
1995   (?A B. (A INTER B = EMRTY) /\ (A INTER P = EMRTY) /\
1996     (B INTER P = EMRTY) /\ (P UNION A UNION B = R) /\
1997    (!c u. (R c) /\ (u = mk_open_half_set P {c}) ==>
1998       (u = A) \/ (u = B) \/ (u = P)) /\
1999      (!a b. (A a) /\ (B b) ==> ~(segment a b INTER L = EMPTY)))`;;
2000
2001 (* ------------------------------------------------------------------ *)
2002 (* Metric Space *)
2003 (* ------------------------------------------------------------------ *)
2004
2005 let metric_space = euclid_def `metric_space (X:A->bool,d:A->A->real)
2006    <=>
2007    !x y z.
2008       (X x) /\ (X y) /\ (X z) ==>
2009          (((&.0) <=. (d x y)) /\
2010           ((&.0 = d x y) = (x = y)) /\
2011           (d x y = d y x) /\
2012           (d x z <=. d x y + d y z))`;;
2013
2014 (* ------------------------------------------------------------------ *)
2015 (* Measure *)
2016 (* ------------------------------------------------------------------ *)
2017
2018 let set_translate = euclid_def
2019   `set_translate v X = { z | ?x. (X x) /\ (z = v + x) }`;;
2020
2021 let set_scale = euclid_def
2022   `set_scale r X = { z | ?x. (X x) /\ (z = r *# x) }`;;
2023
2024 let mk_rectangle = euclid_def
2025   `mk_rectangle a b = { z | !(i:num). (a i <=. z i) /\ (z i <. b i) }`;;
2026
2027 let one_vec = euclid_def
2028   `one_vec n = (\i. if (i<| n) then (&.1) else (&.0))`;;
2029
2030 let mk_cube = euclid_def
2031   `mk_cube n k v =
2032     let (r = twopow (--: (&: k))) in
2033     let (vv = (\i. (real_of_int (v i)))) in
2034      mk_rectangle (r *# vv) (r *# (vv + (one_vec n)))`;;
2035
2036 let inner_cube = euclid_def
2037   `inner_cube n k A =
2038     { v | (mk_cube n k v SUBSET A) /\
2039       (!i. (n <| i) ==> (&:0 = v i)) }`;;
2040
2041 let outer_cube = euclid_def
2042   `outer_cube n k A =
2043     { v | ~((mk_cube n k v) INTER A = EMPTY) /\
2044       (!i. (n <| i) ==> (&:0 = v i)) }`;;
2045
2046 let inner_vol = euclid_def
2047   `inner_vol n k A =
2048     (&. (CARD (inner_cube n k A)))*(twopow (--: (&: (n*k))))`;;
2049
2050 let outer_vol = euclid_def
2051   `outer_vol n k A =
2052     (&. (CARD (outer_cube n k A)))*(twopow (--: (&: (n*k))))`;;
2053
2054 let euclid_bounded = euclid_def
2055   `euclid_bounded A = (?R. !(x:num->real) i. (A x) ==> (x i <. R))`;;
2056
2057 let vol = euclid_def
2058   `vol n A = lim (\k. outer_vol n k A)`;;
2059
2060 (* ------------------------------------------------------------------ *)
2061 (* COMPUTING PI *)
2062 (* ------------------------------------------------------------------ *)
2063
2064 unambiguous_interface();;
2065 prioritize_real();;
2066
2067 (* ------------------------------------------------------------------ *)
2068 (* general series approximations *)
2069 (* ------------------------------------------------------------------ *)
2070
2071 let SER_APPROX1 = prove_by_refinement(
2072   `!s f g.  (f sums s) /\ (summable g) ==>
2073     (!k. ((!n. (||. (f (n+k)) <=. (g (n+k)))) ==>
2074     ( (s - (sum(0,k) f)) <=. (suminf (\n. (g (n +| k)))))))`,
2075   (* {{{ proof *)
2076   [
2077   REPEAT GEN_TAC;
2078   DISCH_ALL_TAC;
2079   GEN_TAC;
2080   DISCH_TAC;
2081   IMP_RES_THEN ASSUME_TAC SUM_SUMMABLE;
2082   IMP_RES_THEN (fun th -> (ASSUME_TAC (SPEC `k:num` th))) SER_OFFSET;
2083   IMP_RES_THEN ASSUME_TAC SUM_UNIQ;
2084   SUBGOAL_THEN `(\n. (f (n+ k))) sums (s - (sum(0,k) f))` ASSUME_TAC;
2085   ASM_MESON_TAC[];
2086   SUBGOAL_THEN `summable (\n. (f (n+k))) /\ (suminf (\n. (f (n+k))) <=. (suminf (\n. (g (n+k)))))` ASSUME_TAC;
2087   MATCH_MP_TAC SER_LE2;
2088   BETA_TAC;
2089   ASM_REWRITE_TAC[];
2090   IMP_RES_THEN ASSUME_TAC SER_OFFSET;
2091   FIRST_X_ASSUM (fun th -> ACCEPT_TAC (MATCH_MP SUM_SUMMABLE (((SPEC `k:num`) th))));
2092   ASM_MESON_TAC[SUM_UNIQ]
2093   ]);;
2094   (* }}} *)
2095
2096 let SER_APPROX = prove_by_refinement(
2097   `!s f g.  (f sums s) /\ (!n. (||. (f n) <=. (g n))) /\
2098        (summable g) ==>
2099     (!k. (abs (s - (sum(0,k) f)) <=. (suminf (\n. (g (n +| k))))))`,
2100   (* {{{ proof *)
2101   [
2102   REPEAT GEN_TAC;
2103   DISCH_ALL_TAC;
2104   GEN_TAC;
2105   REWRITE_TAC[REAL_ABS_BOUNDS];
2106   CONJ_TAC;
2107   SUBGOAL_THEN `(!k. ((!n. (||. ((\p. (--. (f p))) (n+k))) <=. (g (n+k)))) ==> ((--.s) - (sum(0,k) (\p. (--. (f p)))) <=. (suminf (\n. (g (n +k))))))` ASSUME_TAC;
2108   MATCH_MP_TAC SER_APPROX1;
2109   ASM_REWRITE_TAC[];
2110   MATCH_MP_TAC SER_NEG ;
2111   ASM_REWRITE_TAC[];
2112   MATCH_MP_TAC (REAL_ARITH (`(--. s -. (--. u) <=. x) ==> (--. x <=. (s -. u))`));
2113   ONCE_REWRITE_TAC[GSYM SUM_NEG];
2114   FIRST_X_ASSUM (fun th -> (MATCH_MP_TAC th));
2115   BETA_TAC;
2116   ASM_REWRITE_TAC[REAL_ABS_NEG];
2117   H_VAL2 CONJ (HYP "0") (HYP "2");
2118   IMP_RES_THEN MATCH_MP_TAC SER_APPROX1 ;
2119   GEN_TAC;
2120   ASM_MESON_TAC[];
2121   ]);;
2122   (* }}} *)
2123
2124 (* ------------------------------------------------------------------ *)
2125 (* now for pi calculation stuff *)
2126 (* ------------------------------------------------------------------ *)
2127
2128
2129 let local_def = local_definition "trig";;
2130
2131
2132 let PI_EST = prove_by_refinement(
2133                `!n. (1 <=| n) ==> (abs(&4 / &(8 * n + 1) -
2134             &2 / &(8 * n + 4) -
2135             &1 / &(8 * n + 5) -
2136             &1 / &(8 * n + 6)) <= &.622/(&.819))`,
2137   (* {{{ proof *)
2138    [
2139    GEN_TAC THEN DISCH_ALL_TAC;
2140    REWRITE_TAC[real_div];
2141    MATCH_MP_TAC (REWRITE_RULE[real_div] (REWRITE_RULE[REAL_RAT_REDUCE_CONV `(&.4/(&.9) +(&.2/(&.12)) + (&.1/(&.13))+ (&.1/(&.14)))`] (REAL_ARITH `(abs((&.4)*.u)<=. (&.4)/(&.9)) /\ (abs((&.2)*.v)<=. (&.2)/(&.12)) /\ (abs((&.1)*w) <=. (&.1)/(&.13)) /\ (abs((&.1)*x) <=. (&.1)/(&.14)) ==> (abs((&.4)*u -(&.2)*v - (&.1)*w - (&.1)*x) <= (&.4/(&.9) +(&.2/(&.12)) + (&.1/(&.13))+ (&.1/(&.14))))`)));
2142    IMP_RES_THEN ASSUME_TAC (ARITH_RULE `1 <=| n ==> (0 < n)`);
2143    FIRST_X_ASSUM (fun th -> ASSUME_TAC (REWRITE_RULE[GSYM REAL_OF_NUM_LT] th));
2144    ASSUME_TAC (prove(`(a<=.b) ==> (&.n*a <=. (&.n)*b)`,MESON_TAC[REAL_PROP_LE_LMUL;REAL_POS]));
2145    REWRITE_TAC[REAL_ABS_MUL;REAL_ABS_INV;prove(`||.(&.n) = (&.n)`,MESON_TAC[REAL_POS;REAL_ABS_REFL])];
2146    REPEAT CONJ_TAC THEN (POP_ASSUM (fun th -> MATCH_MP_TAC th)) THEN (MATCH_MP_TAC (prove(`((&.0 <. (&.n)) /\ (&.n <=. a)) ==> (inv(a)<=. (inv(&.n)))`,MESON_TAC[REAL_ABS_REFL;REAL_ABS_INV;REAL_LE_INV2]))) THEN
2147    REWRITE_TAC[REAL_LT;REAL_LE] THEN (H_UNDISCH_TAC (HYP"0")) THEN
2148    ARITH_TAC]);;
2149   (* }}} *)
2150
2151 let pi_fun = local_def `pi_fun n = inv (&.16 **. n) *.
2152           (&.4 / &.(8 *| n +| 1) -.
2153            &.2 / &.(8 *| n +| 4) -.
2154            &.1 / &.(8 *| n +| 5) -.
2155            &.1 / &.(8 *| n +| 6))`;;
2156
2157 let pi_bound_fun = local_def `pi_bound_fun n = if (n=0) then (&.8) else
2158     (((&.15)/(&.16))*(inv(&.16 **. n))) `;;
2159
2160 let PI_EST2 = prove_by_refinement(
2161     `!k. abs(pi_fun k) <=. (pi_bound_fun k)`,
2162   (* {{{ proof *)
2163    [
2164    GEN_TAC;
2165    REWRITE_TAC[pi_fun;pi_bound_fun];
2166    COND_CASES_TAC;
2167    ASM_REWRITE_TAC[];
2168    CONV_TAC (NUM_REDUCE_CONV);
2169    (CONV_TAC (REAL_RAT_REDUCE_CONV));
2170    CONV_TAC (RAND_CONV (REWR_CONV (REAL_ARITH `a*b = b*.a`)));
2171    REWRITE_TAC[REAL_ABS_MUL;REAL_ABS_INV;REAL_ABS_POW;prove(`||.(&.n) = (&.n)`,MESON_TAC[REAL_POS;REAL_ABS_REFL])];
2172    MATCH_MP_TAC (prove(`!x y z. (&.0 <. z /\ (y <=. x) ==> (z*y <=. (z*x)))`,MESON_TAC[REAL_LE_LMUL_EQ]));
2173    ASSUME_TAC (REWRITE_RULE[] (REAL_RAT_REDUCE_CONV `(&.622)/(&.819) <=. (&.15)/(&.16)`));
2174    IMP_RES_THEN ASSUME_TAC (ARITH_RULE `~(k=0) ==> (1<=| k)`);
2175    IMP_RES_THEN ASSUME_TAC (PI_EST);
2176    CONJ_TAC;
2177    SIMP_TAC[REAL_POW_LT;REAL_LT_INV;ARITH_RULE `&.0 < (&.16)`];
2178    ASM_MESON_TAC[REAL_LE_TRANS];
2179    ]);;
2180   (* }}} *)
2181
2182 let GP16 = prove_by_refinement(
2183   `!k. (\n. inv (&16 pow k) * inv (&16 pow n)) sums
2184          inv (&16 pow k) * &16 / &15`,
2185   (* {{{ proof *)
2186   [
2187   GEN_TAC;
2188   ASSUME_TAC (REWRITE_RULE[] (REAL_RAT_REDUCE_CONV `abs (&.1 / (&. 16)) <. (&.1)`));
2189   IMP_RES_THEN (fun th -> ASSUME_TAC (CONV_RULE REAL_RAT_REDUCE_CONV th)) GP;
2190   MATCH_MP_TAC SER_CMUL;
2191   ASM_REWRITE_TAC[GSYM REAL_POW_INV;REAL_INV_1OVER];
2192   ]);;
2193   (* }}} *)
2194
2195 let GP16a = prove_by_refinement(
2196    `!k. (0<|k) ==> (\n. (pi_bound_fun (n+k))) sums (inv(&.16 **. k))`,
2197   (* {{{ proof *)
2198    [
2199    GEN_TAC;
2200    DISCH_TAC;
2201    SUBGOAL_THEN `(\n. pi_bound_fun (n+k)) = (\n. ((&.15/(&.16))* (inv(&.16)**. k) *. inv(&.16 **. n)))` (fun th-> REWRITE_TAC[th]);
2202    MATCH_MP_TAC EQ_EXT;
2203    X_GEN_TAC `n:num` THEN BETA_TAC;
2204    REWRITE_TAC[pi_bound_fun];
2205    COND_CASES_TAC;
2206    ASM_MESON_TAC[ARITH_RULE `0<| k ==> (~(n+k = 0))`];
2207    REWRITE_TAC[GSYM REAL_MUL_ASSOC];
2208    AP_TERM_TAC;
2209    REWRITE_TAC[REAL_INV_MUL;REAL_POW_ADD;REAL_POW_INV;REAL_MUL_AC];
2210    SUBGOAL_THEN `(\n. (&.15/(&.16)) *. ((inv(&.16)**. k)*. inv(&.16 **. n))) sums ((&.15/(&.16)) *.(inv(&.16**. k)*. ((&.16)/(&.15))))` ASSUME_TAC;
2211    MATCH_MP_TAC SER_CMUL;
2212    REWRITE_TAC[REAL_POW_INV];
2213    ACCEPT_TAC (SPEC `k:num` GP16);
2214    FIRST_X_ASSUM MP_TAC;
2215    REWRITE_TAC[REAL_MUL_ASSOC];
2216    MATCH_MP_TAC (prove (`(x=y) ==> ((a sums x) ==> (a sums y))`,MESON_TAC[]));
2217    MATCH_MP_TAC (REAL_ARITH `(b*(a*c) = (b*(&.1))) ==> ((a*b)*c = b)`);
2218    AP_TERM_TAC;
2219    CONV_TAC (REAL_RAT_REDUCE_CONV);
2220    ]);;
2221   (* }}} *)
2222
2223 let PI_SER = prove_by_refinement(
2224   `!k. (0<|k) ==> (abs(pi - (sum(0,k) pi_fun)) <=. (inv(&.16 **. (k))))`,
2225   (* {{{ proof *)
2226    [
2227    GEN_TAC THEN DISCH_TAC;
2228    ASSUME_TAC (ONCE_REWRITE_RULE[ETA_AX] (REWRITE_RULE[GSYM pi_fun] POLYLOG_THM));
2229    ASSUME_TAC PI_EST2;
2230    IMP_RES_THEN (ASSUME_TAC) GP16a;
2231    IMP_RES_THEN (ASSUME_TAC) SUM_SUMMABLE;
2232    IMP_RES_THEN (ASSUME_TAC) SER_OFFSET_REV;
2233    IMP_RES_THEN (ASSUME_TAC) SUM_SUMMABLE;
2234    MP_TAC (SPECL [`pi`;`pi_fun`;`pi_bound_fun` ] SER_APPROX);
2235    ASM_REWRITE_TAC[];
2236    DISCH_THEN (fun th -> MP_TAC (SPEC `k:num` th));
2237    SUBGOAL_THEN `suminf (\n. pi_bound_fun (n + k)) = inv (&.16 **. k)` (fun th -> (MESON_TAC[th]));
2238    ASM_MESON_TAC[SUM_UNIQ];
2239    ]);;
2240   (* }}} *)
2241
2242 (* replace 3 by SUC (SUC (SUC 0)) *)
2243 let SUC_EXPAND_CONV tm =
2244    let count = dest_numeral tm in
2245    let rec add_suc i r =
2246      if (i <=/ (Int 0)) then r
2247      else add_suc (i -/ (Int 1)) (mk_comb (`SUC`,r)) in
2248    let tm' = add_suc count `0` in
2249    REWRITE_RULE[] (ARITH_REWRITE_CONV[] (mk_eq (tm,tm')));;
2250
2251 let inv_twopow = prove(
2252   `!n. inv (&.16 **. n) = (twopow (--: (&:(4*n)))) `,
2253     REWRITE_TAC[TWOPOW_NEG;GSYM (NUM_RED_CONV `2 EXP 4`);
2254     REAL_OF_NUM_POW;EXP_MULT]);;
2255
2256 let PI_SERn n =
2257    let SUM_EXPAND_CONV =
2258            (ARITH_REWRITE_CONV[]) THENC
2259            (TOP_DEPTH_CONV SUC_EXPAND_CONV) THENC
2260            (REWRITE_CONV[sum]) THENC
2261            (ARITH_REWRITE_CONV[REAL_ADD_LID;GSYM REAL_ADD_ASSOC]) in
2262    let sum_thm = SUM_EXPAND_CONV (vsubst [n,`i:num`] `sum(0,i) f`) in
2263    let gt_thm = ARITH_RULE (vsubst [n,`i:num`] `0 <| i`) in
2264    ((* CONV_RULE REAL_RAT_REDUCE_CONV *)(CONV_RULE (ARITH_REWRITE_CONV[]) (BETA_RULE (REWRITE_RULE[sum_thm;pi_fun;inv_twopow] (MATCH_MP PI_SER gt_thm)))));;
2265
2266 (* abs(pi - u ) < e *)
2267 let recompute_pi bprec =
2268    let n = (bprec /4) in
2269    let pi_ser = PI_SERn (mk_numeral (Int n)) in
2270    let _ = remove_real_constant `pi` in
2271    (add_real_constant pi_ser; INTERVAL_OF_TERM bprec `pi`);;
2272
2273 (* ------------------------------------------------------------------ *)
2274 (* restore defaults *)
2275 (* ------------------------------------------------------------------ *)
2276
2277 reduce_local_interface("trig");;
2278 pop_priority();;
2279
2280
2281
2282
2283
2284
2285