text_formalization/packing/SLTSTLO.hl

   1 (* ========================================================================= *)\r
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)\r
   3 (*                                                                           *)\r
   4 (*      Authour   : VU KHAC KY                                               *)\r
   5 (*      Book lemma:  SLTSTLO                                                 *)\r
   6 (*      Chaper    : Packing (Marchal Cells)                                  *)\r
   7 (*      Date      : June - July 2011                                         *)\r
   8 (*                                                                           *)\r
   9 (* ========================================================================= *)\r
  10 \r
  11 module Sltstlo = struct \r
  12 \r
  13 open Rogers;;\r
  14 open Vukhacky_tactics;;\r
  15 open Pack_defs;;\r
  16 open Pack_concl;; \r
  17 open Pack1;;\r
  18 open Sphere;; \r
  19 open Marchal_cells;;\r
  20 open Marchal_cells_2_new;;\r
  21 open Emnwuus;;\r
  22 \r
  23 \r
  24 let seans_fn () =\r
  25 let (tms,tm) = top_goal () in\r
  26 let vss = map frees (tm::tms) in\r
  27 let vs = setify (flat vss) in\r
  28 map dest_var vs;;\r
  29 \r
  30 \r
  31 let NULLSET_SPHERE = prove_by_refinement\r
  32  (`(!P. (?(v:real^3)(r:real). (r> &0)/\ (P={w:real^3 | norm (w-v)= r})) ==> NULLSET P)`,\r
  33   [\r
  34     X_GEN_TAC `s:real^3->bool` THEN STRIP_TAC;\r
  35     FIRST_X_ASSUM(MP_TAC);\r
  36     STRIP_TAC THEN ASM_REWRITE_TAC[GSYM dist] ;\r
  37     ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[NEGLIGIBLE_SPHERE];\r
  38   ]);;\r
  39 \r
  40 \r
  41 (* =========================================================================== *)\r
  42 \r
  43 let SLTSTLO1 = prove_by_refinement (\r
  44  SLTSTLO1_concl,\r
  45 \r
  46 [(REPEAT GEN_TAC THEN REPEAT STRIP_TAC);\r
  47 \r
  48 (* =================== Case 1 ============================================== *)\r
  49 \r
  50  (ASM_CASES_TAC `hl (ul:(real^3)list) < sqrt(&2)`);\r
  51  (EXISTS_TAC `4`);\r
  52  (REWRITE_TAC[ARITH_RULE `4 <= 4`]);\r
  53   (* New subgoal *)\r
  54    (SUBGOAL_THEN `mcell4 V ul = convex hull (set_of_list (ul:(real^3)list))`   \r
  55     ASSUME_TAC);\r
  56   \r
  57   (REWRITE_TAC[mcell4]);\r
  58    (COND_CASES_TAC);\r
  59    (REFL_TAC);\r
  60    (SUBGOAL_THEN `F` ASSUME_TAC);\r
  61    (UP_ASM_TAC THEN UP_ASM_TAC THEN MESON_TAC[]);\r
  62    (UP_ASM_TAC THEN MESON_TAC[]);\r
  63    (SUBGOAL_THEN `mcell 4 V ul = mcell4 V (ul:(real^3)list)`  ASSUME_TAC);\r
  64    (REWRITE_TAC[mcell]);\r
  65    (COND_CASES_TAC);\r
  66    (SUBGOAL_THEN `F` ASSUME_TAC);\r
  67    (MESON_TAC[ASSUME `4 = 0`;ARITH_RULE `~(4 = 0)`]);\r
  68    (UP_ASM_TAC THEN MESON_TAC[]);\r
  69    (COND_CASES_TAC);\r
  70    (SUBGOAL_THEN `F` ASSUME_TAC);\r
  71    (MESON_TAC[ASSUME `4 = 1`;ARITH_RULE `~(4 = 1)`]);\r
  72    (UP_ASM_TAC THEN MESON_TAC[]);\r
  73    (COND_CASES_TAC);\r
  74    (SUBGOAL_THEN `F` ASSUME_TAC);       \r
  75    (MESON_TAC[ASSUME `4 = 2`;ARITH_RULE `~(4 = 2)`]);\r
  76    (UP_ASM_TAC THEN MESON_TAC[]);\r
  77    (COND_CASES_TAC);\r
  78    (SUBGOAL_THEN `F` ASSUME_TAC);\r
  79    (MESON_TAC[ASSUME `4 = 3`;ARITH_RULE `~(4 = 3)`]);\r
  80    (UP_ASM_TAC THEN MESON_TAC[]);\r
  81    (REFL_TAC);\r
  82   \r
  83  (ASM_REWRITE_TAC[]);\r
  84  (DEL_TAC THEN DEL_TAC); \r
  85 \r
  86 (* New subgoal *)\r
  87  (SUBGOAL_THEN `convex hull set_of_list (ul:(real^3)list) =\r
  88              UNIONS {rogers V (left_action_list p ul) | p permutes 0..3}`\r
  89    ASSUME_TAC);\r
  90  (MATCH_MP_TAC WQPRRDY);\r
  91  (ASM_REWRITE_TAC[IN]);\r
  92 (* End subgoal *)\r
  93  (PURE_ASM_REWRITE_TAC[]);\r
  94  (REWRITE_TAC[IN_UNIONS]);\r
  95  (EXISTS_TAC `rogers V (ul:(real^3)list)`);\r
  96  (ASM_REWRITE_TAC[IN_ELIM_THM]);\r
  97  (EXISTS_TAC `I:(num->num)`);\r
  98  (STRIP_TAC);\r
  99  (MESON_TAC[PERMUTES_I]);\r
 100  (AP_TERM_TAC);\r
 101  (REWRITE_TAC[Packing3.LEFT_ACTION_LIST_I]);\r
 102 \r
 103 (* Finish case 1 *)\r
 104 \r
 105 (* =================== Case 2 ============================================== *)\r
 106 \r
 107  (NEW_GOAL `sqrt (&2) <= hl (ul:(real^3)list)`);\r
 108  (UP_ASM_TAC THEN REAL_ARITH_TAC);\r
 109  (SUBGOAL_THEN `? u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]` CHOOSE_TAC);\r
 110  (MP_TAC (ASSUME `barV V 3 ul`));\r
 111  (REWRITE_TAC[BARV_3_EXPLICIT]);\r
 112  (FIRST_X_ASSUM CHOOSE_TAC);\r
 113  (FIRST_X_ASSUM CHOOSE_TAC);\r
 114  (FIRST_X_ASSUM CHOOSE_TAC);\r
 115 \r
 116  (ASM_CASES_TAC `dist(u0:real^3, p) >= sqrt(&2)`);\r
 117  (EXISTS_TAC `0`);\r
 118  (REWRITE_TAC[ARITH_RULE `0 <= 4`]);\r
 119  (SUBGOAL_THEN `mcell 0 V ul = mcell0 V (ul:(real^3)list)`  ASSUME_TAC);\r
 120  (REWRITE_TAC[mcell]);\r
 121  (ONCE_ASM_REWRITE_TAC[]);\r
 122  (REWRITE_TAC[mcell0]);\r
 123  (REWRITE_TAC[DIFF; IN; IN_ELIM_THM]);\r
 124  STRIP_TAC;\r
 125  (ASM_MESON_TAC[IN]);\r
 126  (REWRITE_TAC[ball;IN_ELIM_THM]);\r
 127 \r
 128  (SUBGOAL_THEN `HD (ul:(real^3)list) = u0` ASSUME_TAC);\r
 129  (ASM_REWRITE_TAC[HD]);\r
 130  (ASM_REWRITE_TAC[]);\r
 131  (ASM_REAL_ARITH_TAC);\r
 132 \r
 133 (* Finish case 2 *)\r
 134 \r
 135 (* =================== Case 3 ============================================== *)\r
 136  (NEW_GOAL `dist (u0, p:real^3) < sqrt (&2)`);\r
 137  (UP_ASM_TAC THEN REAL_ARITH_TAC);\r
 138  (ASM_CASES_TAC `~(p IN rcone_gt (HD (ul:(real^3)list)) (HD (TL ul))\r
 139                (hl (truncate_simplex 1 ul) / sqrt (&2))) `);\r
 140  (EXISTS_TAC `1`);\r
 141  (REWRITE_TAC[ARITH_RULE `1 <= 4`]);\r
 142  (SUBGOAL_THEN `mcell 1 V ul = mcell1 V (ul:(real^3)list)`  ASSUME_TAC);\r
 143  (REWRITE_TAC[mcell]);\r
 144  (COND_CASES_TAC);\r
 145  (SUBGOAL_THEN `F` MP_TAC);\r
 146  (UP_ASM_TAC THEN ARITH_TAC);\r
 147  (MESON_TAC[]);\r
 148  (REFL_TAC);\r
 149  (ONCE_ASM_REWRITE_TAC[]);\r
 150  (REWRITE_TAC[mcell1]);\r
 151  (COND_CASES_TAC);\r
 152 \r
 153  (REWRITE_TAC[IN_DIFF]);\r
 154  (ASM_REWRITE_TAC[IN_INTER]);\r
 155  (REWRITE_WITH `HD [u0;u1;u2;u3] = u0:real^3`);\r
 156  (REWRITE_TAC[HD]);\r
 157  (REWRITE_TAC[cball;IN;IN_ELIM_THM]);\r
 158  (ASM_REAL_ARITH_TAC);\r
 159 \r
 160  (NEW_GOAL `F`);\r
 161  (ASM_MESON_TAC[]);\r
 162  (UP_ASM_TAC THEN MESON_TAC[]);\r
 163 \r
 164 (* Finish case 3 *)\r
 165 \r
 166 (* =================== Case 4 ============================================== *)\r
 167  (NEW_GOAL `p IN rcone_gt (HD (ul:(real^3)list)) (HD (TL ul))\r
 168                (hl (truncate_simplex 1 ul) / sqrt (&2))`);\r
 169  (UP_ASM_TAC THEN MESON_TAC[]);\r
 170  (SWITCH_TAC THEN DEL_TAC);\r
 171  (UP_ASM_TAC THEN ASM_REWRITE_TAC[HD;TL; TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
 172  (STRIP_TAC);\r
 173 \r
 174  (ASM_CASES_TAC `p IN aff_ge {u0:real^3, u1} {mxi V ul, omega_list_n V ul 3}`);\r
 175  (EXISTS_TAC `2`);\r
 176  (REWRITE_TAC[ARITH_RULE `2 <= 4`]);\r
 177  (REWRITE_TAC[MCELL_EXPLICIT; mcell2]);\r
 178  (COND_CASES_TAC);\r
 179  (LET_TAC);\r
 180  (REWRITE_TAC[IN_INTER]);\r
 181  (ASM_REWRITE_TAC[HD;TL]);\r
 182  (REWRITE_TAC[GSYM (ASSUME `ul = [u0; u1; u2; u3:real^3]`)]);\r
 183  (ASM_REWRITE_TAC[]);\r
 184  (UP_ASM_TAC THEN UP_ASM_TAC THEN  \r
 185    ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
 186  (REPEAT STRIP_TAC);\r
 187  (MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET B) ==> p IN B`));\r
 188  (EXISTS_TAC `rcone_gt (u0:real^3) u1 a`);\r
 189  (REWRITE_TAC[RCONE_GT_SUBSET_RCONE_GE]);\r
 190  (ASM_MESON_TAC[]);\r
 191  (MATCH_MP_TAC RCONEGE_INTER_VORONOI_CLOSED_IMP_RCONEGE);\r
 192  (EXISTS_TAC `V:real^3->bool`);\r
 193  (ASM_REWRITE_TAC[]);\r
 194 \r
 195  (NEW_GOAL `voronoi_nondg V (ul:(real^3)list)`);\r
 196  (UNDISCH_TAC `barV V 3 (ul:(real^3)list)`);\r
 197  (REWRITE_TAC[BARV]);\r
 198  (STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC);\r
 199  (ASM_REWRITE_TAC[LENGTH; INITIAL_SUBLIST;ARITH_RULE `0 < 3 + 1`]);\r
 200  (EXISTS_TAC `[]:(real^3)list`);\r
 201  (REWRITE_TAC[APPEND]);\r
 202  (UP_ASM_TAC THEN REWRITE_TAC[VORONOI_NONDG]);\r
 203  (ASM_REWRITE_TAC[set_of_list]);\r
 204 \r
 205  (REPEAT STRIP_TAC); \r
 206   (* Break into 7 subgoals *)\r
 207 \r
 208 (* Subgoal 1 & subgoal 2 *)\r
 209  (ASM_SET_TAC[]);\r
 210  (ASM_SET_TAC[]);\r
 211  (NEW_GOAL `&0 < hl [u0; u1:real^3]`);\r
 212  (REWRITE_WITH `hl [u0;u1:real^3] = \r
 213                  hl (truncate_simplex 1 (ul:(real^3)list))`);\r
 214  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
 215  (MATCH_MP_TAC BARV_IMP_HL_1_POS_LT);\r
 216  (EXISTS_TAC `V:real^3->bool`);\r
 217  (ASM_REWRITE_TAC[]);\r
 218  (NEW_GOAL `hl [u0;u1:real^3] = &0`);\r
 219  (ASM_REWRITE_TAC[HL;set_of_list;SET_RULE `{a, a} = {a}`]);\r
 220  (NEW_GOAL `radV {u1:real^3} = dist (circumcenter {u1},u1)`);\r
 221  (NEW_GOAL `(!w. w IN {u1:real^3} ==> radV {u1} = dist (circumcenter {u1},w))`);\r
 222  (MATCH_MP_TAC Rogers.OAPVION2);\r
 223  (REWRITE_TAC[AFFINE_INDEPENDENT_1]);\r
 224  (FIRST_X_ASSUM MATCH_MP_TAC);\r
 225  (SET_TAC[]);\r
 226  (ASM_REWRITE_TAC[Rogers.CIRCUMCENTER_1; dist]);\r
 227  (NORM_ARITH_TAC);\r
 228  (ASM_REAL_ARITH_TAC);\r
 229  (EXPAND_TAC "a");\r
 230  (MATCH_MP_TAC REAL_LT_DIV);\r
 231  (STRIP_TAC);\r
 232  (REWRITE_WITH `hl [u0;u1:real^3] = \r
 233                  hl (truncate_simplex 1 (ul:(real^3)list))`);\r
 234  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
 235  (MATCH_MP_TAC BARV_IMP_HL_1_POS_LT);\r
 236  (EXISTS_TAC `V:real^3->bool`);\r
 237  (ASM_REWRITE_TAC[]);\r
 238  (MATCH_MP_TAC SQRT_POS_LT);\r
 239  (REAL_ARITH_TAC);\r
 240  (EXPAND_TAC "a");\r
 241  (NEW_GOAL `hl [u0; u1:real^3] / sqrt (&2) <= &1 <=> \r
 242              hl [u0; u1] <= &1 * sqrt (&2)`);\r
 243  (MATCH_MP_TAC REAL_LE_LDIV_EQ);\r
 244  (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);\r
 245  (ASM_REWRITE_TAC[]);\r
 246  (ASM_REAL_ARITH_TAC);\r
 247 \r
 248  (MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET B) ==> p IN B`));\r
 249  (EXISTS_TAC `rcone_gt (u0:real^3) u1 a`);\r
 250  (REWRITE_TAC[RCONE_GT_SUBSET_RCONE_GE]);\r
 251  (ASM_MESON_TAC[]);\r
 252 \r
 253  (REWRITE_WITH `p IN voronoi_closed V (u0:real^3) <=>\r
 254                  (?vl. vl IN barV V 3 /\\r
 255                     p IN rogers V vl /\\r
 256                     truncate_simplex 0 vl = [u0])`);\r
 257  (MATCH_MP_TAC Rogers.GLTVHUM);\r
 258  (ASM_REWRITE_TAC[]);\r
 259  (ASM_SET_TAC[]);\r
 260  (EXISTS_TAC `ul:(real^3)list`);\r
 261  (ASM_REWRITE_TAC[IN; TRUNCATE_SIMPLEX_EXPLICIT_0]);\r
 262  (UP_ASM_TAC THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
 263  (REWRITE_TAC[MESON [] `~(a /\ b) <=> ~a \/ ~ b`]);\r
 264  (DISCH_TAC);\r
 265  (NEW_GOAL `~(hl [u0; u1:real^3] < sqrt (&2))`);\r
 266  (ASM_MESON_TAC[]);\r
 267  (NEW_GOAL `hl [u0; u1:real^3] >= sqrt (&2)`);\r
 268  (ASM_REAL_ARITH_TAC);\r
 269  (ABBREV_TAC `t = hl [u0; u1:real^3] / sqrt (&2)`);\r
 270  (NEW_GOAL `&1 <= t`);\r
 271  (EXPAND_TAC "t");\r
 272  (NEW_GOAL `&1 <= hl [u0; u1:real^3] / sqrt (&2) <=> \r
 273              &1 * sqrt (&2) <= hl [u0; u1]`);\r
 274  (MATCH_MP_TAC REAL_LE_RDIV_EQ);\r
 275  (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);\r
 276  (ASM_REWRITE_TAC[]);\r
 277  (ASM_REAL_ARITH_TAC);\r
 278  (UNDISCH_TAC `p IN rcone_gt (u0:real^3) u1 t`);\r
 279  (REWRITE_TAC[rcone_gt;rconesgn; IN; IN_ELIM_THM; dist]);\r
 280  (DISCH_TAC);\r
 281  (NEW_GOAL `F`);\r
 282  (NEW_GOAL `(p - u0) dot (u1 - u0) <= norm (p - u0) * norm (u1 - u0:real^3)`);\r
 283  (REWRITE_TAC[NORM_CAUCHY_SCHWARZ]);\r
 284  (NEW_GOAL `norm (p - u0) * norm (u1 - u0) * t >= \r
 285              norm (p - u0) * norm (u1 - u0:real^3) `);\r
 286  (REWRITE_TAC[REAL_ARITH `a * b * t >= a * b <=> &0 <= (t - &1) * (a * b)`]);\r
 287  (MATCH_MP_TAC REAL_LE_MUL);\r
 288  (STRIP_TAC);\r
 289  (ASM_REAL_ARITH_TAC);\r
 290  (MATCH_MP_TAC REAL_LE_MUL);\r
 291  (REWRITE_TAC[NORM_POS_LE]);\r
 292  (ASM_REAL_ARITH_TAC);\r
 293  (UP_ASM_TAC THEN MESON_TAC[]);\r
 294 \r
 295 (* Finish case 4 *)\r
 296 \r
 297 (* =================== Case 5 ============================================== *)\r
 298 \r
 299  (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`);\r
 300  (NEW_GOAL `mxi V (ul:(real^3)list) = omega_list_n V ul 2`);\r
 301  (REWRITE_TAC[mxi]);\r
 302  (COND_CASES_TAC);\r
 303  (REFL_TAC);\r
 304  (NEW_GOAL `F`);\r
 305  (ASM_REAL_ARITH_TAC);\r
 306  (UP_ASM_TAC THEN MESON_TAC[]);\r
 307  (NEW_GOAL `p IN aff_ge {u0, u1:real^3} {mxi V ul, omega_list_n V ul 3}`);\r
 308  (MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET B) ==> p IN B`));\r
 309 \r
 310  (EXISTS_TAC `rogers V (ul:(real^3)list)`);\r
 311  STRIP_TAC;\r
 312  (ASM_REWRITE_TAC[]);\r
 313  (MATCH_MP_TAC (SET_RULE `(?s. p SUBSET s /\ s SUBSET B) ==> p SUBSET B`));\r
 314  (EXISTS_TAC `convex hull ({u0, u1:real^3} UNION {mxi V ul, omega_list_n V ul 3})`);\r
 315  (STRIP_TAC);\r
 316  (NEW_GOAL \r
 317  `convex hull ({u0, u1:real^3} UNION {mxi V ul, omega_list_n V ul 3}) = \r
 318   convex hull (convex hull ({u0, u1} UNION {mxi V ul, omega_list_n V ul 3}))`);\r
 319  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
 320  (REWRITE_TAC[CONVEX_HULL_EQ; CONVEX_CONVEX_HULL]);\r
 321  (ONCE_ASM_REWRITE_TAC[]);\r
 322  (REWRITE_TAC[ROGERS]);\r
 323  (MATCH_MP_TAC CONVEX_HULL_SUBSET);\r
 324 \r
 325  (ASM_REWRITE_TAC\r
 326   [LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4` ; SET_OF_0_TO_3]);\r
 327  (REWRITE_TAC[IMAGE;SUBSET;IN;IN_ELIM_THM]);\r
 328  (REPEAT STRIP_TAC);\r
 329 \r
 330  (ASM_CASES_TAC `x' = 0`);\r
 331  (REWRITE_WITH `x = u0:real^3`);\r
 332  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[OMEGA_LIST_N;HD]);\r
 333  (ONCE_REWRITE_TAC[GSYM IN]);\r
 334  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);\r
 335  (SET_TAC[]);\r
 336 \r
 337  (ASM_CASES_TAC `x' = 1`);\r
 338  (REWRITE_WITH `x = circumcenter {u0,u1:real^3}`);\r
 339  (ASM_REWRITE_TAC[]);\r
 340  (MATCH_MP_TAC OMEGA_LIST_1_EXPLICIT_NEW);\r
 341  (EXISTS_TAC `u2:real^3`);\r
 342  (EXISTS_TAC `u3:real^3`);\r
 343  (ASM_REWRITE_TAC[IN]);\r
 344  (STRIP_TAC);\r
 345  (ASM_MESON_TAC[IN]);\r
 346 \r
 347  (ASM_CASES_TAC `hl [u0; u1:real^3] < sqrt (&2)`);\r
 348  (ASM_REWRITE_TAC[]);\r
 349  (NEW_GOAL `hl [u0; u1:real^3] >= sqrt (&2)`);\r
 350  (ASM_REAL_ARITH_TAC);\r
 351  (ABBREV_TAC `t = hl [u0; u1:real^3] / sqrt (&2)`);\r
 352  (NEW_GOAL `&1 <= t`);\r
 353  (EXPAND_TAC "t");\r
 354  (NEW_GOAL `&1 <= hl [u0; u1:real^3] / sqrt (&2) <=> \r
 355              &1 * sqrt (&2) <= hl [u0; u1]`);\r
 356  (MATCH_MP_TAC REAL_LE_RDIV_EQ);\r
 357  (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);\r
 358  (ASM_REWRITE_TAC[]);\r
 359  (ASM_REAL_ARITH_TAC);\r
 360  (UNDISCH_TAC `p IN rcone_gt (u0:real^3) u1 t`);\r
 361  (REWRITE_TAC[rcone_gt;rconesgn; IN; IN_ELIM_THM; dist]);\r
 362  (DISCH_TAC);\r
 363  (NEW_GOAL `F`);\r
 364  (NEW_GOAL `(p - u0) dot (u1 - u0) <= norm (p - u0) * norm (u1 - u0:real^3)`);\r
 365  (REWRITE_TAC[NORM_CAUCHY_SCHWARZ]);\r
 366  (NEW_GOAL `norm (p - u0) * norm (u1 - u0) * t >= \r
 367              norm (p - u0) * norm (u1 - u0:real^3) `);\r
 368  (REWRITE_TAC[REAL_ARITH `a * b * t >= a * b <=> &0 <= (t - &1) * (a * b)`]);\r
 369  (MATCH_MP_TAC REAL_LE_MUL);\r
 370  (STRIP_TAC);\r
 371  (ASM_REAL_ARITH_TAC);\r
 372  (MATCH_MP_TAC REAL_LE_MUL);\r
 373  (REWRITE_TAC[NORM_POS_LE]);\r
 374  (ASM_REAL_ARITH_TAC);\r
 375  (UP_ASM_TAC THEN MESON_TAC[]);\r
 376  (ONCE_REWRITE_TAC[GSYM IN]);\r
 377 \r
 378  (MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET B) ==> p IN B`));\r
 379  (EXISTS_TAC `convex hull ({u0, u1:real^3})`);\r
 380  (STRIP_TAC);\r
 381  (REWRITE_TAC[Rogers.CIRCUMCENTER_2; midpoint;CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
 382  (EXISTS_TAC `&1 / (&2)`);\r
 383  (EXISTS_TAC `&1 / (&2)`);\r
 384  (ASM_SIMP_TAC[REAL_LE_DIV; REAL_ARITH `&0 <= &1 /\ &0 <= &2`]);\r
 385  (STRIP_TAC);\r
 386  (REAL_ARITH_TAC);\r
 387  (VECTOR_ARITH_TAC);\r
 388  (MATCH_MP_TAC CONVEX_HULL_SUBSET);\r
 389  (SET_TAC[]);\r
 390 \r
 391  (ASM_CASES_TAC `x' = 2`);\r
 392  (ASM_REWRITE_TAC[]);\r
 393  (ONCE_REWRITE_TAC[GSYM IN]);\r
 394  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);\r
 395  (SET_TAC[]);\r
 396 \r
 397  (ASM_CASES_TAC `x' = 3`);\r
 398  (ASM_REWRITE_TAC[]);\r
 399  (ONCE_REWRITE_TAC[GSYM IN]);\r
 400  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);\r
 401  (SET_TAC[]);\r
 402  (NEW_GOAL `F`);\r
 403  (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN DEL_TAC);\r
 404  (UP_ASM_TAC THEN TRUONG_SET_TAC[]);\r
 405  (UP_ASM_TAC THEN MESON_TAC[]);\r
 406  (ASM_REWRITE_TAC[SET_RULE `{a, b} UNION {c , d} = {a, b, c,d}`]);\r
 407  (REWRITE_TAC[CONVEX_HULL_4_SUBSET_AFF_GE_2_2]);\r
 408  (NEW_GOAL `F`);\r
 409  (ASM_MESON_TAC[]);\r
 410  (ASM_MESON_TAC[]);\r
 411 \r
 412 \r
 413  (NEW_GOAL `hl (truncate_simplex 2 (ul:(real^3)list)) < sqrt (&2)`);\r
 414  (ASM_REAL_ARITH_TAC);\r
 415  (EXISTS_TAC `3`);\r
 416  (REWRITE_TAC[ARITH_RULE `3 <= 4`]);\r
 417  (REWRITE_TAC[MCELL_EXPLICIT; mcell3]);\r
 418  (COND_CASES_TAC);\r
 419 \r
 420  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);\r
 421  (REWRITE_TAC[SET_RULE `{a, b ,c} UNION {d} = {a, b , c, d}`]);\r
 422 \r
 423 \r
 424 \r
 425  (NEW_GOAL \r
 426   `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\\r
 427                   dist (u0,s:real^3) = sqrt (&2) /\\r
 428                   mxi V ul = s)`);\r
 429  (MATCH_MP_TAC MXI_EXPLICIT_OLD);\r
 430  (ASM_MESON_TAC[]);\r
 431  (FIRST_X_ASSUM CHOOSE_TAC);\r
 432  (REWRITE_WITH `mxi V [u0; u1; u2; u3] = s:real^3`);\r
 433  (ASM_MESON_TAC[]);\r
 434 \r
 435 (* ========================================================================= *)\r
 436 \r
 437  (ABBREV_TAC `a = omega_list_n V ul 1`);\r
 438  (ABBREV_TAC `b = omega_list_n V ul 2`);\r
 439  (ABBREV_TAC `c = omega_list_n V ul 3`);\r
 440 \r
 441  (NEW_GOAL `p IN convex hull {u0, a, b, c:real^3}`);\r
 442  (EXPAND_TAC "a" THEN EXPAND_TAC "b" THEN EXPAND_TAC "c");\r
 443  (REWRITE_WITH `u0:real^3 = HD ul`);\r
 444  (ASM_REWRITE_TAC[HD]);\r
 445  (REWRITE_WITH `convex hull\r
 446  {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3} =\r
 447  rogers V ul`);\r
 448  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
 449  (MATCH_MP_TAC ROGERS_EXPLICIT);\r
 450  (ASM_REWRITE_TAC[]);\r
 451  (ASM_REWRITE_TAC[]);\r
 452  (NEW_GOAL `a = midpoint (u0, u1:real^3)`);\r
 453  (REWRITE_TAC[GSYM Rogers.CIRCUMCENTER_2]);\r
 454  (EXPAND_TAC "a");\r
 455  (REWRITE_WITH `{u0,u1} = set_of_list [u0;(u1:real^3)]`);\r
 456  (MESON_TAC[set_of_list]);\r
 457  (REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`; OMEGA_LIST_TRUNCATE_1]);\r
 458  (MATCH_MP_TAC XNHPWAB1);\r
 459 \r
 460  (EXISTS_TAC `1`);\r
 461  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);\r
 462 \r
 463  (MP_TAC (ASSUME `barV V 3 ul`) THEN REWRITE_TAC[IN;BARV]);\r
 464  (REPEAT STRIP_TAC);\r
 465  (REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC 0) = 1 + 1`]);\r
 466  (NEW_GOAL `initial_sublist vl (ul:(real^3)list)`);\r
 467  (UNDISCH_TAC `initial_sublist vl [u0:real^3; u1]`);\r
 468  (REWRITE_TAC[INITIAL_SUBLIST] THEN STRIP_TAC);\r
 469  (EXISTS_TAC `APPEND yl [u2;u3:real^3]`);\r
 470  (REWRITE_TAC[APPEND_ASSOC; GSYM (ASSUME `[u0:real^3; u1] = APPEND vl yl`)]);\r
 471  (ASM_REWRITE_TAC[APPEND]);\r
 472  (ASM_MESON_TAC[]);\r
 473 \r
 474 \r
 475 \r
 476  (ABBREV_TAC `sl = truncate_simplex 2 (ul:(real^3)list)`);\r
 477  (MATCH_MP_TAC (REAL_ARITH `hl (sl:(real^3)list) < b /\ a < hl sl ==> a < b`));\r
 478  (ASM_REWRITE_TAC[]);\r
 479  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 sl`);\r
 480  (EXPAND_TAC "sl" THEN DEL_TAC);\r
 481  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
 482  (EXPAND_TAC "sl" THEN REWRITE_TAC[ASSUME \r
 483   `ul = [u0;u1;u2:real^3;u3]`; TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
 484  (REWRITE_WITH `hl ([u0;u1;u2:real^3]) = \r
 485                  hl (truncate_simplex 2 (sl:(real^3)list))`);\r
 486  (AP_TERM_TAC);\r
 487  (ASM_MESON_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
 488  (REWRITE_WITH `[u0;u1;u2:real^3] = sl`);\r
 489  (ASM_MESON_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
 490 \r
 491  (NEW_GOAL `!i j.  i < j /\ j <= 2\r
 492                      ==> hl (truncate_simplex i (sl:(real^3)list)) \r
 493                        < hl (truncate_simplex j sl)`);\r
 494  (MATCH_MP_TAC XNHPWAB4);\r
 495  (EXISTS_TAC `V:real^3->bool`);\r
 496 \r
 497  (ASM_REWRITE_TAC[]);\r
 498  (EXPAND_TAC "sl" THEN REWRITE_TAC[IN]);\r
 499  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
 500  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
 501  (FIRST_ASSUM MATCH_MP_TAC);\r
 502  (ARITH_TAC);\r
 503 \r
 504 (* ================================================================== *)\r
 505  (NEW_GOAL `p IN convex hull {b, c, u0, u1:real^3}`);\r
 506  (UP_ASM_TAC THEN UP_ASM_TAC);\r
 507  (REWRITE_TAC[CONVEX_HULL_4; midpoint; IN; IN_ELIM_THM]);\r
 508  (REPEAT STRIP_TAC);\r
 509  (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`);\r
 510  (EXISTS_TAC `u + v * inv (&2)` THEN EXISTS_TAC `v * inv (&2)`);\r
 511  (ASM_REWRITE_TAC[]);\r
 512  (NEW_GOAL `&0 <= v * inv (&2)`);\r
 513  (MATCH_MP_TAC REAL_LE_MUL);\r
 514  (ASM_REAL_ARITH_TAC);\r
 515  (ASM_REWRITE_TAC[REAL_ARITH `w + z + (u + v * inv (&2)) + v * inv (&2) = \r
 516    u + v + w + z`]);\r
 517  (STRIP_TAC);\r
 518  (MATCH_MP_TAC REAL_LE_ADD);\r
 519  (ASM_REWRITE_TAC[]);\r
 520  (VECTOR_ARITH_TAC);\r
 521  (NEW_GOAL `convex hull {b, c, u0, u1:real^3} = \r
 522    convex hull {b, s, u0, u1} UNION convex hull {s, c, u0, u1}`);\r
 523  (MATCH_MP_TAC CONVEX_HULL_BREAK_KY_LEMMA);\r
 524  (ASM_REWRITE_TAC[]);\r
 525  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[IN_UNION]);\r
 526  (NEW_GOAL `~(p IN convex hull {s, c, u0, u1:real^3})`);\r
 527  (STRIP_TAC);\r
 528 \r
 529  (NEW_GOAL `p IN aff_ge {u0, u1} {mxi V ul, c:real^3}`);\r
 530 \r
 531 \r
 532 \r
 533 \r
 534 \r
 535  (NEW_GOAL `convex hull {s, c, u0, u1} SUBSET aff_ge {u0, u1} {s, c:real^3}`);\r
 536  (REWRITE_WITH `{s, c, u0, u1} = {u0,u1,s, c:real^3}`);\r
 537  (SET_TAC[]);\r
 538  (REWRITE_TAC[CONVEX_HULL_4_SUBSET_AFF_GE_2_2]);\r
 539  (ASM_SET_TAC[]);\r
 540  (ASM_MESON_TAC[]);\r
 541  (DISCH_TAC);\r
 542  (NEW_GOAL `p IN convex hull {b, s, u0, u1:real^3}`);\r
 543  (ASM_MESON_TAC[]);\r
 544 \r
 545  (NEW_GOAL `b IN convex hull {u0,u1,u2:real^3}`);\r
 546  (EXPAND_TAC "b");\r
 547  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;OMEGA_LIST_TRUNCATE_2]);\r
 548  (ABBREV_TAC `wl = [u0;u1;u2:real^3]`);\r
 549  (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list wl`);\r
 550  (EXPAND_TAC "wl" THEN REWRITE_TAC[set_of_list]);\r
 551  (MATCH_MP_TAC XNHPWAB2);\r
 552  (EXISTS_TAC `2`);\r
 553  (REWRITE_WITH `wl = truncate_simplex 2 (ul:(real^3)list)`);\r
 554  (EXPAND_TAC "wl" THEN REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`]);\r
 555  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
 556  (ASM_REWRITE_TAC[IN]);\r
 557  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
 558  (EXISTS_TAC `3` THEN ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);\r
 559 \r
 560  (UP_ASM_TAC THEN UP_ASM_TAC);\r
 561  (REWRITE_TAC[CONVEX_HULL_3; CONVEX_HULL_4; IN; IN_ELIM_THM]);\r
 562  (REPEAT STRIP_TAC);\r
 563 \r
 564  (EXISTS_TAC `w + u * u'`);\r
 565  (EXISTS_TAC `z + u * v'`);\r
 566  (EXISTS_TAC `u * w'`);\r
 567  (EXISTS_TAC `v:real`);\r
 568 \r
 569  (ASM_SIMP_TAC[REAL_LE_ADD; REAL_LE_MUL]);\r
 570  (STRIP_TAC);\r
 571  (ASM_REWRITE_TAC[REAL_ARITH `(w + u * u') + (z + u * v') + u * w' + v = \r
 572   u * (u' + v' + w') + v + w + z`; REAL_MUL_RID]);\r
 573  (VECTOR_ARITH_TAC);\r
 574  (NEW_GOAL `F`);\r
 575  (ASM_MESON_TAC[]);\r
 576  (ASM_MESON_TAC[])]);;\r
 577 \r
 578 (* =========================================================================== *)\r
 579 (* =========================================================================== *)\r
 580 \r
 581 let SLTSTLO2 = prove_by_refinement (\r
 582  SLTSTLO2_concl,\r
 583 \r
 584 [(REPEAT STRIP_TAC);\r
 585  (ABBREV_TAC `B1 = frontier (rogers V (ul:(real^3)list))`);\r
 586  (ABBREV_TAC `B2 = {w| norm ((w:real^3) - (HD ul)) = sqrt (&2)}`);\r
 587  (ABBREV_TAC `B3 = rcone_eq (HD (ul:(real^3)list)) (HD (TL ul)) \r
 588   (hl (truncate_simplex 1 ul) / sqrt (&2))`);\r
 589  (ABBREV_TAC `B4 = affine hull {(HD (ul:(real^3)list)), (HD (TL ul)), \r
 590   mxi V ul}`);\r
 591  (ABBREV_TAC `B5 = convex hull {omega_list_n V ul 2, \r
 592    omega_list_n V (ul:(real^3)list) 3 }`);\r
 593  (ABBREV_TAC `B6 = affine hull {(HD (ul:(real^3)list)), (HD (TL ul)), \r
 594   (HD (TL (TL ul)))}`);\r
 595  (ABBREV_TAC `B7 = affine hull {omega_list_n V ul 1, omega_list_n V ul 2, \r
 596   omega_list_n V ul 3}`);\r
 597 \r
 598  (ABBREV_TAC `Z = B1 UNION B2 UNION B3 UNION B4 UNION \r
 599   (B5:real^3->bool) UNION B6 UNION B7`);\r
 600  (EXISTS_TAC `Z:real^3->bool`);\r
 601  (REPEAT STRIP_TAC);\r
 602 \r
 603  (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);\r
 604  (MP_TAC (ASSUME `barV V 3 ul`));\r
 605  (REWRITE_TAC[BARV_3_EXPLICIT]);\r
 606  (FIRST_X_ASSUM CHOOSE_TAC);\r
 607  (FIRST_X_ASSUM CHOOSE_TAC);\r
 608  (FIRST_X_ASSUM CHOOSE_TAC);\r
 609  (FIRST_X_ASSUM CHOOSE_TAC);\r
 610 \r
 611  (EXPAND_TAC "Z");\r
 612  (MATCH_MP_TAC NEGLIGIBLE_UNION);\r
 613  (STRIP_TAC);\r
 614  (EXPAND_TAC "B1" THEN MATCH_MP_TAC NEGLIGIBLE_CONVEX_FRONTIER);\r
 615  (ASM_SIMP_TAC[ROGERS_EXPLICIT;CONVEX_CONVEX_HULL]);\r
 616  (MATCH_MP_TAC NEGLIGIBLE_UNION);\r
 617  (STRIP_TAC);\r
 618 \r
 619  (* revised 2013-05-25: *)\r
 620  (NEW_GOAL `(?(v:real^3)(r:real). (r> &0)/\ (B2 ={w:real^3 | norm (w-v)= r}))`);\r
 621  (EXPAND_TAC "B2");\r
 622  (EXISTS_TAC `(HD ul):real^3` THEN EXISTS_TAC `sqrt(&2)`);\r
 623  (ASM_REWRITE_TAC[REAL_ARITH `a > &0 <=> &0 < a`]);\r
 624  (MATCH_MP_TAC SQRT_POS_LT);\r
 625  (REAL_ARITH_TAC);\r
 626  (ASM_SIMP_TAC[NULLSET_SPHERE]);\r
 627  (* end of revision *)\r
 628 \r
 629  (MATCH_MP_TAC NEGLIGIBLE_UNION);\r
 630  (STRIP_TAC);\r
 631  (EXPAND_TAC "B3");\r
 632  (MATCH_MP_TAC NEGLIGIBLE_RCONE_EQ);\r
 633  (ASM_REWRITE_TAC[HD;TL]);\r
 634  (STRIP_TAC);\r
 635  (NEW_GOAL `aff_dim (set_of_list [u0;u1:real^3]) = &0`);\r
 636  (ASM_REWRITE_TAC[set_of_list; SET_RULE `{x, x} = {x}`; AFF_DIM_SING]);\r
 637  (NEW_GOAL `aff_dim (set_of_list [u0;u1:real^3]) = &1`);\r
 638  (MATCH_MP_TAC MHFTTZN1);\r
 639  (EXISTS_TAC `V:real^3->bool`);\r
 640  (ASM_REWRITE_TAC[]); \r
 641  (REWRITE_WITH `[u0; u0:real^3] = truncate_simplex 1 ul`);\r
 642  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
 643  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
 644  (EXISTS_TAC `3`);\r
 645  (ASM_REWRITE_TAC[]);\r
 646  (ARITH_TAC);\r
 647  (NEW_GOAL `&0 = &1`);\r
 648  (ASM_MESON_TAC[INT_OF_NUM_EQ;REAL_OF_NUM_EQ]);\r
 649  (UP_ASM_TAC THEN REAL_ARITH_TAC);\r
 650  (MATCH_MP_TAC NEGLIGIBLE_UNION);\r
 651  (STRIP_TAC);\r
 652  (EXPAND_TAC "B4");\r
 653  (REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]);\r
 654  (MATCH_MP_TAC NEGLIGIBLE_UNION);\r
 655  (STRIP_TAC);\r
 656  (EXPAND_TAC "B5");\r
 657  (ONCE_REWRITE_TAC[SET_RULE `{a,b:real^3} = {a,a,b}`]);\r
 658  (MESON_TAC[NEGLIGIBLE_CONVEX_HULL_3]);\r
 659  (MATCH_MP_TAC NEGLIGIBLE_UNION);\r
 660  (STRIP_TAC);\r
 661  (EXPAND_TAC "B6");\r
 662  (REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]);\r
 663  (EXPAND_TAC "B7");\r
 664  (REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]);\r
 665 \r
 666 (* ========================================================================= *)\r
 667 \r
 668  (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);\r
 669  (MP_TAC (ASSUME `barV V 3 ul`));\r
 670  (REWRITE_TAC[BARV_3_EXPLICIT]);\r
 671  (FIRST_X_ASSUM CHOOSE_TAC);\r
 672  (FIRST_X_ASSUM CHOOSE_TAC);\r
 673  (FIRST_X_ASSUM CHOOSE_TAC);\r
 674  (FIRST_X_ASSUM CHOOSE_TAC);\r
 675 \r
 676  (REWRITE_TAC[EXISTS_UNIQUE]);\r
 677  (NEW_GOAL `?i. i <= 4 /\ p IN mcell i V ul`);\r
 678  (MATCH_MP_TAC SLTSTLO1);\r
 679  (ASM_REWRITE_TAC[]);\r
 680  (ASM_SET_TAC[]);\r
 681  (FIRST_X_ASSUM CHOOSE_TAC THEN EXISTS_TAC `i:num`);\r
 682  (STRIP_TAC);\r
 683  (ASM_REWRITE_TAC[]);\r
 684 \r
 685 (* ========================================================================= *)\r
 686 \r
 687  (ASM_CASES_TAC `hl (ul:(real^3)list) < sqrt(&2)`);\r
 688  (NEW_GOAL ` mcell0 V ul = {} /\ mcell1 V ul = {} /\\r
 689               mcell2 V ul = {} /\ mcell3 V ul = {}`);\r
 690  (ASM_MESON_TAC[EMNWUUS2]);\r
 691  (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC);\r
 692 \r
 693  (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> \r
 694                 ~ (y = 0 \/ y = 1 \/ y = 2 \/ y = 3)`);\r
 695  (REPEAT STRIP_TAC);\r
 696  (UNDISCH_TAC `p IN mcell y V ul` THEN ASM_REWRITE_TAC[MCELL_EXPLICIT]);\r
 697  (SET_TAC[]);\r
 698  (UNDISCH_TAC `p IN mcell y V ul` THEN ASM_REWRITE_TAC[MCELL_EXPLICIT]);\r
 699  (SET_TAC[]);\r
 700  (UNDISCH_TAC `p IN mcell y V ul` THEN ASM_REWRITE_TAC[MCELL_EXPLICIT]);\r
 701  (SET_TAC[]);\r
 702  (UNDISCH_TAC `p IN mcell y V ul` THEN ASM_REWRITE_TAC[MCELL_EXPLICIT]);\r
 703  (SET_TAC[]);\r
 704  (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 4`);\r
 705  (GEN_TAC THEN DISCH_TAC);\r
 706  (NEW_GOAL `~(y = 0 \/ y = 1 \/ y = 2 \/ y = 3)`);\r
 707  (ASM_SIMP_TAC[]);\r
 708  (ASM_ARITH_TAC);\r
 709  (GEN_TAC THEN DISCH_TAC);\r
 710  (NEW_GOAL `y = 4`);\r
 711  (ASM_MESON_TAC[]);\r
 712  (NEW_GOAL `i = 4`);\r
 713  (ASM_MESON_TAC[]);\r
 714  (ASM_MESON_TAC[]);\r
 715  (NEW_GOAL `sqrt (&2) <= hl (ul:(real^3)list)`);\r
 716  (UP_ASM_TAC THEN REAL_ARITH_TAC);\r
 717 \r
 718 (* ========================================================================= *)\r
 719 \r
 720  (ASM_CASES_TAC `dist(u0:real^3, p) >= sqrt(&2)`);\r
 721  (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> \r
 722                 ~ (y = 4 \/ y = 1 \/ y = 2 \/ y = 3)`);\r
 723  (REPEAT STRIP_TAC);\r
 724  (NEW_GOAL `mcell 4 V ul = {}`);\r
 725 \r
 726  (SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);\r
 727  (COND_CASES_TAC);\r
 728  (NEW_GOAL `F`);\r
 729  (ASM_MESON_TAC[]);\r
 730  (ASM_MESON_TAC[]);\r
 731  (REFL_TAC);\r
 732  (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 4`]);\r
 733  (REWRITE_TAC[ASSUME `mcell 4 V ul = {}`]);\r
 734  (SET_TAC[]);\r
 735  (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 1`;\r
 736    MCELL_EXPLICIT;mcell1]);\r
 737  (COND_CASES_TAC);\r
 738  (STRIP_TAC);\r
 739  (NEW_GOAL `~(p:real^3 IN B2)`);\r
 740  (UNDISCH_TAC `p IN rogers V ul DIFF Z` THEN REWRITE_TAC[IN_DIFF]);\r
 741  (EXPAND_TAC "Z" THEN REWRITE_TAC[IN_UNION]);\r
 742  (SET_TAC[]);\r
 743  (NEW_GOAL `p:real^3 IN cball (HD ul,sqrt (&2))`);\r
 744  (ASM_SET_TAC[IN_DIFF;IN_INTER]);\r
 745  (NEW_GOAL `~(p:real^3 IN B2 UNION ball (HD ul,sqrt (&2)))`);\r
 746  (ASM_REWRITE_TAC[IN_UNION;HD;ball;IN;IN_ELIM_THM]);\r
 747  (ASM_REAL_ARITH_TAC);\r
 748  (UP_ASM_TAC THEN REWRITE_WITH `B2 UNION ball (HD ul,sqrt (&2)) = \r
 749    cball (HD (ul:(real^3)list),sqrt (&2))`);\r
 750  (EXPAND_TAC "B2");\r
 751  (REWRITE_TAC[SET_EQ_LEMMA; IN_UNION; cball; ball;IN;IN_ELIM_THM]);\r
 752  (ONCE_REWRITE_TAC[DIST_SYM]);\r
 753  (REWRITE_TAC[dist] THEN REAL_ARITH_TAC);\r
 754  (ASM_REWRITE_TAC[]);\r
 755  (SET_TAC[]);\r
 756 \r
 757 \r
 758  (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 2`;\r
 759    MCELL_EXPLICIT;mcell2]);\r
 760  (COND_CASES_TAC);\r
 761  (LET_TAC);\r
 762  (ASM_REWRITE_TAC[HD;TL] THEN STRIP_TAC);\r
 763  (NEW_GOAL `p:real^3 IN (rcone_ge u0 u1 a INTER rcone_ge u1 u0 a)`);\r
 764  (ASM_SET_TAC[IN_INTER]);\r
 765  (UP_ASM_TAC THEN REWRITE_TAC[IN_INTER;rcone_ge;rconesgn;IN;IN_ELIM_THM]);\r
 766  (REPEAT STRIP_TAC);\r
 767  (NEW_GOAL `(p - u0) dot (u1 - u0:real^3) + (p - u1) dot (u0 - u1) >= \r
 768              dist (p,u0) * dist (u1,u0) * a + dist (p,u1) * dist (u0,u1) * a`);\r
 769  (ASM_REAL_ARITH_TAC);\r
 770  (UP_ASM_TAC THEN REWRITE_TAC[DIST_SYM]);\r
 771  (REWRITE_WITH `(p - u0) dot (u1 - u0:real^3) + (p - u1) dot (u0 - u1) = \r
 772                  (u0 - u1) dot (u0 - u1)`);\r
 773  (VECTOR_ARITH_TAC);\r
 774  (REWRITE_TAC[REAL_ARITH `x * a * b + y * a * b = (x + y) * a * b`; \r
 775                GSYM NORM_POW_2; GSYM dist]);\r
 776 \r
 777 (* ========================================================================== *)\r
 778  (NEW_GOAL `dist (p,u0:real^3) <= dist (p,u1) /\ a = (inv(&2) * dist (u0,u1)) / sqrt (&2)`);\r
 779  (REPEAT STRIP_TAC);\r
 780 \r
 781  (NEW_GOAL `p IN rogers V ul`);\r
 782  (ASM_SET_TAC[IN_DIFF]);\r
 783  (NEW_GOAL `(p:real^3) IN voronoi_closed V u0`);\r
 784  (NEW_GOAL `(p:real^3) IN voronoi_closed V u0 <=>\r
 785                   (?vl. vl IN barV V 3 /\\r
 786                     p IN rogers V vl /\\r
 787                     truncate_simplex 0 vl = [u0:real^3])`);\r
 788  (MATCH_MP_TAC GLTVHUM);\r
 789  (ASM_REWRITE_TAC[]);\r
 790  (MATCH_MP_TAC BARV_IMP_u0_IN_V);\r
 791  (EXISTS_TAC `ul:(real^3)list`);\r
 792  (EXISTS_TAC `u1:real^3`);\r
 793  (EXISTS_TAC `u2:real^3`);\r
 794  (EXISTS_TAC `u3:real^3`);\r
 795  (ASM_REWRITE_TAC[]);\r
 796  (ASM_REWRITE_TAC[]);\r
 797  (EXISTS_TAC `ul:(real^3)list`);\r
 798  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_0]);\r
 799  (ASM_SET_TAC[]);\r
 800  (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed;IN;IN_ELIM_THM]);\r
 801  (DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC);\r
 802  (NEW_GOAL `set_of_list (ul:(real^3)list) SUBSET V`);\r
 803  (MATCH_MP_TAC Packing3.BARV_SUBSET);\r
 804  (EXISTS_TAC `3` THEN ASM_MESON_TAC[]);\r
 805  (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list]);\r
 806  (SET_TAC[]);\r
 807  (EXPAND_TAC "a");\r
 808  (AP_THM_TAC);\r
 809  (AP_TERM_TAC);\r
 810  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; HL;set_of_list]);\r
 811  (NEW_GOAL `!w. w IN {u0,u1:real^3} ==> \r
 812    radV {u0,u1} = dist (circumcenter {u0,u1},w)`);\r
 813  (MATCH_MP_TAC Rogers.OAPVION2);\r
 814  (REWRITE_TAC[AFFINE_INDEPENDENT_IFF_CARD]);\r
 815  (STRIP_TAC);\r
 816  (REWRITE_TAC[Geomdetail.FINITE6]);\r
 817  (NEW_GOAL `aff_dim {u0, u1:real^3} = &1`);\r
 818  (ABBREV_TAC `vl = [u0;u1:real^3]`);\r
 819  (REWRITE_WITH `{u0, u1:real^3} = set_of_list vl`);\r
 820  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
 821  (MATCH_MP_TAC Rogers.MHFTTZN1);\r
 822  (EXISTS_TAC `V:real^3->bool`);\r
 823  (ASM_REWRITE_TAC[]);\r
 824  (REWRITE_WITH `vl = truncate_simplex 1 ul:(real^3)list`);\r
 825  (EXPAND_TAC "vl" THEN DEL_TAC);\r
 826  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
 827  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
 828  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);\r
 829  (ARITH_TAC);\r
 830  (ASM_REWRITE_TAC[]);\r
 831  (ONCE_REWRITE_TAC[ARITH_RULE \r
 832    `&1 = &(CARD {u0, u1:real^3}) - (&1):int \r
 833     <=> &(CARD {u0, u1:real^3}) = (&2):int`]);\r
 834  (ONCE_REWRITE_TAC[INT_OF_NUM_EQ]);\r
 835  (REWRITE_TAC[Geomdetail.CARD2]);\r
 836  (REPEAT STRIP_TAC);\r
 837 \r
 838  (NEW_GOAL `CARD {u0, u1:real^3} = 1`);\r
 839  (REWRITE_WITH `{u0, u1} = {u1:real^3}`);\r
 840  (ASM_SET_TAC[]);\r
 841  (REWRITE_TAC[Geomdetail.CARD_SING]);\r
 842  (NEW_GOAL `aff_dim {u0, u1} <= &(CARD {u0, u1:real^3}) - (&1):int`);\r
 843  (MATCH_MP_TAC AFF_DIM_LE_CARD);\r
 844  (REWRITE_TAC[Geomdetail.FINITE6]);\r
 845  (NEW_GOAL `(&2):int <= &(CARD {u0, u1:real^3})`);\r
 846  (ONCE_REWRITE_TAC[ARITH_RULE  \r
 847    `(&2):int <= &(CARD {u0, u1:real^3}) <=>\r
 848     &1 <= &(CARD {u0, u1:real^3}) - (&1):int`]);\r
 849  (ASM_MESON_TAC[]);\r
 850  (NEW_GOAL `&(CARD {u0, u1:real^3}) <= (&2):int`);\r
 851  (ONCE_REWRITE_TAC[INT_OF_NUM_LE]);\r
 852  (REWRITE_TAC[Geomdetail.CARD2]);\r
 853  (NEW_GOAL `CARD {u0, u1:real^3} = 2`);\r
 854  (ONCE_REWRITE_TAC[GSYM INT_OF_NUM_EQ]);\r
 855  (ASM_ARITH_TAC);\r
 856  (ASM_ARITH_TAC);\r
 857 \r
 858  (REWRITE_WITH `radV {u0, u1} = dist (circumcenter {u0, u1},u0:real^3)`);\r
 859  (FIRST_X_ASSUM MATCH_MP_TAC);\r
 860  (TRUONG_SET_TAC[]);\r
 861  (REWRITE_TAC[CIRCUMCENTER_2;midpoint;dist;\r
 862    VECTOR_ARITH `inv (&2) % (u0 + u1) - u0 = inv (&2) % (u1 - u0)`]);\r
 863  (REWRITE_TAC[NORM_MUL]);\r
 864  (REWRITE_WITH `abs (inv (&2)) = inv (&2)`);\r
 865  (REWRITE_TAC[REAL_ABS_REFL]);\r
 866  (REAL_ARITH_TAC);\r
 867  (REWRITE_TAC[GSYM dist]);\r
 868  (MESON_TAC[DIST_SYM]);\r
 869  (UP_ASM_TAC THEN REPEAT STRIP_TAC);\r
 870  (NEW_GOAL `(dist (p,u0) + dist (p,u1:real^3)) * dist (u0,u1) * a >= \r
 871              (&2 * dist (p,u0)) * dist (u0,u1) * a`);\r
 872  (REWRITE_TAC[REAL_ARITH `(x + y) * a * b >= (&2 * x) * a * b <=>\r
 873                            &0 <= (y - x) * a * b`]);\r
 874  (MATCH_MP_TAC REAL_LE_MUL);\r
 875  (STRIP_TAC);\r
 876  (ASM_REAL_ARITH_TAC);\r
 877  (MATCH_MP_TAC REAL_LE_MUL);\r
 878  (STRIP_TAC);\r
 879  (REWRITE_TAC[DIST_POS_LE]);\r
 880  (ASM_REWRITE_TAC[]);\r
 881  (MATCH_MP_TAC REAL_LE_DIV);\r
 882  (STRIP_TAC);\r
 883  (MATCH_MP_TAC REAL_LE_MUL);\r
 884  (STRIP_TAC);\r
 885  (REAL_ARITH_TAC);\r
 886  (REWRITE_TAC[DIST_POS_LE]);\r
 887  (MATCH_MP_TAC SQRT_POS_LE);\r
 888  (REAL_ARITH_TAC);\r
 889 \r
 890  (NEW_GOAL `dist (u0,u1:real^3) pow 2 >= (&2 * dist (p,u0)) * dist (u0,u1) * a `);\r
 891  (ASM_REAL_ARITH_TAC);\r
 892  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
 893  (REWRITE_TAC[REAL_ARITH `(&2 * x) * a * (inv(&2) * a) / b = (x / b) * a pow 2`]);\r
 894  (REWRITE_TAC[REAL_ARITH `a >= x * a <=> &0 <= a * (&1 - x)`]);\r
 895  (DISCH_TAC);\r
 896  (NEW_GOAL `&0 <= dist (u0,u1) pow 2 * (&1 - dist (p,u0) / sqrt (&2))          \r
 897              <=> &0 <= (&1 - dist (p,u0:real^3) / sqrt (&2))`);\r
 898  (NEW_GOAL `&0 < dist (u0,u1:real^3) pow 2`);\r
 899  (REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT; DIST_EQ_0]);\r
 900  (STRIP_TAC);\r
 901 \r
 902 \r
 903  (NEW_GOAL `aff_dim {u0, u1:real^3} = &1`);\r
 904  (ABBREV_TAC `vl = [u0;u1:real^3]`);\r
 905  (REWRITE_WITH `{u0, u1:real^3} = set_of_list vl`);\r
 906  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
 907  (MATCH_MP_TAC Rogers.MHFTTZN1);\r
 908  (EXISTS_TAC `V:real^3->bool`);\r
 909  (ASM_REWRITE_TAC[]);\r
 910  (REWRITE_WITH `vl = truncate_simplex 1 ul:(real^3)list`);\r
 911  (EXPAND_TAC "vl" THEN DEL_TAC);\r
 912  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
 913  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
 914  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);\r
 915  (ARITH_TAC);\r
 916  (NEW_GOAL `CARD {u0, u1:real^3} = 1`);\r
 917  (REWRITE_WITH `{u0, u1} = {u1:real^3}`);\r
 918  (ASM_SET_TAC[]);\r
 919  (REWRITE_TAC[Geomdetail.CARD_SING]);\r
 920  (NEW_GOAL `aff_dim {u0, u1} <= &(CARD {u0, u1:real^3}) - (&1):int`);\r
 921  (MATCH_MP_TAC AFF_DIM_LE_CARD);\r
 922  (REWRITE_TAC[Geomdetail.FINITE6]);\r
 923  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);\r
 924  (ASM_ARITH_TAC);\r
 925  (ASM_MESON_TAC[REAL_LE_MUL_EQ]);\r
 926  (NEW_GOAL `&0 <= &1 - dist (p,u0:real^3) / sqrt (&2)`);\r
 927  (ASM_MESON_TAC[]);\r
 928  (UP_ASM_TAC THEN REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);\r
 929  (REWRITE_WITH `dist (p,u0:real^3) / sqrt (&2) <= &1 \r
 930              <=> dist (p,u0) <= &1 * sqrt (&2)`);\r
 931  (MATCH_MP_TAC REAL_LE_LDIV_EQ);\r
 932  (MATCH_MP_TAC SQRT_POS_LT);\r
 933  (REAL_ARITH_TAC);\r
 934  (REWRITE_TAC [REAL_MUL_LID]);\r
 935  (STRIP_TAC);\r
 936  (NEW_GOAL `dist (p, u0:real^3) = sqrt (&2)`);\r
 937  (UP_ASM_TAC THEN ONCE_REWRITE_TAC[DIST_SYM]);\r
 938  (ASM_REAL_ARITH_TAC);\r
 939  (NEW_GOAL `~(p:real^3 IN B2)`);\r
 940  (ASM_SET_TAC[IN_DIFF]);\r
 941  (UP_ASM_TAC THEN EXPAND_TAC "B2" THEN REWRITE_TAC[IN;IN_ELIM_THM]);\r
 942  (ASM_REWRITE_TAC[HD;GSYM dist]);\r
 943  (SET_TAC[]);\r
 944 \r
 945 (* ========================================================================= *)\r
 946 \r
 947  (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 3`;\r
 948    MCELL_EXPLICIT;mcell3]);\r
 949  (COND_CASES_TAC);\r
 950 \r
 951  (ASM_REWRITE_TAC[HD;TL;set_of_list]);\r
 952  (NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\\r
 953                   dist (u0,s) = sqrt (&2) /\\r
 954                   mxi V ul = s:real^3)`);\r
 955  (MATCH_MP_TAC MXI_EXPLICIT_OLD);\r
 956  (ASM_REWRITE_TAC[]);\r
 957  (FIRST_X_ASSUM CHOOSE_TAC);\r
 958  (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC);\r
 959  (UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);\r
 960  (REWRITE_TAC[SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);\r
 961  (STRIP_TAC);\r
 962  (SUBGOAL_THEN `p:real^3 IN rogers V ul` MP_TAC);\r
 963  (ASM_SET_TAC[IN_DIFF]);\r
 964  (ASM_SIMP_TAC[ROGERS_EXPLICIT; HD]);\r
 965  (ABBREV_TAC `s1 = omega_list_n V [u0; u1; u2; u3:real^3] 1`);\r
 966  (ABBREV_TAC `s2 = omega_list_n V [u0; u1; u2; u3:real^3] 2`);\r
 967  (ABBREV_TAC `s3 = omega_list_n V [u0; u1; u2; u3:real^3] 3`);\r
 968  (STRIP_TAC);\r
 969  (NEW_GOAL `?m n:real^3. \r
 970              between p (m,n) /\ between m (u0,s1) /\ between n (s2,s3)`);\r
 971  (ASM_SIMP_TAC[CONVEX_HULL_4_IMP_2_2]);\r
 972  (UP_ASM_TAC THEN REPEAT STRIP_TAC);\r
 973  (NEW_GOAL `between (p - m:real^3) (vec 0, n - m)`);\r
 974  (UNDISCH_TAC `between p (m,n:real^3)` THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;\r
 975    CONVEX_HULL_2;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);\r
 976  (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN ASM_REWRITE_TAC[]);\r
 977  (REWRITE_WITH `(u % m + v % n) - m:real^3 = (u % m + v % n) - (u + v) % m`);\r
 978  (ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);\r
 979  (VECTOR_ARITH_TAC);\r
 980  (NEW_GOAL `between (proj_point (s2 - m) (p - m:real^3))\r
 981              (vec 0, proj_point (s2 - m) (n - m))`);\r
 982  (REWRITE_WITH `vec 0 = proj_point (s2 - m) (m - m:real^3)`);\r
 983  (REWRITE_TAC[VECTOR_SUB_REFL; PRO_EXP; DOT_LZERO; REAL_ARITH `&0 / a = &0`]);\r
 984  (VECTOR_ARITH_TAC);\r
 985  (MATCH_MP_TAC BETWEEN_PROJ_POINT);\r
 986  (ASM_REWRITE_TAC[VECTOR_SUB_REFL]);\r
 987  (ABBREV_TAC `p' = proj_point (s2 - m) (p - m:real^3)`);\r
 988  (ABBREV_TAC `n' = proj_point (s2 - m) (n - m:real^3)`);\r
 989 \r
 990 \r
 991 (* ============================================================================ *)\r
 992 \r
 993  (ABBREV_TAC `vl = [u0;u1;u2:real^3]`);\r
 994  (NEW_GOAL `s2:real^3 = circumcenter (set_of_list vl)`);\r
 995  (EXPAND_TAC "s2" THEN EXPAND_TAC "vl");\r
 996  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_2]);\r
 997  (MATCH_MP_TAC XNHPWAB1);\r
 998  (EXISTS_TAC `2`);\r
 999  (REWRITE_WITH `[u0; u1; u2:real^3] = truncate_simplex 2 ul`);\r
1000  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1001  (ASM_REWRITE_TAC[IN]);\r
1002  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1003  (EXISTS_TAC `3`);\r
1004  (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);\r
1005 \r
1006  (NEW_GOAL `s3 IN voronoi_list V (truncate_simplex 2 (ul:(real^3)list))`);\r
1007  (NEW_GOAL `s3 IN voronoi_list V (truncate_simplex (SUC 2) \r
1008    [u0:real^3; u1; u2; u3])`);\r
1009  (EXPAND_TAC "s3");\r
1010  (REWRITE_TAC[OMEGA_LIST_N;ARITH_RULE `3 = SUC 2`]);\r
1011  (MATCH_MP_TAC CLOSEST_POINT_IN_SET);\r
1012  (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);\r
1013  (MATCH_MP_TAC Packing3.BARV_IMP_VORONOI_LIST_NOT_EMPTY);\r
1014  (EXISTS_TAC `3`);\r
1015  (REWRITE_WITH `truncate_simplex (SUC 2) [u0; u1; u2; u3:real^3] = ul`);\r
1016  (ASM_REWRITE_TAC[ARITH_RULE `SUC 2 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3]);\r
1017  (ASM_MESON_TAC[]);\r
1018  (UP_ASM_TAC);\r
1019  (REWRITE_WITH `truncate_simplex (SUC 2) [u0; u1; u2; u3:real^3] = ul`);\r
1020  (ASM_REWRITE_TAC[ARITH_RULE `SUC 2 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3]);\r
1021  (STRIP_TAC);\r
1022  (NEW_GOAL `voronoi_list V (ul:(real^3)list) SUBSET \r
1023    voronoi_list V (truncate_simplex 2 ul)`);\r
1024  (ASM_REWRITE_TAC[VORONOI_LIST;VORONOI_SET; SUBSET;   \r
1025    TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list; IN_INTERS]);\r
1026  (EXPAND_TAC "vl" THEN REWRITE_TAC[IN; IN_ELIM_THM;set_of_list] \r
1027    THEN REPEAT STRIP_TAC);\r
1028  (FIRST_ASSUM MATCH_MP_TAC);\r
1029  (EXISTS_TAC `v:real^3`);\r
1030  (ASM_REWRITE_TAC[]);\r
1031  (SWITCH_TAC THEN UP_ASM_TAC THEN TRUONG_SET_TAC[]);\r
1032  (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[SUBSET]);\r
1033 \r
1034 \r
1035  (NEW_GOAL `n' = s2:real^3 - m`);\r
1036  (EXPAND_TAC "n'");\r
1037  (UNDISCH_TAC `between n (s2,s3:real^3)` THEN REWRITE_TAC[\r
1038   BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);\r
1039  (REWRITE_TAC[ASSUME `n:real^3 = u % s2 + v % s3`]);\r
1040  (REWRITE_WITH `(u % s2 + v % s3) - m:real^3 = (s2 - m) + v % (s3 - s2)`);\r
1041  (REWRITE_TAC[VECTOR_ARITH `(u % s2 + v % s3) - m = s2 - m + v % (s3 - s2) \r
1042    <=> (u + v) % s2 = s2`]);\r
1043  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1044  (REWRITE_TAC[PRO_EXP]);\r
1045  (REWRITE_WITH `((s2 - m + v % (s3 - s2)) dot (s2 - m)) / \r
1046                  ((s2 - m) dot (s2 - m:real^3)) = &1`);\r
1047  (REWRITE_TAC[DOT_LADD; REAL_ARITH `(a + b) / c = a / c + b / c`]);\r
1048  (REWRITE_WITH `((s2 - m) dot (s2 - m)) / ((s2 - m) dot (s2 - m:real^3)) = &1`);\r
1049  (MATCH_MP_TAC REAL_DIV_REFL);\r
1050  (REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0;NORM_EQ_0]);\r
1051  (REWRITE_TAC[VECTOR_ARITH `s2 - m = vec 0 <=> s2 = m`]);\r
1052  (STRIP_TAC);\r
1053 \r
1054  (NEW_GOAL `between s2 (u0, s1:real^3)`);\r
1055  (ASM_MESON_TAC[]);\r
1056  (NEW_GOAL `s2 IN affine hull {u0, s1:real^3}`);\r
1057  (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);\r
1058  (STRIP_TAC);\r
1059  (NEW_GOAL `convex hull {u0,s1:real^3} SUBSET affine hull {u0,s1}`);\r
1060  (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);\r
1061  (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);\r
1062  (NEW_GOAL `affine hull {u0,s1,s2} = affine hull {u0, s1:real^3}`);\r
1063  (MATCH_MP_TAC AFFINE_HULLS_EQ);\r
1064  (REWRITE_TAC[SUBSET; SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`]);\r
1065  (REPEAT STRIP_TAC);\r
1066  (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);\r
1067  (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);\r
1068  (ASM_MESON_TAC[]);\r
1069  (UP_ASM_TAC);\r
1070  (REWRITE_TAC[SUBSET; SET_RULE `x IN {b,c} <=> x = b \/ x = c`]);\r
1071  (REPEAT STRIP_TAC);\r
1072  (ASM_REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);\r
1073  (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);\r
1074  (STRIP_TAC);\r
1075  (REAL_ARITH_TAC);\r
1076  (VECTOR_ARITH_TAC);\r
1077  (ASM_REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);\r
1078  (EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0`);\r
1079  (STRIP_TAC);\r
1080  (REAL_ARITH_TAC);\r
1081  (VECTOR_ARITH_TAC);\r
1082 \r
1083  (NEW_GOAL `aff_dim {u0,s1,s2:real^3} <= &1`);\r
1084  (ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL]);\r
1085  (ONCE_ASM_REWRITE_TAC[]);\r
1086  (ONCE_REWRITE_TAC[AFF_DIM_AFFINE_HULL]);\r
1087  (MATCH_MP_TAC (ARITH_RULE `(?x. x <= &1 /\ y <= x:int) ==> y <= &1`));\r
1088  (EXISTS_TAC `&(CARD {u0,s1:real^3}):int - &1`);\r
1089  (STRIP_TAC);\r
1090  (REWRITE_TAC[ARITH_RULE `a:int - &1 <= &1 <=> a <= &2`; INT_OF_NUM_LE]);\r
1091  (REWRITE_TAC[Geomdetail.CARD2]);\r
1092  (MATCH_MP_TAC AFF_DIM_LE_CARD);\r
1093  (REWRITE_TAC[Geomdetail.FINITE6]);\r
1094 \r
1095  (NEW_GOAL `aff_dim {u0,s1,s2:real^3} = &2`);\r
1096 \r
1097  (NEW_GOAL `vl:(real^3)list = truncate_simplex 2 ul`);\r
1098  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
1099  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1100  (REWRITE_WITH `aff_dim {u0,s1,s2:real^3} = \r
1101                  aff_dim {omega_list_n V vl j | j IN 0..2}`);\r
1102  (AP_TERM_TAC);\r
1103  (REWRITE_TAC[IN_NUMSEG_0]);\r
1104  (REWRITE_TAC[SET_EQ_LEMMA; \r
1105    SET_RULE `x IN {a,b,c} <=> (x = a \/ x = b \/ x = c)`; IN;IN_ELIM_THM]);\r
1106  (REPEAT STRIP_TAC);\r
1107  (EXISTS_TAC `0`);\r
1108  (REWRITE_TAC[ARITH_RULE `0 <= 2`; OMEGA_LIST_N]);\r
1109  (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);\r
1110  (ASM_REWRITE_TAC[]);\r
1111 \r
1112  (EXISTS_TAC `1`);\r
1113  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);\r
1114  (EXPAND_TAC "vl");\r
1115  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1116  (DEL_TAC);\r
1117  (EXPAND_TAC "s1");\r
1118  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);\r
1119 \r
1120  (EXISTS_TAC `2`);\r
1121  (REWRITE_TAC[ARITH_RULE `2 <= 2`; ASSUME `x = s2:real^3`] THEN EXPAND_TAC "vl" THEN DEL_TAC);\r
1122  (EXPAND_TAC "s2");\r
1123  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);\r
1124  (REWRITE_TAC[set_of_list; OMEGA_LIST_TRUNCATE_2;\r
1125    OMEGA_LIST_TRUNCATE_2_NEW1]);\r
1126 \r
1127  (ASM_CASES_TAC `j = 0`);\r
1128  (DISJ1_TAC);\r
1129  (REWRITE_TAC[ASSUME `x:real^3 =  omega_list_n V vl j`; OMEGA_LIST_N; HD]);\r
1130  (EXPAND_TAC "vl");\r
1131  (REWRITE_TAC[ASSUME `j = 0`]);\r
1132  (REWRITE_TAC[OMEGA_LIST_N; HD]);\r
1133 \r
1134  (ASM_CASES_TAC `j = 1`);\r
1135  (DISJ2_TAC);\r
1136  (DISJ1_TAC);\r
1137  (ASM_REWRITE_TAC[]);\r
1138  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);\r
1139  (EXPAND_TAC "s1");\r
1140  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);\r
1141 \r
1142  (ASM_CASES_TAC `j = 2`);\r
1143  (DISJ2_TAC);\r
1144  (DISJ2_TAC);\r
1145  (REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`]);\r
1146  (EXPAND_TAC "vl");\r
1147  (EXPAND_TAC "s2");\r
1148  (REWRITE_TAC[ASSUME `j = 2`; OMEGA_LIST_TRUNCATE_2; OMEGA_LIST_TRUNCATE_2_NEW1]);\r
1149  (SUBGOAL_THEN `F` MP_TAC);\r
1150  (ASM_ARITH_TAC);\r
1151  (MESON_TAC[]);\r
1152 \r
1153  (MATCH_MP_TAC XNHPWAB3);\r
1154  (ASM_REWRITE_TAC[IN]);\r
1155  STRIP_TAC;\r
1156  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1157  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
1158  (ASM_MESON_TAC[]);\r
1159  (ASM_MESON_TAC[]);\r
1160  (ASM_ARITH_TAC);\r
1161 \r
1162 (* ========================================================================= *)\r
1163 \r
1164 (* ========================================================================== *)\r
1165  (MATCH_MP_TAC (REAL_ARITH `x = &0 ==> a + x = a`));\r
1166  (REWRITE_TAC[DOT_LMUL]);\r
1167  (REWRITE_WITH `(s3 - s2) dot (s2 - m:real^3) = &0`);\r
1168  (ONCE_REWRITE_TAC[VECTOR_ARITH `a dot (b - c) = -- (a dot (c - b))`]);\r
1169  (ONCE_REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]);\r
1170  (REWRITE_TAC[ASSUME `s2:real^3 = circumcenter (set_of_list vl)`]);\r
1171  (MATCH_MP_TAC MHFTTZN4);\r
1172  (EXISTS_TAC `V:real^3->bool`);\r
1173  (EXISTS_TAC `2`);\r
1174  (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);\r
1175  (EXPAND_TAC "vl" THEN DEL_TAC);\r
1176  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1177  (REPEAT STRIP_TAC);\r
1178  (ASM_REWRITE_TAC[]);\r
1179 \r
1180  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1181  (EXISTS_TAC `3`);\r
1182  (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);\r
1183 \r
1184 (* ========================================================================== *)\r
1185  (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);\r
1186  (ASM_REWRITE_TAC[]);\r
1187  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);\r
1188  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
1189  (UNDISCH_TAC `between m (u0,s1:real^3)`);\r
1190  (REWRITE_WITH `s1 = midpoint (u0,u1:real^3)`);\r
1191  (EXPAND_TAC "s1");\r
1192 \r
1193  (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 = \r
1194                  omega_list_n V [u0; u1:real^3] 1`);\r
1195  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2;OMEGA_LIST_TRUNCATE_1]);\r
1196  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2]);\r
1197  (REWRITE_WITH `omega_list V [u0; u1:real^3] = \r
1198    circumcenter (set_of_list [u0;u1])`);\r
1199  (MATCH_MP_TAC XNHPWAB1);\r
1200  (EXISTS_TAC `1`);\r
1201  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);\r
1202 \r
1203  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);\r
1204  (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
1205  (REWRITE_TAC[IN] THEN STRIP_TAC);\r
1206  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1207  (EXISTS_TAC `2` THEN REWRITE_TAC[ARITH_RULE `1 <= 2`]);\r
1208  (REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`);\r
1209  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
1210  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1211  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1212  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
1213 \r
1214  (NEW_GOAL `!i j.  i < j /\ j <= 2\r
1215                      ==> hl (truncate_simplex i (vl:(real^3)list)) \r
1216                        < hl (truncate_simplex j vl)`);\r
1217 \r
1218  (MATCH_MP_TAC XNHPWAB4);\r
1219  (EXISTS_TAC `V:real^3->bool`);\r
1220  (ASM_REWRITE_TAC[IN]);\r
1221  (REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`);\r
1222  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
1223  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1224  (ASM_REWRITE_TAC[]);\r
1225  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1226  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
1227  (ASM_MESON_TAC[]);\r
1228  (NEW_GOAL `hl (truncate_simplex 1 (vl:(real^3)list)) < hl (truncate_simplex 2 vl)`);\r
1229  (FIRST_X_ASSUM MATCH_MP_TAC);\r
1230  (ARITH_TAC);\r
1231 \r
1232  (NEW_GOAL `truncate_simplex 2 vl = truncate_simplex 2 ul:(real^3)list`);\r
1233  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
1234  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1235  (MATCH_MP_TAC (REAL_ARITH `a < hl (truncate_simplex 2 (vl:(real^3)list)) /\ \r
1236    hl (truncate_simplex 2 vl) < b ==> a < b`));\r
1237  (ASM_REWRITE_TAC[]);\r
1238  (ASM_MESON_TAC[]);\r
1239  (REWRITE_TAC[set_of_list;Rogers.CIRCUMCENTER_2]);\r
1240  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; midpoint; IN; IN_ELIM_THM; AFFINE_HULL_3]);\r
1241  (REPEAT STRIP_TAC);\r
1242  (EXISTS_TAC `u' + v' * inv (&2)`);\r
1243  (EXISTS_TAC `v' * inv (&2)`);\r
1244  (EXISTS_TAC `&0`);\r
1245  (STRIP_TAC);\r
1246  (REWRITE_TAC[REAL_ARITH `(u' + v' * inv (&2)) + v' * inv (&2) + &0 = u' + v'`]);\r
1247  (ASM_REWRITE_TAC[]);\r
1248  (ASM_REWRITE_TAC[]);\r
1249  (VECTOR_ARITH_TAC);\r
1250  (REWRITE_TAC[REAL_MUL_RZERO; REAL_ARITH `&0 / x = &0`]);\r
1251  (VECTOR_ARITH_TAC);\r
1252 \r
1253 (* ========================================================================== *)\r
1254 \r
1255  (NEW_GOAL `norm (u0 - p:real^3) pow 2 = \r
1256              norm ((p'+ m) - p) pow 2 + norm (u0 - (p' + m)) pow 2`);\r
1257  (MATCH_MP_TAC PYTHAGORAS);\r
1258  (REWRITE_WITH `p - (p'+ m) = projection (s2 - m) (p - m:real^3)`);\r
1259  (REWRITE_TAC[VECTOR_ARITH `p - (a + b:real^3) = (p - b) - a`]);\r
1260  (EXPAND_TAC "p'" THEN REWRITE_TAC[proj_point]);\r
1261  (UNDISCH_TAC `between (p - m) (vec 0,n - m:real^3)`);\r
1262  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN; \r
1263   IN_ELIM_THM; VECTOR_MUL_RZERO;VECTOR_ADD_LID]); \r
1264  (REPEAT STRIP_TAC);\r
1265  (VECTOR_ARITH_TAC);\r
1266  (NEW_GOAL `(?k. k <= &1 /\ &0 <= k /\\r
1267    projection (s2 - m) (p - m:real^3) = k % projection (s2 - m) (n - m))`);\r
1268  (MATCH_MP_TAC PARALLEL_PROJECTION);\r
1269  (ASM_REWRITE_TAC[]);\r
1270  (STRIP_TAC);\r
1271  (NEW_GOAL `s2 = m:real^3`);\r
1272  (ASM_REWRITE_TAC[]);\r
1273  (SWITCH_TAC THEN DEL_TAC);\r
1274 \r
1275  (NEW_GOAL `between s2 (u0, s1:real^3)`);\r
1276  (ASM_MESON_TAC[]);\r
1277  (NEW_GOAL `s2 IN affine hull {u0, s1:real^3}`);\r
1278  (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);\r
1279  (STRIP_TAC);\r
1280  (NEW_GOAL `convex hull {u0,s1:real^3} SUBSET affine hull {u0,s1}`);\r
1281  (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);\r
1282  (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);\r
1283 \r
1284  (NEW_GOAL `affine hull {u0,s1,s2} = affine hull {u0, s1:real^3}`);\r
1285  (MATCH_MP_TAC AFFINE_HULLS_EQ);\r
1286  (REWRITE_TAC[SUBSET; SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`]);\r
1287  (REPEAT STRIP_TAC);\r
1288  (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);\r
1289  (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);\r
1290  (ASM_MESON_TAC[]);\r
1291  (UP_ASM_TAC);\r
1292  (REWRITE_TAC[SUBSET; SET_RULE `x IN {b,c} <=> x = b \/ x = c`]);\r
1293  (REPEAT STRIP_TAC);\r
1294  (ASM_REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);\r
1295  (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);\r
1296  (STRIP_TAC);\r
1297  (REAL_ARITH_TAC);\r
1298  (VECTOR_ARITH_TAC);\r
1299  (REWRITE_TAC[ASSUME `x = s1:real^3`;AFFINE_HULL_3;IN;IN_ELIM_THM]);\r
1300  (EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0`);\r
1301  (STRIP_TAC);\r
1302  (REAL_ARITH_TAC);\r
1303  (VECTOR_ARITH_TAC);\r
1304 \r
1305  (NEW_GOAL `aff_dim {u0,s1,s2:real^3} <= &1`);\r
1306  (ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL]);\r
1307  (ONCE_ASM_REWRITE_TAC[]);\r
1308  (ONCE_REWRITE_TAC[AFF_DIM_AFFINE_HULL]);\r
1309  (MATCH_MP_TAC (ARITH_RULE `(?x. x <= &1 /\ y <= x:int) ==> y <= &1`));\r
1310  (EXISTS_TAC `&(CARD {u0,s1:real^3}):int - &1`);\r
1311  (STRIP_TAC);\r
1312  (REWRITE_TAC[ARITH_RULE `a:int - &1 <= &1 <=> a <= &2`; INT_OF_NUM_LE]);\r
1313  (REWRITE_TAC[Geomdetail.CARD2]);\r
1314  (MATCH_MP_TAC AFF_DIM_LE_CARD);\r
1315  (REWRITE_TAC[Geomdetail.FINITE6]);\r
1316 \r
1317  (NEW_GOAL `aff_dim {u0,s1,s2:real^3} = &2`);\r
1318 \r
1319  (NEW_GOAL `vl:(real^3)list = truncate_simplex 2 ul`);\r
1320  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
1321  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1322  (REWRITE_WITH `aff_dim {u0,s1,s2:real^3} = \r
1323                  aff_dim {omega_list_n V vl j | j IN 0..2}`);\r
1324  (AP_TERM_TAC);\r
1325  (REWRITE_TAC[IN_NUMSEG_0]);\r
1326  (REWRITE_TAC[SET_EQ_LEMMA; \r
1327    SET_RULE `x IN {a,b,c} <=> (x = a \/ x = b \/ x = c)`; IN;IN_ELIM_THM]);\r
1328  (REPEAT STRIP_TAC);\r
1329  (EXISTS_TAC `0`);\r
1330  (REWRITE_TAC[ARITH_RULE `0 <= 2`; OMEGA_LIST_N]);\r
1331  (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);\r
1332  (ASM_REWRITE_TAC[]);\r
1333 \r
1334  (EXISTS_TAC `1`);\r
1335  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);\r
1336  (EXPAND_TAC "vl");\r
1337  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1338  (DEL_TAC);\r
1339  (EXPAND_TAC "s1");\r
1340  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);\r
1341 \r
1342  (EXISTS_TAC `2`);\r
1343  (REWRITE_TAC[ARITH_RULE `2 <= 2`; ASSUME `x = s2:real^3`] THEN EXPAND_TAC "vl" THEN DEL_TAC);\r
1344  (EXPAND_TAC "s2");\r
1345  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);\r
1346  (REWRITE_TAC[set_of_list; OMEGA_LIST_TRUNCATE_2;\r
1347    OMEGA_LIST_TRUNCATE_2_NEW1]);\r
1348 \r
1349  (ASM_CASES_TAC `j = 0`);\r
1350  (DISJ1_TAC);\r
1351  (REWRITE_TAC[ASSUME `x:real^3 =  omega_list_n V vl j`; OMEGA_LIST_N; HD]);\r
1352  (EXPAND_TAC "vl");\r
1353  (REWRITE_TAC[ASSUME `j = 0`]);\r
1354  (REWRITE_TAC[OMEGA_LIST_N; HD]);\r
1355 \r
1356  (ASM_CASES_TAC `j = 1`);\r
1357  (DISJ2_TAC);\r
1358  (DISJ1_TAC);\r
1359  (ASM_REWRITE_TAC[]);\r
1360  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);\r
1361  (EXPAND_TAC "s1");\r
1362  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);\r
1363 \r
1364  (ASM_CASES_TAC `j = 2`);\r
1365  (DISJ2_TAC);\r
1366  (DISJ2_TAC);\r
1367  (REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`]);\r
1368  (EXPAND_TAC "vl");\r
1369  (EXPAND_TAC "s2");\r
1370  (REWRITE_TAC[ASSUME `j = 2`; OMEGA_LIST_TRUNCATE_2; OMEGA_LIST_TRUNCATE_2_NEW1]);\r
1371  (SUBGOAL_THEN `F` MP_TAC);\r
1372  (ASM_ARITH_TAC);\r
1373  (MESON_TAC[]);\r
1374 \r
1375  (MATCH_MP_TAC XNHPWAB3);\r
1376  (ASM_REWRITE_TAC[IN]);\r
1377  STRIP_TAC;\r
1378  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1379  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
1380  (ASM_MESON_TAC[]);\r
1381  (ASM_MESON_TAC[]);\r
1382  (ASM_ARITH_TAC);\r
1383 \r
1384  (FIRST_X_ASSUM CHOOSE_TAC);\r
1385  (UP_ASM_TAC THEN STRIP_TAC);\r
1386 \r
1387 \r
1388  (REWRITE_TAC[ASSUME `projection (s2 - m) (p - m:real^3) = \r
1389    k % projection (s2 - m) (n - m)`]);\r
1390  (REWRITE_TAC[projection_proj_point; orthogonal]);\r
1391  (REWRITE_TAC[ASSUME `proj_point (s2 - m) (n - m:real^3) = n'`]);\r
1392  (REWRITE_TAC[ASSUME `n' = s2 - m:real^3`; \r
1393    VECTOR_ARITH `n - m - (a - m:real^3) = n - a`]);\r
1394  (UNDISCH_TAC `between n (s2,s3:real^3)`);\r
1395  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM] THEN \r
1396    REPEAT STRIP_TAC);\r
1397  (REWRITE_TAC[ASSUME `n = u % s2 + v % s3:real^3`]);\r
1398  (REWRITE_WITH `(u % s2 + v % s3:real^3) - s2 = (u % s2 + v % s3) - (u + v) % s2`);\r
1399  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
1400  (REWRITE_TAC[VECTOR_ARITH \r
1401   `(u % s2 + v % s3) - (u + v) % s2 = v % (s3 - s2:real^3)`]);\r
1402  (ONCE_REWRITE_TAC[VECTOR_ARITH \r
1403   `u0 - (p' + m) = ((u0:real^3) + s2 - (p' + m)) - s2`]);\r
1404  (NEW_GOAL `(s3 - s2:real^3) dot ((u0 + s2 - (p' + m)) - s2) = &0`);\r
1405  (ASM_REWRITE_TAC[]);\r
1406  (MATCH_MP_TAC MHFTTZN4);\r
1407  (EXISTS_TAC `V:real^3->bool`);\r
1408  (EXISTS_TAC `2`);\r
1409  (ASM_REWRITE_TAC[]);\r
1410  (STRIP_TAC);\r
1411  (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);\r
1412  (ASM_REWRITE_TAC[]);\r
1413  (EXPAND_TAC "vl");\r
1414  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1415  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1416  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
1417  (STRIP_TAC);\r
1418  (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);\r
1419  (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);\r
1420  (ASM_REWRITE_TAC[]);\r
1421  (EXPAND_TAC "vl");\r
1422  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1423  (ASM_REWRITE_TAC[]);\r
1424  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
1425 \r
1426  (NEW_GOAL `!a b c m n p.\r
1427    m IN affine hull {a,b,c:real^3} /\\r
1428    n IN affine hull {a,b,c} /\\r
1429    p IN affine hull {a,b,c}\r
1430    ==> m + n - p IN affine hull {a,b,c}`);\r
1431  (REWRITE_TAC[AFFINE_HULL_3; IN;IN_ELIM_THM]);\r
1432  (REPEAT STRIP_TAC);\r
1433  (EXISTS_TAC `(u' + u'') - u'''`);\r
1434  (EXISTS_TAC `(v' + v'') - v'''`);\r
1435  (EXISTS_TAC `(w + w') - w''`);\r
1436  STRIP_TAC;\r
1437  (ASM_REAL_ARITH_TAC);\r
1438  (ASM_REWRITE_TAC[]);\r
1439  (VECTOR_ARITH_TAC);\r
1440  (FIRST_X_ASSUM MATCH_MP_TAC);\r
1441 \r
1442  (REPEAT STRIP_TAC);\r
1443 \r
1444  (REWRITE_TAC[AFFINE_HULL_3; IN;IN_ELIM_THM]);\r
1445  (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);\r
1446  STRIP_TAC;\r
1447  (ASM_REAL_ARITH_TAC);\r
1448  (VECTOR_ARITH_TAC);\r
1449 \r
1450 \r
1451  (MATCH_MP_TAC Rogers.OAPVION1);\r
1452  (STRIP_TAC);\r
1453  (SET_TAC[]);\r
1454  (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);\r
1455  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
1456  (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);\r
1457 \r
1458  (EXISTS_TAC `V:real^3->bool`);\r
1459  (EXISTS_TAC `2`);\r
1460  (ASM_REWRITE_TAC[]);\r
1461  (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);\r
1462  (ASM_REWRITE_TAC[]);\r
1463  (EXPAND_TAC "vl");\r
1464  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1465  (MATCH_MP_TAC Packing3. TRUNCATE_SIMPLEX_BARV);\r
1466  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
1467 \r
1468  (EXPAND_TAC "p'");\r
1469  (REWRITE_TAC[PRO_EXP]);\r
1470  (ABBREV_TAC `h = ((p - m) dot (s2 - m)) / ((s2 - m) dot (s2 - m:real^3))`);\r
1471 \r
1472  (NEW_GOAL `!a b c x y r.\r
1473    x IN affine hull {a,b,c:real^3} /\\r
1474    y IN affine hull {a,b,c} \r
1475    ==> r % (x - y) + y IN affine hull {a,b,c}`);\r
1476  (REWRITE_TAC[AFFINE_HULL_3; IN;IN_ELIM_THM]);\r
1477  (REPEAT STRIP_TAC);\r
1478  (EXISTS_TAC `r * (u' - u'') + u''`);\r
1479  (EXISTS_TAC `r * (v' - v'') + v''`);\r
1480  (EXISTS_TAC `r * (w - w') + w'`);\r
1481  STRIP_TAC;\r
1482  (REWRITE_TAC[REAL_ARITH \r
1483  `(r * (u' - u'') + u'') + (r * (v' - v'') + v'') + r * (w - w') + w' = \r
1484   r * (u' + v' + w) - r * (u'' + v'' + w') + (u'' + v'' + w')`]);\r
1485  (ASM_REWRITE_TAC[REAL_MUL_RID]);\r
1486  (ASM_REAL_ARITH_TAC);\r
1487  (ASM_REWRITE_TAC[]);\r
1488  (VECTOR_ARITH_TAC);\r
1489  (FIRST_X_ASSUM MATCH_MP_TAC);\r
1490  (ASM_REWRITE_TAC[]);\r
1491  (STRIP_TAC);\r
1492 \r
1493 \r
1494  (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);\r
1495  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
1496  (MATCH_MP_TAC Rogers.OAPVION1);\r
1497  (STRIP_TAC);\r
1498  (REWRITE_WITH `set_of_list vl = {u0, u1, u2:real^3}`);\r
1499  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
1500  (SET_TAC[]);\r
1501  (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);\r
1502  (EXISTS_TAC `V:real^3->bool`);\r
1503  (EXISTS_TAC `2`);\r
1504  (ASM_REWRITE_TAC[]);\r
1505  (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);\r
1506  (ASM_REWRITE_TAC[]);\r
1507  (EXPAND_TAC "vl");\r
1508  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1509  (MATCH_MP_TAC Packing3. TRUNCATE_SIMPLEX_BARV);\r
1510  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
1511 \r
1512  (UNDISCH_TAC `between m (u0,s1:real^3)`);\r
1513  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;\r
1514    AFFINE_HULL_3;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);\r
1515  (UP_ASM_TAC);\r
1516 \r
1517  (REWRITE_WITH `s1 = midpoint (u0,u1:real^3)`);\r
1518  (REWRITE_TAC[GSYM (ASSUME `omega_list_n V [u0; u1; u2; u3:real^3] 1 = s1`)]);\r
1519  (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 = \r
1520                  omega_list_n V [u0; u1:real^3] 1`);\r
1521  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2;OMEGA_LIST_TRUNCATE_1]);\r
1522  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2]);\r
1523  (REWRITE_WITH `omega_list V [u0; u1:real^3] = \r
1524    circumcenter (set_of_list [u0;u1])`);\r
1525  (MATCH_MP_TAC XNHPWAB1);\r
1526  (EXISTS_TAC `1`);\r
1527  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);\r
1528 \r
1529  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);\r
1530  (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
1531  (REWRITE_TAC[IN] THEN STRIP_TAC);\r
1532  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1533  (EXISTS_TAC `2` THEN REWRITE_TAC[ARITH_RULE `1 <= 2`]);\r
1534  (REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`);\r
1535  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
1536  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1537  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1538  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
1539 \r
1540  (NEW_GOAL `!i j.  i < j /\ j <= 2\r
1541                      ==> hl (truncate_simplex i (vl:(real^3)list)) \r
1542                        < hl (truncate_simplex j vl)`);\r
1543 \r
1544  (MATCH_MP_TAC XNHPWAB4);\r
1545  (EXISTS_TAC `V:real^3->bool`);\r
1546  (ASM_REWRITE_TAC[IN]);\r
1547  (REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`);\r
1548  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
1549  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1550  (ASM_REWRITE_TAC[]);\r
1551  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1552  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
1553  (ASM_MESON_TAC[]);\r
1554  (NEW_GOAL `hl (truncate_simplex 1 (vl:(real^3)list)) < hl (truncate_simplex 2 vl)`);\r
1555  (FIRST_X_ASSUM MATCH_MP_TAC);\r
1556  (ARITH_TAC);\r
1557 \r
1558  (NEW_GOAL `truncate_simplex 2 vl = truncate_simplex 2 ul:(real^3)list`);\r
1559  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
1560  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1561  (MATCH_MP_TAC (REAL_ARITH `a < hl (truncate_simplex 2 (vl:(real^3)list)) /\ \r
1562    hl (truncate_simplex 2 vl) < b ==> a < b`));\r
1563  (ASM_REWRITE_TAC[]);\r
1564  (ASM_MESON_TAC[]);\r
1565  (REWRITE_TAC[set_of_list;Rogers.CIRCUMCENTER_2]);\r
1566  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; midpoint; IN; IN_ELIM_THM; AFFINE_HULL_3]);\r
1567  (REPEAT STRIP_TAC);\r
1568  (EXISTS_TAC `u' + v' * inv (&2)`);\r
1569  (EXISTS_TAC `v' * inv (&2)`);\r
1570  (EXISTS_TAC `&0`);\r
1571  (STRIP_TAC);\r
1572  (REWRITE_TAC[REAL_ARITH `(u' + v' * inv (&2)) + v' * inv (&2) + &0 = u' + v'`]);\r
1573  (ASM_REWRITE_TAC[]);\r
1574  (ASM_REWRITE_TAC[]);\r
1575  (VECTOR_ARITH_TAC);\r
1576 \r
1577  (REWRITE_TAC[VECTOR_ARITH `a % b % c dot d = a * b * (c dot d)`]);\r
1578  (ASM_REWRITE_TAC[]);\r
1579  (REWRITE_TAC[REAL_MUL_RZERO]);\r
1580 \r
1581 (* ========================================================================= *)\r
1582  (NEW_GOAL `norm (u0 - s:real^3) pow 2 = \r
1583              norm (s2 - s) pow 2 + norm (u0 - s2) pow 2`);\r
1584 \r
1585  (MATCH_MP_TAC PYTHAGORAS);\r
1586  (ASM_REWRITE_TAC[orthogonal]);\r
1587  (MATCH_MP_TAC MHFTTZN4);\r
1588  (EXISTS_TAC `V:real^3->bool`);\r
1589  (EXISTS_TAC `2`);\r
1590  (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);\r
1591  (EXPAND_TAC "vl" THEN DEL_TAC);\r
1592  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1593  (REPEAT STRIP_TAC);\r
1594  (ASM_REWRITE_TAC[]);\r
1595  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1596  (EXISTS_TAC `3`);\r
1597  (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);\r
1598 \r
1599  (UNDISCH_TAC `between s (s2,s3:real^3)`);\r
1600  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
1601  (REPEAT STRIP_TAC);\r
1602  (ONCE_REWRITE_TAC [GSYM IN]);\r
1603  (ONCE_ASM_REWRITE_TAC[]);\r
1604  (NEW_GOAL `convex (affine hull voronoi_list V \r
1605   (truncate_simplex 2 [u0; u1; u2; u3:real^3]))`);\r
1606  (MATCH_MP_TAC POLYHEDRON_IMP_CONVEX);\r
1607  (REWRITE_TAC[POLYHEDRON_AFFINE_HULL]);\r
1608  (UP_ASM_TAC THEN REWRITE_TAC[convex]);\r
1609  (DISCH_TAC);\r
1610  (FIRST_ASSUM MATCH_MP_TAC);\r
1611  (ASM_REWRITE_TAC[]);\r
1612  (REPEAT STRIP_TAC);\r
1613  (REWRITE_WITH `truncate_simplex 2 [u0; u1; u2; u3:real^3] = vl`);\r
1614  (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1615  (NEW_GOAL `affine hull (voronoi_list V vl) INTER \r
1616              affine hull (set_of_list vl) =\r
1617              {circumcenter (set_of_list (vl:(real^3)list))}`);\r
1618  (MATCH_MP_TAC Rogers.MHFTTZN3);\r
1619  (EXISTS_TAC `2`);\r
1620  (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);\r
1621  (EXPAND_TAC "vl" THEN DEL_TAC);\r
1622  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1623  (REPEAT STRIP_TAC);\r
1624  (ASM_REWRITE_TAC[]);\r
1625  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1626  (EXISTS_TAC `3`);\r
1627  (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);\r
1628  (UP_ASM_TAC THEN SET_TAC[]);\r
1629 \r
1630  (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);\r
1631  (ASM_MESON_TAC[]);\r
1632  (ASM_REWRITE_TAC[]);\r
1633  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);\r
1634  (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);\r
1635  (SET_TAC[]);\r
1636 \r
1637 (* ======================================================================== *)\r
1638 \r
1639  (NEW_GOAL `norm (u0 - (p' + m)) pow 2 <= norm (u0 - s2:real^3) pow 2`);\r
1640  (REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS; REAL_ABS_NORM;GSYM dist]);\r
1641  (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]);\r
1642  (NEW_GOAL \r
1643   `(?y. y IN {m, s2:real^3} /\\r
1644        (!x. x IN convex hull {m,s2} ==> norm (x - u0) <= norm (y - u0 )))`);\r
1645  (MATCH_MP_TAC SIMPLEX_FURTHEST_LE);\r
1646  (STRIP_TAC);\r
1647  (REWRITE_TAC[Geomdetail.FINITE6]);\r
1648  (SET_TAC[]);\r
1649  (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE `x IN {a, b} <=> x = b \/ x = a`] \r
1650    THEN REPEAT STRIP_TAC);\r
1651  (UP_ASM_TAC THEN REWRITE_TAC[ASSUME `y' = s2:real^3`]);\r
1652  (DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC);\r
1653  (UNDISCH_TAC `between p' (vec 0,n':real^3)`);\r
1654  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
1655  (REPEAT STRIP_TAC);\r
1656  (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN ASM_REWRITE_TAC[]);\r
1657  (REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; VECTOR_ARITH \r
1658   `a % (x - y) + y = b % y + a % x <=> ((b + a) - &1) % y = vec 0`]);\r
1659  (ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO]);\r
1660  (MATCH_MP_TAC (REAL_ARITH `(?s. a <= s /\ s <= b) ==> a <= b`));\r
1661 \r
1662  (EXISTS_TAC `norm (m - u0:real^3)`);\r
1663  (STRIP_TAC);\r
1664  (UP_ASM_TAC THEN REWRITE_TAC[ASSUME `y' = m:real^3`]);\r
1665  (DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC);\r
1666  (UNDISCH_TAC `between p' (vec 0,n':real^3)`);\r
1667  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
1668  (REPEAT STRIP_TAC);\r
1669  (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN ASM_REWRITE_TAC[]);\r
1670  (REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; VECTOR_ARITH \r
1671   `a % (x - y) + y = b % y + a % x <=> ((b + a) - &1) % y = vec 0`]);\r
1672  (ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO]);\r
1673 \r
1674  (MATCH_MP_TAC (REAL_ARITH `(?s. a <= s /\ s <= b) ==> a <= b`));\r
1675  (EXISTS_TAC `norm (s1 - u0:real^3)`);\r
1676  (STRIP_TAC);\r
1677  (REWRITE_TAC[GSYM dist]);\r
1678  (ONCE_REWRITE_TAC[DIST_SYM]);\r
1679  (UNDISCH_TAC `between m (u0,s1:real^3)`);\r
1680  (REWRITE_TAC[between]);\r
1681  (STRIP_TAC);\r
1682  (ASM_REWRITE_TAC[]);\r
1683  (REWRITE_TAC[REAL_ARITH `a <= a + b <=> &0 <= b`; DIST_POS_LE]);\r
1684  (NEW_GOAL `norm (s2 - u0:real^3) pow 2 = \r
1685    norm (s1 - u0) pow 2 + norm (s2 - s1) pow 2`);\r
1686  (MATCH_MP_TAC PYTHAGORAS);\r
1687 \r
1688  (ABBREV_TAC `sl = [u0;u1:real^3]`);\r
1689  (NEW_GOAL `s1:real^3 = circumcenter (set_of_list sl)`);\r
1690  (EXPAND_TAC "s1" THEN EXPAND_TAC "sl");\r
1691  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]);\r
1692  (MATCH_MP_TAC XNHPWAB1);\r
1693  (EXISTS_TAC `1`);\r
1694  (REWRITE_WITH `[u0; u1:real^3] = truncate_simplex 1 ul`);\r
1695  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
1696  (ASM_REWRITE_TAC[IN]);\r
1697  (STRIP_TAC);\r
1698  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1699  (EXISTS_TAC `3`);\r
1700  (ASM_MESON_TAC[ARITH_RULE `1 <= 3`]);\r
1701  (DEL_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
1702  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);\r
1703  (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
1704 \r
1705  (NEW_GOAL `!i j.  i < j /\ j <= 2\r
1706                      ==> hl (truncate_simplex i (vl:(real^3)list)) \r
1707                        < hl (truncate_simplex j vl)`);\r
1708 \r
1709  (MATCH_MP_TAC XNHPWAB4);\r
1710  (EXISTS_TAC `V:real^3->bool`);\r
1711  (ASM_REWRITE_TAC[IN]);\r
1712  (REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`);\r
1713  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
1714  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1715  (ASM_REWRITE_TAC[]);\r
1716  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1717  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
1718  (ASM_MESON_TAC[]);\r
1719  (NEW_GOAL `hl (truncate_simplex 1 (vl:(real^3)list)) < hl (truncate_simplex 2 vl)`);\r
1720  (FIRST_X_ASSUM MATCH_MP_TAC);\r
1721  (ARITH_TAC);\r
1722 \r
1723  (NEW_GOAL `truncate_simplex 2 vl = truncate_simplex 2 ul:(real^3)list`);\r
1724  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
1725  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1726  (MATCH_MP_TAC (REAL_ARITH `a < hl (truncate_simplex 2 (vl:(real^3)list)) /\ \r
1727    hl (truncate_simplex 2 vl) < b ==> a < b`));\r
1728  (ASM_REWRITE_TAC[]);\r
1729  (ASM_MESON_TAC[]);\r
1730 \r
1731  (REWRITE_TAC [ASSUME `s1:real^3 = circumcenter (set_of_list sl)`;orthogonal]);\r
1732  (ONCE_REWRITE_TAC[DOT_SYM]);\r
1733  (MATCH_MP_TAC MHFTTZN4);\r
1734 \r
1735  (EXISTS_TAC `V:real^3->bool`);\r
1736  (EXISTS_TAC `1`);\r
1737  (ASM_REWRITE_TAC[]);\r
1738  (STRIP_TAC);\r
1739  (REWRITE_WITH `sl:(real^3)list = truncate_simplex 1 ul`);\r
1740  (ASM_REWRITE_TAC[]);\r
1741  (EXPAND_TAC "sl");\r
1742  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
1743  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1744  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);\r
1745 \r
1746  (STRIP_TAC);\r
1747  (NEW_GOAL `affine hull (voronoi_list V vl) SUBSET \r
1748              affine hull (voronoi_list V (sl:(real^3)list))`);\r
1749  (MATCH_MP_TAC AFFINE_SUBSET_KY_LEMMA);\r
1750  (EXPAND_TAC "sl" THEN EXPAND_TAC "vl" THEN REWRITE_TAC\r
1751   [set_of_list; SET_RULE `x IN {a, b} <=> x = a \/ x = b`; \r
1752    SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`; \r
1753    VORONOI_LIST; VORONOI_SET;voronoi_closed; SUBSET;IN_INTERS]);\r
1754  (REWRITE_TAC[IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);\r
1755  (FIRST_ASSUM MATCH_MP_TAC);\r
1756  (EXISTS_TAC `v:real^3`);\r
1757  (ASM_REWRITE_TAC[]);\r
1758  (FIRST_ASSUM MATCH_MP_TAC);\r
1759  (EXISTS_TAC `v:real^3`);\r
1760  (ASM_REWRITE_TAC[]);\r
1761 \r
1762 \r
1763  (MATCH_MP_TAC (SET_RULE `(?C. C SUBSET B /\ s IN C ) ==> s IN B`));\r
1764  (EXISTS_TAC `affine hull voronoi_list V (vl:(real^3)list)`);\r
1765  (ASM_REWRITE_TAC[]);\r
1766 \r
1767  (NEW_GOAL `affine hull (voronoi_list V vl) INTER \r
1768              affine hull (set_of_list vl) =\r
1769              {circumcenter (set_of_list (vl:(real^3)list))}`);\r
1770  (MATCH_MP_TAC Rogers.MHFTTZN3);\r
1771  (EXISTS_TAC `2`);\r
1772  (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);\r
1773  (EXPAND_TAC "vl" THEN DEL_TAC);\r
1774  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1775  (REPEAT STRIP_TAC);\r
1776  (ASM_REWRITE_TAC[]);\r
1777  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1778  (EXISTS_TAC `3`);\r
1779  (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);\r
1780  (UP_ASM_TAC THEN SET_TAC[]);\r
1781 \r
1782  (EXPAND_TAC "sl" THEN REWRITE_TAC[set_of_list]);\r
1783  (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);\r
1784  (SET_TAC[IN]);\r
1785 \r
1786  (REWRITE_WITH `norm (s1 - u0:real^3) <= norm (s2 - u0) \r
1787   <=> norm (s1 - u0) pow 2 <= norm (s2 - u0) pow 2`);\r
1788  (MATCH_MP_TAC Collect_geom.POW2_COND);\r
1789  (REWRITE_TAC[NORM_POS_LE]);\r
1790  (UP_ASM_TAC THEN MATCH_MP_TAC \r
1791   (REAL_ARITH `(&0 <= c) ==> (a = b + c ==> b <= a)`));\r
1792  (REWRITE_TAC[REAL_LE_POW_2]);\r
1793 \r
1794 (* ==================================================================== *)\r
1795 \r
1796  (NEW_GOAL `norm (u0 - s:real^3) < norm (u0 - p)`);\r
1797  (MATCH_MP_TAC (REAL_ARITH `(?s. a <= s /\ s < b) ==> a < b`));\r
1798  (EXISTS_TAC `sqrt (&2)`);\r
1799  (STRIP_TAC);\r
1800  (REWRITE_TAC[GSYM dist]);\r
1801  (ASM_REAL_ARITH_TAC);\r
1802  (REWRITE_TAC[GSYM dist]);\r
1803  (UNDISCH_TAC `dist (u0,p:real^3) >= sqrt (&2)`);\r
1804  (MATCH_MP_TAC (REAL_ARITH `~(a = b) ==> (a >= b ==> b < a)`));\r
1805  (STRIP_TAC);\r
1806  (NEW_GOAL `~(p:real^3 IN B2)`);\r
1807  (ASM_SET_TAC[IN_DIFF]);\r
1808  (UP_ASM_TAC THEN EXPAND_TAC "B2" THEN REWRITE_TAC[IN;IN_ELIM_THM]);\r
1809  (ASM_REWRITE_TAC[HD; GSYM dist]);\r
1810  (ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]);\r
1811 \r
1812  (NEW_GOAL `norm (u0 - s:real^3) pow 2 < norm (u0 - p) pow 2`);\r
1813  (REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS; REAL_ABS_NORM]);\r
1814  (ASM_REWRITE_TAC[]);\r
1815 \r
1816  (NEW_GOAL `norm (s2 - s:real^3) pow 2 < norm ((p' + m) - p:real^3) pow 2`);\r
1817  (REWRITE_WITH `norm (s2 - s) pow 2 = \r
1818    norm (u0 - s:real^3) pow 2 - norm (u0 - s2) pow 2`);\r
1819  (ASM_REAL_ARITH_TAC);\r
1820  (REWRITE_WITH `norm ((p' + m) - p) pow 2 = \r
1821    norm (u0 - p:real^3) pow 2 - norm (u0 - (p' + m)) pow 2`);\r
1822  (ASM_REAL_ARITH_TAC);\r
1823  (ASM_REAL_ARITH_TAC);\r
1824 \r
1825 (* ======================================================================== *)\r
1826 \r
1827  (UNDISCH_TAC `p IN convex hull {u0, u1, u2, s:real^3}`);\r
1828  (REWRITE_TAC[CONVEX_HULL_4; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);\r
1829  (NEW_GOAL `(?m1. m1 IN convex hull {u0, u1, u2} /\ \r
1830                    between p (m1, s:real^3))`);\r
1831  (ASM_CASES_TAC `(u + v + w = &0)`);\r
1832  (NEW_GOAL `p = s:real^3`);\r
1833  (ASM_REWRITE_TAC[]);\r
1834  (REWRITE_WITH `u = &0 /\ v = &0 /\ w = &0 /\ z = &1`);\r
1835  (ASM_REAL_ARITH_TAC);\r
1836  (VECTOR_ARITH_TAC);\r
1837  (NEW_GOAL `F`);\r
1838  (NEW_GOAL `~(p:real^3 IN B2)`);\r
1839  (ASM_SET_TAC[IN_DIFF]);\r
1840  (UP_ASM_TAC THEN EXPAND_TAC "B2" THEN REWRITE_TAC[IN;IN_ELIM_THM]);\r
1841  (ASM_REWRITE_TAC[HD; GSYM dist]);\r
1842  (REWRITE_WITH `u = &0 /\ v = &0 /\ w = &0 /\ z = &1`);\r
1843  (ASM_REAL_ARITH_TAC);\r
1844  (REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_LID]);\r
1845  (ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]);\r
1846  (UP_ASM_TAC THEN MESON_TAC[]);\r
1847 \r
1848  (EXISTS_TAC `(u / (u + v + w)) % u0 + (v / (u + v + w)) % u1 + \r
1849                (w / (u + v + w)) % u2:real^3`);\r
1850  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;CONVEX_HULL_3; IN;\r
1851    IN_ELIM_THM] THEN REPEAT STRIP_TAC);\r
1852  (EXISTS_TAC `u / (u + v + w)`);\r
1853  (EXISTS_TAC `v / (u + v + w)`);\r
1854  (EXISTS_TAC `w / (u + v + w)`);\r
1855  (ASM_REWRITE_TAC[REAL_ARITH `a / x + b / x + c / x = (a + b + c) / x`]);\r
1856  (REPEAT STRIP_TAC);\r
1857  (MATCH_MP_TAC REAL_LE_DIV);\r
1858  (ASM_REAL_ARITH_TAC);\r
1859  (MATCH_MP_TAC REAL_LE_DIV);\r
1860  (ASM_REAL_ARITH_TAC);\r
1861  (MATCH_MP_TAC REAL_LE_DIV);\r
1862  (ASM_REAL_ARITH_TAC);\r
1863  (MATCH_MP_TAC REAL_DIV_REFL);\r
1864  (ASM_REAL_ARITH_TAC);\r
1865  (EXISTS_TAC `u + v + w:real`);\r
1866  (EXISTS_TAC `z:real`);\r
1867  (REPEAT STRIP_TAC);\r
1868  (ASM_REAL_ARITH_TAC);\r
1869  (ASM_REAL_ARITH_TAC);\r
1870  (ASM_REAL_ARITH_TAC);\r
1871  (ASM_REWRITE_TAC[]);\r
1872  (REWRITE_TAC[VECTOR_ARITH `a % (x/ a % u0 + y / a % u1 + z / a % u2) = \r
1873   (a / a) % (x % u0) + (a / a) % (y % u1) + (a / a) % (z % u2)`]);\r
1874  (REWRITE_WITH `(u + v + w) / (u + v + w) = &1`);\r
1875  (ASM_SIMP_TAC [REAL_DIV_REFL]);\r
1876  (REWRITE_TAC[VECTOR_MUL_LID]);\r
1877  (VECTOR_ARITH_TAC);\r
1878 \r
1879  (UP_ASM_TAC THEN REPEAT STRIP_TAC);\r
1880 \r
1881 (* ======================================================================== *)\r
1882 \r
1883  (NEW_GOAL `(?k. k <= &1 /\ &0 <= k /\\r
1884    projection (s2 - m) (p - m:real^3) = k % projection (s2 - m) (n - m))`);\r
1885  (MATCH_MP_TAC PARALLEL_PROJECTION);\r
1886  (ASM_REWRITE_TAC[]);\r
1887  (STRIP_TAC);\r
1888  (NEW_GOAL `s2 = m:real^3`);\r
1889  (ASM_REWRITE_TAC[]);\r
1890  (SWITCH_TAC THEN DEL_TAC);\r
1891 \r
1892  (NEW_GOAL `between s2 (u0, s1:real^3)`);\r
1893  (ASM_MESON_TAC[]);\r
1894  (NEW_GOAL `s2 IN affine hull {u0, s1:real^3}`);\r
1895  (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);\r
1896  (STRIP_TAC);\r
1897  (NEW_GOAL `convex hull {u0,s1:real^3} SUBSET affine hull {u0,s1}`);\r
1898  (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);\r
1899  (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);\r
1900 \r
1901  (NEW_GOAL `affine hull {u0,s1,s2} = affine hull {u0, s1:real^3}`);\r
1902  (MATCH_MP_TAC AFFINE_HULLS_EQ);\r
1903  (REWRITE_TAC[SUBSET; SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`]);\r
1904  (REPEAT STRIP_TAC);\r
1905  (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);\r
1906  (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]);\r
1907  (ASM_MESON_TAC[]);\r
1908  (UP_ASM_TAC);\r
1909  (REWRITE_TAC[SUBSET; SET_RULE `x IN {b,c} <=> x = b \/ x = c`]);\r
1910  (REPEAT STRIP_TAC);\r
1911  (ASM_REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);\r
1912  (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);\r
1913  (STRIP_TAC);\r
1914  (REAL_ARITH_TAC);\r
1915  (VECTOR_ARITH_TAC);\r
1916  (REWRITE_TAC[ASSUME `x = s1:real^3`;AFFINE_HULL_3;IN;IN_ELIM_THM]);\r
1917  (EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0`);\r
1918  (STRIP_TAC);\r
1919  (REAL_ARITH_TAC);\r
1920  (VECTOR_ARITH_TAC);\r
1921 \r
1922  (NEW_GOAL `aff_dim {u0,s1,s2:real^3} <= &1`);\r
1923  (ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL]);\r
1924  (ONCE_ASM_REWRITE_TAC[]);\r
1925  (ONCE_REWRITE_TAC[AFF_DIM_AFFINE_HULL]);\r
1926  (MATCH_MP_TAC (ARITH_RULE `(?x. x <= &1 /\ y <= x:int) ==> y <= &1`));\r
1927  (EXISTS_TAC `&(CARD {u0,s1:real^3}):int - &1`);\r
1928  (STRIP_TAC);\r
1929  (REWRITE_TAC[ARITH_RULE `a:int - &1 <= &1 <=> a <= &2`; INT_OF_NUM_LE]);\r
1930  (REWRITE_TAC[Geomdetail.CARD2]);\r
1931  (MATCH_MP_TAC AFF_DIM_LE_CARD);\r
1932  (REWRITE_TAC[Geomdetail.FINITE6]);\r
1933 \r
1934  (NEW_GOAL `aff_dim {u0,s1,s2:real^3} = &2`);\r
1935 \r
1936  (NEW_GOAL `vl:(real^3)list = truncate_simplex 2 ul`);\r
1937  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
1938  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1939  (REWRITE_WITH `aff_dim {u0,s1,s2:real^3} = \r
1940                  aff_dim {omega_list_n V vl j | j IN 0..2}`);\r
1941  (AP_TERM_TAC);\r
1942  (REWRITE_TAC[IN_NUMSEG_0]);\r
1943  (REWRITE_TAC[SET_EQ_LEMMA; \r
1944    SET_RULE `x IN {a,b,c} <=> (x = a \/ x = b \/ x = c)`; IN;IN_ELIM_THM]);\r
1945  (REPEAT STRIP_TAC);\r
1946  (EXISTS_TAC `0`);\r
1947  (REWRITE_TAC[ARITH_RULE `0 <= 2`; OMEGA_LIST_N]);\r
1948  (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);\r
1949  (ASM_REWRITE_TAC[]);\r
1950 \r
1951  (EXISTS_TAC `1`);\r
1952  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);\r
1953  (EXPAND_TAC "vl");\r
1954  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
1955  (DEL_TAC);\r
1956  (EXPAND_TAC "s1");\r
1957  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);\r
1958 \r
1959  (EXISTS_TAC `2`);\r
1960  (REWRITE_TAC[ARITH_RULE `2 <= 2`; ASSUME `x = s2:real^3`] THEN EXPAND_TAC "vl" THEN DEL_TAC);\r
1961  (EXPAND_TAC "s2");\r
1962  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);\r
1963  (REWRITE_TAC[set_of_list; OMEGA_LIST_TRUNCATE_2;\r
1964    OMEGA_LIST_TRUNCATE_2_NEW1]);\r
1965 \r
1966  (ASM_CASES_TAC `j = 0`);\r
1967  (DISJ1_TAC);\r
1968  (REWRITE_TAC[ASSUME `x:real^3 =  omega_list_n V vl j`; OMEGA_LIST_N; HD]);\r
1969  (EXPAND_TAC "vl");\r
1970  (REWRITE_TAC[ASSUME `j = 0`]);\r
1971  (REWRITE_TAC[OMEGA_LIST_N; HD]);\r
1972 \r
1973  (ASM_CASES_TAC `j = 1`);\r
1974  (DISJ2_TAC);\r
1975  (DISJ1_TAC);\r
1976  (ASM_REWRITE_TAC[]);\r
1977  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);\r
1978  (EXPAND_TAC "s1");\r
1979  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]);\r
1980 \r
1981  (ASM_CASES_TAC `j = 2`);\r
1982  (DISJ2_TAC);\r
1983  (DISJ2_TAC);\r
1984  (REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`]);\r
1985  (EXPAND_TAC "vl");\r
1986  (EXPAND_TAC "s2");\r
1987  (REWRITE_TAC[ASSUME `j = 2`; OMEGA_LIST_TRUNCATE_2; OMEGA_LIST_TRUNCATE_2_NEW1]);\r
1988  (SUBGOAL_THEN `F` MP_TAC);\r
1989  (ASM_ARITH_TAC);\r
1990  (MESON_TAC[]);\r
1991 \r
1992  (MATCH_MP_TAC XNHPWAB3);\r
1993  (ASM_REWRITE_TAC[IN]);\r
1994  STRIP_TAC;\r
1995  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
1996  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
1997  (ASM_MESON_TAC[]);\r
1998  (ASM_MESON_TAC[]);\r
1999  (ASM_ARITH_TAC);\r
2000 \r
2001  (NEW_GOAL `?h. h <= &1 /\ &0 <= h /\\r
2002    projection (s2 - m1:real^3) (p - m1) = h % projection (s2 - m1) (s - m1)`);\r
2003  (MATCH_MP_TAC PARALLEL_PROJECTION);\r
2004  (ASM_REWRITE_TAC[]);\r
2005  (STRIP_TAC);\r
2006  (NEW_GOAL `s2 = m1:real^3`);\r
2007  (ASM_REWRITE_TAC[]);\r
2008  (SWITCH_TAC THEN DEL_TAC);\r
2009  (NEW_GOAL `between p (s2, s:real^3)`);\r
2010  (ASM_MESON_TAC[]);\r
2011  (NEW_GOAL `between p (s3, s2:real^3)`);\r
2012  (MATCH_MP_TAC BETWEEN_TRANS);\r
2013  (EXISTS_TAC `s:real^3`);\r
2014  (STRIP_TAC);\r
2015  (ASM_MESON_TAC[BETWEEN_SYM]);\r
2016  (ASM_MESON_TAC[BETWEEN_SYM]);\r
2017 \r
2018  (NEW_GOAL `p:real^3 IN B5`);\r
2019  (EXPAND_TAC "B5");\r
2020  (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);\r
2021  (EXPAND_TAC "s2");\r
2022  (EXPAND_TAC "s3");\r
2023  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
2024  (MESON_TAC[SET_RULE `{a,b} = {b, a}`]);\r
2025  (NEW_GOAL `~(p:real^3 IN B5)`);\r
2026  (ASM_SET_TAC[IN_DIFF]);\r
2027  (ASM_MESON_TAC[]);\r
2028 \r
2029  (FIRST_X_ASSUM CHOOSE_TAC);\r
2030  (FIRST_X_ASSUM CHOOSE_TAC);\r
2031 \r
2032  (NEW_GOAL `projection (s2 - m1) (s - m1) = s - s2:real^3`);\r
2033  (REWRITE_TAC[projection; VECTOR_ARITH `a - b - x % (d - b) = a - d \r
2034   <=> (&1 - x) % (d - b:real^3) = vec 0`]);\r
2035  (REWRITE_WITH `&1 - ((s - m1) dot (s2 - m1:real^3)) / ((s2 - m1) dot (s2 - m1)) = &0`);\r
2036  (REWRITE_TAC[REAL_ARITH `&1 - a = &0 <=> a = &1`]);\r
2037  (REWRITE_WITH `((s - m1) dot (s2 - m1)) / ((s2 - m1) dot (s2 - m1)) = &1 \r
2038   <=> ((s - m1) dot (s2 - m1)) = &1 * ((s2 - m1) dot (s2 - m1:real^3))`);\r
2039  (MATCH_MP_TAC REAL_EQ_LDIV_EQ);\r
2040  (REWRITE_TAC[GSYM NORM_POW_2; GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT;\r
2041    NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);\r
2042  (STRIP_TAC);\r
2043 \r
2044  (NEW_GOAL `between p (s2, s:real^3)`);\r
2045  (ASM_MESON_TAC[]);\r
2046  (NEW_GOAL `between p (s3, s2:real^3)`);\r
2047  (MATCH_MP_TAC BETWEEN_TRANS);\r
2048  (EXISTS_TAC `s:real^3`);\r
2049  (STRIP_TAC);\r
2050  (ASM_MESON_TAC[BETWEEN_SYM]);\r
2051  (ASM_MESON_TAC[BETWEEN_SYM]);\r
2052 \r
2053  (NEW_GOAL `p:real^3 IN B5`);\r
2054  (EXPAND_TAC "B5");\r
2055  (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]);\r
2056  (EXPAND_TAC "s2");\r
2057  (EXPAND_TAC "s3");\r
2058  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
2059  (MESON_TAC[SET_RULE `{a,b} = {b, a}`]);\r
2060  (NEW_GOAL `~(p:real^3 IN B5)`);\r
2061  (ASM_SET_TAC[IN_DIFF]);\r
2062  (ASM_MESON_TAC[]);\r
2063  (REWRITE_TAC[REAL_MUL_LID]);\r
2064  (ONCE_REWRITE_TAC[REAL_ARITH `a = b <=> a - b = &0`]);\r
2065  (REWRITE_TAC[VECTOR_ARITH \r
2066   `(s - m1) dot r - (s2 - m1) dot r = (s - s2) dot r:real^3`]);\r
2067  (REWRITE_WITH `(s - s2) dot (s2 - m1) = --((s - s2) dot (m1 - s2:real^3))`);\r
2068  (VECTOR_ARITH_TAC);\r
2069  (ONCE_REWRITE_TAC[REAL_ARITH `-- a = &0 <=> a = &0`]);\r
2070  (UNDISCH_TAC `between s (s2,s3:real^3)`);\r
2071  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;IN;IN_ELIM_THM; CONVEX_HULL_2]);\r
2072  (REPEAT STRIP_TAC);\r
2073  (REWRITE_TAC[ASSUME `s = u' % s2 + v' % s3:real^3`]);\r
2074  (REWRITE_WITH `(u' % s2 + v' % s3) - s2:real^3 = \r
2075   (u' % s2 + v' % s3) - (u' + v') % s2`);\r
2076  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
2077  (REWRITE_TAC[VECTOR_ARITH \r
2078   `(u' % s2 + v' % s3) - (u' + v') % s2 = v' % (s3 - s2)`; DOT_LMUL]);\r
2079  (REWRITE_WITH `(s3 - s2) dot (m1 - s2:real^3) = &0`);\r
2080  (ASM_REWRITE_TAC[]);\r
2081 \r
2082 \r
2083 \r
2084  (MATCH_MP_TAC MHFTTZN4);\r
2085  (EXISTS_TAC `V:real^3->bool`);\r
2086  (EXISTS_TAC `2`);\r
2087  (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);\r
2088  (EXPAND_TAC "vl" THEN DEL_TAC);\r
2089  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
2090  (REPEAT STRIP_TAC);\r
2091  (ASM_REWRITE_TAC[]);\r
2092  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
2093  (EXISTS_TAC `3`);\r
2094  (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);\r
2095  (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);\r
2096  (ONCE_ASM_REWRITE_TAC[]);\r
2097 \r
2098  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;   \r
2099    TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);\r
2100  (UNDISCH_TAC `m1 IN convex hull {u0, u1, u2:real^3}`);\r
2101  (NEW_GOAL `convex hull {u0, u1, u2:real^3} SUBSET \r
2102              affine hull {u0, u1, u2:real^3}`);\r
2103  (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);\r
2104  (UP_ASM_TAC THEN SET_TAC[]);\r
2105  (REAL_ARITH_TAC);\r
2106  (VECTOR_ARITH_TAC);\r
2107  (ABBREV_TAC `M = projection (s2 - m1) (p - m1:real^3)`);\r
2108  (ABBREV_TAC `N = projection (s2 - m) (p - m:real^3)`);\r
2109  (NEW_GOAL `M = N:real^3`);\r
2110  (NEW_GOAL `?r. N = r % M:real^3`);\r
2111  (ASM_REWRITE_TAC[]);\r
2112  (NEW_GOAL `projection (s2 - m) (n - m:real^3) = n - s2`);\r
2113  (REWRITE_TAC[projection_proj_point; ASSUME `n' = s2 - m:real^3`;\r
2114    ASSUME `proj_point (s2 - m) (n - m) = n':real^3`]);\r
2115  (VECTOR_ARITH_TAC);\r
2116  (REWRITE_WITH `circumcenter (set_of_list vl) = s2:real^3`);\r
2117  (ASM_MESON_TAC[]);\r
2118  (REWRITE_TAC[ASSUME `projection (s2 - m) (n - m) = n - s2:real^3`]);\r
2119  (UNDISCH_TAC `between n (s2,s3:real^3)`);\r
2120  (UNDISCH_TAC `between s (s2,s3:real^3)`);\r
2121  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
2122  (REPEAT STRIP_TAC);\r
2123 \r
2124  (REWRITE_TAC[ASSUME `n = u'' % s2 + v'' % s3:real^3`; \r
2125                ASSUME `s = u' % s2 + v' % s3:real^3`]);\r
2126  (REWRITE_WITH `(u' % s2 + v' % s3) - s2:real^3  \r
2127                   = (u' % s2 + v' % s3) - (u' + v') % s2 /\ \r
2128                  (u'' % s2 + v'' % s3) - s2  \r
2129                   = (u'' % s2 + v'' % s3) - (u'' + v'') % s2`);\r
2130  (ASM_REWRITE_TAC[VECTOR_MUL_LID]);\r
2131  (REWRITE_TAC[VECTOR_ARITH `(u % s + v % r) - (u + v) % s = v % (r - s)`]);\r
2132  (REWRITE_TAC[VECTOR_MUL_ASSOC]);\r
2133  (REWRITE_TAC[VECTOR_ARITH `a % x = b % x <=> (a - b) % x = vec 0`]);\r
2134  (REWRITE_TAC[REAL_ARITH `(r * h) * v' = r * (h * v')`]);\r
2135  (ASM_CASES_TAC `h * v' = &0`);\r
2136  (NEW_GOAL `F`);\r
2137  (ASM_CASES_TAC `h = &0`);\r
2138  (NEW_GOAL `M:real^3 = vec 0`);\r
2139  (ASM_REWRITE_TAC[VECTOR_MUL_LZERO]);\r
2140  (UP_ASM_TAC THEN EXPAND_TAC "M" THEN REWRITE_TAC[projection]);\r
2141  (ABBREV_TAC `kts = ((p - m1) dot (s2 - m1)) / ((s2 - m1) dot (s2 - m1:real^3))`);\r
2142  (REWRITE_TAC [VECTOR_ARITH `a - p - c = vec 0 <=> a = p + c`]);\r
2143  (STRIP_TAC);\r
2144  (NEW_GOAL `p IN affine hull {u0,u1,u2:real^3}`);\r
2145  (REWRITE_TAC[ASSUME `p = m1 + kts % (s2 - m1:real^3)`]);\r
2146  (MATCH_MP_TAC TRANSLATE_AFFINE_KY_LEMMA1);\r
2147  (REWRITE_TAC[MESON[] `A /\ B /\ A <=> A /\ B`]);\r
2148  (STRIP_TAC);\r
2149  (NEW_GOAL `convex hull {u0,u1,u2:real^3} SUBSET affine hull {u0, u1, u2}`);\r
2150  (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);\r
2151  (UNDISCH_TAC `m1 IN convex hull {u0, u1, u2:real^3}`);\r
2152  (UP_ASM_TAC THEN SET_TAC[]);\r
2153  (ASM_REWRITE_TAC[]);\r
2154  (EXPAND_TAC "vl");\r
2155  (REWRITE_TAC[set_of_list]);\r
2156  (MATCH_MP_TAC Rogers.OAPVION1);\r
2157  (STRIP_TAC);\r
2158  (SET_TAC[]);\r
2159  (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);\r
2160  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
2161  (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);\r
2162 \r
2163  (EXISTS_TAC `V:real^3->bool`);\r
2164  (EXISTS_TAC `2`);\r
2165  (ASM_REWRITE_TAC[]);\r
2166  (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);\r
2167  (ASM_REWRITE_TAC[]);\r
2168  (EXPAND_TAC "vl");\r
2169  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
2170  (MATCH_MP_TAC Packing3. TRUNCATE_SIMPLEX_BARV);\r
2171  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
2172 \r
2173  (NEW_GOAL `~(p:real^3 IN B6)`);\r
2174  (ASM_SET_TAC[IN_DIFF]);\r
2175  (UP_ASM_TAC THEN EXPAND_TAC "B6");\r
2176  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;HD;TL]);\r
2177  (ASM_REWRITE_TAC[]);\r
2178  (NEW_GOAL `v' = &0`);\r
2179  (ASM_MESON_TAC[REAL_ENTIRE]);\r
2180  (NEW_GOAL `s = s2:real^3`);\r
2181  (ASM_REWRITE_TAC[]);\r
2182  (REWRITE_WITH `u' = &1`);\r
2183  (ASM_REAL_ARITH_TAC);\r
2184  (REWRITE_TAC[VECTOR_MUL_LID]);\r
2185  (VECTOR_ARITH_TAC);\r
2186 \r
2187  (NEW_GOAL `!w. w IN {u0,u1,u2:real^3} ==> \r
2188    radV {u0,u1,u2} = dist (circumcenter {u0,u1,u2},w)`);\r
2189  (MATCH_MP_TAC Rogers.OAPVION2);\r
2190  (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);\r
2191  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
2192  (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);\r
2193  (EXISTS_TAC `V:real^3->bool`);\r
2194  (EXISTS_TAC `2`);\r
2195  (ASM_REWRITE_TAC[]);\r
2196  (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);\r
2197  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
2198  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
2199  (EXISTS_TAC `3`);\r
2200  (ASM_REWRITE_TAC[]);\r
2201  (ARITH_TAC);\r
2202 \r
2203  (NEW_GOAL `hl (truncate_simplex 2 (ul:(real^3)list)) = dist (s2, u0:real^3)`);\r
2204  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;  \r
2205    TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list; HL]);\r
2206  (REWRITE_WITH `s2 = circumcenter {u0,u1,u2:real^3}`);\r
2207  (ASM_REWRITE_TAC[]);\r
2208  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
2209  (FIRST_ASSUM MATCH_MP_TAC);\r
2210  (SET_TAC[]);\r
2211  (NEW_GOAL `hl (truncate_simplex 2 (ul:(real^3)list)) = sqrt (&2)`);\r
2212  (ONCE_ASM_REWRITE_TAC[]);\r
2213  (REWRITE_TAC[GSYM (ASSUME `s = s2:real^3`)]);\r
2214  (ONCE_REWRITE_TAC[DIST_SYM]);\r
2215  (ASM_REWRITE_TAC[]);\r
2216  (ASM_REAL_ARITH_TAC);\r
2217  (UP_ASM_TAC THEN MESON_TAC[]);\r
2218  (EXISTS_TAC `(k * v'') / (h * v')`);\r
2219  (REWRITE_TAC[REAL_ARITH `k * v'' - (k * v'') / (h * v') * h * v' = \r
2220                            (k * v'') * (&1 - (h * v') / (h * v'))`]);\r
2221  (REWRITE_WITH `(h * v') / (h * v') = &1`);\r
2222  (MATCH_MP_TAC REAL_DIV_REFL);\r
2223  (ASM_REWRITE_TAC[]);\r
2224  (REWRITE_TAC[REAL_SUB_REFL;REAL_MUL_RZERO; VECTOR_MUL_LZERO]);\r
2225  (FIRST_X_ASSUM CHOOSE_TAC);\r
2226 \r
2227  (NEW_GOAL `r = &1`);\r
2228  (ASM_CASES_TAC `r = &1`);\r
2229  (ASM_REWRITE_TAC[]);\r
2230  (NEW_GOAL `p IN affine hull {u0,u1,u2:real^3}`);\r
2231  (MATCH_MP_TAC IN_AFFINE_HULL_KY_LEMMA3_alt);\r
2232  (EXISTS_TAC `M:real^3`);\r
2233  (EXISTS_TAC `r:real`);\r
2234  (REWRITE_WITH `p - M = (m1:real^3) + proj_point (s2 - m1) (p - m1)`);\r
2235  (EXPAND_TAC "M" THEN REWRITE_TAC[proj_point]);\r
2236  (VECTOR_ARITH_TAC);\r
2237  (REWRITE_WITH `p - r % M =(m:real^3) + proj_point (s2 - m) (p - m)`);\r
2238  (REWRITE_TAC[GSYM (ASSUME `N = r % M:real^3`)]);\r
2239  (EXPAND_TAC "N" THEN REWRITE_TAC[proj_point]);\r
2240  (VECTOR_ARITH_TAC);\r
2241  (REWRITE_TAC[PRO_EXP]);\r
2242 \r
2243  (REPEAT STRIP_TAC);\r
2244  (MATCH_MP_TAC TRANSLATE_AFFINE_KY_LEMMA1 );\r
2245  (REWRITE_TAC[MESON[] `A /\ B /\ A <=> A /\ B`]);\r
2246  (REPEAT STRIP_TAC);\r
2247 \r
2248  (NEW_GOAL `convex hull {u0,u1,u2} SUBSET  affine hull {u0,u1,u2:real^3}`);\r
2249  (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);\r
2250  (UP_ASM_TAC THEN UNDISCH_TAC `m1:real^3 IN convex hull {u0,u1,u2}` THEN  \r
2251    SET_TAC[]);\r
2252  (ASM_REWRITE_TAC[]);\r
2253  (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);\r
2254  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
2255  (MATCH_MP_TAC Rogers.BARV_CIRCUMCENTER_EXISTS);\r
2256  (EXISTS_TAC `V:real^3->bool`);\r
2257  (EXISTS_TAC `2`);\r
2258  (ASM_REWRITE_TAC[]);\r
2259  (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);\r
2260  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
2261  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
2262  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
2263  (MATCH_MP_TAC TRANSLATE_AFFINE_KY_LEMMA1);\r
2264 \r
2265  (REWRITE_TAC[MESON[] `A/\B/\A <=> A/\B`]);\r
2266  (STRIP_TAC);\r
2267 \r
2268  (MATCH_MP_TAC IN_AFFINE_HULL_3_KY_LEMMA2);\r
2269  (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `s1:real^3`);\r
2270  (REPEAT STRIP_TAC);\r
2271  (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);\r
2272  (SET_TAC[]);\r
2273 \r
2274  (MATCH_MP_TAC (SET_RULE`(?s. s SUBSET b /\ a IN s) ==> a IN b`));\r
2275  (EXISTS_TAC `convex hull {u0, u1,u2:real^3}`);\r
2276  (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);\r
2277  (MATCH_MP_TAC (SET_RULE`(?s. s SUBSET b /\ a IN s) ==> a IN b`));\r
2278  (EXISTS_TAC `convex hull {u0, u1:real^3}`);\r
2279  (STRIP_TAC);   \r
2280  (MATCH_MP_TAC CONVEX_HULL_SUBSET);\r
2281  (SET_TAC[]);\r
2282 \r
2283  (REWRITE_WITH `{u0, u1:real^3} = set_of_list [u0;u1]`);\r
2284  (REWRITE_TAC[set_of_list]);\r
2285  (EXPAND_TAC "s1");\r
2286  (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 = \r
2287                  omega_list V [u0;u1:real^3]`);\r
2288  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]);\r
2289  (MATCH_MP_TAC XNHPWAB2);\r
2290  (EXISTS_TAC `1`);\r
2291  (REPEAT STRIP_TAC);\r
2292  (ASM_REWRITE_TAC[]);\r
2293 \r
2294  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`);\r
2295  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
2296  (REWRITE_TAC[IN]);\r
2297  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
2298  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);\r
2299 \r
2300  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);\r
2301  (EXPAND_TAC "vl");\r
2302  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
2303  (MATCH_MP_TAC (REAL_ARITH `(?s. s < b /\ a <= s) ==> a < b`));\r
2304  (EXISTS_TAC `hl (vl:(real^3)list)`);\r
2305  (STRIP_TAC);\r
2306  (REWRITE_WITH `vl = truncate_simplex 2 (ul:(real^3)list)`);\r
2307  (ASM_REWRITE_TAC[]);\r
2308  (EXPAND_TAC "vl");\r
2309  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
2310  (ASM_REWRITE_TAC[]);\r
2311  (MATCH_MP_TAC Rogers.HL_DECREASE);\r
2312  (EXISTS_TAC `V:real^3->bool`);\r
2313  (EXISTS_TAC `2`);\r
2314  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`;IN]);\r
2315  (REWRITE_WITH `vl = truncate_simplex 2 (ul:(real^3)list)`);\r
2316  (ASM_REWRITE_TAC[]);\r
2317  (EXPAND_TAC "vl");\r
2318  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
2319  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
2320  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
2321 \r
2322  (ASM_REWRITE_TAC[]);\r
2323 \r
2324  (ASM_REWRITE_TAC[]);\r
2325  (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);\r
2326  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
2327  (MATCH_MP_TAC Rogers.BARV_CIRCUMCENTER_EXISTS);\r
2328  (EXISTS_TAC `V:real^3->bool`);\r
2329  (EXISTS_TAC `2`);\r
2330  (ASM_REWRITE_TAC[]);\r
2331  (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`);\r
2332  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
2333  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
2334  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
2335  (ASM_MESON_TAC[]);\r
2336  (NEW_GOAL `~(p:real^3 IN B6)`);\r
2337  (ASM_SET_TAC[IN_DIFF]);\r
2338  (UP_ASM_TAC THEN EXPAND_TAC "B6");\r
2339  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;HD;TL]);\r
2340  (STRIP_TAC);\r
2341  (NEW_GOAL `F`);\r
2342  (ASM_MESON_TAC[]);\r
2343  (ASM_MESON_TAC[]);\r
2344  (REWRITE_TAC[ASSUME `N = r % M:real^3`; ASSUME `r = &1`]);\r
2345  (VECTOR_ARITH_TAC);\r
2346 \r
2347 \r
2348 \r
2349  (NEW_GOAL `norm (M:real^3) <= norm (s2 - s:real^3)`);\r
2350  (REWRITE_WITH `norm (s2 - s:real^3) = norm (projection (s2 - m1) (s - m1))`);\r
2351  (REWRITE_WITH `norm (s2 - s:real^3) = norm (s - s2)`);\r
2352  (NORM_ARITH_TAC);\r
2353  (AP_TERM_TAC);\r
2354  (ASM_MESON_TAC[]);\r
2355  (REWRITE_TAC[ASSUME \r
2356   `h <= &1 /\ &0 <= h /\ M = h % projection (s2 - m1) (s - m1:real^3)`]);\r
2357  (REWRITE_TAC[NORM_MUL;REAL_ARITH `a * b <= b <=> &0 <= b * (&1 - a)`]);\r
2358  (MATCH_MP_TAC REAL_LE_MUL);\r
2359  (REWRITE_TAC[NORM_POS_LE; REAL_ARITH `&0 <= a - b <=> b <= a`]);\r
2360  (REWRITE_WITH `abs h = h`);\r
2361  (REWRITE_TAC[REAL_ABS_REFL]);\r
2362  (ASM_REWRITE_TAC[]);\r
2363  (ASM_REWRITE_TAC[]);\r
2364  (NEW_GOAL `norm (s2 - s:real^3) < norm (N:real^3) `);\r
2365  (REWRITE_WITH `norm (s2 - s:real^3) < norm (N:real^3) <=> \r
2366                  norm (s2 - s) pow 2 < norm (N:real^3) pow 2`);\r
2367  (MATCH_MP_TAC Pack1.bp_bdt);\r
2368  (REWRITE_TAC[NORM_POS_LE]);\r
2369  (REWRITE_WITH `norm (N:real^3) = norm ((p' + m) - p:real^3)`);\r
2370 \r
2371  (REWRITE_TAC[GSYM (ASSUME `projection (s2 - m) (p - m) = N:real^3`)]);\r
2372  (REWRITE_TAC[projection_proj_point]);\r
2373  (REWRITE_TAC[ASSUME `proj_point (s2 - m) (p - m) = p':real^3`]);\r
2374  (NORM_ARITH_TAC);\r
2375  (ASM_REWRITE_TAC[]);\r
2376  (NEW_GOAL `norm (s2 - s:real^3) < norm (M:real^3)`);\r
2377  (ASM_MESON_TAC[]);\r
2378  (ASM_REAL_ARITH_TAC);\r
2379  (SET_TAC[]);\r
2380 \r
2381 (* ======================================================================= *)\r
2382  (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 0`);\r
2383  (REPEAT STRIP_TAC);\r
2384  (NEW_GOAL `~(y = 4 \/ y = 1 \/ y = 2 \/ y = 3)`);\r
2385  (ASM_SIMP_TAC[]);\r
2386  (ASM_ARITH_TAC);\r
2387  (NEW_GOAL `i = 0`);\r
2388  (FIRST_ASSUM MATCH_MP_TAC);\r
2389  (ASM_SIMP_TAC[]);\r
2390  (REWRITE_TAC[ASSUME `i = 0`]);\r
2391  (ASM_REWRITE_TAC[]);\r
2392 \r
2393 (* ====================================================================== *)\r
2394 \r
2395  (NEW_GOAL `dist (u0, p:real^3) < sqrt (&2)`);\r
2396  (UP_ASM_TAC THEN REAL_ARITH_TAC);\r
2397  (ASM_CASES_TAC `~(p IN rcone_gt (HD (ul:(real^3)list)) (HD (TL ul))\r
2398                (hl (truncate_simplex 1 ul) / sqrt (&2))) `);\r
2399  (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> \r
2400                 ~ (y = 4 \/ y = 0 \/ y = 2 \/ y = 3)`);\r
2401  (REPEAT STRIP_TAC);\r
2402  (NEW_GOAL `mcell 4 V ul = {}`);\r
2403  (SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);\r
2404  (COND_CASES_TAC);\r
2405  (NEW_GOAL `F`);\r
2406  (ASM_MESON_TAC[]);\r
2407  (ASM_MESON_TAC[]);\r
2408  (REFL_TAC);\r
2409  (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 4`]);\r
2410  (REWRITE_TAC[ASSUME `mcell 4 V ul = {}`]);\r
2411  (SET_TAC[]);\r
2412  (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 0`;\r
2413    MCELL_EXPLICIT;mcell0]);\r
2414  (STRIP_TAC);\r
2415  (NEW_GOAL `~(p:real^3 IN ball (HD ul,sqrt (&2)))`);\r
2416  (ASM_SET_TAC[IN_DIFF]);\r
2417  (UP_ASM_TAC THEN ASM_REWRITE_TAC[HD;IN;ball;IN_ELIM_THM]);\r
2418 \r
2419  (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 2`;\r
2420    MCELL_EXPLICIT;mcell2]);\r
2421  (COND_CASES_TAC);\r
2422  (LET_TAC);\r
2423  (REWRITE_TAC[IN_INTER]);\r
2424  (REPEAT STRIP_TAC);\r
2425  (NEW_GOAL `p:real^3 IN rcone_gt (HD ul) (HD (TL ul)) a`);\r
2426  (REWRITE_TAC[RCONE_GT_GE;IN_DIFF]);\r
2427  (ASM_REWRITE_TAC[]);\r
2428  (REWRITE_TAC[HD;TL;IN;IN_ELIM_THM]);\r
2429  (STRIP_TAC);\r
2430  (NEW_GOAL `~(p:real^3 IN B3)`);\r
2431  (ASM_SET_TAC[IN_DIFF]);\r
2432  (UP_ASM_TAC THEN EXPAND_TAC "B3" THEN REWRITE_TAC[rcone_eq;rconesgn]);\r
2433  (ASM_REWRITE_TAC[HD;TL;IN;IN_ELIM_THM;dist]);\r
2434  (ASM_MESON_TAC[]);\r
2435  (SET_TAC[]);\r
2436 \r
2437 (* ======================================================================= *)\r
2438 \r
2439  (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 3`;\r
2440    MCELL_EXPLICIT;mcell3]);\r
2441  (COND_CASES_TAC);\r
2442 \r
2443  (NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\\r
2444                   dist (u0,s) = sqrt (&2) /\\r
2445                   mxi V ul = s:real^3)`);\r
2446  (MATCH_MP_TAC MXI_EXPLICIT_OLD);\r
2447  (ASM_REWRITE_TAC[]);\r
2448  (FIRST_X_ASSUM CHOOSE_TAC);\r
2449 \r
2450  (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC);\r
2451  (UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);\r
2452  (REWRITE_TAC[SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);\r
2453  (STRIP_TAC);\r
2454 \r
2455  (SUBGOAL_THEN `p:real^3 IN rogers V ul` MP_TAC);\r
2456  (ASM_SET_TAC[IN_DIFF]);\r
2457  (ASM_SIMP_TAC[ROGERS_EXPLICIT; HD]);\r
2458  (ABBREV_TAC `s1 = omega_list_n V [u0; u1; u2; u3:real^3] 1`);\r
2459  (ABBREV_TAC `s2 = omega_list_n V [u0; u1; u2; u3:real^3] 2`);\r
2460  (ABBREV_TAC `s3 = omega_list_n V [u0; u1; u2; u3:real^3] 3`);\r
2461  (STRIP_TAC);\r
2462 \r
2463  (ABBREV_TAC  `vl = [u0;u1;u2:real^3]`);\r
2464  (NEW_GOAL `vl = truncate_simplex 2 ul:(real^3)list`);\r
2465  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2] THEN EXPAND_TAC "vl");\r
2466  (NEW_GOAL `barV V 2 vl`);\r
2467  (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
2468  (EXISTS_TAC `3` THEN ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);\r
2469  (NEW_GOAL `LENGTH (vl:(real^3)list) = 3 /\ CARD {u0,u1,u2:real^3} = 3`);\r
2470  (REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list vl`);\r
2471  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
2472  (REWRITE_TAC[ARITH_RULE `3 = 2 + 1`]);\r
2473  (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);\r
2474  (EXISTS_TAC `V:real^3->bool`);\r
2475  (ASM_REWRITE_TAC[]);\r
2476 \r
2477  (NEW_GOAL `s2:real^3 = omega_list V vl`);\r
2478  (EXPAND_TAC "s2" THEN EXPAND_TAC "vl"  THEN \r
2479    REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
2480  (MESON_TAC[OMEGA_LIST_TRUNCATE_2]);\r
2481 \r
2482  (NEW_GOAL `s2 = circumcenter {u0,u1,u2:real^3}`);\r
2483  (REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list vl`);\r
2484  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
2485  (REWRITE_TAC[ASSUME `s2 = omega_list V vl`]);\r
2486  (MATCH_MP_TAC Rogers.XNHPWAB1);\r
2487  (EXISTS_TAC `2` THEN REWRITE_TAC[IN]);\r
2488  (ASM_REWRITE_TAC[]);\r
2489  (ASM_MESON_TAC[]);\r
2490 \r
2491  (NEW_GOAL `dist (s2,u0:real^3) = hl (truncate_simplex 2 (ul:(real^3)list))`);\r
2492  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
2493  (REWRITE_TAC[GSYM (ASSUME `vl:(real^3)list = truncate_simplex 2 ul`)]);\r
2494  (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);\r
2495  (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);\r
2496  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
2497  (REWRITE_WITH `u0:real^3 = HD vl`);\r
2498  (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);\r
2499  (MATCH_MP_TAC Rogers.HL_EQ_DIST0);\r
2500  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);\r
2501  (ASM_REWRITE_TAC[]);\r
2502 \r
2503  (NEW_GOAL `~(s = s2:real^3)`);\r
2504  (STRIP_TAC);\r
2505  (NEW_GOAL `dist (u0,s:real^3) < sqrt (&2)`);\r
2506  (ONCE_REWRITE_TAC[DIST_SYM]);\r
2507  (REWRITE_TAC[ASSUME `s = s2:real^3`]);\r
2508  (ASM_MESON_TAC[]);\r
2509  (ASM_REAL_ARITH_TAC);\r
2510 \r
2511  (NEW_GOAL `(s2:real^3) IN voronoi_list V vl`);\r
2512  (SIMP_TAC[ASSUME `s2 = omega_list V vl`]);\r
2513  (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);\r
2514  (EXISTS_TAC `2`);\r
2515  (ASM_REWRITE_TAC[]);\r
2516 \r
2517  (NEW_GOAL `(s3:real^3) IN voronoi_list V ul`);\r
2518  (REWRITE_WITH `s3 = omega_list V ul`);\r
2519  (EXPAND_TAC "s3" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; OMEGA_LIST]);\r
2520  (REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) - 1 = 3`]);\r
2521  (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);\r
2522  (EXISTS_TAC `3`);\r
2523  (ASM_REWRITE_TAC[]);\r
2524 \r
2525  (NEW_GOAL `(s3:real^3) IN voronoi_list V vl`);\r
2526  (MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET A) ==> a IN A`));\r
2527  (EXISTS_TAC `voronoi_list V ul`);\r
2528  (STRIP_TAC);\r
2529  (ASM_REWRITE_TAC[]);\r
2530  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
2531  (REWRITE_TAC[VORONOI_LIST;VORONOI_SET;voronoi_closed;set_of_list; \r
2532    SUBSET; IN_INTERS]);\r
2533  (ONCE_REWRITE_TAC[IN]);\r
2534  (REWRITE_TAC[IN_ELIM_THM]);\r
2535  (REPEAT STRIP_TAC);\r
2536  (FIRST_ASSUM MATCH_MP_TAC);\r
2537  (EXISTS_TAC `v:real^3`);\r
2538  (ASM_REWRITE_TAC[]);\r
2539  (UNDISCH_TAC `v IN {u0, u1, u2:real^3}`);\r
2540  (SET_TAC[]);\r
2541 \r
2542  (NEW_GOAL `s IN voronoi_list V vl`);\r
2543  (NEW_GOAL `convex (voronoi_list V vl)`);\r
2544  (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);\r
2545  (UP_ASM_TAC THEN REWRITE_TAC[convex] THEN STRIP_TAC);\r
2546  (UNDISCH_TAC `between s (s2,s3:real^3)`);\r
2547  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
2548  (REPEAT STRIP_TAC);\r
2549  (ONCE_REWRITE_TAC[GSYM IN]);\r
2550  (REWRITE_TAC[ASSUME `s = u % s2 + v % s3:real^3`]);\r
2551  (FIRST_ASSUM MATCH_MP_TAC);\r
2552  (ASM_REWRITE_TAC[]);\r
2553 \r
2554  (NEW_GOAL `~ (s IN affine hull {u0,u1,u2:real^3})`);\r
2555  STRIP_TAC;\r
2556 \r
2557  (NEW_GOAL `(s:real^3 - s2) dot (s - s2) = &0`);\r
2558  (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);\r
2559  (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);\r
2560  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
2561  (MATCH_MP_TAC MHFTTZN4);\r
2562  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);\r
2563  (REPEAT STRIP_TAC);\r
2564  (ASM_REWRITE_TAC[]);\r
2565  (ASM_REWRITE_TAC[]);\r
2566  (ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]);\r
2567  (EXPAND_TAC "vl" THEN ASM_MESON_TAC[set_of_list]);\r
2568  (UP_ASM_TAC THEN REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0;\r
2569    NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);\r
2570  (ASM_REWRITE_TAC[]);\r
2571 \r
2572  (NEW_GOAL `CARD {u0, u1, u2, s:real^3} = 4`);\r
2573  (ONCE_REWRITE_TAC[SET_RULE `{u0, u1, u2, s} = {s, u0, u1, u2}`]);\r
2574  (REWRITE_WITH `4 = SUC (CARD {u0,u1,u2:real^3})`);\r
2575  (ASM_REWRITE_TAC[]);\r
2576  (ARITH_TAC);\r
2577  (MATCH_MP_TAC (MESON[Geomdetail.CARD_CLAUSES_IMP] \r
2578   `!s a. FINITE s /\ ~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s)`));\r
2579  (REWRITE_TAC[Geomdetail.FINITE6]);\r
2580  (STRIP_TAC);\r
2581  (NEW_GOAL `s IN affine hull {u0, u1, u2:real^3}`);\r
2582  (UP_ASM_TAC THEN REWRITE_TAC[IN_AFFINE_KY_LEMMA1]);\r
2583  (ASM_MESON_TAC[]);\r
2584 \r
2585  (NEW_GOAL `~affine_dependent {u0, u1, u2, s:real^3}`);\r
2586  (ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {d,a,b,c}`]);\r
2587  (MATCH_MP_TAC AFFINE_INDEPENDENT_INSERT);\r
2588  (ASM_REWRITE_TAC[]);\r
2589  (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);\r
2590  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
2591  (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);\r
2592  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2` THEN ASM_REWRITE_TAC[]);\r
2593 \r
2594  (NEW_GOAL `s2 IN convex hull {u0, u1, u2:real^3}`);\r
2595  (REWRITE_WITH `s2 = omega_list V vl /\ {u0, u1, u2:real^3} = set_of_list vl`);\r
2596  (EXPAND_TAC "s2" THEN EXPAND_TAC "vl");\r
2597  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_2;set_of_list]);\r
2598  (MATCH_MP_TAC Rogers.XNHPWAB2);\r
2599  (EXISTS_TAC `2`);\r
2600  (ASM_REWRITE_TAC[IN]);\r
2601  (ASM_MESON_TAC[]);\r
2602 \r
2603  (NEW_GOAL `s1 = inv (&2) % (u0 + u1:real^3)`);\r
2604  (ONCE_REWRITE_TAC[GSYM midpoint]);\r
2605  (EXPAND_TAC "s1");\r
2606 \r
2607  (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 = \r
2608                  omega_list_n V [u0; u1:real^3] 1`);\r
2609  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2;OMEGA_LIST_TRUNCATE_1]);\r
2610  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2]);\r
2611  (REWRITE_WITH `omega_list V [u0; u1:real^3] = \r
2612    circumcenter (set_of_list [u0;u1])`);\r
2613  (MATCH_MP_TAC XNHPWAB1);\r
2614  (EXISTS_TAC `1`);\r
2615  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);\r
2616 \r
2617  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);\r
2618  (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
2619  (REWRITE_TAC[IN] THEN STRIP_TAC);\r
2620  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
2621  (EXISTS_TAC `2` THEN REWRITE_TAC[ARITH_RULE `1 <= 2`]);\r
2622  (ASM_REWRITE_TAC[]);\r
2623 \r
2624  (NEW_GOAL `!i j.  i < j /\ j <= 2\r
2625                      ==> hl (truncate_simplex i (vl:(real^3)list)) \r
2626                        < hl (truncate_simplex j vl)`);\r
2627 \r
2628  (MATCH_MP_TAC XNHPWAB4);\r
2629  (EXISTS_TAC `V:real^3->bool`);\r
2630  (ASM_REWRITE_TAC[IN]);\r
2631  (ASM_MESON_TAC[]);\r
2632 \r
2633  (NEW_GOAL `hl (truncate_simplex 1 (vl:(real^3)list)) < hl (truncate_simplex 2 vl)`);\r
2634  (FIRST_X_ASSUM MATCH_MP_TAC);\r
2635  (ARITH_TAC);\r
2636 \r
2637  (NEW_GOAL `truncate_simplex 2 vl = truncate_simplex 2 ul:(real^3)list`);\r
2638  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
2639  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);\r
2640  (MATCH_MP_TAC (REAL_ARITH `a < hl (truncate_simplex 2 (vl:(real^3)list)) /\ \r
2641    hl (truncate_simplex 2 vl) < b ==> a < b`));\r
2642  (ASM_REWRITE_TAC[]);\r
2643  (ASM_MESON_TAC[]);\r
2644  (REWRITE_TAC[set_of_list;Rogers.CIRCUMCENTER_2]);\r
2645 \r
2646  (NEW_GOAL `~(s3 IN affine hull {u0,u1,u2:real^3})`);\r
2647  (STRIP_TAC);\r
2648  (NEW_GOAL `(s3 - s2) dot (s3 - s2:real^3) = &0`);\r
2649  (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);\r
2650  (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);\r
2651  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
2652  (MATCH_MP_TAC MHFTTZN4);\r
2653  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);\r
2654  (REPEAT STRIP_TAC);\r
2655  (ASM_REWRITE_TAC[]);\r
2656  (ASM_REWRITE_TAC[]);\r
2657  (ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]);\r
2658  (EXPAND_TAC "vl" THEN ASM_MESON_TAC[set_of_list]);\r
2659  (UP_ASM_TAC THEN REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0;\r
2660    NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);\r
2661  (STRIP_TAC);\r
2662  (UNDISCH_TAC `between s (s2,s3:real^3)`);\r
2663  (REWRITE_TAC[ASSUME `s3= s2:real^3`; BETWEEN_REFL_EQ]);\r
2664  (ASM_REWRITE_TAC[]);\r
2665 \r
2666  (NEW_GOAL `p IN convex hull {u0, u1, s2, s:real^3}`);\r
2667  (MATCH_MP_TAC CONVEX_HULL_KY_LEMMA_5);\r
2668  (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `s3:real^3`);\r
2669  (REPEAT STRIP_TAC);\r
2670  (ASM_MESON_TAC[]);\r
2671  (ASM_MESON_TAC[]);\r
2672  (ASM_MESON_TAC[]);\r
2673  (ASM_MESON_TAC[]);\r
2674  (ASM_MESON_TAC[]);\r
2675  (NEW_GOAL `~(p:real^3 IN B4)`);\r
2676  (ASM_SET_TAC[IN_DIFF]);\r
2677  (UP_ASM_TAC THEN EXPAND_TAC "B4" THEN REWRITE_TAC[ASSUME \r
2678    `ul = [u0;u1;u2;u3:real^3]`; HD;TL; \r
2679     ASSUME `mxi V [u0; u1; u2; u3] = s:real^3`]);\r
2680  (ASM_MESON_TAC[]);\r
2681  (REWRITE_TAC[IN_INTER; ASSUME `p IN convex hull {u0, u1, u2, s:real^3}`]);\r
2682  (UNDISCH_TAC `p IN convex hull {u0, s1, s2, s3:real^3}`);\r
2683  (REWRITE_TAC[ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`;\r
2684    CONVEX_HULL_4;IN;IN_ELIM_THM]);\r
2685  (REPEAT STRIP_TAC);\r
2686  (EXISTS_TAC `u + v * inv (&2)`);\r
2687  (EXISTS_TAC `v * inv (&2)`);\r
2688  (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`);\r
2689  (REPEAT STRIP_TAC);\r
2690  (MATCH_MP_TAC REAL_LE_ADD);\r
2691  (ASM_REWRITE_TAC[]);\r
2692  (MATCH_MP_TAC REAL_LE_MUL);\r
2693  (ASM_REWRITE_TAC[]);\r
2694  (REAL_ARITH_TAC);\r
2695  (MATCH_MP_TAC REAL_LE_MUL);\r
2696  (ASM_REWRITE_TAC[]);\r
2697  (REAL_ARITH_TAC);\r
2698  (ASM_REWRITE_TAC[]);\r
2699  (ASM_REWRITE_TAC[]);\r
2700  (REWRITE_TAC[REAL_ARITH \r
2701   `(u + v * inv (&2)) + v * inv (&2) + w + z = u + v + w + z`]);\r
2702  (ASM_REWRITE_TAC[]);\r
2703  (REWRITE_TAC[ASSUME \r
2704    `p = u % u0 + v % inv (&2) % (u0 + u1) + w % s2 + z % s3:real^3`]);\r
2705  (VECTOR_ARITH_TAC);\r
2706 \r
2707 (* ========================================================================== *)\r
2708 \r
2709  (NEW_GOAL `?m n. between p (m,n) /\ between m (u0,u1) /\ between n (s2,s:real^3)`);\r
2710  (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_4_IMP_2_2]);\r
2711  (UP_ASM_TAC THEN REPEAT STRIP_TAC);\r
2712 \r
2713  (NEW_GOAL `between m (u0, s1:real^3)`);\r
2714  (ASM_CASES_TAC `between m (u0, s1:real^3)`);\r
2715  (UP_ASM_TAC THEN MESON_TAC[]);\r
2716  (NEW_GOAL `between m (s1, u1:real^3)`);\r
2717  (NEW_GOAL `between m (u0, s1) \/ between m (s1, u1:real^3)`);\r
2718  (MATCH_MP_TAC BETWEEN_TRANS_3_CASES);\r
2719  (ASM_REWRITE_TAC[]);\r
2720  (REWRITE_TAC[GSYM midpoint;BETWEEN_MIDPOINT]);\r
2721  (ASM_MESON_TAC[]);\r
2722  (NEW_GOAL `F`);\r
2723  (NEW_GOAL `between n (s2,s3:real^3)`);\r
2724  (ONCE_REWRITE_TAC[BETWEEN_SYM]);\r
2725  (MATCH_MP_TAC BETWEEN_TRANS);\r
2726  (EXISTS_TAC `s:real^3`);\r
2727  (ONCE_REWRITE_TAC[BETWEEN_SYM]);\r
2728  (ASM_MESON_TAC[]);\r
2729 \r
2730  (UP_ASM_TAC THEN UP_ASM_TAC THEN UNDISCH_TAC `between p (m,n:real^3)`);\r
2731  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
2732  (REPEAT STRIP_TAC);\r
2733  (UNDISCH_TAC `p = u % m + v % n:real^3`);\r
2734  (REWRITE_TAC[ASSUME `m = u' % s1 + v' % u1:real^3`; \r
2735    ASSUME `n = u'' % s2 + v'' % s3:real^3`]);\r
2736  (REWRITE_WITH `u1 = &2 % s1 - u0:real^3`);\r
2737  (REWRITE_TAC[ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`]);\r
2738  (VECTOR_ARITH_TAC);\r
2739  (REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);\r
2740  (REWRITE_TAC [VECTOR_ARITH \r
2741   `((u * u') % s1 + (u * v') % (&2 % s1 - u0)) +\r
2742    (v * u'') % s2 +\r
2743    (v * v'') % s3 = \r
2744    (u * (-- v')) % u0 + (u * u' + v' * &2 * u) % s1 + (v * u'') % s2 + (v * v'') % s3`]); \r
2745  (STRIP_TAC);\r
2746  (NEW_GOAL `u * --v' = &0`);\r
2747  (MATCH_MP_TAC AFFINE_DEPENDENT_KY_LEMMA1);\r
2748  (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `s1:real^3`);\r
2749  (EXISTS_TAC `s2:real^3` THEN EXISTS_TAC `s3:real^3`);\r
2750  (EXISTS_TAC `p:real^3`);\r
2751  (EXISTS_TAC `u * u' + v' * &2 * u`);\r
2752  (EXISTS_TAC `v * u''`);\r
2753  (EXISTS_TAC `v * v''`);\r
2754 \r
2755  (NEW_GOAL `~(affine_dependent {u0,s1,s2:real^3})`);\r
2756  (REWRITE_WITH `{u0,s1,s2:real^3} = {omega_list_n V vl i | i <= 2}`);\r
2757  (EXPAND_TAC "s1" THEN EXPAND_TAC "s2");\r
2758  (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 = omega_list_n V vl 1`);\r
2759  (EXPAND_TAC "vl" THEN REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW1; OMEGA_LIST_TRUNCATE_1]);\r
2760  (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 2 = omega_list_n V vl 2`);\r
2761  (EXPAND_TAC "vl" THEN REWRITE_TAC[OMEGA_LIST_TRUNCATE_2_NEW1; OMEGA_LIST_TRUNCATE_2]);\r
2762  (REWRITE_WITH `u0 = omega_list_n V vl 0`);\r
2763  (REWRITE_TAC[OMEGA_LIST_N]);\r
2764  (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);\r
2765  (REWRITE_TAC[OMEGA_LIST_UP_TO_2]);\r
2766  (MATCH_MP_TAC Rogers.AFFINE_INDEPENDENT_OMEGA_LIST_N);\r
2767  (ASM_MESON_TAC[]);\r
2768 \r
2769 (* ======================================================================== *)\r
2770 \r
2771  (NEW_GOAL `~affine_dependent {u0, s1, s2, s3:real^3}`);\r
2772  (ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {d,a,b,c}`]);\r
2773  (MATCH_MP_TAC AFFINE_INDEPENDENT_INSERT);\r
2774  STRIP_TAC;\r
2775  (ASM_REWRITE_TAC[]);\r
2776 \r
2777  (NEW_GOAL `~(s3 = s2:real^3)`);\r
2778  (STRIP_TAC);\r
2779  (UNDISCH_TAC `between s (s2,s3:real^3)`);\r
2780  (REWRITE_TAC[ASSUME `s3= s2:real^3`; BETWEEN_REFL_EQ]);\r
2781  (ASM_REWRITE_TAC[]);\r
2782  (STRIP_TAC);\r
2783 \r
2784  (NEW_GOAL `(s3 IN affine hull {u0,u1,u2:real^3})`);\r
2785  (UNDISCH_TAC `s2 IN convex hull {u0,u1,u2:real^3}` THEN UP_ASM_TAC THEN\r
2786    REWRITE_TAC[AFFINE_HULL_3; CONVEX_HULL_3; IN;IN_ELIM_THM; \r
2787    ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`]);\r
2788  (REPEAT STRIP_TAC);\r
2789 \r
2790  (REWRITE_TAC[ASSUME \r
2791    `s3 = u''' % u0 + v''' % inv (&2) % (u0 + u1) + w % s2:real^3`;\r
2792    ASSUME `s2 = u'''' % u0 + v'''' % u1 + w' % u2:real^3`]);\r
2793  (EXISTS_TAC `u''' + v''' * inv (&2) + w * u''''`);\r
2794  (EXISTS_TAC `v''' * inv (&2) + w * v''''`);\r
2795  (EXISTS_TAC `w * w'`);\r
2796  (STRIP_TAC);\r
2797  (REWRITE_TAC[REAL_ARITH \r
2798  `(u''' + v''' * inv (&2) + w * u'''') +\r
2799   (v''' * inv (&2) + w * v'''') + w * w' = \r
2800   (u''' + v''') + w * (u'''' + v'''' + w')`]);\r
2801  (ASM_REWRITE_TAC[REAL_ARITH `(a + b) + c * &1 = a + b + c`]);\r
2802  (VECTOR_ARITH_TAC);\r
2803  (ASM_MESON_TAC[]);\r
2804 \r
2805  (REPEAT STRIP_TAC);\r
2806  (ASM_MESON_TAC[]);\r
2807 \r
2808  (ONCE_REWRITE_TAC [SET_RULE `{u0, s1, s2, s3} = {s3,u0, s1, s2}`]);\r
2809  (NEW_GOAL `CARD {u0,s1,s2:real^3} = 3`);\r
2810  (REWRITE_WITH `{u0,s1,s2:real^3} = {omega_list_n V vl i | i <= 2}`);\r
2811  (EXPAND_TAC "s1" THEN EXPAND_TAC "s2");\r
2812  (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 = omega_list_n V vl 1`);\r
2813  (EXPAND_TAC "vl" THEN REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW1; OMEGA_LIST_TRUNCATE_1]);\r
2814  (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 2 = omega_list_n V vl 2`);\r
2815  (EXPAND_TAC "vl" THEN REWRITE_TAC[OMEGA_LIST_TRUNCATE_2_NEW1; OMEGA_LIST_TRUNCATE_2]);\r
2816  (REWRITE_WITH `u0 = omega_list_n V vl 0`);\r
2817  (REWRITE_TAC[OMEGA_LIST_N]);\r
2818  (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);\r
2819  (REWRITE_TAC[OMEGA_LIST_UP_TO_2]);\r
2820  (REWRITE_WITH `{omega_list_n V vl i | i <= 2} = IMAGE (omega_list_n V vl) {i | i <= 2}`);\r
2821  (REWRITE_TAC[IMAGE]);\r
2822  (SET_TAC[]);\r
2823  (REWRITE_TAC[NUMSEG_LE]);\r
2824  (REWRITE_WITH `IMAGE (omega_list_n V vl) (0..2) = {omega_list_n V vl i | i IN (0..2)}`);\r
2825  (REWRITE_TAC[IMAGE]);\r
2826  (SET_TAC[]);\r
2827  (NEW_GOAL `aff_dim {omega_list_n V vl j | j IN 0..2} = &2`);\r
2828  (MATCH_MP_TAC XNHPWAB3);\r
2829  (ASM_MESON_TAC[IN]);\r
2830  (NEW_GOAL `aff_dim {omega_list_n V vl i | i IN 0..2} <= \r
2831   &(CARD {omega_list_n V vl i | i IN 0..2}) - &1`);\r
2832  (MATCH_MP_TAC AFF_DIM_LE_CARD);\r
2833  (REWRITE_WITH `{omega_list_n V vl i | i IN (0..2)} = IMAGE (omega_list_n V vl) (0..2)`);\r
2834  (REWRITE_TAC[IMAGE]);\r
2835  (SET_TAC[]);\r
2836  (REWRITE_TAC[GSYM NUMSEG_LE]);\r
2837  (REWRITE_WITH `IMAGE (omega_list_n V vl) {i | i <= 2} = {omega_list_n V vl i | i <= 2}`);\r
2838  (REWRITE_TAC[IMAGE]);\r
2839  (SET_TAC[]);\r
2840  (REWRITE_TAC[OMEGA_LIST_UP_TO_2;Geomdetail.FINITE6]);\r
2841  (UP_ASM_TAC THEN REWRITE_TAC[ARITH_RULE `a:int <= b - &1 <=> a + &1 <= b`]);\r
2842  (REWRITE_TAC[ASSUME `aff_dim {omega_list_n V vl j | j IN 0..2} = &2`;\r
2843    ARITH_RULE `&2 + &1 = &3:int`; INT_OF_NUM_LE]);\r
2844  (STRIP_TAC);\r
2845  (NEW_GOAL `CARD {omega_list_n V vl i | i IN 0..2} <= 3`);\r
2846  (REWRITE_WITH `{omega_list_n V vl i | i IN (0..2)} = IMAGE (omega_list_n V vl) (0..2)`);\r
2847  (REWRITE_TAC[IMAGE]);\r
2848  (SET_TAC[]);\r
2849  (REWRITE_TAC[GSYM NUMSEG_LE]);\r
2850  (REWRITE_WITH `IMAGE (omega_list_n V vl) {i | i <= 2} = {omega_list_n V vl i | i <= 2}`);\r
2851  (REWRITE_TAC[IMAGE]);\r
2852  (SET_TAC[]);\r
2853  (REWRITE_TAC[OMEGA_LIST_UP_TO_2; Geomdetail.CARD3]);\r
2854  (ASM_ARITH_TAC);\r
2855  (REWRITE_WITH `4 = SUC (CARD {u0, s1, s2:real^3})`);\r
2856  (ASM_REWRITE_TAC[]);\r
2857  (ARITH_TAC);\r
2858  (MATCH_MP_TAC (MESON[Geomdetail.CARD_CLAUSES_IMP] \r
2859   `!a s. FINITE s /\ ~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s)`));\r
2860  (REWRITE_TAC[Geomdetail.FINITE6]);\r
2861  (STRIP_TAC);\r
2862 \r
2863  (NEW_GOAL `~(s3 IN affine hull {u0,s1,s2:real^3})`);\r
2864  (STRIP_TAC);\r
2865  (NEW_GOAL `(s3 IN affine hull {u0,u1,u2:real^3})`);\r
2866  (UNDISCH_TAC `s2 IN convex hull {u0,u1,u2:real^3}` THEN UP_ASM_TAC THEN\r
2867    REWRITE_TAC[AFFINE_HULL_3; CONVEX_HULL_3; IN;IN_ELIM_THM; \r
2868    ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`]);\r
2869  (REPEAT STRIP_TAC);\r
2870 \r
2871  (REWRITE_TAC[ASSUME \r
2872    `s3 = u''' % u0 + v''' % inv (&2) % (u0 + u1) + w % s2:real^3`;\r
2873    ASSUME `s2 = u'''' % u0 + v'''' % u1 + w' % u2:real^3`]);\r
2874  (EXISTS_TAC `u''' + v''' * inv (&2) + w * u''''`);\r
2875  (EXISTS_TAC `v''' * inv (&2) + w * v''''`);\r
2876  (EXISTS_TAC `w * w'`);\r
2877  (STRIP_TAC);\r
2878  (REWRITE_TAC[REAL_ARITH \r
2879  `(u''' + v''' * inv (&2) + w * u'''') +\r
2880   (v''' * inv (&2) + w * v'''') + w * w' = \r
2881   (u''' + v''') + w * (u'''' + v'''' + w')`]);\r
2882  (ASM_REWRITE_TAC[REAL_ARITH `(a + b) + c * &1 = a + b + c`]);\r
2883  (VECTOR_ARITH_TAC);\r
2884  (ASM_MESON_TAC[]);\r
2885  (NEW_GOAL `s3 IN affine hull {u0, s1, s2:real^3}`);\r
2886  (UNDISCH_TAC `s3 IN {u0, s1, s2:real^3}` THEN \r
2887    REWRITE_TAC [IN_AFFINE_KY_LEMMA1]);\r
2888  (ASM_MESON_TAC[]);\r
2889  (ASM_MESON_TAC[]);\r
2890  (REWRITE_TAC[REAL_ARITH \r
2891    `u * --v' + (u * u' + v' * &2 * u) + v * u'' + v * v''\r
2892     = u * (u' + v') + v * (u'' + v'')`]);\r
2893  (ASM_REWRITE_TAC[REAL_MUL_RID]);\r
2894  (ASM_REWRITE_TAC[]);\r
2895  (REWRITE_TAC[REAL_ARITH `a * (-- b) <= &0 <=> &0 <= a * b`]);\r
2896  (ASM_SIMP_TAC[REAL_LE_MUL]);\r
2897  (NEW_GOAL `p IN affine hull {s1, s2, s3:real^3}`);\r
2898  (REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);\r
2899  (EXISTS_TAC `u * u' + v' * &2 * u`);\r
2900  (EXISTS_TAC `v * u''`);\r
2901  (EXISTS_TAC `v * v''`);\r
2902  (STRIP_TAC);\r
2903  (REWRITE_TAC[REAL_ARITH `(u * u' + v' * &2 * u) + v * u'' + v * v'' = \r
2904    (u * (u' + v') + v * (u'' + v'')) - (u * -- v')`]);\r
2905  (ASM_REWRITE_TAC[REAL_MUL_RID]);\r
2906  (REAL_ARITH_TAC);\r
2907  (ASM_REWRITE_TAC[]);\r
2908  (VECTOR_ARITH_TAC);\r
2909  (NEW_GOAL `~(p:real^3 IN B7)`);\r
2910  (ASM_SET_TAC[IN_DIFF]);\r
2911  (UP_ASM_TAC THEN EXPAND_TAC "B7");\r
2912  (UP_ASM_TAC THEN EXPAND_TAC "s1" THEN EXPAND_TAC "s2" THEN EXPAND_TAC "s3");\r
2913  (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
2914  (UP_ASM_TAC THEN MESON_TAC[]);\r
2915 \r
2916 (* ========================================================================= *)\r
2917 \r
2918  (NEW_GOAL `?q. between p (u0,q) /\ between q (n,s1:real^3)`);\r
2919  (UNDISCH_TAC `between p (m,n:real^3)` THEN UP_ASM_TAC);\r
2920  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;IN;IN_ELIM_THM; CONVEX_HULL_2]);\r
2921  (REPEAT STRIP_TAC);\r
2922  (EXISTS_TAC `((u' * v) / (u' * v + v')) % s1 + \r
2923                (v' / (u' * v + v')) % n:real^3`);\r
2924  (NEW_GOAL `~((u' * v + v') =  &0)`);\r
2925  (STRIP_TAC);\r
2926  (NEW_GOAL `p = u0:real^3`);\r
2927  (ASM_REWRITE_TAC[]);\r
2928  (NEW_GOAL `u' * v = &0 /\ v' = &0`);\r
2929  (NEW_GOAL `&0 <= u' * v /\ &0 <= v'`);\r
2930  (ASM_SIMP_TAC [REAL_LE_MUL]);\r
2931  (ASM_REAL_ARITH_TAC);\r
2932  (NEW_GOAL `u' * u = &1`);\r
2933  (NEW_GOAL `u' * u + (u' * v + v') = &1`);\r
2934  (REWRITE_TAC[REAL_ARITH `u' * u + (u' * v + v') = u' * (u + v) + v'`]);\r
2935  (ASM_MESON_TAC[REAL_MUL_RID]);\r
2936  (ASM_REAL_ARITH_TAC);\r
2937  (REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);\r
2938  (ONCE_REWRITE_TAC[REAL_ARITH `a * b * c = (a * b) * c`]);\r
2939  (ASM_REWRITE_TAC[]);\r
2940  (VECTOR_ARITH_TAC);\r
2941 \r
2942  (NEW_GOAL `~(p:real^3 IN B6)`);\r
2943  (ASM_SET_TAC[IN_DIFF]);\r
2944  (UP_ASM_TAC THEN EXPAND_TAC "B6" THEN REWRITE_TAC[\r
2945    ASSUME `ul = [u0;u1;u2;u3:real^3]`; HD; TL]);\r
2946  (REWRITE_TAC[ASSUME `p = u0:real^3`; AFFINE_HULL_3;IN;IN_ELIM_THM]);\r
2947  (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);\r
2948  (STRIP_TAC);\r
2949  (REAL_ARITH_TAC);\r
2950  (VECTOR_ARITH_TAC);\r
2951 \r
2952  (STRIP_TAC);\r
2953  (EXISTS_TAC `u' * u`);\r
2954  (EXISTS_TAC `u' * v + v'`);\r
2955  (REPEAT STRIP_TAC);\r
2956  (ASM_SIMP_TAC[REAL_LE_MUL]);\r
2957  (ASM_SIMP_TAC[REAL_LE_ADD;REAL_LE_MUL]);\r
2958  (ASM_REWRITE_TAC[REAL_ARITH `u' * u + u' * v + v' = u' * (u + v) + v'`;\r
2959    REAL_MUL_RID]);\r
2960  (REWRITE_TAC[ASSUME `p = u' % m + v' % n:real^3`; \r
2961    ASSUME `m = u % u0 + v % s1:real^3`;VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);\r
2962 \r
2963  (REWRITE_TAC[VECTOR_ARITH `((u' * v + v') * (u' * v) / (u' * v + v')) % s1 = \r
2964                ((u' * v + v') / (u' * v + v')) % ((u' * v) % s1)`]);\r
2965  (REWRITE_TAC[VECTOR_ARITH `((u' * v + v') * v' / (u' * v + v')) % n = \r
2966                ((u' * v + v') / (u' * v + v')) % (v' % n)`]);\r
2967  (REWRITE_TAC[VECTOR_ARITH `(x + a % y) + b % z = x + m % a % y + m % b % z \r
2968    <=> (m - &1) % (a % y + b % z )= vec 0`]);\r
2969 \r
2970  (REWRITE_WITH `(u' * v + v') / (u' * v + v') = &1`);\r
2971  (MATCH_MP_TAC REAL_DIV_REFL);\r
2972  (ASM_REWRITE_TAC[]);\r
2973  (VECTOR_ARITH_TAC);\r
2974 \r
2975  (EXISTS_TAC `v' / (u' * v + v')`);\r
2976  (EXISTS_TAC `(u' * v) / (u' * v + v')`);\r
2977  (REPEAT STRIP_TAC);\r
2978  (ASM_SIMP_TAC[REAL_LE_DIV;REAL_LE_ADD;REAL_LE_MUL]);\r
2979  (ASM_SIMP_TAC[REAL_LE_DIV;REAL_LE_ADD;REAL_LE_MUL]);\r
2980  (REWRITE_TAC[REAL_ARITH `a / x + b / x = (b + a) / x`]);\r
2981  (MATCH_MP_TAC REAL_DIV_REFL);\r
2982  (ASM_REWRITE_TAC[]);\r
2983  (VECTOR_ARITH_TAC);\r
2984 \r
2985  (UP_ASM_TAC THEN REPEAT STRIP_TAC);\r
2986 \r
2987 \r
2988 (* ========================================================================= *)\r
2989 \r
2990  (UNDISCH_TAC `~(p:real^3 IN\r
2991         rcone_gt (HD ul) (HD (TL ul))\r
2992         (hl (truncate_simplex 1 ul) / sqrt (&2)))`);\r
2993  (ASM_REWRITE_TAC[HD;TL]);\r
2994  (REWRITE_WITH `hl  (truncate_simplex 1 [u0; u1; u2; u3:real^3]) = dist (s1, u0)`);\r
2995  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
2996  (REWRITE_WITH `dist (s1,u0) = dist (circumcenter (set_of_list [u0;u1:real^3]),    HD [u0;u1:real^3])`);\r
2997  (REWRITE_TAC[HD; set_of_list; Rogers.CIRCUMCENTER_2]);\r
2998  (ASM_REWRITE_TAC[midpoint]);\r
2999  (MATCH_MP_TAC Rogers.HL_EQ_DIST0);\r
3000  (EXISTS_TAC `V:real^3->bool`);\r
3001  (EXISTS_TAC `1`);\r
3002  (ASM_REWRITE_TAC[]);\r
3003  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);\r
3004  (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
3005  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
3006  (EXISTS_TAC `2`);\r
3007  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);\r
3008 \r
3009 \r
3010  (NEW_GOAL `q:real^3 IN rcone_ge u0 u1 (dist (s1,u0) / sqrt (&2))`);\r
3011  (REWRITE_TAC[rcone_ge; rconesgn;IN;IN_ELIM_THM]);\r
3012  (REWRITE_WITH `(q - u0) dot (u1 - u0) = \r
3013   (q - s1) dot (u1 - u0) + (s1 - u0) dot (u1 - u0:real^3)`);\r
3014  (VECTOR_ARITH_TAC);\r
3015  (REWRITE_WITH `(q - s1) dot (u1 - u0:real^3) = &0`);\r
3016  (REWRITE_WITH `u1 - u0 = (-- &2) % (u0:real^3 - s1)`);\r
3017  (ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);\r
3018  (REWRITE_TAC[DOT_RMUL]);\r
3019  (REWRITE_WITH `(q - s1) dot (u0 - s1:real^3) = &0`);\r
3020  (REWRITE_WITH `s1 = circumcenter (set_of_list [u0;u1:real^3])`);\r
3021  (ASM_REWRITE_TAC[set_of_list; Rogers.CIRCUMCENTER_2; midpoint]);\r
3022  (MATCH_MP_TAC MHFTTZN4);\r
3023  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`);\r
3024  (REPEAT STRIP_TAC);\r
3025  (ASM_REWRITE_TAC[]);\r
3026  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);\r
3027  (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
3028  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
3029  (EXISTS_TAC `2`);\r
3030  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);\r
3031 \r
3032  (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);\r
3033  (NEW_GOAL `n IN voronoi_list V [u0; u1:real^3]`);\r
3034  (NEW_GOAL `s2 IN voronoi_list V [u0; u1:real^3]`);\r
3035 \r
3036  (NEW_GOAL `(s2:real^3) IN voronoi_list V vl`);\r
3037  (SIMP_TAC[ASSUME `s2 = omega_list V vl`]);\r
3038  (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);\r
3039  (EXISTS_TAC `2`);\r
3040  (ASM_REWRITE_TAC[]);\r
3041 \r
3042  (MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET A) ==> a IN A`));\r
3043  (EXISTS_TAC `voronoi_list V vl`);\r
3044  (STRIP_TAC);\r
3045  (ASM_REWRITE_TAC[]);\r
3046  (EXPAND_TAC "vl");\r
3047  (REWRITE_TAC[VORONOI_LIST;VORONOI_SET;voronoi_closed;set_of_list; \r
3048    SUBSET; IN_INTERS]);\r
3049  (ONCE_REWRITE_TAC[IN]);\r
3050  (REWRITE_TAC[IN_ELIM_THM]);\r
3051  (REPEAT STRIP_TAC);\r
3052  (FIRST_ASSUM MATCH_MP_TAC);\r
3053  (EXISTS_TAC `v:real^3`);\r
3054  (ASM_REWRITE_TAC[]);\r
3055  (UNDISCH_TAC `v IN {u0, u1:real^3}`);\r
3056  (SET_TAC[]);\r
3057 \r
3058  (NEW_GOAL `s3 IN voronoi_list V [u0; u1]`);\r
3059  (MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET A) ==> a IN A`));\r
3060  (EXISTS_TAC `voronoi_list V vl`);\r
3061  (STRIP_TAC);\r
3062  (ASM_REWRITE_TAC[]);\r
3063  (EXPAND_TAC "vl");\r
3064  (REWRITE_TAC[VORONOI_LIST;VORONOI_SET;voronoi_closed;set_of_list; \r
3065    SUBSET; IN_INTERS]);\r
3066  (ONCE_REWRITE_TAC[IN]);\r
3067  (REWRITE_TAC[IN_ELIM_THM]);\r
3068  (REPEAT STRIP_TAC);\r
3069  (FIRST_ASSUM MATCH_MP_TAC);\r
3070  (EXISTS_TAC `v:real^3`);\r
3071  (ASM_REWRITE_TAC[]);\r
3072  (UNDISCH_TAC `v IN {u0, u1:real^3}`);\r
3073  (SET_TAC[]);\r
3074 \r
3075  (NEW_GOAL `convex (voronoi_list V [u0;u1:real^3])`);\r
3076  (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);\r
3077  (UP_ASM_TAC THEN REWRITE_TAC[convex] THEN STRIP_TAC);\r
3078  (SUBGOAL_THEN `between n (s2,s3:real^3)` MP_TAC);\r
3079  (ONCE_REWRITE_TAC[BETWEEN_SYM]);\r
3080  (MATCH_MP_TAC BETWEEN_TRANS);\r
3081  (EXISTS_TAC `s:real^3`);\r
3082  (ONCE_REWRITE_TAC[BETWEEN_SYM]);\r
3083  (ASM_REWRITE_TAC[]);\r
3084  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
3085  (REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM IN]);\r
3086  (REWRITE_TAC[ASSUME `n = u % s2 + v % s3:real^3`]);\r
3087  (FIRST_ASSUM MATCH_MP_TAC);\r
3088  (ASM_REWRITE_TAC[]);\r
3089 \r
3090  (UNDISCH_TAC `between q (n,s1:real^3)`);\r
3091  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
3092  (REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM IN]);\r
3093  (REWRITE_TAC[ASSUME `q = u % n + v % s1:real^3`]);\r
3094  (NEW_GOAL `convex (voronoi_list V [u0;u1:real^3])`);\r
3095  (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);\r
3096  (UP_ASM_TAC THEN REWRITE_TAC[convex] THEN STRIP_TAC);\r
3097  (FIRST_ASSUM MATCH_MP_TAC);\r
3098  (ASM_REWRITE_TAC[]);\r
3099  (REWRITE_TAC[GSYM (ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`)]);\r
3100  (REWRITE_WITH `s1 = omega_list V [u0;u1:real^3]`);\r
3101  (EXPAND_TAC "s1");\r
3102  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]);\r
3103  (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);\r
3104  (EXISTS_TAC `1`);\r
3105  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`);\r
3106  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
3107  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
3108  (EXISTS_TAC `3`);\r
3109  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);\r
3110  (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);\r
3111  (REWRITE_TAC[set_of_list] THEN SET_TAC[]);\r
3112  (REAL_ARITH_TAC);\r
3113 \r
3114  (REWRITE_WITH `(s1 - u0) dot (u1 - u0:real^3) = dist (s1,u0) * dist (u1,u0)`);\r
3115  (REWRITE_TAC[dist]);\r
3116  (REWRITE_TAC [NORM_CAUCHY_SCHWARZ_EQ]);\r
3117  (REWRITE_TAC[ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`; \r
3118    VECTOR_ARITH `inv (&2) % (u0 + u1) - u0 = inv (&2) % (u1 - u0)`]);\r
3119  (REWRITE_TAC[NORM_MUL; VECTOR_MUL_ASSOC; REAL_ABS_MUL]);\r
3120  (REWRITE_WITH `abs (inv (&2)) = inv (&2)`);\r
3121  (REWRITE_TAC[REAL_ABS_REFL]);\r
3122  (REAL_ARITH_TAC);\r
3123  (VECTOR_ARITH_TAC);\r
3124  (REWRITE_TAC[REAL_ADD_LID; REAL_ARITH `a * b >= x * b * a / t <=>\r
3125    &0 <= a * b * (&1 - x / t)`]);\r
3126  (MATCH_MP_TAC REAL_LE_MUL);\r
3127  (STRIP_TAC);\r
3128  (REWRITE_TAC[DIST_POS_LE]);\r
3129  (MATCH_MP_TAC REAL_LE_MUL);\r
3130  (STRIP_TAC);\r
3131  (REWRITE_TAC[DIST_POS_LE]);\r
3132  (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);\r
3133  (REWRITE_WITH `dist (q,u0:real^3) / sqrt (&2) <= &1 \r
3134    <=> dist (q,u0) <= &1 * sqrt (&2) `);\r
3135  (MATCH_MP_TAC REAL_LE_LDIV_EQ);\r
3136  (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);\r
3137  (ONCE_REWRITE_TAC[DIST_SYM]);\r
3138  (ONCE_REWRITE_TAC[REAL_MUL_LID]);\r
3139 \r
3140  (NEW_GOAL `dist (u0,s1:real^3) = hl (truncate_simplex 1 [u0;u1:real^3])`);\r
3141  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
3142  (REWRITE_WITH `s1 = omega_list V [u0;u1:real^3]`);\r
3143  (EXPAND_TAC "s1");\r
3144  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]);\r
3145  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
3146  (ONCE_REWRITE_TAC[DIST_SYM]);\r
3147  (REWRITE_WITH ` dist (omega_list V [u0; u1],u0) =     \r
3148    dist (omega_list V [u0; u1],HD [u0;u1:real^3])`);\r
3149  (REWRITE_TAC[HD]);\r
3150  (MATCH_MP_TAC Rogers.WAUFCHE2);\r
3151  (EXISTS_TAC `1`);\r
3152  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);\r
3153  (EXPAND_TAC "vl");\r
3154  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
3155  (REPEAT STRIP_TAC);\r
3156  (ASM_REWRITE_TAC[]);\r
3157  (REWRITE_TAC[IN]);\r
3158  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
3159  (EXISTS_TAC `2`);\r
3160  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);\r
3161 \r
3162  (NEW_GOAL `hl (truncate_simplex 1 vl) <= hl (vl:(real^3)list)`);\r
3163  (MATCH_MP_TAC Rogers.HL_DECREASE);\r
3164  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);\r
3165  (ASM_REWRITE_TAC[IN; ARITH_RULE `1 <= 2`]);\r
3166  (NEW_GOAL `hl (vl:(real^3)list) < sqrt (&2)`);\r
3167  (ONCE_ASM_REWRITE_TAC[]);\r
3168  (ASM_REAL_ARITH_TAC);\r
3169  (ASM_REAL_ARITH_TAC);\r
3170 \r
3171 \r
3172  (NEW_GOAL `hl (truncate_simplex 1 [u0;u1:real^3]) <= hl (vl:(real^3)list)`);\r
3173  (REWRITE_WITH `truncate_simplex 1 [u0;u1:real^3] =  \r
3174    truncate_simplex 1 vl`);\r
3175  (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
3176  (MATCH_MP_TAC Rogers.HL_DECREASE);\r
3177  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);\r
3178  (ASM_REWRITE_TAC[IN; ARITH_RULE `1 <= 2`]);\r
3179  (NEW_GOAL `hl (vl:(real^3)list) < sqrt (&2)`);\r
3180  (ONCE_ASM_REWRITE_TAC[]);\r
3181  (ASM_REAL_ARITH_TAC);\r
3182  (NEW_GOAL `dist (u0,s1:real^3) < sqrt (&2)`);\r
3183  (ONCE_ASM_REWRITE_TAC[]);\r
3184  (ASM_REAL_ARITH_TAC);\r
3185  (NEW_GOAL `?y. y IN {n,s1:real^3} /\\r
3186   (!x. x IN convex hull {n,s1} ==> norm (x - u0) <= norm (y - u0))`);\r
3187  (MATCH_MP_TAC SIMPLEX_FURTHEST_LE);\r
3188  (REWRITE_TAC[Geomdetail.FINITE6]);\r
3189  (SET_TAC[]);\r
3190  (UP_ASM_TAC THEN REWRITE_TAC [SET_RULE `a IN {x,y} <=> a = x \/ a = y`] \r
3191    THEN REPEAT STRIP_TAC);\r
3192  (NEW_GOAL `dist (u0,q) <= dist (u0, n:real^3)`);\r
3193  (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC\r
3194   [dist; GSYM (ASSUME `y' = n:real^3`)]);\r
3195  (POP_ASSUM MATCH_MP_TAC);\r
3196  (REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);\r
3197  (ASM_REWRITE_TAC[]);\r
3198 \r
3199  (NEW_GOAL `dist (u0,n:real^3) <= sqrt (&2)`);\r
3200  (NEW_GOAL `?y. y IN {s2,s:real^3} /\\r
3201   (!x. x IN convex hull {s2,s} ==> norm (x - u0) <= norm (y - u0))`);\r
3202  (MATCH_MP_TAC SIMPLEX_FURTHEST_LE);\r
3203  (REWRITE_TAC[Geomdetail.FINITE6]);\r
3204  (SET_TAC[]);\r
3205  (UP_ASM_TAC THEN REWRITE_TAC [SET_RULE `a IN {x,y} <=> a = x \/ a = y`] \r
3206    THEN REPEAT STRIP_TAC);\r
3207  (NEW_GOAL `dist (u0,n) <= dist (u0, s2:real^3)`);\r
3208  (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC\r
3209   [dist; GSYM (ASSUME `y'' = s2:real^3`)]);\r
3210  (POP_ASSUM MATCH_MP_TAC);\r
3211  (REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);\r
3212  (ASM_REWRITE_TAC[]);\r
3213  (NEW_GOAL `dist (u0,s2:real^3) < sqrt (&2)`);\r
3214  (ONCE_REWRITE_TAC[DIST_SYM]);\r
3215  (ONCE_ASM_REWRITE_TAC[]);\r
3216  (ASM_REWRITE_TAC[]);\r
3217  (ASM_REAL_ARITH_TAC);\r
3218  (NEW_GOAL `dist (u0,n) <= dist (u0, s:real^3)`);\r
3219  (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC\r
3220   [dist; GSYM (ASSUME `y'' = s:real^3`)]);\r
3221  (POP_ASSUM MATCH_MP_TAC);\r
3222  (REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);\r
3223  (ASM_REWRITE_TAC[]);\r
3224  (ASM_REAL_ARITH_TAC);\r
3225  (ASM_REAL_ARITH_TAC);\r
3226 \r
3227  (NEW_GOAL `dist (u0,q) <= dist (u0, s1:real^3)`);\r
3228  (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC\r
3229   [dist; GSYM (ASSUME `y' = s1:real^3`)]);\r
3230  (POP_ASSUM MATCH_MP_TAC);\r
3231  (REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);\r
3232  (ASM_REWRITE_TAC[]);\r
3233  (ASM_REAL_ARITH_TAC);\r
3234 \r
3235 (* ========================================================================== *)\r
3236 \r
3237  (NEW_GOAL `p:real^3 IN rcone_ge u0 u1 (dist (s1,u0) / sqrt (&2))`);\r
3238  (UNDISCH_TAC `between p (u0,q:real^3)`);\r
3239  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
3240  (REPEAT STRIP_TAC);\r
3241  (ONCE_REWRITE_TAC[GSYM IN]);\r
3242  (REWRITE_TAC[ASSUME `p = u % u0 + v % q:real^3`]);\r
3243  (REWRITE_WITH `u % u0 + v % q = u0 + v % (q - u0:real^3)`);\r
3244  (REWRITE_TAC[VECTOR_ARITH `u % u0 + v % q = u0 + v % (q - u0) <=>\r
3245    ((u + v) - &1) % u0 = vec 0`]);\r
3246  (ASM_REWRITE_TAC[]);\r
3247  (VECTOR_ARITH_TAC);\r
3248  (MATCH_MP_TAC RCONE_GE_TRANS);\r
3249  (REWRITE_TAC[VECTOR_ARITH `u0 + q - u0:real^3 = q`]);\r
3250  (ASM_REWRITE_TAC[]);\r
3251  (REWRITE_TAC[RCONE_GT_GE; IN_DIFF]);\r
3252  (STRIP_TAC);\r
3253  (ASM_REWRITE_TAC[]);\r
3254  (REWRITE_TAC[IN;IN_ELIM_THM]);\r
3255  (STRIP_TAC);\r
3256  (NEW_GOAL `~(p:real^3 IN B3)`);\r
3257  (ASM_SET_TAC[]);\r
3258  (UP_ASM_TAC THEN EXPAND_TAC "B3" THEN REWRITE_TAC[ASSUME \r
3259   `ul =  [u0;u1;u2;u3:real^3]`; HD;TL]);\r
3260  (REWRITE_WITH `hl (truncate_simplex 1 [u0; u1; u2; u3]) = dist (s1,u0:real^3)`);\r
3261  (REWRITE_WITH `truncate_simplex 1 [u0; u1; u2; u3] = \r
3262    truncate_simplex 1 [u0;u1:real^3]`);\r
3263  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
3264  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
3265  (REWRITE_WITH `s1 = omega_list V [u0;u1:real^3]`);\r
3266  (EXPAND_TAC "s1");\r
3267  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]);\r
3268  (REWRITE_WITH ` dist (omega_list V [u0; u1],u0) =     \r
3269    dist (omega_list V [u0; u1],HD [u0;u1:real^3])`);\r
3270  (REWRITE_TAC[HD]);\r
3271  (MATCH_MP_TAC Rogers.WAUFCHE2);\r
3272  (EXISTS_TAC `1`);\r
3273  (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`);\r
3274  (EXPAND_TAC "vl");\r
3275  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
3276  (REPEAT STRIP_TAC);\r
3277  (ASM_REWRITE_TAC[]);\r
3278  (REWRITE_TAC[IN]);\r
3279  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
3280  (EXISTS_TAC `2`);\r
3281  (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]);\r
3282 \r
3283  (NEW_GOAL `hl (truncate_simplex 1 vl) <= hl (vl:(real^3)list)`);\r
3284  (MATCH_MP_TAC Rogers.HL_DECREASE);\r
3285  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);\r
3286  (ASM_REWRITE_TAC[IN; ARITH_RULE `1 <= 2`]);\r
3287  (NEW_GOAL `hl (vl:(real^3)list) < sqrt (&2)`);\r
3288  (ONCE_ASM_REWRITE_TAC[]);\r
3289  (ASM_REAL_ARITH_TAC);\r
3290  (ASM_REAL_ARITH_TAC);\r
3291 \r
3292  (REWRITE_TAC[rcone_eq;rconesgn;IN;IN_ELIM_THM]);\r
3293  (UP_ASM_TAC THEN REWRITE_TAC[dist] THEN MESON_TAC[]);\r
3294  (SET_TAC[]);\r
3295 \r
3296  (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 1`);\r
3297  (GEN_TAC THEN STRIP_TAC);\r
3298  (NEW_GOAL `~(y = 4 \/ y = 0 \/ y = 2 \/ y = 3)`);\r
3299  (ASM_SIMP_TAC[]);\r
3300  (ASM_ARITH_TAC);\r
3301  (NEW_GOAL `i = 1`);\r
3302  (FIRST_ASSUM MATCH_MP_TAC);\r
3303  (ASM_REWRITE_TAC[]);\r
3304  (GEN_TAC THEN STRIP_TAC);\r
3305  (ASM_REWRITE_TAC[]);\r
3306  (FIRST_ASSUM MATCH_MP_TAC);\r
3307  (ASM_REWRITE_TAC[]);\r
3308  (UP_ASM_TAC THEN REWRITE_TAC[MESON[] `~ ~ A <=> A`] THEN DISCH_TAC);\r
3309 \r
3310 (* ======================================================================== *)\r
3311 \r
3312 \r
3313  (ASM_CASES_TAC \r
3314   `p IN aff_ge {u0:real^3, u1} {mxi V ul, omega_list_n V ul 3}`);\r
3315 \r
3316  (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> \r
3317                 ~ (y = 4 \/ y = 0 \/ y = 1 \/ y = 3)`);\r
3318  (REPEAT STRIP_TAC);\r
3319  (NEW_GOAL `mcell 4 V ul = {}`);\r
3320  (SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);\r
3321  (COND_CASES_TAC);\r
3322  (NEW_GOAL `F`);\r
3323  (ASM_MESON_TAC[]);\r
3324  (ASM_MESON_TAC[]);\r
3325  (REFL_TAC);\r
3326  (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 4`]);\r
3327  (REWRITE_TAC[ASSUME `mcell 4 V ul = {}`]);\r
3328  (SET_TAC[]);\r
3329  (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 0`;\r
3330    MCELL_EXPLICIT;mcell0]);\r
3331  (STRIP_TAC);\r
3332  (NEW_GOAL `~(p:real^3 IN ball (HD ul,sqrt (&2)))`);\r
3333  (ASM_SET_TAC[IN_DIFF]);\r
3334  (UP_ASM_TAC THEN ASM_REWRITE_TAC[HD;IN;ball;IN_ELIM_THM]);\r
3335 \r
3336  (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 1`;\r
3337    MCELL_EXPLICIT;mcell1]);\r
3338  (COND_CASES_TAC);\r
3339  (REWRITE_TAC[IN_DIFF]);\r
3340  (STRIP_TAC);\r
3341  (ASM_MESON_TAC[]);\r
3342  (SET_TAC[]);\r
3343 \r
3344 (* ======================================================================= *)\r
3345 \r
3346  (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 3`;\r
3347    MCELL_EXPLICIT;mcell3]);\r
3348  (COND_CASES_TAC);\r
3349 \r
3350  (NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\\r
3351                   dist (u0,s) = sqrt (&2) /\\r
3352                   mxi V ul = s:real^3)`);\r
3353  (MATCH_MP_TAC MXI_EXPLICIT_OLD);\r
3354  (ASM_REWRITE_TAC[]);\r
3355  (FIRST_X_ASSUM CHOOSE_TAC);\r
3356 \r
3357  (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC);\r
3358  (UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);\r
3359  (REWRITE_TAC[SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);\r
3360  (STRIP_TAC);\r
3361  (ABBREV_TAC `s2 = omega_list_n V [u0; u1; u2; u3:real^3] 2`);\r
3362  (ABBREV_TAC `s3 = omega_list_n V [u0; u1; u2; u3:real^3] 3`);\r
3363  (NEW_GOAL `p IN aff_ge {u0, u1} {s, s3:real^3}`);\r
3364  (ASM_MESON_TAC[]);\r
3365  (ABBREV_TAC  `vl = [u0;u1;u2:real^3]`);\r
3366  (NEW_GOAL `vl = truncate_simplex 2 ul:(real^3)list`);\r
3367  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2] THEN EXPAND_TAC "vl");\r
3368  (NEW_GOAL `barV V 2 vl`);\r
3369  (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);\r
3370  (EXISTS_TAC `3` THEN ASM_MESON_TAC[ARITH_RULE `2 <= 3`]);\r
3371  (NEW_GOAL `LENGTH (vl:(real^3)list) = 3 /\ CARD {u0,u1,u2:real^3} = 3`);\r
3372  (REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list vl`);\r
3373  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
3374  (REWRITE_TAC[ARITH_RULE `3 = 2 + 1`]);\r
3375  (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);\r
3376  (EXISTS_TAC `V:real^3->bool`);\r
3377  (ASM_REWRITE_TAC[]);\r
3378  (NEW_GOAL `s2:real^3 = omega_list V vl`);\r
3379  (EXPAND_TAC "s2" THEN EXPAND_TAC "vl"  THEN \r
3380    REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
3381  (MESON_TAC[OMEGA_LIST_TRUNCATE_2]);\r
3382 \r
3383  (NEW_GOAL `s2 = circumcenter {u0,u1,u2:real^3}`);\r
3384  (REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list vl`);\r
3385  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
3386  (REWRITE_TAC[ASSUME `s2 = omega_list V vl`]);\r
3387  (MATCH_MP_TAC Rogers.XNHPWAB1);\r
3388  (EXISTS_TAC `2` THEN REWRITE_TAC[IN]);\r
3389  (ASM_REWRITE_TAC[]);\r
3390  (ASM_MESON_TAC[]);\r
3391  (NEW_GOAL `dist (s2,u0:real^3) = hl (truncate_simplex 2 (ul:(real^3)list))`);\r
3392  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
3393  (REWRITE_TAC[GSYM (ASSUME `vl:(real^3)list = truncate_simplex 2 ul`)]);\r
3394  (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);\r
3395  (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);\r
3396  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
3397  (REWRITE_WITH `u0:real^3 = HD vl`);\r
3398  (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]);\r
3399  (MATCH_MP_TAC Rogers.HL_EQ_DIST0);\r
3400  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);\r
3401  (ASM_REWRITE_TAC[]);\r
3402 \r
3403  (NEW_GOAL `~(s = s2:real^3)`);\r
3404  (STRIP_TAC);\r
3405  (NEW_GOAL `dist (u0,s:real^3) < sqrt (&2)`);\r
3406  (ONCE_REWRITE_TAC[DIST_SYM]);\r
3407  (REWRITE_TAC[ASSUME `s = s2:real^3`]);\r
3408  (ASM_MESON_TAC[]);\r
3409  (ASM_REAL_ARITH_TAC);\r
3410 \r
3411  (NEW_GOAL `(s2:real^3) IN voronoi_list V vl`);\r
3412  (SIMP_TAC[ASSUME `s2 = omega_list V vl`]);\r
3413  (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);\r
3414  (EXISTS_TAC `2`);\r
3415  (ASM_REWRITE_TAC[]);\r
3416 \r
3417  (NEW_GOAL `(s3:real^3) IN voronoi_list V ul`);\r
3418  (REWRITE_WITH `s3 = omega_list V ul`);\r
3419  (EXPAND_TAC "s3" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; OMEGA_LIST]);\r
3420  (REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) - 1 = 3`]);\r
3421  (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);\r
3422  (EXISTS_TAC `3`);\r
3423  (ASM_REWRITE_TAC[]);\r
3424 \r
3425  (NEW_GOAL `(s3:real^3) IN voronoi_list V vl`);\r
3426  (MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET A) ==> a IN A`));\r
3427  (EXISTS_TAC `voronoi_list V ul`);\r
3428  (STRIP_TAC);\r
3429  (ASM_REWRITE_TAC[]);\r
3430  (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);\r
3431  (REWRITE_TAC[VORONOI_LIST;VORONOI_SET;voronoi_closed;set_of_list; \r
3432    SUBSET; IN_INTERS]);\r
3433  (ONCE_REWRITE_TAC[IN]);\r
3434  (REWRITE_TAC[IN_ELIM_THM]);\r
3435  (REPEAT STRIP_TAC);\r
3436  (FIRST_ASSUM MATCH_MP_TAC);\r
3437  (EXISTS_TAC `v:real^3`);\r
3438  (ASM_REWRITE_TAC[]);\r
3439  (UNDISCH_TAC `v IN {u0, u1, u2:real^3}`);\r
3440  (SET_TAC[]);\r
3441 \r
3442  (NEW_GOAL `s IN voronoi_list V vl`);\r
3443  (NEW_GOAL `convex (voronoi_list V vl)`);\r
3444  (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]);\r
3445  (UP_ASM_TAC THEN REWRITE_TAC[convex] THEN STRIP_TAC);\r
3446  (UNDISCH_TAC `between s (s2,s3:real^3)`);\r
3447  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
3448  (REPEAT STRIP_TAC);\r
3449  (ONCE_REWRITE_TAC[GSYM IN]);\r
3450  (REWRITE_TAC[ASSUME `s = u % s2 + v % s3:real^3`]);\r
3451  (FIRST_ASSUM MATCH_MP_TAC);\r
3452  (ASM_REWRITE_TAC[]);\r
3453 \r
3454  (NEW_GOAL `~ (s IN affine hull {u0,u1,u2:real^3})`);\r
3455  STRIP_TAC;\r
3456  (NEW_GOAL `(s:real^3 - s2) dot (s - s2) = &0`);\r
3457  (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);\r
3458  (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);\r
3459  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
3460  (MATCH_MP_TAC MHFTTZN4);\r
3461  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);\r
3462  (REPEAT STRIP_TAC);\r
3463  (ASM_REWRITE_TAC[]);\r
3464  (ASM_REWRITE_TAC[]);\r
3465  (ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]);\r
3466  (EXPAND_TAC "vl" THEN ASM_MESON_TAC[set_of_list]);\r
3467  (UP_ASM_TAC THEN REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0;\r
3468    NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);\r
3469  (ASM_REWRITE_TAC[]);\r
3470 \r
3471  (NEW_GOAL `~affine_dependent {u0, u1, u2, s:real^3}`);\r
3472  (ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {d,a,b,c}`]);\r
3473  (MATCH_MP_TAC AFFINE_INDEPENDENT_INSERT);\r
3474  (ASM_REWRITE_TAC[]);\r
3475  (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);\r
3476  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
3477  (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);\r
3478  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2` THEN ASM_REWRITE_TAC[]);\r
3479 \r
3480  (NEW_GOAL `s2 IN convex hull {u0, u1, u2:real^3}`);\r
3481  (REWRITE_WITH `s2 = omega_list V vl /\ {u0, u1, u2:real^3} = set_of_list vl`);\r
3482  (EXPAND_TAC "s2" THEN EXPAND_TAC "vl");\r
3483  (REWRITE_TAC[OMEGA_LIST_TRUNCATE_2;set_of_list]);\r
3484  (MATCH_MP_TAC Rogers.XNHPWAB2);\r
3485  (EXISTS_TAC `2`);\r
3486  (ASM_REWRITE_TAC[IN]);\r
3487  (ASM_MESON_TAC[]);\r
3488 \r
3489  (NEW_GOAL `~ (s3 IN affine hull {u0,u1,u2:real^3})`);\r
3490   STRIP_TAC;\r
3491  (NEW_GOAL `(s3:real^3 - s2) dot (s3 - s2) = &0`);\r
3492  (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]);\r
3493  (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`);\r
3494  (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]);\r
3495  (MATCH_MP_TAC MHFTTZN4);\r
3496  (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);\r
3497  (REPEAT STRIP_TAC);\r
3498  (ASM_REWRITE_TAC[]);\r
3499  (ASM_REWRITE_TAC[]);\r
3500  (ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]);\r
3501  (EXPAND_TAC "vl" THEN ASM_MESON_TAC[set_of_list]);\r
3502  (UP_ASM_TAC THEN REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0;\r
3503    NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]);\r
3504  (REPEAT STRIP_TAC);\r
3505  (UNDISCH_TAC `between s (s2,s3:real^3)`);\r
3506  (REWRITE_TAC[ASSUME `s3 = s2:real^3`]);\r
3507  (REWRITE_TAC[BETWEEN_REFL_EQ]);\r
3508  (ASM_MESON_TAC[]);\r
3509 \r
3510  (NEW_GOAL `DISJOINT {u0,u1} {s, s3:real^3}`);\r
3511  (REWRITE_TAC[DISJOINT]);\r
3512  (MATCH_MP_TAC (SET_RULE `~ (a IN s) /\ ~ (b IN s) ==> s INTER {a, b} = {}`));\r
3513  (REPEAT STRIP_TAC);\r
3514  (NEW_GOAL `s IN affine hull {u0, u1,u2:real^3}`);\r
3515  (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);\r
3516  (UP_ASM_TAC THEN SET_TAC[]);\r
3517  (ASM_MESON_TAC[]);\r
3518  (NEW_GOAL `s3 IN affine hull {u0, u1,u2:real^3}`);\r
3519  (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1);\r
3520  (UP_ASM_TAC THEN SET_TAC[]);\r
3521  (ASM_MESON_TAC[]);\r
3522  (UNDISCH_TAC `p IN aff_ge {u0, u1} {s, s3:real^3}`);\r
3523  (ASM_SIMP_TAC[AFF_GE_2_2]);\r
3524  (REWRITE_TAC[IN;IN_ELIM_THM]);\r
3525  (NEW_GOAL `?k1 k2. k1 + k2 = &1 /\ k2 <= &0 /\ k1 % s + k2 % s2 = s3:real^3`);\r
3526  (UNDISCH_TAC `between s (s2,s3:real^3)`);\r
3527  (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);\r
3528  (REPEAT STRIP_TAC);\r
3529  (EXISTS_TAC `&1 / v` THEN EXISTS_TAC ` -- u / v`);\r
3530  (NEW_GOAL `~(v = &0)`);\r
3531  (STRIP_TAC);\r
3532  (NEW_GOAL `s = s2:real^3`);\r
3533  (REWRITE_TAC[ASSUME `s = u % s2 + v % s3:real^3`]);\r
3534  (REWRITE_WITH `v = &0 /\ u = &1`);\r
3535  (ASM_REAL_ARITH_TAC);\r
3536  (VECTOR_ARITH_TAC);\r
3537  (ASM_MESON_TAC[]);\r
3538  (REPEAT STRIP_TAC);\r
3539  (REWRITE_TAC[REAL_ARITH `&1 / v + --u / v = (&1 - u) / v`]);\r
3540  (REWRITE_WITH `&1 - u = v`);\r
3541  (ASM_REAL_ARITH_TAC);\r
3542  (ASM_SIMP_TAC[REAL_DIV_REFL]);\r
3543  (REWRITE_TAC[REAL_ARITH `--u / v <= &0 <=> &0 <= u / v`]);\r
3544  (ASM_SIMP_TAC[REAL_LE_DIV]);\r
3545  (REWRITE_TAC[ASSUME `s = u % s2 + v % s3:real^3`]);\r
3546  (REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);\r
3547  (REWRITE_TAC[VECTOR_ARITH \r
3548  `((&1 / v * u) % s2 + (&1 / v * v) % s3) + --u / v % s2 = s3 <=> \r
3549   (v / v - &1) % s3 = vec 0`]);\r
3550  (REWRITE_WITH `v / v = &1`);\r
3551  (ASM_SIMP_TAC[REAL_DIV_REFL]);\r
3552  (VECTOR_ARITH_TAC);\r
3553  (FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC);\r
3554  (REWRITE_WITH `s3 = k1 % s + k2 % s2:real^3`);\r
3555  (ASM_REWRITE_TAC[]);\r
3556  (UNDISCH_TAC `s2 IN convex hull {u0, u1, u2:real^3}`);\r
3557  (REWRITE_TAC[CONVEX_HULL_3; IN_ELIM_THM; IN]);\r
3558  (REPEAT STRIP_TAC);\r
3559  (UP_ASM_TAC THEN REWRITE_TAC[ASSUME `s2 = u % u0 + v % u1 + w % u2:real^3`]);\r
3560  (REWRITE_TAC [VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);\r
3561  (REWRITE_TAC[VECTOR_ARITH `t1 % u0 + t2 % u1 + t3 % s + (t4 * k1) % s + \r
3562    ((t4 * k2) * u) % u0 + ((t4 * k2) * v) % u1 + \r
3563    ((t4 * k2) * w) % u2 = (t4 * k2 * w) % u2 +\r
3564   (t1 + t4 * k2 * u) % u0 + (t2 + t4 * k2 * v) % u1 + (t3 + t4 * k1) % s`]);\r
3565  (STRIP_TAC);\r
3566  (NEW_GOAL `t4 * k2 * w = &0`);\r
3567  (MATCH_MP_TAC AFFINE_DEPENDENT_KY_LEMMA1);\r
3568  (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `s:real^3` THEN EXISTS_TAC `p:real^3`);\r
3569  (EXISTS_TAC `t1 + t4 * k2 * u`);\r
3570  (EXISTS_TAC `t2 + t4 * k2 * v`);\r
3571  (EXISTS_TAC `t3 + t4 * k1`);\r
3572  (ASM_REWRITE_TAC[]);\r
3573  (REPEAT STRIP_TAC);\r
3574  (UP_ASM_TAC THEN REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE \r
3575  `{u2, u0, u1, s} = {u0, u1, u2, s}`]);\r
3576  (ASM_REWRITE_TAC[]);\r
3577  (ONCE_REWRITE_TAC[SET_RULE \r
3578  `{u2, u0, u1, s} = {s, u0, u1, u2}`]);\r
3579  (REWRITE_WITH `4 = SUC (CARD {u0,u1,u2:real^3})`);\r
3580  (ASM_REWRITE_TAC[]);\r
3581  (ARITH_TAC);\r
3582  (MATCH_MP_TAC (MESON[Geomdetail.CARD_CLAUSES_IMP] \r
3583   `!s a. FINITE s /\ ~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s)`));\r
3584  (REWRITE_TAC[Geomdetail.FINITE6]);\r
3585  (STRIP_TAC);\r
3586  (NEW_GOAL `s IN affine hull {u0, u1, u2:real^3}`);\r
3587  (UP_ASM_TAC THEN REWRITE_TAC[IN_AFFINE_KY_LEMMA1]);\r
3588  (ASM_MESON_TAC[]);\r
3589  (REWRITE_TAC[GSYM (ASSUME `p =\r
3590       (t4 * k2 * w) % u2 +\r
3591       (t1 + t4 * k2 * u) % u0 +\r
3592       (t2 + t4 * k2 * v) % u1 +\r
3593       (t3 + t4 * k1) % s:real^3`)]);\r
3594  (ONCE_REWRITE_TAC[SET_RULE \r
3595  `{u2, u0, u1, s} = {u0, u1, u2,s}`]);\r
3596  (ASM_REWRITE_TAC[]);\r
3597  (REWRITE_TAC[REAL_ARITH \r
3598   `t4 * k2 * w + (t1 + t4 * k2 * u) + (t2 + t4 * k2 * v) + t3 + t4 * k1 = \r
3599    t1 + t2 + t3 + t4 * (k1 + k2 * (u + v + w))`]);\r
3600  (ASM_REWRITE_TAC[REAL_MUL_RID]);\r
3601  (NEW_GOAL `&0 <= -- k2`);\r
3602  (ASM_REAL_ARITH_TAC);\r
3603  (REWRITE_TAC[REAL_ARITH `a * b * c <= &0 <=> &0 <= a * c * (-- b)`]);\r
3604  (ASM_SIMP_TAC[REAL_LE_MUL]);\r
3605  (NEW_GOAL `p IN affine hull {u0,u1,s:real^3}`);\r
3606  (REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);\r
3607  (EXISTS_TAC `t1 + t4 * k2 * u`);\r
3608  (EXISTS_TAC `t2 + t4 * k2 * v`);\r
3609  (EXISTS_TAC `t3 + t4 * k1`);\r
3610  (ASM_REWRITE_TAC[VECTOR_MUL_LZERO;VECTOR_ADD_LID]);\r
3611  (REWRITE_TAC[REAL_ARITH \r
3612   `(t1 + t4 * k2 * u) + (t2 + t4 * k2 * v) + t3 + t4 * k1 \r
3613   = (t1 + t2 + t3 + t4 * (k1 + k2 * (u + v + w))) - (t4 * k2 * w)`]);\r
3614  (ASM_REWRITE_TAC[REAL_MUL_RID]);\r
3615  (REAL_ARITH_TAC);\r
3616  (NEW_GOAL `~(p:real^3 IN B4)`);\r
3617  (ASM_SET_TAC[]);\r
3618  (UP_ASM_TAC THEN EXPAND_TAC "B4" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; HD;TL]);\r
3619  (REWRITE_WITH `mxi V [u0; u1; u2; u3] = s`);\r
3620  (ASM_MESON_TAC[]);\r
3621  (ASM_REWRITE_TAC[]);\r
3622  (SET_TAC[]);\r
3623 \r
3624  (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 2`);\r
3625  (GEN_TAC THEN STRIP_TAC);\r
3626  (NEW_GOAL `~(y = 4 \/ y = 0 \/ y = 1 \/ y = 3)`);\r
3627  (ASM_SIMP_TAC[]);\r
3628  (ASM_ARITH_TAC);\r
3629  (NEW_GOAL `i = 2`);\r
3630  (FIRST_ASSUM MATCH_MP_TAC);\r
3631  (ASM_REWRITE_TAC[]);\r
3632  (GEN_TAC THEN STRIP_TAC);\r
3633  (ASM_REWRITE_TAC[]);\r
3634  (FIRST_ASSUM MATCH_MP_TAC);\r
3635  (ASM_REWRITE_TAC[]);\r
3636 \r
3637 (* ===================================================================== *)\r
3638 \r
3639  (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> \r
3640                 ~ (y = 4 \/ y = 0 \/ y = 1 \/ y = 2)`);\r
3641  (REPEAT STRIP_TAC);\r
3642  (NEW_GOAL `mcell 4 V ul = {}`);\r
3643  (SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);\r
3644  (COND_CASES_TAC);\r
3645  (NEW_GOAL `F`);\r
3646  (ASM_MESON_TAC[]);\r
3647  (ASM_MESON_TAC[]);\r
3648  (REFL_TAC);\r
3649  (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 4`]);\r
3650  (REWRITE_TAC[ASSUME `mcell 4 V ul = {}`]);\r
3651  (SET_TAC[]);\r
3652 \r
3653  (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 0`;\r
3654    MCELL_EXPLICIT;mcell0]);\r
3655  (STRIP_TAC);\r
3656  (NEW_GOAL `~(p:real^3 IN ball (HD ul,sqrt (&2)))`);\r
3657  (ASM_SET_TAC[IN_DIFF]);\r
3658  (UP_ASM_TAC THEN ASM_REWRITE_TAC[HD;IN;ball;IN_ELIM_THM]);\r
3659 \r
3660  (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 1`;\r
3661    MCELL_EXPLICIT;mcell1]);\r
3662  (COND_CASES_TAC);\r
3663  (REWRITE_TAC[IN_DIFF]);\r
3664  (STRIP_TAC);\r
3665  (ASM_MESON_TAC[]);\r
3666  (SET_TAC[]);\r
3667 \r
3668  (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 2`;\r
3669    MCELL_EXPLICIT;mcell2]);\r
3670  (COND_CASES_TAC);\r
3671  (LET_TAC);\r
3672  (UNDISCH_TAC `~(p IN aff_ge {u0, u1} {mxi V ul, omega_list_n V ul 3})`);\r
3673  (REWRITE_TAC[IN_INTER; ASSUME `ul = [u0;u1;u2;u3:real^3]`;HD;TL]);\r
3674  (MESON_TAC[]);\r
3675  (SET_TAC[]);\r
3676 \r
3677  (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 3`);\r
3678  (GEN_TAC THEN STRIP_TAC);\r
3679  (NEW_GOAL `~(y = 4 \/ y = 0 \/ y = 1 \/ y = 2)`);\r
3680  (ASM_SIMP_TAC[]);\r
3681  (ASM_ARITH_TAC);\r
3682  (NEW_GOAL `i = 3`);\r
3683  (FIRST_ASSUM MATCH_MP_TAC);\r
3684  (ASM_REWRITE_TAC[]);\r
3685  (GEN_TAC THEN STRIP_TAC);\r
3686  (ASM_REWRITE_TAC[]);\r
3687  (FIRST_ASSUM MATCH_MP_TAC);\r
3688  (ASM_REWRITE_TAC[])]);;\r
3689 \r
3690 \r
3691 end;; \r
3692 \r