text_formalization/trigonometry/euler_main_theorem.hl

   1 (* ========================================================================= *)
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   3 (*          COMPLEMENT LEMMAS FOR EULER TRIANGLE LEMMA                       *)
   4 (*                                                                           *)
   5 (*                       EULER TRIANGLE LEMMA                                *)
   6 (*                                                                           *)
   7 (*      Authour : VU KHAC KY                                                 *)
   8 (*      Date : 2010-04-02                                                    *)
   9 (*      Books name: JLPSDHF                                                  *)
  10 (* ========================================================================= *)
  11
  12
  13 (* =========================================================================*)
  14 (*                                                                          *)
  15 (*         BEGIN THE MAIN THEORM ABOUT EULER ANGLE SUM                      *)
  16 (*                                                                          *)
  17 (*==========================================================================*)
  18
  19
  20 flyspeck_needs "general/sphere.hl";;
  21
  22 flyspeck_needs "general/prove_by_refinement.hl";;
  23
  24 flyspeck_needs "trigonometry/trig1.hl";;
  25 flyspeck_needs "trigonometry/trig2.hl";;
  26 flyspeck_needs "trigonometry/delta_x.hl";;
  27 flyspeck_needs "trigonometry/euler_complement.hl";;
  28 flyspeck_needs "trigonometry/euler_multivariate.hl";;
  29
  30
  31
  32 module Euler_main_theorem = struct
  33
  34 open Sphere;;
  35 open Trigonometry1;;
  36 open Trigonometry2;;
  37 open Prove_by_refinement;;
  38 open Delta_x;;
  39 open Euler_complement;;
  40 open Euler_multivariate;;
  41
  42 let euler_angle_sum_rescale =
  43  ` !v0:real^3 v1 v2 v3 p x1 x2 x3 x4 x5 x6 alpha1 alpha2 alpha3 d w1 w2 w3.
  44           p = euler_p v0 v1 v2 v3 /\
  45           x1,x2,x3,x4,x5,x6 = xlist v0 v1 v2 v3 /\
  46           alpha1 = dihV v0 v1 v2 v3 /\
  47           alpha2 = dihV v0 v2 v3 v1 /\
  48           alpha3 = dihV v0 v3 v1 v2 /\
  49           d = delta_x x1 x2 x3 x4 x5 x6 /\
  50           w1 = v1 - v0 /\
  51           w2 = v2 - v0 /\
  52           w3 = v3 - v0 /\
  53           &0 < d /\
  54           norm w1 = &1 /\
  55           norm w2 = &1 /\
  56           norm w3 = &1
  57           ==> alpha1 + alpha2 + alpha3 - pi = pi - &2 * atn2 (sqrt d,&2 * p)`;;
  58
  59 let EULER_ANGLE_SUM_rescal = prove_by_refinement (euler_angle_sum_rescale ,
  60
  61 [ (REPEAT GEN_TAC) ;
  62  (REPEAT STRIP_TAC);
  63  (REPLICATE_TAC 11 UP_ASM_TAC);
  64  (FIRST_ASSUM MP_TAC THEN SWITCH_TAC THEN FIRST_ASSUM MP_TAC);
  65  (REWRITE_TAC[euler_p;xlist;ylist]);
  66  (REPEAT LET_TAC);
  67  (REPEAT UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ] THEN REPEAT STRIP_TAC);
  68
  69 (* ==========================================================================*)
  70 (*    3 FIRST SUBGOALS:                                                      *)
  71 (* ==========================================================================*)
  72
  73    (SUBGOAL_THEN
  74         ` ~collinear {(v0:real^3), v1, v2} /\
  75           ~collinear {v0, v1, v3} /\
  76           ~collinear {v0, v3, v2}`
  77     ASSUME_TAC);
  78    (ASM_MESON_TAC[DELTA_X_LT_0_COLLINEAR]);
  79
  80    (SUBGOAL_THEN `y1 = &1 /\ y2 = &1 /\ y3 = &1` ASSUME_TAC);
  81    (EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");
  82    (PURE_ONCE_REWRITE_TAC[DIST_SYM]);
  83    (PURE_ONCE_REWRITE_TAC[dist]);
  84    (ASM_MESON_TAC[]);
  85    (UP_ASM_TAC THEN STRIP_TAC);
  86
  87    (SUBGOAL_THEN `x1 = &1 /\ x2 = &1 /\ x3 = &1` ASSUME_TAC);
  88    (ASM_REWRITE_TAC[]);
  89    (ONCE_ASM_REWRITE_TAC[REAL_POW_2]);
  90    REAL_ARITH_TAC;
  91    (UP_ASM_TAC THEN STRIP_TAC);
  92
  93 (* ==========================================================================*)
  94 (*   Subgoal 4:    Comput p and delta                                       *)
  95 (* ==========================================================================*)
  96
  97    (SUBGOAL_THEN
  98     `&2 * p = &8 - x4 - x5 - x6 /\ d = ups_x x4 x5 x6 - x4 * x5 * x6`
  99     ASSUME_TAC);
 100
 101      (SUBGOAL_THEN
 102        `x4 = (v2 - v3) dot (v2 - v3:real^3) /\
 103         x5 = (v1 - v3) dot (v1 - v3) /\
 104         x6 = (v1 - v2) dot (v1 - v2)`
 105        ASSUME_TAC);
 106
 107      (ASM_REWRITE_TAC[]);
 108      (EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6");
 109      (ONCE_REWRITE_TAC[dist]);
 110      (REWRITE_TAC[NORM_POW_2]);
 111
 112    CONJ_TAC;  (* Break into 2 subgoals *)
 113
 114      (REPEAT UP_ASM_TAC THEN DISCH_TAC THEN DISCH_TAC);
 115      (DEL_TAC THEN REPEAT DISCH_TAC);
 116      (ONCE_ASM_REWRITE_TAC[]);
 117      (ONCE_ASM_REWRITE_TAC[]);
 118      (REWRITE_TAC [REAL_MUL_LID]);
 119      (EXPAND_TAC "w1'" THEN EXPAND_TAC "w2'" THEN EXPAND_TAC "w3'");
 120      (EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6");
 121      (REWRITE_TAC[dist]);
 122      (REWRITE_TAC[NORM_POW_2]);
 123      (ASM_MESON_TAC[LEMMA_FOR_EULER_AFTER_RESCALE]);
 124
 125      (ASM_REWRITE_TAC[]);
 126      (REWRITE_TAC[ups_x;delta_x]);
 127      (ONCE_ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
 128
 129 (* ========================================================================= *)
 130 (*      Re-comput alpha1, alpha2, alpha3 .                                  *)
 131 (* ========================================================================= *)
 132
 133 (* ------------------------------------------------------------------------- *)
 134 (*      Subgoal 5:  alpha1                                                   *)
 135 (* ------------------------------------------------------------------------- *)
 136
 137
 138    (SUBGOAL_THEN
 139   `alpha1 =
 140    pi / &2 -
 141    atn2 (sqrt (&4 * x1 * delta_x x1 x2 x3 x4 x5 x6),delta_x4 x1 x2 x3 x4 x5 x6)`
 142    ASSUME_TAC);
 143
 144  (REPLICATE_TAC 7 DEL_TAC THEN UP_ASM_TAC THEN DISCH_TAC);
 145  (MP_TAC COMPUTE_DIHV_ATN2);
 146  (ASM_MESON_TAC[COMPUTE_DIHV_ATN2]);
 147
 148 (* ------------------------------------------------------------------------- *)
 149 (*      Subgoal 6:  alpha2                                                   *)
 150 (* ------------------------------------------------------------------------- *)
 151
 152    (SUBGOAL_THEN
 153   `alpha2 =
 154    pi / &2 -
 155    atn2 (sqrt (&4 * x2 * delta_x x2 x3 x1 x5 x6 x4),delta_x4 x2 x3 x1 x5 x6 x4)`
 156    ASSUME_TAC);
 157
 158    (REPLICATE_TAC 8 DEL_TAC);
 159
 160      (SUBGOAL_THEN
 161       `x4 = dist (v2:real^3,v3) pow 2 /\
 162        x5 = dist (v3,v1) pow 2 /\
 163        x6 = dist (v2,v1) pow 2 /\
 164       ~collinear {v0, v2, v3} /\
 165       ~collinear {v0, v2, v1}`
 166        ASSUME_TAC);
 167      (ASM_MESON_TAC[DIST_SYM;SET_RULE `{v0,v1, v2} = {v0,v2,v1}`]);
 168
 169    (REPLICATE_TAC 13 UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC);
 170    (REPEAT DISCH_TAC);
 171    (ONCE_ASM_REWRITE_TAC[]);
 172    (EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");
 173    (ASM_MESON_TAC[COMPUTE_DIHV_ATN2]);
 174
 175 (* ------------------------------------------------------------------------- *)
 176 (*      Subgoal 7:  alpha3                                                   *)
 177 (* ------------------------------------------------------------------------- *)
 178
 179
 180    (SUBGOAL_THEN
 181   `alpha3 =
 182    pi / &2 -
 183    atn2 (sqrt (&4 * x3 * delta_x x3 x1 x2 x6 x4 x5),delta_x4 x3 x1 x2 x6 x4 x5)`
 184    ASSUME_TAC);
 185
 186    (REPLICATE_TAC 9 DEL_TAC);
 187
 188      (SUBGOAL_THEN
 189       `x5 = dist (v3:real^3,v1) pow 2 /\
 190        x4 = dist (v3,v2) pow 2 /\
 191        x6 = dist (v1,v2) pow 2 /\
 192       ~collinear {v0, v3, v1} /\
 193       ~collinear {v0, v3, v2}`
 194        ASSUME_TAC);
 195      (ASM_MESON_TAC[DIST_SYM;SET_RULE `{v0,v1, v2} = {v0,v2,v1}`]);
 196
 197    (REPLICATE_TAC 13 UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC);
 198    (REPEAT DISCH_TAC);
 199    (ONCE_ASM_REWRITE_TAC[]);
 200    (EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");
 201    (ASM_MESON_TAC[COMPUTE_DIHV_ATN2]);
 202
 203 (* ------------------------------------------------------------------------- *)
 204 (*      Subgoal 8:  delta_x is symmetry                                      *)
 205 (* ------------------------------------------------------------------------- *)
 206
 207    (SUBGOAL_THEN
 208     `delta_x x2 x3 x1 x5 x6 x4 = d /\ delta_x x3 x1 x2 x6 x4 x5 = d`
 209      ASSUME_TAC);
 210
 211      (SUBGOAL_THEN
 212      `x2, x3, x1, x5, x6, x4 = xlist (v0:real^3) v2 v3 v1`
 213       ASSUME_TAC);
 214      (REWRITE_TAC[xlist;ylist]);
 215      (REPEAT LET_TAC);
 216      (UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC);
 217      (ASM_MESON_TAC[DIST_SYM]);
 218
 219      (SUBGOAL_THEN
 220       `x3, x1, x2, x6, x4, x5 = xlist (v0:real^3) v3 v1 v2`
 221        ASSUME_TAC);
 222      (REWRITE_TAC[xlist;ylist]);
 223      (REPEAT LET_TAC);
 224      (UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC);
 225      (ASM_MESON_TAC[DIST_SYM]);
 226
 227    (ASM_REWRITE_TAC[]);
 228    (REWRITE_TAC[delta_x]);
 229    REAL_ARITH_TAC;
 230
 231 (* ------------------------------------------------------------------------- *)
 232 (*      Subgoal 9:  Th simplest  form of alpha1,2,3                         *)
 233 (* ------------------------------------------------------------------------- *)
 234
 235    (SUBGOAL_THEN
 236   `alpha1 =
 237    pi / &2 - atn ((-- &2 * x4 + &2 * x5 + &2 * x6 - x5 * x6) / sqrt (&4 * d)) /\
 238    alpha2 =
 239    pi / &2 - atn ((-- &2 * x5 + &2 * x6 + &2 * x4 - x6 * x4) / sqrt (&4 * d)) /\
 240    alpha3 =
 241    pi / &2 - atn ((-- &2 * x6 + &2 * x4 + &2 * x5 - x4 * x5) / sqrt (&4 * d))`
 242    ASSUME_TAC);
 243
 244    (ABBREV_TAC `4D = &4 * d`);
 245    (REPLICATE_TAC 21 UP_ASM_TAC THEN REPLICATE_TAC 9 DEL_TAC);
 246    (REPEAT DISCH_TAC);
 247    (ONCE_ASM_REWRITE_TAC[]);
 248    (REWRITE_TAC[REAL_ARITH `a - x = a - y <=> x = y`]);
 249
 250    (REWRITE_TAC[GSYM (ASSUME `d = delta_x x1 x2 x3 x4 x5 x6`)]);
 251    (REWRITE_TAC[ASSUME `delta_x x2 x3 x1 x5 x6 x4 = d /\
 252                          delta_x x3 x1 x2 x6 x4 x5 = d`]);
 253
 254    (REWRITE_TAC[delta_x4]);
 255    (REWRITE_TAC[ASSUME `x1 = &1`]);
 256    (REWRITE_TAC[ASSUME `x2 = &1`]);
 257    (REWRITE_TAC[ASSUME `x3 = &1`]);
 258    (REWRITE_TAC[REAL_MUL_LID;REAL_MUL_RID]);
 259
 260    (REWRITE_TAC[REAL_ARITH
 261      `-- &1 - x4 + x5 + x6 - x5 * x6 + -- &1 + &1 + &1 - x4 + x5 + x6
 262       = (-- &2 * x4 + &2 * x5 + &2 * x6 - x5 * x6) /\
 263       -- &1 - x5 + x6 + x4 - x6 * x4 + -- &1 + &1 + &1 - x5 + x6 + x4
 264       = (-- &2 * x5 + &2 * x6 + &2 * x4 - x6 * x4) /\
 265       -- &1 - x6 + x4 + x5 - x4 * x5 + -- &1 + &1 + &1 - x6 + x4 + x5
 266       = (-- &2 * x6 + &2 * x4 + &2 * x5 - x4 * x5)`]);
 267    (EXPAND_TAC "4D");
 268
 269      (SUBGOAL_THEN `&0 < sqrt (&4 * d)` ASSUME_TAC);
 270      (MATCH_MP_TAC SQRT_POS_LT);
 271      (ASM_MESON_TAC[REAL_ARITH `&0 < &4`;REAL_LT_MUL]);
 272
 273    (ASM_MESON_TAC[ATN2_BREAKDOWN]);
 274
 275 (* ------------------------------------------------------------------------- *)
 276 (*      Subgoal 10, 11:  Something remains                                   *)
 277 (* ------------------------------------------------------------------------- *)
 278
 279  (ABBREV_TAC `a = (x4:real)`);
 280  (ABBREV_TAC `b = (x5:real)`);
 281  (ABBREV_TAC `c = (x6:real)`);
 282
 283    (SUBGOAL_THEN
 284     `atn2 (sqrt d,&2 * p) = atn ((&8 - a - b - c) / sqrt d)`
 285      ASSUME_TAC);
 286      (SUBGOAL_THEN `&0 < sqrt d ` ASSUME_TAC);
 287      (MATCH_MP_TAC SQRT_POS_LT THEN ASM_MESON_TAC[]);
 288
 289    (ASM_MESON_TAC[ATN2_BREAKDOWN]);
 290
 291
 292    (SUBGOAL_THEN `sqrt (&4 * d) = &2 * sqrt d` ASSUME_TAC);
 293      (SUBGOAL_THEN `sqrt (&4 * d) = sqrt (&4) * sqrt d` ASSUME_TAC);
 294      (MATCH_MP_TAC SQRT_MUL);
 295      ASM_REAL_ARITH_TAC;
 296    (ASM_REWRITE_TAC[]);
 297    (AP_THM_TAC THEN AP_TERM_TAC);
 298    (REWRITE_TAC[REAL_ARITH `&4 = &2 * &2 `]);
 299    (REWRITE_TAC[MESON[SQRT_MUL;REAL_ARITH `&0 <= &2`]
 300      `sqrt (&2 * &2) = sqrt (&2) * sqrt (&2)`]);
 301    (REWRITE_TAC[GSYM POW_2]);
 302    (MATCH_MP_TAC SQRT_POW_2);
 303    REAL_ARITH_TAC;
 304
 305    (REPLICATE_TAC 7 UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC);
 306    (REPLICATE_TAC 16 UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC);
 307    (REPEAT STRIP_TAC);
 308    (ONCE_ASM_REWRITE_TAC[]);
 309
 310 (* ------------------------------------------------------------------------- *)
 311 (*      Subgoal 12:  &0 < a, b , c < &4                                      *)
 312 (* ------------------------------------------------------------------------- *)
 313
 314  (SUBGOAL_THEN `a < &4 /\ b < &4 /\ c < &4` ASSUME_TAC);
 315  (EXPAND_TAC "a" THEN EXPAND_TAC "b" THEN EXPAND_TAC "c");
 316  (ASM_REWRITE_TAC[REAL_ARITH `&4 = &2 pow 2`]);
 317  (REPEAT STRIP_TAC);
 318
 319    (MATCH_MP_TAC REAL_POW_LT2);
 320    (EXPAND_TAC "y4");
 321    (REWRITE_TAC[ARITH_RULE `~(2 = 0)`; DIST_POS_LE]);
 322    (MATCH_MP_TAC (REAL_ARITH
 323     `dist (v0:real^3,v2) = &1 /\ dist (v0,v3) = &1 /\
 324      dist (v2,v3) < dist (v0:real^3,v2) + dist (v0,v3)
 325      ==> dist (v2,v3) < &2`));
 326    STRIP_TAC;
 327    (ASM_REWRITE_TAC[]);
 328    STRIP_TAC;
 329    (ASM_REWRITE_TAC[]);
 330    (MATCH_MP_TAC (REAL_ARITH `a <= b /\ ~(a = b) ==> a < b`));
 331    (REWRITE_TAC[DIST_TRIANGLE_ALT]);
 332    (REWRITE_TAC[dist]);
 333    (MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
 334    (REWRITE_TAC[REAL_ARITH `(a + b) pow 2 = a pow 2 + b pow 2 + &2 * a * b`]);
 335    (REWRITE_TAC[NORM_POW_2]);
 336  (ABBREV_TAC `m = v0:real^3 - v2`);
 337  (ABBREV_TAC `n = v0:real^3 - v3`);
 338  (SUBGOAL_THEN `v2:real^3 - v3 = n - m` ASSUME_TAC);
 339  (EXPAND_TAC "m" THEN EXPAND_TAC "n" THEN VECTOR_ARITH_TAC);
 340  (ONCE_ASM_REWRITE_TAC[]);
 341  (REWRITE_TAC[NORM_POW_2]);
 342  (REWRITE_TAC[VECTOR_ARITH
 343   `(m - n) dot (m - n) = m dot m + n dot n - &2 * m dot n`]);
 344  (REWRITE_TAC[REAL_ARITH `a + b - &2 * c = b + a + &2 * d <=> --c = d`]);
 345  (MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
 346  (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(--x) pow 2 = x pow 2`]);
 347  (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(x * y) pow 2 = (y pow 2) * (x pow 2)`]);
 348  (REWRITE_TAC [NORM_POW_2]);
 349  (ONCE_REWRITE_TAC[VECTOR_ARITH `(n dot m) = (--n) dot (--m)`]);
 350
 351  (REWRITE_TAC[MESON[] `(a <=> b) <=> (~b <=> ~a)`; DOT_CAUCHY_SCHWARZ_EQUAL]);
 352  (EXPAND_TAC "n" THEN EXPAND_TAC "m");
 353  (ONCE_REWRITE_TAC[VECTOR_ARITH `--(x - y) = y - x:real^3`]);
 354  (ONCE_REWRITE_TAC[GSYM COLLINEAR_3]);
 355  (PURE_ONCE_REWRITE_TAC[SET_RULE `{a, b , c} = {b, a, c}`]);
 356  (ASM_REWRITE_TAC[]);
 357
 358
 359
 360    (MATCH_MP_TAC REAL_POW_LT2);
 361    (EXPAND_TAC "y5");
 362    (REWRITE_TAC[ARITH_RULE `~(2 = 0)`; DIST_POS_LE]);
 363    (MATCH_MP_TAC (REAL_ARITH
 364     `dist (v0:real^3,v1) = &1 /\ dist (v0,v3) = &1 /\
 365      dist (v1,v3) < dist (v0:real^3,v1) + dist (v0,v3)
 366      ==> dist (v1,v3) < &2`));
 367    STRIP_TAC;
 368    (ASM_REWRITE_TAC[]);
 369    STRIP_TAC;
 370    (ASM_REWRITE_TAC[]);
 371    (MATCH_MP_TAC (REAL_ARITH `a <= b /\ ~(a = b) ==> a < b`));
 372    (REWRITE_TAC[DIST_TRIANGLE_ALT]);
 373    (REWRITE_TAC[dist]);
 374    (MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
 375    (REWRITE_TAC[REAL_ARITH `(a + b) pow 2 = a pow 2 + b pow 2 + &2 * a * b`]);
 376    (REWRITE_TAC[NORM_POW_2]);
 377  (ABBREV_TAC `m = v0:real^3 - v1`);
 378  (ABBREV_TAC `n = v0:real^3 - v3`);
 379  (SUBGOAL_THEN `v1:real^3 - v3 = n - m` ASSUME_TAC);
 380  (EXPAND_TAC "m" THEN EXPAND_TAC "n" THEN VECTOR_ARITH_TAC);
 381  (ONCE_ASM_REWRITE_TAC[]);
 382  (REWRITE_TAC[NORM_POW_2]);
 383  (REWRITE_TAC[VECTOR_ARITH
 384   `(m - n) dot (m - n) = m dot m + n dot n - &2 * m dot n`]);
 385  (REWRITE_TAC[REAL_ARITH `a + b - &2 * c = b + a + &2 * d <=> --c = d`]);
 386  (MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
 387  (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(--x) pow 2 = x pow 2`]);
 388  (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(x * y) pow 2 = (y pow 2) * (x pow 2)`]);
 389  (REWRITE_TAC [NORM_POW_2]);
 390  (ONCE_REWRITE_TAC[VECTOR_ARITH `(n dot m) = (--n) dot (--m)`]);
 391
 392  (REWRITE_TAC[MESON[] `(a <=> b) <=> (~b <=> ~a)`; DOT_CAUCHY_SCHWARZ_EQUAL]);
 393  (EXPAND_TAC "n" THEN EXPAND_TAC "m");
 394  (ONCE_REWRITE_TAC[VECTOR_ARITH `--(x - y) = y - x:real^3`]);
 395  (ONCE_REWRITE_TAC[GSYM COLLINEAR_3]);
 396  (PURE_ONCE_REWRITE_TAC[SET_RULE `{a, b , c} = {b, c, a}`]);
 397  (ASM_REWRITE_TAC[]);
 398
 399
 400
 401    (MATCH_MP_TAC REAL_POW_LT2);
 402    (EXPAND_TAC "y6");
 403    (REWRITE_TAC[ARITH_RULE `~(2 = 0)`; DIST_POS_LE]);
 404    (MATCH_MP_TAC (REAL_ARITH
 405     `dist (v0:real^3,v1) = &1 /\ dist (v0,v3) = &1 /\
 406      dist (v1,v3) < dist (v0:real^3,v1) + dist (v0,v3)
 407      ==> dist (v1,v3) < &2`));
 408    STRIP_TAC;
 409    (ASM_REWRITE_TAC[]);
 410    STRIP_TAC;
 411    (ASM_REWRITE_TAC[]);
 412    (MATCH_MP_TAC (REAL_ARITH `a <= b /\ ~(a = b) ==> a < b`));
 413    (REWRITE_TAC[DIST_TRIANGLE_ALT]);
 414    (REWRITE_TAC[dist]);
 415    (MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
 416    (REWRITE_TAC[REAL_ARITH `(a + b) pow 2 = a pow 2 + b pow 2 + &2 * a * b`]);
 417    (REWRITE_TAC[NORM_POW_2]);
 418  (ABBREV_TAC `m = v0:real^3 - v1`);
 419  (ABBREV_TAC `n = v0:real^3 - v2`);
 420  (SUBGOAL_THEN `v1:real^3 - v2 = n - m` ASSUME_TAC);
 421  (EXPAND_TAC "m" THEN EXPAND_TAC "n" THEN VECTOR_ARITH_TAC);
 422  (ONCE_ASM_REWRITE_TAC[]);
 423  (REWRITE_TAC[NORM_POW_2]);
 424  (REWRITE_TAC[VECTOR_ARITH
 425   `(m - n) dot (m - n) = m dot m + n dot n - &2 * m dot n`]);
 426  (REWRITE_TAC[REAL_ARITH `a + b - &2 * c = b + a + &2 * d <=> --c = d`]);
 427  (MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
 428  (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(--x) pow 2 = x pow 2`]);
 429  (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(x * y) pow 2 = (y pow 2) * (x pow 2)`]);
 430  (REWRITE_TAC [NORM_POW_2]);
 431  (ONCE_REWRITE_TAC[VECTOR_ARITH `(n dot m) = (--n) dot (--m)`]);
 432
 433  (REWRITE_TAC[MESON[] `(a <=> b) <=> (~b <=> ~a)`; DOT_CAUCHY_SCHWARZ_EQUAL]);
 434  (EXPAND_TAC "n" THEN EXPAND_TAC "m");
 435  (ONCE_REWRITE_TAC[VECTOR_ARITH `--(x - y) = y - x:real^3`]);
 436  (ONCE_REWRITE_TAC[GSYM COLLINEAR_3]);
 437  (PURE_ONCE_REWRITE_TAC[SET_RULE `{a, b , c} = {b, c, a}`]);
 438  (ASM_REWRITE_TAC[]);
 439
 440
 441
 442  (SUBGOAL_THEN `&0 < a /\ &0 < b /\ &0 < c` ASSUME_TAC);
 443  (EXPAND_TAC "a" THEN EXPAND_TAC "b" THEN EXPAND_TAC "c");
 444  (ASM_REWRITE_TAC[]);
 445
 446  STRIP_TAC;
 447
 448    (MATCH_MP_TAC REAL_POW_LT);
 449    (EXPAND_TAC "y4");
 450    (REWRITE_TAC[dist]);
 451    (MATCH_MP_TAC (NORM_ARITH `~(v2 = v3) ==> &0 < norm (v2 - v3)`));
 452    STRIP_TAC;
 453    (MATCH_MP_TAC (MESON[]
 454      ` collinear {v0:real^3, v2, v3} /\ ~ collinear {v0, v2, v3} ==> F`));
 455    (CONJ_TAC);
 456
 457    (ASM_REWRITE_TAC[]);
 458    (REWRITE_TAC[SET_RULE `{a, b , b} = {a, b}`]);
 459    (ASM_MESON_TAC[COLLINEAR_2]);
 460    (ASM_MESON_TAC[]);
 461
 462  STRIP_TAC;
 463    (MATCH_MP_TAC REAL_POW_LT);
 464    (EXPAND_TAC "y5");
 465    (REWRITE_TAC[dist]);
 466    (MATCH_MP_TAC (NORM_ARITH `~(v1 = v3) ==> &0 < norm (v1 - v3)`));
 467    STRIP_TAC;
 468    (MATCH_MP_TAC (MESON[]
 469      ` collinear {v0:real^3, v3, v1} /\ ~ collinear {v0, v3, v1} ==> F`));
 470    (CONJ_TAC);
 471
 472    (ASM_REWRITE_TAC[]);
 473    (REWRITE_TAC[SET_RULE `{a, b , b} = {a, b}`]);
 474    (ASM_MESON_TAC[COLLINEAR_2]);
 475    (ASM_MESON_TAC[]);
 476
 477
 478    (MATCH_MP_TAC REAL_POW_LT);
 479    (EXPAND_TAC "y6");
 480    (REWRITE_TAC[dist]);
 481    (MATCH_MP_TAC (NORM_ARITH `~(v1 = v2) ==> &0 < norm (v1 - v2)`));
 482    STRIP_TAC;
 483    (MATCH_MP_TAC (MESON[]
 484      ` collinear {v0:real^3, v1, v2} /\ ~ collinear {v0, v1, v2} ==> F`));
 485    (CONJ_TAC);
 486
 487    (REWRITE_TAC[ASSUME `v1 :real^3 = v2`]);
 488    (REWRITE_TAC[SET_RULE `{a, b , b} = {a, b}`]);
 489    (ASM_MESON_TAC[COLLINEAR_2]);
 490    (ASM_MESON_TAC[]);
 491
 492 (* ------------------------------------------------------------------------- *)
 493 (*      FINISH the EULER LEMMA                                               *)
 494 (* ------------------------------------------------------------------------- *)
 495
 496  (REPLICATE_TAC 3 UP_ASM_TAC);
 497  (REPLICATE_TAC 9 DEL_TAC);
 498  (UP_ASM_TAC THEN REPLICATE_TAC 13 DEL_TAC THEN UP_ASM_TAC);
 499  (REPEAT DEL_TAC THEN REPEAT DISCH_TAC);
 500  (ASM_REWRITE_TAC[]);
 501  (MP_TAC DERIVATIVE_WRT_A_Euler_lemma THEN LET_TAC);
 502  (ASM_MESON_TAC[])]);;
 503
 504
 505 let euler_triangle_t = `!v0 v1 v2 v3:real^3.
 506     let p = euler_p v0 v1 v2 v3 in
 507     let (x1,x2,x3,x4,x5,x6) = xlist v0 v1 v2 v3 in
 508     let alpha1 = dihV v0 v1 v2 v3 in
 509     let alpha2 = dihV v0 v2 v3 v1 in
 510     let alpha3 = dihV v0 v3 v1 v2 in
 511     let d = delta_x x1 x2 x3 x4 x5 x6 in
 512     ((&0 < d) ==>
 513       (alpha1 + alpha2 + alpha3 - pi = pi - &2 * atn2(sqrt(d), (&2 * p))))`;;
 514
 515 let EULER_TRIANGLE = prove_by_refinement (euler_triangle_t ,
 516   [MATCH_MP_TAC EULER_FORMULA_RESCALE;
 517    MP_TAC EULER_ANGLE_SUM_rescal;
 518    MESON_TAC[]]);;
 519
 520
 521
 522 end;;