legacy/oldleg/geomdetail.ml

   1 (* ================================ *)\r
   2 (* ===== NGUYEN QUANG TRUONG ====== *)\r
   3 \r
   4 (*\r
   5 \r
   6 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\r
   7 \r
   8 *)\r
   9 let voronoi_trg = new_definition ` voronoi_trg v S = { x | !w. ((S w) /\ ~(w=v))\r
  10 ==> (dist ( x , v ) < dist ( x , w )) }`;;\r
  11 \r
  12 \r
  13 let conv0_2 = new_definition ` conv0_2 s = conv0 s `;;\r
  14 \r
  15 \r
  16 let convex = new_definition `convex s <=> !x y u v. x IN s /\ y IN s /\ &0 <= u /\\r
  17      &0 <= v /\ (u + v = &1) ==> (u % x + v % y) IN s`;;\r
  18 \r
  19 let aff = new_definition `aff = ( hull ) affine`;;         \r
  20            \r
  21 \r
  22 \r
  23 let conv_trg = new_definition ` conv_trg s = convex hull s`;;\r
  24 \r
  25 let border = new_definition ` border s = { x | ! ep. ep > &0 /\ ( ? a b. ~ (b IN s ) /\\r
  26  dist (b, x) < ep /\ a IN s /\ dist (a, x) < ep ) }`;;  \r
  27 \r
  28 let packing_trg = new_definition `packing_trg (s:real^3 -> bool) = (! x y.  s x /\ s y /\ ( ~(x=y))\r
  29   ==> dist ( x, y) >= &2 ) `;;\r
  30 \r
  31 let center_pac = new_definition ` center_pac s v = ( packing_trg s /\ s v )`;;\r
  32 \r
  33 let centered_pac = new_definition ` centered_pac s v = ( packing s /\ v IN s )`;;\r
  34 \r
  35 let d3 = new_definition ` d3 x y = dist (x,y)`;;\r
  36 \r
  37 let voronoi2 = new_definition ` voronoi2 v S = {x| x IN voronoi_trg v S /\ d3 x v < &2 }`;;\r
  38 \r
  39 let voro2 = new_definition ` voro2 v s = {x| x IN voronoi v s /\ d3 x v < &2 }`;;\r
  40 \r
  41 let t0 = new_definition ` t0 = #1.255`;;\r
  42 \r
  43 \r
  44 let quasi_tri = new_definition ` quasi_tri tri s = ( packing s /\ \r
  45   tri SUBSET s /\\r
  46   (? a b c. ~( a=b \/ b=c\/ c=a) /\  { a, b, c } = tri ) /\\r
  47   (! x y.  ( x IN tri /\ y IN tri /\ (~(x=y)) ) ==> ( d3 x y <= &2 * t0 )))`;;\r
  48 \r
  49 \r
  50 let simplex = new_definition ` simplex (d:real^3 -> bool) s = ( packing s /\\r
  51   d SUBSET s /\ \r
  52 ( ? v1 v2 v3 v4. ~( v1 = v2 \/ v3 = v4 ) /\ {v1, v2 } INTER {v3, v4 } = {}/\ {v1,v2,v3,v4} = d )\r
  53  )`;;\r
  54 \r
  55 let quasi_reg_tet = new_definition ` quasi_reg_tet x s = ( simplex x s /\\r
  56    (! v w. ( v IN x /\ w IN x /\ \r
  57     ( ~ ( v = w))) \r
  58   ==> ( d3 v w <= &2 * t0 )) )`;;\r
  59 \r
  60 let quarter = new_definition ` quarter (q:real^3 -> bool) s =\r
  61   ( packing s /\\r
  62          simplex q s /\\r
  63          (?v w.\r
  64               v IN q /\\r
  65               w IN q /\\r
  66               &2 * t0 <= d3 v w /\\r
  67               d3 v w <= sqrt (&8) /\\r
  68               (!x y.\r
  69                    x IN q /\ y IN q /\ ~({x, y} = {v, w})\r
  70                    ==> d3 x y <= &2 * t0)))`;;\r
  71 \r
  72 let diagonal = new_definition ` diagonal d1 d2 q s = ( quarter q s /\\r
  73          {d1, d2} SUBSET q /\\r
  74          (!x y. x IN q /\ y IN q ==> d3 x y <= d3 d1 d2))`;;\r
  75 \r
  76  let strict_qua = new_definition ` strict_qua d s = ( quarter d s /\ \r
  77   ( ? x y. x IN d /\ y IN d /\ &2 * t0 < d3 x y /\ d3 x y < sqrt( &8 ) ))`;; \r
  78 \r
  79 let strict_qua2 = new_definition ` strict_qua2 d (ch:real^3 -> bool ) s = ( quarter d s /\ ch SUBSET d \r
  80   /\ ( ? x y. ~( x = y ) /\ ch = {x,y} /\ &2 * t0 < d3 x y /\ d3 x y < sqrt ( &8 ) ) )`;;\r
  81 \r
  82 \r
  83 \r
  84 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 =\r
  85          ( packing s /\\r
  86          ( &2 * t0 < dist (v,w) /\ dist (v,w) < sqrt (&8) ) /\\r
  87          (!x. x IN {v1, v2, v3, v4}\r
  88               ==> dist (x,v) <= &2 * t0 /\ dist (x,w) <= &2 * t0) /\\r
  89          {v, w, v1, v2, v3, v4} SUBSET s /\\r
  90          (&2 <= dist (v1,v2) /\ dist (v1,v2) <= &2 * t0) /\\r
  91          (&2 <= dist (v2,v3) /\ dist (v2,v3) <= &2 * t0) /\\r
  92          (&2 <= dist (v3,v4) /\ dist (v3,v4) <= &2 * t0) /\\r
  93          &2 <= dist (v4,v1) /\\r
  94          dist (v4,v1) <= &2 * t0 ) `;;\r
  95 \r
  96 \r
  97 let adjacent_pai = new_definition ` adjacent_pai v v1 v3 v2 v4 s = ( strict_qua2 { v , v1 , v3 , v2 } { v1 , v3 } s\r
  98   /\ strict_qua2 { v , v1 , v3 , v4 } { v1 , v3 } s /\\r
  99   ( conv0 { v , v1 , v3 , v2 } INTER conv0 { v , v1 , v3 , v4 } = {} ) )`;;\r
 100 \r
 101 let conflicting_dia = new_definition ` conflicting_dia v v1 v3 v2 v4 s = ( adjacent_pai v v1 v3 v2 v4 s\r
 102 /\ adjacent_pai v v2 v4 v1 v3 s )`;;\r
 103 \r
 104  let interior_pos = new_definition `interior_pos v v1 v3 v2 v4 s = ( conflicting_dia v v1 v3 v2 v4 s \r
 105   /\ ~( conv0 { v1, v3 } INTER conv0 { v , v2 , v4 } = {} ))`;;  \r
 106 \r
 107 let isolated_qua = new_definition ` isolated_qua q s = ( quarter q s /\ ~( ? v v1 v2 v3 v4. q = \r
 108   {v, v1, v2, v3} /\ adjacent_pai v v1 v2 v3 v4 s))`;;\r
 109 \r
 110 let isolated_pai = new_definition ` isolated_pai q1 q2 s = ( isolated_qua q1 s /\ isolated_qua q2 s /\\r
 111   ~ (conv0 q1 INTER conv0 q2 = {}))`;;\r
 112 \r
 113 let anchor = new_definition ` anchor (v:real^3) v1 v2 s = ( {v, v1, v2} SUBSET s /\ d3 v1 v2 <= sqrt ( &8 ) /\\r
 114   d3 v1 v2 >= &2 * t0 /\ d3 v v1 <= &2 * t0 /\ d3 v v2 <= &2 * t0 )`;;\r
 115 \r
 116 let anchor_points = new_definition ` anchor_points v w s = { t | &2 * t0 <= d3 v w /\\r
 117   anchor t v w s }`;;\r
 118 \r
 119 let Q_SYS = new_definition ` Q_SYS s = {q | quasi_reg_tet q s \/\r
 120               strict_qua q s /\\r
 121               (?c d.\r
 122                    !qq. c IN q /\\r
 123                         d IN q /\\r
 124                         d3 c d > &2 * t0 /\\r
 125                         (quasi_reg_tet qq s \/ strict_qua qq s) /\\r
 126                         conv0 {c, d} INTER conv0 qq = {}) \/\r
 127               strict_qua q s /\\r
 128               (CARD\r
 129                {t | ?v w.\r
 130                         v IN q /\ w IN q /\ &2 * t0 < d3 v w /\ anchor t v w s} >\r
 131                4 \/\r
 132                CARD\r
 133                {t | ?v w.\r
 134                         v IN q /\ w IN q /\ &2 * t0 < d3 v w /\ anchor t v w s} =\r
 135                4 /\\r
 136                ~(?v1 v2 v3 v4 v w. v IN q /\\r
 137                      w IN q /\\r
 138                      {v1, v2, v3, v4} SUBSET anchor_points v w s\r
 139                       /\\r
 140                      \r
 141                      &2 * t0 < d3 v w /\\r
 142                      quartered_oct v w v1 v2 v3 v4 s))\r
 143   \/ (? v w v1 v2 v3 v4. q = { v, w, v1, v2} /\ quartered_oct v w v1 v2 v3 v4 s )\r
 144   \/ (? v v1 v3 v2 v4. ( q = {v, v1, v2, v3} \/ q = {v, v1, v3, v4} ) /\\r
 145   interior_pos v v1 v3 v2 v4 s /\ anchor_points v1 v3 s = { v, v2, v4} /\\r
 146   anchor_points v2 v4 s = { v, v1, v3 } )}`;; \r
 147 \r
 148 let barrier = new_definition ` barrier s = { { (v1 : real^3 ) , ( v2 :real^3 ) , (v3 :real^3) } |\r
 149   quasi_tri { v1 , v2 , v3 } s \/ \r
 150   (? v4. ( { v1 , v2 , v3 } UNION { v4 }) IN Q_SYS s ) } `;;\r
 151 \r
 152 let obstructed = new_definition ` obstructed x y s = ( ? bar. bar IN barrier s /\\r
 153   ( ~ (conv0_2 { x , y } INTER conv_trg bar = {})))`;;\r
 154 \r
 155 let obstruct = new_definition ` obstruct x y s = ( ? bar. bar IN barrier s /\\r
 156   ( ~ (conv0 { x , y } INTER conv bar = {})))`;;\r
 157 \r
 158 let unobstructed = new_definition ` unobstructed x y s = ( ~( obstructed x y s ))`;;\r
 159 \r
 160 let VC_trg = new_definition ` VC_trg x s = { z | d3 x z < &2 /\ ~obstructed x z s /\\r
 161   (! y. y IN s /\ ~ ( x = y ) /\ ~(obstructed z y s)   ==> d3 x z < d3 y z )} `;;  \r
 162 \r
 163 let VC_INFI_trg = new_definition ` VC_INFI_trg s = { z | ( ! x. x IN s /\\r
 164   ~( z IN VC_trg x s ))}`;;\r
 165 \r
 166 \r
 167 let lambda_x = new_definition `lambda_x x s = {w | w IN s /\ d3 w x < &2 /\\r
 168 ~obstructed w x s }`;;\r
 169 \r
 170 let lambda_y = new_definition ` lambda_y y s = { w| w IN s /\ d3 w y < &2 /\\r
 171    ~obstruct w y s} `;;\r
 172 \r
 173 let VC = new_definition `VC v s = { x | v IN lambda_x x s /\ \r
 174 (!w. w IN lambda_x x s /\ ~(w = v) ==> d3 x v < d3 x w) }`;;\r
 175 \r
 176 let VC_INFI = new_definition ` VC_INFI s = { z | ( ! x. ~( z IN VC x s ))}`;;\r
 177 \r
 178 \r
 179 let SET_TAC =\r
 180    let basicthms =\r
 181     [NOT_IN_EMPTY; IN_UNIV; IN_UNION; IN_INTER; IN_DIFF; IN_INSERT;\r
 182      IN_DELETE; IN_REST; IN_INTERS; IN_UNIONS; IN_IMAGE] in\r
 183    let allthms = basicthms @ map (REWRITE_RULE[IN]) basicthms @\r
 184                  [IN_ELIM_THM; IN] in\r
 185    let PRESET_TAC =\r
 186      TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ)) THEN\r
 187      REPEAT COND_CASES_TAC THEN\r
 188      REWRITE_TAC[EXTENSION; SUBSET; PSUBSET; DISJOINT; SING] THEN\r
 189      REWRITE_TAC allthms in\r
 190    fun ths ->\r
 191      PRESET_TAC THEN\r
 192      (if ths = [] then ALL_TAC else MP_TAC(end_itlist CONJ ths)) THEN\r
 193      MESON_TAC[];;\r
 194 \r
 195  let SET_RULE tm = prove(tm,SET_TAC[]);;\r
 196 \r
 197 (* some TRUONG TACTICS *)\r
 198 \r
 199 let PHA = REWRITE_TAC[ MESON[] ` (a/\b)/\c <=> a/\ b /\ c `];;\r
 200 \r
 201 let NGOAC = REWRITE_TAC[ MESON[] ` a/\b/\c <=> (a/\b)/\c `];;\r
 202 \r
 203 let DAO = NGOAC THEN REWRITE_TAC[ MESON[]` a /\ b <=> b /\ a`];;\r
 204 \r
 205 let PHAT = REWRITE_TAC[ MESON[] ` (a\/b)\/c <=> a\/b\/c `];;\r
 206 \r
 207 let NGOACT =  REWRITE_TAC[ GSYM (MESON[] ` (a\/b)\/c <=> a\/b\/c `)];;\r
 208 \r
 209 let KHANANG = PHA THEN REWRITE_TAC[ MESON[]` ( a\/ b ) /\ c <=> a /\ c \/ b /\ c `] THEN \r
 210  REWRITE_TAC[ MESON[]` a /\ ( b \/ c ) <=> a /\ b \/ a /\ c `];;\r
 211 \r
 212 let ATTACH thm = MATCH_MP (MESON[]` ! a b. ( a ==> b ) ==> ( a <=> a /\ b )`) thm;;\r
 213 \r
 214 let CUTHE1 th = MATCH_MP (MESON[]` ( ! a. P a ) ==> P a `) th ;;\r
 215 \r
 216 let CUTHE2 th = MATCH_MP (MESON[]` ( ! a b. P a b ) ==> P a b`) th ;;\r
 217 \r
 218 let CUTHE3 th = MATCH_MP (MESON[]` ( ! a b c. P a b c ) ==> P a b c`) th ;;\r
 219 \r
 220 let CUTHE4 th = MATCH_MP (MESON[]` ( ! a b c d. P a b c d ) ==> P a b c d`) th ;;\r
 221 \r
 222 let CUTHE5 th = MATCH_MP (MESON[]` ( ! a b c d e. P a b c d e) ==> P a b c d e`) th ;;\r
 223 \r
 224 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 ;;\r
 225 \r
 226 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 ;;\r
 227 \r
 228 let NHANH tm = ONCE_REWRITE_TAC[ ATTACH (tm)];;\r
 229 \r
 230 \r
 231 let trg_sub_bo = prove ( `A SUBSET B <=> (!x. A x ==> B x)`, SET_TAC[] );;\r
 232 \r
 233 let trg_sub_se = prove ( `A SUBSET B <=> (!x. x IN A  ==> x IN B )`, SET_TAC[] );;\r
 234 \r
 235 let trg_setbool = prove (`x IN A <=> A x `, SET_TAC[] );;\r
 236 \r
 237 let trg_boolset = prove (` A x <=>  x IN A `, SET_TAC[] );;\r
 238 \r
 239 let trg_in_union = prove (` x IN ( A UNION B ) <=> x IN A \/ x IN B `, SET_TAC[]);;\r
 240 \r
 241 let not_in_set3 = prove ( `~ ( x IN { z | A z /\ B z /\ C z } ) <=> ~ A x \/ ~ B x \/ ~ C x `,\r
 242   SET_TAC[]);;\r
 243 \r
 244 let trg_d3_sym = prove ( `! x y. d3 x y = d3 y x `, SIMP_TAC[d3; DIST_SYM]);;\r
 245 \r
 246 let affine_hull_e = prove (`affine hull {} = {}`, \r
 247  REWRITE_TAC[AFFINE_EMPTY; AFFINE_HULL_EQ]);;\r
 248 \r
 249 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 \r
 250   /\ Q a b ))`;;\r
 251 \r
 252 let wlog_real = MESON[REAL_ARITH `( ! a b:real. a <= b \/ b <= a )`] ` \r
 253 (! a:real b:real . P a b = P b a ) ==> ((? a:real b . P a b ) <=> ( ? a b. P a b \r
 254   /\ a <= b ))`;;\r
 255 \r
 256 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)\r
 257      ==> ((?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))`;;\r
 258 \r
 259 \r
 260 let tarski_arith = new_axiom `! bar. bar IN barrier s /\\r
 261                                ~(conv_trg bar INTER conv0_2 { v0 , x } ={}) /\ \r
 262                                ~ ( v0 IN bar ) /\\r
 263                                  x IN voronoi2 v0 s /\ \r
 264                               ~ ( x IN UNIONS {aff_ge {v0} {v1, v2} | {v0, v1, v2} IN barrier s} ) \r
 265                             ==> { v0 } UNION bar IN Q_SYS s `;;\r
 266 \r
 267 let simp_def = new_axiom ` (! a x y (z:real^A).\r
 268                               aff_ge {a} {x, y, z} = { t | ? s i j k. &0 <= i \r
 269                               /\ &0 <= j /\ &0 <= k /\ s + i + j + k = &1 /\\r
 270                               t = s % a + i % x + j % y + k % z }) /\\r
 271 \r
 272           (!v0 v1 v2.\r
 273           aff_ge {v0} {v1, v2} =\r
 274           {t | ?u v w.\r
 275                    &0 <= v /\\r
 276                    &0 <= w /\\r
 277                    u + v + w = &1 /\\r
 278                    t = u % v0 + v % v1 + w % v2}) /\\r
 279      (!v0 v1 v2 v3.\r
 280           aff_gt {v0} {v1, v2, v3} =\r
 281           {t | ?x y z w.\r
 282                    &0 < y /\\r
 283                    &0 < z /\\r
 284                    &0 < w /\\r
 285                    x + y + z + w = &1 /\\r
 286                    t = x % v0 + y % v1 + z % v2 + w % v3}) /\\r
 287      (!v0 v1 v2 v3.\r
 288           aff_le {v1, v2, v3} {v0} =\r
 289           {t | ?a b c d.\r
 290                    d <= &0  /\\r
 291                    a + b + c + d = &1 /\\r
 292                    t = a % v1 + b % v2 + c % v3 + d % v0}) /\\r
 293      ( ! v0 v1. conv0_2 { v0, v1 } = { x | ? t. &0 < t /\ t < &1 /\ x = t % v0 + (&1 - t ) % v1 } ) /\\r
 294      (! s. conv_trg s = conv s )`;;\r
 295 \r
 296 \r
 297 let AFFINE_HULL_SINGLE = prove(`!x. affine hull {x} = {x}`,\r
 298   SIMP_TAC[AFFINE_SING; AFFINE_HULL_EQ]);;\r
 299 \r
 300 let usefull = MESON[] ` (!x. a x ==> b x ) ==>(?x. a x ) ==> c ==> d <=>\r
 301  (!x. a x ==> b x) ==> (?x. a x /\ b x ) ==> c ==> d `;;\r
 302 \r
 303 let v1_in_convex3 = prove (` ! v1 v2 v3. v1 IN {t | ?a b c.\r
 304               &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1 /\\r
 305  t = a % v1 + b % v2 + c % v3}`, REPEAT GEN_TAC THEN REWRITE_TAC[ IN_ELIM_THM] THEN \r
 306 EXISTS_TAC ` &1 ` THEN EXISTS_TAC ` &0 ` THEN EXISTS_TAC ` &0 ` THEN \r
 307 REWRITE_TAC[ VECTOR_ARITH ` &1 % v1 + &0 % v2 + &0 % v3 = v1 `] THEN REAL_ARITH_TAC);;\r
 308 \r
 309 \r
 310 let v3_in_convex3 = prove( `! v1 v2 v3. v3 IN\r
 311      {t | ?a b c.\r
 312               &0 <= a /\\r
 313               &0 <= b /\\r
 314               &0 <= c /\\r
 315               a + b + c = &1 /\\r
 316               t = a % v1 + b % v2 + c % v3}`, REWRITE_TAC[IN_ELIM_THM] THEN REPEAT GEN_TAC\r
 317 THEN REPLICATE_TAC 2 (EXISTS_TAC `&0`) THEN EXISTS_TAC ` &1` THEN REWRITE_TAC[VECTOR_MUL_LZERO;\r
 318  VECTOR_ADD_LID; VECTOR_MUL_LID] THEN REAL_ARITH_TAC);;\r
 319 \r
 320 \r
 321 let v1v2v3_in_convex3 = prove (` ! v1 v2 v3 . v1 IN {t | ?a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\ \r
 322 a + b + c = &1 /\ t = a % v1 + b % v2 + c % v3}\r
 323    /\ v2 IN {t | ?a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1 /\ t = a % v1 + b % v2 + c % v3}\r
 324   /\ v3 IN {t | ?a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1 /\ t = a % v1 + b % v2 + c % v3}`,\r
 325 REWRITE_TAC[v1_in_convex3; v3_in_convex3] THEN REPEAT GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN \r
 326 EXISTS_TAC ` &0` THEN EXISTS_TAC ` &1` THEN EXISTS_TAC ` &0` THEN\r
 327 REWRITE_TAC[VECTOR_ARITH` v2 = &0 % v1 + &1 % v2 + &0 % v3`] THEN REAL_ARITH_TAC);;\r
 328 \r
 329 \r
 330 let convex3 = prove( `!v1 v2 v3.\r
 331      convex\r
 332      {t | ?a b c.\r
 333               &0 <= a /\\r
 334               &0 <= b /\\r
 335               &0 <= c /\\r
 336               a + b + c = &1 /\\r
 337               t = a % v1 + b % v2 + c % v3}`,\r
 338 REWRITE_TAC[convex; IN_ELIM_THM] THEN \r
 339 REPEAT GEN_TAC THEN STRIP_TAC THEN \r
 340 EXISTS_TAC ` u * a + v * a'` THEN \r
 341 EXISTS_TAC ` u * b + v * b'` THEN \r
 342 EXISTS_TAC ` u * c + v * c'` THEN \r
 343 REPEAT (FIRST_X_ASSUM MP_TAC) THEN \r
 344 REWRITE_TAC[MESON[] ` a==> b==> c <=> a /\ b==> c`] THEN PHA THEN \r
 345 REWRITE_TAC[ MESON[]` &0 <= a /\ l <=> l /\ &0 <= a `] THEN PHA THEN \r
 346 NHANH (MESON[REAL_LE_MUL; REAL_ARITH ` &0 <= a /\ &0 <= b ==> &0 <= a +b `]` &0 <= v /\\r
 347  &0 <= u /\\r
 348  &0 <= c' /\\r
 349  &0 <= b' /\\r
 350  &0 <= a' /\\r
 351  &0 <= c /\\r
 352  &0 <= b /\\r
 353  &0 <= a ==> &0 <= u * c + v * c' /\\r
 354      &0 <= u * b + v * b' /\\r
 355      &0 <= u * a + v * a'`) THEN \r
 356 REWRITE_TAC[REAL_ARITH` ( a + y ) + ( b + x ) + c + z = ( a + b + c) + (\r
 357   y + x + z ) `] THEN \r
 358 REWRITE_TAC[REAL_ARITH ` a * b + a * c = a * ( b + c) `] THEN \r
 359 SIMP_TAC[] THEN \r
 360 REWRITE_TAC[ REAL_ARITH ` a * &1 = a `] THEN SIMP_TAC[] THEN \r
 361 REWRITE_TAC[VECTOR_ARITH` u % (a % v1 + b % v2 + c % v3) + v % (a' % v1 + b' % v2 + c' % v3) =\r
 362      (u * a + v * a') % v1 + (u * b + v * b') % v2 + (u * c + v * c') % v3`]);;\r
 363 \r
 364 let INTERS_SUBSET = SET_RULE `! P t0. P t0 ==> INTERS { t| P t } SUBSET t0`;;\r
 365 \r
 366 let SET3_SUBSET = SET_RULE`! a b c. {a,b,c} SUBSET s <=> a IN s /\ b IN s /\ c IN s `;;\r
 367 \r
 368 let SUM_TWO_RATIO = REAL_FIELD ` ~(a + b = &0) <=> a / ( a + b) + b /(a+b) = &1`;; \r
 369 \r
 370 let minconvex3 = prove(`!t v1 v2 v3.\r
 371          convex t /\ {v1, v2, v3} SUBSET t\r
 372          ==> (!a b c.\r
 373                   &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1\r
 374                   ==> a % v1 + b % v2 + c % v3 IN t)`,\r
 375 REPEAT GEN_TAC THEN \r
 376 REWRITE_TAC[convex; SET3_SUBSET] THEN \r
 377 STRIP_TAC THEN \r
 378 REPEAT GEN_TAC THEN \r
 379 ONCE_REWRITE_TAC[ MESON[]` &0 <= a /\ &0 <= b /\ l<=> ( a + b = &0 \/ \r
 380   ~( a + b = &0)) /\ &0 <= a /\ &0 <= b /\ l`] THEN \r
 381 REWRITE_TAC[RIGHT_OR_DISTRIB] THEN \r
 382 REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a ==> c ) /\ ( b ==> c )`] THEN \r
 383 REWRITE_TAC[REAL_ARITH` a + b = &0 /\ &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1\r
 384   <=> &0 = a /\ &0 = b /\ &1 = c `] THEN \r
 385 ONCE_REWRITE_TAC[ EQ_SYM_EQ] THEN \r
 386 SIMP_TAC[] THEN \r
 387 ASM_REWRITE_TAC[ VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_LID] THEN \r
 388 REWRITE_TAC[MESON[]`&0 = a + b <=> a + b = &0`; SUM_TWO_RATIO] THEN \r
 389 NHANH (MESON[REAL_ARITH ` &0 <= a /\ &0 <= b ==> &0 <= a + b `]`\r
 390   dau /\ &0 <= a /\ &0 <= b /\ l ==> &0 <= a + b `) THEN \r
 391 NHANH (MESON[REAL_LE_DIV]` (aa /\ &0 <= a /\ &0 <= b /\ bb) /\ &0 <= a + b\r
 392      ==> &0 <= a / (a + b) /\ &0 <= b / (a + b)`) THEN \r
 393 REWRITE_TAC[GSYM SUM_TWO_RATIO] THEN \r
 394 PHA THEN \r
 395 NHANH (MESON[REAL_DIV_LMUL]` ~(a + b = &0) ==> a = (a+b) *(a/(a+b)) /\ b = \r
 396   (a+b) *(b/(a+b))`) THEN \r
 397 REWRITE_TAC[MESON[VECTOR_MUL_RCANCEL]` ( dau /\ a = (a + b) * a / (a + b) /\ b = (a + b) * b / (a + b))\r
 398   /\ l ==> a % v1 + b % v2 + c % v3 IN t <=>\r
 399   ( dau /\ a = (a + b) * a / (a + b) /\ b = (a + b) * b / (a + b))\r
 400   /\ l ==> ((a + b) * a / (a + b)) % v1 + ((a + b) * b / (a + b)) % v2 + c % v3 IN t`] THEN \r
 401 REWRITE_TAC[ VECTOR_ARITH ` ((a + b) * a / (a + b)) % v1 + ((a + b) * b / (a + b)) % v2 + c % v3 \r
 402   = (a + b) % ( (a / (a + b)) % v1 + (b / (a + b)) % v2) + c % v3 `] THEN \r
 403 REWRITE_TAC[SUM_TWO_RATIO] THEN \r
 404 ASM_MESON_TAC[ REAL_ARITH` a + b + c = (a + b ) + c`]);;\r
 405 \r
 406 \r
 407 let EQ_EXPAND = MESON[] `(a <=> b) <=> ( a ==> b ) /\ ( b ==> a )` ;;\r
 408 \r
 409 \r
 410 \r
 411 let OTHER_CONVEX_CONDI = prove(` ! s. convex s <=> (! a b c v1 v2 v3. {v1, v2, v3} SUBSET s /\\r
 412     &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1\r
 413                   ==> a % v1 + b % v2 + c % v3 IN s)`,\r
 414 REWRITE_TAC[EQ_EXPAND; MESON[minconvex3]`!s. (convex s\r
 415       ==> (!a b c v1 v2 v3.\r
 416                {v1, v2, v3} SUBSET s /\\r
 417                &0 <= a /\\r
 418                &0 <= b /\\r
 419                &0 <= c /\\r
 420                a + b + c = &1\r
 421                ==> a % v1 + b % v2 + c % v3 IN s))`; convex] THEN STRIP_TAC THEN \r
 422 REWRITE_TAC[SET3_SUBSET] THEN DISCH_TAC THEN \r
 423 REWRITE_TAC[REAL_ARITH`&0 <= u /\ &0 <= v /\ u + v = &1 <=>\r
 424   &0 <= u /\ &0 <= v / &2 /\ u + v/ &2 + v / &2 = &1`] THEN \r
 425 ONCE_REWRITE_TAC[MESON[REAL_ARITH` a = a / &2 + a / &2`]` u % x + v % y = \r
 426    u % x + ( v/ &2 + v/ &2 ) % y `] THEN REWRITE_TAC[ VECTOR_ADD_RDISTRIB] THEN \r
 427 ASM_MESON_TAC[]);;\r
 428 \r
 429 \r
 430 (* ============== *)\r
 431 \r
 432 \r
 433 let convex3_in_inters = prove (` ! v1 v2 v3. {t | ?a b c.\r
 434           &0 <= a /\\r
 435           &0 <= b /\\r
 436           &0 <= c /\\r
 437           a + b + c = &1 /\\r
 438           t = a % v1 + b % v2 + c % v3} SUBSET\r
 439  INTERS {t | convex t /\ {v1, v2, v3} SUBSET t} `, \r
 440 REPEAT GEN_TAC THEN \r
 441 MATCH_MP_TAC (SET_RULE ` ( ! x. x IN A ==> x IN B ) ==> A SUBSET B`) THEN \r
 442 REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[IN_INTERS] THEN \r
 443 REWRITE_TAC[MESON[] `( !x. (?a b c.\r
 444           &0 <= a /\\r
 445           &0 <= b /\\r
 446           &0 <= c /\\r
 447           a + b + c = &1 /\\r
 448           x = a % v1 + b % v2 + c % v3)\r
 449      ==> (!t. convex t /\ {v1, v2, v3} SUBSET t ==> x IN t))\r
 450   <=>( !x. (?a b c.\r
 451           &0 <= a /\\r
 452           &0 <= b /\\r
 453           &0 <= c /\\r
 454           a + b + c = &1 /\\r
 455           x = a % v1 + b % v2 + c % v3)\r
 456      ==> (!t. convex t /\ {v1, v2, v3} SUBSET t /\ (?a b c.\r
 457           &0 <= a /\\r
 458           &0 <= b /\\r
 459           &0 <= c /\\r
 460           a + b + c = &1 /\\r
 461           x = a % v1 + b % v2 + c % v3) ==> x IN t)) `] THEN \r
 462 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN FIRST_X_ASSUM MP_TAC THEN \r
 463 REWRITE_TAC[ IN_ELIM_THM ; TAUT ` a ==> b ==> c <=> a /\ b ==> c `] THEN \r
 464 MESON_TAC[minconvex3]);;\r
 465 \r
 466 \r
 467 (* =========== *)\r
 468 \r
 469 \r
 470 \r
 471 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 \r
 472 /\ t = a % v1 + b % v2 + c % v3}`, REPEAT GEN_TAC THEN\r
 473 REWRITE_TAC[conv; hull] THEN REPEAT GEN_TAC THEN \r
 474 REWRITE_TAC[ SET_RULE` a = b <=> a SUBSET b /\ b SUBSET a `] THEN\r
 475 REWRITE_TAC[conv_trg; hull] THEN \r
 476 MATCH_MP_TAC (MATCH_MP ( MESON[] `(! a b. P a b) ==> P a b` ) (MESON[INTERS_SUBSET ]` \r
 477   ! P t0 . ( P t0 /\ aa ) ==> INTERS {t | P t} SUBSET t0 /\ aa`)) THEN \r
 478  REWRITE_TAC[convex3] THEN REWRITE_TAC[ SET_RULE `{v1 , v2, v3} SUBSET a <=>\r
 479   v1 IN a /\ v2 IN a /\ v3 IN a`] THEN REWRITE_TAC [ v1v2v3_in_convex3] THEN \r
 480 REWRITE_TAC[ SET_RULE` v1 IN t /\ v2 IN t /\ v3 IN t <=> {v1, v2, v3} SUBSET t`] THEN \r
 481 REWRITE_TAC[convex3_in_inters]);;\r
 482 \r
 483 \r
 484 \r
 485 \r
 486 \r
 487 \r
 488 \r
 489 \r
 490 \r
 491 \r
 492 \r
 493 \r
 494 \r
 495 \r
 496 \r
 497 \r
 498 \r
 499 \r
 500 \r
 501 \r
 502 \r
 503 \r
 504 (* =========== begining lemma 8.2 ========== *)\r
 505 \r
 506 let near = new_definition ` near (v0:real^N) (r:real) s = { x | x IN s /\\r
 507   dist(x,v0) < r } `;;\r
 508 \r
 509 let near2t0 = new_definition ` near2t0 v0 s = { x | x IN s /\ dist(v0,x) < &2 * t0 }`;;\r
 510 \r
 511 let e_plane = new_definition ` e_plane (a:real^N) (b:real^N) x = ( ~( a=b) /\ dist(a,x) = dist(b,x))`;;\r
 512 \r
 513 let min_dist = new_definition ` min_dist (x:real^3) s = ((?u. u IN s /\\r
 514                   (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/\r
 515              (?u v.\r
 516                   u IN s /\\r
 517                   v IN s /\\r
 518                   ~(u = v) /\\r
 519                   dist (u,x) = dist (v,x) /\\r
 520                   (!w. w IN s ==> dist (u,x) <= dist (w,x)))) `;;\r
 521 \r
 522 \r
 523 let exists_min_dist = new_axiom ` ! (x :real^3) (s:real^3 -> bool).\r
 524   ~(s = {}) /\ packing s\r
 525          ==> min_dist x s`;;\r
 526 \r
 527 \r
 528 let tarski_FFSXOWD = new_axiom ` !v0 v1 v2 v3 s.\r
 529          packing s /\\r
 530          ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\\r
 531          dist (v1,v2) <= #2.51 /\\r
 532          dist (v2,v3) <= #2.51 /\\r
 533          dist (v3,v1) < sqrt (&8) /\\r
 534          {v1, v2, v3} SUBSET s /\\r
 535          ~(v0 IN {v1, v2, v3})\r
 536          ==> normball v0 #1.255 INTER conv {v1, v2, v3} = {} `;; \r
 537 \r
 538 \r
 539 (* ========== simplize.ml ============ *)\r
 540 \r
 541 let SET3_SUBSET = SET_RULE`! a b c. {a,b,c} SUBSET s <=> a IN s /\ b IN s /\ c IN s `;;\r
 542 \r
 543 \r
 544 let FINITE6 = MESON[ FINITE_RULES ] `! a b c d e f.\r
 545          FINITE {} /\\r
 546          FINITE {a} /\\r
 547          FINITE {a, b} /\\r
 548          FINITE {a, b, c} /\\r
 549          FINITE {a, b, c, d} /\\r
 550          FINITE {a, b, c, d, e} /\\r
 551          FINITE {a, b, c, d, e, f} `;; \r
 552 \r
 553 (* ========= new simplizing ========== *)\r
 554 \r
 555 let elimin = REWRITE_RULE[IN];;\r
 556 \r
 557 let CONV_EM = prove(`conv {} = {}:real^A->bool`,\r
 558   REWRITE_TAC[conv;sgn_ge;affsign;UNION_EMPTY;FUN_EQ_THM;elimin\r
 559 NOT_IN_EMPTY;lin_combo;SUM_CLAUSES]\r
 560   THEN REAL_ARITH_TAC);;\r
 561 \r
 562 let CONV_SING = prove(`!u. conv {u:real^A} = {u}`,\r
 563  REWRITE_TAC[conv;sgn_ge;affsign;FUN_EQ_THM;UNION_EMPTY;lin_combo;SUM_SING;VSUM_SING;\r
 564  elimin IN_SING] THEN REPEAT GEN_TAC THEN\r
 565  REWRITE_TAC[TAUT `(p <=> q) = ((p ==> q) /\ (q ==> p))`] THEN\r
 566  REPEAT STRIP_TAC THENL [ASM_MESON_TAC[VECTOR_MUL_LID];\r
 567  ASM_REWRITE_TAC[]] THEN EXISTS_TAC `\ (v:real^A). &1` THEN\r
 568  MESON_TAC[VECTOR_MUL_LID;REAL_ARITH `&0 <= &1`] );;\r
 569 \r
 570 \r
 571 let NOV9 = prove(`!x y z.(x = y /\ y = z\r
 572       ==> conv {y, z} =\r
 573           {w | ?a b c.\r
 574                    &0 <= a /\\r
 575                    &0 <= b /\\r
 576                    &0 <= c /\\r
 577                    a + b + c = &1 /\\r
 578                    w = a % y + b % y + c % z})`,\r
 579 SIMP_TAC[] THEN REWRITE_TAC[SET_RULE` {a,a} = {a}`] THEN \r
 580 REWRITE_TAC[ CONV_SING;  GSYM VECTOR_ADD_RDISTRIB] THEN \r
 581 REWRITE_TAC[ MESON[]` a + b + c = &1 /\ w = (a + b + c) % z <=>a + b + c = &1 /\\r
 582    w = &1 % z `; VECTOR_MUL_LID] THEN REWRITE_TAC[ FUN_EQ_THM] THEN \r
 583 REWRITE_TAC[ SET_RULE ` {a} x <=> a = x `; IN_ELIM_THM] THEN \r
 584 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN \r
 585 NGOAC THEN REWRITE_TAC[ LEFT_EXISTS_AND_THM] THEN \r
 586 MATCH_MP_TAC (MESON[] ` a ==> ( z = x <=> a /\ x = z )`) THEN \r
 587 REPLICATE_TAC 2 (EXISTS_TAC `&0`) THEN EXISTS_TAC ` &1` THEN REAL_ARITH_TAC);;\r
 588 \r
 589 \r
 590 let IN_ACT_SING = SET_RULE `! a x. ({a} x <=> a = x ) /\ ( x IN {a} <=> x = a) /\ {a} a`;;\r
 591 \r
 592 \r
 593 let NOV10 = prove(` ! x y. (x = y\r
 594       ==> (!x. y = x <=>\r
 595                (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x = a % y + b % y))) `,\r
 596 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN \r
 597 REWRITE_TAC[ MESON[VECTOR_MUL_LID]` a + b = &1 /\ x = (a + b) % y <=> a + b = &1 /\ \r
 598 x = y`]THEN REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN NGOAC THEN \r
 599 REWRITE_TAC[LEFT_EXISTS_AND_THM] THEN MATCH_MP_TAC (MESON[]` a ==> ( x = y <=> a /\\r
 600  y = x )`)THEN EXISTS_TAC `&0` THEN EXISTS_TAC ` &1` THEN REAL_ARITH_TAC);;\r
 601 \r
 602 \r
 603 \r
 604 \r
 605 \r
 606 let IN_SET2 = SET_RULE `!a b x.\r
 607          (x IN {a, b} <=> x = a \/ x = b) /\ ({a, b} x <=> x = a \/ x = b)`;;\r
 608 \r
 609 \r
 610 let VSUM_DIS2 = prove(` ! x y f. ~(x=y) ==>  vsum {x,y} f = f x + f y`, REWRITE_TAC[\r
 611    SET_RULE ` ~( x = y)\r
 612  <=> ~(x IN {y})`] THEN MESON_TAC[ FINITE_RULES; VSUM_CLAUSES; VSUM_SING]);;\r
 613 \r
 614 let SUM_DIS2 = prove(`! x y f. ~(x=y) ==> sum {x,y} f = f x + f y `,REWRITE_TAC[\r
 615    SET_RULE ` ~( x = y)\r
 616  <=> ~(x IN {y})`] THEN MESON_TAC[ FINITE_RULES; SUM_CLAUSES; SUM_SING]);;\r
 617  \r
 618 \r
 619 let TRUONG_LEMMA = prove\r
 620   (  `!x y x':real^N.\r
 621        (?f. x' = f x % x + f y % y /\ (&0 <= f x /\ &0 <= f y) /\\r
 622             f x + f y = &1) <=>\r
 623        (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x' = a % x + b % y)`   ,\r
 624    REPEAT GEN_TAC THEN EQ_TAC \r
 625 THENL [MESON_TAC[]; STRIP_TAC] THEN\r
 626    ASM_CASES_TAC `y:real^N = x` THENL\r
 627     [EXISTS_TAC `\x:real^N. &1 / &2`;\r
 628      EXISTS_TAC `\u:real^N. if u = x then (a:real) else b`] THEN\r
 629    ASM_REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN\r
 630    CONV_TAC REAL_RAT_REDUCE_CONV);;\r
 631 \r
 632 \r
 633 let NOV11 = prove(`! z. {z} =\r
 634  {w | ?a b c.\r
 635           &0 <= a /\\r
 636           &0 <= b /\\r
 637           &0 <= c /\\r
 638           a + b + c = &1 /\\r
 639           w = a % z + b % z + c % z}`,\r
 640 REWRITE_TAC[ FUN_EQ_THM; IN_ACT_SING; IN_ELIM_THM] THEN \r
 641 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN \r
 642 REWRITE_TAC[ MESON[VECTOR_MUL_LID]`a + b + c = &1 /\\r
 643           x = (a + b + c) % z <=> a + b + c = &1 /\ x = z`] THEN \r
 644 NGOAC THEN MATCH_MP_TAC (MESON[]` (? a b c. P a b c) ==> (! z x. z = x <=>\r
 645   (? a b c. P a b c /\ x = z))`) THEN \r
 646 REPLICATE_TAC 2 (EXISTS_TAC `&0`) THEN \r
 647 EXISTS_TAC `&1` THEN REAL_ARITH_TAC);;\r
 648 \r
 649 \r
 650 \r
 651 let CONV2_CONV3 = prove(` !x' y z.\r
 652          (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x' = a % y + b % z)\r
 653          ==> (?a b c.\r
 654                   &0 <= a /\\r
 655                   &0 <= b /\\r
 656                   &0 <= c /\\r
 657                   a + b + c = &1 /\\r
 658                   x' = a % y + b % y + c % z)`,\r
 659 REPEAT GEN_TAC THEN REWRITE_TAC[ VECTOR_ARITH` a % y + b % y + c % z = (a+b) %y + c%z`] THEN STRIP_TAC THEN \r
 660 REPLICATE_TAC 2 (EXISTS_TAC `a/ &2`) THEN \r
 661 EXISTS_TAC `b:real` THEN \r
 662 REWRITE_TAC[ REAL_ARITH` a / &2 + a / &2 = a /\ a / &2 + a / &2 + b = a + b `] THEN \r
 663 ASM_SIMP_TAC[] THEN \r
 664 ASM_REAL_ARITH_TAC);;\r
 665 \r
 666 \r
 667 let CONV3_CONV2 = prove(`! x' y z. (?a b c.\r
 668       &0 <= a /\\r
 669       &0 <= b /\\r
 670       &0 <= c /\\r
 671       a + b + c = &1 /\\r
 672       x' = a % y + b % y + c % z)\r
 673  ==> (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x' = a % y + b % z)`,\r
 674 REPEAT GEN_TAC THEN STRIP_TAC THEN EXISTS_TAC ` a + b:real` THEN \r
 675 EXISTS_TAC `c:real` THEN \r
 676 REWRITE_TAC[VECTOR_ADD_RDISTRIB] THEN \r
 677 REWRITE_TAC[VECTOR_ARITH` (a % y + b % y) + c % z = a % y + b % y + c % z `] THEN \r
 678 ASM_SIMP_TAC[REAL_ARITH ` a + b + c = (a + b) + c`] THEN \r
 679 ASM_REAL_ARITH_TAC);;\r
 680 \r
 681 \r
 682 let CONV_SET2 = prove(` ! x y:real^A. conv {x,y} = {w | ? a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\\r
 683   w = a%x + b%y}`,\r
 684 ONCE_REWRITE_TAC[ MESON[] ` (! a b. P a b ) <=> ( ! a b. a = b \/ ~( a= b)\r
 685   ==> P a b )`] THEN \r
 686 REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a==> c) /\ ( b==> c)`] THEN \r
 687 SIMP_TAC[] THEN \r
 688 REWRITE_TAC[ SET_RULE ` {a,a} = {a}`; CONV_SING; FUN_EQ_THM; IN_ELIM_THM] THEN \r
 689 REWRITE_TAC[ IN_ACT_SING] THEN \r
 690 REWRITE_TAC[NOV10] THEN \r
 691 REWRITE_TAC[conv; sgn_ge; affsign; lin_combo] THEN \r
 692 REWRITE_TAC[UNION_EMPTY; IN_SET2] THEN \r
 693 ONCE_REWRITE_TAC[ MESON[]`  ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>\r
 694   ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`] THEN \r
 695 REWRITE_TAC[ MESON[VSUM_DIS2; SUM_DIS2]` ~(x = y) /\\r
 696                     x' = vsum {x, y} ff /\ l /\ sum {x, y} f = &1 <=> ~(x = y) /\\r
 697                     x' = ff x + ff y /\ l /\ f x + f y = &1 `] THEN \r
 698 REWRITE_TAC[ MESON[]` (!w. w = x \/ w = y ==> &0 <= f w) <=> &0 <= f x /\ &0 <= f y`] THEN \r
 699 ONCE_REWRITE_TAC[ GSYM (MESON[]`  ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>\r
 700   ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`)] THEN \r
 701 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN \r
 702 REWRITE_TAC[ TRUONG_LEMMA]);;\r
 703 \r
 704 \r
 705 let CONV3_A_EQ = prove(`! x y z. (x = y \/ y = z \/ z = x\r
 706   ==> conv {x, y, z} =\r
 707       {w | ?a b c.\r
 708                &0 <= a /\\r
 709                &0 <= b /\\r
 710                &0 <= c /\\r
 711                a + b + c = &1 /\\r
 712                w = a % x + b % y + c % z})`,\r
 713 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)\r
 714   ==> (! a b c. a = b \/ b = c \/ c = a ==> P a b c )`) THEN \r
 715 SIMP_TAC[ MESON[ SET_RULE ` {a,b,c} = {b,a,c} `]`conv {x, y, z} = conv {y,x,z}`] THEN  \r
 716 SIMP_TAC[ MESON[ REAL_ARITH` a + b + c = b + a + c`; VECTOR_ARITH` a % x + b % y + c % z\r
 717   = b % y + a % x + c % z `]` (?a b c.\r
 718                &0 <= a /\\r
 719                &0 <= b /\\r
 720                &0 <= c /\\r
 721                a + b + c = &1 /\\r
 722                w = a % x + b % y + c % z)\r
 723   <=> (?a b c.\r
 724                &0 <= a /\\r
 725                &0 <= b /\\r
 726                &0 <= c /\\r
 727                a + b + c = &1 /\\r
 728                w = a % y + b % x + c % z)`] THEN \r
 729 MATCH_MP_TAC (MESON[]` (! a b c. P a b c <=> P c b a ) /\ (! a b c. a = b ==> P a b c) \r
 730   ==> (! a b c. a = b \/ b = c ==> P a b c)`) THEN \r
 731 SIMP_TAC[ MESON[SET_RULE `{a,b,c} ={c,b,a} `]` conv {a,b,c} = conv {c,b,a}`] THEN \r
 732 SIMP_TAC[ MESON[REAL_ARITH` a + b + c = c + b + a`; VECTOR_ARITH` a % x + b % y + c % z\r
 733   = c % z + b % y + a % x `]`(?a b c.\r
 734                &0 <= a /\\r
 735                &0 <= b /\\r
 736                &0 <= c /\\r
 737                a + b + c = &1 /\\r
 738                w = a % x + b % y + c % z) <=> \r
 739   (?a b c.\r
 740                &0 <= a /\\r
 741                &0 <= b /\\r
 742                &0 <= c /\\r
 743                a + b + c = &1 /\\r
 744                w = a % z + b % y + c % x)`] THEN \r
 745 REWRITE_TAC[ SET_RULE`{a,a,b} = {a,b}`] THEN \r
 746 ONCE_REWRITE_TAC[ MESON[]` x = y ==> conv {y,z} = s <=> x = y /\( y = z \/\r
 747   ~(y=z))==> conv {y,z} = s `] THEN \r
 748 KHANANG THEN REWRITE_TAC[ MESON[]` a \/ b ==> c <=> (a==> c) /\ (b==> c)`] THEN \r
 749 SIMP_TAC[] THEN REWRITE_TAC[SET_RULE`{a,a} ={a}`; CONV_SING] THEN \r
 750 SIMP_TAC[NOV11] THEN REWRITE_TAC [ GSYM NOV11] THEN \r
 751 REWRITE_TAC[CONV_SET2] THEN \r
 752 REPEAT GEN_TAC THEN STRIP_TAC THEN \r
 753  REWRITE_TAC[ FUN_EQ_THM; IN_ELIM_THM] THEN \r
 754 GEN_TAC THEN REWRITE_TAC[MESON[]` (a <=> b ) <=> ( a ==> b) /\ (b==> a)`] THEN \r
 755 REWRITE_TAC[CONV2_CONV3; CONV3_CONV2]);;\r
 756 \r
 757 \r
 758 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 `,\r
 759 NHANH (SET_RULE` ~(x = y \/ y = z \/ z = x) ==> ({x} INTER {y,z} = {}) `) THEN \r
 760 REWRITE_TAC[ GSYM DISJOINT; SET_RULE `{x, y, z} = {x} UNION {y,z}` ] THEN \r
 761 REWRITE_TAC[MESON[FINITE6; VSUM_UNION]` aa /\ DISJOINT {x} {y, z}\r
 762      ==> vsum ({x} UNION {y, z}) f = ab <=>  aa /\ DISJOINT {x} {y, z} ==>\r
 763   vsum {x} f + vsum {y,z} f = ab `] THEN \r
 764  MESON_TAC[VSUM_SING; VSUM_DIS2]);;\r
 765 \r
 766 \r
 767 let SUM_DIS3 = prove(` ! x y z f. ~(x = y \/ y = z \/ z = x) ==> sum {x, y, z} f = \r
 768   f x + f y + f z `,\r
 769 NHANH (SET_RULE` ~(x = y \/ y = z \/ z = x) ==> ({x} INTER {y,z} = {}) `) THEN \r
 770 REWRITE_TAC[ GSYM DISJOINT; SET_RULE `{x, y, z} = {x} UNION {y,z}` ] THEN \r
 771 REWRITE_TAC[MESON[FINITE6; SUM_UNION]` aa /\ DISJOINT {x} {y, z}\r
 772      ==> sum ({x} UNION {y, z}) f = ab <=>  aa /\ DISJOINT {x} {y, z} ==>\r
 773   sum {x} f + sum {y,z} f = ab `] THEN MESON_TAC[ SUM_SING; SUM_DIS2]);;\r
 774 \r
 775 \r
 776 \r
 777 let EQ_EXPAND = MESON[] `(a <=> b) <=> ( a ==> b ) /\ ( b ==> a )` ;;\r
 778 \r
 779 \r
 780 \r
 781 let CONV_SET3 = prove(`! x y z:real^A. conv {x,y,z} = { w | ? a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\\r
 782 a + b + c = &1 /\ w = a % x + b % y + c % z } `,\r
 783 REPEAT GEN_TAC THEN \r
 784 ONCE_REWRITE_TAC[ MESON[]` conv {x,y,z} = s <=> (x = y \/ y= z \/ z = x ) \/\r
 785   ~(x = y \/ y= z \/ z = x ) ==> conv {x,y,z} = s`] THEN \r
 786 ONCE_REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a ==> c ) /\(b==>c)`] THEN \r
 787 REWRITE_TAC[CONV3_A_EQ] THEN    \r
 788 REWRITE_TAC[conv; FUN_EQ_THM; affsign; IN_ELIM_THM; sgn_ge; lin_combo; UNION_EMPTY] THEN \r
 789 DISCH_TAC THEN GEN_TAC THEN FIRST_X_ASSUM MP_TAC THEN \r
 790 ONCE_REWRITE_TAC[ MESON[]` a ==> ((?f. P f ) <=> la ) <=> \r
 791   a ==> ((?f. a /\ P f ) <=> la ) `] THEN REWRITE_TAC[MESON[VSUM_DIS3]` ~(x = y \/ \r
 792 y = z \/ z = x) /\ x' = vsum {x, y, z} f /\ l <=>   ~(x = y \/ y = z \/ z = x) /\\r
 793 x' = f x + f y + f z /\ l `] THEN \r
 794 REWRITE_TAC[ MESON[SUM_DIS3]` ~(x = y \/ y = z \/ z = x) /\ P /\ Q /\ sum {x,y,z} f = &1 \r
 795   <=> ~(x = y \/ y = z \/ z = x) /\ P /\ Q /\ ( f x + f y + f z ) = &1`] THEN \r
 796 REWRITE_TAC[SET_RULE ` (!w. {x, y, z} w ==> &0 <= f w) <=> &0 <= f x /\ \r
 797    &0 <= f y /\ &0 <= f z `] THEN \r
 798 ONCE_REWRITE_TAC[ GSYM (MESON[]` a ==> ((?f. P f ) <=> la ) <=> \r
 799   a ==> ((?f. a /\ P f ) <=> la ) `)] THEN DISCH_TAC THEN \r
 800 REWRITE_TAC[ EQ_EXPAND] THEN \r
 801 REWRITE_TAC[ MESON[]` (?f. x' = f x % x + f y % y + f z % z /\\r
 802        (&0 <= f x /\ &0 <= f y /\ &0 <= f z) /\\r
 803        f x + f y + f z = &1)\r
 804   ==> (?a b c.\r
 805            &0 <= a /\\r
 806            &0 <= b /\\r
 807            &0 <= c /\\r
 808            a + b + c = &1 /\\r
 809            x' = a % x + b % y + c % z)`] THEN STRIP_TAC THEN \r
 810 EXISTS_TAC ` (\d. if d = (x:real^A) then (a:real) else ( if d = (y:real^A) then \r
 811   (b:real)  else c ))` THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN \r
 812 REWRITE_TAC[ MESON[]`~( a \/ b ) <=> ~a /\ ~b `] THEN SIMP_TAC[]);;\r
 813 \r
 814 (* ========== *)\r
 815 let CONV3_EQ = prove(` ! x y z. conv_trg {x,y,z} = conv {x,y,z} `, REWRITE_TAC[simpl_conv3;\r
 816 CONV_SET3]);;\r
 817 (* ========= *)\r
 818 \r
 819 let CONV_BAR_EQ = prove(`! bar s. bar IN barrier s ==> conv bar = conv_trg bar `,\r
 820 REWRITE_TAC[barrier; IN_ELIM_THM] THEN MESON_TAC[CONV_SET3; simpl_conv3]);;\r
 821 \r
 822 let OBSTRUCT_EQ = prove(`!x y s. obstruct x y s <=> obstructed x y s`,\r
 823 REWRITE_TAC[obstruct; obstructed] THEN REWRITE_TAC[obstruct; obstructed; conv0_2] THEN \r
 824 MESON_TAC[CONV_BAR_EQ]);;\r
 825 \r
 826 (* === repare VC === *)\r
 827 \r
 828 (* ==== CARD ASSERTION ==== *)\r
 829 \r
 830 \r
 831 let CARD_CLAUSES_IMP = prove(` !a s.\r
 832      FINITE s\r
 833      ==> CARD (a INSERT s) <= SUC (CARD s) /\\r
 834          (a IN s ==> CARD (a INSERT s) = CARD s) /\\r
 835          (~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s))`,\r
 836 ONCE_REWRITE_TAC[ MESON[] ` ( a ==> b /\ c ) <=> ( a ==> b ) /\ ( a ==> c )`] THEN \r
 837 REWRITE_TAC[ MESON[CARD_CLAUSES] ` FINITE s ==> ( a IN s ==> CARD (a INSERT s) = CARD s ) /\\r
 838   (~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s))`] THEN \r
 839 MESON_TAC[ CARD_CLAUSES; ARITH_RULE ` a <= SUC a /\ a <= a `]);;\r
 840 \r
 841 (* =================== *)\r
 842 \r
 843 let CARD_SING = prove( `! a: A. CARD {a} = 1`, REWRITE_TAC[ MESON[ FINITE6; CARD_EQ_NSUM ] \r
 844 ` CARD {a} = nsum {a} (\x. 1)`] THEN REWRITE_TAC[ NSUM_SING ]);;\r
 845 \r
 846 let CARD_SET2 = prove( ` ! a b . ( CARD {a, b} = 2 <=> ~(a = b)) /\ (CARD {a, b} = 1 <=> a = b ) `,\r
 847 REWRITE_TAC[ MESON[ FINITE6; CARD_CLAUSES ] ` CARD {a,b} = (if a IN {b} then CARD {b} else SUC (CARD {b}))`]\r
 848 THEN REWRITE_TAC[ MESON[ FINITE6; CARD_CLAUSES ] ` CARD {a} = (if a IN {} then CARD {} else SUC (CARD {}))`]\r
 849 THEN REWRITE_TAC[ NOT_IN_EMPTY; IN_SING; CARD_CLAUSES; ADD1] THEN \r
 850 MESON_TAC[ ARITH_RULE `  ~( 0+ 1 = 2 ) /\ (0 + 1) + 1 = 2 /\ ~((0 + 1) + 1 = 1 ) /\ 0 + 1 = 1  `]);;\r
 851 \r
 852 (* ============== *)\r
 853 \r
 854 let CARD_EQUATION = prove(`!(s: A -> bool) t.\r
 855      FINITE s /\ FINITE t\r
 856      ==> CARD (s UNION t) + CARD (s INTER t) = CARD s + CARD t `, \r
 857 NHANH (MESON[FINITE_INTER; FINITE_UNION] `FINITE s /\ FINITE t ==> FINITE ( s UNION t ) /\\r
 858     FINITE ( s INTER t ) `) THEN MESON_TAC[ CARD_EQ_NSUM; NSUM_INCL_EXCL]);;\r
 859 \r
 860 \r
 861 let CARD_DISJOINT = prove(` ! s: A -> bool t. FINITE s /\ FINITE t ==> \r
 862        ( CARD s + CARD t = CARD ( s UNION t ) <=> s INTER t ={} )`,\r
 863 MESON_TAC[CARD_EQUATION; ARITH_RULE ` a + b = a <=> b = 0 `; FINITE_INTER; CARD_EQ_0]);;\r
 864 \r
 865 \r
 866 let CARD2 = prove(` ! a b . CARD {a,b} <= 2 /\ ( CARD {a,b} = 2 <=> ~(a = b ) )`,\r
 867 REWRITE_TAC[ MESON[ CARD_SET2] ` CARD {a, b} = 2 <=> ~(a = b)`] THEN MP_TAC CARD_SET2 THEN \r
 868 ONCE_REWRITE_TAC[ MESON[] ` CARD {a, b} <= 2 <=>\r
 869   ( a = b \/ ~( a = b)) /\ CARD {a, b} <= 2`] THEN KHANANG THEN \r
 870 REWRITE_TAC[ MESON[CARD_SET2] `a = b /\ CARD {a, b} <= 2 \/ ~(a = b) /\ CARD {a, b} <= 2 \r
 871   <=> a = b /\ 1 <= 2 \/ ~(a = b) /\ 2 <= 2`] THEN \r
 872 MESON_TAC[ARITH_RULE ` 1 <= 2 /\ 2 <= 2 `]);;\r
 873 \r
 874 \r
 875 let CARD3 = prove(`! a b c . CARD {a,b,c} <= 3 /\ \r
 876   ( CARD {a,b,c} = 3 <=> ~( a =b \/ b= c\/ c= a ))`, \r
 877 REWRITE_TAC[ SET_RULE ` {a,b,c} = {a} UNION {b,c}`] THEN \r
 878 REWRITE_TAC[ ARITH_RULE ` CARD ({a} UNION {b, c}) <= 3 <=>\r
 879   CARD ({a} UNION {b, c}) + CARD ({a} INTER {b, c}) <= 3 + CARD ({a} INTER {b, c})`] THEN \r
 880 REWRITE_TAC[ ARITH_RULE ` CARD ({a} UNION {b, c}) = 3 <=>\r
 881   CARD ({a} UNION {b, c}) + CARD ({a} INTER {b, c}) = 3 + CARD ({a} INTER {b, c})`] THEN \r
 882 REWRITE_TAC[ MESON[ FINITE_RULES; CARD_EQUATION] ` CARD ({a} UNION {b, c}) + CARD ({a} INTER {b, c})\r
 883   = CARD {a} + CARD {b,c} `] THEN REWRITE_TAC[ CARD_SING] THEN \r
 884 REWRITE_TAC[ ARITH_RULE `! a b. (1 + a <= 3 + b <=> a <= 2 + b ) /\\r
 885   (1 + a = 3 + b <=> a = 2 + b )`] THEN \r
 886 REWRITE_TAC[ MESON[CARD2; ARITH_RULE ` a <= b ==> a <= b + c: num`] ` CARD {b, c} <=   2 + CARD ({a} INTER {b, c})`] THEN \r
 887 ONCE_REWRITE_TAC[ MESON[CARD2]` CARD {b, c} = P b c <=> CARD {b, c} <= 2 /\   CARD {b, c} = P b c`] THEN \r
 888 REWRITE_TAC[ ARITH_RULE ` a <= 2 /\ a = 2 + b <=> a = 2 /\ b = 0`] THEN \r
 889 REWRITE_TAC[ MESON[FINITE_RULES; CARD2; FINITE_INTER; CARD_EQ_0] ` CARD {b, c} = 2 /\ CARD ({a} INTER {b, c}) = 0 \r
 890   <=> ~(b=c) /\ {a} INTER {b, c} = {}`] THEN SET_TAC[]);;\r
 891 \r
 892 (* ========= *)\r
 893 \r
 894 \r
 895 let CARD4 = prove(`!a b c d.\r
 896      CARD {a, b, c, d} <= 4 /\\r
 897      (CARD {a, b, c, d} = 4 <=>\r
 898       ~(a IN {b, c, d}) /\ ~(b = c \/ c = d \/ d = b))`,\r
 899 NHANH (MESON[FINITE6; CARD_CLAUSES_IMP]` CARD {a, b, c, d} <= 4 ==> CARD {a, b, c, d} \r
 900    <= SUC (CARD {b,c,d})`) THEN \r
 901 NHANH ( MESON[CARD3] ` aa <= SUC (CARD {b, c, d}) ==> CARD {b,c,d} <= 3 `) THEN \r
 902 REWRITE_TAC[ ARITH_RULE ` CARD {a, b, c, d} <= 4 /\\r
 903      CARD {a, b, c, d} <= SUC (CARD {b, c, d}) /\\r
 904      CARD {b, c, d} <= 3 <=>\r
 905      CARD {a, b, c, d} <= SUC (CARD {b, c, d}) /\ CARD {b, c, d} <= 3`] THEN \r
 906 SIMP_TAC[MESON[FINITE_RULES; CARD_CLAUSES_IMP] ` CARD {a, b, c, d} <= SUC \r
 907         (CARD {b, c, d})`; CARD3; CARD_CLAUSES_IMP] THEN \r
 908 REWRITE_TAC[ ARITH_RULE ` CARD {a, b, c, d} = 4 <=> CARD {a, b, c, d} + CARD ( {a} \r
 909    INTER {b,c,d} ) = 4 + CARD ({a} INTER {b,c,d})`] THEN \r
 910 REWRITE_TAC[ SET_RULE ` {a,b,c,d} = {a} UNION {b,c,d} ` ] THEN \r
 911 REWRITE_TAC[ MESON[FINITE_RULES; CARD_EQUATION; CARD_SING] ` CARD ({a} UNION {b, c, d}) + CARD ({a} INTER {b, c, d})\r
 912   = 1 + CARD {b,c,d} `] THEN \r
 913 NHANH (MESON[CARD3] ` 1 + CARD {b, c, d} = aa ==> CARD {b,c,d} <= 3 `) THEN \r
 914 REWRITE_TAC[ ARITH_RULE `1 + CARD {b, c, d} = 4 + CARD ({a} INTER {b, c, d}) /\\r
 915      CARD {b, c, d} <= 3 <=>\r
 916      CARD {b, c, d} = 3 /\ CARD ({a} INTER {b, c, d}) = 0`] THEN  \r
 917 REWRITE_TAC[ CARD3] THEN \r
 918 MESON_TAC[ FINITE_RULES; FINITE_INTER; CARD_EQ_0; SET_RULE ` \r
 919   {a} INTER {b, c, d} = {} <=> ~(a IN {b, c, d})` ]);;\r
 920 \r
 921 \r
 922 let CARD5 = prove(` ! a b c d e. CARD {a,b,c,d,e} <= 5 /\\r
 923   ( CARD {a,b,c,d,e} = 5 <=> ~( a IN {b,c,d,e}) /\ \r
 924                             ~(b IN {c, d, e}) /\ ~(c = d \/ d = e \/ e = c))`,\r
 925 ONCE_REWRITE_TAC[ MESON[ FINITE_RULES; CARD_CLAUSES_IMP] ` CARD {a, b, c, d, e} <= 5 <=>\r
 926   CARD {a, b, c, d, e} <= SUC ( CARD {b,c,d,e} ) ==> CARD {a, b, c, d, e} <= 5`] THEN \r
 927 ONCE_REWRITE_TAC[ MESON[CARD4] ` aa ==> CARD {a, b, c, d, e} <= 5 <=>\r
 928   aa /\ CARD {b,c,d,e} <= 4 ==> CARD {a, b, c, d, e} <= 5`] THEN \r
 929 REWRITE_TAC[ ARITH_RULE ` a <= SUC b /\ b <= 4 ==> a <= 5 `] THEN \r
 930 REWRITE_TAC[ ARITH_RULE ` CARD {a, b, c, d, e} = 5 <=>\r
 931   CARD {a, b, c, d, e} + CARD ({a} INTER {b,c,d,e} ) = 5 + CARD ({a} INTER {b,c,d,e} )`] THEN \r
 932 REWRITE_TAC[ SET_RULE ` {a,b,c,d,e} = {a} UNION {b,c,d,e} `] THEN \r
 933 REWRITE_TAC[ MESON[FINITE_RULES; CARD_EQUATION; CARD_SING ]` CARD ({a} UNION {b, c, d, e}) + \r
 934   CARD ({a} INTER {b, c, d, e})  = 1 + CARD {b,c,d,e} `] THEN \r
 935 ONCE_REWRITE_TAC[ MESON[ CARD4] ` 1 + CARD {b, c, d, e} = aa <=> CARD {b,c,d,e} <= 4 /\ \r
 936      1 + CARD {b, c, d, e} = aa `] THEN \r
 937 REWRITE_TAC[ ARITH_RULE ` a <= 4 /\ 1 + a = 5 + b <=> a = 4 /\ b = 0`] THEN \r
 938 REWRITE_TAC[ CARD4; MESON[FINITE_RULES; FINITE_INTER; CARD_EQ_0] `\r
 939   CARD ({a} INTER {b, c, d, e}) = 0 <=> {a} INTER {b, c, d, e} ={} `] THEN SET_TAC[]);;\r
 940 (* ============ *)\r
 941 \r
 942 let set_3elements = prove(`(?a b c. ~(a = b \/ b = c \/ c = a) /\ {a, b, c} = {v1, v2, v3}) <=>\r
 943  ~(v1 = v2 \/ v2 = v3 \/ v3 = v1)`, REWRITE_TAC[GSYM CARD3] THEN \r
 944 MESON_TAC[]);;\r
 945 \r
 946 \r
 947 let db_t0 = prove(`&2 * t0 = &2 * #1.255 /\ &2 * t0 = #2.51 /\ &2 * #1.255 = #2.51`,\r
 948   REWRITE_TAC[t0] THEN REAL_ARITH_TAC);;\r
 949 \r
 950 \r
 951 let without_lost = MESON[] ` ! P x. (!a b. P a b <=> P b a) /\ (?a b. P a b /\ x = a)\r
 952      ==> (?a b. P a b /\ (x = a \/ x = b))`;;\r
 953 \r
 954 let condi_of_wlofg = MESON[]` (!a b. P a b <=> P b a)\r
 955      ==> ((?a b. P a b /\ (x = a \/ x = b)) <=> (?a b. P a b /\ x = a))`;;\r
 956 \r
 957 \r
 958 (* ============ *)\r
 959  let CARD_SET_OF_LIST_LE = prove\r
 960   (`!l. CARD(set_of_list l) <= LENGTH l`,\r
 961    LIST_INDUCT_TAC THEN\r
 962    SIMP_TAC[LENGTH; set_of_list; CARD_CLAUSES; FINITE_SET_OF_LIST] THEN\r
 963    ASM_ARITH_TAC);;\r
 964 \r
 965  let HAS_SIZE_SET_OF_LIST = prove\r
 966   (`!l. (set_of_list l) HAS_SIZE (LENGTH l) <=> PAIRWISE (\x y. ~(x = y)) l`,\r
 967    REWRITE_TAC[HAS_SIZE; FINITE_SET_OF_LIST] THEN LIST_INDUCT_TAC THEN\r
 968    ASM_SIMP_TAC[CARD_CLAUSES; LENGTH; set_of_list; PAIRWISE; ALL;\r
 969                 FINITE_SET_OF_LIST; GSYM ALL_MEM; IN_SET_OF_LIST] THEN\r
 970    COND_CASES_TAC THEN ASM_REWRITE_TAC[SUC_INJ] THEN\r
 971    ASM_MESON_TAC[CARD_SET_OF_LIST_LE; ARITH_RULE `~(SUC n <= n)`]);;\r
 972 \r
 973 (* ====================In your theorem we want the n=4 case, so we instantiate it:\r
 974 =========================== *)\r
 975 \r
 976  let HAS_SIZE_SET_OF_LIST_4 = prove\r
 977   (`!a b c d:A. {a,b,c,d} HAS_SIZE 4 <=> PAIRWISE (\x y. ~(x = y)) [a;b;c;d]`,\r
 978    REPEAT GEN_TAC THEN MP_TAC(ISPEC `[a;b;c;d]:A list`HAS_SIZE_SET_OF_LIST) THEN\r
 979    REWRITE_TAC[LENGTH; set_of_list; ARITH])  ;;\r
 980 \r
 981 (* ============================================================================\r
 982  Then finally, using this and a bit of straightforward rearrangement,\r
 983 we can collapse the desired theorem to a lemma that MESON can prove\r
 984 automatically: \r
 985 ===============================================================================*)\r
 986 \r
 987  let SET_OF_4 = prove\r
 988   (`! a b c d. ( ? v1 v2 v3 v4:A. ~( v1 = v2 \/ v3 = v4 ) /\\r
 989                                 {v1, v2 } INTER {v3, v4 } = {} /\\r
 990                                 { a , b , c , d } = { v1 , v2, v3 ,v4}) <=>\r
 991     ~ ( a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d )`,\r
 992    REPEAT GEN_TAC THEN\r
 993    REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; INTER_EMPTY; SET_RULE\r
 994     `(a INSERT s) INTER t = {} <=> ~(a IN t) /\ s INTER t = {}`] THEN\r
 995    MP_TAC(MESON[]\r
 996     `(?v1 v2 v3 v4:A. {a,b,c,d} = {v1,v2,v3,v4} /\ {v1,v2,v3,v4} HAS_SIZE 4) <=>\r
 997      {a,b,c,d} HAS_SIZE 4`) THEN\r
 998    REWRITE_TAC[HAS_SIZE_SET_OF_LIST_4; PAIRWISE; ALL; DE_MORGAN_THM; CONJ_ACI]);;\r
 999 \r
1000 \r
1001 let def_simplex = prove(`! s a b c d. simplex {a, b, c, d} s <=>\r
1002   packing s /\\r
1003          {a, b, c, d} SUBSET s /\\r
1004   ~ ( a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d ) `, REWRITE_TAC[ simplex]\r
1005 THEN REPEAT GEN_TAC THEN MATCH_MP_TAC (MESON[] ` ( x <=> y ) ==> ( a /\ b /\ x <=> \r
1006 a /\ b /\ y ) `) THEN ONCE_REWRITE_TAC[MESON[]` {v1, v2, v3, v4} = {a, b, c, d} <=>\r
1007  {a, b, c, d}  = {v1, v2, v3, v4} ` ] THEN REWRITE_TAC[ SET_OF_4]);;\r
1008 \r
1009 \r
1010 let strict_qua2_imply_strict_qua = prove(`! q d s. strict_qua2 q d s ==> strict_qua q s `,\r
1011 REWRITE_TAC[ strict_qua2; strict_qua] THEN NHANH (SET_RULE` d = {x, y} ==> x IN d /\\r
1012  y IN d `) THEN MESON_TAC[ SET_RULE ` x IN d /\ d SUBSET s ==> x IN s `]);;\r
1013 \r
1014 (* ========== have added to database more =====================*)\r
1015 \r
1016 \r
1017 let strict_qua2_interior_pos = prove( `!s v v1 v2 v3 v4.\r
1018      interior_pos v v1 v3 v2 v4 s\r
1019      ==> strict_qua2 {v, v1, v3, v2} {v1, v3} s /\\r
1020          strict_qua2 {v, v1, v3, v4} {v1, v3} s /\\r
1021          strict_qua2 {v, v2, v4, v1} {v2, v4} s /\\r
1022          strict_qua2 {v, v2, v4, v3} {v2, v4} s`,\r
1023 REWRITE_TAC[ interior_pos; conflicting_dia; adjacent_pai] THEN MESON_TAC[]);;\r
1024 \r
1025 \r
1026 let RELATE_Q_SYS = prove (` ! q s. (?v v1 v3 v2 v4.\r
1027       (q = {v, v1, v2, v3} \/ q = {v, v1, v3, v4}) /\\r
1028       interior_pos v v1 v3 v2 v4 s /\\r
1029       anchor_points v1 v3 s = {v, v2, v4} /\\r
1030       anchor_points v2 v4 s = {v, v1, v3})\r
1031  ==> strict_qua q s`,\r
1032 NHANH (MATCH_MP (MESON[]`( ! a b c d e f. P a b c d e f ) \r
1033    ==> P a b c d e f`) strict_qua2_interior_pos) THEN \r
1034 NHANH (MATCH_MP (MESON[] `( ! x y z. P x y z ) ==> P x y z `) \r
1035   strict_qua2_imply_strict_qua) THEN \r
1036 MESON_TAC[ SET_RULE ` {v, v1, v2 , v3 } = {v, v1, v3, v2}`]);;\r
1037 \r
1038 (* ======= *)\r
1039 \r
1040 let strict_qua_in_oct = prove (`! (q:real^3 -> bool) (s:real^3 -> bool ). (?v w v1 v2 v3 v4.\r
1041                    q = {v, w, v1, v2} /\ quartered_oct v w v1 v2 v3 v4 s)\r
1042   ==> strict_qua q s `, \r
1043 \r
1044 REWRITE_TAC[ quartered_oct; strict_qua; quarter] THEN \r
1045 ONCE_REWRITE_TAC[ GSYM (MESON[ DIST_TRIANGLE]` dist (v,w) <= dist (v,v1) + dist (v1,w) /\\r
1046      dist (v,w) <= dist (v,v2) + dist (v2,w) /\\r
1047      q = {v, w, v1, v2} <=>\r
1048      q = {v, w, v1, v2} `)] THEN \r
1049 ONCE_REWRITE_TAC[SET_RULE ` (!x. x IN {v1, v2, v3, v4}\r
1050           ==> dist (x,v) <= &2 * t0 /\ dist (x,w) <= &2 * t0) <=>\r
1051      (!x. x IN {v1, v2, v3, v4}\r
1052           ==> dist (x,v) <= &2 * t0 /\ dist (x,w) <= &2 * t0) /\\r
1053      dist (v1,v) <= &2 * t0 /\\r
1054      dist (v1,w) <= &2 * t0 /\ \r
1055   dist (v2,v) <= &2 * t0 /\\r
1056      dist (v2,w) <= &2 * t0 `]  THEN \r
1057 PHA THEN REWRITE_TAC[ GSYM d3 ] THEN \r
1058 ONCE_REWRITE_TAC[ SET_RULE ` q = {v, w, v1, v2} <=> q = {v, w, v1, v2} /\\r
1059   v IN q /\ w IN q `] THEN \r
1060 REWRITE_TAC[ MESON[]` d3 v w <= d3 v v1 + d3 v1 w /\\r
1061           d3 v w <= d3 v v2 + d3 v2 w /\\r
1062           (q = {v, w, v1, v2} /\ v IN q /\ w IN q) /\\r
1063           packing s /\\r
1064           &2 * t0 < d3 v w /\\r
1065           d3 v w < sqrt (&8) /\ last <=> ((q = {v, w, v1, v2} /\ v IN q /\ w IN q) /\\r
1066           packing s /\\r
1067           &2 * t0 < d3 v w /\\r
1068           d3 v w < sqrt (&8) ) /\ d3 v w <= d3 v v1 + d3 v1 w /\\r
1069           d3 v w <= d3 v v2 + d3 v2 w /\ last ` ] THEN \r
1070 REWRITE_TAC[ MESON[]` (?v w v1 v2 v3 v4.\r
1071           ((q = {v, w, v1, v2} /\ v IN q /\ w IN q) /\\r
1072            packing s /\\r
1073            &2 * t0 < d3 v w /\\r
1074            d3 v w < sqrt (&8)) /\\r
1075           last v w v1 v2 v3 v4 )\r
1076      ==> aa /\ bb /\ cc /\\r
1077          (?x y. x IN q /\ y IN q /\ &2 * t0 < d3 x y /\ d3 x y < sqrt (&8)) <=>\r
1078      (?v w v1 v2 v3 v4.\r
1079           ((q = {v, w, v1, v2} /\ v IN q /\ w IN q) /\\r
1080            packing s /\\r
1081            &2 * t0 < d3 v w /\\r
1082            d3 v w < sqrt (&8)) /\\r
1083           last v w v1 v2 v3 v4)\r
1084      ==> aa /\ bb /\ cc  `] THEN \r
1085 REWRITE_TAC[ simplex] THEN PHA THEN SIMP_TAC[] THEN REWRITE_TAC[ d3 ] THEN \r
1086 ONCE_REWRITE_TAC[ MESON[ prove(\r
1087                          `dist (v,w) <= dist (v,v1) + dist (v1,w) /\\r
1088                            dist (v1,v) <= &2 * t0 /\\r
1089                            dist (v1,w) <= &2 * t0 /\\r
1090                               &2 * t0 < dist (v,w) /\\r
1091                               dist (v,w) < sqrt (&8)\r
1092                             ==> &0 < dist (v,v1) /\ &0 < dist (v1,w)`, SIMP_TAC[ DIST_SYM; t0] THEN \r
1093                           REAL_ARITH_TAC)] `\r
1094           &2 * t0 < dist (v,w) /\\r
1095      dist (v,w) < sqrt (&8) /\\r
1096      dist (v,w) <= dist (v,v1) + dist (v1,w) /\\r
1097      dist (v,w) <= dist (v,v2) + dist (v2,w) /\\r
1098      (!x. x IN {v1, v2, v3, v4}\r
1099           ==> dist (x,v) <= &2 * t0 /\ dist (x,w) <= &2 * t0) /\\r
1100      dist (v1,v) <= &2 * t0 /\\r
1101      dist (v1,w) <= &2 * t0 /\\r
1102      dist (v2,v) <= &2 * t0 /\\r
1103      dist (v2,w) <= &2 * t0 /\\r
1104      last <=>\r
1105      &2 * t0 < dist (v,w) /\\r
1106      dist (v,w) < sqrt (&8) /\\r
1107      dist (v,w) <= dist (v,v1) + dist (v1,w) /\\r
1108      dist (v,w) <= dist (v,v2) + dist (v2,w) /\\r
1109      (!x. x IN {v1, v2, v3, v4}\r
1110           ==> dist (x,v) <= &2 * t0 /\ dist (x,w) <= &2 * t0) /\\r
1111      dist (v1,v) <= &2 * t0 /\\r
1112      dist (v1,w) <= &2 * t0 /\\r
1113      dist (v2,v) <= &2 * t0 /\\r
1114      dist (v2,w) <= &2 * t0 /\\r
1115      &0 < dist (v,v1) /\\r
1116      &0 < dist (v1,w) /\ &0 < dist (v,v2) /\\r
1117      &0 < dist (v2,w) /\\r
1118      last `] THEN \r
1119 REWRITE_TAC[ t0] THEN \r
1120 ONCE_REWRITE_TAC[ REAL_ARITH ` &2 <= dist (v1,v2) <=> &2 <= dist (v1,v2) /\ \r
1121   &0 < dist(v1,v2) `] THEN \r
1122 REWRITE_TAC[ MESON[] ` &0 < dist ( a, b ) /\ sau <=> sau /\ &0 < dist ( a,b) `] THEN PHA THEN \r
1123 ONCE_REWRITE_TAC[ MESON[ DIST_NZ]` &0 < dist(a,b) <=> &0 < dist(a,b) /\ ~(a=b) `] THEN \r
1124 PHA THEN  \r
1125 REWRITE_TAC[ MESON[]` ~(a=b) /\ last <=> last /\ ~( a=b) `] THEN PHA THEN \r
1126 REWRITE_TAC[ MESON[] ` q = {v, w, v1, v2} /\\r
1127           v IN q /\\r
1128           w IN q /\\r
1129           packing s /\ last <=> packing s /\ q = {v, w, v1, v2} /\\r
1130           v IN q /\\r
1131           w IN q /\\r
1132            last `] THEN \r
1133 REWRITE_TAC[ MESON[] `  (?v w v1 v2 v3 v4.\r
1134           packing s /\ last v w v1 v2 v3 v4 ) <=> packing s /\ (?v w v1 v2 v3 v4.\r
1135          last v w v1 v2 v3 v4 ) `] THEN SIMP_TAC[] THEN \r
1136 REWRITE_TAC[ MESON[] ` q = {v, w, v1, v2}  /\ last <=> last /\  q = {v, w, v1, v2} `] THEN \r
1137 ONCE_REWRITE_TAC[ SET_RULE `  {v, w, v1, v2, v3, v4} SUBSET s /\\r
1138           q = {v, w, v1, v2} <=> {v, w, v1, v2, v3, v4} SUBSET s /\\r
1139           q = {v, w, v1, v2} /\ q SUBSET s `] THEN \r
1140 REWRITE_TAC[ MESON[] `  ~(v = v1) /\\r
1141           ~(v1 = w) /\\r
1142           ~(v = v2) /\\r
1143           ~(v2 = w) /\\r
1144           ~(v4 = v1) /\\r
1145           ~(v3 = v4) /\\r
1146           ~(v2 = v3) /\\r
1147           ~(v1 = v2) /\\r
1148           {v, w, v1, v2, v3, v4} SUBSET s /\\r
1149           q = {v, w, v1, v2} /\\r
1150           q SUBSET s <=> {v, w, v1, v2, v3, v4} SUBSET s /\ \r
1151   q SUBSET s /\ (  ~(v = v1) /\\r
1152           ~(v1 = w) /\\r
1153           ~(v = v2) /\\r
1154           ~(v2 = w) /\\r
1155           ~(v4 = v1) /\\r
1156           ~(v3 = v4) /\\r
1157           ~(v2 = v3) /\\r
1158           ~(v1 = v2) /\ q = {v, w, v1, v2}  )  `] THEN \r
1159 REWRITE_TAC[ MESON[] ` a /\ b/\ c <=> ( a/\ b) /\ c `] THEN \r
1160 REWRITE_TAC[ MESON[]` a /\ b <=> b /\ a `] THEN \r
1161 REWRITE_TAC[ MESON[] ` (?v w v1 v2 v3 v4.\r
1162           q = {v, w, v1, v2} /\\r
1163           ~(v1 = v2) /\\r
1164           ~(v2 = v3) /\\r
1165           ~(v3 = v4) /\\r
1166           ~(v4 = v1) /\\r
1167           ~(v2 = w) /\\r
1168           ~(v = v2) /\\r
1169           ~(v1 = w) /\\r
1170           ~(v = v1) /\\r
1171           q SUBSET s /\ la v w v1 v2 v3 v4 ) <=> \r
1172   q SUBSET s /\ (?v w v1 v2 v3 v4.\r
1173           q = {v, w, v1, v2} /\\r
1174           ~(v1 = v2) /\\r
1175           ~(v2 = v3) /\\r
1176           ~(v3 = v4) /\\r
1177           ~(v4 = v1) /\\r
1178           ~(v2 = w) /\\r
1179           ~(v = v2) /\\r
1180           ~(v1 = w) /\\r
1181           ~(v = v1) /\\r
1182           la v w v1 v2 v3 v4 ) `] THEN SIMP_TAC[] THEN \r
1183 ONCE_REWRITE_TAC[ MESON[ REAL_ARITH ` &0 < &2 * #1.255 /\ \r
1184 ( ! a b c. a < b /\ b < c ==> a < c )`; DIST_NZ ] ` &2 * #1.255 < dist (v,w)\r
1185  <=> ~(v=w) /\ &2 * #1.255 < dist (v,w) ` ] THEN PHA THEN \r
1186 REWRITE_TAC[ MESON[] ` (~(v = w) /\ &2 * #1.255 < dist (v,w) /\ v IN q /\ w IN q <=>\r
1187       &2 * #1.255 < dist (v,w) /\ v IN q /\ w IN q /\ ~(v = w)) /\\r
1188      (a /\ b /\ c <=> (a /\ b) /\ c) `] THEN \r
1189 REWRITE_TAC[ MESON[] ` ~(v = w) /\ &2 * #1.255 < dist (v,w) /\ v IN q /\ w IN q <=>\r
1190       &2 * #1.255 < dist (v,w) /\ v IN q /\ w IN q /\ ~(v = w)\r
1191      `] THEN \r
1192 REWRITE_TAC[ MESON[] ` a /\ b /\ c <=> (a/\b) /\ c `] THEN \r
1193 REWRITE_TAC [MESON[] ` aa /\  ~(v = w) <=> ~(v=w) /\ aa `] THEN PHA  THEN \r
1194 REWRITE_TAC[ MESON[]` ~(v = w) /\\r
1195           ~(v = v1) /\\r
1196           ~(v1 = w) /\\r
1197           ~(v = v2) /\\r
1198           ~(v2 = w) /\\r
1199           ~(v4 = v1) /\\r
1200           ~(v3 = v4) /\\r
1201           ~(v2 = v3) /\\r
1202           ~(v1 = v2) /\\r
1203           q = {v, w, v1, v2} /\ last <=> (~(v = w) /\\r
1204           ~(v = v1) /\\r
1205           ~(v1 = w) /\\r
1206           ~(v = v2) /\\r
1207           ~(v2 = w) /\\r
1208           ~(v4 = v1) /\\r
1209           ~(v3 = v4) /\\r
1210           ~(v2 = v3) /\\r
1211           ~(v1 = v2) /\\r
1212           q = {v, w, v1, v2}) /\ last `] THEN \r
1213 SIMP_TAC[ SET_RULE ` {v1, v2, v3, v4} = q <=> q = {v1, v2, v3, v4}`] THEN \r
1214 ONCE_REWRITE_TAC[ MESON[ SET_RULE ` ~(v = w) /\\r
1215            ~(v = v1) /\\r
1216            ~(v1 = w) /\\r
1217            ~(v = v2) /\\r
1218            ~(v2 = w) /\\r
1219            ~(v4 = v1) /\\r
1220            ~(v3 = v4) /\\r
1221            ~(v2 = v3) /\\r
1222            ~(v1 = v2) ==>\r
1223    ( {v, w} INTER {v1, v2 } = {} /\ ~(v = w \/ v1 = v2 ) )` ] `\r
1224   ~(v = w) /\\r
1225      ~(v = v1) /\\r
1226      ~(v1 = w) /\\r
1227      ~(v = v2) /\\r
1228      ~(v2 = w) /\\r
1229      ~(v4 = v1) /\\r
1230      ~(v3 = v4) /\\r
1231      ~(v2 = v3) /\\r
1232      ~(v1 = v2) /\\r
1233      q = {v, w, v1, v2} <=>\r
1234      (q = {v, w, v1, v2} /\\r
1235       {v, w} INTER {v1, v2} = {} /\\r
1236       ~(v = w \/ v1 = v2)) /\\r
1237      ~(v = w) /\\r
1238      ~(v = v1) /\\r
1239      ~(v1 = w) /\\r
1240      ~(v = v2) /\\r
1241      ~(v2 = w) /\\r
1242      ~(v4 = v1) /\\r
1243      ~(v3 = v4) /\\r
1244      ~(v2 = v3) /\\r
1245      ~(v1 = v2) `] THEN \r
1246 PHA THEN ONCE_REWRITE_TAC[MESON[]` (?v w v1 v2 v3 v4.\r
1247           q = {v, w, v1, v2} /\\r
1248           {v, w} INTER {v1, v2} = {} /\\r
1249           ~(v = w \/ v1 = v2) /\\r
1250           last v w v1 v2 v3 v4) <=>\r
1251      (?v w v1 v2.\r
1252           q = {v, w, v1, v2} /\\r
1253           {v, w} INTER {v1, v2} = {} /\\r
1254           ~(v = w \/ v1 = v2)) /\\r
1255      (?v w v1 v2 v3 v4.\r
1256           q = {v, w, v1, v2} /\\r
1257           {v, w} INTER {v1, v2} = {} /\\r
1258           ~(v = w \/ v1 = v2) /\\r
1259           last v w v1 v2 v3 v4) `] THEN SIMP_TAC[] THEN PHA THEN \r
1260 MATCH_MP_TAC (MESON[] `(! q s. gi q s ==> cc q s ) ==> \r
1261    ( ! q s. a q /\ gi q s /\ b s ==> cc q s ) `) THEN \r
1262 REWRITE_TAC[ MESON[] ` {v, w, v1, v2, v3, v4} SUBSET s /\ a <=> a /\\r
1263  {v, w, v1, v2, v3, v4} SUBSET s `] THEN \r
1264 REWRITE_TAC[ MESON[]` q = {v, w, v1, v2} /\ a <=> a /\ q = {v, w, v1, v2} `] THEN PHA THEN \r
1265 ONCE_REWRITE_TAC[SET_RULE ` {v, w, v1, v2, v3, v4} SUBSET s /\ q = {v, w, v1, v2} <=>\r
1266      {v, w, v1, v2, v3, v4} SUBSET s /\ q = {v, w, v1, v2} /\ q SUBSET s `] THEN \r
1267 NGOAC THEN ONCE_REWRITE_TAC[MESON[] ` (?v w v1 v2 v3 v4. aaa v w v1 v2 v3 v4 /\ \r
1268   q SUBSET s ) <=> q SUBSET s /\ (?v w v1 v2 v3 v4. aaa v w v1 v2 v3 v4)`] THEN PHA THEN \r
1269 SIMP_TAC[] THEN \r
1270 REWRITE_TAC[ MESON[]` dist (v1,v2) <= &2 * #1.255 /\\r
1271      &0 < dist (v1,v2) /\\r
1272      &2 <= dist (v1,v2) /\\r
1273      dist (v2,w) <= &2 * #1.255 /\\r
1274      dist (v2,v) <= &2 * #1.255 /\\r
1275      dist (v1,w) <= &2 * #1.255 /\\r
1276      dist (v1,v) <= &2 * #1.255 /\\r
1277      last <=>\r
1278      &0 < dist (v1,v2) /\\r
1279      &2 <= dist (v1,v2) /\\r
1280      last /\\r
1281      dist (v1,v2) <= &2 * #1.255 /\\r
1282      dist (v2,w) <= &2 * #1.255 /\\r
1283      dist (v2,v) <= &2 * #1.255 /\\r
1284      dist (v1,w) <= &2 * #1.255 /\\r
1285      dist (v1,v) <= &2 * #1.255 `] THEN PHA  THEN \r
1286 ONCE_REWRITE_TAC[ SET_RULE ` q = {v, w, v1, v2} <=>\r
1287      q = {v, w, v1, v2} /\\r
1288      (!x y.\r
1289           ~({x, y} = {v, w}) /\ x IN q /\ y IN q\r
1290           ==> (x = v \/ x = w \/ x = v1 \/ x = v2) /\\r
1291               (y = v \/ y = w \/ y = v1 \/ y = v2) /\\r
1292               ~(x = v /\ y = w \/ x = w /\ y = v)) `] THEN \r
1293 REWRITE_TAC[ MESON[] ` ~( a\/ b ) <=> ~ a /\ ~ b `] THEN \r
1294 NGOAC THEN REWRITE_TAC[ MESON[] ` a /\ ( b \/ c ) <=> a /\ b \/ a /\ c `] THEN \r
1295 \r
1296 PHA THEN REWRITE_TAC[ MESON[]` day /\ ~(x = v /\ y = w) /\\r
1297                    ~(x = w /\ y = v) <=> \r
1298   ~(x = v /\ y = w) /\\r
1299                    ~(x = w /\ y = v) /\ day `] THEN \r
1300 PHA THEN REWRITE_TAC[ MESON[] ` ( a \/ b ) /\c <=> a /\ c \/ b /\ c `] THEN PHA THEN \r
1301 REWRITE_TAC[ MESON[] ` (a\/b) \/ c <=> a \/ b\/ c`] THEN \r
1302 REWRITE_TAC[ MESON[] ` ~(x = v /\ y = w) /\\r
1303      ~(x = w /\ y = v) /\\r
1304      (x = v /\ y = v \/\r
1305       x = w /\ y = v \/\r
1306       x = v1 /\ y = v \/\r
1307       x = v2 /\ y = v \/\r
1308       x = v /\ y = w \/\r
1309       last) <=>\r
1310      ~(x = v /\ y = w) /\\r
1311      ~(x = w /\ y = v) /\\r
1312      (x = v /\ y = v \/ x = v1 /\ y = v \/ x = v2 /\ y = v \/ last) `] THEN \r
1313 REWRITE_TAC[ MESON[ SET_RULE ` ~({x, y} = {v, w}) <=> ~(x = v /\ y = w) /\ ~(x = w /\ y = v)`]\r
1314   ` (!x y.\r
1315           ~({x, y} = {v, w}) /\ x IN q /\ y IN q\r
1316           ==> ~(x = v /\ y = w) /\ ~(x = w /\ y = v) /\ last x y)\r
1317      <=> (!x y. ~({x, y} = {v, w}) /\ x IN q /\ y IN q ==> last x y) `] THEN \r
1318 ONCE_REWRITE_TAC[ MESON[DIST_REFL; REAL_ARITH ` a = &0 ==> a <= &2 * #1.255 `]\r
1319  ` x = v /\ y = v <=> x = v /\ y = v /\ dist(x,y) <= &2 * #1.255 `] THEN \r
1320 REWRITE_TAC[ MESON[]` ( ! x y. P x y ) /\ last <=> last /\ ( ! x y. P x y)`] THEN PHA THEN \r
1321 ONCE_REWRITE_TAC[MESON[]` dist (v1,v2) <= &2 * #1.255 /\\r
1322      dist (v2,w) <= &2 * #1.255 /\\r
1323      dist (v2,v) <= &2 * #1.255 /\\r
1324      dist (v1,w) <= &2 * #1.255 /\\r
1325      dist (v1,v) <= &2 * #1.255 /\\r
1326      (!x y. ~({x, y} = {v, w}) /\ x IN q /\ y IN q ==> last x y) <=>\r
1327      dist (v1,v2) <= &2 * #1.255 /\\r
1328      dist (v2,w) <= &2 * #1.255 /\\r
1329      dist (v2,v) <= &2 * #1.255 /\\r
1330      dist (v1,w) <= &2 * #1.255 /\\r
1331      dist (v1,v) <= &2 * #1.255 /\\r
1332      (!x y.\r
1333           ~({x, y} = {v, w}) /\ x IN q /\ y IN q\r
1334           ==> \r
1335               dist (v1,v2) <= &2 * #1.255 /\\r
1336               dist (v2,w) <= &2 * #1.255 /\\r
1337               dist (v2,v) <= &2 * #1.255 /\\r
1338               dist (v1,w) <= &2 * #1.255 /\\r
1339               dist (v1,v) <= &2 * #1.255 /\ last x y) `] THEN \r
1340 REWRITE_TAC[ MESON[ DIST_SYM]`dist (v1,v2) <= &2 * #1.255 /\\r
1341      dist (v2,w) <= &2 * #1.255 /\\r
1342      dist (v2,v) <= &2 * #1.255 /\\r
1343      dist (v1,w) <= &2 * #1.255 /\\r
1344      dist (v1,v) <= &2 * #1.255 /\\r
1345      (x = v /\ y = v /\ dist (x,y) <= &2 * #1.255 \/\r
1346       x = v1 /\ y = v \/\r
1347       x = v2 /\ y = v \/\r
1348       last) <=>\r
1349      dist (v1,v2) <= &2 * #1.255 /\\r
1350      dist (v2,w) <= &2 * #1.255 /\\r
1351      dist (v2,v) <= &2 * #1.255 /\\r
1352      dist (v1,w) <= &2 * #1.255 /\\r
1353      dist (v1,v) <= &2 * #1.255 /\\r
1354      (x = v /\ y = v /\ dist (x,y) <= &2 * #1.255 \/\r
1355       x = v1 /\ y = v /\ dist (x,y) <= &2 * #1.255 \/\r
1356       x = v2 /\ y = v /\ dist (x,y) <= &2 * #1.255 \/\r
1357       last) `] THEN \r
1358 REWRITE_TAC[ MESON[]` a \/ b \/ c <=> (a \/ b ) \/ c `] THEN \r
1359 REWRITE_TAC[ MESON[] ` ((((a \/ x = v2 /\ y = v1) \/ x = v /\ y = v2) \/ x = w /\ y = v2) \/\r
1360       x = v1 /\ y = v2) \/\r
1361      x = v2 /\ y = v2 /\ dist (x,y) <= &2 * #1.255 <=>\r
1362      (((x = v2 /\ y = v1 \/ x = v /\ y = v2) \/ x = w /\ y = v2) \/\r
1363       x = v1 /\ y = v2) \/\r
1364      x = v2 /\ y = v2 /\ dist (x,y) <= &2 * #1.255 \/\r
1365      a `] THEN \r
1366 REWRITE_TAC[ GSYM (MESON[]` a \/ b \/ c <=> (a \/ b ) \/ c `)] THEN \r
1367 REWRITE_TAC[MESON[DIST_SYM ]` dist (v1,v2) <= &2 * #1.255 /\\r
1368                    dist (v2,w) <= &2 * #1.255 /\\r
1369                    dist (v2,v) <= &2 * #1.255 /\\r
1370                    dist (v1,w) <= &2 * #1.255 /\\r
1371                    dist (v1,v) <= &2 * #1.255 /\\r
1372                    (x = v2 /\ y = v1 \/\r
1373                     x = v /\ y = v2 \/\r
1374                     x = w /\ y = v2 \/\r
1375                     x = v1 /\ y = v2 \/ last ) \r
1376   <=> dist (v1,v2) <= &2 * #1.255 /\\r
1377                    dist (v2,w) <= &2 * #1.255 /\\r
1378                    dist (v2,v) <= &2 * #1.255 /\\r
1379                    dist (v1,w) <= &2 * #1.255 /\\r
1380                    dist (v1,v) <= &2 * #1.255 /\\r
1381                    ((x = v2 /\ y = v1 \/ \r
1382                     x = v /\ y = v2 \/\r
1383                     x = w /\ y = v2 \/\r
1384                     x = v1 /\ y = v2 ) /\ dist( x,y) <= &2 * #1.255 \/ last ) `] THEN \r
1385 REWRITE_TAC[ MESON[]` a \/ b \/ c <=> (a \/ b ) \/ c `] THEN \r
1386 REWRITE_TAC[ MESON[]` ((((a \/ x = v1 /\ y = w) \/\r
1387                        x = v2 /\ y = w) \/\r
1388                       x = v /\ y = v1) \/\r
1389                      x = w /\ y = v1) \/\r
1390                     x = v1 /\ y = v1 /\ dist (x,y) <= &2 * #1.255 <=>\r
1391   (((x = v1 /\ y = w \/\r
1392                        x = v2 /\ y = w) \/\r
1393                       x = v /\ y = v1) \/\r
1394                      x = w /\ y = v1) \/\r
1395                     x = v1 /\ y = v1 /\ dist (x,y) <= &2 * #1.255 \/ a `] THEN \r
1396 REWRITE_TAC[ GSYM (MESON[]` a \/ b \/ c <=> (a \/ b ) \/ c `)] THEN \r
1397 REWRITE_TAC[ MESON[ DIST_SYM ] ` \r
1398   dist (v1,v2) <= &2 * #1.255 /\\r
1399      dist (v2,w) <= &2 * #1.255 /\\r
1400      dist (v2,v) <= &2 * #1.255 /\\r
1401      dist (v1,w) <= &2 * #1.255 /\\r
1402      dist (v1,v) <= &2 * #1.255 /\\r
1403      (x = v1 /\ y = w \/\r
1404       x = v2 /\ y = w \/\r
1405       x = v /\ y = v1 \/\r
1406       x = w /\ y = v1 \/\r
1407       last) <=>\r
1408      dist (v1,v2) <= &2 * #1.255 /\\r
1409      dist (v2,w) <= &2 * #1.255 /\\r
1410      dist (v2,v) <= &2 * #1.255 /\\r
1411      dist (v1,w) <= &2 * #1.255 /\\r
1412      dist (v1,v) <= &2 * #1.255 /\\r
1413      ((x = v1 /\ y = w \/\r
1414        x = v2 /\ y = w \/\r
1415        x = v /\ y = v1 \/\r
1416        x = w /\ y = v1) /\\r
1417       dist (x,y) <= &2 * #1.255 \/\r
1418       last) `] THEN \r
1419 REWRITE_TAC[ MESON[] ` x = v1 /\ y = v2 /\ dist (x,y) <= &2 * #1.255 \r
1420   <=> (x = v1 /\ y = v2) /\ dist (x,y) <= &2 * #1.255 `] THEN \r
1421 REWRITE_TAC[ GSYM (MESON[]` a \/ b \/ c <=> (a \/ b ) \/ c `)] THEN \r
1422 REWRITE_TAC[ MESON[]` a /\ c \/ b /\ c <=> ( a\/ b) /\ c `] THEN NGOAC THEN \r
1423 ONCE_REWRITE_TAC[ MESON[] ` ( ! x y. P x y ==> L x y /\ TT x y ) <=>\r
1424   ( ! x y. P x y ==> L x y /\ TT x y ) /\ ( ! x y. P x y ==> TT x y ) `] THEN \r
1425 NGOAC THEN \r
1426 REWRITE_TAC[ MESON[]` a /\ (!x y.\r
1427                (~({x, y} = {v, w}) /\ x IN q) /\ y IN q\r
1428                ==> dist (x,y) <= &2 * #1.255) <=> (!x y.\r
1429                (~({x, y} = {v, w}) /\ x IN q) /\ y IN q\r
1430                ==> dist (x,y) <= &2 * #1.255) /\ a `] THEN \r
1431 REWRITE_TAC[ MESON[]` ((( a /\dist (v,w) < sqrt (&8)) /\\r
1432                     &2 * #1.255 < dist (v,w)) /\\r
1433                    v IN q) /\\r
1434                   w IN q\r
1435   <=> (((dist (v,w) < sqrt (&8)) /\\r
1436                     &2 * #1.255 < dist (v,w)) /\\r
1437                    v IN q) /\\r
1438                   w IN q /\ a `] THEN PHA THEN \r
1439 ONCE_REWRITE_TAC[MESON[ REAL_ARITH ` a < b ==> a <= b `]` (?v w v1 v2 v3 v4.\r
1440           (!x y.\r
1441                ~({x, y} = {v, w}) /\ x IN q /\ y IN q\r
1442                ==> dist (x,y) <= &2 * #1.255) /\\r
1443           dist (v,w) < sqrt (&8) /\\r
1444           &2 * #1.255 < dist (v,w) /\\r
1445           v IN q /\\r
1446           w IN q /\ last v w v1 v2 v3 v4 )\r
1447   <=> (?v w.\r
1448               (!x y.\r
1449                    ~({x, y} = {v, w}) /\ x IN q /\ y IN q\r
1450                    ==> dist (x,y) <= &2 * #1.255) /\\r
1451               dist (v,w) <= sqrt (&8) /\\r
1452               &2 * #1.255 <= dist (v,w) /\\r
1453               v IN q /\\r
1454               w IN q) /\ (?v w v1 v2 v3 v4.\r
1455           (!x y.\r
1456                ~({x, y} = {v, w}) /\ x IN q /\ y IN q\r
1457                ==> dist (x,y) <= &2 * #1.255) /\\r
1458           dist (v,w) < sqrt (&8) /\\r
1459           &2 * #1.255 < dist (v,w) /\\r
1460           v IN q /\\r
1461           w IN q /\ last v w v1 v2 v3 v4 )`] THEN PHA THEN \r
1462 REPEAT GEN_TAC THEN MATCH_MP_TAC (MESON[] ` ( b ==> d ) ==> (a /\ b /\ c ==> d) `) THEN \r
1463 MESON_TAC[]);;\r
1464 \r
1465 (* ======== *)\r
1466 \r
1467 let WHEN_IN_Q_SYS = prove (`! q s. q IN Q_SYS s ==> quasi_reg_tet q s \/ strict_qua q s \/ \r
1468 (?v v1 v3 v2 v4.\r
1469                    (q = {v, v1, v2, v3} \/ q = {v, v1, v3, v4}) /\\r
1470                    interior_pos v v1 v3 v2 v4 s /\\r
1471                    anchor_points v1 v3 s = {v, v2, v4} /\\r
1472                    anchor_points v2 v4 s = {v, v1, v3})`,\r
1473 REWRITE_TAC[ Q_SYS; IN_ELIM_THM] THEN MESON_TAC[strict_qua_in_oct] );; \r
1474 \r
1475 (* ====== *)\r
1476 \r
1477 \r
1478 let CASES_OF_Q_SYS = prove (`!q s. q IN Q_SYS s ==> quasi_reg_tet q s \/ strict_qua q s`,\r
1479 NHANH (MATCH_MP (MESON[]` ( ! a b. P a b) ==> P a b` ) WHEN_IN_Q_SYS) THEN \r
1480 REPEAT GEN_TAC THEN MATCH_MP_TAC (MESON[]` ( c ==> b) ==>  aa /\ ( a \/ b\/ c )\r
1481   ==> a \/ b `) THEN REWRITE_TAC[ RELATE_Q_SYS]);;\r
1482 \r
1483 (* ======= *)\r
1484 \r
1485 \r
1486 let simplex_interior_pos = prove(`!s v v1 v2 v3 v4.\r
1487      interior_pos v v1 v3 v2 v4 s\r
1488      ==> simplex {v, v1, v3, v2} s /\\r
1489          simplex {v, v1, v3, v4} s /\\r
1490          simplex {v, v2, v4, v1} s /\\r
1491          simplex {v, v2, v4, v3} s`,\r
1492 ONCE_REWRITE_TAC[ MESON[strict_qua2_interior_pos]` \r
1493 interior_pos v v1 v3 v2 v4 s <=>\r
1494   interior_pos v v1 v3 v2 v4 s /\ strict_qua2 {v, v1, v3, v2} {v1, v3} s /\\r
1495              strict_qua2 {v, v1, v3, v4} {v1, v3} s /\\r
1496              strict_qua2 {v, v2, v4, v1} {v2, v4} s /\\r
1497              strict_qua2 {v, v2, v4, v3} {v2, v4} s `] THEN \r
1498 REWRITE_TAC[ strict_qua2 ] THEN \r
1499 NGOAC THEN REWRITE_TAC[ MESON[]` a /\  quarter {v, v1, v2, v3} s <=> \r
1500   quarter {v, v1, v2, v3} s /\ a `] THEN PHA THEN \r
1501 REPEAT GEN_TAC THEN MATCH_MP_TAC (MESON[] ` (a /\ b/\c /\ d ==> las )\r
1502   ==> ( a/\ b/\ c/\ d /\ dd ==> las ) `) THEN \r
1503 NGOAC THEN REWRITE_TAC[ MESON[] `(( a /\ packing s ) /\\r
1504     simplex {v, v1, v2, v3} s) <=> simplex {v, v1, v2, v3} s /\ packing s /\ a`] THEN \r
1505 REWRITE_TAC[MESON[]`  packing s /\ a <=> a /\ packing s`] THEN PHA THEN \r
1506 MESON_TAC[quarter]);;\r
1507 \r
1508 (* =========== *)\r
1509 \r
1510 \r
1511 let QUA_TET_IMPLY_QUA_TRI = prove(` ! s v0 v1 v2 . (?v4. quasi_reg_tet ({v0, v1, v2} UNION {v4}) s)\r
1512  ==> quasi_tri {v0, v1, v2} s`, REWRITE_TAC[ quasi_reg_tet; quasi_tri] THEN \r
1513 REWRITE_TAC[ SET_RULE ` {a,b,c} UNION {d} = {a,b,c,d} `; def_simplex; set_3elements] THEN \r
1514 MESON_TAC[SET_RULE ` {a,b,c} SUBSET {a,b,c,d} ` ; SUBSET; SUBSET_TRANS]);;\r
1515 \r
1516 \r
1517 let PAIR_D3 = prove(` ! i j u w. {u,w} = {i,j} ==> d3 i j = d3 u w `, \r
1518 REWRITE_TAC[ SET_RULE ` {u, w} = {i, j} <=>  u= i /\ w = j \/ u = j /\ w = i `] THEN \r
1519 MESON_TAC[ trg_d3_sym]);;\r
1520 \r
1521 \r
1522 let PAIR_DIST = prove(` ! i j u w. {u,w} = {i,j} ==> dist(i,j) = dist(u,w) `, \r
1523 REWRITE_TAC[ SET_RULE ` {u, w} = {i, j} <=>  u= i /\ w = j \/ u = j /\ w = i `] THEN \r
1524 MESON_TAC[ DIST_SYM]);;\r
1525 \r
1526 \r
1527 \r
1528 (* ============== *)\r
1529 \r
1530 let DIAGONAL_QUA = prove(`!a b q s.\r
1531      a IN q /\\r
1532      b IN q /\\r
1533      &2 * t0 < d3 a b /\\r
1534      quarter q s \r
1535      ==> diagonal a b q s `,\r
1536 REWRITE_TAC[diagonal; SET_RULE ` a IN q /\ b IN q /\ &2 * t0 < d3 a b /\ quarter q s\r
1537      ==> quarter q s /\  {a, b} SUBSET q /\ l <=>  a IN q /\ b IN q /\ &2 * t0 < d3 a b \r
1538    /\ quarter q s ==> l`] THEN REWRITE_TAC[quarter] THEN NGOAC THEN \r
1539 REWRITE_TAC[ MESON[] ` a /\ (? u v. P u v ) <=> (? u v. a /\ P u v ) `] THEN \r
1540 REWRITE_TAC[ REAL_ARITH ` a < b <=> ~( b <= a ) `] THEN \r
1541 PHA THEN REWRITE_TAC[ MESON[]` a IN q /\  b IN q /\ ~(d3 a b <= &2 * t0)  /\ las <=> \r
1542 las /\ a IN q /\  b IN q /\ ~(d3 a b <= &2 * t0) `] THEN PHA THEN \r
1543 NHANH (MESON[]` (!x y.\r
1544                x IN q /\ y IN q /\ ~({x, y} = {v, w}) ==> d3 x y <= &2 * t0) /\\r
1545           a IN q /\\r
1546           b IN q /\\r
1547           ~(d3 a b <= &2 * t0) ==> {a,b} = {v,w} `) THEN \r
1548 NHANH (MESON[ PAIR_D3] ` aa /\ {a, b} = {v, w} ==> d3 a b = d3 v w `) THEN \r
1549 MESON_TAC[ PAIR_D3; REAL_ARITH` (a <= a) /\ ( a <= b /\ b <= c ==> a <= c ) `]);;\r
1550 \r
1551 \r
1552 \r
1553 \r
1554 let NOV2 = prove( `!a b c v4.\r
1555      (?i j. i IN {a, b, c} /\ j IN {a, b, c} /\ ~(i = j) /\ #2.51 < d3 i j) /\\r
1556      (?v w.\r
1557           v IN {a, b, c, v4} /\\r
1558           w IN {a, b, c, v4} /\\r
1559           #2.51 <= d3 v w /\\r
1560           d3 v w <= sqrt (&8) /\\r
1561           (!x y.\r
1562                x IN {a, b, c, v4} /\ y IN {a, b, c, v4} /\ ~({x, y} = {v, w})\r
1563                ==> d3 x y <= #2.51))\r
1564      ==> (?i j.\r
1565               i IN {a, b, c} /\\r
1566               j IN {a, b, c} /\\r
1567               #2.51 < d3 i j /\\r
1568               (!x y.\r
1569                    x IN {a, b, c} /\ y IN {a, b, c} /\ ~({x, y} = {i, j})\r
1570                    ==> d3 x y <= #2.51))`,\r
1571 REWRITE_TAC[ MESON[] ` (? i j. P i j ) /\ (? v w. Q v w ) <=> ( ? i j u w. P i j /\ Q u w ) `] THEN \r
1572 REWRITE_TAC[ MESON[] ` (i IN {a, b, c} /\ j IN {a, b, c} /\ ~(i = j) /\ #2.51 < d3 i j) /\ aa <=>\r
1573   aa /\ (i IN {a, b, c} /\ j IN {a, b, c} /\ ~(i = j) /\ #2.51 < d3 i j)`] THEN \r
1574 PHA THEN \r
1575 REWRITE_TAC[ REAL_ARITH ` a < b <=> ~( b <= a ) `] THEN \r
1576 NHANH (MESON[ SET_RULE ` x IN {a,b,c} ==> x IN {a,b,c,d} ` ] ` (!x y.\r
1577                x IN {a, b, c, v4} /\ y IN {a, b, c, v4} /\ ~({x, y} = {u, w})\r
1578                ==> d3 x y <= #2.51) /\\r
1579           i IN {a, b, c} /\\r
1580           j IN {a, b, c} /\\r
1581           ~(i = j) /\\r
1582           ~(d3 i j <= #2.51)\r
1583   ==> {i,j} = {u,w} `) THEN PHA THEN \r
1584 NHANH ( MESON[ PAIR_D3] ` ~(d3 i j <= #2.51) /\\r
1585           {i, j} = {u, w} ==> d3 i j = d3 u w `) THEN \r
1586 PHA THEN REWRITE_TAC[ MESON[]` {i, j} = {u, w} /\ a <=> a /\ {i, j} = {u, w}`] THEN \r
1587 REWRITE_TAC[ MESON[] ` (! x y. P x y ) /\ a <=> a /\ (! x y. P x y) `] THEN PHA THEN \r
1588 NHANH ( MESON[  SET_RULE ` x IN {a,b,c} ==> x IN {a,b,c,d} `] ` {i, j} = {u, w} /\\r
1589           (!x y.\r
1590                x IN {a, b, c, v4} /\ y IN {a, b, c, v4} /\ ~({x, y} = {u, w})\r
1591                ==> d3 x y <= #2.51)\r
1592   ==> (!x y.\r
1593                x IN {a, b, c} /\ y IN {a, b, c} /\ ~({x, y} = {i, j})\r
1594                ==> d3 x y <= #2.51)`) THEN MESON_TAC[]);;\r
1595 \r
1596 \r
1597 \r
1598 let TRIANGLE_IN_STRICT_QUA = prove( `!s a b c.\r
1599      (?v4. strict_qua ( {a,b,c} UNION {v4}) s)\r
1600      ==> quasi_tri {a,b,c} s \/\r
1601          (?aa bb.\r
1602               {aa, bb} SUBSET {a,b,c} /\\r
1603               #2.51 < dist (aa,bb) /\\r
1604               (!x y.\r
1605                    ~({x, y} = {aa, bb}) /\ {x, y} SUBSET {a,b,c}\r
1606                    ==> dist (x,y) <= #2.51))`,\r
1607 REWRITE_TAC[ strict_qua; quarter; simplex] THEN \r
1608 REWRITE_TAC[SET_RULE `{a, b, c} UNION {d} = {a,b,c,d}`;MESON[]` {v1, v2, v3, v4'} = \r
1609  {a, b, c, v4} <=> {a, b, c, v4} = {v1, v2, v3, v4'} `;  SET_OF_4] THEN \r
1610 REWRITE_TAC[ quasi_tri] THEN \r
1611 NHANH (MESON[] ` {a, b, c, v4} SUBSET s ==> ((!i j.\r
1612            i IN {a, b, c} /\ j IN {a, b, c} /\ ~(i = j)\r
1613            ==> d3 i j <= &2 * t0) \/\r
1614       (?i j.\r
1615            i IN {a, b, c} /\ j IN {a, b, c} /\ ~(i = j)\r
1616            /\ ~(d3 i j <= &2 * t0))) `) THEN PHA THEN \r
1617 NHANH (SET_RULE ` {a, b, c, v4} SUBSET s ==> {a, b, c} SUBSET s `) THEN \r
1618 REPEAT GEN_TAC THEN KHANANG THEN \r
1619 MATCH_MP_TAC (MESON[] ` ((? a. P a) ==> l) /\ ((?a. Q a ) ==> l ) ==> \r
1620   (?a . P a \/ Q a ) ==> l `) THEN \r
1621 REWRITE_TAC[ MESON[]` (?v4. packing s /\\r
1622            packing s /\\r
1623            {a, b, c, v4} SUBSET s /\\r
1624            {a, b, c} SUBSET s /\\r
1625            (!i j.\r
1626                 i IN {a, b, c} /\ j IN {a, b, c} /\ ~(i = j)\r
1627                 ==> d3 i j <= &2 * t0) /\\r
1628            ~(a = b \/ a = c \/ a = v4 \/ b = c \/ b = v4 \/ c = v4) /\\r
1629            (?v w.\r
1630                 v IN {a, b, c, v4} /\\r
1631                 w IN {a, b, c, v4} /\\r
1632                 &2 * t0 <= d3 v w /\\r
1633                 d3 v w <= sqrt (&8) /\\r
1634                 (!x y.\r
1635                      x IN {a, b, c, v4} /\\r
1636                      y IN {a, b, c, v4} /\\r
1637                      ~({x, y} = {v, w})\r
1638                      ==> d3 x y <= &2 * t0)) /\\r
1639            (?x y.\r
1640                 x IN {a, b, c, v4} /\\r
1641                 y IN {a, b, c, v4} /\\r
1642                 &2 * t0 < d3 x y /\\r
1643                 d3 x y < sqrt (&8)))\r
1644      ==> packing s /\\r
1645          {a, b, c} SUBSET s /\\r
1646          (?a' b' c'.\r
1647               ~(a' = b' \/ b' = c' \/ c' = a') /\ {a', b', c'} = {a, b, c}) /\\r
1648          (!x y.\r
1649               x IN {a, b, c} /\ y IN {a, b, c} /\ ~(x = y)\r
1650               ==> d3 x y <= &2 * t0) \/\r
1651          (?aa bb.\r
1652               {aa, bb} SUBSET {a, b, c} /\\r
1653               #2.51 < dist (aa,bb) /\\r
1654               (!x y.\r
1655                    ~({x, y} = {aa, bb}) /\ {x, y} SUBSET {a, b, c}\r
1656                    ==> dist (x,y) <= #2.51))`] THEN \r
1657 REWRITE_TAC[ GSYM d3; REAL_ARITH ` ~( a <= b ) <=> b < a `] THEN \r
1658 REWRITE_TAC[ t0; REAL_ARITH` &2 * #1.255 = #2.51 `] THEN \r
1659 REWRITE_TAC[ SET_RULE ` {aa, bb} SUBSET s <=> aa IN s /\ bb IN s `] THEN \r
1660 ONCE_REWRITE_TAC[ MESON[]`(? x y. P x y ) /\ a <=> a /\ (? x y. P x y )`] THEN PHA THEN \r
1661 ONCE_REWRITE_TAC[ MESON[] ` (? x y . P x y ) /\ a /\ b <=> a /\ b /\ (? x y. P x y)`] THEN \r
1662 NHANH (CUTHE4 NOV2 ) THEN MESON_TAC[]);;\r
1663 \r
1664 (* ================== *)\r
1665 \r
1666 \r
1667 let A_LEMMA = prove(`!s v0 v1 v2.\r
1668      quasi_tri {v0, v1, v2} s\r
1669      ==> (!xx yy.\r
1670               ~(xx = yy) /\ {xx, yy} SUBSET {v1, v2, v0}\r
1671               ==> &2 <= dist (xx,yy) /\ dist (xx,yy) <= sqrt (&8)) /\\r
1672          ((!aa bb.\r
1673                aa IN {v1, v2, v0} /\ bb IN {v1, v2, v0}\r
1674                ==> dist (aa,bb) <= #2.51) \/\r
1675           (?aa bb.\r
1676                {aa, bb} SUBSET {v1, v2, v0} /\\r
1677                #2.51 < dist (aa,bb) /\\r
1678                (!x y.\r
1679                     ~({x, y} = {aa, bb}) /\ {x, y} SUBSET {v1, v2, v0}\r
1680                     ==> dist (x,y) <= #2.51)))`,\r
1681 REWRITE_TAC[ MESON[]` a /\ {v0, v1, v2} SUBSET s /\ c <=> ( a /\ {v0, v1, v2} \r
1682    SUBSET s) /\ c ` ] THEN NHANH (MESON[SET_RULE ` {x,y} SUBSET b /\ b SUBSET s ==> \r
1683   s x /\ s y `]` (!u v. s u /\ s v /\ ~(u = v) ==> &2 <= dist (u,v)) /\\r
1684      {v0, v1, v2} SUBSET s ==> (!xx yy.\r
1685               ~(xx = yy) /\ {xx, yy} SUBSET {v0, v1, v2}\r
1686               ==> &2 <= dist (xx,yy) ) `) THEN \r
1687 REWRITE_TAC[ quasi_tri; set_3elements; packing; MESON[] ` a /\ {v0, v1, v2} SUBSET s /\ c <=>\r
1688    ( a /\ {v0, v1, v2} SUBSET s)/\c` ] THEN \r
1689 NHANH (MESON[ SET_RULE ` x IN a /\ a SUBSET s ==> s x ` ] ` (!u v. s u /\ s v /\\r
1690    ~(u = v) ==> &2 <= dist (u,v)) /\ {v0, v1, v2} SUBSET s ==> (!x y.\r
1691           x IN {v0, v1, v2} /\ y IN {v0, v1, v2} /\ ~(x = y)\r
1692           ==> &2 <= dist (x,y))`) THEN PHA THEN \r
1693 REWRITE_TAC[ SET_RULE ` x IN {v0, v1, v2} /\ y IN {v0, v1, v2} /\ ~(x = y) <=> \r
1694   ~(x = y) /\ {x, y } SUBSET {v0, v1, v2}`] THEN \r
1695 REWRITE_TAC[ t0] THEN \r
1696 ONCE_REWRITE_TAC[ MESON[ MATCH_MP REAL_LT_RSQRT (REAL_ARITH ` (&2 * #1.255) pow 2 < &8 `); REAL_ARITH` a <= b /\ b < c ==> a <= c ` ]`\r
1697   d3 x y <= &2 * #1.255 <=> d3 x y <= &2 * #1.255 /\ d3 x y <= sqrt( &8 ) `] THEN \r
1698 REWRITE_TAC[ REAL_ARITH ` &2 * #1.255 = #2.51`] THEN \r
1699 NHANH ( MESON[d3; DIST_SYM; DIST_REFL; REAL_ARITH ` &0 <= #2.51 `]` (!x y.\r
1700           ~(x = y) /\ {x, y} SUBSET {v0, v1, v2}\r
1701           ==> d3 x y <= #2.51 /\ d3 x y <= sqrt (&8))\r
1702   ==> (!x y.\r
1703           {x, y} SUBSET {v0, v1, v2}\r
1704           ==> d3 x y <= #2.51 )`) THEN \r
1705 REWRITE_TAC[ GSYM d3] THEN REWRITE_TAC[ SET_RULE ` a IN s /\ b IN s <=>\r
1706    {a,b} SUBSET s `] THEN \r
1707 MESON_TAC[ SET_RULE` {v0, v1, v2} = {v1, v2, v0}`]);;\r
1708 \r
1709 \r
1710 \r
1711 let NOV1 = prove(` ! s v0 v1 v2 . (?v4. quasi_reg_tet ({v0, v1, v2} UNION {v4}) s)\r
1712  ==> (!xx yy.\r
1713           ~(xx = yy) /\ {xx, yy} SUBSET {v1, v2, v0}\r
1714           ==> &2 <= dist (xx,yy) /\ dist (xx,yy) <= sqrt (&8)) /\\r
1715      ((!aa bb.\r
1716            aa IN {v1, v2, v0} /\ bb IN {v1, v2, v0} ==> dist (aa,bb) <= #2.51) \/\r
1717       (?aa bb.\r
1718            {aa, bb} SUBSET {v1, v2, v0} /\\r
1719            #2.51 < dist (aa,bb) /\\r
1720            (!x y.\r
1721                 ~({x, y} = {aa, bb}) /\ {x, y} SUBSET {v1, v2, v0}\r
1722                 ==> dist (x,y) <= #2.51)))`, NHANH (CUTHE4 QUA_TET_IMPLY_QUA_TRI) THEN \r
1723 REPEAT GEN_TAC THEN MATCH_MP_TAC (MESON[]` (b ==> c) ==> a /\ b ==> c `) THEN \r
1724  REWRITE_TAC[ A_LEMMA]);;\r
1725 \r
1726 \r
1727 \r
1728 (* ================ *)\r
1729 \r
1730 \r
1731 \r
1732 (* ======= have added to database_more =========== *)\r
1733 \r
1734 \r
1735 \r
1736 let DOT_SUB_ADD = VECTOR_ARITH `! a b. b dot b - a dot a = (b - a) dot (b + a)` ;;\r
1737 \r
1738 let DIST_LT_HALF_PLANE = prove(`!x:real^A a:real^A b:real^A. \r
1739     dist(x,a) < dist(x,b) <=> &0 < (a - b) dot (&2 % x - (a + b))`,\r
1740 ABBREV_TAC ` an a b x = ((a:real^A) - b) dot (&2 % x - (a + b))` THEN \r
1741 REWRITE_TAC[dist; vector_norm] THEN \r
1742 REWRITE_TAC[MESON[DOT_POS_LE; SQRT_MONO_LT_EQ]` sqrt ( x dot x) < sqrt (y dot y) <=>\r
1743   x dot x < y dot y `] THEN \r
1744 REWRITE_TAC[DOT_LSUB; DOT_RSUB] THEN \r
1745 SIMP_TAC[DOT_SYM] THEN \r
1746 ONCE_REWRITE_TAC[ GSYM REAL_SUB_LT] THEN \r
1747 REWRITE_TAC[ REAL_ARITH ` x dot x -\r
1748      b dot x -\r
1749      (b dot x - b dot b) -\r
1750      (x dot x - a dot x - (a dot x - a dot a)) =\r
1751      &2 * (a dot x - b dot x) + b dot b - a dot a`] THEN \r
1752 REWRITE_TAC[GSYM DOT_LSUB; GSYM DOT_RMUL] THEN \r
1753 REWRITE_TAC[DOT_SUB_ADD; VECTOR_ARITH `(b - a) dot (b + a) = \r
1754   ( -- ( a - b) ) dot ( a + b) `] THEN \r
1755 REWRITE_TAC[VECTOR_ARITH ` (a - b) dot &2 % x + --(a - b) dot (a + b) = \r
1756   (a-b) dot ( &2 % x - (a+b))`] THEN \r
1757 ASM_REWRITE_TAC[REAL_ARITH ` a - &0 = a` ]);;\r
1758 \r
1759 \r
1760 let OR_IMP_EX = MESON[]` ! a b c. a \/ b ==> c <=> (a ==> c) /\ ( b ==> c)` ;;\r
1761 \r
1762 \r
1763 let HALF_PLANE_CONV = prove(`! a b:real^N.  convex { x| x | dist(x,a) < dist (x,b) }`,\r
1764 REWRITE_TAC[DIST_LT_HALF_PLANE; convex; IN_ELIM_THM] THEN \r
1765 REWRITE_TAC[VECTOR_ARITH ` &2 % (u % x + v % y) - (a + b) \r
1766    = u % ( &2 % x ) + v % ( &2 % y ) - &1 % (a + b )`] THEN \r
1767 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN SIMP_TAC[] THEN \r
1768 REWRITE_TAC[VECTOR_ARITH ` (a - b) dot (u % &2 % x +\r
1769    v % &2 % y - (u + v) % (a + b))  = u * (a - b) dot (&2 % x - (a + b))\r
1770    + v * (a - b) dot (&2 % y - (a + b))`] THEN \r
1771 REWRITE_TAC[REAL_ARITH` &0 <= u /\ &0 <= v /\ &1 = u + v <=>\r
1772      &0 = u /\ &1 = v \/ &0 < u /\ &0 <= v /\ &1 = u + v`] THEN \r
1773 KHANANG THEN \r
1774 REWRITE_TAC[OR_IMP_EX] THEN \r
1775 ONCE_REWRITE_TAC[ EQ_SYM_EQ] THEN SIMP_TAC[] THEN \r
1776 REWRITE_TAC[REAL_POLY_CLAUSES] THEN \r
1777 SIMP_TAC[ REAL_ARITH ` a + &0 = a `] THEN \r
1778 NHANH (MESON[REAL_LT_MUL]`  &0 < (a - b) dot (&2 % x - (a + b)) /\\r
1779      &0 < (a - b) dot (&2 % y - (a + b)) /\\r
1780      &0 < u  /\ l ==> &0 < u * ((a - b) dot (&2 % x - (a + b)))`) THEN \r
1781 NHANH (MESON[REAL_ARITH` &0 < a ==> &0 <= a `; REAL_LE_MUL]`\r
1782   &0 < (a - b) dot (&2 % y - (a + b)) /\\r
1783       &0 < u /\\r
1784       &0 <= v /\ l ==> &0 <= v * ((a - b) dot (&2 % y - (a + b)))`)\r
1785  THEN REAL_ARITH_TAC);;\r
1786 \r
1787 let HALF_PLANE_CONV_EP = REWRITE_RULE[convex; IN_ELIM_THM] HALF_PLANE_CONV;;\r
1788 \r
1789 let VORONOI_CONV = prove( ` ! (s:real^A -> bool) v. convex (voronoi v s )`,\r
1790 REWRITE_TAC[voronoi] THEN REPEAT GEN_TAC THEN \r
1791 REWRITE_TAC[convex; IN_ELIM_THM] THEN MESON_TAC[HALF_PLANE_CONV_EP]);;\r
1792 \r
1793 let CONVEX_IM_CONV2_SU = prove(`! s u v. convex s /\ u IN s /\ v IN s ==> conv {u,v} SUBSET s `,\r
1794 REWRITE_TAC[convex; CONV_SET2] THEN SET_TAC[]);;\r
1795 \r
1796 (* have not added *)\r
1797 \r
1798 let U_IN_CONV2 = prove(`! u v. u IN conv {u,v} `,\r
1799 REWRITE_TAC[ CONV_SET2; IN_ELIM_THM] THEN REPEAT GEN_TAC\r
1800 THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0 ` THEN \r
1801 REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN \r
1802 REAL_ARITH_TAC);;\r
1803 \r
1804 let UV_IN_CONV2 = prove(` ! u v. u IN conv {u,v} /\ v IN conv {u,v} `, \r
1805 MESON_TAC[U_IN_CONV2; SET_RULE ` {u,v} = {v,u} `]);;\r
1806 \r
1807 let CONVEX_AS_CONV2 = prove(` ! s. convex s ==> ( ! u v. u IN s /\ v IN s <=>\r
1808    conv {u,v} SUBSET s )`, REWRITE_TAC[ EQ_EXPAND] THEN \r
1809 SIMP_TAC[CONVEX_IM_CONV2_SU ] THEN MESON_TAC[SUBSET; UV_IN_CONV2]);;\r
1810 \r
1811 \r
1812 \r
1813 \r
1814 \r
1815 \r
1816 let CONV0_SING = prove(`! x:real^A . conv0 {x} = {x} `,\r
1817 REWRITE_TAC[conv0; FUN_EQ_THM; affsign; lin_combo] THEN \r
1818 REWRITE_TAC[UNION_EMPTY; VSUM_SING; SUM_SING; IN_ACT_SING; sgn_gt] THEN \r
1819 REWRITE_TAC[MESON[REAL_ARITH` &0 < &1 `]` (!w. x = w ==> &0 < f w) /\ \r
1820   f x = &1 <=> f x = &1 `] THEN \r
1821 REWRITE_TAC[MESON[VECTOR_MUL_LID]` (?f. x' = f x % x /\ f x = &1) <=>\r
1822    x' = x /\ (? f. f x = &1 ) `] THEN \r
1823 MESON_TAC[prove(`!x:real^A. ? f. f x = &1`, GEN_TAC THEN EXISTS_TAC \r
1824   `(\x:real^A. &1)` THEN MESON_TAC[])]);;\r
1825 \r
1826 \r
1827 let NOV10' = prove(`! x y.      (x = y\r
1828       ==> (!x. y = x <=>\r
1829                (?a b. &0 < a /\ &0 < b /\ a + b = &1 /\ x = a % y + b % y)))`,\r
1830 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN \r
1831 REWRITE_TAC[MESON[VECTOR_MUL_LID]` a + b = &1 /\\r
1832     x = (a + b) % y <=> a + b = &1 /\ x = y `] THEN \r
1833 MESON_TAC[prove(` ?a b. &0 < a /\ &0 < b /\ a + b = &1`, REPEAT \r
1834   (EXISTS_TAC ` &1 / &2 `) THEN REAL_ARITH_TAC)]);;\r
1835 \r
1836 \r
1837 let CONV0_SET2 = prove(` ! x y:real^A. conv0 {x,y} = {w | ? a b. &0 < a /\ &0 < b /\ a + b = &1 /\\r
1838   w = a%x + b%y}`,\r
1839 ONCE_REWRITE_TAC[ MESON[] ` (! a b. P a b ) <=> ( ! a b. a = b \/ ~( a= b)\r
1840   ==> P a b )`] THEN \r
1841 REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a==> c) /\ ( b==> c)`] THEN \r
1842 SIMP_TAC[] THEN \r
1843 REWRITE_TAC[ SET_RULE ` {a,a} = {a}`; CONV0_SING; FUN_EQ_THM; IN_ELIM_THM] THEN \r
1844 REWRITE_TAC[ IN_ACT_SING; NOV10'] THEN \r
1845 REWRITE_TAC[conv0 ; sgn_gt; affsign; lin_combo] THEN \r
1846 REWRITE_TAC[UNION_EMPTY; IN_SET2] THEN \r
1847 ONCE_REWRITE_TAC[ MESON[]`  ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>\r
1848   ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`] THEN \r
1849 REWRITE_TAC[ MESON[VSUM_DIS2; SUM_DIS2]` ~(x = y) /\\r
1850                     x' = vsum {x, y} ff /\ l /\ sum {x, y} f = &1 <=> ~(x = y) /\\r
1851                     x' = ff x + ff y /\ l /\ f x + f y = &1 `]  THEN \r
1852 REWRITE_TAC[ MESON[]` (!w. w = x \/ w = y ==> &0 < f w) <=> &0 < f x /\ &0 < f y`] THEN \r
1853 ONCE_REWRITE_TAC[ GSYM (MESON[]`  ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>\r
1854   ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`)] THEN \r
1855 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN \r
1856 REWRITE_TAC[ EQ_EXPAND] THEN \r
1857 SIMP_TAC[ MESON[]` ((?f. x' = f x % x + f y % y /\ (&0 < f x /\ &0 < f y) /\ f x + f y = &1)\r
1858   ==> (?a b. &0 < a /\ &0 < b /\ a + b = &1 /\ x' = a % x + b % y)) `] THEN \r
1859 STRIP_TAC THEN EXISTS_TAC ` (\(d:real^A). if d = x then (a:real) else b )` THEN \r
1860 ASM_SIMP_TAC[]);;\r
1861 \r
1862 \r
1863 let CONV02_SU_CONV2 = prove(` ! u v. conv0 {u,v} SUBSET conv {u,v} `,\r
1864 REWRITE_TAC[ CONV_SET2; CONV0_SET2] THEN \r
1865 MP_TAC (REAL_ARITH ` ! a . &0 < a ==> &0 <= a `) THEN SET_TAC[]);;\r
1866 \r
1867 \r
1868 let CONVEX_IM_CONV02_SU = prove(`! s u v. convex s /\ u IN s /\ v IN s ==> \r
1869 conv0 {u, v} SUBSET s`,\r
1870 MESON_TAC[CONV02_SU_CONV2; CONVEX_IM_CONV2_SU; SUBSET_TRANS]);;\r
1871 \r
1872 let PAIR_EQ_EXPAND =\r
1873  SET_RULE `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`;;\r
1874 \r
1875 let IN_SET3 = SET_RULE ` x IN {a,b,c} <=> x = a \/ x = b \/ x = c `;;\r
1876 \r
1877 let IN_SET4 = SET_RULE ` x IN {a,b,c,d} <=> x = a \/ x = b \/ x = c \/ x = d `;;\r
1878 \r
1879 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} ` ;;\r
1880 \r
1881 \r
1882 \r
1883 \r
1884 \r
1885 (* TAG 1 *)\r
1886 \r
1887 let DIA_OF_QUARTER = prove(`! a b q s. diagonal a b q s ==> &2 * t0 <= d3 a b /\ d3 a b \r
1888    <= sqrt (&8) `,\r
1889 REWRITE_TAC[ diagonal; quarter] THEN \r
1890 REWRITE_TAC[ SET_RULE ` {a,b} SUBSET s <=> a IN s /\ b IN s `] THEN \r
1891 REWRITE_TAC[ SET_RULE ` {a,b} SUBSET s <=> a IN s /\ b IN s `; t0] THEN \r
1892 MESON_TAC[PAIR_D3; MATCH_MP REAL_LE_RSQRT (REAL_ARITH ` (&2 * #1.255) pow 2 <= &8 `);\r
1893   REAL_ARITH ` a <= b /\ b <= c ==> a <= c `]);;\r
1894 \r
1895 let D3_REFL = prove(` !x. d3 x x = &0 ` , MESON_TAC[d3; DIST_REFL]);;\r
1896 \r
1897 let db_t0_sq8 = MATCH_MP REAL_LT_RSQRT (REAL_ARITH ` #2.51 pow 2 < &8 `);;\r
1898 \r
1899 let def_obstructed = prove(`!s x y.\r
1900      obstructed x y s <=>\r
1901      (?bar. bar IN barrier s /\ ~(conv0 {x, y} INTER conv bar = {}))`,\r
1902   REWRITE_TAC[ obstructed; conv0_2] THEN REWRITE_TAC[ simp_def]);;\r
1903 \r
1904 let SUB_PACKING = prove(`!sub s.\r
1905      packing s /\ sub SUBSET s\r
1906      ==> (!x y. x IN sub /\ y IN sub /\ ~(x = y) ==> &2 <= d3 x y)`,\r
1907 REWRITE_TAC[ packing; GSYM d3] THEN SET_TAC[]);;\r
1908 \r
1909 \r
1910 \r
1911 \r
1912 let SHORT_EDGES = prove(` ! a b c w. d3 c a <= &2 * t0 /\\r
1913  d3 c b <= &2 * t0 /\\r
1914  (!aa. aa IN {a, b, c} ==> d3 aa w <= &2 * t0)\r
1915  ==> (!x y.\r
1916           x IN {a, b, c, w} /\ y IN {a, b, c, w} /\ ~({x, y} = {a, b})\r
1917           ==> d3 x y <= &2 * t0)`,\r
1918 REPEAT GEN_TAC THEN \r
1919 REWRITE_TAC[ IN_SET3; IN_SET4; PAIR_EQ_EXPAND; t0] THEN \r
1920 MESON_TAC[ D3_REFL; trg_d3_sym; REAL_ARITH ` &0 <= &2 * #1.255`]);;\r
1921 \r
1922 \r
1923 \r
1924 (* == CARD ASSERTIONN == *)\r
1925 (* changing truong *)\r
1926 \r
1927 let OBS_SYM = prove(` ! a b s. obstructed a b s <=> obstructed b a s `, \r
1928  REWRITE_TAC[ def_obstructed] THEN SIMP_TAC[ SET_RULE` {a,b} = {b,a}`]);;\r
1929 \r
1930 (* need VC *)\r
1931 let OBS_IMP_NOT_IN_VC = prove(`!x w s. obstructed x w s ==> ~(x IN VC w s \/ w IN VC x s)`,\r
1932 REWRITE_TAC[VC; lambda_x; IN_ELIM_THM] THEN MESON_TAC[ OBS_SYM]);;\r
1933 \r
1934 \r
1935 let IN_Q_IMP_BAR = \r
1936 prove(` {v0, v1, v2, w} IN Q_SYS s ==> {v0,v1,v2} IN barrier s `, \r
1937 REWRITE_TAC[ barrier; SET_RULE` {a,b,c} UNION {d} = {a,b,c,d} `; IN_ELIM_THM]\r
1938  THEN MESON_TAC[]);;\r
1939 \r
1940 \r
1941 let v_near2t0_v = MESON[near2t0; t0; DIST_REFL; SET_RULE ` x IN { x | P x} <=> P x ` ;\r
1942  REAL_ARITH ` &0 < &2 * #1.255 `] ` w IN s  ==>  w IN near2t0 w s  `;;\r
1943 \r
1944 (* need VC *)\r
1945 let in_VC = prove( \r
1946 `!w s x.\r
1947      w IN s /\\r
1948      dist (w,x) < &2 /\\r
1949      (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\\r
1950      ~obstructed w x s\r
1951      ==> x IN VC w s`, REWRITE_TAC[ VC; lambda_x ; d3; IN_ELIM_THM] THEN \r
1952   MESON_TAC[ DIST_SYM; SET_RULE ` i IN x <=> x i `]);;\r
1953 \r
1954 \r
1955 let MEETING_CONDITION = prove(` ! x y v1 v2 v3. ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\ dist (x,y) < t0\r
1956  ==> ~(normball x #1.255 INTER conv {v1, v2, v3} = {})`,\r
1957 REWRITE_TAC[ GSYM conv0_2; simp_def] THEN \r
1958 REWRITE_TAC[ SET_RULE ` ~( a INTER b = {} ) <=> (? d. d IN   a /\ d IN b )`;\r
1959   IN_ELIM_THM] THEN \r
1960 NHANH (MESON[ VECTOR_ARITH ` x = &1 % x ` ]` d = t % x + (&1 - t) % y ==> \r
1961   x = &1 % x `) THEN \r
1962 NHANH (VECTOR_ARITH ` d = t % x + (&1 - t) % y /\ x = &1 % x\r
1963      ==> d - x = (t - &1) % ( x - y)`) THEN \r
1964 NHANH ( MESON[NORM_MUL]` d - x = (t - &1) % (x - y) ==> norm ( d - x ) = \r
1965   abs ( t- &1 ) * norm ( x-y)`) THEN \r
1966 REWRITE_TAC[ GSYM dist] THEN \r
1967 NHANH (REAL_ARITH `&0 < t /\ t < &1 /\ aa ==> abs (t - &1) < &1`) THEN \r
1968 NHANH (MESON[DIST_POS_LE]` dist (d,x) = abs (t - &1) * dist (x,y) ==> &0 <= dist(x,y)`) THEN \r
1969 PHA THEN \r
1970 REWRITE_TAC[ REAL_ARITH ` abs (t - &1) < &1 <=> &0 < &1 - abs (t - &1) `] THEN \r
1971 NHANH (MESON[REAL_LE_MUL_EQ] ` &0 <= dist (x,y) /\\r
1972                &0 < &1 - abs (t - &1) ==>  &0 <= dist (x,y) * (&1 - abs (t - &1))`) THEN \r
1973 REWRITE_TAC[ REAL_ARITH ` a * (  b - c ) = a * b - a * c `] THEN \r
1974 REWRITE_TAC[ REAL_ARITH ` &0 <= a - b <=> b <= a `] THEN \r
1975 NHANH (REAL_ARITH ` dist (d,x) = abs (t - &1) * dist (x,y) /\\r
1976                (&0 <= dist (x,y) /\ &0 < &1 - abs (t - &1)) /\\r
1977                dist (x,y) * abs (t - &1) <= dist (x,y) * &1\r
1978   ==> dist(d,x) <= dist(x,y)`) THEN \r
1979 NGOAC THEN NHANH (MESON[]`(? d . ( ? t. PP t d /\ dist (d,x) <= dist (x,y)) /\ aa d )  ==> (? d. dist (d,x)\r
1980    <= dist (x,y) /\ aa d ) `) THEN \r
1981 PHA THEN REPEAT GEN_TAC THEN \r
1982 MATCH_MP_TAC (MESON[] ` (b /\ c ==> d) ==> ( a/\ b/\ c )==> d `) THEN \r
1983 REWRITE_TAC[normball; IN_ELIM_THM; GSYM t0] THEN \r
1984 REWRITE_TAC[ MESON[]` (? a . P a ) /\ aa <=> (? a. aa /\ P a ) `] THEN \r
1985 MESON_TAC[ REAL_ARITH ` a < b /\ c <= a ==> c < b `]);;\r
1986 \r
1987 \r
1988 (* needs VC *)\r
1989 let VC_DISJOINT = prove ( `! s a b. ( ~( a = b ) ==> VC a s INTER VC b s = {}) /\ \r
1990                                                      VC a s INTER VC_INFI s = {} `, \r
1991 REWRITE_TAC[ VC_INFI; SET_RULE ` VC a s INTER {z | !x. ~(z IN VC x s)} = {} `] THEN \r
1992 REWRITE_TAC[ VC; lambda_x ] THEN \r
1993 REWRITE_TAC[ SET_RULE` a INTER b = {} <=> (! x. ~( x IN a /\ x IN b ))`] THEN \r
1994 REWRITE_TAC[ SET_RULE ` x IN { x | p x } <=> p x `] THEN \r
1995 REWRITE_TAC[ MESON[] ` ! a P. a ==> (!x. ~P x) <=> a ==> (!x. ~a \/ ~P x) `] THEN \r
1996 REWRITE_TAC[ MESON[] ` a = b \/\r
1997      ~(((a IN s /\ d3 a x < &2 /\ ~obstructed a x s) /\\r
1998         (!w. (w IN s /\ d3 w x < &2 /\ ~obstructed w x s) /\ ~(w = a)\r
1999              ==> d3 x a < d3 x w)) /\\r
2000        (b IN s /\ d3 b x < &2 /\ ~obstructed b x s) /\\r
2001        (!w. (w IN s /\ d3 w x < &2 /\ ~obstructed w x s) /\ ~(w = b)\r
2002             ==> d3 x b < d3 x w)) <=>\r
2003      ~(~(a = b) /\\r
2004        ((a IN s /\ d3 a x < &2 /\ ~obstructed a x s) /\\r
2005         (!w. (w IN s /\ d3 w x < &2 /\ ~obstructed w x s) /\ ~(w = a)\r
2006              ==> d3 x a < d3 x w)) /\\r
2007        (b IN s /\ d3 b x < &2 /\ ~obstructed b x s) /\\r
2008        (!w. (w IN s /\ d3 w x < &2 /\ ~obstructed w x s) /\ ~(w = b)\r
2009             ==> d3 x b < d3 x w)) `] THEN PHA THEN \r
2010 MESON_TAC[ REAL_ARITH ` ! a b. ~( a < b /\ b < a ) `]);;\r
2011 \r
2012 \r
2013 let DIAGONAL_STRICT_QUA = prove(` !a b q s.\r
2014      a IN q /\ b IN q /\ &2 * t0 < d3 a b /\ strict_qua q s\r
2015      ==> diagonal a b q s`,\r
2016 REWRITE_TAC[ SET_RULE ` a IN q /\ b IN q /\ l ==> aa /\ {a,b} SUBSET q /\ bb\r
2017   <=> a IN q /\ b IN q /\ l ==> aa /\ bb `] THEN \r
2018 REWRITE_TAC[ MESON[]` a /\ b/\ c /\ d /\ e ==> d /\ f <=> a /\ b/\ c /\ d /\ e ==> f `] THEN \r
2019 MESON_TAC[strict_qua; DIAGONAL_QUA]);;\r
2020 \r
2021 (* ========== *) \r
2022 \r
2023 let DIAGONAL_BARRIER = prove(` ! s v1 v2 bar .v1 IN bar /\ v2 IN bar /\ bar IN barrier s /\ &2 * t0 < d3 v1 v2 \r
2024   ==> (? w. diagonal v1 v2 ( w INSERT bar ) s )`,\r
2025 REWRITE_TAC[ barrier; IN_ELIM_THM] THEN \r
2026 PHA THEN REWRITE_TAC[ MESON[] ` a /\ b /\ (? u v w. P u v w ) /\ d <=>\r
2027   (? u v w. P u v w /\ a /\ b /\ d ) `] THEN \r
2028 KHANANG THEN \r
2029 REWRITE_TAC[ MESON[]` (? a b c. P a b c) /\ l <=> (?a b c. P a b c /\ l)`] THEN \r
2030 REWRITE_TAC[ quasi_tri; t0] THEN \r
2031 NHANH ( REAL_ARITH ` &2 * #1.255 < a ==> ~( a = &0 ) `) THEN \r
2032 REWRITE_TAC[d3; DIST_EQ_0] THEN \r
2033 NGOAC THEN \r
2034 PURE_ONCE_REWRITE_TAC[ MESON[]` P {a,b,c} /\ bar = {a,b,c} <=> P bar /\ bar \r
2035   = {a,b,c} `] THEN \r
2036 REWRITE_TAC[quasi_tri; REAL_ARITH ` a <= b <=> ~( b < a ) `] THEN PHA THEN \r
2037 REWRITE_TAC[ MESON[]` ~((!x y.\r
2038             x IN bar /\ y IN bar /\ ~(x = y) ==> ~(&2 * #1.255 < dist (x,y))) /\\r
2039        aaa /\\r
2040        v1 IN bar /\\r
2041        v2 IN bar /\\r
2042        &2 * #1.255 < dist (v1,v2) /\\r
2043        ~(v1 = v2))`] THEN \r
2044 NHANH (CUTHE2 CASES_OF_Q_SYS) THEN \r
2045 REWRITE_TAC[ MESON[]` (? a . P a ) /\ l <=> (? a. P a /\ l ) `] THEN \r
2046 KHANANG THEN \r
2047 PURE_ONCE_REWRITE_TAC[ MESON[]` P bar /\ bar = s /\ l <=> P s /\ bar = s /\ l`] THEN \r
2048 NHANH (MESON[QUA_TET_IMPLY_QUA_TRI] ` quasi_reg_tet ({v0, v1, v2} UNION {v4}) s ==>\r
2049   quasi_tri {v0, v1, v2} s`) THEN \r
2050 REWRITE_TAC[ quasi_tri] THEN \r
2051 REWRITE_TAC[d3;t0; REAL_ARITH ` a <= &2 * #1.255 <=> ~(&2 * #1.255 < a ) `] THEN PHA THEN \r
2052 REWRITE_TAC[ MESON[]` ~((!x y.\r
2053             x IN {v1', v2', v3} /\ y IN {v1', v2', v3} /\ ~(x = y)\r
2054             ==> ~(&2 * #1.255 < dist (x,y))) /\\r
2055        bar = {v1', v2', v3} /\\r
2056        v1 IN bar /\\r
2057        v2 IN bar /\\r
2058        &2 * #1.255 < dist (v1,v2) /\\r
2059        ~(v1 = v2))`] THEN \r
2060 REWRITE_TAC[ GSYM d3; GSYM t0] THEN \r
2061 REWRITE_TAC[ MESON[]` strict_qua ({v1', v2', v3} UNION {v4}) s /\ bar = {v1', v2', v3} /\ l <=>\r
2062      strict_qua (bar UNION {v4}) s /\ bar = {v1', v2', v3} /\ l`] THEN \r
2063 ONCE_REWRITE_TAC[ SET_RULE ` bar UNION {v4} = v4 INSERT bar `] THEN \r
2064 MESON_TAC[ DIAGONAL_STRICT_QUA; SET_RULE ` x IN bar ==> x IN ( a INSERT bar)`]);;\r
2065 \r
2066 \r
2067 (* ======= end simplizee.ml =========== *)\r
2068 \r
2069 (* ======= im_le_82.ml ================ *)\r
2070 \r
2071 let quasi_tri_case = prove( ` ! s x y. (?v1 v2 v3.\r
2072       ~(x IN {v1, v2, v3}) /\\r
2073       quasi_tri {v1, v2, v3} s /\\r
2074       ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\\r
2075       dist (x,y) < t0)\r
2076  ==> (?v1 v2 v3.\r
2077           packing s /\\r
2078           ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\\r
2079           dist (v1,v2) <= #2.51 /\\r
2080           dist (v2,v3) <= #2.51 /\\r
2081           dist (v3,v1) < sqrt (&8) /\\r
2082           {v1, v2, v3} SUBSET s /\\r
2083           ~(x IN {v1, v2, v3}) /\\r
2084           ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\\r
2085           dist (x,y) < t0)`,\r
2086 REWRITE_TAC[ quasi_tri; set_3elements] THEN PHA THEN \r
2087  REWRITE_TAC[ d3; MESON[t0; REAL_ARITH ` &2 * #1.255 = #2.51 `] ` &2 * t0 = #2.51 `] THEN \r
2088 REWRITE_TAC[ MESON[]` a /\ b /\ c /\ d /\e /\ f <=> a /\ b /\ c /\ (d /\e) /\ f`] THEN \r
2089 ONCE_REWRITE_TAC[ SET_RULE ` ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\\r
2090           (!x y.\r
2091                x IN {v1, v2, v3} /\ y IN {v1, v2, v3} /\ ~(x = y)\r
2092                ==> dist (x,y) <= #2.51)\r
2093   <=> ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\\r
2094           (!x y.\r
2095                x IN {v1, v2, v3} /\ y IN {v1, v2, v3} /\ ~(x = y)\r
2096                ==> dist (x,y) <= #2.51) /\\r
2097    dist (v1,v2) <= #2.51 /\\r
2098               dist (v2,v3) <= #2.51 /\\r
2099               dist (v3,v1) <= #2.51 `] THEN \r
2100 ONCE_REWRITE_TAC[MESON[ REAL_ARITH ` &2 * #1.255 = #2.51 `; MATCH_MP REAL_LT_RSQRT (REAL_ARITH `(&2 * #1.255) pow 2 < &8`); \r
2101   REAL_ARITH` a <= b /\ b < c ==> a < c `] `\r
2102   a /\ dist (v3,v1) <= #2.51 <=> a /\ dist (v3,v1) < sqrt ( &8 ) /\ dist (v3,v1) <= #2.51`] THEN \r
2103  MESON_TAC[]);;\r
2104 \r
2105 \r
2106 \r
2107 (* ----------- have added to database_more --------------*)\r
2108 \r
2109 \r
2110 \r
2111 let OCT23 = prove(`! s v1 v2 v3 v4.\r
2112      {v1, v2, v3} UNION {v4} IN Q_SYS s\r
2113      ==> packing s /\\r
2114          ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\\r
2115          {v1, v2, v3} SUBSET s` ,\r
2116 REPEAT GEN_TAC THEN MP_TAC (prove(`! q s. q IN Q_SYS s ==> quasi_reg_tet q s \/ strict_qua q s \/ \r
2117 (?v v1 v3 v2 v4.\r
2118                    (q = {v, v1, v2, v3} \/ q = {v, v1, v3, v4}) /\\r
2119                    interior_pos v v1 v3 v2 v4 s /\\r
2120                    anchor_points v1 v3 s = {v, v2, v4} /\\r
2121                    anchor_points v2 v4 s = {v, v1, v3})`,\r
2122 REWRITE_TAC[ Q_SYS; IN_ELIM_THM] THEN MESON_TAC[strict_qua_in_oct] )) THEN \r
2123 MATCH_MP_TAC (MESON[]`((!q s. q IN Q_SYS s ==> R q s)\r
2124       ==> R ({v1, v2, v3} UNION {v4}) s\r
2125       ==> last v1 v2 v3 s)\r
2126      ==> (!q s. q IN Q_SYS s ==> R q s)\r
2127      ==> {v1, v2, v3} UNION {v4} IN Q_SYS s\r
2128      ==> last v1 v2 v3 s`) THEN \r
2129 DISCH_TAC THEN \r
2130 REWRITE_TAC[ quasi_reg_tet; strict_qua ] THEN \r
2131  PHA THEN KHANANG  THEN \r
2132 REWRITE_TAC[ quarter] THEN \r
2133 PHA THEN \r
2134 REWRITE_TAC[ MESON[]` packing s /\simplex ({v1, v2, v3} UNION {v4}) s /\ last <=> \r
2135    simplex ({v1, v2, v3} UNION {v4}) s /\ packing s /\ last`] THEN \r
2136 REWRITE_TAC[ SET_RULE ` {v1, v2, v3} UNION {v4} = { v1, v2, v3, v4} `] THEN \r
2137 MP_TAC (MESON[ def_simplex; SET_RULE ` {a, b, c, d} SUBSET s ==> {a, b, c} SUBSET s `] `\r
2138   simplex {v1, v2, v3, v4} s ==> packing s /\ ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\ {v1, v2, v3} SUBSET s `) THEN \r
2139 MATCH_MP_TAC (MESON[]` (cc ==> last)\r
2140      ==> (aa ==> last)\r
2141      ==> aa /\ la1 \/ aa /\ la2 \/ cc\r
2142      ==> last`) THEN \r
2143 REWRITE_TAC[ MESON[]` a = b /\ (aa /\ bb b s) /\ last <=> bb a s /\ aa /\ a = b /\ last`] THEN \r
2144 REWRITE_TAC[def_simplex] THEN \r
2145 ONCE_REWRITE_TAC[ MESON[simplex_interior_pos]` interior_pos v v1 v3 v2 v4 s <=> interior_pos v v1 v3 v2 v4 s\r
2146               /\ simplex {v, v1, v3, v2} s /\\r
2147                simplex {v, v1, v3, v4} s /\\r
2148                simplex {v, v2, v4, v1} s /\\r
2149                simplex {v, v2, v4, v3} s `] THEN PHA THEN \r
2150 REWRITE_TAC[ MESON[]` {v1, v2, v3, v4} = {v, v1', v2', v3'} /\\r
2151       aa /\  simplex {v, v1', v3', v2'} s /\ ss\r
2152   <=> ( simplex {v, v1', v3', v2'} s /\ {v1, v2, v3, v4} = {v, v1', v2', v3'}) /\ aa /\ ss `] THEN \r
2153 REWRITE_TAC[ MESON[SET_RULE ` {v, v1, v2 , v3} = {v, v1, v3, v2} ` ] ` \r
2154   (simplex {v, v1', v3', v2'} s /\ {v1, v2, v3, v4} = {v, v1', v2', v3'}) /\ ff <=>\r
2155   simplex {v1, v2, v3, v4} s /\ {v1, v2, v3, v4} = {v, v1', v2', v3'} /\ ff`] THEN \r
2156 MESON_TAC[ def_simplex; SET_RULE ` {v1, v2, v3, v4} SUBSET s ==> {v1, v2, v3} SUBSET s`]);;\r
2157 \r
2158 \r
2159 (* ================== *)\r
2160 \r
2161 \r
2162 let OCT24 = prove(`! s x y.  (?v1 v2 v3.\r
2163       ~(x IN {v1, v2, v3}) /\\r
2164       (?v4. (!vv1 vv2 vv3.\r
2165                  {vv1, vv2, vv3} = {v1, v2, v3} ==> ~(#2.51 < dist (vv3,vv1))) /\\r
2166             {v1, v2, v3} UNION {v4} IN Q_SYS s) /\\r
2167       ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\\r
2168       dist (x,y) < t0) ==>\r
2169 (?v1 v2 v3.\r
2170           packing s /\\r
2171           ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\\r
2172           dist (v1,v2) <= #2.51 /\\r
2173           dist (v2,v3) <= #2.51 /\\r
2174           dist (v3,v1) < sqrt (&8) /\\r
2175           {v1, v2, v3} SUBSET s /\\r
2176           ~(x IN {v1, v2, v3}) /\\r
2177           ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\\r
2178           dist (x,y) < t0)`,\r
2179 ONCE_REWRITE_TAC[ MESON[OCT23] ` {v1, v2, v3} UNION {v4} IN Q_SYS s <=>\r
2180   {v1, v2, v3} UNION {v4} IN Q_SYS s /\ packing s /\\r
2181              ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\\r
2182              {v1, v2, v3} SUBSET s `] THEN \r
2183 ONCE_REWRITE_TAC[ MESON[ SET_RULE` {v1, v3 , v2 } = { v1, v2 , v3} /\ { v2, v1, v3 } = { v1, v2, v3 }`]`\r
2184   (!vv1 vv2 vv3.\r
2185           {vv1, vv2, vv3} = {v1, v2, v3} ==> ~(#2.51 < dist (vv3,vv1)))\r
2186      <=> (!vv1 vv2 vv3.\r
2187           {vv1, vv2, vv3} = {v1, v2, v3} ==> ~(#2.51 < dist (vv3,vv1))) /\ ~(#2.51 < dist (v3,v1)) /\\r
2188          ~(#2.51 < dist (v2,v1)) /\\r
2189          ~(#2.51 < dist (v3,v2)) `] THEN \r
2190 REWRITE_TAC[ REAL_ARITH ` ~( a < b ) <=> b <= a`] THEN SIMP_TAC[ DIST_SYM] THEN \r
2191 MESON_TAC[MESON[ MATCH_MP REAL_LT_RSQRT (REAL_ARITH `(&2 * #1.255) pow 2 < &8`);\r
2192   REAL_ARITH ` &2 * #1.255 = #2.51 /\ ( a <= b /\ b < c ==> a < c ) `]` dist (v1,v3) <= #2.51\r
2193   <=> dist (v1,v3) <= #2.51 /\ dist (v1,v3) < sqrt (&8) `]);;\r
2194 \r
2195 \r
2196 \r
2197 (* ============= *)\r
2198 \r
2199 \r
2200 let quasi_reg_tet_case = prove (`! s x y. (?v1 v2 v3.\r
2201        (?v4 vv1 vv2 vv3.\r
2202             {vv1, vv2, vv3} = {v1, v2, v3} /\\r
2203             #2.51 < dist (vv3,vv1) /\\r
2204             {v1, v2, v3} UNION {v4} IN Q_SYS s /\\r
2205             quasi_reg_tet ({v1, v2, v3} UNION {v4}) s) /\\r
2206        ~(x IN {v1, v2, v3}) /\\r
2207        ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}))\r
2208   ==> (?v1 v2 v3.\r
2209            packing s /\\r
2210            ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\\r
2211            dist (v1,v2) <= #2.51 /\\r
2212            dist (v2,v3) <= #2.51 /\\r
2213            dist (v3,v1) < sqrt (&8) /\\r
2214            {v1, v2, v3} SUBSET s /\\r
2215            ~(x IN {v1, v2, v3}) /\\r
2216            ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}))`,\r
2217 REWRITE_TAC[quasi_reg_tet; SET_RULE ` {v1, v2, v3} UNION {v4} = {v1, v2, v3, v4} `; def_simplex] THEN \r
2218 REWRITE_TAC[ MESON[]` (packing s /\\r
2219            {v1, v2, v3, v4} SUBSET s /\\r
2220            ~(v1 = v2 \/ v1 = v3 \/ v1 = v4 \/ v2 = v3 \/ v2 = v4 \/ v3 = v4)) /\ a <=>\r
2221   a /\  ~(v1 = v2 \/ v1 = v3 \/ v1 = v4 \/ v2 = v3 \/ v2 = v4 \/ v3 = v4) /\ (packing s /\\r
2222            {v1, v2, v3, v4} SUBSET s\r
2223           ) `] THEN \r
2224 ONCE_REWRITE_TAC[ ATTACH (MESON[ SET_RULE` v1 IN {v1, v2, v3, v4} /\ v2 IN { v1, v2, v3, v4} /\ v3 IN { v1, v2, v3, v4} `] `\r
2225   (!v w.\r
2226                v IN {v1, v2, v3, v4} /\ w IN {v1, v2, v3, v4} /\ ~(v = w)\r
2227                ==> d3 v w <= &2 * t0) /\\r
2228           ~(v1 = v2 \/ v1 = v3 \/ v1 = v4 \/ v2 = v3 \/ v2 = v4 \/ v3 = v4) /\last\r
2229   ==> d3 v1 v2 <= &2 * t0 /\ d3 v2 v3 <= &2 * t0 /\ d3 v3 v1 <= &2 * t0 `)] THEN \r
2230 REWRITE_TAC[ t0; GSYM d3;  REAL_ARITH ` &2 * #1.255  = #2.51 `] THEN \r
2231 ONCE_REWRITE_TAC[ ATTACH (MESON[ MATCH_MP REAL_LT_RSQRT (REAL_ARITH `(&2 * #1.255) pow 2 < &8`) ; REAL_ARITH ` &2 * #1.255 = #2.51 /\ ( a <= b /\ b < c ==> a < c ) `]\r
2232   ` d3 v1 v2 <= #2.51 /\\r
2233           d3 v2 v3 <= #2.51 /\\r
2234           d3 v3 v1 <= #2.51 ==> d3 v3 v1 < sqrt (&8) `)] THEN \r
2235 MESON_TAC[ SET_RULE ` {v1, v2, v3, v4} SUBSET s ==> {v1, v2, v3} SUBSET s`]);;\r
2236 \r
2237 let DIST_PAIR_LEMMA = prove\r
2238  (`{a,b} = {c,d} ==> dist(a,b) = dist(c,d)`,\r
2239  REWRITE_TAC[PAIR_EQ_EXPAND] THEN MESON_TAC[DIST_SYM]);;\r
2240 \r
2241 let OTHER_LEMMA = prove\r
2242  (`!a:real^3 b c d.\r
2243          (?v w.\r
2244               v IN {a, b, c, d} /\\r
2245               w IN {a, b, c, d} /\\r
2246               &2 * t0 <= d3 v w /\\r
2247               d3 v w <= sqrt (&8) /\\r
2248               (!x y.\r
2249                    x IN {a, b, c, d} /\\r
2250                    y IN {a, b, c, d} /\\r
2251                    ~(x = v /\ y = w \/ x = w /\ y = v)\r
2252                    ==> d3 x y <= &2 * t0)) /\\r
2253          (?x y.\r
2254               x IN {a, b, c, d} /\\r
2255               y IN {a, b, c, d} /\\r
2256               &2 * t0 < d3 x y /\\r
2257               d3 x y < sqrt (&8)) /\\r
2258          &2 * t0 < d3 d b\r
2259          ==> &2 * t0 < d3 d b /\\r
2260              d3 d b < sqrt (&8) /\\r
2261              (!x y.\r
2262                   x IN {a, b, c, d} /\\r
2263                   y IN {a, b, c, d} /\\r
2264                   ~({x, y} = {d, b})\r
2265                   ==> d3 x y <= &2 * t0)`, REWRITE_TAC [d3] THEN \r
2266  REPEAT GEN_TAC THEN REWRITE_TAC[t0; CONJ_ASSOC] THEN\r
2267  DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN\r
2268  REWRITE_TAC[GSYM CONJ_ASSOC; GSYM PAIR_EQ_EXPAND] THEN\r
2269  REWRITE_TAC[LEFT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN\r
2270  MAP_EVERY X_GEN_TAC [`v:real^3`; `w:real^3`] THEN\r
2271  DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN\r
2272  ASM_CASES_TAC `{v,w} = {d,b:real^3}` THENL\r
2273   [FIRST_ASSUM(SUBST_ALL_TAC o MATCH_MP DIST_PAIR_LEMMA) THEN\r
2274    FIRST_X_ASSUM SUBST_ALL_TAC;\r
2275    FIRST_X_ASSUM(MP_TAC o SPECL [`d:real^3`; `b:real^3`]) THEN\r
2276    ASM_REWRITE_TAC[GSYM REAL_NOT_LT; IN_INSERT]] THEN\r
2277  ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN\r
2278  MAP_EVERY X_GEN_TAC [`x:real^3`; `y:real^3`] THEN STRIP_TAC THEN\r
2279  FIRST_X_ASSUM(MP_TAC o SPECL [`x:real^3`; `y:real^3`]) THEN\r
2280  ASM_REWRITE_TAC[GSYM REAL_NOT_LT] THEN ASM_MESON_TAC[DIST_PAIR_LEMMA]);;\r
2281 \r
2282 \r
2283 (* ======OCT 23====== *)\r
2284 \r
2285 let hard_case = prove(`! s x y.  (?v1 v2 v3.\r
2286        (?v4 vv1 vv2 vv3.\r
2287             {vv1, vv2, vv3} = {v1, v2, v3} /\\r
2288             #2.51 < dist (vv3,vv1) /\\r
2289             {v1, v2, v3} UNION {v4} IN Q_SYS s /\\r
2290             strict_qua ({v1, v2, v3} UNION {v4}) s) /\\r
2291        ~(x IN {v1, v2, v3}) /\\r
2292        ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}))\r
2293   ==> (?v1 v2 v3.\r
2294            packing s /\\r
2295            ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\\r
2296            dist (v1,v2) <= #2.51 /\\r
2297            dist (v2,v3) <= #2.51 /\\r
2298            dist (v3,v1) < sqrt (&8) /\\r
2299            {v1, v2, v3} SUBSET s /\\r
2300            ~(x IN {v1, v2, v3}) /\\r
2301            ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}))`,\r
2302 REWRITE_TAC[ SET_RULE ` {v1, v2, v3} UNION { v4} = { v1, v2, v3 , v4} `;\r
2303   strict_qua] THEN \r
2304 REWRITE_TAC [ REAL_ARITH ` #2.51 = &2 * #1.255`] THEN \r
2305 PURE_ONCE_REWRITE_TAC[ MESON[]` (?v4 v1 v2 v3. P v4 v1 v2 v3) <=> (?a b c d. P a b c d)`] THEN \r
2306 ONCE_REWRITE_TAC[MESON[SET_RULE ` {b, c, d} = {v1, v2, v3} ==> {v1, v2, v3, a} = { a, b, c ,d }`]\r
2307   ` (? a b c d. {b, c, d} = {v1, v2, v3} /\ P a b c d v1 v2 v3 {v1, v2, v3, a} )\r
2308   <=> (? a b c d. {b, c, d} = {v1, v2, v3} /\ P a b c d v1 v2 v3 { a, b, c ,d })`] THEN \r
2309 REWRITE_TAC[quarter] THEN \r
2310 REWRITE_TAC[quarter;def_simplex] THEN PHA THEN \r
2311 REWRITE_TAC[MESON[]`&2 * #1.255 < dist (d,b) /\ a <=> a /\ &2 * #1.255 < dist (d,b)`] THEN PHA THEN \r
2312 REWRITE_TAC[ GSYM t0; GSYM d3] THEN \r
2313 REWRITE_TAC[ SET_RULE ` ~({a, b} = {c, d}) <=> ~(a = c /\ b = d \/ a = d /\ b = c)`] THEN \r
2314 NHANH (MATCH_MP (MESON[]` (! a b c d. P a b c d ) ==> P a b c d`) OTHER_LEMMA ) THEN PHA THEN \r
2315 PURE_ONCE_REWRITE_TAC[ MESON[]` ~(a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d)\r
2316   /\ aa <=> aa /\ ~(a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d)`] THEN PHA THEN \r
2317 NHANH (SET_RULE ` ~(a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d)\r
2318   ==> ~({b, c} = {d,b} ) /\ ~({c,d} = {d,b})`) THEN \r
2319 NHANH (SET_RULE` ~({b, c} = {d, b}) /\\r
2320                ~({c, d} = {d, b}) ==> b IN {a, b, c, d} /\\r
2321   c IN {a, b, c, d} /\ d IN {a, b, c, d} `) THEN PHA THEN \r
2322 NHANH (MESON[]` (!x y.\r
2323           x IN {a, b, c, d} /\ y IN {a, b, c, d} /\ ~({x, y} = {d, b})\r
2324           ==> d3 x y <= &2 * t0) /\\r
2325      aaa /\\r
2326      ~({b, c} = {d, b}) /\\r
2327      ~({c, d} = {d, b}) /\\r
2328      b IN {a, b, c, d} /\\r
2329      c IN {a, b, c, d} /\\r
2330      d IN {a, b, c, d}\r
2331      ==> d3 b c <= &2 * t0 /\ d3 c d <= &2 * t0`) THEN \r
2332 REWRITE_TAC[ MESON[]`{b, c, d} = {v1, v2, v3} /\ a <=> a /\ {b, c, d} = {v1, v2, v3} `] THEN \r
2333 PHA THEN REWRITE_TAC[ MESON[]`{a, b, c, d} SUBSET s /\ aa <=> aa /\ {a, b, c, d} SUBSET s`] THEN \r
2334 REWRITE_TAC[ MESON[]` ~(a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d) /\ aa\r
2335   <=> aa /\ ~(a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d) `] THEN \r
2336 REWRITE_TAC[ MESON[]` (?a b c d. aa a b c d /\ packing s /\ P a b c d )\r
2337   <=> packing s /\ (? a b c d. aa a b c d /\ P a b c d)`] THEN \r
2338 SIMP_TAC[] THEN PHA THEN \r
2339 REWRITE_TAC[ MESON[]` d3 d b < sqrt (&8)/\ a<=> a /\ d3 d b < sqrt (&8)`] THEN \r
2340 PHA THEN NHANH (SET_RULE ` {b, c, d} = {v1, v2, v3} /\\r
2341                ~(a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d) /\\r
2342                {a, b, c, d} SUBSET s /\ last\r
2343   ==> {v1, v2, v3} SUBSET s /\ ~( b = c \/ c= d \/ d= b )`) THEN PHA THEN \r
2344 REWRITE_TAC[ MESON[]` d3 b c <= &2 * t0 /\\r
2345                d3 c d <= &2 * t0  /\ a <=> a /\ d3 b c <= &2 * t0 /\\r
2346                d3 c d <= &2 * t0  `] THEN \r
2347 MESON_TAC[]);;\r
2348 \r
2349 \r
2350 (* =========== *)\r
2351 \r
2352 let OCTOR23 = prove(`(?v1 v2 v3.\r
2353       ~(x IN {v1, v2, v3}) /\\r
2354       (?v4 vv1 vv2 vv3.\r
2355            {vv1, vv2, vv3} = {v1, v2, v3} /\\r
2356            #2.51 < dist (vv3,vv1) /\\r
2357            {v1, v2, v3} UNION {v4} IN Q_SYS s) /\\r
2358       ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\\r
2359       dist (x,y) < t0)\r
2360 ==> (?v1 v2 v3.\r
2361           packing s /\\r
2362           ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\\r
2363           dist (v1,v2) <= #2.51 /\\r
2364           dist (v2,v3) <= #2.51 /\\r
2365           dist (v3,v1) < sqrt (&8) /\\r
2366           {v1, v2, v3} SUBSET s /\\r
2367           ~(x IN {v1, v2, v3}) /\\r
2368           ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\\r
2369           dist (x,y) < t0)`,\r
2370 REWRITE_TAC[ MESON[]` a /\ (?v4 vv1 vv2 vv3.\r
2371            {vv1, vv2, vv3} = {v1, v2, v3} /\\r
2372            #2.51 < dist (vv3,vv1) /\\r
2373            {v1, v2, v3} UNION {v4} IN Q_SYS s) /\ b <=> (?v4 vv1 vv2 vv3.\r
2374            {vv1, vv2, vv3} = {v1, v2, v3} /\\r
2375            #2.51 < dist (vv3,vv1) /\\r
2376            {v1, v2, v3} UNION {v4} IN Q_SYS s) /\ a /\ b `] THEN \r
2377 NGOAC THEN REWRITE_TAC[ MESON[]` (( a /\ ~(x IN {v1, v2, v3})) /\\r
2378            ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {})) /\\r
2379           dist (x,y) < t0 <=> a /\ ( ~(x IN {v1, v2, v3}) /\\r
2380            ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\\r
2381           dist (x,y) < t0)`] THEN \r
2382 NGOAC THEN MATCH_MP_TAC (MESON[]` ((? a b c. P a b c ) ==> (? a b c. Q a b c) )\r
2383   ==> (? a b c. P a b c /\ d ) ==> ( ? a b c. Q a b c /\ d )`) THEN \r
2384 ONCE_REWRITE_TAC[ prove (`!q s.\r
2385      q IN Q_SYS s <=>\r
2386      q IN Q_SYS s /\\r
2387      (quasi_reg_tet q s \/\r
2388       strict_qua q s \/\r
2389       (?v v1 v3 v2 v4.\r
2390            (q = {v, v1, v2, v3} \/ q = {v, v1, v3, v4}) /\\r
2391            interior_pos v v1 v3 v2 v4 s /\\r
2392            anchor_points v1 v3 s = {v, v2, v4} /\\r
2393            anchor_points v2 v4 s = {v, v1, v3}))`, MP_TAC WHEN_IN_Q_SYS THEN \r
2394   REWRITE_TAC[ MESON[]` (! q s. P q s ==> R q s ) ==> ( ! q s. P q s <=> P q s\r
2395  /\ R q s ) `])] THEN \r
2396 KHANANG THEN \r
2397 MATCH_MP_TAC (MESON[]` ((?v1 v2 v3. (?a b c d. P v1 v2 v3 a b c d) /\ cc v1 v2 v3) ==> las) /\\r
2398      ((?v1 v2 v3. (?a b c d. Q v1 v2 v3 a b c d) /\ cc v1 v2 v3) ==> las) /\\r
2399      ((?v1 v2 v3. (?a b c d. R v1 v2 v3 a b c d) /\ cc v1 v2 v3) ==> las)\r
2400      ==> (?v1 v2 v3.\r
2401               (?a b c d.\r
2402                    P v1 v2 v3 a b c d \/\r
2403                    Q v1 v2 v3 a b c d \/\r
2404                    R v1 v2 v3 a b c d) /\\r
2405               cc v1 v2 v3)\r
2406      ==> las`) THEN \r
2407 SIMP_TAC[quasi_reg_tet_case; hard_case] THEN \r
2408 REWRITE_TAC[ MESON[]` a /\ as \/ b /\ as <=> ( a \/ b ) /\ as `] THEN \r
2409 NHANH (MATCH_MP (MESON[]` (! q s. P q s) ==> P q s`) RELATE_Q_SYS) THEN \r
2410 \r
2411 MATCH_MP_TAC (MESON[]` ((? v1 v2 v3 . (? a b c d. aa a b c d v1 v2 v3 /\ bb a b c d v1 v2 v3\r
2412   /\ cc a b c d v1 v2 v3 /\ ee a b c d v1 v2 v3 )\r
2413   /\ las v1 v2 v3 ) ==> last )\r
2414   ==> (? v1 v2 v3 . (? a b c d. aa a b c d v1 v2 v3 /\ bb a b c d v1 v2 v3\r
2415   /\ cc a b c d v1 v2 v3 /\ dd a b c d v1 v2 v3 /\ ee a b c d v1 v2 v3 )\r
2416   /\ las v1 v2 v3 ) ==> last `) THEN \r
2417 REWRITE_TAC[ hard_case]);;\r
2418 \r
2419 (* ============ *)\r
2420 \r
2421 \r
2422 let OCTO23 = prove (` ! s x y. (?v1 v2 v3.\r
2423       ~(x IN {v1, v2, v3}) /\\r
2424       (quasi_tri {v1, v2, v3} s \/ (?v4. {v1, v2, v3} UNION {v4} IN Q_SYS s)) /\\r
2425       ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\\r
2426       dist (x,y) < t0)\r
2427  ==> (?v1 v2 v3.\r
2428           packing s /\\r
2429           ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\\r
2430           dist (v1,v2) <= #2.51 /\\r
2431           dist (v2,v3) <= #2.51 /\\r
2432           dist (v3,v1) < sqrt (&8) /\\r
2433           {v1, v2, v3} SUBSET s /\\r
2434           ~(x IN {v1, v2, v3}) /\\r
2435           ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\\r
2436           dist (x,y) < t0) `,\r
2437 REWRITE_TAC[MESON[]`  (?v4. {v1, v2, v3} UNION {v4} IN Q_SYS s) <=>\r
2438      (?v4 vv1 vv2 vv3.\r
2439           ({vv1, vv2, vv3} = {v1, v2, v3} /\ #2.51 < dist (vv3,vv1)) /\\r
2440           {v1, v2, v3} UNION {v4} IN Q_SYS s) \/\r
2441      (?v4. (!vv1 vv2 vv3.\r
2442                 {vv1, vv2, vv3} = {v1, v2, v3} ==> ~(#2.51 < dist (vv3,vv1))) /\\r
2443            {v1, v2, v3} UNION {v4} IN Q_SYS s) `] THEN KHANANG THEN REPEAT GEN_TAC THEN \r
2444 REWRITE_TAC[ MESON[]` (?a b c. P a b c \/ Q a b c \/ R a b c) <=>\r
2445      (?a b c. P a b c) \/ (?a b c. Q a b c) \/ (?a b c. R a b c) `] THEN \r
2446 MATCH_MP_TAC (MESON[]` ( a ==> l ) /\ ( b==> l ) /\ ( c==> l ) ==> a \/ b\/ c ==> l `) THEN\r
2447 REWRITE_TAC[ quasi_tri_case; OCT24; OCTOR23 ]);;\r
2448 \r
2449 \r
2450 \r
2451 \r
2452 (* ===== *)\r
2453 \r
2454 let IN_AFF_GE_CON = prove(`!x y v3 v2.\r
2455      ~(conv0 {x, y} INTER conv_trg {x, v2, v3} = {})\r
2456      ==> y IN aff_ge {x} {v2, v3}`,\r
2457 REWRITE_TAC[ GSYM conv0_2; simpl_conv3; simp_def; SET_RULE` ~( a INTER b = {}) <=> \r
2458   (? x . x IN a /\ x IN b )`; IN_ELIM_THM] THEN \r
2459 NGOAC THEN \r
2460 REWRITE_TAC[ MESON[]` (?x'. (?t. P t /\ x' = t % x + (&1 - t) % y) /\\r
2461            (?a b c. Q a b c /\ x' = a % x + b % v2 + c % v3)) <=>\r
2462      (?a b c t. P t /\ Q a b c /\ t % x + (&1 - t) % y = a % x + b % v2 + c % v3)`] THEN \r
2463 REWRITE_TAC[ VECTOR_ARITH ` t % x + (&1 - t) % y = a % x + b % v2 + c % v3 \r
2464   <=> (&1 - t ) % y = ( a - t ) % x + b % v2 + c % v3 `] THEN \r
2465 REWRITE_TAC[ MESON[]` t < &1 /\ a <=> a /\ t < &1 `] THEN PHA THEN \r
2466 NHANH (REAL_ARITH` t < &1 ==> ~ ( &1 - t = &0 )`) THEN \r
2467 REWRITE_TAC[ MESON[]` (t < &1 /\ ~(&1 - t = &0)) /\ aa <=> aa /\ ~(&1 - t = &0) /\\r
2468   t < &1 `] THEN \r
2469 REWRITE_TAC[ MESON[]` (t < &1 /\ ~(&1 - t = &0)) /\ aa <=> t < &1 /\ aa /\ ~(&1 - t = &0)\r
2470   `] THEN PHA THEN \r
2471 ONCE_REWRITE_TAC[ MESON[REAL_FIELD `! a b. ~ ( b = &0 ) <=> a = b * a / b /\ ~ ( b = &0 ) `] `\r
2472   ~ ( b = &0 ) <=> ( ! a . a = b * a / b ) /\ ~ ( b = &0 )`] THEN \r
2473 PHA THEN REWRITE_TAC[ MESON[ VECTOR_MUL_RCANCEL ] ` (&1 - t) % y = (a - t) % x + b % v2 + c % v3 /\\r
2474           (!a. a = (&1 - t) * a / (&1 - t)) /\ las \r
2475   <=> (&1 - t) % y = ((&1 - t) * (a - t ) / (&1 - t)) % x + ((&1 - t) * b / (&1 - t)) % v2 + ((&1 - t) * c / (&1 - t)) % v3 /\\r
2476           (!a. a = (&1 - t) * a / (&1 - t)) /\ las `] THEN \r
2477 REWRITE_TAC[ VECTOR_ARITH ` ( a * b ) % v1 + ( a * c ) % v2 + ( a * d ) % v3 = a % ( b % v1 + c % v2 + d % v3 ) `] THEN \r
2478 REWRITE_TAC[ MESON[ VECTOR_MUL_LCANCEL_IMP; VECTOR_MUL_RCANCEL ] ` (&1 - t) % y =\r
2479           (&1 - t) %\r
2480           ((a - t) / (&1 - t) % x + b / (&1 - t) % v2 + c / (&1 - t) % v3) /\\r
2481           tttt /\\r
2482           ~(&1 - t = &0) /\ l <=>  y =\r
2483           \r
2484           ((a - t) / (&1 - t) % x + b / (&1 - t) % v2 + c / (&1 - t) % v3) /\\r
2485           tttt /\\r
2486           ~(&1 - t = &0) /\ l  `] THEN \r
2487 REWRITE_TAC[ REAL_ARITH ` t < &1 <=> &0 < &1 - t `] THEN \r
2488 REWRITE_TAC[ MESON[]`&0 <= a /\ &0 <= b /\\r
2489           &0 <= c /\ las <=> &0 <= a /\ las /\ &0 <= b /\\r
2490           &0 <= c `] THEN PHA THEN \r
2491 REWRITE_TAC[ MESON[REAL_ARITH ` &0 < a ==> &0 <= a `; REAL_LE_DIV ]`\r
2492   &0 < &1 - t /\ &0 <= a /\ &0 <= b <=>\r
2493      &0 < &1 - t /\\r
2494      &0 <= a /\\r
2495      &0 <= b /\\r
2496      &0 <= a / (&1 - t) /\\r
2497      &0 <= b / (&1 - t) `] THEN \r
2498 MESON_TAC[MESON[REAL_FIELD `~(&1 - t = &0) /\ a + b + c = &1\r
2499      ==> (a - t) / (&1 - t) + b / (&1 - t) + c / (&1 - t) = &1 `]` \r
2500   a + b + c = &1 /\\r
2501           y = (a - t) / (&1 - t) % x + b / (&1 - t) % v2 + c / (&1 - t) % v3 /\\r
2502           cccc  /\\r
2503           ~(&1 - t = &0) /\ las\r
2504   <=> a + b + c = &1 /\ cccc  /\ ~(&1 - t = &0) /\ las /\ y = (a - t) / (&1 - t) % x + b / (&1 - t) % v2 + c / (&1 - t) % v3\r
2505   /\ (a - t) / (&1 - t) + b / (&1 - t) + c / (&1 - t) = &1  `]);;\r
2506 \r
2507 \r
2508 (* ============= *)\r
2509 \r
2510 let xxii = MATCH_MP REAL_LT_RSQRT (REAL_ARITH `(&2 * #1.255) pow 2 < &8`);;\r
2511 \r
2512 \r
2513 let import_le = prove( `!x y s.\r
2514      x IN s /\\r
2515      dist (x,y) < t0 /\\r
2516      ~(y IN UNIONS {aff_ge {x} {w1, w2} | w1,w2 | {x, w1, w2} IN barrier s})\r
2517      ==> ~obstructed x y s`,\r
2518 REWRITE_TAC[ MESON[]` a /\ b /\ ~c ==> ~d <=> a /\ b /\ d ==> c`] THEN \r
2519 REWRITE_TAC[ obstructed ; barrier] THEN \r
2520 REWRITE_TAC[ IN_ELIM_THM] THEN \r
2521 ONCE_REWRITE_TAC[ MESON[]` (? a . P a ) <=> ( ? a. ( x IN a \/ ~( x IN a )) /\ P a)`] THEN  \r
2522 REWRITE_TAC[ MESON[] ` (?b. aa b /\ (?u v w. P u v w /\ b = {u, v, w}) /\ cc b) <=>\r
2523      (?u v w. aa {u, v, w} /\ P u v w /\ cc {u, v, w}) `] THEN \r
2524 REWRITE_TAC[ MESON[]` (x IN {v1, v2, v3} \/ ~(x IN {v1, v2, v3})) /\ a <=>\r
2525   x IN {v1, v2, v3} /\ a \/ ~(x IN {v1, v2, v3}) /\ a `] THEN \r
2526 ONCE_REWRITE_TAC[ MESON[]`(? a c b. P a b c \/ Q a b c ) \r
2527   <=> ( ? a b c. Q a b c \/ P a b c) `] THEN \r
2528 ONCE_REWRITE_TAC[ MESON[]` aa /\ (?a c b. P a b c \/ Q a b c) <=>\r
2529      aa /\ (?a b c. P a b c /\ aa \/ Q a b c) `] THEN PHA THEN \r
2530 REWRITE_TAC[conv0_2] THEN \r
2531 REWRITE_TAC[ MESON[]` (?a. P a \/ Q a) <=> (?a. P a) \/ (?a. Q a)`] THEN \r
2532 NHANH (MATCH_MP (MESON[]` (! a b c. P a b c) ==> P a b c `) OCTO23) THEN \r
2533 NHANH (MATCH_MP (MESON[]` (! x y a b c. P x y a b c ) ==> P x y a b c `)\r
2534   MEETING_CONDITION) THEN \r
2535 ONCE_REWRITE_TAC[MESON[]` v1 /\ v2/\ v3 /\ v4 /\ v5/\ v6 /\ v7 /\ las\r
2536   <=> ( v1 /\ v2/\ v3 /\ v4 /\ v5/\ v6 /\ v7)  /\ las`] THEN \r
2537 NHANH (MATCH_MP (MESON[]` (! a b c d e. P a b c d e ) ==> P a b c  d e`) tarski_FFSXOWD ) THEN \r
2538 PHA THEN \r
2539 REWRITE_TAC[ MESON[]` normball x #1.255 INTER conv {v1, v2, v3} = {} /\ a \r
2540   <=> a /\ normball x #1.255 INTER conv {v1, v2, v3} = {} `] THEN \r
2541 PHA THEN SIMP_TAC[ MESON[]` ~ a /\ a <=> F `] THEN \r
2542 REPEAT GEN_TAC THEN MATCH_MP_TAC (MESON[]` (c ==> l) ==> a /\ b/\ c==> l`) THEN \r
2543 REWRITE_TAC[SET_RULE ` x IN {a, b, c} <=> x = a \/ x = b \/ x = c `] THEN \r
2544 MATCH_MP_TAC (MESON[]` (!a b c. P a b c <=> P b a c) /\\r
2545      ((?a b c. (x = a \/ x = c) /\ P a b c) ==> las)\r
2546      ==> (?a b c. (x = a \/ x = b \/ x = c) /\ P a b c)\r
2547      ==> las`) THEN \r
2548 SIMP_TAC[ MESON[SET_RULE ` { a, b, c} = { b , a, c} ` ]` !v1 v2 v3.\r
2549          (quasi_tri {v1, v2, v3} s \/\r
2550           (?v4. {v1, v2, v3} UNION {v4} IN Q_SYS s)) /\\r
2551          ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) <=>\r
2552          (quasi_tri {v2, v1, v3} s \/\r
2553           (?v4. {v2, v1, v3} UNION {v4} IN Q_SYS s)) /\\r
2554          ~(conv0 {x, y} INTER conv_trg {v2, v1, v3} = {})`] THEN \r
2555 MATCH_MP_TAC (MESON[]` (!a b c. P a b c <=> P c b a ) /\\r
2556      ((?a b c. (x = a ) /\ P a b c) ==> las)\r
2557      ==> (?a b c. (x = a \/ x = c) /\ P a b c)\r
2558      ==> las`) THEN \r
2559 SIMP_TAC[ MESON[SET_RULE ` { a, b, c} = {c ,  b , a} ` ]` !v1 v2 v3.\r
2560       (quasi_tri {v1, v2, v3} s \/ (?v4. {v1, v2, v3} UNION {v4} IN Q_SYS s)) /\\r
2561       ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) <=>\r
2562       (quasi_tri {v3, v2, v1} s \/ (?v4. {v3, v2, v1} UNION {v4} IN Q_SYS s)) /\\r
2563       ~(conv0 {x, y} INTER conv_trg {v3, v2, v1} = {})`] THEN \r
2564 PURE_ONCE_REWRITE_TAC[ MESON[]` (?v1 v2 v3. x = v1 /\ P x v1 v2 v3) <=>\r
2565      (?v1 v2 v3. x = v1 /\ P x x v2 v3) `] THEN \r
2566 NHANH (MATCH_MP (MESON[]` (! a b c d. P a b c d) ==> P a b c d`) IN_AFF_GE_CON) THEN \r
2567 MATCH_MP_TAC (MESON[]` ((? v1 v2 v3.  P v1 v2 v3 /\ PP v1 v2 v3 ) \r
2568   ==> last )\r
2569   ==> (? v1 v2 v3. a v1 /\ P v1 v2 v3 /\ b v2 v3 /\ PP v1 v2 v3 ) \r
2570   ==> last `) THEN \r
2571 REWRITE_TAC[ IN_UNIONS; IN_ELIM_THM] THEN \r
2572 MESON_TAC[]);;\r
2573 \r
2574 \r
2575 \r
2576 \r
2577 \r
2578 \r
2579 (* ======================== end im_le_82.ml =============================== *)\r
2580 \r
2581 let lemma_of_lemma82 = prove (` ! (x:real^3) (v0:real^3) s Z. centered_pac s v0 /\ Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\\r
2582  x IN normball v0 t0 DIFF Z\r
2583  ==> (?w. w IN near2t0 v0 s /\ x IN voronoi w s)`, REPEAT GEN_TAC THEN REWRITE_TAC[centered_pac] THEN \r
2584 REWRITE_TAC[ SET_RULE `packing s /\ v0 IN s <=> packing s /\ v0 IN s /\ ~(s={})`] THEN \r
2585 REWRITE_TAC[MESON[exists_min_dist] ` (packing s /\ v0 IN s /\ ~(s = {})) /\\r
2586  Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\\r
2587  x IN normball v0 t0 DIFF Z  <=>(packing s /\ v0 IN s /\ ~(s = {})) /\\r
2588  Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\\r
2589  x IN normball v0 t0 DIFF Z /\ min_dist x s `] THEN \r
2590 SIMP_TAC[normball; min_dist] THEN \r
2591 REWRITE_TAC[SET_RULE` x IN a DIFF b <=> x IN a /\ ~( x IN b )`] THEN \r
2592 REWRITE_TAC[SET_RULE ` x IN { x | P x } <=> P x `] THEN PHA THEN \r
2593 REWRITE_TAC[MESON[]` dist (x,v0) < t0 /\\r
2594  ~(x IN Z) /\\r
2595  ((?u. u IN s /\ (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/\r
2596   (?u v.\r
2597        u IN s /\\r
2598        v IN s /\\r
2599        ~(u = v) /\\r
2600        dist (u,x) = dist (v,x) /\\r
2601        (!w. w IN s ==> dist (u,x) <= dist (w,x)))) <=>\r
2602   dist (x,v0) < t0 /\\r
2603  ~(x IN Z) /\\r
2604  ((?u. u IN s /\ (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/\r
2605   ( ~(x IN Z) /\ (?u v.\r
2606        u IN s /\\r
2607        v IN s /\\r
2608        ~(u = v) /\\r
2609        dist (u,x) = dist (v,x) /\\r
2610        (!w. w IN s ==> dist (u,x) <= dist (w,x)) /\ dist (x,v0) < t0 ))) `] THEN \r
2611 REWRITE_TAC[MESON[DIST_TRIANGLE] ` v0 IN s /\\r
2612      ~(s = {}) /\\r
2613      Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\\r
2614      dist (x,v0) < t0 /\\r
2615      ~(x IN Z) /\\r
2616      ((?u. u IN s /\ (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/\r
2617       ~(x IN Z) /\\r
2618       (?u v.\r
2619            u IN s /\\r
2620            v IN s /\\r
2621            ~(u = v) /\\r
2622            dist (u,x) = dist (v,x) /\\r
2623            (!w. w IN s ==> dist (u,x) <= dist (w,x)) /\\r
2624            dist (x,v0) < t0)) <=>\r
2625      v0 IN s /\\r
2626      ~(s = {}) /\\r
2627      Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\\r
2628      dist (x,v0) < t0 /\\r
2629      ~(x IN Z) /\\r
2630      ((?u. u IN s /\ (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/\r
2631       ~(x IN Z) /\\r
2632       (?u v.\r
2633            u IN s /\\r
2634            dist (u,v0) <= dist (u,x) + dist (x,v0) /\\r
2635            dist (u,x) <= dist (v0,x) /\\r
2636            v IN s /\\r
2637            dist (v,v0) <= dist (v,x) + dist (x,v0) /\\r
2638            dist (v,x) <= dist (v0,x) /\\r
2639            ~(u = v) /\\r
2640            dist (u,x) = dist (v,x) /\\r
2641            (!w. w IN s ==> dist (u,x) <= dist (w,x)) /\\r
2642            dist (x,v0) < t0)) `] THEN \r
2643 REWRITE_TAC[MESON[] ` u IN s /\\r
2644      dist (u,v0) <= dist (u,x) + dist (x,v0) /\\r
2645      dist (u,x) <= dist (v0,x) /\\r
2646      v IN s /\\r
2647      dist (v,v0) <= dist (v,x) + dist (x,v0) /\\r
2648      dist (v,x) <= dist (v0,x) /\\r
2649      ~(u = v) /\\r
2650      dist (u,x) = dist (v,x) /\\r
2651      (!w. w IN s ==> dist (u,x) <= dist (w,x)) /\\r
2652      dist (x,v0) < t0 <=>\r
2653      u IN s /\\r
2654      (dist (u,v0) <= dist (u,x) + dist (x,v0) /\\r
2655       dist (u,x) <= dist (v0,x) /\\r
2656       dist (x,v0) < t0) /\\r
2657      v IN s /\\r
2658      (dist (v,v0) <= dist (v,x) + dist (x,v0) /\\r
2659       dist (v,x) <= dist (v0,x) /\\r
2660       dist (x,v0) < t0) /\\r
2661      ~(u = v) /\\r
2662      dist (u,x) = dist (v,x) /\\r
2663      (!w. w IN s ==> dist (u,x) <= dist (w,x))`] THEN \r
2664 SIMP_TAC[DIST_SYM] THEN \r
2665 REWRITE_TAC[REAL_ARITH ` dist (u,v0) <= dist (u,x) + dist (v0,x) /\\r
2666         dist (u,x) <= dist (v0,x) /\\r
2667         dist (v0,x) < t0\r
2668   <=> dist (u,v0) <= dist (u,x) + dist (v0,x) /\\r
2669         dist (u,x) <= dist (v0,x) /\\r
2670         dist (v0,x) < t0 /\ dist(u, v0) < &2 * t0 `] THEN \r
2671 REWRITE_TAC[ MESON[] ` a /\ b /\c/\ d /\ e ==> f <=> a/\b/\c/\d ==> e ==> f `] THEN SIMP_TAC[] THEN \r
2672 REWRITE_TAC[ IN_UNIONS; e_plane; near2t0] THEN \r
2673 REWRITE_TAC[SET_RULE ` x IN { x | P x } <=> P x `] THEN \r
2674 REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[ MESON[] ` (?t. (?u v.\r
2675                  ((u IN s /\ dist (v0,u) < &2 * t0) /\\r
2676                   v IN s /\\r
2677                   dist (v0,v) < &2 * t0) /\\r
2678                  t = e_plane u v) /\\r
2679             x IN t ) \r
2680   <=> (?u v.\r
2681                  ((u IN s /\ dist (v0,u) < &2 * t0) /\\r
2682                   v IN s /\\r
2683                   dist (v0,v) < &2 * t0) /\\r
2684                  x IN e_plane u v) `] THEN \r
2685 REWRITE_TAC[ SET_RULE ` x IN e_plane u v <=> e_plane u v x `; e_plane] THEN \r
2686 PHA THEN SIMP_TAC[ MESON[DIST_SYM] ` ~(?u v.\r
2687             u IN s /\\r
2688             dist (v0,u) < &2 * t0 /\\r
2689             v IN s /\\r
2690             dist (v0,v) < &2 * t0 /\\r
2691             ~(u = v) /\\r
2692             dist (u,x) = dist (v,x)) /\\r
2693       (?u v.\r
2694            u IN s /\\r
2695            dist (u,v0) <= dist (u,x) + dist (v0,x) /\\r
2696            dist (u,x) <= dist (v0,x) /\\r
2697            dist (v0,x) < t0 /\\r
2698            dist (u,v0) < &2 * t0 /\\r
2699            v IN s /\\r
2700            dist (v,v0) <= dist (v,x) + dist (v0,x) /\\r
2701            dist (v,x) <= dist (v0,x) /\\r
2702            dist (v0,x) < t0 /\\r
2703            dist (v,v0) < &2 * t0 /\\r
2704            ~(u = v) /\\r
2705            dist (u,x) = dist (v,x) /\\r
2706            (!w. w IN s ==> dist (u,x) <= dist (w,x))) <=> F `] THEN \r
2707 REWRITE_TAC[voronoi] THEN REWRITE_TAC[ SET_RULE ` x IN { x | P x } <=> P x `] THEN \r
2708 REWRITE_TAC[ MESON[] ` dist (v0,x) < t0 /\\r
2709      ~(?u v.\r
2710            u IN s /\\r
2711            dist (v0,u) < &2 * t0 /\\r
2712            v IN s /\\r
2713            dist (v0,v) < &2 * t0 /\\r
2714            ~(u = v) /\\r
2715            dist (u,x) = dist (v,x)) /\\r
2716      (?u. u IN s /\ (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x)))\r
2717   <=> dist (v0,x) < t0 /\\r
2718      ~(?u v.\r
2719            u IN s /\\r
2720            dist (v0,u) < &2 * t0 /\\r
2721            v IN s /\\r
2722            dist (v0,v) < &2 * t0 /\\r
2723            ~(u = v) /\\r
2724            dist (u,x) = dist (v,x)) /\\r
2725      (?u. u IN s /\dist (v0,x) < t0  /\  (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x)))`] THEN \r
2726 REWRITE_TAC[ MESON[DIST_TRIANGLE] `(?u. u IN s /\\r
2727           dist (v0,x) < t0 /\\r
2728           (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) <=>\r
2729      (?u. u IN s /\\r
2730           dist (v0,x) < t0 /\\r
2731           dist (u,v0) <= dist (u,x) + dist (x,v0) /\\r
2732           (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) `] THEN \r
2733 REWRITE_TAC[ MESON[] ` ( a ==> b==> c <=> a/\b ==> c ) `] THEN PHA THEN \r
2734 ONCE_REWRITE_TAC[ MESON[] ` a /\ b /\ c ==> d <=> a/\c /\b ==> d `] THEN PHA THEN \r
2735 ONCE_REWRITE_TAC[MESON[] ` !P. (?u. P u) /\ v0 IN s <=>\r
2736          ((?u. u = v0 /\ P u) \/ (?u. ~(u = v0) /\ P u)) /\ v0 IN s`] THEN \r
2737 REWRITE_TAC[t0] THEN ONCE_REWRITE_TAC[MESON[ DIST_REFL; REAL_ARITH ` &0 < &2 * #1.255 ` ] ` u = v0 /\ las  <=> u = v0  /\ dist(u,v0 ) < &2 * #1.255 /\ las `] THEN \r
2738 REWRITE_TAC[ MESON[] ` ((?u. u = v0 /\\r
2739            dist (u,v0) < &2 * #1.255 /\\r
2740            u IN s /\\r
2741            dist (v0,x) < #1.255 /\\r
2742            dist (u,v0) <= dist (u,x) + dist (x,v0) /\\r
2743            (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/\r
2744       (?u. ~(u = v0) /\\r
2745            u IN s /\\r
2746            dist (v0,x) < #1.255 /\\r
2747            dist (u,v0) <= dist (u,x) + dist (x,v0) /\\r
2748            (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x)))) /\\r
2749      v0 IN s <=>\r
2750      ((?u. u = v0 /\\r
2751            dist (u,v0) < &2 * #1.255 /\\r
2752            u IN s /\\r
2753            v0 IN s /\\r
2754            dist (v0,x) < #1.255 /\\r
2755            dist (u,v0) <= dist (u,x) + dist (x,v0) /\\r
2756            (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/\r
2757       (?u. ~(u = v0) /\\r
2758            u IN s /\\r
2759            v0 IN s /\\r
2760            dist (v0,x) < #1.255 /\\r
2761            dist (u,v0) <= dist (u,x) + dist (x,v0) /\\r
2762            (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x)))) /\\r
2763      v0 IN s `] THEN REWRITE_TAC[ MESON[] ` ~(u = v0) /\\r
2764      u IN s /\\r
2765      v0 IN s /\\r
2766      dist (v0,x) < #1.255 /\\r
2767      dist (u,v0) <= dist (u,x) + dist (x,v0) /\\r
2768      (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x)) <=>\r
2769      ~(u = v0) /\\r
2770     \r
2771      u IN s /\\r
2772      v0 IN s /\ (  dist (u,x) < dist (v0,x) /\\r
2773      dist (v0,x) < #1.255 /\\r
2774      dist (u,v0) <= dist (u,x) + dist (x,v0) ) /\\r
2775      (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x)) `] THEN SIMP_TAC[DIST_SYM] THEN \r
2776 PURE_ONCE_REWRITE_TAC[ REAL_ARITH `  ( dist (u,x) < dist (v0,x) /\\r
2777      dist (v0,x) < #1.255 /\\r
2778      dist (u,v0) <= dist (u,x) + dist (v0,x))  <=>\r
2779      (dist (u,x) < dist (v0,x) /\\r
2780       dist (v0,x) < #1.255 /\\r
2781       dist (u,v0) <= dist (u,x) + dist (v0,x)) /\\r
2782      dist (u,v0) < &2 * #1.255 ` ] THEN \r
2783 MATCH_MP_TAC (MESON[] `((?u. u = v0 /\\r
2784            dist (u,v0) < &2 * #1.255 /\\r
2785            u IN s /\\r
2786            v0 IN s /\\r
2787            dist (v0,x) < #1.255 /\\r
2788            dist (u,v0) <= dist (u,x) + dist (v0,x) /\\r
2789            (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/\r
2790       (?u. ~(u = v0) /\\r
2791            u IN s /\\r
2792            v0 IN s /\\r
2793            ((dist (u,x) < dist (v0,x) /\\r
2794              dist (v0,x) < #1.255 /\\r
2795              dist (u,v0) <= dist (u,x) + dist (v0,x)) /\\r
2796             dist (u,v0) < &2 * #1.255) /\\r
2797            (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x)))\r
2798       ==> (?w. w IN s /\\r
2799                dist (v0,w) < &2 * #1.255 /\\r
2800                (!w'. s w' /\ ~(w' = w) ==> dist (w,x) < dist (w',x))))\r
2801      ==> packing s /\\r
2802          ~(s = {}) /\\r
2803          Z =\r
2804          UNIONS\r
2805          {e_plane u v | u IN s /\\r
2806                         dist (u,v0) < &2 * #1.255 /\\r
2807                         v IN s /\\r
2808                         dist (v,v0) < &2 * #1.255} /\\r
2809          dist (v0,x) < #1.255 /\\r
2810          ~(?u v.\r
2811                u IN s /\\r
2812                dist (u,v0) < &2 * #1.255 /\\r
2813                v IN s /\\r
2814                dist (v,v0) < &2 * #1.255 /\\r
2815                ~(u = v) /\\r
2816                dist (u,x) = dist (v,x)) /\\r
2817          ((?u. u = v0 /\\r
2818                dist (u,v0) < &2 * #1.255 /\\r
2819                u IN s /\\r
2820                v0 IN s /\\r
2821                dist (v0,x) < #1.255 /\\r
2822                dist (u,v0) <= dist (u,x) + dist (v0,x) /\\r
2823                (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/\r
2824           (?u. ~(u = v0) /\\r
2825                u IN s /\\r
2826                v0 IN s /\\r
2827                ((dist (u,x) < dist (v0,x) /\\r
2828                  dist (v0,x) < #1.255 /\\r
2829                  dist (u,v0) <= dist (u,x) + dist (v0,x)) /\\r
2830                 dist (u,v0) < &2 * #1.255) /\\r
2831                (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x)))) /\\r
2832          v0 IN s\r
2833      ==> (?w. w IN s /\\r
2834               dist (v0,w) < &2 * #1.255 /\\r
2835               (!w'. s w' /\ ~(w' = w) ==> dist (w,x) < dist (w',x))) `) THEN \r
2836 MESON_TAC [DIST_SYM; SET_RULE ` ! x s. s x <=> x IN s ` ]);;\r
2837 \r
2838 \r
2839 \r