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