text_formalization/packing/AJRIPQN.hl

   1 (* ========================================================================= *)
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   3 (*                                                                           *)
   4 (*      Authour   : VU KHAC KY                                               *)
   5 (*      Book lemma: AJRIPQN                                                  *)
   6 (*      Chaper    : Packing                                                  *)
   7 (*                                                                           *)
   8 (* ========================================================================= *)
   9
  10
  11 module Ajripqn = struct
  12
  13 open Rogers;;
  14 open Vukhacky_tactics;;
  15 open Pack_defs;;
  16 open Pack_concl;;
  17 open Pack1;;
  18 open Sphere;;
  19 open Marchal_cells;;
  20 open Emnwuus;;
  21 open Marchal_cells_2_new;;
  22 open Lepjbdj;;
  23 open Hdtfnfz;;
  24 open Urrphbz1;;
  25 open Sltstlo;;
  26 open Qzksykg;;
  27 open Rvfxzbu;;
  28 open Ddzuphj;;
  29
  30 (* ========================================================================= *)
  31
  32 let AJRIPQN_concl =
  33 `!V ul vl i j.
  34     saturated V /\ packing V /\ barV V 3 ul /\ barV V 3 vl /\
  35     i IN {0,1,2,3,4} /\ j IN {0,1,2,3,4} /\
  36     ~NULLSET (mcell i V ul INTER mcell j V vl) ==>
  37     i = j /\ mcell i V ul = mcell j V vl`;;
  38
  39 (* ========================================================================= *)
  40 (*     Supported lemmas                                                      *)
  41
  42 let VOL_POS_LT_AFF_DIM_3 = prove_by_refinement (
  43  `!S:real^3->bool. measurable S /\ &0 < vol S ==> aff_dim S = &3`,
  44 [(REPEAT STRIP_TAC);
  45  (NEW_GOAL `aff_dim (S:real^3->bool) <= &(dimindex (:3))`);
  46  (ASM_REWRITE_TAC[AFF_DIM_LE_UNIV]);
  47  (UP_ASM_TAC THEN REWRITE_TAC[DIMINDEX_3] THEN STRIP_TAC);
  48  (ASM_CASES_TAC `aff_dim (S:real^3->bool) <= &2`);
  49  (NEW_GOAL `negligible (S:real^3->bool)`);
  50  (MATCH_MP_TAC COPLANAR_IMP_NEGLIGIBLE);
  51  (MATCH_MP_TAC Rogers.AFF_DIM_LE_2_IMP_COPLANAR);
  52  (ASM_REWRITE_TAC[]);
  53  (NEW_GOAL `vol (S:real^3->bool) = &0`);
  54  (NEW_GOAL `(!Z:real^3->bool. NULLSET Z ==> vol Z = &0)`);
  55  (MESON_TAC[volume_props]);
  56  (ASM_MESON_TAC[]);
  57  (NEW_GOAL `F`);
  58  (ASM_REAL_ARITH_TAC);
  59  (ASM_MESON_TAC[]);
  60  (ASM_ARITH_TAC)]);;
  61
  62 let UP_TO_4_KY_LEMMA = prove (`!i. i <= 4 <=> i IN {0,1,2,3,4}`,
  63  REWRITE_TAC[SET_RULE `i IN {0,1,2,3,4} <=>
  64             (i = 0 \/ i = 1 \/ i = 2 \/ i = 3 \/i= 4)`] THEN ARITH_TAC);;
  65
  66 let FINITE_SET_LIST_LEMMA = prove
  67  (`!s:A->bool.
  68        FINITE s
  69        ==> FINITE
  70         {y | ?u0 u1 u2 u3.
  71                u0 IN s /\
  72                u1 IN s /\
  73                u2 IN s /\
  74                u3 IN s /\
  75                y = [u0; u1; u2; u3]}`,
  76  REWRITE_TAC[SET_RULE
  77   `{y | ?u0 u1 u2 u3. u0 IN s /\ u1 IN s /\ u2 IN s /\ u3 IN s /\
  78                       y = [u0; u1; u2; u3]} =
  79    {CONS u0 y1 | u0 IN s /\
  80                  y1 IN {CONS u1 y2 | u1 IN s /\
  81                                      y2 IN {[u2;u3] | u2 IN s /\
  82                                                       u3 IN s}}}`] THEN
  83   REPEAT(GEN_TAC THEN DISCH_TAC THEN
  84         MATCH_MP_TAC FINITE_PRODUCT_DEPENDENT THEN ASM_REWRITE_TAC[]));;
  85
  86 (* ========================================================================= *)
  87 (* Main theorem *)
  88
  89 let AJRIPQN = prove_by_refinement (AJRIPQN_concl,
  90
  91 [(REPEAT GEN_TAC THEN STRIP_TAC);
  92
  93  (ABBREV_TAC `S = mcell i V ul INTER mcell j V vl`);
  94  (UNDISCH_TAC `~NULLSET (S:real^3->bool)`);
  95  (REWRITE_WITH `~NULLSET (S:real^3->bool) <=> &0 < measure S`);
  96  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
  97  (MATCH_MP_TAC MEASURABLE_MEASURE_POS_LT);
  98  (EXPAND_TAC "S" THEN MATCH_MP_TAC MEASURABLE_INTER);
  99  (ASM_SIMP_TAC[MEASURABLE_MCELL]);
 100
 101  (DISCH_TAC);
 102  (NEW_GOAL `bounded (S:real^3->bool)`);
 103  (EXPAND_TAC "S" THEN MATCH_MP_TAC BOUNDED_INTER);
 104  (ASM_SIMP_TAC[BOUNDED_MCELL]);
 105  (UP_ASM_TAC THEN REWRITE_TAC[bounded]);
 106  (STRIP_TAC);
 107
 108  (NEW_GOAL `?(v:real^3) S1.
 109     v IN V /\ S1 SUBSET S /\ measurable S1 /\ &0 < measure S1 /\
 110     S1 SUBSET (voronoi_closed V v)`);
 111  (ABBREV_TAC `SP = {v:real^3 | v IN V /\
 112                                 ~(voronoi_closed V v INTER S = {})}`);
 113  (NEW_GOAL `FINITE (SP:(real^3->bool))`);
 114  (NEW_GOAL `SP SUBSET (V INTER ball ((vec 0):real^3, a + &2))`);
 115  (EXPAND_TAC "SP" THEN REWRITE_TAC[SUBSET;IN_INTER;IN;IN_ELIM_THM; ball]);
 116  (REPEAT STRIP_TAC);
 117  (ASM_REWRITE_TAC[]);
 118  (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE `~(A = {}) <=> (?z. z IN A)`]);
 119  (REWRITE_TAC[IN_INTER]);
 120  (REPEAT STRIP_TAC);
 121  (REWRITE_TAC[dist; NORM_ARITH `norm (vec 0 - a) = norm a`]);
 122  (NEW_GOAL `norm x <= norm z + dist (x , z:real^3)`);
 123  (REWRITE_TAC[dist] THEN NORM_ARITH_TAC);
 124  (NEW_GOAL `norm (z:real^3) <= a`);
 125  (FIRST_ASSUM MATCH_MP_TAC);
 126  (ASM_REWRITE_TAC[]);
 127  (NEW_GOAL `dist (x, z:real^3) < &2`);
 128  (ONCE_REWRITE_TAC[DIST_SYM]);
 129  (MATCH_MP_TAC Pack2.voronoi_in_ball);
 130  (EXISTS_TAC `V:real^3->bool`);
 131  (ASM_REWRITE_TAC[]);
 132  (ASM_REAL_ARITH_TAC);
 133
 134  (MATCH_MP_TAC FINITE_SUBSET);
 135  (EXISTS_TAC `V INTER ball ((vec 0):real^3,a + &2)`);
 136  (ASM_REWRITE_TAC[]);
 137  (MATCH_MP_TAC KIUMVTC);
 138  (ASM_REWRITE_TAC[]);
 139  (NEW_GOAL `~((S:real^3->bool) = {})`);
 140  (STRIP_TAC);
 141  (UNDISCH_TAC `&0 < vol (S:real^3->bool)`);
 142  (ASM_REWRITE_TAC[MEASURE_EMPTY]);
 143  (REAL_ARITH_TAC);
 144  (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE `~(A = {}) <=> (?z. z IN A)`]);
 145  (REPEAT STRIP_TAC);
 146  (NEW_GOAL `norm (z:real^3) <= a`);
 147  (FIRST_ASSUM MATCH_MP_TAC);
 148  (ASM_REWRITE_TAC[]);
 149  (NEW_GOAL `&0 <= norm (z:real^3)`);
 150  (REWRITE_TAC[NORM_POS_LE]);
 151  (ASM_REAL_ARITH_TAC);
 152
 153  (ABBREV_TAC `f = (\v:real^3. voronoi_closed V v INTER S)`);
 154  (ABBREV_TAC `SPP = IMAGE (f:(real^3->real^3->bool)) (SP:real^3->bool)`);
 155  (NEW_GOAL `FINITE (SPP:(real^3->bool)->bool)`);
 156  (EXPAND_TAC "SPP" THEN MATCH_MP_TAC FINITE_IMAGE THEN ASM_REWRITE_TAC[]);
 157  (NEW_GOAL `(S:real^3->bool) = (UNIONS SPP)`);
 158  (EXPAND_TAC "SPP" THEN REWRITE_TAC[SET_EQ_LEMMA; UNIONS_IMAGE;IN;IN_ELIM_THM]
 159    THEN REPEAT STRIP_TAC);
 160  (EXPAND_TAC "f");
 161  (NEW_GOAL `?v:real^3. v IN V /\ x IN voronoi_closed V v`);
 162  (MATCH_MP_TAC Packing3.TIWWFYQ);
 163  (ASM_REWRITE_TAC[]);
 164  (UP_ASM_TAC THEN REPEAT STRIP_TAC);
 165  (EXISTS_TAC `v:real^3`);
 166  (STRIP_TAC);
 167  (EXPAND_TAC "SP" THEN REWRITE_TAC[IN_ELIM_THM]);
 168  (ASM_REWRITE_TAC[]);
 169  (REWRITE_TAC[SET_RULE `~(A = {}) <=> (?z. z IN A)`]);
 170  (EXISTS_TAC `x:real^3`);
 171  (REWRITE_TAC[IN_INTER]);
 172  (ASM_REWRITE_TAC[]);
 173  (ASM_SET_TAC[]);
 174  (ONCE_REWRITE_TAC[GSYM IN]);
 175  (REWRITE_TAC[IN_INTER]);
 176  (ASM_SET_TAC[]);
 177  (UP_ASM_TAC THEN EXPAND_TAC "f");
 178  (REWRITE_WITH `(voronoi_closed V x' INTER S) (x:real^3)
 179    <=> x IN (voronoi_closed V x' INTER S)`);
 180  (MESON_TAC[GSYM IN]);
 181  (REWRITE_TAC[IN_INTER]);
 182  (ASM_SET_TAC[]);
 183
 184  (NEW_GOAL `!s1. s1 IN SPP ==> measurable (s1:(real^3->bool))`);
 185  (EXPAND_TAC "SPP" THEN EXPAND_TAC "f" THEN REWRITE_TAC[IMAGE;IN;
 186    IN_ELIM_THM]);
 187  (REPEAT STRIP_TAC);
 188  (ONCE_ASM_REWRITE_TAC[]);
 189  (MATCH_MP_TAC MEASURABLE_INTER);
 190  (STRIP_TAC);
 191  (ASM_SIMP_TAC[Packing3.DRUQUFE]);
 192  (EXPAND_TAC "S");
 193  (MATCH_MP_TAC MEASURABLE_INTER);
 194  (ASM_SIMP_TAC[MEASURABLE_MCELL]);
 195
 196
 197  (NEW_GOAL `?S1:real^3->bool. S1 IN SPP /\ ~(negligible S1)`);
 198  (ONCE_REWRITE_TAC[MESON[] `S <=> ~S ==> F`]);
 199  (STRIP_TAC);
 200  (NEW_GOAL `!S1:real^3->bool. S1 IN SPP ==> negligible S1`);
 201  (UP_ASM_TAC THEN MESON_TAC[]);
 202  (NEW_GOAL `negligible (UNIONS (SPP:(real^3->bool)->bool))`);
 203  (MATCH_MP_TAC NEGLIGIBLE_UNIONS);
 204  (ASM_REWRITE_TAC[]);
 205  (UP_ASM_TAC THEN REWRITE_TAC[GSYM (ASSUME `S:real^3->bool = UNIONS SPP`)]);
 206  (REWRITE_WITH `~NULLSET S <=> &0 < measure (S:real^3->bool)`);
 207  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 208  (MATCH_MP_TAC MEASURABLE_MEASURE_POS_LT);
 209  (EXPAND_TAC "S");
 210  (MATCH_MP_TAC MEASURABLE_INTER);
 211  (ASM_SIMP_TAC[MEASURABLE_MCELL]);
 212  (ASM_REWRITE_TAC[]);
 213  (FIRST_X_ASSUM CHOOSE_TAC);
 214
 215  (UP_ASM_TAC THEN EXPAND_TAC "SPP" THEN EXPAND_TAC "f" THEN
 216    REWRITE_TAC[IMAGE;IN;IN_ELIM_THM]);
 217  (EXPAND_TAC "SP" THEN REWRITE_TAC[IN;IN_ELIM_THM;
 218    SET_RULE `~(s = {}) <=> (?x. x IN s)`]);
 219  (REPEAT STRIP_TAC);
 220  (EXISTS_TAC `x:real^3`);
 221  (EXISTS_TAC `S1:real^3->bool`);
 222  (REPEAT STRIP_TAC);
 223  (ASM_REWRITE_TAC[]);
 224  (ASM_SET_TAC[]);
 225  (ONCE_ASM_REWRITE_TAC[]);
 226  (MATCH_MP_TAC MEASURABLE_INTER);
 227  (STRIP_TAC);
 228  (ASM_SIMP_TAC[Packing3.DRUQUFE]);
 229  (EXPAND_TAC "S");
 230  (MATCH_MP_TAC MEASURABLE_INTER);
 231  (ASM_SIMP_TAC[MEASURABLE_MCELL]);
 232
 233  (REWRITE_WITH `&0 < measure (S1:real^3->bool) <=> ~NULLSET S1`);
 234  (MATCH_MP_TAC MEASURABLE_MEASURE_POS_LT);
 235  (ONCE_ASM_REWRITE_TAC[]);
 236  (MATCH_MP_TAC MEASURABLE_INTER);
 237  (STRIP_TAC);
 238  (ASM_SIMP_TAC[Packing3.DRUQUFE]);
 239  (EXPAND_TAC "S");
 240  (MATCH_MP_TAC MEASURABLE_INTER);
 241  (ASM_SIMP_TAC[MEASURABLE_MCELL]);
 242  (ASM_REWRITE_TAC[]);
 243  (ASM_SET_TAC[]);
 244  (UP_ASM_TAC THEN STRIP_TAC);
 245 (* ======================================================================== *)
 246 (* OK here *)
 247
 248  (NEW_GOAL `?wl:(real^3)list S2.
 249     barV V 3 wl /\ S2 SUBSET S1 /\ measurable S2 /\
 250    &0 < measure S2 /\ S2 SUBSET (rogers V wl)`);
 251
 252  (ABBREV_TAC
 253   `SP = {wl| wl IN barV V 3 /\ HD wl = v /\ ~(rogers V wl INTER S1 = {})}`);
 254  (NEW_GOAL `FINITE (SP:((real^3)list->bool))`);
 255  (ABBREV_TAC `H = {u:real^3| u IN V /\ dist (u,v) <= &4}`);
 256  (NEW_GOAL `SP SUBSET
 257    {wl | ?u0 u1 u2 u3.
 258    u0 IN H /\ u1 IN H /\ u2 IN H /\ u3 IN H /\ wl = [u0;u1;u2;u3:real^3]}`);
 259  (EXPAND_TAC "SP" THEN REWRITE_TAC[SUBSET;IN;IN_ELIM_THM]);
 260  (REPEAT STRIP_TAC);
 261  (NEW_GOAL `?u0 u1 u2 u3. x = [u0:real^3;u1;u2;u3]`);
 262  (MP_TAC (ASSUME `barV V 3 x`));
 263  (REWRITE_TAC[BARV_3_EXPLICIT]);
 264  (FIRST_X_ASSUM CHOOSE_TAC);
 265  (FIRST_X_ASSUM CHOOSE_TAC);
 266  (FIRST_X_ASSUM CHOOSE_TAC);
 267  (FIRST_X_ASSUM CHOOSE_TAC);
 268  (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
 269  (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
 270  (ASM_REWRITE_TAC[]);
 271  (NEW_GOAL `omega_list V x IN voronoi_list V x`);
 272  (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST);
 273  (EXISTS_TAC `3`);
 274  (ASM_REWRITE_TAC[]);
 275  (ABBREV_TAC `u = omega_list V x`);
 276  (UNDISCH_TAC `(u:real^3) IN voronoi_list V x` THEN ASM_REWRITE_TAC[]);
 277  (NEW_GOAL `u0 = v:real^3`);
 278  (EXPAND_TAC "v" THEN REWRITE_TAC[ASSUME `x = [u0;u1;u2;u3:real^3]`;HD]);
 279  (DISCH_TAC THEN EXPAND_TAC "H" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 280  (NEW_GOAL `set_of_list (x:(real^3)list) SUBSET V`);
 281  (MATCH_MP_TAC Packing3.BARV_SUBSET);
 282  (EXISTS_TAC `3`);
 283  (ASM_REWRITE_TAC[]);
 284  (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list]);
 285  (DISCH_TAC);
 286  (REWRITE_WITH `V v /\ (V:real^3->bool) u1 /\ V u2 /\ V (u3:real^3)`);
 287  (UP_ASM_TAC THEN SET_TAC[]);
 288  (NEW_GOAL `!z. z IN {v, u1, u2, u3:real^3} ==> dist (z,v) <= &4`);
 289  (NEW_GOAL `!z. z IN {v, u1, u2, u3:real^3} ==> dist (z,u) <= &2`);
 290  (REPEAT STRIP_TAC);
 291  (ASM_CASES_TAC `dist (z,u:real^3) <= &2`);
 292  (ASM_REWRITE_TAC[]);
 293  (UNDISCH_TAC `saturated (V:real^3->bool)`);
 294  (REWRITE_TAC[saturated]);
 295  (REPEAT STRIP_TAC);
 296  (NEW_GOAL `?y. y IN V /\ dist (u, y:real^3) < &2`);
 297  (ASM_REWRITE_TAC[]);
 298  (UP_ASM_TAC THEN STRIP_TAC);
 299  (NEW_GOAL `u IN voronoi_closed V (z:real^3)`);
 300  (UNDISCH_TAC `u IN voronoi_list V [u0; u1; u2; u3:real^3]`);
 301  (REWRITE_TAC[VORONOI_LIST;VORONOI_SET; set_of_list; IN_INTERS]);
 302  (STRIP_TAC);
 303  (FIRST_ASSUM MATCH_MP_TAC);
 304  (ASM_SET_TAC[]);
 305  (ONCE_REWRITE_TAC[DIST_SYM]);
 306  (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed; IN;IN_ELIM_THM]);
 307  (STRIP_TAC);
 308  (NEW_GOAL `dist (u,z:real^3) <= dist (u,y)`);
 309  (FIRST_ASSUM MATCH_MP_TAC);
 310  (ASM_SET_TAC[]);
 311  (ASM_REAL_ARITH_TAC);
 312  (REPEAT STRIP_TAC);
 313  (NEW_GOAL `dist (z, v) <= dist (z, u) + dist (v, u:real^3)`);
 314  (NORM_ARITH_TAC);
 315  (NEW_GOAL `dist (z,u:real^3) <= &2`);
 316  (FIRST_ASSUM MATCH_MP_TAC);
 317  (ASM_SET_TAC[]);
 318  (NEW_GOAL `dist (v,u:real^3) <= &2`);
 319  (FIRST_ASSUM MATCH_MP_TAC);
 320  (SET_TAC[]);
 321  (ASM_REAL_ARITH_TAC);
 322  (ASM_SIMP_TAC[SET_RULE
 323   `a IN {a,b,c,d} /\ b IN {a,b,c,d} /\ c IN {a,b,c,d} /\ d IN {a,b,c,d}`]);
 324  (MATCH_MP_TAC FINITE_SUBSET);
 325  (EXISTS_TAC `{wl | ?a b c d.
 326    a IN H /\ b IN H /\ c IN H /\ d IN H /\ wl = [a;b;c;d:real^3]}`);
 327  (ASM_REWRITE_TAC[]);
 328
 329  (MATCH_MP_TAC FINITE_SET_LIST_LEMMA);
 330  (EXPAND_TAC "H");
 331  (MATCH_MP_TAC FINITE_SUBSET);
 332  (EXISTS_TAC `V INTER ball (v:real^3, &5)`);
 333  (ASM_SIMP_TAC[KIUMVTC; REAL_ARITH `&0 <= &5`]);
 334  (EXPAND_TAC "H" THEN REWRITE_TAC[SUBSET; ball; IN_INTER; IN;IN_ELIM_THM]);
 335  (REPEAT STRIP_TAC);
 336  (ASM_REWRITE_TAC[]);
 337  (ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REAL_ARITH_TAC);
 338  (ABBREV_TAC `f = (\wl:(real^3)list. rogers V wl INTER S1)`);
 339  (ABBREV_TAC `SPP = IMAGE (f:((real^3)list->real^3->bool))
 340   (SP:(real^3)list->bool)`);
 341  (NEW_GOAL `FINITE (SPP:(real^3->bool)->bool)`);
 342  (EXPAND_TAC "SPP" THEN MATCH_MP_TAC FINITE_IMAGE THEN ASM_REWRITE_TAC[]);
 343
 344  (NEW_GOAL `(S1:real^3->bool) = (UNIONS SPP)`);
 345  (EXPAND_TAC "SPP" THEN REWRITE_TAC[SET_EQ_LEMMA; UNIONS_IMAGE;IN;IN_ELIM_THM]
 346    THEN REPEAT STRIP_TAC);
 347  (EXPAND_TAC "f");
 348  (NEW_GOAL `?vl. vl IN barV V 3 /\
 349                     x IN rogers V vl /\
 350                     truncate_simplex 0 vl = [v]`);
 351  (REWRITE_WITH `(?vl. vl IN barV V 3 /\ x IN rogers V vl /\
 352    truncate_simplex 0 vl = [v]) <=>  x IN voronoi_closed V v`);
 353  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 354  (MATCH_MP_TAC Rogers.GLTVHUM);
 355  (ASM_REWRITE_TAC[]);
 356  (ASM_SET_TAC[]);
 357  (UP_ASM_TAC THEN STRIP_TAC);
 358  (EXISTS_TAC `vl':(real^3)list`);
 359  (STRIP_TAC);
 360  (EXPAND_TAC "SP" THEN REWRITE_TAC[IN_ELIM_THM]);
 361  (ASM_REWRITE_TAC[]);
 362
 363  (NEW_GOAL `?u0 u1 u2 u3. vl' = [u0:real^3;u1;u2;u3]`);
 364  (SUBGOAL_THEN `barV V 3 vl'` MP_TAC);
 365  (ASM_SET_TAC[]);
 366  (REWRITE_TAC[BARV_3_EXPLICIT]);
 367  (FIRST_X_ASSUM CHOOSE_TAC);
 368  (FIRST_X_ASSUM CHOOSE_TAC);
 369  (FIRST_X_ASSUM CHOOSE_TAC);
 370  (FIRST_X_ASSUM CHOOSE_TAC);
 371  (NEW_GOAL `v = u0:real^3`);
 372  (UNDISCH_TAC `truncate_simplex 0 vl' = [v:real^3]`);
 373  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_0]);
 374  (STRIP_TAC);
 375  (NEW_GOAL `v = HD [v:real^3] /\ u0 = HD [u0:real^3]`);
 376  (REWRITE_TAC[HD]);
 377  (ONCE_ASM_REWRITE_TAC[]);
 378  (AP_TERM_TAC THEN ASM_REWRITE_TAC[]);
 379  (STRIP_TAC);
 380  (ASM_REWRITE_TAC[HD]);
 381  (REWRITE_TAC[SET_RULE `~(x = {}) <=> (?y. y IN x)`]);
 382  (EXISTS_TAC `x:real^3`);
 383  (REWRITE_TAC[IN_INTER]);
 384  (ASM_REWRITE_TAC[IN]);
 385  (REWRITE_WITH `(rogers V vl' INTER S1) x <=> x IN rogers V vl'/\ x IN S1`);
 386  (REWRITE_TAC[IN; GSYM IN_INTER]);
 387  (ASM_REWRITE_TAC[IN]);
 388  (UNDISCH_TAC `(f:(real^3)list->real^3->bool) x' x`);
 389  (EXPAND_TAC "f");
 390  (REWRITE_WITH `(rogers V x' INTER S1) x <=> x IN rogers V x'/\ x IN S1`);
 391  (REWRITE_TAC[IN; GSYM IN_INTER]);
 392  (SET_TAC[]);
 393
 394
 395  (NEW_GOAL `!s1. s1 IN SPP ==> measurable (s1:(real^3->bool))`);
 396  (EXPAND_TAC "SPP" THEN EXPAND_TAC "f" THEN REWRITE_TAC[IMAGE;IN;
 397    IN_ELIM_THM]);
 398  (REPEAT STRIP_TAC);
 399  (ONCE_ASM_REWRITE_TAC[]);
 400  (MATCH_MP_TAC MEASURABLE_INTER);
 401  (STRIP_TAC);
 402  (MATCH_MP_TAC MEASURABLE_ROGERS);
 403  (ASM_REWRITE_TAC[]);
 404  (UNDISCH_TAC `(SP:(real^3)list->bool) x`);
 405  (EXPAND_TAC "SP" THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC);
 406  (ASM_SET_TAC[]);
 407  (ASM_REWRITE_TAC[]);
 408
 409  (NEW_GOAL `?S2:real^3->bool. S2 IN SPP /\ ~(negligible S2)`);
 410  (ONCE_REWRITE_TAC[MESON[] `S <=> ~S ==> F`]);
 411  (STRIP_TAC);
 412  (NEW_GOAL `!S2:real^3->bool. S2 IN SPP ==> negligible S2`);
 413  (UP_ASM_TAC THEN MESON_TAC[]);
 414  (NEW_GOAL `negligible (UNIONS (SPP:(real^3->bool)->bool))`);
 415  (MATCH_MP_TAC NEGLIGIBLE_UNIONS);
 416  (ASM_REWRITE_TAC[]);
 417  (UP_ASM_TAC THEN REWRITE_TAC[GSYM (ASSUME `S1:real^3->bool = UNIONS SPP`)]);
 418  (REWRITE_WITH `~NULLSET S1 <=> &0 < measure (S1:real^3->bool)`);
 419  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 420  (MATCH_MP_TAC MEASURABLE_MEASURE_POS_LT);
 421  (ASM_REWRITE_TAC[]);
 422  (ASM_REWRITE_TAC[]);
 423
 424  (FIRST_X_ASSUM CHOOSE_TAC);
 425  (UP_ASM_TAC THEN EXPAND_TAC "SPP" THEN EXPAND_TAC "f" THEN
 426    REWRITE_TAC[IMAGE;IN;IN_ELIM_THM]);
 427  (EXPAND_TAC "SP" THEN REWRITE_TAC[IN;IN_ELIM_THM;
 428    SET_RULE `~(s = {}) <=> (?x. x IN s)`]);
 429  (REPEAT STRIP_TAC);
 430  (EXISTS_TAC `x:(real^3)list`);
 431  (EXISTS_TAC `S2:real^3->bool`);
 432  (REPEAT STRIP_TAC);
 433  (ASM_REWRITE_TAC[]);
 434  (ASM_SET_TAC[]);
 435  (ONCE_ASM_REWRITE_TAC[]);
 436  (MATCH_MP_TAC MEASURABLE_INTER);
 437  (STRIP_TAC);
 438  (MATCH_MP_TAC MEASURABLE_ROGERS);
 439  (ASM_REWRITE_TAC[]);
 440  (ASM_REWRITE_TAC[]);
 441  (REWRITE_WITH `&0 < measure (S2:real^3->bool) <=> ~NULLSET S2`);
 442  (MATCH_MP_TAC MEASURABLE_MEASURE_POS_LT);
 443  (ONCE_ASM_REWRITE_TAC[]);
 444  (MATCH_MP_TAC MEASURABLE_INTER);
 445  (STRIP_TAC);
 446  (MATCH_MP_TAC MEASURABLE_ROGERS);
 447  (ASM_REWRITE_TAC[]);
 448  (ASM_REWRITE_TAC[]);
 449  (ASM_REWRITE_TAC[]);
 450  (ASM_SET_TAC[]);
 451  (UP_ASM_TAC THEN STRIP_TAC);
 452
 453 (* ======================================================================== *)
 454 (* ----------------------------- *)
 455 (* OK here *)
 456
 457  (NEW_GOAL
 458   `?S3. S3 SUBSET S2 /\
 459         measurable S3 /\
 460         &0 < vol S3 /\
 461        (!kl. barV V 3 kl /\ ~(rogers V kl = rogers V wl) ==> S3 INTER rogers V kl = {})`);
 462  (ABBREV_TAC
 463   `SP = {kl| kl IN barV V 3 /\ ~(rogers V kl INTER S2 = {})}`);
 464  (NEW_GOAL `FINITE (SP:((real^3)list->bool))`);
 465  (ABBREV_TAC `H = {u:real^3| u IN V /\ dist (u,HD wl) <= &12}`);
 466  (NEW_GOAL `SP SUBSET
 467    {kl | ?u0 u1 u2 u3.
 468    u0 IN H /\ u1 IN H /\ u2 IN H /\ u3 IN H /\ kl = [u0;u1;u2;u3:real^3]}`);
 469  (EXPAND_TAC "SP" THEN REWRITE_TAC[SUBSET;IN;IN_ELIM_THM]);
 470  (REPEAT STRIP_TAC);
 471  (NEW_GOAL `?u0 u1 u2 u3. x = [u0:real^3;u1;u2;u3]`);
 472  (MP_TAC (ASSUME `barV V 3 x`));
 473  (REWRITE_TAC[BARV_3_EXPLICIT]);
 474  (FIRST_X_ASSUM CHOOSE_TAC);
 475  (FIRST_X_ASSUM CHOOSE_TAC);
 476  (FIRST_X_ASSUM CHOOSE_TAC);
 477  (FIRST_X_ASSUM CHOOSE_TAC);
 478  (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
 479  (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
 480  (ASM_REWRITE_TAC[]);
 481  (NEW_GOAL `set_of_list x SUBSET (V:real^3 ->bool)`);
 482  (MATCH_MP_TAC Packing3.BARV_SUBSET);
 483  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 484  (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list]);
 485   DISCH_TAC;
 486  (NEW_GOAL `!u. u IN {u0,u1,u2,u3} ==> dist (u, u0:real^3) <= &4`);
 487  (REPEAT STRIP_TAC);
 488  (NEW_GOAL `aff_dim (voronoi_list V (x:(real^3)list)) + &(LENGTH x) = &4`);
 489  (UNDISCH_TAC `barV V 3 x` THEN REWRITE_TAC[BARV;VORONOI_NONDG]);
 490  (STRIP_TAC);
 491  (MATCH_MP_TAC (MESON[] `
 492    LENGTH x < 5 /\ set_of_list x SUBSET (V:real^3->bool) /\ A ==> A`));
 493  (FIRST_ASSUM MATCH_MP_TAC);
 494  (REWRITE_TAC[Packing3.INITIAL_SUBLIST_REFL]);
 495  (ASM_REWRITE_TAC[]);
 496  (ARITH_TAC);
 497  (NEW_GOAL `LENGTH (x:(real^3)list) = 4`);
 498  (MATCH_MP_TAC (MESON[] `A /\ CARD (set_of_list (x:(real^3)list)) = 3 + 1 ==> A`));
 499  (REWRITE_TAC[ARITH_RULE `4 = 3 + 1`]);
 500  (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
 501  (EXISTS_TAC `V:real^3->bool`);
 502  (ASM_REWRITE_TAC[]);
 503  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 504  (REWRITE_TAC[ARITH_RULE `(a:int) + &4 = &4 <=> a = &0`; AFF_DIM_EQ_0]);
 505  (REPEAT STRIP_TAC);
 506
 507  (NEW_GOAL `!p. p IN {u0, u1, u2, u3:real^3} ==> dist (a', p) <= &2`);
 508  (REPEAT STRIP_TAC);
 509  (NEW_GOAL `a' IN voronoi_closed V (p:real^3)`);
 510  (SWITCH_TAC THEN UP_ASM_TAC THEN REWRITE_TAC[VORONOI_LIST;VORONOI_SET; set_of_list; INTERS]);
 511  (MATCH_MP_TAC (SET_RULE `(s IN A ==> B) ==> (A = {s} ==> B)`));
 512  (REWRITE_TAC[IN;IN_ELIM_THM]);
 513  (REPEAT STRIP_TAC);
 514  (FIRST_ASSUM MATCH_MP_TAC);
 515  (EXISTS_TAC `p:real^3`);
 516  (STRIP_TAC);
 517  (ASM_MESON_TAC[IN]);
 518  (REWRITE_TAC[ETA_AX]);
 519  (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed;IN;IN_ELIM_THM] THEN DISCH_TAC);
 520  (NEW_GOAL `?y. y IN V /\ dist (a',y:real^3) < &2`);
 521  (ASM_MESON_TAC[saturated]);
 522  (FIRST_X_ASSUM CHOOSE_TAC);
 523  (MATCH_MP_TAC (REAL_ARITH `m <= dist (a', y:real^3) /\
 524                              dist (a', y:real^3) < b ==> m <= b`));
 525  (ASM_REWRITE_TAC[]);
 526  (FIRST_ASSUM MATCH_MP_TAC);
 527  (ASM_MESON_TAC[IN]);
 528  (NEW_GOAL `dist (u, u0) <= dist (a', u) + dist (a', u0:real^3)`);
 529  (NORM_ARITH_TAC);
 530  (NEW_GOAL `dist (a', u) <= &2 /\ dist (a', u0:real^3) <= &2`);
 531  (ASM_SIMP_TAC[]);
 532  (FIRST_ASSUM MATCH_MP_TAC);
 533  (SET_TAC[]);
 534  (ASM_REAL_ARITH_TAC);
 535  (NEW_GOAL `u0 IN {u0, u1, u2, u3:real^3} /\ u1 IN {u0, u1, u2, u3} /\
 536              u2 IN {u0, u1, u2, u3} /\ u3 IN {u0, u1, u2, u3}`);
 537  (SET_TAC[]);
 538  (EXPAND_TAC "H");
 539  (REWRITE_TAC[IN_ELIM_THM]);
 540  (REWRITE_WITH `(u0:real^3) IN V /\ u1 IN V /\ u2 IN V /\ u3 IN V`);
 541  (ASM_SET_TAC[]);
 542  (NEW_GOAL `!u. u IN {u0,u1,u2,u3} ==> dist (u:real^3, HD wl) <= &12`);
 543  (UNDISCH_TAC `~(rogers V x INTER S2 = {})`);
 544  (REWRITE_TAC[SET_RULE `~(s = {}) <=> (?p. p IN s)`]);
 545  (REPEAT STRIP_TAC);
 546  (NEW_GOAL `dist (u,HD wl) <= dist (u,u0:real^3) + dist (u0, p) + dist (p, HD wl)`);
 547  (NORM_ARITH_TAC);
 548  (NEW_GOAL `dist (u,u0:real^3) <= &4 /\ dist (u0,p) <= &4 /\ dist (p,HD wl) <= &4`);
 549  (ASM_SIMP_TAC[]);
 550  (STRIP_TAC);
 551  (SUBGOAL_THEN `p IN rogers V x` ASSUME_TAC);
 552  (ASM_SET_TAC[]);
 553  (NEW_GOAL `p IN voronoi_closed V (u0:real^3)`);
 554  (REWRITE_WITH `p IN voronoi_closed V u0 <=>
 555                    (?vl. vl IN barV V 3 /\
 556                     p IN rogers V vl /\
 557                     truncate_simplex 0 vl = [u0])`);
 558  (MATCH_MP_TAC Rogers.GLTVHUM);
 559  (ASM_REWRITE_TAC[]);
 560  (ASM_SET_TAC[]);
 561  (EXISTS_TAC `x:(real^3)list`);
 562  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_0]);
 563  (ASM_MESON_TAC[IN]);
 564  (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed; IN;IN_ELIM_THM] THEN DISCH_TAC);
 565
 566  (NEW_GOAL `?y. y IN V /\ dist (p,y:real^3) < &2`);
 567  (ASM_MESON_TAC[saturated]);
 568  (FIRST_X_ASSUM CHOOSE_TAC);
 569
 570  (MATCH_MP_TAC (REAL_ARITH `m <= dist (p, y:real^3) /\
 571                              dist (p, y:real^3) < &2 ==> m <= &4`));
 572  (ASM_REWRITE_TAC[]);
 573  (REWRITE_WITH `dist (u0,p) = dist (p,u0:real^3)`);
 574  (MESON_TAC[DIST_SYM]);
 575  (FIRST_ASSUM MATCH_MP_TAC);
 576  (ASM_MESON_TAC[IN]);
 577
 578  (SUBGOAL_THEN `p IN rogers V wl` ASSUME_TAC);
 579  (ASM_SET_TAC[]);
 580  (NEW_GOAL `?w0 w1 w2 w3. wl = [w0:real^3;w1;w2;w3]`);
 581  (MP_TAC (ASSUME `barV V 3 wl`));
 582  (REWRITE_TAC[BARV_3_EXPLICIT]);
 583  (FIRST_X_ASSUM CHOOSE_TAC);
 584  (FIRST_X_ASSUM CHOOSE_TAC);
 585  (FIRST_X_ASSUM CHOOSE_TAC);
 586  (FIRST_X_ASSUM CHOOSE_TAC);
 587  (ASM_REWRITE_TAC[HD]);
 588
 589  (NEW_GOAL `p IN voronoi_closed V (w0:real^3)`);
 590  (REWRITE_WITH `p IN voronoi_closed V w0 <=>
 591                    (?vl. vl IN barV V 3 /\
 592                     p IN rogers V vl /\
 593                     truncate_simplex 0 vl = [w0])`);
 594  (MATCH_MP_TAC Rogers.GLTVHUM);
 595  (ASM_REWRITE_TAC[]);
 596  (NEW_GOAL `set_of_list wl SUBSET (V:real^3->bool)`);
 597  (MATCH_MP_TAC Packing3.BARV_SUBSET);
 598  (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 599  (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
 600  (EXISTS_TAC `wl:(real^3)list`);
 601  (ASM_MESON_TAC[IN;TRUNCATE_SIMPLEX_EXPLICIT_0]);
 602  (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed; IN;IN_ELIM_THM] THEN DISCH_TAC);
 603
 604  (NEW_GOAL `?y. y IN V /\ dist (p,y:real^3) < &2`);
 605  (ASM_MESON_TAC[saturated]);
 606  (FIRST_X_ASSUM CHOOSE_TAC);
 607
 608  (MATCH_MP_TAC (REAL_ARITH `m <= dist (p, y:real^3) /\
 609                              dist (p, y:real^3) < &2 ==> m <= &4`));
 610  (ASM_REWRITE_TAC[]);
 611  (FIRST_ASSUM MATCH_MP_TAC);
 612  (ASM_MESON_TAC[IN]);
 613  (ASM_REAL_ARITH_TAC);
 614  (ASM_SIMP_TAC[]);
 615
 616
 617  (MATCH_MP_TAC FINITE_SUBSET);
 618  (EXISTS_TAC `{kl | ?u0 u1 u2 u3:real^3.
 619                 u0 IN H /\ u1 IN H /\ u2 IN H /\ u3 IN H /\
 620                 kl = [u0; u1; u2; u3]}`);
 621  (ASM_REWRITE_TAC[]);
 622  (MATCH_MP_TAC FINITE_SET_LIST_LEMMA);
 623  (EXPAND_TAC "H");
 624  (MATCH_MP_TAC FINITE_SUBSET);
 625  (EXISTS_TAC `V INTER ball ((HD wl):real^3, &15)`);
 626  (ASM_SIMP_TAC[KIUMVTC; REAL_ARITH `&0 <= &15`]);
 627  (EXPAND_TAC "H" THEN REWRITE_TAC[SUBSET; ball; IN_INTER; IN;IN_ELIM_THM]);
 628  (REPEAT STRIP_TAC);
 629  (ASM_REWRITE_TAC[]);
 630  (ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REAL_ARITH_TAC);
 631
 632 (* ======================================================================== *)
 633 (* Ok here *)
 634
 635  (ABBREV_TAC `f = (\kl:(real^3)list. rogers V kl INTER rogers V wl)`);
 636  (ABBREV_TAC `SPP = IMAGE (f:((real^3)list->real^3->bool))
 637   ((SP:(real^3)list->bool) DIFF {zl| rogers V zl = rogers V wl})`);
 638
 639  (NEW_GOAL `FINITE (SPP:(real^3->bool)->bool)`);
 640  (EXPAND_TAC "SPP" THEN MATCH_MP_TAC FINITE_IMAGE THEN ASM_REWRITE_TAC[]);
 641  (MATCH_MP_TAC FINITE_SUBSET);
 642  (EXISTS_TAC `SP:(real^3)list->bool`);
 643  (ASM_REWRITE_TAC[]);
 644  (SET_TAC[]);
 645
 646  (EXISTS_TAC `(S2:real^3->bool) DIFF (rogers V wl INTER UNIONS SPP)`);
 647  (REWRITE_TAC[SET_RULE `A DIFF B SUBSET A`]);
 648  (REPEAT STRIP_TAC);
 649  (MATCH_MP_TAC MEASURABLE_DIFF);
 650  (ASM_REWRITE_TAC[MEASURABLE_INTER]);
 651  (MATCH_MP_TAC MEASURABLE_INTER);
 652  (STRIP_TAC);
 653  (MATCH_MP_TAC MEASURABLE_ROGERS);
 654  (ASM_REWRITE_TAC[]);
 655  (MATCH_MP_TAC MEASURABLE_UNIONS);
 656  (ASM_REWRITE_TAC[]);
 657  (EXPAND_TAC "SPP");
 658  (EXPAND_TAC "f");
 659  (REWRITE_TAC[BETA_THM; IMAGE;IN;IN_ELIM_THM]);
 660  (REPEAT STRIP_TAC);
 661  (ASM_REWRITE_TAC[]);
 662  (MATCH_MP_TAC MEASURABLE_INTER);
 663  (ASM_SIMP_TAC [MEASURABLE_ROGERS]);
 664  (MATCH_MP_TAC MEASURABLE_ROGERS);
 665  (ASM_REWRITE_TAC[]);
 666  (UNDISCH_TAC `(SP DIFF {zl | rogers V zl = rogers V wl}) x`);
 667  (REWRITE_WITH `(SP DIFF {zl | rogers V zl = rogers V wl}) x <=>
 668   x IN (SP DIFF {zl | rogers V zl = rogers V wl})`);
 669  (MESON_TAC[IN]);
 670  (REWRITE_TAC[IN_DIFF]);
 671  (EXPAND_TAC "SP" THEN REWRITE_TAC[IN_ELIM_THM]);
 672  (MESON_TAC[IN]);
 673  (REWRITE_WITH `measure (S2 DIFF rogers V wl INTER UNIONS SPP) = measure S2`);
 674  (MATCH_MP_TAC MEASURE_NEGLIGIBLE_SYMDIFF);
 675  (REWRITE_TAC[SET_RULE `(A DIFF B) DIFF A UNION A DIFF (A DIFF B) = A INTER B`]);
 676  (MATCH_MP_TAC NEGLIGIBLE_SUBSET);
 677  (EXISTS_TAC `rogers V wl INTER UNIONS SPP`);
 678  (REWRITE_TAC[SET_RULE `A INTER B SUBSET B`]);
 679  (REWRITE_TAC[INTER_UNIONS]);
 680  (MATCH_MP_TAC NEGLIGIBLE_UNIONS);
 681  (STRIP_TAC);
 682  (REWRITE_WITH `{rogers V wl INTER x | x IN SPP} = IMAGE (\x. rogers V wl INTER x) SPP`);
 683  (REWRITE_TAC[IMAGE; SET_EQ_LEMMA; IN;IN_ELIM_THM]);
 684  (MATCH_MP_TAC FINITE_IMAGE);
 685  (ASM_REWRITE_TAC[]);
 686  (EXPAND_TAC "SPP" THEN EXPAND_TAC "SP" THEN EXPAND_TAC "f");
 687  (REWRITE_TAC[IMAGE;IN;IN_ELIM_THM]);
 688  (REPEAT STRIP_TAC);
 689  (ASM_REWRITE_TAC[SET_RULE `a INTER b INTER a = a INTER b`]);
 690  (MATCH_MP_TAC COPLANAR_IMP_NEGLIGIBLE);
 691  (MATCH_MP_TAC DUUNHOR);
 692  (UNDISCH_TAC `({kl | barV V 3 kl /\ ~(rogers V kl INTER S2 = {})} DIFF
 693                  {zl | rogers V zl = rogers V wl}) x'`);
 694  (REWRITE_WITH
 695   `({kl | barV V 3 kl /\ ~(rogers V kl INTER S2 = {})} DIFF
 696     {zl | rogers V zl = rogers V wl}) x' <=>
 697     x' IN ({kl | barV V 3 kl /\ ~(rogers V kl INTER S2 = {})} DIFF
 698            {zl | rogers V zl = rogers V wl})`);
 699  (MESON_TAC[IN]);
 700  (REWRITE_TAC[IN_DIFF]);
 701  (REWRITE_TAC[IN; IN_ELIM_THM]);
 702  (DISCH_TAC THEN ASM_REWRITE_TAC[]);
 703  (ASM_REWRITE_TAC[]);
 704
 705  (EXPAND_TAC "SPP" THEN EXPAND_TAC "SP" THEN EXPAND_TAC "f");
 706  (REWRITE_TAC[IMAGE;IN;IN_ELIM_THM]);
 707  (REWRITE_TAC[MESON[IN; IN_DIFF] `(S DIFF P) x <=> x IN S /\ ~(x IN P)`]);
 708  (REWRITE_TAC[IN;IN_ELIM_THM]);
 709  (MATCH_MP_TAC (SET_RULE `(!p. p IN S ==> ~(p IN P)) ==> (S INTER P = {})`));
 710  (REWRITE_TAC[IN_DIFF; IN_INTER;IN_UNIONS; MESON[] `~(A /\ B) <=> ~A \/ ~ B`]);
 711
 712  (REPEAT STRIP_TAC);
 713  (NEW_GOAL `p IN rogers V wl`);
 714  (ASM_SET_TAC[]);
 715  (ASM_MESON_TAC[]);
 716  (NEW_GOAL `?t. t IN
 717             {y | ?x. ((barV V 3 x /\ ~(rogers V x INTER S2 = {})) /\
 718                       ~(rogers V x = rogers V wl)) /\
 719                      y = rogers V x INTER rogers V wl} /\
 720             p IN t`);
 721  (EXISTS_TAC `rogers V kl INTER rogers V wl`);
 722  (ASM_REWRITE_TAC[IN_INTER]);
 723  (STRIP_TAC);
 724  (REWRITE_TAC[IN;IN_ELIM_THM]);
 725  (EXISTS_TAC `kl:(real^3)list`);
 726  (ASM_REWRITE_TAC[]);
 727  (REWRITE_TAC[SET_RULE `~(A INTER B = {}) <=> (?z. z IN A /\ z IN B)`]);
 728  (EXISTS_TAC `p:real^3`);
 729  (ASM_REWRITE_TAC[]);
 730  (ASM_SET_TAC[]);
 731  (ASM_MESON_TAC[]);
 732  (UP_ASM_TAC THEN STRIP_TAC);
 733
 734 (* ========================================================================= *)
 735 (* OK here *)
 736
 737  (NEW_GOAL `?k:num S4. k <= 4 /\
 738    S4 SUBSET S3 /\ measurable S4 /\ &0 < measure S4 /\
 739    S4 SUBSET (mcell k V wl)`);
 740
 741  (ABBREV_TAC
 742   `SP = {k:num| ~(mcell k V wl INTER S3 = {}) /\ k <= 4}`);
 743  (NEW_GOAL `FINITE (SP:(num ->bool))`);
 744  (MATCH_MP_TAC FINITE_SUBSET);
 745  (EXISTS_TAC `{k | k <= 4}`);
 746  (EXPAND_TAC "SP");
 747  (SET_TAC[FINITE_NUMSEG_LE]);
 748
 749  (ABBREV_TAC `f = (\k:num. mcell k V wl INTER S3)`);
 750  (ABBREV_TAC `SPP = IMAGE (f:(num->real^3->bool))
 751   (SP:num->bool)`);
 752  (NEW_GOAL `FINITE (SPP:(real^3->bool)->bool)`);
 753  (EXPAND_TAC "SPP" THEN MATCH_MP_TAC FINITE_IMAGE THEN ASM_REWRITE_TAC[]);
 754
 755  (NEW_GOAL `(S3:real^3->bool) = (UNIONS SPP)`);
 756  (EXPAND_TAC "SPP" THEN REWRITE_TAC[SET_EQ_LEMMA; UNIONS_IMAGE;IN;IN_ELIM_THM]
 757    THEN REPEAT STRIP_TAC);
 758  (EXPAND_TAC "f");
 759
 760  (NEW_GOAL `?j. j <= 4 /\ x IN mcell j V wl`);
 761  (MATCH_MP_TAC SLTSTLO1);
 762  (ASM_REWRITE_TAC[]);
 763  (MATCH_MP_TAC (SET_RULE `(x:real^3) IN S3 /\ S3 SUBSET B ==> x IN B`));
 764  (STRIP_TAC);
 765  (UP_ASM_TAC THEN SIMP_TAC[IN]);
 766  (ASM_SET_TAC[]);
 767  (UP_ASM_TAC THEN STRIP_TAC);
 768  (EXISTS_TAC `j':num`);
 769  (STRIP_TAC);
 770  (EXPAND_TAC "SP");
 771  (REWRITE_TAC[IN_ELIM_THM]);
 772  (ASM_REWRITE_TAC[INTER]);
 773  (ASM_SET_TAC[]);
 774  (ONCE_REWRITE_TAC[GSYM IN]);
 775  (ASM_SET_TAC[]);
 776  (UP_ASM_TAC THEN EXPAND_TAC "f");
 777  (ONCE_REWRITE_TAC
 778   [MESON[IN] `(mcell x' V wl INTER S3) x <=> x IN (mcell x' V wl INTER S3)`]);
 779  (REWRITE_TAC[IN_INTER; IN]);
 780  (MESON_TAC[]);
 781
 782  (NEW_GOAL `!s1. s1 IN SPP ==> measurable (s1:(real^3->bool))`);
 783  (EXPAND_TAC "SPP" THEN EXPAND_TAC "f" THEN REWRITE_TAC[IMAGE;IN;
 784    IN_ELIM_THM]);
 785  (REPEAT STRIP_TAC);
 786  (ONCE_ASM_REWRITE_TAC[]);
 787  (MATCH_MP_TAC MEASURABLE_INTER);
 788  (STRIP_TAC);
 789  (MATCH_MP_TAC MEASURABLE_MCELL);
 790  (ASM_REWRITE_TAC[]);
 791  (ASM_REWRITE_TAC[]);
 792
 793  (NEW_GOAL `?k. k <= 4 /\ ~negligible (mcell k V wl INTER S3)`);
 794  (REWRITE_WITH `(?k. k <= 4 /\ ~negligible (mcell k V wl INTER S3)) <=>
 795                 ~(!k. (k <= 4) ==> negligible (mcell k V wl INTER S3))`);
 796  (MESON_TAC[]);
 797  (STRIP_TAC);
 798  (NEW_GOAL `negligible (UNIONS (SPP:(real^3->bool)->bool))`);
 799  (MATCH_MP_TAC NEGLIGIBLE_UNIONS);
 800  (ASM_REWRITE_TAC[]);
 801  (EXPAND_TAC "SPP" THEN EXPAND_TAC "f");
 802  (REWRITE_TAC[IMAGE]);
 803  (REWRITE_TAC[IN; IN_ELIM_THM]);
 804  (REPEAT STRIP_TAC);
 805  (ONCE_ASM_REWRITE_TAC[]);
 806  (FIRST_ASSUM MATCH_MP_TAC);
 807  (UNDISCH_TAC `(SP:num->bool) x`);
 808  (EXPAND_TAC "SP" THEN REWRITE_TAC[IN_ELIM_THM]);
 809  (MESON_TAC[]);
 810
 811  (UP_ASM_TAC THEN REWRITE_TAC[GSYM
 812   (ASSUME `S3 = UNIONS (SPP:(real^3->bool)->bool)`)]);
 813  (REWRITE_WITH `~NULLSET S3 <=> &0 < measure (S3:real^3->bool)`);
 814  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 815  (MATCH_MP_TAC MEASURABLE_MEASURE_POS_LT);
 816  (ASM_REWRITE_TAC[]);
 817  (ASM_REWRITE_TAC[]);
 818  (UP_ASM_TAC THEN STRIP_TAC THEN EXISTS_TAC `k:num`
 819    THEN EXISTS_TAC `mcell k V wl INTER S3`);
 820  (REPEAT STRIP_TAC);
 821
 822  (ASM_REWRITE_TAC[]);
 823  (SET_TAC[]);
 824  (MATCH_MP_TAC MEASURABLE_INTER);
 825  (ASM_REWRITE_TAC[]);
 826  (MATCH_MP_TAC MEASURABLE_MCELL);
 827  (ASM_REWRITE_TAC[]);
 828  (REWRITE_WITH `&0 < measure (mcell k V wl INTER S3) <=>
 829                 ~negligible (mcell k V wl INTER S3)`);
 830  (MATCH_MP_TAC MEASURABLE_MEASURE_POS_LT);
 831  (MATCH_MP_TAC MEASURABLE_INTER);
 832  (ASM_REWRITE_TAC[]);
 833  (MATCH_MP_TAC MEASURABLE_MCELL);
 834  (ASM_REWRITE_TAC[]);
 835  (ASM_REWRITE_TAC[]);
 836  (SET_TAC[]);
 837  (UP_ASM_TAC THEN STRIP_TAC);
 838
 839 (* -------------------------------------------------------------------------- *)
 840 (* OK here *)
 841
 842  (NEW_GOAL `?S5. S5 SUBSET S4 /\ measurable S5 /\ &0 < measure S5 /\
 843                  (!h. ~(h = k) /\ h <= 4 ==> (S5 INTER mcell h V wl = {}))`);
 844  (NEW_GOAL `?Z. !p. saturated V /\ packing V /\ barV V 3 wl
 845                  ==> NULLSET Z /\
 846                      (p IN rogers V wl DIFF Z
 847                       ==> (?!i. i <= 4 /\ p IN mcell i V wl))`);
 848  (ASM_REWRITE_TAC[SLTSTLO2]);
 849  (UP_ASM_TAC THEN STRIP_TAC);
 850  (NEW_GOAL `NULLSET Z /\ !p. (p IN rogers V wl DIFF Z
 851                ==> (?!i. i <= 4 /\ p IN mcell i V wl))`);
 852  (NEW_GOAL `!p. NULLSET Z /\ (p IN rogers V wl DIFF Z
 853                ==> (?!i. i <= 4 /\ p IN mcell i V wl))`);
 854  (GEN_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
 855  (ASM_REWRITE_TAC[]);
 856  (UP_ASM_TAC THEN MESON_TAC[]);
 857  (UP_ASM_TAC THEN REWRITE_TAC[EXISTS_UNIQUE] THEN STRIP_TAC);
 858
 859  (EXISTS_TAC `S4 DIFF (Z:real^3->bool)`);
 860  (REPEAT STRIP_TAC);
 861  (SET_TAC[]);
 862  (MATCH_MP_TAC MEASURABLE_DIFF);
 863  (ASM_REWRITE_TAC[]);
 864  (ASM_MESON_TAC[MEASURABLE_RULES]);
 865  (REWRITE_WITH `measure (S4 DIFF Z) = measure (S4:real^3->bool)`);
 866  (MATCH_MP_TAC MEASURE_NEGLIGIBLE_SYMDIFF);
 867  (MATCH_MP_TAC NEGLIGIBLE_SUBSET);
 868  (EXISTS_TAC `Z:real^3->bool`);
 869  (ASM_REWRITE_TAC[]);
 870  (SET_TAC[]);
 871  (ASM_REWRITE_TAC[]);
 872  (REWRITE_TAC[SET_RULE `A = {} <=> (!x. x IN A ==> F)`]);
 873  (GEN_TAC THEN STRIP_TAC);
 874  (NEW_GOAL `x IN mcell k V wl`);
 875  (MATCH_MP_TAC (SET_RULE `x IN (S4 DIFF Z) INTER mcell h V wl /\
 876   (S4 DIFF Z) INTER mcell h V wl SUBSET A ==> x IN A`));
 877  (ASM_REWRITE_TAC[]);
 878  (ASM_SET_TAC[]);
 879
 880  (NEW_GOAL `x IN rogers V wl DIFF Z`);
 881  (ASM_SET_TAC[]);
 882  (NEW_GOAL `(?i. (i <= 4 /\ x IN mcell i V wl) /\
 883                    (!y. y <= 4 /\ x IN mcell y V wl ==> y = i))`);
 884  (FIRST_ASSUM MATCH_MP_TAC);
 885  (ASM_REWRITE_TAC[]);
 886  (UP_ASM_TAC THEN STRIP_TAC);
 887
 888  (NEW_GOAL `k = i':num`);
 889  (FIRST_ASSUM MATCH_MP_TAC);
 890  (ASM_REWRITE_TAC[]);
 891  (NEW_GOAL `h = i':num`);
 892  (FIRST_ASSUM MATCH_MP_TAC);
 893  (ASM_REWRITE_TAC[]);
 894  (ASM_SET_TAC[]);
 895  (ASM_MESON_TAC[]);
 896  (UP_ASM_TAC THEN STRIP_TAC);
 897
 898 (* -------------------------------------------------------------------------- *)
 899 (* OK here *)
 900  (NEW_GOAL `mcell i V ul SUBSET
 901              UNIONS {rogers V (left_action_list p ul) | p permutes 0..i - 1}`);
 902  (MATCH_MP_TAC QZKSYKG2);
 903  (ASM_REWRITE_TAC[]);
 904
 905  (NEW_GOAL `~(S5 = {}:real^3->bool)`);
 906  (STRIP_TAC);
 907  (NEW_GOAL `negligible (S5:real^3->bool)`);
 908  (ASM_REWRITE_TAC[NEGLIGIBLE_EMPTY]);
 909  (NEW_GOAL `vol (S5) = &0`);
 910  (ASM_SIMP_TAC[volume_props]);
 911  (ASM_REAL_ARITH_TAC);
 912  (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE `~(S = {}) <=> (?x. x IN S)`]);
 913  (STRIP_TAC);
 914
 915  (NEW_GOAL `S5 SUBSET mcell i V ul /\ S5 SUBSET mcell j V vl`);
 916  (ASM_SET_TAC[]);
 917  (NEW_GOAL `S5 SUBSET
 918              UNIONS {rogers V (left_action_list p ul) | p permutes 0..i - 1}`);
 919  (UP_ASM_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 920  (NEW_GOAL `x IN UNIONS {rogers V (left_action_list p ul) | p permutes 0..i - 1}`);
 921  (UP_ASM_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 922  (UP_ASM_TAC THEN REWRITE_TAC[IN_UNIONS; IN; IN_ELIM_THM] THEN STRIP_TAC);
 923  (ABBREV_TAC `kl:(real^3)list = left_action_list p ul`);
 924  (NEW_GOAL `barV V 3 kl`);
 925  (MATCH_MP_TAC QZKSYKG1);
 926  (EXISTS_TAC `ul:(real^3)list`);
 927  (EXISTS_TAC `i:num` THEN EXISTS_TAC `p:num->num`);
 928  (ASM_REWRITE_TAC[]);
 929  (NEW_GOAL `x IN mcell i V ul`);
 930  (ASM_SET_TAC[]);
 931  (UP_ASM_TAC THEN SET_TAC[]);
 932
 933  (NEW_GOAL `rogers V kl = rogers V wl`);
 934  (ASM_CASES_TAC `rogers V kl = rogers V wl`);
 935  (ASM_REWRITE_TAC[]);
 936  (NEW_GOAL `F`);
 937  (NEW_GOAL `S3 INTER rogers V kl = {}`);
 938  (ASM_SIMP_TAC[]);
 939  (UP_ASM_TAC THEN ASM_SET_TAC[]);
 940  (ASM_MESON_TAC[]);
 941
 942  (NEW_GOAL `mcell i V kl = mcell i V ul`);
 943  (EXPAND_TAC "kl");
 944  (MATCH_MP_TAC RVFXZBU);
 945  (ASM_REWRITE_TAC[]);
 946
 947  (NEW_GOAL `mcell i V kl = mcell i V wl`);
 948  (MATCH_MP_TAC DDZUPHJ);
 949  (ASM_REWRITE_TAC[]);
 950  (STRIP_TAC);
 951  (MATCH_MP_TAC VOL_POS_LT_AFF_DIM_3);
 952  (ASM_SIMP_TAC[MEASURABLE_ROGERS]);
 953  (NEW_GOAL `vol S5 <= vol (rogers V wl)`);
 954  (MATCH_MP_TAC MEASURE_SUBSET);
 955  (ASM_SIMP_TAC[MEASURABLE_ROGERS]);
 956  (ASM_SET_TAC[]);
 957  (ASM_REAL_ARITH_TAC);
 958  (ASM_SET_TAC[]);
 959
 960  (NEW_GOAL `mcell j V vl SUBSET
 961              UNIONS {rogers V (left_action_list q vl) | q permutes 0..j - 1}`);
 962  (MATCH_MP_TAC QZKSYKG2);
 963  (ASM_REWRITE_TAC[]);
 964
 965  (NEW_GOAL `~(S5 = {}:real^3->bool)`);
 966  (STRIP_TAC);
 967  (NEW_GOAL `negligible (S5:real^3->bool)`);
 968  (ASM_REWRITE_TAC[NEGLIGIBLE_EMPTY]);
 969  (NEW_GOAL `vol (S5) = &0`);
 970  (ASM_SIMP_TAC[volume_props]);
 971  (ASM_REAL_ARITH_TAC);
 972  (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE `~(S = {}) <=> (?x. x IN S)`]);
 973  (STRIP_TAC);
 974
 975  (NEW_GOAL `S5 SUBSET
 976              UNIONS {rogers V (left_action_list q vl) | q permutes 0..j - 1}`);
 977  (SET_TAC[ASSUME `S5 SUBSET mcell i V ul /\ S5 SUBSET mcell j V vl`; ASSUME
 978    `mcell j V vl SUBSET
 979       UNIONS {rogers V (left_action_list q vl) | q permutes 0..j - 1}`]);
 980  (NEW_GOAL `x' IN UNIONS {rogers V (left_action_list q vl) | q permutes 0..j - 1}`);
 981  (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 982
 983  (UP_ASM_TAC THEN REWRITE_TAC[IN_UNIONS; IN; IN_ELIM_THM] THEN STRIP_TAC);
 984  (ABBREV_TAC `sl:(real^3)list = left_action_list q vl`);
 985  (NEW_GOAL `barV V 3 sl`);
 986  (MATCH_MP_TAC QZKSYKG1);
 987  (EXISTS_TAC `vl:(real^3)list`);
 988  (EXISTS_TAC `j:num` THEN EXISTS_TAC `q:num->num`);
 989  (ASM_REWRITE_TAC[]);
 990  (ASM_SET_TAC[]);
 991
 992  (NEW_GOAL `rogers V sl = rogers V wl`);
 993  (ASM_CASES_TAC `rogers V sl = rogers V wl`);
 994  (ASM_REWRITE_TAC[]);
 995  (NEW_GOAL `F`);
 996  (NEW_GOAL `S3 INTER rogers V sl = {}`);
 997  (ASM_SIMP_TAC[]);
 998  (ASM_SET_TAC[]);
 999  (ASM_MESON_TAC[]);
1000
1001  (NEW_GOAL `mcell j V sl = mcell j V vl`);
1002  (EXPAND_TAC "sl");
1003  (MATCH_MP_TAC RVFXZBU);
1004  (ASM_REWRITE_TAC[]);
1005
1006  (NEW_GOAL `mcell j V sl = mcell j V wl`);
1007  (MATCH_MP_TAC DDZUPHJ);
1008  (ASM_REWRITE_TAC[]);
1009  (STRIP_TAC);
1010
1011  (MATCH_MP_TAC VOL_POS_LT_AFF_DIM_3);
1012  (ASM_SIMP_TAC[MEASURABLE_ROGERS]);
1013  (NEW_GOAL `vol S5 <= vol (rogers V wl)`);
1014  (MATCH_MP_TAC MEASURE_SUBSET);
1015  (ASM_SIMP_TAC[MEASURABLE_ROGERS]);
1016  (ASM_SET_TAC[]);
1017  (ASM_REAL_ARITH_TAC);
1018  (ASM_SET_TAC[]);
1019
1020  (NEW_GOAL `S5 SUBSET (mcell i V ul INTER mcell j V vl)`);
1021  (ASM_REWRITE_TAC[]);
1022  (ASM_SET_TAC[]);
1023  (UP_ASM_TAC THEN REWRITE_WITH
1024    `mcell i V ul = mcell i V wl /\ mcell j V vl = mcell j V wl`);
1025  (ASM_MESON_TAC[]);
1026  (STRIP_TAC);
1027
1028  (NEW_GOAL `i = k:num`);
1029  (ASM_CASES_TAC `i = k:num`);
1030  (ASM_REWRITE_TAC[]);
1031  (NEW_GOAL `S5 INTER mcell i V wl = {}`);
1032  (FIRST_ASSUM MATCH_MP_TAC);
1033  (ASM_REWRITE_TAC[UP_TO_4_KY_LEMMA]);
1034  (NEW_GOAL `F`);
1035  (UP_ASM_TAC THEN ASM_SET_TAC[]);
1036  (ASM_MESON_TAC[]);
1037
1038  (NEW_GOAL `j = k:num`);
1039  (ASM_CASES_TAC `j = k:num`);
1040  (ASM_REWRITE_TAC[]);
1041  (NEW_GOAL `S5 INTER mcell j V wl = {}`);
1042  (FIRST_ASSUM MATCH_MP_TAC);
1043  (ASM_REWRITE_TAC[UP_TO_4_KY_LEMMA]);
1044  (NEW_GOAL `F`);
1045  (UP_ASM_TAC THEN ASM_SET_TAC[]);
1046  (ASM_MESON_TAC[]);
1047
1048  (ASM_REWRITE_TAC[])]);;
1049
1050
1051 end;;