Update from HH
[hl193./.git] / 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