legacy/oldleg/geomdetail_08.ml

   1
   2 (* tchales, This does not run in Multivariate *)
   3
   4
   5 let TRIANGLE_IN_BARRIER = prove(` ! s v0 v1 v2 . {v0, v1, v2} IN barrier s
   6  ==> (!xx yy.
   7           ~(xx = yy) /\ {xx, yy} SUBSET {v1, v2, v0}
   8           ==> &2 <= dist (xx,yy) /\ dist (xx,yy) <= sqrt (&8)) /\
   9      ((!aa bb.
  10            aa IN {v1, v2, v0} /\ bb IN {v1, v2, v0} ==> dist (aa,bb) <= #2.51) \/
  11       (?aa bb.
  12            {aa, bb} SUBSET {v1, v2, v0} /\
  13            #2.51 < dist (aa,bb) /\
  14            (!x y.
  15                 ~({x, y} = {aa, bb}) /\ {x, y} SUBSET {v1, v2, v0}
  16                 ==> dist (x,y) <= #2.51)))`,
  17 REWRITE_TAC[ barrier; IN_ELIM_THM] THEN
  18 REWRITE_TAC[ GSYM (MESON[]` P {x, y, z} <=>
  19        (?a b c. P {a, b, c} /\ {x, y, z} = {a, b, c})`)] THEN
  20 MP_TAC A_LEMMA THEN
  21 REWRITE_TAC[ MESON[]` (! a b c d. P a b c d ==> las a b c d ) ==> (! a b c d .
  22   P a b c d \/ Q a b c d ==> las a b c d) <=>
  23   (! a b c d. P a b c d ==> las a b c d ) ==> (! a b c d .
  24   Q a b c d ==> las a b c d)`] THEN DISCH_TAC THEN
  25 NHANH (CUTHE2 CASES_OF_Q_SYS) THEN
  26 REPEAT GEN_TAC THEN
  27 MATCH_MP_TAC (MESON[]` ((? a. Q a) ==> l) /\ ((?a. R a ) ==> l) ==>
  28   (? a. P a /\ ( Q a \/ R a )) ==> l `) THEN
  29 REWRITE_TAC[ NOV1] THEN
  30 NHANH (CUTHE4 TRIANGLE_IN_STRICT_QUA) THEN
  31 MATCH_MP_TAC (MESON[]` (b ==> l) /\ ( a /\ c ==> l) ==> a /\ ( b \/ c ) ==> l`) THEN
  32 ASM_REWRITE_TAC[] THEN
  33 REWRITE_TAC[ strict_qua; quarter; SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`;  def_simplex] THEN
  34 PHA THEN
  35 REWRITE_TAC[ MESON[]` a /\ a /\ l <=> a /\ l `; packing ] THEN
  36 MATCH_MP_TAC (MESON[] `(a ==> aa) /\ (b ==> bb) ==> a /\ b ==> aa /\ (cc \/ bb)`) THEN
  37 SIMP_TAC[ SET_RULE `{a,b,c} = {c,a,b} `] THEN
  38 NHANH (SET_RULE `  {v0, v1, v2, v4} SUBSET s ==> {v0,v1,v2} SUBSET s `) THEN
  39 NHANH ( MESON[SET_RULE ` x IN a /\ a SUBSET s ==> s x `]`(!u v. s u /\ s v /\ ~(u = v) ==> &2 <= dist (u,v)) /\
  40        ({v0, v1, v2, v4} SUBSET s /\ {v0, v1, v2} SUBSET s) /\ l ==>
  41   (!u v. u IN {v0,v1,v2} /\ v IN {v0,v1,v2} /\ ~(u = v) ==> &2 <= dist (u,v))`) THEN
  42 REWRITE_TAC[t0] THEN
  43 NHANH ( MESON[PAIR_D3] ` d3 v w <= sqrt (&8) ==> (! x y. x IN {v0, v1, v2, v4} /\
  44                   y IN {v0, v1, v2, v4} /\ {x,y} = {v,w} ==> d3 x y <= sqrt (&8) )`) THEN
  45 REWRITE_TAC[ SET_RULE ` {a,b} SUBSET s <=> a IN s /\ b IN s `] THEN
  46 SIMP_TAC[ SET_RULE ` {a,b,c} = {c,a,b} `] THEN
  47 REWRITE_TAC[ GSYM d3 ] THEN
  48 MESON_TAC[ MATCH_MP REAL_LE_RSQRT (REAL_ARITH ` (&2 * #1.255 ) pow 2 <= &8 `);
  49   SET_RULE ` x IN {a,b,c} ==> x IN {a,b,c,d} `; REAL_ARITH ` a <= b /\ b <= c ==> a <= c `]);;
  50
  51 (* ============== *)
  52
  53
  54
  55 (* lemma 8.2 *)
  56
  57
  58
  59
  60
  61 let le1_82 = prove (`!s v0 Y.
  62      centered_pac s v0 /\
  63      w IN near2t0 v0 s /\
  64      Y =
  65      UNIONS
  66      {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s}
  67      ==> UNIONS {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2} IN barrier s} SUBSET
  68          Y`, SIMP_TAC[] THEN SET_TAC[]);;
  69
  70
  71
  72 let rhand_subset_lhand = prove (` ! (s:real^3 -> bool) (v0:real^3) Z Y.
  73      centered_pac s v0 /\
  74      Y =
  75      UNIONS
  76      {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
  77      Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s}
  78      ==>
  79          normball v0 t0 INTER voronoi v0 s DIFF (Y UNION Z) SUBSET
  80  normball v0 t0 INTER VC v0 s DIFF (Y UNION Z)`, REWRITE_TAC[ SET_RULE ` a INTER b DIFF c SUBSET a INTER d DIFF c <=>
  81      (!x. x IN a INTER b DIFF c ==> x IN d) ` ] THEN
  82 REWRITE_TAC[ GSYM (     MESON[centered_pac; le1_82; prove (` ! x s. centered_pac s x ==> x IN near2t0 x s `, REWRITE_TAC[
  83   centered_pac; near2t0] THEN REWRITE_TAC[ MESON [DIST_REFL; t0; REAL_ARITH ` &0 < &2 * #1.255 `] `
  84   packing s /\ v0 IN s <=> packing s /\ v0 IN s /\ dist (v0,v0) < &2 * t0`] THEN
  85   SET_TAC[] ) ] ` !s v0 Z Y.
  86    centered_pac s v0 /\
  87      Y =
  88      UNIONS
  89      {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
  90      Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\
  91      UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
  92      Y
  93      ==> last <=>
  94      centered_pac s v0 /\
  95      Y =
  96      UNIONS
  97      {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
  98      Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s}
  99      ==> last `)] THEN
 100 REWRITE_TAC[SET_RULE ` x IN a INTER b DIFF c <=> x IN a /\ x IN b /\ ~( x IN c )`] THEN
 101 REWRITE_TAC[ MESON[] ` centered_pac s v0 /\
 102      Y =
 103      UNIONS
 104      {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
 105      Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\
 106      UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
 107      Y
 108      ==> (!x. x IN normball v0 t0 /\ x IN voronoi v0 s /\ ~(x IN Y UNION Z)
 109               ==> x IN VC v0 s) <=>
 110      centered_pac s v0 /\
 111      Y =
 112      UNIONS
 113      {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
 114      Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\
 115      UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
 116      Y
 117      ==> (!x. x IN normball v0 t0 /\
 118               x IN voronoi v0 s /\
 119               ~(x IN Y UNION Z) /\
 120               UNIONS
 121               {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
 122               Y
 123               ==> x IN VC v0 s) `] THEN
 124 ONCE_REWRITE_TAC[ SET_RULE ` ~(x IN Y UNION Z) /\
 125      UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
 126      Y <=>
 127      ~(x IN
 128        UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s}) /\
 129      ~(x IN Y UNION Z) /\
 130      UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
 131      Y `] THEN REWRITE_TAC[ centered_pac ] THEN
 132 REWRITE_TAC[ MESON[] ` (packing s /\ v0 IN s) /\
 133      Y =
 134      UNIONS
 135      {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
 136      Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\
 137      UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
 138      Y
 139      ==> (!x. x IN normball v0 t0 /\
 140               x IN voronoi v0 s /\
 141               ~(x IN
 142                 UNIONS
 143                 {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s}) /\
 144               ~(x IN Y UNION Z) /\
 145               UNIONS
 146               {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
 147               Y
 148               ==> x IN VC v0 s) <=>
 149      (packing s /\ v0 IN s) /\
 150      Y =
 151      UNIONS
 152      {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
 153      Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\
 154      UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
 155      Y
 156      ==> (!x. v0 IN s /\
 157               x IN normball v0 t0 /\
 158               x IN voronoi v0 s /\
 159               ~(x IN
 160                 UNIONS
 161                 {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s}) /\
 162               ~(x IN Y UNION Z) /\
 163               UNIONS
 164               {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
 165               Y
 166               ==> x IN VC v0 s) `] THEN
 167 REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[normball] THEN
 168 REWRITE_TAC[ SET_RULE ` z IN { x | P x } <=> P z `] THEN
 169 REWRITE_TAC[ voronoi; VC; lambda_x; d3 ] THEN
 170 REWRITE_TAC[ SET_RULE ` x IN { x | P x } <=> P x `] THEN
 171 REWRITE_TAC[MESON[DIST_SYM ; import_le ] ` v0 IN s /\
 172      dist (x,v0) < t0 /\
 173      (!w. s w /\ ~(w = v0) ==> dist (x,v0) < dist (x,w)) /\
 174      ~(x IN
 175        UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s}) /\
 176      ~(x IN Y UNION Z) /\
 177      UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
 178      Y <=>
 179      v0 IN s /\
 180      dist (x,v0) < t0 /\
 181      (!w. s w /\ ~(w = v0) ==> dist (x,v0) < dist (x,w)) /\
 182      ~(x IN
 183        UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s}) /\
 184      ~(x IN Y UNION Z) /\
 185      UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
 186      Y /\
 187      ~obstructed v0 x s `] THEN
 188 ONCE_REWRITE_TAC[MESON[t0; REAL_ARITH ` #1.255 < &2 /\ (! a b (c:real). a < b
 189 /\ b < c ==> a < c ) `; DIST_SYM ]` dist ( x, v0 ) < t0 <=> dist ( x, v0 ) < t0 /\
 190  dist ( v0, x) < &2 `] THEN
 191 SIMP_TAC[ DIST_SYM ] THEN
 192 MESON_TAC[ SET_RULE ` ! s x. s x <=> x IN s `]);;
 193
 194
 195
 196 (* ++++++++++++++++++++++++++++ *)
 197
 198
 199
 200
 201 let lhand_subset_rhand = prove(`  ! (s:real^3 -> bool) (v0:real^3) Z Y.
 202      centered_pac s v0 /\
 203      Y =
 204      UNIONS
 205      {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
 206      Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s}
 207      ==> normball v0 t0 INTER VC v0 s DIFF (Y UNION Z) SUBSET
 208          normball v0 t0 INTER voronoi v0 s DIFF (Y UNION Z)`,
 209 REWRITE_TAC[ SET_RULE ` a INTER b DIFF c SUBSET a INTER d DIFF c <=>
 210      a INTER b DIFF c DIFF d = {} `] THEN
 211 REWRITE_TAC[ SET_RULE ` a = {} <=> (! x. ~ (x IN a))`] THEN
 212 REWRITE_TAC[ SET_RULE` x IN a DIFF b <=> x IN a /\ ~( x IN b ) `] THEN
 213 REWRITE_TAC[ SET_RULE ` x IN a INTER b <=> x IN a /\ x IN b `] THEN PHA THEN
 214 REWRITE_TAC[ SET_RULE ` x IN normball v0 t0 /\ x IN VC v0 s /\ ~(x IN Y UNION Z) /\ P x  <=>
 215      x IN normball v0 t0 DIFF Z /\ x IN VC v0 s /\ ~(x IN Y UNION Z) /\ P x  `] THEN
 216 REWRITE_TAC[MESON[lemma_of_lemma82]`
 217   centered_pac s v0 /\
 218      Y =
 219      UNIONS
 220      {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
 221      Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s}
 222      ==> (!x. ~(x IN normball v0 t0 DIFF Z /\
 223                 x IN VC v0 s /\
 224                 ~(x IN Y UNION Z) /\
 225                 ~(x IN voronoi v0 s))) <=>
 226      centered_pac s v0 /\
 227      Y =
 228      UNIONS
 229      {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
 230      Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s}
 231      ==> (!x. ~(x IN normball v0 t0 DIFF Z /\
 232                 (?w. w IN near2t0 v0 s /\ x IN voronoi w s) /\
 233                 x IN VC v0 s /\
 234                 ~(x IN Y UNION Z) /\
 235                 ~(x IN voronoi v0 s))) `] THEN
 236 REWRITE_TAC[ MESON[] `
 237   (?w. w IN near2t0 v0 s /\ x IN voronoi w s) /\
 238      x IN VC v0 s /\
 239      ~(x IN Y UNION Z) /\
 240      ~(x IN voronoi v0 s) <=>
 241      (?w. w IN near2t0 v0 s /\ x IN voronoi w s /\ ~(w = v0)) /\
 242      x IN VC v0 s /\
 243      ~(x IN Y UNION Z) /\
 244      ~(x IN voronoi v0 s) `] THEN
 245 REWRITE_TAC[ MESON[near2t0] `
 246   (?w. w IN near2t0 v0 s /\ x IN voronoi w s /\ ~(w = v0)) <=>
 247      (?w. w IN {x | x IN s /\ dist (v0,x) < &2 * t0} /\
 248           x IN voronoi w s /\
 249           ~(w = v0)) `] THEN
 250 REWRITE_TAC[ SET_RULE` a IN { a | p a } <=> p a `] THEN
 251 REWRITE_TAC[ voronoi; lambda_x] THEN
 252 REWRITE_TAC[ SET_RULE ` x IN { v | P v } <=> P x `] THEN PHA THEN
 253 REWRITE_TAC[ MESON[] ` a /\ b /\ d ==> c <=> b /\ d ==> a ==> c `] THEN
 254 REPEAT GEN_TAC THEN DISCH_TAC THEN
 255 REWRITE_TAC[centered_pac] THEN
 256 MATCH_MP_TAC (MESON[]` (a /\ b ==> (!x. ~b \/ P x)) ==> a /\ b ==> (!x. P x)`) THEN
 257 REWRITE_TAC[ MESON[] ` ~(v0 IN s) \/ ~(x IN normball v0 t0 DIFF Z /\ last) <=>
 258      ~(v0 IN s /\ x IN normball v0 t0 DIFF Z /\ last)`] THEN
 259 REWRITE_TAC[ MESON[]`
 260   v0 IN s /\
 261      x IN normball v0 t0 DIFF Z /\
 262      (?w. w IN s /\
 263           dist (v0,w) < &2 * t0 /\
 264           (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
 265           ~(w = v0)) /\
 266      last <=>
 267      x IN normball v0 t0 DIFF Z /\
 268      (?w. w IN s /\
 269           v0 IN s /\
 270           dist (v0,w) < &2 * t0 /\
 271           (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
 272           ~(w = v0)) /\
 273      last`] THEN
 274 REWRITE_TAC[ MESON[ SET_RULE` x IN s <=> s x `] `
 275   (?w. w IN s /\
 276           v0 IN s /\
 277           dist (v0,w) < &2 * t0 /\
 278           (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
 279           ~(w = v0)) <=>
 280      (?w. w IN s /\
 281           v0 IN s /\
 282           dist (x,w) < dist (x,v0) /\
 283           dist (v0,w) < &2 * t0 /\
 284           (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
 285           ~(w = v0)) `] THEN
 286 REWRITE_TAC[ SET_RULE ` x IN a DIFF b <=> x IN a /\ ~ ( x IN b ) `] THEN
 287 REWRITE_TAC[ MESON[normball ; SET_RULE `x IN { x | p x } <=> p x `] ` x IN normball v0 t0
 288   <=> dist (x,v0) < t0 `] THEN
 289 REWRITE_TAC[ MESON[REAL_ARITH ` a < b /\ b < c ==> a < c `]`
 290   (dist (x,v0) < t0 /\ ~(x IN Z)) /\
 291             (?w. w IN s /\
 292                  v0 IN s /\
 293                  dist (x,w) < dist (x,v0) /\
 294                  dist (v0,w) < &2 * t0 /\
 295                  (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
 296                  ~(w = v0)) /\ las
 297   <=> (dist (x,v0) < t0 /\ ~(x IN Z)) /\
 298             (?w. w IN s /\
 299                  v0 IN s /\ dist(x,w) < t0 /\
 300                  dist (x,w) < dist (x,v0) /\
 301                  dist (v0,w) < &2 * t0 /\
 302                  (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
 303                  ~(w = v0)) /\ las  `] THEN
 304 ASM_SIMP_TAC[] THEN PHA THEN
 305 REWRITE_TAC[ MESON[] ` a /\ b /\ c /\ d /\ las <=> (a /\ d ) /\ b /\ c /\ las `] THEN
 306 ONCE_REWRITE_TAC[ MESON[near2t0; SET_RULE ` x IN { x | p x } <=> p x ` ]` (w IN s /\ dist (v0,w) < &2 * t0) <=>
 307   w IN near2t0 v0 s /\ (w IN s /\ dist (v0,w) < &2 * t0) `] THEN
 308 REWRITE_TAC[ SET_RULE ` ~ ( x IN a UNION b) <=> ~( x IN a ) /\ ~ (x IN b)`] THEN PHA THEN
 309  SIMP_TAC[MESON[] ` a /\ a /\ b <=> a /\ b `] THEN
 310 REWRITE_TAC[ MESON[] ` a/\ b /\ ( ? w. P w ) /\ la <=> b /\ ( ? w. a /\ P w ) /\ la `] THEN
 311 ONCE_REWRITE_TAC[  MESON[ SET_RULE ` w IN near2t0 v0 s
 312      ==> UNIONS {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2} IN barrier s} SUBSET
 313          UNIONS
 314          {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} `]
 315   `  w IN near2t0 v0 s /\
 316                  w IN s /\ last
 317   <=> UNIONS {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2} IN barrier s} SUBSET
 318          UNIONS
 319          {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
 320   w IN near2t0 v0 s /\
 321                  w IN s /\ last `] THEN
 322 REWRITE_TAC[ MESON[] ` a /\ b /\ c /\ d /\ last <=> a /\ b /\ ( c/\ d ) /\ last `] THEN
 323 REWRITE_TAC[ SET_RULE ` ~ ( x IN a ) /\ b SUBSET a <=> ~ ( x IN a )/\ ~( x IN b ) /\ b SUBSET a`] THEN PHA THEN
 324 REWRITE_TAC[ MESON[DIST_SYM; import_le ] ` dist (x,v0) < t0 /\
 325                  x IN VC v0 s /\
 326                  ~(x IN
 327                    UNIONS
 328                    {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\
 329                                           {w, w1, w2} IN barrier s}) /\
 330                  ~(x IN
 331                    UNIONS
 332                    {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2} IN barrier s}) /\
 333                  UNIONS
 334                  {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2} IN barrier s} SUBSET
 335                  UNIONS
 336                  {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\
 337                                         {w, w1, w2} IN barrier s} /\
 338                  w IN near2t0 v0 s /\
 339                  w IN s /\
 340                  dist (v0,w) < &2 * t0 /\
 341                  (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
 342                  dist (x,w) < t0 /\
 343                  dist (x,w) < dist (x,v0) /\
 344                  ~(w = v0)
 345   <=> dist (x,v0) < t0 /\
 346                  x IN VC v0 s /\
 347                  ~(x IN
 348                    UNIONS
 349                    {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\
 350                                           {w, w1, w2} IN barrier s}) /\
 351                  ~(x IN
 352                    UNIONS
 353                    {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2} IN barrier s}) /\
 354                  UNIONS
 355                  {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2} IN barrier s} SUBSET
 356                  UNIONS
 357                  {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\
 358                                         {w, w1, w2} IN barrier s} /\
 359                  w IN near2t0 v0 s /\
 360                  w IN s /\
 361                  dist (v0,w) < &2 * t0 /\
 362                  (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
 363                  dist (x,w) < t0 /\
 364                  dist (x,w) < dist (x,v0) /\
 365                  ~(w = v0) /\ ~obstructed w x s `] THEN
 366 ONCE_REWRITE_TAC[ MESON[t0; REAL_ARITH ` #1.255 < &2 /\ (! a b c. a < b /\ b < c ==> a < c )` ] `
 367   dist (x,w) < t0 /\ dist (x,w) < dist (x,v0) /\ last <=>
 368      dist (x,w) < &2 /\ dist (x,w) < t0 /\ dist (x,w) < dist (x,v0) /\ last`] THEN
 369 REWRITE_TAC[ MESON[ in_VC; DIST_SYM ] `w IN s /\
 370      dist (v0,w) < &2 * t0 /\
 371      (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
 372      dist (x,w) < &2 /\
 373      dist (x,w) < t0 /\
 374      dist (x,w) < dist (x,v0) /\
 375      ~(w = v0) /\
 376      ~obstructed w x s <=>
 377      dist (v0,w) < &2 * t0 /\
 378      dist (x,w) < t0 /\
 379      ~(w = v0) /\
 380      dist (x,w) < dist (x,v0) /\
 381      w IN s /\
 382      (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
 383      dist (x,w) < &2 /\
 384      ~obstructed w x s` ]  THEN
 385 REWRITE_TAC[ MESON[DIST_SYM] ` dist(x,w) < &2 <=> dist (w,x) < &2 `] THEN
 386 REWRITE_TAC[MESON[in_VC]` w IN s /\
 387                  (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
 388                  dist (w,x) < &2 /\
 389                  ~obstructed w x s
 390   <=> w IN s /\
 391                  (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
 392                  dist (w,x) < &2 /\
 393                  ~obstructed w x s /\ x IN VC w s ` ] THEN
 394 REWRITE_TAC[ MESON[]`  ~(w = v0) /\
 395                  dist (x,w) < dist (x,v0) /\
 396                  w IN s /\
 397                  (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
 398                  dist (w,x) < &2 /\
 399                  ~obstructed w x s /\
 400                  x IN VC w s <=>
 401
 402                  dist (x,w) < dist (x,v0) /\
 403                  w IN s /\
 404                  (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
 405                  dist (w,x) < &2 /\
 406                  ~obstructed w x s /\
 407                ~(w = v0) /\  x IN VC w s `] THEN
 408 ONCE_REWRITE_TAC[ MESON[]` dist (x,v0) < t0 /\
 409                  x IN VC v0 s /\ last <=> dist (x,v0) < t0  /\ last /\ x IN VC v0 s `]
 410 THEN PHA THEN
 411 ONCE_REWRITE_TAC[SET_RULE ` x IN a /\ x IN b <=> ~ ( a INTER b = {} ) /\ x IN a /\ x IN b `] THEN
 412 SIMP_TAC[ MESON[VC_DISJOINT ] `  ~(w = v0) /\
 413                  ~(VC w s INTER VC v0 s = {}) /\
 414                  x IN VC w s /\
 415                  x IN VC v0 s <=> F `]);;
 416
 417
 418 (* +++++++++++++++++++++++++ *)
 419
 420 let lemma82_FOCUDTG = prove (`! (s:real^3 -> bool) (v0:real^3) Z Y.
 421      centered_pac s v0 /\
 422      Y =
 423      UNIONS
 424      {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
 425      Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s}
 426      ==> normball v0 t0 INTER VC v0 s DIFF (Y UNION Z) =
 427          normball v0 t0 INTER voronoi v0 s DIFF (Y UNION Z)`,
 428   REWRITE_TAC[ SET_RULE ` a ==> (b = c) <=> a ==>( b SUBSET c /\ c SUBSET b ) `]
 429   THEN MESON_TAC[ lhand_subset_rhand; rhand_subset_lhand] );;
 430
 431 (* ========= END LEMMA 8.2 ======== *)
 432
 433 let a_le_sub = SET_RULE ` w IN near2t0 v0 s
 434      ==> UNIONS {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2} IN barrier s} SUBSET
 435          UNIONS
 436          {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} `;;
 437
 438
 439
 440
 441
 442
 443
 444
 445
 446
 447
 448
 449
 450
 451
 452
 453
 454
 455
 456
 457
 458
 459 (* ============= BEGIN LEMMA 8.3 =========== *)
 460
 461
 462 let barrier' = new_definition ` barrier' v0 s =
 463          {{a, b, c} | {a, b, c} IN barrier s /\ v0 IN {a, b, c} \/
 464                       (?q. diagonal a b q s /\ q IN Q_SYS s /\ c IN anchor_points a b s)} `;;
 465
 466
 467 let lemma7_7_CXRHOVG = new_axiom `!s q1 q2 v w.
 468          {v, w} SUBSET q1 INTER q2 /\ quarter q2 s /\  diagonal v w q1 s /\ q1 IN Q_SYS s
 469          ==> q2 IN Q_SYS s `;;
 470
 471
 472 let tarski_UMMNOJN = new_axiom` !x w v0 v1 v2.
 473          ~(conv {x, w} INTER cone v0 {v1, v2} = {}) /\
 474          dist (x,v0) < dist (x,v1) /\
 475          dist (x,v0) < dist (x,v2) /\
 476          dist (x,w) < dist (x,v0) /\
 477          (!xx yy.
 478               ~(xx = yy) /\ {xx, yy} SUBSET {v1, v2, v0}
 479               ==> &2 <= dist (xx,yy) /\ dist (xx,yy) <= sqrt (&8)) /\
 480          ((!aa bb.
 481                aa IN {v1, v2, v0} /\ bb IN {v1, v2, v0}
 482                ==> dist (aa,bb) <= #2.51) \/
 483           (?aa bb.
 484                {aa, bb} SUBSET {v1, v2, v0} /\
 485                #2.51 < dist (aa,bb) /\
 486                (!x y.
 487                     ~({x, y} = {aa, bb}) /\ {x, y} SUBSET {v1, v2, v0}
 488                     ==> dist (x,y) <= #2.51)))
 489          ==> (!a. a IN {v1, v2, v0} ==> dist (w,a) <= #2.51) /\
 490              ~(conv {v0, v1, v2} INTER conv0 {x, w} = {}) `;;
 491
 492 (* ================ *)
 493
 494 let TRIANGLE_IN_BARRIER' = prove(
 495 `!s v0 v1 v2.
 496      {v0, v1, v2} IN barrier' v0 s
 497      ==> (!xx yy.
 498               ~(xx = yy) /\ {xx, yy} SUBSET {v1, v2, v0}
 499               ==> &2 <= dist (xx,yy) /\ dist (xx,yy) <= sqrt (&8)) /\
 500   ((!aa bb.
 501                aa IN {v1, v2, v0} /\ bb IN {v1, v2, v0}
 502                ==> dist (aa,bb) <= #2.51) \/
 503           (?aa bb.
 504                {aa, bb} SUBSET {v1, v2, v0} /\
 505                #2.51 < dist (aa,bb) /\
 506                (!x y.
 507                     ~({x, y} = {aa, bb}) /\ {x, y} SUBSET {v1, v2, v0}
 508                     ==> dist (x,y) <= #2.51))) `,
 509 REWRITE_TAC[ barrier'; IN_ELIM_THM] THEN MATCH_MP_TAC (MESON[] ` (!s v0 v1 v2.
 510           (?a b c.
 511                ({a, b, c} IN barrier s /\ v0 IN {a, b, c} \/
 512                 (?q. diagonal a b q s /\ c IN anchor_points a b s)) /\
 513                {v0, v1, v2} = {a, b, c})
 514           ==> las s v0 v1 v2 )
 515      ==> (!s v0 v1 v2.
 516               (?a b c.
 517                    ({a, b, c} IN barrier s /\ v0 IN {a, b, c} \/
 518                     (?q. diagonal a b q s /\
 519                          q IN Q_SYS s /\
 520                          c IN anchor_points a b s)) /\
 521                    {v0, v1, v2} = {a, b, c})
 522               ==> las s v0 v1 v2 )`) THEN
 523 REWRITE_TAC[ MESON[]` ( ? a b c. ( P {a,b,c} \/ Q a b c ) /\ {v0, v1, v2} = {a, b, c} ) <=>
 524   P {v0, v1, v2} \/ ( ? a b c. Q a b c  /\ {v0, v1, v2} = {a, b, c} ) `] THEN
 525 REPEAT GEN_TAC THEN
 526 MATCH_MP_TAC (MESON[]` (a ==> l) /\ (c ==> l) ==> a /\ b \/ c ==> l`) THEN
 527 REWRITE_TAC[ TRIANGLE_IN_BARRIER] THEN
 528 NHANH (CUTHE4 DIA_OF_QUARTER) THEN
 529 REWRITE_TAC[ anchor_points; IN_ELIM_THM; anchor] THEN
 530 NHANH (MESON[diagonal; quarter] ` diagonal a b q s ==> packing s `) THEN PHA THEN
 531 REWRITE_TAC[ MESON[] ` packing s /\ aa /\ bb /\ cc /\ {c, a, b} SUBSET s /\ l
 532   <=> ( packing s /\ {c, a, b} SUBSET s ) /\ aa /\ bb /\ cc /\ l `] THEN
 533 NHANH (CUTHE2 SUB_PACKING ) THEN
 534 REWRITE_TAC[GSYM d3] THEN
 535 REWRITE_TAC[ REAL_ARITH ` &2 * t0 <= d3 a b <=> d3 a b <= &2 * t0 /\ &2 * t0 = d3 a b  \/ &2 * t0
 536   < d3 a b `; t0; REAL_ARITH ` &2 * #1.255 = #2.51 ` ] THEN
 537 REWRITE_TAC[ SET_RULE ` {x,y} SUBSET s <=> x IN s /\ y IN s`] THEN
 538 SIMP_TAC[ SET_RULE `!a b c.  {c, a, b} = {a, b, c}`] THEN PHA THEN
 539 REWRITE_TAC[ MESON[]` a /\ b /\ a /\ l <=> a /\ b /\ l `] THEN
 540 KHANANG THEN
 541 REWRITE_TAC[ MESON[]` (?q. P q /\ l1 \/ P q /\ l2) <=> (?q. P q) /\ (l1 \/ l2)`] THEN
 542 PHA THEN
 543 MATCH_MP_TAC (MESON[] ` ((? a b c. Q a b c) ==> l) ==> (? a b c. P a b c /\ Q a b c ) ==> l `) THEN
 544 REWRITE_TAC[ MESON[]` ( a \/ b ) /\ c <=> a /\ c \/ b /\ c `] THEN
 545 ONCE_REWRITE_TAC[ MESON[]` (d3 a b <= #2.51 /\ l <=> l /\ d3 a b <= #2.51) /\
 546   (#2.51 < d3 a b /\ l <=> l /\ #2.51 < d3 a b) `] THEN PHA THEN
 547 REWRITE_TAC[ MESON[]` d3 c a <= #2.51 /\
 548       d3 c b <= #2.51 /\
 549       d3 a b <= #2.51 /\ l <=> ( d3 a b <= #2.51 /\
 550       d3 c a <= #2.51 /\
 551       d3 c b <= #2.51 ) /\ l `] THEN
 552 NHANH ( CUTHE3 (
 553 prove(`! a b c. d3 a b <= #2.51 /\ d3 c a <= #2.51 /\
 554        d3 c b <= #2.51 ==> (!aa bb. aa IN {a,b,c} /\ bb IN {a,b,c} ==> d3 aa bb <= #2.51)`,
 555 REWRITE_TAC[ SET_RULE ` x IN {a,b,c} <=> x = a \/ x= b \/  x= c `] THEN
 556 MESON_TAC[ D3_REFL; trg_d3_sym; REAL_ARITH ` &0 <= #2.51 `]))) THEN
 557 REWRITE_TAC[ MESON[] ` d3 a b <= sqrt (&8) /\
 558      d3 a b >= #2.51 /\
 559      d3 c a <= #2.51 /\
 560      d3 c b <= #2.51 /\
 561      #2.51 < d3 a b /\
 562      l <=>
 563      d3 a b >= #2.51 /\
 564      l /\
 565      #2.51 < d3 a b /\
 566      d3 a b <= sqrt (&8) /\
 567      d3 c a <= #2.51 /\
 568      d3 c b <= #2.51 `] THEN
 569 NHANH (CUTHE3 (
 570 prove(`!a b c.
 571      #2.51 < d3 a b /\
 572      d3 a b <= sqrt (&8) /\
 573      d3 c a <= #2.51 /\
 574      d3 c b <= #2.51
 575      ==> (?aa bb.
 576               aa IN {a, b, c} /\
 577               bb IN {a, b, c} /\
 578               #2.51 < d3 aa bb /\
 579               (!x y.
 580                    ~({x, y} = {aa, bb}) /\ x IN {a, b, c} /\ y IN {a, b, c}
 581                    ==> d3 x y <= #2.51)) /\
 582          (!xx yy.
 583               ~(xx = yy) /\ xx IN {a,b,c} /\ yy IN {a,b,c}
 584               ==> d3 xx yy <= sqrt (&8))`,
 585 REWRITE_TAC[ MESON[]` (? a b. P a b ) /\ l <=> (? a b. P a b /\ l ) `] THEN
 586 REWRITE_TAC[ SET_RULE ` x IN {a,b,c} <=> x = a \/ x = b \/ x = c `] THEN
 587 REPEAT GEN_TAC THEN DISCH_TAC THEN EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`
 588 THEN FIRST_X_ASSUM MP_TAC THEN
 589 REWRITE_TAC[ SET_RULE `{a,b} ={x,y} <=> a = x /\ b = y \/ a = y /\ b = x `] THEN
 590 MESON_TAC[trg_d3_sym; db_t0_sq8; D3_REFL; REAL_ARITH ` &0 <= #2.51 /\ (! a b c. a <= b /\ b < c ==> a <= c )`]))) THEN
 591 PHA THEN
 592 ONCE_REWRITE_TAC[ MESON[] `(! x y. P x y ) /\ l <=> l /\ (! x y. P x y) `] THEN
 593 PHA THEN
 594 ONCE_REWRITE_TAC[ SET_RULE ` {v0, v1, v2} = {a, b, c} <=> {v1, v2, v0} = {a, b, c}`] THEN
 595 NHANH ( MESON[db_t0_sq8 ; REAL_ARITH ` a <= b /\ b < c ==> a <= c `]` (!aa bb. aa IN {a, b, c} /\ bb IN {a, b, c} ==> d3 aa bb <= #2.51) /\
 596       {v1, v2, v0} = {a, b, c} /\
 597       (!x y. x IN {a, b, c} /\ y IN {a, b, c} /\ ~(x = y) ==> &2 <= d3 x y)
 598   ==> (! x y. ~(x=y) /\ x IN {v1,v2,v0} /\ y IN {v1,v2,v0}==> &2 <= d3 x y /\
 599   d3 x y <= sqrt (&8)) `) THEN
 600 PHA THEN REWRITE_TAC[ MESON[]` {v1, v2, v0} = {a, b, c} /\ l <=> l /\ {v1, v2, v0} = {a, b, c}`] THEN PHA THEN
 601 PURE_ONCE_REWRITE_TAC[ MESON[]` P {a,b,c} /\ Q {a,b,c} /\ R {a,b,c} /\ {v1,v2,v0} = {a,b,c} <=> P {v1,v2,v0} /\
 602   Q {v1,v2,v0} /\ R {v1,v2,v0} /\ {v1,v2,v0} = {a,b,c} ` ] THEN
 603 MESON_TAC[]);;
 604
 605
 606 (* -----------
 607 -------------- *)
 608
 609
 610 let NOV6 = prove(` ! s v0 v1 v2 w. packing s /\
 611   CARD {v0, v1, v2, w} = 4 /\
 612  (!a. a IN {v1, v2, v0} ==> dist (w,a) <= #2.51) /\
 613  {v0, v1, v2, w} SUBSET s /\
 614  (?a b c.
 615       {a, b, c} = {v0, v1, v2} /\
 616       &2 * t0 <= d3 a b /\
 617       d3 a b <= sqrt (&8) /\
 618       c IN anchor_points a b s)
 619  ==> quarter {v0, v1, v2, w} s`,
 620 REWRITE_TAC[ quarter; def_simplex] THEN
 621 REWRITE_TAC[ prove(`! v0 v1 v2 w. CARD {v0, v1, v2, w} = 4  <=> ~(v0 = v1 \/ v0 = v2 \/ v0 = w \/ v1 = v2 \/ v1 = w \/ v2 = w)`,
 622   REWRITE_TAC[ CARD4] THEN SET_TAC[])] THEN
 623 SIMP_TAC[] THEN
 624 NHANH ( SET_RULE ` {a, b, c} = {v0, v1, v2} ==> a IN {v0,v1,v2,w} /\
 625   b IN {v0,v1,v2,w} `) THEN
 626 REWRITE_TAC[ MESON[]` (!a . P a ) /\ a /\ (? a b c. Q a b c) <=>
 627   a /\ (?a b c. Q a b c /\ (!a . P a ))`] THEN
 628 REWRITE_TAC[ anchor_points; anchor; IN_ELIM_THM] THEN PHA THEN
 629 SIMP_TAC[ SET_RULE ` {v1, v2, v0} = {v0, v1, v2}`] THEN
 630 PURE_ONCE_REWRITE_TAC[ MESON []`  {a, b, c} = {v0, v1, v2} /\ P {v0, v1, v2}
 631   <=> {a, b, c} = {v0, v1, v2} /\ P {a, b, c}`] THEN
 632 ONCE_REWRITE_TAC[ DIST_SYM] THEN
 633 REWRITE_TAC[ GSYM d3 ] THEN
 634 REWRITE_TAC[ MESON[t0; REAL_ARITH ` #2.51 = &2 * #1.255 `] ` #2.51 = &2 * t0 `] THEN
 635 NHANH (CUTHE4 SHORT_EDGES) THEN
 636 PURE_ONCE_REWRITE_TAC[ SET_RULE ` {a, b, c, w} = w INSERT {a,b,c} `] THEN
 637 PURE_ONCE_REWRITE_TAC[ GSYM (MESON []`  {a, b, c} = {v0, v1, v2} /\ P {v0, v1, v2}
 638   <=> {a, b, c} = {v0, v1, v2} /\ P {a, b, c}`)] THEN MESON_TAC[]);;
 639
 640 (* ============ *)
 641
 642 let NOV7 = prove(`!s v0 v1 v2 w x . CARD {v0, v1, v2, w, x} = 5 /\
 643      (!a. a IN {v1, v2, v0} ==> dist (w,a) <= #2.51) /\
 644      {v0, v1, v2, w} SUBSET s /\
 645      (?a b c.
 646           (?q. diagonal a b q s /\ q IN Q_SYS s /\ c IN anchor_points a b s) /\
 647           {v0, v1, v2} = {a, b, c})
 648      ==> {v0, v1, v2, w} IN Q_SYS s`,
 649 ONCE_REWRITE_TAC[ SET_RULE ` {v0, v1, v2, w, x} = {x,v0, v1, v2, w}`] THEN
 650 REWRITE_TAC[CARD5; GSYM CARD4] THEN
 651 NHANH (CUTHE4 DIA_OF_QUARTER) THEN
 652 NHANH (MESON[diagonal; quarter] `diagonal a b q s ==> packing s `) THEN
 653 PHA THEN REWRITE_TAC[ MESON[]` (?q. diagonal a b q s /\ a1 /\ a2 /\ a3 /\ q IN Q_SYS s /\ a4) <=>
 654      a1 /\ a2 /\ a3 /\ a4 /\ (?q. diagonal a b q s /\ q IN Q_SYS s) `] THEN
 655 NHANH ( MESON[NOV6]` CARD {v0, v1, v2, w} = 4 /\
 656      (!a. a IN {v1, v2, v0} ==> dist (w,a) <= #2.51) /\
 657      {v0, v1, v2, w} SUBSET s /\
 658      (?a b c.
 659           (packing s /\
 660            &2 * t0 <= d3 a b /\
 661            d3 a b <= sqrt (&8) /\
 662            c IN anchor_points a b s /\
 663            (?q. diagonal a b q s /\ q IN Q_SYS s)) /\
 664           {v0, v1, v2} = {a, b, c})
 665      ==> quarter {v0, v1, v2, w} s`) THEN
 666 PHA THEN REWRITE_TAC[ MESON[]` (? a. P a) /\ aa <=> (? a . P a /\ aa )`] THEN
 667 NHANH (MESON[diagonal] ` diagonal a b q s ==> {a,b} SUBSET q `) THEN
 668 PHA THEN REWRITE_TAC[ MESON[]` (? a. P a) /\ aa <=> (? a . P a /\ aa )`] THEN
 669 NHANH (SET_RULE ` {v0, v1, v2} = {a, b, c} ==> {a,b} SUBSET {v0,v1,v2,w} `) THEN
 670 REWRITE_TAC[ SET_RULE ` {a, b} SUBSET q /\ aa /\ bb /\ {a, b} SUBSET {v0, v1, v2, w} <=>
 671      {a, b} SUBSET q INTER {v0, v1, v2, w} /\ aa /\ bb`] THEN
 672 MESON_TAC[lemma7_7_CXRHOVG]);;
 673
 674
 675 let lemma8_3_OVOAHCG =prove(`!s v0 v1 v2 w x. {v0, v1, v2, w} SUBSET s /\ CARD {v0,v1,v2,w,x} = 5  /\
 676      centered_pac s v0 /\
 677      ~(conv {x, w} INTER aff_ge {v0} {v1, v2} = {}) /\
 678      {v0, v1, v2} IN barrier' v0 s /\
 679      unobstructed v0 x s /\
 680      dist (x,v0) < dist (x,v1) /\
 681      dist (x,v0) < dist (x,v2)
 682      ==> ~(x IN VC w s)`,
 683 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[ MESON[] ` a ==> ~b <=> a /\ b ==> ~b`] THEN
 684 REWRITE_TAC[IN_ELIM_THM] THEN
 685 NHANH (MESON[CARD5] ` CARD {x, w, v0, v1, v2} = 5 ==> ~(x IN {w,v0,v1,v2})`) THEN
 686 NHANH ( SET_RULE ` ~(x IN {w,v0,v1,v2}) ==> ~( x = w ) `) THEN
 687 PHA THEN  REWRITE_TAC[  MESON[]` unobstructed v0 x s /\ a <=> a /\
 688   unobstructed v0 x s `] THEN REWRITE_TAC[ MESON[]` ~(x = w) /\ a <=> a /\ ~(x = w) `]
 689    THEN PHA THEN
 690 NHANH (SET_RULE ` ~(v0 IN {v1, v2, w, x}) ==> ~( v0 = w )`) THEN
 691 NGOAC THEN MATCH_MP_TAC (MESON[] ` (a ==> c) ==> ( a /\ b ==> c ) `) THEN PHA THEN
 692 REWRITE_TAC[ unobstructed] THEN
 693 REWRITE_TAC[ MESON[] ` ~(v0 = w) /\ centered_pac s v0 /\ aa /\ bb /\ cc /\
 694   x IN VC w s /\  ~obstructed v0 x s /\ las <=>
 695   aa /\ bb /\ cc /\ las /\ ( centered_pac s v0 /\ ~(v0 = w) /\
 696   ~obstructed v0 x s  /\ x IN VC w s   )`] THEN
 697 NHANH (CUTHE4 (prove(` ! s v0 w x . centered_pac s v0 /\ ~(v0 = w) /\ ~obstructed v0 x s /\ x IN VC w s
 698 ==> d3 w x < d3 v0 x`, REWRITE_TAC[ VC; lambda_x; IN_ELIM_THM] THEN PURE_ONCE_REWRITE_TAC
 699 [ MESON[] `( !s v0 w x. a v0 x s w ==> b v0 x w ) <=> ( ! s v0 w x. ( d3 v0 x < &2 \/
 700 ~(d3 v0 x < &2)) /\ a v0 x s w ==> b v0 x w) `] THEN MESON_TAC[centered_pac; trg_d3_sym;
 701   REAL_ARITH` ~(d3 v0 x < &2) /\ d3 w x < &2 ==> d3 w x < d3 v0 x`]))) THEN
 702 NHANH (CUTHE4 TRIANGLE_IN_BARRIER') THEN
 703 PHA THEN
 704 ONCE_REWRITE_TAC[MESON[] ` a1 /\ a2 /\ a3 /\  a4 /\
 705 ~(conv {x, w} INTER aff_ge {v0} {v1, v2} = {}) /\ aa /\  bb /\  cc /\  dd /\  a5 <=> aa /\
 706      bb /\  cc /\   dd /\   ~(conv {x, w} INTER aff_ge {v0} {v1, v2} = {}) /\  a3 /\ a4 /\
 707   a5 /\   a1 /\  a2`] THEN ONCE_REWRITE_TAC[ trg_d3_sym] THEN REWRITE_TAC[d3] THEN
 708 REWRITE_TAC[MESON[aff_ge_def; cone]` aff_ge {v0} {v1, v2} = cone v0 {v1,v2}`] THEN
 709 ONCE_REWRITE_TAC[ MESON[] ` CARD {v0, v1, v2, w, x} = 5 /\ a1 /\ a2 /\ a3 /\ a4 /\ a5 /\ a6 /\ l <=>
 710      a1 /\ a2 /\ a3 /\ a4 /\ a5 /\ a6 /\ CARD {v0, v1, v2, w, x} = 5 /\ l`] THEN
 711 NHANH (CUTHE5 tarski_UMMNOJN) THEN
 712 PHA THEN REWRITE_TAC[ MESON[] ` ( a \/ b ) /\ c <=> c /\ ( a \/ b ) `] THEN
 713 REWRITE_TAC[ MESON[] `{v0, v1, v2} IN barrier' v0 s /\ a <=>
 714   a /\ {v0, v1, v2} IN barrier' v0 s`] THEN
 715 REWRITE_TAC[ barrier'; IN_ELIM_THM] THEN
 716 PURE_ONCE_REWRITE_TAC[ MESON[]` (?a b c.
 717       ( P  {a, b, c} \/
 718        Q a b c ) /\
 719       {v0, v1, v2} = {a, b, c})
 720   <=> P {v0, v1, v2} \/  (? a b c. Q a b c /\ {v0, v1, v2} = {a, b, c})`] THEN PHA THEN
 721 ONCE_REWRITE_TAC[ MESON[] ` ~(conv {v0, v1, v2} INTER conv0 {x, w} = {}) /\ aa /\ (b \/ bb) <=>
 722      ~(conv {v0, v1, v2} INTER conv0 {x, w} = {}) /\
 723      aa /\
 724      (~(conv {v0, v1, v2} INTER conv0 {x, w} = {}) /\ b \/ bb)`] THEN
 725 REWRITE_TAC[ SET_RULE ` conv {v0, v1, v2} INTER conv0 {x, w} =
 726           conv0 {x, w} INTER conv {v0, v1, v2}`] THEN
 727 NHANH (MESON[ def_obstructed] ` ~(conv0 {x, w} INTER conv {v0, v1, v2} = {}) /\
 728   {v0, v1, v2} IN barrier s /\ l ==> obstructed x w s `) THEN
 729 PHA THEN REWRITE_TAC[ MESON[] ` {v0, v1, v2, w} SUBSET s /\ a <=> a /\ {v0, v1, v2, w}
 730    SUBSET s`] THEN
 731 REWRITE_TAC[ MESON[] ` (!a. a IN {v1, v2, v0} ==> dist (w,a) <= #2.51) /\ a <=>
 732    a /\ (!a. a IN {v1, v2, v0} ==> dist (w,a) <= #2.51)`] THEN
 733 REWRITE_TAC[ MESON[]` CARD {v0, v1, v2, w, x} = 5 /\ a <=>
 734     a /\ CARD {v0, v1, v2, w, x} = 5 `] THEN
 735 PHA THEN
 736 ONCE_REWRITE_TAC[ MESON[] ` ( a \/ b) /\ a1 /\ a2 /\ {v0, v1, v2, w} SUBSET s <=> ( a \/
 737   a2 /\ a1 /\ {v0, v1, v2, w} SUBSET s /\ b) /\ a1 /\ a2 /\ {v0, v1, v2, w} SUBSET s`] THEN
 738 NHANH (CUTHE6 NOV7) THEN
 739 NHANH (prove(` {v0, v1, v2, w} IN Q_SYS s ==> {v0,v1,v2} IN barrier s `,
 740   REWRITE_TAC[ barrier; SET_RULE` {a,b,c} UNION {d} = {a,b,c,d} `; IN_ELIM_THM]
 741    THEN MESON_TAC[])) THEN
 742 ONCE_REWRITE_TAC[ MESON[] ` ~(conv0 {x, w} INTER conv {v0, v1, v2} = {}) /\ a1
 743   /\ ( a \/ b ) /\ l <=>  ~(conv0 {x, w} INTER conv {v0, v1, v2} = {}) /\ a1
 744   /\ ( a \/ b /\ ~(conv0 {x, w} INTER conv {v0, v1, v2} = {}) ) /\ l`] THEN
 745 PHA THEN NHANH (MESON[def_obstructed] ` {v0, v1, v2} IN barrier s /\
 746   ~(conv0 {x, w} INTER conv {v0, v1, v2} = {}) ==> obstructed x w s`) THEN
 747 REWRITE_TAC[ MESON[]` (a /\ b \/ a /\ c ) <=> a /\ ( b \/ c ) `] THEN
 748 DAO THEN
 749 REWRITE_TAC[ MESON[] `( obstructed x w s /\ b \/ obstructed x w s
 750   /\ c ) <=>  obstructed x w s /\ ( b \/ c ) `] THEN PHA THEN
 751 REWRITE_TAC[MESON[ OBS_IMP_NOT_IN_VC] ` a1/\a2/\a3 /\ obstructed x w s /\ l
 752   ==> ~(x IN VC w s)`]);;
 753
 754 let lambda_x = prove(` ! x s. lambda_x x s ={w | w IN s /\ d3 w x < &2 /\ ~obstruct w x s}`,
 755 REWRITE_TAC[lambda_x; OBSTRUCT_EQ]);;
 756
 757 (* ==== end repare VC === *)
 758
 759
 760 (* LEMMA 8.1 *)
 761
 762
 763
 764 let TCQPONA = new_axiom ` ! s v v1 v2 v3.
 765   packing s /\
 766  CARD {v, v1, v2, v3} = 4 /\
 767  {v, v1, v2, v3} SUBSET s /\
 768  d3 v1 v2 <= &2 * t0 /\
 769  d3 v2 v3 <= &2 * t0 /\
 770  d3 v3 v1 <= &2 * t0 /\
 771  ~(conv {v1, v2, v3} INTER voronoi v s = {})
 772  ==> (!x. x IN {v1, v2, v3} ==> &2 <= d3 x v /\ d3 x v <= &2 * t0)`;;
 773
 774
 775
 776 let CEWWWDQ = new_axiom ` !s v v1 v2 v3.
 777      packing s /\
 778      CARD {v, v1, v2, v3}  = 4 /\
 779      {v, v1, v2, v3}  SUBSET s /\
 780      d3 v1 v2 <= &2 * t0 /\
 781      d3 v2 v3 <= &2 * t0 /\
 782      d3 v1 v3 <= sqrt (&8) /\
 783      ~(conv {v1, v2, v3} INTER voronoi v s = {})
 784      ==> (!x. x IN {v1, v2, v3} ==> &2 <= d3 x v /\ d3 x v <= &2 * t0)`;;
 785
 786
 787
 788
 789 let QHSEWMI = new_axiom ` !v1 v2 v3 w1 w2.
 790          ~(conv {w1, w2} INTER conv {v1, v2, v3} = {}) /\
 791          ~(w1 IN conv {v1,v2,v3})
 792          ==> w2 IN cone w1 {v1, v2, v3}`;;
 793
 794
 795
 796
 797 (* =================== *)
 798
 799 let BAR_TRI = prove(` ! b s. b IN barrier s <=> (? x y z . b = {x,y,z} /\ {x,y,z} IN barrier s)`,
 800 REWRITE_TAC[ barrier ; IN_ELIM_THM] THEN MESON_TAC[]);;
 801
 802
 803
 804
 805
 806 let NOV20 = prove(` ! v0 x' y z. v0 IN {x', y, z} <=> (?yy zz. {v0, yy, zz} = {x', y, z})`,
 807 REPEAT GEN_TAC THEN
 808 REWRITE_TAC[EQ_EXPAND] THEN
 809 REWRITE_TAC[SET_RULE `((?yy zz. {v0, yy, zz} = {x', y, z})
 810    ==> v0 IN {x', y, z})`] THEN
 811 REWRITE_TAC[IN_SET3] THEN
 812 MESON_TAC[SET_RULE ` x = a
 813      ==> {x, b, c} = {a, b, c} /\
 814          {x, b, c} = {b, a, c} /\
 815          {x, b, c} = {b, c, a}`]);;
 816
 817
 818
 819 let X_IN_VOR_X = prove(` ! x:real^A s. x IN voronoi x s `,
 820 REWRITE_TAC[voronoi; IN_ELIM_THM; DIST_REFL; DIST_POS_LT] THEN
 821 MESON_TAC[DIST_POS_LT]);;
 822
 823 let IN_VO2_EQ = prove(` ! s v0 x . x IN voro2 v0 s <=>
 824  (!w. s w /\ ~(w = v0) ==> d3 x v0 < d3 x w) /\ d3 x v0 < &2`,
 825 REWRITE_TAC[voro2; voronoi; IN_ELIM_THM; d3]);;
 826
 827 let IN_VO_EQ = prove(`! x s v0 . x IN voronoi v0 s <=> (!w. s w /\
 828    ~(w = v0) ==> dist(x,v0) < dist(x,w))`, REWRITE_TAC[voronoi; IN_ELIM_THM]);;
 829
 830
 831 let IN_BAR_DISTINCT = prove(` ! a b c s. {a,b,c} IN barrier s ==>
 832    ~( a = b\/ b= c \/ c = a)`,
 833 REWRITE_TAC[barrier; IN_ELIM_THM; quasi_tri;set_3elements] THEN
 834 KHANANG THEN REWRITE_TAC[EXISTS_OR_THM] THEN NHANH ( MESON[]` (?v1 v2 v3.
 835           (a1  /\  a2 v1 v2 v3  /\
 836            ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\
 837            a3 v1 v2 v3 ) /\
 838           {a, b, c} = {v1, v2, v3}) ==> (?v1 v2 v3.
 839            ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\
 840           {a, b, c} = {v1, v2, v3})`) THEN
 841 ONCE_REWRITE_TAC[MESON[EQ_SYM_EQ]` {a,b,c} = {x,y,z} <=> {x,y,z} = {a,b,c}` ] THEN
 842 REWRITE_TAC[ set_3elements] THEN MESON_TAC[OCT23]);;
 843
 844
 845 let FOUR_POINTS = prove(`!a b c d s.
 846      {a, b, c} IN barrier s /\ ~(d IN {a, b, c}) ==> CARD {a, b, c, d} = 4`,
 847 NHANH (CUTHE4 IN_BAR_DISTINCT) THEN ONCE_REWRITE_TAC[
 848 SET_RULE ` {a,b,c,d} = {d,a,b,c} `] THEN MESON_TAC[CARD4]);;
 849
 850
 851 (* ========= *)
 852
 853
 854 let IN_Q_SYS_IMP4 = prove(`!q s. q IN Q_SYS s ==>
 855   (?a b c d. {a, b, c} UNION {d} = q)`,
 856 NHANH (SPEC_ALL CASES_OF_Q_SYS) THEN
 857 REWRITE_TAC[quasi_reg_tet; strict_qua; quarter; simplex] THEN
 858 REWRITE_TAC[SET_RULE` {a,b,c,d} = {a,b,c} UNION {d} `] THEN
 859 MESON_TAC[]);;
 860
 861
 862 let SET2_SU_EX = SET_RULE` {(a:A),b} SUBSET s <=> a IN s /\ b IN s `;;
 863 let D3_SYM = MESON[trg_d3_sym]` ! x y. d3 x y = d3 y x `;;
 864
 865
 866 let EXISTS_DIA = prove(`! q s. quarter q s ==> (? a b. diagonal a b q s)`,
 867 REWRITE_TAC[quarter; diagonal] THEN
 868 REWRITE_TAC[SET2_SU_EX] THEN
 869 SIMP_TAC[] THEN
 870 NHANH (MESON[REAL_LE_TRANS]`&2 * t0 <= d3 v w /\ a1 /\ (!x y. P x y ==> d3 x y <= &2 * t0)
 871      ==> (!x y. P x y ==> d3 x y <= d3 v w)`) THEN
 872 MP_TAC PAIR_D3 THEN
 873 REWRITE_TAC[MESON[REAL_ARITH ` a = b ==> a <= b `] ` a ==> b = c:real <=>
 874   a ==> ( b = c /\ b <= c )`] THEN
 875 MESON_TAC[]);;
 876
 877
 878 let QUARTER_EQ_EX_DIA = prove(`! q s. quarter q s <=> (? a b. diagonal a b q s)`,
 879 REWRITE_TAC[EQ_EXPAND; EXISTS_DIA; diagonal] THEN MESON_TAC[]);;
 880
 881
 882 let IN_Q_IMP = prove(`!q s.
 883      q IN Q_SYS s ==>
 884      quasi_reg_tet q s \/
 885      (?a b q1.
 886           {a, b} SUBSET q INTER q1 /\ quarter q s /\ diagonal a b q1 s /\ q1 IN Q_SYS s)`,
 887 REWRITE_TAC[MESON[CASES_OF_Q_SYS]`  (q IN Q_SYS s ==> a ) <=> q IN Q_SYS s
 888     /\ (quasi_reg_tet q s \/ strict_qua q s) ==> a `] THEN
 889 KHANANG THEN
 890 REWRITE_TAC[MESON[]` a \/ b ==> c <=> (a ==> c) /\ ( b==> c) `] THEN
 891 SIMP_TAC[] THEN
 892 REWRITE_TAC[strict_qua] THEN
 893 NHANH (SPEC_ALL EXISTS_DIA) THEN
 894 NHANH (MESON[diagonal]`  diagonal d1 d2 q s ==>  {d1, d2} SUBSET q `) THEN
 895 REWRITE_TAC[SUBSET_INTER] THEN
 896 MESON_TAC[]);;
 897
 898 let NOV21 = prove(` ! q s. quasi_reg_tet q s ==> q IN Q_SYS s`,
 899 REWRITE_TAC[Q_SYS; IN_ELIM_THM] THEN REWRITE_TAC[ MESON[]` a ==> a \/ b `]);;
 900
 901
 902 let NOVE21 = prove(` ! q s. quasi_reg_tet q s \/
 903      (?a b q1.
 904           {a, b} SUBSET q1 INTER q /\ quarter q s /\ diagonal a b q1 s /\ q1 IN Q_SYS s)
 905   ==> q IN Q_SYS s `,
 906 MP_TAC NOV21 THEN REWRITE_TAC[OR_IMP_EX] THEN SIMP_TAC[] THEN
 907 MP_TAC lemma7_7_CXRHOVG THEN MESON_TAC[]);;
 908
 909
 910 let COND_Q_SYS =prove(`!q s.
 911      q IN Q_SYS s <=>  quasi_reg_tet q s \/
 912      (?a b q1. {a, b} SUBSET q INTER q1 /\ quarter q s /\
 913      diagonal a b q1 s /\ q1 IN Q_SYS s)`, REWRITE_TAC[EQ_EXPAND] THEN
 914 REWRITE_TAC[IN_Q_IMP] THEN MESON_TAC[INTER_COMM; NOVE21]);;
 915
 916 (* ============ *)
 917
 918 let SET4_SUB_EX = SET_RULE ` {a,b,c,d} SUBSET s <=>
 919      a IN s /\ b IN s /\ c IN s /\ (d:A) IN s `;;
 920
 921
 922
 923 let IMP_QUA_RE_TE = prove(`!s v0 x y z. v0 IN s /\ packing s /\
 924      {x, y, z} SUBSET s /\
 925      (!aa bb. aa IN {y, z, x} /\ bb IN {y, z, x} ==> dist (aa,bb) <= #2.51) /\
 926      ~(voronoi v0 s INTER conv {x, y, z} = {}) /\
 927      CARD {x, y, z, v0} = 4 ==> quasi_reg_tet {v0,x,y,z} s `,
 928 NHANH (SET_RULE ` (! aa bb. aa IN {y, z, x} /\ bb IN {y, z, x} ==> P aa bb )
 929   ==> P x y /\ P y z /\ P z x `) THEN
 930 ONCE_REWRITE_TAC[ SET_RULE `{a,b,c,d} = {d,a,b,c}`] THEN
 931 REWRITE_TAC[ SET_RULE ` v0 IN s /\ packing s /\
 932      {x, y, z} SUBSET s /\ l <=> packing s /\ {v0,x,y,z} SUBSET s /\ l `] THEN
 933 REWRITE_TAC[ MESON[]` a /\ b/\ ( c1 /\ c2 ) /\ d /\ e <=> c1 /\ a /\ e
 934    /\ b /\ c2 /\d `] THEN
 935 ONCE_REWRITE_TAC[INTER_COMM] THEN
 936 REWRITE_TAC[ GSYM db_t0; GSYM d3] THEN PHA THEN
 937 NHANH (SPEC_ALL TCQPONA) THEN
 938 REWRITE_TAC[quasi_reg_tet; def_simplex; CARD4;IN_SET3; IN_SET4;
 939    DE_MORGAN_THM; SET4_SUB_EX; db_t0] THEN
 940 SIMP_TAC[] THEN PHA THEN DAO THEN
 941 REWRITE_TAC[ MESON[D3_SYM]` (!x'. x' = x \/ x' = y \/ x' = z ==>
 942   d3 x' v0 <= #2.51 /\ &2 <= d3 x' v0) /\     a1 /\
 943      d3 z x <= #2.51 /\
 944      d3 y z <= #2.51 /\
 945      d3 x y <= #2.51 /\
 946      l  ==> (!v w. ~(v = w) /\
 947               (v = z \/ v = v0 \/ v = x \/ v = y) /\
 948               (w = z \/ w = v0 \/ w = x \/ w = y)
 949               ==> d3 v w <= #2.51)`]);;
 950
 951 (* =========== *)
 952
 953 let SET3_U_SET1 = SET_RULE ` {a,b,c} UNION {d} = {a,b,c,d} `;;
 954
 955
 956 let IN_BA_IM_PA_SU = prove(`! s x y z. {x, y, z} IN barrier s ==>
 957 packing s /\ {x, y, z} SUBSET s`,
 958 REWRITE_TAC[barrier; IN_ELIM_THM] THEN
 959 NHANH (SPEC_ALL CASES_OF_Q_SYS) THEN REPEAT GEN_TAC THEN
 960 REWRITE_TAC[quasi_tri] THEN KHANANG THEN
 961 REWRITE_TAC[MESON[]` (?a b c. P a b c \/ Q a b c) ==> l <=>
 962        ((?a b c . P a b c ) ==> l) /\ ((?a b c. Q a b c) ==> l)`] THEN
 963 REWRITE_TAC[MESON[]` (?v1 v2 v3.  (packing s /\
 964         {v1, v2, v3} SUBSET s /\P v1 v2 v3 ) /\
 965        {x, y, z} = {v1, v2, v3}) ==> packing s /\ {x, y, z} SUBSET s`] THEN
 966 REWRITE_TAC[quasi_reg_tet; strict_qua; quarter; SET3_U_SET1; def_simplex] THEN
 967 REWRITE_TAC[SET_RULE ` {a,b,c,d} SUBSET s <=> {a,b,c} SUBSET s /\ d IN s `] THEN
 968 MESON_TAC[]);;
 969
 970
 971 let FIRST_NOV22 = prove(` ! s v0 x y z. {x, y, z} IN barrier s /\
 972  (!xx yy.
 973       ~(xx = yy) /\ {xx, yy} SUBSET {y, z, x}
 974       ==> &2 <= dist (xx,yy) /\ dist (xx,yy) <= sqrt (&8)) /\
 975  (!aa bb. aa IN {y, z, x} /\ bb IN {y, z, x} ==> dist (aa,bb) <= #2.51) /\
 976  v0 IN s /\
 977  ~(voronoi v0 s INTER conv {x, y, z} = {}) /\
 978  CARD {x, y, z, v0} = 4
 979  ==> {v0, x, y, z} IN Q_SYS s`,
 980 NHANH (SPEC_ALL IN_BA_IM_PA_SU ) THEN
 981 PHA THEN
 982 ONCE_REWRITE_TAC[MESON[]` a1 /\ a2 /\ a3 /\ a4 /\ a5 /\ a6 /\ a7 /\ a8 <=>
 983   a1 /\ a4 /\ a6 /\ a2 /\ a3 /\ a5 /\ a7 /\ a8 `] THEN
 984 NHANH (SPEC_ALL IMP_QUA_RE_TE) THEN
 985 MESON_TAC[COND_Q_SYS]);;
 986
 987
 988
 989 let QUA_TRI_EDGE = prove(` ! q s. quasi_tri q s ==>
 990   (! a b. a IN q /\ b IN q ==> d3 a b <= &2 * t0 )`,REWRITE_TAC[quasi_tri; db_t0]
 991 THEN MP_TAC D3_REFL THEN MP_TAC (REAL_ARITH ` &0 <= #2.51 `) THEN MESON_TAC[]);;
 992
 993
 994 let BAR_WI_LONG_ED = prove(`!bar s.
 995      bar IN barrier s /\ (?a b. #2.51 < d3 a b /\ a IN bar /\ b IN bar)
 996      ==> (?w. w INSERT bar IN Q_SYS s /\ strict_qua (w INSERT bar) s)`,
 997 REWRITE_TAC[barrier; IN_ELIM_THM] THEN REPEAT GEN_TAC THEN STRIP_TAC THENL
 998 [REPEAT (FIRST_X_ASSUM MP_TAC);REPEAT (FIRST_X_ASSUM MP_TAC)]
 999  THENL [NHANH (SPEC_ALL QUA_TRI_EDGE);
1000 ABBREV_TAC ` an w s = (w:real^3 INSERT (bar:real^3 -> bool) IN Q_SYS s)`] THENL
1001 [REWRITE_TAC[ GSYM db_t0]; NHANH (SPEC_ALL CASES_OF_Q_SYS)] THENL
1002 [MESON_TAC[REAL_ARITH ` a <= b <=> ~( b < a )`];
1003 NHANH (MESON[QUA_TET_IMPLY_QUA_TRI]`quasi_reg_tet ({v0, v1, v2} UNION {v4}) s ==>
1004   quasi_tri {v0, v1, v2} s`)] THEN NHANH (SPEC_ALL QUA_TRI_EDGE) THEN
1005 STRIP_TAC THENL [ASM_MESON_TAC[db_t0; REAL_ARITH` a <= b <=> ~( b < a ) `];
1006 ASM_MESON_TAC[SET_RULE ` s UNION {a} = a INSERT s `]]);;
1007
1008 (* ======= *)
1009
1010 let PER_SET3 = SET_RULE ` {a,b,c} = {a,c,b} /\ {a,b,c} = {b,a,c} /\
1011   {a,b,c} = {c,a,b} /\ {a,b,c} = {b,c,a} /\ {a,b,c} = {c,b,a} `;;
1012
1013 let EXI_THIRD_PO =prove( ` ! a b c x y: A. {x,y} SUBSET {a,b,c} /\ ~(x=y)
1014   ==> (? z. {x,y,z} = {a,b,c} ) `, REPEAT GEN_TAC THEN
1015 REWRITE_TAC[SET2_SU_EX] THEN REWRITE_TAC[SET2_SU_EX; IN_SET3] THEN
1016 KHANANG THEN REWRITE_TAC[MESON[]`x = a /\ y = a /\ ~(x = y) <=> F`] THEN
1017 MESON_TAC[ PER_SET3]);;
1018
1019
1020
1021
1022 let IMP_QUA = prove(` ! a b c s v0. packing s /\
1023  CARD {v0, a, b, c} = 4 /\
1024  {v0, a, b, c} SUBSET s /\
1025  d3 a b <= &2 * t0 /\
1026  d3 b c <= &2 * t0 /\ &2 * t0 <= d3 a c /\
1027  d3 a c <= sqrt (&8) /\
1028  (!x. x IN {a, b, c} ==> &2 <= d3 x v0 /\ d3 x v0 <= &2 * t0)
1029 ==> quarter {v0, a, b, c} s `,
1030 REWRITE_TAC[quarter; def_simplex; CARD4; IN_SET3; DE_MORGAN_THM] THEN
1031 SIMP_TAC[] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
1032 EXISTS_TAC `a:real^3` THEN EXISTS_TAC `c:real^3` THEN
1033 ASM_SIMP_TAC[FOUR_IN] THEN REWRITE_TAC[IN_SET4; PAIR_EQ_EXPAND] THEN
1034 MP_TAC (MESON[REAL_ARITH ` &0 <= #2.51`; db_t0]` &0 <= &2*t0 `) THEN
1035 ASM_MESON_TAC[D3_SYM; D3_REFL]);;
1036
1037
1038 let QUA_RE_TE_EDGE = prove(`! a b q s. quasi_reg_tet q s /\ a IN q /\ b IN q
1039  ==> d3 a b <= &2 * t0 `, REWRITE_TAC[quasi_reg_tet] THEN MP_TAC D3_REFL THEN
1040 REWRITE_TAC[db_t0] THEN MESON_TAC[REAL_ARITH `&0 <= #2.51 `]);;
1041
1042 (* ========= *)
1043
1044
1045 let CONSI_OF_LE77 = prove(`!s v0 v4 w x y z.
1046      quarter ({x, y, z} UNION {v0}) s /\
1047      aa IN {x, y, z} /\
1048      bb IN {x, y, z} /\
1049      {x, y, z} UNION {v4} IN Q_SYS s /\
1050      diagonal aa bb ({x, y, z} UNION {v4}) s
1051      ==> {x, y, z} UNION {v0} IN Q_SYS s`,
1052 REWRITE_TAC[MESON[]` quarter q s /\ a <=>a/\quarter q s `] THEN
1053 PHA THEN NHANH (SET_RULE `  aa IN {x, y, z} /\ bb IN {x, y, z} /\ l
1054      ==> (!v0 v4.
1055               {aa, bb} SUBSET
1056               ({x, y, z} UNION {v4}) INTER ({x, y, z} UNION {v0}))`) THEN
1057 PHA THEN NHANH (MESON[]` diagonal aa bb ({x, y, z} UNION {v4}) s /\
1058      quarter ({x, y, z} UNION {v0}) s /\
1059      (!v0 v4. P v0 v4) ==> P v0 v4 `) THEN MESON_TAC[lemma7_7_CXRHOVG]);;
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069 let IMP_IN_Q_SYS = prove( ` ! s v0 x y z . {x, y, z} IN barrier s /\ v0 IN s /\
1070  ~(voronoi v0 s INTER conv {x, y, z} = {}) /\
1071  CARD {x, y, z, v0} = 4
1072  ==> {v0, x, y, z} IN Q_SYS s`,
1073 NHANH (CUTHE4 TRIANGLE_IN_BARRIER) THEN
1074 KHANANG THEN
1075 REWRITE_TAC[OR_IMP_EX] THEN
1076 REWRITE_TAC[FIRST_NOV22] THEN
1077 REPEAT GEN_TAC THEN
1078 MATCH_MP_TAC (MESON[]`(a /\ c ==> d ) ==> a /\ b /\ c ==> d `) THEN
1079 NHANH (SPEC_ALL IN_BA_IM_PA_SU) THEN
1080 REWRITE_TAC[MESON[]` a /\ b /\ c ==> d <=> b ==> a /\ c ==> d`] THEN
1081 NHANH (MESON[DIST_NZ; REAL_ARITH ` &0 < #2.51 /\ ( a < b /\ b < c ==> a < c )`]`
1082   #2.51 < dist (aa,bb) ==> ~( aa = bb ) `) THEN
1083 REWRITE_TAC[ MESON[]` a /\ ( b /\ c ) /\ l <=> (a /\ c ) /\ b /\ l`] THEN
1084 NHANH (SPEC_ALL EXI_THIRD_PO) THEN
1085 REWRITE_TAC[MESON[]` a/\ b/\ c/\ d <=> c /\ a/\b/\d`] THEN
1086 STRIP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN
1087 ONCE_REWRITE_TAC[ EQ_SYM_EQ] THEN
1088 REWRITE_TAC[MESON[]` a = b ==> P a <=> a = b ==> P b `] THEN
1089 ONCE_REWRITE_TAC[ EQ_SYM_EQ] THEN
1090 ONCE_REWRITE_TAC[ SET_RULE ` {x, y, z, v0} = {v0,y,z,x} `] THEN
1091 REWRITE_TAC[CARD4; GSYM CARD3] THEN
1092 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
1093 REWRITE_TAC[MESON[]` a = b ==> P a <=> a = b ==> P b `] THEN
1094 REWRITE_TAC[IMP_IMP] THEN PHA THEN
1095 REWRITE_TAC[MESON[]` (! a b. P a b ) /\l <=> l/\(!a b. P a b)`] THEN
1096 PHA THEN
1097 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
1098 REWRITE_TAC[CARD3] THEN
1099 NHANH (SET_RULE ` ~(aa = bb \/ bb = z' \/ z' = aa) /\
1100  (!x' y'.
1101       ~({x', y'} = {aa, bb}) /\ {x', y'} SUBSET {aa, bb, z'}
1102       ==> P x' y') ==>
1103   P bb z' /\ P z' aa `) THEN
1104 PHA THEN
1105 REWRITE_TAC[MESON[CARD4]` ~(v0 IN {aa, bb, z'}) /\
1106  ~(aa = bb \/ bb = z' \/ z' = aa) /\ l <=> CARD {v0,aa,bb,z'} = 4 /\ l `] THEN
1107 ONCE_REWRITE_TAC[ SET_RULE ` {v0, aa, bb, z'} = {v0,bb,z',aa}`] THEN
1108 SIMP_TAC[SET_RULE ` {y,z,x} = {x,y,z} `] THEN
1109 REWRITE_TAC[ GSYM d3; GSYM db_t0] THEN
1110 REWRITE_TAC[ GSYM d3; GSYM db_t0; SET2_SU_EX] THEN
1111 REWRITE_TAC[MESON[]` (aa IN {x, y, z} /\ bb IN {x, y, z}) /\a1 /\a2 /\
1112  &2 * t0 < d3 aa bb /\a3 /\ a4  /\ a5 /\ l <=> (aa IN {x, y, z} /\ bb IN {x, y, z}
1113   /\ a5 /\ &2 * t0 < d3 aa bb) /\ a1 /\ a2 /\ a3 /\ a4 /\ l `] THEN
1114 NHANH (SPEC_ALL DIAGONAL_BARRIER) THEN
1115 NHANH (SPEC_ALL DIA_OF_QUARTER) THEN
1116 REWRITE_TAC[ GSYM LEFT_AND_EXISTS_THM] THEN
1117 PHA THEN
1118 REWRITE_TAC[MESON[]` d3 aa bb <= sqrt (&8) /\ l <=>l/\d3 aa bb <= sqrt (&8)`] THEN
1119 REWRITE_TAC[MESON[]` a = b /\ P b <=> a = b /\ P a`] THEN
1120 PHA THEN REWRITE_TAC[MESON[]` ~ ( a INTER b = {}) /\ l <=> l/\ ~ ( a INTER b = {})`]
1121   THEN PHA THEN
1122 REWRITE_TAC[SET_RULE` v0 IN s /\
1123      a1 /\
1124      {aa, bb, z'} SUBSET s /\
1125      CARD {v0, aa, bb, z'} = 4 /\
1126      l /\
1127      las <=>
1128      l /\ a1 /\ CARD {v0, aa, bb, z'} = 4 /\ {v0, bb, z', aa} SUBSET s /\ las`] THEN
1129 ONCE_REWRITE_TAC[MESON[SET_RULE ` {v0, aa, bb, z'} = {v0,bb,z',aa}`]` CARD {v0, aa, bb, z'} =4
1130   <=> CARD {v0,bb,z',aa} = 4 `] THEN
1131 ONCE_REWRITE_TAC[INTER_COMM] THEN
1132 ONCE_REWRITE_TAC[MESON[SET_RULE ` {a,b,c} = {b,c,a}`]`
1133    conv {a,b,c} = conv {b,c,a} `] THEN
1134 ONCE_REWRITE_TAC[MESON[D3_SYM]` d3 aa bb <= sqrt (&8) <=> d3 bb aa <= sqrt (&8)`] THEN
1135 NHANH (SPEC_ALL CEWWWDQ) THEN
1136 NHANH (REAL_ARITH ` a < b ==> a <= b `) THEN
1137 ONCE_REWRITE_TAC[MESON[]` ( a/\ b ) /\ c <=> c /\ b /\ a `] THEN
1138 PHA THEN
1139 NHANH (MESON[IMP_QUA; D3_SYM]` packing s /\
1140  CARD {v0, bb, z', aa} = 4 /\
1141  {v0, bb, z', aa} SUBSET s /\
1142  d3 bb z' <= &2 * t0 /\
1143  d3 z' aa <= &2 * t0 /\
1144  d3 bb aa <= sqrt (&8) /\ a2 /\
1145  (!x. x IN {bb, z', aa} ==> &2 <= d3 x v0 /\ d3 x v0 <= &2 * t0) /\
1146  &2 * t0 <= d3 aa bb /\ a1 ==> quarter {v0, bb, z', aa} s`) THEN
1147 REWRITE_TAC[MESON[]`( ? a. P a ) /\ l <=> l /\ (?a. P a) `] THEN
1148 REWRITE_TAC[barrier; IN_ELIM_THM] THEN
1149 REWRITE_TAC[MESON[]` P b /\ a = b <=> a = b /\ P a `] THEN
1150 REWRITE_TAC[GSYM LEFT_AND_EXISTS_THM] THEN
1151 PHA THEN
1152 REWRITE_TAC[MESON[]`( a < b /\ l <=> l /\ a < b ) /\
1153        ( ( x \/ y ) /\ z <=> z /\ ( x \/ y ))`] THEN
1154 REWRITE_TAC[ MESON[]` a IN s /\ b /\ c <=> c /\ a IN s /\ b `] THEN
1155 NHANH (SPEC_ALL QUA_TRI_EDGE) THEN
1156 PHA THEN
1157 REWRITE_TAC[MESON[real_lt]`&2 * t0 < d3 aa bb /\
1158      (a1 /\ (!a b. a IN s /\ b IN s ==> d3 a b <= &2 * t0) \/ a2) /\
1159      aa IN s /\
1160      bb IN s <=>
1161      &2 * t0 < d3 aa bb /\ a2 /\ aa IN s /\ bb IN s`] THEN
1162 NHANH (SPEC_ALL CASES_OF_Q_SYS) THEN
1163 REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
1164 KHANANG THEN
1165 NHANH (MESON[SET_RULE ` a IN s ==> a IN ( s UNION t )`; QUA_RE_TE_EDGE]`
1166   quasi_reg_tet ({x, y, z} UNION {v4}) s /\
1167                  aa IN {x, y, z} /\
1168                  bb IN {x, y, z} ==> d3 aa bb <= &2 * t0 `) THEN
1169 DAO THEN
1170 REWRITE_TAC [REAL_ARITH ` a <= b <=> ~( b < a ) `] THEN
1171 REWRITE_TAC[MESON[]`(?v4. ~(&2 * t0 < d3 aa bb) /\ P v4 \/ Q v4) /\ a1 /\ &2 * t0 < d3 aa bb <=>
1172      (?v4. Q v4) /\ a1 /\ &2 * t0 < d3 aa bb`] THEN
1173 REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
1174 PHA THEN
1175 NHANH (MESON[SET_RULE` a IN s ==> a IN ( s UNION t ) `; DIAGONAL_STRICT_QUA]`
1176   bb IN {x, y, z} /\
1177       aa IN {x, y, z} /\ a1 /\
1178       strict_qua ({x, y, z} UNION {v4}) s /\
1179       a2  /\
1180       &2 * t0 < d3 aa bb /\ l ==> diagonal aa bb ({x, y, z} UNION {v4}) s  `) THEN
1181 NHANH (MESON[strict_qua]` strict_qua q s /\ l ==> quarter q s `) THEN
1182 PHA THEN
1183 REWRITE_TAC[SET_RULE ` {v0, bb, z', aa} = {aa,bb,z'} UNION {v0}`] THEN
1184 DAO THEN
1185 REWRITE_TAC[MESON[]` a = b /\ l <=> l/\ a= b `] THEN
1186 REWRITE_TAC[MESON[]`  quarter q s /\
1187          &2 * t0 < d3 aa bb /\l <=> &2 * t0 < d3 aa bb /\l /\ quarter q s`] THEN
1188 PHA THEN
1189 REWRITE_TAC[MESON[]` quarter ({aa, bb, z'} UNION {v0}) s /\
1190      a1 /\
1191       {aa, bb, z'} = {x, y, z} /\ l <=> l /\ a1 /\  {aa, bb, z'} = {x, y, z}
1192    /\ quarter ({x, y, z} UNION {v0}) s`] THEN
1193 REWRITE_TAC[MESON[]` a IN Q_SYS s /\ l <=> l /\ a IN Q_SYS s`] THEN
1194 REWRITE_TAC[MESON[]` a IN s /\ b /\ l <=>l /\ a IN s /\b `] THEN
1195 REWRITE_TAC[ MESON[]` diagonal aa bb ({x, y, z} UNION {v4}) s /\ l <=>
1196   l /\ diagonal aa bb ({x, y, z} UNION {v4}) s`] THEN
1197 PHA THEN
1198 NHANH (MESON[CONSI_OF_LE77]` quarter ({x, y, z} UNION {v0}) s /\
1199       aa IN {x, y, z} /\
1200       bb IN {x, y, z} /\
1201       {x, y, z} UNION {v4} IN Q_SYS s /\a1/\
1202       diagonal aa bb ({x, y, z} UNION {v4}) s
1203   ==> {x, y, z} UNION {v0} IN Q_SYS s`) THEN
1204 DAO THEN
1205 REWRITE_TAC[GSYM RIGHT_AND_EXISTS_THM] THEN
1206 REWRITE_TAC[MESON[SET_RULE ` {x, y, z} UNION {v0}  =  {y, v0, x} UNION {z} `;CASES_OF_Q_SYS]`
1207   {x, y, z} UNION {v0} IN Q_SYS s /\ last
1208      ==> {y, v0, x} UNION {z} IN Q_SYS s /\
1209          quasi_reg_tet ({y, v0, x} UNION {z}) s \/
1210          {y, v0, x} UNION {z} IN Q_SYS s /\
1211          strict_qua ({y, v0, x} UNION {z}) s`]);;
1212
1213 (* ========= *)
1214
1215
1216 let POS_EQ_INV_POS = prove(`!x. &0 < x <=> &0 < &1 / x`, GEN_TAC THEN EQ_TAC
1217 THENL [REWRITE_TAC[MESON[REAL_LT_RDIV_0; REAL_ARITH ` &0 < &1 `]`! b.  &0 < b
1218    ==> &0 < &1 / b `];REWRITE_TAC[] THEN
1219 MESON_TAC[MESON[REAL_LT_RDIV_0; REAL_ARITH ` &0 < &1 `]` &0 < b
1220     ==> &0 < &1 / b `; REAL_FIELD ` &1 / ( &1 / x ) = x ` ]]);;
1221
1222
1223 let STRIP_TR = REPEAT STRIP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC)
1224       THEN REWRITE_TAC[IMP_IMP] THEN PHA;;
1225
1226 let INTER_DIF_EM_EX = SET_RULE `! a b. ~(a INTER b = {}) <=> (? x. x IN a /\ x IN b ) `;;
1227
1228
1229
1230
1231 let AFF_LE_CONE =prove(` ! a b x y z. ~( conv0 {a,b} INTER conv {x,y,z} = {})
1232   ==> ( b IN aff_le {x,y,z} {a}) /\ ( b IN cone a {x,y,z}) `,
1233 REWRITE_TAC[CONV_SET3; CONV0_SET2; INTER_DIF_EM_EX; IN_ELIM_THM] THEN
1234 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN
1235 REWRITE_TAC[IMP_IMP] THEN PHA THEN REWRITE_TAC[MESON[]` x' = aa /\a1
1236  /\a2 /\a3/\a4 /\ x' = bb <=> x' = aa /\a1 /\a2 /\a3/\a4 /\ aa = bb `]
1237 THEN REWRITE_TAC[ VECTOR_ARITH ` a + b:real^N = c <=> b = c - a`] THEN
1238 NHANH (MESON[VECTOR_MUL_LCANCEL]`  b' % b = a ==> (&1 / b') % (b' % b)
1239   = (&1 / b') % a `) THEN REWRITE_TAC[VECTOR_MUL_ASSOC;
1240  VECTOR_SUB_LDISTRIB; VECTOR_ADD_LDISTRIB; simp_def] THEN
1241 NHANH (MESON[POS_EQ_INV_POS]` &0 < a ==> &0 < &1 / a `) THEN
1242 REWRITE_TAC[VECTOR_ARITH ` a - b % x = a + ( -- b ) % x `] THEN
1243 MP_TAC (REAL_FIELD `! b.  &0 < b ==>  &1 / b * b = &1 `) THEN
1244 REWRITE_TAC[IMP_IMP] THEN PHA THEN REWRITE_TAC[REAL_ARITH ` a / b * c
1245 = (a * c) / b`; REAL_MUL_LID; VECTOR_ARITH ` a - b % x = a + (--b) % x `] THEN
1246 REWRITE_TAC[REAL_ARITH ` -- ( a / b ) = ( -- a ) / b `] THEN
1247 NHANH (MESON[REAL_ARITH ` a / m + b / m + c / m + d / m = ( a + b + c + d ) / m `]`
1248   b' / b' % b = (a'' / b' % x + b'' / b' % y + c / b' % z) + --a' / b' % a
1249   ==> a'' / b' + b'' / b' + c / b' + -- a' / b' = ( a'' + b'' + c + -- a' ) / b' `)
1250  THEN NHANH (MESON[REAL_ARITH ` a' + b' = &1 /\  a'' + b'' + c = &1
1251   ==> a'' + b'' + c + --a' = b' `]` a' + b' = &1 /\a1 /\a2 /\a3 /\a4 /\
1252    a'' + b'' + c = &1 /\ l  ==> a'' + b'' + c + --a' = b'`) THEN
1253 MP_TAC (REAL_ARITH ` ! a. a < &0 ==> a <= &0 `) THEN REWRITE_TAC[ IN_ELIM_THM]
1254  THEN NHANH (MESON[]`(!b. &0 < b ==> b / b = &1) /\ --a' / b' < &0 /\
1255      &0 < a' /\ &0 < &1 / a' /\ &0 < b' /\ l ==>  b' / b' = &1 `) THEN
1256 REWRITE_TAC[MESON[] ` a /\ b' / b' = &1 ==> l <=> b' / b' = &1 ==> a ==> l`] THEN
1257 SIMP_TAC[VECTOR_MUL_LID] THEN PHA THEN NHANH (MESON[REAL_LT_DIV]
1258 ` &0 < a' /\ &0 < &1 / a' /\ &0 < b' /\ l ==> &0 < a' / b' `) THEN
1259 REWRITE_TAC[REAL_ARITH ` &0 < a' / b' <=> --a' / b' < &0 `] THEN
1260 REWRITE_TAC[ MESON[]` a = x / y /\ x = y <=> a = y/ y /\ x = y `] THEN
1261 REWRITE_TAC[ VECTOR_ARITH ` ((a:real^N) + b ) + c = a + b + c `] THEN
1262 STRIP_TR THENL [MESON_TAC[VECTOR_MUL_LID];
1263 REWRITE_TAC[cone; GSYM aff_ge_def; simp_def; IN_ELIM_THM]] THEN
1264 MP_TAC VECTOR_MUL_LID THEN SIMP_TAC[VECTOR_ARITH ` a + b + c + (d:real^N)
1265  = b + c + d + a `] THEN REWRITE_TAC[MESON[]` &0 <= a /\ l <=> l /\ &0 <= a `]
1266  THEN SIMP_TAC[ REAL_ARITH ` a + b + c + d = b + c + d + a `] THEN
1267 REWRITE_TAC[ MESON[]` &0 < a /\ l <=> l /\ &0 < a `] THEN PHA THEN
1268 NHANH (MESON[REAL_ARITH ` &0 < b ==> &0 <= b `; REAL_LE_DIV]` &0 <= c /\
1269      &0 <= b'' /\ &0 <= a'' /\ &0 < b' /\ &0 < a' ==>
1270 &0 <= a'' / b' /\ &0 <= b''/ b' /\ &0 <= c/ b' `) THEN
1271 NHANH (MESON[REAL_FIELD `  &0 < b' ==> b' / b' = &1 `]`(&0 <= c /\ &0
1272 <= b'' /\ &0 <= a'' /\ &0 < b' /\ &0 < a') ==> b' / b' = &1 `) THEN
1273 REWRITE_TAC[ MESON[]` a / a = &1 /\ l <=> l /\ a / a = &1 `] THEN DAO THEN
1274 REWRITE_TAC[IMP_IMP] THEN  REWRITE_TAC[ MESON[]`b' / b' = &1 /\ &0 < a' /\
1275  &0 < b' /\ l <=> &0 < a' /\ l /\ &0 < b' /\ b' / b' = &1  `] THEN
1276 REWRITE_TAC[ MESON[]` a = (b:real^N) /\ l <=> l /\ b = a `] THEN
1277 PHA THEN REWRITE_TAC[ MESON[]` aaa = b' / b' % b /\ &0 < b' /\
1278      b' / b' = &1 <=> &0 < b' /\ b' / b' = &1 /\ aaa = &1 % b `]
1279 THEN REWRITE_TAC[ VECTOR_MUL_LID] THEN MESON_TAC[]);;
1280
1281
1282 let NOVE30 = prove(`! P l. ( ! x y z i j k s. ( P x y z i j k s <=> P y x z j i k s)
1283  /\ ( l x y z <=> l y x z ) ) /\ (! x y z i j k s. i <= j /\ P x y z i j k s ==>
1284 l x y z )   ==> (! x y z i j k s. P x y z i j k s ==> l x y z ) `,
1285 ONCE_REWRITE_TAC[ MESON[]` a ==> (!x y z i j k s. P x y z i j k s ==> l x y z) <=>
1286      (a ==> (!x y z i j k s. i <= j /\ P x y z i j k s ==> l x y z)) /\(a ==>
1287  (!x y z i j k s. ~(i <= j) /\ P x y z i j k s ==> l x y z)) `] THEN REPEAT
1288 GEN_TAC THEN
1289 CONJ_TAC THENL [MESON_TAC[]; MESON_TAC[REAL_ARITH ` ~( a <= b ) ==> b <= a `]]);;
1290
1291
1292
1293 let NOVE31 = prove(`! P l. ( ! x y z i j k s. ( P x y z i j k s <=> P z y x k j i s )
1294  /\ ( l x y z <=> l z y x ) ) /\ (! x y z i j k s. i <= j /\ i <= k /\ P x y z i j k s
1295  ==> l x y z )   ==> (! x y z i j k s. i <= j /\ P x y z i j k s ==> l x y z ) `,
1296 ONCE_REWRITE_TAC[ MESON[]` a ==> (!x y z i j k s. P x y z i j k s ==> l x y z) <=>
1297      (a ==> (!x y z i j k s. i <= k /\ P x y z i j k s ==> l x y z)) /\(a ==>
1298  (!x y z i j k s. ~(i <= k) /\ P x y z i j k s ==> l x y z)) `] THEN REPEAT
1299 GEN_TAC THEN CONJ_TAC THENL [MESON_TAC[];   MESON_TAC[REAL_LE_TRANS;
1300 REAL_ARITH ` ~( a <= b ) ==> b <= a `]]);;
1301
1302
1303
1304
1305 let IMP_IN_BA = prove(`! x y z a s. {x,y,z} UNION {a} IN Q_SYS s ==> {x,y,z} IN barrier s `,
1306 REWRITE_TAC[barrier; IN_ELIM_THM] THEN MESON_TAC[]);;
1307
1308
1309
1310 let IMP_IN_AFF4  = prove(` ! s v0 xx x y z. xx IN cone v0 {x, y, z} /\
1311  ~(xx IN UNIONS {aff_ge {v0} {v1, v2} | v1,v2 | barrier s {v0, v1, v2}}) /\
1312  {v0, x, y, z} IN Q_SYS s ==> xx IN aff_gt {v0} {x, y, z}`,
1313 REWRITE_TAC[cone; GSYM aff_ge_def; simp_def; IN_ELIM_THM] THEN
1314 REPLICATE_TAC 3 GEN_TAC THEN REWRITE_TAC[MESON[]` ( ! x y z. (? s i j k.
1315  P s i j k x y z ) /\ Q x y z ==> l x y z) <=> ( ! x y z i j k s.
1316 P s i j k x y z /\ Q x y z ==> l x y z ) `] THEN MATCH_MP_TAC NOVE30 THEN
1317 CONJ_TAC THENL [MESON_TAC[PER_SET3; REAL_ARITH ` a + b + c = b + a + c ` ;
1318   VECTOR_ARITH `(a:real^N ) + b + c = b + a + c `]; MATCH_MP_TAC NOVE31 THEN
1319 CONJ_TAC]THENL [MESON_TAC[PER_SET3; REAL_ARITH ` a + b + c = c + b + a ` ;
1320  VECTOR_ARITH `(a:real^N ) + b + c = c + b + a `]; PHA] THEN
1321 REWRITE_TAC[MESON[REAL_ARITH ` &0 <= i <=> i = &0 \/ &0 < i `]`
1322   &0 <= i /\ &0 <= j /\ &0 <= k /\ l <=> ( i = &0 \/ &0 < i ) /\ &0 <= j /\
1323    &0 <= k /\ l `] THEN KHANANG THEN REPEAT GEN_TAC THEN
1324 STRIP_TAC THENL [REPEAT (FIRST_X_ASSUM MP_TAC) THEN REPLICATE_TAC 3 DISCH_TAC
1325  THEN REWRITE_TAC[IMP_IMP] THEN ASM_SIMP_TAC[] THEN REWRITE_TAC[VECTOR_MUL_LZERO;
1326 VECTOR_ADD_LID; REAL_ADD_LID] THEN REWRITE_TAC[SET_RULE ` {v0, x, y, z} = {v0,y,z}
1327  UNION {x} `] THEN NHANH (SPEC_ALL IMP_IN_BA) THEN REWRITE_TAC[IN_UNIONS;
1328 IN_ELIM_THM] THEN REWRITE_TAC[MESON[IN]` barrier s a /\ l <=> a IN barrier s /\
1329 l`] THEN PHA THEN REWRITE_TAC[MESON[]` (? t. (? v1 v2 . P v1 v2 /\ t = Q v1 v2 )
1330 /\ xx IN t )  <=> (? v1 v2. P v1 v2 /\ xx IN Q v1 v2 ) `] THEN REWRITE_TAC[IN_ELIM_THM]
1331  THEN MESON_TAC[]; STRIP_TR THEN REWRITE_TAC[MESON[REAL_ARITH ` i <= j /\ &0 < i
1332 ==> &0 < j `]`  i <= j /\ i <= k /\ &0 < i /\l  <=> i <= j /\ i <= k /\ &0 < j /\
1333  &0 < k /\ &0 < i /\ l`] THEN MESON_TAC[]]);;
1334
1335
1336
1337
1338
1339 let VORO2_EX =prove(`! v0 s. voro2 v0 s = {x | (!w. s w /\ ~(w = v0) ==>
1340   d3 x v0 < d3 x w) /\ d3 x v0 < &2} `, REWRITE_TAC[voro2; voronoi; d3 ]
1341  THEN SET_TAC[]);;
1342
1343
1344
1345 let LEMMA81 = prove(`!(X:real^3 -> bool) Z s v0:real^3 .
1346      centered_pac s v0 /\
1347      Z = UNIONS {aff_ge {v0} {v1, v2} | v1,v2 | {v0, v1, v2} IN barrier s} /\
1348      X = UNIONS
1349      {aff_gt {v0} {v1, v2, v3} INTER
1350       aff_le {v1, v2, v3} {v0} INTER
1351       voro2 v0 s | v1,v2,v3 | {v0, v1, v2, v3} IN Q_SYS s}
1352      ==> voro2 v0 s SUBSET X UNION Z UNION VC v0 s`,
1353 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[SET_RULE ` as SUBSET a UNION b UNION c <=>
1354 ( as DIFF (b UNION c))   SUBSET a`] THEN REWRITE_TAC[SUBSET; IN_DIFF; IN_UNION;
1355  VC; lambda_x; IN_ELIM_THM; voro2;voronoi; GSYM d3;  DE_MORGAN_THM; centered_pac]
1356  THEN ABBREV_TAC ` ketluan x  = ((x:real^3) IN (X:real^3 -> bool))` THEN SIMP_TAC[]
1357  THEN PHA THEN REWRITE_TAC[MESON[]` a /\b/\e/\c==>d <=> c ==> a/\b/\e==>d`] THEN
1358  DISCH_TAC THEN REWRITE_TAC[GSYM (MESON[]` a /\b/\e/\c==>d <=> c ==> a/\b/\e==>d`)]
1359 THEN REWRITE_TAC[MESON[trg_d3_sym]` d3 x v0 < &2 /\ aa/\
1360           ((~(d3 v0 x < &2) \/ l) \/ l') <=> d3 x v0 < &2 /\ aa/\ (l\/ l')`; IN] THEN
1361 PHA THEN REWRITE_TAC[MESON[]` (!w. s w /\ ~(w = v0) ==> d3 x v0 < d3 x w) /\
1362  aa /\ bb /\ (cc \/ ~(!w. s w /\ dd w /\ ee w /\ ~(w = v0) ==> d3 x v0 < d3 x w)) <=>
1363      (!w. s w /\ ~(w = v0) ==> d3 x v0 < d3 x w) /\ aa /\ bb /\ cc`] THEN
1364 REWRITE_TAC[obstruct] THEN ONCE_REWRITE_TAC[BAR_TRI] THEN
1365 REWRITE_TAC[ MESON[]`(?bar. (?x y z. bar = {x, y, z} /\ P {x, y, z}) /\ Q bar) <=>
1366      (?x y z. P {x, y, z} /\ Q {x, y, z})`] THEN NHANH (MESON[]` ~(conv0 {v0, x} INTER
1367 conv {x', y, z} = {}) ==>  v0 IN {x' ,y,z} \/ ~( v0 IN {x', y,z})`) THEN KHANANG THEN
1368 NHANH (MESON[IN_SET3; SET_RULE` x = a ==> {x,b,c} = {a,b,c} /\ {x,b,c} = {b,c,a} /\
1369  {x,b,c} = {b,a,c}  `]`  x IN {a,b,c} ==> (? yy zz. {x,yy,zz} = {a,b,c})`) THEN
1370 REWRITE_TAC[EXISTS_OR_THM] THEN NGOAC THEN REWRITE_TAC[MESON[]`(?x' y z. P {x', y, z}
1371 /\ (?yy zz. {x, yy, zz} = {x', y, z})) <=> (?y z. P {x, y, z})`] THEN
1372 NHANH (CUTHE4 IN_AFF_GE_CON) THEN PHA THEN
1373 REWRITE_TAC[SET_RULE`  ~UNIONS {aff_ge {v0} {v1, v2} | v1,v2 | barrier s {v0, v1, v2}} x /\
1374 ((?y z. {v0, y, z} IN barrier s /\ aaa y z /\ x IN aff_ge {v0} {y, z} /\
1375  bbb y z) \/  last) <=> ~UNIONS {aff_ge {v0} {v1, v2} | v1,v2 | barrier s {v0, v1, v2}} x /\
1376      last`] THEN REWRITE_TAC[DE_MORGAN_THM] THEN SIMP_TAC[GSYM NOV20] THEN
1377 REWRITE_TAC[d3; GSYM IN_VO_EQ] THEN NHANH (MESON[X_IN_VOR_X; VORONOI_CONV]` x IN voronoi v0 s
1378    ==> v0 IN voronoi v0 s /\ convex (voronoi v0 s )`) THEN
1379 NHANH (MESON[CONVEX_IM_CONV02_SU ]` x IN voronoi v0 s /\    v0 IN voronoi v0 s /\
1380  convex (voronoi v0 s) ==> conv0 {v0,x} SUBSET voronoi v0 s `) THEN PHA THEN
1381 DISCH_TAC THEN GEN_TAC THEN STRIP_TAC THENL [REPEAT (FIRST_X_ASSUM MP_TAC) THEN
1382 REWRITE_TAC[ IMP_IMP] THEN PHA THEN NHANH (SET_RULE` conv0 {v0, x} SUBSET voronoi v0 s
1383 /\a1  /\a2  /\a3  /\ ~(conv0 {v0, x} INTER conv {x', y, z} = {}) /\ l ==>
1384   ~( voronoi v0 s INTER conv {x', y, z} = {})`) THEN NHANH (MESON[FOUR_POINTS]
1385 ` {x', y, z} IN barrier s /\ a1 /\   ~(v0 IN {x', y, z}) ==> CARD {x',y,z, v0} = 4 `)
1386  THEN PHA THEN NHANH (SET_RULE `  conv0 {v0, x} SUBSET s /\ a1 /\a2 /\a3 /\
1387  ~(conv0 {v0, x} INTER s1  = {}) /\ l ==> ~( s INTER s1 = {}) `) THEN PHA THEN
1388 REWRITE_TAC[MESON[]`( s x /\ l <=>l/\ s x)/\ (a IN barrier s /\ l <=>
1389    l /\ a IN barrier s) `] THEN NHANH (SPEC_ALL (REWRITE_RULE[CONV3_EQ] IN_AFF_GE_CON))
1390  THEN PHA THEN REWRITE_TAC[SET_RULE ` ~UNIONS {aff_ge {v0} {v1, v2} | v1,v2 |
1391   barrier s {v0, v1, v2}} x /\  a1 /\ x IN aff_ge {v0} {y, z} /\
1392    a2 /\ a3/\ {v0, y, z} IN barrier s /\ a4 <=> F `] ; REPEAT (FIRST_X_ASSUM MP_TAC)]
1393  THEN REWRITE_TAC[ IMP_IMP] THEN PHA THEN
1394 NHANH (SET_RULE` conv0 {v0, x} SUBSET voronoi v0 s /\a1  /\a2  /\a3  /\
1395  ~(conv0 {v0, x} INTER conv {x', y, z} = {}) /\ l ==>
1396   ~( voronoi v0 s INTER conv {x', y, z} = {})`) THEN
1397 NHANH (MESON[FOUR_POINTS]` {x', y, z} IN barrier s /\ a1 /\
1398   ~(v0 IN {x', y, z}) ==> CARD {x',y,z, v0} = 4 `) THEN PHA THEN NHANH (SET_RULE `
1399  conv0 {v0, x} SUBSET s /\ a1 /\a2 /\a3 /\ ~(conv0 {v0, x} INTER s1  = {}) /\ l
1400 ==> ~( s INTER s1 = {}) `) THEN PHA THEN REWRITE_TAC[MESON[]`( s x /\ l <=>l/\
1401  s x)/\ (a IN barrier s /\ l <=>   l /\ a IN barrier s) `] THEN PHA THEN
1402 NHANH (MESON[IMP_IN_Q_SYS; IN]` CARD {x', y, z, v0} = 4 /\
1403  ~(voronoi v0 s INTER conv {x', y, z} = {}) /\ {x', y, z} IN barrier s /\
1404  s v0 ==> {v0,x',y,z} IN Q_SYS s `) THEN NHANH (SPEC_ALL AFF_LE_CONE) THEN PHA THEN
1405 ONCE_REWRITE_TAC[MESON[IN] ` ~ UNIONS s x <=> ~ ( x IN UNIONS s ) `] THEN
1406 ONCE_REWRITE_TAC[MESON[]` a1 /\a /\ b /\ x IN cone v0 {x', y, z} /\ l <=>a /\ b /\ l /\
1407   x IN cone v0 {x', y, z} /\ a1 `] THEN PHA THEN REWRITE_TAC[MESON[]` a IN Q_SYS s /\
1408  b /\ c <=> b /\ c /\ a IN Q_SYS s`] THEN NHANH (SPEC_ALL IMP_IN_AFF4) THEN
1409 NGOAC THEN REWRITE_TAC[MESON[]` (a /\ b ) /\ x IN aff_gt {v0} {x', y, z} <=>
1410   x IN aff_gt {v0} {x', y, z}/\ b/\ a `] THEN PHA THEN DAO THEN
1411 REWRITE_TAC[GSYM VORO2_EX] THEN REWRITE_TAC[prove(`dist (x,v0) < &2 /\a1/\a2/\a3 /\
1412 x IN voronoi v0 s /\ l  <=> a1/\a2/\a3 /\ l /\ x IN voro2 v0 s`, REWRITE_TAC[GSYM d3;
1413   voro2; IN_ELIM_THM] THEN MESON_TAC[])] THEN REWRITE_TAC[MESON[]`x IN aff_le a s /\
1414  l <=> l /\ x IN aff_le a s `] THEN DAO THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
1415 SIMP_TAC[] THEN ONCE_REWRITE_TAC[MESON[]` (! x. P x ) /\ a = b /\ l <=> b = a /\ l /\
1416   (! x . P x )`] THEN SIMP_TAC[] THEN MATCH_MP_TAC (MESON[]` ( a1 /\a2/\a3/\a4 ==> l )
1417 ==> ( a1/\a2/\a3/\a4/\a5 ==> l ) `) THEN REWRITE_TAC[IN_UNIONS; IN_ELIM_THM] THEN
1418 REWRITE_TAC[ MESON[]` (?t. (? a b c. P a b c /\ t = Q a b c ) /\ x IN t )
1419   <=> (? a b c. P a b c /\ x IN Q a b c ) `] THEN REWRITE_TAC[IN_INTER] THEN
1420 SET_TAC[]);;