1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
10 (* REDO THE beta_bump *)
20 `!(P:A->bool) (Q:A->bool). (Q ((@) P)) <=> (\t. Q t) ((@) P)`,MESON_TAC[]) in
21 let unbeta_tac = CONV_TAC (HIGHER_REWRITE_CONV[unbeta] true) in
22 unbeta_tac THEN (MATCH_MP_TAC Tactics.SELECT_THM) THEN BETA_TAC THEN
23 REPEAT WEAK_STRIP_TAC;;
25 let BETA_ORDERED_PAIR_THM = prove_by_refinement(
27 ((\ ( u, v). g u v) x = g (FST x) (SND x))`,
31 INTRO_TAC (GSYM PAIR) [`x`];
32 DISCH_THEN SUBST1_TAC;
33 BY(REWRITE_TAC[GABS_DEF;GEQ_DEF])
37 let BIJ_SUM = prove_by_refinement(
38 `!(A:A->bool) (B:B->bool) f ab.
39 BIJ ab A B ==> (sum A (f o ab) = sum B f)`,
43 BY(ASM_MESON_TAC[ SUM_IMAGE ; Misc_defs_and_lemmas.SURJ_IMAGE ])
47 let EL_EXPLICIT = prove_by_refinement(
48 `!h t. EL 0 (CONS (h:a) t) = h /\
49 EL 1 (CONS h t) = EL 0 t /\
50 EL 2 (CONS h t) = EL 1 t /\
51 EL 3 (CONS h t) = EL 2 t /\
52 EL 4 (CONS h t) = EL 3 t /\
53 EL 5 (CONS h t) = EL 4 t /\
54 EL 6 (CONS h t) = EL 5 t`,
57 BY(REWRITE_TAC[EL;HD;TL;arith `6 = SUC 5 /\ 5 = SUC 4 /\ 4 = SUC 3 /\ 3 = SUC 2 /\ 2 = SUC 1 /\ 1 = SUC 0`])
61 let LENGTH1 = prove_by_refinement(
62 `!ul:(A) list. LENGTH ul = 1 ==> ul = [EL 0 ul]`,
65 REWRITE_TAC[LENGTH_EQ_CONS;arith `1 = SUC 0`;LENGTH_EQ_NIL];
66 REPEAT WEAK_STRIP_TAC;
67 BY(ASM_REWRITE_TAC[EL;HD])
71 let LENGTH2 = prove_by_refinement(
72 `!ul:(A) list. LENGTH ul = 2 ==> ul = [EL 0 ul;EL 1 ul]`,
75 REWRITE_TAC[LENGTH_EQ_CONS;arith `2 = SUC 1`];
76 REPEAT WEAK_STRIP_TAC;
78 FIRST_X_ASSUM (unlist ONCE_REWRITE_TAC o (MATCH_MP LENGTH1));
79 BY(REWRITE_TAC[EL;HD;arith `1 = SUC 0`;TL])
83 let LENGTH3 = prove_by_refinement(
84 `!(ul:(A)list). LENGTH ul = 3 ==> ul = [EL 0 ul; EL 1 ul; EL 2 ul]`,
87 REWRITE_TAC[LENGTH_EQ_CONS;arith `3 = SUC 2`];
88 REPEAT WEAK_STRIP_TAC;
90 FIRST_X_ASSUM (unlist ONCE_REWRITE_TAC o (MATCH_MP LENGTH2));
91 BY(REWRITE_TAC[EL;HD;arith `1 = SUC 0`;arith `2 = SUC 1`;TL])
95 let LENGTH4 = prove_by_refinement(
96 `!(ul:(A)list). LENGTH ul = 4 ==> ul = [EL 0 ul; EL 1 ul; EL 2 ul; EL 3 ul]`,
99 REWRITE_TAC[LENGTH_EQ_CONS;arith `4 = SUC 3`];
100 REPEAT WEAK_STRIP_TAC;
102 FIRST_X_ASSUM (unlist ONCE_REWRITE_TAC o (MATCH_MP LENGTH3));
103 BY(REWRITE_TAC[EL;HD;arith `1 = SUC 0`;arith `2 = SUC 1`;arith `3 = SUC 2`;TL])
107 let set_of_list2 = prove_by_refinement(
108 `!(ul:(A) list). LENGTH ul = 2 ==> set_of_list ul = {EL 0 ul, EL 1 ul}`,
111 REPEAT WEAK_STRIP_TAC;
112 FIRST_X_ASSUM (MP_TAC o (MATCH_MP LENGTH2));
113 ABBREV_TAC `a:A = EL 0 ul`;
114 ABBREV_TAC `b:A = EL 1 ul`;
115 DISCH_THEN SUBST1_TAC;
116 BY(REWRITE_TAC[set_of_list])
120 let set_of_list2_explicit = prove_by_refinement(
121 `!(a:A) b. set_of_list [a;b] = {a,b}`,
124 REPEAT WEAK_STRIP_TAC;
125 GMATCH_SIMP_TAC set_of_list2;
126 BY(REWRITE_TAC[LENGTH;EL;HD;TL;arith `1 = SUC 0 /\ 2 = SUC 1`])
130 let set_of_list3 = prove_by_refinement(
131 `!(ul:(A) list). LENGTH ul = 3 ==> set_of_list ul = {EL 0 ul, EL 1 ul, EL 2 ul}`,
134 REPEAT WEAK_STRIP_TAC;
135 FIRST_X_ASSUM (MP_TAC o (MATCH_MP LENGTH3));
136 ABBREV_TAC `a:A = EL 0 ul`;
137 ABBREV_TAC `b:A = EL 1 ul`;
138 ABBREV_TAC `c:A = EL 2 ul`;
139 DISCH_THEN SUBST1_TAC;
140 BY(REWRITE_TAC[set_of_list])
144 let set_of_list3_explicit = prove_by_refinement(
145 `!(a:A) b c. set_of_list [a;b;c] = {a,b,c}`,
148 REPEAT WEAK_STRIP_TAC;
149 GMATCH_SIMP_TAC set_of_list3;
150 BY(REWRITE_TAC[EL;HD;TL;arith `2 = SUC 1 /\ 1 = SUC 0 /\ 3 = SUC 2 /\ 4 = SUC 3`;LENGTH])
154 let set_of_list4 = prove_by_refinement(
155 `!(ul:(A) list). LENGTH ul = 4 ==> set_of_list ul = {EL 0 ul, EL 1 ul, EL 2 ul, EL 3 ul}`,
158 REPEAT WEAK_STRIP_TAC;
159 FIRST_X_ASSUM (MP_TAC o (MATCH_MP LENGTH4));
160 ABBREV_TAC `a:A = EL 0 ul`;
161 ABBREV_TAC `b:A = EL 1 ul`;
162 ABBREV_TAC `c:A = EL 2 ul`;
163 ABBREV_TAC `d:A = EL 3 ul`;
164 DISCH_THEN SUBST1_TAC;
165 BY(REWRITE_TAC[set_of_list])
169 let set_of_list4_explicit = prove_by_refinement(
170 `!(a:A) b c d. set_of_list [a;b;c;d] = {a,b,c,d}`,
173 REPEAT WEAK_STRIP_TAC;
174 GMATCH_SIMP_TAC set_of_list4;
175 BY(REWRITE_TAC[EL;HD;TL;arith `2 = SUC 1 /\ 1 = SUC 0 /\ 3 = SUC 2 /\ 4 = SUC 3`;LENGTH])
179 let SET_OF_LIST_TRUNCATE_1 = prove_by_refinement(
180 `!(ul:(A)list). 2 <= LENGTH ul ==> set_of_list (truncate_simplex 1 ul) = {EL 0 ul,EL 1 ul}`,
183 REPEAT WEAK_STRIP_TAC;
184 GMATCH_SIMP_TAC set_of_list2;
186 REWRITE_TAC[arith `2 = 1 + 1`];
187 MATCH_MP_TAC Packing3.LENGTH_TRUNCATE_SIMPLEX;
188 BY(ASM_REWRITE_TAC[arith `1 + 1 =2`]);
189 REPEAT (GMATCH_SIMP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
190 BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC)
194 let SET_OF_LIST_TRUNCATE_2 = prove_by_refinement(
195 `!(ul:(A)list). 3 <= LENGTH ul ==> set_of_list (truncate_simplex 2 ul) = {EL 0 ul,EL 1 ul,EL 2 ul}`,
198 REPEAT WEAK_STRIP_TAC;
199 GMATCH_SIMP_TAC set_of_list3;
201 REWRITE_TAC[arith `3 = 2 + 1`];
202 MATCH_MP_TAC Packing3.LENGTH_TRUNCATE_SIMPLEX;
203 BY(ASM_REWRITE_TAC[arith `2 + 1 =3`]);
204 REPEAT (GMATCH_SIMP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
206 BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC)
211 let VX_EMPTY = prove_by_refinement(
212 `!V vl k. (NULLSET (mcell k V vl)) ==> (VX V (mcell k V vl) = {})`,
215 REPEAT WEAK_STRIP_TAC;
216 BY(ASM_REWRITE_TAC[Pack_defs.VX])
220 let RIJRIED = prove_by_refinement(
221 `!V vl k. (NULLSET (mcell k V vl)) ==> (edgeX V (mcell k V vl) = {})`,
224 REPEAT WEAK_STRIP_TAC;
225 REWRITE_TAC[Pack_defs.edgeX];
226 INTRO_TAC VX_EMPTY[`V`;`vl`;`k`];
227 ASM_SIMP_TAC[EXTENSION;IN_ELIM_THM;NOT_IN_EMPTY];
232 let HDTFNFZ_SUBSET = prove_by_refinement(
238 ==> VX V X SUBSET V INTER X`,
241 REPEAT WEAK_STRIP_TAC;
242 TYPIFY `NULLSET X` ASM_CASES_TAC;
243 BY(ASM_MESON_TAC[EMPTY_SUBSET;VX_EMPTY]);
244 BY(ASM_MESON_TAC[Hdtfnfz.HDTFNFZ;SUBSET_REFL])
248 let HDTFNFZ_ALT = prove_by_refinement(
255 ==> VX V X = V INTER X`,
258 ASM_MESON_TAC[Hdtfnfz.HDTFNFZ]
262 let VORONOI_V = prove_by_refinement(
263 `!V (w:real^A). w IN V ==> (V INTER voronoi_closed V w = {w})`,
266 REWRITE_TAC[Sphere.voronoi_closed;EXTENSION;IN_SING;IN_INTER;IN_ELIM_THM];
268 REPEAT WEAK_STRIP_TAC;
269 BY(ASM_MESON_TAC[DIST_EQ_0;arith `x <= &0 /\ &0 <= x ==> x = &0`;DIST_POS_LE])
273 let V_CELL0_EMPTY = prove_by_refinement(
274 `!V vl. saturated V /\ packing V /\ barV V 3 vl ==> V INTER (mcell0 V vl) = {}`,
277 REPEAT WEAK_STRIP_TAC;
278 REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER;Pack_defs.mcell0;IN_DIFF];
279 REPEAT WEAK_STRIP_TAC;
280 INTRO_TAC Marchal_cells_3.ROGERS_SUBSET_VORONOI_CLOSED [`V`;`vl`];
283 INTRO_TAC VORONOI_V [`V`;`HD vl`];
284 REWRITE_TAC[EXTENSION;IN_SING;IN_INTER];
285 TYPIFY `x = HD vl` ASM_CASES_TAC;
286 FIRST_X_ASSUM_ST `ball` MP_TAC;
288 ASM_REWRITE_TAC[ball;IN_ELIM_THM;DIST_REFL];
289 MATCH_MP_TAC (TAUT `a ==> (~a ==> b)`);
290 GMATCH_SIMP_TAC REAL_LT_RSQRT;
292 DISCH_THEN ( MP_TAC);
294 BY(ASM_MESON_TAC[Packing3.BARV_SUBSET;SUBSET;IN;Packing3.BARV_IMP_HD_IN_SET_OF_LIST]);
295 DISCH_THEN (C INTRO_TAC [`x`]);
296 BY(ASM_MESON_TAC[SUBSET])
300 let V_CELL1_SINGLE = prove_by_refinement(
301 `!V vl. saturated V /\ packing V /\ barV V 3 vl ==> V INTER (mcell1 V vl) SUBSET {HD vl}`,
304 REPEAT WEAK_STRIP_TAC;
305 REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER;Pack_defs.mcell1;IN_DIFF;SUBSET;IN_SING];
306 REPEAT WEAK_STRIP_TAC;
307 FIRST_X_ASSUM MP_TAC;
310 TYPIFY `x IN cball(HD vl,sqrt(&2))` (C SUBGOAL_THEN MP_TAC);
311 FIRST_X_ASSUM MP_TAC;
313 REWRITE_TAC[cball;IN_ELIM_THM];
314 TYPIFY `sqrt(&2) < sqrt(&4)` (C SUBGOAL_THEN MP_TAC);
315 GMATCH_SIMP_TAC SQRT_MONO_LT_EQ;
317 REWRITE_TAC[Collect_geom2.SQRT4_EQ2];
318 FIRST_X_ASSUM_ST `packing` MP_TAC;
319 REWRITE_TAC[Sphere.packing];
320 TYPIFY `HD vl IN V` (C SUBGOAL_THEN ASSUME_TAC);
321 BY(ASM_MESON_TAC[Packing3.BARV_SUBSET;SUBSET;IN;Packing3.BARV_IMP_HD_IN_SET_OF_LIST]);
322 BY(ASM_MESON_TAC[IN;arith `&2 <= d /\ d <= s /\ s < &2 ==> F`]);
323 BY(REWRITE_TAC[NOT_IN_EMPTY])
327 let EDGE_IMP_K2 = prove_by_refinement(
328 `!V vl k. saturated V /\ packing V /\ barV V 3 vl /\ (k <= 1) ==> (edgeX V (mcell k V vl) = {})`,
331 REPEAT WEAK_STRIP_TAC;
332 ASM_REWRITE_TAC[EXTENSION;Pack_defs.mcell;NOT_IN_EMPTY;Pack_defs.edgeX;IN_ELIM_THM;IN_INSERT];
333 REPEAT WEAK_STRIP_TAC;
334 REPEAT (FIRST_X_ASSUM_ST `mcell0` MP_TAC);
336 INTRO_TAC V_CELL0_EMPTY [`V`;`vl`];
337 INTRO_TAC HDTFNFZ_SUBSET [`V`;`vl`;`0`;`mcell 0 V vl`];
338 ASM_REWRITE_TAC[Pack_defs.mcell];
340 TYPIFY `k=1` (C SUBGOAL_THEN ASSUME_TAC);
341 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
343 INTRO_TAC HDTFNFZ_SUBSET [`V`;`vl`;`1`;`mcell 1 V vl`];
344 ASM_REWRITE_TAC[Pack_defs.mcell;arith `~(1=0)`];
345 INTRO_TAC V_CELL1_SINGLE [`V`;`vl`];
347 REWRITE_TAC[SUBSET;IN_SING;IN_INTER];
348 REPEAT WEAK_STRIP_TAC;
349 BY(ASM_MESON_TAC[IN])
356 (* 2 CELL EXPLICIT *)
358 let MCELL2_VERTEX = prove_by_refinement(
359 `!V ul. saturated V /\ packing V /\ barV V 3 ul ==>
360 VX V (mcell2 V ul) SUBSET {EL 0 ul,EL 1 ul}`,
364 REPEAT WEAK_STRIP_TAC;
365 TYPIFY `set_of_list (truncate_simplex 1 ul) = {EL 0 ul, EL 1 ul}` (C SUBGOAL_THEN ASSUME_TAC);
366 TYPIFY `LENGTH ul = 4` (C SUBGOAL_THEN MP_TAC);
367 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3+1 = 4`]);
368 DISCH_THEN (MP_TAC o (MATCH_MP LENGTH4));
369 BY(MESON_TAC[Marchal_cells.TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list2_explicit]);
370 INTRO_TAC Rogers.XYOFCGX [`V`;`{EL 0 ul,EL 1 ul}`;`circumcenter {EL 0 ul,EL 1 ul}`];
371 INTRO_TAC Urrphbz1.MCELL_2_PROPERTIES_lemma1 [`V`;`ul`;`0`;`x`];
372 INTRO_TAC HDTFNFZ_SUBSET [`V`;`ul`;`2`;`mcell2 V ul`];
375 BY(REWRITE_TAC[Pack_defs.mcell;arith `~(2 = 0) /\ ~(2 = 1)`]);
377 TYPIFY `x IN V /\ x IN mcell2 V ul` (C SUBGOAL_THEN MP_TAC);
378 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
382 REWRITE_TAC[Rogers.CIRCUMCENTER_2];
385 MATCH_MP_TAC SUBSET_TRANS;
386 TYPIFY `set_of_list ul` EXISTS_TAC;
388 GMATCH_SIMP_TAC set_of_list4;
391 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`]);
392 BY(ASM_MESON_TAC[Packing3.BARV_SUBSET]);
394 BY(REWRITE_TAC[AFFINE_INDEPENDENT_2]);
395 FIRST_X_ASSUM_ST `mcell2` MP_TAC;
396 REWRITE_TAC[Pack_defs.mcell2];
397 REWRITE_TAC[Pack_defs.HL];
398 COND_CASES_TAC THEN REWRITE_TAC[NOT_IN_EMPTY];
400 FIRST_X_ASSUM MP_TAC;
401 MATCH_MP_TAC (arith `x = x' ==> (x < y /\ z ==> x' < y)`);
402 BY(ASM_REWRITE_TAC[]);
403 REWRITE_TAC[IN_DIFF];
404 DISCH_THEN (C INTRO_TAC [`EL 0 ul`;`x`]);
405 REPEAT WEAK_STRIP_TAC;
407 FIRST_X_ASSUM_ST `dist` MP_TAC;
411 FIRST_X_ASSUM_ST `dist` (MP_TAC o (ONCE_REWRITE_RULE[DIST_SYM]));
412 TYPIFY ` hl(truncate_simplex 1 ul) = dist(HD ul,midpoint (HD ul,HD (TL ul)))` ENOUGH_TO_SHOW_TAC;
413 DISCH_THEN SUBST1_TAC;
414 REWRITE_TAC[EL;arith `1 = SUC 0`];
416 TYPIFY ` (truncate_simplex 1 ul) = [EL 0 ul; EL 1 ul]` (C SUBGOAL_THEN SUBST1_TAC);
417 TYPIFY `LENGTH ul = 4` (C SUBGOAL_THEN MP_TAC);
418 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3+1 = 4`]);
419 DISCH_THEN (MP_TAC o (MATCH_MP LENGTH4));
420 BY(MESON_TAC[Marchal_cells.TRUNCATE_SIMPLEX_EXPLICIT_1]);
421 ASM_REWRITE_TAC[Marchal_cells_3.HL_2];
422 REWRITE_TAC[DIST_MIDPOINT];
423 REWRITE_TAC[EL;arith `1 = SUC 0`];
428 let MCELL2_EDGE = prove_by_refinement(
429 `!V ul e. saturated V /\ packing V /\ barV V 3 ul /\ edgeX V (mcell2 V ul) e ==>
430 e = {EL 0 ul, EL 1 ul}`,
433 REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM];
434 REPEAT WEAK_STRIP_TAC;
435 INTRO_TAC MCELL2_VERTEX [`V`;`ul`];
437 REWRITE_TAC[Geomdetail.PAIR_EQ_EXPAND];
438 REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
440 FIRST_ASSUM (C INTRO_TAC [`u`]);
441 FIRST_X_ASSUM (C INTRO_TAC [`v`]);
442 BY(ASM_MESON_TAC[IN])
446 (* 3 AND 4 CELL EXPLICIT *)
448 let MCELL4 = prove_by_refinement(
449 `!V ul. mcell4 V ul = mcell 4 V ul`,
452 BY(REWRITE_TAC[Pack_defs.mcell;arith `~(4 =0) /\ ~(4 = 1) /\ ~(4=2) /\ ~(4=3)`])
456 let MCELL3 = prove_by_refinement(
457 `!V ul. mcell3 V ul = mcell 3 V ul`,
460 BY(REWRITE_TAC[Pack_defs.mcell;arith `~(3 =0) /\ ~(3 = 1) /\ ~(3=2)`])
464 let MCELL2 = prove_by_refinement(
465 `!V ul. mcell2 V ul = mcell 2 V ul`,
468 BY(REWRITE_TAC[Pack_defs.mcell;arith `~(2 =0) /\ ~(2 = 1)`])
472 let MCELL1 = prove_by_refinement(
473 `!V ul. mcell1 V ul = mcell 1 V ul`,
476 BY(REWRITE_TAC[Pack_defs.mcell;arith `~(1 =0)`])
480 let MCELL0 = prove_by_refinement(
481 `!V ul. mcell0 V ul = mcell 0 V ul`,
484 BY(REWRITE_TAC[Pack_defs.mcell;arith `~(1 =0)`])
488 let MCELL_CELL_PARAMETERS_EXIST = prove_by_refinement(
489 `!V ul k X. (k <= 4) /\ packing V /\ saturated V /\ (X = mcell k V ul) /\ ul IN barV V 3 /\ ~NULLSET X ==>
490 FST (cell_params V X) = k`,
493 REWRITE_TAC[Pack_defs.cell_params];
494 REPEAT WEAK_STRIP_TAC;
495 SELECT_TAC THEN (REPEAT (FIRST_X_ASSUM MP_TAC)) THEN (REWRITE_TAC[BETA_ORDERED_PAIR_THM]);
496 INTRO_TAC Ajripqn.AJRIPQN [`V`;`ul`;`SND t`;`k`;`FST t`];
497 REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY;arith `x = 0 \/ x = 1 \/ x = 2 \/ x = 3 \/ x = 4 <=> x <= 4`];
499 REPEAT WEAK_STRIP_TAC;
500 FIRST_X_ASSUM_ST `==>` MP_TAC;
503 BY(ASM_MESON_TAC[INTER_IDEMPOT]);
504 BY(DISCH_THEN (unlist REWRITE_TAC));
505 REPEAT WEAK_STRIP_TAC;
506 FIRST_X_ASSUM MP_TAC;
507 REWRITE_TAC[NOT_EXISTS_THM];
508 DISCH_THEN (C INTRO_TAC [`k,ul`]);
509 BY(ASM_REWRITE_TAC[])
513 let MCELL4_CELL_PARAMETERS_EXIST = prove_by_refinement(
514 `!V ul X. packing V /\ saturated V /\ (X = mcell4 V ul) /\ ul IN barV V 3 /\ ~NULLSET X ==>
515 FST (cell_params V X) = 4`,
518 REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_CELL_PARAMETERS_EXIST THEN ASM_REWRITE_TAC[MCELL4;arith `4 <= 4`];
523 let MCELL3_CELL_PARAMETERS_EXIST = prove_by_refinement(
524 `!V ul X. packing V /\ saturated V /\ (X = mcell3 V ul) /\ ul IN barV V 3 /\ ~NULLSET X ==>
525 FST (cell_params V X) = 3`,
528 REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_CELL_PARAMETERS_EXIST THEN ASM_REWRITE_TAC[MCELL3;arith `3 <= 4`];
533 let MCELL2_CELL_PARAMETERS_EXIST = prove_by_refinement(
534 `!V ul X. packing V /\ saturated V /\ (X = mcell2 V ul) /\ ul IN barV V 3 /\ ~NULLSET X ==>
535 FST (cell_params V X) = 2`,
538 REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_CELL_PARAMETERS_EXIST THEN ASM_REWRITE_TAC[MCELL2;arith `2 <= 4`];
543 let MCELL_PARAM_UL = prove_by_refinement(
544 `!V ul vl X k. (k<= 4) /\ packing V /\ saturated V /\ (X = mcell k V ul) /\ ul IN barV V 3 /\ ~NULLSET X /\
545 vl = SND (cell_params V X) ==>
546 (X = mcell k V vl /\ vl IN barV V 3)`,
549 REWRITE_TAC[Pack_defs.cell_params];
550 REPEAT WEAK_STRIP_TAC;
551 INTRO_TAC MCELL_CELL_PARAMETERS_EXIST [`V`;`ul`;`k`;`X`];
553 REWRITE_TAC[Pack_defs.cell_params];
554 WEAK_SELECT_TAC THEN (REPEAT (FIRST_X_ASSUM MP_TAC)) THEN (REWRITE_TAC[BETA_ORDERED_PAIR_THM]);
555 WEAK_SELECT_TAC THEN (REPEAT (FIRST_X_ASSUM MP_TAC)) THEN (REWRITE_TAC[BETA_ORDERED_PAIR_THM]);
556 REPEAT WEAK_STRIP_TAC;
559 REPEAT WEAK_STRIP_TAC;
562 REWRITE_TAC[NOT_EXISTS_THM];
563 DISCH_THEN (C INTRO_TAC [`k,ul`]);
564 BY(ASM_MESON_TAC[FST;SND])
568 let MCELL4_PARAM_UL = prove_by_refinement(
569 `!V ul vl X. packing V /\ saturated V /\ (X = mcell4 V ul) /\ ul IN barV V 3 /\ ~NULLSET X /\
570 vl = SND (cell_params V X) ==>
571 (X = mcell4 V (vl) /\ vl IN barV V 3)`,
575 REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_PARAM_UL;
576 BY(ASM_MESON_TAC[arith `4 <= 4`])
580 let MCELL3_PARAM_UL = prove_by_refinement(
581 `!V ul vl X. packing V /\ saturated V /\ (X = mcell3 V ul) /\ ul IN barV V 3 /\ ~NULLSET X /\
582 vl = SND (cell_params V X) ==>
583 (X = mcell3 V (vl) /\ vl IN barV V 3)`,
587 REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_PARAM_UL;
588 BY(ASM_MESON_TAC[arith `3 <= 4`])
592 let MCELL2_PARAM_UL = prove_by_refinement(
593 `!V ul vl X. packing V /\ saturated V /\ (X = mcell2 V ul) /\ ul IN barV V 3 /\ ~NULLSET X /\
594 vl = SND (cell_params V X) ==>
595 (X = mcell2 V (vl) /\ vl IN barV V 3)`,
599 REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_PARAM_UL;
600 BY(ASM_MESON_TAC[arith `2 <= 4`])
604 let MCELL4_VX = prove_by_refinement(
605 `!V ul X. packing V /\ saturated V /\ (X = mcell4 V ul) /\ ul IN barV V 3 ==>
606 VX V X SUBSET (set_of_list (SND (cell_params V X)))`,
609 REWRITE_TAC[Pack_defs.VX];
610 REPEAT WEAK_STRIP_TAC;
612 BY(REWRITE_TAC[EMPTY_SUBSET]);
613 REWRITE_TAC[LET_DEF;LET_END_DEF];
614 REWRITE_TAC[BETA_ORDERED_PAIR_THM];
615 INTRO_TAC MCELL4_CELL_PARAMETERS_EXIST [`V`;`ul`;`X`];
618 ASM_REWRITE_TAC[arith `~(4 = 0) /\ 4 - 1 = 3`];
619 MATCH_MP_TAC (MESON[SUBSET_REFL] `a = b ==> a SUBSET b`);
621 INTRO_TAC MCELL4_PARAM_UL [`V`;`ul`;`SND (cell_params V X)`;`X`];
623 REPEAT WEAK_STRIP_TAC;
624 MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_REFL;
625 BY(ASM_MESON_TAC[Sphere.BARV;IN])
629 let MCELL3_VX = prove_by_refinement(
630 `!V ul X. packing V /\ saturated V /\ (X = mcell3 V ul) /\ ul IN barV V 3 ==>
631 VX V X SUBSET (set_of_list (truncate_simplex 2 (SND (cell_params V X))))`,
634 REWRITE_TAC[Pack_defs.VX];
635 REPEAT WEAK_STRIP_TAC;
637 BY(REWRITE_TAC[EMPTY_SUBSET]);
638 REWRITE_TAC[LET_DEF;LET_END_DEF];
639 REWRITE_TAC[BETA_ORDERED_PAIR_THM];
640 INTRO_TAC MCELL3_CELL_PARAMETERS_EXIST [`V`;`ul`;`X`];
643 ASM_REWRITE_TAC[arith `~(3 = 0) /\ 2 = 3 - 1`];
648 let MCELL4_SET_OF_LIST_VX = prove_by_refinement(
649 `!V ul X. packing V /\ saturated V /\ (X = mcell4 V ul) /\ ~(NULLSET X) /\ barV V 3 ul ==>
650 set_of_list ul = V INTER X`,
653 REPEAT WEAK_STRIP_TAC;
654 TYPIFY `set_of_list ul SUBSET V INTER X /\ V INTER X = VX V X /\ VX V X SUBSET set_of_list (SND (cell_params V X)) /\ CARD (set_of_list (SND (cell_params V X))) <= 4 /\ CARD (set_of_list ul) = 4` ENOUGH_TO_SHOW_TAC;
655 REPEAT WEAK_STRIP_TAC;
656 TYPIFY `set_of_list ul = set_of_list (SND (cell_params V X))` ENOUGH_TO_SHOW_TAC;
657 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
658 MATCH_MP_TAC CARD_SUBSET_LE;
660 BY(REWRITE_TAC[FINITE_SET_OF_LIST]);
662 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
663 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
665 REWRITE_TAC[SUBSET_INTER];
667 MATCH_MP_TAC Packing3.BARV_SUBSET;
669 FIRST_X_ASSUM_ST `NULLSET` MP_TAC;
670 ASM_REWRITE_TAC[Pack_defs.mcell4];
672 BY(REWRITE_TAC[HULL_SUBSET]);
673 BY(REWRITE_TAC[NEGLIGIBLE_EMPTY]);
676 BY(ASM_MESON_TAC[HDTFNFZ_ALT;MCELL4]);
678 MATCH_MP_TAC MCELL4_VX;
679 BY(ASM_MESON_TAC[IN]);
681 TYPIFY `LENGTH (SND (cell_params V X)) = 4` ENOUGH_TO_SHOW_TAC;
682 BY(MESON_TAC[Geomdetail.CARD_SET_OF_LIST_LE]);
683 INTRO_TAC MCELL4_PARAM_UL [`V`;`ul`;`SND(cell_params V X)`;`X`];
686 BY(ASM_REWRITE_TAC[IN]);
687 BY(MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`]);
688 REWRITE_TAC[arith `4 = 3 + 1`];
689 MATCH_MP_TAC Marchal_cells_3.BARV_CARD_LEMMA;
694 let MCELL3_SET_OF_LIST_VX = prove_by_refinement(
695 `!V ul X. packing V /\ saturated V /\ (X = mcell3 V ul) /\ ~(NULLSET X) /\ barV V 3 ul ==>
696 set_of_list (truncate_simplex 2 ul) = V INTER X`,
699 REPEAT WEAK_STRIP_TAC;
700 TYPIFY `set_of_list (truncate_simplex 2 ul) SUBSET V INTER X /\ V INTER X = VX V X /\ VX V X SUBSET set_of_list (truncate_simplex 2 (SND (cell_params V X))) /\ CARD (set_of_list (truncate_simplex 2 (SND (cell_params V X)))) <= 3 /\ CARD (set_of_list (truncate_simplex 2 ul)) = 3` ENOUGH_TO_SHOW_TAC;
701 REPEAT WEAK_STRIP_TAC;
702 TYPIFY `set_of_list (truncate_simplex 2 ul) = set_of_list (truncate_simplex 2 (SND (cell_params V X)))` ENOUGH_TO_SHOW_TAC;
703 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
704 MATCH_MP_TAC CARD_SUBSET_LE;
706 BY(REWRITE_TAC[FINITE_SET_OF_LIST]);
708 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
709 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
710 COMMENT "list of conjunts";
712 REWRITE_TAC[SUBSET_INTER];
714 MATCH_MP_TAC SUBSET_TRANS;
715 TYPIFY `set_of_list ul` EXISTS_TAC;
717 MATCH_MP_TAC Rogers.SET_OF_LIST_TRUNCATE_SIMPLEX_SUBSET;
718 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `2 + 1 <= 3 + 1`]);
719 MATCH_MP_TAC Packing3.BARV_SUBSET;
721 FIRST_X_ASSUM_ST `NULLSET` MP_TAC;
722 ASM_REWRITE_TAC[Pack_defs.mcell3];
725 MATCH_MP_TAC SUBSET_TRANS;
726 TYPIFY `set_of_list (truncate_simplex 2 ul) UNION {mxi V ul}` EXISTS_TAC;
729 BY(REWRITE_TAC[HULL_SUBSET]);
730 BY(REWRITE_TAC[NEGLIGIBLE_EMPTY]);
733 BY(ASM_MESON_TAC[HDTFNFZ_ALT;MCELL3]);
735 MATCH_MP_TAC MCELL3_VX;
736 BY(ASM_MESON_TAC[IN]);
738 TYPIFY `2+1 <= LENGTH (SND (cell_params V X))` ENOUGH_TO_SHOW_TAC;
739 BY(MESON_TAC[Geomdetail.CARD_SET_OF_LIST_LE;Packing3.LENGTH_TRUNCATE_SIMPLEX;arith `2+1= 3 /\ 2 + 1 <= 2+1`]);
740 INTRO_TAC MCELL3_PARAM_UL [`V`;`ul`;`SND(cell_params V X)`;`X`];
743 BY(ASM_REWRITE_TAC[IN]);
744 BY(MESON_TAC[Sphere.BARV;IN;arith `2 + 1 <= 3+1`]);
745 INTRO_TAC Marchal_cells_3.BARV_CARD_LEMMA [`V`;`ul`;`3`];
747 TYPIFY `LENGTH ul = 4` (C SUBGOAL_THEN ASSUME_TAC);
748 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`]);
749 FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP LENGTH4));
750 FIRST_X_ASSUM SUBST1_TAC;
751 REWRITE_TAC[Marchal_cells.TRUNCATE_SIMPLEX_EXPLICIT_2];
752 REWRITE_TAC[set_of_list3_explicit;set_of_list4_explicit];
753 TYPED_ABBREV_TAC `(s:real^3 -> bool) = {EL 0 ul, EL 1 ul, EL 2 ul}` ;
754 TYPIFY ` {EL 0 ul, EL 1 ul, EL 2 ul, EL 3 ul} = (EL 3 ul) INSERT s ` (C SUBGOAL_THEN SUBST1_TAC);
757 GMATCH_SIMP_TAC (CONJUNCT2 CARD_CLAUSES);
759 BY(ASM_MESON_TAC[FINITE_EMPTY;FINITE_INSERT]);
761 BY(ASM_MESON_TAC[Geomdetail.CARD3;arith `~( 3 + 1 <= 3)`]);
766 let MCELL4_EDGE = prove_by_refinement(
767 `!V ul u v. packing V /\ saturated V /\ ~NULLSET (mcell4 V ul) /\ barV V 3 ul ==>
768 ({u,v} IN edgeX V (mcell4 V ul) <=> (~(u= v) /\ {u,v} SUBSET set_of_list ul))`,
771 REPEAT WEAK_STRIP_TAC;
772 REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM];
773 INTRO_TAC HDTFNFZ_ALT [`V`;`ul`;`4`;`mcell4 V ul`];
775 BY(ASM_REWRITE_TAC[MCELL4]);
776 DISCH_THEN SUBST1_TAC;
777 INTRO_TAC (GSYM MCELL4_SET_OF_LIST_VX) [`V`;`ul`;`mcell4 V ul`];
779 BY(ASM_REWRITE_TAC[]);
780 DISCH_THEN SUBST1_TAC;
781 REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;Geomdetail.PAIR_EQ_EXPAND];
786 let MCELL3_EDGE = prove_by_refinement(
787 `!V ul u v. packing V /\ saturated V /\ ~NULLSET (mcell3 V ul) /\ barV V 3 ul ==>
788 ({u,v} IN edgeX V (mcell3 V ul) <=> (~(u= v) /\ {u,v} SUBSET (set_of_list(truncate_simplex 2 ul))))`,
791 REPEAT WEAK_STRIP_TAC;
792 REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM];
793 INTRO_TAC HDTFNFZ_ALT [`V`;`ul`;`3`;`mcell3 V ul`];
795 BY(ASM_REWRITE_TAC[MCELL3]);
796 DISCH_THEN SUBST1_TAC;
797 INTRO_TAC (GSYM MCELL3_SET_OF_LIST_VX) [`V`;`ul`;`mcell3 V ul`];
799 BY(ASM_REWRITE_TAC[]);
800 DISCH_THEN SUBST1_TAC;
801 REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;Geomdetail.PAIR_EQ_EXPAND];
806 let EDGE_MCELL_EL = prove_by_refinement(
807 `!V X e. e IN edgeX V X ==> (?u v. e = {u,v} /\ ~(u=v))`,
810 REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM];
816 let MCELL_EDGE = prove_by_refinement(
817 `!V ul k e. (k < 4) /\ packing V /\ saturated V /\ ~NULLSET (mcell k V ul) /\ barV V 3 ul /\
818 e IN edgeX V (mcell k V ul) ==> e SUBSET (set_of_list(truncate_simplex 2 ul))`,
821 REPEAT WEAK_STRIP_TAC;
822 TYPIFY `LENGTH ul = 4` (C SUBGOAL_THEN ASSUME_TAC);
823 BY(ASM_MESON_TAC[Sphere.BARV;arith `3 + 1 = 4`]);
824 TYPIFY `k = 3 \/ k = 2 \/ k <= 1` (C SUBGOAL_THEN MP_TAC);
825 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
826 INTRO_TAC EDGE_MCELL_EL [`V`;`mcell k V ul`;`e`];
828 BY(ASM_REWRITE_TAC[]);
831 REPEAT WEAK_STRIP_TAC;
832 INTRO_TAC MCELL3_EDGE [`V`;`ul`;`u`;`v`];
833 BY(ASM_MESON_TAC[MCELL3]);
834 INTRO_TAC MCELL2_EDGE [`V`;`ul`;`e`];
836 BY(ASM_MESON_TAC[IN;MCELL2]);
838 DISCH_THEN SUBST1_TAC;
839 GMATCH_SIMP_TAC SET_OF_LIST_TRUNCATE_2;
844 INTRO_TAC EDGE_IMP_K2 [`V`;`ul`;`k`];
846 BY(ASM_MESON_TAC[NOT_IN_EMPTY])
851 let MCELL_BUMP_0 = prove_by_refinement(
852 `!V ul e k. (k < 4 ) /\ packing V /\ saturated V /\ barV V 3 ul /\ ~NULLSET (mcell k V ul)
853 ==> beta_bumpA V e (mcell k V ul) = &0`,
856 REPEAT WEAK_STRIP_TAC;
857 REWRITE_TAC[Pack_defs.beta_bumpA];
858 REWRITE_TAC[LET_DEF;LET_END_DEF];
859 REWRITE_TAC[BETA_ORDERED_PAIR_THM];
860 INTRO_TAC MCELL_CELL_PARAMETERS_EXIST [`V`;`ul`;`k`;`mcell k V ul`];
862 BY(ASM_SIMP_TAC[arith `k < 4 ==> k <= 4`;IN]);
863 DISCH_THEN SUBST1_TAC;
864 ASM_SIMP_TAC[arith `k < 4 ==> ~(k=4)`];
865 REWRITE_TAC[GSPEC;SETSPEC];
866 BY(REWRITE_TAC[SYM EMPTY;SUM_CLAUSES])
871 let CARD2_EDGEX = prove_by_refinement(
872 `!V X e. e IN edgeX V X ==> CARD e = 2`,
875 REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM];
876 REPEAT WEAK_STRIP_TAC;
878 BY(ASM_SIMP_TAC[Hypermap.CARD_TWO_ELEMENTS])
882 let DIFF_EDGEX = prove_by_refinement(
883 `!V X ul k e. (k < 4) /\ packing V /\ saturated V /\ (X = mcell k V ul) /\ ~NULLSET X /\ barV V 3 ul /\
884 e IN edgeX V X ==> ~((VX V X DIFF e) IN edgeX V X)`,
887 REPEAT WEAK_STRIP_TAC;
888 ABBREV_TAC `e' = (VX V X DIFF e)`;
889 INTRO_TAC MCELL_EDGE [`V`;`ul`;`k`;`e`];
892 INTRO_TAC MCELL_EDGE [`V`;`ul`;`k`;`e'`];
895 REPEAT WEAK_STRIP_TAC;
896 REPEAT (FIRST_X_ASSUM_ST `set_of_list` MP_TAC);
897 TYPIFY `3 <= LENGTH ul` (C SUBGOAL_THEN ASSUME_TAC);
898 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 <= 3 + 1`]);
899 ASM_SIMP_TAC[ SET_OF_LIST_TRUNCATE_2];
900 REPEAT WEAK_STRIP_TAC;
901 INTRO_TAC Geomdetail.CARD3 [`EL 0 ul`;`EL 1 ul`;`EL 2 ul`];
902 REPEAT WEAK_STRIP_TAC;
903 INTRO_TAC CARD_UNION_GEN [`e`;`e'`];
904 TYPIFY `e INTER e' = {}` ((C SUBGOAL_THEN SUBST1_TAC));
905 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
906 REWRITE_TAC[CARD_CLAUSES;arith `x - 0 = x`];
907 TYPIFY `FINITE {EL 0 ul, EL 1 ul, EL 2 ul}` (C SUBGOAL_THEN MP_TAC);
908 BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]);
910 DISCH_THEN ( MP_TAC) THEN ANTS_TAC;
911 BY(ASM_MESON_TAC[FINITE_SUBSET]);
912 TYPIFY `CARD (e UNION e') <= CARD {EL 0 ul, EL 1 ul, EL 2 ul}` (C SUBGOAL_THEN ASSUME_TAC);
913 MATCH_MP_TAC CARD_SUBSET;
914 BY(ASM_REWRITE_TAC[UNION_SUBSET]);
915 REPEAT (FIRST_X_ASSUM (MP_TAC o (MATCH_MP CARD2_EDGEX)));
916 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC)
920 let CRITICAL_EDGEX_ALT = prove_by_refinement(
921 `!V X e. e IN critical_edgeX V X <=> e IN edgeX V X /\ hminus <= radV e /\ radV e <= hplus `,
924 REWRITE_TAC[Pack_defs.critical_edgeX;Pack_defs.HL;Pack_defs.edgeX];
925 REWRITE_TAC[IN_ELIM_THM;set_of_list2_explicit];
930 let SUBCRITICAL_EDGEX_ALT = prove_by_refinement(
931 `!V X e. e IN subcritical_edgeX V X <=> e IN edgeX V X /\ radV e < hminus `,
934 REWRITE_TAC[Pack_defs.subcritical_edgeX;Pack_defs.HL;Pack_defs.edgeX];
935 REWRITE_TAC[IN_ELIM_THM;set_of_list2_explicit];
940 let MCELL_BUMP_0 = prove_by_refinement(
941 `!V ul e k. (k < 4 ) /\ packing V /\ saturated V /\ barV V 3 ul /\ ~NULLSET (mcell k V ul)
942 ==> beta_bump_v1 V e (mcell k V ul) = &0`,
945 REWRITE_TAC[Pack_defs.beta_bump_v1];
946 REPEAT WEAK_STRIP_TAC;
947 ABBREV_TAC `e' = VX V (mcell k V ul) DIFF e`;
948 REWRITE_TAC[LET_DEF;LET_END_DEF];
949 REWRITE_TAC[CRITICAL_EDGEX_ALT;IN_ELIM_THM];
951 BY(ASM_MESON_TAC[DIFF_EDGEX]);
956 let MCELL4_EDGE_OPP = prove_by_refinement(
958 packing V /\ saturated V /\ barV V 3 ul /\ ~NULLSET (mcell4 V ul) ==>
959 VX V (mcell4 V ul) DIFF {EL 0 ul, EL 1 ul} = {EL 2 ul, EL 3 ul}`,
962 REPEAT WEAK_STRIP_TAC;
963 ABBREV_TAC `e' = VX V (mcell4 V ul) DIFF {EL 0 ul, EL 1 ul}`;
964 TYPIFY `VX V (mcell4 V ul) = set_of_list ul` (C SUBGOAL_THEN ASSUME_TAC);
965 GMATCH_SIMP_TAC Hdtfnfz.HDTFNFZ;
967 BY(ASM_MESON_TAC[MCELL4]);
968 MATCH_MP_TAC (GSYM MCELL4_SET_OF_LIST_VX);
969 BY(ASM_MESON_TAC[MCELL4]);
970 INTRO_TAC set_of_list4 [`ul`];
972 BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`]);
974 TYPIFY `e' SUBSET {EL 2 ul, EL 3 ul}` (C SUBGOAL_THEN ASSUME_TAC);
975 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
976 TYPIFY `e' = {EL 2 ul,EL 3 ul}` (C SUBGOAL_THEN ASSUME_TAC);
977 MATCH_MP_TAC CARD_SUBSET_LE;
978 ASM_REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY];
979 INTRO_TAC Marchal_cells_3.BARV_CARD_LEMMA [`V`;`ul`;`3`];
981 ASM_REWRITE_TAC[arith `3 + 1 = 4`];
982 INTRO_TAC Hypermap.CARD_MINUS_DIFF_TWO_SET [`{EL 0 ul, EL 1 ul, EL 2 ul, EL 3 ul}`;`EL 0 ul`;`EL 1 ul`];
983 REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY];
987 REPEAT WEAK_STRIP_TAC;
988 MATCH_MP_TAC (arith `v <= 2 /\ 2 <= x ==> v <= x`);
989 REWRITE_TAC[Geomdetail.CARD2];
990 MATCH_MP_TAC (arith `(?u. 4 = x + u /\ u <= 2) ==> 2 <= x`);
991 TYPIFY `CARD {EL 0 ul, EL 1 ul}` EXISTS_TAC;
994 BY(REWRITE_TAC[Geomdetail.CARD2]);
995 BY(ASM_REWRITE_TAC[])
999 let MCELL_BUMP_OPP = prove_by_refinement(
1000 `!V ul. packing V /\ saturated V /\ barV V 3 ul /\ ~NULLSET (mcell4 V ul) /\
1001 ~({EL 2 ul,EL 3 ul} IN critical_edgeX V (mcell4 V ul)) ==>
1002 beta_bump_v1 V {EL 0 ul,EL 1 ul} (mcell4 V ul) = &0
1006 REWRITE_TAC[Pack_defs.beta_bump_v1];
1007 REPEAT WEAK_STRIP_TAC;
1008 INTRO_TAC MCELL4_EDGE_OPP [`V`;`ul`];
1010 BY(ASM_REWRITE_TAC[]);
1011 DISCH_THEN SUBST1_TAC;
1012 REWRITE_TAC[LET_DEF;LET_END_DEF];
1013 BY(ASM_REWRITE_TAC[])
1017 let BETA_BUMP_NZ = prove_by_refinement(
1018 `!V ul e e'. packing V /\
1021 ~NULLSET (mcell4 V ul) /\
1022 (e = {EL 0 ul, EL 1 ul}) /\
1023 (e' = {EL 2 ul, EL 3 ul}) /\
1024 (e IN critical_edgeX V (mcell4 V ul)) /\
1025 (e' IN critical_edgeX V (mcell4 V ul)) /\
1026 (!f. f IN edgeX V (mcell4 V ul) ==> (f = e \/ f = e' \/ f IN subcritical_edgeX V (mcell4 V ul))) ==>
1027 beta_bump_v1 V e (mcell4 V ul) = bump (radV e) - bump (radV e')`,
1030 REPEAT WEAK_STRIP_TAC;
1031 INTRO_TAC MCELL4_EDGE_OPP [`V`;`ul`];
1033 BY(ASM_REWRITE_TAC[]);
1035 ASM_REWRITE_TAC[Pack_defs.beta_bump_v1];
1036 ASM_REWRITE_TAC[LET_DEF;LET_END_DEF];
1040 FIRST_X_ASSUM_ST `mcell4` MP_TAC;
1043 REWRITE_TAC[MCELL4;Pack_defs.mcell_set;IN_ELIM_THM];
1044 BY(ASM_MESON_TAC[IN]);
1046 BY(ASM_MESON_TAC[]);
1051 let BETA_BUMP_INVOLUTION = prove_by_refinement(
1052 `!V X r e. saturated V /\ packing V /\ mcell_set V X /\
1053 e IN critical_edgeX V X /\
1054 (\e. VX V X DIFF e) = r ==>
1058 REPEAT WEAK_STRIP_TAC;
1060 TYPIFY `e SUBSET VX V X` ENOUGH_TO_SHOW_TAC;
1062 FIRST_X_ASSUM_ST `IN` MP_TAC;
1063 REWRITE_TAC[CRITICAL_EDGEX_ALT];
1064 REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM];
1070 let BETA_BUMP_INVOLUTION = prove_by_refinement(
1071 `!V X r e. saturated V /\ packing V /\ mcell_set V X /\
1072 e IN critical_edgeX V X /\ ~(beta_bump_v1 V e X = &0) /\
1073 (\e. VX V X DIFF e) = r ==>
1077 REPEAT WEAK_STRIP_TAC;
1079 TYPIFY `e SUBSET VX V X` ENOUGH_TO_SHOW_TAC;
1081 FIRST_X_ASSUM_ST `IN` MP_TAC;
1082 REWRITE_TAC[CRITICAL_EDGEX_ALT];
1083 REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM];
1089 let BETA_BUMP_ALT = prove_by_refinement(
1090 `!V X r e. saturated V /\ packing V /\ mcell_set V X /\
1091 (\e. VX V X DIFF e) = r ==>
1092 beta_bump_v1 V e X =
1093 if ~(NULLSET X) /\ e IN critical_edgeX V X /\ r e IN critical_edgeX V X /\
1094 (!f. f IN edgeX V X ==> f = e \/ f = (r e) \/ f IN subcritical_edgeX V X) then bump (radV e) - bump (radV (r e))
1098 REPEAT WEAK_STRIP_TAC;
1099 REWRITE_TAC[Pack_defs.beta_bump_v1];
1100 REWRITE_TAC[Pack_defs.beta_bump_v1;LET_DEF;LET_END_DEF];
1102 BY(ASM_REWRITE_TAC[IN])
1106 let BETA_BUMP_INVOLUTION_CRITICAL = prove_by_refinement(
1107 `!V X r e. saturated V /\ packing V /\ mcell_set V X /\
1108 e IN critical_edgeX V X /\ ~(beta_bump_v1 V e X = &0) /\
1109 (\e. VX V X DIFF e) = r ==>
1110 r e IN critical_edgeX V X`,
1113 REPEAT WEAK_STRIP_TAC;
1115 INTRO_TAC BETA_BUMP_ALT [`V`;`X`;`r`;`e`];
1116 BY(ASM_REWRITE_TAC[])
1120 let BETA_BUMP_INVOLUTION_NEG = prove_by_refinement(
1121 `!V X r e. saturated V /\ packing V /\ mcell_set V X /\
1122 e IN critical_edgeX V X /\ ~(beta_bump_v1 V e X = &0) /\
1123 (\e. VX V X DIFF e) = r ==>
1124 beta_bump_v1 V (r e) X = -- beta_bump_v1 V e X`,
1127 REPEAT WEAK_STRIP_TAC;
1128 INTRO_TAC BETA_BUMP_INVOLUTION_CRITICAL [`V`;`X`;`r`;`e`];
1131 INTRO_TAC BETA_BUMP_ALT [`V`;`X`;`r`;`e`];
1133 DISCH_THEN SUBST1_TAC;
1134 INTRO_TAC BETA_BUMP_ALT [`V`;`X`;`r`;`r e`];
1136 DISCH_THEN SUBST1_TAC;
1137 TYPIFY `r (r e) = e` (C SUBGOAL_THEN SUBST1_TAC);
1138 INTRO_TAC BETA_BUMP_INVOLUTION [`V`;`X`;`r`;`e`];
1139 DISCH_THEN MATCH_MP_TAC;
1140 BY(ASM_REWRITE_TAC[]);
1141 REPEAT COND_CASES_TAC;
1143 BY(ASM_MESON_TAC[]);
1144 BY(ASM_MESON_TAC[]);
1149 let BETA_BUMP_INVOLUTION_BIJ = prove_by_refinement(
1150 `!V X s r. saturated V /\ packing V /\ mcell_set V X /\
1151 ({e | e IN critical_edgeX V X /\ ~(beta_bump_v1 V e X = &0) } = s ) /\
1152 (\e. VX V X DIFF e) = r ==>
1156 REWRITE_TAC[BIJ;INJ];
1157 REPEAT WEAK_STRIP_TAC;
1162 REWRITE_TAC[IN_ELIM_THM];
1163 REPEAT WEAK_STRIP_TAC;
1164 BY(ASM_MESON_TAC[BETA_BUMP_INVOLUTION_NEG;arith `(-- x = &0 <=> x = &0)`; BETA_BUMP_INVOLUTION_CRITICAL]);
1166 REWRITE_TAC[IN_ELIM_THM];
1167 REPEAT WEAK_STRIP_TAC;
1168 TYPIFY `r ( r x) = r ( r y)` (C SUBGOAL_THEN ASSUME_TAC);
1170 BY(ASM_REWRITE_TAC[]);
1171 BY(ASM_MESON_TAC[BETA_BUMP_INVOLUTION]);
1176 REWRITE_TAC[IN_ELIM_THM];
1177 REPEAT WEAK_STRIP_TAC;
1178 TYPIFY `r x` EXISTS_TAC;
1180 FIRST_X_ASSUM_ST `==>` MP_TAC;
1182 REWRITE_TAC[IN_ELIM_THM];
1183 BY(ASM_MESON_TAC[]);
1185 BY(ASM_MESON_TAC[BETA_BUMP_INVOLUTION])
1189 let SUM_BETA_BUMP_LEMMA = prove_by_refinement(
1190 `!V X. saturated V /\ packing V /\ mcell_set V X ==>
1191 sum {e | e IN critical_edgeX V X } (\e. beta_bump_v1 V e X) = &0`,
1194 REPEAT WEAK_STRIP_TAC;
1195 ABBREV_TAC `s = {e | e IN critical_edgeX V X /\ ~(beta_bump_v1 V e X = &0) } `;
1196 INTRO_TAC SUM_SUPERSET [`(\e. beta_bump_v1 V e X)`;`s`;`{e | e IN critical_edgeX V X }`];
1199 REWRITE_TAC[IN_ELIM_THM;SUBSET];
1201 DISCH_THEN SUBST1_TAC;
1202 ABBREV_TAC `r = (\e. VX V X DIFF e)`;
1203 INTRO_TAC BIJ_SUM [`s`;`s`;`(\e. beta_bump_v1 V e X)`;`r`];
1205 BY(ASM_MESON_TAC[ BETA_BUMP_INVOLUTION_BIJ]);
1206 INTRO_TAC SUM_EQ [`((\e. beta_bump_v1 V e X) o r)`;`(\e. -- beta_bump_v1 V e X)`;`s`];
1209 REWRITE_TAC[IN_ELIM_THM];
1211 BY(ASM_MESON_TAC[BETA_BUMP_INVOLUTION_NEG]);
1212 DISCH_THEN SUBST1_TAC;
1213 REWRITE_TAC[SUM_NEG];
1218 let REAL_ABS_TRIANGLE_BOUND = prove_by_refinement(
1219 `!a b x. a <= x /\ x <= b ==> abs x <= abs a + abs b`,
1226 let CRITICAL_EDGEX_BOUND = prove_by_refinement(
1227 `?c1. !V X e. e IN critical_edgeX V X ==> abs(radV e - h0) <= c1`,
1230 REWRITE_TAC[CRITICAL_EDGEX_ALT];
1231 EXISTS_TAC `abs (hplus) + abs (hminus) + abs (h0)`;
1232 REPEAT WEAK_STRIP_TAC;
1233 INTRO_TAC REAL_ABS_TRIANGLE_BOUND [`hminus`;`hplus`;`radV e`];
1239 let ABS_BUMP = prove_by_refinement(
1240 `!h c1. abs(h- h0) <= c1 ==> abs(bump h) <= abs (#0.005) * (&1 + (c1 pow 2) / abs((hplus - h0) pow 2))`,
1243 REWRITE_TAC[Pack_defs.bump ];
1244 REPEAT WEAK_STRIP_TAC;
1245 REWRITE_TAC[REAL_ABS_MUL];
1246 GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP;
1249 MATCH_MP_TAC (arith ` abs x + abs y <= z ==> abs (x - y) <= z`);
1250 REWRITE_TAC[arith `abs(&1) + x <= &1 + y <=> x <= y`];
1251 REWRITE_TAC[REAL_ABS_DIV];
1252 REWRITE_TAC[real_div];
1253 MATCH_MP_TAC Real_ext.REAL_PROP_LE_RMUL;
1254 REWRITE_TAC[REAL_LE_INV_EQ];
1257 REWRITE_TAC[REAL_ABS_POW];
1258 MATCH_MP_TAC Collect_geom2.POS_IMP_POW2;
1264 let BOUND_BETA_BUMP = prove_by_refinement(
1266 saturated V /\ packing V /\ mcell_set V X /\ critical_edgeX V X e
1267 ==> beta_bump_v1 V e X <= c`,
1270 INTRO_TAC CRITICAL_EDGEX_BOUND [];
1271 REPEAT WEAK_STRIP_TAC;
1272 EXISTS_TAC `&2 * abs (#0.005) * (&1 + (c1 pow 2) / abs((hplus - h0) pow 2))`;
1273 REPEAT WEAK_STRIP_TAC;
1274 REWRITE_TAC[Pack_defs.beta_bump_v1;LET_DEF;LET_END_DEF];
1276 MATCH_MP_TAC REAL_LE_TRANS;
1277 ABBREV_TAC `e' = VX V X DIFF e`;
1278 TYPIFY `abs (bump (radV e)) + abs (bump (radV e'))` EXISTS_TAC;
1281 MATCH_MP_TAC (arith `x <= z /\ y <= z ==> x + y <= &2 * z`);
1282 BY(ASM_MESON_TAC[ ABS_BUMP]);
1283 MATCH_MP_TAC (arith `&0 <= x ==> &0 <= &2 * abs (#0.005) * x`);
1284 REWRITE_TAC[real_div];
1285 MATCH_MP_TAC (arith `&0 <= x ==> &0 <= &1 + x`);
1286 GMATCH_SIMP_TAC REAL_LE_MUL;
1287 REWRITE_TAC[REAL_LE_INV_EQ];
1288 REWRITE_TAC[ REAL_LE_POW_2];