text_formalization/packing/NJIUTIU.hl

   1 (* ========================================================================= *)\r
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)\r
   3 (*                                                                           *)\r
   4 (*      Authour   : VU KHAC KY                                               *)\r
   5 (*      Book lemma: NJIUTIU                                                  *)\r
   6 (*      Chaper    : Packing (Marchal cells)                                  *)\r
   7 (*                                                                           *)\r
   8 (* ========================================================================= *)\r
   9 \r
  10 \r
  11 (* ========================================================================= *)\r
  12 \r
  13 module Njiutiu = struct\r
  14 \r
  15 open Rogers;;\r
  16 open Vukhacky_tactics;;\r
  17 open Pack_defs;;\r
  18 open Pack_concl;; \r
  19 open Pack1;;\r
  20 open Sphere;; \r
  21 open Marchal_cells;;\r
  22 open Emnwuus;;\r
  23 open Marchal_cells_2_new;;\r
  24 open Lepjbdj;;\r
  25 \r
  26 \r
  27 let NJIUTIU_concl = \r
  28  `!V ul vl.\r
  29          saturated V /\ packing V /\\r
  30          barV V 3 ul /\ barV V 3 vl /\\r
  31          rogers V ul = rogers V vl /\ aff_dim (rogers V ul) = &3 \r
  32         ==> (!i. 0 <= i /\ i <= 3 \r
  33                  ==> omega_list_n V ul i = omega_list_n V vl i)`;;\r
  34 \r
  35 (* ========================================================================= *)\r
  36 (* supporting lemmas *)\r
  37 \r
  38 let CLOSEST_POINT_SUBSET_lemma = prove_by_refinement (\r
  39  `!(a:real^3) x S P. \r
  40       (a = closest_point S x /\ a IN P /\ P SUBSET S /\ \r
  41        convex P /\ closed P /\ closed S /\ ~(P = {})) \r
  42      ==> (a = closest_point P x)`,\r
  43 [(REPEAT STRIP_TAC);\r
  44  (ABBREV_TAC `s = closest_point P (x:real^3)`);\r
  45  (ASM_CASES_TAC `~(a:real^3 = s)`);\r
  46  (NEW_GOAL `dist (x:real^3, s) < dist (x, a)`);\r
  47  (EXPAND_TAC "s");\r
  48  (MATCH_MP_TAC CLOSEST_POINT_LT);\r
  49  (ASM_MESON_TAC[]);\r
  50  (NEW_GOAL `s:real^3 IN P`);\r
  51  (EXPAND_TAC "s");\r
  52  (MATCH_MP_TAC CLOSEST_POINT_IN_SET);\r
  53  (ASM_REWRITE_TAC[]);\r
  54  (NEW_GOAL `dist (x, a) <= dist (x, s:real^3)`);\r
  55  (ASM_REWRITE_TAC[]);\r
  56  (MATCH_MP_TAC CLOSEST_POINT_LE);\r
  57  (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);\r
  58  (NEW_GOAL `F`);\r
  59  (ASM_REAL_ARITH_TAC);\r
  60  (ASM_MESON_TAC[]);\r
  61  (ASM_MESON_TAC[])]);;\r
  62 \r
  63 (* ---------------------------------------------------------------------------*)\r
  64 let AFF_DEPENDENT_AFF_DIM_4 = prove_by_refinement (\r
  65  `!a b c d:real^3. \r
  66    affine_dependent {a,b,c,d} ==> aff_dim {a,b,c,d} <= &2`,\r
  67 [(REWRITE_TAC[affine_dependent]);\r
  68  (REPEAT STRIP_TAC);\r
  69 \r
  70  (ASM_CASES_TAC `x = a:real^3`);\r
  71  (ONCE_REWRITE_TAC [AFF_DIM_INSERT]);\r
  72  (COND_CASES_TAC);\r
  73  (NEW_GOAL `aff_dim {b,c,d:real^3} <= &(CARD {b,c,d}) - &1`);\r
  74  (MATCH_MP_TAC AFF_DIM_LE_CARD);\r
  75  (REWRITE_TAC[Geomdetail.FINITE6]);\r
  76  (NEW_GOAL `&(CARD {b, c, d:real^3}) <= &3:int`);\r
  77  (REWRITE_TAC[INT_OF_NUM_LE; Geomdetail.CARD3]);\r
  78  (ASM_ARITH_TAC);\r
  79  (NEW_GOAL `F`);\r
  80  (NEW_GOAL `affine hull({a, b, c, d:real^3} DELETE x) \r
  81              SUBSET affine hull {b, c, d}`);\r
  82  (MATCH_MP_TAC AFFINE_SUBSET_KY_LEMMA);\r
  83  (ASM_REWRITE_TAC[] THEN SET_TAC[]);\r
  84  (ASM_SET_TAC[]);\r
  85  (ASM_MESON_TAC[]);\r
  86 \r
  87  (ASM_CASES_TAC `x = b:real^3`);\r
  88  (ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {b,a,c,d}`]);\r
  89  (ONCE_REWRITE_TAC [AFF_DIM_INSERT]);\r
  90  (COND_CASES_TAC);\r
  91  (NEW_GOAL `aff_dim {a,c,d:real^3} <= &(CARD {a,c,d}) - &1`);\r
  92  (MATCH_MP_TAC AFF_DIM_LE_CARD);\r
  93  (REWRITE_TAC[Geomdetail.FINITE6]);\r
  94  (NEW_GOAL `&(CARD {a, c, d:real^3}) <= &3:int`);\r
  95  (REWRITE_TAC[INT_OF_NUM_LE; Geomdetail.CARD3]);\r
  96  (ASM_ARITH_TAC);\r
  97  (NEW_GOAL `F`);\r
  98  (NEW_GOAL `affine hull({a, b, c, d:real^3} DELETE x) \r
  99              SUBSET affine hull {a, c, d}`);\r
 100  (MATCH_MP_TAC AFFINE_SUBSET_KY_LEMMA);\r
 101  (ASM_REWRITE_TAC[] THEN SET_TAC[]);\r
 102  (ASM_SET_TAC[]);\r
 103  (ASM_MESON_TAC[]);\r
 104 \r
 105  (ASM_CASES_TAC `x = c:real^3`);\r
 106  (ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {c,a,b,d}`]);\r
 107  (ONCE_REWRITE_TAC [AFF_DIM_INSERT]);\r
 108  (COND_CASES_TAC);\r
 109  (NEW_GOAL `aff_dim {a,b,d:real^3} <= &(CARD {a,b,d}) - &1`);\r
 110  (MATCH_MP_TAC AFF_DIM_LE_CARD);\r
 111  (REWRITE_TAC[Geomdetail.FINITE6]);\r
 112  (NEW_GOAL `&(CARD {a, b, d:real^3}) <= &3:int`);\r
 113  (REWRITE_TAC[INT_OF_NUM_LE; Geomdetail.CARD3]);\r
 114  (ASM_ARITH_TAC);\r
 115  (NEW_GOAL `F`);\r
 116  (NEW_GOAL `affine hull({a, b, c, d:real^3} DELETE x) \r
 117              SUBSET affine hull {a, b, d}`);\r
 118  (MATCH_MP_TAC AFFINE_SUBSET_KY_LEMMA);\r
 119  (ASM_REWRITE_TAC[] THEN SET_TAC[]);\r
 120  (ASM_SET_TAC[]);\r
 121  (ASM_MESON_TAC[]);\r
 122 \r
 123  (ASM_CASES_TAC `x = d:real^3`);\r
 124  (ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {d,a,b,c}`]);\r
 125  (ONCE_REWRITE_TAC [AFF_DIM_INSERT]);\r
 126  (COND_CASES_TAC);\r
 127  (NEW_GOAL `aff_dim {a,b,c:real^3} <= &(CARD {a,b,c}) - &1`);\r
 128  (MATCH_MP_TAC AFF_DIM_LE_CARD);\r
 129  (REWRITE_TAC[Geomdetail.FINITE6]);\r
 130  (NEW_GOAL `&(CARD {a, b,c:real^3}) <= &3:int`);\r
 131  (REWRITE_TAC[INT_OF_NUM_LE; Geomdetail.CARD3]);\r
 132  (ASM_ARITH_TAC);\r
 133  (NEW_GOAL `F`);\r
 134  (NEW_GOAL `affine hull({a, b, c, d:real^3} DELETE x) \r
 135              SUBSET affine hull {a, b, c}`);\r
 136  (MATCH_MP_TAC AFFINE_SUBSET_KY_LEMMA);\r
 137  (ASM_REWRITE_TAC[] THEN SET_TAC[]);\r
 138  (ASM_SET_TAC[]);\r
 139  (ASM_MESON_TAC[]);\r
 140 \r
 141  (NEW_GOAL `F`);\r
 142  (ASM_SET_TAC[]);\r
 143  (ASM_MESON_TAC[])]);;\r
 144 \r
 145 (* ========================================================================== *)\r
 146 (*        Main theorem                                                        *)\r
 147 (* ========================================================================== *)\r
 148 \r
 149 let NJIUTIU = prove_by_refinement (NJIUTIU_concl,\r
 150 \r
 151 [(REPEAT GEN_TAC THEN STRIP_TAC);\r
 152  (NEW_GOAL \r
 153  `rogers V ul =\r
 154   convex hull\r
 155     {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`);\r
 156  (ASM_MESON_TAC[ROGERS_EXPLICIT]);\r
 157  (NEW_GOAL \r
 158  `rogers V vl =\r
 159   convex hull\r
 160     {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`);\r
 161  (ASM_MESON_TAC[ROGERS_EXPLICIT]);\r
 162  (NEW_GOAL \r
 163   `{HD (ul:(real^3)list), omega_list_n V ul 1, omega_list_n V ul 2, \r
 164     omega_list_n V ul 3}\r
 165  = {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`);\r
 166  (REWRITE_WITH \r
 167  `{HD (ul:(real^3)list), omega_list_n V ul 1, omega_list_n V ul 2,\r
 168    omega_list_n V ul 3}\r
 169  = {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3} <=>\r
 170    convex hull \r
 171    {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}\r
 172  = convex hull \r
 173    {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`);\r
 174  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
 175  (MATCH_MP_TAC Packing3.CONVEX_HULL_EQ_EQ_SET_EQ);\r
 176  (REPEAT STRIP_TAC);\r
 177  (NEW_GOAL `aff_dim {HD (ul:(real^3)list), omega_list_n V ul 1, \r
 178                       omega_list_n V ul 2, omega_list_n V ul 3} <= &2`);\r
 179  (MATCH_MP_TAC AFF_DEPENDENT_AFF_DIM_4);\r
 180  (ASM_REWRITE_TAC[]);\r
 181  (UP_ASM_TAC THEN PURE_ONCE_REWRITE_TAC[GSYM AFF_DIM_CONVEX_HULL]);\r
 182  (REWRITE_TAC[GSYM (ASSUME `rogers V ul =\r
 183   convex hull\r
 184   {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`)]);\r
 185  (ASM_ARITH_TAC);\r
 186  (NEW_GOAL `aff_dim {HD (vl:(real^3)list), omega_list_n V vl 1, \r
 187                       omega_list_n V vl 2, omega_list_n V vl 3} <= &2`);\r
 188  (MATCH_MP_TAC AFF_DEPENDENT_AFF_DIM_4);\r
 189  (ASM_REWRITE_TAC[]);\r
 190  (UP_ASM_TAC THEN PURE_ONCE_REWRITE_TAC[GSYM AFF_DIM_CONVEX_HULL]);\r
 191  (REWRITE_TAC[GSYM (ASSUME `rogers V vl =\r
 192   convex hull\r
 193   {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`)]);\r
 194  (REWRITE_TAC[GSYM (ASSUME `rogers V ul = rogers V vl`)]);\r
 195  (ASM_ARITH_TAC);\r
 196  (ASM_MESON_TAC[]);\r
 197  (ABBREV_TAC `W = {HD (ul:(real^3)list), omega_list_n V ul 1, \r
 198                     omega_list_n V ul 2, omega_list_n V ul 3}`);\r
 199 \r
 200  (NEW_GOAL `!i j.\r
 201                   i < 4 /\ j < 4 /\ ~(i = j)\r
 202                   ==> ~(omega_list_n V ul i = omega_list_n V ul j)`);\r
 203  (MATCH_MP_TAC Rogers.ROGERS_AFF_DIM_FULL);\r
 204  (ASM_REWRITE_TAC[]);\r
 205  (NEW_GOAL \r
 206   `~(omega_list_n V ul 0 = omega_list_n V ul 1) /\\r
 207    ~(omega_list_n V ul 0 = omega_list_n V ul 2) /\\r
 208    ~(omega_list_n V ul 0 = omega_list_n V ul 3) /\\r
 209    ~(omega_list_n V ul 1 = omega_list_n V ul 2) /\\r
 210    ~(omega_list_n V ul 1 = omega_list_n V ul 3) /\\r
 211    ~(omega_list_n V ul 2 = omega_list_n V ul 3)`);\r
 212  (ASM_SIMP_TAC[ARITH_RULE \r
 213   `0 < 4 /\ 1 < 4 /\ 2 < 4 /\ 3 < 4 /\ ~(0 = 1) /\ ~(0 = 2) /\ ~(0 = 3) /\\r
 214    ~(1 = 2) /\ ~(2 = 3) /\ ~(1 = 3)`]);\r
 215 \r
 216  (NEW_GOAL `(omega_list_n V ul 1) IN voronoi_list V (truncate_simplex 1 ul)`);\r
 217  (MATCH_MP_TAC Packing3.OMEGA_LIST_N_IN_VORONOI_LIST);\r
 218  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);\r
 219  (NEW_GOAL `(omega_list_n V ul 2) IN voronoi_list V (truncate_simplex 2 ul)`);\r
 220  (MATCH_MP_TAC Packing3.OMEGA_LIST_N_IN_VORONOI_LIST);\r
 221  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
 222  (NEW_GOAL `(omega_list_n V ul 3) IN voronoi_list V (truncate_simplex 3 ul)`);\r
 223  (MATCH_MP_TAC Packing3.OMEGA_LIST_N_IN_VORONOI_LIST);\r
 224  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `3 <= 3`]);\r
 225  (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);\r
 226  (MATCH_MP_TAC BARV_3_EXPLICIT);\r
 227  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);\r
 228  (UP_ASM_TAC THEN STRIP_TAC);\r
 229  (NEW_GOAL `voronoi_list V (truncate_simplex 2 ul) SUBSET \r
 230              voronoi_list V (truncate_simplex 1 ul) /\ \r
 231              voronoi_list V (truncate_simplex 3 ul) SUBSET \r
 232              voronoi_list V (truncate_simplex 1 ul) /\ \r
 233              voronoi_list V (truncate_simplex 3 ul) SUBSET \r
 234              voronoi_list V (truncate_simplex 2 ul)`);\r
 235  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1; TRUNCATE_SIMPLEX_EXPLICIT_2; TRUNCATE_SIMPLEX_EXPLICIT_3; VORONOI_LIST;VORONOI_SET; set_of_list]);\r
 236  (SET_TAC[]);\r
 237  (UP_ASM_TAC THEN STRIP_TAC);\r
 238 \r
 239  (NEW_GOAL `!i j.\r
 240                   i < 4 /\ j < 4 /\ ~(i = j)\r
 241                   ==> ~(omega_list_n V vl i = omega_list_n V vl j)`);\r
 242  (MATCH_MP_TAC Rogers.ROGERS_AFF_DIM_FULL);\r
 243  (ASM_MESON_TAC[]);\r
 244  (NEW_GOAL \r
 245   `~(omega_list_n V vl 0 = omega_list_n V vl 1) /\\r
 246    ~(omega_list_n V vl 0 = omega_list_n V vl 2) /\\r
 247    ~(omega_list_n V vl 0 = omega_list_n V vl 3) /\\r
 248    ~(omega_list_n V vl 1 = omega_list_n V vl 2) /\\r
 249    ~(omega_list_n V vl 1 = omega_list_n V vl 3) /\\r
 250    ~(omega_list_n V vl 2 = omega_list_n V vl 3)`);\r
 251  (ASM_SIMP_TAC[ARITH_RULE \r
 252   `0 < 4 /\ 1 < 4 /\ 2 < 4 /\ 3 < 4 /\ ~(0 = 1) /\ ~(0 = 2) /\ ~(0 = 3) /\\r
 253    ~(1 = 2) /\ ~(2 = 3) /\ ~(1 = 3)`]);\r
 254 \r
 255  (NEW_GOAL `(omega_list_n V vl 1) IN voronoi_list V (truncate_simplex 1 vl)`);\r
 256  (MATCH_MP_TAC Packing3.OMEGA_LIST_N_IN_VORONOI_LIST);\r
 257  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);\r
 258  (NEW_GOAL `(omega_list_n V vl 2) IN voronoi_list V (truncate_simplex 2 vl)`);\r
 259  (MATCH_MP_TAC Packing3.OMEGA_LIST_N_IN_VORONOI_LIST);\r
 260  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);\r
 261  (NEW_GOAL `(omega_list_n V vl 3) IN voronoi_list V (truncate_simplex 3 vl)`);\r
 262  (MATCH_MP_TAC Packing3.OMEGA_LIST_N_IN_VORONOI_LIST);\r
 263  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `3 <= 3`]);\r
 264  (NEW_GOAL `?v0 v1 v2 v3. vl = [v0;v1;v2;v3:real^3]`);\r
 265  (MATCH_MP_TAC BARV_3_EXPLICIT);\r
 266  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);\r
 267  (UP_ASM_TAC THEN STRIP_TAC);\r
 268  (NEW_GOAL `voronoi_list V (truncate_simplex 2 vl) SUBSET \r
 269              voronoi_list V (truncate_simplex 1 vl) /\ \r
 270              voronoi_list V (truncate_simplex 3 vl) SUBSET \r
 271              voronoi_list V (truncate_simplex 1 vl) /\ \r
 272              voronoi_list V (truncate_simplex 3 vl) SUBSET \r
 273              voronoi_list V (truncate_simplex 2 vl)`);\r
 274  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1; TRUNCATE_SIMPLEX_EXPLICIT_2; TRUNCATE_SIMPLEX_EXPLICIT_3; VORONOI_LIST;VORONOI_SET; set_of_list]);\r
 275  (SET_TAC[]);\r
 276  (UP_ASM_TAC THEN STRIP_TAC);\r
 277 \r
 278  (NEW_GOAL `HD (ul:(real^3)list) = HD vl`);\r
 279  (MATCH_MP_TAC ROGERS_INTER_V_LEMMA);\r
 280  (EXISTS_TAC `V:real^3->bool`);\r
 281  (REPEAT STRIP_TAC);\r
 282  (ASM_REWRITE_TAC[]);\r
 283  (ASM_REWRITE_TAC[]);\r
 284  (ASM_REWRITE_TAC[]);\r
 285  (NEW_GOAL `set_of_list ul SUBSET (V:real^3->bool)`);\r
 286  (MATCH_MP_TAC Packing3.BARV_SUBSET);\r
 287  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);\r
 288  (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list; HD] THEN SET_TAC[]);\r
 289  (REWRITE_TAC[GSYM (ASSUME `rogers V ul = rogers V vl`)]);\r
 290  (ONCE_REWRITE_TAC[MESON[IN] `rogers V ul s <=> s IN rogers V ul`]);\r
 291  (REWRITE_WITH `rogers V ul =\r
 292              convex hull\r
 293              {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V\r
 294                                                                ul\r
 295                                                                3}`);\r
 296  (ASM_SIMP_TAC[ROGERS_EXPLICIT]);\r
 297  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);\r
 298  (SET_TAC[]);\r
 299  (NEW_GOAL `omega_list_n V ul 0 = omega_list_n V vl 0`);\r
 300  (REWRITE_TAC[OMEGA_LIST_N]);\r
 301  (ASM_MESON_TAC[]);\r
 302 \r
 303 (* Case 1: i = 1 *)\r
 304  (NEW_GOAL `omega_list_n V ul 1 = omega_list_n V vl 1`);\r
 305  (REWRITE_WITH `omega_list_n V ul 1 = \r
 306       closest_point (convex hull (W DIFF {HD ul})) (omega_list_n V ul 0)`);\r
 307  (MATCH_MP_TAC CLOSEST_POINT_SUBSET_lemma);\r
 308  (EXISTS_TAC `voronoi_list V (truncate_simplex (SUC 0) ul)`);\r
 309  (REPEAT STRIP_TAC); (* 7 subgoals *)\r
 310 \r
 311  (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `1 = SUC 0`]); (* finish subgoal 1 *)\r
 312  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);\r
 313  (EXPAND_TAC "W");\r
 314  (REWRITE_WITH `HD ul = omega_list_n V ul 0`);\r
 315  (REWRITE_TAC[OMEGA_LIST_N]);\r
 316  (ASM_SET_TAC[]);                                      (* finish subgoal 2 *)\r
 317 \r
 318  (NEW_GOAL `voronoi_list V (truncate_simplex (SUC 0) ul) = \r
 319              convex hull (voronoi_list V (truncate_simplex (SUC 0) ul))`);\r
 320  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
 321  (REWRITE_TAC[CONVEX_HULL_EQ;Packing3.CONVEX_VORONOI_LIST]);\r
 322  (ONCE_REWRITE_TAC[ASSUME \r
 323   `voronoi_list V (truncate_simplex (SUC 0) ul) = \r
 324    convex hull (voronoi_list V (truncate_simplex (SUC 0) ul))`]);\r
 325  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);\r
 326  (REWRITE_WITH `W:real^3->bool DIFF {HD ul} = \r
 327   {omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`);\r
 328  (EXPAND_TAC "W" THEN REWRITE_WITH `HD ul = omega_list_n V ul 0`);\r
 329  (REWRITE_TAC[OMEGA_LIST_N]);\r
 330  (ASM_SET_TAC[]);\r
 331  (REWRITE_TAC[ARITH_RULE `SUC 0 = 1`]);\r
 332  (ASM_SET_TAC[]);                                       (* finish subgoal 3 *)\r
 333  (REWRITE_TAC[CONVEX_CONVEX_HULL]);                     (* finish subgoal 4 *)\r
 334  (MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);       \r
 335  (MATCH_MP_TAC FINITE_DIFF);\r
 336  (EXPAND_TAC "W" THEN REWRITE_TAC[Geomdetail.FINITE6]); (* finish subgoal 5 *)\r
 337  (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);           (* finish subgoal 6 *)\r
 338  (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_EQ_EMPTY]);\r
 339  (EXPAND_TAC "W" THEN REWRITE_WITH `HD ul = omega_list_n V ul 0`);\r
 340  (REWRITE_TAC[OMEGA_LIST_N]);\r
 341  (ASM_SET_TAC[]);                                       (* finish subgoal 7 *)\r
 342 \r
 343  (REWRITE_WITH `omega_list_n V vl 1 = \r
 344       closest_point (convex hull (W DIFF {HD vl})) (omega_list_n V vl 0)`);\r
 345  (MATCH_MP_TAC CLOSEST_POINT_SUBSET_lemma);\r
 346  (EXISTS_TAC `voronoi_list V (truncate_simplex (SUC 0) vl)`);\r
 347  (REPEAT STRIP_TAC); (* 7 subgoals *)\r
 348 \r
 349  (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `1 = SUC 0`]); (* finish subgoal 1 *)\r
 350  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);\r
 351  (EXPAND_TAC "W");\r
 352  (REWRITE_WITH `HD vl = omega_list_n V vl 0`);\r
 353  (REWRITE_TAC[OMEGA_LIST_N]);\r
 354  (ASM_SET_TAC[]);                                      (* finish subgoal 2 *)\r
 355 \r
 356  (NEW_GOAL `voronoi_list V (truncate_simplex (SUC 0) vl) = \r
 357              convex hull (voronoi_list V (truncate_simplex (SUC 0) vl))`);\r
 358  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
 359  (REWRITE_TAC[CONVEX_HULL_EQ;Packing3.CONVEX_VORONOI_LIST]);\r
 360  (ONCE_REWRITE_TAC[ASSUME \r
 361   `voronoi_list V (truncate_simplex (SUC 0) vl) = \r
 362    convex hull (voronoi_list V (truncate_simplex (SUC 0) vl))`]);\r
 363  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);\r
 364  (REWRITE_WITH `W:real^3->bool DIFF {HD vl} = \r
 365   {omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`);\r
 366  (REWRITE_TAC[ASSUME `W:real^3->bool = \r
 367   {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`]);\r
 368  (REWRITE_WITH `HD vl = omega_list_n V vl 0`);\r
 369  (REWRITE_TAC[OMEGA_LIST_N]);\r
 370  (ASM_SET_TAC[]);\r
 371 \r
 372  (REWRITE_TAC[ARITH_RULE `SUC 0 = 1`]);\r
 373  (ASM_SET_TAC[]);                                       (* finish subgoal 3 *)\r
 374  (REWRITE_TAC[CONVEX_CONVEX_HULL]);                     (* finish subgoal 4 *)\r
 375  (MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);       \r
 376  (MATCH_MP_TAC FINITE_DIFF);\r
 377  (EXPAND_TAC "W" THEN REWRITE_TAC[Geomdetail.FINITE6]); (* finish subgoal 5 *)\r
 378  (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);           (* finish subgoal 6 *)\r
 379  (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_EQ_EMPTY]);\r
 380  (REWRITE_TAC[ASSUME `W:real^3->bool = \r
 381   {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`]);\r
 382  (REWRITE_WITH `HD vl = omega_list_n V vl 0`);\r
 383  (REWRITE_TAC[OMEGA_LIST_N]);\r
 384  (ASM_SET_TAC[]);                                       (* finish subgoal 7 *)\r
 385  (ASM_MESON_TAC[]);\r
 386  (* ------------------------------------------------------------------------- *)\r
 387 (* Case 2: i = 2 *)\r
 388  (NEW_GOAL `omega_list_n V ul 2 = omega_list_n V vl 2`);\r
 389  (REWRITE_WITH `omega_list_n V ul 2 = \r
 390       closest_point (convex hull (W DIFF {HD ul, omega_list_n V ul 1})) (omega_list_n V ul 1)`);\r
 391  (MATCH_MP_TAC CLOSEST_POINT_SUBSET_lemma);\r
 392  (EXISTS_TAC `voronoi_list V (truncate_simplex (SUC 1) ul)`);\r
 393  (REPEAT STRIP_TAC); (* 7 subgoals *)\r
 394 \r
 395  (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `2 = SUC 1`]); (* finish subgoal 1 *)\r
 396  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);\r
 397  (EXPAND_TAC "W");\r
 398  (REWRITE_WITH `HD ul = omega_list_n V ul 0`);\r
 399  (REWRITE_TAC[OMEGA_LIST_N]);\r
 400  (ASM_SET_TAC[]);                                      (* finish subgoal 2 *)\r
 401 \r
 402  (NEW_GOAL `voronoi_list V (truncate_simplex (SUC 1) ul) = \r
 403              convex hull (voronoi_list V (truncate_simplex (SUC 1) ul))`);\r
 404  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
 405  (REWRITE_TAC[CONVEX_HULL_EQ;Packing3.CONVEX_VORONOI_LIST]);\r
 406  (ONCE_REWRITE_TAC[ASSUME \r
 407   `voronoi_list V (truncate_simplex (SUC 1) ul) = \r
 408    convex hull (voronoi_list V (truncate_simplex (SUC 1) ul))`]);\r
 409  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);\r
 410  (REWRITE_WITH `W:real^3->bool DIFF {HD ul, omega_list_n V ul 1} = \r
 411   {omega_list_n V ul 2, omega_list_n V ul 3}`);\r
 412  (EXPAND_TAC "W" THEN REWRITE_WITH `HD ul = omega_list_n V ul 0`);\r
 413  (REWRITE_TAC[OMEGA_LIST_N]);\r
 414  (ASM_SET_TAC[]);\r
 415  (REWRITE_TAC[ARITH_RULE `SUC 1 = 2`]);\r
 416  (ASM_SET_TAC[]);                                       (* finish subgoal 3 *)\r
 417  (REWRITE_TAC[CONVEX_CONVEX_HULL]);                     (* finish subgoal 4 *)\r
 418  (MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);       \r
 419  (MATCH_MP_TAC FINITE_DIFF);\r
 420  (EXPAND_TAC "W" THEN REWRITE_TAC[Geomdetail.FINITE6]); (* finish subgoal 5 *)\r
 421  (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);           (* finish subgoal 6 *)\r
 422  (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_EQ_EMPTY]);\r
 423  (EXPAND_TAC "W" THEN REWRITE_WITH `HD ul = omega_list_n V ul 0`);\r
 424  (REWRITE_TAC[OMEGA_LIST_N]);\r
 425  (ASM_SET_TAC[]);                                       (* finish subgoal 7 *)\r
 426 \r
 427  (REWRITE_WITH \r
 428  `omega_list_n V vl 2 = \r
 429   closest_point (convex hull (W DIFF {HD vl,  omega_list_n V vl 1}))   \r
 430  (omega_list_n V vl 1)`);\r
 431  (MATCH_MP_TAC CLOSEST_POINT_SUBSET_lemma);\r
 432  (EXISTS_TAC `voronoi_list V (truncate_simplex (SUC 1) vl)`);\r
 433  (REPEAT STRIP_TAC); (* 7 subgoals *)\r
 434 \r
 435  (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `2 = SUC 1`]); (* finish subgoal 1 *)\r
 436  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);\r
 437  (REWRITE_TAC[ASSUME `W:real^3->bool = \r
 438   {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`]);\r
 439  (REWRITE_WITH `HD vl = omega_list_n V vl 0`);\r
 440  (REWRITE_TAC[OMEGA_LIST_N]);\r
 441  (ASM_SET_TAC[]);                                      (* finish subgoal 2 *)\r
 442 \r
 443  (NEW_GOAL `voronoi_list V (truncate_simplex (SUC 1) vl) = \r
 444              convex hull (voronoi_list V (truncate_simplex (SUC 1) vl))`);\r
 445  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
 446  (REWRITE_TAC[CONVEX_HULL_EQ;Packing3.CONVEX_VORONOI_LIST]);\r
 447  (ONCE_REWRITE_TAC[ASSUME \r
 448   `voronoi_list V (truncate_simplex (SUC 1) vl) = \r
 449    convex hull (voronoi_list V (truncate_simplex (SUC 1) vl))`]);\r
 450  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);\r
 451  (REWRITE_WITH `W:real^3->bool DIFF {HD vl, omega_list_n V vl 1} = \r
 452                  {omega_list_n V vl 2, omega_list_n V vl 3}`);\r
 453  (REWRITE_TAC[ASSUME `W:real^3->bool = \r
 454   {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`]);\r
 455  (REWRITE_WITH `HD vl = omega_list_n V vl 0`);\r
 456  (REWRITE_TAC[OMEGA_LIST_N]);\r
 457  (ASM_SET_TAC[]);\r
 458 \r
 459  (REWRITE_TAC[ARITH_RULE `SUC 1 = 2`]);\r
 460  (ASM_SET_TAC[]);                                       (* finish subgoal 3 *)\r
 461  (REWRITE_TAC[CONVEX_CONVEX_HULL]);                     (* finish subgoal 4 *)\r
 462  (MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);       \r
 463  (MATCH_MP_TAC FINITE_DIFF);\r
 464  (EXPAND_TAC "W" THEN REWRITE_TAC[Geomdetail.FINITE6]); (* finish subgoal 5 *)\r
 465  (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);           (* finish subgoal 6 *)\r
 466  (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_EQ_EMPTY]);\r
 467  (REWRITE_TAC[ASSUME `W:real^3->bool = \r
 468   {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`]);\r
 469  (REWRITE_WITH `HD vl = omega_list_n V vl 0`);\r
 470  (REWRITE_TAC[OMEGA_LIST_N]);\r
 471  (ASM_SET_TAC[]);                                       (* finish subgoal 7 *)\r
 472  (ASM_MESON_TAC[]);\r
 473 \r
 474 (* ------------------------------------------------------------------------- *)\r
 475 (* Case 3: i = 3 *)\r
 476  (NEW_GOAL `omega_list_n V ul 3 = omega_list_n V vl 3`);\r
 477  (REWRITE_WITH \r
 478    `omega_list_n V ul 3 = closest_point \r
 479       (convex hull (W DIFF {HD ul, omega_list_n V ul 1, omega_list_n V ul 2}))\r
 480       (omega_list_n V ul 2)`);\r
 481  (MATCH_MP_TAC CLOSEST_POINT_SUBSET_lemma);\r
 482  (EXISTS_TAC `voronoi_list V (truncate_simplex (SUC 2) ul)`);\r
 483  (REPEAT STRIP_TAC); (* 7 subgoals *)\r
 484 \r
 485  (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `3 = SUC 2`]); (* finish subgoal 1 *)\r
 486  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);\r
 487  (EXPAND_TAC "W");\r
 488  (REWRITE_WITH `HD ul = omega_list_n V ul 0`);\r
 489  (REWRITE_TAC[OMEGA_LIST_N]);\r
 490  (ASM_SET_TAC[]);                                      (* finish subgoal 2 *)\r
 491 \r
 492  (NEW_GOAL `voronoi_list V (truncate_simplex (SUC 2) ul) = \r
 493              convex hull (voronoi_list V (truncate_simplex (SUC 2) ul))`);\r
 494  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
 495  (REWRITE_TAC[CONVEX_HULL_EQ;Packing3.CONVEX_VORONOI_LIST]);\r
 496  (ONCE_REWRITE_TAC[ASSUME \r
 497   `voronoi_list V (truncate_simplex (SUC 2) ul) = \r
 498    convex hull (voronoi_list V (truncate_simplex (SUC 2) ul))`]);\r
 499  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);\r
 500  (REWRITE_WITH \r
 501   `W:real^3->bool DIFF {HD ul, omega_list_n V ul 1, omega_list_n V ul 2} = \r
 502   {omega_list_n V ul 3}`);\r
 503  (EXPAND_TAC "W" THEN REWRITE_WITH `HD ul = omega_list_n V ul 0`);\r
 504  (REWRITE_TAC[OMEGA_LIST_N]);\r
 505  (ASM_SET_TAC[]);\r
 506  (REWRITE_TAC[ARITH_RULE `SUC 2 = 3`]);\r
 507  (ASM_SET_TAC[]);                                       (* finish subgoal 3 *)\r
 508  (REWRITE_TAC[CONVEX_CONVEX_HULL]);                     (* finish subgoal 4 *)\r
 509  (MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);       \r
 510  (MATCH_MP_TAC FINITE_DIFF);\r
 511  (EXPAND_TAC "W" THEN REWRITE_TAC[Geomdetail.FINITE6]); (* finish subgoal 5 *)\r
 512  (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);           (* finish subgoal 6 *)\r
 513  (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_EQ_EMPTY]);\r
 514  (EXPAND_TAC "W" THEN REWRITE_WITH `HD ul = omega_list_n V ul 0`);\r
 515  (REWRITE_TAC[OMEGA_LIST_N]);\r
 516  (ASM_SET_TAC[]);                                       (* finish subgoal 7 *)\r
 517 \r
 518  (REWRITE_WITH \r
 519  `omega_list_n V vl 3 = \r
 520   closest_point \r
 521   (convex hull (W DIFF {HD vl,  omega_list_n V vl 1, omega_list_n V vl 2}))\r
 522   (omega_list_n V vl 2)`);\r
 523  (MATCH_MP_TAC CLOSEST_POINT_SUBSET_lemma);\r
 524  (EXISTS_TAC `voronoi_list V (truncate_simplex (SUC 2) vl)`);\r
 525  (REPEAT STRIP_TAC); (* 7 subgoals *)\r
 526 \r
 527  (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `3 = SUC 2`]); (* finish subgoal 1 *)\r
 528  (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);\r
 529  (REWRITE_TAC[ASSUME `W:real^3->bool = \r
 530   {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`]);\r
 531  (REWRITE_WITH `HD vl = omega_list_n V vl 0`);\r
 532  (REWRITE_TAC[OMEGA_LIST_N]);\r
 533  (ASM_SET_TAC[]);                                      (* finish subgoal 2 *)\r
 534 \r
 535  (NEW_GOAL `voronoi_list V (truncate_simplex (SUC 2) vl) = \r
 536              convex hull (voronoi_list V (truncate_simplex (SUC 2) vl))`);\r
 537  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
 538  (REWRITE_TAC[CONVEX_HULL_EQ;Packing3.CONVEX_VORONOI_LIST]);\r
 539  (ONCE_REWRITE_TAC[ASSUME \r
 540   `voronoi_list V (truncate_simplex (SUC 2) vl) = \r
 541    convex hull (voronoi_list V (truncate_simplex (SUC 2) vl))`]);\r
 542  (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);\r
 543  (REWRITE_WITH \r
 544   `W:real^3->bool DIFF {HD vl, omega_list_n V vl 1, omega_list_n V vl 2} \r
 545    = {omega_list_n V vl 3}`);\r
 546  (REWRITE_TAC[ASSUME `W:real^3->bool = \r
 547   {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`]);\r
 548  (REWRITE_WITH `HD vl = omega_list_n V vl 0`);\r
 549  (REWRITE_TAC[OMEGA_LIST_N]);\r
 550  (ASM_SET_TAC[]);\r
 551 \r
 552  (REWRITE_TAC[ARITH_RULE `SUC 2 = 3`]);\r
 553  (ASM_SET_TAC[]);                                       (* finish subgoal 3 *)\r
 554  (REWRITE_TAC[CONVEX_CONVEX_HULL]);                     (* finish subgoal 4 *)\r
 555  (MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);       \r
 556  (MATCH_MP_TAC FINITE_DIFF);\r
 557  (EXPAND_TAC "W" THEN REWRITE_TAC[Geomdetail.FINITE6]); (* finish subgoal 5 *)\r
 558  (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);           (* finish subgoal 6 *)\r
 559  (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_EQ_EMPTY]);\r
 560  (REWRITE_TAC[ASSUME `W:real^3->bool = \r
 561   {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`]);\r
 562  (REWRITE_WITH `HD vl = omega_list_n V vl 0`);\r
 563  (REWRITE_TAC[OMEGA_LIST_N]);\r
 564  (ASM_SET_TAC[]);                                       (* finish subgoal 7 *)\r
 565  (ASM_MESON_TAC[]);\r
 566  (REPEAT STRIP_TAC);\r
 567  (ASM_CASES_TAC `i = 0`);\r
 568  (ASM_MESON_TAC[]);\r
 569  (ASM_CASES_TAC `i = 1`);\r
 570  (ASM_MESON_TAC[]);\r
 571  (ASM_CASES_TAC `i = 2`);\r
 572  (ASM_MESON_TAC[]);\r
 573  (ASM_CASES_TAC `i = 3`);\r
 574  (ASM_MESON_TAC[]);\r
 575  (NEW_GOAL `F`);\r
 576  (ASM_ARITH_TAC);\r
 577  (ASM_MESON_TAC[])]);;\r
 578 \r
 579 \r
 580 end;;\r
 581 \r