text_formalization/packing/sum_gammaX_lmfun_estimate.hl

   1 (* ========================================================================= *)
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   3 (*                                                                           *)
   4 (*      Authour   : VU KHAC KY                                               *)
   5 (*      Book lemma: UPFZBZM                                                  *)
   6 (*      SUM_GAMMAX_LMFUN_ESTIMATE - a supported lemma.                       *)
   7 (*      Chaper    : Packing (Clusters)                                       *)
   8 (*                                                                           *)
   9 (* ========================================================================= *)
  10
  11 module Sum_gammax_lmfun_estimate = struct
  12
  13 open Sphere;;
  14 open Euler_main_theorem;;
  15 open Pack_defs;;
  16 open Pack_concl;;
  17 open Pack1;;
  18 open Pack2;;
  19 open Packing3;;
  20 open Rogers;;
  21 open Vukhacky_tactics;;
  22 open Marchal_cells;;
  23 open Emnwuus;;
  24 (* open Marchal_cells_2;; *)
  25 open Marchal_cells_2_new;;
  26 open Urrphbz1;;
  27 open Lepjbdj;;
  28 open Hdtfnfz;;
  29 open Rvfxzbu;;
  30 open Sltstlo;;
  31 open Urrphbz2;;
  32 open Urrphbz3;;
  33 open Ynhyjit;;
  34 open Njiutiu;;
  35 open Tezffsk;;
  36 open Qzksykg;;
  37 open Ddzuphj;;
  38 open Ajripqn;;
  39 open Qzyzmjc;;
  40 open Upfzbzm_support_lemmas;;
  41 open Marchal_cells_3;;
  42 open Grutoti;;
  43
  44 let TSKAJXY_statement = new_definition
  45    `TSKAJXY_statement <=>
  46       (!V X.
  47           saturated V /\
  48           packing V /\
  49           mcell_set V X /\
  50           critical_edgeX V X = {}
  51           ==> gammaX V X lmfun >= &0)`;;
  52
  53 let SUM_GAMMAX_LMFUN_ESTIMATE_concl =
  54   `!V. ?c. !r. saturated V /\ packing V /\ &1 <= r /\
  55                cell_cluster_estimate_v1 V /\ TSKAJXY_statement ==>
  56     c * r pow 2 <=  sum {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X}
  57     (\X. gammaX V X lmfun)`;;
  58
  59 (* ========================================================================= *)
  60 (* ========================================================================= *)
  61
  62 let SUM_GAMMAX_LMFUN_ESTIMATE = prove_by_refinement (
  63     SUM_GAMMAX_LMFUN_ESTIMATE_concl,
  64
  65 [(GEN_TAC);
  66
  67 (* ================== Choose the constants ================================= *)
  68
  69  (NEW_GOAL `?cc1. (&1 <= cc1) /\ (!V X.
  70              packing V /\ saturated V /\ mcell_set V X
  71              ==> gammaX V X lmfun <= cc1)`);
  72  (MP_TAC BOUND_GAMMA_X_lmfun THEN STRIP_TAC);
  73  (EXISTS_TAC `max (c:real) (&1)`);
  74  (STRIP_TAC);
  75  (REAL_ARITH_TAC);
  76  (REPEAT STRIP_TAC);
  77  (NEW_GOAL `gammaX V X lmfun <= c`);
  78  (ASM_MESON_TAC[]);
  79  (ASM_REAL_ARITH_TAC);
  80  (UP_ASM_TAC THEN STRIP_TAC);
  81
  82  (NEW_GOAL `?cc2. (&1 <= cc2) /\
  83             (!V u0.
  84              saturated V /\ packing V /\ u0 IN V
  85              ==> & (CARD {X | mcell_set V X /\ VX V X u0}) <= cc2)`);
  86
  87  (MP_TAC CARD_MCELL_CONTAINS_POINT_klemma);
  88  (STRIP_TAC);
  89  (EXISTS_TAC `max (&c:real) (&1)`);
  90  (STRIP_TAC);
  91  (REAL_ARITH_TAC);
  92  (REPEAT STRIP_TAC);
  93  (NEW_GOAL `&(CARD {X | mcell_set V X /\ VX V X u0}) <= (&c:real)`);
  94  (REWRITE_TAC[REAL_OF_NUM_LE]);
  95  (ASM_MESON_TAC[]);
  96  (ABBREV_TAC `s = &(CARD {X | mcell_set V X /\ VX V X u0})`);
  97  (ASM_REAL_ARITH_TAC);
  98  (UP_ASM_TAC THEN STRIP_TAC);
  99
 100  (NEW_GOAL
 101  `?cc3. &1 <= cc3 /\
 102        (!V X e.
 103             saturated V /\ packing V /\ mcell_set V X /\ critical_edgeX V X e
 104             ==> beta_bump_v1 V e X <= cc3)`);
 105  (MP_TAC Bump.BOUND_BETA_BUMP THEN STRIP_TAC);
 106  (EXISTS_TAC `max (c:real) (&1)`);
 107  (STRIP_TAC);
 108  (REAL_ARITH_TAC);
 109  (REPEAT STRIP_TAC);
 110  (NEW_GOAL `beta_bump_v1 V e X <= c`);
 111  (ASM_MESON_TAC[]);
 112  (ASM_REAL_ARITH_TAC);
 113  (UP_ASM_TAC THEN STRIP_TAC);
 114
 115  (NEW_GOAL
 116  `?cc4. &1 <= cc4 /\
 117        (!V u0.
 118            saturated V /\ packing V /\ u0 IN V
 119             ==> &(CARD {X | mcell_set V X /\ VX V X u0}) <= cc4)`);
 120  (MP_TAC CARD_MCELL_CONTAINS_POINT_klemma THEN STRIP_TAC);
 121  (EXISTS_TAC `max (&c) (&1)`);
 122  (STRIP_TAC);
 123  (REAL_ARITH_TAC);
 124  (REPEAT STRIP_TAC);
 125  (NEW_GOAL `&(CARD {X | mcell_set V X /\ VX V X u0}) <= &c`);
 126  (REWRITE_TAC[REAL_OF_NUM_LE]);
 127  (ASM_MESON_TAC[]);
 128  (ABBREV_TAC `s = &(CARD {X | mcell_set V X /\ VX V X u0})`);
 129  (ASM_REAL_ARITH_TAC);
 130  (UP_ASM_TAC THEN STRIP_TAC);
 131
 132  (ASM_CASES_TAC `saturated V /\ packing V`);
 133
 134  (NEW_GOAL
 135   `?dd1. !r. &1 <= r ==>
 136    &(CARD (V INTER ball ((vec 0):real^3,r) DIFF V INTER ball (vec 0,r - &8))) <=
 137     dd1 * r pow 2`);
 138
 139  (REWRITE_WITH `!r p. V INTER ball (p:real^3,r) DIFF V INTER ball (p,r - &8)
 140     = V INTER ball (p:real^3,r + &0) DIFF V INTER ball (p,r - &8)`);
 141  (ASM_REWRITE_TAC[REAL_ARITH `a + &0 = a`]);
 142  (ASM_SIMP_TAC[PACKING_BALL_BOUNDARY]);
 143  (TAKE_TAC);
 144
 145  (ABBREV_TAC `dd2 = max dd1 (&1)`);
 146  (ABBREV_TAC `dd = &1 / &2 * dd2 * (&4) pow 3 * cc2 * cc1`);
 147
 148  (NEW_GOAL
 149   `?dd3. !r. &1 <= r ==>
 150   &(CARD (V INTER ball ((vec 0):real^3,r) DIFF V INTER ball (vec 0,r - &16))) <=
 151    dd3 * r pow 2`);
 152
 153  (REWRITE_WITH `!r p. V INTER ball (p:real^3,r) DIFF V INTER ball (p,r - &16)
 154     = V INTER ball (p:real^3,r + &0) DIFF V INTER ball (p,r - &16)`);
 155  (ASM_REWRITE_TAC[REAL_ARITH `a + &0 = a`]);
 156  (ASM_SIMP_TAC[PACKING_BALL_BOUNDARY]);
 157  (TAKE_TAC);
 158
 159  (ABBREV_TAC `dd4 = max dd3 (&1)`);
 160  (ABBREV_TAC `ss1 = (&4) pow 3 * cc4 * cc3`);
 161  (ABBREV_TAC `ss = &1 / &2 * dd4 * ss1`);
 162
 163  (ABBREV_TAC `c:real = -- (dd + ss)`);
 164  (EXISTS_TAC `c:real`);
 165
 166
 167 (* ============================================================================ *)
 168
 169  (REPEAT STRIP_TAC);
 170  (NEW_GOAL `!X. mcell_set V X /\ critical_edgeX V X  = {} ==>
 171                  gammaX V X lmfun >= &0`);
 172  (UP_ASM_TAC THEN REWRITE_TAC[TSKAJXY_statement]);
 173  (STRIP_TAC);
 174  (ASM_SIMP_TAC[]);
 175
 176  (ABBREV_TAC `B = {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X}`);
 177  (ABBREV_TAC `B0 = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\
 178                          critical_edgeX V X = {}}`);
 179  (ABBREV_TAC `B1 = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\
 180                          ~(critical_edgeX V X = {})}`);
 181  (NEW_GOAL `FINITE (B1:(real^3->bool)->bool)`);
 182  (EXPAND_TAC "B1");
 183  (MATCH_MP_TAC FINITE_SUBSET);
 184  (EXISTS_TAC `{X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);
 185  (STRIP_TAC);
 186  (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);
 187  (SET_TAC[]);
 188
 189  (REWRITE_WITH `B = B0 UNION B1:(real^3->bool)->bool`);
 190  (EXPAND_TAC "B" THEN EXPAND_TAC "B1" THEN EXPAND_TAC "B0");
 191  (SET_TAC[]);
 192  (REWRITE_WITH `sum (B0 UNION B1) (\X. gammaX V X lmfun) =
 193    sum B0 (\X. gammaX V X lmfun) + sum B1 (\X. gammaX V X lmfun)`);
 194  (MATCH_MP_TAC SUM_UNION);
 195  (REPEAT STRIP_TAC);
 196  (EXPAND_TAC "B0");
 197  (MATCH_MP_TAC FINITE_SUBSET);
 198  (EXISTS_TAC `{X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);
 199  (STRIP_TAC);
 200  (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);
 201  (SET_TAC[]);
 202  (ASM_REWRITE_TAC[]);
 203  (EXPAND_TAC "B1" THEN EXPAND_TAC "B0");
 204  (SET_TAC[]);
 205  (MATCH_MP_TAC (REAL_ARITH `&0 <= b /\ a <= c ==> a <= b + c`));
 206  (STRIP_TAC);
 207  (MATCH_MP_TAC SUM_POS_LE);
 208  (STRIP_TAC);
 209  (EXPAND_TAC "B0");
 210  (MATCH_MP_TAC FINITE_SUBSET);
 211  (EXISTS_TAC `{X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);
 212  (STRIP_TAC);
 213  (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);
 214  (SET_TAC[]);
 215  (REWRITE_TAC[BETA_THM; REAL_ARITH `&0 <= a <=> a >= &0`]);
 216  (EXPAND_TAC "B0" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 217  (REPEAT STRIP_TAC);
 218  (ASM_SIMP_TAC[]);
 219
 220  (REWRITE_WITH
 221   `sum B1 (\X. gammaX V X lmfun) =
 222    sum B1 (\X. (gammaX V X lmfun) *
 223                 sum (critical_edgeX V X) (\e. critical_weight V X))`);
 224  (MATCH_MP_TAC SUM_EQ);
 225  (EXPAND_TAC "B1" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 226  (REPEAT STRIP_TAC);
 227  (REWRITE_TAC[critical_weight]);
 228  (REWRITE_WITH
 229   `sum (critical_edgeX V x) (\e. &1 / &(CARD (critical_edgeX V x))) =
 230    &(CARD (critical_edgeX V x)) * (&1 / &(CARD (critical_edgeX V x)))`);
 231  (MATCH_MP_TAC SUM_CONST);
 232  (REWRITE_TAC[FINITE_critical_edgeX]);
 233  (REWRITE_TAC[REAL_ARITH `a * &1 / a = a / a`]);
 234  (REWRITE_WITH `&(CARD (critical_edgeX V x)) / &(CARD (critical_edgeX V x)) = &1`);
 235  (MATCH_MP_TAC REAL_DIV_REFL);
 236  (REWRITE_TAC[REAL_OF_NUM_EQ]);
 237  (REWRITE_WITH `CARD (critical_edgeX V x) = 0 <=> critical_edgeX V x = {}`);
 238  (MATCH_MP_TAC CARD_EQ_0);
 239  (REWRITE_TAC[FINITE_critical_edgeX]);
 240  (ASM_REWRITE_TAC[]);
 241  (REAL_ARITH_TAC);
 242
 243 (* ------------------------------------------------------------------------- *)
 244 (* Hint:      - See proofs of KIZHLTL1; KIZHLTL2 to adapt                    *)
 245 (* ------------------------------------------------------------------------- *)
 246
 247  (REWRITE_TAC[GSYM SUM_LMUL]);
 248
 249  (ABBREV_TAC `T1:real^3->bool = V INTER ball (vec 0, r)`);
 250  (ABBREV_TAC `T2 = {{u0, u1:real^3} | u0 IN T1 /\ u1 IN T1 /\ ~(u0 = u1) /\
 251                                        hl [u0; u1] <= hplus}`);
 252  (NEW_GOAL `FINITE (T2:(real^3->bool)->bool)`);
 253  (EXPAND_TAC "T2" THEN MATCH_MP_TAC FINITE_SUBSET);
 254  (EXISTS_TAC `{{u0, u1:real^3} | u0 IN T1 /\ u1 IN T1}`);
 255  (STRIP_TAC);
 256  (MATCH_MP_TAC FINITE_SET_PRODUCT_KY_LEMMA);
 257  (EXPAND_TAC "T1" THEN MATCH_MP_TAC Pack2.KIUMVTC);
 258  (ASM_REWRITE_TAC[]);
 259  (SET_TAC[]);
 260
 261  (REWRITE_WITH
 262  `sum B1 (\X. sum (critical_edgeX V X)
 263                    (\x. gammaX V X lmfun * critical_weight V X)) =
 264   sum B1 (\X. sum {y:real^3->bool| y IN T2 /\ critical_edgeX V X y}
 265                    (\x. gammaX V X lmfun * critical_weight V X))`);
 266  (MATCH_MP_TAC SUM_EQ);
 267  (EXPAND_TAC "B1" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 268  (REPEAT STRIP_TAC);
 269  (AP_THM_TAC THEN AP_TERM_TAC);
 270  (REWRITE_TAC[SET_RULE `a = b <=> b SUBSET a /\ a SUBSET b`]);
 271  (STRIP_TAC);
 272  (SET_TAC[]);
 273  (REWRITE_TAC[SET_RULE `A SUBSET {y | T2 y /\ A y} <=> A SUBSET T2`]);
 274  (EXPAND_TAC "T2" THEN REWRITE_TAC[SUBSET; critical_edgeX; IN; IN_ELIM_THM; edgeX]);
 275  (REPEAT STRIP_TAC);
 276  (EXPAND_TAC "T1" THEN REWRITE_TAC[IN_ELIM_THM]);
 277  (EXISTS_TAC `u':real^3` THEN EXISTS_TAC `v':real^3`);
 278  (REWRITE_TAC[ASSUME `~(u' = v':real^3)`]);
 279
 280  (REWRITE_TAC[ASSUME `x' = {u, v:real^3}`; MESON[IN] `V (x:real^3) <=> x IN V`;
 281                GSYM (ASSUME `{u, v} = {u', v':real^3}`); IN_INTER]);
 282
 283  (NEW_GOAL `VX V x = V INTER x`);
 284  (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
 285  (UNDISCH_TAC `mcell_set V x` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]);
 286  (STRIP_TAC);
 287  (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 288  (ASM_REWRITE_TAC[]);
 289  (STRIP_TAC);
 290  (NEW_GOAL `VX V x = {}`);
 291  (REWRITE_TAC[VX]);
 292  (ASM_REWRITE_TAC[]);
 293  (UNDISCH_TAC `VX V x u'` THEN ASM_REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]);
 294  (SET_TAC[]);
 295
 296  (STRIP_TAC);
 297  (ASM_SET_TAC[]);
 298  (STRIP_TAC);
 299  (ASM_SET_TAC[]);
 300  (REWRITE_WITH `hl [u'; v':real^3] = hl [u; v:real^3]`);
 301  (ASM_REWRITE_TAC[HL; set_of_list]);
 302  (ASM_REWRITE_TAC[]);
 303
 304  (ABBREV_TAC `f = (\X. (\x:real^3->bool.
 305                             gammaX V X lmfun * critical_weight V X))`);
 306  (REWRITE_WITH
 307  `sum B1 (\X. sum {y | y IN T2 /\ critical_edgeX V X y}
 308                   (\x:real^3->bool. gammaX V X lmfun * critical_weight V X)) =
 309   sum B1 (\X. sum {y | y IN T2 /\ critical_edgeX V X y}
 310                   (\x:real^3->bool. f X x))`);
 311  (EXPAND_TAC "f" THEN REFL_TAC);
 312  (REWRITE_WITH
 313   `sum B1 (\X. sum {y | y IN T2 /\ critical_edgeX V X y} (\x. f X x)) =
 314    sum T2 (\x. sum {X | X IN B1 /\ critical_edgeX V X x} (\X. f X x))`);
 315  (ASM_SIMP_TAC[SUM_SUM_RESTRICT]);
 316
 317  (EXPAND_TAC "B1" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 318  (REWRITE_TAC[MESON[] `(A/\B/\C)/\D <=> A/\B/\C/\D`]);
 319  (REWRITE_WITH
 320 `sum T2 (\x. sum
 321                {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\
 322                    ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
 323         (\X. f X x)) =
 324  sum T2  (\x. sum {X | mcell_set V X /\
 325                      ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
 326       (\X. f X x)) -
 327 sum T2  (\x. sum {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
 328                       ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
 329       (\X. f X x))`);
 330  (REWRITE_TAC[REAL_ARITH `a = b - c <=> b = a + c`]);
 331  (REWRITE_WITH
 332 ` sum T2
 333  (\x. sum
 334       {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\
 335            ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
 336       (\X. f X x)) +
 337  sum T2
 338  (\x. sum
 339       {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
 340            ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
 341       (\X. f X x)) =
 342  sum T2
 343  (\x. (\x. sum
 344       {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\
 345            ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
 346       (\X. f X x)) x +
 347 (\x. sum
 348       {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
 349            ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
 350       (\X. f X x)) x)`);
 351  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 352  (MATCH_MP_TAC SUM_ADD);
 353  (ASM_REWRITE_TAC[]);
 354  (MATCH_MP_TAC SUM_EQ);
 355  (REWRITE_TAC[BETA_THM] THEN REPEAT STRIP_TAC);
 356
 357  (REWRITE_WITH
 358 `sum
 359  {X | X SUBSET ball (vec 0,r) /\
 360       mcell_set V X /\
 361       ~(critical_edgeX V X = {}) /\
 362       critical_edgeX V X x}
 363  (\X. f X x) +
 364  sum
 365  {X | ~(X SUBSET ball (vec 0,r)) /\
 366       mcell_set V X /\
 367       ~(critical_edgeX V X = {}) /\
 368       critical_edgeX V X x}
 369  (\X. f X x) =
 370  sum ({X | X SUBSET ball (vec 0,r) /\
 371       mcell_set V X /\
 372       ~(critical_edgeX V X = {}) /\
 373       critical_edgeX V X x} UNION
 374       {X | ~(X SUBSET ball (vec 0,r)) /\
 375       mcell_set V X /\
 376       ~(critical_edgeX V X = {}) /\
 377       critical_edgeX V X x})
 378  (\X. f X x)`);
 379  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 380  (MATCH_MP_TAC SUM_UNION);
 381  (REPEAT STRIP_TAC);
 382
 383  (MATCH_MP_TAC FINITE_SUBSET);
 384  (EXISTS_TAC `B1:(real^3->bool)->bool`);
 385  (ASM_REWRITE_TAC[]);
 386  (EXPAND_TAC "B1" THEN SET_TAC[]);
 387
 388  (UP_ASM_TAC THEN EXPAND_TAC "T2");
 389  (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 390  (MATCH_MP_TAC FINITE_SUBSET);
 391  (EXISTS_TAC `{X | X SUBSET ball (vec 0,r + &8) /\ mcell_set V X}`);
 392  (STRIP_TAC);
 393  (ASM_SIMP_TAC[Marchal_cells_3.FINITE_MCELL_SET_LEMMA]);
 394  (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM]);
 395  (REPEAT STRIP_TAC);
 396  (NEW_GOAL `x SUBSET VX V x'`);
 397  (UNDISCH_TAC `critical_edgeX V x' x` THEN REWRITE_TAC[critical_edgeX;edgeX]);
 398  (REWRITE_TAC[IN_ELIM_THM]);
 399  (REPEAT STRIP_TAC);
 400  (REWRITE_TAC[ASSUME `x = {u, v:real^3}`; ASSUME `{u, v:real^3} = {u', v'}`]);
 401  (SET_TAC[ASSUME `VX V x' u'`; ASSUME `VX V x' v'`]);
 402  (NEW_GOAL `VX V x' = V INTER x'`);
 403  (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
 404  (UNDISCH_TAC `mcell_set V x'` THEN REWRITE_TAC[mcell_set; IN_ELIM_THM; IN]);
 405  (REPEAT STRIP_TAC);
 406  (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 407  (ASM_REWRITE_TAC[]);
 408  (STRIP_TAC);
 409  (NEW_GOAL `VX V x' = {}`);
 410  (ASM_REWRITE_TAC[VX]);
 411  (UNDISCH_TAC `x SUBSET VX V x'` THEN REWRITE_TAC[ASSUME `VX V x' = {}`]);
 412  (REWRITE_TAC[ASSUME `x = {u0, u1:real^3}`] THEN SET_TAC[]);
 413  (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`; IN_BALL]);
 414  (NEW_GOAL `dist (vec 0, x'') <= dist (vec 0, u0:real^3) + dist (u0, x'')`);
 415  (NORM_ARITH_TAC);
 416  (NEW_GOAL `dist (vec 0, u0:real^3) < r`);
 417  (REWRITE_TAC[GSYM IN_BALL]);
 418  (UNDISCH_TAC `(T1:real^3->bool) u0` THEN EXPAND_TAC "T1");
 419  (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`] THEN SET_TAC[]);
 420  (NEW_GOAL `dist (u0, x'':real^3) < &8`);
 421  (REWRITE_TAC[GSYM IN_BALL]);
 422  (NEW_GOAL `x' SUBSET ball (u0:real^3,&8)`);
 423  (UNDISCH_TAC `mcell_set V x'` THEN REWRITE_TAC[mcell_set; IN_ELIM_THM; IN]);
 424  (REPEAT STRIP_TAC);
 425  (ASM_REWRITE_TAC[]);
 426  (MATCH_MP_TAC MCELL_SUBSET_BALL8);
 427  (ASM_REWRITE_TAC[]);
 428  (REWRITE_TAC[GSYM (ASSUME `x' = mcell i V ul`)]);
 429  (UNDISCH_TAC `x SUBSET VX V x'` THEN UNDISCH_TAC `VX V x' = V INTER x'`);
 430  (ASM_REWRITE_TAC[]);
 431  (SET_TAC[]);
 432  (SUBGOAL_THEN `(x'':real^3) IN x'` MP_TAC);
 433  (UNDISCH_TAC `(x':real^3->bool) x''` THEN SET_TAC[]);
 434  (UP_ASM_TAC THEN SET_TAC[]);
 435  (ASM_REAL_ARITH_TAC);
 436  (ASM_REWRITE_TAC[]);
 437  (SET_TAC[]);
 438
 439  (REWRITE_WITH ` ({X | X SUBSET ball (vec 0,r) /\
 440        mcell_set V X /\
 441        ~(critical_edgeX V X = {}) /\
 442        critical_edgeX V X x} UNION
 443   {X | ~(X SUBSET ball (vec 0,r)) /\
 444        mcell_set V X /\
 445        ~(critical_edgeX V X = {}) /\
 446        critical_edgeX V X x}) =
 447  {X | mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}`);
 448  (SET_TAC[]);
 449  (REWRITE_WITH
 450   `(\x. sum
 451       {X | mcell_set V X /\
 452            ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} (\X. f X x)) =
 453     (\x. sum
 454       {X | mcell_set V X /\ critical_edgeX V X x} (\X. f X x))`);
 455  (REWRITE_TAC[FUN_EQ_THM]);
 456  (STRIP_TAC);
 457  (REWRITE_WITH
 458 `{X | mcell_set V X /\
 459       ~(!x. critical_edgeX V X x <=> {} x) /\ critical_edgeX V X x} =
 460  {X | mcell_set V X /\ critical_edgeX V X x}`);
 461  (REWRITE_TAC[SET_RULE `A = B <=> A SUBSET B /\ B SUBSET A`]);
 462  (STRIP_TAC);
 463  (SET_TAC[]);
 464  (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 465  (ASM_REWRITE_TAC[]);
 466  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 467  (REWRITE_TAC[MESON[IN] `(A:(real^3->bool)->bool) x <=> x IN A`]);
 468  (SET_TAC[]);
 469  (ASM_REWRITE_TAC[]);
 470
 471  (REWRITE_WITH
 472   ` (\x. sum
 473       {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
 474            ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} (\X. f X x)) =
 475      (\x. sum
 476       {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
 477            critical_edgeX V X x} (\X. f X x))`);
 478  (REWRITE_TAC[FUN_EQ_THM]);
 479  (STRIP_TAC);
 480  (REWRITE_WITH
 481 `{X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
 482       ~(!x. critical_edgeX V X x <=> {} x) /\ critical_edgeX V X x} =
 483  {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x}`);
 484  (REWRITE_TAC[SET_RULE `A = B <=> A SUBSET B /\ B SUBSET A`]);
 485  (STRIP_TAC);
 486  (SET_TAC[]);
 487  (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM]);
 488  (GEN_TAC THEN DISCH_TAC);
 489  (ASM_REWRITE_TAC[]);
 490  (UP_ASM_TAC THEN REPEAT STRIP_TAC);
 491  (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 492  (REWRITE_TAC[MESON[IN] `(A:(real^3->bool)->bool) x <=> x IN A`]);
 493  (SET_TAC[]);
 494
 495 (* OK here *)
 496
 497  (MATCH_MP_TAC (REAL_ARITH `(?x. c <= x /\ a + x <= b) ==> a <= b - c`));
 498  (EXISTS_TAC `dd * r pow 2`);
 499  (STRIP_TAC);
 500
 501  (ABBREV_TAC
 502    `T3:real^3->bool = V INTER ball (vec 0, r) DIFF ball (vec 0, r - &8)`);
 503  (ABBREV_TAC `T4 = {{u0:real^3, u1} | u0 IN T3 /\ u1 IN T3 /\
 504                                       ~(u0 = u1) /\ hl [u0; u1] <= hplus}`);
 505  (REWRITE_WITH `sum T2
 506  (\x. sum
 507       {X | ~(X SUBSET ball (vec 0,r)) /\
 508            mcell_set V X /\
 509            critical_edgeX V X x}
 510       (\X. f X x)) =  sum T4
 511  (\x. sum
 512       {X | ~(X SUBSET ball (vec 0,r)) /\
 513            mcell_set V X /\
 514            critical_edgeX V X x}
 515       (\X. f X x))`);
 516
 517  (EXPAND_TAC "T2");
 518  (MATCH_MP_TAC SUM_SUPERSET);
 519  (STRIP_TAC);
 520  (EXPAND_TAC "T4" THEN EXPAND_TAC "T1" THEN EXPAND_TAC "T3" THEN SET_TAC[]);
 521
 522  (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 523  (REWRITE_WITH
 524   `{X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x} =
 525    {}`);
 526  (REWRITE_TAC[SET_RULE `x = {} <=> ~(?s. s IN x)`]);
 527  (REWRITE_TAC[IN; IN_ELIM_THM] THEN STRIP_TAC);
 528
 529  (NEW_GOAL `(x:real^3->bool) SUBSET s`);
 530  (MATCH_MP_TAC CRITICAL_EDGEX_SUBSET_MCELL);
 531  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 532
 533  (NEW_GOAL `?p:real^3. p IN s DIFF ball (vec 0,r)`);
 534  (UNDISCH_TAC `~(s SUBSET ball ((vec 0):real^3,r))` THEN SET_TAC[]);
 535  (UP_ASM_TAC THEN STRIP_TAC);
 536  (UP_ASM_TAC THEN REWRITE_TAC[IN_DIFF; IN_BALL; REAL_ARITH
 537    `~(a < r) <=> r <= a`] THEN STRIP_TAC);
 538  (NEW_GOAL `s SUBSET ball (p:real^3,&8)`);
 539  (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);
 540  (EXISTS_TAC `V:real^3->bool`);
 541  (ASM_REWRITE_TAC[]);
 542  (NEW_GOAL `u0:real^3 IN ball (p,&8) /\ u1 IN ball (p,&8)`);
 543  (ASM_SET_TAC[]);
 544  (UP_ASM_TAC THEN REWRITE_TAC[IN_BALL] THEN STRIP_TAC);
 545  (UNDISCH_TAC `~(T4:(real^3->bool)->bool) x`);
 546  (REWRITE_TAC[MESON[IN] `(T4:(real^3->bool)->bool) x <=> x IN T4`]);
 547  (EXPAND_TAC "T4" THEN EXPAND_TAC "T3" THEN REWRITE_TAC[IN_INTER; IN_DIFF; IN_BALL]);
 548  (REWRITE_TAC[IN; IN_ELIM_THM]);
 549  (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);
 550  (UNDISCH_TAC `(T1:(real^3->bool)) u0` THEN
 551    UNDISCH_TAC `(T1:(real^3->bool)) u1`);
 552  (REWRITE_WITH `!x. T1 x <=> x:real^3 IN T1`);
 553  (ASM_REWRITE_TAC[IN]);
 554  (EXPAND_TAC "T1" THEN REWRITE_TAC[IN_INTER; IN_BALL]);
 555  (REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 556  (NEW_GOAL `dist (vec 0,p) <= dist (p, u0) + dist (vec 0, u0:real^3)`);
 557  (NORM_ARITH_TAC);
 558  (ASM_REAL_ARITH_TAC);
 559  (NEW_GOAL `dist (vec 0,p) <= dist (p, u1) + dist (vec 0, u1:real^3)`);
 560  (NORM_ARITH_TAC);
 561  (ASM_REAL_ARITH_TAC);
 562  (REWRITE_TAC[SUM_CLAUSES]);
 563
 564  (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`));
 565  (EXISTS_TAC `sum T4 (\x:real^3->bool. cc2 * cc1)`);
 566  (STRIP_TAC);
 567  (MATCH_MP_TAC SUM_LE);
 568  (STRIP_TAC);
 569  (MATCH_MP_TAC FINITE_SUBSET);
 570  (EXISTS_TAC `{{u0:real^3, u1} | u0 IN T3 /\ u1 IN T3}`);
 571  (STRIP_TAC);
 572  (MATCH_MP_TAC FINITE_SUBSET);
 573  (ABBREV_TAC `S_temp = {u0, u1:real^3 | u0 IN T3 /\ u1 IN T3}`);
 574  (ABBREV_TAC `f_temp = (\(u0,u1:real^3). {u0, u1})`);
 575  (EXISTS_TAC `IMAGE (f_temp:real^3#real^3->real^3->bool) S_temp`);
 576  (STRIP_TAC);
 577  (MATCH_MP_TAC FINITE_IMAGE);
 578  (EXPAND_TAC "S_temp" THEN MATCH_MP_TAC FINITE_PRODUCT THEN REWRITE_TAC[]);
 579  (MATCH_MP_TAC FINITE_SUBSET);
 580  (EXISTS_TAC `T1:real^3->bool`);
 581  (STRIP_TAC);
 582  (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 583  (ASM_SET_TAC[]);
 584  (EXPAND_TAC "f_temp" THEN EXPAND_TAC "S_temp" THEN
 585    REWRITE_TAC[IMAGE; SUBSET; IN; IN_ELIM_THM]);
 586  (REPEAT STRIP_TAC);
 587  (EXISTS_TAC `u0:real^3, u1:real^3` THEN ASM_REWRITE_TAC[]);
 588  (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);
 589  (ASM_SET_TAC[]);
 590  (REWRITE_TAC[IN] THEN EXPAND_TAC "T4" THEN EXPAND_TAC "T3" THEN
 591    REWRITE_TAC[ABS_SIMP; IN_DIFF; IN_INTER; IN_ELIM_THM]);
 592  (REPEAT STRIP_TAC);
 593
 594  (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`));
 595  (EXISTS_TAC
 596  `sum {X| ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x}
 597   (\x. cc1)`);
 598  (STRIP_TAC);
 599  (MATCH_MP_TAC SUM_LE);
 600  (STRIP_TAC);
 601  (MATCH_MP_TAC FINITE_SUBSET);
 602  (EXISTS_TAC `{X | mcell_set V X /\ edgeX V X x}`);
 603  (STRIP_TAC);
 604  (MATCH_MP_TAC Marchal_cells_3.FINITE_EDGE_X2);
 605  (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);
 606  (REWRITE_TAC[critical_edgeX] THEN SET_TAC[]);
 607  (REWRITE_TAC[BETA_THM; ABS_SIMP; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 608  (EXPAND_TAC "f");
 609  (NEW_GOAL `critical_weight V x' <= &1`);
 610  (REWRITE_TAC[critical_weight]);
 611  (REWRITE_WITH `&1 / &(CARD (critical_edgeX V x')) <= &1 <=>
 612                  &1  <= &(CARD (critical_edgeX V x'))`);
 613  (MATCH_MP_TAC Packing3.REAL_DIV_LE_1);
 614  (REWRITE_TAC[REAL_OF_NUM_LT; ARITH_RULE `0 < a <=> ~(a = 0)`]);
 615  (REWRITE_WITH `CARD (critical_edgeX V x') = 0 <=> critical_edgeX V x' = {}`);
 616  (MATCH_MP_TAC CARD_EQ_0);
 617  (REWRITE_TAC[critical_edgeX; edgeX] THEN MATCH_MP_TAC FINITE_SUBSET);
 618
 619  (EXISTS_TAC `{{u0:real^3, u1} | u0 IN VX V x' /\ u1 IN VX V x'}`);
 620  (STRIP_TAC);
 621  (MATCH_MP_TAC FINITE_SUBSET);
 622  (ABBREV_TAC `S_temp = {u0, u1:real^3 | u0 IN VX V x' /\ u1 IN VX V x'}`);
 623  (ABBREV_TAC `f_temp = (\(u0,u1:real^3). {u0, u1})`);
 624  (EXISTS_TAC `IMAGE (f_temp:real^3#real^3->real^3->bool) S_temp`);
 625  (STRIP_TAC);
 626  (MATCH_MP_TAC FINITE_IMAGE);
 627  (EXPAND_TAC "S_temp" THEN MATCH_MP_TAC FINITE_PRODUCT THEN REWRITE_TAC[]);
 628  (MATCH_MP_TAC FINITE_VX);
 629  (ASM_REWRITE_TAC[]);
 630  (EXPAND_TAC "f_temp" THEN EXPAND_TAC "S_temp" THEN
 631    REWRITE_TAC[IMAGE; SUBSET; IN; IN_ELIM_THM]);
 632  (REPEAT STRIP_TAC);
 633  (EXISTS_TAC `u0':real^3, u1':real^3` THEN ASM_REWRITE_TAC[]);
 634  (EXISTS_TAC `u0':real^3` THEN EXISTS_TAC `u1':real^3` THEN ASM_REWRITE_TAC[]);
 635  (ASM_SET_TAC[]);
 636  (UP_ASM_TAC THEN SET_TAC[]);
 637  (REWRITE_TAC[REAL_OF_NUM_LE; ARITH_RULE `1 <= a <=> ~(a = 0)`]);
 638  (REWRITE_WITH `CARD (critical_edgeX V x') = 0 <=> critical_edgeX V x' = {}`);
 639  (MATCH_MP_TAC CARD_EQ_0);
 640  (REWRITE_TAC[critical_edgeX; edgeX] THEN MATCH_MP_TAC FINITE_SUBSET);
 641  (EXISTS_TAC `{{u0:real^3, u1} | u0 IN VX V x' /\ u1 IN VX V x'}`);
 642  (STRIP_TAC);
 643  (MATCH_MP_TAC FINITE_SUBSET);
 644  (ABBREV_TAC `S_temp = {u0, u1:real^3 | u0 IN VX V x' /\ u1 IN VX V x'}`);
 645  (ABBREV_TAC `f_temp = (\(u0,u1:real^3). {u0, u1})`);
 646  (EXISTS_TAC `IMAGE (f_temp:real^3#real^3->real^3->bool) S_temp`);
 647  (STRIP_TAC);
 648  (MATCH_MP_TAC FINITE_IMAGE);
 649  (EXPAND_TAC "S_temp" THEN MATCH_MP_TAC FINITE_PRODUCT THEN REWRITE_TAC[]);
 650  (MATCH_MP_TAC FINITE_VX);
 651  (ASM_REWRITE_TAC[]);
 652  (EXPAND_TAC "f_temp" THEN EXPAND_TAC "S_temp" THEN
 653    REWRITE_TAC[IMAGE; SUBSET; IN; IN_ELIM_THM]);
 654  (REPEAT STRIP_TAC);
 655  (EXISTS_TAC `u0':real^3, u1':real^3` THEN ASM_REWRITE_TAC[]);
 656  (EXISTS_TAC `u0':real^3` THEN EXISTS_TAC `u1':real^3` THEN ASM_REWRITE_TAC[]);
 657  (ASM_SET_TAC[]);
 658  (UP_ASM_TAC THEN SET_TAC[]);
 659  (NEW_GOAL `&0 <= critical_weight V x'`);
 660  (REWRITE_TAC[critical_weight] THEN MATCH_MP_TAC REAL_LE_DIV);
 661  (REWRITE_TAC[REAL_ARITH `&0 <= &1`; REAL_OF_NUM_LE]);
 662  (ARITH_TAC);
 663  (NEW_GOAL `gammaX V x' lmfun <= cc1`);
 664  (FIRST_ASSUM MATCH_MP_TAC);
 665  (ASM_REWRITE_TAC[]);
 666  (NEW_GOAL `gammaX V x' lmfun * critical_weight V x' <= cc1 * critical_weight V x'`);
 667
 668  (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
 669  (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
 670  (MATCH_MP_TAC REAL_LE_MUL THEN ASM_REAL_ARITH_TAC);
 671
 672  (NEW_GOAL `cc1 * critical_weight V x' <= cc1`);
 673  (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
 674  (REWRITE_WITH `!x b. b - b * x = b * (&1 - x)`);
 675  (REAL_ARITH_TAC);
 676  (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
 677  (ASM_REAL_ARITH_TAC);
 678  (ASM_REAL_ARITH_TAC);
 679  (ASM_REAL_ARITH_TAC);
 680  (REWRITE_WITH
 681  `sum
 682   {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x}
 683   (\x. cc1) =
 684  &(CARD
 685    {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x})
 686    * cc1`);
 687  (MATCH_MP_TAC SUM_CONST);
 688  (MATCH_MP_TAC FINITE_SUBSET);
 689  (EXISTS_TAC `{X | mcell_set V X /\ edgeX V X x}`);
 690  (STRIP_TAC);
 691  (MATCH_MP_TAC Marchal_cells_3.FINITE_EDGE_X2);
 692  (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);
 693  (REWRITE_TAC[critical_edgeX] THEN SET_TAC[]);
 694
 695  (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
 696  (REWRITE_TAC[REAL_ARITH `a * x - b * x = x * (a - b)`]);
 697  (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
 698  (ASM_REAL_ARITH_TAC);
 699  (NEW_GOAL
 700   ` &(CARD
 701      {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x})
 702     <=  &(CARD {X | mcell_set V X /\ VX V X u0})`);
 703  (REWRITE_TAC[REAL_OF_NUM_LE] THEN MATCH_MP_TAC CARD_SUBSET);
 704  (STRIP_TAC);
 705  (ASM_REWRITE_TAC[critical_edgeX; edgeX; IN; IN_ELIM_THM]);
 706  (SET_TAC[]);
 707  (MATCH_MP_TAC FINITE_SUBSET);
 708  (EXISTS_TAC `{X | X SUBSET ball (u0,&8) /\ mcell_set V X}`);
 709  (STRIP_TAC);
 710  (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA_2);
 711  (ASM_REWRITE_TAC[]);
 712  (ONCE_REWRITE_TAC[SUBSET]);
 713  (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 714  (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);
 715  (EXISTS_TAC `V:real^3->bool`);
 716  (ASM_REWRITE_TAC[]);
 717  (NEW_GOAL `VX V x' = V INTER x'`);
 718  (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
 719  (UNDISCH_TAC `mcell_set V x'` THEN
 720    REWRITE_TAC[mcell_set; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 721  (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 722  (ASM_REWRITE_TAC[]);
 723  (STRIP_TAC);
 724  (UNDISCH_TAC `VX V x' u0` THEN ASM_REWRITE_TAC[VX]);
 725  (REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]);
 726  (SET_TAC[]);
 727  (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 728  (ASM_REWRITE_TAC[]);
 729
 730  (NEW_GOAL `&(CARD {X | mcell_set V X /\ VX V X u0}) <= cc2`);
 731  (ASM_MESON_TAC[]);
 732
 733  (ABBREV_TAC `s1_temp = &(CARD
 734        {X | ~(X SUBSET ball (vec 0,r)) /\
 735             mcell_set V X /\
 736             critical_edgeX V X x})`);
 737  (ABBREV_TAC `s2_temp = &(CARD {X | mcell_set V X /\ VX V X u0})`);
 738  (ASM_REAL_ARITH_TAC);
 739
 740  (ABBREV_TAC `g = (\x:real^3->bool. cc2 * cc1)`);
 741
 742  (REWRITE_WITH
 743   `sum T4 (g:(real^3->bool)->real) =
 744    &1 / &2 *
 745    sum {m,n | m IN T3 /\ n IN T3 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus}
 746    (\(m:real^3,n). g {m, n})`);
 747  (ONCE_REWRITE_TAC[REAL_ARITH `a = &1 / &2 * b <=> b = &2 * a`]);
 748  (EXPAND_TAC "T4");
 749  (REWRITE_TAC[HL_2; REAL_ARITH `inv (&2) * a <= b <=> a <= &2 * b`]);
 750  (MATCH_MP_TAC SUM_PAIR_2_SET);
 751  (MATCH_MP_TAC FINITE_SUBSET);
 752  (EXISTS_TAC `T1:real^3->bool`);
 753  (STRIP_TAC);
 754  (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 755  (ASM_SET_TAC[]);
 756  (REWRITE_TAC[REAL_ARITH `&1 / &2 * s <= t <=> s <= &2 * t`]);
 757
 758  (ABBREV_TAC
 759   `h = (\m:real^3. {n | n IN T3 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus})`);
 760  (REWRITE_WITH
 761   `{m,n | m IN T3 /\ n IN T3 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus} =
 762    {m:real^3,n | m IN T3 /\ n IN h m}`);
 763  (EXPAND_TAC "h");
 764  (SET_TAC[PAIR_EQ]);
 765  (ABBREV_TAC `k = (\m n. (g:(real^3->bool)->real) {m,n})`);
 766  (REWRITE_WITH `(\(m,n). (g:(real^3->bool)->real) {m, n}) = (\(m,n). k m n)`);
 767  (REWRITE_TAC[FUN_EQ_THM]);
 768  (STRIP_TAC);
 769  (NEW_GOAL `(x:real^3#real^3) = FST x, SND x`);
 770  (REWRITE_TAC[PAIR]);
 771  (ONCE_REWRITE_TAC[ASSUME `(x:real^3#real^3) = FST x, SND x`]);
 772  (EXPAND_TAC "k" THEN REWRITE_TAC[]);
 773  (REWRITE_WITH
 774   `sum {m:real^3,n:real^3 | m IN T3 /\ n IN h m} (\(m,n). k m n)  =
 775    sum T3 (\m. sum (h m) (k m))`);
 776  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 777  (MATCH_MP_TAC SUM_SUM_PRODUCT);
 778  (STRIP_TAC);
 779
 780  (MATCH_MP_TAC FINITE_SUBSET);
 781  (EXISTS_TAC `T1:real^3->bool`);
 782  (STRIP_TAC);
 783  (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 784  (ASM_SET_TAC[]);
 785  (REPEAT STRIP_TAC);
 786  (EXPAND_TAC "h");
 787
 788  (MATCH_MP_TAC FINITE_SUBSET);
 789  (EXISTS_TAC `T3:real^3->bool`);
 790  (STRIP_TAC);
 791  (MATCH_MP_TAC FINITE_SUBSET);
 792  (EXISTS_TAC `T1:real^3->bool`);
 793  (STRIP_TAC);
 794  (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 795  (ASM_SET_TAC[]);
 796  (SET_TAC[]);
 797
 798  (EXPAND_TAC "k" THEN EXPAND_TAC "g");
 799  (NEW_GOAL `sum T3 (\m. sum ((h:real^3->real^3->bool) m) (\n. cc2 * cc1)) <=
 800              sum T3 (\m. (&4) pow 3 * cc2 * cc1)`);
 801  (MATCH_MP_TAC SUM_LE);
 802  (STRIP_TAC);
 803  (MATCH_MP_TAC FINITE_SUBSET);
 804  (EXISTS_TAC `T1:real^3->bool`);
 805  (STRIP_TAC);
 806  (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 807  (ASM_SET_TAC[]);
 808  (EXPAND_TAC "h" THEN REPEAT STRIP_TAC THEN REWRITE_TAC[]);
 809  (REWRITE_WITH
 810  `sum {n:real^3 | n IN T3 /\ ~(x = n) /\
 811                   dist (x,n) <= &2 * hplus} (\n. cc2 * cc1) =
 812   &(CARD {n | n IN T3 /\ ~(x = n) /\ dist (x,n) <= &2 * hplus}) *
 813   (cc2 * cc1)`);
 814  (MATCH_MP_TAC SUM_CONST);
 815  (MATCH_MP_TAC FINITE_SUBSET);
 816  (EXISTS_TAC `T3:real^3->bool`);
 817  (STRIP_TAC);
 818  (MATCH_MP_TAC FINITE_SUBSET);
 819  (EXISTS_TAC `T1:real^3->bool`);
 820  (STRIP_TAC);
 821  (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 822  (ASM_SET_TAC[]);
 823  (SET_TAC[]);
 824
 825  (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
 826  (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
 827  (MATCH_MP_TAC REAL_LE_MUL);
 828  (STRIP_TAC);
 829  (ONCE_REWRITE_TAC[GSYM (REAL_ARITH `(a <= b <=> &0 <= b - a)`)]);
 830
 831
 832  (NEW_GOAL
 833    `&(CARD {n | n IN T3 /\ ~(x = n) /\ dist (x,n) <= &2 * hplus}) <=
 834     &(CARD (V INTER ball (x:real^3, &3)))`);
 835  (REWRITE_TAC[REAL_OF_NUM_LE]);
 836  (MATCH_MP_TAC CARD_SUBSET);
 837  (STRIP_TAC);
 838  (EXPAND_TAC "T3" THEN REWRITE_TAC[IN_DIFF; IN_BALL]);
 839  (REWRITE_TAC[IN_INTER; IN_BALL; IN_ELIM_THM; SUBSET; IN]);
 840  (REPEAT STRIP_TAC);
 841  (ASM_REWRITE_TAC[]);
 842  (NEW_GOAL `&2 * hplus < &3`);
 843  (REWRITE_TAC[hplus] THEN REAL_ARITH_TAC);
 844  (ASM_REAL_ARITH_TAC);
 845  (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 846  (NEW_GOAL `&(CARD (V INTER ball (x:real^3,&3))) <= &4 pow 3`);
 847  (REWRITE_TAC[REAL_ARITH `&4 = &3 + &1`]);
 848  (MATCH_MP_TAC BOUNDS_VGEN_klemma);
 849  (ASM_REWRITE_TAC[REAL_ARITH `&0 <= &3`]);
 850  (ABBREV_TAC
 851  `s1 = &(CARD {n:real^3 | n IN T3 /\ ~(x = n) /\ dist (x,n) <= &2 * hplus})`);
 852  (ASM_REAL_ARITH_TAC);
 853  (MATCH_MP_TAC REAL_LE_MUL);
 854  (ASM_REAL_ARITH_TAC);
 855  (NEW_GOAL `sum T3 (\m:real^3. &4 pow 3 * cc2 * cc1) <= &2 * dd * r pow 2`);
 856  (REWRITE_WITH
 857   `sum T3 (\m:real^3. &4 pow 3 * cc2 * cc1) =
 858    &(CARD T3) * &4 pow 3 * cc2 * cc1`);
 859  (MATCH_MP_TAC SUM_CONST);
 860  (MATCH_MP_TAC FINITE_SUBSET);
 861  (EXISTS_TAC `T1:real^3->bool`);
 862  (STRIP_TAC);
 863  (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
 864  (ASM_SET_TAC[]);
 865  (EXPAND_TAC "dd");
 866
 867  (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
 868  (REWRITE_TAC[REAL_ARITH
 869  `&2 * (&1 / &2 * dd2 * &4 pow 3 * cc2 * cc1) * r pow 2 -
 870  &(CARD (T3:real^3->bool)) * &4 pow 3 * cc2 * cc1 =
 871   (&4 pow 3 * cc2 * cc1) * (dd2 * r pow 2 - &(CARD T3))`]);
 872  (MATCH_MP_TAC REAL_LE_MUL);
 873  (STRIP_TAC);
 874  (REWRITE_TAC[REAL_ARITH `&0 <= &4 pow 3 * x <=> &0 <= x`]);
 875  (MATCH_MP_TAC REAL_LE_MUL);
 876  (ASM_REAL_ARITH_TAC);
 877  (ONCE_REWRITE_TAC[GSYM (REAL_ARITH `(a <= b <=> &0 <= b - a)`)]);
 878  (EXPAND_TAC "T3");
 879
 880  (ONCE_REWRITE_TAC[SET_RULE `A INTER B DIFF C = A INTER B DIFF A INTER C`]);
 881  (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`));
 882  (EXISTS_TAC `dd1 * r pow 2`);
 883  (STRIP_TAC);
 884  (FIRST_ASSUM MATCH_MP_TAC);
 885  (ASM_REWRITE_TAC[]);
 886  (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
 887  (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b ) * x`]);
 888  (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
 889  (ASM_REAL_ARITH_TAC);
 890  (REWRITE_TAC[REAL_LE_POW_2]);
 891  (ASM_REAL_ARITH_TAC);
 892
 893 (* ======================================================================== *)
 894 (* CHECK DEN DAY LA OK ROI - (._o) (0_o) *)
 895 (* ==================================================================== *)
 896
 897  (REWRITE_WITH
 898  `sum T2 (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (\X. f X x)) =
 899   sum T2 (\e. cluster_gamma_v1 V e (cell_cluster V e)) -
 900   sum T2 (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (beta_bump_v1 V x))`);
 901  (REWRITE_TAC[REAL_ARITH `a = b - c <=> b = a + c`]);
 902  (ABBREV_TAC
 903  `f1 = (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (\X. f X x))`);
 904  (ABBREV_TAC
 905  `f2 = (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (beta_bump_v1 V x))`);
 906  (REWRITE_WITH
 907  `sum T2 (\e. cluster_gamma_v1 V e (cell_cluster V e)) =
 908   sum T2 (\e:real^3->bool. f1 e + f2 e)`);
 909  (MATCH_MP_TAC SUM_EQ);
 910  (EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 911  (EXPAND_TAC "f1" THEN EXPAND_TAC "f2" THEN REWRITE_TAC[cluster_gamma_v1; cell_cluster]);
 912  (REWRITE_TAC[FUN_EQ_THM] THEN REPEAT STRIP_TAC);
 913  (EXPAND_TAC "f");
 914  (REWRITE_TAC[SET_RULE `{X | x IN critical_edgeX V X /\ mcell_set V X} =
 915                          {X | mcell_set V X /\ critical_edgeX V X x}`]);
 916  (MATCH_MP_TAC SUM_ADD);
 917  (MATCH_MP_TAC FINITE_SUBSET);
 918  (EXISTS_TAC `{X | X SUBSET ball (u0,&8) /\ mcell_set V X}`);
 919  (STRIP_TAC);
 920  (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA_2);
 921  (ASM_REWRITE_TAC[]);
 922  (ONCE_REWRITE_TAC[SUBSET]);
 923  (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 924  (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);
 925  (EXISTS_TAC `V:real^3->bool`);
 926  (ASM_REWRITE_TAC[]);
 927  (NEW_GOAL `VX V x' = V INTER x'`);
 928  (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
 929  (UNDISCH_TAC `mcell_set V x'` THEN
 930    REWRITE_TAC[mcell_set; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 931  (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 932  (ASM_REWRITE_TAC[]);
 933  (STRIP_TAC);
 934  (UNDISCH_TAC `critical_edgeX V x' x` THEN
 935    REWRITE_TAC[critical_edgeX; edgeX; IN; IN_ELIM_THM] THEN STRIP_TAC);
 936  (NEW_GOAL `VX V x' u0`);
 937  (NEW_GOAL `u0 = u' \/ u0 = v':real^3`);
 938  (ASM_SET_TAC[]);
 939  (UP_ASM_TAC THEN STRIP_TAC);
 940  (REWRITE_TAC[ASSUME `u0 = u':real^3`]);
 941  (ASM_REWRITE_TAC[]);
 942  (REWRITE_TAC[ASSUME `u0 = v':real^3`]);
 943  (ASM_REWRITE_TAC[]);
 944
 945  (UNDISCH_TAC `VX V x' u0` THEN ASM_REWRITE_TAC[VX]);
 946  (REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]);
 947  (SET_TAC[]);
 948
 949  (NEW_GOAL `VX V x' u0`);
 950  (UNDISCH_TAC `mcell_set V x'` THEN
 951    REWRITE_TAC[mcell_set; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 952  (UNDISCH_TAC `critical_edgeX V x' x` THEN
 953    REWRITE_TAC[critical_edgeX; edgeX; IN; IN_ELIM_THM] THEN STRIP_TAC);
 954  (NEW_GOAL `u0 = u' \/ u0 = v':real^3`);
 955  (ASM_SET_TAC[]);
 956  (UP_ASM_TAC THEN STRIP_TAC);
 957  (REWRITE_TAC[ASSUME `u0 = u':real^3`]);
 958  (ASM_REWRITE_TAC[]);
 959  (REWRITE_TAC[ASSUME `u0 = v':real^3`]);
 960  (ASM_REWRITE_TAC[]);
 961  (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 962  (ASM_REWRITE_TAC[]);
 963  (MATCH_MP_TAC SUM_ADD);
 964  (ASM_REWRITE_TAC[]);
 965
 966  (MATCH_MP_TAC (REAL_ARITH `&0 <= a /\ b + x <= &0 ==> x <= a - b`));
 967  (STRIP_TAC);
 968  (MATCH_MP_TAC SUM_POS_LE);
 969  (ASM_REWRITE_TAC[]);
 970  (EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 971  (REPEAT STRIP_TAC);
 972
 973  (UNDISCH_TAC `cell_cluster_estimate_v1 V`);
 974  (REWRITE_TAC[cell_cluster_estimate_v1]);
 975  (REWRITE_TAC[REAL_ARITH `&0 <= a <=> a >= &0`] THEN STRIP_TAC);
 976  (ASM_REWRITE_TAC[]);
 977
 978  (ABBREV_TAC
 979   `f1 = (\x. sum {X | X SUBSET ball (vec 0, r + &8) /\
 980                       ~(X SUBSET ball (vec 0, r - &8)) /\
 981                       mcell_set V X /\
 982                       critical_edgeX V X x} (beta_bump_v1 V x))`);
 983  (ABBREV_TAC
 984   `f2 = (\x. sum {X | X SUBSET ball (vec 0, r - &8) /\ mcell_set V X /\
 985                       critical_edgeX V X x} (beta_bump_v1 V x))`);
 986  (REWRITE_WITH
 987   `sum T2 (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (beta_bump_v1 V x))
 988    = sum (T2:(real^3->bool)->bool) f1 + sum T2 f2`);
 989  (REWRITE_WITH
 990   `sum (T2:(real^3->bool)->bool) f1 + sum T2 f2 = sum T2 (\x. f1 x + f2 x)`);
 991  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 992  (MATCH_MP_TAC SUM_ADD);
 993  (ASM_REWRITE_TAC[]);
 994
 995  (MATCH_MP_TAC SUM_EQ);
 996  (EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 997  (EXPAND_TAC "f1" THEN EXPAND_TAC "f2");
 998  (ABBREV_TAC
 999  `s1 = {X | X SUBSET ball (vec 0,r + &8) /\ ~(X SUBSET ball (vec 0,r - &8)) /\
1000             mcell_set V X /\ critical_edgeX V X x}`);
1001  (ABBREV_TAC `s2 = {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X /\
1002                          critical_edgeX V X x}`);
1003  (REWRITE_WITH `{X | mcell_set V X /\ critical_edgeX V X x} = s1 UNION s2`);
1004  (EXPAND_TAC "s1" THEN EXPAND_TAC "s2" THEN
1005    REWRITE_TAC[SET_EQ_LEMMA; IN_UNION; IN_ELIM_THM; IN]);
1006  (REPEAT STRIP_TAC);
1007  (ASM_REWRITE_TAC[]);
1008
1009  (ASM_CASES_TAC `x' SUBSET ball ((vec 0):real^3,r - &8)`);
1010  (ASM_REWRITE_TAC[]);
1011  (ASM_REWRITE_TAC[SUBSET; IN_DIFF; IN_BALL]);
1012  (REPEAT STRIP_TAC);
1013
1014  (NEW_GOAL `x' SUBSET ball (u0:real^3, &8)`);
1015  (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);
1016
1017  (EXISTS_TAC `V:real^3->bool`);
1018  (ASM_REWRITE_TAC[]);
1019  (NEW_GOAL `x:real^3->bool SUBSET x'`);
1020  (MATCH_MP_TAC CRITICAL_EDGEX_SUBSET_MCELL);
1021  (EXISTS_TAC `V:real^3->bool`);
1022  (ASM_REWRITE_TAC[]);
1023  (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
1024  (SET_TAC[]);
1025  (NEW_GOAL `dist (u0:real^3, x'') < &8`);
1026  (REWRITE_TAC[GSYM IN_BALL] THEN ASM_SET_TAC[]);
1027  (NEW_GOAL `dist (vec 0, x'') <= dist (u0, x'') + dist (vec 0, u0:real^3)`);
1028  (NORM_ARITH_TAC);
1029  (NEW_GOAL `dist (vec 0, u0:real^3) < r`);
1030  (REWRITE_TAC[GSYM IN_BALL]);
1031  (UNDISCH_TAC `(T1:real^3->bool) u0`);
1032  (EXPAND_TAC "T1" THEN REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]);
1033  (SET_TAC[]);
1034  (ASM_REAL_ARITH_TAC);
1035  (ASM_REWRITE_TAC[]);
1036
1037  (ASM_REWRITE_TAC[]);
1038  (ASM_REWRITE_TAC[]);
1039  (ASM_REWRITE_TAC[]);
1040  (MATCH_MP_TAC SUM_UNION);
1041  (REPEAT STRIP_TAC);
1042  (MATCH_MP_TAC FINITE_SUBSET);
1043  (EXISTS_TAC `{X | X SUBSET ball (vec 0,r + &8) /\ mcell_set V X}`);
1044  (STRIP_TAC);
1045  (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA_2]);
1046  (ASM_SET_TAC[]);
1047  (MATCH_MP_TAC FINITE_SUBSET);
1048  (EXISTS_TAC `{X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X}`);
1049  (STRIP_TAC);
1050  (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA_2]);
1051  (ASM_SET_TAC[]);
1052
1053 (* ======================================================================== *)
1054 (* ======================================================================== *)
1055
1056  (EXPAND_TAC "s1" THEN EXPAND_TAC "s2" THEN SET_TAC[]);
1057
1058  (REWRITE_WITH `sum (T2:(real^3->bool)->bool) f2 = &0`);
1059  (EXPAND_TAC "f2");
1060  (REWRITE_TAC[SET_RULE
1061   `!V r x. {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X /\
1062                          critical_edgeX V X x} =
1063            {X | X IN {X| X SUBSET ball (vec 0,r - &8) /\ mcell_set V X} /\
1064                          critical_edgeX V X x}`]);
1065  (REWRITE_WITH
1066  `sum T2
1067   (\x. sum
1068       {X | X IN {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X} /\
1069            critical_edgeX V X x}
1070       (beta_bump_v1 V x)) =
1071  sum T2
1072   (\x. sum
1073       {X | X IN {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X} /\
1074            critical_edgeX V X x}
1075       (\X. beta_bump_v1 V x X))`);
1076  (REWRITE_WITH `!x V. (\X. beta_bump_v1 V x X) = beta_bump_v1 V x`);
1077  (REWRITE_TAC[FUN_EQ_THM] THEN ASM_REWRITE_TAC[]);
1078
1079  (ABBREV_TAC `t = {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X}`);
1080  (ABBREV_TAC `g = beta_bump_v1 V`);
1081  (ABBREV_TAC `s = T2:(real^3->bool)->bool`);
1082  (REWRITE_WITH
1083    `sum s (\x. sum {X | X IN t /\ critical_edgeX V X x} (\X. g x X)) =
1084     sum t (\X. sum {x | x IN s /\ critical_edgeX V X x} (\x. g x X))`);
1085  (MATCH_MP_TAC SUM_SUM_RESTRICT);
1086  (STRIP_TAC);
1087  (EXPAND_TAC "s" THEN ASM_REWRITE_TAC[]);
1088  (EXPAND_TAC "t");
1089  (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA);
1090  (ASM_REWRITE_TAC[]);
1091  (EXPAND_TAC "s" THEN EXPAND_TAC "t" THEN EXPAND_TAC "g");
1092  (MATCH_MP_TAC SUM_EQ_0);
1093  (REWRITE_TAC[IN; IN_ELIM_THM] THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC);
1094
1095  (REWRITE_WITH `{x' | T2 x' /\ critical_edgeX V x x'} =
1096                  {x' | x' IN critical_edgeX V x}`);
1097  (MATCH_MP_TAC (SET_RULE `A SUBSET B /\ B SUBSET A ==> A = B`));
1098  (STRIP_TAC);
1099  (SET_TAC[]);
1100  (ASM_REWRITE_TAC[IN]);
1101  (REWRITE_TAC[GSYM (ASSUME `{{u0:real^3, u1} | u0 IN T1 /\ u1 IN T1 /\
1102                              ~(u0 = u1) /\ hl [u0; u1] <= hplus} = s`)]);
1103
1104  (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; critical_edgeX; edgeX]);
1105  (REPEAT STRIP_TAC);
1106  (EXISTS_TAC `u':real^3` THEN EXISTS_TAC `v':real^3` THEN ASM_REWRITE_TAC[]);
1107  (EXPAND_TAC "T1");
1108  (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`; IN_INTER; IN_BALL]);
1109  (NEW_GOAL `VX V x = V INTER x`);
1110  (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
1111  (UNDISCH_TAC `mcell_set V x` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]);
1112  (STRIP_TAC);
1113  (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
1114  (ASM_REWRITE_TAC[IN]);
1115  (STRIP_TAC THEN UNDISCH_TAC `VX V x u'`);
1116  (ASM_REWRITE_TAC[VX; MESON[IN] `{} x <=> x IN {}`] THEN SET_TAC[]);
1117  (REWRITE_WITH `u':real^3 IN V /\ v' IN V`);
1118  (ASM_SET_TAC[]);
1119  (REPEAT STRIP_TAC);
1120
1121  (NEW_GOAL `u':real^3 IN ball (vec 0, r - &8)`);
1122  (ASM_SET_TAC[]);
1123  (UP_ASM_TAC THEN REWRITE_TAC[IN_BALL] THEN REAL_ARITH_TAC);
1124  (NEW_GOAL `v':real^3 IN ball (vec 0, r - &8)`);
1125  (ASM_SET_TAC[]);
1126  (UP_ASM_TAC THEN REWRITE_TAC[IN_BALL] THEN REAL_ARITH_TAC);
1127  (REWRITE_WITH `hl [u'; v':real^3] = hl [u; v:real^3]`);
1128  (REWRITE_TAC[HL; set_of_list]);
1129  (ASM_REWRITE_TAC[]);
1130  (ASM_REWRITE_TAC[]);
1131
1132  (EXISTS_TAC `u:real^3` THEN EXISTS_TAC `v:real^3`);
1133  (ASM_REWRITE_TAC[]);
1134  (EXISTS_TAC `u':real^3` THEN EXISTS_TAC `v':real^3`);
1135  (ASM_REWRITE_TAC[]);
1136  (MATCH_MP_TAC Bump.SUM_BETA_BUMP_LEMMA);
1137  (ASM_REWRITE_TAC[]);
1138
1139  (REWRITE_TAC[REAL_ARITH `a + &0 = a`]);
1140  (EXPAND_TAC "T2");
1141  (REWRITE_TAC[HL_2; REAL_ARITH `inv (&2) * a <= b <=> a <= &2 * b`]);
1142  (REWRITE_WITH
1143  `sum {{u0:real^3, u1} | u0 IN T1 /\ u1 IN T1 /\ ~(u0 = u1) /\
1144                          dist (u0,u1) <= &2 * hplus} f1 =
1145  &1 / &2 *
1146  sum {m,n | m IN T1 /\ n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus}
1147      (\(m,n). f1 {m, n})`);
1148  (REWRITE_TAC[REAL_ARITH `a = &1 / &2 * b <=> b = &2 * a`]);
1149  (MATCH_MP_TAC SUM_PAIR_2_SET);
1150  (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA);
1151  (ASM_REWRITE_TAC[]);
1152
1153  (ABBREV_TAC
1154   `T3 = V INTER ball ((vec 0):real^3,r) DIFF ball (vec 0, r - &16)`);
1155  (REWRITE_WITH
1156   `sum {m:real^3,n | m IN T1 /\ n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus}
1157      (\(m,n). f1 {m, n}) =
1158    sum {m,n | m IN T3 /\ n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus}
1159  (\(m,n). f1 {m, n})`);
1160  (MATCH_MP_TAC SUM_SUPERSET);
1161  (STRIP_TAC);
1162  (EXPAND_TAC "T1" THEN EXPAND_TAC "T3" THEN
1163    REWRITE_TAC[SUBSET; IN; IN_ELIM_THM]);
1164  (REPEAT STRIP_TAC);
1165  (EXISTS_TAC `m:real^3` THEN EXISTS_TAC `n:real^3` THEN ASM_REWRITE_TAC[]);
1166  (EXPAND_TAC "T1" THEN UNDISCH_TAC
1167    `(V INTER ball ((vec 0):real^3,r) DIFF ball (vec 0,r - &16)) m` THEN
1168    REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]);
1169  (SET_TAC[]);
1170  (EXPAND_TAC "T1" THEN EXPAND_TAC "T3" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
1171  (REPEAT STRIP_TAC);
1172  (ASM_REWRITE_TAC[]);
1173  (EXPAND_TAC "f1");
1174  (REWRITE_WITH
1175  `{X | X SUBSET ball (vec 0,r + &8) /\
1176        ~(X SUBSET ball (vec 0,r - &8)) /\
1177        mcell_set V X /\
1178        critical_edgeX V X {m, n}} = {}`);
1179  (REWRITE_TAC[SET_RULE `y = {} <=> ~(?x. x IN y)`]);
1180  (REPEAT STRIP_TAC);
1181  (UNDISCH_TAC `~(?m n.
1182             ((V INTER ball (vec 0,r) DIFF ball (vec 0,r - &16)) m /\
1183              (V INTER ball (vec 0,r)) n /\
1184              ~(m = n) /\
1185              dist (m:real^3,n) <= &2 * hplus) /\
1186             x = m,n) ` THEN REWRITE_TAC[]);
1187  (EXISTS_TAC `m:real^3` THEN EXISTS_TAC `n:real^3`);
1188  (ASM_REWRITE_TAC[]);
1189  (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]);
1190  (EXPAND_TAC "T3" THEN REWRITE_TAC[IN_DIFF; IN; IN_BALL]);
1191  (ASM_REWRITE_TAC[]);
1192  (UP_ASM_TAC THEN REWRITE_TAC[IN; IN_ELIM_THM]);
1193  (REPEAT STRIP_TAC);
1194  (NEW_GOAL `?p:real^3. p IN x' /\ ~(p IN ball (vec 0,r - &8))`);
1195  (UNDISCH_TAC `~(x' SUBSET ball ((vec 0):real^3,r - &8))`);
1196  (SET_TAC[]);
1197  (UP_ASM_TAC THEN STRIP_TAC);
1198  (UP_ASM_TAC THEN REWRITE_TAC[IN_BALL]);
1199  (NEW_GOAL `x' SUBSET ball (p:real^3, &8)`);
1200  (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);
1201  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
1202  (NEW_GOAL `m:real^3 IN x'`);
1203  (UNDISCH_TAC `critical_edgeX V x' {m, n}` THEN
1204    REWRITE_TAC[critical_edgeX; edgeX; IN_ELIM_THM; IN]);
1205  (REPEAT STRIP_TAC);
1206
1207  (NEW_GOAL `VX V x' = V INTER x'`);
1208  (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
1209  (UNDISCH_TAC `mcell_set V x'` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]);
1210  (STRIP_TAC);
1211  (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
1212  (ASM_REWRITE_TAC[IN]);
1213  (STRIP_TAC THEN UNDISCH_TAC `VX V x' u'`);
1214  (ASM_REWRITE_TAC[VX; MESON[IN] `{} x <=> x IN {}`] THEN SET_TAC[]);
1215
1216  (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]);
1217  (ASM_SET_TAC[]);
1218  (NEW_GOAL `dist (p, m:real^3) < &8`);
1219  (REWRITE_TAC[GSYM IN_BALL]);
1220  (ASM_SET_TAC[]);
1221  (NEW_GOAL `dist (vec 0, p) <= dist (vec 0, m:real^3) + dist (p, m)`);
1222  (NORM_ARITH_TAC);
1223  (ASM_REAL_ARITH_TAC);
1224  (REWRITE_TAC[SUM_CLAUSES]);
1225
1226  (ABBREV_TAC
1227   `g = (\m:real^3. {n | n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus})`);
1228  (REWRITE_WITH
1229   `{m,n | m IN T3 /\ n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus} =
1230    {m,n:real^3 | m IN T3 /\ n IN g m}`);
1231  (EXPAND_TAC "g" THEN ASM_REWRITE_TAC[] THEN SET_TAC[]);
1232  (ABBREV_TAC `h = (\m. (\n. (f1:(real^3->bool)->real) {m, n}))`);
1233  (REWRITE_WITH `(\(m,n). (f1:(real^3->bool)->real) {m, n}) =
1234                  (\(m,n). h m n)`);
1235  (REWRITE_TAC[FUN_EQ_THM]);
1236  (STRIP_TAC THEN ASM_REWRITE_TAC[]);
1237  (NEW_GOAL `x:real^3#real^3 = FST x, SND x`);
1238  (REWRITE_TAC[PAIR]);
1239  (ONCE_ASM_REWRITE_TAC[]);
1240  (EXPAND_TAC "h" THEN REWRITE_TAC[]);
1241
1242  (REWRITE_WITH `sum {m,n | m IN T3 /\ n IN g m} (\(m,n). h m n) =
1243                  sum T3 (\m. sum (g m) ((h:real^3->real^3->real) m))`);
1244  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
1245  (MATCH_MP_TAC SUM_SUM_PRODUCT);
1246  (STRIP_TAC);
1247
1248  (MATCH_MP_TAC FINITE_SUBSET);
1249  (EXISTS_TAC `V:real^3->bool INTER ball (vec 0,r)`);
1250  (STRIP_TAC);
1251  (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
1252  (EXPAND_TAC "T3" THEN SET_TAC[]);
1253
1254  (REPEAT STRIP_TAC);
1255  (EXPAND_TAC "g" THEN REWRITE_TAC[]);
1256  (MATCH_MP_TAC FINITE_SUBSET);
1257  (EXISTS_TAC `V:real^3->bool INTER ball (vec 0,r)`);
1258  (STRIP_TAC);
1259  (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
1260  (EXPAND_TAC "T1" THEN SET_TAC[]);
1261
1262  (NEW_GOAL
1263   `sum T3 (\m. sum ((g:real^3->real^3->bool) m) (h m)) <=
1264    sum T3 (\n:real^3. ss1)`);
1265  (MATCH_MP_TAC SUM_LE);
1266  (STRIP_TAC);
1267  (MATCH_MP_TAC FINITE_SUBSET);
1268  (EXISTS_TAC `V:real^3->bool INTER ball (vec 0,r)`);
1269  (STRIP_TAC);
1270  (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
1271  (EXPAND_TAC "T3" THEN SET_TAC[]);
1272  (REPEAT STRIP_TAC THEN REWRITE_TAC[]);
1273
1274  (NEW_GOAL `sum ((g:real^3->real^3->bool) x) (h x) <= sum (g x) (\x. cc4 * cc3)`);
1275  (MATCH_MP_TAC SUM_LE);
1276  (STRIP_TAC);
1277  (EXPAND_TAC "g" THEN REWRITE_TAC[]);
1278  (MATCH_MP_TAC FINITE_SUBSET);
1279  (EXISTS_TAC `V:real^3->bool INTER ball (vec 0,r)`);
1280  (STRIP_TAC);
1281  (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
1282  (EXPAND_TAC "T1" THEN SET_TAC[]);
1283
1284  (REPEAT STRIP_TAC THEN EXPAND_TAC "h" THEN REWRITE_TAC[]);
1285  (EXPAND_TAC "f1");
1286  (ABBREV_TAC `S1 = {X | X SUBSET ball (vec 0,r + &8) /\
1287       ~(X SUBSET ball (vec 0,r - &8)) /\
1288       mcell_set V X /\
1289       critical_edgeX V X {x, x'}}`);
1290  (NEW_GOAL `sum (S1:(real^3->bool)->bool) (beta_bump_v1 V {x, x'}) <=
1291              sum S1 (\x. cc3)`);
1292  (MATCH_MP_TAC SUM_LE);
1293  (STRIP_TAC);
1294  (MATCH_MP_TAC FINITE_SUBSET);
1295  (EXISTS_TAC `{X | X SUBSET ball (vec 0,r + &8) /\ mcell_set V X}`);
1296  (STRIP_TAC);
1297  (REPEAT STRIP_TAC THEN REWRITE_TAC[]);
1298  (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA);
1299  (ASM_REWRITE_TAC[]);
1300  (EXPAND_TAC "S1" THEN SET_TAC[]);
1301  (REPEAT STRIP_TAC);
1302  (REWRITE_TAC[]);
1303  (FIRST_ASSUM MATCH_MP_TAC);
1304  (UP_ASM_TAC THEN EXPAND_TAC "S1" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
1305  (STRIP_TAC THEN ASM_REWRITE_TAC[]);
1306
1307  (NEW_GOAL `sum S1 (\x:real^3->bool. cc3) = &(CARD S1) * cc3`);
1308  (MATCH_MP_TAC SUM_CONST);
1309  (MATCH_MP_TAC FINITE_SUBSET);
1310  (EXISTS_TAC `{X | X SUBSET ball (vec 0,r + &8) /\ mcell_set V X}`);
1311  (STRIP_TAC);
1312  (REPEAT STRIP_TAC THEN REWRITE_TAC[]);
1313  (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA);
1314  (ASM_REWRITE_TAC[]);
1315  (EXPAND_TAC "S1" THEN SET_TAC[]);
1316  (NEW_GOAL `&(CARD (S1:(real^3->bool)->bool)) <= cc4`);
1317  (NEW_GOAL `&(CARD (S1:(real^3->bool)->bool)) <=
1318              &(CARD {X | mcell_set V X /\ VX V X x})`);
1319  (REWRITE_TAC[REAL_OF_NUM_LE]);
1320  (MATCH_MP_TAC CARD_SUBSET);
1321  (STRIP_TAC);
1322  (EXPAND_TAC "S1" THEN
1323    REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; critical_edgeX; edgeX] THEN
1324    REPEAT STRIP_TAC);
1325  (ASM_REWRITE_TAC[]);
1326  (NEW_GOAL `x:real^3 = u' \/ x = v'`);
1327  (ASM_SET_TAC[]);
1328  (UP_ASM_TAC THEN STRIP_TAC);
1329  (ASM_REWRITE_TAC[]);
1330  (ASM_REWRITE_TAC[]);
1331
1332  (MATCH_MP_TAC FINITE_SUBSET);
1333  (EXISTS_TAC `{X | X SUBSET ball (x:real^3, &8) /\ mcell_set V X}`);
1334  (STRIP_TAC);
1335  (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA_2);
1336  (ASM_REWRITE_TAC[]);
1337  (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
1338  (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]);
1339  (NEW_GOAL `VX V x'' = V INTER x''`);
1340  (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
1341  (UNDISCH_TAC `mcell_set V x''` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]);
1342  (STRIP_TAC);
1343  (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
1344  (ASM_REWRITE_TAC[IN]);
1345  (STRIP_TAC THEN UNDISCH_TAC `VX V x'' x`);
1346  (ASM_REWRITE_TAC[VX; MESON[IN] `{} x <=> x IN {}`] THEN SET_TAC[]);
1347  (NEW_GOAL `x'' SUBSET ball (x:real^3, &8)`);
1348  (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);
1349  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
1350  (ASM_SET_TAC[]);
1351  (ASM_SET_TAC[]);
1352  (ASM_REWRITE_TAC[]);
1353  (NEW_GOAL `&(CARD {X | mcell_set V X /\ VX V X x}) <= cc4`);
1354  (FIRST_ASSUM MATCH_MP_TAC);
1355  (ASM_REWRITE_TAC[]);
1356  (UNDISCH_TAC `x IN (T3:real^3->bool)` THEN EXPAND_TAC "T3");
1357  (SET_TAC[]);
1358  (ABBREV_TAC `s_temp = &(CARD {X | mcell_set V X /\ VX V X x})`);
1359  (ASM_REAL_ARITH_TAC);
1360  (NEW_GOAL `sum (S1:(real^3->bool)->bool) (\x. cc3) <= cc4 * cc3`);
1361  (ASM_REWRITE_TAC[]);
1362  (ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`]);
1363  (ONCE_REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
1364  (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
1365  (ASM_REAL_ARITH_TAC);
1366  (ASM_REAL_ARITH_TAC);
1367  (ABBREV_TAC `s_temp = sum (S1:(real^3->bool)->bool) (\x. cc3)`);
1368  (ASM_REAL_ARITH_TAC);
1369
1370
1371
1372  (NEW_GOAL `sum ((g:real^3->real^3->bool) x) (\x. cc4 * cc3) <= ss1`);
1373  (REWRITE_WITH
1374   `sum ((g:real^3->real^3->bool) x) (\x. cc4 * cc3) =
1375    &(CARD (g x)) * cc4 * cc3`);
1376  (MATCH_MP_TAC SUM_CONST);
1377  (EXPAND_TAC "g");
1378  (MATCH_MP_TAC FINITE_SUBSET);
1379  (EXISTS_TAC `T1:real^3->bool`);
1380  (STRIP_TAC);
1381  (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA);
1382  (ASM_REWRITE_TAC[]);
1383  (SET_TAC[]);
1384
1385  (NEW_GOAL `&(CARD ((g:real^3->real^3->bool) x)) <=
1386              &(CARD (V INTER ball (x:real^3, &3)))`);
1387  (REWRITE_TAC[REAL_OF_NUM_LE]);
1388  (MATCH_MP_TAC CARD_SUBSET);
1389  (STRIP_TAC);
1390  (EXPAND_TAC "g" THEN EXPAND_TAC "T1" THEN
1391    REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; IN_INTER; IN_BALL]);
1392  (REPEAT STRIP_TAC);
1393  (ASM_REWRITE_TAC[]);
1394  (NEW_GOAL `&2 * hplus < &3`);
1395  (REWRITE_TAC[hplus] THEN REAL_ARITH_TAC);
1396  (ASM_REAL_ARITH_TAC);
1397  (ASM_SIMP_TAC[FINITE_PACK_LEMMA]);
1398
1399  (EXPAND_TAC "ss1");
1400  (ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`]);
1401  (ONCE_REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
1402  (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
1403  (ONCE_REWRITE_TAC[GSYM (REAL_ARITH `a <= b <=> &0 <= b - a`)]);
1404  (NEW_GOAL `&(CARD (V INTER ball (x:real^3,&3))) <= &4 pow 3`);
1405  (REWRITE_TAC[REAL_ARITH `&4 = &3 + &1`]);
1406  (MATCH_MP_TAC BOUNDS_VGEN_klemma);
1407  (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
1408  (ASM_REAL_ARITH_TAC);
1409  (MATCH_MP_TAC REAL_LE_MUL);
1410  (ASM_REAL_ARITH_TAC);
1411
1412  (ASM_REAL_ARITH_TAC);
1413
1414  (EXPAND_TAC "g");
1415  (REWRITE_TAC[REAL_ARITH `&1 / &2 * x + a <= &0 <=> x <= &2 * (-- a)`]);
1416  (REWRITE_TAC[REAL_ARITH `c * r pow 2 + d * r pow 2 = (c + d) * r pow 2`]);
1417  (REWRITE_WITH `(c:real) + dd = -- ss`);
1418  (EXPAND_TAC "c");
1419  (REAL_ARITH_TAC);
1420  (REWRITE_TAC[REAL_ARITH `&2 * --(--ss * r pow 2) = &2 * ss * r pow 2`]);
1421  (NEW_GOAL `sum T3 (\n:real^3. ss1) <= &2 * ss * r pow 2`);
1422  (REWRITE_WITH `sum T3 (\n:real^3. ss1) = &(CARD (T3)) * ss1`);
1423  (MATCH_MP_TAC SUM_CONST);
1424  (MATCH_MP_TAC FINITE_SUBSET);
1425  (EXISTS_TAC `(V:real^3->bool) INTER ball (vec 0,r)`);
1426  (STRIP_TAC);
1427  (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
1428  (EXPAND_TAC "T3" THEN SET_TAC[]);
1429  (EXPAND_TAC "ss");
1430  (REWRITE_TAC[REAL_ARITH
1431    `&2 * (&1 / &2 * dd4 * ss1) * r pow 2 = (dd4 * r pow 2) * ss1`]);
1432  (ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`]);
1433  (ONCE_REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
1434  (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
1435  (ONCE_REWRITE_TAC[GSYM (REAL_ARITH `a <= b <=> &0 <= b - a`)]);
1436  (EXPAND_TAC "T3");
1437  (ONCE_REWRITE_TAC[SET_RULE `A INTER B DIFF C = A INTER B DIFF A INTER C`]);
1438
1439  (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`));
1440  (EXISTS_TAC `dd3 * r pow 2`);
1441  (STRIP_TAC);
1442  (FIRST_ASSUM MATCH_MP_TAC);
1443  (ASM_REWRITE_TAC[]);
1444  (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
1445  (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b ) * x`]);
1446  (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
1447  (ASM_REAL_ARITH_TAC);
1448  (REWRITE_TAC[REAL_LE_POW_2]);
1449  (EXPAND_TAC "ss1");
1450  (MATCH_MP_TAC REAL_LE_MUL);
1451  (STRIP_TAC);
1452  (ASM_REAL_ARITH_TAC);
1453  (MATCH_MP_TAC REAL_LE_MUL);
1454  (ASM_REAL_ARITH_TAC);
1455
1456  (REWRITE_WITH
1457  `sum T3 (\m:real^3. sum {n | n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus}
1458          (h m)) =
1459   sum T3 (\m. sum (g m) (h m))`);
1460  (EXPAND_TAC "g" THEN REWRITE_TAC[]);
1461  (ASM_REAL_ARITH_TAC);
1462
1463  (EXISTS_TAC `&0`);
1464  (REPEAT STRIP_TAC);
1465  (NEW_GOAL `F`);
1466  (UNDISCH_TAC `~(saturated V /\ packing V)` THEN ASM_REWRITE_TAC[]);
1467  (ASM_MESON_TAC[])]);;
1468
1469
1470 end;;