text_formalization/leg/collect_geom.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: leg                                                               *)
   5 (* Author: Nguyen Quang Truong                                               *)
   6 (* Date: 2010-02-09                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10
  11 flyspeck_needs "general/sphere.hl";;
  12 flyspeck_needs "leg/geomdetail.hl";;
  13 flyspeck_needs "leg/affprops.hl";;
  14 flyspeck_needs "leg/cayleyR_def.hl";;
  15
  16 module Collect_geom  = struct
  17
  18 (*
  19
  20 thales:
  21 global replace rho->rho_x
  22
  23 This file gives an alternative def of rho_ij, delta, chi.
  24 These should be reconciled with main flyspeck library
  25
  26
  27 *)
  28
  29   let packing = Sphere.packing;;
  30   let eta_x = Sphere.eta_x;;
  31   let eta_y = Sphere.eta_y;;
  32   let aff = Sphere.aff;;  (* also appears in Geomdetail *)
  33   let line = Sphere.line;;
  34   let circumcenter = Sphere.circumcenter;;
  35   let radV = Sphere.radV;;
  36
  37   let conv = Geomdetail.conv;;
  38   let CONV0_SET2 = Geomdetail.CONV0_SET2;;
  39   let OR_IMP_EX = Geomdetail.OR_IMP_EX;;
  40   let CONV_SET3 = Geomdetail.CONV_SET3;;
  41   let INTERS_SUBSET = Geomdetail.INTERS_SUBSET;;
  42   let DOT_SUB_ADD = Geomdetail.DOT_SUB_ADD;;
  43   let trg_dist3_sym = Geomdetail.trg_dist3_sym;;
  44   let DIST_LT_HALF_PLANE = Geomdetail.DIST_LT_HALF_PLANE;;
  45
  46   let simp_def2 = Affprops.affprops;;
  47
  48   let cayleyR = Cayleyr.cayleyR;;
  49
  50   let BY = Hales_tactic.BY;;
  51
  52 prioritize_real();;
  53
  54 (* dist3 is deprecated *)
  55 let dist3 = new_definition `dist3 (v:real^3) w = dist(v,w)`;;
  56
  57 let ups_x = new_definition ` ups_x x1 x2 x6 =
  58          --x1 * x1 - x2 * x2 - x6 * x6 +
  59          &2 * x1 * x6 +
  60          &2 * x1 * x2 +
  61          &2 * x2 * x6 `;;
  62
  63 (*
  64 let rho_ij = new_definition ` rho_ij (x12 :real) x13 x14 x23 x24 x34 =
  65          --(x14 * x14 * x23 * x23) -
  66          x13 * x13 * x24 * x24 -
  67          x12 * x12 * x34 * x34 +
  68          &2 *
  69          (x12 * x14 * x23 * x34 +
  70           x12 * x13 * x24 * x34 +
  71           x13 * x14 * x23 * x24) `;;
  72 *)
  73
  74 let rho_ij'_rho_x = new_definition `rho_ij' x1 x2 x3 x6 x5 x4 = rho_x x1 x2 x3 x4 x5 x6`;;
  75
  76 let rho_ij' = prove_by_refinement(
  77   `!x12 x34 x13 x14 x23 x24. rho_ij' (x12 :real) x13 x14 x23 x24 x34 =
  78          --(x14 * x14 * x23 * x23) -
  79          x13 * x13 * x24 * x24 -
  80          x12 * x12 * x34 * x34 +
  81          &2 *
  82          (x12 * x14 * x23 * x34 +
  83           x12 * x13 * x24 * x34 +
  84           x13 * x14 * x23 * x24)`,
  85   (* {{{ proof *)
  86   [
  87   (REWRITE_TAC[rho_ij'_rho_x;Sphere.rho_x]);
  88   BY(REAL_ARITH_TAC)
  89   ]);;
  90   (* }}} *)
  91
  92 let chi = new_definition ` chi x12 x13 x14 x23 x24 x34 =
  93          x13 * x23 * x24 +
  94          x14 * x23 * x24 +
  95          x12 * x23 * x34 +
  96          x14 * x23 * x34 +
  97          x12 * x24 * x34 +
  98          x13 * x24 * x34 -
  99          &2 * x23 * x24 * x34 -
 100          x12 * x34 * x34 -
 101          x14 * x23 * x23 -
 102          x13 * x24 * x24 `;;
 103
 104 let delta = new_definition ` delta x12 x13 x14 x23 x24 x34 =
 105    --(x12 * x13 * x23) -
 106          x12 * x14 * x24 -
 107          x13 * x14 * x34 -
 108          x23 * x24 * x34 +
 109          x12 * x34 * (--x12 + x13 + x14 + x23 + x24 - x34) +
 110          x13 * x24 * (x12 - x13 + x14 + x23 - x24 + x34 ) +
 111          x14 * x23 * ( x12 + x13 - x14 - x23 + x24 + x34 ) `;;
 112
 113 let eta_v = new_definition ` eta_v v1 v2 (v3: real^N) =
 114         let e1 = dist (v2, v3) in
 115           let e2 = dist (v1, v3) in
 116           let e3 = dist (v2, v1) in
 117           e1 * e2 * e3 / sqrt ( ups_x (e1 pow 2 ) ( e2 pow 2) ( e3 pow 2 ) ) `;;
 118
 119 let max_real = new_definition(`max_real x y =
 120         if (y < x) then x else y`);;
 121
 122 let max_real3 = new_definition ` max_real3 x y z = max_real (max_real x y ) z `;;
 123
 124 let ups_x_pow2 = new_definition` ups_x_pow2 x y z = ups_x ( x*x ) ( y * y) ( z * z)`;;
 125
 126 let plane_norm = new_definition `
 127   plane_norm p <=>
 128          (?n v0. ~(n = vec 0) /\ p = {v | n dot (v - v0) = &0}) `;;
 129
 130
 131 let delta_x34 = new_definition ` delta_x34 x12 x13 x14 x23 x24 x34  =
 132 -- &2 * x12 * x34 +
 133 (--x13 * x14 +
 134       --x23 * x24 +
 135       x13 * x24 +
 136       x14 * x23 +
 137       --x12 * x12 +
 138       x12 * x14 +
 139       x12 * x24 +
 140       x12 * x13 +
 141       x12 * x23) `;;
 142
 143
 144 (*
 145 let plane_3p = new_definition `plane_3p (a:real^3) b c =
 146          {x | ~collinear {a, b, c} /\
 147               (?ta tb tc. ta + tb + tc = &1 /\ x = ta % a + tb % b + tc % c)}`;;
 148 *)
 149
 150 (* end new_definition *)
 151
 152 (* NGUYEN DUC PHUONG *)
 153 (* Definition of Cayley  Menger square cm3 *)
 154
 155
 156 let cm3_ups_x = new_definition `!(v1:real^3) (v2:real^3) (v3:real^3).
 157    cm3_ups_x v1 v2 v3 =
 158   (((v2 - v1)$2 * (v3 - v1)$3 ) - ((v2 - v1)$3 * (v3 - v1)$2)) pow 2 +
 159   (((v2 - v1)$3 * (v3 - v1)$1 ) - ((v2 - v1)$1 * (v3 - v1)$3)) pow 2 +
 160   (((v2 - v1)$1 * (v3 - v1)$2 ) - ((v2 - v1)$2 * (v3 - v1)$1)) pow 2 `;;
 161
 162
 163 (* Nguyen Tuyen Hoang, Nguyen Duc Phuong *)
 164
 165 (* The polynomial ups can be expressed as a Cayley- Menger square *)
 166
 167 let lemma_cm3 = prove (`!(x:real^3) y.
 168 (x-y)$1 = x$1 - y$1 /\ (x-y)$2 = x$2 - y$2 /\ (x-y)$3 = x$3 - y$3`,
 169
 170 (REPEAT GEN_TAC) THEN (REPEAT CONJ_TAC) THENL
 171 [(MESON_TAC[VECTOR_SUB_COMPONENT;DIMINDEX_3;ARITH_RULE `1 <= 1 /\ 1 <= 3`]);
 172 (MESON_TAC[VECTOR_SUB_COMPONENT;DIMINDEX_3;ARITH_RULE `1 <= 2 /\ 2 <= 3`]);
 173 (MESON_TAC[VECTOR_SUB_COMPONENT;DIMINDEX_3;ARITH_RULE `1 <= 3 /\ 3 <= 3`])]);;
 174
 175 let lemma7 = prove ( `! (v1 : real ^3)(v2: real^3)(v3:real^3).
 176   cm3_ups_x v1 v2 v3 =
 177   ups_x (norm (v1 -v2) pow 2) (norm (v2 -v3) pow 2) (norm (v3 -v1) pow 2) / &4`,
 178
 179  (REPEAT GEN_TAC) THEN
 180  (REWRITE_TAC[cm3_ups_x; ups_x]) THEN
 181  (REWRITE_TAC[GSYM DOT_SQUARE_NORM;DOT_3;REAL_POW_2]) THEN
 182  (REWRITE_TAC[lemma_cm3]) THEN
 183   REAL_ARITH_TAC );;
 184
 185 let pow_g = prove ( `! (x:real). &0 <= x pow 2`,
 186   GEN_TAC THEN REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE]);;
 187
 188 let lemma8 = prove ( `! (v1:real^3)(v2:real^3)(v3:real^3).
 189 &0 <= ups_x (norm (v1 - v2) pow 2)(norm (v2 - v3) pow 2)(norm (v3 - v1) pow 2)`,
 190  (REPEAT GEN_TAC)
 191 THEN (MATCH_MP_TAC (REAL_ARITH `&0 <= a/ &4 ==> &0 <= a `))
 192 THEN (REWRITE_TAC[GSYM lemma7])
 193 THEN (REWRITE_TAC[cm3_ups_x])
 194
 195 THEN (ABBREV_TAC `(a:real) = (((v2:real^3) - v1)$2 * (v3 - v1)$3 - (v2 - v1)$3 * (v3 - v1)$2) pow 2`)
 196 THEN (FIRST_X_ASSUM ((LABEL_TAC "1") o GSYM))
 197 THEN (ABBREV_TAC `(b:real) = (((v2:real^3) - v1)$3 * (v3 - v1)$1 - (v2 - v1)$1 * (v3 - v1)$3) pow 2`)
 198 THEN (FIRST_X_ASSUM((LABEL_TAC "2") o GSYM))
 199 THEN (ABBREV_TAC `(c:real) = (((v2:real^3) - v1)$1 * (v3 - v1)$2 - (v2 - v1)$2 * (v3 - v1)$1) pow 2`)
 200 THEN (FIRST_X_ASSUM((LABEL_TAC "3") o GSYM))
 201
 202 THEN (MATCH_MP_TAC (SPEC_ALL REAL_LE_ADD))
 203 THEN CONJ_TAC
 204 THEN (ASM_REWRITE_TAC[pow_g])
 205 THEN (MATCH_MP_TAC (SPEC_ALL REAL_LE_ADD))
 206 THEN CONJ_TAC
 207 THEN (ASM_REWRITE_TAC[pow_g]));;
 208
 209 (* ========== *)
 210 (* QUANG TRUONG *)
 211 (* ============ *)
 212 let GONTONG = REAL_RING ` ((a + b) + c = a + b + c ) `;;
 213
 214 let SUB_SUM_SUB = REAL_RING ` (a - ( b + c ) = a - b - c )/\( a - (b- c) = a - b + c )` ;;
 215
 216 (* lemma 4, p 7 *)
 217 let JVUNDLC = prove(`!a b c s.
 218      s = (a + b + c) / &2
 219      ==> &16 * s * (s - a) * (s - b) * (s - c) =
 220          ups_x (a pow 2) (b pow 2) (c pow 2)`, SIMP_TAC [ ups_x] THEN
 221 REWRITE_TAC[REAL_FIELD` a / &2 - b = ( a - &2 * b ) / &2 `] THEN
 222 REWRITE_TAC[REAL_FIELD ` &16 * ( a / &2 ) * ( b / &2 ) * (c / &2 ) *
 223 ( d / &2 ) = a * b * c * d `] THEN REAL_ARITH_TAC);;
 224
 225 let SET_TAC =
 226    let basicthms =
 227     [NOT_IN_EMPTY; IN_UNIV; IN_UNION; IN_INTER; IN_DIFF; IN_INSERT;
 228      IN_DELETE; IN_REST; IN_INTERS; IN_UNIONS; IN_IMAGE] in
 229    let allthms = basicthms @ map (REWRITE_RULE[IN]) basicthms @
 230                  [IN_ELIM_THM; IN] in
 231    let PRESET_TAC =
 232      TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ)) THEN
 233      REPEAT COND_CASES_TAC THEN
 234      REWRITE_TAC[EXTENSION; SUBSET; PSUBSET; DISJOINT; SING] THEN
 235      REWRITE_TAC allthms in
 236    fun ths ->
 237      PRESET_TAC THEN
 238      (if ths = [] then ALL_TAC else MP_TAC(end_itlist CONJ ths)) THEN
 239      MESON_TAC[];;
 240
 241  let SET_RULE tm = prove(tm,SET_TAC[]);;
 242
 243 (* some TRUONG TACTICS *)
 244
 245 let PHA = REWRITE_TAC[ MESON[] ` (a/\b)/\c <=> a/\ b /\ c `];;
 246
 247 let NGOAC = REWRITE_TAC[ MESON[] ` a/\b/\c <=> (a/\b)/\c `];;
 248
 249 let DAO = NGOAC THEN REWRITE_TAC[ MESON[]` a /\ b <=> b /\ a`];;
 250
 251 let PHAT = REWRITE_TAC[ MESON[] ` (a\/b)\/c <=> a\/b\/c `];;
 252
 253 let NGOACT =  REWRITE_TAC[ GSYM (MESON[] ` (a\/b)\/c <=> a\/b\/c `)];;
 254
 255 let KHANANG = PHA THEN REWRITE_TAC[ MESON[]` ( a\/ b ) /\ c <=> a /\ c \/ b /\ c `] THEN
 256  REWRITE_TAC[ MESON[]` a /\ ( b \/ c ) <=> a /\ b \/ a /\ c `];;
 257
 258 let ATTACH thm = MATCH_MP (MESON[]` ! a b. ( a ==> b ) ==> ( a <=> a /\ b )`) thm;;
 259
 260 let NHANH tm = ONCE_REWRITE_TAC[ ATTACH (tm)];;
 261 let STRIP_TR = REPEAT STRIP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC)
 262       THEN REWRITE_TAC[IMP_IMP] THEN PHA;;
 263
 264
 265 let elimin = REWRITE_RULE[IN];;
 266
 267 let CONV_EM = prove(`conv {} = {}:real^A->bool`,
 268   REWRITE_TAC[conv;sgn_ge;affsign;UNION_EMPTY;FUN_EQ_THM;elimin
 269 NOT_IN_EMPTY;lin_combo;SUM_CLAUSES]
 270   THEN REAL_ARITH_TAC);;
 271
 272 let CONV_SING = prove(`!u. conv {u:real^A} = {u}`,
 273  REWRITE_TAC[conv;sgn_ge;affsign;FUN_EQ_THM;UNION_EMPTY;lin_combo;SUM_SING;VSUM_SING;
 274  elimin IN_SING] THEN REPEAT GEN_TAC THEN
 275  REWRITE_TAC[TAUT `(p <=> q) = ((p ==> q) /\ (q ==> p))`] THEN
 276  REPEAT STRIP_TAC THENL [ASM_MESON_TAC[VECTOR_MUL_LID];
 277  ASM_REWRITE_TAC[]] THEN EXISTS_TAC `\ (v:real^A). &1` THEN
 278  MESON_TAC[VECTOR_MUL_LID;REAL_ARITH `&0 <= &1`] );;
 279
 280 let IN_ACT_SING = SET_RULE `! a x. ({a} x <=> a = x ) /\ ( x IN {a} <=> x = a) /\ {a} a`;;
 281
 282 let IN_SET2 = SET_RULE `!a b x.
 283          (x IN {a, b} <=> x = a \/ x = b) /\ ({a, b} x <=> x = a \/ x = b)`;;
 284
 285 let SUM_DIS2 = prove(`! x y f. ~(x=y) ==> sum {x,y} f = f x + f y `,REWRITE_TAC[
 286    SET_RULE ` ~( x = y)
 287  <=> ~(x IN {y})`] THEN MESON_TAC[ FINITE_RULES; SUM_CLAUSES; SUM_SING]);;
 288
 289
 290 let VSUM_DIS2 = prove(` ! x y f. ~(x=y) ==>  vsum {x,y} f = f x + f y`, REWRITE_TAC[
 291    SET_RULE ` ~( x = y)
 292  <=> ~(x IN {y})`] THEN MESON_TAC[ FINITE_RULES; VSUM_CLAUSES; VSUM_SING]);;
 293
 294 let NOV10 = prove(` ! x y. (x = y
 295       ==> (!x. y = x <=>
 296                (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x = a % y + b % y))) `,
 297 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN
 298 REWRITE_TAC[ MESON[VECTOR_MUL_LID]` a + b = &1 /\ x = (a + b) % y <=> a + b = &1 /\
 299 x = y`]THEN REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN NGOAC THEN
 300 REWRITE_TAC[LEFT_EXISTS_AND_THM] THEN MATCH_MP_TAC (MESON[]` a ==> ( x = y <=> a /\
 301  y = x )`)THEN EXISTS_TAC `&0` THEN EXISTS_TAC ` &1` THEN REAL_ARITH_TAC);;
 302
 303
 304 let TRUONG_LEMMA = prove
 305   (  `!x y x':real^N.
 306        (?f. x' = f x % x + f y % y /\ (&0 <= f x /\ &0 <= f y) /\
 307             f x + f y = &1) <=>
 308        (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x' = a % x + b % y)`   ,
 309    REPEAT GEN_TAC THEN EQ_TAC
 310 THENL [MESON_TAC[]; STRIP_TAC] THEN
 311    ASM_CASES_TAC `y:real^N = x` THENL
 312     [EXISTS_TAC `\x:real^N. &1 / &2`;
 313      EXISTS_TAC `\u:real^N. if u = x then (a:real) else b`] THEN
 314    ASM_REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN
 315    CONV_TAC REAL_RAT_REDUCE_CONV);;
 316
 317 let CONV_SET2 = prove(` ! x y:real^A. conv {x,y} = {w | ? a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\
 318   w = a%x + b%y}`,
 319 ONCE_REWRITE_TAC[ MESON[] ` (! a b. P a b ) <=> ( ! a b. a = b \/ ~( a= b)
 320   ==> P a b )`] THEN
 321 REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a==> c) /\ ( b==> c)`] THEN
 322 SIMP_TAC[] THEN REWRITE_TAC[ SET_RULE ` {a,a} = {a}`; CONV_SING; FUN_EQ_THM;
 323  IN_ELIM_THM] THEN REWRITE_TAC[ IN_ACT_SING] THEN REWRITE_TAC[NOV10] THEN
 324 REWRITE_TAC[conv; sgn_ge; affsign; lin_combo] THEN
 325 REWRITE_TAC[UNION_EMPTY; IN_SET2] THEN
 326 ONCE_REWRITE_TAC[ MESON[]`  ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
 327   ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`] THEN
 328 REWRITE_TAC[ MESON[VSUM_DIS2; SUM_DIS2]` ~(x = y) /\x' = vsum {x, y} ff /\ l /\
 329 sum {x, y} f = &1 <=> ~(x = y) /\ x' = ff x + ff y /\ l /\ f x + f y = &1 `] THEN
 330 REWRITE_TAC[ MESON[]` (!w. w = x \/ w = y ==> &0 <= f w) <=> &0 <= f x /\ &0 <= f y`]
 331 THEN ONCE_REWRITE_TAC[ GSYM (MESON[]`  ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
 332   ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`)] THEN
 333 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN REWRITE_TAC[ TRUONG_LEMMA]);;
 334
 335 let LE_OF_ZPGPXNN = prove(` ! a b v v1 v2 . &0 <= a /\ &0 <= b /\ a + b = &1 /\
 336  v = a % v1 + b % v2  ==> dist ( v,v1) + dist (v,v2) = dist(v1,v2)`,
 337 SIMP_TAC[dist; REAL_ARITH ` a + b = &1 <=> b = &1 - a `] THEN
 338 REWRITE_TAC[VECTOR_ARITH ` (a % v1 + (&1 - a) % v2) - v1 = ( a - &1 )%( v1 - v2)`] THEN
 339 REWRITE_TAC[VECTOR_ARITH` (a % v1 + (&1 - a) % v2) - v2 = a % ( v1 - v2) `] THEN
 340 SIMP_TAC[NORM_MUL; GSYM REAL_ABS_REFL] THEN REWRITE_TAC[ REAL_ARITH ` abs ( a - &1 )
 341  = abs ( &1 - a ) `] THEN REAL_ARITH_TAC);;
 342
 343 let LENGTH_EQUA = prove(` ! v v1 v2. v IN conv {v1,v2} ==> dist (v,v1) +
 344  dist (v,v2) = dist (v1,v2) `,REWRITE_TAC[CONV_SET2; IN_ELIM_THM] THEN
 345 MESON_TAC[LE_OF_ZPGPXNN]);;
 346
 347 (* lemma 10. p 14 *)
 348 let ZPGPXNN = prove(`!v1 v2 v. dist (v1,v2) < dist (v,v1) + dist (v,v2) ==>
 349  ~(v IN conv {v1, v2})`,
 350 REWRITE_TAC[MESON[] `a ==> ~ b <=> ~(a /\ b )`] THEN REWRITE_TAC[CONV_SET2; IN_ELIM_THM]
 351 THEN MESON_TAC[LE_OF_ZPGPXNN; REAL_ARITH ` a < b ==> ~ ( a = b ) `]);;
 352
 353 let REDUCE_T2 = MESON[]` !P Q.
 354      (!v1 v2 v3 t1 t2 t3. P v1 t1 v2 t2 v3 t3 <=> P v2 t2 v1 t1 v3 t3) /\
 355      (!v1 v2 v3. Q v1 v2 v3 <=> Q v2 v1 v3) /\
 356      (!v1 v2 v3 t1 t2 t3.
 357           ~(t1 = &0 /\ t3 = &0) /\ P v1 t1 v2 t2 v3 t3 ==> Q v1 v2 v3)
 358      ==> (!v1 v2 v3 t1 t2 t3.
 359               ~(t1 = &0 /\ t2 = &0 /\ t3 = &0) /\ P v1 t1 v2 t2 v3 t3
 360               ==> Q v1 v2 v3)`;;
 361
 362 let VEC_PER2_3 = VECTOR_ARITH `((a:real^N ) + b + c = b + a + c)/\
 363    ( (a:real^N ) + b + c = c + b + a )`;;
 364 let PER2_IN3 = SET_RULE `  {a,b,c} = {b,a,c} /\ {a,b,c} = {c,b,a}`;;
 365
 366 let REDUCE_T3 = MESON[]`!P Q.
 367      (!v1 v2 v3 t1 t2 t3. P v1 t1 v2 t2 v3 t3 <=> P v3 t3 v2 t2 v1 t1) /\
 368      (!v1 v2 v3. Q v1 v2 v3 <=> Q v3 v2 v1) /\
 369      (!v1 v2 v3 t1 t2 t3. ~(t1 = &0) /\ P v1 t1 v2 t2 v3 t3 ==> Q v1 v2 v3)
 370      ==> (!v1 v2 v3 t1 t2 t3.
 371               ~(t1 = &0 /\ t3 = &0) /\ P v1 t1 v2 t2 v3 t3 ==> Q v1 v2 v3)`;;
 372
 373 let SUB_PACKING = prove(`!sub s.
 374      packing s /\ sub SUBSET s
 375      ==> (!x y. x IN sub /\ y IN sub /\ ~(x = y) ==> &2 <= dist3 x y)`,
 376 REWRITE_TAC[ packing; GSYM dist3] THEN SET_TAC[]);;
 377
 378
 379 let PAIR_EQ_EXPAND =
 380  SET_RULE `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`;;
 381
 382 let IN_SET3 = SET_RULE ` x IN {a,b,c} <=> x = a \/ x = b \/ x = c `;;
 383 let IN_SET4 = SET_RULE ` x IN {a,b,c,d} <=> x = a \/ x = b \/ x = c \/ x = d `;;
 384
 385 (* le 8. p 13 *)
 386 let SGFCDZO = prove(`! (v1:real^3) v2 v3 t1 t2 t3.
 387      t1 % v1 + t2 % v2 + t3 % v3 = vec 0 /\
 388      t1 + t2 + t3 = &0 /\
 389      ~(t1 = &0 /\ t2 = &0 /\ t3 = &0)
 390      ==> collinear {v1, v2, v3}`,
 391 ONCE_REWRITE_TAC[MESON[]` a /\ b/\c <=> c /\ a /\ b `] THEN
 392 MATCH_MP_TAC REDUCE_T2 THEN
 393 CONJ_TAC THENL [SIMP_TAC[VEC_PER2_3; REAL_ADD_AC]; CONJ_TAC THENL
 394   [SIMP_TAC[PER2_IN3]; MATCH_MP_TAC REDUCE_T3]] THEN
 395 CONJ_TAC THENL [SIMP_TAC[REAL_ADD_AC; VEC_PER2_3];
 396 CONJ_TAC THENL [SIMP_TAC[PER2_IN3];  REWRITE_TAC[]]] THEN
 397 REPEAT GEN_TAC THEN REWRITE_TAC[collinear] THEN
 398 STRIP_TAC THEN EXISTS_TAC `v2 - (v3:real^3)` THEN
 399 ONCE_REWRITE_TAC[MESON[]` x IN s /\ y IN s <=>
 400   ( x = y \/ ~ ( x = y))/\ x IN s /\ y IN s `] THEN
 401 REWRITE_TAC[IN_SET3] THEN REPEAT GEN_TAC THEN
 402 REWRITE_TAC[MESON[]` (a \/ b) /\ c ==> d <=> (a /\ c ==> d) /\ (b /\ c ==> d)`]
 403 THEN CONJ_TAC THENL [DISCH_TAC THEN EXISTS_TAC `&0` THEN
 404 FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC (MESON[]` (a ==> c) ==> a /\ b ==> c `) THEN
 405 MESON_TAC[VECTOR_MUL_LZERO; VECTOR_SUB_EQ]; STRIP_TAC] THENL [
 406
 407 ASM_MESON_TAC[] ;
 408
 409 EXISTS_TAC ` t3  / t1 ` THEN ASM_SIMP_TAC[] THEN STRIP_TR THEN
 410 ONCE_REWRITE_TAC[MESON[VECTOR_MUL_LCANCEL]`
 411   ~(t1 = &0) /\ a ==> x = y <=> ~(t1 = &0) /\ a ==> t1 % x = t1 % y`] THEN
 412 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN SIMP_TAC[REAL_DIV_LMUL] THEN
 413 ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
 414 REWRITE_TAC[ VECTOR_ARITH ` ( a + b + (c:real^N) ) - vec 0 = vec 0 <=>
 415   a = -- ( b + c ) `; REAL_ARITH` a + b + c = &0 <=> a = -- ( b + c ) `] THEN
 416 SIMP_TAC[VECTOR_SUB_LDISTRIB] THEN
 417 MESON_TAC[VECTOR_ARITH ` --(t2 % v2 + t3 % v3) - --(t2 + t3) % v2 -
 418   (t3 % v2 - t3 % v3) = vec 0`];
 419
 420 EXISTS_TAC ` ( -- t2 ) / t1 ` THEN ASM_SIMP_TAC[] THEN STRIP_TR THEN
 421 ONCE_REWRITE_TAC[MESON[VECTOR_MUL_LCANCEL]`
 422   ~(t1 = &0) /\ a ==> x = y <=> ~(t1 = &0) /\ a ==> t1 % x = t1 % y`] THEN
 423 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN SIMP_TAC[REAL_DIV_LMUL] THEN
 424 ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
 425 REWRITE_TAC[ VECTOR_ARITH ` ( a + b + (c:real^N) ) - vec 0 = vec 0 <=>
 426   a = -- ( b + c ) `; REAL_ARITH` a + b + c = &0 <=> a = -- ( b + c ) `] THEN
 427 SIMP_TAC[VECTOR_SUB_LDISTRIB] THEN
 428 MESON_TAC[VECTOR_ARITH ` --(t2 % v2 + t3 % v3) - --(t2 + t3) % v3 -
 429  (--t2 % v2 - --t2 % v3) =  vec 0`];
 430
 431
 432 EXISTS_TAC ` ( -- t3) / t1 ` THEN ASM_SIMP_TAC[] THEN STRIP_TR THEN
 433 ONCE_REWRITE_TAC[MESON[VECTOR_MUL_LCANCEL]`
 434   ~(t1 = &0) /\ a ==> x = y <=> ~(t1 = &0) /\ a ==> t1 % x = t1 % y`] THEN
 435 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN SIMP_TAC[REAL_DIV_LMUL] THEN
 436 ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
 437 REWRITE_TAC[ VECTOR_ARITH ` ( a + b + (c:real^N) ) - vec 0 = vec 0 <=>
 438   a = -- ( b + c ) `; REAL_ARITH` a + b + c = &0 <=> a = -- ( b + c ) `] THEN
 439 SIMP_TAC[VECTOR_SUB_LDISTRIB] THEN MESON_TAC[VECTOR_ARITH ` --(t2 + t3) % v2
 440 - --(t2 % v2 + t3 % v3) - (--t3 % v2 - --t3 % v3) = vec 0`];
 441
 442
 443 ASM_MESON_TAC[];
 444
 445
 446 EXISTS_TAC ` &1 ` THEN ASM_SIMP_TAC[VECTOR_MUL_LID];
 447
 448
 449 EXISTS_TAC ` t2 / t1 ` THEN ASM_SIMP_TAC[] THEN STRIP_TR THEN
 450 ONCE_REWRITE_TAC[MESON[VECTOR_MUL_LCANCEL]`
 451   ~(t1 = &0) /\ a ==> x = y <=> ~(t1 = &0) /\ a ==> t1 % x = t1 % y`] THEN
 452 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN SIMP_TAC[REAL_DIV_LMUL] THEN
 453 ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
 454 REWRITE_TAC[ VECTOR_ARITH ` ( a + b + (c:real^N) ) - vec 0 = vec 0 <=>
 455   a = -- ( b + c ) `; REAL_ARITH` a + b + c = &0 <=> a = -- ( b + c ) `] THEN
 456 SIMP_TAC[VECTOR_SUB_LDISTRIB] THEN
 457 MESON_TAC[VECTOR_ARITH ` --(t2 + t3) % v3 - --(t2 % v2 + t3 % v3) -
 458    (t2 % v2 - t2 % v3) = vec 0`];
 459
 460 EXISTS_TAC ` -- &1 ` THEN ASM_MESON_TAC[VECTOR_ARITH ` v3 - v2 = -- &1 % (v2 - v3)`];
 461
 462
 463 ASM_MESON_TAC[]]);;
 464
 465
 466 (* le 2. p 6 *)
 467 let RHUFIIB = prove( ` !x12 x13 x14 x23 x24 x34.
 468          rho_ij' x12 x13 x14 x23 x24 x34 * ups_x x34 x24 x23 =
 469          chi x12 x13 x14 x23 x24 x34 pow 2 +
 470          &4 * delta x12 x13 x14 x23 x24 x34 * x34 * x24 * x23 `,
 471 REWRITE_TAC[rho_ij'; chi; delta; ups_x] THEN REAL_ARITH_TAC);;
 472
 473
 474 let RIGHT_END_POINT = prove( `!x aa bb.
 475      (?a b. &0 < a /\ b = &0 /\ a + b = &1 /\ x = a % aa + b % bb) <=> x = aa`,
 476 REPEAT GEN_TAC THEN EQ_TAC THENL [STRIP_TR THEN
 477 REWRITE_TAC[ MESON[REAL_ARITH `b = &0 /\ a + b = &1 <=> b= &0 /\ a = &1 `]`
 478    b = &0 /\ a + b = &1 /\ P a b  <=>  b = &0 /\ a = &1 /\ P (&1 ) ( &0 ) `] THEN
 479 MESON_TAC[VECTOR_ARITH ` &1 % aa + &0 % bb = aa `];
 480 DISCH_TAC  THEN EXISTS_TAC ` &1 ` THEN EXISTS_TAC ` &0 ` THEN
 481 REWRITE_TAC[REAL_ARITH ` &0 < &1 /\ &1 + &0 = &1 `] THEN
 482 ASM_MESON_TAC[VECTOR_ARITH ` &1 % aa + &0 % bb = aa `]]);;
 483
 484 let LEFT_END_POINT = prove(` !x aa bb.
 485      (?a b. a = &0 /\ &0 < b /\ a + b = &1 /\ x = &0 % aa + &1 % bb)
 486   <=> x = bb `,
 487 REWRITE_TAC[VECTOR_ARITH ` &0 % aa + &1 % bb = bb `] THEN
 488 MESON_TAC[REAL_ARITH ` &0 = &0 /\ &0 < &1 /\ &0 + &1 = &1 `]);;
 489
 490
 491 let CONV_CONV0 = prove(`! x a b. x IN conv {a,b} <=> x = a \/ x = b \/ x IN conv0 {a,b} `,
 492 REWRITE_TAC[CONV_SET2; CONV0_SET2; IN_ELIM_THM] THEN
 493 REWRITE_TAC[REAL_ARITH ` &0 <= a <=> a = &0 \/ &0 < a `] THEN
 494 KHANANG THEN REWRITE_TAC[EXISTS_OR_THM] THEN
 495 SIMP_TAC[MESON[REAL_ARITH ` ~(a = &0 /\ b = &0 /\ a + b = &1)`]`
 496   ~(a = &0 /\ b = &0 /\ a + b = &1 /\ las )` ] THEN
 497 REWRITE_TAC[MESON[REAL_ARITH ` a = &0 /\ a + b = &1 <=> a = &0 /\ b = &1 `]`
 498   a = &0 /\ &0 < b /\ a + b = &1 /\ x = a % aa + b % ba <=>
 499      a = &0 /\ &0 < b /\ a + b = &1 /\ x = &0 % aa + &1 % ba`] THEN
 500 MESON_TAC[ RIGHT_END_POINT; LEFT_END_POINT]);;
 501
 502
 503 let GONTONG = REWRITE_TAC[REAL_ARITH ` ( a + b ) + c = a + b + c `];;
 504
 505 (* le 27. p 20 *)
 506 let MAEWNPU = prove(` ?b c.
 507          !x12 x13 x14 x23 x24 x34.
 508              delta x12 x13 x14 x23 x24 x34 =
 509              --x12 * x34 pow 2 +
 510              b x12 x13 x14 x23 x24 * x34 +
 511              c x12 x13 x14 x23 x24 `,
 512 REWRITE_TAC[delta; REAL_ARITH ` a - b = a + -- b `;
 513   REAL_ARITH ` a * (b + c )= a * b + a * c ` ] THEN
 514 REWRITE_TAC[REAL_ARITH ` a * b * -- c = -- a * b * c /\ -- ( a * b ) = -- a * b `] THEN
 515 REWRITE_TAC[REAL_ARITH` x12 * x34 * x23 + x12 * x34 * x24 +
 516    --x12 * x34 * x34 = x12 * x34 * x23 + x12 * x34 * x24 +
 517    -- x12 * ( x34 pow 2 )  `] THEN
 518 REWRITE_TAC[REAL_ARITH ` ( a + b ) + c = a + b + c `] THEN
 519 REWRITE_TAC[REAL_ARITH ` a + b * c pow 2 + d = b * c pow 2 + a + d `] THEN
 520 ONCE_REWRITE_TAC[REAL_ARITH `a + b + c + d + e = a + d + b + c + e `] THEN
 521 REWRITE_TAC[REAL_ARITH ` a * b * c = ( a * b ) * c `] THEN
 522 REPLICATE_TAC 30 ( ONCE_REWRITE_TAC[REAL_ARITH ` a * x pow 2 + b * x + d + e
 523   = a * x pow 2 + b * x + e + d `] THEN GONTONG THEN REWRITE_TAC[ REAL_ARITH
 524  ` a * x pow 2 + b * x + d * x  + e = a * x pow 2 + ( b  +  d)  * x  + e`]) THEN
 525 REPLICATE_TAC 50 ( ONCE_REWRITE_TAC[REAL_ARITH ` a * x pow 2 + b * x + d + e
 526   = a * x pow 2 + b * x + e + d `] THEN GONTONG THEN ONCE_REWRITE_TAC[ REAL_ARITH ` a * x pow 2 + b * x + (d * x) * h  + e
 527  = a * x pow 2 + ( b  +  d * h )  * x  + e`]) THEN
 528 EXISTS_TAC ` (\ x12 x13 x14 x23 x24. --x13 * x14 +
 529           --x23 * x24 +
 530           x13 * x24 +
 531           x14 * x23 +
 532           --x12 * x12 +
 533           x12 * x14 +
 534           x12 * x24 +
 535           x12 * x13 +
 536           x12 * x23 ) ` THEN
 537 EXISTS_TAC ` (\ x12 x13 x14 x23 x24. (x14 * x23) * x12 +
 538          (x14 * x23) * x13 +
 539          (--x14 * x23) * x14 +
 540          (--x14 * x23) * x23 +
 541          (x14 * x23) * x24 +
 542          (--x12 * x13) * x23 +
 543          (--x12 * x14) * x24 +
 544          (x13 * x24) * x12 +
 545          (--x13 * x24) * x13 +
 546          (x13 * x24) * x14 +
 547          (x13 * x24) * x23 +
 548          (--x13 * x24) * x24 ) ` THEN
 549 SIMP_TAC[]);;
 550
 551 (* ----new ------- *)
 552
 553 let DELTA_COEFS = new_specification ["b_coef"; "c_coef"] MAEWNPU;;
 554
 555
 556 let DELTA_X34 = prove(` !x12 x13 x14 x23 x24 x34.
 557      delta x12 x13 x14 x23 x24 x34 =
 558      --x12 * x34 pow 2 +
 559      (--x13 * x14 +
 560       --x23 * x24 +
 561       x13 * x24 +
 562       x14 * x23 +
 563       --x12 * x12 +
 564       x12 * x14 +
 565       x12 * x24 +
 566       x12 * x13 +
 567       x12 * x23) *
 568      x34 +
 569      (x14 * x23) * x12 +
 570      (x14 * x23) * x13 +
 571      (--x14 * x23) * x14 +
 572      (--x14 * x23) * x23 +
 573      (x14 * x23) * x24 +
 574      (--x12 * x13) * x23 +
 575      (--x12 * x14) * x24 +
 576      (x13 * x24) * x12 +
 577      (--x13 * x24) * x13 +
 578      (x13 * x24) * x14 +
 579      (x13 * x24) * x23 +
 580      (--x13 * x24) * x24`, REWRITE_TAC[delta] THEN REAL_ARITH_TAC);;
 581
 582 let C_COEF_FORMULA = prove(`! x12 x13 x14 x23 x24. c_coef x12 x13 x14 x23 x24
 583   = (x14 * x23) * x12 +
 584          (x14 * x23) * x13 +
 585          (--x14 * x23) * x14 +
 586          (--x14 * x23) * x23 +
 587          (x14 * x23) * x24 +
 588          (--x12 * x13) * x23 +
 589          (--x12 * x14) * x24 +
 590          (x13 * x24) * x12 +
 591          (--x13 * x24) * x13 +
 592          (x13 * x24) * x14 +
 593          (x13 * x24) * x23 +
 594          (--x13 * x24) * x24`, MP_TAC DELTA_COEFS THEN
 595 NHANH (MESON[]` (!x12 x13 x14 x23 x24 x34. p x12 x13 x14 x23 x24 x34)
 596   ==> (! x12 x13 x14 x23 x24. p x12 x13 x14 x23 x24 (&0) ) `) THEN
 597 REWRITE_TAC[DELTA_X34] THEN
 598 REWRITE_TAC[REAL_ARITH ` &0 pow 2 = &0 `; REAL_MUL_RZERO; REAL_ADD_LID] THEN
 599 SIMP_TAC[]);;
 600
 601 let BC_DEL_FOR = prove(` ! x12 x13 x14 x23 x24. b_coef x12 x13 x14 x23 x24 =
 602   --x13 * x14 +
 603           --x23 * x24 +
 604           x13 * x24 +
 605           x14 * x23 +
 606           --x12 * x12 +
 607           x12 * x14 +
 608           x12 * x24 +
 609           x12 * x13 +
 610           x12 * x23 /\
 611   c_coef x12 x13 x14 x23 x24 =
 612          (x14 * x23) * x12 +
 613          (x14 * x23) * x13 +
 614          (--x14 * x23) * x14 +
 615          (--x14 * x23) * x23 +
 616          (x14 * x23) * x24 +
 617          (--x12 * x13) * x23 +
 618          (--x12 * x14) * x24 +
 619          (x13 * x24) * x12 +
 620          (--x13 * x24) * x13 +
 621          (x13 * x24) * x14 +
 622          (x13 * x24) * x23 +
 623          (--x13 * x24) * x24 `, REWRITE_TAC[C_COEF_FORMULA] THEN
 624 MP_TAC DELTA_COEFS THEN NHANH (MESON[]` (!x12 x13 x14 x23 x24 x34.
 625 p x12 x13 x14 x23 x24 x34)
 626   ==> (! x12 x13 x14 x23 x24. p x12 x13 x14 x23 x24 (&1) ) `) THEN
 627 REWRITE_TAC[DELTA_X34; C_COEF_FORMULA] THEN
 628 REWRITE_TAC[REAL_ARITH ` a + b + c = a + b' + c <=> b = b' `] THEN
 629 SIMP_TAC[REAL_RING` a * &1 = a `]);;
 630
 631 (*
 632 let AGBWHRD = prove(` !x12 x13 x14 x23 x24 x12 x13 x14 x23 x24.
 633          b_coef x12 x13 x14 x23 x24 pow 2 +
 634          &4 * x12 * c_coef x12 x13 x14 x23 x24 =
 635          ups_x x12 x23 x13 * ups_x x12 x24 x14`, REWRITE_TAC[BC_DEL_FOR; ups_x] THEN
 636 REAL_ARITH_TAC);;
 637 *)
 638
 639 let COLLINEAR_EX = prove(` ! x y (z:real^3) . collinear {x,y,z} <=> ( ? a b c. a + b + c = &0 /\ ~ ( a = &0 /\
 640 b = &0 /\ c = &0 ) /\ a % x + b % y + c % z = vec 0 ) `,
 641 REWRITE_TAC[collinear] THEN
 642 REPEAT GEN_TAC THEN
 643 STRIP_TR THEN
 644 EQ_TAC THENL [
 645 NHANH (SET_RULE` (!x' y'. x' IN {x, y, z} /\ y' IN {x, y, z} ==> P x' y' )
 646     ==> P x y /\ P x z `) THEN
 647 STRIP_TR THEN
 648 DISJ_CASES_TAC (MESON[]` c = &0 /\ c' = &0 \/ ~( c = &0 /\ c' = &0  ) `) THENL [
 649 ASM_SIMP_TAC[VECTOR_ARITH ` x - y = &0 % t <=> y = x`] THEN
 650 DISCH_TAC THEN
 651 EXISTS_TAC ` &1 ` THEN EXISTS_TAC ` &1 ` THEN
 652 EXISTS_TAC ` -- &2 ` THEN
 653 REWRITE_TAC[REAL_ARITH ` &1 + &1 + -- &2 = &0 /\
 654  ~(&1 = &0 /\ &1 = &0 /\ -- &2 = &0)`; VECTOR_ARITH` &1 % x + &1 % x +
 655   -- &2 % x = vec 0`];
 656
 657
 658
 659 NHANH (MESON[VECTOR_MUL_LCANCEL]` x = c % u /\
 660   y  = c' % u ==> c' % x = c' % (c % u) /\ c % y = c % c' % u `) THEN
 661 REWRITE_TAC[VECTOR_ARITH ` x = c' % c % u /\ y = c % c' % u <=>
 662    x = y /\ y = c % c' % u`] THEN
 663 REWRITE_TAC[VECTOR_ARITH ` c' % (x - y) = c % (x - z) <=> (c - c' ) % x + c' % y +
 664   -- c % z = vec 0 `] THEN
 665 ASM_MESON_TAC[REAL_ARITH ` (( c - b ) + b + -- c = &0 ) /\ (~( c = &0 )
 666    <=> ~( -- c = &0 ))`]];REWRITE_TAC[GSYM collinear] THEN MESON_TAC[SGFCDZO]]);;
 667
 668
 669 let MAX_REAL_LESS_EX = prove(`!x y a. max_real x y <= a <=> x <= a /\ y <= a`,
 670 REWRITE_TAC[max_real; COND_EXPAND; COND_ELIM_THM;COND_RAND; COND_RATOR] THEN
 671 REPEAT GEN_TAC THEN
 672 MESON_TAC[REAL_ARITH ` (~ ( b < a ) /\ b <= c ==> a <= c)`;  REAL_ARITH ` a < b /\ b <= c ==> a <= c `]);;
 673
 674
 675 let MAX_REAL3_LESS_EX = prove(`! x y z a. max_real3 x y z <= a <=> x <= a /\
 676 y <= a /\ z <= a `, REWRITE_TAC[max_real3; MAX_REAL_LESS_EX] THEN MESON_TAC[]);;
 677
 678
 679 MESON[]` (!x y z.
 680           (P x y z <=> P y x z) /\
 681           (P x y z <=> P x z y) /\
 682           (Q x y z <=> Q y x z) /\
 683           (Q x y z <=> Q x z y)) /\
 684      (!x y z. P x y z ==> Q x y z)
 685      ==> (!x y z. P x y z ==> Q x y z /\ Q y x z /\ Q z x y)`;;
 686 (* ========== *)
 687
 688 let UPS_X_SYM = prove(` ! x y z. ups_x x y z = ups_x y x z /\
 689   ups_x x y z = ups_x x z y `, REWRITE_TAC[ups_x] THEN REAL_ARITH_TAC);;
 690
 691 let PER_MUL3 = REAL_ARITH ` a*b*c = b * a * c /\ a *b *c = a * c * b `;;
 692
 693 let ETA_X_SYM = prove(` ! x y z. &0 <= x /\ &0 <= y /\ &0 <= z /\ &0 <= ups_x x y z ==>
 694   eta_x x y z = eta_x y x z /\ eta_x x y z = eta_x x z y `,
 695 REWRITE_TAC[eta_x] THEN
 696 NHANH (MESON[UPS_X_SYM]` &0 <= ups_x x y z ==> &0 <= ups_x y x z
 697   /\ &0 <= ups_x x z y `) THEN
 698 NHANH (MESON[REAL_LE_MUL]`&0 <= x /\ &0 <= y /\ &0 <= z /\ las ==>
 699   &0 <= x * y * z`) THEN
 700 PHA THEN NHANH (MESON[REAL_LE_DIV; REAL_ARITH ` a * b * c = b * a * c
 701   /\ a * b * c = a * c * b `]`
 702   &0 <= ups_x x y z /\ &0 <= aa /\ &0 <= bb /\ &0 <= x * y * z
 703      ==> &0 <= (x * y * z) / ups_x x y z /\
 704          &0 <= (y * x * z) / aa /\
 705          &0 <= (x * z * y) / bb`) THEN
 706 SIMP_TAC[SQRT_INJ] THEN
 707 MESON_TAC[UPS_X_SYM; PER_MUL3]);;
 708
 709 let ETA_Y_SYM = prove(` ! x y z. &0 <= ups_x (x * x) (y * y) (z * z) ==>
 710   eta_y x y z = eta_y y x z /\ eta_y x y z = eta_y x z y `,
 711 REWRITE_TAC[eta_y] THEN REPEAT LET_TAC THEN MESON_TAC[ETA_X_SYM; REAL_LE_SQUARE]);;
 712
 713
 714
 715 let ETA_Y_SYMM = MESON[UPS_X_SYM; ETA_Y_SYM]` ! x y z. &0 <= ups_x (x * x) (y * y) (z * z)
 716    ==> eta_y x y z = eta_y x z y /\
 717          eta_y x y z = eta_y y x z /\
 718          eta_y x y z = eta_y z x y /\
 719          eta_y x y z = eta_y y z x /\
 720          eta_y x y z = eta_y z y x`;;
 721
 722
 723 let IMPLY_POS = prove(`! x y z . &0 <= ups_x (x * x) (y * y) (z * z) ==>
 724   &0 <= ((z * z) * (x * x) * y * y) / ups_x (z * z) (x * x) (y * y) /\
 725   &0 <= ((x * x) * (y * y) * z * z) / ups_x (x * x) (y * y) (z * z) /\
 726   &0 <= ((y * y) * (z * z) * x * x) / ups_x (y * y) (z * z) (x * x) `, MP_TAC
 727  REAL_LE_SQUARE THEN MP_TAC REAL_LE_MUL THEN MESON_TAC[UPS_X_SYM; REAL_LE_DIV]);;
 728
 729 let POW2_COND = MESON[REAL_ABS_REFL; REAL_LE_SQUARE_ABS]` ! a b. &0 <= a /\ &0 <= b ==>
 730 ( a <= b <=> a pow 2 <= b pow 2 ) `;;
 731
 732
 733 let TRUONGG = prove(`! x y z. &0 < ups_x_pow2 z x y ==>
 734  ((z * z) * (x * x) * y * y) / ups_x (z * z) (x * x) (y * y) -
 735     z pow 2 / &4 = ( z pow 2 * (( z pow 2 - x pow 2 - y pow 2 ) pow 2 ))
 736    / (&4 * ups_x_pow2 z x y )`,
 737 REWRITE_TAC[ups_x; ups_x_pow2] THEN CONV_TAC REAL_FIELD);;
 738
 739 let RE_TRUONGG = REWRITE_RULE[GSYM ups_x_pow2] TRUONGG;;
 740
 741 let HVXIKHW = prove(` !x y z.
 742          &0 <= x /\ &0 <= y /\ &0 <= z /\ &0 < ups_x_pow2 x y z
 743          ==> max_real3 x y z / &2 <= eta_y x y z`,
 744 REWRITE_TAC[REAL_ARITH` a / &2 <= b <=> a <= &2 * b `; MAX_REAL3_LESS_EX] THEN
 745 REWRITE_TAC[eta_x; ups_x_pow2] THEN
 746 NHANH (REAL_ARITH` &0 < a ==> &0 <= a `) THEN
 747 DAO THEN REPEAT GEN_TAC THEN
 748 REWRITE_TAC[MESON[ETA_Y_SYMM]` &0 <= ups_x (x * x) (y * y) (z * z) /\ las
 749  ==> z <= &2 * eta_y x y z /\ x <= &2 * eta_y x y z /\ y <= &2 * eta_y x y z
 750   <=> &0 <= ups_x (x * x) (y * y) (z * z) /\ las
 751  ==> z <= &2 * eta_y z x y /\ x <= &2 * eta_y x y z /\ y <= &2 * eta_y y z x`] THEN
 752 REWRITE_TAC[eta_y] THEN CONV_TAC (TOP_DEPTH_CONV let_CONV) THEN REWRITE_TAC[eta_x]
 753 THEN NHANH (SPEC_ALL IMPLY_POS) THEN
 754 NHANH (SPEC_ALL (prove(` ! a b x y. &0 <= a / b /\ &0 <= x /\ &0 <= y ==>
 755    &0 <=  &2 * sqrt ( a/b) /\ &0 <= &2 * sqrt x /\ &0 <= &2 * sqrt y `,
 756 REWRITE_TAC[REAL_ARITH ` &0 <= &2 * a <=> &0 <= a `] THEN
 757 SIMP_TAC[SQRT_WORKS]))) THEN SIMP_TAC[POW2_COND] THEN
 758 REWRITE_TAC[REAL_ARITH ` x <= ( &2 * y ) pow 2 <=> x / &4 <= y pow 2 `] THEN
 759 SIMP_TAC[ SQRT_POW_2] THEN REWRITE_TAC[ GSYM ups_x_pow2] THEN
 760 REWRITE_TAC[REAL_FIELD` a / b <= c <=> &0 <= c - a / b `] THEN
 761 SIMP_TAC[ups_x_pow2; UPS_X_SYM; RE_TRUONGG] THEN DAO THEN
 762 MATCH_MP_TAC (MESON[]` (a4 ==> l) ==> (a1/\a2/\a3/\a4/\a5) ==> l `) THEN
 763 MP_TAC REAL_LE_SQUARE THEN MP_TAC REAL_LE_MUL THEN MP_TAC REAL_LE_DIV THEN
 764 REWRITE_TAC[GSYM REAL_POW_2] THEN MESON_TAC[REAL_ARITH ` &0 < a ==> &0 <= &4 * a `]);;
 765
 766
 767 let EXISTS_INV = REAL_FIELD` ~( a = &0 ) <=> a * &1 / a = &1 /\ &1 / a * a = &1 `;;
 768
 769
 770 let REAL_LT_RDIV_0 = prove( `!y z. &0 < z ==> (&0 < (y / z) <=> &0 < y)`,
 771   MESON_TAC[REAL_LT_DIV;REAL_LT_MUL;REAL_DIV_RMUL;REAL_ARITH `&0 < x==> ~(x= &0)`]);;
 772
 773 let POS_EQ_INV_POS = prove(`!x. &0 < x <=> &0 < &1 / x`, GEN_TAC THEN EQ_TAC
 774 THENL [REWRITE_TAC[MESON[REAL_LT_RDIV_0; REAL_ARITH ` &0 < &1 `]`! b.  &0 < b
 775    ==> &0 < &1 / b `];REWRITE_TAC[] THEN
 776 MESON_TAC[MESON[REAL_LT_RDIV_0; REAL_ARITH ` &0 < &1 `]` &0 < b
 777     ==> &0 < &1 / b `; REAL_FIELD ` &1 / ( &1 / x ) = x ` ]]);;
 778
 779
 780 let MIDDLE_POINT = prove(` ! x y (z:real^3) . collinear {x,y,z} ==> x IN conv {y,z} \/
 781 y IN conv {x,z} \/  z IN conv {x,y} `, REWRITE_TAC[COLLINEAR_EX] THEN REPEAT
 782 GEN_TAC THEN
 783 MATCH_MP_TAC (prove(`(!(a:real) (b:real) (c:real). P a b c <=> P (--a) (--b) (--c)) /\
 784    ((?a b c. &0 <= a /\ P a b c) ==> l) ==>  ( ? a b c. P a b c ) ==> l `,
 785  DISCH_TAC THEN ASM_MESON_TAC[REAL_ARITH ` ! a. a <= &0 \/ &0 <= a`;
 786    REAL_ARITH ` a <= &0 <=> &0 <= -- a `])) THEN
 787 CONJ_TAC THENL [MESON_TAC[REAL_ARITH` a = &0 <=> -- a = &0 `; REAL_ARITH ` a + b + c = &0
 788   <=> --a + --b + --c = &0`; VECTOR_ARITH ` a % x + b % y + c % z = vec 0
 789   <=> --a % x + --b % y + --c % z = vec 0 `]; STRIP_TAC] THEN
 790 DISJ_CASES_TAC (REAL_ARITH ` &0 < b \/ b <= &0`) THENL
 791 [STRIP_TR THEN REWRITE_TAC[VECTOR_ARITH ` a + b + c % z = vec 0 <=>
 792   --c % z = a + b `] THEN
 793 NHANH (MESON[VECTOR_MUL_LCANCEL]` a % x = y ==> (&1 / a) % a % x = &1 / a % y `) THEN
 794 REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
 795 REWRITE_TAC[MESON[]` a1/\a2/\a3/\a4/\a5 ==> l <=> a1 /\ a5 /\ a2 ==>
 796   a3/\a4 ==> l `] THEN
 797 NHANH (REAL_FIELD ` &0 <= a /\ &0 < b /\ a + b + c = &0 ==>
 798   a / ( -- c ) + b /( -- c ) = &1 /\ ~ ( -- c = &0 )/\ &0 < -- c `) THEN
 799 SIMP_TAC[EXISTS_INV] THEN
 800 ONCE_REWRITE_TAC[MESON[POS_EQ_INV_POS]` a /\ &0 < c <=> a /\ &0 < &1 / c `] THEN
 801 REWRITE_TAC[VECTOR_MUL_LID; CONV_SET2; IN_ELIM_THM; GSYM (REAL_ARITH` a / b =
 802    &1 / b * a `)] THEN
 803 ONCE_REWRITE_TAC[REAL_ARITH` a / b = &1 / b * a `] THEN
 804 MP_TAC (GEN_ALL (MESON[REAL_ARITH`( a * &1 = a ) /\ ( &0 < a ==> &0 <= a )`;
 805  REAL_LE_MUL]` &0 < &1 / c * &1 /\ ( &0 <= a \/ &0 < a ) ==> &0 <= &1 / c * a `)) THEN
 806 MESON_TAC[]; STRIP_TR THEN
 807 NHANH (MESON[REAL_ARITH` &0 <= c \/ c <= &0`]` a + b + v = &0 ==>
 808   &0 <= v \/ v <= &0 `) THEN
 809 REWRITE_TAC[MESON[]` a1/\(a2 /\ (aa\/ bb))/\ dd <=>
 810   (aa\/bb) /\ a1/\a2/\dd`] THEN SPEC_TAC (`a:real`, `a:real`) THEN
 811 SPEC_TAC (`b:real`, `b:real`) THEN SPEC_TAC (`c:real`, `c:real`) THEN
 812 KHANANG THEN REWRITE_TAC[(prove( `&0 <= c /\ &0 <= a /\ a + b + c = &0 /\
 813  ~(a = &0 /\ b = &0 /\ c = &0) /\ a % x + b % y + c % z = vec 0 /\
 814  b <= &0 <=> --a <= &0 /\ &0 <= --b /\ --b + --c + --a = &0 /\
 815  ~(--b = &0 /\ --c = &0 /\ --a = &0) /\ --b % y + --c % z + -- a % x = vec 0 /\
 816  --c <= &0`, MESON_TAC[
 817 REAL_ARITH ` (a = &0 <=> --a = &0) /\ ( b <= &0 <=> &0 <= -- b ) /\
 818      (&0 <= a <=> --a <= &0) /\
 819      (a + b + c = &0 <=> --b + --c + -- a = &0)`;
 820 VECTOR_ARITH` a % x + b % y + c % z = vec 0 <=>
 821  --b % y + --c % z + --a % x = vec 0 `]))] THEN
 822 REWRITE_TAC[MESON[]` a \/ b ==> c <=> (a ==> c) /\(b==>c)`] THEN
 823 REWRITE_TAC[MESON[REAL_ARITH `&0 <= a <=> a = &0 \/ &0 < a `]`
 824   c <= &0 /\ &0 <= a /\ l <=> ( a = &0 \/ &0 < a ) /\ c <= &0 /\ l`] THEN
 825 KHANANG THEN
 826 REWRITE_TAC[MESON[REAL_ARITH `a = &0 /\ c <= &0 /\ a + b + c = &0 /\ b <= &0
 827      ==> a = &0 /\ b = &0 /\ c = &0`]`a = &0 /\      c <= &0 /\
 828       a + b + c = &0 /\ ~(a = &0 /\ b = &0 /\ c = &0) /\a2/\ b <= &0 <=> F `] THEN
 829 NHANH (MESON[REAL_FIELD ` &0 < a /\
 830          a + b + c = &0 ==> -- b / a + -- c / a = &1 `]`&0 < a /\      c <= &0 /\
 831       a + b + c = &0 /\ l ==> --b / a + --c / a = &1 `) THEN
 832 REWRITE_TAC[VECTOR_ARITH `  a % x + b % y + c % z = vec 0 <=>
 833   a % x = -- b % y + -- c % z `] THEN
 834 NHANH (MESON[VECTOR_MUL_LCANCEL]` a % x = y ==> &1 / a % a % x = &1 / a % y `) THEN
 835 REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_ARITH ` &1 / a * b
 836   = b / a `;VECTOR_MUL_LID ] THEN PHA THEN
 837 PURE_ONCE_REWRITE_TAC[MESON[REAL_FIELD ` &0 < a ==> a / a = &1`]`
 838    &0 < a /\ P ( a / a) <=> &0 < a /\ P ( &1 ) `] THEN
 839 REWRITE_TAC[VECTOR_MUL_LID ] THEN
 840 REWRITE_TAC[MESON[SET_RULE ` {a,b} = {b,a}`]` y IN conv {x, z} \/ z IN conv {x, y}
 841   <=> y IN conv {z,x} \/ z IN conv {x,y} `] THEN
 842 REWRITE_TAC[CONV_SET2; IN_ELIM_THM] THEN
 843 REWRITE_TAC[ REAL_ARITH ` a <= &0 <=> &0 <= -- a `] THEN
 844 MESON_TAC[REAL_LE_DIV; REAL_ARITH ` &0 < a ==> &0 <= a `]]);;
 845
 846 let IN_CONV_COLLINEAR = prove(` ! (v:real^3) v1 v2. v IN conv {v1,v2} ==>
 847 collinear {v,v1,v2} `, REWRITE_TAC[COLLINEAR_EX] THEN
 848 REWRITE_TAC[COLLINEAR_EX; CONV_SET2; IN_ELIM_THM] THEN
 849 REWRITE_TAC[VECTOR_ARITH ` v = a % v1 + b % v2 <=>
 850    &1 % v + -- a % v1 + -- b % v2 = vec 0 `] THEN
 851 MESON_TAC[REAL_ARITH `~ ( &1 = &0 ) /\ (a + b = &1 <=> &1 + --a + --b = &0 )`]);;
 852
 853 let PER_SET3 = SET_RULE ` {a,b,c} = {a,c,b} /\ {a,b,c} = {b,a,c} /\
 854   {a,b,c} = {c,a,b} /\ {a,b,c} = {b,c,a} /\ {a,b,c} = {c,b,a} `;;
 855
 856 let COLLINERA_AS_IN_CONV2 = prove(` ! x y (z:real^3) . collinear {x,y,z} <=>
 857 x IN conv {y,z} \/
 858 y IN conv {x,z} \/  z IN conv {x,y}`,
 859 MESON_TAC[PER_SET3; IN_CONV_COLLINEAR; MIDDLE_POINT]);;
 860
 861 let LENGTH_EQ_EX = prove(`!v v1 v2.
 862      dist (v1,v) + dist (v,v2) = dist (v1,v2) <=>
 863      ~(dist (v1,v2) < dist (v1,v) + dist (v,v2))`,
 864 REPEAT GEN_TAC THEN
 865 REWRITE_TAC[REAL_ARITH ` ~( a < b) <=> b <= a `] THEN
 866 EQ_TAC THENL [REAL_ARITH_TAC;
 867 NHANH (MESON[DIST_TRIANGLE]` dist (v1,v) + dist (v,v2) <= dist (v1,v2)
 868   ==> dist(v1,v2) <= dist (v1,v) + dist (v,v2)`) THEN
 869 REAL_ARITH_TAC]);;
 870
 871
 872 (* HARRISON have proved this lemma as following, but it must be loaded after convex.ml *)
 873
 874 let BETWEEN_IFF_IN_CONVEX_HULL = prove
 875   (`!v v1 v2:real^N.
 876          dist(v1,v) + dist(v,v2) = dist(v1,v2) <=> v IN convex hull {v1,v2}`,
 877    REPEAT GEN_TAC THEN ASM_CASES_TAC  `v1:real^N = v2` THENL
 878     [ASM_REWRITE_TAC[INSERT_AC; CONVEX_HULL_SING; IN_SING] THEN NORM_ARITH_TAC;
 879      REWRITE_TAC[CONVEX_HULL_2_ALT; IN_ELIM_THM] THEN EQ_TAC THENL
 880       [DISCH_TAC THEN EXISTS_TAC `dist(v1:real^N,v) / dist(v1,v2)` THEN
 881        ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_LE_RDIV_EQ; DIST_POS_LT] THEN CONJ_TAC
 882        THENL [FIRST_ASSUM(SUBST1_TAC o SYM) THEN NORM_ARITH_TAC; ALL_TAC] THEN
 883        MATCH_MP_TAC VECTOR_MUL_LCANCEL_IMP THEN
 884        EXISTS_TAC `dist(v1:real^N,v2)` THEN
 885        ASM_SIMP_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB; REAL_SUB_LDISTRIB;
 886                     REAL_DIV_LMUL; DIST_EQ_0] THEN
 887        FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [DIST_TRIANGLE_EQ] o SYM) THEN
 888        FIRST_ASSUM(SUBST1_TAC o SYM) THEN
 889        REWRITE_TAC[dist; REAL_ARITH `(a + b) * &1 - a = b`] THEN
 890        VECTOR_ARITH_TAC;
 891        STRIP_TAC THEN ASM_REWRITE_TAC[dist] THEN
 892        REWRITE_TAC[VECTOR_ARITH `a - (a + b:real^N) = --b`;
 893                    VECTOR_ARITH `(a + u % (b - a)) - b = (&1 - u) % (a - b)`;
 894                    NORM_NEG; NORM_MUL; GSYM REAL_ADD_LDISTRIB] THEN
 895        REWRITE_TAC[NORM_SUB] THEN REPEAT(POP_ASSUM MP_TAC) THEN
 896        CONV_TAC REAL_FIELD]]);;
 897
 898 (* From this, your version follows easily: *)
 899
 900  let BETWEEN_IMP_IN_CONVEX_HULL = prove
 901   (`!v v1 v2. dist(v1,v) + dist(v,v2) = dist(v1,v2)
 902               ==> (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\
 903                          v = a % v1 + b % v2)`,
 904    REWRITE_TAC[BETWEEN_IFF_IN_CONVEX_HULL; CONVEX_HULL_2; IN_ELIM_THM] THEN
 905    REWRITE_TAC[CONJ_ASSOC]);;
 906
 907
 908
 909 let PRE_HE = prove(` ! x y z. let p = ( x + y + z ) / &2 in
 910   ups_x_pow2 x y z = &16 * p * ( p - x ) * ( p - y ) * ( p - z ) `,
 911 CONV_TAC (TOP_DEPTH_CONV let_CONV) THEN
 912 REWRITE_TAC[ups_x_pow2; ups_x] THEN REAL_ARITH_TAC);;
 913
 914 let PRE_HER = prove(`!x y z.
 915      ups_x_pow2 x y z =
 916      &16 *
 917      (x + y + z) / &2 *
 918      ((x + y + z) / &2 - x) *
 919      ((x + y + z) / &2 - y) *
 920      ((x + y + z) / &2 - z)`,
 921 REWRITE_TAC[ups_x_pow2; ups_x] THEN REAL_ARITH_TAC);;
 922
 923
 924 let TRIVIVAL_LE = prove(`!v1 v2 v3.
 925      ~(v2 = v3 /\ v1 = v2)
 926      ==> ~(dist (v1,v2) + dist (v1,v3) + dist (v2,v3) = &0)`,
 927 SIMP_TAC[DE_MORGAN_THM; DIST_NZ] THEN
 928 NHANH (MESON[DIST_POS_LE]`&0 < dist (v2,v3) \/ &0 < dist (v1,v2) ==>
 929   &0 <= dist(v1,v3) `) THEN MP_TAC DIST_POS_LE THEN KHANANG THEN
 930 REWRITE_TAC[OR_IMP_EX] THEN
 931 NHANH (MESON[DIST_POS_LE]`&0 < dist (v2,v3) /\ &0 <= dist (v1,v3)
 932   ==> &0 <= dist(v1,v2) `) THEN
 933 SIMP_TAC[REAL_ARITH`( &0 < a /\ &0 <= b ) /\ &0 <= c ==> ~(c + b + a = &0 ) `] THEN
 934 NHANH (MESON[DIST_POS_LE]`&0 < dist (v1,v2) /\ &0 <= dist (v1,v3) ==>
 935   &0 <= dist(v2,v3) `) THEN
 936 MESON_TAC[REAL_ARITH ` &0 < a /\ &0 <= b /\ &0 <= c ==> ~( a + b + c = &0 ) `]);;
 937
 938
 939
 940 let MID_COND = prove(` ! v v1 v2. v IN conv {v1,v2} <=> dist(v1,v) + dist(v,v2)
 941  = dist(v1,v2) `, REPEAT GEN_TAC THEN EQ_TAC THENL [MESON_TAC[LENGTH_EQUA; DIST_SYM];
 942 REWRITE_TAC[CONV_SET2; IN_ELIM_THM] THEN
 943 MESON_TAC[DIST_SYM; BETWEEN_IMP_IN_CONVEX_HULL]]);;
 944
 945
 946 (* lemma 9. p 13 *)
 947 let FHFMKIY = prove(`!(v1:real^3) v2 v3 x12 x13 x23.
 948          x12 = dist (v1,v2) pow 2 /\
 949          x13 = dist (v1,v3) pow 2 /\
 950          x23 = dist (v2,v3) pow 2
 951          ==> (collinear {v1, v2, v3} <=> ups_x x12 x13 x23 = &0)`,
 952 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[] THEN REWRITE_TAC[COLLINERA_AS_IN_CONV2]
 953  THEN REWRITE_TAC[REAL_ARITH ` x pow 2 = x * x `; GSYM ups_x_pow2] THEN
 954 REWRITE_TAC[PRE_HER] THEN REWRITE_TAC[REAL_ENTIRE] THEN
 955 ONCE_REWRITE_TAC[MESON[]`( v1 IN conv {v2, v3} \/ a \/ b <=> l ) <=>
 956 (v1 = v2 /\ v1 = v3 ) \/  ~(v1 = v2 /\ v1 = v3) ==> ( v1 IN conv {v2, v3}
 957 \/ a \/ b <=> l )`] THEN REWRITE_TAC[OR_IMP_EX] THEN
 958 SIMP_TAC[DIST_SYM; DIST_REFL; MESON[]` a= b/\ a= c <=> b = c /\ a= b`] THEN
 959 SIMP_TAC[SET_RULE ` {a,a} = {a} /\ a IN {a} `; CONV_SING;
 960    REAL_ARITH ` (&0 + &0 + &0)/ &2 = &0 `] THEN SIMP_TAC[ TRIVIVAL_LE;
 961 REAL_ARITH `~( &16 = &0) /\(~( a = &0) ==> ~( a / &2 = &0))`] THEN
 962 REWRITE_TAC[REAL_ARITH ` (a+ b + c ) / &2 - a = &0 <=> b + c = a `] THEN
 963 REWRITE_TAC[REAL_ARITH ` (a+ b + c ) / &2 - b = &0 <=> c + a = b  `] THEN
 964 REWRITE_TAC[REAL_ARITH ` (a+ b + c ) / &2 - c = &0 <=> a + b = c `] THEN
 965 REWRITE_TAC[MESON[SET_RULE `{a,b} = {b,a} `]`v2 IN conv {v1, v3} \/ v3 IN
 966 conv {v1, v2}  <=> v2 IN conv {v3,v1} \/ v3 IN conv {v1, v2}`] THEN
 967 REWRITE_TAC[MID_COND] THEN MESON_TAC[DIST_SYM]);;
 968
 969 (* le 11. p 14 *)
 970 (* NGUYEN QUANG TRUONG *)
 971
 972
 973 (* These following lemma are Multivariate/convex.ml *)
 974
 975
 976 let affine_dependent = new_definition
 977  `affine_dependent (s:real^N -> bool) <=>
 978         ?x. x IN s /\ x IN (affine hull (s DELETE x))`;;
 979
 980  let AFFINE_HULL_FINITE = prove
 981   (`!s:real^N->bool.
 982        FINITE s
 983        ==> affine hull s = {y | ?u. sum s u = &1 /\ vsum s (\v. u v % v) = y}`,
 984    GEN_TAC THEN DISCH_TAC THEN
 985    REWRITE_TAC[EXTENSION; AFFINE_HULL_EXPLICIT; IN_ELIM_THM] THEN
 986    X_GEN_TAC `x:real^N` THEN EQ_TAC THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THENL
 987     [MAP_EVERY X_GEN_TAC [`t:real^N->bool`; `f:real^N->real`] THEN
 988      STRIP_TAC THEN
 989      EXISTS_TAC `\x:real^N. if x IN t then f x else &0` THEN
 990      REWRITE_TAC[] THEN ONCE_REWRITE_TAC[COND_RAND] THEN
 991      ONCE_REWRITE_TAC[COND_RATOR] THEN REWRITE_TAC[VECTOR_MUL_LZERO] THEN
 992      ASM_SIMP_TAC[GSYM VSUM_RESTRICT_SET; GSYM SUM_RESTRICT_SET] THEN
 993      ASM_SIMP_TAC[SET_RULE `t SUBSET s ==> {x | x IN s /\ x IN t} = t`];
 994      X_GEN_TAC `f:real^N->real` THEN
 995      ASM_CASES_TAC `s:real^N->bool = {}` THEN
 996      ASM_REWRITE_TAC[SUM_CLAUSES; REAL_OF_NUM_EQ; ARITH] THEN STRIP_TAC THEN
 997      MAP_EVERY EXISTS_TAC [`s:real^N->bool`; `f:real^N->real`] THEN
 998      ASM_REWRITE_TAC[GSYM EXTENSION; SUBSET_REFL]]);;
 999
1000  let IN_AFFINE_HULL_IMP_COLLINEAR = prove
1001   (`!a b c:real^N. a IN (affine hull {b,c}) ==> collinear {a,b,c}`,
1002    REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC
1003     [`a:real^N = b`; `a:real^N = c`; `b:real^N = c`] THEN
1004    TRY(ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_SING; COLLINEAR_2] THEN NO_TAC) THEN
1005    SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; FINITE_SING] THEN
1006    SIMP_TAC[SUM_CLAUSES; VSUM_CLAUSES; FINITE_RULES; REAL_ADD_RID] THEN
1007    ASM_REWRITE_TAC[IN_INSERT; IN_ELIM_THM; NOT_IN_EMPTY; VECTOR_ADD_RID] THEN
1008    DISCH_THEN(X_CHOOSE_THEN `f:real^N->real` STRIP_ASSUME_TAC) THEN
1009    ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {c,b,a}`] THEN
1010    ASM_REWRITE_TAC[COLLINEAR_3; COLLINEAR_LEMMA; VECTOR_SUB_EQ] THEN
1011    EXISTS_TAC `(f:real^N->real) c` THEN EXPAND_TAC "a" THEN
1012    FIRST_X_ASSUM(SUBST1_TAC o MATCH_MP (REAL_ARITH
1013     `b + c = &1 ==> b = &1 - c`)) THEN VECTOR_ARITH_TAC);;
1014
1015
1016  let AFFINE_DEPENDENT_3_IMP_COLLINEAR = prove
1017   (`!a b c:real^N. affine_dependent{a,b,c} ==> collinear{a,b,c}`,
1018    REPEAT GEN_TAC THEN
1019    MAP_EVERY ASM_CASES_TAC
1020     [`a:real^N = b`; `a:real^N = c`; `b:real^N = c`] THEN
1021    TRY(ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_SING; COLLINEAR_2] THEN NO_TAC) THEN
1022    REWRITE_TAC[affine_dependent; IN_INSERT; NOT_IN_EMPTY] THEN STRIP_TAC THEN
1023    FIRST_X_ASSUM SUBST_ALL_TAC THENL
1024     [ALL_TAC;
1025      ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {b,a,c}`];
1026      ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {c,b,a}`]] THEN
1027    MATCH_MP_TAC IN_AFFINE_HULL_IMP_COLLINEAR THEN
1028    FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (MESON[]
1029     `x IN s ==> s = t ==> x IN t`)) THEN
1030    AP_TERM_TAC THEN ASM SET_TAC[]);;
1031
1032 (* LEMMA 11 *)
1033 let FAFKVLR = prove
1034  (`!v1 v2 v3 v:real^N.
1035        ~collinear{v1,v2,v3} /\ v IN (affine hull {v1,v2,v3})
1036
1037        ==> ?t1 t2 t3. v = t1 % v1 + t2 % v2 + t3 % v3 /\
1038                       t1 + t2 + t3 = &1 /\
1039                       !ta tb tc. v = ta % v1 + tb % v2 + tc % v3 /\
1040
1041                                  ta + tb + tc = &1
1042                                  ==> ta = t1 /\ tb = t2 /\ tc = t3`,
1043  REPEAT GEN_TAC THEN
1044  MAP_EVERY ASM_CASES_TAC
1045   [`v1:real^N = v2`; `v2:real^N = v3`; `v1:real^N = v3`] THEN
1046  TRY(ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_SING; COLLINEAR_2] THEN NO_TAC) THEN
1047  SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; FINITE_SING; IN_ELIM_THM] THEN
1048  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1049  SIMP_TAC[SUM_CLAUSES; VSUM_CLAUSES; FINITE_INSERT; FINITE_SING;
1050           SUM_SING; VSUM_SING] THEN
1051  ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; LEFT_IMP_EXISTS_THM] THEN
1052  X_GEN_TAC `f:real^N->real` THEN STRIP_TAC THEN
1053  MAP_EVERY EXISTS_TAC
1054   [`(f:real^N->real) v1`; `(f:real^N->real) v2`; `(f:real^N->real) v3`] THEN
1055  ASM_REWRITE_TAC[] THEN REPEAT GEN_TAC THEN EXPAND_TAC "v" THEN
1056  DISCH_TAC THEN MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN
1057  UNDISCH_TAC `~collinear{v1:real^N,v2,v3}` THEN REWRITE_TAC[] THEN
1058  MATCH_MP_TAC AFFINE_DEPENDENT_3_IMP_COLLINEAR THEN
1059  SIMP_TAC[AFFINE_DEPENDENT_EXPLICIT_FINITE; FINITE_INSERT; FINITE_RULES;
1060           SUM_CLAUSES; VSUM_CLAUSES] THEN
1061  ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
1062  EXISTS_TAC `\x. if x = v1 then f v1 - ta
1063                  else if x = v2 then f v2 - tb
1064                  else (f:real^N->real) v3 - tc` THEN
1065  ASM_REWRITE_TAC[REAL_ADD_RID; VECTOR_ADD_RID] THEN REPEAT CONJ_TAC THENL
1066   [ASM_REAL_ARITH_TAC;
1067    ASM_REWRITE_TAC[EXISTS_OR_THM; RIGHT_OR_DISTRIB; UNWIND_THM2] THEN
1068    ASM_REWRITE_TAC[REAL_SUB_0] THEN ASM_MESON_TAC[];
1069    ASM_REWRITE_TAC[VECTOR_ARITH
1070     `(a - a') % x + (b - b') % y + (c - c') % z = vec 0 <=>
1071      a % x + b % y + c % z = a' % x + b' % y + c' % z`] THEN
1072    ASM_MESON_TAC[]]);;
1073
1074
1075
1076  let FAFKVLR_ALT = prove
1077   (`!v1 v2 v3 v:real^N.
1078          ~collinear{v1,v2,v3} /\ v IN (affine hull {v1,v2,v3})
1079          ==> ?!(t1,t2,t3). v = t1 % v1 + t2 % v2 + t3 % v3 /\
1080                            t1 + t2 + t3 = &1`,
1081    REWRITE_TAC(map(REWRITE_RULE[ETA_AX])
1082     [EXISTS_UNIQUE; FORALL_PAIR_THM; EXISTS_PAIR_THM]) THEN
1083    REWRITE_TAC[PAIR_EQ; GSYM CONJ_ASSOC; FAFKVLR]);;
1084
1085
1086 let equivalent_lemma = prove(` (?t1 t2 t3.
1087          !v1 v2 v3 (v:real^N).
1088              v IN affine hull {v1, v2, v3} /\ ~collinear {v1, v2, v3}
1089              ==> v =
1090                  t1 v1 v2 v3 v % v1 + t2 v1 v2 v3 v % v2 + t3 v1 v2 v3 v % v3 /\
1091                  t1 v1 v2 v3 v + t2 v1 v2 v3 v + t3 v1 v2 v3 v = &1 /\
1092                  (!ta tb tc.
1093                       v = ta % v1 + tb % v2 + tc % v3 /\ ta + tb + tc = &1
1094                       ==> ta = t1 v1 v2 v3 v /\
1095                           tb = t2 v1 v2 v3 v /\
1096                           tc = t3 v1 v2 v3 v))  <=>
1097
1098           ( !v1 v2 v3 (v:real^N).
1099              v IN affine hull {v1, v2, v3} /\ ~collinear {v1, v2, v3}
1100           ==> (?t1 t2 t3.
1101                    v = t1 % v1 + t2 % v2 + t3 % v3 /\
1102                    t1 + t2 + t3 = &1 /\
1103                    (!ta tb tc.
1104                         v = ta % v1 + tb % v2 + tc % v3 /\ ta + tb + tc = &1
1105                         ==> ta = t1 /\ tb = t2 /\ tc = t3))) `,
1106 REWRITE_TAC[GSYM SKOLEM_THM; LEFT_FORALL_IMP_THM; RIGHT_EXISTS_IMP_THM]);;
1107
1108
1109  let LAMBDA_TRIPLED_THM = prove
1110   (`!t. (\(x,y,z). t x y z) = (\p. t (FST p) (FST(SND p)) (SND(SND p)))`,
1111    REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM]);;
1112
1113  let FORALL_TRIPLED_THM = prove
1114   (`!P. (!(x,y,z). P x y z) <=> (!x y z. P x y z)`,
1115    REWRITE_TAC[LAMBDA_TRIPLED_THM] THEN REWRITE_TAC[FORALL_PAIR_THM]);;
1116
1117  let EXISTS_TRIPLED_THM = prove
1118   (`!P. (?(x,y,z). P x y z) <=> (?x y z. P x y z)`,
1119    REWRITE_TAC[LAMBDA_TRIPLED_THM] THEN REWRITE_TAC[EXISTS_PAIR_THM]);;
1120
1121  let EXISTS_UNIQUE_TRIPLED_THM = prove
1122   (`!P. (?!(x,y,z). P x y z) <=>
1123         (?x y z. P x y z /\
1124                  (!x' y' z'. P x' y' z' ==> x' = x /\ y' = y /\ z' = z))`,
1125    REWRITE_TAC[REWRITE_RULE[ETA_AX] EXISTS_UNIQUE] THEN
1126    REWRITE_TAC[FORALL_TRIPLED_THM; EXISTS_TRIPLED_THM] THEN
1127    REWRITE_TAC[EXISTS_PAIR_THM; FORALL_PAIR_THM; PAIR_EQ]);;
1128
1129
1130  let theoremmm = prove
1131  (`( !v1 v2 v3 v:real^N.
1132       v IN affine hull {v1, v2, v3} /\ ~collinear {v1, v2, v3}
1133       ==> (?t1 t2 t3.
1134                v = t1 % v1 + t2 % v2 + t3 % v3 /\
1135                t1 + t2 + t3 = &1 /\
1136                (!ta tb tc.
1137                     v = ta % v1 + tb % v2 + tc % v3 /\
1138                     ta + tb + tc = &1
1139                     ==> ta = t1 /\ tb = t2 /\ tc = t3)) )
1140    <=>
1141    ( !v1 v2 v3 v:real^N.
1142             ~collinear {v1, v2, v3} /\ v IN affine hull {v1, v2, v3}
1143             ==> (?!(t1,t2,t3). v = t1 % v1 + t2 % v2 + t3 % v3 /\
1144                                t1 + t2 + t3 = &1))`,
1145    REWRITE_TAC[EXISTS_UNIQUE_TRIPLED_THM] THEN REWRITE_TAC[CONJ_ACI]);;
1146
1147
1148
1149
1150 let FAFKVLR = prove(` (?t1 t2 t3.
1151          !v1 v2 v3 (v:real^N).
1152              v IN affine hull {v1, v2, v3} /\ ~collinear {v1, v2, v3}
1153              ==> v =
1154                  t1 v1 v2 v3 v % v1 + t2 v1 v2 v3 v % v2 + t3 v1 v2 v3 v % v3 /\
1155                  t1 v1 v2 v3 v + t2 v1 v2 v3 v + t3 v1 v2 v3 v = &1 /\
1156                  (!ta tb tc.
1157                       v = ta % v1 + tb % v2 + tc % v3 /\ ta + tb + tc = &1
1158                       ==> ta = t1 v1 v2 v3 v /\
1159                           tb = t2 v1 v2 v3 v /\
1160                           tc = t3 v1 v2 v3 v))  `,
1161 SIMP_TAC[equivalent_lemma; FAFKVLR]);;
1162 let LEMMA11 = FAFKVLR;;
1163 let lemma11 = REWRITE_RULE[equivalent_lemma] FAFKVLR;;
1164 let COEFS = new_specification ["coef1"; "coef2"; "coef3"] FAFKVLR;;
1165
1166 let lem11 = REWRITE_RULE[simp_def2; IN_ELIM_THM] lemma11;;
1167
1168 let REAL_PER3 = REAL_ARITH `!a b c. a + b + c = b + a + c /\ a + b + c = c + b + a `;;
1169
1170
1171 MESON[VEC_PER2_3]` (!ta tb tc.
1172       v = ta % v1 + tb % v2 + tc % v3 ==> ta = t1 /\ tb = t2 /\ tc = t3) /\bbb/\
1173  v = ta''' % v1 + tb''' % v2 + t''' % v3 /\
1174  v = ta'' % v3 + tb'' % v1 + t'' % v2 /\
1175  v = ta' % v2 + tb' % v3 + t' % v1 /\
1176 aa  ==> t' = t1 /\ t'' = t2 /\ t''' = t3 `;;
1177
1178 let NOT_COLLINEAR_IMP_2_UNEQUAL = MESON[INSERT_INSERT; COLLINEAR_2; INSERT_AC]
1179 `~collinear {v0, va, vb} ==> ~(v0 = va) /\ ~(v0 = vb) `;;
1180
1181 let COLLINEAR_DISJOINT3  = prove(`!v1:real^A v2 v3. ~collinear {v1,v2,v3} ==>
1182   DISJOINT {v2,v3} {v1}`,
1183   REWRITE_TAC[DISJOINT_INSERT;DISJOINT_EMPTY;IN_INSERT;NOT_IN_EMPTY] THEN
1184   MESON_TAC[NOT_COLLINEAR_IMP_2_UNEQUAL]
1185                               );;
1186
1187 let COLLINEAR_DISJOINT_PERM3  = prove(`!v1:real^A v2 v3. (~collinear {v1,v2,v3} ==>
1188   DISJOINT {v1,v2} {v3}) /\ (~collinear {v1,v2,v3} ==> DISJOINT {v2,v3} {v1}) /\
1189    (~collinear {v1,v2,v3} ==> DISJOINT {v3,v1} {v2})`,
1190   REPEAT GEN_TAC THEN
1191   SUBGOAL_THEN `{v3:real^A,v1,v2} = {v1,v2,v3} /\ {v2,v3,v1}={v1,v2,v3}` MP_TAC THENL
1192   [SET_TAC[] ; ASM_MESON_TAC[COLLINEAR_DISJOINT3]]);;
1193
1194 let simp_def_ge = prove(` !a:real^A b v0.
1195           DISJOINT {a, b} {v0}
1196           ==>
1197               aff_ge {a, b} {v0} =
1198               {x | ?ta tb t.
1199                        ta + tb + t = &1 /\
1200                        &0 <= t /\
1201                        x = ta % a + tb % b + t % v0} `,
1202    MESON_TAC[simp_def2]);;
1203
1204
1205 let IN_CONV3_EQ = prove(`! (v:real^3) v1 v2 v3. ~collinear {v1,v2,v3} ==> (v IN conv {v1, v2, v3} <=>
1206   v IN aff_ge {v1,v2} {v3} /\
1207   v IN aff_ge {v2,v3} {v1} /\ v IN aff_ge {v3,v1} {v2} )`,
1208 SIMP_TAC[CONV_SET3; COLLINEAR_DISJOINT_PERM3;simp_def_ge; IN_ELIM_THM] THEN
1209 REPEAT GEN_TAC THEN DISCH_TAC THEN  EQ_TAC THENL [
1210 MESON_TAC[REAL_ARITH` a + b + c = b + a + c /\ a + b + c = c + b + a `;
1211   VECTOR_ARITH `(a:real^N) + b + c = b + a + c /\ a + b + c = c + b + a `; lem11];
1212 NHANH (MESON[]` (? a b c. P a b c /\ Q c /\ R a b c) /\ aa /\ bb ==>
1213    (? a b c. P a b c /\ R a b c) `) THEN
1214 FIRST_X_ASSUM MP_TAC THEN
1215 REWRITE_TAC[IMP_IMP] THEN
1216 REWRITE_TAC[MESON[]` ~a/\ b <=> b /\ ~ a `] THEN
1217 PHA THEN
1218 NHANH (SPEC_ALL lem11) THEN
1219 STRIP_TR THEN REWRITE_TAC[MESON[]` (v = w:real^N) /\ a <=> a /\ v = w `] THEN PHA] THEN
1220 NHANH (MESON[VEC_PER2_3; REAL_PER3]` ta + tb + t = &1 /\
1221  &0 <= t /\
1222  ta' + tb' + t' = &1 /\
1223  &0 <= t' /\
1224  ta'' + tb'' + t'' = &1 /\
1225  &0 <= t'' /\
1226 a1/\
1227 a2/\
1228  t1 + t2 + t3 = &1 /\
1229  (!ta tb tc.
1230       ta + tb + tc = &1 /\ v = ta % v1 + tb % v2 + tc % v3
1231       ==> ta = t1 /\ tb = t2 /\ tc = t3) /\
1232  v = t1 % v1 + t2 % v2 + t3 % v3 /\
1233 a3/\
1234  v = ta'' % v3 + tb'' % v1 + t'' % v2 /\
1235  v = ta' % v2 + tb' % v3 + t' % v1 /\
1236  v = ta % v1 + tb % v2 + t % v3 ==> t1 = t' /\ t2 = t'' /\ t3 = t`) THEN
1237 MESON_TAC[]);;
1238
1239
1240 let IN_CONV03_EQ = prove(
1241 `! (v:real^3) v1 v2 v3. ~collinear {v1,v2,v3} ==>
1242 (v IN conv0 {v1, v2, v3} <=>   v IN aff_gt {v1,v2} {v3} /\
1243   v IN aff_gt {v2,v3} {v1} /\ v IN aff_gt {v3,v1} {v2} )`,
1244 SIMP_TAC[CONV_SET3; COLLINEAR_DISJOINT_PERM3;simp_def2; IN_ELIM_THM] THEN
1245 REPEAT GEN_TAC THEN DISCH_TAC THEN  EQ_TAC THENL [
1246 MESON_TAC[REAL_ARITH` a + b + c = b + a + c /\ a + b + c = c + b + a `;
1247   VECTOR_ARITH `(a:real^N) + b + c = b + a + c /\ a + b + c = c + b + a `; lem11];
1248 NHANH (MESON[]` (? a b c. P a b c /\ Q c /\ R a b c) /\ aa /\ bb ==>
1249    (? a b c. P a b c /\ R a b c) `) THEN
1250 FIRST_X_ASSUM MP_TAC THEN
1251 REWRITE_TAC[IMP_IMP] THEN
1252 REWRITE_TAC[MESON[]` ~a/\ b <=> b /\ ~ a `] THEN
1253 PHA THEN
1254 NHANH (SPEC_ALL lem11) THEN
1255 STRIP_TR THEN REWRITE_TAC[MESON[]` (v = w:real^N) /\ a <=> a /\ v = w `]]
1256  THEN PHA THEN NHANH (MESON[VEC_PER2_3; REAL_PER3]`
1257   ta + tb + t = &1 /\
1258  &0 < t /\
1259  ta' + tb' + t' = &1 /\
1260  &0 < t' /\
1261  ta'' + tb'' + t'' = &1 /\
1262  &0 < t'' /\ a33 /\ a22 /\
1263  t1 + t2 + t3 = &1 /\
1264  (!ta tb tc.
1265       ta + tb + tc = &1 /\ v = ta % v1 + tb % v2 + tc % v3
1266       ==> ta = t1 /\ tb = t2 /\ tc = t3) /\
1267  v = t1 % v1 + t2 % v2 + t3 % v3 /\ a11 /\
1268  v = ta'' % v3 + tb'' % v1 + t'' % v2 /\
1269  v = ta' % v2 + tb' % v3 + t' % v1 /\
1270  v = ta % v1 + tb % v2 + t % v3 ==>
1271   t1 = t' /\ t2 = t'' /\ t3 = t `) THEN MESON_TAC[]);;
1272
1273
1274 let AFFINE_SET_GEN_BY_TWO_POINTS =
1275 prove(`! a b. affine {x | ?ta tb. ta + tb = &1 /\ x = ta % a + tb % b}`,
1276 REWRITE_TAC[affine; IN_ELIM_THM] THEN
1277 REPEAT GEN_TAC THEN
1278 STRIP_TAC THEN
1279 EXISTS_TAC ` u * ta + v * ta' ` THEN
1280 EXISTS_TAC ` u * tb + v * tb' ` THEN
1281 REWRITE_TAC[REAL_ARITH ` (u * ta + v * ta') + u * tb + v * tb' =
1282   u * (ta + tb) + v * (ta' + tb' ) `] THEN
1283 ASM_SIMP_TAC[REAL_ARITH ` a * &1 = a `] THEN
1284 CONV_TAC VECTOR_ARITH);;
1285
1286 let SET2_SU_EX = SET_RULE` {(a:A),b} SUBSET s <=> a IN s /\ b IN s `;;
1287
1288 let GENERATING_POINT_IN_SET_AFF = prove(` ! a b. {a,b} SUBSET {x | ?ta tb.
1289 ta + tb = &1 /\ x = ta % a + tb % b}`,REWRITE_TAC[SET2_SU_EX; IN_ELIM_THM]
1290 THEN REPEAT GEN_TAC THEN
1291 MESON_TAC[REAL_ARITH` &0 + &1 = &1 /\ a + b = b + a`; VECTOR_ARITH `
1292   a = &0 % b + &1 % a /\ a = &1 % a + &0 % b `]);;
1293
1294
1295 let AFF_2POINTS_INTERPRET = prove(`!a b. aff {a, b} = {x | ?ta tb. ta + tb = &1 /\ x = ta % a + tb % b}`,
1296 REWRITE_TAC[aff; hull] THEN
1297 REPEAT GEN_TAC THEN
1298 REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN
1299 SIMP_TAC[INTERS_SUBSET; AFFINE_SET_GEN_BY_TWO_POINTS;
1300   GENERATING_POINT_IN_SET_AFF] THEN
1301 REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN
1302 REWRITE_TAC[SUBSET; IN_ELIM_THM; IN_INTERS; affine] THEN
1303 SET_TAC[]);;
1304
1305
1306 (* corrected with DISJOINT by thales *)
1307
1308 let IN_AFF_GE_INTERPRET_TO_AFF_GT_AND_AFF = prove(` ! v v1 v2 v3 .
1309    DISJOINT{v1,v2} {v3} ==>
1310 (v IN aff_ge {v1,v2} {v3} <=> v IN aff_gt {v1,v2} {v3} \/
1311   v IN aff {v1,v2}) `,
1312 REPEAT STRIP_TAC THEN
1313 ASM_SIMP_TAC[simp_def2; AFF_2POINTS_INTERPRET; IN_ELIM_THM ] THEN
1314 REWRITE_TAC [REAL_ARITH ` &0 <= a <=> &0 < a \/ a = &0 `] THEN
1315 MESON_TAC[REAL_ARITH ` (&0 <= a <=> &0 < a \/ a = &0 )/\( a + &0 = a ) `;
1316   VECTOR_ARITH ` a + &0 % c = a `]);;
1317
1318 let DOWN_TAC = REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IMP_IMP] THEN PHA;;
1319 let IMP_IMP_TAC = REWRITE_TAC[IMP_IMP] THEN PHA;;
1320
1321
1322 let AFFINE_AFF_HULL = prove(` ! s. affine ( aff s ) `,
1323 REWRITE_TAC[aff; AFFINE_AFFINE_HULL]);;
1324
1325
1326 let AFFINE_CONTAIN_LINE = prove(`! a b s. affine s /\ {a,b} SUBSET s ==>
1327  aff {a,b} SUBSET s `,
1328 REWRITE_TAC[affine ; AFF_2POINTS_INTERPRET; IN_ELIM_THM] THEN SET_TAC[]);;
1329
1330 let VECTOR_SUB_DISTRIBUTE = VECTOR_ARITH ` ! a x y. a % x - a % y = a % ( x - y ) `;;
1331
1332
1333 let CHANGE_SIDE = prove(` ~( a = &0 ) ==> ( x = a % y <=> ( &1 / a) % x = y )`,
1334 MESON_TAC[ VECTOR_ARITH `  ( a * b ) % x = a % b % x `; VECTOR_MUL_LID;
1335   REAL_FIELD `~( a = &0 ) ==>  a * &1 / a = &1 `; VECTOR_MUL_LCANCEL]);;
1336
1337
1338 let PRE_INVERSE_SUB = prove(` ! a b v w. {a, b} SUBSET aff {v, w} /\ ~(a = b)
1339  ==> {v, w} SUBSET aff {a, b}`,
1340 REWRITE_TAC[AFF_2POINTS_INTERPRET; SET2_SU_EX; IN_ELIM_THM] THEN
1341 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN
1342 REWRITE_TAC[IMP_IMP] THEN PHA THEN
1343 NHANH (MESON[]` (a:real^N) = b /\ gg /\ a' = b' /\ ll ==> a - a' = b - b' `) THEN
1344 REWRITE_TAC[VECTOR_ARITH` (ta % v + tb % w) - (ta' % v + tb' % w) =
1345   ( ta - ta') % v + ( tb - tb' ) % w `] THEN
1346 PHA THEN REWRITE_TAC[MESON[]` a = &1 /\ b <=> b /\ a = &1 `] THEN PHA THEN
1347 NHANH (REAL_ARITH ` ta + tb = &1 /\ ta' + tb' = &1 ==> ta' - ta = tb - tb' `) THEN
1348 REWRITE_TAC[VECTOR_ARITH ` a + ( x - y ) % b = a - ( y - x) % b `] THEN
1349 REWRITE_TAC[MESON[]` a - b = ta % v - tb % w /\aa/\
1350    ta = tb <=> a - b = ta % v - ta % w /\ aa /\ ta = tb `] THEN
1351 ASM_CASES_TAC `(ta:real) = ta' ` THENL [ASM_SIMP_TAC[REAL_SUB_REFL;
1352 VECTOR_MUL_LZERO; VECTOR_SUB_RZERO; VECTOR_SUB_EQ] THEN MESON_TAC[]; ALL_TAC] THEN
1353 REWRITE_TAC[VECTOR_SUB_DISTRIBUTE] THEN FIRST_X_ASSUM MP_TAC THEN
1354 ONCE_REWRITE_TAC[REAL_ARITH` ~( a = b) <=> ~( a - b = &0 )`] THEN IMP_IMP_TAC THEN
1355 REWRITE_TAC[MESON[]` ~( a = b:real) /\ l <=> l /\ ~(a = b) `; MESON[]`
1356 a = d % b /\ l  <=> l /\  a = d % b `] THEN PHA THEN
1357 REWRITE_TAC[MESON[CHANGE_SIDE]` x = a % y /\ ~( a = &0 ) <=>  &1 / a % x = y /\
1358  ~( a = &0 )`] THEN NHANH (MESON[VECTOR_MUL_LCANCEL]` ta - ta' = tb' - tb /\
1359  a = b  /\ l ==> tb % a = tb % b /\ ta % a = ta % b `) THEN
1360 ONCE_REWRITE_TAC[MESON[]` a = (b:real^n) /\ l <=> l /\ a = b `] THEN PHA
1361 THEN REWRITE_TAC[GSYM VECTOR_SUB_DISTRIBUTE] THEN
1362 ONCE_REWRITE_TAC[VECTOR_ARITH` a = (b:real^N) /\ a1 = (b1:real^N) /\ a2 =
1363   (b2:real^N) <=> a2 = b2 /\ a + a2 = b + b2 /\ a2 - a1 = b2 - b1 `] THEN
1364 REWRITE_TAC[VECTOR_ARITH` (ta % v + tb % w) - (ta % v - ta % w) = ( ta + tb ) % w `;
1365   VECTOR_ARITH` tb % v - tb % w + ta % v + tb % w = ( ta + tb ) % v `] THEN
1366 REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_ARITH` a - ( x % a - y % b ) =
1367 (&1 - x ) % a + y % b `] THEN REWRITE_TAC[VECTOR_ARITH` a % x - b % y + x =
1368 (a + &1 ) % x + --b % y `] THEN
1369 REWRITE_TAC[MESON[]` a = &1 /\ b = &1 /\ l <=> a = &1 /\ l /\b = &1 `] THEN
1370 DAO THEN MATCH_MP_TAC (MESON[]`( a1 /\a2/\a3/\a5 ==> l) ==>
1371 (a1/\a2/\a3/\a4/\a5/\a6   ==> l ) `) THEN PURE_ONCE_REWRITE_TAC[ MESON[]`
1372  a + b = &1 /\ P ( a + b ) <=> a + b = &1 /\  P (&1) `] THEN
1373 REWRITE_TAC[VECTOR_MUL_LID] THEN MESON_TAC[REAL_FIELD ` ~(ta - ta' = &0)
1374      ==> (tb * &1 / (ta - ta') + &1) + --(tb * &1 / (ta - ta')) = &1 /\
1375   &1 - ta * &1 / (ta - ta') + ta * &1 / (ta - ta') = &1 `]);;
1376
1377
1378
1379 let LEMMA5 = prove(
1380 `!(a:real^N) b x. line x /\ {a, b} SUBSET x /\ ~(a = b) ==> x = aff {a, b}`,
1381 REWRITE_TAC[line; GSYM aff] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
1382 REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN ASM_SIMP_TAC[AFFINE_AFF_HULL;
1383 AFFINE_CONTAIN_LINE] THEN STRIP_TR THEN
1384 ABBREV_TAC ` (ki : bool ) = aff {(v:real^N), (w:real^N)}
1385   SUBSET aff {(a:real^N), (b:real^N)}` THEN
1386 REWRITE_TAC[MESON[]` a/\b/\c ==> d <=> b ==> a/\c ==> d `] THEN SIMP_TAC[]
1387 THEN DISCH_TAC THEN IMP_IMP_TAC THEN
1388 NHANH (MESON[PRE_INVERSE_SUB]`{a, b} SUBSET aff {v, w} /\ aa /\ ~(a = b)
1389   ==> {v, w} SUBSET aff {a, b} `) THEN
1390 NHANH (MESON[AFFINE_AFF_HULL]` aa /\ v SUBSET aff {a, b} ==> affine (aff {a,b})`)
1391 THEN DOWN_TAC THEN MESON_TAC[AFFINE_CONTAIN_LINE]);;
1392
1393 let RCEABUJ = LEMMA5;;
1394
1395
1396 let COL_EQ_UPS_0 = GEN_ALL (MESON[FHFMKIY]` collinear {(v1:real^3), v2, v3} <=>
1397  ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) = &0`);;
1398
1399
1400
1401 let EQ_POW2_COND = prove(`!a b. &0 <= a /\ &0 <= b ==> (a = b <=> a pow 2 = b pow 2)`,
1402 REWRITE_TAC[REAL_ARITH` a = b <=> a <= b /\ b <= a `] THEN SIMP_TAC[POW2_COND]);;
1403
1404
1405 let D3_POS_LE = MESON[dist3; DIST_POS_LE]` ! x y. &0 <= dist3 x y `;;
1406
1407
1408 let delta_x12 = new_definition ` delta_x12 x12 x13 x14 x23 x24 x34 =
1409   -- x13 * x23 + -- x14 * x24 + x34 * ( -- x12 + x13 + x14 + x23 + x24 + -- x34 )
1410   + -- x12 * x34 + x13 * x24 + x14 * x23 `;;
1411
1412 let delta_x13 = new_definition` delta_x13 x12 x13 x14 x23 x24 x34 =
1413   -- x12 * x23 + -- x14 * x34 + x12 * x34 + x24 * ( x12 + -- x13 + x14 + x23 +
1414   -- x24 + x34 ) + -- x13 * x24 + x14 * x23 `;;
1415
1416 let delta_x14 = new_definition`delta_x14 x12 x13 x14 x23 x24 x34 =
1417          --x12 * x24 +
1418          --x13 * x34 +
1419          x12 * x34 +
1420          x13 * x24 +
1421          x23 * (x12 + x13 + --x14 + --x23 + x24 + x34) +
1422          --x14 * x23`;;
1423
1424
1425
1426 let DIST_POW2_DOT =
1427 prove(` ! a (b:real^N) . dist (a,b) pow 2 = ( a - b ) dot ( a- b) `,
1428 SIMP_TAC[dist; vector_norm; DOT_POS_LE; SQRT_WORKS]);;
1429
1430
1431 (* REMOVED. thales
1432 (* the following lemma is in Multivariate/convex.ml *)
1433 let AFFINE_HULL_3 = new_axiom_removed` affine hull {a,b,c} =
1434     { u % a + v % b + w % c | u + v + w = &1}`;;
1435 *)
1436
1437 let LET_TR = CONV_TAC (TOP_DEPTH_CONV let_CONV);;
1438
1439
1440 (* BEGINING *)
1441 (* lemma 16 SDIHJZK *)
1442
1443 let TO_UYCH = prove(` &0 < ups_x a12 a13 a23 ==>
1444   delta_x12 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 +
1445      delta_x13 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 +
1446      delta_x14 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 =
1447      &1 `,
1448 REWRITE_TAC[ups_x; delta_x12; delta_x13; delta_x14] THEN CONV_TAC REAL_FIELD);;
1449
1450
1451
1452
1453 let NOT_UPS_X_ZERO_IMP_SMT = prove(`~(ups_x a12 a13 a23 = &0)
1454  ==> (delta_x13 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a12 +
1455      delta_x13 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
1456      delta_x14 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
1457      (a12 + a13 - a23) +
1458      (delta_x14 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a13
1459      =
1460      a01 - delta a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 /\
1461
1462 (delta_x14 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a23 +
1463      delta_x14 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
1464      delta_x12 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
1465      (a23 + a12 - a13) +
1466      (delta_x12 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a12
1467       =
1468      a02 - delta a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 /\
1469
1470 (delta_x12 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a13 +
1471      delta_x12 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
1472      delta_x13 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23 *
1473      (a13 + a23 - a12) +
1474      (delta_x13 a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23) pow 2 * a23 =
1475      a03 - delta a01 a02 a03 a12 a13 a23 / ups_x a12 a13 a23`,
1476 ONCE_REWRITE_TAC[REAL_FIELD` ~( a = &0 ) ==> ( x = y ) /\ ( xx = yy ) /\ ( xxx = yyy)
1477   <=> ~( a = &0 ) ==> ( x * a pow 2 = y * a pow 2 ) /\
1478   ( xx * a pow 2 = yy * a pow 2 ) /\
1479   ( xxx * a pow 2 = yyy * a pow 2 ) `] THEN
1480 SIMP_TAC[REAL_FIELD` ~( a = &0 ) ==> ( b - c / a ) * a pow 2 = b * a pow 2 - c * a `
1481   ; REAL_ADD_RDISTRIB] THEN
1482 SIMP_TAC[REAL_ARITH` ( a * b ) * c = a * b * c `;
1483   REAL_FIELD` ~ ( a = &0 ) ==> ( b / a ) pow 2 * c * a pow 2 =
1484   b pow 2 * c `; REAL_FIELD ` ~ ( a = &0 ) ==> b / a * c / a * d *
1485   a pow 2 = b * c * d `] THEN DISCH_TAC THEN
1486 REWRITE_TAC[delta_x12; delta_x13; delta_x14; delta; ups_x] THEN REAL_ARITH_TAC);;
1487
1488
1489 let TROI_OI_DAT_HOI = MESON[ lemma8; dist; DIST_SYM]` &0 <=
1490            ups_x ( dist((v1:real^3),v2) pow 2) (dist(v2,v3) pow 2)
1491            (dist(v1,v3) pow 2)`;;
1492
1493
1494
1495 let ZERO_LE_UPS_X = MESON[TROI_OI_DAT_HOI; dist3; DIST_SYM]`
1496   &0 <= ups_x (dist3 x y pow 2) (dist3 x z pow 2) (dist3 y z pow 2) `;;
1497
1498
1499 let UPS_X_EQ_ZERO_COND = prove(` ! v1 v2 (v3: real^3). (collinear {v1, v2, v3} <=>
1500             ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2)
1501             (dist (v2,v3) pow 2) =
1502             &0) `,
1503 MP_TAC FHFMKIY THEN MESON_TAC[]);;
1504
1505
1506
1507 let NORM_POW2_SUM2 = prove(` norm ( a % x + b % y ) pow 2 =
1508   a pow 2 * norm x pow 2 + &2 * ( a * b ) * ( x dot y ) +
1509   b pow 2 * norm y pow 2 `, REWRITE_TAC[vector_norm] THEN
1510 SIMP_TAC[DOT_POS_LE; SQRT_WORKS] THEN CONV_TAC VECTOR_ARITH);;
1511
1512
1513
1514 let X_DOT_X_EQ = prove( ` x dot x = norm x pow 2 `,
1515 SIMP_TAC[vector_norm; DOT_POS_LE; SQRT_WORKS]);;
1516
1517
1518
1519 let SUB_DIST_POW2_INTERPRETE = prove(`! x y (v:real^N) c.
1520 dist(x,v) pow 2 - dist(y,v) pow 2 = c <=>
1521 ( &2 % v  - ( x + y )) dot ( y - x ) = c `,
1522 SIMP_TAC[DIST_POW2_DOT; DOT_SUB_ADD; VECTOR_ARITH`
1523  (x - v - (y - v)) dot (x - v + y - v) =  (&2 % v - (x + y)) dot (y - x) `]);;
1524
1525 let D3_SYM = MESON[trg_dist3_sym]` ! x y. dist3 x y = dist3 y x `;;
1526
1527 let REAL_DIV_LZERO = prove(
1528   `!x. &0 / x = &0`,
1529   REPEAT GEN_TAC THEN REWRITE_TAC[real_div; REAL_MUL_LZERO]);;
1530
1531 let SDIHJZK = prove(`! (v1:real^3) v2 v3 (a01: real) a02 a03.
1532          ~collinear {v1, v2, v3} /\
1533          (let x12 = dist3 v1 v2 pow 2 in
1534           let x13 = dist3 v1 v3 pow 2 in
1535           let x23 = dist3 v2 v3 pow 2 in delta a01 a02 a03 x12 x13 x23 = &0)
1536          ==> (?!v0. a01 = dist3 v0 v1 pow 2 /\
1537                     a02 = dist3 v0 v2 pow 2 /\
1538                     a03 = dist3 v0 v3 pow 2 /\
1539                     (let x12 = dist3 v1 v2 pow 2 in
1540                      let x13 = dist3 v1 v3 pow 2 in
1541                      let x23 = dist3 v2 v3 pow 2 in
1542                      let vv = ups_x x12 x13 x23 in
1543                      let t1 = delta_x12 a01 a02 a03 x12 x13 x23 / vv in
1544                      let t2 = delta_x13 a01 a02 a03 x12 x13 x23 / vv in
1545                      let t3 = delta_x14 a01 a02 a03 x12 x13 x23 / vv in
1546                      v0 = t1 % v1 + t2 % v2 + t3 % v3 /\ t1 + t2 + t3 = &1 ))`,
1547 REPEAT GEN_TAC THEN
1548 LET_TR THEN
1549 STRIP_TAC THEN
1550 REWRITE_TAC[EXISTS_UNIQUE] THEN
1551 EXISTS_TAC ` delta_x12 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1552        (dist3 v2 v3 pow 2) /
1553        ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1554        v1 +
1555        delta_x13 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1556        (dist3 v2 v3 pow 2) /
1557        ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1558        v2 +
1559        delta_x14 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1560        (dist3 v2 v3 pow 2) /
1561        ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1562        v3 ` THEN
1563 UNDISCH_TAC `~collinear {(v1:real^3), v2, v3}` THEN
1564 MP_TAC (GEN_ALL ZERO_LE_UPS_X) THEN
1565 REWRITE_TAC[UPS_X_EQ_ZERO_COND] THEN
1566 REWRITE_TAC[MESON[]` a ==> b ==> c <=> a /\ b ==> c `; dist3] THEN
1567 NHANH (MESON[REAL_ARITH ` &0 <= a <=> &0 < a \/ a = &0 `]`
1568    (!(x:real^3) y z.
1569         &0 <= ups_x (dist (x,y) pow 2) (dist (x,z) pow 2) (dist (y,z) pow 2)) /\
1570    ~(ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) = &0)
1571     ==> &0 < ups_x (dist ((v1:real^3),v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) `) THEN
1572 REWRITE_TAC[ GSYM dist3] THEN
1573 STRIP_TAC THEN
1574 CONJ_TAC THENL [
1575
1576 UNDISCH_TAC ` &0 < ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2)` THEN
1577 ABBREV_TAC ` a12 = dist3 v1 v2 pow 2 ` THEN ABBREV_TAC ` a13 = dist3 v1 v3 pow 2 ` THEN
1578 ABBREV_TAC ` a23 = dist3 v2 v3 pow 2 ` THEN SIMP_TAC[TO_UYCH] THEN
1579 REWRITE_TAC[MESON[dist3; dist] ` aa = dist3 a b pow 2 <=> aa = norm ( a- b ) pow 2 `] THEN
1580 ONCE_REWRITE_TAC[VECTOR_ARITH ` a - b = a - &1 % b `] THEN
1581 NHANH (GSYM TO_UYCH) THEN SIMP_TAC[] THEN
1582 SIMP_TAC[VECTOR_ARITH ` (a % v1 + b % v2 + c % v3) - (a + b + c) % v2 =
1583      (b % v2 + c % v3 + a % v1) - (b + c + a) % v2 /\
1584   (a % v1 + b % v2 + c % v3) - (a + b + c) % v3 =
1585   (c % v3 + a % v1 + b % v2 ) - ( c + a + b ) % v3 `] THEN
1586 REWRITE_TAC[VECTOR_ARITH` ( a % v1 + b % v2 + c % v3)  -
1587   ( a + b + c ) % v1 = b % ( v2 - v1 ) + c % ( v3 - v1 ) `] THEN
1588 REWRITE_TAC[NORM_POW2_SUM2 ; REAL_ARITH ` &2 * ( a * b ) * c = a * b * &2 * c `] THEN
1589 REWRITE_TAC[VECTOR_ARITH ` &2 * ( x dot y ) = x dot x + y dot y - ( x - y ) dot ( x - y ) `] THEN
1590 REWRITE_TAC[VECTOR_ARITH` v1 - v3 - (v2 - v3) = (v1:real^3) - v2 `] THEN
1591 REWRITE_TAC[X_DOT_X_EQ; GSYM dist; GSYM dist3] THEN
1592 SIMP_TAC[D3_SYM] THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN
1593 UNDISCH_TAC ` ~(ups_x a12 a13 a23 = &0)` THEN NHANH NOT_UPS_X_ZERO_IMP_SMT  THEN
1594 ASM_SIMP_TAC[REAL_DIV_LZERO; REAL_SUB_RZERO];
1595 MESON_TAC[]]);;
1596
1597
1598
1599 let HALF_OF_LE16 = prove(` ! (v1:real^3) v2 v3 (a01: real) a02 a03.
1600          ~collinear {v1, v2, v3} /\
1601          (let x12 = dist3 v1 v2 pow 2 in
1602           let x13 = dist3 v1 v3 pow 2 in
1603           let x23 = dist3 v2 v3 pow 2 in delta a01 a02 a03 x12 x13 x23 = &0)
1604 ==> ?v0. (v0 IN aff {v1, v2, v3} /\
1605        a01 = dist3 v0 v1 pow 2 /\
1606        a02 = dist3 v0 v2 pow 2 /\
1607        a03 = dist3 v0 v3 pow 2 /\
1608        (let x12 = dist3 v1 v2 pow 2 in
1609         let x13 = dist3 v1 v3 pow 2 in
1610         let x23 = dist3 v2 v3 pow 2 in
1611         let vv = ups_x x12 x13 x23 in
1612         let t1 = delta_x12 a01 a02 a03 x12 x13 x23 / vv in
1613         let t2 = delta_x13 a01 a02 a03 x12 x13 x23 / vv in
1614         let t3 = delta_x14 a01 a02 a03 x12 x13 x23 / vv in
1615         v0 = t1 % v1 + t2 % v2 + t3 % v3)) `,
1616 REPEAT GEN_TAC THEN LET_TR THEN STRIP_TAC THEN REWRITE_TAC[EXISTS_UNIQUE] THEN
1617 EXISTS_TAC ` delta_x12 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1618        (dist3 v2 v3 pow 2) /
1619        ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1620        v1 +
1621        delta_x13 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1622        (dist3 v2 v3 pow 2) /
1623        ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1624        v2 +
1625        delta_x14 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1626        (dist3 v2 v3 pow 2) /
1627        ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1628        v3 ` THEN
1629 UNDISCH_TAC `~collinear {(v1:real^3), v2, v3}` THEN
1630 MP_TAC (GEN_ALL ZERO_LE_UPS_X) THEN
1631 REWRITE_TAC[UPS_X_EQ_ZERO_COND] THEN
1632 REWRITE_TAC[MESON[]` a ==> b ==> c <=> a /\ b ==> c `; dist3] THEN
1633 NHANH (MESON[REAL_ARITH ` &0 <= a <=> &0 < a \/ a = &0 `]`
1634    (!(x:real^3) y z.
1635         &0 <= ups_x (dist (x,y) pow 2) (dist (x,z) pow 2) (dist (y,z) pow 2)) /\
1636    ~(ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) = &0)
1637     ==> &0 < ups_x (dist ((v1:real^3),v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) `) THEN
1638 REWRITE_TAC[ GSYM dist3] THEN
1639 STRIP_TAC THEN
1640 UNDISCH_TAC ` &0 < ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2)` THEN
1641 ABBREV_TAC ` a12 = dist3 v1 v2 pow 2 ` THEN ABBREV_TAC ` a13 = dist3 v1 v3 pow 2 ` THEN
1642 ABBREV_TAC ` a23 = dist3 v2 v3 pow 2 ` THEN SIMP_TAC[TO_UYCH] THEN
1643 REWRITE_TAC[MESON[dist3; dist] ` aa = dist3 a b pow 2 <=> aa = norm ( a- b ) pow 2 `] THEN
1644 ONCE_REWRITE_TAC[VECTOR_ARITH ` a - b = a - &1 % b `] THEN
1645 NHANH (GSYM TO_UYCH) THEN SIMP_TAC[] THEN
1646 SIMP_TAC[VECTOR_ARITH ` (a % v1 + b % v2 + c % v3) - (a + b + c) % v2 =
1647      (b % v2 + c % v3 + a % v1) - (b + c + a) % v2 /\
1648   (a % v1 + b % v2 + c % v3) - (a + b + c) % v3 =
1649   (c % v3 + a % v1 + b % v2 ) - ( c + a + b ) % v3 `] THEN
1650 REWRITE_TAC[VECTOR_ARITH` ( a % v1 + b % v2 + c % v3)  -
1651   ( a + b + c ) % v1 = b % ( v2 - v1 ) + c % ( v3 - v1 ) `] THEN
1652 REWRITE_TAC[NORM_POW2_SUM2 ; REAL_ARITH ` &2 * ( a * b ) * c = a * b * &2 * c `] THEN
1653 REWRITE_TAC[VECTOR_ARITH ` &2 * ( x dot y ) = x dot x + y dot y - ( x - y ) dot ( x - y ) `] THEN
1654 REWRITE_TAC[VECTOR_ARITH` v1 - v3 - (v2 - v3) = (v1:real^3) - v2 `] THEN
1655 REWRITE_TAC[X_DOT_X_EQ; GSYM dist; GSYM dist3] THEN
1656 SIMP_TAC[D3_SYM] THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN
1657 UNDISCH_TAC ` ~(ups_x a12 a13 a23 = &0)` THEN NHANH NOT_UPS_X_ZERO_IMP_SMT  THEN
1658 ASM_SIMP_TAC[REAL_DIV_LZERO; REAL_SUB_RZERO] THEN
1659 REWRITE_TAC[aff; AFFINE_HULL_3; IN_ELIM_THM] THEN ASM_MESON_TAC[]);;
1660
1661
1662
1663
1664 let EQ_SUB_DIST_POW2_IMP_IDENTIFIED = prove(` ! v1 v2 v3 (u:real^N) w.
1665 {u,w} SUBSET affine hull {v1,v2,v3} /\
1666 dist (u,v2) pow 2 - dist (u,v1) pow 2 = dist (w,v2) pow 2 - dist (w,v1) pow 2 /\
1667 dist (u,v3) pow 2 - dist (u,v1) pow 2 = dist (w,v3) pow 2 - dist (w,v1) pow 2 ==>
1668 w = u `,
1669 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[DIST_SYM] THEN
1670 SIMP_TAC[SUB_DIST_POW2_INTERPRETE ] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
1671 SIMP_TAC[SUB_DIST_POW2_INTERPRETE ] THEN
1672 ONCE_REWRITE_TAC[REAL_ARITH` a = b <=> a - b = &0 `] THEN
1673 SIMP_TAC[GSYM DOT_LSUB] THEN
1674 SIMP_TAC[GSYM DOT_LSUB; VECTOR_ARITH` a - b - ( aa - b ) =
1675   (a:real^N) - aa `; GSYM VECTOR_SUB_LDISTRIB; AFFINE_HULL_3;
1676   SET2_SU_EX; IN_ELIM_THM] THEN STRIP_TAC THEN
1677 REPEAT (FIRST_X_ASSUM MP_TAC ) THEN
1678 REWRITE_TAC[MESON[]` a ==> b ==> c <=> b /\ a ==> c `] THEN
1679 NHANH (MESON[]` a = (aa:real^N) /\ la /\ b = bb /\ lb ==>
1680   a - b = aa - bb `) THEN
1681 REWRITE_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `] THEN PHA THEN
1682 STRIP_TAC THEN FIRST_X_ASSUM MP_TAC THEN UNDISCH_TAC`u' = &1 - (v + w')` THEN
1683 UNDISCH_TAC`u'' = &1 - (v' + w'')` THEN SIMP_TAC[] THEN
1684 SIMP_TAC[VECTOR_ARITH` ((&1 - (v' + w'')) % v1 + v' % v2 + w'' % v3) -
1685      ((&1 - (v + w')) % v1 + v % v2 + w' % v3) =
1686   ( v - v' ) % ( v1 - v2 ) + (w' - w'' ) % ( v1 - v3 ) `] THEN
1687 REPEAT STRIP_TAC THEN
1688 ONCE_REWRITE_TAC[VECTOR_ARITH ` a = b <=> b - a = vec 0` ] THEN
1689 REWRITE_TAC[GSYM DOT_EQ_0] THEN FIRST_X_ASSUM MP_TAC THEN
1690 REWRITE_TAC[MESON[]` a = b ==> a dot a = &0 <=> a = b ==>
1691   a dot b = &0 `] THEN
1692 REWRITE_TAC[DOT_RADD; DOT_RMUL; REAL_ARITH ` a * ( b dot c ) + aa * bb = &0
1693   <=> a * &2 * ( b dot c ) + aa * &2 * bb = &0 `] THEN
1694 ONCE_REWRITE_TAC[GSYM DOT_LMUL] THEN
1695 ABBREV_TAC ` as = &2 % ((w:real^N) - u) dot (v1 - v2)` THEN
1696 ABBREV_TAC ` bs = &2 % ((w:real^N) - u) dot (v1 - v3)` THEN
1697 DISCH_TAC THEN ASM_SIMP_TAC[] THEN REAL_ARITH_TAC);;
1698
1699 (* lemma 16 SDIHJZK *)
1700
1701 let SDIHJZK = prove(`! (v1:real^3) v2 v3 (a01: real) a02 a03.
1702          ~collinear {v1, v2, v3} /\
1703          (let x12 = dist3 v1 v2 pow 2 in
1704           let x13 = dist3 v1 v3 pow 2 in
1705           let x23 = dist3 v2 v3 pow 2 in delta a01 a02 a03 x12 x13 x23 = &0)
1706          ==> (?v0. v0 IN aff {v1,v2,v3} /\
1707                     a01 = dist3 v0 v1 pow 2 /\
1708                     a02 = dist3 v0 v2 pow 2 /\
1709                     a03 = dist3 v0 v3 pow 2 /\
1710                    (! vv0. vv0 IN aff {v1,v2,v3} /\
1711                     a01 = dist3 vv0 v1 pow 2 /\
1712                     a02 = dist3 vv0 v2 pow 2 /\
1713                     a03 = dist3 vv0 v3 pow 2 ==> vv0 = v0 ) /\
1714                     (let x12 = dist3 v1 v2 pow 2 in
1715                      let x13 = dist3 v1 v3 pow 2 in
1716                      let x23 = dist3 v2 v3 pow 2 in
1717                      let vv = ups_x x12 x13 x23 in
1718                      let t1 = delta_x12 a01 a02 a03 x12 x13 x23  / vv in
1719                      let t2 = delta_x13 a01 a02 a03 x12 x13 x23  / vv in
1720                      let t3 = delta_x14 a01 a02 a03 x12 x13 x23  / vv in
1721                      v0 = t1 % v1 + t2 % v2 + t3 % v3))`,
1722 REPEAT GEN_TAC THEN NHANH (SPEC_ALL HALF_OF_LE16  ) THEN STRIP_TAC THEN
1723 EXISTS_TAC `v0:real^3` THEN ASM_SIMP_TAC[] THEN
1724 GEN_TAC THEN UNDISCH_TAC ` (v0:real^3) IN aff {v1, v2, v3}` THEN
1725 ONCE_REWRITE_TAC[REAL_ARITH ` a1 = b1 /\ a2 = b2 /\ a3 = b3 <=>
1726   a2 - a1 = b2 - b1 /\ a3 - a1 = b3 - b1 /\ a1 = b1 `] THEN
1727 REWRITE_TAC[aff; SET2_SU_EX] THEN REWRITE_TAC[dist3] THEN
1728 PHA THEN MESON_TAC[SET2_SU_EX; EQ_SUB_DIST_POW2_IMP_IDENTIFIED]);;
1729
1730
1731
1732 let SDIHJZK_INTERPRETE = prove(`!(v1:real^3) v2 v3 a01 a02 a03.
1733      ~collinear {v1, v2, v3} /\
1734      delta a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) =
1735      &0
1736      ==> (?v0. v0 IN aff {v1, v2, v3} /\
1737                a01 = dist3 v0 v1 pow 2 /\
1738                a02 = dist3 v0 v2 pow 2 /\
1739                a03 = dist3 v0 v3 pow 2 /\
1740                (!vv0. vv0 IN aff {v1, v2, v3} /\
1741                       a01 = dist3 vv0 v1 pow 2 /\
1742                       a02 = dist3 vv0 v2 pow 2 /\
1743                       a03 = dist3 vv0 v3 pow 2
1744                       ==> vv0 = v0) /\
1745                v0 =
1746                delta_x12 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1747                (dist3 v2 v3 pow 2) /
1748                ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1749                v1 +
1750                delta_x13 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1751                (dist3 v2 v3 pow 2) /
1752                ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1753                v2 +
1754                delta_x14 a01 a02 a03 (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2)
1755                (dist3 v2 v3 pow 2) /
1756                ups_x (dist3 v1 v2 pow 2) (dist3 v1 v3 pow 2) (dist3 v2 v3 pow 2) %
1757                v3)`, MP_TAC SDIHJZK THEN LET_TR THEN SIMP_TAC[]);;
1758
1759
1760
1761 let DELTA_RRR_INTERPRETE = prove(` delta r r r a b c = -- a * b * c + r * ups_x a b c `,
1762 REWRITE_TAC[delta; ups_x] THEN REAL_ARITH_TAC);;
1763
1764
1765 let NOT_UPS_X_EQ_0_IMP = prove(` ~( ups_x a b c = &0 )
1766  ==> delta ( ( a * b * c ) / ups_x a b c ) ( ( a * b * c ) / ups_x a b c )
1767   ( ( a * b * c ) / ups_x a b c ) a b c = &0 `,
1768 REWRITE_TAC[DELTA_RRR_INTERPRETE ] THEN CONV_TAC REAL_FIELD);;
1769
1770
1771
1772
1773 let COL_EQ_UPS_0 = GEN_ALL (MESON[FHFMKIY]` collinear {(v1:real^3), v2, v3} <=>
1774  ups_x (dist (v1,v2) pow 2) (dist (v1,v3) pow 2) (dist (v2,v3) pow 2) = &0`);;
1775
1776
1777 (* CDEUSDF POST ZERO_LE_UPS_X *)
1778
1779
1780 let REAL_LE_SQUARE_POW =
1781 MESON[REAL_POW_2; REAL_LE_SQUARE]`! x. &0 <= x pow 2 `;;
1782
1783
1784 let PROVE_EXISTS_RADV = prove(`!(va:real^3) vb vc.
1785      ~collinear {va, vb, vc}
1786      ==> (?p. p IN affine hull {va, vb, vc} /\
1787               (?c. ( !w. w IN {va, vb, vc} ==> c = dist (p,w)) /\
1788                  (!p'. p' IN affine hull {va, vb, vc} /\
1789                     ( !w. w IN {va, vb, vc} ==> c = dist (p',w))
1790                     ==> p = p'))) `,
1791 REWRITE_TAC[COL_EQ_UPS_0] THEN
1792 NHANH (NOT_UPS_X_EQ_0_IMP ) THEN
1793 REWRITE_TAC[GSYM COL_EQ_UPS_0] THEN
1794 REWRITE_TAC[GSYM dist3] THEN
1795 NHANH (SPEC_ALL SDIHJZK_INTERPRETE) THEN
1796 REWRITE_TAC[EXISTS_UNIQUE] THEN
1797 REPEAT STRIP_TAC THEN
1798 ABBREV_TAC ` r = (dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
1799       ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2)  ` THEN
1800 EXISTS_TAC ` v0 :real^3` THEN
1801 UNDISCH_TAC ` (v0:real^3) IN aff {va, vb, vc}` THEN
1802 SIMP_TAC[aff; SET_RULE ` (! x. x IN {a,b,c} ==> P x ) <=>
1803   P a /\ P b /\ P c `] THEN
1804 DISCH_TAC THEN EXISTS_TAC ` sqrt ( r ) ` THEN
1805 UNDISCH_TAC ` (dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
1806       ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) = r` THEN
1807 NHANH (MESON[REAL_LE_SQUARE_POW; REAL_LE_DIV; REAL_LE_MUL;
1808   ZERO_LE_UPS_X ]` (dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
1809  ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) =
1810  r ==> &0 <= r `) THEN
1811 SIMP_TAC[SQRT_WORKS; EQ_POW2_COND; D3_POS_LE] THEN
1812 ASM_MESON_TAC[aff]);;
1813
1814
1815
1816
1817 let COND_FOR_CIRCUMCENTER_PROPERTIESS = prove(`~collinear {(v1:real^3), v2, v3}
1818  ==> circumcenter {v1, v2, v3} IN affine hull {v1, v2, v3} /\
1819      (?c. !v. v IN {v1, v2, v3} ==> c = dist (circumcenter {v1, v2, v3}, v))`,
1820 NHANH (MESON[PROVE_EXISTS_RADV]`~collinear {(va:real^3), vb, vc}
1821          ==> (?p. p IN affine hull {va, vb, vc} /\
1822                   (?c. (!w. w IN {va, vb, vc} ==> c = dist (p,w)))) `) THEN
1823 REWRITE_TAC[IN; circumcenter] THEN MESON_TAC[EXISTS_THM]);;
1824
1825
1826 let DELTA_X14_RRR = prove(` delta_x14 r r r a b c = a * ( b + c - a ) `,
1827 REWRITE_TAC[delta_x14] THEN REAL_ARITH_TAC);;
1828
1829
1830 let DELTA_X1I_RRR = prove(` delta_x12 r r r a b c = c * ( b + a - c ) /\
1831   delta_x13 r r r a b c = b * ( c + a  - b ) /\
1832   delta_x14 r r r a b c = a * (c + b - a) `,
1833 REWRITE_TAC[delta_x12; delta_x13; delta_x14] THEN REAL_ARITH_TAC);;
1834
1835
1836
1837
1838
1839 let PRE_RADV_COND = prove(` ~ collinear {va,vb,vc} ==>
1840 (? c. ! w. {va,vb,(vc:real^3)} w ==> c = dist(circumcenter {va,vb,vc} , w )) `,
1841 NHANH (COND_FOR_CIRCUMCENTER_PROPERTIESS ) THEN MESON_TAC[IN]);;
1842
1843
1844 let NOT_COL_IMP_RADV_PROPERTIY = prove(` ~collinear {(va:real^3), vb, vc}
1845  ==>  ( ! w. {va, vb, vc} w ==>
1846   radV {va, vb, vc} = dist (circumcenter {va, vb, vc},w)) `,
1847 NHANH (PRE_RADV_COND ) THEN SIMP_TAC[EXISTS_THM; radV]);;
1848
1849
1850
1851
1852 let CIRCUMCENTER_FORMULAR2 = prove(`! (va:real^3) vb vc a b c.
1853      a = dist3 vb vc /\ b = dist3 va vc /\ c = dist3 va vb /\ ~collinear {va, vb, vc}
1854      ==>
1855          (let al_a =
1856               (a pow 2 * (b pow 2 + c pow 2 - a pow 2)) /
1857               (ups_x (a pow 2) (b pow 2) (c pow 2)) in
1858           let al_b =
1859               (b pow 2 * (a pow 2 + c pow 2 - b pow 2)) /
1860               (ups_x (a pow 2) (b pow 2) (c pow 2)) in
1861           let al_c =
1862               (c pow 2 * (a pow 2 + b pow 2 - c pow 2)) /
1863               (ups_x (a pow 2) (b pow 2) (c pow 2)) in
1864           al_a % va + al_b % vb + al_c % vc = circumcenter {va, vb, vc})`,
1865 REWRITE_TAC[COL_EQ_UPS_0] THEN
1866 NHANH (NOT_UPS_X_EQ_0_IMP) THEN
1867 REWRITE_TAC[GSYM COL_EQ_UPS_0; GSYM dist3] THEN
1868 NHANH (SPEC_ALL SDIHJZK_INTERPRETE ) THEN
1869 REPEAT STRIP_TAC THEN
1870 ABBREV_TAC ` r = (dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
1871            ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) ` THEN
1872 UNDISCH_TAC ` v0 =
1873       delta_x12 r r r (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) /
1874       ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) %
1875       va +
1876       delta_x13 r r r (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) /
1877       ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) %
1878       vb +
1879       delta_x14 r r r (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) /
1880       ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) %
1881       vc`  THEN
1882 LET_TR THEN
1883 UNDISCH_TAC ` a = dist3 vb vc ` THEN
1884 UNDISCH_TAC ` b = dist3 va vc ` THEN
1885 UNDISCH_TAC ` c = dist3 va vb ` THEN
1886 SIMP_TAC[DELTA_X1I_RRR] THEN
1887 SIMP_TAC[MESON[UPS_X_SYM]` ups_x a b c = ups_x c b a `] THEN
1888 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
1889 SIMP_TAC[] THEN
1890 REPEAT STRIP_TAC THEN
1891 UNDISCH_TAC ` ~collinear {(va:real^3), vb, vc} ` THEN
1892 NHANH (COND_FOR_CIRCUMCENTER_PROPERTIESS) THEN
1893 REWRITE_TAC[SET_RULE ` (! x. x IN {a,b,c} ==> P x )
1894   <=> P a /\ P b /\ P c `] THEN
1895 REWRITE_TAC[SET_RULE ` (! x. x IN {a,b,c} ==> P x )
1896   <=> P a /\ P b /\ P c `; MESON[]` (? cc. cc = a /\ cc = b /\ cc = c)
1897   <=> a = b /\ a = c  `] THEN
1898 UNDISCH_TAC ` v0 IN aff {va, vb, (vc:real^3)}` THEN
1899 REWRITE_TAC[aff; SET_RULE ` a IN s ==> b /\ aa IN s /\ l ==>
1900   ll <=> b ==>  {a,aa} SUBSET s /\ l ==> ll `] THEN
1901 DISCH_TAC THEN
1902 UNDISCH_TAC` r = dist3 v0 va pow 2 ` THEN
1903 UNDISCH_TAC` r = dist3 v0 vb pow 2 ` THEN
1904 UNDISCH_TAC` r = dist3 v0 vc pow 2 ` THEN
1905 REWRITE_TAC[MESON[]` r = a1 ==> r = a2 ==> r = a3 ==> l ==> ll <=>
1906   r = a1 /\ l /\ a2 = a3 /\ a1 = a3 ==> ll `;dist3] THEN
1907 ONCE_REWRITE_TAC[MESON[]` dist(a,b) = s <=> s = dist(a,b) `] THEN
1908 SIMP_TAC[DIST_POS_LE; EQ_POW2_COND] THEN
1909 ONCE_REWRITE_TAC[REAL_ARITH` a = b <=> a - b = &0 `] THEN
1910 MESON_TAC[EQ_SUB_DIST_POW2_IMP_IDENTIFIED ]);;
1911
1912 let REAL_LE_POW_2 = prove(` ! x. &0 <= x pow 2 `,
1913 REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE]);;
1914
1915
1916
1917 let NOT_COLL_IMP_RADV_FORMULAR = prove(`! (va:real^3) vb vc a b c.
1918      a = dist3 vb vc /\ b = dist3 va vc /\ c = dist3 va vb /\ ~collinear {va, vb, vc}
1919      ==>  radV {va, vb, vc} = eta_y a b c`,
1920 REWRITE_TAC[COL_EQ_UPS_0] THEN
1921 NHANH (NOT_UPS_X_EQ_0_IMP) THEN
1922 REWRITE_TAC[GSYM COL_EQ_UPS_0; GSYM dist3] THEN
1923 NHANH (SPEC_ALL SDIHJZK_INTERPRETE ) THEN
1924 REPEAT STRIP_TAC THEN
1925 ABBREV_TAC ` r = (dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
1926            ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2) ` THEN
1927 LET_TR THEN
1928 UNDISCH_TAC ` a = dist3 vb vc ` THEN
1929 UNDISCH_TAC ` b = dist3 va vc ` THEN
1930 UNDISCH_TAC ` c = dist3 va vb ` THEN
1931 SIMP_TAC[DELTA_X1I_RRR] THEN
1932 SIMP_TAC[MESON[UPS_X_SYM]` ups_x a b c = ups_x c b a `] THEN
1933 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
1934 SIMP_TAC[] THEN
1935 REPEAT STRIP_TAC THEN
1936 UNDISCH_TAC ` ~collinear {(va:real^3), vb, vc} ` THEN
1937 NHANH (COND_FOR_CIRCUMCENTER_PROPERTIESS) THEN
1938 REWRITE_TAC[SET_RULE ` (! x. x IN {a,b,c} ==> P x )
1939   <=> P a /\ P b /\ P c `] THEN
1940 REWRITE_TAC[SET_RULE ` (! x. x IN {a,b,c} ==> P x )
1941   <=> P a /\ P b /\ P c `; MESON[]` (? cc. cc = a /\ cc = b /\ cc = c)
1942   <=> a = b /\ a = c  `] THEN
1943 UNDISCH_TAC ` v0 IN aff {va, vb, (vc:real^3)}` THEN
1944 REWRITE_TAC[aff; SET_RULE ` a IN s ==> b /\ aa IN s /\ l ==>
1945   ll <=> b ==>  {a,aa} SUBSET s /\ l ==> ll `] THEN
1946 DISCH_TAC THEN
1947 UNDISCH_TAC` r = dist3 v0 va pow 2 ` THEN
1948 UNDISCH_TAC` r = dist3 v0 vb pow 2 ` THEN
1949 UNDISCH_TAC` r = dist3 v0 vc pow 2 ` THEN
1950 REWRITE_TAC[MESON[]` r = a1 ==> r = a2 ==> r = a3 ==> l ==> ll <=>
1951   r = a1 /\ l /\ a2 = a3 /\ a1 = a3 ==> ll `;dist3] THEN
1952 ONCE_REWRITE_TAC[MESON[]` dist(a,b) = s <=> s = dist(a,b) `] THEN
1953 SIMP_TAC[DIST_POS_LE; EQ_POW2_COND] THEN
1954 ONCE_REWRITE_TAC[REAL_ARITH` a = b <=> a - b = &0 `] THEN
1955 REWRITE_TAC[MESON[]` ( a /\ a1 = &0 /\ a2 = &0 ) /\ b1 = &0 /\ b2 = &0 <=>
1956   b1 = &0 /\ b2 = &0 /\ a /\ b1 = a1 /\ b2 = a2 `] THEN
1957 NHANH (SPEC_ALL EQ_SUB_DIST_POW2_IMP_IDENTIFIED ) THEN
1958 STRIP_TAC THEN
1959 UNDISCH_TAC ` ~collinear {(va:real^3), vb, vc}` THEN
1960 NHANH (NOT_COL_IMP_RADV_PROPERTIY ) THEN
1961 FIRST_X_ASSUM MP_TAC THEN
1962 SIMP_TAC[] THEN
1963 SIMP_TAC[SET_RULE ` (!w. {va, vb, vc} w ==> P w ) <=>
1964   P va /\ P vb /\ P vc `] THEN
1965 REPEAT STRIP_TAC THEN
1966 EXPAND_TAC "a" THEN
1967 EXPAND_TAC "b" THEN
1968 EXPAND_TAC "c" THEN
1969 UNDISCH_TAC ` r - dist ((v0:real^3),vc) pow 2 = &0 ` THEN
1970 SIMP_TAC[REAL_ARITH` a - b = &0 <=> b = a `] THEN
1971 EXPAND_TAC "r" THEN
1972 REWRITE_TAC[eta_y; eta_x] THEN
1973 LET_TR THEN
1974 MP_TAC (GEN_ALL ZERO_LE_UPS_X) THEN
1975 SIMP_TAC[GSYM REAL_POW_2] THEN
1976 SIMP_TAC[REAL_ARITH` a * b * c = c * b * a `;
1977   UPS_X_SYM; dist3] THEN
1978 MP_TAC (MESON[dist3; DIST_POS_LE]` &0 <= dist3 v0 vc `) THEN
1979 MP_TAC (MESON[REAL_LE_DIV; REAL_LE_MUL_EQ; REAL_LE_POW_2;REAL_LE_MUL; ZERO_LE_UPS_X;
1980 SQRT_WORKS]` &0 <= ((dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
1981       ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2)) /\
1982   &0 <= sqrt ((dist3 va vb pow 2 * dist3 va vc pow 2 * dist3 vb vc pow 2) /
1983       ups_x (dist3 va vb pow 2) (dist3 va vc pow 2) (dist3 vb vc pow 2)) `) THEN
1984 REWRITE_TAC[MESON[]` a ==> b ==> c <=> b /\ a ==> c `] THEN
1985 MATCH_MP_TAC (MESON[]` (a1 /\ a3 ==> l) ==> a1 /\a2 /\a3 ==> l`) THEN
1986 SIMP_TAC[dist3; EQ_POW2_COND; SQRT_WORKS]);;
1987
1988
1989 let CDEUSDF = prove(`!(va:real^3) vb vc a b c.
1990      a = dist3 vb vc /\ b = dist3 va vc /\ c = dist3 va vb /\ ~collinear {va, vb, vc}
1991      ==> (?p. p IN affine hull {va, vb, vc} /\
1992               (?c. ( !w. w IN {va, vb, vc} ==> c = dist (p,w)) /\
1993               (!p'. p' IN affine hull {va, vb, vc} /\
1994                     ( !w. w IN {va, vb, vc} ==> c = dist (p',w))
1995                     ==> p = p'))) /\
1996          (let al_a =
1997               (a pow 2 * (b pow 2 + c pow 2 - a pow 2)) /
1998               (ups_x (a pow 2) (b pow 2) (c pow 2)) in
1999           let al_b =
2000               (b pow 2 * (a pow 2 + c pow 2 - b pow 2)) /
2001               (ups_x (a pow 2) (b pow 2) (c pow 2)) in
2002           let al_c =
2003               (c pow 2 * (a pow 2 + b pow 2 - c pow 2)) /
2004               (ups_x (a pow 2) (b pow 2) (c pow 2)) in
2005           al_a % va + al_b % vb + al_c % vc = circumcenter {va, vb, vc}) /\
2006          radV {va, vb, vc} = eta_y a b c`,
2007 SIMP_TAC[PROVE_EXISTS_RADV; CIRCUMCENTER_FORMULAR2;  NOT_COLL_IMP_RADV_FORMULAR ]);;
2008
2009 let LEMMA17 = CDEUSDF;;
2010
2011 let DIST_EQ_IS_UNIQUE = prove(` {u, w} SUBSET affine hull {v1, v2, v3} /\
2012   dist (u,v2) = dist (u,v1) /\ dist (u,v3) = dist (u,v1) /\
2013   dist (w,v2) = dist (w,v1) /\ dist (w,v3) = dist (w,v1) ==>
2014   u = w `,
2015 SIMP_TAC[EQ_POW2_COND; DIST_POS_LE] THEN ONCE_REWRITE_TAC[REAL_ARITH`
2016  a = b <=> a - b = &0 `] THEN MESON_TAC[EQ_SUB_DIST_POW2_IMP_IDENTIFIED]);;
2017
2018
2019 let NEVER_USED_AGAIN = prove(` p IN affine hull {va, vb, vc} /\ c = dist (p,va)
2020 /\ c = dist (p,vb) /\ c = dist (p,vc)  ==>
2021   (! p'.  p' IN affine hull {va, vb, vc} /\
2022            dist (p',vb) = dist (p',va) /\
2023            dist (p',vc) = dist (p',va) <=>
2024   p' IN affine hull {va, vb, vc} /\
2025   c = dist (p',va) /\
2026   c = dist (p',vb) /\
2027   c = dist (p',vc) )`,
2028 MESON_TAC[DIST_EQ_IS_UNIQUE; SET2_SU_EX]);;
2029
2030
2031
2032 let TRUONG_WELL = prove(`! (va:real^3) vb vc. ~collinear {va, vb, vc}
2033      ==> (?p. p IN affine hull {va, vb, vc} /\
2034               (?c. !w. w IN {va, vb, vc} ==> c = dist (p,w)) /\
2035               (!p'. p' IN affine hull {va, vb, vc} /\
2036                     (?c. !w. w IN {va, vb, vc} ==> c = dist (p',w))
2037                     ==> p = p'))`,
2038 NHANH (SPEC_ALL PROVE_EXISTS_RADV) THEN REPEAT STRIP_TAC THEN EXISTS_TAC `p:real^3`
2039 THEN CONJ_TAC THENL [ASM_SIMP_TAC[]; CONJ_TAC] THENL [ASM_MESON_TAC[];
2040 REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN
2041 REWRITE_TAC[SET_RULE` (!a. a IN {x,y,z} ==> p a)
2042   <=> p x /\ p y /\ p z `] THEN
2043 REWRITE_TAC[MESON[]` (?c. c = a /\ c = b /\ c = cc ) <=>
2044  b = a /\ cc = a `]] THEN
2045 REWRITE_TAC[MESON[]` a ==> b ==> c <=> a /\b ==> c `] THEN
2046   PHA THEN MESON_TAC[NEVER_USED_AGAIN ]);;
2047
2048
2049
2050
2051 let NGAY_MONG6 = MESON[TRUONG_WELL] `! va vb (vc:real^3).
2052          ~collinear {va, vb, vc} ==> (?p. p IN affine hull {va, vb, vc} /\
2053                   (?c. !w. w IN {va, vb, vc} ==> c = dist (p,w))  ) `;;
2054
2055
2056 let CIRCUMCENTER_PROPTIES = prove(`!va vb (vc:real^3).
2057      ~collinear {va, vb, vc}
2058      ==> circumcenter {va, vb, vc} IN affine hull {va, vb, vc} /\
2059 (?c. !w. w IN {va, vb, vc}
2060                   ==> c = dist (circumcenter {va, vb, vc},w))`,
2061 NHANH (SPEC_ALL NGAY_MONG6) THEN REWRITE_TAC[IN;
2062 circumcenter; EXISTS_THM] THEN SIMP_TAC[]);;
2063
2064
2065
2066
2067
2068
2069 let SIMP_DOT_ALEM = prove(  `&0 < (b - a) dot x <=> x dot (a - b) < &0`,
2070 SIMP_TAC[DOT_SYM] THEN
2071 REWRITE_TAC[ REAL_ARITH ` a < &0 <=> &0 < -- a `; GSYM DOT_RNEG] THEN
2072 REWRITE_TAC[VECTOR_ARITH ` -- ((a:real^N) - b) = b - a `]);;
2073
2074
2075
2076
2077 let MONG7_ROI = prove(` ! p a (b:real^A). dist (p,a) = dist (p,b) <=>
2078   (p - &1 / &2 % ( a + b )) dot ( a - b)  = &0 `,
2079 REWRITE_TAC[ REAL_ARITH ` a = b <=> ~ ( a < b) /\ ~( b < a ) `;
2080 DIST_LT_HALF_PLANE] THEN
2081 REWRITE_TAC[VECTOR_ARITH` (p - &1 / &2 % (a + b)) dot (a - b)
2082   = &1 / &2 * ( (&2 % p - (a + b ) ) dot ( a- b ) )  `] THEN
2083 REWRITE_TAC[REAL_ARITH `( &1 / &2 * a < &0 <=> a < &0) /\
2084 (&0 < &1 / &2 * a <=> &0 < a )`] THEN
2085 REWRITE_TAC[SIMP_DOT_ALEM] THEN
2086 SIMP_TAC[VECTOR_ARITH` (a - b) dot (c - d) = (b - a) dot (d - c)`; DOT_SYM;
2087 VECTOR_ADD_SYM] THEN MESON_TAC[]);;
2088
2089 let LEMMA26 = prove(`!v1 v2 (v3:real^3) p.
2090      ~collinear {v1, v2, v3} /\ p = circumcenter {v1, v2, v3}
2091      ==> (p - &1 / &2 % (v1 + v2)) dot (v1 - v2) = &0 /\
2092          (p - &1 / &2 % (v2 + v3)) dot (v2 - v3) = &0 /\
2093          (p - &1 / &2 % (v3 + v1)) dot (v3 - v1) = &0`,
2094 NHANH (SPEC_ALL CIRCUMCENTER_PROPTIES) THEN
2095 NHANH (SET_RULE` (?c. !w. w IN {v1, v2, v3} ==> c = P w) ==> P v1 = P v2
2096   /\ P v2 = P v3 /\ P v3 = P v1 `) THEN
2097 SIMP_TAC[MONG7_ROI]);;
2098
2099 let POXDVXO = LEMMA26;;
2100
2101
2102
2103 let NOT_COLL_IMP_RADV_EQ_ETA_Y = MESON[prove(`!va vb vc a b c.
2104      a = dist3 vb vc /\ b = dist3 va vc /\ c = dist3 va vb /\ ~collinear {va, vb, vc}
2105      ==> radV {va, vb, vc} = eta_y (dist3 vb vc) (dist3 va vc) (dist3 va vb)`,
2106 SIMP_TAC[CDEUSDF])]`
2107   !va vb vc . ~collinear {va, vb, vc}
2108      ==> radV {va, vb, vc} = eta_y (dist3 vb vc) (dist3 va vc) (dist3 va vb)`;;
2109
2110 let COLLINEAR2 = prove(` ! x (y:real^N). collinear {x,y} `,
2111    REPEAT GEN_TAC THEN REWRITE_TAC[collinear] THEN
2112    EXISTS_TAC ` x -(y: real^N)` THEN
2113    ASM_SIMP_TAC[SET_RULE` a = b ==> {a,b,c} = {a,c} `] THEN
2114    REWRITE_TAC[IN_SET2] THEN
2115    REPEAT GEN_TAC THEN
2116    STRIP_TAC THENL
2117    [ASM_SIMP_TAC[] THEN EXISTS_TAC ` &0 ` THEN CONV_TAC VECTOR_ARITH;
2118    ASM_SIMP_TAC[] THEN EXISTS_TAC ` &1 ` THEN CONV_TAC VECTOR_ARITH;
2119    ASM_SIMP_TAC[] THEN EXISTS_TAC ` -- &1 ` THEN CONV_TAC VECTOR_ARITH;
2120    ASM_SIMP_TAC[] THEN EXISTS_TAC ` &0 ` THEN CONV_TAC VECTOR_ARITH]
2121                       );;
2122
2123 let TWO_EQ_IMP_COL3 = prove(` ! (x:real^N) y z .  x = y ==> collinear {x, y, z} `,
2124 STRIP_TR THEN SIMP_TAC[SET_RULE` a = b ==> {a,b,c} = {a,c} `; COLLINEAR2]);;
2125
2126
2127 let NOT_CO_IMP_DIST_POS = prove(`! x y z. ~ collinear {x,y,z} ==> &0 < dist (x,y) `,
2128 NHANH (MESON[TWO_EQ_IMP_COL3]` ~collinear {x, y, z} ==> ~( x= y) `) THEN
2129 SIMP_TAC[DIST_POS_LT]);;
2130
2131
2132 let NOT_COLL_IMP_POS_SUM = prove( ` !x y z.
2133      ~collinear {x, y, z} ==> &0 < ( dist3 x y + dist3 y z + dist3 z x) / &2 `,
2134 NHANH (SPEC_ALL NOT_CO_IMP_DIST_POS) THEN
2135 NHANH (MESON[DIST_POS_LE]` ~collinear {x, y, z} ==>
2136   &0 <= dist (y,z) /\ &0 <= dist (z,x) `) THEN
2137 SIMP_TAC[dist3] THEN REAL_ARITH_TAC);;
2138
2139 let PER_SET2 = SET_RULE ` {a,b} = {b,a} `;;
2140
2141
2142 let COLLINEAR_AS_IN_CONV2 = MESON[PER_SET2; COLLINERA_AS_IN_CONV2]`! x y (z:real^3). collinear {x, y, z} <=>
2143  x IN conv {y, z} \/ y IN conv {z, x} \/ z IN conv {x, y}`;;
2144
2145 let COLLINEAR_IMP_POS_UPS2 = prove(` ! x y (z:real^3). ~ collinear {x,y,z} ==>
2146   &0 < ups_x_pow2 ( dist3 x y ) ( dist3 y z ) ( dist3 z x ) `,
2147 REWRITE_TAC[PRE_HER] THEN NHANH (SPEC_ALL NOT_COLL_IMP_POS_SUM ) THEN
2148 REWRITE_TAC[COLLINEAR_AS_IN_CONV2] THEN REWRITE_TAC[MID_COND] THEN
2149 REWRITE_TAC[LENGTH_EQ_EX] THEN REWRITE_TAC[DE_MORGAN_THM] THEN
2150 SIMP_TAC[dist3] THEN REPEAT GEN_TAC THEN SIMP_TAC[
2151 prove(` &0 < a ==> ( &0 < &16 * a * b <=> &0 < b ) `,
2152 REWRITE_TAC[REAL_ARITH ` &0 < &16 * a <=> &0 < a `] THEN
2153 REWRITE_TAC[REAL_LT_MUL_EQ])] THEN
2154 REWRITE_TAC[REAL_ARITH ` (a + b + c ) / &2 - a = ( b + c - a ) / &2 `] THEN
2155 REWRITE_TAC[REAL_ARITH ` (a + b + c ) / &2 - b = ( c + a - b ) / &2 `] THEN
2156 REWRITE_TAC[REAL_ARITH ` (a + b + c ) / &2 - c = ( a + b - c ) / &2 `] THEN
2157 REWRITE_TAC[REAL_ARITH ` a < b + c <=> &0 < ( b + c - a ) / &2 `] THEN
2158 SIMP_TAC[DIST_SYM] THEN SIMP_TAC[REAL_ARITH ` a + b - c = b + a - c `] THEN
2159 SIMP_TAC[REAL_LT_MUL]);;
2160
2161
2162
2163 let RADV_FORMULAR = MESON[CDEUSDF]` !(va:real^3) vb vc.
2164      ~collinear {va, vb, vc}
2165      ==> radV {va, vb, vc} = eta_y (dist3 vb vc) (dist3 va vc) (dist3 va vb)`;;
2166
2167
2168
2169 let MUL3_SYM = REAL_ARITH ` ! a b c. a * b * c = b * a * c /\
2170   a * b * c = c * b * a `;;
2171
2172 let ETA_X_SYMM = prove(` ! a b c. eta_x a b c = eta_x b a c /\
2173  eta_x a b c = eta_x c b a `,SIMP_TAC[eta_x; MUL3_SYM; UPS_X_SYM]);;
2174
2175 let ETA_Y_SYYM = prove(` ! x y z. eta_y x y z = eta_y y x z /\
2176 eta_y x y z = eta_y z y x `, REWRITE_TAC[eta_y] THEN
2177 CONV_TAC (TOP_DEPTH_CONV let_CONV) THEN MESON_TAC[ETA_X_SYMM]);;
2178
2179
2180
2181 let NOT_COL3_IMP_DIFF = MESON[PER_SET3; TWO_EQ_IMP_COL3]`!a b c.
2182 ~collinear {a, b, c} ==> ~(a = b \/ a = c \/ b = c)`;;
2183
2184 let LET_TR = CONV_TAC (TOP_DEPTH_CONV let_CONV);;
2185
2186
2187 let POW2_COND_LT = MESON[POW2_COND; REAL_ARITH ` &0 < a ==> &0 <= a `]`
2188   !a b. &0 < a /\ &0 < b ==> (a <= b <=> a pow 2 <= b pow 2)`;;
2189
2190
2191 let ETA_Y_2 = prove(` eta_y (&2) (&2) (&2)  = &2 / sqrt (&3) `,
2192 REWRITE_TAC[eta_y; eta_x; ups_x] THEN
2193 LET_TR THEN
2194 REWRITE_TAC[REAL_ARITH ` ((&2 * &2) * (&2 * &2) * &2 * &2) /
2195   (--(&2 * &2) * &2 * &2 - (&2 * &2) * &2 * &2 - (&2 * &2) * &2 * &2 +
2196    &2 * (&2 * &2) * &2 * &2 +
2197    &2 * (&2 * &2) * &2 * &2 +
2198    &2 * (&2 * &2) * &2 * &2) = &4 / &3 `] THEN
2199 MP_TAC (MESON[REAL_LT_DIV; MESON[SQRT_POS_LT; REAL_ARITH` &0 < &3 `] `
2200 &0 < sqrt (&3) `; REAL_ARITH ` &0 < &2 /\ &0 < &4 /\ &0 < &3 `] ` &0 < &4 / &3
2201 /\ &0 < &2 / sqrt (&3) `) THEN
2202 REWRITE_TAC[REAL_ARITH` a = b <=> a <= b /\ b <= a `] THEN
2203 SIMP_TAC[SQRT_POS_LT; POW2_COND_LT] THEN
2204 REWRITE_TAC[GSYM (REAL_ARITH` a = b <=> a <= b /\ b <= a `)] THEN
2205 SIMP_TAC[REAL_LT_IMP_LE; SQRT_POW_2] THEN
2206 REWRITE_TAC[REAL_FIELD` (a/ b) pow 2 = a pow 2 / ( b pow 2 ) `] THEN
2207 SIMP_TAC[REAL_ARITH ` &0 <= &3 `; SQRT_POW_2] THEN
2208 REAL_ARITH_TAC);;
2209
2210 let D3_POS_LE = MESON[dist3; DIST_POS_LE]` ! x y. &0 <= dist3 x y `;;
2211
2212
2213 (* le 19. p 17 *)
2214
2215
2216
2217 let cayleytr = new_definition `
2218   cayleytr x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 =
2219   &2 * x23 * x25 * x34 +
2220       &2 * x23 * x24 * x35 +
2221       -- &1 * x23 pow 2 * x45 +
2222       -- &2 * x15 * x23 * x34 +
2223       -- &2 * x15 * x23 * x24 +
2224       &2 * x15 * x23 pow 2 +
2225       -- &2 * x14 * x23 * x35 +
2226       -- &2 * x14 * x23 * x25 +
2227       &2 * x14 * x23 pow 2 +
2228       &4 * x14 * x15 * x23 +
2229       -- &2 * x13 * x25 * x34 +
2230       -- &2 * x13 * x24 * x35 +
2231       &4 * x13 * x24 * x25 +
2232       &2 * x13 * x23 * x45 +
2233       -- &2 * x13 * x23 * x25 +
2234       -- &2 * x13 * x23 * x24 +
2235       &2 * x13 * x15 * x34 +
2236       -- &2 * x13 * x15 * x24 +
2237       -- &2 * x13 * x15 * x23 +
2238       &2 * x13 * x14 * x35 +
2239       -- &2 * x13 * x14 * x25 +
2240       -- &2 * x13 * x14 * x23 +
2241       -- &1 * x13 pow 2 * x45 +
2242       &2 * x13 pow 2 * x25 +
2243       &2 * x13 pow 2 * x24 +
2244       &4 * x12 * x34 * x35 +
2245       -- &2 * x12 * x25 * x34 +
2246       -- &2 * x12 * x24 * x35 +
2247       &2 * x12 * x23 * x45 +
2248       -- &2 * x12 * x23 * x35 +
2249       -- &2 * x12 * x23 * x34 +
2250    -- &2 * x12 * x15 * x34 +
2251       &2 * x12 * x15 * x24 +
2252       -- &2 * x12 * x15 * x23 +
2253       -- &2 * x12 * x14 * x35 +
2254       &2 * x12 * x14 * x25 +
2255       -- &2 * x12 * x14 * x23 +
2256       &2 * x12 * x13 * x45 +
2257       -- &2 * x12 * x13 * x35 +
2258       -- &2 * x12 * x13 * x34 +
2259       -- &2 * x12 * x13 * x25 +
2260       -- &2 * x12 * x13 * x24 +
2261       &4 * x12 * x13 * x23 +
2262       -- &1 * x12 pow 2 * x45 +
2263       &2 * x12 pow 2 * x35 +
2264       &2 * x12 pow 2 * x34 `;;
2265
2266
2267 let LTCTBAN = prove(` cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 =
2268 ups_x x12 x13 x23 * x45 pow 2 + cayleytr x12 x13 x14 x15 x23 x24 x25 x34 x35 ( &0 )
2269 * x45 + cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 ( &0 ) `,
2270 REWRITE_TAC[ups_x; cayleyR;cayleytr] THEN REAL_ARITH_TAC);;
2271
2272
2273
2274 (* ------------------------------------------------------------------------- *)
2275 (* Flyspeck definitions we use.                                              *)
2276 (* ------------------------------------------------------------------------- *)
2277
2278 let plane = new_definition
2279  `plane x = (?u v w. ~(collinear {u,v,w}) /\ (x = affine hull {u,v,w}))`;;
2280
2281 (* renamed from coplanar, because j. harrison changed the def. -thales *)
2282
2283 let coplanar_alt = new_definition `coplanar_alt S = (?x. plane x /\ S SUBSET x)`;;
2284
2285
2286 (* renamed condA to condA, thales *)
2287
2288 (*
2289 let condA = new_definition `condA (v1:real^3) v2 v3 v4 x12 x13 x14 x23 x24 x34 =
2290   ( ~ ( v1 = v2 ) /\ coplanar_alt {v1,v2,v3,v4} /\
2291   ( dist ( v1, v2) pow 2 ) = x12 /\
2292   dist (v1,v3) pow 2 = x13 /\
2293   dist (v1,v4) pow 2 = x14 /\
2294   dist (v2,v3) pow 2 = x23 /\ dist (v2,v4) pow 2 = x24 )`;;
2295 *)
2296
2297 let det_vec3 = new_definition ` det_vec3 (a:real^3) (b:real^3) (c:real^3) =
2298   a$1 * b$2 * c$3 + b$1 * c$2 * a$3 + c$1 * a$2 * b$3 -
2299   ( a$1 * c$2 * b$3 + b$1 * a$2 * c$3 + c$1 * b$2 * a$3 ) `;;
2300
2301 let COPLANAR_DET_EQ_0 = prove
2302  (`!v0 v1 (v2: real^3) v3.
2303        coplanar_alt {v0,v1,v2,v3} <=>
2304        det(vector[v1 - v0; v2 - v0; v3 - v0]) = &0`,
2305  REPEAT GEN_TAC THEN REWRITE_TAC[DET_EQ_0_RANK; RANK_ROW] THEN
2306  REWRITE_TAC[rows; row; LAMBDA_ETA] THEN
2307  ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
2308  REWRITE_TAC[GSYM numseg; DIMINDEX_3] THEN
2309  CONV_TAC(ONCE_DEPTH_CONV NUMSEG_CONV) THEN
2310  SIMP_TAC[IMAGE_CLAUSES; VECTOR_3] THEN EQ_TAC THENL
2311   [REWRITE_TAC[coplanar_alt; plane; LEFT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
2312    MAP_EVERY X_GEN_TAC
2313     [`p:real^3->bool`; `a:real^3`; `b:real^3`; `c:real^3`] THEN
2314    DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
2315    FIRST_X_ASSUM SUBST1_TAC THEN
2316    W(MP_TAC o PART_MATCH lhand AFFINE_HULL_INSERT_SUBSET_SPAN o
2317        rand o lhand o goal_concl) THEN
2318    REWRITE_TAC[GSYM IMP_CONJ_ALT] THEN
2319    DISCH_THEN(MP_TAC o MATCH_MP SUBSET_TRANS) THEN
2320    DISCH_THEN(MP_TAC o ISPEC `\x:real^3. x - a` o MATCH_MP IMAGE_SUBSET) THEN
2321    ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
2322    REWRITE_TAC[IMAGE_CLAUSES; GSYM IMAGE_o; o_DEF; VECTOR_ADD_SUB; IMAGE_ID;
2323                SIMPLE_IMAGE] THEN
2324    REWRITE_TAC[INSERT_SUBSET] THEN STRIP_TAC THEN
2325    GEN_REWRITE_TAC LAND_CONV [GSYM DIM_SPAN] THEN MATCH_MP_TAC LET_TRANS THEN
2326    EXISTS_TAC `CARD {b - a:real^3,c - a}` THEN
2327    CONJ_TAC THENL
2328     [MATCH_MP_TAC SPAN_CARD_GE_DIM;
2329      SIMP_TAC[CARD_CLAUSES; FINITE_RULES] THEN ARITH_TAC] THEN
2330    REWRITE_TAC[FINITE_INSERT; FINITE_RULES] THEN
2331    GEN_REWRITE_TAC RAND_CONV [GSYM SPAN_SPAN] THEN
2332    MATCH_MP_TAC SPAN_MONO THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
2333    MP_TAC(VECTOR_ARITH `!x y:real^3. x - y = (x - a) - (y - a)`) THEN
2334    DISCH_THEN(fun th -> REPEAT CONJ_TAC THEN
2335      GEN_REWRITE_TAC LAND_CONV [th]) THEN
2336    MATCH_MP_TAC SPAN_SUB THEN ASM_REWRITE_TAC[];
2337
2338    DISCH_TAC THEN
2339    MP_TAC(ISPECL [`{v1 - v0,v2 - v0,v3 - v0}:real^3->bool`; `2`]
2340                  LOWDIM_EXPAND_BASIS) THEN
2341    ASM_REWRITE_TAC[ARITH_RULE `n <= 2 <=> n < 3`; DIMINDEX_3; ARITH] THEN
2342    DISCH_THEN(X_CHOOSE_THEN `t:real^3->bool`
2343     (CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC)) THEN
2344    CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN
2345    REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
2346    MAP_EVERY X_GEN_TAC [`a:real^3`; `b:real^3`] THEN
2347    DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
2348    REWRITE_TAC[coplanar_alt; plane] THEN
2349    EXISTS_TAC `affine hull {v0,v0 + a,v0 + b}:real^3->bool` THEN
2350    CONJ_TAC THENL
2351     [MAP_EVERY EXISTS_TAC [`v0:real^3`; `v0 + a:real^3`; `v0 + b:real^3`] THEN
2352      REWRITE_TAC[COLLINEAR_3; COLLINEAR_LEMMA;
2353                  VECTOR_ARITH `--x = vec 0 <=> x = vec 0`;
2354                  VECTOR_ARITH `u - (u + a):real^3 = --a`;
2355                  VECTOR_ARITH `(u + b) - (u + a):real^3 = b - a`] THEN
2356      REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ;
2357        VECTOR_ARITH `b - a = c % -- a <=> (c - &1) % a + &1 % b = vec 0`] THEN
2358      ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
2359       [ASM_MESON_TAC[IN_INSERT; INDEPENDENT_NONZERO]; ALL_TAC] THEN
2360      DISCH_THEN(X_CHOOSE_TAC `u:real`) THEN
2361      FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [independent]) THEN
2362      REWRITE_TAC[DEPENDENT_EXPLICIT] THEN
2363      MAP_EVERY EXISTS_TAC [`{a:real^3,b}`;
2364                            `\x:real^3. if x = a then u - &1 else &1`] THEN
2365      REWRITE_TAC[FINITE_INSERT; FINITE_RULES; SUBSET_REFL] THEN
2366      CONJ_TAC THENL
2367       [EXISTS_TAC `b:real^3` THEN ASM_REWRITE_TAC[IN_INSERT] THEN
2368        REAL_ARITH_TAC;
2369        ALL_TAC] THEN
2370      SIMP_TAC[VSUM_CLAUSES; FINITE_RULES] THEN
2371      ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; VECTOR_ADD_RID];
2372      ALL_TAC] THEN
2373    W(MP_TAC o PART_MATCH (lhs o rand) AFFINE_HULL_INSERT_SPAN o
2374      rand o goal_concl) THEN
2375    ANTS_TAC THENL
2376     [REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
2377      REWRITE_TAC[VECTOR_ARITH `u = u + a <=> a = vec 0`] THEN
2378      ASM_MESON_TAC[INDEPENDENT_NONZERO; IN_INSERT];
2379      ALL_TAC] THEN
2380    DISCH_THEN SUBST1_TAC THEN
2381    ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
2382    REWRITE_TAC[SIMPLE_IMAGE; IMAGE_CLAUSES; IMAGE_ID; VECTOR_ADD_SUB] THEN
2383    MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC
2384     `IMAGE (\v:real^3. v0 + v) (span{v1 - v0, v2 - v0, v3 - v0})` THEN
2385    ASM_SIMP_TAC[IMAGE_SUBSET] THEN
2386    REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_IMAGE] THEN CONJ_TAC THENL
2387     [EXISTS_TAC `vec 0:real^3` THEN REWRITE_TAC[SPAN_0] THEN VECTOR_ARITH_TAC;
2388      REWRITE_TAC[VECTOR_ARITH `v1:real^N = v0 + x <=> x = v1 - v0`] THEN
2389      REWRITE_TAC[UNWIND_THM2] THEN REPEAT CONJ_TAC THEN
2390      MATCH_MP_TAC SPAN_SUPERSET THEN REWRITE_TAC[IN_INSERT]]]);;
2391
2392
2393 (* renamed from COPLANAR Jan 2013, to avoid clash with hol-light/Multivariate/Flyspeck.ml thm *)
2394
2395 let COPLANAR_ALT = prove
2396  (`2 <= dimindex(:N)
2397   ==> !s:real^N->bool. coplanar_alt s <=> ?u v w. s SUBSET affine hull {u,v,w}`,
2398  DISCH_TAC THEN GEN_TAC THEN REWRITE_TAC[coplanar_alt; plane] THEN
2399  REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
2400  ONCE_REWRITE_TAC[MESON[]
2401   `(?x u v w. p x u v w) <=> (?u v w x. p x u v w)`] THEN
2402  REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM; UNWIND_THM2] THEN
2403  EQ_TAC THENL [MESON_TAC[]; REWRITE_TAC[LEFT_IMP_EXISTS_THM]] THEN
2404  MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`; `w:real^N`] THEN DISCH_TAC THEN
2405  SUBGOAL_THEN
2406   `s SUBSET {u + x:real^N | x | x IN span {y - u | y IN {v,w}}}`
2407  MP_TAC THENL
2408   [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
2409     (REWRITE_RULE[IMP_CONJ] SUBSET_TRANS)) THEN
2410    REWRITE_TAC[AFFINE_HULL_INSERT_SUBSET_SPAN];
2411    ALL_TAC] THEN
2412  ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
2413  DISCH_THEN(MP_TAC o ISPEC `\x:real^N. x - u` o MATCH_MP IMAGE_SUBSET) THEN
2414  REWRITE_TAC[GSYM IMAGE_o; o_DEF; VECTOR_ADD_SUB; IMAGE_ID; SIMPLE_IMAGE] THEN
2415  REWRITE_TAC[IMAGE_CLAUSES] THEN
2416  MP_TAC(ISPECL [`{v - u:real^N,w - u}`; `2`] LOWDIM_EXPAND_BASIS) THEN
2417  ANTS_TAC THENL
2418   [ASM_REWRITE_TAC[] THEN MATCH_MP_TAC LE_TRANS THEN
2419    EXISTS_TAC `CARD{v - u:real^N,w - u}` THEN
2420    SIMP_TAC[DIM_LE_CARD; FINITE_INSERT; FINITE_RULES] THEN
2421    SIMP_TAC[CARD_CLAUSES; FINITE_RULES] THEN ARITH_TAC;
2422    ALL_TAC] THEN
2423  DISCH_THEN(X_CHOOSE_THEN `t:real^N->bool`
2424   (CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC)) THEN
2425  CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN
2426  REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
2427  MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN
2428  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
2429  UNDISCH_TAC `span {v - u, w - u} SUBSET span {a:real^N, b}` THEN
2430  REWRITE_TAC[GSYM IMP_CONJ_ALT] THEN
2431  DISCH_THEN(ASSUME_TAC o MATCH_MP SUBSET_TRANS) THEN
2432  MAP_EVERY EXISTS_TAC [`u:real^N`; `u + a:real^N`; `u + b:real^N`] THEN
2433  CONJ_TAC THENL
2434   [REWRITE_TAC[COLLINEAR_3; COLLINEAR_LEMMA;
2435                VECTOR_ARITH `--x = vec 0 <=> x = vec 0`;
2436                VECTOR_ARITH `u - (u + a):real^N = --a`;
2437                VECTOR_ARITH `(u + b) - (u + a):real^N = b - a`] THEN
2438    REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ;
2439      VECTOR_ARITH `b - a = c % -- a <=> (c - &1) % a + &1 % b = vec 0`] THEN
2440    ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
2441     [ASM_MESON_TAC[IN_INSERT; INDEPENDENT_NONZERO]; ALL_TAC] THEN
2442    DISCH_THEN(X_CHOOSE_TAC `u:real`) THEN
2443    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [independent]) THEN
2444    REWRITE_TAC[DEPENDENT_EXPLICIT] THEN
2445    MAP_EVERY EXISTS_TAC [`{a:real^N,b}`;
2446                          `\x:real^N. if x = a then u - &1 else &1`] THEN
2447    REWRITE_TAC[FINITE_INSERT; FINITE_RULES; SUBSET_REFL] THEN
2448    CONJ_TAC THENL
2449     [EXISTS_TAC `b:real^N` THEN ASM_REWRITE_TAC[IN_INSERT] THEN
2450      REAL_ARITH_TAC;
2451      ALL_TAC] THEN
2452    SIMP_TAC[VSUM_CLAUSES; FINITE_RULES] THEN
2453    ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; VECTOR_ADD_RID];
2454    ALL_TAC] THEN
2455  W(MP_TAC o PART_MATCH (lhs o rand) AFFINE_HULL_INSERT_SPAN o rand o goal_concl) THEN
2456  ANTS_TAC THENL
2457   [REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
2458    REWRITE_TAC[VECTOR_ARITH `u = u + a <=> a = vec 0`] THEN
2459    ASM_MESON_TAC[INDEPENDENT_NONZERO; IN_INSERT];
2460    ALL_TAC] THEN
2461  DISCH_THEN SUBST1_TAC THEN
2462  FIRST_ASSUM(MP_TAC o ISPEC `\x:real^N. u + x` o MATCH_MP IMAGE_SUBSET) THEN
2463  REWRITE_TAC[GSYM IMAGE_o; o_DEF; IMAGE_ID;
2464              ONCE_REWRITE_RULE[VECTOR_ADD_SYM] VECTOR_SUB_ADD] THEN
2465  MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] SUBSET_TRANS) THEN
2466  REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN
2467  REWRITE_TAC[SIMPLE_IMAGE; IMAGE_CLAUSES; VECTOR_ADD_SUB] THEN
2468  SET_TAC[]);;
2469
2470 (* this LEMMA in determinants.ml
2471 let DET_3 = new_axiom_removed`!A:real^3^3.
2472         det(A) = A$1$1 * A$2$2 * A$3$3 +
2473                  A$1$2 * A$2$3 * A$3$1 +
2474                  A$1$3 * A$2$1 * A$3$2 -
2475                  A$1$1 * A$2$3 * A$3$2 -
2476                  A$1$2 * A$2$1 * A$3$3 -
2477                  A$1$3 * A$2$2 * A$3$1`;;
2478 *)
2479
2480 let det_vec3 = new_definition ` det_vec3 (a:real^3) (b:real^3) (c:real^3) =
2481   a$1 * b$2 * c$3 + b$1 * c$2 * a$3 + c$1 * a$2 * b$3 -
2482   ( a$1 * c$2 * b$3 + b$1 * a$2 * c$3 + c$1 * b$2 * a$3 ) `;;
2483
2484
2485 let DET_VEC3_EXPAND = prove
2486  (`det (vector [a; b; (c:real^3)] ) = det_vec3 a b c`,
2487  REWRITE_TAC[det_vec3; DET_3; VECTOR_3] THEN REAL_ARITH_TAC);;
2488
2489 let COPLANAR_DET_VEC3_EQ_0 = prove( `!v0 v1 (v2: real^3) v3.
2490        coplanar_alt {v0,v1,v2,v3} <=>
2491        det_vec3 ( v1 - v0 ) ( v2 - v0 ) ( v3 - v0 ) = &0`, REWRITE_TAC[COPLANAR_DET_EQ_0; DET_VEC3_EXPAND]);;
2492
2493
2494
2495 let COPLANAR_3 = prove
2496  (`!a b c:real^N. 2 <= dimindex(:N) ==> coplanar_alt {a,b,c}`,
2497  SIMP_TAC[COPLANAR_ALT; SUBSET] THEN MESON_TAC[HULL_INC]);;
2498
2499 let NONCOPLANAR_4_DISTINCT = prove
2500  (`!a b c d:real^N.
2501        ~(coplanar_alt{a,b,c,d}) /\ 2 <= dimindex(:N)
2502        ==> ~(a = b) /\ ~(a = c) /\ ~(a = d) /\
2503            ~(b = c) /\ ~(b = d) /\ ~(c = d)`,
2504  REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
2505  ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[DE_MORGAN_THM] THEN
2506  STRIP_TAC THEN ASM_SIMP_TAC[INSERT_AC; COPLANAR_3]);;
2507
2508
2509
2510 let NONCOPLANAR_3_BASIS = prove
2511  (`!v1 v2 v3 v0 v:real^3.
2512     ~coplanar_alt {v0, v1, v2, v3}
2513     ==> (?t1 t2 t3.
2514              v = t1 % (v1 - v0) + t2 % (v2 - v0) + t3 % (v3 - v0) /\
2515              (!ta tb tc.
2516                   v = ta % (v1 - v0) + tb % (v2 - v0) + tc % (v3 - v0)
2517                   ==> ta = t1 /\ tb = t2 /\ tc = t3))`,
2518  REPEAT STRIP_TAC THEN
2519  FIRST_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
2520    NONCOPLANAR_4_DISTINCT)) THEN
2521  REWRITE_TAC[DIMINDEX_3; ARITH] THEN STRIP_TAC THEN
2522  SUBGOAL_THEN `independent {v1 - v0:real^3,v2 - v0,v3 - v0}` ASSUME_TAC THENL
2523   [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [COPLANAR_DET_EQ_0]) THEN
2524    ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[independent] THEN
2525    DISCH_TAC THEN MATCH_MP_TAC DET_DEPENDENT_ROWS THEN
2526    REWRITE_TAC[rows; row; LAMBDA_ETA; GSYM IN_NUMSEG; DIMINDEX_3] THEN
2527    ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN
2528    CONV_TAC(ONCE_DEPTH_CONV NUMSEG_CONV) THEN
2529    ASM_REWRITE_TAC[IMAGE_CLAUSES; VECTOR_3];
2530    ALL_TAC] THEN
2531  MP_TAC(ISPECL [`(:real^3)`; `{v1 - v0:real^3,v2 - v0,v3 - v0}`]
2532    CARD_GE_DIM_INDEPENDENT) THEN
2533  ASM_REWRITE_TAC[DIM_UNIV; SUBSET_UNIV] THEN ANTS_TAC THENL
2534   [SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_RULES] THEN
2535    ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; DIMINDEX_3; ARITH;
2536                    VECTOR_ARITH `x - a:real^N = y - a <=> x = y`];
2537    ALL_TAC] THEN
2538  REWRITE_TAC[SUBSET; IN_UNIV; SPAN_BREAKDOWN_EQ; SPAN_EMPTY] THEN
2539  DISCH_THEN(MP_TAC o SPEC `v:real^3`) THEN
2540  MAP_EVERY (fun t -> MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC t)
2541            [`t1:real`; `t2:real`; `t3:real`] THEN
2542  REWRITE_TAC[IN_SING; VECTOR_ARITH
2543    `a - b - c - d:real^N = vec 0 <=> a = b + c + d`] THEN
2544  DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[] THEN
2545  MAP_EVERY X_GEN_TAC [`ta:real`; `tb:real`; `tc:real`] THEN
2546  REWRITE_TAC[VECTOR_ARITH
2547   `t1 % x + t2 % y + t3 % z = ta % x + tb % y + tc % z <=>
2548    (t1 - ta) % x + (t2 - tb) % y + (t3 - tc) % z = vec 0`] THEN
2549  STRIP_TAC THEN FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [independent]) THEN
2550  REWRITE_TAC[DEPENDENT_EXPLICIT; NOT_EXISTS_THM] THEN
2551  DISCH_THEN(MP_TAC o SPECL
2552   [`{v1 - v0:real^3,v2 - v0,v3 - v0}`;
2553    `\v:real^3. if v = v1 - v0 then t1 - ta
2554                else if v = v2 - v0 then t2 - tb
2555                else t3 - tc`]) THEN
2556  SIMP_TAC[FINITE_INSERT; FINITE_RULES; SUBSET_REFL; VSUM_CLAUSES] THEN
2557  ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; VECTOR_ADD_RID;
2558                  RIGHT_OR_DISTRIB; EXISTS_OR_THM; UNWIND_THM2;
2559                    VECTOR_ARITH `x - a:real^N = y - a <=> x = y`] THEN
2560  SIMP_TAC[DE_MORGAN_THM; REAL_SUB_0]);;
2561
2562
2563
2564 let DET_VEC3_AND_DELTA = prove(`!(a:real^3) b c d.
2565      &4 * ( det_vec3 (a - d) (b - d) (c - d) ) pow 2 =
2566      delta  ( dist3 a d pow 2)
2567      (dist3 b d pow 2)
2568      (dist3 c d pow 2) (dist3 a b pow 2) (dist3 a c pow 2) (dist3 b c pow 2)   `,
2569 SIMP_TAC[dist3; dist] THEN
2570 REWRITE_TAC[GSYM (MESON[VECTOR_ARITH ` (a :real^N) - b = ( a - x ) - ( b - x ) `]`
2571   delta      (norm (a - d) pow 2)     (norm (b - d) pow 2)
2572      (norm (c - d) pow 2) (norm ((a - d)  - (b - d )) pow 2)
2573 (norm ((a - d)  - ( c - d )) pow 2) (norm ((b - d ) - ( c - d )) pow 2)    =
2574    delta   (norm (a - d) pow 2)     (norm (b - d) pow 2)   (norm (c - d) pow 2)
2575 (norm (a - b) pow 2) (norm (a - c) pow 2) (norm (b - c) pow 2)    `)] THEN
2576 SIMP_TAC[ vector_norm; DOT_POS_LE; SQRT_WORKS] THEN
2577 REWRITE_TAC[DOT_3] THEN
2578 REWRITE_TAC[MESON[lemma_cm3]`((a:real^3) - d - (b - d))$1 = (a - d)$1 - (b - d)$1 /\
2579   (a - d - (b - d))$2 = (a - d)$2 - (b - d)$2 /\
2580   (a - d - (b - d))$3 = (a - d)$3 - (b - d)$3 `] THEN
2581 REWRITE_TAC[delta; det_vec3] THEN
2582 REAL_ARITH_TAC);;
2583
2584
2585
2586 let POLFLZY = prove(` !(x1:real^3) x2 x3 x4.
2587          let x12 = dist (x1,x2) pow 2 in
2588          let x13 = dist (x1,x3) pow 2 in
2589          let x14 = dist (x1,x4) pow 2 in
2590          let x23 = dist (x2,x3) pow 2 in
2591          let x24 = dist (x2,x4) pow 2 in
2592          let x34 = dist (x3,x4) pow 2 in
2593          coplanar_alt {x1, x2, x3, x4} <=> delta x12 x13 x14 x23 x24 x34 = &0 `,
2594 LET_TR THEN REPEAT GEN_TAC THEN MP_TAC (GSYM (SPECL [` x2 :real^3`;
2595 ` x3:real^3`;` x4:real^3`; ` x1 :real^3`] DET_VEC3_AND_DELTA)) THEN
2596 SIMP_TAC[dist3; DIST_SYM] THEN REWRITE_TAC[REAL_ARITH ` &4 * a = &0 <=> a = &0 `]
2597 THEN SIMP_TAC[GSYM ( REAL_FIELD ` x = &0 <=> x pow 2 = &0 `);
2598 COPLANAR_DET_VEC3_EQ_0]);;
2599
2600
2601 let LEMMA15 = POLFLZY;;
2602
2603 let muy_delta = new_definition ` muy_delta = delta `;;
2604
2605
2606 (* LEMMA29 *)
2607 (*
2608 let VCRJIHC = prove(`!(v1:real^3) v2 v3 v4 x34 x12 x13 x14 x23 x24.
2609          condA v1 v2 v3 v4 x12 x13 x14 x23 x24 x34
2610          ==> muy_delta x12 x13 x14 x23 x24 (dist (v3,v4) pow 2) = &0`,
2611 REWRITE_TAC[condA; muy_delta] THEN MP_TAC POLFLZY THEN LET_TR THEN MESON_TAC[]);;
2612 *)
2613
2614 let ZERO_NEUTRAL = REAL_ARITH ` ! x. &0 * x = &0 /\ x * &0 = &0 /\ &0 + x = x /\ x + &0 = x /\ x - &0 = x /\
2615   -- &0 = &0 `;;
2616
2617 let EQUATE_CONEFS_POLINOMIAL_POW2 = prove( `!a b c aa bb cc. ( ! x.
2618      a * x pow 2 + b * x + c = aa * x pow 2 + bb * x + cc ) <=>
2619      a = aa /\ b = bb /\ c = cc`, REPEAT GEN_TAC THEN EQ_TAC THENL [
2620 NHANH (MESON[]` (! (x:real). P x ) ==> P ( &0 ) /\ P ( &1 ) /\ P ( -- &1 )`) THEN
2621 REAL_ARITH_TAC THEN REAL_ARITH_TAC; SIMP_TAC[]]);;
2622
2623 let GJWYYPS = prove(`!x12 x13 x14 x15 x23 x24 x25 x34 x35 a b c.
2624     (! x45.  cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 =
2625      a  * x45 pow 2 + b * x45 + c )
2626      ==> b pow 2 - &4 * a * c =
2627          &16 * delta x12 x13 x14 x23 x24 x34 * delta x12 x13 x15 x23 x25 x35`,
2628 ONCE_REWRITE_TAC[LTCTBAN] THEN REPEAT GEN_TAC THEN
2629 REWRITE_TAC[EQUATE_CONEFS_POLINOMIAL_POW2] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]
2630 THEN SIMP_TAC[] THEN DISCH_TAC THEN REWRITE_TAC[ups_x; cayleytr; cayleyR;
2631  delta; ZERO_NEUTRAL] THEN REAL_ARITH_TAC);;
2632
2633 let LEMMA51 = GJWYYPS ;;
2634
2635 let NOT_TOW_EQ_IMP_COL_EQUAVALENT = prove_by_refinement(
2636 `!v1 v2 (v:real^3). ~(v1 = v2) ==> (collinear {v, v1, v2} <=> v IN aff {v1, v2})`,
2637   (* {{{ proof *)
2638   [
2639   (REWRITE_TAC[COLLINEAR_EX]);
2640   (NHANH (MESON[]` a % b + c = vec 0 ==> ( a = &0 \/ ~(a = &0 ))`));
2641   (KHANANG);
2642   (NGOAC THEN PURE_ONCE_REWRITE_TAC[MESON[]` P a /\ a = &0 <=> P ( &0 )   /\ a = &0 `]);
2643   (REWRITE_TAC[REAL_ADD_LID; VECTOR_MUL_LZERO; VECTOR_ADD_LID]);
2644   (REWRITE_TAC[REAL_ARITH ` a + b= &0 <=> a = -- b `; VECTOR_ARITH` a % x + b % y = vec 0  <=> a % x = ( -- b) % y`]);
2645   (NHANH (MESON[REAL_ARITH ` a = &0 <=> -- a = &0 `; VECTOR_MUL_LCANCEL]` (b = --c /\ ~(b = &0 /\ c = &0)) /\ b % v1 = --c % v2  ==> v1 = v2 `));
2646   (SIMP_TAC[]);
2647   (REWRITE_TAC[AFF_2POINTS_INTERPRET; IN_ELIM_THM]);
2648   (REPEAT GEN_TAC THEN DISCH_TAC THEN EQ_TAC);
2649     (REWRITE_TAC[VECTOR_ARITH ` a % v + b % v1 + c % v2 = vec 0 <=>  a % v = ( -- b) % v1 + ( --c ) % v2 `]);
2650     (PHA THEN REWRITE_TAC[MESON[CHANGE_SIDE]` a % v = v1  /\               ~(a = &0) <=> v = &1 / a % v1 /\ ~( a = &0 ) `]);
2651     (REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; REAL_ARITH `&1 / a * b = b / a`]);
2652      (REWRITE_TAC[AFF_2POINTS_INTERPRET; IN_ELIM_THM]);
2653     BY( (MESON_TAC[REAL_FIELD ` ~ ( a = &0 ) /\ a = -- (b + c) ==>   ( -- b) / a + ( -- c) / a = &1 `]));
2654    (STRIP_TAC);
2655    (EXISTS_TAC ` &1 `);
2656    (EXISTS_TAC ` -- ta`);
2657    (EXISTS_TAC ` -- tb`);
2658    (PHA);
2659    (ASM_SIMP_TAC[REAL_ARITH` ~(&1 = &0 ) /\ -- ( -- a + -- b ) = a + b `]);
2660   BY( (CONV_TAC VECTOR_ARITH))
2661   ]);;
2662   (* }}} *)
2663
2664
2665 (*
2666 let LEMMA30 = prove(`!v1 v2 v3 v4 x12 x13 x14 x23 x24 x34 a b c.
2667          condA v1 v2 v3 v4 x12 x13 x14 x23 x24 x34 /\
2668          (!x12 x13 x14 x23 x24 x34.
2669               muy_delta x12 x13 x14 x23 x24 x34 =
2670               a x12 x13 x14 x23 x24 * x34 pow 2 +
2671               b x12 x13 x14 x23 x24 * x34 +
2672               c x12 x13 x14 x23 x24 )
2673          ==> (v3 IN aff {v1, v2} \/ v4 IN aff {v1, v2} <=>
2674               b x12 x13 x14 x23 x24 pow 2 -
2675               &4 * a x12 x13 x14 x23 x24 * c x12 x13 x14 x23 x24 =
2676               &0)`,
2677 REWRITE_TAC[muy_delta; DELTA_COEFS; EQUATE_CONEFS_POLINOMIAL_POW2 ] THEN
2678 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN SIMP_TAC[] THEN REPEAT GEN_TAC THEN
2679 DISCH_TAC THEN REWRITE_TAC[REAL_ARITH` a - b * -- c * d = a + b * c * d `;
2680 AGBWHRD] THEN DOWN_TAC THEN SIMP_TAC[condA; REAL_ENTIRE;
2681 GSYM NOT_TOW_EQ_IMP_COL_EQUAVALENT] THEN ONCE_REWRITE_TAC[MESON[PER_SET3]`
2682  p {v3, v1, v2} \/ p {v4, v1, v2}  <=> p {v1,v2,v3} \/ p {v1,v2,v4} `] THEN
2683 ONCE_REWRITE_TAC[MESON[UPS_X_SYM]` ups_x x12 x23 x13 = &0 \/
2684 ups_x x12 x24 x14 = &0 <=>     ups_x x12 x13 x23 = &0 \/
2685 ups_x x12 x14 x24 = &0 `] THEN MESON_TAC[UPS_X_SYM; PER_SET3; FHFMKIY]);;
2686 *)
2687
2688 (* let EWVIFXW = LEMMA30;; *)
2689
2690
2691 let LEMMA51 = GJWYYPS;;
2692 let LEMMA50 = LTCTBAN;;
2693 let muy_v = new_definition ` muy_v (x1: real^N ) (x2:real^N) (x3:real^N) (x4:real^N)
2694 (x5:real^N) x45 =
2695           (let x12 = dist (x1,x2) pow 2 in
2696           let x13 = dist (x1,x3) pow 2 in
2697           let x14 = dist (x1,x4) pow 2 in
2698           let x15 = dist (x1,x5) pow 2 in
2699           let x23 = dist (x2,x3) pow 2 in
2700           let x24 = dist (x2,x4) pow 2 in
2701           let x25 = dist (x2,x5) pow 2 in
2702           let x34 = dist (x3,x4) pow 2 in
2703           let x35 = dist (x3,x5) pow 2 in
2704           cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45) `;;
2705
2706 let REMOVE_TAC = MATCH_MP_TAC (MESON[]` a ==> b ==> a `);;
2707
2708 let ALE = MESON[LTCTBAN]`!x12 x13 x14 x15 x23 x24 x25 x34 x35.
2709      (!a b c. (! x.
2710           cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x =
2711           a * x pow 2 + b * x + c )
2712           ==> b pow 2 - &4 * a * c = &0)
2713      ==> cayleytr x12 x13 x14 x15 x23 x24 x25 x34 x35 (&0) pow 2 -
2714          &4 *
2715          ups_x x12 x13 x23 *
2716          cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 (&0) =
2717          &0`;;
2718
2719 let DISCRIMINANT_OF_CAY = MESON[LTCTBAN; GJWYYPS]`cayleytr x12 x13 x14 x15 x23 x24 x25 x34 x35 (&0) pow 2 -
2720  &4 * ups_x x12 x13 x23 * cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 (&0) =
2721  &16 * delta x12 x13 x14 x23 x24 x34 * delta x12 x13 x15 x23 x25 x35`;;
2722
2723 let NOT_TWO_EQ_IMP_COL_EQUAVALENT = NOT_TOW_EQ_IMP_COL_EQUAVALENT;;
2724
2725 let GDLRUZB = prove(` ! (v1:real^3) (v2:real^3) (v3:real^3) (v4:real^3) (v5:real^3) a b c.
2726   coplanar_alt {v1, v2, v3, v4} \/ coplanar_alt {v1, v2, v3, v5} <=>
2727          (! a b c. (! x. muy_v v1 v2 v3 v4 v5 x = a * x pow 2 + b * x + c )
2728  ==> b pow 2 - &4 * a * c = &0) `,REWRITE_TAC[muy_v] THEN LET_TR THEN
2729 REPEAT GEN_TAC THEN EQ_TAC THENL [DISCH_TAC THEN
2730 NHANH (MESON[GJWYYPS]` (!x45. cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 =
2731                 a * x45 pow 2 + b * x45 + c)
2732          ==> b pow 2 - &4 * a * c =
2733              &16 *
2734              delta x12 x13 x14 x23 x24 x34 *
2735              delta x12 x13 x15 x23 x25 x35`) THEN SIMP_TAC[] THEN
2736 UNDISCH_TAC ` coplanar_alt {(v1:real^3), v2, v3, v4}\/ coplanar_alt {v1, v2, v3, v5}` THEN
2737 MP_TAC LEMMA15 THEN LET_TR THEN REWRITE_TAC[REAL_FIELD` &16 * a * b = &0
2738 <=> a = &0 \/ b = &0 `] THEN SIMP_TAC[]; NHANH (SPEC_ALL ALE) THEN
2739 REWRITE_TAC[DISCRIMINANT_OF_CAY ] THEN MP_TAC POLFLZY THEN LET_TR THEN
2740 REWRITE_TAC[REAL_FIELD` &16 * a * b = &0 <=> a = &0 \/ b = &0 `] THEN
2741 MESON_TAC[]]);;
2742
2743
2744 let DET_VECC3_AND_DELTA = prove(` (! d a b c .
2745       delta (dist3 d a pow 2) (dist3 d b pow 2) (dist3 d c pow 2) (dist3 a b pow 2)
2746       (dist3 a c pow 2)
2747       (dist3 b c pow 2) =
2748       &4 * det_vec3 (a - d) (b - d) (c - d) pow 2) `, MESON_TAC[D3_SYM;
2749 DET_VEC3_AND_DELTA]);;
2750
2751
2752 let DELTA_POS_4POINTS = prove(`!x1 x2 x3 (x4:real^3).
2753      &0 <=
2754      delta (dist (x1,x2) pow 2) (dist (x1,x3) pow 2) (dist (x1,x4) pow 2)
2755      (dist (x2,x3) pow 2)
2756      (dist (x2,x4) pow 2)
2757      (dist (x3,x4) pow 2)`, REWRITE_TAC[GSYM dist3] THEN SIMP_TAC[D3_SYM] THEN
2758 MP_TAC (DET_VECC3_AND_DELTA) THEN SIMP_TAC[] THEN DISCH_TAC THEN MP_TAC
2759  REAL_LE_SQUARE_POW THEN MESON_TAC[REAL_ARITH` &0 <= x <=> &0 <= &4 * x `]);;
2760
2761
2762
2763 let DIST_POW2_DOT =
2764 prove(` ! a (b:real^N) . dist (a,b) pow 2 = ( a - b ) dot ( a- b) `,
2765 SIMP_TAC[dist; vector_norm; DOT_POS_LE; SQRT_WORKS]);;
2766
2767 let UPS_X_POS = MESON[lemma8; UPS_X_SYM; NORM_SUB]` &0 <=
2768           ups_x (norm ((x1 : real^3) - x2) pow 2) (norm (x1 - x3) pow 2)
2769           (norm (x2 - x3) pow 2) `;;
2770
2771 let UPS_X_SYM = MESON[UPS_X_SYM]` !x y z. ups_x x y z = ups_x y x z /\ ups_x x y z = ups_x x z y
2772   /\ ups_x x y z = ups_x x z y `;;
2773
2774
2775 end;;