(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*                                                                           *)
(*      Authour   : VU KHAC KY                                               *)
(*      Book lemma: QZYZMJC                                                  *)
(*      Chaper    : Packing (Marchal cells)                                  *)
(*                                                                           *)
(* ========================================================================= *)


(* ========================================================================= *)
(* The lemma statement has been corrected                                    *)

module Qzyzmjc = struct


open Rogers;;
open Vukhacky_tactics;;
open Pack_defs;;
open Pack_concl;; 
open Pack1;;
open Sphere;; 
open Marchal_cells;;
open Emnwuus;;
open Marchal_cells_2_new;;
open Lepjbdj;;
open Hdtfnfz;;
open Urrphbz1;;
open Sltstlo;;
open Qzksykg;;
open Rvfxzbu;;
open Ddzuphj;;
open Urrphbz2;;
open Ajripqn;;

let QZYZMJC1_concl = 
`!V v X.
     saturated V /\ packing V /\ v IN V
     ==> sum {X | mcell_set V X /\ v IN VX V X} (\t. sol v t) = &4 * pi`;;

(* ========================================================================= *)
(* Lemma 1 *)
let mcell_set_2 = 
prove_by_refinement (
 `!V:real^3->bool.  mcell_set V = 
   {X | ?i ul. X = mcell i V ul /\ ul IN barV V 3 /\ i <= 4}`,


[(REWRITE_TAC[mcell_set] THEN GEN_TAC);
 (MATCH_MP_TAC (SET_RULE `A SUBSET B /\ B SUBSET A ==> B = A`));
 (STRIP_TAC);
 (SET_TAC[]);
 (REWRITE_TAC[SUBSET;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (ASM_CASES_TAC `i <= 4`);
 (EXISTS_TAC `i:num` THEN EXISTS_TAC `ul:(real^3)list`);
 (ASM_REWRITE_TAC[]);
 (EXISTS_TAC `4:num` THEN EXISTS_TAC `ul:(real^3)list`);
 (ASM_REWRITE_TAC[ARITH_RULE `4 <= 4`]);
 (ASM_SIMP_TAC [MCELL_EXPLICIT; ARITH_RULE `~(i <= 4) ==> (i >= 4)`; 
 ARITH_RULE `4 >= 4`])]);;
(* ========================================================================= *)
(* Lemma 2 *)
let BARV_3_IMP_FINITE_lemma1 = 
prove_by_refinement(
 `!V ul u v.
     packing V /\ saturated V /\ barV V 3 ul /\ {u, v} SUBSET set_of_list ul
     ==> dist (u,v) < &4`,

[(REPEAT STRIP_TAC);

 (NEW_GOAL `?a. voronoi_list V ul = {a} /\
                    a = circumcenter (set_of_list ul) /\
                    hl ul = dist (HD ul,a)`);
 (MATCH_MP_TAC VORONOI_LIST_3_SINGLETON_EXPLICIT);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (NEW_GOAL `!s. s IN set_of_list ul ==> dist (a, s:real^3) < &2`);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `?y. y IN V /\ dist (a,y:real^3) < &2`);
 (ASM_MESON_TAC[saturated]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (SUBGOAL_THEN `a IN voronoi_list V ul` MP_TAC);
 (ASM_SET_TAC[]);
 (REWRITE_TAC[VORONOI_LIST; VORONOI_SET; voronoi_closed; IN_INTERS]);
 (STRIP_TAC);
 (NEW_GOAL `a IN {x | !w. V w ==> dist (x,s:real^3) <= dist (x,w)}`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[IN; IN_ELIM_THM] THEN STRIP_TAC);
 (NEW_GOAL `dist (a,s) <= dist (a, y:real^3)`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_SET_TAC[]);
 (ASM_REAL_ARITH_TAC);
 (NEW_GOAL `dist (u, v:real^3) <= dist (u,a) + dist (a,v)`);
 (REWRITE_TAC[DIST_TRIANGLE]);
 (NEW_GOAL `dist (u,a:real^3) < &2`);
 (ONCE_REWRITE_TAC[DIST_SYM]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_SET_TAC[]);
 (NEW_GOAL `dist (a,v:real^3) < &2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_SET_TAC[]);
 (ASM_REAL_ARITH_TAC)]);;
(* ========================================================================= *)
(* Lemma 3 *)
let BARV_3_IMP_FINITE_lemma2 = 
prove_by_refinement (
 `!V ul v k. packing V /\ saturated V /\ barV V 3 ul /\ v IN set_of_list ul 
    ==> set_of_list ul SUBSET ball (v, &4)`,

[(REWRITE_TAC[SUBSET; ball; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (MATCH_MP_TAC BARV_3_IMP_FINITE_lemma1);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `ul:(real^3)list`);
 (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[])]);;
(* ========================================================================= *)
(* Lemma 4 *)

let lemma_r_r'_fix2 = 
prove_by_refinement (
 `!C x r s.
         measurable C /\ radial_norm r x C /\ s > &0 /\ s <= r
         ==> measurable (C INTER normball x s) /\
             vol (C INTER normball x s) = vol C * (s / r) pow 3 `,

[(REPEAT GEN_TAC);
 (ASM_CASES_TAC `s < r`);
 (ASM_MESON_TAC[Vol1.lemma_r_r'_fix]);
 (STRIP_TAC);
 (NEW_GOAL `s = r:real`);
 (ASM_REAL_ARITH_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `C INTER normball x r = C:real^3->bool`);
 (MATCH_MP_TAC (SET_RULE `A SUBSET B ==> A INTER B = A`));
 (UNDISCH_TAC `radial_norm r (x:real^3) C`);
 (REWRITE_TAC[GSYM RADIAL_VS_RADIAL_NORM; radial; NORMBALL_BALL] THEN SET_TAC[]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `r / r = &1`);
 (MATCH_MP_TAC REAL_DIV_REFL THEN ASM_REAL_ARITH_TAC);
 (REAL_ARITH_TAC)]);;
(* ========================================================================= *)
(* Lemma 5 *)
let MCELL_SET_NOT_EMPTY = 
prove_by_refinement (
 `!V v X.
     saturated V /\ packing V /\ v IN V
     ==> ~({X | mcell_set V X /\ ~NULLSET X /\ v IN V INTER X} = {})`,


[(REWRITE_TAC[mcell_set; SET_RULE `~(s = {}) <=> (?x. x IN s)`; IN;
   IN_ELIM_THM]);
 (REPEAT STRIP_TAC);

 (ASM_CASES_TAC `!i ul. 1 <= i /\ i <= 4 /\ barV V 3 ul /\ 
                         truncate_simplex 0 ul = [v] ==> 
                         negligible (mcell i V ul)`);
 (NEW_GOAL `!vl. barV V 3 vl /\ 
                  truncate_simplex 0 vl = [v] ==> 
                  negligible (rogers V vl INTER ball (v, sqrt (&2)))`);
 (REPEAT STRIP_TAC);

 (NEW_GOAL `vol (rogers V vl) <= 
             vol (UNIONS {x | ?i. i <= 4 /\ x = mcell i V vl})`);
 (MATCH_MP_TAC MEASURE_SUBSET);
 (STRIP_TAC);
 (MATCH_MP_TAC MEASURABLE_ROGERS);
 (ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (MATCH_MP_TAC MEASURABLE_UNIONS);
 (STRIP_TAC);
 (REWRITE_TAC[GSYM IN_NUMSEG_0]);
 (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
 (REWRITE_TAC[FINITE_NUMSEG]);
 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MEASURABLE_MCELL);
 (ASM_REWRITE_TAC[]);

 (REWRITE_TAC[SUBSET]);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[IN_UNIONS; IN;IN_ELIM_THM]);

 (NEW_GOAL `?i. i <= 4 /\ x IN mcell i V vl`);
 (MATCH_MP_TAC SLTSTLO1);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `mcell i V vl`);
 (STRIP_TAC);
 (EXISTS_TAC `i:num`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[IN]);


 (UP_ASM_TAC THEN REWRITE_WITH 
 `UNIONS {x | ?i. i <= 4 /\ x = mcell i V vl} = 
  UNIONS {x | ?i. 1 <= i /\ i <= 4 /\ x = mcell i V vl} UNION (mcell 0 V vl)`);
 (ONCE_REWRITE_TAC[SET_EQ_LEMMA] THEN REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; IN_UNIONS; IN_UNION]);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `i = 0`);
 (DISJ2_TAC);
 (ASM_SET_TAC[]);
 (DISJ1_TAC);
 (EXISTS_TAC `t:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (EXISTS_TAC `i:num` THEN ASM_REWRITE_TAC[]);
 (ASM_ARITH_TAC);
 (EXISTS_TAC `t:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (EXISTS_TAC `i:num` THEN ASM_REWRITE_TAC[]);
 (EXISTS_TAC `mcell 0 V vl`);
 (ASM_REWRITE_TAC[]);
 (EXISTS_TAC `0` THEN ASM_REWRITE_TAC[]);
 (ARITH_TAC);

 (ABBREV_TAC `S1 = UNIONS {x | ?i. 1 <= i /\ i <= 4 /\ x = mcell i V vl}`);
 (REWRITE_WITH `vol (S1 UNION mcell 0 V vl) = 
               vol (S1) + vol (mcell 0 V vl) - vol (S1 INTER mcell 0 V vl)`);
 (MATCH_MP_TAC MEASURE_UNION);
 (STRIP_TAC);
 (EXPAND_TAC "S1" THEN MATCH_MP_TAC MEASURABLE_UNIONS);
 (STRIP_TAC);
 (REWRITE_TAC[SET_RULE `A /\ B /\ C <=> (A /\ B) /\ C`]);
 (REWRITE_TAC[GSYM IN_NUMSEG]);
 (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
 (REWRITE_TAC[FINITE_NUMSEG]);
 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MEASURABLE_MCELL);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC MEASURABLE_MCELL);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `vol S1 = &0`);

 (MATCH_MP_TAC MEASURE_EQ_0);
 (EXPAND_TAC "S1" THEN MATCH_MP_TAC NEGLIGIBLE_UNIONS);
 (STRIP_TAC);
 (REWRITE_TAC[SET_RULE `A /\ B /\ C <=> (A /\ B) /\ C`]);
 (REWRITE_TAC[GSYM IN_NUMSEG]);
 (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
 (REWRITE_TAC[FINITE_NUMSEG]);
 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `vol (S1 INTER mcell 0 V vl) = &0`);
 (MATCH_MP_TAC MEASURE_EQ_0);
 (MATCH_MP_TAC NEGLIGIBLE_INTER);
 (DISJ1_TAC);
 (REWRITE_WITH `NULLSET S1 <=> vol S1 = &0`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC MEASURABLE_MEASURE_EQ_0);

 (EXPAND_TAC "S1" THEN MATCH_MP_TAC MEASURABLE_UNIONS);
 (STRIP_TAC);
 (REWRITE_TAC[SET_RULE `A /\ B /\ C <=> (A /\ B) /\ C`]);
 (REWRITE_TAC[GSYM IN_NUMSEG]);
 (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
 (REWRITE_TAC[FINITE_NUMSEG]);
 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MEASURABLE_MCELL);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);

 (ASM_REWRITE_TAC[REAL_ARITH `&0 + a - &0 = a`]);

 (ABBREV_TAC `S2 = rogers V vl INTER ball (v,sqrt (&2))`);
 (ABBREV_TAC `S3 = rogers V vl DIFF ball (v,sqrt (&2))`);
 (REWRITE_WITH `mcell 0 V vl = S3`);
 (REWRITE_TAC[mcell0; MCELL_EXPLICIT]);
 (EXPAND_TAC "S3");
 (REWRITE_WITH `HD vl = v:real^3`);
 (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 0 vl)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (NEW_GOAL `?u0 u1 u2 u3. vl = [u0;u1;u2;u3:real^3]`);
 (MATCH_MP_TAC BARV_3_EXPLICIT);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (ASM_REWRITE_TAC[HD]);
 (REWRITE_WITH `rogers V vl = S2 UNION S3`);
 (ASM_SET_TAC[]);
 (REWRITE_WITH `vol (S2 UNION S3) = vol (S2) + vol (S3) - vol (S2 INTER S3)`);
 (MATCH_MP_TAC MEASURE_UNION);
 (EXPAND_TAC "S2" THEN EXPAND_TAC "S3");
 (STRIP_TAC);
 (MATCH_MP_TAC MEASURABLE_INTER);
 (REWRITE_TAC[MEASURABLE_BALL]);
 (MATCH_MP_TAC MEASURABLE_ROGERS);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC MEASURABLE_DIFF);
 (REWRITE_TAC[MEASURABLE_BALL]);
 (MATCH_MP_TAC MEASURABLE_ROGERS);
 (ASM_REWRITE_TAC[]);

 (REWRITE_WITH `S2 INTER S3 = {}:real^3->bool`);
 (ASM_SET_TAC[]);
 (REWRITE_TAC[MEASURE_EMPTY; REAL_ARITH `a + b - &0 <= b <=> a <= &0`]);
 (NEW_GOAL `&0 <= vol S2`);
 (MATCH_MP_TAC MEASURE_POS_LE);

 (EXPAND_TAC "S2" THEN MATCH_MP_TAC MEASURABLE_INTER);
 (REWRITE_TAC[MEASURABLE_BALL]);
 (MATCH_MP_TAC MEASURABLE_ROGERS THEN ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (REWRITE_WITH `NULLSET S2 <=> vol S2 = &0`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN MATCH_MP_TAC MEASURABLE_MEASURE_EQ_0);
 (EXPAND_TAC "S2" THEN MATCH_MP_TAC MEASURABLE_INTER);
 (REWRITE_TAC[MEASURABLE_BALL]);
 (MATCH_MP_TAC MEASURABLE_ROGERS THEN ASM_REWRITE_TAC[]);
 (ASM_REAL_ARITH_TAC);

 (NEW_GOAL `voronoi_closed V v = 
   UNIONS {y| ?vl. vl IN barV V 3 /\
                    y = rogers V vl /\
                    truncate_simplex 0 vl = [v:real^3]}`);
 (ONCE_REWRITE_TAC[SET_RULE `s = t <=> (!x. x IN s <=> x IN t)`]);

 (REWRITE_WITH `!x. x IN voronoi_closed V v <=>
                  (?vl. vl IN barV V 3 /\
                         x IN rogers V vl /\
                         truncate_simplex 0 vl = [v])`);
 (GEN_TAC THEN MATCH_MP_TAC GLTVHUM);
 (ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (REWRITE_TAC[IN_UNIONS; IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EQ_TAC);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `rogers V vl` THEN ASM_REWRITE_TAC[]);
 (EXISTS_TAC `vl:(real^3)list` THEN ASM_REWRITE_TAC[]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `vl:(real^3)list` THEN ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);

 (NEW_GOAL `voronoi_closed V v INTER ball (v,sqrt (&2)) = 
    UNIONS
      {y | ?vl. vl IN barV V 3 /\
                y = rogers V vl INTER ball (v,sqrt (&2))  /\
                truncate_simplex 0 vl = [v]}`);
 (ASM_REWRITE_TAC[]);
 (ONCE_REWRITE_TAC[SET_EQ_LEMMA]);
 (REWRITE_TAC[IN_INTER; IN_UNIONS]);
 (ONCE_REWRITE_TAC[IN]);
 (REWRITE_TAC[IN_ELIM_THM]);
 (REPEAT STRIP_TAC);

 (EXISTS_TAC `rogers V vl INTER ball (v,sqrt (&2))`);
 (STRIP_TAC);
 (EXISTS_TAC `vl:(real^3)list`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[MESON[IN] `(a INTER b) x <=> x IN (a INTER b)`]);
 (ASM_SIMP_TAC[IN_INTER]);
 (ASM_SET_TAC[]);

 (EXISTS_TAC `rogers V vl`);
 (STRIP_TAC);
 (EXISTS_TAC `vl:(real^3)list`);
 (ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (ASM_SET_TAC[]);

 (NEW_GOAL `NULLSET (voronoi_closed V v INTER ball (v,sqrt (&2)))`);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC NEGLIGIBLE_UNIONS);
 (REWRITE_TAC[IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);


 (ABBREV_TAC `s2 = V INTER ball (v:real^3, &4)`);
 (ABBREV_TAC `s3 = {ul | ?u0 u1 u2 u3.
                      u0 IN s2 /\
                      u1 IN s2 /\
                      u2 IN s2 /\
                      u3 IN s2 /\
                      ul = [u0; u1; u2; u3:real^3]}`);
 (ABBREV_TAC `f = (\t. rogers V t INTER ball (v:real^3,sqrt (&2)))`);
 (MATCH_MP_TAC FINITE_SUBSET);

 (EXISTS_TAC `{y | ?vl. vl IN s3 /\y = (f:((real^3)list)->real^3->bool) vl}`);
 (REPEAT STRIP_TAC);
 (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
 (EXPAND_TAC "s3");
 (MATCH_MP_TAC FINITE_SET_LIST_LEMMA);
 (EXPAND_TAC "s2");
 (MATCH_MP_TAC Pack1.KIUMVTC);
 (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);

 (EXPAND_TAC "f" THEN EXPAND_TAC "s3");
 (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]    THEN REPEAT STRIP_TAC);
 (NEW_GOAL `?u0 u1 u2 u3. vl = [u0;u1;u2;u3:real^3]`);
 (MATCH_MP_TAC BARV_3_EXPLICIT);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `vl:(real^3)list`);
 (ASM_REWRITE_TAC[]);
 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
 (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `!s:real^3. s IN set_of_list vl ==> s IN s2`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "s2");

 (NEW_GOAL `set_of_list vl SUBSET (V INTER ball (v:real^3, &4))`);
 (REWRITE_TAC[SUBSET_INTER]);
 (STRIP_TAC);
 (MATCH_MP_TAC Packing3.BARV_SUBSET);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);

 (MATCH_MP_TAC BARV_3_IMP_FINITE_lemma2);
 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `v = HD [v:real^3]`);
 (REWRITE_TAC[HD]);
 (ONCE_REWRITE_TAC[ASSUME `v = HD [v:real^3]`]);
 (REWRITE_TAC[GSYM (ASSUME `truncate_simplex 0 vl = [v:real^3]`)]);
 (REWRITE_TAC[ASSUME `vl = [u0; u1; u2; u3:real^3]`]);
 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_0; HD;set_of_list]);
 (SET_TAC[]);
 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 (REPEAT STRIP_TAC);
 (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
 (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
 (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
 (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);

 (ASM_REWRITE_TAC[]);
 (ASM_SIMP_TAC[]);

 (NEW_GOAL `NULLSET (ball (v, &1))`);
 (MATCH_MP_TAC NEGLIGIBLE_SUBSET);
 (EXISTS_TAC `voronoi_closed V v INTER ball (v:real^3,sqrt (&2))`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[SUBSET; IN_INTER; IN_BALL; voronoi_closed]);
 (REWRITE_TAC[IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `w = v:real^3`);
 (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
 (NEW_GOAL `dist (v,w) <= dist (v, x) + dist (x, w:real^3)`);
 (REWRITE_TAC[DIST_TRIANGLE]);
 (NEW_GOAL `&2 <= dist (v,w:real^3)`);
 (UNDISCH_TAC `packing (V:real^3->bool)`);
 (REWRITE_TAC[packing] THEN STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
 (ASM_SET_TAC[]);
 (REWRITE_WITH `dist (x,v) = dist (v,x:real^3)`);
 (REWRITE_TAC[DIST_SYM]);
 (ASM_REAL_ARITH_TAC);
 (NEW_GOAL `&1 < sqrt (&2)`);
 (REWRITE_WITH `&1 < sqrt (&2) <=> &1 pow 2 < sqrt (&2) pow 2`);
 (MATCH_MP_TAC Pack1.bp_bdt);
 (ASM_SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &1 /\ &0 <= &2`]);
 (ASM_SIMP_TAC[SQRT_POW_2; REAL_ARITH `&0 <= &2`]);
 (REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);
 (NEW_GOAL `F`);
 (NEW_GOAL `vol (ball (v, &1)) = &4 / &3 * pi * (&1) pow 3`);
 (ASM_SIMP_TAC[REAL_ARITH `&0 <= &1`; VOLUME_BALL]);
 (NEW_GOAL `vol (ball (v, &1)) > &0`);
 (ASM_REWRITE_TAC[REAL_ARITH `&4 / &3 * pi * &1 pow 3 > &0 <=> 
                   &0 < &4 / &3 * pi`]);
 (MATCH_MP_TAC REAL_LT_MUL);
 (STRIP_TAC);
 (MATCH_MP_TAC REAL_LT_DIV THEN REAL_ARITH_TAC);
 (REWRITE_TAC[PI_POS]);

 (NEW_GOAL `vol (ball (v,&1)) = &0`);
 (REWRITE_WITH `vol (ball (v,&1)) = &0 <=> NULLSET (ball (v,&1))`);
 (MATCH_MP_TAC MEASURABLE_MEASURE_EQ_0);
 (REWRITE_TAC[MEASURABLE_BALL]);
 (ASM_REWRITE_TAC[]);
 (ASM_REAL_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE 
 `~(!i ul.  1 <= i /\ i <= 4 /\ barV V 3 ul /\ truncate_simplex 0 ul = [v]
            ==> NULLSET (mcell i V ul)) <=>
   (?i ul. 1 <= i /\ i <= 4 /\ barV V 3 ul /\ truncate_simplex 0 ul = [v] /\
      ~NULLSET (mcell i V ul))`]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `mcell i V ul`);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `i:num` THEN EXISTS_TAC `ul:(real^3)list`);
 (ASM_REWRITE_TAC[]);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `V INTER mcell i V ul = 
   set_of_list (truncate_simplex (i - 1) ul)`);
 (MATCH_MP_TAC LEPJBDJ);
 (ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (UNDISCH_TAC `~NULLSET (mcell i V ul) ` THEN  
   ASM_REWRITE_TAC[NEGLIGIBLE_EMPTY]);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
 (MATCH_MP_TAC BARV_3_EXPLICIT);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (NEW_GOAL `set_of_list (truncate_simplex 0 ul) SUBSET
               set_of_list (truncate_simplex (i-1) (ul:(real^3)list))`);
 (MATCH_MP_TAC Rogers.TRUNCATE_SIMPLEX_SUBSET);
 (ASM_REWRITE_TAC[LENGTH] THEN ASM_ARITH_TAC);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_0; set_of_list]);
 (SET_TAC[])]);;
(* ======================================================================= *)
(*   Main theorem                                                          *)
(* ======================================================================= *)


let QZYZMJC = prove_by_refinement ( QZYZMJC1_concl,

[(REPEAT STRIP_TAC);

(* Simplify the set *)
 (REWRITE_WITH 
  `{X | mcell_set V X /\ v IN VX V X} = 
   {X | mcell_set V X /\ ~(negligible X) /\ v IN V INTER X}`);
 (REWRITE_TAC[SET_EQ_LEMMA]);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[IN; IN_ELIM_THM]);
 (STRIP_TAC);
 (ASM_SET_TAC[]);
 (NEW_GOAL `v IN VX V x`);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC);
 (ASM_CASES_TAC `negligible (x:real^3->bool)`);
 (REWRITE_TAC[VX]);
 (COND_CASES_TAC);
 (SET_TAC[]);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);
 (NEW_GOAL `x IN mcell_set V`);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[mcell_set;IN;IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (ASM_MESON_TAC[]);
 (REWRITE_WITH `V INTER x = VX V x`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC HDTFNFZ);
 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);

 (REWRITE_TAC[IN; IN_ELIM_THM] THEN STRIP_TAC);
 (ASM_SET_TAC[]);
 (REWRITE_WITH `VX V x = V INTER x`);
 (MATCH_MP_TAC HDTFNFZ);
 (NEW_GOAL `x IN mcell_set V`);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[mcell_set;IN;IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[GSYM (ASSUME `x = mcell i V ul`)] THEN ASM_SET_TAC[]);
 (REWRITE_TAC[MESON [IN] `(V INTER x) v <=> v IN V INTER x`]);
 (ASM_SET_TAC[]);
 (* finish simplifyng the set *)

(* -------------------------------------------------------------------------- *)
(* begin to prove the set is finite *)


 (NEW_GOAL  `FINITE {X | mcell_set V X /\ v IN V INTER X}`);
 (REWRITE_TAC[mcell_set_2; IN_ELIM_THM]);
 (ABBREV_TAC `s = {(i, ul)| barV V 3 ul /\ v IN V INTER mcell i V ul /\ i <= 4}`);
 (ABBREV_TAC `f = (\x:num#(real^3)list. mcell (FST x) V (SND x))`);

 (REWRITE_WITH 
  `{X |(?i ul. X = mcell i V ul /\ ul IN barV V 3/\ i <= 4) /\ v IN V INTER X}
 = {X | ?y:num#(real^3)list. y IN s /\ X = f y}`);

 (EXPAND_TAC "s" THEN EXPAND_TAC "f");
 (ONCE_REWRITE_TAC[SET_EQ_LEMMA] THEN ONCE_REWRITE_TAC[IN]);
 (REWRITE_TAC[IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `(i:num, ul:(real^3)list)`);
 (ASM_REWRITE_TAC[FST;SND]);
 (EXISTS_TAC `i:num` THEN EXISTS_TAC `ul:(real^3)list`);
 (REWRITE_TAC[GSYM (ASSUME `x = mcell i V ul`)]);
 (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);
 (EXISTS_TAC `i:num` THEN EXISTS_TAC `ul:(real^3)list`);
 (ASM_REWRITE_TAC[IN]);
 (ASM_REWRITE_TAC[]);

 (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
 (EXPAND_TAC "s");
 (ABBREV_TAC `s1 = {0,1,2,3,4}`);
 (ABBREV_TAC `s2 = V INTER ball (v:real^3, &4)`);
 (ABBREV_TAC `s3 = {ul | ?u0 u1 u2 u3.
                      u0 IN s2 /\
                      u1 IN s2 /\
                      u2 IN s2 /\
                      u3 IN s2 /\
                      ul = [u0; u1; u2; u3:real^3]}`);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{(i:num, ul:(real^3)list)| i IN s1 /\ ul IN s3}`);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_PRODUCT);
 (EXPAND_TAC "s1" THEN EXPAND_TAC "s3");
 (REWRITE_TAC[Geomdetail.FINITE6]);
 (MATCH_MP_TAC FINITE_SET_LIST_LEMMA);
 (EXPAND_TAC "s2" THEN MATCH_MP_TAC Pack1.KIUMVTC);
 (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
 (EXPAND_TAC "s1" THEN EXPAND_TAC "s3" THEN REWRITE_TAC[SUBSET]);
 (ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `i:num` THEN EXISTS_TAC `ul:(real^3)list`);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[SET_RULE `i IN {0,1,2,3,4} <=> i = 0\/i=1\/i=2\/i=3\/i=4`]);
 (ASM_ARITH_TAC);
 (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
 (MATCH_MP_TAC BARV_3_EXPLICIT);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
 (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `!s:real^3. s IN set_of_list ul ==> s IN s2`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "s2");

 (NEW_GOAL `set_of_list ul SUBSET (V INTER ball (v:real^3, &4))`);
 (REWRITE_TAC[SUBSET_INTER]);
 (STRIP_TAC);
 (MATCH_MP_TAC Packing3.BARV_SUBSET);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC BARV_3_IMP_FINITE_lemma2);
 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `V INTER mcell i V ul = set_of_list(truncate_simplex (i - 1) ul)`);
 (MATCH_MP_TAC LEPJBDJ);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_CASES_TAC `i = 0`);
 (UNDISCH_TAC `v IN V INTER mcell i V ul`);
 (REWRITE_TAC[ASSUME `i = 0`; MCELL_EXPLICIT; mcell0; IN_INTER; IN_DIFF]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `F`);
 (NEW_GOAL `v:real^3 = HD ul`);
 (MATCH_MP_TAC Marchal_cells_2_new.ROGERS_INTER_V_LEMMA);
 (EXISTS_TAC `V:real^3->bool`);
 (REWRITE_TAC[MESON[IN] `rogers V ul v <=> v IN rogers V ul`]);
 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `~(v:real^3 IN ball (HD ul,sqrt (&2)))`);
 (ASM_REWRITE_TAC[IN_BALL; DIST_REFL]);
 (ASM_SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);
 (ASM_ARITH_TAC);
 (ASM_SET_TAC[]);

 (NEW_GOAL `set_of_list (truncate_simplex (i - 1) ul) SUBSET 
  set_of_list (ul:(real^3)list)`);
 (MATCH_MP_TAC Rogers.SET_OF_LIST_TRUNCATE_SIMPLEX_SUBSET);
 (ASM_REWRITE_TAC[LENGTH] THEN ASM_ARITH_TAC);
 (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
 (ASM_SET_TAC[]);

 (ASM_SET_TAC[]);
 (REPEAT STRIP_TAC);
 (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
 (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
 (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
 (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
 (ASM_REWRITE_TAC[]);

(* finish to prove the set is finite *)
(* -------------------------------------------------------------------------- *)

 (NEW_GOAL `FINITE {X | mcell_set V X /\ ~NULLSET X /\ v IN V INTER X}`);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | mcell_set V X /\ v IN V INTER X}`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (SET_TAC[]);

 (ABBREV_TAC `S = {X | mcell_set V X /\ ~NULLSET X /\ v IN V INTER X}`);
 (ABBREV_TAC 
 `P = (\X r. X IN S ==> r > &0 /\ radial r v (X INTER ball (v:real^3,r)))`);
 (NEW_GOAL `?f:(real^3->bool)->real. (!X:real^3->bool. P X (f X))`);
 (REWRITE_TAC[GSYM SKOLEM_THM]);
 (EXPAND_TAC "P");
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `X:real^3 ->bool IN S`);
 (NEW_GOAL `?c. c > &0 /\ radial c v (X INTER ball (v:real^3,c))`);
 (REWRITE_TAC[GSYM eventually_radial]);
 (UP_ASM_TAC THEN EXPAND_TAC "S" THEN REWRITE_TAC[IN;IN_ELIM_THM;mcell_set]);
 (REPEAT STRIP_TAC);
 (ONCE_ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC URRPHBZ2);
 (ASM_REWRITE_TAC[] THEN UP_ASM_TAC THEN SET_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `c:real`);
 (STRIP_TAC THEN ASM_REWRITE_TAC[]);
 (EXISTS_TAC `&1`);
 (STRIP_TAC);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (UP_ASM_TAC THEN EXPAND_TAC "P" THEN STRIP_TAC);
 (REWRITE_WITH 
  `sum S (\t. sol v t) = 
   sum S (\t. &3 * vol (t INTER normball v (f t)) / (f t) pow 3)`);
 (MATCH_MP_TAC SUM_EQ);
 (REWRITE_TAC[BETA_THM]);
 (REPEAT STRIP_TAC);
 (MATCH_MP_TAC sol);

 (ASM_SIMP_TAC[NORMBALL_BALL; GSYM RADIAL_VS_RADIAL_NORM]);
 (MATCH_MP_TAC MEASURABLE_INTER);
 (REWRITE_TAC[MEASURABLE_BALL]);
 (UP_ASM_TAC THEN EXPAND_TAC"S" THEN REWRITE_TAC[IN;IN_ELIM_THM;mcell_set]);
 (STRIP_TAC THEN ASM_REWRITE_TAC[]);
 (ASM_SIMP_TAC[MEASURABLE_MCELL]);

 (NEW_GOAL `~(S:(real^3->bool)->bool = {})`);
 (EXPAND_TAC "S");
 (MATCH_MP_TAC MCELL_SET_NOT_EMPTY);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `?r. r > &0 /\ r < &1 /\ !x:real^3->bool. x IN S ==> r <= f x`);
 (NEW_GOAL `?r. r > &0 /\ !x:real^3->bool. x IN S ==> r <= f x`);
 (NEW_GOAL `?r. r IN (IMAGE f (S:(real^3->bool)->bool)) /\ 
                  (!x. x IN (IMAGE f S) ==> r <= x)`);
 (MATCH_MP_TAC INF_FINITE_LEMMA);
 (STRIP_TAC);
 (ASM_SIMP_TAC[FINITE_IMAGE]);
 (REWRITE_TAC[IMAGE_EQ_EMPTY]);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);

 (UNDISCH_TAC `r IN IMAGE (f:(real^3->bool)->real) S`);
 (REWRITE_TAC[IMAGE]);
 (ONCE_REWRITE_TAC[IN]);
 (REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC);
 (EXISTS_TAC `r:real`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_SIMP_TAC[]);
 (REPEAT STRIP_TAC);
 (FIRST_ASSUM MATCH_MP_TAC);
 (REWRITE_TAC[IMAGE; IN; IN_ELIM_THM]);
 (EXISTS_TAC `x':real^3->bool` THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `min r (inv(&2))`);
 (NEW_GOAL `inv (&2) > &0 /\ inv (&2) < &1`);
 (REAL_ARITH_TAC);
 (REWRITE_TAC[REAL_ARITH `a > b <=> b < a`]);
 (ASM_SIMP_TAC[REAL_LT_MIN]);
 (STRIP_TAC);
 (ASM_REAL_ARITH_TAC);
 (ASM_SIMP_TAC[REAL_MIN_LT]);
 (ASM_SIMP_TAC[REAL_MIN_LE]);
 (UP_ASM_TAC THEN STRIP_TAC);

 (REWRITE_WITH 
  `sum S (\t. &3 * vol (t INTER normball v (f t)) / f t pow 3)
 = sum S (\t. &3 * vol (t INTER normball (v:real^3) r)  / r pow 3)`);
 (MATCH_MP_TAC SUM_EQ);
 (REWRITE_TAC[BETA_THM] THEN REPEAT STRIP_TAC);
 (ABBREV_TAC `C:real^3->bool = x INTER normball v (f x)`);
 (REWRITE_WITH `x INTER normball v r = C INTER normball (v:real^3) r`);
 (EXPAND_TAC "C");
 (MATCH_MP_TAC (SET_RULE `A SUBSET B ==> x INTER A = (x INTER B) INTER A`));
 (REWRITE_TAC[normball; SUBSET;IN;IN_ELIM_THM]);
 (NEW_GOAL `r <= f (x:real^3->bool)`);
 (ASM_SIMP_TAC[]);
 (ASM_REAL_ARITH_TAC);

 (REWRITE_WITH `measurable (C INTER normball v r) /\
                 vol (C INTER normball v r) = 
                 vol C * (r / f (x:real^3->bool)) pow 3`);
 (MATCH_MP_TAC lemma_r_r'_fix2);
 (EXPAND_TAC "C" THEN REPEAT STRIP_TAC);
 (MATCH_MP_TAC MEASURABLE_INTER);
 (REWRITE_TAC[NORMBALL_BALL; MEASURABLE_BALL]);
 (UNDISCH_TAC `x:real^3->bool IN S` THEN EXPAND_TAC "S");
 (REWRITE_TAC[mcell_set;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_SIMP_TAC[MEASURABLE_MCELL]);
 (REWRITE_TAC[NORMBALL_BALL; GSYM RADIAL_VS_RADIAL_NORM]);
 (ASM_SIMP_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_SIMP_TAC[]);

 (REWRITE_TAC[REAL_POW_DIV]);
 (REWRITE_TAC[REAL_ARITH `a * (b * c / d) / c = (a * b / d) * (c / c)`]);
 (REWRITE_WITH `r pow 3 / r pow 3 = &1`);
 (MATCH_MP_TAC REAL_DIV_REFL);
 (MATCH_MP_TAC Real_ext.REAL_PROP_NZ_POW);
 (ASM_REAL_ARITH_TAC);
 (REAL_ARITH_TAC);

 (REWRITE_WITH 
 `sum S (\t:real^3->bool. &3 * vol (t INTER normball v r) / r pow 3) = 
  sum S (\t. (&3 / r pow 3) * vol (t INTER normball v r))`);
 (MATCH_MP_TAC SUM_EQ);
 (REWRITE_TAC[BETA_THM] THEN REAL_ARITH_TAC);
 (REWRITE_TAC [SUM_LMUL]);
 (ABBREV_TAC `g = (\t:real^3->bool. t INTER normball v r)`);
 (REWRITE_WITH `sum S (\t:real^3->bool. 
   vol (t INTER normball v r)) = sum S (\t. vol (g t))`);
 (EXPAND_TAC "g" THEN REWRITE_TAC[]);
 (REWRITE_WITH `sum S (\t:real^3->bool. vol (g t)) = measure (UNIONS (IMAGE g S))`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC MEASURE_NEGLIGIBLE_UNIONS_IMAGE);
 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "g");
 (REPEAT STRIP_TAC);
 (MATCH_MP_TAC MEASURABLE_INTER);
 (REWRITE_TAC[NORMBALL_BALL; MEASURABLE_BALL]);
 (UNDISCH_TAC `t:real^3->bool IN S` THEN EXPAND_TAC "S");
 (REWRITE_TAC[mcell_set;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_SIMP_TAC[MEASURABLE_MCELL]);

 (MATCH_MP_TAC NEGLIGIBLE_SUBSET);
 (EXISTS_TAC `t INTER y:real^3->bool`);
 (STRIP_TAC);
 (ASM_CASES_TAC `negligible (t INTER y:real^3->bool)`);
 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `t:real^3->bool IN S` THEN UNDISCH_TAC `y:real^3->bool IN S` 
   THEN EXPAND_TAC "S");
 (REWRITE_TAC[mcell_set_2;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `~(t = y:real^3->bool)`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `i' = i /\ mcell i' V ul' = mcell i V ul`);
 (MATCH_MP_TAC AJRIPQN);
 (REWRITE_TAC[GSYM (ASSUME `t = mcell i' V ul'`); 
   GSYM (ASSUME `y = mcell i V ul`)]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[SET_RULE `a IN {0,1,2,3,4}<=> a=0\/a=1\/a=2\/a=3\/a=4`]);
 (ASM_ARITH_TAC);
 (SET_TAC[]);

 (EXPAND_TAC "g" THEN EXPAND_TAC "S" THEN REWRITE_TAC[IMAGE]);

 (NEW_GOAL `!s p:real^3->bool. 
  UNIONS {y| ?x. x IN s /\ y = x INTER p} = 
  UNIONS {y| ?x. x IN s /\ y = x} INTER p`);
 (ONCE_REWRITE_TAC[SET_EQ_LEMMA]);
 (REPEAT STRIP_TAC);
 (ASM_SET_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[IN_INTER; IN_UNIONS]);

 (ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `x' INTER p:real^3->bool`);
 (STRIP_TAC);
 (EXISTS_TAC `x':real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[MESON[IN] `(x' INTER p) x <=> x IN x' INTER p`]);
 (ASM_SET_TAC[]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH 
 `UNIONS {y | ?x:real^3->bool. x IN S /\ y = x INTER normball v r} = 
  UNIONS {y | ?x. x IN S /\ y = x} INTER normball v r`);
 (UP_ASM_TAC THEN MESON_TAC[]);

(* ----------------------------------------------------------------------- *)
(* OK here *)

 (EXPAND_TAC "S");
 (ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);
 (ABBREV_TAC `S1 = 
   UNIONS {y | ?x:real^3->bool. (mcell_set V x /\ ~NULLSET x /\ 
   v IN V INTER x) /\ y = x} INTER normball v r`);
 (ABBREV_TAC `S2 = 
   UNIONS {y | ?x:real^3->bool. (mcell_set V x /\ NULLSET x /\ 
   v IN V INTER x) /\ y = x} INTER normball v r`);
 (ABBREV_TAC `S3 = 
   UNIONS {y | ?x:real^3->bool. (mcell_set V x /\ v IN V INTER x) /\ y = x} 
   INTER normball v r`);

 (NEW_GOAL `S3 = S2 UNION S1:real^3->bool`);
 (EXPAND_TAC "S1" THEN EXPAND_TAC "S2" THEN EXPAND_TAC "S3");
 (ONCE_REWRITE_TAC[SET_EQ_LEMMA] THEN REWRITE_TAC[IN_INTER; IN_UNIONS;
   IN_UNION; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `negligible (x':real^3->bool)`);
 (DISJ1_TAC);
 (STRIP_TAC);
 (EXISTS_TAC `t:real^3->bool` THEN STRIP_TAC);
 (EXISTS_TAC `x':real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (DISJ2_TAC);
 (STRIP_TAC);
 (EXISTS_TAC `t:real^3->bool` THEN STRIP_TAC);
 (EXISTS_TAC `x':real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);

 (EXISTS_TAC `t:real^3->bool` THEN STRIP_TAC);
 (EXISTS_TAC `x':real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);

 (EXISTS_TAC `t:real^3->bool` THEN STRIP_TAC);
 (EXISTS_TAC `x':real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `measure (S3:real^3->bool) = 
   measure S2 + measure (S1:real^3->bool) - measure (S2 INTER S1)`);
 (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MEASURE_UNION);
 (EXPAND_TAC "S1" THEN EXPAND_TAC "S2" THEN STRIP_TAC);

 (MATCH_MP_TAC MEASURABLE_INTER);
 (REWRITE_TAC[MEASURABLE_BALL; NORMBALL_BALL]);
 (MATCH_MP_TAC MEASURABLE_UNIONS);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | mcell_set V X /\ v IN V INTER X}`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[SUBSET; IN_INTER; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[IN_ELIM_THM; mcell_set; IN] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC MEASURABLE_MCELL);
 (ASM_REWRITE_TAC[]);

 (MATCH_MP_TAC MEASURABLE_INTER);
 (REWRITE_TAC[MEASURABLE_BALL; NORMBALL_BALL]);
 (MATCH_MP_TAC MEASURABLE_UNIONS);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | mcell_set V X /\ v IN V INTER X}`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[SUBSET; IN_INTER; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[IN_ELIM_THM; mcell_set; IN] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC MEASURABLE_MCELL);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `measure (S2:real^3->bool) = &0`);
 (EXPAND_TAC "S2");
 (MATCH_MP_TAC MEASURE_EQ_0);
 (MATCH_MP_TAC NEGLIGIBLE_SUBSET);
 (EXISTS_TAC `UNIONS {y | ?x:real^3->bool. (mcell_set V x /\ 
   NULLSET x /\ v IN V INTER x) /\ y = x}`);
 (REWRITE_TAC[SET_RULE `A INTER B SUBSET A`]);
 (MATCH_MP_TAC NEGLIGIBLE_UNIONS);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | mcell_set V X /\ v IN V INTER X}`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[SUBSET; IN_INTER; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[IN_ELIM_THM; mcell_set; IN] THEN REPEAT STRIP_TAC);
 (REWRITE_TAC[ASSUME `t = x:real^3->bool`]);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `measure (S2 INTER S1:real^3->bool) = &0`);
 (MATCH_MP_TAC MEASURE_EQ_0);
 (MATCH_MP_TAC NEGLIGIBLE_SUBSET);
 (EXISTS_TAC `S2:real^3->bool`);
 (REWRITE_TAC[SET_RULE `A INTER B SUBSET A`]);
 (REWRITE_WITH `negligible S2 <=> measure (S2:real^3->bool) = &0`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC MEASURABLE_MEASURE_EQ_0);
 (EXPAND_TAC "S2");
 (MATCH_MP_TAC MEASURABLE_INTER);
 (REWRITE_TAC[MEASURABLE_BALL; NORMBALL_BALL]);
 (MATCH_MP_TAC MEASURABLE_UNIONS);
 (STRIP_TAC);
 (MATCH_MP_TAC FINITE_SUBSET);
 (EXISTS_TAC `{X | mcell_set V X /\ v IN V INTER X}`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[SUBSET; IN_INTER; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[IN_ELIM_THM; mcell_set; IN] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC MEASURABLE_MCELL);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);

 (REWRITE_WITH `vol S1 = vol S3`);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_WITH `S3 = normball (v:real^3) r`);
 (EXPAND_TAC "S3");
 (REWRITE_TAC[SET_RULE `A INTER B = B <=> B SUBSET A`]);

 (NEW_GOAL `normball v r SUBSET voronoi_closed V (v:real^3)`);
 (REWRITE_TAC[NORMBALL_BALL; SUBSET; IN_BALL; voronoi_closed]);
 (REWRITE_TAC[IN; IN_ELIM_THM]);
 (REPEAT STRIP_TAC);

 (ASM_CASES_TAC `w = v:real^3`);
 (ASM_REWRITE_TAC[]);
 (REAL_ARITH_TAC);

 (NEW_GOAL `dist (v, w) <= dist (v, x) + dist (x, w:real^3)`);
 (REWRITE_TAC[DIST_TRIANGLE]);
 (REWRITE_WITH `dist (x,v:real^3) = dist (v, x)`);
 (REWRITE_TAC[DIST_SYM]);
 (NEW_GOAL `&2 <= dist (v, w:real^3)`);
 (UNDISCH_TAC `packing (V:real^3->bool)` THEN REWRITE_TAC[packing] 
   THEN REPEAT STRIP_TAC);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (ASM_REAL_ARITH_TAC);

 (NEW_GOAL `voronoi_closed V (v:real^3) INTER normball v r SUBSET UNIONS 
  {y | ?x. (mcell_set V x /\ v IN V INTER x) /\ y = x}`);
 (REWRITE_TAC[SUBSET; IN_UNIONS; IN_INTER] THEN GEN_TAC);
 (REWRITE_WITH `x IN voronoi_closed V v <=>  (?vl. vl IN barV V 3 /\
                    x IN rogers V vl /\
                    truncate_simplex 0 vl = [v:real^3])`);
 (MATCH_MP_TAC GLTVHUM);
 (ASM_REWRITE_TAC[]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `?i. i <= 4 /\ x IN mcell i V vl`);
 (MATCH_MP_TAC SLTSTLO1);
 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `vl IN barV V 3 ` THEN REWRITE_TAC[IN]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `mcell i V vl`);
 (ASM_REWRITE_TAC[mcell_set] THEN ONCE_REWRITE_TAC[IN]);
 (REWRITE_TAC[IN_ELIM_THM]);
 (EXISTS_TAC `mcell i V vl`);
 (REWRITE_TAC[]);
 (STRIP_TAC);
 (EXISTS_TAC `i:num` THEN EXISTS_TAC `vl:(real^3)list`);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `i = 0`);
 (UNDISCH_TAC `x IN mcell i V vl` THEN ASM_REWRITE_TAC
   [MCELL_EXPLICIT; mcell0; IN_DIFF; IN_BALL]);
 (NEW_GOAL `?u0 u1 u2 u3. vl = [u0;u1;u2;u3:real^3]`);
 (MATCH_MP_TAC BARV_3_EXPLICIT);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `vl IN barV V 3 ` THEN REWRITE_TAC[IN]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 0 vl)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3. HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);

 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_0; HD]);
 (STRIP_TAC);
 (NEW_GOAL `F`);
 (UNDISCH_TAC `x:real^3 IN normball v r`);
 (REWRITE_TAC[NORMBALL_BALL; IN_BALL]);
 (NEW_GOAL `&1 < sqrt (&2)`);
 (REWRITE_WITH `&1 < sqrt (&2) <=> &1 pow 2 < sqrt (&2) pow 2`);
 (MATCH_MP_TAC Pack1.bp_bdt);
 (ASM_SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &1 /\ &0 <= &2`]);
 (ASM_SIMP_TAC[SQRT_POW_2; REAL_ARITH `&0 <= &2`]);
 (REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `V INTER mcell i V vl = 
   set_of_list (truncate_simplex (i - 1) vl)`);
 (MATCH_MP_TAC LEPJBDJ);
 (ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (UNDISCH_TAC `vl IN barV V 3 ` THEN REWRITE_TAC[IN]);
 (STRIP_TAC);
 (ASM_ARITH_TAC);
 (SWITCH_TAC THEN UP_ASM_TAC THEN SET_TAC[]);

 (NEW_GOAL `v IN V INTER mcell i V vl`);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `?u0 u1 u2 u3. vl = [u0;u1;u2;u3:real^3]`);
 (MATCH_MP_TAC BARV_3_EXPLICIT);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `vl IN barV V 3 ` THEN REWRITE_TAC[IN]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (NEW_GOAL `set_of_list (truncate_simplex 0 vl) SUBSET
               set_of_list (truncate_simplex (i-1) (vl:(real^3)list))`);
 (MATCH_MP_TAC Rogers.TRUNCATE_SIMPLEX_SUBSET);
 (ASM_REWRITE_TAC[LENGTH] THEN ASM_ARITH_TAC);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_0; set_of_list]);
 (SET_TAC[]);
 (UP_ASM_TAC THEN SET_TAC[]);

 (UP_ASM_TAC THEN REWRITE_WITH 
  `voronoi_closed V v INTER normball v r = normball (v:real^3) r`);
 (ASM_SET_TAC[]);

 (REWRITE_TAC[NORMBALL_BALL]);
 (REWRITE_WITH `vol (ball (v:real^3,r)) = &4 / &3 * pi * r pow 3`);
 (MATCH_MP_TAC VOLUME_BALL);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_TAC[REAL_ARITH `&3 / r pow 3 * &4 / &3 * pi * r pow 3 = 
                           (&4 * pi) * (r pow 3 / r pow 3)`]);
 (REWRITE_WITH `r pow 3 / r pow 3 = &1`);
 (MATCH_MP_TAC REAL_DIV_REFL);
 (MATCH_MP_TAC REAL_POW_NZ);
 (ASM_REAL_ARITH_TAC);
 (REAL_ARITH_TAC)]);;

end;;