text_formalization/packing/TSKAJXY.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Packing                                                           *)
   5 (* Lemma: TSKAJXY                                                             *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2012-01-15                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11 (*
  12
  13 Remaining cases of TSKAJXY.
  14
  15 *)
  16
  17 flyspeck_needs "usr/thales/hales_tactic.hl";;
  18
  19 module Tskajxy = struct
  20
  21   open Hales_tactic;;
  22
  23 let GAMMAX_NULLSET = prove_by_refinement(
  24   `!V f X ul k. saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell k V ul) /\ NULLSET X ==>
  25   gammaX V X f = &0`,
  26   (* {{{ proof *)
  27   [
  28   REPEAT WEAK_STRIP_TAC;
  29   REWRITE_TAC[Pack_defs.gammaX];
  30   TYPIFY `total_solid V X = &0` (C SUBGOAL_THEN SUBST1_TAC);
  31     REWRITE_TAC[Pack_defs.total_solid];
  32     TYPIFY `(VX V X = {})` (C SUBGOAL_THEN SUBST1_TAC);
  33       ASM_REWRITE_TAC[];
  34       MATCH_MP_TAC Bump.VX_EMPTY;
  35       BY(ASM_MESON_TAC[]);
  36     BY(REWRITE_TAC[SUM_CLAUSES]);
  37   TYPIFY `(edgeX V X = {})` (C SUBGOAL_THEN SUBST1_TAC);
  38     ASM_REWRITE_TAC[];
  39     MATCH_MP_TAC Bump.RIJRIED;
  40     BY(ASM_MESON_TAC[]);
  41   REWRITE_TAC[SUM_CLAUSES];
  42   TYPIFY `vol X = &0` (C SUBGOAL_THEN SUBST1_TAC);
  43     BY(ASM_MESON_TAC[volume_props]);
  44   BY(REAL_ARITH_TAC)
  45   ]);;
  46   (* }}} *)
  47
  48 let GAMMAX_MCELL1 = prove_by_refinement(
  49   `!V X ul.  saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell1 V ul) /\ ~(NULLSET X) ==>
  50     gammaX V X lmfun = vol X - (&2 * mm1 /pi) * sol (EL 0 ul) X`,
  51   (* {{{ proof *)
  52   [
  53   REWRITE_TAC[Pack_defs.gammaX];
  54   REPEAT WEAK_STRIP_TAC;
  55   TYPIFY `edgeX V X = {}` (C SUBGOAL_THEN SUBST1_TAC);
  56     BY(ASM_MESON_TAC[Bump.EDGE_IMP_K2;Bump.MCELL1;arith `1 <= 1`]);
  57   REWRITE_TAC[SUM_CLAUSES;Pack_defs.total_solid;arith `x + y* &0 = x`];
  58   REPEAT AP_TERM_TAC;
  59   TYPIFY `VX V X = {EL 0 ul}` ENOUGH_TO_SHOW_TAC;
  60     DISCH_THEN SUBST1_TAC;
  61     BY(REWRITE_TAC[SUM_SING]);
  62   REWRITE_TAC[EL];
  63   MATCH_MP_TAC SUBSET_ANTISYM;
  64   CONJ_TAC;
  65     MATCH_MP_TAC SUBSET_TRANS;
  66     TYPIFY `V INTER X` EXISTS_TAC;
  67     CONJ_TAC;
  68       MATCH_MP_TAC Bump.HDTFNFZ_SUBSET;
  69       BY(ASM_MESON_TAC[Bump.MCELL1]);
  70     ASM_REWRITE_TAC[];
  71     MATCH_MP_TAC Bump.V_CELL1_SINGLE;
  72     BY(ASM_REWRITE_TAC[]);
  73   GMATCH_SIMP_TAC Hdtfnfz.HDTFNFZ;
  74   REWRITE_TAC[SUBSET;IN_SING;IN_INTER];
  75   CONJ_TAC;
  76     BY(ASM_MESON_TAC[Bump.MCELL1]);
  77   REPEAT WEAK_STRIP_TAC;
  78   ASM_REWRITE_TAC[];
  79   CONJ2_TAC;
  80     MATCH_MP_TAC Marchal_cells_3.HD_IN_MCELL;
  81     BY(ASM_MESON_TAC[NEGLIGIBLE_EMPTY;arith `~(1=0)`;Bump.MCELL1]);
  82   INTRO_TAC Packing3.BARV_SUBSET [`V`;`3`;`ul`];
  83   GMATCH_SIMP_TAC Bump.set_of_list4;
  84   REWRITE_TAC[EL;SUBSET;IN_INSERT;NOT_IN_EMPTY];
  85   BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3 + 1 = 4`])
  86   ]);;
  87   (* }}} *)
  88
  89 let MCELL2_VX_PROPS = prove_by_refinement(
  90   `!V X ul.  saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell2 V ul) /\ ~(NULLSET X) ==>
  91     (VX V X = {EL 0 ul,EL 1 ul}) /\ ~(EL 0 ul = EL 1 ul) /\ (edgeX V X = {{EL 0 ul, EL 1 ul}})`,
  92   (* {{{ proof *)
  93   [
  94   REWRITE_TAC[Pack_defs.gammaX];
  95   REPEAT WEAK_STRIP_TAC;
  96   TYPIFY `VX V X = {EL 0 ul, EL 1 ul}` (C SUBGOAL_THEN MP_TAC);
  97     GMATCH_SIMP_TAC Bump.HDTFNFZ_ALT;
  98     CONJ_TAC;
  99       BY(ASM_MESON_TAC[Bump.MCELL2]);
 100     ASM_REWRITE_TAC[Bump.MCELL2];
 101     GMATCH_SIMP_TAC Lepjbdj.LEPJBDJ;
 102     ASM_REWRITE_TAC[arith `1 <= 2 /\ 2 <= 4 /\ 2 -1 = 1`];
 103     CONJ_TAC;
 104       BY(ASM_MESON_TAC[NEGLIGIBLE_EMPTY;Bump.MCELL2]);
 105     MATCH_MP_TAC Bump.SET_OF_LIST_TRUNCATE_1;
 106     BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `2 <= 3 + 1`]);
 107   DISCH_TAC;
 108   TYPIFY `~(EL 0 ul = EL 1 ul)` (C SUBGOAL_THEN MP_TAC);
 109     INTRO_TAC Marchal_cells_3.BARV_CARD_LEMMA [`V`;`ul`;`3`];
 110     ASM_REWRITE_TAC[arith ` 3 + 1 = 4`];
 111     GMATCH_SIMP_TAC Bump.set_of_list4;
 112     CONJ_TAC;
 113       BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3 + 1 = 4`]);
 114     BY(MESON_TAC[Marchal_cells_2_new.CARD4_IMP_DISTINCT]);
 115   DISCH_TAC;
 116   TYPIFY `edgeX V X = {{EL 0 ul, EL 1 ul}}` (C SUBGOAL_THEN MP_TAC);
 117     REWRITE_TAC[Pack_defs.edgeX];
 118     REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ];
 119     TYPIFY `!w. VX V X w <=> w IN VX V X` (C SUBGOAL_THEN (unlist REWRITE_TAC));
 120       BY(SET_TAC[]);
 121     CONJ_TAC;
 122       ASM_REWRITE_TAC[SUBSET;IN_INSERT;IN_SING;IN_ELIM_THM];
 123       REBIND_TAC (`x:real^3->bool`,"A");
 124       GEN_TAC;
 125       REPEAT WEAK_STRIP_TAC;
 126             BY(ASM_MESON_TAC[]);
 127           BY(ASM_MESON_TAC[]);
 128         BY(ASM_REWRITE_TAC[] THEN SET_TAC[]);
 129       BY(ASM_MESON_TAC[]);
 130     REWRITE_TAC[SUBSET];
 131     ASM_REWRITE_TAC[];
 132     FIRST_X_ASSUM MP_TAC;
 133     BY(SET_TAC[]);
 134   BY(ASM_SIMP_TAC[])
 135   ]);;
 136   (* }}} *)
 137
 138 let GAMMAX_MCELL2 = prove_by_refinement(
 139   `!V X ul.  saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell2 V ul) /\ ~(NULLSET X) ==>
 140     gammaX V X lmfun = vol X - (&2 * mm1 /pi) * (sol (EL 0 ul) X + sol (EL 1 ul) X) +
 141        (&8*mm2/ pi) * lmfun (hl [EL 0 ul;EL 1 ul]) * dihX V X (EL 0 ul,EL 1 ul)`,
 142   (* {{{ proof *)
 143   [
 144   REWRITE_TAC[Pack_defs.gammaX];
 145   REPEAT WEAK_STRIP_TAC;
 146   TYPIFY `X IN mcell_set V` (C SUBGOAL_THEN ASSUME_TAC);
 147     REWRITE_TAC[Pack_defs.mcell_set;Bump.MCELL2;IN_ELIM_THM];
 148     BY(ASM_MESON_TAC[IN;Bump.MCELL2]);
 149   INTRO_TAC MCELL2_VX_PROPS [`V`;`X`;`ul`];
 150   ANTS_TAC;
 151     BY(ASM_REWRITE_TAC[]);
 152   REPEAT WEAK_STRIP_TAC;
 153   TYPIFY `total_solid V X = (sol (EL 0 ul) X + sol (EL 1 ul) X)` (C SUBGOAL_THEN SUBST1_TAC);
 154     ASM_REWRITE_TAC[Pack_defs.total_solid];
 155     ASM_REWRITE_TAC[];
 156     GMATCH_SIMP_TAC Geomdetail.SUM_DIS2;
 157     BY(ASM_REWRITE_TAC[]);
 158   ASM_REWRITE_TAC[IN_SING;SUM_SING];
 159   GMATCH_SIMP_TAC Marchal_cells_3.BETA_PAIR_THM;
 160   CONJ_TAC;
 161     REPEAT WEAK_STRIP_TAC;
 162     REWRITE_TAC[Pack_defs.HL;Bump.set_of_list2_explicit];
 163     TYPIFY `{v,u} = {u,v}` (C SUBGOAL_THEN SUBST1_TAC);
 164       BY(SET_TAC[]);
 165     COND_CASES_TAC;
 166       REWRITE_TAC[];
 167       AP_THM_TAC;
 168       AP_TERM_TAC;
 169       MATCH_MP_TAC Marchal_cells_3.DIHX_SYM;
 170       BY(ASM_MESON_TAC[IN_SING;IN]);
 171     BY(REWRITE_TAC[]);
 172   BY(REAL_ARITH_TAC)
 173   ]);;
 174   (* }}} *)
 175
 176 (* renamed from RCONE_GT_BALL_PLANE *)
 177
 178 let RCONE_GT_HYPERPLANE = prove_by_refinement(
 179   `!v0 v1 b t (p:real^A) r.
 180       p dot (v1 - v0) = b /\  ~(v1 = v0) /\ (&0 < t) /\  (b - v0 dot (v1 - v0) = r * t * dist(v1,v0))  ==>
 181        (p IN rcone_gt v0 v1 t <=> p IN ball (v0,r))`,
 182   (* {{{ proof *)
 183   [
 184   REWRITE_TAC[Sphere.rcone_gt;Sphere.rconesgn;ball;IN_ELIM_THM];
 185   REPEAT WEAK_STRIP_TAC;
 186   TYPIFY `(p - v0) dot (v1 - v0) = p dot (v1 - v0) - v0 dot (v1 - v0)` (C SUBGOAL_THEN SUBST1_TAC);
 187     BY(VECTOR_ARITH_TAC);
 188   ASM_REWRITE_TAC[];
 189   REWRITE_TAC[arith `dp * d * t > r * t * d <=> (&0  < d * t * (dp - r))`];
 190   GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
 191   ASM_REWRITE_TAC[];
 192   GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
 193   ASM_REWRITE_TAC[GSYM DIST_NZ];
 194   BY(MESON_TAC[DIST_SYM;arith `&0 < x - y <=> y < x`])
 195   ]);;
 196   (* }}} *)
 197
 198 let RCONE_GE_HYPERPLANE = prove_by_refinement(
 199   `!v0 v1 b t (p:real^A) r.
 200       p dot (v1 - v0) = b /\  ~(v1 = v0) /\ (&0 < t) /\  (b - v0 dot (v1 - v0) = r * t * dist(v1,v0))  ==>
 201        (p IN rcone_ge v0 v1 t <=> p IN cball (v0,r))`,
 202   (* {{{ proof *)
 203   [
 204   REWRITE_TAC[Sphere.rcone_ge;Sphere.rconesgn;cball;IN_ELIM_THM];
 205   REPEAT WEAK_STRIP_TAC;
 206   TYPIFY `(p - v0) dot (v1 - v0) = p dot (v1 - v0) - v0 dot (v1 - v0)` (C SUBGOAL_THEN SUBST1_TAC);
 207     BY(VECTOR_ARITH_TAC);
 208   ASM_REWRITE_TAC[];
 209   REWRITE_TAC[arith `dp * d * t >= r * t * d <=> (&0  <= d * t * (dp - r))`];
 210   GMATCH_SIMP_TAC REAL_LE_MUL_EQ;
 211   ASM_REWRITE_TAC[];
 212   GMATCH_SIMP_TAC REAL_LE_MUL_EQ;
 213   ASM_REWRITE_TAC[GSYM DIST_NZ];
 214   BY(MESON_TAC[DIST_SYM;arith `&0 <= x - y <=> y <= x`])
 215   ]);;
 216   (* }}} *)
 217
 218 (* renamed from BALL_DIFF_RCONE_GE *)
 219
 220 let BALL_DIFF_RCONE_GT = prove_by_refinement(
 221   `!u0 u1 (p:real^A) a r.
 222      p IN ball(u0,r) DIFF rcone_gt u0 u1 a /\ &0 <= a ==>
 223     p dot (u1 - u0) <= u0 dot (u1 - u0) + r * a * dist(u1,u0)`,
 224   (* {{{ proof *)
 225   [
 226   REWRITE_TAC[Sphere.rcone_gt;Sphere.rconesgn;ball;IN_ELIM_THM;IN_DIFF;arith `~(x > y) <=> (x <= y)`];
 227   REPEAT WEAK_STRIP_TAC;
 228   FIRST_X_ASSUM_ST `dot` MP_TAC;
 229   TYPIFY `(p - u0) dot (u1 - u0) = p dot (u1 - u0) - u0 dot (u1 - u0)` (C SUBGOAL_THEN SUBST1_TAC);
 230     BY(VECTOR_ARITH_TAC);
 231   TYPIFY `dist (p,u0) * dist (u1,u0) * a <= r * a * dist(u1,u0)` ENOUGH_TO_SHOW_TAC;
 232     BY(REAL_ARITH_TAC);
 233   MATCH_MP_TAC (arith `&0 <= (r - dp) * d1 * a ==> dp * d1 * a <= r * a * d1`);
 234   GMATCH_SIMP_TAC REAL_LE_MUL;
 235   CONJ_TAC;
 236     BY(ASM_MESON_TAC [arith `d < r ==> &0 <= r - d`;DIST_SYM]);
 237   GMATCH_SIMP_TAC REAL_LE_MUL;
 238   ASM_REWRITE_TAC[];
 239   BY(REWRITE_TAC[DIST_POS_LE])
 240   ]);;
 241   (* }}} *)
 242
 243 (* renamed from BALL_DIFF_RCONE_GT_BISECTOR *)
 244
 245 let BALL_DIFF_RCONE_GT_BISECTOR = prove_by_refinement(
 246   `!u0 u1 (p:real^A) r h.
 247     p IN ball(u0,r) DIFF rcone_gt u0 u1 (h/r) /\ &2 * h = dist(u1,u0) /\ &0 < r  ==>
 248     dist(p,u0) <= dist(p,u1)`,
 249   (* {{{ proof *)
 250   [
 251   REPEAT WEAK_STRIP_TAC;
 252   INTRO_TAC BALL_DIFF_RCONE_GT [`u0`;`u1`;`p`;`h/r`;`r`];
 253   ASM_REWRITE_TAC[];
 254   ANTS_TAC;
 255     GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
 256     ASM_REWRITE_TAC[arith `&0 * x = &0`];
 257     ONCE_REWRITE_TAC[arith `&0 <= h <=> &0 <= &2 * h`];
 258     BY(ASM_MESON_TAC[DIST_POS_LE]);
 259   TYPIFY `r * h / r * dist(u1,u0) = (dist(u1,u0)) pow 2 / &2` (C SUBGOAL_THEN SUBST1_TAC);
 260     FIRST_X_ASSUM (SUBST1_TAC o SYM);
 261     Calc_derivative.CALC_ID_TAC;
 262     BY((FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
 263   REWRITE_TAC[Leaf_cell.DIST_LE_HALF_PLANE];
 264   REWRITE_TAC[Collect_geom.DIST_POW2_DOT];
 265   MATCH_MP_TAC (arith `&2 * a + c -  b - &2 * b1  = &0 ==>     (a <= b1 + b / &2  ==> &0 <= c)`);
 266   BY(VECTOR_ARITH_TAC)
 267   ]);;
 268   (* }}} *)
 269
 270 let MCELL1_EXPLICIT = prove_by_refinement(
 271  `!V X ul. saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell1 V ul) /\ ~(NULLSET X) ==>
 272    (X = rogers V ul INTER cball (HD ul,sqrt (&2)) DIFF
 273  rcone_gt (HD ul) (HD (TL ul)) (hl (truncate_simplex 1 ul) / sqrt (&2)))`,
 274   (* {{{ proof *)
 275   [
 276   REWRITE_TAC[Pack_defs.mcell1];
 277   REPEAT WEAK_STRIP_TAC;
 278   TYPIFY `sqrt (&2) <= hl ul` (C SUBGOAL_THEN ASSUME_TAC);
 279     PROOF_BY_CONTR_TAC;
 280     FIRST_X_ASSUM_ST `rogers` MP_TAC;
 281     ASM_REWRITE_TAC[];
 282     BY(ASM_MESON_TAC[NEGLIGIBLE_EMPTY]);
 283   FIRST_X_ASSUM_ST `rogers` MP_TAC;
 284   BY(ASM_REWRITE_TAC[])
 285   ]);;
 286   (* }}} *)
 287
 288 let MCELL1_VOL_RESTRICT = prove_by_refinement(
 289   `!V X ul. saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell1 V ul) /\ ~(NULLSET X) ==>
 290     vol X = vol (X INTER ball(EL 0 ul, sqrt(&2)))`,
 291   (* {{{ proof *)
 292   [
 293   REPEAT WEAK_STRIP_TAC;
 294   TYPIFY `measurable X /\ measurable (X INTER ball(EL 0 ul, sqrt(&2)))` (C SUBGOAL_THEN ASSUME_TAC);
 295     SUBCONJ_TAC;
 296       BY(ASM_MESON_TAC[Urrphbz1.MEASURABLE_MCELL;Bump.MCELL1]);
 297     DISCH_TAC;
 298     MATCH_MP_TAC MEASURABLE_INTER;
 299     BY(ASM_REWRITE_TAC[MEASURABLE_BALL]);
 300   MATCH_MP_TAC Vol1.VOLUME_PROPS_SDIFF;
 301   ASM_REWRITE_TAC[SDIFF];
 302   MATCH_MP_TAC (CONJUNCT2 NULLSET_RULES);
 303   CONJ2_TAC;
 304     TYPIFY `!x. (x = {}) ==> NULLSET x` ENOUGH_TO_SHOW_TAC;
 305       DISCH_THEN MATCH_MP_TAC;
 306       BY(SET_TAC[]);
 307     BY(MESON_TAC[NEGLIGIBLE_EMPTY]);
 308   TYPIFY `X DIFF (X INTER ball(EL 0 ul,sqrt(&2))) SUBSET cball (EL 0 ul,sqrt(&2)) DIFF ball(EL 0 ul,sqrt(&2))` (C SUBGOAL_THEN ASSUME_TAC);
 309     TYPIFY `X SUBSET cball(EL 0 ul,sqrt(&2))` ENOUGH_TO_SHOW_TAC;
 310       BY(SET_TAC[]);
 311     INTRO_TAC MCELL1_EXPLICIT [`V`;`X`;`ul`];
 312     ASM_REWRITE_TAC[];
 313     DISCH_THEN SUBST1_TAC;
 314     REWRITE_TAC[EL];
 315     BY(SET_TAC[]);
 316   MATCH_MP_TAC NEGLIGIBLE_SUBSET;
 317   FIRST_X_ASSUM MP_TAC;
 318   TYPIFY `cball (EL 0 ul,sqrt(&2)) DIFF ball(EL 0 ul,sqrt(&2)) = {p | dist(EL 0 ul,p) = sqrt(&2)}` (C SUBGOAL_THEN SUBST1_TAC);
 319     REWRITE_TAC[EXTENSION;cball;ball;IN_ELIM_THM;IN_DIFF];
 320     BY(REAL_ARITH_TAC);
 321   ASM_REWRITE_TAC[];
 322   DISCH_TAC;
 323   TYPIFY `{p | dist(EL 0 ul,p) = sqrt(&2) }` EXISTS_TAC;
 324   ASM_REWRITE_TAC[];
 325   BY(REWRITE_TAC[NEGLIGIBLE_SPHERE])
 326   ]);;
 327   (* }}} *)
 328
 329 let MCELL1_SOL_RESTRICT = prove_by_refinement(
 330   `!V X ul. saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell1 V ul) /\ ~(NULLSET X) ==>
 331     sol (EL 0 ul) X = sol (EL 0 ul) (X INTER ball(EL 0 ul, sqrt(&2)))`,
 332   (* {{{ proof *)
 333   [
 334   REPEAT WEAK_STRIP_TAC;
 335   INTRO_TAC Urrphbz2.URRPHBZ2 [`V`;`ul`;`1`;`EL 0 ul`];
 336   ANTS_TAC;
 337     ASM_REWRITE_TAC[];
 338     INTRO_TAC Packing3.BARV_SUBSET [`V`;`3`;`ul`];
 339     ASM_REWRITE_TAC[];
 340     GMATCH_SIMP_TAC Bump.set_of_list4;
 341     CONJ2_TAC;
 342       BY(SET_TAC[]);
 343     BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`]);
 344   REWRITE_TAC[Sphere.eventually_radial];
 345   REPEAT WEAK_STRIP_TAC;
 346   TYPIFY `?r'. (&0 < r' /\ r' <= r /\ r' <= sqrt(&2))` (C SUBGOAL_THEN ASSUME_TAC);
 347     EXISTS_TAC `if (r <= sqrt(&2)) then r else sqrt(&2)`;
 348     COND_CASES_TAC;
 349       BY(ASM_SIMP_TAC[arith `r > &0 ==> &0 < r`;arith `r <= r`]);
 350     ASM_SIMP_TAC[arith `s <= s`;arith `~(r <= s) ==> (s <= r)`];
 351     GMATCH_SIMP_TAC REAL_LT_RSQRT;
 352     BY(REAL_ARITH_TAC);
 353   FIRST_X_ASSUM MP_TAC THEN WEAK_STRIP_TAC;
 354   INTRO_TAC Conforming.RADIAL_NORM_CO [`r`;`r'`;`EL 0 ul`;`X`];
 355   ASM_REWRITE_TAC[GSYM Marchal_cells_2_new.RADIAL_VS_RADIAL_NORM;Bump.MCELL1;NORMBALL_BALL];
 356   REPEAT WEAK_STRIP_TAC;
 357   INTRO_TAC Vol1.sol [`EL 0 ul`;`X`;`r'`];
 358   INTRO_TAC Vol1.sol [`EL 0 ul`;`X INTER ball (EL 0 ul,sqrt(&2))`;`r'`];
 359   ASM_REWRITE_TAC[arith `r' > &0 <=> &0 < r'`;NORMBALL_BALL;INTER_ASSOC;GSYM Marchal_cells_2_new.RADIAL_VS_RADIAL_NORM;Bump.MCELL1];
 360   TYPIFY ` ball(EL 0 ul,sqrt(&2)) INTER ball(EL 0 ul,r') = ball(EL 0 ul,r')` (C SUBGOAL_THEN SUBST1_TAC);
 361     REWRITE_TAC[ball;EXTENSION;IN_ELIM_THM;IN_INTER];
 362     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
 363   TYPIFY `measurable (mcell 1 V ul INTER ball (EL 0 ul,r'))` (C SUBGOAL_THEN ((unlist ASM_REWRITE_TAC)));
 364     MATCH_MP_TAC MEASURABLE_INTER;
 365     CONJ2_TAC;
 366       BY(ASM_REWRITE_TAC[MEASURABLE_BALL]);
 367     BY(ASM_MESON_TAC[Urrphbz1.MEASURABLE_MCELL;Bump.MCELL1]);
 368   BY(REAL_ARITH_TAC)
 369   ]);;
 370   (* }}} *)
 371
 372 let CONV_CONVEX_HULL = prove_by_refinement(
 373   `!(s:real^A->bool). conv s = convex hull s`,
 374   (* {{{ proof *)
 375   [
 376   BY(REWRITE_TAC[Geomdetail.conv;aff_ge_def;CONVEX_HULL_AFF_GE])
 377   ]);;
 378   (* }}} *)
 379
 380 let CONVEX_HULL_4_AFF_GE = prove_by_refinement(
 381   `!(w0:real^3) w1 w2 w3.  ~coplanar {w0,w1, w2,w3} ==>
 382     (convex hull {w0,w1,w2,w3} = aff_ge {w0} {w1,w2,w3} INTER aff_ge {w1,w2,w3} {w0})`,
 383   (* {{{ proof *)
 384   [
 385   REPEAT WEAK_STRIP_TAC;
 386   INTRO_TAC DIMINDEX_3 [];
 387   DISCH_TAC;
 388   INTRO_TAC Collect_geom2.ARIKWRQ [`w0`;`w1`;`w2`;`w3`];
 389   REWRITE_TAC[LET_DEF;LET_END_DEF;CONV_CONVEX_HULL];
 390   TYPIFY `~coplanar_alt {w0,w1,w2,w3}` (C SUBGOAL_THEN ASSUME_TAC);
 391     BY(ASM_MESON_TAC[Leaf_cell.coplanar_eq_coplanar_alt;arith `2 <= 3`]);
 392   ASM_REWRITE_TAC[];
 393   TYPIFY `CARD {w0,w1,w2,w3} = 4` (C SUBGOAL_THEN ASSUME_TAC);
 394     MATCH_MP_TAC Collect_geom2.NOT_COPLANAR_IMP_CARD4;
 395     BY(ASM_REWRITE_TAC[]);
 396   ASM_REWRITE_TAC[];
 397   DISCH_THEN SUBST1_TAC;
 398   TYPIFY `({w0,w1,w2,w3} DIFF {w0} = {w1,w2,w3}) /\ ({w0,w1,w2,w3} DIFF {w1} = {w0,w2,w3}) /\ ({w0,w1,w2,w3} DIFF {w2} = {w0,w3,w1} ) /\ ({w0,w1,w2,w3} DIFF {w3} = {w0,w1,w2})` (C SUBGOAL_THEN (unlist REWRITE_TAC));
 399     FIRST_X_ASSUM (MP_TAC o (MATCH_MP Leaf_cell.CARD4_ALL_DISTINCT));
 400     BY(SET_TAC[]);
 401   INTRO_TAC Cfyxfty.inter_aff_ge_3_1_is_aff_ge_1_3 [`w0`;`w1`;`w2`;`w3`];
 402   ASM_REWRITE_TAC[];
 403   BY(SET_TAC[])
 404   ]);;
 405   (* }}} *)
 406
 407 let RADIAL_ALT = prove_by_refinement(
 408   `!(x:real^A) r A. radial r x A <=> (A SUBSET ball(x,r) /\
 409     (!y t. &0 < t /\ y IN A /\ x + t % (y- x) IN ball(x,r) ==> x + t % (y - x)
 410   IN A))`,
 411   (* {{{ proof *)
 412   [
 413   REPEAT WEAK_STRIP_TAC;
 414   REWRITE_TAC[Sphere.radial];
 415   TYPIFY `A SUBSET ball(x,r)` ASM_CASES_TAC;
 416     ASM_REWRITE_TAC[];
 417     MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a = b)`);
 418     CONJ_TAC;
 419       REPEAT WEAK_STRIP_TAC;
 420       FIRST_X_ASSUM (C INTRO_TAC [`y - (x:real^A)`]);
 421       ANTS_TAC;
 422         TYPIFY `x + y - x = (y:real^A)` (C SUBGOAL_THEN SUBST1_TAC);
 423           BY(VECTOR_ARITH_TAC);
 424         BY(ASM_REWRITE_TAC[]);
 425       DISCH_THEN (C INTRO_TAC [`t`]);
 426       DISCH_THEN MATCH_MP_TAC;
 427       ASM_SIMP_TAC[arith `&0 < t ==> t > &0`];
 428       FIRST_X_ASSUM MP_TAC;
 429       REWRITE_TAC[ball;IN_ELIM_THM;dist];
 430       TYPIFY `x - (x + t % (y - x)) = (-- t) % (y - x)` (C SUBGOAL_THEN SUBST1_TAC);
 431         BY(VECTOR_ARITH_TAC);
 432       REWRITE_TAC[NORM_MUL];
 433       BY(ASM_SIMP_TAC[arith `&0 < t ==> abs (-- t) = t`]);
 434     COMMENT "second direction";
 435     REPEAT WEAK_STRIP_TAC;
 436     FIRST_X_ASSUM_ST `ball` (C INTRO_TAC [`x + (u:real^A)`;`t`]);
 437     TYPIFY `(x + u) - x = (u:real^A)` (C SUBGOAL_THEN SUBST1_TAC);
 438       BY(VECTOR_ARITH_TAC);
 439     DISCH_THEN MATCH_MP_TAC;
 440     ASM_SIMP_TAC[arith `t > &0 ==> &0 < t`];
 441     FIRST_X_ASSUM MP_TAC;
 442     REWRITE_TAC[ball;IN_ELIM_THM;dist;varith `x - (x + t % u) = (-- t) % (u:real^A)`;NORM_MUL];
 443     BY(ASM_SIMP_TAC[arith `t > &0 ==> abs(-- t) = t`]);
 444   BY(ASM_REWRITE_TAC[])
 445   ]);;
 446   (* }}} *)
 447
 448 let CONVEX_HULL_SCALE = prove_by_refinement(
 449   `!(w0:real^3) w1 w2 w3 w t.   ~coplanar {w0,w1,w2,w3} /\ w IN convex hull {w0,w1,w2,w3} /\ &0 <= t /\
 450   (w0 + t % (w - w0) IN aff_ge {w1,w2,w3} {w0} ) ==>
 451    (w0 + t % (w - w0) IN convex hull {w0,w1,w2,w3})`,
 452   (* {{{ proof *)
 453   [
 454   REPEAT WEAK_STRIP_TAC;
 455   ASM_SIMP_TAC[CONVEX_HULL_4_AFF_GE];
 456   REPEAT WEAK_STRIP_TAC;
 457   ASM_SIMP_TAC[CONVEX_HULL_4_AFF_GE];
 458   ASM_REWRITE_TAC[IN_INTER];
 459   TYPIFY `DISJOINT {w0} {w1,w2,w3}` (C SUBGOAL_THEN ASSUME_TAC);
 460     BY(ASM_MESON_TAC[Planarity.notcoplanar_disjoints]);
 461   ASM_SIMP_TAC[ Planarity.AFF_GE_1_3];
 462   REWRITE_TAC[IN_ELIM_THM];
 463   FIRST_X_ASSUM_ST `convex` MP_TAC;
 464   REWRITE_TAC[Marchal_cells_2_new.CONVEX_HULL_4;IN_ELIM_THM];
 465   REPEAT WEAK_STRIP_TAC;
 466   ASM_REWRITE_TAC[];
 467   GEXISTL_TAC [`&1 + t * (u - &1)`;`t * v`;`t * w'`;`t * z`];
 468   GMATCH_SIMP_TAC REAL_LE_MUL;
 469   GMATCH_SIMP_TAC REAL_LE_MUL;
 470   GMATCH_SIMP_TAC REAL_LE_MUL;
 471   ASM_REWRITE_TAC[];
 472   CONJ_TAC;
 473     FIRST_X_ASSUM_ST `&1` MP_TAC;
 474     BY(CONV_TAC REAL_RING);
 475   BY(VECTOR_ARITH_TAC)
 476   ]);;
 477   (* }}} *)
 478
 479 let IMAGE_4_EXPLICIT = prove_by_refinement(
 480   `!(f:num->B).  { f i | i <= 3 } = {f 0 , f 1 ,f 2, f 3}`,
 481   (* {{{ proof *)
 482   [
 483   REPEAT WEAK_STRIP_TAC;
 484   REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_INSERT;NOT_IN_EMPTY];
 485   REWRITE_TAC[arith `i <= 3 <=> (i = 0 \/ i = 1 \/ i = 2 \/ i = 3)`];
 486   BY(MESON_TAC[])
 487   ]);;
 488   (* }}} *)
 489
 490 let NULLSET_MCELL1 = prove_by_refinement(
 491   `!V ul. packing V /\ saturated V /\ ul IN barV V 3 /\ ~NULLSET (mcell1 V ul) ==> ~NULLSET (rogers V ul)`,
 492   (* {{{ proof *)
 493   [
 494   REPEAT WEAK_STRIP_TAC;
 495   INTRO_TAC MCELL1_EXPLICIT [`V`;`mcell1 V ul`;`ul`];
 496   ANTS_TAC;
 497     ASM_REWRITE_TAC[];
 498     BY(ASM_MESON_TAC[IN]);
 499   DISCH_TAC;
 500   TYPIFY `mcell1 V ul SUBSET rogers V ul` (C SUBGOAL_THEN ASSUME_TAC);
 501     FIRST_X_ASSUM MP_TAC;
 502     BY(SET_TAC[]);
 503   BY(ASM_MESON_TAC[NEGLIGIBLE_SUBSET])
 504   ]);;
 505   (* }}} *)
 506
 507 let NOT_COPLANAR_OMEGA_LIST_N = prove_by_refinement(
 508   `!V ul. packing V /\ saturated V /\ ul IN barV V 3 /\ ~NULLSET (mcell1 V ul) ==>
 509         ~coplanar { omega_list_n V ul i | i <= 3}`,
 510   (* {{{ proof *)
 511   [
 512   REWRITE_TAC[coplanar];
 513   REWRITE_TAC[IMAGE_4_EXPLICIT];
 514   REPEAT WEAK_STRIP_TAC;
 515   INTRO_TAC NULLSET_MCELL1 [`V`;`ul`];
 516   ASM_REWRITE_TAC[];
 517   GMATCH_SIMP_TAC Marchal_cells_2_new.ROGERS_EXPLICIT;
 518   REWRITE_TAC[GSYM Sphere.OMEGA_LIST_N];
 519   ASM_REWRITE_TAC[];
 520   CONJ_TAC;
 521     BY(ASM_MESON_TAC[IN]);
 522   TYPED_ABBREV_TAC `s = {omega_list_n V ul 0, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`;
 523   TYPIFY `convex hull s SUBSET affine hull {u,v,w}` (C SUBGOAL_THEN ASSUME_TAC);
 524     MATCH_MP_TAC SUBSET_TRANS;
 525     TYPIFY `affine hull s` EXISTS_TAC;
 526     REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL];
 527     INTRO_TAC Marchal_cells_2_new.AFFINE_SUBSET_KY_LEMMA [`s`;`affine hull {u,v,w}`];
 528     REWRITE_TAC[Planarity.AFFINE_HULL_AFFINE_EQ];
 529     DISCH_THEN MATCH_MP_TAC;
 530     BY(ASM_REWRITE_TAC[]);
 531   TYPIFY `convex hull s SUBSET affine hull {u,v,w}` ENOUGH_TO_SHOW_TAC;
 532     BY(ASM_MESON_TAC[NEGLIGIBLE_AFFINE_HULL_3;NEGLIGIBLE_SUBSET]);
 533   BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[])
 534   ]);;
 535   (* }}} *)
 536
 537 let NOT_COPLANAR_R3 = prove_by_refinement(
 538   `!s. ~coplanar s ==> affine hull s = (:real^3)`,
 539   (* {{{ proof *)
 540   [
 541   REPEAT WEAK_STRIP_TAC;
 542   INTRO_TAC AFF_DIM_EQ_FULL [`s`];
 543   INTRO_TAC AFF_DIM_LE_UNIV [`s`];
 544   REWRITE_TAC[DIMINDEX_3];
 545   BY(ASM_MESON_TAC[Rogers.AFF_DIM_LE_2_IMP_COPLANAR;INT_ARITH `~(x <= int_of_num 2) /\ x <= &3 ==> x = &3`])
 546   ]);;
 547   (* }}} *)
 548
 549 let BARV_DISTINCT = prove_by_refinement(
 550   `!V ul. packing V /\ saturated V /\ ul IN barV V 1 ==>
 551     ~(EL 0 ul = EL 1 ul)`,
 552   (* {{{ proof *)
 553   [
 554   REPEAT WEAK_STRIP_TAC;
 555   INTRO_TAC Packing3.TRUNCATE_SIMPLEX_BARV [`V`;`0`;`1`;`ul`];
 556   ANTS_TAC;
 557     BY(ASM_MESON_TAC[IN;arith `0 <= 1`]);
 558   FIRST_X_ASSUM_ST `barV` MP_TAC;
 559   REWRITE_TAC[Sphere.BARV;IN;Sphere.VORONOI_NONDG];
 560   REWRITE_TAC[Sphere.VORONOI_LIST;Sphere.VORONOI_SET];
 561   REPEAT WEAK_STRIP_TAC;
 562   (FIRST_X_ASSUM (C INTRO_TAC [`truncate_simplex 0 ul`]));
 563   (FIRST_X_ASSUM (C INTRO_TAC [`ul`]));
 564   ASM_REWRITE_TAC[Packing3.INITIAL_SUBLIST_REFL;arith `0 < 1 + 1 /\ 0 < 0 + 1 /\ 1 + 1 < 5 /\ 0 + 1 < 5`];
 565   REWRITE_TAC[arith `1 + 1 = 2 /\ 0 + 1 = 1`];
 566   TYPIFY `set_of_list (truncate_simplex 0 ul) = set_of_list ul` ENOUGH_TO_SHOW_TAC;
 567     DISCH_THEN SUBST1_TAC;
 568     BY(INT_ARITH_TAC);
 569   GMATCH_SIMP_TAC Packing3.TRUNCATE_0_EQ_HEAD;
 570   REWRITE_TAC[set_of_list];
 571   GMATCH_SIMP_TAC Bump.set_of_list2;
 572   FIRST_X_ASSUM SUBST1_TAC;
 573   FIRST_X_ASSUM SUBST1_TAC;
 574   FIRST_X_ASSUM (SUBST1_TAC o GSYM);
 575   REWRITE_TAC[arith `1 + 1 = 2 /\ 1 <= 1 + 1`;EL];
 576   BY(SET_TAC[])
 577   ]);;
 578   (* }}} *)
 579
 580 let OMEGA_LIST_BISECTOR = prove_by_refinement(
 581   `!V ul. packing V /\ saturated V /\ ul IN barV V 3 /\ ~NULLSET (mcell1 V ul) ==>
 582     aff_ge  {omega_list_n V ul 1, omega_list_n V ul 2,  omega_list_n V ul 3} {EL 0 ul} =
 583       bis_le (EL 0 ul) (EL 1 ul)`,
 584   (* {{{ proof *)
 585   [
 586   REWRITE_TAC[Sphere.bis_le;EXTENSION;IN_ELIM_THM];
 587   REPEAT WEAK_STRIP_TAC;
 588   INTRO_TAC NOT_COPLANAR_OMEGA_LIST_N [`V`;`ul`];
 589   ANTS_TAC;
 590     BY(ASM_REWRITE_TAC[]);
 591   ASM_REWRITE_TAC[IMAGE_4_EXPLICIT];
 592   REWRITE_TAC[Sphere.OMEGA_LIST_N;GSYM EL];
 593   DISCH_TAC;
 594   GMATCH_SIMP_TAC Cfyxfty.AFF_GE_3_1;
 595   SUBCONJ_TAC;
 596     ONCE_REWRITE_TAC[DISJOINT_SYM];
 597     BY(ASM_MESON_TAC[Planarity.notcoplanar_disjoints]);
 598   DISCH_TAC;
 599   REWRITE_TAC[IN_ELIM_THM];
 600   TYPIFY `!t1 t2 t3 t4.  t1 + t2 + t3 + t4 = &1 /\ x = t1 % omega_list_n V ul 1 + t2 % omega_list_n V ul 2 + t3 % omega_list_n V ul 3 + t4 % EL 0 ul ==> (&0 <= t4 <=> dist(x,EL 0 ul) <= dist(x, EL 1 ul))` ENOUGH_TO_SHOW_TAC;
 601     REPEAT WEAK_STRIP_TAC;
 602     MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a = b)`);
 603     CONJ_TAC;
 604       REPEAT WEAK_STRIP_TAC;
 605       BY(ASM_MESON_TAC[]);
 606     DISCH_TAC;
 607     FIRST_X_ASSUM_ST `coplanar` MP_TAC;
 608     TYPIFY `!a b c d. {a,b,c,d} = {b,c,d,(a:real^3)}` (C SUBGOAL_THEN (unlist ONCE_REWRITE_TAC));
 609       BY(SET_TAC[]);
 610     DISCH_THEN (MP_TAC o (MATCH_MP NOT_COPLANAR_R3));
 611     REWRITE_TAC[Collect_geom2.AFFINE_HULL_4;EXTENSION;IN_UNIV;IN_ELIM_THM];
 612     BY(ASM_MESON_TAC[]);
 613   REPEAT WEAK_STRIP_TAC;
 614   TYPIFY `dist(omega_list_n V ul 1,EL 0 ul) = dist(omega_list_n V ul 1,EL 1 ul) /\ dist(omega_list_n V ul 2,EL 0 ul) = dist(omega_list_n V ul 2,EL 1 ul) /\ dist(omega_list_n V ul 3,EL 0 ul) = dist(omega_list_n V ul 3,EL 1 ul)` (C SUBGOAL_THEN ASSUME_TAC);
 615     INTRO_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN [`V`;`ul`;`3`;`1`];
 616     DISCH_TAC;
 617     FIRST_ASSUM (C INTRO_TAC [`1`]);
 618     FIRST_ASSUM (C INTRO_TAC [`2`]);
 619     FIRST_X_ASSUM (C INTRO_TAC [`3`]);
 620     ASM_REWRITE_TAC[arith `1 <= 3 /\ 3 <= 3 /\ 1 <= 2 /\ 2 <= 3 /\ 1 <= 1`];
 621     TYPIFY `barV V 3 ul` (C SUBGOAL_THEN (unlist REWRITE_TAC));
 622       BY(ASM_MESON_TAC[IN]);
 623     INTRO_TAC Leaf_cell.VORONOI_LIST_EQ [`V`;`truncate_simplex 1 ul`];
 624     TYPIFY `set_of_list (truncate_simplex 1 ul) = {EL 0 ul, EL 1 ul}` (C SUBGOAL_THEN SUBST1_TAC);
 625       MATCH_MP_TAC Bump.SET_OF_LIST_TRUNCATE_1;
 626       BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `2 <= 3 + 1`]);
 627     REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
 628     ONCE_REWRITE_TAC[MESON[] `(!x y. P x y) = !y x. P x y`];
 629     DISCH_THEN (C INTRO_TAC [`1`]);
 630     TYPIFY `barV V 1 (truncate_simplex 1 ul)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
 631       MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV;
 632       EXISTS_TAC `3`;
 633       BY(ASM_MESON_TAC[IN;arith `1 <= 3`]);
 634     BY(MESON_TAC[]);
 635   FIRST_X_ASSUM MP_TAC;
 636   REWRITE_TAC[Leaf_cell.DIST_EQ_HALF_PLANE];
 637   ASM_REWRITE_TAC[Leaf_cell.DIST_LE_HALF_PLANE];
 638   TYPED_ABBREV_TAC `(n:real^3) = (EL 0 ul - EL 1 ul)`;
 639   TYPED_ABBREV_TAC `(m:real^3) = (EL 0 ul + EL 1 ul)`;
 640   TYPIFY `n dot      (&2 %      (t1 % omega_list_n V ul 1 +       t2 % omega_list_n V ul 2 +       t3 % omega_list_n V ul 3 +       t4 % EL 0 ul) -  m) = t1 * n dot (&2 % omega_list_n V ul 1 - m) + t2 * n dot (&2 % omega_list_n V ul 2 - m) + t3 * n dot (&2 % omega_list_n V ul 3 - m) + t4 * n dot (&2 % EL 0 ul - m)` (C SUBGOAL_THEN SUBST1_TAC);
 641     FIRST_X_ASSUM (MP_TAC o (MATCH_MP (arith `t1 + t2 + t3 + t4 = &1 ==> t4 = &1 - t1 - t2 - t3`)));
 642     DISCH_THEN SUBST1_TAC;
 643     BY(VECTOR_ARITH_TAC);
 644   DISCH_THEN ((unlist REWRITE_TAC) o GSYM);
 645   REWRITE_TAC[arith `x * &0 = &0 /\ &0 + x = x`];
 646   MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a = b)`);
 647   CONJ_TAC;
 648     DISCH_TAC;
 649     GMATCH_SIMP_TAC REAL_LE_MUL;
 650     ASM_REWRITE_TAC[];
 651     EXPAND_TAC "n";
 652     EXPAND_TAC "m";
 653     BY(REWRITE_TAC[GSYM Leaf_cell.DIST_LE_HALF_PLANE;DIST_REFL;DIST_POS_LE]);
 654   COMMENT "other direction";
 655   TYPIFY `&0 < (n dot (&2 % EL 0 ul - m))` ENOUGH_TO_SHOW_TAC;
 656     REPEAT WEAK_STRIP_TAC;
 657     MATCH_MP_TAC Real_ext.REAL_PROP_NN_RCANCEL;
 658     BY(ASM_MESON_TAC[]);
 659   EXPAND_TAC "n";
 660   EXPAND_TAC "m";
 661   REWRITE_TAC[GSYM Collect_geom.DIST_LT_HALF_PLANE];
 662   REWRITE_TAC[DIST_REFL];
 663   MATCH_MP_TAC DIST_POS_LT;
 664   INTRO_TAC BARV_DISTINCT [`V`;`truncate_simplex 1 ul`];
 665   ANTS_TAC;
 666     ASM_REWRITE_TAC[IN];
 667     MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV;
 668     BY(ASM_MESON_TAC[IN;arith `1 <= 3`]);
 669   REPEAT (GMATCH_SIMP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
 670   BY(ASM_MESON_TAC[arith `1 + 1 <= 3 + 1 /\ 1 <= 1 /\ 0 <= 1`;IN;Sphere.BARV])
 671   ]);;
 672   (* }}} *)
 673
 674 let DIFF_INTER = prove_by_refinement(
 675   `!(X:A->bool) Y Z. (X DIFF Y) INTER Z = (X INTER Z) DIFF Y`,
 676   (* {{{ proof *)
 677   [
 678   BY(SET_TAC[])
 679   ]);;
 680   (* }}} *)
 681
 682 let RCONE_GT_SCALE = prove_by_refinement(
 683   `!u0 u1 (u:real^A) a t. &0 < t /\ u0 + u IN rcone_gt u0 u1 a ==> u0 + t % u IN rcone_gt u0 u1 a`,
 684   (* {{{ proof *)
 685   [
 686   REWRITE_TAC[rcone_gt;rconesgn;IN_ELIM_THM;dist];
 687   REWRITE_TAC[varith `!(v:real^A). (u0 + v) - u0 = v`];
 688   REWRITE_TAC[NORM_MUL;DOT_LMUL;arith `x > y <=> y < x`];
 689   REPEAT WEAK_STRIP_TAC;
 690   ASM_SIMP_TAC[arith `&0 < t ==> abs t = t`];
 691   REWRITE_TAC[GSYM REAL_MUL_ASSOC];
 692   GMATCH_SIMP_TAC REAL_LT_LMUL_EQ;
 693   BY(ASM_REWRITE_TAC[])
 694   ]);;
 695   (* }}} *)
 696
 697 let BARV3_TRUNC1 = prove_by_refinement(
 698   `!V ul. ul IN barV V 3 ==> truncate_simplex 1 ul = [EL 0 ul;EL 1 ul]`,
 699   (* {{{ proof *)
 700   [
 701   REPEAT WEAK_STRIP_TAC;
 702   TYPIFY `ul = [EL 0 ul;EL 1 ul; EL 2 ul; EL 3 ul]` (C SUBGOAL_THEN ASSUME_TAC);
 703     MATCH_MP_TAC Bump.LENGTH4;
 704     BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3+1 = 4`]);
 705   BY(ASM_MESON_TAC[Marchal_cells.TRUNCATE_SIMPLEX_EXPLICIT_1])
 706   ]);;
 707   (* }}} *)
 708
 709 let MCELL1_RADIAL = prove_by_refinement(
 710   `!V X ul. saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell1 V ul) /\ ~(NULLSET X) ==>
 711     radial (sqrt(&2)) (EL 0 ul) (X INTER ball(EL 0 ul,sqrt (&2)))
 712 `,
 713   (* {{{ proof *)
 714   [
 715   REPEAT WEAK_STRIP_TAC;
 716   REWRITE_TAC[Sphere.radial];
 717   CONJ_TAC;
 718     BY(SET_TAC[]);
 719   ASM_REWRITE_TAC[];
 720   INTRO_TAC MCELL1_EXPLICIT [`V`;`mcell1 V ul`;`ul`];
 721   ANTS_TAC;
 722     BY(ASM_MESON_TAC[]);
 723   REWRITE_TAC[Bump.MCELL1];
 724   DISCH_THEN SUBST1_TAC;
 725   REWRITE_TAC [GSYM EL];
 726   REPEAT WEAK_STRIP_TAC;
 727   TYPIFY `ball (EL 0 ul,sqrt(&2)) SUBSET cball(EL 0 ul,sqrt(&2))` (C SUBGOAL_THEN ASSUME_TAC);
 728     BY(REWRITE_TAC[BALL_SUBSET_CBALL]);
 729   FIRST_X_ASSUM_ST `rogers` MP_TAC;
 730   TYPIFY `((rogers V ul INTER cball (EL 0 ul,sqrt(&2))) DIFF rcone_gt (EL 0 ul) (EL (SUC 0) ul) (hl (truncate_simplex 1 ul) / sqrt (&2))) INTER  ball (EL 0 ul,sqrt (&2)) = (rogers V ul INTER ball (EL 0 ul,sqrt(&2))) DIFF rcone_gt (EL 0 ul) (EL (SUC 0) ul) (hl (truncate_simplex 1 ul) / sqrt (&2))` (C SUBGOAL_THEN SUBST1_TAC);
 731     REWRITE_TAC[GSYM DIFF_INTER];
 732     FIRST_X_ASSUM MP_TAC;
 733     REWRITE_TAC[ INTER_ASSOC];
 734     BY(SET_TAC[]);
 735   REWRITE_TAC[IN_INTER;IN_DIFF];
 736   REPEAT WEAK_STRIP_TAC;
 737   TYPIFY `~(EL 0 ul = EL 1 ul)` (C SUBGOAL_THEN ASSUME_TAC);
 738     INTRO_TAC BARV_DISTINCT [`V`;`truncate_simplex 1 ul`];
 739     ANTS_TAC;
 740       ASM_REWRITE_TAC[IN];
 741       MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV;
 742       BY(ASM_MESON_TAC[IN;arith `1 <= 3`]);
 743     REPEAT (GMATCH_SIMP_TAC Packing3.EL_TRUNCATE_SIMPLEX);
 744     BY(ASM_MESON_TAC[arith `1 + 1 <= 3 + 1 /\ 1 <= 1 /\ 0 <= 1`;IN;Sphere.BARV]);
 745   MATCH_MP_TAC (TAUT `a /\ b ==> b /\ a`);
 746   SUBCONJ_TAC;
 747     REPEAT (FIRST_X_ASSUM_ST `SUC` MP_TAC);
 748     REWRITE_TAC[arith `SUC 0 = 1`];
 749     REPEAT WEAK_STRIP_TAC;
 750     FIRST_X_ASSUM_ST `~` MP_TAC;
 751     REWRITE_TAC[];
 752     TYPIFY `EL 0 ul + u = (EL 0 ul + (&1/t) % (t % u))` (C SUBGOAL_THEN SUBST1_TAC);
 753       REWRITE_TAC[VECTOR_MUL_ASSOC];
 754       TYPIFY `(&1 / t) * t = &1` ENOUGH_TO_SHOW_TAC;
 755         DISCH_THEN SUBST1_TAC;
 756         BY(VECTOR_ARITH_TAC);
 757       Calc_derivative.CALC_ID_TAC;
 758       BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
 759     MATCH_MP_TAC RCONE_GT_SCALE;
 760     GMATCH_SIMP_TAC REAL_LT_DIV;
 761     ASM_REWRITE_TAC[];
 762     BY(ASM_REWRITE_TAC[arith `&0 < &1 /\ ( &0 < t <=> t > &0)`]);
 763   COMMENT "down to 1";
 764   DISCH_TAC;
 765   MATCH_MP_TAC (TAUT `a /\ b ==> b /\ a`);
 766   SUBCONJ_TAC;
 767     REWRITE_TAC[ball;IN_ELIM_THM;dist];
 768     TYPIFY `!u v. (u:real^3) - (u + t % v) = (-- t) % v` (C SUBGOAL_THEN (unlist REWRITE_TAC));
 769       BY(VECTOR_ARITH_TAC);
 770     REWRITE_TAC[NORM_MUL];
 771     BY(ASM_SIMP_TAC[arith `t > &0 ==> abs(-- t) = t`]);
 772   DISCH_TAC;
 773   COMMENT "last goal";
 774   FIRST_X_ASSUM_ST `rogers` MP_TAC;
 775   REPEAT (GMATCH_SIMP_TAC Marchal_cells_2_new.ROGERS_EXPLICIT);
 776   ASM_REWRITE_TAC[GSYM EL];
 777   TYPED_ABBREV_TAC `(w:real^3) = EL 0 ul + u`;
 778   TYPIFY `t % u = t % (w - EL 0 ul)` (C SUBGOAL_THEN SUBST1_TAC);
 779     EXPAND_TAC "w";
 780     BY(VECTOR_ARITH_TAC);
 781   DISCH_TAC;
 782   MATCH_MP_TAC CONVEX_HULL_SCALE;
 783   ASM_SIMP_TAC[arith `t > &0 ==> &0 <= t`];
 784   SUBCONJ_TAC;
 785     INTRO_TAC NOT_COPLANAR_OMEGA_LIST_N [`V`;`ul`];
 786     ANTS_TAC;
 787       BY(ASM_MESON_TAC[IN]);
 788     REWRITE_TAC[IMAGE_4_EXPLICIT];
 789     BY(MESON_TAC[Sphere.OMEGA_LIST_N;EL]);
 790   DISCH_TAC;
 791   GMATCH_SIMP_TAC OMEGA_LIST_BISECTOR;
 792   ASM_REWRITE_TAC[IN];
 793   INTRO_TAC BALL_DIFF_RCONE_GT_BISECTOR [`EL 0 ul`;`EL 1 ul`;`EL 0 ul + t % u`;`sqrt(&2)`;`hl(truncate_simplex 1 ul)`];
 794   ANTS_TAC;
 795     ASM_REWRITE_TAC[IN_DIFF];
 796     CONJ_TAC;
 797       BY(ASM_MESON_TAC[arith `1 = SUC 0`]);
 798     CONJ2_TAC;
 799       GMATCH_SIMP_TAC REAL_LT_RSQRT;
 800       BY(REAL_ARITH_TAC);
 801     GMATCH_SIMP_TAC BARV3_TRUNC1;
 802     CONJ_TAC;
 803       BY(ASM_MESON_TAC[IN]);
 804     ONCE_REWRITE_TAC[DIST_SYM];
 805     REWRITE_TAC[Marchal_cells_3.HL_2];
 806     BY(REAL_ARITH_TAC);
 807   REWRITE_TAC[Sphere.bis_le;IN_ELIM_THM];
 808   REWRITE_TAC[dist];
 809   EXPAND_TAC "w";
 810   REWRITE_TAC[arith `!u v. (u + w) - u = (w:real^3)`];
 811   DISCH_THEN (unlist REWRITE_TAC);
 812   BY(ASM_MESON_TAC[])
 813   ]);;
 814   (* }}} *)
 815
 816 let MCELL1_VOL = prove_by_refinement(
 817   `!V X ul.  saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell1 V ul) /\ ~(NULLSET X) ==>
 818     vol X = (sqrt(&2) pow 3 / &3) * sol (EL 0 ul) X`,
 819   (* {{{ proof *)
 820   [
 821   REPEAT WEAK_STRIP_TAC;
 822   INTRO_TAC MCELL1_VOL_RESTRICT [`V`;`X`;`ul`];
 823   ASM_REWRITE_TAC[];
 824   DISCH_THEN SUBST1_TAC;
 825   INTRO_TAC MCELL1_SOL_RESTRICT [`V`;`X`;`ul`];
 826   ASM_REWRITE_TAC[];
 827   DISCH_THEN SUBST1_TAC;
 828   INTRO_TAC MCELL1_RADIAL [`V`;`X`;`ul`];
 829   ASM_REWRITE_TAC[];
 830   DISCH_TAC;
 831   GMATCH_SIMP_TAC Vol1.sol_spec;
 832   EXISTS_TAC `sqrt(&2)`;
 833   REWRITE_TAC[GSYM CONJ_ASSOC];
 834   CONJ_TAC;
 835     REWRITE_TAC[arith `x > y <=> y < x`];
 836     GMATCH_SIMP_TAC REAL_LT_RSQRT;
 837     BY(REAL_ARITH_TAC);
 838   CONJ_TAC;
 839     REWRITE_TAC[INTER_ASSOC;INTER_IDEMPOT];
 840     MATCH_MP_TAC MEASURABLE_INTER;
 841     REWRITE_TAC[MEASURABLE_BALL;Bump.MCELL1;];
 842     MATCH_MP_TAC Urrphbz1.MEASURABLE_MCELL;
 843     BY(ASM_REWRITE_TAC[]);
 844   ASM_REWRITE_TAC[INTER_ASSOC;INTER_IDEMPOT];
 845   Calc_derivative.CALC_ID_TAC;
 846   GMATCH_SIMP_TAC SQRT_EQ_0;
 847   BY(REAL_ARITH_TAC)
 848   ]);;
 849   (* }}} *)
 850
 851 let HJKDESR1a_1cell = prove_by_refinement(
 852   `&0 <  &8 * pi * sqrt2 / &3  -  &8 * mm1 `,
 853   (* {{{ proof *)
 854   [
 855   REWRITE_TAC[ arith `&8 * pi * sqrt2 / &3 = (&8 / &3) * (pi * sqrt2)`];
 856   MATCH_MP_TAC (arith `&3 * mm1 < z ==> &0 < (&8/ &3) * z  - &8 * mm1`);
 857   MATCH_MP_TAC REAL_LT_TRANS;
 858   EXISTS_TAC (`&3 * #1.3`);
 859   GMATCH_SIMP_TAC REAL_LT_LMUL_EQ;
 860   GMATCH_SIMP_TAC REAL_LT_MUL2;
 861   MP_TAC Flyspeck_constants.bounds;
 862   BY(REAL_ARITH_TAC)
 863   ]);;
 864
 865 let TSKAJXY_1 = prove_by_refinement(
 866   `!V ul.  saturated V /\ packing V /\ barV V 3 ul ==>
 867     gammaX V (mcell1 V ul) lmfun >= &0 `,
 868   (* {{{ proof *)
 869   [
 870   REPEAT WEAK_STRIP_TAC;
 871   ASM_CASES_TAC `NULLSET (mcell1 V ul)`;
 872     BY(ASM_MESON_TAC[GAMMAX_NULLSET;arith `x = &0 ==> x >= &0`;Bump.MCELL1]);
 873   GMATCH_SIMP_TAC GAMMAX_MCELL1;
 874   TYPIFY `ul` EXISTS_TAC;
 875   ASM_REWRITE_TAC[];
 876   INTRO_TAC MCELL1_VOL [`V`;`mcell1 V ul`;`ul`];
 877   ASM_REWRITE_TAC[];
 878   DISCH_TAC;
 879   TYPIFY `sol (EL 0 ul) (mcell1 V ul) = (&3 / sqrt(&2) pow 3) * vol (mcell1 V ul)` (C SUBGOAL_THEN SUBST1_TAC);
 880     ASM_REWRITE_TAC[];
 881     Calc_derivative.CALC_ID_TAC;
 882     GMATCH_SIMP_TAC SQRT_EQ_0;
 883     BY(REAL_ARITH_TAC);
 884   REWRITE_TAC[arith `b - c * d* b = (&1 - c* d) * b`;arith `x >= &0 <=> &0 <= x`];
 885   GMATCH_SIMP_TAC REAL_LE_MUL;
 886   CONJ2_TAC;
 887     REWRITE_TAC[arith `&0 <= x <=> x >= &0`];
 888     MATCH_MP_TAC Vol1.VOLUME_PROPS_MEASURABLE;
 889     REWRITE_TAC[Bump.MCELL1];
 890     MATCH_MP_TAC Urrphbz1.URRPHBZ1;
 891     BY(ASM_REWRITE_TAC[]);
 892   INTRO_TAC HJKDESR1a_1cell [];
 893   SUBGOAL_THEN `!x y. (x = (&8 * pi * sqrt(&2) / &3) * y)  ==> (&0 < x ==> &0 <= y)` MATCH_MP_TAC;
 894     REPEAT WEAK_STRIP_TAC;
 895     FIRST_X_ASSUM MP_TAC;
 896     ASM_REWRITE_TAC[];
 897     DISCH_THEN (MP_TAC o (MATCH_MP (arith `&0 < x ==> &0 <= x`)));
 898     DISCH_TAC;
 899     MATCH_MP_TAC Real_ext.REAL_PROP_NN_LCANCEL;
 900     TYPIFY `(&8 * pi * sqrt (&2) / &3)` EXISTS_TAC;
 901     ASM_REWRITE_TAC[];
 902     GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
 903     REWRITE_TAC[ REAL_OF_NUM_LT];
 904     GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
 905     GMATCH_SIMP_TAC REAL_LT_DIV;
 906     REWRITE_TAC[ REAL_OF_NUM_LT];
 907     GMATCH_SIMP_TAC REAL_LT_RSQRT;
 908     REWRITE_TAC[PI_POS];
 909     CONJ_TAC;
 910       BY(REAL_ARITH_TAC);
 911     BY(ARITH_TAC);
 912   Calc_derivative.CALC_ID_TAC;
 913   ASM_SIMP_TAC[PI_POS;arith `&0 < x ==> ~(x = &0)`;arith `~(&3= &0)`];
 914   GMATCH_SIMP_TAC SQRT_EQ_0;
 915   REWRITE_TAC[Sphere.sqrt2];
 916   CONJ_TAC;
 917     BY(REAL_ARITH_TAC);
 918   CONJ_TAC;
 919     BY(REAL_ARITH_TAC);
 920   TYPIFY `sqrt(&2) pow 3 = &2 * sqrt(&2)` (C SUBGOAL_THEN SUBST1_TAC);
 921     REWRITE_TAC[arith `3 = SUC 2`;real_pow];
 922     GMATCH_SIMP_TAC SQRT_POW_2;
 923     BY(REAL_ARITH_TAC);
 924   BY(REAL_ARITH_TAC)
 925   ]);;
 926   (* }}} *)
 927
 928 let MCELL_CELL_PARAMETERS_D_EXIST = prove_by_refinement(
 929   `!V ul vl k X. (k <= 4) /\ packing V /\ saturated V /\ (X = mcell k V ul) /\  ul IN barV V 3 /\
 930     initial_sublist vl ul /\
 931    ~NULLSET X ==>
 932      FST (cell_params_d V X vl) = k`,
 933   (* {{{ proof *)
 934   [
 935   REWRITE_TAC[Pack_defs.cell_params_d];
 936   REPEAT WEAK_STRIP_TAC;
 937   SELECT_TAC THEN (REPEAT (FIRST_X_ASSUM MP_TAC)) THEN (REWRITE_TAC[Bump.BETA_ORDERED_PAIR_THM]);
 938     INTRO_TAC Ajripqn.AJRIPQN [`V`;`ul`;`SND t`;`k`;`FST t`];
 939     REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY;arith `x = 0 \/ x = 1 \/ x = 2 \/ x  = 3 \/ x = 4 <=> x <= 4`];
 940     REWRITE_TAC[IN];
 941     REPEAT WEAK_STRIP_TAC;
 942     FIRST_X_ASSUM_ST `==>` MP_TAC;
 943     ANTS_TAC;
 944       ASM_REWRITE_TAC[];
 945       BY(ASM_MESON_TAC[INTER_IDEMPOT]);
 946     BY(DISCH_THEN (unlist REWRITE_TAC));
 947   REPEAT WEAK_STRIP_TAC;
 948   FIRST_X_ASSUM MP_TAC;
 949   REWRITE_TAC[NOT_EXISTS_THM];
 950   DISCH_THEN (C INTRO_TAC [`k,ul`]);
 951   BY(ASM_REWRITE_TAC[])
 952   ]);;
 953   (* }}} *)
 954
 955 let INITIAL_SUBLIST_2 = prove_by_refinement(
 956   `!ul. LENGTH ul = 4 ==> initial_sublist [EL 0 (ul:(A)list);EL 1 ul] ul`,
 957   (* {{{ proof *)
 958   [
 959   REPEAT WEAK_STRIP_TAC;
 960   INTRO_TAC Bump.LENGTH4 [`ul`];
 961   ANTS_TAC;
 962     BY(ASM_REWRITE_TAC[]);
 963   DISCH_TAC;
 964   TYPIFY `ul = APPEND [EL 0 ul;EL 1 ul] [EL 2 ul;EL 3 ul]` ENOUGH_TO_SHOW_TAC;
 965     BY(ASM_MESON_TAC[Packing3.INITIAL_SUBLIST_APPEND]);
 966   REWRITE_TAC[APPEND];
 967   BY(ASM_MESON_TAC[])
 968   ]);;
 969   (* }}} *)
 970
 971 let MCELL2_CELL_PARAMETERS_EXIST = prove_by_refinement(
 972   `!V ul X. packing V /\ saturated V /\ (X = mcell2 V ul) /\  ul IN barV V 3 /\ ~NULLSET X ==>
 973      FST (cell_params_d V X [EL 0 ul;EL 1 ul]) = 2`,
 974   (* {{{ proof *)
 975   [
 976   REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_CELL_PARAMETERS_D_EXIST THEN ASM_REWRITE_TAC[Bump.MCELL2;arith `2 <= 4`];
 977   TYPIFY `ul` EXISTS_TAC;
 978   ASM_REWRITE_TAC[];
 979   MATCH_MP_TAC INITIAL_SUBLIST_2;
 980   BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`])
 981   ]);;
 982   (* }}} *)
 983
 984 let MCELL_PARAM_D_UL = prove_by_refinement(
 985   `!V ul ul' vl X k. (k<= 4) /\ packing V /\ saturated V /\ (X = mcell k V ul) /\ ul IN barV V 3 /\ ~NULLSET X /\
 986     initial_sublist ul' ul /\
 987     vl = SND (cell_params_d V X ul') ==>
 988     (X = mcell k V vl /\ vl IN barV V 3 /\ initial_sublist ul' vl)`,
 989   (* {{{ proof *)
 990   [
 991   REWRITE_TAC[Pack_defs.cell_params_d];
 992   REPEAT WEAK_STRIP_TAC;
 993   INTRO_TAC MCELL_CELL_PARAMETERS_D_EXIST [`V`;`ul`;`ul'`;`k`;`X`];
 994   ASM_REWRITE_TAC[];
 995   REWRITE_TAC[Pack_defs.cell_params_d];
 996   Bump.WEAK_SELECT_TAC THEN (REPEAT (FIRST_X_ASSUM MP_TAC)) THEN (REWRITE_TAC[Bump.BETA_ORDERED_PAIR_THM]);
 997   Bump.WEAK_SELECT_TAC THEN (REPEAT (FIRST_X_ASSUM MP_TAC)) THEN (REWRITE_TAC[Bump.BETA_ORDERED_PAIR_THM]);
 998   REPEAT WEAK_STRIP_TAC;
 999   CONJ_TAC;
1000     BY(MESON_TAC[]);
1001   REPEAT WEAK_STRIP_TAC;
1002   CONJ_TAC;
1003     BY(ASM_MESON_TAC[]);
1004   REWRITE_TAC[NOT_EXISTS_THM];
1005   DISCH_THEN (C INTRO_TAC [`k,ul`]);
1006   BY(ASM_MESON_TAC[FST;SND])
1007   ]);;
1008   (* }}} *)
1009
1010 let MCELL2_PARAM_D_UL = prove_by_refinement(
1011   `!V ul ul' vl X. packing V /\ saturated V /\ (X = mcell2 V ul) /\ ul IN barV V 3 /\ ~NULLSET X /\
1012     initial_sublist ul' ul /\
1013     vl = SND (cell_params_d V X ul') ==>
1014     (X = mcell2 V (vl) /\ vl IN barV V 3 /\ initial_sublist ul' vl)`,
1015   (* {{{ proof *)
1016   [
1017   REWRITE_TAC[Bump.MCELL2];
1018   REPEAT WEAK_STRIP_TAC THEN MATCH_MP_TAC MCELL_PARAM_D_UL;
1019   BY(ASM_MESON_TAC[arith `2 <= 4`])
1020   ]);;
1021   (* }}} *)
1022
1023 let MCELL2_DIHX = prove_by_refinement(
1024   `!V X ul.  saturated V /\ packing V /\ barV V 3 ul /\ (X = mcell2 V ul) /\ ~(NULLSET X) ==>
1025     dihX V X (EL 0 ul, EL 1 ul) = dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3)`,
1026   (* {{{ proof *)
1027   [
1028   REPEAT WEAK_STRIP_TAC;
1029   ASM_REWRITE_TAC[Pack_defs.dihX;Pack_defs.dihu2;LET_DEF;LET_END_DEF;Bump.BETA_ORDERED_PAIR_THM];
1030   GMATCH_SIMP_TAC MCELL2_CELL_PARAMETERS_EXIST;
1031   ASM_REWRITE_TAC[IN];
1032   CONJ_TAC;
1033     BY(ASM_MESON_TAC[]);
1034   TYPED_ABBREV_TAC `(vl:(real^3)list) = SND (cell_params_d V (mcell2 V ul) [EL 0 ul; EL 1 ul])`;
1035   INTRO_TAC MCELL2_PARAM_D_UL [`V`;`ul`;`[EL 0 ul;EL 1 ul]`;`vl`;`X`];
1036   ASM_REWRITE_TAC[IN];
1037   ANTS_TAC;
1038     MATCH_MP_TAC INITIAL_SUBLIST_2;
1039     BY(ASM_MESON_TAC[Sphere.BARV;IN;arith `3 + 1 = 4`]);
1040   REPEAT WEAK_STRIP_TAC;
1041   INTRO_TAC Marchal_cells_3.MCELL_ID_OMEGA_LIST_N [`V`;`2`;`2`;`ul`;`vl`];
1042   ANTS_TAC;
1043     ASM_REWRITE_TAC[IN_INSERT];
1044     BY(ASM_MESON_TAC[Bump.MCELL2]);
1045   REWRITE_TAC[arith `2 = 2`;arith `2 - 1 = 1`];
1046   DISCH_THEN (C INTRO_TAC [`3`]);
1047   REWRITE_TAC[arith `1 <= 3 /\ 3 <= 3`];
1048   DISCH_THEN SUBST1_TAC;
1049   INTRO_TAC Marchal_cells_3.MCELL_ID_MXI_2 [`V`;`2`;`2`;`ul`;`vl`];
1050   ANTS_TAC;
1051     ASM_REWRITE_TAC[IN_INSERT];
1052     BY(ASM_MESON_TAC[Bump.MCELL2]);
1053   DISCH_THEN SUBST1_TAC;
1054   INTRO_TAC INITIAL_SUBLIST_2 [`vl`];
1055   ANTS_TAC;
1056     BY(ASM_MESON_TAC[Sphere.BARV;arith `3 + 1 = 4`]);
1057   DISCH_TAC;
1058   INTRO_TAC Packing3.INITIAL_SUBLIST_UNIQUE [`2`;`[EL 0 ul;EL 1 ul]`;`[EL 0 vl;EL 1 vl]`;`vl`];
1059   ASM_REWRITE_TAC[LENGTH;arith `SUC (SUC 0) = 2`];
1060   REWRITE_TAC[CONS_11];
1061   BY(DISCH_THEN (unlist REWRITE_TAC))
1062   ]);;
1063   (* }}} *)
1064
1065 let BIS_LE_INTER = prove_by_refinement(
1066   `!u0 (u1:real^A).  bis_le u0 u1 INTER bis_le u1 u0 = bis u0 u1`,
1067   (* {{{ proof *)
1068   [
1069   REWRITE_TAC[Sphere.bis_le;EXTENSION;IN_ELIM_THM;IN_INTER;Sphere.bis];
1070   BY(REAL_ARITH_TAC)
1071   ]);;
1072   (* }}} *)
1073
1074 let BIS_LE_UNION = prove_by_refinement(
1075   `!u0 (u1:real^A). bis_le u0 u1 UNION bis_le u1 u0 = (:real^A)`,
1076   (* {{{ proof *)
1077   [
1078   REWRITE_TAC[Sphere.bis_le;EXTENSION;IN_ELIM_THM;IN_UNION;IN_UNIV];
1079   BY(REAL_ARITH_TAC)
1080   ]);;
1081   (* }}} *)
1082
1083 let BIS_HYPERPLANE = prove_by_refinement(
1084   `!u0 (u1:real^A). bis u0 u1 = { p | (&2 % (u0 - u1)) dot p = (u0 - u1) dot (u0 + u1)}`,
1085   (* {{{ proof *)
1086   [
1087   REWRITE_TAC[Sphere.bis;EXTENSION;Leaf_cell.DIST_EQ_HALF_PLANE;IN_ELIM_THM];
1088   REPEAT WEAK_STRIP_TAC;
1089   MATCH_MP_TAC (arith `u = a - (b) ==> (&0 = u <=> a = b)`);
1090   BY(VECTOR_ARITH_TAC)
1091   ]);;
1092   (* }}} *)
1093
1094 let MCELL2_INTER_BIS_LE_MEASURABLE = prove_by_refinement(
1095   `!u0 u1 V X ul. packing V /\ saturated V /\
1096          barV V 3 ul /\
1097          X = mcell2 V ul ==>
1098     measurable (X INTER bis_le u0 u1)`,
1099   (* {{{ proof *)
1100   [
1101   REPEAT WEAK_STRIP_TAC;
1102   MATCH_MP_TAC MEASURABLE_CONVEX;
1103   CONJ_TAC;
1104     MATCH_MP_TAC CONVEX_INTER;
1105     ASM_REWRITE_TAC[Bump.MCELL2;Packing3.CONVEX_BIS_LE];
1106     MATCH_MP_TAC Leaf_cell.MCELL_CONVEX;
1107     BY(ASM_MESON_TAC[arith `2 <= 2`]);
1108   MATCH_MP_TAC BOUNDED_SUBSET;
1109   TYPIFY `X` EXISTS_TAC;
1110   CONJ2_TAC;
1111     BY(SET_TAC[]);
1112   ASM_REWRITE_TAC[Bump.MCELL2];
1113   MATCH_MP_TAC Urrphbz1.BOUNDED_MCELL;
1114   BY(ASM_REWRITE_TAC[])
1115   ]);;
1116   (* }}} *)
1117
1118 let MCELL2_VOL_SPLIT = prove_by_refinement(
1119   `!V X ul.          saturated V /\
1120          packing V /\
1121          barV V 3 ul /\
1122          X = mcell2 V ul /\
1123          ~NULLSET X ==>
1124          vol X = vol (X INTER bis_le (EL 0 ul) (EL 1 ul)) + vol (X INTER bis_le (EL 1 ul) (EL 0 ul))`,
1125   (* {{{ proof *)
1126   [
1127   REPEAT WEAK_STRIP_TAC;
1128   GMATCH_SIMP_TAC (GSYM MEASURE_NEGLIGIBLE_UNION);
1129   TYPIFY ` ((X INTER bis_le (EL 0 ul) (EL 1 ul)) INTER    X INTER   bis_le (EL 1 ul) (EL 0 ul)) = X INTER bis (EL 0 ul) (EL 1 ul)` (C SUBGOAL_THEN SUBST1_TAC);
1130     INTRO_TAC BIS_LE_INTER [`EL 0 ul`;`EL 1 ul`];
1131     BY(SET_TAC[]);
1132   TYPIFY `(X INTER bis_le (EL 0 ul) (EL 1 ul) UNION   X INTER bis_le (EL 1 ul) (EL 0 ul)) = X` (C SUBGOAL_THEN SUBST1_TAC);
1133     INTRO_TAC BIS_LE_UNION [`EL 0 ul`;`EL 1 ul`];
1134     BY(SET_TAC[]);
1135   REWRITE_TAC[];
1136   REWRITE_TAC[CONJ_ASSOC];
1137   CONJ_TAC;
1138     BY(ASM_MESON_TAC[MCELL2_INTER_BIS_LE_MEASURABLE]);
1139   REWRITE_TAC[BIS_HYPERPLANE];
1140   MATCH_MP_TAC NEGLIGIBLE_SUBSET;
1141   TYPIFY `{p | &2 % (EL 0 ul - EL 1 ul) dot p =          (EL 0 ul - EL 1 ul) dot (EL 0 ul + EL 1 ul)}` EXISTS_TAC;
1142   CONJ2_TAC;
1143     BY(SET_TAC[]);
1144   MATCH_MP_TAC NEGLIGIBLE_HYPERPLANE;
1145   REWRITE_TAC[DE_MORGAN_THM];
1146   DISJ1_TAC;
1147   REWRITE_TAC[VECTOR_MUL_EQ_0;arith `~(&2 = &0)`];
1148   REWRITE_TAC[varith `!a (b:real^A). a - b = vec 0 <=> a = b`];
1149   DISCH_TAC;
1150   BY(ASM_MESON_TAC[MCELL2_VX_PROPS])
1151   ]);;
1152   (* }}} *)
1153
1154 let RCONE_GE_COS = prove_by_refinement(
1155   `!(u:real^3) v a.  ~(u=v) ==>
1156     rcone_ge u v a = {u} UNION { x | a <= cos(arcV u v x) }`,
1157   (* {{{ proof *)
1158   [
1159   REPEAT WEAK_STRIP_TAC;
1160   ONCE_REWRITE_TAC[Trigonometry2.ARC_SYM];
1161   REWRITE_TAC[Sphere.rcone_ge;Sphere.rconesgn;EXTENSION;IN_ELIM_THM;IN_UNION;IN_SING;Trigonometry1.DOT_COS];
1162   REWRITE_TAC[dist;arith `x >= y <=> y <= x`];
1163   REPEAT WEAK_STRIP_TAC;
1164   TYPIFY `x = u` ASM_CASES_TAC;
1165     ASM_REWRITE_TAC[];
1166     REWRITE_TAC[VECTOR_SUB_REFL;NORM_0];
1167     BY(REAL_ARITH_TAC);
1168   ASM_REWRITE_TAC[];
1169   REWRITE_TAC[arith `nu * nv * a <= nu * nv * c <=> &0 <= nu * nv * (c - a)`];
1170   GMATCH_SIMP_TAC REAL_LE_MUL_EQ;
1171   GMATCH_SIMP_TAC REAL_LE_MUL_EQ;
1172   REWRITE_TAC[NORM_POS_LT];
1173   REWRITE_TAC[GSYM Trigonometry2.ARCV_VEC0_FORM];
1174   REWRITE_TAC[varith `(v:real^3) -  u = vec 0 <=> (v = u)`];
1175   ASM_REWRITE_TAC[];
1176   BY(REAL_ARITH_TAC)
1177   ]);;
1178   (* }}} *)
1179
1180 let DIST_LAW_OF_COS_ALT = prove_by_refinement(
1181 `!u v (w:real^3). dist (v,w) pow 2 =
1182         dist (u,v) pow 2 +
1183         dist (u,w) pow 2 - &2 * dist (u,v) * dist (u,w) * cos (arcV u v w)`,
1184   (* {{{ proof *)
1185   [
1186     BY(MESON_TAC[Trigonometry1.DIST_LAW_OF_COS])
1187   ]);;
1188   (* }}} *)
1189
1190 let ATN_INV = prove_by_refinement(
1191   `!x y. &0 < x /\ &0 < y ==> atn (x / y) = pi / &2 - atn (y/x) `,
1192   (* {{{ proof *)
1193   [
1194   REPEAT WEAK_STRIP_TAC;
1195   INTRO_TAC Merge_ineq.atn_inv [`y/x`];
1196   ANTS_TAC;
1197     GMATCH_SIMP_TAC REAL_LT_DIV;
1198     BY(ASM_REWRITE_TAC[]);
1199   TYPIFY `&1 / (y / x) = x / y` (C SUBGOAL_THEN SUBST1_TAC);
1200     Calc_derivative.CALC_ID_TAC;
1201     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1202   BY(REAL_ARITH_TAC)
1203   ]);;
1204   (* }}} *)
1205
1206 let REAL_DIV_NEG = prove_by_refinement(
1207   `!x y. (x / --y) = -- (x/y)`,
1208   (* {{{ proof *)
1209   [
1210   REWRITE_TAC[real_div;REAL_INV_NEG];
1211   BY(REAL_ARITH_TAC)
1212   ]);;
1213   (* }}} *)
1214
1215 let ATN2_Y_NEG = prove_by_refinement(
1216   `!x y. y < &0 ==> atn2(x,y) = -- (pi / &2) - atn(x/y)`,
1217   (* {{{ proof *)
1218   [
1219   REPEAT WEAK_STRIP_TAC;
1220   REWRITE_TAC[Trigonometry2.atn2];
1221   TYPIFY `abs y < x` ASM_CASES_TAC;
1222     ASM_REWRITE_TAC[];
1223     TYPED_ABBREV_TAC `(u:real) = -- y`;
1224     REPEAT (FIRST_X_ASSUM_ST `<` MP_TAC);
1225     TYPIFY `y = -- u` (C SUBGOAL_THEN SUBST1_TAC);
1226       BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1227     REWRITE_TAC[arith `-- u < &0 <=> &0 < u`;arith `-- u / x = -- (u/x)`;REAL_DIV_NEG];
1228     REWRITE_TAC[ATN_NEG];
1229     REPEAT WEAK_STRIP_TAC;
1230     GMATCH_SIMP_TAC ATN_INV;
1231     CONJ2_TAC;
1232       BY(REAL_ARITH_TAC);
1233     ASM_REWRITE_TAC[];
1234     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1235   ASM_REWRITE_TAC[];
1236   BY(ASM_SIMP_TAC[arith `y < &0 ==> ~(&0 < y)`])
1237   ]);;
1238   (* }}} *)
1239
1240 let RCONE_PAIR = prove_by_refinement(
1241   `!(u:real^3) v t. ~(u=v) /\ &0 < t /\ t <= &1 ==> rcone_ge u v t INTER bis_le u v SUBSET rcone_ge v u t`,
1242   (* {{{ proof *)
1243   [
1244   REPEAT WEAK_STRIP_TAC;
1245   GMATCH_SIMP_TAC RCONE_GE_COS;
1246   GMATCH_SIMP_TAC RCONE_GE_COS;
1247   ASM_REWRITE_TAC[SUBSET;IN_INTER;IN_UNION;IN_SING;IN_ELIM_THM;Sphere.bis_le];
1248   GEN_TAC;
1249   TYPIFY `x = u` ASM_CASES_TAC;
1250     BY(ASM_SIMP_TAC[Local_lemmas1.ACR_REFL;COS_0]);
1251   ASM_REWRITE_TAC[];
1252   TYPIFY `x = v` ASM_CASES_TAC;
1253     BY(ASM_SIMP_TAC[Local_lemmas1.ACR_REFL;COS_0]);
1254   ASM_REWRITE_TAC[];
1255   REPEAT WEAK_STRIP_TAC;
1256   FIRST_X_ASSUM_ST `cos` MP_TAC;
1257   MATCH_MP_TAC (arith `(t <= x ==> x <= y) ==> (t <= x ==> t <= y)`);
1258   DISCH_TAC;
1259   MATCH_MP_TAC COS_MONO_LE;
1260   REWRITE_TAC[Local_lemmas1.ARCV_BOUNDS];
1261   TYPIFY `&0 < cos (arcV u v x)` (C SUBGOAL_THEN ASSUME_TAC);
1262     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1263   REPLICATE_TAC 2 (GMATCH_SIMP_TAC Trigonometry1.arcVarc);
1264   ASM_REWRITE_TAC[];
1265   TYPIFY `dist(v,x) pow 2 < dist(u,v) pow 2 + dist(u,x) pow 2` (C SUBGOAL_THEN ASSUME_TAC);
1266     INTRO_TAC DIST_LAW_OF_COS_ALT [`u`;`v`;`x`];
1267     TYPIFY `&0 < &2 * dist(u,v) * dist (u,x) * cos (arcV u v x)` ENOUGH_TO_SHOW_TAC;
1268       BY(REAL_ARITH_TAC);
1269     GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
1270     CONJ_TAC;
1271       BY(REAL_ARITH_TAC);
1272     GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
1273     GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
1274     BY(ASM_SIMP_TAC[GSYM DIST_POS_LT]);
1275   TYPIFY `dist(v,u) = dist(u,v)` (C SUBGOAL_THEN SUBST1_TAC);
1276     BY(MESON_TAC[DIST_SYM]);
1277   TYPED_ABBREV_TAC  `(c:real) = dist(u,v)` ;
1278   TYPED_ABBREV_TAC  `(b:real) = dist(v,x)` ;
1279   TYPED_ABBREV_TAC  `(a:real) = dist(u,x)` ;
1280   REWRITE_TAC[Local_lemmas1.COS_ARCV];
1281   REWRITE_TAC[Sphere.arclength];
1282   REWRITE_TAC[arith `t + u <= t + v <=> u <= v`];
1283   FIRST_X_ASSUM_ST `dist(x,u) <= dist(x,v)` MP_TAC;
1284   ONCE_REWRITE_TAC[DIST_SYM];
1285   ASM_REWRITE_TAC[];
1286   DISCH_TAC;
1287   TYPIFY `a pow 2 <= b pow 2` (C SUBGOAL_THEN ASSUME_TAC);
1288     MATCH_MP_TAC Collect_geom2.POS_IMP_POW2;
1289     ASM_REWRITE_TAC[];
1290     EXPAND_TAC "a";
1291     BY(REWRITE_TAC[DIST_POS_LE]);
1292   TYPIFY `ups_x (c*c) (a*a) (b*b) = ups_x (c*c) (b*b) (a*a)` (C SUBGOAL_THEN SUBST1_TAC);
1293     BY(MESON_TAC[Collect_geom.UPS_X_SYM]);
1294   TYPED_ABBREV_TAC  `(up:real) = ups_x (c*c) (b*b) (a*a)` ;
1295   REPEAT (GMATCH_SIMP_TAC ATN2_Y_NEG);
1296   SUBCONJ_TAC;
1297     FIRST_X_ASSUM_ST `<` MP_TAC;
1298     BY(REAL_ARITH_TAC);
1299   DISCH_TAC;
1300   SUBCONJ_TAC;
1301     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1302   DISCH_TAC;
1303   MATCH_MP_TAC (arith `y <= x ==> u - x <= u - y`);
1304   REWRITE_TAC[ATN_MONO_LE_EQ];
1305   TYPIFY `&0 <= sqrt up` (C SUBGOAL_THEN ASSUME_TAC);
1306     GMATCH_SIMP_TAC SQRT_POS_LE;
1307     EXPAND_TAC "up";
1308     BY(ASM_MESON_TAC[Collect_geom.TROI_OI_DAT_HOI;REAL_POW_2]);
1309   REWRITE_TAC[real_div];
1310   GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP;
1311   ASM_REWRITE_TAC[];
1312   REWRITE_TAC[arith `x - y - z = --(y + z - x)`;REAL_INV_NEG;arith `-- x <= --y <=> y <= x`];
1313   GMATCH_SIMP_TAC REAL_LE_INV2;
1314   BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
1315   ]);;
1316   (* }}} *)
1317
1318 let MCELL2_SPLIT = prove_by_refinement(
1319   `!V X ul.
1320        saturated V /\
1321          packing V /\
1322          barV V 3 ul /\
1323          X = mcell2 V ul /\
1324          ~NULLSET X ==>
1325          (X INTER bis_le (EL 0 ul) (EL 1 ul) =
1326              rcone_ge (EL 0 ul) (EL 1 ul) (hl (truncate_simplex 1 ul) / sqrt (&2))  INTER
1327                aff_ge {EL 0 ul,EL 1 ul} {mxi V ul,omega_list_n V ul 3} INTER bis_le (EL 0 ul) (EL 1 ul))`,
1328   (* {{{ proof *)
1329   [
1330   REPEAT WEAK_STRIP_TAC;
1331   INTRO_TAC Pack_defs.mcell2 [`V`;`ul`];
1332   TYPIFY `~(hl (truncate_simplex 1 ul) < sqrt (&2) /\ sqrt (&2) <= hl ul)` ASM_CASES_TAC;
1333     ASM_REWRITE_TAC[];
1334     BY(ASM_MESON_TAC[NEGLIGIBLE_EMPTY]);
1335   FIRST_ASSUM ((unlist REWRITE_TAC) o (REWRITE_RULE[NOT_CLAUSES]));
1336   ASM_REWRITE_TAC[LET_DEF;LET_END_DEF];
1337   DISCH_THEN SUBST1_TAC;
1338   TYPED_ABBREV_TAC  `(a:real) = hl (truncate_simplex 1 ul)/ (sqrt (&2))` ;
1339   TYPIFY `HD ul = EL 0 ul /\ HD(TL ul) = EL 1 ul` (C SUBGOAL_THEN (unlist REWRITE_TAC));
1340     BY(REWRITE_TAC[EL;arith `1 = SUC 0`]);
1341   SUBGOAL_THEN `!(a:real^3->bool) b c d. (a INTER d SUBSET b) ==> ((a INTER b INTER c) INTER d = a INTER c INTER d)` (MATCH_MP_TAC);
1342     BY(SET_TAC[]);
1343   MATCH_MP_TAC RCONE_PAIR;
1344   EXPAND_TAC "a";
1345   SUBCONJ_TAC;
1346     BY(ASM_MESON_TAC[MCELL2_VX_PROPS]);
1347   DISCH_TAC;
1348   TYPIFY `&0 < sqrt(&2)` (C SUBGOAL_THEN ASSUME_TAC);
1349     GMATCH_SIMP_TAC REAL_LT_RSQRT;
1350     BY(REAL_ARITH_TAC);
1351   CONJ2_TAC;
1352     GMATCH_SIMP_TAC REAL_LE_LDIV_EQ;
1353     ASM_REWRITE_TAC[arith `&1 * x = x`];
1354     FIRST_X_ASSUM_ST `~ ~ x` MP_TAC THEN REWRITE_TAC[];
1355     BY(REAL_ARITH_TAC);
1356   GMATCH_SIMP_TAC REAL_LT_DIV;
1357   ASM_REWRITE_TAC[];
1358   BY(ASM_MESON_TAC[Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT])
1359   ]);;
1360   (* }}} *)
1361
1362 let FRUSTT_RCONE_GE = prove_by_refinement(
1363   `!u v  h a .
1364     &0 < a /\ ~(u= v) ==>
1365     NULLSET (SDIFF
1366                (frustt u v h a)
1367                (rcone_ge u v a INTER {y | (y- u) dot (v-u)  <= h * norm (v-u) }))`,
1368   (* {{{ proof *)
1369   [
1370   REPEAT WEAK_STRIP_TAC;
1371   ASM_REWRITE_TAC[frustt;frustum;EXTENSION;IN_ELIM_THM;LET_DEF;LET_END_DEF;IN_INTER];
1372   REWRITE_TAC[IN;arith `&0 * x = &0`;SDIFF];
1373   MATCH_MP_TAC NEGLIGIBLE_UNION;
1374   CONJ_TAC;
1375     TYPIFY `!s. (s = {}) ==> NULLSET s` (C SUBGOAL_THEN MATCH_MP_TAC);
1376       BY(MESON_TAC[NEGLIGIBLE_EMPTY]);
1377     REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_DIFF;IN_ELIM_THM;IN_INTER];
1378     REPEAT WEAK_STRIP_TAC;
1379     FIRST_X_ASSUM MP_TAC;
1380     REWRITE_TAC[];
1381     CONJ_TAC;
1382       BY(ASM_MESON_TAC[Marchal_cells_2_new.RCONE_GT_SUBSET_RCONE_GE;IN;SUBSET]);
1383     BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1384   MATCH_MP_TAC NEGLIGIBLE_SUBSET;
1385   TYPIFY `(rcone_ge u v a DIFF rcone_gt u v a) UNION {y | (y - u) dot (v - u) = h * norm (v - u)}` EXISTS_TAC;
1386   CONJ_TAC;
1387     MATCH_MP_TAC NEGLIGIBLE_UNION;
1388     CONJ_TAC;
1389       REWRITE_TAC[RCONE_GT_GE];
1390       MATCH_MP_TAC NEGLIGIBLE_SUBSET;
1391       TYPIFY `{x | (x - u) dot (v - u) = norm (x - u) * norm (v - u) * a}` EXISTS_TAC;
1392       CONJ2_TAC;
1393         BY(SET_TAC[]);
1394       TYPIFY `circular_cone {x | (x - u) dot (v - u) = norm (x - u) * norm (v - u) * a}` ENOUGH_TO_SHOW_TAC;
1395         BY(MESON_TAC[NULLSET_RULES]);
1396       REWRITE_TAC[circular_cone;c_cone];
1397       REWRITE_TAC[EXISTS_PAIRED_THM];
1398       GEXISTL_TAC [`u`;`v - (u:real^3)`;`a`];
1399       BY(ASM_REWRITE_TAC[varith `v - (u:real^3) = vec 0 <=> u = v`]);
1400     TYPIFY `!y u w a. (y- u) dot (w:real^3) = a <=> w dot y = a + u dot w` (C SUBGOAL_THEN (unlist ONCE_REWRITE_TAC));
1401       REPEAT WEAK_STRIP_TAC;
1402       MATCH_MP_TAC (arith `(x = y - z ==> (x = a' <=> y = a' + z))`);
1403       BY(VECTOR_ARITH_TAC);
1404     MATCH_MP_TAC NEGLIGIBLE_HYPERPLANE;
1405     BY(ASM_REWRITE_TAC[varith `(v:real^3) - u = vec 0 <=> u = v`]);
1406   REWRITE_TAC[SUBSET;IN_DIFF;IN_UNION;IN_INTER;IN_ELIM_THM];
1407   REWRITE_TAC[IN];
1408   REPEAT WEAK_STRIP_TAC;
1409   ASM_REWRITE_TAC[];
1410   MATCH_MP_TAC (TAUT (`(a ==>b)   ==> (~ a \/ b)`));
1411   DISCH_TAC;
1412   ASM_SIMP_TAC [(arith `x <= y ==> ((x = y) <=> ~(x < y))`)];
1413   DISCH_TAC;
1414   FIRST_X_ASSUM_ST `~` MP_TAC;
1415   ASM_REWRITE_TAC[];
1416   FIRST_X_ASSUM_ST `rcone_gt` MP_TAC;
1417   REWRITE_TAC[Sphere.rcone_gt;Sphere.rconesgn;IN_ELIM_THM];
1418   TYPIFY `&0 <= dist(x,u) * dist(v,u) * a` ENOUGH_TO_SHOW_TAC;
1419     BY(REAL_ARITH_TAC);
1420   GMATCH_SIMP_TAC REAL_LE_MUL;
1421   GMATCH_SIMP_TAC REAL_LE_MUL;
1422   BY(ASM_SIMP_TAC[DIST_POS_LE;arith `&0 < a ==> &0 <= a`])
1423   ]);;
1424   (* }}} *)
1425
1426 let SDIFF_SUBSET = prove_by_refinement(
1427   `!X Y Z.SDIFF (X INTER Z) (Y INTER Z) SUBSET  SDIFF X Y `,
1428   (* {{{ proof *)
1429   [
1430   REWRITE_TAC[SDIFF];
1431   BY(SET_TAC[])
1432   ]);;
1433   (* }}} *)
1434
1435 let SDIFF_TRANS = prove_by_refinement(
1436   `!X Y (Z:A->bool). SDIFF X Z SUBSET SDIFF X Y UNION SDIFF Y Z`,
1437   (* {{{ proof *)
1438   [
1439   REWRITE_TAC[SDIFF];
1440   BY(SET_TAC[])
1441   ]);;
1442   (* }}} *)
1443
1444 let NULL_SDIFF_TRANS = prove_by_refinement(
1445   `!X Y Z. NULLSET (SDIFF X Y) /\ NULLSET (SDIFF Y Z) ==> NULLSET(SDIFF X Z)`,
1446   (* {{{ proof *)
1447   [
1448   REPEAT WEAK_STRIP_TAC;
1449   MATCH_MP_TAC NEGLIGIBLE_SUBSET;
1450   BY(ASM_MESON_TAC[SDIFF_TRANS;NEGLIGIBLE_UNION])
1451   ]);;
1452   (* }}} *)
1453
1454
1455 let FRUSTT_WEDGE_RCONE_GE = prove_by_refinement(
1456   `!u v  w1 w2 h a .
1457     &0 < a /\ ~(u= v) /\
1458     &0 < a /\ a <= &1 /\ &0 <= h /\ ~(u = v) /\
1459     ~collinear {u,v,w1} /\ ~collinear{ u,v,w2} ==>
1460     NULLSET (SDIFF
1461                (frustt u v h a INTER wedge u v w1 w2)
1462                (rcone_ge u v a INTER {y | (y- u) dot (v-u)  <= h * norm (v-u) } INTER wedge_ge u v w1 w2))`,
1463   (* {{{ proof *)
1464   [
1465   REPEAT WEAK_STRIP_TAC;
1466   MATCH_MP_TAC NULL_SDIFF_TRANS;
1467   TYPIFY `frustt u v h a INTER wedge_ge u v w1 w2` EXISTS_TAC;
1468   CONJ2_TAC;
1469     MATCH_MP_TAC NEGLIGIBLE_SUBSET;
1470     TYPIFY `SDIFF (frustt u v h a)      (rcone_ge u v a INTER       {y | (y - u) dot (v - u) <= h * norm (v - u)})` EXISTS_TAC;
1471     CONJ_TAC;
1472       BY(ASM_MESON_TAC[FRUSTT_RCONE_GE]);
1473     BY(MESON_TAC[INTER_ASSOC;SDIFF_SUBSET]);
1474   COMMENT "down to 1";
1475   ONCE_REWRITE_TAC[INTER_COMM];
1476   MATCH_MP_TAC NEGLIGIBLE_SUBSET;
1477   TYPIFY `SDIFF (wedge u v w1 w2) (wedge_ge u v w1 w2)` EXISTS_TAC;
1478   CONJ2_TAC;
1479     BY(MESON_TAC[SDIFF_SUBSET]);
1480   REWRITE_TAC[SDIFF];
1481   MATCH_MP_TAC NEGLIGIBLE_UNION;
1482   CONJ_TAC;
1483     TYPIFY `wedge u v w1 w2 DIFF wedge_ge u v w1 w2  = {}` (C SUBGOAL_THEN (unlist REWRITE_TAC));
1484       BY(SET_TAC[Leaf_cell.WEDGE_SUBSET_WEDGE_GE]);
1485     BY(REWRITE_TAC[NEGLIGIBLE_EMPTY]);
1486   MATCH_MP_TAC NEGLIGIBLE_SUBSET;
1487   TYPIFY `affine hull {u,v,w1} UNION affine hull {u,v,w2}` EXISTS_TAC;
1488   CONJ_TAC;
1489     MATCH_MP_TAC NEGLIGIBLE_UNION;
1490     BY(REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]);
1491   MATCH_MP_TAC SUBSET_TRANS;
1492   TYPIFY `aff_ge {u,v} {w1} UNION aff_ge {u,v} {w2}` EXISTS_TAC;
1493   CONJ_TAC;
1494     INTRO_TAC Leaf_cell.WEDGE_WEDGE_GE [`u`;`v`;`w1`;`w2`];
1495     ANTS_TAC;
1496       BY(ASM_REWRITE_TAC[]);
1497     BY(SET_TAC[]);
1498   TYPIFY `!(A:real^3->bool) B A' B'. A SUBSET A' /\ B SUBSET B' ==> (A UNION B) SUBSET (A' UNION B')` (C SUBGOAL_THEN MATCH_MP_TAC);
1499     BY(SET_TAC[]);
1500   TYPIFY `!(u:real^3) v w. {u,v,w} = {u,v} UNION {w}` (C SUBGOAL_THEN (unlist REWRITE_TAC));
1501     BY(SET_TAC[]);
1502   BY(REWRITE_TAC[AFF_GE_SUBSET_AFFINE_HULL])
1503   ]);;
1504   (* }}} *)
1505
1506 let MCELL2_SUBSET_AFF_GE = prove_by_refinement(
1507   `!V ul. packing V /\ saturated V /\ ul IN barV V 3 ==>
1508     mcell2 V ul SUBSET  aff_ge {EL 0 ul, EL 1 ul} {mxi V ul, omega_list_n V ul 3}`,
1509   (* {{{ proof *)
1510   [
1511   REPEAT WEAK_STRIP_TAC;
1512   REWRITE_TAC[SUBSET;Pack_defs.mcell2];
1513   GEN_TAC;
1514   COND_CASES_TAC;
1515     REWRITE_TAC[LET_DEF;LET_END_DEF;EL;arith `1 = SUC 0`];
1516     BY(SET_TAC[]);
1517   BY(REWRITE_TAC[NOT_IN_EMPTY])
1518   ]);;
1519   (* }}} *)
1520
1521 let NOT_COPLANAR_EXTREME_MCELL2 = prove_by_refinement(
1522   `!V ul. packing V /\ saturated V /\ ul IN barV V 3 /\ ~NULLSET (mcell2 V ul) ==>
1523         ~coplanar { EL 0 ul, EL 1 ul, mxi V ul, omega_list_n V ul 3 }`,
1524   (* {{{ proof *)
1525   [
1526   REPEAT WEAK_STRIP_TAC;
1527   FIRST_X_ASSUM_ST `~` MP_TAC;
1528   REWRITE_TAC[];
1529   MATCH_MP_TAC COPLANAR_IMP_NEGLIGIBLE;
1530   MATCH_MP_TAC COPLANAR_SUBSET;
1531   TYPIFY `affine hull {EL 0 ul, EL 1 ul, mxi V ul, omega_list_n V ul 3}` EXISTS_TAC;
1532   CONJ_TAC;
1533     BY(ASM_REWRITE_TAC[COPLANAR_AFFINE_HULL_COPLANAR]);
1534   MATCH_MP_TAC SUBSET_TRANS;
1535   TYPIFY `aff_ge {EL 0 ul, EL 1 ul} {mxi V ul, omega_list_n V ul 3}` EXISTS_TAC;
1536   ASM_SIMP_TAC[MCELL2_SUBSET_AFF_GE];
1537   TYPIFY `!a b c (d:real^3). {a,b,c,d} = {a,b} UNION {c,d}` (C SUBGOAL_THEN (unlist REWRITE_TAC));
1538     BY(SET_TAC[]);
1539   BY(REWRITE_TAC[AFF_GE_SUBSET_AFFINE_HULL])
1540   ]);;
1541   (* }}} *)
1542
1543 let MCELL2_DIHV_LT_PI  = prove_by_refinement(
1544   `!V X ul.         packing V /\ saturated V /\
1545          barV V 3 ul /\
1546          X = mcell2 V ul /\
1547          ~NULLSET X ==> dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) < pi`,
1548   (* {{{ proof *)
1549   [
1550   REPEAT WEAK_STRIP_TAC;
1551   TYPIFY `~(dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) = pi)` ENOUGH_TO_SHOW_TAC;
1552     MATCH_MP_TAC (arith `(x <= pi) ==> (~(x = pi) ==> x < pi)`);
1553     BY(REWRITE_TAC[DIHV_RANGE]);
1554   TYPIFY `~coplanar { EL 0 ul, EL 1 ul, mxi V ul, omega_list_n V ul 3 }` ((C SUBGOAL_THEN ASSUME_TAC));
1555     BY(ASM_MESON_TAC[NOT_COPLANAR_EXTREME_MCELL2;IN]);
1556   TYPIFY `~collinear {EL 0 ul,EL 1 ul,mxi V ul} /\ ~collinear {EL 0 ul, EL 1 ul,omega_list_n V ul 3}` ((C SUBGOAL_THEN ASSUME_TAC));
1557     TYPIFY `!a b c (d:real^3). {a,b,c,d} = {a,b,d,c}` ((C SUBGOAL_THEN MP_TAC));
1558       BY(SET_TAC[]);
1559     BY(ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);
1560   BY(ASM_MESON_TAC[DIHV_EQ_0_PI_EQ_COPLANAR])
1561   ]);;
1562   (* }}} *)
1563
1564 let MCELL2_DIHV_AZIM = prove_by_refinement(
1565   `!V X ul h. packing V /\ saturated V /\
1566          barV V 3 ul /\
1567          X = mcell2 V ul /\
1568          ~NULLSET X  ==> ?w1 w2.  {w1,w2} = {mxi V ul,omega_list_n V ul 3} /\ dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) = azim (EL 0 ul) (EL 1 ul) w1 w2`,
1569   (* {{{ proof *)
1570   [
1571   REPEAT WEAK_STRIP_TAC;
1572   INTRO_TAC NOT_COPLANAR_EXTREME_MCELL2 [`V`;`ul`];
1573   ASM_REWRITE_TAC[];
1574   ANTS_TAC;
1575     BY(ASM_MESON_TAC[IN]);
1576   DISCH_TAC;
1577   TYPIFY `~collinear {EL 0 ul,EL 1 ul,mxi V ul} /\ ~collinear {EL 0 ul, EL 1 ul,omega_list_n V ul 3}` ((C SUBGOAL_THEN ASSUME_TAC));
1578     TYPIFY `!a b c (d:real^3). {a,b,c,d} = {a,b,d,c}` ((C SUBGOAL_THEN MP_TAC));
1579       BY(SET_TAC[]);
1580     BY(ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);
1581   TYPIFY `azim (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) <= pi` ASM_CASES_TAC;
1582     BY(ASM_MESON_TAC[Local_lemmas.AZIM_LE_PI_EQ_DIHV]);
1583   FIRST_ASSUM MP_TAC;
1584   DISCH_THEN (MP_TAC o (ONCE_REWRITE_RULE[Rogers.AZIM_COMPL_EXT]));
1585   COND_CASES_TAC;
1586     BY(ASM_MESON_TAC[PI_POS;arith `&0 < x ==> &0 <= x`]);
1587   DISCH_TAC;
1588   TYPIFY `azim (EL 0 ul) (EL 1 ul) (omega_list_n V ul 3) (mxi V ul) <= pi` (C SUBGOAL_THEN ASSUME_TAC);
1589     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1590   ONCE_REWRITE_TAC[DIHV_SYM];
1591   TYPIFY `!b. {mxi V ul,b} = {b,mxi V ul}` (C SUBGOAL_THEN (unlist REWRITE_TAC));
1592     BY(SET_TAC[]);
1593   BY(ASM_MESON_TAC[Local_lemmas.AZIM_LE_PI_EQ_DIHV])
1594   ]);;
1595   (* }}} *)
1596
1597 let BIS_LE_NORM = prove_by_refinement(
1598   `!u (v:real^A). bis_le u v = { y | (y - u) dot (v - u) <= norm (v - u) pow 2 / &2}`,
1599   (* {{{ proof *)
1600   [
1601   REWRITE_TAC[Packing3.BIS_LE_EQ_HALFSPACE;EXTENSION;IN_ELIM_THM;GSYM DOT_SQUARE_NORM];
1602   REPEAT WEAK_STRIP_TAC;
1603   MATCH_MP_TAC (arith `(a - b = &2 * (c - d)) ==> (a <= b <=> c <= d)`);
1604   REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL;DOT_RMUL;DOT_LSUB;DOT_RSUB];
1605   TYPIFY `x dot v = v dot x` (C SUBGOAL_THEN SUBST1_TAC);
1606     BY(VECTOR_ARITH_TAC);
1607   TYPIFY `x dot u = u dot x` (C SUBGOAL_THEN SUBST1_TAC);
1608     BY(VECTOR_ARITH_TAC);
1609   TYPIFY `v dot u = u dot v` (C SUBGOAL_THEN SUBST1_TAC);
1610     BY(VECTOR_ARITH_TAC);
1611   BY(REAL_ARITH_TAC)
1612   ]);;
1613   (* }}} *)
1614
1615 let BIS_LT_NORM = prove_by_refinement(
1616   `!u (v:real^A) x. dist(x,u) < dist(x,v) <=>  (x - u) dot (v - u) < norm (v - u) pow 2 / &2`,
1617   (* {{{ proof *)
1618   [
1619   REWRITE_TAC[Geomdetail.DIST_LT_HALF_PLANE;EXTENSION;IN_ELIM_THM;GSYM DOT_SQUARE_NORM];
1620   REPEAT WEAK_STRIP_TAC;
1621   MATCH_MP_TAC (arith `( &0 = b + &2 * (c - d)) ==> (&0 < b <=> c < d)`);
1622   REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL;DOT_RMUL;DOT_LSUB;DOT_RSUB];
1623   TYPIFY `x dot v = v dot x` (C SUBGOAL_THEN SUBST1_TAC);
1624     BY(VECTOR_ARITH_TAC);
1625   TYPIFY `x dot u = u dot x` (C SUBGOAL_THEN SUBST1_TAC);
1626     BY(VECTOR_ARITH_TAC);
1627   TYPIFY `v dot u = u dot v` (C SUBGOAL_THEN SUBST1_TAC);
1628     BY(VECTOR_ARITH_TAC);
1629   BY(REAL_ARITH_TAC)
1630   ]);;
1631   (* }}} *)
1632
1633 let SDIFF_SYM = prove_by_refinement(
1634   `!(X:A->bool) Y. SDIFF X Y = SDIFF Y X`,
1635   (* {{{ proof *)
1636   [
1637   REWRITE_TAC[SDIFF];
1638   BY(SET_TAC[])
1639   ]);;
1640   (* }}} *)
1641
1642 let MCELL2_VOL_SPLIT_EXPLICIT = prove_by_refinement(
1643   `!V X ul h.        saturated V /\
1644          packing V /\
1645          barV V 3 ul /\
1646          X = mcell2 V ul /\
1647          h = hl (truncate_simplex 1 ul) /\
1648          h < sqrt(&2) /\
1649          ~NULLSET X ==>
1650          vol (X INTER bis_le (EL 0 ul) (EL 1 ul)) =
1651              dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3)  * (&2 - h pow 2) * h / &6`,
1652   (* {{{ proof *)
1653   [
1654   REPEAT WEAK_STRIP_TAC;
1655   TYPIFY `dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) < pi` (C SUBGOAL_THEN ASSUME_TAC);
1656     MATCH_MP_TAC MCELL2_DIHV_LT_PI;
1657     BY(ASM_MESON_TAC[]);
1658   INTRO_TAC MCELL2_DIHV_AZIM [`V`;`X`;`ul`;`h`];
1659   ANTS_TAC;
1660     BY(ASM_MESON_TAC[]);
1661   REPEAT WEAK_STRIP_TAC;
1662   ASM_REWRITE_TAC[];
1663   INTRO_TAC NOT_COPLANAR_EXTREME_MCELL2 [`V`;`ul`];
1664   ASM_REWRITE_TAC[];
1665   ANTS_TAC;
1666     BY(ASM_MESON_TAC[IN]);
1667   DISCH_TAC;
1668   TYPIFY `~collinear {EL 0 ul,EL 1 ul,mxi V ul} /\ ~collinear {EL 0 ul, EL 1 ul,omega_list_n V ul 3}` ((C SUBGOAL_THEN ASSUME_TAC));
1669     TYPIFY `!a b c (d:real^3). {a,b,c,d} = {a,b,d,c}` ((C SUBGOAL_THEN MP_TAC));
1670       BY(SET_TAC[]);
1671     BY(ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);
1672   TYPIFY `~collinear {EL 0 ul, EL 1 ul,w1} /\ ~collinear {EL 0 ul,EL 1 ul, w2}` (C SUBGOAL_THEN ASSUME_TAC);
1673     FIRST_X_ASSUM_ST `{a,b} = {c,d}` MP_TAC;
1674     REWRITE_TAC[Geomdetail.PAIR_EQ_EXPAND];
1675     BY(REPEAT WEAK_STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]);
1676   TYPIFY `&0 < h` (C SUBGOAL_THEN ASSUME_TAC);
1677     ASM_REWRITE_TAC[];
1678     MATCH_MP_TAC Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT;
1679     BY(ASM_MESON_TAC[]);
1680   INTRO_TAC VOLUME_FRUSTT_WEDGE [`EL 0 ul`;`EL 1 ul`;`w1`;`w2`;`h`;`h / sqrt(&2)`];
1681   ANTS_TAC;
1682     ASM_REWRITE_TAC[];
1683     REWRITE_TAC[real_div];
1684     GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
1685     GMATCH_SIMP_TAC REAL_LT_INV;
1686     GMATCH_SIMP_TAC REAL_LT_RSQRT;
1687     CONJ_TAC;
1688       BY(REAL_ARITH_TAC);
1689     BY(ASM_MESON_TAC[]);
1690   REPEAT WEAK_STRIP_TAC;
1691   FIRST_X_ASSUM MP_TAC;
1692   COND_CASES_TAC;
1693     PROOF_BY_CONTR_TAC;
1694     FIRST_X_ASSUM_ST `\/` MP_TAC;
1695     ASM_SIMP_TAC[arith `&0 < h ==> ~(h < &0)`];
1696     GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
1697     GMATCH_SIMP_TAC REAL_LT_RSQRT;
1698     BY(REPEAT (FIRST_X_ASSUM_ST `<` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
1699   TYPIFY `(h / (h / sqrt(&2))) pow 2 = &2` (C SUBGOAL_THEN SUBST1_TAC);
1700     Calc_derivative.CALC_ID_TAC;
1701     CONJ2_TAC;
1702       REWRITE_TAC[GSYM Sphere.sqrt2;REAL_POW_MUL];
1703       REWRITE_TAC[Nonlin_def.sqrt2_sqrt2;REAL_POW_2];
1704       BY(REAL_ARITH_TAC);
1705     ASM_SIMP_TAC[arith `&0 < h ==> ~(h = &0)`;arith `~(&1 = &0)`];
1706     GMATCH_SIMP_TAC SQRT_EQ_0;
1707     BY(REAL_ARITH_TAC);
1708   ASM_REWRITE_TAC[];
1709   DISCH_THEN (SUBST1_TAC o GSYM);
1710   MATCH_MP_TAC Vol1.VOLUME_PROPS_SDIFF;
1711   CONJ_TAC;
1712     MATCH_MP_TAC MCELL2_INTER_BIS_LE_MEASURABLE;
1713     BY(ASM_MESON_TAC[]);
1714   CONJ_TAC;
1715     FIRST_X_ASSUM_ST `frustt` MP_TAC;
1716     BY(ASM_REWRITE_TAC[]);
1717   GMATCH_SIMP_TAC MCELL2_SPLIT;
1718   TYPIFY `V` EXISTS_TAC;
1719   ASM_REWRITE_TAC[];
1720   FIRST_X_ASSUM_ST `{a,b} = {c,d}` (ASSUME_TAC o GSYM);
1721   ASM_REWRITE_TAC[];
1722   GMATCH_SIMP_TAC (GSYM Local_lemmas.WEDGE_GE_EQ_AFF_GE);
1723   ASM_REWRITE_TAC[];
1724   CONJ_TAC;
1725     BY(ASM_MESON_TAC[]);
1726   CONJ_TAC;
1727     BY(ASM_MESON_TAC[]);
1728   ONCE_REWRITE_TAC[SDIFF_SYM];
1729   ONCE_REWRITE_TAC[SET_RULE `a INTER b INTER c = a INTER c INTER b`];
1730   REWRITE_TAC[BIS_LE_NORM];
1731   TYPIFY `hl (truncate_simplex 1 ul) = dist(EL 1 ul,EL 0 ul) / &2` (C SUBGOAL_THEN ASSUME_TAC);
1732     GMATCH_SIMP_TAC BARV3_TRUNC1;
1733     CONJ_TAC;
1734       BY(ASM_MESON_TAC[IN]);
1735     ONCE_REWRITE_TAC[DIST_SYM];
1736     REWRITE_TAC[Marchal_cells_3.HL_2];
1737     BY(REAL_ARITH_TAC);
1738   TYPIFY `norm (EL 1 ul - EL 0 ul) pow 2 / &2 = hl (truncate_simplex 1 ul) * norm (EL 1 ul - EL 0 ul)` (C SUBGOAL_THEN SUBST1_TAC);
1739     ASM_REWRITE_TAC[dist];
1740     BY(REAL_ARITH_TAC);
1741   MATCH_MP_TAC FRUSTT_WEDGE_RCONE_GE;
1742   FIRST_X_ASSUM kill;
1743   ASM_REWRITE_TAC[];
1744   TYPIFY `&0 < sqrt(&2)` (C SUBGOAL_THEN ASSUME_TAC);
1745     GMATCH_SIMP_TAC REAL_LT_RSQRT;
1746     BY(REAL_ARITH_TAC);
1747   TYPIFY `&0 < hl(truncate_simplex 1 ul)` (C SUBGOAL_THEN ASSUME_TAC);
1748     BY(ASM_MESON_TAC[Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT]);
1749   SUBCONJ_TAC;
1750     GMATCH_SIMP_TAC REAL_LT_DIV;
1751     BY(ASM_REWRITE_TAC[]);
1752   DISCH_TAC;
1753   SUBCONJ_TAC;
1754     BY(ASM_MESON_TAC[IN;MCELL2_VX_PROPS]);
1755   DISCH_TAC;
1756   ASM_SIMP_TAC[arith `&0 < h ==> &0 <= h`];
1757   GMATCH_SIMP_TAC REAL_LE_LDIV_EQ;
1758   ASM_REWRITE_TAC[];
1759   REWRITE_TAC[arith `&1 * x = x`];
1760   MATCH_MP_TAC (arith `x < y ==> x <= y`);
1761   BY(ASM_MESON_TAC[])
1762   ]);;
1763   (* }}} *)
1764
1765 let MCELL2_HL_LT_SQRT2 = prove_by_refinement(
1766   `!V ul.        saturated V /\
1767          packing V /\
1768          barV V 3 ul /\
1769          ~NULLSET (mcell2 V ul) ==>
1770           hl (truncate_simplex 1 ul) < sqrt(&2)
1771 `,
1772   (* {{{ proof *)
1773   [
1774   REPEAT WEAK_STRIP_TAC;
1775   PROOF_BY_CONTR_TAC;
1776   FIRST_X_ASSUM_ST `NULLSET` MP_TAC;
1777   BY(ASM_REWRITE_TAC[Pack_defs.mcell2;NEGLIGIBLE_EMPTY])
1778   ]);;
1779   (* }}} *)
1780
1781 let LEFT_ACTION_LIST_1_PROPERTIES_ALT = prove_by_refinement(
1782  `!V ul xl p.
1783          packing V /\
1784          saturated V /\
1785          barV V 3 ul /\
1786          p permutes 0..1 /\
1787          hl (truncate_simplex 1 ul) < sqrt (&2) /\
1788          sqrt (&2) <= hl ul /\
1789          xl = left_action_list p ul
1790          ==> xl IN barV V 3 /\
1791              omega_list_n V xl 1 = omega_list_n V ul 1 /\
1792              omega_list_n V xl 2 = omega_list_n V ul 2 /\
1793              omega_list_n V xl 3 = omega_list_n V ul 3 /\
1794              mxi V xl = mxi V ul`,
1795   (* {{{ proof *)
1796   [
1797   REWRITE_TAC[Marchal_cells_2_new.LEFT_ACTION_LIST_1_PROPERTIES]
1798   ]);;
1799   (* }}} *)
1800
1801 let MCELL2_PERMUTE_01 = prove_by_refinement(
1802   `!V ul. saturated V /\ packing V /\ barV V 3 ul /\ ~NULLSET (mcell2 V ul) ==>
1803     (?vl.  (EL 0 ul = EL 1 vl) /\ (EL 1 ul = EL 0 vl) /\ (mxi V ul = mxi V vl) /\
1804        (omega_list_n V ul 3 = omega_list_n V vl 3) /\
1805        (hl (truncate_simplex 1 ul) = hl (truncate_simplex 1 vl)) /\
1806        (mcell2 V ul = mcell2 V vl) /\ barV V 3 vl)`,
1807   (* {{{ proof *)
1808   [
1809   REPEAT WEAK_STRIP_TAC;
1810   TYPIFY `LENGTH ul = 4` (C SUBGOAL_THEN ASSUME_TAC);
1811     BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3 + 1 = 4`]);
1812   INTRO_TAC Bump.LENGTH4 [`ul`];
1813   ANTS_TAC;
1814     BY(ASM_REWRITE_TAC[]);
1815   INTRO_TAC MCELL2_HL_LT_SQRT2 [`V`;`ul`];
1816   ANTS_TAC;
1817     BY(ASM_MESON_TAC[]);
1818   REPEAT WEAK_STRIP_TAC;
1819   INTRO_TAC Leaf_cell.TWO_REARRANGEMENT_LEMMA_ALT [`V`;`ul`;`EL 0 ul`;`EL 1 ul`;`EL 2 ul`;`EL 3 ul`];
1820   ANTS_TAC;
1821     BY(ASM_MESON_TAC[]);
1822   REPEAT WEAK_STRIP_TAC;
1823   TYPED_ABBREV_TAC  `(vl:(real^3) list) = left_action_list p ul` ;
1824   TYPIFY `vl` EXISTS_TAC;
1825   INTRO_TAC LEFT_ACTION_LIST_1_PROPERTIES_ALT [`V`;`ul`;`vl`;`p`];
1826   ANTS_TAC;
1827     ASM_REWRITE_TAC[];
1828     PROOF_BY_CONTR_TAC;
1829     FIRST_X_ASSUM_ST `mcell2` MP_TAC;
1830     BY(ASM_REWRITE_TAC[Pack_defs.mcell2;NEGLIGIBLE_EMPTY]);
1831   REWRITE_TAC[IN;Bump.MCELL2];
1832   REPEAT WEAK_STRIP_TAC;
1833   ASM_REWRITE_TAC[];
1834   INTRO_TAC Rvfxzbu.RVFXZBU [`V`;`ul`;`2`;`p`];
1835   ANTS_TAC;
1836     BY(ASM_REWRITE_TAC[arith `2 - 1 = 1`;IN_INSERT]);
1837   DISCH_TAC;
1838   REWRITE_TAC[CONJ_ASSOC];
1839   CONJ2_TAC;
1840     BY(ASM_MESON_TAC[]);
1841   PROOF_BY_CONTR_TAC;
1842   TYPIFY `LENGTH vl = 4` (C SUBGOAL_THEN ASSUME_TAC);
1843     BY(ASM_MESON_TAC[IN;Sphere.BARV;arith `3 + 1 = 4`]);
1844   INTRO_TAC Bump.LENGTH4 [`vl`];
1845   ANTS_TAC;
1846     BY(ASM_REWRITE_TAC[]);
1847   DISCH_TAC;
1848   FIRST_X_ASSUM_ST `~` MP_TAC;
1849   REWRITE_TAC[];
1850   SUBCONJ_TAC;
1851     BY(ASM_MESON_TAC[CONS_11]);
1852   DISCH_TAC;
1853   REWRITE_TAC[Pack_defs.HL];
1854   AP_TERM_TAC;
1855   REPEAT (GMATCH_SIMP_TAC Bump.SET_OF_LIST_TRUNCATE_1);
1856   ASM_SIMP_TAC[arith `x = 4 ==> 2 <= x`];
1857   BY(SET_TAC[])
1858   ]);;
1859   (* }}} *)
1860
1861 let MCELL2_VOL = prove_by_refinement(
1862   `!V X ul h.        saturated V /\
1863          packing V /\
1864          barV V 3 ul /\
1865          X = mcell2 V ul /\
1866          h = hl (truncate_simplex 1 ul) /\
1867          ~NULLSET X ==>
1868          vol X =
1869              dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3)  * (&2 - h pow 2) * h / &3`,
1870   (* {{{ proof *)
1871   [
1872   REPEAT WEAK_STRIP_TAC;
1873   INTRO_TAC MCELL2_VOL_SPLIT [`V`;`X`;`ul`];
1874   ANTS_TAC;
1875     BY(ASM_MESON_TAC[]);
1876   DISCH_THEN SUBST1_TAC;
1877   MATCH_MP_TAC (arith `x = a/ &2 /\ y = a / &2 ==> (x + y = a)`);
1878   TYPIFY `h < sqrt(&2)` (C SUBGOAL_THEN ASSUME_TAC);
1879     ASM_REWRITE_TAC[];
1880     BY(ASM_MESON_TAC[MCELL2_HL_LT_SQRT2]);
1881   COMMENT "first branch";
1882   CONJ_TAC;
1883     INTRO_TAC MCELL2_VOL_SPLIT_EXPLICIT [`V`;`X`;`ul`;`h`];
1884     ANTS_TAC;
1885       BY(ASM_MESON_TAC[]);
1886     DISCH_THEN SUBST1_TAC;
1887     BY(REAL_ARITH_TAC);
1888   COMMENT "second branch";
1889   INTRO_TAC MCELL2_PERMUTE_01 [`V`;`ul`];
1890   ANTS_TAC;
1891     BY(ASM_MESON_TAC[]);
1892   REPEAT WEAK_STRIP_TAC;
1893   ASM_REWRITE_TAC[];
1894   ONCE_REWRITE_TAC[Marchal_cells_2_new.DIHV_SYM];
1895   INTRO_TAC MCELL2_VOL_SPLIT_EXPLICIT [`V`;`X`;`vl`;`hl (truncate_simplex 1 vl)`];
1896   ANTS_TAC;
1897     BY(ASM_MESON_TAC[]);
1898   ASM_REWRITE_TAC[];
1899   DISCH_THEN SUBST1_TAC;
1900   BY(REAL_ARITH_TAC)
1901   ]);;
1902   (* }}} *)
1903
1904 let BALL_SUBSET_BIS_LE = prove_by_refinement(
1905   `!u (v:real^A) r.
1906     &2 * r <= dist(u,v) ==>
1907     ball(u,r) SUBSET bis_le u v`,
1908   (* {{{ proof *)
1909   [
1910   REWRITE_TAC[ball;Sphere.bis_le;SUBSET;IN_ELIM_THM];
1911   REPEAT WEAK_STRIP_TAC;
1912   TYPIFY `dist(x,u) = dist(u,x)` (C SUBGOAL_THEN SUBST1_TAC);
1913     BY(MESON_TAC[DIST_SYM]);
1914   PROOF_BY_CONTR_TAC;
1915   INTRO_TAC DIST_TRIANGLE [`u`;`x`;`v`];
1916   BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
1917   ]);;
1918   (* }}} *)
1919
1920 let BALL_SUBSET_BIS_LT = prove_by_refinement(
1921   `!u (v:real^A) r.
1922     &2 * r <= dist(u,v) ==>
1923     ball(u,r) SUBSET {y | dist(y, u) < dist(y, v)}`,
1924   (* {{{ proof *)
1925   [
1926   REWRITE_TAC[ball;Sphere.bis_le;SUBSET;IN_ELIM_THM];
1927   REPEAT WEAK_STRIP_TAC;
1928   TYPIFY `dist(x,u) = dist(u,x)` (C SUBGOAL_THEN SUBST1_TAC);
1929     BY(MESON_TAC[DIST_SYM]);
1930   PROOF_BY_CONTR_TAC;
1931   INTRO_TAC DIST_TRIANGLE [`u`;`x`;`v`];
1932   BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
1933   ]);;
1934   (* }}} *)
1935
1936 let RADIAL_LE = prove_by_refinement(
1937   `!r r' (x:real^3) C.     r' <= r /\ &0 < r'
1938             ==> radial r x (C INTER ball( x, r))
1939             ==> radial r' x (C INTER ball( x, r'))`,
1940   (* {{{ proof *)
1941   [
1942   BY(REWRITE_TAC[Marchal_cells_2_new.RADIAL_VS_RADIAL_NORM;GSYM NORMBALL_BALL;Conforming.RADIAL_NORM_CO])
1943   ]);;
1944   (* }}} *)
1945
1946 let MCELL2_SOL = prove_by_refinement(
1947   `!V X ul h.        saturated V /\
1948          packing V /\
1949          barV V 3 ul /\
1950          X = mcell2 V ul /\
1951          h = hl (truncate_simplex 1 ul) /\
1952          h < sqrt(&2) /\
1953          ~NULLSET X ==>
1954          sol (EL 0 ul) X =
1955              dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3)  * (&1 - h / sqrt(&2))`,
1956   (* {{{ proof *)
1957   [
1958   REPEAT WEAK_STRIP_TAC;
1959   TYPIFY `dist(EL 0 ul,EL 1 ul) / &2 = hl (truncate_simplex 1 ul) ` (C SUBGOAL_THEN ASSUME_TAC);
1960     GMATCH_SIMP_TAC BARV3_TRUNC1;
1961     CONJ_TAC;
1962       BY(ASM_MESON_TAC[IN]);
1963     REWRITE_TAC[Marchal_cells_3.HL_2];
1964     BY(REAL_ARITH_TAC);
1965   TYPIFY `!r. r < h ==> X INTER ball (EL 0 ul,r) = (X INTER bis_le (EL 0 ul) (EL 1 ul)) INTER ball(EL 0 ul,r)` (C SUBGOAL_THEN ASSUME_TAC);
1966     REPEAT WEAK_STRIP_TAC;
1967     TYPIFY `ball (EL 0 ul,r) SUBSET bis_le (EL 0 ul) (EL 1 ul)` ENOUGH_TO_SHOW_TAC;
1968       BY(SET_TAC[]);
1969     MATCH_MP_TAC BALL_SUBSET_BIS_LE;
1970     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1971   TYPIFY `&0 < sqrt(&2) ` (C SUBGOAL_THEN ASSUME_TAC);
1972     GMATCH_SIMP_TAC REAL_LT_RSQRT;
1973     BY(REAL_ARITH_TAC);
1974   TYPIFY `&0 < h` (C SUBGOAL_THEN ASSUME_TAC);
1975     ASM_REWRITE_TAC[];
1976     MATCH_MP_TAC Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT;
1977     BY(ASM_MESON_TAC[]);
1978   TYPIFY `&0 < h / sqrt(&2) /\ h / sqrt(&2) < &1` (C SUBGOAL_THEN ASSUME_TAC);
1979     GMATCH_SIMP_TAC REAL_LT_DIV;
1980     CONJ_TAC;
1981       BY(ASM_MESON_TAC[]);
1982     GMATCH_SIMP_TAC REAL_LT_LDIV_EQ;
1983     ASM_REWRITE_TAC[arith `(&1 * x = x)`];
1984     BY(ASM_MESON_TAC[]);
1985   COMMENT "0. basic setup of azim and dih";
1986   TYPIFY `dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) < pi` (C SUBGOAL_THEN ASSUME_TAC);
1987     MATCH_MP_TAC MCELL2_DIHV_LT_PI;
1988     BY(ASM_MESON_TAC[]);
1989   INTRO_TAC MCELL2_DIHV_AZIM [`V`;`X`;`ul`;`h`];
1990   ANTS_TAC;
1991     BY(ASM_MESON_TAC[]);
1992   REPEAT WEAK_STRIP_TAC;
1993   ASM_REWRITE_TAC[];
1994   COMMENT "show non-degeneracy";
1995   INTRO_TAC NOT_COPLANAR_EXTREME_MCELL2 [`V`;`ul`];
1996   ASM_REWRITE_TAC[];
1997   ANTS_TAC;
1998     BY(ASM_MESON_TAC[IN]);
1999   DISCH_TAC;
2000   TYPIFY `~collinear {EL 0 ul,EL 1 ul,mxi V ul} /\ ~collinear {EL 0 ul, EL 1 ul,omega_list_n V ul 3}` ((C SUBGOAL_THEN ASSUME_TAC));
2001     TYPIFY `!a b c (d:real^3). {a,b,c,d} = {a,b,d,c}` ((C SUBGOAL_THEN MP_TAC));
2002       BY(SET_TAC[]);
2003     BY(ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);
2004   TYPIFY `~collinear {EL 0 ul, EL 1 ul,w1} /\ ~collinear {EL 0 ul,EL 1 ul, w2}` (C SUBGOAL_THEN ASSUME_TAC);
2005     FIRST_X_ASSUM_ST `{a,b} = {c,d}` MP_TAC;
2006     REWRITE_TAC[Geomdetail.PAIR_EQ_EXPAND];
2007     BY(REPEAT WEAK_STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]);
2008   COMMENT "next";
2009   TYPIFY `EL 0 ul IN V` (C SUBGOAL_THEN ASSUME_TAC);
2010     INTRO_TAC MCELL2_VX_PROPS [`V`;`X`;`ul`];
2011     ANTS_TAC;
2012       BY(ASM_MESON_TAC[]);
2013     INTRO_TAC Bump.HDTFNFZ_ALT [`V`;`ul`;`2`;`X`];
2014     ANTS_TAC;
2015       BY(ASM_MESON_TAC[Bump.MCELL2]);
2016     DISCH_THEN SUBST1_TAC;
2017     BY(SET_TAC[]);
2018   INTRO_TAC Urrphbz2.URRPHBZ2 [`V`;`ul`;`2`;`EL 0 ul`];
2019   ANTS_TAC;
2020     BY(ASM_REWRITE_TAC[]);
2021   REWRITE_TAC[GSYM Bump.MCELL2];
2022   REWRITE_TAC[Sphere.eventually_radial];
2023   REPEAT WEAK_STRIP_TAC;
2024   COMMENT "next2";
2025   TYPIFY `?r'. r' <= h /\ &0 < r' /\ radial r' (EL 0 ul) (mcell2 V ul INTER ball (EL 0 ul,r'))` (C SUBGOAL_THEN MP_TAC);
2026     TYPIFY `if (r <= h) then r else h` EXISTS_TAC;
2027     COND_CASES_TAC;
2028       BY(ASM_REWRITE_TAC[arith `&0 < r <=> r > &0`]);
2029     REWRITE_TAC[arith `h <= h`];
2030     BY(ASM_MESON_TAC[RADIAL_LE;arith `~(r <= h) ==> (h <= r)`]);
2031   REPLICATE_TAC 2 (FIRST_X_ASSUM kill);
2032   REPEAT WEAK_STRIP_TAC;
2033   GMATCH_SIMP_TAC Vol1.sol_spec;
2034   TYPIFY `r'` EXISTS_TAC;
2035   ASM_REWRITE_TAC[arith `r' > &0 <=> &0 < r'`];
2036   SUBCONJ_TAC;
2037     MATCH_MP_TAC MEASURABLE_INTER;
2038     REWRITE_TAC[MEASURABLE_BALL;Bump.MCELL2];
2039     BY(ASM_MESON_TAC[Urrphbz1.MEASURABLE_MCELL]);
2040   DISCH_TAC;
2041   COMMENT "1. done with sol  ";
2042   INTRO_TAC MCELL2_VX_PROPS [`V`;`X`;`ul`];
2043   ANTS_TAC;
2044     BY(ASM_MESON_TAC[]);
2045   REPEAT WEAK_STRIP_TAC;
2046   INTRO_TAC VOLUME_CONIC_CAP_STRONG [`EL 0 ul`;`EL 1 ul`;`r'`;`h/ sqrt(&2)`];
2047   ANTS_TAC;
2048     BY(ASM_MESON_TAC[]);
2049   COND_CASES_TAC;
2050     TYPIFY `~(&1 <= h / sqrt(&2))` (C SUBGOAL_THEN ASSUME_TAC);
2051       MATCH_MP_TAC (arith `a < b ==> ~(b <= a)`);
2052       BY(ASM_REWRITE_TAC[]);
2053     BY(ASM_MESON_TAC[arith `&0 < r' ==> ~(r' < &0)`]);
2054   REPEAT WEAK_STRIP_TAC;
2055   COMMENT "add wedge";
2056   INTRO_TAC Vol1.VOLUME_PROPS_CONIC_CAP [`EL 0 ul`;`EL 1 ul`;`w1`;`w2`;`r'`;`h / sqrt(&2)`];
2057   ANTS_TAC;
2058     ASM_REWRITE_TAC[];
2059     BY(ASM_MESON_TAC[arith `&0 < r' ==> r' >= &0`;arith `&0 < h' ==> h' >= -- &1`;arith `h' < &1 ==> h' <= &1`]);
2060   REWRITE_TAC[vol_conic_cap_wedge];
2061   TYPIFY `!v x. &3 * v / r' pow 3 = x <=> v = x * r' pow 3 / &3` (C SUBGOAL_THEN (unlist REWRITE_TAC));
2062     REPEAT WEAK_STRIP_TAC;
2063     MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a = b)`);
2064     CONJ_TAC THEN REPEAT WEAK_STRIP_TAC;
2065       EXPAND_TAC "x";
2066       Calc_derivative.CALC_ID_TAC;
2067       BY(ASM_MESON_TAC[arith `~(&3 = &0)`;arith `&0 < r' ==> ~(r' = &0)`]);
2068     ASM_REWRITE_TAC[];
2069     Calc_derivative.CALC_ID_TAC;
2070     BY(ASM_MESON_TAC[arith `~(&3 = &0)`;arith `&0 < r' ==> ~(r' = &0)`]);
2071   ASM_REWRITE_TAC[GSYM REAL_MUL_ASSOC];
2072   DISCH_THEN (SUBST1_TAC o SYM);
2073   COMMENT "pure volumes left";
2074   MATCH_MP_TAC Vol1.VOLUME_PROPS_SDIFF;
2075   ASM_REWRITE_TAC[];
2076   CONJ_TAC;
2077     BY(REWRITE_TAC[MEASURABLE_CONIC_CAP_WEDGE]);
2078   REWRITE_TAC[conic_cap;NORMBALL_BALL];
2079   COMMENT "SDIFF to match volumes";
2080   ONCE_REWRITE_TAC[SDIFF_SYM];
2081   INTRO_TAC FRUSTT_WEDGE_RCONE_GE [`EL 0 ul`;`EL 1 ul`;`w1`;`w2`;`h`;`h/ sqrt(&2)`];
2082   ANTS_TAC;
2083     ASM_REWRITE_TAC[];
2084     BY(ASM_MESON_TAC[arith `h' < y ==> h' <= y`]);
2085   ASM_REWRITE_TAC[];
2086   DISCH_TAC;
2087   INTRO_TAC SDIFF_SUBSET [`(frustt (EL 0 ul) (EL 1 ul) (hl (truncate_simplex 1 ul))        (hl (truncate_simplex 1 ul) / sqrt (&2)) INTER       wedge (EL 0 ul) (EL 1 ul) w1 w2)`;` (rcone_ge (EL 0 ul) (EL 1 ul) (hl (truncate_simplex 1 ul) / sqrt (&2)) INTER      {y | (y - EL 0 ul) dot (EL 1 ul - EL 0 ul) <=           hl (truncate_simplex 1 ul) * norm (EL 1 ul - EL 0 ul)} INTER      wedge_ge (EL 0 ul) (EL 1 ul) w1 w2)`;`ball ((EL 0 ul),r')`];
2088   DISCH_THEN (MP_TAC o (MATCH_MP (REWRITE_RULE[TAUT `(a /\ b ==> c) <=> (b ==> (a ==> c))`] NEGLIGIBLE_SUBSET)));
2089   ANTS_TAC;
2090     BY(ASM_REWRITE_TAC[]);
2091   COMMENT "match frustt";
2092   TYPIFY `(frustt (EL 0 ul) (EL 1 ul) (hl (truncate_simplex 1 ul))    (hl (truncate_simplex 1 ul) / sqrt (&2)) INTER    wedge (EL 0 ul) (EL 1 ul) w1 w2) INTER   ball (EL 0 ul,r') = (ball (EL 0 ul,r') INTER        rcone_gt (EL 0 ul) (EL 1 ul) (hl (truncate_simplex 1 ul) / sqrt (&2))) INTER       wedge (EL 0 ul) (EL 1 ul) w1 w2` (C SUBGOAL_THEN SUBST1_TAC);
2093     REWRITE_TAC[frustt;frustum;LET_DEF;EXTENSION;IN_ELIM_THM;LET_DEF;LET_END_DEF;IN_INTER];
2094     REPEAT WEAK_STRIP_TAC;
2095     REWRITE_TAC[arith `&0 * x = &0`];
2096     TYPIFY `~(x IN ball(EL 0 ul,r'))` ASM_CASES_TAC;
2097       BY(ASM_REWRITE_TAC[]);
2098     TYPIFY `~(x IN rcone_gt (EL 0 ul) (EL 1 ul) (hl (truncate_simplex 1 ul) / sqrt (&2)))` ASM_CASES_TAC;
2099       BY(ASM_MESON_TAC[IN]);
2100     TYPIFY `~(x IN wedge (EL 0 ul) (EL 1 ul) w1 w2)` ASM_CASES_TAC;
2101       BY(ASM_REWRITE_TAC[]);
2102     REPEAT (FIRST_X_ASSUM_ST `~ ~ x` MP_TAC) THEN REWRITE_TAC[] THEN REPEAT WEAK_STRIP_TAC THEN ASM_REWRITE_TAC[];
2103     CONJ_TAC;
2104       BY(ASM_MESON_TAC[IN]);
2105     CONJ_TAC;
2106       FIRST_X_ASSUM_ST `rcone_gt` MP_TAC;
2107       REWRITE_TAC[Sphere.rcone_gt;Sphere.rconesgn;IN_ELIM_THM];
2108       TYPIFY `&0 <=  dist (x,EL 0 ul) * dist (EL 1 ul,EL 0 ul) * hl (truncate_simplex 1 ul) / sqrt (&2)` ENOUGH_TO_SHOW_TAC;
2109         BY(REAL_ARITH_TAC);
2110       GMATCH_SIMP_TAC REAL_LE_MUL;
2111       GMATCH_SIMP_TAC REAL_LE_MUL;
2112       REWRITE_TAC[DIST_POS_LE];
2113       MATCH_MP_TAC (arith `&0 < h' ==> &0 <= h'`);
2114       BY(ASM_MESON_TAC[]);
2115     INTRO_TAC BALL_SUBSET_BIS_LT [`EL 0 ul`;`EL 1 ul`;`r'`];
2116     ANTS_TAC;
2117       BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2118     REWRITE_TAC[SUBSET;IN_ELIM_THM];
2119     DISCH_THEN (C INTRO_TAC [`x`]);
2120     ASM_REWRITE_TAC[];
2121     REWRITE_TAC[BIS_LT_NORM];
2122     ONCE_REWRITE_TAC[arith `x pow 2 / &2 = (x / &2) * x`];
2123     FIRST_X_ASSUM_ST `dist a / &2 = h` (SUBST1_TAC o GSYM);
2124     ONCE_REWRITE_TAC[DIST_SYM];
2125     BY(REWRITE_TAC[dist]);
2126   TYPIFY `((rcone_ge (EL 0 ul) (EL 1 ul) (hl (truncate_simplex 1 ul) / sqrt (&2)) INTER    {y | (y - EL 0 ul) dot (EL 1 ul - EL 0 ul) <=        hl (truncate_simplex 1 ul) * norm (EL 1 ul - EL 0 ul)} INTER   wedge_ge (EL 0 ul) (EL 1 ul) w1 w2) INTER  ball (EL 0 ul,r')) =  (mcell2 V ul INTER ball (EL 0 ul,r'))` ENOUGH_TO_SHOW_TAC;
2127     DISCH_THEN SUBST1_TAC;
2128     BY(REWRITE_TAC[]);
2129   TYPIFY `mcell2 V ul INTER ball (EL 0 ul,r') = mcell2 V ul INTER bis_le (EL 0 ul) (EL 1 ul) INTER ball (EL 0 ul,r')` (C SUBGOAL_THEN SUBST1_TAC);
2130     INTRO_TAC BALL_SUBSET_BIS_LE [`EL 0 ul`;`EL 1 ul`;`r'`];
2131     ANTS_TAC;
2132       BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2133     BY(SET_TAC[]);
2134   INTRO_TAC MCELL2_SPLIT [`V`;`mcell2 V ul`;`ul`];
2135   ANTS_TAC;
2136     BY(ASM_MESON_TAC[]);
2137   REWRITE_TAC[GSYM INTER_ASSOC];
2138   DISCH_THEN SUBST1_TAC;
2139   FIRST_X_ASSUM_ST `{a,b} = {c,d}` (SUBST1_TAC o SYM);
2140   TYPIFY `wedge_ge (EL 0 ul) (EL 1 ul) w1 w2 = aff_ge {EL 0 ul, EL 1 ul} {w1,w2}` (C SUBGOAL_THEN SUBST1_TAC);
2141     MATCH_MP_TAC Local_lemmas.WEDGE_GE_EQ_AFF_GE;
2142     BY(ASM_MESON_TAC[]);
2143   REWRITE_TAC[BIS_LE_NORM];
2144   ONCE_REWRITE_TAC[arith `x pow 2 / &2 = (x / &2) * x`];
2145   FIRST_X_ASSUM_ST `dist a / &2 = h` (SUBST1_TAC o GSYM);
2146   ONCE_REWRITE_TAC[DIST_SYM];
2147   REWRITE_TAC[dist];
2148   BY(SET_TAC[])
2149   ]);;
2150   (* }}} *)
2151
2152 let gamma2_x_div_azim_v2 =
2153   new_definition `gamma2_x_div_azim_v2 m x = (&8 - x)* sqrt x / (&24) -
2154   ( &2 * (&2 * mm1/ pi) * (&1 - sqrt x / sqrt8) -
2155       (&8 * mm2 / pi) * m * lfun (sqrt x / &2))`;;
2156
2157 (*
2158 let GAMMAX_GAMMA2_X = prove_by_refinement(
2159   `!V X ul y1 y2 y3 y4 y5 y6.
2160         saturated V /\
2161          packing V /\
2162          barV V 3 ul /\
2163          X = mcell2 V ul /\
2164           ~NULLSET X /\
2165     y1 = dist(EL 0 ul,EL 1 ul) /\
2166     y2 = dist(EL 0 ul,mxi V ul) /\
2167     y3 = dist(EL 0 ul,omega_list_n V ul 3) /\
2168     y4 = dist(mxi V ul,omega_list_n V ul 3) /\
2169     y5 = dist(EL 1 ul,omega_list_n V ul 3) /\
2170     y6 = dist(EL 1 ul,mxi V ul)
2171     ==>
2172     gammaX V X lmfun =
2173              gamma2_x_div_azim_v2 (h0cut y1) (y1 * y1) * dih_y y1 y2 y3 y4 y5 y6`,
2174   (* {{{ proof *)
2175   [
2176   REPEAT WEAK_STRIP_TAC;
2177   INTRO_TAC GAMMAX_MCELL2 [`V`;`X`;`ul`];
2178   ANTS_TAC;
2179     BY(ASM_MESON_TAC[]);
2180   DISCH_THEN SUBST1_TAC;
2181   INTRO_TAC MCELL2_VOL [`V`;`X`;`ul`;`hl (truncate_simplex 1 ul)`];
2182   ANTS_TAC;
2183     BY(ASM_MESON_TAC[]);
2184   DISCH_THEN SUBST1_TAC;
2185   INTRO_TAC MCELL2_HL_LT_SQRT2 [`V`;`ul`];
2186   ANTS_TAC;
2187     BY(ASM_MESON_TAC[]);
2188   REPEAT WEAK_STRIP_TAC;
2189   INTRO_TAC MCELL2_SOL [`V`;`X`;`ul`;`hl (truncate_simplex 1 ul)`];
2190   ANTS_TAC;
2191     BY(ASM_MESON_TAC[]);
2192   DISCH_THEN SUBST1_TAC;
2193   TYPIFY `sol (EL 1 ul) X =  dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) * (&1 - hl (truncate_simplex 1 ul) / sqrt (&2))` (C SUBGOAL_THEN MP_TAC);
2194     INTRO_TAC MCELL2_PERMUTE_01 [`V`;`ul`];
2195     ANTS_TAC;
2196       BY(ASM_MESON_TAC[]);
2197     REPEAT WEAK_STRIP_TAC;
2198     ASM_REWRITE_TAC[];
2199     INTRO_TAC MCELL2_SOL [`V`;`X`;`vl`;`hl (truncate_simplex 1 vl)`];
2200     ANTS_TAC;
2201       BY(ASM_MESON_TAC[]);
2202     ASM_REWRITE_TAC[];
2203     DISCH_THEN SUBST1_TAC;
2204     BY(MESON_TAC[Marchal_cells_2_new.DIHV_SYM]);
2205   DISCH_THEN SUBST1_TAC;
2206   INTRO_TAC MCELL2_DIHX [`V`;`X`;`ul`];
2207   ANTS_TAC;
2208     BY(ASM_MESON_TAC[]);
2209   DISCH_THEN SUBST1_TAC;
2210   REWRITE_TAC[arith `d * a - m * (d * a' + d * a') + m' * l * d = (a - &2 * m * a' + m' * l) * d`];
2211   MATCH_MP_TAC (arith `a = b /\ c = d ==> (a*c = b * d)`);
2212   COMMENT "show non-degeneracy";
2213   INTRO_TAC NOT_COPLANAR_EXTREME_MCELL2 [`V`;`ul`];
2214   ASM_REWRITE_TAC[];
2215   ANTS_TAC;
2216     BY(ASM_MESON_TAC[IN]);
2217   DISCH_TAC;
2218   TYPIFY `~collinear {EL 0 ul,EL 1 ul,mxi V ul} /\ ~collinear {EL 0 ul, EL 1 ul,omega_list_n V ul 3}` ((C SUBGOAL_THEN ASSUME_TAC));
2219     TYPIFY `!a b c (d:real^3). {a,b,c,d} = {a,b,d,c}` ((C SUBGOAL_THEN MP_TAC));
2220       BY(SET_TAC[]);
2221     BY(ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);
2222   CONJ2_TAC;
2223     INTRO_TAC Merge_ineq.DIHV_EQ_DIH_Y [`EL 0 ul`;`EL 1 ul`;`mxi V ul`;`omega_list_n V ul 3`];
2224     ANTS_TAC;
2225       BY(ASM_MESON_TAC[]);
2226     BY(REWRITE_TAC[LET_DEF;LET_END_DEF]);
2227   TYPED_ABBREV_TAC  `(h:real) = hl (truncate_simplex 1 ul)` ;
2228   TYPIFY `dist(EL 0 ul,EL 1 ul)  = &2 * hl (truncate_simplex 1 ul) ` (C SUBGOAL_THEN ASSUME_TAC);
2229     ONCE_REWRITE_TAC[arith `(x = &2 * h <=> x / &2 = h)`];
2230     GMATCH_SIMP_TAC BARV3_TRUNC1;
2231     CONJ_TAC;
2232       BY(ASM_MESON_TAC[IN]);
2233     REWRITE_TAC[Marchal_cells_3.HL_2];
2234     BY(REAL_ARITH_TAC);
2235   ASM_REWRITE_TAC[];
2236   REWRITE_TAC[gamma2_x_div_azim_v2];
2237   COMMENT "simplify polynomial identity";
2238   TYPIFY `&0 < h` (C SUBGOAL_THEN ASSUME_TAC);
2239     EXPAND_TAC "h";
2240     MATCH_MP_TAC Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT;
2241     BY(ASM_MESON_TAC[]);
2242   TYPIFY `[EL 0 ul; EL 1 ul] = truncate_simplex 1 ul` (C SUBGOAL_THEN SUBST1_TAC);
2243     BY(ASM_MESON_TAC[BARV3_TRUNC1;IN]);
2244   TYPIFY `sqrt((&2 * h) * (&2 * h)) = &2 * h` (C SUBGOAL_THEN SUBST1_TAC);
2245     GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2246     BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
2247   MATCH_MP_TAC (arith `(a = a') /\ (b = b') /\ (c = c') ==> a - b + c = a' - (b' - c')`);
2248   CONJ_TAC;
2249     BY(REAL_ARITH_TAC);
2250   CONJ2_TAC;
2251     AP_TERM_TAC;
2252     ASM_REWRITE_TAC[];
2253     INTRO_TAC Merge_ineq.lmfun_h0cut [`(&2 * h)`];
2254     REWRITE_TAC[arith `(&2 * h) / &2 = h`];
2255     BY(REAL_ARITH_TAC);
2256   AP_TERM_TAC;
2257   AP_TERM_TAC;
2258   AP_TERM_TAC;
2259   REWRITE_TAC[Nonlinear_lemma.sqrt8_sqrt2;Sphere.sqrt2];
2260   Calc_derivative.CALC_ID_TAC;
2261   REPEAT (GMATCH_SIMP_TAC SQRT_EQ_0);
2262   BY(REAL_ARITH_TAC)
2263   ]);;
2264   (* }}} *)
2265 *)
2266
2267 let GAMMAX_GAMMA2_X = prove_by_refinement(
2268   `!V X ul y1 y2 y3 y4 y5 y6.
2269         saturated V /\
2270          packing V /\
2271          barV V 3 ul /\
2272          X = mcell2 V ul /\
2273           ~NULLSET X /\
2274     y1 = dist(EL 0 ul,EL 1 ul) /\
2275     y2 = dist(EL 0 ul,mxi V ul) /\
2276     y3 = dist(EL 0 ul,omega_list_n V ul 3) /\
2277     y4 = dist(mxi V ul,omega_list_n V ul 3) /\
2278     y5 = dist(EL 1 ul,omega_list_n V ul 3) /\
2279     y6 = dist(EL 1 ul,mxi V ul)
2280     ==>
2281     &0 <= dih_y y1 y2 y3 y4 y5 y6 /\
2282     gammaX V X lmfun =
2283              gamma2_x_div_azim_v2 (h0cut y1) (y1 * y1) * dih_y y1 y2 y3 y4 y5 y6`,
2284   (* {{{ proof *)
2285   [
2286   REPEAT WEAK_STRIP_TAC;
2287   INTRO_TAC GAMMAX_MCELL2 [`V`;`X`;`ul`];
2288   ANTS_TAC;
2289     BY(ASM_MESON_TAC[]);
2290   DISCH_THEN SUBST1_TAC;
2291   INTRO_TAC MCELL2_VOL [`V`;`X`;`ul`;`hl (truncate_simplex 1 ul)`];
2292   ANTS_TAC;
2293     BY(ASM_MESON_TAC[]);
2294   DISCH_THEN SUBST1_TAC;
2295   INTRO_TAC MCELL2_HL_LT_SQRT2 [`V`;`ul`];
2296   ANTS_TAC;
2297     BY(ASM_MESON_TAC[]);
2298   REPEAT WEAK_STRIP_TAC;
2299   INTRO_TAC MCELL2_SOL [`V`;`X`;`ul`;`hl (truncate_simplex 1 ul)`];
2300   ANTS_TAC;
2301     BY(ASM_MESON_TAC[]);
2302   DISCH_THEN SUBST1_TAC;
2303   TYPIFY `sol (EL 1 ul) X =  dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3) * (&1 - hl (truncate_simplex 1 ul) / sqrt (&2))` (C SUBGOAL_THEN MP_TAC);
2304     INTRO_TAC MCELL2_PERMUTE_01 [`V`;`ul`];
2305     ANTS_TAC;
2306       BY(ASM_MESON_TAC[]);
2307     REPEAT WEAK_STRIP_TAC;
2308     ASM_REWRITE_TAC[];
2309     INTRO_TAC MCELL2_SOL [`V`;`X`;`vl`;`hl (truncate_simplex 1 vl)`];
2310     ANTS_TAC;
2311       BY(ASM_MESON_TAC[]);
2312     ASM_REWRITE_TAC[];
2313     DISCH_THEN SUBST1_TAC;
2314     BY(MESON_TAC[Marchal_cells_2_new.DIHV_SYM]);
2315   DISCH_THEN SUBST1_TAC;
2316   INTRO_TAC MCELL2_DIHX [`V`;`X`;`ul`];
2317   ANTS_TAC;
2318     BY(ASM_MESON_TAC[]);
2319   DISCH_THEN SUBST1_TAC;
2320   REWRITE_TAC[arith `d * a - m * (d * a' + d * a') + m' * l * d = (a - &2 * m * a' + m' * l) * d`];
2321   MATCH_MP_TAC (arith `&0 <= c /\ a = b /\ c = d ==> (&0 <= d /\ a*c = b * d)`);
2322   CONJ_TAC;
2323     BY(REWRITE_TAC[DIHV_RANGE]);
2324   COMMENT "show non-degeneracy";
2325   INTRO_TAC NOT_COPLANAR_EXTREME_MCELL2 [`V`;`ul`];
2326   ASM_REWRITE_TAC[];
2327   ANTS_TAC;
2328     BY(ASM_MESON_TAC[IN]);
2329   DISCH_TAC;
2330   TYPIFY `~collinear {EL 0 ul,EL 1 ul,mxi V ul} /\ ~collinear {EL 0 ul, EL 1 ul,omega_list_n V ul 3}` ((C SUBGOAL_THEN ASSUME_TAC));
2331     TYPIFY `!a b c (d:real^3). {a,b,c,d} = {a,b,d,c}` ((C SUBGOAL_THEN MP_TAC));
2332       BY(SET_TAC[]);
2333     BY(ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);
2334   CONJ2_TAC;
2335     INTRO_TAC Merge_ineq.DIHV_EQ_DIH_Y [`EL 0 ul`;`EL 1 ul`;`mxi V ul`;`omega_list_n V ul 3`];
2336     ANTS_TAC;
2337       BY(ASM_MESON_TAC[]);
2338     BY(REWRITE_TAC[LET_DEF;LET_END_DEF]);
2339   TYPED_ABBREV_TAC  `(h:real) = hl (truncate_simplex 1 ul)` ;
2340   TYPIFY `dist(EL 0 ul,EL 1 ul)  = &2 * hl (truncate_simplex 1 ul) ` (C SUBGOAL_THEN ASSUME_TAC);
2341     ONCE_REWRITE_TAC[arith `(x = &2 * h <=> x / &2 = h)`];
2342     GMATCH_SIMP_TAC BARV3_TRUNC1;
2343     CONJ_TAC;
2344       BY(ASM_MESON_TAC[IN]);
2345     REWRITE_TAC[Marchal_cells_3.HL_2];
2346     BY(REAL_ARITH_TAC);
2347   ASM_REWRITE_TAC[];
2348   REWRITE_TAC[gamma2_x_div_azim_v2];
2349   COMMENT "simplify polynomial identity";
2350   TYPIFY `&0 < h` (C SUBGOAL_THEN ASSUME_TAC);
2351     EXPAND_TAC "h";
2352     MATCH_MP_TAC Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT;
2353     BY(ASM_MESON_TAC[]);
2354   TYPIFY `[EL 0 ul; EL 1 ul] = truncate_simplex 1 ul` (C SUBGOAL_THEN SUBST1_TAC);
2355     BY(ASM_MESON_TAC[BARV3_TRUNC1;IN]);
2356   TYPIFY `sqrt((&2 * h) * (&2 * h)) = &2 * h` (C SUBGOAL_THEN SUBST1_TAC);
2357     GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2358     BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
2359   MATCH_MP_TAC (arith `(a = a') /\ (b = b') /\ (c = c') ==> a - b + c = a' - (b' - c')`);
2360   CONJ_TAC;
2361     BY(REAL_ARITH_TAC);
2362   CONJ2_TAC;
2363     AP_TERM_TAC;
2364     ASM_REWRITE_TAC[];
2365     INTRO_TAC Merge_ineq.lmfun_h0cut [`(&2 * h)`];
2366     REWRITE_TAC[arith `(&2 * h) / &2 = h`];
2367     BY(REAL_ARITH_TAC);
2368   AP_TERM_TAC;
2369   AP_TERM_TAC;
2370   AP_TERM_TAC;
2371   REWRITE_TAC[Nonlinear_lemma.sqrt8_sqrt2;Sphere.sqrt2];
2372   Calc_derivative.CALC_ID_TAC;
2373   REPEAT (GMATCH_SIMP_TAC SQRT_EQ_0);
2374   BY(REAL_ARITH_TAC)
2375   ]);;
2376   (* }}} *)
2377
2378
2379
2380
2381
2382 let TSKAJXY_2 = prove_by_refinement(
2383   `!V X ul.
2384     pack_nonlinear_non_ox3q1h /\   saturated V /\
2385           packing V /\
2386     barV V 3 ul /\
2387     X = mcell2 V ul
2388           ==> gammaX V X lmfun >= &0`,
2389   (* {{{ proof *)
2390   [
2391   REPEAT WEAK_STRIP_TAC;
2392   TYPIFY `NULLSET X` ASM_CASES_TAC;
2393     INTRO_TAC GAMMAX_NULLSET [`V`;`lmfun`;`X`;`ul`;`2`];
2394     ANTS_TAC;
2395       BY(ASM_MESON_TAC[Bump.MCELL2]);
2396     BY(REAL_ARITH_TAC);
2397   INTRO_TAC GAMMAX_GAMMA2_X [`V`;`X`;`ul`;`dist(EL 0 ul,EL 1 ul)`;`dist(EL 0 ul,mxi V ul)`;`dist(EL 0 ul,omega_list_n V ul 3)`;`dist(mxi V ul,omega_list_n V ul 3)`;`dist(EL 1 ul,omega_list_n V ul 3)`;`dist(EL 1 ul,mxi V ul)`];
2398   ASM_REWRITE_TAC[];
2399   REPEAT WEAK_STRIP_TAC;
2400   ASM_REWRITE_TAC[];
2401   REWRITE_TAC[arith `a * b >= &0 <=> &0 <= a * b`];
2402   GMATCH_SIMP_TAC REAL_LE_MUL;
2403   ASM_REWRITE_TAC[];
2404   TYPIFY ` (!y. &2 <= y /\ y <= sqrt8 ==> &0 <= gamma2_x_div_azim_v2 (h0cut y) (y * y))` (C SUBGOAL_THEN ASSUME_TAC);
2405     MATCH_MP_TAC Merge_ineq.GRKIBMP;
2406     INTRO_TAC (Merge_ineq.get_pack_nonlinear_non_ox3q1h "GRKIBMP A V2") [];
2407     INTRO_TAC (Merge_ineq.get_pack_nonlinear_non_ox3q1h "GRKIBMP B V2") [];
2408     BY(MESON_TAC[]);
2409   FIRST_X_ASSUM MATCH_MP_TAC;
2410   INTRO_TAC MCELL2_VX_PROPS [`V`;`X`;`ul`];
2411   ASM_REWRITE_TAC[];
2412   INTRO_TAC Bump.HDTFNFZ_ALT [`V`;`ul`;`2`;`X`];
2413   ANTS_TAC;
2414     BY(ASM_MESON_TAC[Bump.MCELL2]);
2415   ASM_REWRITE_TAC[];
2416   DISCH_THEN SUBST1_TAC;
2417   REPEAT WEAK_STRIP_TAC;
2418   TYPIFY `EL 0 ul IN V /\ EL 1 ul IN V` (C SUBGOAL_THEN ASSUME_TAC);
2419     BY(FIRST_X_ASSUM_ST `INTER` MP_TAC THEN SET_TAC[]);
2420   CONJ_TAC;
2421     FIRST_X_ASSUM_ST `packing` MP_TAC;
2422     REWRITE_TAC[Sphere.packing];
2423     DISCH_THEN MATCH_MP_TAC;
2424     BY(ASM_MESON_TAC[IN]);
2425   INTRO_TAC MCELL2_HL_LT_SQRT2 [`V`;`ul`];
2426   ANTS_TAC;
2427     BY(ASM_MESON_TAC[]);
2428   REWRITE_TAC[Nonlinear_lemma.sqrt8_sqrt2;Sphere.sqrt2];
2429   TYPIFY `dist(EL 0 ul,EL 1 ul)  = &2 * hl (truncate_simplex 1 ul) ` (C SUBGOAL_THEN ASSUME_TAC);
2430     ONCE_REWRITE_TAC[arith `(x = &2 * h <=> x / &2 = h)`];
2431     GMATCH_SIMP_TAC BARV3_TRUNC1;
2432     CONJ_TAC;
2433       BY(ASM_MESON_TAC[IN]);
2434     REWRITE_TAC[Marchal_cells_3.HL_2];
2435     BY(REAL_ARITH_TAC);
2436   ASM_REWRITE_TAC[];
2437   BY(REAL_ARITH_TAC)
2438   ]);;
2439   (* }}} *)
2440
2441 let tsk_required_ineq =
2442   let cell3_hyp = ["QZECFIC wt0";"QZECFIC wt0 corner";"QZECFIC wt0 sqrt8";
2443               "QZECFIC wt1";"QZECFIC wt2 A";"CIHTIUM";"CJFZZDW";] in
2444   let tsk = ["TSKAJXY-GXSABWC DIV"; "TSKAJXY-IYOUOBF sharp v2";
2445              "TSKAJXY-IYOUOBF sym";
2446    "TSKAJXY-RIBCYXU sharp"; "TSKAJXY-RIBCYXU sym"; "TSKAJXY-TADIAMB";
2447    "TSKAJXY-WKGUESB sym"; "TSKAJXY-XLLIPLS"; "TSKAJXY-delta_x4";
2448    "TSKAJXY-eulerA"] in
2449   let grk = ["GRKIBMP A V2";"GRKIBMP B V2"] in
2450     cell3_hyp @ tsk @ grk;;
2451
2452 let TSKAJXY = prove_by_refinement(
2453   `!V X.
2454     pack_nonlinear_non_ox3q1h /\
2455           saturated V /\
2456           packing V /\
2457           mcell_set V X /\
2458           critical_edgeX V X = {}
2459           ==> gammaX V X lmfun >= &0`,
2460   (* {{{ proof *)
2461   [
2462   REPEAT WEAK_STRIP_TAC;
2463   TYPIFY ` ~(?i ul. ul IN barV V 3 /\ (i = 1 \/ i = 2) /\ X = mcell i V ul)` ASM_CASES_TAC;
2464     INTRO_TAC Tskajxy_034.TSKAJXY_034 [];
2465     ANTS_TAC;
2466       EVERY (map (fun t -> INTRO_TAC (Merge_ineq.get_pack_nonlinear_non_ox3q1h t) []) tsk_required_ineq);
2467       REPEAT WEAK_STRIP_TAC THEN ASM_REWRITE_TAC[];
2468       CONJ_TAC;
2469         MATCH_MP_TAC Merge_ineq.GRKIBMP;
2470         BY(ASM_REWRITE_TAC[]);
2471       MATCH_MP_TAC Merge_ineq.cell3_from_ineq_thm;
2472       BY(ASM_REWRITE_TAC[]);
2473     REWRITE_TAC[Tskajxy_034.TSKAJXY_statement_special_case];
2474     DISCH_THEN MATCH_MP_TAC;
2475     BY(ASM_MESON_TAC[]);
2476   FIRST_X_ASSUM MP_TAC;
2477   REWRITE_TAC[];
2478   REPEAT WEAK_STRIP_TAC;
2479     ASM_REWRITE_TAC[GSYM Bump.MCELL1];
2480     MATCH_MP_TAC TSKAJXY_1;
2481     BY(ASM_MESON_TAC[IN]);
2482   ASM_REWRITE_TAC[GSYM Bump.MCELL2];
2483   MATCH_MP_TAC TSKAJXY_2;
2484   BY(ASM_MESON_TAC[IN])
2485  ]);;
2486   (* }}} *)
2487
2488 end;;
2489