text_formalization/packing/bump.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Packing                                                           *)
   5 (* Lemma: OXLZLEZ                                                             *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2012-12-31                                                           *)
   8 (* ========================================================================== *)
   9
  10 (* REDO THE beta_bump  *)
  11
  12
  13
  14 module Bump = struct
  15
  16   open Hales_tactic;;
  17
  18 let WEAK_SELECT_TAC  =
  19   let unbeta = prove(
  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;;
  24
  25 let BETA_ORDERED_PAIR_THM = prove_by_refinement(
  26  `!(g:A->B->C) x.
  27     ((\ ( u, v). g u v) x = g (FST x) (SND x))`,
  28   (* {{{ proof *)
  29   [
  30   REPEAT GEN_TAC;
  31   INTRO_TAC (GSYM PAIR) [`x`];
  32   DISCH_THEN SUBST1_TAC;
  33   BY(REWRITE_TAC[GABS_DEF;GEQ_DEF])
  34   ]);;
  35   (* }}} *)
  36
  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)`,
  40   (* {{{ proof *)
  41   [
  42   REWRITE_TAC[BIJ;INJ];
  43   BY(ASM_MESON_TAC[ SUM_IMAGE ; Misc_defs_and_lemmas.SURJ_IMAGE ])
  44   ]);;
  45   (* }}} *)
  46
  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`,
  55   (* {{{ proof *)
  56   [
  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`])
  58   ]);;
  59   (* }}} *)
  60
  61 let LENGTH1 = prove_by_refinement(
  62   `!ul:(A) list. LENGTH ul = 1 ==> ul = [EL 0 ul]`,
  63   (* {{{ proof *)
  64   [
  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])
  68   ]);;
  69   (* }}} *)
  70
  71 let LENGTH2 = prove_by_refinement(
  72   `!ul:(A) list. LENGTH ul = 2 ==> ul = [EL 0 ul;EL 1 ul]`,
  73   (* {{{ proof *)
  74   [
  75   REWRITE_TAC[LENGTH_EQ_CONS;arith `2 = SUC 1`];
  76   REPEAT WEAK_STRIP_TAC;
  77   ASM_REWRITE_TAC[];
  78   FIRST_X_ASSUM (unlist ONCE_REWRITE_TAC o (MATCH_MP LENGTH1));
  79   BY(REWRITE_TAC[EL;HD;arith `1 = SUC 0`;TL])
  80   ]);;
  81   (* }}} *)
  82
  83 let LENGTH3 = prove_by_refinement(
  84   `!(ul:(A)list). LENGTH ul = 3 ==> ul = [EL 0 ul; EL 1 ul; EL 2 ul]`,
  85   (* {{{ proof *)
  86   [
  87   REWRITE_TAC[LENGTH_EQ_CONS;arith `3 = SUC 2`];
  88   REPEAT WEAK_STRIP_TAC;
  89   ASM_REWRITE_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])
  92   ]);;
  93   (* }}} *)
  94
  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]`,
  97   (* {{{ proof *)
  98   [
  99   REWRITE_TAC[LENGTH_EQ_CONS;arith `4 = SUC 3`];
 100   REPEAT WEAK_STRIP_TAC;
 101   ASM_REWRITE_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])
 104   ]);;
 105   (* }}} *)
 106
 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}`,
 109   (* {{{ proof *)
 110   [
 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])
 117   ]);;
 118   (* }}} *)
 119
 120 let set_of_list2_explicit = prove_by_refinement(
 121   `!(a:A) b. set_of_list [a;b] = {a,b}`,
 122   (* {{{ proof *)
 123   [
 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`])
 127   ]);;
 128   (* }}} *)
 129
 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}`,
 132   (* {{{ proof *)
 133   [
 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])
 141   ]);;
 142   (* }}} *)
 143
 144 let set_of_list3_explicit = prove_by_refinement(
 145   `!(a:A) b c. set_of_list [a;b;c] = {a,b,c}`,
 146   (* {{{ proof *)
 147   [
 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])
 151   ]);;
 152   (* }}} *)
 153
 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}`,
 156   (* {{{ proof *)
 157   [
 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])
 166   ]);;
 167   (* }}} *)
 168
 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}`,
 171   (* {{{ proof *)
 172   [
 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])
 176   ]);;
 177   (* }}} *)
 178
 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}`,
 181   (* {{{ proof *)
 182   [
 183   REPEAT WEAK_STRIP_TAC;
 184   GMATCH_SIMP_TAC set_of_list2;
 185   CONJ_TAC;
 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)
 191   ]);;
 192   (* }}} *)
 193
 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}`,
 196   (* {{{ proof *)
 197   [
 198   REPEAT WEAK_STRIP_TAC;
 199   GMATCH_SIMP_TAC set_of_list3;
 200   CONJ_TAC;
 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);
 205   ASM_REWRITE_TAC[];
 206   BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC)
 207   ]);;
 208   (* }}} *)
 209
 210
 211 let VX_EMPTY = prove_by_refinement(
 212   `!V vl k. (NULLSET (mcell k V vl)) ==> (VX V (mcell k V vl) = {})`,
 213   (* {{{ proof *)
 214   [
 215   REPEAT WEAK_STRIP_TAC;
 216   BY(ASM_REWRITE_TAC[Pack_defs.VX])
 217   ]);;
 218   (* }}} *)
 219
 220 let RIJRIED = prove_by_refinement(
 221   `!V vl k.  (NULLSET (mcell k V vl)) ==> (edgeX V (mcell k V vl) = {})`,
 222   (* {{{ proof *)
 223   [
 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];
 228   BY(MESON_TAC[IN])
 229   ]);;
 230   (* }}} *)
 231
 232 let  HDTFNFZ_SUBSET = prove_by_refinement(
 233  `!V ul k X.
 234          saturated V /\
 235          packing V /\
 236          barV V 3 ul /\
 237          X = mcell k V ul
 238          ==> VX V X SUBSET V INTER X`,
 239   (* {{{ proof *)
 240   [
 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])
 245   ]);;
 246   (* }}} *)
 247
 248 let HDTFNFZ_ALT = prove_by_refinement(
 249   `!V ul k X.
 250     saturated V /\
 251     packing V /\
 252     barV V 3 ul /\
 253     X = mcell k V ul /\
 254     ~NULLSET X
 255     ==> VX V X = V INTER X`,
 256   (* {{{ proof *)
 257   [
 258     ASM_MESON_TAC[Hdtfnfz.HDTFNFZ]
 259   ]);;
 260   (* }}} *)
 261
 262 let VORONOI_V = prove_by_refinement(
 263   `!V (w:real^A). w IN V ==> (V INTER voronoi_closed V w = {w})`,
 264   (* {{{ proof *)
 265   [
 266   REWRITE_TAC[Sphere.voronoi_closed;EXTENSION;IN_SING;IN_INTER;IN_ELIM_THM];
 267   REWRITE_TAC[IN];
 268   REPEAT WEAK_STRIP_TAC;
 269   BY(ASM_MESON_TAC[DIST_EQ_0;arith `x <= &0 /\ &0 <= x ==> x = &0`;DIST_POS_LE])
 270   ]);;
 271   (* }}} *)
 272
 273 let V_CELL0_EMPTY = prove_by_refinement(
 274   `!V vl. saturated V /\ packing V /\  barV V 3 vl  ==> V INTER (mcell0 V vl) = {}`,
 275   (* {{{ proof *)
 276   [
 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`];
 281   ASM_REWRITE_TAC[];
 282   DISCH_TAC;
 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;
 287     REWRITE_TAC[ball];
 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;
 291     BY(REAL_ARITH_TAC);
 292   DISCH_THEN ( MP_TAC);
 293   ANTS_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])
 297   ]);;
 298   (* }}} *)
 299
 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}`,
 302   (* {{{ proof *)
 303   [
 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;
 308   COND_CASES_TAC;
 309     DISCH_TAC;
 310     TYPIFY `x IN cball(HD vl,sqrt(&2))` (C SUBGOAL_THEN MP_TAC);
 311       FIRST_X_ASSUM MP_TAC;
 312       BY(SET_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;
 316       BY(REAL_ARITH_TAC);
 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])
 324   ]);;
 325   (* }}} *)
 326
 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) = {})`,
 329   (* {{{ proof *)
 330   [
 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);
 335   COND_CASES_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];
 339     BY(SET_TAC[IN]);
 340   TYPIFY `k=1` (C SUBGOAL_THEN ASSUME_TAC);
 341     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 342   ASM_REWRITE_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`];
 346   ASM_REWRITE_TAC[];
 347   REWRITE_TAC[SUBSET;IN_SING;IN_INTER];
 348   REPEAT WEAK_STRIP_TAC;
 349   BY(ASM_MESON_TAC[IN])
 350   ]);;
 351   (* }}} *)
 352
 353
 354 (* DEC 31, 2012 *)
 355
 356 (* 2 CELL EXPLICIT *)
 357
 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}`,
 361   (* {{{ proof *)
 362   [
 363   REWRITE_TAC[SUBSET];
 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`];
 373   ASM_REWRITE_TAC[];
 374   ANTS_TAC;
 375     BY(REWRITE_TAC[Pack_defs.mcell;arith `~(2 = 0) /\ ~(2 = 1)`]);
 376   DISCH_TAC;
 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[]);
 379   WEAK_STRIP_TAC;
 380   ASM_REWRITE_TAC[];
 381   DISCH_TAC;
 382   REWRITE_TAC[Rogers.CIRCUMCENTER_2];
 383   ANTS_TAC;
 384     CONJ_TAC;
 385       MATCH_MP_TAC SUBSET_TRANS;
 386       TYPIFY `set_of_list ul` EXISTS_TAC;
 387       CONJ_TAC;
 388         GMATCH_SIMP_TAC set_of_list4;
 389         CONJ2_TAC;
 390           BY(SET_TAC[]);
 391         BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`]);
 392       BY(ASM_MESON_TAC[Packing3.BARV_SUBSET]);
 393     CONJ_TAC;
 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];
 399     DISCH_THEN kill;
 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;
 406   PROOF_BY_CONTR_TAC;
 407   FIRST_X_ASSUM_ST `dist` MP_TAC;
 408   ANTS_TAC;
 409     ASM_REWRITE_TAC[];
 410     BY(SET_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`];
 415     BY(REAL_ARITH_TAC);
 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`];
 424   BY(REAL_ARITH_TAC)
 425   ]);;
 426   (* }}} *)
 427
 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}`,
 431   (* {{{ proof *)
 432   [
 433   REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM];
 434   REPEAT WEAK_STRIP_TAC;
 435   INTRO_TAC MCELL2_VERTEX [`V`;`ul`];
 436   ASM_REWRITE_TAC[];
 437   REWRITE_TAC[Geomdetail.PAIR_EQ_EXPAND];
 438   REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
 439   DISCH_TAC;
 440   FIRST_ASSUM (C INTRO_TAC [`u`]);
 441   FIRST_X_ASSUM (C INTRO_TAC [`v`]);
 442   BY(ASM_MESON_TAC[IN])
 443   ]);;
 444   (* }}} *)
 445
 446 (* 3 AND 4 CELL EXPLICIT *)
 447
 448 let MCELL4 = prove_by_refinement(
 449   `!V ul. mcell4 V ul = mcell 4 V ul`,
 450   (* {{{ proof *)
 451   [
 452   BY(REWRITE_TAC[Pack_defs.mcell;arith `~(4 =0) /\ ~(4 = 1) /\ ~(4=2) /\ ~(4=3)`])
 453   ]);;
 454   (* }}} *)
 455
 456 let MCELL3 = prove_by_refinement(
 457   `!V ul. mcell3 V ul = mcell 3 V ul`,
 458   (* {{{ proof *)
 459   [
 460   BY(REWRITE_TAC[Pack_defs.mcell;arith `~(3 =0) /\ ~(3 = 1) /\ ~(3=2)`])
 461   ]);;
 462   (* }}} *)
 463
 464 let MCELL2 = prove_by_refinement(
 465   `!V ul. mcell2 V ul = mcell 2 V ul`,
 466   (* {{{ proof *)
 467   [
 468   BY(REWRITE_TAC[Pack_defs.mcell;arith `~(2 =0) /\ ~(2 = 1)`])
 469   ]);;
 470   (* }}} *)
 471
 472 let MCELL1 = prove_by_refinement(
 473   `!V ul. mcell1 V ul = mcell 1 V ul`,
 474   (* {{{ proof *)
 475   [
 476   BY(REWRITE_TAC[Pack_defs.mcell;arith `~(1 =0)`])
 477   ]);;
 478   (* }}} *)
 479
 480 let MCELL0 = prove_by_refinement(
 481   `!V ul. mcell0 V ul = mcell 0 V ul`,
 482   (* {{{ proof *)
 483   [
 484   BY(REWRITE_TAC[Pack_defs.mcell;arith `~(1 =0)`])
 485   ]);;
 486   (* }}} *)
 487
 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`,
 491   (* {{{ proof *)
 492   [
 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`];
 498     REWRITE_TAC[IN];
 499     REPEAT WEAK_STRIP_TAC;
 500     FIRST_X_ASSUM_ST `==>` MP_TAC;
 501     ANTS_TAC;
 502       ASM_REWRITE_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[])
 510   ]);;
 511   (* }}} *)
 512
 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`,
 516   (* {{{ proof *)
 517   [
 518   REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_CELL_PARAMETERS_EXIST THEN ASM_REWRITE_TAC[MCELL4;arith `4 <= 4`];
 519   BY(ASM_MESON_TAC[])
 520   ]);;
 521   (* }}} *)
 522
 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`,
 526   (* {{{ proof *)
 527   [
 528   REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_CELL_PARAMETERS_EXIST THEN ASM_REWRITE_TAC[MCELL3;arith `3 <= 4`];
 529   BY(ASM_MESON_TAC[])
 530   ]);;
 531   (* }}} *)
 532
 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`,
 536   (* {{{ proof *)
 537   [
 538   REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_CELL_PARAMETERS_EXIST THEN ASM_REWRITE_TAC[MCELL2;arith `2 <= 4`];
 539   BY(ASM_MESON_TAC[])
 540   ]);;
 541   (* }}} *)
 542
 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)`,
 547   (* {{{ proof *)
 548   [
 549   REWRITE_TAC[Pack_defs.cell_params];
 550   REPEAT WEAK_STRIP_TAC;
 551   INTRO_TAC MCELL_CELL_PARAMETERS_EXIST [`V`;`ul`;`k`;`X`];
 552   ASM_REWRITE_TAC[];
 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;
 557   CONJ_TAC;
 558     BY(MESON_TAC[]);
 559   REPEAT WEAK_STRIP_TAC;
 560   CONJ_TAC;
 561     BY(ASM_MESON_TAC[]);
 562   REWRITE_TAC[NOT_EXISTS_THM];
 563   DISCH_THEN (C INTRO_TAC [`k,ul`]);
 564   BY(ASM_MESON_TAC[FST;SND])
 565   ]);;
 566   (* }}} *)
 567
 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)`,
 572   (* {{{ proof *)
 573   [
 574   REWRITE_TAC[MCELL4];
 575   REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_PARAM_UL;
 576   BY(ASM_MESON_TAC[arith `4 <= 4`])
 577   ]);;
 578   (* }}} *)
 579
 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)`,
 584   (* {{{ proof *)
 585   [
 586   REWRITE_TAC[MCELL3];
 587   REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_PARAM_UL;
 588   BY(ASM_MESON_TAC[arith `3 <= 4`])
 589   ]);;
 590   (* }}} *)
 591
 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)`,
 596   (* {{{ proof *)
 597   [
 598   REWRITE_TAC[MCELL2];
 599   REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_PARAM_UL;
 600   BY(ASM_MESON_TAC[arith `2 <= 4`])
 601   ]);;
 602   (* }}} *)
 603
 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)))`,
 607   (* {{{ proof *)
 608   [
 609   REWRITE_TAC[Pack_defs.VX];
 610   REPEAT WEAK_STRIP_TAC;
 611   COND_CASES_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`];
 616   ASM_REWRITE_TAC[];
 617   DISCH_TAC;
 618   ASM_REWRITE_TAC[arith `~(4 = 0) /\ 4 - 1 = 3`];
 619   MATCH_MP_TAC (MESON[SUBSET_REFL] `a = b ==> a SUBSET b`);
 620   AP_TERM_TAC;
 621   INTRO_TAC MCELL4_PARAM_UL [`V`;`ul`;`SND (cell_params V X)`;`X`];
 622   ASM_REWRITE_TAC[];
 623   REPEAT WEAK_STRIP_TAC;
 624   MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_REFL;
 625   BY(ASM_MESON_TAC[Sphere.BARV;IN])
 626   ]);;
 627   (* }}} *)
 628
 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))))`,
 632   (* {{{ proof *)
 633   [
 634   REWRITE_TAC[Pack_defs.VX];
 635   REPEAT WEAK_STRIP_TAC;
 636   COND_CASES_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`];
 641   ASM_REWRITE_TAC[];
 642   DISCH_TAC;
 643   ASM_REWRITE_TAC[arith `~(3 = 0) /\ 2 = 3 - 1`];
 644   BY(SET_TAC[])
 645   ]);;
 646   (* }}} *)
 647
 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`,
 651   (* {{{ proof *)
 652   [
 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;
 659     CONJ_TAC;
 660       BY(REWRITE_TAC[FINITE_SET_OF_LIST]);
 661     CONJ_TAC;
 662       BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
 663     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 664   CONJ_TAC;
 665     REWRITE_TAC[SUBSET_INTER];
 666     CONJ_TAC;
 667       MATCH_MP_TAC Packing3.BARV_SUBSET;
 668       BY(ASM_MESON_TAC[]);
 669     FIRST_X_ASSUM_ST `NULLSET` MP_TAC;
 670     ASM_REWRITE_TAC[Pack_defs.mcell4];
 671     COND_CASES_TAC;
 672       BY(REWRITE_TAC[HULL_SUBSET]);
 673     BY(REWRITE_TAC[NEGLIGIBLE_EMPTY]);
 674   COMMENT "goal 2";
 675   CONJ_TAC;
 676     BY(ASM_MESON_TAC[HDTFNFZ_ALT;MCELL4]);
 677   CONJ_TAC;
 678     MATCH_MP_TAC MCELL4_VX;
 679     BY(ASM_MESON_TAC[IN]);
 680   CONJ_TAC;
 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`];
 684     ASM_REWRITE_TAC[];
 685     ANTS_TAC;
 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;
 690   BY(ASM_MESON_TAC[])
 691   ]);;
 692   (* }}} *)
 693
 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`,
 697   (* {{{ proof *)
 698   [
 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;
 705     CONJ_TAC;
 706       BY(REWRITE_TAC[FINITE_SET_OF_LIST]);
 707     CONJ_TAC;
 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";
 711   CONJ_TAC;
 712     REWRITE_TAC[SUBSET_INTER];
 713     CONJ_TAC;
 714       MATCH_MP_TAC SUBSET_TRANS;
 715       TYPIFY `set_of_list ul` EXISTS_TAC;
 716       CONJ_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;
 720       BY(ASM_MESON_TAC[]);
 721     FIRST_X_ASSUM_ST `NULLSET` MP_TAC;
 722     ASM_REWRITE_TAC[Pack_defs.mcell3];
 723     COND_CASES_TAC;
 724       DISCH_TAC;
 725       MATCH_MP_TAC SUBSET_TRANS;
 726       TYPIFY `set_of_list (truncate_simplex 2 ul) UNION {mxi V ul}` EXISTS_TAC;
 727       CONJ_TAC;
 728         BY(SET_TAC[]);
 729       BY(REWRITE_TAC[HULL_SUBSET]);
 730     BY(REWRITE_TAC[NEGLIGIBLE_EMPTY]);
 731   COMMENT "goal 2";
 732   CONJ_TAC;
 733     BY(ASM_MESON_TAC[HDTFNFZ_ALT;MCELL3]);
 734   CONJ_TAC;
 735     MATCH_MP_TAC MCELL3_VX;
 736     BY(ASM_MESON_TAC[IN]);
 737   CONJ_TAC;
 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`];
 741     ASM_REWRITE_TAC[];
 742     ANTS_TAC;
 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`];
 746   ASM_REWRITE_TAC[];
 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);
 755     EXPAND_TAC "s";
 756     BY(SET_TAC[]);
 757   GMATCH_SIMP_TAC (CONJUNCT2 CARD_CLAUSES);
 758   CONJ_TAC;
 759     BY(ASM_MESON_TAC[FINITE_EMPTY;FINITE_INSERT]);
 760   COND_CASES_TAC;
 761     BY(ASM_MESON_TAC[Geomdetail.CARD3;arith `~( 3 + 1 <= 3)`]);
 762   BY(ARITH_TAC)
 763   ]);;
 764   (* }}} *)
 765
 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))`,
 769   (* {{{ proof *)
 770   [
 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`];
 774   ANTS_TAC;
 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`];
 778   ANTS_TAC;
 779     BY(ASM_REWRITE_TAC[]);
 780   DISCH_THEN SUBST1_TAC;
 781   REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;Geomdetail.PAIR_EQ_EXPAND];
 782   BY(MESON_TAC[IN])
 783   ]);;
 784   (* }}} *)
 785
 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))))`,
 789   (* {{{ proof *)
 790   [
 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`];
 794   ANTS_TAC;
 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`];
 798   ANTS_TAC;
 799     BY(ASM_REWRITE_TAC[]);
 800   DISCH_THEN SUBST1_TAC;
 801   REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;Geomdetail.PAIR_EQ_EXPAND];
 802   BY(MESON_TAC[IN])
 803   ]);;
 804   (* }}} *)
 805
 806 let EDGE_MCELL_EL = prove_by_refinement(
 807   `!V X e. e IN edgeX V X ==> (?u v. e = {u,v} /\ ~(u=v))`,
 808   (* {{{ proof *)
 809   [
 810   REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM];
 811   BY(MESON_TAC[])
 812   ]);;
 813   (* }}} *)
 814
 815
 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))`,
 819   (* {{{ proof *)
 820   [
 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`];
 827   ANTS_TAC;
 828     BY(ASM_REWRITE_TAC[]);
 829   WEAK_STRIP_TAC;
 830   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`];
 835     ANTS_TAC;
 836       BY(ASM_MESON_TAC[IN;MCELL2]);
 837     ASM_REWRITE_TAC[];
 838     DISCH_THEN SUBST1_TAC;
 839     GMATCH_SIMP_TAC SET_OF_LIST_TRUNCATE_2;
 840     ASM_REWRITE_TAC[];
 841     CONJ_TAC;
 842       BY(ARITH_TAC);
 843     BY(SET_TAC[]);
 844   INTRO_TAC EDGE_IMP_K2 [`V`;`ul`;`k`];
 845   ASM_REWRITE_TAC[];
 846   BY(ASM_MESON_TAC[NOT_IN_EMPTY])
 847   ]);;
 848   (* }}} *)
 849
 850 (*
 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`,
 854   (* {{{ proof *)
 855   [
 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`];
 861   ANTS_TAC;
 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])
 867   ]);;
 868   (* }}} *)
 869 *)
 870
 871 let CARD2_EDGEX = prove_by_refinement(
 872   `!V X e. e IN edgeX V X ==> CARD e = 2`,
 873   (* {{{ proof *)
 874   [
 875   REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM];
 876   REPEAT WEAK_STRIP_TAC;
 877   ASM_REWRITE_TAC[];
 878   BY(ASM_SIMP_TAC[Hypermap.CARD_TWO_ELEMENTS])
 879   ]);;
 880   (* }}} *)
 881
 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)`,
 885   (* {{{ proof *)
 886   [
 887   REPEAT WEAK_STRIP_TAC;
 888   ABBREV_TAC `e' = (VX V X DIFF e)`;
 889   INTRO_TAC MCELL_EDGE [`V`;`ul`;`k`;`e`];
 890   ANTS_TAC;
 891     BY(ASM_MESON_TAC[]);
 892   INTRO_TAC MCELL_EDGE [`V`;`ul`;`k`;`e'`];
 893   ANTS_TAC;
 894     BY(ASM_MESON_TAC[]);
 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]);
 909   DISCH_TAC;
 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)
 917   ]);;
 918   (* }}} *)
 919
 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 `,
 922   (* {{{ proof *)
 923   [
 924   REWRITE_TAC[Pack_defs.critical_edgeX;Pack_defs.HL;Pack_defs.edgeX];
 925   REWRITE_TAC[IN_ELIM_THM;set_of_list2_explicit];
 926   BY(MESON_TAC[])
 927   ]);;
 928   (* }}} *)
 929
 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 `,
 932   (* {{{ proof *)
 933   [
 934   REWRITE_TAC[Pack_defs.subcritical_edgeX;Pack_defs.HL;Pack_defs.edgeX];
 935   REWRITE_TAC[IN_ELIM_THM;set_of_list2_explicit];
 936   BY(MESON_TAC[])
 937   ]);;
 938   (* }}} *)
 939
 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`,
 943   (* {{{ proof *)
 944   [
 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];
 950   COND_CASES_TAC;
 951     BY(ASM_MESON_TAC[DIFF_EDGEX]);
 952   BY(REWRITE_TAC[])
 953   ]);;
 954   (* }}} *)
 955
 956 let MCELL4_EDGE_OPP = prove_by_refinement(
 957   `!V ul.
 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}`,
 960   (* {{{ proof *)
 961   [
 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;
 966     CONJ_TAC;
 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`];
 971   ANTS_TAC;
 972     BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`]);
 973   DISCH_TAC;
 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`];
 980     ASM_REWRITE_TAC[];
 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];
 984     ANTS_TAC;
 985       BY(SET_TAC[]);
 986     ASM_REWRITE_TAC[];
 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;
 992     CONJ_TAC;
 993       BY(ASM_MESON_TAC[]);
 994     BY(REWRITE_TAC[Geomdetail.CARD2]);
 995   BY(ASM_REWRITE_TAC[])
 996   ]);;
 997   (* }}} *)
 998
 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
1003   `,
1004   (* {{{ proof *)
1005   [
1006   REWRITE_TAC[Pack_defs.beta_bump_v1];
1007   REPEAT WEAK_STRIP_TAC;
1008   INTRO_TAC MCELL4_EDGE_OPP [`V`;`ul`];
1009   ANTS_TAC;
1010     BY(ASM_REWRITE_TAC[]);
1011   DISCH_THEN SUBST1_TAC;
1012   REWRITE_TAC[LET_DEF;LET_END_DEF];
1013   BY(ASM_REWRITE_TAC[])
1014   ]);;
1015   (* }}} *)
1016
1017  let BETA_BUMP_NZ = prove_by_refinement(
1018   `!V ul e e'.         packing V /\
1019          saturated V /\
1020          barV V 3 ul /\
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')`,
1028   (* {{{ proof *)
1029   [
1030   REPEAT WEAK_STRIP_TAC;
1031   INTRO_TAC MCELL4_EDGE_OPP [`V`;`ul`];
1032   ANTS_TAC;
1033     BY(ASM_REWRITE_TAC[]);
1034   DISCH_TAC;
1035   ASM_REWRITE_TAC[Pack_defs.beta_bump_v1];
1036   ASM_REWRITE_TAC[LET_DEF;LET_END_DEF];
1037   COND_CASES_TAC;
1038     BY(REWRITE_TAC[]);
1039   PROOF_BY_CONTR_TAC;
1040   FIRST_X_ASSUM_ST `mcell4` MP_TAC;
1041   REWRITE_TAC[];
1042   CONJ_TAC;
1043     REWRITE_TAC[MCELL4;Pack_defs.mcell_set;IN_ELIM_THM];
1044     BY(ASM_MESON_TAC[IN]);
1045   CONJ_TAC;
1046     BY(ASM_MESON_TAC[]);
1047   BY(ASM_MESON_TAC[])
1048 ]);;
1049   (* }}} *)
1050
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 ==>
1055     r ( r e) = e`,
1056   (* {{{ proof *)
1057   [
1058   REPEAT WEAK_STRIP_TAC;
1059   EXPAND_TAC "r";
1060   TYPIFY `e SUBSET VX V X` ENOUGH_TO_SHOW_TAC;
1061     BY(SET_TAC[]);
1062   FIRST_X_ASSUM_ST `IN` MP_TAC;
1063   REWRITE_TAC[CRITICAL_EDGEX_ALT];
1064   REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM];
1065   BY(SET_TAC[])
1066   ]);;
1067   (* }}} *)
1068
1069 (*
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 ==>
1074     r ( r e) = e`,
1075   (* {{{ proof *)
1076   [
1077   REPEAT WEAK_STRIP_TAC;
1078   EXPAND_TAC "r";
1079   TYPIFY `e SUBSET VX V X` ENOUGH_TO_SHOW_TAC;
1080     BY(SET_TAC[]);
1081   FIRST_X_ASSUM_ST `IN` MP_TAC;
1082   REWRITE_TAC[CRITICAL_EDGEX_ALT];
1083   REWRITE_TAC[Pack_defs.edgeX;IN_ELIM_THM];
1084   BY(SET_TAC[])
1085   ]);;
1086   (* }}} *)
1087 *)
1088
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))
1095     else &0`,
1096   (* {{{ proof *)
1097   [
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];
1101   EXPAND_TAC "r";
1102   BY(ASM_REWRITE_TAC[IN])
1103   ]);;
1104   (* }}} *)
1105
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`,
1111   (* {{{ proof *)
1112   [
1113   REPEAT WEAK_STRIP_TAC;
1114   PROOF_BY_CONTR_TAC;
1115   INTRO_TAC BETA_BUMP_ALT [`V`;`X`;`r`;`e`];
1116   BY(ASM_REWRITE_TAC[])
1117   ]);;
1118   (* }}} *)
1119
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`,
1125   (* {{{ proof *)
1126   [
1127   REPEAT WEAK_STRIP_TAC;
1128   INTRO_TAC BETA_BUMP_INVOLUTION_CRITICAL [`V`;`X`;`r`;`e`];
1129   ASM_REWRITE_TAC[];
1130   DISCH_TAC;
1131   INTRO_TAC BETA_BUMP_ALT [`V`;`X`;`r`;`e`];
1132   ASM_REWRITE_TAC[];
1133   DISCH_THEN SUBST1_TAC;
1134   INTRO_TAC BETA_BUMP_ALT [`V`;`X`;`r`;`r e`];
1135   ASM_REWRITE_TAC[];
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;
1142         BY(REAL_ARITH_TAC);
1143       BY(ASM_MESON_TAC[]);
1144     BY(ASM_MESON_TAC[]);
1145   BY(REAL_ARITH_TAC)
1146   ]);;
1147   (* }}} *)
1148
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 ==>
1153     BIJ r s s`,
1154   (* {{{ proof *)
1155   [
1156   REWRITE_TAC[BIJ;INJ];
1157   REPEAT WEAK_STRIP_TAC;
1158   SUBCONJ_TAC;
1159     CONJ_TAC;
1160       GEN_TAC;
1161       EXPAND_TAC "s";
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]);
1165     EXPAND_TAC "s";
1166     REWRITE_TAC[IN_ELIM_THM];
1167     REPEAT WEAK_STRIP_TAC;
1168     TYPIFY `r ( r x) = r ( r y)` (C SUBGOAL_THEN ASSUME_TAC);
1169       AP_TERM_TAC;
1170       BY(ASM_REWRITE_TAC[]);
1171     BY(ASM_MESON_TAC[BETA_BUMP_INVOLUTION]);
1172   DISCH_TAC;
1173   REWRITE_TAC[SURJ];
1174   ASM_REWRITE_TAC[];
1175   EXPAND_TAC "s";
1176   REWRITE_TAC[IN_ELIM_THM];
1177   REPEAT WEAK_STRIP_TAC;
1178   TYPIFY `r x` EXISTS_TAC;
1179   SUBCONJ_TAC;
1180     FIRST_X_ASSUM_ST `==>` MP_TAC;
1181     EXPAND_TAC "s";
1182     REWRITE_TAC[IN_ELIM_THM];
1183     BY(ASM_MESON_TAC[]);
1184   DISCH_TAC;
1185   BY(ASM_MESON_TAC[BETA_BUMP_INVOLUTION])
1186   ]);;
1187   (* }}} *)
1188
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`,
1192   (* {{{ proof *)
1193   [
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 }`];
1197   ANTS_TAC;
1198     EXPAND_TAC "s";
1199     REWRITE_TAC[IN_ELIM_THM;SUBSET];
1200     BY(MESON_TAC[]);
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`];
1204   ANTS_TAC;
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`];
1207   ANTS_TAC;
1208     EXPAND_TAC "s";
1209     REWRITE_TAC[IN_ELIM_THM];
1210     REWRITE_TAC[o_DEF];
1211     BY(ASM_MESON_TAC[BETA_BUMP_INVOLUTION_NEG]);
1212   DISCH_THEN SUBST1_TAC;
1213   REWRITE_TAC[SUM_NEG];
1214   BY(REAL_ARITH_TAC)
1215   ]);;
1216   (* }}} *)
1217
1218 let REAL_ABS_TRIANGLE_BOUND = prove_by_refinement(
1219   `!a b x.  a <= x /\ x <= b ==> abs x <= abs a + abs b`,
1220   (* {{{ proof *)
1221   [
1222   BY(REAL_ARITH_TAC)
1223   ]);;
1224   (* }}} *)
1225
1226 let CRITICAL_EDGEX_BOUND = prove_by_refinement(
1227   `?c1. !V X e. e IN critical_edgeX V X ==> abs(radV e - h0) <= c1`,
1228   (* {{{ proof *)
1229   [
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`];
1234   ASM_REWRITE_TAC[];
1235   BY(REAL_ARITH_TAC)
1236   ]);;
1237   (* }}} *)
1238
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))`,
1241   (* {{{ proof *)
1242   [
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;
1247   CONJ_TAC;
1248     BY(REAL_ARITH_TAC);
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];
1255   CONJ2_TAC;
1256     BY(REAL_ARITH_TAC);
1257   REWRITE_TAC[REAL_ABS_POW];
1258   MATCH_MP_TAC Collect_geom2.POS_IMP_POW2;
1259   ASM_REWRITE_TAC[];
1260   BY(REAL_ARITH_TAC)
1261   ]);;
1262   (* }}} *)
1263
1264 let BOUND_BETA_BUMP = prove_by_refinement(
1265  `?c. !V X e.
1266          saturated V /\ packing V /\ mcell_set V X /\ critical_edgeX V X e
1267          ==> beta_bump_v1 V e X <= c`,
1268   (* {{{ proof *)
1269   [
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];
1275   COND_CASES_TAC;
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;
1279     CONJ_TAC;
1280       BY(REAL_ARITH_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];
1289   BY(REAL_ARITH_TAC)
1290   ]);;
1291   (* }}} *)
1292
1293
1294 end;;