text_formalization/packing/QZYZMJC.hl

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