(* ========================================================================= *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Authour : VU KHAC KY *) (* Book lemma: UPFZBZM *) (* SUM_GAMMAX_LMFUN_ESTIMATE - a supported lemma. *) (* Chaper : Packing (Clusters) *) (* *) (* ========================================================================= *) open Sum_beta_bump;; let TSKAJXY_statement = new_definition `TSKAJXY_statement <=> (!V X. saturated V /\ packing V /\ mcell_set V X /\ critical_edgeX V X = {} ==> gammaX V X lmfun >= &0)`;; let SUM_GAMMAX_LMFUN_ESTIMATE_concl = `!V. ?c. !r. saturated V /\ packing V /\ &1 <= r /\ cell_cluster_estimate V /\ TSKAJXY_statement ==> c * r pow 2 <= sum {X | X SUBSET ball (vec 0, r) /\ mcell_set V X} (\X. gammaX V X lmfun)`;; (* ========================================================================= *) (* ========================================================================= *) let SUM_GAMMAX_LMFUN_ESTIMATE = prove_by_refinement ( SUM_GAMMAX_LMFUN_ESTIMATE_concl, [(GEN_TAC); (* ================== Choose the constants ================================= *) (NEW_GOAL `?cc1. (&1 <= cc1) /\ (!V X. packing V /\ saturated V /\ mcell_set V X ==> gammaX V X lmfun <= cc1)`); (MP_TAC BOUND_GAMMA_X_lmfun THEN STRIP_TAC); (EXISTS_TAC `max (c:real) (&1)`); (STRIP_TAC); (REAL_ARITH_TAC); (REPEAT STRIP_TAC); (NEW_GOAL `gammaX V X lmfun <= c`); (ASM_MESON_TAC[]); (ASM_REAL_ARITH_TAC); (UP_ASM_TAC THEN STRIP_TAC); (NEW_GOAL `?cc2. (&1 <= cc2) /\ (!V u0. saturated V /\ packing V /\ u0 IN V ==> & (CARD {X | mcell_set V X /\ VX V X u0}) <= cc2)`); (MP_TAC CARD_MCELL_CONTAINS_POINT_klemma); (STRIP_TAC); (EXISTS_TAC `max (&c:real) (&1)`); (STRIP_TAC); (REAL_ARITH_TAC); (REPEAT STRIP_TAC); (NEW_GOAL `&(CARD {X | mcell_set V X /\ VX V X u0}) <= (&c:real)`); (REWRITE_TAC[REAL_OF_NUM_LE]); (ASM_MESON_TAC[]); (ABBREV_TAC `s = &(CARD {X | mcell_set V X /\ VX V X u0})`); (ASM_REAL_ARITH_TAC); (UP_ASM_TAC THEN STRIP_TAC); (NEW_GOAL `?cc3. &1 <= cc3 /\ (!V X e. saturated V /\ packing V /\ mcell_set V X /\ critical_edgeX V X e ==> beta_bump V e X <= cc3)`); (MP_TAC BOUND_BETA_BUMP THEN STRIP_TAC); (EXISTS_TAC `max (c:real) (&1)`); (STRIP_TAC); (REAL_ARITH_TAC); (REPEAT STRIP_TAC); (NEW_GOAL `beta_bump V e X <= c`); (ASM_MESON_TAC[]); (ASM_REAL_ARITH_TAC); (UP_ASM_TAC THEN STRIP_TAC); (NEW_GOAL `?cc4. &1 <= cc4 /\ (!V u0. saturated V /\ packing V /\ u0 IN V ==> &(CARD {X | mcell_set V X /\ VX V X u0}) <= cc4)`); (MP_TAC CARD_MCELL_CONTAINS_POINT_klemma THEN STRIP_TAC); (EXISTS_TAC `max (&c) (&1)`); (STRIP_TAC); (REAL_ARITH_TAC); (REPEAT STRIP_TAC); (NEW_GOAL `&(CARD {X | mcell_set V X /\ VX V X u0}) <= &c`); (REWRITE_TAC[REAL_OF_NUM_LE]); (ASM_MESON_TAC[]); (ABBREV_TAC `s = &(CARD {X | mcell_set V X /\ VX V X u0})`); (ASM_REAL_ARITH_TAC); (UP_ASM_TAC THEN STRIP_TAC); (ASM_CASES_TAC `saturated V /\ packing V`); (NEW_GOAL `?dd1. !r. &1 <= r ==> &(CARD (V INTER ball ((vec 0):real^3,r) DIFF V INTER ball (vec 0,r - &8))) <= dd1 * r pow 2`); (REWRITE_WITH `!r p. V INTER ball (p:real^3,r) DIFF V INTER ball (p,r - &8) = V INTER ball (p:real^3,r + &0) DIFF V INTER ball (p,r - &8)`); (ASM_REWRITE_TAC[REAL_ARITH `a + &0 = a`]); (ASM_SIMP_TAC[PACKING_BALL_BOUNDARY]); (TAKE_TAC); (ABBREV_TAC `dd2 = max dd1 (&1)`); (ABBREV_TAC `dd = &1 / &2 * dd2 * (&4) pow 3 * cc2 * cc1`); (NEW_GOAL `?dd3. !r. &1 <= r ==> &(CARD (V INTER ball ((vec 0):real^3,r) DIFF V INTER ball (vec 0,r - &16))) <= dd3 * r pow 2`); (REWRITE_WITH `!r p. V INTER ball (p:real^3,r) DIFF V INTER ball (p,r - &16) = V INTER ball (p:real^3,r + &0) DIFF V INTER ball (p,r - &16)`); (ASM_REWRITE_TAC[REAL_ARITH `a + &0 = a`]); (ASM_SIMP_TAC[PACKING_BALL_BOUNDARY]); (TAKE_TAC); (ABBREV_TAC `dd4 = max dd3 (&1)`); (ABBREV_TAC `ss1 = (&4) pow 3 * cc4 * cc3`); (ABBREV_TAC `ss = &1 / &2 * dd4 * ss1`); (ABBREV_TAC `c:real = -- (dd + ss)`); (EXISTS_TAC `c:real`); (* ============================================================================ *) (REPEAT STRIP_TAC); (NEW_GOAL `!X. mcell_set V X /\ critical_edgeX V X = {} ==> gammaX V X lmfun >= &0`); (UP_ASM_TAC THEN REWRITE_TAC[TSKAJXY_statement]); (STRIP_TAC); (ASM_SIMP_TAC[]); (ABBREV_TAC `B = {X | X SUBSET ball (vec 0, r) /\ mcell_set V X}`); (ABBREV_TAC `B0 = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\ critical_edgeX V X = {}}`); (ABBREV_TAC `B1 = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\ ~(critical_edgeX V X = {})}`); (NEW_GOAL `FINITE (B1:(real^3->bool)->bool)`); (EXPAND_TAC "B1"); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `{X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`); (STRIP_TAC); (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]); (SET_TAC[]); (REWRITE_WITH `B = B0 UNION B1:(real^3->bool)->bool`); (EXPAND_TAC "B" THEN EXPAND_TAC "B1" THEN EXPAND_TAC "B0"); (SET_TAC[]); (REWRITE_WITH `sum (B0 UNION B1) (\X. gammaX V X lmfun) = sum B0 (\X. gammaX V X lmfun) + sum B1 (\X. gammaX V X lmfun)`); (MATCH_MP_TAC SUM_UNION); (REPEAT STRIP_TAC); (EXPAND_TAC "B0"); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `{X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`); (STRIP_TAC); (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]); (SET_TAC[]); (ASM_REWRITE_TAC[]); (EXPAND_TAC "B1" THEN EXPAND_TAC "B0"); (SET_TAC[]); (MATCH_MP_TAC (REAL_ARITH `&0 <= b /\ a <= c ==> a <= b + c`)); (STRIP_TAC); (MATCH_MP_TAC SUM_POS_LE); (STRIP_TAC); (EXPAND_TAC "B0"); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `{X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`); (STRIP_TAC); (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]); (SET_TAC[]); (REWRITE_TAC[BETA_THM; REAL_ARITH `&0 <= a <=> a >= &0`]); (EXPAND_TAC "B0" THEN REWRITE_TAC[IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (ASM_SIMP_TAC[]); (REWRITE_WITH `sum B1 (\X. gammaX V X lmfun) = sum B1 (\X. (gammaX V X lmfun) * sum (critical_edgeX V X) (\e. critical_weight V X))`); (MATCH_MP_TAC SUM_EQ); (EXPAND_TAC "B1" THEN REWRITE_TAC[IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (REWRITE_TAC[critical_weight]); (REWRITE_WITH `sum (critical_edgeX V x) (\e. &1 / &(CARD (critical_edgeX V x))) = &(CARD (critical_edgeX V x)) * (&1 / &(CARD (critical_edgeX V x)))`); (MATCH_MP_TAC SUM_CONST); (REWRITE_TAC[FINITE_critical_edgeX]); (REWRITE_TAC[REAL_ARITH `a * &1 / a = a / a`]); (REWRITE_WITH `&(CARD (critical_edgeX V x)) / &(CARD (critical_edgeX V x)) = &1`); (MATCH_MP_TAC REAL_DIV_REFL); (REWRITE_TAC[REAL_OF_NUM_EQ]); (REWRITE_WITH `CARD (critical_edgeX V x) = 0 <=> critical_edgeX V x = {}`); (MATCH_MP_TAC CARD_EQ_0); (REWRITE_TAC[FINITE_critical_edgeX]); (ASM_REWRITE_TAC[]); (REAL_ARITH_TAC); (* ------------------------------------------------------------------------- *) (* Hint: - See proofs of KIZHLTL1; KIZHLTL2 to adapt *) (* ------------------------------------------------------------------------- *) (REWRITE_TAC[GSYM SUM_LMUL]); (ABBREV_TAC `T1:real^3->bool = V INTER ball (vec 0, r)`); (ABBREV_TAC `T2 = {{u0, u1:real^3} | u0 IN T1 /\ u1 IN T1 /\ ~(u0 = u1) /\ hl [u0; u1] <= hplus}`); (NEW_GOAL `FINITE (T2:(real^3->bool)->bool)`); (EXPAND_TAC "T2" THEN MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `{{u0, u1:real^3} | u0 IN T1 /\ u1 IN T1}`); (STRIP_TAC); (MATCH_MP_TAC FINITE_SET_PRODUCT_KY_LEMMA); (EXPAND_TAC "T1" THEN MATCH_MP_TAC Pack2.KIUMVTC); (ASM_REWRITE_TAC[]); (SET_TAC[]); (REWRITE_WITH `sum B1 (\X. sum (critical_edgeX V X) (\x. gammaX V X lmfun * critical_weight V X)) = sum B1 (\X. sum {y:real^3->bool| y IN T2 /\ critical_edgeX V X y} (\x. gammaX V X lmfun * critical_weight V X))`); (MATCH_MP_TAC SUM_EQ); (EXPAND_TAC "B1" THEN REWRITE_TAC[IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (AP_THM_TAC THEN AP_TERM_TAC); (REWRITE_TAC[SET_RULE `a = b <=> b SUBSET a /\ a SUBSET b`]); (STRIP_TAC); (SET_TAC[]); (REWRITE_TAC[SET_RULE `A SUBSET {y | T2 y /\ A y} <=> A SUBSET T2`]); (EXPAND_TAC "T2" THEN REWRITE_TAC[SUBSET; critical_edgeX; IN; IN_ELIM_THM; edgeX]); (REPEAT STRIP_TAC); (EXPAND_TAC "T1" THEN REWRITE_TAC[IN_ELIM_THM]); (EXISTS_TAC `u':real^3` THEN EXISTS_TAC `v':real^3`); (REWRITE_TAC[ASSUME `~(u' = v':real^3)`]); (REWRITE_TAC[ASSUME `x' = {u, v:real^3}`; MESON[IN] `V (x:real^3) <=> x IN V`; GSYM (ASSUME `{u, v} = {u', v':real^3}`); IN_INTER]); (NEW_GOAL `VX V x = V INTER x`); (MATCH_MP_TAC Hdtfnfz.HDTFNFZ); (UNDISCH_TAC `mcell_set V x` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]); (STRIP_TAC); (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`); (ASM_REWRITE_TAC[]); (STRIP_TAC); (NEW_GOAL `VX V x = {}`); (REWRITE_TAC[VX]); (ASM_REWRITE_TAC[]); (UNDISCH_TAC `VX V x u'` THEN ASM_REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]); (SET_TAC[]); (STRIP_TAC); (ASM_SET_TAC[]); (STRIP_TAC); (ASM_SET_TAC[]); (REWRITE_WITH `hl [u'; v':real^3] = hl [u; v:real^3]`); (ASM_REWRITE_TAC[HL; set_of_list]); (ASM_REWRITE_TAC[]); (ABBREV_TAC `f = (\X. (\x:real^3->bool. gammaX V X lmfun * critical_weight V X))`); (REWRITE_WITH `sum B1 (\X. sum {y | y IN T2 /\ critical_edgeX V X y} (\x:real^3->bool. gammaX V X lmfun * critical_weight V X)) = sum B1 (\X. sum {y | y IN T2 /\ critical_edgeX V X y} (\x:real^3->bool. f X x))`); (EXPAND_TAC "f" THEN REFL_TAC); (REWRITE_WITH `sum B1 (\X. sum {y | y IN T2 /\ critical_edgeX V X y} (\x. f X x)) = sum T2 (\x. sum {X | X IN B1 /\ critical_edgeX V X x} (\X. f X x))`); (ASM_SIMP_TAC[SUM_SUM_RESTRICT]); (EXPAND_TAC "B1" THEN REWRITE_TAC[IN; IN_ELIM_THM]); (REWRITE_TAC[MESON[] `(A/\B/\C)/\D <=> A/\B/\C/\D`]); (REWRITE_WITH `sum T2 (\x. sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} (\X. f X x)) = sum T2 (\x. sum {X | mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} (\X. f X x)) - sum T2 (\x. sum {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} (\X. f X x))`); (REWRITE_TAC[REAL_ARITH `a = b - c <=> b = a + c`]); (REWRITE_WITH ` sum T2 (\x. sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} (\X. f X x)) + sum T2 (\x. sum {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} (\X. f X x)) = sum T2 (\x. (\x. sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} (\X. f X x)) x + (\x. sum {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} (\X. f X x)) x)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC SUM_ADD); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC SUM_EQ); (REWRITE_TAC[BETA_THM] THEN REPEAT STRIP_TAC); (REWRITE_WITH `sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} (\X. f X x) + sum {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} (\X. f X x) = sum ({X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} UNION {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}) (\X. f X x)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC SUM_UNION); (REPEAT STRIP_TAC); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `B1:(real^3->bool)->bool`); (ASM_REWRITE_TAC[]); (EXPAND_TAC "B1" THEN SET_TAC[]); (UP_ASM_TAC THEN EXPAND_TAC "T2"); (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `{X | X SUBSET ball (vec 0,r + &8) /\ mcell_set V X}`); (STRIP_TAC); (ASM_SIMP_TAC[Marchal_cells_3.FINITE_MCELL_SET_LEMMA]); (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (NEW_GOAL `x SUBSET VX V x'`); (UNDISCH_TAC `critical_edgeX V x' x` THEN REWRITE_TAC[critical_edgeX;edgeX]); (REWRITE_TAC[IN_ELIM_THM]); (REPEAT STRIP_TAC); (REWRITE_TAC[ASSUME `x = {u, v:real^3}`; ASSUME `{u, v:real^3} = {u', v'}`]); (SET_TAC[ASSUME `VX V x' u'`; ASSUME `VX V x' v'`]); (NEW_GOAL `VX V x' = V INTER x'`); (MATCH_MP_TAC Hdtfnfz.HDTFNFZ); (UNDISCH_TAC `mcell_set V x'` THEN REWRITE_TAC[mcell_set; IN_ELIM_THM; IN]); (REPEAT STRIP_TAC); (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`); (ASM_REWRITE_TAC[]); (STRIP_TAC); (NEW_GOAL `VX V x' = {}`); (ASM_REWRITE_TAC[VX]); (UNDISCH_TAC `x SUBSET VX V x'` THEN REWRITE_TAC[ASSUME `VX V x' = {}`]); (REWRITE_TAC[ASSUME `x = {u0, u1:real^3}`] THEN SET_TAC[]); (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`; IN_BALL]); (NEW_GOAL `dist (vec 0, x'') <= dist (vec 0, u0:real^3) + dist (u0, x'')`); (NORM_ARITH_TAC); (NEW_GOAL `dist (vec 0, u0:real^3) < r`); (REWRITE_TAC[GSYM IN_BALL]); (UNDISCH_TAC `(T1:real^3->bool) u0` THEN EXPAND_TAC "T1"); (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`] THEN SET_TAC[]); (NEW_GOAL `dist (u0, x'':real^3) < &8`); (REWRITE_TAC[GSYM IN_BALL]); (NEW_GOAL `x' SUBSET ball (u0:real^3,&8)`); (UNDISCH_TAC `mcell_set V x'` THEN REWRITE_TAC[mcell_set; IN_ELIM_THM; IN]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC MCELL_SUBSET_BALL8); (ASM_REWRITE_TAC[]); (REWRITE_TAC[GSYM (ASSUME `x' = mcell i V ul`)]); (UNDISCH_TAC `x SUBSET VX V x'` THEN UNDISCH_TAC `VX V x' = V INTER x'`); (ASM_REWRITE_TAC[]); (SET_TAC[]); (SUBGOAL_THEN `(x'':real^3) IN x'` MP_TAC); (UNDISCH_TAC `(x':real^3->bool) x''` THEN SET_TAC[]); (UP_ASM_TAC THEN SET_TAC[]); (ASM_REAL_ARITH_TAC); (ASM_REWRITE_TAC[]); (SET_TAC[]); (REWRITE_WITH ` ({X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} UNION {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}) = {X | mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}`); (SET_TAC[]); (REWRITE_WITH `(\x. sum {X | mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} (\X. f X x)) = (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (\X. f X x))`); (REWRITE_TAC[FUN_EQ_THM]); (STRIP_TAC); (REWRITE_WITH `{X | mcell_set V X /\ ~(!x. critical_edgeX V X x <=> {} x) /\ critical_edgeX V X x} = {X | mcell_set V X /\ critical_edgeX V X x}`); (REWRITE_TAC[SET_RULE `A = B <=> A SUBSET B /\ B SUBSET A`]); (STRIP_TAC); (SET_TAC[]); (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (REWRITE_TAC[MESON[IN] `(A:(real^3->bool)->bool) x <=> x IN A`]); (SET_TAC[]); (ASM_REWRITE_TAC[]); (REWRITE_WITH ` (\x. sum {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} (\X. f X x)) = (\x. sum {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x} (\X. f X x))`); (REWRITE_TAC[FUN_EQ_THM]); (STRIP_TAC); (REWRITE_WITH `{X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ ~(!x. critical_edgeX V X x <=> {} x) /\ critical_edgeX V X x} = {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x}`); (REWRITE_TAC[SET_RULE `A = B <=> A SUBSET B /\ B SUBSET A`]); (STRIP_TAC); (SET_TAC[]); (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM]); (GEN_TAC THEN DISCH_TAC); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN REPEAT STRIP_TAC); (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (REWRITE_TAC[MESON[IN] `(A:(real^3->bool)->bool) x <=> x IN A`]); (SET_TAC[]); (* OK here *) (MATCH_MP_TAC (REAL_ARITH `(?x. c <= x /\ a + x <= b) ==> a <= b - c`)); (EXISTS_TAC `dd * r pow 2`); (STRIP_TAC); (ABBREV_TAC `T3:real^3->bool = V INTER ball (vec 0, r) DIFF ball (vec 0, r - &8)`); (ABBREV_TAC `T4 = {{u0:real^3, u1} | u0 IN T3 /\ u1 IN T3 /\ ~(u0 = u1) /\ hl [u0; u1] <= hplus}`); (REWRITE_WITH `sum T2 (\x. sum {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x} (\X. f X x)) = sum T4 (\x. sum {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x} (\X. f X x))`); (EXPAND_TAC "T2"); (MATCH_MP_TAC SUM_SUPERSET); (STRIP_TAC); (EXPAND_TAC "T4" THEN EXPAND_TAC "T1" THEN EXPAND_TAC "T3" THEN SET_TAC[]); (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC); (REWRITE_WITH `{X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x} = {}`); (REWRITE_TAC[SET_RULE `x = {} <=> ~(?s. s IN x)`]); (REWRITE_TAC[IN; IN_ELIM_THM] THEN STRIP_TAC); (NEW_GOAL `(x:real^3->bool) SUBSET s`); (MATCH_MP_TAC CRITICAL_EDGEX_SUBSET_MCELL); (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]); (NEW_GOAL `?p:real^3. p IN s DIFF ball (vec 0,r)`); (UNDISCH_TAC `~(s SUBSET ball ((vec 0):real^3,r))` THEN SET_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (UP_ASM_TAC THEN REWRITE_TAC[IN_DIFF; IN_BALL; REAL_ARITH `~(a < r) <=> r <= a`] THEN STRIP_TAC); (NEW_GOAL `s SUBSET ball (p:real^3,&8)`); (MATCH_MP_TAC MCELL_SUBSET_BALL8_2); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (NEW_GOAL `u0:real^3 IN ball (p,&8) /\ u1 IN ball (p,&8)`); (ASM_SET_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[IN_BALL] THEN STRIP_TAC); (UNDISCH_TAC `~(T4:(real^3->bool)->bool) x`); (REWRITE_TAC[MESON[IN] `(T4:(real^3->bool)->bool) x <=> x IN T4`]); (EXPAND_TAC "T4" THEN EXPAND_TAC "T3" THEN REWRITE_TAC[IN_INTER; IN_DIFF; IN_BALL]); (REWRITE_TAC[IN; IN_ELIM_THM]); (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]); (UNDISCH_TAC `(T1:(real^3->bool)) u0` THEN UNDISCH_TAC `(T1:(real^3->bool)) u1`); (REWRITE_WITH `!x. T1 x <=> x:real^3 IN T1`); (ASM_REWRITE_TAC[IN]); (EXPAND_TAC "T1" THEN REWRITE_TAC[IN_INTER; IN_BALL]); (REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]); (NEW_GOAL `dist (vec 0,p) <= dist (p, u0) + dist (vec 0, u0:real^3)`); (NORM_ARITH_TAC); (ASM_REAL_ARITH_TAC); (NEW_GOAL `dist (vec 0,p) <= dist (p, u1) + dist (vec 0, u1:real^3)`); (NORM_ARITH_TAC); (ASM_REAL_ARITH_TAC); (REWRITE_TAC[SUM_CLAUSES]); (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`)); (EXISTS_TAC `sum T4 (\x:real^3->bool. cc2 * cc1)`); (STRIP_TAC); (MATCH_MP_TAC SUM_LE); (STRIP_TAC); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `{{u0:real^3, u1} | u0 IN T3 /\ u1 IN T3}`); (STRIP_TAC); (MATCH_MP_TAC FINITE_SUBSET); (ABBREV_TAC `S_temp = {u0, u1:real^3 | u0 IN T3 /\ u1 IN T3}`); (ABBREV_TAC `f_temp = (\(u0,u1:real^3). {u0, u1})`); (EXISTS_TAC `IMAGE (f_temp:real^3#real^3->real^3->bool) S_temp`); (STRIP_TAC); (MATCH_MP_TAC FINITE_IMAGE); (EXPAND_TAC "S_temp" THEN MATCH_MP_TAC FINITE_PRODUCT THEN REWRITE_TAC[]); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `T1:real^3->bool`); (STRIP_TAC); (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]); (ASM_SET_TAC[]); (EXPAND_TAC "f_temp" THEN EXPAND_TAC "S_temp" THEN REWRITE_TAC[IMAGE; SUBSET; IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `u0:real^3, u1:real^3` THEN ASM_REWRITE_TAC[]); (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]); (ASM_SET_TAC[]); (REWRITE_TAC[IN] THEN EXPAND_TAC "T4" THEN EXPAND_TAC "T3" THEN REWRITE_TAC[ABS_SIMP; IN_DIFF; IN_INTER; IN_ELIM_THM]); (REPEAT STRIP_TAC); (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`)); (EXISTS_TAC `sum {X| ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x} (\x. cc1)`); (STRIP_TAC); (MATCH_MP_TAC SUM_LE); (STRIP_TAC); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `{X | mcell_set V X /\ edgeX V X x}`); (STRIP_TAC); (MATCH_MP_TAC Marchal_cells_3.FINITE_EDGE_X2); (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]); (REWRITE_TAC[critical_edgeX] THEN SET_TAC[]); (REWRITE_TAC[BETA_THM; ABS_SIMP; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC); (EXPAND_TAC "f"); (NEW_GOAL `critical_weight V x' <= &1`); (REWRITE_TAC[critical_weight]); (REWRITE_WITH `&1 / &(CARD (critical_edgeX V x')) <= &1 <=> &1 <= &(CARD (critical_edgeX V x'))`); (MATCH_MP_TAC Packing3.REAL_DIV_LE_1); (REWRITE_TAC[REAL_OF_NUM_LT; ARITH_RULE `0 < a <=> ~(a = 0)`]); (REWRITE_WITH `CARD (critical_edgeX V x') = 0 <=> critical_edgeX V x' = {}`); (MATCH_MP_TAC CARD_EQ_0); (REWRITE_TAC[critical_edgeX; edgeX] THEN MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `{{u0:real^3, u1} | u0 IN VX V x' /\ u1 IN VX V x'}`); (STRIP_TAC); (MATCH_MP_TAC FINITE_SUBSET); (ABBREV_TAC `S_temp = {u0, u1:real^3 | u0 IN VX V x' /\ u1 IN VX V x'}`); (ABBREV_TAC `f_temp = (\(u0,u1:real^3). {u0, u1})`); (EXISTS_TAC `IMAGE (f_temp:real^3#real^3->real^3->bool) S_temp`); (STRIP_TAC); (MATCH_MP_TAC FINITE_IMAGE); (EXPAND_TAC "S_temp" THEN MATCH_MP_TAC FINITE_PRODUCT THEN REWRITE_TAC[]); (MATCH_MP_TAC FINITE_VX); (ASM_REWRITE_TAC[]); (EXPAND_TAC "f_temp" THEN EXPAND_TAC "S_temp" THEN REWRITE_TAC[IMAGE; SUBSET; IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `u0':real^3, u1':real^3` THEN ASM_REWRITE_TAC[]); (EXISTS_TAC `u0':real^3` THEN EXISTS_TAC `u1':real^3` THEN ASM_REWRITE_TAC[]); (ASM_SET_TAC[]); (UP_ASM_TAC THEN SET_TAC[]); (REWRITE_TAC[REAL_OF_NUM_LE; ARITH_RULE `1 <= a <=> ~(a = 0)`]); (REWRITE_WITH `CARD (critical_edgeX V x') = 0 <=> critical_edgeX V x' = {}`); (MATCH_MP_TAC CARD_EQ_0); (REWRITE_TAC[critical_edgeX; edgeX] THEN MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `{{u0:real^3, u1} | u0 IN VX V x' /\ u1 IN VX V x'}`); (STRIP_TAC); (MATCH_MP_TAC FINITE_SUBSET); (ABBREV_TAC `S_temp = {u0, u1:real^3 | u0 IN VX V x' /\ u1 IN VX V x'}`); (ABBREV_TAC `f_temp = (\(u0,u1:real^3). {u0, u1})`); (EXISTS_TAC `IMAGE (f_temp:real^3#real^3->real^3->bool) S_temp`); (STRIP_TAC); (MATCH_MP_TAC FINITE_IMAGE); (EXPAND_TAC "S_temp" THEN MATCH_MP_TAC FINITE_PRODUCT THEN REWRITE_TAC[]); (MATCH_MP_TAC FINITE_VX); (ASM_REWRITE_TAC[]); (EXPAND_TAC "f_temp" THEN EXPAND_TAC "S_temp" THEN REWRITE_TAC[IMAGE; SUBSET; IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `u0':real^3, u1':real^3` THEN ASM_REWRITE_TAC[]); (EXISTS_TAC `u0':real^3` THEN EXISTS_TAC `u1':real^3` THEN ASM_REWRITE_TAC[]); (ASM_SET_TAC[]); (UP_ASM_TAC THEN SET_TAC[]); (NEW_GOAL `&0 <= critical_weight V x'`); (REWRITE_TAC[critical_weight] THEN MATCH_MP_TAC REAL_LE_DIV); (REWRITE_TAC[REAL_ARITH `&0 <= &1`; REAL_OF_NUM_LE]); (ARITH_TAC); (NEW_GOAL `gammaX V x' lmfun <= cc1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `gammaX V x' lmfun * critical_weight V x' <= cc1 * critical_weight V x'`); (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]); (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]); (MATCH_MP_TAC REAL_LE_MUL THEN ASM_REAL_ARITH_TAC); (NEW_GOAL `cc1 * critical_weight V x' <= cc1`); (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]); (REWRITE_WITH `!x b. b - b * x = b * (&1 - x)`); (REAL_ARITH_TAC); (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (REWRITE_WITH `sum {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x} (\x. cc1) = &(CARD {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x}) * cc1`); (MATCH_MP_TAC SUM_CONST); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `{X | mcell_set V X /\ edgeX V X x}`); (STRIP_TAC); (MATCH_MP_TAC Marchal_cells_3.FINITE_EDGE_X2); (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]); (REWRITE_TAC[critical_edgeX] THEN SET_TAC[]); (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]); (REWRITE_TAC[REAL_ARITH `a * x - b * x = x * (a - b)`]); (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC); (ASM_REAL_ARITH_TAC); (NEW_GOAL ` &(CARD {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x}) <= &(CARD {X | mcell_set V X /\ VX V X u0})`); (REWRITE_TAC[REAL_OF_NUM_LE] THEN MATCH_MP_TAC CARD_SUBSET); (STRIP_TAC); (ASM_REWRITE_TAC[critical_edgeX; edgeX; IN; IN_ELIM_THM]); (SET_TAC[]); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `{X | X SUBSET ball (u0,&8) /\ mcell_set V X}`); (STRIP_TAC); (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA_2); (ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[SUBSET]); (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC); (MATCH_MP_TAC MCELL_SUBSET_BALL8_2); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (NEW_GOAL `VX V x' = V INTER x'`); (MATCH_MP_TAC Hdtfnfz.HDTFNFZ); (UNDISCH_TAC `mcell_set V x'` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC); (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`); (ASM_REWRITE_TAC[]); (STRIP_TAC); (UNDISCH_TAC `VX V x' u0` THEN ASM_REWRITE_TAC[VX]); (REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]); (SET_TAC[]); (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]); (ASM_REWRITE_TAC[]); (NEW_GOAL `&(CARD {X | mcell_set V X /\ VX V X u0}) <= cc2`); (ASM_MESON_TAC[]); (ABBREV_TAC `s1_temp = &(CARD {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x})`); (ABBREV_TAC `s2_temp = &(CARD {X | mcell_set V X /\ VX V X u0})`); (ASM_REAL_ARITH_TAC); (ABBREV_TAC `g = (\x:real^3->bool. cc2 * cc1)`); (REWRITE_WITH `sum T4 (g:(real^3->bool)->real) = &1 / &2 * sum {m,n | m IN T3 /\ n IN T3 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus} (\(m:real^3,n). g {m, n})`); (ONCE_REWRITE_TAC[REAL_ARITH `a = &1 / &2 * b <=> b = &2 * a`]); (EXPAND_TAC "T4"); (REWRITE_TAC[HL_2; REAL_ARITH `inv (&2) * a <= b <=> a <= &2 * b`]); (MATCH_MP_TAC SUM_PAIR_2_SET); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `T1:real^3->bool`); (STRIP_TAC); (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]); (ASM_SET_TAC[]); (REWRITE_TAC[REAL_ARITH `&1 / &2 * s <= t <=> s <= &2 * t`]); (ABBREV_TAC `h = (\m:real^3. {n | n IN T3 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus})`); (REWRITE_WITH `{m,n | m IN T3 /\ n IN T3 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus} = {m:real^3,n | m IN T3 /\ n IN h m}`); (EXPAND_TAC "h"); (SET_TAC[PAIR_EQ]); (ABBREV_TAC `k = (\m n. (g:(real^3->bool)->real) {m,n})`); (REWRITE_WITH `(\(m,n). (g:(real^3->bool)->real) {m, n}) = (\(m,n). k m n)`); (REWRITE_TAC[FUN_EQ_THM]); (STRIP_TAC); (NEW_GOAL `(x:real^3#real^3) = FST x, SND x`); (REWRITE_TAC[PAIR]); (ONCE_REWRITE_TAC[ASSUME `(x:real^3#real^3) = FST x, SND x`]); (EXPAND_TAC "k" THEN REWRITE_TAC[]); (REWRITE_WITH `sum {m:real^3,n:real^3 | m IN T3 /\ n IN h m} (\(m,n). k m n) = sum T3 (\m. sum (h m) (k m))`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC SUM_SUM_PRODUCT); (STRIP_TAC); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `T1:real^3->bool`); (STRIP_TAC); (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]); (ASM_SET_TAC[]); (REPEAT STRIP_TAC); (EXPAND_TAC "h"); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `T3:real^3->bool`); (STRIP_TAC); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `T1:real^3->bool`); (STRIP_TAC); (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]); (ASM_SET_TAC[]); (SET_TAC[]); (EXPAND_TAC "k" THEN EXPAND_TAC "g"); (NEW_GOAL `sum T3 (\m. sum ((h:real^3->real^3->bool) m) (\n. cc2 * cc1)) <= sum T3 (\m. (&4) pow 3 * cc2 * cc1)`); (MATCH_MP_TAC SUM_LE); (STRIP_TAC); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `T1:real^3->bool`); (STRIP_TAC); (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]); (ASM_SET_TAC[]); (EXPAND_TAC "h" THEN REPEAT STRIP_TAC THEN REWRITE_TAC[]); (REWRITE_WITH `sum {n:real^3 | n IN T3 /\ ~(x = n) /\ dist (x,n) <= &2 * hplus} (\n. cc2 * cc1) = &(CARD {n | n IN T3 /\ ~(x = n) /\ dist (x,n) <= &2 * hplus}) * (cc2 * cc1)`); (MATCH_MP_TAC SUM_CONST); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `T3:real^3->bool`); (STRIP_TAC); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `T1:real^3->bool`); (STRIP_TAC); (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]); (ASM_SET_TAC[]); (SET_TAC[]); (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]); (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]); (MATCH_MP_TAC REAL_LE_MUL); (STRIP_TAC); (ONCE_REWRITE_TAC[GSYM (REAL_ARITH `(a <= b <=> &0 <= b - a)`)]); (NEW_GOAL `&(CARD {n | n IN T3 /\ ~(x = n) /\ dist (x,n) <= &2 * hplus}) <= &(CARD (V INTER ball (x:real^3, &3)))`); (REWRITE_TAC[REAL_OF_NUM_LE]); (MATCH_MP_TAC CARD_SUBSET); (STRIP_TAC); (EXPAND_TAC "T3" THEN REWRITE_TAC[IN_DIFF; IN_BALL]); (REWRITE_TAC[IN_INTER; IN_BALL; IN_ELIM_THM; SUBSET; IN]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `&2 * hplus < &3`); (REWRITE_TAC[hplus] THEN REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]); (NEW_GOAL `&(CARD (V INTER ball (x:real^3,&3))) <= &4 pow 3`); (REWRITE_TAC[REAL_ARITH `&4 = &3 + &1`]); (MATCH_MP_TAC BOUNDS_VGEN_klemma); (ASM_REWRITE_TAC[REAL_ARITH `&0 <= &3`]); (ABBREV_TAC `s1 = &(CARD {n:real^3 | n IN T3 /\ ~(x = n) /\ dist (x,n) <= &2 * hplus})`); (ASM_REAL_ARITH_TAC); (MATCH_MP_TAC REAL_LE_MUL); (ASM_REAL_ARITH_TAC); (NEW_GOAL `sum T3 (\m:real^3. &4 pow 3 * cc2 * cc1) <= &2 * dd * r pow 2`); (REWRITE_WITH `sum T3 (\m:real^3. &4 pow 3 * cc2 * cc1) = &(CARD T3) * &4 pow 3 * cc2 * cc1`); (MATCH_MP_TAC SUM_CONST); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `T1:real^3->bool`); (STRIP_TAC); (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]); (ASM_SET_TAC[]); (EXPAND_TAC "dd"); (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]); (REWRITE_TAC[REAL_ARITH `&2 * (&1 / &2 * dd2 * &4 pow 3 * cc2 * cc1) * r pow 2 - &(CARD (T3:real^3->bool)) * &4 pow 3 * cc2 * cc1 = (&4 pow 3 * cc2 * cc1) * (dd2 * r pow 2 - &(CARD T3))`]); (MATCH_MP_TAC REAL_LE_MUL); (STRIP_TAC); (REWRITE_TAC[REAL_ARITH `&0 <= &4 pow 3 * x <=> &0 <= x`]); (MATCH_MP_TAC REAL_LE_MUL); (ASM_REAL_ARITH_TAC); (ONCE_REWRITE_TAC[GSYM (REAL_ARITH `(a <= b <=> &0 <= b - a)`)]); (EXPAND_TAC "T3"); (ONCE_REWRITE_TAC[SET_RULE `A INTER B DIFF C = A INTER B DIFF A INTER C`]); (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`)); (EXISTS_TAC `dd1 * r pow 2`); (STRIP_TAC); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]); (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b ) * x`]); (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC); (ASM_REAL_ARITH_TAC); (REWRITE_TAC[REAL_LE_POW_2]); (ASM_REAL_ARITH_TAC); (* ======================================================================== *) (* CHECK DEN DAY LA OK ROI - (._o) (0_o) *) (* ==================================================================== *) (REWRITE_WITH `sum T2 (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (\X. f X x)) = sum T2 (\e. cluster_gammaX V e (cell_cluster V e)) - sum T2 (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (beta_bump V x))`); (REWRITE_TAC[REAL_ARITH `a = b - c <=> b = a + c`]); (ABBREV_TAC `f1 = (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (\X. f X x))`); (ABBREV_TAC `f2 = (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (beta_bump V x))`); (REWRITE_WITH `sum T2 (\e. cluster_gammaX V e (cell_cluster V e)) = sum T2 (\e:real^3->bool. f1 e + f2 e)`); (MATCH_MP_TAC SUM_EQ); (EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC); (EXPAND_TAC "f1" THEN EXPAND_TAC "f2" THEN REWRITE_TAC[cluster_gammaX; cell_cluster]); (REWRITE_TAC[FUN_EQ_THM] THEN REPEAT STRIP_TAC); (EXPAND_TAC "f"); (REWRITE_TAC[SET_RULE `{X | x IN critical_edgeX V X /\ mcell_set V X} = {X | mcell_set V X /\ critical_edgeX V X x}`]); (MATCH_MP_TAC SUM_ADD); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `{X | X SUBSET ball (u0,&8) /\ mcell_set V X}`); (STRIP_TAC); (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA_2); (ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[SUBSET]); (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC); (MATCH_MP_TAC MCELL_SUBSET_BALL8_2); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (NEW_GOAL `VX V x' = V INTER x'`); (MATCH_MP_TAC Hdtfnfz.HDTFNFZ); (UNDISCH_TAC `mcell_set V x'` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC); (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`); (ASM_REWRITE_TAC[]); (STRIP_TAC); (UNDISCH_TAC `critical_edgeX V x' x` THEN REWRITE_TAC[critical_edgeX; edgeX; IN; IN_ELIM_THM] THEN STRIP_TAC); (NEW_GOAL `VX V x' u0`); (NEW_GOAL `u0 = u' \/ u0 = v':real^3`); (ASM_SET_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_TAC[ASSUME `u0 = u':real^3`]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[ASSUME `u0 = v':real^3`]); (ASM_REWRITE_TAC[]); (UNDISCH_TAC `VX V x' u0` THEN ASM_REWRITE_TAC[VX]); (REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]); (SET_TAC[]); (NEW_GOAL `VX V x' u0`); (UNDISCH_TAC `mcell_set V x'` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC); (UNDISCH_TAC `critical_edgeX V x' x` THEN REWRITE_TAC[critical_edgeX; edgeX; IN; IN_ELIM_THM] THEN STRIP_TAC); (NEW_GOAL `u0 = u' \/ u0 = v':real^3`); (ASM_SET_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_TAC[ASSUME `u0 = u':real^3`]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[ASSUME `u0 = v':real^3`]); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC SUM_ADD); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC (REAL_ARITH `&0 <= a /\ b + x <= &0 ==> x <= a - b`)); (STRIP_TAC); (MATCH_MP_TAC SUM_POS_LE); (ASM_REWRITE_TAC[]); (EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (UNDISCH_TAC `cell_cluster_estimate V`); (REWRITE_TAC[cell_cluster_estimate]); (REWRITE_TAC[REAL_ARITH `&0 <= a <=> a >= &0`] THEN STRIP_TAC); (ASM_REWRITE_TAC[]); (ABBREV_TAC `f1 = (\x. sum {X | X SUBSET ball (vec 0, r + &8) /\ ~(X SUBSET ball (vec 0, r - &8)) /\ mcell_set V X /\ critical_edgeX V X x} (beta_bump V x))`); (ABBREV_TAC `f2 = (\x. sum {X | X SUBSET ball (vec 0, r - &8) /\ mcell_set V X /\ critical_edgeX V X x} (beta_bump V x))`); (REWRITE_WITH `sum T2 (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (beta_bump V x)) = sum (T2:(real^3->bool)->bool) f1 + sum T2 f2`); (REWRITE_WITH `sum (T2:(real^3->bool)->bool) f1 + sum T2 f2 = sum T2 (\x. f1 x + f2 x)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC SUM_ADD); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC SUM_EQ); (EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC); (EXPAND_TAC "f1" THEN EXPAND_TAC "f2"); (ABBREV_TAC `s1 = {X | X SUBSET ball (vec 0,r + &8) /\ ~(X SUBSET ball (vec 0,r - &8)) /\ mcell_set V X /\ critical_edgeX V X x}`); (ABBREV_TAC `s2 = {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X /\ critical_edgeX V X x}`); (REWRITE_WITH `{X | mcell_set V X /\ critical_edgeX V X x} = s1 UNION s2`); (EXPAND_TAC "s1" THEN EXPAND_TAC "s2" THEN REWRITE_TAC[SET_EQ_LEMMA; IN_UNION; IN_ELIM_THM; IN]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (ASM_CASES_TAC `x' SUBSET ball ((vec 0):real^3,r - &8)`); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[SUBSET; IN_DIFF; IN_BALL]); (REPEAT STRIP_TAC); (NEW_GOAL `x' SUBSET ball (u0:real^3, &8)`); (MATCH_MP_TAC MCELL_SUBSET_BALL8_2); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (NEW_GOAL `x:real^3->bool SUBSET x'`); (MATCH_MP_TAC CRITICAL_EDGEX_SUBSET_MCELL); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (SET_TAC[]); (NEW_GOAL `dist (u0:real^3, x'') < &8`); (REWRITE_TAC[GSYM IN_BALL] THEN ASM_SET_TAC[]); (NEW_GOAL `dist (vec 0, x'') <= dist (u0, x'') + dist (vec 0, u0:real^3)`); (NORM_ARITH_TAC); (NEW_GOAL `dist (vec 0, u0:real^3) < r`); (REWRITE_TAC[GSYM IN_BALL]); (UNDISCH_TAC `(T1:real^3->bool) u0`); (EXPAND_TAC "T1" THEN REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]); (SET_TAC[]); (ASM_REAL_ARITH_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC SUM_UNION); (REPEAT STRIP_TAC); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `{X | X SUBSET ball (vec 0,r + &8) /\ mcell_set V X}`); (STRIP_TAC); (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA_2]); (ASM_SET_TAC[]); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `{X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X}`); (STRIP_TAC); (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA_2]); (ASM_SET_TAC[]); (* ======================================================================== *) (* ======================================================================== *) (EXPAND_TAC "s1" THEN EXPAND_TAC "s2" THEN SET_TAC[]); (REWRITE_WITH `sum (T2:(real^3->bool)->bool) f2 = &0`); (EXPAND_TAC "f2"); (REWRITE_TAC[SET_RULE `!V r x. {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X /\ critical_edgeX V X x} = {X | X IN {X| X SUBSET ball (vec 0,r - &8) /\ mcell_set V X} /\ critical_edgeX V X x}`]); (REWRITE_WITH `sum T2 (\x. sum {X | X IN {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X} /\ critical_edgeX V X x} (beta_bump V x)) = sum T2 (\x. sum {X | X IN {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X} /\ critical_edgeX V X x} (\X. beta_bump V x X))`); (REWRITE_WITH `!x V. (\X. beta_bump V x X) = beta_bump V x`); (REWRITE_TAC[FUN_EQ_THM] THEN ASM_REWRITE_TAC[]); (ABBREV_TAC `t = {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X}`); (ABBREV_TAC `g = beta_bump V`); (ABBREV_TAC `s = T2:(real^3->bool)->bool`); (REWRITE_WITH `sum s (\x. sum {X | X IN t /\ critical_edgeX V X x} (\X. g x X)) = sum t (\X. sum {x | x IN s /\ critical_edgeX V X x} (\x. g x X))`); (MATCH_MP_TAC SUM_SUM_RESTRICT); (STRIP_TAC); (EXPAND_TAC "s" THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "t"); (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA); (ASM_REWRITE_TAC[]); (EXPAND_TAC "s" THEN EXPAND_TAC "t" THEN EXPAND_TAC "g"); (MATCH_MP_TAC SUM_EQ_0); (REWRITE_TAC[IN; IN_ELIM_THM] THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC); (REWRITE_WITH `{x' | T2 x' /\ critical_edgeX V x x'} = {x' | x' IN critical_edgeX V x}`); (MATCH_MP_TAC (SET_RULE `A SUBSET B /\ B SUBSET A ==> A = B`)); (STRIP_TAC); (SET_TAC[]); (ASM_REWRITE_TAC[IN]); (REWRITE_TAC[GSYM (ASSUME `{{u0:real^3, u1} | u0 IN T1 /\ u1 IN T1 /\ ~(u0 = u1) /\ hl [u0; u1] <= hplus} = s`)]); (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; critical_edgeX; edgeX]); (REPEAT STRIP_TAC); (EXISTS_TAC `u':real^3` THEN EXISTS_TAC `v':real^3` THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "T1"); (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`; IN_INTER; IN_BALL]); (NEW_GOAL `VX V x = V INTER x`); (MATCH_MP_TAC Hdtfnfz.HDTFNFZ); (UNDISCH_TAC `mcell_set V x` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]); (STRIP_TAC); (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`); (ASM_REWRITE_TAC[IN]); (STRIP_TAC THEN UNDISCH_TAC `VX V x u'`); (ASM_REWRITE_TAC[VX; MESON[IN] `{} x <=> x IN {}`] THEN SET_TAC[]); (REWRITE_WITH `u':real^3 IN V /\ v' IN V`); (ASM_SET_TAC[]); (REPEAT STRIP_TAC); (NEW_GOAL `u':real^3 IN ball (vec 0, r - &8)`); (ASM_SET_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[IN_BALL] THEN REAL_ARITH_TAC); (NEW_GOAL `v':real^3 IN ball (vec 0, r - &8)`); (ASM_SET_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[IN_BALL] THEN REAL_ARITH_TAC); (REWRITE_WITH `hl [u'; v':real^3] = hl [u; v:real^3]`); (REWRITE_TAC[HL; set_of_list]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (EXISTS_TAC `u:real^3` THEN EXISTS_TAC `v:real^3`); (ASM_REWRITE_TAC[]); (EXISTS_TAC `u':real^3` THEN EXISTS_TAC `v':real^3`); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC SUM_BETA_BUMP_LEMMA); (ASM_REWRITE_TAC[]); (REWRITE_TAC[REAL_ARITH `a + &0 = a`]); (EXPAND_TAC "T2"); (REWRITE_TAC[HL_2; REAL_ARITH `inv (&2) * a <= b <=> a <= &2 * b`]); (REWRITE_WITH `sum {{u0:real^3, u1} | u0 IN T1 /\ u1 IN T1 /\ ~(u0 = u1) /\ dist (u0,u1) <= &2 * hplus} f1 = &1 / &2 * sum {m,n | m IN T1 /\ n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus} (\(m,n). f1 {m, n})`); (REWRITE_TAC[REAL_ARITH `a = &1 / &2 * b <=> b = &2 * a`]); (MATCH_MP_TAC SUM_PAIR_2_SET); (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA); (ASM_REWRITE_TAC[]); (ABBREV_TAC `T3 = V INTER ball ((vec 0):real^3,r) DIFF ball (vec 0, r - &16)`); (REWRITE_WITH `sum {m:real^3,n | m IN T1 /\ n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus} (\(m,n). f1 {m, n}) = sum {m,n | m IN T3 /\ n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus} (\(m,n). f1 {m, n})`); (MATCH_MP_TAC SUM_SUPERSET); (STRIP_TAC); (EXPAND_TAC "T1" THEN EXPAND_TAC "T3" THEN REWRITE_TAC[SUBSET; IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `m:real^3` THEN EXISTS_TAC `n:real^3` THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "T1" THEN UNDISCH_TAC `(V INTER ball ((vec 0):real^3,r) DIFF ball (vec 0,r - &16)) m` THEN REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]); (SET_TAC[]); (EXPAND_TAC "T1" THEN EXPAND_TAC "T3" THEN REWRITE_TAC[IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (EXPAND_TAC "f1"); (REWRITE_WITH `{X | X SUBSET ball (vec 0,r + &8) /\ ~(X SUBSET ball (vec 0,r - &8)) /\ mcell_set V X /\ critical_edgeX V X {m, n}} = {}`); (REWRITE_TAC[SET_RULE `y = {} <=> ~(?x. x IN y)`]); (REPEAT STRIP_TAC); (UNDISCH_TAC `~(?m n. ((V INTER ball (vec 0,r) DIFF ball (vec 0,r - &16)) m /\ (V INTER ball (vec 0,r)) n /\ ~(m = n) /\ dist (m:real^3,n) <= &2 * hplus) /\ x = m,n) ` THEN REWRITE_TAC[]); (EXISTS_TAC `m:real^3` THEN EXISTS_TAC `n:real^3`); (ASM_REWRITE_TAC[]); (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]); (EXPAND_TAC "T3" THEN REWRITE_TAC[IN_DIFF; IN; IN_BALL]); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (NEW_GOAL `?p:real^3. p IN x' /\ ~(p IN ball (vec 0,r - &8))`); (UNDISCH_TAC `~(x' SUBSET ball ((vec 0):real^3,r - &8))`); (SET_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (UP_ASM_TAC THEN REWRITE_TAC[IN_BALL]); (NEW_GOAL `x' SUBSET ball (p:real^3, &8)`); (MATCH_MP_TAC MCELL_SUBSET_BALL8_2); (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]); (NEW_GOAL `m:real^3 IN x'`); (UNDISCH_TAC `critical_edgeX V x' {m, n}` THEN REWRITE_TAC[critical_edgeX; edgeX; IN_ELIM_THM; IN]); (REPEAT STRIP_TAC); (NEW_GOAL `VX V x' = V INTER x'`); (MATCH_MP_TAC Hdtfnfz.HDTFNFZ); (UNDISCH_TAC `mcell_set V x'` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]); (STRIP_TAC); (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`); (ASM_REWRITE_TAC[IN]); (STRIP_TAC THEN UNDISCH_TAC `VX V x' u'`); (ASM_REWRITE_TAC[VX; MESON[IN] `{} x <=> x IN {}`] THEN SET_TAC[]); (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]); (ASM_SET_TAC[]); (NEW_GOAL `dist (p, m:real^3) < &8`); (REWRITE_TAC[GSYM IN_BALL]); (ASM_SET_TAC[]); (NEW_GOAL `dist (vec 0, p) <= dist (vec 0, m:real^3) + dist (p, m)`); (NORM_ARITH_TAC); (ASM_REAL_ARITH_TAC); (REWRITE_TAC[SUM_CLAUSES]); (ABBREV_TAC `g = (\m:real^3. {n | n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus})`); (REWRITE_WITH `{m,n | m IN T3 /\ n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus} = {m,n:real^3 | m IN T3 /\ n IN g m}`); (EXPAND_TAC "g" THEN ASM_REWRITE_TAC[] THEN SET_TAC[]); (ABBREV_TAC `h = (\m. (\n. (f1:(real^3->bool)->real) {m, n}))`); (REWRITE_WITH `(\(m,n). (f1:(real^3->bool)->real) {m, n}) = (\(m,n). h m n)`); (REWRITE_TAC[FUN_EQ_THM]); (STRIP_TAC THEN ASM_REWRITE_TAC[]); (NEW_GOAL `x:real^3#real^3 = FST x, SND x`); (REWRITE_TAC[PAIR]); (ONCE_ASM_REWRITE_TAC[]); (EXPAND_TAC "h" THEN REWRITE_TAC[]); (REWRITE_WITH `sum {m,n | m IN T3 /\ n IN g m} (\(m,n). h m n) = sum T3 (\m. sum (g m) ((h:real^3->real^3->real) m))`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC SUM_SUM_PRODUCT); (STRIP_TAC); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `V:real^3->bool INTER ball (vec 0,r)`); (STRIP_TAC); (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "T3" THEN SET_TAC[]); (REPEAT STRIP_TAC); (EXPAND_TAC "g" THEN REWRITE_TAC[]); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `V:real^3->bool INTER ball (vec 0,r)`); (STRIP_TAC); (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "T1" THEN SET_TAC[]); (NEW_GOAL `sum T3 (\m. sum ((g:real^3->real^3->bool) m) (h m)) <= sum T3 (\n:real^3. ss1)`); (MATCH_MP_TAC SUM_LE); (STRIP_TAC); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `V:real^3->bool INTER ball (vec 0,r)`); (STRIP_TAC); (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "T3" THEN SET_TAC[]); (REPEAT STRIP_TAC THEN REWRITE_TAC[]); (NEW_GOAL `sum ((g:real^3->real^3->bool) x) (h x) <= sum (g x) (\x. cc4 * cc3)`); (MATCH_MP_TAC SUM_LE); (STRIP_TAC); (EXPAND_TAC "g" THEN REWRITE_TAC[]); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `V:real^3->bool INTER ball (vec 0,r)`); (STRIP_TAC); (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "T1" THEN SET_TAC[]); (REPEAT STRIP_TAC THEN EXPAND_TAC "h" THEN REWRITE_TAC[]); (EXPAND_TAC "f1"); (ABBREV_TAC `S1 = {X | X SUBSET ball (vec 0,r + &8) /\ ~(X SUBSET ball (vec 0,r - &8)) /\ mcell_set V X /\ critical_edgeX V X {x, x'}}`); (NEW_GOAL `sum (S1:(real^3->bool)->bool) (beta_bump V {x, x'}) <= sum S1 (\x. cc3)`); (MATCH_MP_TAC SUM_LE); (STRIP_TAC); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `{X | X SUBSET ball (vec 0,r + &8) /\ mcell_set V X}`); (STRIP_TAC); (REPEAT STRIP_TAC THEN REWRITE_TAC[]); (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA); (ASM_REWRITE_TAC[]); (EXPAND_TAC "S1" THEN SET_TAC[]); (REPEAT STRIP_TAC); (REWRITE_TAC[]); (FIRST_ASSUM MATCH_MP_TAC); (UP_ASM_TAC THEN EXPAND_TAC "S1" THEN REWRITE_TAC[IN; IN_ELIM_THM]); (STRIP_TAC THEN ASM_REWRITE_TAC[]); (NEW_GOAL `sum S1 (\x:real^3->bool. cc3) = &(CARD S1) * cc3`); (MATCH_MP_TAC SUM_CONST); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `{X | X SUBSET ball (vec 0,r + &8) /\ mcell_set V X}`); (STRIP_TAC); (REPEAT STRIP_TAC THEN REWRITE_TAC[]); (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA); (ASM_REWRITE_TAC[]); (EXPAND_TAC "S1" THEN SET_TAC[]); (NEW_GOAL `&(CARD (S1:(real^3->bool)->bool)) <= cc4`); (NEW_GOAL `&(CARD (S1:(real^3->bool)->bool)) <= &(CARD {X | mcell_set V X /\ VX V X x})`); (REWRITE_TAC[REAL_OF_NUM_LE]); (MATCH_MP_TAC CARD_SUBSET); (STRIP_TAC); (EXPAND_TAC "S1" THEN REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; critical_edgeX; edgeX] THEN REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `x:real^3 = u' \/ x = v'`); (ASM_SET_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `{X | X SUBSET ball (x:real^3, &8) /\ mcell_set V X}`); (STRIP_TAC); (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA_2); (ASM_REWRITE_TAC[]); (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC); (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]); (NEW_GOAL `VX V x'' = V INTER x''`); (MATCH_MP_TAC Hdtfnfz.HDTFNFZ); (UNDISCH_TAC `mcell_set V x''` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]); (STRIP_TAC); (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`); (ASM_REWRITE_TAC[IN]); (STRIP_TAC THEN UNDISCH_TAC `VX V x'' x`); (ASM_REWRITE_TAC[VX; MESON[IN] `{} x <=> x IN {}`] THEN SET_TAC[]); (NEW_GOAL `x'' SUBSET ball (x:real^3, &8)`); (MATCH_MP_TAC MCELL_SUBSET_BALL8_2); (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]); (ASM_SET_TAC[]); (ASM_SET_TAC[]); (ASM_REWRITE_TAC[]); (NEW_GOAL `&(CARD {X | mcell_set V X /\ VX V X x}) <= cc4`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (UNDISCH_TAC `x IN (T3:real^3->bool)` THEN EXPAND_TAC "T3"); (SET_TAC[]); (ABBREV_TAC `s_temp = &(CARD {X | mcell_set V X /\ VX V X x})`); (ASM_REAL_ARITH_TAC); (NEW_GOAL `sum (S1:(real^3->bool)->bool) (\x. cc3) <= cc4 * cc3`); (ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`]); (ONCE_REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]); (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (ABBREV_TAC `s_temp = sum (S1:(real^3->bool)->bool) (\x. cc3)`); (ASM_REAL_ARITH_TAC); (NEW_GOAL `sum ((g:real^3->real^3->bool) x) (\x. cc4 * cc3) <= ss1`); (REWRITE_WITH `sum ((g:real^3->real^3->bool) x) (\x. cc4 * cc3) = &(CARD (g x)) * cc4 * cc3`); (MATCH_MP_TAC SUM_CONST); (EXPAND_TAC "g"); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `T1:real^3->bool`); (STRIP_TAC); (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA); (ASM_REWRITE_TAC[]); (SET_TAC[]); (NEW_GOAL `&(CARD ((g:real^3->real^3->bool) x)) <= &(CARD (V INTER ball (x:real^3, &3)))`); (REWRITE_TAC[REAL_OF_NUM_LE]); (MATCH_MP_TAC CARD_SUBSET); (STRIP_TAC); (EXPAND_TAC "g" THEN EXPAND_TAC "T1" THEN REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; IN_INTER; IN_BALL]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `&2 * hplus < &3`); (REWRITE_TAC[hplus] THEN REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (ASM_SIMP_TAC[FINITE_PACK_LEMMA]); (EXPAND_TAC "ss1"); (ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`]); (ONCE_REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]); (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC); (ONCE_REWRITE_TAC[GSYM (REAL_ARITH `a <= b <=> &0 <= b - a`)]); (NEW_GOAL `&(CARD (V INTER ball (x:real^3,&3))) <= &4 pow 3`); (REWRITE_TAC[REAL_ARITH `&4 = &3 + &1`]); (MATCH_MP_TAC BOUNDS_VGEN_klemma); (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (MATCH_MP_TAC REAL_LE_MUL); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (EXPAND_TAC "g"); (REWRITE_TAC[REAL_ARITH `&1 / &2 * x + a <= &0 <=> x <= &2 * (-- a)`]); (REWRITE_TAC[REAL_ARITH `c * r pow 2 + d * r pow 2 = (c + d) * r pow 2`]); (REWRITE_WITH `(c:real) + dd = -- ss`); (EXPAND_TAC "c"); (REAL_ARITH_TAC); (REWRITE_TAC[REAL_ARITH `&2 * --(--ss * r pow 2) = &2 * ss * r pow 2`]); (NEW_GOAL `sum T3 (\n:real^3. ss1) <= &2 * ss * r pow 2`); (REWRITE_WITH `sum T3 (\n:real^3. ss1) = &(CARD (T3)) * ss1`); (MATCH_MP_TAC SUM_CONST); (MATCH_MP_TAC FINITE_SUBSET); (EXISTS_TAC `(V:real^3->bool) INTER ball (vec 0,r)`); (STRIP_TAC); (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "T3" THEN SET_TAC[]); (EXPAND_TAC "ss"); (REWRITE_TAC[REAL_ARITH `&2 * (&1 / &2 * dd4 * ss1) * r pow 2 = (dd4 * r pow 2) * ss1`]); (ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`]); (ONCE_REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]); (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC); (ONCE_REWRITE_TAC[GSYM (REAL_ARITH `a <= b <=> &0 <= b - a`)]); (EXPAND_TAC "T3"); (ONCE_REWRITE_TAC[SET_RULE `A INTER B DIFF C = A INTER B DIFF A INTER C`]); (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`)); (EXISTS_TAC `dd3 * r pow 2`); (STRIP_TAC); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]); (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b ) * x`]); (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC); (ASM_REAL_ARITH_TAC); (REWRITE_TAC[REAL_LE_POW_2]); (EXPAND_TAC "ss1"); (MATCH_MP_TAC REAL_LE_MUL); (STRIP_TAC); (ASM_REAL_ARITH_TAC); (MATCH_MP_TAC REAL_LE_MUL); (ASM_REAL_ARITH_TAC); (REWRITE_WITH `sum T3 (\m:real^3. sum {n | n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus} (h m)) = sum T3 (\m. sum (g m) (h m))`); (EXPAND_TAC "g" THEN REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (EXISTS_TAC `&0`); (REPEAT STRIP_TAC); (NEW_GOAL `F`); (UNDISCH_TAC `~(saturated V /\ packing V)` THEN ASM_REWRITE_TAC[]); (ASM_MESON_TAC[])]);;