1 (* ========================================================================= *)
\r
2 (* FLYSPECK - BOOK FORMALIZATION *)
\r
4 (* Authour : VU KHAC KY *)
\r
5 (* Book lemma: SLTSTLO *)
\r
6 (* Chaper : Packing (Marchal Cells) *)
\r
7 (* Date : June - July 2011 *)
\r
9 (* ========================================================================= *)
\r
11 module Sltstlo = struct
\r
14 open Vukhacky_tactics;;
\r
19 open Marchal_cells;;
\r
20 open Marchal_cells_2_new;;
\r
25 let (tms,tm) = top_goal () in
\r
26 let vss = map frees (tm::tms) in
\r
27 let vs = setify (flat vss) in
\r
31 let NULLSET_SPHERE = prove_by_refinement
\r
32 (`(!P. (?(v:real^3)(r:real). (r> &0)/\ (P={w:real^3 | norm (w-v)= r})) ==> NULLSET P)`,
\r
34 X_GEN_TAC `s:real^3->bool` THEN STRIP_TAC;
\r
35 FIRST_X_ASSUM(MP_TAC);
\r
36 STRIP_TAC THEN ASM_REWRITE_TAC[GSYM dist] ;
\r
37 ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[NEGLIGIBLE_SPHERE];
\r
41 (* =========================================================================== *)
\r
43 let SLTSTLO1 = prove_by_refinement (
\r
46 [(REPEAT GEN_TAC THEN REPEAT STRIP_TAC);
\r
48 (* =================== Case 1 ============================================== *)
\r
50 (ASM_CASES_TAC `hl (ul:(real^3)list) < sqrt(&2)`);
\r
52 (REWRITE_TAC[ARITH_RULE `4 <= 4`]);
\r
54 (SUBGOAL_THEN `mcell4 V ul = convex hull (set_of_list (ul:(real^3)list))`
\r
57 (REWRITE_TAC[mcell4]);
\r
60 (SUBGOAL_THEN `F` ASSUME_TAC);
\r
61 (UP_ASM_TAC THEN UP_ASM_TAC THEN MESON_TAC[]);
\r
62 (UP_ASM_TAC THEN MESON_TAC[]);
\r
63 (SUBGOAL_THEN `mcell 4 V ul = mcell4 V (ul:(real^3)list)` ASSUME_TAC);
\r
64 (REWRITE_TAC[mcell]);
\r
66 (SUBGOAL_THEN `F` ASSUME_TAC);
\r
67 (MESON_TAC[ASSUME `4 = 0`;ARITH_RULE `~(4 = 0)`]);
\r
68 (UP_ASM_TAC THEN MESON_TAC[]);
\r
70 (SUBGOAL_THEN `F` ASSUME_TAC);
\r
71 (MESON_TAC[ASSUME `4 = 1`;ARITH_RULE `~(4 = 1)`]);
\r
72 (UP_ASM_TAC THEN MESON_TAC[]);
\r
74 (SUBGOAL_THEN `F` ASSUME_TAC);
\r
75 (MESON_TAC[ASSUME `4 = 2`;ARITH_RULE `~(4 = 2)`]);
\r
76 (UP_ASM_TAC THEN MESON_TAC[]);
\r
78 (SUBGOAL_THEN `F` ASSUME_TAC);
\r
79 (MESON_TAC[ASSUME `4 = 3`;ARITH_RULE `~(4 = 3)`]);
\r
80 (UP_ASM_TAC THEN MESON_TAC[]);
\r
83 (ASM_REWRITE_TAC[]);
\r
84 (DEL_TAC THEN DEL_TAC);
\r
87 (SUBGOAL_THEN `convex hull set_of_list (ul:(real^3)list) =
\r
88 UNIONS {rogers V (left_action_list p ul) | p permutes 0..3}`
\r
90 (MATCH_MP_TAC WQPRRDY);
\r
91 (ASM_REWRITE_TAC[IN]);
\r
93 (PURE_ASM_REWRITE_TAC[]);
\r
94 (REWRITE_TAC[IN_UNIONS]);
\r
95 (EXISTS_TAC `rogers V (ul:(real^3)list)`);
\r
96 (ASM_REWRITE_TAC[IN_ELIM_THM]);
\r
97 (EXISTS_TAC `I:(num->num)`);
\r
99 (MESON_TAC[PERMUTES_I]);
\r
101 (REWRITE_TAC[Packing3.LEFT_ACTION_LIST_I]);
\r
103 (* Finish case 1 *)
\r
105 (* =================== Case 2 ============================================== *)
\r
107 (NEW_GOAL `sqrt (&2) <= hl (ul:(real^3)list)`);
\r
108 (UP_ASM_TAC THEN REAL_ARITH_TAC);
\r
109 (SUBGOAL_THEN `? u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]` CHOOSE_TAC);
\r
110 (MP_TAC (ASSUME `barV V 3 ul`));
\r
111 (REWRITE_TAC[BARV_3_EXPLICIT]);
\r
112 (FIRST_X_ASSUM CHOOSE_TAC);
\r
113 (FIRST_X_ASSUM CHOOSE_TAC);
\r
114 (FIRST_X_ASSUM CHOOSE_TAC);
\r
116 (ASM_CASES_TAC `dist(u0:real^3, p) >= sqrt(&2)`);
\r
118 (REWRITE_TAC[ARITH_RULE `0 <= 4`]);
\r
119 (SUBGOAL_THEN `mcell 0 V ul = mcell0 V (ul:(real^3)list)` ASSUME_TAC);
\r
120 (REWRITE_TAC[mcell]);
\r
121 (ONCE_ASM_REWRITE_TAC[]);
\r
122 (REWRITE_TAC[mcell0]);
\r
123 (REWRITE_TAC[DIFF; IN; IN_ELIM_THM]);
\r
125 (ASM_MESON_TAC[IN]);
\r
126 (REWRITE_TAC[ball;IN_ELIM_THM]);
\r
128 (SUBGOAL_THEN `HD (ul:(real^3)list) = u0` ASSUME_TAC);
\r
129 (ASM_REWRITE_TAC[HD]);
\r
130 (ASM_REWRITE_TAC[]);
\r
131 (ASM_REAL_ARITH_TAC);
\r
133 (* Finish case 2 *)
\r
135 (* =================== Case 3 ============================================== *)
\r
136 (NEW_GOAL `dist (u0, p:real^3) < sqrt (&2)`);
\r
137 (UP_ASM_TAC THEN REAL_ARITH_TAC);
\r
138 (ASM_CASES_TAC `~(p IN rcone_gt (HD (ul:(real^3)list)) (HD (TL ul))
\r
139 (hl (truncate_simplex 1 ul) / sqrt (&2))) `);
\r
141 (REWRITE_TAC[ARITH_RULE `1 <= 4`]);
\r
142 (SUBGOAL_THEN `mcell 1 V ul = mcell1 V (ul:(real^3)list)` ASSUME_TAC);
\r
143 (REWRITE_TAC[mcell]);
\r
145 (SUBGOAL_THEN `F` MP_TAC);
\r
146 (UP_ASM_TAC THEN ARITH_TAC);
\r
149 (ONCE_ASM_REWRITE_TAC[]);
\r
150 (REWRITE_TAC[mcell1]);
\r
153 (REWRITE_TAC[IN_DIFF]);
\r
154 (ASM_REWRITE_TAC[IN_INTER]);
\r
155 (REWRITE_WITH `HD [u0;u1;u2;u3] = u0:real^3`);
\r
157 (REWRITE_TAC[cball;IN;IN_ELIM_THM]);
\r
158 (ASM_REAL_ARITH_TAC);
\r
162 (UP_ASM_TAC THEN MESON_TAC[]);
\r
164 (* Finish case 3 *)
\r
166 (* =================== Case 4 ============================================== *)
\r
167 (NEW_GOAL `p IN rcone_gt (HD (ul:(real^3)list)) (HD (TL ul))
\r
168 (hl (truncate_simplex 1 ul) / sqrt (&2))`);
\r
169 (UP_ASM_TAC THEN MESON_TAC[]);
\r
170 (SWITCH_TAC THEN DEL_TAC);
\r
171 (UP_ASM_TAC THEN ASM_REWRITE_TAC[HD;TL; TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
174 (ASM_CASES_TAC `p IN aff_ge {u0:real^3, u1} {mxi V ul, omega_list_n V ul 3}`);
\r
176 (REWRITE_TAC[ARITH_RULE `2 <= 4`]);
\r
177 (REWRITE_TAC[MCELL_EXPLICIT; mcell2]);
\r
180 (REWRITE_TAC[IN_INTER]);
\r
181 (ASM_REWRITE_TAC[HD;TL]);
\r
182 (REWRITE_TAC[GSYM (ASSUME `ul = [u0; u1; u2; u3:real^3]`)]);
\r
183 (ASM_REWRITE_TAC[]);
\r
184 (UP_ASM_TAC THEN UP_ASM_TAC THEN
\r
185 ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
186 (REPEAT STRIP_TAC);
\r
187 (MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET B) ==> p IN B`));
\r
188 (EXISTS_TAC `rcone_gt (u0:real^3) u1 a`);
\r
189 (REWRITE_TAC[RCONE_GT_SUBSET_RCONE_GE]);
\r
191 (MATCH_MP_TAC RCONEGE_INTER_VORONOI_CLOSED_IMP_RCONEGE);
\r
192 (EXISTS_TAC `V:real^3->bool`);
\r
193 (ASM_REWRITE_TAC[]);
\r
195 (NEW_GOAL `voronoi_nondg V (ul:(real^3)list)`);
\r
196 (UNDISCH_TAC `barV V 3 (ul:(real^3)list)`);
\r
197 (REWRITE_TAC[BARV]);
\r
198 (STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
\r
199 (ASM_REWRITE_TAC[LENGTH; INITIAL_SUBLIST;ARITH_RULE `0 < 3 + 1`]);
\r
200 (EXISTS_TAC `[]:(real^3)list`);
\r
201 (REWRITE_TAC[APPEND]);
\r
202 (UP_ASM_TAC THEN REWRITE_TAC[VORONOI_NONDG]);
\r
203 (ASM_REWRITE_TAC[set_of_list]);
\r
205 (REPEAT STRIP_TAC);
\r
206 (* Break into 7 subgoals *)
\r
208 (* Subgoal 1 & subgoal 2 *)
\r
211 (NEW_GOAL `&0 < hl [u0; u1:real^3]`);
\r
212 (REWRITE_WITH `hl [u0;u1:real^3] =
\r
213 hl (truncate_simplex 1 (ul:(real^3)list))`);
\r
214 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
215 (MATCH_MP_TAC BARV_IMP_HL_1_POS_LT);
\r
216 (EXISTS_TAC `V:real^3->bool`);
\r
217 (ASM_REWRITE_TAC[]);
\r
218 (NEW_GOAL `hl [u0;u1:real^3] = &0`);
\r
219 (ASM_REWRITE_TAC[HL;set_of_list;SET_RULE `{a, a} = {a}`]);
\r
220 (NEW_GOAL `radV {u1:real^3} = dist (circumcenter {u1},u1)`);
\r
221 (NEW_GOAL `(!w. w IN {u1:real^3} ==> radV {u1} = dist (circumcenter {u1},w))`);
\r
222 (MATCH_MP_TAC Rogers.OAPVION2);
\r
223 (REWRITE_TAC[AFFINE_INDEPENDENT_1]);
\r
224 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
226 (ASM_REWRITE_TAC[Rogers.CIRCUMCENTER_1; dist]);
\r
228 (ASM_REAL_ARITH_TAC);
\r
230 (MATCH_MP_TAC REAL_LT_DIV);
\r
232 (REWRITE_WITH `hl [u0;u1:real^3] =
\r
233 hl (truncate_simplex 1 (ul:(real^3)list))`);
\r
234 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
235 (MATCH_MP_TAC BARV_IMP_HL_1_POS_LT);
\r
236 (EXISTS_TAC `V:real^3->bool`);
\r
237 (ASM_REWRITE_TAC[]);
\r
238 (MATCH_MP_TAC SQRT_POS_LT);
\r
241 (NEW_GOAL `hl [u0; u1:real^3] / sqrt (&2) <= &1 <=>
\r
242 hl [u0; u1] <= &1 * sqrt (&2)`);
\r
243 (MATCH_MP_TAC REAL_LE_LDIV_EQ);
\r
244 (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);
\r
245 (ASM_REWRITE_TAC[]);
\r
246 (ASM_REAL_ARITH_TAC);
\r
248 (MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET B) ==> p IN B`));
\r
249 (EXISTS_TAC `rcone_gt (u0:real^3) u1 a`);
\r
250 (REWRITE_TAC[RCONE_GT_SUBSET_RCONE_GE]);
\r
253 (REWRITE_WITH `p IN voronoi_closed V (u0:real^3) <=>
\r
254 (?vl. vl IN barV V 3 /\
\r
255 p IN rogers V vl /\
\r
256 truncate_simplex 0 vl = [u0])`);
\r
257 (MATCH_MP_TAC Rogers.GLTVHUM);
\r
258 (ASM_REWRITE_TAC[]);
\r
260 (EXISTS_TAC `ul:(real^3)list`);
\r
261 (ASM_REWRITE_TAC[IN; TRUNCATE_SIMPLEX_EXPLICIT_0]);
\r
262 (UP_ASM_TAC THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
263 (REWRITE_TAC[MESON [] `~(a /\ b) <=> ~a \/ ~ b`]);
\r
265 (NEW_GOAL `~(hl [u0; u1:real^3] < sqrt (&2))`);
\r
267 (NEW_GOAL `hl [u0; u1:real^3] >= sqrt (&2)`);
\r
268 (ASM_REAL_ARITH_TAC);
\r
269 (ABBREV_TAC `t = hl [u0; u1:real^3] / sqrt (&2)`);
\r
270 (NEW_GOAL `&1 <= t`);
\r
272 (NEW_GOAL `&1 <= hl [u0; u1:real^3] / sqrt (&2) <=>
\r
273 &1 * sqrt (&2) <= hl [u0; u1]`);
\r
274 (MATCH_MP_TAC REAL_LE_RDIV_EQ);
\r
275 (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);
\r
276 (ASM_REWRITE_TAC[]);
\r
277 (ASM_REAL_ARITH_TAC);
\r
278 (UNDISCH_TAC `p IN rcone_gt (u0:real^3) u1 t`);
\r
279 (REWRITE_TAC[rcone_gt;rconesgn; IN; IN_ELIM_THM; dist]);
\r
282 (NEW_GOAL `(p - u0) dot (u1 - u0) <= norm (p - u0) * norm (u1 - u0:real^3)`);
\r
283 (REWRITE_TAC[NORM_CAUCHY_SCHWARZ]);
\r
284 (NEW_GOAL `norm (p - u0) * norm (u1 - u0) * t >=
\r
285 norm (p - u0) * norm (u1 - u0:real^3) `);
\r
286 (REWRITE_TAC[REAL_ARITH `a * b * t >= a * b <=> &0 <= (t - &1) * (a * b)`]);
\r
287 (MATCH_MP_TAC REAL_LE_MUL);
\r
289 (ASM_REAL_ARITH_TAC);
\r
290 (MATCH_MP_TAC REAL_LE_MUL);
\r
291 (REWRITE_TAC[NORM_POS_LE]);
\r
292 (ASM_REAL_ARITH_TAC);
\r
293 (UP_ASM_TAC THEN MESON_TAC[]);
\r
295 (* Finish case 4 *)
\r
297 (* =================== Case 5 ============================================== *)
\r
299 (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`);
\r
300 (NEW_GOAL `mxi V (ul:(real^3)list) = omega_list_n V ul 2`);
\r
301 (REWRITE_TAC[mxi]);
\r
305 (ASM_REAL_ARITH_TAC);
\r
306 (UP_ASM_TAC THEN MESON_TAC[]);
\r
307 (NEW_GOAL `p IN aff_ge {u0, u1:real^3} {mxi V ul, omega_list_n V ul 3}`);
\r
308 (MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET B) ==> p IN B`));
\r
310 (EXISTS_TAC `rogers V (ul:(real^3)list)`);
\r
312 (ASM_REWRITE_TAC[]);
\r
313 (MATCH_MP_TAC (SET_RULE `(?s. p SUBSET s /\ s SUBSET B) ==> p SUBSET B`));
\r
314 (EXISTS_TAC `convex hull ({u0, u1:real^3} UNION {mxi V ul, omega_list_n V ul 3})`);
\r
317 `convex hull ({u0, u1:real^3} UNION {mxi V ul, omega_list_n V ul 3}) =
\r
318 convex hull (convex hull ({u0, u1} UNION {mxi V ul, omega_list_n V ul 3}))`);
\r
319 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
320 (REWRITE_TAC[CONVEX_HULL_EQ; CONVEX_CONVEX_HULL]);
\r
321 (ONCE_ASM_REWRITE_TAC[]);
\r
322 (REWRITE_TAC[ROGERS]);
\r
323 (MATCH_MP_TAC CONVEX_HULL_SUBSET);
\r
326 [LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4` ; SET_OF_0_TO_3]);
\r
327 (REWRITE_TAC[IMAGE;SUBSET;IN;IN_ELIM_THM]);
\r
328 (REPEAT STRIP_TAC);
\r
330 (ASM_CASES_TAC `x' = 0`);
\r
331 (REWRITE_WITH `x = u0:real^3`);
\r
332 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[OMEGA_LIST_N;HD]);
\r
333 (ONCE_REWRITE_TAC[GSYM IN]);
\r
334 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
\r
337 (ASM_CASES_TAC `x' = 1`);
\r
338 (REWRITE_WITH `x = circumcenter {u0,u1:real^3}`);
\r
339 (ASM_REWRITE_TAC[]);
\r
340 (MATCH_MP_TAC OMEGA_LIST_1_EXPLICIT_NEW);
\r
341 (EXISTS_TAC `u2:real^3`);
\r
342 (EXISTS_TAC `u3:real^3`);
\r
343 (ASM_REWRITE_TAC[IN]);
\r
345 (ASM_MESON_TAC[IN]);
\r
347 (ASM_CASES_TAC `hl [u0; u1:real^3] < sqrt (&2)`);
\r
348 (ASM_REWRITE_TAC[]);
\r
349 (NEW_GOAL `hl [u0; u1:real^3] >= sqrt (&2)`);
\r
350 (ASM_REAL_ARITH_TAC);
\r
351 (ABBREV_TAC `t = hl [u0; u1:real^3] / sqrt (&2)`);
\r
352 (NEW_GOAL `&1 <= t`);
\r
354 (NEW_GOAL `&1 <= hl [u0; u1:real^3] / sqrt (&2) <=>
\r
355 &1 * sqrt (&2) <= hl [u0; u1]`);
\r
356 (MATCH_MP_TAC REAL_LE_RDIV_EQ);
\r
357 (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);
\r
358 (ASM_REWRITE_TAC[]);
\r
359 (ASM_REAL_ARITH_TAC);
\r
360 (UNDISCH_TAC `p IN rcone_gt (u0:real^3) u1 t`);
\r
361 (REWRITE_TAC[rcone_gt;rconesgn; IN; IN_ELIM_THM; dist]);
\r
364 (NEW_GOAL `(p - u0) dot (u1 - u0) <= norm (p - u0) * norm (u1 - u0:real^3)`);
\r
365 (REWRITE_TAC[NORM_CAUCHY_SCHWARZ]);
\r
366 (NEW_GOAL `norm (p - u0) * norm (u1 - u0) * t >=
\r
367 norm (p - u0) * norm (u1 - u0:real^3) `);
\r
368 (REWRITE_TAC[REAL_ARITH `a * b * t >= a * b <=> &0 <= (t - &1) * (a * b)`]);
\r
369 (MATCH_MP_TAC REAL_LE_MUL);
\r
371 (ASM_REAL_ARITH_TAC);
\r
372 (MATCH_MP_TAC REAL_LE_MUL);
\r
373 (REWRITE_TAC[NORM_POS_LE]);
\r
374 (ASM_REAL_ARITH_TAC);
\r
375 (UP_ASM_TAC THEN MESON_TAC[]);
\r
376 (ONCE_REWRITE_TAC[GSYM IN]);
\r
378 (MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET B) ==> p IN B`));
\r
379 (EXISTS_TAC `convex hull ({u0, u1:real^3})`);
\r
381 (REWRITE_TAC[Rogers.CIRCUMCENTER_2; midpoint;CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
382 (EXISTS_TAC `&1 / (&2)`);
\r
383 (EXISTS_TAC `&1 / (&2)`);
\r
384 (ASM_SIMP_TAC[REAL_LE_DIV; REAL_ARITH `&0 <= &1 /\ &0 <= &2`]);
\r
387 (VECTOR_ARITH_TAC);
\r
388 (MATCH_MP_TAC CONVEX_HULL_SUBSET);
\r
391 (ASM_CASES_TAC `x' = 2`);
\r
392 (ASM_REWRITE_TAC[]);
\r
393 (ONCE_REWRITE_TAC[GSYM IN]);
\r
394 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
\r
397 (ASM_CASES_TAC `x' = 3`);
\r
398 (ASM_REWRITE_TAC[]);
\r
399 (ONCE_REWRITE_TAC[GSYM IN]);
\r
400 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
\r
403 (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN DEL_TAC);
\r
404 (UP_ASM_TAC THEN TRUONG_SET_TAC[]);
\r
405 (UP_ASM_TAC THEN MESON_TAC[]);
\r
406 (ASM_REWRITE_TAC[SET_RULE `{a, b} UNION {c , d} = {a, b, c,d}`]);
\r
407 (REWRITE_TAC[CONVEX_HULL_4_SUBSET_AFF_GE_2_2]);
\r
413 (NEW_GOAL `hl (truncate_simplex 2 (ul:(real^3)list)) < sqrt (&2)`);
\r
414 (ASM_REAL_ARITH_TAC);
\r
416 (REWRITE_TAC[ARITH_RULE `3 <= 4`]);
\r
417 (REWRITE_TAC[MCELL_EXPLICIT; mcell3]);
\r
420 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);
\r
421 (REWRITE_TAC[SET_RULE `{a, b ,c} UNION {d} = {a, b , c, d}`]);
\r
426 `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
\r
427 dist (u0,s:real^3) = sqrt (&2) /\
\r
429 (MATCH_MP_TAC MXI_EXPLICIT_OLD);
\r
431 (FIRST_X_ASSUM CHOOSE_TAC);
\r
432 (REWRITE_WITH `mxi V [u0; u1; u2; u3] = s:real^3`);
\r
435 (* ========================================================================= *)
\r
437 (ABBREV_TAC `a = omega_list_n V ul 1`);
\r
438 (ABBREV_TAC `b = omega_list_n V ul 2`);
\r
439 (ABBREV_TAC `c = omega_list_n V ul 3`);
\r
441 (NEW_GOAL `p IN convex hull {u0, a, b, c:real^3}`);
\r
442 (EXPAND_TAC "a" THEN EXPAND_TAC "b" THEN EXPAND_TAC "c");
\r
443 (REWRITE_WITH `u0:real^3 = HD ul`);
\r
444 (ASM_REWRITE_TAC[HD]);
\r
445 (REWRITE_WITH `convex hull
\r
446 {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3} =
\r
448 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
449 (MATCH_MP_TAC ROGERS_EXPLICIT);
\r
450 (ASM_REWRITE_TAC[]);
\r
451 (ASM_REWRITE_TAC[]);
\r
452 (NEW_GOAL `a = midpoint (u0, u1:real^3)`);
\r
453 (REWRITE_TAC[GSYM Rogers.CIRCUMCENTER_2]);
\r
455 (REWRITE_WITH `{u0,u1} = set_of_list [u0;(u1:real^3)]`);
\r
456 (MESON_TAC[set_of_list]);
\r
457 (REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`; OMEGA_LIST_TRUNCATE_1]);
\r
458 (MATCH_MP_TAC XNHPWAB1);
\r
461 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
\r
463 (MP_TAC (ASSUME `barV V 3 ul`) THEN REWRITE_TAC[IN;BARV]);
\r
464 (REPEAT STRIP_TAC);
\r
465 (REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC 0) = 1 + 1`]);
\r
466 (NEW_GOAL `initial_sublist vl (ul:(real^3)list)`);
\r
467 (UNDISCH_TAC `initial_sublist vl [u0:real^3; u1]`);
\r
468 (REWRITE_TAC[INITIAL_SUBLIST] THEN STRIP_TAC);
\r
469 (EXISTS_TAC `APPEND yl [u2;u3:real^3]`);
\r
470 (REWRITE_TAC[APPEND_ASSOC; GSYM (ASSUME `[u0:real^3; u1] = APPEND vl yl`)]);
\r
471 (ASM_REWRITE_TAC[APPEND]);
\r
476 (ABBREV_TAC `sl = truncate_simplex 2 (ul:(real^3)list)`);
\r
477 (MATCH_MP_TAC (REAL_ARITH `hl (sl:(real^3)list) < b /\ a < hl sl ==> a < b`));
\r
478 (ASM_REWRITE_TAC[]);
\r
479 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 sl`);
\r
480 (EXPAND_TAC "sl" THEN DEL_TAC);
\r
481 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
482 (EXPAND_TAC "sl" THEN REWRITE_TAC[ASSUME
\r
483 `ul = [u0;u1;u2:real^3;u3]`; TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
484 (REWRITE_WITH `hl ([u0;u1;u2:real^3]) =
\r
485 hl (truncate_simplex 2 (sl:(real^3)list))`);
\r
487 (ASM_MESON_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
488 (REWRITE_WITH `[u0;u1;u2:real^3] = sl`);
\r
489 (ASM_MESON_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
491 (NEW_GOAL `!i j. i < j /\ j <= 2
\r
492 ==> hl (truncate_simplex i (sl:(real^3)list))
\r
493 < hl (truncate_simplex j sl)`);
\r
494 (MATCH_MP_TAC XNHPWAB4);
\r
495 (EXISTS_TAC `V:real^3->bool`);
\r
497 (ASM_REWRITE_TAC[]);
\r
498 (EXPAND_TAC "sl" THEN REWRITE_TAC[IN]);
\r
499 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
500 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
501 (FIRST_ASSUM MATCH_MP_TAC);
\r
504 (* ================================================================== *)
\r
505 (NEW_GOAL `p IN convex hull {b, c, u0, u1:real^3}`);
\r
506 (UP_ASM_TAC THEN UP_ASM_TAC);
\r
507 (REWRITE_TAC[CONVEX_HULL_4; midpoint; IN; IN_ELIM_THM]);
\r
508 (REPEAT STRIP_TAC);
\r
509 (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`);
\r
510 (EXISTS_TAC `u + v * inv (&2)` THEN EXISTS_TAC `v * inv (&2)`);
\r
511 (ASM_REWRITE_TAC[]);
\r
512 (NEW_GOAL `&0 <= v * inv (&2)`);
\r
513 (MATCH_MP_TAC REAL_LE_MUL);
\r
514 (ASM_REAL_ARITH_TAC);
\r
515 (ASM_REWRITE_TAC[REAL_ARITH `w + z + (u + v * inv (&2)) + v * inv (&2) =
\r
518 (MATCH_MP_TAC REAL_LE_ADD);
\r
519 (ASM_REWRITE_TAC[]);
\r
520 (VECTOR_ARITH_TAC);
\r
521 (NEW_GOAL `convex hull {b, c, u0, u1:real^3} =
\r
522 convex hull {b, s, u0, u1} UNION convex hull {s, c, u0, u1}`);
\r
523 (MATCH_MP_TAC CONVEX_HULL_BREAK_KY_LEMMA);
\r
524 (ASM_REWRITE_TAC[]);
\r
525 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[IN_UNION]);
\r
526 (NEW_GOAL `~(p IN convex hull {s, c, u0, u1:real^3})`);
\r
529 (NEW_GOAL `p IN aff_ge {u0, u1} {mxi V ul, c:real^3}`);
\r
535 (NEW_GOAL `convex hull {s, c, u0, u1} SUBSET aff_ge {u0, u1} {s, c:real^3}`);
\r
536 (REWRITE_WITH `{s, c, u0, u1} = {u0,u1,s, c:real^3}`);
\r
538 (REWRITE_TAC[CONVEX_HULL_4_SUBSET_AFF_GE_2_2]);
\r
542 (NEW_GOAL `p IN convex hull {b, s, u0, u1:real^3}`);
\r
545 (NEW_GOAL `b IN convex hull {u0,u1,u2:real^3}`);
\r
547 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;OMEGA_LIST_TRUNCATE_2]);
\r
548 (ABBREV_TAC `wl = [u0;u1;u2:real^3]`);
\r
549 (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list wl`);
\r
550 (EXPAND_TAC "wl" THEN REWRITE_TAC[set_of_list]);
\r
551 (MATCH_MP_TAC XNHPWAB2);
\r
553 (REWRITE_WITH `wl = truncate_simplex 2 (ul:(real^3)list)`);
\r
554 (EXPAND_TAC "wl" THEN REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`]);
\r
555 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
556 (ASM_REWRITE_TAC[IN]);
\r
557 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
558 (EXISTS_TAC `3` THEN ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
\r
560 (UP_ASM_TAC THEN UP_ASM_TAC);
\r
561 (REWRITE_TAC[CONVEX_HULL_3; CONVEX_HULL_4; IN; IN_ELIM_THM]);
\r
562 (REPEAT STRIP_TAC);
\r
564 (EXISTS_TAC `w + u * u'`);
\r
565 (EXISTS_TAC `z + u * v'`);
\r
566 (EXISTS_TAC `u * w'`);
\r
567 (EXISTS_TAC `v:real`);
\r
569 (ASM_SIMP_TAC[REAL_LE_ADD; REAL_LE_MUL]);
\r
571 (ASM_REWRITE_TAC[REAL_ARITH `(w + u * u') + (z + u * v') + u * w' + v =
\r
572 u * (u' + v' + w') + v + w + z`; REAL_MUL_RID]);
\r
573 (VECTOR_ARITH_TAC);
\r
576 (ASM_MESON_TAC[])]);;
\r
578 (* =========================================================================== *)
\r
579 (* =========================================================================== *)
\r
581 let SLTSTLO2 = prove_by_refinement (
\r
584 [(REPEAT STRIP_TAC);
\r
585 (ABBREV_TAC `B1 = frontier (rogers V (ul:(real^3)list))`);
\r
586 (ABBREV_TAC `B2 = {w| norm ((w:real^3) - (HD ul)) = sqrt (&2)}`);
\r
587 (ABBREV_TAC `B3 = rcone_eq (HD (ul:(real^3)list)) (HD (TL ul))
\r
588 (hl (truncate_simplex 1 ul) / sqrt (&2))`);
\r
589 (ABBREV_TAC `B4 = affine hull {(HD (ul:(real^3)list)), (HD (TL ul)),
\r
591 (ABBREV_TAC `B5 = convex hull {omega_list_n V ul 2,
\r
592 omega_list_n V (ul:(real^3)list) 3 }`);
\r
593 (ABBREV_TAC `B6 = affine hull {(HD (ul:(real^3)list)), (HD (TL ul)),
\r
594 (HD (TL (TL ul)))}`);
\r
595 (ABBREV_TAC `B7 = affine hull {omega_list_n V ul 1, omega_list_n V ul 2,
\r
596 omega_list_n V ul 3}`);
\r
598 (ABBREV_TAC `Z = B1 UNION B2 UNION B3 UNION B4 UNION
\r
599 (B5:real^3->bool) UNION B6 UNION B7`);
\r
600 (EXISTS_TAC `Z:real^3->bool`);
\r
601 (REPEAT STRIP_TAC);
\r
603 (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);
\r
604 (MP_TAC (ASSUME `barV V 3 ul`));
\r
605 (REWRITE_TAC[BARV_3_EXPLICIT]);
\r
606 (FIRST_X_ASSUM CHOOSE_TAC);
\r
607 (FIRST_X_ASSUM CHOOSE_TAC);
\r
608 (FIRST_X_ASSUM CHOOSE_TAC);
\r
609 (FIRST_X_ASSUM CHOOSE_TAC);
\r
612 (MATCH_MP_TAC NEGLIGIBLE_UNION);
\r
614 (EXPAND_TAC "B1" THEN MATCH_MP_TAC NEGLIGIBLE_CONVEX_FRONTIER);
\r
615 (ASM_SIMP_TAC[ROGERS_EXPLICIT;CONVEX_CONVEX_HULL]);
\r
616 (MATCH_MP_TAC NEGLIGIBLE_UNION);
\r
619 (* revised 2013-05-25: *)
\r
620 (NEW_GOAL `(?(v:real^3)(r:real). (r> &0)/\ (B2 ={w:real^3 | norm (w-v)= r}))`);
\r
622 (EXISTS_TAC `(HD ul):real^3` THEN EXISTS_TAC `sqrt(&2)`);
\r
623 (ASM_REWRITE_TAC[REAL_ARITH `a > &0 <=> &0 < a`]);
\r
624 (MATCH_MP_TAC SQRT_POS_LT);
\r
626 (ASM_SIMP_TAC[NULLSET_SPHERE]);
\r
627 (* end of revision *)
\r
629 (MATCH_MP_TAC NEGLIGIBLE_UNION);
\r
632 (MATCH_MP_TAC NEGLIGIBLE_RCONE_EQ);
\r
633 (ASM_REWRITE_TAC[HD;TL]);
\r
635 (NEW_GOAL `aff_dim (set_of_list [u0;u1:real^3]) = &0`);
\r
636 (ASM_REWRITE_TAC[set_of_list; SET_RULE `{x, x} = {x}`; AFF_DIM_SING]);
\r
637 (NEW_GOAL `aff_dim (set_of_list [u0;u1:real^3]) = &1`);
\r
638 (MATCH_MP_TAC MHFTTZN1);
\r
639 (EXISTS_TAC `V:real^3->bool`);
\r
640 (ASM_REWRITE_TAC[]);
\r
641 (REWRITE_WITH `[u0; u0:real^3] = truncate_simplex 1 ul`);
\r
642 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
643 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
645 (ASM_REWRITE_TAC[]);
\r
647 (NEW_GOAL `&0 = &1`);
\r
648 (ASM_MESON_TAC[INT_OF_NUM_EQ;REAL_OF_NUM_EQ]);
\r
649 (UP_ASM_TAC THEN REAL_ARITH_TAC);
\r
650 (MATCH_MP_TAC NEGLIGIBLE_UNION);
\r
653 (REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]);
\r
654 (MATCH_MP_TAC NEGLIGIBLE_UNION);
\r
657 (ONCE_REWRITE_TAC[SET_RULE `{a,b:real^3} = {a,a,b}`]);
\r
658 (MESON_TAC[NEGLIGIBLE_CONVEX_HULL_3]);
\r
659 (MATCH_MP_TAC NEGLIGIBLE_UNION);
\r
662 (REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]);
\r
664 (REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]);
\r
666 (* ========================================================================= *)
\r
668 (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);
\r
669 (MP_TAC (ASSUME `barV V 3 ul`));
\r
670 (REWRITE_TAC[BARV_3_EXPLICIT]);
\r
671 (FIRST_X_ASSUM CHOOSE_TAC);
\r
672 (FIRST_X_ASSUM CHOOSE_TAC);
\r
673 (FIRST_X_ASSUM CHOOSE_TAC);
\r
674 (FIRST_X_ASSUM CHOOSE_TAC);
\r
676 (REWRITE_TAC[EXISTS_UNIQUE]);
\r
677 (NEW_GOAL `?i. i <= 4 /\ p IN mcell i V ul`);
\r
678 (MATCH_MP_TAC SLTSTLO1);
\r
679 (ASM_REWRITE_TAC[]);
\r
681 (FIRST_X_ASSUM CHOOSE_TAC THEN EXISTS_TAC `i:num`);
\r
683 (ASM_REWRITE_TAC[]);
\r
685 (* ========================================================================= *)
\r
687 (ASM_CASES_TAC `hl (ul:(real^3)list) < sqrt(&2)`);
\r
688 (NEW_GOAL ` mcell0 V ul = {} /\ mcell1 V ul = {} /\
\r
689 mcell2 V ul = {} /\ mcell3 V ul = {}`);
\r
690 (ASM_MESON_TAC[EMNWUUS2]);
\r
691 (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC);
\r
693 (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==>
\r
694 ~ (y = 0 \/ y = 1 \/ y = 2 \/ y = 3)`);
\r
695 (REPEAT STRIP_TAC);
\r
696 (UNDISCH_TAC `p IN mcell y V ul` THEN ASM_REWRITE_TAC[MCELL_EXPLICIT]);
\r
698 (UNDISCH_TAC `p IN mcell y V ul` THEN ASM_REWRITE_TAC[MCELL_EXPLICIT]);
\r
700 (UNDISCH_TAC `p IN mcell y V ul` THEN ASM_REWRITE_TAC[MCELL_EXPLICIT]);
\r
702 (UNDISCH_TAC `p IN mcell y V ul` THEN ASM_REWRITE_TAC[MCELL_EXPLICIT]);
\r
704 (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 4`);
\r
705 (GEN_TAC THEN DISCH_TAC);
\r
706 (NEW_GOAL `~(y = 0 \/ y = 1 \/ y = 2 \/ y = 3)`);
\r
709 (GEN_TAC THEN DISCH_TAC);
\r
710 (NEW_GOAL `y = 4`);
\r
712 (NEW_GOAL `i = 4`);
\r
715 (NEW_GOAL `sqrt (&2) <= hl (ul:(real^3)list)`);
\r
716 (UP_ASM_TAC THEN REAL_ARITH_TAC);
\r
718 (* ========================================================================= *)
\r
720 (ASM_CASES_TAC `dist(u0:real^3, p) >= sqrt(&2)`);
\r
721 (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==>
\r
722 ~ (y = 4 \/ y = 1 \/ y = 2 \/ y = 3)`);
\r
723 (REPEAT STRIP_TAC);
\r
724 (NEW_GOAL `mcell 4 V ul = {}`);
\r
726 (SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);
\r
732 (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 4`]);
\r
733 (REWRITE_TAC[ASSUME `mcell 4 V ul = {}`]);
\r
735 (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 1`;
\r
736 MCELL_EXPLICIT;mcell1]);
\r
739 (NEW_GOAL `~(p:real^3 IN B2)`);
\r
740 (UNDISCH_TAC `p IN rogers V ul DIFF Z` THEN REWRITE_TAC[IN_DIFF]);
\r
741 (EXPAND_TAC "Z" THEN REWRITE_TAC[IN_UNION]);
\r
743 (NEW_GOAL `p:real^3 IN cball (HD ul,sqrt (&2))`);
\r
744 (ASM_SET_TAC[IN_DIFF;IN_INTER]);
\r
745 (NEW_GOAL `~(p:real^3 IN B2 UNION ball (HD ul,sqrt (&2)))`);
\r
746 (ASM_REWRITE_TAC[IN_UNION;HD;ball;IN;IN_ELIM_THM]);
\r
747 (ASM_REAL_ARITH_TAC);
\r
748 (UP_ASM_TAC THEN REWRITE_WITH `B2 UNION ball (HD ul,sqrt (&2)) =
\r
749 cball (HD (ul:(real^3)list),sqrt (&2))`);
\r
751 (REWRITE_TAC[SET_EQ_LEMMA; IN_UNION; cball; ball;IN;IN_ELIM_THM]);
\r
752 (ONCE_REWRITE_TAC[DIST_SYM]);
\r
753 (REWRITE_TAC[dist] THEN REAL_ARITH_TAC);
\r
754 (ASM_REWRITE_TAC[]);
\r
758 (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 2`;
\r
759 MCELL_EXPLICIT;mcell2]);
\r
762 (ASM_REWRITE_TAC[HD;TL] THEN STRIP_TAC);
\r
763 (NEW_GOAL `p:real^3 IN (rcone_ge u0 u1 a INTER rcone_ge u1 u0 a)`);
\r
764 (ASM_SET_TAC[IN_INTER]);
\r
765 (UP_ASM_TAC THEN REWRITE_TAC[IN_INTER;rcone_ge;rconesgn;IN;IN_ELIM_THM]);
\r
766 (REPEAT STRIP_TAC);
\r
767 (NEW_GOAL `(p - u0) dot (u1 - u0:real^3) + (p - u1) dot (u0 - u1) >=
\r
768 dist (p,u0) * dist (u1,u0) * a + dist (p,u1) * dist (u0,u1) * a`);
\r
769 (ASM_REAL_ARITH_TAC);
\r
770 (UP_ASM_TAC THEN REWRITE_TAC[DIST_SYM]);
\r
771 (REWRITE_WITH `(p - u0) dot (u1 - u0:real^3) + (p - u1) dot (u0 - u1) =
\r
772 (u0 - u1) dot (u0 - u1)`);
\r
773 (VECTOR_ARITH_TAC);
\r
774 (REWRITE_TAC[REAL_ARITH `x * a * b + y * a * b = (x + y) * a * b`;
\r
775 GSYM NORM_POW_2; GSYM dist]);
\r
777 (* ========================================================================== *)
\r
778 (NEW_GOAL `dist (p,u0:real^3) <= dist (p,u1) /\ a = (inv(&2) * dist (u0,u1)) / sqrt (&2)`);
\r
779 (REPEAT STRIP_TAC);
\r
781 (NEW_GOAL `p IN rogers V ul`);
\r
782 (ASM_SET_TAC[IN_DIFF]);
\r
783 (NEW_GOAL `(p:real^3) IN voronoi_closed V u0`);
\r
784 (NEW_GOAL `(p:real^3) IN voronoi_closed V u0 <=>
\r
785 (?vl. vl IN barV V 3 /\
\r
786 p IN rogers V vl /\
\r
787 truncate_simplex 0 vl = [u0:real^3])`);
\r
788 (MATCH_MP_TAC GLTVHUM);
\r
789 (ASM_REWRITE_TAC[]);
\r
790 (MATCH_MP_TAC BARV_IMP_u0_IN_V);
\r
791 (EXISTS_TAC `ul:(real^3)list`);
\r
792 (EXISTS_TAC `u1:real^3`);
\r
793 (EXISTS_TAC `u2:real^3`);
\r
794 (EXISTS_TAC `u3:real^3`);
\r
795 (ASM_REWRITE_TAC[]);
\r
796 (ASM_REWRITE_TAC[]);
\r
797 (EXISTS_TAC `ul:(real^3)list`);
\r
798 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_0]);
\r
800 (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed;IN;IN_ELIM_THM]);
\r
801 (DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
\r
802 (NEW_GOAL `set_of_list (ul:(real^3)list) SUBSET V`);
\r
803 (MATCH_MP_TAC Packing3.BARV_SUBSET);
\r
804 (EXISTS_TAC `3` THEN ASM_MESON_TAC[]);
\r
805 (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list]);
\r
810 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; HL;set_of_list]);
\r
811 (NEW_GOAL `!w. w IN {u0,u1:real^3} ==>
\r
812 radV {u0,u1} = dist (circumcenter {u0,u1},w)`);
\r
813 (MATCH_MP_TAC Rogers.OAPVION2);
\r
814 (REWRITE_TAC[AFFINE_INDEPENDENT_IFF_CARD]);
\r
816 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
817 (NEW_GOAL `aff_dim {u0, u1:real^3} = &1`);
\r
818 (ABBREV_TAC `vl = [u0;u1:real^3]`);
\r
819 (REWRITE_WITH `{u0, u1:real^3} = set_of_list vl`);
\r
820 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
821 (MATCH_MP_TAC Rogers.MHFTTZN1);
\r
822 (EXISTS_TAC `V:real^3->bool`);
\r
823 (ASM_REWRITE_TAC[]);
\r
824 (REWRITE_WITH `vl = truncate_simplex 1 ul:(real^3)list`);
\r
825 (EXPAND_TAC "vl" THEN DEL_TAC);
\r
826 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
827 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
828 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
\r
830 (ASM_REWRITE_TAC[]);
\r
831 (ONCE_REWRITE_TAC[ARITH_RULE
\r
832 `&1 = &(CARD {u0, u1:real^3}) - (&1):int
\r
833 <=> &(CARD {u0, u1:real^3}) = (&2):int`]);
\r
834 (ONCE_REWRITE_TAC[INT_OF_NUM_EQ]);
\r
835 (REWRITE_TAC[Geomdetail.CARD2]);
\r
836 (REPEAT STRIP_TAC);
\r
838 (NEW_GOAL `CARD {u0, u1:real^3} = 1`);
\r
839 (REWRITE_WITH `{u0, u1} = {u1:real^3}`);
\r
841 (REWRITE_TAC[Geomdetail.CARD_SING]);
\r
842 (NEW_GOAL `aff_dim {u0, u1} <= &(CARD {u0, u1:real^3}) - (&1):int`);
\r
843 (MATCH_MP_TAC AFF_DIM_LE_CARD);
\r
844 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
845 (NEW_GOAL `(&2):int <= &(CARD {u0, u1:real^3})`);
\r
846 (ONCE_REWRITE_TAC[ARITH_RULE
\r
847 `(&2):int <= &(CARD {u0, u1:real^3}) <=>
\r
848 &1 <= &(CARD {u0, u1:real^3}) - (&1):int`]);
\r
850 (NEW_GOAL `&(CARD {u0, u1:real^3}) <= (&2):int`);
\r
851 (ONCE_REWRITE_TAC[INT_OF_NUM_LE]);
\r
852 (REWRITE_TAC[Geomdetail.CARD2]);
\r
853 (NEW_GOAL `CARD {u0, u1:real^3} = 2`);
\r
854 (ONCE_REWRITE_TAC[GSYM INT_OF_NUM_EQ]);
\r
858 (REWRITE_WITH `radV {u0, u1} = dist (circumcenter {u0, u1},u0:real^3)`);
\r
859 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
860 (TRUONG_SET_TAC[]);
\r
861 (REWRITE_TAC[CIRCUMCENTER_2;midpoint;dist;
\r
862 VECTOR_ARITH `inv (&2) % (u0 + u1) - u0 = inv (&2) % (u1 - u0)`]);
\r
863 (REWRITE_TAC[NORM_MUL]);
\r
864 (REWRITE_WITH `abs (inv (&2)) = inv (&2)`);
\r
865 (REWRITE_TAC[REAL_ABS_REFL]);
\r
867 (REWRITE_TAC[GSYM dist]);
\r
868 (MESON_TAC[DIST_SYM]);
\r
869 (UP_ASM_TAC THEN REPEAT STRIP_TAC);
\r
870 (NEW_GOAL `(dist (p,u0) + dist (p,u1:real^3)) * dist (u0,u1) * a >=
\r
871 (&2 * dist (p,u0)) * dist (u0,u1) * a`);
\r
872 (REWRITE_TAC[REAL_ARITH `(x + y) * a * b >= (&2 * x) * a * b <=>
\r
873 &0 <= (y - x) * a * b`]);
\r
874 (MATCH_MP_TAC REAL_LE_MUL);
\r
876 (ASM_REAL_ARITH_TAC);
\r
877 (MATCH_MP_TAC REAL_LE_MUL);
\r
879 (REWRITE_TAC[DIST_POS_LE]);
\r
880 (ASM_REWRITE_TAC[]);
\r
881 (MATCH_MP_TAC REAL_LE_DIV);
\r
883 (MATCH_MP_TAC REAL_LE_MUL);
\r
886 (REWRITE_TAC[DIST_POS_LE]);
\r
887 (MATCH_MP_TAC SQRT_POS_LE);
\r
890 (NEW_GOAL `dist (u0,u1:real^3) pow 2 >= (&2 * dist (p,u0)) * dist (u0,u1) * a `);
\r
891 (ASM_REAL_ARITH_TAC);
\r
892 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
893 (REWRITE_TAC[REAL_ARITH `(&2 * x) * a * (inv(&2) * a) / b = (x / b) * a pow 2`]);
\r
894 (REWRITE_TAC[REAL_ARITH `a >= x * a <=> &0 <= a * (&1 - x)`]);
\r
896 (NEW_GOAL `&0 <= dist (u0,u1) pow 2 * (&1 - dist (p,u0) / sqrt (&2))
\r
897 <=> &0 <= (&1 - dist (p,u0:real^3) / sqrt (&2))`);
\r
898 (NEW_GOAL `&0 < dist (u0,u1:real^3) pow 2`);
\r
899 (REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT; DIST_EQ_0]);
\r
903 (NEW_GOAL `aff_dim {u0, u1:real^3} = &1`);
\r
904 (ABBREV_TAC `vl = [u0;u1:real^3]`);
\r
905 (REWRITE_WITH `{u0, u1:real^3} = set_of_list vl`);
\r
906 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
907 (MATCH_MP_TAC Rogers.MHFTTZN1);
\r
908 (EXISTS_TAC `V:real^3->bool`);
\r
909 (ASM_REWRITE_TAC[]);
\r
910 (REWRITE_WITH `vl = truncate_simplex 1 ul:(real^3)list`);
\r
911 (EXPAND_TAC "vl" THEN DEL_TAC);
\r
912 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
913 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
914 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
\r
916 (NEW_GOAL `CARD {u0, u1:real^3} = 1`);
\r
917 (REWRITE_WITH `{u0, u1} = {u1:real^3}`);
\r
919 (REWRITE_TAC[Geomdetail.CARD_SING]);
\r
920 (NEW_GOAL `aff_dim {u0, u1} <= &(CARD {u0, u1:real^3}) - (&1):int`);
\r
921 (MATCH_MP_TAC AFF_DIM_LE_CARD);
\r
922 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
923 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
925 (ASM_MESON_TAC[REAL_LE_MUL_EQ]);
\r
926 (NEW_GOAL `&0 <= &1 - dist (p,u0:real^3) / sqrt (&2)`);
\r
928 (UP_ASM_TAC THEN REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
\r
929 (REWRITE_WITH `dist (p,u0:real^3) / sqrt (&2) <= &1
\r
930 <=> dist (p,u0) <= &1 * sqrt (&2)`);
\r
931 (MATCH_MP_TAC REAL_LE_LDIV_EQ);
\r
932 (MATCH_MP_TAC SQRT_POS_LT);
\r
934 (REWRITE_TAC [REAL_MUL_LID]);
\r
936 (NEW_GOAL `dist (p, u0:real^3) = sqrt (&2)`);
\r
937 (UP_ASM_TAC THEN ONCE_REWRITE_TAC[DIST_SYM]);
\r
938 (ASM_REAL_ARITH_TAC);
\r
939 (NEW_GOAL `~(p:real^3 IN B2)`);
\r
940 (ASM_SET_TAC[IN_DIFF]);
\r
941 (UP_ASM_TAC THEN EXPAND_TAC "B2" THEN REWRITE_TAC[IN;IN_ELIM_THM]);
\r
942 (ASM_REWRITE_TAC[HD;GSYM dist]);
\r
945 (* ========================================================================= *)
\r
947 (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 3`;
\r
948 MCELL_EXPLICIT;mcell3]);
\r
951 (ASM_REWRITE_TAC[HD;TL;set_of_list]);
\r
952 (NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
\r
953 dist (u0,s) = sqrt (&2) /\
\r
954 mxi V ul = s:real^3)`);
\r
955 (MATCH_MP_TAC MXI_EXPLICIT_OLD);
\r
956 (ASM_REWRITE_TAC[]);
\r
957 (FIRST_X_ASSUM CHOOSE_TAC);
\r
958 (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC);
\r
959 (UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);
\r
960 (REWRITE_TAC[SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);
\r
962 (SUBGOAL_THEN `p:real^3 IN rogers V ul` MP_TAC);
\r
963 (ASM_SET_TAC[IN_DIFF]);
\r
964 (ASM_SIMP_TAC[ROGERS_EXPLICIT; HD]);
\r
965 (ABBREV_TAC `s1 = omega_list_n V [u0; u1; u2; u3:real^3] 1`);
\r
966 (ABBREV_TAC `s2 = omega_list_n V [u0; u1; u2; u3:real^3] 2`);
\r
967 (ABBREV_TAC `s3 = omega_list_n V [u0; u1; u2; u3:real^3] 3`);
\r
969 (NEW_GOAL `?m n:real^3.
\r
970 between p (m,n) /\ between m (u0,s1) /\ between n (s2,s3)`);
\r
971 (ASM_SIMP_TAC[CONVEX_HULL_4_IMP_2_2]);
\r
972 (UP_ASM_TAC THEN REPEAT STRIP_TAC);
\r
973 (NEW_GOAL `between (p - m:real^3) (vec 0, n - m)`);
\r
974 (UNDISCH_TAC `between p (m,n:real^3)` THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;
\r
975 CONVEX_HULL_2;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
\r
976 (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN ASM_REWRITE_TAC[]);
\r
977 (REWRITE_WITH `(u % m + v % n) - m:real^3 = (u % m + v % n) - (u + v) % m`);
\r
978 (ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);
\r
979 (VECTOR_ARITH_TAC);
\r
980 (NEW_GOAL `between (proj_point (s2 - m) (p - m:real^3))
\r
981 (vec 0, proj_point (s2 - m) (n - m))`);
\r
982 (REWRITE_WITH `vec 0 = proj_point (s2 - m) (m - m:real^3)`);
\r
983 (REWRITE_TAC[VECTOR_SUB_REFL; PRO_EXP; DOT_LZERO; REAL_ARITH `&0 / a = &0`]);
\r
984 (VECTOR_ARITH_TAC);
\r
985 (MATCH_MP_TAC BETWEEN_PROJ_POINT);
\r
986 (ASM_REWRITE_TAC[VECTOR_SUB_REFL]);
\r
987 (ABBREV_TAC `p' = proj_point (s2 - m) (p - m:real^3)`);
\r
988 (ABBREV_TAC `n' = proj_point (s2 - m) (n - m:real^3)`);
\r
991 (* ============================================================================ *)
\r
993 (ABBREV_TAC `vl = [u0;u1;u2:real^3]`);
\r
994 (NEW_GOAL `s2:real^3 = circumcenter (set_of_list vl)`);
\r
995 (EXPAND_TAC "s2" THEN EXPAND_TAC "vl");
\r
996 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_2]);
\r
997 (MATCH_MP_TAC XNHPWAB1);
\r
999 (REWRITE_WITH `[u0; u1; u2:real^3] = truncate_simplex 2 ul`);
\r
1000 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1001 (ASM_REWRITE_TAC[IN]);
\r
1002 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1004 (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
\r
1006 (NEW_GOAL `s3 IN voronoi_list V (truncate_simplex 2 (ul:(real^3)list))`);
\r
1007 (NEW_GOAL `s3 IN voronoi_list V (truncate_simplex (SUC 2)
\r
1008 [u0:real^3; u1; u2; u3])`);
\r
1009 (EXPAND_TAC "s3");
\r
1010 (REWRITE_TAC[OMEGA_LIST_N;ARITH_RULE `3 = SUC 2`]);
\r
1011 (MATCH_MP_TAC CLOSEST_POINT_IN_SET);
\r
1012 (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);
\r
1013 (MATCH_MP_TAC Packing3.BARV_IMP_VORONOI_LIST_NOT_EMPTY);
\r
1015 (REWRITE_WITH `truncate_simplex (SUC 2) [u0; u1; u2; u3:real^3] = ul`);
\r
1016 (ASM_REWRITE_TAC[ARITH_RULE `SUC 2 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3]);
\r
1017 (ASM_MESON_TAC[]);
\r
1019 (REWRITE_WITH `truncate_simplex (SUC 2) [u0; u1; u2; u3:real^3] = ul`);
\r
1020 (ASM_REWRITE_TAC[ARITH_RULE `SUC 2 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3]);
\r
1022 (NEW_GOAL `voronoi_list V (ul:(real^3)list) SUBSET
\r
1023 voronoi_list V (truncate_simplex 2 ul)`);
\r
1024 (ASM_REWRITE_TAC[VORONOI_LIST;VORONOI_SET; SUBSET;
\r
1025 TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list; IN_INTERS]);
\r
1026 (EXPAND_TAC "vl" THEN REWRITE_TAC[IN; IN_ELIM_THM;set_of_list]
\r
1027 THEN REPEAT STRIP_TAC);
\r
1028 (FIRST_ASSUM MATCH_MP_TAC);
\r
1029 (EXISTS_TAC `v:real^3`);
\r
1030 (ASM_REWRITE_TAC[]);
\r
1031 (SWITCH_TAC THEN UP_ASM_TAC THEN TRUONG_SET_TAC[]);
\r
1032 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[SUBSET]);
\r
1035 (NEW_GOAL `n' = s2:real^3 - m`);
\r
1036 (EXPAND_TAC "n'");
\r
1037 (UNDISCH_TAC `between n (s2,s3:real^3)` THEN REWRITE_TAC[
\r
1038 BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
\r
1039 (REWRITE_TAC[ASSUME `n:real^3 = u % s2 + v % s3`]);
\r
1040 (REWRITE_WITH `(u % s2 + v % s3) - m:real^3 = (s2 - m) + v % (s3 - s2)`);
\r
1041 (REWRITE_TAC[VECTOR_ARITH `(u % s2 + v % s3) - m = s2 - m + v % (s3 - s2)
\r
1042 <=> (u + v) % s2 = s2`]);
\r
1043 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1044 (REWRITE_TAC[PRO_EXP]);
\r
1045 (REWRITE_WITH `((s2 - m + v % (s3 - s2)) dot (s2 - m)) /
\r
1046 ((s2 - m) dot (s2 - m:real^3)) = &1`);
\r
1047 (REWRITE_TAC[DOT_LADD; REAL_ARITH `(a + b) / c = a / c + b / c`]);
\r
1048 (REWRITE_WITH `((s2 - m) dot (s2 - m)) / ((s2 - m) dot (s2 - m:real^3)) = &1`);
\r
1049 (MATCH_MP_TAC REAL_DIV_REFL);
\r
1050 (REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0;NORM_EQ_0]);
\r
1051 (REWRITE_TAC[VECTOR_ARITH `s2 - m = vec 0 <=> s2 = m`]);
\r
1054 (NEW_GOAL `between s2 (u0, s1:real^3)`);
\r
1055 (ASM_MESON_TAC[]);
\r
1056 (NEW_GOAL `s2 IN affine hull {u0, s1:real^3}`);
\r
1057 (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);
\r
1059 (NEW_GOAL `convex hull {u0,s1:real^3} SUBSET affine hull {u0,s1}`);
\r
1060 (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
\r
1061 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
\r
1062 (NEW_GOAL `affine hull {u0,s1,s2} = affine hull {u0, s1:real^3}`);
\r
1063 (MATCH_MP_TAC AFFINE_HULLS_EQ);
\r
1064 (REWRITE_TAC[SUBSET; SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`]);
\r
1065 (REPEAT STRIP_TAC);
\r
1066 (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);
\r
1067 (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);
\r
1068 (ASM_MESON_TAC[]);
\r
1070 (REWRITE_TAC[SUBSET; SET_RULE `x IN {b,c} <=> x = b \/ x = c`]);
\r
1071 (REPEAT STRIP_TAC);
\r
1072 (ASM_REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);
\r
1073 (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);
\r
1076 (VECTOR_ARITH_TAC);
\r
1077 (ASM_REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);
\r
1078 (EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0`);
\r
1081 (VECTOR_ARITH_TAC);
\r
1083 (NEW_GOAL `aff_dim {u0,s1,s2:real^3} <= &1`);
\r
1084 (ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL]);
\r
1085 (ONCE_ASM_REWRITE_TAC[]);
\r
1086 (ONCE_REWRITE_TAC[AFF_DIM_AFFINE_HULL]);
\r
1087 (MATCH_MP_TAC (ARITH_RULE `(?x. x <= &1 /\ y <= x:int) ==> y <= &1`));
\r
1088 (EXISTS_TAC `&(CARD {u0,s1:real^3}):int - &1`);
\r
1090 (REWRITE_TAC[ARITH_RULE `a:int - &1 <= &1 <=> a <= &2`; INT_OF_NUM_LE]);
\r
1091 (REWRITE_TAC[Geomdetail.CARD2]);
\r
1092 (MATCH_MP_TAC AFF_DIM_LE_CARD);
\r
1093 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
1095 (NEW_GOAL `aff_dim {u0,s1,s2:real^3} = &2`);
\r
1097 (NEW_GOAL `vl:(real^3)list = truncate_simplex 2 ul`);
\r
1098 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
1099 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1100 (REWRITE_WITH `aff_dim {u0,s1,s2:real^3} =
\r
1101 aff_dim {omega_list_n V vl j | j IN 0..2}`);
\r
1103 (REWRITE_TAC[IN_NUMSEG_0]);
\r
1104 (REWRITE_TAC[SET_EQ_LEMMA;
\r
1105 SET_RULE `x IN {a,b,c} <=> (x = a \/ x = b \/ x = c)`; IN;IN_ELIM_THM]);
\r
1106 (REPEAT STRIP_TAC);
\r
1108 (REWRITE_TAC[ARITH_RULE `0 <= 2`; OMEGA_LIST_N]);
\r
1109 (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);
\r
1110 (ASM_REWRITE_TAC[]);
\r
1113 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);
\r
1114 (EXPAND_TAC "vl");
\r
1115 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1117 (EXPAND_TAC "s1");
\r
1118 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);
\r
1121 (REWRITE_TAC[ARITH_RULE `2 <= 2`; ASSUME `x = s2:real^3`] THEN EXPAND_TAC "vl" THEN DEL_TAC);
\r
1122 (EXPAND_TAC "s2");
\r
1123 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
\r
1124 (REWRITE_TAC[set_of_list; OMEGA_LIST_TRUNCATE_2;
\r
1125 OMEGA_LIST_TRUNCATE_2_NEW1]);
\r
1127 (ASM_CASES_TAC `j = 0`);
\r
1129 (REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`; OMEGA_LIST_N; HD]);
\r
1130 (EXPAND_TAC "vl");
\r
1131 (REWRITE_TAC[ASSUME `j = 0`]);
\r
1132 (REWRITE_TAC[OMEGA_LIST_N; HD]);
\r
1134 (ASM_CASES_TAC `j = 1`);
\r
1137 (ASM_REWRITE_TAC[]);
\r
1138 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
\r
1139 (EXPAND_TAC "s1");
\r
1140 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);
\r
1142 (ASM_CASES_TAC `j = 2`);
\r
1145 (REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`]);
\r
1146 (EXPAND_TAC "vl");
\r
1147 (EXPAND_TAC "s2");
\r
1148 (REWRITE_TAC[ASSUME `j = 2`; OMEGA_LIST_TRUNCATE_2; OMEGA_LIST_TRUNCATE_2_NEW1]);
\r
1149 (SUBGOAL_THEN `F` MP_TAC);
\r
1153 (MATCH_MP_TAC XNHPWAB3);
\r
1154 (ASM_REWRITE_TAC[IN]);
\r
1156 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1157 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
1158 (ASM_MESON_TAC[]);
\r
1159 (ASM_MESON_TAC[]);
\r
1162 (* ========================================================================= *)
\r
1164 (* ========================================================================== *)
\r
1165 (MATCH_MP_TAC (REAL_ARITH `x = &0 ==> a + x = a`));
\r
1166 (REWRITE_TAC[DOT_LMUL]);
\r
1167 (REWRITE_WITH `(s3 - s2) dot (s2 - m:real^3) = &0`);
\r
1168 (ONCE_REWRITE_TAC[VECTOR_ARITH `a dot (b - c) = -- (a dot (c - b))`]);
\r
1169 (ONCE_REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]);
\r
1170 (REWRITE_TAC[ASSUME `s2:real^3 = circumcenter (set_of_list vl)`]);
\r
1171 (MATCH_MP_TAC MHFTTZN4);
\r
1172 (EXISTS_TAC `V:real^3->bool`);
\r
1174 (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
\r
1175 (EXPAND_TAC "vl" THEN DEL_TAC);
\r
1176 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1177 (REPEAT STRIP_TAC);
\r
1178 (ASM_REWRITE_TAC[]);
\r
1180 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1182 (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
\r
1184 (* ========================================================================== *)
\r
1185 (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
\r
1186 (ASM_REWRITE_TAC[]);
\r
1187 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);
\r
1188 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
1189 (UNDISCH_TAC `between m (u0,s1:real^3)`);
\r
1190 (REWRITE_WITH `s1 = midpoint (u0,u1:real^3)`);
\r
1191 (EXPAND_TAC "s1");
\r
1193 (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 =
\r
1194 omega_list_n V [u0; u1:real^3] 1`);
\r
1195 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2;OMEGA_LIST_TRUNCATE_1]);
\r
1196 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2]);
\r
1197 (REWRITE_WITH `omega_list V [u0; u1:real^3] =
\r
1198 circumcenter (set_of_list [u0;u1])`);
\r
1199 (MATCH_MP_TAC XNHPWAB1);
\r
1201 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
\r
1203 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
\r
1204 (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
1205 (REWRITE_TAC[IN] THEN STRIP_TAC);
\r
1206 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1207 (EXISTS_TAC `2` THEN REWRITE_TAC[ARITH_RULE `1 <= 2`]);
\r
1208 (REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`);
\r
1209 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
1210 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1211 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1212 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
1214 (NEW_GOAL `!i j. i < j /\ j <= 2
\r
1215 ==> hl (truncate_simplex i (vl:(real^3)list))
\r
1216 < hl (truncate_simplex j vl)`);
\r
1218 (MATCH_MP_TAC XNHPWAB4);
\r
1219 (EXISTS_TAC `V:real^3->bool`);
\r
1220 (ASM_REWRITE_TAC[IN]);
\r
1221 (REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`);
\r
1222 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
1223 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1224 (ASM_REWRITE_TAC[]);
\r
1225 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1226 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
1227 (ASM_MESON_TAC[]);
\r
1228 (NEW_GOAL `hl (truncate_simplex 1 (vl:(real^3)list)) < hl (truncate_simplex 2 vl)`);
\r
1229 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
1232 (NEW_GOAL `truncate_simplex 2 vl = truncate_simplex 2 ul:(real^3)list`);
\r
1233 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
1234 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1235 (MATCH_MP_TAC (REAL_ARITH `a < hl (truncate_simplex 2 (vl:(real^3)list)) /\
\r
1236 hl (truncate_simplex 2 vl) < b ==> a < b`));
\r
1237 (ASM_REWRITE_TAC[]);
\r
1238 (ASM_MESON_TAC[]);
\r
1239 (REWRITE_TAC[set_of_list;Rogers.CIRCUMCENTER_2]);
\r
1240 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; midpoint; IN; IN_ELIM_THM; AFFINE_HULL_3]);
\r
1241 (REPEAT STRIP_TAC);
\r
1242 (EXISTS_TAC `u' + v' * inv (&2)`);
\r
1243 (EXISTS_TAC `v' * inv (&2)`);
\r
1244 (EXISTS_TAC `&0`);
\r
1246 (REWRITE_TAC[REAL_ARITH `(u' + v' * inv (&2)) + v' * inv (&2) + &0 = u' + v'`]);
\r
1247 (ASM_REWRITE_TAC[]);
\r
1248 (ASM_REWRITE_TAC[]);
\r
1249 (VECTOR_ARITH_TAC);
\r
1250 (REWRITE_TAC[REAL_MUL_RZERO; REAL_ARITH `&0 / x = &0`]);
\r
1251 (VECTOR_ARITH_TAC);
\r
1253 (* ========================================================================== *)
\r
1255 (NEW_GOAL `norm (u0 - p:real^3) pow 2 =
\r
1256 norm ((p'+ m) - p) pow 2 + norm (u0 - (p' + m)) pow 2`);
\r
1257 (MATCH_MP_TAC PYTHAGORAS);
\r
1258 (REWRITE_WITH `p - (p'+ m) = projection (s2 - m) (p - m:real^3)`);
\r
1259 (REWRITE_TAC[VECTOR_ARITH `p - (a + b:real^3) = (p - b) - a`]);
\r
1260 (EXPAND_TAC "p'" THEN REWRITE_TAC[proj_point]);
\r
1261 (UNDISCH_TAC `between (p - m) (vec 0,n - m:real^3)`);
\r
1262 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN;
\r
1263 IN_ELIM_THM; VECTOR_MUL_RZERO;VECTOR_ADD_LID]);
\r
1264 (REPEAT STRIP_TAC);
\r
1265 (VECTOR_ARITH_TAC);
\r
1266 (NEW_GOAL `(?k. k <= &1 /\ &0 <= k /\
\r
1267 projection (s2 - m) (p - m:real^3) = k % projection (s2 - m) (n - m))`);
\r
1268 (MATCH_MP_TAC PARALLEL_PROJECTION);
\r
1269 (ASM_REWRITE_TAC[]);
\r
1271 (NEW_GOAL `s2 = m:real^3`);
\r
1272 (ASM_REWRITE_TAC[]);
\r
1273 (SWITCH_TAC THEN DEL_TAC);
\r
1275 (NEW_GOAL `between s2 (u0, s1:real^3)`);
\r
1276 (ASM_MESON_TAC[]);
\r
1277 (NEW_GOAL `s2 IN affine hull {u0, s1:real^3}`);
\r
1278 (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);
\r
1280 (NEW_GOAL `convex hull {u0,s1:real^3} SUBSET affine hull {u0,s1}`);
\r
1281 (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
\r
1282 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
\r
1284 (NEW_GOAL `affine hull {u0,s1,s2} = affine hull {u0, s1:real^3}`);
\r
1285 (MATCH_MP_TAC AFFINE_HULLS_EQ);
\r
1286 (REWRITE_TAC[SUBSET; SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`]);
\r
1287 (REPEAT STRIP_TAC);
\r
1288 (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);
\r
1289 (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);
\r
1290 (ASM_MESON_TAC[]);
\r
1292 (REWRITE_TAC[SUBSET; SET_RULE `x IN {b,c} <=> x = b \/ x = c`]);
\r
1293 (REPEAT STRIP_TAC);
\r
1294 (ASM_REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);
\r
1295 (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);
\r
1298 (VECTOR_ARITH_TAC);
\r
1299 (REWRITE_TAC[ASSUME `x = s1:real^3`;AFFINE_HULL_3;IN;IN_ELIM_THM]);
\r
1300 (EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0`);
\r
1303 (VECTOR_ARITH_TAC);
\r
1305 (NEW_GOAL `aff_dim {u0,s1,s2:real^3} <= &1`);
\r
1306 (ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL]);
\r
1307 (ONCE_ASM_REWRITE_TAC[]);
\r
1308 (ONCE_REWRITE_TAC[AFF_DIM_AFFINE_HULL]);
\r
1309 (MATCH_MP_TAC (ARITH_RULE `(?x. x <= &1 /\ y <= x:int) ==> y <= &1`));
\r
1310 (EXISTS_TAC `&(CARD {u0,s1:real^3}):int - &1`);
\r
1312 (REWRITE_TAC[ARITH_RULE `a:int - &1 <= &1 <=> a <= &2`; INT_OF_NUM_LE]);
\r
1313 (REWRITE_TAC[Geomdetail.CARD2]);
\r
1314 (MATCH_MP_TAC AFF_DIM_LE_CARD);
\r
1315 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
1317 (NEW_GOAL `aff_dim {u0,s1,s2:real^3} = &2`);
\r
1319 (NEW_GOAL `vl:(real^3)list = truncate_simplex 2 ul`);
\r
1320 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
1321 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1322 (REWRITE_WITH `aff_dim {u0,s1,s2:real^3} =
\r
1323 aff_dim {omega_list_n V vl j | j IN 0..2}`);
\r
1325 (REWRITE_TAC[IN_NUMSEG_0]);
\r
1326 (REWRITE_TAC[SET_EQ_LEMMA;
\r
1327 SET_RULE `x IN {a,b,c} <=> (x = a \/ x = b \/ x = c)`; IN;IN_ELIM_THM]);
\r
1328 (REPEAT STRIP_TAC);
\r
1330 (REWRITE_TAC[ARITH_RULE `0 <= 2`; OMEGA_LIST_N]);
\r
1331 (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);
\r
1332 (ASM_REWRITE_TAC[]);
\r
1335 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);
\r
1336 (EXPAND_TAC "vl");
\r
1337 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1339 (EXPAND_TAC "s1");
\r
1340 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);
\r
1343 (REWRITE_TAC[ARITH_RULE `2 <= 2`; ASSUME `x = s2:real^3`] THEN EXPAND_TAC "vl" THEN DEL_TAC);
\r
1344 (EXPAND_TAC "s2");
\r
1345 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
\r
1346 (REWRITE_TAC[set_of_list; OMEGA_LIST_TRUNCATE_2;
\r
1347 OMEGA_LIST_TRUNCATE_2_NEW1]);
\r
1349 (ASM_CASES_TAC `j = 0`);
\r
1351 (REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`; OMEGA_LIST_N; HD]);
\r
1352 (EXPAND_TAC "vl");
\r
1353 (REWRITE_TAC[ASSUME `j = 0`]);
\r
1354 (REWRITE_TAC[OMEGA_LIST_N; HD]);
\r
1356 (ASM_CASES_TAC `j = 1`);
\r
1359 (ASM_REWRITE_TAC[]);
\r
1360 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
\r
1361 (EXPAND_TAC "s1");
\r
1362 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);
\r
1364 (ASM_CASES_TAC `j = 2`);
\r
1367 (REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`]);
\r
1368 (EXPAND_TAC "vl");
\r
1369 (EXPAND_TAC "s2");
\r
1370 (REWRITE_TAC[ASSUME `j = 2`; OMEGA_LIST_TRUNCATE_2; OMEGA_LIST_TRUNCATE_2_NEW1]);
\r
1371 (SUBGOAL_THEN `F` MP_TAC);
\r
1375 (MATCH_MP_TAC XNHPWAB3);
\r
1376 (ASM_REWRITE_TAC[IN]);
\r
1378 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1379 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
1380 (ASM_MESON_TAC[]);
\r
1381 (ASM_MESON_TAC[]);
\r
1384 (FIRST_X_ASSUM CHOOSE_TAC);
\r
1385 (UP_ASM_TAC THEN STRIP_TAC);
\r
1388 (REWRITE_TAC[ASSUME `projection (s2 - m) (p - m:real^3) =
\r
1389 k % projection (s2 - m) (n - m)`]);
\r
1390 (REWRITE_TAC[projection_proj_point; orthogonal]);
\r
1391 (REWRITE_TAC[ASSUME `proj_point (s2 - m) (n - m:real^3) = n'`]);
\r
1392 (REWRITE_TAC[ASSUME `n' = s2 - m:real^3`;
\r
1393 VECTOR_ARITH `n - m - (a - m:real^3) = n - a`]);
\r
1394 (UNDISCH_TAC `between n (s2,s3:real^3)`);
\r
1395 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM] THEN
\r
1396 REPEAT STRIP_TAC);
\r
1397 (REWRITE_TAC[ASSUME `n = u % s2 + v % s3:real^3`]);
\r
1398 (REWRITE_WITH `(u % s2 + v % s3:real^3) - s2 = (u % s2 + v % s3) - (u + v) % s2`);
\r
1399 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1400 (REWRITE_TAC[VECTOR_ARITH
\r
1401 `(u % s2 + v % s3) - (u + v) % s2 = v % (s3 - s2:real^3)`]);
\r
1402 (ONCE_REWRITE_TAC[VECTOR_ARITH
\r
1403 `u0 - (p' + m) = ((u0:real^3) + s2 - (p' + m)) - s2`]);
\r
1404 (NEW_GOAL `(s3 - s2:real^3) dot ((u0 + s2 - (p' + m)) - s2) = &0`);
\r
1405 (ASM_REWRITE_TAC[]);
\r
1406 (MATCH_MP_TAC MHFTTZN4);
\r
1407 (EXISTS_TAC `V:real^3->bool`);
\r
1409 (ASM_REWRITE_TAC[]);
\r
1411 (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
\r
1412 (ASM_REWRITE_TAC[]);
\r
1413 (EXPAND_TAC "vl");
\r
1414 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1415 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1416 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
1418 (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
\r
1419 (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
\r
1420 (ASM_REWRITE_TAC[]);
\r
1421 (EXPAND_TAC "vl");
\r
1422 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1423 (ASM_REWRITE_TAC[]);
\r
1424 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
1426 (NEW_GOAL `!a b c m n p.
\r
1427 m IN affine hull {a,b,c:real^3} /\
\r
1428 n IN affine hull {a,b,c} /\
\r
1429 p IN affine hull {a,b,c}
\r
1430 ==> m + n - p IN affine hull {a,b,c}`);
\r
1431 (REWRITE_TAC[AFFINE_HULL_3; IN;IN_ELIM_THM]);
\r
1432 (REPEAT STRIP_TAC);
\r
1433 (EXISTS_TAC `(u' + u'') - u'''`);
\r
1434 (EXISTS_TAC `(v' + v'') - v'''`);
\r
1435 (EXISTS_TAC `(w + w') - w''`);
\r
1437 (ASM_REAL_ARITH_TAC);
\r
1438 (ASM_REWRITE_TAC[]);
\r
1439 (VECTOR_ARITH_TAC);
\r
1440 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
1442 (REPEAT STRIP_TAC);
\r
1444 (REWRITE_TAC[AFFINE_HULL_3; IN;IN_ELIM_THM]);
\r
1445 (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);
\r
1447 (ASM_REAL_ARITH_TAC);
\r
1448 (VECTOR_ARITH_TAC);
\r
1451 (MATCH_MP_TAC Rogers.OAPVION1);
\r
1454 (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
\r
1455 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
1456 (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);
\r
1458 (EXISTS_TAC `V:real^3->bool`);
\r
1460 (ASM_REWRITE_TAC[]);
\r
1461 (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
\r
1462 (ASM_REWRITE_TAC[]);
\r
1463 (EXPAND_TAC "vl");
\r
1464 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1465 (MATCH_MP_TAC Packing3. TRUNCATE_SIMPLEX_BARV);
\r
1466 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
1468 (EXPAND_TAC "p'");
\r
1469 (REWRITE_TAC[PRO_EXP]);
\r
1470 (ABBREV_TAC `h = ((p - m) dot (s2 - m)) / ((s2 - m) dot (s2 - m:real^3))`);
\r
1472 (NEW_GOAL `!a b c x y r.
\r
1473 x IN affine hull {a,b,c:real^3} /\
\r
1474 y IN affine hull {a,b,c}
\r
1475 ==> r % (x - y) + y IN affine hull {a,b,c}`);
\r
1476 (REWRITE_TAC[AFFINE_HULL_3; IN;IN_ELIM_THM]);
\r
1477 (REPEAT STRIP_TAC);
\r
1478 (EXISTS_TAC `r * (u' - u'') + u''`);
\r
1479 (EXISTS_TAC `r * (v' - v'') + v''`);
\r
1480 (EXISTS_TAC `r * (w - w') + w'`);
\r
1482 (REWRITE_TAC[REAL_ARITH
\r
1483 `(r * (u' - u'') + u'') + (r * (v' - v'') + v'') + r * (w - w') + w' =
\r
1484 r * (u' + v' + w) - r * (u'' + v'' + w') + (u'' + v'' + w')`]);
\r
1485 (ASM_REWRITE_TAC[REAL_MUL_RID]);
\r
1486 (ASM_REAL_ARITH_TAC);
\r
1487 (ASM_REWRITE_TAC[]);
\r
1488 (VECTOR_ARITH_TAC);
\r
1489 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
1490 (ASM_REWRITE_TAC[]);
\r
1494 (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
\r
1495 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
1496 (MATCH_MP_TAC Rogers.OAPVION1);
\r
1498 (REWRITE_WITH `set_of_list vl = {u0, u1, u2:real^3}`);
\r
1499 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
1501 (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);
\r
1502 (EXISTS_TAC `V:real^3->bool`);
\r
1504 (ASM_REWRITE_TAC[]);
\r
1505 (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
\r
1506 (ASM_REWRITE_TAC[]);
\r
1507 (EXPAND_TAC "vl");
\r
1508 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1509 (MATCH_MP_TAC Packing3. TRUNCATE_SIMPLEX_BARV);
\r
1510 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
1512 (UNDISCH_TAC `between m (u0,s1:real^3)`);
\r
1513 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;
\r
1514 AFFINE_HULL_3;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
\r
1517 (REWRITE_WITH `s1 = midpoint (u0,u1:real^3)`);
\r
1518 (REWRITE_TAC[GSYM (ASSUME `omega_list_n V [u0; u1; u2; u3:real^3] 1 = s1`)]);
\r
1519 (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 =
\r
1520 omega_list_n V [u0; u1:real^3] 1`);
\r
1521 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2;OMEGA_LIST_TRUNCATE_1]);
\r
1522 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2]);
\r
1523 (REWRITE_WITH `omega_list V [u0; u1:real^3] =
\r
1524 circumcenter (set_of_list [u0;u1])`);
\r
1525 (MATCH_MP_TAC XNHPWAB1);
\r
1527 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
\r
1529 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
\r
1530 (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
1531 (REWRITE_TAC[IN] THEN STRIP_TAC);
\r
1532 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1533 (EXISTS_TAC `2` THEN REWRITE_TAC[ARITH_RULE `1 <= 2`]);
\r
1534 (REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`);
\r
1535 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
1536 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1537 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1538 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
1540 (NEW_GOAL `!i j. i < j /\ j <= 2
\r
1541 ==> hl (truncate_simplex i (vl:(real^3)list))
\r
1542 < hl (truncate_simplex j vl)`);
\r
1544 (MATCH_MP_TAC XNHPWAB4);
\r
1545 (EXISTS_TAC `V:real^3->bool`);
\r
1546 (ASM_REWRITE_TAC[IN]);
\r
1547 (REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`);
\r
1548 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
1549 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1550 (ASM_REWRITE_TAC[]);
\r
1551 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1552 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
1553 (ASM_MESON_TAC[]);
\r
1554 (NEW_GOAL `hl (truncate_simplex 1 (vl:(real^3)list)) < hl (truncate_simplex 2 vl)`);
\r
1555 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
1558 (NEW_GOAL `truncate_simplex 2 vl = truncate_simplex 2 ul:(real^3)list`);
\r
1559 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
1560 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1561 (MATCH_MP_TAC (REAL_ARITH `a < hl (truncate_simplex 2 (vl:(real^3)list)) /\
\r
1562 hl (truncate_simplex 2 vl) < b ==> a < b`));
\r
1563 (ASM_REWRITE_TAC[]);
\r
1564 (ASM_MESON_TAC[]);
\r
1565 (REWRITE_TAC[set_of_list;Rogers.CIRCUMCENTER_2]);
\r
1566 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; midpoint; IN; IN_ELIM_THM; AFFINE_HULL_3]);
\r
1567 (REPEAT STRIP_TAC);
\r
1568 (EXISTS_TAC `u' + v' * inv (&2)`);
\r
1569 (EXISTS_TAC `v' * inv (&2)`);
\r
1570 (EXISTS_TAC `&0`);
\r
1572 (REWRITE_TAC[REAL_ARITH `(u' + v' * inv (&2)) + v' * inv (&2) + &0 = u' + v'`]);
\r
1573 (ASM_REWRITE_TAC[]);
\r
1574 (ASM_REWRITE_TAC[]);
\r
1575 (VECTOR_ARITH_TAC);
\r
1577 (REWRITE_TAC[VECTOR_ARITH `a % b % c dot d = a * b * (c dot d)`]);
\r
1578 (ASM_REWRITE_TAC[]);
\r
1579 (REWRITE_TAC[REAL_MUL_RZERO]);
\r
1581 (* ========================================================================= *)
\r
1582 (NEW_GOAL `norm (u0 - s:real^3) pow 2 =
\r
1583 norm (s2 - s) pow 2 + norm (u0 - s2) pow 2`);
\r
1585 (MATCH_MP_TAC PYTHAGORAS);
\r
1586 (ASM_REWRITE_TAC[orthogonal]);
\r
1587 (MATCH_MP_TAC MHFTTZN4);
\r
1588 (EXISTS_TAC `V:real^3->bool`);
\r
1590 (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
\r
1591 (EXPAND_TAC "vl" THEN DEL_TAC);
\r
1592 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1593 (REPEAT STRIP_TAC);
\r
1594 (ASM_REWRITE_TAC[]);
\r
1595 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1597 (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
\r
1599 (UNDISCH_TAC `between s (s2,s3:real^3)`);
\r
1600 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
1601 (REPEAT STRIP_TAC);
\r
1602 (ONCE_REWRITE_TAC [GSYM IN]);
\r
1603 (ONCE_ASM_REWRITE_TAC[]);
\r
1604 (NEW_GOAL `convex (affine hull voronoi_list V
\r
1605 (truncate_simplex 2 [u0; u1; u2; u3:real^3]))`);
\r
1606 (MATCH_MP_TAC POLYHEDRON_IMP_CONVEX);
\r
1607 (REWRITE_TAC[POLYHEDRON_AFFINE_HULL]);
\r
1608 (UP_ASM_TAC THEN REWRITE_TAC[convex]);
\r
1610 (FIRST_ASSUM MATCH_MP_TAC);
\r
1611 (ASM_REWRITE_TAC[]);
\r
1612 (REPEAT STRIP_TAC);
\r
1613 (REWRITE_WITH `truncate_simplex 2 [u0; u1; u2; u3:real^3] = vl`);
\r
1614 (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1615 (NEW_GOAL `affine hull (voronoi_list V vl) INTER
\r
1616 affine hull (set_of_list vl) =
\r
1617 {circumcenter (set_of_list (vl:(real^3)list))}`);
\r
1618 (MATCH_MP_TAC Rogers.MHFTTZN3);
\r
1620 (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
\r
1621 (EXPAND_TAC "vl" THEN DEL_TAC);
\r
1622 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1623 (REPEAT STRIP_TAC);
\r
1624 (ASM_REWRITE_TAC[]);
\r
1625 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1627 (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
\r
1628 (UP_ASM_TAC THEN SET_TAC[]);
\r
1630 (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
\r
1631 (ASM_MESON_TAC[]);
\r
1632 (ASM_REWRITE_TAC[]);
\r
1633 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);
\r
1634 (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
\r
1637 (* ======================================================================== *)
\r
1639 (NEW_GOAL `norm (u0 - (p' + m)) pow 2 <= norm (u0 - s2:real^3) pow 2`);
\r
1640 (REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS; REAL_ABS_NORM;GSYM dist]);
\r
1641 (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]);
\r
1643 `(?y. y IN {m, s2:real^3} /\
\r
1644 (!x. x IN convex hull {m,s2} ==> norm (x - u0) <= norm (y - u0 )))`);
\r
1645 (MATCH_MP_TAC SIMPLEX_FURTHEST_LE);
\r
1647 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
1649 (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE `x IN {a, b} <=> x = b \/ x = a`]
\r
1650 THEN REPEAT STRIP_TAC);
\r
1651 (UP_ASM_TAC THEN REWRITE_TAC[ASSUME `y' = s2:real^3`]);
\r
1652 (DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
\r
1653 (UNDISCH_TAC `between p' (vec 0,n':real^3)`);
\r
1654 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
1655 (REPEAT STRIP_TAC);
\r
1656 (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN ASM_REWRITE_TAC[]);
\r
1657 (REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; VECTOR_ARITH
\r
1658 `a % (x - y) + y = b % y + a % x <=> ((b + a) - &1) % y = vec 0`]);
\r
1659 (ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO]);
\r
1660 (MATCH_MP_TAC (REAL_ARITH `(?s. a <= s /\ s <= b) ==> a <= b`));
\r
1662 (EXISTS_TAC `norm (m - u0:real^3)`);
\r
1664 (UP_ASM_TAC THEN REWRITE_TAC[ASSUME `y' = m:real^3`]);
\r
1665 (DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
\r
1666 (UNDISCH_TAC `between p' (vec 0,n':real^3)`);
\r
1667 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
1668 (REPEAT STRIP_TAC);
\r
1669 (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN ASM_REWRITE_TAC[]);
\r
1670 (REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; VECTOR_ARITH
\r
1671 `a % (x - y) + y = b % y + a % x <=> ((b + a) - &1) % y = vec 0`]);
\r
1672 (ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO]);
\r
1674 (MATCH_MP_TAC (REAL_ARITH `(?s. a <= s /\ s <= b) ==> a <= b`));
\r
1675 (EXISTS_TAC `norm (s1 - u0:real^3)`);
\r
1677 (REWRITE_TAC[GSYM dist]);
\r
1678 (ONCE_REWRITE_TAC[DIST_SYM]);
\r
1679 (UNDISCH_TAC `between m (u0,s1:real^3)`);
\r
1680 (REWRITE_TAC[between]);
\r
1682 (ASM_REWRITE_TAC[]);
\r
1683 (REWRITE_TAC[REAL_ARITH `a <= a + b <=> &0 <= b`; DIST_POS_LE]);
\r
1684 (NEW_GOAL `norm (s2 - u0:real^3) pow 2 =
\r
1685 norm (s1 - u0) pow 2 + norm (s2 - s1) pow 2`);
\r
1686 (MATCH_MP_TAC PYTHAGORAS);
\r
1688 (ABBREV_TAC `sl = [u0;u1:real^3]`);
\r
1689 (NEW_GOAL `s1:real^3 = circumcenter (set_of_list sl)`);
\r
1690 (EXPAND_TAC "s1" THEN EXPAND_TAC "sl");
\r
1691 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]);
\r
1692 (MATCH_MP_TAC XNHPWAB1);
\r
1694 (REWRITE_WITH `[u0; u1:real^3] = truncate_simplex 1 ul`);
\r
1695 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
1696 (ASM_REWRITE_TAC[IN]);
\r
1698 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1700 (ASM_MESON_TAC[ARITH_RULE `1 <= 3`]);
\r
1701 (DEL_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
1702 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
\r
1703 (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
1705 (NEW_GOAL `!i j. i < j /\ j <= 2
\r
1706 ==> hl (truncate_simplex i (vl:(real^3)list))
\r
1707 < hl (truncate_simplex j vl)`);
\r
1709 (MATCH_MP_TAC XNHPWAB4);
\r
1710 (EXISTS_TAC `V:real^3->bool`);
\r
1711 (ASM_REWRITE_TAC[IN]);
\r
1712 (REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`);
\r
1713 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
1714 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1715 (ASM_REWRITE_TAC[]);
\r
1716 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1717 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
1718 (ASM_MESON_TAC[]);
\r
1719 (NEW_GOAL `hl (truncate_simplex 1 (vl:(real^3)list)) < hl (truncate_simplex 2 vl)`);
\r
1720 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
1723 (NEW_GOAL `truncate_simplex 2 vl = truncate_simplex 2 ul:(real^3)list`);
\r
1724 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
1725 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1726 (MATCH_MP_TAC (REAL_ARITH `a < hl (truncate_simplex 2 (vl:(real^3)list)) /\
\r
1727 hl (truncate_simplex 2 vl) < b ==> a < b`));
\r
1728 (ASM_REWRITE_TAC[]);
\r
1729 (ASM_MESON_TAC[]);
\r
1731 (REWRITE_TAC [ASSUME `s1:real^3 = circumcenter (set_of_list sl)`;orthogonal]);
\r
1732 (ONCE_REWRITE_TAC[DOT_SYM]);
\r
1733 (MATCH_MP_TAC MHFTTZN4);
\r
1735 (EXISTS_TAC `V:real^3->bool`);
\r
1737 (ASM_REWRITE_TAC[]);
\r
1739 (REWRITE_WITH `sl:(real^3)list = truncate_simplex 1 ul`);
\r
1740 (ASM_REWRITE_TAC[]);
\r
1741 (EXPAND_TAC "sl");
\r
1742 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
1743 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1744 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
\r
1747 (NEW_GOAL `affine hull (voronoi_list V vl) SUBSET
\r
1748 affine hull (voronoi_list V (sl:(real^3)list))`);
\r
1749 (MATCH_MP_TAC AFFINE_SUBSET_KY_LEMMA);
\r
1750 (EXPAND_TAC "sl" THEN EXPAND_TAC "vl" THEN REWRITE_TAC
\r
1751 [set_of_list; SET_RULE `x IN {a, b} <=> x = a \/ x = b`;
\r
1752 SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`;
\r
1753 VORONOI_LIST; VORONOI_SET;voronoi_closed; SUBSET;IN_INTERS]);
\r
1754 (REWRITE_TAC[IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
\r
1755 (FIRST_ASSUM MATCH_MP_TAC);
\r
1756 (EXISTS_TAC `v:real^3`);
\r
1757 (ASM_REWRITE_TAC[]);
\r
1758 (FIRST_ASSUM MATCH_MP_TAC);
\r
1759 (EXISTS_TAC `v:real^3`);
\r
1760 (ASM_REWRITE_TAC[]);
\r
1763 (MATCH_MP_TAC (SET_RULE `(?C. C SUBSET B /\ s IN C ) ==> s IN B`));
\r
1764 (EXISTS_TAC `affine hull voronoi_list V (vl:(real^3)list)`);
\r
1765 (ASM_REWRITE_TAC[]);
\r
1767 (NEW_GOAL `affine hull (voronoi_list V vl) INTER
\r
1768 affine hull (set_of_list vl) =
\r
1769 {circumcenter (set_of_list (vl:(real^3)list))}`);
\r
1770 (MATCH_MP_TAC Rogers.MHFTTZN3);
\r
1772 (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
\r
1773 (EXPAND_TAC "vl" THEN DEL_TAC);
\r
1774 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1775 (REPEAT STRIP_TAC);
\r
1776 (ASM_REWRITE_TAC[]);
\r
1777 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1779 (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
\r
1780 (UP_ASM_TAC THEN SET_TAC[]);
\r
1782 (EXPAND_TAC "sl" THEN REWRITE_TAC[set_of_list]);
\r
1783 (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
\r
1786 (REWRITE_WITH `norm (s1 - u0:real^3) <= norm (s2 - u0)
\r
1787 <=> norm (s1 - u0) pow 2 <= norm (s2 - u0) pow 2`);
\r
1788 (MATCH_MP_TAC Collect_geom.POW2_COND);
\r
1789 (REWRITE_TAC[NORM_POS_LE]);
\r
1790 (UP_ASM_TAC THEN MATCH_MP_TAC
\r
1791 (REAL_ARITH `(&0 <= c) ==> (a = b + c ==> b <= a)`));
\r
1792 (REWRITE_TAC[REAL_LE_POW_2]);
\r
1794 (* ==================================================================== *)
\r
1796 (NEW_GOAL `norm (u0 - s:real^3) < norm (u0 - p)`);
\r
1797 (MATCH_MP_TAC (REAL_ARITH `(?s. a <= s /\ s < b) ==> a < b`));
\r
1798 (EXISTS_TAC `sqrt (&2)`);
\r
1800 (REWRITE_TAC[GSYM dist]);
\r
1801 (ASM_REAL_ARITH_TAC);
\r
1802 (REWRITE_TAC[GSYM dist]);
\r
1803 (UNDISCH_TAC `dist (u0,p:real^3) >= sqrt (&2)`);
\r
1804 (MATCH_MP_TAC (REAL_ARITH `~(a = b) ==> (a >= b ==> b < a)`));
\r
1806 (NEW_GOAL `~(p:real^3 IN B2)`);
\r
1807 (ASM_SET_TAC[IN_DIFF]);
\r
1808 (UP_ASM_TAC THEN EXPAND_TAC "B2" THEN REWRITE_TAC[IN;IN_ELIM_THM]);
\r
1809 (ASM_REWRITE_TAC[HD; GSYM dist]);
\r
1810 (ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]);
\r
1812 (NEW_GOAL `norm (u0 - s:real^3) pow 2 < norm (u0 - p) pow 2`);
\r
1813 (REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS; REAL_ABS_NORM]);
\r
1814 (ASM_REWRITE_TAC[]);
\r
1816 (NEW_GOAL `norm (s2 - s:real^3) pow 2 < norm ((p' + m) - p:real^3) pow 2`);
\r
1817 (REWRITE_WITH `norm (s2 - s) pow 2 =
\r
1818 norm (u0 - s:real^3) pow 2 - norm (u0 - s2) pow 2`);
\r
1819 (ASM_REAL_ARITH_TAC);
\r
1820 (REWRITE_WITH `norm ((p' + m) - p) pow 2 =
\r
1821 norm (u0 - p:real^3) pow 2 - norm (u0 - (p' + m)) pow 2`);
\r
1822 (ASM_REAL_ARITH_TAC);
\r
1823 (ASM_REAL_ARITH_TAC);
\r
1825 (* ======================================================================== *)
\r
1827 (UNDISCH_TAC `p IN convex hull {u0, u1, u2, s:real^3}`);
\r
1828 (REWRITE_TAC[CONVEX_HULL_4; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
\r
1829 (NEW_GOAL `(?m1. m1 IN convex hull {u0, u1, u2} /\
\r
1830 between p (m1, s:real^3))`);
\r
1831 (ASM_CASES_TAC `(u + v + w = &0)`);
\r
1832 (NEW_GOAL `p = s:real^3`);
\r
1833 (ASM_REWRITE_TAC[]);
\r
1834 (REWRITE_WITH `u = &0 /\ v = &0 /\ w = &0 /\ z = &1`);
\r
1835 (ASM_REAL_ARITH_TAC);
\r
1836 (VECTOR_ARITH_TAC);
\r
1838 (NEW_GOAL `~(p:real^3 IN B2)`);
\r
1839 (ASM_SET_TAC[IN_DIFF]);
\r
1840 (UP_ASM_TAC THEN EXPAND_TAC "B2" THEN REWRITE_TAC[IN;IN_ELIM_THM]);
\r
1841 (ASM_REWRITE_TAC[HD; GSYM dist]);
\r
1842 (REWRITE_WITH `u = &0 /\ v = &0 /\ w = &0 /\ z = &1`);
\r
1843 (ASM_REAL_ARITH_TAC);
\r
1844 (REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_LID]);
\r
1845 (ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]);
\r
1846 (UP_ASM_TAC THEN MESON_TAC[]);
\r
1848 (EXISTS_TAC `(u / (u + v + w)) % u0 + (v / (u + v + w)) % u1 +
\r
1849 (w / (u + v + w)) % u2:real^3`);
\r
1850 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;CONVEX_HULL_3; IN;
\r
1851 IN_ELIM_THM] THEN REPEAT STRIP_TAC);
\r
1852 (EXISTS_TAC `u / (u + v + w)`);
\r
1853 (EXISTS_TAC `v / (u + v + w)`);
\r
1854 (EXISTS_TAC `w / (u + v + w)`);
\r
1855 (ASM_REWRITE_TAC[REAL_ARITH `a / x + b / x + c / x = (a + b + c) / x`]);
\r
1856 (REPEAT STRIP_TAC);
\r
1857 (MATCH_MP_TAC REAL_LE_DIV);
\r
1858 (ASM_REAL_ARITH_TAC);
\r
1859 (MATCH_MP_TAC REAL_LE_DIV);
\r
1860 (ASM_REAL_ARITH_TAC);
\r
1861 (MATCH_MP_TAC REAL_LE_DIV);
\r
1862 (ASM_REAL_ARITH_TAC);
\r
1863 (MATCH_MP_TAC REAL_DIV_REFL);
\r
1864 (ASM_REAL_ARITH_TAC);
\r
1865 (EXISTS_TAC `u + v + w:real`);
\r
1866 (EXISTS_TAC `z:real`);
\r
1867 (REPEAT STRIP_TAC);
\r
1868 (ASM_REAL_ARITH_TAC);
\r
1869 (ASM_REAL_ARITH_TAC);
\r
1870 (ASM_REAL_ARITH_TAC);
\r
1871 (ASM_REWRITE_TAC[]);
\r
1872 (REWRITE_TAC[VECTOR_ARITH `a % (x/ a % u0 + y / a % u1 + z / a % u2) =
\r
1873 (a / a) % (x % u0) + (a / a) % (y % u1) + (a / a) % (z % u2)`]);
\r
1874 (REWRITE_WITH `(u + v + w) / (u + v + w) = &1`);
\r
1875 (ASM_SIMP_TAC [REAL_DIV_REFL]);
\r
1876 (REWRITE_TAC[VECTOR_MUL_LID]);
\r
1877 (VECTOR_ARITH_TAC);
\r
1879 (UP_ASM_TAC THEN REPEAT STRIP_TAC);
\r
1881 (* ======================================================================== *)
\r
1883 (NEW_GOAL `(?k. k <= &1 /\ &0 <= k /\
\r
1884 projection (s2 - m) (p - m:real^3) = k % projection (s2 - m) (n - m))`);
\r
1885 (MATCH_MP_TAC PARALLEL_PROJECTION);
\r
1886 (ASM_REWRITE_TAC[]);
\r
1888 (NEW_GOAL `s2 = m:real^3`);
\r
1889 (ASM_REWRITE_TAC[]);
\r
1890 (SWITCH_TAC THEN DEL_TAC);
\r
1892 (NEW_GOAL `between s2 (u0, s1:real^3)`);
\r
1893 (ASM_MESON_TAC[]);
\r
1894 (NEW_GOAL `s2 IN affine hull {u0, s1:real^3}`);
\r
1895 (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);
\r
1897 (NEW_GOAL `convex hull {u0,s1:real^3} SUBSET affine hull {u0,s1}`);
\r
1898 (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
\r
1899 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
\r
1901 (NEW_GOAL `affine hull {u0,s1,s2} = affine hull {u0, s1:real^3}`);
\r
1902 (MATCH_MP_TAC AFFINE_HULLS_EQ);
\r
1903 (REWRITE_TAC[SUBSET; SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`]);
\r
1904 (REPEAT STRIP_TAC);
\r
1905 (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);
\r
1906 (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);
\r
1907 (ASM_MESON_TAC[]);
\r
1909 (REWRITE_TAC[SUBSET; SET_RULE `x IN {b,c} <=> x = b \/ x = c`]);
\r
1910 (REPEAT STRIP_TAC);
\r
1911 (ASM_REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);
\r
1912 (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);
\r
1915 (VECTOR_ARITH_TAC);
\r
1916 (REWRITE_TAC[ASSUME `x = s1:real^3`;AFFINE_HULL_3;IN;IN_ELIM_THM]);
\r
1917 (EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0`);
\r
1920 (VECTOR_ARITH_TAC);
\r
1922 (NEW_GOAL `aff_dim {u0,s1,s2:real^3} <= &1`);
\r
1923 (ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL]);
\r
1924 (ONCE_ASM_REWRITE_TAC[]);
\r
1925 (ONCE_REWRITE_TAC[AFF_DIM_AFFINE_HULL]);
\r
1926 (MATCH_MP_TAC (ARITH_RULE `(?x. x <= &1 /\ y <= x:int) ==> y <= &1`));
\r
1927 (EXISTS_TAC `&(CARD {u0,s1:real^3}):int - &1`);
\r
1929 (REWRITE_TAC[ARITH_RULE `a:int - &1 <= &1 <=> a <= &2`; INT_OF_NUM_LE]);
\r
1930 (REWRITE_TAC[Geomdetail.CARD2]);
\r
1931 (MATCH_MP_TAC AFF_DIM_LE_CARD);
\r
1932 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
1934 (NEW_GOAL `aff_dim {u0,s1,s2:real^3} = &2`);
\r
1936 (NEW_GOAL `vl:(real^3)list = truncate_simplex 2 ul`);
\r
1937 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
1938 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1939 (REWRITE_WITH `aff_dim {u0,s1,s2:real^3} =
\r
1940 aff_dim {omega_list_n V vl j | j IN 0..2}`);
\r
1942 (REWRITE_TAC[IN_NUMSEG_0]);
\r
1943 (REWRITE_TAC[SET_EQ_LEMMA;
\r
1944 SET_RULE `x IN {a,b,c} <=> (x = a \/ x = b \/ x = c)`; IN;IN_ELIM_THM]);
\r
1945 (REPEAT STRIP_TAC);
\r
1947 (REWRITE_TAC[ARITH_RULE `0 <= 2`; OMEGA_LIST_N]);
\r
1948 (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);
\r
1949 (ASM_REWRITE_TAC[]);
\r
1952 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);
\r
1953 (EXPAND_TAC "vl");
\r
1954 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1956 (EXPAND_TAC "s1");
\r
1957 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);
\r
1960 (REWRITE_TAC[ARITH_RULE `2 <= 2`; ASSUME `x = s2:real^3`] THEN EXPAND_TAC "vl" THEN DEL_TAC);
\r
1961 (EXPAND_TAC "s2");
\r
1962 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
\r
1963 (REWRITE_TAC[set_of_list; OMEGA_LIST_TRUNCATE_2;
\r
1964 OMEGA_LIST_TRUNCATE_2_NEW1]);
\r
1966 (ASM_CASES_TAC `j = 0`);
\r
1968 (REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`; OMEGA_LIST_N; HD]);
\r
1969 (EXPAND_TAC "vl");
\r
1970 (REWRITE_TAC[ASSUME `j = 0`]);
\r
1971 (REWRITE_TAC[OMEGA_LIST_N; HD]);
\r
1973 (ASM_CASES_TAC `j = 1`);
\r
1976 (ASM_REWRITE_TAC[]);
\r
1977 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
\r
1978 (EXPAND_TAC "s1");
\r
1979 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);
\r
1981 (ASM_CASES_TAC `j = 2`);
\r
1984 (REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`]);
\r
1985 (EXPAND_TAC "vl");
\r
1986 (EXPAND_TAC "s2");
\r
1987 (REWRITE_TAC[ASSUME `j = 2`; OMEGA_LIST_TRUNCATE_2; OMEGA_LIST_TRUNCATE_2_NEW1]);
\r
1988 (SUBGOAL_THEN `F` MP_TAC);
\r
1992 (MATCH_MP_TAC XNHPWAB3);
\r
1993 (ASM_REWRITE_TAC[IN]);
\r
1995 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1996 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
1997 (ASM_MESON_TAC[]);
\r
1998 (ASM_MESON_TAC[]);
\r
2001 (NEW_GOAL `?h. h <= &1 /\ &0 <= h /\
\r
2002 projection (s2 - m1:real^3) (p - m1) = h % projection (s2 - m1) (s - m1)`);
\r
2003 (MATCH_MP_TAC PARALLEL_PROJECTION);
\r
2004 (ASM_REWRITE_TAC[]);
\r
2006 (NEW_GOAL `s2 = m1:real^3`);
\r
2007 (ASM_REWRITE_TAC[]);
\r
2008 (SWITCH_TAC THEN DEL_TAC);
\r
2009 (NEW_GOAL `between p (s2, s:real^3)`);
\r
2010 (ASM_MESON_TAC[]);
\r
2011 (NEW_GOAL `between p (s3, s2:real^3)`);
\r
2012 (MATCH_MP_TAC BETWEEN_TRANS);
\r
2013 (EXISTS_TAC `s:real^3`);
\r
2015 (ASM_MESON_TAC[BETWEEN_SYM]);
\r
2016 (ASM_MESON_TAC[BETWEEN_SYM]);
\r
2018 (NEW_GOAL `p:real^3 IN B5`);
\r
2019 (EXPAND_TAC "B5");
\r
2020 (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);
\r
2021 (EXPAND_TAC "s2");
\r
2022 (EXPAND_TAC "s3");
\r
2023 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
2024 (MESON_TAC[SET_RULE `{a,b} = {b, a}`]);
\r
2025 (NEW_GOAL `~(p:real^3 IN B5)`);
\r
2026 (ASM_SET_TAC[IN_DIFF]);
\r
2027 (ASM_MESON_TAC[]);
\r
2029 (FIRST_X_ASSUM CHOOSE_TAC);
\r
2030 (FIRST_X_ASSUM CHOOSE_TAC);
\r
2032 (NEW_GOAL `projection (s2 - m1) (s - m1) = s - s2:real^3`);
\r
2033 (REWRITE_TAC[projection; VECTOR_ARITH `a - b - x % (d - b) = a - d
\r
2034 <=> (&1 - x) % (d - b:real^3) = vec 0`]);
\r
2035 (REWRITE_WITH `&1 - ((s - m1) dot (s2 - m1:real^3)) / ((s2 - m1) dot (s2 - m1)) = &0`);
\r
2036 (REWRITE_TAC[REAL_ARITH `&1 - a = &0 <=> a = &1`]);
\r
2037 (REWRITE_WITH `((s - m1) dot (s2 - m1)) / ((s2 - m1) dot (s2 - m1)) = &1
\r
2038 <=> ((s - m1) dot (s2 - m1)) = &1 * ((s2 - m1) dot (s2 - m1:real^3))`);
\r
2039 (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
\r
2040 (REWRITE_TAC[GSYM NORM_POW_2; GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT;
\r
2041 NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
\r
2044 (NEW_GOAL `between p (s2, s:real^3)`);
\r
2045 (ASM_MESON_TAC[]);
\r
2046 (NEW_GOAL `between p (s3, s2:real^3)`);
\r
2047 (MATCH_MP_TAC BETWEEN_TRANS);
\r
2048 (EXISTS_TAC `s:real^3`);
\r
2050 (ASM_MESON_TAC[BETWEEN_SYM]);
\r
2051 (ASM_MESON_TAC[BETWEEN_SYM]);
\r
2053 (NEW_GOAL `p:real^3 IN B5`);
\r
2054 (EXPAND_TAC "B5");
\r
2055 (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);
\r
2056 (EXPAND_TAC "s2");
\r
2057 (EXPAND_TAC "s3");
\r
2058 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
2059 (MESON_TAC[SET_RULE `{a,b} = {b, a}`]);
\r
2060 (NEW_GOAL `~(p:real^3 IN B5)`);
\r
2061 (ASM_SET_TAC[IN_DIFF]);
\r
2062 (ASM_MESON_TAC[]);
\r
2063 (REWRITE_TAC[REAL_MUL_LID]);
\r
2064 (ONCE_REWRITE_TAC[REAL_ARITH `a = b <=> a - b = &0`]);
\r
2065 (REWRITE_TAC[VECTOR_ARITH
\r
2066 `(s - m1) dot r - (s2 - m1) dot r = (s - s2) dot r:real^3`]);
\r
2067 (REWRITE_WITH `(s - s2) dot (s2 - m1) = --((s - s2) dot (m1 - s2:real^3))`);
\r
2068 (VECTOR_ARITH_TAC);
\r
2069 (ONCE_REWRITE_TAC[REAL_ARITH `-- a = &0 <=> a = &0`]);
\r
2070 (UNDISCH_TAC `between s (s2,s3:real^3)`);
\r
2071 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;IN;IN_ELIM_THM; CONVEX_HULL_2]);
\r
2072 (REPEAT STRIP_TAC);
\r
2073 (REWRITE_TAC[ASSUME `s = u' % s2 + v' % s3:real^3`]);
\r
2074 (REWRITE_WITH `(u' % s2 + v' % s3) - s2:real^3 =
\r
2075 (u' % s2 + v' % s3) - (u' + v') % s2`);
\r
2076 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
2077 (REWRITE_TAC[VECTOR_ARITH
\r
2078 `(u' % s2 + v' % s3) - (u' + v') % s2 = v' % (s3 - s2)`; DOT_LMUL]);
\r
2079 (REWRITE_WITH `(s3 - s2) dot (m1 - s2:real^3) = &0`);
\r
2080 (ASM_REWRITE_TAC[]);
\r
2084 (MATCH_MP_TAC MHFTTZN4);
\r
2085 (EXISTS_TAC `V:real^3->bool`);
\r
2087 (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
\r
2088 (EXPAND_TAC "vl" THEN DEL_TAC);
\r
2089 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
2090 (REPEAT STRIP_TAC);
\r
2091 (ASM_REWRITE_TAC[]);
\r
2092 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
2094 (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
\r
2095 (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
\r
2096 (ONCE_ASM_REWRITE_TAC[]);
\r
2098 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
\r
2099 TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);
\r
2100 (UNDISCH_TAC `m1 IN convex hull {u0, u1, u2:real^3}`);
\r
2101 (NEW_GOAL `convex hull {u0, u1, u2:real^3} SUBSET
\r
2102 affine hull {u0, u1, u2:real^3}`);
\r
2103 (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
\r
2104 (UP_ASM_TAC THEN SET_TAC[]);
\r
2106 (VECTOR_ARITH_TAC);
\r
2107 (ABBREV_TAC `M = projection (s2 - m1) (p - m1:real^3)`);
\r
2108 (ABBREV_TAC `N = projection (s2 - m) (p - m:real^3)`);
\r
2109 (NEW_GOAL `M = N:real^3`);
\r
2110 (NEW_GOAL `?r. N = r % M:real^3`);
\r
2111 (ASM_REWRITE_TAC[]);
\r
2112 (NEW_GOAL `projection (s2 - m) (n - m:real^3) = n - s2`);
\r
2113 (REWRITE_TAC[projection_proj_point; ASSUME `n' = s2 - m:real^3`;
\r
2114 ASSUME `proj_point (s2 - m) (n - m) = n':real^3`]);
\r
2115 (VECTOR_ARITH_TAC);
\r
2116 (REWRITE_WITH `circumcenter (set_of_list vl) = s2:real^3`);
\r
2117 (ASM_MESON_TAC[]);
\r
2118 (REWRITE_TAC[ASSUME `projection (s2 - m) (n - m) = n - s2:real^3`]);
\r
2119 (UNDISCH_TAC `between n (s2,s3:real^3)`);
\r
2120 (UNDISCH_TAC `between s (s2,s3:real^3)`);
\r
2121 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
2122 (REPEAT STRIP_TAC);
\r
2124 (REWRITE_TAC[ASSUME `n = u'' % s2 + v'' % s3:real^3`;
\r
2125 ASSUME `s = u' % s2 + v' % s3:real^3`]);
\r
2126 (REWRITE_WITH `(u' % s2 + v' % s3) - s2:real^3
\r
2127 = (u' % s2 + v' % s3) - (u' + v') % s2 /\
\r
2128 (u'' % s2 + v'' % s3) - s2
\r
2129 = (u'' % s2 + v'' % s3) - (u'' + v'') % s2`);
\r
2130 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
2131 (REWRITE_TAC[VECTOR_ARITH `(u % s + v % r) - (u + v) % s = v % (r - s)`]);
\r
2132 (REWRITE_TAC[VECTOR_MUL_ASSOC]);
\r
2133 (REWRITE_TAC[VECTOR_ARITH `a % x = b % x <=> (a - b) % x = vec 0`]);
\r
2134 (REWRITE_TAC[REAL_ARITH `(r * h) * v' = r * (h * v')`]);
\r
2135 (ASM_CASES_TAC `h * v' = &0`);
\r
2137 (ASM_CASES_TAC `h = &0`);
\r
2138 (NEW_GOAL `M:real^3 = vec 0`);
\r
2139 (ASM_REWRITE_TAC[VECTOR_MUL_LZERO]);
\r
2140 (UP_ASM_TAC THEN EXPAND_TAC "M" THEN REWRITE_TAC[projection]);
\r
2141 (ABBREV_TAC `kts = ((p - m1) dot (s2 - m1)) / ((s2 - m1) dot (s2 - m1:real^3))`);
\r
2142 (REWRITE_TAC [VECTOR_ARITH `a - p - c = vec 0 <=> a = p + c`]);
\r
2144 (NEW_GOAL `p IN affine hull {u0,u1,u2:real^3}`);
\r
2145 (REWRITE_TAC[ASSUME `p = m1 + kts % (s2 - m1:real^3)`]);
\r
2146 (MATCH_MP_TAC TRANSLATE_AFFINE_KY_LEMMA1);
\r
2147 (REWRITE_TAC[MESON[] `A /\ B /\ A <=> A /\ B`]);
\r
2149 (NEW_GOAL `convex hull {u0,u1,u2:real^3} SUBSET affine hull {u0, u1, u2}`);
\r
2150 (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
\r
2151 (UNDISCH_TAC `m1 IN convex hull {u0, u1, u2:real^3}`);
\r
2152 (UP_ASM_TAC THEN SET_TAC[]);
\r
2153 (ASM_REWRITE_TAC[]);
\r
2154 (EXPAND_TAC "vl");
\r
2155 (REWRITE_TAC[set_of_list]);
\r
2156 (MATCH_MP_TAC Rogers.OAPVION1);
\r
2159 (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
\r
2160 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
2161 (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);
\r
2163 (EXISTS_TAC `V:real^3->bool`);
\r
2165 (ASM_REWRITE_TAC[]);
\r
2166 (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
\r
2167 (ASM_REWRITE_TAC[]);
\r
2168 (EXPAND_TAC "vl");
\r
2169 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
2170 (MATCH_MP_TAC Packing3. TRUNCATE_SIMPLEX_BARV);
\r
2171 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
2173 (NEW_GOAL `~(p:real^3 IN B6)`);
\r
2174 (ASM_SET_TAC[IN_DIFF]);
\r
2175 (UP_ASM_TAC THEN EXPAND_TAC "B6");
\r
2176 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;HD;TL]);
\r
2177 (ASM_REWRITE_TAC[]);
\r
2178 (NEW_GOAL `v' = &0`);
\r
2179 (ASM_MESON_TAC[REAL_ENTIRE]);
\r
2180 (NEW_GOAL `s = s2:real^3`);
\r
2181 (ASM_REWRITE_TAC[]);
\r
2182 (REWRITE_WITH `u' = &1`);
\r
2183 (ASM_REAL_ARITH_TAC);
\r
2184 (REWRITE_TAC[VECTOR_MUL_LID]);
\r
2185 (VECTOR_ARITH_TAC);
\r
2187 (NEW_GOAL `!w. w IN {u0,u1,u2:real^3} ==>
\r
2188 radV {u0,u1,u2} = dist (circumcenter {u0,u1,u2},w)`);
\r
2189 (MATCH_MP_TAC Rogers.OAPVION2);
\r
2190 (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
\r
2191 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
2192 (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);
\r
2193 (EXISTS_TAC `V:real^3->bool`);
\r
2195 (ASM_REWRITE_TAC[]);
\r
2196 (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
\r
2197 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
2198 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
2200 (ASM_REWRITE_TAC[]);
\r
2203 (NEW_GOAL `hl (truncate_simplex 2 (ul:(real^3)list)) = dist (s2, u0:real^3)`);
\r
2204 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
\r
2205 TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list; HL]);
\r
2206 (REWRITE_WITH `s2 = circumcenter {u0,u1,u2:real^3}`);
\r
2207 (ASM_REWRITE_TAC[]);
\r
2208 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
2209 (FIRST_ASSUM MATCH_MP_TAC);
\r
2211 (NEW_GOAL `hl (truncate_simplex 2 (ul:(real^3)list)) = sqrt (&2)`);
\r
2212 (ONCE_ASM_REWRITE_TAC[]);
\r
2213 (REWRITE_TAC[GSYM (ASSUME `s = s2:real^3`)]);
\r
2214 (ONCE_REWRITE_TAC[DIST_SYM]);
\r
2215 (ASM_REWRITE_TAC[]);
\r
2216 (ASM_REAL_ARITH_TAC);
\r
2217 (UP_ASM_TAC THEN MESON_TAC[]);
\r
2218 (EXISTS_TAC `(k * v'') / (h * v')`);
\r
2219 (REWRITE_TAC[REAL_ARITH `k * v'' - (k * v'') / (h * v') * h * v' =
\r
2220 (k * v'') * (&1 - (h * v') / (h * v'))`]);
\r
2221 (REWRITE_WITH `(h * v') / (h * v') = &1`);
\r
2222 (MATCH_MP_TAC REAL_DIV_REFL);
\r
2223 (ASM_REWRITE_TAC[]);
\r
2224 (REWRITE_TAC[REAL_SUB_REFL;REAL_MUL_RZERO; VECTOR_MUL_LZERO]);
\r
2225 (FIRST_X_ASSUM CHOOSE_TAC);
\r
2227 (NEW_GOAL `r = &1`);
\r
2228 (ASM_CASES_TAC `r = &1`);
\r
2229 (ASM_REWRITE_TAC[]);
\r
2230 (NEW_GOAL `p IN affine hull {u0,u1,u2:real^3}`);
\r
2231 (MATCH_MP_TAC IN_AFFINE_HULL_KY_LEMMA3_alt);
\r
2232 (EXISTS_TAC `M:real^3`);
\r
2233 (EXISTS_TAC `r:real`);
\r
2234 (REWRITE_WITH `p - M = (m1:real^3) + proj_point (s2 - m1) (p - m1)`);
\r
2235 (EXPAND_TAC "M" THEN REWRITE_TAC[proj_point]);
\r
2236 (VECTOR_ARITH_TAC);
\r
2237 (REWRITE_WITH `p - r % M =(m:real^3) + proj_point (s2 - m) (p - m)`);
\r
2238 (REWRITE_TAC[GSYM (ASSUME `N = r % M:real^3`)]);
\r
2239 (EXPAND_TAC "N" THEN REWRITE_TAC[proj_point]);
\r
2240 (VECTOR_ARITH_TAC);
\r
2241 (REWRITE_TAC[PRO_EXP]);
\r
2243 (REPEAT STRIP_TAC);
\r
2244 (MATCH_MP_TAC TRANSLATE_AFFINE_KY_LEMMA1 );
\r
2245 (REWRITE_TAC[MESON[] `A /\ B /\ A <=> A /\ B`]);
\r
2246 (REPEAT STRIP_TAC);
\r
2248 (NEW_GOAL `convex hull {u0,u1,u2} SUBSET affine hull {u0,u1,u2:real^3}`);
\r
2249 (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
\r
2250 (UP_ASM_TAC THEN UNDISCH_TAC `m1:real^3 IN convex hull {u0,u1,u2}` THEN
\r
2252 (ASM_REWRITE_TAC[]);
\r
2253 (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
\r
2254 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
2255 (MATCH_MP_TAC Rogers.BARV_CIRCUMCENTER_EXISTS);
\r
2256 (EXISTS_TAC `V:real^3->bool`);
\r
2258 (ASM_REWRITE_TAC[]);
\r
2259 (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
\r
2260 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
2261 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
2262 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
2263 (MATCH_MP_TAC TRANSLATE_AFFINE_KY_LEMMA1);
\r
2265 (REWRITE_TAC[MESON[] `A/\B/\A <=> A/\B`]);
\r
2268 (MATCH_MP_TAC IN_AFFINE_HULL_3_KY_LEMMA2);
\r
2269 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `s1:real^3`);
\r
2270 (REPEAT STRIP_TAC);
\r
2271 (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
\r
2274 (MATCH_MP_TAC (SET_RULE`(?s. s SUBSET b /\ a IN s) ==> a IN b`));
\r
2275 (EXISTS_TAC `convex hull {u0, u1,u2:real^3}`);
\r
2276 (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);
\r
2277 (MATCH_MP_TAC (SET_RULE`(?s. s SUBSET b /\ a IN s) ==> a IN b`));
\r
2278 (EXISTS_TAC `convex hull {u0, u1:real^3}`);
\r
2280 (MATCH_MP_TAC CONVEX_HULL_SUBSET);
\r
2283 (REWRITE_WITH `{u0, u1:real^3} = set_of_list [u0;u1]`);
\r
2284 (REWRITE_TAC[set_of_list]);
\r
2285 (EXPAND_TAC "s1");
\r
2286 (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 =
\r
2287 omega_list V [u0;u1:real^3]`);
\r
2288 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]);
\r
2289 (MATCH_MP_TAC XNHPWAB2);
\r
2291 (REPEAT STRIP_TAC);
\r
2292 (ASM_REWRITE_TAC[]);
\r
2294 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`);
\r
2295 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
2296 (REWRITE_TAC[IN]);
\r
2297 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
2298 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
\r
2300 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
\r
2301 (EXPAND_TAC "vl");
\r
2302 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
2303 (MATCH_MP_TAC (REAL_ARITH `(?s. s < b /\ a <= s) ==> a < b`));
\r
2304 (EXISTS_TAC `hl (vl:(real^3)list)`);
\r
2306 (REWRITE_WITH `vl = truncate_simplex 2 (ul:(real^3)list)`);
\r
2307 (ASM_REWRITE_TAC[]);
\r
2308 (EXPAND_TAC "vl");
\r
2309 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
2310 (ASM_REWRITE_TAC[]);
\r
2311 (MATCH_MP_TAC Rogers.HL_DECREASE);
\r
2312 (EXISTS_TAC `V:real^3->bool`);
\r
2314 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`;IN]);
\r
2315 (REWRITE_WITH `vl = truncate_simplex 2 (ul:(real^3)list)`);
\r
2316 (ASM_REWRITE_TAC[]);
\r
2317 (EXPAND_TAC "vl");
\r
2318 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
2319 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
2320 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
2322 (ASM_REWRITE_TAC[]);
\r
2324 (ASM_REWRITE_TAC[]);
\r
2325 (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
\r
2326 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
2327 (MATCH_MP_TAC Rogers.BARV_CIRCUMCENTER_EXISTS);
\r
2328 (EXISTS_TAC `V:real^3->bool`);
\r
2330 (ASM_REWRITE_TAC[]);
\r
2331 (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);
\r
2332 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
2333 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
2334 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
2335 (ASM_MESON_TAC[]);
\r
2336 (NEW_GOAL `~(p:real^3 IN B6)`);
\r
2337 (ASM_SET_TAC[IN_DIFF]);
\r
2338 (UP_ASM_TAC THEN EXPAND_TAC "B6");
\r
2339 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;HD;TL]);
\r
2342 (ASM_MESON_TAC[]);
\r
2343 (ASM_MESON_TAC[]);
\r
2344 (REWRITE_TAC[ASSUME `N = r % M:real^3`; ASSUME `r = &1`]);
\r
2345 (VECTOR_ARITH_TAC);
\r
2349 (NEW_GOAL `norm (M:real^3) <= norm (s2 - s:real^3)`);
\r
2350 (REWRITE_WITH `norm (s2 - s:real^3) = norm (projection (s2 - m1) (s - m1))`);
\r
2351 (REWRITE_WITH `norm (s2 - s:real^3) = norm (s - s2)`);
\r
2354 (ASM_MESON_TAC[]);
\r
2355 (REWRITE_TAC[ASSUME
\r
2356 `h <= &1 /\ &0 <= h /\ M = h % projection (s2 - m1) (s - m1:real^3)`]);
\r
2357 (REWRITE_TAC[NORM_MUL;REAL_ARITH `a * b <= b <=> &0 <= b * (&1 - a)`]);
\r
2358 (MATCH_MP_TAC REAL_LE_MUL);
\r
2359 (REWRITE_TAC[NORM_POS_LE; REAL_ARITH `&0 <= a - b <=> b <= a`]);
\r
2360 (REWRITE_WITH `abs h = h`);
\r
2361 (REWRITE_TAC[REAL_ABS_REFL]);
\r
2362 (ASM_REWRITE_TAC[]);
\r
2363 (ASM_REWRITE_TAC[]);
\r
2364 (NEW_GOAL `norm (s2 - s:real^3) < norm (N:real^3) `);
\r
2365 (REWRITE_WITH `norm (s2 - s:real^3) < norm (N:real^3) <=>
\r
2366 norm (s2 - s) pow 2 < norm (N:real^3) pow 2`);
\r
2367 (MATCH_MP_TAC Pack1.bp_bdt);
\r
2368 (REWRITE_TAC[NORM_POS_LE]);
\r
2369 (REWRITE_WITH `norm (N:real^3) = norm ((p' + m) - p:real^3)`);
\r
2371 (REWRITE_TAC[GSYM (ASSUME `projection (s2 - m) (p - m) = N:real^3`)]);
\r
2372 (REWRITE_TAC[projection_proj_point]);
\r
2373 (REWRITE_TAC[ASSUME `proj_point (s2 - m) (p - m) = p':real^3`]);
\r
2375 (ASM_REWRITE_TAC[]);
\r
2376 (NEW_GOAL `norm (s2 - s:real^3) < norm (M:real^3)`);
\r
2377 (ASM_MESON_TAC[]);
\r
2378 (ASM_REAL_ARITH_TAC);
\r
2381 (* ======================================================================= *)
\r
2382 (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 0`);
\r
2383 (REPEAT STRIP_TAC);
\r
2384 (NEW_GOAL `~(y = 4 \/ y = 1 \/ y = 2 \/ y = 3)`);
\r
2387 (NEW_GOAL `i = 0`);
\r
2388 (FIRST_ASSUM MATCH_MP_TAC);
\r
2390 (REWRITE_TAC[ASSUME `i = 0`]);
\r
2391 (ASM_REWRITE_TAC[]);
\r
2393 (* ====================================================================== *)
\r
2395 (NEW_GOAL `dist (u0, p:real^3) < sqrt (&2)`);
\r
2396 (UP_ASM_TAC THEN REAL_ARITH_TAC);
\r
2397 (ASM_CASES_TAC `~(p IN rcone_gt (HD (ul:(real^3)list)) (HD (TL ul))
\r
2398 (hl (truncate_simplex 1 ul) / sqrt (&2))) `);
\r
2399 (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==>
\r
2400 ~ (y = 4 \/ y = 0 \/ y = 2 \/ y = 3)`);
\r
2401 (REPEAT STRIP_TAC);
\r
2402 (NEW_GOAL `mcell 4 V ul = {}`);
\r
2403 (SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);
\r
2406 (ASM_MESON_TAC[]);
\r
2407 (ASM_MESON_TAC[]);
\r
2409 (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 4`]);
\r
2410 (REWRITE_TAC[ASSUME `mcell 4 V ul = {}`]);
\r
2412 (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 0`;
\r
2413 MCELL_EXPLICIT;mcell0]);
\r
2415 (NEW_GOAL `~(p:real^3 IN ball (HD ul,sqrt (&2)))`);
\r
2416 (ASM_SET_TAC[IN_DIFF]);
\r
2417 (UP_ASM_TAC THEN ASM_REWRITE_TAC[HD;IN;ball;IN_ELIM_THM]);
\r
2419 (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 2`;
\r
2420 MCELL_EXPLICIT;mcell2]);
\r
2423 (REWRITE_TAC[IN_INTER]);
\r
2424 (REPEAT STRIP_TAC);
\r
2425 (NEW_GOAL `p:real^3 IN rcone_gt (HD ul) (HD (TL ul)) a`);
\r
2426 (REWRITE_TAC[RCONE_GT_GE;IN_DIFF]);
\r
2427 (ASM_REWRITE_TAC[]);
\r
2428 (REWRITE_TAC[HD;TL;IN;IN_ELIM_THM]);
\r
2430 (NEW_GOAL `~(p:real^3 IN B3)`);
\r
2431 (ASM_SET_TAC[IN_DIFF]);
\r
2432 (UP_ASM_TAC THEN EXPAND_TAC "B3" THEN REWRITE_TAC[rcone_eq;rconesgn]);
\r
2433 (ASM_REWRITE_TAC[HD;TL;IN;IN_ELIM_THM;dist]);
\r
2434 (ASM_MESON_TAC[]);
\r
2437 (* ======================================================================= *)
\r
2439 (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 3`;
\r
2440 MCELL_EXPLICIT;mcell3]);
\r
2443 (NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
\r
2444 dist (u0,s) = sqrt (&2) /\
\r
2445 mxi V ul = s:real^3)`);
\r
2446 (MATCH_MP_TAC MXI_EXPLICIT_OLD);
\r
2447 (ASM_REWRITE_TAC[]);
\r
2448 (FIRST_X_ASSUM CHOOSE_TAC);
\r
2450 (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC);
\r
2451 (UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);
\r
2452 (REWRITE_TAC[SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);
\r
2455 (SUBGOAL_THEN `p:real^3 IN rogers V ul` MP_TAC);
\r
2456 (ASM_SET_TAC[IN_DIFF]);
\r
2457 (ASM_SIMP_TAC[ROGERS_EXPLICIT; HD]);
\r
2458 (ABBREV_TAC `s1 = omega_list_n V [u0; u1; u2; u3:real^3] 1`);
\r
2459 (ABBREV_TAC `s2 = omega_list_n V [u0; u1; u2; u3:real^3] 2`);
\r
2460 (ABBREV_TAC `s3 = omega_list_n V [u0; u1; u2; u3:real^3] 3`);
\r
2463 (ABBREV_TAC `vl = [u0;u1;u2:real^3]`);
\r
2464 (NEW_GOAL `vl = truncate_simplex 2 ul:(real^3)list`);
\r
2465 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2] THEN EXPAND_TAC "vl");
\r
2466 (NEW_GOAL `barV V 2 vl`);
\r
2467 (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
2468 (EXISTS_TAC `3` THEN ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
\r
2469 (NEW_GOAL `LENGTH (vl:(real^3)list) = 3 /\ CARD {u0,u1,u2:real^3} = 3`);
\r
2470 (REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list vl`);
\r
2471 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
2472 (REWRITE_TAC[ARITH_RULE `3 = 2 + 1`]);
\r
2473 (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
\r
2474 (EXISTS_TAC `V:real^3->bool`);
\r
2475 (ASM_REWRITE_TAC[]);
\r
2477 (NEW_GOAL `s2:real^3 = omega_list V vl`);
\r
2478 (EXPAND_TAC "s2" THEN EXPAND_TAC "vl" THEN
\r
2479 REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
2480 (MESON_TAC[OMEGA_LIST_TRUNCATE_2]);
\r
2482 (NEW_GOAL `s2 = circumcenter {u0,u1,u2:real^3}`);
\r
2483 (REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list vl`);
\r
2484 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
2485 (REWRITE_TAC[ASSUME `s2 = omega_list V vl`]);
\r
2486 (MATCH_MP_TAC Rogers.XNHPWAB1);
\r
2487 (EXISTS_TAC `2` THEN REWRITE_TAC[IN]);
\r
2488 (ASM_REWRITE_TAC[]);
\r
2489 (ASM_MESON_TAC[]);
\r
2491 (NEW_GOAL `dist (s2,u0:real^3) = hl (truncate_simplex 2 (ul:(real^3)list))`);
\r
2492 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
2493 (REWRITE_TAC[GSYM (ASSUME `vl:(real^3)list = truncate_simplex 2 ul`)]);
\r
2494 (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);
\r
2495 (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
\r
2496 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
2497 (REWRITE_WITH `u0:real^3 = HD vl`);
\r
2498 (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);
\r
2499 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
\r
2500 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
\r
2501 (ASM_REWRITE_TAC[]);
\r
2503 (NEW_GOAL `~(s = s2:real^3)`);
\r
2505 (NEW_GOAL `dist (u0,s:real^3) < sqrt (&2)`);
\r
2506 (ONCE_REWRITE_TAC[DIST_SYM]);
\r
2507 (REWRITE_TAC[ASSUME `s = s2:real^3`]);
\r
2508 (ASM_MESON_TAC[]);
\r
2509 (ASM_REAL_ARITH_TAC);
\r
2511 (NEW_GOAL `(s2:real^3) IN voronoi_list V vl`);
\r
2512 (SIMP_TAC[ASSUME `s2 = omega_list V vl`]);
\r
2513 (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
\r
2515 (ASM_REWRITE_TAC[]);
\r
2517 (NEW_GOAL `(s3:real^3) IN voronoi_list V ul`);
\r
2518 (REWRITE_WITH `s3 = omega_list V ul`);
\r
2519 (EXPAND_TAC "s3" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; OMEGA_LIST]);
\r
2520 (REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) - 1 = 3`]);
\r
2521 (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
\r
2523 (ASM_REWRITE_TAC[]);
\r
2525 (NEW_GOAL `(s3:real^3) IN voronoi_list V vl`);
\r
2526 (MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET A) ==> a IN A`));
\r
2527 (EXISTS_TAC `voronoi_list V ul`);
\r
2529 (ASM_REWRITE_TAC[]);
\r
2530 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
2531 (REWRITE_TAC[VORONOI_LIST;VORONOI_SET;voronoi_closed;set_of_list;
\r
2532 SUBSET; IN_INTERS]);
\r
2533 (ONCE_REWRITE_TAC[IN]);
\r
2534 (REWRITE_TAC[IN_ELIM_THM]);
\r
2535 (REPEAT STRIP_TAC);
\r
2536 (FIRST_ASSUM MATCH_MP_TAC);
\r
2537 (EXISTS_TAC `v:real^3`);
\r
2538 (ASM_REWRITE_TAC[]);
\r
2539 (UNDISCH_TAC `v IN {u0, u1, u2:real^3}`);
\r
2542 (NEW_GOAL `s IN voronoi_list V vl`);
\r
2543 (NEW_GOAL `convex (voronoi_list V vl)`);
\r
2544 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
\r
2545 (UP_ASM_TAC THEN REWRITE_TAC[convex] THEN STRIP_TAC);
\r
2546 (UNDISCH_TAC `between s (s2,s3:real^3)`);
\r
2547 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
2548 (REPEAT STRIP_TAC);
\r
2549 (ONCE_REWRITE_TAC[GSYM IN]);
\r
2550 (REWRITE_TAC[ASSUME `s = u % s2 + v % s3:real^3`]);
\r
2551 (FIRST_ASSUM MATCH_MP_TAC);
\r
2552 (ASM_REWRITE_TAC[]);
\r
2554 (NEW_GOAL `~ (s IN affine hull {u0,u1,u2:real^3})`);
\r
2557 (NEW_GOAL `(s:real^3 - s2) dot (s - s2) = &0`);
\r
2558 (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);
\r
2559 (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
\r
2560 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
2561 (MATCH_MP_TAC MHFTTZN4);
\r
2562 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
\r
2563 (REPEAT STRIP_TAC);
\r
2564 (ASM_REWRITE_TAC[]);
\r
2565 (ASM_REWRITE_TAC[]);
\r
2566 (ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]);
\r
2567 (EXPAND_TAC "vl" THEN ASM_MESON_TAC[set_of_list]);
\r
2568 (UP_ASM_TAC THEN REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0;
\r
2569 NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
\r
2570 (ASM_REWRITE_TAC[]);
\r
2572 (NEW_GOAL `CARD {u0, u1, u2, s:real^3} = 4`);
\r
2573 (ONCE_REWRITE_TAC[SET_RULE `{u0, u1, u2, s} = {s, u0, u1, u2}`]);
\r
2574 (REWRITE_WITH `4 = SUC (CARD {u0,u1,u2:real^3})`);
\r
2575 (ASM_REWRITE_TAC[]);
\r
2577 (MATCH_MP_TAC (MESON[Geomdetail.CARD_CLAUSES_IMP]
\r
2578 `!s a. FINITE s /\ ~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s)`));
\r
2579 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
2581 (NEW_GOAL `s IN affine hull {u0, u1, u2:real^3}`);
\r
2582 (UP_ASM_TAC THEN REWRITE_TAC[IN_AFFINE_KY_LEMMA1]);
\r
2583 (ASM_MESON_TAC[]);
\r
2585 (NEW_GOAL `~affine_dependent {u0, u1, u2, s:real^3}`);
\r
2586 (ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {d,a,b,c}`]);
\r
2587 (MATCH_MP_TAC AFFINE_INDEPENDENT_INSERT);
\r
2588 (ASM_REWRITE_TAC[]);
\r
2589 (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
\r
2590 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
2591 (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);
\r
2592 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2` THEN ASM_REWRITE_TAC[]);
\r
2594 (NEW_GOAL `s2 IN convex hull {u0, u1, u2:real^3}`);
\r
2595 (REWRITE_WITH `s2 = omega_list V vl /\ {u0, u1, u2:real^3} = set_of_list vl`);
\r
2596 (EXPAND_TAC "s2" THEN EXPAND_TAC "vl");
\r
2597 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_2;set_of_list]);
\r
2598 (MATCH_MP_TAC Rogers.XNHPWAB2);
\r
2600 (ASM_REWRITE_TAC[IN]);
\r
2601 (ASM_MESON_TAC[]);
\r
2603 (NEW_GOAL `s1 = inv (&2) % (u0 + u1:real^3)`);
\r
2604 (ONCE_REWRITE_TAC[GSYM midpoint]);
\r
2605 (EXPAND_TAC "s1");
\r
2607 (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 =
\r
2608 omega_list_n V [u0; u1:real^3] 1`);
\r
2609 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2;OMEGA_LIST_TRUNCATE_1]);
\r
2610 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2]);
\r
2611 (REWRITE_WITH `omega_list V [u0; u1:real^3] =
\r
2612 circumcenter (set_of_list [u0;u1])`);
\r
2613 (MATCH_MP_TAC XNHPWAB1);
\r
2615 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
\r
2617 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
\r
2618 (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
2619 (REWRITE_TAC[IN] THEN STRIP_TAC);
\r
2620 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
2621 (EXISTS_TAC `2` THEN REWRITE_TAC[ARITH_RULE `1 <= 2`]);
\r
2622 (ASM_REWRITE_TAC[]);
\r
2624 (NEW_GOAL `!i j. i < j /\ j <= 2
\r
2625 ==> hl (truncate_simplex i (vl:(real^3)list))
\r
2626 < hl (truncate_simplex j vl)`);
\r
2628 (MATCH_MP_TAC XNHPWAB4);
\r
2629 (EXISTS_TAC `V:real^3->bool`);
\r
2630 (ASM_REWRITE_TAC[IN]);
\r
2631 (ASM_MESON_TAC[]);
\r
2633 (NEW_GOAL `hl (truncate_simplex 1 (vl:(real^3)list)) < hl (truncate_simplex 2 vl)`);
\r
2634 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
2637 (NEW_GOAL `truncate_simplex 2 vl = truncate_simplex 2 ul:(real^3)list`);
\r
2638 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
2639 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
2640 (MATCH_MP_TAC (REAL_ARITH `a < hl (truncate_simplex 2 (vl:(real^3)list)) /\
\r
2641 hl (truncate_simplex 2 vl) < b ==> a < b`));
\r
2642 (ASM_REWRITE_TAC[]);
\r
2643 (ASM_MESON_TAC[]);
\r
2644 (REWRITE_TAC[set_of_list;Rogers.CIRCUMCENTER_2]);
\r
2646 (NEW_GOAL `~(s3 IN affine hull {u0,u1,u2:real^3})`);
\r
2648 (NEW_GOAL `(s3 - s2) dot (s3 - s2:real^3) = &0`);
\r
2649 (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);
\r
2650 (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
\r
2651 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
2652 (MATCH_MP_TAC MHFTTZN4);
\r
2653 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
\r
2654 (REPEAT STRIP_TAC);
\r
2655 (ASM_REWRITE_TAC[]);
\r
2656 (ASM_REWRITE_TAC[]);
\r
2657 (ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]);
\r
2658 (EXPAND_TAC "vl" THEN ASM_MESON_TAC[set_of_list]);
\r
2659 (UP_ASM_TAC THEN REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0;
\r
2660 NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
\r
2662 (UNDISCH_TAC `between s (s2,s3:real^3)`);
\r
2663 (REWRITE_TAC[ASSUME `s3= s2:real^3`; BETWEEN_REFL_EQ]);
\r
2664 (ASM_REWRITE_TAC[]);
\r
2666 (NEW_GOAL `p IN convex hull {u0, u1, s2, s:real^3}`);
\r
2667 (MATCH_MP_TAC CONVEX_HULL_KY_LEMMA_5);
\r
2668 (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `s3:real^3`);
\r
2669 (REPEAT STRIP_TAC);
\r
2670 (ASM_MESON_TAC[]);
\r
2671 (ASM_MESON_TAC[]);
\r
2672 (ASM_MESON_TAC[]);
\r
2673 (ASM_MESON_TAC[]);
\r
2674 (ASM_MESON_TAC[]);
\r
2675 (NEW_GOAL `~(p:real^3 IN B4)`);
\r
2676 (ASM_SET_TAC[IN_DIFF]);
\r
2677 (UP_ASM_TAC THEN EXPAND_TAC "B4" THEN REWRITE_TAC[ASSUME
\r
2678 `ul = [u0;u1;u2;u3:real^3]`; HD;TL;
\r
2679 ASSUME `mxi V [u0; u1; u2; u3] = s:real^3`]);
\r
2680 (ASM_MESON_TAC[]);
\r
2681 (REWRITE_TAC[IN_INTER; ASSUME `p IN convex hull {u0, u1, u2, s:real^3}`]);
\r
2682 (UNDISCH_TAC `p IN convex hull {u0, s1, s2, s3:real^3}`);
\r
2683 (REWRITE_TAC[ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`;
\r
2684 CONVEX_HULL_4;IN;IN_ELIM_THM]);
\r
2685 (REPEAT STRIP_TAC);
\r
2686 (EXISTS_TAC `u + v * inv (&2)`);
\r
2687 (EXISTS_TAC `v * inv (&2)`);
\r
2688 (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`);
\r
2689 (REPEAT STRIP_TAC);
\r
2690 (MATCH_MP_TAC REAL_LE_ADD);
\r
2691 (ASM_REWRITE_TAC[]);
\r
2692 (MATCH_MP_TAC REAL_LE_MUL);
\r
2693 (ASM_REWRITE_TAC[]);
\r
2695 (MATCH_MP_TAC REAL_LE_MUL);
\r
2696 (ASM_REWRITE_TAC[]);
\r
2698 (ASM_REWRITE_TAC[]);
\r
2699 (ASM_REWRITE_TAC[]);
\r
2700 (REWRITE_TAC[REAL_ARITH
\r
2701 `(u + v * inv (&2)) + v * inv (&2) + w + z = u + v + w + z`]);
\r
2702 (ASM_REWRITE_TAC[]);
\r
2703 (REWRITE_TAC[ASSUME
\r
2704 `p = u % u0 + v % inv (&2) % (u0 + u1) + w % s2 + z % s3:real^3`]);
\r
2705 (VECTOR_ARITH_TAC);
\r
2707 (* ========================================================================== *)
\r
2709 (NEW_GOAL `?m n. between p (m,n) /\ between m (u0,u1) /\ between n (s2,s:real^3)`);
\r
2710 (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_4_IMP_2_2]);
\r
2711 (UP_ASM_TAC THEN REPEAT STRIP_TAC);
\r
2713 (NEW_GOAL `between m (u0, s1:real^3)`);
\r
2714 (ASM_CASES_TAC `between m (u0, s1:real^3)`);
\r
2715 (UP_ASM_TAC THEN MESON_TAC[]);
\r
2716 (NEW_GOAL `between m (s1, u1:real^3)`);
\r
2717 (NEW_GOAL `between m (u0, s1) \/ between m (s1, u1:real^3)`);
\r
2718 (MATCH_MP_TAC BETWEEN_TRANS_3_CASES);
\r
2719 (ASM_REWRITE_TAC[]);
\r
2720 (REWRITE_TAC[GSYM midpoint;BETWEEN_MIDPOINT]);
\r
2721 (ASM_MESON_TAC[]);
\r
2723 (NEW_GOAL `between n (s2,s3:real^3)`);
\r
2724 (ONCE_REWRITE_TAC[BETWEEN_SYM]);
\r
2725 (MATCH_MP_TAC BETWEEN_TRANS);
\r
2726 (EXISTS_TAC `s:real^3`);
\r
2727 (ONCE_REWRITE_TAC[BETWEEN_SYM]);
\r
2728 (ASM_MESON_TAC[]);
\r
2730 (UP_ASM_TAC THEN UP_ASM_TAC THEN UNDISCH_TAC `between p (m,n:real^3)`);
\r
2731 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
2732 (REPEAT STRIP_TAC);
\r
2733 (UNDISCH_TAC `p = u % m + v % n:real^3`);
\r
2734 (REWRITE_TAC[ASSUME `m = u' % s1 + v' % u1:real^3`;
\r
2735 ASSUME `n = u'' % s2 + v'' % s3:real^3`]);
\r
2736 (REWRITE_WITH `u1 = &2 % s1 - u0:real^3`);
\r
2737 (REWRITE_TAC[ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`]);
\r
2738 (VECTOR_ARITH_TAC);
\r
2739 (REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);
\r
2740 (REWRITE_TAC [VECTOR_ARITH
\r
2741 `((u * u') % s1 + (u * v') % (&2 % s1 - u0)) +
\r
2744 (u * (-- v')) % u0 + (u * u' + v' * &2 * u) % s1 + (v * u'') % s2 + (v * v'') % s3`]);
\r
2746 (NEW_GOAL `u * --v' = &0`);
\r
2747 (MATCH_MP_TAC AFFINE_DEPENDENT_KY_LEMMA1);
\r
2748 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `s1:real^3`);
\r
2749 (EXISTS_TAC `s2:real^3` THEN EXISTS_TAC `s3:real^3`);
\r
2750 (EXISTS_TAC `p:real^3`);
\r
2751 (EXISTS_TAC `u * u' + v' * &2 * u`);
\r
2752 (EXISTS_TAC `v * u''`);
\r
2753 (EXISTS_TAC `v * v''`);
\r
2755 (NEW_GOAL `~(affine_dependent {u0,s1,s2:real^3})`);
\r
2756 (REWRITE_WITH `{u0,s1,s2:real^3} = {omega_list_n V vl i | i <= 2}`);
\r
2757 (EXPAND_TAC "s1" THEN EXPAND_TAC "s2");
\r
2758 (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 = omega_list_n V vl 1`);
\r
2759 (EXPAND_TAC "vl" THEN REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW1; OMEGA_LIST_TRUNCATE_1]);
\r
2760 (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 2 = omega_list_n V vl 2`);
\r
2761 (EXPAND_TAC "vl" THEN REWRITE_TAC[OMEGA_LIST_TRUNCATE_2_NEW1; OMEGA_LIST_TRUNCATE_2]);
\r
2762 (REWRITE_WITH `u0 = omega_list_n V vl 0`);
\r
2763 (REWRITE_TAC[OMEGA_LIST_N]);
\r
2764 (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);
\r
2765 (REWRITE_TAC[OMEGA_LIST_UP_TO_2]);
\r
2766 (MATCH_MP_TAC Rogers.AFFINE_INDEPENDENT_OMEGA_LIST_N);
\r
2767 (ASM_MESON_TAC[]);
\r
2769 (* ======================================================================== *)
\r
2771 (NEW_GOAL `~affine_dependent {u0, s1, s2, s3:real^3}`);
\r
2772 (ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {d,a,b,c}`]);
\r
2773 (MATCH_MP_TAC AFFINE_INDEPENDENT_INSERT);
\r
2775 (ASM_REWRITE_TAC[]);
\r
2777 (NEW_GOAL `~(s3 = s2:real^3)`);
\r
2779 (UNDISCH_TAC `between s (s2,s3:real^3)`);
\r
2780 (REWRITE_TAC[ASSUME `s3= s2:real^3`; BETWEEN_REFL_EQ]);
\r
2781 (ASM_REWRITE_TAC[]);
\r
2784 (NEW_GOAL `(s3 IN affine hull {u0,u1,u2:real^3})`);
\r
2785 (UNDISCH_TAC `s2 IN convex hull {u0,u1,u2:real^3}` THEN UP_ASM_TAC THEN
\r
2786 REWRITE_TAC[AFFINE_HULL_3; CONVEX_HULL_3; IN;IN_ELIM_THM;
\r
2787 ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`]);
\r
2788 (REPEAT STRIP_TAC);
\r
2790 (REWRITE_TAC[ASSUME
\r
2791 `s3 = u''' % u0 + v''' % inv (&2) % (u0 + u1) + w % s2:real^3`;
\r
2792 ASSUME `s2 = u'''' % u0 + v'''' % u1 + w' % u2:real^3`]);
\r
2793 (EXISTS_TAC `u''' + v''' * inv (&2) + w * u''''`);
\r
2794 (EXISTS_TAC `v''' * inv (&2) + w * v''''`);
\r
2795 (EXISTS_TAC `w * w'`);
\r
2797 (REWRITE_TAC[REAL_ARITH
\r
2798 `(u''' + v''' * inv (&2) + w * u'''') +
\r
2799 (v''' * inv (&2) + w * v'''') + w * w' =
\r
2800 (u''' + v''') + w * (u'''' + v'''' + w')`]);
\r
2801 (ASM_REWRITE_TAC[REAL_ARITH `(a + b) + c * &1 = a + b + c`]);
\r
2802 (VECTOR_ARITH_TAC);
\r
2803 (ASM_MESON_TAC[]);
\r
2805 (REPEAT STRIP_TAC);
\r
2806 (ASM_MESON_TAC[]);
\r
2808 (ONCE_REWRITE_TAC [SET_RULE `{u0, s1, s2, s3} = {s3,u0, s1, s2}`]);
\r
2809 (NEW_GOAL `CARD {u0,s1,s2:real^3} = 3`);
\r
2810 (REWRITE_WITH `{u0,s1,s2:real^3} = {omega_list_n V vl i | i <= 2}`);
\r
2811 (EXPAND_TAC "s1" THEN EXPAND_TAC "s2");
\r
2812 (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 = omega_list_n V vl 1`);
\r
2813 (EXPAND_TAC "vl" THEN REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW1; OMEGA_LIST_TRUNCATE_1]);
\r
2814 (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 2 = omega_list_n V vl 2`);
\r
2815 (EXPAND_TAC "vl" THEN REWRITE_TAC[OMEGA_LIST_TRUNCATE_2_NEW1; OMEGA_LIST_TRUNCATE_2]);
\r
2816 (REWRITE_WITH `u0 = omega_list_n V vl 0`);
\r
2817 (REWRITE_TAC[OMEGA_LIST_N]);
\r
2818 (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);
\r
2819 (REWRITE_TAC[OMEGA_LIST_UP_TO_2]);
\r
2820 (REWRITE_WITH `{omega_list_n V vl i | i <= 2} = IMAGE (omega_list_n V vl) {i | i <= 2}`);
\r
2821 (REWRITE_TAC[IMAGE]);
\r
2823 (REWRITE_TAC[NUMSEG_LE]);
\r
2824 (REWRITE_WITH `IMAGE (omega_list_n V vl) (0..2) = {omega_list_n V vl i | i IN (0..2)}`);
\r
2825 (REWRITE_TAC[IMAGE]);
\r
2827 (NEW_GOAL `aff_dim {omega_list_n V vl j | j IN 0..2} = &2`);
\r
2828 (MATCH_MP_TAC XNHPWAB3);
\r
2829 (ASM_MESON_TAC[IN]);
\r
2830 (NEW_GOAL `aff_dim {omega_list_n V vl i | i IN 0..2} <=
\r
2831 &(CARD {omega_list_n V vl i | i IN 0..2}) - &1`);
\r
2832 (MATCH_MP_TAC AFF_DIM_LE_CARD);
\r
2833 (REWRITE_WITH `{omega_list_n V vl i | i IN (0..2)} = IMAGE (omega_list_n V vl) (0..2)`);
\r
2834 (REWRITE_TAC[IMAGE]);
\r
2836 (REWRITE_TAC[GSYM NUMSEG_LE]);
\r
2837 (REWRITE_WITH `IMAGE (omega_list_n V vl) {i | i <= 2} = {omega_list_n V vl i | i <= 2}`);
\r
2838 (REWRITE_TAC[IMAGE]);
\r
2840 (REWRITE_TAC[OMEGA_LIST_UP_TO_2;Geomdetail.FINITE6]);
\r
2841 (UP_ASM_TAC THEN REWRITE_TAC[ARITH_RULE `a:int <= b - &1 <=> a + &1 <= b`]);
\r
2842 (REWRITE_TAC[ASSUME `aff_dim {omega_list_n V vl j | j IN 0..2} = &2`;
\r
2843 ARITH_RULE `&2 + &1 = &3:int`; INT_OF_NUM_LE]);
\r
2845 (NEW_GOAL `CARD {omega_list_n V vl i | i IN 0..2} <= 3`);
\r
2846 (REWRITE_WITH `{omega_list_n V vl i | i IN (0..2)} = IMAGE (omega_list_n V vl) (0..2)`);
\r
2847 (REWRITE_TAC[IMAGE]);
\r
2849 (REWRITE_TAC[GSYM NUMSEG_LE]);
\r
2850 (REWRITE_WITH `IMAGE (omega_list_n V vl) {i | i <= 2} = {omega_list_n V vl i | i <= 2}`);
\r
2851 (REWRITE_TAC[IMAGE]);
\r
2853 (REWRITE_TAC[OMEGA_LIST_UP_TO_2; Geomdetail.CARD3]);
\r
2855 (REWRITE_WITH `4 = SUC (CARD {u0, s1, s2:real^3})`);
\r
2856 (ASM_REWRITE_TAC[]);
\r
2858 (MATCH_MP_TAC (MESON[Geomdetail.CARD_CLAUSES_IMP]
\r
2859 `!a s. FINITE s /\ ~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s)`));
\r
2860 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
2863 (NEW_GOAL `~(s3 IN affine hull {u0,s1,s2:real^3})`);
\r
2865 (NEW_GOAL `(s3 IN affine hull {u0,u1,u2:real^3})`);
\r
2866 (UNDISCH_TAC `s2 IN convex hull {u0,u1,u2:real^3}` THEN UP_ASM_TAC THEN
\r
2867 REWRITE_TAC[AFFINE_HULL_3; CONVEX_HULL_3; IN;IN_ELIM_THM;
\r
2868 ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`]);
\r
2869 (REPEAT STRIP_TAC);
\r
2871 (REWRITE_TAC[ASSUME
\r
2872 `s3 = u''' % u0 + v''' % inv (&2) % (u0 + u1) + w % s2:real^3`;
\r
2873 ASSUME `s2 = u'''' % u0 + v'''' % u1 + w' % u2:real^3`]);
\r
2874 (EXISTS_TAC `u''' + v''' * inv (&2) + w * u''''`);
\r
2875 (EXISTS_TAC `v''' * inv (&2) + w * v''''`);
\r
2876 (EXISTS_TAC `w * w'`);
\r
2878 (REWRITE_TAC[REAL_ARITH
\r
2879 `(u''' + v''' * inv (&2) + w * u'''') +
\r
2880 (v''' * inv (&2) + w * v'''') + w * w' =
\r
2881 (u''' + v''') + w * (u'''' + v'''' + w')`]);
\r
2882 (ASM_REWRITE_TAC[REAL_ARITH `(a + b) + c * &1 = a + b + c`]);
\r
2883 (VECTOR_ARITH_TAC);
\r
2884 (ASM_MESON_TAC[]);
\r
2885 (NEW_GOAL `s3 IN affine hull {u0, s1, s2:real^3}`);
\r
2886 (UNDISCH_TAC `s3 IN {u0, s1, s2:real^3}` THEN
\r
2887 REWRITE_TAC [IN_AFFINE_KY_LEMMA1]);
\r
2888 (ASM_MESON_TAC[]);
\r
2889 (ASM_MESON_TAC[]);
\r
2890 (REWRITE_TAC[REAL_ARITH
\r
2891 `u * --v' + (u * u' + v' * &2 * u) + v * u'' + v * v''
\r
2892 = u * (u' + v') + v * (u'' + v'')`]);
\r
2893 (ASM_REWRITE_TAC[REAL_MUL_RID]);
\r
2894 (ASM_REWRITE_TAC[]);
\r
2895 (REWRITE_TAC[REAL_ARITH `a * (-- b) <= &0 <=> &0 <= a * b`]);
\r
2896 (ASM_SIMP_TAC[REAL_LE_MUL]);
\r
2897 (NEW_GOAL `p IN affine hull {s1, s2, s3:real^3}`);
\r
2898 (REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);
\r
2899 (EXISTS_TAC `u * u' + v' * &2 * u`);
\r
2900 (EXISTS_TAC `v * u''`);
\r
2901 (EXISTS_TAC `v * v''`);
\r
2903 (REWRITE_TAC[REAL_ARITH `(u * u' + v' * &2 * u) + v * u'' + v * v'' =
\r
2904 (u * (u' + v') + v * (u'' + v'')) - (u * -- v')`]);
\r
2905 (ASM_REWRITE_TAC[REAL_MUL_RID]);
\r
2907 (ASM_REWRITE_TAC[]);
\r
2908 (VECTOR_ARITH_TAC);
\r
2909 (NEW_GOAL `~(p:real^3 IN B7)`);
\r
2910 (ASM_SET_TAC[IN_DIFF]);
\r
2911 (UP_ASM_TAC THEN EXPAND_TAC "B7");
\r
2912 (UP_ASM_TAC THEN EXPAND_TAC "s1" THEN EXPAND_TAC "s2" THEN EXPAND_TAC "s3");
\r
2913 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
2914 (UP_ASM_TAC THEN MESON_TAC[]);
\r
2916 (* ========================================================================= *)
\r
2918 (NEW_GOAL `?q. between p (u0,q) /\ between q (n,s1:real^3)`);
\r
2919 (UNDISCH_TAC `between p (m,n:real^3)` THEN UP_ASM_TAC);
\r
2920 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;IN;IN_ELIM_THM; CONVEX_HULL_2]);
\r
2921 (REPEAT STRIP_TAC);
\r
2922 (EXISTS_TAC `((u' * v) / (u' * v + v')) % s1 +
\r
2923 (v' / (u' * v + v')) % n:real^3`);
\r
2924 (NEW_GOAL `~((u' * v + v') = &0)`);
\r
2926 (NEW_GOAL `p = u0:real^3`);
\r
2927 (ASM_REWRITE_TAC[]);
\r
2928 (NEW_GOAL `u' * v = &0 /\ v' = &0`);
\r
2929 (NEW_GOAL `&0 <= u' * v /\ &0 <= v'`);
\r
2930 (ASM_SIMP_TAC [REAL_LE_MUL]);
\r
2931 (ASM_REAL_ARITH_TAC);
\r
2932 (NEW_GOAL `u' * u = &1`);
\r
2933 (NEW_GOAL `u' * u + (u' * v + v') = &1`);
\r
2934 (REWRITE_TAC[REAL_ARITH `u' * u + (u' * v + v') = u' * (u + v) + v'`]);
\r
2935 (ASM_MESON_TAC[REAL_MUL_RID]);
\r
2936 (ASM_REAL_ARITH_TAC);
\r
2937 (REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);
\r
2938 (ONCE_REWRITE_TAC[REAL_ARITH `a * b * c = (a * b) * c`]);
\r
2939 (ASM_REWRITE_TAC[]);
\r
2940 (VECTOR_ARITH_TAC);
\r
2942 (NEW_GOAL `~(p:real^3 IN B6)`);
\r
2943 (ASM_SET_TAC[IN_DIFF]);
\r
2944 (UP_ASM_TAC THEN EXPAND_TAC "B6" THEN REWRITE_TAC[
\r
2945 ASSUME `ul = [u0;u1;u2;u3:real^3]`; HD; TL]);
\r
2946 (REWRITE_TAC[ASSUME `p = u0:real^3`; AFFINE_HULL_3;IN;IN_ELIM_THM]);
\r
2947 (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);
\r
2950 (VECTOR_ARITH_TAC);
\r
2953 (EXISTS_TAC `u' * u`);
\r
2954 (EXISTS_TAC `u' * v + v'`);
\r
2955 (REPEAT STRIP_TAC);
\r
2956 (ASM_SIMP_TAC[REAL_LE_MUL]);
\r
2957 (ASM_SIMP_TAC[REAL_LE_ADD;REAL_LE_MUL]);
\r
2958 (ASM_REWRITE_TAC[REAL_ARITH `u' * u + u' * v + v' = u' * (u + v) + v'`;
\r
2960 (REWRITE_TAC[ASSUME `p = u' % m + v' % n:real^3`;
\r
2961 ASSUME `m = u % u0 + v % s1:real^3`;VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);
\r
2963 (REWRITE_TAC[VECTOR_ARITH `((u' * v + v') * (u' * v) / (u' * v + v')) % s1 =
\r
2964 ((u' * v + v') / (u' * v + v')) % ((u' * v) % s1)`]);
\r
2965 (REWRITE_TAC[VECTOR_ARITH `((u' * v + v') * v' / (u' * v + v')) % n =
\r
2966 ((u' * v + v') / (u' * v + v')) % (v' % n)`]);
\r
2967 (REWRITE_TAC[VECTOR_ARITH `(x + a % y) + b % z = x + m % a % y + m % b % z
\r
2968 <=> (m - &1) % (a % y + b % z )= vec 0`]);
\r
2970 (REWRITE_WITH `(u' * v + v') / (u' * v + v') = &1`);
\r
2971 (MATCH_MP_TAC REAL_DIV_REFL);
\r
2972 (ASM_REWRITE_TAC[]);
\r
2973 (VECTOR_ARITH_TAC);
\r
2975 (EXISTS_TAC `v' / (u' * v + v')`);
\r
2976 (EXISTS_TAC `(u' * v) / (u' * v + v')`);
\r
2977 (REPEAT STRIP_TAC);
\r
2978 (ASM_SIMP_TAC[REAL_LE_DIV;REAL_LE_ADD;REAL_LE_MUL]);
\r
2979 (ASM_SIMP_TAC[REAL_LE_DIV;REAL_LE_ADD;REAL_LE_MUL]);
\r
2980 (REWRITE_TAC[REAL_ARITH `a / x + b / x = (b + a) / x`]);
\r
2981 (MATCH_MP_TAC REAL_DIV_REFL);
\r
2982 (ASM_REWRITE_TAC[]);
\r
2983 (VECTOR_ARITH_TAC);
\r
2985 (UP_ASM_TAC THEN REPEAT STRIP_TAC);
\r
2988 (* ========================================================================= *)
\r
2990 (UNDISCH_TAC `~(p:real^3 IN
\r
2991 rcone_gt (HD ul) (HD (TL ul))
\r
2992 (hl (truncate_simplex 1 ul) / sqrt (&2)))`);
\r
2993 (ASM_REWRITE_TAC[HD;TL]);
\r
2994 (REWRITE_WITH `hl (truncate_simplex 1 [u0; u1; u2; u3:real^3]) = dist (s1, u0)`);
\r
2995 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
2996 (REWRITE_WITH `dist (s1,u0) = dist (circumcenter (set_of_list [u0;u1:real^3]), HD [u0;u1:real^3])`);
\r
2997 (REWRITE_TAC[HD; set_of_list; Rogers.CIRCUMCENTER_2]);
\r
2998 (ASM_REWRITE_TAC[midpoint]);
\r
2999 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
\r
3000 (EXISTS_TAC `V:real^3->bool`);
\r
3002 (ASM_REWRITE_TAC[]);
\r
3003 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
\r
3004 (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
3005 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
3007 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);
\r
3010 (NEW_GOAL `q:real^3 IN rcone_ge u0 u1 (dist (s1,u0) / sqrt (&2))`);
\r
3011 (REWRITE_TAC[rcone_ge; rconesgn;IN;IN_ELIM_THM]);
\r
3012 (REWRITE_WITH `(q - u0) dot (u1 - u0) =
\r
3013 (q - s1) dot (u1 - u0) + (s1 - u0) dot (u1 - u0:real^3)`);
\r
3014 (VECTOR_ARITH_TAC);
\r
3015 (REWRITE_WITH `(q - s1) dot (u1 - u0:real^3) = &0`);
\r
3016 (REWRITE_WITH `u1 - u0 = (-- &2) % (u0:real^3 - s1)`);
\r
3017 (ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);
\r
3018 (REWRITE_TAC[DOT_RMUL]);
\r
3019 (REWRITE_WITH `(q - s1) dot (u0 - s1:real^3) = &0`);
\r
3020 (REWRITE_WITH `s1 = circumcenter (set_of_list [u0;u1:real^3])`);
\r
3021 (ASM_REWRITE_TAC[set_of_list; Rogers.CIRCUMCENTER_2; midpoint]);
\r
3022 (MATCH_MP_TAC MHFTTZN4);
\r
3023 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
\r
3024 (REPEAT STRIP_TAC);
\r
3025 (ASM_REWRITE_TAC[]);
\r
3026 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
\r
3027 (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
3028 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
3030 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);
\r
3032 (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
\r
3033 (NEW_GOAL `n IN voronoi_list V [u0; u1:real^3]`);
\r
3034 (NEW_GOAL `s2 IN voronoi_list V [u0; u1:real^3]`);
\r
3036 (NEW_GOAL `(s2:real^3) IN voronoi_list V vl`);
\r
3037 (SIMP_TAC[ASSUME `s2 = omega_list V vl`]);
\r
3038 (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
\r
3040 (ASM_REWRITE_TAC[]);
\r
3042 (MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET A) ==> a IN A`));
\r
3043 (EXISTS_TAC `voronoi_list V vl`);
\r
3045 (ASM_REWRITE_TAC[]);
\r
3046 (EXPAND_TAC "vl");
\r
3047 (REWRITE_TAC[VORONOI_LIST;VORONOI_SET;voronoi_closed;set_of_list;
\r
3048 SUBSET; IN_INTERS]);
\r
3049 (ONCE_REWRITE_TAC[IN]);
\r
3050 (REWRITE_TAC[IN_ELIM_THM]);
\r
3051 (REPEAT STRIP_TAC);
\r
3052 (FIRST_ASSUM MATCH_MP_TAC);
\r
3053 (EXISTS_TAC `v:real^3`);
\r
3054 (ASM_REWRITE_TAC[]);
\r
3055 (UNDISCH_TAC `v IN {u0, u1:real^3}`);
\r
3058 (NEW_GOAL `s3 IN voronoi_list V [u0; u1]`);
\r
3059 (MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET A) ==> a IN A`));
\r
3060 (EXISTS_TAC `voronoi_list V vl`);
\r
3062 (ASM_REWRITE_TAC[]);
\r
3063 (EXPAND_TAC "vl");
\r
3064 (REWRITE_TAC[VORONOI_LIST;VORONOI_SET;voronoi_closed;set_of_list;
\r
3065 SUBSET; IN_INTERS]);
\r
3066 (ONCE_REWRITE_TAC[IN]);
\r
3067 (REWRITE_TAC[IN_ELIM_THM]);
\r
3068 (REPEAT STRIP_TAC);
\r
3069 (FIRST_ASSUM MATCH_MP_TAC);
\r
3070 (EXISTS_TAC `v:real^3`);
\r
3071 (ASM_REWRITE_TAC[]);
\r
3072 (UNDISCH_TAC `v IN {u0, u1:real^3}`);
\r
3075 (NEW_GOAL `convex (voronoi_list V [u0;u1:real^3])`);
\r
3076 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
\r
3077 (UP_ASM_TAC THEN REWRITE_TAC[convex] THEN STRIP_TAC);
\r
3078 (SUBGOAL_THEN `between n (s2,s3:real^3)` MP_TAC);
\r
3079 (ONCE_REWRITE_TAC[BETWEEN_SYM]);
\r
3080 (MATCH_MP_TAC BETWEEN_TRANS);
\r
3081 (EXISTS_TAC `s:real^3`);
\r
3082 (ONCE_REWRITE_TAC[BETWEEN_SYM]);
\r
3083 (ASM_REWRITE_TAC[]);
\r
3084 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
3085 (REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM IN]);
\r
3086 (REWRITE_TAC[ASSUME `n = u % s2 + v % s3:real^3`]);
\r
3087 (FIRST_ASSUM MATCH_MP_TAC);
\r
3088 (ASM_REWRITE_TAC[]);
\r
3090 (UNDISCH_TAC `between q (n,s1:real^3)`);
\r
3091 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
3092 (REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM IN]);
\r
3093 (REWRITE_TAC[ASSUME `q = u % n + v % s1:real^3`]);
\r
3094 (NEW_GOAL `convex (voronoi_list V [u0;u1:real^3])`);
\r
3095 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
\r
3096 (UP_ASM_TAC THEN REWRITE_TAC[convex] THEN STRIP_TAC);
\r
3097 (FIRST_ASSUM MATCH_MP_TAC);
\r
3098 (ASM_REWRITE_TAC[]);
\r
3099 (REWRITE_TAC[GSYM (ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`)]);
\r
3100 (REWRITE_WITH `s1 = omega_list V [u0;u1:real^3]`);
\r
3101 (EXPAND_TAC "s1");
\r
3102 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]);
\r
3103 (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
\r
3105 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`);
\r
3106 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
3107 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
3109 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
\r
3110 (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
\r
3111 (REWRITE_TAC[set_of_list] THEN SET_TAC[]);
\r
3114 (REWRITE_WITH `(s1 - u0) dot (u1 - u0:real^3) = dist (s1,u0) * dist (u1,u0)`);
\r
3115 (REWRITE_TAC[dist]);
\r
3116 (REWRITE_TAC [NORM_CAUCHY_SCHWARZ_EQ]);
\r
3117 (REWRITE_TAC[ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`;
\r
3118 VECTOR_ARITH `inv (&2) % (u0 + u1) - u0 = inv (&2) % (u1 - u0)`]);
\r
3119 (REWRITE_TAC[NORM_MUL; VECTOR_MUL_ASSOC; REAL_ABS_MUL]);
\r
3120 (REWRITE_WITH `abs (inv (&2)) = inv (&2)`);
\r
3121 (REWRITE_TAC[REAL_ABS_REFL]);
\r
3123 (VECTOR_ARITH_TAC);
\r
3124 (REWRITE_TAC[REAL_ADD_LID; REAL_ARITH `a * b >= x * b * a / t <=>
\r
3125 &0 <= a * b * (&1 - x / t)`]);
\r
3126 (MATCH_MP_TAC REAL_LE_MUL);
\r
3128 (REWRITE_TAC[DIST_POS_LE]);
\r
3129 (MATCH_MP_TAC REAL_LE_MUL);
\r
3131 (REWRITE_TAC[DIST_POS_LE]);
\r
3132 (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
\r
3133 (REWRITE_WITH `dist (q,u0:real^3) / sqrt (&2) <= &1
\r
3134 <=> dist (q,u0) <= &1 * sqrt (&2) `);
\r
3135 (MATCH_MP_TAC REAL_LE_LDIV_EQ);
\r
3136 (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);
\r
3137 (ONCE_REWRITE_TAC[DIST_SYM]);
\r
3138 (ONCE_REWRITE_TAC[REAL_MUL_LID]);
\r
3140 (NEW_GOAL `dist (u0,s1:real^3) = hl (truncate_simplex 1 [u0;u1:real^3])`);
\r
3141 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
3142 (REWRITE_WITH `s1 = omega_list V [u0;u1:real^3]`);
\r
3143 (EXPAND_TAC "s1");
\r
3144 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]);
\r
3145 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
3146 (ONCE_REWRITE_TAC[DIST_SYM]);
\r
3147 (REWRITE_WITH ` dist (omega_list V [u0; u1],u0) =
\r
3148 dist (omega_list V [u0; u1],HD [u0;u1:real^3])`);
\r
3149 (REWRITE_TAC[HD]);
\r
3150 (MATCH_MP_TAC Rogers.WAUFCHE2);
\r
3152 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
\r
3153 (EXPAND_TAC "vl");
\r
3154 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
3155 (REPEAT STRIP_TAC);
\r
3156 (ASM_REWRITE_TAC[]);
\r
3157 (REWRITE_TAC[IN]);
\r
3158 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
3160 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);
\r
3162 (NEW_GOAL `hl (truncate_simplex 1 vl) <= hl (vl:(real^3)list)`);
\r
3163 (MATCH_MP_TAC Rogers.HL_DECREASE);
\r
3164 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
\r
3165 (ASM_REWRITE_TAC[IN; ARITH_RULE `1 <= 2`]);
\r
3166 (NEW_GOAL `hl (vl:(real^3)list) < sqrt (&2)`);
\r
3167 (ONCE_ASM_REWRITE_TAC[]);
\r
3168 (ASM_REAL_ARITH_TAC);
\r
3169 (ASM_REAL_ARITH_TAC);
\r
3172 (NEW_GOAL `hl (truncate_simplex 1 [u0;u1:real^3]) <= hl (vl:(real^3)list)`);
\r
3173 (REWRITE_WITH `truncate_simplex 1 [u0;u1:real^3] =
\r
3174 truncate_simplex 1 vl`);
\r
3175 (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
3176 (MATCH_MP_TAC Rogers.HL_DECREASE);
\r
3177 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
\r
3178 (ASM_REWRITE_TAC[IN; ARITH_RULE `1 <= 2`]);
\r
3179 (NEW_GOAL `hl (vl:(real^3)list) < sqrt (&2)`);
\r
3180 (ONCE_ASM_REWRITE_TAC[]);
\r
3181 (ASM_REAL_ARITH_TAC);
\r
3182 (NEW_GOAL `dist (u0,s1:real^3) < sqrt (&2)`);
\r
3183 (ONCE_ASM_REWRITE_TAC[]);
\r
3184 (ASM_REAL_ARITH_TAC);
\r
3185 (NEW_GOAL `?y. y IN {n,s1:real^3} /\
\r
3186 (!x. x IN convex hull {n,s1} ==> norm (x - u0) <= norm (y - u0))`);
\r
3187 (MATCH_MP_TAC SIMPLEX_FURTHEST_LE);
\r
3188 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
3190 (UP_ASM_TAC THEN REWRITE_TAC [SET_RULE `a IN {x,y} <=> a = x \/ a = y`]
\r
3191 THEN REPEAT STRIP_TAC);
\r
3192 (NEW_GOAL `dist (u0,q) <= dist (u0, n:real^3)`);
\r
3193 (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC
\r
3194 [dist; GSYM (ASSUME `y' = n:real^3`)]);
\r
3195 (POP_ASSUM MATCH_MP_TAC);
\r
3196 (REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
\r
3197 (ASM_REWRITE_TAC[]);
\r
3199 (NEW_GOAL `dist (u0,n:real^3) <= sqrt (&2)`);
\r
3200 (NEW_GOAL `?y. y IN {s2,s:real^3} /\
\r
3201 (!x. x IN convex hull {s2,s} ==> norm (x - u0) <= norm (y - u0))`);
\r
3202 (MATCH_MP_TAC SIMPLEX_FURTHEST_LE);
\r
3203 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
3205 (UP_ASM_TAC THEN REWRITE_TAC [SET_RULE `a IN {x,y} <=> a = x \/ a = y`]
\r
3206 THEN REPEAT STRIP_TAC);
\r
3207 (NEW_GOAL `dist (u0,n) <= dist (u0, s2:real^3)`);
\r
3208 (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC
\r
3209 [dist; GSYM (ASSUME `y'' = s2:real^3`)]);
\r
3210 (POP_ASSUM MATCH_MP_TAC);
\r
3211 (REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
\r
3212 (ASM_REWRITE_TAC[]);
\r
3213 (NEW_GOAL `dist (u0,s2:real^3) < sqrt (&2)`);
\r
3214 (ONCE_REWRITE_TAC[DIST_SYM]);
\r
3215 (ONCE_ASM_REWRITE_TAC[]);
\r
3216 (ASM_REWRITE_TAC[]);
\r
3217 (ASM_REAL_ARITH_TAC);
\r
3218 (NEW_GOAL `dist (u0,n) <= dist (u0, s:real^3)`);
\r
3219 (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC
\r
3220 [dist; GSYM (ASSUME `y'' = s:real^3`)]);
\r
3221 (POP_ASSUM MATCH_MP_TAC);
\r
3222 (REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
\r
3223 (ASM_REWRITE_TAC[]);
\r
3224 (ASM_REAL_ARITH_TAC);
\r
3225 (ASM_REAL_ARITH_TAC);
\r
3227 (NEW_GOAL `dist (u0,q) <= dist (u0, s1:real^3)`);
\r
3228 (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC
\r
3229 [dist; GSYM (ASSUME `y' = s1:real^3`)]);
\r
3230 (POP_ASSUM MATCH_MP_TAC);
\r
3231 (REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
\r
3232 (ASM_REWRITE_TAC[]);
\r
3233 (ASM_REAL_ARITH_TAC);
\r
3235 (* ========================================================================== *)
\r
3237 (NEW_GOAL `p:real^3 IN rcone_ge u0 u1 (dist (s1,u0) / sqrt (&2))`);
\r
3238 (UNDISCH_TAC `between p (u0,q:real^3)`);
\r
3239 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
3240 (REPEAT STRIP_TAC);
\r
3241 (ONCE_REWRITE_TAC[GSYM IN]);
\r
3242 (REWRITE_TAC[ASSUME `p = u % u0 + v % q:real^3`]);
\r
3243 (REWRITE_WITH `u % u0 + v % q = u0 + v % (q - u0:real^3)`);
\r
3244 (REWRITE_TAC[VECTOR_ARITH `u % u0 + v % q = u0 + v % (q - u0) <=>
\r
3245 ((u + v) - &1) % u0 = vec 0`]);
\r
3246 (ASM_REWRITE_TAC[]);
\r
3247 (VECTOR_ARITH_TAC);
\r
3248 (MATCH_MP_TAC RCONE_GE_TRANS);
\r
3249 (REWRITE_TAC[VECTOR_ARITH `u0 + q - u0:real^3 = q`]);
\r
3250 (ASM_REWRITE_TAC[]);
\r
3251 (REWRITE_TAC[RCONE_GT_GE; IN_DIFF]);
\r
3253 (ASM_REWRITE_TAC[]);
\r
3254 (REWRITE_TAC[IN;IN_ELIM_THM]);
\r
3256 (NEW_GOAL `~(p:real^3 IN B3)`);
\r
3258 (UP_ASM_TAC THEN EXPAND_TAC "B3" THEN REWRITE_TAC[ASSUME
\r
3259 `ul = [u0;u1;u2;u3:real^3]`; HD;TL]);
\r
3260 (REWRITE_WITH `hl (truncate_simplex 1 [u0; u1; u2; u3]) = dist (s1,u0:real^3)`);
\r
3261 (REWRITE_WITH `truncate_simplex 1 [u0; u1; u2; u3] =
\r
3262 truncate_simplex 1 [u0;u1:real^3]`);
\r
3263 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
3264 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
3265 (REWRITE_WITH `s1 = omega_list V [u0;u1:real^3]`);
\r
3266 (EXPAND_TAC "s1");
\r
3267 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]);
\r
3268 (REWRITE_WITH ` dist (omega_list V [u0; u1],u0) =
\r
3269 dist (omega_list V [u0; u1],HD [u0;u1:real^3])`);
\r
3270 (REWRITE_TAC[HD]);
\r
3271 (MATCH_MP_TAC Rogers.WAUFCHE2);
\r
3273 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);
\r
3274 (EXPAND_TAC "vl");
\r
3275 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
3276 (REPEAT STRIP_TAC);
\r
3277 (ASM_REWRITE_TAC[]);
\r
3278 (REWRITE_TAC[IN]);
\r
3279 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
3281 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);
\r
3283 (NEW_GOAL `hl (truncate_simplex 1 vl) <= hl (vl:(real^3)list)`);
\r
3284 (MATCH_MP_TAC Rogers.HL_DECREASE);
\r
3285 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
\r
3286 (ASM_REWRITE_TAC[IN; ARITH_RULE `1 <= 2`]);
\r
3287 (NEW_GOAL `hl (vl:(real^3)list) < sqrt (&2)`);
\r
3288 (ONCE_ASM_REWRITE_TAC[]);
\r
3289 (ASM_REAL_ARITH_TAC);
\r
3290 (ASM_REAL_ARITH_TAC);
\r
3292 (REWRITE_TAC[rcone_eq;rconesgn;IN;IN_ELIM_THM]);
\r
3293 (UP_ASM_TAC THEN REWRITE_TAC[dist] THEN MESON_TAC[]);
\r
3296 (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 1`);
\r
3297 (GEN_TAC THEN STRIP_TAC);
\r
3298 (NEW_GOAL `~(y = 4 \/ y = 0 \/ y = 2 \/ y = 3)`);
\r
3301 (NEW_GOAL `i = 1`);
\r
3302 (FIRST_ASSUM MATCH_MP_TAC);
\r
3303 (ASM_REWRITE_TAC[]);
\r
3304 (GEN_TAC THEN STRIP_TAC);
\r
3305 (ASM_REWRITE_TAC[]);
\r
3306 (FIRST_ASSUM MATCH_MP_TAC);
\r
3307 (ASM_REWRITE_TAC[]);
\r
3308 (UP_ASM_TAC THEN REWRITE_TAC[MESON[] `~ ~ A <=> A`] THEN DISCH_TAC);
\r
3310 (* ======================================================================== *)
\r
3314 `p IN aff_ge {u0:real^3, u1} {mxi V ul, omega_list_n V ul 3}`);
\r
3316 (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==>
\r
3317 ~ (y = 4 \/ y = 0 \/ y = 1 \/ y = 3)`);
\r
3318 (REPEAT STRIP_TAC);
\r
3319 (NEW_GOAL `mcell 4 V ul = {}`);
\r
3320 (SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);
\r
3323 (ASM_MESON_TAC[]);
\r
3324 (ASM_MESON_TAC[]);
\r
3326 (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 4`]);
\r
3327 (REWRITE_TAC[ASSUME `mcell 4 V ul = {}`]);
\r
3329 (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 0`;
\r
3330 MCELL_EXPLICIT;mcell0]);
\r
3332 (NEW_GOAL `~(p:real^3 IN ball (HD ul,sqrt (&2)))`);
\r
3333 (ASM_SET_TAC[IN_DIFF]);
\r
3334 (UP_ASM_TAC THEN ASM_REWRITE_TAC[HD;IN;ball;IN_ELIM_THM]);
\r
3336 (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 1`;
\r
3337 MCELL_EXPLICIT;mcell1]);
\r
3339 (REWRITE_TAC[IN_DIFF]);
\r
3341 (ASM_MESON_TAC[]);
\r
3344 (* ======================================================================= *)
\r
3346 (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 3`;
\r
3347 MCELL_EXPLICIT;mcell3]);
\r
3350 (NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
\r
3351 dist (u0,s) = sqrt (&2) /\
\r
3352 mxi V ul = s:real^3)`);
\r
3353 (MATCH_MP_TAC MXI_EXPLICIT_OLD);
\r
3354 (ASM_REWRITE_TAC[]);
\r
3355 (FIRST_X_ASSUM CHOOSE_TAC);
\r
3357 (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC);
\r
3358 (UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);
\r
3359 (REWRITE_TAC[SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);
\r
3361 (ABBREV_TAC `s2 = omega_list_n V [u0; u1; u2; u3:real^3] 2`);
\r
3362 (ABBREV_TAC `s3 = omega_list_n V [u0; u1; u2; u3:real^3] 3`);
\r
3363 (NEW_GOAL `p IN aff_ge {u0, u1} {s, s3:real^3}`);
\r
3364 (ASM_MESON_TAC[]);
\r
3365 (ABBREV_TAC `vl = [u0;u1;u2:real^3]`);
\r
3366 (NEW_GOAL `vl = truncate_simplex 2 ul:(real^3)list`);
\r
3367 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2] THEN EXPAND_TAC "vl");
\r
3368 (NEW_GOAL `barV V 2 vl`);
\r
3369 (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
3370 (EXISTS_TAC `3` THEN ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);
\r
3371 (NEW_GOAL `LENGTH (vl:(real^3)list) = 3 /\ CARD {u0,u1,u2:real^3} = 3`);
\r
3372 (REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list vl`);
\r
3373 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
3374 (REWRITE_TAC[ARITH_RULE `3 = 2 + 1`]);
\r
3375 (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
\r
3376 (EXISTS_TAC `V:real^3->bool`);
\r
3377 (ASM_REWRITE_TAC[]);
\r
3378 (NEW_GOAL `s2:real^3 = omega_list V vl`);
\r
3379 (EXPAND_TAC "s2" THEN EXPAND_TAC "vl" THEN
\r
3380 REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
3381 (MESON_TAC[OMEGA_LIST_TRUNCATE_2]);
\r
3383 (NEW_GOAL `s2 = circumcenter {u0,u1,u2:real^3}`);
\r
3384 (REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list vl`);
\r
3385 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
3386 (REWRITE_TAC[ASSUME `s2 = omega_list V vl`]);
\r
3387 (MATCH_MP_TAC Rogers.XNHPWAB1);
\r
3388 (EXISTS_TAC `2` THEN REWRITE_TAC[IN]);
\r
3389 (ASM_REWRITE_TAC[]);
\r
3390 (ASM_MESON_TAC[]);
\r
3391 (NEW_GOAL `dist (s2,u0:real^3) = hl (truncate_simplex 2 (ul:(real^3)list))`);
\r
3392 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
3393 (REWRITE_TAC[GSYM (ASSUME `vl:(real^3)list = truncate_simplex 2 ul`)]);
\r
3394 (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);
\r
3395 (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
\r
3396 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
3397 (REWRITE_WITH `u0:real^3 = HD vl`);
\r
3398 (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);
\r
3399 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
\r
3400 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
\r
3401 (ASM_REWRITE_TAC[]);
\r
3403 (NEW_GOAL `~(s = s2:real^3)`);
\r
3405 (NEW_GOAL `dist (u0,s:real^3) < sqrt (&2)`);
\r
3406 (ONCE_REWRITE_TAC[DIST_SYM]);
\r
3407 (REWRITE_TAC[ASSUME `s = s2:real^3`]);
\r
3408 (ASM_MESON_TAC[]);
\r
3409 (ASM_REAL_ARITH_TAC);
\r
3411 (NEW_GOAL `(s2:real^3) IN voronoi_list V vl`);
\r
3412 (SIMP_TAC[ASSUME `s2 = omega_list V vl`]);
\r
3413 (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
\r
3415 (ASM_REWRITE_TAC[]);
\r
3417 (NEW_GOAL `(s3:real^3) IN voronoi_list V ul`);
\r
3418 (REWRITE_WITH `s3 = omega_list V ul`);
\r
3419 (EXPAND_TAC "s3" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; OMEGA_LIST]);
\r
3420 (REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) - 1 = 3`]);
\r
3421 (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
\r
3423 (ASM_REWRITE_TAC[]);
\r
3425 (NEW_GOAL `(s3:real^3) IN voronoi_list V vl`);
\r
3426 (MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET A) ==> a IN A`));
\r
3427 (EXISTS_TAC `voronoi_list V ul`);
\r
3429 (ASM_REWRITE_TAC[]);
\r
3430 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
3431 (REWRITE_TAC[VORONOI_LIST;VORONOI_SET;voronoi_closed;set_of_list;
\r
3432 SUBSET; IN_INTERS]);
\r
3433 (ONCE_REWRITE_TAC[IN]);
\r
3434 (REWRITE_TAC[IN_ELIM_THM]);
\r
3435 (REPEAT STRIP_TAC);
\r
3436 (FIRST_ASSUM MATCH_MP_TAC);
\r
3437 (EXISTS_TAC `v:real^3`);
\r
3438 (ASM_REWRITE_TAC[]);
\r
3439 (UNDISCH_TAC `v IN {u0, u1, u2:real^3}`);
\r
3442 (NEW_GOAL `s IN voronoi_list V vl`);
\r
3443 (NEW_GOAL `convex (voronoi_list V vl)`);
\r
3444 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
\r
3445 (UP_ASM_TAC THEN REWRITE_TAC[convex] THEN STRIP_TAC);
\r
3446 (UNDISCH_TAC `between s (s2,s3:real^3)`);
\r
3447 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
3448 (REPEAT STRIP_TAC);
\r
3449 (ONCE_REWRITE_TAC[GSYM IN]);
\r
3450 (REWRITE_TAC[ASSUME `s = u % s2 + v % s3:real^3`]);
\r
3451 (FIRST_ASSUM MATCH_MP_TAC);
\r
3452 (ASM_REWRITE_TAC[]);
\r
3454 (NEW_GOAL `~ (s IN affine hull {u0,u1,u2:real^3})`);
\r
3456 (NEW_GOAL `(s:real^3 - s2) dot (s - s2) = &0`);
\r
3457 (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);
\r
3458 (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
\r
3459 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
3460 (MATCH_MP_TAC MHFTTZN4);
\r
3461 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
\r
3462 (REPEAT STRIP_TAC);
\r
3463 (ASM_REWRITE_TAC[]);
\r
3464 (ASM_REWRITE_TAC[]);
\r
3465 (ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]);
\r
3466 (EXPAND_TAC "vl" THEN ASM_MESON_TAC[set_of_list]);
\r
3467 (UP_ASM_TAC THEN REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0;
\r
3468 NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
\r
3469 (ASM_REWRITE_TAC[]);
\r
3471 (NEW_GOAL `~affine_dependent {u0, u1, u2, s:real^3}`);
\r
3472 (ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {d,a,b,c}`]);
\r
3473 (MATCH_MP_TAC AFFINE_INDEPENDENT_INSERT);
\r
3474 (ASM_REWRITE_TAC[]);
\r
3475 (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
\r
3476 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
3477 (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);
\r
3478 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2` THEN ASM_REWRITE_TAC[]);
\r
3480 (NEW_GOAL `s2 IN convex hull {u0, u1, u2:real^3}`);
\r
3481 (REWRITE_WITH `s2 = omega_list V vl /\ {u0, u1, u2:real^3} = set_of_list vl`);
\r
3482 (EXPAND_TAC "s2" THEN EXPAND_TAC "vl");
\r
3483 (REWRITE_TAC[OMEGA_LIST_TRUNCATE_2;set_of_list]);
\r
3484 (MATCH_MP_TAC Rogers.XNHPWAB2);
\r
3486 (ASM_REWRITE_TAC[IN]);
\r
3487 (ASM_MESON_TAC[]);
\r
3489 (NEW_GOAL `~ (s3 IN affine hull {u0,u1,u2:real^3})`);
\r
3491 (NEW_GOAL `(s3:real^3 - s2) dot (s3 - s2) = &0`);
\r
3492 (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);
\r
3493 (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);
\r
3494 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);
\r
3495 (MATCH_MP_TAC MHFTTZN4);
\r
3496 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
\r
3497 (REPEAT STRIP_TAC);
\r
3498 (ASM_REWRITE_TAC[]);
\r
3499 (ASM_REWRITE_TAC[]);
\r
3500 (ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]);
\r
3501 (EXPAND_TAC "vl" THEN ASM_MESON_TAC[set_of_list]);
\r
3502 (UP_ASM_TAC THEN REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0;
\r
3503 NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
\r
3504 (REPEAT STRIP_TAC);
\r
3505 (UNDISCH_TAC `between s (s2,s3:real^3)`);
\r
3506 (REWRITE_TAC[ASSUME `s3 = s2:real^3`]);
\r
3507 (REWRITE_TAC[BETWEEN_REFL_EQ]);
\r
3508 (ASM_MESON_TAC[]);
\r
3510 (NEW_GOAL `DISJOINT {u0,u1} {s, s3:real^3}`);
\r
3511 (REWRITE_TAC[DISJOINT]);
\r
3512 (MATCH_MP_TAC (SET_RULE `~ (a IN s) /\ ~ (b IN s) ==> s INTER {a, b} = {}`));
\r
3513 (REPEAT STRIP_TAC);
\r
3514 (NEW_GOAL `s IN affine hull {u0, u1,u2:real^3}`);
\r
3515 (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
\r
3516 (UP_ASM_TAC THEN SET_TAC[]);
\r
3517 (ASM_MESON_TAC[]);
\r
3518 (NEW_GOAL `s3 IN affine hull {u0, u1,u2:real^3}`);
\r
3519 (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);
\r
3520 (UP_ASM_TAC THEN SET_TAC[]);
\r
3521 (ASM_MESON_TAC[]);
\r
3522 (UNDISCH_TAC `p IN aff_ge {u0, u1} {s, s3:real^3}`);
\r
3523 (ASM_SIMP_TAC[AFF_GE_2_2]);
\r
3524 (REWRITE_TAC[IN;IN_ELIM_THM]);
\r
3525 (NEW_GOAL `?k1 k2. k1 + k2 = &1 /\ k2 <= &0 /\ k1 % s + k2 % s2 = s3:real^3`);
\r
3526 (UNDISCH_TAC `between s (s2,s3:real^3)`);
\r
3527 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
3528 (REPEAT STRIP_TAC);
\r
3529 (EXISTS_TAC `&1 / v` THEN EXISTS_TAC ` -- u / v`);
\r
3530 (NEW_GOAL `~(v = &0)`);
\r
3532 (NEW_GOAL `s = s2:real^3`);
\r
3533 (REWRITE_TAC[ASSUME `s = u % s2 + v % s3:real^3`]);
\r
3534 (REWRITE_WITH `v = &0 /\ u = &1`);
\r
3535 (ASM_REAL_ARITH_TAC);
\r
3536 (VECTOR_ARITH_TAC);
\r
3537 (ASM_MESON_TAC[]);
\r
3538 (REPEAT STRIP_TAC);
\r
3539 (REWRITE_TAC[REAL_ARITH `&1 / v + --u / v = (&1 - u) / v`]);
\r
3540 (REWRITE_WITH `&1 - u = v`);
\r
3541 (ASM_REAL_ARITH_TAC);
\r
3542 (ASM_SIMP_TAC[REAL_DIV_REFL]);
\r
3543 (REWRITE_TAC[REAL_ARITH `--u / v <= &0 <=> &0 <= u / v`]);
\r
3544 (ASM_SIMP_TAC[REAL_LE_DIV]);
\r
3545 (REWRITE_TAC[ASSUME `s = u % s2 + v % s3:real^3`]);
\r
3546 (REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);
\r
3547 (REWRITE_TAC[VECTOR_ARITH
\r
3548 `((&1 / v * u) % s2 + (&1 / v * v) % s3) + --u / v % s2 = s3 <=>
\r
3549 (v / v - &1) % s3 = vec 0`]);
\r
3550 (REWRITE_WITH `v / v = &1`);
\r
3551 (ASM_SIMP_TAC[REAL_DIV_REFL]);
\r
3552 (VECTOR_ARITH_TAC);
\r
3553 (FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC);
\r
3554 (REWRITE_WITH `s3 = k1 % s + k2 % s2:real^3`);
\r
3555 (ASM_REWRITE_TAC[]);
\r
3556 (UNDISCH_TAC `s2 IN convex hull {u0, u1, u2:real^3}`);
\r
3557 (REWRITE_TAC[CONVEX_HULL_3; IN_ELIM_THM; IN]);
\r
3558 (REPEAT STRIP_TAC);
\r
3559 (UP_ASM_TAC THEN REWRITE_TAC[ASSUME `s2 = u % u0 + v % u1 + w % u2:real^3`]);
\r
3560 (REWRITE_TAC [VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);
\r
3561 (REWRITE_TAC[VECTOR_ARITH `t1 % u0 + t2 % u1 + t3 % s + (t4 * k1) % s +
\r
3562 ((t4 * k2) * u) % u0 + ((t4 * k2) * v) % u1 +
\r
3563 ((t4 * k2) * w) % u2 = (t4 * k2 * w) % u2 +
\r
3564 (t1 + t4 * k2 * u) % u0 + (t2 + t4 * k2 * v) % u1 + (t3 + t4 * k1) % s`]);
\r
3566 (NEW_GOAL `t4 * k2 * w = &0`);
\r
3567 (MATCH_MP_TAC AFFINE_DEPENDENT_KY_LEMMA1);
\r
3568 (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `s:real^3` THEN EXISTS_TAC `p:real^3`);
\r
3569 (EXISTS_TAC `t1 + t4 * k2 * u`);
\r
3570 (EXISTS_TAC `t2 + t4 * k2 * v`);
\r
3571 (EXISTS_TAC `t3 + t4 * k1`);
\r
3572 (ASM_REWRITE_TAC[]);
\r
3573 (REPEAT STRIP_TAC);
\r
3574 (UP_ASM_TAC THEN REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE
\r
3575 `{u2, u0, u1, s} = {u0, u1, u2, s}`]);
\r
3576 (ASM_REWRITE_TAC[]);
\r
3577 (ONCE_REWRITE_TAC[SET_RULE
\r
3578 `{u2, u0, u1, s} = {s, u0, u1, u2}`]);
\r
3579 (REWRITE_WITH `4 = SUC (CARD {u0,u1,u2:real^3})`);
\r
3580 (ASM_REWRITE_TAC[]);
\r
3582 (MATCH_MP_TAC (MESON[Geomdetail.CARD_CLAUSES_IMP]
\r
3583 `!s a. FINITE s /\ ~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s)`));
\r
3584 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
3586 (NEW_GOAL `s IN affine hull {u0, u1, u2:real^3}`);
\r
3587 (UP_ASM_TAC THEN REWRITE_TAC[IN_AFFINE_KY_LEMMA1]);
\r
3588 (ASM_MESON_TAC[]);
\r
3589 (REWRITE_TAC[GSYM (ASSUME `p =
\r
3590 (t4 * k2 * w) % u2 +
\r
3591 (t1 + t4 * k2 * u) % u0 +
\r
3592 (t2 + t4 * k2 * v) % u1 +
\r
3593 (t3 + t4 * k1) % s:real^3`)]);
\r
3594 (ONCE_REWRITE_TAC[SET_RULE
\r
3595 `{u2, u0, u1, s} = {u0, u1, u2,s}`]);
\r
3596 (ASM_REWRITE_TAC[]);
\r
3597 (REWRITE_TAC[REAL_ARITH
\r
3598 `t4 * k2 * w + (t1 + t4 * k2 * u) + (t2 + t4 * k2 * v) + t3 + t4 * k1 =
\r
3599 t1 + t2 + t3 + t4 * (k1 + k2 * (u + v + w))`]);
\r
3600 (ASM_REWRITE_TAC[REAL_MUL_RID]);
\r
3601 (NEW_GOAL `&0 <= -- k2`);
\r
3602 (ASM_REAL_ARITH_TAC);
\r
3603 (REWRITE_TAC[REAL_ARITH `a * b * c <= &0 <=> &0 <= a * c * (-- b)`]);
\r
3604 (ASM_SIMP_TAC[REAL_LE_MUL]);
\r
3605 (NEW_GOAL `p IN affine hull {u0,u1,s:real^3}`);
\r
3606 (REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);
\r
3607 (EXISTS_TAC `t1 + t4 * k2 * u`);
\r
3608 (EXISTS_TAC `t2 + t4 * k2 * v`);
\r
3609 (EXISTS_TAC `t3 + t4 * k1`);
\r
3610 (ASM_REWRITE_TAC[VECTOR_MUL_LZERO;VECTOR_ADD_LID]);
\r
3611 (REWRITE_TAC[REAL_ARITH
\r
3612 `(t1 + t4 * k2 * u) + (t2 + t4 * k2 * v) + t3 + t4 * k1
\r
3613 = (t1 + t2 + t3 + t4 * (k1 + k2 * (u + v + w))) - (t4 * k2 * w)`]);
\r
3614 (ASM_REWRITE_TAC[REAL_MUL_RID]);
\r
3616 (NEW_GOAL `~(p:real^3 IN B4)`);
\r
3618 (UP_ASM_TAC THEN EXPAND_TAC "B4" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; HD;TL]);
\r
3619 (REWRITE_WITH `mxi V [u0; u1; u2; u3] = s`);
\r
3620 (ASM_MESON_TAC[]);
\r
3621 (ASM_REWRITE_TAC[]);
\r
3624 (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 2`);
\r
3625 (GEN_TAC THEN STRIP_TAC);
\r
3626 (NEW_GOAL `~(y = 4 \/ y = 0 \/ y = 1 \/ y = 3)`);
\r
3629 (NEW_GOAL `i = 2`);
\r
3630 (FIRST_ASSUM MATCH_MP_TAC);
\r
3631 (ASM_REWRITE_TAC[]);
\r
3632 (GEN_TAC THEN STRIP_TAC);
\r
3633 (ASM_REWRITE_TAC[]);
\r
3634 (FIRST_ASSUM MATCH_MP_TAC);
\r
3635 (ASM_REWRITE_TAC[]);
\r
3637 (* ===================================================================== *)
\r
3639 (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==>
\r
3640 ~ (y = 4 \/ y = 0 \/ y = 1 \/ y = 2)`);
\r
3641 (REPEAT STRIP_TAC);
\r
3642 (NEW_GOAL `mcell 4 V ul = {}`);
\r
3643 (SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);
\r
3646 (ASM_MESON_TAC[]);
\r
3647 (ASM_MESON_TAC[]);
\r
3649 (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 4`]);
\r
3650 (REWRITE_TAC[ASSUME `mcell 4 V ul = {}`]);
\r
3653 (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 0`;
\r
3654 MCELL_EXPLICIT;mcell0]);
\r
3656 (NEW_GOAL `~(p:real^3 IN ball (HD ul,sqrt (&2)))`);
\r
3657 (ASM_SET_TAC[IN_DIFF]);
\r
3658 (UP_ASM_TAC THEN ASM_REWRITE_TAC[HD;IN;ball;IN_ELIM_THM]);
\r
3660 (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 1`;
\r
3661 MCELL_EXPLICIT;mcell1]);
\r
3663 (REWRITE_TAC[IN_DIFF]);
\r
3665 (ASM_MESON_TAC[]);
\r
3668 (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 2`;
\r
3669 MCELL_EXPLICIT;mcell2]);
\r
3672 (UNDISCH_TAC `~(p IN aff_ge {u0, u1} {mxi V ul, omega_list_n V ul 3})`);
\r
3673 (REWRITE_TAC[IN_INTER; ASSUME `ul = [u0;u1;u2;u3:real^3]`;HD;TL]);
\r
3677 (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 3`);
\r
3678 (GEN_TAC THEN STRIP_TAC);
\r
3679 (NEW_GOAL `~(y = 4 \/ y = 0 \/ y = 1 \/ y = 2)`);
\r
3682 (NEW_GOAL `i = 3`);
\r
3683 (FIRST_ASSUM MATCH_MP_TAC);
\r
3684 (ASM_REWRITE_TAC[]);
\r
3685 (GEN_TAC THEN STRIP_TAC);
\r
3686 (ASM_REWRITE_TAC[]);
\r
3687 (FIRST_ASSUM MATCH_MP_TAC);
\r
3688 (ASM_REWRITE_TAC[])]);;
\r