Update from HH
[Flyspeck/.git] / text_formalization / packing / TSKAJXY_034.hl
1 (* ========================================================================= *)
2 (*                FLYSPECK - BOOK FORMALIZATION                              *)
3 (*                                                                           *)
4 (*      Author    : VU KHAC KY                                               *)
5 (*      Book lemma: TSKAJXY                                                  *)
6 (*      Chapter   : Packing (Clusters)                                       *)
7 (*      Date: November 2013                                                  *)
8 (*                                                                           *)
9 (* ========================================================================= *)
10
11
12 (*
13
14 This does the special cases of Lemma TSKAJXY for 0, 3, and 4-cells
15
16 *)
17
18 module Tskajxy_034 = struct
19
20 open Sphere;;
21 open Euler_main_theorem;;
22 open Pack_defs;;
23 open Pack_concl;;
24 open Pack1;;
25 open Pack2;;
26 open Packing3;;
27 open Rogers;;
28 open Vukhacky_tactics;;
29 open Marchal_cells;;
30 open Emnwuus;;
31 (* open Marchal_cells_2;; *)
32 open Marchal_cells_2_new;;
33 open Urrphbz1;;
34 open Lepjbdj;;
35 open Hdtfnfz;;
36 open Rvfxzbu;;
37 open Sltstlo;;
38 open Urrphbz2;;
39 open Urrphbz3;;
40 open Ynhyjit;;
41 open Njiutiu;;
42 open Tezffsk;;
43 open Qzksykg;;
44 open Ddzuphj;;
45 open Ajripqn;;
46 open Qzyzmjc;;
47 open Upfzbzm_support_lemmas;;
48 open Marchal_cells_3;;
49 open Grutoti;;
50 open Kizhltl;;
51 open Sum_gammax_lmfun_estimate;;
52 open Upfzbzm;;
53 open Rdwkarc;;
54 open Ineq;;
55 open Merge_ineq;;
56 open Hales_tactic;;
57 open Tskajxy_lemmas;;
58
59 (* ======================================================================== *)
60
61 let cell3_from_ineq = 
62  `!y4 y5 y6.
63          &2 <= y4 /\
64          &2 <= y5 /\
65          &2 <= y6 /\
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`;;
71
72
73 let GRKIBMP_concl = 
74   `!y. &2 <= y /\ y <= sqrt8 ==>
75      &0 <= gamma2_x_div_azim_v2 (h0cut y) (y*y)`;;
76
77 let tsk_hyp_new = mk_conj(GRKIBMP_concl, 
78                               mk_conj(cell3_from_ineq,tsk_hyp));;
79
80 let TSKAJXY_statement_special_case = new_definition
81    `TSKAJXY_statement_special_case <=>
82       (!V X.
83           saturated V /\
84           packing V /\
85           mcell_set V X /\
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)`;;
89
90 g (mk_imp(tsk_hyp_new,`TSKAJXY_statement_special_case`));;
91
92 let TSKAJXY_034 = Prove_by_refinement.prove_by_refinement(
93    (mk_imp(tsk_hyp_new,`TSKAJXY_statement_special_case`)),
94   (* {{{ proof *)
95   [
96    (STRIP_TAC);
97   (REWRITE_TAC[TSKAJXY_statement_special_case; mcell_set; IN_ELIM_THM]);
98   (REWRITE_TAC[IN]);
99   (REPEAT STRIP_TAC);
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]);
104     (REPEAT STRIP_TAC);
105         (MATCH_MP_TAC MEASURE_EQ_0);
106         BY((ASM_REWRITE_TAC[]));
107       (DISJ2_TAC);
108       (REWRITE_WITH `VX V X = {}`);
109         (REWRITE_TAC[VX]);
110         BY((ASM_REWRITE_TAC[]));
111       BY((REWRITE_TAC[SUM_CLAUSES]));
112     (DISJ2_TAC);
113     (REWRITE_WITH `edgeX V X = {}`);
114       (REWRITE_TAC[edgeX]);
115       (REWRITE_WITH `VX V X = {}`);
116         (REWRITE_TAC[VX]);
117         BY((ASM_REWRITE_TAC[]));
118       (ONCE_REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]);
119       BY((SET_TAC[]));
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`);
125       (ASM_REWRITE_TAC[]);
126       BY((ASM_SIMP_TAC[MCELL_EXPLICIT]));
127     (UP_ASM_TAC THEN REWRITE_TAC[mcell4]);
128     (COND_CASES_TAC);
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]);
134       (STRIP_TAC);
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`);
147           (ASM_REWRITE_TAC[]);
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`);
153             (ASM_REWRITE_TAC[]);
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);
169       (ASM_REWRITE_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]);
172         (REPEAT STRIP_TAC);
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]);
177                       (REPEAT STRIP_TAC);
178                           (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
179                           (ASM_REWRITE_TAC[]);
180                           (STRIP_TAC);
181                             BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
182                           (STRIP_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));
189                     BY((ASM_SET_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]);
194                     (REPEAT STRIP_TAC);
195                         (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u2:real^3`);
196                         (ASM_REWRITE_TAC[]);
197                         (STRIP_TAC);
198                           BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
199                         (STRIP_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));
206                   BY((ASM_SET_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]);
211                   (REPEAT STRIP_TAC);
212                       (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u3:real^3`);
213                       (ASM_REWRITE_TAC[]);
214                       (STRIP_TAC);
215                         BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
216                       (STRIP_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));
223                 BY((ASM_SET_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]);
228                 (REPEAT STRIP_TAC);
229                     (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
230                     (ASM_REWRITE_TAC[]);
231                     (STRIP_TAC);
232                       BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
233                     (STRIP_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));
240               BY((ASM_SET_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]);
245               (REPEAT STRIP_TAC);
246                   (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u3:real^3`);
247                   (ASM_REWRITE_TAC[]);
248                   (STRIP_TAC);
249                     BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
250                   (STRIP_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));
257             BY((ASM_SET_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]);
262             (REPEAT STRIP_TAC);
263                 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3`);
264                 (ASM_REWRITE_TAC[]);
265                 (STRIP_TAC);
266                   BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
267                 (STRIP_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));
274           BY((ASM_SET_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]);
285             (REPEAT LET_TAC);
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]);
289             (ASM_REWRITE_TAC[]);
290             (STRIP_TAC);
291             BY((ASM_REWRITE_TAC[]));
292           (REPEAT LET_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[]));
310       (ASM_REWRITE_TAC[]);
311       (NEW_GOAL `!u v. {u,v} IN edgeX V X ==> (#2.0 <= dist (u,v) /\ dist(u,v) <= sqrt8)`);
312         (REPEAT GEN_TAC);
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]);
316         (STRIP_TAC);
317         (MP_TAC (ASSUME `packing V`));
318         (REWRITE_TAC[packing; REAL_ARITH `#2.0 = &2`] THEN STRIP_TAC);
319         (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);
323             BY((SET_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[]));
328           (STRIP_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[]));
331           (STRIP_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);
335           BY((SET_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`));
347           (STRIP_TAC);
348             (REWRITE_WITH `dist (s,u:real^3) = radV {u0,u1,u2,u3:real^3}`);
349               (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
350               (EXPAND_TAC "s");
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);
354               BY((SET_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]);
360             (EXPAND_TAC "s");
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);
364             BY((SET_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)`);
374         (REPEAT STRIP_TAC);
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 ]));
377                   BY((ASM_ARITH_TAC));
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 ]));
380                 BY((ASM_ARITH_TAC));
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 ]));
383               BY((ASM_ARITH_TAC));
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 ]));
386             BY((ASM_ARITH_TAC));
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 ]));
389           BY((ASM_ARITH_TAC));
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 ]));
392         BY((ASM_ARITH_TAC));
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]);
397         (REPEAT STRIP_TAC);
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`]);
401           (REPEAT STRIP_TAC);
402                                         (NEW_GOAL `F`);
403                                           BY((ASM_MESON_TAC[]));
404                                         BY((ASM_MESON_TAC[]));
405                                       (REWRITE_WITH `{u,v} = {v,u:real^3}`);
406                                         BY((SET_TAC[]));
407                                       BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
408                                     (REWRITE_WITH `{u,v} = {v,u:real^3}`);
409                                       BY((SET_TAC[]));
410                                     BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
411                                   (REWRITE_WITH `{u,v} = {v,u:real^3}`);
412                                     BY((SET_TAC[]));
413                                   BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
414                                 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
415                               (NEW_GOAL `F`);
416                                 BY((ASM_MESON_TAC[]));
417                               BY((ASM_MESON_TAC[]));
418                             (REWRITE_WITH `{u,v} = {v,u:real^3}`);
419                               BY((SET_TAC[]));
420                             BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
421                           (REWRITE_WITH `{u,v} = {v,u:real^3}`);
422                             BY((SET_TAC[]));
423                           BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
424                         BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
425                       BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
426                     (NEW_GOAL `F`);
427                       BY((ASM_MESON_TAC[]));
428                     BY((ASM_MESON_TAC[]));
429                   (REWRITE_WITH `{u,v} = {v,u:real^3}`);
430                     BY((SET_TAC[]));
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[]));
435           (NEW_GOAL `F`);
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`]);
441         (REPEAT STRIP_TAC);
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[]));
448       (STRIP_TAC);
449         (EXPAND_TAC "y1");
450         (FIRST_ASSUM MATCH_MP_TAC);
451         BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
452       (STRIP_TAC);
453         (EXPAND_TAC "y2");
454         (FIRST_ASSUM MATCH_MP_TAC);
455         BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
456       (STRIP_TAC);
457         (EXPAND_TAC "y3");
458         (FIRST_ASSUM MATCH_MP_TAC);
459         BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
460       (STRIP_TAC);
461         (EXPAND_TAC "y4");
462         (FIRST_ASSUM MATCH_MP_TAC);
463         BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
464       (STRIP_TAC);
465         (EXPAND_TAC "y5");
466         (FIRST_ASSUM MATCH_MP_TAC);
467         BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
468       (STRIP_TAC);
469         (EXPAND_TAC "y6");
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));
476         (STRIP_TAC);
477           (STRIP_TAC);
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]));
488           (STRIP_TAC);
489           (NEW_GOAL `NULLSET X`);
490             (MATCH_MP_TAC NEGLIGIBLE_SUBSET);
491             (EXISTS_TAC `affine hull {u0, u1, u2, u3:real^3}`);
492             (STRIP_TAC);
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]);
501             (COND_CASES_TAC);
502               BY((ASM_REWRITE_TAC[set_of_list; CONVEX_HULL_SUBSET_AFFINE_HULL]));
503             BY((SET_TAC[]));
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");
508         BY((REWRITE_TAC[]));
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[]));
527     (STRIP_TAC);
528     (NEW_GOAL `F`);
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[]));
538       (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`]);
544       BY((SET_TAC[]));
545     (REWRITE_TAC[gammaX]);
546     (MATCH_MP_TAC (REAL_ARITH `b = &0 /\ c = &0 /\ &0 <= a ==> a - b + c >= &0`));
547     (REPEAT STRIP_TAC);
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);
556   DISCH_TAC;
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);
561     BY(MESON_TAC[]);
562   REPEAT (FIRST_X_ASSUM_ST `gamma4fgcy` kill);
563   COMMENT "end of insert";
564   (NEW_GOAL `X = mcell3 V ul`);
565     (ASM_REWRITE_TAC[]);
566     BY((ASM_SIMP_TAC[MCELL_EXPLICIT]));
567   (UP_ASM_TAC THEN REWRITE_TAC[mcell3]);
568   (COND_CASES_TAC);
569     (STRIP_TAC);
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[]);
586       BY((ARITH_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[]);
591       BY((ARITH_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}`);
595       (STRIP_TAC);
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);
602       BY((ASM_SET_TAC[]));
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]);
605     (STRIP_TAC);
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)`);
631       (REPEAT STRIP_TAC);
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 ]));
634                 BY((ASM_ARITH_TAC));
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 ]));
637               BY((ASM_ARITH_TAC));
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 ]));
640             BY((ASM_ARITH_TAC));
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 ]));
643           BY((ASM_ARITH_TAC));
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 ]));
646         BY((ASM_ARITH_TAC));
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 ]));
649       BY((ASM_ARITH_TAC));
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[]));
668     (STRIP_TAC);
669     (NEW_GOAL `~coplanar {u0,u1,u2,s:real^3}`);
670       (ONCE_REWRITE_TAC[GSYM COPLANAR_AFFINE_HULL_COPLANAR]);
671       (STRIP_TAC);
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`);
683         (NEW_GOAL `F`);
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[]));
688       BY((ASM_ARITH_TAC));
689     (NEW_GOAL `~(u0 = s:real^3) /\ ~(u1 = s) /\ ~(u2 = s)`);
690       (REPEAT STRIP_TAC);
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 ]));
693           BY((ASM_ARITH_TAC));
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 ]));
696         BY((ASM_ARITH_TAC));
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 ]));
699       BY((ASM_ARITH_TAC));
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`];
705     ASM_REWRITE_TAC[];
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]);
712     ASM_REWRITE_TAC[];
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]);
723       BY(MESON_TAC[]);
724     INTRO_TAC Collect_geom.RADV_FORMULAR [`u0`;`u1`;`u2`];
725     REWRITE_TAC[Collect_geom.dist3];
726     ANTS_TAC;
727       BY(ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);
728     ASM_REWRITE_TAC[];
729     FIRST_X_ASSUM_ST `hl vl` MP_TAC;
730     EXPAND_TAC "vl";
731     TYPIFY `hl (truncate_simplex 2 ul) = radV {u0,u1,u2}` ENOUGH_TO_SHOW_TAC;
732       BY(REAL_ARITH_TAC);
733     REWRITE_TAC[Pack_defs.HL];
734     AP_TERM_TAC;
735     GMATCH_SIMP_TAC Bump.SET_OF_LIST_TRUNCATE_2;
736     ASM_REWRITE_TAC[Bump.EL_EXPLICIT];
737     REWRITE_TAC[LENGTH];
738     BY(ARITH_TAC);
739   BY(ASM_MESON_TAC[NEGLIGIBLE_EMPTY])
740   ]);;
741   (* }}} *)
742
743
744 (* ======================================================================== *)
745
746 (* OLD SCRIPT FOLLOWS *)
747
748
749 end;;