1 (* ========================================================================= *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Authour : VU KHAC KY *)
5 (* Book lemma: QZKSYKG *)
8 (* ========================================================================= *)
11 module Qzksykg = struct
14 open Vukhacky_tactics;;
21 open Marchal_cells_2_new;;
26 let CONVEX_HULL_4_IMP_3_1 = prove_by_refinement (
28 x IN convex hull {a,b,c,d} ==>
30 x1 IN convex hull {a,b,c} /\
31 &0 <= t1 /\ &0 <= t2 /\ t1 + t2 = &1 /\
32 x = t1 % x1 + t2 % d)`,
33 [(REWRITE_TAC[CONVEX_HULL_4; CONVEX_HULL_3;IN;IN_ELIM_THM]);
35 (ASM_CASES_TAC `z < &1`);
37 (EXISTS_TAC `(u/ (u + v + w)) % a + (v/ (u+v+w)) % b + (w/(u+v+w)) % (c:real^3)`);
38 (EXISTS_TAC `(u + v + w):real` THEN EXISTS_TAC `z:real`);
40 (EXISTS_TAC `u/(u+v+w)`);
41 (EXISTS_TAC `v/(u+v+w)`);
42 (EXISTS_TAC `w/(u+v+w)`);
44 (MATCH_MP_TAC REAL_LE_DIV);
46 (MATCH_MP_TAC REAL_LE_DIV);
48 (MATCH_MP_TAC REAL_LE_DIV);
50 (REWRITE_TAC[REAL_ARITH `u / (u + v + w) + v / (u + v + w) + w / (u + v + w)=
51 (u + v + w) / (u + v + w)`]);
52 (MATCH_MP_TAC REAL_DIV_REFL);
58 (REWRITE_TAC[VECTOR_ARITH `s % (s1 /s % a + s2 / s % b + s3/ s % c) =
59 (s * s1 / s) % a + (s * s2 / s) % b + (s * s3 / s) % c`]);
60 (REWRITE_TAC[REAL_ARITH `s * s1 / s = s1 * (s / s)`]);
61 (REWRITE_WITH `(u + v + w) / (u + v + w) = &1`);
62 (MATCH_MP_TAC REAL_DIV_REFL);
64 (ASM_REWRITE_TAC[REAL_MUL_RID] THEN VECTOR_ARITH_TAC);
66 (NEW_GOAL `z = &1 /\ u = &0 /\ v = &0 /\ w = &0`);
68 (EXISTS_TAC `a:real^3`);
69 (EXISTS_TAC `&0` THEN EXISTS_TAC `&1`);
70 (ASM_REWRITE_TAC[ARITH_RULE `&0 <= &0 /\ &0 <= &1 /\ &0 + &1 = &1`]);
72 (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);
73 (ASM_REWRITE_TAC[ARITH_RULE `&0 <= &0 /\ &0 <= &1 /\ &1 + &0 + &0 = &1`]);
75 (VECTOR_ARITH_TAC)]);;
78 let BARV_2_EXPLICIT = prove_by_refinement (
79 `!V vl. barV V 2 vl ==> ?u0 u1 u2. vl = [u0;u1;u2]`,
80 [(REWRITE_TAC[BARV] THEN REPEAT STRIP_TAC);
81 (NEW_GOAL `?x0 xl. (vl:(real^3)list) = CONS x0 xl /\ LENGTH xl = 2`);
82 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
84 (UP_ASM_TAC THEN STRIP_TAC);
85 (EXISTS_TAC `x0:real^3`);
86 (NEW_GOAL `?x1 yl. (xl:(real^3)list) = CONS x1 yl /\ LENGTH yl = 1`);
87 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
89 (UP_ASM_TAC THEN STRIP_TAC);
90 (EXISTS_TAC `x1:real^3`);
91 (NEW_GOAL `?x2 zl. (yl:(real^3)list) = CONS x2 zl /\ LENGTH zl = 0`);
92 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
94 (UP_ASM_TAC THEN STRIP_TAC);
95 (EXISTS_TAC `x2:real^3`);
96 (NEW_GOAL `(zl:(real^3)list) = []`);
97 (ASM_MESON_TAC[LENGTH_EQ_NIL]);
98 (ASM_REWRITE_TAC[])]);;
100 let ROGERS_EXPLICIT_2 = prove_by_refinement (
102 saturated V /\ packing V /\ barV V 2 ul ==>
103 rogers V ul = convex hull
104 {HD ul, omega_list_n V ul 1, omega_list_n V ul 2}`,
106 [(REPEAT STRIP_TAC THEN REWRITE_TAC[ROGERS]);
107 (NEW_GOAL `?u0 u1 u2. (ul:(real^3)list) = [u0:real^3;u1;u2]`);
108 (MATCH_MP_TAC BARV_2_EXPLICIT THEN EXISTS_TAC `V:real^3->bool`);
110 (UP_ASM_TAC THEN STRIP_TAC);
111 (REWRITE_WITH `{j | j < LENGTH (ul:(real^3)list)} = {0, 1,2}`);
112 (ASM_REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC 0)) = 3`]);
113 (SET_TAC[ARITH_RULE `0 < 3 /\ 1 < 3 /\ 2 < 3 /\
114 (!j. j < 3 ==> (j=0\/j=1\/j=2))`]);
115 (REWRITE_TAC[IMAGE]);
117 (REWRITE_TAC[SET_RULE `!x. x IN {0,1,2} <=> (x = 0 \/x = 1 \/x = 2)`]);
119 `!y. (?x. (x = 0 \/ x = 1 \/ x = 2) /\ y = omega_list_n V ul x)
120 <=> (y = omega_list_n V ul 0) \/ (y = omega_list_n V ul 1) \/
121 (y = omega_list_n V ul 2)`);
124 `{y | y = omega_list_n V ul 0 \/ y = omega_list_n V ul 1 \/
125 y = omega_list_n V ul 2}
126 = {omega_list_n V ul 0, omega_list_n V ul 1, omega_list_n V ul 2}`);
128 (REWRITE_WITH `omega_list_n V ul 0 = HD ul`);
129 (REWRITE_TAC[OMEGA_LIST_N])]);;
131 let TWO_REARRANGEMENT_LEMMA = prove_by_refinement (
132 `!V ul p u0 u1 u2 u3.
133 packing V /\ saturated V /\ barV V 3 ul /\ ul = [u0;u1;u2;u3] ==>
134 (?p. p permutes 0..1 /\ [u1;u0;u2;u3] = left_action_list p ul)`,
136 (ABBREV_TAC `p = (\i. if i = 0 then 1 else if i = 1 then 0 else i)`);
137 (EXISTS_TAC `p:num->num`);
139 (NEW_GOAL `p 0 = 1`);
145 (NEW_GOAL `p 1 = 0`);
152 (NEW_GOAL `!i. 1 < i ==> p i = i`);
165 (NEW_GOAL `inverse p 0 = 1`);
166 (REWRITE_TAC[inverse]);
167 (MATCH_MP_TAC SELECT_UNIQUE);
168 (GEN_TAC THEN EQ_TAC);
169 (REWRITE_TAC[BETA_THM]);
170 (ASM_CASES_TAC `y = 0`);
173 (ASM_CASES_TAC `1 < y`);
177 (STRIP_TAC THEN ASM_REWRITE_TAC[BETA_THM]);
179 (NEW_GOAL `inverse p 1 = 0`);
180 (REWRITE_TAC[inverse]);
181 (MATCH_MP_TAC SELECT_UNIQUE);
182 (GEN_TAC THEN EQ_TAC);
183 (REWRITE_TAC[BETA_THM]);
184 (ASM_CASES_TAC `y = 1`);
187 (ASM_CASES_TAC `1 < y`);
191 (STRIP_TAC THEN ASM_REWRITE_TAC[BETA_THM]);
193 (NEW_GOAL `!i. 1 < i ==> inverse p i = i`);
195 (REWRITE_TAC[inverse]);
196 (MATCH_MP_TAC SELECT_UNIQUE);
197 (GEN_TAC THEN EQ_TAC);
198 (REWRITE_TAC[BETA_THM]);
199 (ASM_CASES_TAC `y = 0`);
205 (ASM_CASES_TAC `y = 1`);
214 (NEW_GOAL `(p:num->num) y = y`);
215 (UNDISCH_TAC `1 < y` THEN ASM_REWRITE_TAC[]);
217 (STRIP_TAC THEN ASM_REWRITE_TAC[BETA_THM]);
220 (MATCH_MP_TAC Hypermap.lemma_permutes_via_surjetive);
221 (REWRITE_WITH `0..1 = {0,1}`);
222 (REWRITE_TAC[GSYM NUMSEG_LE; ARITH_RULE `x <= 1 <=> x = 0 \/ x = 1`]);
224 (REWRITE_TAC[Geomdetail.FINITE6; SET_RULE `a IN {x,y} <=> a = x \/ a = y`]);
227 (ASM_REWRITE_TAC[left_action_list;LENGTH; ARITH_RULE
228 `SUC (SUC (SUC (SUC 0))) = 4`]);
229 (ASM_REWRITE_TAC[TABLE_4]);
230 (ASM_SIMP_TAC[TABLE_4; EL;HD;TL; ARITH_RULE `1 < 2 /\ 1 < 3`]);
231 (REWRITE_TAC[EL; HD; TL; ARITH_RULE `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`])]);;
234 let SET_SUBSET_AFFINE_HULL = prove (
235 `!S:real^3->bool. S SUBSET affine hull S`,
237 MATCH_MP_TAC (SET_RULE `(?C. A SUBSET C /\ C SUBSET B) ==> A SUBSET B`) THEN
238 EXISTS_TAC `convex hull S:real^3->bool` THEN
239 REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL; SUBSET] THEN
240 REWRITE_TAC[IN_SET_IMP_IN_CONVEX_HULL_SET]);;
242 (* ========================================================================= *)
250 ~ (mcell k V ul = {}) /\
251 p permutes 0..(k - 1) /\
252 vl = left_action_list p ul
261 ==> (mcell k V ul SUBSET
262 UNIONS{rogers V (left_action_list p ul) | p permutes 0..(k-1)})`;;
264 (* ========================================================================= *)
266 let QZKSYKG1 = prove_by_refinement (QZKSYKG1_concl,
268 (ASM_CASES_TAC `k = 0 \/ k = 1`);
269 (UNDISCH_TAC `p permutes 0..(k-1)`);
270 (REWRITE_WITH `k - 1 = 0`);
272 (REWRITE_TAC[Packing3.PERMUTES_TRIVIAL]);
274 (ASM_REWRITE_TAC[Packing3.LEFT_ACTION_LIST_I]);
275 (NEW_GOAL `k IN {2,3,4}`);
280 (ASM_CASES_TAC `k = 4`);
281 (UNDISCH_TAC `~(mcell k V ul = {})`);
282 (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);
285 (REWRITE_TAC[MESON[IN] `barV V 3 s <=> s IN barV V 3`]);
286 (MATCH_MP_TAC Rogers.YIFVQDV_1);
287 (ASM_REWRITE_TAC[IN]);
288 (REWRITE_WITH `3 = k - 1`);
293 (* Cases k = 3, k = 2 *)
297 (!j. k - 1 <= j /\ j <= 3
298 ==> omega_list_n V vl j = omega_list_n V ul j)`);
299 (MATCH_MP_TAC YNHYJIT);
300 (EXISTS_TAC `p:num->num`);
302 (UNDISCH_TAC `~(mcell k V ul = {})`);
304 (ASM_CASES_TAC `k = 3`);
305 (SIMP_TAC [ASSUME `k = 3`; MCELL_EXPLICIT; mcell3]);
308 (ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`]);
314 (SIMP_TAC [ASSUME `k = 2`; MCELL_EXPLICIT; mcell2]);
318 (ASM_REWRITE_TAC[ARITH_RULE `2 - 1 = 1`]);
322 (* ========================================================================= *)
325 let QZKSYKG2 = prove_by_refinement ( QZKSYKG2_concl,
328 (ASM_CASES_TAC `k = 0 \/ k = 1`);
329 (REWRITE_WITH `k - 1 = 0`);
331 (REWRITE_TAC[Packing3.PERMUTES_TRIVIAL]);
332 (REWRITE_TAC[Packing3.SING_GSPEC_APP; UNIONS_1;
333 Packing3.LEFT_ACTION_LIST_I]);
334 (UP_ASM_TAC THEN STRIP_TAC);
335 (ASM_SIMP_TAC[MCELL_EXPLICIT; mcell0]);
337 (ASM_SIMP_TAC[MCELL_EXPLICIT; mcell1]);
342 (* ======================================================================== *)
344 (ASM_CASES_TAC `k = 4`);
345 (REWRITE_WITH `k - 1 = 3`);
347 (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`; mcell4]);
349 (REWRITE_WITH `convex hull set_of_list ul =
350 UNIONS {rogers V (left_action_list p ul) | p permutes 0..3}`);
351 (MATCH_MP_TAC Rogers.WQPRRDY);
352 (ASM_REWRITE_TAC[IN]);
356 (* ======================================================================== *)
358 (ASM_CASES_TAC `k = 3`);
359 (REWRITE_WITH `k - 1 = 2`);
361 (ASM_SIMP_TAC[MCELL_EXPLICIT; mcell3]);
364 (ABBREV_TAC `m = mxi V ul`);
365 (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
366 (MATCH_MP_TAC BARV_3_EXPLICIT THEN EXISTS_TAC `V:real^3->bool`);
368 (UP_ASM_TAC THEN STRIP_TAC);
369 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list;
370 SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);
371 (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
373 (REWRITE_TAC[SUBSET]);
374 (GEN_TAC THEN DISCH_TAC);
375 (NEW_GOAL `(?x1 t1 t2.
376 x1 IN convex hull {u0, u1, u2:real^3} /\
380 x = t1 % x1 + t2 % m)`);
381 (ASM_SIMP_TAC[CONVEX_HULL_4_IMP_3_1]);
382 (UP_ASM_TAC THEN STRIP_TAC);
383 (REWRITE_TAC[ASSUME `x:real^3 = t1 % x1 + t2 % m`]);
385 (UNDISCH_TAC `x1 IN convex hull {u0, u1, u2:real^3}`);
386 (REWRITE_WITH `convex hull {u0,u1,u2:real^3} =
387 UNIONS {rogers V (left_action_list p (truncate_simplex 2 ul)) | p permutes 0..2}`);
388 (REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list (truncate_simplex 2 ul)`);
389 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);
390 (MATCH_MP_TAC Rogers.WQPRRDY);
391 (ASM_REWRITE_TAC[IN]);
392 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
393 (EXISTS_TAC `3` THEN REWRITE_TAC[ARITH_RULE `2 <= 3`]);
395 (REWRITE_TAC[IN_UNIONS]);
398 (NEW_GOAL `?p:num->num. p permutes 0..2 /\ t = rogers V (left_action_list p (truncate_simplex 2 ul))`);
400 (UP_ASM_TAC THEN STRIP_TAC);
401 (ABBREV_TAC `zl:(real^3)list = left_action_list p (truncate_simplex 2 ul)`);
402 (EXISTS_TAC `rogers V (left_action_list p ul)`);
405 (ABBREV_TAC `vl:(real^3)list = left_action_list p ul`);
409 {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`);
410 (MATCH_MP_TAC ROGERS_EXPLICIT);
412 (REWRITE_TAC[MESON[IN] `barV V 3 vl <=> vl IN barV V 3`]);
413 (REWRITE_WITH `vl IN barV V 3 /\
414 omega_list_n V vl 2 = omega_list_n V ul 2 /\
415 omega_list_n V vl 3 = omega_list_n V ul 3 /\
416 mxi V vl = mxi V ul`);
417 (MATCH_MP_TAC LEFT_ACTION_LIST_PROPERTIES);
418 (EXISTS_TAC `p:num->num` THEN ASM_REWRITE_TAC[]);
420 (NEW_GOAL `zl = truncate_simplex 2 (vl:(real^3)list)`);
421 (EXPAND_TAC "zl" THEN EXPAND_TAC "vl");
422 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; LENGTH;
423 ARITH_RULE `SUC (SUC (SUC 0)) = 3`; TABLE_4; ARITH_RULE `SUC 3 = 4`;
424 ASSUME `ul = [u0;u1;u2;u3:real^3]`; left_action_list]);
426 (REWRITE_WITH `EL (inverse p 0) [u0; u1; u2:real^3] =
427 EL (inverse p 0) [u0; u1; u2; u3] /\
428 EL (inverse p 1) [u0; u1; u2:real^3] =
429 EL (inverse p 1) [u0; u1; u2; u3] /\
430 EL (inverse p 2) [u0; u1; u2:real^3] =
431 EL (inverse p 2) [u0; u1; u2; u3]`);
432 (REWRITE_WITH `[u0; u1; u2:real^3] = truncate_simplex 2 [u0; u1; u2; u3]`);
433 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
435 (NEW_GOAL `!i. i IN 0..2 ==> inverse p i IN 0..2`);
437 (ABBREV_TAC `y = inverse (p:num->num) i`);
438 (ASM_CASES_TAC `y IN 0..2`);
441 (MP_TAC (ASSUME `p permutes 0..2`) THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
443 (NEW_GOAL `(p:num->num) y = y`);
445 (UP_ASM_TAC THEN EXPAND_TAC "y");
446 (REWRITE_WITH `(p:num->num) (inverse p i) = i`);
447 (MESON_TAC[PERMUTES_INVERSES; ASSUME `p permutes 0..2`]);
453 (MATCH_MP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
454 (REWRITE_TAC[LENGTH; ARITH_RULE `2 + 1 <= SUC(SUC(SUC(SUC 0)))`]);
455 (NEW_GOAL `inverse p 0 IN 0..2`);
456 (FIRST_ASSUM MATCH_MP_TAC);
457 (REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
458 (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0]);
461 (MATCH_MP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
462 (REWRITE_TAC[LENGTH; ARITH_RULE `2 + 1 <= SUC(SUC(SUC(SUC 0)))`]);
463 (NEW_GOAL `inverse p 1 IN 0..2`);
464 (FIRST_ASSUM MATCH_MP_TAC);
465 (REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
466 (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0]);
468 (MATCH_MP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
469 (REWRITE_TAC[LENGTH; ARITH_RULE `2 + 1 <= SUC(SUC(SUC(SUC 0)))`]);
470 (NEW_GOAL `inverse p 2 IN 0..2`);
471 (FIRST_ASSUM MATCH_MP_TAC);
472 (REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
473 (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0]);
475 (NEW_GOAL `rogers V zl =
476 convex hull {HD zl, omega_list_n V zl 1, omega_list_n V zl 2}`);
477 (MATCH_MP_TAC ROGERS_EXPLICIT_2);
479 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
480 (EXISTS_TAC `3` THEN REWRITE_TAC[ARITH_RULE `2 <= 3`]);
482 (REWRITE_TAC[MESON[IN] `barV V 3 vl <=> vl IN barV V 3`]);
483 (REWRITE_WITH `vl IN barV V 3 /\
484 omega_list_n V vl 2 = omega_list_n V ul 2 /\
485 omega_list_n V vl 3 = omega_list_n V ul 3 /\
486 mxi V vl = mxi V ul`);
487 (MATCH_MP_TAC LEFT_ACTION_LIST_PROPERTIES);
488 (EXISTS_TAC `p:num->num` THEN ASM_REWRITE_TAC[]);
491 (* ------------------------------ *)
493 `x1 IN convex hull {HD zl, omega_list_n V zl 1, omega_list_n V zl 2}`);
495 (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_3;IN;IN_ELIM_THM]);
497 (ABBREV_TAC `q1 = omega_list_n V zl 1`);
498 (ABBREV_TAC `q2 = omega_list_n V zl 2`);
499 (ABBREV_TAC `s3 = omega_list_n V ul 3`);
500 (ABBREV_TAC `q0 = HD (zl:(real^3)list)`);
502 (NEW_GOAL `vl IN barV V 3 /\
503 omega_list_n V vl 2 = omega_list_n V ul 2 /\
504 omega_list_n V vl 3 = omega_list_n V ul 3 /\
505 mxi V vl = mxi V ul`);
506 (MATCH_MP_TAC LEFT_ACTION_LIST_PROPERTIES);
507 (EXISTS_TAC `p:num->num`);
509 (UP_ASM_TAC THEN REWRITE_TAC[IN] THEN STRIP_TAC);
510 (NEW_GOAL `?v0 v1 v2 v3. vl = [v0;v1;v2;v3:real^3]`);
511 (MATCH_MP_TAC BARV_3_EXPLICIT);
512 (EXISTS_TAC `V:real^3->bool`);
514 (UP_ASM_TAC THEN STRIP_TAC);
516 (NEW_GOAL `HD vl = q0:real^3`);
517 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
518 (EXPAND_TAC "q0" THEN
519 REWRITE_TAC[ASSUME `zl:(real^3)list = truncate_simplex 2 vl`]);
520 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
521 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
523 (NEW_GOAL `omega_list_n V vl 1 = q1`);
524 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
525 (EXPAND_TAC "q1" THEN
526 REWRITE_TAC[ASSUME `zl:(real^3)list = truncate_simplex 2 vl`]);
527 (REWRITE_TAC[ARITH_RULE `2 = 1 + 1`]);
528 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
529 (MATCH_MP_TAC Packing3.OMEGA_LIST_N_LEMMA);
530 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
532 (NEW_GOAL `omega_list_n V vl 2 = q2`);
533 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
534 (EXPAND_TAC "q2" THEN
535 REWRITE_TAC[ASSUME `zl:(real^3)list = truncate_simplex 2 vl`]);
536 (REWRITE_WITH `truncate_simplex 2 (vl:(real^3)list) =
537 truncate_simplex (2 + 0) vl`);
538 (REWRITE_TAC[ARITH_RULE `2 + 0 = 2`]);
539 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
540 (MATCH_MP_TAC Packing3.OMEGA_LIST_N_LEMMA);
541 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
543 (UNDISCH_TAC `omega_list_n V vl 2 = omega_list_n V ul 2` THEN
546 (NEW_GOAL `between m (q2, s3:real^3)`);
547 (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
548 dist (u0,s) = sqrt (&2) /\
550 (MATCH_MP_TAC MXI_EXPLICIT);
551 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN
552 EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[]);
553 (UP_ASM_TAC THEN STRIP_TAC);
555 (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;IN;IN_ELIM_THM;
556 CONVEX_HULL_2; CONVEX_HULL_4]);
558 (EXISTS_TAC `t1 * u` THEN EXISTS_TAC `t1 * v`);
559 (EXISTS_TAC `t1 * w + t2 * u'` THEN EXISTS_TAC `t2 * v'`);
560 (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_ADD]);
563 `t1 * u + t1 * v + (t1 * w + t2 * u') + t2 * v' =
564 t1 * (u + v + w) + t2 * (u' + v')`);
566 (ASM_REWRITE_TAC[REAL_MUL_RID]);
570 (* ========================================================================= *)
574 (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
575 (MATCH_MP_TAC BARV_3_EXPLICIT THEN EXISTS_TAC `V:real^3->bool`);
577 (UP_ASM_TAC THEN STRIP_TAC);
578 (SIMP_TAC[ASSUME `k = 2`; MCELL_EXPLICIT; mcell2]);
582 (ABBREV_TAC `m = mxi V ul`);
583 (ABBREV_TAC `s2 = omega_list_n V ul 2`);
584 (ABBREV_TAC `s3 = omega_list_n V ul 3`);
585 (ASM_REWRITE_TAC[HD;TL; ARITH_RULE `2 - 1 = 1`]);
586 (MATCH_MP_TAC (SET_RULE `(?C. C SUBSET B /\ A SUBSET C) ==> A SUBSET B`));
587 (EXISTS_TAC `convex hull {u0, u1, s2, s3:real^3}`);
588 (REPEAT STRIP_TAC); (* Two subgoals *)
590 (* ------------------------------------------------------ *)
592 (MATCH_MP_TAC (SET_RULE `(?C. C SUBSET B /\ A SUBSET C) ==> A SUBSET B`));
593 (EXISTS_TAC `rogers V ul UNION rogers V [u1;u0;u2;u3:real^3]`);
595 (REWRITE_TAC[SUBSET; IN_UNIONS; IN_UNION]);
597 (REWRITE_TAC[IN;IN_ELIM_THM]);
598 (EXISTS_TAC `rogers V ul`);
600 (EXISTS_TAC `I:num->num`);
601 (ASM_REWRITE_TAC[PERMUTES_I; Packing3.LEFT_ACTION_LIST_I]);
602 (UP_ASM_TAC THEN REWRITE_TAC[IN]);
604 (REWRITE_TAC[IN;IN_ELIM_THM]);
605 (EXISTS_TAC `rogers V [u1;u0;u2;u3]`);
607 (NEW_GOAL `?p. p permutes 0..1 /\ [u1;u0;u2;u3:real^3] = left_action_list p ul`);
608 (MATCH_MP_TAC TWO_REARRANGEMENT_LEMMA);
609 (EXISTS_TAC `V:real^3->bool`);
611 (UP_ASM_TAC THEN STRIP_TAC);
612 (EXISTS_TAC `p:num->num`);
614 (UP_ASM_TAC THEN REWRITE_TAC[IN]);
615 (NEW_GOAL `?p. p permutes 0..1 /\ [u1;u0;u2;u3:real^3] = left_action_list p ul`);
616 (MATCH_MP_TAC TWO_REARRANGEMENT_LEMMA);
617 (EXISTS_TAC `V:real^3->bool`);
619 (UP_ASM_TAC THEN STRIP_TAC);
622 (ABBREV_TAC `vl = [u1;u0;u2;u3:real^3]`);
623 (NEW_GOAL `barV V 3 vl /\
624 (!j. 1 <= j /\ j <= 3
625 ==> omega_list_n V vl j = omega_list_n V ul j)`);
626 (ONCE_REWRITE_TAC[ARITH_RULE `1 = 2 - 1`]);
627 (MATCH_MP_TAC YNHYJIT);
628 (EXISTS_TAC `p:num->num` THEN REWRITE_TAC[ARITH_RULE `2 - 1 = 1`]);
629 (ASM_REWRITE_TAC[SET_RULE `2 IN {2,3,4}`]);
630 (UP_ASM_TAC THEN STRIP_TAC);
631 (ABBREV_TAC `s1 = omega_list_n V ul 1`);
632 (NEW_GOAL `rogers V ul = convex hull {HD ul, s1, s2, s3}`);
633 (EXPAND_TAC "s1" THEN EXPAND_TAC "s2" THEN EXPAND_TAC "s3");
634 (MATCH_MP_TAC ROGERS_EXPLICIT);
637 (NEW_GOAL `rogers V vl = convex hull {HD vl, omega_list_n V vl 1,
638 omega_list_n V vl 2, omega_list_n V vl 3}`);
639 (MATCH_MP_TAC ROGERS_EXPLICIT);
642 (NEW_GOAL `omega_list_n V vl 1 = s1`);
643 (EXPAND_TAC "s1" THEN FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
644 (NEW_GOAL `omega_list_n V vl 2 = s2`);
645 (EXPAND_TAC "s2" THEN FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
646 (NEW_GOAL `omega_list_n V vl 3 = s3`);
647 (EXPAND_TAC "s3" THEN FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
649 (ASM_REWRITE_TAC[HD]);
650 (REWRITE_TAC[GSYM (ASSUME `vl = left_action_list p (ul:(real^3)list)`);
651 GSYM (ASSUME `ul = [u0; u1; u2; u3:real^3]`)]);
652 (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);
654 (NEW_GOAL `s1 = circumcenter {u1, u0:real^3}`);
655 (EXPAND_TAC "s1" THEN MATCH_MP_TAC Marchal_cells_2_new.OMEGA_LIST_1_EXPLICIT_NEW);
656 (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3` THEN REWRITE_TAC[IN]);
658 (REWRITE_WITH `hl [u1;u0:real^3] =
659 hl (truncate_simplex 1 (ul:(real^3)list))`);
660 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1; HL]);
661 (REWRITE_TAC[set_of_list; SET_RULE `{a,b} = {b,a}`]);
663 (UP_ASM_TAC THEN REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN STRIP_TAC);
666 (REWRITE_TAC[SUBSET; CONVEX_HULL_4; IN; IN_ELIM_THM; IN_UNION]);
669 (ASM_CASES_TAC `u <= v:real`);
671 (EXISTS_TAC `v - u:real` THEN EXISTS_TAC `&2 * u`);
672 (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`);
673 (ASM_SIMP_TAC[REAL_ARITH `v - u + &2 * u + w + z = u + v + w + z`; REAL_LE_MUL; REAL_ARITH `&0 <= &2`; REAL_ARITH `&0 <= a - b <=> b <= a`]);
675 (NEW_GOAL `v <= u:real`);
676 (ASM_REAL_ARITH_TAC);
678 (EXISTS_TAC `u - v:real` THEN EXISTS_TAC `&2 * v`);
679 (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`);
680 (ASM_SIMP_TAC[REAL_ARITH `u - v + &2 * v + w + z = u + v + w + z`;
681 REAL_LE_MUL; REAL_ARITH `&0 <= &2`; REAL_ARITH `&0 <= a - b <=> b <= a`]);
684 (* ------------------------------------------------------ *)
686 (REWRITE_TAC[SUBSET; IN_INTER]);
688 (ABBREV_TAC `s1 = omega_list_n V ul 1`);
690 (NEW_GOAL `s1 = circumcenter {u0, u1:real^3}`);
691 (EXPAND_TAC "s1" THEN MATCH_MP_TAC Marchal_cells_2_new.OMEGA_LIST_1_EXPLICIT_NEW);
692 (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3` THEN REWRITE_TAC[IN]);
694 (REWRITE_WITH `hl [u0;u1:real^3] =
695 hl (truncate_simplex 1 (ul:(real^3)list))`);
696 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1; HL;set_of_list]);
699 (ABBREV_TAC `vl:(real^3)list = truncate_simplex 1 ul`);
701 (NEW_GOAL `s1:real^3 IN voronoi_list V vl`);
702 (EXPAND_TAC "vl" THEN EXPAND_TAC "s1");
703 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
704 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
705 (NEW_GOAL `s2:real^3 IN voronoi_list V vl`);
706 (EXPAND_TAC "vl" THEN EXPAND_TAC "s2");
707 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
708 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
709 (NEW_GOAL `s3:real^3 IN voronoi_list V vl`);
710 (EXPAND_TAC "vl" THEN EXPAND_TAC "s3");
711 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
712 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
714 (NEW_GOAL `m IN voronoi_list V vl`);
715 (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`);
716 (REWRITE_WITH `m = s2:real^3`);
717 (EXPAND_TAC "m" THEN REWRITE_TAC[mxi]);
724 (NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
725 dist (u0,s) = sqrt (&2) /\
727 (MATCH_MP_TAC MXI_EXPLICIT);
728 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
730 (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
731 (FIRST_X_ASSUM CHOOSE_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
734 (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
735 (EXISTS_TAC `convex hull {s2, s3:real^3}`);
737 (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
738 (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V vl <=>
739 convex hull {s2, s3} SUBSET (convex hull (voronoi_list V vl))`);
740 (REWRITE_WITH `convex hull (voronoi_list V vl) = voronoi_list V vl`);
741 (REWRITE_TAC[CONVEX_HULL_EQ]);
742 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
743 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
746 (NEW_GOAL `~(u0 = u1:real^3)`);
748 (NEW_GOAL `LENGTH (ul:(real^3)list) = 3 + 1 /\
749 CARD (set_of_list ul) = 3 + 1`);
750 (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
751 (EXISTS_TAC `V:real^3->bool`);
753 (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list;
754 SET_RULE `{u1, u1, u2, u3} = {u1,u2,u3}`]);
755 (NEW_GOAL `CARD {u1,u2,u3:real^3} <= 3`);
756 (REWRITE_TAC[Geomdetail.CARD3]);
759 (UNDISCH_TAC `x IN aff_ge {u0, u1} {m, s3:real^3}`);
760 (REWRITE_WITH `aff_ge {u0, u1} {m, s3:real^3} =
764 t1 + t2 + t3 + t4 = &1 /\
765 y = t1 % u0 + t2 % u1 + t3 % m + t4 % s3}`);
766 (MATCH_MP_TAC AFF_GE_2_2);
768 (NEW_GOAL `~(m IN {u0, u1:real^3})`);
771 (ASM_CASES_TAC `m = u0:real^3`);
772 (UNDISCH_TAC `m IN voronoi_list V vl`);
773 (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list;
774 ASSUME `ul = [u0;u1;u2;u3:real^3]`; VORONOI_LIST; VORONOI_SET]);
776 (NEW_GOAL `m:real^3 IN voronoi_closed V u1`);
777 (UP_ASM_TAC THEN SET_TAC[]);
778 (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
780 (NEW_GOAL `dist (u0, u1:real^3) <= dist (u0, u0)`);
781 (FIRST_ASSUM MATCH_MP_TAC);
782 (NEW_GOAL `{u0, u1, u2, u3:real^3} SUBSET V`);
783 (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`);
784 (ASM_REWRITE_TAC[set_of_list]);
785 (MATCH_MP_TAC Packing3.BARV_SUBSET);
786 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
787 (ONCE_REWRITE_TAC[MESON[IN] `V u0 <=> u0 IN V`]);
788 (UP_ASM_TAC THEN SET_TAC[]);
789 (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]);
791 (NEW_GOAL `dist (u0, u1:real^3) = &0`);
792 (NEW_GOAL `&0 <= dist (u0, u1:real^3)`);
793 (REWRITE_TAC[DIST_POS_LE]);
794 (ASM_REAL_ARITH_TAC);
795 (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]);
798 (ASM_CASES_TAC `m = u1:real^3`);
799 (UNDISCH_TAC `m IN voronoi_list V vl`);
800 (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list;
801 ASSUME `ul = [u0;u1;u2;u3:real^3]`; VORONOI_LIST; VORONOI_SET]);
803 (NEW_GOAL `m:real^3 IN voronoi_closed V u0`);
804 (UP_ASM_TAC THEN SET_TAC[]);
805 (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
807 (NEW_GOAL `dist (u1, u0:real^3) <= dist (u1, u1)`);
808 (FIRST_ASSUM MATCH_MP_TAC);
809 (NEW_GOAL `{u0, u1, u2, u3:real^3} SUBSET V`);
810 (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`);
811 (ASM_REWRITE_TAC[set_of_list]);
812 (MATCH_MP_TAC Packing3.BARV_SUBSET);
813 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
814 (ONCE_REWRITE_TAC[MESON[IN] `V u0 <=> u0 IN V`]);
815 (UP_ASM_TAC THEN SET_TAC[]);
816 (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]);
818 (NEW_GOAL `dist (u1, u0:real^3) = &0`);
819 (NEW_GOAL `&0 <= dist (u1, u0:real^3)`);
820 (REWRITE_TAC[DIST_POS_LE]);
821 (ASM_REAL_ARITH_TAC);
822 (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]);
827 (NEW_GOAL `~(s3 IN {u0, u1:real^3})`);
830 (ASM_CASES_TAC `s3 = u0:real^3`);
831 (UNDISCH_TAC `s3 IN voronoi_list V vl`);
832 (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list;
833 ASSUME `ul = [u0;u1;u2;u3:real^3]`; VORONOI_LIST; VORONOI_SET]);
835 (NEW_GOAL `s3:real^3 IN voronoi_closed V u1`);
836 (UP_ASM_TAC THEN SET_TAC[]);
837 (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
839 (NEW_GOAL `dist (u0, u1:real^3) <= dist (u0, u0)`);
840 (FIRST_ASSUM MATCH_MP_TAC);
841 (NEW_GOAL `{u0, u1, u2, u3:real^3} SUBSET V`);
842 (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`);
843 (ASM_REWRITE_TAC[set_of_list]);
844 (MATCH_MP_TAC Packing3.BARV_SUBSET);
845 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
846 (ONCE_REWRITE_TAC[MESON[IN] `V u0 <=> u0 IN V`]);
847 (UP_ASM_TAC THEN SET_TAC[]);
848 (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]);
850 (NEW_GOAL `dist (u0, u1:real^3) = &0`);
851 (NEW_GOAL `&0 <= dist (u0, u1:real^3)`);
852 (REWRITE_TAC[DIST_POS_LE]);
853 (ASM_REAL_ARITH_TAC);
854 (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]);
857 (ASM_CASES_TAC `s3 = u1:real^3`);
858 (UNDISCH_TAC `s3 IN voronoi_list V vl`);
859 (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list;
860 ASSUME `ul = [u0;u1;u2;u3:real^3]`; VORONOI_LIST; VORONOI_SET]);
862 (NEW_GOAL `s3:real^3 IN voronoi_closed V u0`);
863 (UP_ASM_TAC THEN SET_TAC[]);
864 (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
866 (NEW_GOAL `dist (u1, u0:real^3) <= dist (u1, u1)`);
867 (FIRST_ASSUM MATCH_MP_TAC);
868 (NEW_GOAL `{u0, u1, u2, u3:real^3} SUBSET V`);
869 (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`);
870 (ASM_REWRITE_TAC[set_of_list]);
871 (MATCH_MP_TAC Packing3.BARV_SUBSET);
872 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
873 (ONCE_REWRITE_TAC[MESON[IN] `V u0 <=> u0 IN V`]);
874 (UP_ASM_TAC THEN SET_TAC[]);
875 (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]);
877 (NEW_GOAL `dist (u1, u0:real^3) = &0`);
878 (NEW_GOAL `&0 <= dist (u1, u0:real^3)`);
879 (REWRITE_TAC[DIST_POS_LE]);
880 (ASM_REAL_ARITH_TAC);
881 (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]);
885 (REWRITE_TAC[DISJOINT]);
888 (* ======================================================================== *)
891 (REWRITE_TAC[IN; IN_ELIM_THM]);
893 (NEW_GOAL `&0 <= t1 /\ &0 <= t2`);
895 (ASM_CASES_TAC `&0 < t3 + t4`);
896 (ABBREV_TAC `t5 = t3 + t4:real`);
897 (ABBREV_TAC `z = t3 / t5 % m + t4 / t5 % (s3:real^3)`);
898 (NEW_GOAL `between z (m, s3:real^3)`);
899 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
900 (EXISTS_TAC `t3 / t5` THEN EXISTS_TAC `t4 / t5`);
901 (ASM_SIMP_TAC[REAL_LE_DIV; REAL_ARITH `&0 < a ==> &0 <= a`]);
902 (ASM_REWRITE_TAC[REAL_ARITH `a/b+c/b = (a+c)/b`]);
903 (MATCH_MP_TAC REAL_DIV_REFL THEN ASM_REAL_ARITH_TAC);
905 (NEW_GOAL `z IN voronoi_list V vl`);
906 (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
907 (EXISTS_TAC `convex hull {m, s3:real^3}`);
909 (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
910 (REWRITE_WITH `convex hull {m, s3:real^3} SUBSET voronoi_list V vl <=>
911 convex hull {m, s3} SUBSET (convex hull (voronoi_list V vl))`);
912 (REWRITE_WITH `convex hull (voronoi_list V vl) = voronoi_list V vl`);
913 (REWRITE_TAC[CONVEX_HULL_EQ]);
914 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
915 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
918 (* ------------------------------------------------------------------------ *)
920 (ASM_CASES_TAC `t1 < &0`);
922 (UNDISCH_TAC `x:real^3 IN rcone_ge u1 u0 a`);
923 (REWRITE_TAC[rcone_ge;rconesgn; IN; IN_ELIM_THM]);
924 (REWRITE_TAC[REAL_ARITH `~(a >= b) <=> a < b`]);
925 (NEW_GOAL `x = t1 % u0 + t2 % u1 + t5 % (z:real^3)`);
926 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "z" THEN EXPAND_TAC "t5");
927 (REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]);
928 (REWRITE_TAC[REAL_ARITH `a * b / a = b * (a / a)`]);
929 (ASM_SIMP_TAC[REAL_DIV_REFL; REAL_ARITH `&0 < y ==> ~(y = &0)`;
932 (REWRITE_WITH `x - u1:real^3 = t1 % (u0 - u1) + t5 % (z - u1)`);
933 (REWRITE_WITH `x - u1:real^3 = x - (t1 + t2 + t5) % u1`);
934 (REWRITE_WITH `t1 + t2 + t5 = &1`);
935 (ASM_REAL_ARITH_TAC);
937 (REWRITE_TAC[ASSUME `x = t1 % u0 + t2 % u1 + t5 % z:real^3`]);
940 (REWRITE_TAC[DOT_LADD; DOT_LMUL; GSYM NORM_POW_2]);
941 (NEW_GOAL `(z - u1) dot (u0 - u1:real^3) <=
942 norm (z - u1:real^3) * norm (u0 - u1) * a`);
944 (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`);
945 (NEW_GOAL `m = s2:real^3`);
946 (EXPAND_TAC "m" THEN REWRITE_TAC[mxi] THEN COND_CASES_TAC);
952 (NEW_GOAL `u0 - u1 = &2 % (u0 - s1:real^3)`);
953 (REWRITE_TAC[ASSUME `s1 = circumcenter {u0, u1:real^3}`; CIRCUMCENTER_2;
954 midpoint; VECTOR_ARITH `u0 - inv (&2) % (u0 + u1) = inv (&2) % (u0 - u1)`]);
957 (NEW_GOAL `(z - s1) dot (u0 - s1:real^3) = &0`);
959 (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
960 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
961 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
962 (MATCH_MP_TAC Rogers.MHFTTZN4);
963 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
966 (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
967 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
968 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
969 (EXISTS_TAC `voronoi_list V vl`);
970 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
971 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
972 (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
973 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
974 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
975 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
978 (NEW_GOAL `norm (s2 - u1) <= norm (z - u1:real^3)`);
979 (REWRITE_WITH `norm (s2 - u1) <= norm (z - u1:real^3) <=>
980 norm (s2 - u1) pow 2 <= norm (z - u1:real^3) pow 2`);
981 (ASM_SIMP_TAC[Collect_geom.POW2_COND; NORM_POS_LE]);
982 (REWRITE_WITH `s2 - u1 = (s2 - s1) + (s1 - u1:real^3) /\
983 z - u1 = (z - s1) + (s1 - u1:real^3)`);
985 (REWRITE_WITH `norm (s2 - s1 + s1 - u1) pow 2 =
986 norm (s2 - s1) pow 2 + norm (s1 - u1:real^3) pow 2`);
987 (NEW_GOAL `(s2 - s1) dot (s1 - u1:real^3) = &0`);
988 (REWRITE_WITH `s1 - u1 = u0 - s1:real^3`);
989 (ASM_REWRITE_TAC[CIRCUMCENTER_2; midpoint] THEN VECTOR_ARITH_TAC);
991 (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
992 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
993 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
994 (MATCH_MP_TAC Rogers.MHFTTZN4);
995 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
998 (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
999 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1000 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1001 (EXISTS_TAC `voronoi_list V vl`);
1002 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1003 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1004 (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
1005 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1006 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1007 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1009 (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
1011 (REWRITE_WITH `norm (z - s1 + s1 - u1:real^3) pow 2 =
1012 norm (z - s1) pow 2 + norm (s1 - u1) pow 2`);
1013 (NEW_GOAL `(z - s1) dot (s1 - u1:real^3) = &0`);
1014 (REWRITE_WITH `s1 - u1 = u0 - s1:real^3`);
1015 (ASM_REWRITE_TAC[CIRCUMCENTER_2; midpoint] THEN VECTOR_ARITH_TAC);
1016 (ASM_REWRITE_TAC[]);
1017 (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
1018 (REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`]);
1019 (REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)] THEN
1020 REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `2 = SUC 1`]);
1021 (REWRITE_TAC[ARITH_RULE `SUC 1 = 2`]);
1022 (REWRITE_TAC[GSYM dist; DIST_SYM]);
1023 (ASM_REWRITE_TAC[]);
1024 (REWRITE_WITH `!a b c d:real^3.
1025 dist (a, b:real^3) pow 2 <= dist (c,d) pow 2 <=> dist (a,b) <= dist (c,d)`);
1026 (REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]);
1027 (SIMP_TAC[Collect_geom.POW2_COND; DIST_POS_LE]);
1028 (MATCH_MP_TAC CLOSEST_POINT_LE);
1029 (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);
1030 (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
1031 (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`);
1033 (NEW_GOAL `s2:real^3 IN voronoi_list V zl`);
1034 (EXPAND_TAC "zl" THEN REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)]);
1035 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
1036 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1037 (NEW_GOAL `s3:real^3 IN voronoi_list V zl`);
1038 (EXPAND_TAC "zl" THEN EXPAND_TAC "s3");
1039 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
1040 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1041 (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
1042 (EXISTS_TAC `convex hull {s2, s3:real^3}`);
1044 (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
1046 (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V zl <=>
1047 convex hull {s2, s3} SUBSET (convex hull (voronoi_list V zl))`);
1048 (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
1049 (REWRITE_TAC[CONVEX_HULL_EQ]);
1050 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
1051 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
1054 (REWRITE_WITH `(z - u1) dot (u0 - u1:real^3) = &2 * norm (u0 - s1) pow 2`);
1055 (REWRITE_WITH `(z - u1) dot (u0 - u1) = (z - s1) dot (u0 - u1) +
1056 (s1 - u1) dot (u0 - u1:real^3)`);
1058 (REWRITE_TAC[ASSUME `u0 - u1 = &2 % (u0 - s1:real^3)`; DOT_RMUL]);
1059 (REWRITE_WITH `(s1 - u1) = (u0 - s1:real^3)`);
1060 (ASM_REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN VECTOR_ARITH_TAC);
1061 (ASM_REWRITE_TAC[NORM_POW_2] THEN REAL_ARITH_TAC);
1064 (NEW_GOAL `&2 * norm (u0 - s1:real^3) pow 2 <=
1065 norm (s2 - u1) * norm (u0 - u1) * a`);
1066 (NEW_GOAL `norm (s2 - u1:real^3) >= sqrt (&2)`);
1067 (NEW_GOAL `norm (s2 - u1:real^3) >=
1068 hl (truncate_simplex 2 (ul:(real^3)list))`);
1069 (REWRITE_TAC[GSYM dist]);
1070 (NEW_GOAL `?p. p permutes 0..1 /\
1071 [u1; u0; u2; u3:real^3] = left_action_list p ul`);
1072 (MATCH_MP_TAC TWO_REARRANGEMENT_LEMMA);
1073 (EXISTS_TAC `V:real^3->bool`);
1074 (ASM_REWRITE_TAC[]);
1075 (UP_ASM_TAC THEN STRIP_TAC);
1076 (ABBREV_TAC `ul' = [u1;u0;u2;u3:real^3]`);
1077 (NEW_GOAL `barV V 3 ul' /\
1078 (!j. 1 <= j /\ j <= 3
1079 ==> omega_list_n V ul' j = omega_list_n V ul j)`);
1080 (ONCE_REWRITE_TAC[ARITH_RULE `1 = 2 - 1`]);
1081 (MATCH_MP_TAC YNHYJIT);
1082 (EXISTS_TAC `p:num->num` THEN REWRITE_TAC[ARITH_RULE `2 - 1 = 1`;
1083 SET_RULE `2 IN {2,3,4}`]);
1084 (ASM_REWRITE_TAC[]);
1085 (UP_ASM_TAC THEN STRIP_TAC);
1086 (REWRITE_WITH `s2 = omega_list_n V ul' 2 /\ u1 = HD ul'`);
1088 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
1089 (REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)] );
1090 (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
1091 (REWRITE_TAC[GSYM (ASSUME `[u1; u0; u2; u3:real^3] = ul'`); HD] );
1092 (REWRITE_TAC[REAL_ARITH `a >= b <=> b <= a`]);
1093 (ABBREV_TAC `xl:(real^3)list = truncate_simplex 2 ul'`);
1094 (REWRITE_WITH `hl (truncate_simplex 2 (ul:(real^3)list)) =
1095 hl (xl:(real^3)list)`);
1097 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1098 GSYM (ASSUME `[u1;u0;u2;u3:real^3] = ul'`); TRUNCATE_SIMPLEX_EXPLICIT_2]);
1099 (REWRITE_TAC[HL; set_of_list; SET_RULE `{u0, u1, u2} = {u1,u0,u2}`]);
1100 (REWRITE_WITH `omega_list_n V ul' 2 = omega_list V xl`);
1101 (REWRITE_WITH `omega_list V xl = omega_list_n V xl 2`);
1102 (REWRITE_TAC[OMEGA_LIST]);
1103 (EXPAND_TAC "xl" THEN REWRITE_TAC[GSYM
1104 (ASSUME `[u1; u0; u2; u3:real^3] = ul'`); TRUNCATE_SIMPLEX_EXPLICIT_2]);
1105 (REWRITE_TAC[LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`]);
1108 `truncate_simplex 2 (ul':(real^3)list) = truncate_simplex (2 + 0) ul'`);
1109 (REWRITE_TAC[ARITH_RULE `2 + 0 = 2`]);
1110 (MATCH_MP_TAC Packing3.OMEGA_LIST_N_LEMMA);
1111 (REWRITE_TAC[GSYM (ASSUME `[u1; u0; u2; u3:real^3] = ul'`); LENGTH]);
1113 (REWRITE_WITH `HD ul' = HD (xl:(real^3)list)`);
1114 (ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN EXPAND_TAC "xl");
1115 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
1116 (REWRITE_TAC[GSYM (ASSUME `[u1; u0; u2; u3:real^3] = ul'`); LENGTH]);
1118 (MATCH_MP_TAC Rogers.WAUFCHE1);
1120 (REWRITE_TAC[IN] THEN EXPAND_TAC "xl");
1122 (ASM_REWRITE_TAC[]);
1123 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1124 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1125 (ASM_REAL_ARITH_TAC);
1128 (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u0:real^3)`);
1129 (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
1130 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1131 TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
1132 (ASM_REWRITE_TAC[]);
1134 (REWRITE_WITH `u0:real^3 = HD vl`);
1135 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1136 TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list; HD]);
1137 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
1138 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
1140 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1141 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1142 (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]);
1143 (REWRITE_TAC[ASSUME `u0 - u1 = &2 % (u0 - s1:real^3)`; NORM_MUL]);
1144 (REWRITE_WITH `abs (&2) = &2`);
1145 (REWRITE_TAC[REAL_ABS_REFL; REAL_ARITH `&0 <= &2`]);
1146 (REWRITE_TAC[REAL_ARITH `a * (&2 * b) * b / c = (&2 * b pow 2) * ( a / c)`]);
1147 (REWRITE_TAC[REAL_ARITH `a <= a * b <=> &0 <= a * (b - &1)`]);
1148 (MATCH_MP_TAC REAL_LE_MUL);
1149 (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_POW_2; REAL_ARITH `&0 <= &2`]);
1150 (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
1151 (REWRITE_WITH `&1 <= norm (s2 - u1) / sqrt (&2) <=>
1152 &1 * sqrt (&2) <= norm (s2 - u1:real^3)`);
1153 (MATCH_MP_TAC REAL_LE_RDIV_EQ);
1154 (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);
1155 (ASM_REAL_ARITH_TAC);
1156 (NEW_GOAL `norm (s2 - u1) * norm (u0 - u1:real^3) * a <=
1157 norm (z - u1) * norm (u0 - u1) * a`);
1158 (REWRITE_TAC[REAL_ARITH `a * x * y <= b * x * y <=>
1159 &0 <= (x * y) * (b - a)`]);
1160 (MATCH_MP_TAC REAL_LE_MUL);
1162 (MATCH_MP_TAC REAL_LE_MUL);
1163 (REWRITE_TAC[NORM_POS_LE]);
1164 (EXPAND_TAC "a" THEN MATCH_MP_TAC REAL_LE_DIV);
1165 (REWRITE_WITH `hl vl = dist (circumcenter (set_of_list vl),(HD vl):real^3)`);
1166 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
1167 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
1169 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1170 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1171 (REWRITE_TAC[DIST_POS_LE]);
1172 (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
1173 (ASM_REAL_ARITH_TAC);
1174 (ASM_REAL_ARITH_TAC);
1176 (* ------------------------------------------------------------------------- *)
1179 (* ----------------------------------------------------- *)
1181 (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
1182 dist (u0,s) = sqrt (&2) /\
1184 (MATCH_MP_TAC MXI_EXPLICIT);
1185 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
1186 (REWRITE_TAC[REAL_ARITH `a < b <=> ~(a >= b)`]);
1187 (ASM_REWRITE_TAC[]);
1188 (FIRST_X_ASSUM CHOOSE_TAC);
1189 (UP_ASM_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN STRIP_TAC);
1191 (NEW_GOAL `u0 - u1 = &2 % (u0 - s1:real^3)`);
1192 (REWRITE_TAC[ASSUME `s1 = circumcenter {u0, u1:real^3}`; CIRCUMCENTER_2;
1193 midpoint; VECTOR_ARITH `u0 - inv (&2) % (u0 + u1) = inv (&2) % (u0 - u1)`]);
1196 (NEW_GOAL `(z - s1) dot (u0 - s1:real^3) = &0`);
1197 (ASM_REWRITE_TAC[]);
1198 (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
1199 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1200 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1201 (MATCH_MP_TAC Rogers.MHFTTZN4);
1202 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
1204 (ASM_REWRITE_TAC[]);
1205 (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1206 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1207 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1208 (EXISTS_TAC `voronoi_list V vl`);
1209 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1210 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1211 (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
1212 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1213 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1214 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1217 (NEW_GOAL `between m (s2, z:real^3)`);
1218 (MATCH_MP_TAC BETWEEN_TRANS_2);
1219 (EXISTS_TAC `s3:real^3`);
1221 (ONCE_REWRITE_TAC[BETWEEN_SYM]);
1222 (ASM_REWRITE_TAC[]);
1223 (ASM_REWRITE_TAC[]);
1224 (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`);
1226 (NEW_GOAL `s2:real^3 IN voronoi_list V zl`);
1227 (EXPAND_TAC "s2" THEN EXPAND_TAC "zl");
1228 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
1229 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1231 (NEW_GOAL `s3:real^3 IN voronoi_list V zl`);
1232 (EXPAND_TAC "s3" THEN EXPAND_TAC "zl");
1233 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
1234 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1236 (NEW_GOAL `m:real^3 IN voronoi_list V zl`);
1237 (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
1238 (EXISTS_TAC `convex hull {s2, s3:real^3}`);
1240 (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
1241 (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V zl <=>
1242 convex hull {s2, s3} SUBSET (convex hull (voronoi_list V zl))`);
1243 (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
1244 (REWRITE_TAC[CONVEX_HULL_EQ]);
1245 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
1246 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
1249 (NEW_GOAL `z:real^3 IN voronoi_list V zl`);
1250 (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
1251 (EXISTS_TAC `convex hull {m, s3:real^3}`);
1253 (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
1254 (REWRITE_WITH `convex hull {m, s3:real^3} SUBSET voronoi_list V zl <=>
1255 convex hull {m, s3} SUBSET (convex hull (voronoi_list V zl))`);
1256 (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
1257 (REWRITE_TAC[CONVEX_HULL_EQ]);
1258 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
1259 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
1262 (NEW_GOAL `norm (m - u1) <= norm (z - u1:real^3)`);
1263 (REWRITE_WITH `norm (m - u1) <= norm (z - u1:real^3) <=>
1264 norm (m - u1) pow 2 <= norm (z - u1:real^3) pow 2`);
1265 (ASM_SIMP_TAC[Collect_geom.POW2_COND; NORM_POS_LE]);
1266 (REWRITE_WITH `m - u1 = (m - s2) + (s2 - u1:real^3) /\
1267 z - u1 = (z - s2) + (s2 - u1:real^3)`);
1269 (REWRITE_WITH `norm (m - s2 + s2 - u1) pow 2 =
1270 norm (m - s2) pow 2 + norm (s2 - u1:real^3) pow 2`);
1271 (NEW_GOAL `(m - s2) dot (s2 - u1:real^3) = &0`);
1272 (ONCE_REWRITE_TAC[VECTOR_ARITH
1273 `(m - s2) dot (s2 - u1) = -- ((m - s2) dot (u1 - s2))`]);
1274 (REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]);
1275 (REWRITE_WITH `s2:real^3 = circumcenter (set_of_list zl)`);
1276 (REWRITE_WITH `s2:real^3 = omega_list V zl`);
1279 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`;
1280 Marchal_cells.OMEGA_LIST_TRUNCATE_2]);
1281 (MATCH_MP_TAC Rogers.XNHPWAB1);
1283 (REWRITE_TAC[IN; REAL_ARITH `a < b <=> ~(a >= b)`]);
1284 (ASM_REWRITE_TAC[]);
1285 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1286 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1287 (MATCH_MP_TAC Rogers.MHFTTZN4);
1288 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
1290 (ASM_REWRITE_TAC[]);
1291 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1292 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1293 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1294 (EXISTS_TAC `voronoi_list V zl`);
1295 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1296 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1297 (EXISTS_TAC `set_of_list (zl:(real^3)list)`);
1298 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1299 (EXPAND_TAC "zl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2;
1300 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1302 (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
1305 `norm (z - s2 + s2 - u1) pow 2 =
1306 norm (z - s2) pow 2 + norm (s2 - u1:real^3) pow 2`);
1307 (NEW_GOAL `(z - s2) dot (s2 - u1:real^3) = &0`);
1308 (ONCE_REWRITE_TAC[VECTOR_ARITH
1309 `(z - s2) dot (s2 - u1) = -- ((z - s2) dot (u1 - s2))`]);
1310 (REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]);
1311 (REWRITE_WITH `s2:real^3 = circumcenter (set_of_list zl)`);
1312 (REWRITE_WITH `s2:real^3 = omega_list V zl`);
1315 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`;
1316 Marchal_cells.OMEGA_LIST_TRUNCATE_2]);
1317 (MATCH_MP_TAC Rogers.XNHPWAB1);
1319 (REWRITE_TAC[IN; REAL_ARITH `a < b <=> ~(a >= b)`]);
1320 (ASM_REWRITE_TAC[]);
1321 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1322 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1323 (MATCH_MP_TAC Rogers.MHFTTZN4);
1324 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
1326 (ASM_REWRITE_TAC[]);
1327 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1328 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1329 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1330 (EXISTS_TAC `voronoi_list V zl`);
1331 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1332 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1333 (EXISTS_TAC `set_of_list (zl:(real^3)list)`);
1334 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1335 (EXPAND_TAC "zl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2;
1336 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1338 (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
1339 (REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`]);
1341 (MP_TAC (ASSUME `between m (s2,z:real^3)`));
1342 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN;IN_ELIM_THM] THEN STRIP_TAC);
1343 (REWRITE_TAC[ASSUME `m = u % s2 + v % z:real^3`]);
1345 `(u % s2 + v % z) - s2 = (u % s2 + v % z) - (u + v) % s2:real^3`);
1346 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
1347 (REWRITE_TAC[VECTOR_ARITH `(u % s2 + v % z) - (u + v) % s2 = v % (z - s2)`]);
1348 (REWRITE_TAC[NORM_MUL; REAL_ARITH `(a*b) pow 2 = a pow 2 * b pow 2`;
1349 REAL_ARITH `a * b <= b <=> &0 <= b * (&1 - a)`]);
1350 (MATCH_MP_TAC REAL_LE_MUL);
1351 (REWRITE_TAC[REAL_LE_POW_2]);
1352 (REWRITE_WITH `abs (v:real) = v`);
1353 (ASM_REWRITE_TAC[REAL_ABS_REFL]);
1354 (REWRITE_TAC[REAL_ARITH `&0 <= &1 - a <=> a <= &1 pow 2`]);
1355 (REWRITE_WITH ` v pow 2 <= &1 pow 2 <=> v <= &1`);
1356 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
1357 (MATCH_MP_TAC Collect_geom.POW2_COND);
1358 (ASM_REAL_ARITH_TAC);
1359 (ASM_REAL_ARITH_TAC);
1361 (NEW_GOAL `norm (m - u1:real^3) = dist (u0, s:real^3)`);
1362 (ONCE_REWRITE_TAC[DIST_SYM]);
1363 (ASM_REWRITE_TAC[GSYM dist]);
1364 (UNDISCH_TAC `m IN voronoi_list V zl`);
1365 (ASM_REWRITE_TAC[VORONOI_LIST; VORONOI_SET]);
1367 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);
1369 (NEW_GOAL `s:real^3 IN voronoi_closed V u0 /\ s IN voronoi_closed V u1`);
1370 (UP_ASM_TAC THEN SET_TAC[]);
1371 (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
1373 (NEW_GOAL `{u0,u1,u2,u3:real^3} SUBSET V`);
1374 (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list ul`);
1375 (ASM_REWRITE_TAC[set_of_list]);
1376 (MATCH_MP_TAC Packing3.BARV_SUBSET);
1377 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
1380 (NEW_GOAL `dist (s,u0) <= dist (s,u1:real^3)`);
1381 (FIRST_ASSUM MATCH_MP_TAC);
1382 (ONCE_REWRITE_TAC[MESON[IN] `V s <=> s IN V`]);
1384 (NEW_GOAL `dist (s,u1) <= dist (s,u0:real^3)`);
1385 (FIRST_ASSUM MATCH_MP_TAC);
1386 (ONCE_REWRITE_TAC[MESON[IN] `V s <=> s IN V`]);
1388 (ASM_REAL_ARITH_TAC);
1390 (NEW_GOAL `norm (m - u1:real^3) = sqrt (&2)`);
1391 (ASM_REAL_ARITH_TAC);
1393 (REWRITE_WITH `(z - u1) dot (u0 - u1:real^3) = &2 * norm (u0 - s1) pow 2`);
1394 (REWRITE_WITH `(z - u1) dot (u0 - u1) = (z - s1) dot (u0 - u1) +
1395 (s1 - u1) dot (u0 - u1:real^3)`);
1397 (REWRITE_TAC[ASSUME `u0 - u1 = &2 % (u0 - s1:real^3)`; DOT_RMUL]);
1398 (REWRITE_WITH `(s1 - u1) = (u0 - s1:real^3)`);
1399 (ASM_REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN VECTOR_ARITH_TAC);
1400 (ASM_REWRITE_TAC[NORM_POW_2] THEN REAL_ARITH_TAC);
1402 (NEW_GOAL `&2 * norm (u0 - s1:real^3) pow 2 <=
1403 norm (m - u1) * norm (u0 - u1) * a`);
1405 (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u0:real^3)`);
1406 (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
1407 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1408 TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
1409 (ASM_REWRITE_TAC[]);
1411 (REWRITE_WITH `u0:real^3 = HD vl`);
1412 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1413 TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list; HD]);
1414 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
1415 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
1417 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1418 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1419 (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]);
1420 (REWRITE_TAC[ASSUME `u0 - u1 = &2 % (u0 - s1:real^3)`; NORM_MUL]);
1421 (REWRITE_WITH `abs (&2) = &2`);
1422 (REWRITE_TAC[REAL_ABS_REFL; REAL_ARITH `&0 <= &2`]);
1423 (REWRITE_TAC[REAL_ARITH `a * (&2 * b) * b / c = (&2 * b pow 2) * ( a / c)`]);
1424 (REWRITE_TAC[REAL_ARITH `a <= a * b <=> &0 <= a * (b - &1)`]);
1425 (MATCH_MP_TAC REAL_LE_MUL);
1426 (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_POW_2; REAL_ARITH `&0 <= &2`]);
1427 (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
1428 (REWRITE_WITH `sqrt (&2) / sqrt (&2) = &1`);
1429 (MATCH_MP_TAC REAL_DIV_REFL);
1430 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
1431 (SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]);
1434 (NEW_GOAL `norm (m - u1) * norm (u0 - u1:real^3) * a <=
1435 norm (z - u1) * norm (u0 - u1) * a`);
1436 (REWRITE_TAC[REAL_ARITH `a * x * y <= b * x * y <=>
1437 &0 <= (x * y) * (b - a)`]);
1438 (MATCH_MP_TAC REAL_LE_MUL);
1440 (MATCH_MP_TAC REAL_LE_MUL);
1441 (REWRITE_TAC[NORM_POS_LE]);
1442 (EXPAND_TAC "a" THEN MATCH_MP_TAC REAL_LE_DIV);
1443 (REWRITE_WITH `hl vl = dist (circumcenter (set_of_list vl),(HD vl):real^3)`);
1444 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
1445 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
1447 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1448 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1449 (REWRITE_TAC[DIST_POS_LE]);
1450 (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
1451 (ASM_REAL_ARITH_TAC);
1452 (ASM_REAL_ARITH_TAC);
1454 (NEW_GOAL `t1 * norm (u0 - u1:real^3) pow 2 + t5 * ((z - u1) dot (u0 - u1))
1455 <= t1 * norm (u0 - u1) pow 2 + t5 * (norm (z - u1) * norm (u0 - u1) * a)`);
1456 (REWRITE_TAC[REAL_ARITH `a + b * c <= a + b * d <=> &0 <= b * (d - c)`]);
1457 (MATCH_MP_TAC REAL_LE_MUL);
1458 (ASM_REAL_ARITH_TAC);
1461 `t1 * norm (u0 - u1) pow 2 + t5 * norm (z - u1:real^3) * norm (u0 - u1) * a
1462 < norm (t1 % (u0 - u1) + t5 % (z - u1)) * norm (u0 - u1) * a`);
1464 (REWRITE_TAC[REAL_ARITH
1465 `t1 * norm (u0 - u1) pow 2 + t5 * norm (z - u1:real^3) * norm (u0 - u1) * a
1466 < norm (t1 % (u0 - u1) + t5 % (z - u1)) * norm (u0 - u1) * a <=>
1467 &0 < (a * norm (t1 % (u0 - u1) + t5 % (z - u1)) - t1 * norm (u0 - u1) -
1468 t5 * a * norm (z - u1)) * norm (u0 - u1)`]);
1469 (MATCH_MP_TAC REAL_LT_MUL);
1471 (REWRITE_TAC[REAL_ARITH `&0 < a - b - c <=> b + c < a`]);
1473 (NEW_GOAL `t1 * norm (u0 - u1) < a * t1 * norm (u0 - u1:real^3)`);
1474 (REWRITE_TAC[REAL_ARITH `a * b < c * a * b <=> &0 < (--a) * b * (&1 - c)`]);
1475 (MATCH_MP_TAC REAL_LT_MUL);
1477 (ASM_REAL_ARITH_TAC);
1478 (MATCH_MP_TAC REAL_LT_MUL);
1480 (REWRITE_TAC[NORM_POS_LT; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
1481 (ASM_REWRITE_TAC[]);
1482 (REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`] THEN EXPAND_TAC "a");
1483 (REWRITE_WITH `hl (vl:(real^3)list) / sqrt (&2) < &1 <=> hl vl < &1 * sqrt (&2) `);
1484 (MATCH_MP_TAC REAL_LT_LDIV_EQ);
1485 (MATCH_MP_TAC SQRT_POS_LT);
1487 (ASM_REWRITE_TAC[REAL_MUL_LID]);
1489 (NEW_GOAL `a * t1 * norm (u0 - u1) + t5 * a * norm (z - u1) <=
1490 a * norm (t1 % (u0 - u1) + t5 % (z - u1:real^3))`);
1491 (REWRITE_TAC[REAL_ARITH
1492 `a * t1 * norm (u0 - u1) + t5 * a * norm (z - u1) <=
1493 a * norm (t1 % (u0 - u1) + t5 % (z - u1)) <=>
1494 &0 <= a * (norm (t1 % (u0 - u1) + t5 % (z - u1)) + (--t1 * norm (u0 - u1)) - t5 * norm (z - u1))`]);
1495 (MATCH_MP_TAC REAL_LE_MUL);
1498 (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u0:real^3)`);
1499 (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
1500 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1501 TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
1502 (ASM_REWRITE_TAC[]);
1504 (REWRITE_WITH `u0:real^3 = HD vl`);
1505 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1506 TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list; HD]);
1507 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
1508 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
1510 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1511 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1512 (MATCH_MP_TAC REAL_LE_DIV);
1513 (REWRITE_TAC[DIST_POS_LE]);
1514 (ASM_SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
1516 (ONCE_REWRITE_TAC[REAL_ARITH `&0 <= a + b - c <=> c <= a + b`]);
1517 (ABBREV_TAC `k1 = t1 % (u0 - u1) + t5 % (z - u1:real^3)`);
1518 (REWRITE_WITH `t5 * norm (z - u1) = norm (t5 % (z - u1:real^3))`);
1519 (REWRITE_TAC[NORM_MUL]);
1520 (REWRITE_WITH `abs t5 = t5`);
1521 (REWRITE_TAC[REAL_ABS_REFL]);
1522 (ASM_REAL_ARITH_TAC);
1523 (REWRITE_WITH `--t1 * norm (u0 - u1) = norm ((--t1) % (u0 - u1:real^3))`);
1524 (REWRITE_TAC[NORM_MUL]);
1525 (REWRITE_WITH `abs (--t1) = --t1`);
1526 (REWRITE_TAC[REAL_ABS_REFL]);
1527 (ASM_REAL_ARITH_TAC);
1528 (REWRITE_WITH `t5 % (z - u1) = k1 + --t1 % (u0 - u1:real^3)`);
1529 (EXPAND_TAC "k1" THEN VECTOR_ARITH_TAC);
1530 (REWRITE_TAC[NORM_TRIANGLE]);
1531 (ASM_REAL_ARITH_TAC);
1532 (REWRITE_TAC[NORM_POS_LT; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
1533 (ASM_REWRITE_TAC[]);
1534 (ASM_REAL_ARITH_TAC);
1537 (* ----------------------------------------------------------------------- *)
1538 (* Half of the proof *)
1541 (ASM_CASES_TAC `t2 < &0`);
1543 (UNDISCH_TAC `x:real^3 IN rcone_ge u0 u1 a`);
1544 (REWRITE_TAC[rcone_ge;rconesgn; IN; IN_ELIM_THM]);
1545 (REWRITE_TAC[REAL_ARITH `~(a >= b) <=> a < b`]);
1546 (NEW_GOAL `x = t1 % u0 + t2 % u1 + t5 % (z:real^3)`);
1547 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "z" THEN EXPAND_TAC "t5");
1548 (REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]);
1549 (REWRITE_TAC[REAL_ARITH `a * b / a = b * (a / a)`]);
1550 (ASM_SIMP_TAC[REAL_DIV_REFL; REAL_ARITH `&0 < y ==> ~(y = &0)`;
1552 (REWRITE_TAC[dist]);
1553 (REWRITE_WITH `x - u0:real^3 = t2 % (u1 - u0) + t5 % (z - u0)`);
1554 (REWRITE_WITH `x - u0:real^3 = x - (t1 + t2 + t5) % u0`);
1555 (REWRITE_WITH `t1 + t2 + t5 = &1`);
1556 (ASM_REAL_ARITH_TAC);
1558 (REWRITE_TAC[ASSUME `x = t1 % u0 + t2 % u1 + t5 % z:real^3`]);
1561 (REWRITE_TAC[DOT_LADD; DOT_LMUL; GSYM NORM_POW_2]);
1562 (NEW_GOAL `(z - u0) dot (u1 - u0:real^3) <=
1563 norm (z - u0:real^3) * norm (u1 - u0) * a`);
1565 (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`);
1566 (NEW_GOAL `m = s2:real^3`);
1567 (EXPAND_TAC "m" THEN REWRITE_TAC[mxi] THEN COND_CASES_TAC);
1568 (ASM_REWRITE_TAC[]);
1573 (NEW_GOAL `u1 - u0 = &2 % (u1 - s1:real^3)`);
1574 (REWRITE_TAC[ASSUME `s1 = circumcenter {u0, u1:real^3}`; CIRCUMCENTER_2;
1575 midpoint; VECTOR_ARITH `u1 - inv (&2) % (u0 + u1) = inv (&2) % (u1 - u0)`]);
1578 (NEW_GOAL `(z - s1) dot (u1 - s1:real^3) = &0`);
1579 (ASM_REWRITE_TAC[]);
1580 (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
1581 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1582 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1583 (MATCH_MP_TAC Rogers.MHFTTZN4);
1584 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
1586 (ASM_REWRITE_TAC[]);
1587 (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1588 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1589 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1590 (EXISTS_TAC `voronoi_list V vl`);
1591 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1592 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1593 (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
1594 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1595 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1596 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1599 (NEW_GOAL `norm (s2 - u0) <= norm (z - u0:real^3)`);
1600 (REWRITE_WITH `norm (s2 - u0) <= norm (z - u0:real^3) <=>
1601 norm (s2 - u0) pow 2 <= norm (z - u0:real^3) pow 2`);
1602 (ASM_SIMP_TAC[Collect_geom.POW2_COND; NORM_POS_LE]);
1603 (REWRITE_WITH `s2 - u0 = (s2 - s1) + (s1 - u0:real^3) /\
1604 z - u0 = (z - s1) + (s1 - u0:real^3)`);
1606 (REWRITE_WITH `norm (s2 - s1 + s1 - u0) pow 2 =
1607 norm (s2 - s1) pow 2 + norm (s1 - u0:real^3) pow 2`);
1608 (NEW_GOAL `(s2 - s1) dot (s1 - u0:real^3) = &0`);
1609 (REWRITE_WITH `s1 - u0 = u1 - s1:real^3`);
1610 (ASM_REWRITE_TAC[CIRCUMCENTER_2; midpoint] THEN VECTOR_ARITH_TAC);
1611 (ASM_REWRITE_TAC[]);
1612 (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
1613 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1614 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1615 (MATCH_MP_TAC Rogers.MHFTTZN4);
1616 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
1618 (ASM_REWRITE_TAC[]);
1619 (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1620 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1621 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1622 (EXISTS_TAC `voronoi_list V vl`);
1623 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1624 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1625 (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
1626 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1627 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1628 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1630 (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
1632 (REWRITE_WITH `norm (z - s1 + s1 - u0:real^3) pow 2 =
1633 norm (z - s1) pow 2 + norm (s1 - u0) pow 2`);
1634 (NEW_GOAL `(z - s1) dot (s1 - u0:real^3) = &0`);
1635 (REWRITE_WITH `s1 - u0 = u1 - s1:real^3`);
1636 (ASM_REWRITE_TAC[CIRCUMCENTER_2; midpoint] THEN VECTOR_ARITH_TAC);
1637 (ASM_REWRITE_TAC[]);
1638 (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
1639 (REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`]);
1640 (REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)] THEN
1641 REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `2 = SUC 1`]);
1642 (REWRITE_TAC[ARITH_RULE `SUC 1 = 2`]);
1643 (REWRITE_TAC[GSYM dist; DIST_SYM]);
1644 (ASM_REWRITE_TAC[]);
1645 (REWRITE_WITH `!a b c d:real^3.
1646 dist (a, b:real^3) pow 2 <= dist (c,d) pow 2 <=> dist (a,b) <= dist (c,d)`);
1647 (REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]);
1648 (SIMP_TAC[Collect_geom.POW2_COND; DIST_POS_LE]);
1649 (MATCH_MP_TAC CLOSEST_POINT_LE);
1650 (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);
1651 (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
1652 (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`);
1654 (NEW_GOAL `s2:real^3 IN voronoi_list V zl`);
1655 (EXPAND_TAC "zl" THEN REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)]);
1656 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
1657 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1658 (NEW_GOAL `s3:real^3 IN voronoi_list V zl`);
1659 (EXPAND_TAC "zl" THEN EXPAND_TAC "s3");
1660 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
1661 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1662 (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
1663 (EXISTS_TAC `convex hull {s2, s3:real^3}`);
1665 (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
1667 (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V zl <=>
1668 convex hull {s2, s3} SUBSET (convex hull (voronoi_list V zl))`);
1669 (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
1670 (REWRITE_TAC[CONVEX_HULL_EQ]);
1671 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
1672 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
1675 (REWRITE_WITH `(z - u0) dot (u1 - u0:real^3) = &2 * norm (u1 - s1) pow 2`);
1676 (REWRITE_WITH `(z - u0) dot (u1 - u0) = (z - s1) dot (u1 - u0) +
1677 (s1 - u0) dot (u1 - u0:real^3)`);
1679 (REWRITE_TAC[ASSUME `u1 - u0 = &2 % (u1 - s1:real^3)`; DOT_RMUL]);
1680 (REWRITE_WITH `(s1 - u0) = (u1 - s1:real^3)`);
1681 (ASM_REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN VECTOR_ARITH_TAC);
1682 (ASM_REWRITE_TAC[NORM_POW_2] THEN REAL_ARITH_TAC);
1685 (NEW_GOAL `&2 * norm (u1 - s1:real^3) pow 2 <=
1686 norm (s2 - u0) * norm (u1 - u0) * a`);
1687 (NEW_GOAL `norm (s2 - u0:real^3) >= sqrt (&2)`);
1688 (NEW_GOAL `norm (s2 - u0:real^3) >=
1689 hl (truncate_simplex 2 (ul:(real^3)list))`);
1690 (REWRITE_TAC[GSYM dist]);
1691 (ONCE_REWRITE_TAC[REAL_ARITH `a >= b <=> b <= a`]);
1692 (ABBREV_TAC `xl:(real^3)list = truncate_simplex 2 ul`);
1694 (REWRITE_WITH `s2 = omega_list V xl`);
1695 (ONCE_REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)]);
1696 (REWRITE_TAC[Marchal_cells.OMEGA_LIST_TRUNCATE_2;
1697 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1698 (EXPAND_TAC "xl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;
1699 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1700 (REWRITE_WITH `u0:real^3 = HD xl`);
1702 (REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`;
1703 TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
1704 (MATCH_MP_TAC Rogers.WAUFCHE1);
1706 (REWRITE_TAC[IN] THEN EXPAND_TAC "xl");
1708 (ASM_REWRITE_TAC[]);
1709 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1710 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1711 (ASM_REAL_ARITH_TAC);
1714 (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u1:real^3)`);
1715 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
1716 (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
1717 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1718 TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
1719 (ASM_REWRITE_TAC[]);
1720 (NEW_GOAL `!w:real^3. w IN set_of_list vl
1721 ==> dist (circumcenter (set_of_list vl),w) = hl vl`);
1722 (MATCH_MP_TAC Rogers.HL_PROPERTIES);
1723 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
1724 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
1725 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1726 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1727 (FIRST_ASSUM MATCH_MP_TAC);
1729 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1730 TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
1733 (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]);
1734 (REWRITE_TAC[ASSUME `u1 - u0 = &2 % (u1 - s1:real^3)`; NORM_MUL]);
1735 (REWRITE_WITH `abs (&2) = &2`);
1736 (REWRITE_TAC[REAL_ABS_REFL; REAL_ARITH `&0 <= &2`]);
1737 (REWRITE_TAC[REAL_ARITH `a * (&2 * b) * b / c = (&2 * b pow 2) * ( a / c)`]);
1738 (REWRITE_TAC[REAL_ARITH `a <= a * b <=> &0 <= a * (b - &1)`]);
1739 (MATCH_MP_TAC REAL_LE_MUL);
1740 (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_POW_2; REAL_ARITH `&0 <= &2`]);
1741 (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
1742 (REWRITE_WITH `&1 <= norm (s2 - u0) / sqrt (&2) <=>
1743 &1 * sqrt (&2) <= norm (s2 - u0:real^3)`);
1744 (MATCH_MP_TAC REAL_LE_RDIV_EQ);
1745 (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);
1746 (ASM_REAL_ARITH_TAC);
1747 (NEW_GOAL `norm (s2 - u0) * norm (u1 - u0:real^3) * a <=
1748 norm (z - u0) * norm (u1 - u0) * a`);
1749 (REWRITE_TAC[REAL_ARITH `a * x * y <= b * x * y <=>
1750 &0 <= (x * y) * (b - a)`]);
1751 (MATCH_MP_TAC REAL_LE_MUL);
1753 (MATCH_MP_TAC REAL_LE_MUL);
1754 (REWRITE_TAC[NORM_POS_LE]);
1755 (EXPAND_TAC "a" THEN MATCH_MP_TAC REAL_LE_DIV);
1756 (REWRITE_WITH `hl vl = dist (circumcenter (set_of_list vl),(HD vl):real^3)`);
1757 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
1758 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]);
1760 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1761 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1762 (REWRITE_TAC[DIST_POS_LE]);
1763 (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
1764 (ASM_REAL_ARITH_TAC);
1765 (ASM_REAL_ARITH_TAC);
1767 (* ------------------------------------------------------------------------- *)
1770 (* ----------------------------------------------------- *)
1772 (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
1773 dist (u0,s) = sqrt (&2) /\
1775 (MATCH_MP_TAC MXI_EXPLICIT);
1776 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
1777 (REWRITE_TAC[REAL_ARITH `a < b <=> ~(a >= b)`]);
1778 (ASM_REWRITE_TAC[]);
1779 (FIRST_X_ASSUM CHOOSE_TAC);
1780 (UP_ASM_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN STRIP_TAC);
1782 (NEW_GOAL `u1 - u0 = &2 % (u1 - s1:real^3)`);
1783 (REWRITE_TAC[ASSUME `s1 = circumcenter {u0, u1:real^3}`; CIRCUMCENTER_2;
1784 midpoint; VECTOR_ARITH `u1 - inv (&2) % (u0 + u1) = inv (&2) % (u1 - u0)`]);
1787 (NEW_GOAL `(z - s1) dot (u1 - s1:real^3) = &0`);
1788 (ASM_REWRITE_TAC[]);
1789 (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`);
1790 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1791 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1792 (MATCH_MP_TAC Rogers.MHFTTZN4);
1793 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
1795 (ASM_REWRITE_TAC[]);
1796 (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1797 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1798 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1799 (EXISTS_TAC `voronoi_list V vl`);
1800 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1801 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1802 (EXISTS_TAC `set_of_list (vl:(real^3)list)`);
1803 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1804 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1;
1805 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1808 (NEW_GOAL `between m (s2, z:real^3)`);
1809 (MATCH_MP_TAC BETWEEN_TRANS_2);
1810 (EXISTS_TAC `s3:real^3`);
1812 (ONCE_REWRITE_TAC[BETWEEN_SYM]);
1813 (ASM_REWRITE_TAC[]);
1814 (ASM_REWRITE_TAC[]);
1815 (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`);
1817 (NEW_GOAL `s2:real^3 IN voronoi_list V zl`);
1818 (EXPAND_TAC "s2" THEN EXPAND_TAC "zl");
1819 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
1820 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1822 (NEW_GOAL `s3:real^3 IN voronoi_list V zl`);
1823 (EXPAND_TAC "s3" THEN EXPAND_TAC "zl");
1824 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
1825 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1827 (NEW_GOAL `m:real^3 IN voronoi_list V zl`);
1828 (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
1829 (EXISTS_TAC `convex hull {s2, s3:real^3}`);
1831 (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
1832 (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V zl <=>
1833 convex hull {s2, s3} SUBSET (convex hull (voronoi_list V zl))`);
1834 (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
1835 (REWRITE_TAC[CONVEX_HULL_EQ]);
1836 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
1837 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
1840 (NEW_GOAL `z:real^3 IN voronoi_list V zl`);
1841 (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`));
1842 (EXISTS_TAC `convex hull {m, s3:real^3}`);
1844 (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);
1845 (REWRITE_WITH `convex hull {m, s3:real^3} SUBSET voronoi_list V zl <=>
1846 convex hull {m, s3} SUBSET (convex hull (voronoi_list V zl))`);
1847 (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`);
1848 (REWRITE_TAC[CONVEX_HULL_EQ]);
1849 (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);
1850 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
1853 (NEW_GOAL `norm (m - u0) <= norm (z - u0:real^3)`);
1854 (REWRITE_WITH `norm (m - u0) <= norm (z - u0:real^3) <=>
1855 norm (m - u0) pow 2 <= norm (z - u0:real^3) pow 2`);
1856 (ASM_SIMP_TAC[Collect_geom.POW2_COND; NORM_POS_LE]);
1857 (REWRITE_WITH `m - u0 = (m - s2) + (s2 - u0:real^3) /\
1858 z - u0 = (z - s2) + (s2 - u0:real^3)`);
1860 (REWRITE_WITH `norm (m - s2 + s2 - u0) pow 2 =
1861 norm (m - s2) pow 2 + norm (s2 - u0:real^3) pow 2`);
1862 (NEW_GOAL `(m - s2) dot (s2 - u0:real^3) = &0`);
1863 (ONCE_REWRITE_TAC[VECTOR_ARITH
1864 `(m - s2) dot (s2 - u0) = -- ((m - s2) dot (u0 - s2))`]);
1865 (REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]);
1866 (REWRITE_WITH `s2:real^3 = circumcenter (set_of_list zl)`);
1867 (REWRITE_WITH `s2:real^3 = omega_list V zl`);
1870 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`;
1871 Marchal_cells.OMEGA_LIST_TRUNCATE_2]);
1872 (MATCH_MP_TAC Rogers.XNHPWAB1);
1874 (REWRITE_TAC[IN; REAL_ARITH `a < b <=> ~(a >= b)`]);
1875 (ASM_REWRITE_TAC[]);
1876 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1877 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1878 (MATCH_MP_TAC Rogers.MHFTTZN4);
1879 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
1881 (ASM_REWRITE_TAC[]);
1882 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1883 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1884 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1885 (EXISTS_TAC `voronoi_list V zl`);
1886 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1887 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1888 (EXISTS_TAC `set_of_list (zl:(real^3)list)`);
1889 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1890 (EXPAND_TAC "zl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2;
1891 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1893 (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
1896 `norm (z - s2 + s2 - u0) pow 2 =
1897 norm (z - s2) pow 2 + norm (s2 - u0:real^3) pow 2`);
1898 (NEW_GOAL `(z - s2) dot (s2 - u0:real^3) = &0`);
1899 (ONCE_REWRITE_TAC[VECTOR_ARITH
1900 `(z - s2) dot (s2 - u0) = -- ((z - s2) dot (u0 - s2))`]);
1901 (REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]);
1902 (REWRITE_WITH `s2:real^3 = circumcenter (set_of_list zl)`);
1903 (REWRITE_WITH `s2:real^3 = omega_list V zl`);
1906 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`;
1907 Marchal_cells.OMEGA_LIST_TRUNCATE_2]);
1908 (MATCH_MP_TAC Rogers.XNHPWAB1);
1910 (REWRITE_TAC[IN; REAL_ARITH `a < b <=> ~(a >= b)`]);
1911 (ASM_REWRITE_TAC[]);
1912 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1913 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1914 (MATCH_MP_TAC Rogers.MHFTTZN4);
1915 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
1917 (ASM_REWRITE_TAC[]);
1918 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1919 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1920 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1921 (EXISTS_TAC `voronoi_list V zl`);
1922 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1923 (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`));
1924 (EXISTS_TAC `set_of_list (zl:(real^3)list)`);
1925 (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]);
1926 (EXPAND_TAC "zl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2;
1927 ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
1929 (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]);
1930 (REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`]);
1932 (MP_TAC (ASSUME `between m (s2,z:real^3)`));
1933 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN;IN_ELIM_THM] THEN STRIP_TAC);
1934 (REWRITE_TAC[ASSUME `m = u % s2 + v % z:real^3`]);
1936 `(u % s2 + v % z) - s2 = (u % s2 + v % z) - (u + v) % s2:real^3`);
1937 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
1938 (REWRITE_TAC[VECTOR_ARITH `(u % s2 + v % z) - (u + v) % s2 = v % (z - s2)`]);
1939 (REWRITE_TAC[NORM_MUL; REAL_ARITH `(a*b) pow 2 = a pow 2 * b pow 2`;
1940 REAL_ARITH `a * b <= b <=> &0 <= b * (&1 - a)`]);
1941 (MATCH_MP_TAC REAL_LE_MUL);
1942 (REWRITE_TAC[REAL_LE_POW_2]);
1943 (REWRITE_WITH `abs (v:real) = v`);
1944 (ASM_REWRITE_TAC[REAL_ABS_REFL]);
1945 (REWRITE_TAC[REAL_ARITH `&0 <= &1 - a <=> a <= &1 pow 2`]);
1946 (REWRITE_WITH ` v pow 2 <= &1 pow 2 <=> v <= &1`);
1947 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
1948 (MATCH_MP_TAC Collect_geom.POW2_COND);
1949 (ASM_REAL_ARITH_TAC);
1950 (ASM_REAL_ARITH_TAC);
1952 (NEW_GOAL `norm (m - u0:real^3) = dist (u0, s:real^3)`);
1953 (ONCE_REWRITE_TAC[DIST_SYM]);
1954 (ASM_REWRITE_TAC[GSYM dist]);
1955 (NEW_GOAL `norm (m - u0:real^3) = sqrt (&2)`);
1956 (ASM_REAL_ARITH_TAC);
1958 (REWRITE_WITH `(z - u0) dot (u1 - u0:real^3) = &2 * norm (u1 - s1) pow 2`);
1959 (REWRITE_WITH `(z - u0) dot (u1 - u0) = (z - s1) dot (u1 - u0) +
1960 (s1 - u0) dot (u1 - u0:real^3)`);
1962 (REWRITE_TAC[ASSUME `u1 - u0 = &2 % (u1 - s1:real^3)`; DOT_RMUL]);
1963 (REWRITE_WITH `(s1 - u0) = (u1 - s1:real^3)`);
1964 (ASM_REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN VECTOR_ARITH_TAC);
1965 (ASM_REWRITE_TAC[NORM_POW_2] THEN REAL_ARITH_TAC);
1967 (NEW_GOAL `&2 * norm (u1 - s1:real^3) pow 2 <=
1968 norm (m - u0) * norm (u1 - u0) * a`);
1970 (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u1:real^3)`);
1971 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
1972 (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
1973 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1974 TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
1975 (ASM_REWRITE_TAC[]);
1976 (NEW_GOAL `!w:real^3. w IN set_of_list vl
1977 ==> dist (circumcenter (set_of_list vl),w) = hl vl`);
1978 (MATCH_MP_TAC Rogers.HL_PROPERTIES);
1979 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
1980 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
1981 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
1982 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
1983 (FIRST_ASSUM MATCH_MP_TAC);
1985 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
1986 TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
1989 (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]);
1990 (REWRITE_TAC[ASSUME `u1 - u0 = &2 % (u1 - s1:real^3)`; NORM_MUL]);
1991 (REWRITE_WITH `abs (&2) = &2`);
1992 (REWRITE_TAC[REAL_ABS_REFL; REAL_ARITH `&0 <= &2`]);
1993 (REWRITE_TAC[REAL_ARITH `a * (&2 * b) * b / c = (&2 * b pow 2) * ( a / c)`]);
1994 (REWRITE_TAC[REAL_ARITH `a <= a * b <=> &0 <= a * (b - &1)`]);
1995 (MATCH_MP_TAC REAL_LE_MUL);
1996 (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_POW_2; REAL_ARITH `&0 <= &2`]);
1997 (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
1998 (REWRITE_WITH `sqrt (&2) / sqrt (&2) = &1`);
1999 (MATCH_MP_TAC REAL_DIV_REFL);
2000 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
2001 (SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]);
2004 (NEW_GOAL `norm (m - u0) * norm (u1 - u0:real^3) * a <=
2005 norm (z - u0) * norm (u1 - u0) * a`);
2006 (REWRITE_TAC[REAL_ARITH `a * x * y <= b * x * y <=>
2007 &0 <= (x * y) * (b - a)`]);
2008 (MATCH_MP_TAC REAL_LE_MUL);
2010 (MATCH_MP_TAC REAL_LE_MUL);
2011 (REWRITE_TAC[NORM_POS_LE]);
2012 (EXPAND_TAC "a" THEN MATCH_MP_TAC REAL_LE_DIV);
2013 (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u1:real^3)`);
2014 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
2015 (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
2016 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
2017 TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
2018 (ASM_REWRITE_TAC[]);
2019 (NEW_GOAL `!w:real^3. w IN set_of_list vl
2020 ==> dist (circumcenter (set_of_list vl),w) = hl vl`);
2021 (MATCH_MP_TAC Rogers.HL_PROPERTIES);
2022 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
2023 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
2024 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
2025 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
2026 (FIRST_ASSUM MATCH_MP_TAC);
2028 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
2029 TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
2031 (REWRITE_TAC[DIST_POS_LE]);
2032 (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
2033 (ASM_REAL_ARITH_TAC);
2034 (ASM_REAL_ARITH_TAC);
2037 (NEW_GOAL `t2 * norm (u1 - u0:real^3) pow 2 + t5 * ((z - u0) dot (u1 - u0))
2038 <= t2 * norm (u1 - u0) pow 2 + t5 * (norm (z - u0) * norm (u1 - u0) * a)`);
2039 (REWRITE_TAC[REAL_ARITH `a + b * c <= a + b * d <=> &0 <= b * (d - c)`]);
2040 (MATCH_MP_TAC REAL_LE_MUL);
2041 (ASM_REAL_ARITH_TAC);
2044 `t2 * norm (u1 - u0) pow 2 + t5 * norm (z - u0:real^3) * norm (u1 - u0) * a
2045 < norm (t2 % (u1 - u0) + t5 % (z - u0)) * norm (u1 - u0) * a`);
2047 (REWRITE_TAC[REAL_ARITH
2048 `t2 * norm (u1 - u0) pow 2 + t5 * norm (z - u0:real^3) * norm (u1 - u0) * a
2049 < norm (t2 % (u1 - u0) + t5 % (z - u0)) * norm (u1 - u0) * a <=>
2050 &0 < (a * norm (t2 % (u1 - u0) + t5 % (z - u0)) - t2 * norm (u1 - u0) -
2051 t5 * a * norm (z - u0)) * norm (u1 - u0)`]);
2052 (MATCH_MP_TAC REAL_LT_MUL);
2054 (REWRITE_TAC[REAL_ARITH `&0 < a - b - c <=> b + c < a`]);
2056 (NEW_GOAL `t2 * norm (u1 - u0) < a * t2 * norm (u1 - u0:real^3)`);
2057 (REWRITE_TAC[REAL_ARITH `a * b < c * a * b <=> &0 < (--a) * b * (&1 - c)`]);
2058 (MATCH_MP_TAC REAL_LT_MUL);
2060 (ASM_REAL_ARITH_TAC);
2061 (MATCH_MP_TAC REAL_LT_MUL);
2063 (REWRITE_TAC[NORM_POS_LT; VECTOR_ARITH `a - b = vec 0 <=> b = a`]);
2064 (ASM_REWRITE_TAC[]);
2065 (REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`] THEN EXPAND_TAC "a");
2066 (REWRITE_WITH `hl (vl:(real^3)list) / sqrt (&2) < &1 <=> hl vl < &1 * sqrt (&2) `);
2067 (MATCH_MP_TAC REAL_LT_LDIV_EQ);
2068 (MATCH_MP_TAC SQRT_POS_LT);
2070 (ASM_REWRITE_TAC[REAL_MUL_LID]);
2072 (NEW_GOAL `a * t2 * norm (u1 - u0) + t5 * a * norm (z - u0) <=
2073 a * norm (t2 % (u1 - u0) + t5 % (z - u0:real^3))`);
2074 (REWRITE_TAC[REAL_ARITH
2075 `a * t2 * norm (u1 - u0) + t5 * a * norm (z - u0) <=
2076 a * norm (t2 % (u1 - u0) + t5 % (z - u0)) <=>
2077 &0 <= a * (norm (t2 % (u1 - u0) + t5 % (z - u0)) + (--t2 * norm (u1 - u0)) - t5 * norm (z - u0))`]);
2078 (MATCH_MP_TAC REAL_LE_MUL);
2081 (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u1:real^3)`);
2082 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
2083 (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`);
2084 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
2085 TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
2086 (ASM_REWRITE_TAC[]);
2087 (NEW_GOAL `!w:real^3. w IN set_of_list vl
2088 ==> dist (circumcenter (set_of_list vl),w) = hl vl`);
2089 (MATCH_MP_TAC Rogers.HL_PROPERTIES);
2090 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
2091 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
2092 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
2093 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
2094 (FIRST_ASSUM MATCH_MP_TAC);
2096 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
2097 TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
2100 (MATCH_MP_TAC REAL_LE_DIV);
2101 (REWRITE_TAC[DIST_POS_LE]);
2102 (ASM_SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
2104 (ONCE_REWRITE_TAC[REAL_ARITH `&0 <= a + b - c <=> c <= a + b`]);
2105 (ABBREV_TAC `k1 = t2 % (u1 - u0) + t5 % (z - u0:real^3)`);
2106 (REWRITE_WITH `t5 * norm (z - u0) = norm (t5 % (z - u0:real^3))`);
2107 (REWRITE_TAC[NORM_MUL]);
2108 (REWRITE_WITH `abs t5 = t5`);
2109 (REWRITE_TAC[REAL_ABS_REFL]);
2110 (ASM_REAL_ARITH_TAC);
2111 (REWRITE_WITH `--t2 * norm (u1 - u0) = norm ((--t2) % (u1 - u0:real^3))`);
2112 (REWRITE_TAC[NORM_MUL]);
2113 (REWRITE_WITH `abs (--t2) = --t2`);
2114 (REWRITE_TAC[REAL_ABS_REFL]);
2115 (ASM_REAL_ARITH_TAC);
2116 (REWRITE_WITH `t5 % (z - u0) = k1 + --t2 % (u1 - u0:real^3)`);
2117 (EXPAND_TAC "k1" THEN VECTOR_ARITH_TAC);
2118 (REWRITE_TAC[NORM_TRIANGLE]);
2119 (ASM_REAL_ARITH_TAC);
2120 (REWRITE_TAC[NORM_POS_LT; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
2121 (ASM_REWRITE_TAC[]);
2122 (ASM_REAL_ARITH_TAC);
2125 (ASM_REAL_ARITH_TAC);
2127 (* ------------------------------------------------------------------------ *)
2129 (NEW_GOAL `t3 = &0 /\ t4 = &0`);
2130 (ASM_REAL_ARITH_TAC);
2132 (ASM_CASES_TAC `t1 < &0`);
2134 (UNDISCH_TAC `x:real^3 IN rcone_ge u1 u0 a`);
2135 (REWRITE_TAC[rcone_ge;rconesgn; IN; IN_ELIM_THM]);
2136 (REWRITE_TAC[REAL_ARITH `~(a >= b) <=> a < b`]);
2138 (REWRITE_TAC[dist]);
2139 (REWRITE_WITH `x - u1 = t1 % (u0 - u1:real^3)`);
2140 (REWRITE_WITH `x - u1 = x - (t1 + t2) % u1:real^3`);
2141 (REWRITE_WITH `t1 + t2 = &1`);
2142 (ASM_REAL_ARITH_TAC);
2144 (ASM_REWRITE_TAC[]);
2147 (REWRITE_TAC[DOT_LMUL;GSYM NORM_POW_2]);
2148 (NEW_GOAL `t1 * norm (u0 - u1:real^3) pow 2 < &0`);
2149 (REWRITE_TAC[REAL_ARITH `a * b < &0 <=> &0 < (--a) * b`]);
2150 (MATCH_MP_TAC REAL_LT_MUL);
2152 (ASM_REAL_ARITH_TAC);
2153 (REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT; NORM_EQ_0]);
2154 (ASM_REWRITE_TAC[VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
2156 (NEW_GOAL `&0 <= norm (t1 % (u0 - u1:real^3)) * norm (u0 - u1) * a`);
2157 (MATCH_MP_TAC REAL_LE_MUL);
2158 (REWRITE_TAC[NORM_POS_LE]);
2159 (MATCH_MP_TAC REAL_LE_MUL);
2160 (REWRITE_TAC[NORM_POS_LE]);
2162 (REWRITE_WITH `hl (vl:(real^3)list) =
2163 dist (circumcenter (set_of_list vl),HD vl)`);
2164 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
2165 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
2166 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
2167 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
2168 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
2169 (MATCH_MP_TAC REAL_LE_DIV);
2170 (REWRITE_TAC[DIST_POS_LE]);
2171 (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
2172 (ASM_REAL_ARITH_TAC);
2175 (ASM_CASES_TAC `t2 < &0`);
2177 (UNDISCH_TAC `x:real^3 IN rcone_ge u0 u1 a`);
2178 (REWRITE_TAC[rcone_ge;rconesgn; IN; IN_ELIM_THM]);
2179 (REWRITE_TAC[REAL_ARITH `~(a >= b) <=> a < b`]);
2181 (REWRITE_TAC[dist]);
2182 (REWRITE_WITH `x - u0 = t2 % (u1 - u0:real^3)`);
2183 (REWRITE_WITH `x - u0 = x - (t1 + t2) % u0:real^3`);
2184 (REWRITE_WITH `t1 + t2 = &1`);
2185 (ASM_REAL_ARITH_TAC);
2187 (ASM_REWRITE_TAC[]);
2190 (REWRITE_TAC[DOT_LMUL;GSYM NORM_POW_2]);
2191 (NEW_GOAL `t2 * norm (u1 - u0:real^3) pow 2 < &0`);
2192 (REWRITE_TAC[REAL_ARITH `a * b < &0 <=> &0 < (--a) * b`]);
2193 (MATCH_MP_TAC REAL_LT_MUL);
2195 (ASM_REAL_ARITH_TAC);
2196 (REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT; NORM_EQ_0]);
2197 (ASM_REWRITE_TAC[VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
2199 (NEW_GOAL `&0 <= norm (t2 % (u1 - u0:real^3)) * norm (u1 - u0) * a`);
2200 (MATCH_MP_TAC REAL_LE_MUL);
2201 (REWRITE_TAC[NORM_POS_LE]);
2202 (MATCH_MP_TAC REAL_LE_MUL);
2203 (REWRITE_TAC[NORM_POS_LE]);
2205 (REWRITE_WITH `hl (vl:(real^3)list) =
2206 dist (circumcenter (set_of_list vl),HD vl)`);
2207 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
2208 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);
2209 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl");
2210 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
2211 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);
2212 (MATCH_MP_TAC REAL_LE_DIV);
2213 (REWRITE_TAC[DIST_POS_LE]);
2214 (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]);
2215 (ASM_REAL_ARITH_TAC);
2218 (ASM_REAL_ARITH_TAC);
2220 (REWRITE_TAC[CONVEX_HULL_4; IN; IN_ELIM_THM]);
2221 (NEW_GOAL `between m (s2, s3:real^3)`);
2222 (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`);
2226 (ASM_REWRITE_TAC[BETWEEN_REFL]);
2230 (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\
2231 dist (u0,s) = sqrt (&2) /\
2233 (MATCH_MP_TAC MXI_EXPLICIT);
2234 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
2235 (REWRITE_TAC[REAL_ARITH `a < b <=> ~(a >= b)`]);
2236 (ASM_REWRITE_TAC[]);
2237 (FIRST_ASSUM CHOOSE_TAC THEN UP_ASM_TAC);
2238 (ASM_REWRITE_TAC[] THEN STRIP_TAC);
2239 (ASM_REWRITE_TAC[]);
2241 (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; IN; IN_ELIM_THM]);
2243 (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`);
2244 (EXISTS_TAC `t3 * u` THEN EXISTS_TAC `t3 * v + t4`);
2245 (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_ADD]);
2247 (REWRITE_TAC[REAL_ARITH `t1 + t2 + t3 * u + t3 * v + t4 =
2248 t1 + t2 + t3 * (u + v) + t4`]);
2249 (ASM_REWRITE_TAC[REAL_MUL_RID]);