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