1 (* ========================================================================= *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Author : VU KHAC KY *)
5 (* Book lemma: TSKAJXY *)
6 (* Chapter : Packing (Clusters) *)
7 (* Date: November 2013 *)
9 (* ========================================================================= *)
14 This does the special cases of Lemma TSKAJXY for 0, 3, and 4-cells
18 module Tskajxy_034 = struct
21 open Euler_main_theorem;;
28 open Vukhacky_tactics;;
31 (* open Marchal_cells_2;; *)
32 open Marchal_cells_2_new;;
47 open Upfzbzm_support_lemmas;;
48 open Marchal_cells_3;;
51 open Sum_gammax_lmfun_estimate;;
59 (* ======================================================================== *)
66 y4 <= &2 * sqrt (&2) /\
67 y5 <= &2 * sqrt (&2) /\
68 y6 <= &2 * sqrt (&2) /\
69 eta_y y4 y5 y6 < sqrt (&2)
70 ==> &0 <= gamma3f y4 y5 y6 sqrt2 lmfun`;;
74 `!y. &2 <= y /\ y <= sqrt8 ==>
75 &0 <= gamma2_x_div_azim_v2 (h0cut y) (y*y)`;;
77 let tsk_hyp_new = mk_conj(GRKIBMP_concl,
78 mk_conj(cell3_from_ineq,tsk_hyp));;
80 let TSKAJXY_statement_special_case = new_definition
81 `TSKAJXY_statement_special_case <=>
86 ~(?i ul. ul IN barV V 3 /\ (i = 1 \/ i = 2) /\ X = mcell i V ul) /\
87 critical_edgeX V X = {}
88 ==> gammaX V X lmfun >= &0)`;;
90 g (mk_imp(tsk_hyp_new,`TSKAJXY_statement_special_case`));;
92 let TSKAJXY_034 = Prove_by_refinement.prove_by_refinement(
93 (mk_imp(tsk_hyp_new,`TSKAJXY_statement_special_case`)),
97 (REWRITE_TAC[TSKAJXY_statement_special_case; mcell_set; IN_ELIM_THM]);
100 (ASM_CASES_TAC `NULLSET X`);
101 (REWRITE_TAC[gammaX]);
102 (MATCH_MP_TAC (REAL_ARITH `x = &0 /\ y = &0 /\ z = &0 ==> x - y + z >= &0`));
103 (REWRITE_TAC[total_solid; REAL_ENTIRE]);
105 (MATCH_MP_TAC MEASURE_EQ_0);
106 BY((ASM_REWRITE_TAC[]));
108 (REWRITE_WITH `VX V X = {}`);
110 BY((ASM_REWRITE_TAC[]));
111 BY((REWRITE_TAC[SUM_CLAUSES]));
113 (REWRITE_WITH `edgeX V X = {}`);
114 (REWRITE_TAC[edgeX]);
115 (REWRITE_WITH `VX V X = {}`);
117 BY((ASM_REWRITE_TAC[]));
118 (ONCE_REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]);
120 BY((REWRITE_TAC[SUM_CLAUSES]));
121 (NEW_GOAL `~(X:real^3->bool = {})`);
122 BY((STRIP_TAC THEN SWITCH_TAC THEN UP_ASM_TAC THEN REWRITE_TAC[ASSUME `X:real^3->bool = {}`; NEGLIGIBLE_EMPTY]));
123 (ASM_CASES_TAC `i >= 4`);
124 (NEW_GOAL `X = mcell4 V ul`);
126 BY((ASM_SIMP_TAC[MCELL_EXPLICIT]));
127 (UP_ASM_TAC THEN REWRITE_TAC[mcell4]);
129 (NEW_GOAL `?u0 u1 u2 u3. ul = [u0; u1; u2; u3:real^3]`);
130 (MATCH_MP_TAC BARV_3_EXPLICIT);
131 BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
132 (UP_ASM_TAC THEN STRIP_TAC);
133 (REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`; set_of_list]);
135 (ABBREV_TAC `y1 = dist (u0:real^3, u1)`);
136 (ABBREV_TAC `y2 = dist (u0:real^3, u2)`);
137 (ABBREV_TAC `y3 = dist (u0:real^3, u3)`);
138 (ABBREV_TAC `y4 = dist (u2:real^3, u3)`);
139 (ABBREV_TAC `y5 = dist (u1:real^3, u3)`);
140 (ABBREV_TAC `y6 = dist (u1:real^3, u2)`);
141 (NEW_GOAL `VX V X = {u0,u1,u2,u3}`);
142 (REWRITE_WITH `VX V X = V INTER X`);
143 (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
144 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
145 BY((ASM_REWRITE_TAC[]));
146 (REWRITE_WITH `X = mcell 4 V ul`);
148 BY((MESON_TAC[ARITH_RULE `4 >= 4`; ASSUME `i >= 4`; MCELL_EXPLICIT]));
149 (REWRITE_WITH `V INTER mcell 4 V ul = set_of_list (truncate_simplex (4 - 1) ul)`);
150 (MATCH_MP_TAC Lepjbdj.LEPJBDJ);
151 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 4 /\ 4 <= 4`]);
152 (REWRITE_WITH ` mcell 4 V [u0; u1; u2; u3] = X`);
154 BY((MESON_TAC[ARITH_RULE `4 >= 4`; ASSUME `i >= 4`; MCELL_EXPLICIT]));
155 BY((ASM_REWRITE_TAC[]));
156 BY((ASM_REWRITE_TAC[ARITH_RULE `4 - 1 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3; set_of_list]));
157 (REWRITE_WITH `vol X = vol_y y1 y2 y3 y4 y5 y6 /\ gammaX V X lmfun = gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun`);
158 (MATCH_MP_TAC gammaX_gamm4fgcy);
159 (EXISTS_TAC `ul:(real^3)list`);
160 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
161 (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
162 (EXISTS_TAC `i:num`);
163 BY((ASM_REWRITE_TAC[]));
164 (NEW_GOAL `!y1 y2 y3 y4 y5 y6. ineq [#2.0,y1,sqrt8; #2.0,y2,sqrt8; #2.0,y3,sqrt8; #2.0,y4,sqrt8; #2.0, y5, sqrt8; #2.0,y6,sqrt8] (~critical_edge_y y1 /\ ~critical_edge_y y2 /\ ~critical_edge_y y3 /\ ~critical_edge_y y4 /\ ~critical_edge_y y5 /\ ~critical_edge_y y6 /\ &0 < delta_y y1 y2 y3 y4 y5 y6 /\ rad2_y y1 y2 y3 y4 y5 y6 < &2 ==> gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun >= &0)`);
165 (MATCH_MP_TAC TSKAJXY_DERIVED4);
166 BY((ASM_REWRITE_TAC[]));
167 (UP_ASM_TAC THEN REWRITE_TAC[ineq; MESON[] `a ==> b ==> c <=> (a /\ b) ==> c`] THEN STRIP_TAC);
168 (FIRST_ASSUM MATCH_MP_TAC);
170 (NEW_GOAL `~(critical_edge_y y1) /\ ~(critical_edge_y y2) /\ ~(critical_edge_y y3) /\ ~(critical_edge_y y4) /\ ~(critical_edge_y y5) /\ ~(critical_edge_y y6) /\ &0 < delta_y y1 y2 y3 y4 y5 y6`);
171 (REWRITE_TAC[critical_edge_y]);
173 (NEW_GOAL `{u0:real^3, u1} IN critical_edgeX V X`);
174 (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
175 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
176 (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
178 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
181 BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
183 BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
184 (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y1`);
185 (EXPAND_TAC "y1" THEN REWRITE_TAC[dist; ASSUME `u0:real^3 = u1`; NORM_ARITH `norm (u1 - u1) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);
186 BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
187 BY((ASM_REAL_ARITH_TAC));
188 BY((ASM_REAL_ARITH_TAC));
190 (NEW_GOAL `{u0:real^3, u2} IN critical_edgeX V X`);
191 (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
192 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u2:real^3`);
193 (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
195 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u2:real^3`);
198 BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
200 BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
201 (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y2`);
202 (EXPAND_TAC "y2" THEN REWRITE_TAC[dist; ASSUME `u0:real^3 = u2`; NORM_ARITH `norm (u2 - u2) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);
203 BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
204 BY((ASM_REAL_ARITH_TAC));
205 BY((ASM_REAL_ARITH_TAC));
207 (NEW_GOAL `{u0:real^3, u3} IN critical_edgeX V X`);
208 (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
209 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u3:real^3`);
210 (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
212 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u3:real^3`);
215 BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
217 BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
218 (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y3`);
219 (EXPAND_TAC "y3" THEN REWRITE_TAC[dist; ASSUME `u0:real^3 = u3`; NORM_ARITH `norm (u3 - u3) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);
220 BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
221 BY((ASM_REAL_ARITH_TAC));
222 BY((ASM_REAL_ARITH_TAC));
224 (NEW_GOAL `{u2:real^3, u3} IN critical_edgeX V X`);
225 (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
226 (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
227 (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
229 (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
232 BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
234 BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
235 (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y4`);
236 (EXPAND_TAC "y4" THEN REWRITE_TAC[dist; ASSUME `u2:real^3 = u3`; NORM_ARITH `norm (u3 - u3) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);
237 BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
238 BY((ASM_REAL_ARITH_TAC));
239 BY((ASM_REAL_ARITH_TAC));
241 (NEW_GOAL `{u1:real^3, u3} IN critical_edgeX V X`);
242 (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
243 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u3:real^3`);
244 (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
246 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u3:real^3`);
249 BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
251 BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
252 (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y5`);
253 (EXPAND_TAC "y5" THEN REWRITE_TAC[dist; ASSUME `u1:real^3 = u3`; NORM_ARITH `norm (u3 - u3) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);
254 BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
255 BY((ASM_REAL_ARITH_TAC));
256 BY((ASM_REAL_ARITH_TAC));
258 (NEW_GOAL `{u1:real^3, u2} IN critical_edgeX V X`);
259 (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
260 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3`);
261 (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
263 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3`);
266 BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
268 BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
269 (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y6`);
270 (EXPAND_TAC "y6" THEN REWRITE_TAC[dist; ASSUME `u1:real^3 = u2`; NORM_ARITH `norm (u2 - u2) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);
271 BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
272 BY((ASM_REAL_ARITH_TAC));
273 BY((ASM_REAL_ARITH_TAC));
275 (REWRITE_WITH `&0 < delta_y y1 y2 y3 y4 y5 y6 <=> &0 < sqrt (delta_y y1 y2 y3 y4 y5 y6)`);
276 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
277 (MATCH_MP_TAC SQRT_LT_0);
278 (REWRITE_TAC[delta_y]);
279 (ABBREV_TAC `x1 = y1 * y1` THEN ABBREV_TAC `x2 = y2 * y2`);
280 (ABBREV_TAC `x3 = y3 * y3` THEN ABBREV_TAC `x4 = y4 * y4`);
281 (ABBREV_TAC `x5 = y5 * y5` THEN ABBREV_TAC `x6 = y6 * y6`);
282 (REWRITE_WITH `delta_x x1 x2 x3 x4 x5 x6 = (let a = u1:real^3 - u0 in let b = u2 - u0 in let c = u3 - u0 in &4 * (a$1 * b$2 * c$3 - a$1 * b$3 * c$2 - a$2 * b$1 * c$3 + a$2 * b$3 * c$1 + a$3 * b$1 * c$2 - a$3 * b$2 * c$1) pow 2)`);
283 (MATCH_MP_TAC Delta_x.COMPUTE_DELTA_X);
284 (REWRITE_TAC[xlist; ylist]);
286 (EXPAND_TAC "x1" THEN EXPAND_TAC "x2" THEN EXPAND_TAC "x3");
287 (EXPAND_TAC "x4" THEN EXPAND_TAC "x5" THEN EXPAND_TAC "x6");
288 (UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ; GSYM REAL_POW_2]);
291 BY((ASM_REWRITE_TAC[]));
293 (REWRITE_TAC[REAL_ARITH `&0 <= &4 * a <=> &0 <= a`]);
294 BY((REWRITE_TAC[Real_ext.REAL_LE_POW_2]));
295 (ONCE_REWRITE_TAC[REAL_ARITH `&0 < a <=> &0 < a / &12`]);
296 (REWRITE_WITH `sqrt (delta_y y1 y2 y3 y4 y5 y6) / &12 = vol (convex hull {u0,u1,u2,u3})`);
297 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
298 (REWRITE_TAC[delta_y; GSYM REAL_POW_2]);
299 (EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");
300 (EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6");
301 BY((REWRITE_TAC[VOLUME_OF_CLOSED_TETRAHEDRON]));
302 (REWRITE_TAC[GSYM (ASSUME `X = convex hull {u0, u1, u2, u3:real^3}`)]);
303 (REWRITE_WITH `&0 < vol X <=> ~NULLSET X`);
304 (MATCH_MP_TAC MEASURABLE_MEASURE_POS_LT);
305 (REWRITE_TAC[ASSUME `X = convex hull {u0, u1, u2, u3:real^3}`]);
306 (MATCH_MP_TAC MEASURABLE_CONVEX_HULL);
307 (MATCH_MP_TAC FINITE_IMP_BOUNDED);
308 BY((REWRITE_TAC[Geomdetail.FINITE6]));
309 BY((ASM_REWRITE_TAC[]));
311 (NEW_GOAL `!u v. {u,v} IN edgeX V X ==> (#2.0 <= dist (u,v) /\ dist(u,v) <= sqrt8)`);
313 (REWRITE_TAC[edgeX; IN]);
314 (REWRITE_TAC[MESON[IN] `VX V X x <=> x IN VX V X`]);
315 (ASM_REWRITE_TAC[IN_ELIM_THM]);
317 (MP_TAC (ASSUME `packing V`));
318 (REWRITE_TAC[packing; REAL_ARITH `#2.0 = &2`] THEN STRIP_TAC);
320 (FIRST_ASSUM MATCH_MP_TAC);
321 (NEW_GOAL `u:real^3 IN {u0,u1,u2,u3} /\ v IN {u0,u1,u2,u3}`);
322 (DEL_TAC THEN UP_ASM_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);
324 (NEW_GOAL `{u0,u1,u2,u3:real^3} SUBSET V`);
325 (REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
326 (MATCH_MP_TAC BARV_SUBSET);
327 BY((EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]));
329 (REWRITE_TAC[MESON[IN] `(V:real^3->bool) x <=> x IN V`]);
330 BY((UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]));
332 (REWRITE_TAC[MESON[IN] `(V:real^3->bool) x <=> x IN V`]);
333 BY((UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]));
334 (DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);
336 (ABBREV_TAC `s = circumcenter {u0,u1,u2,u3:real^3}`);
337 (NEW_GOAL `dist (u,v:real^3) <= dist (s,u) + dist (s, v)`);
338 BY((NORM_ARITH_TAC));
339 (NEW_GOAL `!w. w IN {u0,u1,u2,u3:real^3} ==> radV {u0,u1,u2,u3:real^3} = dist (circumcenter {u0,u1,u2,u3:real^3},w)`);
340 (MATCH_MP_TAC Rogers.OAPVION2);
341 (REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
342 (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);
343 BY((EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]));
344 (NEW_GOAL `dist (s,u) + dist (s,v:real^3) <= sqrt8`);
345 (REWRITE_TAC[Nonlinear_lemma.sqrt8_sqrt2; sqrt2]);
346 (MATCH_MP_TAC (REAL_ARITH `a < x /\ b < x ==> a + b <= &2 * x`));
348 (REWRITE_WITH `dist (s,u:real^3) = radV {u0,u1,u2,u3:real^3}`);
349 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
351 (FIRST_ASSUM MATCH_MP_TAC);
352 (DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN DEL_TAC);
353 (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);
355 (REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
356 (REWRITE_TAC[GSYM HL]);
357 BY((ASM_REWRITE_TAC[]));
358 (REWRITE_WITH `dist (s,v:real^3) = radV {u0,u1,u2,u3:real^3}`);
359 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
361 (FIRST_ASSUM MATCH_MP_TAC);
362 (DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN DEL_TAC);
363 (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);
365 (REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
366 (REWRITE_TAC[GSYM HL]);
367 BY((ASM_REWRITE_TAC[]));
368 BY((ASM_REAL_ARITH_TAC));
369 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`);
370 (REWRITE_TAC[ARITH_RULE `4 = 3 + 1`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
371 (MATCH_MP_TAC Marchal_cells_3.BARV_CARD_LEMMA);
372 BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
373 (NEW_GOAL `~(u0 = u1:real^3) /\ ~(u0 = u2) /\ ~(u0 = u3) /\ ~(u1 = u2) /\ ~(u1 = u3) /\ ~(u2 = u3)`);
375 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
376 BY((REWRITE_TAC[ASSUME `u0 = u1:real^3`; SET_RULE `{u1, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
378 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
379 BY((REWRITE_TAC[ASSUME `u0 = u2:real^3`; SET_RULE `{u2, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
381 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
382 BY((REWRITE_TAC[ASSUME `u0 = u3:real^3`; SET_RULE `{u3, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
384 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
385 BY((REWRITE_TAC[ASSUME `u1 = u2:real^3`; SET_RULE `{u0, u2, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ]));
387 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
388 BY((REWRITE_TAC[ASSUME `u1 = u3:real^3`; SET_RULE `{u0, u3, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ]));
390 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
391 BY((REWRITE_TAC[ASSUME `u2 = u3:real^3`; SET_RULE `{u0, u1, u3, u3} = {u0,u1,u3}`;Geomdetail.CARD3 ]));
393 (NEW_GOAL `edgeX V X = {{u0,u1:real^3}, {u0,u2}, {u0,u3}, {u1,u2}, {u1,u3}, {u2,u3}}`);
394 (REWRITE_TAC[edgeX]);
395 (ONCE_REWRITE_TAC[SET_EQ_LEMMA]);
396 (REWRITE_TAC[IN_ELIM_THM]);
398 (UNDISCH_TAC `VX V X u` THEN UNDISCH_TAC `VX V X v`);
399 (REWRITE_TAC[MESON[IN] `VX V X s <=> s IN VX V X`]);
400 (ASM_REWRITE_TAC[SET_RULE `v IN {u0, u1, u2, u3} <=> v = u0 \/ v = u1 \/ v = u2 \/ v = u3`]);
403 BY((ASM_MESON_TAC[]));
404 BY((ASM_MESON_TAC[]));
405 (REWRITE_WITH `{u,v} = {v,u:real^3}`);
407 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
408 (REWRITE_WITH `{u,v} = {v,u:real^3}`);
410 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
411 (REWRITE_WITH `{u,v} = {v,u:real^3}`);
413 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
414 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
416 BY((ASM_MESON_TAC[]));
417 BY((ASM_MESON_TAC[]));
418 (REWRITE_WITH `{u,v} = {v,u:real^3}`);
420 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
421 (REWRITE_WITH `{u,v} = {v,u:real^3}`);
423 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
424 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
425 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
427 BY((ASM_MESON_TAC[]));
428 BY((ASM_MESON_TAC[]));
429 (REWRITE_WITH `{u,v} = {v,u:real^3}`);
431 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
432 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
433 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
434 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
436 BY((ASM_MESON_TAC[]));
437 BY((ASM_MESON_TAC[]));
438 (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE `x IN {a,b,c,d,e,f} <=> x = a \/ x = b \/ x = c \/ x = d \/ x = e \/ x = f`]);
439 (REWRITE_TAC[MESON[IN] `VX V X s <=> s IN VX V X`]);
440 (ASM_REWRITE_TAC[SET_RULE `v IN {u0, u1, u2, u3} <=> v = u0 \/ v = u1 \/ v = u2 \/ v = u3`]);
442 BY((EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]));
443 BY((EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u2:real^3` THEN ASM_REWRITE_TAC[]));
444 BY((EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[]));
445 BY((EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN ASM_REWRITE_TAC[]));
446 BY((EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[]));
447 BY((EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[]));
450 (FIRST_ASSUM MATCH_MP_TAC);
451 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
454 (FIRST_ASSUM MATCH_MP_TAC);
455 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
458 (FIRST_ASSUM MATCH_MP_TAC);
459 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
462 (FIRST_ASSUM MATCH_MP_TAC);
463 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
466 (FIRST_ASSUM MATCH_MP_TAC);
467 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
470 (FIRST_ASSUM MATCH_MP_TAC);
471 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
472 (REWRITE_WITH `rad2_y y1 y2 y3 y4 y5 y6 = radV {u0,u1,u2,u3:real^3} pow 2`);
473 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
474 (REWRITE_TAC[rad2_y; y_of_x]);
475 (GMATCH_SIMP_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] Merge_ineq.GDRQXLGv2));
478 (REWRITE_TAC[ARITH_RULE `4 = 3 + 1`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
479 (MATCH_MP_TAC Marchal_cells_3.BARV_CARD_LEMMA);
480 BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
481 (REWRITE_TAC[Collect_geom.coplanar_alt]);
482 (REWRITE_TAC[GSYM Trigonometry2.coplanar1]);
483 (REWRITE_TAC[coplanar] THEN STRIP_TAC);
484 (NEW_GOAL `affine hull {u0, u1, u2, u3:real^3} SUBSET affine hull (affine hull {u, v, w})`);
485 BY((ASM_SIMP_TAC[Marchal_cells_2_new.AFFINE_SUBSET_KY_LEMMA]));
486 (UP_ASM_TAC THEN REWRITE_WITH `affine hull (affine hull {u, v, w}) = affine hull {u:real^3, v, w}`);
487 BY((REWRITE_TAC[AFFINE_HULL_EQ; AFFINE_AFFINE_HULL]));
489 (NEW_GOAL `NULLSET X`);
490 (MATCH_MP_TAC NEGLIGIBLE_SUBSET);
491 (EXISTS_TAC `affine hull {u0, u1, u2, u3:real^3}`);
493 (MATCH_MP_TAC NEGLIGIBLE_SUBSET);
494 (EXISTS_TAC `affine hull {u,v,w:real^3}`);
495 (REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]);
496 BY((ASM_REWRITE_TAC[]));
497 (REWRITE_TAC[ASSUME `X = mcell i V ul`]);
498 (REWRITE_WITH `mcell i V ul = mcell4 V ul`);
499 BY((MESON_TAC[ARITH_RULE `4 >= 4`; MCELL_EXPLICIT; ASSUME `i >= 4`]));
500 (REWRITE_TAC[mcell4]);
502 BY((ASM_REWRITE_TAC[set_of_list; CONVEX_HULL_SUBSET_AFFINE_HULL]));
504 BY((UP_ASM_TAC THEN ASM_REWRITE_TAC[]));
505 (REWRITE_TAC[GSYM REAL_POW_2]);
506 (EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");
507 (EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6");
509 (REWRITE_WITH `radV {u0, u1, u2, u3:real^3} = hl (ul:(real^3)list)`);
510 BY((ASM_REWRITE_TAC[HL;set_of_list]));
511 (REWRITE_WITH `hl (ul:(real^3)list) pow 2 < &2 <=> sqrt (hl ul pow 2) < sqrt (&2)`);
512 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
513 (MATCH_MP_TAC Real_ext.REAL_PROP_LT_SQRT);
514 BY((REWRITE_TAC[REAL_LE_POW_2] THEN REAL_ARITH_TAC));
515 (REWRITE_WITH `sqrt (hl (ul:(real^3)list) pow 2) = hl ul`);
516 (MATCH_MP_TAC POW_2_SQRT);
517 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
518 (NEW_GOAL `hl (truncate_simplex 1 ul) <= hl (ul:(real^3)list)`);
519 (MATCH_MP_TAC Rogers.HL_DECREASE);
520 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3`);
521 BY((ASM_REWRITE_TAC[IN; ARITH_RULE `1 <= 3`]));
522 (NEW_GOAL `&0 < hl (truncate_simplex 1 (ul:(real^3)list))`);
523 (MATCH_MP_TAC Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT);
524 BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
525 BY((ASM_REAL_ARITH_TAC));
526 BY((ASM_REWRITE_TAC[]));
529 BY((UP_ASM_TAC THEN ASM_REWRITE_TAC[]));
530 BY((UP_ASM_TAC THEN ASM_REWRITE_TAC[]));
531 (COMMENT "END OF 4-CELL CASE");
532 (ASM_CASES_TAC `i = 0`);
533 (NEW_GOAL `VX V X = {}`);
534 (REWRITE_WITH `VX V X = V INTER X`);
535 (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
536 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
537 BY((ASM_REWRITE_TAC[]));
539 (MATCH_MP_TAC Lepjbdj.LEPJBDJ_0);
540 BY((ASM_REWRITE_TAC[]));
541 (NEW_GOAL `edgeX V X = {}`);
542 (REWRITE_TAC[edgeX]);
543 (ASM_REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`; SET_RULE `x IN {} <=> F`]);
545 (REWRITE_TAC[gammaX]);
546 (MATCH_MP_TAC (REAL_ARITH `b = &0 /\ c = &0 /\ &0 <= a ==> a - b + c >= &0`));
548 BY((ASM_REWRITE_TAC[total_solid; SUM_CLAUSES] THEN REAL_ARITH_TAC));
549 BY((ASM_REWRITE_TAC[SUM_CLAUSES] THEN REAL_ARITH_TAC));
550 (MATCH_MP_TAC MEASURE_POS_LE);
551 (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC Urrphbz1.MEASURABLE_MCELL);
552 BY((ASM_REWRITE_TAC[]));
553 COMMENT "insert. thales. Jan 2013";
554 FIRST_X_ASSUM_ST `gamma3f` MP_TAC;
555 REPEAT (FIRST_X_ASSUM_ST `ineq` kill);
557 TYPIFY `i = 3` (C SUBGOAL_THEN ASSUME_TAC);
558 MATCH_MP_TAC (arith `~(i >= 4) /\ ~(i=0) /\ ~((i=1) \/ (i=2)) ==> (i = 3)`);
559 REPLICATE_TAC 9 (FIRST_X_ASSUM MP_TAC);
560 REPEAT (FIRST_X_ASSUM kill);
562 REPEAT (FIRST_X_ASSUM_ST `gamma4fgcy` kill);
563 COMMENT "end of insert";
564 (NEW_GOAL `X = mcell3 V ul`);
566 BY((ASM_SIMP_TAC[MCELL_EXPLICIT]));
567 (UP_ASM_TAC THEN REWRITE_TAC[mcell3]);
570 (NEW_GOAL `?u0 u1 u2 u3. ul = [u0; u1; u2; u3:real^3]`);
571 (MATCH_MP_TAC BARV_3_EXPLICIT);
572 BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
573 (UP_ASM_TAC THEN STRIP_TAC);
574 (NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\ dist (u0,s) = sqrt (&2) /\ mxi V ul = s)`);
575 (MATCH_MP_TAC MXI_EXPLICIT);
576 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
577 BY((ASM_REWRITE_TAC[]));
578 (UP_ASM_TAC THEN STRIP_TAC);
579 (ABBREV_TAC `s2 = omega_list_n V ul 2`);
580 (ABBREV_TAC `s3 = omega_list_n V ul 3`);
581 (ABBREV_TAC `vl = truncate_simplex 2 (ul:(real^3)list)`);
582 (NEW_GOAL `s2 IN voronoi_list V vl`);
583 (EXPAND_TAC "s2" THEN EXPAND_TAC "vl");
584 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
585 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
587 (NEW_GOAL `s3 IN voronoi_list V vl`);
588 (EXPAND_TAC "s3" THEN EXPAND_TAC "vl");
589 (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
590 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
592 (NEW_GOAL `s IN voronoi_list V vl`);
593 (MATCH_MP_TAC (SET_RULE `(?x. s IN x /\ x SUBSET t)==> s IN t`));
594 (EXISTS_TAC `convex hull {s2,s3:real^3}`);
596 BY((ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]));
597 (NEW_GOAL `voronoi_list V vl = convex hull (voronoi_list V vl)`);
598 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
599 BY((REWRITE_TAC[CONVEX_HULL_EQ; Packing3.CONVEX_VORONOI_LIST]));
600 (ONCE_REWRITE_TAC[ASSUME `voronoi_list V vl = convex hull voronoi_list V vl`]);
601 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
603 (MP_TAC (ASSUME `s IN voronoi_list V vl`));
604 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; VORONOI_LIST; VORONOI_SET; set_of_list; SET_RULE `x IN {a,b,c} <=> x=a\/x=b\/x=c`; IN_INTERS]);
606 (NEW_GOAL `s IN voronoi_closed V u0 /\ s IN voronoi_closed V u1 /\ s IN voronoi_closed V (u2:real^3)`);
607 BY((UP_ASM_TAC THEN SET_TAC[]));
608 (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM] THEN STRIP_TAC);
609 (NEW_GOAL `u0 IN V /\ u1 IN V /\ u2 IN V /\ (u3:real^3) IN V`);
610 (REWRITE_TAC[SET_RULE `u0 IN V /\ u1 IN V /\ u2 IN V /\ (u3:real^3) IN V <=> {u0,u1,u2,u3} SUBSET V`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
611 (MATCH_MP_TAC BARV_SUBSET);
612 BY((EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]));
613 (FIRST_ASSUM MP_TAC THEN REWRITE_TAC[IN] THEN STRIP_TAC);
614 (NEW_GOAL `dist (s,u1:real^3) = sqrt(&2)`);
615 (REWRITE_TAC[GSYM (ASSUME `dist (u0:real^3, s) = sqrt (&2)`)]);
616 (REWRITE_WITH `dist (u0,s:real^3) = dist (s,u0)`);
617 BY((NORM_ARITH_TAC));
618 (REWRITE_TAC[REAL_ARITH `a = b <=> a <= b /\ b <= a`]);
619 BY((ASM_SIMP_TAC[]));
620 (NEW_GOAL `dist (s,u2:real^3) = sqrt(&2)`);
621 (REWRITE_TAC[GSYM (ASSUME `dist (u0:real^3, s) = sqrt (&2)`)]);
622 (REWRITE_WITH `dist (u0,s:real^3) = dist (s,u0)`);
623 BY((NORM_ARITH_TAC));
624 (REWRITE_TAC[REAL_ARITH `a = b <=> a <= b /\ b <= a`]);
625 BY((ASM_SIMP_TAC[]));
626 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`);
627 (REWRITE_TAC[ARITH_RULE `4 = 3 + 1`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
628 (MATCH_MP_TAC Marchal_cells_3.BARV_CARD_LEMMA);
629 BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
630 (NEW_GOAL `~(u0 = u1:real^3) /\ ~(u0 = u2) /\ ~(u0 = u3) /\ ~(u1 = u2) /\ ~(u1 = u3) /\ ~(u2 = u3)`);
632 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
633 BY((REWRITE_TAC[ASSUME `u0 = u1:real^3`; SET_RULE `{u1, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
635 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
636 BY((REWRITE_TAC[ASSUME `u0 = u2:real^3`; SET_RULE `{u2, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
638 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
639 BY((REWRITE_TAC[ASSUME `u0 = u3:real^3`; SET_RULE `{u3, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
641 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
642 BY((REWRITE_TAC[ASSUME `u1 = u2:real^3`; SET_RULE `{u0, u2, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ]));
644 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
645 BY((REWRITE_TAC[ASSUME `u1 = u3:real^3`; SET_RULE `{u0, u3, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ]));
647 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
648 BY((REWRITE_TAC[ASSUME `u2 = u3:real^3`; SET_RULE `{u0, u1, u3, u3} = {u0,u1,u3}`;Geomdetail.CARD3 ]));
650 (NEW_GOAL `VX V X = {u0,u1,u2}`);
651 (REWRITE_WITH `VX V X = V INTER X`);
652 (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
653 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `3`);
654 BY((ASM_REWRITE_TAC[]));
655 (REWRITE_WITH `X = mcell 3 V ul`);
656 BY((ASM_REWRITE_TAC[]));
657 (REWRITE_WITH `V INTER mcell 3 V ul = set_of_list (truncate_simplex (3 - 1) ul)`);
658 (MATCH_MP_TAC Lepjbdj.LEPJBDJ);
659 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3 /\ 3 <= 4`]);
660 (REWRITE_WITH ` mcell 3 V [u0; u1; u2; u3] = X`);
661 BY((ASM_REWRITE_TAC[]));
662 BY((ASM_REWRITE_TAC[]));
663 BY((ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]));
664 (UNDISCH_TAC `X = convex hull (set_of_list vl UNION {mxi V ul})`);
665 (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2; ASSUME `ul = [u0;u1;u2;u3:real^3]`; SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);
666 (REWRITE_WITH `mxi V [u0; u1; u2; u3] = s`);
667 BY((EXPAND_TAC "s" THEN AP_TERM_TAC THEN ASM_REWRITE_TAC[]));
669 (NEW_GOAL `~coplanar {u0,u1,u2,s:real^3}`);
670 (ONCE_REWRITE_TAC[GSYM COPLANAR_AFFINE_HULL_COPLANAR]);
672 (NEW_GOAL `NULLSET X`);
673 (MATCH_MP_TAC COPLANAR_IMP_NEGLIGIBLE);
674 (REWRITE_TAC[ASSUME `X = convex hull {u0, u1, u2, s:real^3}`]);
675 (MATCH_MP_TAC COPLANAR_SUBSET);
676 (EXISTS_TAC `affine hull {u0, u1, u2, s:real^3}`);
677 BY((ASM_REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]));
678 BY((UP_ASM_TAC THEN ASM_REWRITE_TAC[]));
679 (NEW_GOAL `CARD {u0, u1, u2, s:real^3} = 4`);
680 (NEW_GOAL `CARD {u0, u1, u2, s:real^3} <= 4`);
681 BY((REWRITE_TAC[Geomdetail.CARD4]));
682 (ASM_CASES_TAC `CARD {u0, u1, u2, s:real^3} <= 3`);
684 (UNDISCH_TAC `~coplanar {u0, u1, u2, s:real^3}`);
685 (REWRITE_TAC[] THEN MATCH_MP_TAC COPLANAR_SMALL);
686 BY((ASM_REWRITE_TAC[Geomdetail.FINITE6]));
687 BY((UP_ASM_TAC THEN MESON_TAC[]));
689 (NEW_GOAL `~(u0 = s:real^3) /\ ~(u1 = s) /\ ~(u2 = s)`);
691 (NEW_GOAL `CARD {u0, u1, u2,s:real^3} <= 3`);
692 BY((REWRITE_TAC[ASSUME `u0 = s:real^3`; SET_RULE `{s, u1, u2, s} = {s,u1,u2}`;Geomdetail.CARD3 ]));
694 (NEW_GOAL `CARD {u0, u1, u2, s:real^3} <= 3`);
695 BY((REWRITE_TAC[ASSUME `u1 = s:real^3`; SET_RULE `{u0, s, u2, s} = {u0,u2,s}`;Geomdetail.CARD3 ]));
697 (NEW_GOAL `CARD {u0, u1, u2, s:real^3} <= 3`);
698 BY((REWRITE_TAC[ASSUME `u2 = s:real^3`; SET_RULE `{u0, u1, s, s} = {u0,u1,s}`;Geomdetail.CARD3 ]));
700 (ABBREV_TAC `y4 = dist (u1:real^3, u2)`);
701 (ABBREV_TAC `y5 = dist (u0:real^3, u2)`);
702 (ABBREV_TAC `y6 = dist (u0:real^3, u1)`);
703 COMMENT "insert by thales, Jan 2013";
704 INTRO_TAC Tskajxy_lemmas.gammaX_gamma3f [`V`;`X`;`ul`;`u0`;`u1`;`u2`;`u3`;`y4`;`y5`;`y6`];
706 REPEAT WEAK_STRIP_TAC THEN ASM_REWRITE_TAC[arith `x >= &0 <=> &0 <= x`];
707 REPLICATE_TAC 8 (FIRST_X_ASSUM kill);
708 FIRST_X_ASSUM MATCH_MP_TAC;
709 TYPIFY `&2 <= y4 /\ &2 <= y5 /\ &2 <= y6` (C SUBGOAL_THEN ASSUME_TAC);
710 REPLICATE_TAC 3 (FIRST_X_ASSUM (SUBST1_TAC o SYM));
711 BY(ASM_MESON_TAC[packing]);
713 TYPIFY `y4 <= &2 * sqrt (&2) /\ y5 <= &2 * sqrt (&2) /\ y6 <= &2 * sqrt (&2)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
714 REPLICATE_TAC 3 (FIRST_X_ASSUM (SUBST1_TAC o SYM));
715 TYPIFY `!(u:real^3) v. (dist(u,s) = sqrt(&2) /\ dist(v,s) = sqrt(&2)) ==> (dist(u,v) <= &2 * sqrt(&2))` (C SUBGOAL_THEN ASSUME_TAC);
716 REPEAT WEAK_STRIP_TAC;
717 FIRST_X_ASSUM (ASSUME_TAC o (ONCE_REWRITE_RULE[DIST_SYM]));
718 INTRO_TAC DIST_TRIANGLE [`u`;`s`;`v`];
719 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
720 REPEAT (FIRST_X_ASSUM_ST `x = sqrt(&2)` MP_TAC);
721 TYPIFY `!u. dist (s,u) = dist(u,s)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
722 BY(MESON_TAC[DIST_SYM]);
724 INTRO_TAC Collect_geom.RADV_FORMULAR [`u0`;`u1`;`u2`];
725 REWRITE_TAC[Collect_geom.dist3];
727 BY(ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);
729 FIRST_X_ASSUM_ST `hl vl` MP_TAC;
731 TYPIFY `hl (truncate_simplex 2 ul) = radV {u0,u1,u2}` ENOUGH_TO_SHOW_TAC;
733 REWRITE_TAC[Pack_defs.HL];
735 GMATCH_SIMP_TAC Bump.SET_OF_LIST_TRUNCATE_2;
736 ASM_REWRITE_TAC[Bump.EL_EXPLICIT];
739 BY(ASM_MESON_TAC[NEGLIGIBLE_EMPTY])
744 (* ======================================================================== *)
746 (* OLD SCRIPT FOLLOWS *)