text_formalization/packing/URRPHBZ1.hl

   1 (* ========================================================================= *)
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   3 (*                                                                           *)
   4 (*      Authour   : VU KHAC KY                                               *)
   5 (*      Book lemma:  URRPHBZ1                                                *)
   6 (*      Chaper    : Packing (Marchal cells)                                  *)
   7 (*                                                                           *)
   8 (* ========================================================================= *)
   9
  10 (* emailed from Ky to Hales, July 14, 2011 *)
  11
  12 module Urrphbz1 = struct
  13
  14 open Rogers;;
  15 open Vukhacky_tactics;;
  16 open Pack_defs;;
  17 open Pack_concl;;
  18 open Pack1;;
  19 open Sphere;;
  20 open Marchal_cells;;
  21 open Emnwuus;;
  22 open Marchal_cells_2_new;;
  23
  24 let INTER_RCONE_GE_IMP_BETWEEN_PROJ_POINT = prove_by_refinement (
  25  `!a:real^3 b p r.
  26     ~(a = b) /\ &0 <= r /\ p IN rcone_ge a b r INTER rcone_ge b a r  ==>
  27     between (proj_point (b - a) (p - a) + a) (a, b)`,
  28 [(REPEAT STRIP_TAC);
  29  (REWRITE_TAC[between;PRO_EXP] THEN ONCE_REWRITE_TAC[DIST_SYM]);
  30  (REWRITE_TAC[dist; VECTOR_ARITH `(k % x + a) - a = k % x /\
  31   m - (h % (m - n) + n) = (&1 - h) % (m - n)`]);
  32  (ABBREV_TAC `h = ((p - a) dot (b - a)) / ((b - a) dot (b - a:real^3))`);
  33  (REWRITE_TAC[NORM_MUL]);
  34  (REWRITE_WITH `abs h = h /\ abs (&1 - h) = &1 - h`);
  35  (REWRITE_TAC[REAL_ABS_REFL]);
  36  (STRIP_TAC);
  37  (EXPAND_TAC "h" THEN MATCH_MP_TAC REAL_LE_DIV);
  38  (REWRITE_TAC[GSYM NORM_POW_2; REAL_LE_POW_2]);
  39  (SUBGOAL_THEN `p IN rcone_ge a (b:real^3) r` MP_TAC);
  40  (ASM_SET_TAC[]);
  41  (REWRITE_TAC[rcone_ge;rconesgn;IN;IN_ELIM_THM]);
  42  (STRIP_TAC);
  43  (NEW_GOAL `&0 <= dist (p,a) * dist (b,a:real^3) * r`);
  44  (ASM_SIMP_TAC[REAL_LE_MUL;DIST_POS_LE]);
  45  (ASM_REAL_ARITH_TAC);
  46  (EXPAND_TAC "h" THEN REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
  47  (SUBGOAL_THEN `p IN rcone_ge b (a:real^3) r` MP_TAC);
  48  (ASM_SET_TAC[]);
  49  (REWRITE_TAC[rcone_ge;rconesgn;IN;IN_ELIM_THM]);
  50  (STRIP_TAC);
  51  (REWRITE_WITH `((p - a) dot (b - a)) / ((b - a) dot (b - a)) <= &1
  52   <=> ((p - a) dot (b - a)) <= &1 * ((b - a) dot (b - a:real^3))`);
  53  (MATCH_MP_TAC REAL_LE_LDIV_EQ);
  54  (REWRITE_TAC[GSYM NORM_POW_2; GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT;
  55    NORM_EQ_0; VECTOR_ARITH `b - a = vec 0 <=> a = b`]);
  56  (ASM_REWRITE_TAC[]);
  57  (REWRITE_TAC [REAL_MUL_LID; REAL_ARITH `a <= b <=> ~(b < a)`]);
  58  (STRIP_TAC);
  59  (NEW_GOAL `(p - b) dot (a - b) + (p - a) dot (b - a) >
  60              dist (p,b) * dist (a,b) * r + (b - a) dot (b - a:real^3)`);
  61  (ASM_REAL_ARITH_TAC);
  62  (UP_ASM_TAC THEN REWRITE_TAC[VECTOR_ARITH `(p - b) dot (a - b) +
  63  (p - a) dot (b - a) = (b - a) dot (b - a)`;
  64   REAL_ARITH `~(x > y + x) <=> &0 <= y`]);
  65  (ASM_SIMP_TAC[REAL_LE_MUL;DIST_POS_LE]);
  66  (REAL_ARITH_TAC)]);;
  67
  68 (* ================================================================== *)
  69
  70 let INTER_RCONE_GE_LE_lemma = prove_by_refinement(
  71  `!a:real^3 b p s h r.
  72     ~(a = b) /\ s = midpoint (a, b) /\ &0 < r /\ ~(p = a) /\ ~(p = b) /\
  73     inv (&2) <= r pow 2 /\
  74     between (proj_point (b - a) (p - a) + a) (a, s) /\
  75     p IN rcone_ge a b r INTER rcone_ge b a r  ==> dist (s, p) <=  dist (s, a)`,
  76 [(REPEAT STRIP_TAC);
  77  (NEW_GOAL `&0 <= r`);
  78  (ASM_REAL_ARITH_TAC);
  79  (ABBREV_TAC `p' = proj_point (b - a) (p - a) + a:real^3`);
  80  (ABBREV_TAC `x = a + (dist (a, s) / dist (a, p':real^3)) % (p - a)`);
  81  (NEW_GOAL `(p - a) dot (b - a:real^3) >= dist (p,a) * dist (b,a) * r`);
  82  (SUBGOAL_THEN `p IN rcone_ge a (b:real^3) r` MP_TAC);
  83  (ASM_SET_TAC[]);
  84  (REWRITE_TAC[rcone_ge;rconesgn;IN;IN_ELIM_THM]);
  85
  86  (NEW_GOAL `between p (a, x:real^3)`);
  87  (EXPAND_TAC "x" THEN REWRITE_TAC[between]);
  88  (ONCE_REWRITE_TAC[DIST_SYM]);
  89  (REWRITE_TAC[dist; VECTOR_ARITH `(a + x) - a = x:real^3 /\
  90   ((a + k % (p - a) ) - p = (k - &1) % (p - a))`; NORM_MUL]);
  91  (REWRITE_WITH `abs (norm (a - s) / norm (a - p':real^3)) =
  92    norm (a - s) / norm (a - p')`);
  93  (REWRITE_TAC[REAL_ABS_REFL]);
  94  (SIMP_TAC[REAL_LE_DIV; NORM_POS_LE]);
  95  (REWRITE_WITH `abs (norm (a - s) / norm (a - p':real^3) - &1) =
  96    norm (a - s) / norm (a - p') - &1`);
  97  (REWRITE_TAC[REAL_ABS_REFL]);
  98  (ONCE_REWRITE_TAC[NORM_ARITH `norm (a - b) = norm (b - a)`]);
  99  (EXPAND_TAC "p'" THEN SIMP_TAC[VECTOR_ARITH `(k % s + a) - a = k % s`;
 100    PRO_EXP; NORM_MUL;REAL_ABS_DIV; GSYM NORM_POW_2; REAL_LE_POW_2]);
 101  (REWRITE_WITH `abs ((p - a) dot (b - a:real^3))  = (p - a) dot (b - a) /\
 102    abs (norm (b - a) pow 2) = norm (b - a) pow 2`);
 103  (REWRITE_TAC[REAL_ABS_REFL; REAL_LE_POW_2]);
 104  (NEW_GOAL `&0 <= dist (p,a) * dist (b,a:real^3) * r`);
 105  (ASM_SIMP_TAC[REAL_LE_MUL;DIST_POS_LE]);
 106  (ASM_REAL_ARITH_TAC);
 107  (REWRITE_TAC[REAL_ARITH `&0 <= x - &1 <=> &1 <= x`]);
 108  (REWRITE_WITH `b = &2 % s - a:real^3`);
 109  (ASM_REWRITE_TAC[midpoint] THEN VECTOR_ARITH_TAC);
 110  (REWRITE_TAC[VECTOR_ARITH `&2 % s - a - a = &2 % (s - a)`; NORM_MUL;
 111    DOT_RMUL; MESON[REAL_ABS_REFL; REAL_ARITH `&0 <= &2`] `abs (&2) = &2`]);
 112  (REWRITE_TAC[real_div; REAL_INV_MUL; REAL_INV_INV]);
 113
 114  (REWRITE_TAC[REAL_ARITH `x * ((inv (&2) * inv (y)) * (&2 * x) pow 2) *
 115  inv (&2) * inv (x) = (x * inv (x)) * (x pow 2) *  inv (y)`]);
 116  (REWRITE_WITH `norm (s - a:real^3) * inv (norm (s - a)) = &1`);
 117  (MATCH_MP_TAC REAL_MUL_RINV);
 118  (REWRITE_TAC[NORM_EQ_0]);
 119  (ASM_REWRITE_TAC[midpoint; VECTOR_ARITH `inv (&2) % (a + b) - a =
 120    inv (&2) % (b - a)`; VECTOR_MUL_EQ_0]);
 121  (ASM_REWRITE_TAC[VECTOR_ARITH `b -a = vec 0 <=> a = b`]);
 122  (REAL_ARITH_TAC);
 123  (REWRITE_TAC[REAL_MUL_LID; GSYM real_div]);
 124
 125
 126  (NEW_GOAL `&0 < (p - a) dot (s - a:real^3)`);
 127  (REWRITE_WITH `(p - a) dot (s - a:real^3) = inv (&2) * (p - a) dot (b - a)`);
 128  (ASM_REWRITE_TAC[midpoint] THEN VECTOR_ARITH_TAC);
 129  (MATCH_MP_TAC REAL_LT_MUL);
 130  (REWRITE_TAC[REAL_ARITH `&0 < inv (&2)`]);
 131  (NEW_GOAL `&0 < dist (p,a) * dist (b,a:real^3) * r`);
 132  (ASM_SIMP_TAC[REAL_LT_MUL;DIST_POS_LT]);
 133  (ASM_REAL_ARITH_TAC);
 134  (REWRITE_WITH `&1 <= norm (s - a) pow 2 / ((p - a) dot (s - a))
 135   <=> &1 * ((p - a) dot (s - a:real^3)) <= norm (s - a) pow 2 `);
 136  (ASM_SIMP_TAC[REAL_LE_RDIV_EQ]);
 137  (REWRITE_TAC[REAL_MUL_LID]);
 138  (ONCE_REWRITE_TAC[VECTOR_ARITH `(p - a) dot (s - a) =
 139   (p - a - (p' - a)) dot (s - a) + (p' - a) dot (s - a:real^3)`]);
 140  (EXPAND_TAC "p'" THEN REWRITE_TAC[VECTOR_ARITH `(x + a) - a = x:real^3`]);
 141  (REWRITE_TAC[GSYM projection_proj_point]);
 142  (REWRITE_WITH `s - a:real^3 = inv (&2) % (b - a)`);
 143  (ASM_REWRITE_TAC[midpoint] THEN VECTOR_ARITH_TAC);
 144  (REWRITE_TAC[DOT_RMUL;Packing3.PROJECTION_ORTHOGONAL;REAL_MUL_RZERO;
 145    REAL_ADD_LID]);
 146  (REWRITE_WITH `proj_point (b - a) (p - a:real^3) = p' - a`);
 147  (EXPAND_TAC "p'" THEN VECTOR_ARITH_TAC);
 148  (REWRITE_WITH `(p' - a) dot (b - a) = norm (p'- a) * norm (b - a:real^3)`);
 149  (REWRITE_TAC[NORM_CAUCHY_SCHWARZ_EQ]);
 150  (SUBGOAL_THEN `between p' (a, b:real^3)` MP_TAC);
 151  (EXPAND_TAC "p'" THEN MATCH_MP_TAC INTER_RCONE_GE_IMP_BETWEEN_PROJ_POINT);
 152  (EXISTS_TAC `r:real` THEN ASM_REWRITE_TAC[]);
 153  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; IN; IN_ELIM_THM]);
 154  (REPEAT STRIP_TAC);
 155  (FIRST_ASSUM REWRITE_ONLY_TAC);
 156  (REWRITE_WITH `(u % a + v % b) - a = (u % a + v % b) - (u + v) % a:real^3`);
 157  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
 158  (REWRITE_TAC[VECTOR_ARITH `(u % a + v % b) - (u + v) % a = v % (b - a)`;
 159    NORM_MUL; VECTOR_MUL_ASSOC]);
 160  (REWRITE_WITH `abs v = v`);
 161  (ASM_SIMP_TAC[REAL_ABS_REFL]);
 162  (VECTOR_ARITH_TAC);
 163
 164  (NEW_GOAL `inv (&2) * norm (p' - a) * norm (b - a:real^3) <=
 165              inv (&2) * norm (s - a) * norm (b - a)`);
 166  (REWRITE_TAC[REAL_ARITH `a * x * b <= a * y * b <=> &0 <= (a * b) * (y - x)`]);
 167  (MATCH_MP_TAC REAL_LE_MUL);
 168  (STRIP_TAC);
 169  (MATCH_MP_TAC REAL_LE_MUL);
 170  (REWRITE_TAC[NORM_POS_LE; REAL_ARITH `&0 <= inv (&2)`]);
 171  (REWRITE_TAC[GSYM dist]);
 172  (ONCE_REWRITE_TAC[DIST_SYM]);
 173  (UNDISCH_TAC `between p' (a,s:real^3)` THEN REWRITE_TAC[between]);
 174  (DISCH_TAC THEN FIRST_ASSUM REWRITE_ONLY_TAC);
 175  (REWRITE_TAC[REAL_ARITH `(a + b) - a = b`; DIST_POS_LE]);
 176
 177  (NEW_GOAL `norm (inv (&2) % (b - a:real^3)) pow 2 =
 178              inv (&2) * norm (s - a) * norm (b - a)`);
 179  (REWRITE_TAC[NORM_MUL; REAL_POW_2; REAL_ARITH `abs (inv (&2)) = inv (&2)`]);
 180  (REWRITE_TAC[REAL_ARITH
 181   `(z * x) * z * x = z * y * x <=> (y - z * x) * x * z = &0`]);
 182  (REWRITE_WITH `s - a:real^3 = inv (&2) % (b - a)`);
 183  (ASM_REWRITE_TAC[midpoint] THEN VECTOR_ARITH_TAC);
 184  (REWRITE_TAC[NORM_MUL; REAL_ARITH `abs (inv (&2)) = inv (&2)`]);
 185  (REAL_ARITH_TAC);
 186  (ASM_REAL_ARITH_TAC);
 187  (REAL_ARITH_TAC);
 188
 189  (NEW_GOAL `x IN rcone_ge (a:real^3) b r`);
 190  (EXPAND_TAC "x");
 191  (MATCH_MP_TAC RCONE_GE_TRANS);
 192  (STRIP_TAC);
 193  (SIMP_TAC[REAL_LE_DIV;DIST_POS_LE]);
 194  (ASM_REWRITE_TAC[VECTOR_ARITH `(a:real^3) + p - a = p`]);
 195  (ASM_SET_TAC[]);
 196
 197  (NEW_GOAL `(p' - a) dot (b - a) = norm (p'- a) * norm (b - a:real^3)`);
 198  (REWRITE_TAC[NORM_CAUCHY_SCHWARZ_EQ]);
 199  (SUBGOAL_THEN `between p' (a, b:real^3)` MP_TAC);
 200  (EXPAND_TAC "p'" THEN MATCH_MP_TAC INTER_RCONE_GE_IMP_BETWEEN_PROJ_POINT);
 201  (EXISTS_TAC `r:real` THEN ASM_REWRITE_TAC[]);
 202  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; IN; IN_ELIM_THM]);
 203  (REPEAT STRIP_TAC);
 204  (FIRST_ASSUM REWRITE_ONLY_TAC);
 205  (REWRITE_WITH `(u % a + v % b) - a = (u % a + v % b) - (u + v) % a:real^3`);
 206  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
 207  (REWRITE_TAC[VECTOR_ARITH `(u % a + v % b) - (u + v) % a = v % (b - a)`;
 208    NORM_MUL; VECTOR_MUL_ASSOC]);
 209  (REWRITE_WITH `abs v = v`);
 210  (ASM_SIMP_TAC[REAL_ABS_REFL]);
 211  (VECTOR_ARITH_TAC);
 212
 213  (NEW_GOAL `(x - s:real^3) dot (a - s) = &0`);
 214  (EXPAND_TAC "x");
 215  (REWRITE_TAC[VECTOR_ARITH `((a + m % x) - s) dot (a - s) = (s - a) dot (s - a) - m * (x dot (s - a))`]);
 216
 217  (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]);
 218  (REWRITE_WITH `(p - a) dot (s - a) =
 219   (p - a - (p' - a)) dot (s - a) + (p' - a) dot (s - a:real^3)`);
 220  (VECTOR_ARITH_TAC);
 221
 222  (EXPAND_TAC "p'" THEN REWRITE_TAC[VECTOR_ARITH `(x + a) - a = x:real^3`]);
 223  (REWRITE_TAC[GSYM projection_proj_point]);
 224  (REWRITE_WITH `s - a:real^3 = inv (&2) % (b - a)`);
 225  (ASM_REWRITE_TAC[midpoint] THEN VECTOR_ARITH_TAC);
 226  (REWRITE_TAC[DOT_RMUL;Packing3.PROJECTION_ORTHOGONAL;REAL_MUL_RZERO;
 227    REAL_ADD_LID]);
 228  (REWRITE_WITH `proj_point (b - a) (p - a:real^3) = p' - a`);
 229  (EXPAND_TAC "p'" THEN VECTOR_ARITH_TAC);
 230  (FIRST_ASSUM REWRITE_ONLY_TAC);
 231  (REWRITE_TAC[DOT_LMUL; NORM_MUL; REAL_ARITH `abs (inv (&2)) = inv (&2)`;
 232    GSYM NORM_POW_2]);
 233  (REWRITE_TAC [REAL_ARITH `m * m * (x pow 2) - (m * x) / y * m * y * x = &0
 234   <=> m * m * x * x * (y / y - &1) = &0 `]);
 235  (REWRITE_WITH `norm (p' - a) / norm (p' - a:real^3) = &1`);
 236  (MATCH_MP_TAC REAL_DIV_REFL);
 237  (REWRITE_TAC[NORM_EQ_0]);
 238  (EXPAND_TAC "p'" THEN REWRITE_TAC[VECTOR_ARITH `(x + a:real^3) - a = x`]);
 239  (REWRITE_TAC[PRO_EXP;VECTOR_MUL_EQ_0]);
 240  (ASM_REWRITE_TAC[VECTOR_ARITH `b - a = vec 0 <=> a = b`]);
 241  (ONCE_REWRITE_TAC [REAL_ARITH `a / b = a * (&1 / b)`]);
 242  (REWRITE_TAC[REAL_ENTIRE]);
 243  (NEW_GOAL `~((p - a) dot (b - a:real^3) = &0)`);
 244  (NEW_GOAL `&0 < dist (p,a) * dist (b,a:real^3) * r`);
 245  (ASM_SIMP_TAC[REAL_LT_MUL; DIST_POS_LT]);
 246  (ASM_REAL_ARITH_TAC);
 247  (ASM_REWRITE_TAC[]);
 248  (MATCH_MP_TAC Trigonometry2.NOT_EQ0_IMP_NEITHER_INVERT);
 249  (REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0; NORM_EQ_0]);
 250  (ASM_REWRITE_TAC[VECTOR_ARITH `b - a = vec 0 <=> a = b`]);
 251  (REAL_ARITH_TAC);
 252  (NEW_GOAL `dist (s, x) <= dist (s, a:real^3)`);
 253  (NEW_GOAL `norm (a - x:real^3) pow 2 = norm (s - x) pow 2 + norm (a - s) pow 2`);
 254  (MATCH_MP_TAC PYTHAGORAS);
 255  (ASM_REWRITE_TAC[orthogonal]);
 256  (NEW_GOAL `norm (a - s) pow 2 >= inv (&2) * norm (a - x:real^3) pow 2`);
 257  (ONCE_REWRITE_TAC[NORM_ARITH `norm (x - y) = norm (y - x)`]);
 258  (EXPAND_TAC "x" THEN REWRITE_TAC[VECTOR_ARITH `(x + y:real^3) - x = y`]);
 259  (REWRITE_TAC[NORM_MUL]);
 260  (ONCE_REWRITE_TAC[DIST_SYM]);
 261  (REWRITE_TAC[dist]);
 262  (REWRITE_WITH `abs (norm (s - a) / norm (p' - a:real^3)) =
 263                       norm (s - a) / norm (p' - a)`);
 264  (REWRITE_TAC[REAL_ABS_REFL]);
 265  (SIMP_TAC[REAL_LE_DIV;NORM_POS_LE]);
 266  (REWRITE_TAC[REAL_ARITH `(x / y * z) pow 2 = x pow 2 * (z / y) pow 2`]);
 267  (REWRITE_TAC[REAL_ARITH
 268    `x pow 2 >= a *  x pow 2 * b <=> &0 <= x pow 2 * (&1 - a * b)`]);
 269  (MATCH_MP_TAC REAL_LE_MUL);
 270  (STRIP_TAC);
 271
 272  (REWRITE_TAC[REAL_LE_POW_2]);
 273  (REWRITE_TAC[REAL_ARITH `&0 <= &1 - a <=> a <= &1`]);
 274  (NEW_GOAL `norm (p' - a) >= r * norm (p - a:real^3)`);
 275  (EXPAND_TAC "p'" THEN REWRITE_TAC[VECTOR_ARITH `(x + y:real^3) - y = x`]);
 276  (REWRITE_TAC[PRO_EXP]);
 277  (SUBGOAL_THEN `p IN rcone_ge (a:real^3) b r` MP_TAC);
 278  (ASM_SET_TAC[]);
 279  (REWRITE_TAC[rcone_ge;rconesgn;IN;IN_ELIM_THM; dist]);
 280  (STRIP_TAC);
 281  (REWRITE_TAC[NORM_MUL;REAL_ABS_DIV;GSYM NORM_POW_2]);
 282  (REWRITE_WITH `abs ((p - a) dot (b - a)) = (p - a) dot (b - a:real^3) /\
 283                  abs (norm (b - a) pow 2) = norm (b - a) pow 2`);
 284  (REWRITE_TAC[REAL_ABS_REFL;REAL_LE_POW_2]);
 285  (NEW_GOAL `&0 <= norm (p - a) * norm (b - a:real^3) * r`);
 286  (ASM_SIMP_TAC[REAL_LE_MUL; NORM_POS_LE]);
 287  (ASM_REAL_ARITH_TAC);
 288  (REWRITE_TAC[REAL_ARITH `a / x * y >= b <=> b <= (a * y) / x`]);
 289  (REWRITE_WITH `r * norm (p - a) <=
 290    (((p - a) dot (b - a)) * norm (b - a)) / norm (b - a) pow 2
 291    <=> (r * norm (p - a)) * norm (b - a) pow 2 <=
 292    (((p - a) dot (b - a)) * norm (b - a:real^3))`);
 293  (MATCH_MP_TAC REAL_LE_RDIV_EQ);
 294  (REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT; NORM_EQ_0]);
 295  (ASM_REWRITE_TAC[VECTOR_ARITH `b - a = vec 0 <=> a = b`]);
 296  (REWRITE_TAC[REAL_ARITH
 297    `(a * b) * x pow 2 <= m * x  <=> &0 <= x * (m - b * x * a)`]);
 298  (MATCH_MP_TAC REAL_LE_MUL);
 299  (REWRITE_TAC[NORM_POS_LE]);
 300  (ASM_REAL_ARITH_TAC);
 301
 302  (REWRITE_TAC[REAL_POW_DIV;REAL_ARITH `a * b / c = (a * b) / c`]);
 303  (REWRITE_WITH `(inv (&2) * norm (p - a) pow 2) / norm (p' - a) pow 2 <= &1
 304  <=> (inv (&2) * norm (p - a) pow 2) <= &1 * norm (p' - a:real^3) pow 2`);
 305  (MATCH_MP_TAC REAL_LE_LDIV_EQ);
 306  (REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT]);
 307  (STRIP_TAC);
 308  (NEW_GOAL `norm (p - a:real^3) = &0`);
 309  (NEW_GOAL `r * norm (p - a:real^3) = &0`);
 310  (NEW_GOAL `&0 <= r * norm (p - a:real^3)`);
 311  (ASM_SIMP_TAC[REAL_LE_MUL;NORM_POS_LE]);
 312  (ASM_REAL_ARITH_TAC);
 313  (UP_ASM_TAC THEN REWRITE_TAC[REAL_ENTIRE]);
 314  (REWRITE_WITH `~(r = &0)`);
 315  (ASM_REAL_ARITH_TAC);
 316  (UP_ASM_TAC THEN REWRITE_TAC[NORM_EQ_0]);
 317  (ASM_REWRITE_TAC[NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
 318  (REWRITE_TAC[REAL_MUL_LID]);
 319  (NEW_GOAL `(r * norm (p - a)) pow 2 <= norm (p' - a:real^3) pow 2`);
 320  (REWRITE_WITH `(r * norm (p - a)) pow 2 <= norm (p' - a:real^3) pow 2
 321                 <=> r * norm (p - a) <= norm (p' - a)`);
 322  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 323  (MATCH_MP_TAC Trigonometry2.POW2_COND);
 324  (ASM_SIMP_TAC[REAL_LE_MUL;NORM_POS_LE]);
 325  (ASM_REAL_ARITH_TAC);
 326  (NEW_GOAL `inv (&2) * norm (p - a:real^3) pow 2 <= (r * norm (p - a)) pow 2`);
 327  (REWRITE_TAC[REAL_ARITH
 328   `a * x pow 2 <= (m * x) pow 2 <=> &0 <= (m pow 2 - a) * (x pow 2)`]);
 329  (MATCH_MP_TAC REAL_LE_MUL);
 330  (STRIP_TAC);
 331  (ASM_REAL_ARITH_TAC);
 332  (REWRITE_TAC[REAL_LE_POW_2]);
 333  (ASM_REAL_ARITH_TAC);
 334
 335  (NEW_GOAL `norm (s - x) pow 2 <= norm (a - s:real^3) pow 2`);
 336  (ASM_REAL_ARITH_TAC);
 337  (REWRITE_WITH `dist (s,x) <= dist (s,a:real^3)
 338    <=> dist (s,x) pow 2 <= dist (s,a) pow 2`);
 339  (MATCH_MP_TAC Trigonometry2.POW2_COND);
 340  (REWRITE_TAC[DIST_POS_LE]);
 341  (UP_ASM_TAC THEN REWRITE_TAC[GSYM dist] THEN MESON_TAC[DIST_SYM]);
 342
 343  (ONCE_REWRITE_TAC[DIST_SYM]);
 344  (REWRITE_TAC[dist]);
 345  (NEW_GOAL `?y. y IN {a, x:real^3} /\
 346                   (!m. m IN convex hull {a,x} ==> norm (m - s) <= norm (y - s))`);
 347  (MATCH_MP_TAC SIMPLEX_FURTHEST_LE);
 348  (REWRITE_TAC[Geomdetail.FINITE6]);
 349  (SET_TAC[]);
 350  (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE `a IN {x,y} <=> a = x \/ a = y`]
 351    THEN STRIP_TAC);
 352  (UP_ASM_TAC THEN FIRST_ASSUM REWRITE_ONLY_TAC);
 353  (DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
 354  (REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL] THEN ASM_REWRITE_TAC[]);
 355  (UP_ASM_TAC THEN FIRST_ASSUM REWRITE_ONLY_TAC);
 356  (DISCH_TAC);
 357  (NEW_GOAL `norm (p - s) <= norm (x - s:real^3)`);
 358  (FIRST_ASSUM MATCH_MP_TAC);
 359  (REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL] THEN ASM_REWRITE_TAC[]);
 360  (NEW_GOAL `norm (x - s) <= norm (a - s:real^3)`);
 361  (REWRITE_TAC[GSYM dist]);
 362  (ASM_MESON_TAC[DIST_SYM]);
 363  (ASM_REAL_ARITH_TAC)]);;
 364
 365 (* ================================================================== *)
 366 let MCELL_2_PROPERTIES_lemma1 = prove_by_refinement (
 367  `!V ul k p.
 368      saturated V /\
 369      packing V /\
 370      barV V 3 ul /\
 371      p IN mcell2 V ul
 372      ==> dist (midpoint (HD ul, HD (TL ul)), p) <=
 373          hl (truncate_simplex 1 ul)`,
 374 [(REPEAT STRIP_TAC);
 375
 376  (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);
 377  (MP_TAC (ASSUME `barV V 3 ul`));
 378  (REWRITE_TAC[BARV_3_EXPLICIT]);
 379  (FIRST_X_ASSUM CHOOSE_TAC);
 380  (FIRST_X_ASSUM CHOOSE_TAC);
 381  (FIRST_X_ASSUM CHOOSE_TAC);
 382  (FIRST_X_ASSUM CHOOSE_TAC);
 383  (ASM_REWRITE_TAC[HD;TL;TRUNCATE_SIMPLEX_EXPLICIT_1]);
 384  (UNDISCH_TAC `p IN mcell2 V ul` THEN REWRITE_TAC[mcell2]);
 385  (COND_CASES_TAC);
 386  (LET_TAC);
 387  (REWRITE_TAC[IN_INTER] THEN DISCH_TAC);
 388  (UP_ASM_TAC THEN ASM_REWRITE_TAC[HD;TL] THEN STRIP_TAC);
 389
 390  (NEW_GOAL `barV V 1 [u0;u1:real^3]`);
 391  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`);
 392  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 393  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 394  (EXISTS_TAC `3` THEN REWRITE_TAC[ARITH_RULE `1 <= 3`]);
 395  (ASM_REWRITE_TAC[]);
 396
 397  (NEW_GOAL `LENGTH (ul:(real^3)list) = 3 + 1 /\ CARD (set_of_list ul) = 3 + 1`);
 398  (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
 399  (EXISTS_TAC `V:real^3->bool`);
 400  (ASM_REWRITE_TAC[]);
 401
 402  (NEW_GOAL `~ (u0 = u1:real^3)`);
 403  (STRIP_TAC);
 404  (NEW_GOAL `CARD (set_of_list (ul:(real^3)list)) <= 3`);
 405  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; set_of_list]);
 406  (ASM_REWRITE_TAC[SET_RULE `{x,x,a,b} = {x,a,b}`;Geomdetail.CARD3]);
 407  (ASM_ARITH_TAC);
 408
 409  (ABBREV_TAC `s1 = omega_list_n V ul 1`);
 410  (NEW_GOAL `s1 = midpoint (u0,u1:real^3)`);
 411  (EXPAND_TAC "s1");
 412  (REWRITE_WITH `omega_list_n V ul 1 =
 413                  omega_list V [u0; u1:real^3]`);
 414  (REWRITE_TAC [ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 415  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]);
 416  (REWRITE_WITH `omega_list V [u0; u1:real^3] =
 417    circumcenter (set_of_list [u0;u1])`);
 418  (MATCH_MP_TAC XNHPWAB1);
 419  (EXISTS_TAC `1`);
 420  (ASM_REWRITE_TAC[IN]);
 421  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`);
 422  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 423  (ASM_REWRITE_TAC[]);
 424  (REWRITE_TAC[set_of_list;Rogers.CIRCUMCENTER_2]);
 425
 426  (NEW_GOAL `s1 = omega_list V [u0; u1:real^3]`);
 427  (EXPAND_TAC "s1" THEN REWRITE_TAC [ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 428  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]);
 429
 430  (NEW_GOAL `hl [u0;u1] = dist (s1, u0:real^3)`);
 431  (REWRITE_WITH `dist (s1, u0:real^3) = dist (omega_list V [u0;u1],HD [u0;u1])`);
 432  (REWRITE_TAC[HD; ASSUME `s1 = omega_list V [u0; u1:real^3]`]);
 433  (MATCH_MP_TAC Rogers.WAUFCHE2);
 434  (EXISTS_TAC `1`);
 435  (ASM_REWRITE_TAC[IN]);
 436  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`);
 437  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 438  (ASM_REWRITE_TAC[]);
 439
 440  (ASM_CASES_TAC `p = u0:real^3`);
 441  (ASM_REWRITE_TAC[]);
 442  (REAL_ARITH_TAC);
 443  (ASM_CASES_TAC `p = u1:real^3`);
 444  (ASM_REWRITE_TAC[midpoint; dist]);
 445  (NORM_ARITH_TAC);
 446
 447  (NEW_GOAL `between (proj_point (u1 - u0) (p - u0) + u0) (u0,u1:real^3)`);
 448  (MATCH_MP_TAC INTER_RCONE_GE_IMP_BETWEEN_PROJ_POINT);
 449  (EXISTS_TAC `a:real`);
 450  (REPEAT STRIP_TAC);
 451  (ASM_MESON_TAC[]);
 452  (EXPAND_TAC "a");
 453  (MATCH_MP_TAC REAL_LE_DIV);
 454  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;TRUNCATE_SIMPLEX_EXPLICIT_1]);
 455  (ASM_REWRITE_TAC[DIST_POS_LE]);
 456  (MATCH_MP_TAC SQRT_POS_LE);
 457  (REAL_ARITH_TAC);
 458  (REWRITE_TAC[IN_INTER]);
 459  (ASM_REWRITE_TAC[]);
 460  (ASM_CASES_TAC `between (proj_point (u1 - u0) (p - u0) + u0) (u0,s1:real^3)`);
 461
 462  (REWRITE_TAC[GSYM (ASSUME `s1 = midpoint (u0,u1:real^3)`)]);
 463  (REWRITE_TAC[ASSUME `hl [u0; u1] = dist (s1,u0:real^3)`]);
 464  (MATCH_MP_TAC INTER_RCONE_GE_LE_lemma);
 465  (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `a:real`);
 466  (ASM_REWRITE_TAC[IN_INTER]);
 467  (EXPAND_TAC "a");
 468  (REPEAT STRIP_TAC);
 469  (MATCH_MP_TAC REAL_LT_DIV);
 470  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 471  (STRIP_TAC);
 472  (MATCH_MP_TAC DIST_POS_LT);
 473  (REWRITE_TAC[midpoint; VECTOR_ARITH `inv (&2) % (u0 + u1) = u0 <=> inv (&2) %
 474   (u0 - u1) = vec 0`; VECTOR_MUL_EQ_0; REAL_ARITH `~(inv (&2) = &0)`]);
 475  (ASM_REWRITE_TAC[VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
 476  (ASM_SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]);
 477
 478  (REWRITE_TAC[Trigonometry2.DIV_POW2]);
 479  (REWRITE_WITH `sqrt (&2) pow 2 = &2`);
 480  (MATCH_MP_TAC SQRT_POW_2);
 481  (REAL_ARITH_TAC);
 482  (ASM_REWRITE_TAC[REAL_ARITH `inv (&2) <= a / &2 <=> &1 <= a`]);
 483  (ASM_REWRITE_TAC [TRUNCATE_SIMPLEX_EXPLICIT_1; ASSUME `hl [u0; u1] =
 484   dist (s1,u0:real^3)`; midpoint; dist; VECTOR_ARITH `inv (&2) % (u0 + u1) -
 485   u0 = inv (&2) % (u1 - u0)`; NORM_MUL; REAL_ABS_INV; MESON[REAL_ABS_REFL;
 486   REAL_ARITH `&0 <= &2`]`abs (&2) = (&2)`]);
 487  (NEW_GOAL `&1 <= inv (&2) * norm (u1 - u0:real^3)`);
 488  (REWRITE_TAC[REAL_ARITH `&1 <= inv (&2) * a <=> &2 <= a`; GSYM dist]);
 489  (UNDISCH_TAC `packing V`);
 490  (REWRITE_TAC[packing] THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
 491  (NEW_GOAL `set_of_list ul SUBSET V:real^3->bool`);
 492  (MATCH_MP_TAC Packing3.BARV_SUBSET);
 493  (EXISTS_TAC `3`);
 494  (ASM_REWRITE_TAC[]);
 495  (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list]);
 496  (SET_TAC[GSYM IN]);
 497  (NEW_GOAL `&1 pow 2 <= (inv (&2) * norm (u1 - u0:real^3)) pow 2`);
 498  (REWRITE_WITH `&1 pow 2 <= (inv (&2) * norm (u1 - u0:real^3)) pow 2
 499                 <=> &1 <= (inv (&2) * norm (u1 - u0:real^3))`);
 500  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 501  (MATCH_MP_TAC Trigonometry2.POW2_COND);
 502  (ASM_SIMP_TAC[REAL_LE_MUL; REAL_ARITH `&0 <= &1 /\ &0 <= inv (&2)`;
 503    NORM_POS_LE]);
 504  (ASM_REWRITE_TAC[]);
 505  (UP_ASM_TAC THEN REWRITE_TAC[REAL_ARITH `&1 pow 2 = &1`]);
 506
 507
 508  (ASM_CASES_TAC `between (proj_point (u1 - u0) (p - u0) + u0) (s1,u1:real^3)`);
 509
 510  (NEW_GOAL `hl [u0;u1] = dist (s1, u1:real^3)`);
 511  (REWRITE_WITH `dist (s1, u1) = dist (s1, u0:real^3)`);
 512  (ASM_REWRITE_TAC[midpoint;dist]);
 513  (NORM_ARITH_TAC);
 514  (ASM_REWRITE_TAC[]);
 515
 516  (REWRITE_TAC[GSYM (ASSUME `s1 = midpoint (u0,u1:real^3)`)]);
 517  (REWRITE_TAC[ASSUME `hl [u0; u1] = dist (s1,u1:real^3)`]);
 518  (MATCH_MP_TAC INTER_RCONE_GE_LE_lemma);
 519  (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `a:real`);
 520  (ASM_REWRITE_TAC[IN_INTER]);
 521  (EXPAND_TAC "a");
 522  (REPEAT STRIP_TAC);
 523  (REWRITE_TAC[midpoint] THEN VECTOR_ARITH_TAC);
 524  (MATCH_MP_TAC REAL_LT_DIV);
 525  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 526  (STRIP_TAC);
 527  (MATCH_MP_TAC DIST_POS_LT);
 528  (REWRITE_TAC[midpoint; VECTOR_ARITH `inv (&2) % (u0 + u1) = u0 <=> inv (&2) %
 529   (u0 - u1) = vec 0`; VECTOR_MUL_EQ_0; REAL_ARITH `~(inv (&2) = &0)`]);
 530  (ASM_REWRITE_TAC[VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
 531  (ASM_SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]);
 532  (REWRITE_TAC[Trigonometry2.DIV_POW2]);
 533  (REWRITE_WITH `sqrt (&2) pow 2 = &2`);
 534  (MATCH_MP_TAC SQRT_POW_2);
 535  (REAL_ARITH_TAC);
 536  (ASM_REWRITE_TAC[REAL_ARITH `inv (&2) <= a / &2 <=> &1 <= a`]);
 537  (ASM_REWRITE_TAC [TRUNCATE_SIMPLEX_EXPLICIT_1; ASSUME `hl [u0; u1] =
 538   dist (s1,u0:real^3)`; midpoint; dist; VECTOR_ARITH `inv (&2) % (u0 + u1) -
 539   u0 = inv (&2) % (u1 - u0)`; NORM_MUL; REAL_ABS_INV; MESON[REAL_ABS_REFL;
 540   REAL_ARITH `&0 <= &2`]`abs (&2) = (&2)`]);
 541  (NEW_GOAL `&1 <= inv (&2) * norm (u1 - u0:real^3)`);
 542  (REWRITE_TAC[REAL_ARITH `&1 <= inv (&2) * a <=> &2 <= a`; GSYM dist]);
 543  (UNDISCH_TAC `packing V`);
 544  (REWRITE_TAC[packing] THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
 545  (NEW_GOAL `set_of_list ul SUBSET V:real^3->bool`);
 546  (MATCH_MP_TAC Packing3.BARV_SUBSET);
 547  (EXISTS_TAC `3`);
 548  (ASM_REWRITE_TAC[]);
 549  (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list]);
 550  (SET_TAC[GSYM IN]);
 551  (NEW_GOAL `&1 pow 2 <= (inv (&2) * norm (u1 - u0:real^3)) pow 2`);
 552  (REWRITE_WITH `&1 pow 2 <= (inv (&2) * norm (u1 - u0:real^3)) pow 2
 553                 <=> &1 <= (inv (&2) * norm (u1 - u0:real^3))`);
 554  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 555  (MATCH_MP_TAC Trigonometry2.POW2_COND);
 556  (ASM_SIMP_TAC[REAL_LE_MUL; REAL_ARITH `&0 <= &1 /\ &0 <= inv (&2)`;
 557    NORM_POS_LE]);
 558  (ASM_REWRITE_TAC[]);
 559  (UP_ASM_TAC THEN REWRITE_TAC[REAL_ARITH `&1 pow 2 = &1`]);
 560  (REWRITE_WITH `midpoint (u0,u1) = s1:real^3`);
 561  (ASM_REWRITE_TAC[midpoint] THEN VECTOR_ARITH_TAC);
 562  (ONCE_REWRITE_TAC[BETWEEN_SYM]);
 563
 564  (REWRITE_WITH `proj_point (u0 - u1) (p - u1) + u1:real^3 =
 565                  proj_point (u1 - u0) (p - u0) + u0`);
 566  (REWRITE_TAC[PRO_EXP; GSYM NORM_POW_2; GSYM dist; DIST_SYM]);
 567  (REWRITE_TAC[VECTOR_ARITH
 568   `(a / x) % (m - n) + n = (b / x) % (n - m) + m
 569    <=> ((a + b) / x - &1) % (m - n) = vec 0`]);
 570  (REWRITE_TAC[VECTOR_ARITH `(p - u1) dot (u0 - u1) + (p - u0) dot (u1 - u0)
 571   = (u0 - u1) dot (u0 - u1)`]);
 572  (REWRITE_TAC[GSYM NORM_POW_2; GSYM dist]);
 573  (REWRITE_WITH `dist (u0,u1) pow 2 / dist (u0,u1:real^3) pow 2 = &1`);
 574  (MATCH_MP_TAC REAL_DIV_REFL);
 575  (REWRITE_TAC[Trigonometry2.POW2_EQ_0; DIST_EQ_0]);
 576  (ASM_REWRITE_TAC[]);
 577  (VECTOR_ARITH_TAC);
 578  (ASM_REWRITE_TAC[]);
 579  (NEW_GOAL `between (proj_point (u1 - u0) (p - u0) + u0) (u0,s1) \/
 580              between (proj_point (u1 - u0) (p - u0) + u0) (s1, u1:real^3)`);
 581  (MATCH_MP_TAC BETWEEN_TRANS_3_CASES);
 582  (ASM_REWRITE_TAC[BETWEEN_MIDPOINT]);
 583  (NEW_GOAL `F`);
 584  (ASM_MESON_TAC[]);
 585  (ASM_MESON_TAC[]);
 586  (STRIP_TAC);
 587  (NEW_GOAL `F`);
 588  (ASM_SET_TAC[]);
 589  (ASM_MESON_TAC[])]);;
 590
 591 (* ==================================================================== *)
 592
 593 let BOUNDED_MCELL = prove_by_refinement (
 594  `!V ul k.
 595      saturated V /\
 596      packing V /\
 597      barV V 3 ul
 598      ==> bounded (mcell k V ul)`,
 599 [(REPEAT STRIP_TAC);
 600  (ASM_CASES_TAC `k = 0`);
 601  (ASM_REWRITE_TAC[]);
 602  (REPEAT STRIP_TAC THEN REWRITE_TAC[MCELL_EXPLICIT; mcell0]);
 603  (MATCH_MP_TAC BOUNDED_DIFF);
 604  (ASM_SIMP_TAC[ROGERS_EXPLICIT]);
 605  (MATCH_MP_TAC FINITE_IMP_BOUNDED_CONVEX_HULL);
 606  (REWRITE_TAC[Geomdetail.FINITE6]);
 607
 608  (ASM_CASES_TAC `k = 1`);
 609  (MATCH_MP_TAC BOUNDED_SUBSET);
 610  (EXISTS_TAC `rogers V ul`);
 611  (STRIP_TAC);
 612  (ASM_SIMP_TAC[ROGERS_EXPLICIT]);
 613  (MATCH_MP_TAC FINITE_IMP_BOUNDED_CONVEX_HULL);
 614  (REWRITE_TAC[Geomdetail.FINITE6]);
 615  (ASM_REWRITE_TAC[MCELL_EXPLICIT;mcell1]);
 616  (COND_CASES_TAC);
 617  (SET_TAC[]);
 618  (SET_TAC[]);
 619
 620  (ASM_CASES_TAC `k = 2`);
 621  (ASM_REWRITE_TAC[]);
 622  (REPEAT STRIP_TAC THEN REWRITE_TAC[MCELL_EXPLICIT]);
 623  (REWRITE_TAC[bounded]);
 624  (EXISTS_TAC `norm (midpoint (HD ul,HD (TL ul))) +
 625                hl (truncate_simplex 1 (ul:(real^3)list))`);
 626  (REPEAT STRIP_TAC);
 627  (NEW_GOAL `norm (x:real^3) <= norm (x - midpoint (HD ul,HD (TL ul))) +
 628    norm (midpoint (HD ul,HD (TL ul)))`);
 629  (NORM_ARITH_TAC);
 630  (UP_ASM_TAC THEN REWRITE_TAC[GSYM dist]);
 631  (ONCE_REWRITE_TAC[DIST_SYM]);
 632  (NEW_GOAL `dist (midpoint (HD ul,HD (TL ul)),x:real^3) <=
 633              hl (truncate_simplex 1 ul)`);
 634  (MATCH_MP_TAC MCELL_2_PROPERTIES_lemma1);
 635  (EXISTS_TAC `V:real^3->bool`);
 636  (ASM_REWRITE_TAC[]);
 637  (DISCH_TAC);
 638  (ASM_REAL_ARITH_TAC);
 639
 640  (ASM_CASES_TAC `k = 3`);
 641  (ASM_REWRITE_TAC[]);
 642  (REPEAT STRIP_TAC THEN REWRITE_TAC[MCELL_EXPLICIT;mcell3]);
 643  (COND_CASES_TAC);
 644  (MATCH_MP_TAC FINITE_IMP_BOUNDED_CONVEX_HULL);
 645  (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);
 646  (MP_TAC (ASSUME `barV V 3 ul`));
 647  (REWRITE_TAC[BARV_3_EXPLICIT]);
 648  (FIRST_X_ASSUM CHOOSE_TAC);
 649  (FIRST_X_ASSUM CHOOSE_TAC);
 650  (FIRST_X_ASSUM CHOOSE_TAC);
 651  (FIRST_X_ASSUM CHOOSE_TAC);
 652  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list;
 653    SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`; Geomdetail.FINITE6]);
 654  (REWRITE_TAC[BOUNDED_EMPTY]);
 655
 656  (NEW_GOAL `k >= 4`);
 657  (ASM_ARITH_TAC);
 658  (ASM_SIMP_TAC[MCELL_EXPLICIT;mcell4]);
 659  (COND_CASES_TAC);
 660  (MATCH_MP_TAC FINITE_IMP_BOUNDED_CONVEX_HULL);
 661  (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);
 662  (MP_TAC (ASSUME `barV V 3 ul`));
 663  (REWRITE_TAC[BARV_3_EXPLICIT]);
 664  (FIRST_X_ASSUM CHOOSE_TAC);
 665  (FIRST_X_ASSUM CHOOSE_TAC);
 666  (FIRST_X_ASSUM CHOOSE_TAC);
 667  (FIRST_X_ASSUM CHOOSE_TAC);
 668  (ASM_REWRITE_TAC[set_of_list; Geomdetail.FINITE6]);
 669  (REWRITE_TAC[BOUNDED_EMPTY])]);;
 670
 671 (* ================================================================== *)
 672
 673 let MEASURABLE_MCELL = prove (
 674  `!V ul k.
 675      saturated V /\
 676      packing V /\
 677      barV V 3 ul
 678      ==> measurable (mcell k V ul)`,
 679  (REPEAT STRIP_TAC) THEN
 680  (MATCH_MP_TAC MEASURABLE_COMPACT) THEN
 681  (REWRITE_TAC[COMPACT_EQ_BOUNDED_CLOSED]) THEN
 682  (ASM_SIMP_TAC[CLOSED_MCELL;BOUNDED_MCELL]));;
 683
 684 (* MEASURABLE_MCELL = URRPHBZ1 *)
 685
 686 let URRPHBZ1 = prove (URRPHBZ1_concl, REWRITE_TAC[MEASURABLE_MCELL]);;
 687
 688 end;;