legacy/oldpacking/packing/development/TSKAJXY.hl

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