(* ========================================================================= *)
(*                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;;