1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
10 (* Leaf and Cell Lemmas *)
12 module Leaf_cell = struct
17 let leaf = new_definition `leaf V ul <=> ul IN barV V 2 /\ hl ul < sqrt2`;;
19 let stem = new_definition `stem (ul:(A)list) = set_of_list (truncate_simplex 1 ul)`;;
21 (* START WITH GENERIC LEMMAS *)
23 let coplanar_eq_coplanar_alt = prove(
24 `!s:real^N->bool. 2 <= dimindex(:N) ==> (coplanar s <=> coplanar_alt s)`,
26 ASM_SIMP_TAC[COPLANAR; Collect_geom.coplanar_alt]);;
28 let RE_EQVL_IMP_SYM = prove_by_refinement(
29 `!a b. re_eqvl a b ==> re_eqvl b a`,
32 REWRITE_TAC[Trigonometry2.re_eqvl];
33 REPEAT WEAK_STRIP_TAC;
35 GMATCH_SIMP_TAC REAL_LT_INV;
37 Calc_derivative.CALC_ID_TAC;
38 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
42 let RE_EQVL_SYM = prove_by_refinement(
43 `!a b. re_eqvl a b <=> re_eqvl b a`,
46 MESON_TAC[RE_EQVL_IMP_SYM]
50 let RE_EQVL_SCALE1 = prove_by_refinement(
51 `!a b t. &0 < t ==> (re_eqvl (t * a) b <=> re_eqvl a b)`,
54 REWRITE_TAC[Trigonometry2.re_eqvl];
55 REPEAT WEAK_STRIP_TAC;
56 REWRITE_TAC[TAUT `(a <=> b) <=> ((a ==> b) /\ (b ==> a))`];
58 REPEAT WEAK_STRIP_TAC;
60 GMATCH_SIMP_TAC REAL_LT_DIV;
62 Calc_derivative.CALC_ID_TAC;
63 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
64 REPEAT WEAK_STRIP_TAC;
66 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
72 let RE_EQVL_SCALE2 = prove_by_refinement(
73 `!a b t. &0 < t ==> (re_eqvl a (t* b) <=> re_eqvl a b)`,
76 MESON_TAC[RE_EQVL_SCALE1;RE_EQVL_SYM]
80 let RE_EQVL_REFL = prove_by_refinement(
84 REWRITE_TAC[Trigonometry2.re_eqvl];
91 let WEDGE_GE_NULL = prove_by_refinement(
92 `!u0 u1 v1 v2. ~collinear {u0,u1,v1} /\ ~collinear {u0,u1,v2} /\ azim u0 u1 v1 v2 = &0 ==>
93 wedge_ge u0 u1 v1 v2 = aff_ge {u0,u1} {v1}`,
96 REPEAT WEAK_STRIP_TAC;
97 REWRITE_TAC[EXTENSION];
99 GMATCH_SIMP_TAC (GSYM Local_lemmas.AZIM_EQ_0_GE_ALT2);
100 REWRITE_TAC[Local_lemmas.WEDGE_GE_AZIM_LE];
102 INTRO_TAC Local_lemmas.AZIM_RANGE [`u0`;`u1`;`v1`;`x`];
107 let X_IN_AFF_GE_LEFT = prove_by_refinement(
108 `!(x:real^A) S U. (x IN S DIFF U) ==> (x IN aff_ge S U)`,
111 REPEAT WEAK_STRIP_TAC;
112 GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `aff_ge S U = aff_ge (S DIFF U) U`) SUBST1_TAC));
113 REWRITE_TAC[Sphere.aff_ge_def];
114 BY(MESON_TAC[ AFFSIGN_DISJOINT_DIFF]);
115 MATCH_MP_TAC Packing3.IN_TRANS;
116 GOAL_TERM (fun w -> (EXISTS_TAC ( env w`aff_ge (S DIFF U) {}`)));
118 MATCH_MP_TAC AFF_GE_MONO_RIGHT;
120 REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL];
121 MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
122 BY(ASM_REWRITE_TAC[])
126 let WEDGE_WEDGE_GE = prove_by_refinement(
127 `!u0 u1 v1 v2. ~collinear {u0,u1,v1} /\ ~collinear {u0,u1,v2} ==>
128 wedge_ge u0 u1 v1 v2 SUBSET wedge u0 u1 v1 v2 UNION aff_ge {u0,u1} {v1} UNION aff_ge {u0,u1} {v2}`,
131 REPEAT WEAK_STRIP_TAC;
133 REWRITE_TAC[IN_UNION];
134 REWRITE_TAC[Local_lemmas.WEDGE_GE_AZIM_LE];
135 REPEAT WEAK_STRIP_TAC;
136 GOAL_TERM (fun w -> (ASM_CASES_TAC ( env w `x IN affine hull {u0,u1}`)));
137 INTRO_TAC AFFINE_HULL_SUBSET_AFF_GE [`{u0,u1}`;`{v1}`];
140 REWRITE_TAC[DISJOINT];
141 REWRITE_TAC[Collect_geom2.INTER_DISJONT_EX];
142 REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
143 GOAL_TERM (fun w -> (SUBGOAL_THEN ( env w `{u0,u1,v1} = {v1,u0,u1}`) ASSUME_TAC));
145 BY(ASM_MESON_TAC[Collect_geom.NOT_COLLINEAR_IMP_2_UNEQUAL]);
147 GMATCH_SIMP_TAC WEDGE_ALT;
148 REWRITE_TAC[IN_ELIM_THM];
151 BY(ASM_MESON_TAC[Collect_geom.NOT_COLLINEAR_IMP_2_UNEQUAL]);
153 GOAL_TERM (fun w -> (ENOUGH_TO_SHOW_TAC ( env w `(azim u0 u1 v1 x = &0 ==> x IN aff_ge {u0,u1} {v1}) /\ (azim u0 u1 v1 x = azim u0 u1 v1 v2 ==> x IN aff_ge {u0,u1} {v2})`)));
154 INTRO_TAC Local_lemmas.AZIM_RANGE [`u0`;`u1`;`v1`;`x`];
155 FIRST_X_ASSUM_ST `azim` MP_TAC;
156 BY(MESON_TAC[arith `x <= y ==> x = y \/ x < y`]);
157 GMATCH_SIMP_TAC (Local_lemmas.AZIM_EQ_0_GE_ALT2);
159 GMATCH_SIMP_TAC (GSYM Local_lemmas.AZIM_EQ_0_GE_ALT2);
161 ONCE_REWRITE_TAC[arith `x = azim a b c d <=> azim a b c d = x`];
162 GMATCH_SIMP_TAC AZIM_EQ;
163 GMATCH_SIMP_TAC Local_lemmas.AZIM_EQ_0_GE_ALT2;
165 INTRO_TAC AFF_GT_SUBSET_AFF_GE [`{u0,u1}`;`{v2}`];
167 DISCH_THEN (unlist REWRITE_TAC);
168 GMATCH_SIMP_TAC COLLINEAR_3_AFFINE_HULL;
169 BY(ASM_REWRITE_TAC[])
173 let WEDGE_GE_ALMOST_DISJOINT = prove_by_refinement(
174 `!u0 u1 v1 v2. ~collinear {u0,u1,v1} /\ ~collinear {u0,u1,v2} ==>
175 wedge_ge u0 u1 v1 v2 INTER wedge_ge u0 u1 v2 v1 SUBSET aff_ge {u0,u1} {v1} UNION aff_ge {u0,u1} {v2}
179 REPEAT WEAK_STRIP_TAC;
180 ASM_CASES_TAC `azim u0 u1 v1 v2 = &0`;
181 MATCH_MP_TAC SUBSET_TRANS;
182 GOAL_TERM (fun w -> (EXISTS_TAC ( env w `wedge_ge u0 u1 v1 v2`)));
185 GMATCH_SIMP_TAC WEDGE_GE_NULL;
188 SUBGOAL_THEN `&0 < azim u0 u1 v1 v2` ASSUME_TAC;
189 MATCH_MP_TAC (arith `~(x = &0) /\ (&0 <= x) ==> (&0 < x)`);
190 BY(ASM_REWRITE_TAC[Local_lemmas.AZIM_RANGE;]);
191 INTRO_TAC WEDGE_WEDGE_GE [`u0`;`u1`;`v1`;`v2`];
192 INTRO_TAC WEDGE_WEDGE_GE [`u0`;`u1`;`v2`;`v1`];
194 GOAL_TERM (fun w -> (ENOUGH_TO_SHOW_TAC ( env w `wedge u0 u1 v1 v2 INTER wedge u0 u1 v2 v1 = {}`)));
196 INTRO_TAC Counting_spheres.WEDGE_ORDER_DISJOINT [`u0`;`u1`;`v1`;`2`;`\ i. if (i=2) then v2 else v1`];
198 REWRITE_TAC[arith `~(2 + 1 = 2) /\ ~(1 = 2)`];
199 REWRITE_TAC[IN_NUMSEG];
200 REWRITE_TAC[arith `!i. (1 <= i /\ i <= 2) <=> (i = 1 \/ i = 2)`];
203 REPEAT WEAK_STRIP_TAC;
204 FIRST_X_ASSUM MP_TAC;
205 BY(ASM_REWRITE_TAC[arith `~(1=2)`]);
206 FIRST_X_ASSUM MP_TAC;
207 BY(ASM_REWRITE_TAC[]);
208 REWRITE_TAC[arith `! j k. ((j = 1 \/ j = 2) /\ (k = 1 \/ k = 2) /\ j < k) <=> (j=1 /\ k=2)`];
209 REPEAT WEAK_STRIP_TAC;
210 ASM_REWRITE_TAC[arith `~(1=2)`];
211 BY(ASM_REWRITE_TAC[AZIM_REFL]);
212 DISCH_THEN (C INTRO_TAC [`1`;`2`]);
213 BY(REWRITE_TAC[arith `~(1=2) /\ (1 + 1 = 2) /\ ~(2 + 1 = 2)`])
217 let AFF_DIM_3 = prove_by_refinement(
218 `!a (b:real^A) c. aff_dim {a,b,c} <= &2`,
221 ONCE_REWRITE_TAC[AFF_DIM_INSERT];
222 REWRITE_TAC[AFF_DIM_2];
223 REPEAT WEAK_STRIP_TAC;
224 BY(REPEAT COND_CASES_TAC THEN INT_ARITH_TAC)
228 let COPLANAR_IMP_AFF_DIM = prove_by_refinement(
229 `!(s:real^A->bool). coplanar s ==> aff_dim s <= &2`,
232 REWRITE_TAC[Trigonometry2.coplanar];
233 REPEAT WEAK_STRIP_TAC;
234 MATCH_MP_TAC INT_LE_TRANS;
235 TYPIFY `aff_dim (affine hull {u,v,w})` EXISTS_TAC;
237 MATCH_MP_TAC AFF_DIM_SUBSET;
238 BY(ASM_REWRITE_TAC[]);
239 REWRITE_TAC[AFF_DIM_AFFINE_HULL];
240 ONCE_REWRITE_TAC[AFF_DIM_INSERT];
241 REWRITE_TAC[AFF_DIM_2];
242 BY(REPEAT COND_CASES_TAC THEN INT_ARITH_TAC)
246 let COPLANAR_INSERT = prove_by_refinement(
247 `!s (p:real^A). aff_dim s = &2 /\ coplanar (p INSERT s) ==> p IN affine hull s`,
250 REPEAT WEAK_STRIP_TAC;
251 FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP COPLANAR_IMP_AFF_DIM));
252 FIRST_X_ASSUM_ST `INSERT` MP_TAC;
253 REWRITE_TAC[AFF_DIM_INSERT];
255 COND_CASES_TAC THEN REWRITE_TAC[];
260 let COPLANAR_UNION = prove_by_refinement(
261 `!P Q (a:real^A) b. ~(P = {}) /\ ~(Q = {}) /\
262 (!p. p IN P ==> ~collinear {p,a,b}) /\
263 (!q. q IN Q ==> ~collinear {q,a,b}) /\
264 (! p q. p IN P /\ q IN Q ==> coplanar {p,q,a,b}) ==>
265 coplanar (P UNION Q UNION {a,b})
269 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY];
270 REPEAT WEAK_STRIP_TAC;
271 ABBREV_TAC `(E:real^A->bool) = affine hull {x,a,b}`;
272 TYPIFY `aff_dim {x,a,b} = &2 /\ aff_dim {x',a,b} = &2` (C SUBGOAL_THEN ASSUME_TAC);
273 INTRO_TAC COLLINEAR_AFF_DIM [`{x,a,b}`];
274 INTRO_TAC COLLINEAR_AFF_DIM [`{x',a,b}`];
276 INTRO_TAC AFF_DIM_3 [`x`;`a`;`b`];
277 INTRO_TAC AFF_DIM_3 [`x'`;`a`;`b`];
279 TYPIFY `Q SUBSET E` (C SUBGOAL_THEN ASSUME_TAC);
281 REPEAT WEAK_STRIP_TAC;
283 MATCH_MP_TAC COPLANAR_INSERT;
285 TYPIFY `{x'',x,a,b} = {x,x'',a,b}` (C SUBGOAL_THEN SUBST1_TAC);
288 TYPIFY `affine hull {x',a,b} = E` (C SUBGOAL_THEN ASSUME_TAC);
290 TYPIFY `affine hull {x,a,b} = affine hull (affine hull {x,a,b})` (C SUBGOAL_THEN SUBST1_TAC);
291 BY(REWRITE_TAC[Planarity.AFFINE_HULL_AFFINE_EQ]);
292 MATCH_MP_TAC AFF_DIM_EQ_AFFINE_HULL;
294 TYPIFY `x' IN affine hull {x,a,b} /\ {a,b} SUBSET affine hull {x,a,b}` ENOUGH_TO_SHOW_TAC;
297 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
298 MATCH_MP_TAC SUBSET_TRANS;
299 TYPIFY `{x,a,b}` EXISTS_TAC;
302 BY(REWRITE_TAC[HULL_SUBSET]);
303 ASM_REWRITE_TAC[AFF_DIM_AFFINE_HULL];
305 TYPIFY `P SUBSET E` (C SUBGOAL_THEN ASSUME_TAC);
307 REPEAT WEAK_STRIP_TAC;
309 MATCH_MP_TAC COPLANAR_INSERT;
311 REWRITE_TAC[coplanar];
312 GEXISTL_TAC [`x'`;`a`;`b`];
313 TYPIFY `P UNION Q SUBSET affine hull {x',a,b} /\ {a,b} SUBSET {x',a,b} /\ {x',a,b} SUBSET affine hull {x',a,b}` ENOUGH_TO_SHOW_TAC;
316 REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC);
318 REWRITE_TAC[HULL_SUBSET];
323 let CONNECTED_SEGMENT_NOT_COVERED = prove_by_refinement(
324 `!(A:real^A -> bool) B a b. (open) A /\ (open) B /\ a IN A /\ b IN B /\ (A INTER B = {}) ==>
325 (?x. x IN segment [a,b] /\ ~(x IN A) /\ ~(x IN B)) `,
328 REPEAT WEAK_STRIP_TAC;
329 TYPIFY `(!x. x IN segment [a,b] ==> (x IN A) \/ (x IN B)) ==> F ` ENOUGH_TO_SHOW_TAC;
332 INTRO_TAC (CONJUNCT1 CONNECTED_SEGMENT) [`a`;`b`];
333 REWRITE_TAC[connected];
334 GEXISTL_TAC [`A`;`B`];
337 BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]);
339 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
340 INTRO_TAC ENDS_IN_SEGMENT [`a`;`b`];
341 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[])
345 (* END OF GENERIC LEMMAS *)
347 let GBEWYFX = prove_by_refinement(
348 `!V ul. packing V /\ saturated V /\ leaf V ul ==>
349 ~(collinear (set_of_list ul)) `,
352 REWRITE_TAC[leaf;IN;COLLINEAR_AFF_DIM];
353 REPEAT WEAK_STRIP_TAC;
354 INTRO_TAC Rogers.MHFTTZN1 [`V`;`ul`;`2`];
356 FIRST_X_ASSUM MP_TAC;
361 let NWVRFMF = prove_by_refinement(
362 `!V ul p. packing V /\ saturated V /\ leaf V ul /\ {p} facet_of (voronoi_list V ul) ==>
363 (?vl. vl IN barV V 3 /\ truncate_simplex 2 vl = ul /\ omega_list V vl = p)`,
366 REWRITE_TAC[leaf;IN];
367 REPEAT WEAK_STRIP_TAC;
368 INTRO_TAC Rogers.IDBEZAL [`V`;`ul`;`2`;`{p}`];
369 ASM_REWRITE_TAC[arith `2 < 3`;arith `2 + 1 = 3`];
370 REPEAT WEAK_STRIP_TAC;
371 TYPIFY `vl` EXISTS_TAC;
373 INTRO_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST [`V`;`vl`;`3`];
375 BY(ASM_MESON_TAC[IN_SING])
379 let YBZFUPO = prove_by_refinement(
380 `!V ul. packing V /\ saturated V /\ leaf V ul ==>
381 (?p1 p2. voronoi_list V ul = convex hull {p1,p2} /\ ~(p1 = p2) /\
382 (!f. f facet_of voronoi_list V ul <=> f IN {{p1},{p2}}))`,
385 REWRITE_TAC[leaf;IN];
386 REPEAT WEAK_STRIP_TAC;
387 INTRO_TAC Packing3.AFF_DIM_VORONOI_LIST [`V`;`ul`;`2`];
388 ASM_REWRITE_TAC[arith `&3 - int_of_num 2 = &1`];
390 INTRO_TAC Polyhedron.EXPAND_EDGE_POLYTOPE [`voronoi_list V ul`;`voronoi_list V ul`];
392 GMATCH_SIMP_TAC FACE_OF_REFL;
393 REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST];
394 GMATCH_SIMP_TAC Packing3.POLYTOPE_VORONOI_LIST_BARV;
397 BY(ASM_REWRITE_TAC[]);
398 REPEAT WEAK_STRIP_TAC;
400 TYPIFY `a` EXISTS_TAC;
401 TYPIFY `b` EXISTS_TAC;
403 BY(REWRITE_TAC[SEGMENT_CONVEX_HULL]);
405 INTRO_TAC EXTREME_POINT_OF_SEGMENT [`a`;`b`;`a`];
406 INTRO_TAC EXTREME_POINT_OF_SEGMENT [`a`;`b`;`b`];
407 INTRO_TAC EXTREME_POINT_OF_SEGMENT [`a`;`b`];
409 REWRITE_TAC[GSYM FACE_OF_SING];
410 REWRITE_TAC[facet_of];
411 REPEAT WEAK_STRIP_TAC;
414 INTRO_TAC (CONJUNCT1 SEGMENT_EQ_SING) [`b`;`b`;`b`];
417 FIRST_X_ASSUM_ST `voronoi_list` MP_TAC;
418 FIRST_X_ASSUM_ST `convex` kill;
421 FIRST_X_ASSUM_ST `1` MP_TAC;
423 REWRITE_TAC[AFF_DIM_SING];
427 TYPIFY `{{a},{b}} f <=> f IN {{a},{b}}` (C SUBGOAL_THEN SUBST1_TAC);
429 REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
430 TYPIFY `aff_dim(segment[a,b]) - &1 = &0` (C SUBGOAL_THEN SUBST1_TAC);
431 BY(ASM_MESON_TAC[arith ` &1 - int_of_num 1 = &0`]);
432 REWRITE_TAC[AFF_DIM_EQ_0];
433 SUBGOAL_THEN `!(x:real^3). ~({x} = {})` ASSUME_TAC;
435 REWRITE_TAC[TAUT `(b <=> a) <=> ((a ==> b) /\ (b ==> a))`];
437 BY(DISCH_THEN DISJ_CASES_TAC THEN ASM_MESON_TAC[]);
438 REPEAT WEAK_STRIP_TAC;
443 let PERMUTES_a_PERMUTES_b = prove_by_refinement(
444 `!p a b. a <= b /\ p permutes 0..a ==> p permutes 0..b`,
447 REWRITE_TAC[permutes;IN_NUMSEG];
448 REPEAT WEAK_STRIP_TAC;
450 REPEAT WEAK_STRIP_TAC;
451 FIRST_X_ASSUM MATCH_MP_TAC;
452 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC)
456 let PERMUTE_BARV3 = prove_by_refinement(
457 `!V ul p. packing V /\ saturated V /\ ul IN barV V 3 /\
458 hl (truncate_simplex 2 ul) < sqrt2 /\ p permutes 0..1 ==>
459 left_action_list p ul IN barV V 3`,
462 REPEAT WEAK_STRIP_TAC;
463 TYPIFY `hl ul < sqrt2` ASM_CASES_TAC;
464 MATCH_MP_TAC Rogers.YIFVQDV_1;
465 ASM_REWRITE_TAC[GSYM Sphere.sqrt2];
466 MATCH_MP_TAC PERMUTES_a_PERMUTES_b;
467 BY(ASM_MESON_TAC[arith `1 <= 3`]);
468 INTRO_TAC Ynhyjit.YNHYJIT [`V`;`ul`;`3`;`p`;`left_action_list p ul`];
469 ASM_SIMP_TAC[GSYM Sphere.sqrt2;arith `3 -1 = 2`];
470 ASM_SIMP_TAC[arith `~(x < y) ==> y <= x`];
473 BY(ASM_MESON_TAC[IN]);
476 MATCH_MP_TAC PERMUTES_a_PERMUTES_b;
477 BY(ASM_MESON_TAC[arith `1 <= 2`]);
482 let ZASUVOR = prove_by_refinement(
483 `!V u0 u1 u2. packing V /\ saturated V /\ leaf V [u0;u1;u2] ==>
484 leaf V [u1;u0;u2] /\ (stem [u0;u1;u2] = stem [u1;u0;u2])`,
487 REPEAT WEAK_STRIP_TAC;
488 INTRO_TAC YBZFUPO [`V`;`[u0;u1;u2]`];
490 REPEAT WEAK_STRIP_TAC;
491 INTRO_TAC NWVRFMF [`V`;`[u0;u1;u2]`;`p1`];
492 FIRST_X_ASSUM_ST `convex` kill;
494 REWRITE_TAC[IN_INSERT];
495 REPEAT WEAK_STRIP_TAC;
496 INTRO_TAC PERMUTES_SWAP [`0`;`1`;`0..1`];
498 REWRITE_TAC[IN_NUMSEG];
503 REWRITE_TAC[Marchal_cells.TRUNCATE_SIMPLEX_EXPLICIT_1];
504 REWRITE_TAC[set_of_list];
506 SUBGOAL_THEN `left_action_list (swap(0,1)) vl IN barV V 3` ASSUME_TAC;
507 MATCH_MP_TAC PERMUTE_BARV3;
509 BY(ASM_MESON_TAC[leaf]);
510 FIRST_X_ASSUM_ST `leaf` MP_TAC;
511 REWRITE_TAC[leaf;IN];
512 REWRITE_TAC[Pack_defs.HL;set_of_list];
513 REPEAT WEAK_STRIP_TAC;
514 TYPIFY `{u1,u0,u2} = {u0,u1,u2}` (C SUBGOAL_THEN SUBST1_TAC);
517 INTRO_TAC Packing3.TRUNCATE_SIMPLEX_BARV [`V`;`2`;`3`;`left_action_list (swap(0,1)) vl`];
519 BY(ASM_MESON_TAC[IN;arith `2 <= 3`]);
520 TYPIFY `truncate_simplex 2 (left_action_list (swap (0,1)) vl) = [u1;u0;u2]` ENOUGH_TO_SHOW_TAC;
521 DISCH_THEN SUBST1_TAC;
523 TYPIFY `?w. left_action_list (swap (0,1)) vl = [u1;u0;u2;w]` ENOUGH_TO_SHOW_TAC;
524 REPEAT WEAK_STRIP_TAC;
526 BY(REWRITE_TAC[Marchal_cells.TRUNCATE_SIMPLEX_EXPLICIT_2]);
527 TYPIFY `EL 3 vl` EXISTS_TAC;
528 REWRITE_TAC[Pack_defs.left_action_list];
529 REWRITE_TAC[Packing3.LIST_EL_EQ];
530 TYPIFY `LENGTH vl = 4` (C SUBGOAL_THEN ASSUME_TAC);
531 REPEAT (FIRST_X_ASSUM_ST `barV` MP_TAC);
532 REWRITE_TAC[Sphere.BARV;IN];
533 BY(MESON_TAC[arith `3 + 1 = 4`]);
534 REWRITE_TAC[Packing3.LENGTH_TABLE];
540 SIMP_TAC[Packing3.EL_TABLE];
541 REWRITE_TAC[INVERSE_SWAP];
542 REWRITE_TAC[arith `j< 4 <=> (j = 0 \/ j = 1 \/ j = 2 \/ j = 3)`];
543 INTRO_TAC (GSYM Packing3.EL_TRUNCATE_SIMPLEX) [`vl`;`2`];
544 ASM_REWRITE_TAC[arith `2 + 1 <= 4`];
545 BY(REPEAT WEAK_STRIP_TAC THEN ASM_SIMP_TAC[swap;EL;HD;arith `0 <= 2 /\ 1 <= 2 /\ 2 <= 2 /\ ~(1 = 0) /\ ~(2 = 1) /\ ~(2=0) /\ ~(3=0) /\ ~(3=1)`] THEN REWRITE_TAC[arith `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`;EL;HD;TL])
549 let NORM_FLATTEN = prove_by_refinement(
550 `!u w (p:real^A). norm (u - p) pow 2 - norm (w - p) pow 2 = (u dot u) - (w dot w) + &2 % (w - u) dot p`,
553 REPEAT WEAK_STRIP_TAC;
554 REWRITE_TAC[NORM_POW_2];
559 let truncate_set_of_list = prove_by_refinement(
560 `!(vl:(A)list) k. 0 < k /\ LENGTH vl = (k+1) ==>
561 set_of_list vl SUBSET set_of_list(truncate_simplex (k-1) vl) UNION {EL k vl}`,
564 REPEAT WEAK_STRIP_TAC;
566 REWRITE_TAC[IN_SET_OF_LIST;IN_UNION;IN_SING];
567 REWRITE_TAC[MEM_EXISTS_EL];
568 REPEAT WEAK_STRIP_TAC;
569 GMATCH_SIMP_TAC Packing3.LENGTH_TRUNCATE_SIMPLEX;
570 TYPIFY `k - 1 + 1 = k` (C SUBGOAL_THEN SUBST1_TAC);
571 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
573 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
574 ASM_CASES_TAC `i = (k:num)`;
575 BY(ASM_REWRITE_TAC[]);
578 GMATCH_SIMP_TAC Packing3.EL_TRUNCATE_SIMPLEX;
580 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC)
584 let DIST_LE_HALF_PLANE = prove_by_refinement(
585 `!x:real^A a:real^A b:real^A.
586 dist(x,a) <= dist(x,b) <=> &0 <= (a - b) dot (&2 % x - (a + b))`,
588 ABBREV_TAC ` an a b x = ((a:real^A) - b) dot (&2 % x - (a + b))`;
589 REWRITE_TAC[dist; vector_norm];
590 REWRITE_TAC[MESON[DOT_POS_LE; SQRT_MONO_LE_EQ]` sqrt ( x dot x) <= sqrt (y dot y) <=> x dot x <= y dot y `];
591 REWRITE_TAC[DOT_LSUB; DOT_RSUB];
593 ONCE_REWRITE_TAC[ GSYM REAL_SUB_LE];
594 REWRITE_TAC[ REAL_ARITH ` x dot x - b dot x - (b dot x - b dot b) - (x dot x - a dot x - (a dot x - a dot a)) = &2 * (a dot x - b dot x) + b dot b - a dot a`];
595 REWRITE_TAC[GSYM DOT_LSUB; GSYM DOT_RMUL];
597 TYPIFY `(a - b) dot &2 % x + b dot b - a dot a = (a - b) dot (&2 % x - (a + b))` (C SUBGOAL_THEN SUBST1_TAC);
598 BY(VECTOR_ARITH_TAC);
599 REWRITE_TAC[arith `x - &0 = x`];
603 let DIST_EQ_HALF_PLANE = prove_by_refinement(
604 `!x:real^A a:real^A b:real^A.
605 dist(x,a) = dist(x,b) <=> &0 = (a - b) dot (&2 % x - (a + b))`,
607 ABBREV_TAC ` an a b x = ((a:real^A) - b) dot (&2 % x - (a + b))`;
608 REWRITE_TAC[dist; vector_norm];
609 REWRITE_TAC[MESON[DOT_POS_LE; SQRT_INJ]` sqrt ( x dot x) = sqrt (y dot y) <=> x dot x = y dot y `];
611 ONCE_REWRITE_TAC[arith `x = y <=> y - x = &0`];
612 TYPIFY `(x - b) dot (x - b) - (x - a) dot (x - a) = ((a - b) dot (&2 % x - (a + b)))` (C SUBGOAL_THEN SUBST1_TAC);
613 BY(VECTOR_ARITH_TAC);
614 BY(ASM_MESON_TAC[arith `x - &0 = x`])
617 let FUZBZGI_0 = prove_by_refinement(
618 `!V ul p1 p2 t1 t2. packing V /\ saturated V /\ leaf V ul /\
619 (voronoi_list V ul = convex hull {p1, p2}) /\
621 (circumcenter (set_of_list ul) = t1 % p1 + t2 % p2) /\
623 (!f. f facet_of voronoi_list V ul <=> f IN {{p1}, {p2}}) ==>
627 REPEAT WEAK_STRIP_TAC;
629 TYPIFY `barV V 2 ul` (C SUBGOAL_THEN ASSUME_TAC);
630 BY(ASM_MESON_TAC[leaf;IN]);
631 COMMENT "end insert";
632 COMMENT "borrowed_from _1 lemma";
633 INTRO_TAC NWVRFMF [`V`;`ul`;`p1`];
638 ABBREV_TAC `q = t1 % p1 + t2 % (p2:real^3)`;
639 INTRO_TAC Rogers.XYOFCGX [`V`;`set_of_list ul`;`q`];
641 TYPIFY `set_of_list ul SUBSET V` (C SUBGOAL_THEN ASSUME_TAC);
642 BY(ASM_MESON_TAC[Packing3.BARV_SUBSET;leaf;IN]);
646 FIRST_X_ASSUM_ST `leaf` MP_TAC;
647 REWRITE_TAC[leaf;Sphere.sqrt2;Pack_defs.HL];
649 MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT;
650 BY(ASM_MESON_TAC[leaf;IN]);
651 ONCE_REWRITE_TAC[DIST_SYM];
652 REWRITE_TAC[arith `x > y <=> y < x`];
653 REWRITE_TAC[Collect_geom.DIST_LT_HALF_PLANE];
654 DISCH_THEN (C INTRO_TAC [`HD ul`;`EL 3 vl`]);
655 REWRITE_TAC[IN_DIFF];
656 TYPIFY `HD ul IN set_of_list ul` (C SUBGOAL_THEN (ASSUME_TAC));
657 REWRITE_TAC[IN_SET_OF_LIST];
658 REWRITE_TAC[MEM_EXISTS_EL];
661 FIRST_X_ASSUM_ST `leaf` MP_TAC;
662 REWRITE_TAC[leaf;Sphere.BARV;IN];
664 TYPIFY `barV V 3 vl` (C SUBGOAL_THEN ASSUME_TAC);
665 BY(ASM_MESON_TAC[IN]);
666 TYPIFY `EL 3 vl IN V` (C SUBGOAL_THEN (ASSUME_TAC));
667 INTRO_TAC Packing3.BARV_SUBSET [`V`;`3`;`vl`];
669 REWRITE_TAC[ IN_SET_OF_LIST ; SUBSET; MEM_EXISTS_EL];
670 (FIRST_X_ASSUM_ST `barV V 3` MP_TAC);
671 REWRITE_TAC[Sphere.BARV;IN];
672 BY(MESON_TAC[arith `3 < 3 + 1`]);
675 TYPIFY `LENGTH vl = 4` (C SUBGOAL_THEN ASSUME_TAC);
676 BY(ASM_MESON_TAC[Sphere.BARV;arith `4 = 3 + 1`]);
677 INTRO_TAC Rogers.MHFTTZN1 [`V`;`vl`;`3`];
682 INTRO_TAC truncate_set_of_list [`vl`;`3`];
683 ASM_SIMP_TAC[arith `0 < 3 /\ 3 + 1 = 4 /\ 3 - 1 = 2`];
685 INTRO_TAC AFF_DIM_SUBSET [`set_of_list vl`;`set_of_list ul`];
687 REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC);
690 TYPIFY `aff_dim (set_of_list ul) = &2` (C SUBGOAL_THEN SUBST1_TAC);
691 MATCH_MP_TAC Rogers.MHFTTZN1;
692 BY(ASM_MESON_TAC[leaf;IN]);
695 COMMENT "back to 1' do <=.";
696 TYPIFY `voronoi_list V ul SUBSET voronoi_closed V (HD ul)` (C SUBGOAL_THEN ASSUME_TAC);
697 MATCH_MP_TAC Packing3.VORONOI_LIST_SUBSET_VORONOI_CLOSED;
698 FIRST_X_ASSUM_ST `leaf` MP_TAC;
699 REWRITE_TAC[IN;leaf;Sphere.BARV];
701 FIRST_X_ASSUM MP_TAC;
702 REWRITE_TAC[Pack2.VORONOI_CLOSED;SUBSET];
703 REWRITE_TAC[IN_ELIM_THM];
704 REWRITE_TAC[DIST_LE_HALF_PLANE];
705 DISCH_THEN (C INTRO_TAC [`p2`]);
707 (GMATCH_SIMP_TAC Marchal_cells_2_new.IN_SET_IMP_IN_CONVEX_HULL_SET);
710 GOAL_TERM (fun w -> (DISCH_THEN (MP_TAC o (ISPEC ( env w `EL 3 vl`)))));
713 COMMENT "back to 1a, do =.";
714 INTRO_TAC Marchal_cells_2_new.VORONOI_LIST_3_SINGLETON_EXPLICIT [`V`;`vl`];
717 INTRO_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST [`V`;`vl`;`3`];
718 ASM_REWRITE_TAC[IN_SING];
720 COMMENT "back to 1b";
721 INTRO_TAC Rogers.HL_PROPERTIES [`V`;`vl`;`3`];
723 GOAL_TERM (fun w -> (DISCH_THEN (MP_TAC o (ISPEC ( env w `EL 3 vl`)))));
724 REWRITE_TAC[IN_SET_OF_LIST];
725 REWRITE_TAC[MEM_EXISTS_EL];
728 BY(ASM_REWRITE_TAC[arith `3 < 4`]);
729 TYPIFY `dist (HD vl,circumcenter (set_of_list vl)) = dist (circumcenter (set_of_list vl), HD vl)` (C SUBGOAL_THEN SUBST1_TAC);
730 BY(MESON_TAC[DIST_SYM]);
731 REWRITE_TAC[DIST_EQ_HALF_PLANE];
733 TYPIFY `HD vl = HD ul` (C SUBGOAL_THEN SUBST1_TAC);
735 MATCH_MP_TAC (GSYM Packing3.HD_TRUNCATE_SIMPLEX);
736 BY(ASM_REWRITE_TAC[arith `2 + 1 <= 4`]);
737 ONCE_REWRITE_TAC[arith `&0 = x <=> &0 = -- x`];
738 TYPIFY ` --((EL 3 vl - HD ul) dot (&2 % circumcenter (set_of_list vl) - (EL 3 vl + HD ul))) = (( HD ul - EL 3 vl) dot (&2 % p1 - (HD ul + EL 3 vl)))` (C SUBGOAL_THEN SUBST1_TAC);
740 BY(VECTOR_ARITH_TAC);
742 FIRST_X_ASSUM_ST `&0 < x` MP_TAC;
744 ABBREV_TAC `(w:real^3) = HD ul - EL 3 vl`;
745 TYPIFY `w dot (&2 % (t1 % p1 + t2 % p2) - (HD ul + EL 3 vl)) = t1 * (w dot (&2 % p1 - (HD ul + EL 3 vl))) + t2 * ( w dot (&2 % p2 - (HD ul + EL 3 vl)))` (C SUBGOAL_THEN SUBST1_TAC);
746 FIRST_X_ASSUM_ST `x = &1` MP_TAC;
747 REWRITE_TAC[arith `t1 + t2 = &1 <=> t2 = &1 - t1`];
748 DISCH_THEN SUBST1_TAC;
749 BY(VECTOR_ARITH_TAC);
750 FIRST_X_ASSUM_ST `circumcenter` kill;
751 FIRST_X_ASSUM_ST `&0` (SUBST1_TAC o GSYM);
752 REWRITE_TAC[arith `t1 * &0 + x = x`];
753 ASM_CASES_TAC `((w:real^3) dot (&2 % p2 - (HD ul + EL 3 vl))) = &0`;
754 BY(ASM_MESON_TAC[arith `~(&0 < t * &0)`]);
755 REWRITE_TAC[REAL_MUL_POS_LT];
756 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
760 let FUZBZGI_1 = prove_by_refinement(
761 `!V ul. packing V /\ saturated V /\ leaf V ul ==>
763 (voronoi_list V ul = convex hull {p1, p2}) /\
765 (circumcenter (set_of_list ul) = t1 % p1 + t2 % p2) /\
767 (&0 < t1 /\ &0 < t2)`,
770 REPEAT WEAK_STRIP_TAC;
771 INTRO_TAC YBZFUPO [`V`;`ul`];
773 REPEAT WEAK_STRIP_TAC;
774 TYPIFY `p1` EXISTS_TAC;
775 TYPIFY `p2` EXISTS_TAC;
777 TYPIFY `circumcenter (set_of_list ul) IN affine hull voronoi_list V ul` (C SUBGOAL_THEN MP_TAC);
778 INTRO_TAC Rogers.MHFTTZN3 [`V`;`ul`;`2`];
781 BY(ASM_MESON_TAC[leaf;IN]);
783 ASM_REWRITE_TAC[AFFINE_HULL_CONVEX_HULL;AFFINE_HULL_2];
784 ABBREV_TAC `(q:real^3) = circumcenter (set_of_list ul)`;
785 REWRITE_TAC[IN_ELIM_THM];
786 REPEAT WEAK_STRIP_TAC;
787 TYPIFY `u` EXISTS_TAC;
788 TYPIFY `v` EXISTS_TAC;
791 MATCH_MP_TAC FUZBZGI_0;
792 GOAL_TERM (fun w -> (GEXISTL_TAC ( envl w [`V`;`ul`;`p2`;`p1`;`v`])));
798 BY(VECTOR_ARITH_TAC);
800 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
801 TYPIFY `{{p1},{p2}} = {{p2},{p1}}` (C SUBGOAL_THEN SUBST1_TAC);
804 MATCH_MP_TAC FUZBZGI_0;
805 GOAL_TERM (fun w -> (GEXISTL_TAC ( envl w [`V`;`ul`;`p1`;`p2`;`u`])));
810 let chi_msb = new_definition `chi_msb ul p =
811 ((EL 1 ul - EL 0 ul) cross (EL 2 ul - EL 0 ul)) dot (p - EL 0 ul)`;;
813 let chi_msb_swap_01 = prove_by_refinement(
814 `!a b c d. chi_msb [a;b;c] d = -- chi_msb [b;a;c] d`,
817 REWRITE_TAC[chi_msb;EL;HD;TL;arith `2 = SUC 1 /\ 1 = SUC 0`];
818 REPEAT WEAK_STRIP_TAC;
819 SUBGOAL_THEN `(d - a) = (d - b) + (b - (a:real^3))` SUBST1_TAC;
820 BY(VECTOR_ARITH_TAC);
821 SUBGOAL_THEN `(c - a) = (c - b) + (b - (a:real^3))` SUBST1_TAC;
822 BY(VECTOR_ARITH_TAC);
823 REWRITE_TAC[CROSS_RADD;DOT_RADD];
824 REWRITE_TAC[DOT_LADD];
825 REWRITE_TAC[CROSS_REFL];
826 REWRITE_TAC[DOT_LZERO];
827 REWRITE_TAC[arith `x + &0 = x`];
828 SUBGOAL_THEN `((b - a) cross (c - b)) dot (b - a) = &0` SUBST1_TAC;
829 BY(MESON_TAC[CROSS_TRIPLE;CROSS_REFL;DOT_LZERO]);
830 REWRITE_TAC[arith `x + &0 = x`];
831 REWRITE_TAC[GSYM DOT_LNEG];
834 REWRITE_TAC[GSYM CROSS_LNEG];
835 AP_THM_TAC THEN AP_TERM_TAC;
840 let chi_msb_swap_23 = prove_by_refinement(
841 `!a b c d. chi_msb [a;b;c] d = -- chi_msb[a;b;d] c`,
844 REWRITE_TAC[chi_msb;EL;HD;TL;arith `2 = SUC 1 /\ 1 = SUC 0`];
845 REPEAT WEAK_STRIP_TAC;
846 ONCE_REWRITE_TAC[CROSS_TRIPLE];
847 REWRITE_TAC[GSYM DOT_LNEG];
848 BY(REWRITE_TAC[GSYM CROSS_SKEW])
852 let chi_msb_swap_12 = prove_by_refinement(
853 `!a b c d. chi_msb [a;b;c] d = -- chi_msb [a;c;b] d`,
856 REWRITE_TAC[chi_msb;EL;HD;TL;arith `2 = SUC 1 /\ 1 = SUC 0`];
857 REPEAT WEAK_STRIP_TAC;
858 REWRITE_TAC[GSYM DOT_LNEG];
861 BY(REWRITE_TAC[GSYM CROSS_SKEW])
865 let chi_msb_additive_a = prove_by_refinement(
866 `!a b c d t1 t2 t3 t4. (t1 + t2 + t3 + t4 = &1) ==>
867 (chi_msb [t1 % a + t2 % b + t3 % c + t4 % d;b;c] d) = t1 * (chi_msb [a;b;c] d)`,
870 REPEAT WEAK_STRIP_TAC;
871 ONCE_REWRITE_TAC[chi_msb_swap_01];
872 REWRITE_TAC[chi_msb;EL;HD;TL;arith`2 = SUC 1 /\ 1 = SUC 0`];
873 TYPIFY `(t1 % a + t2 % b + t3 % c + t4 % d) - b = t1 % (a - b) + t3 % (c - b) + t4 % (d - b)` (C SUBGOAL_THEN SUBST1_TAC);
874 FIRST_X_ASSUM (SUBST1_TAC o (MATCH_MP (arith `t1 + t2 + t3 + t4 = &1 ==> t2 = &1 - t1 - t3 -t4`)));
875 BY(VECTOR_ARITH_TAC);
876 REWRITE_TAC[GSYM DOT_LNEG;GSYM CROSS_LNEG];
877 REWRITE_TAC[GSYM DOT_LMUL];
878 TYPIFY `--(t1 % (a - b) + t3 % (c - b) + t4 % (d - b)) = t1 % (--(a-b)) + (-- t3) % (c - b) + (-- t4) % (d - b)` (C SUBGOAL_THEN SUBST1_TAC);
879 BY(VECTOR_ARITH_TAC);
880 REWRITE_TAC[CROSS_LADD];
881 REWRITE_TAC[DOT_LADD];
882 REWRITE_TAC[CROSS_REFL;CROSS_LMUL];
883 TYPIFY ` --t4 % ((d - b) cross (c - b)) dot (d - b) = &0` (C SUBGOAL_THEN SUBST1_TAC);
884 REWRITE_TAC[ DOT_LMUL];
885 BY(MESON_TAC[CROSS_TRIPLE;CROSS_REFL;DOT_LZERO;arith `t * &0 = &0`]);
886 REWRITE_TAC[DOT_LMUL;DOT_LZERO];
891 let chi_msb_additive_d = prove_by_refinement(
892 `!a b c d t1 t2 t3 t4. (t1 + t2 + t3 + t4 = &1) ==>
893 chi_msb [a;b;c] (t1 % a + t2 % b + t3 % c + t4 % d) = t4 * chi_msb [a;b;c] d`,
896 REPEAT WEAK_STRIP_TAC;
897 ONCE_REWRITE_TAC[chi_msb_swap_23];
898 ONCE_REWRITE_TAC[chi_msb_swap_12];
899 REWRITE_TAC[arith `-- -- x = x`];
900 ONCE_REWRITE_TAC[chi_msb_swap_01];
901 SUBST1_TAC (varith `t1 % a + t2 % b + t3 % c + t4 % d = t4 % d + t1 % (a:real^3) + t2 % b + t3 % c`);
902 REWRITE_TAC[arith `-- x = t * -- y <=> x = t * y`];
903 MATCH_MP_TAC chi_msb_additive_a;
904 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
908 let CHI_MSB_ADDITIVE = prove_by_refinement(
909 `!ul t1 t2 p1 p2. (t1 + t2 = &1) ==>
910 chi_msb ul (t1 % p1 + t2 % p2) = t1 * chi_msb ul p1 + t2 * chi_msb ul p2`,
913 REPEAT WEAK_STRIP_TAC;
914 REWRITE_TAC[chi_msb];
915 FIRST_X_ASSUM (SUBST1_TAC o (MATCH_MP (arith `t1 + t2 = &1 ==> t1 = &1 - t2`)));
920 let CHI_MSB_CONVEX = prove_by_refinement(
921 `!ul. convex { p | &0 <= chi_msb ul p }`,
925 REWRITE_TAC[ CONVEX_ALT];
926 REWRITE_TAC[IN_ELIM_THM];
927 REPEAT WEAK_STRIP_TAC;
928 GMATCH_SIMP_TAC CHI_MSB_ADDITIVE;
931 MATCH_MP_TAC (arith `&0 <= x /\ &0 <= y ==> &0 <= x + y`);
932 GMATCH_SIMP_TAC REAL_LE_MUL;
933 GMATCH_SIMP_TAC REAL_LE_MUL;
935 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
939 let CHI_MSB_INCLUDES_CONVEX_HULL = prove_by_refinement(
940 `!S ul. S SUBSET {p | &0 <= chi_msb ul p } ==>
941 convex hull S SUBSET {p | &0 <= chi_msb ul p}`,
944 REPEAT WEAK_STRIP_TAC;
945 FIRST_X_ASSUM (MP_TAC o (MATCH_MP Marchal_cells.CONVEX_HULL_SUBSET));
946 BY(MESON_TAC[CHI_MSB_CONVEX;CONVEX_HULL_EQ])
951 let AFFINE_IMP_CHI_MSB_0 = prove_by_refinement(
952 `!ul (p:real^3). LENGTH ul = 3 /\ p IN affine hull (set_of_list ul) ==>
956 REPEAT WEAK_STRIP_TAC;
957 FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP set_of_list3));
958 FIRST_X_ASSUM_ST `IN` MP_TAC;
959 ASM_REWRITE_TAC[AFFINE_HULL_3];
960 REWRITE_TAC[IN_ELIM_THM];
961 REPEAT WEAK_STRIP_TAC;
962 ASM_REWRITE_TAC[chi_msb];
963 FIRST_X_ASSUM_ST `&1` (unlist REWRITE_TAC o (MATCH_MP (arith `u + v + w = &1 ==> u = &1 - v - w`)));
964 TYPIFY `((EL 1 ul - EL 0 ul) cross (EL 2 ul - EL 0 ul)) dot (((&1 - v - w) % EL 0 ul + v % EL 1 ul + w % EL 2 ul) - EL 0 ul) = v * (((EL 1 ul - EL 0 ul) cross (EL 2 ul - EL 0 ul)) dot (EL 1 ul - EL 0 ul)) + w * (((EL 1 ul - EL 0 ul) cross (EL 2 ul - EL 0 ul)) dot (EL 2 ul - EL 0 ul))` (C SUBGOAL_THEN SUBST1_TAC);
965 BY(VECTOR_ARITH_TAC);
966 MATCH_MP_TAC (arith `a = &0 /\ b = &0 ==> v *a + w * b = &0`);
968 ONCE_REWRITE_TAC[Trigonometry1.cross_triple];
969 ONCE_REWRITE_TAC[Trigonometry1.cross_triple];
970 BY(REWRITE_TAC[CROSS_REFL;DOT_LZERO]);
971 ONCE_REWRITE_TAC[Trigonometry1.cross_triple];
972 BY(REWRITE_TAC[CROSS_REFL;DOT_LZERO])
976 let CHI_MSB_IMP_COPLANAR = prove_by_refinement(
977 `!ul p. chi_msb ul p = &0 ==> coplanar { EL 0 ul, EL 1 ul, EL 2 ul, p}`,
980 BY(REWRITE_TAC[Local_lemmas.COPLANAR_IFF_CROSS_DOT;chi_msb])
984 let CHI_MSB_COPLANAR = prove_by_refinement(
985 `!a b c d. coplanar {a,b,c,d} <=> chi_msb [a;b;c] d = &0`,
988 REWRITE_TAC[Local_lemmas.COPLANAR_IFF_CROSS_DOT];
989 REWRITE_TAC[chi_msb];
990 BY(REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`])
995 let JDHAWAY_0 = prove_by_refinement(
996 `!V ul p1 p2 t1 t2. packing V /\ saturated V /\ leaf V ul /\
997 (voronoi_list V ul = convex hull {p1, p2}) /\
999 (circumcenter (set_of_list ul) = t1 % p1 + t2 % p2) /\
1001 (&0 < t1 /\ &0 < t2) ==>
1002 ~(chi_msb ul p1 = &0)`,
1005 REPEAT WEAK_STRIP_TAC;
1006 FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP CHI_MSB_IMP_COPLANAR));
1007 TYPIFY `p1 IN affine hull (set_of_list ul)` (C SUBGOAL_THEN ASSUME_TAC);
1008 MATCH_MP_TAC COPLANAR_INSERT;
1010 TYPIFY `p1 INSERT set_of_list ul = {EL 0 ul, EL 1 ul, EL 2 ul, p1}` ENOUGH_TO_SHOW_TAC;
1011 BY(DISCH_THEN (unlist ASM_REWRITE_TAC));
1012 GMATCH_SIMP_TAC set_of_list3;
1015 BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
1016 MATCH_MP_TAC Rogers.MHFTTZN1;
1017 BY(ASM_MESON_TAC[leaf;IN]);
1018 INTRO_TAC Rogers.MHFTTZN3 [`V`;`ul`;`2`];
1020 BY(ASM_MESON_TAC[leaf;IN]);
1021 REWRITE_TAC[EXTENSION;IN_INTER;IN_SING];
1022 DISCH_THEN (MP_TAC o (ISPEC `p1:real^3`));
1024 REWRITE_TAC[AFFINE_HULL_CONVEX_HULL];
1025 TYPIFY `p1 IN affine hull {p1, p2}` (C SUBGOAL_THEN (unlist REWRITE_TAC));
1026 INTRO_TAC Qzksykg.SET_SUBSET_AFFINE_HULL [`{p1,p2}`];
1028 FIRST_X_ASSUM_ST `&1` MP_TAC;
1029 REWRITE_TAC[arith `t1 + t2 = &1 <=> t1 = &1 - t2`];
1030 DISCH_THEN SUBST1_TAC;
1031 TYPIFY `p1 = (&1 - t2) % p1 + t2 % p2 <=> t2 % p1 = t2 % p2` (C SUBGOAL_THEN SUBST1_TAC);
1032 BY(VECTOR_ARITH_TAC);
1033 REWRITE_TAC[VECTOR_MUL_LCANCEL];
1034 BY(ASM_SIMP_TAC[arith `&0 < t ==> ~(t = &0)`])
1038 let JDHAWAY_1 = prove_by_refinement(
1040 packing V /\ saturated V /\ leaf V ul ==>
1041 chi_msb ul (circumcenter (set_of_list ul)) = &0`,
1044 REPEAT WEAK_STRIP_TAC;
1045 MATCH_MP_TAC AFFINE_IMP_CHI_MSB_0;
1047 BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2+1 = 3`]);
1048 MATCH_MP_TAC Rogers.BARV_CIRCUMCENTER_EXISTS;
1049 BY(ASM_MESON_TAC[leaf;IN])
1053 let JDWAWAY = prove_by_refinement(
1055 packing V /\ saturated V /\ leaf V ul /\
1056 (voronoi_list V ul = convex hull {p1, p2}) /\
1058 (circumcenter (set_of_list ul) = t1 % p1 + t2 % p2) /\
1060 (&0 < t1 /\ &0 < t2) ==>
1061 ~(chi_msb ul p1 = &0) /\ ~(chi_msb ul p2 = &0) /\
1062 (chi_msb ul p1 < &0 <=> &0 < chi_msb ul p2)`,
1065 REPEAT WEAK_STRIP_TAC;
1067 INTRO_TAC JDHAWAY_0 [`V`;`ul`;`p1`;`p2`;`t1`;`t2`];
1068 DISCH_THEN MATCH_MP_TAC;
1069 BY(ASM_MESON_TAC[]);
1072 INTRO_TAC JDHAWAY_0 [`V`;`ul`;`p2`;`p1`;`t2`;`t1`];
1073 DISCH_THEN MATCH_MP_TAC;
1079 BY(VECTOR_ARITH_TAC);
1080 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1082 INTRO_TAC JDHAWAY_1 [`V`;`ul`];
1083 ASM_SIMP_TAC[CHI_MSB_ADDITIVE];
1084 TYPIFY `&0 < chi_msb ul p2 <=> &0 < t2 * chi_msb ul p2` (C SUBGOAL_THEN SUBST1_TAC);
1085 REWRITE_TAC[REAL_MUL_POS_LT];
1086 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1087 DISCH_THEN (SUBST1_TAC o (MATCH_MP (arith `t1 * x + y = &0 ==> y = t1 * (--x)`)));
1088 REWRITE_TAC[REAL_MUL_POS_LT];
1089 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
1093 let cc_pe_exists = prove_by_refinement(
1094 `!V ul. ?p1. (?p2. packing V /\ saturated V /\ leaf V ul ==>
1095 (voronoi_list V ul = convex hull {p1, p2}) /\
1101 REPEAT WEAK_STRIP_TAC;
1102 REWRITE_TAC[MESON[] `(?p. x ==> R p) <=> (x ==> ?p. R p)`];
1103 REPEAT WEAK_STRIP_TAC;
1104 INTRO_TAC FUZBZGI_1 [`V`;`ul`];
1106 REPEAT WEAK_STRIP_TAC;
1107 ASM_CASES_TAC `&0 < chi_msb ul p1`;
1108 GEXISTL_TAC [`p1`;`p2`];
1109 BY(ASM_REWRITE_TAC[]);
1110 GEXISTL_TAC [`p2`;`p1`];
1115 INTRO_TAC (GSYM JDWAWAY) [`V`;`ul`;`p1`;`p2`;`t1`;`t2`];
1117 BY(ASM_REWRITE_TAC[]);
1118 REPEAT WEAK_STRIP_TAC;
1119 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
1123 let cc_pe = new_specification ["cc_pe1";"cc_pe2"]
1124 (REWRITE_RULE[SKOLEM_THM] cc_pe_exists);;
1126 let FACET_OF_SEGMENT = prove_by_refinement(
1127 `!a (b:real^A). ~(a = b) ==> {a} facet_of segment [a,b]`,
1130 REPEAT WEAK_STRIP_TAC;
1131 REWRITE_TAC[facet_of];
1132 REWRITE_TAC[AFF_DIM_SING];
1134 REWRITE_TAC[FACE_OF_SING];
1135 BY(REWRITE_TAC[EXTREME_POINT_OF_SEGMENT]);
1138 REWRITE_TAC[SEGMENT_CONVEX_HULL];
1139 REWRITE_TAC[AFF_DIM_CONVEX_HULL];
1140 REWRITE_TAC[AFF_DIM_2];
1146 let CC_PE_FACET_OF = prove_by_refinement(
1147 `!V ul. packing V /\ saturated V /\ leaf V ul ==>
1148 {cc_pe1 V ul} facet_of (voronoi_list V ul)`,
1151 REPEAT WEAK_STRIP_TAC;
1152 INTRO_TAC cc_pe [`V`;`ul`];
1154 REPEAT WEAK_STRIP_TAC;
1155 ASM_REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL ];
1156 MATCH_MP_TAC FACET_OF_SEGMENT;
1157 BY(ASM_REWRITE_TAC[])
1161 let cc_uh_exists = prove_by_refinement(
1162 `!V ul. ?vl. packing V /\ saturated V /\ leaf V ul ==>
1163 vl IN barV V 3 /\ truncate_simplex 2 vl = ul /\ omega_list V vl = (cc_pe1 V ul)`,
1166 REPEAT WEAK_STRIP_TAC;
1167 REWRITE_TAC[MESON[] `(?p. x ==> R p) <=> (x ==> ?p. R p)`];
1168 REPEAT WEAK_STRIP_TAC;
1169 INTRO_TAC NWVRFMF [`V`;`ul`;`cc_pe1 V ul`];
1170 BY(ASM_SIMP_TAC[CC_PE_FACET_OF])
1174 let cc_uh = new_specification ["cc_uh"]
1175 (REWRITE_RULE[SKOLEM_THM] cc_uh_exists);;
1177 let cc_ke = new_definition `cc_ke V ul =
1178 if hl (cc_uh V ul) < sqrt2 then 4 else 3`;;
1180 let cc_A0 = new_definition
1181 `cc_A0 (ul:(real^A) list) = aff_gt {EL 0 ul,EL 1 ul} {EL 2 ul}`;;
1183 let cc_cell = new_definition `cc_cell V ul = mcell (cc_ke V ul) V (cc_uh V ul)`;;
1185 let CC_CELL4 = prove_by_refinement(
1186 `!V ul. packing V /\ saturated V /\ leaf V ul /\ cc_ke V ul = 4 ==>
1187 cc_cell V ul = convex hull set_of_list (cc_uh V ul)`,
1190 REPEAT WEAK_STRIP_TAC;
1191 ASM_REWRITE_TAC[cc_cell;Pack_defs.mcell;arith `~(4=0) /\ ~(4=1) /\ ~(4=2) /\ ~(4=3)`];
1192 REWRITE_TAC[Pack_defs.mcell4];
1193 FIRST_X_ASSUM MP_TAC;
1195 REWRITE_TAC[Sphere.sqrt2];
1198 BY(REWRITE_TAC[arith `~(3=4)`])
1202 let CC_CELL3 = prove_by_refinement(
1203 `!V ul. packing V /\ saturated V /\ leaf V ul /\ cc_ke V ul = 3 ==>
1204 cc_cell V ul = convex hull
1205 (set_of_list (ul) UNION
1206 {mxi V (cc_uh V ul)})`,
1209 REPEAT WEAK_STRIP_TAC;
1210 ASM_REWRITE_TAC[cc_cell;Pack_defs.mcell;arith `~(3=0) /\ ~(3=1) /\ ~(3=2)`];
1211 REWRITE_TAC[Pack_defs.mcell3];
1212 FIRST_X_ASSUM MP_TAC;
1213 REWRITE_TAC[cc_ke;GSYM Sphere.sqrt2];
1215 BY(REWRITE_TAC[arith `~(4=3)`]);
1216 REWRITE_TAC[arith `3=3`];
1217 ASM_SIMP_TAC[arith `~(x < y) ==> (y <= x)`];
1218 INTRO_TAC cc_uh [`V`;`ul`];
1220 REPEAT WEAK_STRIP_TAC;
1222 FIRST_X_ASSUM_ST `leaf` MP_TAC;
1223 REWRITE_TAC[leaf;IN;Sphere.BARV];
1224 REPEAT WEAK_STRIP_TAC;
1225 BY(ASM_REWRITE_TAC[])
1229 let CC_KE_34 = prove_by_refinement(
1230 `!V ul. cc_ke V ul = 3 \/ cc_ke V ul = 4`,
1233 BY(MESON_TAC[cc_ke])
1237 let CC_CELL34 = prove_by_refinement(
1238 `!V ul pp. packing V /\ saturated V /\ leaf V ul /\
1239 ((if (cc_ke V ul = 3) then mxi V (cc_uh V ul) else (EL 3 (cc_uh V ul))) = pp) ==>
1240 cc_cell V ul = convex hull { EL 0 ul, EL 1 ul, EL 2 ul, pp}`,
1243 REPEAT WEAK_STRIP_TAC;
1244 FIRST_X_ASSUM MP_TAC;
1246 ASM_SIMP_TAC[CC_CELL3];
1249 GMATCH_SIMP_TAC set_of_list3;
1251 BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
1253 SUBGOAL_THEN `cc_ke V ul = 4` ASSUME_TAC;
1254 BY(ASM_MESON_TAC[CC_KE_34]);
1255 ASM_SIMP_TAC[CC_CELL4];
1258 GMATCH_SIMP_TAC set_of_list4;
1261 INTRO_TAC cc_uh [`V`;`ul`];
1263 BY(MESON_TAC[IN;Sphere.BARV;arith `3 + 1 = 4`]);
1264 INTRO_TAC cc_uh [`V`;`ul`];
1266 REPEAT WEAK_STRIP_TAC;
1267 INTRO_TAC Packing3.EL_TRUNCATE_SIMPLEX [`cc_uh V ul`;`2`];
1269 TYPIFY `2 + 1 <= LENGTH (cc_uh V ul)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
1270 FIRST_X_ASSUM_ST `barV` MP_TAC;
1271 REWRITE_TAC[Sphere.BARV;IN];
1272 BY(MESON_TAC[arith `2 + 1 <= 3 + 1`]);
1273 BY(MESON_TAC[arith `0 <= 2 /\ 1 <= 2 /\ 2 <= 2`])
1277 let U2_IN_CC_CELL = prove_by_refinement(
1278 `!V ul. packing V /\ saturated V /\ leaf V ul ==>
1279 (EL 2 ul IN cc_cell V ul)`,
1282 REPEAT WEAK_STRIP_TAC;
1283 ABBREV_TAC `p = (if (cc_ke V ul = 3) then mxi V (cc_uh V ul) else (EL 3 (cc_uh V ul)))`;
1284 INTRO_TAC CC_CELL34 [`V`;`ul`;`p`];
1286 DISCH_THEN SUBST1_TAC;
1287 MATCH_MP_TAC Marchal_cells_2_new.IN_SET_IMP_IN_CONVEX_HULL_SET;
1292 let U2_IN_AFF_GT = prove_by_refinement(
1293 `!V ul. packing V /\ saturated V /\ leaf V ul ==>
1294 EL 2 ul IN aff_gt {EL 0 ul, EL 1 ul} {EL 2 ul}`,
1297 REPEAT WEAK_STRIP_TAC;
1298 MATCH_MP_TAC Local_lemmas.DISJOINT_IMP_Z_IN_AFF_GT;
1299 REWRITE_TAC[DISJOINT;EXTENSION;NOT_IN_EMPTY;IN_INTER;IN_INSERT];
1302 INTRO_TAC GBEWYFX [`V`;`ul`];
1304 GMATCH_SIMP_TAC set_of_list3;
1306 BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
1307 FIRST_X_ASSUM MP_TAC;
1308 REPEAT WEAK_STRIP_TAC;
1309 TYPIFY `{EL 0 ul, EL 1 ul, EL 2 ul} = { EL 0 ul, EL 1 ul}` (C SUBGOAL_THEN SUBST1_TAC);
1310 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
1311 BY(REWRITE_TAC[COLLINEAR_2]);
1312 TYPIFY `{EL 0 ul, EL 1 ul, EL 2 ul} = { EL 0 ul, EL 1 ul}` (C SUBGOAL_THEN SUBST1_TAC);
1313 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
1314 BY(REWRITE_TAC[COLLINEAR_2])
1318 let EL_CC_UH = prove_by_refinement(
1319 `!V ul. packing V /\ saturated V /\ leaf V ul ==>
1320 EL 0 (cc_uh V ul) = EL 0 ul /\
1321 EL 1 (cc_uh V ul) = EL 1 ul /\
1322 EL 2 (cc_uh V ul) = EL 2 ul`,
1325 REPEAT WEAK_STRIP_TAC;
1326 INTRO_TAC cc_uh [`V`;`ul`];
1328 REPEAT WEAK_STRIP_TAC;
1329 INTRO_TAC Packing3.EL_TRUNCATE_SIMPLEX [`cc_uh V ul`;`2`];
1330 TYPIFY `2 + 1 <= LENGTH (cc_uh V ul)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
1331 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `2 + 1 <= 3 + 1`]);
1332 BY(ASM_MESON_TAC[arith `0 <= 2 /\ 1 <= 2 /\ 2 <= 2`])
1336 let NUNRRDS_0 = prove_by_refinement(
1337 `!V ul. packing V /\ saturated V /\ leaf V ul ==>
1338 ~(cc_A0 ul INTER cc_cell V ul = {})`,
1341 REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER];
1342 REPEAT WEAK_STRIP_TAC;
1343 GOAL_TERM (fun w -> (FIRST_X_ASSUM (MP_TAC o (ISPEC ( env w `EL 2 ul`)))));
1347 MATCH_MP_TAC U2_IN_CC_CELL;
1348 BY(ASM_REWRITE_TAC[]);
1349 COMMENT "second side";
1350 MATCH_MP_TAC U2_IN_AFF_GT;
1355 let AFF_GE_MONO_TRANS = prove_by_refinement(
1356 `!X Y (S:real^A->bool). S SUBSET X ==> aff_ge (X DIFF S) (Y UNION S) SUBSET aff_ge X Y`,
1359 BY(MESON_TAC[Local_lemmas.AFF_GE_MONO_TRANS])
1363 let NUNRRDS_1 = prove_by_refinement(
1364 `!V ul pp. packing V /\ saturated V /\ leaf V ul /\
1365 (if (cc_ke V ul = 3) then mxi V (cc_uh V ul) else (EL 3 (cc_uh V ul))) = pp
1367 cc_cell V ul SUBSET aff_ge {EL 0 ul, EL 1 ul, EL 2 ul} {pp}`,
1370 REPEAT WEAK_STRIP_TAC;
1371 INTRO_TAC CC_CELL34 [`V`;`ul`;`pp`];
1373 DISCH_THEN SUBST1_TAC;
1374 REWRITE_TAC[CONVEX_HULL_AFF_GE];
1375 INTRO_TAC (AFF_GE_MONO_TRANS) [`{EL 0 ul, EL 1 ul, EL 2 ul}`;`{pp}`;`{EL 0 ul, EL 1 ul, EL 2 ul}`];
1378 TYPIFY `{EL 0 ul, EL 1 ul, EL 2 ul} DIFF {EL 0 ul, EL 1 ul, EL 2 ul} = {}` (C SUBGOAL_THEN SUBST1_TAC);
1380 TYPIFY `{pp} UNION {EL 0 ul, EL 1 ul, EL 2 ul} = {EL 0 ul, EL 1 ul, EL 2 ul, pp}` (C SUBGOAL_THEN SUBST1_TAC);
1386 let CELL4_NONDEG = prove_by_refinement(
1387 `!V ul. packing V /\ saturated V /\ leaf V ul /\ (cc_ke V ul = 4) ==>
1388 ~(EL 3 (cc_uh V ul) IN affine hull (set_of_list ul))`,
1391 REPEAT WEAK_STRIP_TAC;
1392 INTRO_TAC Rogers.MHFTTZN1 [`V`;`ul`;`2`];
1393 INTRO_TAC Rogers.MHFTTZN1 [`V`;`cc_uh V ul`;`3`];
1394 INTRO_TAC cc_uh [`V`;`ul`];
1398 TYPIFY `barV V 2 ul` (C SUBGOAL_THEN (unlist REWRITE_TAC));
1399 BY(ASM_MESON_TAC[leaf;IN]);
1401 TYPIFY `set_of_list (cc_uh V ul) = (EL 3 (cc_uh V ul)) INSERT (set_of_list ul)` (C SUBGOAL_THEN ASSUME_TAC);
1402 GMATCH_SIMP_TAC set_of_list4;
1403 GMATCH_SIMP_TAC set_of_list3;
1405 BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2+1=3`]);
1407 BY(ASM_MESON_TAC[Sphere.BARV;arith `3 + 1 = 4`]);
1408 ASM_SIMP_TAC[EL_CC_UH];
1411 FIRST_X_ASSUM_ST `int_of_num 3` MP_TAC;
1413 ASM_REWRITE_TAC[AFF_DIM_INSERT];
1418 let K4_CHI_MSB_EQVL = prove_by_refinement(
1419 `!V ul. packing V /\ saturated V /\ leaf V ul /\
1422 re_eqvl (chi_msb ul (EL 3 (cc_uh V ul))) (chi_msb ul (cc_pe1 V ul))`,
1425 REPEAT WEAK_STRIP_TAC;
1426 INTRO_TAC cc_uh [`V`;`ul`];
1428 REPEAT WEAK_STRIP_TAC;
1429 INTRO_TAC Rogers.XNHPWAB2 [`V`;`cc_uh V ul`;`3`];
1432 BY(ASM_MESON_TAC[cc_ke;arith `~(3 = 4)`;Sphere.sqrt2]);
1433 GMATCH_SIMP_TAC set_of_list4;
1435 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 =4`]);
1436 REWRITE_TAC[Marchal_cells_2_new.CONVEX_HULL_4;IN_ELIM_THM];
1437 REPEAT WEAK_STRIP_TAC;
1439 TYPIFY `chi_msb ul = chi_msb [EL 0 ul;EL 1 ul;EL 2 ul]` (C SUBGOAL_THEN SUBST1_TAC);
1440 ONCE_REWRITE_TAC[FUN_EQ_THM];
1441 BY(REWRITE_TAC[chi_msb;HD;TL;EL;arith `1 = SUC 0 /\ 2 = SUC 1`]);
1442 INTRO_TAC EL_CC_UH [`V`;`ul`];
1444 REPEAT WEAK_STRIP_TAC;
1446 GMATCH_SIMP_TAC chi_msb_additive_d;
1448 GMATCH_SIMP_TAC RE_EQVL_SCALE2;
1449 REWRITE_TAC[RE_EQVL_REFL];
1450 ASM_SIMP_TAC[arith `&0 <= z ==> (&0 < z <=> ~(z = &0))`];
1452 TYPIFY `chi_msb ul (cc_pe1 V ul) = &0` (C SUBGOAL_THEN ASSUME_TAC);
1454 TYPIFY `chi_msb ul = chi_msb [EL 0 ul;EL 1 ul;EL 2 ul]` (C SUBGOAL_THEN SUBST1_TAC);
1455 ONCE_REWRITE_TAC[FUN_EQ_THM];
1456 BY(REWRITE_TAC[chi_msb;HD;TL;EL;arith `1 = SUC 0 /\ 2 = SUC 1`]);
1457 GMATCH_SIMP_TAC chi_msb_additive_d;
1458 ASM_REWRITE_TAC[arith `&0 * t = &0`];
1459 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1460 INTRO_TAC cc_pe [`V`;`ul`];
1466 let K4_CHI_MSB_POS = prove_by_refinement(
1467 `!V ul. packing V /\ saturated V /\ leaf V ul /\
1470 ( &0 < chi_msb ul (EL 3 (cc_uh V ul )))`,
1473 REPEAT WEAK_STRIP_TAC;
1474 INTRO_TAC K4_CHI_MSB_EQVL [`V`;`ul`];
1476 REWRITE_TAC[Trigonometry2.re_eqvl];
1477 REPEAT WEAK_STRIP_TAC;
1479 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
1481 INTRO_TAC cc_pe [`V`;`ul`];
1487 let MXI_BETWEEN = prove_by_refinement(
1488 `!V ul vl. packing V /\ saturated V /\ leaf V ul /\ cc_ke V ul = 3 /\
1490 between (mxi V vl) (omega_list_n V vl 2, omega_list_n V vl 3) /\
1491 dist(EL 0 ul, mxi V vl) = sqrt2`,
1494 REPEAT WEAK_STRIP_TAC;
1495 INTRO_TAC Marchal_cells_2_new.MXI_EXPLICIT [`V`;`cc_uh V ul`;`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`EL 3 (cc_uh V ul)`];
1496 INTRO_TAC EL_CC_UH [`V`;`ul`];
1497 INTRO_TAC cc_uh [`V`;`ul`];
1499 REPEAT WEAK_STRIP_TAC;
1500 FIRST_X_ASSUM MP_TAC;
1501 ASM_REWRITE_TAC[GSYM Sphere.sqrt2];
1504 BY(ASM_MESON_TAC[IN]);
1506 FIRST_X_ASSUM_ST `barV` MP_TAC;
1507 REWRITE_TAC[LENGTH4;IN;Sphere.BARV;arith `3 + 1 =4`];
1508 REPEAT WEAK_STRIP_TAC;
1509 BY(ASM_MESON_TAC[ LENGTH4]);
1511 BY(ASM_MESON_TAC[leaf]);
1512 BY(ASM_MESON_TAC[cc_ke;arith `~(4 = 3)`;arith `sqrt2 <= x <=> ~(x < sqrt2)`]);
1513 REPEAT WEAK_STRIP_TAC;
1518 let affine_invert = prove_by_refinement(
1519 `!u p (q:real^A) s. ~(u= &0) /\ affine s /\ (&1 - u) % p + u % q IN s /\ p IN s ==>
1523 REWRITE_TAC[affine];
1524 REPEAT WEAK_STRIP_TAC;
1525 FIRST_X_ASSUM (C INTRO_TAC [`((&1 - u) % p + u % q)`;`p`;`inv u`;`&1 - inv u`]);
1526 ASM_REWRITE_TAC[arith `x + &1 - x = &1`];
1527 TYPIFY `inv u % ((&1 - u) % p + u % q) + (&1 - inv u) % p = q` (C SUBGOAL_THEN SUBST1_TAC);
1528 TYPIFY `inv u % ((&1 - u) % p + u % q) + (&1 - inv u) % p = (inv u * (&1 - u) + (&1 - inv u)) % p + (inv u * u) % q` (C SUBGOAL_THEN SUBST1_TAC);
1529 BY(VECTOR_ARITH_TAC);
1530 TYPIFY `(inv u * (&1 - u) + &1 - inv u) = &0` (C SUBGOAL_THEN SUBST1_TAC);
1531 Calc_derivative.CALC_ID_TAC;
1532 BY(ASM_REWRITE_TAC[]);
1533 TYPIFY `(inv u * u) = &1` (C SUBGOAL_THEN SUBST1_TAC);
1534 Calc_derivative.CALC_ID_TAC;
1535 BY(ASM_REWRITE_TAC[]);
1536 BY(VECTOR_ARITH_TAC);
1541 let CELL3_NONDEG = prove_by_refinement(
1542 `!V ul. packing V /\ saturated V /\ leaf V ul /\ cc_ke V ul = 3 ==>
1543 ~(mxi V (cc_uh V ul) IN affine hull (set_of_list ul)) /\
1544 &0 < chi_msb ul (mxi V (cc_uh V ul))`,
1547 REPEAT WEAK_STRIP_TAC;
1548 ABBREV_TAC `vl = cc_uh V ul`;
1549 INTRO_TAC MXI_BETWEEN [`V`;`ul`;`vl`];
1550 ASM_REWRITE_TAC[BETWEEN_IN_SEGMENT;closed_segment;IN_ELIM_THM];
1551 REPEAT WEAK_STRIP_TAC;
1552 INTRO_TAC cc_pe [`V`;`ul`];
1553 INTRO_TAC cc_uh [`V`;`ul`];
1555 REPEAT WEAK_STRIP_TAC;
1556 TYPIFY `LENGTH vl = 4` (C SUBGOAL_THEN ASSUME_TAC);
1557 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`]);
1558 INTRO_TAC Sphere.OMEGA_LIST [`V`;`vl`];
1559 ASM_REWRITE_TAC[arith `4 - 1 = 3`];
1561 INTRO_TAC EL_CC_UH [`V`;`ul`];
1563 REPEAT WEAK_STRIP_TAC;
1564 TYPIFY `omega_list_n V vl 2 = circumcenter (set_of_list ul)` (C SUBGOAL_THEN ASSUME_TAC);
1565 INTRO_TAC (GSYM Rogers.XNHPWAB1) [`V`;`ul`;`2`];
1566 ASM_REWRITE_TAC[GSYM Sphere.sqrt2];
1568 BY(ASM_MESON_TAC[leaf;IN]);
1569 DISCH_THEN SUBST1_TAC;
1570 FIRST_X_ASSUM_ST `leaf` MP_TAC;
1571 REWRITE_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 =3`];
1572 REPEAT WEAK_STRIP_TAC;
1573 ASM_REWRITE_TAC[Pack_concl.JJGTQMN;arith `3 - 1 = 2`];
1574 INTRO_TAC Packing3.TRUNCATE_SIMPLEX_REFL [`2`;`ul`];
1575 ASM_REWRITE_TAC[arith `3 = 2 + 1`];
1576 REPEAT (GMATCH_SIMP_TAC (GSYM Packing3.OMEGA_LIST_LEMMA));
1577 ASM_REWRITE_TAC[arith `2 + 1 <= 3 /\ 2 + 1 <= 4`];
1578 BY(ASM_MESON_TAC[]);
1579 GMATCH_SIMP_TAC CHI_MSB_ADDITIVE;
1580 ASM_REWRITE_TAC[arith `&1 - u + u = &1`];
1581 GMATCH_SIMP_TAC JDHAWAY_1;
1583 BY(ASM_MESON_TAC[]);
1584 REWRITE_TAC[arith `x * &0 + v = v`];
1585 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
1586 ASM_SIMP_TAC[arith `&0 <= u ==> (&0 < u <=> ~(u = &0))`];
1587 SUBGOAL_THEN ` &0 < chi_msb ul (omega_list_n V vl 3)` (unlist REWRITE_TAC);
1588 BY(ASM_MESON_TAC[]);
1590 ASM_CASES_TAC `u = &0`;
1592 FIRST_X_ASSUM_ST `&1 - u` MP_TAC;
1594 REWRITE_TAC[VECTOR_MUL_LID;arith `&1 - &0 = &1 /\ x + &0 = x`;VECTOR_MUL_LZERO;VECTOR_ADD_RID];
1596 FIRST_X_ASSUM_ST `leaf` MP_TAC;
1597 REWRITE_TAC[leaf;IN];
1598 REPEAT WEAK_STRIP_TAC;
1599 FIRST_X_ASSUM_ST `hl` MP_TAC;
1601 GMATCH_SIMP_TAC Rogers.HL_EQ_DIST0;
1603 BY(ASM_MESON_TAC[]);
1604 BY(ASM_MESON_TAC[DIST_SYM;EL;arith `~(sqrt2 < sqrt2)`]);
1606 SUBGOAL_THEN `&0 < u` ASSUME_TAC;
1607 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1609 TYPIFY `cc_pe1 V ul IN affine hull set_of_list ul` (C SUBGOAL_THEN MP_TAC);
1610 MATCH_MP_TAC affine_invert;
1611 GEXISTL_TAC [`u`;`circumcenter (set_of_list ul)`];
1612 ASM_REWRITE_TAC[AFFINE_AFFINE_HULL];
1613 MATCH_MP_TAC Rogers.BARV_CIRCUMCENTER_EXISTS;
1614 BY(ASM_MESON_TAC[leaf;IN]);
1616 FIRST_X_ASSUM_ST `chi_msb` MP_TAC;
1618 MATCH_MP_TAC (arith `(x = &0) ==> ~(&0 < x)`);
1619 MATCH_MP_TAC AFFINE_IMP_CHI_MSB_0;
1621 BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`])
1625 let CELL_NN = prove_by_refinement(
1626 `!V ul p. packing V /\ saturated V /\ leaf V ul /\
1627 p IN cc_cell V ul ==> &0 <= chi_msb ul p`,
1630 REPEAT WEAK_STRIP_TAC;
1631 TYPIFY `LENGTH ul = 3` (C SUBGOAL_THEN ASSUME_TAC);
1632 BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
1633 INTRO_TAC CHI_MSB_CONVEX [`ul`];
1634 FIRST_X_ASSUM_ST `cc_cell` MP_TAC;
1635 GMATCH_SIMP_TAC CC_CELL34;
1636 ABBREV_TAC `pp = (if cc_ke V ul = 3 then mxi V (cc_uh V ul) else EL 3 (cc_uh V ul))`;
1639 INTRO_TAC Marchal_cells.CONVEX_HULL_SUBSET [`{EL 0 ul, EL 1 ul, EL 2 ul, pp}`;`{p | &0 <= chi_msb ul p}`];
1640 REPEAT WEAK_STRIP_TAC;
1641 FIRST_X_ASSUM_ST `SUBSET` MP_TAC;
1643 REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;IN_ELIM_THM];
1645 SUBGOAL_THEN `&0 <= chi_msb ul pp` ASSUME_TAC;
1646 MATCH_MP_TAC (arith `&0 < x ==> &0 <= x`);
1649 INTRO_TAC CELL3_NONDEG [`V`;`ul`];
1650 BY(ASM_MESON_TAC[]);
1651 SUBGOAL_THEN `cc_ke V ul = 4` ASSUME_TAC;
1652 BY(ASM_MESON_TAC[CC_KE_34]);
1653 MATCH_MP_TAC K4_CHI_MSB_POS;
1654 BY(ASM_REWRITE_TAC[]);
1655 SUBGOAL_THEN `x IN set_of_list ul ==> &0 <= chi_msb ul x` ASSUME_TAC;
1657 MATCH_MP_TAC (arith ` x = &0 ==> &0 <= x`);
1658 MATCH_MP_TAC AFFINE_IMP_CHI_MSB_0;
1659 BY(ASM_MESON_TAC[SUBSET;Qzksykg.SET_SUBSET_AFFINE_HULL]);
1660 FIRST_X_ASSUM MP_TAC;
1661 GMATCH_SIMP_TAC set_of_list3;
1662 ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
1663 BY(ASM_MESON_TAC[]);
1664 TYPIFY `convex hull {p | &0 <= chi_msb ul p} = {p | &0 <= chi_msb ul p}` (C SUBGOAL_THEN SUBST1_TAC);
1665 BY(ASM_MESON_TAC[CONVEX_HULL_EQ]);
1666 REWRITE_TAC[SUBSET;IN_ELIM_THM];
1667 DISCH_THEN MATCH_MP_TAC;
1668 BY(ASM_REWRITE_TAC[])
1672 let delta_delta_x = prove_by_refinement(
1673 `!x1 x2 x3 x4 x5 x6. delta x1 x2 x3 x6 x5 x4 = delta_x x1 x2 x3 x4 x5 x6 `,
1676 REWRITE_TAC[Collect_geom.delta;Sphere.delta_x];
1681 let ZWVCBMN = prove_by_refinement(
1682 `!a b c d. ~coplanar {a,b,c,d} ==> &0 < vol (convex hull {a,b,c,d})`,
1685 REWRITE_TAC[VOLUME_OF_CLOSED_TETRAHEDRON];
1686 REPEAT WEAK_STRIP_TAC;
1687 GMATCH_SIMP_TAC REAL_LT_DIV;
1688 REWRITE_TAC[ REAL_OF_NUM_LT];
1689 GMATCH_SIMP_TAC REAL_LT_RSQRT;
1690 REWRITE_TAC[GSYM delta_delta_x];
1691 INTRO_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] (GSYM Collect_geom.POLFLZY)) [`a`;`b`;`c`;`d`];
1692 INTRO_TAC coplanar_eq_coplanar_alt [`{a,b,c,d}`];
1693 REWRITE_TAC[DIMINDEX_3];
1696 DISCH_THEN (SUBST1_TAC o GSYM);
1699 ASM_SIMP_TAC[arith `0 < 12`;arith `~(x = &0) ==> (&0 pow 2 < x <=> &0 <= x)`];
1700 BY(MESON_TAC[Collect_geom2.DELTA_POS_4POINTS])
1704 let MCELL4_NONPLANAR = prove_by_refinement(
1705 `!V vl. packing V /\ saturated V /\ barV V 3 vl /\ hl vl < sqrt2 ==>
1706 ~coplanar (mcell4 V vl)`,
1709 REPEAT WEAK_STRIP_TAC;
1710 INTRO_TAC Rogers.MHFTTZN1 [`V`;`vl`;`3`];
1713 INTRO_TAC Pack_defs.mcell4 [`V`;`vl`];
1714 ASM_REWRITE_TAC[GSYM Sphere.sqrt2];
1716 FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP COPLANAR_IMP_AFF_DIM));
1717 INTRO_TAC AFF_DIM_SUBSET [`set_of_list vl`;`convex hull set_of_list vl`];
1719 BY(MESON_TAC[HULL_SUBSET]);
1720 REPEAT (FIRST_X_ASSUM_ST `aff_dim` MP_TAC);
1726 let MXI_IN_VORONOI_LIST = prove_by_refinement(
1727 `!V vl. packing V /\ saturated V /\ barV V 3 vl /\ sqrt2 <= hl vl /\
1728 hl (truncate_simplex 2 vl) < sqrt2 ==>
1729 mxi V vl IN voronoi_list V (truncate_simplex 2 vl) /\
1730 dist(EL 0 vl,mxi V vl) = sqrt2`,
1733 REPEAT WEAK_STRIP_TAC;
1734 INTRO_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN [`V`;`vl`;`3`;`2`;`2`];
1735 INTRO_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN [`V`;`vl`;`3`;`2`;`3`];
1743 INTRO_TAC Packing3.CONVEX_VORONOI_LIST [`V`;`truncate_simplex 2 vl`];
1745 INTRO_TAC Marchal_cells_2_new.MXI_EXPLICIT [`V`;`vl`;`EL 0 vl`;`EL 1 vl`;`EL 2 vl`;`EL 3 vl`];
1746 REWRITE_TAC[BETWEEN_IN_CONVEX_HULL];
1748 ASM_REWRITE_TAC[GSYM Sphere.sqrt2];
1749 GMATCH_SIMP_TAC LENGTH4;
1750 REWRITE_TAC[EL;HD;TL;arith `3 = SUC 2 /\ 2 = SUC 1 /\ 1 = SUC 0`];
1751 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3+1=4`]);
1752 REPEAT WEAK_STRIP_TAC;
1753 ASM_REWRITE_TAC[Sphere.sqrt2];
1754 TYPED_ABBREV_TAC `(a:real^3->bool) = voronoi_list V (truncate_simplex 2 vl)` ;
1755 TYPIFY `{omega_list_n V vl 2,omega_list_n V vl 3} SUBSET a` (C SUBGOAL_THEN ASSUME_TAC);
1756 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
1757 FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP Marchal_cells.CONVEX_HULL_SUBSET));
1758 BY(ASM_MESON_TAC[CONVEX_HULL_EQ;Packing3.IN_TRANS])
1762 let VORONOI_LIST_EQ = prove_by_refinement(
1763 `!V ul p k. p IN voronoi_list V ul /\ barV V k ul==>
1764 (?r. !q. q IN set_of_list ul ==> dist(p,q) = r)`,
1767 REWRITE_TAC[Sphere.VORONOI_LIST;Sphere.VORONOI_SET;Sphere.voronoi_closed;IN_INTERS;IN_ELIM_THM;LEFT_IMP_EXISTS_THM];
1769 ONCE_REWRITE_TAC[MESON [] `(!p q. R p q) <=> (!q p. R p q)`];
1770 REWRITE_TAC[TAUT `(a /\ b ==> c) <=> (a ==> b ==> c)`];
1771 REWRITE_TAC[MESON[] `!a. (!p. a ==> b p) <=> (a ==> (!p. b p))`];
1772 REWRITE_TAC[MESON[] `!a p. (!t. (t = a) ==> (p IN t)) <=> (p IN a)`];
1773 REWRITE_TAC[IN_ELIM_THM];
1774 TYPIFY `set_of_list ul = {}` ASM_CASES_TAC;
1775 BY(ASM_REWRITE_TAC[NOT_IN_EMPTY]);
1776 FIRST_X_ASSUM (MP_TAC o (REWRITE_RULE[Misc_defs_and_lemmas.EMPTY_EXISTS]));
1777 REPEAT WEAK_STRIP_TAC;
1778 GOAL_TERM (fun w -> (EXISTS_TAC ( env w `dist(p,u)`)));
1779 REPEAT WEAK_STRIP_TAC;
1780 BY(ASM_MESON_TAC[Packing3.BARV_SUBSET;arith `x <= y /\ y <= x ==> (x = y)`;IN;SUBSET])
1784 let NOT_COL_IMP_RADV = prove_by_refinement(
1785 `!va vb (vc:real^3). ~collinear {va, vb, vc}
1786 ==> (!w. w IN {va, vb, vc}
1787 ==> radV {va, vb, vc} = dist (circumcenter {va, vb, vc},w))`,
1790 MESON_TAC[IN;Collect_geom.NOT_COL_IMP_RADV_PROPERTIY]
1794 let MCELL3_NONPLANAR = prove_by_refinement(
1795 `!V vl. packing V /\ saturated V /\ barV V 3 vl /\ sqrt2 <= hl vl /\
1796 hl (truncate_simplex 2 vl) < sqrt2 ==>
1797 ~coplanar (mcell3 V vl)`,
1800 REPEAT WEAK_STRIP_TAC;
1801 TYPIFY `LENGTH vl = 4` (C SUBGOAL_THEN ASSUME_TAC);
1802 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3+1 = 4`]);
1803 INTRO_TAC Packing3.LENGTH_TRUNCATE_SIMPLEX [`2`;`vl`];
1805 BY(ASM_MESON_TAC[arith `2 + 1 <= 4`]);
1806 REWRITE_TAC[arith `2 + 1 = 3`];
1808 TYPIFY `coplanar (set_of_list (truncate_simplex 2 vl))` (C SUBGOAL_THEN ASSUME_TAC);
1809 GMATCH_SIMP_TAC set_of_list3;
1810 BY(ASM_REWRITE_TAC[COPLANAR_3]);
1811 INTRO_TAC Pack_defs.mcell3 [`V`;`vl`];
1812 ASM_REWRITE_TAC[GSYM Sphere.sqrt2];
1814 TYPIFY `set_of_list(truncate_simplex 2 vl) = {EL 0 vl,EL 1 vl,EL 2 vl}` (C SUBGOAL_THEN ASSUME_TAC);
1815 GMATCH_SIMP_TAC set_of_list3;
1817 REPEAT (GMATCH_SIMP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
1820 TYPIFY `barV V 2 (truncate_simplex 2 vl)` (C SUBGOAL_THEN ASSUME_TAC);
1821 GMATCH_SIMP_TAC Packing3.TRUNCATE_SIMPLEX_BARV;
1822 BY(ASM_MESON_TAC[arith `2 <= 3`]);
1824 INTRO_TAC GBEWYFX [`V`;`truncate_simplex 2 vl`];
1826 BY(ASM_SIMP_TAC[leaf;IN]);
1828 COMMENT "main reduction";
1829 TYPIFY `(mxi V vl IN affine hull set_of_list (truncate_simplex 2 vl))` ENOUGH_TO_SHOW_TAC;
1831 INTRO_TAC Rogers.OAPVION3 [`set_of_list (truncate_simplex 2 vl)`];
1834 FIRST_X_ASSUM_ST `collinear` MP_TAC;
1836 MATCH_MP_TAC AFFINE_DEPENDENT_IMP_COLLINEAR_3;
1837 BY(ASM_MESON_TAC[]);
1838 GOAL_TERM (fun w -> (DISCH_THEN (MP_TAC o (ISPEC ( env w `mxi V vl`)))));
1840 INTRO_TAC MXI_IN_VORONOI_LIST [`V`;`vl`];
1842 REPEAT WEAK_STRIP_TAC;
1843 FIRST_X_ASSUM MP_TAC;
1845 GOAL_TERM (fun w -> (EXISTS_TAC ( env w `sqrt2`)));
1846 REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
1849 INTRO_TAC VORONOI_LIST_EQ [`V`;`truncate_simplex 2 vl`;`mxi V vl`;`2`];
1851 BY(ASM_REWRITE_TAC[]);
1852 REPEAT WEAK_STRIP_TAC;
1854 DISCH_THEN GMATCH_SIMP_TAC;
1855 ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
1856 GOAL_TERM (fun w -> (FIRST_X_ASSUM (MP_TAC o (ISPEC ( env w `EL 0 vl`)))));
1857 ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
1858 BY(ASM_MESON_TAC[DIST_SYM]);
1859 INTRO_TAC GBEWYFX [`V`;`truncate_simplex 2 vl`];
1861 BY(ASM_SIMP_TAC[leaf;IN]);
1862 FIRST_X_ASSUM_ST `hl` MP_TAC;
1863 ASM_REWRITE_TAC[Pack_defs.HL];
1864 INTRO_TAC NOT_COL_IMP_RADV [`EL 0 vl`;`EL 1 vl`; `EL 2 vl`];
1866 BY(ASM_MESON_TAC[]);
1867 REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
1868 FIRST_X_ASSUM MP_TAC;
1869 BY(MESON_TAC[arith `~(sqrt2 < sqrt2)` ; DIST_SYM]);
1870 COMMENT "back to 1 goal";
1871 TYPIFY `coplanar (set_of_list (truncate_simplex 2 vl) UNION {mxi V vl})` (C SUBGOAL_THEN ASSUME_TAC);
1872 MATCH_MP_TAC COPLANAR_SUBSET;
1873 GOAL_TERM (fun w -> (EXISTS_TAC ( env w `mcell3 V vl`)));
1875 BY(MESON_TAC[HULL_SUBSET]);
1877 TYPIFY `aff_dim (set_of_list (truncate_simplex 2 vl) UNION {mxi V vl}) <= &2` (C SUBGOAL_THEN ASSUME_TAC);
1878 MATCH_MP_TAC COPLANAR_IMP_AFF_DIM;
1879 BY(ASM_REWRITE_TAC[]);
1880 TYPIFY `&2 <= aff_dim (set_of_list (truncate_simplex 2 vl))` (C SUBGOAL_THEN ASSUME_TAC);
1881 INTRO_TAC COLLINEAR_AFF_DIM [`(set_of_list (truncate_simplex 2 vl))`];
1884 FIRST_X_ASSUM_ST `UNION` MP_TAC;
1886 INTRO_TAC AFF_DIM_INSERT [`mxi V vl`;`set_of_list (truncate_simplex 2 vl)`];
1889 FIRST_X_ASSUM_ST `aff_dim` MP_TAC;
1890 TYPIFY `mxi V vl INSERT set_of_list (truncate_simplex 2 vl) = set_of_list (truncate_simplex 2 vl) UNION {mxi V vl}` (C SUBGOAL_THEN SUBST1_TAC);
1896 let MCELL2_SUBSET_AFF_GE = prove_by_refinement(
1897 `!V ul. mcell2 V ul SUBSET aff_ge {HD ul, HD (TL ul)} {mxi V ul, omega_list_n V ul 3}`,
1900 REPEAT WEAK_STRIP_TAC;
1901 REWRITE_TAC[Pack_defs.mcell2];
1903 REWRITE_TAC[LET_DEF;LET_END_DEF];
1909 let CONDS_IN_CONV2 = prove_by_refinement(
1910 `!t2 t3 (v:real^A) w. &0 <= t2 /\ &0 <= t3 /\ ~(t2 = &0 /\ t3 = &0)
1911 ==> t2 / (t2 + t3) % v + t3 / (t2 + t3) % w IN conv {v, w}`,
1914 MESON_TAC[Local_lemmas.CONDS_IN_CONV2]
1918 let NEG_SIGNS_LEMMA = prove_by_refinement(
1919 `!(a:real^3) b c d t0' t0'' t1 t1' s s'.
1920 aff {a, b} INTER conv {c, d} = {} /\
1921 c = t0' % a + t1 % b + s % p /\
1922 t0' + t1 + s = &1 /\
1923 d = t0'' % a + t1' % b + s' % p /\
1924 t0'' + t1' + s' = &1
1926 s < &0 ==> s' < &0`,
1929 REPEAT WEAK_STRIP_TAC;
1930 REWRITE_TAC[arith `s' < &0 <=> ~(&0 <= s')`];
1932 FIRST_X_ASSUM_ST `INTER` MP_TAC;
1933 REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER;NOT_FORALL_THM];
1934 GOAL_TERM (fun w -> (EXISTS_TAC( env w ` (s' / ( s' + (-- s))) % c + ((-- s) / (s' + (--s))) % d`)));
1936 MATCH_MP_TAC CONDS_IN_CONV2;
1937 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1939 TYPIFY `s' / (s' + --s) % (t0' % a + t1 % b + s % p) + --s / (s' + --s) % (t0'' % a + t1' % b + s' % p) = s' / (s' + --s) % (t0' % a + t1 % b ) + --s / (s' + --s) % (t0'' % a + t1' % b ) + ((s' * s/ (s' + --s)) + ( s' * (--s) / (s' + --s))) % p` (C SUBGOAL_THEN SUBST1_TAC);
1940 BY(VECTOR_ARITH_TAC);
1941 TYPIFY ` (s' * s / (s' + --s) + s' * --s / (s' + --s)) = &0` (C SUBGOAL_THEN SUBST1_TAC);
1942 Calc_derivative.CALC_ID_TAC;
1943 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1944 REWRITE_TAC[Sphere.aff];
1945 REWRITE_TAC[AFFINE_HULL_2;IN_ELIM_THM];
1946 GEXISTL_TAC [`(s' / (s' + --s) * t0' + (-- s)/(s' + --s) * t0'')`;`(s' / (s' + --s) * t1 + (-- s)/(s' + --s) * t1')`];
1948 Calc_derivative.CALC_ID_TAC;
1950 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1951 REPEAT (FIRST_X_ASSUM_ST `&1` MP_TAC);
1952 BY(CONV_TAC (REAL_RING));
1953 BY(VECTOR_ARITH_TAC)
1957 let COPLANAR_AFF_GE_REDUCE = prove_by_refinement(
1958 `!(a:real^3) b c d. coplanar {a,b,c,d} /\ aff {a,b} INTER conv {c,d} = {} /\
1959 ~(a = b) ==> (?p. aff_ge {a,b} {c,d} SUBSET aff_ge {a,b} {p})`,
1962 REPEAT WEAK_STRIP_TAC;
1963 TYPIFY `aff_ge {a,b} {c,d} SUBSET aff{a,b}` ASM_CASES_TAC;
1964 TYPIFY `?p. DISJOINT {a,b} {p}` (C SUBGOAL_THEN MP_TAC);
1965 BY(ASM_MESON_TAC[Fan.th3a;Trigonometry2.TOW_DISTINCT_POINTS_EXISTS_RD_NOT_COLLINEAR]);
1966 REPEAT WEAK_STRIP_TAC;
1967 GOAL_TERM (fun w -> (EXISTS_TAC ( env w `p`)));
1968 BY(ASM_MESON_TAC[AFF_GE_MONO_RIGHT;SUBSET_TRANS;EMPTY_SUBSET;AFF_GE_EQ_AFFINE_HULL;Trigonometry2.aff]);
1969 TYPIFY `?p. p IN aff_ge {a,b} {c,d} DIFF aff{a,b}` (C SUBGOAL_THEN MP_TAC);
1970 FIRST_X_ASSUM MP_TAC;
1972 REWRITE_TAC[IN_DIFF];
1973 REPEAT WEAK_STRIP_TAC;
1974 GOAL_TERM (fun w -> (EXISTS_TAC ( env w `p`)));
1975 TYPIFY `p IN affine hull {a,b,c,d}` (C SUBGOAL_THEN ASSUME_TAC);
1976 INTRO_TAC AFF_GE_SUBSET_AFFINE_HULL [`{a,b}`;`{c,d}`];
1977 TYPIFY `{a,b} UNION {c,d} = {a,b,c,d}` (C SUBGOAL_THEN SUBST1_TAC);
1979 FIRST_X_ASSUM_ST `aff_ge` MP_TAC;
1981 TYPIFY `~(collinear {a,b,p})` (C SUBGOAL_THEN ASSUME_TAC);
1982 FIRST_X_ASSUM (MP_TAC o (MATCH_MP COLLINEAR_3_IN_AFFINE_HULL) o GSYM);
1983 BY(ASM_MESON_TAC[Sphere.aff]);
1984 TYPIFY `aff_dim {a,b,p} = &2` (C SUBGOAL_THEN ASSUME_TAC);
1985 FIRST_X_ASSUM MP_TAC;
1986 REWRITE_TAC[COLLINEAR_AFF_DIM];
1987 INTRO_TAC AFF_DIM_2 [`a`;`b`];
1989 INTRO_TAC AFF_DIM_INSERT [`p`;`{a,b}`];
1990 ASM_REWRITE_TAC[GSYM Sphere.aff];
1991 TYPIFY `{p,a,b} = {a,b,p}` (C SUBGOAL_THEN SUBST1_TAC);
1994 INTRO_TAC AFF_DIM_EQ_AFFINE_HULL [`{a,b,p}`;`affine hull {a,b,c,d}`];
1997 REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
1998 BY(REPEAT WEAK_STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC HULL_INC THEN SET_TAC[]);
1999 INTRO_TAC COPLANAR_IMP_AFF_DIM [`{a,b,c,d}`];
2001 BY(REWRITE_TAC[AFF_DIM_AFFINE_HULL]);
2002 REWRITE_TAC[Planarity.AFFINE_HULL_AFFINE_EQ];
2004 TYPIFY `{c,d} SUBSET affine hull {a,b,p}` (C SUBGOAL_THEN ASSUME_TAC);
2006 REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
2007 BY(REPEAT WEAK_STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC HULL_INC THEN SET_TAC[]);
2008 TYPIFY `(?tt0 t1 s. c = tt0 % a + t1 % b + s % p /\ tt0 + t1 + s = &1) /\ (?tt0' t1' s'. d = tt0' % a + t1' % b + s' % p /\ tt0' + t1' + s' = &1)` (C SUBGOAL_THEN MP_TAC);
2009 FIRST_X_ASSUM MP_TAC;
2010 REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
2011 REWRITE_TAC[AFFINE_HULL_3;IN_ELIM_THM];
2013 REPEAT WEAK_STRIP_TAC;
2014 SUBGOAL_THEN `s < &0 ==> s' < &0` ASSUME_TAC;
2015 COMMENT "change here";
2016 MATCH_MP_TAC NEG_SIGNS_LEMMA;
2017 GEXISTL_TAC [`a`;`b`;`c`;`d`;`tt0`;`tt0'`;`t1`;`t1'`];
2018 BY(ASM_REWRITE_TAC[]);
2019 SUBGOAL_THEN `s' < &0 ==> s < &0` ASSUME_TAC;
2020 MATCH_MP_TAC NEG_SIGNS_LEMMA;
2021 GEXISTL_TAC [`a`;`b`;`d`;`c`;`tt0'`;`tt0`;`t1'`;`t1`];
2022 TYPIFY `{d,c} = {c,d}` (C SUBGOAL_THEN SUBST1_TAC);
2024 BY(ASM_REWRITE_TAC[]);
2025 COMMENT "back to 1";
2027 FIRST_X_ASSUM_ST `x IN aff_ge u v` MP_TAC;
2028 TYPIFY `DISJOINT {a,b} {c,d}` (C SUBGOAL_THEN ASSUME_TAC);
2029 FIRST_X_ASSUM_ST `INTER` MP_TAC;
2030 REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER;Sphere.aff;DISJOINT;IN_INSERT];
2031 TYPIFY `a IN {a,b} /\ b IN {a,b} /\ c IN {c,d} /\ d IN {c,d}` (C SUBGOAL_THEN MP_TAC);
2033 TYPIFY `({a,b} = {b,a}) /\ ({c,d} = {d,c})` (C SUBGOAL_THEN MP_TAC);
2035 BY(MESON_TAC[HULL_INC;Geomdetail.U_IN_CONV2]);
2036 INTRO_TAC Nkezbfc_local.AFF_GE_2_2 [`a`;`b`;`c`;`d`];
2038 BY(ASM_REWRITE_TAC[]);
2039 DISCH_THEN SUBST1_TAC;
2040 REWRITE_TAC[IN_ELIM_THM];
2041 REPEAT WEAK_STRIP_TAC;
2042 FIRST_X_ASSUM MP_TAC;
2044 TYPIFY `(p = t1'' % a + t2 % b + t3 % (tt0 % a + t1 % b + s % p) + t4 % (tt0' % a + t1' % b + s' % p)) <=> (&1 - t3 * s - t4 * s') % p = (t1'' + t3 * tt0 + t4 * tt0' ) % a + (t2 + t3 * t1 + t4 * t1') % b` (C SUBGOAL_THEN SUBST1_TAC);
2045 BY(VECTOR_ARITH_TAC);
2046 ASM_CASES_TAC `~(&1 - t3 * s - t4 * s' = &0)`;
2048 FIRST_X_ASSUM_ST `aff` MP_TAC;
2049 REWRITE_TAC[Sphere.aff;AFFINE_HULL_2;IN_ELIM_THM];
2050 GEXISTL_TAC [`(t1'' + t3 * tt0 + t4 * tt0')/(&1 - t3 * s - t4 * s')`;`(t2 + t3 * t1 + t4 * t1')/(&1 - t3 * s - t4 * s')`];
2052 Calc_derivative.CALC_ID_TAC;
2054 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN (CONV_TAC REAL_RING));
2055 MATCH_MP_TAC VECTOR_MUL_LCANCEL_IMP;
2056 EXISTS_TAC `&1 - t3 * s - t4 * s'`;
2058 REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC];
2059 TYPIFY `((&1 - t3 * s - t4 * s') * (t1'' + t3 * tt0 + t4 * tt0') / (&1 - t3 * s - t4 * s')) = (t1'' + t3 * tt0 + t4 * tt0')` (C SUBGOAL_THEN SUBST1_TAC);
2060 Calc_derivative.CALC_ID_TAC;
2061 BY(ASM_REWRITE_TAC[]);
2062 TYPIFY `((&1 - t3 * s - t4 * s') * (t2 + t3 * t1 + t4 * t1') / (&1 - t3 * s - t4 * s')) = (t2 + t3 * t1 + t4 * t1')` (C SUBGOAL_THEN SUBST1_TAC);
2063 Calc_derivative.CALC_ID_TAC;
2064 BY(ASM_REWRITE_TAC[]);
2066 FIRST_X_ASSUM MP_TAC;
2068 (REPEAT WEAK_STRIP_TAC);
2069 FIRST_X_ASSUM_ST `~` MP_TAC;
2071 TYPIFY `&0 <= s /\ &0 <= s'` (C SUBGOAL_THEN ASSUME_TAC);
2072 REWRITE_TAC[arith `&0 <= s /\ &0 <= s' <=> ~(s < &0 \/ s' < &0)`];
2074 TYPIFY `s < &0 /\ s' < &0` (C SUBGOAL_THEN ASSUME_TAC);
2075 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2076 TYPIFY `&0 < t3 * s + t4 * s' ` (C SUBGOAL_THEN MP_TAC);
2077 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2079 MATCH_MP_TAC (arith `&0 <= t3 * (-- s) /\ &0 <= t4 * (-- s') ==> ~(&0 < t3 *( s) + t4 * ( s'))`);
2080 GMATCH_SIMP_TAC REAL_LE_MUL;
2081 GMATCH_SIMP_TAC REAL_LE_MUL;
2082 BY(ASM_SIMP_TAC[arith `ss < &0 ==> &0 <= -- ss`]);
2083 REWRITE_TAC[SUBSET];
2085 GMATCH_SIMP_TAC Marchal_cells_2_new.AFF_GE_2_2;
2087 GMATCH_SIMP_TAC AFF_GE_2_1;
2088 ASM_REWRITE_TAC[IN_ELIM_THM];
2090 MATCH_MP_TAC Fan.th3a;
2091 BY(ASM_REWRITE_TAC[]);
2092 REPEAT WEAK_STRIP_TAC;
2094 GEXISTL_TAC [`t1'''+t3' * tt0 + t4' * tt0'`;`t2' + t3' * t1 + t4' * t1'`;`t3' * s + t4' * s'`];
2096 MATCH_MP_TAC (arith `&0 <= x /\ &0 <= y ==> &0 <= x + y`);
2097 GMATCH_SIMP_TAC REAL_LE_MUL;
2098 GMATCH_SIMP_TAC REAL_LE_MUL;
2099 BY(ASM_REWRITE_TAC[]);
2101 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN (CONV_TAC REAL_RING));
2102 BY(VECTOR_ARITH_TAC)
2106 let AFFINE_DEPENDENT_EXPLICIT_4 = prove_by_refinement(
2107 `!(a:real^A) b c d ta tb tc td. ~affine_dependent {a,b,c,d} /\
2108 CARD {a,b,c,d} = 4 /\
2109 ta + tb + tc + td = &0 /\
2110 ta % a + tb % b + tc % c + td % d = vec 0 ==>
2111 (ta = &0 /\ tb = &0 /\ tc = &0 /\ td = &0)`,
2114 REPEAT WEAK_STRIP_TAC;
2115 INTRO_TAC AFFINE_DEPENDENT_EXPLICIT[`{a,b,c,d}`];
2117 REWRITE_TAC[NOT_EXISTS_THM];
2118 DISCH_THEN (C INTRO_TAC [`{a,b,c,d}`;`\u. if (u=a) then ta else (if (u=b) then tb else (if (u=c) then tc else td))`]);
2119 TYPIFY `FINITE {a,b,c,d}` (C SUBGOAL_THEN (unlist REWRITE_TAC));
2120 BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]);
2121 TYPIFY `{a, b, c, d} SUBSET {a, b, c, d}` (C SUBGOAL_THEN (unlist REWRITE_TAC));
2123 TYPIFY `~(a = b) /\ ~(a = c) /\ ~(a = d) /\ ~(b = c) /\ ~(b = d) /\ ~(c = d)` (C SUBGOAL_THEN (ASSUME_TAC));
2124 TYPIFY ` {a,b,c,d} = {a,c,b,d} /\ {a,b,c,d}= {a,d,b,c} /\ {a,b,c,d} = {b,c,a,d} /\ {a,b,c,d} = {b,d,a,c} /\ {a,b,c,d} = {c,d,a,b}` (C SUBGOAL_THEN MP_TAC);
2126 REPEAT WEAK_STRIP_TAC;
2127 BY(REPEAT CONJ_TAC THEN MATCH_MP_TAC Marchal_cells_2_new.CARD4_IMP_DISTINCT THEN FIRST_X_ASSUM_ST `4` (SUBST1_TAC o GSYM) THEN (REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC)) THEN MESON_TAC[]);
2128 TYPIFY `vsum {a, b, c, d} (\v. (if v = a then ta else if v = b then tb else if v = c then tc else td) % v) = vec 0` (C SUBGOAL_THEN (unlist REWRITE_TAC));
2129 REPEAT (GMATCH_SIMP_TAC (CONJUNCT2 VSUM_CLAUSES));
2130 REWRITE_TAC[ (CONJUNCT1 VSUM_CLAUSES)];
2131 ASM_REWRITE_TAC[FINITE_EMPTY;FINITE_INSERT;NOT_IN_EMPTY;IN_INSERT];
2132 FIRST_X_ASSUM_ST `0` MP_TAC;
2133 BY(VECTOR_ARITH_TAC);
2134 TYPIFY `sum {a, b, c, d} (\u. if u = a then ta else if u = b then tb else if u = c then tc else td) = &0` (C SUBGOAL_THEN (unlist REWRITE_TAC));
2135 REPEAT (GMATCH_SIMP_TAC (CONJUNCT2 SUM_CLAUSES));
2136 REWRITE_TAC[ (CONJUNCT1 SUM_CLAUSES)];
2137 ASM_REWRITE_TAC[FINITE_EMPTY;FINITE_INSERT;NOT_IN_EMPTY;IN_INSERT];
2138 FIRST_X_ASSUM_ST `&0` MP_TAC;
2140 REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
2141 REWRITE_TAC[NOT_EXISTS_THM];
2145 DISCH_THEN (C INTRO_TAC [`a`]);
2146 FIRST_X_ASSUM (C INTRO_TAC [`b`]);
2147 FIRST_X_ASSUM (C INTRO_TAC [`c`]);
2148 FIRST_X_ASSUM (C INTRO_TAC [`d`]);
2154 let COPLANAR_AFF_GE_REDUCE2 = prove_by_refinement(
2155 `!S (a:real^3) b c d. ~coplanar {a,b,c,d} /\ coplanar S /\ {a,b} SUBSET S /\ S SUBSET aff_ge {a,b} {c,d} ==>
2156 (?p. S SUBSET aff_ge {a,b} {p})`,
2159 REPEAT WEAK_STRIP_TAC;
2160 TYPIFY `~(a = b)` (C SUBGOAL_THEN ASSUME_TAC);
2162 FIRST_X_ASSUM_ST `~` MP_TAC;
2164 TYPIFY `{b,b,c,d} = {b,c,d}` (C SUBGOAL_THEN SUBST1_TAC);
2166 BY(REWRITE_TAC[COPLANAR_3]);
2167 TYPIFY `S SUBSET affine hull {a,b}` ASM_CASES_TAC;
2168 TYPIFY `?p. DISJOINT {a,b} {p}` (C SUBGOAL_THEN MP_TAC);
2169 BY(ASM_MESON_TAC[Fan.th3a;Trigonometry2.TOW_DISTINCT_POINTS_EXISTS_RD_NOT_COLLINEAR]);
2170 REPEAT WEAK_STRIP_TAC;
2171 GOAL_TERM (fun w -> (EXISTS_TAC ( env w `p`)));
2172 BY(ASM_MESON_TAC[AFF_GE_MONO_RIGHT;SUBSET_TRANS;EMPTY_SUBSET;AFF_GE_EQ_AFFINE_HULL;Trigonometry2.aff]);
2173 TYPIFY `?p. p IN S DIFF affine hull {a,b}` (C SUBGOAL_THEN MP_TAC);
2174 FIRST_X_ASSUM MP_TAC;
2176 REPEAT WEAK_STRIP_TAC;
2177 TYPIFY `p` EXISTS_TAC;
2178 TYPIFY `p IN aff_ge {a,b} {c,d}` (C SUBGOAL_THEN ASSUME_TAC);
2179 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
2180 REWRITE_TAC[SUBSET];
2181 REPEAT WEAK_STRIP_TAC;
2182 TYPIFY `x IN aff_ge {a,b} {c,d}` (C SUBGOAL_THEN ASSUME_TAC);
2183 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
2184 TYPIFY `~(collinear {a,b,p})` (C SUBGOAL_THEN ASSUME_TAC);
2185 FIRST_X_ASSUM (MP_TAC o (MATCH_MP COLLINEAR_3_IN_AFFINE_HULL) o GSYM);
2186 DISCH_THEN (C INTRO_TAC [`p`]);
2187 DISCH_THEN SUBST1_TAC;
2188 FIRST_X_ASSUM_ST `DIFF` MP_TAC;
2190 TYPIFY `aff_dim {a,b,p} = &2` (C SUBGOAL_THEN ASSUME_TAC);
2191 FIRST_X_ASSUM MP_TAC;
2192 REWRITE_TAC[COLLINEAR_AFF_DIM];
2193 INTRO_TAC AFF_DIM_2 [`a`;`b`];
2195 INTRO_TAC AFF_DIM_INSERT [`p`;`{a,b}`];
2196 ASM_REWRITE_TAC[GSYM Sphere.aff];
2197 TYPIFY `{p,a,b} = {a,b,p}` (C SUBGOAL_THEN SUBST1_TAC);
2200 INTRO_TAC AFF_DIM_EQ_AFFINE_HULL [`{a,b,p}`;`affine hull S`];
2203 MATCH_MP_TAC SUBSET_TRANS;
2204 TYPIFY `S` EXISTS_TAC;
2206 BY(REWRITE_TAC[HULL_SUBSET]);
2207 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
2208 INTRO_TAC COPLANAR_IMP_AFF_DIM [`S`];
2210 BY(REWRITE_TAC[AFF_DIM_AFFINE_HULL]);
2211 REWRITE_TAC[Planarity.AFFINE_HULL_AFFINE_EQ];
2213 TYPIFY `x IN affine hull {a,b,p}` (C SUBGOAL_THEN ASSUME_TAC);
2215 BY(ASM_MESON_TAC[HULL_SUBSET;SUBSET;IN]);
2216 REPEAT (FIRST_X_ASSUM_ST `p IN aff_ge {a,b} {c,d}` MP_TAC);
2217 REPEAT (GMATCH_SIMP_TAC Marchal_cells_2_new.AFF_GE_2_2);
2219 FIRST_X_ASSUM_ST `~coplanar U` MP_TAC;
2220 TYPIFY `{a,b,c,d} = {a,c,b,d}` ((C SUBGOAL_THEN SUBST1_TAC));
2222 BY(MESON_TAC[Planarity.notcoplanar_disjoints]);
2223 GMATCH_SIMP_TAC AFF_GE_2_1;
2225 BY(ASM_MESON_TAC[Fan.th3a]);
2226 REWRITE_TAC[IN_ELIM_THM];
2227 REPEAT WEAK_STRIP_TAC;
2228 FIRST_X_ASSUM_ST `affine` MP_TAC;
2229 REWRITE_TAC[AFFINE_HULL_3];
2230 REWRITE_TAC[IN_ELIM_THM];
2231 REPEAT WEAK_STRIP_TAC;
2232 GEXISTL_TAC [`u`;`v`;`w`];
2234 BY(ASM_MESON_TAC[]);
2235 FIRST_X_ASSUM MP_TAC;
2237 TYPIFY `(t1' % a + t2' % b + t3' % c + t4' % d = u % a + v % b + w % (t1 % a + t2 % b + t3 % c + t4 % d)) <=> (t1' - w * t1 - u) % a + (t2' - w * t2 - v) % b + (t3' - w * t3) % c + (t4' - w * t4) % d = vec 0` (C SUBGOAL_THEN (unlist REWRITE_TAC));
2238 BY(VECTOR_ARITH_TAC);
2240 TYPIFY `CARD {a,b,c,d} = 4` ((C SUBGOAL_THEN ASSUME_TAC));
2241 MATCH_MP_TAC Collect_geom2.NOT_COPLANAR_IMP_CARD4;
2242 GMATCH_SIMP_TAC (GSYM coplanar_eq_coplanar_alt);
2243 REWRITE_TAC[DIMINDEX_3];
2246 TYPIFY `~affine_dependent {a,b,c,d}` ((C SUBGOAL_THEN ASSUME_TAC));
2248 FIRST_X_ASSUM (MP_TAC o (MATCH_MP Njiutiu.AFF_DEPENDENT_AFF_DIM_4));
2249 BY(ASM_MESON_TAC[Rogers.AFF_DIM_LE_2_IMP_COPLANAR]);
2250 INTRO_TAC AFFINE_DEPENDENT_EXPLICIT_4 [`a`;`b`;`c`;`d`;`t1' - w * t1 - u`;`t2' - w * t2 - v`;`t3' - w * t3`;`t4' - w * t4`];
2253 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN CONV_TAC REAL_RING);
2254 REWRITE_TAC[arith `a - b = &0 <=> a = b`];
2255 REPEAT WEAK_STRIP_TAC;
2256 TYPIFY `&0 <= w * t3 /\ &0 <= w * t4` ((C SUBGOAL_THEN MP_TAC));
2257 BY(ASM_MESON_TAC[]);
2258 REWRITE_TAC[Misc_defs_and_lemmas.REAL_MUL_NN];
2259 ASM_SIMP_TAC[arith `&0 <= t ==> (t <= &0 <=> t = &0)`];
2260 ENOUGH_TO_SHOW_TAC `t3 = &0 /\ t4 = &0 ==> F`;
2262 REPEAT WEAK_STRIP_TAC;
2263 REPEAT (FIRST_X_ASSUM_ST `%` MP_TAC);
2265 TYPIFY `t1 % a + t2 % b + &0 % c + &0 % d = t1 % a + t2 % b` (C SUBGOAL_THEN SUBST1_TAC);
2266 BY(VECTOR_ARITH_TAC);
2267 REPEAT WEAK_STRIP_TAC;
2268 FIRST_X_ASSUM_ST `DIFF` MP_TAC;
2269 REWRITE_TAC[DIFF;AFFINE_HULL_2;IN_ELIM_THM;NOT_EXISTS_THM];
2270 REPEAT WEAK_STRIP_TAC;
2271 FIRST_X_ASSUM (C INTRO_TAC [`t1`;`t2`]);
2274 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2275 BY(ASM_REWRITE_TAC[])
2279 let CONVEX_PLANE_INTER = prove_by_refinement(
2280 `!(a:real^A) b p q. ~(a = b) /\ DISJOINT {a,b} {p} /\ q IN aff_gt {a,b} {p} ==>
2281 (?c. c IN aff_gt {a,b} {p} /\
2282 c IN convex hull {a,b,p} INTER convex hull {a,b,q})`,
2285 REPEAT WEAK_STRIP_TAC;
2286 FIRST_X_ASSUM_ST `IN` MP_TAC;
2287 (GMATCH_SIMP_TAC AFF_GT_2_1);
2288 ASM_REWRITE_TAC[IN_ELIM_THM];
2289 REPEAT WEAK_STRIP_TAC;
2290 ABBREV_TAC `(r:real->real^A) t = (&1 - t) % ((&1/ &2) % a + (&1/ &2) % b) + t % p`;
2291 TYPIFY `!t. &0 <= t /\ t <= &1 ==> r t IN convex hull {a,b,p}` ((C SUBGOAL_THEN ASSUME_TAC));
2292 REPEAT WEAK_STRIP_TAC;
2293 REWRITE_TAC[CONVEX_HULL_3;IN_ELIM_THM];
2294 GEXISTL_TAC [`(&1 -t) / &2`;`(&1- t)/ &2`;`t`];
2297 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2298 GOAL_TERM (fun w -> (FIRST_X_ASSUM (SUBST1_TAC o GSYM o (ISPEC ( env w `t`)))));
2299 BY(VECTOR_ARITH_TAC);
2300 TYPIFY `?t. &0 < t /\ t <= &1 /\ r t IN convex hull {a,b,q}` ENOUGH_TO_SHOW_TAC;
2301 REPEAT WEAK_STRIP_TAC;
2302 TYPIFY `r t` EXISTS_TAC;
2304 GEXISTL_TAC [`(&1 - t) / &2 `;`(&1 - t)/ &2`;`t`];
2308 GOAL_TERM (fun w -> (FIRST_X_ASSUM (SUBST1_TAC o GSYM o (ISPEC ( env w `t`)))));
2309 BY(VECTOR_ARITH_TAC);
2310 REWRITE_TAC[IN_INTER];
2312 REWRITE_TAC[CONVEX_HULL_3];
2313 REWRITE_TAC[IN_ELIM_THM];
2314 GEXISTL_TAC [`(&1 - t) / &2 `;`(&1 - t)/ &2`;`t`];
2316 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2317 GOAL_TERM (fun w -> (FIRST_X_ASSUM (SUBST1_TAC o GSYM o (ISPEC ( env w `t`)))));
2318 BY(VECTOR_ARITH_TAC);
2319 REWRITE_TAC[CONVEX_HULL_3;IN_ELIM_THM];
2321 ABBREV_TAC `eps = inv (abs t1 + abs t2 + &2 * abs t3 + &2 * abs (t1 - t2 - &1) + &2 * abs(t2 - t1 - &1) + &10)`;
2322 EXISTS_TAC `&2 * eps * t3`;
2324 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
2325 REWRITE_TAC[ REAL_OF_NUM_LT];
2326 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
2330 GMATCH_SIMP_TAC REAL_LT_INV;
2335 REWRITE_TAC[arith `a * inv b * c = (a * c)/ b`];
2336 GMATCH_SIMP_TAC REAL_LE_LDIV_EQ;
2340 TYPIFY `&0 <= eps` (C SUBGOAL_THEN ASSUME_TAC);
2342 REWRITE_TAC[REAL_LE_INV_EQ];
2344 GEXISTL_TAC [`&1/ &2 + eps * ( (t2 - t1) - &1 )`;`&1/ &2 + eps * ( (t1 - t2) - &1 )`;`&2 * eps`];
2345 TYPIFY `(&1 / &2 + eps * (t2 - t1 - &1)) + (&1 / &2 + eps * (t1 - t2 - &1)) + &2 * eps = &1` (C SUBGOAL_THEN (unlist REWRITE_TAC));
2347 TYPIFY `r (&2 * eps * t3) = (&1 / &2 + eps * (t2 - t1 - &1)) % a + (&1 / &2 + eps * (t1 - t2 - &1)) % b + (&2 * eps) % (t1 % a + t2 % b + t3 % p)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
2348 GOAL_TERM (fun w -> (FIRST_X_ASSUM (SUBST1_TAC o GSYM o (ISPEC ( env w `&2 * eps * t3`)))));
2349 FIRST_X_ASSUM_ST `t1 + t2 + t3 = &1` ((unlist REWRITE_TAC) o (REWRITE_RULE[arith `t1 + t2 + t3 = &1 <=> t3 = &1 - t2 - t1`]));
2350 BY(VECTOR_ARITH_TAC);
2351 TYPIFY `&0 <= &2 * eps` (C SUBGOAL_THEN (unlist REWRITE_TAC));
2352 GMATCH_SIMP_TAC REAL_LE_MUL;
2353 BY(ASM_REWRITE_TAC[arith `&0 <= &2`]);
2354 REPEAT (GMATCH_SIMP_TAC (arith `abs(a * b) <= &1 / &2 ==> &0 <= &1/ &2 + a * b`));
2355 REWRITE_TAC[REAL_ABS_MUL];
2356 ASM_SIMP_TAC[arith `&0 <= eps ==> abs (eps) = eps`];
2357 GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
2358 REWRITE_TAC[ REAL_OF_NUM_LT];
2360 GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
2361 REWRITE_TAC[ REAL_OF_NUM_LT];
2362 REWRITE_TAC[arith `0 < 2`];
2363 REWRITE_TAC[arith `(inv a * b) * d <= c <=> (b * d) / a <= c`];
2364 GMATCH_SIMP_TAC REAL_LE_LDIV_EQ;
2365 GMATCH_SIMP_TAC REAL_LE_LDIV_EQ;
2370 let CONVEX_R3_INTER = prove_by_refinement(
2371 `!(a:real^3) b c p q. ~coplanar {a,b,c,p} /\ q IN aff_gt {a,b,c} {p} ==>
2372 (?d. ~coplanar {a,b,c,d} /\ d IN convex hull {a,b,c,p} INTER convex hull {a,b,c,q})`,
2375 REPEAT WEAK_STRIP_TAC;
2376 TYPIFY `DISJOINT {a,b,c} {p}` ((C SUBGOAL_THEN ASSUME_TAC));
2377 BY(ASM_MESON_TAC[Planarity.notcoplanar_disjoints]);
2378 FIRST_X_ASSUM_ST `IN` MP_TAC;
2379 GMATCH_SIMP_TAC AFF_GT_3_1;
2380 ASM_REWRITE_TAC[IN_ELIM_THM];
2381 REPEAT WEAK_STRIP_TAC;
2382 ABBREV_TAC `(r:real^3) = (&1 / &3) % a + (&1/ &3 ) % b + (&1 / &3) % c`;
2383 TYPIFY `?t. ~coplanar {a,b,c, (&1 - t) % r + t % q} /\ (&1 - t) % r + t % q IN convex hull{a,b,c,p} INTER convex hull {a,b,c,q}` ENOUGH_TO_SHOW_TAC;
2385 REWRITE_TAC[IN_INTER];
2386 REWRITE_TAC[Marchal_cells_2_new.CONVEX_HULL_4];
2387 ASM_REWRITE_TAC[IN_ELIM_THM];
2389 TYPIFY `?s. s < &1 /\ &0 < s /\ &0 < (&1 - s)/ &3 + s * t1 /\ &0 < (&1 -s)/ &3 + s * t2 /\ &0 < (&1 - s)/ &3 + s * t3 ` (C SUBGOAL_THEN MP_TAC);
2390 EXISTS_TAC (`inv (&4 + &3 * abs t1 + &3 * abs t2 + &3 * abs t3)`);
2391 TYPIFY `&0 < &4 + &3 * abs t1 + &3 * abs t2 + &3 * abs t3` ((C SUBGOAL_THEN ASSUME_TAC));
2394 REWRITE_TAC[arith `inv x = &1 / x`];
2395 ASM_SIMP_TAC[REAL_LT_LDIV_EQ];
2398 GMATCH_SIMP_TAC REAL_LT_INV;
2399 BY(ASM_REWRITE_TAC[]);
2400 REWRITE_TAC[arith `&0 < (&1 - inv x)/ &3 + inv x * t <=> (&1 - &3 * t)/x < &1`];
2401 (ASM_SIMP_TAC[REAL_LT_LDIV_EQ]);
2403 REPEAT WEAK_STRIP_TAC;
2404 EXISTS_TAC `s:real`;
2407 GEXISTL_TAC [`(&1 - s)/ &3 + s * t1`;`(&1- s)/ &3 + s * t2`;`(&1- s)/ &3 + s * t3`;`s * t4`];
2408 ASM_SIMP_TAC[arith `&0 < x ==> &0 <= x`];
2409 GMATCH_SIMP_TAC REAL_LE_MUL;
2410 ASM_SIMP_TAC[arith `&0 < x ==> &0 <= x`];
2411 FIRST_X_ASSUM_ST `t1 + t2 + t3 + t4 = &1` (SUBST1_TAC o (REWRITE_RULE[arith `t1 + t2 + t3 + t4 = &1 <=> t4 = &1 - t1 - t2 - t3`]));
2415 BY(VECTOR_ARITH_TAC);
2416 GEXISTL_TAC [`(&1 - s)/ &3 `;`(&1- s)/ &3 `;`(&1- s)/ &3`;`s `];
2417 ASM_SIMP_TAC[arith `s < &1 ==> &0 <= (&1 - s) / &3`];
2418 ASM_SIMP_TAC[arith `&0 < x ==> &0 <= x`];
2421 FIRST_X_ASSUM_ST `t1 + t2 + t3 + t4 = &1` (SUBST1_TAC o (REWRITE_RULE[arith `t1 + t2 + t3 + t4 = &1 <=> t4 = &1 - t1 - t2 - t3`]));
2423 BY(VECTOR_ARITH_TAC);
2424 (COMMENT "last goal, coplanarity");
2425 FIRST_X_ASSUM_ST `coplanar` MP_TAC;
2426 REWRITE_TAC[CHI_MSB_COPLANAR];
2427 TYPIFY `((&1 - s) % (&1 / &3 % a + &1 / &3 % b + &1 / &3 % c) + s % (t1 % a + t2 % b + t3 % c + t4 % p)) = ((&1 - s)/ &3 + s * t1) % a + ((&1 - s)/ &3 + s * t2) % b + ((&1 - s) / &3 + s * t3) % c + (s * t4) % p` (C SUBGOAL_THEN SUBST1_TAC);
2428 BY(VECTOR_ARITH_TAC);
2430 GMATCH_SIMP_TAC chi_msb_additive_d;
2432 FIRST_X_ASSUM_ST `x = &1` MP_TAC;
2433 BY(CONV_TAC REAL_RING);
2434 REWRITE_TAC[REAL_ENTIRE];
2436 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
2440 let MCELL2_CONVEX = prove_by_refinement(
2441 `!V vl. saturated V /\ packing V /\ barV V 3 vl ==> convex (mcell2 V vl)`,
2444 REWRITE_TAC[Pack_defs.mcell2];
2445 REPEAT WEAK_STRIP_TAC;
2447 REWRITE_TAC[LET_DEF;LET_END_DEF];
2448 MATCH_MP_TAC CONVEX_INTER;
2449 GMATCH_SIMP_TAC CONVEX_INTER;
2450 REWRITE_TAC[CONVEX_AFF_GE];
2451 TYPIFY `&0 <= hl (truncate_simplex 1 vl) / sqrt (&2)` ENOUGH_TO_SHOW_TAC;
2452 BY(MESON_TAC[Marchal_cells_2_new.CONVEX_RCONE_GE]);
2453 GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
2454 REWRITE_TAC[arith `&0 * x = &0`];
2455 GMATCH_SIMP_TAC REAL_LT_RSQRT;
2458 BY(ASM_MESON_TAC[Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT;arith `&0 < x ==> &0 <= x`]);
2459 BY(REWRITE_TAC[CONVEX_EMPTY])
2463 let MCELL_CONVEX = prove_by_refinement(
2464 `!V vl k. saturated V /\ packing V /\ barV V 3 vl /\ 2 <= k ==> convex (mcell k V vl)`,
2467 REWRITE_TAC[Pack_defs.mcell];
2468 REPEAT WEAK_STRIP_TAC;
2469 TYPIFY `~(k=0) /\ ~(k=1)` (C SUBGOAL_THEN ASSUME_TAC);
2470 BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
2472 REPEAT COND_CASES_TAC;
2473 BY(ASM_MESON_TAC[MCELL2_CONVEX]);
2474 REWRITE_TAC[Pack_defs.mcell3];
2476 BY(REWRITE_TAC[CONVEX_CONVEX_HULL]);
2477 BY(REWRITE_TAC[CONVEX_EMPTY]);
2478 REWRITE_TAC[Pack_defs.mcell4];
2480 BY(REWRITE_TAC[CONVEX_CONVEX_HULL]);
2481 BY(REWRITE_TAC[CONVEX_EMPTY])
2485 let CHI_MSB_AFF_GT_0 = prove_by_refinement(
2486 `!a b c q q'. ~coplanar {a,b,c,q} /\
2487 &0 < chi_msb [a;b;c] q /\ &0 < chi_msb [a;b;c] q' ==>
2488 (q' IN aff_gt {a,b,c} {q})`,
2491 REPEAT WEAK_STRIP_TAC;
2492 INTRO_TAC AFF_DIM_EQ_AFFINE_HULL [`{a,b,c, q}`;`(:real^3)`];
2493 REWRITE_TAC[AFFINE_HULL_UNIV];
2497 REWRITE_TAC[AFF_DIM_UNIV;DIMINDEX_3];
2498 ENOUGH_TO_SHOW_TAC `~(aff_dim {a,b,c, (q:real^3)} <= &2)`;
2500 BY(ASM_MESON_TAC[Rogers.AFF_DIM_LE_2_IMP_COPLANAR]);
2501 REWRITE_TAC[EXTENSION;IN_UNIV];
2502 DISCH_THEN (C INTRO_TAC [`q'`]);
2503 REWRITE_TAC[Collect_geom2.AFFINE_HULL_4];
2504 REWRITE_TAC[IN_ELIM_THM];
2505 REPEAT WEAK_STRIP_TAC;
2506 FIRST_X_ASSUM_ST `chi_msb` MP_TAC;
2508 INTRO_TAC chi_msb_additive_d [`a`;`b`;`c`;`q`;`u`;`v`;`w`;`z`];
2510 DISCH_THEN SUBST1_TAC;
2511 ASM_SIMP_TAC[Real_ext.REAL_PROP_POS_RMUL];
2513 GMATCH_SIMP_TAC AFF_GT_3_1;
2514 REWRITE_TAC[IN_ELIM_THM];
2516 BY(ASM_MESON_TAC[]);
2517 BY(ASM_MESON_TAC[Planarity.notcoplanar_disjoints])
2521 let CHI_MSB_POS2 = prove_by_refinement(
2522 `!a b c d p. DISJOINT {a,b} {c} /\ d IN aff_gt {a,b} {c} ==> re_eqvl (chi_msb [a;b;d] p) (chi_msb[a;b;c] p)`,
2525 REPEAT WEAK_STRIP_TAC;
2526 FIRST_X_ASSUM MP_TAC;
2527 REWRITE_TAC[Trigonometry2.re_eqvl];
2528 ASM_SIMP_TAC[AFF_GT_2_1];
2529 REWRITE_TAC[IN_ELIM_THM];
2530 REPEAT WEAK_STRIP_TAC;
2531 EXISTS_TAC `t3:real`;
2533 ONCE_REWRITE_TAC[chi_msb_swap_23];
2534 TYPIFY `t1 % a + t2 % b + t3 % c = t1 % a + t2 % b + (&0) % p + t3 % c` (C SUBGOAL_THEN SUBST1_TAC);
2535 BY(VECTOR_ARITH_TAC);
2536 GMATCH_SIMP_TAC chi_msb_additive_d;
2537 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
2541 let MCELL_ARG_REDUCE = prove_by_refinement(
2542 `!V ul i. (?j. j <= 4 /\ mcell i V ul = mcell j V ul)`,
2545 REPEAT WEAK_STRIP_TAC;
2546 ASM_CASES_TAC `i <= 4`;
2548 BY(ASM_REWRITE_TAC[]);
2549 TYPIFY `~(i=0) /\ ~(i=1) /\ ~(i=2) /\ ~(i = 3) /\ ~(i=4)` (C SUBGOAL_THEN ASSUME_TAC);
2550 BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
2554 REWRITE_TAC[Pack_defs.mcell];
2555 BY(ASM_REWRITE_TAC[arith `~(4 =0) /\ ~(4 = 1) /\ ~(4 = 2) /\ ~(4 =3)`])
2559 let AJRIPQN_0 = prove_by_refinement(
2565 ~NULLSET (mcell i V ul INTER mcell j V vl)
2566 ==> mcell j V vl = mcell i V ul
2570 REPEAT WEAK_STRIP_TAC;
2571 INTRO_TAC MCELL_ARG_REDUCE [`V`;`ul`;`i`];
2572 INTRO_TAC MCELL_ARG_REDUCE [`V`;`vl`;`j`];
2573 REPEAT WEAK_STRIP_TAC;
2574 INTRO_TAC Ajripqn.AJRIPQN [`V`;`ul`;`vl`;`j''`;`j'`];
2577 REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
2579 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
2581 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
2582 BY(ASM_MESON_TAC[]);
2587 let CFFONNL = prove_by_refinement(
2588 `!V ul X. packing V /\ saturated V /\ leaf V ul /\ X IN mcell_set V /\
2589 {EL 0 ul,EL 1 ul} IN edgeX V X /\
2590 ~(X INTER cc_A0 ul = {}) /\ ~(X = cc_cell V ul) ==> (X = cc_cell V [EL 1 ul;EL 0 ul;EL 2 ul])`,
2593 REWRITE_TAC[cc_A0;Pack_defs.mcell_set;IN_ELIM_THM];
2594 REPEAT WEAK_STRIP_TAC;
2595 TYPIFY `~NULLSET X` (C SUBGOAL_THEN ASSUME_TAC);
2596 BY(ASM_MESON_TAC[RIJRIED;EXTENSION;NOT_IN_EMPTY]);
2597 INTRO_TAC COPLANAR_IMP_NEGLIGIBLE [`X`];
2600 TYPIFY `LENGTH ul = 3` (C SUBGOAL_THEN ASSUME_TAC);
2601 BY(ASM_MESON_TAC [leaf;Sphere.BARV;IN;arith `3 = 2 + 1`]);
2602 TYPIFY `[EL 0 ul;EL 1 ul; EL 2 ul] = ul` (C SUBGOAL_THEN ASSUME_TAC);
2603 BY(ASM_MESON_TAC[LENGTH3]);
2604 TYPIFY `{EL 0 ul,EL 1 ul, EL 2 ul} = set_of_list ul` (C SUBGOAL_THEN ASSUME_TAC);
2605 BY(ASM_MESON_TAC[set_of_list3]);
2606 INTRO_TAC AFF_GT_SUBSET_AFFINE_HULL [`{EL 0 ul, EL 1 ul}`;`{EL 2 ul}`];
2607 TYPIFY `{EL 0 ul, EL 1 ul} UNION {EL 2 ul} = {EL 0 ul,EL 1 ul, EL 2 ul}` (C SUBGOAL_THEN SUBST1_TAC);
2611 TYPIFY `?p. p IN X INTER aff_gt {EL 0 ul, EL 1 ul} {EL 2 ul}` (C SUBGOAL_THEN MP_TAC);
2612 FIRST_X_ASSUM_ST `INTER` MP_TAC;
2614 REPEAT WEAK_STRIP_TAC;
2615 TYPIFY `~(X SUBSET affine hull set_of_list ul)` (C SUBGOAL_THEN ASSUME_TAC);
2616 FIRST_X_ASSUM (SUBST1_TAC o GSYM);
2618 INTRO_TAC COPLANAR_3 [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`];
2620 ONCE_REWRITE_TAC[GSYM COPLANAR_AFFINE_HULL_COPLANAR];
2621 BY(ASM_MESON_TAC[COPLANAR_SUBSET]);
2622 COMMENT "back to 1";
2623 TYPIFY `aff_dim (set_of_list ul) = &2` (C SUBGOAL_THEN ASSUME_TAC);
2624 MATCH_MP_TAC Rogers.MHFTTZN1;
2625 BY(ASM_MESON_TAC[IN;leaf]);
2626 TYPIFY `?q. q IN X DIFF affine hull set_of_list ul` (C SUBGOAL_THEN MP_TAC);
2627 FIRST_X_ASSUM_ST `SUBSET` MP_TAC;
2629 REPEAT WEAK_STRIP_TAC;
2631 TYPIFY `~ (chi_msb ul q = &0)` (C SUBGOAL_THEN ASSUME_TAC);
2632 FIRST_X_ASSUM_ST `[]` (SUBST1_TAC o GSYM);
2633 REWRITE_TAC[GSYM CHI_MSB_COPLANAR];
2635 FIRST_X_ASSUM_ST `DIFF` MP_TAC;
2636 REWRITE_TAC[IN_DIFF];
2637 REPEAT WEAK_STRIP_TAC;
2638 FIRST_X_ASSUM MP_TAC;
2640 MATCH_MP_TAC COPLANAR_INSERT;
2642 FIRST_X_ASSUM_ST `coplanar` MP_TAC;
2643 MATCH_MP_TAC (TAUT (`a = b ==> (a ==> b)`));
2645 FIRST_X_ASSUM_ST `{}` (SUBST1_TAC o GSYM);
2647 TYPIFY `{EL 0 ul, EL 1 ul} SUBSET X` (C SUBGOAL_THEN ASSUME_TAC);
2648 MATCH_MP_TAC Marchal_cells_3.EDGEX_SUBSET_MCELL;
2649 TYPIFY `V` EXISTS_TAC;
2652 BY(ASM_MESON_TAC[IN]);
2653 REWRITE_TAC[Pack_defs.mcell_set];
2654 REWRITE_TAC[IN_ELIM_THM];
2655 BY(ASM_MESON_TAC[]);
2656 COMMENT "redo here";
2657 TYPIFY `2 <= i` (C SUBGOAL_THEN ASSUME_TAC);
2658 REWRITE_TAC[arith `2 <= i <=> ~(i <= 1)`];
2659 REPEAT WEAK_STRIP_TAC;
2660 INTRO_TAC EDGE_IMP_K2 [`V`;`ul'`;`i`];
2661 ASM_REWRITE_TAC[EXTENSION;NOT_IN_EMPTY];
2664 BY(ASM_MESON_TAC[IN]);
2665 BY(ASM_MESON_TAC[]);
2666 COMMENT "next show convex SUBSET X";
2667 TYPIFY `convex hull {EL 0 ul,EL 1 ul,p,q} SUBSET convex hull X` (C SUBGOAL_THEN ASSUME_TAC);
2668 MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET;
2669 REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
2670 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
2671 FIRST_X_ASSUM MP_TAC;
2672 TYPIFY `convex hull X = X` (C SUBGOAL_THEN SUBST1_TAC);
2673 REWRITE_TAC[CONVEX_HULL_EQ];
2675 MATCH_MP_TAC MCELL_CONVEX;
2676 BY(ASM_MESON_TAC[IN]);
2678 COMMENT "2. create Y ";
2679 ABBREV_TAC `(wl) = (if (&0 < chi_msb ul q ) then ul else [EL 1 ul; EL 0 ul; EL 2 ul])`;
2680 TYPIFY `&0 < chi_msb wl q` (C SUBGOAL_THEN ASSUME_TAC);
2683 ONCE_REWRITE_TAC[chi_msb_swap_01];
2684 MATCH_MP_TAC(arith `~(x = &0) /\ ~(&0 < x) ==> &0 < -- x`);
2685 BY(ASM_MESON_TAC[]);
2686 ABBREV_TAC `k = cc_ke V wl`;
2687 ABBREV_TAC `Y = cc_cell V (wl)`;
2688 TYPIFY `EL 2 wl = EL 2 ul` (C SUBGOAL_THEN ASSUME_TAC);
2692 BY(REWRITE_TAC[EL;HD;TL;arith `2 = SUC 1 /\ 1 = SUC 0`]);
2693 TYPIFY `set_of_list wl = set_of_list ul` (C SUBGOAL_THEN ASSUME_TAC);
2697 FIRST_X_ASSUM_ST `x = set_of_list ul` (SUBST1_TAC o GSYM);
2698 GMATCH_SIMP_TAC set_of_list3;
2699 REWRITE_TAC[LENGTH;arith `SUC (SUC(SUC 0)) = 3`];
2700 REWRITE_TAC[EL;HD;TL;arith `2 = SUC 1 /\ 1 = SUC 0`];
2702 TYPIFY `leaf V wl` (C SUBGOAL_THEN ASSUME_TAC);
2705 BY(ASM_REWRITE_TAC[]);
2706 BY(ASM_MESON_TAC[ ZASUVOR]);
2707 COMMENT "points in Y";
2708 TYPIFY `LENGTH wl = 3` (C SUBGOAL_THEN ASSUME_TAC);
2711 BY(ASM_REWRITE_TAC[]);
2712 BY(REWRITE_TAC[LENGTH;arith `SUC (SUC(SUC 0)) = 3`]);
2713 TYPIFY `{EL 0 ul,EL 1 ul, EL 2 ul} SUBSET Y` (C SUBGOAL_THEN ASSUME_TAC);
2715 GMATCH_SIMP_TAC CC_CELL34;
2716 ABBREV_TAC `pp = (if k=3 then mxi V (cc_uh V ( wl)) else EL 3 (cc_uh V wl))`;
2717 TYPIFY `pp` EXISTS_TAC;
2719 TYPIFY `set_of_list wl SUBSET {EL 0 wl, EL 1 wl, EL 2 ul, pp}` ENOUGH_TO_SHOW_TAC;
2720 BY(ASM_MESON_TAC[Ldurdpn.SUBSET_P_HULL;SUBSET_TRANS]);
2721 FIRST_X_ASSUM_ST `x = EL 2 ul` (SUBST1_TAC o GSYM);
2722 GMATCH_SIMP_TAC set_of_list3;
2724 BY(ASM_REWRITE_TAC[]);
2727 TYPIFY `EL 2 ul IN Y INTER aff_gt {EL 0 ul, EL 1 ul} {EL 2 ul}` (C SUBGOAL_THEN ASSUME_TAC);
2728 REWRITE_TAC[IN_INTER];
2730 FIRST_X_ASSUM MP_TAC;
2732 BY((MESON_TAC[Local_lemmas.X_IN_AFF_GT_X]));
2733 COMMENT "now pos half space point";
2734 TYPIFY `?q'. &0 < chi_msb wl q' /\ q' IN Y` (C SUBGOAL_THEN ASSUME_TAC);
2735 INTRO_TAC CELL_NN [`V`;`wl`];
2737 REPEAT WEAK_STRIP_TAC;
2738 ABBREV_TAC `pp = (if cc_ke V wl = 3 then mxi V (cc_uh V wl) else EL 3 (cc_uh V wl))`;
2739 INTRO_TAC CC_CELL34 [`V`;`wl`;`pp`];
2741 DISCH_THEN SUBST1_TAC;
2742 TYPIFY `pp` EXISTS_TAC;
2744 MATCH_MP_TAC HULL_INC;
2748 BY(ASM_MESON_TAC[CELL3_NONDEG]);
2749 MATCH_MP_TAC K4_CHI_MSB_POS;
2750 BY(ASM_MESON_TAC[CC_KE_34]);
2751 FIRST_X_ASSUM MP_TAC;
2753 COMMENT "now common point in the plane";
2754 INTRO_TAC GBEWYFX [`V`;`ul`];
2757 INTRO_TAC Fan.th3a [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`];
2759 BY(ASM_REWRITE_TAC[]);
2761 INTRO_TAC CONVEX_PLANE_INTER [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`p`];
2765 FIRST_X_ASSUM_ST `edgeX` MP_TAC;
2766 REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM];
2768 REPEAT (FIRST_X_ASSUM_ST `p IN x INTER y` MP_TAC);
2770 (REPEAT WEAK_STRIP_TAC);
2771 TYPIFY `{EL 0 wl,EL 1 wl} = {EL 0 ul,EL 1 ul}` (C SUBGOAL_THEN ASSUME_TAC);
2775 REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0`];
2777 TYPIFY `[EL 0 wl;EL 1 wl; EL 2 wl] = wl` (C SUBGOAL_THEN ASSUME_TAC);
2778 BY(ASM_MESON_TAC[LENGTH3]);
2779 INTRO_TAC CHI_MSB_POS2 [`EL 0 wl`;`EL 1 wl`;`EL 2 wl`;`c`;`q`];
2780 INTRO_TAC CHI_MSB_POS2 [`EL 0 wl`;`EL 1 wl`;`EL 2 wl`;`c`;`q'`];
2782 BY(ASM_REWRITE_TAC[]);
2783 REWRITE_TAC[Trigonometry2.re_eqvl];
2787 BY(ASM_REWRITE_TAC[]);
2789 INTRO_TAC CONVEX_R3_INTER [`EL 0 ul`;`EL 1 ul`;`c`;`q`;`q'`];
2791 TYPIFY `{EL 0 ul, EL 1 ul, c, q} = {EL 0 wl, EL 1 wl, c,q}` (C SUBGOAL_THEN ASSUME_TAC);
2792 FIRST_X_ASSUM_ST `{EL 0 wl, EL 1 wl} = {EL 0 ul, EL 1 ul}` MP_TAC;
2796 REWRITE_TAC[CHI_MSB_COPLANAR];
2797 MATCH_MP_TAC (arith `&0 < x ==> ~(x = &0)`);
2798 FIRST_X_ASSUM_ST `*` SUBST1_TAC;
2799 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
2800 BY(ASM_REWRITE_TAC[]);
2803 TYPIFY ` {EL 0 ul, EL 1 ul, c} = {EL 0 wl, EL 1 wl, c}` (C SUBGOAL_THEN SUBST1_TAC);
2804 FIRST_X_ASSUM_ST `{EL 0 wl, EL 1 wl} = {EL 0 ul, EL 1 ul}` MP_TAC;
2806 MATCH_MP_TAC CHI_MSB_AFF_GT_0;
2808 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
2809 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
2810 BY(ASM_REWRITE_TAC[]);
2812 (COMMENT "S. back to 1. Show u0 u1 c d in X INTER Y");
2813 TYPIFY `convex hull X = X /\ convex hull Y = Y` (C SUBGOAL_THEN ASSUME_TAC);
2814 ASM_REWRITE_TAC[CONVEX_HULL_EQ];
2816 REWRITE_TAC[cc_cell];
2817 REPEAT (GMATCH_SIMP_TAC MCELL_CONVEX);
2818 ASM_SIMP_TAC[CC_KE_34;arith `k= 3 \/ k = 4 ==> 2 <= k`];
2820 REPEAT (FIRST_X_ASSUM_ST `barV` MP_TAC);
2821 BY(REWRITE_TAC[IN]);
2822 BY(ASM_MESON_TAC[IN;cc_uh]);
2824 TYPIFY `convex hull {EL 0 ul, EL 1 ul, c, q} SUBSET convex hull X` (C SUBGOAL_THEN MP_TAC);
2825 MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET;
2826 REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
2827 FIRST_X_ASSUM_ST `convex hull {EL 0 ul, EL 1 ul, p, q} SUBSET X` MP_TAC;
2828 REPEAT (FIRST_X_ASSUM_ST `INTER` MP_TAC);
2829 REPEAT (FIRST_X_ASSUM kill);
2830 REWRITE_TAC[IN_INTER];
2831 INTRO_TAC Marchal_cells.CONVEX_HULL_SUBSET [`{EL 0 ul,EL 1 ul,p}`;`{EL 0 ul,EL 1 ul,p,q}`];
2834 REWRITE_TAC[SUBSET];
2835 TYPIFY `!y. y = EL 0 ul \/ y = EL 1 ul ==> y IN {EL 0 ul,EL 1 ul,p}` (C SUBGOAL_THEN MP_TAC);
2837 TYPIFY `q IN {EL 0 ul,EL 1 ul,p,q}` (C SUBGOAL_THEN MP_TAC);
2839 BY(MESON_TAC[HULL_INC]);
2840 FIRST_ASSUM (unlist REWRITE_TAC);
2843 TYPIFY `convex hull {EL 0 ul,EL 1 ul,c,q'} SUBSET convex hull Y` (C SUBGOAL_THEN MP_TAC);
2844 MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET;
2845 REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
2847 TYPIFY `q' IN Y` (C SUBGOAL_THEN MP_TAC);
2848 BY(ASM_REWRITE_TAC[]);
2849 FIRST_X_ASSUM_ST `{EL 0 ul, EL 1 ul, EL 2 ul} SUBSET Y` (MP_TAC o (MATCH_MP Marchal_cells.CONVEX_HULL_SUBSET));
2850 TYPIFY `{EL 0 ul, EL 1 ul, c} SUBSET convex hull {EL 0 ul, EL 1 ul, EL 2 ul}` (C SUBGOAL_THEN MP_TAC);
2851 REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `INTER` MP_TAC);
2852 REWRITE_TAC[IN_INTER;SUBSET;IN_INSERT;NOT_IN_EMPTY];
2853 TYPIFY `EL 0 ul IN {EL 0 ul,EL 1 ul,EL 2 ul} /\ EL 1 ul IN {EL 0 ul,EL 1 ul, EL 2 ul}` (C SUBGOAL_THEN MP_TAC);
2855 BY(MESON_TAC[HULL_INC]);
2856 FIRST_X_ASSUM_ST `/\` (unlist REWRITE_TAC);
2858 FIRST_X_ASSUM_ST `/\` (unlist REWRITE_TAC);
2860 COMMENT "S. now X INTER Y";
2861 TYPIFY `convex hull {EL 0 ul,EL 1 ul, c,d} SUBSET X INTER Y` (C SUBGOAL_THEN ASSUME_TAC);
2862 MATCH_MP_TAC SUBSET_TRANS;
2863 TYPIFY `convex hull {EL 0 ul, EL 1 ul, c, q} INTER convex hull {EL 0 ul, EL 1 ul, c, q'}` EXISTS_TAC;
2865 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
2866 REWRITE_TAC[SUBSET_INTER];
2868 INTRO_TAC Marchal_cells.CONVEX_HULL_SUBSET [`{EL 0 ul, EL 1 ul, c, d}`;` convex hull {EL 0 ul, EL 1 ul, c, q}`];
2869 REWRITE_TAC[HULL_HULL];
2870 DISCH_THEN MATCH_MP_TAC;
2871 TYPIFY `d IN convex hull {EL 0 ul, EL 1 ul, c, q} /\ {EL 0 ul, EL 1 ul, c} SUBSET convex hull {EL 0 ul, EL 1 ul, c, q}` ENOUGH_TO_SHOW_TAC;
2874 FIRST_X_ASSUM_ST `INTER` MP_TAC;
2876 REWRITE_TAC[SUBSET];
2877 BY(MESON_TAC[HULL_INC;MESON[IN_INSERT;NOT_IN_EMPTY] `!x. x IN {EL 0 ul,EL 1 ul,c} ==> x IN {EL 0 ul, EL 1 ul,c,q}`]);
2878 INTRO_TAC Marchal_cells.CONVEX_HULL_SUBSET [`{EL 0 ul, EL 1 ul, c, d}`;` convex hull {EL 0 ul, EL 1 ul, c, q'}`];
2879 REWRITE_TAC[HULL_HULL];
2880 DISCH_THEN MATCH_MP_TAC;
2881 TYPIFY `d IN convex hull {EL 0 ul, EL 1 ul, c, q'} /\ {EL 0 ul, EL 1 ul, c} SUBSET convex hull {EL 0 ul, EL 1 ul, c, q'}` ENOUGH_TO_SHOW_TAC;
2884 FIRST_X_ASSUM_ST `INTER` MP_TAC;
2886 REWRITE_TAC[SUBSET];
2887 BY(MESON_TAC[HULL_INC;MESON[IN_INSERT;NOT_IN_EMPTY] `!x. x IN {EL 0 ul,EL 1 ul,c} ==> x IN {EL 0 ul, EL 1 ul,c,q'}`]);
2888 COMMENT "T. back to 1. now show X = Y ";
2889 TYPIFY `X = Y` (C SUBGOAL_THEN ASSUME_TAC);
2890 INTRO_TAC AJRIPQN_0 [`V`;`ul'`;`cc_uh V wl`;`i`;`cc_ke V wl`];
2891 ASM_REWRITE_TAC[GSYM cc_cell];
2892 DISCH_THEN (MATCH_MP_TAC o GSYM);
2894 FIRST_X_ASSUM_ST `barV` MP_TAC;
2895 BY(REWRITE_TAC[IN]);
2897 BY(ASM_MESON_TAC[IN;cc_uh]);
2899 TYPIFY `NULLSET (convex hull {EL 0 ul, EL 1 ul, c, d})` (C SUBGOAL_THEN ASSUME_TAC);
2900 MATCH_MP_TAC NEGLIGIBLE_SUBSET;
2901 TYPIFY `X INTER Y` EXISTS_TAC;
2902 FIRST_X_ASSUM_ST `convex` (unlist REWRITE_TAC);
2903 FIRST_X_ASSUM MP_TAC;
2904 BY(ASM_REWRITE_TAC[]);
2905 FIRST_X_ASSUM_ST `coplanar` (MP_TAC o (MATCH_MP ZWVCBMN));
2907 MATCH_MP_TAC (arith `x = &0 ==> ~(&0 < x)`);
2908 FIRST_X_ASSUM MP_TAC;
2909 BY(MESON_TAC[volume_props]);
2910 REPEAT (FIRST_X_ASSUM_ST `convex` kill);
2911 FIRST_X_ASSUM_ST `~(X = (Y:real^3->bool))` MP_TAC;
2913 ENOUGH_TO_SHOW_TAC `cc_cell V wl = cc_cell V [EL 1 ul; EL 0 ul; EL 2 ul]`;
2914 BY(ASM_MESON_TAC[]);
2915 FIRST_X_ASSUM_ST `COND` MP_TAC;
2919 BY(ASM_MESON_TAC[]);
2924 let CC_CELL_IN_MCELL_SET = prove_by_refinement(
2925 `!V ul. saturated V /\ packing V /\ leaf V ul ==>
2926 cc_cell V ul IN mcell_set V`,
2929 REPEAT WEAK_STRIP_TAC;
2930 REWRITE_TAC[Pack_defs.mcell_set;IN_ELIM_THM];
2931 REWRITE_TAC[cc_cell];
2932 GEXISTL_TAC [`cc_ke V ul`;`cc_uh V ul`];
2934 BY(ASM_MESON_TAC[cc_uh])
2938 let CARD4_ALL_DISTINCT = prove_by_refinement(
2939 `!(a:A) b c d. CARD {a,b,c,d}= 4 ==>
2940 ~(a = b) /\ ~(a = c) /\ ~(a = d) /\ ~(b = c) /\ ~(b = d) /\ ~(c = d)`,
2943 REPEAT WEAK_STRIP_TAC;
2944 TYPIFY ` {a,b,c,d} = {a,c,b,d} /\ {a,b,c,d}= {a,d,b,c} /\ {a,b,c,d} = {b,c,a,d} /\ {a,b,c,d} = {b,d,a,c} /\ {a,b,c,d} = {c,d,a,b}` (C SUBGOAL_THEN MP_TAC);
2946 REPEAT WEAK_STRIP_TAC;
2947 BY(REPEAT CONJ_TAC THEN MATCH_MP_TAC Marchal_cells_2_new.CARD4_IMP_DISTINCT THEN FIRST_X_ASSUM_ST `4` (SUBST1_TAC o GSYM) THEN (REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC)) THEN MESON_TAC[])
2952 let LENGTH4_SET2 = prove_by_refinement(
2953 `!(a:A) b c d e f. CARD {a,b,c,d} = 4 /\ set_of_list [a;b;c;d] = set_of_list [a;b;e;f] ==>
2954 ((e = c /\ (f = d)) \/ ((e = d) /\ (f = c))) `,
2958 REWRITE_TAC[set_of_list4_explicit];
2959 REPEAT WEAK_STRIP_TAC;
2960 FIRST_X_ASSUM (MP_TAC o (MATCH_MP CARD4_ALL_DISTINCT));
2961 FIRST_X_ASSUM MP_TAC;
2962 REWRITE_TAC[EXTENSION;IN_INSERT;NOT_IN_EMPTY];
2963 REPEAT WEAK_STRIP_TAC;
2964 FIRST_ASSUM (C INTRO_TAC [`c`]);
2965 FIRST_ASSUM (C INTRO_TAC [`d`]);
2966 FIRST_ASSUM (C INTRO_TAC [`e`]);
2967 FIRST_X_ASSUM (C INTRO_TAC [`f`]);
2973 let LENGTH4_SET2_SWAP01 = prove_by_refinement(
2974 `!(a:A) b c d e f. CARD {a,b,c,d} = 4 /\ set_of_list [a;b;c;d] = set_of_list [b;a;e;f] ==>
2975 ((e = c /\ (f = d)) \/ ((e = d) /\ (f = c))) `,
2979 REWRITE_TAC[set_of_list4_explicit];
2980 REPEAT WEAK_STRIP_TAC;
2981 FIRST_X_ASSUM (MP_TAC o (MATCH_MP CARD4_ALL_DISTINCT));
2982 FIRST_X_ASSUM MP_TAC;
2983 REWRITE_TAC[EXTENSION;IN_INSERT;NOT_IN_EMPTY];
2984 REPEAT WEAK_STRIP_TAC;
2985 FIRST_ASSUM (C INTRO_TAC [`c`]);
2986 FIRST_ASSUM (C INTRO_TAC [`d`]);
2987 FIRST_ASSUM (C INTRO_TAC [`e`]);
2988 FIRST_X_ASSUM (C INTRO_TAC [`f`]);
2994 let CC_CELL_NOT_COPLANAR = prove_by_refinement(
2995 `!V ul. packing V /\
2997 leaf V ul ==> ~coplanar (cc_cell V ul)`,
3000 REWRITE_TAC[cc_cell];
3001 REWRITE_TAC[Pack_defs.mcell];
3002 REPEAT WEAK_STRIP_TAC;
3003 FIRST_X_ASSUM MP_TAC;
3004 INTRO_TAC CC_KE_34 [`V`;`ul`];
3006 ABBREV_TAC `k = cc_ke V ul`;
3007 TYPIFY `~(k=0) /\ ~(k=1) /\ ~(k=2)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
3008 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
3009 FIRST_X_ASSUM_ST `\/` DISJ_CASES_TAC;
3011 MATCH_MP_TAC MCELL3_NONPLANAR;
3014 BY(ASM_MESON_TAC[cc_uh;IN]);
3015 FIRST_X_ASSUM_ST `cc_ke` MP_TAC;
3018 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
3019 BY(ASM_MESON_TAC[cc_uh;leaf;IN;arith `~(x < sqrt2) ==> sqrt2 <= x`]);
3020 ASM_REWRITE_TAC[arith `~(4=3)`];
3021 MATCH_MP_TAC MCELL4_NONPLANAR;
3023 FIRST_X_ASSUM_ST `cc_ke` MP_TAC;
3026 BY(ASM_MESON_TAC[REWRITE_RULE[IN] cc_uh]);
3027 BY(ASM_REWRITE_TAC[arith `~(3=4)`])
3031 let CC_CELL_NOT_COPLANAR_EXTREME = prove_by_refinement(
3032 `!V ul pp. packing V /\
3035 ((if cc_ke V ul = 3 then mxi V (cc_uh V ul) else EL 3 (cc_uh V ul)) =
3036 pp) ==> ~coplanar {EL 0 ul, EL 1 ul, EL 2 ul,pp}`,
3039 ONCE_REWRITE_TAC[GSYM COPLANAR_AFFINE_HULL_COPLANAR];
3040 REPEAT WEAK_STRIP_TAC;
3041 TYPIFY `coplanar (convex hull {EL 0 ul, EL 1 ul, EL 2 ul, pp})` (C SUBGOAL_THEN ASSUME_TAC);
3042 BY(ASM_MESON_TAC[COPLANAR_SUBSET;CONVEX_HULL_SUBSET_AFFINE_HULL]);
3043 INTRO_TAC CC_CELL34 [`V`;`ul`;`pp`];
3046 BY(ASM_MESON_TAC[CC_CELL_NOT_COPLANAR])
3050 let CC_CELL_NOT_NULLSET = prove_by_refinement(
3051 `!V ul. packing V /\ saturated V /\ leaf V ul ==>
3052 ~NULLSET (cc_cell V ul)`,
3055 REPEAT WEAK_STRIP_TAC;
3056 TYPIFY `vol(cc_cell V ul) = &0` (C SUBGOAL_THEN ASSUME_TAC);
3057 BY(ASM_MESON_TAC[volume_props]);
3058 ABBREV_TAC `(p:real^3) = (if cc_ke V ul = 3 then mxi V (cc_uh V ul) else EL 3 (cc_uh V ul))`;
3059 INTRO_TAC CC_CELL34 [`V`;`ul`;`p`];
3062 INTRO_TAC ZWVCBMN [`EL 0 ul`;` EL 1 ul`;` EL 2 ul`;` p`];
3064 MATCH_MP_TAC CC_CELL_NOT_COPLANAR_EXTREME;
3065 BY(ASM_MESON_TAC[]);
3066 FIRST_X_ASSUM (SUBST1_TAC o GSYM);
3067 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
3071 let CC_CELL_EXTREME_CARD = prove_by_refinement(
3072 `!V ul pp. packing V /\
3075 ((if cc_ke V ul = 3 then mxi V (cc_uh V ul) else EL 3 (cc_uh V ul)) =
3076 pp) ==> CARD {EL 0 ul, EL 1 ul, EL 2 ul,pp} = 4`,
3079 REPEAT WEAK_STRIP_TAC;
3080 MATCH_MP_TAC Collect_geom2.NOT_COPLANAR_IMP_CARD4;
3081 GMATCH_SIMP_TAC (GSYM coplanar_eq_coplanar_alt);
3082 REWRITE_TAC[DIMINDEX_3;arith `2 <= 3`];
3083 MATCH_MP_TAC CC_CELL_NOT_COPLANAR_EXTREME;
3088 let CC_CELL_INDEPENDENT = prove_by_refinement(
3089 `!V ul pp. packing V /\
3092 (if cc_ke V ul = 3 then mxi V (cc_uh V ul) else EL 3 (cc_uh V ul)) =
3093 pp ==> ~affine_dependent {EL 0 ul, EL 1 ul, EL 2 ul,pp}`,
3096 REPEAT WEAK_STRIP_TAC;
3097 FIRST_X_ASSUM MP_TAC;
3098 REWRITE_TAC[AFFINE_INDEPENDENT_IFF_CARD];
3099 GMATCH_SIMP_TAC CC_CELL_EXTREME_CARD;
3101 TYPIFY `V` EXISTS_TAC;
3102 BY(ASM_REWRITE_TAC[]);
3104 BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]);
3105 REWRITE_TAC[INT_ARITH `&4 - (int_of_num) 1 = &3`];
3106 REWRITE_TAC[INT_ARITH `x = int_of_num 3 <=> x <= &3 /\ ~(x <= &2)`];
3108 INTRO_TAC AFF_DIM_LE_UNIV [`{EL 0 ul, EL 1 ul, EL 2 ul, pp}`];
3109 BY(REWRITE_TAC[DIMINDEX_3]);
3110 DISCH_THEN (MP_TAC o (MATCH_MP Rogers.AFF_DIM_LE_2_IMP_COPLANAR));
3112 MATCH_MP_TAC CC_CELL_NOT_COPLANAR_EXTREME;
3113 TYPIFY `V` EXISTS_TAC;
3114 BY(ASM_REWRITE_TAC[])
3118 let CC_CELL_CONVEX_HULL_INJ = prove_by_refinement(
3119 `!V ul vl pu pv. packing V /\ saturated V /\ leaf V ul /\ leaf V vl /\
3120 (if cc_ke V ul = 3 then mxi V (cc_uh V ul) else EL 3 (cc_uh V ul)) = pu /\
3121 (if cc_ke V vl = 3 then mxi V (cc_uh V vl) else EL 3 (cc_uh V vl)) = pv /\
3122 cc_cell V ul = cc_cell V vl ==>
3123 {EL 0 ul, EL 1 ul, EL 2 ul, pu} = {EL 0 vl,EL 1 vl, EL 2 vl, pv}
3127 REPEAT WEAK_STRIP_TAC;
3128 INTRO_TAC Packing3.CONVEX_HULL_EQ_EQ_SET_EQ [` {EL 0 ul, EL 1 ul, EL 2 ul, pu}`;`{EL 0 vl,EL 1 vl, EL 2 vl, pv}`];
3130 BY(CONJ_TAC THEN MATCH_MP_TAC CC_CELL_INDEPENDENT THEN TYPIFY `V` EXISTS_TAC THEN ASM_REWRITE_TAC[]);
3131 DISCH_THEN (unlist REWRITE_TAC o SYM);
3132 FIRST_X_ASSUM MP_TAC;
3133 REPEAT (GMATCH_SIMP_TAC CC_CELL34);
3134 TYPIFY `pv` EXISTS_TAC;
3136 TYPIFY `pu` EXISTS_TAC;
3137 BY(ASM_REWRITE_TAC[])
3141 let FUEIMOV_K = prove_by_refinement(
3142 `!V ul vl. saturated V /\ packing V /\ leaf V ul /\ leaf V vl /\
3143 cc_cell V ul = cc_cell V vl ==> (cc_ke V ul = cc_ke V vl)`,
3146 REWRITE_TAC[cc_cell];
3147 REPEAT WEAK_STRIP_TAC;
3148 INTRO_TAC Ajripqn.AJRIPQN [`V`;`(cc_uh V ul)`;`(cc_uh V vl)`;`(cc_ke V ul)`;`(cc_ke V vl)`];
3149 ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
3150 DISCH_THEN MATCH_MP_TAC;
3151 TYPIFY `barV V 3 (cc_uh V ul) /\ barV V 3 (cc_uh V vl)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
3152 BY(ASM_MESON_TAC[REWRITE_RULE[IN] cc_uh]);
3153 ASM_SIMP_TAC[CC_KE_34];
3154 REWRITE_TAC[INTER_IDEMPOT];
3155 BY(ASM_MESON_TAC[ CC_CELL_NOT_NULLSET;cc_cell])
3159 let LIST_OF_CC_UH = prove_by_refinement(
3160 `!V ul. saturated V /\ packing V /\ leaf V ul ==>
3161 (cc_uh V ul) = [EL 0 ul; EL 1 ul; EL 2 ul; EL 3 (cc_uh V ul)]`,
3164 REPEAT WEAK_STRIP_TAC;
3165 TYPIFY `LENGTH (cc_uh V ul) = 4` (C SUBGOAL_THEN ASSUME_TAC);
3166 BY(ASM_MESON_TAC[cc_uh;IN;Sphere.BARV;arith `3 + 1 = 4`]);
3167 GMATCH_SIMP_TAC LENGTH4;
3169 ASM_SIMP_TAC[EL_CC_UH];
3170 BY(SIMP_TAC[EL;HD;TL;arith `3 = SUC 2 /\ 2 = SUC 1 /\ 1 = SUC 0`])
3174 let SET_OF_LIST_CC_UH = prove_by_refinement(
3175 `!V ul. saturated V /\ packing V /\ leaf V ul ==>
3176 set_of_list (cc_uh V ul) = {EL 0 ul, EL 1 ul, EL 2 ul, EL 3 (cc_uh V ul)}`,
3179 REPEAT WEAK_STRIP_TAC;
3180 TYPIFY `LENGTH (cc_uh V ul) = 4` (C SUBGOAL_THEN ASSUME_TAC);
3181 BY(ASM_MESON_TAC[cc_uh;IN;Sphere.BARV;arith `3 + 1 = 4`]);
3182 GMATCH_SIMP_TAC set_of_list4;
3184 BY(ASM_SIMP_TAC[EL_CC_UH])
3188 let MCELL4_EXTREME_POINT = prove_by_refinement(
3189 `!V ul vl. saturated V /\ packing V /\ leaf V ul /\ leaf V vl /\
3190 cc_cell V ul = cc_cell V vl /\ (cc_ke V ul = 4) ==> set_of_list (cc_uh V ul) = set_of_list (cc_uh V vl)`,
3193 REPEAT WEAK_STRIP_TAC;
3194 TYPIFY `cc_ke V vl = 4` (C SUBGOAL_THEN ASSUME_TAC);
3195 BY(ASM_MESON_TAC[FUEIMOV_K]);
3196 ASM_SIMP_TAC[SET_OF_LIST_CC_UH];
3197 INTRO_TAC CC_CELL_CONVEX_HULL_INJ[`V`;`ul`;`vl`;`EL 3 (cc_uh V ul)`;`EL 3 (cc_uh V vl)`];
3198 BY(ASM_SIMP_TAC [arith `k = 4 ==> ~(k = 3)`])
3202 let STEM_OF_LEAF = prove_by_refinement(
3203 `!V ul. leaf V ul ==>
3204 stem ul = {EL 0 ul, EL 1 ul}`,
3207 REWRITE_TAC[stem;leaf;IN;Sphere.BARV;arith `2 + 1 = 3`];
3208 REPEAT WEAK_STRIP_TAC;
3209 GMATCH_SIMP_TAC set_of_list2;
3211 REWRITE_TAC[arith `2 = 1 + 1`];
3212 MATCH_MP_TAC Packing3.LENGTH_TRUNCATE_SIMPLEX;
3213 BY(ASM_REWRITE_TAC[arith `1 + 1 <= 3`]);
3215 BY(ASM_MESON_TAC[arith `1+1<= 3 /\ 0 <= 1 /\ 1 <= 1`;Packing3.EL_TRUNCATE_SIMPLEX])
3219 let FUEIMOV_4 = prove_by_refinement(
3220 `!V ul vl. saturated V /\ packing V /\ leaf V ul /\ leaf V vl /\
3221 cc_cell V ul = cc_cell V vl /\ (stem ul = stem vl) /\ (cc_ke V ul = 4) /\ ~(ul = vl) ==>
3222 cc_uh V vl = [EL 1 ul;EL 0 ul;EL 3 (cc_uh V ul);EL 2 ul]`,
3225 REPEAT WEAK_STRIP_TAC;
3226 TYPIFY `cc_ke V vl = 4` (C SUBGOAL_THEN ASSUME_TAC);
3227 BY(ASM_MESON_TAC[FUEIMOV_K]);
3228 INTRO_TAC MCELL4_EXTREME_POINT [`V`;`ul`;`vl`];
3230 REPEAT (GMATCH_SIMP_TAC SET_OF_LIST_CC_UH);
3232 FIRST_X_ASSUM_ST `stem` MP_TAC;
3233 REPEAT (GMATCH_SIMP_TAC STEM_OF_LEAF);
3235 BY(ASM_MESON_TAC[]);
3237 BY(ASM_MESON_TAC[]);
3239 TYPIFY `(EL 0 vl = EL 0 ul /\ EL 1 vl = EL 1 ul) \/ (EL 0 vl = EL 1 ul /\ EL 1 vl = EL 0 ul)` (C SUBGOAL_THEN ASSUME_TAC);
3240 FIRST_X_ASSUM MP_TAC;
3242 INTRO_TAC K4_CHI_MSB_POS [`V`;`ul`];
3245 INTRO_TAC K4_CHI_MSB_POS [`V`;`vl`];
3248 TYPIFY ` [EL 0 ul; EL 1 ul; EL 2 ul] = ul /\ [EL 0 vl; EL 1 vl; EL 2 vl] = vl` (C SUBGOAL_THEN ASSUME_TAC);
3249 BY(ASM_MESON_TAC[LENGTH3;leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
3250 FIRST_X_ASSUM_ST `\/` DISJ_CASES_TAC;
3253 INTRO_TAC LENGTH4_SET2 [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`EL 3 (cc_uh V ul)`;`EL 2 vl`;`EL 3 (cc_uh V vl)`];
3255 INTRO_TAC CC_CELL_EXTREME_CARD[`V`;`ul`;`EL 3(cc_uh V ul)`];
3256 ASM_REWRITE_TAC[arith `~(4=3)`];
3257 DISCH_THEN (SUBST1_TAC);
3258 BY(ASM_REWRITE_TAC[set_of_list4_explicit]);
3259 DISCH_THEN DISJ_CASES_TAC;
3260 BY(ASM_MESON_TAC[]);
3261 REPEAT (FIRST_X_ASSUM_ST `/\` MP_TAC) THEN REPEAT WEAK_STRIP_TAC;
3263 REPEAT (FIRST_X_ASSUM_ST `chi_msb` MP_TAC);
3264 ABBREV_TAC `c = cc_uh V ul`;
3265 ABBREV_TAC `d = cc_uh V vl`;
3268 REPEAT (FIRST_X_ASSUM_ST `CONS x y = z` kill);
3271 ONCE_REWRITE_TAC[chi_msb_swap_23];
3272 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
3273 COMMENT "second branch";
3276 INTRO_TAC LENGTH4_SET2_SWAP01 [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`EL 3 (cc_uh V ul)`;`EL 2 vl`;`EL 3 (cc_uh V vl)`];
3278 INTRO_TAC CC_CELL_EXTREME_CARD[`V`;`ul`;`EL 3(cc_uh V ul)`];
3279 ASM_REWRITE_TAC[arith `~(4=3)`];
3280 DISCH_THEN (SUBST1_TAC);
3281 BY(ASM_REWRITE_TAC[set_of_list4_explicit]);
3282 DISCH_THEN DISJ_CASES_TAC;
3283 REPEAT (FIRST_X_ASSUM_ST `/\` MP_TAC) THEN REPEAT WEAK_STRIP_TAC;
3285 REPEAT (FIRST_X_ASSUM_ST `chi_msb` MP_TAC);
3286 ABBREV_TAC `c = cc_uh V ul`;
3287 ABBREV_TAC `d = cc_uh V vl`;
3290 REPEAT (FIRST_X_ASSUM_ST `CONS x y = z` kill);
3293 ONCE_REWRITE_TAC[chi_msb_swap_01];
3294 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
3295 INTRO_TAC LIST_OF_CC_UH [`V`;`vl`];
3297 BY(ASM_REWRITE_TAC[]);
3298 DISCH_THEN SUBST1_TAC;
3303 let MXI_NOT_IN_V = prove_by_refinement(
3304 `!V ul. saturated V /\ packing V /\ leaf V ul /\ (cc_ke V ul = 3) ==>
3305 ~(mxi V (cc_uh V ul) IN V)`,
3308 REPEAT WEAK_STRIP_TAC;
3309 INTRO_TAC MXI_IN_VORONOI_LIST [`V`;`(cc_uh V ul)`];
3313 BY(ASM_MESON_TAC[cc_uh;IN]);
3314 FIRST_X_ASSUM_ST `cc_ke` MP_TAC;
3317 BY(REWRITE_TAC[arith `~(4=3)`]);
3318 ASM_SIMP_TAC[arith `~(x < y) ==> (y <= x)`];
3319 BY(ASM_MESON_TAC[cc_uh;leaf]);
3320 REPEAT WEAK_STRIP_TAC;
3321 TYPIFY `EL 0 (cc_uh V ul) = EL 0 ul` (C SUBGOAL_THEN ASSUME_TAC);
3322 BY(ASM_MESON_TAC[EL_CC_UH]);
3323 TYPIFY `EL 0 (cc_uh V ul) IN V` (C SUBGOAL_THEN ASSUME_TAC);
3324 ASM_REWRITE_TAC[EL];
3325 INTRO_TAC Packing3.BARV_SUBSET [`V`;`2`;`ul`];
3327 BY(ASM_MESON_TAC[leaf;IN]);
3328 INTRO_TAC Packing3.BARV_IMP_HD_IN_SET_OF_LIST [`V`;`2`;`ul`];
3330 BY(ASM_MESON_TAC[leaf;IN]);
3331 BY(ASM_MESON_TAC[Packing3.IN_TRANS]);
3332 TYPIFY `&0 < sqrt2 /\ sqrt2 < sqrt(&4)` (C SUBGOAL_THEN MP_TAC);
3333 REWRITE_TAC[Sphere.sqrt2];
3334 GMATCH_SIMP_TAC REAL_LT_RSQRT;
3337 GMATCH_SIMP_TAC REAL_LT_RSQRT;
3338 GMATCH_SIMP_TAC SQRT_POW_2;
3340 REWRITE_TAC[Collect_geom2.SQRT4_EQ2];
3341 REPEAT WEAK_STRIP_TAC;
3342 FIRST_X_ASSUM_ST `packing` MP_TAC;
3343 REWRITE_TAC[Sphere.packing;NOT_FORALL_THM];
3344 GEXISTL_TAC [`EL 0 (cc_uh V ul)`;`mxi V (cc_uh V ul)`];
3346 ASM_SIMP_TAC[arith `x < y ==> ~(y <= x)`];
3348 BY(ASM_MESON_TAC[IN]);
3350 BY(ASM_MESON_TAC[IN]);
3352 FIRST_X_ASSUM_ST `dist` MP_TAC;
3353 ASM_REWRITE_TAC[DIST_REFL];
3354 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
3358 let MCELL_V_INTER_EXTREME = prove_by_refinement(
3360 saturated V /\ packing V /\ leaf V ul /\ (cc_ke V ul = 3)
3362 V INTER {EL 0 ul,EL 1 ul, EL 2 ul,mxi V (cc_uh V ul)} = set_of_list ul`,
3365 REPEAT WEAK_STRIP_TAC;
3366 TYPIFY `LENGTH ul = 3` (C SUBGOAL_THEN ASSUME_TAC);
3367 BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
3368 MATCH_MP_TAC SUBSET_ANTISYM;
3370 REWRITE_TAC[SUBSET_INTER];
3372 MATCH_MP_TAC Packing3.BARV_SUBSET;
3374 BY(ASM_MESON_TAC[leaf;IN]);
3375 GMATCH_SIMP_TAC set_of_list3;
3378 GMATCH_SIMP_TAC set_of_list3;
3380 INTRO_TAC MXI_NOT_IN_V [`V`;`ul`];
3386 let MCELL_EXTREME_DIFF_V = prove_by_refinement(
3388 saturated V /\ packing V /\ leaf V ul /\ (cc_ke V ul = 3)
3390 {EL 0 ul,EL 1 ul, EL 2 ul,mxi V (cc_uh V ul)} DIFF V = {mxi V (cc_uh V ul)}`,
3393 REPEAT WEAK_STRIP_TAC;
3394 TYPIFY `LENGTH ul = 3` (C SUBGOAL_THEN ASSUME_TAC);
3395 BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
3396 MATCH_MP_TAC SUBSET_ANTISYM;
3398 INTRO_TAC MXI_NOT_IN_V [`V`;`ul`];
3401 INTRO_TAC MCELL_V_INTER_EXTREME [`V`;`ul`];
3403 GMATCH_SIMP_TAC set_of_list3;
3409 let FUEIMOV_3 = prove_by_refinement(
3410 `!V ul vl. saturated V /\ packing V /\ leaf V ul /\ leaf V vl /\ (cc_ke V ul = 3) /\
3411 {EL 0 ul,EL 1 ul} = {EL 0 vl,EL 1 vl} /\ cc_cell V ul = cc_cell V vl ==> (ul = vl)`,
3414 REPEAT WEAK_STRIP_TAC;
3415 TYPIFY `LENGTH ul = 3 /\ LENGTH vl = 3` (C SUBGOAL_THEN MP_TAC);
3416 BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
3417 REPEAT WEAK_STRIP_TAC;
3418 TYPIFY `cc_ke V vl = 3` (C SUBGOAL_THEN ASSUME_TAC);
3419 INTRO_TAC CC_KE_34 [`V`;`vl`];
3420 DISCH_THEN DISJ_CASES_TAC;
3421 BY(ASM_REWRITE_TAC[]);
3422 INTRO_TAC FUEIMOV_K [`V`;`vl`;`ul`];
3423 BY(ASM_REWRITE_TAC[]);
3424 INTRO_TAC CC_CELL_CONVEX_HULL_INJ [`V`;`ul`;`vl`;`mxi V (cc_uh V ul)`;`mxi V (cc_uh V vl)`];
3427 TYPIFY `mxi V (cc_uh V ul) = mxi V (cc_uh V vl)` (C SUBGOAL_THEN ASSUME_TAC);
3428 INTRO_TAC MCELL_EXTREME_DIFF_V [`V`;`ul`];
3429 INTRO_TAC MCELL_EXTREME_DIFF_V [`V`;`vl`];
3430 FIRST_X_ASSUM MP_TAC;
3433 TYPIFY `{EL 0 ul, EL 1 ul, EL 2 ul} = {EL 0 vl, EL 1 vl, EL 2 vl}` (C SUBGOAL_THEN ASSUME_TAC);
3434 INTRO_TAC MCELL_V_INTER_EXTREME [`V`;`ul`];
3435 INTRO_TAC MCELL_V_INTER_EXTREME [`V`;`vl`];
3437 REPEAT (GMATCH_SIMP_TAC set_of_list3);
3439 BY(ASM_REWRITE_TAC[]);
3441 BY(ASM_REWRITE_TAC[]);
3442 FIRST_X_ASSUM_ST `EL` MP_TAC;
3444 TYPIFY `~(EL 0 ul = EL 1 ul)` (C SUBGOAL_THEN ASSUME_TAC);
3445 MATCH_MP_TAC Marchal_cells_2_new.CARD4_IMP_DISTINCT;
3446 GEXISTL_TAC [`EL 2 ul`;`mxi V (cc_uh V ul)`];
3447 MATCH_MP_TAC CC_CELL_EXTREME_CARD;
3448 TYPIFY `V` EXISTS_TAC;
3449 BY(ASM_REWRITE_TAC[]);
3450 TYPIFY `~(EL 1 ul = EL 2 ul)` (C SUBGOAL_THEN ASSUME_TAC);
3451 MATCH_MP_TAC Marchal_cells_2_new.CARD4_IMP_DISTINCT;
3452 GEXISTL_TAC [`EL 0 ul`;`mxi V (cc_uh V ul)`];
3453 TYPIFY `{EL 1 ul, EL 2 ul, EL 0 ul, mxi V (cc_uh V ul)} = {EL 0 ul, EL 1 ul, EL 2 ul, mxi V (cc_uh V ul)}` (C SUBGOAL_THEN SUBST1_TAC);
3455 MATCH_MP_TAC CC_CELL_EXTREME_CARD;
3456 TYPIFY `V` EXISTS_TAC;
3457 BY(ASM_REWRITE_TAC[]);
3458 TYPIFY `~(EL 0 ul = EL 2 ul)` (C SUBGOAL_THEN ASSUME_TAC);
3459 MATCH_MP_TAC Marchal_cells_2_new.CARD4_IMP_DISTINCT;
3460 GEXISTL_TAC [`EL 1 ul`;`mxi V (cc_uh V ul)`];
3461 TYPIFY `{EL 0 ul, EL 2 ul, EL 1 ul, mxi V (cc_uh V ul)} = {EL 0 ul, EL 1 ul, EL 2 ul, mxi V (cc_uh V ul)}` (C SUBGOAL_THEN SUBST1_TAC);
3463 MATCH_MP_TAC CC_CELL_EXTREME_CARD;
3464 TYPIFY `V` EXISTS_TAC;
3465 BY(ASM_REWRITE_TAC[]);
3466 TYPIFY `((EL 0 vl = EL 0 ul) /\ (EL 1 vl = EL 1 ul)) \/ ((EL 0 vl = EL 1 ul) /\ (EL 1 vl = EL 0 ul))` (C SUBGOAL_THEN ASSUME_TAC);
3467 FIRST_X_ASSUM_ST `{a,b}={c,d}` MP_TAC;
3468 REWRITE_TAC[Collect_geom.PAIR_EQ_EXPAND];
3469 DISCH_THEN DISJ_CASES_TAC;
3470 BY(ASM_REWRITE_TAC[]);
3471 BY(ASM_REWRITE_TAC[]);
3472 COMMENT "1. next match EL 2";
3473 TYPIFY `EL 2 vl = EL 2 ul` (C SUBGOAL_THEN ASSUME_TAC);
3474 (FIRST_X_ASSUM_ST `x INSERT y = x' INSERT y'` MP_TAC);
3475 REWRITE_TAC[EXTENSION;IN_INSERT;NOT_IN_EMPTY];
3477 FIRST_ASSUM (C INTRO_TAC [`EL 0 ul`]);
3478 FIRST_ASSUM (C INTRO_TAC [`EL 1 ul`]);
3479 FIRST_X_ASSUM (C INTRO_TAC [`EL 2 ul`]);
3480 REPEAT (FIRST_X_ASSUM_ST `~` MP_TAC);
3482 FIRST_X_ASSUM DISJ_CASES_TAC;
3487 COMMENT "1. now use chi_msb to eliminate the second case";
3488 FIRST_X_ASSUM DISJ_CASES_TAC;
3489 ONCE_REWRITE_TAC[EQ_SYM_EQ];
3490 GMATCH_SIMP_TAC LENGTH3;
3492 BY(ASM_MESON_TAC[LENGTH3]);
3493 INTRO_TAC CELL3_NONDEG [`V`;`ul`];
3495 INTRO_TAC CELL3_NONDEG [`V`;`vl`];
3497 REPEAT WEAK_STRIP_TAC;
3498 ABBREV_TAC `xi = mxi V (cc_uh V vl)`;
3499 TYPIFY `chi_msb vl xi = chi_msb [EL 1 ul;EL 0 ul;EL 2 ul] xi` (C SUBGOAL_THEN MP_TAC);
3500 REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
3501 REPEAT (FIRST_X_ASSUM (MP_TAC o (MATCH_MP LENGTH3)));
3503 DISCH_THEN SUBST1_TAC;
3504 BY(ASM_REWRITE_TAC[]);
3505 ONCE_REWRITE_TAC[chi_msb_swap_01];
3506 REPEAT (FIRST_X_ASSUM (MP_TAC o (MATCH_MP LENGTH3)));
3507 DISCH_THEN (SUBST1_TAC o GSYM);
3508 REPEAT (FIRST_X_ASSUM_ST `chi_msb` MP_TAC);
3513 let TWO_REARRANGEMENT_LEMMA_ALT = prove_by_refinement(
3515 packing V /\ saturated V /\ barV V 3 ul /\ ul = [u0;u1;u2;u3] ==>
3516 (?p. p permutes 0..1 /\ [u1;u0;u2;u3] = left_action_list p ul)`,
3519 BY(MESON_TAC[Qzksykg.TWO_REARRANGEMENT_LEMMA])
3523 let MCELL2_EDGE_FIRST = prove_by_refinement(
3524 `!V ul u v. saturated V /\ packing V /\ ul IN barV V 3 /\
3525 {u,v} IN edgeX V (mcell2 V ul) ==>
3526 (?vl. vl IN barV V 3 /\ u = EL 0 vl /\ v = EL 1 vl /\ mcell2 V ul = mcell2 V vl)`,
3529 REPEAT WEAK_STRIP_TAC;
3530 TYPIFY `barV V 3 ul` (C SUBGOAL_THEN ASSUME_TAC);
3531 BY(ASM_MESON_TAC[IN]);
3532 INTRO_TAC MCELL2_EDGE [`V`;`ul`;`{u,v}`];
3534 BY(ASM_MESON_TAC[IN]);
3535 REWRITE_TAC[Geomdetail.PAIR_EQ_EXPAND];
3536 REPEAT WEAK_STRIP_TAC;
3537 TYPIFY `ul` EXISTS_TAC;
3538 BY(ASM_REWRITE_TAC[]);
3539 COMMENT "second case";
3540 INTRO_TAC TWO_REARRANGEMENT_LEMMA_ALT [`V`;`ul`;`v`;`u`;`EL 2 ul`;`EL 3 ul`];
3543 MATCH_MP_TAC LENGTH4;
3544 BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3 + 1 = 4`]);
3545 REPEAT WEAK_STRIP_TAC;
3546 INTRO_TAC Rvfxzbu.RVFXZBU [`V`;`ul`;`2`;`p`];
3548 BY(ASM_REWRITE_TAC[IN_INSERT;arith `2 -1 = 1`]);
3550 INTRO_TAC Qzksykg.QZKSYKG1 [`V`;`ul`;`left_action_list p ul`;`2`;`p`];
3552 ASM_REWRITE_TAC[IN_INSERT;arith `2 - 1 = 1`];
3554 BY(ASM_MESON_TAC[NOT_IN_EMPTY; RIJRIED;MCELL2;NEGLIGIBLE_EMPTY]);
3556 TYPIFY `left_action_list p ul` EXISTS_TAC;
3557 ASM_REWRITE_TAC[IN;MCELL2];
3558 FIRST_X_ASSUM_ST `EL 3` (SUBST1_TAC o SYM);
3559 REPEAT (FIRST_X_ASSUM_ST `EL` MP_TAC);
3560 REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0`];
3565 let FINITE_CARD1_IMP_SINGLETON = prove_by_refinement(
3566 `!(S:A->bool). FINITE S /\ CARD S = 1 ==> (?x. S = {x})`,
3569 ASM_MESON_TAC[ Local_lemmas.FINITE_CARD1_IMP_SINGLETON]
3573 let SET2_INSERT1 = prove_by_refinement(
3574 `!(a:A) b x y z. {a,b} SUBSET {x,y,z} /\ ~(a = b) ==> (?c. {a,b,c} = {x,y,z})`,
3577 REPEAT WEAK_STRIP_TAC;
3578 TYPIFY `FINITE ({x, y, z} DIFF {a, b})` (C SUBGOAL_THEN ASSUME_TAC);
3579 MATCH_MP_TAC FINITE_DIFF;
3580 BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]);
3581 TYPIFY `CARD {x,y,z} <= 3` (C SUBGOAL_THEN ASSUME_TAC);
3582 BY(MESON_TAC[Geomdetail.CARD3]);
3583 INTRO_TAC Hypermap.LEMMA_CARD_DIFF [`{x,y,z}`;`{a,b}`];
3584 ASM_REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY];
3585 TYPIFY `CARD {a,b} = 2` (C SUBGOAL_THEN SUBST1_TAC);
3586 BY(ASM_REWRITE_TAC[Geomdetail.CARD_SET2]);
3588 TYPIFY `CARD ({x,y,z} DIFF {a,b}) = 0 \/ CARD({x,y,z} DIFF {a,b}) = 1` (C SUBGOAL_THEN MP_TAC);
3589 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
3590 REPEAT WEAK_STRIP_TAC;
3591 INTRO_TAC CARD_EQ_0 [`{x, y, z} DIFF {a, b}`];
3593 REPEAT WEAK_STRIP_TAC;
3594 TYPIFY `a` EXISTS_TAC;
3595 FIRST_X_ASSUM MP_TAC;
3596 FIRST_X_ASSUM_ST `SUBSET` MP_TAC;
3598 INTRO_TAC FINITE_CARD1_IMP_SINGLETON [`{x, y, z} DIFF {a, b}`];
3600 REPEAT WEAK_STRIP_TAC;
3601 TYPIFY `x'` EXISTS_TAC;
3602 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[])
3606 let MCELL3_EDGE_FIRST = prove_by_refinement(
3607 `!V ul u v. saturated V /\ packing V /\ ul IN barV V 3 /\
3608 {u,v} IN edgeX V (mcell3 V ul) ==>
3609 (?vl. vl IN barV V 3 /\ u = EL 0 vl /\ v = EL 1 vl /\ mcell3 V ul = mcell3 V vl)`,
3612 REPEAT WEAK_STRIP_TAC;
3613 TYPIFY `barV V 3 ul` (C SUBGOAL_THEN ASSUME_TAC);
3614 BY(ASM_MESON_TAC[IN]);
3615 TYPIFY `~NULLSET(mcell3 V ul)` (C SUBGOAL_THEN ASSUME_TAC);
3616 BY(ASM_MESON_TAC[NOT_IN_EMPTY; RIJRIED;MCELL3;NEGLIGIBLE_EMPTY]);
3617 INTRO_TAC MCELL3_EDGE [`V`;`ul`;`u`;`v`];
3619 BY(ASM_MESON_TAC[IN]);
3621 REPEAT WEAK_STRIP_TAC;
3622 INTRO_TAC SET_OF_LIST_TRUNCATE_2 [`ul`];
3624 BY(ASM_MESON_TAC[arith `3 <= 3 + 1`;IN;Sphere.BARV]);
3626 INTRO_TAC SET2_INSERT1 [`u`;`v`;`EL 0 ul`;`EL 1 ul`;`EL 2 ul`];
3628 BY(ASM_MESON_TAC[]);
3629 REPEAT WEAK_STRIP_TAC;
3630 TYPIFY `{EL 0 ul, EL 1 ul, EL 2 ul, EL 3 ul} = set_of_list ul` (C SUBGOAL_THEN ASSUME_TAC);
3631 ONCE_REWRITE_TAC[EQ_SYM_EQ];
3632 MATCH_MP_TAC set_of_list4;
3633 BY(ASM_MESON_TAC[arith `3+1 = 4`;IN;Sphere.BARV]);
3634 INTRO_TAC Marchal_cells_3.LEFT_ACTION_LIST_2_EXISTS [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`u`;`v`;`c`;`EL 3 ul`];
3637 INTRO_TAC Marchal_cells_3.BARV_CARD_LEMMA [`V`;`ul`;`3`];
3639 BY(ASM_MESON_TAC[IN]);
3640 MATCH_MP_TAC (arith `(x = y) ==> (x = 3 +1 ==> y = 4)`);
3642 REPEAT WEAK_STRIP_TAC;
3643 TYPIFY `left_action_list p ul` EXISTS_TAC;
3644 INTRO_TAC Rvfxzbu.RVFXZBU [`V`;`ul`;`3`;`p`];
3646 BY(ASM_REWRITE_TAC[IN_INSERT;arith `3 -1 = 2`]);
3648 INTRO_TAC Qzksykg.QZKSYKG1 [`V`;`ul`;`left_action_list p ul`;`3`;`p`];
3650 ASM_REWRITE_TAC[IN_INSERT;arith `3 - 1 = 2`];
3652 BY(ASM_MESON_TAC[NOT_IN_EMPTY; RIJRIED;MCELL3;NEGLIGIBLE_EMPTY]);
3654 ASM_REWRITE_TAC[IN;MCELL3];
3655 INTRO_TAC LENGTH4 [`ul`];
3657 BY(ASM_MESON_TAC[arith `3 + 1 = 4`;IN;Sphere.BARV]);
3658 DISCH_THEN (ASSUME_TAC o SYM);
3659 FIRST_X_ASSUM_ST `CONS x y = left_action_list p q` MP_TAC;
3661 DISCH_THEN (SUBST1_TAC o SYM);
3662 BY(REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0`])
3666 let SET2_INSERT2 = prove_by_refinement(
3667 `!(a:A) b w x y z. {a,b} SUBSET {w,x,y,z} /\ ~(a = b) /\ CARD {w,x,y,z} = 4 ==>
3668 (?c d. {w,x,y,z} = {a,b,c,d})`,
3671 REPEAT WEAK_STRIP_TAC;
3672 INTRO_TAC Hypermap.LEMMA_CARD_DIFF [`{w,x,y,z}`;`{a,b}`];
3673 ASM_REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY];
3674 INTRO_TAC Hypermap.CARD_TWO_ELEMENTS [`a`;`b`];
3676 DISCH_THEN SUBST1_TAC;
3677 REWRITE_TAC [arith `4 = x + 2 <=> x = 2`];
3679 INTRO_TAC Rogers.CARD_2_IMP_DOUBLE [`{w, x, y, z} DIFF {a, b}`];
3682 MATCH_MP_TAC FINITE_DIFF;
3683 BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]);
3684 REPEAT WEAK_STRIP_TAC;
3685 GEXISTL_TAC [`a'`;`b'`];
3686 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[])
3690 let MCELL4_EDGE_FIRST = prove_by_refinement(
3691 `!V ul u v. saturated V /\ packing V /\ ul IN barV V 3 /\
3692 {u,v} IN edgeX V (mcell4 V ul) ==>
3693 (?vl. vl IN barV V 3 /\ u = EL 0 vl /\ v = EL 1 vl /\ mcell4 V ul = mcell4 V vl)`,
3696 REPEAT WEAK_STRIP_TAC;
3697 TYPIFY `barV V 3 ul` (C SUBGOAL_THEN ASSUME_TAC);
3698 BY(ASM_MESON_TAC[IN]);
3699 TYPIFY `~NULLSET(mcell4 V ul)` (C SUBGOAL_THEN ASSUME_TAC);
3700 BY(ASM_MESON_TAC[NOT_IN_EMPTY; RIJRIED;MCELL4;NEGLIGIBLE_EMPTY]);
3701 INTRO_TAC MCELL4_EDGE [`V`;`ul`;`u`;`v`];
3703 BY(ASM_REWRITE_TAC[]);
3705 REPEAT WEAK_STRIP_TAC;
3706 TYPIFY `{EL 0 ul, EL 1 ul, EL 2 ul, EL 3 ul} = set_of_list ul` (C SUBGOAL_THEN ASSUME_TAC);
3707 ONCE_REWRITE_TAC[EQ_SYM_EQ];
3708 MATCH_MP_TAC set_of_list4;
3709 BY(ASM_MESON_TAC[arith `3+1 = 4`;IN;Sphere.BARV]);
3710 INTRO_TAC Marchal_cells_3.BARV_CARD_LEMMA [`V`;`ul`;`3`];
3711 ASM_REWRITE_TAC[arith `3 + 1 = 4`];
3713 INTRO_TAC SET2_INSERT2 [`u`;`v`;`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`EL 3 ul`];
3715 REPEAT WEAK_STRIP_TAC;
3716 INTRO_TAC Marchal_cells_3.LEFT_ACTION_LIST_3_EXISTS [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`EL 3 ul`;`u`;`v`;`c`;`d`];
3719 BY(ASM_MESON_TAC[]);
3720 REPEAT WEAK_STRIP_TAC;
3721 TYPIFY `left_action_list p ul` EXISTS_TAC;
3722 INTRO_TAC Rvfxzbu.RVFXZBU [`V`;`ul`;`4`;`p`];
3724 BY(ASM_REWRITE_TAC[IN_INSERT;arith `4 -1 = 3`]);
3726 INTRO_TAC Qzksykg.QZKSYKG1 [`V`;`ul`;`left_action_list p ul`;`4`;`p`];
3728 ASM_REWRITE_TAC[IN_INSERT;arith `4 - 1 = 3`];
3730 BY(ASM_MESON_TAC[MCELL4;NEGLIGIBLE_EMPTY]);
3732 ASM_REWRITE_TAC[IN;MCELL4];
3733 INTRO_TAC LENGTH4 [`ul`];
3735 BY(ASM_MESON_TAC[arith `3 + 1 = 4`;IN;Sphere.BARV]);
3736 DISCH_THEN (ASSUME_TAC o SYM);
3737 FIRST_X_ASSUM_ST `CONS x y = left_action_list p q` MP_TAC;
3739 DISCH_THEN (SUBST1_TAC o SYM);
3740 BY(REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0`])
3745 (* MCELL_EDGE_FIRST is YSAKKTX in the notes *)
3747 let MCELL_EDGE_FIRST = prove_by_refinement(
3748 `!V ul k u v. saturated V /\ packing V /\ ul IN barV V 3 /\
3749 {u,v} IN edgeX V (mcell k V ul) ==>
3750 (?vl. vl IN barV V 3 /\ mcell k V vl = mcell k V ul /\ u = EL 0 vl /\ v = EL 1 vl)
3754 REPEAT WEAK_STRIP_TAC;
3755 MP_TAC (arith `k <= 1 \/ k = 2 \/ k = 3 \/ 4 <= k`);
3756 REPEAT WEAK_STRIP_TAC;
3757 BY(ASM_MESON_TAC[EDGE_IMP_K2;NOT_IN_EMPTY;IN]);
3758 INTRO_TAC MCELL2_EDGE_FIRST [`V`;`ul`;`u`;`v`];
3759 REWRITE_TAC[MCELL2];
3760 BY(ASM_MESON_TAC[]);
3761 INTRO_TAC MCELL3_EDGE_FIRST [`V`;`ul`;`u`;`v`];
3762 REWRITE_TAC[MCELL3];
3763 BY(ASM_MESON_TAC[]);
3764 INTRO_TAC MCELL4_EDGE_FIRST [`V`;`ul`;`u`;`v`];
3765 FIRST_X_ASSUM_ST `mcell` MP_TAC;
3766 ASM_REWRITE_TAC[Pack_defs.mcell];
3767 ASM_SIMP_TAC [arith `4 <= k ==> ~(k=0) /\ ~(k = 1) /\ ~(k=2) /\ ~(k = 3)`];
3772 let BARV3_TRUNC2 = prove_by_refinement(
3773 `!V ul. ul IN barV V 3 ==> truncate_simplex 2 ul = [EL 0 ul;EL 1 ul;EL 2 ul]`,
3776 REPEAT WEAK_STRIP_TAC;
3777 TYPIFY `ul = [EL 0 ul;EL 1 ul; EL 2 ul; EL 3 ul]` (C SUBGOAL_THEN ASSUME_TAC);
3778 MATCH_MP_TAC LENGTH4;
3779 BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3+1 = 4`]);
3780 BY(ASM_MESON_TAC[Marchal_cells.TRUNCATE_SIMPLEX_EXPLICIT_2])
3784 let RBUTTCS = prove_by_refinement(
3785 `!V vl u v. saturated V /\ packing V /\ {u,v} IN edgeX V (mcell4 V vl) /\ vl IN barV V 3 ==>
3786 (?ul. leaf V ul /\ stem ul = {u,v} /\ (mcell4 V vl = cc_cell V ul))`,
3789 REPEAT WEAK_STRIP_TAC;
3790 INTRO_TAC MCELL_EDGE_FIRST [`V`;`vl`;`4`;`u`;`v`];
3793 BY(ASM_MESON_TAC[MCELL4]);
3794 REPEAT WEAK_STRIP_TAC;
3795 TYPIFY `~(mcell 4 V vl' = {})` (C SUBGOAL_THEN MP_TAC);
3796 BY(ASM_MESON_TAC[NOT_IN_EMPTY; RIJRIED;MCELL4;NEGLIGIBLE_EMPTY]);
3798 FIRST_X_ASSUM_ST `mcell 4 V vl' = mcell 4 V vl` (fun t -> REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[MCELL4] THEN SUBST1_TAC (SYM t));
3799 REWRITE_TAC[MCELL4] THEN REPEAT WEAK_STRIP_TAC;
3800 TYPED_ABBREV_TAC `(wl:(real^3) list) = truncate_simplex 2 (vl')` ;
3801 TYPIFY `hl vl' < sqrt(&2)` (C SUBGOAL_THEN ASSUME_TAC);
3802 FIRST_X_ASSUM_ST `mcell` MP_TAC;
3803 REWRITE_TAC[GSYM MCELL4;Pack_defs.mcell4];
3805 INTRO_TAC Rogers.XNHPWAB4 [`V`;`vl'`;`3`];
3807 DISCH_THEN (C INTRO_TAC [`2`;`3`]);
3810 TYPIFY `truncate_simplex 3 vl' = vl'` (C SUBGOAL_THEN ASSUME_TAC);
3811 MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_REFL;
3812 BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3 + 1 =4`]);
3815 TYPIFY `hl wl < sqrt(&2)` (C SUBGOAL_THEN ASSUME_TAC);
3816 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
3817 TYPIFY `leaf V wl` (C SUBGOAL_THEN ASSUME_TAC);
3819 ASM_REWRITE_TAC[Sphere.sqrt2];
3822 MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV;
3823 BY(ASM_MESON_TAC[IN;arith `2 <= 3`]);
3824 TYPIFY `EL 0 wl = u /\ EL 1 wl = v /\ EL 2 wl = EL 2 vl'` (C SUBGOAL_THEN ASSUME_TAC);
3826 REPEAT (GMATCH_SIMP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
3827 ASM_REWRITE_TAC[arith `1 <= 2 /\ 0 <= 2 /\ 2 <= 2`];
3828 BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `2 + 1 <= 3 + 1`]);
3829 ASM_CASES_TAC `mcell 4 V vl' = cc_cell V wl`;
3830 TYPIFY `wl` EXISTS_TAC;
3831 GMATCH_SIMP_TAC STEM_OF_LEAF;
3833 BY(ASM_MESON_TAC[]);
3834 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
3835 INTRO_TAC CFFONNL [`V`;`wl`;`mcell 4 V vl'`];
3838 REWRITE_TAC[Pack_defs.mcell_set;IN_ELIM_THM];
3840 BY(ASM_MESON_TAC[]);
3842 BY(ASM_MESON_TAC[]);
3843 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY];
3844 TYPIFY `EL 2 wl` EXISTS_TAC;
3845 REWRITE_TAC[IN_INTER];
3847 INTRO_TAC Lepjbdj.LEPJBDJ [`V`;`vl'`;`4`];
3848 ASM_REWRITE_TAC[arith `1 <= 4 /\ 4 <= 4 /\ 4 - 1 = 3`];
3850 BY(ASM_MESON_TAC[IN]);
3851 TYPIFY `EL 2 vl' IN set_of_list vl'` ENOUGH_TO_SHOW_TAC;
3853 GMATCH_SIMP_TAC set_of_list4;
3855 BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3+1 = 4`]);
3857 BY(REWRITE_TAC[cc_A0;Local_lemmas.X_IN_AFF_GT_X]);
3858 DISCH_THEN SUBST1_TAC;
3859 TYPIFY `[EL 1 vl';EL 0 vl';EL 2 vl']` EXISTS_TAC;
3861 TYPIFY `wl = [EL 0 vl';EL 1 vl'; EL 2 vl']` (C SUBGOAL_THEN ASSUME_TAC);
3863 GMATCH_SIMP_TAC BARV3_TRUNC2;
3864 BY(ASM_MESON_TAC[]);
3865 INTRO_TAC ZASUVOR [`V`;`EL 0 vl'`;`EL 1 vl'`;`EL 2 vl'`];
3867 BY(ASM_MESON_TAC[]);
3868 REPEAT WEAK_STRIP_TAC;
3870 GMATCH_SIMP_TAC STEM_OF_LEAF;
3872 BY(ASM_MESON_TAC[]);
3873 REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0`];
3878 let STEM_EDGEX = prove_by_refinement(
3879 `!V ul. packing V /\ saturated V /\ leaf V ul ==>
3880 {EL 0 ul,EL 1 ul} IN edgeX V (cc_cell V ul)`,
3883 REPEAT WEAK_STRIP_TAC;
3884 INTRO_TAC CC_CELL_NOT_NULLSET [`V`;`ul`];
3885 ASM_REWRITE_TAC[cc_cell];
3887 INTRO_TAC CC_KE_34 [`V`;`ul`];
3889 INTRO_TAC LIST_OF_CC_UH [`V`;`ul`];
3892 INTRO_TAC Marchal_cells_3.BARV_CARD_LEMMA [`V`;`cc_uh V ul`;`3`];
3893 INTRO_TAC EL_CC_UH [`V`;`ul`];
3896 INTRO_TAC cc_uh [`V`;`ul`];
3898 REPEAT WEAK_STRIP_TAC;
3899 FIRST_X_ASSUM MP_TAC;
3901 BY(ASM_MESON_TAC[IN]);
3902 REWRITE_TAC[arith `3 + 1 = 4`];
3904 INTRO_TAC set_of_list4 [`cc_uh V ul`];
3906 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 =4`]);
3908 INTRO_TAC Marchal_cells_2_new.CARD4_IMP_DISTINCT [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`EL 3 (cc_uh V ul)`];
3910 BY(ASM_MESON_TAC[]);
3913 FIRST_X_ASSUM DISJ_CASES_TAC;
3914 ASM_REWRITE_TAC[GSYM MCELL3];
3915 GMATCH_SIMP_TAC Bump.MCELL3_EDGE;
3918 BY(ASM_MESON_TAC[IN;MCELL3]);
3920 GMATCH_SIMP_TAC set_of_list3;
3922 BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `3 = 2 + 1`]);
3924 COMMENT "do case 4";
3925 ASM_REWRITE_TAC[GSYM MCELL4];
3926 GMATCH_SIMP_TAC Bump.MCELL4_EDGE;
3929 BY(ASM_MESON_TAC[IN;MCELL4]);
3935 let FCHKUGT = prove_by_refinement(
3936 `!V u0 u1 u2 u2'. saturated V /\ packing V /\ cc_A0 [u0;u1;u2] = cc_A0 [u0;u1;u2'] /\
3937 leaf V [u0;u1;u2] /\ leaf V [u0;u1;u2'] ==> (u2 = u2')`,
3940 REWRITE_TAC[cc_A0;EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`];
3941 REPEAT WEAK_STRIP_TAC;
3942 TYPIFY `~(u0 = u1)` (C SUBGOAL_THEN ASSUME_TAC);
3943 INTRO_TAC STEM_EDGEX [`V`;`[u0;u1;u2]`];
3945 ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`;CONS_11];
3946 REWRITE_TAC[IN_ELIM_THM;Pack_defs.edgeX;Geomdetail.PAIR_EQ_EXPAND];
3948 INTRO_TAC ZASUVOR [`V`;`u0`;`u1`;`u2`];
3951 INTRO_TAC CFFONNL [`V`;`[u0;u1;u2]`;`cc_cell V [u0;u1;u2']`];
3952 ASM_SIMP_TAC[CC_CELL_IN_MCELL_SET];
3953 REWRITE_TAC[TAUT `(a /\ b /\ ~c ==> d) <=> (a /\ b ==> c \/ d)`];
3955 REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0`];
3957 TYPIFY `{u0,u1} = {EL 0 [u0;u1;u2'],EL 1 [u0;u1;u2']}` (C SUBGOAL_THEN SUBST1_TAC);
3958 BY(REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0`]);
3959 MATCH_MP_TAC STEM_EDGEX;
3960 BY(ASM_REWRITE_TAC[]);
3961 INTRO_TAC NUNRRDS_0 [`V`;`[u0;u1;u2']`];
3962 ASM_REWRITE_TAC[cc_A0];
3963 REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`];
3964 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
3965 REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`];
3967 INTRO_TAC CC_KE_34 [`V`;`[u0;u1;u2']`];
3969 DISCH_THEN DISJ_CASES_TAC;
3970 FIRST_X_ASSUM DISJ_CASES_TAC;
3971 INTRO_TAC FUEIMOV_3 [`V`;`[u0;u1;u2']`;`[u0;u1;u2]`];
3972 ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`;CONS_11];
3974 INTRO_TAC FUEIMOV_3 [`V`;`[u0;u1;u2']`;`[u1;u0;u2]`];
3976 BY(ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`;CONS_11;Geomdetail.PAIR_EQ_EXPAND]);
3977 BY(ASM_REWRITE_TAC[CONS_11]);
3980 FIRST_X_ASSUM DISJ_CASES_TAC;
3981 INTRO_TAC FUEIMOV_4 [`V`;`[u0;u1;u2']`;`[u0;u1;u2]`];
3982 REWRITE_TAC[CONS_11];
3984 DISCH_THEN MP_TAC THEN ANTS_TAC;
3985 REPEAT (GMATCH_SIMP_TAC STEM_OF_LEAF);
3986 REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`;Geomdetail.PAIR_EQ_EXPAND];
3987 BY(ASM_MESON_TAC[]);
3988 ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`];
3989 INTRO_TAC LIST_OF_CC_UH [`V`;`[u0;u1;u2]`];
3991 DISCH_THEN SUBST1_TAC;
3992 BY(ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`;CONS_11]);
3993 COMMENT "case k=4 a";
3994 INTRO_TAC FUEIMOV_4 [`V`;`[u0;u1;u2']`;`[u1;u0;u2]`];
3995 REWRITE_TAC[CONS_11];
3997 DISCH_THEN MP_TAC THEN ANTS_TAC;
3998 REPEAT (GMATCH_SIMP_TAC STEM_OF_LEAF);
3999 REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`;Geomdetail.PAIR_EQ_EXPAND];
4000 BY(ASM_MESON_TAC[]);
4001 INTRO_TAC LIST_OF_CC_UH [`V`;`[u1;u0;u2]`];
4003 DISCH_THEN SUBST1_TAC;
4004 REWRITE_TAC[CONS_11];
4005 TYPIFY `EL 2 [u1;u0;u2] = u2` (C SUBGOAL_THEN SUBST1_TAC);
4006 BY(ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`;CONS_11]);
4007 REPEAT WEAK_STRIP_TAC;
4008 INTRO_TAC CC_CELL_NOT_COPLANAR_EXTREME [`V`;`[u0;u1;u2']`;`u2`];
4009 ASM_REWRITE_TAC[arith `~(4=3)`];
4011 FIRST_X_ASSUM (SUBST1_TAC o SYM);
4012 ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`;CONS_11];
4013 REPLICATE_TAC 8 (FIRST_X_ASSUM kill);
4014 REWRITE_TAC[coplanar];
4015 GEXISTL_TAC [`u0`;`u1`;`u2`];
4016 TYPIFY `{u0,u1,u2} SUBSET affine hull {u0,u1,u2}` (C SUBGOAL_THEN ASSUME_TAC);
4017 BY(REWRITE_TAC[HULL_SUBSET]);
4018 TYPIFY `u2' IN affine hull {u0,u1,u2}` ENOUGH_TO_SHOW_TAC;
4019 BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]);
4020 MATCH_MP_TAC Packing3.IN_TRANS;
4021 TYPIFY `aff_gt {u0,u1} {u2}` EXISTS_TAC;
4023 INTRO_TAC AFF_GT_SUBSET_AFFINE_HULL [`{u0,u1}`;`{u2}`];
4024 TYPIFY `{u0,u1} UNION {u2} = {u0,u1,u2}` (C SUBGOAL_THEN SUBST1_TAC);
4028 BY(REWRITE_TAC[Local_lemmas.X_IN_AFF_GT_X])
4032 let AZIM_BASE_SHIFT_LE = prove_by_refinement(
4034 ~(collinear {x,y,b1}) /\ ~(collinear {x,y,b2}) /\ ~(collinear {x,y,w1}) /\
4035 ~(collinear {x,y,w2}) /\
4036 azim x y b1 b2 <= azim x y b1 w1 /\
4037 azim x y b1 b2 <= azim x y b1 w2 ==>
4038 azim x y b1 w2 - azim x y b1 w1 = azim x y b2 w2 - azim x y b2 w1`,
4041 REPEAT WEAK_STRIP_TAC;
4042 INTRO_TAC Fan.sum4_azim_fan [`x`;`y`;`b1`;`b2`;`w1`];
4043 DISCH_THEN GMATCH_SIMP_TAC;
4044 INTRO_TAC Fan.sum4_azim_fan [`x`;`y`;`b1`;`b2`;`w2`];
4045 DISCH_THEN GMATCH_SIMP_TAC;
4051 let WEDGE_GE_SPLIT = prove_by_refinement(
4053 ~(collinear {u0,u1,u2}) /\
4054 ~(collinear {u0,u1,u3}) /\
4055 w IN wedge u0 u1 u2 u3 ==>
4056 ( ~(collinear {u0,u1,w}) /\
4057 wedge_ge u0 u1 u2 u3 = wedge_ge u0 u1 u2 w UNION wedge_ge u0 u1 w u3)`,
4060 REWRITE_TAC[wedge;IN_ELIM_THM];
4061 REWRITE_TAC[EXTENSION;IN_UNION;Local_lemmas.WEDGE_GE_AZIM_LE];
4062 REPEAT WEAK_STRIP_TAC;
4064 REPEAT WEAK_STRIP_TAC;
4065 ASM_CASES_TAC `azim u0 u1 u2 x <= azim u0 u1 u2 w`;
4067 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
4069 TYPIFY `collinear {u0,u1,x}` ASM_CASES_TAC;
4070 INTRO_TAC (CONJUNCT2 (CONJUNCT2 AZIM_DEGENERATE)) [`u0`;`u1`;`u2`;`x`];
4072 DISCH_THEN SUBST1_TAC;
4073 INTRO_TAC (CONJUNCT2 (CONJUNCT2 AZIM_DEGENERATE)) [`u0`;`u1`;`w`;`x`];
4075 DISCH_THEN SUBST1_TAC;
4076 BY(REWRITE_TAC[Local_lemmas.AZIM_RANGE]);
4077 ONCE_REWRITE_TAC[arith `x <= y <=> &0 <= y - x`];
4078 INTRO_TAC AZIM_BASE_SHIFT_LE [`u0`;`u1`;`u2`;`w`;`u3`;`x`];
4080 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
4084 let IN_CONV0_IMP_AZIM_PI_ALT = prove_by_refinement(
4085 `!x e a b. ~collinear {x, a, e} /\ x IN conv0 {a, b} ==> azim x e a b = pi`,
4088 MESON_TAC[Local_lemmas.IN_CONV0_IMP_AZIM_PI]
4092 let AFF_GT_0_2 = prove
4099 y = t2 % v + t3 % w}`,
4103 let MIDPOINT_IN_CONV0 = prove_by_refinement(
4104 `!(p:real^A) q. (#0.5) % (p + q) IN conv0 {p,q}`,
4107 REWRITE_TAC[conv0;SYM Sphere.aff_gt_def;AFF_GT_0_2];
4108 REWRITE_TAC[conv0;SYM Sphere.aff_gt_def;AFF_GT_0_2;IN_ELIM_THM];
4109 REPEAT WEAK_STRIP_TAC;
4110 GEXISTL_TAC [`#0.5`;`#0.5`];
4111 BY(REPEAT CONJ_TAC THENL [REAL_ARITH_TAC;REAL_ARITH_TAC;REAL_ARITH_TAC;VECTOR_ARITH_TAC])
4115 let AZIM_SPLIT_POINT = prove_by_refinement(
4117 ~collinear {u0,u1,u2} /\
4118 ~collinear {u0,u1,u3} /\
4119 pi < azim u0 u1 u2 u3 ==>
4121 w IN wedge u0 u1 u2 u3 /\
4122 azim u0 u1 u2 w = pi /\
4123 azim u0 u1 w u3 < pi)
4127 REPEAT WEAK_STRIP_TAC;
4128 ABBREV_TAC `(w:real^3) = &2 % u0 - u2`;
4129 TYPIFY `w` EXISTS_TAC;
4130 INTRO_TAC IN_CONV0_IMP_AZIM_PI_ALT [`u0`;`u1`;`u2`;`w`];
4133 TYPIFY `{u0,u2,u1} = {u0,u1,u2}` ENOUGH_TO_SHOW_TAC;
4134 BY(DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[]);
4136 INTRO_TAC MIDPOINT_IN_CONV0 [`u2`;`w`];
4137 MATCH_MP_TAC (TAUT `(a = b) ==> (a ==> b)`);
4138 AP_THM_TAC THEN AP_TERM_TAC;
4140 BY(VECTOR_ARITH_TAC);
4143 ASM_REWRITE_TAC[wedge;IN_ELIM_THM];
4144 REWRITE_TAC[PI_POS];
4147 INTRO_TAC (CONJUNCT2 (CONJUNCT2 AZIM_DEGENERATE)) [`u0`;`u1`;`u2`;`w`];
4152 INTRO_TAC Fan.sum4_azim_fan [`u0`;`u1`;`u2`;`w`;`u3`];
4155 BY(FIRST_X_ASSUM_ST `pi < x` MP_TAC THEN REAL_ARITH_TAC);
4156 REWRITE_TAC[arith `x = pi + y <=> y = x - pi`];
4157 DISCH_THEN SUBST1_TAC;
4158 BY(REWRITE_TAC[Local_lemmas.AZIM_RANGE;arith `x - pi < pi <=> x < &2 * pi`])
4162 let CLOSED_WEDGE_LT_PI = prove_by_refinement(
4163 `!u0 u1 u2 u3. ~collinear {u0,u1,u2} /\ ~ collinear {u0,u1,u3} /\
4164 azim u0 u1 u2 u3 < pi ==> closed (wedge_ge u0 u1 u2 u3)`,
4167 REPEAT WEAK_STRIP_TAC;
4168 ASM_SIMP_TAC[Local_lemmas.WEDGE_GE_EQ_AFF_GE];
4169 MATCH_MP_TAC CLOSED_AFF_GE;
4170 BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY])
4174 let CLOSED_WEDGE_EQ_PI = prove_by_refinement(
4175 `!u0 u1 u2 u3. ~collinear {u0,u1,u2} /\ ~ collinear {u0,u1,u3} /\
4176 azim u0 u1 u2 u3 = pi ==> closed (wedge_ge u0 u1 u2 u3)`,
4179 REPEAT WEAK_STRIP_TAC;
4180 ASM_SIMP_TAC[Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT];
4181 ABBREV_TAC `e = ((u1 - u0) cross (u2 - u0))`;
4182 TYPIFY `!x. e dot (x - u0) = e dot x - e dot u0` (C SUBGOAL_THEN (unlist REWRITE_TAC));
4183 BY(VECTOR_ARITH_TAC);
4184 ONCE_REWRITE_TAC[arith `&0 <= x - y <=> x >= y`];
4185 BY(REWRITE_TAC[CLOSED_HALFSPACE_GE])
4189 let CLOSED_WEDGE = prove_by_refinement(
4190 `!u0 u1 u2 u3. ~collinear {u0,u1,u2} /\ ~ collinear {u0,u1,u3} ==> closed (wedge_ge u0 u1 u2 u3)`,
4193 REPEAT WEAK_STRIP_TAC;
4194 TYPIFY `azim u0 u1 u2 u3 < pi \/ azim u0 u1 u2 u3 = pi \/ pi < azim u0 u1 u2 u3` (C SUBGOAL_THEN MP_TAC);
4196 REPEAT WEAK_STRIP_TAC;
4197 BY(ASM_MESON_TAC[CLOSED_WEDGE_LT_PI]);
4198 BY(ASM_MESON_TAC[CLOSED_WEDGE_EQ_PI]);
4199 INTRO_TAC AZIM_SPLIT_POINT [`u0`;`u1`;`u2`;`u3`];
4201 REPEAT WEAK_STRIP_TAC;
4202 INTRO_TAC WEDGE_GE_SPLIT [`u0`;`u1`;`u2`;`u3`;`w`];
4204 REPEAT WEAK_STRIP_TAC;
4206 MATCH_MP_TAC CLOSED_UNION;
4208 BY(ASM_MESON_TAC[CLOSED_WEDGE_EQ_PI]);
4209 BY(ASM_MESON_TAC[CLOSED_WEDGE_LT_PI])
4213 let WEDGE_INTER_AFF_GE = prove_by_refinement(
4215 wedge u0 u1 v1 v2 INTER aff_ge {u0,u1} {v1} = {} /\
4216 wedge u0 u1 v1 v2 INTER aff_ge {u0,u1} {v2} = {}
4220 REWRITE_TAC[wedge;EXTENSION;NOT_IN_EMPTY;IN_INTER;IN_ELIM_THM];
4221 REPEAT WEAK_STRIP_TAC;
4223 REPEAT WEAK_STRIP_TAC;
4224 FIRST_X_ASSUM MP_TAC;
4225 GMATCH_SIMP_TAC (GSYM Local_lemmas.AZIM_EQ_0_GE_ALT2);
4227 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
4229 BY(ASM_MESON_TAC[AZIM_DEGENERATE;arith `~(&0 < &0)`]);
4230 REPEAT WEAK_STRIP_TAC;
4231 FIRST_X_ASSUM MP_TAC;
4232 GMATCH_SIMP_TAC (GSYM Local_lemmas.AZIM_EQ_0_GE_ALT2);
4235 BY(ASM_MESON_TAC[AZIM_DEGENERATE;arith `~(&0 < x /\ x < &0)`]);
4237 TYPIFY `~collinear {u0,u1,v1}` (C SUBGOAL_THEN ASSUME_TAC);
4238 BY(ASM_MESON_TAC[AZIM_DEGENERATE;arith `~(&0 < &0)`]);
4240 INTRO_TAC Fan.sum5_azim_fan [`u0`;`u1`;`v1`;`v2`;`x`];
4242 REWRITE_TAC[Local_lemmas.AZIM_RANGE];
4243 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
4247 let AFF_GE_SUBSET_WEDGE_GE = prove_by_refinement(
4249 ~collinear {u0,u1,v1} /\
4250 ~collinear {u0,u1,v2} ==>
4251 aff_ge {u0,u1} {v1} SUBSET wedge_ge u0 u1 v1 v2 /\
4252 aff_ge {u0,u1} {v2} SUBSET wedge_ge u0 u1 v1 v2
4256 REWRITE_TAC[Local_lemmas.WEDGE_GE_AZIM_LE;EXTENSION;NOT_IN_EMPTY;SUBSET;IN_ELIM_THM];
4257 REPEAT WEAK_STRIP_TAC;
4258 REWRITE_TAC[AND_FORALL_THM];
4260 ASM_SIMP_TAC[GSYM Local_lemmas.AZIM_EQ_0_GE_ALT2;Local_lemmas.AZIM_RANGE];
4262 TYPIFY `collinear {u0,u1,x}` ASM_CASES_TAC;
4263 BY(ASM_MESON_TAC[AZIM_DEGENERATE;Local_lemmas.AZIM_RANGE]);
4264 INTRO_TAC Fan.sum5_azim_fan [`u0`;`u1`;`v1`;`v2`;`x`];
4265 ASM_REWRITE_TAC[Local_lemmas.AZIM_RANGE];
4270 let BDXKHTW_PREP_LEMMA = prove_by_refinement(
4271 `!u0 u1 v1 v2 V X. saturated V /\ packing V /\ leaf V [u0;u1;v1] /\ leaf V [u0;u1;v2] /\
4273 {u0,u1} IN edgeX V X /\
4274 ~(azim u0 u1 v1 v2 = &0) /\ (?y. y IN X INTER wedge u0 u1 v1 v2) /\
4275 (?x. x IN X /\ ~(x IN wedge_ge u0 u1 v1 v2)) ==>
4276 (convex X /\ ~(u0=u1) /\ ~collinear {u0,u1,v1} /\ ~collinear {u0,u1,v2} /\
4277 (?p q. p IN X INTER wedge u0 u1 v1 v2 /\ q IN X DIFF wedge_ge u0 u1 v1 v2 /\ ~coplanar {p,q,u0,u1} /\
4278 ~(p IN aff_ge {u0,u1} {v1} UNION aff_ge {u0,u1} {v2}) /\
4279 ~(q IN aff_ge {u0,u1} {v1} UNION aff_ge {u0,u1} {v2})))
4283 COMMENT "initialize";
4284 REWRITE_TAC[SUBSET;Pack_defs.mcell_set;IN_ELIM_THM];
4285 REPEAT WEAK_STRIP_TAC;
4286 INTRO_TAC GBEWYFX [`V`;`[u0;u1;v1]`];
4287 INTRO_TAC GBEWYFX [`V`;`[u0;u1;v2]`];
4288 ASM_REWRITE_TAC[Bump.set_of_list3_explicit];
4289 REPEAT WEAK_STRIP_TAC;
4290 ASM_CASES_TAC `NULLSET X`;
4291 INTRO_TAC Bump.RIJRIED [`V`;`ul`;`i`];
4294 BY(ASM_MESON_TAC[]);
4296 BY(ASM_MESON_TAC[NOT_IN_EMPTY]);
4297 TYPIFY `2 <= i` (C SUBGOAL_THEN ASSUME_TAC);
4298 REWRITE_TAC[arith `2 <= i <=> ~(i <= 1)`];
4300 INTRO_TAC Bump.EDGE_IMP_K2 [`V`;`ul`;`i`];
4303 BY(ASM_MESON_TAC[IN]);
4304 BY(ASM_MESON_TAC[NOT_IN_EMPTY]);
4305 TYPIFY `convex X` (C SUBGOAL_THEN ASSUME_TAC);
4306 BY(ASM_MESON_TAC[MCELL_CONVEX;IN]);
4308 ABBREV_TAC `(s:real^3->bool) = aff_ge {u0,u1} {v1} UNION aff_ge {u0,u1} {v2}`;
4309 TYPIFY `NULLSET s` (C SUBGOAL_THEN ASSUME_TAC);
4311 MATCH_MP_TAC (CONJUNCT2 NULLSET_RULES);
4312 BY(ASM_SIMP_TAC[Conforming.NEGLIGIBLE_AFF_GE_2_1]);
4313 ABBREV_TAC `(X':real^3->bool) = X DIFF s`;
4314 COMMENT "X' not planar";
4315 TYPIFY `~(coplanar X')` (C SUBGOAL_THEN ASSUME_TAC);
4318 TYPIFY `~(coplanar X)` (C SUBGOAL_THEN ASSUME_TAC);
4319 BY(ASM_MESON_TAC[COPLANAR_IMP_NEGLIGIBLE]);
4320 TYPIFY `X SUBSET X' UNION s` (C SUBGOAL_THEN ASSUME_TAC);
4323 FIRST_X_ASSUM_ST `~NULLSET X` MP_TAC;
4325 MATCH_MP_TAC NEGLIGIBLE_SUBSET;
4326 TYPIFY `X' UNION s` EXISTS_TAC;
4328 MATCH_MP_TAC (CONJUNCT2 NULLSET_RULES);
4330 BY(ASM_MESON_TAC[COPLANAR_IMP_NEGLIGIBLE]);
4331 COMMENT "X'' not planar";
4332 INTRO_TAC COPLANAR_UNION [`X' INTER wedge u0 u1 v1 v2`;`X' INTER ((:real^3) DIFF wedge_ge u0 u1 v1 v2)`;`u0`;`u1`];
4333 ABBREV_TAC `X'' = (X' INTER wedge u0 u1 v1 v2 UNION X' INTER ((:real^3) DIFF wedge_ge u0 u1 v1 v2) UNION {u0, u1})`;
4334 TYPIFY `X' SUBSET X''` (C SUBGOAL_THEN ASSUME_TAC);
4336 REWRITE_TAC[SUBSET;IN_UNION;IN_INTER;IN_DIFF;IN_UNIV];
4337 REPEAT WEAK_STRIP_TAC;
4339 MATCH_MP_TAC (TAUT `(~a ==> b) ==> (a \/ b \/ c)`);
4341 INTRO_TAC WEDGE_WEDGE_GE [`u0`;`u1`;`v1`;`v2`];
4343 REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC);
4346 TYPIFY `~(coplanar X'')` (C SUBGOAL_THEN (unlist REWRITE_TAC));
4347 REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC);
4348 BY(MESON_TAC[COPLANAR_SUBSET]);
4349 COMMENT "start on conjuncts";
4351 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY];
4352 TYPIFY `y` EXISTS_TAC;
4354 REWRITE_TAC[IN_INTER;IN_DIFF];
4355 TYPIFY `~(y IN s)` ENOUGH_TO_SHOW_TAC;
4356 BY(REPEAT (FIRST_X_ASSUM_ST `INTER` MP_TAC) THEN SET_TAC[]);
4358 INTRO_TAC WEDGE_INTER_AFF_GE [`u0`;`u1`;`v1`;`v2`];
4359 BY(REPEAT (FIRST_X_ASSUM_ST `INTER` MP_TAC) THEN SET_TAC[]);
4361 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY];
4362 TYPIFY `x` EXISTS_TAC;
4364 TYPIFY `s SUBSET wedge_ge u0 u1 v1 v2` ENOUGH_TO_SHOW_TAC;
4365 REPEAT (FIRST_X_ASSUM_ST `IN` MP_TAC);
4368 REWRITE_TAC[UNION_SUBSET];
4369 BY(ASM_SIMP_TAC[AFF_GE_SUBSET_WEDGE_GE]);
4370 COMMENT "next conjunct A";
4371 TYPIFY `~(u0 = u1)` (C SUBGOAL_THEN ASSUME_TAC);
4372 FIRST_X_ASSUM_ST `~collinear t` kill;
4373 FIRST_X_ASSUM_ST `~collinear t` MP_TAC;
4374 BY(MESON_TAC[Collect_geom.NOT_COLLINEAR_IMP_2_UNEQUAL]);
4375 REWRITE_TAC[TAUT `(a /\ b /\ c) = ((a /\ b) /\ c)`];
4377 REWRITE_TAC[AND_FORALL_THM];
4381 REWRITE_TAC[IN_INTER;IN_UNION;IN_DIFF];
4382 TYPIFY `collinear {p,u0,u1} ==> p IN aff_ge {u0,u1} {v1}` ENOUGH_TO_SHOW_TAC;
4384 TYPIFY `{p,u0,u1} = {u0,u1,p}` (C SUBGOAL_THEN SUBST1_TAC);
4386 ASM_SIMP_TAC[COLLINEAR_3_IN_AFFINE_HULL];
4387 TYPIFY `affine hull {u0,u1} SUBSET aff_ge {u0,u1} {v1}` ENOUGH_TO_SHOW_TAC;
4389 MATCH_MP_TAC AFFINE_HULL_SUBSET_AFF_GE;
4390 BY(ASM_SIMP_TAC[Fan.th3a]);
4392 FIRST_X_ASSUM_ST `mcell` MP_TAC;
4395 BY(ASM_MESON_TAC[]);
4396 FIRST_X_ASSUM MP_TAC;
4397 REWRITE_TAC[NOT_FORALL_THM];
4398 REPEAT WEAK_STRIP_TAC;
4399 GEXISTL_TAC [`p`;`q`];
4400 FIRST_X_ASSUM MP_TAC;
4402 FIRST_X_ASSUM_ST `X = mcell i V ul` SUBST1_TAC;
4407 let WEDGE_SUBSET_WEDGE_GE = prove_by_refinement(
4408 `!u0 u1 u2 u3. wedge u0 u1 u2 u3 SUBSET wedge_ge u0 u1 u2 u3`,
4411 REWRITE_TAC[wedge;SUBSET;Local_lemmas.WEDGE_GE_AZIM_LE;IN_ELIM_THM];
4416 let AFF_INTER_IMP_COPLANAR = prove_by_refinement(
4417 `!a b c (d:real^3). ~(affine hull {a,b} INTER affine hull {c,d} ={}) ==>
4418 coplanar {a,b,c,d}`,
4421 REWRITE_TAC[EXTENSION;IN_INTER;NOT_IN_EMPTY];
4422 REWRITE_TAC[AFFINE_HULL_2_ALT;IN_ELIM_THM;IN_UNIV;NOT_FORALL_THM];
4423 REPEAT WEAK_STRIP_TAC;
4424 REWRITE_TAC[coplanar];
4425 ASM_CASES_TAC `u = &0`;
4426 GEXISTL_TAC [`b`;`c`;`d`];
4427 TYPIFY `{b,c,d} SUBSET affine hull {b,c,d} /\ a IN affine hull {b,c,d}` ENOUGH_TO_SHOW_TAC;
4429 REWRITE_TAC[HULL_SUBSET];
4430 REWRITE_TAC[AFFINE_HULL_3;IN_ELIM_THM];
4431 GEXISTL_TAC [`&0`;`&1 - u'`;`u'`];
4434 BY(REPEAT (FIRST_X_ASSUM_ST `%` MP_TAC) THEN ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);
4435 GEXISTL_TAC [`a`;`c`;`d`];
4436 TYPIFY `{a,c,d} SUBSET affine hull {a,c,d} /\ b IN affine hull {a,c,d}` ENOUGH_TO_SHOW_TAC;
4438 REWRITE_TAC[HULL_SUBSET];
4439 REWRITE_TAC[AFFINE_HULL_3;IN_ELIM_THM];
4440 GEXISTL_TAC [`(u - &1)/ u`;`(&1 - u')/ u`;`u' / u`];
4442 Calc_derivative.CALC_ID_TAC;
4443 BY(ASM_REWRITE_TAC[]);
4444 MATCH_MP_TAC VECTOR_MUL_LCANCEL_IMP;
4445 TYPIFY `u` EXISTS_TAC;
4447 REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC];
4448 TYPIFY `!x. u * x / u = x` (C SUBGOAL_THEN (unlist REWRITE_TAC));
4450 Calc_derivative.CALC_ID_TAC;
4451 BY(ASM_REWRITE_TAC[]);
4452 BY(REPEAT (FIRST_X_ASSUM_ST `%` MP_TAC) THEN VECTOR_ARITH_TAC)
4456 let NOT_COLLINEAR_AFF_DIM2 = prove_by_refinement(
4457 `!(a:real^A) b c. ~collinear {a,b,c} ==> aff_dim {a,b,c} = &2`,
4460 REWRITE_TAC[COLLINEAR_AFF_DIM];
4461 REPEAT WEAK_STRIP_TAC;
4462 INTRO_TAC AFF_DIM_3 [`a`;`b`;`c`];
4463 BY(FIRST_X_ASSUM MP_TAC THEN INT_ARITH_TAC)
4467 let ADD_NN_ZERO = prove_by_refinement(
4468 `!a b x y. &0 < a /\ &0 < b /\ &0 <= x /\ &0 <= y /\ a * x + b * y = &0 ==> (x = &0 /\ y = &0)`,
4471 REPEAT WEAK_STRIP_TAC;
4473 FIRST_X_ASSUM_ST `+` (MP_TAC o (MATCH_MP (arith `x + y = &0 ==> (~(&0 <= x) \/ ~(&0 <= y) \/ (x = &0 /\ y = &0))`)));
4474 REPEAT WEAK_STRIP_TAC;
4475 FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[];
4476 GMATCH_SIMP_TAC REAL_LE_MUL;
4477 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
4478 FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[];
4479 GMATCH_SIMP_TAC REAL_LE_MUL;
4480 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
4481 REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC);
4482 REWRITE_TAC[REAL_ENTIRE];
4483 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
4487 let BDXKHTW = prove_by_refinement(
4488 `!u0 u1 v1 v2 V X. saturated V /\ packing V /\ leaf V [u0;u1;v1] /\ leaf V [u0;u1;v2] /\
4490 {u0,u1} IN edgeX V X /\
4491 ~(azim u0 u1 v1 v2 = &0) /\ (?y. y IN X INTER wedge u0 u1 v1 v2) ==>
4492 (X SUBSET wedge_ge u0 u1 v1 v2)`,
4495 REPEAT WEAK_STRIP_TAC;
4497 INTRO_TAC BDXKHTW_PREP_LEMMA [`u0`;`u1`;`v1`;`v2`;`V`;`X`];
4499 BY(ASM_MESON_TAC[SUBSET]);
4500 REPEAT WEAK_STRIP_TAC;
4501 INTRO_TAC CONNECTED_SEGMENT_NOT_COVERED [`wedge u0 u1 v1 v2`;`(:real^3) DIFF wedge_ge u0 u1 v1 v2`;`p`;`q`];
4503 ASM_SIMP_TAC[OPEN_WEDGE;CLOSED_WEDGE;GSYM closed];
4504 REWRITE_TAC[TAUT `(a /\ b /\ c) = ((a /\ b) /\ c)`];
4506 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
4507 BY(SET_TAC[WEDGE_SUBSET_WEDGE_GE]);
4508 REWRITE_TAC[IN_DIFF;IN_UNIV];
4509 REPEAT WEAK_STRIP_TAC;
4511 TYPIFY `x IN X` (C SUBGOAL_THEN ASSUME_TAC);
4512 TYPIFY `segment [p,q] SUBSET X` ENOUGH_TO_SHOW_TAC;
4513 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
4514 FIRST_X_ASSUM_ST `convex` MP_TAC;
4515 REWRITE_TAC[ CONVEX_CONTAINS_SEGMENT];
4516 BY(REPEAT (FIRST_X_ASSUM_ST `IN` MP_TAC) THEN SET_TAC[]);
4517 COMMENT "x IN aff_ge";
4518 TYPIFY `?v. leaf V [u0;u1;v] /\ ~collinear {u0,u1,v} /\ x IN aff_ge {u0,u1} {v} /\ ~(p IN aff_ge {u0,u1} {v}) /\ ~(q IN aff_ge {u0,u1} {v})` (C SUBGOAL_THEN MP_TAC);
4519 INTRO_TAC WEDGE_WEDGE_GE [`u0`;`u1`;`v1`;`v2`];
4521 REPEAT (FIRST_X_ASSUM_ST `UNION` MP_TAC);
4522 REWRITE_TAC[SUBSET;IN_UNION];
4523 BY(ASM_MESON_TAC[]);
4524 REPEAT WEAK_STRIP_TAC;
4525 COMMENT "non degeneracies";
4526 TYPIFY `~(x = p) /\ ~(x = q)` (C SUBGOAL_THEN ASSUME_TAC);
4527 BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
4528 FIRST_X_ASSUM_ST `segment` MP_TAC;
4529 REWRITE_TAC[closed_segment;IN_ELIM_THM];
4530 REPEAT WEAK_STRIP_TAC;
4531 TYPIFY `~(p = q)` (C SUBGOAL_THEN ASSUME_TAC);
4532 FIRST_X_ASSUM_ST `DIFF` MP_TAC;
4533 FIRST_X_ASSUM_ST `INTER` MP_TAC;
4534 BY(SET_TAC[WEDGE_SUBSET_WEDGE_GE]);
4535 TYPIFY `&0 < u` (C SUBGOAL_THEN ASSUME_TAC);
4536 ASM_SIMP_TAC[arith `&0 <= u ==> (&0 < u <=> ~(u= &0))`];
4538 FIRST_X_ASSUM_ST `%` MP_TAC;
4539 BY(ASM_REWRITE_TAC[varith `(&1 - &0) % p + &0 % q = (p:real^3)`]);
4540 TYPIFY `u < &1` (C SUBGOAL_THEN ASSUME_TAC);
4541 ASM_SIMP_TAC[arith `u <= &1 ==> (u < &1 <=> ~(u= &1))`];
4543 FIRST_X_ASSUM_ST `%` MP_TAC;
4544 BY(ASM_REWRITE_TAC[varith `(&1 - &1) % p + &1 % q = (q:real^3)`]);
4545 COMMENT "x not in aff {u0,u1}";
4546 TYPIFY `~(x IN affine hull {u0,u1})` (C SUBGOAL_THEN ASSUME_TAC);
4548 FIRST_X_ASSUM_ST `coplanar` MP_TAC;
4550 MATCH_MP_TAC AFF_INTER_IMP_COPLANAR;
4551 ASM_REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER;NOT_FORALL_THM];
4552 TYPIFY `x` EXISTS_TAC;
4554 REWRITE_TAC[AFFINE_HULL_2_ALT;IN_ELIM_THM;IN_UNIV];
4555 TYPIFY `u` EXISTS_TAC;
4556 BY(VECTOR_ARITH_TAC);
4557 COMMENT "x in aff_gt";
4558 TYPIFY `x IN aff_gt {u0,u1} {v}` (C SUBGOAL_THEN ASSUME_TAC);
4559 TYPIFY `DISJOINT {u0,u1} {v}` (C SUBGOAL_THEN ASSUME_TAC);
4560 BY(ASM_SIMP_TAC[Fan.th3a]);
4561 REPLICATE_TAC 5 (FIRST_X_ASSUM_ST `IN` MP_TAC);
4562 ASM_SIMP_TAC[Collect_geom.IN_AFF_GE_INTERPRET_TO_AFF_GT_AND_AFF];
4563 BY(MESON_TAC[Sphere.aff]);
4564 COMMENT "introduce cc";
4565 TYPIFY `?ul. leaf V ul /\ X = cc_cell V ul /\ stem ul = {u0,u1} /\ cc_A0 ul = aff_gt {u0,u1} {v} /\ set_of_list ul = {u0,u1,v} ` (C SUBGOAL_THEN MP_TAC);
4566 INTRO_TAC CFFONNL [`V`;`[u0;u1;v]`;`X`];
4568 REWRITE_TAC[TAUT `(a /\ b /\ ~c ==> d) <=> (a /\ b ==> (c \/ d))`];
4570 ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`;cc_A0];
4571 REWRITE_TAC[EXTENSION;IN_INTER;NOT_IN_EMPTY;NOT_FORALL_THM];
4572 TYPIFY `x` EXISTS_TAC;
4573 BY(ASM_REWRITE_TAC[]);
4574 REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`];
4575 DISCH_THEN DISJ_CASES_TAC;
4576 TYPIFY `[u0;u1;v]` EXISTS_TAC;
4577 ASM_REWRITE_TAC[cc_A0;EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`;set_of_list3_explicit];
4578 GMATCH_SIMP_TAC STEM_OF_LEAF;
4579 REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`];
4580 BY(ASM_MESON_TAC[]);
4581 TYPIFY `[u1;u0;v]` EXISTS_TAC;
4582 ASM_REWRITE_TAC[cc_A0;EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`;set_of_list3_explicit];
4583 INTRO_TAC ZASUVOR [`V`;`u0`;`u1`;`v`];
4585 REPEAT WEAK_STRIP_TAC;
4590 AP_THM_TAC THEN AP_TERM_TAC;
4592 GMATCH_SIMP_TAC STEM_OF_LEAF;
4593 ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`];
4596 BY(ASM_MESON_TAC[]);
4597 REPEAT WEAK_STRIP_TAC;
4598 COMMENT "introduce chi_msb";
4599 INTRO_TAC CELL_NN [`V`;`ul`;`p`];
4602 FIRST_X_ASSUM_ST `INTER` MP_TAC;
4606 INTRO_TAC CELL_NN [`V`;`ul`;`q`];
4609 FIRST_X_ASSUM_ST `DIFF` MP_TAC;
4613 COMMENT "chi x = 0";
4614 INTRO_TAC AFFINE_IMP_CHI_MSB_0 [`ul`;`x`];
4617 BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
4618 REPEAT (FIRST_X_ASSUM_ST `aff_gt` MP_TAC);
4620 TYPIFY ` {u0,u1,v} = {u0,u1} UNION {v} ` (C SUBGOAL_THEN SUBST1_TAC);
4622 TYPIFY `aff_gt {u0, u1} {v} SUBSET affine hull ({u0, u1} UNION {v})` ENOUGH_TO_SHOW_TAC;
4624 BY(MESON_TAC[AFF_GT_SUBSET_AFFINE_HULL]);
4626 GMATCH_SIMP_TAC CHI_MSB_ADDITIVE;
4630 FIRST_X_ASSUM_ST `coplanar` MP_TAC;
4631 REWRITE_TAC[coplanar];
4632 GEXISTL_TAC [`u0`;`u1`;`v`];
4633 TYPIFY `p IN affine hull {u0,u1,v} /\ q IN affine hull {u0,u1,v} /\ {u0,u1,v} SUBSET affine hull {u0,u1,v}` ENOUGH_TO_SHOW_TAC;
4635 REWRITE_TAC[HULL_SUBSET];
4636 FIRST_X_ASSUM_ST `x = {a,b,c}` (SUBST1_TAC o SYM);
4637 REPEAT (GMATCH_SIMP_TAC COPLANAR_INSERT);
4638 COMMENT "fresh start";
4639 REPEAT (GMATCH_SIMP_TAC set_of_list3);
4640 TYPIFY `!p. {p,EL 0 ul, EL 1 ul, EL 2 ul} = {EL 0 ul, EL 1 ul, EL 2 ul,p}` (C SUBGOAL_THEN (unlist ONCE_REWRITE_TAC));
4642 REWRITE_TAC[CHI_MSB_COPLANAR];
4643 REPEAT (GMATCH_SIMP_TAC NOT_COLLINEAR_AFF_DIM2);
4644 TYPIFY `LENGTH ul = 3` (C SUBGOAL_THEN ASSUME_TAC);
4645 BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
4646 TYPIFY `set_of_list ul = {EL 0 ul, EL 1 ul, EL 2 ul}` (C SUBGOAL_THEN ASSUME_TAC);
4647 BY(ASM_SIMP_TAC[set_of_list3]);
4649 BY(ASM_MESON_TAC[GBEWYFX]);
4651 TYPIFY ` [EL 0 ul;EL 1 ul;EL 2 ul] = ul` ((C SUBGOAL_THEN SUBST1_TAC));
4652 BY(ASM_SIMP_TAC[ GSYM LENGTH3]);
4653 MATCH_MP_TAC (TAUT `a /\ b ==> b /\ a`);
4654 MATCH_MP_TAC ADD_NN_ZERO;
4655 GEXISTL_TAC [`(&1 - u)`;`u`];
4656 BY(ASM_SIMP_TAC[arith `u < &1 ==> &0 < &1 - u`])
4660 let AZIM_POS_IMP_SUM_2PI_ALT = prove_by_refinement(
4662 &0 < azim a b c d ==> azim a b c d + azim a b d c = &2 * pi
4666 MESON_TAC[Local_lemmas1.AZIM_POS_IMP_SUM_2PI]
4670 let WEDGE_GE_COMPLEMENT = prove_by_refinement(
4672 ~(azim u0 u1 v1 v2 = &0) ==>
4673 (:real^3) DIFF wedge_ge u0 u1 v1 v2 = wedge u0 u1 v2 v1`,
4676 REWRITE_TAC[EXTENSION;wedge;Local_lemmas.WEDGE_GE_AZIM_LE;IN_DIFF;IN_UNIV;IN_ELIM_THM];
4677 REWRITE_TAC[arith `~(x <= y) <=> (y < x)`];
4678 REPEAT WEAK_STRIP_TAC;
4679 TYPIFY `~(collinear {u0,u1,v1}) /\ ~collinear {u0,u1,v2}` (C SUBGOAL_THEN ASSUME_TAC);
4680 BY(ASM_MESON_TAC[AZIM_DEGENERATE]);
4681 TYPIFY `collinear {u0,u1,x}` ASM_CASES_TAC;
4683 ASM_SIMP_TAC[AZIM_DEGENERATE;arith `~(x < &0) <=> &0 <= x`];
4684 BY(REWRITE_TAC[Local_lemmas.AZIM_RANGE]);
4686 TYPIFY `&0 < azim u0 u1 v1 v2` (C SUBGOAL_THEN ASSUME_TAC);
4687 BY(ASM_SIMP_TAC[arith `~(x = &0) ==> (&0 < x <=> &0 <= x)`;Local_lemmas.AZIM_RANGE]);
4688 REWRITE_TAC[TAUT `(a <=> b) <=> ((a ==> b) /\ (b ==> a))`];
4690 REPEAT WEAK_STRIP_TAC;
4691 INTRO_TAC Fan.sum4_azim_fan [`u0`;`u1`;`v1`;`v2`;`x`];
4692 ASM_SIMP_TAC[arith `x < y ==> x <= y`];
4693 INTRO_TAC AZIM_POS_IMP_SUM_2PI_ALT [`u0`;`u1`;`v1`;`v2`];
4694 INTRO_TAC Local_lemmas.AZIM_RANGE [`u0`;`u1`;`v1`;`x`];
4695 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
4696 REPEAT WEAK_STRIP_TAC;
4697 INTRO_TAC Fan.sum4_azim_fan [`u0`;`u1`;`v2`;`x`;`v1`];
4698 ASM_SIMP_TAC[arith `x < y ==> x <= y`];
4699 INTRO_TAC AZIM_POS_IMP_SUM_2PI_ALT [`u0`;`u1`;`v2`;`v1`];
4700 INTRO_TAC AZIM_POS_IMP_SUM_2PI_ALT [`u0`;`u1`;`x`;`v1`];
4701 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
4705 let WEDGE_COMPLEMENT = prove_by_refinement(
4706 `!u0 u1 v1 v2. ~(azim u0 u1 v1 v2 = &0) ==>
4707 (:real^3) DIFF wedge u0 u1 v1 v2 = wedge_ge u0 u1 v2 v1`,
4710 REPEAT WEAK_STRIP_TAC;
4711 TYPIFY `~(azim u0 u1 v2 v1 = &0)` (C SUBGOAL_THEN ASSUME_TAC);
4712 BY(ASM_MESON_TAC[Local_lemmas.AZIM_EQ_0_SYM2]);
4713 INTRO_TAC WEDGE_GE_COMPLEMENT [`u0`;`u1`;`v2`;`v1`];
4719 let EWYBJUA = prove_by_refinement(
4720 `!u0 u1 v1 v2 V X. saturated V /\ packing V /\ leaf V [u0;u1;v1] /\ leaf V [u0;u1;v2] /\
4722 {u0,u1} IN edgeX V X /\
4723 ~(azim u0 u1 v1 v2 = &0) ==>
4724 (X SUBSET wedge_ge u0 u1 v1 v2) \/ (X SUBSET wedge_ge u0 u1 v2 v1)`,
4727 REPEAT WEAK_STRIP_TAC;
4728 TYPIFY `~(X INTER wedge u0 u1 v1 v2 = {})` ASM_CASES_TAC;
4730 MATCH_MP_TAC BDXKHTW;
4731 TYPIFY `V` EXISTS_TAC;
4733 BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]);
4734 TYPIFY `~(X INTER wedge u0 u1 v2 v1 = {})` ASM_CASES_TAC;
4736 MATCH_MP_TAC BDXKHTW;
4737 TYPIFY `V` EXISTS_TAC;
4740 BY(ASM_MESON_TAC[Local_lemmas.AZIM_EQ_0_SYM2]);
4741 BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]);
4743 TYPIFY `~collinear {u0,u1,v1}` (C SUBGOAL_THEN ASSUME_TAC);
4744 INTRO_TAC GBEWYFX [`V`;`[u0;u1;v1]`];
4746 GMATCH_SIMP_TAC set_of_list3;
4747 ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`];
4748 BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
4749 TYPIFY `~collinear {u0,u1,v2}` (C SUBGOAL_THEN ASSUME_TAC);
4750 INTRO_TAC GBEWYFX [`V`;`[u0;u1;v2]`];
4752 GMATCH_SIMP_TAC set_of_list3;
4753 ASM_REWRITE_TAC[EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`];
4754 BY(ASM_MESON_TAC[leaf;IN;Sphere.BARV;arith `2 + 1 = 3`]);
4755 TYPIFY `NULLSET X` ASM_CASES_TAC;
4756 FIRST_X_ASSUM_ST `mcell_set` MP_TAC;
4757 REWRITE_TAC[Pack_defs.mcell_set;IN_ELIM_THM];
4758 REPEAT WEAK_STRIP_TAC;
4759 INTRO_TAC Bump.RIJRIED [`V`;`ul`;`i`];
4762 BY(ASM_MESON_TAC[]);
4764 BY(ASM_MESON_TAC[NOT_IN_EMPTY]);
4765 ABBREV_TAC `(s:real^3->bool) = aff_ge {u0,u1} {v1} UNION aff_ge {u0,u1} {v2}`;
4766 TYPIFY `NULLSET s` (C SUBGOAL_THEN ASSUME_TAC);
4768 MATCH_MP_TAC (CONJUNCT2 NULLSET_RULES);
4769 BY(ASM_SIMP_TAC[Conforming.NEGLIGIBLE_AFF_GE_2_1]);
4770 TYPIFY `X SUBSET aff_ge {u0,u1} {v1} UNION aff_ge {u0,u1} {v2}` ASM_CASES_TAC;
4771 BY(ASM_MESON_TAC[NEGLIGIBLE_SUBSET]);
4772 TYPIFY `?x. x IN X DIFF s` (C SUBGOAL_THEN MP_TAC);
4773 FIRST_X_ASSUM MP_TAC;
4776 REPEAT WEAK_STRIP_TAC;
4777 TYPIFY `~(u0 = u1)` (C SUBGOAL_THEN ASSUME_TAC);
4778 FIRST_X_ASSUM_ST `~collinear t` MP_TAC;
4779 BY(MESON_TAC[Collect_geom.NOT_COLLINEAR_IMP_2_UNEQUAL]);
4780 TYPIFY `collinear {u0,u1,x}` ASM_CASES_TAC;
4781 INTRO_TAC COLLINEAR_3_IN_AFFINE_HULL [`u0`;`u1`;`x`];
4783 TYPIFY `affine hull {u0,u1} SUBSET aff_ge {u0,u1} {v1}` ENOUGH_TO_SHOW_TAC;
4784 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
4785 MATCH_MP_TAC AFFINE_HULL_SUBSET_AFF_GE;
4786 MATCH_MP_TAC Fan.th3a;
4787 BY(ASM_REWRITE_TAC[]);
4788 REPEAT (FIRST_X_ASSUM_ST `INTER` MP_TAC);
4789 REWRITE_TAC[EXTENSION;IN_INTER;NOT_IN_EMPTY];
4790 (DISCH_THEN (C INTRO_TAC [`x`]));
4791 FIRST_X_ASSUM_ST `DIFF` MP_TAC;
4792 REWRITE_TAC[IN_DIFF];
4796 TYPIFY `x IN wedge_ge u0 u1 v2 v1` (C SUBGOAL_THEN ASSUME_TAC);
4797 INTRO_TAC WEDGE_COMPLEMENT [`u0`;`u1`;`v1`;`v2`];
4798 ASM_REWRITE_TAC[EXTENSION;IN_DIFF;IN_UNIV];
4799 BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
4800 (DISCH_THEN (C INTRO_TAC [`x`]));
4803 INTRO_TAC WEDGE_WEDGE_GE [`u0`;`u1`;`v2`;`v1`];
4805 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[])