text_formalization/leg/geomdetail.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Lemmas in Geometry                                         *)
   5 (* Author: NGUYEN QUANG TRUONG                                              *)
   6 (* Date: 2010-02-09                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10 (*
  11
  12 Note: 2010-02-07.  This file was written for the pre-2009 version of the proof of the Kepler
  13 conjecture.  Various things from this file are no longer needed.  For now, we load it,
  14 because some proofs from collect_geom.hl rely on this file.
  15
  16 Eventually this file should be pruned down to what is really needed.
  17
  18 voronoi_trg -> voronoi_
  19 conv -> (hull) convex
  20 aff -> (hull) affine
  21 dist3 -> dist
  22 convex_trg -> (hull) convex
  23 simplex -> geomdetail'simplex renamed.
  24 deprecated: t0, voronoi2, voro2, center_pac, centered_pac, quasi_tri, quasi_reg_tet,
  25 quarter, diagonal, strict_qua, strict_qua2, quartered_oct, ... (many others.)
  26
  27
  28 -THALES
  29
  30 Feb 18, 2013 some lemmas were deleted that were not needed, svn1626.
  31 *)
  32
  33
  34 flyspeck_needs "general/sphere.hl";;
  35
  36 module Geomdetail (* : Geomdetail_type *) = struct
  37
  38   let packing = Sphere.packing;;
  39   let voronoi_open = Sphere.voronoi_open;;
  40
  41
  42 (* ================================ *)
  43 (* ===== NGUYEN QUANG TRUONG ====== *)
  44
  45
  46
  47 (*
  48
  49 Note:  I have split the file into 2 pieces: geomdetail.ml and geomdetail_08.ml.  Not everything in geomdetail_08.ml loads with the Multivariate directory, but these are the parts that are least likely to be used in the revision of the proof in 2009. Everything in this file now loads with Multivariate. --tch July 14, 2009
  50
  51 *)
  52 let near = new_definition ` near (v0:real^N) (r:real) s = { x | x IN s /\
  53   dist(x,v0) < r } `;;
  54
  55 (*
  56 let voronoi_trg = new_definition ` voronoi_trg v S = { x | !w. ((S w) /\ ~(w=v))
  57 ==> (dist ( x , v ) < dist ( x , w )) }`;;
  58 *)
  59
  60 let conv0_2 = new_definition ` conv0_2 s = conv0 s `;;
  61
  62 let convex = new_definition `convex s <=> !x y u v. x IN s /\ y IN s /\ &0 <= u /\
  63      &0 <= v /\ (u + v = &1) ==> (u % x + v % y) IN s`;;
  64
  65 let aff = new_definition `aff = ( hull ) affine`;;
  66
  67 let conv_trg = new_definition ` conv_trg s = convex hull s`;;
  68
  69 let border = new_definition ` border s = { x | ! ep. ep > &0 /\ ( ? a b. ~ (b IN s ) /\
  70  dist (b, x) < ep /\ a IN s /\ dist (a, x) < ep ) }`;;
  71
  72 let packing_trg = new_definition `packing_trg (s:real^3 -> bool) = (! x y.  s x /\ s y /\ ( ~(x=y))
  73   ==> dist ( x, y) >= &2 ) `;;
  74
  75 let center_pac = new_definition ` center_pac s v = ( packing_trg s /\ s v )`;;
  76
  77 let centered_pac = new_definition ` centered_pac s v = ( packing s /\ v IN s )`;;
  78
  79 let dist3 = new_definition ` dist3 (x:real^3) y = dist (x,y)`;;
  80
  81 (* let voronoi2 = new_definition ` voronoi2 v S = {x| x IN voronoi_trg v S /\ dist3 x v < &2 }`;; *)
  82
  83 (* let voro2 = new_definition ` voro2 v s = {x| x IN voronoi_open s v /\ dist3 x v < &2 }`;; *)
  84
  85 (*
  86 removed 2013-07-27:
  87 let t0 = new_definition ` t0 = #1.255`;;
  88
  89 let quasi_tri = new_definition ` quasi_tri tri s = ( packing s /\
  90   tri SUBSET s /\
  91   (? a b c. ~( a=b \/ b=c\/ c=a) /\  { a, b, c } = tri ) /\
  92   (! x y.  ( x IN tri /\ y IN tri /\ (~(x=y)) ) ==> ( dist3 x y <= &2 * t0 )))`;;
  93
  94 *)
  95
  96 let simplex = new_definition ` geomdetail'simplex (d:real^3 -> bool) s = ( packing s /\
  97   d SUBSET s /\
  98 ( ? v1 v2 v3 v4. ~( v1 = v2 \/ v3 = v4 ) /\ {v1, v2 } INTER {v3, v4 } = {}/\ {v1,v2,v3,v4} = d )
  99  )`;;
 100
 101 (*
 102 let quarter = new_definition ` quarter (q:real^3 -> bool) s =
 103   ( packing s /\
 104          geomdetail'simplex q s /\
 105          (?v w.
 106               v IN q /\
 107               w IN q /\
 108               &2 * t0 <= dist3 v w /\
 109               dist3 v w <= sqrt (&8) /\
 110               (!x y.
 111                    x IN q /\ y IN q /\ ~({x, y} = {v, w})
 112                    ==> dist3 x y <= &2 * t0)))`;;
 113 *)
 114
 115 (*
 116
 117 let quasi_reg_tet = new_definition ` quasi_reg_tet x s = ( geomdetail'simplex x s /\
 118    (! v w. ( v IN x /\ w IN x /\
 119     ( ~ ( v = w)))
 120   ==> ( dist3 v w <= &2 * t0 )) )`;;
 121
 122
 123 let diagonal = new_definition ` diagonal d1 d2 q s = ( quarter q s /\
 124          {d1, d2} SUBSET q /\
 125          (!x y. x IN q /\ y IN q ==> dist3 x y <= dist3 d1 d2))`;;
 126
 127
 128  let strict_qua = new_definition ` strict_qua d s = ( quarter d s /\
 129   ( ? x y. x IN d /\ y IN d /\ &2 * t0 < dist3 x y /\ dist3 x y < sqrt( &8 ) ))`;;
 130
 131 let strict_qua2 = new_definition ` strict_qua2 d (ch:real^3 -> bool ) s = ( quarter d s /\ ch SUBSET d
 132   /\ ( ? x y. ~( x = y ) /\ ch = {x,y} /\ &2 * t0 < dist3 x y /\ dist3 x y < sqrt ( &8 ) ) )`;;
 133
 134
 135
 136
 137 let quartered_oct = new_definition `quartered_oct  (v:real^3)  (w:real^3) (v1:real^3)  (v2:real^3)  (v3:real^3)  (v4:real^3)  s =
 138          ( packing s /\
 139          ( &2 * t0 < dist (v,w) /\ dist (v,w) < sqrt (&8) ) /\
 140          (!x. x IN {v1, v2, v3, v4}
 141               ==> dist (x,v) <= &2 * t0 /\ dist (x,w) <= &2 * t0) /\
 142          {v, w, v1, v2, v3, v4} SUBSET s /\
 143          (&2 <= dist (v1,v2) /\ dist (v1,v2) <= &2 * t0) /\
 144          (&2 <= dist (v2,v3) /\ dist (v2,v3) <= &2 * t0) /\
 145          (&2 <= dist (v3,v4) /\ dist (v3,v4) <= &2 * t0) /\
 146          &2 <= dist (v4,v1) /\
 147          dist (v4,v1) <= &2 * t0 ) `;;
 148
 149 let adjacent_pai = new_definition ` adjacent_pai v v1 v3 v2 v4 s = ( strict_qua2 { v , v1 , v3 , v2 } { v1 , v3 } s
 150   /\ strict_qua2 { v , v1 , v3 , v4 } { v1 , v3 } s /\
 151   ( conv0 { v , v1 , v3 , v2 } INTER conv0 { v , v1 , v3 , v4 } = {} ) )`;;
 152
 153
 154 let conflicting_dia = new_definition ` conflicting_dia v v1 v3 v2 v4 s = ( adjacent_pai v v1 v3 v2 v4 s
 155 /\ adjacent_pai v v2 v4 v1 v3 s )`;;
 156
 157
 158  let interior_pos = new_definition `interior_pos v v1 v3 v2 v4 s = ( conflicting_dia v v1 v3 v2 v4 s
 159   /\ ~( conv0 { v1, v3 } INTER conv0 { v , v2 , v4 } = {} ))`;;
 160
 161 let isolated_qua = new_definition ` isolated_qua q s = ( quarter q s /\ ~( ? v v1 v2 v3 v4. q =
 162   {v, v1, v2, v3} /\ adjacent_pai v v1 v2 v3 v4 s))`;;
 163
 164 let isolated_pai = new_definition ` isolated_pai q1 q2 s = ( isolated_qua q1 s /\ isolated_qua q2 s /\
 165   ~ (conv0 q1 INTER conv0 q2 = {}))`;;
 166
 167 let anchor = new_definition ` anchor (v:real^3) v1 v2 s = ( {v, v1, v2} SUBSET s /\ dist3 v1 v2 <= sqrt ( &8 ) /\
 168   dist3 v1 v2 >= &2 * t0 /\ dist3 v v1 <= &2 * t0 /\ dist3 v v2 <= &2 * t0 )`;;
 169
 170
 171 let anchor_points = new_definition ` anchor_points v w s = { t | &2 * t0 <= dist3 v w /\
 172   anchor t v w s }`;;
 173
 174
 175 let Q_SYS = new_definition ` Q_SYS s = {q | quasi_reg_tet q s \/
 176               strict_qua q s /\
 177               (?c d.
 178                    !qq. c IN q /\
 179                         d IN q /\
 180                         dist3 c d > &2 * t0 /\
 181                         (quasi_reg_tet qq s \/ strict_qua qq s) /\
 182                         conv0 {c, d} INTER conv0 qq = {}) \/
 183               strict_qua q s /\
 184               (CARD
 185                {t | ?v w.
 186                         v IN q /\ w IN q /\ &2 * t0 < dist3 v w /\ anchor t v w s} >
 187                4 \/
 188                CARD
 189                {t | ?v w.
 190                         v IN q /\ w IN q /\ &2 * t0 < dist3 v w /\ anchor t v w s} =
 191                4 /\
 192                ~(?v1 v2 v3 v4 v w. v IN q /\
 193                      w IN q /\
 194                      {v1, v2, v3, v4} SUBSET anchor_points v w s
 195                       /\
 196
 197                      &2 * t0 < dist3 v w /\
 198                      quartered_oct v w v1 v2 v3 v4 s))
 199   \/ (? v w v1 v2 v3 v4. q = { v, w, v1, v2} /\ quartered_oct v w v1 v2 v3 v4 s )
 200   \/ (? v v1 v3 v2 v4. ( q = {v, v1, v2, v3} \/ q = {v, v1, v3, v4} ) /\
 201   interior_pos v v1 v3 v2 v4 s /\ anchor_points v1 v3 s = { v, v2, v4} /\
 202   anchor_points v2 v4 s = { v, v1, v3 } )}`;;
 203 *)
 204
 205 (* deprecated - thales *)
 206 let conv = new_definition `conv S:real^A->bool = affsign sgn_ge {} S`;;
 207
 208
 209 (*
 210 let barrier = new_definition ` barrier s = { { (v1 : real^3 ) , ( v2 :real^3 ) , (v3 :real^3) } |
 211   quasi_tri { v1 , v2 , v3 } s \/
 212   (? v4. ( { v1 , v2 , v3 } UNION { v4 }) IN Q_SYS s ) } `;;
 213
 214 let obstructed = new_definition ` obstructed x y s = ( ? bar. bar IN barrier s /\
 215   ( ~ (conv0_2 { x , y } INTER conv_trg bar = {})))`;;
 216
 217 let obstruct = new_definition ` obstruct x y s = ( ? bar. bar IN barrier s /\
 218   ( ~ (conv0 { x , y } INTER conv bar = {})))`;;
 219
 220 let unobstructed = new_definition ` unobstructed x y s = ( ~( obstructed x y s ))`;;
 221
 222 let VC_trg = new_definition ` VC_trg x s = { z | dist3 x z < &2 /\ ~obstructed x z s /\
 223   (! y. y IN s /\ ~ ( x = y ) /\ ~(obstructed z y s)   ==> dist3 x z < dist3 y z )} `;;
 224
 225 let VC_INFI_trg = new_definition ` VC_INFI_trg s = { z | ( ! x. x IN s /\
 226   ~( z IN VC_trg x s ))}`;;
 227
 228 let VC = new_definition `VC v s = { x | v IN lambda_x x s /\
 229 (!w. w IN lambda_x x s /\ ~(w = v) ==> dist3 x v < dist3 x w) }`;;
 230
 231 let VC_INFI = new_definition ` VC_INFI s = { z | ( ! x. ~( z IN VC x s ))}`;;
 232 *)
 233
 234
 235 let SET_TAC =
 236    let basicthms =
 237     [NOT_IN_EMPTY; IN_UNIV; IN_UNION; IN_INTER; IN_DIFF; IN_INSERT;
 238      IN_DELETE; IN_REST; IN_INTERS; IN_UNIONS; IN_IMAGE] in
 239    let allthms = basicthms @ map (REWRITE_RULE[IN]) basicthms @
 240                  [IN_ELIM_THM; IN] in
 241    let PRESET_TAC =
 242      TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ)) THEN
 243      REPEAT COND_CASES_TAC THEN
 244      REWRITE_TAC[EXTENSION; SUBSET; PSUBSET; DISJOINT; SING] THEN
 245      REWRITE_TAC allthms in
 246    fun ths ->
 247      PRESET_TAC THEN
 248      (if ths = [] then ALL_TAC else MP_TAC(end_itlist CONJ ths)) THEN
 249      MESON_TAC[];;
 250
 251  let SET_RULE tm = prove(tm,SET_TAC[]);;
 252
 253 (* some TRUONG TACTICS *)
 254
 255 let PHA = REWRITE_TAC[ MESON[] ` (a/\b)/\c <=> a/\ b /\ c `];;
 256
 257 let NGOAC = REWRITE_TAC[ MESON[] ` a/\b/\c <=> (a/\b)/\c `];;
 258
 259 let DAO = NGOAC THEN REWRITE_TAC[ MESON[]` a /\ b <=> b /\ a`];;
 260
 261 let PHAT = REWRITE_TAC[ MESON[] ` (a\/b)\/c <=> a\/b\/c `];;
 262
 263 let NGOACT =  REWRITE_TAC[ GSYM (MESON[] ` (a\/b)\/c <=> a\/b\/c `)];;
 264
 265 let KHANANG = PHA THEN REWRITE_TAC[ MESON[]` ( a\/ b ) /\ c <=> a /\ c \/ b /\ c `] THEN
 266  REWRITE_TAC[ MESON[]` a /\ ( b \/ c ) <=> a /\ b \/ a /\ c `];;
 267
 268 let ATTACH thm = MATCH_MP (MESON[]` ! a b. ( a ==> b ) ==> ( a <=> a /\ b )`) thm;;
 269
 270 let CUTHE1 th = MATCH_MP (MESON[]` ( ! a. P a ) ==> P a `) th ;;
 271
 272 let CUTHE2 th = MATCH_MP (MESON[]` ( ! a b. P a b ) ==> P a b`) th ;;
 273
 274 let CUTHE3 th = MATCH_MP (MESON[]` ( ! a b c. P a b c ) ==> P a b c`) th ;;
 275
 276 let CUTHE4 th = MATCH_MP (MESON[]` ( ! a b c d. P a b c d ) ==> P a b c d`) th ;;
 277
 278 let CUTHE5 th = MATCH_MP (MESON[]` ( ! a b c d e. P a b c d e) ==> P a b c d e`) th ;;
 279
 280 let CUTHE6 th = MATCH_MP (MESON[]` ( ! a b c d e f. P a b c d e f) ==> P a b c d e f`) th ;;
 281
 282 let CUTHE7 th = MATCH_MP (MESON[]` ( ! a b c d e f h. P a b c d e f h) ==> P a b c d e f h`) th ;;
 283
 284 let NHANH tm = ONCE_REWRITE_TAC[ ATTACH (tm)];;
 285
 286
 287 let trg_sub_bo = prove ( `A SUBSET B <=> (!x. A x ==> B x)`, SET_TAC[] );;
 288
 289 let trg_sub_se = prove ( `A SUBSET B <=> (!x. x IN A  ==> x IN B )`, SET_TAC[] );;
 290
 291 let trg_setbool = prove (`x IN A <=> A x `, SET_TAC[] );;
 292
 293 let trg_boolset = prove (` A x <=>  x IN A `, SET_TAC[] );;
 294
 295 let trg_in_union = prove (` x IN ( A UNION B ) <=> x IN A \/ x IN B `, SET_TAC[]);;
 296
 297 let not_in_set3 = prove ( `~ ( x IN { z | A z /\ B z /\ C z } ) <=> ~ A x \/ ~ B x \/ ~ C x `,
 298   SET_TAC[]);;
 299
 300 let trg_dist3_sym = prove ( `! x y. dist3 x y = dist3 y x `, SIMP_TAC[dist3; DIST_SYM]);;
 301
 302 let affine_hull_e = prove (`affine hull {} = {}`,
 303  REWRITE_TAC[AFFINE_EMPTY; AFFINE_HULL_EQ]);;
 304
 305 let wlog = MESON[]` (! a b. ( P a b = P b a ) /\ ( Q a b \/ Q b a ) ) ==> ((? a b . P a b ) <=> ( ? a b. P a b
 306   /\ Q a b ))`;;
 307
 308 let wlog_real = MESON[REAL_ARITH `( ! a b:real. a <= b \/ b <= a )`] `
 309 (! a:real b:real . P a b = P b a ) ==> ((? a:real b . P a b ) <=> ( ? a b. P a b
 310   /\ a <= b ))`;;
 311
 312 let dkdx = MESON[REAL_ARITH ` ! a b:real. a <= b \/ b <= a `]`! P. (!a b u v m n p . P a b u v m n p <=> P b a v u m n p)
 313      ==> ((?a b u v m n p. P a b u v m n p) <=> (?a b u v m n p. P a b u v m n p /\ a <= b))`;;
 314
 315
 316 let AFFINE_HULL_SINGLE = prove(`!x. affine hull {x} = {x}`,
 317   SIMP_TAC[AFFINE_SING; AFFINE_HULL_EQ]);;
 318
 319 let usefull = MESON[] ` (!x. a x ==> b x ) ==>(?x. a x ) ==> c ==> d <=>
 320  (!x. a x ==> b x) ==> (?x. a x /\ b x ) ==> c ==> d `;;
 321
 322 let v1_in_convex3 = prove (` ! v1 v2 v3. v1 IN {t | ?a b c.
 323               &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1 /\
 324  t = a % v1 + b % v2 + c % v3}`, REPEAT GEN_TAC THEN REWRITE_TAC[ IN_ELIM_THM] THEN
 325 EXISTS_TAC ` &1 ` THEN EXISTS_TAC ` &0 ` THEN EXISTS_TAC ` &0 ` THEN
 326 REWRITE_TAC[ VECTOR_ARITH ` &1 % v1 + &0 % v2 + &0 % v3 = v1 `] THEN REAL_ARITH_TAC);;
 327
 328
 329 let v3_in_convex3 = prove( `! v1 v2 v3. v3 IN
 330      {t | ?a b c.
 331               &0 <= a /\
 332               &0 <= b /\
 333               &0 <= c /\
 334               a + b + c = &1 /\
 335               t = a % v1 + b % v2 + c % v3}`, REWRITE_TAC[IN_ELIM_THM] THEN REPEAT GEN_TAC
 336 THEN REPLICATE_TAC 2 (EXISTS_TAC `&0`) THEN EXISTS_TAC ` &1` THEN REWRITE_TAC[VECTOR_MUL_LZERO;
 337  VECTOR_ADD_LID; VECTOR_MUL_LID] THEN REAL_ARITH_TAC);;
 338
 339
 340 let v1v2v3_in_convex3 = prove (` ! v1 v2 v3 . v1 IN {t | ?a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\
 341 a + b + c = &1 /\ t = a % v1 + b % v2 + c % v3}
 342    /\ v2 IN {t | ?a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1 /\ t = a % v1 + b % v2 + c % v3}
 343   /\ v3 IN {t | ?a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1 /\ t = a % v1 + b % v2 + c % v3}`,
 344 REWRITE_TAC[v1_in_convex3; v3_in_convex3] THEN REPEAT GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN
 345 EXISTS_TAC ` &0` THEN EXISTS_TAC ` &1` THEN EXISTS_TAC ` &0` THEN
 346 REWRITE_TAC[VECTOR_ARITH` v2 = &0 % v1 + &1 % v2 + &0 % v3`] THEN REAL_ARITH_TAC);;
 347
 348
 349 let convex3 = prove( `!v1 v2 v3.
 350      convex
 351      {t | ?a b c.
 352               &0 <= a /\
 353               &0 <= b /\
 354               &0 <= c /\
 355               a + b + c = &1 /\
 356               t = a % v1 + b % v2 + c % v3}`,
 357 REWRITE_TAC[convex; IN_ELIM_THM] THEN
 358 REPEAT GEN_TAC THEN STRIP_TAC THEN
 359 EXISTS_TAC ` u * a + v * a'` THEN
 360 EXISTS_TAC ` u * b + v * b'` THEN
 361 EXISTS_TAC ` u * c + v * c'` THEN
 362 REPEAT (FIRST_X_ASSUM MP_TAC) THEN
 363 REWRITE_TAC[MESON[] ` a==> b==> c <=> a /\ b==> c`] THEN PHA THEN
 364 REWRITE_TAC[ MESON[]` &0 <= a /\ l <=> l /\ &0 <= a `] THEN PHA THEN
 365 NHANH (MESON[REAL_LE_MUL; REAL_ARITH ` &0 <= a /\ &0 <= b ==> &0 <= a +b `]` &0 <= v /\
 366  &0 <= u /\
 367  &0 <= c' /\
 368  &0 <= b' /\
 369  &0 <= a' /\
 370  &0 <= c /\
 371  &0 <= b /\
 372  &0 <= a ==> &0 <= u * c + v * c' /\
 373      &0 <= u * b + v * b' /\
 374      &0 <= u * a + v * a'`) THEN
 375 REWRITE_TAC[REAL_ARITH` ( a + y ) + ( b + x ) + c + z = ( a + b + c) + (
 376   y + x + z ) `] THEN
 377 REWRITE_TAC[REAL_ARITH ` a * b + a * c = a * ( b + c) `] THEN
 378 SIMP_TAC[] THEN
 379 REWRITE_TAC[ REAL_ARITH ` a * &1 = a `] THEN SIMP_TAC[] THEN
 380 REWRITE_TAC[VECTOR_ARITH` u % (a % v1 + b % v2 + c % v3) + v % (a' % v1 + b' % v2 + c' % v3) =
 381      (u * a + v * a') % v1 + (u * b + v * b') % v2 + (u * c + v * c') % v3`]);;
 382
 383 let INTERS_SUBSET = SET_RULE `! P t0. P t0 ==> INTERS { t| P t } SUBSET t0`;;
 384
 385 let SET3_SUBSET = SET_RULE`! a b c. {a,b,c} SUBSET s <=> a IN s /\ b IN s /\ c IN s `;;
 386
 387 let SUM_TWO_RATIO = REAL_FIELD ` ~(a + b = &0) <=> a / ( a + b) + b /(a+b) = &1`;;
 388
 389 let minconvex3 = prove(`!t v1 v2 v3.
 390          convex t /\ {v1, v2, v3} SUBSET t
 391          ==> (!a b c.
 392                   &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1
 393                   ==> a % v1 + b % v2 + c % v3 IN t)`,
 394 REPEAT GEN_TAC THEN
 395 REWRITE_TAC[convex; SET3_SUBSET] THEN
 396 STRIP_TAC THEN
 397 REPEAT GEN_TAC THEN
 398 ONCE_REWRITE_TAC[ MESON[]` &0 <= a /\ &0 <= b /\ l<=> ( a + b = &0 \/
 399   ~( a + b = &0)) /\ &0 <= a /\ &0 <= b /\ l`] THEN
 400 REWRITE_TAC[RIGHT_OR_DISTRIB] THEN
 401 REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a ==> c ) /\ ( b ==> c )`] THEN
 402 REWRITE_TAC[REAL_ARITH` a + b = &0 /\ &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1
 403   <=> &0 = a /\ &0 = b /\ &1 = c `] THEN
 404 ONCE_REWRITE_TAC[ EQ_SYM_EQ] THEN
 405 SIMP_TAC[] THEN
 406 ASM_REWRITE_TAC[ VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_LID] THEN
 407 REWRITE_TAC[MESON[]`&0 = a + b <=> a + b = &0`; SUM_TWO_RATIO] THEN
 408 NHANH (MESON[REAL_ARITH ` &0 <= a /\ &0 <= b ==> &0 <= a + b `]`
 409   dau /\ &0 <= a /\ &0 <= b /\ l ==> &0 <= a + b `) THEN
 410 NHANH (MESON[REAL_LE_DIV]` (aa /\ &0 <= a /\ &0 <= b /\ bb) /\ &0 <= a + b
 411      ==> &0 <= a / (a + b) /\ &0 <= b / (a + b)`) THEN
 412 REWRITE_TAC[GSYM SUM_TWO_RATIO] THEN
 413 PHA THEN
 414 NHANH (MESON[REAL_DIV_LMUL]` ~(a + b = &0) ==> a = (a+b) *(a/(a+b)) /\ b =
 415   (a+b) *(b/(a+b))`) THEN
 416 REWRITE_TAC[MESON[VECTOR_MUL_RCANCEL]` ( dau /\ a = (a + b) * a / (a + b) /\ b = (a + b) * b / (a + b))
 417   /\ l ==> a % v1 + b % v2 + c % v3 IN t <=>
 418   ( dau /\ a = (a + b) * a / (a + b) /\ b = (a + b) * b / (a + b))
 419   /\ l ==> ((a + b) * a / (a + b)) % v1 + ((a + b) * b / (a + b)) % v2 + c % v3 IN t`] THEN
 420 REWRITE_TAC[ VECTOR_ARITH ` ((a + b) * a / (a + b)) % v1 + ((a + b) * b / (a + b)) % v2 + c % v3
 421   = (a + b) % ( (a / (a + b)) % v1 + (b / (a + b)) % v2) + c % v3 `] THEN
 422 REWRITE_TAC[SUM_TWO_RATIO] THEN
 423 ASM_MESON_TAC[ REAL_ARITH` a + b + c = (a + b ) + c`]);;
 424
 425
 426 let EQ_EXPAND = MESON[] `(a <=> b) <=> ( a ==> b ) /\ ( b ==> a )` ;;
 427
 428
 429
 430 let OTHER_CONVEX_CONDI = prove(` ! s. convex s <=> (! a b c v1 v2 v3. {v1, v2, v3} SUBSET s /\
 431     &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1
 432                   ==> a % v1 + b % v2 + c % v3 IN s)`,
 433 REWRITE_TAC[EQ_EXPAND; MESON[minconvex3]`!s. (convex s
 434       ==> (!a b c v1 v2 v3.
 435                {v1, v2, v3} SUBSET s /\
 436                &0 <= a /\
 437                &0 <= b /\
 438                &0 <= c /\
 439                a + b + c = &1
 440                ==> a % v1 + b % v2 + c % v3 IN s))`; convex] THEN STRIP_TAC THEN
 441 REWRITE_TAC[SET3_SUBSET] THEN DISCH_TAC THEN
 442 REWRITE_TAC[REAL_ARITH`&0 <= u /\ &0 <= v /\ u + v = &1 <=>
 443   &0 <= u /\ &0 <= v / &2 /\ u + v/ &2 + v / &2 = &1`] THEN
 444 ONCE_REWRITE_TAC[MESON[REAL_ARITH` a = a / &2 + a / &2`]` u % x + v % y =
 445    u % x + ( v/ &2 + v/ &2 ) % y `] THEN REWRITE_TAC[ VECTOR_ADD_RDISTRIB] THEN
 446 ASM_MESON_TAC[]);;
 447
 448
 449 (* ============== *)
 450
 451
 452 let convex3_in_inters = prove (` ! v1 v2 v3. {t | ?a b c.
 453           &0 <= a /\
 454           &0 <= b /\
 455           &0 <= c /\
 456           a + b + c = &1 /\
 457           t = a % v1 + b % v2 + c % v3} SUBSET
 458  INTERS {t | convex t /\ {v1, v2, v3} SUBSET t} `,
 459 REPEAT GEN_TAC THEN
 460 MATCH_MP_TAC (SET_RULE ` ( ! x. x IN A ==> x IN B ) ==> A SUBSET B`) THEN
 461 REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[IN_INTERS] THEN
 462 REWRITE_TAC[MESON[] `( !x. (?a b c.
 463           &0 <= a /\
 464           &0 <= b /\
 465           &0 <= c /\
 466           a + b + c = &1 /\
 467           x = a % v1 + b % v2 + c % v3)
 468      ==> (!t. convex t /\ {v1, v2, v3} SUBSET t ==> x IN t))
 469   <=>( !x. (?a b c.
 470           &0 <= a /\
 471           &0 <= b /\
 472           &0 <= c /\
 473           a + b + c = &1 /\
 474           x = a % v1 + b % v2 + c % v3)
 475      ==> (!t. convex t /\ {v1, v2, v3} SUBSET t /\ (?a b c.
 476           &0 <= a /\
 477           &0 <= b /\
 478           &0 <= c /\
 479           a + b + c = &1 /\
 480           x = a % v1 + b % v2 + c % v3) ==> x IN t)) `] THEN
 481 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN FIRST_X_ASSUM MP_TAC THEN
 482 REWRITE_TAC[ IN_ELIM_THM ; TAUT ` a ==> b ==> c <=> a /\ b ==> c `] THEN
 483 MESON_TAC[minconvex3]);;
 484
 485
 486 (* =========== *)
 487
 488
 489
 490 let simpl_conv3 =prove(` ! v1 v2 v3. conv_trg {v1 , v2 ,v3} = {t | ?a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1
 491 /\ t = a % v1 + b % v2 + c % v3}`, REPEAT GEN_TAC THEN
 492 REWRITE_TAC[conv; hull] THEN REPEAT GEN_TAC THEN
 493 REWRITE_TAC[ SET_RULE` a = b <=> a SUBSET b /\ b SUBSET a `] THEN
 494 REWRITE_TAC[conv_trg; hull] THEN
 495 MATCH_MP_TAC (MATCH_MP ( MESON[] `(! a b. P a b) ==> P a b` ) (MESON[INTERS_SUBSET ]`
 496   ! P t0 . ( P t0 /\ aa ) ==> INTERS {t | P t} SUBSET t0 /\ aa`)) THEN
 497  REWRITE_TAC[convex3] THEN REWRITE_TAC[ SET_RULE `{v1 , v2, v3} SUBSET a <=>
 498   v1 IN a /\ v2 IN a /\ v3 IN a`] THEN REWRITE_TAC [ v1v2v3_in_convex3] THEN
 499 REWRITE_TAC[ SET_RULE` v1 IN t /\ v2 IN t /\ v3 IN t <=> {v1, v2, v3} SUBSET t`] THEN
 500 REWRITE_TAC[convex3_in_inters]);;
 501
 502
 503 (* =========== begining lemma 8.2 ========== *)
 504
 505
 506 (*
 507 let near2t0 = new_definition ` near2t0 v0 s = { x | x IN s /\ dist(v0,x) < &2 * t0 }`;;
 508
 509 let e_plane = new_definition ` e_plane (a:real^N) (b:real^N) x = ( ~( a=b) /\ dist(a,x) = dist(b,x))`;;
 510 *)
 511
 512 let min_dist = new_definition ` min_dist (x:real^3) s = ((?u. u IN s /\
 513                   (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/
 514              (?u v.
 515                   u IN s /\
 516                   v IN s /\
 517                   ~(u = v) /\
 518                   dist (u,x) = dist (v,x) /\
 519                   (!w. w IN s ==> dist (u,x) <= dist (w,x)))) `;;
 520
 521 (* ========== simplize.ml ============ *)
 522
 523 let SET3_SUBSET = SET_RULE`! a b c. {a,b,c} SUBSET s <=> a IN s /\ b IN s /\ c IN s `;;
 524
 525 let FINITE6 = MESON[ FINITE_RULES ] `! a b c d e f.
 526          FINITE {} /\
 527          FINITE {a} /\
 528          FINITE {a, b} /\
 529          FINITE {a, b, c} /\
 530          FINITE {a, b, c, d} /\
 531          FINITE {a, b, c, d, e} /\
 532          FINITE {a, b, c, d, e, f} `;;
 533
 534 (* ========= new simplizing ========== *)
 535
 536 let elimin = REWRITE_RULE[IN];;
 537
 538 let CONV_EM = prove(`conv {} = {}:real^A->bool`,
 539   REWRITE_TAC[conv;sgn_ge;affsign;UNION_EMPTY;FUN_EQ_THM;elimin
 540 NOT_IN_EMPTY;lin_combo;SUM_CLAUSES]
 541   THEN REAL_ARITH_TAC);;
 542
 543 let CONV_SING = prove(`!u. conv {u:real^A} = {u}`,
 544  REWRITE_TAC[conv;sgn_ge;affsign;FUN_EQ_THM;UNION_EMPTY;lin_combo;SUM_SING;VSUM_SING;
 545  elimin IN_SING] THEN REPEAT GEN_TAC THEN
 546  REWRITE_TAC[TAUT `(p <=> q) = ((p ==> q) /\ (q ==> p))`] THEN
 547  REPEAT STRIP_TAC THENL [ASM_MESON_TAC[VECTOR_MUL_LID];
 548  ASM_REWRITE_TAC[]] THEN EXISTS_TAC `\ (v:real^A). &1` THEN
 549  MESON_TAC[VECTOR_MUL_LID;REAL_ARITH `&0 <= &1`] );;
 550
 551
 552 let NOV9 = prove(`!x y z.(x = y /\ y = z
 553       ==> conv {y, z} =
 554           {w | ?a b c.
 555                    &0 <= a /\
 556                    &0 <= b /\
 557                    &0 <= c /\
 558                    a + b + c = &1 /\
 559                    w = a % y + b % y + c % z})`,
 560 SIMP_TAC[] THEN REWRITE_TAC[SET_RULE` {a,a} = {a}`] THEN
 561 REWRITE_TAC[ CONV_SING;  GSYM VECTOR_ADD_RDISTRIB] THEN
 562 REWRITE_TAC[ MESON[]` a + b + c = &1 /\ w = (a + b + c) % z <=>a + b + c = &1 /\
 563    w = &1 % z `; VECTOR_MUL_LID] THEN REWRITE_TAC[ FUN_EQ_THM] THEN
 564 REWRITE_TAC[ SET_RULE ` {a} x <=> a = x `; IN_ELIM_THM] THEN
 565 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
 566 NGOAC THEN REWRITE_TAC[ LEFT_EXISTS_AND_THM] THEN
 567 MATCH_MP_TAC (MESON[] ` a ==> ( z = x <=> a /\ x = z )`) THEN
 568 REPLICATE_TAC 2 (EXISTS_TAC `&0`) THEN EXISTS_TAC ` &1` THEN REAL_ARITH_TAC);;
 569
 570 let IN_ACT_SING = SET_RULE `! a x. ({a} x <=> a = x ) /\ ( x IN {a} <=> x = a) /\ {a} a`;;
 571
 572 let NOV10 = prove(` ! x y. (x = y
 573       ==> (!x. y = x <=>
 574                (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x = a % y + b % y))) `,
 575 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN
 576 REWRITE_TAC[ MESON[VECTOR_MUL_LID]` a + b = &1 /\ x = (a + b) % y <=> a + b = &1 /\
 577 x = y`]THEN REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN NGOAC THEN
 578 REWRITE_TAC[LEFT_EXISTS_AND_THM] THEN MATCH_MP_TAC (MESON[]` a ==> ( x = y <=> a /\
 579  y = x )`)THEN EXISTS_TAC `&0` THEN EXISTS_TAC ` &1` THEN REAL_ARITH_TAC);;
 580
 581 let IN_SET2 = SET_RULE `!a b x.
 582          (x IN {a, b} <=> x = a \/ x = b) /\ ({a, b} x <=> x = a \/ x = b)`;;
 583
 584
 585 let VSUM_DIS2 = prove(` ! x y f. ~(x=y) ==>  vsum {x,y} f = f x + f y`, REWRITE_TAC[
 586    SET_RULE ` ~( x = y)
 587  <=> ~(x IN {y})`] THEN MESON_TAC[ FINITE_RULES; VSUM_CLAUSES; VSUM_SING]);;
 588
 589 let SUM_DIS2 = prove(`! x y f. ~(x=y) ==> sum {x,y} f = f x + f y `,REWRITE_TAC[
 590    SET_RULE ` ~( x = y)
 591  <=> ~(x IN {y})`] THEN MESON_TAC[ FINITE_RULES; SUM_CLAUSES; SUM_SING]);;
 592
 593
 594 let TRUONG_LEMMA = prove
 595   (  `!x y x':real^N.
 596        (?f. x' = f x % x + f y % y /\ (&0 <= f x /\ &0 <= f y) /\
 597             f x + f y = &1) <=>
 598        (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x' = a % x + b % y)`   ,
 599    REPEAT GEN_TAC THEN EQ_TAC
 600 THENL [MESON_TAC[]; STRIP_TAC] THEN
 601    ASM_CASES_TAC `y:real^N = x` THENL
 602     [EXISTS_TAC `\x:real^N. &1 / &2`;
 603      EXISTS_TAC `\u:real^N. if u = x then (a:real) else b`] THEN
 604    ASM_REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN
 605    CONV_TAC REAL_RAT_REDUCE_CONV);;
 606
 607
 608 let NOV11 = prove(`! z. {z} =
 609  {w | ?a b c.
 610           &0 <= a /\
 611           &0 <= b /\
 612           &0 <= c /\
 613           a + b + c = &1 /\
 614           w = a % z + b % z + c % z}`,
 615 REWRITE_TAC[ FUN_EQ_THM; IN_ACT_SING; IN_ELIM_THM] THEN
 616 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN
 617 REWRITE_TAC[ MESON[VECTOR_MUL_LID]`a + b + c = &1 /\
 618           x = (a + b + c) % z <=> a + b + c = &1 /\ x = z`] THEN
 619 NGOAC THEN MATCH_MP_TAC (MESON[]` (? a b c. P a b c) ==> (! z x. z = x <=>
 620   (? a b c. P a b c /\ x = z))`) THEN
 621 REPLICATE_TAC 2 (EXISTS_TAC `&0`) THEN
 622 EXISTS_TAC `&1` THEN REAL_ARITH_TAC);;
 623
 624
 625
 626 let CONV2_CONV3 = prove(` !x' y z.
 627          (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x' = a % y + b % z)
 628          ==> (?a b c.
 629                   &0 <= a /\
 630                   &0 <= b /\
 631                   &0 <= c /\
 632                   a + b + c = &1 /\
 633                   x' = a % y + b % y + c % z)`,
 634 REPEAT GEN_TAC THEN REWRITE_TAC[ VECTOR_ARITH` a % y + b % y + c % z = (a+b) %y + c%z`] THEN STRIP_TAC THEN
 635 REPLICATE_TAC 2 (EXISTS_TAC `a/ &2`) THEN
 636 EXISTS_TAC `b:real` THEN
 637 REWRITE_TAC[ REAL_ARITH` a / &2 + a / &2 = a /\ a / &2 + a / &2 + b = a + b `] THEN
 638 ASM_SIMP_TAC[] THEN
 639 ASM_REAL_ARITH_TAC);;
 640
 641
 642 let CONV3_CONV2 = prove(`! x' y z. (?a b c.
 643       &0 <= a /\
 644       &0 <= b /\
 645       &0 <= c /\
 646       a + b + c = &1 /\
 647       x' = a % y + b % y + c % z)
 648  ==> (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x' = a % y + b % z)`,
 649 REPEAT GEN_TAC THEN STRIP_TAC THEN EXISTS_TAC ` a + b:real` THEN
 650 EXISTS_TAC `c:real` THEN
 651 REWRITE_TAC[VECTOR_ADD_RDISTRIB] THEN
 652 REWRITE_TAC[VECTOR_ARITH` (a % y + b % y) + c % z = a % y + b % y + c % z `] THEN
 653 ASM_SIMP_TAC[REAL_ARITH ` a + b + c = (a + b) + c`] THEN
 654 ASM_REAL_ARITH_TAC);;
 655
 656 let CONV_SET2 = prove(` ! x y:real^A. conv {x,y} = {w | ? a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\
 657   w = a%x + b%y}`,
 658 ONCE_REWRITE_TAC[ MESON[] ` (! a b. P a b ) <=> ( ! a b. a = b \/ ~( a= b)
 659   ==> P a b )`] THEN
 660 REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a==> c) /\ ( b==> c)`] THEN
 661 SIMP_TAC[] THEN
 662 REWRITE_TAC[ SET_RULE ` {a,a} = {a}`; CONV_SING; FUN_EQ_THM; IN_ELIM_THM] THEN
 663 REWRITE_TAC[ IN_ACT_SING] THEN
 664 REWRITE_TAC[NOV10] THEN
 665 REWRITE_TAC[conv; sgn_ge; affsign; lin_combo] THEN
 666 REWRITE_TAC[UNION_EMPTY; IN_SET2] THEN
 667 ONCE_REWRITE_TAC[ MESON[]`  ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
 668   ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`] THEN
 669 REWRITE_TAC[ MESON[VSUM_DIS2; SUM_DIS2]` ~(x = y) /\
 670                     x' = vsum {x, y} ff /\ l /\ sum {x, y} f = &1 <=> ~(x = y) /\
 671                     x' = ff x + ff y /\ l /\ f x + f y = &1 `] THEN
 672 REWRITE_TAC[ MESON[]` (!w. w = x \/ w = y ==> &0 <= f w) <=> &0 <= f x /\ &0 <= f y`] THEN
 673 ONCE_REWRITE_TAC[ GSYM (MESON[]`  ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
 674   ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`)] THEN
 675 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
 676 REWRITE_TAC[ TRUONG_LEMMA]);;
 677
 678 let CONV3_A_EQ = prove(`! x y z. (x = y \/ y = z \/ z = x
 679   ==> conv {x, y, z} =
 680       {w | ?a b c.
 681                &0 <= a /\
 682                &0 <= b /\
 683                &0 <= c /\
 684                a + b + c = &1 /\
 685                w = a % x + b % y + c % z})`,
 686 MATCH_MP_TAC (MESON[] `(! a b c. P a b c <=> P b a c) /\ (! a b c. a = b \/ b = c ==> P a b c)
 687   ==> (! a b c. a = b \/ b = c \/ c = a ==> P a b c )`) THEN
 688 SIMP_TAC[ MESON[ SET_RULE ` {a,b,c} = {b,a,c} `]`conv {x, y, z} = conv {y,x,z}`] THEN
 689 SIMP_TAC[ MESON[ REAL_ARITH` a + b + c = b + a + c`; VECTOR_ARITH` a % x + b % y + c % z
 690   = b % y + a % x + c % z `]` (?a b c.
 691                &0 <= a /\
 692                &0 <= b /\
 693                &0 <= c /\
 694                a + b + c = &1 /\
 695                w = a % x + b % y + c % z)
 696   <=> (?a b c.
 697                &0 <= a /\
 698                &0 <= b /\
 699                &0 <= c /\
 700                a + b + c = &1 /\
 701                w = a % y + b % x + c % z)`] THEN
 702 MATCH_MP_TAC (MESON[]` (! a b c. P a b c <=> P c b a ) /\ (! a b c. a = b ==> P a b c)
 703   ==> (! a b c. a = b \/ b = c ==> P a b c)`) THEN
 704 SIMP_TAC[ MESON[SET_RULE `{a,b,c} ={c,b,a} `]` conv {a,b,c} = conv {c,b,a}`] THEN
 705 SIMP_TAC[ MESON[REAL_ARITH` a + b + c = c + b + a`; VECTOR_ARITH` a % x + b % y + c % z
 706   = c % z + b % y + a % x `]`(?a b c.
 707                &0 <= a /\
 708                &0 <= b /\
 709                &0 <= c /\
 710                a + b + c = &1 /\
 711                w = a % x + b % y + c % z) <=>
 712   (?a b c.
 713                &0 <= a /\
 714                &0 <= b /\
 715                &0 <= c /\
 716                a + b + c = &1 /\
 717                w = a % z + b % y + c % x)`] THEN
 718 REWRITE_TAC[ SET_RULE`{a,a,b} = {a,b}`] THEN
 719 ONCE_REWRITE_TAC[ MESON[]` x = y ==> conv {y,z} = s <=> x = y /\( y = z \/
 720   ~(y=z))==> conv {y,z} = s `] THEN
 721 KHANANG THEN REWRITE_TAC[ MESON[]` a \/ b ==> c <=> (a==> c) /\ (b==> c)`] THEN
 722 SIMP_TAC[] THEN REWRITE_TAC[SET_RULE`{a,a} ={a}`; CONV_SING] THEN
 723 SIMP_TAC[NOV11] THEN REWRITE_TAC [ GSYM NOV11] THEN
 724 REWRITE_TAC[CONV_SET2] THEN
 725 REPEAT GEN_TAC THEN STRIP_TAC THEN
 726  REWRITE_TAC[ FUN_EQ_THM; IN_ELIM_THM] THEN
 727 GEN_TAC THEN REWRITE_TAC[MESON[]` (a <=> b ) <=> ( a ==> b) /\ (b==> a)`] THEN
 728 REWRITE_TAC[CONV2_CONV3; CONV3_CONV2]);;
 729
 730
 731 let VSUM_DIS3 = prove( `! x y z f. ~(x=y\/y=z\/z=x) ==> vsum {x,y,z} f = f x + f y + f z `,
 732 NHANH (SET_RULE` ~(x = y \/ y = z \/ z = x) ==> ({x} INTER {y,z} = {}) `) THEN
 733 REWRITE_TAC[ GSYM DISJOINT; SET_RULE `{x, y, z} = {x} UNION {y,z}` ] THEN
 734 REWRITE_TAC[MESON[FINITE6; VSUM_UNION]` aa /\ DISJOINT {x} {y, z}
 735      ==> vsum ({x} UNION {y, z}) f = ab <=>  aa /\ DISJOINT {x} {y, z} ==>
 736   vsum {x} f + vsum {y,z} f = ab `] THEN
 737  MESON_TAC[VSUM_SING; VSUM_DIS2]);;
 738
 739
 740 let SUM_DIS3 = prove(` ! x y z f. ~(x = y \/ y = z \/ z = x) ==> sum {x, y, z} f =
 741   f x + f y + f z `,
 742 NHANH (SET_RULE` ~(x = y \/ y = z \/ z = x) ==> ({x} INTER {y,z} = {}) `) THEN
 743 REWRITE_TAC[ GSYM DISJOINT; SET_RULE `{x, y, z} = {x} UNION {y,z}` ] THEN
 744 REWRITE_TAC[MESON[FINITE6; SUM_UNION]` aa /\ DISJOINT {x} {y, z}
 745      ==> sum ({x} UNION {y, z}) f = ab <=>  aa /\ DISJOINT {x} {y, z} ==>
 746   sum {x} f + sum {y,z} f = ab `] THEN MESON_TAC[ SUM_SING; SUM_DIS2]);;
 747
 748 let EQ_EXPAND = MESON[] `(a <=> b) <=> ( a ==> b ) /\ ( b ==> a )` ;;
 749
 750 let CONV_SET3 = prove(`! x y z:real^A. conv {x,y,z} = { w | ? a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\
 751 a + b + c = &1 /\ w = a % x + b % y + c % z } `,
 752 REPEAT GEN_TAC THEN
 753 ONCE_REWRITE_TAC[ MESON[]` conv {x,y,z} = s <=> (x = y \/ y= z \/ z = x ) \/
 754   ~(x = y \/ y= z \/ z = x ) ==> conv {x,y,z} = s`] THEN
 755 ONCE_REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a ==> c ) /\(b==>c)`] THEN
 756 REWRITE_TAC[CONV3_A_EQ] THEN
 757 REWRITE_TAC[conv; FUN_EQ_THM; affsign; IN_ELIM_THM; sgn_ge; lin_combo; UNION_EMPTY] THEN
 758 DISCH_TAC THEN GEN_TAC THEN FIRST_X_ASSUM MP_TAC THEN
 759 ONCE_REWRITE_TAC[ MESON[]` a ==> ((?f. P f ) <=> la ) <=>
 760   a ==> ((?f. a /\ P f ) <=> la ) `] THEN REWRITE_TAC[MESON[VSUM_DIS3]` ~(x = y \/
 761 y = z \/ z = x) /\ x' = vsum {x, y, z} f /\ l <=>   ~(x = y \/ y = z \/ z = x) /\
 762 x' = f x + f y + f z /\ l `] THEN
 763 REWRITE_TAC[ MESON[SUM_DIS3]` ~(x = y \/ y = z \/ z = x) /\ P /\ Q /\ sum {x,y,z} f = &1
 764   <=> ~(x = y \/ y = z \/ z = x) /\ P /\ Q /\ ( f x + f y + f z ) = &1`] THEN
 765 REWRITE_TAC[SET_RULE ` (!w. {x, y, z} w ==> &0 <= f w) <=> &0 <= f x /\
 766    &0 <= f y /\ &0 <= f z `] THEN
 767 ONCE_REWRITE_TAC[ GSYM (MESON[]` a ==> ((?f. P f ) <=> la ) <=>
 768   a ==> ((?f. a /\ P f ) <=> la ) `)] THEN DISCH_TAC THEN
 769 REWRITE_TAC[ EQ_EXPAND] THEN
 770 REWRITE_TAC[ MESON[]` (?f. x' = f x % x + f y % y + f z % z /\
 771        (&0 <= f x /\ &0 <= f y /\ &0 <= f z) /\
 772        f x + f y + f z = &1)
 773   ==> (?a b c.
 774            &0 <= a /\
 775            &0 <= b /\
 776            &0 <= c /\
 777            a + b + c = &1 /\
 778            x' = a % x + b % y + c % z)`] THEN STRIP_TAC THEN
 779 EXISTS_TAC ` (\d. if d = (x:real^A) then (a:real) else ( if d = (y:real^A) then
 780   (b:real)  else c ))` THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN
 781 REWRITE_TAC[ MESON[]`~( a \/ b ) <=> ~a /\ ~b `] THEN SIMP_TAC[]);;
 782
 783 (* ========== *)
 784 let CONV3_EQ = prove(` ! x y z. conv_trg {x,y,z} = conv {x,y,z} `, REWRITE_TAC[simpl_conv3;
 785 CONV_SET3]);;
 786 (* ========= *)
 787
 788 (* ==== CARD ASSERTION ==== *)
 789
 790
 791 let CARD_CLAUSES_IMP = prove(` !a s.
 792      FINITE s
 793      ==> CARD (a INSERT s) <= SUC (CARD s) /\
 794          (a IN s ==> CARD (a INSERT s) = CARD s) /\
 795          (~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s))`,
 796 ONCE_REWRITE_TAC[ MESON[] ` ( a ==> b /\ c ) <=> ( a ==> b ) /\ ( a ==> c )`] THEN
 797 REWRITE_TAC[ MESON[CARD_CLAUSES] ` FINITE s ==> ( a IN s ==> CARD (a INSERT s) = CARD s ) /\
 798   (~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s))`] THEN
 799 MESON_TAC[ CARD_CLAUSES; ARITH_RULE ` a <= SUC a /\ a <= a `]);;
 800
 801 (* =================== *)
 802
 803 let CARD_SING = prove( `! a: A. CARD {a} = 1`, REWRITE_TAC[ MESON[ FINITE6; CARD_EQ_NSUM ]
 804 ` CARD {a} = nsum {a} (\x. 1)`] THEN REWRITE_TAC[ NSUM_SING ]);;
 805
 806 let CARD_SET2 = prove( ` ! a b . ( CARD {a, b} = 2 <=> ~(a = b)) /\ (CARD {a, b} = 1 <=> a = b ) `,
 807 REWRITE_TAC[ MESON[ FINITE6; CARD_CLAUSES ] ` CARD {a,b} = (if a IN {b} then CARD {b} else SUC (CARD {b}))`]
 808 THEN REWRITE_TAC[ MESON[ FINITE6; CARD_CLAUSES ] ` CARD {a} = (if a IN {} then CARD {} else SUC (CARD {}))`]
 809 THEN REWRITE_TAC[ NOT_IN_EMPTY; IN_SING; CARD_CLAUSES; ADD1] THEN
 810 MESON_TAC[ ARITH_RULE `  ~( 0+ 1 = 2 ) /\ (0 + 1) + 1 = 2 /\ ~((0 + 1) + 1 = 1 ) /\ 0 + 1 = 1  `]);;
 811
 812 (* ============== *)
 813
 814 let CARD_EQUATION = prove(`!(s: A -> bool) t.
 815      FINITE s /\ FINITE t
 816      ==> CARD (s UNION t) + CARD (s INTER t) = CARD s + CARD t `,
 817 NHANH (MESON[FINITE_INTER; FINITE_UNION] `FINITE s /\ FINITE t ==> FINITE ( s UNION t ) /\
 818     FINITE ( s INTER t ) `) THEN MESON_TAC[ CARD_EQ_NSUM; NSUM_INCL_EXCL]);;
 819
 820
 821 let CARD_DISJOINT = prove(` ! s: A -> bool t. FINITE s /\ FINITE t ==>
 822        ( CARD s + CARD t = CARD ( s UNION t ) <=> s INTER t ={} )`,
 823 MESON_TAC[CARD_EQUATION; ARITH_RULE ` a + b = a <=> b = 0 `; FINITE_INTER; CARD_EQ_0]);;
 824
 825
 826 let CARD2 = prove(` ! a b . CARD {a,b} <= 2 /\ ( CARD {a,b} = 2 <=> ~(a = b ) )`,
 827 REWRITE_TAC[ MESON[ CARD_SET2] ` CARD {a, b} = 2 <=> ~(a = b)`] THEN MP_TAC CARD_SET2 THEN
 828 ONCE_REWRITE_TAC[ MESON[] ` CARD {a, b} <= 2 <=>
 829   ( a = b \/ ~( a = b)) /\ CARD {a, b} <= 2`] THEN KHANANG THEN
 830 REWRITE_TAC[ MESON[CARD_SET2] `a = b /\ CARD {a, b} <= 2 \/ ~(a = b) /\ CARD {a, b} <= 2
 831   <=> a = b /\ 1 <= 2 \/ ~(a = b) /\ 2 <= 2`] THEN
 832 MESON_TAC[ARITH_RULE ` 1 <= 2 /\ 2 <= 2 `]);;
 833
 834
 835 let CARD3 = prove(`! a b c . CARD {a,b,c} <= 3 /\
 836   ( CARD {a,b,c} = 3 <=> ~( a =b \/ b= c\/ c= a ))`,
 837 REWRITE_TAC[ SET_RULE ` {a,b,c} = {a} UNION {b,c}`] THEN
 838 REWRITE_TAC[ ARITH_RULE ` CARD ({a} UNION {b, c}) <= 3 <=>
 839   CARD ({a} UNION {b, c}) + CARD ({a} INTER {b, c}) <= 3 + CARD ({a} INTER {b, c})`] THEN
 840 REWRITE_TAC[ ARITH_RULE ` CARD ({a} UNION {b, c}) = 3 <=>
 841   CARD ({a} UNION {b, c}) + CARD ({a} INTER {b, c}) = 3 + CARD ({a} INTER {b, c})`] THEN
 842 REWRITE_TAC[ MESON[ FINITE_RULES; CARD_EQUATION] ` CARD ({a} UNION {b, c}) + CARD ({a} INTER {b, c})
 843   = CARD {a} + CARD {b,c} `] THEN REWRITE_TAC[ CARD_SING] THEN
 844 REWRITE_TAC[ ARITH_RULE `! a b. (1 + a <= 3 + b <=> a <= 2 + b ) /\
 845   (1 + a = 3 + b <=> a = 2 + b )`] THEN
 846 REWRITE_TAC[ MESON[CARD2; ARITH_RULE ` a <= b ==> a <= b + c: num`] ` CARD {b, c} <=   2 + CARD ({a} INTER {b, c})`] THEN
 847 ONCE_REWRITE_TAC[ MESON[CARD2]` CARD {b, c} = P b c <=> CARD {b, c} <= 2 /\   CARD {b, c} = P b c`] THEN
 848 REWRITE_TAC[ ARITH_RULE ` a <= 2 /\ a = 2 + b <=> a = 2 /\ b = 0`] THEN
 849 REWRITE_TAC[ MESON[FINITE_RULES; CARD2; FINITE_INTER; CARD_EQ_0] ` CARD {b, c} = 2 /\ CARD ({a} INTER {b, c}) = 0
 850   <=> ~(b=c) /\ {a} INTER {b, c} = {}`] THEN SET_TAC[]);;
 851
 852 (* ========= *)
 853
 854
 855 let CARD4 = prove(`!a b c d.
 856      CARD {a, b, c, d} <= 4 /\
 857      (CARD {a, b, c, d} = 4 <=>
 858       ~(a IN {b, c, d}) /\ ~(b = c \/ c = d \/ d = b))`,
 859 NHANH (MESON[FINITE6; CARD_CLAUSES_IMP]` CARD {a, b, c, d} <= 4 ==> CARD {a, b, c, d}
 860    <= SUC (CARD {b,c,d})`) THEN
 861 NHANH ( MESON[CARD3] ` aa <= SUC (CARD {b, c, d}) ==> CARD {b,c,d} <= 3 `) THEN
 862 REWRITE_TAC[ ARITH_RULE ` CARD {a, b, c, d} <= 4 /\
 863      CARD {a, b, c, d} <= SUC (CARD {b, c, d}) /\
 864      CARD {b, c, d} <= 3 <=>
 865      CARD {a, b, c, d} <= SUC (CARD {b, c, d}) /\ CARD {b, c, d} <= 3`] THEN
 866 SIMP_TAC[MESON[FINITE_RULES; CARD_CLAUSES_IMP] ` CARD {a, b, c, d} <= SUC
 867         (CARD {b, c, d})`; CARD3; CARD_CLAUSES_IMP] THEN
 868 REWRITE_TAC[ ARITH_RULE ` CARD {a, b, c, d} = 4 <=> CARD {a, b, c, d} + CARD ( {a}
 869    INTER {b,c,d} ) = 4 + CARD ({a} INTER {b,c,d})`] THEN
 870 REWRITE_TAC[ SET_RULE ` {a,b,c,d} = {a} UNION {b,c,d} ` ] THEN
 871 REWRITE_TAC[ MESON[FINITE_RULES; CARD_EQUATION; CARD_SING] ` CARD ({a} UNION {b, c, d}) + CARD ({a} INTER {b, c, d})
 872   = 1 + CARD {b,c,d} `] THEN
 873 NHANH (MESON[CARD3] ` 1 + CARD {b, c, d} = aa ==> CARD {b,c,d} <= 3 `) THEN
 874 REWRITE_TAC[ ARITH_RULE `1 + CARD {b, c, d} = 4 + CARD ({a} INTER {b, c, d}) /\
 875      CARD {b, c, d} <= 3 <=>
 876      CARD {b, c, d} = 3 /\ CARD ({a} INTER {b, c, d}) = 0`] THEN
 877 REWRITE_TAC[ CARD3] THEN
 878 MESON_TAC[ FINITE_RULES; FINITE_INTER; CARD_EQ_0; SET_RULE `
 879   {a} INTER {b, c, d} = {} <=> ~(a IN {b, c, d})` ]);;
 880
 881
 882 let CARD5 = prove(` ! a b c d e. CARD {a,b,c,d,e} <= 5 /\
 883   ( CARD {a,b,c,d,e} = 5 <=> ~( a IN {b,c,d,e}) /\
 884                             ~(b IN {c, d, e}) /\ ~(c = d \/ d = e \/ e = c))`,
 885 ONCE_REWRITE_TAC[ MESON[ FINITE_RULES; CARD_CLAUSES_IMP] ` CARD {a, b, c, d, e} <= 5 <=>
 886   CARD {a, b, c, d, e} <= SUC ( CARD {b,c,d,e} ) ==> CARD {a, b, c, d, e} <= 5`] THEN
 887 ONCE_REWRITE_TAC[ MESON[CARD4] ` aa ==> CARD {a, b, c, d, e} <= 5 <=>
 888   aa /\ CARD {b,c,d,e} <= 4 ==> CARD {a, b, c, d, e} <= 5`] THEN
 889 REWRITE_TAC[ ARITH_RULE ` a <= SUC b /\ b <= 4 ==> a <= 5 `] THEN
 890 REWRITE_TAC[ ARITH_RULE ` CARD {a, b, c, d, e} = 5 <=>
 891   CARD {a, b, c, d, e} + CARD ({a} INTER {b,c,d,e} ) = 5 + CARD ({a} INTER {b,c,d,e} )`] THEN
 892 REWRITE_TAC[ SET_RULE ` {a,b,c,d,e} = {a} UNION {b,c,d,e} `] THEN
 893 REWRITE_TAC[ MESON[FINITE_RULES; CARD_EQUATION; CARD_SING ]` CARD ({a} UNION {b, c, d, e}) +
 894   CARD ({a} INTER {b, c, d, e})  = 1 + CARD {b,c,d,e} `] THEN
 895 ONCE_REWRITE_TAC[ MESON[ CARD4] ` 1 + CARD {b, c, d, e} = aa <=> CARD {b,c,d,e} <= 4 /\
 896      1 + CARD {b, c, d, e} = aa `] THEN
 897 REWRITE_TAC[ ARITH_RULE ` a <= 4 /\ 1 + a = 5 + b <=> a = 4 /\ b = 0`] THEN
 898 REWRITE_TAC[ CARD4; MESON[FINITE_RULES; FINITE_INTER; CARD_EQ_0] `
 899   CARD ({a} INTER {b, c, d, e}) = 0 <=> {a} INTER {b, c, d, e} ={} `] THEN SET_TAC[]);;
 900 (* ============ *)
 901
 902 let set_3elements = prove(`(?a b c. ~(a = b \/ b = c \/ c = a) /\ {a, b, c} = {v1, v2, v3}) <=>
 903  ~(v1 = v2 \/ v2 = v3 \/ v3 = v1)`, REWRITE_TAC[GSYM CARD3] THEN
 904 MESON_TAC[]);;
 905
 906
 907 (*
 908 let db_t0 = prove(`&2 * t0 = &2 * #1.255 /\ &2 * t0 = #2.51 /\ &2 * #1.255 = #2.51`,
 909   REWRITE_TAC[t0] THEN REAL_ARITH_TAC);;
 910 *)
 911
 912 let without_lost = MESON[] ` ! P x. (!a b. P a b <=> P b a) /\ (?a b. P a b /\ x = a)
 913      ==> (?a b. P a b /\ (x = a \/ x = b))`;;
 914
 915 let condi_of_wlofg = MESON[]` (!a b. P a b <=> P b a)
 916      ==> ((?a b. P a b /\ (x = a \/ x = b)) <=> (?a b. P a b /\ x = a))`;;
 917
 918 (* ============ *)
 919  let CARD_SET_OF_LIST_LE = prove
 920   (`!l. CARD(set_of_list l) <= LENGTH l`,
 921    LIST_INDUCT_TAC THEN
 922    SIMP_TAC[LENGTH; set_of_list; CARD_CLAUSES; FINITE_SET_OF_LIST] THEN
 923    ASM_ARITH_TAC);;
 924
 925  let HAS_SIZE_SET_OF_LIST = prove
 926   (`!l. (set_of_list l) HAS_SIZE (LENGTH l) <=> PAIRWISE (\x y. ~(x = y)) l`,
 927    REWRITE_TAC[HAS_SIZE; FINITE_SET_OF_LIST] THEN LIST_INDUCT_TAC THEN
 928    ASM_SIMP_TAC[CARD_CLAUSES; LENGTH; set_of_list; PAIRWISE; ALL;
 929                 FINITE_SET_OF_LIST; GSYM ALL_MEM; IN_SET_OF_LIST] THEN
 930    COND_CASES_TAC THEN ASM_REWRITE_TAC[SUC_INJ] THEN
 931    ASM_MESON_TAC[CARD_SET_OF_LIST_LE; ARITH_RULE `~(SUC n <= n)`]);;
 932
 933 (* ====================In your theorem we want the n=4 case, so we instantiate it:
 934 =========================== *)
 935
 936  let HAS_SIZE_SET_OF_LIST_4 = prove
 937   (`!a b c d:A. {a,b,c,d} HAS_SIZE 4 <=> PAIRWISE (\x y. ~(x = y)) [a;b;c;d]`,
 938    REPEAT GEN_TAC THEN MP_TAC(ISPEC `[a;b;c;d]:A list`HAS_SIZE_SET_OF_LIST) THEN
 939    REWRITE_TAC[LENGTH; set_of_list; ARITH])  ;;
 940
 941 (* ============================================================================
 942  Then finally, using this and a bit of straightforward rearrangement,
 943 we can collapse the desired theorem to a lemma that MESON can prove
 944 automatically:
 945 ===============================================================================*)
 946
 947  let SET_OF_4 = prove
 948   (`! a b c d. ( ? v1 v2 v3 v4:A. ~( v1 = v2 \/ v3 = v4 ) /\
 949                                 {v1, v2 } INTER {v3, v4 } = {} /\
 950                                 { a , b , c , d } = { v1 , v2, v3 ,v4}) <=>
 951     ~ ( a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d )`,
 952    REPEAT GEN_TAC THEN
 953    REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; INTER_EMPTY; SET_RULE
 954     `(a INSERT s) INTER t = {} <=> ~(a IN t) /\ s INTER t = {}`] THEN
 955    MP_TAC(MESON[]
 956     `(?v1 v2 v3 v4:A. {a,b,c,d} = {v1,v2,v3,v4} /\ {v1,v2,v3,v4} HAS_SIZE 4) <=>
 957      {a,b,c,d} HAS_SIZE 4`) THEN
 958    REWRITE_TAC[HAS_SIZE_SET_OF_LIST_4; PAIRWISE; ALL; DE_MORGAN_THM; CONJ_ACI]);;
 959
 960
 961 let def_simplex = prove(`! s a b c d. geomdetail'simplex {a, b, c, d} s <=>
 962   packing s /\
 963          {a, b, c, d} SUBSET s /\
 964   ~ ( a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d ) `, REWRITE_TAC[ simplex]
 965 THEN REPEAT GEN_TAC THEN MATCH_MP_TAC (MESON[] ` ( x <=> y ) ==> ( a /\ b /\ x <=>
 966 a /\ b /\ y ) `) THEN ONCE_REWRITE_TAC[MESON[]` {v1, v2, v3, v4} = {a, b, c, d} <=>
 967  {a, b, c, d}  = {v1, v2, v3, v4} ` ] THEN REWRITE_TAC[ SET_OF_4]);;
 968
 969
 970 (* =========== *)
 971
 972 let PAIR_D3 = prove(` ! i j u w. {u,w} = {i,j} ==> dist3 i j = dist3 u w `,
 973 REWRITE_TAC[ SET_RULE ` {u, w} = {i, j} <=>  u= i /\ w = j \/ u = j /\ w = i `] THEN
 974 MESON_TAC[ trg_dist3_sym]);;
 975
 976 let PAIR_DIST = prove(` ! i j u w. {u,w} = {i,j} ==> dist(i,j) = dist(u,w) `,
 977 REWRITE_TAC[ SET_RULE ` {u, w} = {i, j} <=>  u= i /\ w = j \/ u = j /\ w = i `] THEN
 978 MESON_TAC[ DIST_SYM]);;
 979
 980 (* ================== *)
 981
 982 let DOT_SUB_ADD = VECTOR_ARITH `! a b. b dot b - a dot a = (b - a) dot (b + a)` ;;
 983
 984 let DIST_LT_HALF_PLANE = prove(`!x:real^A a:real^A b:real^A.
 985     dist(x,a) < dist(x,b) <=> &0 < (a - b) dot (&2 % x - (a + b))`,
 986 ABBREV_TAC ` an a b x = ((a:real^A) - b) dot (&2 % x - (a + b))` THEN
 987 REWRITE_TAC[dist; vector_norm] THEN
 988 REWRITE_TAC[MESON[DOT_POS_LE; SQRT_MONO_LT_EQ]` sqrt ( x dot x) < sqrt (y dot y) <=>
 989   x dot x < y dot y `] THEN
 990 REWRITE_TAC[DOT_LSUB; DOT_RSUB] THEN
 991 SIMP_TAC[DOT_SYM] THEN
 992 ONCE_REWRITE_TAC[ GSYM REAL_SUB_LT] THEN
 993 REWRITE_TAC[ REAL_ARITH ` x dot x -
 994      b dot x -
 995      (b dot x - b dot b) -
 996      (x dot x - a dot x - (a dot x - a dot a)) =
 997      &2 * (a dot x - b dot x) + b dot b - a dot a`] THEN
 998 REWRITE_TAC[GSYM DOT_LSUB; GSYM DOT_RMUL] THEN
 999 REWRITE_TAC[DOT_SUB_ADD; VECTOR_ARITH `(b - a) dot (b + a) =
1000   ( -- ( a - b) ) dot ( a + b) `] THEN
1001 REWRITE_TAC[VECTOR_ARITH ` (a - b) dot &2 % x + --(a - b) dot (a + b) =
1002   (a-b) dot ( &2 % x - (a+b))`] THEN
1003 ASM_REWRITE_TAC[REAL_ARITH ` a - &0 = a` ]);;
1004
1005 let OR_IMP_EX = MESON[]` ! a b c. a \/ b ==> c <=> (a ==> c) /\ ( b ==> c)` ;;
1006
1007 let HALF_PLANE_CONV = prove(`! a b:real^N.  convex { x| x | dist(x,a) < dist (x,b) }`,
1008 REWRITE_TAC[DIST_LT_HALF_PLANE; convex; IN_ELIM_THM] THEN
1009 REWRITE_TAC[VECTOR_ARITH ` &2 % (u % x + v % y) - (a + b)
1010    = u % ( &2 % x ) + v % ( &2 % y ) - &1 % (a + b )`] THEN
1011 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN SIMP_TAC[] THEN
1012 REWRITE_TAC[VECTOR_ARITH ` (a - b) dot (u % &2 % x +
1013    v % &2 % y - (u + v) % (a + b))  = u * (a - b) dot (&2 % x - (a + b))
1014    + v * (a - b) dot (&2 % y - (a + b))`] THEN
1015 REWRITE_TAC[REAL_ARITH` &0 <= u /\ &0 <= v /\ &1 = u + v <=>
1016      &0 = u /\ &1 = v \/ &0 < u /\ &0 <= v /\ &1 = u + v`] THEN
1017 KHANANG THEN
1018 REWRITE_TAC[OR_IMP_EX] THEN
1019 ONCE_REWRITE_TAC[ EQ_SYM_EQ] THEN SIMP_TAC[] THEN
1020 REWRITE_TAC[REAL_POLY_CLAUSES] THEN
1021 SIMP_TAC[ REAL_ARITH ` a + &0 = a `] THEN
1022 NHANH (MESON[REAL_LT_MUL]`  &0 < (a - b) dot (&2 % x - (a + b)) /\
1023      &0 < (a - b) dot (&2 % y - (a + b)) /\
1024      &0 < u  /\ l ==> &0 < u * ((a - b) dot (&2 % x - (a + b)))`) THEN
1025 NHANH (MESON[REAL_ARITH` &0 < a ==> &0 <= a `; REAL_LE_MUL]`
1026   &0 < (a - b) dot (&2 % y - (a + b)) /\
1027       &0 < u /\
1028       &0 <= v /\ l ==> &0 <= v * ((a - b) dot (&2 % y - (a + b)))`)
1029  THEN REAL_ARITH_TAC);;
1030
1031 let HALF_PLANE_CONV_EP = REWRITE_RULE[convex; IN_ELIM_THM] HALF_PLANE_CONV;;
1032
1033 let VORONOI_CONV = prove( ` ! (s:real^A -> bool) v. convex (voronoi_open s v)`,
1034 REWRITE_TAC[voronoi_open] THEN REPEAT GEN_TAC THEN
1035 REWRITE_TAC[convex; IN_ELIM_THM] THEN MESON_TAC[HALF_PLANE_CONV_EP]);;
1036
1037 let CONVEX_IM_CONV2_SU = prove(`! s u v. convex s /\ u IN s /\ v IN s ==> conv {u,v} SUBSET s `,
1038 REWRITE_TAC[convex; CONV_SET2] THEN SET_TAC[]);;
1039
1040 (* have not added *)
1041
1042 let U_IN_CONV2 = prove(`! u v. u IN conv {u,v} `,
1043 REWRITE_TAC[ CONV_SET2; IN_ELIM_THM] THEN REPEAT GEN_TAC
1044 THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0 ` THEN
1045 REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
1046 REAL_ARITH_TAC);;
1047
1048 let UV_IN_CONV2 = prove(` ! u v. u IN conv {u,v} /\ v IN conv {u,v} `,
1049 MESON_TAC[U_IN_CONV2; SET_RULE ` {u,v} = {v,u} `]);;
1050
1051 let CONVEX_AS_CONV2 = prove(` ! s. convex s ==> ( ! u v. u IN s /\ v IN s <=>
1052    conv {u,v} SUBSET s )`, REWRITE_TAC[ EQ_EXPAND] THEN
1053 SIMP_TAC[CONVEX_IM_CONV2_SU ] THEN MESON_TAC[SUBSET; UV_IN_CONV2]);;
1054
1055 let CONV0_SING = prove(`! x:real^A . conv0 {x} = {x} `,
1056 REWRITE_TAC[conv0; FUN_EQ_THM; affsign; lin_combo] THEN
1057 REWRITE_TAC[UNION_EMPTY; VSUM_SING; SUM_SING; IN_ACT_SING; sgn_gt] THEN
1058 REWRITE_TAC[MESON[REAL_ARITH` &0 < &1 `]` (!w. x = w ==> &0 < f w) /\
1059   f x = &1 <=> f x = &1 `] THEN
1060 REWRITE_TAC[MESON[VECTOR_MUL_LID]` (?f. x' = f x % x /\ f x = &1) <=>
1061    x' = x /\ (? f. f x = &1 ) `] THEN
1062 MESON_TAC[prove(`!x:real^A. ? f. f x = &1`, GEN_TAC THEN EXISTS_TAC
1063   `(\x:real^A. &1)` THEN MESON_TAC[])]);;
1064
1065 let NOV10' = prove(`! x y.      (x = y
1066       ==> (!x. y = x <=>
1067                (?a b. &0 < a /\ &0 < b /\ a + b = &1 /\ x = a % y + b % y)))`,
1068 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN
1069 REWRITE_TAC[MESON[VECTOR_MUL_LID]` a + b = &1 /\
1070     x = (a + b) % y <=> a + b = &1 /\ x = y `] THEN
1071 MESON_TAC[prove(` ?a b. &0 < a /\ &0 < b /\ a + b = &1`, REPEAT
1072   (EXISTS_TAC ` &1 / &2 `) THEN REAL_ARITH_TAC)]);;
1073
1074 let CONV0_SET2 = prove(` ! x y:real^A. conv0 {x,y} = {w | ? a b. &0 < a /\ &0 < b /\ a + b = &1 /\
1075   w = a%x + b%y}`,
1076 ONCE_REWRITE_TAC[ MESON[] ` (! a b. P a b ) <=> ( ! a b. a = b \/ ~( a= b)
1077   ==> P a b )`] THEN
1078 REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a==> c) /\ ( b==> c)`] THEN
1079 SIMP_TAC[] THEN
1080 REWRITE_TAC[ SET_RULE ` {a,a} = {a}`; CONV0_SING; FUN_EQ_THM; IN_ELIM_THM] THEN
1081 REWRITE_TAC[ IN_ACT_SING; NOV10'] THEN
1082 REWRITE_TAC[conv0 ; sgn_gt; affsign; lin_combo] THEN
1083 REWRITE_TAC[UNION_EMPTY; IN_SET2] THEN
1084 ONCE_REWRITE_TAC[ MESON[]`  ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
1085   ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`] THEN
1086 REWRITE_TAC[ MESON[VSUM_DIS2; SUM_DIS2]` ~(x = y) /\
1087                     x' = vsum {x, y} ff /\ l /\ sum {x, y} f = &1 <=> ~(x = y) /\
1088                     x' = ff x + ff y /\ l /\ f x + f y = &1 `]  THEN
1089 REWRITE_TAC[ MESON[]` (!w. w = x \/ w = y ==> &0 < f w) <=> &0 < f x /\ &0 < f y`] THEN
1090 ONCE_REWRITE_TAC[ GSYM (MESON[]`  ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
1091   ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`)] THEN
1092 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
1093 REWRITE_TAC[ EQ_EXPAND] THEN
1094 SIMP_TAC[ MESON[]` ((?f. x' = f x % x + f y % y /\ (&0 < f x /\ &0 < f y) /\ f x + f y = &1)
1095   ==> (?a b. &0 < a /\ &0 < b /\ a + b = &1 /\ x' = a % x + b % y)) `] THEN
1096 STRIP_TAC THEN EXISTS_TAC ` (\(d:real^A). if d = x then (a:real) else b )` THEN
1097 ASM_SIMP_TAC[]);;
1098
1099 let CONV02_SU_CONV2 = prove(` ! u v. conv0 {u,v} SUBSET conv {u,v} `,
1100 REWRITE_TAC[ CONV_SET2; CONV0_SET2] THEN
1101 MP_TAC (REAL_ARITH ` ! a . &0 < a ==> &0 <= a `) THEN SET_TAC[]);;
1102
1103
1104 let CONVEX_IM_CONV02_SU = prove(`! s u v. convex s /\ u IN s /\ v IN s ==>
1105 conv0 {u, v} SUBSET s`,
1106 MESON_TAC[CONV02_SU_CONV2; CONVEX_IM_CONV2_SU; SUBSET_TRANS]);;
1107
1108 let PAIR_EQ_EXPAND =
1109  SET_RULE `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`;;
1110
1111 let IN_SET3 = SET_RULE ` x IN {a,b,c} <=> x = a \/ x = b \/ x = c `;;
1112
1113 let IN_SET4 = SET_RULE ` x IN {a,b,c,d} <=> x = a \/ x = b \/ x = c \/ x = d `;;
1114
1115 let FOUR_IN = SET_RULE `!a b c d. a IN {a,b,c,d} /\ b IN {a,b,c,d} /\c IN {a,b,c,d} /\ d IN {a,b,c,d} ` ;;
1116
1117 (* TAG 1 *)
1118
1119 let D3_REFL = prove(` !x. dist3 x x = &0 ` , MESON_TAC[dist3; DIST_REFL]);;
1120
1121 let db_t0_sq8 = MATCH_MP REAL_LT_RSQRT (REAL_ARITH ` #2.51 pow 2 < &8 `);;
1122
1123 let SUB_PACKING = prove(`!sub s.
1124      packing s /\ sub SUBSET s
1125      ==> (!x y. x IN sub /\ y IN sub /\ ~(x = y) ==> &2 <= dist3 x y)`,
1126 REWRITE_TAC[ packing; GSYM dist3] THEN SET_TAC[]);;
1127
1128 let DIST_PAIR_LEMMA = prove
1129  (`{a,b} = {c,d} ==> dist(a,b) = dist(c,d)`,
1130  REWRITE_TAC[PAIR_EQ_EXPAND] THEN MESON_TAC[DIST_SYM]);;
1131
1132 end;;