1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALISATION *)
6 (* Author: Vuong Anh Quyen *)
8 (* ========================================================================== *)
11 flyspeck_needs "hypermap/hypermap.hl";;
12 flyspeck_needs "fan/fan_defs.hl";;
13 flyspeck_needs "fan/planarity.hl";;
14 flyspeck_needs "leg/geomdetail.hl";;
15 flyspeck_needs "packing/pack2.hl";; (* for KIUMVTC *)
16 flyspeck_needs "packing/pack_defs.hl";; (* for h0 def and others *)
17 flyspeck_needs "trigonometry/trig1.hl";;
18 flyspeck_needs "general/prove_by_refinement.hl";;
19 flyspeck_needs "tame/tame_concl.hl";;
20 flyspeck_needs "tame/tame_defs.hl";; (* was commented out *)
22 module Fatugpd = struct
34 open Prove_by_refinement;;
36 let JBDNJJB = Planarity.JBDNJJB;;
40 let UBHDEUU2_concl = Tame_concl.UBHDEUU2_concl;;
42 let UBHDEUU2_hypothesis = new_definition (mk_eq(`UBHDEUU2_hypothesis:bool`,UBHDEUU2_concl));;
44 let UBHDEUU2_quasi = UNDISCH(MATCH_MP (TAUT `(x = y) ==> (x ==> y)`) UBHDEUU2_hypothesis);;
49 let Q_LABEL_TAC term phr = UNDISCH_THEN term (LABEL_TAC phr);;
51 let Q_ABBREV_TAC term str = (ABBREV_TAC term) THEN
52 FIRST_X_ASSUM (LABEL_TAC str);;
54 let Q_EXPAND_TAC str = (USE_THEN str (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));;
56 (* some of my lemmas that may help others *)
57 let NOT_EMPTY_IMAGE = prove
58 ( ` !(S:A -> bool) (f:A->B). ~( S = {}) ==> ~( IMAGE f S = {})`, SET_TAC[]);;
60 (* lemma about sup of function on finite set *)
61 let finite_num_func_attain_max =
63 `! (S:A->bool) (f:A->num). FINITE S /\ ~ (S = {})
64 ==> (? x. x IN S /\ (! y. y IN S ==> f y <= f x))`,
70 ` FINITE (IMAGE (& o(f:A->num)) (S:A->bool)) /\ ~ (IMAGE (& o f) S = {})`
74 (ASM_SIMP_TAC[FINITE_IMAGE]);
76 (ASM_SIMP_TAC[NOT_EMPTY_IMAGE]);
78 (FIRST_ASSUM(MP_TAC o (MATCH_MP SUP_FINITE)));
79 (CONV_TAC(PAT_CONV `\k. _ IN k /\ _ ==> _` (REWRITE_CONV[IMAGE])));
80 (PURE_REWRITE_TAC[IN_ELIM_THM]);
85 (FIRST_X_ASSUM(MP_TAC o SPEC ` (& o (f:A->num)) y`));
88 (SUBGOAL_THEN ` (& o (f:A->num)) y IN IMAGE (& o f) S` ASSUME_TAC);
89 (PURE_REWRITE_TAC[IMAGE;IN_ELIM_THM]);
90 (EXISTS_TAC `y:A` THEN ASM_SIMP_TAC[]);
92 (ASM_SIMP_TAC[o_THM; REAL_OF_NUM_LE]);
96 (* lemma about property of sup *)
97 let sup_property1 = prove_by_refinement(
98 `! (S:real->bool). ~(S = {}) /\(?b. !x. x IN S ==> x <= b) ==>
99 (! epsilon. epsilon > &0 ==> ?x. x IN S /\ x > sup S - epsilon)`,
101 (GEN_TAC THEN DISCH_THEN (MP_TAC o (MATCH_MP SUP)));
102 (STRIP_TAC THEN GEN_TAC);
103 (DISCH_THEN (ASSUME_TAC o (MATCH_MP (ARITH_RULE
104 ` epsilon > &0 ==> ~ ( sup (S:real->bool) <= sup S - epsilon)`))));
105 (MATCH_MP_TAC (MESON[]
106 `! (P:A->bool) (Q:A->bool). ~(!(x:A). P x ==> ~ (Q x))
107 ==> (?(x:A). P x /\ Q x)`));
108 (PURE_REWRITE_TAC[ARITH_RULE
109 `~(x > sup S - epsilon) <=> x <= sup S - epsilon`]);
110 (ASM_MESON_TAC[]);]);;
113 (* lemma about maximal of num bounded function *)
115 let bdd_num_func_attain_max = prove_by_refinement(
116 `! (S:A ->bool) (f:A-> num). ~(S = {})/\(?m. !x. x IN S ==> f x <= m)
117 ==> (?x. x IN S /\ (!y. y IN S ==> f y <= f x))`,
121 (SUBGOAL_THEN `~( IMAGE (& o (f:A->num)) (S:A->bool) = {})
122 /\ (? b. ! y. y IN (IMAGE (& o f) S) ==> y <= b)` ASSUME_TAC);
129 (EXISTS_TAC `& (m:num)`);
130 (PURE_REWRITE_TAC[IN_ELIM_THM;IMAGE;o_THM]);
132 (ONCE_ASM_REWRITE_TAC[]);
133 (ASM_SIMP_TAC[REAL_OF_NUM_LE]);
135 (FIRST_ASSUM (MP_TAC o MATCH_MP SUP));
136 (ABBREV_TAC `p = sup (IMAGE (& o (f:A->num)) (S:A->bool))` THEN STRIP_TAC);
139 `?z. z IN (IMAGE (& o (f:A->num)) (S:A->bool)) /\ z > p - &1` MP_TAC);
141 (FIRST_ASSUM (MP_TAC o (SPEC `&1`) o (MATCH_MP sup_property1)));
142 (SIMP_TAC[ARITH_RULE `&1 > &0`]);
144 (PURE_REWRITE_TAC[IN_ELIM_THM;IMAGE;o_THM] THEN STRIP_TAC );
146 (ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);
147 (MATCH_MP_TAC (ARITH_RULE ` n < (m:num) + 1 ==> n <= m`));
150 `&((f:A->num) y) IN (IMAGE (& o f) (S:A->bool))` ASSUME_TAC);
151 (ASM_SIMP_TAC[IN_ELIM_THM;o_THM;IMAGE]);
156 (SUBGOAL_THEN `&((f:A->num) y) <= p` ASSUME_TAC);
160 (fst(EQ_IMP_RULE (SPECL [`(f:A->num) y`;`f x + 1`] REAL_OF_NUM_LT))));
161 (PURE_REWRITE_TAC[GSYM REAL_OF_NUM_ADD]);
166 let BIJ_CARD_EQ = prove
167 ( `! (V:A->bool) (U:B->bool) (f:A->B). FINITE V /\ BIJ f V U
168 ==> CARD U = CARD V`,
169 REPEAT GEN_TAC THEN REWRITE_TAC[BIJ;INJ;SURJ] THEN STRIP_TAC THEN
170 MATCH_MP_TAC CARD_EQ_CARD_IMP THEN ASM_SIMP_TAC[] THEN
171 ONCE_REWRITE_TAC[CARD_EQ_SYM] THEN REWRITE_TAC[eq_c]
172 THEN EXISTS_TAC `f:A->B` THEN ASM_MESON_TAC[]);;
175 (* another property of sup *)
176 let SUP_lt = prove_by_refinement(
177 `! (S:real -> bool) (b:real).
178 ~(S = {}) /\ FINITE S /\ (!x. x IN S ==> x < b) ==> sup S < b`,
181 (FIRST_ASSUM (fun thm -> (MATCH_MP_TAC thm)));
182 (ASM_SIMP_TAC[SUP_FINITE]);
187 let epsilon_lemma = prove_by_refinement(
188 `! (a:real) b. a < b ==> ? epsilon. epsilon > &0 /\ b > a + epsilon`,
191 (EXISTS_TAC `(b - a) / &2`);
195 let normalize = new_definition `!(v:real^N). normalize v = inv (norm v) % v`;;
197 let norm_normalize = prove_by_refinement(
198 `! (v:real^3). ~(v = vec 0) ==> norm (normalize v) = &1 `,
200 (GEN_TAC THEN STRIP_TAC);
201 (PURE_REWRITE_TAC[normalize;NORM_MUL;REAL_ABS_INV;REAL_ABS_NORM]);
202 (MATCH_MP_TAC REAL_MUL_LINV);
203 (ASM_MESON_TAC[NORM_EQ_0]);
207 let normalize_vec_0 = prove_by_refinement(
208 `normalize (vec 0:real^N) = (vec 0:real^N)`,
209 [(PURE_REWRITE_TAC[normalize;REAL_INV_0;NORM_0;VECTOR_MUL_LZERO]);
210 VECTOR_ARITH_TAC;]);;
213 let norm_mul_normalize = prove_by_refinement(
214 `! (v:real^3).(norm v) % (normalize v) = v`,
217 (ASM_CASES_TAC `v:real^3 = vec 0`);
220 (ASM_SIMP_TAC[normalize_vec_0; VECTOR_MUL_RZERO]);
223 (PURE_REWRITE_TAC[normalize;VECTOR_MUL_ASSOC]);
224 (SUBGOAL_THEN `~(norm (v:real^3) = &0)` (ASSUME_TAC o MATCH_MP REAL_MUL_RINV));
225 (ASM_MESON_TAC[NORM_EQ_0]);
226 (ASM_SIMP_TAC[VECTOR_MUL_LID]);]);;
229 let dot_normalize = prove_by_refinement(
230 `! v:real^3. v dot (normalize v) = norm v`,
233 (ASM_CASES_TAC `v:real^3 = vec 0`);
236 (ASM_SIMP_TAC[NORM_0;DOT_LZERO]);
239 (SUBGOAL_THEN ` norm (v:real^3) * (v dot normalize v) = norm v pow 2` MP_TAC);
240 (ONCE_REWRITE_TAC[GSYM DOT_RMUL]);
241 (ASM_SIMP_TAC[norm_mul_normalize;DOT_SQUARE_NORM]);
243 (ONCE_REWRITE_TAC[REAL_POW_2]);
244 (MATCH_MP_TAC (REWRITE_RULE [TAUT `A /\ B ==> C <=> A ==> (B ==> C)`] REAL_EQ_LCANCEL_IMP));
245 (ASM_SIMP_TAC[NORM_EQ_0]);]);;
248 let fourier = prove_by_refinement(
249 ` ! (v:real^3) (e1:real^3) e2 e3. orthonormal e1 e2 e3
250 ==> v = (v dot e1) % e1 + (v dot e2) % e2 + (v dot e3) % e3`,
253 (FIRST_ASSUM (ASSUME_TAC o (MATCH_MP ORTHONORMAL_IMP_SPANNING)));
254 (UNDISCH_TAC `orthonormal (e1:real^3) e2 e3`);
255 (ONCE_REWRITE_TAC[orthonormal]);
257 (ABBREV_TAC `(u:real^3) = (v dot e1) % e1 + (v dot e2) % e2 + (v dot e3) % e3`);
259 (SUBGOAL_THEN ` (v:real^3) dot e1 = u dot e1 ` ASSUME_TAC);
261 (ASM_SIMP_TAC[DOT_LADD;DOT_LMUL;DOT_SYM;REAL_MUL_RZERO;
262 REAL_ADD_RID;REAL_MUL_RID]);
265 (SUBGOAL_THEN ` (v:real^3) dot e2 = u dot e2 ` ASSUME_TAC);
267 (ASM_SIMP_TAC[DOT_LADD;DOT_LMUL;DOT_SYM;REAL_MUL_RZERO;
268 REAL_ADD_RID;REAL_MUL_RID;REAL_ADD_LID]);
271 (SUBGOAL_THEN ` (v:real^3) dot e3 = u dot e3 ` ASSUME_TAC);
273 (ASM_SIMP_TAC[DOT_LADD;DOT_LMUL;DOT_SYM;REAL_MUL_RZERO;
274 REAL_ADD_RID;REAL_MUL_RID;REAL_ADD_LID]);
277 (SUBGOAL_THEN `(v:real^3) - u IN span {e1:real^3, e2, e3}` MP_TAC);
280 (SIMP_TAC[SPAN_3;IN_ELIM_THM;IN_UNIV]);
284 (SUBGOAL_THEN `((v:real^3) - u) dot (v - u) = &0` MP_TAC);
285 (PURE_REWRITE_TAC[DOT_LSUB]);
286 (ASM_SIMP_TAC[DOT_RMUL;DOT_RADD;REAL_SUB_REFL]);
288 (ASM_SIMP_TAC[DOT_EQ_0;VECTOR_SUB_EQ]);]);;
291 let norm_lemma1 = prove_by_refinement(
292 `! (v:real^3) (e1:real^3) e2 e3. orthonormal e1 e2 e3 ==>
293 norm v = sqrt ((v dot e1) pow 2 + (v dot e2) pow 2 + (v dot e3) pow 2)`,
296 (PURE_REWRITE_TAC[vector_norm]);
297 (FIRST_ASSUM (ASSUME_TAC o MATCH_MP fourier));
298 (FIRST_ASSUM (fun thm -> CONV_TAC (PAT_CONV `\x. sqrt (x dot x) = _` (ONCE_REWRITE_CONV[thm]))));
299 (PURE_REWRITE_TAC[DOT_RADD;DOT_LADD;DOT_RMUL;DOT_LMUL;
300 REAL_ADD_RDISTRIB;REAL_ADD_LDISTRIB]);
301 (ONCE_REWRITE_TAC[REAL_MUL_ASSOC]);
302 (ONCE_REWRITE_TAC[GSYM REAL_POW_2]);
303 (FIRST_ASSUM (MP_TAC o MATCH_MP
304 (fst (EQ_IMP_RULE (SPECL [`e1:real^3`;`e2:real^3`;`e3:real^3`] orthonormal)))));
306 (ASM_SIMP_TAC[DOT_SYM;REAL_MUL_RZERO;REAL_ADD_RID;
307 REAL_ADD_LID;REAL_MUL_RID]);]);;
310 let coordinates_lemma = prove_by_refinement(
311 `! (v:real^3) (e1:real^3) e2 e3 (x:real) y z. orthonormal e1 e2 e3 /\
312 v = x % e1 + y % e2 + z % e3 ==>
313 x = v dot e1 /\ y = v dot e2 /\ z = v dot e3`,
317 (FIRST_ASSUM (fun thm -> MP_TAC (SPEC `v:real^3` (MATCH_MP fourier thm))));
318 (ASM_MESON_TAC[ORTHONORMAL_IMP_INDEPENDENT_EXPLICIT]);]);;
321 let dot_coordinates = prove_by_refinement(
322 `! v:real^3 u e1 e2 e3. orthonormal e1 e2 e3
323 ==> v dot u = (v dot e1) * (u dot e1) + (v dot e2) * (u dot e2)
324 + (v dot e3) * (u dot e3)`,
327 (FIRST_ASSUM((LABEL_TAC "a") o (MATCH_MP (SPEC `u:real^3` fourier))));
328 (USE_THEN "a" (fun thm -> (CONV_TAC (PAT_CONV `\x. A dot x = B`
329 (ONCE_REWRITE_CONV[thm])))));
330 (ONCE_REWRITE_TAC[VECTOR_ARITH `(v:real^3) dot (a % e1 + b % e2 + c % e3) =
331 (v dot e1) * a + (v dot e2 ) * b + (v dot e3) * c`]);
335 let dot_coordinates_2 = prove_by_refinement(
336 `! (v:real^3) u e1 e2 e3 x y z a b c. orthonormal e1 e2 e3 /\
337 v = x % e1 + y % e2 + z % e3 /\ u = a % e1 + b % e2 + c % e3
338 ==> v dot u = x * a + y * b + z * c`,
339 [(ONCE_REWRITE_TAC[orthonormal]);
341 (ONCE_ASM_REWRITE_TAC[]);
342 (ASM_SIMP_TAC[DOT_SYM;DOT_LADD;DOT_RADD;DOT_LMUL;DOT_RMUL]);
346 let norm_lemma2 = prove_by_refinement(
347 `! (v:real^3) e1 e2 e3 x y z. orthonormal e1 e2 e3 /\
348 v = x % e1 + y % e2 + z % e3 ==>
349 norm v = sqrt (x pow 2 + y pow 2 + z pow 2)`,
353 (FIRST_ASSUM (fun thm -> ONCE_REWRITE_TAC [ MATCH_MP norm_lemma1 (CONJUNCT1 thm)]));
354 (FIRST_ASSUM (fun thm -> SIMP_TAC[ MATCH_MP coordinates_lemma thm]));]);;
357 let dot_gt_0 = prove_by_refinement(
358 `! v:real^3 u. &0 < v dot u <=> &0 < v dot normalize u `,
361 (ASM_CASES_TAC `u:real^3 = vec 0`);
364 (ASM_SIMP_TAC[normalize_vec_0]);
367 ( CONV_TAC(PAT_CONV `\x. &0 < A dot x <=> B`(ONCE_REWRITE_CONV[GSYM norm_mul_normalize])));
368 (PURE_REWRITE_TAC[DOT_RMUL]);
369 (MATCH_MP_TAC (CONJUNCT1 REAL_LT_MUL_EQ));
370 (MATCH_MP_TAC (REAL_ARITH `&0 <= x /\ ~(x = &0) ==> &0 < x`));
371 (ASM_SIMP_TAC[NORM_POS_LE;NORM_EQ_0]);]);;
374 let dot_eq_0 = prove_by_refinement(
375 `! v:real^3 u. v dot u = &0 <=> (normalize v) dot u = &0`,
378 (ASM_CASES_TAC `v:real^3 = vec 0`);
381 (ASM_SIMP_TAC[normalize_vec_0]);
384 (CONV_TAC(PAT_CONV `\x. x dot y = &0 <=> A`
385 (ONCE_REWRITE_CONV[GSYM norm_mul_normalize])));
386 (ONCE_REWRITE_TAC[DOT_LMUL]);
387 (CONV_TAC(PAT_CONV `\x. x <=> A` (ONCE_REWRITE_CONV
388 [ARITH_RULE `&0 = norm (v:real^3) * &0`])));
389 (ONCE_REWRITE_TAC[REAL_EQ_MUL_LCANCEL]);
390 (ASM_SIMP_TAC[NORM_EQ_0]);]);;
393 let azim_ge_azim_dart = prove_by_refinement(
394 `! (V:real^3->bool) E w u v. FAN (vec 0, V, E) /\ w IN V /\
395 u IN set_of_edge w V E /\ v IN set_of_edge w V E /\ ~(w = u) /\ ~(v = u)
396 ==> azim (vec 0) w u v >= azim_dart (V,E) (w,u)`,
399 (ASM_SIMP_TAC[azim_dart]);
400 (PURE_REWRITE_TAC[azim_fan]);
403 (SUBGOAL_THEN `CARD (set_of_edge (w:real^3) V E) > 1` ASSUME_TAC);
404 (MP_TAC (SPECL [`vec 0:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;
405 `u:real^3`;`w:real^3`] Fan.remark1_fan));
408 (MP_TAC(ISPECL [`v:real^3`;`u:real^3`] Hypermap.CARD_TWO_ELEMENTS));
410 (MATCH_MP_TAC (ARITH_RULE `(a:num) <= b ==> a = 2 ==> b > 1`));
411 (MATCH_MP_TAC CARD_SUBSET);
416 (SUBGOAL_THEN `~(set_of_edge (w:real^3) V E = {u})` ASSUME_TAC);
417 (ONCE_REWRITE_TAC[TAUT ` ~A <=> A ==> F`]);
418 (DISCH_THEN (MP_TAC o (AP_TERM `(\(S:real^3->bool). CARD S)`)));
419 (SIMP_TAC[BETA_THM;Geomdetail.CARD_SING]);
421 (MP_TAC (SPECL [`vec 0 :real^3`;`V:real^3 -> bool`;
422 `E:(real^3->bool)->bool`;`w:real^3`;`u:real^3`] Fan.SIGMA_FAN));
425 (ASM_SIMP_TAC[ARITH_RULE `a >= b <=> b <= a`]);]);;
430 (* definitions in the proof *)
432 let set_of_iso = new_definition
433 ` set_of_iso W = {w| w IN W /\ set_of_edge w W (ECTC W) = {}}`;;
436 (* lemmas prepared for the proof *)
437 let lemma1 = prove_by_refinement(
438 `! (S:real^3->bool). packing S /\ S SUBSET ball_annulus ==> FINITE S`,
443 (SUBGOAL_THEN ` (S:real^3->bool) = S INTER ball (vec 0,&3 * h0)` ASSUME_TAC);
445 (MATCH_MP_TAC (SET_RULE `! U V. U SUBSET ball_annulus /\ ball_annulus SUBSET V ==> (U = U INTER V)`));
446 (ASM_SIMP_TAC[ball_annulus;ball;cball;IN_DIFF;SUBSET;IN_ELIM_THM;h0]);
448 (MATCH_MP_TAC (ARITH_RULE ` u <= &2 * #1.26 ==> u < &3 * #1.26`));
451 (ONCE_ASM_REWRITE_TAC[]);
452 (ASM_SIMP_TAC[KIUMVTC]);]);;
455 let lemma2 = prove_by_refinement(
456 `! (V:real^3 -> bool) v. packing V /\ FINITE V /\ v IN V
457 ==> ? epsilon. epsilon > &0 /\
458 (! w. w IN V /\ ~(w = v) /\ ~(w IN set_of_edge v V (ECTC V))
459 ==> dist (v,w) > &2 + epsilon )`,
462 (ABBREV_TAC `(S:real^3->bool) = {w|w IN V /\ ~(w = v) /\ ~(w IN set_of_edge v V (ECTC V))}`);
464 (ASM_CASES_TAC `(S:real^3 ->bool) = {}`);
468 (SIMP_TAC[ARITH_RULE `&1 > &0`]);
471 (SUBGOAL_THEN `~((S:real^3->bool) = {})` ASSUME_TAC);
479 (SUBGOAL_THEN `FINITE (S:real^3 -> bool)` ASSUME_TAC);
481 (ISPECL [`(S:real^3-> bool)`;`(V:real^3 ->bool)`] FINITE_SUBSET));
484 (ABBREV_TAC `(f:real^3 -> real) = (\w. dist (v,w))`);
486 (SUBGOAL_THEN `&2 < inf (IMAGE (f:real^3 -> real) (S:real^3 ->bool))` ASSUME_TAC);
489 `FINITE (IMAGE (f:real^3 ->real) S) /\ ~ (IMAGE f S = {})` ASSUME_TAC);
490 (ASM_SIMP_TAC[FINITE_IMAGE;NOT_EMPTY_IMAGE]);
492 (ASM_SIMP_TAC[REAL_LT_INF_FINITE]);
494 (PURE_REWRITE_TAC[IN_ELIM_THM;IMAGE]);
496 (ONCE_ASM_REWRITE_TAC[]);
498 (MATCH_MP_TAC (ARITH_RULE `! (a:real). &2 <= a /\ ~(&2 = a) ==> &2 < a`));
501 (UNDISCH_TAC `packing (V:real^3 -> bool)`);
502 (PURE_REWRITE_TAC[packing]);
503 (DISCH_THEN (fun thm -> MATCH_MP_TAC (ISPECL [`x':real^3`;`v:real^3`] thm)));
507 (SUBGOAL_THEN `&2 = dist (v,x') ==> (x' IN set_of_edge v V (ECTC V))` ASSUME_TAC);
509 (PURE_REWRITE_TAC[set_of_edge]);
510 (ASM_SIMP_TAC[ECTC;IN_ELIM_THM]);
511 (EXISTS_TAC `v:real^3`);
512 (EXISTS_TAC `x':real^3`);
517 (FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP epsilon_lemma)));
518 (FIRST_X_ASSUM CHOOSE_TAC);
519 (EXISTS_TAC `epsilon:real`);
522 (MATCH_MP_TAC (ARITH_RULE `! u:real v w. u >= v /\ v > w ==> u > w`));
523 (EXISTS_TAC `inf (IMAGE (f:real^3 -> real) (S:real^3 -> bool))`);
527 (SUBGOAL_THEN `dist (v,w:real^3) IN (IMAGE (f:real^3 -> real) S)` ASSUME_TAC);
528 (PURE_REWRITE_TAC[IMAGE;IN_ELIM_THM]);
529 (EXISTS_TAC `w:real^3`);
534 (ASM_SIMP_TAC[IN_ELIM_THM]);
541 (SUBGOAL_THEN `~(IMAGE (f:real^3 -> real) S = {})
542 /\ (? b:real. !x. x IN (IMAGE f S) ==> b <= x )` ASSUME_TAC);
543 (ASM_SIMP_TAC[NOT_EMPTY_IMAGE]);
547 (PURE_REWRITE_TAC[IN_ELIM_THM;IMAGE]);
549 (ONCE_ASM_REWRITE_TAC[]);
551 (UNDISCH_TAC `packing (V:real^3 -> bool)`);
552 (PURE_REWRITE_TAC[packing]);
553 (DISCH_THEN (fun thm -> MP_TAC (ISPECL [`v:real^3`;`x':real^3`] thm)));
554 (MATCH_MP_TAC (TAUT `U ==> ((U ==> V)==> V) `));
556 (CONV_TAC (PAT_CONV `\x y. x /\ y /\ _ ` (ONCE_REWRITE_CONV[GSYM IN])));
558 (UNDISCH_TAC `(x':real^3) IN S`);
560 (PURE_REWRITE_TAC[IN_ELIM_THM]);
563 (FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP INF)));
564 (ONCE_REWRITE_TAC[ARITH_RULE `a >= b <=> b <= a`]);
565 (FIRST_X_ASSUM (fun thm -> MATCH_MP_TAC (CONJUNCT1 thm)));
566 (ASM_SIMP_TAC[]); ]);;
569 let lemma3 = prove_by_refinement(
570 `! (w:real^3) (W:real^3 -> bool). packing W /\ w IN W /\
571 ~(set_of_edge w W (ECTC W) = {}) /\ ~(surrounded_node (W,(ECTC W)) w)
572 ==> ?u. (u IN set_of_edge w W (ECTC W)) /\ (azim_dart (W, (ECTC W)) (w,u) >= pi)`,
574 (PURE_REWRITE_TAC[surrounded_node]);
575 (PURE_REWRITE_TAC[GSYM EXISTS_NOT_THM]);
576 (PURE_REWRITE_TAC[TAUT `~(A ==> B) <=> A /\ ~B`]);
577 (PURE_REWRITE_TAC[ARITH_RULE `~ (a < pi) <=> a >= pi`]);
578 (PURE_REWRITE_TAC[dart_of_fan]);
579 (PURE_REWRITE_TAC[SET_RULE `x IN A UNION B <=> x IN A \/ x IN B`]);
580 (SIMP_TAC[IN_ELIM_THM]);
584 (SUBGOAL_THEN `set_of_edge (w:real^3) (W:real^3 ->bool) (ECTC W) = {}` ASSUME_TAC);
585 (FIRST_X_ASSUM (fun thm -> ALL_TAC));
586 (FIRST_X_ASSUM (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
591 (EXISTS_TAC `SND (x:real^3 # real^3)`);
592 (Q_LABEL_TAC `FST (x:real^3 # real^3) = w` "a");
593 (USE_THEN "a" (fun thm -> SIMP_TAC[PAIR; GSYM thm]));
595 (PURE_REWRITE_TAC[IN_ELIM_THM;set_of_edge]);
598 (SUBGOAL_THEN `w:real^3 = v` (LABEL_TAC "b"));
599 (REMOVE_THEN "a" (fun thm -> PURE_REWRITE_TAC[GSYM thm]));
602 (UNDISCH_TAC `{v:real^3,w':real^3} IN ECTC (W:real^3 -> bool)`);
603 (REWRITE_TAC[ECTC;IN_ELIM_THM;Geomdetail.PAIR_EQ_EXPAND]);
610 (ASM_SIMP_TAC[]);]);;
614 let lemma4 = prove_by_refinement(
616 ~collinear {vec 0, w, u} /\ ~collinear {vec 0, w, v} /\
617 azim (vec 0) w u v >= pi
618 ==> (w cross u) dot v <= &0`,
621 (MP_TAC (SPECL [`w:real^3`;`u:real^3`;`v:real^3`] JBDNJJB));
624 (ABBREV_TAC `(a:real) = ((w:real^3) cross u) dot v`);
625 (MATCH_MP_TAC (SPECL [`t:real`;`a:real`;`&0`] REAL_LE_LCANCEL_IMP));
627 (Q_LABEL_TAC `sin (azim (vec 0) w u v ) = t * a` "b");
628 (USE_THEN "b" (fun thm -> (ONCE_REWRITE_TAC[GSYM thm; REAL_MUL_RZERO])));
631 (SUBGOAL_THEN `azim (vec 0 :real^3) w u v < &2 * pi` ASSUME_TAC);
632 (SIMP_TAC[SPECL [`vec 0:real^3`;`w:real^3`;`u:real^3`;`v:real^3`] azim]);
634 (ABBREV_TAC `b:real = azim (vec 0:real^3) w u v`);
635 (ONCE_REWRITE_TAC[ARITH_RULE `m <= &0 <=> &0 <= -- m `]);
636 (ONCE_REWRITE_TAC[GSYM SIN_NEG]);
637 (ONCE_REWRITE_TAC[GSYM SIN_PERIODIC]);
640 (SUBGOAL_THEN `-- pi < --b + &2 * pi /\ --b + &2 * pi <= pi` ASSUME_TAC);
643 (ABBREV_TAC `c:real = --b + &2 * pi`);
644 (FIRST_ASSUM (ASSUME_TAC o (MATCH_MP SIN_NEGPOS_PI)));
645 (ONCE_REWRITE_TAC[ARITH_RULE `&0 <= x <=> x = &0 \/ &0 < x`]);
646 (ONCE_ASM_REWRITE_TAC[]);
647 (MATCH_MP_TAC (ARITH_RULE ` (&0 <= c /\ c <= pi) ==> ((c = &0 \/ c = pi) \/ &0 < c /\ c < pi)`));
650 (MATCH_MP_TAC (ARITH_RULE `b < a ==> &0 <= --b + a`));
651 (ASM_SIMP_TAC[]);]);;
654 let lemma5 = prove_by_refinement(
655 `! (V:real^3 -> bool) v. packing V /\ V SUBSET ball_annulus /\ v IN V
656 ==> ! u. (u IN set_of_edge v V (ECTC V)) ==> v dot u > &0`,
660 (SUBGOAL_THEN `!(w:real^3). w IN V ==> w dot w >= &4` (LABEL_TAC "a"));
662 (MP_TAC (SET_RULE `(w:real^3) IN V /\ V SUBSET ball_annulus ==> w IN ball_annulus`));
664 (PURE_REWRITE_TAC[ball_annulus]);
665 (PURE_REWRITE_TAC[DIFF;ball;IN_ELIM_THM]);
666 (PURE_REWRITE_TAC[REAL_ARITH `~(a < &2) <=> a >= &2`]);
667 (PURE_REWRITE_TAC[dist; DIST_SYM;VECTOR_SUB_RZERO]);
668 (PURE_REWRITE_TAC[NORM_GE_SQUARE]);
670 (SIMP_TAC[ARITH_RULE `~(&2 <= &0) /\ &2 pow 2 = &4`]);
671 (MATCH_MP_TAC (ARITH_RULE `&2 * a > &0 ==> a > &0`));
672 (ONCE_REWRITE_TAC[VECTOR_ARITH `&2 * (v dot u) = v dot v + u dot u - (v - u) dot (v - u)`]);
675 (SUBGOAL_THEN `(v:real^3 - u) dot (v - u) = &4 /\ u IN V` MP_TAC);
676 (UNDISCH_TAC `u:real^3 IN set_of_edge v V (ECTC V)`);
677 (SIMP_TAC[set_of_edge;ECTC;IN_ELIM_THM]);
679 (ONCE_REWRITE_TAC[DOT_SQUARE_NORM]);
680 (ONCE_REWRITE_TAC[GSYM dist]);
681 (FIRST_ASSUM (MP_TAC o (MATCH_MP (fst (EQ_IMP_RULE Geomdetail.PAIR_EQ_EXPAND)))));
688 (ONCE_REWRITE_TAC[DIST_SYM]);
694 (MATCH_MP_TAC (ARITH_RULE `a >= &4 /\ b >= &4 ==> a + b - &4 > &0`));
695 (USE_THEN "a" (fun thm -> MP_TAC( SPEC `v:real^3` thm)));
696 (USE_THEN "a" (fun thm -> MP_TAC( SPEC `u:real^3` thm)));
697 (ASM_SIMP_TAC[]);]);;
700 let lemma6 = prove_by_refinement(
701 `! v:real^3 u (phi:real) e1 e2 e3. e1 = normalize v /\
702 orthonormal e1 e2 e3 /\
703 u = (cos phi * norm v) % e1 + (sin phi * norm v) % e2
704 ==> norm u = norm v`,
708 (SUBGOAL_THEN `orthonormal e1 e2 e3 /\
709 u:real^3 = (cos (phi:real) * norm (v:real^3)) % e1 + (sin phi * norm v) % e2 + &0 % e3` ASSUME_TAC);
713 (FIRST_X_ASSUM (ASSUME_TAC o MATCH_MP (SPECL [`u:real^3`;`e1:real^3`;`e2:real^3`;`e3:real^3`;
714 ` cos (phi:real) * norm (v:real^3)`;`sin (phi:real) * norm (v:real^3)`;`&0`]
716 (ONCE_ASM_REWRITE_TAC[]);
717 (ONCE_REWRITE_TAC[ARITH_RULE `( a * m) pow 2 + (b * m) pow 2 + &0 pow 2
718 = (b pow 2 + a pow 2) * m pow 2`]);
719 (SIMP_TAC[SIN_CIRCLE;REAL_MUL_LID]);
720 (MATCH_MP_TAC POW_2_SQRT);
721 (SIMP_TAC[NORM_POS_LE]);]);;
724 let lemma7 = prove_by_refinement(
725 `! v:real^3 u (phi:real) e1 e2 e3. e1 = normalize v /\
726 orthonormal e1 e2 e3 /\ &0 < phi /\ phi < pi /\ &0 < norm v /\
727 u = (cos phi * norm v) % e1 + (sin phi * norm v) % e2
728 ==> (! w:real^3. &0 < w dot e1 /\ w dot e2 <= &0
729 ==> dist (v,w) < dist (u,w))`,
732 (PURE_REWRITE_TAC[dist;NORM_LT]);
733 (ONCE_REWRITE_TAC[ARITH_RULE `a < b <=> &0 < b - a `]);
734 (ONCE_REWRITE_TAC[VECTOR_ARITH `(u - w) dot (u - w) - (v - w) dot (v - w) =
735 u dot u - v dot v - &2 * ((u - v) dot w )`]);
736 (ONCE_REWRITE_TAC[DOT_SQUARE_NORM]);
739 (SUBGOAL_THEN `norm (u:real^3) = norm (v:real^3)` ASSUME_TAC);
740 (MATCH_MP_TAC (SPECL [`v:real^3`;`u:real^3`;`phi:real`; `e1:real^3`;
741 `e2:real^3`;`e3:real^3`] lemma6));
744 (FIRST_ASSUM (fun thm -> SIMP_TAC[thm; ARITH_RULE `a - a - b = --b`]));
745 (ONCE_REWRITE_TAC[ARITH_RULE `&0 < --(&2 * a) <=> a < &0`]);
748 (SUBGOAL_THEN `v:real^3 = (norm v) % e1` (LABEL_TAC "v_coordinate"));
749 (ASM_SIMP_TAC[norm_mul_normalize]);
751 (Q_LABEL_TAC `orthonormal e1 e2 e3` "base");
752 (USE_THEN "base" (ASSUME_TAC o MATCH_MP (SPECL [`(u - v):real^3`;`w:real^3`;
753 `e1:real^3`;`e2:real^3`;`e3:real^3`] dot_coordinates)));
754 (ONCE_ASM_REWRITE_TAC[]);
757 (SUBGOAL_THEN `(u:real^3 - v) dot e1 = (cos phi - &1) * norm v /\
758 (u - v) dot e2 = sin phi * norm v /\ (u - v) dot e3 = &0` MP_TAC);
759 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
760 (MATCH_MP_TAC (SPECL [`u:real^3 - v`;`e1:real^3`;`e2:real^3`;`e3:real^3`;
761 `(cos phi - &1) * norm v`;`sin phi * norm v`;`&0`] coordinates_lemma));
762 (USE_THEN "base" (fun thm -> SIMP_TAC[thm]));
763 (USE_THEN "v_coordinate" (fun thm -> CONV_TAC( PAT_CONV
764 `\x. U - x = _` (ONCE_REWRITE_CONV[thm]))));
765 (Q_LABEL_TAC `u:real^3 = (cos phi * norm (v:real^3)) % e1 + (sin phi * norm v) % e2` "u");
766 (USE_THEN "u" (fun thm -> ONCE_REWRITE_TAC[thm]));
768 (DISCH_THEN (LABEL_TAC "c"));
769 (USE_THEN "c" (fun thm -> ONCE_REWRITE_TAC[thm]));
770 (PURE_REWRITE_TAC[REAL_MUL_LZERO;REAL_ADD_RID]);
771 (MATCH_MP_TAC (REAL_ARITH `a < &0 /\ b <= &0 ==> a + b < &0`));
775 (ONCE_REWRITE_TAC[REAL_ARITH
776 `((a - &1) * b) * c < &0 <=> &0 < ((&1 - a) * b) * c`]);
777 (MATCH_MP_TAC REAL_LT_MUL);
779 (MATCH_MP_TAC REAL_LT_MUL);
781 (ONCE_REWRITE_TAC[REAL_ARITH
782 `&0 < &1 - a <=> (a <= &1 /\ ~(a = &1))`]);
783 (SIMP_TAC[COS_BOUNDS;COS_ONE_2PI]);
784 (ONCE_REWRITE_TAC[ TAUT `~(A \/ B) <=> ~A /\ ~B`]);
788 (ONCE_REWRITE_TAC[TAUT `~A <=> A ==> F`]);
790 (FIRST_X_ASSUM(LABEL_TAC "phi"));
794 (SUBGOAL_THEN `0 < n:num` ASSUME_TAC);
795 (ONCE_REWRITE_TAC[GSYM REAL_OF_NUM_LT]);
796 (MATCH_MP_TAC (SPECL [`&0`;`&(n:num)`;`&2 * pi`]
797 REAL_LT_RCANCEL_IMP));
798 (SIMP_TAC[ARITH_RULE `&0 * &2 * pi = &0`;
799 ARITH_RULE `&0 < &2 * a <=> &0 < a`]);
800 (USE_THEN "phi" (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
801 (ASM_SIMP_TAC[PI_POS]);
804 (SUBGOAL_THEN `n:num < 1` ASSUME_TAC);
805 (ONCE_REWRITE_TAC[GSYM REAL_OF_NUM_LT]);
806 (MATCH_MP_TAC (SPECL [`&(n:num)`;`&1`;`&2 * pi`]
807 REAL_LT_RCANCEL_IMP));
808 (SIMP_TAC[ARITH_RULE `&1 * &2 * pi = &2 * pi`;
809 ARITH_RULE `&0 < &2 * a <=> &0 < a`]);
810 (USE_THEN "phi" (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
812 (MATCH_MP_TAC(ARITH_RULE `a < pi /\ pi < b ==> a < b`));
814 (MATCH_MP_TAC(ARITH_RULE `&0 < a ==> a < &2 * a`));
816 (ASM_MESON_TAC[ARITH_RULE `~(0 < n:num /\ n < 1)`]);
819 (ONCE_REWRITE_TAC[TAUT `~A <=> A ==> F`]);
821 (FIRST_X_ASSUM(LABEL_TAC "phi"));
823 (SUBGOAL_THEN `~(&0 < phi:real)` ASSUME_TAC);
824 (USE_THEN "phi" (fun thm -> ONCE_REWRITE_TAC[thm]));
825 (ONCE_REWRITE_TAC[ARITH_RULE `~(&0 < -- a) <=> &0 <= a`]);
826 (MATCH_MP_TAC REAL_LE_MUL);
827 (SIMP_TAC[REAL_POS]);
828 (MATCH_MP_TAC (ARITH_RULE `&0 < a ==> &0 <= a`));
829 (MATCH_MP_TAC REAL_LT_MUL);
835 (ONCE_REWRITE_TAC[ARITH_RULE `a * b <= &0 <=> &0 <= a * (--b)`]);
836 (MATCH_MP_TAC REAL_LE_MUL);
837 (ONCE_REWRITE_TAC[ARITH_RULE `&0 <= -- a <=> a <= &0`]);
839 (MATCH_MP_TAC REAL_LE_MUL);
840 (SIMP_TAC[NORM_POS_LE]);
841 (MATCH_MP_TAC SIN_POS_PI_LE);
845 let lemma8 = prove_by_refinement(
846 `! w:real^3 W:real^3->bool. w IN W
847 ==> set_of_edge w W (ECTC W) = {v| v IN W /\ dist (w,v) = &2}`,
850 (MATCH_MP_TAC SUBSET_ANTISYM);
854 (PURE_REWRITE_TAC[SUBSET]);
856 (SIMP_TAC[set_of_edge;ECTC;IN_ELIM_THM]);
858 (SUBGOAL_THEN `dist (w:real^3,x) = dist (v:real^3,w'')` ASSUME_TAC);
859 (MATCH_MP_TAC Geomdetail.DIST_PAIR_LEMMA);
864 (PURE_REWRITE_TAC[SUBSET]);
866 (SIMP_TAC[set_of_edge;ECTC;IN_ELIM_THM]);
868 (EXISTS_TAC `w:real^3`);
869 (EXISTS_TAC `x:real^3`);
871 (ONCE_REWRITE_TAC[DIST_NZ]);
877 let FATUGPD_quasi = prove_by_refinement( ` UBHDEUU2_hypothesis ==> (!V. packing V /\ V SUBSET ball_annulus
878 ==> (?W phi. BIJ phi V W /\ (!v. v IN V ==> norm(v) = norm(phi v)) /\
879 (!w. w IN W ==> (set_of_edge w W (ECTC W) = {}) \/ (surrounded_node (W,(ECTC W)) w))))`,
885 `S = {(U:real^3->bool)| FINITE U /\ packing U /\
886 (?phi. BIJ phi (V:real^3->bool) U /\
887 (! v. v IN V ==> norm v = norm (phi v)))}`);
889 `(f:(real^3 ->bool)->num) =
890 (\U. CARD (set_of_iso U))`);
893 (SUBGOAL_THEN `FINITE (V:real^3->bool)` (LABEL_TAC "finite_v"));
894 (ASM_SIMP_TAC[lemma1]);
897 (SUBGOAL_THEN `! (U:real^3 ->bool). U IN S ==> FINITE U` (LABEL_TAC "finite_u"));
899 (SIMP_TAC[IN_ELIM_THM]);
903 `~ ((S:(real^3->bool)->bool) = {}) /\
904 (?m. !U. U IN S ==> (f:(real^3->bool)->num) U <= m)` (LABEL_TAC "asm1"));
908 (PURE_REWRITE_TAC[GSYM MEMBER_NOT_EMPTY]);
909 (EXISTS_TAC `V:real^3->bool`);
911 (ASM_SIMP_TAC[IN_ELIM_THM]);
912 (EXISTS_TAC `(I:real^3->real^3)`);
916 (SIMP_TAC[BIJ;INJ;SURJ;I_THM]);
923 (EXISTS_TAC `CARD (V:real^3->bool)`);
927 (SUBGOAL_THEN `! (U:real^3->bool). U IN S ==> CARD U = CARD (V:real^3->bool)` MP_TAC);
930 (PURE_REWRITE_TAC[IN_ELIM_THM]);
932 (MATCH_MP_TAC BIJ_CARD_EQ);
933 (EXISTS_TAC `phi:real^3->real^3`);
936 (DISCH_THEN (MP_TAC o (fun thm -> (SPEC `U:real^3 ->bool` thm))));
937 (MATCH_MP_TAC (TAUT ` (p ==> (q ==> r)) ==> ((p ==> q) ==> (p ==> r))`));
941 (SUBGOAL_THEN `(f:(real^3->bool) -> num) U <= CARD U` ASSUME_TAC);
943 (MATCH_MP_TAC CARD_SUBSET);
946 (* subgoal 3.2.2.1 *)
947 (SET_TAC[set_of_iso]);
949 (* subgoal 3.2.2.2 *)
950 (UNDISCH_TAC `(U:real^3->bool) IN (S:(real^3->bool)->bool)`);
955 (REMOVE_THEN "asm1" (ASSUME_TAC o (MATCH_MP bdd_num_func_attain_max)));
956 (FIRST_X_ASSUM CHOOSE_TAC);
957 (EXISTS_TAC `U:real^3->bool`);
959 (FIRST_X_ASSUM MP_TAC);
961 (UNDISCH_TAC `U:real^3 -> bool IN S`);
963 (SIMP_TAC[IN_ELIM_THM]);
965 (EXISTS_TAC `phi:real^3 ->real^3`);
970 (SUBGOAL_THEN `! v:real^3. v IN U ==> norm v <= &2 * h0 /\ ~(norm v < &2)`
971 (LABEL_TAC "norm_bdd"));
973 (UNDISCH_TAC `BIJ phi (V:real^3->bool) (U:real^3->bool)`);
974 (PURE_REWRITE_TAC[BIJ;SURJ]);
977 (FIRST_ASSUM (fun thm -> MP_TAC (SPEC `v:real^3` thm)));
978 (FIRST_ASSUM (fun thm -> SIMP_TAC[thm]));
980 (UNDISCH_TAC `! v:real^3. v IN V ==> norm v = norm ((phi:real^3 -> real^3) v)`);
981 (DISCH_THEN (fun thm -> MP_TAC (SPEC `y:real^3` thm)));
983 (MATCH_MP_TAC (ARITH_RULE
984 `a <= &2 * h0 /\ ~(a < &2) ==> a = b ==> b <= &2 * h0 /\ ~(b < &2)`));
987 (SUBGOAL_THEN `y:real^3 IN ball_annulus` MP_TAC);
988 (MATCH_MP_TAC (SET_RULE `y:real^3 IN V /\ V SUBSET ball_annulus ==> y IN ball_annulus`));
991 (PURE_REWRITE_TAC[IN_ELIM_THM;ball_annulus;DIFF;cball;ball]);
995 (SUBGOAL_THEN `(U:real^3 -> bool) SUBSET ball_annulus` (LABEL_TAC "u_annu"));
996 (PURE_REWRITE_TAC[SUBSET]);
999 (PURE_REWRITE_TAC[IN_ELIM_THM;ball_annulus;DIFF;cball;ball]);
1004 (SUBGOAL_THEN `! v:real^3. v IN U ==> ~(v = vec 0)` (LABEL_TAC "not_0"));
1007 (ONCE_REWRITE_TAC[GSYM NORM_POS_LT]);
1008 (MATCH_MP_TAC (ARITH_RULE `~(norm (v:real^3) < &2) ==> &0 < norm v`));
1012 (SUBGOAL_THEN `!v:real^3. v IN set_of_edge w U (ECTC U)
1013 ==> ~(collinear {vec 0, w, v})` (LABEL_TAC "not_li"));
1015 (MP_TAC (SPECL [`w:real^3`;`U:real^3->bool`] lemma8));
1017 (SIMP_TAC[IN_ELIM_THM;ECTC]);
1018 (MATCH_MP_TAC (TAUT `(B ==> C) ==> (A ==> B ==> C)`));
1020 (ONCE_REWRITE_TAC[COLLINEAR_BETWEEN_CASES]);
1021 (ONCE_REWRITE_TAC[TAUT `~(A \/ B \/ C) <=> ~A /\ ~B /\ ~C`]);
1022 (ONCE_REWRITE_TAC[between]);
1023 (ONCE_REWRITE_TAC[DIST_0]);
1024 (CONV_TAC (PAT_CONV `\x. A /\ ~( _ = x + _ ) /\ ~( _ = _ + x)`
1025 (ONCE_REWRITE_CONV[DIST_SYM])));
1027 (MATCH_MP_TAC (ARITH_RULE
1028 `(a <= &2 * #1.26) /\ ~(a < &2) /\ (b <= &2 * #1.26) /\ ~(b < &2)
1029 ==> ~(&2 = a + b) /\ ~(b = &2 + a) /\ ~(a = b + &2)`));
1030 (ONCE_REWRITE_TAC[GSYM h0]);
1033 (ASM_CASES_TAC `~(set_of_edge (w:real^3) (U:real^3->bool) (ECTC U) = {}) /\
1034 ~(surrounded_node (U,ECTC U) w)`);
1036 (ABBREV_TAC `result:bool = (set_of_edge w U (ECTC U) = {} \/ surrounded_node (U,ECTC U) w)`);
1037 (MP_TAC (SPECL [`U:real^3 -> bool`;`w:real^3`] lemma2));
1040 (MP_TAC (SPECL[`w:real^3`;`U:real^3->bool`] lemma3));
1043 (Q_ABBREV_TAC `e1:real^3 = normalize w` "e1");
1044 (Q_ABBREV_TAC `y:real^3 = w cross u` "y_axis");
1045 (Q_ABBREV_TAC `e2:real^3 = normalize y` "e2");
1046 (Q_ABBREV_TAC `e3:real^3 = e1 cross e2` "e3");
1049 (SUBGOAL_THEN `orthonormal (e1:real^3) e2 e3` ASSUME_TAC);
1050 (PURE_REWRITE_TAC[orthonormal]);
1051 (ONCE_REWRITE_TAC[GSYM NORM_EQ_1]);
1053 (SUBGOAL_THEN `norm (e1:real^3) = &1` ASSUME_TAC);
1054 (Q_EXPAND_TAC "e1");
1055 (MATCH_MP_TAC norm_normalize);
1059 (SUBGOAL_THEN `norm (e2:real^3) = &1` ASSUME_TAC);
1060 (Q_EXPAND_TAC "e2");
1061 (MATCH_MP_TAC norm_normalize);
1062 (Q_EXPAND_TAC "y_axis");
1063 (ONCE_REWRITE_TAC[CROSS_EQ_0]);
1067 (SUBGOAL_THEN `(e1:real^3) dot e2 = &0` ASSUME_TAC);
1068 (Q_EXPAND_TAC "e1");
1069 (ONCE_REWRITE_TAC[GSYM dot_eq_0]);
1070 (Q_EXPAND_TAC "e2");
1071 (ONCE_REWRITE_TAC[DOT_SYM]);
1072 (ONCE_REWRITE_TAC[GSYM dot_eq_0]);
1073 (Q_EXPAND_TAC "y_axis");
1074 (SIMP_TAC[DOT_CROSS_SELF]);
1077 (SUBGOAL_THEN `(e1:real^3) dot e3 = &0 /\ e2 dot e3 = &0` ASSUME_TAC);
1078 (Q_EXPAND_TAC "e3");
1079 (SIMP_TAC[DOT_CROSS_SELF]);
1082 (SUBGOAL_THEN `norm (e3:real^3) = &1` ASSUME_TAC);
1083 (Q_EXPAND_TAC "e3");
1084 (MP_TAC(ISPECL [`e1:real^3`;`e2:real^3`] NORM_CROSS_DOT));
1085 (ASM_SIMP_TAC[REAL_POW_2;REAL_MUL_RZERO;REAL_ADD_RID;REAL_MUL_RID]);
1086 (ONCE_REWRITE_TAC[GSYM REAL_POW_2]);
1088 (MP_TAC(SPECL [`norm (e3:real^3)`;`2`] REAL_POW_EQ_1_IMP));
1089 (ASM_SIMP_TAC[ARITH_RULE `~(2 = 0)`]);
1091 (MATCH_MP_TAC (ARITH_RULE `abs x = &1 /\ &0 <= x ==> x = &1`));
1092 (ASM_SIMP_TAC[NORM_POS_LE]);
1095 (ONCE_REWRITE_TAC[DOT_SQUARE_NORM]);
1096 (ASM_SIMP_TAC[REAL_POW_2]);
1100 (SUBGOAL_THEN `!v:real^3. v IN set_of_edge w U (ECTC U)
1101 ==> v dot e2 <= &0` ASSUME_TAC);
1104 (ONCE_REWRITE_TAC[DOT_SYM]);
1105 (ONCE_REWRITE_TAC[ARITH_RULE `a <= &0 <=> &0 < --a \/ a = &0`]);
1106 (ONCE_REWRITE_TAC[VECTOR_ARITH `--((e2:real^3) dot v) = (--v) dot e2`]);
1107 (Q_EXPAND_TAC "e2");
1108 (ONCE_REWRITE_TAC[GSYM dot_gt_0]);
1109 (ONCE_REWRITE_TAC[GSYM dot_eq_0]);
1110 (ONCE_REWRITE_TAC[VECTOR_ARITH ` --(v:real^3) dot y = -- (y dot v)`]);
1111 (ONCE_REWRITE_TAC[ARITH_RULE ` (&0 < --a \/ a = &0 )<=> a <= &0`]);
1112 (Q_EXPAND_TAC "y_axis");
1113 (ASM_CASES_TAC `v:real^3 = u`);
1116 (FIRST_ASSUM(fun thm -> SIMP_TAC[thm;DOT_CROSS_SELF]));
1120 (MP_TAC (SPECL [`w:real^3`;`u:real^3`;`v:real^3`] lemma4));
1122 (MATCH_MP_TAC (TAUT `A ==> (A ==>B) ==> B`));
1123 (MP_TAC (SPEC `U:real^3 -> bool` UBHDEUU2_quasi));
1126 (MP_TAC (SPECL [`U:real^3->bool`;`(ECTC U):(real^3->bool)->bool`;`w:real^3`;
1127 `u:real^3`;`v:real^3`] azim_ge_azim_dart));
1131 (SUBGOAL_THEN `~(w:real^3 = u)` ASSUME_TAC);
1132 (UNDISCH_TAC `u:real^3 IN set_of_edge w U (ECTC U)`);
1133 (MP_TAC(SPECL [`w:real^3`;`U:real^3->bool`] lemma8));
1134 (ASM_SIMP_TAC[IN_ELIM_THM]);
1137 (ONCE_REWRITE_TAC[GSYM DIST_EQ_0]);
1144 (SUBGOAL_THEN `?(a:real). &0 < a /\ a < pi /\
1145 (&2 - &2 * cos a ) * ( norm (w:real^3) pow 2) < epsilon pow 2` ASSUME_TAC);
1146 (MP_TAC (SPEC `&0` REAL_CONTINUOUS_AT_COS));
1147 (ONCE_REWRITE_TAC[real_continuous_atreal]);
1148 (DISCH_THEN (MP_TAC o (SPEC
1149 `epsilon pow 2 / (&2 * norm(w:real^3) pow 2)`)));
1153 `&0 < epsilon pow 2/ (&2 * norm (w:real^3) pow 2)` ASSUME_TAC);
1154 (MATCH_MP_TAC REAL_LT_DIV);
1157 (* subgoal 10.1.1 *)
1158 (MATCH_MP_TAC REAL_POW_LT);
1159 (ASM_SIMP_TAC[ARITH_RULE `&0 < a <=> a > &0`]);
1161 (* subgoal 10.1.2 *)
1162 (MATCH_MP_TAC (ARITH_RULE ` &0 < a ==> &0 < &2 * a`));
1163 (MATCH_MP_TAC REAL_POW_LT);
1164 (ASM_SIMP_TAC[NORM_POS_LT]);
1166 (ASM_SIMP_TAC[COS_0;REAL_MUL_RID;REAL_SUB_RZERO]);
1167 (DISCH_THEN CHOOSE_TAC);
1168 (FIRST_X_ASSUM MP_TAC);
1170 (Q_ABBREV_TAC `m:real = min (d / &2) (pi / &2)` "phi");
1171 (EXISTS_TAC `m:real`);
1173 (SUBGOAL_THEN `&0 < m:real` ASSUME_TAC);
1174 (Q_EXPAND_TAC "phi");
1175 (SIMP_TAC[REAL_LT_MIN;PI2_BOUNDS]);
1176 (MATCH_MP_TAC REAL_LT_DIV);
1180 (SUBGOAL_THEN `m < pi` ASSUME_TAC);
1181 (Q_EXPAND_TAC "phi");
1182 (ONCE_REWRITE_TAC[REAL_MIN_LT]);
1184 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> a / &2 < a`));
1188 (ONCE_REWRITE_TAC [REAL_ARITH `(&2 - &2 * a) * b = (&1 - a) * (&2 * b)`]);
1189 (MP_TAC (SPECL [`&1 - cos (m:real)`;`epsilon:real pow 2`;
1190 `&2 * norm (w:real^3) pow 2`] REAL_LT_RDIV_EQ));
1193 (SUBGOAL_THEN `&0 < &2 * norm (w:real^3) pow 2` ASSUME_TAC);
1194 (ONCE_REWRITE_TAC[ARITH_RULE `&0 < &2 * a <=> &0 < a`]);
1195 (MATCH_MP_TAC REAL_POW_LT);
1196 (ASM_SIMP_TAC[NORM_POS_LT]);
1199 (MATCH_MP_TAC (TAUT `A ==> (A <=> B ) ==> B`));
1200 (MATCH_MP_TAC (REAL_ARITH `abs a < b ==> a < b`));
1201 (ONCE_REWRITE_TAC[REAL_ARITH `abs (a - b) = abs (b - a)`]);
1202 (FIRST_ASSUM (fun thm -> MATCH_MP_TAC thm));
1205 (SUBGOAL_THEN `abs (m:real) = m` ASSUME_TAC);
1206 (ONCE_REWRITE_TAC[REAL_ABS_REFL]);
1209 (Q_EXPAND_TAC "phi");
1210 (ONCE_REWRITE_TAC[REAL_MIN_LT]);
1214 (FIRST_X_ASSUM CHOOSE_TAC);
1215 (Q_ABBREV_TAC `s:real^3 =
1216 (cos a * norm (w:real^3)) % e1 + (sin a * norm w) % e2` "subs_point");
1217 (Q_ABBREV_TAC `U':real^3 -> bool = s INSERT (U DELETE w)` "new_set");
1220 (SUBGOAL_THEN `!(v:real^3). v IN U /\ ~(v = w) ==> &2 < dist (s,v)`
1221 (LABEL_TAC "dist_gt_2"));
1224 (ASM_CASES_TAC `(v:real^3) IN set_of_edge w U (ECTC U)`);
1227 (SUBGOAL_THEN `dist ((w:real^3),v) = &2` ASSUME_TAC);
1228 (FIRST_X_ASSUM MP_TAC);
1229 (MP_TAC (SPECL [`w:real^3`;`U:real^3->bool`] lemma8));
1231 (MATCH_MP_TAC (TAUT `B ==> (A ==> B)`));
1232 (SIMP_TAC[IN_ELIM_THM]);
1234 (FIRST_X_ASSUM (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
1235 (MP_TAC (SPECL [`w:real^3`;`s:real^3`;`a:real`;
1236 `e1:real^3`;`e2:real^3`;`e3:real^3`] lemma7));
1237 (ASM_SIMP_TAC[NORM_POS_LT]);
1238 (DISCH_THEN (fun thm -> MATCH_MP_TAC (SPEC `v:real^3` thm)));
1240 (Q_EXPAND_TAC "e1");
1241 (ONCE_REWRITE_TAC[GSYM dot_gt_0]);
1242 (ONCE_REWRITE_TAC[ARITH_RULE `&0 < a <=> a > &0`]);
1243 (ONCE_REWRITE_TAC[DOT_SYM]);
1244 (MP_TAC (SPECL [`U:real^3->bool`;`w:real^3`] lemma5));
1248 (ONCE_REWRITE_TAC[DIST_SYM]);
1249 (MATCH_MP_TAC (REAL_ARITH `&2 < dist (v:real^3,w) - dist (s,w) /\
1250 dist (v,w) - dist (s,w) <= a ==> &2 < a`));
1251 (SIMP_TAC[Pack1.real_sub_norm]);
1252 (MATCH_MP_TAC (REAL_ARITH
1253 `a > &2 + (epsilon:real) /\ b < epsilon ==> &2 < a - b`));
1254 (ONCE_REWRITE_TAC[DIST_SYM]);
1256 (ONCE_REWRITE_TAC[DIST_SYM]);
1257 (PURE_REWRITE_TAC[dist]);
1258 (ONCE_REWRITE_TAC[NORM_LT_SQUARE]);
1259 (ASM_SIMP_TAC[ARITH_RULE `&0 < a <=> a > &0`]);
1261 (* subgoal 11.2.1 *)
1262 (SUBGOAL_THEN `s:real^3 - w = ((cos (a:real) - &1) * norm (w:real^3)) % e1 +
1263 (sin a * norm w) % e2 + &0 % e3` ASSUME_TAC);
1264 (* subgoal 11.2.1.1 *)
1265 (SUBGOAL_THEN `w:real^3 = norm w % e1` ASSUME_TAC);
1266 (Q_EXPAND_TAC "e1");
1267 (SIMP_TAC[norm_mul_normalize]);
1269 (FIRST_X_ASSUM(fun thm -> CONV_TAC(PAT_CONV `\x. s - x = A`
1270 (ONCE_REWRITE_CONV[thm]))));
1271 (Q_EXPAND_TAC "subs_point");
1272 (SIMP_TAC[VECTOR_MUL_LZERO;VECTOR_ADD_RID]);
1273 (ONCE_REWRITE_TAC[VECTOR_ARITH
1274 `(a % (e1:real^3) + b % e2) - c % e1 = (a - c) % e1 + b % e2`]);
1275 (SIMP_TAC[ARITH_RULE `a * b - b = (a - &1) * b`]);
1277 [`s:real^3 - w`;`s:real^3 - w`;`e1:real^3`;`e2:real^3`;`e3:real^3`;
1278 `(cos a - &1) * norm (w:real^3)`;`sin a * norm (w:real^3)`;`&0`;
1279 `(cos a - &1) * norm (w:real^3)`;`sin a * norm (w:real^3)`;`&0`]
1280 dot_coordinates_2));
1282 (MATCH_MP_TAC (TAUT `B ==> A ==> B`));
1283 (ONCE_REWRITE_TAC [REAL_ARITH
1284 `(a * b) * a * b + (c * b) * c * b + &0 * &0 = (a * a + c * c) * b pow 2`]);
1285 (ONCE_REWRITE_TAC [REAL_ARITH
1286 `(a - &1) * (a - &1) + b * b = &1 - &2 * a + b pow 2 + a pow 2`]);
1287 (SIMP_TAC[SIN_CIRCLE]);
1288 (ASM_SIMP_TAC[REAL_ARITH `&1 - b + &1 = &2 - b`]);
1291 (SUBGOAL_THEN `!(v:real^3). v IN U' /\ ~(v = s) ==> &2 < dist (s,v)`
1294 (Q_EXPAND_TAC "new_set");
1295 (SIMP_TAC[IN_INSERT; TAUT ` ((A \/ B) /\ ~A) <=> (~A /\ B)`]);
1296 (SIMP_TAC[IN_DELETE]);
1300 (SUBGOAL_THEN `~(s:real^3 IN U)` ASSUME_TAC);
1301 (ONCE_REWRITE_TAC[SET_RULE `~(x IN S) <=> (!y. y IN S ==> ~(x = y))`]);
1304 (ASM_CASES_TAC `y':real^3 = w`);
1308 (* subgoal 13.1.1 *)
1309 (SUBGOAL_THEN `w:real^3 = norm w % e1 + &0 % e2 + &0 % e3` ASSUME_TAC);
1310 (SIMP_TAC[ VECTOR_ARITH `a % e1 + &0 % e2 + &0 % e3 = a % e1`]);
1311 (Q_EXPAND_TAC "e1");
1312 (SIMP_TAC[norm_mul_normalize]);
1314 (FIRST_X_ASSUM (fun thm -> ONCE_REWRITE_TAC[thm]));
1315 (USE_THEN "subs_point" (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
1316 (CONV_TAC(PAT_CONV `\x. ~(x = A)` (ONCE_REWRITE_CONV[
1317 VECTOR_ARITH `a % e1 + b % e2 = a % e1 + b % e2 + &0 % e3`])));
1318 (MP_TAC ( SPECL [`e1:real^3`;`e2:real^3`;`e3:real^3`;
1319 `cos a * norm (w:real^3)`;`sin a * norm (w:real^3)`;`&0`;
1320 `norm (w:real^3)`;`&0`;`&0`] ORTHONORMAL_IMP_INDEPENDENT_EXPLICIT ));
1321 (MATCH_MP_TAC(TAUT `(A /\ ~C) ==> ((A ==> ( B <=> C)) ==> ~B) `));
1323 (MATCH_MP_TAC (TAUT `~B ==> ~ (A /\ B)`));
1324 (SIMP_TAC[REAL_ENTIRE]);
1325 (SIMP_TAC[TAUT `~(A \/ B) <=> ~A /\ ~B`]);
1328 (* subgoal 13.1.2 *)
1329 (ASM_SIMP_TAC[PI_WORKS]);
1330 (* subgoal 13.1.3 *)
1331 (MATCH_MP_TAC(ARITH_RULE `&0 < x ==> ~(x = &0)`));
1332 (ASM_SIMP_TAC[NORM_POS_LT]);
1335 (ONCE_REWRITE_TAC[DIST_NZ]);
1336 (MATCH_MP_TAC (ARITH_RULE `&2 < a ==> &0 < a`));
1337 (USE_THEN "dist_gt_2" (fun thm -> MATCH_MP_TAC thm));
1342 (SUBGOAL_THEN `U':real^3 -> bool IN S` ASSUME_TAC);
1344 (SIMP_TAC[IN_ELIM_THM]);
1347 (SUBGOAL_THEN `norm (s:real^3) = norm (w:real^3)` ASSUME_TAC);
1348 (MP_TAC (SPECL [`w:real^3`;`s:real^3`;`a:real`;
1349 `e1:real^3`;`e2:real^3`;`e3:real^3`] lemma6));
1353 (SUBGOAL_THEN `FINITE (U':real^3->bool)` ASSUME_TAC);
1354 (Q_EXPAND_TAC "new_set");
1355 (ONCE_REWRITE_TAC[FINITE_INSERT]);
1356 (ASM_SIMP_TAC[FINITE_DELETE]);
1359 (SUBGOAL_THEN `packing (U':real^3 -> bool)` ASSUME_TAC);
1360 (PURE_REWRITE_TAC[packing]);
1362 (CONV_TAC(PAT_CONV `\x. x /\ x /\ A ==> B`
1363 (ONCE_REWRITE_CONV[GSYM IN])));
1365 (ASM_CASES_TAC `u':real^3 = s`);
1367 (* subgoal 14.3.1 *)
1369 (MATCH_MP_TAC (ARITH_RULE `&2 < a ==> &2 <= a`));
1370 (FIRST_ASSUM (fun thm -> MATCH_MP_TAC thm));
1372 (FIRST_X_ASSUM(fun thm-> ONCE_REWRITE_TAC[GSYM thm]));
1373 (ASM_SIMP_TAC[EQ_SYM_EQ]);
1375 (ASM_CASES_TAC `v:real^3 = s`);
1377 (* subgoal 14.3.2.1 *)
1379 (ONCE_REWRITE_TAC[DIST_SYM]);
1380 (MATCH_MP_TAC (ARITH_RULE `&2 < a ==> &2 <= a`));
1381 (FIRST_ASSUM (fun thm -> MATCH_MP_TAC thm));
1384 (* subgoal 14.3.2.2 *)
1385 (UNDISCH_TAC `u':real^3 IN U'`);
1386 (Q_EXPAND_TAC "new_set");
1387 (ASM_SIMP_TAC[IN_INSERT;IN_DELETE]);
1389 (UNDISCH_TAC `v:real^3 IN U'`);
1390 (Q_EXPAND_TAC "new_set");
1391 (ASM_SIMP_TAC[IN_INSERT;IN_DELETE]);
1393 (UNDISCH_TAC `packing (U:real^3->bool)`);
1394 (PURE_REWRITE_TAC[packing]);
1395 (DISCH_THEN (fun thm -> MATCH_MP_TAC (SPECL [`u':real^3`;`v:real^3`] thm)));
1396 (CONV_TAC(PAT_CONV `\x. x /\ x /\ A` (ONCE_REWRITE_CONV[GSYM IN])));
1400 (Q_ABBREV_TAC `(h:real^3->real^3) = (\v. if v = w then s else v)` "h");
1401 (EXISTS_TAC `(h:real^3->real^3) o (phi:real^3->real^3)`);
1405 (MATCH_MP_TAC Hypermap.COMPOSE_BIJ);
1406 (EXISTS_TAC `U:real^3->bool`);
1408 (* subgoal 14.4.1 *)
1409 (SUBGOAL_THEN `!v:real^3. v IN U ==> (h:real^3->real^3) v IN U'` ASSUME_TAC);
1412 (SIMP_TAC[BETA_THM]);
1414 (* subgoal 14.4.1.1 *)
1415 (Q_EXPAND_TAC "new_set");
1417 (* subgoal 14.5.1.2 *)
1418 (Q_EXPAND_TAC "new_set");
1419 (SIMP_TAC[IN_INSERT]);
1421 (ASM_SIMP_TAC[IN_DELETE]);
1423 (ASM_SIMP_TAC[BIJ;INJ;SURJ]);
1426 (* subgoal 14.5.2 *)
1428 (UNDISCH_TAC `(h:real^3->real^3) x = h y'`);
1430 (SIMP_TAC[BETA_THM]);
1433 (* subgoal 14.5.2.1 *)
1435 (* subgoal 14.5.2.1.1 *)
1437 (* subgoal 14.5.2.1.2 *)
1440 (* subgoal 14.5.2.2 *)
1443 (* subgoal 14.5.2.2.1 *)
1446 (* subgoal 14.5.2.2.2 *)
1449 (* subgoal 14.5.3 *)
1451 (ASM_CASES_TAC `x:real^3 = s`);
1453 (* subgoal 14.5.3.1 *)
1454 (EXISTS_TAC `w:real^3`);
1457 (SIMP_TAC[BETA_THM]);
1459 (* subgoal 14.5.3.2 *)
1460 (EXISTS_TAC `x:real^3`);
1461 (UNDISCH_TAC `x:real^3 IN U'`);
1462 (Q_EXPAND_TAC "new_set");
1463 (ASM_SIMP_TAC[IN_INSERT;IN_DELETE]);
1466 (ASM_SIMP_TAC[BETA_THM]);
1472 (SUBGOAL_THEN `! x:real^3. x IN U ==> norm x = norm ((h:real^3->real^3) x)` MATCH_MP_TAC);
1475 (SIMP_TAC[BETA_THM]);
1477 (* subgoal 14.6.1 *)
1480 (* subgoal 14.6.2 *)
1483 (UNDISCH_TAC `BIJ (phi:real^3->real^3) V U`);
1485 (DISCH_THEN (fun thm -> MP_TAC (CONJUNCT1 thm)));
1487 (DISCH_THEN (fun thm -> MATCH_MP_TAC (CONJUNCT1 thm)));
1491 (SUBGOAL_THEN `~((f:(real^3->bool)->num) U' <= f U)` ASSUME_TAC);
1492 (ONCE_REWRITE_TAC[ ARITH_RULE `~((a:num) <= b) <=> (b < a)`]);
1494 (MATCH_MP_TAC CARD_PSUBSET);
1498 (ONCE_REWRITE_TAC[PSUBSET_ALT]);
1501 (* subgoal 15.1.1 *)
1502 (ONCE_REWRITE_TAC[SUBSET]);
1504 (ONCE_REWRITE_TAC[set_of_iso]);
1505 (SIMP_TAC[IN_ELIM_THM]);
1508 (* subgoal 15.1.1.1 *)
1509 (SUBGOAL_THEN `x:real^3 IN U'` ASSUME_TAC);
1510 (Q_EXPAND_TAC "new_set");
1511 (SIMP_TAC[IN_INSERT]);
1513 (SIMP_TAC[IN_DELETE]);
1518 (ONCE_REWRITE_TAC[GSYM SUBSET_EMPTY]);
1519 (UNDISCH_TAC `set_of_edge x U (ECTC U) = {}`);
1520 (DISCH_THEN(fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
1521 (MP_TAC (SPECL [`x:real^3`;`U:real^3->bool`] lemma8));
1523 (MATCH_MP_TAC (TAUT `B ==> (A ==> B)`));
1524 (MP_TAC (SPECL [`x:real^3`;`U':real^3->bool`] lemma8));
1526 (MATCH_MP_TAC (TAUT `B ==> (A ==> B)`));
1527 (SIMP_TAC[SUBSET;IN_ELIM_THM]);
1529 (Q_EXPAND_TAC "new_set");
1530 (SIMP_TAC[IN_INSERT;IN_DELETE]);
1531 (MATCH_MP_TAC (TAUT `(D ==> ~A) ==> (A \/ B /\ C) /\ D ==> B`));
1532 (MATCH_MP_TAC (TAUT `(B ==> ~A) ==> (A ==> ~B)`));
1535 (ONCE_REWRITE_TAC[DIST_SYM]);
1536 (MATCH_MP_TAC (ARITH_RULE `&2 < a ==> ~(a = &2)`));
1537 (USE_THEN "dist_gt_2" (fun thm -> MATCH_MP_TAC thm));
1542 (EXISTS_TAC `s:real^3`);
1544 (* subgoal 15.2.1 *)
1545 (SIMP_TAC[set_of_iso;IN_ELIM_THM]);
1546 (* subgoal 15.2.1.1 *)
1547 (SUBGOAL_THEN `s:real^3 IN U'` ASSUME_TAC);
1548 (Q_EXPAND_TAC "new_set");
1552 (MP_TAC (SPECL [`s:real^3`;`U':real^3->bool`] lemma8));
1554 (MATCH_MP_TAC (TAUT ` B ==> A ==> B`));
1555 (ONCE_REWRITE_TAC[SET_RULE `{x| P x} = {} <=> !x. ~(P x)`]);
1557 (MATCH_MP_TAC (TAUT ` (A ==> ~B) ==> ~(A /\ B)`));
1559 (ASM_CASES_TAC `v:real^3 = s`);
1561 (* subgoal 15.2.1.2 *)
1562 (ASM_SIMP_TAC[DIST_REFL]);
1564 (* subgoal 15.2.1.3 *)
1565 (MATCH_MP_TAC (ARITH_RULE `&2 < a ==> ~ (a = &2)`));
1566 (USE_THEN "iso" (fun thm -> MATCH_MP_TAC thm));
1569 (* subgoal 15.2.2 *)
1570 (ASM_SIMP_TAC[set_of_iso;IN_ELIM_THM]);
1571 (MATCH_MP_TAC ( ISPECL [`set_of_iso (U':real^3->bool)`;
1572 `U':real^3->bool`] FINITE_SUBSET));
1573 (ASM_SIMP_TAC[set_of_iso]);