4 let dirac_delta = new_definition `dirac_delta (i:num) =
5 (\j. if (i=j) then (&.1) else (&.0))`;;
7 let min_num = new_definition
8 `min_num (X:num->bool) = @m. (m IN X) /\ (!n. (n IN X) ==> (m <= n))`;;
10 let min_least = prove_by_refinement (
11 `!(X:num->bool) c. (X c) ==> (X (min_num X) /\ (min_num X <=| c))`,
15 REWRITE_TAC[min_num;IN];
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))];
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') `]
29 let max_real = new_definition(`max_real x y =
30 if (y <. x) then x else y`);;
32 let min_real = new_definition(`min_real x y =
33 if (x <. y) then x else y`);;
35 let deriv = new_definition(`deriv f x = @d. (f diffl d)(x)`);;
36 let deriv2 = new_definition(`deriv2 f = (deriv (deriv f))`);;
38 let square_le = prove_by_refinement(
39 `!x y. (&.0 <=. x) /\ (&.0 <=. y) /\ (x*.x <=. y*.y) ==> (x <=. y)`,
44 UNDISCH_FIND_TAC `( *. )` ;
45 ONCE_REWRITE_TAC[REAL_ARITH `(a <=. b) <=> (&.0 <= (b - a))`];
46 REWRITE_TAC[GSYM REAL_DIFFSQ];
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))`];
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))`,
63 REWRITE_TAC[GSYM LEFT_FORALL_IMP_THM];
65 SPEC_TAC (`t:num->num`,`t:num->num`);
66 SPEC_TAC (`n:num`,`n:num`);
69 REWRITE_TAC[ARITH_RULE `0<=|m`];
72 ASM_MESON_TAC[ARITH_RULE`(a=0) ==> (a <=|0)`];
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))`;
87 FIRST_ASSUM (fun t-> MP_TAC(SPEC `b:num->num` t));
88 SUBGOAL_TAC `!m. (n<=|m) ==> (b m =0)`;
90 ASM_CASES_TAC `m = (n:num)`;
92 SUBGOAL_TAC ( `(n <=| m) /\ (~(m = n)) ==> (SUC n <=| m)`);
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`;
101 ASM_CASES_TAC `(i:num) = n`;
104 MATCH_MP_TAC (ARITH_RULE `x <=| M ==> (x <=| M+ u)`);
109 let REAL_INV_LT = prove_by_refinement(
110 `!x y z. (&.0 <. x) ==> ((inv(x)*y < z) <=> (y <. x*z))`,
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];
122 let REAL_MUL_NN = prove_by_refinement(
123 `!x y. (&.0 <= x*y) <=>
124 ((&.0 <= x /\ (&.0 <=. y)) \/ ((x <= &.0) /\ (y <= &.0) ))`,
128 SUBGOAL_TAC `! x y. ((&.0 < x) ==> ((&.0 <= x*y) <=> ((&.0 <= x /\ (&.0 <=. y)) \/ ((x <= &.0) /\ (y <= &.0) ))))`;
130 ASM_SIMP_TAC[REAL_ARITH `((&.0 <. x) ==> (&.0 <=. x))`;REAL_ARITH `(&.0 <. x) ==> ~(x <=. &.0)`];
132 ASM_MESON_TAC[REAL_PROP_NN_LCANCEL];
133 ASM_MESON_TAC[REAL_LE_MUL;REAL_LT_IMP_LE];
135 DISJ_CASES_TAC (REAL_ARITH `(&.0 < x) \/ (x = &.0) \/ (x < &.0)`);
137 UND 1 THEN DISCH_THEN DISJ_CASES_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)`]);
145 ASM_SIMP_TAC[REAL_ARITH `((x <. &.0) ==> ~(&.0 <=. x))`;REAL_ARITH `(x <. &.0) ==> (x <=. &.0)`];
149 let ABS_SQUARE = prove_by_refinement(
150 `!t u. abs(t) <. u ==> t*t <. u*u`,
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)`;
161 MATCH_MP_TAC REAL_PROP_LT_LRMUL;
167 let ABS_SQUARE_LE = prove_by_refinement(
168 `!t u. abs(t) <=. u ==> t*t <=. u*u`,
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)`;
179 MATCH_MP_TAC REAL_PROP_LE_LRMUL;
185 let twopow_eps = prove_by_refinement(
186 `!R e. ?n. (&.0 <. R)/\ (&.0 <. e) ==> R*(twopow(--: (&:n))) <. e`,
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");
198 ASSUME_TAC (SPEC `R/e` REAL_ARCH_SIMPLE);
202 MESON_TAC[POW_2_LT;REAL_LET_TRANS];
208 (* ------------------------------------------------------------------ *)
209 (* finite products, in imitation of finite sums *)
210 (* ------------------------------------------------------------------ *)
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))`,
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[]
223 let prod_DEF = new_specification ["prod"] prod_EXISTS;;
226 (`!n m. (prod(n,0) f = &1) /\
227 (prod(n,SUC m) f = prod(n,m) f * f(n + m))`,
229 REWRITE_TAC[prod_DEF]);;
232 let PROD_TWO = prove_by_refinement(
233 `!f n p. prod(0,n) f * prod(n,p) f = prod(0,n + p) f`,
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];
243 let ABS_PROD = prove_by_refinement(
244 `!f m n. abs(prod(m,n) f) = prod(m,n) (\n. abs(f n))`,
247 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC;
250 ASM_REWRITE_TAC[prod;ABS_MUL]
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)`,
260 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN 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))`];
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))`]
275 let PROD_POS = prove_by_refinement
276 (`!f. (!n. &0 <= f(n)) ==> !m n. &0 <= prod(m,n) f`,
280 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[prod];
282 ASM_MESON_TAC[REAL_LE_MUL]
286 let PROD_POS_GEN = prove_by_refinement
288 (!n. m <= n ==> &0 <= f(n))
289 ==> &0 <= prod(m,n) f`,
293 REPEAT STRIP_TAC THEN SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN REWRITE_TAC[prod];
295 ASM_MESON_TAC[REAL_LE_MUL;ARITH_RULE `m <=| (m +| n)`]
301 (`!f m n. abs(prod(m,n) (\m. abs(f m))) = prod(m,n) (\m. abs(f m))`,
303 REWRITE_TAC[ABS_PROD;REAL_ARITH `||. (||. x) = (||. x)`]);;
306 let PROD_ZERO = prove_by_refinement
307 (`!f m n. (?p. (m <= p /\ (p < (n+| m)) /\ (f p = (&.0)))) ==>
311 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN (REWRITE_TAC[prod]);
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;
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));
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`,
328 EVERY(replicate GEN_TAC 3) THEN INDUCT_TAC THEN ASM_REWRITE_TAC[prod];
330 REWRITE_TAC[REAL_MUL_AC];
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`,
338 EVERY(replicate GEN_TAC 3) THEN INDUCT_TAC THEN ASM_REWRITE_TAC[prod;pow];
340 REWRITE_TAC[REAL_MUL_AC];
344 (* ------------------------------------------------------------------ *)
345 (* LEMMAS ABOUT SETS *)
346 (* ------------------------------------------------------------------ *)
348 (* IN_ELIM_THM produces garbled results at times. I like this better: *)
350 (*** JRH replaced this with the "new" IN_ELIM_THM; see how it works.
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)`,
359 REWRITE_TAC[IN; GSPEC];
366 let IN_ELIM_THM' = IN_ELIM_THM;;
368 let SURJ_IMAGE = prove_by_refinement(
369 `!(f:A->B) a b. SURJ f a b ==> (b = (IMAGE f a))`,
374 REWRITE_TAC[SURJ;IMAGE];
376 REWRITE_TAC[EXTENSION];
378 REWRITE_TAC[IN_ELIM_THM];
385 let SURJ_FINITE = prove_by_refinement(
386 `!a b (f:A->B). FINITE a /\ (SURJ f a b) ==> FINITE b`,
390 ASM_MESON_TAC[SURJ_IMAGE;FINITE_IMAGE]
395 let BIJ_INVERSE = prove_by_refinement(
396 `!a b (f:A->B). (SURJ f a b) ==> (?(g:B->A). (INJ g b a))`,
402 SUBGOAL_THEN `!y. ?u. ((y IN b) ==> ((u IN a) /\ ((f:A->B) u = y)))` ASSUME_TAC;
405 H_REWRITE_RULE[THM SKOLEM_THM] (HYP "1");
407 H_UNDISCH_TAC (HYP"2");
408 DISCH_THEN CHOOSE_TAC;
410 REWRITE_TAC[INJ] THEN CONJ_TAC THEN (ASM_MESON_TAC[])
416 (* complement of an intersection is a union of complements *)
417 let UNIONS_INTERS = prove_by_refinement(
419 (X DIFF (INTERS V) = UNIONS (IMAGE ((DIFF) X) V))`,
424 MATCH_MP_TAC SUBSET_ANTISYM;
426 REWRITE_TAC[SUBSET;IMAGE;IN_ELIM_THM];
428 REWRITE_TAC[IN_DIFF;IN_INTERS;IN_UNIONS;NOT_FORALL_THM];
430 UNDISCH_FIND_THEN `(?)` CHOOSE_TAC;
431 EXISTS_TAC `(X DIFF t):A->bool`;
432 REWRITE_TAC[IN_ELIM_THM];
434 EXISTS_TAC `t:A->bool`;
436 REWRITE_TAC[IN_DIFF];
438 REWRITE_TAC[SUBSET;IMAGE;IN_ELIM_THM];
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];
445 UNDISCH_FIND_THEN `(?)` CHOOSE_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];
455 let INTERS_SUBSET = prove_by_refinement (
456 `!X (A:A->bool). (A IN X) ==> (INTERS X SUBSET A)`,
460 REWRITE_TAC[SUBSET;IN_INTERS];
465 let sub_union = prove_by_refinement(
466 `!X (U:(A->bool)->bool). (U X) ==> (X SUBSET (UNIONS U))`,
470 REWRITE_TAC[SUBSET;IN_ELIM_THM;UNIONS];
473 EXISTS_TAC `X:A->bool`;
478 let IMAGE_SURJ = prove_by_refinement(
479 `!(f:A->B) a. SURJ f a (IMAGE f a)`,
482 REWRITE_TAC[SURJ;IMAGE;IN_ELIM_THM];
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))`,
493 EXISTS_TAC `{x | (x IN (X:A->bool))/\ (f x IN (Y:B->bool)) }`;
495 REWRITE_TAC[SUBSET;IN_ELIM_THM];
497 REWRITE_TAC[EXTENSION];
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));
507 let UNIONS_INTER = prove_by_refinement(
508 `!(U:(A->bool)->bool) A. (((UNIONS U) INTER A) =
509 (UNIONS (IMAGE ((INTER) A) U)))`,
513 MATCH_MP_TAC (prove(`((C SUBSET (B:A->bool)) /\ (C SUBSET A) /\ ((A INTER B) SUBSET C)) ==> ((B INTER A) = C)`,SET_TAC[]));
515 REWRITE_TAC[SUBSET;UNIONS;IN_ELIM_THM];
516 REWRITE_TAC[IN_IMAGE];
518 REWRITE_TAC[SUBSET;UNIONS;IN_IMAGE];
520 REWRITE_TAC[IN_ELIM_THM];
522 DISCH_THEN CHOOSE_TAC;
523 ASM_MESON_TAC[IN_INTER];
524 REWRITE_TAC[IN_INTER];
525 REWRITE_TAC[IN_ELIM_THM];
528 UNDISCH_FIND_THEN `(?)` CHOOSE_TAC;
529 EXISTS_TAC `A INTER (u:A->bool)`;
534 let UNIONS_SUBSET = prove_by_refinement(
535 `!U (X:A->bool). (!A. (A IN U) ==> (A SUBSET X)) ==> (UNIONS U SUBSET X)`,
543 let SUBSET_INTER = prove_by_refinement(
544 `!X A (B:A->bool). (X SUBSET (A INTER B)) <=> (X SUBSET A) /\ (X SUBSET B)`,
547 REWRITE_TAC[SUBSET;INTER;IN_ELIM_THM];
552 let EMPTY_EXISTS = prove_by_refinement(
553 `!X. ~(X = {}) <=> (? (u:A). (u IN X))`,
556 REWRITE_TAC[EXTENSION];
557 REWRITE_TAC[IN;EMPTY];
562 let UNIONS_UNIONS = prove_by_refinement(
563 `!A B. (A SUBSET B) ==>(UNIONS (A:(A->bool)->bool) SUBSET (UNIONS B))`,
566 REWRITE_TAC[SUBSET;UNIONS;IN_ELIM_THM];
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))`,
579 REWRITE_TAC[EXTENSION;IN_UNIONS];
581 REWRITE_TAC[EXTENSION;IN_UNIONS];
583 DISCH_THEN (CHOOSE_THEN MP_TAC);
586 DISCH_THEN CHOOSE_TAC;
587 EXISTS_TAC `UNIONS (t':(A->bool)->bool)`;
588 REWRITE_TAC[IN_UNIONS;IN_IMAGE];
590 EXISTS_TAC `(t':(A->bool)->bool)`;
593 DISCH_THEN CHOOSE_TAC;
595 REWRITE_TAC[IN_IMAGE];
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)`;
605 EXISTS_TAC `x':(A->bool)->bool`;
612 let INTERS_SUBSET2 = prove_by_refinement(
613 `!X A. (?(x:A->bool). (A x /\ (x SUBSET X))) ==> ((INTERS A) SUBSET X)`,
616 REWRITE_TAC[SUBSET;INTERS;IN_ELIM_THM'];
622 (**** New proof by JRH; old one breaks because of new set comprehensions
624 let INTERS_EMPTY = prove_by_refinement(
625 `INTERS EMPTY = (UNIV:A->bool)`,
628 REWRITE_TAC[INTERS;NOT_IN_EMPTY;IN_ELIM_THM';];
629 REWRITE_TAC[UNIV;GSPEC];
632 REWRITE_TAC[IN_ELIM_THM'];
639 let INTERS_EMPTY = prove_by_refinement(
640 `INTERS EMPTY = (UNIV:A->bool)`,
643 let preimage = new_definition `preimage dom (f:A->B)
644 Z = {x | (x IN dom) /\ (f x IN Z)}`;;
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)`,
650 REWRITE_TAC[preimage];
651 REWRITE_TAC[IN_ELIM_THM']
655 (* Partial functions, which we identify with functions that
656 take the canonical choice of element outside the domain. *)
658 let supp = new_definition
659 `supp (f:A->B) = \ x. ~(f x = (CHOICE (UNIV:B ->bool)) )`;;
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))) `;;
667 let reflexive = new_definition
668 `reflexive (f:A->A->bool) <=> (!x. f x x)`;;
670 let symmetric = new_definition
671 `symmetric (f:A->A->bool) <=> (!x y. f x y ==> f y x)`;;
673 let transitive = new_definition
674 `transitive (f:A->A->bool) <=> (!x y z. f x y /\ f y z ==> f x z)`;;
676 let equivalence_relation = new_definition
677 `equivalence_relation (f:A->A->bool) <=>
678 (reflexive f) /\ (symmetric f) /\ (transitive f)`;;
680 (* We do not introduce the equivalence class of f explicitly, because
681 it is represented directly in HOL by (f a) *)
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))))`;;
687 let DIFF_DIFF2 = prove_by_refinement(
688 `!X (A:A->bool). (A SUBSET X) ==> ((X DIFF (X DIFF A)) = A)`,
693 (*** Old proof replaced by JRH: no longer UNWIND_THM[12] clause in IN_ELIM_THM
695 let GSPEC_THM = prove_by_refinement(
696 `!P (x:A). (?y. P y /\ (x = y)) <=> P x`,
697 [REWRITE_TAC[IN_ELIM_THM]]);;
701 let GSPEC_THM = prove_by_refinement(
702 `!P (x:A). (?y. P y /\ (x = y)) <=> P x`,
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[]);;
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]]);;
727 let NUM_COUNTABLE = prove_by_refinement(
728 `COUNTABLE (UNIV:num->bool)`,
732 REWRITE_TAC[COUNTABLE;CARD_GE_REFL];
737 let NUM2_COUNTABLE = prove_by_refinement(
738 `COUNTABLE {((x:num),(y:num)) | T}`,
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'];
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'`;
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");
759 DISCH_THEN (fun t -> REWRITE_TAC[t]);
762 CONV_TAC (quant_left_CONV "a");
766 USE 1 (SPECL [`0`;`t:num`]);
767 UND 1 THEN REDUCE_TAC;
768 DISCH_THEN (X_CHOOSE_TAC `n:num`);
770 USE 0 (SPEC `n:num`);
773 DISCH_THEN (fun t-> REWRITE_TAC[GSYM t]);
774 CONV_TAC (ONCE_DEPTH_CONV GEN_BETA_CONV);
782 REWRITE_TAC [ARITH_RULE `SUC t = t+|1`];
784 ABBREV_TAC `t' = SUC t`;
785 USE 2 (SPEC `SUC b`);
789 REWRITE_TAC[ARITH_RULE `SUC a +| b = a +| SUC b`];
790 DISCH_THEN (X_CHOOSE_TAC `n:num`);
793 USE 0 (SPEC `n:num`);
796 DISCH_THEN (fun t->REWRITE_TAC[GSYM t]);
797 CONV_TAC (ONCE_DEPTH_CONV GEN_BETA_CONV);
800 DISCH_THEN (fun t->REWRITE_TAC[t]);
801 REWRITE_TAC[ARITH_RULE `SUC a = a+| 1`];
805 let COUNTABLE_UNIONS = prove_by_refinement(
806 `!A:(A->bool)->bool. (COUNTABLE A) /\
807 (!a. (a IN A) ==> (COUNTABLE a)) ==> (COUNTABLE (UNIONS A))`,
812 USE 0 (REWRITE_RULE[COUNTABLE;GE_C;IN_UNIV]);
814 USE 0 (CONV_RULE (quant_left_CONV "x"));
815 USE 0 (CONV_RULE (quant_left_CONV "x"));
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"));
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))`;
825 USE 1 (SPEC `a:A->bool`);
826 USE 0 (SPEC `a:A->bool`);
827 EXISTS_TAC `(x:(A->bool)->num) a`;
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)`));
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)))`;
838 DISCH_THEN (CHOOSE_THEN MP_TAC);
840 USE 3 (SPEC `t:A->bool`);
842 UND 3 THEN (ASM_REWRITE_TAC[]);
843 REPEAT (DISCH_THEN(CHOOSE_THEN (MP_TAC)));
845 USE 2 (SPEC `(u:num,v:num)`);
846 SUBGOAL_TAC `?x' y'. (u:num,v:num) = (x',y')`;
851 DISCH_THEN (CHOOSE_THEN (ASSUME_TAC o GSYM));
857 let COUNTABLE_IMAGE = prove_by_refinement(
858 `!(A:A->bool) (B:B->bool) . (COUNTABLE A) /\ (?f. (B SUBSET IMAGE f A)) ==>
862 REWRITE_TAC[COUNTABLE;GE_C;IN_UNIV;IN_ELIM_THM';SUBSET];
865 USE 1 (REWRITE_RULE[IMAGE;IN_ELIM_THM']);
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)`;
875 DISCH_THEN CHOOSE_TAC;
877 UND 0 THEN (ASM_REWRITE_TAC[]) THEN DISCH_TAC;
882 let COUNTABLE_CARD = prove_by_refinement(
883 `!(A:A->bool) (B:B->bool). (COUNTABLE A) /\ (A >=_c B) ==>
889 MATCH_MP_TAC COUNTABLE_IMAGE;
890 EXISTS_TAC `A:A->bool`;
892 REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM'];
893 USE 1 (REWRITE_RULE[GE_C]);
901 let COUNTABLE_NUMSEG = prove_by_refinement(
902 `!n. COUNTABLE {x | x <| n}`,
906 REWRITE_TAC[COUNTABLE;GE_C;IN_UNIV];
907 EXISTS_TAC `I:num->num`;
909 REWRITE_TAC[IN_ELIM_THM'];
914 let FINITE_COUNTABLE = prove_by_refinement(
915 `!(A:A->bool). (FINITE A) ==> (COUNTABLE A)`,
919 USE 0 (MATCH_MP FINITE_HAS_SIZE_LEMMA);
921 ASSUME_TAC(SPEC `n:num` COUNTABLE_NUMSEG);
923 USE 0 (MATCH_MP COUNTABLE_CARD);
928 let num_infinite = prove_by_refinement(
929 `~ (FINITE (UNIV:num->bool))`,
933 USE 0 (REWRITE_RULE[]);
934 USE 0 (MATCH_MP num_FINITE_AVOID);
935 USE 0 (REWRITE_RULE[IN_UNIV]);
940 let num_SEG_UNION = prove_by_refinement(
941 `!i. ({u | i <| u} UNION {m | m <=| i}) = UNIV`,
945 SUBGOAL_TAC `({u | i <| u} UNION {m | m <=| i}) = UNIV`;
948 REWRITE_TAC[UNIV;UNION;IN_ELIM_THM'];
954 let num_above_infinite = prove_by_refinement(
955 `!i. ~ (FINITE {u | i <| u})`,
960 USE 0 (REWRITE_RULE[]);
961 ASSUME_TAC(SPEC `i:num` FINITE_NUMSEG_LE);
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];
969 REWRITE_TAC[num_infinite];
973 let INTER_FINITE = prove_by_refinement(
974 `!s (t:A->bool). (FINITE s ==> FINITE(s INTER t)) /\ (FINITE t ==> FINITE (s INTER t))`,
978 CONV_TAC (quant_right_CONV "t");
979 CONV_TAC (quant_right_CONV "s");
982 SUBGOAL_TAC `s INTER t SUBSET (s:A->bool)`;
984 ASM_MESON_TAC[FINITE_SUBSET];
985 MESON_TAC[INTER_COMM];
990 let num_above_finite = prove_by_refinement(
991 `!i J. (FINITE (J INTER {u | (i <| u)})) ==> (FINITE J)`,
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];
998 ASM (ONCE_REWRITE_TAC)[];
999 REWRITE_TAC[FINITE_UNION];
1001 MP_TAC (SPEC `i:num` FINITE_NUMSEG_LE);
1002 REWRITE_TAC[INTER_FINITE];
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))`,
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"));
1022 USE 1 (CONV_RULE REDUCE_CONV);
1023 ASM_REWRITE_TAC[SUBSET];
1026 SUBGOAL_TAC `?j'. j = SUC j'`;
1027 DISJ_CASES_TAC (SPEC `j:num` num_CASES);
1032 DISCH_THEN CHOOSE_TAC;
1034 USE 0 (SPEC `j':num`);
1035 USE 1(SPECL [`j':num`;`i:num`]);
1037 SUBGOAL_TAC `(n = j'-|i)`;
1042 SUBGOAL_TAC `(i<=| j')`;
1043 USE 2 (MATCH_MP(ARITH_RULE `(SUC n = j -| i) ==> (0 < j -| i)`));
1051 ASM_MESON_TAC[SUBSET_TRANS];
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))`,
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"));
1071 USE 1 (CONV_RULE REDUCE_CONV);
1072 ASM_REWRITE_TAC[SUBSET];
1075 SUBGOAL_TAC `?j'. j = SUC j'`;
1076 DISJ_CASES_TAC (SPEC `j:num` num_CASES);
1081 DISCH_THEN CHOOSE_TAC;
1083 USE 0 (SPEC `j':num`);
1084 USE 1(SPECL [`j':num`;`i:num`]);
1086 SUBGOAL_TAC `(n = j'-|i)`;
1091 SUBGOAL_TAC `(i<=| j')`;
1092 USE 2 (MATCH_MP(ARITH_RULE `(SUC n = j -| i) ==> (0 < j -| i)`));
1100 ASM_MESON_TAC[SUBSET_TRANS];
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) }))`,
1112 USE 3 ( CONV_RULE (quant_left_CONV "b"));
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;
1119 REWRITE_TAC[IN_ELIM_THM'];
1120 ABBREV_TAC `j = (x:A)`;
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]);
1129 CONV_TAC (quant_left_CONV "x");
1130 CONV_TAC (quant_left_CONV "x");
1131 EXISTS_TAC (`u:B->bool`);
1133 EXISTS_TAC (`{i' | I' i' /\ (C INTER u) ((f:A->B) i')}`);
1135 REWRITE_TAC[IN_ELIM_THM';INTER];
1143 USE 4 (REWRITE_RULE[IN_ELIM_THM';INTER]);
1144 USE 4 (REWRITE_RULE[IN]);
1148 SUBGOAL_TAC `FINITE (IMAGE (\b. {i | I' i /\ (C INTER b) ((f:A->B) i)}) B)`;
1149 MATCH_MP_TAC FINITE_IMAGE;
1151 SIMP_TAC[FINITE_UNIONS];
1154 REWRITE_TAC[IN_IMAGE];
1155 DISCH_THEN (X_CHOOSE_TAC `b:B->bool`);
1157 USE 3 (SPEC `b:B->bool`);
1161 ABBREV_TAC `r = {i | I' i /\ (C INTER b) ((f:A->B) i)}`;
1166 let real_FINITE = prove_by_refinement(
1167 `!(s:real->bool). FINITE s ==> (?a. !x. x IN s ==> (x <=. a))`,
1171 ASSUME_TAC REAL_ARCH_SIMPLE;
1172 USE 1 (CONV_RULE (quant_left_CONV "n"));
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);
1179 ASSUME_TAC(fst(EQ_IMP_RULE(SPEC `IMAGE (n:real->num) s` num_FINITE)));
1183 USE 2 (REWRITE_RULE[IN_IMAGE]);
1184 USE 2 (CONV_RULE NAME_CONFLICT_CONV);
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`);
1193 USE 1 (SPEC `x:real`);
1195 MATCH_MP_TAC (REAL_ARITH `a<=b ==> ((x <= a) ==> (x <=. b))`);
1201 let UNIONS_DELETE = prove_by_refinement(
1202 `!s. (UNIONS (s:(A->bool)->bool)) = (UNIONS (s DELETE (EMPTY)))`,
1205 REWRITE_TAC[UNIONS;DELETE;EMPTY];
1207 MATCH_MP_TAC EQ_EXT;
1208 REWRITE_TAC[IN_ELIM_THM'];
1216 (* ------------------------------------------------------------------ *)
1217 (* Partial functions, which we identify with functions that
1218 take the canonical choice of element outside the domain. *)
1219 (* ------------------------------------------------------------------ *)
1221 let SUPP = new_definition
1222 `SUPP (f:A->B) = \ x. ~(f x = (CHOICE (UNIV:B ->bool)) )`;;
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))) `;;
1228 (* ------------------------------------------------------------------ *)
1230 (* ------------------------------------------------------------------ *)
1232 let compose = new_definition
1233 `compose f g = \x. (f (g x))`;;
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)`,
1241 REPEAT GEN_TAC THEN REWRITE_TAC[compose];
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)`,
1250 EVERY[REPEAT GEN_TAC;
1251 REWRITE_TAC[INJ;compose];
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)`,
1260 EVERY[REWRITE_TAC[SURJ;compose];
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)`,
1273 ASM_MESON_TAC[COMP_INJ;COMP_SURJ]]);;
1278 (* ------------------------------------------------------------------ *)
1279 (* general construction of an inverse function on a domain *)
1280 (* ------------------------------------------------------------------ *)
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))))`,
1288 REWRITE_TAC[GSYM SKOLEM_THM];
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];
1293 SUBGOAL_TAC `?u. !y. ((y IN b)==> ((u y IN a) /\ ((f:A->B) (u y) = y)))`;
1294 REWRITE_TAC[GSYM SKOLEM_THM];
1297 DISCH_THEN CHOOSE_TAC;
1298 EXISTS_TAC `u:B->A`;
1303 FIRST_X_ASSUM (fun th -> ASSUME_TAC (AP_TERM `f:A->B` th));
1310 let INVERSE_DEF = new_specification ["INV"] INVERSE_FN;;
1312 let INVERSE_BIJ = prove_by_refinement(
1313 `!(f:A->B) a b. (BIJ f a b) ==> ((BIJ (INV f a b) b a))`,
1319 ASM_SIMP_TAC[INVERSE_DEF];
1322 ASM_MESON_TAC[INVERSE_DEF;INJ];
1323 GEN_TAC THEN DISCH_TAC;
1324 EXISTS_TAC `(f:A->B) x`;
1327 SUBGOAL_THEN `((f:A->B) x) IN b` ASSUME_TAC;
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");
1334 FIRST_X_ASSUM (fun th -> MP_TAC (SPECL [`INV (f:A->B) a b (f x)`;`x:A`] th));
1337 SUBGOAL_THEN `INV (f:A->B) a b (f x) IN a` ASSUME_TAC;
1338 ASM_MESON_TAC[INVERSE_DEF;INJ];
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))`,
1350 FIRST_X_ASSUM (fun th -> (ASSUME_TAC th THEN (ASSUME_TAC (MATCH_MP INVERSE_DEF (CONJUNCT2 (REWRITE_RULE[BIJ] th))))));
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;
1357 IMP_RES_THEN ASSUME_TAC INVERSE_BIJ;
1358 ASM_MESON_TAC[BIJ;INJ];
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;
1366 let FINITE_BIJ = prove(
1367 `!a b (f:A->B). FINITE a /\ (BIJ f a b) ==> (FINITE b)`,
1370 MESON_TAC[SURJ_IMAGE;BIJ;INJ;FINITE_IMAGE]
1375 let FINITE_INJ = prove_by_refinement(
1376 `!a b (f:A->B). FINITE b /\ (INJ f a b) ==> (FINITE a)`,
1382 MP_TAC (SPECL [`f:A->B`;`b:B->bool`;`a:A->bool`] FINITE_IMAGE_INJ_GENERAL);
1384 SUBGOAL_THEN `(a:A->bool) SUBSET ({x | (x IN a) /\ ((f:A->B) x IN b)})` ASSUME_TAC;
1385 REWRITE_TAC[SUBSET];
1387 REWRITE_TAC[IN_ELIM_THM];
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)})` ;
1393 FIRST_X_ASSUM (fun th -> MATCH_MP_TAC th);
1395 ASM_MESON_TAC[BIJ;INJ];
1403 let FINITE_BIJ2 = prove_by_refinement(
1404 `!a b (f:A->B). FINITE b /\ (BIJ f a b) ==> (FINITE a)`,
1408 MESON_TAC[BIJ;FINITE_INJ]
1412 let BIJ_CARD = prove_by_refinement(
1413 `!a b (f:A->B). FINITE a /\ (BIJ f a b) ==> (CARD a = (CARD b))`,
1417 ASM_MESON_TAC[SURJ_IMAGE;BIJ;INJ;CARD_IMAGE_INJ];
1422 let PAIR_LEMMA = prove_by_refinement(
1423 `!(x:num#num) i j. ((FST x = i) /\ (SND x = j)) <=> (x = (i,j))` ,
1427 MESON_TAC[FST;SND;PAIR];
1431 let CARD_SING = prove_by_refinement(
1432 `!(u:A->bool). (SING u ) ==> (CARD u = 1)`,
1437 DISCH_THEN (CHOOSE_TAC);
1439 ASSUME_TAC FINITE_RULES;
1440 ASM_SIMP_TAC[CARD_CLAUSES;NOT_IN_EMPTY];
1441 ACCEPT_TAC (NUM_RED_CONV `SUC 0`)
1445 let FINITE_SING = prove_by_refinement(
1446 `!(x:A). FINITE ({x})`,
1450 MESON_TAC[FINITE_RULES]
1454 let NUM_INTRO = prove_by_refinement(
1455 `!f P.((!(n:num). !(g:A). (f g = n) ==> (P g)) ==> (!g. (P g)))`,
1462 H_VAL (SPECL [`(f:A->num) (g:A)`; `g:A`]) (HYP "0");
1469 (* ------------------------------------------------------------------ *)
1470 (* Lemmas about the support of a function *)
1471 (* ------------------------------------------------------------------ *)
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))) }`,
1480 REWRITE_TAC[EXTENSION;FUN];
1482 REWRITE_TAC[IN_ELIM_THM;INSERT;NOT_IN_EMPTY;SUBSET_EMPTY;SUPP];
1484 ONCE_REWRITE_TAC[EXTENSION];
1487 DISCH_TAC THEN (MATCH_MP_TAC EQ_EXT);
1490 DISCH_TAC THEN (ASM_REWRITE_TAC[]) THEN BETA_TAC;
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) }
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))`;
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];
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`;
1518 EXPAND_TAC "g" THEN BETA_TAC;
1520 REWRITE_TAC[IN;COND_ELIM_THM];
1523 EXPAND_TAC "g" THEN BETA_TAC;
1525 ASM_CASES_TAC `(x:A) = s`;
1532 REWRITE_TAC[FUN;SUPP];
1534 X_GEN_TAC `f1:A->B`;
1535 X_GEN_TAC `f2:A->B`;
1538 MATCH_MP_TAC EQ_EXT;
1540 ASM_CASES_TAC `(x:A) = s`;
1541 POPL_TAC[1;2;3;4;6;7];
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`))));
1548 H_UNDISCH_TAC (HYP "0");
1553 REWRITE_TAC[FUN;SUPP;IN_ELIM_THM];
1554 REWRITE_TAC[IN;INSERT;SUBSET];
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;
1563 EXISTS_TAC `\ (x:A). if (x = s) then (v:B) else (u x)`;
1567 REWRITE_TAC[IN_ELIM_THM;COND_ELIM_THM];
1572 REWRITE_TAC[IN_ELIM_THM;COND_ELIM_THM];
1573 ASM_CASES_TAC `(t:A) = s`;
1574 POPL_TAC[1;3;4;5;6];
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[])];
1584 MATCH_MP_TAC EQ_EXT;
1587 DISJ_CASES_TAC (prove(`(((t:A)=s) <=> T) \/ ((t=s) <=> F)`,MESON_TAC[]));
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))`,
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];
1610 let dets_flag = ref true;;
1611 dets_flag:= !labels_flag;;
1615 labels_flag:=false;;
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)))`,
1624 MATCH_MP_TAC (SPEC `CARD:(A->bool)->num` ((INST_TYPE) [`:A->bool`,`:A`] NUM_INTRO));
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];
1634 REWRITE_TAC[FINITE_SING];
1635 MATCH_MP_TAC CARD_SING;
1639 FIRST_X_ASSUM (fun th -> ASSUME_TAC (SPEC `(a:A->bool) DELETE (CHOICE a)` th)) ;
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];
1649 MESON_TAC[ ( ARITH_RULE `!n. (SUC n -| 1) = n`)];
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);
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))`);
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)`;
1671 MATCH_MP_TAC FINITE_PRODUCT;
1673 ASM_MESON_TAC[HAS_SIZE];
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)`;
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]
1692 labels_flag:= true;;
1695 (* ------------------------------------------------------------------ *)
1696 (* ------------------------------------------------------------------ *)
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 *)
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)))`);;
1709 (* pick out parts of n-tuples *)
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)))))))`);;
1724 (* ------------------------------------------------------------------ *)
1725 (* Basic Definitions of Euclidean Space, Metric Spaces, and Topology *)
1726 (* ------------------------------------------------------------------ *)
1728 (* ------------------------------------------------------------------ *)
1730 (* ------------------------------------------------------------------ *)
1732 let euclid_def = local_definition "euclid";;
1733 mk_local_interface "euclid";;
1736 ("+", `euclid'euclid_plus:(num->real)->(num->real)->(num->real)`);;
1738 make_overloadable "*#" `:A -> B -> B`;;
1740 let euclid_scale = euclid_def
1741 `euclid_scale t f = \ (i:num). (t*. (f i))`;;
1743 overload_interface ("*#",`euclid'euclid_scale`);;
1745 parse_as_infix("*#",(20,"right"));;
1747 let euclid_neg = euclid_def `euclid_neg f = \ (i:num). (--. (f i))`;;
1749 (* This is highly ambiguous: -- f x can be read as
1750 (-- f) x or as -- (f x). *)
1751 overload_interface ("--",`euclid'euclid_neg`);;
1754 ("-", `euclid'euclid_minus:(num->real)->(num->real)->(num->real)`);;
1756 (* ------------------------------------------------------------------ *)
1757 (* Euclidean Space *)
1758 (* ------------------------------------------------------------------ *)
1760 let euclid_plus = euclid_def
1761 `euclid_plus f g = \ (i:num). (f i) +. (g i)`;;
1763 let euclid = euclid_def `euclid n v <=> !m. (n <=| m) ==> (v m = &.0)`;;
1765 let euclidean = euclid_def `euclidean v <=> ?n. euclid n v`;;
1767 let euclid_minus = euclid_def
1768 `euclid_minus f g = \(i:num). (f i) -. (g i)`;;
1770 let euclid0 = euclid_def `euclid0 = \(i:num). &.0`;;
1772 let coord = euclid_def `coord i (f:num->real) = f i`;;
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))`;;
1778 let norm = euclid_def `norm f = sqrt(dot f f)`;;
1780 let d_euclid = euclid_def `d_euclid f g = norm (f - g)`;;
1784 (* ------------------------------------------------------------------ *)
1785 (* Euclidean and Convex geometry *)
1786 (* ------------------------------------------------------------------ *)
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))`,
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);
1801 let sum_vector = new_specification ["sum_vector"] sum_vector_EXISTS;;
1803 let mk_segment = euclid_def
1804 `mk_segment x y = { u | ?a. (&.0 <=. a) /\ (a <=. &.1) /\
1805 (u = a *# x + (&.1 - a) *# y) }`;;
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) }`;;
1811 let convex = euclid_def
1812 `convex S <=> !x y. (S x) /\ (S y) ==> (mk_segment x y SUBSET S)`;;
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)))}`;;
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)))}`;;
1824 let mk_line = euclid_def `mk_line x y =
1825 {z| ?t. (z = (t *# x) + ((&.1 - t) *# y)) }`;;
1827 let affine = euclid_def
1828 `affine S <=> !x y. (S x ) /\ (S y) ==> (mk_line x y SUBSET S)`;;
1830 let affine_dim = euclid_def
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))`;;
1835 let collinear = euclid_def
1836 `collinear S <=> (?n. affine_dim n S /\ (n < 2))`;;
1838 let coplanar = euclid_def
1839 `coplanar S <=> (?n. affine_dim n S /\ (n < 3))`;;
1841 let line = euclid_def
1842 `line L <=> (affine L) /\ (affine_dim 1 L)`;;
1844 let plane = euclid_def
1845 `plane P <=> (affine P) /\ (affine_dim 2 P)`;;
1847 let space = euclid_def
1848 `space R <=> (affine R) /\ (affine_dim 3 R)`;;
1852 General constructor of conical objects, including
1853 rays, cones, half-planes, etc.
1855 L is the edge. C is the set of generators in the positive
1858 If L is a line, and C = {c}, we get the half-plane bounded by
1861 If L is a point, and C is general, we get the cone at L generated
1864 If L and C are both singletons, we get the ray ending at L.
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)) }`;;
1873 let mk_half_set = euclid_def
1875 { u | ?t v c. (L v) /\ (S c) /\ (&.0 <=. t) /\
1876 (u = (t *# (c - v) + (&.1 - t) *# v)) }`;;
1879 let mk_angle = euclid_def `mk_angle x y z =
1880 (mk_half_set {x} {y}) UNION (mk_half_set {x} {z})`;;
1882 let mk_signed_angle = euclid_def `mk_signed_angle x y z =
1883 (mk_half_set {x} {y} , mk_half_set {x} {z})`;;
1885 let mk_convex_cone = euclid_def
1886 `mk_convex_cone v (S:(num->real)->bool) =
1887 mk_half_set {v} (convex_hull S)`;;
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))) ==>
1894 let saturated_packing = euclid_def(`saturated_packing S <=>
1896 (!z. (affine_hull S z) ==>
1897 (?x. ((S x) /\ ((d_euclid x z) < (&.2))))))`);;
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
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)
1910 let triple_product = euclid_def(`triple_product v1 v2 v3 =
1911 dot v1 (cross_product3 v2 v3)`);;
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)`;;
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})`;;
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)`;;
1929 (* ------------------------------------------------------------------ *)
1930 (* Statements of Theorems in Euclidean Geometry (no proofs *)
1931 (* ------------------------------------------------------------------ *)
1933 let half_set_convex = `!L S. convex (mk_half_set L S)`;;
1935 let open_half_set_convex = `!L S . convex (mk_open_half_set L S )`;;
1937 let affine_dim0 = `!S. (affine_dim 0 S) = (SING S)`;;
1939 let hull_convex = `!S. (convex (convex_hull S))`;;
1941 let hull_minimal = `!S T. (convex T) /\ (S SUBSET T) ==>
1942 (convex_hull S) SUBSET T`;;
1944 let affine_hull_affine = `!S. (affine (affine_hull S))`;;
1946 let affine_hull_minimal = `!S T. (affine T) /\ (S SUBSET T) ==>
1947 (affine_hull S) SUBSET T`;;
1949 let mk_line_dim = `!x y. ~(x = y) ==> affine_dim 1 (mk_line x y)`;;
1951 let affine_convex_hull = `!S. (affine_hull S) = (affine_hull (convex_hull S))`;;
1953 let convex_hull_hull = `!S. (convex_hull S) = (convex_hull (convex_hull S))`;;
1955 let euclid_affine_dim = `!n. affine_dim n (euclid n)`;;
1957 let affine_dim_subset = `!m n T S.
1958 (affine_dim m T) /\ (affine_dim n S) /\ (T SUBSET S) ==> (m <= n)`;;
1960 (* A few of the Birkhoff postulates of Geometry (incomplete) *)
1962 let line_postulate = `!x y. ~(x = y) ==>
1963 (?!L. (L x) /\ (L y) /\ (line L))`;;
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)))))`;;
1969 let affine_postulate = `!n. (affine_dim n P) ==> (?S.
1970 (S SUBSET P) /\ (S HAS_SIZE n) /\ (affine_dim n S))`;;
1972 let line_plane = `!P x y. (plane P) /\ (P x) /\ (P y) ==>
1973 (mk_line x y SUBSET P)`;;
1975 let plane_of_pt = `!S. (S HAS_SIZE 3) ==> (?P. (plane P) /\
1978 let plane_of_pt_unique = `!S. (S HAS_SIZE 3) ==> (collinear S) \/
1979 (?! P. (plane P) /\ (S SUBSET P))`;;
1981 let plane_inter = `!P Q. (plane P) /\ (plane Q) ==>
1982 (P INTER Q = EMPTY) \/ (line (P INTER Q)) \/ (P = Q)`;;
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)))`;;
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)))`;;
2001 (* ------------------------------------------------------------------ *)
2003 (* ------------------------------------------------------------------ *)
2005 let metric_space = euclid_def `metric_space (X:A->bool,d:A->A->real)
2008 (X x) /\ (X y) /\ (X z) ==>
2009 (((&.0) <=. (d x y)) /\
2010 ((&.0 = d x y) = (x = y)) /\
2012 (d x z <=. d x y + d y z))`;;
2014 (* ------------------------------------------------------------------ *)
2016 (* ------------------------------------------------------------------ *)
2018 let set_translate = euclid_def
2019 `set_translate v X = { z | ?x. (X x) /\ (z = v + x) }`;;
2021 let set_scale = euclid_def
2022 `set_scale r X = { z | ?x. (X x) /\ (z = r *# x) }`;;
2024 let mk_rectangle = euclid_def
2025 `mk_rectangle a b = { z | !(i:num). (a i <=. z i) /\ (z i <. b i) }`;;
2027 let one_vec = euclid_def
2028 `one_vec n = (\i. if (i<| n) then (&.1) else (&.0))`;;
2030 let mk_cube = euclid_def
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)))`;;
2036 let inner_cube = euclid_def
2038 { v | (mk_cube n k v SUBSET A) /\
2039 (!i. (n <| i) ==> (&:0 = v i)) }`;;
2041 let outer_cube = euclid_def
2043 { v | ~((mk_cube n k v) INTER A = EMPTY) /\
2044 (!i. (n <| i) ==> (&:0 = v i)) }`;;
2046 let inner_vol = euclid_def
2048 (&. (CARD (inner_cube n k A)))*(twopow (--: (&: (n*k))))`;;
2050 let outer_vol = euclid_def
2052 (&. (CARD (outer_cube n k A)))*(twopow (--: (&: (n*k))))`;;
2054 let euclid_bounded = euclid_def
2055 `euclid_bounded A = (?R. !(x:num->real) i. (A x) ==> (x i <. R))`;;
2057 let vol = euclid_def
2058 `vol n A = lim (\k. outer_vol n k A)`;;
2060 (* ------------------------------------------------------------------ *)
2062 (* ------------------------------------------------------------------ *)
2064 unambiguous_interface();;
2067 (* ------------------------------------------------------------------ *)
2068 (* general series approximations *)
2069 (* ------------------------------------------------------------------ *)
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)))))))`,
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;
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;
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]
2096 let SER_APPROX = prove_by_refinement(
2097 `!s f g. (f sums s) /\ (!n. (||. (f n) <=. (g n))) /\
2099 (!k. (abs (s - (sum(0,k) f)) <=. (suminf (\n. (g (n +| k))))))`,
2105 REWRITE_TAC[REAL_ABS_BOUNDS];
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;
2110 MATCH_MP_TAC SER_NEG ;
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));
2116 ASM_REWRITE_TAC[REAL_ABS_NEG];
2117 H_VAL2 CONJ (HYP "0") (HYP "2");
2118 IMP_RES_THEN MATCH_MP_TAC SER_APPROX1 ;
2124 (* ------------------------------------------------------------------ *)
2125 (* now for pi calculation stuff *)
2126 (* ------------------------------------------------------------------ *)
2129 let local_def = local_definition "trig";;
2132 let PI_EST = prove_by_refinement(
2133 `!n. (1 <=| n) ==> (abs(&4 / &(8 * n + 1) -
2136 &1 / &(8 * n + 6)) <= &.622/(&.819))`,
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
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))`;;
2157 let pi_bound_fun = local_def `pi_bound_fun n = if (n=0) then (&.8) else
2158 (((&.15)/(&.16))*(inv(&.16 **. n))) `;;
2160 let PI_EST2 = prove_by_refinement(
2161 `!k. abs(pi_fun k) <=. (pi_bound_fun k)`,
2165 REWRITE_TAC[pi_fun;pi_bound_fun];
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);
2177 SIMP_TAC[REAL_POW_LT;REAL_LT_INV;ARITH_RULE `&.0 < (&.16)`];
2178 ASM_MESON_TAC[REAL_LE_TRANS];
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`,
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];
2195 let GP16a = prove_by_refinement(
2196 `!k. (0<|k) ==> (\n. (pi_bound_fun (n+k))) sums (inv(&.16 **. k))`,
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];
2206 ASM_MESON_TAC[ARITH_RULE `0<| k ==> (~(n+k = 0))`];
2207 REWRITE_TAC[GSYM REAL_MUL_ASSOC];
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)`);
2219 CONV_TAC (REAL_RAT_REDUCE_CONV);
2223 let PI_SER = prove_by_refinement(
2224 `!k. (0<|k) ==> (abs(pi - (sum(0,k) pi_fun)) <=. (inv(&.16 **. (k))))`,
2227 GEN_TAC THEN DISCH_TAC;
2228 ASSUME_TAC (ONCE_REWRITE_RULE[ETA_AX] (REWRITE_RULE[GSYM pi_fun] POLYLOG_THM));
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);
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];
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')));;
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]);;
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)))));;
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`);;
2273 (* ------------------------------------------------------------------ *)
2274 (* restore defaults *)
2275 (* ------------------------------------------------------------------ *)
2277 reduce_local_interface("trig");;