text_formalization/trigonometry/euler_complement.hl

   1
   2 (* ========================================================================= *)
   3 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   4 (*          COMPLEMENT LEMMAS FOR EULER TRIANGLE LEMMA                       *)
   5 (*                                                                           *)
   6 (*                  LEMMA ABOUT RESCALING                                    *)
   7 (*                                                                           *)
   8 (*      Authour : VU KHAC KY                                                 *)
   9 (*                                                                           *)
  10 (* ========================================================================= *)
  11
  12
  13 flyspeck_needs "trigonometry/delta_x.hl";;
  14
  15 (* ========================================================================= *)
  16 (*                     SOME USEFUL TACTICS                                   *)
  17 (* ========================================================================= *)
  18 module Euler_complement = struct
  19
  20 open Sphere;;
  21 open Trigonometry1;;
  22 open Trigonometry2;;
  23 open Prove_by_refinement;;
  24 open Delta_x;;
  25
  26 let UP_ASM_TAC = FIRST_X_ASSUM MP_TAC;;
  27
  28 let DEL_TAC = FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC (MESON[] `a ==> b ==> a`);;
  29
  30 let SWITCH_TAC =
  31    FIRST_X_ASSUM MP_TAC THEN
  32    FIRST_X_ASSUM MP_TAC THEN
  33    MATCH_MP_TAC (MESON[] `(a ==> b ==> c) ==> (b ==> a ==> c)`) THEN
  34    DISCH_TAC THEN
  35    DISCH_TAC;;
  36
  37 (* ========================================================================= *)
  38 (*                  THE FIRST LEMMA                                          *)
  39 (* ========================================================================= *)
  40
  41 let euler_after_rescale_t =
  42    `!v0:real^3 v1 v2 v3.
  43        norm (v1 - v0) = &1
  44        ==> norm (v2 - v0) = &1
  45        ==> norm (v3 - v0) = &1
  46        ==> &2 *
  47              (&1 +
  48              (v2 - v0) dot (v3 - v0) +
  49              (v3 - v0) dot (v1 - v0) +
  50              (v1 - v0) dot (v2 - v0)) =
  51             &8 -
  52             (v2 - v3) dot (v2 - v3) -
  53             (v1 - v3) dot (v1 - v3) -
  54             (v1 - v2) dot (v1 - v2)`;;
  55
  56 let LEMMA_FOR_EULER_AFTER_RESCALE = prove_by_refinement (euler_after_rescale_t,
  57
  58 [(REPEAT GEN_TAC THEN REPEAT DISCH_TAC);
  59 (ABBREV_TAC `a = v1:real^3 - v0`);
  60 (ABBREV_TAC `b = v2:real^3 - v0`);
  61 (ABBREV_TAC `c = v3:real^3 - v0`);
  62
  63   (ONCE_REWRITE_TAC[VECTOR_ARITH `x:real^3 - y = (x - v0) - (y - v0)`]);
  64   (PURE_ONCE_ASM_REWRITE_TAC[]);
  65   (DEL_TAC THEN DEL_TAC THEN DEL_TAC);
  66   (REWRITE_TAC[VECTOR_ARITH
  67     `(x:real^3 - y) dot (x - y) = x dot x + y dot y - &2 * x dot y`]) ;
  68
  69   (PURE_ONCE_REWRITE_TAC[GSYM NORM_POW_2]);
  70   (PURE_ONCE_ASM_REWRITE_TAC[]);
  71   (PURE_ONCE_REWRITE_TAC[REAL_ARITH `&1 pow 2 = &1`]);
  72   (PURE_REWRITE_TAC[DOT_SYM]);
  73   REAL_ARITH_TAC]);;
  74
  75 (*========================================================================= *)
  76 (*                                                                          *)
  77 (*             THE SECOND LEMMA : DIHV UNCHANGED                            *)
  78 (*                                                                          *)
  79 (* =========================================================================*)
  80
  81 let dihv_rescale_unchanged_t =
  82
  83 `!v0 v1 v2 v3 w0 w1:real^3 w2 w3 m n p.
  84      v1 - v0 = m % (w1 - w0) /\
  85      v2 - v0 = n % (w2 - w0) /\
  86      v3 - v0 = p % (w3 - w0) /\
  87      &0 < m /\
  88      &0 < n /\
  89      &0 < p
  90      ==> dihV v0 v1 v2 v3 = dihV w0 w1 w2 w3`;;
  91
  92 let DIHV_RESCALE_UNCHANGED = prove_by_refinement (dihv_rescale_unchanged_t ,
  93
  94 [(REPEAT GEN_TAC THEN REPEAT STRIP_TAC);
  95 (REWRITE_TAC[dihV] THEN REPEAT LET_TAC);
  96 (REWRITE_TAC[arcV]);
  97 (AP_TERM_TAC);
  98 (REWRITE_TAC[VECTOR_SUB_RZERO]);
  99
 100   (* Begin subgoal 1 *)
 101
 102   (SUBGOAL_THEN `vap':real^3 = (m * m * n) % vap` ASSUME_TAC);
 103   (EXPAND_TAC "vap'" THEN EXPAND_TAC "vap");
 104   (PURE_ONCE_REWRITE_TAC[ASSUME `(vc':real^3) = m % vc`]);
 105   (PURE_ONCE_REWRITE_TAC[ASSUME `(va':real^3) = n % va`]);
 106   (PURE_REWRITE_TAC[DOT_LMUL;DOT_RMUL]);
 107   (REWRITE_TAC[VECTOR_SUB_LDISTRIB;VECTOR_MUL_ASSOC]);
 108   (REWRITE_TAC[REAL_ARITH `(a * b * c) * d = (a * b * d) * c`]);
 109   (AP_TERM_TAC);
 110   (AP_THM_TAC THEN AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC);
 111   REAL_ARITH_TAC;
 112   (* End subgoal 1 *)
 113
 114   (* Begin subgoal 2 *)
 115
 116   (SUBGOAL_THEN `vbp':real^3 = (m * m * p)  % vbp` ASSUME_TAC);
 117   (EXPAND_TAC "vbp'" THEN EXPAND_TAC "vbp");
 118   (PURE_ONCE_REWRITE_TAC[ASSUME `(vc':real^3) = m % vc`]);
 119   (PURE_ONCE_REWRITE_TAC[ASSUME `(vb':real^3) = p % vb`]);
 120   (PURE_REWRITE_TAC[DOT_LMUL;DOT_RMUL]);
 121   (REWRITE_TAC[VECTOR_SUB_LDISTRIB;VECTOR_MUL_ASSOC]);
 122   (REWRITE_TAC[REAL_ARITH `(a * b * c) * d = (a * b * d) * c`]);
 123   (AP_TERM_TAC);
 124   (AP_THM_TAC THEN AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC);
 125   REAL_ARITH_TAC;
 126   (* End subgoal 2 *)
 127
 128 (PURE_ONCE_ASM_REWRITE_TAC[]);
 129 (PURE_REWRITE_TAC[DOT_LMUL;DOT_RMUL]);
 130 (PURE_REWRITE_TAC[NORM_MUL]);
 131 (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(a * b) * c * d = (a * c) * b * d`]);
 132 (PURE_REWRITE_TAC[REAL_ABS_MUL]);
 133
 134
 135   (SUBGOAL_THEN `&0 <= m /\ &0 <= n /\ &0 <= p` ASSUME_TAC);
 136   ASM_REAL_ARITH_TAC;
 137
 138   (SUBGOAL_THEN `abs m = m /\ abs n = n /\ abs p = p` ASSUME_TAC);
 139   (UP_ASM_TAC THEN MESON_TAC[GSYM REAL_ABS_REFL]);
 140
 141 (UP_ASM_TAC THEN STRIP_TAC);
 142 (PURE_ONCE_ASM_REWRITE_TAC[]);
 143 (PURE_ONCE_REWRITE_TAC[REAL_MUL_ASSOC]);
 144 (PURE_ONCE_REWRITE_TAC[REAL_ARITH
 145    `(m * m * m * p) * m * n = (m * m * n) * m * m * p`]);
 146 (ABBREV_TAC `s = (m * m * n) * m * m * p`);
 147 (PURE_ONCE_REWRITE_TAC[GSYM REAL_MUL_ASSOC]);
 148 (PURE_REWRITE_TAC[real_div;REAL_INV_MUL]);
 149 (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(a * b * c) = (c * b) * a`]);
 150 (REWRITE_TAC[REAL_ARITH `((a * b) * c) * d * e = (((c * d) * b) * a) * e`]);
 151 (AP_THM_TAC THEN AP_TERM_TAC);
 152 (AP_THM_TAC THEN AP_TERM_TAC);
 153
 154 (PURE_ONCE_REWRITE_TAC[GSYM REAL_MUL_LID]);
 155 (ONCE_REWRITE_TAC[REAL_ARITH `&1 * x * y = x * y`]);
 156 (AP_THM_TAC THEN AP_TERM_TAC);
 157 (MATCH_MP_TAC REAL_MUL_LINV);
 158 (EXPAND_TAC "s");
 159 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
 160 (ASM_MESON_TAC[REAL_LT_MUL])]);;
 161
 162 (*===========================================================================*)
 163 (*    THE THIRD LEMMA :                                                      *)
 164 (*               The lemmas help to compute p after rescaling                *)
 165 (*                          (in general)                                     *)
 166 (*                                                                           *)
 167 (*===========================================================================*)
 168
 169 let compute_euler_p_after_rescale_t =
 170 `!v0:real^3 v1 v2 v3 v0' v1' v2' v3' m n p.
 171      v1 - v0 = m % (v1' - v0') /\
 172      v2 - v0 = n % (v2' - v0') /\
 173      v3 - v0 = p % (v3' - v0') /\
 174      &0 < m /\
 175      &0 < n /\
 176      &0 < p
 177      ==> euler_p v0 v1 v2 v3 = (m * n * p) * euler_p v0' v1' v2' v3'`;;
 178
 179
 180 let COMPUTE_EULER_P_AFTER_RESCALE =
 181  prove_by_refinement (compute_euler_p_after_rescale_t,
 182
 183 [(REPEAT GEN_TAC THEN STRIP_TAC);
 184 (REWRITE_TAC[euler_p]);
 185 (PURE_ONCE_REWRITE_TAC[ylist]);
 186 (REPEAT LET_TAC);
 187 (REPLICATE_TAC 8 UP_ASM_TAC);
 188 (PURE_REWRITE_TAC[PAIR_EQ]);
 189 (PURE_ONCE_REWRITE_TAC[DIST_SYM]);
 190 (PURE_REWRITE_TAC[dist]);
 191 (REPEAT STRIP_TAC);
 192 (ASM_REWRITE_TAC[]);
 193 (EXPAND_TAC "y1'" THEN EXPAND_TAC "y2'" THEN EXPAND_TAC "y3'");
 194 (EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");
 195 (REPLICATE_TAC 3 UP_ASM_TAC);
 196 (REPLICATE_TAC 6 DEL_TAC);
 197 (REPLICATE_TAC 3 UP_ASM_TAC);
 198 (REPLICATE_TAC 6 DEL_TAC);
 199 (REPEAT STRIP_TAC);
 200
 201 (PURE_ONCE_ASM_REWRITE_TAC[]);
 202 (REPLICATE_TAC 6 DEL_TAC);
 203 (PURE_ONCE_ASM_REWRITE_TAC[]);
 204 (PURE_ONCE_REWRITE_TAC[NORM_MUL]);
 205
 206
 207   (SUBGOAL_THEN `&0 <= m /\ &0 <= n /\ &0 <= p` ASSUME_TAC);
 208   (ASM_MESON_TAC[REAL_ARITH `&0 < a ==> &0 <= a`]);
 209   (SUBGOAL_THEN `abs m = m /\ abs n = n /\ abs p = p` ASSUME_TAC);
 210   (UP_ASM_TAC THEN MESON_TAC[REAL_ABS_REFL]);
 211
 212 (PURE_ONCE_ASM_REWRITE_TAC[]);
 213 (PURE_REWRITE_TAC[DOT_RMUL;DOT_LMUL]);
 214 REAL_ARITH_TAC]);;
 215
 216 (* ========================================================================= *)
 217 (*       THE 4-TH LEMMA                                                      *)
 218 (*                  This lemma is for computing delta_x                      *)
 219 (*                                                                           *)
 220 (* ========================================================================= *)
 221
 222 let VECTOR_EQ_COMPONENT = prove
 223  (`!x:real^N y i. x = y ==> x$i = y$i`,
 224   REPEAT GEN_TAC THEN
 225   SUBGOAL_THEN `?k. 1 <= k /\ k <= dimindex(:N) /\ !z:real^N. z$i = z$k`
 226   CHOOSE_TAC THENL
 227    [REWRITE_TAC[FINITE_INDEX_INRANGE];
 228     ASM_SIMP_TAC[vector_sub; CART_EQ; LAMBDA_BETA]]);;
 229
 230 let compute_delta_x_after_rescale_t =
 231  `!v0 v1 v2 v3 v0' v1' v2' v3' m n p x1 x2 x3 x4 x5 x6 x1' x2' x3' x4' x5' x6'.
 232      v1:real^3 - v0 = m % (v1' - v0') /\
 233       v2 - v0 = n % (v2' - v0') /\
 234       v3 - v0 = p % (v3' - v0') /\
 235       &0 <= m /\
 236       &0 <= n /\
 237       &0 <= p /\
 238       x1',x2',x3',x4',x5',x6' = xlist v0' v1' v2' v3' /\
 239       x1,x2,x3,x4,x5,x6 = xlist v0 v1 v2 v3 /\
 240       &0 <= delta_x x1' x2' x3' x4' x5' x6'
 241       ==> delta_x x1 x2 x3 x4 x5 x6 =
 242          (m * n * p) * (m * n * p) * delta_x x1' x2' x3' x4' x5' x6'`;;
 243
 244
 245 let COMPUTE_DELTA_X_AFTER_RESCALE =
 246
 247 prove_by_refinement (compute_delta_x_after_rescale_t ,
 248
 249 [(REPEAT GEN_TAC THEN REPEAT STRIP_TAC);
 250
 251   (SUBGOAL_THEN `delta_x x1 x2 x3 x4 x5 x6 =
 252              (let a = v1:real^3 - v0 in
 253               let b = v2 - v0 in
 254               let c = v3 - v0 in
 255               &4 * (a$1 * b$2 * c$3 - a$1 * b$3 * c$2 - a$2 * b$1 * c$3 +
 256                a$2 * b$3 * c$1 + a$3 * b$1 * c$2 - a$3 * b$2 * c$1) pow 2)`
 257     ASSUME_TAC);
 258   (ASM_MESON_TAC[COMPUTE_DELTA_X]);
 259
 260   (SUBGOAL_THEN `delta_x x1' x2' x3' x4' x5' x6' =
 261              (let a' = v1':real^3 - v0' in
 262               let b' = v2' - v0' in
 263               let c' = v3' - v0' in
 264           &4 * (a'$1 * b'$2 * c'$3 - a'$1 * b'$3 * c'$2 - a'$2 * b'$1 * c'$3 +
 265           a'$2 * b'$3 * c'$1 + a'$3 * b'$1 * c'$2 - a'$3 * b'$2 * c'$1) pow 2)`
 266      ASSUME_TAC);
 267   (ASM_MESON_TAC[COMPUTE_DELTA_X]);
 268
 269 (ASM_REWRITE_TAC[]);
 270 (REPEAT LET_TAC);
 271
 272   (SUBGOAL_THEN `(a:real^3)$1 = m * (a':real^3)$1 /\
 273                    (b:real^3)$1 = n * (b':real^3)$1 /\
 274                    (c:real^3)$1 = p * (c':real^3)$1 /\
 275                    a$2 = m * a'$2 /\
 276                    a$3 = m * a'$3 /\
 277                    b$2 = n * b'$2 /\
 278                    b$3 = n * b'$3 /\
 279                    c$2 = p * c'$2 /\
 280                    c$3 = p * c'$3` ASSUME_TAC);
 281
 282   (ASM_MESON_TAC[VECTOR_EQ_COMPONENT;VECTOR_MUL_COMPONENT]);
 283 (ONCE_ASM_REWRITE_TAC[]);
 284 (REWRITE_TAC[POW_2]);
 285 REAL_ARITH_TAC]);;
 286
 287 (* =========================================================================*)
 288 (*     THE 5-TH LEMMA :                                                     *)
 289 (*             Similar lemma for computing Sqrt(delta_x)                    *)
 290 (*==========================================================================*)
 291
 292 let sqrt_delta_x_after_rescale =
 293 `!v0 v1 v2 v3 v0' v1' v2' v3' m n p x1 x2 x3 x4 x5 x6 x1' x2' x3' x4' x5' x6'.
 294      v1:real^3 - v0 = m % (v1' - v0') /\
 295       v2 - v0 = n % (v2' - v0') /\
 296       v3 - v0 = p % (v3' - v0') /\
 297       &0 <= m /\
 298       &0 <= n /\
 299       &0 <= p /\
 300       x1',x2',x3',x4',x5',x6' = xlist v0' v1' v2' v3' /\
 301       x1,x2,x3,x4,x5,x6 = xlist v0 v1 v2 v3 /\
 302       &0 <= delta_x x1' x2' x3' x4' x5' x6'
 303      ==> sqrt (delta_x x1 x2 x3 x4 x5 x6) =
 304          (m * n * p) * sqrt (delta_x x1' x2' x3' x4' x5' x6')`;;
 305
 306 let SQRT_DELTA_X_AFTER_RESCALE  =
 307 prove_by_refinement (sqrt_delta_x_after_rescale,
 308
 309 [(REPEAT GEN_TAC THEN REPEAT STRIP_TAC);
 310
 311   (SUBGOAL_THEN
 312      `delta_x x1 x2 x3 x4 x5 x6 =
 313          (m * n * p) * (m * n * p) * delta_x x1' x2' x3' x4' x5' x6'`
 314      ASSUME_TAC);
 315   (ASM_MESON_TAC[COMPUTE_DELTA_X_AFTER_RESCALE]);
 316
 317 (PURE_ONCE_ASM_REWRITE_TAC[]);
 318 (ABBREV_TAC `S = m * n * p`);
 319 (PURE_REWRITE_TAC[REAL_MUL_ASSOC]);
 320
 321   (SUBGOAL_THEN
 322     `sqrt ((S * S) * delta_x x1' x2' x3' x4' x5' x6') =
 323      sqrt (S * S) * sqrt (delta_x x1' x2' x3' x4' x5' x6')`
 324      ASSUME_TAC);
 325   (MATCH_MP_TAC SQRT_MUL);
 326   (EXPAND_TAC "S");
 327   (ASM_MESON_TAC[REAL_LE_MUL]);
 328
 329 (PURE_ONCE_ASM_REWRITE_TAC[]);
 330 (AP_THM_TAC THEN AP_TERM_TAC);
 331
 332   (SUBGOAL_THEN `sqrt (S * S) = sqrt S pow 2` ASSUME_TAC);
 333   (REWRITE_TAC[REAL_POW_2]);
 334   (MATCH_MP_TAC SQRT_MUL);
 335   (EXPAND_TAC "S");
 336   (ASM_MESON_TAC[REAL_LE_MUL]);
 337
 338 (PURE_ONCE_ASM_REWRITE_TAC[]);
 339 (MATCH_MP_TAC SQRT_POW_2);
 340 (EXPAND_TAC "S");
 341 (ASM_MESON_TAC[REAL_LE_MUL])]);;
 342
 343
 344 (* ===========================================================================*)
 345 (*    THE SIXTH LEMMA :                                                       *)
 346 (*                                                                            *)
 347 (*    This following sub-lemma is necessary for proving the 6-th Lemma        *)
 348 (*                                                                            *)
 349 (* ===========================================================================*)
 350
 351 let SQRT_OF_POW_2_LE = prove_by_refinement (
 352  `!x. (&0 <= x) ==> sqrt (x pow 2) = x`,
 353
 354 [(GEN_TAC THEN DISCH_TAC);
 355  (REWRITE_TAC[REAL_POW_2]);
 356    (SUBGOAL_THEN `sqrt (x * x) = (sqrt x) pow 2` ASSUME_TAC);   (PURE_REWRITE_TAC[REAL_POW_2]);
 357    (MATCH_MP_TAC SQRT_MUL);
 358    (ASM_REWRITE_TAC[]);
 359  (PURE_ASM_REWRITE_TAC[]);
 360  (ASM_MESON_TAC[SQRT_POW_2])]);;
 361
 362 (* ===========================================================================*)
 363 (*    THE SIXTH LEMMA :                                                       *)
 364 (*         This lemma says that if the Euler formulation holds                *)
 365 (*         for the case where x1 = x2 = x3 = 1 then it holds for all cases    *)
 366 (*                                                                            *)
 367 (* ===========================================================================*)
 368
 369 let EULER_FORMULA_RESCALE = prove_by_refinement (
 370  `(!v0 v1:real^3 v2 v3 p x1 x2 x3 x4 x5 x6 alpha1 alpha2 alpha3 d w1 w2 w3.
 371       p = euler_p v0 v1 v2 v3 /\
 372       x1,x2,x3,x4,x5,x6 = xlist v0 v1 v2 v3 /\
 373       alpha1 = dihV v0 v1 v2 v3 /\
 374       alpha2 = dihV v0 v2 v3 v1 /\
 375       alpha3 = dihV v0 v3 v1 v2 /\
 376       d = delta_x x1 x2 x3 x4 x5 x6 /\
 377       w1 = v1 - v0 /\
 378       w2 = v2 - v0 /\
 379       w3 = v3 - v0 /\
 380       &0 < d /\
 381       norm w1 = &1 /\
 382       norm w2 = &1 /\
 383       norm w3 = &1
 384       ==> alpha1 + alpha2 + alpha3 - pi = pi - &2 * atn2 (sqrt d,&2 * p))
 385  ==> (!v0 v1:real^3 v2 v3.
 386         let p = euler_p v0 v1 v2 v3 in
 387         let x1,x2,x3,x4,x5,x6 = xlist v0 v1 v2 v3 in
 388         let alpha1 = dihV v0 v1 v2 v3 in
 389         let alpha2 = dihV v0 v2 v3 v1 in
 390         let alpha3 = dihV v0 v3 v1 v2 in
 391         let d = delta_x x1 x2 x3 x4 x5 x6 in
 392         &0 < d
 393         ==> alpha1 + alpha2 + alpha3 - pi = pi - &2 * atn2 (sqrt d,&2 * p))`,
 394
 395 (* -------------------------------------------------------------------------*)
 396 (*             Rescale by considering new points v1',v2',v3'                *)
 397 (* -------------------------------------------------------------------------*)
 398
 399 [(DISCH_TAC THEN REPEAT GEN_TAC THEN REPEAT LET_TAC THEN DISCH_TAC);
 400
 401 (ABBREV_TAC `v1' = v0 + inv (norm(v1:real^3 - v0)) % (v1 - v0)`);
 402 (ABBREV_TAC `v2' = v0 + inv (norm(v2:real^3 - v0)) % (v2 - v0)`);
 403 (ABBREV_TAC `v3' = v0 + inv (norm(v3:real^3 - v0)) % (v3 - v0)`);
 404 (ABBREV_TAC `w1' = (v1':real^3) - v0`);
 405 (ABBREV_TAC `w2' = (v2':real^3) - v0`);
 406 (ABBREV_TAC `w3' = (v3':real^3)- v0`);
 407
 408 (* -------------------------------------------------------------------------*)
 409 (*   Subgoal 1:   &0 < norm (v1 - v0)                                       *)
 410 (*                &0 < norm (v2 - v0)                                       *)
 411 (*                &0 < norm (v3 - v0)                                       *)
 412 (* -------------------------------------------------------------------------*)
 413
 414   (SUBGOAL_THEN
 415      `&0 < norm (v1:real^3 - v0)  /\
 416       &0 < norm (v2:real^3 - v0)  /\
 417       &0 < norm (v3:real^3 - v0)`
 418      ASSUME_TAC);
 419
 420   (PURE_ONCE_REWRITE_TAC[NORM_POS_LT]);
 421   (PURE_REWRITE_TAC[VECTOR_ARITH `(a - b = vec 0) <=> (a = b)`;
 422                       MESON[] `(a <=> b) <=> ~ a <=> ~ b`]);
 423   (REPEAT CONJ_TAC);  (* Break into 3 subgoal *)
 424
 425     STRIP_TAC;
 426     (SUBGOAL_THEN `collinear {v0:real^3 , v1,  v2}` ASSUME_TAC);
 427     (PURE_ONCE_ASM_REWRITE_TAC[]);
 428     (PURE_REWRITE_TAC[collinear; SET_RULE `{a, a, b} = {a , b}`]);
 429     (EXISTS_TAC `v2:real^3 - v0`);
 430     (REPEAT GEN_TAC);
 431     (REWRITE_TAC[SET_RULE ` x IN {a, b} <=> (x = a \/ x = b)`]);
 432     STRIP_TAC;   (* Break into 4 subgoals *)
 433
 434       (PURE_ONCE_ASM_REWRITE_TAC[]);
 435       (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC);
 436       (PURE_ONCE_ASM_REWRITE_TAC[]);
 437       (EXISTS_TAC `-- &1` THEN VECTOR_ARITH_TAC);
 438       (PURE_ONCE_ASM_REWRITE_TAC[]);
 439       (EXISTS_TAC `&1` THEN VECTOR_ARITH_TAC);
 440       (PURE_ONCE_ASM_REWRITE_TAC[]);
 441       (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC);
 442    (ASM_MESON_TAC[DELTA_X_LT_0_COLLINEAR]);
 443
 444     STRIP_TAC;
 445     (SUBGOAL_THEN `collinear {v0:real^3 , v1,  v2}` ASSUME_TAC);
 446     (PURE_ONCE_ASM_REWRITE_TAC[]);
 447     (PURE_REWRITE_TAC[collinear; SET_RULE `{a, b, a} = {a , b}`]);
 448     (EXISTS_TAC `v1:real^3 - v0`);
 449     (REPEAT GEN_TAC);
 450     (REWRITE_TAC[SET_RULE ` x IN {a, b} <=> (x = a \/ x = b)`]);
 451     STRIP_TAC;   (* Break into 4 subgoals *)
 452
 453       (PURE_ONCE_ASM_REWRITE_TAC[]);
 454       (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC);
 455       (PURE_ONCE_ASM_REWRITE_TAC[]);
 456       (EXISTS_TAC `-- &1` THEN VECTOR_ARITH_TAC);
 457       (PURE_ONCE_ASM_REWRITE_TAC[]);
 458       (EXISTS_TAC `&1` THEN VECTOR_ARITH_TAC);
 459       (PURE_ONCE_ASM_REWRITE_TAC[]);
 460       (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC);
 461    (ASM_MESON_TAC[DELTA_X_LT_0_COLLINEAR]);
 462
 463     STRIP_TAC;
 464     (SUBGOAL_THEN `collinear {v0:real^3 , v1,  v3}` ASSUME_TAC);
 465     (PURE_ONCE_ASM_REWRITE_TAC[]);
 466     (PURE_REWRITE_TAC[collinear; SET_RULE `{a, b, a} = {a , b}`]);
 467     (EXISTS_TAC `v1:real^3 - v0`);
 468     (REPEAT GEN_TAC);
 469     (REWRITE_TAC[SET_RULE ` x IN {a, b} <=> (x = a \/ x = b)`]);
 470     STRIP_TAC;   (* Break into 4 subgoals *)
 471
 472       (PURE_ONCE_ASM_REWRITE_TAC[]);
 473       (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC);
 474       (PURE_ONCE_ASM_REWRITE_TAC[]);
 475       (EXISTS_TAC `-- &1` THEN VECTOR_ARITH_TAC);
 476       (PURE_ONCE_ASM_REWRITE_TAC[]);
 477       (EXISTS_TAC `&1` THEN VECTOR_ARITH_TAC);
 478       (PURE_ONCE_ASM_REWRITE_TAC[]);
 479       (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC);
 480    (ASM_MESON_TAC[DELTA_X_LT_0_COLLINEAR]);
 481
 482
 483 (* -------------------------------------------------------------------------*)
 484 (*   Subgoal 2:   w1', w2', w3' havnorms equal 1                          *)
 485 (* -------------------------------------------------------------------------*)
 486
 487   (SUBGOAL_THEN
 488      `norm (w1':real^3) = &1 /\
 489       norm (w2':real^3) = &1 /\
 490       norm (w3':real^3) = &1`
 491      ASSUME_TAC);
 492
 493   (EXPAND_TAC "w1'" THEN EXPAND_TAC "w2'" THEN EXPAND_TAC "w3'");
 494   (UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC THEN DISCH_TAC);
 495   (EXPAND_TAC "v1'" THEN EXPAND_TAC "v2'" THEN EXPAND_TAC "v3'");
 496   (ONCE_REWRITE_TAC[VECTOR_ARITH `((a:real^3) + b) - a = b`]);
 497   (REWRITE_TAC[NORM_MUL;REAL_ABS_INV]);
 498
 499       (SUBGOAL_THEN
 500          `abs (norm (v1 - v0)) = norm (v1:real^3 - v0) /\
 501           abs (norm (v2 - v0)) = norm (v2:real^3 - v0) /\
 502           abs (norm (v3 - v0)) = norm (v3:real^3 - v0)`
 503           ASSUME_TAC);
 504       (SIMP_TAC[NORM_POS_LE;REAL_ABS_REFL]);
 505
 506   (ONCE_ASM_REWRITE_TAC[]);
 507   (ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> ~(a = &0)`;REAL_MUL_LINV]);
 508
 509 (* ------------------------------------------------------------------------- *)
 510 (*  SUBGOAL 3 :                                                              *)
 511 (*                  alpha1, alpha2, alpha3 arunchanged                     *)
 512 (* ------------------------------------------------------------------------- *)
 513
 514 (ABBREV_TAC `alpha1' = dihV (v0:real^3) v1' v2' v3'`);
 515 (ABBREV_TAC `alpha2' = dihV (v0:real^3) v2' v3' v1'`);
 516 (ABBREV_TAC `alpha3' = dihV (v0:real^3) v3' v1' v2'`);
 517
 518   (SUBGOAL_THEN
 519     `alpha1:real = alpha1' /\ alpha2:real = alpha2' /\ alpha3:real = alpha3'`
 520     ASSUME_TAC);
 521   (EXPAND_TAC "alpha1" THEN EXPAND_TAC "alpha2" THEN EXPAND_TAC "alpha3");
 522   (EXPAND_TAC "alpha1'" THEN EXPAND_TAC "alpha2'" THEN EXPAND_TAC "alpha3'");
 523   (ABBREV_TAC `m = inv (norm (v1:real^3 - v0))`);
 524   (ABBREV_TAC `n = inv (norm (v2:real^3 - v0))`);
 525   (ABBREV_TAC `q = inv (norm (v3:real^3 - v0))`);
 526
 527      (SUBGOAL_THEN
 528         ` v1' - v0 = m % (v1:real^3 - v0) /\
 529           v2' - v0 = n % (v2:real^3 - v0) /\
 530           v3' - v0 = q % (v3:real^3 - v0)`
 531          ASSUME_TAC);
 532      (EXPAND_TAC "v1'" THEN EXPAND_TAC "v2'" THEN EXPAND_TAC "v3'");
 533      (VECTOR_ARITH_TAC);
 534
 535      (SUBGOAL_THEN `&0 < m /\ &0 < n /\ &0 < q ` ASSUME_TAC);
 536      (EXPAND_TAC "m" THEN EXPAND_TAC "n" THEN EXPAND_TAC "q");
 537      (REPLICATE_TAC 8 DEL_TAC THEN UP_ASM_TAC THEN STRIP_TAC);
 538      (ASM_MESON_TAC[REAL_LT_INV]);
 539
 540   (ASM_MESON_TAC[DIHV_RESCALE_UNCHANGED]);
 541
 542
 543 (* ========================================================================== *)
 544 (*  Subgoal 4:                                                                *)
 545 (*       (x1',x2',x3,'x4',x5',x6') = xlist (v0:real^3) v1' v2' v3'            *)
 546 (* ========================================================================== *)
 547
 548 (ABBREV_TAC `p' = euler_p (v0:real^3) v1' v2' v3'`);
 549 (ABBREV_TAC `x1' = dist (v0:real^3,v1') pow 2`);
 550 (ABBREV_TAC `x2' = dist (v0:real^3,v2') pow 2`);
 551 (ABBREV_TAC `x3' = dist (v0:real^3,v3') pow 2`);
 552 (ABBREV_TAC `x4' = dist (v2':real^3,v3') pow 2`);
 553 (ABBREV_TAC `x5' = dist (v1':real^3,v3') pow 2`);
 554 (ABBREV_TAC `x6' = dist (v1':real^3,v2') pow 2`);
 555 (ABBREV_TAC `d' = delta_x (x1':real) x2' x3' x4' x5' x6' `);
 556
 557   (SUBGOAL_THEN
 558     `x1':real,x2',x3',x4',x5',x6' =
 559      xlist (v0:real^3) v1' v2' v3'`
 560     ASSUME_TAC);
 561
 562   (REWRITE_TAC[xlist;ylist]);
 563   (REPEAT LET_TAC);
 564   (UP_ASM_TAC THEN PURE_REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC);
 565   (ASM_MESON_TAC[PAIR_EQ]);
 566
 567 (* --------------------------------------------------------------------------*)
 568 (*  Subgoal 5:                                                               *)
 569 (*                          p' = k * p with somk                           *)
 570 (*---------------------------------------------------------------------------*)
 571
 572 (ABBREV_TAC `t1 = inv (norm ((v1:real^3) - v0)) `);
 573 (ABBREV_TAC `t2 = inv (norm ((v2:real^3) - v0)) `);
 574 (ABBREV_TAC `t3 = inv (norm ((v3:real^3) - v0)) `);
 575
 576   (SUBGOAL_THEN `p' = (t1 * t2 * t3) * p` ASSUME_TAC);
 577   (EXPAND_TAC "p" THEN EXPAND_TAC "p'");
 578   (MATCH_MP_TAC COMPUTE_EULER_P_AFTER_RESCALE);
 579   (EXPAND_TAC "v1'" THEN EXPAND_TAC "v2'" THEN EXPAND_TAC "v3'");
 580   (REWRITE_TAC[VECTOR_ARITH `((a:real^3) + b) - a = b`]);
 581   (EXPAND_TAC "t1" THEN EXPAND_TAC "t2" THEN EXPAND_TAC "t3");
 582   (ASM_MESON_TAC[REAL_LT_INV]);
 583
 584 (* --------------------------------------------------------------------------*)
 585 (*  Subgoal 6:                                                               *)
 586 (*                          d' = k * d with somk                           *)
 587 (*---------------------------------------------------------------------------*)
 588
 589   (SUBGOAL_THEN `d' = (t1 * t2 * t3) * (t1 * t2 * t3) * d` ASSUME_TAC);
 590   (EXPAND_TAC "d" THEN EXPAND_TAC "d'");
 591   (MATCH_MP_TAC COMPUTE_DELTA_X_AFTER_RESCALE);
 592   (EXISTS_TAC `v0:real^3`);
 593   (EXISTS_TAC `v1':real^3`);
 594   (EXISTS_TAC `v2':real^3`);
 595   (EXISTS_TAC `v3':real^3`);
 596   (EXISTS_TAC `v0:real^3`);
 597   (EXISTS_TAC `v1:real^3`);
 598   (EXISTS_TAC `v2:real^3`);
 599   (EXISTS_TAC `v3:real^3`);
 600   (EXPAND_TAC "v1'" THEN EXPAND_TAC "v2'" THEN EXPAND_TAC "v3'");
 601   (REWRITE_TAC[VECTOR_ARITH `((a:real^3) + b) - a = b`]);
 602   (ASM_REWRITE_TAC[]);
 603
 604     (SUBGOAL_THEN `&0 < t1 /\ &0 < t2 /\ &0 < t3 /\ &0 <  d` ASSUME_TAC);
 605     (EXPAND_TAC "t1" THEN EXPAND_TAC "t2" THEN EXPAND_TAC "t3");
 606     (REPLICATE_TAC 18 DEL_TAC);
 607     (UP_ASM_TAC THEN REPLICATE_TAC 6 DEL_TAC THEN UP_ASM_TAC);
 608     (MESON_TAC[REAL_LT_INV]);
 609
 610   (UP_ASM_TAC THEN MESON_TAC[REAL_ARITH `&0 < a ==> &0 <= a`]);
 611
 612
 613 (* -------------------------------------------------------------------------- *)
 614 (*  Subgoal 7:                                                                *)
 615 (*                This part is thproof of  d' > 0                           *)
 616 (* -------------------------------------------------------------------------- *)
 617
 618
 619   (SUBGOAL_THEN `&0 < d'` ASSUME_TAC);
 620   (PURE_ONCE_ASM_REWRITE_TAC[]);
 621
 622     (SUBGOAL_THEN `&0 < t1 /\ &0 < t2 /\ &0 < t3 /\ &0 <  d` ASSUME_TAC);
 623     (EXPAND_TAC "t1" THEN EXPAND_TAC "t2" THEN EXPAND_TAC "t3");
 624     (REPLICATE_TAC 19 DEL_TAC);
 625     (UP_ASM_TAC THEN REPLICATE_TAC 6 DEL_TAC THEN UP_ASM_TAC);
 626     (MESON_TAC[REAL_LT_INV]);
 627
 628   (UP_ASM_TAC THEN MESON_TAC[REAL_LT_MUL]);
 629
 630 (*---------------------------------------------------------------------------*)
 631 (*  Subgoal 8:                                                               *)
 632 (*                    atn2 (sqrt d,&2 * p) is unchanged                      *)
 633 (*---------------------------------------------------------------------------*)
 634
 635   (SUBGOAL_THEN `&2 * atn2 (sqrt (d':real), &2 * (p':real)) =
 636                    &2 * atn2 (sqrt (d:real), &2 * (p:real))` ASSUME_TAC);
 637   AP_TERM_TAC;
 638     (* Sugoal 8.1 *)
 639
 640     (SUBGOAL_THEN `&0 < sqrt d /\ &0 < sqrt d'` ASSUME_TAC);
 641     (MESON_TAC[ASSUME `&0 < d`; ASSUME `&0 < d'`; SQRT_POS_LT]);
 642     (* Sugoal 8.2 *)
 643     (SUBGOAL_THEN `atn2 (sqrt d,&2 * p) = atn ((&2 * p) / sqrt d)`
 644        ASSUME_TAC);
 645     (FIRST_ASSUM MP_TAC THEN MESON_TAC[ATN2_BREAKDOWN]);
 646     (* Sugoal 8.3 *)
 647
 648     (SUBGOAL_THEN `atn2 (sqrt d',&2 * p') = atn ((&2 * p') / sqrt d')`
 649        ASSUME_TAC);
 650     (MESON_TAC[ASSUME `&0 < sqrt d /\ &0 < sqrt d'`; ATN2_BREAKDOWN]);
 651
 652   (ONCE_ASM_REWRITE_TAC[]);
 653   AP_TERM_TAC;
 654   (DEL_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN STRIP_TAC);
 655
 656      (* Sugoal 8.4 *)
 657      (SUBGOAL_THEN `((&2 * p') / sqrt d' = (&2 * p) / sqrt d) <=>
 658                       &2 * p' = ((&2 * p) / sqrt d) * sqrt d'`
 659         ASSUME_TAC);
 660      (UP_ASM_TAC THEN MESON_TAC[REAL_EQ_LDIV_EQ]);
 661
 662   (ONCE_ASM_REWRITE_TAC[]);
 663   (REWRITE_TAC[REAL_ARITH `((x * y) / b) * c = x * (c * y) / b`]);
 664   AP_TERM_TAC;
 665   DEL_TAC;
 666   (PURE_ASM_REWRITE_TAC[REAL_EQ_LDIV_EQ]);
 667   (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(x * y) / b = (x / b) * y`]);
 668   (AP_THM_TAC THEN AP_TERM_TAC);
 669   (ABBREV_TAC `S = t1 * t2 * t3`);
 670   (REWRITE_TAC[REAL_MUL_ASSOC;GSYM REAL_POW_2]);
 671
 672     (* Subgoal 8.5 *)
 673     (SUBGOAL_THEN `sqrt (S pow 2 * d) = sqrt (S pow 2) * sqrt d` ASSUME_TAC);
 674     (MATCH_MP_TAC SQRT_MUL);
 675     (ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> &0 <= a`]);
 676     (MESON_TAC[REAL_LE_POW_2]);
 677
 678   (ONCE_ASM_REWRITE_TAC[]);
 679   (ONCE_REWRITE_TAC[REAL_ARITH `(a * b) / c = a * (b / c)`]);
 680
 681     (* Subgoal 8.6 *)
 682     (SUBGOAL_THEN `sqrt d / sqrt d = &1` ASSUME_TAC);
 683     (MATCH_MP_TAC REAL_DIV_REFL);
 684     (ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> ~ (a = &0)`]);
 685
 686   (ONCE_ASM_REWRITE_TAC[]);
 687   (REWRITE_TAC[REAL_MUL_RID]);
 688   (MATCH_MP_TAC (GSYM SQRT_OF_POW_2_LE));
 689   (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
 690   (EXPAND_TAC "S");
 691
 692     (* Subgoal 8.7 *)
 693     (SUBGOAL_THEN `&0 < t1 /\ &0 < t2 /\ &0 < t3 /\ &0 <  d` ASSUME_TAC);
 694     (EXPAND_TAC "t1" THEN EXPAND_TAC "t2" THEN EXPAND_TAC "t3");
 695     (REPLICATE_TAC 19 DEL_TAC);
 696     (ASM_MESON_TAC[REAL_LT_INV]);
 697   (UP_ASM_TAC THEN MESON_TAC[REAL_LT_MUL]);
 698
 699 (*---------------------------------------------------------------------------*)
 700 (*   SUBGOAL 9 :                                                             *)
 701 (*                         Finish the lemma about rescaling                  *)
 702 (*---------------------------------------------------------------------------*)
 703
 704   (SUBGOAL_THEN
 705      `alpha1' + alpha2' + alpha3' - pi = pi - &2 * atn2 (sqrt d',&2 * p')`
 706      ASSUME_TAC);
 707   (ASM_MESON_TAC[]);
 708
 709 (ASM_MESON_TAC[])]);;
 710
 711 (* ==========================================================================*)
 712 (*       LEMMA 7 :                                                           *)
 713 (*       ~ collinear {a, b, c} ==> norm(a - b) > &0                          *)
 714 (* ==========================================================================*)
 715
 716 let COLLINEAR_NORM_LT_0 = prove_by_refinement (
 717  `!(a:real^3) b c. ~collinear {a, b, c} ==> &0 < norm (a - b)`,
 718
 719 [(REPEAT GEN_TAC THEN REPEAT STRIP_TAC);
 720 (REWRITE_TAC[NORM_POS_LT]);
 721 STRIP_TAC;
 722 (UP_ASM_TAC THEN PURE_ONCE_REWRITE_TAC[
 723    VECTOR_ARITH `(a:real^3) - b = vec 0 <=> b - a = vec 0`]);
 724 STRIP_TAC;
 725
 726   (SUBGOAL_THEN `collinear {(a:real^3), b, c}` ASSUME_TAC);
 727   (MATCH_MP_TAC (GEN_ALL ALLEMI_COLLINEAR));
 728   (ASM_REWRITE_TAC[]);
 729   (MESON_TAC [VECTOR_ARITH `a dot vec 0 = &0`;
 730                 VECTOR_ARITH `a % vec 0 = vec 0`;
 731                 VECTOR_ARITH `(&0) % c = vec 0`]);
 732 (ASM_MESON_TAC[])]);;
 733
 734 (* ========================================================================= *)
 735 (*       LEMMA 8:                                                            *)
 736 (* ========================================================================= *)
 737
 738 let REAL_LT_RSQRT2 = prove
 739  (`!x y. x pow 2 < y ==> -- sqrt y < x`,
 740   REPEAT STRIP_TAC THEN
 741   MATCH_MP_TAC(REAL_ARITH `abs x < a ==> -- a < x`) THEN
 742   REWRITE_TAC[GSYM POW_2_SQRT_ABS] THEN
 743   MATCH_MP_TAC SQRT_MONO_LT THEN
 744   ASM_REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE]);;
 745
 746 let EULER_TRIANGLE_REAL_INTERVAL = prove_by_refinement (
 747  `!s a b c.
 748        s = {x | &0 < ups_x x b c - x * b * c} /\ &0 < ups_x a b c - a * b * c
 749        ==> is_realinterval s`,
 750
 751 [(REPEAT GEN_TAC THEN STRIP_TAC);
 752 (ABBREV_TAC `d = b * c * b * c / &4 - b * c * (b + c) + &4 * b * c `);
 753 (ABBREV_TAC `f = (\a. a - b - c + b * c / &2)`);
 754
 755 (* ------------------------------------------------------------------------- *)
 756 (*             SUBGOAL 1                                                     *)
 757 (* ------------------------------------------------------------------------- *)
 758
 759
 760   (SUBGOAL_THEN `&0 < d` ASSUME_TAC);
 761   (EXPAND_TAC "d" THEN DEL_TAC THEN DEL_TAC);
 762   (UP_ASM_TAC THEN REWRITE_TAC[ups_x] THEN DISCH_TAC);
 763   (MATCH_MP_TAC (REAL_ARITH
 764      `&0 <= (a - b - c + b * c / &2) pow 2 /\
 765       &0 < S - (a - b - c + b * c / &2) pow 2 ==> &0 < S`));
 766   (REWRITE_TAC[REAL_LE_POW_2]);
 767   ASM_REAL_ARITH_TAC;
 768
 769 (* ------------------------------------------------------------------------- *)
 770 (*           SUBGOAL 2                                                       *)
 771 (* ------------------------------------------------------------------------- *)
 772
 773   (SUBGOAL_THEN
 774     `!(z:real). z IN s <=> f z < sqrt d /\ --sqrt d < f z`
 775     ASSUME_TAC);
 776   GEN_TAC;
 777   (ONCE_ASM_REWRITE_TAC[] THEN ONCE_ASM_REWRITE_TAC[IN_ELIM_THM]);
 778   (EQ_TAC);  (* Break into 2 subgoal 2.1 and 2.2  *)
 779
 780       (REWRITE_TAC[ups_x] THEN DISCH_TAC);
 781       (SUBGOAL_THEN `(f (z:real)) pow 2 < d /\ (f z) pow 2 < d` ASSUME_TAC);
 782       (EXPAND_TAC "d" THEN EXPAND_TAC "f");
 783       (PURE_REWRITE_TAC[REAL_POW_2]);
 784       (ASM_REAL_ARITH_TAC);
 785       (ASM_MESON_TAC[REAL_LT_RSQRT;REAL_LT_RSQRT2]);
 786
 787       (REWRITE_TAC[ups_x] THEN EXPAND_TAC "f");
 788       STRIP_TAC;
 789       (REWRITE_TAC[REAL_ARITH
 790          `(--z * z - b * b - c * c + &2 * z * c + &2 * z * b + &2 * b * c) -
 791           z * b * c =
 792           (b * c * b * c / &4 - b * c * (b + c) + &4 * b * c) -
 793           (z - b - c + b * c / &2) pow 2`]);
 794       (REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`]);
 795       (PURE_ONCE_ASM_REWRITE_TAC[]);
 796       (REPLICATE_TAC 2 UP_ASM_TAC THEN PURE_REWRITE_TAC[MESON[REAL_BOUNDS_LT]
 797          `(a < x ==> -- x < a ==> y) <=> abs a < x ==> y` ]);
 798       DISCH_TAC;
 799
 800         (SUBGOAL_THEN `d = sqrt d pow 2` ASSUME_TAC);
 801         (ASM_MESON_TAC[REAL_ARITH `&0 < a ==> &0 <= a`; SQRT_POW_2]);
 802       (PURE_ONCE_ASM_REWRITE_TAC[]);
 803       (ASM_REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS]);
 804       (MATCH_MP_TAC (REAL_ARITH `x = sqrt d /\ y < sqrt d  ==> y < x`));
 805       (ASM_REWRITE_TAC[]);
 806       (PURE_REWRITE_TAC[REAL_ABS_REFL]);
 807       (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
 808       (ASM_MESON_TAC[SQRT_POS_LT]);
 809
 810 (* ------------------------------------------------------------------------- *)
 811 (*           LAST SUBGOALS                                                   *)
 812 (* ------------------------------------------------------------------------- *)
 813
 814 (REWRITE_TAC[is_realinterval]);
 815 (REPEAT GEN_TAC THEN STRIP_TAC);
 816 (ONCE_ASM_REWRITE_TAC[]);
 817 CONJ_TAC;
 818
 819   (SUBGOAL_THEN `f (c':real) <= f b'` ASSUME_TAC);
 820   (EXPAND_TAC "f" THEN ASM_REAL_ARITH_TAC);
 821   (SUBGOAL_THEN `f (b':real) < sqrt d` ASSUME_TAC);
 822   (EXPAND_TAC "f" THEN ASM_MESON_TAC[]);
 823   (ASM_REAL_ARITH_TAC);
 824
 825   (SUBGOAL_THEN `f (a':real) <= f c'` ASSUME_TAC);
 826   (EXPAND_TAC "f" THEN ASM_REAL_ARITH_TAC);
 827   (SUBGOAL_THEN `-- sqrt d < f (a':real)` ASSUME_TAC);
 828   (EXPAND_TAC "f" THEN ASM_MESON_TAC[]);
 829   (ASM_REAL_ARITH_TAC)]);;
 830
 831 (* ==========================================================================*)
 832 (*       LEMMA 10:                                                           *)
 833 (*                                                                           *)
 834 (* ==========================================================================*)
 835
 836 let OJEKOJF2 =
 837  prove (`!v0:real^3 v1 v2 v3.
 838          let ga = dihV v0 v1 v2 v3 in
 839          let v01 = dist (v0,v1) pow 2 in
 840          let v02 = dist (v0,v2) pow 2 in
 841          let v03 = dist (v0,v3) pow 2 in
 842          let v12 = dist (v1,v2) pow 2 in
 843          let v13 = dist (v1,v3) pow 2 in
 844          let v23 = dist (v2,v3) pow 2 in
 845          ~collinear {v0, v1, v2} /\ ~collinear {v0, v1, v3}
 846          ==> ga =
 847              pi / &2 -
 848              atn2
 849              (sqrt (&4 * v01 * delta_x v01 v02 v03 v23 v13 v12),
 850               delta_x4 v01 v02 v03 v23 v13 v12)`,
 851     MP_TAC OJEKOJF THEN REPEAT LET_TAC THEN MESON_TAC[]);;
 852
 853 let COMPUTE_DIHV_ATN2 = prove
 854 (`!(v0:real^3) v1 v2 v3 gamma x1 x2 x3 x4 x5 x6.
 855                     gamma = dihV v0 v1 v2 v3 /\
 856                      x1 = dist (v0,v1) pow 2 /\
 857                      x2 = dist (v0,v2) pow 2 /\
 858                      x3 = dist (v0,v3) pow 2 /\
 859                      x6 = dist (v1,v2) pow 2 /\
 860                      x5 = dist (v1,v3) pow 2 /\
 861                      x4 = dist (v2,v3) pow 2 /\
 862                      ~collinear {v0, v1, v2} /\
 863                      ~collinear {v0, v1, v3}
 864  ==>  gamma = pi / &2 - atn2( sqrt ( &4 * x1 * delta_x x1 x2 x3 x4 x5 x6),
 865                                      delta_x4 x1 x2 x3 x4 x5 x6)`,
 866 REPEAT STRIP_TAC THEN MP_TAC OJEKOJF2 THEN REPEAT LET_TAC THEN
 867 ASM_REWRITE_TAC[] THEN EXPAND_TAC "ga" THEN
 868 EXPAND_TAC "v01" THEN EXPAND_TAC "v02" THEN EXPAND_TAC "v03" THEN
 869 EXPAND_TAC "v13" THEN EXPAND_TAC "v23" THEN EXPAND_TAC "v12" THEN
 870 DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
 871
 872 end;;