text_formalization/packing/TSKAJXY_034.hl

   1 (* ========================================================================= *)
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   3 (*                                                                           *)
   4 (*      Author    : VU KHAC KY                                               *)
   5 (*      Book lemma: TSKAJXY                                                  *)
   6 (*      Chapter   : Packing (Clusters)                                       *)
   7 (*      Date: November 2013                                                  *)
   8 (*                                                                           *)
   9 (* ========================================================================= *)
  10
  11
  12 (*
  13
  14 This does the special cases of Lemma TSKAJXY for 0, 3, and 4-cells
  15
  16 *)
  17
  18 module Tskajxy_034 = struct
  19
  20 open Sphere;;
  21 open Euler_main_theorem;;
  22 open Pack_defs;;
  23 open Pack_concl;;
  24 open Pack1;;
  25 open Pack2;;
  26 open Packing3;;
  27 open Rogers;;
  28 open Vukhacky_tactics;;
  29 open Marchal_cells;;
  30 open Emnwuus;;
  31 (* open Marchal_cells_2;; *)
  32 open Marchal_cells_2_new;;
  33 open Urrphbz1;;
  34 open Lepjbdj;;
  35 open Hdtfnfz;;
  36 open Rvfxzbu;;
  37 open Sltstlo;;
  38 open Urrphbz2;;
  39 open Urrphbz3;;
  40 open Ynhyjit;;
  41 open Njiutiu;;
  42 open Tezffsk;;
  43 open Qzksykg;;
  44 open Ddzuphj;;
  45 open Ajripqn;;
  46 open Qzyzmjc;;
  47 open Upfzbzm_support_lemmas;;
  48 open Marchal_cells_3;;
  49 open Grutoti;;
  50 open Kizhltl;;
  51 open Sum_gammax_lmfun_estimate;;
  52 open Upfzbzm;;
  53 open Rdwkarc;;
  54 open Ineq;;
  55 open Merge_ineq;;
  56 open Hales_tactic;;
  57 open Tskajxy_lemmas;;
  58
  59 (* ======================================================================== *)
  60
  61 let cell3_from_ineq =
  62  `!y4 y5 y6.
  63          &2 <= y4 /\
  64          &2 <= y5 /\
  65          &2 <= y6 /\
  66          y4 <= &2 * sqrt (&2) /\
  67          y5 <= &2 * sqrt (&2) /\
  68          y6 <= &2 * sqrt (&2) /\
  69          eta_y y4 y5 y6 < sqrt (&2)
  70          ==> &0 <= gamma3f y4 y5 y6 sqrt2 lmfun`;;
  71
  72
  73 let GRKIBMP_concl =
  74   `!y. &2 <= y /\ y <= sqrt8 ==>
  75      &0 <= gamma2_x_div_azim_v2 (h0cut y) (y*y)`;;
  76
  77 let tsk_hyp_new = mk_conj(GRKIBMP_concl,
  78                               mk_conj(cell3_from_ineq,tsk_hyp));;
  79
  80 let TSKAJXY_statement_special_case = new_definition
  81    `TSKAJXY_statement_special_case <=>
  82       (!V X.
  83           saturated V /\
  84           packing V /\
  85           mcell_set V X /\
  86           ~(?i ul. ul IN barV V 3 /\ (i = 1 \/ i = 2) /\ X = mcell i V ul) /\
  87           critical_edgeX V X = {}
  88           ==> gammaX V X lmfun >= &0)`;;
  89
  90 g (mk_imp(tsk_hyp_new,`TSKAJXY_statement_special_case`));;
  91
  92 let TSKAJXY_034 = Prove_by_refinement.prove_by_refinement(
  93    (mk_imp(tsk_hyp_new,`TSKAJXY_statement_special_case`)),
  94   (* {{{ proof *)
  95   [
  96    (STRIP_TAC);
  97   (REWRITE_TAC[TSKAJXY_statement_special_case; mcell_set; IN_ELIM_THM]);
  98   (REWRITE_TAC[IN]);
  99   (REPEAT STRIP_TAC);
 100   (ASM_CASES_TAC `NULLSET X`);
 101     (REWRITE_TAC[gammaX]);
 102     (MATCH_MP_TAC (REAL_ARITH `x = &0 /\ y = &0 /\ z = &0 ==> x - y + z >= &0`));
 103     (REWRITE_TAC[total_solid; REAL_ENTIRE]);
 104     (REPEAT STRIP_TAC);
 105         (MATCH_MP_TAC MEASURE_EQ_0);
 106         BY((ASM_REWRITE_TAC[]));
 107       (DISJ2_TAC);
 108       (REWRITE_WITH `VX V X = {}`);
 109         (REWRITE_TAC[VX]);
 110         BY((ASM_REWRITE_TAC[]));
 111       BY((REWRITE_TAC[SUM_CLAUSES]));
 112     (DISJ2_TAC);
 113     (REWRITE_WITH `edgeX V X = {}`);
 114       (REWRITE_TAC[edgeX]);
 115       (REWRITE_WITH `VX V X = {}`);
 116         (REWRITE_TAC[VX]);
 117         BY((ASM_REWRITE_TAC[]));
 118       (ONCE_REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]);
 119       BY((SET_TAC[]));
 120     BY((REWRITE_TAC[SUM_CLAUSES]));
 121   (NEW_GOAL `~(X:real^3->bool = {})`);
 122     BY((STRIP_TAC THEN SWITCH_TAC THEN UP_ASM_TAC THEN REWRITE_TAC[ASSUME `X:real^3->bool = {}`; NEGLIGIBLE_EMPTY]));
 123   (ASM_CASES_TAC `i >= 4`);
 124     (NEW_GOAL `X = mcell4 V ul`);
 125       (ASM_REWRITE_TAC[]);
 126       BY((ASM_SIMP_TAC[MCELL_EXPLICIT]));
 127     (UP_ASM_TAC THEN REWRITE_TAC[mcell4]);
 128     (COND_CASES_TAC);
 129       (NEW_GOAL `?u0 u1 u2 u3. ul = [u0; u1; u2; u3:real^3]`);
 130         (MATCH_MP_TAC BARV_3_EXPLICIT);
 131         BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
 132       (UP_ASM_TAC THEN STRIP_TAC);
 133       (REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`; set_of_list]);
 134       (STRIP_TAC);
 135       (ABBREV_TAC `y1 = dist (u0:real^3, u1)`);
 136       (ABBREV_TAC `y2 = dist (u0:real^3, u2)`);
 137       (ABBREV_TAC `y3 = dist (u0:real^3, u3)`);
 138       (ABBREV_TAC `y4 = dist (u2:real^3, u3)`);
 139       (ABBREV_TAC `y5 = dist (u1:real^3, u3)`);
 140       (ABBREV_TAC `y6 = dist (u1:real^3, u2)`);
 141       (NEW_GOAL `VX V X = {u0,u1,u2,u3}`);
 142         (REWRITE_WITH `VX V X = V INTER X`);
 143           (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
 144           (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 145           BY((ASM_REWRITE_TAC[]));
 146         (REWRITE_WITH `X = mcell 4 V ul`);
 147           (ASM_REWRITE_TAC[]);
 148           BY((MESON_TAC[ARITH_RULE `4 >= 4`; ASSUME `i >= 4`; MCELL_EXPLICIT]));
 149         (REWRITE_WITH `V INTER mcell 4 V ul = set_of_list (truncate_simplex (4 - 1) ul)`);
 150           (MATCH_MP_TAC Lepjbdj.LEPJBDJ);
 151           (ASM_REWRITE_TAC[ARITH_RULE `1 <= 4 /\ 4 <= 4`]);
 152           (REWRITE_WITH ` mcell 4 V [u0; u1; u2; u3] = X`);
 153             (ASM_REWRITE_TAC[]);
 154             BY((MESON_TAC[ARITH_RULE `4 >= 4`; ASSUME `i >= 4`; MCELL_EXPLICIT]));
 155           BY((ASM_REWRITE_TAC[]));
 156         BY((ASM_REWRITE_TAC[ARITH_RULE `4 - 1 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3; set_of_list]));
 157       (REWRITE_WITH `vol X = vol_y y1 y2 y3 y4 y5 y6 /\ gammaX V X lmfun = gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun`);
 158         (MATCH_MP_TAC gammaX_gamm4fgcy);
 159         (EXISTS_TAC `ul:(real^3)list`);
 160         (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
 161         (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
 162         (EXISTS_TAC `i:num`);
 163         BY((ASM_REWRITE_TAC[]));
 164       (NEW_GOAL `!y1 y2 y3 y4 y5 y6. ineq [#2.0,y1,sqrt8; #2.0,y2,sqrt8; #2.0,y3,sqrt8; #2.0,y4,sqrt8; #2.0, y5, sqrt8; #2.0,y6,sqrt8] (~critical_edge_y y1 /\ ~critical_edge_y y2 /\ ~critical_edge_y y3 /\ ~critical_edge_y y4 /\ ~critical_edge_y y5 /\ ~critical_edge_y y6 /\ &0 < delta_y y1 y2 y3 y4 y5 y6 /\ rad2_y y1 y2 y3 y4 y5 y6 < &2 ==> gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun >= &0)`);
 165         (MATCH_MP_TAC TSKAJXY_DERIVED4);
 166         BY((ASM_REWRITE_TAC[]));
 167       (UP_ASM_TAC THEN REWRITE_TAC[ineq; MESON[] `a ==> b ==> c <=> (a /\ b) ==> c`] THEN STRIP_TAC);
 168       (FIRST_ASSUM MATCH_MP_TAC);
 169       (ASM_REWRITE_TAC[]);
 170       (NEW_GOAL `~(critical_edge_y y1) /\ ~(critical_edge_y y2) /\ ~(critical_edge_y y3) /\ ~(critical_edge_y y4) /\ ~(critical_edge_y y5) /\ ~(critical_edge_y y6) /\ &0 < delta_y y1 y2 y3 y4 y5 y6`);
 171         (REWRITE_TAC[critical_edge_y]);
 172         (REPEAT STRIP_TAC);
 173                     (NEW_GOAL `{u0:real^3, u1} IN critical_edgeX V X`);
 174                       (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
 175                       (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
 176                       (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
 177                       (REPEAT STRIP_TAC);
 178                           (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
 179                           (ASM_REWRITE_TAC[]);
 180                           (STRIP_TAC);
 181                             BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
 182                           (STRIP_TAC);
 183                             BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
 184                           (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y1`);
 185                           (EXPAND_TAC "y1" THEN REWRITE_TAC[dist; ASSUME `u0:real^3 = u1`; NORM_ARITH `norm (u1 - u1) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);
 186                           BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
 187                         BY((ASM_REAL_ARITH_TAC));
 188                       BY((ASM_REAL_ARITH_TAC));
 189                     BY((ASM_SET_TAC[]));
 190                   (NEW_GOAL `{u0:real^3, u2} IN critical_edgeX V X`);
 191                     (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
 192                     (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u2:real^3`);
 193                     (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
 194                     (REPEAT STRIP_TAC);
 195                         (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u2:real^3`);
 196                         (ASM_REWRITE_TAC[]);
 197                         (STRIP_TAC);
 198                           BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
 199                         (STRIP_TAC);
 200                           BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
 201                         (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y2`);
 202                         (EXPAND_TAC "y2" THEN REWRITE_TAC[dist; ASSUME `u0:real^3 = u2`; NORM_ARITH `norm (u2 - u2) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);
 203                         BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
 204                       BY((ASM_REAL_ARITH_TAC));
 205                     BY((ASM_REAL_ARITH_TAC));
 206                   BY((ASM_SET_TAC[]));
 207                 (NEW_GOAL `{u0:real^3, u3} IN critical_edgeX V X`);
 208                   (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
 209                   (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u3:real^3`);
 210                   (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
 211                   (REPEAT STRIP_TAC);
 212                       (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u3:real^3`);
 213                       (ASM_REWRITE_TAC[]);
 214                       (STRIP_TAC);
 215                         BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
 216                       (STRIP_TAC);
 217                         BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
 218                       (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y3`);
 219                       (EXPAND_TAC "y3" THEN REWRITE_TAC[dist; ASSUME `u0:real^3 = u3`; NORM_ARITH `norm (u3 - u3) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);
 220                       BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
 221                     BY((ASM_REAL_ARITH_TAC));
 222                   BY((ASM_REAL_ARITH_TAC));
 223                 BY((ASM_SET_TAC[]));
 224               (NEW_GOAL `{u2:real^3, u3} IN critical_edgeX V X`);
 225                 (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
 226                 (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
 227                 (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
 228                 (REPEAT STRIP_TAC);
 229                     (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
 230                     (ASM_REWRITE_TAC[]);
 231                     (STRIP_TAC);
 232                       BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
 233                     (STRIP_TAC);
 234                       BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
 235                     (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y4`);
 236                     (EXPAND_TAC "y4" THEN REWRITE_TAC[dist; ASSUME `u2:real^3 = u3`; NORM_ARITH `norm (u3 - u3) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);
 237                     BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
 238                   BY((ASM_REAL_ARITH_TAC));
 239                 BY((ASM_REAL_ARITH_TAC));
 240               BY((ASM_SET_TAC[]));
 241             (NEW_GOAL `{u1:real^3, u3} IN critical_edgeX V X`);
 242               (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
 243               (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u3:real^3`);
 244               (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
 245               (REPEAT STRIP_TAC);
 246                   (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u3:real^3`);
 247                   (ASM_REWRITE_TAC[]);
 248                   (STRIP_TAC);
 249                     BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
 250                   (STRIP_TAC);
 251                     BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
 252                   (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y5`);
 253                   (EXPAND_TAC "y5" THEN REWRITE_TAC[dist; ASSUME `u1:real^3 = u3`; NORM_ARITH `norm (u3 - u3) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);
 254                   BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
 255                 BY((ASM_REAL_ARITH_TAC));
 256               BY((ASM_REAL_ARITH_TAC));
 257             BY((ASM_SET_TAC[]));
 258           (NEW_GOAL `{u1:real^3, u2} IN critical_edgeX V X`);
 259             (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
 260             (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3`);
 261             (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
 262             (REPEAT STRIP_TAC);
 263                 (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3`);
 264                 (ASM_REWRITE_TAC[]);
 265                 (STRIP_TAC);
 266                   BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
 267                 (STRIP_TAC);
 268                   BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
 269                 (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y6`);
 270                 (EXPAND_TAC "y6" THEN REWRITE_TAC[dist; ASSUME `u1:real^3 = u2`; NORM_ARITH `norm (u2 - u2) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);
 271                 BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
 272               BY((ASM_REAL_ARITH_TAC));
 273             BY((ASM_REAL_ARITH_TAC));
 274           BY((ASM_SET_TAC[]));
 275         (REWRITE_WITH `&0 < delta_y y1 y2 y3 y4 y5 y6 <=> &0 < sqrt (delta_y y1 y2 y3 y4 y5 y6)`);
 276           (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 277           (MATCH_MP_TAC SQRT_LT_0);
 278           (REWRITE_TAC[delta_y]);
 279           (ABBREV_TAC `x1 = y1 * y1` THEN ABBREV_TAC `x2 = y2 * y2`);
 280           (ABBREV_TAC `x3 = y3 * y3` THEN ABBREV_TAC `x4 = y4 * y4`);
 281           (ABBREV_TAC `x5 = y5 * y5` THEN ABBREV_TAC `x6 = y6 * y6`);
 282           (REWRITE_WITH `delta_x x1 x2 x3 x4 x5 x6 = (let a = u1:real^3 - u0 in let b = u2 - u0 in let c = u3 - u0 in &4 * (a$1 * b$2 * c$3 - a$1 * b$3 * c$2 - a$2 * b$1 * c$3 + a$2 * b$3 * c$1 + a$3 * b$1 * c$2 - a$3 * b$2 * c$1) pow 2)`);
 283             (MATCH_MP_TAC Delta_x.COMPUTE_DELTA_X);
 284             (REWRITE_TAC[xlist; ylist]);
 285             (REPEAT LET_TAC);
 286             (EXPAND_TAC "x1" THEN EXPAND_TAC "x2" THEN EXPAND_TAC "x3");
 287             (EXPAND_TAC "x4" THEN EXPAND_TAC "x5" THEN EXPAND_TAC "x6");
 288             (UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ; GSYM REAL_POW_2]);
 289             (ASM_REWRITE_TAC[]);
 290             (STRIP_TAC);
 291             BY((ASM_REWRITE_TAC[]));
 292           (REPEAT LET_TAC);
 293           (REWRITE_TAC[REAL_ARITH `&0 <= &4 * a <=> &0 <= a`]);
 294           BY((REWRITE_TAC[Real_ext.REAL_LE_POW_2]));
 295         (ONCE_REWRITE_TAC[REAL_ARITH `&0 < a <=> &0 < a / &12`]);
 296         (REWRITE_WITH `sqrt (delta_y y1 y2 y3 y4 y5 y6) / &12 = vol (convex hull {u0,u1,u2,u3})`);
 297           (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 298           (REWRITE_TAC[delta_y; GSYM REAL_POW_2]);
 299           (EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");
 300           (EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6");
 301           BY((REWRITE_TAC[VOLUME_OF_CLOSED_TETRAHEDRON]));
 302         (REWRITE_TAC[GSYM (ASSUME `X = convex hull {u0, u1, u2, u3:real^3}`)]);
 303         (REWRITE_WITH `&0 < vol X <=> ~NULLSET X`);
 304           (MATCH_MP_TAC MEASURABLE_MEASURE_POS_LT);
 305           (REWRITE_TAC[ASSUME `X = convex hull {u0, u1, u2, u3:real^3}`]);
 306           (MATCH_MP_TAC MEASURABLE_CONVEX_HULL);
 307           (MATCH_MP_TAC FINITE_IMP_BOUNDED);
 308           BY((REWRITE_TAC[Geomdetail.FINITE6]));
 309         BY((ASM_REWRITE_TAC[]));
 310       (ASM_REWRITE_TAC[]);
 311       (NEW_GOAL `!u v. {u,v} IN edgeX V X ==> (#2.0 <= dist (u,v) /\ dist(u,v) <= sqrt8)`);
 312         (REPEAT GEN_TAC);
 313         (REWRITE_TAC[edgeX; IN]);
 314         (REWRITE_TAC[MESON[IN] `VX V X x <=> x IN VX V X`]);
 315         (ASM_REWRITE_TAC[IN_ELIM_THM]);
 316         (STRIP_TAC);
 317         (MP_TAC (ASSUME `packing V`));
 318         (REWRITE_TAC[packing; REAL_ARITH `#2.0 = &2`] THEN STRIP_TAC);
 319         (STRIP_TAC);
 320           (FIRST_ASSUM MATCH_MP_TAC);
 321           (NEW_GOAL `u:real^3 IN {u0,u1,u2,u3} /\ v IN {u0,u1,u2,u3}`);
 322             (DEL_TAC THEN UP_ASM_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);
 323             BY((SET_TAC[]));
 324           (NEW_GOAL `{u0,u1,u2,u3:real^3} SUBSET V`);
 325             (REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
 326             (MATCH_MP_TAC BARV_SUBSET);
 327             BY((EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]));
 328           (STRIP_TAC);
 329             (REWRITE_TAC[MESON[IN] `(V:real^3->bool) x <=> x IN V`]);
 330             BY((UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]));
 331           (STRIP_TAC);
 332             (REWRITE_TAC[MESON[IN] `(V:real^3->bool) x <=> x IN V`]);
 333             BY((UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]));
 334           (DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);
 335           BY((SET_TAC[]));
 336         (ABBREV_TAC `s = circumcenter {u0,u1,u2,u3:real^3}`);
 337         (NEW_GOAL `dist (u,v:real^3) <= dist (s,u) + dist (s, v)`);
 338           BY((NORM_ARITH_TAC));
 339         (NEW_GOAL `!w. w IN {u0,u1,u2,u3:real^3} ==> radV {u0,u1,u2,u3:real^3} = dist (circumcenter {u0,u1,u2,u3:real^3},w)`);
 340           (MATCH_MP_TAC Rogers.OAPVION2);
 341           (REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
 342           (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);
 343           BY((EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]));
 344         (NEW_GOAL `dist (s,u) + dist (s,v:real^3) <= sqrt8`);
 345           (REWRITE_TAC[Nonlinear_lemma.sqrt8_sqrt2; sqrt2]);
 346           (MATCH_MP_TAC (REAL_ARITH `a < x /\ b < x ==> a + b <= &2 * x`));
 347           (STRIP_TAC);
 348             (REWRITE_WITH `dist (s,u:real^3) = radV {u0,u1,u2,u3:real^3}`);
 349               (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 350               (EXPAND_TAC "s");
 351               (FIRST_ASSUM MATCH_MP_TAC);
 352               (DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN DEL_TAC);
 353               (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);
 354               BY((SET_TAC[]));
 355             (REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
 356             (REWRITE_TAC[GSYM HL]);
 357             BY((ASM_REWRITE_TAC[]));
 358           (REWRITE_WITH `dist (s,v:real^3) = radV {u0,u1,u2,u3:real^3}`);
 359             (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 360             (EXPAND_TAC "s");
 361             (FIRST_ASSUM MATCH_MP_TAC);
 362             (DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN DEL_TAC);
 363             (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);
 364             BY((SET_TAC[]));
 365           (REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
 366           (REWRITE_TAC[GSYM HL]);
 367           BY((ASM_REWRITE_TAC[]));
 368         BY((ASM_REAL_ARITH_TAC));
 369       (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`);
 370         (REWRITE_TAC[ARITH_RULE `4 = 3 + 1`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
 371         (MATCH_MP_TAC Marchal_cells_3.BARV_CARD_LEMMA);
 372         BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
 373       (NEW_GOAL `~(u0 = u1:real^3) /\ ~(u0 = u2) /\ ~(u0 = u3) /\ ~(u1 = u2) /\ ~(u1 = u3) /\ ~(u2 = u3)`);
 374         (REPEAT STRIP_TAC);
 375                   (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
 376                     BY((REWRITE_TAC[ASSUME `u0 = u1:real^3`; SET_RULE `{u1, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
 377                   BY((ASM_ARITH_TAC));
 378                 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
 379                   BY((REWRITE_TAC[ASSUME `u0 = u2:real^3`; SET_RULE `{u2, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
 380                 BY((ASM_ARITH_TAC));
 381               (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
 382                 BY((REWRITE_TAC[ASSUME `u0 = u3:real^3`; SET_RULE `{u3, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
 383               BY((ASM_ARITH_TAC));
 384             (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
 385               BY((REWRITE_TAC[ASSUME `u1 = u2:real^3`; SET_RULE `{u0, u2, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ]));
 386             BY((ASM_ARITH_TAC));
 387           (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
 388             BY((REWRITE_TAC[ASSUME `u1 = u3:real^3`; SET_RULE `{u0, u3, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ]));
 389           BY((ASM_ARITH_TAC));
 390         (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
 391           BY((REWRITE_TAC[ASSUME `u2 = u3:real^3`; SET_RULE `{u0, u1, u3, u3} = {u0,u1,u3}`;Geomdetail.CARD3 ]));
 392         BY((ASM_ARITH_TAC));
 393       (NEW_GOAL `edgeX V X = {{u0,u1:real^3}, {u0,u2}, {u0,u3}, {u1,u2}, {u1,u3}, {u2,u3}}`);
 394         (REWRITE_TAC[edgeX]);
 395         (ONCE_REWRITE_TAC[SET_EQ_LEMMA]);
 396         (REWRITE_TAC[IN_ELIM_THM]);
 397         (REPEAT STRIP_TAC);
 398           (UNDISCH_TAC `VX V X u` THEN UNDISCH_TAC `VX V X v`);
 399           (REWRITE_TAC[MESON[IN] `VX V X s <=> s IN VX V X`]);
 400           (ASM_REWRITE_TAC[SET_RULE `v IN {u0, u1, u2, u3} <=> v = u0 \/ v = u1 \/ v = u2 \/ v = u3`]);
 401           (REPEAT STRIP_TAC);
 402                                         (NEW_GOAL `F`);
 403                                           BY((ASM_MESON_TAC[]));
 404                                         BY((ASM_MESON_TAC[]));
 405                                       (REWRITE_WITH `{u,v} = {v,u:real^3}`);
 406                                         BY((SET_TAC[]));
 407                                       BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 408                                     (REWRITE_WITH `{u,v} = {v,u:real^3}`);
 409                                       BY((SET_TAC[]));
 410                                     BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 411                                   (REWRITE_WITH `{u,v} = {v,u:real^3}`);
 412                                     BY((SET_TAC[]));
 413                                   BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 414                                 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 415                               (NEW_GOAL `F`);
 416                                 BY((ASM_MESON_TAC[]));
 417                               BY((ASM_MESON_TAC[]));
 418                             (REWRITE_WITH `{u,v} = {v,u:real^3}`);
 419                               BY((SET_TAC[]));
 420                             BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 421                           (REWRITE_WITH `{u,v} = {v,u:real^3}`);
 422                             BY((SET_TAC[]));
 423                           BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 424                         BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 425                       BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 426                     (NEW_GOAL `F`);
 427                       BY((ASM_MESON_TAC[]));
 428                     BY((ASM_MESON_TAC[]));
 429                   (REWRITE_WITH `{u,v} = {v,u:real^3}`);
 430                     BY((SET_TAC[]));
 431                   BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 432                 BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 433               BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 434             BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 435           (NEW_GOAL `F`);
 436             BY((ASM_MESON_TAC[]));
 437           BY((ASM_MESON_TAC[]));
 438         (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE `x IN {a,b,c,d,e,f} <=> x = a \/ x = b \/ x = c \/ x = d \/ x = e \/ x = f`]);
 439         (REWRITE_TAC[MESON[IN] `VX V X s <=> s IN VX V X`]);
 440         (ASM_REWRITE_TAC[SET_RULE `v IN {u0, u1, u2, u3} <=> v = u0 \/ v = u1 \/ v = u2 \/ v = u3`]);
 441         (REPEAT STRIP_TAC);
 442                   BY((EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]));
 443                 BY((EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u2:real^3` THEN ASM_REWRITE_TAC[]));
 444               BY((EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[]));
 445             BY((EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN ASM_REWRITE_TAC[]));
 446           BY((EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[]));
 447         BY((EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[]));
 448       (STRIP_TAC);
 449         (EXPAND_TAC "y1");
 450         (FIRST_ASSUM MATCH_MP_TAC);
 451         BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 452       (STRIP_TAC);
 453         (EXPAND_TAC "y2");
 454         (FIRST_ASSUM MATCH_MP_TAC);
 455         BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 456       (STRIP_TAC);
 457         (EXPAND_TAC "y3");
 458         (FIRST_ASSUM MATCH_MP_TAC);
 459         BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 460       (STRIP_TAC);
 461         (EXPAND_TAC "y4");
 462         (FIRST_ASSUM MATCH_MP_TAC);
 463         BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 464       (STRIP_TAC);
 465         (EXPAND_TAC "y5");
 466         (FIRST_ASSUM MATCH_MP_TAC);
 467         BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 468       (STRIP_TAC);
 469         (EXPAND_TAC "y6");
 470         (FIRST_ASSUM MATCH_MP_TAC);
 471         BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
 472       (REWRITE_WITH `rad2_y y1 y2 y3 y4 y5 y6 = radV {u0,u1,u2,u3:real^3} pow 2`);
 473         (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 474         (REWRITE_TAC[rad2_y; y_of_x]);
 475         (GMATCH_SIMP_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] Merge_ineq.GDRQXLGv2));
 476         (STRIP_TAC);
 477           (STRIP_TAC);
 478             (REWRITE_TAC[ARITH_RULE `4 = 3 + 1`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
 479             (MATCH_MP_TAC Marchal_cells_3.BARV_CARD_LEMMA);
 480             BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
 481           (REWRITE_TAC[Collect_geom.coplanar_alt]);
 482           (REWRITE_TAC[GSYM Trigonometry2.coplanar1]);
 483           (REWRITE_TAC[coplanar] THEN STRIP_TAC);
 484           (NEW_GOAL `affine hull {u0, u1, u2, u3:real^3} SUBSET affine hull (affine hull {u, v, w})`);
 485             BY((ASM_SIMP_TAC[Marchal_cells_2_new.AFFINE_SUBSET_KY_LEMMA]));
 486           (UP_ASM_TAC THEN REWRITE_WITH `affine hull (affine hull {u, v, w}) = affine hull {u:real^3, v, w}`);
 487             BY((REWRITE_TAC[AFFINE_HULL_EQ; AFFINE_AFFINE_HULL]));
 488           (STRIP_TAC);
 489           (NEW_GOAL `NULLSET X`);
 490             (MATCH_MP_TAC NEGLIGIBLE_SUBSET);
 491             (EXISTS_TAC `affine hull {u0, u1, u2, u3:real^3}`);
 492             (STRIP_TAC);
 493               (MATCH_MP_TAC NEGLIGIBLE_SUBSET);
 494               (EXISTS_TAC `affine hull {u,v,w:real^3}`);
 495               (REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]);
 496               BY((ASM_REWRITE_TAC[]));
 497             (REWRITE_TAC[ASSUME `X = mcell i V ul`]);
 498             (REWRITE_WITH `mcell i V ul = mcell4 V ul`);
 499               BY((MESON_TAC[ARITH_RULE `4 >= 4`; MCELL_EXPLICIT; ASSUME `i >= 4`]));
 500             (REWRITE_TAC[mcell4]);
 501             (COND_CASES_TAC);
 502               BY((ASM_REWRITE_TAC[set_of_list; CONVEX_HULL_SUBSET_AFFINE_HULL]));
 503             BY((SET_TAC[]));
 504           BY((UP_ASM_TAC THEN ASM_REWRITE_TAC[]));
 505         (REWRITE_TAC[GSYM REAL_POW_2]);
 506         (EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");
 507         (EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6");
 508         BY((REWRITE_TAC[]));
 509       (REWRITE_WITH `radV {u0, u1, u2, u3:real^3} = hl (ul:(real^3)list)`);
 510         BY((ASM_REWRITE_TAC[HL;set_of_list]));
 511       (REWRITE_WITH `hl (ul:(real^3)list) pow 2 < &2 <=> sqrt (hl ul pow 2) < sqrt (&2)`);
 512         (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 513         (MATCH_MP_TAC Real_ext.REAL_PROP_LT_SQRT);
 514         BY((REWRITE_TAC[REAL_LE_POW_2] THEN REAL_ARITH_TAC));
 515       (REWRITE_WITH `sqrt (hl (ul:(real^3)list) pow 2) = hl ul`);
 516         (MATCH_MP_TAC POW_2_SQRT);
 517         (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
 518         (NEW_GOAL `hl (truncate_simplex 1 ul) <= hl (ul:(real^3)list)`);
 519           (MATCH_MP_TAC Rogers.HL_DECREASE);
 520           (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3`);
 521           BY((ASM_REWRITE_TAC[IN; ARITH_RULE `1 <= 3`]));
 522         (NEW_GOAL `&0 < hl (truncate_simplex 1 (ul:(real^3)list))`);
 523           (MATCH_MP_TAC Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT);
 524           BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
 525         BY((ASM_REAL_ARITH_TAC));
 526       BY((ASM_REWRITE_TAC[]));
 527     (STRIP_TAC);
 528     (NEW_GOAL `F`);
 529       BY((UP_ASM_TAC THEN ASM_REWRITE_TAC[]));
 530     BY((UP_ASM_TAC THEN ASM_REWRITE_TAC[]));
 531   (COMMENT "END OF 4-CELL CASE");
 532   (ASM_CASES_TAC `i = 0`);
 533     (NEW_GOAL `VX V X = {}`);
 534       (REWRITE_WITH `VX V X = V INTER X`);
 535         (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
 536         (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 537         BY((ASM_REWRITE_TAC[]));
 538       (ASM_REWRITE_TAC[]);
 539       (MATCH_MP_TAC Lepjbdj.LEPJBDJ_0);
 540       BY((ASM_REWRITE_TAC[]));
 541     (NEW_GOAL `edgeX V X = {}`);
 542       (REWRITE_TAC[edgeX]);
 543       (ASM_REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`; SET_RULE `x IN {} <=> F`]);
 544       BY((SET_TAC[]));
 545     (REWRITE_TAC[gammaX]);
 546     (MATCH_MP_TAC (REAL_ARITH `b = &0 /\ c = &0 /\ &0 <= a ==> a - b + c >= &0`));
 547     (REPEAT STRIP_TAC);
 548         BY((ASM_REWRITE_TAC[total_solid; SUM_CLAUSES] THEN REAL_ARITH_TAC));
 549       BY((ASM_REWRITE_TAC[SUM_CLAUSES] THEN REAL_ARITH_TAC));
 550     (MATCH_MP_TAC MEASURE_POS_LE);
 551     (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC Urrphbz1.MEASURABLE_MCELL);
 552     BY((ASM_REWRITE_TAC[]));
 553   COMMENT "insert. thales. Jan 2013";
 554   FIRST_X_ASSUM_ST `gamma3f` MP_TAC;
 555   REPEAT (FIRST_X_ASSUM_ST `ineq` kill);
 556   DISCH_TAC;
 557   TYPIFY `i = 3` (C SUBGOAL_THEN ASSUME_TAC);
 558     MATCH_MP_TAC (arith `~(i >= 4) /\ ~(i=0) /\ ~((i=1) \/ (i=2))   ==> (i = 3)`);
 559     REPLICATE_TAC 9 (FIRST_X_ASSUM MP_TAC);
 560     REPEAT (FIRST_X_ASSUM kill);
 561     BY(MESON_TAC[]);
 562   REPEAT (FIRST_X_ASSUM_ST `gamma4fgcy` kill);
 563   COMMENT "end of insert";
 564   (NEW_GOAL `X = mcell3 V ul`);
 565     (ASM_REWRITE_TAC[]);
 566     BY((ASM_SIMP_TAC[MCELL_EXPLICIT]));
 567   (UP_ASM_TAC THEN REWRITE_TAC[mcell3]);
 568   (COND_CASES_TAC);
 569     (STRIP_TAC);
 570     (NEW_GOAL `?u0 u1 u2 u3. ul = [u0; u1; u2; u3:real^3]`);
 571       (MATCH_MP_TAC BARV_3_EXPLICIT);
 572       BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
 573     (UP_ASM_TAC THEN STRIP_TAC);
 574     (NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\ dist (u0,s) = sqrt (&2) /\ mxi V ul = s)`);
 575       (MATCH_MP_TAC MXI_EXPLICIT);
 576       (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
 577       BY((ASM_REWRITE_TAC[]));
 578     (UP_ASM_TAC THEN STRIP_TAC);
 579     (ABBREV_TAC `s2 = omega_list_n V ul 2`);
 580     (ABBREV_TAC `s3 = omega_list_n V ul 3`);
 581     (ABBREV_TAC `vl = truncate_simplex 2 (ul:(real^3)list)`);
 582     (NEW_GOAL `s2 IN voronoi_list V vl`);
 583       (EXPAND_TAC "s2" THEN EXPAND_TAC "vl");
 584       (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 585       (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 586       BY((ARITH_TAC));
 587     (NEW_GOAL `s3 IN voronoi_list V vl`);
 588       (EXPAND_TAC "s3" THEN EXPAND_TAC "vl");
 589       (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
 590       (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 591       BY((ARITH_TAC));
 592     (NEW_GOAL `s IN voronoi_list V vl`);
 593       (MATCH_MP_TAC (SET_RULE `(?x. s IN x /\ x SUBSET t)==> s IN t`));
 594       (EXISTS_TAC `convex hull {s2,s3:real^3}`);
 595       (STRIP_TAC);
 596         BY((ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]));
 597       (NEW_GOAL `voronoi_list V vl = convex hull (voronoi_list V vl)`);
 598         (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 599         BY((REWRITE_TAC[CONVEX_HULL_EQ; Packing3.CONVEX_VORONOI_LIST]));
 600       (ONCE_REWRITE_TAC[ASSUME `voronoi_list V vl = convex hull voronoi_list V vl`]);
 601       (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 602       BY((ASM_SET_TAC[]));
 603     (MP_TAC (ASSUME `s IN voronoi_list V vl`));
 604     (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; VORONOI_LIST; VORONOI_SET; set_of_list; SET_RULE `x IN {a,b,c} <=> x=a\/x=b\/x=c`; IN_INTERS]);
 605     (STRIP_TAC);
 606     (NEW_GOAL `s IN voronoi_closed V u0 /\ s IN voronoi_closed V u1 /\ s IN voronoi_closed V (u2:real^3)`);
 607       BY((UP_ASM_TAC THEN SET_TAC[]));
 608     (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM] THEN STRIP_TAC);
 609     (NEW_GOAL `u0 IN V /\ u1 IN V /\ u2 IN V /\ (u3:real^3) IN V`);
 610       (REWRITE_TAC[SET_RULE `u0 IN V /\ u1 IN V /\ u2 IN V /\ (u3:real^3) IN V <=> {u0,u1,u2,u3} SUBSET V`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
 611       (MATCH_MP_TAC BARV_SUBSET);
 612       BY((EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]));
 613     (FIRST_ASSUM MP_TAC THEN REWRITE_TAC[IN] THEN STRIP_TAC);
 614     (NEW_GOAL `dist (s,u1:real^3) = sqrt(&2)`);
 615       (REWRITE_TAC[GSYM (ASSUME `dist (u0:real^3, s) = sqrt (&2)`)]);
 616       (REWRITE_WITH `dist (u0,s:real^3) = dist (s,u0)`);
 617         BY((NORM_ARITH_TAC));
 618       (REWRITE_TAC[REAL_ARITH `a = b <=> a <= b /\ b <= a`]);
 619       BY((ASM_SIMP_TAC[]));
 620     (NEW_GOAL `dist (s,u2:real^3) = sqrt(&2)`);
 621       (REWRITE_TAC[GSYM (ASSUME `dist (u0:real^3, s) = sqrt (&2)`)]);
 622       (REWRITE_WITH `dist (u0,s:real^3) = dist (s,u0)`);
 623         BY((NORM_ARITH_TAC));
 624       (REWRITE_TAC[REAL_ARITH `a = b <=> a <= b /\ b <= a`]);
 625       BY((ASM_SIMP_TAC[]));
 626     (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`);
 627       (REWRITE_TAC[ARITH_RULE `4 = 3 + 1`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
 628       (MATCH_MP_TAC Marchal_cells_3.BARV_CARD_LEMMA);
 629       BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
 630     (NEW_GOAL `~(u0 = u1:real^3) /\ ~(u0 = u2) /\ ~(u0 = u3) /\ ~(u1 = u2) /\ ~(u1 = u3) /\ ~(u2 = u3)`);
 631       (REPEAT STRIP_TAC);
 632                 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
 633                   BY((REWRITE_TAC[ASSUME `u0 = u1:real^3`; SET_RULE `{u1, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
 634                 BY((ASM_ARITH_TAC));
 635               (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
 636                 BY((REWRITE_TAC[ASSUME `u0 = u2:real^3`; SET_RULE `{u2, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
 637               BY((ASM_ARITH_TAC));
 638             (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
 639               BY((REWRITE_TAC[ASSUME `u0 = u3:real^3`; SET_RULE `{u3, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
 640             BY((ASM_ARITH_TAC));
 641           (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
 642             BY((REWRITE_TAC[ASSUME `u1 = u2:real^3`; SET_RULE `{u0, u2, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ]));
 643           BY((ASM_ARITH_TAC));
 644         (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
 645           BY((REWRITE_TAC[ASSUME `u1 = u3:real^3`; SET_RULE `{u0, u3, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ]));
 646         BY((ASM_ARITH_TAC));
 647       (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
 648         BY((REWRITE_TAC[ASSUME `u2 = u3:real^3`; SET_RULE `{u0, u1, u3, u3} = {u0,u1,u3}`;Geomdetail.CARD3 ]));
 649       BY((ASM_ARITH_TAC));
 650     (NEW_GOAL `VX V X = {u0,u1,u2}`);
 651       (REWRITE_WITH `VX V X = V INTER X`);
 652         (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
 653         (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `3`);
 654         BY((ASM_REWRITE_TAC[]));
 655       (REWRITE_WITH `X = mcell 3 V ul`);
 656         BY((ASM_REWRITE_TAC[]));
 657       (REWRITE_WITH `V INTER mcell 3 V ul = set_of_list (truncate_simplex (3 - 1) ul)`);
 658         (MATCH_MP_TAC Lepjbdj.LEPJBDJ);
 659         (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3 /\ 3 <= 4`]);
 660         (REWRITE_WITH ` mcell 3 V [u0; u1; u2; u3] = X`);
 661           BY((ASM_REWRITE_TAC[]));
 662         BY((ASM_REWRITE_TAC[]));
 663       BY((ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]));
 664     (UNDISCH_TAC `X = convex hull (set_of_list vl UNION {mxi V ul})`);
 665     (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2; ASSUME `ul = [u0;u1;u2;u3:real^3]`; SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);
 666     (REWRITE_WITH `mxi V [u0; u1; u2; u3] = s`);
 667       BY((EXPAND_TAC "s" THEN AP_TERM_TAC THEN ASM_REWRITE_TAC[]));
 668     (STRIP_TAC);
 669     (NEW_GOAL `~coplanar {u0,u1,u2,s:real^3}`);
 670       (ONCE_REWRITE_TAC[GSYM COPLANAR_AFFINE_HULL_COPLANAR]);
 671       (STRIP_TAC);
 672       (NEW_GOAL `NULLSET X`);
 673         (MATCH_MP_TAC COPLANAR_IMP_NEGLIGIBLE);
 674         (REWRITE_TAC[ASSUME `X = convex hull {u0, u1, u2, s:real^3}`]);
 675         (MATCH_MP_TAC COPLANAR_SUBSET);
 676         (EXISTS_TAC `affine hull {u0, u1, u2, s:real^3}`);
 677         BY((ASM_REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]));
 678       BY((UP_ASM_TAC THEN ASM_REWRITE_TAC[]));
 679     (NEW_GOAL `CARD {u0, u1, u2, s:real^3} = 4`);
 680       (NEW_GOAL `CARD {u0, u1, u2, s:real^3} <= 4`);
 681         BY((REWRITE_TAC[Geomdetail.CARD4]));
 682       (ASM_CASES_TAC `CARD {u0, u1, u2, s:real^3} <= 3`);
 683         (NEW_GOAL `F`);
 684           (UNDISCH_TAC `~coplanar {u0, u1, u2, s:real^3}`);
 685           (REWRITE_TAC[] THEN MATCH_MP_TAC COPLANAR_SMALL);
 686           BY((ASM_REWRITE_TAC[Geomdetail.FINITE6]));
 687         BY((UP_ASM_TAC THEN MESON_TAC[]));
 688       BY((ASM_ARITH_TAC));
 689     (NEW_GOAL `~(u0 = s:real^3) /\ ~(u1 = s) /\ ~(u2 = s)`);
 690       (REPEAT STRIP_TAC);
 691           (NEW_GOAL `CARD {u0, u1, u2,s:real^3} <= 3`);
 692             BY((REWRITE_TAC[ASSUME `u0 = s:real^3`; SET_RULE `{s, u1, u2, s} = {s,u1,u2}`;Geomdetail.CARD3 ]));
 693           BY((ASM_ARITH_TAC));
 694         (NEW_GOAL `CARD {u0, u1, u2, s:real^3} <= 3`);
 695           BY((REWRITE_TAC[ASSUME `u1 = s:real^3`; SET_RULE `{u0, s, u2, s} = {u0,u2,s}`;Geomdetail.CARD3 ]));
 696         BY((ASM_ARITH_TAC));
 697       (NEW_GOAL `CARD {u0, u1, u2, s:real^3} <= 3`);
 698         BY((REWRITE_TAC[ASSUME `u2 = s:real^3`; SET_RULE `{u0, u1, s, s} = {u0,u1,s}`;Geomdetail.CARD3 ]));
 699       BY((ASM_ARITH_TAC));
 700     (ABBREV_TAC `y4 = dist (u1:real^3, u2)`);
 701     (ABBREV_TAC `y5 = dist (u0:real^3, u2)`);
 702     (ABBREV_TAC `y6 = dist (u0:real^3, u1)`);
 703     COMMENT "insert by thales, Jan 2013";
 704     INTRO_TAC Tskajxy_lemmas.gammaX_gamma3f [`V`;`X`;`ul`;`u0`;`u1`;`u2`;`u3`;`y4`;`y5`;`y6`];
 705     ASM_REWRITE_TAC[];
 706     REPEAT WEAK_STRIP_TAC THEN ASM_REWRITE_TAC[arith `x >= &0 <=> &0 <= x`];
 707     REPLICATE_TAC 8 (FIRST_X_ASSUM kill);
 708     FIRST_X_ASSUM MATCH_MP_TAC;
 709     TYPIFY `&2 <= y4 /\ &2 <= y5 /\ &2 <= y6` (C SUBGOAL_THEN ASSUME_TAC);
 710       REPLICATE_TAC 3 (FIRST_X_ASSUM (SUBST1_TAC o SYM));
 711       BY(ASM_MESON_TAC[packing]);
 712     ASM_REWRITE_TAC[];
 713     TYPIFY `y4 <= &2 * sqrt (&2) /\  y5 <= &2 * sqrt (&2) /\ y6 <= &2 * sqrt (&2)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
 714       REPLICATE_TAC 3 (FIRST_X_ASSUM (SUBST1_TAC o SYM));
 715       TYPIFY `!(u:real^3) v. (dist(u,s) = sqrt(&2) /\ dist(v,s) = sqrt(&2)) ==> (dist(u,v) <= &2 * sqrt(&2))` (C SUBGOAL_THEN ASSUME_TAC);
 716         REPEAT WEAK_STRIP_TAC;
 717         FIRST_X_ASSUM (ASSUME_TAC o (ONCE_REWRITE_RULE[DIST_SYM]));
 718         INTRO_TAC DIST_TRIANGLE [`u`;`s`;`v`];
 719         BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
 720       REPEAT (FIRST_X_ASSUM_ST `x = sqrt(&2)` MP_TAC);
 721       TYPIFY `!u. dist (s,u) = dist(u,s)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
 722         BY(MESON_TAC[DIST_SYM]);
 723       BY(MESON_TAC[]);
 724     INTRO_TAC Collect_geom.RADV_FORMULAR [`u0`;`u1`;`u2`];
 725     REWRITE_TAC[Collect_geom.dist3];
 726     ANTS_TAC;
 727       BY(ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);
 728     ASM_REWRITE_TAC[];
 729     FIRST_X_ASSUM_ST `hl vl` MP_TAC;
 730     EXPAND_TAC "vl";
 731     TYPIFY `hl (truncate_simplex 2 ul) = radV {u0,u1,u2}` ENOUGH_TO_SHOW_TAC;
 732       BY(REAL_ARITH_TAC);
 733     REWRITE_TAC[Pack_defs.HL];
 734     AP_TERM_TAC;
 735     GMATCH_SIMP_TAC Bump.SET_OF_LIST_TRUNCATE_2;
 736     ASM_REWRITE_TAC[Bump.EL_EXPLICIT];
 737     REWRITE_TAC[LENGTH];
 738     BY(ARITH_TAC);
 739   BY(ASM_MESON_TAC[NEGLIGIBLE_EMPTY])
 740   ]);;
 741   (* }}} *)
 742
 743
 744 (* ======================================================================== *)
 745
 746 (* OLD SCRIPT FOLLOWS *)
 747
 748
 749 end;;