legacy/oldpacking/ky_packing/UPFZBZM_working.hl

   1
   2
   3 (* ========================================================================= *)
   4 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   5 (*                                                                           *)
   6 (*      Author   :  VU KHAC KY                                               *)
   7 (*      Book lemma: UPFZBZM                                                  *)
   8 (*      Chaper    : Packing (Clusters)                                       *)
   9 (*      Date      : October 3, 2010                                          *)
  10 (*                                                                           *)
  11 (* ========================================================================= *)
  12
  13 (* ========================================================================= *)
  14 (*                     FILES NEED TO BE LOADED                               *)
  15 (* ========================================================================= *)
  16
  17 (*
  18 Note: This file has very uncertain status -- T. Hales
  19 *)
  20
  21 (*
  22 needs "prove_by_refinement.hl";;
  23 needs "flyspeck_needs.hl";;
  24 needs "flyspeck_load.hl";;
  25 *)
  26
  27 flyspeck_needs "nonlinear/vukhacky_tactics.hl";;
  28 flyspeck_needs "packing/pack_defs.hl";;
  29 flyspeck_needs "packing/beta_pair_thm.hl";;
  30 flyspeck_needs "packing/pack_concl.hl";;
  31 flyspeck_needs "packing/pack1.hl";;
  32
  33
  34 module Upfzbzm_working = struct
  35
  36 open Pack_defs;;
  37 open Pack_concl;;
  38 open Vukhacky_tactics;;
  39 open Pack1;;
  40 (* open Prove_by_refinement;; *)
  41
  42
  43
  44 (*-------------------------------------------------------------------------- *)
  45
  46  let UPFZBZM_concl =
  47    `!V.  saturated V /\ packing V /\ cell_cluster_estimate V /\
  48          marchal_inequality /\
  49          lmfun_inequality V ==>
  50     (?G. negligible_fun_0 G V /\ fcc_compatible G V)`;;
  51
  52 (* ------------------------------------------------------------------------- *)
  53
  54 (* ========================================================================= *)
  55 (*             LIST OF THINGS THAT ARE UNPROVED                              *)
  56 (* ========================================================================= *)
  57
  58 let tau0_not_zero = new_axiom `~(tau0 = &0)`;;
  59 let ZERO_LT_MM2_LEMMA = new_axiom `&0 < mm2`;;
  60 let lmfun_vs_marchal = new_axiom
  61   `!h. ~(hminus <= h /\ h <= hplus)  ==> lmfun (h) >= marchal (h)`;;
  62 (* Tom said he will formalize 3 above axioms *)
  63
  64 (*
  65  let DIHX_POS = new_axiom `!u v V X. &0 <= dihX V X (u,v)`;;
  66      Note: Finished but there is a CHEAT_TAC left.
  67
  68  let FINITE_edgeX = new_axiom `!V X. FINITE (edgeX V X)`;;
  69      Note:  Finished
  70
  71  let FINITE_critical_edgeX = new_axiom `!V X. FINITE (critical_edgeX V X)`;;
  72      Note : Finished
  73 *)
  74
  75
  76 let FINITE_MCELL_SET_LEMMA = new_axiom
  77    `!V r. FINITE {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`;;
  78
  79   (* This will be formalized by using the fact that:
  80       -  each mcell has a vertex v IN V.
  81       - FINITE (B(0,r) INTER V)
  82    *)
  83
  84
  85 let KIZHLTL1 = new_axiom
  86  `!V. ?c. !r. saturated V /\ packing V /\ &1 <= r
  87    ==> sum {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X} vol +
  88        c * r pow 2 <=
  89        sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open  V u))`;;
  90
  91 let KIZHLTL2 = new_axiom
  92   `!V. ?c. !r. saturated V /\ packing V /\ &1 <= r
  93          ==> &(CARD (V INTER ball (vec 0,r))) * &8 * mm1 + c * r pow 2 <=
  94             (&2 * mm1 / pi) *
  95    sum {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X} (total_solid V)`;;
  96
  97 let KIZHLTL3 = new_axiom
  98 `!V f.
  99          ?c. !r. saturated V /\
 100                  packing V /\
 101                  &1 <= r /\
 102                  (?c1. !x. &2 <= x /\ x < sqrt (&8) ==> abs (f x) <= c1)
 103                  ==> (&8 * mm2 / pi) *
 104                      sum {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X}
 105                      (\X. sum (edgeX V X)
 106                           (\({u, v}). dihX V X (u,v) * f (hl [u; v]))) +
 107                      c * r pow 2 <=
 108                      &8 *
 109                      mm2 *
 110                      sum (V INTER ball (vec 0,r))
 111                      (\u. sum
 112                           {v | v IN V /\ ~(u = v) /\ dist (u,v) < sqrt (&8)}
 113                           (\v. f (hl [u; v])))`;;
 114
 115 (* 3 axioms above are parts of KIZHLTL. They will be proved in another file *)
 116
 117 let SUM_GAMMAX_LMFUM_ESTIMATE_concl =
 118   `!V. ?c. !r. saturated V /\ packing V /\ &1 <= r /\
 119                cell_cluster_estimate V /\ marchal_inequality /\
 120                lmfun_inequality V ==>
 121     c * r pow 2 <=  sum {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X}
 122     (\X. gammaX V X lmfun)`;;
 123
 124 let SUM_GAMMAX_LMFUM_ESTIMATE = new_axiom SUM_GAMMAX_LMFUM_ESTIMATE_concl;;
 125 (* This axiom is the most important thm here *)
 126
 127 let negligible_fun_any_C = new_axiom
 128    `!f S. negligible_fun_0 f S <=>
 129     (?C.  (!r. &1 <= r ==> sum (S INTER ball ((vec 0),r)) f <= C * r pow 2))`;;
 130 (* This is done in file "ky_lemma_negligible.hl" *)
 131
 132 (* In addition, there is 3 CHEAT_TAC that are used *)
 133
 134 (* ========================================================================= *)
 135
 136 let SUM_GAMMAX_LMFUM_ESTIMATE_concl =
 137   `!V. ?c. !r. saturated V /\ packing V /\ &1 <= r /\
 138                cell_cluster_estimate V /\ marchal_inequality /\
 139                lmfun_inequality V ==>
 140     c * r pow 2 <=  sum {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X}
 141     (\X. gammaX V X lmfun)`;;
 142
 143 (* ----------------------  We prove it below ------------------------------- *)
 144
 145 g SUM_GAMMAX_LMFUM_ESTIMATE_concl;;
 146 e (GEN_TAC);;
 147 e (EXISTS_TAC `c:real`);;
 148 e (REPEAT STRIP_TAC);;
 149
 150 e (SUBGOAL_THEN `!X. (critical_edgeX V X  = {}) ==>
 151      (!u v:real^3. {u, v} IN edgeX V X ==>
 152      lmfun (hl [u; v]) >= marchal (hl [u ; v]))`  ASSUME_TAC);;
 153 e (REPEAT STRIP_TAC);;
 154 e (SUBGOAL_THEN `~(hminus <= hl [u:real^3; v] /\ hl [u; v] <= hplus)`
 155    ASSUME_TAC);;
 156 e STRIP_TAC;;
 157 e (SUBGOAL_THEN `critical_edgeX V X {u, v}` ASSUME_TAC);;
 158 e (REWRITE_TAC[critical_edgeX]);;
 159 e (REWRITE_TAC[IN_ELIM_THM]);;
 160 e (EXISTS_TAC `u:real^3`);;
 161 e (EXISTS_TAC `v:real^3`);;
 162 e (ASM_REWRITE_TAC[]);;
 163 e (SUBGOAL_THEN `~ (critical_edgeX V X = {})` ASSUME_TAC);;
 164 e (UP_ASM_TAC);;
 165 e (SET_TAC[]);;
 166 e (ASM_MESON_TAC[]);;
 167 e (ASM_SIMP_TAC[lmfun_vs_marchal]);;
 168
 169 (*  We have already proved that :
 170
 171 !X. critical_edgeX V X = {}
 172           ==> (!u v.
 173                    {u, v} IN edgeX V X
 174                    ==> lmfun (hl [u; v]) >= marchal (hl [u; v]))
 175 *)
 176
 177 e (SUBGOAL_THEN
 178   `!X. mcell_set V X /\ (critical_edgeX V X  = {}) ==> gammaX V X lmfun >= &0` ASSUME_TAC);;
 179 e (REPEAT STRIP_TAC);;
 180 e (MATCH_MP_TAC (REAL_ARITH
 181   `a >= gammaX V X marchal /\ gammaX V X marchal >= &0 ==> a >= &0`));;
 182 e CONJ_TAC;;
 183
 184   (* break into 2 small part *)
 185
 186 e (REWRITE_TAC[gammaX]);;
 187 e (MATCH_MP_TAC (REAL_ARITH `a <= b ==> x - y + b >= x - y + a`));;
 188 e (MATCH_MP_TAC REAL_LE_LMUL);;
 189 e STRIP_TAC;;
 190 e (MATCH_MP_TAC REAL_LE_MUL);;
 191 e CONJ_TAC;;
 192 e REAL_ARITH_TAC;;
 193 e (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));;
 194 e (MATCH_MP_TAC REAL_LT_DIV);;
 195 e (REWRITE_TAC[PI_POS;ZERO_LT_MM2_LEMMA]);;
 196
 197 e (MATCH_MP_TAC SUM_LE);;
 198 e (REWRITE_TAC[FINITE_edgeX]);;
 199 e (REWRITE_TAC[edgeX;IN_ELIM_THM]);;
 200 e (REPEAT STRIP_TAC);;
 201 e (REWRITE_TAC[ASSUME `x = {u:real^3, v}`;BETA_THM]);;
 202
 203 e (REWRITE_WITH `(\({u, v}). dihX V X (u,v) * marchal (hl [u; v])) {u, v} =
 204                  dihX V X (u,v) * marchal (hl [u; v])`);;
 205 e (MATCH_MP_TAC BETA_PAIR_THM);;
 206
 207 e (REWRITE_TAC[HL;DIHX_SYM]);;
 208 e (REPEAT GEN_TAC);;
 209 e (REWRITE_WITH `set_of_list [u':real^3; v'] = set_of_list [v'; u']`);;
 210 e (REWRITE_TAC[set_of_list]);;
 211 e (SET_TAC[]);;
 212
 213 e (REWRITE_WITH `(\({u, v}). dihX V X (u,v) * lmfun (hl [u; v])) {u, v} =
 214                  dihX V X (u,v) * lmfun (hl [u; v])`);;
 215 e (MATCH_MP_TAC BETA_PAIR_THM);;
 216
 217 e (REWRITE_TAC[HL;DIHX_SYM]);;
 218 e (REPEAT GEN_TAC);;
 219 e (REWRITE_WITH `set_of_list [u':real^3; v'] = set_of_list [v'; u']`);;
 220 e (REWRITE_TAC[set_of_list]);;
 221 e (SET_TAC[]);;
 222
 223 e (MATCH_MP_TAC (REAL_ARITH `&0 <= a * ( y - x) ==> a * x <= a * y`));;
 224 e (MATCH_MP_TAC REAL_LE_MUL);;
 225 e STRIP_TAC;;
 226 e (REWRITE_TAC[DIHX_POS]);;
 227 e (MATCH_MP_TAC (REAL_ARITH `a >= b ==> &0 <= a - b`));;
 228 e (NEW_GOAL `{u, v} IN edgeX V X`);;
 229 e (ASM_REWRITE_TAC[edgeX]);;
 230 e (DEL_TAC THEN REPLICATE_TAC 3 UP_ASM_TAC THEN SET_TAC[]);;
 231 e (ASM_MESON_TAC[]);;
 232
 233 e (MP_TAC (ASSUME `marchal_inequality`));;
 234 e (REWRITE_TAC[marchal_inequality]);;
 235 e (DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC);;
 236 e (ASM_REWRITE_TAC[]);;
 237
 238 (* ------------------------------------------------------------------------ *)
 239
 240 e (ABBREV_TAC `B_0_r = {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X}`);;
 241 e (ABBREV_TAC `B_0_r_empty = B_0_r INTER {X| critical_edgeX V X = {}}`);;
 242 e (ABBREV_TAC `B_0_r_no_empty = B_0_r INTER {X| ~(critical_edgeX V X = {})}`);;
 243
 244 e (SUBGOAL_THEN
 245   `B_0_r:(real^3->bool)->bool = B_0_r_empty UNION B_0_r_no_empty` ASSUME_TAC);;
 246 e (EXPAND_TAC "B_0_r_empty");;
 247 e (EXPAND_TAC "B_0_r_no_empty");;
 248 e (EXPAND_TAC "B_0_r");;
 249 e (SET_TAC[]);;
 250 e (ASM_REWRITE_TAC[]);;
 251
 252 e (SUBGOAL_THEN `FINITE (B_0_r:(real^3->bool)->bool)` ASSUME_TAC);;
 253 e (EXPAND_TAC "B_0_r");;
 254 e (REWRITE_TAC[FINITE_MCELL_SET_LEMMA]);;
 255
 256 e (SUBGOAL_THEN `FINITE (B_0_r_empty:(real^3->bool)->bool)` ASSUME_TAC);;
 257 e (MATCH_MP_TAC FINITE_SUBSET);;
 258 e (EXISTS_TAC `(B_0_r:(real^3->bool)->bool)`);;
 259 e (ASM_REWRITE_TAC[]);;
 260 e (SET_TAC[]);;
 261
 262 e (SUBGOAL_THEN `FINITE (B_0_r_no_empty:(real^3->bool)->bool)` ASSUME_TAC);;
 263 e (MATCH_MP_TAC FINITE_SUBSET);;
 264 e (EXISTS_TAC `(B_0_r:(real^3->bool)->bool)`);;
 265 e (ASM_REWRITE_TAC[]);;
 266 e (SET_TAC[]);;
 267
 268 e (SUBGOAL_THEN `DISJOINT B_0_r_empty (B_0_r_no_empty:(real^3->bool)->bool)` ASSUME_TAC);;
 269 e (REWRITE_TAC[IN_DISJOINT]);;
 270 e (EXPAND_TAC "B_0_r_empty" THEN EXPAND_TAC "B_0_r_no_empty");;
 271 e (STRIP_TAC);;
 272 e (SUBGOAL_THEN `x IN {X | critical_edgeX V X = {}}` ASSUME_TAC);;
 273 e (DEL_TAC THEN UP_ASM_TAC THEN SET_TAC[]);;
 274 e (SUBGOAL_THEN `x IN {X | ~(critical_edgeX V X = {})}` ASSUME_TAC);;
 275 e (DEL_TAC THEN UP_ASM_TAC THEN SET_TAC[]);;
 276 e (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);;
 277
 278 e (REWRITE_WITH
 279   `sum (B_0_r_empty UNION B_0_r_no_empty) (\X. gammaX V X lmfun) =
 280    sum (B_0_r_empty) (\X. gammaX V X lmfun) +
 281    sum (B_0_r_no_empty) (\X. gammaX V X lmfun)`);;
 282 e (MATCH_MP_TAC SUM_UNION);;
 283 e (ASM_REWRITE_TAC[]);;
 284
 285 e (SUBGOAL_THEN `&0 <= sum B_0_r_empty (\X. gammaX V X lmfun)` ASSUME_TAC);;
 286 e (MATCH_MP_TAC SUM_POS_LE);;
 287 e STRIP_TAC;;
 288
 289     e (ASM_REWRITE_TAC[]);;
 290     e (EXPAND_TAC "B_0_r_empty");;
 291     e (EXPAND_TAC "B_0_r");;
 292     e (REWRITE_TAC[REAL_ARITH `&0 <= x <=> x >= &0`]);;
 293     e (MP_TAC (ASSUME
 294       `!X. mcell_set V X /\ critical_edgeX V X = {} ==>
 295         gammaX V X lmfun >= &0`));;
 296     e (SET_TAC[]);;
 297
 298 e (MATCH_MP_TAC (REAL_ARITH `x <= a /\ &0 <= b ==> x <= b + a`));;
 299 e (ASM_REWRITE_TAC[]);;
 300
 301 e (REWRITE_WITH
 302   `sum B_0_r_no_empty (\X. gammaX V X lmfun) =
 303    sum B_0_r (\X. (gammaX V X lmfun) *
 304    sum (critical_edgeX V X) (\e. critical_weight V X))`);;
 305 e (ASM_REWRITE_TAC[]);;
 306
 307 e (REWRITE_WITH
 308 `sum (B_0_r_empty UNION B_0_r_no_empty)
 309  (\X. gammaX V X lmfun * sum (critical_edgeX V X) (\e. critical_weight V X)) =
 310  sum B_0_r_empty
 311  (\X. gammaX V X lmfun * sum (critical_edgeX V X) (\e. critical_weight V X)) +
 312  sum B_0_r_no_empty
 313  (\X. gammaX V X lmfun * sum (critical_edgeX V X) (\e. critical_weight V X))`
 314 );;
 315 e (MATCH_MP_TAC SUM_UNION);;
 316 e (ASM_REWRITE_TAC[]);;
 317
 318 e (SUBGOAL_THEN
 319  `sum B_0_r_empty
 320   (\X. gammaX V X lmfun * sum (critical_edgeX V X)
 321   (\e. critical_weight V X)) = &0` ASSUME_TAC);;
 322 e (MATCH_MP_TAC SUM_EQ_0);;
 323 e (EXPAND_TAC "B_0_r_empty");;
 324 e (GEN_TAC THEN REWRITE_TAC[IN_INTER;IN_ELIM_THM]);;
 325 e (STRIP_TAC);;
 326 e (MATCH_MP_TAC (MESON[REAL_MUL_RZERO] `x = &0 ==> y * x = &0`));;
 327 e (MATCH_MP_TAC (MESON[SUM_CLAUSES] `x = {} ==> sum x f = &0`));;
 328 e (ASM_REWRITE_TAC[]);;
 329
 330
 331 e (ASM_REWRITE_TAC[REAL_ADD_LID]);;
 332 e (MATCH_MP_TAC (SUM_EQ));;
 333 e GEN_TAC;;
 334 e (EXPAND_TAC "B_0_r_no_empty" THEN EXPAND_TAC "B_0_r");;
 335 e (REWRITE_TAC[IN_INTER;IN_ELIM_THM]);;
 336 e DISCH_TAC;;
 337 e (MATCH_MP_TAC (MESON[REAL_MUL_RID] `x = &1 ==> y = y * x`));;
 338 e (REWRITE_TAC[critical_weight]);;
 339 e (SUBGOAL_THEN )
 340 e (SIMP_TAC[SUM_CONST]);;
 341 e (NEW_GOAL `FINITE (critical_edgeX V x)`);;
 342 e (ASM_SIMP_TAC[FINITE_critical_edgeX]);;
 343 e (ASM_SIMP_TAC[SUM_CONST]);;
 344 e (REWRITE_TAC[REAL_ARITH `a * &1 / a = (a * &1) / a`; REAL_MUL_RID]);;
 345 e (MATCH_MP_TAC REAL_DIV_REFL);;
 346 e (MATCH_MP_TAC (MESON[REAL_OF_NUM_EQ] `~(x = 0) ==> ~ (&x = &0)`));;
 347 e (UP_ASM_TAC THEN UP_ASM_TAC);;
 348 e (MESON_TAC[CARD_EQ_0]);;
 349
 350 (* ------------------------------------------------------------------------- *)
 351
 352 e (ABBREV_TAC
 353  `temp_set = {e:real^3->bool | (?X. X IN B_0_r /\ e IN critical_edgeX V X)}`);;
 354 e (SUBGOAL_THEN `FINITE (temp_set:(real^3->bool)->bool)` ASSUME_TAC);;
 355 e CHEAT_TAC;;
 356
 357   (* Used CHEAT_TAC here. But it seems to be easy *)
 358
 359 e (REWRITE_WITH
 360  `sum B_0_r
 361  (\X. gammaX V X lmfun *
 362       sum (critical_edgeX V X) (\e. critical_weight V X)) =
 363   sum B_0_r
 364  (\X. sum (critical_edgeX V X) (\e. gammaX V X lmfun * critical_weight V X))`);;
 365 e (REWRITE_TAC[GSYM SUM_LMUL]);;
 366
 367 e (REWRITE_WITH
 368  `sum B_0_r
 369  (\X. sum (critical_edgeX V X) (\e. gammaX V X lmfun * critical_weight V X)) =
 370   sum B_0_r
 371  (\X. sum {e | e IN temp_set /\ critical_edgeX V X e}
 372  (\e. gammaX V X lmfun * critical_weight V X))`);;
 373 e (MATCH_MP_TAC SUM_EQ);;
 374 e (GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[IN_ELIM_THM]);;
 375 e (MATCH_MP_TAC (MESON[] `(s = r) ==> sum s f = sum r f`));;
 376 e (REWRITE_TAC[SET_RULE
 377  `(X = Y) <=> (!x. (x IN X ==> x IN Y) /\ (x IN Y ==> x IN X))`]);;
 378 e (GEN_TAC THEN STRIP_TAC);;
 379 e (REWRITE_TAC[IN_ELIM_THM]);;
 380 e (REPEAT STRIP_TAC);;
 381 e (EXPAND_TAC "temp_set" THEN REWRITE_TAC[IN_ELIM_THM]);;
 382 e (EXISTS_TAC `x:real^3 -> bool`);;
 383 e (ASM_REWRITE_TAC[]);;
 384 e (UP_ASM_TAC THEN SET_TAC[]);;
 385 e (REWRITE_TAC[IN_ELIM_THM]);;
 386 e (SET_TAC[]);;
 387 e (REWRITE_WITH
 388  `sum B_0_r
 389   (\X. sum {e | e IN temp_set /\ critical_edgeX V X e}
 390       (\e. gammaX V X lmfun * critical_weight V X)) =
 391   sum temp_set
 392  (\e. sum {X | X IN B_0_r /\ critical_edgeX V X e}
 393       (\X. gammaX V X lmfun * critical_weight V X))`);;
 394 e (MATCH_MP_TAC SUM_SUM_RESTRICT);;
 395 e (ASM_REWRITE_TAC[]);;
 396
 397
 398
 399
 400
 401
 402
 403
 404
 405
 406
 407 e (REWRITE_WITH
 408 `sum temp_set
 409  (\e. sum {X | X IN B_0_r /\ critical_edgeX V X e}
 410       (\X. gammaX V X lmfun * critical_weight V X)) =
 411 sum temp_set
 412  (\e. sum {X | critical_edgeX V X e}
 413       (\X. gammaX V X lmfun * critical_weight V X))`);;
 414 e (MATCH_MP_TAC SUM_EQ);;
 415 e (EXPAND_TAC "temp_set");;
 416 e (REWRITE_TAC[IN_ELIM_THM]);;
 417 e (GEN_TAC THEN DISCH_TAC);;
 418 e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
 419 e (MATCH_MP_TAC SUM_EQ_SUPERSET);;
 420 e (REPEAT STRIP_TAC);;
 421 e (MATCH_MP_TAC FINITE_SUBSET);;
 422 e (EXISTS_TAC `{X:real^3->bool | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);;
 423
 424 e (EXPAND_TAC "B_0_r");;
 425  THEN REWRITE_TAC[FINITE_MCELL_SET_LEMMA]);;
 426 e (SET_TAC[]);;
 427 e (SET_TAC[]);;
 428 e (MESON_TAC[]);;
 429 e (UP_ASM_TAC THEN REWRITE_TAC[BETA_THM; IN_ELIM_THM]);;
 430
 431
 432 FINITE_critical_edgeX;;
 433 FINITE_MCELL_SET_LEMMA;;
 434 e ();;
 435
 436
 437
 438
 439 e CHEAT_TAC;;
 440 seans_fn();;
 441
 442
 443
 444
 445
 446
 447
 448
 449
 450
 451
 452
 453
 454
 455
 456
 457 (* ========================================================================== *)
 458
 459 g `!u v V X. dihX V X (u,v) = dihX V X (v,u)`;;
 460 e (REPEAT GEN_TAC);;
 461 e (REWRITE_TAC[dihX] THEN COND_CASES_TAC);;
 462 e (LET_TAC THEN COND_CASES_TAC);;
 463 e (MESON_TAC[]);;
 464 e (ASM_MESON_TAC[]);;
 465 e (REPEAT LET_TAC THEN COND_CASES_TAC);;
 466 e (REWRITE_TAC[dihX2]);;
 467 e (REPEAT LET_TAC);;
 468 e (REWRITE_WITH `ul':(real^3)list = ul''`);;
 469 e (UP_ASM_TAC THEN MESON_TAC[PAIR_EQ]);;
 470 e (REWRITE_TAC[DIHV_SYM]);;
 471 e COND_CASES_TAC;;
 472 e COND_CASES_TAC;;
 473 e (ASM_MESON_TAC[]);;
 474 e COND_CASES_TAC;;
 475 e (ASM_MESON_TAC[]);;
 476 e COND_CASES_TAC;;
 477 e (REWRITE_TAC[dihX3]);;
 478 e (REPEAT LET_TAC);;
 479 e (REWRITE_WITH `ul':(real^3)list = ul''`);;
 480 e (UP_ASM_TAC THEN MESON_TAC[PAIR_EQ]);;
 481 e (REWRITE_WITH `ul'':(real^3)list = ul`);;
 482 e (UNDISCH_TAC `k'',ul'' = (k:num),(ul:(real^3)list)` THEN MESON_TAC[PAIR_EQ]);;
 483 e (UNDISCH_TAC `cell_params V X = k'',ul''`);;
 484 e (REWRITE_TAC[cell_params]);;
 485 e (SUBGOAL_THEN `k'':num = k /\ ul'':(real^3)list = ul `ASSUME_TAC);;
 486 e (ASM_MESON_TAC[PAIR_EQ]);;
 487 e (SUBGOAL_THEN `k':num = k /\ ul':(real^3)list = ul `ASSUME_TAC);;
 488 e (ASM_MESON_TAC[PAIR_EQ]);;
 489 e (ASM_REWRITE_TAC[]);;
 490 e DISCH_TAC;;
 491 e (SIMP_TAC[SUM_SING]);;
 492
 493 e (NEW_GOAL
 494 `?p vl. {vl,p | p permutes {0, 1, 2} /\
 495                 vl = left_action_list p ul /\
 496                 v = EL 0 (vl:(real^3)list) /\
 497                 u = EL 1 vl} =
 498         {(vl,p)}`);;
 499 e (ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM;IN_SING]);;
 500 e (SIMP_TAC[GSYM KY_SING_SET_LEMMA]);;
 501
 502 e (ABBREV_TAC `p = (\k. if )`)
 503 e (EXISTS_TAC)
 504
 505 SET_RULE
 506
 507 let KY_SING_SET_LEMMA = prove (
 508  `(!y. P y <=> y = x) ==> {y | P y} = {x}`, REPEAT STRIP_TAC THEN
 509   ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM;IN_SING]);;
 510
 511 e (REWRITE)
 512
 513
 514 search [`x IN y`;`x IN z`];;
 515 search [`x IN {y}`];;
 516
 517 permutes;;
 518
 519 permutes;;
 520
 521
 522 seans_fn();;
 523
 524
 525 e CHEAT_TAC;;
 526
 527
 528
 529
 530
 531 dihX3;;
 532
 533 (* ------------------------------------------------------------------------- *)
 534 e (ASM_MESON_TAC[]);;
 535 e COND_CASES_TAC;;
 536 e COND_CASES_TAC;;
 537 e (ASM_MESON_TAC[]);;
 538 e COND_CASES_TAC;;
 539 e (ASM_MESON_TAC[]);;
 540 e COND_CASES_TAC;;
 541 e (ASM_MESON_TAC[]);;
 542 e COND_CASES_TAC;;
 543 e (REWRITE_TAC[dihX4]);;
 544 e (REPEAT LET_TAC);;
 545 e (REWRITE_TAC[REAL_EQ_MUL_LCANCEL]);;
 546 e DISJ2_TAC;;
 547 e CHEAT_TAC;;
 548
 549
 550 (* ------------------------------------------------------------------------- *)
 551 e (ASM_MESON_TAC[]);;
 552 e COND_CASES_TAC;;
 553 e (MESON_TAC[]);;
 554 e COND_CASES_TAC;;
 555 e (ASM_MESON_TAC[]);;
 556 e COND_CASES_TAC;;
 557 e (ASM_MESON_TAC[]);;
 558 e COND_CASES_TAC;;
 559 e (ASM_MESON_TAC[]);;
 560 e (MESON_TAC[]);;
 561
 562
 563 search [`c * a = c * b`];;
 564 SUM_EQ;;
 565
 566
 567
 568 let FINITE_MCELL_SET_LEMMA = new_axiom
 569
 570 g  `!V r. FINITE {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`;;
 571 e (REPEAT STRIP_TAC);;
 572 e (REWRITE_TAC[mcell_set]);;
 573
 574
 575 seans_fn();;
 576
 577
 578 open Sphere;;
 579
 580 let EMNWUUS1 = new_axiom EMNWUUS1_concl;;
 581 let EMNWUUS2 = new_axiom EMNWUUS2_concl;;
 582
 583 INTER;;
 584
 585
 586
 587 g `!V X p r. packing V /\ saturated V /\ mcell_set V X /\
 588         ~(X INTER ball (p,r) = {}) ==> X SUBSET (ball (p, r + &3))`;;
 589 e (REWRITE_TAC[GSYM MEMBER_NOT_EMPTY;SUBSET;ball;IN_ELIM_THM;INTER]);;
 590 e (REPEAT STRIP_TAC);;
 591 e (MATCH_MP_TAC(REAL_ARITH
 592   `dist (p,x) < r /\
 593    dist (x,x') <= &3 /\
 594    dist (p,x') <= dist (p,x) + dist (x,x') ==>
 595    dist (p,x') < r + &3 `));;
 596 e (REPEAT STRIP_TAC);;  (* 3 subgoals *)
 597   (* Subgoal 1 *)
 598 e (ASM_REWRITE_TAC[]);;  (* Finish first subgoal *)
 599   (* Subgoal 2 *)
 600
 601 e (UNDISCH_TAC `mcell_set V X`);;
 602 e (REWRITE_TAC[mcell_set;IN_ELIM_THM;mcell]);;
 603 e (REPEAT STRIP_TAC);;
 604 e (UP_ASM_TAC THEN UP_ASM_TAC THEN REPEAT COND_CASES_TAC);;
 605 (* Break into more 5 subgoals *)
 606
 607 e (REWRITE_TAC[mcell0] THEN REPEAT DISCH_TAC);;
 608 e (NEW_GOAL `~affine_dependent (set_of_list (ul:(real^3)list))`);;
 609 e (UP_ASM_TAC THEN REWRITE_TAC[IN;IN_ELIM_THM;BARV]);;
 610 VORONOI_NONDG;;
 611
 612
 613
 614
 615
 616 (*-------------------- The lemma about sum of beta_bump ---------------------*)
 617
 618
 619 g `!V X. saturated V /\ packing V /\ mcell_set V X ==>
 620          sum {e | e IN critical_edgeX V X } (\e. beta_bump V e X) = &0`;;
 621 e (REPEAT STRIP_TAC THEN UP_ASM_TAC);;
 622 e (REWRITE_TAC[mcell_set; IN_ELIM_THM]);;
 623 e (DISCH_TAC);;
 624 e (REWRITE_TAC[beta_bump]);;
 625 e (REPEAT LET_TAC);;
 626 e (ASM_CASES_TAC `~(k = 4)`);;
 627
 628    (* Two case. Here is CASE 1*)
 629
 630 e (NEW_GOAL `!e. sum
 631       {e',e'',p,vl | k = 4 /\
 632                      critical_edgeX V X = {e', e''} /\
 633                      e = e' /\
 634                      p permutes 0..3 /\
 635                      vl = left_action_list p ul /\
 636                      e' = {EL 0 vl, EL 1 vl} /\
 637                      e'' = {EL 2 vl, EL 3 vl}}
 638       (\(e',e'',p,vl). (bump (hl [EL 0 vl; EL 1 vl]) -
 639                         bump (hl [EL 2 vl; EL 3 vl])) /
 640                        &4) = &0`);;
 641 e GEN_TAC;;
 642 e (ABBREV_TAC `SET1 = {e',e'',p,vl | k = 4 /\
 643                     critical_edgeX V X = {e', e''} /\
 644                     e = e' /\
 645                     p permutes 0..3 /\
 646                     vl = left_action_list p ul /\
 647                     e' = {EL 0 vl, EL 1 vl} /\
 648                     e'' = {EL 2 vl, EL 3 vl}}`);;
 649
 650 e (NEW_GOAL
 651   `SET1:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->bool = {}`);;
 652 e (EXPAND_TAC "SET1");;
 653 e (MP_TAC (ASSUME `~(k = 4)`));;
 654 e (SET_TAC[]);;
 655 e (ASM_REWRITE_TAC[]);;
 656 e (ASM_REWRITE_TAC[SUM_CLAUSES]);;
 657 e (ASM_REWRITE_TAC[SUM_0]);;
 658
 659   (* Here is case 2 *)
 660
 661 e (NEW_GOAL `k = 4`);;
 662 e (UP_ASM_TAC THEN MESON_TAC[]);;
 663 e (SWITCH_TAC THEN DEL_TAC);;
 664 e (SWITCH_TAC);;
 665 e (UP_ASM_TAC THEN REWRITE_TAC[cell_params]);;
 666 e DISCH_TAC;;
 667
 668 (* ------------------------------------------------------------------------ *)
 669
 670 e (NEW_GOAL `k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul`);;
 671 e (NEW_GOAL ` (?k ul. k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul) /\ ((@(k,ul). k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul) = k,ul)`);;
 672 e (ASM_REWRITE_TAC[]);;
 673 e (CHOOSE_TAC (ASSUME `?i ul. X = mcell i V ul /\ ul IN barV V 3`));;
 674 e (CHOOSE_TAC (ASSUME `?ul. X = mcell i V ul /\ ul IN barV V 3`));;
 675 e (ASM_CASES_TAC `i <= 4`);;
 676 e (EXISTS_TAC `i:num`);;
 677 e (EXISTS_TAC `ul':(real^3) list`);;
 678 e (ASM_REWRITE_TAC[]);;
 679
 680 e (EXISTS_TAC `4`);;
 681 e (EXISTS_TAC `ul':(real^3) list`);;
 682 e (ASM_REWRITE_TAC[ARITH_RULE `4 <= 4`]);;
 683 e (REWRITE_TAC[mcell]);;
 684 e (COND_CASES_TAC);;
 685 e (UP_ASM_TAC THEN UP_ASM_TAC);;
 686 e (MESON_TAC[ARITH_RULE `~(i <= 4) ==> (i = 0) ==> F`]);;
 687 e (DEL_TAC);;
 688 e (COND_CASES_TAC);;
 689 e (UP_ASM_TAC THEN UP_ASM_TAC);;
 690 e (MESON_TAC[ARITH_RULE `~(i <= 4) ==> (i = 1) ==> F`]);;
 691 e (DEL_TAC);;
 692 e (COND_CASES_TAC);;
 693 e (UP_ASM_TAC THEN UP_ASM_TAC);;
 694 e (MESON_TAC[ARITH_RULE `~(i <= 4) ==> (i = 2) ==> F`]);;
 695 e (DEL_TAC);;
 696 e (COND_CASES_TAC);;
 697 e (UP_ASM_TAC THEN UP_ASM_TAC);;
 698 e (MESON_TAC[ARITH_RULE `~(i <= 4) ==> (i = 3) ==> F`]);;
 699 e (DEL_TAC);;
 700 e (COND_CASES_TAC);;
 701 e (UP_ASM_TAC THEN MESON_TAC[ARITH_RULE `4 = 0 ==> F`]);;
 702 e (COND_CASES_TAC);;
 703 e (UP_ASM_TAC THEN MESON_TAC[ARITH_RULE `4 = 1 ==> F`]);;
 704 e (COND_CASES_TAC);;
 705 e (UP_ASM_TAC THEN MESON_TAC[ARITH_RULE `4 = 2 ==> F`]);;
 706 e (COND_CASES_TAC);;
 707 e (UP_ASM_TAC THEN MESON_TAC[ARITH_RULE `4 = 3 ==> F`]);;
 708 e (REWRITE_TAC[]);;
 709 e (UP_ASM_TAC);;
 710
 711 e (ABBREV_TAC `P = (\k. k <= 4)`);;
 712 e (ABBREV_TAC `Q = (\ul. ul IN barV V 3)`);;
 713 e (ABBREV_TAC `R = (\k ul. X = mcell k V ul)`);;
 714
 715 e (REWRITE_WITH
 716 `(?k ul. k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul) /\
 717  (@(k,ul). k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul) = k,ul
 718  ==> k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul <=>
 719  (?k ul. P k /\ Q ul /\ R k ul) /\ (@(k,ul). P k /\ Q ul /\ R k ul) = k,ul
 720  ==> P k /\ Q ul /\ R k ul`);;
 721 e (EXPAND_TAC "P" THEN EXPAND_TAC "Q" THEN EXPAND_TAC "R");;
 722 e (REWRITE_TAC[IN_ELIM_THM]);;
 723 e (REWRITE_TAC[JOHN_SELECT_THM]);;
 724
 725 e (UP_ASM_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN DEL_TAC THEN REPEAT STRIP_TAC);;
 726 e (UP_ASM_TAC THEN UP_ASM_TAC THEN DEL_TAC THEN REPEAT STRIP_TAC);;
 727 e (REWRITE_WITH `{e | e IN critical_edgeX V X} = critical_edgeX V X`);;
 728 e (SET_TAC[]);;
 729
 730 (* ------------------------------------------------------------------------- *)
 731
 732 e (ASM_CASES_TAC
 733  `?(ed:real^3->bool) ed'. ~ (ed = ed') /\ critical_edgeX V X = {ed , ed'}`);;
 734 e (FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC);;
 735 e (UP_ASM_TAC THEN STRIP_TAC);;
 736 e (ASM_REWRITE_TAC[]);;
 737 e (ASM_SIMP_TAC[SUM_SET_OF_2_ELEMENTS]);;
 738
 739
 740 e (NEW_GOAL
 741 `{e',e'',p,vl | {ed, ed'} = {e', e''} /\
 742                 ed' = e' /\
 743                 p permutes 0..3 /\
 744                 vl = left_action_list p ul /\
 745                 e' = {EL 0 vl, EL 1 vl} /\
 746                 e'' = {EL 2 vl, EL 3 vl}}
 747 = {ed',ed:real^3->bool,p,vl |  p permutes 0..3 /\
 748                 vl = left_action_list p ul /\
 749                 ed' = {EL 0 vl, EL 1 vl} /\
 750                 ed = {EL 2 vl, EL 3 vl}}`);;
 751 e (REWRITE_TAC[EXTENSION;IN;IN_ELIM_THM] THEN GEN_TAC THEN REPEAT STRIP_TAC);;
 752 e (EQ_TAC);;
 753 e (REPEAT STRIP_TAC);;
 754 e (EXISTS_TAC `ed':real^3->bool` THEN EXISTS_TAC `ed:real^3->bool`);;
 755 e (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`);;
 756 e (NEW_GOAL `ed':real^3->bool = e' /\ ed:real^3->bool = e''`);;
 757 e (ASM_SET_TAC[]);;
 758 e (REPEAT STRIP_TAC);;
 759 e (ASM_REWRITE_TAC[]);;
 760 e (ASM_REWRITE_TAC[]);;
 761 e (ASM_MESON_TAC[]);;
 762 e (REWRITE_TAC[ASSUME `x :(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list
 763                        = e', e'', p, vl`]);;
 764 e (REWRITE_TAC[PAIR_EQ]);;
 765 e (ASM_REWRITE_TAC[]);;
 766
 767
 768 e (REPEAT STRIP_TAC);;
 769 e (EXISTS_TAC `ed'':real^3->bool` THEN EXISTS_TAC `ed''':real^3->bool`);;
 770 e (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`);;
 771 e (REPEAT STRIP_TAC);;
 772
 773
 774 e (SET_TAC[]);;
 775 e (REWRITE_TAC[]);;
 776 e (ASM_MESON_TAC[]);;
 777 e (ASM_MESON_TAC[]);;
 778
 779
 780 e (REWRITE_TAC[ASSUME `x :(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list
 781                        = e', e'', p, vl`]);;
 782 e (REWRITE_TAC[PAIR_EQ]);;
 783 e (ASM_REWRITE_TAC[]);;
 784
 785 seans_fn();;
 786 e ()
 787
 788 e (EXISTS_TAC `ed':real^3->bool` THEN EXISTS_TAC `ed:real^3->bool`);;
 789 e (NEW_GOAL `?(vl:(real^3)list).
 790               ed' = {EL 0 vl, EL 1 vl} /\ ed = {EL 2 vl, EL 3 vl}`);;
 791 e (NEW_GOAL `?ed1:real^3 ed2. ed = {ed1, ed2}`);;
 792 e (NEW_GOAL `critical_edgeX V X ed`);;
 793 e (UP_ASM_TAC THEN SET_TAC[]);;
 794 e (UP_ASM_TAC THEN REWRITE_TAC[critical_edgeX;IN_ELIM_THM]);;
 795 e (MESON_TAC[]);;
 796 e (FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC);;
 797
 798 e (NEW_GOAL `?ed1':real^3 ed2'. ed' = {ed1', ed2'}`);;
 799 e (NEW_GOAL `critical_edgeX V X ed'`);;
 800 e (UP_ASM_TAC THEN SET_TAC[]);;
 801 e (UP_ASM_TAC THEN REWRITE_TAC[critical_edgeX;IN_ELIM_THM]);;
 802 e (MESON_TAC[]);;
 803 e (FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC);;
 804
 805 e (EXISTS_TAC `[ed1':real^3;ed2';ed1;ed2]`);;
 806 e (ASM_REWRITE_TAC[EL_0;EL_1;EL_2;EL_3]);;
 807 e (FIRST_X_ASSUM CHOOSE_TAC);;
 808 e (EXISTS_TAC `vl:(real^3)list`);;
 809
 810 e (NEW_GOAL `?p. p permutes 0..3 /\
 811                 (vl:(real^3)list) = left_action_list p ul`);;
 812 e CHEAT_TAC;;
 813 e (FIRST_X_ASSUM CHOOSE_TAC);;
 814 e (EXISTS_TAC `p:num->num`);;
 815 e (REWRITE_TAC[EXTENSION;IN;IN_ELIM_THM] THEN GEN_TAC THEN REPEAT STRIP_TAC);;
 816 e (EQ_TAC);;
 817 e (REPEAT STRIP_TAC);;
 818  THEN REWRITE_TAC [SET_RULE `{y} x <=> y = x`]);;
 819 e (REWRITE_TAC[ASSUME ]);;
 820 e (REWRITE_TAC[PAIR_EQ]);;
 821 e (NEW_GOAL `ed' = (e':real^3->bool) /\ (ed:real^3->bool) = e''`);;
 822 e (ASM_SET_TAC[]);;
 823 e (REPEAT STRIP_TAC);;
 824 e (ASM_MESON_TAC[]);;
 825 e (ASM_MESON_TAC[]);;
 826 e (NEW_GOAL `vl:(real^3)list = vl':(real^3)list`);;
 827
 828
 829 e (ASM_SET_TAC[]);;
 830
 831 seans_fn();;
 832 e (EXISTS_TAC `(\x:real^3. if x = (EL 0 (ul:(real^3)list))  then (EL 0 vl) else if x = (EL 1 ul) then (EL 1 vl) else if x = (EL 2 ul)  then (EL 2 vl) else (EL 3 vl))`);;
 833 e (REWRITE_TAC[left_action_list]);;
 834 inverse;;
 835
 836
 837
 838
 839 ARITH_RULE `3 = SUC 2 /\ 2 = SUC 1/\ 1 = SUC 0`;EL;HD]);;
 840 e (REWRITE_TAC[EL;ARITH_RULE `2 = SUC 1`]);;
 841 e (REWRITE_TAC[EL;ARITH_RULE `1 = SUC 0`]);;
 842 TL;;
 843  /\ 2 = SUC 1 /\ 1 = SUC 0`]);;
 844 EL;;
 845
 846 let EL_0 = prove (`!a b c d. EL 0 [a;b;c;d] = a`, REWRITE_TAC[EL;HD]);;
 847
 848 let EL_1 = prove (`!a b c d. EL 1 [a;b;c;d] = b`,
 849            REWRITE_TAC[EL;ARITH_RULE `1 = SUC 0`;TL;HD]);;
 850 let EL_2 = prove (`!a b c d. EL 2 [a;b;c;d] = c`,
 851            REWRITE_TAC[EL;ARITH_RULE `2 = SUC 1 /\ 1 = SUC 0`;TL;HD;EL_1]);;
 852 let EL_3 = prove (`!a b c d. EL 3 [a;b;c;d] = d`, REWRITE_TAC
 853            [EL;ARITH_RULE `3 = SUC 2 /\ 2 = SUC 1 /\ 1 = SUC 0 `;TL;HD;EL_2]);;
 854
 855 critical_edgeX;;
 856
 857
 858
 859
 860
 861
 862
 863
 864
 865
 866 e (MATCH_MP_TAC SING_SET_KY_LEMMA);;
 867
 868                   {ed, ed'} = {e', e''} /\
 869                     ed' = e' /\
 870                     p permutes 0..3 /\
 871                     vl = left_action_list p ul /\
 872                     e' = {EL 0 vl, EL 1 vl} /\
 873                     e'' = {EL 2 vl, EL 3 vl}`);;
 874
 875 e CHEAT_TAC;;
 876 e (NEW_GOAL
 877   `?y. {(e':real^3->bool,e'',p,vl)| {ed, ed'} = {e', e''} /\
 878                     ed' = e' /\
 879                     p permutes 0..3 /\
 880                     vl = left_action_list p ul /\
 881                     e' = {EL 0 vl, EL 1 vl} /\
 882                     e'' = {EL 2 vl, EL 3 vl}} = {y}`);;
 883
 884 e (ASM_MESON_TAC[SING_SET_KY_LEMMA]);;
 885 SING_SET_KY_LEMMA;;
 886
 887
 888  THEN SET_TAC[]);;
 889 e (ASM_SET_TAC[]);;
 890
 891 EXISTS_PAIRED_THM;;
 892
 893
 894 (*
 895 g `!P. (?! y:A. P y) ==> (?y. {x| P x} = {y})`;;
 896
 897 e (REWRITE_TAC[EXISTS_UNIQUE] THEN REPEAT STRIP_TAC);;
 898 e (EXISTS_TAC `y:A` THEN REWRITE_TAC[EXTENSION;IN;IN_ELIM_THM] THEN GEN_TAC);;
 899 e (EQ_TAC);;
 900 e (SET_TAC[]);;
 901 e (REWRITE_TAC [SET_RULE `{y} x <=> y = x`]);;
 902 e (ASM_MESON_TAC[]);;
 903 let SING_SET_KY_LEMMA = top_thm();;
 904
 905 *)
 906
 907
 908
 909
 910
 911  let john_harrison_lemma1 = prove
 912   (`(\(x,y). P x y) = (\p. P (FST p) (SND p))`,
 913    REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM]);;
 914
 915  let john_harrison_lemma2 = MESON[] `(?x. P x) /\ (@x. P x) = a ==> P a`;;
 916
 917  let JOHN_SELECT_THM = prove
 918   (`(?x y. P x /\ Q y /\ R x y) /\
 919     (@(x,y). P x /\ Q y /\ R x y) = (a,b)
 920     ==> P a /\ Q b /\ R a b`,
 921    REWRITE_TAC[GSYM EXISTS_PAIRED_THM] THEN
 922    REWRITE_TAC[john_harrison_lemma1] THEN
 923    DISCH_THEN(MP_TAC o MATCH_MP john_harrison_lemma2) THEN
 924    REWRITE_TAC[FST; SND]);;
 925
 926
 927
 928
 929
 930 SET_1
 931
 932 search [`x = {a}`];;
 933
 934 SET_RULE
 935 SUM_SUB;;
 936 seans_fn();;
 937 critical_edgeX;;
 938
 939
 940 e CHEAT_TAC;;
 941
 942
 943 (* -------------------------------------------------------*)
 944
 945 e (MATCH_MP_TAC SUM_EQ_0);;
 946 e (GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[IN_ELIM_THM]);;
 947 e (NEW_GOAL `! e e'. (e = e') \/ ~(critical_edgeX V X = {e, e'})`);;
 948 e (ASM_MESON_TAC[]);;
 949 e (MATCH_MP_TAC SUM_EQ_0);;
 950 e (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM]);;
 951 e (STRIP_TAC);;
 952 e (ASM_REWRITE_TAC[IN_ELIM_THM]);;
 953 e (MATCH_MP_TAC (REAL_ARITH `a = &0 ==> a / &4 = &0`));;
 954 e (MATCH_MP_TAC (REAL_ARITH `a = b ==> a - b = &0`));;
 955 e (AP_TERM_TAC);;
 956 e (REWRITE_TAC[HL]);;
 957 e (AP_TERM_TAC);;
 958 e (REWRITE_WITH `!a:real^3 b. set_of_list[a;b] = {a, b}`);;
 959 e (MESON_TAC[set_of_list]);;
 960 e (REWRITE_TAC[GSYM
 961   (ASSUME `vl:(real^3)list = left_action_list (p:num->num) ul`)]);;
 962 e (SUBGOAL_THEN `e':real^3->bool = e''`ASSUME_TAC);;
 963 e (ASM_MESON_TAC[]);;
 964 e (ASM_MESON_TAC[]);;
 965
 966 let SUM_BETA_BUMP_LEMMA = top_thm();;
 967
 968
 969 end;;