1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
13 Remaining cases of TSKAJXY.
17 flyspeck_needs "usr/thales/hales_tactic.hl";;
19 module Tskajxy = struct
23 let GAMMAX_NULLSET = prove_by_refinement(
24 `!V f X ul k. saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell k V ul) /\ NULLSET X ==>
28 REPEAT WEAK_STRIP_TAC;
29 REWRITE_TAC[Pack_defs.gammaX];
30 TYPIFY `total_solid V X = &0` (C SUBGOAL_THEN SUBST1_TAC);
31 REWRITE_TAC[Pack_defs.total_solid];
32 TYPIFY `(VX V X = {})` (C SUBGOAL_THEN SUBST1_TAC);
34 MATCH_MP_TAC Bump.VX_EMPTY;
36 BY(REWRITE_TAC[SUM_CLAUSES]);
37 TYPIFY `(edgeX V X = {})` (C SUBGOAL_THEN SUBST1_TAC);
39 MATCH_MP_TAC Bump.RIJRIED;
41 REWRITE_TAC[SUM_CLAUSES];
42 TYPIFY `vol X = &0` (C SUBGOAL_THEN SUBST1_TAC);
43 BY(ASM_MESON_TAC[volume_props]);
48 let GAMMAX_MCELL1 = prove_by_refinement(
49 `!V X ul. saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell1 V ul) /\ ~(NULLSET X) ==>
50 gammaX V X lmfun = vol X - (&2 * mm1 /pi) * sol (EL 0 ul) X`,
53 REWRITE_TAC[Pack_defs.gammaX];
54 REPEAT WEAK_STRIP_TAC;
55 TYPIFY `edgeX V X = {}` (C SUBGOAL_THEN SUBST1_TAC);
56 BY(ASM_MESON_TAC[Bump.EDGE_IMP_K2;Bump.MCELL1;arith `1 <= 1`]);
57 REWRITE_TAC[SUM_CLAUSES;Pack_defs.total_solid;arith `x + y* &0 = x`];
59 TYPIFY `VX V X = {EL 0 ul}` ENOUGH_TO_SHOW_TAC;
60 DISCH_THEN SUBST1_TAC;
61 BY(REWRITE_TAC[SUM_SING]);
63 MATCH_MP_TAC SUBSET_ANTISYM;
65 MATCH_MP_TAC SUBSET_TRANS;
66 TYPIFY `V INTER X` EXISTS_TAC;
68 MATCH_MP_TAC Bump.HDTFNFZ_SUBSET;
69 BY(ASM_MESON_TAC[Bump.MCELL1]);
71 MATCH_MP_TAC Bump.V_CELL1_SINGLE;
72 BY(ASM_REWRITE_TAC[]);
73 GMATCH_SIMP_TAC Hdtfnfz.HDTFNFZ;
74 REWRITE_TAC[SUBSET;IN_SING;IN_INTER];
76 BY(ASM_MESON_TAC[Bump.MCELL1]);
77 REPEAT WEAK_STRIP_TAC;
80 MATCH_MP_TAC Marchal_cells_3.HD_IN_MCELL;
81 BY(ASM_MESON_TAC[NEGLIGIBLE_EMPTY;arith `~(1=0)`;Bump.MCELL1]);
82 INTRO_TAC Packing3.BARV_SUBSET [`V`;`3`;`ul`];
83 GMATCH_SIMP_TAC Bump.set_of_list4;
84 REWRITE_TAC[EL;SUBSET;IN_INSERT;NOT_IN_EMPTY];
85 BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3 + 1 = 4`])
89 let MCELL2_VX_PROPS = prove_by_refinement(
90 `!V X ul. saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell2 V ul) /\ ~(NULLSET X) ==>
91 (VX V X = {EL 0 ul,EL 1 ul}) /\ ~(EL 0 ul = EL 1 ul) /\ (edgeX V X = {{EL 0 ul, EL 1 ul}})`,
94 REWRITE_TAC[Pack_defs.gammaX];
95 REPEAT WEAK_STRIP_TAC;
96 TYPIFY `VX V X = {EL 0 ul, EL 1 ul}` (C SUBGOAL_THEN MP_TAC);
97 GMATCH_SIMP_TAC Bump.HDTFNFZ_ALT;
99 BY(ASM_MESON_TAC[Bump.MCELL2]);
100 ASM_REWRITE_TAC[Bump.MCELL2];
101 GMATCH_SIMP_TAC Lepjbdj.LEPJBDJ;
102 ASM_REWRITE_TAC[arith `1 <= 2 /\ 2 <= 4 /\ 2 -1 = 1`];
104 BY(ASM_MESON_TAC[NEGLIGIBLE_EMPTY;Bump.MCELL2]);
105 MATCH_MP_TAC Bump.SET_OF_LIST_TRUNCATE_1;
106 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `2 <= 3 + 1`]);
108 TYPIFY `~(EL 0 ul = EL 1 ul)` (C SUBGOAL_THEN MP_TAC);
109 INTRO_TAC Marchal_cells_3.BARV_CARD_LEMMA [`V`;`ul`;`3`];
110 ASM_REWRITE_TAC[arith ` 3 + 1 = 4`];
111 GMATCH_SIMP_TAC Bump.set_of_list4;
113 BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3 + 1 = 4`]);
114 BY(MESON_TAC[Marchal_cells_2_new.CARD4_IMP_DISTINCT]);
116 TYPIFY `edgeX V X = {{EL 0 ul, EL 1 ul}}` (C SUBGOAL_THEN MP_TAC);
117 REWRITE_TAC[Pack_defs.edgeX];
118 REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ];
119 TYPIFY `!w. VX V X w <=> w IN VX V X` (C SUBGOAL_THEN (unlist REWRITE_TAC));
122 ASM_REWRITE_TAC[SUBSET;IN_INSERT;IN_SING;IN_ELIM_THM];
123 REBIND_TAC (`x:real^3->bool`,"A");
125 REPEAT WEAK_STRIP_TAC;
128 BY(ASM_REWRITE_TAC[] THEN SET_TAC[]);
132 FIRST_X_ASSUM MP_TAC;
138 let GAMMAX_MCELL2 = prove_by_refinement(
139 `!V X ul. saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell2 V ul) /\ ~(NULLSET X) ==>
140 gammaX V X lmfun = vol X - (&2 * mm1 /pi) * (sol (EL 0 ul) X + sol (EL 1 ul) X) +
141 (&8*mm2/ pi) * lmfun (hl [EL 0 ul;EL 1 ul]) * dihX V X (EL 0 ul,EL 1 ul)`,
144 REWRITE_TAC[Pack_defs.gammaX];
145 REPEAT WEAK_STRIP_TAC;
146 TYPIFY `X IN mcell_set V` (C SUBGOAL_THEN ASSUME_TAC);
147 REWRITE_TAC[Pack_defs.mcell_set;Bump.MCELL2;IN_ELIM_THM];
148 BY(ASM_MESON_TAC[IN;Bump.MCELL2]);
149 INTRO_TAC MCELL2_VX_PROPS [`V`;`X`;`ul`];
151 BY(ASM_REWRITE_TAC[]);
152 REPEAT WEAK_STRIP_TAC;
153 TYPIFY `total_solid V X = (sol (EL 0 ul) X + sol (EL 1 ul) X)` (C SUBGOAL_THEN SUBST1_TAC);
154 ASM_REWRITE_TAC[Pack_defs.total_solid];
156 GMATCH_SIMP_TAC Geomdetail.SUM_DIS2;
157 BY(ASM_REWRITE_TAC[]);
158 ASM_REWRITE_TAC[IN_SING;SUM_SING];
159 GMATCH_SIMP_TAC Marchal_cells_3.BETA_PAIR_THM;
161 REPEAT WEAK_STRIP_TAC;
162 REWRITE_TAC[Pack_defs.HL;Bump.set_of_list2_explicit];
163 TYPIFY `{v,u} = {u,v}` (C SUBGOAL_THEN SUBST1_TAC);
169 MATCH_MP_TAC Marchal_cells_3.DIHX_SYM;
170 BY(ASM_MESON_TAC[IN_SING;IN]);
176 (* renamed from RCONE_GT_BALL_PLANE *)
178 let RCONE_GT_HYPERPLANE = prove_by_refinement(
179 `!v0 v1 b t (p:real^A) r.
180 p dot (v1 - v0) = b /\ ~(v1 = v0) /\ (&0 < t) /\ (b - v0 dot (v1 - v0) = r * t * dist(v1,v0)) ==>
181 (p IN rcone_gt v0 v1 t <=> p IN ball (v0,r))`,
184 REWRITE_TAC[Sphere.rcone_gt;Sphere.rconesgn;ball;IN_ELIM_THM];
185 REPEAT WEAK_STRIP_TAC;
186 TYPIFY `(p - v0) dot (v1 - v0) = p dot (v1 - v0) - v0 dot (v1 - v0)` (C SUBGOAL_THEN SUBST1_TAC);
187 BY(VECTOR_ARITH_TAC);
189 REWRITE_TAC[arith `dp * d * t > r * t * d <=> (&0 < d * t * (dp - r))`];
190 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
192 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
193 ASM_REWRITE_TAC[GSYM DIST_NZ];
194 BY(MESON_TAC[DIST_SYM;arith `&0 < x - y <=> y < x`])
198 let RCONE_GE_HYPERPLANE = prove_by_refinement(
199 `!v0 v1 b t (p:real^A) r.
200 p dot (v1 - v0) = b /\ ~(v1 = v0) /\ (&0 < t) /\ (b - v0 dot (v1 - v0) = r * t * dist(v1,v0)) ==>
201 (p IN rcone_ge v0 v1 t <=> p IN cball (v0,r))`,
204 REWRITE_TAC[Sphere.rcone_ge;Sphere.rconesgn;cball;IN_ELIM_THM];
205 REPEAT WEAK_STRIP_TAC;
206 TYPIFY `(p - v0) dot (v1 - v0) = p dot (v1 - v0) - v0 dot (v1 - v0)` (C SUBGOAL_THEN SUBST1_TAC);
207 BY(VECTOR_ARITH_TAC);
209 REWRITE_TAC[arith `dp * d * t >= r * t * d <=> (&0 <= d * t * (dp - r))`];
210 GMATCH_SIMP_TAC REAL_LE_MUL_EQ;
212 GMATCH_SIMP_TAC REAL_LE_MUL_EQ;
213 ASM_REWRITE_TAC[GSYM DIST_NZ];
214 BY(MESON_TAC[DIST_SYM;arith `&0 <= x - y <=> y <= x`])
218 (* renamed from BALL_DIFF_RCONE_GE *)
220 let BALL_DIFF_RCONE_GT = prove_by_refinement(
221 `!u0 u1 (p:real^A) a r.
222 p IN ball(u0,r) DIFF rcone_gt u0 u1 a /\ &0 <= a ==>
223 p dot (u1 - u0) <= u0 dot (u1 - u0) + r * a * dist(u1,u0)`,
226 REWRITE_TAC[Sphere.rcone_gt;Sphere.rconesgn;ball;IN_ELIM_THM;IN_DIFF;arith `~(x > y) <=> (x <= y)`];
227 REPEAT WEAK_STRIP_TAC;
228 FIRST_X_ASSUM_ST `dot` MP_TAC;
229 TYPIFY `(p - u0) dot (u1 - u0) = p dot (u1 - u0) - u0 dot (u1 - u0)` (C SUBGOAL_THEN SUBST1_TAC);
230 BY(VECTOR_ARITH_TAC);
231 TYPIFY `dist (p,u0) * dist (u1,u0) * a <= r * a * dist(u1,u0)` ENOUGH_TO_SHOW_TAC;
233 MATCH_MP_TAC (arith `&0 <= (r - dp) * d1 * a ==> dp * d1 * a <= r * a * d1`);
234 GMATCH_SIMP_TAC REAL_LE_MUL;
236 BY(ASM_MESON_TAC [arith `d < r ==> &0 <= r - d`;DIST_SYM]);
237 GMATCH_SIMP_TAC REAL_LE_MUL;
239 BY(REWRITE_TAC[DIST_POS_LE])
243 (* renamed from BALL_DIFF_RCONE_GT_BISECTOR *)
245 let BALL_DIFF_RCONE_GT_BISECTOR = prove_by_refinement(
246 `!u0 u1 (p:real^A) r h.
247 p IN ball(u0,r) DIFF rcone_gt u0 u1 (h/r) /\ &2 * h = dist(u1,u0) /\ &0 < r ==>
248 dist(p,u0) <= dist(p,u1)`,
251 REPEAT WEAK_STRIP_TAC;
252 INTRO_TAC BALL_DIFF_RCONE_GT [`u0`;`u1`;`p`;`h/r`;`r`];
255 GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
256 ASM_REWRITE_TAC[arith `&0 * x = &0`];
257 ONCE_REWRITE_TAC[arith `&0 <= h <=> &0 <= &2 * h`];
258 BY(ASM_MESON_TAC[DIST_POS_LE]);
259 TYPIFY `r * h / r * dist(u1,u0) = (dist(u1,u0)) pow 2 / &2` (C SUBGOAL_THEN SUBST1_TAC);
260 FIRST_X_ASSUM (SUBST1_TAC o SYM);
261 Calc_derivative.CALC_ID_TAC;
262 BY((FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
263 REWRITE_TAC[Leaf_cell.DIST_LE_HALF_PLANE];
264 REWRITE_TAC[Collect_geom.DIST_POW2_DOT];
265 MATCH_MP_TAC (arith `&2 * a + c - b - &2 * b1 = &0 ==> (a <= b1 + b / &2 ==> &0 <= c)`);
270 let MCELL1_EXPLICIT = prove_by_refinement(
271 `!V X ul. saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell1 V ul) /\ ~(NULLSET X) ==>
272 (X = rogers V ul INTER cball (HD ul,sqrt (&2)) DIFF
273 rcone_gt (HD ul) (HD (TL ul)) (hl (truncate_simplex 1 ul) / sqrt (&2)))`,
276 REWRITE_TAC[Pack_defs.mcell1];
277 REPEAT WEAK_STRIP_TAC;
278 TYPIFY `sqrt (&2) <= hl ul` (C SUBGOAL_THEN ASSUME_TAC);
280 FIRST_X_ASSUM_ST `rogers` MP_TAC;
282 BY(ASM_MESON_TAC[NEGLIGIBLE_EMPTY]);
283 FIRST_X_ASSUM_ST `rogers` MP_TAC;
284 BY(ASM_REWRITE_TAC[])
288 let MCELL1_VOL_RESTRICT = prove_by_refinement(
289 `!V X ul. saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell1 V ul) /\ ~(NULLSET X) ==>
290 vol X = vol (X INTER ball(EL 0 ul, sqrt(&2)))`,
293 REPEAT WEAK_STRIP_TAC;
294 TYPIFY `measurable X /\ measurable (X INTER ball(EL 0 ul, sqrt(&2)))` (C SUBGOAL_THEN ASSUME_TAC);
296 BY(ASM_MESON_TAC[Urrphbz1.MEASURABLE_MCELL;Bump.MCELL1]);
298 MATCH_MP_TAC MEASURABLE_INTER;
299 BY(ASM_REWRITE_TAC[MEASURABLE_BALL]);
300 MATCH_MP_TAC Vol1.VOLUME_PROPS_SDIFF;
301 ASM_REWRITE_TAC[SDIFF];
302 MATCH_MP_TAC (CONJUNCT2 NULLSET_RULES);
304 TYPIFY `!x. (x = {}) ==> NULLSET x` ENOUGH_TO_SHOW_TAC;
305 DISCH_THEN MATCH_MP_TAC;
307 BY(MESON_TAC[NEGLIGIBLE_EMPTY]);
308 TYPIFY `X DIFF (X INTER ball(EL 0 ul,sqrt(&2))) SUBSET cball (EL 0 ul,sqrt(&2)) DIFF ball(EL 0 ul,sqrt(&2))` (C SUBGOAL_THEN ASSUME_TAC);
309 TYPIFY `X SUBSET cball(EL 0 ul,sqrt(&2))` ENOUGH_TO_SHOW_TAC;
311 INTRO_TAC MCELL1_EXPLICIT [`V`;`X`;`ul`];
313 DISCH_THEN SUBST1_TAC;
316 MATCH_MP_TAC NEGLIGIBLE_SUBSET;
317 FIRST_X_ASSUM MP_TAC;
318 TYPIFY `cball (EL 0 ul,sqrt(&2)) DIFF ball(EL 0 ul,sqrt(&2)) = {p | dist(EL 0 ul,p) = sqrt(&2)}` (C SUBGOAL_THEN SUBST1_TAC);
319 REWRITE_TAC[EXTENSION;cball;ball;IN_ELIM_THM;IN_DIFF];
323 TYPIFY `{p | dist(EL 0 ul,p) = sqrt(&2) }` EXISTS_TAC;
325 BY(REWRITE_TAC[NEGLIGIBLE_SPHERE])
329 let MCELL1_SOL_RESTRICT = prove_by_refinement(
330 `!V X ul. saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell1 V ul) /\ ~(NULLSET X) ==>
331 sol (EL 0 ul) X = sol (EL 0 ul) (X INTER ball(EL 0 ul, sqrt(&2)))`,
334 REPEAT WEAK_STRIP_TAC;
335 INTRO_TAC Urrphbz2.URRPHBZ2 [`V`;`ul`;`1`;`EL 0 ul`];
338 INTRO_TAC Packing3.BARV_SUBSET [`V`;`3`;`ul`];
340 GMATCH_SIMP_TAC Bump.set_of_list4;
343 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`]);
344 REWRITE_TAC[Sphere.eventually_radial];
345 REPEAT WEAK_STRIP_TAC;
346 TYPIFY `?r'. (&0 < r' /\ r' <= r /\ r' <= sqrt(&2))` (C SUBGOAL_THEN ASSUME_TAC);
347 EXISTS_TAC `if (r <= sqrt(&2)) then r else sqrt(&2)`;
349 BY(ASM_SIMP_TAC[arith `r > &0 ==> &0 < r`;arith `r <= r`]);
350 ASM_SIMP_TAC[arith `s <= s`;arith `~(r <= s) ==> (s <= r)`];
351 GMATCH_SIMP_TAC REAL_LT_RSQRT;
353 FIRST_X_ASSUM MP_TAC THEN WEAK_STRIP_TAC;
354 INTRO_TAC Conforming.RADIAL_NORM_CO [`r`;`r'`;`EL 0 ul`;`X`];
355 ASM_REWRITE_TAC[GSYM Marchal_cells_2_new.RADIAL_VS_RADIAL_NORM;Bump.MCELL1;NORMBALL_BALL];
356 REPEAT WEAK_STRIP_TAC;
357 INTRO_TAC Vol1.sol [`EL 0 ul`;`X`;`r'`];
358 INTRO_TAC Vol1.sol [`EL 0 ul`;`X INTER ball (EL 0 ul,sqrt(&2))`;`r'`];
359 ASM_REWRITE_TAC[arith `r' > &0 <=> &0 < r'`;NORMBALL_BALL;INTER_ASSOC;GSYM Marchal_cells_2_new.RADIAL_VS_RADIAL_NORM;Bump.MCELL1];
360 TYPIFY ` ball(EL 0 ul,sqrt(&2)) INTER ball(EL 0 ul,r') = ball(EL 0 ul,r')` (C SUBGOAL_THEN SUBST1_TAC);
361 REWRITE_TAC[ball;EXTENSION;IN_ELIM_THM;IN_INTER];
362 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
363 TYPIFY `measurable (mcell 1 V ul INTER ball (EL 0 ul,r'))` (C SUBGOAL_THEN ((unlist ASM_REWRITE_TAC)));
364 MATCH_MP_TAC MEASURABLE_INTER;
366 BY(ASM_REWRITE_TAC[MEASURABLE_BALL]);
367 BY(ASM_MESON_TAC[Urrphbz1.MEASURABLE_MCELL;Bump.MCELL1]);
372 let CONV_CONVEX_HULL = prove_by_refinement(
373 `!(s:real^A->bool). conv s = convex hull s`,
376 BY(REWRITE_TAC[Geomdetail.conv;aff_ge_def;CONVEX_HULL_AFF_GE])
380 let CONVEX_HULL_4_AFF_GE = prove_by_refinement(
381 `!(w0:real^3) w1 w2 w3. ~coplanar {w0,w1, w2,w3} ==>
382 (convex hull {w0,w1,w2,w3} = aff_ge {w0} {w1,w2,w3} INTER aff_ge {w1,w2,w3} {w0})`,
385 REPEAT WEAK_STRIP_TAC;
386 INTRO_TAC DIMINDEX_3 [];
388 INTRO_TAC Collect_geom2.ARIKWRQ [`w0`;`w1`;`w2`;`w3`];
389 REWRITE_TAC[LET_DEF;LET_END_DEF;CONV_CONVEX_HULL];
390 TYPIFY `~coplanar_alt {w0,w1,w2,w3}` (C SUBGOAL_THEN ASSUME_TAC);
391 BY(ASM_MESON_TAC[Leaf_cell.coplanar_eq_coplanar_alt;arith `2 <= 3`]);
393 TYPIFY `CARD {w0,w1,w2,w3} = 4` (C SUBGOAL_THEN ASSUME_TAC);
394 MATCH_MP_TAC Collect_geom2.NOT_COPLANAR_IMP_CARD4;
395 BY(ASM_REWRITE_TAC[]);
397 DISCH_THEN SUBST1_TAC;
398 TYPIFY `({w0,w1,w2,w3} DIFF {w0} = {w1,w2,w3}) /\ ({w0,w1,w2,w3} DIFF {w1} = {w0,w2,w3}) /\ ({w0,w1,w2,w3} DIFF {w2} = {w0,w3,w1} ) /\ ({w0,w1,w2,w3} DIFF {w3} = {w0,w1,w2})` (C SUBGOAL_THEN (unlist REWRITE_TAC));
399 FIRST_X_ASSUM (MP_TAC o (MATCH_MP Leaf_cell.CARD4_ALL_DISTINCT));
401 INTRO_TAC Cfyxfty.inter_aff_ge_3_1_is_aff_ge_1_3 [`w0`;`w1`;`w2`;`w3`];
407 let RADIAL_ALT = prove_by_refinement(
408 `!(x:real^A) r A. radial r x A <=> (A SUBSET ball(x,r) /\
409 (!y t. &0 < t /\ y IN A /\ x + t % (y- x) IN ball(x,r) ==> x + t % (y - x)
413 REPEAT WEAK_STRIP_TAC;
414 REWRITE_TAC[Sphere.radial];
415 TYPIFY `A SUBSET ball(x,r)` ASM_CASES_TAC;
417 MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a = b)`);
419 REPEAT WEAK_STRIP_TAC;
420 FIRST_X_ASSUM (C INTRO_TAC [`y - (x:real^A)`]);
422 TYPIFY `x + y - x = (y:real^A)` (C SUBGOAL_THEN SUBST1_TAC);
423 BY(VECTOR_ARITH_TAC);
424 BY(ASM_REWRITE_TAC[]);
425 DISCH_THEN (C INTRO_TAC [`t`]);
426 DISCH_THEN MATCH_MP_TAC;
427 ASM_SIMP_TAC[arith `&0 < t ==> t > &0`];
428 FIRST_X_ASSUM MP_TAC;
429 REWRITE_TAC[ball;IN_ELIM_THM;dist];
430 TYPIFY `x - (x + t % (y - x)) = (-- t) % (y - x)` (C SUBGOAL_THEN SUBST1_TAC);
431 BY(VECTOR_ARITH_TAC);
432 REWRITE_TAC[NORM_MUL];
433 BY(ASM_SIMP_TAC[arith `&0 < t ==> abs (-- t) = t`]);
434 COMMENT "second direction";
435 REPEAT WEAK_STRIP_TAC;
436 FIRST_X_ASSUM_ST `ball` (C INTRO_TAC [`x + (u:real^A)`;`t`]);
437 TYPIFY `(x + u) - x = (u:real^A)` (C SUBGOAL_THEN SUBST1_TAC);
438 BY(VECTOR_ARITH_TAC);
439 DISCH_THEN MATCH_MP_TAC;
440 ASM_SIMP_TAC[arith `t > &0 ==> &0 < t`];
441 FIRST_X_ASSUM MP_TAC;
442 REWRITE_TAC[ball;IN_ELIM_THM;dist;varith `x - (x + t % u) = (-- t) % (u:real^A)`;NORM_MUL];
443 BY(ASM_SIMP_TAC[arith `t > &0 ==> abs(-- t) = t`]);
444 BY(ASM_REWRITE_TAC[])
448 let CONVEX_HULL_SCALE = prove_by_refinement(
449 `!(w0:real^3) w1 w2 w3 w t. ~coplanar {w0,w1,w2,w3} /\ w IN convex hull {w0,w1,w2,w3} /\ &0 <= t /\
450 (w0 + t % (w - w0) IN aff_ge {w1,w2,w3} {w0} ) ==>
451 (w0 + t % (w - w0) IN convex hull {w0,w1,w2,w3})`,
454 REPEAT WEAK_STRIP_TAC;
455 ASM_SIMP_TAC[CONVEX_HULL_4_AFF_GE];
456 REPEAT WEAK_STRIP_TAC;
457 ASM_SIMP_TAC[CONVEX_HULL_4_AFF_GE];
458 ASM_REWRITE_TAC[IN_INTER];
459 TYPIFY `DISJOINT {w0} {w1,w2,w3}` (C SUBGOAL_THEN ASSUME_TAC);
460 BY(ASM_MESON_TAC[Planarity.notcoplanar_disjoints]);
461 ASM_SIMP_TAC[ Planarity.AFF_GE_1_3];
462 REWRITE_TAC[IN_ELIM_THM];
463 FIRST_X_ASSUM_ST `convex` MP_TAC;
464 REWRITE_TAC[Marchal_cells_2_new.CONVEX_HULL_4;IN_ELIM_THM];
465 REPEAT WEAK_STRIP_TAC;
467 GEXISTL_TAC [`&1 + t * (u - &1)`;`t * v`;`t * w'`;`t * z`];
468 GMATCH_SIMP_TAC REAL_LE_MUL;
469 GMATCH_SIMP_TAC REAL_LE_MUL;
470 GMATCH_SIMP_TAC REAL_LE_MUL;
473 FIRST_X_ASSUM_ST `&1` MP_TAC;
474 BY(CONV_TAC REAL_RING);
479 let IMAGE_4_EXPLICIT = prove_by_refinement(
480 `!(f:num->B). { f i | i <= 3 } = {f 0 , f 1 ,f 2, f 3}`,
483 REPEAT WEAK_STRIP_TAC;
484 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_INSERT;NOT_IN_EMPTY];
485 REWRITE_TAC[arith `i <= 3 <=> (i = 0 \/ i = 1 \/ i = 2 \/ i = 3)`];
490 let NULLSET_MCELL1 = prove_by_refinement(
491 `!V ul. packing V /\ saturated V /\ ul IN barV V 3 /\ ~NULLSET (mcell1 V ul) ==> ~NULLSET (rogers V ul)`,
494 REPEAT WEAK_STRIP_TAC;
495 INTRO_TAC MCELL1_EXPLICIT [`V`;`mcell1 V ul`;`ul`];
498 BY(ASM_MESON_TAC[IN]);
500 TYPIFY `mcell1 V ul SUBSET rogers V ul` (C SUBGOAL_THEN ASSUME_TAC);
501 FIRST_X_ASSUM MP_TAC;
503 BY(ASM_MESON_TAC[NEGLIGIBLE_SUBSET])
507 let NOT_COPLANAR_OMEGA_LIST_N = prove_by_refinement(
508 `!V ul. packing V /\ saturated V /\ ul IN barV V 3 /\ ~NULLSET (mcell1 V ul) ==>
509 ~coplanar { omega_list_n V ul i | i <= 3}`,
512 REWRITE_TAC[coplanar];
513 REWRITE_TAC[IMAGE_4_EXPLICIT];
514 REPEAT WEAK_STRIP_TAC;
515 INTRO_TAC NULLSET_MCELL1 [`V`;`ul`];
517 GMATCH_SIMP_TAC Marchal_cells_2_new.ROGERS_EXPLICIT;
518 REWRITE_TAC[GSYM Sphere.OMEGA_LIST_N];
521 BY(ASM_MESON_TAC[IN]);
522 TYPED_ABBREV_TAC `s = {omega_list_n V ul 0, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`;
523 TYPIFY `convex hull s SUBSET affine hull {u,v,w}` (C SUBGOAL_THEN ASSUME_TAC);
524 MATCH_MP_TAC SUBSET_TRANS;
525 TYPIFY `affine hull s` EXISTS_TAC;
526 REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL];
527 INTRO_TAC Marchal_cells_2_new.AFFINE_SUBSET_KY_LEMMA [`s`;`affine hull {u,v,w}`];
528 REWRITE_TAC[Planarity.AFFINE_HULL_AFFINE_EQ];
529 DISCH_THEN MATCH_MP_TAC;
530 BY(ASM_REWRITE_TAC[]);
531 TYPIFY `convex hull s SUBSET affine hull {u,v,w}` ENOUGH_TO_SHOW_TAC;
532 BY(ASM_MESON_TAC[NEGLIGIBLE_AFFINE_HULL_3;NEGLIGIBLE_SUBSET]);
533 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[])
537 let NOT_COPLANAR_R3 = prove_by_refinement(
538 `!s. ~coplanar s ==> affine hull s = (:real^3)`,
541 REPEAT WEAK_STRIP_TAC;
542 INTRO_TAC AFF_DIM_EQ_FULL [`s`];
543 INTRO_TAC AFF_DIM_LE_UNIV [`s`];
544 REWRITE_TAC[DIMINDEX_3];
545 BY(ASM_MESON_TAC[Rogers.AFF_DIM_LE_2_IMP_COPLANAR;INT_ARITH `~(x <= int_of_num 2) /\ x <= &3 ==> x = &3`])
549 let BARV_DISTINCT = prove_by_refinement(
550 `!V ul. packing V /\ saturated V /\ ul IN barV V 1 ==>
551 ~(EL 0 ul = EL 1 ul)`,
554 REPEAT WEAK_STRIP_TAC;
555 INTRO_TAC Packing3.TRUNCATE_SIMPLEX_BARV [`V`;`0`;`1`;`ul`];
557 BY(ASM_MESON_TAC[IN;arith `0 <= 1`]);
558 FIRST_X_ASSUM_ST `barV` MP_TAC;
559 REWRITE_TAC[Sphere.BARV;IN;Sphere.VORONOI_NONDG];
560 REWRITE_TAC[Sphere.VORONOI_LIST;Sphere.VORONOI_SET];
561 REPEAT WEAK_STRIP_TAC;
562 (FIRST_X_ASSUM (C INTRO_TAC [`truncate_simplex 0 ul`]));
563 (FIRST_X_ASSUM (C INTRO_TAC [`ul`]));
564 ASM_REWRITE_TAC[Packing3.INITIAL_SUBLIST_REFL;arith `0 < 1 + 1 /\ 0 < 0 + 1 /\ 1 + 1 < 5 /\ 0 + 1 < 5`];
565 REWRITE_TAC[arith `1 + 1 = 2 /\ 0 + 1 = 1`];
566 TYPIFY `set_of_list (truncate_simplex 0 ul) = set_of_list ul` ENOUGH_TO_SHOW_TAC;
567 DISCH_THEN SUBST1_TAC;
569 GMATCH_SIMP_TAC Packing3.TRUNCATE_0_EQ_HEAD;
570 REWRITE_TAC[set_of_list];
571 GMATCH_SIMP_TAC Bump.set_of_list2;
572 FIRST_X_ASSUM SUBST1_TAC;
573 FIRST_X_ASSUM SUBST1_TAC;
574 FIRST_X_ASSUM (SUBST1_TAC o GSYM);
575 REWRITE_TAC[arith `1 + 1 = 2 /\ 1 <= 1 + 1`;EL];
580 let OMEGA_LIST_BISECTOR = prove_by_refinement(
581 `!V ul. packing V /\ saturated V /\ ul IN barV V 3 /\ ~NULLSET (mcell1 V ul) ==>
582 aff_ge {omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3} {EL 0 ul} =
583 bis_le (EL 0 ul) (EL 1 ul)`,
586 REWRITE_TAC[Sphere.bis_le;EXTENSION;IN_ELIM_THM];
587 REPEAT WEAK_STRIP_TAC;
588 INTRO_TAC NOT_COPLANAR_OMEGA_LIST_N [`V`;`ul`];
590 BY(ASM_REWRITE_TAC[]);
591 ASM_REWRITE_TAC[IMAGE_4_EXPLICIT];
592 REWRITE_TAC[Sphere.OMEGA_LIST_N;GSYM EL];
594 GMATCH_SIMP_TAC Cfyxfty.AFF_GE_3_1;
596 ONCE_REWRITE_TAC[DISJOINT_SYM];
597 BY(ASM_MESON_TAC[Planarity.notcoplanar_disjoints]);
599 REWRITE_TAC[IN_ELIM_THM];
600 TYPIFY `!t1 t2 t3 t4. t1 + t2 + t3 + t4 = &1 /\ x = t1 % omega_list_n V ul 1 + t2 % omega_list_n V ul 2 + t3 % omega_list_n V ul 3 + t4 % EL 0 ul ==> (&0 <= t4 <=> dist(x,EL 0 ul) <= dist(x, EL 1 ul))` ENOUGH_TO_SHOW_TAC;
601 REPEAT WEAK_STRIP_TAC;
602 MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a = b)`);
604 REPEAT WEAK_STRIP_TAC;
607 FIRST_X_ASSUM_ST `coplanar` MP_TAC;
608 TYPIFY `!a b c d. {a,b,c,d} = {b,c,d,(a:real^3)}` (C SUBGOAL_THEN (unlist ONCE_REWRITE_TAC));
610 DISCH_THEN (MP_TAC o (MATCH_MP NOT_COPLANAR_R3));
611 REWRITE_TAC[Collect_geom2.AFFINE_HULL_4;EXTENSION;IN_UNIV;IN_ELIM_THM];
613 REPEAT WEAK_STRIP_TAC;
614 TYPIFY `dist(omega_list_n V ul 1,EL 0 ul) = dist(omega_list_n V ul 1,EL 1 ul) /\ dist(omega_list_n V ul 2,EL 0 ul) = dist(omega_list_n V ul 2,EL 1 ul) /\ dist(omega_list_n V ul 3,EL 0 ul) = dist(omega_list_n V ul 3,EL 1 ul)` (C SUBGOAL_THEN ASSUME_TAC);
615 INTRO_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN [`V`;`ul`;`3`;`1`];
617 FIRST_ASSUM (C INTRO_TAC [`1`]);
618 FIRST_ASSUM (C INTRO_TAC [`2`]);
619 FIRST_X_ASSUM (C INTRO_TAC [`3`]);
620 ASM_REWRITE_TAC[arith `1 <= 3 /\ 3 <= 3 /\ 1 <= 2 /\ 2 <= 3 /\ 1 <= 1`];
621 TYPIFY `barV V 3 ul` (C SUBGOAL_THEN (unlist REWRITE_TAC));
622 BY(ASM_MESON_TAC[IN]);
623 INTRO_TAC Leaf_cell.VORONOI_LIST_EQ [`V`;`truncate_simplex 1 ul`];
624 TYPIFY `set_of_list (truncate_simplex 1 ul) = {EL 0 ul, EL 1 ul}` (C SUBGOAL_THEN SUBST1_TAC);
625 MATCH_MP_TAC Bump.SET_OF_LIST_TRUNCATE_1;
626 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `2 <= 3 + 1`]);
627 REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
628 ONCE_REWRITE_TAC[MESON[] `(!x y. P x y) = !y x. P x y`];
629 DISCH_THEN (C INTRO_TAC [`1`]);
630 TYPIFY `barV V 1 (truncate_simplex 1 ul)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
631 MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV;
633 BY(ASM_MESON_TAC[IN;arith `1 <= 3`]);
635 FIRST_X_ASSUM MP_TAC;
636 REWRITE_TAC[Leaf_cell.DIST_EQ_HALF_PLANE];
637 ASM_REWRITE_TAC[Leaf_cell.DIST_LE_HALF_PLANE];
638 TYPED_ABBREV_TAC `(n:real^3) = (EL 0 ul - EL 1 ul)`;
639 TYPED_ABBREV_TAC `(m:real^3) = (EL 0 ul + EL 1 ul)`;
640 TYPIFY `n dot (&2 % (t1 % omega_list_n V ul 1 + t2 % omega_list_n V ul 2 + t3 % omega_list_n V ul 3 + t4 % EL 0 ul) - m) = t1 * n dot (&2 % omega_list_n V ul 1 - m) + t2 * n dot (&2 % omega_list_n V ul 2 - m) + t3 * n dot (&2 % omega_list_n V ul 3 - m) + t4 * n dot (&2 % EL 0 ul - m)` (C SUBGOAL_THEN SUBST1_TAC);
641 FIRST_X_ASSUM (MP_TAC o (MATCH_MP (arith `t1 + t2 + t3 + t4 = &1 ==> t4 = &1 - t1 - t2 - t3`)));
642 DISCH_THEN SUBST1_TAC;
643 BY(VECTOR_ARITH_TAC);
644 DISCH_THEN ((unlist REWRITE_TAC) o GSYM);
645 REWRITE_TAC[arith `x * &0 = &0 /\ &0 + x = x`];
646 MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a = b)`);
649 GMATCH_SIMP_TAC REAL_LE_MUL;
653 BY(REWRITE_TAC[GSYM Leaf_cell.DIST_LE_HALF_PLANE;DIST_REFL;DIST_POS_LE]);
654 COMMENT "other direction";
655 TYPIFY `&0 < (n dot (&2 % EL 0 ul - m))` ENOUGH_TO_SHOW_TAC;
656 REPEAT WEAK_STRIP_TAC;
657 MATCH_MP_TAC Real_ext.REAL_PROP_NN_RCANCEL;
661 REWRITE_TAC[GSYM Collect_geom.DIST_LT_HALF_PLANE];
662 REWRITE_TAC[DIST_REFL];
663 MATCH_MP_TAC DIST_POS_LT;
664 INTRO_TAC BARV_DISTINCT [`V`;`truncate_simplex 1 ul`];
667 MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV;
668 BY(ASM_MESON_TAC[IN;arith `1 <= 3`]);
669 REPEAT (GMATCH_SIMP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
670 BY(ASM_MESON_TAC[arith `1 + 1 <= 3 + 1 /\ 1 <= 1 /\ 0 <= 1`;IN;Sphere.BARV])
674 let DIFF_INTER = prove_by_refinement(
675 `!(X:A->bool) Y Z. (X DIFF Y) INTER Z = (X INTER Z) DIFF Y`,
682 let RCONE_GT_SCALE = prove_by_refinement(
683 `!u0 u1 (u:real^A) a t. &0 < t /\ u0 + u IN rcone_gt u0 u1 a ==> u0 + t % u IN rcone_gt u0 u1 a`,
686 REWRITE_TAC[rcone_gt;rconesgn;IN_ELIM_THM;dist];
687 REWRITE_TAC[varith `!(v:real^A). (u0 + v) - u0 = v`];
688 REWRITE_TAC[NORM_MUL;DOT_LMUL;arith `x > y <=> y < x`];
689 REPEAT WEAK_STRIP_TAC;
690 ASM_SIMP_TAC[arith `&0 < t ==> abs t = t`];
691 REWRITE_TAC[GSYM REAL_MUL_ASSOC];
692 GMATCH_SIMP_TAC REAL_LT_LMUL_EQ;
693 BY(ASM_REWRITE_TAC[])
697 let BARV3_TRUNC1 = prove_by_refinement(
698 `!V ul. ul IN barV V 3 ==> truncate_simplex 1 ul = [EL 0 ul;EL 1 ul]`,
701 REPEAT WEAK_STRIP_TAC;
702 TYPIFY `ul = [EL 0 ul;EL 1 ul; EL 2 ul; EL 3 ul]` (C SUBGOAL_THEN ASSUME_TAC);
703 MATCH_MP_TAC Bump.LENGTH4;
704 BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3+1 = 4`]);
705 BY(ASM_MESON_TAC[Marchal_cells.TRUNCATE_SIMPLEX_EXPLICIT_1])
709 let MCELL1_RADIAL = prove_by_refinement(
710 `!V X ul. saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell1 V ul) /\ ~(NULLSET X) ==>
711 radial (sqrt(&2)) (EL 0 ul) (X INTER ball(EL 0 ul,sqrt (&2)))
715 REPEAT WEAK_STRIP_TAC;
716 REWRITE_TAC[Sphere.radial];
720 INTRO_TAC MCELL1_EXPLICIT [`V`;`mcell1 V ul`;`ul`];
723 REWRITE_TAC[Bump.MCELL1];
724 DISCH_THEN SUBST1_TAC;
725 REWRITE_TAC [GSYM EL];
726 REPEAT WEAK_STRIP_TAC;
727 TYPIFY `ball (EL 0 ul,sqrt(&2)) SUBSET cball(EL 0 ul,sqrt(&2))` (C SUBGOAL_THEN ASSUME_TAC);
728 BY(REWRITE_TAC[BALL_SUBSET_CBALL]);
729 FIRST_X_ASSUM_ST `rogers` MP_TAC;
730 TYPIFY `((rogers V ul INTER cball (EL 0 ul,sqrt(&2))) DIFF rcone_gt (EL 0 ul) (EL (SUC 0) ul) (hl (truncate_simplex 1 ul) / sqrt (&2))) INTER ball (EL 0 ul,sqrt (&2)) = (rogers V ul INTER ball (EL 0 ul,sqrt(&2))) DIFF rcone_gt (EL 0 ul) (EL (SUC 0) ul) (hl (truncate_simplex 1 ul) / sqrt (&2))` (C SUBGOAL_THEN SUBST1_TAC);
731 REWRITE_TAC[GSYM DIFF_INTER];
732 FIRST_X_ASSUM MP_TAC;
733 REWRITE_TAC[ INTER_ASSOC];
735 REWRITE_TAC[IN_INTER;IN_DIFF];
736 REPEAT WEAK_STRIP_TAC;
737 TYPIFY `~(EL 0 ul = EL 1 ul)` (C SUBGOAL_THEN ASSUME_TAC);
738 INTRO_TAC BARV_DISTINCT [`V`;`truncate_simplex 1 ul`];
741 MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV;
742 BY(ASM_MESON_TAC[IN;arith `1 <= 3`]);
743 REPEAT (GMATCH_SIMP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
744 BY(ASM_MESON_TAC[arith `1 + 1 <= 3 + 1 /\ 1 <= 1 /\ 0 <= 1`;IN;Sphere.BARV]);
745 MATCH_MP_TAC (TAUT `a /\ b ==> b /\ a`);
747 REPEAT (FIRST_X_ASSUM_ST `SUC` MP_TAC);
748 REWRITE_TAC[arith `SUC 0 = 1`];
749 REPEAT WEAK_STRIP_TAC;
750 FIRST_X_ASSUM_ST `~` MP_TAC;
752 TYPIFY `EL 0 ul + u = (EL 0 ul + (&1/t) % (t % u))` (C SUBGOAL_THEN SUBST1_TAC);
753 REWRITE_TAC[VECTOR_MUL_ASSOC];
754 TYPIFY `(&1 / t) * t = &1` ENOUGH_TO_SHOW_TAC;
755 DISCH_THEN SUBST1_TAC;
756 BY(VECTOR_ARITH_TAC);
757 Calc_derivative.CALC_ID_TAC;
758 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
759 MATCH_MP_TAC RCONE_GT_SCALE;
760 GMATCH_SIMP_TAC REAL_LT_DIV;
762 BY(ASM_REWRITE_TAC[arith `&0 < &1 /\ ( &0 < t <=> t > &0)`]);
765 MATCH_MP_TAC (TAUT `a /\ b ==> b /\ a`);
767 REWRITE_TAC[ball;IN_ELIM_THM;dist];
768 TYPIFY `!u v. (u:real^3) - (u + t % v) = (-- t) % v` (C SUBGOAL_THEN (unlist REWRITE_TAC));
769 BY(VECTOR_ARITH_TAC);
770 REWRITE_TAC[NORM_MUL];
771 BY(ASM_SIMP_TAC[arith `t > &0 ==> abs(-- t) = t`]);
774 FIRST_X_ASSUM_ST `rogers` MP_TAC;
775 REPEAT (GMATCH_SIMP_TAC Marchal_cells_2_new.ROGERS_EXPLICIT);
776 ASM_REWRITE_TAC[GSYM EL];
777 TYPED_ABBREV_TAC `(w:real^3) = EL 0 ul + u`;
778 TYPIFY `t % u = t % (w - EL 0 ul)` (C SUBGOAL_THEN SUBST1_TAC);
780 BY(VECTOR_ARITH_TAC);
782 MATCH_MP_TAC CONVEX_HULL_SCALE;
783 ASM_SIMP_TAC[arith `t > &0 ==> &0 <= t`];
785 INTRO_TAC NOT_COPLANAR_OMEGA_LIST_N [`V`;`ul`];
787 BY(ASM_MESON_TAC[IN]);
788 REWRITE_TAC[IMAGE_4_EXPLICIT];
789 BY(MESON_TAC[Sphere.OMEGA_LIST_N;EL]);
791 GMATCH_SIMP_TAC OMEGA_LIST_BISECTOR;
793 INTRO_TAC BALL_DIFF_RCONE_GT_BISECTOR [`EL 0 ul`;`EL 1 ul`;`EL 0 ul + t % u`;`sqrt(&2)`;`hl(truncate_simplex 1 ul)`];
795 ASM_REWRITE_TAC[IN_DIFF];
797 BY(ASM_MESON_TAC[arith `1 = SUC 0`]);
799 GMATCH_SIMP_TAC REAL_LT_RSQRT;
801 GMATCH_SIMP_TAC BARV3_TRUNC1;
803 BY(ASM_MESON_TAC[IN]);
804 ONCE_REWRITE_TAC[DIST_SYM];
805 REWRITE_TAC[Marchal_cells_3.HL_2];
807 REWRITE_TAC[Sphere.bis_le;IN_ELIM_THM];
810 REWRITE_TAC[arith `!u v. (u + w) - u = (w:real^3)`];
811 DISCH_THEN (unlist REWRITE_TAC);
816 let MCELL1_VOL = prove_by_refinement(
817 `!V X ul. saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell1 V ul) /\ ~(NULLSET X) ==>
818 vol X = (sqrt(&2) pow 3 / &3) * sol (EL 0 ul) X`,
821 REPEAT WEAK_STRIP_TAC;
822 INTRO_TAC MCELL1_VOL_RESTRICT [`V`;`X`;`ul`];
824 DISCH_THEN SUBST1_TAC;
825 INTRO_TAC MCELL1_SOL_RESTRICT [`V`;`X`;`ul`];
827 DISCH_THEN SUBST1_TAC;
828 INTRO_TAC MCELL1_RADIAL [`V`;`X`;`ul`];
831 GMATCH_SIMP_TAC Vol1.sol_spec;
832 EXISTS_TAC `sqrt(&2)`;
833 REWRITE_TAC[GSYM CONJ_ASSOC];
835 REWRITE_TAC[arith `x > y <=> y < x`];
836 GMATCH_SIMP_TAC REAL_LT_RSQRT;
839 REWRITE_TAC[INTER_ASSOC;INTER_IDEMPOT];
840 MATCH_MP_TAC MEASURABLE_INTER;
841 REWRITE_TAC[MEASURABLE_BALL;Bump.MCELL1;];
842 MATCH_MP_TAC Urrphbz1.MEASURABLE_MCELL;
843 BY(ASM_REWRITE_TAC[]);
844 ASM_REWRITE_TAC[INTER_ASSOC;INTER_IDEMPOT];
845 Calc_derivative.CALC_ID_TAC;
846 GMATCH_SIMP_TAC SQRT_EQ_0;
851 let HJKDESR1a_1cell = prove_by_refinement(
852 `&0 < &8 * pi * sqrt2 / &3 - &8 * mm1 `,
855 REWRITE_TAC[ arith `&8 * pi * sqrt2 / &3 = (&8 / &3) * (pi * sqrt2)`];
856 MATCH_MP_TAC (arith `&3 * mm1 < z ==> &0 < (&8/ &3) * z - &8 * mm1`);
857 MATCH_MP_TAC REAL_LT_TRANS;
858 EXISTS_TAC (`&3 * #1.3`);
859 GMATCH_SIMP_TAC REAL_LT_LMUL_EQ;
860 GMATCH_SIMP_TAC REAL_LT_MUL2;
861 MP_TAC Flyspeck_constants.bounds;
865 let TSKAJXY_1 = prove_by_refinement(
866 `!V ul. saturated V /\ packing V /\ barV V 3 ul ==>
867 gammaX V (mcell1 V ul) lmfun >= &0 `,
870 REPEAT WEAK_STRIP_TAC;
871 ASM_CASES_TAC `NULLSET (mcell1 V ul)`;
872 BY(ASM_MESON_TAC[GAMMAX_NULLSET;arith `x = &0 ==> x >= &0`;Bump.MCELL1]);
873 GMATCH_SIMP_TAC GAMMAX_MCELL1;
874 TYPIFY `ul` EXISTS_TAC;
876 INTRO_TAC MCELL1_VOL [`V`;`mcell1 V ul`;`ul`];
879 TYPIFY `sol (EL 0 ul) (mcell1 V ul) = (&3 / sqrt(&2) pow 3) * vol (mcell1 V ul)` (C SUBGOAL_THEN SUBST1_TAC);
881 Calc_derivative.CALC_ID_TAC;
882 GMATCH_SIMP_TAC SQRT_EQ_0;
884 REWRITE_TAC[arith `b - c * d* b = (&1 - c* d) * b`;arith `x >= &0 <=> &0 <= x`];
885 GMATCH_SIMP_TAC REAL_LE_MUL;
887 REWRITE_TAC[arith `&0 <= x <=> x >= &0`];
888 MATCH_MP_TAC Vol1.VOLUME_PROPS_MEASURABLE;
889 REWRITE_TAC[Bump.MCELL1];
890 MATCH_MP_TAC Urrphbz1.URRPHBZ1;
891 BY(ASM_REWRITE_TAC[]);
892 INTRO_TAC HJKDESR1a_1cell [];
893 SUBGOAL_THEN `!x y. (x = (&8 * pi * sqrt(&2) / &3) * y) ==> (&0 < x ==> &0 <= y)` MATCH_MP_TAC;
894 REPEAT WEAK_STRIP_TAC;
895 FIRST_X_ASSUM MP_TAC;
897 DISCH_THEN (MP_TAC o (MATCH_MP (arith `&0 < x ==> &0 <= x`)));
899 MATCH_MP_TAC Real_ext.REAL_PROP_NN_LCANCEL;
900 TYPIFY `(&8 * pi * sqrt (&2) / &3)` EXISTS_TAC;
902 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
903 REWRITE_TAC[ REAL_OF_NUM_LT];
904 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
905 GMATCH_SIMP_TAC REAL_LT_DIV;
906 REWRITE_TAC[ REAL_OF_NUM_LT];
907 GMATCH_SIMP_TAC REAL_LT_RSQRT;
912 Calc_derivative.CALC_ID_TAC;
913 ASM_SIMP_TAC[PI_POS;arith `&0 < x ==> ~(x = &0)`;arith `~(&3= &0)`];
914 GMATCH_SIMP_TAC SQRT_EQ_0;
915 REWRITE_TAC[Sphere.sqrt2];
920 TYPIFY `sqrt(&2) pow 3 = &2 * sqrt(&2)` (C SUBGOAL_THEN SUBST1_TAC);
921 REWRITE_TAC[arith `3 = SUC 2`;real_pow];
922 GMATCH_SIMP_TAC SQRT_POW_2;
928 let MCELL_CELL_PARAMETERS_D_EXIST = prove_by_refinement(
929 `!V ul vl k X. (k <= 4) /\ packing V /\ saturated V /\ (X = mcell k V ul) /\ ul IN barV V 3 /\
930 initial_sublist vl ul /\
932 FST (cell_params_d V X vl) = k`,
935 REWRITE_TAC[Pack_defs.cell_params_d];
936 REPEAT WEAK_STRIP_TAC;
937 SELECT_TAC THEN (REPEAT (FIRST_X_ASSUM MP_TAC)) THEN (REWRITE_TAC[Bump.BETA_ORDERED_PAIR_THM]);
938 INTRO_TAC Ajripqn.AJRIPQN [`V`;`ul`;`SND t`;`k`;`FST t`];
939 REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY;arith `x = 0 \/ x = 1 \/ x = 2 \/ x = 3 \/ x = 4 <=> x <= 4`];
941 REPEAT WEAK_STRIP_TAC;
942 FIRST_X_ASSUM_ST `==>` MP_TAC;
945 BY(ASM_MESON_TAC[INTER_IDEMPOT]);
946 BY(DISCH_THEN (unlist REWRITE_TAC));
947 REPEAT WEAK_STRIP_TAC;
948 FIRST_X_ASSUM MP_TAC;
949 REWRITE_TAC[NOT_EXISTS_THM];
950 DISCH_THEN (C INTRO_TAC [`k,ul`]);
951 BY(ASM_REWRITE_TAC[])
955 let INITIAL_SUBLIST_2 = prove_by_refinement(
956 `!ul. LENGTH ul = 4 ==> initial_sublist [EL 0 (ul:(A)list);EL 1 ul] ul`,
959 REPEAT WEAK_STRIP_TAC;
960 INTRO_TAC Bump.LENGTH4 [`ul`];
962 BY(ASM_REWRITE_TAC[]);
964 TYPIFY `ul = APPEND [EL 0 ul;EL 1 ul] [EL 2 ul;EL 3 ul]` ENOUGH_TO_SHOW_TAC;
965 BY(ASM_MESON_TAC[Packing3.INITIAL_SUBLIST_APPEND]);
971 let MCELL2_CELL_PARAMETERS_EXIST = prove_by_refinement(
972 `!V ul X. packing V /\ saturated V /\ (X = mcell2 V ul) /\ ul IN barV V 3 /\ ~NULLSET X ==>
973 FST (cell_params_d V X [EL 0 ul;EL 1 ul]) = 2`,
976 REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_CELL_PARAMETERS_D_EXIST THEN ASM_REWRITE_TAC[Bump.MCELL2;arith `2 <= 4`];
977 TYPIFY `ul` EXISTS_TAC;
979 MATCH_MP_TAC INITIAL_SUBLIST_2;
980 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`])
984 let MCELL_PARAM_D_UL = prove_by_refinement(
985 `!V ul ul' vl X k. (k<= 4) /\ packing V /\ saturated V /\ (X = mcell k V ul) /\ ul IN barV V 3 /\ ~NULLSET X /\
986 initial_sublist ul' ul /\
987 vl = SND (cell_params_d V X ul') ==>
988 (X = mcell k V vl /\ vl IN barV V 3 /\ initial_sublist ul' vl)`,
991 REWRITE_TAC[Pack_defs.cell_params_d];
992 REPEAT WEAK_STRIP_TAC;
993 INTRO_TAC MCELL_CELL_PARAMETERS_D_EXIST [`V`;`ul`;`ul'`;`k`;`X`];
995 REWRITE_TAC[Pack_defs.cell_params_d];
996 Bump.WEAK_SELECT_TAC THEN (REPEAT (FIRST_X_ASSUM MP_TAC)) THEN (REWRITE_TAC[Bump.BETA_ORDERED_PAIR_THM]);
997 Bump.WEAK_SELECT_TAC THEN (REPEAT (FIRST_X_ASSUM MP_TAC)) THEN (REWRITE_TAC[Bump.BETA_ORDERED_PAIR_THM]);
998 REPEAT WEAK_STRIP_TAC;
1001 REPEAT WEAK_STRIP_TAC;
1003 BY(ASM_MESON_TAC[]);
1004 REWRITE_TAC[NOT_EXISTS_THM];
1005 DISCH_THEN (C INTRO_TAC [`k,ul`]);
1006 BY(ASM_MESON_TAC[FST;SND])
1010 let MCELL2_PARAM_D_UL = prove_by_refinement(
1011 `!V ul ul' vl X. packing V /\ saturated V /\ (X = mcell2 V ul) /\ ul IN barV V 3 /\ ~NULLSET X /\
1012 initial_sublist ul' ul /\
1013 vl = SND (cell_params_d V X ul') ==>
1014 (X = mcell2 V (vl) /\ vl IN barV V 3 /\ initial_sublist ul' vl)`,
1017 REWRITE_TAC[Bump.MCELL2];
1018 REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_PARAM_D_UL;
1019 BY(ASM_MESON_TAC[arith `2 <= 4`])
1023 let MCELL2_DIHX = prove_by_refinement(
1024 `!V X ul. saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell2 V ul) /\ ~(NULLSET X) ==>
1025 dihX V X (EL 0 ul, EL 1 ul) = dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3)`,
1028 REPEAT WEAK_STRIP_TAC;
1029 ASM_REWRITE_TAC[Pack_defs.dihX;Pack_defs.dihu2;LET_DEF;LET_END_DEF;Bump.BETA_ORDERED_PAIR_THM];
1030 GMATCH_SIMP_TAC MCELL2_CELL_PARAMETERS_EXIST;
1031 ASM_REWRITE_TAC[IN];
1033 BY(ASM_MESON_TAC[]);
1034 TYPED_ABBREV_TAC `(vl:(real^3)list) = SND (cell_params_d V (mcell2 V ul) [EL 0 ul; EL 1 ul])`;
1035 INTRO_TAC MCELL2_PARAM_D_UL [`V`;`ul`;`[EL 0 ul;EL 1 ul]`;`vl`;`X`];
1036 ASM_REWRITE_TAC[IN];
1038 MATCH_MP_TAC INITIAL_SUBLIST_2;
1039 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`]);
1040 REPEAT WEAK_STRIP_TAC;
1041 INTRO_TAC Marchal_cells_3.MCELL_ID_OMEGA_LIST_N [`V`;`2`;`2`;`ul`;`vl`];
1043 ASM_REWRITE_TAC[IN_INSERT];
1044 BY(ASM_MESON_TAC[Bump.MCELL2]);
1045 REWRITE_TAC[arith `2 = 2`;arith `2 - 1 = 1`];
1046 DISCH_THEN (C INTRO_TAC [`3`]);
1047 REWRITE_TAC[arith `1 <= 3 /\ 3 <= 3`];
1048 DISCH_THEN SUBST1_TAC;
1049 INTRO_TAC Marchal_cells_3.MCELL_ID_MXI_2 [`V`;`2`;`2`;`ul`;`vl`];
1051 ASM_REWRITE_TAC[IN_INSERT];
1052 BY(ASM_MESON_TAC[Bump.MCELL2]);
1053 DISCH_THEN SUBST1_TAC;
1054 INTRO_TAC INITIAL_SUBLIST_2 [`vl`];
1056 BY(ASM_MESON_TAC[Sphere.BARV;arith `3 + 1 = 4`]);
1058 INTRO_TAC Packing3.INITIAL_SUBLIST_UNIQUE [`2`;`[EL 0 ul;EL 1 ul]`;`[EL 0 vl;EL 1 vl]`;`vl`];
1059 ASM_REWRITE_TAC[LENGTH;arith `SUC (SUC 0) = 2`];
1060 REWRITE_TAC[CONS_11];
1061 BY(DISCH_THEN (unlist REWRITE_TAC))
1065 let BIS_LE_INTER = prove_by_refinement(
1066 `!u0 (u1:real^A). bis_le u0 u1 INTER bis_le u1 u0 = bis u0 u1`,
1069 REWRITE_TAC[Sphere.bis_le;EXTENSION;IN_ELIM_THM;IN_INTER;Sphere.bis];
1074 let BIS_LE_UNION = prove_by_refinement(
1075 `!u0 (u1:real^A). bis_le u0 u1 UNION bis_le u1 u0 = (:real^A)`,
1078 REWRITE_TAC[Sphere.bis_le;EXTENSION;IN_ELIM_THM;IN_UNION;IN_UNIV];
1083 let BIS_HYPERPLANE = prove_by_refinement(
1084 `!u0 (u1:real^A). bis u0 u1 = { p | (&2 % (u0 - u1)) dot p = (u0 - u1) dot (u0 + u1)}`,
1087 REWRITE_TAC[Sphere.bis;EXTENSION;Leaf_cell.DIST_EQ_HALF_PLANE;IN_ELIM_THM];
1088 REPEAT WEAK_STRIP_TAC;
1089 MATCH_MP_TAC (arith `u = a - (b) ==> (&0 = u <=> a = b)`);
1090 BY(VECTOR_ARITH_TAC)
1094 let MCELL2_INTER_BIS_LE_MEASURABLE = prove_by_refinement(
1095 `!u0 u1 V X ul. packing V /\ saturated V /\
1098 measurable (X INTER bis_le u0 u1)`,
1101 REPEAT WEAK_STRIP_TAC;
1102 MATCH_MP_TAC MEASURABLE_CONVEX;
1104 MATCH_MP_TAC CONVEX_INTER;
1105 ASM_REWRITE_TAC[Bump.MCELL2;Packing3.CONVEX_BIS_LE];
1106 MATCH_MP_TAC Leaf_cell.MCELL_CONVEX;
1107 BY(ASM_MESON_TAC[arith `2 <= 2`]);
1108 MATCH_MP_TAC BOUNDED_SUBSET;
1109 TYPIFY `X` EXISTS_TAC;
1112 ASM_REWRITE_TAC[Bump.MCELL2];
1113 MATCH_MP_TAC Urrphbz1.BOUNDED_MCELL;
1114 BY(ASM_REWRITE_TAC[])
1118 let MCELL2_VOL_SPLIT = prove_by_refinement(
1119 `!V X ul. saturated V /\
1124 vol X = vol (X INTER bis_le (EL 0 ul) (EL 1 ul)) + vol (X INTER bis_le (EL 1 ul) (EL 0 ul))`,
1127 REPEAT WEAK_STRIP_TAC;
1128 GMATCH_SIMP_TAC (GSYM MEASURE_NEGLIGIBLE_UNION);
1129 TYPIFY ` ((X INTER bis_le (EL 0 ul) (EL 1 ul)) INTER X INTER bis_le (EL 1 ul) (EL 0 ul)) = X INTER bis (EL 0 ul) (EL 1 ul)` (C SUBGOAL_THEN SUBST1_TAC);
1130 INTRO_TAC BIS_LE_INTER [`EL 0 ul`;`EL 1 ul`];
1132 TYPIFY `(X INTER bis_le (EL 0 ul) (EL 1 ul) UNION X INTER bis_le (EL 1 ul) (EL 0 ul)) = X` (C SUBGOAL_THEN SUBST1_TAC);
1133 INTRO_TAC BIS_LE_UNION [`EL 0 ul`;`EL 1 ul`];
1136 REWRITE_TAC[CONJ_ASSOC];
1138 BY(ASM_MESON_TAC[MCELL2_INTER_BIS_LE_MEASURABLE]);
1139 REWRITE_TAC[BIS_HYPERPLANE];
1140 MATCH_MP_TAC NEGLIGIBLE_SUBSET;
1141 TYPIFY `{p | &2 % (EL 0 ul - EL 1 ul) dot p = (EL 0 ul - EL 1 ul) dot (EL 0 ul + EL 1 ul)}` EXISTS_TAC;
1144 MATCH_MP_TAC NEGLIGIBLE_HYPERPLANE;
1145 REWRITE_TAC[DE_MORGAN_THM];
1147 REWRITE_TAC[VECTOR_MUL_EQ_0;arith `~(&2 = &0)`];
1148 REWRITE_TAC[varith `!a (b:real^A). a - b = vec 0 <=> a = b`];
1150 BY(ASM_MESON_TAC[MCELL2_VX_PROPS])
1154 let RCONE_GE_COS = prove_by_refinement(
1155 `!(u:real^3) v a. ~(u=v) ==>
1156 rcone_ge u v a = {u} UNION { x | a <= cos(arcV u v x) }`,
1159 REPEAT WEAK_STRIP_TAC;
1160 ONCE_REWRITE_TAC[Trigonometry2.ARC_SYM];
1161 REWRITE_TAC[Sphere.rcone_ge;Sphere.rconesgn;EXTENSION;IN_ELIM_THM;IN_UNION;IN_SING;Trigonometry1.DOT_COS];
1162 REWRITE_TAC[dist;arith `x >= y <=> y <= x`];
1163 REPEAT WEAK_STRIP_TAC;
1164 TYPIFY `x = u` ASM_CASES_TAC;
1166 REWRITE_TAC[VECTOR_SUB_REFL;NORM_0];
1169 REWRITE_TAC[arith `nu * nv * a <= nu * nv * c <=> &0 <= nu * nv * (c - a)`];
1170 GMATCH_SIMP_TAC REAL_LE_MUL_EQ;
1171 GMATCH_SIMP_TAC REAL_LE_MUL_EQ;
1172 REWRITE_TAC[NORM_POS_LT];
1173 REWRITE_TAC[GSYM Trigonometry2.ARCV_VEC0_FORM];
1174 REWRITE_TAC[varith `(v:real^3) - u = vec 0 <=> (v = u)`];
1180 let DIST_LAW_OF_COS_ALT = prove_by_refinement(
1181 `!u v (w:real^3). dist (v,w) pow 2 =
1183 dist (u,w) pow 2 - &2 * dist (u,v) * dist (u,w) * cos (arcV u v w)`,
1186 BY(MESON_TAC[Trigonometry1.DIST_LAW_OF_COS])
1190 let ATN_INV = prove_by_refinement(
1191 `!x y. &0 < x /\ &0 < y ==> atn (x / y) = pi / &2 - atn (y/x) `,
1194 REPEAT WEAK_STRIP_TAC;
1195 INTRO_TAC Merge_ineq.atn_inv [`y/x`];
1197 GMATCH_SIMP_TAC REAL_LT_DIV;
1198 BY(ASM_REWRITE_TAC[]);
1199 TYPIFY `&1 / (y / x) = x / y` (C SUBGOAL_THEN SUBST1_TAC);
1200 Calc_derivative.CALC_ID_TAC;
1201 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1206 let REAL_DIV_NEG = prove_by_refinement(
1207 `!x y. (x / --y) = -- (x/y)`,
1210 REWRITE_TAC[real_div;REAL_INV_NEG];
1215 let ATN2_Y_NEG = prove_by_refinement(
1216 `!x y. y < &0 ==> atn2(x,y) = -- (pi / &2) - atn(x/y)`,
1219 REPEAT WEAK_STRIP_TAC;
1220 REWRITE_TAC[Trigonometry2.atn2];
1221 TYPIFY `abs y < x` ASM_CASES_TAC;
1223 TYPED_ABBREV_TAC `(u:real) = -- y`;
1224 REPEAT (FIRST_X_ASSUM_ST `<` MP_TAC);
1225 TYPIFY `y = -- u` (C SUBGOAL_THEN SUBST1_TAC);
1226 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1227 REWRITE_TAC[arith `-- u < &0 <=> &0 < u`;arith `-- u / x = -- (u/x)`;REAL_DIV_NEG];
1228 REWRITE_TAC[ATN_NEG];
1229 REPEAT WEAK_STRIP_TAC;
1230 GMATCH_SIMP_TAC ATN_INV;
1234 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1236 BY(ASM_SIMP_TAC[arith `y < &0 ==> ~(&0 < y)`])
1240 let RCONE_PAIR = prove_by_refinement(
1241 `!(u:real^3) v t. ~(u=v) /\ &0 < t /\ t <= &1 ==> rcone_ge u v t INTER bis_le u v SUBSET rcone_ge v u t`,
1244 REPEAT WEAK_STRIP_TAC;
1245 GMATCH_SIMP_TAC RCONE_GE_COS;
1246 GMATCH_SIMP_TAC RCONE_GE_COS;
1247 ASM_REWRITE_TAC[SUBSET;IN_INTER;IN_UNION;IN_SING;IN_ELIM_THM;Sphere.bis_le];
1249 TYPIFY `x = u` ASM_CASES_TAC;
1250 BY(ASM_SIMP_TAC[Local_lemmas1.ACR_REFL;COS_0]);
1252 TYPIFY `x = v` ASM_CASES_TAC;
1253 BY(ASM_SIMP_TAC[Local_lemmas1.ACR_REFL;COS_0]);
1255 REPEAT WEAK_STRIP_TAC;
1256 FIRST_X_ASSUM_ST `cos` MP_TAC;
1257 MATCH_MP_TAC (arith `(t <= x ==> x <= y) ==> (t <= x ==> t <= y)`);
1259 MATCH_MP_TAC COS_MONO_LE;
1260 REWRITE_TAC[Local_lemmas1.ARCV_BOUNDS];
1261 TYPIFY `&0 < cos (arcV u v x)` (C SUBGOAL_THEN ASSUME_TAC);
1262 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1263 REPLICATE_TAC 2 (GMATCH_SIMP_TAC Trigonometry1.arcVarc);
1265 TYPIFY `dist(v,x) pow 2 < dist(u,v) pow 2 + dist(u,x) pow 2` (C SUBGOAL_THEN ASSUME_TAC);
1266 INTRO_TAC DIST_LAW_OF_COS_ALT [`u`;`v`;`x`];
1267 TYPIFY `&0 < &2 * dist(u,v) * dist (u,x) * cos (arcV u v x)` ENOUGH_TO_SHOW_TAC;
1269 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
1272 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
1273 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
1274 BY(ASM_SIMP_TAC[GSYM DIST_POS_LT]);
1275 TYPIFY `dist(v,u) = dist(u,v)` (C SUBGOAL_THEN SUBST1_TAC);
1276 BY(MESON_TAC[DIST_SYM]);
1277 TYPED_ABBREV_TAC `(c:real) = dist(u,v)` ;
1278 TYPED_ABBREV_TAC `(b:real) = dist(v,x)` ;
1279 TYPED_ABBREV_TAC `(a:real) = dist(u,x)` ;
1280 REWRITE_TAC[Local_lemmas1.COS_ARCV];
1281 REWRITE_TAC[Sphere.arclength];
1282 REWRITE_TAC[arith `t + u <= t + v <=> u <= v`];
1283 FIRST_X_ASSUM_ST `dist(x,u) <= dist(x,v)` MP_TAC;
1284 ONCE_REWRITE_TAC[DIST_SYM];
1287 TYPIFY `a pow 2 <= b pow 2` (C SUBGOAL_THEN ASSUME_TAC);
1288 MATCH_MP_TAC Collect_geom2.POS_IMP_POW2;
1291 BY(REWRITE_TAC[DIST_POS_LE]);
1292 TYPIFY `ups_x (c*c) (a*a) (b*b) = ups_x (c*c) (b*b) (a*a)` (C SUBGOAL_THEN SUBST1_TAC);
1293 BY(MESON_TAC[Collect_geom.UPS_X_SYM]);
1294 TYPED_ABBREV_TAC `(up:real) = ups_x (c*c) (b*b) (a*a)` ;
1295 REPEAT (GMATCH_SIMP_TAC ATN2_Y_NEG);
1297 FIRST_X_ASSUM_ST `<` MP_TAC;
1301 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1303 MATCH_MP_TAC (arith `y <= x ==> u - x <= u - y`);
1304 REWRITE_TAC[ATN_MONO_LE_EQ];
1305 TYPIFY `&0 <= sqrt up` (C SUBGOAL_THEN ASSUME_TAC);
1306 GMATCH_SIMP_TAC SQRT_POS_LE;
1308 BY(ASM_MESON_TAC[Collect_geom.TROI_OI_DAT_HOI;REAL_POW_2]);
1309 REWRITE_TAC[real_div];
1310 GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP;
1312 REWRITE_TAC[arith `x - y - z = --(y + z - x)`;REAL_INV_NEG;arith `-- x <= --y <=> y <= x`];
1313 GMATCH_SIMP_TAC REAL_LE_INV2;
1314 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
1318 let MCELL2_SPLIT = prove_by_refinement(
1325 (X INTER bis_le (EL 0 ul) (EL 1 ul) =
1326 rcone_ge (EL 0 ul) (EL 1 ul) (hl (truncate_simplex 1 ul) / sqrt (&2)) INTER
1327 aff_ge {EL 0 ul,EL 1 ul} {mxi V ul,omega_list_n V ul 3} INTER bis_le (EL 0 ul) (EL 1 ul))`,
1330 REPEAT WEAK_STRIP_TAC;
1331 INTRO_TAC Pack_defs.mcell2 [`V`;`ul`];
1332 TYPIFY `~(hl (truncate_simplex 1 ul) < sqrt (&2) /\ sqrt (&2) <= hl ul)` ASM_CASES_TAC;
1334 BY(ASM_MESON_TAC[NEGLIGIBLE_EMPTY]);
1335 FIRST_ASSUM ((unlist REWRITE_TAC) o (REWRITE_RULE[NOT_CLAUSES]));
1336 ASM_REWRITE_TAC[LET_DEF;LET_END_DEF];
1337 DISCH_THEN SUBST1_TAC;
1338 TYPED_ABBREV_TAC `(a:real) = hl (truncate_simplex 1 ul)/ (sqrt (&2))` ;
1339 TYPIFY `HD ul = EL 0 ul /\ HD(TL ul) = EL 1 ul` (C SUBGOAL_THEN (unlist REWRITE_TAC));
1340 BY(REWRITE_TAC[EL;arith `1 = SUC 0`]);
1341 SUBGOAL_THEN `!(a:real^3->bool) b c d. (a INTER d SUBSET b) ==> ((a INTER b INTER c) INTER d = a INTER c INTER d)` (MATCH_MP_TAC);
1343 MATCH_MP_TAC RCONE_PAIR;
1346 BY(ASM_MESON_TAC[MCELL2_VX_PROPS]);
1348 TYPIFY `&0 < sqrt(&2)` (C SUBGOAL_THEN ASSUME_TAC);
1349 GMATCH_SIMP_TAC REAL_LT_RSQRT;
1352 GMATCH_SIMP_TAC REAL_LE_LDIV_EQ;
1353 ASM_REWRITE_TAC[arith `&1 * x = x`];
1354 FIRST_X_ASSUM_ST `~ ~ x` MP_TAC THEN REWRITE_TAC[];
1356 GMATCH_SIMP_TAC REAL_LT_DIV;
1358 BY(ASM_MESON_TAC[Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT])
1362 let FRUSTT_RCONE_GE = prove_by_refinement(
1364 &0 < a /\ ~(u= v) ==>
1367 (rcone_ge u v a INTER {y | (y- u) dot (v-u) <= h * norm (v-u) }))`,
1370 REPEAT WEAK_STRIP_TAC;
1371 ASM_REWRITE_TAC[frustt;frustum;EXTENSION;IN_ELIM_THM;LET_DEF;LET_END_DEF;IN_INTER];
1372 REWRITE_TAC[IN;arith `&0 * x = &0`;SDIFF];
1373 MATCH_MP_TAC NEGLIGIBLE_UNION;
1375 TYPIFY `!s. (s = {}) ==> NULLSET s` (C SUBGOAL_THEN MATCH_MP_TAC);
1376 BY(MESON_TAC[NEGLIGIBLE_EMPTY]);
1377 REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_DIFF;IN_ELIM_THM;IN_INTER];
1378 REPEAT WEAK_STRIP_TAC;
1379 FIRST_X_ASSUM MP_TAC;
1382 BY(ASM_MESON_TAC[Marchal_cells_2_new.RCONE_GT_SUBSET_RCONE_GE;IN;SUBSET]);
1383 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1384 MATCH_MP_TAC NEGLIGIBLE_SUBSET;
1385 TYPIFY `(rcone_ge u v a DIFF rcone_gt u v a) UNION {y | (y - u) dot (v - u) = h * norm (v - u)}` EXISTS_TAC;
1387 MATCH_MP_TAC NEGLIGIBLE_UNION;
1389 REWRITE_TAC[RCONE_GT_GE];
1390 MATCH_MP_TAC NEGLIGIBLE_SUBSET;
1391 TYPIFY `{x | (x - u) dot (v - u) = norm (x - u) * norm (v - u) * a}` EXISTS_TAC;
1394 TYPIFY `circular_cone {x | (x - u) dot (v - u) = norm (x - u) * norm (v - u) * a}` ENOUGH_TO_SHOW_TAC;
1395 BY(MESON_TAC[NULLSET_RULES]);
1396 REWRITE_TAC[circular_cone;c_cone];
1397 REWRITE_TAC[EXISTS_PAIRED_THM];
1398 GEXISTL_TAC [`u`;`v - (u:real^3)`;`a`];
1399 BY(ASM_REWRITE_TAC[varith `v - (u:real^3) = vec 0 <=> u = v`]);
1400 TYPIFY `!y u w a. (y- u) dot (w:real^3) = a <=> w dot y = a + u dot w` (C SUBGOAL_THEN (unlist ONCE_REWRITE_TAC));
1401 REPEAT WEAK_STRIP_TAC;
1402 MATCH_MP_TAC (arith `(x = y - z ==> (x = a' <=> y = a' + z))`);
1403 BY(VECTOR_ARITH_TAC);
1404 MATCH_MP_TAC NEGLIGIBLE_HYPERPLANE;
1405 BY(ASM_REWRITE_TAC[varith `(v:real^3) - u = vec 0 <=> u = v`]);
1406 REWRITE_TAC[SUBSET;IN_DIFF;IN_UNION;IN_INTER;IN_ELIM_THM];
1408 REPEAT WEAK_STRIP_TAC;
1410 MATCH_MP_TAC (TAUT (`(a ==>b) ==> (~ a \/ b)`));
1412 ASM_SIMP_TAC [(arith `x <= y ==> ((x = y) <=> ~(x < y))`)];
1414 FIRST_X_ASSUM_ST `~` MP_TAC;
1416 FIRST_X_ASSUM_ST `rcone_gt` MP_TAC;
1417 REWRITE_TAC[Sphere.rcone_gt;Sphere.rconesgn;IN_ELIM_THM];
1418 TYPIFY `&0 <= dist(x,u) * dist(v,u) * a` ENOUGH_TO_SHOW_TAC;
1420 GMATCH_SIMP_TAC REAL_LE_MUL;
1421 GMATCH_SIMP_TAC REAL_LE_MUL;
1422 BY(ASM_SIMP_TAC[DIST_POS_LE;arith `&0 < a ==> &0 <= a`])
1426 let SDIFF_SUBSET = prove_by_refinement(
1427 `!X Y Z.SDIFF (X INTER Z) (Y INTER Z) SUBSET SDIFF X Y `,
1435 let SDIFF_TRANS = prove_by_refinement(
1436 `!X Y (Z:A->bool). SDIFF X Z SUBSET SDIFF X Y UNION SDIFF Y Z`,
1444 let NULL_SDIFF_TRANS = prove_by_refinement(
1445 `!X Y Z. NULLSET (SDIFF X Y) /\ NULLSET (SDIFF Y Z) ==> NULLSET(SDIFF X Z)`,
1448 REPEAT WEAK_STRIP_TAC;
1449 MATCH_MP_TAC NEGLIGIBLE_SUBSET;
1450 BY(ASM_MESON_TAC[SDIFF_TRANS;NEGLIGIBLE_UNION])
1455 let FRUSTT_WEDGE_RCONE_GE = prove_by_refinement(
1457 &0 < a /\ ~(u= v) /\
1458 &0 < a /\ a <= &1 /\ &0 <= h /\ ~(u = v) /\
1459 ~collinear {u,v,w1} /\ ~collinear{ u,v,w2} ==>
1461 (frustt u v h a INTER wedge u v w1 w2)
1462 (rcone_ge u v a INTER {y | (y- u) dot (v-u) <= h * norm (v-u) } INTER wedge_ge u v w1 w2))`,
1465 REPEAT WEAK_STRIP_TAC;
1466 MATCH_MP_TAC NULL_SDIFF_TRANS;
1467 TYPIFY `frustt u v h a INTER wedge_ge u v w1 w2` EXISTS_TAC;
1469 MATCH_MP_TAC NEGLIGIBLE_SUBSET;
1470 TYPIFY `SDIFF (frustt u v h a) (rcone_ge u v a INTER {y | (y - u) dot (v - u) <= h * norm (v - u)})` EXISTS_TAC;
1472 BY(ASM_MESON_TAC[FRUSTT_RCONE_GE]);
1473 BY(MESON_TAC[INTER_ASSOC;SDIFF_SUBSET]);
1474 COMMENT "down to 1";
1475 ONCE_REWRITE_TAC[INTER_COMM];
1476 MATCH_MP_TAC NEGLIGIBLE_SUBSET;
1477 TYPIFY `SDIFF (wedge u v w1 w2) (wedge_ge u v w1 w2)` EXISTS_TAC;
1479 BY(MESON_TAC[SDIFF_SUBSET]);
1481 MATCH_MP_TAC NEGLIGIBLE_UNION;
1483 TYPIFY `wedge u v w1 w2 DIFF wedge_ge u v w1 w2 = {}` (C SUBGOAL_THEN (unlist REWRITE_TAC));
1484 BY(SET_TAC[Leaf_cell.WEDGE_SUBSET_WEDGE_GE]);
1485 BY(REWRITE_TAC[NEGLIGIBLE_EMPTY]);
1486 MATCH_MP_TAC NEGLIGIBLE_SUBSET;
1487 TYPIFY `affine hull {u,v,w1} UNION affine hull {u,v,w2}` EXISTS_TAC;
1489 MATCH_MP_TAC NEGLIGIBLE_UNION;
1490 BY(REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]);
1491 MATCH_MP_TAC SUBSET_TRANS;
1492 TYPIFY `aff_ge {u,v} {w1} UNION aff_ge {u,v} {w2}` EXISTS_TAC;
1494 INTRO_TAC Leaf_cell.WEDGE_WEDGE_GE [`u`;`v`;`w1`;`w2`];
1496 BY(ASM_REWRITE_TAC[]);
1498 TYPIFY `!(A:real^3->bool) B A' B'. A SUBSET A' /\ B SUBSET B' ==> (A UNION B) SUBSET (A' UNION B')` (C SUBGOAL_THEN MATCH_MP_TAC);
1500 TYPIFY `!(u:real^3) v w. {u,v,w} = {u,v} UNION {w}` (C SUBGOAL_THEN (unlist REWRITE_TAC));
1502 BY(REWRITE_TAC[AFF_GE_SUBSET_AFFINE_HULL])
1506 let MCELL2_SUBSET_AFF_GE = prove_by_refinement(
1507 `!V ul. packing V /\ saturated V /\ ul IN barV V 3 ==>
1508 mcell2 V ul SUBSET aff_ge {EL 0 ul, EL 1 ul} {mxi V ul, omega_list_n V ul 3}`,
1511 REPEAT WEAK_STRIP_TAC;
1512 REWRITE_TAC[SUBSET;Pack_defs.mcell2];
1515 REWRITE_TAC[LET_DEF;LET_END_DEF;EL;arith `1 = SUC 0`];
1517 BY(REWRITE_TAC[NOT_IN_EMPTY])
1521 let NOT_COPLANAR_EXTREME_MCELL2 = prove_by_refinement(
1522 `!V ul. packing V /\ saturated V /\ ul IN barV V 3 /\ ~NULLSET (mcell2 V ul) ==>
1523 ~coplanar { EL 0 ul, EL 1 ul, mxi V ul, omega_list_n V ul 3 }`,
1526 REPEAT WEAK_STRIP_TAC;
1527 FIRST_X_ASSUM_ST `~` MP_TAC;
1529 MATCH_MP_TAC COPLANAR_IMP_NEGLIGIBLE;
1530 MATCH_MP_TAC COPLANAR_SUBSET;
1531 TYPIFY `affine hull {EL 0 ul, EL 1 ul, mxi V ul, omega_list_n V ul 3}` EXISTS_TAC;
1533 BY(ASM_REWRITE_TAC[COPLANAR_AFFINE_HULL_COPLANAR]);
1534 MATCH_MP_TAC SUBSET_TRANS;
1535 TYPIFY `aff_ge {EL 0 ul, EL 1 ul} {mxi V ul, omega_list_n V ul 3}` EXISTS_TAC;
1536 ASM_SIMP_TAC[MCELL2_SUBSET_AFF_GE];
1537 TYPIFY `!a b c (d:real^3). {a,b,c,d} = {a,b} UNION {c,d}` (C SUBGOAL_THEN (unlist REWRITE_TAC));
1539 BY(REWRITE_TAC[AFF_GE_SUBSET_AFFINE_HULL])
1543 let MCELL2_DIHV_LT_PI = prove_by_refinement(
1544 `!V X ul. packing V /\ saturated V /\
1547 ~NULLSET X ==> dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) < pi`,
1550 REPEAT WEAK_STRIP_TAC;
1551 TYPIFY `~(dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) = pi)` ENOUGH_TO_SHOW_TAC;
1552 MATCH_MP_TAC (arith `(x <= pi) ==> (~(x = pi) ==> x < pi)`);
1553 BY(REWRITE_TAC[DIHV_RANGE]);
1554 TYPIFY `~coplanar { EL 0 ul, EL 1 ul, mxi V ul, omega_list_n V ul 3 }` ((C SUBGOAL_THEN ASSUME_TAC));
1555 BY(ASM_MESON_TAC[NOT_COPLANAR_EXTREME_MCELL2;IN]);
1556 TYPIFY `~collinear {EL 0 ul,EL 1 ul,mxi V ul} /\ ~collinear {EL 0 ul, EL 1 ul,omega_list_n V ul 3}` ((C SUBGOAL_THEN ASSUME_TAC));
1557 TYPIFY `!a b c (d:real^3). {a,b,c,d} = {a,b,d,c}` ((C SUBGOAL_THEN MP_TAC));
1559 BY(ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);
1560 BY(ASM_MESON_TAC[DIHV_EQ_0_PI_EQ_COPLANAR])
1564 let MCELL2_DIHV_AZIM = prove_by_refinement(
1565 `!V X ul h. packing V /\ saturated V /\
1568 ~NULLSET X ==> ?w1 w2. {w1,w2} = {mxi V ul,omega_list_n V ul 3} /\ dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) = azim (EL 0 ul) (EL 1 ul) w1 w2`,
1571 REPEAT WEAK_STRIP_TAC;
1572 INTRO_TAC NOT_COPLANAR_EXTREME_MCELL2 [`V`;`ul`];
1575 BY(ASM_MESON_TAC[IN]);
1577 TYPIFY `~collinear {EL 0 ul,EL 1 ul,mxi V ul} /\ ~collinear {EL 0 ul, EL 1 ul,omega_list_n V ul 3}` ((C SUBGOAL_THEN ASSUME_TAC));
1578 TYPIFY `!a b c (d:real^3). {a,b,c,d} = {a,b,d,c}` ((C SUBGOAL_THEN MP_TAC));
1580 BY(ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);
1581 TYPIFY `azim (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) <= pi` ASM_CASES_TAC;
1582 BY(ASM_MESON_TAC[Local_lemmas.AZIM_LE_PI_EQ_DIHV]);
1584 DISCH_THEN (MP_TAC o (ONCE_REWRITE_RULE[Rogers.AZIM_COMPL_EXT]));
1586 BY(ASM_MESON_TAC[PI_POS;arith `&0 < x ==> &0 <= x`]);
1588 TYPIFY `azim (EL 0 ul) (EL 1 ul) (omega_list_n V ul 3) (mxi V ul) <= pi` (C SUBGOAL_THEN ASSUME_TAC);
1589 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1590 ONCE_REWRITE_TAC[DIHV_SYM];
1591 TYPIFY `!b. {mxi V ul,b} = {b,mxi V ul}` (C SUBGOAL_THEN (unlist REWRITE_TAC));
1593 BY(ASM_MESON_TAC[Local_lemmas.AZIM_LE_PI_EQ_DIHV])
1597 let BIS_LE_NORM = prove_by_refinement(
1598 `!u (v:real^A). bis_le u v = { y | (y - u) dot (v - u) <= norm (v - u) pow 2 / &2}`,
1601 REWRITE_TAC[Packing3.BIS_LE_EQ_HALFSPACE;EXTENSION;IN_ELIM_THM;GSYM DOT_SQUARE_NORM];
1602 REPEAT WEAK_STRIP_TAC;
1603 MATCH_MP_TAC (arith `(a - b = &2 * (c - d)) ==> (a <= b <=> c <= d)`);
1604 REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL;DOT_RMUL;DOT_LSUB;DOT_RSUB];
1605 TYPIFY `x dot v = v dot x` (C SUBGOAL_THEN SUBST1_TAC);
1606 BY(VECTOR_ARITH_TAC);
1607 TYPIFY `x dot u = u dot x` (C SUBGOAL_THEN SUBST1_TAC);
1608 BY(VECTOR_ARITH_TAC);
1609 TYPIFY `v dot u = u dot v` (C SUBGOAL_THEN SUBST1_TAC);
1610 BY(VECTOR_ARITH_TAC);
1615 let BIS_LT_NORM = prove_by_refinement(
1616 `!u (v:real^A) x. dist(x,u) < dist(x,v) <=> (x - u) dot (v - u) < norm (v - u) pow 2 / &2`,
1619 REWRITE_TAC[Geomdetail.DIST_LT_HALF_PLANE;EXTENSION;IN_ELIM_THM;GSYM DOT_SQUARE_NORM];
1620 REPEAT WEAK_STRIP_TAC;
1621 MATCH_MP_TAC (arith `( &0 = b + &2 * (c - d)) ==> (&0 < b <=> c < d)`);
1622 REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL;DOT_RMUL;DOT_LSUB;DOT_RSUB];
1623 TYPIFY `x dot v = v dot x` (C SUBGOAL_THEN SUBST1_TAC);
1624 BY(VECTOR_ARITH_TAC);
1625 TYPIFY `x dot u = u dot x` (C SUBGOAL_THEN SUBST1_TAC);
1626 BY(VECTOR_ARITH_TAC);
1627 TYPIFY `v dot u = u dot v` (C SUBGOAL_THEN SUBST1_TAC);
1628 BY(VECTOR_ARITH_TAC);
1633 let SDIFF_SYM = prove_by_refinement(
1634 `!(X:A->bool) Y. SDIFF X Y = SDIFF Y X`,
1642 let MCELL2_VOL_SPLIT_EXPLICIT = prove_by_refinement(
1643 `!V X ul h. saturated V /\
1647 h = hl (truncate_simplex 1 ul) /\
1650 vol (X INTER bis_le (EL 0 ul) (EL 1 ul)) =
1651 dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) * (&2 - h pow 2) * h / &6`,
1654 REPEAT WEAK_STRIP_TAC;
1655 TYPIFY `dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) < pi` (C SUBGOAL_THEN ASSUME_TAC);
1656 MATCH_MP_TAC MCELL2_DIHV_LT_PI;
1657 BY(ASM_MESON_TAC[]);
1658 INTRO_TAC MCELL2_DIHV_AZIM [`V`;`X`;`ul`;`h`];
1660 BY(ASM_MESON_TAC[]);
1661 REPEAT WEAK_STRIP_TAC;
1663 INTRO_TAC NOT_COPLANAR_EXTREME_MCELL2 [`V`;`ul`];
1666 BY(ASM_MESON_TAC[IN]);
1668 TYPIFY `~collinear {EL 0 ul,EL 1 ul,mxi V ul} /\ ~collinear {EL 0 ul, EL 1 ul,omega_list_n V ul 3}` ((C SUBGOAL_THEN ASSUME_TAC));
1669 TYPIFY `!a b c (d:real^3). {a,b,c,d} = {a,b,d,c}` ((C SUBGOAL_THEN MP_TAC));
1671 BY(ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);
1672 TYPIFY `~collinear {EL 0 ul, EL 1 ul,w1} /\ ~collinear {EL 0 ul,EL 1 ul, w2}` (C SUBGOAL_THEN ASSUME_TAC);
1673 FIRST_X_ASSUM_ST `{a,b} = {c,d}` MP_TAC;
1674 REWRITE_TAC[Geomdetail.PAIR_EQ_EXPAND];
1675 BY(REPEAT WEAK_STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]);
1676 TYPIFY `&0 < h` (C SUBGOAL_THEN ASSUME_TAC);
1678 MATCH_MP_TAC Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT;
1679 BY(ASM_MESON_TAC[]);
1680 INTRO_TAC VOLUME_FRUSTT_WEDGE [`EL 0 ul`;`EL 1 ul`;`w1`;`w2`;`h`;`h / sqrt(&2)`];
1683 REWRITE_TAC[real_div];
1684 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
1685 GMATCH_SIMP_TAC REAL_LT_INV;
1686 GMATCH_SIMP_TAC REAL_LT_RSQRT;
1689 BY(ASM_MESON_TAC[]);
1690 REPEAT WEAK_STRIP_TAC;
1691 FIRST_X_ASSUM MP_TAC;
1694 FIRST_X_ASSUM_ST `\/` MP_TAC;
1695 ASM_SIMP_TAC[arith `&0 < h ==> ~(h < &0)`];
1696 GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
1697 GMATCH_SIMP_TAC REAL_LT_RSQRT;
1698 BY(REPEAT (FIRST_X_ASSUM_ST `<` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
1699 TYPIFY `(h / (h / sqrt(&2))) pow 2 = &2` (C SUBGOAL_THEN SUBST1_TAC);
1700 Calc_derivative.CALC_ID_TAC;
1702 REWRITE_TAC[GSYM Sphere.sqrt2;REAL_POW_MUL];
1703 REWRITE_TAC[Nonlin_def.sqrt2_sqrt2;REAL_POW_2];
1705 ASM_SIMP_TAC[arith `&0 < h ==> ~(h = &0)`;arith `~(&1 = &0)`];
1706 GMATCH_SIMP_TAC SQRT_EQ_0;
1709 DISCH_THEN (SUBST1_TAC o GSYM);
1710 MATCH_MP_TAC Vol1.VOLUME_PROPS_SDIFF;
1712 MATCH_MP_TAC MCELL2_INTER_BIS_LE_MEASURABLE;
1713 BY(ASM_MESON_TAC[]);
1715 FIRST_X_ASSUM_ST `frustt` MP_TAC;
1716 BY(ASM_REWRITE_TAC[]);
1717 GMATCH_SIMP_TAC MCELL2_SPLIT;
1718 TYPIFY `V` EXISTS_TAC;
1720 FIRST_X_ASSUM_ST `{a,b} = {c,d}` (ASSUME_TAC o GSYM);
1722 GMATCH_SIMP_TAC (GSYM Local_lemmas.WEDGE_GE_EQ_AFF_GE);
1725 BY(ASM_MESON_TAC[]);
1727 BY(ASM_MESON_TAC[]);
1728 ONCE_REWRITE_TAC[SDIFF_SYM];
1729 ONCE_REWRITE_TAC[SET_RULE `a INTER b INTER c = a INTER c INTER b`];
1730 REWRITE_TAC[BIS_LE_NORM];
1731 TYPIFY `hl (truncate_simplex 1 ul) = dist(EL 1 ul,EL 0 ul) / &2` (C SUBGOAL_THEN ASSUME_TAC);
1732 GMATCH_SIMP_TAC BARV3_TRUNC1;
1734 BY(ASM_MESON_TAC[IN]);
1735 ONCE_REWRITE_TAC[DIST_SYM];
1736 REWRITE_TAC[Marchal_cells_3.HL_2];
1738 TYPIFY `norm (EL 1 ul - EL 0 ul) pow 2 / &2 = hl (truncate_simplex 1 ul) * norm (EL 1 ul - EL 0 ul)` (C SUBGOAL_THEN SUBST1_TAC);
1739 ASM_REWRITE_TAC[dist];
1741 MATCH_MP_TAC FRUSTT_WEDGE_RCONE_GE;
1744 TYPIFY `&0 < sqrt(&2)` (C SUBGOAL_THEN ASSUME_TAC);
1745 GMATCH_SIMP_TAC REAL_LT_RSQRT;
1747 TYPIFY `&0 < hl(truncate_simplex 1 ul)` (C SUBGOAL_THEN ASSUME_TAC);
1748 BY(ASM_MESON_TAC[Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT]);
1750 GMATCH_SIMP_TAC REAL_LT_DIV;
1751 BY(ASM_REWRITE_TAC[]);
1754 BY(ASM_MESON_TAC[IN;MCELL2_VX_PROPS]);
1756 ASM_SIMP_TAC[arith `&0 < h ==> &0 <= h`];
1757 GMATCH_SIMP_TAC REAL_LE_LDIV_EQ;
1759 REWRITE_TAC[arith `&1 * x = x`];
1760 MATCH_MP_TAC (arith `x < y ==> x <= y`);
1765 let MCELL2_HL_LT_SQRT2 = prove_by_refinement(
1766 `!V ul. saturated V /\
1769 ~NULLSET (mcell2 V ul) ==>
1770 hl (truncate_simplex 1 ul) < sqrt(&2)
1774 REPEAT WEAK_STRIP_TAC;
1776 FIRST_X_ASSUM_ST `NULLSET` MP_TAC;
1777 BY(ASM_REWRITE_TAC[Pack_defs.mcell2;NEGLIGIBLE_EMPTY])
1781 let LEFT_ACTION_LIST_1_PROPERTIES_ALT = prove_by_refinement(
1787 hl (truncate_simplex 1 ul) < sqrt (&2) /\
1788 sqrt (&2) <= hl ul /\
1789 xl = left_action_list p ul
1790 ==> xl IN barV V 3 /\
1791 omega_list_n V xl 1 = omega_list_n V ul 1 /\
1792 omega_list_n V xl 2 = omega_list_n V ul 2 /\
1793 omega_list_n V xl 3 = omega_list_n V ul 3 /\
1794 mxi V xl = mxi V ul`,
1797 REWRITE_TAC[Marchal_cells_2_new.LEFT_ACTION_LIST_1_PROPERTIES]
1801 let MCELL2_PERMUTE_01 = prove_by_refinement(
1802 `!V ul. saturated V /\ packing V /\ barV V 3 ul /\ ~NULLSET (mcell2 V ul) ==>
1803 (?vl. (EL 0 ul = EL 1 vl) /\ (EL 1 ul = EL 0 vl) /\ (mxi V ul = mxi V vl) /\
1804 (omega_list_n V ul 3 = omega_list_n V vl 3) /\
1805 (hl (truncate_simplex 1 ul) = hl (truncate_simplex 1 vl)) /\
1806 (mcell2 V ul = mcell2 V vl) /\ barV V 3 vl)`,
1809 REPEAT WEAK_STRIP_TAC;
1810 TYPIFY `LENGTH ul = 4` (C SUBGOAL_THEN ASSUME_TAC);
1811 BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3 + 1 = 4`]);
1812 INTRO_TAC Bump.LENGTH4 [`ul`];
1814 BY(ASM_REWRITE_TAC[]);
1815 INTRO_TAC MCELL2_HL_LT_SQRT2 [`V`;`ul`];
1817 BY(ASM_MESON_TAC[]);
1818 REPEAT WEAK_STRIP_TAC;
1819 INTRO_TAC Leaf_cell.TWO_REARRANGEMENT_LEMMA_ALT [`V`;`ul`;`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`EL 3 ul`];
1821 BY(ASM_MESON_TAC[]);
1822 REPEAT WEAK_STRIP_TAC;
1823 TYPED_ABBREV_TAC `(vl:(real^3) list) = left_action_list p ul` ;
1824 TYPIFY `vl` EXISTS_TAC;
1825 INTRO_TAC LEFT_ACTION_LIST_1_PROPERTIES_ALT [`V`;`ul`;`vl`;`p`];
1829 FIRST_X_ASSUM_ST `mcell2` MP_TAC;
1830 BY(ASM_REWRITE_TAC[Pack_defs.mcell2;NEGLIGIBLE_EMPTY]);
1831 REWRITE_TAC[IN;Bump.MCELL2];
1832 REPEAT WEAK_STRIP_TAC;
1834 INTRO_TAC Rvfxzbu.RVFXZBU [`V`;`ul`;`2`;`p`];
1836 BY(ASM_REWRITE_TAC[arith `2 - 1 = 1`;IN_INSERT]);
1838 REWRITE_TAC[CONJ_ASSOC];
1840 BY(ASM_MESON_TAC[]);
1842 TYPIFY `LENGTH vl = 4` (C SUBGOAL_THEN ASSUME_TAC);
1843 BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3 + 1 = 4`]);
1844 INTRO_TAC Bump.LENGTH4 [`vl`];
1846 BY(ASM_REWRITE_TAC[]);
1848 FIRST_X_ASSUM_ST `~` MP_TAC;
1851 BY(ASM_MESON_TAC[CONS_11]);
1853 REWRITE_TAC[Pack_defs.HL];
1855 REPEAT (GMATCH_SIMP_TAC Bump.SET_OF_LIST_TRUNCATE_1);
1856 ASM_SIMP_TAC[arith `x = 4 ==> 2 <= x`];
1861 let MCELL2_VOL = prove_by_refinement(
1862 `!V X ul h. saturated V /\
1866 h = hl (truncate_simplex 1 ul) /\
1869 dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) * (&2 - h pow 2) * h / &3`,
1872 REPEAT WEAK_STRIP_TAC;
1873 INTRO_TAC MCELL2_VOL_SPLIT [`V`;`X`;`ul`];
1875 BY(ASM_MESON_TAC[]);
1876 DISCH_THEN SUBST1_TAC;
1877 MATCH_MP_TAC (arith `x = a/ &2 /\ y = a / &2 ==> (x + y = a)`);
1878 TYPIFY `h < sqrt(&2)` (C SUBGOAL_THEN ASSUME_TAC);
1880 BY(ASM_MESON_TAC[MCELL2_HL_LT_SQRT2]);
1881 COMMENT "first branch";
1883 INTRO_TAC MCELL2_VOL_SPLIT_EXPLICIT [`V`;`X`;`ul`;`h`];
1885 BY(ASM_MESON_TAC[]);
1886 DISCH_THEN SUBST1_TAC;
1888 COMMENT "second branch";
1889 INTRO_TAC MCELL2_PERMUTE_01 [`V`;`ul`];
1891 BY(ASM_MESON_TAC[]);
1892 REPEAT WEAK_STRIP_TAC;
1894 ONCE_REWRITE_TAC[Marchal_cells_2_new.DIHV_SYM];
1895 INTRO_TAC MCELL2_VOL_SPLIT_EXPLICIT [`V`;`X`;`vl`;`hl (truncate_simplex 1 vl)`];
1897 BY(ASM_MESON_TAC[]);
1899 DISCH_THEN SUBST1_TAC;
1904 let BALL_SUBSET_BIS_LE = prove_by_refinement(
1906 &2 * r <= dist(u,v) ==>
1907 ball(u,r) SUBSET bis_le u v`,
1910 REWRITE_TAC[ball;Sphere.bis_le;SUBSET;IN_ELIM_THM];
1911 REPEAT WEAK_STRIP_TAC;
1912 TYPIFY `dist(x,u) = dist(u,x)` (C SUBGOAL_THEN SUBST1_TAC);
1913 BY(MESON_TAC[DIST_SYM]);
1915 INTRO_TAC DIST_TRIANGLE [`u`;`x`;`v`];
1916 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
1920 let BALL_SUBSET_BIS_LT = prove_by_refinement(
1922 &2 * r <= dist(u,v) ==>
1923 ball(u,r) SUBSET {y | dist(y, u) < dist(y, v)}`,
1926 REWRITE_TAC[ball;Sphere.bis_le;SUBSET;IN_ELIM_THM];
1927 REPEAT WEAK_STRIP_TAC;
1928 TYPIFY `dist(x,u) = dist(u,x)` (C SUBGOAL_THEN SUBST1_TAC);
1929 BY(MESON_TAC[DIST_SYM]);
1931 INTRO_TAC DIST_TRIANGLE [`u`;`x`;`v`];
1932 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
1936 let RADIAL_LE = prove_by_refinement(
1937 `!r r' (x:real^3) C. r' <= r /\ &0 < r'
1938 ==> radial r x (C INTER ball( x, r))
1939 ==> radial r' x (C INTER ball( x, r'))`,
1942 BY(REWRITE_TAC[Marchal_cells_2_new.RADIAL_VS_RADIAL_NORM;GSYM NORMBALL_BALL;Conforming.RADIAL_NORM_CO])
1946 let MCELL2_SOL = prove_by_refinement(
1947 `!V X ul h. saturated V /\
1951 h = hl (truncate_simplex 1 ul) /\
1955 dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) * (&1 - h / sqrt(&2))`,
1958 REPEAT WEAK_STRIP_TAC;
1959 TYPIFY `dist(EL 0 ul,EL 1 ul) / &2 = hl (truncate_simplex 1 ul) ` (C SUBGOAL_THEN ASSUME_TAC);
1960 GMATCH_SIMP_TAC BARV3_TRUNC1;
1962 BY(ASM_MESON_TAC[IN]);
1963 REWRITE_TAC[Marchal_cells_3.HL_2];
1965 TYPIFY `!r. r < h ==> X INTER ball (EL 0 ul,r) = (X INTER bis_le (EL 0 ul) (EL 1 ul)) INTER ball(EL 0 ul,r)` (C SUBGOAL_THEN ASSUME_TAC);
1966 REPEAT WEAK_STRIP_TAC;
1967 TYPIFY `ball (EL 0 ul,r) SUBSET bis_le (EL 0 ul) (EL 1 ul)` ENOUGH_TO_SHOW_TAC;
1969 MATCH_MP_TAC BALL_SUBSET_BIS_LE;
1970 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1971 TYPIFY `&0 < sqrt(&2) ` (C SUBGOAL_THEN ASSUME_TAC);
1972 GMATCH_SIMP_TAC REAL_LT_RSQRT;
1974 TYPIFY `&0 < h` (C SUBGOAL_THEN ASSUME_TAC);
1976 MATCH_MP_TAC Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT;
1977 BY(ASM_MESON_TAC[]);
1978 TYPIFY `&0 < h / sqrt(&2) /\ h / sqrt(&2) < &1` (C SUBGOAL_THEN ASSUME_TAC);
1979 GMATCH_SIMP_TAC REAL_LT_DIV;
1981 BY(ASM_MESON_TAC[]);
1982 GMATCH_SIMP_TAC REAL_LT_LDIV_EQ;
1983 ASM_REWRITE_TAC[arith `(&1 * x = x)`];
1984 BY(ASM_MESON_TAC[]);
1985 COMMENT "0. basic setup of azim and dih";
1986 TYPIFY `dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) < pi` (C SUBGOAL_THEN ASSUME_TAC);
1987 MATCH_MP_TAC MCELL2_DIHV_LT_PI;
1988 BY(ASM_MESON_TAC[]);
1989 INTRO_TAC MCELL2_DIHV_AZIM [`V`;`X`;`ul`;`h`];
1991 BY(ASM_MESON_TAC[]);
1992 REPEAT WEAK_STRIP_TAC;
1994 COMMENT "show non-degeneracy";
1995 INTRO_TAC NOT_COPLANAR_EXTREME_MCELL2 [`V`;`ul`];
1998 BY(ASM_MESON_TAC[IN]);
2000 TYPIFY `~collinear {EL 0 ul,EL 1 ul,mxi V ul} /\ ~collinear {EL 0 ul, EL 1 ul,omega_list_n V ul 3}` ((C SUBGOAL_THEN ASSUME_TAC));
2001 TYPIFY `!a b c (d:real^3). {a,b,c,d} = {a,b,d,c}` ((C SUBGOAL_THEN MP_TAC));
2003 BY(ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);
2004 TYPIFY `~collinear {EL 0 ul, EL 1 ul,w1} /\ ~collinear {EL 0 ul,EL 1 ul, w2}` (C SUBGOAL_THEN ASSUME_TAC);
2005 FIRST_X_ASSUM_ST `{a,b} = {c,d}` MP_TAC;
2006 REWRITE_TAC[Geomdetail.PAIR_EQ_EXPAND];
2007 BY(REPEAT WEAK_STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]);
2009 TYPIFY `EL 0 ul IN V` (C SUBGOAL_THEN ASSUME_TAC);
2010 INTRO_TAC MCELL2_VX_PROPS [`V`;`X`;`ul`];
2012 BY(ASM_MESON_TAC[]);
2013 INTRO_TAC Bump.HDTFNFZ_ALT [`V`;`ul`;`2`;`X`];
2015 BY(ASM_MESON_TAC[Bump.MCELL2]);
2016 DISCH_THEN SUBST1_TAC;
2018 INTRO_TAC Urrphbz2.URRPHBZ2 [`V`;`ul`;`2`;`EL 0 ul`];
2020 BY(ASM_REWRITE_TAC[]);
2021 REWRITE_TAC[GSYM Bump.MCELL2];
2022 REWRITE_TAC[Sphere.eventually_radial];
2023 REPEAT WEAK_STRIP_TAC;
2025 TYPIFY `?r'. r' <= h /\ &0 < r' /\ radial r' (EL 0 ul) (mcell2 V ul INTER ball (EL 0 ul,r'))` (C SUBGOAL_THEN MP_TAC);
2026 TYPIFY `if (r <= h) then r else h` EXISTS_TAC;
2028 BY(ASM_REWRITE_TAC[arith `&0 < r <=> r > &0`]);
2029 REWRITE_TAC[arith `h <= h`];
2030 BY(ASM_MESON_TAC[RADIAL_LE;arith `~(r <= h) ==> (h <= r)`]);
2031 REPLICATE_TAC 2 (FIRST_X_ASSUM kill);
2032 REPEAT WEAK_STRIP_TAC;
2033 GMATCH_SIMP_TAC Vol1.sol_spec;
2034 TYPIFY `r'` EXISTS_TAC;
2035 ASM_REWRITE_TAC[arith `r' > &0 <=> &0 < r'`];
2037 MATCH_MP_TAC MEASURABLE_INTER;
2038 REWRITE_TAC[MEASURABLE_BALL;Bump.MCELL2];
2039 BY(ASM_MESON_TAC[Urrphbz1.MEASURABLE_MCELL]);
2041 COMMENT "1. done with sol ";
2042 INTRO_TAC MCELL2_VX_PROPS [`V`;`X`;`ul`];
2044 BY(ASM_MESON_TAC[]);
2045 REPEAT WEAK_STRIP_TAC;
2046 INTRO_TAC VOLUME_CONIC_CAP_STRONG [`EL 0 ul`;`EL 1 ul`;`r'`;`h/ sqrt(&2)`];
2048 BY(ASM_MESON_TAC[]);
2050 TYPIFY `~(&1 <= h / sqrt(&2))` (C SUBGOAL_THEN ASSUME_TAC);
2051 MATCH_MP_TAC (arith `a < b ==> ~(b <= a)`);
2052 BY(ASM_REWRITE_TAC[]);
2053 BY(ASM_MESON_TAC[arith `&0 < r' ==> ~(r' < &0)`]);
2054 REPEAT WEAK_STRIP_TAC;
2055 COMMENT "add wedge";
2056 INTRO_TAC Vol1.VOLUME_PROPS_CONIC_CAP [`EL 0 ul`;`EL 1 ul`;`w1`;`w2`;`r'`;`h / sqrt(&2)`];
2059 BY(ASM_MESON_TAC[arith `&0 < r' ==> r' >= &0`;arith `&0 < h' ==> h' >= -- &1`;arith `h' < &1 ==> h' <= &1`]);
2060 REWRITE_TAC[vol_conic_cap_wedge];
2061 TYPIFY `!v x. &3 * v / r' pow 3 = x <=> v = x * r' pow 3 / &3` (C SUBGOAL_THEN (unlist REWRITE_TAC));
2062 REPEAT WEAK_STRIP_TAC;
2063 MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a = b)`);
2064 CONJ_TAC THEN REPEAT WEAK_STRIP_TAC;
2066 Calc_derivative.CALC_ID_TAC;
2067 BY(ASM_MESON_TAC[arith `~(&3 = &0)`;arith `&0 < r' ==> ~(r' = &0)`]);
2069 Calc_derivative.CALC_ID_TAC;
2070 BY(ASM_MESON_TAC[arith `~(&3 = &0)`;arith `&0 < r' ==> ~(r' = &0)`]);
2071 ASM_REWRITE_TAC[GSYM REAL_MUL_ASSOC];
2072 DISCH_THEN (SUBST1_TAC o SYM);
2073 COMMENT "pure volumes left";
2074 MATCH_MP_TAC Vol1.VOLUME_PROPS_SDIFF;
2077 BY(REWRITE_TAC[MEASURABLE_CONIC_CAP_WEDGE]);
2078 REWRITE_TAC[conic_cap;NORMBALL_BALL];
2079 COMMENT "SDIFF to match volumes";
2080 ONCE_REWRITE_TAC[SDIFF_SYM];
2081 INTRO_TAC FRUSTT_WEDGE_RCONE_GE [`EL 0 ul`;`EL 1 ul`;`w1`;`w2`;`h`;`h/ sqrt(&2)`];
2084 BY(ASM_MESON_TAC[arith `h' < y ==> h' <= y`]);
2087 INTRO_TAC SDIFF_SUBSET [`(frustt (EL 0 ul) (EL 1 ul) (hl (truncate_simplex 1 ul)) (hl (truncate_simplex 1 ul) / sqrt (&2)) INTER wedge (EL 0 ul) (EL 1 ul) w1 w2)`;` (rcone_ge (EL 0 ul) (EL 1 ul) (hl (truncate_simplex 1 ul) / sqrt (&2)) INTER {y | (y - EL 0 ul) dot (EL 1 ul - EL 0 ul) <= hl (truncate_simplex 1 ul) * norm (EL 1 ul - EL 0 ul)} INTER wedge_ge (EL 0 ul) (EL 1 ul) w1 w2)`;`ball ((EL 0 ul),r')`];
2088 DISCH_THEN (MP_TAC o (MATCH_MP (REWRITE_RULE[TAUT `(a /\ b ==> c) <=> (b ==> (a ==> c))`] NEGLIGIBLE_SUBSET)));
2090 BY(ASM_REWRITE_TAC[]);
2091 COMMENT "match frustt";
2092 TYPIFY `(frustt (EL 0 ul) (EL 1 ul) (hl (truncate_simplex 1 ul)) (hl (truncate_simplex 1 ul) / sqrt (&2)) INTER wedge (EL 0 ul) (EL 1 ul) w1 w2) INTER ball (EL 0 ul,r') = (ball (EL 0 ul,r') INTER rcone_gt (EL 0 ul) (EL 1 ul) (hl (truncate_simplex 1 ul) / sqrt (&2))) INTER wedge (EL 0 ul) (EL 1 ul) w1 w2` (C SUBGOAL_THEN SUBST1_TAC);
2093 REWRITE_TAC[frustt;frustum;LET_DEF;EXTENSION;IN_ELIM_THM;LET_DEF;LET_END_DEF;IN_INTER];
2094 REPEAT WEAK_STRIP_TAC;
2095 REWRITE_TAC[arith `&0 * x = &0`];
2096 TYPIFY `~(x IN ball(EL 0 ul,r'))` ASM_CASES_TAC;
2097 BY(ASM_REWRITE_TAC[]);
2098 TYPIFY `~(x IN rcone_gt (EL 0 ul) (EL 1 ul) (hl (truncate_simplex 1 ul) / sqrt (&2)))` ASM_CASES_TAC;
2099 BY(ASM_MESON_TAC[IN]);
2100 TYPIFY `~(x IN wedge (EL 0 ul) (EL 1 ul) w1 w2)` ASM_CASES_TAC;
2101 BY(ASM_REWRITE_TAC[]);
2102 REPEAT (FIRST_X_ASSUM_ST `~ ~ x` MP_TAC) THEN REWRITE_TAC[] THEN REPEAT WEAK_STRIP_TAC THEN ASM_REWRITE_TAC[];
2104 BY(ASM_MESON_TAC[IN]);
2106 FIRST_X_ASSUM_ST `rcone_gt` MP_TAC;
2107 REWRITE_TAC[Sphere.rcone_gt;Sphere.rconesgn;IN_ELIM_THM];
2108 TYPIFY `&0 <= dist (x,EL 0 ul) * dist (EL 1 ul,EL 0 ul) * hl (truncate_simplex 1 ul) / sqrt (&2)` ENOUGH_TO_SHOW_TAC;
2110 GMATCH_SIMP_TAC REAL_LE_MUL;
2111 GMATCH_SIMP_TAC REAL_LE_MUL;
2112 REWRITE_TAC[DIST_POS_LE];
2113 MATCH_MP_TAC (arith `&0 < h' ==> &0 <= h'`);
2114 BY(ASM_MESON_TAC[]);
2115 INTRO_TAC BALL_SUBSET_BIS_LT [`EL 0 ul`;`EL 1 ul`;`r'`];
2117 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2118 REWRITE_TAC[SUBSET;IN_ELIM_THM];
2119 DISCH_THEN (C INTRO_TAC [`x`]);
2121 REWRITE_TAC[BIS_LT_NORM];
2122 ONCE_REWRITE_TAC[arith `x pow 2 / &2 = (x / &2) * x`];
2123 FIRST_X_ASSUM_ST `dist a / &2 = h` (SUBST1_TAC o GSYM);
2124 ONCE_REWRITE_TAC[DIST_SYM];
2125 BY(REWRITE_TAC[dist]);
2126 TYPIFY `((rcone_ge (EL 0 ul) (EL 1 ul) (hl (truncate_simplex 1 ul) / sqrt (&2)) INTER {y | (y - EL 0 ul) dot (EL 1 ul - EL 0 ul) <= hl (truncate_simplex 1 ul) * norm (EL 1 ul - EL 0 ul)} INTER wedge_ge (EL 0 ul) (EL 1 ul) w1 w2) INTER ball (EL 0 ul,r')) = (mcell2 V ul INTER ball (EL 0 ul,r'))` ENOUGH_TO_SHOW_TAC;
2127 DISCH_THEN SUBST1_TAC;
2129 TYPIFY `mcell2 V ul INTER ball (EL 0 ul,r') = mcell2 V ul INTER bis_le (EL 0 ul) (EL 1 ul) INTER ball (EL 0 ul,r')` (C SUBGOAL_THEN SUBST1_TAC);
2130 INTRO_TAC BALL_SUBSET_BIS_LE [`EL 0 ul`;`EL 1 ul`;`r'`];
2132 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2134 INTRO_TAC MCELL2_SPLIT [`V`;`mcell2 V ul`;`ul`];
2136 BY(ASM_MESON_TAC[]);
2137 REWRITE_TAC[GSYM INTER_ASSOC];
2138 DISCH_THEN SUBST1_TAC;
2139 FIRST_X_ASSUM_ST `{a,b} = {c,d}` (SUBST1_TAC o SYM);
2140 TYPIFY `wedge_ge (EL 0 ul) (EL 1 ul) w1 w2 = aff_ge {EL 0 ul, EL 1 ul} {w1,w2}` (C SUBGOAL_THEN SUBST1_TAC);
2141 MATCH_MP_TAC Local_lemmas.WEDGE_GE_EQ_AFF_GE;
2142 BY(ASM_MESON_TAC[]);
2143 REWRITE_TAC[BIS_LE_NORM];
2144 ONCE_REWRITE_TAC[arith `x pow 2 / &2 = (x / &2) * x`];
2145 FIRST_X_ASSUM_ST `dist a / &2 = h` (SUBST1_TAC o GSYM);
2146 ONCE_REWRITE_TAC[DIST_SYM];
2152 let gamma2_x_div_azim_v2 =
2153 new_definition `gamma2_x_div_azim_v2 m x = (&8 - x)* sqrt x / (&24) -
2154 ( &2 * (&2 * mm1/ pi) * (&1 - sqrt x / sqrt8) -
2155 (&8 * mm2 / pi) * m * lfun (sqrt x / &2))`;;
2158 let GAMMAX_GAMMA2_X = prove_by_refinement(
2159 `!V X ul y1 y2 y3 y4 y5 y6.
2165 y1 = dist(EL 0 ul,EL 1 ul) /\
2166 y2 = dist(EL 0 ul,mxi V ul) /\
2167 y3 = dist(EL 0 ul,omega_list_n V ul 3) /\
2168 y4 = dist(mxi V ul,omega_list_n V ul 3) /\
2169 y5 = dist(EL 1 ul,omega_list_n V ul 3) /\
2170 y6 = dist(EL 1 ul,mxi V ul)
2173 gamma2_x_div_azim_v2 (h0cut y1) (y1 * y1) * dih_y y1 y2 y3 y4 y5 y6`,
2176 REPEAT WEAK_STRIP_TAC;
2177 INTRO_TAC GAMMAX_MCELL2 [`V`;`X`;`ul`];
2179 BY(ASM_MESON_TAC[]);
2180 DISCH_THEN SUBST1_TAC;
2181 INTRO_TAC MCELL2_VOL [`V`;`X`;`ul`;`hl (truncate_simplex 1 ul)`];
2183 BY(ASM_MESON_TAC[]);
2184 DISCH_THEN SUBST1_TAC;
2185 INTRO_TAC MCELL2_HL_LT_SQRT2 [`V`;`ul`];
2187 BY(ASM_MESON_TAC[]);
2188 REPEAT WEAK_STRIP_TAC;
2189 INTRO_TAC MCELL2_SOL [`V`;`X`;`ul`;`hl (truncate_simplex 1 ul)`];
2191 BY(ASM_MESON_TAC[]);
2192 DISCH_THEN SUBST1_TAC;
2193 TYPIFY `sol (EL 1 ul) X = dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) * (&1 - hl (truncate_simplex 1 ul) / sqrt (&2))` (C SUBGOAL_THEN MP_TAC);
2194 INTRO_TAC MCELL2_PERMUTE_01 [`V`;`ul`];
2196 BY(ASM_MESON_TAC[]);
2197 REPEAT WEAK_STRIP_TAC;
2199 INTRO_TAC MCELL2_SOL [`V`;`X`;`vl`;`hl (truncate_simplex 1 vl)`];
2201 BY(ASM_MESON_TAC[]);
2203 DISCH_THEN SUBST1_TAC;
2204 BY(MESON_TAC[Marchal_cells_2_new.DIHV_SYM]);
2205 DISCH_THEN SUBST1_TAC;
2206 INTRO_TAC MCELL2_DIHX [`V`;`X`;`ul`];
2208 BY(ASM_MESON_TAC[]);
2209 DISCH_THEN SUBST1_TAC;
2210 REWRITE_TAC[arith `d * a - m * (d * a' + d * a') + m' * l * d = (a - &2 * m * a' + m' * l) * d`];
2211 MATCH_MP_TAC (arith `a = b /\ c = d ==> (a*c = b * d)`);
2212 COMMENT "show non-degeneracy";
2213 INTRO_TAC NOT_COPLANAR_EXTREME_MCELL2 [`V`;`ul`];
2216 BY(ASM_MESON_TAC[IN]);
2218 TYPIFY `~collinear {EL 0 ul,EL 1 ul,mxi V ul} /\ ~collinear {EL 0 ul, EL 1 ul,omega_list_n V ul 3}` ((C SUBGOAL_THEN ASSUME_TAC));
2219 TYPIFY `!a b c (d:real^3). {a,b,c,d} = {a,b,d,c}` ((C SUBGOAL_THEN MP_TAC));
2221 BY(ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);
2223 INTRO_TAC Merge_ineq.DIHV_EQ_DIH_Y [`EL 0 ul`;`EL 1 ul`;`mxi V ul`;`omega_list_n V ul 3`];
2225 BY(ASM_MESON_TAC[]);
2226 BY(REWRITE_TAC[LET_DEF;LET_END_DEF]);
2227 TYPED_ABBREV_TAC `(h:real) = hl (truncate_simplex 1 ul)` ;
2228 TYPIFY `dist(EL 0 ul,EL 1 ul) = &2 * hl (truncate_simplex 1 ul) ` (C SUBGOAL_THEN ASSUME_TAC);
2229 ONCE_REWRITE_TAC[arith `(x = &2 * h <=> x / &2 = h)`];
2230 GMATCH_SIMP_TAC BARV3_TRUNC1;
2232 BY(ASM_MESON_TAC[IN]);
2233 REWRITE_TAC[Marchal_cells_3.HL_2];
2236 REWRITE_TAC[gamma2_x_div_azim_v2];
2237 COMMENT "simplify polynomial identity";
2238 TYPIFY `&0 < h` (C SUBGOAL_THEN ASSUME_TAC);
2240 MATCH_MP_TAC Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT;
2241 BY(ASM_MESON_TAC[]);
2242 TYPIFY `[EL 0 ul; EL 1 ul] = truncate_simplex 1 ul` (C SUBGOAL_THEN SUBST1_TAC);
2243 BY(ASM_MESON_TAC[BARV3_TRUNC1;IN]);
2244 TYPIFY `sqrt((&2 * h) * (&2 * h)) = &2 * h` (C SUBGOAL_THEN SUBST1_TAC);
2245 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2246 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
2247 MATCH_MP_TAC (arith `(a = a') /\ (b = b') /\ (c = c') ==> a - b + c = a' - (b' - c')`);
2253 INTRO_TAC Merge_ineq.lmfun_h0cut [`(&2 * h)`];
2254 REWRITE_TAC[arith `(&2 * h) / &2 = h`];
2259 REWRITE_TAC[Nonlinear_lemma.sqrt8_sqrt2;Sphere.sqrt2];
2260 Calc_derivative.CALC_ID_TAC;
2261 REPEAT (GMATCH_SIMP_TAC SQRT_EQ_0);
2267 let GAMMAX_GAMMA2_X = prove_by_refinement(
2268 `!V X ul y1 y2 y3 y4 y5 y6.
2274 y1 = dist(EL 0 ul,EL 1 ul) /\
2275 y2 = dist(EL 0 ul,mxi V ul) /\
2276 y3 = dist(EL 0 ul,omega_list_n V ul 3) /\
2277 y4 = dist(mxi V ul,omega_list_n V ul 3) /\
2278 y5 = dist(EL 1 ul,omega_list_n V ul 3) /\
2279 y6 = dist(EL 1 ul,mxi V ul)
2281 &0 <= dih_y y1 y2 y3 y4 y5 y6 /\
2283 gamma2_x_div_azim_v2 (h0cut y1) (y1 * y1) * dih_y y1 y2 y3 y4 y5 y6`,
2286 REPEAT WEAK_STRIP_TAC;
2287 INTRO_TAC GAMMAX_MCELL2 [`V`;`X`;`ul`];
2289 BY(ASM_MESON_TAC[]);
2290 DISCH_THEN SUBST1_TAC;
2291 INTRO_TAC MCELL2_VOL [`V`;`X`;`ul`;`hl (truncate_simplex 1 ul)`];
2293 BY(ASM_MESON_TAC[]);
2294 DISCH_THEN SUBST1_TAC;
2295 INTRO_TAC MCELL2_HL_LT_SQRT2 [`V`;`ul`];
2297 BY(ASM_MESON_TAC[]);
2298 REPEAT WEAK_STRIP_TAC;
2299 INTRO_TAC MCELL2_SOL [`V`;`X`;`ul`;`hl (truncate_simplex 1 ul)`];
2301 BY(ASM_MESON_TAC[]);
2302 DISCH_THEN SUBST1_TAC;
2303 TYPIFY `sol (EL 1 ul) X = dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) * (&1 - hl (truncate_simplex 1 ul) / sqrt (&2))` (C SUBGOAL_THEN MP_TAC);
2304 INTRO_TAC MCELL2_PERMUTE_01 [`V`;`ul`];
2306 BY(ASM_MESON_TAC[]);
2307 REPEAT WEAK_STRIP_TAC;
2309 INTRO_TAC MCELL2_SOL [`V`;`X`;`vl`;`hl (truncate_simplex 1 vl)`];
2311 BY(ASM_MESON_TAC[]);
2313 DISCH_THEN SUBST1_TAC;
2314 BY(MESON_TAC[Marchal_cells_2_new.DIHV_SYM]);
2315 DISCH_THEN SUBST1_TAC;
2316 INTRO_TAC MCELL2_DIHX [`V`;`X`;`ul`];
2318 BY(ASM_MESON_TAC[]);
2319 DISCH_THEN SUBST1_TAC;
2320 REWRITE_TAC[arith `d * a - m * (d * a' + d * a') + m' * l * d = (a - &2 * m * a' + m' * l) * d`];
2321 MATCH_MP_TAC (arith `&0 <= c /\ a = b /\ c = d ==> (&0 <= d /\ a*c = b * d)`);
2323 BY(REWRITE_TAC[DIHV_RANGE]);
2324 COMMENT "show non-degeneracy";
2325 INTRO_TAC NOT_COPLANAR_EXTREME_MCELL2 [`V`;`ul`];
2328 BY(ASM_MESON_TAC[IN]);
2330 TYPIFY `~collinear {EL 0 ul,EL 1 ul,mxi V ul} /\ ~collinear {EL 0 ul, EL 1 ul,omega_list_n V ul 3}` ((C SUBGOAL_THEN ASSUME_TAC));
2331 TYPIFY `!a b c (d:real^3). {a,b,c,d} = {a,b,d,c}` ((C SUBGOAL_THEN MP_TAC));
2333 BY(ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);
2335 INTRO_TAC Merge_ineq.DIHV_EQ_DIH_Y [`EL 0 ul`;`EL 1 ul`;`mxi V ul`;`omega_list_n V ul 3`];
2337 BY(ASM_MESON_TAC[]);
2338 BY(REWRITE_TAC[LET_DEF;LET_END_DEF]);
2339 TYPED_ABBREV_TAC `(h:real) = hl (truncate_simplex 1 ul)` ;
2340 TYPIFY `dist(EL 0 ul,EL 1 ul) = &2 * hl (truncate_simplex 1 ul) ` (C SUBGOAL_THEN ASSUME_TAC);
2341 ONCE_REWRITE_TAC[arith `(x = &2 * h <=> x / &2 = h)`];
2342 GMATCH_SIMP_TAC BARV3_TRUNC1;
2344 BY(ASM_MESON_TAC[IN]);
2345 REWRITE_TAC[Marchal_cells_3.HL_2];
2348 REWRITE_TAC[gamma2_x_div_azim_v2];
2349 COMMENT "simplify polynomial identity";
2350 TYPIFY `&0 < h` (C SUBGOAL_THEN ASSUME_TAC);
2352 MATCH_MP_TAC Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT;
2353 BY(ASM_MESON_TAC[]);
2354 TYPIFY `[EL 0 ul; EL 1 ul] = truncate_simplex 1 ul` (C SUBGOAL_THEN SUBST1_TAC);
2355 BY(ASM_MESON_TAC[BARV3_TRUNC1;IN]);
2356 TYPIFY `sqrt((&2 * h) * (&2 * h)) = &2 * h` (C SUBGOAL_THEN SUBST1_TAC);
2357 GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2358 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
2359 MATCH_MP_TAC (arith `(a = a') /\ (b = b') /\ (c = c') ==> a - b + c = a' - (b' - c')`);
2365 INTRO_TAC Merge_ineq.lmfun_h0cut [`(&2 * h)`];
2366 REWRITE_TAC[arith `(&2 * h) / &2 = h`];
2371 REWRITE_TAC[Nonlinear_lemma.sqrt8_sqrt2;Sphere.sqrt2];
2372 Calc_derivative.CALC_ID_TAC;
2373 REPEAT (GMATCH_SIMP_TAC SQRT_EQ_0);
2382 let TSKAJXY_2 = prove_by_refinement(
2384 pack_nonlinear_non_ox3q1h /\ saturated V /\
2388 ==> gammaX V X lmfun >= &0`,
2391 REPEAT WEAK_STRIP_TAC;
2392 TYPIFY `NULLSET X` ASM_CASES_TAC;
2393 INTRO_TAC GAMMAX_NULLSET [`V`;`lmfun`;`X`;`ul`;`2`];
2395 BY(ASM_MESON_TAC[Bump.MCELL2]);
2397 INTRO_TAC GAMMAX_GAMMA2_X [`V`;`X`;`ul`;`dist(EL 0 ul,EL 1 ul)`;`dist(EL 0 ul,mxi V ul)`;`dist(EL 0 ul,omega_list_n V ul 3)`;`dist(mxi V ul,omega_list_n V ul 3)`;`dist(EL 1 ul,omega_list_n V ul 3)`;`dist(EL 1 ul,mxi V ul)`];
2399 REPEAT WEAK_STRIP_TAC;
2401 REWRITE_TAC[arith `a * b >= &0 <=> &0 <= a * b`];
2402 GMATCH_SIMP_TAC REAL_LE_MUL;
2404 TYPIFY ` (!y. &2 <= y /\ y <= sqrt8 ==> &0 <= gamma2_x_div_azim_v2 (h0cut y) (y * y))` (C SUBGOAL_THEN ASSUME_TAC);
2405 MATCH_MP_TAC Merge_ineq.GRKIBMP;
2406 INTRO_TAC (Merge_ineq.get_pack_nonlinear_non_ox3q1h "GRKIBMP A V2") [];
2407 INTRO_TAC (Merge_ineq.get_pack_nonlinear_non_ox3q1h "GRKIBMP B V2") [];
2409 FIRST_X_ASSUM MATCH_MP_TAC;
2410 INTRO_TAC MCELL2_VX_PROPS [`V`;`X`;`ul`];
2412 INTRO_TAC Bump.HDTFNFZ_ALT [`V`;`ul`;`2`;`X`];
2414 BY(ASM_MESON_TAC[Bump.MCELL2]);
2416 DISCH_THEN SUBST1_TAC;
2417 REPEAT WEAK_STRIP_TAC;
2418 TYPIFY `EL 0 ul IN V /\ EL 1 ul IN V` (C SUBGOAL_THEN ASSUME_TAC);
2419 BY(FIRST_X_ASSUM_ST `INTER` MP_TAC THEN SET_TAC[]);
2421 FIRST_X_ASSUM_ST `packing` MP_TAC;
2422 REWRITE_TAC[Sphere.packing];
2423 DISCH_THEN MATCH_MP_TAC;
2424 BY(ASM_MESON_TAC[IN]);
2425 INTRO_TAC MCELL2_HL_LT_SQRT2 [`V`;`ul`];
2427 BY(ASM_MESON_TAC[]);
2428 REWRITE_TAC[Nonlinear_lemma.sqrt8_sqrt2;Sphere.sqrt2];
2429 TYPIFY `dist(EL 0 ul,EL 1 ul) = &2 * hl (truncate_simplex 1 ul) ` (C SUBGOAL_THEN ASSUME_TAC);
2430 ONCE_REWRITE_TAC[arith `(x = &2 * h <=> x / &2 = h)`];
2431 GMATCH_SIMP_TAC BARV3_TRUNC1;
2433 BY(ASM_MESON_TAC[IN]);
2434 REWRITE_TAC[Marchal_cells_3.HL_2];
2441 let tsk_required_ineq =
2442 let cell3_hyp = ["QZECFIC wt0";"QZECFIC wt0 corner";"QZECFIC wt0 sqrt8";
2443 "QZECFIC wt1";"QZECFIC wt2 A";"CIHTIUM";"CJFZZDW";] in
2444 let tsk = ["TSKAJXY-GXSABWC DIV"; "TSKAJXY-IYOUOBF sharp v2";
2445 "TSKAJXY-IYOUOBF sym";
2446 "TSKAJXY-RIBCYXU sharp"; "TSKAJXY-RIBCYXU sym"; "TSKAJXY-TADIAMB";
2447 "TSKAJXY-WKGUESB sym"; "TSKAJXY-XLLIPLS"; "TSKAJXY-delta_x4";
2448 "TSKAJXY-eulerA"] in
2449 let grk = ["GRKIBMP A V2";"GRKIBMP B V2"] in
2450 cell3_hyp @ tsk @ grk;;
2452 let TSKAJXY = prove_by_refinement(
2454 pack_nonlinear_non_ox3q1h /\
2458 critical_edgeX V X = {}
2459 ==> gammaX V X lmfun >= &0`,
2462 REPEAT WEAK_STRIP_TAC;
2463 TYPIFY ` ~(?i ul. ul IN barV V 3 /\ (i = 1 \/ i = 2) /\ X = mcell i V ul)` ASM_CASES_TAC;
2464 INTRO_TAC Tskajxy_034.TSKAJXY_034 [];
2466 EVERY (map (fun t -> INTRO_TAC (Merge_ineq.get_pack_nonlinear_non_ox3q1h t) []) tsk_required_ineq);
2467 REPEAT WEAK_STRIP_TAC THEN ASM_REWRITE_TAC[];
2469 MATCH_MP_TAC Merge_ineq.GRKIBMP;
2470 BY(ASM_REWRITE_TAC[]);
2471 MATCH_MP_TAC Merge_ineq.cell3_from_ineq_thm;
2472 BY(ASM_REWRITE_TAC[]);
2473 REWRITE_TAC[Tskajxy_034.TSKAJXY_statement_special_case];
2474 DISCH_THEN MATCH_MP_TAC;
2475 BY(ASM_MESON_TAC[]);
2476 FIRST_X_ASSUM MP_TAC;
2478 REPEAT WEAK_STRIP_TAC;
2479 ASM_REWRITE_TAC[GSYM Bump.MCELL1];
2480 MATCH_MP_TAC TSKAJXY_1;
2481 BY(ASM_MESON_TAC[IN]);
2482 ASM_REWRITE_TAC[GSYM Bump.MCELL2];
2483 MATCH_MP_TAC TSKAJXY_2;
2484 BY(ASM_MESON_TAC[IN])