Update from HH
[Flyspeck/.git] / legacy / oldpacking / packing / development / marchal_cells_2.hl
1 (* ========================================================================= *)\r
2 (*                FLYSPECK - BOOK FORMALIZATION                              *)\r
3 (*                                                                           *)\r
4 (*      Authour   : VU KHAC KY                                               *)\r
5 (*      Book lemma:                                                          *)\r
6 (*      Chaper    : Packing (Marchal Cells 2)                                *)\r
7 (*      Date      : October 3, 2010                                          *)\r
8 (*                                                                           *)\r
9 (* ========================================================================= *)\r
10 (*\r
11 #use "/usr/programs/hollight/hollight-svn75/hol.ml";; \r
12 loads "Multivariate/flyspeck.ml";;\r
13 #use "/home/ky/flyspeck/working/boot.hl";; \r
14 flyspeck_needs "trigonometry/trig1.hl";;\r
15 flyspeck_needs "trigonometry/trig2.hl";;\r
16 flyspeck_needs "trigonometry/trigonometry.hl";;\r
17 \r
18 (* =================  Loaded files   ======================================== *)\r
19 \r
20 flyspeck_needs "leg/collect_geom.hl";;\r
21 flyspeck_needs "fan/fan_defs.hl";;\r
22 flyspeck_needs "fan/introduction.hl";; \r
23 flyspeck_needs "fan/topology.hl";;\r
24 flyspeck_needs "fan/fan_misc.hl";; \r
25 flyspeck_needs "fan/HypermapAndFan.hl";; \r
26 flyspeck_needs "packing/pack_defs.hl";;\r
27 flyspeck_needs "packing/pack_concl.hl";; \r
28 flyspeck_needs "packing/pack1.hl";;\r
29 flyspeck_needs "packing/pack2.hl";;\r
30 flyspeck_needs "packing/pack3.hl";;\r
31 flyspeck_needs "packing/Rogers.hl";; \r
32 flyspeck_needs "nonlinear/vukhacky_tactics.hl";;\r
33 *)\r
34 \r
35 (* ====================== Open appropriate files ======================= *)\r
36 \r
37 module Marchal_cells_2 = struct\r
38 \r
39 \r
40 open Rogers;;\r
41 open Prove_by_refinement;;\r
42 open Vukhacky_tactics;;\r
43 open Pack_defs;;\r
44 open Pack_concl;; \r
45 open Pack1;;\r
46 open Sphere;; \r
47 flyspeck_needs "packing/marchal_cells.hl";;\r
48 open Marchal_cells;;\r
49 flyspeck_needs "packing/EMNWUUS.hl";; \r
50 open Emnwuus;;\r
51 \r
52 let seans_fn () =\r
53 let (tms,tm) = top_goal () in\r
54 let vss = map frees (tm::tms) in\r
55 let vs = setify (flat vss) in\r
56 map dest_var vs;;\r
57 \r
58 \r
59 (* ======================================================================= *)\r
60 (* Lemma 1 *)\r
61 let AFF_GE_2_2 = prove\r
62  (`!x v w.\r
63         DISJOINT {x,v} {w,z}\r
64         ==> aff_ge {x,v} {w, z} =\r
65              {y | ?t1 t2 t3 t4.\r
66                      &0 <= t3 /\ &0 <= t4 /\\r
67                      t1 + t2 + t3 + t4 = &1 /\\r
68                      y = t1 % x + t2 % v + t3 % w + t4 % z}`,\r
69   AFF_TAC);;\r
70 (* ======================================================================= *)\r
71 (* Lemma 2 *)\r
72 let MEASURABLE_ROGERS = prove_by_refinement (\r
73  `!V (ul:(real^3)list) k.\r
74      saturated V /\ packing V /\ barV V 3 ul ==> measurable (rogers V ul)`,\r
75 [ (REPEAT STRIP_TAC);\r
76  (REWRITE_TAC[ROGERS]);\r
77  (MATCH_MP_TAC MEASURABLE_CONVEX_HULL);\r
78  (MATCH_MP_TAC FINITE_IMP_BOUNDED);\r
79  (MATCH_MP_TAC FINITE_IMAGE);\r
80  (SUBGOAL_THEN `? u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]` CHOOSE_TAC);\r
81  (MP_TAC (ASSUME `barV V 3 ul`));\r
82  (REWRITE_TAC[BARV_3_EXPLICIT]);\r
83  (FIRST_X_ASSUM CHOOSE_TAC);\r
84  (FIRST_X_ASSUM CHOOSE_TAC);\r
85  (FIRST_X_ASSUM CHOOSE_TAC);\r
86  (NEW_GOAL `LENGTH (ul:(real^3)list) = 4`);\r
87  (ASM_REWRITE_TAC[LENGTH]);\r
88  (ARITH_TAC);\r
89  (ASM_REWRITE_TAC[]);\r
90  (REWRITE_TAC[FINITE_NUMSEG_LT])]);;\r
91 \r
92 (* ======================================================================= *)\r
93 (* Lemma 3 *)\r
94 let CONVEX_RCONE_GE = prove_by_refinement (\r
95  `!a:real^N b r. &0 <= r ==> convex (rcone_ge a b r)`,\r
96 [ (REPEAT STRIP_TAC);\r
97  (REWRITE_TAC[rcone_ge;convex;rconesgn;IN;IN_ELIM_THM]);\r
98  (REPEAT STRIP_TAC);\r
99  (REWRITE_WITH `(u % x + v % y) - a = u % (x - a) + v % (y - a:real^N)`);\r
100  (ASM_REWRITE_TAC[VECTOR_SUB_LDISTRIB; VECTOR_MUL_LID; \r
101   VECTOR_ARITH `a - x % b + c - y % b = (a + c) - (x + y) % b`]);\r
102  (REWRITE_TAC[DOT_LADD;DOT_LMUL]);\r
103  (ASM_CASES_TAC `&0 < u`);\r
104 \r
105   (* 2 Subgoals *)\r
106 \r
107  (NEW_GOAL \r
108   `u * ((x:real^N - a) dot (b - a)) + v * ((y - a) dot (b - a)) >= \r
109    u * dist (x,a) * dist (b,a) * r + v *  dist (y,a) * dist (b,a) * r`);\r
110    (* Subgoal 1.1 *)\r
111 \r
112  (NEW_GOAL\r
113   `u * ((x:real^N - a) dot (b - a)) >= u * dist (x,a) * dist (b,a) * r`);\r
114  (MATCH_MP_TAC (REAL_ARITH `&0 <= a - b ==> a >= b`));\r
115  (REWRITE_TAC[REAL_ARITH `a * b * c * d = a * (b * c * d)`; \r
116                REAL_ARITH `a * b - a * c = a * (b - c)`]);\r
117  (MATCH_MP_TAC REAL_LE_MUL);\r
118  (ASM_REAL_ARITH_TAC);\r
119 \r
120  (NEW_GOAL\r
121   `v * ((y:real^N - a) dot (b - a)) >= v * dist (y,a) * dist (b,a) * r`);\r
122  (MATCH_MP_TAC (REAL_ARITH `&0 <= a - b ==> a >= b`));\r
123  (REWRITE_TAC[REAL_ARITH `a * b * c * d = a * (b * c * d)`; \r
124                REAL_ARITH `a * b - a * c = a * (b - c)`]);\r
125  (MATCH_MP_TAC REAL_LE_MUL);\r
126  (ASM_REAL_ARITH_TAC);\r
127  (ASM_REAL_ARITH_TAC);\r
128 \r
129  (NEW_GOAL \r
130 `dist (u % x + v % y,a) * dist (b,a:real^N) * r <= \r
131  u * dist (x,a) * dist (b,a) * r + v *  dist (y,a) * dist (b,a) * r`);\r
132    (* Subgoal 1.2 *)\r
133 \r
134  (MATCH_MP_TAC (REAL_ARITH `&0 <= a - b ==> b <= a`));\r
135  (REWRITE_TAC[REAL_ARITH `(a * b * x + c * d * x) - e * x  = \r
136                             (a * b + c * d - e) * x`]);\r
137  (MATCH_MP_TAC REAL_LE_MUL);\r
138  STRIP_TAC;\r
139  (REWRITE_TAC[dist]);\r
140  (REWRITE_WITH `(u % x + v % y) - a = u % (x - a) + v % (y - a:real^N)`);\r
141  (ASM_REWRITE_TAC[VECTOR_SUB_LDISTRIB; VECTOR_MUL_LID; \r
142    VECTOR_ARITH `a - x % b + c - y % b = (a + c) - (x + y) % b`]);\r
143  (REWRITE_TAC[REAL_ARITH `&0 <= a + b - c <=> c <= a + b`]);\r
144  (MATCH_MP_TAC (REAL_ARITH \r
145   `m <= norm (u % (x - a:real^N)) + norm (v % (y - a)) /\\r
146    norm (u % (x - a)) = b /\   \r
147    norm (v % (y - a)) = c ==> m <= b + c`));\r
148  (REWRITE_TAC[NORM_TRIANGLE;NORM_MUL]);\r
149  (REWRITE_WITH `abs u = u /\ abs v = v`);\r
150  (ASM_SIMP_TAC[REAL_ABS_REFL]);\r
151 \r
152  (MATCH_MP_TAC REAL_LE_MUL);\r
153  (ASM_REWRITE_TAC[DIST_POS_LE]);\r
154  (ASM_REAL_ARITH_TAC);\r
155 \r
156 (* Subgoal 2 *)\r
157 \r
158  (NEW_GOAL `u = &0`);\r
159  (ASM_REAL_ARITH_TAC);\r
160  (NEW_GOAL `v = &1`);\r
161  (ASM_REAL_ARITH_TAC);\r
162  (ASM_REWRITE_TAC[REAL_MUL_LZERO;REAL_ADD_LID;REAL_MUL_LID]);\r
163  (ASM_REWRITE_TAC[VECTOR_MUL_LZERO;VECTOR_ADD_LID;VECTOR_MUL_LID])]);; \r
164 \r
165 (* ======================================================================= *)\r
166 (* Lemma 4 *)\r
167 let FINITE_PERMUTE_3 = prove_by_refinement \r
168   (`FINITE {p | p permutes {0, 1, 2}}`, \r
169   [MATCH_MP_TAC FINITE_PERMUTATIONS THEN MESON_TAC[FINITE_RULES]]);;\r
170 let FINITE_PERMUTE_4 = prove_by_refinement \r
171   (`FINITE {p | p permutes {0, 1, 2, 3}}`, \r
172   [MATCH_MP_TAC FINITE_PERMUTATIONS THEN MESON_TAC[FINITE_RULES]]);;\r
173 \r
174 (* ======================================================================= *)\r
175 (* Lemma 5 *)\r
176 let TRUONG_SET_TAC = let basicthms =\r
177 [NOT_IN_EMPTY; IN_UNIV; IN_UNION; IN_INTER; IN_DIFF; IN_INSERT;\r
178 IN_DELETE; IN_REST; IN_INTERS; IN_UNIONS; IN_IMAGE] in\r
179 let allthms = basicthms @ map (REWRITE_RULE[IN]) basicthms @\r
180 [IN_ELIM_THM; IN] in\r
181 let PRESET_TAC =\r
182 TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ)) THEN\r
183 REPEAT COND_CASES_TAC THEN\r
184 REWRITE_TAC[EXTENSION; SUBSET; PSUBSET; DISJOINT; SING] THEN\r
185 REWRITE_TAC allthms in\r
186 fun ths ->\r
187 PRESET_TAC THEN\r
188 (if ths = [] then ALL_TAC else MP_TAC(end_itlist CONJ ths)) THEN\r
189 MESON_TAC ths ;;\r
190 \r
191 (* ======================================================================= *)\r
192 (* Lemma 6 *)\r
193 let DISJOINT_KY_LEMMA = prove_by_refinement (\r
194  `~(x = y) /\ ~(x = z) ==> DISJOINT {x} {y, z:real^3}`,\r
195 [(REPEAT STRIP_TAC);\r
196  (REWRITE_TAC[DISJOINT; INTER ; IN; IN_ELIM_THM;Geomdetail.IN_ACT_SING]);\r
197  (MATCH_MP_TAC (MESON [] `(~a ==> F) ==> a`));\r
198  (DISCH_TAC);\r
199  (SUBGOAL_THEN `?t. t IN {x' | x' = x /\ {y, z:real^3} x'}` ASSUME_TAC);\r
200  (UP_ASM_TAC THEN SET_TAC[]);\r
201  (FIRST_X_ASSUM CHOOSE_TAC);\r
202  (UP_ASM_TAC THEN REWRITE_TAC[IN; IN_ELIM_THM]);\r
203  (NEW_GOAL `{y, z:real^3} t <=> (t = y) \/ (t = z)`);\r
204  (TRUONG_SET_TAC[]);\r
205  (ASM_REWRITE_TAC[]);\r
206  (ASM_MESON_TAC[])]);;\r
207 \r
208 (* ======================================================================= *)\r
209 (* Lemma 7 *)\r
210 \r
211 \r
212 let DIHV_SYM = prove_by_refinement (\r
213  `!(x:real^N) y z t. dihV x y z t = dihV y x z t`,\r
214 [ (REPEAT GEN_TAC);\r
215  (REWRITE_TAC[dihV] THEN REPEAT LET_TAC);\r
216  (MATCH_MP_TAC (MESON[]\r
217   `!a b c d x. (a = b) /\ (c = d) ==> arcV x a c = arcV x b d`));\r
218  (REPEAT STRIP_TAC);\r
219   (* Break into 2 subgoals with similar proofs *)\r
220    \r
221   (* Subgoal 1 *)\r
222    (EXPAND_TAC "vap'" THEN EXPAND_TAC "vap");\r
223 \r
224      (REWRITE_WITH `(va':real^N) = va - vc`);\r
225      (EXPAND_TAC "va'" THEN EXPAND_TAC "va" THEN EXPAND_TAC "vc");\r
226      (VECTOR_ARITH_TAC);\r
227 \r
228      (REWRITE_WITH `(vc':real^N) = --vc`);\r
229      (EXPAND_TAC "vc'" THEN EXPAND_TAC "vc");\r
230      (VECTOR_ARITH_TAC);\r
231 \r
232      (REWRITE_WITH \r
233    `(--vc dot --vc) % (va:real^N - vc) = (vc dot vc) % va - (vc dot vc) % vc`);\r
234     (REWRITE_TAC[DOT_RNEG;DOT_LNEG;REAL_ARITH `-- --x = x `]);\r
235     (VECTOR_ARITH_TAC);\r
236 \r
237   (MATCH_MP_TAC (VECTOR_ARITH `a = b + c ==> x:real^N - b - c = x - a `));\r
238   (REWRITE_WITH `((va:real^N - vc) dot --vc) % --vc = \r
239                  (va dot vc) % vc - (vc dot vc) % vc`);\r
240  (REWRITE_TAC[DOT_RNEG;DOT_LNEG;VECTOR_MUL_LNEG; VECTOR_MUL_RNEG]);\r
241  (REWRITE_TAC[VECTOR_NEG_MINUS1;VECTOR_MUL_ASSOC]);\r
242  (REWRITE_TAC[REAL_ARITH `-- &1 * -- &1 * x = x`;\r
243                DOT_LSUB;VECTOR_SUB_RDISTRIB]);\r
244  (VECTOR_ARITH_TAC);\r
245 \r
246    (* Subgoal 2 *)\r
247  (EXPAND_TAC "vbp'" THEN EXPAND_TAC "vbp");\r
248  (REWRITE_WITH `(vb':real^N) = vb - vc`);\r
249  (EXPAND_TAC "vb'" THEN EXPAND_TAC "vb" THEN EXPAND_TAC "vc");\r
250  (VECTOR_ARITH_TAC);\r
251 \r
252    (REWRITE_WITH `(vc':real^N) = --vc`);\r
253    (EXPAND_TAC "vc'" THEN EXPAND_TAC "vc");\r
254    (VECTOR_ARITH_TAC);\r
255 \r
256    (REWRITE_WITH \r
257   `(--vc dot --vc) % (vb:real^N - vc) = (vc dot vc) % vb - (vc dot vc) % vc`);\r
258    (REWRITE_TAC[DOT_RNEG;DOT_LNEG;REAL_ARITH `-- --x = x `]);\r
259    (VECTOR_ARITH_TAC);\r
260  \r
261    (MATCH_MP_TAC (VECTOR_ARITH `a = b + c ==> x:real^N - b - c = x - a `));\r
262    (REWRITE_WITH `((vb:real^N - vc) dot --vc) % --vc = \r
263                  (vb dot vc) % vc - (vc dot vc) % vc`);\r
264    (REWRITE_TAC[DOT_RNEG;DOT_LNEG;VECTOR_MUL_LNEG; VECTOR_MUL_RNEG]);\r
265    (REWRITE_TAC[VECTOR_NEG_MINUS1;VECTOR_MUL_ASSOC]);\r
266    (REWRITE_TAC[REAL_ARITH `-- &1 * -- &1 * x = x`;\r
267                DOT_LSUB;VECTOR_SUB_RDISTRIB]);\r
268    (VECTOR_ARITH_TAC)]);;\r
269 \r
270 \r
271 (* ======================================================================= *)\r
272 (* Lemma 8 *)\r
273 let RCONE_GT_SUBSET_RCONE_GE = prove_by_refinement (\r
274  `! z:real^3 w h. rcone_gt z w h SUBSET rcone_ge z w h`,\r
275 [ (REPEAT GEN_TAC THEN REWRITE_TAC[RCONE_GT_GE]);\r
276  (SET_TAC[])]);;\r
277 \r
278 (* ======================================================================= *)\r
279 (* Lemma 9 *)\r
280 let MCELL_EXPLICIT = prove_by_refinement (\r
281  `!k ul V.\r
282      mcell 0 V ul = mcell0 V ul /\\r
283      mcell 1 V ul = mcell1 V ul /\\r
284      mcell 2 V ul = mcell2 V ul /\\r
285      mcell 3 V ul = mcell3 V ul /\\r
286      (k >= 4 ==> mcell k V ul = mcell4 V ul)`,\r
287 [ (NEW_GOAL `((1 = 0) ==> F) /\ ((2 = 0) ==> F) /\ ((3 = 0) ==> F) /\\r
288 ((2 = 1) ==> F) /\ ((3 = 1) ==> F) /\ ((3 = 2) ==> F)`);\r
289  (ARITH_TAC);\r
290  (REPEAT STRIP_TAC); (REWRITE_TAC[mcell]);\r
291  (REWRITE_TAC[mcell]); (COND_CASES_TAC);\r
292  (ASM_MESON_TAC[]); (MESON_TAC[]);\r
293  (REWRITE_TAC[mcell]); (COND_CASES_TAC);\r
294  (ASM_MESON_TAC[]); (COND_CASES_TAC);\r
295  (ASM_MESON_TAC[]); (MESON_TAC[]);\r
296  (REWRITE_TAC[mcell]); (COND_CASES_TAC);\r
297  (ASM_MESON_TAC[]); (COND_CASES_TAC);\r
298  (ASM_MESON_TAC[]); (COND_CASES_TAC);\r
299  (ASM_MESON_TAC[]); (MESON_TAC[]);\r
300  (REWRITE_TAC[mcell]); (COND_CASES_TAC);\r
301  (ASM_MESON_TAC[ARITH_RULE `~(0 >= 4)`]);\r
302  (COND_CASES_TAC); (ASM_MESON_TAC[ARITH_RULE `~(1 >= 4)`]);\r
303  (COND_CASES_TAC); (ASM_MESON_TAC[ARITH_RULE `~(2 >= 4)`]);\r
304  (COND_CASES_TAC); (ASM_MESON_TAC[ARITH_RULE `~(3 >= 4)`]);\r
305  (MESON_TAC[])]);;\r
306 \r
307 (* ======================================================================= *)\r
308 (* Lemma 10 *)\r
309 let EVENTUALLY_RADIAL_EMPTY = prove_by_refinement (\r
310  `!v:real^3. eventually_radial v {} `,\r
311 [(STRIP_TAC);\r
312  (REWRITE_TAC[eventually_radial;radial]);\r
313  (EXISTS_TAC `&1`);\r
314  (REWRITE_TAC[REAL_ARITH `&1 > &0`;INTER_SUBSET]);\r
315  (REPEAT STRIP_TAC);\r
316  (NEW_GOAL `F`);\r
317  (DEL_TAC THEN DEL_TAC THEN UP_ASM_TAC);\r
318  (REWRITE_TAC[INTER_EMPTY]);\r
319  (SET_TAC[]);\r
320  (UP_ASM_TAC THEN MESON_TAC[])]);;\r
321 \r
322 (* ======================================================================= *)\r
323 (* Lemma 11 *)\r
324 let EVENTUALLY_RADIAL_NOT_IN_CLOSED_SET = prove_by_refinement (\r
325  `!v:real^3 S. ~(S v) /\ (closed S)==> eventually_radial v S`,\r
326 [(REPEAT STRIP_TAC);\r
327  (NEW_GOAL `?r. r > &0 /\ ball(v:real^3, r) INTER S = {}`);\r
328  (UP_ASM_TAC THEN REWRITE_TAC[closed; open_def]);\r
329  (DISCH_TAC);\r
330  (MP_TAC (SPEC `v:real^3` (ASSUME `!x. x IN (:real^3) DIFF S\r
331           ==> (?e. &0 < e /\\r
332                    (!x'. dist (x',x) < e ==> x' IN (:real^3) DIFF S))`)));\r
333  (DISCH_TAC);\r
334  (NEW_GOAL `(?e. &0 < e /\ (!x'. dist (x',v:real^3) < e ==> x' IN (:real^3) DIFF S))`);\r
335  (FIRST_X_ASSUM MATCH_MP_TAC);\r
336  (REWRITE_TAC[IN_DIFF]);\r
337  (ASM_REWRITE_TAC[IN]);\r
338  (MESON_TAC[IN_UNIV;IN]);\r
339  (FIRST_X_ASSUM CHOOSE_TAC);\r
340  (EXISTS_TAC `e:real`);\r
341  (STRIP_TAC);\r
342  (ASM_REAL_ARITH_TAC);\r
343  (REWRITE_TAC[ball]);\r
344  (MATCH_MP_TAC (SET_RULE `(!a:real^3. (a IN A) ==> ~(a IN B)) ==> (A INTER B = {})`));\r
345  (REWRITE_TAC[IN; IN_ELIM_THM]);\r
346  (GEN_TAC THEN DISCH_TAC);\r
347  (NEW_GOAL `a IN (:real^3) DIFF S ==> ~S a `);\r
348  (REWRITE_TAC[IN_DIFF;IN; IN_ELIM_THM]);\r
349  (MESON_TAC[]);\r
350  (FIRST_X_ASSUM MATCH_MP_TAC);\r
351  (UP_ASM_TAC THEN ASM_REWRITE_TAC[DIST_SYM]);\r
352  (REWRITE_TAC[eventually_radial;radial]);\r
353  (FIRST_X_ASSUM CHOOSE_TAC);\r
354  (EXISTS_TAC `r:real`);\r
355  (ASM_REWRITE_TAC[INTER_SUBSET]);\r
356  (REPEAT STRIP_TAC);\r
357  (NEW_GOAL `F`);\r
358  (DEL_TAC THEN DEL_TAC);\r
359  (UP_ASM_TAC THEN REWRITE_WITH `S INTER ball (v,r) = ball (v:real^3,r) INTER S`);\r
360  (SET_TAC[]);\r
361  (ASM_REWRITE_TAC[]);\r
362  (SET_TAC[]);\r
363  (UP_ASM_TAC THEN MESON_TAC[])]);;\r
364 \r
365 (* ======================================================================= *)\r
366 (* Lemma 12 *)\r
367 let CLOSED_CONVEX_HULL_FINITE = prove\r
368   (`!s. FINITE s ==> closed(convex hull s)`,\r
369   MESON_TAC[COMPACT_IMP_CLOSED; COMPACT_CONVEX_HULL;  FINITE_IMP_COMPACT]);;\r
370 \r
371 (* ======================================================================= *)\r
372 (* Lemma 13 *)\r
373 let CLOSED_ROGERS = prove_by_refinement (\r
374  `! V ul:(real^3)list. \r
375    saturated V /\ packing V /\ barV V 3 ul ==> closed (rogers V ul)`,\r
376 [(REPEAT STRIP_TAC THEN REWRITE_TAC[ROGERS]);\r
377  (MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);\r
378  (MATCH_MP_TAC FINITE_IMAGE);\r
379  (REWRITE_WITH `{j | j < LENGTH (ul:(real^3)list)} ={j| j < 4}`);\r
380  (MATCH_MP_TAC (MESON[] `(a = b) ==> ({j:num| j < a} = {j | j < b})`));\r
381  (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);\r
382  (MP_TAC (ASSUME `barV V 3 ul`));\r
383  (REWRITE_TAC[BARV_3_EXPLICIT]);\r
384  (FIRST_X_ASSUM CHOOSE_TAC);\r
385  (FIRST_X_ASSUM CHOOSE_TAC);\r
386  (FIRST_X_ASSUM CHOOSE_TAC);\r
387  (FIRST_X_ASSUM CHOOSE_TAC);\r
388  (ASM_REWRITE_TAC[LENGTH]);\r
389  (ARITH_TAC);\r
390  (REWRITE_TAC[FINITE_NUMSEG_LT])]);;\r
391 \r
392 (* ======================================================================= *)\r
393 (* Lemma 14 *)\r
394 let CLOSED_SET_OF_LIST_KY_LEMMA_1 = prove_by_refinement (\r
395  `!V ul.\r
396      saturated V /\ packing V /\ barV V 3 (ul:(real^3)list)\r
397      ==> closed\r
398          (convex hull (set_of_list (truncate_simplex 2 ul) UNION {mxi V ul}))`,\r
399 [(REPEAT STRIP_TAC THEN MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);\r
400  (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);\r
401  (MP_TAC (ASSUME `barV V 3 ul`));\r
402  (REWRITE_TAC[BARV_3_EXPLICIT]);\r
403  (FIRST_X_ASSUM CHOOSE_TAC);\r
404  (FIRST_X_ASSUM CHOOSE_TAC);\r
405  (FIRST_X_ASSUM CHOOSE_TAC);\r
406  (FIRST_X_ASSUM CHOOSE_TAC);\r
407  (REWRITE_WITH `truncate_simplex 2 ul = [u0;u1;u2:real^3]`);     \r
408  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
409  (REWRITE_TAC[set_of_list]);\r
410  (REWRITE_TAC[ SET_RULE `!a b c d. {a,b,c} UNION {d:real^3} = {a,b,c,d}`]);\r
411  (REWRITE_TAC[Geomdetail.FINITE6])]);;\r
412 (* ======================================================================= *)\r
413 (* Lemma 15 *)\r
414 let CLOSED_SET_OF_LIST_KY_LEMMA_2 = prove_by_refinement (\r
415  `!V (ul:(real^3)list). \r
416      saturated V /\ packing V /\ barV V 3 ul ==> \r
417      closed (convex hull set_of_list ul)`,\r
418 [(REPEAT STRIP_TAC THEN MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);\r
419  (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);\r
420  (MP_TAC (ASSUME `barV V 3 ul`));\r
421  (REWRITE_TAC[BARV_3_EXPLICIT]);\r
422  (FIRST_X_ASSUM CHOOSE_TAC);\r
423  (FIRST_X_ASSUM CHOOSE_TAC);\r
424  (FIRST_X_ASSUM CHOOSE_TAC);\r
425  (FIRST_X_ASSUM CHOOSE_TAC);\r
426  (ASM_REWRITE_TAC[set_of_list]);\r
427  (REWRITE_TAC[Geomdetail.FINITE6])]);;\r
428 \r
429 (* ======================================================================= *)\r
430 (* Lemma 16 *)\r
431 let CLOSED_RCONE_GE = prove_by_refinement (\r
432  `!v0 v1:real^3 a. &0 < a ==> closed (rcone_ge v0 v1 a)`,\r
433 [(REPEAT STRIP_TAC THEN REWRITE_TAC[rcone_ge;rconesgn]);\r
434  (REWRITE_TAC[closed]);\r
435  (REWRITE_WITH `(:real^3) DIFF\r
436   {x | (x - v0) dot (v1 - v0) >= dist (x,v0) * dist (v1,v0) * a} = \r
437   {x | (x - v0) dot (v1 - v0) < dist (x,v0) * dist (v1,v0) * a}`);\r
438  (REWRITE_TAC[Vol1.SET_EQ]);\r
439  (REWRITE_TAC[IN_DIFF;IN;IN_ELIM_THM;IN_UNIV]);\r
440  (REPEAT STRIP_TAC);\r
441  (UP_ASM_TAC THEN REAL_ARITH_TAC);\r
442  (ASM_REAL_ARITH_TAC);\r
443  (REWRITE_TAC[open_def;IN;IN_ELIM_THM]);\r
444  (REPEAT STRIP_TAC);\r
445  (NEW_GOAL `~(v0 = v1:real^3)`);\r
446  STRIP_TAC;\r
447  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
448  (REWRITE_TAC[VECTOR_SUB_REFL; DOT_RZERO; DIST_REFL; REAL_MUL_LZERO;REAL_MUL_RZERO]);\r
449  (REAL_ARITH_TAC);\r
450 \r
451  (ABBREV_TAC `s = dist (x,v0:real^3) * dist (v1,v0) * a`);\r
452  (ABBREV_TAC `t = (x - v0) dot (v1 - v0:real^3)`);\r
453  (EXISTS_TAC `(s - t) / (dist (v1,v0) * a + dist (v1, v0:real^3))`);\r
454  (STRIP_TAC);\r
455  (MATCH_MP_TAC REAL_LT_DIV);\r
456  (STRIP_TAC);\r
457  (ASM_REAL_ARITH_TAC);\r
458  (MATCH_MP_TAC REAL_LT_ADD);\r
459  (ASM_SIMP_TAC [DIST_POS_LT]);\r
460  (MATCH_MP_TAC REAL_LT_MUL);\r
461  (ASM_SIMP_TAC [DIST_POS_LT]);\r
462 \r
463  (REPEAT STRIP_TAC);\r
464  (NEW_GOAL `(x' - v0) dot (v1 - v0) <= \r
465              (x - v0:real^3) dot (v1 - v0) + dist (x',x) * dist (v1,v0) `);\r
466  (MATCH_MP_TAC (REAL_ARITH `&0 <= a - b ==> b <= a`));\r
467  (REWRITE_TAC[REAL_ARITH `(x + y) - z = (x - z) + y`]);\r
468  (REWRITE_TAC[VECTOR_ARITH `x dot y - z dot y = (x - z) dot y`]);\r
469  (REWRITE_TAC[VECTOR_ARITH `(x:real^3) - y - (z - y) = (x - z)`;dist]);\r
470  (REWRITE_WITH ` (x - x':real^3) dot (v1 - v0:real^3) = --  ((x' - x) dot (v1 - v0))`);\r
471  (VECTOR_ARITH_TAC);\r
472 \r
473  (MATCH_MP_TAC (REAL_ARITH `b <= a ==> &0 <= --b + a`));\r
474  (REWRITE_TAC[NORM_CAUCHY_SCHWARZ]);\r
475  (NEW_GOAL `dist (x',v0) * dist (v1,v0:real^3) * a >= \r
476       dist (x,v0) * dist (v1,v0) * a - dist (x',x) * dist (v1,v0) * a `);\r
477  (MATCH_MP_TAC (REAL_ARITH `&0 <= a - b ==> a >= b`));\r
478  (REWRITE_TAC[REAL_ARITH `x * a * b - (y * a * b - z * a * b) = (x - y + z) * (a * b) `]);\r
479  (MATCH_MP_TAC REAL_LE_MUL);\r
480  (STRIP_TAC);\r
481  (MATCH_MP_TAC (REAL_ARITH `b <= a + c ==> &0 <= a - b + c`));\r
482  (REWRITE_TAC[DIST_SYM]);\r
483  (REWRITE_WITH `dist (x, x':real^3) = dist (x', x)`);\r
484  (REWRITE_TAC[DIST_SYM]);\r
485  (REWRITE_TAC[DIST_TRIANGLE]);\r
486  (MATCH_MP_TAC REAL_LE_MUL);\r
487 \r
488  (ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> &0 <= a`; DIST_POS_LE ]);\r
489  (MATCH_MP_TAC (REAL_ARITH `(?n q. m <= n /\ p >= q /\  n < q) ==> m < p`));\r
490  (EXISTS_TAC `(x - v0) dot (v1 - v0) + dist (x',x) * dist (v1,v0:real^3)`);\r
491  (EXISTS_TAC `dist (x,v0:real^3) * dist (v1,v0) * a - dist (x',x) * dist (v1,v0) * a`);\r
492  (ASM_REWRITE_TAC[]);\r
493  (REWRITE_TAC[REAL_ARITH `t + c * b < s - c * b * a <=> c * (b * a + b) < s - t\r
494 `]);\r
495  (NEW_GOAL `dist (x',x) * (dist (v1,v0:real^3) * a + dist (v1,v0)) < s - t <=> \r
496              dist (x':real^3,x) < (s - t) / (dist (v1,v0) * a + dist (v1,v0))`);\r
497  (ONCE_REWRITE_TAC[MESON[] `!a b. (a <=> b) <=> (b <=> a)`]);\r
498  (MATCH_MP_TAC REAL_LT_RDIV_EQ);\r
499  (MATCH_MP_TAC REAL_LT_ADD);\r
500  (ASM_SIMP_TAC[REAL_LT_MUL; REAL_ARITH `&0 < a ==> &0 <= a`; DIST_POS_LT]);\r
501  (ASM_REWRITE_TAC[])]);;\r
502 \r
503 (* ======================================================================= *)\r
504 (* Lemma 17 *)\r
505 let BARV_IMP_HL_1_POS_LT = prove_by_refinement (\r
506  `!V ul:(real^3)list.\r
507      saturated V /\ packing V /\ barV V 3 ul \r
508      ==> &0 < hl (truncate_simplex 1 ul)`,\r
509 [(REPEAT STRIP_TAC);\r
510  (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);\r
511  (MP_TAC (ASSUME `barV V 3 ul`));\r
512  (REWRITE_TAC[BARV_3_EXPLICIT]);\r
513  (REPEAT (FIRST_X_ASSUM CHOOSE_TAC));\r
514  (ABBREV_TAC `vl = truncate_simplex 1 (ul:(real^3)list)`);\r
515  (NEW_GOAL `hl (vl:(real^3)list) = dist (circumcenter (set_of_list vl),HD vl)`);\r
516  (MATCH_MP_TAC HL_EQ_DIST0);\r
517  (EXISTS_TAC `V:real^3->bool`);\r
518  (EXISTS_TAC `1`);\r
519  (ASM_REWRITE_TAC[]);\r
520  (EXPAND_TAC "vl");\r
521  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
522  (EXISTS_TAC `3`);\r
523  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);\r
524 \r
525  (NEW_GOAL `&0 <= hl (vl:(real^3)list)`);\r
526  (ASM_REWRITE_TAC[DIST_POS_LE]);\r
527  (ASM_CASES_TAC `&0 < hl (vl:(real^3)list)`);\r
528  (ASM_REWRITE_TAC[]);\r
529  (NEW_GOAL `hl (vl:(real^3)list) = &0`);\r
530  (ASM_REAL_ARITH_TAC);\r
531  (NEW_GOAL `F`);\r
532  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
533  (REWRITE_TAC[DIST_EQ_0]);\r
534  (REWRITE_WITH `vl = [u0;u1:real^3]`);\r
535  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
536  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
537  (REWRITE_TAC[set_of_list;HD;CIRCUMCENTER_2;midpoint]);\r
538  STRIP_TAC;\r
539  (NEW_GOAL `(u0:real^3) = u1`);\r
540  (UP_ASM_TAC THEN VECTOR_ARITH_TAC);\r
541  (NEW_GOAL `barV V 1 (vl:(real^3)list)`);\r
542  (EXPAND_TAC "vl");\r
543  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
544  (EXISTS_TAC `3`);\r
545  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);\r
546  (NEW_GOAL `CARD (set_of_list (vl:(real^3)list)) = 1 + 1`);\r
547  (ASM_MESON_TAC[BARV_IMP_LENGTH_EQ_CARD]);\r
548  (UP_ASM_TAC THEN REWRITE_WITH `vl = [u0;u1:real^3]`);\r
549  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
550  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
551  (ASM_REWRITE_TAC[set_of_list]);\r
552  (REWRITE_TAC[ SET_RULE `{u1, u1:real^3} = {u1}`]);\r
553  (REWRITE_TAC[Hypermap.CARD_SINGLETON]);\r
554  (ARITH_TAC);\r
555  (UP_ASM_TAC THEN MESON_TAC[])]);;\r
556 \r
557 (* ======================================================================= *)\r
558 (* Lemma 18 *)\r
559 let CLOSED_MCELL = prove_by_refinement (\r
560  `!V ul k v:real^3.\r
561      saturated V /\ packing V /\ barV V 3 ul\r
562      ==> closed (mcell k V ul)`,\r
563 [(REPEAT STRIP_TAC);\r
564  (ASM_CASES_TAC `k = 0`);\r
565  (ASM_REWRITE_TAC[MCELL_EXPLICIT;mcell0]);\r
566  (MATCH_MP_TAC CLOSED_DIFF);\r
567  (ASM_MESON_TAC[CLOSED_ROGERS; OPEN_BALL]);\r
568 \r
569  (ASM_CASES_TAC `k = 1`);\r
570  (ASM_REWRITE_TAC[MCELL_EXPLICIT;mcell1]);\r
571  (COND_CASES_TAC);\r
572  (MATCH_MP_TAC CLOSED_DIFF);\r
573  (STRIP_TAC);\r
574  (MATCH_MP_TAC CLOSED_INTER);\r
575  (ASM_MESON_TAC[CLOSED_ROGERS; CLOSED_CBALL]);\r
576  (REWRITE_TAC[OPEN_RCONE_GT]);\r
577  (REWRITE_TAC[CLOSED_EMPTY]);\r
578 \r
579  (SUBGOAL_THEN `? u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]` CHOOSE_TAC);\r
580  (MP_TAC (ASSUME `barV V 3 ul`));\r
581  (REWRITE_TAC[BARV_3_EXPLICIT]);\r
582  (FIRST_X_ASSUM CHOOSE_TAC);\r
583  (FIRST_X_ASSUM CHOOSE_TAC);\r
584  (FIRST_X_ASSUM CHOOSE_TAC);\r
585  (ASM_CASES_TAC `k = 2`);\r
586 \r
587  (ASM_REWRITE_TAC[MCELL_EXPLICIT;mcell2]);\r
588  (COND_CASES_TAC);\r
589  LET_TAC;\r
590  (MATCH_MP_TAC CLOSED_INTER);\r
591  (STRIP_TAC);\r
592 \r
593  (MATCH_MP_TAC CLOSED_RCONE_GE);\r
594  (EXPAND_TAC "a");\r
595  (MATCH_MP_TAC REAL_LT_DIV);\r
596  (SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]);\r
597  (ASM_MESON_TAC[BARV_IMP_HL_1_POS_LT]);\r
598 \r
599  (MATCH_MP_TAC CLOSED_INTER);\r
600  (STRIP_TAC);\r
601  (MATCH_MP_TAC CLOSED_RCONE_GE);\r
602  (EXPAND_TAC "a");\r
603  (MATCH_MP_TAC REAL_LT_DIV);\r
604  (SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]);\r
605  (ASM_MESON_TAC[BARV_IMP_HL_1_POS_LT]);\r
606 \r
607  (MATCH_MP_TAC CLOSED_AFF_GE);\r
608  (MESON_TAC[Geomdetail.FINITE6]);\r
609  (MESON_TAC[CLOSED_EMPTY]);\r
610 \r
611  (ASM_CASES_TAC `k = 3`);\r
612  (ASM_REWRITE_TAC[MCELL_EXPLICIT;mcell3]);\r
613  (COND_CASES_TAC);\r
614  (ASM_MESON_TAC[CLOSED_SET_OF_LIST_KY_LEMMA_1]);\r
615  (MESON_TAC[CLOSED_EMPTY]);\r
616 \r
617  (NEW_GOAL `k >= 4`);\r
618  (ASM_ARITH_TAC);\r
619  (ASM_SIMP_TAC[MCELL_EXPLICIT;mcell4]);\r
620  (COND_CASES_TAC);\r
621  (ASM_MESON_TAC[CLOSED_SET_OF_LIST_KY_LEMMA_2]);\r
622  (MESON_TAC[CLOSED_EMPTY])\r
623 ]);;\r
624 \r
625 (* ======================================================================= *)\r
626 (* Lemma 19 *)\r
627 let BARV_IMP_u0_IN_V = prove_by_refinement (\r
628  `!V ul u0 u1 u2 u3.\r
629      saturated V /\ packing V /\ barV V 3 ul /\ ul = [u0;u1;u2;u3:real^3]\r
630      ==> u0 IN V`,\r
631 [(REWRITE_TAC[BARV; VORONOI_NONDG]);\r
632  (REPEAT STRIP_TAC);\r
633  (NEW_GOAL `initial_sublist [u0:real^3] ul /\ 0 < LENGTH [u0]`);\r
634  (REWRITE_TAC[INITIAL_SUBLIST;LENGTH; APPEND; ARITH_RULE `0 < SUC 0`]);\r
635  (EXISTS_TAC `[u1;u2;u3:real^3]`);\r
636  (ASM_REWRITE_TAC[]);\r
637  (NEW_GOAL `set_of_list [u0:real^3] SUBSET V`);\r
638  (ASM_SIMP_TAC[]);\r
639  (UP_ASM_TAC THEN REWRITE_TAC[set_of_list]);\r
640  (SET_TAC[])]);;\r
641 \r
642 (* ======================================================================= *)\r
643 (* Lemma 20 *)\r
644 let ROGERS_INTER_V_LEMMA = prove_by_refinement (\r
645  `!V ul v:real^3.\r
646      saturated V /\ packing V /\ barV V 3 ul /\ v IN V /\ (rogers V ul v)\r
647      ==> v = HD ul`,\r
648 [(REPEAT STRIP_TAC);\r
649  (SUBGOAL_THEN `? u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]` CHOOSE_TAC);\r
650  (MP_TAC (ASSUME `barV V 3 ul`));\r
651  (REWRITE_TAC[BARV_3_EXPLICIT]);\r
652  (FIRST_X_ASSUM CHOOSE_TAC);\r
653  (FIRST_X_ASSUM CHOOSE_TAC);\r
654  (FIRST_X_ASSUM CHOOSE_TAC);\r
655  (ASM_REWRITE_TAC[HD]);\r
656 \r
657  (NEW_GOAL `(rogers V ul)  SUBSET (voronoi_closed V (u0:real^3))`);\r
658  (REWRITE_TAC[SUBSET]);\r
659  (REPEAT STRIP_TAC);\r
660  (NEW_GOAL `!p. p IN voronoi_closed V u0 <=>\r
661                (?vl. vl IN barV V 3 /\\r
662                      p IN rogers V vl /\\r
663                      truncate_simplex 0 vl = [u0:real^3])`);\r
664  (GEN_TAC THEN MATCH_MP_TAC GLTVHUM);\r
665  (ASM_REWRITE_TAC[]);\r
666  (ASM_MESON_TAC[BARV_IMP_u0_IN_V]);\r
667  (ASM_REWRITE_TAC[]);\r
668  (EXISTS_TAC `ul:(real^3)list`);\r
669  (ASM_REWRITE_TAC[IN; TRUNCATE_SIMPLEX_EXPLICIT_0]);\r
670  (NEW_GOAL `(v:real^3) IN (voronoi_closed V u0)`);\r
671  (ASM_SET_TAC[]);\r
672  (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed;IN;IN_ELIM_THM]);\r
673  (DISCH_TAC);\r
674  (NEW_GOAL `dist (v,u0) <= dist (v,v:real^3)`);\r
675  (FIRST_ASSUM MATCH_MP_TAC);\r
676  (ASM_REWRITE_TAC[GSYM IN]);\r
677  (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]);\r
678  (DISCH_TAC);\r
679  (NEW_GOAL `dist (v, u0:real^3) = &0`);\r
680  (NEW_GOAL `&0 <= dist (v, u0:real^3)`);\r
681  (REWRITE_TAC[DIST_POS_LE]);\r
682  (ASM_REAL_ARITH_TAC);\r
683  (UP_ASM_TAC THEN MESON_TAC[DIST_EQ_0])]);;\r
684 \r
685 (* ======================================================================= *)\r
686 (* Lemma 21 *)\r
687 let CONVEX_HULL_4 = prove\r
688  (`convex hull {a,b,c,d} =\r
689     { u % a + v % b + w % c + z %d|\r
690       &0 <= u /\ &0 <= v /\ &0 <= w /\ &0 <= z /\ u + v + w + z = &1}`,\r
691   SIMP_TAC[CONVEX_HULL_FINITE; FINITE_INSERT; FINITE_RULES] THEN\r
692   SIMP_TAC[CONVEX_HULL_FINITE_STEP; FINITE_INSERT; FINITE_RULES] THEN\r
693   REWRITE_TAC[REAL_ARITH `x - y = z:real <=> x = y + z`;\r
694               VECTOR_ARITH `x - y = z:real^N <=> x = y + z`] THEN\r
695   REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN SET_TAC[]);;\r
696 \r
697 (* ======================================================================= *)\r
698 (* Lemma 22 *)\r
699 let REAL_LE_DIV_SIMPLIFY_KY_LEMMA = prove_by_refinement (\r
700  `!a b c. &0 < a /\ b <= c / a ==>  a * b <=  c`,\r
701 [(REPEAT STRIP_TAC);\r
702  (NEW_GOAL `a * b <= a * (c / a)`);\r
703  (REWRITE_TAC[REAL_ARITH `x * y <= x * z <=> &0 <= x * (z - y)`]);\r
704  (MATCH_MP_TAC REAL_LE_MUL);\r
705  (ASM_REAL_ARITH_TAC);\r
706  (NEW_GOAL `a * c / a = c`);\r
707  (REWRITE_TAC[REAL_ARITH `a * c / a = c / a * a`]);\r
708  (MATCH_MP_TAC REAL_DIV_RMUL);\r
709  (ASM_REAL_ARITH_TAC);\r
710  (ASM_MESON_TAC[])]);;\r
711 \r
712 (* ======================================================================= *)\r
713 (* Lemma 23 *)\r
714 \r
715 let EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1 = prove_by_refinement (\r
716  `!a b c d:real^3. \r
717    ~( a IN convex hull {b , c, d})\r
718    ==> eventually_radial a (convex hull {a, b , c, d})`,\r
719 [(REPEAT STRIP_TAC);\r
720  (REWRITE_TAC[eventually_radial]);\r
721  (ABBREV_TAC `s = convex hull {b , c, d:real^3}`);\r
722 \r
723  (NEW_GOAL `(?(x:real^3). x IN s /\ \r
724                          (!y:real^3. y IN s ==> dist (a,x) <= dist (a,y)))`);\r
725  (MATCH_MP_TAC DISTANCE_ATTAINS_INF);\r
726  (EXPAND_TAC "s");\r
727  (STRIP_TAC);\r
728  (MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);\r
729  (REWRITE_TAC[Geomdetail.FINITE6]);\r
730  (REWRITE_TAC[CONVEX_HULL_EQ_EMPTY]);\r
731  (SET_TAC[]);\r
732  (FIRST_X_ASSUM CHOOSE_TAC);\r
733  (EXISTS_TAC `dist (a, x:real^3)`);\r
734 \r
735  (NEW_GOAL `dist (a, x) <= dist (a, b:real^3) /\ \r
736              dist (a, x) <= dist (a, c:real^3) /\ \r
737              dist (a, x) <= dist (a, d:real^3)`);\r
738  (UP_ASM_TAC THEN REPEAT STRIP_TAC);\r
739 \r
740  (FIRST_ASSUM MATCH_MP_TAC);\r
741  (EXPAND_TAC "s");\r
742  (MATCH_MP_TAC (SET_RULE `b IN {b} /\ {b} SUBSET s ==> b IN s `));\r
743  (STRIP_TAC);\r
744  (SET_TAC[]);\r
745  (NEW_GOAL `{b:real^3} = convex hull {b}`);\r
746  (ONCE_REWRITE_TAC[MESON[] `a = b <=> b = a` ]);\r
747  (REWRITE_TAC[CONVEX_HULL_EQ]);\r
748  (REWRITE_TAC[CONVEX_SING]);\r
749  (ONCE_ASM_REWRITE_TAC[]);\r
750  (EXPAND_TAC "s");\r
751  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);\r
752  (SET_TAC[]);\r
753 \r
754  (FIRST_ASSUM MATCH_MP_TAC);\r
755  (EXPAND_TAC "s");\r
756  (MATCH_MP_TAC (SET_RULE `c IN {c} /\ {c} SUBSET s ==> c IN s `));\r
757  (STRIP_TAC);\r
758  (SET_TAC[]);\r
759  (NEW_GOAL `{c:real^3} = convex hull {c}`);\r
760  (ONCE_REWRITE_TAC[MESON[] `a = b <=> b = a` ]);\r
761  (REWRITE_TAC[CONVEX_HULL_EQ]);\r
762  (REWRITE_TAC[CONVEX_SING]);\r
763  (ONCE_ASM_REWRITE_TAC[]);\r
764  (EXPAND_TAC "s");\r
765  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);\r
766  (SET_TAC[]);\r
767 \r
768 \r
769  (FIRST_ASSUM MATCH_MP_TAC);\r
770  (EXPAND_TAC "s");\r
771  (MATCH_MP_TAC (SET_RULE `c IN {c} /\ {c} SUBSET s ==> c IN s `));\r
772  (STRIP_TAC);\r
773  (SET_TAC[]);\r
774  (NEW_GOAL `{d:real^3} = convex hull {d}`);\r
775  (ONCE_REWRITE_TAC[MESON[] `a = b <=> b = a` ]);\r
776  (REWRITE_TAC[CONVEX_HULL_EQ]);\r
777  (REWRITE_TAC[CONVEX_SING]);\r
778  (ONCE_ASM_REWRITE_TAC[]);\r
779  (EXPAND_TAC "s");\r
780  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);\r
781  (SET_TAC[]);\r
782 \r
783 (* ======== break main lemma into 2 smaller ones =============== *)\r
784 (* subgoal 1 *)\r
785 \r
786  (STRIP_TAC);\r
787  (ASM_CASES_TAC `dist (a:real^3, x) = &0`);\r
788  (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]);\r
789  (DISCH_TAC);\r
790  (NEW_GOAL `F`);\r
791  (ASM_MESON_TAC[]);\r
792  (UP_ASM_TAC THEN MESON_TAC[]);\r
793  (NEW_GOAL `&0 <= dist (a, x:real^3)`);\r
794  (REWRITE_TAC[DIST_POS_LE]);\r
795  (ASM_REAL_ARITH_TAC);\r
796 \r
797 (* subgoal 2 *)\r
798 \r
799  (REWRITE_TAC[radial; INTER_SUBSET]);\r
800  (REPEAT STRIP_TAC);\r
801  (REWRITE_TAC[IN_INTER]);\r
802  (STRIP_TAC);\r
803  (ASM_CASES_TAC `u:real^3 = vec 0`);\r
804  (ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_RID]);\r
805  (REWRITE_TAC[CONVEX_HULL_4;IN;IN_ELIM_THM]);\r
806  (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);\r
807  (REWRITE_TAC[REAL_ARITH `&0 <= &1 /\ &0 <= &0 /\ &1 + &0 + &0 + &0 = &1`]);\r
808  (VECTOR_ARITH_TAC);\r
809  (NEW_GOAL `?y. y IN convex hull {b, c, d:real^3} /\ \r
810                  (a + t % u) IN convex hull {a, y}`);\r
811  (UNDISCH_TAC `a + u IN convex hull {a, b, c, d:real^3} INTER ball (a,dist (a,x))`);\r
812  (REWRITE_TAC[CONVEX_HULL_4;IN_INTER;IN;IN_ELIM_THM]);\r
813  (REPEAT STRIP_TAC);\r
814  (EXISTS_TAC `(&1 / (&1 - u')) % (v % b + w % c + z % (d:real^3))`);\r
815  (STRIP_TAC);\r
816  (REWRITE_TAC[CONVEX_HULL_3;IN_ELIM_THM]);\r
817  (EXISTS_TAC ` v / (&1 - u')`);\r
818  (EXISTS_TAC ` w / (&1 - u')`);\r
819  (EXISTS_TAC ` z / (&1 - u')`);\r
820  (REPEAT STRIP_TAC);\r
821 \r
822  (MATCH_MP_TAC REAL_LE_DIV);\r
823  (ASM_REAL_ARITH_TAC);\r
824  (MATCH_MP_TAC REAL_LE_DIV);\r
825  (ASM_REAL_ARITH_TAC);\r
826  (MATCH_MP_TAC REAL_LE_DIV);\r
827  (ASM_REAL_ARITH_TAC);\r
828  (REWRITE_TAC[REAL_ARITH `a / x + b / x + c / x = (a + b + c) / x`]);\r
829  (MATCH_MP_TAC (MESON [REAL_DIV_REFL] `~(y = &0) /\ (x = y) ==> x / y = &1`));\r
830  (ASM_REWRITE_TAC[REAL_ARITH `!a b c d e. \r
831       (&1 - a = &0 <=> a = &1) /\ ( b + c + d = &1 - e <=> e + b + c + d = &1)`]);\r
832  (STRIP_TAC);\r
833  (NEW_GOAL `v = &0 /\ w = &0 /\ z = &0`);\r
834  (ASM_REAL_ARITH_TAC);\r
835  (UNDISCH_TAC `(a:real^3) + u = u' % a + v % b + w % c + z % d`);\r
836  (ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO]);\r
837  (REWRITE_TAC[VECTOR_ARITH `a + (u:real^3) = a + vec 0 + vec 0 + vec 0 <=> u = vec 0`]);\r
838  (ASM_MESON_TAC[]);\r
839 \r
840  (REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]);\r
841  (REWRITE_TAC[REAL_ARITH `!x y. &1 / x * y = y / x`]);\r
842 \r
843  (REWRITE_WITH `v % (b:real^3) + w % c + z % d = a + u - u' % a`);\r
844  (SWITCH_TAC THEN UP_ASM_TAC THEN VECTOR_ARITH_TAC);\r
845  (REWRITE_TAC[VECTOR_ARITH `!a t u. a + u - t % a = (&1 - t) % a + u`]);\r
846  (REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]);\r
847  (REWRITE_WITH `&1 / (&1 - u') * (&1 - u') = &1`);\r
848  (REWRITE_TAC[REAL_ARITH `!x y. &1 / x * y = y / x`]);\r
849  (MATCH_MP_TAC REAL_DIV_REFL);\r
850  (REWRITE_TAC[REAL_ARITH `!a. &1 - a = &0 <=> a = &1`]);\r
851  (STRIP_TAC);\r
852  (NEW_GOAL `v = &0 /\ w = &0 /\ z = &0`);\r
853  (ASM_REAL_ARITH_TAC);\r
854  (UNDISCH_TAC `(a:real^3) + u = u' % a + v % b + w % c + z % d`);\r
855  (ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO]);\r
856  (REWRITE_TAC[VECTOR_ARITH `a + (u:real^3) = a + vec 0 + vec 0 + vec 0 <=> u = vec 0`]);\r
857  (ASM_MESON_TAC[]);\r
858  (REWRITE_TAC[VECTOR_MUL_LID; CONVEX_HULL_2;IN_ELIM_THM]);\r
859  (EXISTS_TAC `&1 - t * (&1 - u') `);\r
860  (EXISTS_TAC `t * (&1 - u')`);\r
861  (REPEAT STRIP_TAC);\r
862 \r
863  (REWRITE_TAC[REAL_ARITH `&0 <= &1 - a <=> a <= &1`]);\r
864  (NEW_GOAL `dist (a:real^3, a + u) / (&1 - u') = dist (a, a + (&1 / (&1 - u')) % u)`);\r
865  (REWRITE_TAC[dist; VECTOR_ARITH `a - (a + s:real^3) = -- s`; NORM_NEG; NORM_MUL; REAL_ABS_DIV; REAL_ABS_1]);\r
866  (ONCE_REWRITE_TAC[REAL_ARITH `&1 / x * y = y / x`]);\r
867  (AP_TERM_TAC);\r
868  (ONCE_REWRITE_TAC[MESON[] `x = y <=> y = x`]);\r
869  (REWRITE_TAC[REAL_ABS_REFL]);\r
870  (REWRITE_TAC[REAL_ARITH `!a. &0 <= &1 - a <=> a <= &1`]);\r
871  (ASM_REAL_ARITH_TAC);\r
872  (NEW_GOAL `(&1 - u') * dist (a, x:real^3) <= norm (u:real^3) `);\r
873  (REWRITE_WITH `norm (u:real^3) = dist (a, a +u)`);\r
874  (REWRITE_TAC[dist]);\r
875  (NORM_ARITH_TAC);\r
876  (MATCH_MP_TAC REAL_LE_DIV_SIMPLIFY_KY_LEMMA);\r
877  (ASM_REWRITE_TAC[]);\r
878 \r
879  (STRIP_TAC);\r
880  (ASM_CASES_TAC `(&0 < &1 - u')`);\r
881  (ASM_REWRITE_TAC[]);\r
882  (NEW_GOAL `u' = &1`);\r
883  (NEW_GOAL `u' <= &1`);\r
884  (ASM_REAL_ARITH_TAC);\r
885  (NEW_GOAL `&1 <= u'`);\r
886  (ASM_REAL_ARITH_TAC);\r
887  (ASM_REAL_ARITH_TAC);\r
888  (NEW_GOAL `v = &0 /\ w = &0 /\ z = &0`);\r
889  (ASM_REAL_ARITH_TAC);\r
890  (UNDISCH_TAC `(a:real^3) + u = u' % a + v % b + w % c + z % d`);\r
891  (ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO]);\r
892  (REWRITE_TAC[VECTOR_ARITH `a + (u:real^3) = a + vec 0 + vec 0 + vec 0 <=> u = vec 0`]);\r
893  (ASM_MESON_TAC[]);\r
894 \r
895  (UNDISCH_TAC `x IN s /\ (!y. y IN s ==> dist (a:real^3,x) <= dist (a,y))`);\r
896  (REPEAT STRIP_TAC);\r
897  (FIRST_ASSUM MATCH_MP_TAC);\r
898  (EXPAND_TAC "s" THEN REWRITE_TAC[CONVEX_HULL_3; IN; IN_ELIM_THM]);\r
899 \r
900  (EXISTS_TAC ` v / (&1 - u')`);\r
901  (EXISTS_TAC ` w / (&1 - u')`);\r
902  (EXISTS_TAC ` z / (&1 - u')`);\r
903  (REPEAT STRIP_TAC);\r
904 \r
905  (MATCH_MP_TAC REAL_LE_DIV);\r
906  (ASM_REAL_ARITH_TAC);\r
907  (MATCH_MP_TAC REAL_LE_DIV);\r
908  (ASM_REAL_ARITH_TAC);\r
909  (MATCH_MP_TAC REAL_LE_DIV);\r
910  (ASM_REAL_ARITH_TAC);\r
911  (REWRITE_TAC[REAL_ARITH `a / x + b / x + c / x = (a + b + c) / x`]);\r
912  (MATCH_MP_TAC (MESON [REAL_DIV_REFL] `~(y = &0) /\ (x = y) ==> x / y = &1`));\r
913  (ASM_REWRITE_TAC[REAL_ARITH `!a b c d e. \r
914       (&1 - a = &0 <=> a = &1) /\ ( b + c + d = &1 - e <=> e + b + c + d = &1)`]);\r
915  (STRIP_TAC);\r
916  (NEW_GOAL `v = &0 /\ w = &0 /\ z = &0`);\r
917  (ASM_REAL_ARITH_TAC);\r
918  (UNDISCH_TAC `(a:real^3) + u = u' % a + v % b + w % c + z % d`);\r
919  (ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO]);\r
920  (REWRITE_TAC[VECTOR_ARITH `a + (u:real^3) = a + vec 0 + vec 0 + vec 0 <=> u = vec 0`]);\r
921  (ASM_MESON_TAC[]);\r
922 \r
923  (REWRITE_WITH `v / (&1 - u') % b + w / (&1 - u') % c + z / (&1 - u') % d =\r
924                  &1 / (&1 - u') % (a + u:real^3) - u'/ (&1 - u') % a `);\r
925  (ASM_REWRITE_TAC[]);\r
926  (REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]);\r
927  (REWRITE_TAC[REAL_ARITH `&1 / x  * y = y / x`]);\r
928  (VECTOR_ARITH_TAC);\r
929  (REWRITE_TAC[VECTOR_ADD_LDISTRIB]);\r
930 \r
931 \r
932  (REWRITE_TAC[VECTOR_ARITH `a + b = (t % a + b) - s % a <=> a = (t - s) % a`]);\r
933  (REWRITE_WITH `&1 / (&1 - u') - u' / (&1 - u') = &1`);\r
934  (REWRITE_TAC[REAL_ARITH `a / b - c / b = (a - c) / b`]);\r
935  (MATCH_MP_TAC REAL_DIV_REFL);\r
936  (REWRITE_TAC[REAL_ARITH `!a. &1 - a = &0 <=> a = &1`]);\r
937  (STRIP_TAC);\r
938  (NEW_GOAL `v = &0 /\ w = &0 /\ z = &0`);\r
939  (ASM_REAL_ARITH_TAC);\r
940  (UNDISCH_TAC `(a:real^3) + u = u' % a + v % b + w % c + z % d`);\r
941  (ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO]);\r
942  (REWRITE_TAC[VECTOR_ARITH `a + (u:real^3) = a + vec 0 + vec 0 + vec 0 <=> u = vec 0`]);\r
943  (ASM_MESON_TAC[]);\r
944  (REWRITE_TAC[VECTOR_MUL_LID]);\r
945 \r
946 \r
947 \r
948  (NEW_GOAL `t * ((&1 - u') * dist (a,x:real^3)) <= t * norm (u:real^3)`);\r
949  (REWRITE_TAC[REAL_ARITH `t * s <= t * k <=> &0 <= t * (k - s)`]);\r
950  (MATCH_MP_TAC REAL_LE_MUL);\r
951  (ASM_REAL_ARITH_TAC);\r
952  (NEW_GOAL `t * ((&1 - u') * dist (a,x:real^3)) <= dist (a, x)`);\r
953  (ASM_REAL_ARITH_TAC);\r
954  (NEW_GOAL ` t * (&1 - u') <= &1 <=>\r
955              (t * (&1 - u')) * dist (a,x:real^3) <= &1 * dist (a,x)`);\r
956  (ONCE_REWRITE_TAC[MESON[] `(a <=> b) <=> (b <=> a)`]);\r
957  (MATCH_MP_TAC REAL_LE_RMUL_EQ);\r
958  (ASM_CASES_TAC `dist (a:real^3, x) = &0`);\r
959  (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]);\r
960  (DISCH_TAC);\r
961  (NEW_GOAL `F`);\r
962  (ASM_MESON_TAC[]);\r
963  (UP_ASM_TAC THEN MESON_TAC[]);\r
964  (NEW_GOAL `&0 <= dist (a, x:real^3)`);\r
965  (REWRITE_TAC[DIST_POS_LE]);\r
966  (ASM_REAL_ARITH_TAC);\r
967 \r
968  \r
969  (ASM_REWRITE_TAC[]);\r
970  (ASM_REAL_ARITH_TAC);\r
971  (MATCH_MP_TAC REAL_LE_MUL);\r
972  (ASM_REAL_ARITH_TAC);\r
973  (ASM_REAL_ARITH_TAC);\r
974 \r
975 \r
976  (REWRITE_TAC[VECTOR_SUB_RDISTRIB; VECTOR_ADD_LDISTRIB; VECTOR_MUL_LID; VECTOR_MUL_ASSOC]);\r
977 \r
978  (REWRITE_TAC [VECTOR_ARITH `a + m % u = a - t + t + n % u <=> (m - n) % u = vec 0`; VECTOR_MUL_EQ_0]);\r
979  (DISJ1_TAC);\r
980  (REWRITE_TAC[REAL_ARITH `(a * b) * &1 / b = a * (b / b)`]);\r
981 \r
982 \r
983 (* ======================================================================== *)\r
984 \r
985  (REWRITE_TAC[REAL_ARITH `t - t * s = t * (&1 - s)`]);\r
986  (MATCH_MP_TAC (MESON[REAL_MUL_RZERO] ` x = &0 ==> t * x = &0`));\r
987  (REWRITE_TAC[REAL_ARITH `&1 - t = &0 <=> t = &1`]);\r
988  (MATCH_MP_TAC REAL_DIV_REFL);\r
989 \r
990  (REWRITE_TAC[REAL_ARITH `!a. &1 - a = &0 <=> a = &1`]);\r
991  (STRIP_TAC);\r
992  (NEW_GOAL `v = &0 /\ w = &0 /\ z = &0`);\r
993  (ASM_REAL_ARITH_TAC);\r
994  (UNDISCH_TAC `(a:real^3) + u = u' % a + v % b + w % c + z % d`);\r
995  (ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO]);\r
996  (REWRITE_TAC[VECTOR_ARITH `a + (u:real^3) = a + vec 0 + vec 0 + vec 0 <=> u = vec 0`]);\r
997  (ASM_MESON_TAC[]);\r
998 \r
999  (FIRST_X_ASSUM CHOOSE_TAC);\r
1000  (UP_ASM_TAC THEN REPEAT  STRIP_TAC);\r
1001  (UP_ASM_TAC THEN MATCH_MP_TAC (SET_RULE `A SUBSET B ==> (a IN A ==> a IN B)`));\r
1002  (NEW_GOAL `convex hull {a, b , c, d:real^3} = convex hull (convex hull {a, b, c, d})`);\r
1003  (ONCE_REWRITE_TAC[MESON [] `!a b. a = b <=> b = a`]);\r
1004  (REWRITE_TAC[CONVEX_HULL_EQ; CONVEX_CONVEX_HULL]);\r
1005  (ONCE_ASM_REWRITE_TAC[]);\r
1006  (MATCH_MP_TAC CONVEX_HULL_SUBSET);\r
1007  (MATCH_MP_TAC (SET_RULE `!m a S. m IN S /\ a IN S ==> {a, m} SUBSET S`));\r
1008  (STRIP_TAC);\r
1009  (MATCH_MP_TAC (SET_RULE `m IN convex hull {b, c, d:real^3} /\ \r
1010                            convex hull {b, c, d} SUBSET n ==> m IN n`));\r
1011  (ASM_REWRITE_TAC[]);\r
1012  (EXPAND_TAC "s" THEN MATCH_MP_TAC CONVEX_HULL_SUBSET);\r
1013  (SET_TAC[]);\r
1014  (REWRITE_TAC[CONVEX_HULL_4;IN;IN_ELIM_THM]);\r
1015  (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);\r
1016  (REWRITE_TAC[REAL_ARITH `&0 <= &1 /\ &0 <= &0 /\ &1 + &0 + &0 + &0 = &1`]);\r
1017  (VECTOR_ARITH_TAC);\r
1018 \r
1019  (REWRITE_TAC[ball;IN;IN_ELIM_THM]);\r
1020  (REWRITE_WITH `dist (a:real^3,a + t % u) = t * norm u`);\r
1021  (REWRITE_TAC[dist; VECTOR_ARITH `a - (a + b:real^3) = -- b`; NORM_NEG; \r
1022 NORM_MUL]);\r
1023  (AP_THM_TAC THEN AP_TERM_TAC);\r
1024  (REWRITE_TAC[REAL_ABS_REFL]);\r
1025  (ASM_REAL_ARITH_TAC);\r
1026  (ASM_REWRITE_TAC[])]);;\r
1027 \r
1028 (* ======================================================================= *)\r
1029 (* Lemma 24 *)\r
1030 let U0_NOT_IN_CONVEX_HULL_FROM_ROGERS = prove_by_refinement (\r
1031  `!V (ul:(real^3)list).\r
1032      saturated V /\ packing V /\ barV V 3 ul\r
1033      ==> ~(HD ul IN\r
1034            convex hull\r
1035            {omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3})`,\r
1036 [(REWRITE_TAC[ARITH_RULE `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`; OMEGA_LIST_N]);\r
1037  (REWRITE_TAC[ARITH_RULE `SUC 0 = 1 /\ SUC 1 = 2 /\ SUC 2 = 3`]);\r
1038  (REPEAT STRIP_TAC);\r
1039  (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);\r
1040  (MP_TAC (ASSUME `barV V 3 ul`));\r
1041  (REWRITE_TAC[BARV_3_EXPLICIT]);\r
1042  (FIRST_X_ASSUM CHOOSE_TAC);\r
1043  (FIRST_X_ASSUM CHOOSE_TAC);\r
1044  (FIRST_X_ASSUM CHOOSE_TAC);\r
1045  (FIRST_X_ASSUM CHOOSE_TAC);\r
1046  \r
1047  (ABBREV_TAC `a = closest_point (voronoi_list V \r
1048                   (truncate_simplex 1 (ul:(real^3)list)))`);\r
1049  (ABBREV_TAC `b = closest_point (voronoi_list V \r
1050                   (truncate_simplex 2 (ul:(real^3)list)))`);\r
1051  (ABBREV_TAC `c = closest_point (voronoi_list V \r
1052                   (truncate_simplex 3 (ul:(real^3)list)))`);\r
1053 (* First estimation *)\r
1054 \r
1055  (NEW_GOAL `(a (HD ul)) IN voronoi_list V (truncate_simplex 1 (ul:(real^3)list))`);\r
1056  (EXPAND_TAC "a");\r
1057  (MATCH_MP_TAC CLOSEST_POINT_IN_SET);\r
1058  (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);\r
1059  (MATCH_MP_TAC Packing3.BARV_IMP_VORONOI_LIST_NOT_EMPTY);\r
1060  (EXISTS_TAC `1`);\r
1061  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1062  (EXISTS_TAC `3`);\r
1063  (ASM_REWRITE_TAC[]);\r
1064  (ARITH_TAC);\r
1065 \r
1066 (* Second estimation *)\r
1067 \r
1068  (NEW_GOAL `((b:real^3->real^3) (a (HD ul))) IN voronoi_list V (truncate_simplex 2 (ul:(real^3)list))`);\r
1069  (EXPAND_TAC "b");\r
1070 \r
1071  (MATCH_MP_TAC CLOSEST_POINT_IN_SET);\r
1072  (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);\r
1073  (MATCH_MP_TAC Packing3.BARV_IMP_VORONOI_LIST_NOT_EMPTY);\r
1074  (EXISTS_TAC `2`);\r
1075  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1076  (EXISTS_TAC `3`);\r
1077  (ASM_REWRITE_TAC[]);\r
1078  (ARITH_TAC);\r
1079 \r
1080 (* Third estimation *)\r
1081 \r
1082  (NEW_GOAL `((c:(real^3->real^3))((b:real^3->real^3) (a (HD ul)))) IN voronoi_list V (truncate_simplex 3 (ul:(real^3)list))`);\r
1083  (EXPAND_TAC "c");\r
1084  (MATCH_MP_TAC CLOSEST_POINT_IN_SET);\r
1085  (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);\r
1086  (MATCH_MP_TAC Packing3.BARV_IMP_VORONOI_LIST_NOT_EMPTY);\r
1087  (EXISTS_TAC `3`);\r
1088  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1089  (EXISTS_TAC `3`);\r
1090  (ASM_REWRITE_TAC[]);\r
1091  (ARITH_TAC);\r
1092 \r
1093  (ABBREV_TAC `x:real^3 = (a (HD (ul:(real^3)list)))`);\r
1094  (ABBREV_TAC `y:real^3 = b (x:real^3)`);\r
1095  (ABBREV_TAC `z:real^3 = c (y:real^3)`);\r
1096 \r
1097 \r
1098  (NEW_GOAL `(y:real^3) IN voronoi_list V (truncate_simplex 1 ul)`);\r
1099  (MATCH_MP_TAC (SET_RULE `(?A. a IN A /\ A SUBSET B) ==> a IN B`));\r
1100  (EXISTS_TAC `voronoi_list V (truncate_simplex 2 (ul:(real^3)list))`);\r
1101  (ASM_REWRITE_TAC[VORONOI_LIST;VORONOI_SET]);\r
1102  (MATCH_MP_TAC (SET_RULE `b SUBSET s ==> (INTERS s) SUBSET (INTERS b)`));\r
1103  (REWRITE_TAC[SIMPLE_IMAGE]);\r
1104  (MATCH_MP_TAC IMAGE_SUBSET);\r
1105  (ASM_REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1106  (SET_TAC[]);\r
1107 \r
1108  (NEW_GOAL `(z:real^3) IN voronoi_list V (truncate_simplex 1 ul)`);\r
1109  (MATCH_MP_TAC (SET_RULE `(?A. a IN A /\ A SUBSET B) ==> a IN B`));\r
1110  (EXISTS_TAC `voronoi_list V (truncate_simplex 3 (ul:(real^3)list))`);\r
1111  (ASM_REWRITE_TAC[VORONOI_LIST;VORONOI_SET]);\r
1112  (MATCH_MP_TAC (SET_RULE `b SUBSET s ==> (INTERS s) SUBSET (INTERS b)`));\r
1113  (REWRITE_TAC[SIMPLE_IMAGE]);\r
1114  (MATCH_MP_TAC IMAGE_SUBSET);\r
1115  (ASM_REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; TRUNCATE_SIMPLEX_EXPLICIT_3]);\r
1116  (SET_TAC[]);\r
1117 \r
1118  (NEW_GOAL `convex hull {x, y, z:real^3} SUBSET (convex hull voronoi_list V (truncate_simplex 1 ul))`);\r
1119  (MATCH_MP_TAC CONVEX_HULL_SUBSET);\r
1120  (ASM_SET_TAC[]);\r
1121 \r
1122  (NEW_GOAL `convex hull voronoi_list V (truncate_simplex 1 (ul:(real^3)list)) \r
1123              =  voronoi_list V (truncate_simplex 1 ul)`);\r
1124  (REWRITE_TAC [CONVEX_HULL_EQ; Packing3.CONVEX_VORONOI_LIST]);\r
1125  (NEW_GOAL `u0:real^3 IN voronoi_list V (truncate_simplex 1 ul)`);\r
1126  (REWRITE_WITH `u0:real^3 = HD ul`);\r
1127  (ASM_MESON_TAC[HD]);\r
1128  (ASM_SET_TAC[]);\r
1129  (UP_ASM_TAC);\r
1130  (ASM_REWRITE_TAC[ TRUNCATE_SIMPLEX_EXPLICIT_1; VORONOI_LIST; VORONOI_SET;set_of_list]); \r
1131  (REWRITE_WITH `INTERS {voronoi_closed V v | v IN {u0, u1:real^3}} = \r
1132                         voronoi_closed V u0 INTER voronoi_closed V u1`);\r
1133  (SET_TAC[]);\r
1134 \r
1135 \r
1136  (REWRITE_TAC[IN_INTER; voronoi_closed; IN; IN_ELIM_THM; INTERS; DIST_REFL]);\r
1137  (REPEAT STRIP_TAC);\r
1138  (NEW_GOAL `dist (u0, u1:real^3) <= dist (u0, u0)`);\r
1139  (FIRST_ASSUM MATCH_MP_TAC);\r
1140  (ASM_SET_TAC[BARV_IMP_u0_IN_V]);\r
1141  (NEW_GOAL `u0 = u1:real^3`);\r
1142  (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL] THEN DISCH_TAC);\r
1143  (NEW_GOAL `dist (u0,u1:real^3) = &0`);\r
1144  (NEW_GOAL `&0 <= dist (u0,u1:real^3) `);\r
1145  (REWRITE_TAC[DIST_POS_LE]);\r
1146  (ASM_REAL_ARITH_TAC);\r
1147  (ASM_MESON_TAC[DIST_EQ_0]);\r
1148  (NEW_GOAL `aff_dim (set_of_list [u0;u1:real^3]) = &0`);\r
1149  (ASM_REWRITE_TAC[set_of_list; SET_RULE `{x, x} = {x}`; AFF_DIM_SING]);\r
1150  (NEW_GOAL `aff_dim (set_of_list [u0;u1:real^3]) = &1`);\r
1151  (MATCH_MP_TAC MHFTTZN1);\r
1152  (EXISTS_TAC `V:real^3->bool`);\r
1153  (ASM_REWRITE_TAC[]);\r
1154  (REWRITE_WITH `[u1; u1:real^3] = truncate_simplex 1 ul`);\r
1155  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
1156  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1157  (EXISTS_TAC `3`);\r
1158  (ASM_REWRITE_TAC[]);\r
1159  (ARITH_TAC);\r
1160 \r
1161  (NEW_GOAL `&0 = &1`);\r
1162  (ASM_MESON_TAC[INT_OF_NUM_EQ;REAL_OF_NUM_EQ]);\r
1163  (UP_ASM_TAC THEN REAL_ARITH_TAC)]);;\r
1164 \r
1165 (* ======================================================================= *)\r
1166 (* Lemma 25 *)\r
1167 let RADIAL_VS_RADIAL_NORM = prove_by_refinement (\r
1168  `!(x:real^3) r C. radial r x C <=> radial_norm r x C`,\r
1169 [ (REPEAT GEN_TAC);\r
1170  (REWRITE_TAC[radial; Vol1.radial_norm]);\r
1171  (REWRITE_WITH `!(x:real^3) r. ball (x, r) = normball x r`);\r
1172  (REWRITE_TAC[ball; normball; DIST_SYM])]);; \r
1173 \r
1174 (* ======================================================================= *)\r
1175 (* Lemma 26 *)\r
1176 \r
1177 let EVENTUALLY_RADIAL_INTER = prove_by_refinement (\r
1178  `!(x:real^3) C C'. \r
1179      eventually_radial x C /\ eventually_radial x C' ==>\r
1180      eventually_radial x (C INTER C')`,\r
1181 [ (REWRITE_TAC[eventually_radial; RADIAL_VS_RADIAL_NORM]);\r
1182  (REWRITE_WITH `!(x:real^3) r. ball (x, r) = normball x r`);\r
1183  (REWRITE_TAC[ball; normball; DIST_SYM]); \r
1184  (REPEAT STRIP_TAC);\r
1185  (ASM_CASES_TAC `r >= r'`);\r
1186  (EXISTS_TAC `r':real`);\r
1187  (ASM_REWRITE_TAC[]);\r
1188 \r
1189  (REWRITE_WITH `(C INTER C') INTER normball (x:real^3) r' =\r
1190                   (C INTER normball x r') INTER (C' INTER normball x r')`);\r
1191  (SET_TAC[]);\r
1192  (MATCH_MP_TAC Vol1.inter_radial);\r
1193  (ASM_REWRITE_TAC[]);\r
1194  (UNDISCH_TAC `radial_norm r (x:real^3) (C INTER normball x r)`);\r
1195  (REWRITE_TAC[Vol1.radial_norm; normball]);\r
1196  (REPEAT STRIP_TAC);\r
1197  (REWRITE_TAC[INTER_SUBSET]);\r
1198 \r
1199  (NEW_GOAL `x + u IN C INTER {y | dist (y,x:real^3) < r}`); \r
1200  (MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET t) ==> a IN t `));\r
1201  (EXISTS_TAC `C INTER {y | dist (y,x:real^3) < r'}`);\r
1202  (ASM_REWRITE_TAC[SUBSET;IN_INTER;IN; IN_ELIM_THM]);\r
1203  (REPEAT STRIP_TAC);\r
1204  (ASM_REWRITE_TAC[]);\r
1205  (ASM_REAL_ARITH_TAC);\r
1206  (NEW_GOAL `(!t. t > &0 /\ t * norm u < r\r
1207                    ==> x + t % u IN C INTER {y | dist (y,x:real^3) < r})`);\r
1208  (ASM_MESON_TAC[]);\r
1209  (NEW_GOAL `x + t % u IN C INTER {y | dist (y,x:real^3) < r}`);\r
1210  (FIRST_ASSUM MATCH_MP_TAC);\r
1211  (ASM_REAL_ARITH_TAC);\r
1212  (UP_ASM_TAC THEN REWRITE_TAC[IN_INTER;IN;IN_ELIM_THM]);\r
1213  (REPEAT STRIP_TAC);\r
1214  (ASM_REWRITE_TAC[]);\r
1215  (REWRITE_TAC[dist; VECTOR_ARITH `((a:real^3) + b) - a = b`; NORM_MUL]);\r
1216  (REWRITE_WITH `abs t = t`);\r
1217  (REWRITE_TAC[REAL_ABS_REFL]);\r
1218  (ASM_REAL_ARITH_TAC);\r
1219  (ASM_REWRITE_TAC[]);\r
1220 \r
1221  (EXISTS_TAC `r:real`);\r
1222  (ASM_REWRITE_TAC[]);\r
1223 \r
1224  (REWRITE_WITH `(C INTER C') INTER normball (x:real^3) r =\r
1225                   (C INTER normball x r) INTER (C' INTER normball x r)`);\r
1226  (SET_TAC[]);\r
1227  (MATCH_MP_TAC Vol1.inter_radial);\r
1228  (ASM_REWRITE_TAC[]);\r
1229  (UNDISCH_TAC `radial_norm r' (x:real^3) (C' INTER normball x r')`);\r
1230  (REWRITE_TAC[Vol1.radial_norm; normball]);\r
1231  (REPEAT STRIP_TAC);\r
1232  (REWRITE_TAC[INTER_SUBSET]);\r
1233 \r
1234  (NEW_GOAL `x + u IN C' INTER {y | dist (y,x:real^3) < r'}`); \r
1235  (MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET t) ==> a IN t `));\r
1236  (EXISTS_TAC `C' INTER {y | dist (y,x:real^3) < r}`);\r
1237  (ASM_REWRITE_TAC[SUBSET;IN_INTER;IN; IN_ELIM_THM]);\r
1238  (REPEAT STRIP_TAC);\r
1239  (ASM_REWRITE_TAC[]);\r
1240  (ASM_REAL_ARITH_TAC);\r
1241  (NEW_GOAL `(!t. t > &0 /\ t * norm u < r'\r
1242                    ==> x + t % u IN C' INTER {y | dist (y,x:real^3) < r'})`);\r
1243  (ASM_MESON_TAC[]);\r
1244  (NEW_GOAL `x + t % u IN C' INTER {y | dist (y,x:real^3) < r'}`);\r
1245  (FIRST_ASSUM MATCH_MP_TAC);\r
1246  (ASM_REAL_ARITH_TAC);\r
1247  (UP_ASM_TAC THEN REWRITE_TAC[IN_INTER;IN;IN_ELIM_THM]);\r
1248  (REPEAT STRIP_TAC);\r
1249  (ASM_REWRITE_TAC[]);\r
1250  (REWRITE_TAC[dist; VECTOR_ARITH `((a:real^3) + b) - a = b`; NORM_MUL]);\r
1251  (REWRITE_WITH `abs t = t`);\r
1252  (REWRITE_TAC[REAL_ABS_REFL]);\r
1253  (ASM_REAL_ARITH_TAC);\r
1254  (ASM_REWRITE_TAC[])]);;\r
1255 \r
1256 (* ======================================================================= *)\r
1257 (* Lemma 27 *)\r
1258 let SET_EQ_LEMMA = SET_RULE \r
1259    `A = B <=> (!x. (x IN A ==> x IN B) /\ (x IN B ==> x IN A))`;;\r
1260 \r
1261 let SET_OF_0_TO_3 = prove_by_refinement ( \r
1262  `{j | j < 4} = {0,1,2,3}`,\r
1263 [(REWRITE_TAC[SET_EQ_LEMMA;IN;IN_ELIM_THM] THEN GEN_TAC);\r
1264  (ASM_CASES_TAC `x = 0`); (ASM_REWRITE_TAC[]); \r
1265  (TRUONG_SET_TAC[ARITH_RULE `0 < 4`]);\r
1266  (ASM_CASES_TAC `x = 1`);(ASM_REWRITE_TAC[]);\r
1267  (TRUONG_SET_TAC[ARITH_RULE `1 < 4`]);\r
1268  (ASM_CASES_TAC `x = 2`); (ASM_REWRITE_TAC[]);\r
1269  (TRUONG_SET_TAC[ARITH_RULE `2 < 4`]);\r
1270  (ASM_CASES_TAC `x = 3`); (ASM_REWRITE_TAC[]);\r
1271  (TRUONG_SET_TAC[ARITH_RULE `3 < 4`]);\r
1272  (NEW_GOAL `x >= 4`); (ASM_ARITH_TAC); (REPEAT STRIP_TAC);\r
1273  (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `F`);\r
1274  (UP_ASM_TAC THEN TRUONG_SET_TAC[]); (ASM_MESON_TAC[])]);;\r
1275 \r
1276 let SET_OF_0_TO_2 = prove_by_refinement ( \r
1277  `{j | j <= 2 } = {0,1,2}`,\r
1278 [(REWRITE_TAC[SET_EQ_LEMMA;IN;IN_ELIM_THM] THEN GEN_TAC);\r
1279  (ASM_CASES_TAC `x = 0`); (ASM_REWRITE_TAC[]); \r
1280  (TRUONG_SET_TAC[ARITH_RULE `0 <= 2`]);\r
1281  (ASM_CASES_TAC `x = 1`);(ASM_REWRITE_TAC[]);\r
1282  (TRUONG_SET_TAC[ARITH_RULE `1 <= 2`]);\r
1283  (ASM_CASES_TAC `x = 2`); (ASM_REWRITE_TAC[]);\r
1284  (TRUONG_SET_TAC[ARITH_RULE `2 <= 2`]);\r
1285  (NEW_GOAL `x >= 3`); (ASM_ARITH_TAC); (REPEAT STRIP_TAC);\r
1286  (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `F`);\r
1287  (UP_ASM_TAC THEN TRUONG_SET_TAC[]); (ASM_MESON_TAC[])]);;\r
1288 \r
1289 let ZERO_LT_SQRT_2 = prove_by_refinement(`&1 < sqrt (&2)`,\r
1290 [(NEW_GOAL `&0 < sqrt (&2)`); (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);\r
1291  (NEW_GOAL `&1 = abs (&1) /\ sqrt (&2) = abs (sqrt (&2))`);\r
1292  ONCE_REWRITE_TAC[EQ_SYM_EQ]; REWRITE_TAC[REAL_ABS_REFL]; ASM_REAL_ARITH_TAC;\r
1293  ONCE_ASM_REWRITE_TAC[];\r
1294  REWRITE_TAC[REAL_LT_SQUARE_ABS; REAL_ARITH `&1 pow 2 = &1`];\r
1295  REWRITE_WITH `sqrt (&2) pow 2 = &2`; MATCH_MP_TAC SQRT_POW_2;REAL_ARITH_TAC;\r
1296  REAL_ARITH_TAC]);;\r
1297 \r
1298 (* ======================================================================= *)\r
1299 (* Lemma 28 *)\r
1300 let RCONE_GE_TRANS = prove_by_refinement (\r
1301  `!(a:real^3) b r x t. \r
1302        &0 <= t /\ (a + x) IN rcone_ge a b r ==> a + t % x IN rcone_ge a b r`,\r
1303 [(REWRITE_TAC[rcone_ge; rconesgn; IN; IN_ELIM_THM; dist]);\r
1304  (REWRITE_TAC[VECTOR_ARITH `((a:real^3) + x) - a = x`; DOT_LMUL; NORM_MUL]);\r
1305  (REPEAT STRIP_TAC);\r
1306  (REWRITE_WITH `abs t = t`);\r
1307  (ASM_REWRITE_TAC[REAL_ABS_REFL]);\r
1308  (REWRITE_TAC[REAL_ARITH `t * x >= ( t * m) * n <=> &0 <= t * (x - m * n)`]);\r
1309  (MATCH_MP_TAC REAL_LE_MUL);\r
1310  (ASM_REAL_ARITH_TAC)]);;\r
1311 (* ======================================================================= *)\r
1312 (* Lemma 29 *)\r
1313 \r
1314 let RCONE_GE_INTERS_PROJECTION_KY_LEMMA = prove_by_refinement (\r
1315  `!(a:real^3) b r x:real^3. \r
1316     &0 < r /\ r < &1 /\  ~(a = b) /\ \r
1317     x IN (rcone_ge a b r) INTER (rcone_ge b a r)\r
1318     ==> (?s. s IN convex hull {a, b} /\ (x - s) dot (a - b)= &0 )`,\r
1319 [(REWRITE_TAC[rcone_ge; rconesgn; IN_INTER;IN; IN_ELIM_THM; dist]);\r
1320  (REPEAT STRIP_TAC);\r
1321  (NEW_GOAL `?s. s IN aff {a, b:real^3} /\ (x - s) dot (a - b) = &0`);\r
1322  (MESON_TAC[Trigonometry2.EXISTS_PROJECTING_POINT2]);\r
1323  (FIRST_X_ASSUM CHOOSE_TAC);\r
1324  (EXISTS_TAC `s:real^3`);\r
1325  (UP_ASM_TAC THEN \r
1326    ASM_REWRITE_TAC[Topology.affine_hull_2_fan; IN; IN_ELIM_THM]);\r
1327  (REPEAT STRIP_TAC);\r
1328  (ASM_REWRITE_TAC[CONVEX_HULL_2; IN_ELIM_THM]);\r
1329  (EXISTS_TAC `t1:real`);\r
1330  (EXISTS_TAC `t2:real`);\r
1331  (ASM_REWRITE_TAC[]);\r
1332  (STRIP_TAC);\r
1333 \r
1334 (* Case 1 *)\r
1335 \r
1336  (ASM_CASES_TAC `t1 < &0`);\r
1337  (NEW_GOAL `(x - b:real^3) dot (a - b) < &0`);\r
1338  (REWRITE_WITH `(x - b:real^3) dot (a - b) =      \r
1339                  (x - s) dot (a - b) + (s - b) dot (a - b)`);\r
1340  (VECTOR_ARITH_TAC);\r
1341  (ASM_REWRITE_TAC[REAL_ADD_RID; REAL_ADD_LID]);\r
1342  (REWRITE_WITH `((t1 % a + t2 % b) - b) =  t1 % (a - b:real^3)`);\r
1343  (REWRITE_WITH `((t1 % a + t2 % b) - b:real^3) =  (t1 % a + t2 % b) - (t1 + t2) % b`);\r
1344  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1345  (VECTOR_ARITH_TAC);\r
1346  (REWRITE_TAC[DOT_LMUL]);\r
1347  (ONCE_REWRITE_TAC[GSYM REAL_LT_NEG]);\r
1348  (REWRITE_TAC[REAL_ARITH `-- (a * b) = (-- a) * b`; REAL_NEG_0]);\r
1349  (MATCH_MP_TAC REAL_LT_MUL);\r
1350  (STRIP_TAC);\r
1351  (ASM_REAL_ARITH_TAC);\r
1352  (REWRITE_TAC[GSYM NORM_POW_2]);\r
1353  (MATCH_MP_TAC REAL_POW_LT);\r
1354  (REWRITE_TAC[NORM_POS_LT]);\r
1355  (ASM_REWRITE_TAC[VECTOR_ARITH `(a:real^3 - b = vec 0 <=> a = b)`]);\r
1356  (NEW_GOAL `norm (x - b) * norm (a - b:real^3) * r < &0`);\r
1357  (ASM_REAL_ARITH_TAC);\r
1358  (NEW_GOAL `&0 <= norm (x - b) * norm (a - b:real^3) * r`);\r
1359  (MATCH_MP_TAC REAL_LE_MUL);\r
1360  (REWRITE_TAC[NORM_POS_LE]);\r
1361  (MATCH_MP_TAC REAL_LE_MUL);\r
1362  (REWRITE_TAC[NORM_POS_LE]);\r
1363  (ASM_REAL_ARITH_TAC);\r
1364  (ASM_REAL_ARITH_TAC);\r
1365  (ASM_REAL_ARITH_TAC);\r
1366 \r
1367 (* Case 2 *)\r
1368 \r
1369  (ASM_CASES_TAC `t2 < &0`);\r
1370  (NEW_GOAL `(x - a:real^3) dot (b - a) < &0`);\r
1371  (REWRITE_WITH `(x - a:real^3) dot (b - a) =      \r
1372                  (a - s) dot (a - b) - (x - s) dot (a - b)`);\r
1373  (VECTOR_ARITH_TAC);\r
1374  (ASM_REWRITE_TAC[REAL_ARITH `a - &0 = a`]);\r
1375  (REWRITE_WITH `a - (t1 % a + t2 % b) =  t2 % (a - b:real^3)`);\r
1376  (REWRITE_WITH `(a:real^3) - (t1 % a + t2 % b) =  (t1 + t2) % a - (t1 % a + t2 % b)`);\r
1377 \r
1378  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1379  (VECTOR_ARITH_TAC);\r
1380  (REWRITE_TAC[DOT_LMUL]);\r
1381  (ONCE_REWRITE_TAC[GSYM REAL_LT_NEG]);\r
1382  (REWRITE_TAC[REAL_ARITH `-- (a * b) = (-- a) * b`; REAL_NEG_0]);\r
1383  (MATCH_MP_TAC REAL_LT_MUL);\r
1384  (STRIP_TAC);\r
1385  (ASM_REAL_ARITH_TAC);\r
1386  (REWRITE_TAC[GSYM NORM_POW_2]);\r
1387  (MATCH_MP_TAC REAL_POW_LT);\r
1388  (REWRITE_TAC[NORM_POS_LT]);\r
1389  (ASM_REWRITE_TAC[VECTOR_ARITH `(a:real^3 - b = vec 0 <=> a = b)`]);\r
1390  (NEW_GOAL `norm (x - a) * norm (b - a:real^3) * r < &0`);\r
1391  (ASM_REAL_ARITH_TAC);\r
1392  (NEW_GOAL `&0 <= norm (x - a) * norm (b - a:real^3) * r`);\r
1393  (MATCH_MP_TAC REAL_LE_MUL);\r
1394  (REWRITE_TAC[NORM_POS_LE]);\r
1395  (MATCH_MP_TAC REAL_LE_MUL);\r
1396  (REWRITE_TAC[NORM_POS_LE]);\r
1397  (ASM_REAL_ARITH_TAC);\r
1398  (ASM_REAL_ARITH_TAC);\r
1399  (ASM_REAL_ARITH_TAC);\r
1400 \r
1401  (ASM_REWRITE_TAC[])]);;\r
1402 \r
1403 (* ======================================================================= *)\r
1404 (* Lemma 30 *)\r
1405 let RCONE_GE_INTER_VORONOI_CLOSED_PROJECTION_KY_LEMMA = prove_by_refinement(\r
1406  `!(a:real^3) b r x:real^3 V. \r
1407     &0 < r /\ ~(a = b) /\ a IN V /\ b IN V /\\r
1408     x IN (rcone_ge a b r) INTER (voronoi_closed V a)\r
1409     ==> (?s. s IN convex hull {a, b} /\ (x - s) dot (a - b)= &0 )`,\r
1410 [(REWRITE_TAC[voronoi_closed; rcone_ge; rconesgn; IN_INTER;IN; IN_ELIM_THM; dist]);\r
1411  (REPEAT STRIP_TAC);\r
1412  (NEW_GOAL `?s. s IN aff {a, b:real^3} /\ (x - s) dot (a - b) = &0`);\r
1413  (MESON_TAC[Trigonometry2.EXISTS_PROJECTING_POINT2]);\r
1414  (FIRST_X_ASSUM CHOOSE_TAC);\r
1415  (EXISTS_TAC `s:real^3`);\r
1416  (ASM_REWRITE_TAC[]);\r
1417  (UP_ASM_TAC THEN \r
1418    ASM_REWRITE_TAC[Topology.affine_hull_2_fan; IN; IN_ELIM_THM]);\r
1419  (REPEAT STRIP_TAC);\r
1420  (ASM_REWRITE_TAC[CONVEX_HULL_2; IN_ELIM_THM]);\r
1421  (EXISTS_TAC `t1:real`);\r
1422  (EXISTS_TAC `t2:real`);\r
1423  (ASM_REWRITE_TAC[]);\r
1424  (ONCE_REWRITE_TAC[MESON[] `a /\ b <=> b /\ a`]);\r
1425  (STRIP_TAC);\r
1426 \r
1427 (* Case 1 : &0 <= t2 *)\r
1428 \r
1429  (ASM_CASES_TAC `t2 < &0`);\r
1430  (NEW_GOAL `(x - a:real^3) dot (b - a) < &0`);\r
1431  (REWRITE_WITH `(x - a:real^3) dot (b - a) =      \r
1432                  (a - s) dot (a - b) - (x - s) dot (a - b)`);\r
1433  (VECTOR_ARITH_TAC);\r
1434  (ASM_REWRITE_TAC[REAL_ARITH `a - &0 = a`]);\r
1435  (REWRITE_WITH `a - (t1 % a + t2 % b) =  t2 % (a - b:real^3)`);\r
1436  (REWRITE_WITH `(a:real^3) - (t1 % a + t2 % b) =  (t1 + t2) % a - (t1 % a + t2 % b)`);\r
1437 \r
1438  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1439  (VECTOR_ARITH_TAC);\r
1440  (REWRITE_TAC[DOT_LMUL]);\r
1441  (ONCE_REWRITE_TAC[GSYM REAL_LT_NEG]);\r
1442  (REWRITE_TAC[REAL_ARITH `-- (a * b) = (-- a) * b`; REAL_NEG_0]);\r
1443  (MATCH_MP_TAC REAL_LT_MUL);\r
1444  (STRIP_TAC);\r
1445  (ASM_REAL_ARITH_TAC);\r
1446  (REWRITE_TAC[GSYM NORM_POW_2]);\r
1447  (MATCH_MP_TAC REAL_POW_LT);\r
1448  (REWRITE_TAC[NORM_POS_LT]);\r
1449  (ASM_REWRITE_TAC[VECTOR_ARITH `(a:real^3 - b = vec 0 <=> a = b)`]);\r
1450  (NEW_GOAL `norm (x - a) * norm (b - a:real^3) * r < &0`);\r
1451  (ASM_REAL_ARITH_TAC);\r
1452  (NEW_GOAL `&0 <= norm (x - a) * norm (b - a:real^3) * r`);\r
1453  (MATCH_MP_TAC REAL_LE_MUL);\r
1454  (REWRITE_TAC[NORM_POS_LE]);\r
1455  (MATCH_MP_TAC REAL_LE_MUL);\r
1456  (REWRITE_TAC[NORM_POS_LE]);\r
1457  (ASM_REAL_ARITH_TAC);\r
1458  (ASM_REAL_ARITH_TAC);\r
1459  (ASM_REAL_ARITH_TAC);\r
1460 \r
1461 (* Case 2 : &0 <= t1 *)\r
1462 \r
1463  (ASM_CASES_TAC `t1 < &0`);\r
1464  (NEW_GOAL `norm (x - a) <= norm (x - b:real^3)`);\r
1465  (ASM_SIMP_TAC[]);\r
1466  (NEW_GOAL `norm (x - b) < norm (x - a:real^3)`);\r
1467  (NEW_GOAL `norm (x - b) < norm (x - a:real^3) <=> \r
1468              norm (x - b) pow 2 < norm (x - a) pow 2`);\r
1469  (MATCH_MP_TAC Pack1.bp_bdt);\r
1470  (REWRITE_TAC[NORM_POS_LE]);\r
1471  (ASM_REWRITE_TAC[]);\r
1472 \r
1473 \r
1474  (REWRITE_WITH `norm (x - b) pow 2 = norm (s - b) pow 2 + norm (x - s:real^3) pow 2`);\r
1475  (MATCH_MP_TAC PYTHAGORAS);\r
1476  (REWRITE_TAC[orthogonal]);\r
1477  (REWRITE_WITH `b:real^3 - s = t1 % (b - a)`);\r
1478  (ASM_REWRITE_TAC[]);\r
1479  (REWRITE_WITH `b:real^3 - (t1 % a + t2 % b) = (t1 + t2) % b - (t1 % a + t2 % b)`);\r
1480  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1481  (VECTOR_ARITH_TAC);\r
1482  (REWRITE_TAC[DOT_LMUL]);\r
1483  (REWRITE_WITH `(b - a:real^3) dot (x - s) = -- ((x - s) dot (a - b))`);\r
1484  (VECTOR_ARITH_TAC);\r
1485  (ASM_REWRITE_TAC[]);\r
1486  (REAL_ARITH_TAC);\r
1487 \r
1488 \r
1489  (REWRITE_WITH `norm (x - a) pow 2 = norm (s - a) pow 2 + norm (x - s:real^3) pow 2`);\r
1490  (MATCH_MP_TAC PYTHAGORAS);\r
1491  (REWRITE_TAC[orthogonal]);\r
1492  (REWRITE_WITH `a:real^3 - s = t2 % (a - b)`);\r
1493  (ASM_REWRITE_TAC[]);\r
1494  (REWRITE_WITH `a:real^3 - (t1 % a + t2 % b) = (t1 + t2) % a - (t1 % a + t2 % b)`);\r
1495  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1496  (VECTOR_ARITH_TAC);\r
1497  (REWRITE_TAC[DOT_LMUL]);\r
1498  (REWRITE_WITH `(a - b:real^3) dot (x - s) = ((x - s) dot (a - b))`);\r
1499  (VECTOR_ARITH_TAC);\r
1500  (ASM_REWRITE_TAC[]);\r
1501  (REAL_ARITH_TAC);\r
1502 \r
1503 \r
1504  (MATCH_MP_TAC (REAL_ARITH `x < y ==> x + z < y + z`));\r
1505  (REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS]);\r
1506  (REWRITE_WITH `abs (norm (s - b:real^3)) = norm (s - b)`);\r
1507  (REWRITE_TAC[REAL_ABS_REFL; NORM_POS_LE]);\r
1508  (REWRITE_WITH `abs (norm (s - a:real^3)) = norm (s - a)`);\r
1509  (REWRITE_TAC[REAL_ABS_REFL; NORM_POS_LE]);\r
1510 \r
1511  (REWRITE_WITH `s:real^3 - a = t2 % (b - a)`);\r
1512  (ASM_REWRITE_TAC[]);\r
1513  (REWRITE_WITH `(t1 % a + t2 % b) - a:real^3 = (t1 % a + t2 % b) - (t1 + t2) % a`);\r
1514  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1515  (VECTOR_ARITH_TAC);\r
1516  (REWRITE_WITH `s:real^3 - b = t1 % (a - b)`);\r
1517  (ASM_REWRITE_TAC[]);\r
1518  (REWRITE_WITH `(t1 % a + t2 % b) - b:real^3 = (t1 % a + t2 % b) - (t1 + t2) % b`);\r
1519  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1520  (VECTOR_ARITH_TAC);\r
1521  (REWRITE_TAC[NORM_MUL; GSYM dist; DIST_SYM]);\r
1522  (MATCH_MP_TAC (REAL_ARITH `&0 < x * (a - b) ==> b * x < a * x`));\r
1523  (MATCH_MP_TAC REAL_LT_MUL);\r
1524  (STRIP_TAC);\r
1525  (MATCH_MP_TAC DIST_POS_LT);\r
1526  (ASM_REWRITE_TAC[]);\r
1527  (REWRITE_WITH `t2 = &1 - t1`);\r
1528  (ASM_REAL_ARITH_TAC);\r
1529  (REWRITE_WITH `abs (t1) = abs (-- t1)`);\r
1530  (REWRITE_TAC[REAL_ABS_NEG]);\r
1531  (REWRITE_WITH `abs (&1 - t1) = &1 - t1`);\r
1532  (REWRITE_TAC[REAL_ABS_REFL]);\r
1533  (ASM_REAL_ARITH_TAC);\r
1534  (REWRITE_WITH `abs (-- t1) =  (-- t1)`);\r
1535  (REWRITE_TAC[REAL_ABS_REFL]);\r
1536  (ASM_REAL_ARITH_TAC);\r
1537  (ASM_REAL_ARITH_TAC);\r
1538  (ASM_REAL_ARITH_TAC);\r
1539  (ASM_REAL_ARITH_TAC)]);;\r
1540 \r
1541 (* ======================================================================= *)\r
1542 (* Lemma 31 *)\r
1543 let RCONEGE_INTER_VORONOI_CLOSED_IMP_RCONEGE = prove_by_refinement(\r
1544  `!V a:real^3 b r x.\r
1545      packing V /\\r
1546      saturated V /\\r
1547      a IN V /\\r
1548      b IN V /\\r
1549      ~(a = b) /\\r
1550      &0 < r /\\r
1551      r <= &1 /\\r
1552      x IN rcone_ge a b r /\\r
1553      x IN voronoi_closed V a ==> x IN rcone_ge b a r`,\r
1554 \r
1555 [(REPEAT STRIP_TAC);\r
1556  (NEW_GOAL `?s. s IN convex hull {a, b:real^3} /\ (x - s) dot (a - b) = &0`);\r
1557  (MATCH_MP_TAC RCONE_GE_INTER_VORONOI_CLOSED_PROJECTION_KY_LEMMA);\r
1558  (EXISTS_TAC `r:real`);\r
1559  (EXISTS_TAC `V:real^3->bool`);\r
1560  (ASM_REWRITE_TAC[IN_INTER]);\r
1561  (FIRST_X_ASSUM CHOOSE_TAC);\r
1562  (UNDISCH_TAC `x IN rcone_ge (a:real^3) b r`);\r
1563  (REWRITE_TAC[rcone_ge; rconesgn; IN; IN_ELIM_THM; dist]);\r
1564  (DISCH_TAC);\r
1565  (SWITCH_TAC THEN UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
1566  (REPEAT STRIP_TAC);\r
1567 \r
1568 \r
1569 \r
1570  (NEW_GOAL `((x - (b:real^3)) dot (a - b)) * norm (x - a) >= \r
1571              ((x - a) dot (b - a)) * norm (x - b)`);\r
1572  (REWRITE_WITH `(x - b) dot (a - b:real^3) = \r
1573                  (x - s) dot (a - b) + (s - b) dot (a - b)`);\r
1574  (VECTOR_ARITH_TAC);\r
1575  (REWRITE_WITH `(x - a) dot (b - a:real^3) = \r
1576                  (a - s) dot (a - b) - (x - s) dot (a - b)`);\r
1577  (VECTOR_ARITH_TAC);\r
1578  (ASM_REWRITE_TAC[REAL_ADD_LID; REAL_ARITH `a - &0 = a`]);\r
1579  (REWRITE_WITH `(u % a + v % b) - b = u % (a - b:real^3)`);\r
1580  (REWRITE_WITH `(u % a + v % b:real^3) - b = (u % a + v % b) - (u + v) % b`);\r
1581  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1582  (VECTOR_ARITH_TAC);\r
1583 \r
1584  (REWRITE_WITH `a - (u % a + v % b) = v % (a - b:real^3)`);\r
1585  (REWRITE_WITH `a - (u % a + v % b:real^3) = (u + v) % a - (u % a + v % b)`);\r
1586  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1587  (VECTOR_ARITH_TAC);\r
1588  (REWRITE_TAC[DOT_LMUL; GSYM NORM_POW_2; GSYM dist]);\r
1589  (REWRITE_TAC[REAL_ARITH `(a * x) * y >= (b * x) * z <=> &0 <= x * (a * y - b * z)`]);\r
1590  (MATCH_MP_TAC REAL_LE_MUL);\r
1591  (REWRITE_TAC[REAL_LE_POW_2]);\r
1592  (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);\r
1593  (NEW_GOAL `v * dist (x,b) <= u * dist (x,a:real^3) <=>\r
1594              (v * dist (x,b)) pow 2 <= (u * dist (x,a)) pow 2`);\r
1595  (MATCH_MP_TAC Trigonometry2.POW2_COND);\r
1596  (ASM_SIMP_TAC[REAL_LE_MUL; DIST_POS_LE]);\r
1597  (ASM_REWRITE_TAC[]);\r
1598  (REWRITE_TAC[REAL_ARITH `(x * y) pow 2 = (x pow 2) * (y pow 2)`; dist]);\r
1599 \r
1600  (REWRITE_WITH `norm (x:real^3 - b) pow 2 = norm (s - b) pow 2 + norm (x - s) pow 2`);\r
1601  (MATCH_MP_TAC PYTHAGORAS);\r
1602  (REWRITE_TAC[orthogonal]);\r
1603  (REWRITE_WITH `b - s:real^3 = -- u % (a - b)`);\r
1604  (ASM_REWRITE_TAC[]);\r
1605  (REWRITE_WITH `b:real^3 - (u % a + v % b) = (u + v) % b - (u % a + v % b)`);\r
1606  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1607  (VECTOR_ARITH_TAC);\r
1608  (ASM_MESON_TAC[DOT_LMUL; REAL_MUL_RZERO;DOT_SYM]);\r
1609  (REWRITE_WITH `norm (s - b:real^3) = norm (b - s)`);\r
1610  (NORM_ARITH_TAC);\r
1611  (REWRITE_WITH `b - s:real^3 = -- u % (a - b)`);\r
1612  (ASM_REWRITE_TAC[]);\r
1613  (REWRITE_WITH `b:real^3 - (u % a + v % b) = (u + v) % b - (u % a + v % b)`);\r
1614  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1615  (VECTOR_ARITH_TAC);\r
1616  (REWRITE_TAC[NORM_MUL; REAL_ABS_NEG]);\r
1617 \r
1618  (REWRITE_WITH `norm (x:real^3 - a) pow 2 = norm (s - a) pow 2 + norm (x - s) pow 2`);\r
1619  (MATCH_MP_TAC PYTHAGORAS);\r
1620  (REWRITE_TAC[orthogonal]);\r
1621  (REWRITE_WITH `a - s:real^3 = v % (a - b)`);\r
1622  (ASM_REWRITE_TAC[]);\r
1623  (REWRITE_WITH `a:real^3 - (u % a + v % b) = (u + v) % a - (u % a + v % b)`);\r
1624  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1625  (VECTOR_ARITH_TAC);\r
1626  (ASM_MESON_TAC[DOT_LMUL; REAL_MUL_RZERO;DOT_SYM]);\r
1627  (REWRITE_WITH `norm (s - a:real^3) = norm (a - s)`);\r
1628  (NORM_ARITH_TAC);\r
1629  (REWRITE_WITH `a - s:real^3 = v % (a - b)`);\r
1630  (ASM_REWRITE_TAC[]);\r
1631  (REWRITE_WITH `a:real^3 - (u % a + v % b) = (u + v) % a - (u % a + v % b)`);\r
1632  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1633  (VECTOR_ARITH_TAC);\r
1634  (REWRITE_TAC[NORM_MUL]);\r
1635 \r
1636  (REWRITE_TAC[REAL_POW_MUL; REAL_POW2_ABS]);\r
1637  (REWRITE_TAC[REAL_ARITH `x * (y * z + t) <= y * (x * z + t) <=>\r
1638                           &0 <= t * (y - x)`]);\r
1639  (MATCH_MP_TAC REAL_LE_MUL);\r
1640  (REWRITE_TAC[REAL_LE_POW_2]);\r
1641  (REWRITE_TAC[REAL_ARITH `&0 <= x - y <=> y <= x`]);\r
1642  (NEW_GOAL `v pow 2 <= u pow 2 <=> v <= u`);\r
1643  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
1644  (MATCH_MP_TAC Trigonometry2.POW2_COND THEN ASM_REWRITE_TAC[]);\r
1645  (ASM_REWRITE_TAC[]);\r
1646  (UNDISCH_TAC `(x:real^3) IN voronoi_closed V a`);\r
1647  (REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);\r
1648  (REPEAT STRIP_TAC);\r
1649  (NEW_GOAL `dist (x,a) <= dist (x,b:real^3)`);\r
1650  (FIRST_ASSUM MATCH_MP_TAC);\r
1651  (ASM_SET_TAC[]);\r
1652  (NEW_GOAL `dist (x,a:real^3) <= dist (x,b) <=> \r
1653              dist (x,a) pow 2 <= dist (x,b) pow 2`);\r
1654  (MATCH_MP_TAC Trigonometry2.POW2_COND THEN ASM_REWRITE_TAC[]);\r
1655  (REWRITE_TAC[DIST_POS_LE]);\r
1656  (NEW_GOAL `dist (x,a) pow 2 <= dist (x,b:real^3) pow 2`);\r
1657  (ASM_MESON_TAC[]);\r
1658  (UP_ASM_TAC THEN REWRITE_TAC[dist]);\r
1659 \r
1660  (REWRITE_WITH `norm (x:real^3 - a) pow 2 = norm (s - a) pow 2 + norm (x - s) pow 2`);\r
1661  (MATCH_MP_TAC PYTHAGORAS);\r
1662  (REWRITE_TAC[orthogonal]);\r
1663  (REWRITE_WITH `a - s:real^3 = v % (a - b)`);\r
1664  (ASM_REWRITE_TAC[]);\r
1665  (REWRITE_WITH `a:real^3 - (u % a + v % b) = (u + v) % a - (u % a + v % b)`);\r
1666  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1667  (VECTOR_ARITH_TAC);\r
1668  (ASM_MESON_TAC[DOT_LMUL; REAL_MUL_RZERO;DOT_SYM]);\r
1669 \r
1670  (REWRITE_WITH `norm (s - a:real^3) = norm (a - s)`);\r
1671  (NORM_ARITH_TAC);\r
1672  (REWRITE_WITH `a - s:real^3 = v % (a - b)`);\r
1673  (ASM_REWRITE_TAC[]);\r
1674  (REWRITE_WITH `a:real^3 - (u % a + v % b) = (u + v) % a - (u % a + v % b)`);\r
1675  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1676  (VECTOR_ARITH_TAC);\r
1677  (REWRITE_TAC[NORM_MUL]);\r
1678  (REWRITE_TAC[REAL_POW_MUL; REAL_POW2_ABS]);\r
1679 \r
1680  (REWRITE_WITH `norm (x:real^3 - b) pow 2 = norm (s - b) pow 2 + norm (x - s) pow 2`);\r
1681  (MATCH_MP_TAC PYTHAGORAS);\r
1682  (REWRITE_TAC[orthogonal]);\r
1683  (REWRITE_WITH `b - s:real^3 = -- u % (a - b)`);\r
1684  (ASM_REWRITE_TAC[]);\r
1685  (REWRITE_WITH `b:real^3 - (u % a + v % b) = (u + v) % b - (u % a + v % b)`);\r
1686  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1687  (VECTOR_ARITH_TAC);\r
1688  (ASM_MESON_TAC[DOT_LMUL; REAL_MUL_RZERO;DOT_SYM]);\r
1689  (REWRITE_WITH `norm (s - b:real^3) = norm (b - s)`);\r
1690  (NORM_ARITH_TAC);\r
1691  (REWRITE_WITH `b - s:real^3 = -- u % (a - b)`);\r
1692  (ASM_REWRITE_TAC[]);\r
1693  (REWRITE_WITH `b:real^3 - (u % a + v % b) = (u + v) % b - (u % a + v % b)`);\r
1694  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1695  (VECTOR_ARITH_TAC);\r
1696  (REWRITE_TAC[NORM_MUL; REAL_ABS_NEG; REAL_POW2_ABS; REAL_POW_MUL]);\r
1697 \r
1698  (REWRITE_TAC[REAL_ARITH `a * x + b <= c * x + b <=> &0 <= x * (c - a)`]);\r
1699  (STRIP_TAC);\r
1700  (REWRITE_WITH `v <= u <=> v pow 2 <= u pow 2`);\r
1701  (MATCH_MP_TAC Trigonometry2.POW2_COND);\r
1702  (ASM_REWRITE_TAC[]);\r
1703  (ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`]);\r
1704  (REWRITE_WITH `&0 <= u pow 2 - v pow 2 <=> \r
1705        &0 <= norm (a:real^3 - b) pow 2 * (u pow 2 - v pow 2)`);\r
1706  (NEW_GOAL `(!x y. &0 < x ==> (&0 <= x * y <=> &0 <= y))`);\r
1707  (MESON_TAC[REAL_LE_MUL_EQ]);\r
1708  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
1709  (FIRST_X_ASSUM MATCH_MP_TAC);\r
1710  (MATCH_MP_TAC REAL_POW_LT);\r
1711  (REWRITE_TAC[NORM_POS_LT]);\r
1712  (REWRITE_TAC[VECTOR_ARITH `(a - b:real^3) = vec 0 <=> a = b`]);\r
1713  (ASM_REWRITE_TAC[]);\r
1714  (ASM_REWRITE_TAC[]);\r
1715 \r
1716 \r
1717 (* ======================================================================== *)\r
1718 \r
1719  (ASM_CASES_TAC `&0 < norm (x:real^3 - b)`);\r
1720  (ASM_CASES_TAC `&0 < norm (x:real^3 - a)`);\r
1721 \r
1722  (REWRITE_TAC[REAL_ARITH `a >= b * c <=> c * b <= a`]);\r
1723  (REWRITE_WITH `(norm (a - b) * r) * norm (x - b) <= (x - b) dot (a - b) <=>\r
1724   (norm (a - b) * r) <= ((x - b) dot (a - b)) / norm (x - b:real^3)`);\r
1725  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
1726  (MATCH_MP_TAC REAL_LE_RDIV_EQ);\r
1727  (ASM_REWRITE_TAC[]);\r
1728 \r
1729  (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`));\r
1730 \r
1731  (EXISTS_TAC `((x - a) dot (b - a)) / norm (x - a:real^3)`);\r
1732  (STRIP_TAC);\r
1733 \r
1734  (REWRITE_WITH `norm (a - b) * r <= \r
1735                  ((x - a) dot (b - a)) / norm (x - a) <=> \r
1736                  (norm (a - b) * r)  * norm (x - a) <= \r
1737                  ((x - a) dot (b - a:real^3))`);\r
1738  (MATCH_MP_TAC REAL_LE_RDIV_EQ);\r
1739  (ASM_REWRITE_TAC[]);\r
1740  (REWRITE_WITH \r
1741   `(norm (a - b:real^3) * r) * norm (x - a) = norm (x - a) * norm (b - a) * r`);\r
1742  (REWRITE_WITH `norm (a - b) = norm (b - a:real^3)`);\r
1743  (NORM_ARITH_TAC);\r
1744  (REAL_ARITH_TAC);\r
1745  (ASM_REAL_ARITH_TAC);\r
1746 \r
1747  (NEW_GOAL `((x - a) dot (b - a)) / norm (x - a:real^3) <= \r
1748              ((x - b) dot (a - b)) / norm (x - b) <=> \r
1749              ((x - a) dot (b - a)) * norm (x - b) <= \r
1750              ((x - b) dot (a - b)) * norm (x - a)`);\r
1751  (MATCH_MP_TAC RAT_LEMMA4);\r
1752  (ASM_REWRITE_TAC[]);\r
1753  (ASM_REWRITE_TAC[]);\r
1754  (ASM_REAL_ARITH_TAC);\r
1755 \r
1756  (NEW_GOAL `x = a:real^3`);\r
1757  (ONCE_REWRITE_TAC[VECTOR_ARITH `a = b <=> a - b:real^3 = vec 0`]);\r
1758  (REWRITE_TAC [GSYM NORM_EQ_0]);\r
1759  (NEW_GOAL `&0 <= norm (x - a:real^3)`);\r
1760  (REWRITE_TAC[NORM_POS_LE]);\r
1761  (ASM_REAL_ARITH_TAC);\r
1762  (ASM_REWRITE_TAC[GSYM NORM_POW_2]);\r
1763  (ONCE_REWRITE_TAC[REAL_ARITH `a * a * b = (a pow 2) * b`]);\r
1764  (REWRITE_TAC[REAL_ARITH `a >= a * b <=> &0 <= (&1 - b) * a`]);\r
1765  (MATCH_MP_TAC REAL_LE_MUL);\r
1766  (REWRITE_TAC[REAL_LE_POW_2]);\r
1767  (ASM_REAL_ARITH_TAC);\r
1768 \r
1769  (NEW_GOAL `F`);\r
1770  (NEW_GOAL `x = b:real^3`);\r
1771  (ONCE_REWRITE_TAC[VECTOR_ARITH `a = b <=> a - b:real^3 = vec 0`]);\r
1772  (REWRITE_TAC [GSYM NORM_EQ_0]);\r
1773  (NEW_GOAL `&0 <= norm (x - b:real^3)`);\r
1774  (REWRITE_TAC[NORM_POS_LE]);\r
1775  (ASM_REAL_ARITH_TAC);\r
1776 \r
1777  (UNDISCH_TAC `x IN voronoi_closed V (a:real^3)`);\r
1778  (REWRITE_TAC[voronoi_closed;IN;IN_ELIM_THM]);\r
1779  (STRIP_TAC);\r
1780  (NEW_GOAL `dist (x,a) <= dist (x,b:real^3)`);\r
1781  (FIRST_X_ASSUM MATCH_MP_TAC);\r
1782  (ASM_SET_TAC[]);\r
1783  (UP_ASM_TAC THEN ASM_REWRITE_TAC[DIST_REFL]);\r
1784  (STRIP_TAC);\r
1785  (NEW_GOAL `a = b:real^3`);\r
1786  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
1787  (REWRITE_TAC[GSYM DIST_EQ_0]);\r
1788  (NEW_GOAL `&0 <= dist (b, a:real^3)`);\r
1789  (REWRITE_TAC[DIST_POS_LE]);\r
1790  (ASM_REAL_ARITH_TAC);\r
1791  (ASM_MESON_TAC[]);\r
1792  (ASM_MESON_TAC[])]);;\r
1793 \r
1794 (* ======================================================================= *)\r
1795 (* Lemma 32 *)\r
1796 let OMEGA_LIST_1_EXPLICIT_NEW = prove_by_refinement (\r
1797  `!a:real^3 b c d V ul.\r
1798      saturated V /\\r
1799      packing V /\\r
1800      ul IN barV V 3 /\\r
1801      ul = [a; b; c; d] /\\r
1802      hl [a;b] < sqrt (&2) \r
1803      ==> omega_list_n V ul 1 = circumcenter {a, b}`,\r
1804 [ (REPEAT STRIP_TAC);\r
1805  (REWRITE_WITH `{a,b} = set_of_list [a;(b:real^3)]`);\r
1806  (MESON_TAC[set_of_list]);\r
1807  (REWRITE_WITH `circumcenter (set_of_list [a; b:real^3]) = omega_list V [a:real^3; b]`);\r
1808  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
1809  (MATCH_MP_TAC XNHPWAB1);\r
1810  (EXISTS_TAC `1`);\r
1811  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);\r
1812  (MP_TAC (ASSUME `ul IN barV V 3`) THEN REWRITE_TAC[IN;BARV]);\r
1813 \r
1814  (REPEAT STRIP_TAC);\r
1815  (REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC 0) = 1 + 1`]);\r
1816  (NEW_GOAL `initial_sublist vl (ul:(real^3)list)`);\r
1817  (UNDISCH_TAC `initial_sublist vl [a:real^3; b]`);\r
1818  (REWRITE_TAC[INITIAL_SUBLIST] THEN STRIP_TAC);\r
1819  (EXISTS_TAC `APPEND yl [c;d:real^3]`);\r
1820  (REWRITE_TAC[APPEND_ASSOC; GSYM (ASSUME `[a:real^3; b] = APPEND vl yl`)]);\r
1821  (ASM_REWRITE_TAC[APPEND]);\r
1822  (ASM_MESON_TAC[]);\r
1823  (ASM_REWRITE_TAC[OMEGA_LIST_TRUNCATE_1])]);;\r
1824 \r
1825 (* ======================================================================= *)\r
1826 (* Lemma 33 *)\r
1827 let IN_SET_IMP_IN_CONVEX_HULL_SET = prove_by_refinement (\r
1828  `!a S:real^3->bool. a IN S ==> a IN convex hull S`,\r
1829 [(REPEAT STRIP_TAC);\r
1830  (REWRITE_TAC[SET_RULE `a IN s <=> {a} SUBSET s`]);\r
1831  (NEW_GOAL `{a} = convex hull ({a:real^3})`);\r
1832  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
1833  (SIMP_TAC[CONVEX_HULL_EQ;CONVEX_SING]);\r
1834  (ONCE_ASM_REWRITE_TAC[]);\r
1835  (MATCH_MP_TAC CONVEX_HULL_SUBSET);\r
1836  (ASM_SET_TAC[])]);;\r
1837 \r
1838 (* ======================================================================= *)\r
1839 (* Lemma 34 *)\r
1840 let CONVEX_HULL_BREAK_KY_LEMMA = prove_by_refinement (\r
1841  `!a:real^3 b c d x. between x (a,b) ==> \r
1842 (convex hull {a,b,c,d} = convex hull {a,x, c,d} UNION convex hull {x,b,c,d})`,\r
1843 \r
1844 [(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN; IN_ELIM_THM]);\r
1845  (REWRITE_TAC[SET_EQ_LEMMA]);\r
1846  (REPEAT STRIP_TAC);\r
1847  (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_4; IN_UNION;IN;IN_ELIM_THM]);\r
1848  (REPEAT STRIP_TAC);\r
1849  (ASM_CASES_TAC `u = &0`);\r
1850  (DISJ1_TAC);\r
1851  (EXISTS_TAC `u':real`);\r
1852  (EXISTS_TAC `v':real`);\r
1853  (EXISTS_TAC `w:real`);\r
1854  (EXISTS_TAC `z:real`);\r
1855  (ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]);\r
1856  (REWRITE_WITH `v = &1`);\r
1857  (ASM_REAL_ARITH_TAC);\r
1858  (VECTOR_ARITH_TAC);\r
1859  (NEW_GOAL `&0 < u `);\r
1860  (ASM_REAL_ARITH_TAC);\r
1861  (SWITCH_TAC THEN DEL_TAC);\r
1862  (ASM_CASES_TAC `v = &0`);\r
1863  (DISJ2_TAC);\r
1864  (EXISTS_TAC `u':real`);\r
1865  (EXISTS_TAC `v':real`);\r
1866  (EXISTS_TAC `w:real`);\r
1867  (EXISTS_TAC `z:real`);\r
1868  (ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]);\r
1869  (REWRITE_WITH `u = &1`);\r
1870  (ASM_REAL_ARITH_TAC);\r
1871  (VECTOR_ARITH_TAC);\r
1872  (NEW_GOAL `&0 < v `);\r
1873  (ASM_REAL_ARITH_TAC);\r
1874  (SWITCH_TAC THEN DEL_TAC);\r
1875 \r
1876 \r
1877  (ASM_CASES_TAC `&0 < u' + v'`);\r
1878  (ASM_CASES_TAC `u' / (u' + v') <= u`);\r
1879 \r
1880 (*CASE 1*)\r
1881  (DISJ2_TAC);\r
1882  (EXISTS_TAC `u' / u`);\r
1883  (EXISTS_TAC `v' - v * (u'/ u)`);\r
1884  (EXISTS_TAC `w:real`);\r
1885  (EXISTS_TAC `z:real`);\r
1886  (ASM_REWRITE_TAC[]);\r
1887  (ASM_SIMP_TAC[REAL_LE_DIV]);\r
1888  (REPEAT STRIP_TAC);\r
1889  (REWRITE_WITH `v' - v * u' / u  = (v' * u - v * u' )/ u`);\r
1890  (REWRITE_TAC[REAL_ARITH `(a - b * d) / c  = a / c - b * d / c`]);\r
1891  (AP_THM_TAC THEN AP_TERM_TAC);\r
1892  (REWRITE_WITH `v' = (v' * u) / u <=> v' * u = (v' * u)`);\r
1893  (MATCH_MP_TAC REAL_EQ_RDIV_EQ);\r
1894  (ASM_REWRITE_TAC[]);\r
1895  (REWRITE_WITH `v * u' = u' - u * u'`);\r
1896  (REWRITE_TAC[REAL_ARITH `a * b = b - c * b <=> ((c + a) - &1) * b = &0`]);\r
1897  (ASM_REWRITE_TAC[]);\r
1898  (REAL_ARITH_TAC);\r
1899  (REWRITE_TAC[REAL_ARITH `v' * u - (u' - u * u') =  u * (u' + v') - u'`]);\r
1900  (MATCH_MP_TAC REAL_LE_DIV);\r
1901  (ASM_REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);\r
1902  (NEW_GOAL `u' <= u * (u' + v') <=> u' / (u' + v') <= u`);\r
1903  (ASM_MESON_TAC[REAL_LE_LDIV_EQ]);\r
1904  (ONCE_ASM_REWRITE_TAC[]);\r
1905  (ASM_MESON_TAC[]);\r
1906 \r
1907  (REWRITE_TAC[REAL_ARITH `a + b - e + c + d = (a + b - e) + c + d`]);\r
1908  (REWRITE_WITH `u' / u + v' - v * u' / u = u' + v'`);\r
1909  (ONCE_REWRITE_TAC[REAL_ARITH `a/x + b - m*e/x = c + b <=> (a - m*e)/x = c`]);\r
1910  (NEW_GOAL `(u' - v * u') / u = u' <=> (u' - v * u') = u' * u`);\r
1911  (MATCH_MP_TAC REAL_EQ_LDIV_EQ);\r
1912  (ASM_REWRITE_TAC[]);\r
1913  (ONCE_ASM_REWRITE_TAC[]);\r
1914  (REWRITE_WITH `u' - v * u' = u' * (u + v) - v * u'`);\r
1915  (ASM_REWRITE_TAC[]);\r
1916  (REAL_ARITH_TAC);\r
1917  (ASM_REAL_ARITH_TAC);\r
1918  (ASM_REAL_ARITH_TAC);\r
1919  (REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);\r
1920  (REWRITE_TAC[VECTOR_ARITH `a + b + c + d = (x + m % y) + n % y + c + d <=>\r
1921                              (a - x) + (b - (m + n) % y) = vec 0 `]);\r
1922 \r
1923  (MATCH_MP_TAC (VECTOR_ARITH `a = vec 0 /\ b = vec 0 ==> a + b = vec 0`));\r
1924  (STRIP_TAC);\r
1925  (REWRITE_TAC[VECTOR_ARITH \r
1926   `(x % a - y % a = vec 0) <=> (x - y) % a = vec 0`; VECTOR_MUL_EQ_0]);\r
1927  (DISJ1_TAC);\r
1928  (REWRITE_TAC[REAL_ARITH `x - y / z * t = &0 <=> (y * t) / z = x`]);\r
1929  (NEW_GOAL `(u' * u) / u = u' <=> (u' * u) = u' * u`);\r
1930  (MATCH_MP_TAC REAL_EQ_LDIV_EQ);\r
1931  (ASM_REWRITE_TAC[]);\r
1932  (ONCE_ASM_REWRITE_TAC[]);\r
1933  (REFL_TAC);\r
1934 \r
1935  (REWRITE_TAC[VECTOR_ARITH \r
1936   `(x % a - y % a = vec 0) <=> (x - y) % a = vec 0`; VECTOR_MUL_EQ_0]);\r
1937  (DISJ1_TAC);\r
1938  (REAL_ARITH_TAC);\r
1939 \r
1940 (*CASE 2*)\r
1941 \r
1942 \r
1943  (NEW_GOAL `v' / (u' + v') <= v`);\r
1944  (REWRITE_WITH `v' / (u' + v') = &1 - u' /(u' + v')`);\r
1945  (REWRITE_TAC[REAL_ARITH `a / x = &1 - b / x <=> (b + a) / x = &1`]);\r
1946  (MATCH_MP_TAC REAL_DIV_REFL);\r
1947  (ASM_REAL_ARITH_TAC);\r
1948  (ASM_REAL_ARITH_TAC);\r
1949 \r
1950  (DISJ1_TAC);\r
1951  (EXISTS_TAC `u' - u * (v'/ v)`);\r
1952  (EXISTS_TAC `v' / v`);\r
1953  (EXISTS_TAC `w:real`);\r
1954  (EXISTS_TAC `z:real`);\r
1955  (ASM_REWRITE_TAC[]);\r
1956  (ASM_SIMP_TAC[REAL_LE_DIV]);\r
1957  (REPEAT STRIP_TAC);\r
1958 \r
1959  (REWRITE_WITH `u' - u * v' / v  = (u' * v - u * v' )/ v`);\r
1960  (REWRITE_TAC[REAL_ARITH `(a - b * d) / c  = a / c - b * d / c`]);\r
1961  (AP_THM_TAC THEN AP_TERM_TAC);\r
1962  (REWRITE_WITH `u' = (u' * v) / v <=> u' * v = (u' * v)`);\r
1963  (MATCH_MP_TAC REAL_EQ_RDIV_EQ);\r
1964  (ASM_REWRITE_TAC[]);\r
1965 \r
1966  (REWRITE_WITH `u * v' = v' - v * v'`);\r
1967  (REWRITE_TAC[REAL_ARITH `a * b = b - c * b <=> ((c + a) - &1) * b = &0`]);\r
1968  (ASM_REWRITE_TAC[REAL_ARITH `v + u = u + v`]);\r
1969  (ASM_REAL_ARITH_TAC);\r
1970  (REWRITE_TAC[REAL_ARITH `v' * u - (u' - u * u') =  u * (u' + v') - u'`]);\r
1971  (MATCH_MP_TAC REAL_LE_DIV);\r
1972  (ASM_REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);\r
1973 \r
1974  (NEW_GOAL `v' <= v * (v' + u') <=> v' / (v' + u') <= v`);\r
1975  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
1976  (MATCH_MP_TAC REAL_LE_LDIV_EQ);\r
1977  (ASM_REAL_ARITH_TAC);\r
1978  (ONCE_ASM_REWRITE_TAC[]);\r
1979  (ASM_MESON_TAC[REAL_ADD_SYM]);\r
1980 \r
1981  (REWRITE_TAC[REAL_ARITH `a - e + b + c + d = (a + b - e) + c + d`]);\r
1982  (REWRITE_WITH `u' + v' / v - u * v' / v = u' + v'`);\r
1983 \r
1984  (ONCE_REWRITE_TAC[REAL_ARITH `b + a/x  - m*e/x = b + c <=> (a - m*e)/x = c`]);\r
1985  (NEW_GOAL `(v' - u * v') / v = v' <=> (v' - u * v') = v' * v`);\r
1986  (MATCH_MP_TAC REAL_EQ_LDIV_EQ);\r
1987  (ASM_REWRITE_TAC[]);\r
1988  (ONCE_ASM_REWRITE_TAC[]);\r
1989  (REWRITE_WITH `v' - u * v' = v' * (u + v) - u * v'`);\r
1990  (ASM_REWRITE_TAC[]);\r
1991  (REAL_ARITH_TAC);\r
1992  (ASM_REAL_ARITH_TAC);\r
1993  (ASM_REAL_ARITH_TAC);\r
1994  (REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);\r
1995  (REWRITE_TAC[VECTOR_ARITH `a + b + c + d = (m % y) + (n % y + z) + c + d <=> (b - z) + (a - (m + n) % y) = vec 0 `]);\r
1996 \r
1997  (MATCH_MP_TAC (VECTOR_ARITH `a = vec 0 /\ b = vec 0 ==> b + a = vec 0`));\r
1998  (STRIP_TAC);\r
1999 \r
2000  (REWRITE_TAC[VECTOR_ARITH \r
2001   `(x % a - y % a = vec 0) <=> (x - y) % a = vec 0`; VECTOR_MUL_EQ_0]);\r
2002  (DISJ1_TAC);\r
2003  (REAL_ARITH_TAC);\r
2004  (REWRITE_TAC[VECTOR_ARITH \r
2005   `(x % a - y % a = vec 0) <=> (x - y) % a = vec 0`; VECTOR_MUL_EQ_0]);\r
2006  (DISJ1_TAC);\r
2007 \r
2008  (REWRITE_TAC[REAL_ARITH `x - y / z * t = &0 <=> (y * t) / z = x`]);\r
2009  (NEW_GOAL `(v' * v) / v = v' <=> (v' * v) = v' * v`);\r
2010  (MATCH_MP_TAC REAL_EQ_LDIV_EQ);\r
2011  (ASM_REWRITE_TAC[]);\r
2012  (ONCE_ASM_REWRITE_TAC[]);\r
2013  (REFL_TAC);\r
2014 \r
2015 (* CASE 3 *)\r
2016 \r
2017  (NEW_GOAL `u' + v' = &0`);\r
2018  (ASM_REAL_ARITH_TAC);\r
2019  (DISJ1_TAC);\r
2020  (EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);\r
2021  (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`);\r
2022  (NEW_GOAL `u'= &0 /\ v' = &0`);\r
2023  (ASM_REAL_ARITH_TAC);\r
2024  (UNDISCH_TAC `x' = u' % a + v' % b + w % c + z % (d:real^3)`);\r
2025  (ASM_REWRITE_TAC[VECTOR_MUL_LZERO; REAL_ARITH `&0 <= &0`]);\r
2026  (REPEAT STRIP_TAC);\r
2027  (ASM_MESON_TAC[]);\r
2028  (ASM_MESON_TAC[]);\r
2029 \r
2030 (* ================================ *)\r
2031 \r
2032  (UP_ASM_TAC THEN REWRITE_TAC[IN_UNION]);\r
2033  (REPEAT STRIP_TAC);\r
2034 \r
2035  (NEW_GOAL `convex hull {a, x, c, d} SUBSET convex hull {a, b, c, d:real^3}`);\r
2036  (NEW_GOAL `convex hull {a, b, c, d:real^3} = \r
2037              convex hull (convex hull {a, b, c, d:real^3})`);\r
2038  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
2039  (REWRITE_TAC[CONVEX_HULL_EQ; CONVEX_CONVEX_HULL]);\r
2040  (ONCE_ASM_REWRITE_TAC[]);\r
2041  (MATCH_MP_TAC CONVEX_HULL_SUBSET);\r
2042  (ONCE_REWRITE_TAC[SUBSET; IN;IN_ELIM_THM]);\r
2043  (REPEAT STRIP_TAC);\r
2044  (ASM_CASES_TAC `x'' = a:real^3`);\r
2045  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);\r
2046  (ASM_SET_TAC[]);\r
2047  (ASM_CASES_TAC `x'' = d:real^3`);\r
2048  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);\r
2049  (ASM_SET_TAC[]);\r
2050  (ASM_CASES_TAC `x'' = c:real^3`);\r
2051  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);\r
2052  (ASM_SET_TAC[]);\r
2053  (NEW_GOAL `x'' = u % a + v % (b:real^3)`);\r
2054  (ASM_SET_TAC[]);\r
2055  (ASM_REWRITE_TAC[]);\r
2056  (MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET r) ==> p IN r`));\r
2057  (EXISTS_TAC `convex hull {a, b:real^3}`);\r
2058  (STRIP_TAC);\r
2059  (ASM_REWRITE_TAC[CONVEX_HULL_2; IN; IN_ELIM_THM]);\r
2060  (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real`);\r
2061  (ASM_REWRITE_TAC[]);\r
2062  (MATCH_MP_TAC CONVEX_HULL_SUBSET);\r
2063  (SET_TAC[]);\r
2064  (ASM_SET_TAC[]);\r
2065 \r
2066 (* == *)\r
2067 \r
2068  (NEW_GOAL `convex hull {x, b, c, d} SUBSET convex hull {a, b, c, d:real^3}`);\r
2069  (NEW_GOAL `convex hull {a, b, c, d:real^3} = \r
2070              convex hull (convex hull {a, b, c, d:real^3})`);\r
2071  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
2072  (REWRITE_TAC[CONVEX_HULL_EQ; CONVEX_CONVEX_HULL]);\r
2073  (ONCE_ASM_REWRITE_TAC[]);\r
2074  (MATCH_MP_TAC CONVEX_HULL_SUBSET);\r
2075  (ONCE_REWRITE_TAC[SUBSET; IN;IN_ELIM_THM]);\r
2076  (REPEAT STRIP_TAC);\r
2077  (ASM_CASES_TAC `x'' = b:real^3`);\r
2078  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);\r
2079  (ASM_SET_TAC[]);\r
2080  (ASM_CASES_TAC `x'' = d:real^3`);\r
2081  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);\r
2082  (ASM_SET_TAC[]);\r
2083  (ASM_CASES_TAC `x'' = c:real^3`);\r
2084  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);\r
2085  (ASM_SET_TAC[]);\r
2086  (NEW_GOAL `x'' = u % a + v % (b:real^3)`);\r
2087  (ASM_SET_TAC[]);\r
2088  (ASM_REWRITE_TAC[]);\r
2089  (MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET r) ==> p IN r`));\r
2090  (EXISTS_TAC `convex hull {a, b:real^3}`);\r
2091  (STRIP_TAC);\r
2092  (ASM_REWRITE_TAC[CONVEX_HULL_2; IN; IN_ELIM_THM]);\r
2093  (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real`);\r
2094  (ASM_REWRITE_TAC[]);\r
2095  (MATCH_MP_TAC CONVEX_HULL_SUBSET);\r
2096  (SET_TAC[]);\r
2097  (ASM_SET_TAC[])]);;\r
2098 \r
2099 (* ======================================================================= *)\r
2100 (* Lemma 35 *)\r
2101 let AFF_GE_BREAK_KY_LEMMA = prove_by_refinement (\r
2102  `!a b c d (x:real^3). \r
2103     between x (c, d) /\ \r
2104     DISJOINT {a, b} {c, d} /\ \r
2105     DISJOINT {a, b} {c, x} /\ \r
2106     DISJOINT {a, b} {x, d} ==> \r
2107     aff_ge {a, b} {c, d} = aff_ge {a, b} {c, x} UNION aff_ge {a, b} {x, d}`,\r
2108 [(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; IN; IN_ELIM_THM]);\r
2109  (REPEAT STRIP_TAC);\r
2110 \r
2111  (ASM_SIMP_TAC[AFF_GE_2_2]);\r
2112  (REWRITE_TAC[SET_EQ_LEMMA; IN_UNION; IN; IN_ELIM_THM]);\r
2113  (REPEAT STRIP_TAC);\r
2114 \r
2115   (* Break to 3 subgoal *)\r
2116 \r
2117  (ASM_CASES_TAC `u = &0`);\r
2118  (REWRITE_WITH `v = &1`);\r
2119  (ASM_REAL_ARITH_TAC);\r
2120  (ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID; VECTOR_MUL_LID]);\r
2121  (DISJ1_TAC);\r
2122 \r
2123  (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`);\r
2124  (EXISTS_TAC `t3:real` THEN EXISTS_TAC `t4:real`);\r
2125  (ASM_REWRITE_TAC[]);\r
2126  (NEW_GOAL `&0 <u `);\r
2127  (ASM_REAL_ARITH_TAC);\r
2128  (ASM_CASES_TAC `v = &0`);\r
2129  (REWRITE_WITH `u = &1`);\r
2130  (ASM_REAL_ARITH_TAC);\r
2131  (ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID; VECTOR_MUL_LID]);\r
2132  (DISJ2_TAC);\r
2133  (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`);\r
2134  (EXISTS_TAC `t3:real` THEN EXISTS_TAC `t4:real`);\r
2135  (ASM_REWRITE_TAC[]);\r
2136  (NEW_GOAL `&0 < v `);\r
2137  (ASM_REAL_ARITH_TAC);\r
2138 \r
2139  (ASM_CASES_TAC `&0 < t3 + t4`);\r
2140  (ASM_CASES_TAC `v * (t3 + t4) >= t4`);\r
2141  (DISJ1_TAC);\r
2142  (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`);\r
2143  (EXISTS_TAC `t3 - u * t4 / v` THEN EXISTS_TAC `t4 / v`);\r
2144  (REPEAT STRIP_TAC);\r
2145  (REWRITE_TAC[REAL_ARITH `&0 <= a - b * c / d <=> (b * c) / d <= a `]);\r
2146  (REWRITE_WITH `(u * t4) / v <= t3 <=> (u * t4) <= t3 * v`);\r
2147  (MATCH_MP_TAC REAL_LE_LDIV_EQ);\r
2148  (ASM_REWRITE_TAC[]);\r
2149  (REWRITE_WITH `u * t4 <= t3 * v <=> v * (t3 + t4) >= t4`);\r
2150  (REWRITE_WITH `v * (t3 + t4) >= t4 <=> v * (t3 + t4) >= t4 * (u + v)`);\r
2151  (ASM_REWRITE_TAC[REAL_MUL_RID]);\r
2152  (REAL_ARITH_TAC);\r
2153  (ASM_REWRITE_TAC[]);\r
2154  (MATCH_MP_TAC REAL_LE_DIV);\r
2155  (ASM_REAL_ARITH_TAC);\r
2156  (REWRITE_WITH `t1 + t2 + t3 - u * t4 / v + t4 / v = t1 + t2 + t3 + t4`);\r
2157  (REPEAT AP_TERM_TAC);\r
2158  (REWRITE_TAC[REAL_ARITH \r
2159   `t3 - u * t4 / v + t4 / v = t3 + t4 <=> (t4 - t4 * u) / v = t4`]);\r
2160 \r
2161  (REWRITE_WITH `(t4 - t4 * u) / v = t4 <=> (t4 - t4 * u) = t4 * v`);\r
2162  (MATCH_MP_TAC REAL_EQ_LDIV_EQ);\r
2163  (ASM_REAL_ARITH_TAC);\r
2164  (REWRITE_WITH `(t4 - t4 * u) = t4 * (u + v) - t4 * u`);\r
2165  (ASM_REWRITE_TAC[REAL_MUL_RID]);\r
2166  (REAL_ARITH_TAC);\r
2167  (ASM_REWRITE_TAC[]);\r
2168 \r
2169  (REWRITE_WITH \r
2170  `t1 % a + t2 % b + (t3 - u * t4 / v) % c + t4 / v % (u % c + v % d) = \r
2171   t1 % a + t2 % b + t3 % c + t4 % (d:real^3)`);\r
2172  (REPEAT AP_TERM_TAC);\r
2173 \r
2174  (REWRITE_TAC[VECTOR_SUB_RDISTRIB; VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]);\r
2175  (REWRITE_TAC[VECTOR_ARITH \r
2176   `(x % c - y % c + t % c + z % d = x % c + n % d) <=> \r
2177    (t - y) % c + (z - n) %d = vec 0`]);\r
2178  (REWRITE_WITH `t4 / v * u - u * t4 / v = &0`);\r
2179  (REAL_ARITH_TAC);\r
2180  (REWRITE_WITH `t4 / v * v - t4 = &0`);\r
2181  (REWRITE_TAC[REAL_ARITH `a / b * c - d = &0 <=> (a * c) / b = d`]);\r
2182  (REWRITE_WITH `(t4 * v) / v = t4 <=> (t4 * v) = t4 * v`);\r
2183  (MATCH_MP_TAC REAL_EQ_LDIV_EQ);\r
2184  (ASM_REWRITE_TAC[]);\r
2185  (VECTOR_ARITH_TAC);\r
2186  (ASM_REWRITE_TAC[]);\r
2187 \r
2188  (ASM_CASES_TAC `(u * (t3 + t4) >= t3)`);\r
2189  (DISJ2_TAC);\r
2190  (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`);\r
2191  (EXISTS_TAC `t3 / u` THEN EXISTS_TAC `t4 - v * t3 / u`);\r
2192  (REPEAT STRIP_TAC);\r
2193  (MATCH_MP_TAC REAL_LE_DIV);\r
2194  (ASM_REAL_ARITH_TAC);\r
2195 \r
2196  (REWRITE_TAC[REAL_ARITH `&0 <= a - b * c / d <=> (b * c) / d <= a `]);\r
2197  (REWRITE_WITH `(v * t3) / u <= t4 <=> (v * t3) <= t4 * u`);\r
2198  (MATCH_MP_TAC REAL_LE_LDIV_EQ);\r
2199  (ASM_REWRITE_TAC[]);\r
2200  (REWRITE_WITH `v * t3 <= t4 * u <=> u * (t3 + t4) >= t3`);\r
2201  (REWRITE_WITH `u * (t3 + t4) >= t3 <=> u * (t3 + t4) >= t3 * (u + v)`);\r
2202  (ASM_REWRITE_TAC[REAL_MUL_RID]);\r
2203  (REAL_ARITH_TAC);\r
2204  (ASM_REWRITE_TAC[]);\r
2205 \r
2206  (REWRITE_WITH `t1 + t2 + t3 / u + t4 - v * t3 / u = t1 + t2 + t3 + t4`);\r
2207  (REPEAT AP_TERM_TAC);\r
2208  (REWRITE_TAC[REAL_ARITH \r
2209   `t3 / u + t4 - v * t3 / u = t3 + t4 <=> (t3 - t3 * v) / u = t3`]);\r
2210 \r
2211  (REWRITE_WITH `(t3 - t3 * v) / u = t3 <=> (t3 - t3 * v) = t3 * u`);\r
2212  (MATCH_MP_TAC REAL_EQ_LDIV_EQ);\r
2213  (ASM_REAL_ARITH_TAC);\r
2214  (REWRITE_WITH `(t3 - t3 * v) = t3 * (u + v) - t3 * v`);\r
2215  (ASM_REWRITE_TAC[REAL_MUL_RID]);\r
2216  (REAL_ARITH_TAC);\r
2217  (ASM_REWRITE_TAC[]);\r
2218 \r
2219  (REWRITE_WITH \r
2220  `t1 % a + t2 % b + t3 / u % (u % c + v % d) + (t4 - v * t3 / u) % d = \r
2221   t1 % a + t2 % b + t3 % c + t4 % (d:real^3)`);\r
2222  (REPEAT AP_TERM_TAC);\r
2223 \r
2224  (REWRITE_TAC[VECTOR_SUB_RDISTRIB; VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]);\r
2225  (REWRITE_TAC[VECTOR_ARITH \r
2226   `(x % c + y % d) + a - z % d = t % c + a <=> \r
2227    (x - t) % c + (y - z) %d = vec 0`]);\r
2228  (REWRITE_WITH `t3 / u * v - v * t3 / u = &0`);\r
2229  (REAL_ARITH_TAC);\r
2230  (REWRITE_WITH `t3 / u * u - t3 = &0`);\r
2231  (REWRITE_TAC[REAL_ARITH `a / b * c - d = &0 <=> (a * c) / b = d`]);\r
2232  (REWRITE_WITH `(t3 * u) / u = t3 <=> (t3 * u) = t3 * u`);\r
2233  (MATCH_MP_TAC REAL_EQ_LDIV_EQ);\r
2234  (ASM_REWRITE_TAC[]);\r
2235  (VECTOR_ARITH_TAC);\r
2236  (ASM_REWRITE_TAC[]);\r
2237  (NEW_GOAL `F`);\r
2238  (NEW_GOAL `v * (t3 + t4) < t4 /\ u * (t3 + t4) < t3`);\r
2239  (ASM_REAL_ARITH_TAC);\r
2240  (NEW_GOAL `(u + v) * (t3 + t4) < (t3 + t4)`);\r
2241  (ASM_REAL_ARITH_TAC);\r
2242  (UP_ASM_TAC THEN ASM_REWRITE_TAC[REAL_MUL_LID]);\r
2243  (REAL_ARITH_TAC);\r
2244  (UP_ASM_TAC THEN MESON_TAC[]);\r
2245  (NEW_GOAL `t3 = &0 /\ t4 = &0`);\r
2246  (ASM_REAL_ARITH_TAC);\r
2247  (DISJ1_TAC);\r
2248  (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`);\r
2249  (EXISTS_TAC `t3:real` THEN EXISTS_TAC `t4:real`);\r
2250  (ASM_REWRITE_TAC[VECTOR_MUL_LZERO]);\r
2251 (* finish the first subgoal *)\r
2252 \r
2253  (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`);\r
2254  (EXISTS_TAC `t3 + t4 * u` THEN EXISTS_TAC `t4 * v`);\r
2255  (REPEAT STRIP_TAC);\r
2256  (MATCH_MP_TAC REAL_LE_ADD);\r
2257  (ASM_SIMP_TAC[REAL_LE_MUL]);\r
2258  (ASM_SIMP_TAC[REAL_LE_MUL]);\r
2259  (REWRITE_WITH `t1 + t2 + (t3 + t4 * u) + t4 * v = \r
2260                  t1 + t2 + t3 + t4 * (u + v)`);\r
2261  (REAL_ARITH_TAC);\r
2262  (ASM_REWRITE_TAC[REAL_MUL_RID]);\r
2263  (REWRITE_WITH `t1 % a + t2 % b + (t3 + t4 * u) % c + (t4 * v) % d =\r
2264                  t1 % a + t2 % b + t3 % c + t4 % (u % c + v % (d:real^3))`);\r
2265  (VECTOR_ARITH_TAC);\r
2266  (ASM_REWRITE_TAC[]);\r
2267 \r
2268  (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`);\r
2269  (EXISTS_TAC `t3 * u` THEN EXISTS_TAC `t4 + t3 * v`);\r
2270  (REPEAT STRIP_TAC);\r
2271  (ASM_SIMP_TAC[REAL_LE_MUL]);\r
2272  (MATCH_MP_TAC REAL_LE_ADD);\r
2273  (ASM_SIMP_TAC[REAL_LE_MUL]);\r
2274  (REWRITE_WITH `t1 + t2 + t3 * u + t4 + t3 * v = \r
2275                  t1 + t2 + t3 * (u + v) + t4`);\r
2276  (REAL_ARITH_TAC);\r
2277  (ASM_REWRITE_TAC[REAL_MUL_RID]);\r
2278  (REWRITE_WITH `t1 % a + t2 % b + (t3 * u) % c + (t4 + t3 * v) % d =\r
2279                  t1 % a + t2 % b + t3 % (u % c + v % d) + t4 % (d:real^3)`);\r
2280  (VECTOR_ARITH_TAC);\r
2281  (ASM_REWRITE_TAC[])]);;\r
2282 \r
2283 (* ======================================================================= *)\r
2284 (* Lemma 36 *)\r
2285 let CONVEX_HULL_4_SUBSET_AFF_GE_2_2 = prove_by_refinement (\r
2286  `!a b c d:real^3. \r
2287   convex hull ({a, b, c, d}) SUBSET aff_ge {a, b} {c, d}`,\r
2288 [(REPEAT STRIP_TAC);\r
2289  (ASM_CASES_TAC `DISJOINT {a, b} {c, d:real^3}`);\r
2290  (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; CONVEX_HULL_4]);\r
2291  (REPEAT STRIP_TAC);\r
2292  (ASM_SIMP_TAC[AFF_GE_2_2]);\r
2293  (REWRITE_TAC[IN_ELIM_THM]);\r
2294  (EXISTS_TAC `u:real`);\r
2295  (EXISTS_TAC `v:real`);\r
2296  (EXISTS_TAC `w:real`);\r
2297  (EXISTS_TAC `z:real`);\r
2298  (ASM_REWRITE_TAC[]);\r
2299 \r
2300 (* asm cases 1 *)\r
2301  (ASM_CASES_TAC `c = a:real^3`);\r
2302  (ASM_REWRITE_TAC[]);\r
2303  (ONCE_REWRITE_TAC[AFF_GE_DISJOINT_DIFF]);\r
2304  (ASM_CASES_TAC `b = a:real^3 \/ b = d`);\r
2305  (REWRITE_WITH `{a, b:real^3} DIFF {a, d:real^3} = {}`);\r
2306  (ASM_SET_TAC[]);\r
2307  (ONCE_REWRITE_TAC[CONVEX_HULL_AFF_GE]);\r
2308  (REWRITE_WITH `{a, b, a , d:real^3} = {a, d}`);\r
2309  (TRUONG_SET_TAC[]);\r
2310  (TRUONG_SET_TAC[]);\r
2311  (REWRITE_WITH `{a, b:real^3} DIFF {a, d:real^3} = {b}`);\r
2312  (TRUONG_SET_TAC[]);\r
2313  (NEW_GOAL `DISJOINT {b:real^3} {a, d}`);\r
2314  (TRUONG_SET_TAC[]);\r
2315  (ASM_SIMP_TAC[Fan.AFF_GE_1_2]); \r
2316  (REWRITE_WITH `{a, b, a , d:real^3} = {a, b, d}`);\r
2317  (TRUONG_SET_TAC[]);\r
2318  (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; CONVEX_HULL_3]);\r
2319  (REPEAT STRIP_TAC);\r
2320  (EXISTS_TAC `v:real` THEN EXISTS_TAC `u:real` THEN EXISTS_TAC `w:real`); \r
2321  (ASM_REWRITE_TAC[REAL_ARITH `a + b + c = b + a + c`]);\r
2322  (VECTOR_ARITH_TAC);\r
2323 \r
2324 (* asm cases 2 *)\r
2325  (ASM_CASES_TAC `c = b:real^3`);\r
2326  (ASM_REWRITE_TAC[]);\r
2327  (ONCE_REWRITE_TAC[AFF_GE_DISJOINT_DIFF]);\r
2328  (ASM_CASES_TAC `a = b:real^3 \/ a = d`);\r
2329  (REWRITE_WITH `{a, b:real^3} DIFF {b, d:real^3} = {}`);\r
2330  (ASM_SET_TAC[]);\r
2331  (ONCE_REWRITE_TAC[CONVEX_HULL_AFF_GE]);\r
2332  (REWRITE_WITH `{a, b, b , d:real^3} = {b, d}`);\r
2333  (TRUONG_SET_TAC[]);\r
2334  (TRUONG_SET_TAC[]);\r
2335  (REWRITE_WITH `{a, b:real^3} DIFF {b, d:real^3} = {a}`);\r
2336  (TRUONG_SET_TAC[]);\r
2337  (NEW_GOAL `DISJOINT {a:real^3} {b, d}`);\r
2338  (TRUONG_SET_TAC[]);\r
2339  (ASM_SIMP_TAC[Fan.AFF_GE_1_2]); \r
2340  (REWRITE_WITH `{a, b, b , d:real^3} = {a, b, d}`);\r
2341  (TRUONG_SET_TAC[]);\r
2342  (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; CONVEX_HULL_3]);\r
2343  (REPEAT STRIP_TAC);\r
2344  (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN EXISTS_TAC `w:real`); \r
2345  (ASM_REWRITE_TAC[]);\r
2346 \r
2347 (* asm case 3 *)\r
2348  (ASM_CASES_TAC `d = a:real^3`);\r
2349  (ASM_REWRITE_TAC[]);\r
2350  (ONCE_REWRITE_TAC[AFF_GE_DISJOINT_DIFF]);\r
2351  (ASM_CASES_TAC `b = a:real^3 \/ b = c`);\r
2352  (REWRITE_WITH `{a, b:real^3} DIFF {c, a:real^3} = {}`);\r
2353  (ASM_SET_TAC[]);\r
2354  (ONCE_REWRITE_TAC[CONVEX_HULL_AFF_GE]);\r
2355  (REWRITE_WITH `{a, b, c , a:real^3} = {a, c}`);\r
2356  (TRUONG_SET_TAC[]);\r
2357  (REWRITE_TAC[SET_RULE `{x, y} = {y, x}`]);\r
2358  (TRUONG_SET_TAC[]);\r
2359 \r
2360  (REWRITE_WITH `{a, b:real^3} DIFF {c, a:real^3} = {b}`);\r
2361  (TRUONG_SET_TAC[]);\r
2362  (NEW_GOAL `DISJOINT {b:real^3} {c, a}`);\r
2363  (TRUONG_SET_TAC[]);\r
2364  (ASM_SIMP_TAC[Fan.AFF_GE_1_2]); \r
2365  (REWRITE_WITH `{a, b, c, a:real^3} = {a, b, c}`);\r
2366  (TRUONG_SET_TAC[]);\r
2367  (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; CONVEX_HULL_3]);\r
2368  (REPEAT STRIP_TAC);\r
2369  (EXISTS_TAC `v:real` THEN EXISTS_TAC `w:real` THEN EXISTS_TAC `u:real`); \r
2370  (ASM_REWRITE_TAC[REAL_ARITH `v + w + u = u + v + w`]);\r
2371  (VECTOR_ARITH_TAC);\r
2372 \r
2373 (* last case *)\r
2374  (NEW_GOAL `d = b:real^3`);\r
2375  (ASM_SET_TAC[]);\r
2376  (ASM_REWRITE_TAC[]);\r
2377  (ONCE_REWRITE_TAC[AFF_GE_DISJOINT_DIFF]);\r
2378  (ASM_CASES_TAC `a = b:real^3 \/ a = c`);\r
2379  (REWRITE_WITH `{a, b:real^3} DIFF {c, b:real^3} = {}`);\r
2380  (ASM_SET_TAC[]);\r
2381  (ONCE_REWRITE_TAC[CONVEX_HULL_AFF_GE]);\r
2382  (REWRITE_WITH `{a, b, c , b:real^3} = {c, b}`);\r
2383  (TRUONG_SET_TAC[]);\r
2384  (TRUONG_SET_TAC[]);\r
2385  (REWRITE_WITH `{a, b:real^3} DIFF {c, b:real^3} = {a}`);\r
2386  (TRUONG_SET_TAC[]);\r
2387  (NEW_GOAL `DISJOINT {a:real^3} {c, b}`);\r
2388  (TRUONG_SET_TAC[]);\r
2389  (ASM_SIMP_TAC[Fan.AFF_GE_1_2]); \r
2390  (REWRITE_WITH `{a, b, c , b:real^3} = {a, b, c}`);\r
2391  (TRUONG_SET_TAC[]);\r
2392  (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; CONVEX_HULL_3]);\r
2393  (REPEAT STRIP_TAC);\r
2394  (EXISTS_TAC `u:real` THEN EXISTS_TAC `w:real` THEN EXISTS_TAC `v:real`); \r
2395  (ASM_REWRITE_TAC[REAL_ARITH `a + b + c = a + c + b`]);\r
2396  (VECTOR_ARITH_TAC)]);;\r
2397 \r
2398 (* ======================================================================= *)\r
2399 (* Lemma 37 *)\r
2400 let AFF_INDEPENDENT_SET_OF_LIST_BARV = prove_by_refinement (\r
2401  `!V ul:(real^3)list.packing V /\ saturated V /\ barV V 3 ul\r
2402            ==> ~ affine_dependent (set_of_list ul)`,\r
2403 [(REPEAT STRIP_TAC);\r
2404  (SUBGOAL_THEN `? u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]` CHOOSE_TAC);\r
2405  (MP_TAC (ASSUME `barV V 3 ul`));\r
2406  (REWRITE_TAC[BARV_3_EXPLICIT]);\r
2407  (FIRST_X_ASSUM CHOOSE_TAC);\r
2408  (FIRST_X_ASSUM CHOOSE_TAC);\r
2409  (FIRST_X_ASSUM CHOOSE_TAC);\r
2410 \r
2411  (NEW_GOAL `barV V 3 (ul:(real^3)list)`);\r
2412  (ASM_REWRITE_TAC[]);\r
2413  (NEW_GOAL `~affine_dependent {u0,u1,u2,u3:real^3}`);\r
2414  (REWRITE_TAC[AFFINE_INDEPENDENT_IFF_CARD]);\r
2415  (STRIP_TAC);\r
2416  (REWRITE_TAC[Geomdetail.FINITE6]);\r
2417  (NEW_GOAL `aff_dim {u0, u1, u2, u3:real^3} = &3`);\r
2418  (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`);\r
2419  (ASM_REWRITE_TAC[set_of_list]);\r
2420  (MATCH_MP_TAC Rogers.MHFTTZN1);\r
2421  (EXISTS_TAC `V:real^3->bool`);\r
2422  (ASM_REWRITE_TAC[]);\r
2423  (ASM_REWRITE_TAC[]);\r
2424  (ONCE_REWRITE_TAC[ARITH_RULE \r
2425    `&3 = &(CARD {u0, u1, u2, u3:real^3}) - (&1):int \r
2426     <=> &(CARD {u0, u1, u2, u3:real^3}) = (&4):int`]);\r
2427  (ONCE_REWRITE_TAC[INT_OF_NUM_EQ]);\r
2428  (REWRITE_TAC[Geomdetail.CARD4]);\r
2429  (REPEAT STRIP_TAC);\r
2430 \r
2431  (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);\r
2432  (REWRITE_WITH `{u0, u1, u2, u3} = {u1, u2, u3:real^3}`);\r
2433  (ASM_SET_TAC[]);\r
2434  (REWRITE_TAC[Geomdetail.CARD3]);\r
2435  (NEW_GOAL `aff_dim {u0, u1, u2, u3} <= &(CARD {u0, u1, u2, u3:real^3}) - (&1):int`);\r
2436  (MATCH_MP_TAC AFF_DIM_LE_CARD);\r
2437  (REWRITE_TAC[Geomdetail.FINITE6]);\r
2438  (NEW_GOAL `(&4):int <= &(CARD {u0, u1, u2, u3:real^3})`);\r
2439  (ONCE_REWRITE_TAC[ARITH_RULE  \r
2440    `(&4):int <= &(CARD {u0, u1, u2, u3:real^3}) <=>\r
2441     &3 <= &(CARD {u0, u1, u2, u3:real^3}) - (&1):int`]);\r
2442  (ASM_MESON_TAC[]);\r
2443  (NEW_GOAL `&(CARD {u0, u1, u2, u3:real^3}) <= (&4):int`);\r
2444  (ONCE_REWRITE_TAC[INT_OF_NUM_LE]);\r
2445  (REWRITE_TAC[Geomdetail.CARD4]);\r
2446  (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`);\r
2447  (ONCE_REWRITE_TAC[GSYM INT_OF_NUM_EQ]);\r
2448  (ASM_ARITH_TAC);\r
2449  (ASM_ARITH_TAC);\r
2450 \r
2451  (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);\r
2452  (REWRITE_WITH `{u0, u1, u2, u3} = {u0, u2, u3:real^3}`);\r
2453  (ASM_SET_TAC[]);\r
2454  (REWRITE_TAC[Geomdetail.CARD3]);\r
2455  (NEW_GOAL `aff_dim {u0, u1, u2, u3} <= &(CARD {u0, u1, u2, u3:real^3}) - (&1):int`);\r
2456  (MATCH_MP_TAC AFF_DIM_LE_CARD);\r
2457  (REWRITE_TAC[Geomdetail.FINITE6]);\r
2458  (NEW_GOAL `(&4):int <= &(CARD {u0, u1, u2, u3:real^3})`);\r
2459  (ONCE_REWRITE_TAC[ARITH_RULE  \r
2460    `(&4):int <= &(CARD {u0, u1, u2, u3:real^3}) <=>\r
2461     &3 <= &(CARD {u0, u1, u2, u3:real^3}) - (&1):int`]);\r
2462  (ASM_MESON_TAC[]);\r
2463  (NEW_GOAL `&(CARD {u0, u1, u2, u3:real^3}) <= (&4):int`);\r
2464  (ONCE_REWRITE_TAC[INT_OF_NUM_LE]);\r
2465  (REWRITE_TAC[Geomdetail.CARD4]);\r
2466  (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`);\r
2467  (ONCE_REWRITE_TAC[GSYM INT_OF_NUM_EQ]);\r
2468  (ASM_ARITH_TAC);\r
2469  (ASM_ARITH_TAC);\r
2470 \r
2471  (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);\r
2472  (REWRITE_WITH `{u0, u1, u2, u3} = {u1, u0, u3:real^3}`);\r
2473  (ASM_SET_TAC[]);\r
2474  (REWRITE_TAC[Geomdetail.CARD3]);\r
2475  (NEW_GOAL `aff_dim {u0, u1, u2, u3} <= &(CARD {u0, u1, u2, u3:real^3}) - (&1):int`);\r
2476  (MATCH_MP_TAC AFF_DIM_LE_CARD);\r
2477  (REWRITE_TAC[Geomdetail.FINITE6]);\r
2478  (NEW_GOAL `(&4):int <= &(CARD {u0, u1, u2, u3:real^3})`);\r
2479  (ONCE_REWRITE_TAC[ARITH_RULE  \r
2480    `(&4):int <= &(CARD {u0, u1, u2, u3:real^3}) <=>\r
2481     &3 <= &(CARD {u0, u1, u2, u3:real^3}) - (&1):int`]);\r
2482  (ASM_MESON_TAC[]);\r
2483  (NEW_GOAL `&(CARD {u0, u1, u2, u3:real^3}) <= (&4):int`);\r
2484  (ONCE_REWRITE_TAC[INT_OF_NUM_LE]);\r
2485  (REWRITE_TAC[Geomdetail.CARD4]);\r
2486  (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`);\r
2487  (ONCE_REWRITE_TAC[GSYM INT_OF_NUM_EQ]);\r
2488  (ASM_ARITH_TAC);\r
2489  (ASM_ARITH_TAC);\r
2490 \r
2491  (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);\r
2492  (REWRITE_WITH `{u0, u1, u2, u3} = {u0, u2, u3:real^3}`);\r
2493  (ASM_SET_TAC[]);\r
2494  (REWRITE_TAC[Geomdetail.CARD3]);\r
2495  (NEW_GOAL `aff_dim {u0, u1, u2, u3} <= &(CARD {u0, u1, u2, u3:real^3}) - (&1):int`);\r
2496  (MATCH_MP_TAC AFF_DIM_LE_CARD);\r
2497  (REWRITE_TAC[Geomdetail.FINITE6]);\r
2498  (NEW_GOAL `(&4):int <= &(CARD {u0, u1, u2, u3:real^3})`);\r
2499  (ONCE_REWRITE_TAC[ARITH_RULE  \r
2500    `(&4):int <= &(CARD {u0, u1, u2, u3:real^3}) <=>\r
2501     &3 <= &(CARD {u0, u1, u2, u3:real^3}) - (&1):int`]);\r
2502  (ASM_MESON_TAC[]);\r
2503  (NEW_GOAL `&(CARD {u0, u1, u2, u3:real^3}) <= (&4):int`);\r
2504  (ONCE_REWRITE_TAC[INT_OF_NUM_LE]);\r
2505  (REWRITE_TAC[Geomdetail.CARD4]);\r
2506  (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`);\r
2507  (ONCE_REWRITE_TAC[GSYM INT_OF_NUM_EQ]);\r
2508  (ASM_ARITH_TAC);\r
2509  (ASM_ARITH_TAC);\r
2510  (ASM_MESON_TAC[set_of_list])]);;\r
2511 \r
2512 (* ======================================================================= *)\r
2513 (* Lemma 38 *)\r
2514 let VORONOI_LIST_3_SINGLETON_EXPLICIT = prove_by_refinement (\r
2515  `!V ul.\r
2516       packing V /\ saturated V /\ barV V 3 ul\r
2517       ==> (?a. voronoi_list V ul = {a} /\ \r
2518                a = circumcenter (set_of_list ul) /\\r
2519                hl ul = dist (HD ul, a))`,\r
2520 [(REPEAT STRIP_TAC);\r
2521  (SUBGOAL_THEN `? u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]` CHOOSE_TAC);\r
2522  (MP_TAC (ASSUME `barV V 3 ul`));\r
2523  (REWRITE_TAC[BARV_3_EXPLICIT]);\r
2524  (FIRST_X_ASSUM CHOOSE_TAC);\r
2525  (FIRST_X_ASSUM CHOOSE_TAC);\r
2526  (FIRST_X_ASSUM CHOOSE_TAC);\r
2527 \r
2528  (NEW_GOAL `~affine_dependent {u0,u1,u2,u3:real^3}`);\r
2529  (ASM_MESON_TAC[set_of_list; AFF_INDEPENDENT_SET_OF_LIST_BARV]);\r
2530 \r
2531  (NEW_GOAL `barV V 3 ul`);\r
2532  (ASM_REWRITE_TAC[]);\r
2533  (UP_ASM_TAC THEN REWRITE_TAC[BARV; VORONOI_NONDG]);\r
2534  (REPEAT STRIP_TAC);\r
2535 \r
2536  (NEW_GOAL `initial_sublist ul (ul:(real^3)list) /\ 0 < LENGTH ul`);\r
2537  (ASM_REWRITE_TAC[INITIAL_SUBLIST; LENGTH; \r
2538    ARITH_RULE `0 < 3 + 1 /\ 0 < SUC (SUC (SUC (SUC 0)))`]);\r
2539  (EXISTS_TAC `[]:(real^3)list`);\r
2540  (REWRITE_TAC[APPEND]);\r
2541  (NEW_GOAL `aff_dim (voronoi_list V (ul:(real^3)list)) + &(LENGTH ul) = &4`);\r
2542  (ASM_SIMP_TAC[]);\r
2543  (UP_ASM_TAC THEN ASM_REWRITE_TAC[LENGTH; ARITH_RULE `3 + 1 = 4`]);\r
2544  (DISCH_TAC);\r
2545  (NEW_GOAL `aff_dim (voronoi_list V [u0; u1; u2; u3:real^3]) = &0`);\r
2546  (ASM_ARITH_TAC);\r
2547  (UP_ASM_TAC THEN REWRITE_TAC[AFF_DIM_EQ_0]);\r
2548  (REPEAT STRIP_TAC);\r
2549 \r
2550  (EXISTS_TAC `a:real^3`);\r
2551 \r
2552  (NEW_GOAL `a = circumcenter (set_of_list [u0; u1; u2; u3:real^3])`);\r
2553  (REWRITE_TAC[set_of_list]);\r
2554  (NEW_GOAL `!p. p IN affine hull {u0, u1, u2, u3:real^3} /\ \r
2555                 (?c. !w. w IN {u0, u1, u2, u3} ==> dist (p,w) = c)\r
2556                   ==> p = circumcenter {u0, u1, u2, u3}`);\r
2557  (MATCH_MP_TAC Rogers.OAPVION3);\r
2558  (ASM_REWRITE_TAC[]);\r
2559 \r
2560  (FIRST_X_ASSUM MATCH_MP_TAC);\r
2561  (NEW_GOAL `a IN voronoi_list V [u0; u1; u2; u3:real^3]`);\r
2562  (UP_ASM_TAC THEN TRUONG_SET_TAC[]);\r
2563  (NEW_GOAL `affine hull {u0, u1, u2, u3:real^3} = (:real^3)`);\r
2564  (ONCE_ASM_REWRITE_TAC[GSYM AFF_DIM_EQ_FULL]);\r
2565  (REWRITE_TAC[DIMINDEX_3]);\r
2566  (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`);\r
2567  (ASM_REWRITE_TAC[set_of_list]);\r
2568  (MATCH_MP_TAC Rogers.MHFTTZN1);\r
2569  (EXISTS_TAC `V:real^3->bool`);\r
2570  (ASM_REWRITE_TAC[]);\r
2571  (ASM_REWRITE_TAC[]);\r
2572  (REWRITE_TAC[IN_UNIV]);\r
2573  (EXISTS_TAC `dist (a,u0:real^3)`);\r
2574  (UNDISCH_TAC `a IN voronoi_list V [u0; u1; u2; u3:real^3]`);\r
2575  (REWRITE_TAC[VORONOI_LIST;VORONOI_SET; set_of_list; \r
2576                IN_INTERS; voronoi_closed]);\r
2577  (REPEAT STRIP_TAC);\r
2578  (SWITCH_TAC);\r
2579 \r
2580  (NEW_GOAL `a IN {x | !w. V w ==> dist (x,u0) <= dist (x,w:real^3)}`);\r
2581  (FIRST_X_ASSUM MATCH_MP_TAC);\r
2582  (REWRITE_TAC[IN; IN_ELIM_THM]);\r
2583  (EXISTS_TAC `u0:real^3` THEN REWRITE_TAC[]);\r
2584  (TRUONG_SET_TAC[]);\r
2585 \r
2586  (NEW_GOAL `a IN {x | !w. V w ==> dist (x,u1) <= dist (x,w:real^3)}`);\r
2587  (FIRST_X_ASSUM MATCH_MP_TAC);\r
2588  (REWRITE_TAC[IN; IN_ELIM_THM]);\r
2589  (EXISTS_TAC `u1:real^3` THEN REWRITE_TAC[]);\r
2590  (TRUONG_SET_TAC[]);\r
2591 \r
2592  (NEW_GOAL `a IN {x | !w. V w ==> dist (x,u2) <= dist (x,w:real^3)}`);\r
2593  (FIRST_X_ASSUM MATCH_MP_TAC);\r
2594  (REWRITE_TAC[IN; IN_ELIM_THM]);\r
2595  (EXISTS_TAC `u2:real^3` THEN REWRITE_TAC[]);\r
2596  (TRUONG_SET_TAC[]);\r
2597 \r
2598  (NEW_GOAL `a IN {x | !w. V w ==> dist (x,u3) <= dist (x,w:real^3)}`);\r
2599  (FIRST_X_ASSUM MATCH_MP_TAC);\r
2600  (REWRITE_TAC[IN; IN_ELIM_THM]);\r
2601  (EXISTS_TAC `u3:real^3` THEN REWRITE_TAC[]);\r
2602  (TRUONG_SET_TAC[]);\r
2603 \r
2604  (REPLICATE_TAC 4 UP_ASM_TAC THEN REWRITE_TAC[IN;IN_ELIM_THM]);\r
2605  (REPEAT STRIP_TAC);\r
2606  (NEW_GOAL `u0 IN V /\ u1 IN V /\ u2 IN V /\ (u3:real^3) IN V`);\r
2607  (UNDISCH_TAC `barV V 3 (ul:(real^3)list)`);\r
2608  (REWRITE_TAC[BARV]);\r
2609  (DISCH_TAC);\r
2610  (NEW_GOAL `initial_sublist [u0;u1;u2;u3] ul /\                 \r
2611              0 < LENGTH [u0;u1;u2;u3:real^3]`);\r
2612  (REWRITE_TAC[LENGTH; INITIAL_SUBLIST]);\r
2613  (STRIP_TAC);\r
2614  (EXISTS_TAC `[]:(real^3)list`);\r
2615  (ASM_REWRITE_TAC[APPEND]);\r
2616  (ARITH_TAC);\r
2617 \r
2618  (NEW_GOAL `voronoi_nondg V [u0;u1;u2;u3:real^3]`);\r
2619  (ASM_SIMP_TAC[]);\r
2620  (UP_ASM_TAC THEN REWRITE_TAC[VORONOI_NONDG; set_of_list]);\r
2621  (SET_TAC[]);\r
2622 \r
2623  (UNDISCH_TAC `w IN {u0, u1, u2, u3:real^3}`);\r
2624  (REWRITE_TAC[Geomdetail.IN_SET4] THEN REPEAT STRIP_TAC);\r
2625  (ASM_REWRITE_TAC[]);\r
2626 \r
2627  (ASM_REWRITE_TAC[]);\r
2628  (NEW_GOAL `dist (a,u0) <= dist (a,u1:real^3)`);\r
2629  (MATCH_MP_TAC (ASSUME `!w. V w ==> dist (a,u0) <= dist (a,w:real^3)`));\r
2630  (ASM_REWRITE_TAC[GSYM IN]);\r
2631  (NEW_GOAL `dist (a,u1) <= dist (a,u0:real^3)`);\r
2632  (MATCH_MP_TAC (ASSUME `!w. V w ==> dist (a,u1) <= dist (a,w:real^3)`));\r
2633  (ASM_REWRITE_TAC[GSYM IN]);\r
2634  (ASM_REAL_ARITH_TAC);\r
2635 \r
2636  (ASM_REWRITE_TAC[]);\r
2637  (NEW_GOAL `dist (a,u0) <= dist (a,u2:real^3)`);\r
2638  (MATCH_MP_TAC (ASSUME `!w. V w ==> dist (a,u0) <= dist (a,w:real^3)`));\r
2639  (ASM_REWRITE_TAC[GSYM IN]);\r
2640  (NEW_GOAL `dist (a,u2) <= dist (a,u0:real^3)`);\r
2641  (MATCH_MP_TAC (ASSUME `!w. V w ==> dist (a,u2) <= dist (a,w:real^3)`));\r
2642  (ASM_REWRITE_TAC[GSYM IN]);\r
2643  (ASM_REAL_ARITH_TAC);\r
2644 \r
2645  (ASM_REWRITE_TAC[]);\r
2646  (NEW_GOAL `dist (a,u0) <= dist (a,u3:real^3)`);\r
2647  (MATCH_MP_TAC (ASSUME `!w. V w ==> dist (a,u0) <= dist (a,w:real^3)`));\r
2648  (ASM_REWRITE_TAC[GSYM IN]);\r
2649  (NEW_GOAL `dist (a,u3) <= dist (a,u0:real^3)`);\r
2650  (MATCH_MP_TAC (ASSUME `!w. V w ==> dist (a,u3) <= dist (a,w:real^3)`));\r
2651  (ASM_REWRITE_TAC[GSYM IN]);\r
2652  (ASM_REAL_ARITH_TAC);\r
2653 \r
2654  (ASM_REWRITE_TAC[]);\r
2655  (REWRITE_TAC[HL;HD]);\r
2656  (ONCE_REWRITE_TAC[DIST_SYM]);\r
2657  (ABBREV_TAC `S = set_of_list [u0; u1; u2; u3:real^3]`);\r
2658  (NEW_GOAL `(!w. w IN S ==> radV S = dist (circumcenter S,w:real^3))`);\r
2659  (MATCH_MP_TAC Rogers.OAPVION2);\r
2660  (EXPAND_TAC "S" THEN DEL_TAC THEN ASM_REWRITE_TAC[set_of_list]);\r
2661  (FIRST_ASSUM MATCH_MP_TAC);\r
2662  (EXPAND_TAC "S" THEN REWRITE_TAC[set_of_list]);\r
2663  (TRUONG_SET_TAC[])]);;\r
2664 \r
2665 (* ======================================================================= *)\r
2666 (* Lemma 39 *)\r
2667 let ORTHOGONAL_AFF_HULL_2_KY_LEMMA = prove_by_refinement (\r
2668  `!n a b s p:real^3.\r
2669      orthogonal (a - b) n /\ s IN aff {a, b} /\ p IN aff {a, b}\r
2670      ==> orthogonal (s - p) n`,\r
2671 [(REWRITE_TAC[Trigonometry2.AFF2; IN; IN_ELIM_THM; orthogonal]);\r
2672  (REPEAT STRIP_TAC);\r
2673  (ASM_REWRITE_TAC[VECTOR_ARITH `(t % a + (&1 - t) % b) - (t' % a + (&1 - t') % b) \r
2674   = (t - t') % (a - b)`;DOT_LMUL;REAL_MUL_RZERO])]);;\r
2675 (* ======================================================================= *)\r
2676 (* Lemma 40 *)\r
2677 \r
2678 let DIST_PROJECTION_LT_LEMMA = prove_by_refinement (\r
2679  `!x a b:real^3.  ?s. s IN aff {a, b} /\ \r
2680      (!m n. m IN aff {a, b} /\ n IN aff {a, b} ==> \r
2681 (dist (x, m) < dist (x, n) <=> dist (s,m) < dist (s,n)) /\ \r
2682 (dist (x, m) <= dist (x, n) <=> dist (s,m) <= dist (s,n)))`,\r
2683 [ (REPEAT STRIP_TAC);\r
2684  (SUBGOAL_THEN `?s:real^3. s IN aff {a, b} /\ (x - s) dot (a - b) = &0` CHOOSE_TAC);\r
2685  (REWRITE_TAC[Trigonometry2.EXISTS_PROJECTING_POINT2]) ;\r
2686  (EXISTS_TAC `s:real^3` THEN ASM_REWRITE_TAC[]);\r
2687  (UP_ASM_TAC);\r
2688  (REPEAT STRIP_TAC);\r
2689  (NEW_GOAL `orthogonal (a - b) (x - s:real^3)`);\r
2690  (REWRITE_TAC[orthogonal]);\r
2691  (ONCE_REWRITE_TAC[DOT_SYM] THEN ASM_REWRITE_TAC[]);\r
2692 \r
2693  (EQ_TAC);\r
2694  (REPEAT STRIP_TAC);\r
2695  (REWRITE_TAC[dist]);\r
2696  (NEW_GOAL `norm (s - m:real^3) = abs (norm (s - m)) /\ \r
2697              norm (s - n) = abs (norm (s - n))`);\r
2698  (MESON_TAC[REAL_ABS_REFL;NORM_POS_LE]);\r
2699  (ONCE_ASM_REWRITE_TAC[]);\r
2700  (REWRITE_TAC[REAL_LT_SQUARE_ABS]);\r
2701  (NEW_GOAL `norm (x:real^3 - m) pow 2 < norm (x - n) pow 2`);\r
2702  (ONCE_REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS]);\r
2703 \r
2704  (NEW_GOAL `abs (norm (x - m:real^3)) = (norm (x - m)) /\ \r
2705              abs (norm (x - n)) = (norm (x - n))`);\r
2706  (MESON_TAC[REAL_ABS_REFL;NORM_POS_LE]);\r
2707  (ASM_REWRITE_TAC[]);\r
2708  (REWRITE_TAC[GSYM dist]);\r
2709  (ASM_REWRITE_TAC[]);\r
2710  (NEW_GOAL `norm (x - m:real^3) pow 2 = norm (s - m) pow 2 + norm (x - s) pow 2`);\r
2711  (MATCH_MP_TAC PYTHAGORAS);\r
2712  (MATCH_MP_TAC ORTHOGONAL_AFF_HULL_2_KY_LEMMA);\r
2713  (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);\r
2714  (ASM_REWRITE_TAC[]);\r
2715  (NEW_GOAL `norm (x - n:real^3) pow 2 = norm (s - n) pow 2 + norm (x - s) pow 2`);\r
2716  (MATCH_MP_TAC PYTHAGORAS);\r
2717  (MATCH_MP_TAC ORTHOGONAL_AFF_HULL_2_KY_LEMMA);\r
2718  (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);\r
2719  (ASM_REWRITE_TAC[]);\r
2720  (ASM_REAL_ARITH_TAC);\r
2721 \r
2722  (STRIP_TAC);\r
2723  (REWRITE_TAC[dist]);\r
2724  (NEW_GOAL `norm (x - m:real^3) = abs (norm (x - m)) /\ \r
2725              norm (x - n) = abs (norm (x - n))`);\r
2726  (MESON_TAC[REAL_ABS_REFL;NORM_POS_LE]);\r
2727  (ONCE_ASM_REWRITE_TAC[]);\r
2728  (REWRITE_TAC[REAL_LT_SQUARE_ABS]);\r
2729  (NEW_GOAL `norm (s:real^3 - m) pow 2 < norm (s - n) pow 2`);\r
2730  (ONCE_REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS]);\r
2731 \r
2732  (NEW_GOAL `abs (norm (s - m:real^3)) = (norm (s - m)) /\ \r
2733              abs (norm (s - n)) = (norm (s - n))`);\r
2734  (MESON_TAC[REAL_ABS_REFL;NORM_POS_LE]);\r
2735  (ASM_REWRITE_TAC[]);\r
2736  (REWRITE_TAC[GSYM dist]);\r
2737  (ASM_REWRITE_TAC[]);\r
2738  (NEW_GOAL `norm (x - m:real^3) pow 2 = norm (s - m) pow 2 + norm (x - s) pow 2`);\r
2739  (MATCH_MP_TAC PYTHAGORAS);\r
2740  (MATCH_MP_TAC ORTHOGONAL_AFF_HULL_2_KY_LEMMA);\r
2741  (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);\r
2742  (ASM_REWRITE_TAC[]);\r
2743 \r
2744  (NEW_GOAL `norm (x - n:real^3) pow 2 = norm (s - n) pow 2 + norm (x - s) pow 2`);\r
2745  (MATCH_MP_TAC PYTHAGORAS);\r
2746  (MATCH_MP_TAC ORTHOGONAL_AFF_HULL_2_KY_LEMMA);\r
2747  (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);\r
2748  (ASM_REWRITE_TAC[]);\r
2749  (ASM_REAL_ARITH_TAC);\r
2750 \r
2751  (NEW_GOAL `orthogonal (a - b) (x - s:real^3)`);\r
2752  (REWRITE_TAC[orthogonal]);\r
2753  (ONCE_REWRITE_TAC[DOT_SYM] THEN ASM_REWRITE_TAC[]);\r
2754 \r
2755  (EQ_TAC);\r
2756  (REPEAT STRIP_TAC);\r
2757  (REWRITE_TAC[dist]);\r
2758  (NEW_GOAL `norm (s - m:real^3) = abs (norm (s - m)) /\ \r
2759              norm (s - n) = abs (norm (s - n))`);\r
2760  (MESON_TAC[REAL_ABS_REFL;NORM_POS_LE]);\r
2761  (ONCE_ASM_REWRITE_TAC[]);\r
2762  (REWRITE_TAC[REAL_LE_SQUARE_ABS]);\r
2763  (NEW_GOAL `norm (x:real^3 - m) pow 2 <= norm (x - n) pow 2`);\r
2764  (ONCE_REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS]);\r
2765 \r
2766  (NEW_GOAL `abs (norm (x - m:real^3)) = (norm (x - m)) /\ \r
2767              abs (norm (x - n)) = (norm (x - n))`);\r
2768  (MESON_TAC[REAL_ABS_REFL;NORM_POS_LE]);\r
2769  (ASM_REWRITE_TAC[]);\r
2770  (REWRITE_TAC[GSYM dist]);\r
2771  (ASM_REWRITE_TAC[]);\r
2772  (NEW_GOAL `norm (x - m:real^3) pow 2 = norm (s - m) pow 2 + norm (x - s) pow 2`);\r
2773  (MATCH_MP_TAC PYTHAGORAS);\r
2774  (MATCH_MP_TAC ORTHOGONAL_AFF_HULL_2_KY_LEMMA);\r
2775  (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);\r
2776  (ASM_REWRITE_TAC[]);\r
2777  (NEW_GOAL `norm (x - n:real^3) pow 2 = norm (s - n) pow 2 + norm (x - s) pow 2`);\r
2778  (MATCH_MP_TAC PYTHAGORAS);\r
2779  (MATCH_MP_TAC ORTHOGONAL_AFF_HULL_2_KY_LEMMA);\r
2780  (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);\r
2781  (ASM_REWRITE_TAC[]);\r
2782  (ASM_REAL_ARITH_TAC);\r
2783 \r
2784  (STRIP_TAC);\r
2785  (REWRITE_TAC[dist]);\r
2786  (NEW_GOAL `norm (x - m:real^3) = abs (norm (x - m)) /\ \r
2787              norm (x - n) = abs (norm (x - n))`);\r
2788  (MESON_TAC[REAL_ABS_REFL;NORM_POS_LE]);\r
2789  (ONCE_ASM_REWRITE_TAC[]);\r
2790  (REWRITE_TAC[REAL_LE_SQUARE_ABS]);\r
2791  (NEW_GOAL `norm (s:real^3 - m) pow 2 <= norm (s - n) pow 2`);\r
2792  (ONCE_REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS]);\r
2793 \r
2794  (NEW_GOAL `abs (norm (s - m:real^3)) = (norm (s - m)) /\ \r
2795              abs (norm (s - n)) = (norm (s - n))`);\r
2796  (MESON_TAC[REAL_ABS_REFL;NORM_POS_LE]);\r
2797  (ASM_REWRITE_TAC[]);\r
2798  (REWRITE_TAC[GSYM dist]);\r
2799  (ASM_REWRITE_TAC[]);\r
2800  (NEW_GOAL `norm (x - m:real^3) pow 2 = norm (s - m) pow 2 + norm (x - s) pow 2`);\r
2801  (MATCH_MP_TAC PYTHAGORAS);\r
2802  (MATCH_MP_TAC ORTHOGONAL_AFF_HULL_2_KY_LEMMA);\r
2803  (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);\r
2804  (ASM_REWRITE_TAC[]);\r
2805 \r
2806  (NEW_GOAL `norm (x - n:real^3) pow 2 = norm (s - n) pow 2 + norm (x - s) pow 2`);\r
2807  (MATCH_MP_TAC PYTHAGORAS);\r
2808  (MATCH_MP_TAC ORTHOGONAL_AFF_HULL_2_KY_LEMMA);\r
2809  (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);\r
2810  (ASM_REWRITE_TAC[]);\r
2811  (ASM_REAL_ARITH_TAC)\r
2812 ]);;\r
2813 \r
2814 (* ======================================================================= *)\r
2815 (* Lemma 41 *)\r
2816 \r
2817 let SIMPLEX_FURTHEST_LT_2 = prove_by_refinement (\r
2818  `!a (s:real^N->bool).\r
2819          FINITE s\r
2820          ==> (!x. x IN convex hull s /\ ~(x IN s)\r
2821               ==> (?y. y IN s /\ norm (x - a) < norm (y - a)))`,\r
2822 [(REPEAT STRIP_TAC);\r
2823  (NEW_GOAL `(?y:real^N. y IN convex hull s /\ norm (x - a) < norm (y - a))`);\r
2824  (ASM_SIMP_TAC[SIMPLEX_FURTHEST_LT]);\r
2825  (FIRST_X_ASSUM CHOOSE_TAC);\r
2826  (ASM_CASES_TAC `y:real^N IN s`);\r
2827  (EXISTS_TAC `y:real^N`);\r
2828  (ASM_REWRITE_TAC[]);\r
2829  (SUBGOAL_THEN `(?y. y:real^N IN s /\\r
2830                   (!x. x IN convex hull s ==> norm (x - a) <= norm (y - a)))`\r
2831   CHOOSE_TAC);\r
2832  (MATCH_MP_TAC SIMPLEX_FURTHEST_LE);\r
2833  (ASM_REWRITE_TAC[]);\r
2834  (STRIP_TAC);\r
2835  (UNDISCH_TAC `x:real^N IN convex hull s`);\r
2836  (ASM_REWRITE_TAC[CONVEX_HULL_EMPTY]);\r
2837  (SET_TAC[]);\r
2838  (EXISTS_TAC `y':real^N`);\r
2839  (ASM_REWRITE_TAC[]);\r
2840  (MATCH_MP_TAC (REAL_ARITH `m < norm (y-a:real^N) /\ norm (y-a) <= n ==> m < n`));\r
2841  (ASM_REWRITE_TAC[]);\r
2842  (UP_ASM_TAC THEN STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC);\r
2843  (ASM_REWRITE_TAC[])]);;\r
2844 \r
2845 (* ======================================================================= *)\r
2846 (* Lemma 42 *)\r
2847 \r
2848 let DIST_BETWEEN_FURTHEST_LT = prove_by_refinement (\r
2849   `!x a b s:real^3. \r
2850         between s (a, b) /\ ~(s = a) /\ ~(s = b) /\ ~(a = b) /\\r
2851         dist (x, b) <= dist (x, a) \r
2852     ==> dist (x,s) < dist (x,a)`,\r
2853 [(REPEAT GEN_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL] THEN REPEAT STRIP_TAC \r
2854   THEN NEW_GOAL `(?y:real^3. y IN {a,b} /\ norm (s - x) < norm (y - x))`);\r
2855  (NEW_GOAL`(!h. h IN convex hull {a,b} /\ ~(h IN {a,b:real^3})\r
2856                   ==> (?y. y IN {a,b} /\ norm (h - x) < norm (y - x)))`);\r
2857  (MATCH_MP_TAC SIMPLEX_FURTHEST_LT_2 THEN REWRITE_TAC[Geomdetail.FINITE6]);\r
2858  (FIRST_X_ASSUM MATCH_MP_TAC);\r
2859  (ASM_SET_TAC[]);\r
2860  (FIRST_X_ASSUM CHOOSE_TAC THEN UP_ASM_TAC);\r
2861  (REWRITE_TAC[SET_RULE `a IN {m,n} <=> a = m \/ a = n`]);\r
2862  (REWRITE_TAC[GSYM dist] THEN REPEAT STRIP_TAC);\r
2863  (ASM_MESON_TAC[DIST_SYM]);\r
2864  (ASM_MESON_TAC[DIST_SYM; REAL_ARITH `x < y /\ y <= z ==> x < z`])]);;\r
2865 \r
2866 (* ======================================================================= *)\r
2867 (* Lemma 43 *)\r
2868 \r
2869 let ROGERS_EXPLICIT = prove_by_refinement (\r
2870  `!V ul.\r
2871   saturated V /\ packing V /\ barV V 3 ul ==> \r
2872   rogers V ul = convex hull \r
2873  {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`,\r
2874 [(REPEAT STRIP_TAC THEN REWRITE_TAC[ROGERS]);\r
2875  (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);\r
2876  (MP_TAC (ASSUME `barV V 3 ul`));\r
2877  (REWRITE_TAC[BARV_3_EXPLICIT]);\r
2878  (FIRST_X_ASSUM CHOOSE_TAC);\r
2879  (FIRST_X_ASSUM CHOOSE_TAC);\r
2880  (FIRST_X_ASSUM CHOOSE_TAC);\r
2881  (FIRST_X_ASSUM CHOOSE_TAC);\r
2882  (REWRITE_WITH `{j | j < LENGTH (ul:(real^3)list)} = {0, 1,2,3}`);\r
2883  (ASM_REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`]);\r
2884  (MESON_TAC[SET_OF_0_TO_3]);\r
2885  (REWRITE_TAC[IMAGE]);\r
2886  (AP_TERM_TAC);\r
2887  (REWRITE_WITH `!x. x IN {0,1,2,3} <=> (x = 0 \/x = 1 \/x = 2 \/x = 3)`);\r
2888  (SET_TAC[]);\r
2889  (REWRITE_WITH \r
2890  `!y. (?x. (x = 0 \/ x = 1 \/ x = 2 \/ x = 3) /\ y = omega_list_n V ul x) \r
2891  <=> (y = omega_list_n V ul 0) \/ (y = omega_list_n V ul 1) \/\r
2892      (y = omega_list_n V ul 2) \/(y = omega_list_n V ul 3)`);\r
2893  (SET_TAC[BETA_THM]);\r
2894  (REWRITE_WITH \r
2895     `{y | y = omega_list_n V ul 0 \/ y = omega_list_n V ul 1 \/\r
2896           y = omega_list_n V ul 2 \/ y = omega_list_n V ul 3} \r
2897      =  {omega_list_n V ul 0, omega_list_n V ul 1,\r
2898         omega_list_n V ul 2, omega_list_n V ul 3}`);\r
2899  (SET_TAC[]);\r
2900  (REWRITE_WITH `omega_list_n V ul 0 = HD ul`);\r
2901  (REWRITE_TAC[OMEGA_LIST_N])]);;\r
2902 \r
2903 (* ======================================================================= *)\r
2904 (* Lemma 44 *)\r
2905 let SEGMENT_INTER_CBALL_LEMMA  = prove\r
2906   (`!x r a (b:real^3).\r
2907          dist (x, a) <= r /\ r <= dist (x, b)\r
2908          ==> (?c. between c (a, b) /\ dist (x, c) = r)`,\r
2909    REPEAT STRIP_TAC THEN ASM_CASES_TAC `dist(x:real^3,b) = r` THENL\r
2910     [EXISTS_TAC `b:real^3` THEN ASM_REWRITE_TAC[BETWEEN_REFL];\r
2911      MP_TAC(ISPECL [`segment[a:real^3,b]`; `cball(x:real^3,r)`]\r
2912                    CONNECTED_INTER_FRONTIER) THEN\r
2913      ANTS_TAC THENL\r
2914       [REWRITE_TAC[CONNECTED_SEGMENT; GSYM MEMBER_NOT_EMPTY] THEN CONJ_TAC THENL\r
2915         [EXISTS_TAC `a:real^3` THEN\r
2916          ASM_REWRITE_TAC[IN_INTER; ENDS_IN_SEGMENT; IN_CBALL];\r
2917          EXISTS_TAC `b:real^3` THEN\r
2918          ASM_REWRITE_TAC[IN_DIFF; ENDS_IN_SEGMENT; IN_CBALL] THEN\r
2919          ASM_REAL_ARITH_TAC];\r
2920        REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN MATCH_MP_TAC MONO_EXISTS THEN\r
2921        REWRITE_TAC[FRONTIER_CBALL; IN_ELIM_THM; IN_INTER;\r
2922                    BETWEEN_IN_SEGMENT]]]);;\r
2923 \r
2924 (* ======================================================================= *)\r
2925 (* Lemma 45 *)\r
2926 let CLOSEST_POINT_SING = prove_by_refinement (\r
2927  `!a (b:real^3). closest_point {a} b = a`,\r
2928 [(REPEAT GEN_TAC THEN REWRITE_TAC\r
2929    [closest_point;SET_RULE `a IN {x} <=> a = x`]);\r
2930  (MATCH_MP_TAC SELECT_UNIQUE);\r
2931  (REWRITE_TAC[BETA_THM] THEN GEN_TAC THEN EQ_TAC);\r
2932  (REPEAT STRIP_TAC);\r
2933  (REPEAT STRIP_TAC);\r
2934  (ASM_REWRITE_TAC[]);\r
2935  (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC)]);;\r
2936 \r
2937 (* ======================================================================= *)\r
2938 (* Lemma 46 *)\r
2939 \r
2940 let MXI_EXPLICIT = prove_by_refinement(\r
2941  `!V ul. packing V /\ saturated V /\ barV V 3 ul /\ ul = [u0;u1;u2;u3] /\\r
2942            hl (truncate_simplex 2 ul) < sqrt (&2) /\ sqrt (&2) <= hl ul \r
2943     ==> (?s. between s (omega_list_n V ul 2, omega_list_n V ul 3) /\\r
2944                 dist (u0, s) = sqrt (&2) /\\r
2945                  mxi V ul = s)`,\r
2946 [(REPEAT STRIP_TAC);\r
2947  (NEW_GOAL \r
2948   `?(s:real^3). between s (omega_list_n V ul 2, omega_list_n V ul 3) /\\r
2949                 dist (u0, s) = sqrt (&2)`);\r
2950  (MATCH_MP_TAC SEGMENT_INTER_CBALL_LEMMA);\r
2951  STRIP_TAC;\r
2952 \r
2953  (REWRITE_WITH `dist (u0:real^3,omega_list_n V ul 2) = \r
2954                  hl (truncate_simplex 2 ul)`);\r
2955  (ABBREV_TAC `vl = truncate_simplex 2 (ul:(real^3)list)`);\r
2956  (REWRITE_WITH `hl (vl:(real^3)list) = \r
2957                  dist (circumcenter (set_of_list vl),HD vl)`);\r
2958  (MATCH_MP_TAC Rogers.HL_EQ_DIST0);\r
2959  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);\r
2960  (ASM_REWRITE_TAC[]);\r
2961  (EXPAND_TAC "vl");\r
2962  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
2963  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
2964  (REWRITE_TAC[DIST_SYM]);\r
2965  (AP_TERM_TAC);\r
2966  (REWRITE_TAC[PAIR_EQ]);\r
2967  (STRIP_TAC);\r
2968  (EXPAND_TAC "vl");\r
2969  (DEL_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);\r
2970  (ASM_REWRITE_TAC[Marchal_cells.OMEGA_LIST_TRUNCATE_2]);\r
2971  (REWRITE_WITH `omega_list V [u0; u1; u2] = omega_list V (vl:(real^3)list)`);\r
2972  (EXPAND_TAC "vl");\r
2973  (DEL_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
2974  (MATCH_MP_TAC XNHPWAB1);\r
2975  (EXISTS_TAC `2`);\r
2976  (ASM_REWRITE_TAC[]);\r
2977  (REWRITE_TAC[IN] THEN EXPAND_TAC "vl");\r
2978  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
2979  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
2980  (ASM_REAL_ARITH_TAC);\r
2981 \r
2982 (* ======================================================================== *)\r
2983 \r
2984  (NEW_GOAL `~affine_dependent {u0,u1,u2,u3:real^3}`);\r
2985  (ASM_MESON_TAC[set_of_list; AFF_INDEPENDENT_SET_OF_LIST_BARV]);\r
2986 \r
2987  (REWRITE_WITH `dist (u0:real^3,omega_list_n V ul 3) = \r
2988                  hl (truncate_simplex 3 ul)`);\r
2989  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);\r
2990  (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `3 = SUC 2`]);\r
2991  (ONCE_REWRITE_TAC[ARITH_RULE `SUC 2 = 3`]);\r
2992  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);\r
2993 \r
2994  (NEW_GOAL `barV V 3 ul`);\r
2995  (ASM_REWRITE_TAC[]);\r
2996  (UP_ASM_TAC THEN REWRITE_TAC[BARV; VORONOI_NONDG]);\r
2997  (REPEAT STRIP_TAC);\r
2998  (NEW_GOAL `(?a. voronoi_list V ul = {a:real^3} /\\r
2999                   a = circumcenter (set_of_list ul) /\\r
3000                   hl ul = dist (HD ul,a))`);\r
3001  (ASM_SIMP_TAC[VORONOI_LIST_3_SINGLETON_EXPLICIT]);\r
3002  (UP_ASM_TAC THEN ASM_REWRITE_TAC[HD] THEN REPEAT STRIP_TAC);\r
3003  (REWRITE_TAC[ASSUME `voronoi_list V [u0; u1; u2; u3] = {a:real^3}`]);\r
3004  (REWRITE_TAC[CLOSEST_POINT_SING]);\r
3005  (ASM_MESON_TAC[]);\r
3006  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);\r
3007  (ASM_MESON_TAC[]);\r
3008  (UP_ASM_TAC THEN REPEAT STRIP_TAC);\r
3009 \r
3010  (EXISTS_TAC `s:real^3`);\r
3011  (ASM_REWRITE_TAC[]);\r
3012  (REWRITE_TAC[mxi]);\r
3013  (COND_CASES_TAC);\r
3014  (NEW_GOAL `F`);\r
3015  (UNDISCH_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) < sqrt (&2)`);\r
3016  (ASM_REWRITE_TAC[]);\r
3017  (ASM_REAL_ARITH_TAC);\r
3018 \r
3019  (UP_ASM_TAC THEN MESON_TAC[]);\r
3020  (MATCH_MP_TAC SELECT_UNIQUE);\r
3021  (REPEAT STRIP_TAC);\r
3022  (REWRITE_TAC[BETA_THM]);\r
3023  (REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL;HD]);\r
3024  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
3025  (EQ_TAC);\r
3026  (STRIP_TAC);\r
3027  (ASM_REWRITE_TAC[]);\r
3028  (ASM_MESON_TAC[DIST_SYM]);\r
3029 \r
3030  (DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN\r
3031    REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;\r
3032    CONVEX_HULL_2; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);\r
3033  (ABBREV_TAC `a = omega_list_n V [u0; u1; u2; u3:real^3] 2`);\r
3034  (ABBREV_TAC `b = omega_list_n V [u0; u1; u2; u3:real^3] 3`);\r
3035  (NEW_GOAL `s = u % a + v % (b:real^3)`);\r
3036  (ASM_MESON_TAC[]);\r
3037  (NEW_GOAL `?c. c IN aff {a, b} /\ (u0 - c) dot (a - b:real^3) = &0`);\r
3038  (REWRITE_TAC[Trigonometry2.EXISTS_PROJECTING_POINT2]);\r
3039  (FIRST_X_ASSUM CHOOSE_TAC);\r
3040  (UP_ASM_TAC THEN REWRITE_TAC[Trigonometry2.AFF2;IN;IN_ELIM_THM]);\r
3041  (REPEAT STRIP_TAC);\r
3042 \r
3043 \r
3044  (NEW_GOAL `dist (u0, a:real^3) < sqrt (&2)`);\r
3045  (REWRITE_WITH `dist (u0, a:real^3) = hl (truncate_simplex 2 (ul:(real^3)list))`);\r
3046  (ABBREV_TAC `vl = truncate_simplex 2 (ul:(real^3)list)`);\r
3047  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
3048  (ONCE_REWRITE_TAC[DIST_SYM]);\r
3049  (REWRITE_WITH `a:real^3 = omega_list V vl`);\r
3050  (EXPAND_TAC "vl" THEN DEL_TAC);\r
3051  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; LENGTH; ARITH_RULE `SUC (SUC (SUC 0)) - 1 = 2`]);\r
3052  (EXPAND_TAC "a");\r
3053  (REWRITE_TAC[Marchal_cells.OMEGA_LIST_TRUNCATE_2]);\r
3054  (REWRITE_WITH `u0:real^3 = HD vl`);\r
3055  (EXPAND_TAC "vl" THEN DEL_TAC);\r
3056  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);\r
3057  (MATCH_MP_TAC Rogers.WAUFCHE2);\r
3058  (EXISTS_TAC `2`);\r
3059  (ASM_REWRITE_TAC[]);\r
3060  (EXPAND_TAC "vl" THEN DEL_TAC);\r
3061  (ASM_REWRITE_TAC[IN]);\r
3062  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
3063  (EXISTS_TAC `3`);\r
3064  (ASM_MESON_TAC [ARITH_RULE `2 <= 3 `]);\r
3065  (ASM_REWRITE_TAC[]);\r
3066 \r
3067  (NEW_GOAL `dist (u0, b:real^3) >= sqrt (&2)`);\r
3068  (REWRITE_WITH `dist (u0, b:real^3) = hl (ul:(real^3)list)`);\r
3069  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
3070  (SUBGOAL_THEN `?m. voronoi_list V ul = {m:real^3} /\\r
3071                   m = circumcenter (set_of_list ul) /\\r
3072                   hl ul = dist (HD ul,m)` CHOOSE_TAC);\r
3073  (ASM_SIMP_TAC [VORONOI_LIST_3_SINGLETON_EXPLICIT]);\r
3074  (NEW_GOAL `(b:real^3) IN voronoi_list V ul`);\r
3075  (EXPAND_TAC "b");\r
3076  (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `3 = SUC 2`]);\r
3077  (REWRITE_TAC[ARITH_RULE `SUC 2 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3]);\r
3078  (REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`]);\r
3079  (MATCH_MP_TAC CLOSEST_POINT_IN_SET);\r
3080  (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);\r
3081  (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);\r
3082  (UP_ASM_TAC THEN REPEAT STRIP_TAC);\r
3083  (ASM_SET_TAC[]);\r
3084 \r
3085  (UP_ASM_TAC THEN UP_ASM_TAC THEN REPEAT STRIP_TAC);\r
3086  (UP_ASM_TAC THEN REWRITE_TAC[ASSUME `voronoi_list V ul = {m:real^3}`]);\r
3087  (REWRITE_TAC[IN_SING] THEN STRIP_TAC);\r
3088  (REWRITE_WITH `u0:real^3 = HD ul`);\r
3089  (ASM_REWRITE_TAC[HD]);\r
3090  (REWRITE_TAC[ASSUME `b = m:real^3`]);\r
3091  (ASM_REWRITE_TAC[]);\r
3092  (ASM_REWRITE_TAC[]);\r
3093 \r
3094  (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]\r
3095    THEN ASM_REAL_ARITH_TAC);\r
3096 \r
3097 (* ======================================================================== *)\r
3098 \r
3099  (ASM_CASES_TAC `y = s:real^3`);\r
3100  (ASM_MESON_TAC[]);\r
3101  (NEW_GOAL `between y (a, b:real^3)`);\r
3102  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
3103  (EXISTS_TAC `u':real` THEN EXISTS_TAC `v':real` THEN ASM_REWRITE_TAC[]);\r
3104  (NEW_GOAL `between s (a, b:real^3)`);\r
3105  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
3106  (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN ASM_REWRITE_TAC[]);\r
3107  (ASM_CASES_TAC `between y (s, a:real^3)`);\r
3108 \r
3109  (NEW_GOAL `dist (u0,y) < dist (u0,s:real^3)`);\r
3110  (MATCH_MP_TAC DIST_BETWEEN_FURTHEST_LT);\r
3111  (EXISTS_TAC `a:real^3`);\r
3112  (REPEAT STRIP_TAC);\r
3113 \r
3114  (ASM_REWRITE_TAC[]);\r
3115  (ASM_MESON_TAC[]);\r
3116  (NEW_GOAL `dist (y:real^3,u0) < sqrt (&2)`);\r
3117  (REWRITE_TAC[ASSUME `y = a:real^3`]);\r
3118  (ONCE_REWRITE_TAC[DIST_SYM]);\r
3119  (ASM_MESON_TAC[]);\r
3120  (ASM_REAL_ARITH_TAC);\r
3121 \r
3122  (NEW_GOAL `dist (u0:real^3,s) < sqrt (&2)`);\r
3123  (REWRITE_TAC[ASSUME `s = a:real^3`]);\r
3124  (ASM_MESON_TAC[]);\r
3125  (ASM_REAL_ARITH_TAC);\r
3126 \r
3127  (ASM_REAL_ARITH_TAC);\r
3128  (NEW_GOAL `F`);\r
3129  (UP_ASM_TAC THEN REWRITE_WITH `dist (u0,y) = dist (y,u0:real^3)`);\r
3130  (MESON_TAC[DIST_SYM]);\r
3131  (ASM_REWRITE_TAC[]);\r
3132  (REAL_ARITH_TAC);\r
3133  (UP_ASM_TAC THEN MESON_TAC[]);\r
3134 \r
3135 \r
3136  (ASM_CASES_TAC `between s (y, a:real^3)`);\r
3137 \r
3138  (NEW_GOAL `dist (u0,s) < dist (u0,y:real^3)`);\r
3139  (MATCH_MP_TAC DIST_BETWEEN_FURTHEST_LT);\r
3140  (EXISTS_TAC `a:real^3`);\r
3141  (REPEAT STRIP_TAC);\r
3142 \r
3143  (ASM_REWRITE_TAC[]);\r
3144  (ASM_MESON_TAC[]);\r
3145  (NEW_GOAL `dist (u0,s:real^3) < sqrt (&2)`);\r
3146  (REWRITE_TAC[ASSUME `s = a:real^3`]);\r
3147  (ASM_MESON_TAC[]);\r
3148  (ASM_REAL_ARITH_TAC);\r
3149 \r
3150  (NEW_GOAL `dist (y, u0:real^3) < sqrt (&2)`);\r
3151  (REWRITE_TAC[ASSUME `y = a:real^3`]);\r
3152  (ONCE_REWRITE_TAC[DIST_SYM]);\r
3153  (ASM_MESON_TAC[]);\r
3154  (ASM_REAL_ARITH_TAC);\r
3155 \r
3156  (REWRITE_WITH `dist (u0,y:real^3) = dist (y, u0)`);\r
3157  (MESON_TAC[DIST_SYM]);\r
3158  (ASM_REAL_ARITH_TAC);\r
3159  (NEW_GOAL `F`);\r
3160  (UP_ASM_TAC THEN REWRITE_WITH `dist (u0,y) = dist (y,u0:real^3)`);\r
3161  (MESON_TAC[DIST_SYM]);\r
3162  (ASM_REWRITE_TAC[]);\r
3163  (REAL_ARITH_TAC);\r
3164  (UP_ASM_TAC THEN MESON_TAC[]);\r
3165 \r
3166  (NEW_GOAL `collinear {y, s, a:real^3}`);\r
3167  (MATCH_MP_TAC AFFINE_HULL_3_IMP_COLLINEAR);\r
3168  (REWRITE_TAC[AFFINE_HULL_2;IN;IN_ELIM_THM]);\r
3169  (ASM_REWRITE_TAC[]);\r
3170 \r
3171  (EXISTS_TAC `v / (v - v')`);\r
3172  (EXISTS_TAC `&1 - v / (v - v')`);\r
3173  (REWRITE_TAC[REAL_ARITH `a + &1 - a = &1`]);\r
3174  (REWRITE_TAC[VECTOR_ARITH `a = x1 % (u' % a + v' % b) + x2 % (u % a + v % b)\r
3175    <=> (&1 - x1 * u' - x2 * u) % a - (x1 * v' + x2 * v) % b = vec 0`]);\r
3176  (REWRITE_WITH `&1 - v / (v - v') * u' - (&1 - v / (v - v')) * u = &0`);\r
3177  (REWRITE_TAC[REAL_ARITH `&1 - v / (v - v') * u' - (&1 - v / (v - v')) * u = \r
3178    (&1 - u) + v * (u - u') / (v - v') `]);\r
3179  (REWRITE_WITH `u - u' = v' - v:real`);\r
3180  (ASM_REAL_ARITH_TAC);\r
3181  (REWRITE_TAC[REAL_ARITH `&1 - u + v * (v' - v) / (v - v') = &1 - u - v * (v - v') / (v - v')`]);\r
3182  (REWRITE_WITH  `(v - v') / (v - v') = &1`);\r
3183  (MATCH_MP_TAC REAL_DIV_REFL);\r
3184  (REWRITE_TAC[REAL_ARITH `b - a = &0 <=> a = b`]);\r
3185 \r
3186  (STRIP_TAC);\r
3187  (NEW_GOAL `s = y:real^3`);\r
3188  (REWRITE_TAC[ASSUME `y = u' % a + v' % (b:real^3)`; \r
3189                ASSUME `s = u % a + v % (b:real^3)`]);\r
3190  (NEW_GOAL `u = u':real`);\r
3191  (ASM_REAL_ARITH_TAC);\r
3192  (REWRITE_TAC[ASSUME `v' = v:real`; ASSUME `u = u':real`]);\r
3193  (ASM_MESON_TAC[]);\r
3194  (ASM_REAL_ARITH_TAC);\r
3195 \r
3196  (REWRITE_WITH `v / (v - v') * v' + (&1 - v / (v - v')) * v = &0`);\r
3197  (REWRITE_TAC[REAL_ARITH `v / (v - v') * v' + (&1 - v / (v - v')) * v = \r
3198    v - v * (v - v') / (v - v') `]);\r
3199  (REWRITE_WITH  `(v - v') / (v - v') = &1`);\r
3200  (MATCH_MP_TAC REAL_DIV_REFL);\r
3201  (REWRITE_TAC[REAL_ARITH `b - a = &0 <=> a = b`]);\r
3202  (STRIP_TAC);\r
3203  (NEW_GOAL `s = y:real^3`);\r
3204  (REWRITE_TAC[ASSUME `y = u' % a + v' % (b:real^3)`; \r
3205                ASSUME `s = u % a + v % (b:real^3)`]);\r
3206  (NEW_GOAL `u = u':real`);\r
3207  (ASM_REAL_ARITH_TAC);\r
3208  (REWRITE_TAC[ASSUME `v' = v:real`; ASSUME `u = u':real`]);\r
3209  (ASM_MESON_TAC[]);\r
3210  (ASM_REAL_ARITH_TAC);\r
3211  (VECTOR_ARITH_TAC);\r
3212 \r
3213  (NEW_GOAL `between a (s, y:real^3)`);\r
3214  (UP_ASM_TAC THEN REWRITE_TAC[COLLINEAR_BETWEEN_CASES]);\r
3215  (ASM_MESON_TAC[BETWEEN_SYM]);\r
3216  (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;\r
3217   IN_ELIM_THM] THEN REPEAT STRIP_TAC);\r
3218  (NEW_GOAL `a = u'' % s + v'' % (y:real^3)`);\r
3219  (UP_ASM_TAC THEN REWRITE_TAC[]);\r
3220  (UP_ASM_TAC THEN REWRITE_TAC[ASSUME `y = u' % a + v' % (b:real^3)`; \r
3221    ASSUME `s = u % a + v % (b:real^3)`]);\r
3222 \r
3223  (REWRITE_TAC[VECTOR_ARITH \r
3224   `a = u'' % (u % a + v % b) + v'' % (u' % a + v' % b)  \r
3225    <=> (u''* u + v'' * u' - &1) % a + (u'' * v + v'' * v') % b = vec 0`]);\r
3226  (REWRITE_WITH `(u'' * v + v'' * v') = -- (u'' * u + v'' * u' - &1)`);\r
3227  (REWRITE_TAC[REAL_ARITH `u'' * v + v'' * v' = --(u'' * u + v'' * u' - &1) <=>\r
3228   u'' * (u + v) + v'' * (u' + v') = &1`]);\r
3229  (ASM_REWRITE_TAC[REAL_MUL_RID]);\r
3230  (REWRITE_TAC[VECTOR_ARITH `a % x + -- a % y = a % (x - y)`;VECTOR_MUL_EQ_0]);\r
3231  (REPEAT STRIP_TAC);\r
3232  (NEW_GOAL `u'' * u <= u'' * (u + v)`);\r
3233  (REWRITE_TAC[REAL_ARITH `a * b <= a * (b + c) <=> &0 <= a * c`]);\r
3234  (ASM_SIMP_TAC[REAL_LE_MUL]);\r
3235  (NEW_GOAL `v'' * u' <= v'' * (u' + v')`);\r
3236  (REWRITE_TAC[REAL_ARITH `a * b <= a * (b + c) <=> &0 <= a * c`]);\r
3237  (ASM_SIMP_TAC[REAL_LE_MUL]);\r
3238  (NEW_GOAL `u'' * (u + v) + v'' * (u' + v') = &1`);\r
3239  (ASM_REWRITE_TAC[REAL_MUL_RID]);\r
3240  (NEW_GOAL `v'' * u' = v'' * (u' + v')`);\r
3241  (ASM_REAL_ARITH_TAC);\r
3242  (UP_ASM_TAC THEN REWRITE_TAC[REAL_ARITH `a * b = a * (b + c) <=> &0 = a * c`]);\r
3243  (DISCH_TAC);\r
3244  (NEW_GOAL `u'' * u = u'' * (u + v)`);\r
3245  (ASM_REAL_ARITH_TAC);\r
3246  (UP_ASM_TAC THEN REWRITE_TAC[REAL_ARITH `a * b = a * (b + c) <=> &0 = a * c`]);\r
3247  (DISCH_TAC);\r
3248 \r
3249  (NEW_GOAL `~(u'' = &0)`);\r
3250  (STRIP_TAC);\r
3251  (NEW_GOAL `a = y:real^3`);\r
3252  (REWRITE_TAC[ASSUME `a = u'' % s + v'' % (y:real^3)`]);\r
3253  (REWRITE_WITH `u'' = &0 /\ v'' = &1`);\r
3254  (ASM_REAL_ARITH_TAC);\r
3255  (VECTOR_ARITH_TAC);\r
3256  (NEW_GOAL `dist (y, u0:real^3) < sqrt (&2)`);\r
3257  (ONCE_REWRITE_TAC[DIST_SYM]);\r
3258  (REWRITE_TAC[GSYM (ASSUME `a = y:real^3`)]);\r
3259  (ASM_MESON_TAC[]);\r
3260  (ASM_REAL_ARITH_TAC);\r
3261 \r
3262  (NEW_GOAL `v = &0`);\r
3263  (MP_TAC (GSYM (ASSUME `&0 = u'' * v`)));\r
3264  (REWRITE_TAC[REAL_ENTIRE]);\r
3265  (ASM_MESON_TAC[]);\r
3266 \r
3267  (NEW_GOAL `a = s:real^3`);\r
3268  (REWRITE_TAC[ASSUME `s = u % a + v % (b:real^3)`]);\r
3269  (REWRITE_WITH `u = &1 /\ v = &0`);\r
3270  (ASM_REAL_ARITH_TAC);\r
3271  (VECTOR_ARITH_TAC);\r
3272  (NEW_GOAL `dist (u0:real^3, s) < sqrt (&2)`);\r
3273  (REWRITE_TAC[GSYM (ASSUME `a = s:real^3`)]);\r
3274  (ASM_MESON_TAC[]);\r
3275  (NEW_GOAL `F`);\r
3276  (ASM_REAL_ARITH_TAC);\r
3277  (ASM_MESON_TAC[]);\r
3278  (UP_ASM_TAC THEN REWRITE_TAC[VECTOR_ARITH `a - b = vec 0 <=> a = b`]);\r
3279  (DISCH_TAC);\r
3280  (NEW_GOAL `dist (u0,a:real^3) >= sqrt (&2)`);\r
3281  (REWRITE_TAC[(ASSUME `a = b:real^3`)]);\r
3282  (ASM_MESON_TAC[]);\r
3283  (ASM_REAL_ARITH_TAC)]);;\r
3284 \r
3285 (* ======================================================================= *)\r
3286 (* Lemma 47 *)\r
3287 let CONVEX_HULL_4_IMP_2_2 = prove_by_refinement (\r
3288  `!a b c d p:real^3. \r
3289    p IN convex hull {a,b,c,d} \r
3290    ==> (?m n. between p (m,n) /\ between m (a,b) /\ between n (c,d))`,\r
3291 [(REWRITE_TAC[CONVEX_HULL_4;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);\r
3292  (ASM_CASES_TAC `u + v = &0`);\r
3293  (NEW_GOAL `u = &0 /\ v = &0`);\r
3294  (ASM_REAL_ARITH_TAC);\r
3295  (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `p:real^3`);\r
3296  (REWRITE_TAC[BETWEEN_REFL]);\r
3297  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
3298  (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`);\r
3299  (ASM_REWRITE_TAC[]);\r
3300  (STRIP_TAC);\r
3301  (ASM_REAL_ARITH_TAC);\r
3302  (VECTOR_ARITH_TAC);\r
3303 \r
3304  (ASM_CASES_TAC `w + z = &0`);\r
3305  (NEW_GOAL `w = &0 /\ z = &0`);\r
3306  (ASM_REAL_ARITH_TAC);\r
3307  (EXISTS_TAC `p:real^3` THEN EXISTS_TAC `c:real^3`);\r
3308  (REWRITE_TAC[BETWEEN_REFL]);\r
3309  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
3310  (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real`);\r
3311  (ASM_REWRITE_TAC[]);\r
3312  (STRIP_TAC);\r
3313  (ASM_REAL_ARITH_TAC);\r
3314  (VECTOR_ARITH_TAC);\r
3315 \r
3316  (EXISTS_TAC `u/(u+v) % (a:real^3) + v /(u+v) % b`);\r
3317  (EXISTS_TAC `w/(w+z) % (c:real^3) + z/(w+z) % d`);\r
3318  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
3319  (REPEAT STRIP_TAC);\r
3320  (EXISTS_TAC `u + v` THEN EXISTS_TAC `w + z`);\r
3321  (REPEAT STRIP_TAC);\r
3322  (ASM_REAL_ARITH_TAC);\r
3323  (ASM_REAL_ARITH_TAC);\r
3324  (ASM_REAL_ARITH_TAC);\r
3325  (ASM_REWRITE_TAC[VECTOR_ARITH `x % (y/x % a + z/x % b) = (x/x) % (y %a + z % b)`]);\r
3326  (REWRITE_WITH `(u+v)/(u+v) = &1 /\ (w+z)/(w+z) = &1`);\r
3327  (STRIP_TAC);\r
3328  (MATCH_MP_TAC REAL_DIV_REFL);\r
3329  (ASM_REWRITE_TAC[]);\r
3330  (MATCH_MP_TAC REAL_DIV_REFL);\r
3331  (ASM_REWRITE_TAC[]);\r
3332  (VECTOR_ARITH_TAC);\r
3333  (EXISTS_TAC `u / (u + v)` THEN EXISTS_TAC `v / (u + v)`);\r
3334  (ASM_REWRITE_TAC[]);\r
3335  (REPEAT STRIP_TAC);\r
3336  (MATCH_MP_TAC REAL_LE_DIV);\r
3337  (ASM_REAL_ARITH_TAC);\r
3338  (MATCH_MP_TAC REAL_LE_DIV);\r
3339  (ASM_REAL_ARITH_TAC);\r
3340  (REWRITE_TAC[REAL_ARITH `u /(u + v) + v / (u + v) = (u+v)/(u+v)`]);\r
3341  (MATCH_MP_TAC REAL_DIV_REFL);\r
3342  (ASM_REWRITE_TAC[]);\r
3343 \r
3344  (EXISTS_TAC `w / (w + z)` THEN EXISTS_TAC `z / (w + z)`);\r
3345  (ASM_REWRITE_TAC[]);\r
3346  (REPEAT STRIP_TAC);\r
3347  (MATCH_MP_TAC REAL_LE_DIV);\r
3348  (ASM_REAL_ARITH_TAC);\r
3349  (MATCH_MP_TAC REAL_LE_DIV);\r
3350  (ASM_REAL_ARITH_TAC);\r
3351  (REWRITE_TAC[REAL_ARITH `u /(u + v) + v / (u + v) = (u+v)/(u+v)`]);\r
3352  (MATCH_MP_TAC REAL_DIV_REFL);\r
3353  (ASM_REWRITE_TAC[])]);;\r
3354 \r
3355 (* ======================================================================= *)\r
3356 (* Lemma 48 *)\r
3357 let proj_point = new_definition \r
3358 `!e x. proj_point e x = x - projection e x`;;\r
3359 \r
3360 let projection_proj_point = prove_by_refinement (\r
3361  `!e x. projection e x = x - proj_point e x`, \r
3362 [ REWRITE_TAC[proj_point] THEN VECTOR_ARITH_TAC]);;\r
3363 \r
3364 let PRO_EXP = prove_by_refinement(\r
3365  `!e x. proj_point e x = (x dot e) / (e dot e) % e`, \r
3366 [REWRITE_TAC[projection;proj_point] THEN VECTOR_ARITH_TAC]);;\r
3367 \r
3368 (* ======================================================================= *)\r
3369 (* Lemma 49 *)\r
3370 let BETWEEN_PROJ_POINT = prove_by_refinement (\r
3371  `!a b x e. between x (a,b) ==> \r
3372    between (proj_point e x) (proj_point e a, proj_point e b)`,\r
3373 [(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN;IN_ELIM_THM; PRO_EXP]);\r
3374  (REPEAT STRIP_TAC THEN EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real`);\r
3375  (ASM_REWRITE_TAC[]);\r
3376  (REWRITE_TAC[VECTOR_MUL_ASSOC; \r
3377    VECTOR_ARITH `x % a = m % a + n % a <=> (x -m - n) % a = vec 0`;\r
3378    REAL_ARITH `a / x - u * b / x - v * c / x = (a - u*b - v*c) / x`]);\r
3379  (REWRITE_TAC[VECTOR_ARITH \r
3380   `(u % a + v % b) dot e - u * (a dot e) - v * (b dot e) = &0`]);\r
3381  (REWRITE_TAC[REAL_ARITH `&0/a = &0`]);\r
3382  (VECTOR_ARITH_TAC)]);;\r
3383 \r
3384 (* ======================================================================= *)\r
3385 (* Lemma 50 *)\r
3386 let PARALLEL_PROJECTION = prove_by_refinement (\r
3387  `!x y a:real^N b. between x (a, y) /\ ~(a = b) \r
3388   ==> (?k. k <= &1 /\ &0 <= k /\\r
3389            projection (b - a) (x - a) = k % projection (b - a) (y - a))`,\r
3390 [(REWRITE_TAC[projection; BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]\r
3391    THEN REPEAT STRIP_TAC);\r
3392  (NEW_GOAL `(x - a) = v % (y - a:real^N)`);\r
3393  (REWRITE_WITH `x - a:real^N = (u % a + v % y) - (u + v) % a`);\r
3394  (ASM_REWRITE_TAC[]);\r
3395  (VECTOR_ARITH_TAC);\r
3396  (VECTOR_ARITH_TAC);\r
3397  (ASM_CASES_TAC `((y - a:real^N) dot (b - a) = &0)`);\r
3398  (EXISTS_TAC `v:real`);\r
3399  (REPEAT STRIP_TAC);\r
3400  (ASM_REAL_ARITH_TAC);\r
3401  (ASM_REAL_ARITH_TAC);\r
3402  (ASM_REWRITE_TAC[DOT_LMUL;REAL_MUL_RZERO;Collect_geom.REAL_DIV_LZERO;\r
3403    VECTOR_MUL_LZERO; VECTOR_SUB_RZERO]);\r
3404  (EXISTS_TAC `((x - a) dot (b - a)) / ((y - a) dot (b - a:real^N))`);\r
3405  (REPEAT STRIP_TAC);\r
3406  (ASM_REWRITE_TAC[DOT_LMUL; REAL_ARITH `(a * b) / c = a * (b / c)`]);\r
3407  (REWRITE_WITH `((y - a) dot (b - a)) / ((y - a) dot (b - a:real^N)) = &1`);\r
3408  (MATCH_MP_TAC REAL_DIV_REFL);\r
3409  (ASM_REWRITE_TAC[]);\r
3410  (ASM_REAL_ARITH_TAC);\r
3411  (ASM_REWRITE_TAC[DOT_LMUL; REAL_ARITH `(a * b) / c = a * (b / c)`]);\r
3412  (REWRITE_WITH `((y - a) dot (b - a)) / ((y - a) dot (b - a:real^N)) = &1`);\r
3413  (MATCH_MP_TAC REAL_DIV_REFL);\r
3414  (ASM_REWRITE_TAC[]);\r
3415  (ASM_REAL_ARITH_TAC);\r
3416  (REWRITE_WITH `((x - a) dot (b - a)) / ((y - a) dot (b - a:real^N)) %\r
3417  ((y - a):real^N - ((y - a) dot (b - a)) / ((b - a) dot (b - a)) % \r
3418  (b - a:real^N)) = \r
3419  &1 / ((y - a) dot (b - a)) %\r
3420  ((x - a) dot (b - a)) % (((y - a) - ((y - a) dot (b - a)) / ((b - a) dot \r
3421  (b - a)) % (b - a)))`);\r
3422  (VECTOR_ARITH_TAC);\r
3423  (MATCH_MP_TAC Trigonometry2.VECTOR_MUL_R_TO_L);\r
3424  (REPEAT STRIP_TAC);\r
3425  (ASM_MESON_TAC[]);\r
3426  (ABBREV_TAC `m = (y - a) dot (b - a:real^N)`);\r
3427  (ABBREV_TAC `n = (x - a) dot (b - a:real^N)`);\r
3428  (ABBREV_TAC `p = (b - a) dot (b - a:real^N)`);\r
3429  (REWRITE_TAC[VECTOR_ARITH \r
3430   `m % (x - n / p % (b - a)) = n % (y - m / p % (b - a)) <=> m % x = n % y`]);\r
3431  (EXPAND_TAC "m" THEN EXPAND_TAC "n");\r
3432  (REWRITE_TAC[ASSUME `x - a = v % (y - a:real^N)`; VECTOR_MUL_ASSOC]);\r
3433  (AP_THM_TAC THEN AP_TERM_TAC);\r
3434  (VECTOR_ARITH_TAC)]);;\r
3435 \r
3436 (* ======================================================================= *)\r
3437 (* Lemma 51 *)\r
3438 let NORM_PROJECTION_LE = prove_by_refinement(\r
3439  `!x y a:real^N b. between x (a, y) /\ ~(a = b) \r
3440   ==> norm (projection (b - a) (x - a)) <= norm (projection (b - a) (y - a))`,\r
3441 [(REPEAT GEN_TAC THEN DISCH_TAC);\r
3442  (SUBGOAL_THEN \r
3443   `(?k. k <= &1 /\ &0 <= k /\\r
3444         projection (b - a) (x - a:real^N) = k % projection (b - a) (y - a))`\r
3445    CHOOSE_TAC);\r
3446  (ASM_SIMP_TAC[PARALLEL_PROJECTION]);\r
3447  (ASM_REWRITE_TAC[NORM_MUL]);\r
3448  (REWRITE_WITH `abs k = k`);\r
3449  (ASM_SIMP_TAC[REAL_ABS_REFL]);\r
3450  (REWRITE_TAC[REAL_ARITH `a * b <= b <=> &0 <= (&1 - a) * b`]);\r
3451  (MATCH_MP_TAC REAL_LE_MUL);\r
3452  (STRIP_TAC);\r
3453  (ASM_REAL_ARITH_TAC);\r
3454  (REWRITE_TAC[NORM_POS_LE])]);;\r
3455 \r
3456 (* ======================================================================= *)\r
3457 (* Lemma 52 *)\r
3458 let OMEGA_LIST_TRUNCATE_1_NEW1 = prove_by_refinement (\r
3459  `!V u0:real^3 u1 u2 u3. \r
3460      omega_list_n V [u0;u1;u2] 1 = omega_list V [u0;u1] `,\r
3461 [ (REPEAT GEN_TAC);\r
3462  (REWRITE_TAC[OMEGA_LIST]);\r
3463  (REWRITE_WITH `LENGTH [u0:real^3;u1] - 1 = 1`);\r
3464  (REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC 0) - 1 = 1`]);\r
3465  (REWRITE_TAC[ARITH_RULE `1 = SUC 0`; OMEGA_LIST_N]);\r
3466  (REWRITE_TAC[ARITH_RULE `SUC 0 = 1`;TRUNCATE_SIMPLEX_EXPLICIT_1;HD])]);;\r
3467 \r
3468 let OMEGA_LIST_TRUNCATE_1_NEW2 = prove_by_refinement (\r
3469  `!V u0:real^3 u1 u2 u3. \r
3470      omega_list_n V [u0;u1] 1 = omega_list V [u0;u1] `,\r
3471 [ (REPEAT GEN_TAC);\r
3472  (REWRITE_TAC[OMEGA_LIST]);\r
3473  (REWRITE_WITH `LENGTH [u0:real^3;u1] - 1 = 1`);\r
3474  (REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC 0) - 1 = 1`])]);;\r
3475 \r
3476 let OMEGA_LIST_TRUNCATE_2_NEW1 = prove_by_refinement (\r
3477  `!V u0:real^3 u1 u2 u3. \r
3478      omega_list_n V [u0;u1;u2:real^3] 2 = omega_list V [u0;u1;u2]`,\r
3479 [(REPEAT GEN_TAC);\r
3480  (REWRITE_TAC[OMEGA_LIST]);\r
3481  (REWRITE_WITH `LENGTH [u0:real^3;u1;u2] - 1 = 2`);\r
3482  (REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC 0)) - 1 = 2`])]);;\r
3483 \r
3484 (* ======================================================================= *)\r
3485 (* Lemma 53 *)\r
3486 let IN_AFFINE_KY_LEMMA1 = prove_by_refinement (\r
3487  `!x s. x IN s ==> x IN affine hull s`,\r
3488 [(REPEAT STRIP_TAC);\r
3489  (REWRITE_TAC[affine;hull;IN_INTERS]);\r
3490  (REWRITE_TAC[IN;IN_ELIM_THM]);\r
3491  (REPEAT STRIP_TAC);\r
3492  (UP_ASM_TAC THEN SWITCH_TAC THEN UP_ASM_TAC THEN SET_TAC[])]);;\r
3493 \r
3494 (* ======================================================================= *)\r
3495 (* Lemma 54 *)\r
3496 let AFFINE_SUBSET_KY_LEMMA = prove_by_refinement (\r
3497 `!S B:real^N ->bool. S SUBSET B ==> affine hull S SUBSET affine hull B`,\r
3498 [(REWRITE_TAC[SUBSET;AFFINE_HULL_EXPLICIT; IN;IN_ELIM_THM] THEN \r
3499   REPEAT STRIP_TAC);\r
3500  (EXISTS_TAC `s:real^N->bool`);\r
3501  (EXISTS_TAC `u:real^N->real`);\r
3502  (ASM_REWRITE_TAC[]);\r
3503  (ASM_MESON_TAC[])]);;\r
3504 \r
3505 (* ======================================================================= *)\r
3506 (* Lemma 55 *)\r
3507 let TRANSLATE_AFFINE_KY_LEMMA1 = prove_by_refinement(\r
3508  `!a:real^3 b c x y z k. \r
3509      a IN affine hull {x,y,z} /\ \r
3510      b IN affine hull {x,y,z} /\ \r
3511      c IN affine hull {x,y,z} \r
3512    ==> a + k % (b - c) IN affine hull {x,y,z}`,\r
3513 [(REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);\r
3514  (EXISTS_TAC `u + k * (u' - u'')`);\r
3515  (EXISTS_TAC `v + k * (v' - v'')`);\r
3516  (EXISTS_TAC `w + k * (w' - w'')`);\r
3517  (STRIP_TAC);\r
3518  (REWRITE_WITH \r
3519   `(u + k * (u' - u'')) + (v + k * (v' - v'')) + w + k * (w' - w'') = \r
3520    (u + v + w)  + k * (u' + v' + w') - k * (u'' + v'' + w'')`);\r
3521  (REAL_ARITH_TAC);\r
3522  (ASM_REWRITE_TAC[REAL_SUB_REFL;REAL_ADD_RID]);\r
3523  (ASM_REWRITE_TAC[]);\r
3524  (VECTOR_ARITH_TAC)]);;\r
3525 \r
3526 (* ======================================================================= *)\r
3527 (* Lemma 56 *)\r
3528 let IN_AFFINE_HULL_KY_LEMMA3 = prove_by_refinement (\r
3529  `!x:real^3 y z p a r.\r
3530          p + a IN affine hull {x,y,z} /\ \r
3531          p + r % a IN affine hull  {x,y,z} /\ \r
3532          ~(r = &1) \r
3533       ==> p IN affine hull  {x,y,z}`,\r
3534 [(REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);\r
3535  (EXISTS_TAC `u + (u' - u) / (&1 - r)`);\r
3536  (EXISTS_TAC `v + (v' - v) / (&1 - r)`);\r
3537  (EXISTS_TAC `w + (w' - w) / (&1 - r)`);\r
3538  (STRIP_TAC);\r
3539  (REWRITE_TAC [REAL_ARITH \r
3540  `(u + (u' - u) / (&1 - r)) + (v + (v' - v) / (&1 - r)) + \r
3541   w + (w' - w) / (&1 - r) \r
3542   = (u + v + w) + ((u' + v' + w') - (u + v + w))/ (&1 - r)`]);\r
3543  (ASM_REWRITE_TAC[]);\r
3544  (REAL_ARITH_TAC);\r
3545  (REWRITE_WITH \r
3546 `(u + (u' - u) / (&1 - r)) % (x:real^3) +\r
3547  (v + (v' - v) / (&1 - r)) % y +\r
3548  (w + (w' - w) / (&1 - r)) % z = \r
3549  (p + a) - (&1/(&1 - r)) % ((p + a) - (p + r % a))`);\r
3550  (ASM_REWRITE_TAC[]);\r
3551  (VECTOR_ARITH_TAC);\r
3552  (REWRITE_TAC[VECTOR_ARITH \r
3553  `p = (p + a) - &1 / (&1 - r) % ((p + a) - (p + r % a)) \r
3554   <=>  ((&1 - r) / (&1 - r) - &1) % a = vec 0`]);\r
3555  (REWRITE_WITH `(&1 - r) / (&1 - r) = &1`);\r
3556 \r
3557  (MATCH_MP_TAC REAL_DIV_REFL);\r
3558  (ASM_REAL_ARITH_TAC);\r
3559  (REWRITE_TAC[REAL_SUB_REFL;VECTOR_MUL_LZERO])]);; \r
3560 \r
3561 let IN_AFFINE_HULL_KY_LEMMA3_alt = prove_by_refinement (\r
3562  `!x:real^3 y z p a r.\r
3563          p - a IN affine hull {x, y, z} /\\r
3564          p - r % a IN affine hull {x, y, z} /\\r
3565          ~(r = &1)\r
3566          ==> p IN affine hull {x, y, z}`,\r
3567 [(REWRITE_TAC[VECTOR_ARITH `p - a:real^3 = p + (-- a)`; \r
3568   VECTOR_ARITH `--(r % a) = r % (-- a)`]);\r
3569  (REWRITE_TAC[IN_AFFINE_HULL_KY_LEMMA3])]);;\r
3570 \r
3571 (* ======================================================================= *)\r
3572 (* Lemma 57 *)\r
3573 let IN_AFFINE_HULL_3_KY_LEMMA2 = prove_by_refinement (\r
3574  `!X Y Z a b c. X IN affine hull {a,b,c} /\ \r
3575                            Y IN affine hull {a,b,c} /\ \r
3576                            between Z (X,Y)\r
3577                 ==> Z IN affine hull {a,b,c:real^3}`,\r
3578 [(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;\r
3579   AFFINE_HULL_3;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);\r
3580  (EXISTS_TAC `u'' * u + v'' * u'`);\r
3581  (EXISTS_TAC `u'' * v + v'' * v'`);\r
3582  (EXISTS_TAC `u'' * w + v'' * w'`);\r
3583  (STRIP_TAC);\r
3584  (REWRITE_TAC[REAL_ARITH \r
3585  `(a * x + b * x') + (a * y + b * y') + (a * z + b * z') = \r
3586   a * (x + y + z) + b * (x' + y' + z')`]);\r
3587  (ASM_REWRITE_TAC[]);\r
3588  (ASM_REAL_ARITH_TAC);\r
3589  (ASM_REWRITE_TAC[]);\r
3590  (VECTOR_ARITH_TAC)]);;\r
3591 \r
3592 (* ======================================================================= *)\r
3593 (* Lemma 58 *)\r
3594 let SUM_CLAUSES_alt = prove (`(!x f s.\r
3595           FINITE s\r
3596           ==> sum (x INSERT s) f =\r
3597               (if x IN s then sum s f else f x + sum s f))`, REWRITE_TAC[SUM_CLAUSES]);;\r
3598 \r
3599 let SUM_DIS4 = prove_by_refinement (\r
3600  `!x:A y z t f. CARD {x,y, z, t} = 4 \r
3601    ==> sum {x,y,z,t} f = f x + f y + f z + f t`,\r
3602 [(REPEAT STRIP_TAC);\r
3603  (REWRITE_WITH `sum {x,y, z, t} f =\r
3604                  (if x IN {y, z, t:A} then sum {y, z, t} f \r
3605                   else f x + sum {y, z, t} f)`);\r
3606  (MATCH_MP_TAC SUM_CLAUSES_alt);\r
3607  (REWRITE_TAC[Geomdetail.FINITE6]);(COND_CASES_TAC);(NEW_GOAL `F`);\r
3608  (UP_ASM_TAC THEN REWRITE_TAC\r
3609   [SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`]); \r
3610  (REPEAT STRIP_TAC);\r
3611  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC\r
3612  [SET_RULE `{y,y,z,t} = {y,z,t}`] THEN STRIP_TAC);\r
3613  (NEW_GOAL `CARD {y, z, t:A} <= 3`);\r
3614  (REWRITE_TAC[Geomdetail.CARD3]);\r
3615  (ASM_ARITH_TAC);\r
3616  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC\r
3617  [SET_RULE `{z,y,z,t} = {y,z,t}`] THEN STRIP_TAC);\r
3618  (NEW_GOAL `CARD {y, z, t:A} <= 3`);\r
3619  (REWRITE_TAC[Geomdetail.CARD3]);\r
3620  (ASM_ARITH_TAC);\r
3621  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC\r
3622  [SET_RULE `{t,y,z,t} = {y,z,t}`] THEN STRIP_TAC);\r
3623  (NEW_GOAL `CARD {y, z, t:A} <= 3`);\r
3624  (REWRITE_TAC[Geomdetail.CARD3]);\r
3625  (ASM_ARITH_TAC);\r
3626  (ASM_MESON_TAC[]);\r
3627  (REWRITE_WITH `sum {y, z, t} f =\r
3628                  (if y IN {z, t:A} then sum {z, t} f \r
3629                   else f y + sum {z, t} f)`);\r
3630  (MATCH_MP_TAC SUM_CLAUSES_alt);\r
3631  (REWRITE_TAC[Geomdetail.FINITE6]);\r
3632  SWITCH_TAC; \r
3633  (COND_CASES_TAC);\r
3634  (NEW_GOAL `F`);\r
3635  (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE `x IN {a,b} <=> x = a \/ x = b`]);\r
3636  (REPEAT STRIP_TAC);\r
3637  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[SET_RULE `{x,z,z,t} = {x,z,t}`] THEN STRIP_TAC);\r
3638  (NEW_GOAL `CARD {x, z, t:A} <= 3`);\r
3639  (REWRITE_TAC[Geomdetail.CARD3]);\r
3640  (ASM_ARITH_TAC);\r
3641  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[SET_RULE `{x,t,z,t} = {x,z,t}`] THEN STRIP_TAC);\r
3642  (NEW_GOAL `CARD {x, z, t:A} <= 3`);\r
3643  (REWRITE_TAC[Geomdetail.CARD3]);\r
3644  (ASM_ARITH_TAC);\r
3645  (ASM_MESON_TAC[]);\r
3646  SWITCH_TAC;\r
3647  (REWRITE_WITH `sum {z, t:A} f = f z + f t`);\r
3648  (MATCH_MP_TAC Collect_geom.SUM_DIS2 THEN STRIP_TAC);\r
3649  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[SET_RULE `{x,y,t,t} = {x,y,t}`] THEN STRIP_TAC);\r
3650  (NEW_GOAL `CARD {x, y, t:A} <= 3`);\r
3651  (REWRITE_TAC[Geomdetail.CARD3]);\r
3652  (ASM_ARITH_TAC)]);;\r
3653 \r
3654 (* ======================================================================= *)\r
3655 (* Lemma 59 *)\r
3656 let CARD4_IMP_DISTINCT = prove (\r
3657  `!a b c d. CARD {a, b, c, d} = 4 ==> ~(a = b)`,\r
3658  (REPEAT STRIP_TAC THEN SWITCH_TAC THEN UP_ASM_TAC THEN \r
3659    ASM_REWRITE_TAC[SET_RULE `{a,a,c,d} = {a,c,d}`] THEN STRIP_TAC) THEN\r
3660  (ASM_MESON_TAC[Geomdetail.CARD3; ARITH_RULE `~(4 <= 3)`]));;\r
3661 \r
3662 (* ======================================================================= *)\r
3663 (* Lemma 60 *)\r
3664 let VSUM_CLAUSES_alt = prove (`(!x f s.\r
3665           FINITE s\r
3666           ==> vsum (x INSERT s) f =\r
3667               (if x IN s then vsum s f else f x + vsum s f))`, REWRITE_TAC[VSUM_CLAUSES]);;\r
3668 let VSUM_DIS4 = prove_by_refinement (\r
3669  `!x:A y z t (f:A->real^N). CARD {x,y, z, t} = 4 \r
3670    ==> vsum {x,y,z,t} f = f x + f y + f z + f t`,\r
3671 [(REPEAT STRIP_TAC);\r
3672  (REWRITE_WITH `vsum {x,y, z, t} (f:A->real^N) =\r
3673                  (if x IN {y, z, t:A} then vsum {y, z, t} f \r
3674                   else f x + vsum {y, z, t} f)`);\r
3675  (MATCH_MP_TAC VSUM_CLAUSES_alt);\r
3676  (REWRITE_TAC[Geomdetail.FINITE6]);(COND_CASES_TAC);(NEW_GOAL `F`);\r
3677  (UP_ASM_TAC THEN REWRITE_TAC\r
3678   [SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`]); \r
3679  (REPEAT STRIP_TAC);\r
3680  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC\r
3681  [SET_RULE `{y,y,z,t} = {y,z,t}`] THEN STRIP_TAC);\r
3682  (NEW_GOAL `CARD {y, z, t:A} <= 3`);\r
3683  (REWRITE_TAC[Geomdetail.CARD3]);\r
3684  (ASM_ARITH_TAC);\r
3685  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC\r
3686  [SET_RULE `{z,y,z,t} = {y,z,t}`] THEN STRIP_TAC);\r
3687  (NEW_GOAL `CARD {y, z, t:A} <= 3`);\r
3688  (REWRITE_TAC[Geomdetail.CARD3]);\r
3689  (ASM_ARITH_TAC);\r
3690  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC\r
3691  [SET_RULE `{t,y,z,t} = {y,z,t}`] THEN STRIP_TAC);\r
3692  (NEW_GOAL `CARD {y, z, t:A} <= 3`);\r
3693  (REWRITE_TAC[Geomdetail.CARD3]);\r
3694  (ASM_ARITH_TAC);\r
3695  (ASM_MESON_TAC[]);\r
3696  (REWRITE_WITH `vsum {y, z, t} (f:A->real^N) =\r
3697                  (if y IN {z, t:A} then vsum {z, t} f \r
3698                   else f y + vsum {z, t} f)`);\r
3699  (MATCH_MP_TAC VSUM_CLAUSES_alt);\r
3700  (REWRITE_TAC[Geomdetail.FINITE6]);\r
3701  SWITCH_TAC; \r
3702  (COND_CASES_TAC);\r
3703  (NEW_GOAL `F`);\r
3704  (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE `x IN {a,b} <=> x = a \/ x = b`]);\r
3705  (REPEAT STRIP_TAC);\r
3706  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[SET_RULE `{x,z,z,t} = {x,z,t}`] THEN STRIP_TAC);\r
3707  (NEW_GOAL `CARD {x, z, t:A} <= 3`);\r
3708  (REWRITE_TAC[Geomdetail.CARD3]);\r
3709  (ASM_ARITH_TAC);\r
3710  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[SET_RULE `{x,t,z,t} = {x,z,t}`] THEN STRIP_TAC);\r
3711  (NEW_GOAL `CARD {x, z, t:A} <= 3`);\r
3712  (REWRITE_TAC[Geomdetail.CARD3]);\r
3713  (ASM_ARITH_TAC);\r
3714  (ASM_MESON_TAC[]);\r
3715  SWITCH_TAC;\r
3716  (REWRITE_WITH `vsum {z, t:A} (f:A->real^N) = f z + f t`);\r
3717  (MATCH_MP_TAC Collect_geom.VSUM_DIS2 THEN STRIP_TAC);\r
3718  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[SET_RULE `{x,y,t,t} = {x,y,t}`] THEN STRIP_TAC);\r
3719  (NEW_GOAL `CARD {x, y, t:A} <= 3`);\r
3720  (REWRITE_TAC[Geomdetail.CARD3]);\r
3721  (ASM_ARITH_TAC)]);;\r
3722 \r
3723 (* ======================================================================= *)\r
3724 (* Lemma 61 *)\r
3725 let AFFINE_DEPENDENT_KY_LEMMA1 = prove_by_refinement (\r
3726  `!a:real^3 b c d p:real^3 k1 k2 k3 k4.\r
3727     ~(affine_dependent {a,b,c,d}) /\\r
3728      CARD {a,b,c,d} = 4 /\ \r
3729      p IN convex hull {a,b,c,d} /\\r
3730      k1 + k2 + k3 + k4 = &1 /\    \r
3731      p = k1 % a + k2 % b + k3 % c + k4 % d /\ \r
3732      k1 <= &0 ==> k1 = &0`,\r
3733 [(REPEAT GEN_TAC);\r
3734  (REWRITE_TAC[CONVEX_HULL_4; IN;IN_ELIM_THM]);\r
3735  (REPEAT STRIP_TAC);\r
3736  (ASM_CASES_TAC `k1 = &0`);\r
3737  (ASM_REWRITE_TAC[]);\r
3738  (NEW_GOAL `F`);\r
3739  (NEW_GOAL `affine_dependent {a,b,c,d:real^3}`);\r
3740  (REWRITE_TAC[AFFINE_DEPENDENT_EXPLICIT]);\r
3741  (EXISTS_TAC `{a,b,c,d:real^3}`);\r
3742  (ABBREV_TAC `f = (\x:real^3. if x = a then u - k1 else\r
3743                         if x = b then v - k2 else \r
3744                         if x = c then w - k3 else \r
3745                         if x = d then z - k4 else &0)`);\r
3746  (EXISTS_TAC `f:real^3->real`);\r
3747 \r
3748  (NEW_GOAL `f (a:real^3) = u - k1`);\r
3749  (EXPAND_TAC "f");\r
3750  (COND_CASES_TAC);\r
3751  (REWRITE_TAC[]);\r
3752  (NEW_GOAL `F`);\r
3753  (ASM_MESON_TAC[]);\r
3754  (ASM_MESON_TAC[]);\r
3755 \r
3756  (NEW_GOAL `f (b:real^3) = v - k2`);\r
3757  (EXPAND_TAC "f");\r
3758  (COND_CASES_TAC);\r
3759  (NEW_GOAL `F` THEN UP_ASM_TAC THEN REWRITE_TAC[]);\r
3760  (MATCH_MP_TAC CARD4_IMP_DISTINCT);\r
3761  (EXISTS_TAC `c:real^3` THEN EXISTS_TAC `d:real^3`);\r
3762  (ASM_REWRITE_TAC[SET_RULE `{a,b,c,d} = {b,a,c,d}`]);\r
3763  (COND_CASES_TAC);\r
3764  (REWRITE_TAC[]);\r
3765  (NEW_GOAL `F`);\r
3766  (ASM_MESON_TAC[]);\r
3767  (ASM_MESON_TAC[]);\r
3768 \r
3769  (NEW_GOAL `f (c:real^3) = w - k3`);\r
3770  (EXPAND_TAC "f");\r
3771  (COND_CASES_TAC);\r
3772  (NEW_GOAL `F` THEN UP_ASM_TAC THEN REWRITE_TAC[]);\r
3773  (MATCH_MP_TAC CARD4_IMP_DISTINCT);\r
3774  (EXISTS_TAC `b:real^3` THEN EXISTS_TAC `d:real^3`);\r
3775  (ASM_REWRITE_TAC[SET_RULE `{c,a,b,d} = {a,b,c,d}`]);\r
3776  (COND_CASES_TAC);\r
3777  (NEW_GOAL `F` THEN UP_ASM_TAC THEN REWRITE_TAC[]);\r
3778  (MATCH_MP_TAC CARD4_IMP_DISTINCT);\r
3779  (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `d:real^3`);\r
3780  (ASM_REWRITE_TAC[SET_RULE `{c,b,a,d} = {a,b,c,d}`]);\r
3781  (COND_CASES_TAC);\r
3782  (REWRITE_TAC[]);\r
3783  (NEW_GOAL `F`);\r
3784  (ASM_MESON_TAC[]);\r
3785  (ASM_MESON_TAC[]);\r
3786 \r
3787  (NEW_GOAL `f (d:real^3) = z - k4`);\r
3788  (EXPAND_TAC "f");\r
3789  (COND_CASES_TAC);\r
3790  (NEW_GOAL `F` THEN UP_ASM_TAC THEN REWRITE_TAC[]);\r
3791  (MATCH_MP_TAC CARD4_IMP_DISTINCT);\r
3792  (EXISTS_TAC `c:real^3` THEN EXISTS_TAC `b:real^3`);\r
3793  (ASM_REWRITE_TAC[SET_RULE `{d,a,c, b} = {a,b,c,d}`]);\r
3794  (COND_CASES_TAC);\r
3795  (NEW_GOAL `F` THEN UP_ASM_TAC THEN REWRITE_TAC[]);\r
3796  (MATCH_MP_TAC CARD4_IMP_DISTINCT);\r
3797  (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `c:real^3`);\r
3798  (ASM_REWRITE_TAC[SET_RULE `{d,b,a,c} = {a,b,c,d}`]);\r
3799  (COND_CASES_TAC);\r
3800  (NEW_GOAL `F` THEN UP_ASM_TAC THEN REWRITE_TAC[]);\r
3801  (MATCH_MP_TAC CARD4_IMP_DISTINCT);\r
3802  (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);\r
3803  (ASM_REWRITE_TAC[SET_RULE `{d,c,a,b} = {a,b,c,d}`]);\r
3804  (COND_CASES_TAC);\r
3805  (REWRITE_TAC[]);\r
3806  (NEW_GOAL `F`);\r
3807  (ASM_MESON_TAC[]);\r
3808  (ASM_MESON_TAC[]);\r
3809 \r
3810  (REPEAT STRIP_TAC);\r
3811  (REWRITE_TAC[Geomdetail.FINITE6]);\r
3812  (SET_TAC[]);\r
3813 \r
3814  (REWRITE_WITH `sum {a, b, c, d:real^3} f = f a + f b + f c + f d`);\r
3815  (MATCH_MP_TAC SUM_DIS4);\r
3816  (ASM_REWRITE_TAC[]);\r
3817  (ASM_REWRITE_TAC[]);\r
3818  (REWRITE_TAC[REAL_ARITH\r
3819   `a - x + b - y + c - z + d - t = (a + b + c + d) - (x + y + z + t)`]);\r
3820  (ASM_REWRITE_TAC[REAL_SUB_REFL]);\r
3821  (EXISTS_TAC `a:real^3`);\r
3822  (STRIP_TAC);\r
3823  (SET_TAC[]);\r
3824  (ASM_REWRITE_TAC[]);\r
3825  (ASM_REAL_ARITH_TAC);\r
3826 \r
3827  (REWRITE_WITH `vsum {a, b, c, d:real^3} (\v. f v % v) = \r
3828   (\v. f v % v) a + (\v. f v % v) b + (\v. f v % v) c + (\v. f v % v) d`);\r
3829  (MATCH_MP_TAC VSUM_DIS4);\r
3830  (ASM_REWRITE_TAC[]);\r
3831  (ASM_REWRITE_TAC[]);\r
3832  (REWRITE_TAC[VECTOR_ARITH `\r
3833   (u - k1) % a + (v - k2) % b + (w - k3) % c + (z - k4) % d = \r
3834   (u % a + v % b + w % c + z % d) - (k1 % a + k2 % b + k3 % c + k4 % d)`]);\r
3835  (ASM_MESON_TAC[VECTOR_ARITH `a:real^N - a = vec 0`]);\r
3836  (ASM_MESON_TAC[]);\r
3837  (ASM_MESON_TAC[])]);;\r
3838 \r
3839 (* ======================================================================= *)\r
3840 (* Lemma 62 *)\r
3841 let IN_2_2_IMP_CONVEX_HULL_4 = prove (\r
3842  `!a:real^N b x y m n p. \r
3843      between p (m,n) /\ between m (a,b) /\ between n (x,y)\r
3844      ==> p IN convex hull {a, b, x, y}`,\r
3845  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;CONVEX_HULL_4;\r
3846    IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC) THEN \r
3847  (ASM_REWRITE_TAC[]) THEN \r
3848  (EXISTS_TAC `u * u'` THEN EXISTS_TAC `u * v'`) THEN \r
3849  (EXISTS_TAC `v * u''` THEN EXISTS_TAC `v * v''`) THEN \r
3850  (ASM_SIMP_TAC[REAL_LE_MUL; REAL_ARITH `a * x + a * y + b * z + b * t = \r
3851    a * (x + y) + b * (z + t)`; REAL_MUL_RID]) THEN\r
3852  (VECTOR_ARITH_TAC));;\r
3853 \r
3854 (* ======================================================================= *)\r
3855 (* Lemma 63 *)\r
3856 let BETWEEN_TRANS_3_CASES = prove_by_refinement (\r
3857  `!a b x y:real^3. between x (a,b) /\ between y (a,b) ==> \r
3858                     between x (a, y) \/ between x (y, b) `,\r
3859 [(REPEAT STRIP_TAC);\r
3860  (ASM_CASES_TAC `(a = b:real^3)`);\r
3861  (UNDISCH_TAC `between x (a,b:real^3)`);\r
3862  (UNDISCH_TAC `between y (a,b:real^3)`);\r
3863  (ASM_REWRITE_TAC[BETWEEN_REFL_EQ]);\r
3864  (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[BETWEEN_REFL_EQ]);\r
3865 \r
3866  (ASM_CASES_TAC `between x (a,y:real^3)`);\r
3867  (ASM_MESON_TAC[]);\r
3868  (DISJ2_TAC);\r
3869  (ONCE_REWRITE_TAC[BETWEEN_SYM]);\r
3870  (MATCH_MP_TAC BETWEEN_TRANS_2);\r
3871  (EXISTS_TAC `a:real^3` THEN ASM_REWRITE_TAC[]);\r
3872  (NEW_GOAL `collinear {a,y,x:real^3}`);\r
3873  (ONCE_REWRITE_TAC[SET_RULE `{a,y,x} = {x, a ,y}`]);\r
3874  (MATCH_MP_TAC COLLINEAR_3_TRANS);\r
3875  (EXISTS_TAC `b:real^3`);\r
3876  (REPEAT STRIP_TAC);\r
3877  (ONCE_REWRITE_TAC[SET_RULE `{x,a, b} = {a, x, b}`]);\r
3878  (MATCH_MP_TAC BETWEEN_IMP_COLLINEAR);\r
3879  (ASM_REWRITE_TAC[]);\r
3880  (ONCE_REWRITE_TAC[SET_RULE `{a, b,y} = {a, y, b}`]);\r
3881  (MATCH_MP_TAC BETWEEN_IMP_COLLINEAR);\r
3882  (ASM_REWRITE_TAC[]);\r
3883  (ASM_MESON_TAC[]);\r
3884  (UP_ASM_TAC THEN REWRITE_TAC[COLLINEAR_BETWEEN_CASES]);\r
3885 \r
3886  (ASM_CASES_TAC `between y (x,a:real^3)`);\r
3887  (STRIP_TAC THEN ASM_REWRITE_TAC[]);\r
3888  (ONCE_REWRITE_TAC[MESON[] `(A\/B\/C ==> B) <=> (C\/A ==> B)`]);\r
3889  (REPEAT STRIP_TAC);\r
3890  (NEW_GOAL `F`);\r
3891  (ASM_MESON_TAC[]);\r
3892  (ASM_MESON_TAC[]);\r
3893  (ASM_CASES_TAC `x = y:real^3`);\r
3894  (REWRITE_TAC[ASSUME `x = y:real^3`; BETWEEN_REFL]);\r
3895 \r
3896  (NEW_GOAL `F`);\r
3897  (UNDISCH_TAC `between x (a,b:real^3)` THEN \r
3898    UNDISCH_TAC `between y (a,b:real^3)` THEN \r
3899    UNDISCH_TAC `between a (y,x:real^3)`);\r
3900  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);  \r
3901  (REPEAT STRIP_TAC);\r
3902 \r
3903  (MP_TAC (ASSUME `a = u % y + v % x:real^3`));\r
3904  (REWRITE_TAC[ASSUME `y = u' % a + v' % b:real^3`; \r
3905    ASSUME `x = u'' % a + v'' % b:real^3`]);\r
3906 \r
3907  (REWRITE_WITH `v' = &1 - u' /\ v = &1 - u /\ v'' = &1 - u''`);\r
3908  (ASM_REAL_ARITH_TAC);\r
3909  (REWRITE_TAC [VECTOR_ARITH `\r
3910    a = u % (u' % a + (&1 - u') % b) + (&1 - u) % (u'' % a + (&1 - u'') % b) \r
3911    <=> (&1 - u * u' - (&1 - u) * u'') % (a - b) = vec 0`]);\r
3912  (REWRITE_TAC[VECTOR_MUL_EQ_0]);\r
3913  (ASM_REWRITE_TAC[VECTOR_ARITH `a - b = vec 0 <=> a = b`]);\r
3914  (REWRITE_TAC[REAL_ARITH \r
3915   `&1 - u * u' - (&1 - u) * u'' = u * (&1 - u') + (&1 - u) * (&1 - u'')`]);\r
3916  (NEW_GOAL `&0 <= u * (&1 - u')`);\r
3917  (MATCH_MP_TAC REAL_LE_MUL);\r
3918  (ASM_REAL_ARITH_TAC);\r
3919  (NEW_GOAL `&0 <= (&1 - u) * (&1 - u'')`);\r
3920  (MATCH_MP_TAC REAL_LE_MUL);\r
3921  (ASM_REAL_ARITH_TAC);\r
3922  (STRIP_TAC);\r
3923  (NEW_GOAL `u * (&1 - u') = &0 /\ (&1 - u) * (&1 - u'') = &0`);\r
3924  (ASM_REAL_ARITH_TAC);\r
3925  (UP_ASM_TAC THEN REWRITE_TAC[REAL_ENTIRE]);\r
3926  (REPEAT STRIP_TAC);\r
3927  (ASM_REAL_ARITH_TAC);\r
3928 \r
3929  (UNDISCH_TAC `~between x (a,y:real^3)`);\r
3930  (REWRITE_TAC[ASSUME `x = u'' % a + v'' % b:real^3`]);\r
3931  (REWRITE_WITH `u'' = &1 /\ v'' = &0`);\r
3932  (ASM_REAL_ARITH_TAC);\r
3933  (REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO;VECTOR_ADD_RID; BETWEEN_REFL]);\r
3934 \r
3935  (UNDISCH_TAC `~between y (x,a:real^3)`);\r
3936  (REWRITE_TAC[ASSUME `y = u' % a + v' % b:real^3`]);\r
3937  (REWRITE_WITH `u' = &1 /\ v' = &0`);\r
3938  (ASM_REAL_ARITH_TAC);\r
3939  (REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO;VECTOR_ADD_RID; BETWEEN_REFL]);\r
3940 \r
3941  (UNDISCH_TAC `~between y (x,a:real^3)`);\r
3942  (REWRITE_TAC[ASSUME `y = u' % a + v' % b:real^3`]);\r
3943  (REWRITE_WITH `u' = &1 /\ v' = &0`);\r
3944  (ASM_REAL_ARITH_TAC);\r
3945  (REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO;VECTOR_ADD_RID; BETWEEN_REFL]);\r
3946  (ASM_MESON_TAC[])]);;\r
3947 \r
3948 (* ======================================================================= *)\r
3949 (* Lemma 64 *)\r
3950 \r
3951 let OMEGA_LIST_UP_TO_2 = prove_by_refinement (\r
3952  `! V ul. {omega_list_n V ul i | i <= 2} = \r
3953    {omega_list_n V ul 0, omega_list_n V ul 1, omega_list_n V ul 2}`,\r
3954 [(REPEAT GEN_TAC);\r
3955  (REWRITE_WITH `{omega_list_n V ul i | i <= 2} = \r
3956    IMAGE (omega_list_n V ul) {i| i <= 2}`);\r
3957  (REWRITE_TAC[IMAGE] THEN SET_TAC[]);\r
3958  (REWRITE_WITH `\r
3959  {omega_list_n V ul 0, omega_list_n V ul 1, omega_list_n V ul 2}\r
3960   = IMAGE (omega_list_n V ul) {0,1,2}`);\r
3961  (REWRITE_TAC[IMAGE] THEN SET_TAC[]);\r
3962  (AP_TERM_TAC);\r
3963  (REWRITE_TAC[SET_OF_0_TO_2])]);;\r
3964 \r
3965 (* ======================================================================= *)\r
3966 (* Lemma 65 *)\r
3967 let CONVEX_HULL_KY_LEMMA_5 = prove_by_refinement (\r
3968  `!a:real^3 b c d x y d p. \r
3969       ~(affine_dependent {a,b,c,d}) /\ CARD {a,b,c,d} = 4 /\ ~(d = x) /\\r
3970        x IN convex hull {a,b,c} /\ between d (x,y) /\ \r
3971       ~( p IN affine hull {a,b,d}) /\ \r
3972        p IN convex hull {a,b,c,d} INTER convex hull {a,b,x,y} ==>\r
3973        p IN convex hull {a,b,x,d}`,\r
3974 [(REPEAT STRIP_TAC);\r
3975  (NEW_GOAL `p IN convex hull {a, b, x, y:real^3}`);\r
3976  (ASM_SET_TAC[IN_INTER]);\r
3977  (SUBGOAL_THEN `?m n:real^3. \r
3978    between p (m,n) /\ between m (a,b) /\ between n (x,y)` CHOOSE_TAC);  \r
3979   (ASM_SIMP_TAC[CONVEX_HULL_4_IMP_2_2]);\r
3980  (UP_ASM_TAC THEN REPEAT STRIP_TAC);\r
3981 \r
3982  (ASM_CASES_TAC `between n (x, d:real^3)`);\r
3983  (MATCH_MP_TAC IN_2_2_IMP_CONVEX_HULL_4);\r
3984  (EXISTS_TAC `m:real^3` THEN EXISTS_TAC `n:real^3`);\r
3985  (ASM_REWRITE_TAC[]);\r
3986 \r
3987  (NEW_GOAL `between n (x,d) \/ between n (d, y:real^3)`);\r
3988  (MATCH_MP_TAC BETWEEN_TRANS_3_CASES);\r
3989  (ASM_REWRITE_TAC[]);\r
3990  (NEW_GOAL `between n (d,y:real^3)`);\r
3991  (ASM_MESON_TAC[]);\r
3992 \r
3993  (NEW_GOAL `?k1 k2. n = k1 % d + k2 % x:real^3 /\ k1 + k2 = &1 /\ k2 <= &0`);\r
3994  (UP_ASM_TAC THEN UNDISCH_TAC `between d (x,y:real^3)`);\r
3995  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;IN;IN_ELIM_THM;CONVEX_HULL_2]);\r
3996  (REPEAT STRIP_TAC);\r
3997  (ASM_REWRITE_TAC[]);\r
3998  (EXISTS_TAC `u' + (v'/ v)`);\r
3999  (EXISTS_TAC `-- ((u * v')/ v)`);\r
4000  (REPEAT STRIP_TAC);\r
4001 \r
4002  (REWRITE_TAC[VECTOR_ARITH \r
4003   `u' % (u % x + v % y) + v' % y =  \r
4004    (u' + v' / v) % (u % x + v % y) + --((u * v') / v) % x \r
4005   <=> ((v /v - &1) * v') % y = vec 0`]);\r
4006  (REWRITE_WITH `v / v = &1`);\r
4007  (MATCH_MP_TAC REAL_DIV_REFL);\r
4008  (STRIP_TAC);\r
4009  (NEW_GOAL `d = x:real^3`);\r
4010  (REWRITE_TAC[ASSUME `d = u % x + v % y:real^3`]);\r
4011  (REWRITE_WITH `v = &0 /\ u = &1`);\r
4012  (ASM_REAL_ARITH_TAC);\r
4013  (VECTOR_ARITH_TAC);\r
4014  (ASM_MESON_TAC[]);\r
4015  (VECTOR_ARITH_TAC);\r
4016 \r
4017  (REWRITE_TAC[REAL_ARITH `(u' + v' / v) + --((u * v') / v) = \r
4018    u' + v' * ((&1 - u) / v)`]);\r
4019  (REWRITE_WITH `(&1 - u) / v = &1`);\r
4020  (REWRITE_WITH `&1 - u = v`);\r
4021  (ASM_REAL_ARITH_TAC);\r
4022  (MATCH_MP_TAC REAL_DIV_REFL);\r
4023  (STRIP_TAC);\r
4024  (NEW_GOAL `d = x:real^3`);\r
4025  (REWRITE_TAC[ASSUME `d = u % x + v % y:real^3`]);\r
4026  (REWRITE_WITH `v = &0 /\ u = &1`);\r
4027  (ASM_REAL_ARITH_TAC);\r
4028  (VECTOR_ARITH_TAC);\r
4029  (ASM_MESON_TAC[]);\r
4030  (ASM_REAL_ARITH_TAC);\r
4031  (REWRITE_TAC[REAL_ARITH `-- a <= &0 <=> &0 <= a`]);\r
4032  (MATCH_MP_TAC REAL_LE_DIV);\r
4033  (ASM_SIMP_TAC[REAL_LE_MUL]);\r
4034  (FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC);\r
4035 \r
4036  (UNDISCH_TAC `between p (m,n:real^3)`);\r
4037  (UNDISCH_TAC `between m (a,b:real^3)`);\r
4038  (UNDISCH_TAC `x IN convex hull {a,b,c:real^3}`);\r
4039  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;\r
4040    CONVEX_HULL_3;IN;IN_ELIM_THM]);\r
4041  (REPEAT STRIP_TAC);\r
4042  (NEW_GOAL `F`);\r
4043  (UP_ASM_TAC THEN ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);\r
4044  (REWRITE_TAC[VECTOR_ARITH \r
4045   `(x % a + y % b) + z % d + x' % a + y' % b + z' % c = \r
4046    z' % c + (x + x') % a + (y + y') % b + z % d`]);\r
4047 \r
4048  (REPEAT STRIP_TAC);\r
4049 \r
4050  (NEW_GOAL `v'' * k2 * w = &0`);\r
4051  (MATCH_MP_TAC AFFINE_DEPENDENT_KY_LEMMA1);\r
4052  (EXISTS_TAC `c:real^3` THEN EXISTS_TAC `a:real^3`);\r
4053  (EXISTS_TAC `b:real^3` THEN EXISTS_TAC `d:real^3`);\r
4054  (EXISTS_TAC `p:real^3`);\r
4055  (EXISTS_TAC `u'' * u' + v'' * k2 * u` THEN \r
4056    EXISTS_TAC `u'' * v' + v'' * k2 * v` THEN \r
4057    EXISTS_TAC `v'' * k1`);\r
4058  (STRIP_TAC);\r
4059  (ONCE_REWRITE_TAC[SET_RULE `{c,a,b,d} = {a,b,c,d}`]);\r
4060  (ASM_REWRITE_TAC[]);\r
4061  (REPEAT STRIP_TAC);\r
4062  (ONCE_REWRITE_TAC[SET_RULE `{c,a,b,d} = {a,b,c,d}`]);\r
4063  (ASM_REWRITE_TAC[]);\r
4064  (ONCE_REWRITE_TAC[SET_RULE `{c,a,b,d} = {a,b,c,d}`]);\r
4065  (ASM_SET_TAC[IN_INTER]);\r
4066  (REWRITE_TAC[REAL_ARITH \r
4067    `v'' * k2 * w + (u'' * u' + v'' * k2 * u) +\r
4068    (u'' * v' + v'' * k2 * v) +  v'' * k1 \r
4069     = u'' * (u' + v') +  v'' * (k1 + k2 * (u + v + w))`]);\r
4070  (ASM_REWRITE_TAC[REAL_MUL_RID]);\r
4071  (ASM_REWRITE_TAC[]);\r
4072  (REWRITE_TAC[REAL_ARITH `a * b * c <= &0 <=> &0 <= a * (-- b) * c`]);\r
4073  (MATCH_MP_TAC REAL_LE_MUL);\r
4074  (ASM_REWRITE_TAC[]);\r
4075  (MATCH_MP_TAC REAL_LE_MUL);\r
4076  (ASM_REWRITE_TAC[]);\r
4077  (ASM_REAL_ARITH_TAC);\r
4078  (NEW_GOAL `p IN affine hull {a,b,d:real^3}`);\r
4079  (REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);\r
4080  (EXISTS_TAC `u'' * u' + v'' * k2 * u` THEN \r
4081    EXISTS_TAC `u'' * v' + v'' * k2 * v` THEN \r
4082    EXISTS_TAC `v'' * k1`);\r
4083  (STRIP_TAC);\r
4084  (REWRITE_WITH `(u'' * u' + v'' * k2 * u) + (u'' * v' + v'' * k2 * v) + \r
4085    v'' * k1 = u'' * (u' + v') +  v'' * (k1 + k2 * (u + v + w)) - (v'' * k2 * w)`);\r
4086  (ASM_REAL_ARITH_TAC);\r
4087  (ASM_REWRITE_TAC[REAL_MUL_RID]);\r
4088  (ASM_REAL_ARITH_TAC);\r
4089  (ASM_REWRITE_TAC[]);\r
4090  (VECTOR_ARITH_TAC);\r
4091  (ASM_MESON_TAC[]);\r
4092  (ASM_MESON_TAC[])]);;\r
4093 \r
4094 (* ======================================================================= *)\r
4095 (* Lemma 66 *)\r
4096 (* ======================================================================= *)\r
4097 \r
4098 \r
4099 end;;\r
4100 \r