text_formalization/trigonometry/trig1.hl

   1 (* ========================================================================== *)\r
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)\r
   3 (*                                                                            *)\r
   4 (* Chapter: Trigonometry                                                             *)\r
   5 (* Author: Jason Rute, Thomas C. Hales                                                    *)\r
   6 (* Date: 2010-02-09                                                           *)\r
   7 (* ========================================================================== *)\r
   8 \r
   9 \r
  10 \r
  11 \r
  12 \r
  13 module type Trigonometry1_type = sig\r
  14   (* ADD *)\r
  15 \r
  16 end;;\r
  17 \r
  18 (* \r
  19 Formal Proofs Blueprint Chapter  on Trigonometry \r
  20 some proofs copied from John Harrison.\r
  21 *)\r
  22 \r
  23 flyspeck_needs "general/sphere.hl";;\r
  24 \r
  25 \r
  26 module  Trigonometry1 (* :  Trigonometry1_type *) = struct\r
  27 \r
  28   let atn2 = Sphere.atn2;; \r
  29   let arclength = Sphere.arclength;; \r
  30   let ups_x = Sphere.ups_x;;\r
  31 \r
  32 prioritize_real();;\r
  33 \r
  34 \r
  35 (* This is close to CIRCLE_SINCOS *)\r
  36 \r
  37 let atn2_spec_t = `!x y. ?r. ((-- pi < atn2(x, y)) /\ (atn2(x,y) <= pi) /\\r
  38      (x = r* (cos(atn2(x,y)))) /\ (y = r* (sin (atn2( x, y)))) /\ \r
  39      (&0 <= r))`;;\r
  40 \r
  41 let acs_atn2_t = `!y. (-- &1 <= y /\ y <=  &1) ==> (acs y = pi/(&2) - atn2(sqrt(&1 - y pow 2),y))`;;\r
  42 \r
  43 let arcVarc_t = `!u v w:real^3. ~(u=v) /\ ~(u=w) ==> arcV u v w = arclength (dist( u, v)) (dist( u, w)) (dist( v, w))`;;\r
  44 \r
  45 let law_of_cosines_t = `!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>\r
  46    ((c pow 2) = (a pow 2) + (b pow 2) - &2 * a * b * (cos(arclength a b c)))`;;\r
  47 \r
  48 let law_of_sines_t = `!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>\r
  49    (&2 * a * b * sin (arclength a b c) = sqrt(ups_x (a pow 2) (b pow 2) (c pow 2)))`;;\r
  50 \r
  51 let cross_mag_t = `!u v. norm (u cross v) = (norm u) * (norm v) * sin(arcV (vec 0) u v)`;;\r
  52 \r
  53 let cross_skew_t = `!u v. (u cross v) = -- (v cross u)`;;\r
  54 \r
  55 let cross_triple_t = `!u v w.  (u cross v) dot w =  (v cross w) dot u`;;\r
  56 \r
  57 \r
  58 (* law of cosines *)\r
  59 \r
  60 let spherical_loc_t = `!v0 va vb vc:real^3.\r
  61   ~(collinear {v0,va,vc}) /\ ~(collinear {v0,vb,vc}) ==>\r
  62         (\r
  63     let gamma = dihV v0 vc va vb in\r
  64     let a = arcV v0 vb vc in\r
  65     let b = arcV v0 va vc in\r
  66     let c = arcV v0 va vb in\r
  67       (cos(gamma) = (cos(c) - cos(a)*cos(b))/(sin(a)*sin(b))))`;;\r
  68 \r
  69 let spherical_loc2_t = `!v0 va vb vc:real^3.\r
  70  ~(collinear {v0,va,vc}) /\ ~(collinear {v0,vb,vc}) ==>\r
  71         (\r
  72     let alpha = dihV v0 va vb vc in\r
  73     let beta = dihV v0 vb va vc in\r
  74     let gamma = dihV v0 vc vb va in\r
  75     let c = arcV v0 va vb in\r
  76       (cos(c) = (cos(gamma) + cos(alpha)*cos(beta))/(sin(alpha)*sin(beta))))`;;\r
  77 \r
  78 let dih_formula_t = `!v0 v1 v2 v3:real^3. \r
  79    ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) ==>\r
  80    (\r
  81    let (x1,x2,x3,x4,x5,x6) = xlist v0 v1 v2 v3 in\r
  82     (dihV v0 v1 v2 v3  = dih_x x1 x2 x3 x4 x5 x6)\r
  83    )`;;\r
  84 \r
  85 let dih_x_acs_t = `!x1 x2 x3 x4 x5 x6.\r
  86    (&0 < ups_x x1 x2 x6) /\ (&0 < ups_x x1 x3 x5) /\ (&0 <= delta_x x1 x2 x3 x4 x5 x6) /\ (&0 <= x1) ==>\r
  87    dih_x x1 x2 x3 x4 x5 x6 = acs ((delta_x4 x1 x2 x3 x4 x5 x6)/\r
  88   ((sqrt (ups_x x1 x2 x6)) * (sqrt (ups_x x1 x3 x5))))`;;\r
  89 \r
  90 let beta_cone_t = `!v0 v1 v2 v3:real^3.\r
  91     ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) /\ \r
  92     (dihV v0 v3 v1 v2 = pi/(&2)) ==>\r
  93     (dihV v0 v1 v2 v3 = beta (arcV v0 v1 v3) (arcV v0 v1 v2))`;;\r
  94 \r
  95 let euler_triangle_t = `!v0 v1 v2 v3:real^3. \r
  96     let p = euler_p v0 v1 v2 v3 in\r
  97     let (x1,x2,x3,x4,x5,x6) = xlist v0 v1 v2 v3 in\r
  98     let alpha1 = dihV v0 v1 v2 v3 in\r
  99     let alpha2 = dihV v0 v2 v3 v1 in\r
 100     let alpha3 = dihV v0 v3 v1 v2 in\r
 101     let d = delta_x x1 x2 x3 x4 x5 x6 in\r
 102     ((&0 < d) ==>\r
 103       (alpha1 + alpha2 + alpha3 - pi = pi - &2 * atn2(sqrt(d), (&2 * p))))`;;\r
 104 \r
 105 let polar_cycle_rotate_t = `!V psi u f.\r
 106        (!x y. f (x,y) = (x*cos psi + y*sin psi, -- x*sin psi + y*cos psi)) /\\r
 107        FINITE V  /\ V u ==>\r
 108        (polar_cycle (IMAGE f V) (f u) =  f (polar_cycle V u))`;;\r
 109 \r
 110 let thetaij_t = `!theta1 theta2 k12 k21 theta12 theta21.\r
 111      (&0 <= theta1) /\ (theta1 < &2 * pi) /\ (&0 <= theta2) /\ (theta2 < &2 * pi) /\\r
 112      (theta12 = theta2 - theta1 + &2 * pi * (&k12)) /\\r
 113      (theta21 = theta1 - theta2 + &2 * pi * (&k21)) /\\r
 114      (&0 <= theta12) /\ (theta12 < &2 * pi) /\\r
 115      (&0 <= theta21) /\ (theta21 < &2 * pi) ==>\r
 116      ((theta12+theta21) = (if (theta1=theta2) then (&0) else (&2 * pi)))`;;\r
 117 \r
 118 (* JMR: Changed `polar_angle (FST u) (SND u)` to `Arg(complex u)` *)\r
 119 \r
 120 let thetapq_wind_t = `!W n thetapq kpq. \r
 121     (!x y. (W (x,y) ==> (~(x= &0) /\ ~(y = &0)))) /\\r
 122     (W HAS_SIZE n) /\\r
 123     (!u v. W u /\ W v ==> \r
 124        ((thetapq u v = Arg(complex v) -  Arg(complex u) + &2 * pi * kpq u v) /\  (&0 <= thetapq u v) /\ (thetapq u v < &2 * pi)))\r
 125     ==>\r
 126     ((!u i j. (W u /\ (0 <= i) /\ (i <= j) /\ (j < n)) ==>\r
 127         thetapq u (ITER i (polar_cycle W) u) + thetapq (ITER i (polar_cycle W) u) (ITER j (polar_cycle W) u) = thetapq u (ITER j (polar_cycle W) u)) /\\r
 128     ((!u v.  (W u /\ W v) ==> (Arg(complex u) = Arg(complex v))) \/\r
 129      (!u. (W u)  ==> (sum(0 .. n-1) (\i. thetapq (ITER i (polar_cycle W) u) (ITER (SUC i) (polar_cycle W) u))  = &2 * pi)) ))`;;\r
 130 \r
 131 let zenith_t = `!u v w:real^3.  ~(u=v) /\ ~(w = v)  ==>\r
 132    (?u' r phi e3.\r
 133         (phi = arcV v u w) /\ (r = dist( u, v)) /\ ((dist( w, v)) % e3 = (w-v)) /\\r
 134   ( u' dot e3 = &0) /\ (u = v + u' + (r*cos(phi)) % e3))`;;\r
 135 \r
 136 (* spherical_coord_t deprecated, replaced with Harrison's SPHERICAL_COORDINATES theorem,\r
 137     which is worded slightly differently.\r
 138 *)\r
 139 \r
 140 let polar_coord_zenith_t = `!u v w u' n.\r
 141   ~(collinear {u,v,w}) /\ (aff {u,v,w} u') /\ ~(u' = v) /\\r
 142   (n = (w - v) cross (u - v)) ==>\r
 143    (arcV v (v + n) u' = pi/ (&2))`;;\r
 144 \r
 145 let azim_pair_t = `!v w w1 w2.\r
 146     let a1 = azim v w w1 w2 in\r
 147     let a2 = azim v w w2 w1 in\r
 148     (cyclic_set {w1,w2} v w) ==> \r
 149       (a1 + a2 = (if (a1 = &0) then (&0) else (&2 * pi)))`;;\r
 150 \r
 151 let azim_cycle_sum_t = `!W v w n. \r
 152    (cyclic_set W v w) /\\r
 153    (W HAS_SIZE n) ==>\r
 154    (!p i j. (W p /\ (0 <= i) /\ (i <= j) /\ (j < n)) ==> \r
 155        ((!q.  W q ==> (azim v w p q = &0) ) \/\r
 156        (sum(0 .. n-1) (\i. azim v w (ITER i (azim_cycle W v w) p) (ITER (SUC i) (azim_cycle W v w) p)) = &2 * pi   )))`;;\r
 157 \r
 158 let dih_azim_t = `!v w v1 v2. \r
 159    ~(collinear {v,w,v1}) /\ ~(collinear {v,w,v2}) ==>\r
 160   (cos(azim v w v1 v2) = cos(dihV v w v1 v2))`;;\r
 161 \r
 162 let sph_triangle_ineq_t = `!p u v w:real^3.\r
 163    ~(collinear {p,u,w}) /\ ~(collinear {p,u,v}) /\ ~(collinear {p,v,w}) ==>\r
 164   (arcV p u w <= arcV p u v + arcV p v w)`;;\r
 165 \r
 166 let sph_triangle_ineq_sum_t = `!p:real^3 u r.\r
 167    (!i. (i < r) ==> ~(collinear {p,u i, u (SUC i)})) /\\r
 168    ~(collinear {p,u 0, u r}) ==>\r
 169    (arcV p (u 0) (u r) <= sum(0 .. r-1) (\i. arcV p (u i) (u (SUC i))))`;;\r
 170 \r
 171 let azim_t = `!v w w1 w2 e1 e2 e3.\r
 172          ?psi h1 h2 r1 r2.\r
 173                  ~collinear {v, w, w1} /\\r
 174                  ~collinear {v, w, w2} /\\r
 175                  orthonormal e1 e2 e3 /\\r
 176                  (dist( w, v) % e3 = w - v)\r
 177              ==> &0 <= azim v w w1 w2 /\\r
 178                  azim v w w1 w2 < &2 * pi /\\r
 179                  &0 < r1 /\\r
 180                  &0 < r2 /\\r
 181                  w1 =\r
 182                  (r1 * cos psi) % e1 + (r1 * sin psi) % e2 + h1 % (w - v) /\\r
 183                  (w2 =\r
 184                  (r2 * cos (psi + azim v w w1 w2)) % e1 +\r
 185                  (r2 * sin (psi + azim v w w1 w2)) % e2 +\r
 186                  h2 % (w - v))`;;\r
 187 \r
 188 (* signature for trig theorems.\r
 189    This is the list of theorems that should be provided by\r
 190    an implementation of the blueprint on trig.\r
 191    The signature can be extended, but care needs to made\r
 192    in removing anything, because it may create incompatibilities\r
 193    with other pieces of code. *)\r
 194 \r
 195 (* In every case, there is a term giving the precise theorem to\r
 196    be proved *)\r
 197 \r
 198 \r
 199 module type Trigsig = sig\r
 200   val atn2_spec : thm (* atn2_spec_t  *)\r
 201   val acs_atn2: thm  (* acs_atn2_t *)\r
 202   val arcVarc : thm (*  arcVarc_t *)\r
 203   val law_of_cosines : thm (*  law_of_cosines_t *)\r
 204   val law_of_sines : thm (*  law_of_sines_t *)\r
 205   val cross_mag : thm (*  cross_mag_t *)\r
 206   val cross_skew : thm (*  cross_skew_t *)\r
 207   val cross_triple : thm (*  cross_triple_t *)\r
 208   val spherical_loc : thm (*  spherical_loc_t *)\r
 209   val spherical_loc2 : thm (*  spherical_loc2_t *)\r
 210   val dih_formula : thm (*  dih_formula_t *)\r
 211   val dih_x_acs : thm (*  dih_x_acs_t *)\r
 212   val beta_cone : thm (*  beta_cone_t *)\r
 213   val euler_triangle : thm (*  euler_triangle_t *)\r
 214 (*   val polar_coords : thm (*  polar_coords_t *) *)\r
 215   val polar_cycle_rotate : thm (*  polar_cycle_rotate_t *)\r
 216   val thetaij : thm (*  thetaij_t *)\r
 217   val thetapq_wind : thm (*  thetapq_wind_t *)\r
 218   val zenith : thm (*  zenith_t *)\r
 219 (*  val spherical_coord : thm (*  spherical_coord_t *) *)\r
 220   val polar_coord_zenith : thm (*  polar_coord_zenith_t *)\r
 221   val azim_pair : thm (*  azim_pair_t *)\r
 222   val azim_cycle_sum : thm (*  azim_cycle_sum_t *)\r
 223   val dih_azim : thm (*  dih_azim_t *)\r
 224   val sph_triangle_ineq : thm (*  sph_triangle_ineq_t *)\r
 225   val sph_triangle_ineq_sum : thm (*  sph_triangle_ineq_sum_t *)\r
 226   val azim : thm (*  azim_t   *)\r
 227 end;;\r
 228 \r
 229 (* Here is a single axiom that permits a quick implementation of the\r
 230    module with the given signature.\r
 231    The axiom can be used so that the proofs in different chapters can\r
 232    proceed independently.  *)\r
 233 \r
 234 (*\r
 235 let trig_term_list = new_definition (mk_eq (`trig_term:bool`, (list_mk_conj\r
 236    [\r
 237   atn2_spec_t  ;\r
 238   acs_atn2_t ;\r
 239   arcVarc_t ;\r
 240   law_of_cosines_t ;\r
 241   law_of_sines_t ;\r
 242   cross_mag_t ;\r
 243   cross_skew_t ;\r
 244   cross_triple_t ;\r
 245   spherical_loc_t ;\r
 246   spherical_loc2_t ;\r
 247   dih_formula_t ;\r
 248   dih_x_acs_t ;\r
 249   beta_cone_t ;\r
 250   euler_triangle_t ;\r
 251   polar_cycle_rotate_t ;\r
 252   thetaij_t ;\r
 253   thetapq_wind_t ;\r
 254   zenith_t ;\r
 255   polar_coord_zenith_t ;\r
 256   azim_pair_t ;\r
 257   azim_cycle_sum_t ;\r
 258   dih_azim_t ;\r
 259   sph_triangle_ineq_t ;\r
 260   sph_triangle_ineq_sum_t ;\r
 261   azim_t;\r
 262    ])));;\r
 263 *)\r
 264 \r
 265   \r
 266   (* ---------------------------------------------------------------------- *)\r
 267   (* These are theorems proved in HOL Light, but not in the                 *)\r
 268         (* Multivariate files.  Unless noted, all proofs by John Harrison.        *)\r
 269   (* ---------------------------------------------------------------------- *)\r
 270         \r
 271         (* REAL_LE_POW_2 is in HOL-Light Examples/transc.ml.  *)\r
 272         (* Also called REAL_LE_SQUARE_POW in Examples/analysis.ml. *)\r
 273         \r
 274   let REAL_LE_POW_2 = prove\r
 275    (`!x. &0 <= x pow 2`,\r
 276     REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE]);;\r
 277 \r
 278   (* REAL_DIV_MUL2 is in HOL-Light Examples/analysis.ml.  *)\r
 279   (* Proof in now trivial *)\r
 280         \r
 281         let REAL_DIV_MUL2 = REAL_FIELD\r
 282     `!x z. ~(x = &0) /\ ~(z = &0) ==> !y. y / z = (x * y) / (x * z)`;;\r
 283         \r
 284   (* ---------------------------------------------------------------------- *)\r
 285   (* Useful theorems about real numbers.                                    *)\r
 286   (* ---------------------------------------------------------------------- *)\r
 287   \r
 288   let REAL_LT_MUL_3 = prove\r
 289    (`!x y z. &0 < x /\ &0 < y /\ &0 < z ==> &0 < x * y * z`,\r
 290     REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC [] THEN\r
 291     MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC []);;\r
 292 \r
 293   let SQRT_MUL_L = prove\r
 294    (`!x y. &0 <= x /\ &0 <= y ==> x * sqrt y = sqrt(x pow 2 * y)`,\r
 295     REPEAT STRIP_TAC THEN ASM_SIMP_TAC [REAL_LE_POW_2; SQRT_MUL; POW_2_SQRT]);;\r
 296 \r
 297   let SQRT_MUL_R = prove\r
 298    (`!x y. &0 <= x /\ &0 <= y ==> sqrt x * y = sqrt(x * y pow 2)`,\r
 299     REPEAT STRIP_TAC THEN ASM_SIMP_TAC [REAL_LE_POW_2; SQRT_MUL; POW_2_SQRT]);;\r
 300   \r
 301   (* ---------------------------------------------------------------------- *)\r
 302   (* Basic trig results not included in Examples/transc.ml                  *)\r
 303   (* ---------------------------------------------------------------------- *)\r
 304 \r
 305   (* Next two proofs similar to TAN_PERIODIC_NPI in *)\r
 306   (* Examples/transc.ml by John Harrison *)\r
 307   (* They are no longer needed, but may be useful later. *)\r
 308         \r
 309   let SIN_PERIODIC_N2PI = prove\r
 310    (`!x n. sin(x + &n * (&2 * pi)) = sin(x)`,\r
 311     GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID] THEN\r
 312     REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_ADD_RDISTRIB; REAL_MUL_LID] THEN\r
 313     ASM_REWRITE_TAC[REAL_ADD_ASSOC; SIN_PERIODIC]);;\r
 314   \r
 315   let COS_PERIODIC_N2PI = prove\r
 316    (`!x n. cos(x + &n * (&2 * pi)) = cos(x)`,\r
 317     GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID] THEN\r
 318     REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_ADD_RDISTRIB; REAL_MUL_LID] THEN\r
 319     ASM_REWRITE_TAC[REAL_ADD_ASSOC; COS_PERIODIC]);;\r
 320 \r
 321   let CIRCLE_SINCOS_PI = prove\r
 322    (`!x y. (x pow 2 + y pow 2 = &1) ==> \r
 323        ?t. (--pi < t /\ t <= pi) /\ ((x = cos(t)) /\ (y = sin(t)))`,\r
 324                 ASM_MESON_TAC [CIRCLE_SINCOS; SINCOS_PRINCIPAL_VALUE]);;\r
 325 \r
 326   let SIN_NEGPOS_PI = prove \r
 327    (`!x. (--pi < x /\ x <= pi) ==>\r
 328          (sin x < &0 <=> --pi < x /\ x < &0) /\\r
 329          (sin x = &0 <=> (x = &0 \/ x = pi)) /\\r
 330          (&0 < sin x <=> &0 < x /\ x < pi)`,\r
 331     STRIP_TAC THEN STRIP_TAC THEN SUBGOAL_THEN\r
 332       `if (sin x < &0) then (sin x < &0 <=> --pi < x /\ x < &0) else\r
 333        if (sin x = &0) then (sin x = &0 <=> (x = &0 \/ x = pi)) else\r
 334        (&0 < sin x <=> &0 < x /\ x < pi)` MP_TAC THENL\r
 335     [ SUBGOAL_TAC "a" `--pi < x /\ x < &0 ==> sin x < &0`\r
 336       [ MP_TAC (REWRITE_RULE [SIN_NEG] (SPEC `--x:real` SIN_POS_PI)) THEN\r
 337         REAL_ARITH_TAC ] THEN\r
 338       SUBGOAL_TAC "b" `x = &0 ==> sin x = &0`\r
 339       [ STRIP_TAC THEN ASM_REWRITE_TAC [SIN_0] ] THEN\r
 340       SUBGOAL_TAC "c" `x = pi ==> sin x = &0`\r
 341       [ STRIP_TAC THEN ASM_REWRITE_TAC [SIN_PI] ] THEN\r
 342       LABEL_TAC "d" (SPEC `x:real` SIN_POS_PI) THEN\r
 343       REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;\r
 344       REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ]);;\r
 345 \r
 346   let COS_NEGPOS_PI = prove\r
 347    (`!x. (--pi < x /\ x <= pi) ==>\r
 348          (cos x < &0 <=> (--pi < x /\ x < --(pi / &2)) \/ \r
 349                          (pi / &2 < x /\ x <= pi)) /\\r
 350          (cos x = &0 <=> (x = --(pi / &2) \/ x = pi / &2)) /\\r
 351          (&0 < cos x <=> --(pi / &2) < x /\ x < pi / &2)`,\r
 352     STRIP_TAC THEN STRIP_TAC THEN SUBGOAL_THEN\r
 353       `if (cos x < &0) then (cos x < &0 <=> (--pi < x /\ x < --(pi / &2)) \/ \r
 354                             (pi / &2 < x /\ x <= pi)) else\r
 355        if (cos x = &0) then \r
 356        (cos x = &0 <=> (x = --(pi / &2) \/ x = pi / &2)) else\r
 357        (&0 < cos x <=> --(pi / &2) < x /\ x < pi / &2)` MP_TAC THENL\r
 358     [ SUBGOAL_TAC "a" `--pi < x /\ x < --(pi / &2) ==> cos x < &0`\r
 359       [ MP_TAC (REWRITE_RULE [COS_PERIODIC_PI] \r
 360                (SPEC `x + pi:real` COS_POS_PI2)) THEN\r
 361         REAL_ARITH_TAC ] THEN\r
 362       SUBGOAL_TAC "b" `pi / &2 < x /\ x <= pi ==> cos x < &0`\r
 363       [ MP_TAC (REWRITE_RULE [SIN_NEG; GSYM COS_SIN] \r
 364                (SPEC `--(pi / &2 - x)` SIN_POS_PI2)) THEN\r
 365         SUBGOAL_TAC "b1" `x = pi ==> cos x < &0` \r
 366         [ STRIP_TAC THEN ASM_REWRITE_TAC [COS_PI; REAL_ARITH `&0 < &1`] THEN\r
 367           REAL_ARITH_TAC ] THEN\r
 368         POP_ASSUM MP_TAC THEN REAL_ARITH_TAC ] THEN\r
 369       SUBGOAL_TAC "c" `x = --(pi / &2) ==> cos x = &0`\r
 370       [ STRIP_TAC THEN ASM_REWRITE_TAC [COS_NEG; COS_PI2] ] THEN\r
 371       SUBGOAL_TAC "d" `x = pi / &2 ==> cos x = &0`\r
 372       [ STRIP_TAC THEN ASM_REWRITE_TAC [COS_PI2] ] THEN\r
 373       LABEL_TAC "e" (SPEC `x:real` COS_POS_PI) THEN\r
 374       REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;\r
 375       REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ]);;\r
 376 \r
 377   \r
 378   (* ----------------------------------------------------------------------- *)\r
 379   (* Theory of atan_2 function. See sphere.hl for the definiton. *)\r
 380   (* ----------------------------------------------------------------------- *)\r
 381   \r
 382   (* lemma:atn2_spec *)\r
 383    \r
 384   let dist_lemma = prove\r
 385    (`!x y. ~(x = &0) \/ ~(y = &0) ==> \r
 386       (x / sqrt(x pow 2 + y pow 2)) pow 2 +\r
 387       (y / sqrt(x pow 2 + y pow 2)) pow 2 = &1 /\\r
 388       &0 < sqrt(x pow 2 + y pow 2)`,\r
 389     STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN\r
 390     SUBGOAL_TAC "sum_pos" `&0 < x pow 2 + y pow 2 /\ &0 <= x pow 2 + y pow 2`\r
 391     [ MP_TAC (SPEC `x:real` REAL_LE_POW_2) THEN \r
 392       MP_TAC (SPEC `y:real` REAL_LE_POW_2) THEN\r
 393       IMP_RES_THEN MP_TAC (SPECL [`x:real`; `2`] REAL_POW_NZ) THEN \r
 394       IMP_RES_THEN MP_TAC (SPECL [`y:real`; `2`] REAL_POW_NZ) THEN \r
 395       REAL_ARITH_TAC ] THEN\r
 396     POP_ASSUM MP_TAC THEN STRIP_TAC THEN \r
 397     ASM_SIMP_TAC [REAL_POW_DIV; SQRT_POW_2; SQRT_POS_LT] THEN\r
 398     POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN\r
 399     CONV_TAC REAL_FIELD);;\r
 400   \r
 401   let ATAN2_EXISTS = prove \r
 402    (`!x y. ?t. (--pi < t /\ t <= pi) /\\r
 403          x = sqrt(x pow 2 + y pow 2) * cos t /\\r
 404          y = sqrt(x pow 2 + y pow 2) * sin t`,\r
 405     REPEAT STRIP_TAC THEN ASM_CASES_TAC `(x = &0) /\ (y = &0)` THENL\r
 406     [ ASM_REWRITE_TAC [(SPEC `2` REAL_POW_ZERO)] THEN \r
 407       NUM_REDUCE_TAC THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN \r
 408       REWRITE_TAC [SQRT_0] THEN EXISTS_TAC `pi` THEN MP_TAC PI_POS THEN\r
 409       REAL_ARITH_TAC ;\r
 410       IMP_RES_THEN STRIP_ASSUME_TAC \r
 411       (REWRITE_RULE [TAUT `(~A \/ ~B) <=> ~(A /\ B)`] dist_lemma) THEN\r
 412       IMP_RES_THEN STRIP_ASSUME_TAC CIRCLE_SINCOS_PI THEN \r
 413       POP_ASSUM (MP_TAC o GSYM) THEN POP_ASSUM (MP_TAC o GSYM) THEN\r
 414       STRIP_TAC THEN STRIP_TAC THEN EXISTS_TAC `t:real` THEN \r
 415       ASM_REWRITE_TAC [] THEN\r
 416       POP_ASSUM (K ALL_TAC) THEN POP_ASSUM (K ALL_TAC) THEN \r
 417       POP_ASSUM (K ALL_TAC) THEN POP_ASSUM (K ALL_TAC) THEN\r
 418       POP_ASSUM MP_TAC THEN CONV_TAC REAL_FIELD ]);;\r
 419   \r
 420   (* The official Kepler definition (atn2) is different, but it was easier  *)\r
 421   (* to start with this one and prove it is equivalent.                      *)\r
 422   \r
 423   let ATAN2_TEMP_DEF = new_definition\r
 424     `atan2_temp (x,y) = if (x = &0 /\ y = &0) \r
 425                         then pi \r
 426                         else @t. (--pi < t /\ t <= pi) /\\r
 427                                  x = sqrt(x pow 2 + y pow 2) * cos t /\\r
 428                                  y = sqrt(x pow 2 + y pow 2) * sin t`;;\r
 429                      \r
 430   let ATAN2_TEMP = prove\r
 431    (`!x y. (--pi < atan2_temp (x,y) /\ atan2_temp (x,y) <= pi) /\\r
 432            x = sqrt(x pow 2 + y pow 2) * cos (atan2_temp (x,y)) /\\r
 433            y = sqrt(x pow 2 + y pow 2) * sin (atan2_temp (x,y))`,\r
 434     STRIP_TAC THEN STRIP_TAC THEN REWRITE_TAC [ATAN2_TEMP_DEF] THEN\r
 435     COND_CASES_TAC THENL\r
 436     [ ASM_REWRITE_TAC [(SPEC `2` REAL_POW_ZERO)] THEN \r
 437       NUM_REDUCE_TAC THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN \r
 438       REWRITE_TAC [SQRT_0] THEN MP_TAC PI_POS THEN\r
 439       REAL_ARITH_TAC ; \r
 440       REWRITE_TAC [(SELECT_RULE (SPECL [`x:real`;`y:real`] ATAN2_EXISTS))]]);;\r
 441 \r
 442   let ATAN2_TEMP_SPEC = prove\r
 443    (`!x y. ?r. ((-- pi < atan2_temp(x, y)) /\ (atan2_temp(x,y) <= pi) /\\r
 444        (x = r* (cos(atan2_temp(x,y)))) /\ (y = r* (sin (atan2_temp( x, y)))) /\ \r
 445        (&0 <= r))`,\r
 446     STRIP_TAC THEN STRIP_TAC THEN EXISTS_TAC `sqrt(x pow 2 + y pow 2)` THEN\r
 447     REWRITE_TAC [ATAN2_TEMP] THEN SUBGOAL_TAC "sum_pos" `&0 <= x pow 2 + y pow 2`\r
 448     [ MP_TAC (SPEC `x:real` REAL_LE_POW_2) THEN \r
 449       MP_TAC (SPEC `y:real` REAL_LE_POW_2) THEN\r
 450       REAL_ARITH_TAC ] THEN\r
 451     MP_TAC (SPEC `x pow 2 + y pow 2` SQRT_POS_LE) THEN POP_ASSUM MP_TAC THEN\r
 452     REAL_ARITH_TAC);;\r
 453       \r
 454   let ATAN2_TEMP_BREAKDOWN = prove\r
 455    (`!x y. (&0 < x ==> atan2_temp(x,y) = atn(y / x)) /\\r
 456            (&0 < y ==> atan2_temp(x,y) = pi / &2 - atn(x / y)) /\\r
 457            (y < &0 ==> atan2_temp(x,y) = --(pi / &2) - atn(x / y)) /\\r
 458            (y = &0 /\ x <= &0 ==> atan2_temp(x,y) = pi)`,\r
 459     REPEAT GEN_TAC THEN REPEAT CONJ_TAC THENL\r
 460     [ STRIP_ASSUME_TAC (SPECL [`x:real`;`y:real`] ATAN2_TEMP) THEN\r
 461       ABBREV_TAC `t = atan2_temp (x,y)` THEN \r
 462       ABBREV_TAC `r = sqrt (x pow 2 + y pow 2)` THEN STRIP_TAC THEN\r
 463       SUBGOAL_TAC "r_pos" `&0 < r` \r
 464       [ EXPAND_TAC "r" THEN MP_TAC (SPECL [`x:real`;`y:real`] dist_lemma) THEN\r
 465         POP_ASSUM MP_TAC THEN REAL_ARITH_TAC] THEN\r
 466       SUBGOAL_TAC "tan" `(r * sin t) / (r * cos t) = tan t`\r
 467       [ REWRITE_TAC [tan] THEN POP_ASSUM MP_TAC THEN CONV_TAC REAL_FIELD ] THEN\r
 468       ASM_REWRITE_TAC [] THEN MATCH_MP_TAC (GSYM TAN_ATN) THEN \r
 469       POP_ASSUM (K ALL_TAC) THEN \r
 470       POP_ASSUM (fun th -> POP_ASSUM MP_TAC THEN ASSUME_TAC th) THEN\r
 471       ASM_SIMP_TAC [GSYM COS_NEGPOS_PI; REAL_LT_MUL_EQ] THEN REAL_ARITH_TAC ;\r
 472 \r
 473       STRIP_ASSUME_TAC (SPECL [`x:real`;`y:real`] ATAN2_TEMP) THEN\r
 474       ABBREV_TAC `t = atan2_temp (x,y)` THEN \r
 475       ABBREV_TAC `r = sqrt (x pow 2 + y pow 2)` THEN STRIP_TAC THEN\r
 476       SUBGOAL_TAC "r_pos" `&0 < r` \r
 477       [ EXPAND_TAC "r" THEN MP_TAC (SPECL [`x:real`;`y:real`] dist_lemma) THEN\r
 478         POP_ASSUM MP_TAC THEN REAL_ARITH_TAC] THEN\r
 479       SUBGOAL_TAC "tan" `(r * cos t) / (r * sin t) = inv (tan t)`\r
 480       [ REWRITE_TAC [tan] THEN POP_ASSUM MP_TAC THEN \r
 481         CONV_TAC REAL_FIELD ] THEN\r
 482       ASM_REWRITE_TAC [GSYM TAN_COT] THEN\r
 483       SUBGOAL_THEN `pi / &2 - t = atn (tan (pi / &2 - t))` \r
 484                    (fun th -> REWRITE_TAC [GSYM th] THEN REAL_ARITH_TAC) THEN\r
 485       MATCH_MP_TAC (GSYM TAN_ATN) THEN \r
 486       SUBGOAL_THEN `&0 < t /\ t < pi` \r
 487                    (fun th -> MP_TAC th THEN REAL_ARITH_TAC) THEN\r
 488       POP_ASSUM (K ALL_TAC) THEN \r
 489       POP_ASSUM (fun th -> POP_ASSUM MP_TAC THEN ASSUME_TAC th) THEN\r
 490       ASM_SIMP_TAC [GSYM SIN_NEGPOS_PI; REAL_LT_MUL_EQ] THEN REAL_ARITH_TAC ;\r
 491     \r
 492       STRIP_ASSUME_TAC (SPECL [`x:real`;`y:real`] ATAN2_TEMP) THEN\r
 493       ABBREV_TAC `t = atan2_temp (x,y)` THEN \r
 494       ABBREV_TAC `r = sqrt (x pow 2 + y pow 2)` THEN STRIP_TAC THEN\r
 495       SUBGOAL_TAC "r_pos" `&0 < r` \r
 496       [ EXPAND_TAC "r" THEN MP_TAC (SPECL [`x:real`;`y:real`] dist_lemma) THEN\r
 497         POP_ASSUM MP_TAC THEN REAL_ARITH_TAC] THEN\r
 498       SUBGOAL_TAC "tan" `(r * cos t) / (r * sin t) = --inv (tan (--t))`\r
 499       [ REWRITE_TAC [TAN_NEG; REAL_INV_NEG] THEN \r
 500         REWRITE_TAC [tan; REAL_NEG_NEG] THEN \r
 501         POP_ASSUM MP_TAC THEN CONV_TAC REAL_FIELD ] THEN\r
 502       ASM_REWRITE_TAC [GSYM TAN_COT; ATN_NEG] THEN\r
 503       SUBGOAL_THEN `pi / &2 + t = atn (tan (pi / &2 + t))` \r
 504         (fun th -> REWRITE_TAC [REAL_ARITH `pi / &2 - --t = pi / &2 + t`;GSYM th] \r
 505                    THEN REAL_ARITH_TAC) THEN\r
 506       MATCH_MP_TAC (GSYM TAN_ATN) THEN \r
 507       SUBGOAL_THEN `--pi < t /\ t < &0` \r
 508                    (fun th -> MP_TAC th THEN REAL_ARITH_TAC) THEN\r
 509       POP_ASSUM (K ALL_TAC) THEN\r
 510       POP_ASSUM (fun th -> POP_ASSUM (MP_TAC o (REWRITE_RULE [GSYM REAL_NEG_GT0]))\r
 511                            THEN ASSUME_TAC th) THEN\r
 512       ASM_SIMP_TAC [GSYM SIN_NEGPOS_PI; REAL_LT_MUL_EQ; REAL_NEG_RMUL] THEN \r
 513       REAL_ARITH_TAC ;\r
 514     \r
 515       ASM_CASES_TAC `x = &0` THENL\r
 516     [ STRIP_TAC THEN ASM_REWRITE_TAC [ATAN2_TEMP_DEF];\r
 517       ALL_TAC] THEN\r
 518     STRIP_ASSUME_TAC (SPECL [`x:real`;`y:real`] ATAN2_TEMP) THEN\r
 519     ABBREV_TAC `t = atan2_temp (x,y)` THEN \r
 520     ABBREV_TAC `r = sqrt (x pow 2 + y pow 2)` THEN STRIP_TAC THEN\r
 521     SUBGOAL_TAC "r_pos" `&0 < r` \r
 522     [ EXPAND_TAC "r" THEN MP_TAC (SPECL [`x:real`;`y:real`] dist_lemma) THEN\r
 523       POP_ASSUM MP_TAC THEN FIND_ASSUM MP_TAC `~(x = &0)` THEN \r
 524       REAL_ARITH_TAC ] THEN\r
 525     SUBGOAL_TAC "sin_cos" `sin t = &0 /\ cos t < &0 ==> t = pi`\r
 526     [ ASM_SIMP_TAC [SIN_NEGPOS_PI; COS_NEGPOS_PI] THEN MP_TAC PI_POS THEN\r
 527       REAL_ARITH_TAC ] THEN\r
 528     POP_ASSUM MATCH_MP_TAC THEN \r
 529     SUBGOAL_TAC "x_pos" `&0 < --x` \r
 530     [ FIND_ASSUM MP_TAC `x <= &0` THEN FIND_ASSUM MP_TAC `~(x = &0)` THEN\r
 531       REAL_ARITH_TAC ] THEN\r
 532     POP_ASSUM MP_TAC THEN   \r
 533     POP_ASSUM (fun th -> POP_ASSUM (K ALL_TAC) THEN POP_ASSUM MP_TAC THEN \r
 534                          ASSUME_TAC th) THEN\r
 535     ASM_SIMP_TAC [REAL_LT_MUL_EQ; REAL_NEG_RMUL] THEN POP_ASSUM MP_TAC THEN\r
 536     CONV_TAC REAL_FIELD]);;\r
 537     \r
 538   let ATAN2_TEMP_ALT = prove\r
 539    (`!x y. atan2_temp (x,y) = \r
 540      if ( abs y < x ) then atn(y / x) else\r
 541      (if (&0 < y) then ((pi / &2) - atn(x / y)) else\r
 542      (if (y < &0) then (-- (pi/ &2) - atn (x / y)) else (  pi )))`,\r
 543     STRIP_TAC THEN STRIP_TAC THEN COND_CASES_TAC THENL \r
 544     [ SUBGOAL_THEN `&0 < x` \r
 545                   (fun th -> SIMP_TAC [th; ATAN2_TEMP_BREAKDOWN]) THEN\r
 546       POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;\r
 547       COND_CASES_TAC THENL\r
 548       [ SUBGOAL_THEN `&0 < y` \r
 549                      (fun th -> SIMP_TAC [th; ATAN2_TEMP_BREAKDOWN]) THEN\r
 550         POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;\r
 551         COND_CASES_TAC THENL\r
 552         [ SUBGOAL_THEN `y < &0` \r
 553                       (fun th -> SIMP_TAC [th; ATAN2_TEMP_BREAKDOWN]) THEN\r
 554           POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;\r
 555           SUBGOAL_THEN `y = &0` \r
 556             (fun th -> POP_ASSUM (K ALL_TAC) THEN POP_ASSUM (K ALL_TAC) THEN\r
 557                        ASSUME_TAC th) THENL\r
 558           [ POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC ;\r
 559             SUBGOAL_THEN `x <= &0` \r
 560                         (fun th -> ASM_SIMP_TAC [th; ATAN2_TEMP_BREAKDOWN]) THEN\r
 561             POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC ]]]]);;  \r
 562   \r
 563   (* Show that the working def and the official def are equivalent. *)\r
 564   \r
 565   let ATAN_TEMP_ATN2 = prove\r
 566    (`atn2 = atan2_temp`,\r
 567     REWRITE_TAC [FORALL_PAIR_THM; FUN_EQ_THM; atn2; ATAN2_TEMP_ALT]);;\r
 568 \r
 569   (* These three and the definition should suffice as the basic *)\r
 570   (* specifications for atn2. No more need for atan2_temp.*)\r
 571   \r
 572   let atn2_spec = prove\r
 573    (atn2_spec_t,\r
 574     REWRITE_TAC [ATAN_TEMP_ATN2; ATAN2_TEMP_SPEC]);; \r
 575   \r
 576   let ATN2_BREAKDOWN = prove\r
 577    (`!x y. (&0 < x ==> atn2 (x,y) = atn(y / x)) /\\r
 578            (&0 < y ==> atn2 (x,y) = pi / &2 - atn(x / y)) /\\r
 579            (y < &0 ==> atn2 (x,y) = --(pi / &2) - atn(x / y)) /\\r
 580            (y = &0 /\ x <= &0 ==> atn2(x,y) = pi)`,\r
 581     REWRITE_TAC [ATAN_TEMP_ATN2; ATAN2_TEMP_BREAKDOWN]);;\r
 582     \r
 583   let ATN2_CIRCLE = prove\r
 584    (`!x y. (--pi < atan2_temp (x,y) /\ atan2_temp (x,y) <= pi) /\\r
 585            x = sqrt(x pow 2 + y pow 2) * cos (atan2_temp (x,y)) /\\r
 586            y = sqrt(x pow 2 + y pow 2) * sin (atan2_temp (x,y))`,\r
 587     REWRITE_TAC [ATAN_TEMP_ATN2; ATAN2_TEMP]);;\r
 588 \r
 589   (* Useful properties of atn2. *)\r
 590   \r
 591   let ATN2_0_1 = prove\r
 592    (`atn2 (&0, &1) = pi / &2`,\r
 593     ASSUME_TAC (REAL_ARITH `&0 < &1`) THEN \r
 594     ASM_SIMP_TAC [ATN2_BREAKDOWN] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN\r
 595     REWRITE_TAC [ATN_0] THEN REAL_ARITH_TAC);;\r
 596     \r
 597   let ATN2_0_NEG_1 = prove\r
 598    (`atn2 (&0, --(&1)) = --(pi / &2)`,\r
 599     ASSUME_TAC (REAL_ARITH `--(&1) < &0`) THEN \r
 600     ASM_SIMP_TAC [ATN2_BREAKDOWN] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN\r
 601     REWRITE_TAC [ATN_0] THEN REAL_ARITH_TAC);;\r
 602                           \r
 603   let ATN2_LMUL_EQ = prove\r
 604    (`!a x y. &0 < a ==> atn2(a * x, a * y) = atn2 (x, y)`,\r
 605     REPEAT STRIP_TAC THEN STRIP_ASSUME_TAC \r
 606       (REAL_ARITH `&0 < x \/ &0 < y \/ y < &0 \/ (y = &0 /\ x <= &0)`) THENL\r
 607     [ SUBGOAL_TAC "pos_x" `&0 < a * x` \r
 608       [ let th = SPECL [`&0`;`x:real`;`a:real`] REAL_LT_LMUL_EQ in\r
 609         let th2 = REWRITE_RULE [REAL_MUL_RZERO] th in\r
 610         ASM_SIMP_TAC [th2] ] ;\r
 611       SUBGOAL_TAC "pos_y" `&0 < a * y` \r
 612       [ let th = SPECL [`&0`;`y:real`;`a:real`] REAL_LT_LMUL_EQ in\r
 613         let th2 = REWRITE_RULE [REAL_MUL_RZERO] th in\r
 614         ASM_SIMP_TAC [th2] ] ;\r
 615        SUBGOAL_TAC "neg_y" `a * y < &0` \r
 616       [ let th = SPECL [`y:real`;`&0`;`a:real`] REAL_LT_LMUL_EQ in\r
 617         let th2 = REWRITE_RULE [REAL_MUL_RZERO] th in\r
 618         ASM_SIMP_TAC [th2] ] ;\r
 619       SUBGOAL_TAC "other" `a * y = &0 /\ a * x <= &0`\r
 620       [ ASM_REWRITE_TAC [REAL_MUL_RZERO] THEN\r
 621         let th = SPECL [`x:real`;`&0`;`a:real`] REAL_LE_LMUL_EQ in\r
 622         let th2 = REWRITE_RULE [REAL_MUL_RZERO] th in\r
 623         ASM_SIMP_TAC [th2] ] ] THEN\r
 624     let th1 = SPECL [`x:real`;`y:real`] ATN2_BREAKDOWN in\r
 625     let th2 = SPECL [`a * x:real`;`a * y:real`] ATN2_BREAKDOWN in\r
 626     let th3 = REAL_ARITH `!x. (x < &0 \/ &0 < x) ==> ~(&0 = x)` in\r
 627     ASM_SIMP_TAC [th1; th2; th3; GSYM (SPEC `a:real` REAL_DIV_MUL2)] );;        \r
 628   \r
 629   let ATN2_RNEG = prove\r
 630    (`!x y. (~(y = &0) \/ &0 < x) ==> atn2(x,--y) = --(atn2(x,y))`,\r
 631     STRIP_TAC THEN STRIP_TAC THEN STRIP_ASSUME_TAC \r
 632       (REAL_ARITH `&0 < x \/ &0 < y \/ y < &0 \/ (y = &0 /\ x <= &0)`) THENL\r
 633     [ ASM_REWRITE_TAC [] ;\r
 634       ASM_SIMP_TAC [REAL_LT_IMP_NE] THEN SUBGOAL_TAC "neg" `--y < &0`\r
 635        [ ASM_REWRITE_TAC [REAL_NEG_LT0] ] ;\r
 636       ASM_SIMP_TAC [REAL_LT_IMP_NE] THEN SUBGOAL_TAC "pos" `&0 < --y`\r
 637        [ ASM_REWRITE_TAC [REAL_NEG_GT0] ] ;\r
 638       ASM_REWRITE_TAC [real_lt] ] THEN\r
 639     let th1 = SPECL [`x:real`;`y:real`] ATN2_BREAKDOWN in\r
 640     let th2 = SPECL [`x:real`;`--y:real`] ATN2_BREAKDOWN in\r
 641     let th3 = REAL_ARITH `(--x)/y = --(x/y)` in\r
 642     let th4 = REAL_FIELD `(y < &0 \/ &0 < y) ==>  x / (--y) = --(x/y)` in\r
 643     ASM_SIMP_TAC [th1; th2; th3; th4; ATN_NEG] THEN REAL_ARITH_TAC);;\r
 644 \r
 645   (* lemma:acs_atn2 *)   \r
 646   \r
 647   let acs_atn2 = prove\r
 648    (acs_atn2_t,\r
 649     STRIP_TAC THEN ASM_CASES_TAC `y = &1 \/ y = --(&1)` THENL\r
 650     [ POP_ASSUM DISJ_CASES_TAC THENL\r
 651       [ ASM_REWRITE_TAC [] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN \r
 652         REWRITE_TAC [ACS_1; SQRT_0; ATN2_0_1] THEN REAL_ARITH_TAC ;\r
 653         ASM_REWRITE_TAC [] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN \r
 654         REWRITE_TAC [ACS_NEG_1; SQRT_0; ATN2_0_NEG_1] THEN REAL_ARITH_TAC ] ;\r
 655       STRIP_TAC THEN \r
 656       SUBGOAL_TAC "sqrt" `&0 < sqrt (&1 - y pow 2)`\r
 657       [ MATCH_MP_TAC SQRT_POS_LT THEN\r
 658         SUBGOAL_THEN `&0 <= y pow 2 /\ y pow 2 < &1`\r
 659                      (fun th -> MP_TAC th THEN REAL_ARITH_TAC) THEN\r
 660         REWRITE_TAC [REAL_LE_POW_2; REAL_ARITH `a < &1 <=> a < &1 pow 2`;\r
 661                      GSYM REAL_LT_SQUARE_ABS ] THEN \r
 662         REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ] THEN\r
 663        ASM_SIMP_TAC [ATN2_BREAKDOWN] THEN MATCH_MP_TAC ACS_ATN THEN\r
 664        REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ]);;\r
 665   \r
 666   (* ----------------------------------------------------------------------- *)\r
 667   (* Theory of triangles (without vectors). Includes laws of cosines/sines.  *)\r
 668   (* ----------------------------------------------------------------------- *)\r
 669   \r
 670   let UPS_X_SQUARES = prove\r
 671    (`!a b c. ups_x (a * a) (b * b) (c * c) =\r
 672            &16 * ((a + b + c) / &2) * \r
 673            (((a + b + c) / &2) - a) * \r
 674            (((a + b + c) / &2) - b) * \r
 675            (((a + b + c) / &2) - c)`,\r
 676     REPEAT STRIP_TAC THEN REWRITE_TAC [ups_x] THEN REAL_ARITH_TAC);;\r
 677 \r
 678   (* Theorems assuming a, b, c are lengths of a triangle (c not 0). *)\r
 679 \r
 680   let TRI_UPS_X_POS = prove\r
 681    (`!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>\r
 682      &0 <= ups_x (a * a) (b * b) (c * c)`,\r
 683     REPEAT STRIP_TAC THEN REWRITE_TAC [UPS_X_SQUARES] THEN\r
 684     REPEAT (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC) THENL\r
 685     [ REAL_ARITH_TAC ;\r
 686       REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ;\r
 687       SUBGOAL_THEN `&2 * a <= a + b + c` \r
 688                    (fun th -> MP_TAC th THEN REAL_ARITH_TAC) THEN\r
 689       REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ;\r
 690       SUBGOAL_THEN `&2 * b <= a + b + c` \r
 691                    (fun th -> MP_TAC th THEN REAL_ARITH_TAC) THEN\r
 692       REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ;\r
 693       SUBGOAL_THEN `&2 * c <= a + b + c` \r
 694                    (fun th -> MP_TAC th THEN REAL_ARITH_TAC) THEN\r
 695       REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ]);;\r
 696   \r
 697   let TRI_SQUARES_BOUNDS = prove\r
 698    (`!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>\r
 699      --(&1) <= ((a * a) + (b * b) - (c * c)) / (&2 * a * b) /\\r
 700      ((a * a) + (b * b) - (c * c)) / (&2 * a * b) <= &1`,\r
 701     REPEAT STRIP_TAC THEN \r
 702     SUBGOAL_TAC "2ab_pos" `&0 < &2 * a * b` \r
 703     [ ASM_SIMP_TAC [REAL_LT_MUL_3; REAL_ARITH `&0 < &2`] ] THENL\r
 704     [ SUBGOAL_TAC "abc_square" `c*c <= (a + b) * (a + b)`\r
 705       [ MATCH_MP_TAC (REWRITE_RULE [IMP_IMP] REAL_LE_MUL2) THEN \r
 706         REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ] THEN\r
 707       ASM_SIMP_TAC [REAL_LE_RDIV_EQ] THEN REMOVE_THEN "abc_square" MP_TAC THEN\r
 708       REAL_ARITH_TAC ;\r
 709       SUBGOAL_TAC "abc_square" `(a - b) * (a - b) <= c*c`\r
 710       [ DISJ_CASES_TAC (REAL_ARITH `a <= b \/ b <= a`) THENL\r
 711         [ SUBST1_TAC (REAL_ARITH `(a-b)*(a-b)=(b-a)*(b-a)`); ALL_TAC ] THEN\r
 712         MATCH_MP_TAC (REWRITE_RULE [IMP_IMP] REAL_LE_MUL2) THEN \r
 713         REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC ] THEN\r
 714       ASM_SIMP_TAC [REAL_LE_LDIV_EQ] THEN REMOVE_THEN "abc_square" MP_TAC THEN\r
 715       REAL_ARITH_TAC ]);;\r
 716 \r
 717   let ATN2_ARCLENGTH = prove\r
 718    (`!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>\r
 719      arclength a b c = pi / &2 - atn2(sqrt(ups_x (a*a) (b*b) (c*c)), (a*a) + (b*b) - (c*c))`,\r
 720     REPEAT STRIP_TAC THEN \r
 721     let th = REAL_ARITH `c * c - a * a - b * b = --(a * a + b * b - c * c)` in\r
 722     REWRITE_TAC [arclength; th; ATN2_RNEG] THEN\r
 723     SUBGOAL_THEN `~(a * a + b * b - c * c = &0) \/\r
 724                  &0 < sqrt(ups_x (a*a) (b*b) (c*c))` \r
 725                 (fun th -> ASM_SIMP_TAC [th; ATN2_RNEG] THEN \r
 726                            REAL_ARITH_TAC) THEN\r
 727     REWRITE_TAC [TAUT `(~A \/ B) <=> (A ==> B)`] THEN STRIP_TAC THEN\r
 728     SUBGOAL_TAC "c_ab" `c*c = a*a + b*b` \r
 729     [ POP_ASSUM MP_TAC THEN REAL_ARITH_TAC ] THEN \r
 730     REMOVE_THEN "c_ab" (fun th -> REWRITE_TAC [ups_x; th]) THEN \r
 731     MATCH_MP_TAC SQRT_POS_LT THEN \r
 732     CONV_TAC (DEPTH_BINOP_CONV `(<)` REAL_POLY_CONV) THEN\r
 733     MATCH_MP_TAC REAL_LT_MUL_3 THEN STRIP_TAC THENL\r
 734     [ REAL_ARITH_TAC ;\r
 735       ASM_SIMP_TAC [REAL_POW_LT] ]);;\r
 736 \r
 737   let TRI_LEMMA = prove\r
 738    (`!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>\r
 739      (&2 * a * b) * (a * a + b * b - c * c) / (&2 * a * b) =\r
 740      a * a + b * b - c * c`,\r
 741     REPEAT STRIP_TAC THEN \r
 742     SUBGOAL_TAC "2ab_pos" `&0 < &2 * a * b`\r
 743     [ ASM_SIMP_TAC [REAL_LT_MUL_3; REAL_ARITH `&0 < &2`] ] THEN\r
 744     SUBGOAL_TAC "2ab_not0" `~(&2 * a * b = &0)` \r
 745     [ POP_ASSUM MP_TAC THEN REAL_ARITH_TAC ] THEN\r
 746     ASM_SIMP_TAC [REAL_DIV_LMUL]);;\r
 747 \r
 748   let TRI_UPS_X_SQUARES = prove\r
 749    (`!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>\r
 750      ups_x (a * a) (b * b) (c * c) =\r
 751      (&2 * a * b) pow 2 * (&1 - ((a * a + b * b - c * c) / (&2 * a * b)) pow 2)`,\r
 752     REPEAT STRIP_TAC THEN\r
 753     ASM_SIMP_TAC [ups_x; REAL_SUB_LDISTRIB; GSYM REAL_POW_MUL; TRI_LEMMA] THEN\r
 754     REAL_ARITH_TAC);;\r
 755 \r
 756   let TRI_UPS_X_SQRT = prove\r
 757    (`!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>\r
 758      sqrt(ups_x (a * a) (b * b) (c * c)) =\r
 759      (&2 * a * b) * sqrt(&1 - ((a * a + b * b - c * c) / (&2 * a * b)) pow 2)`,\r
 760     REPEAT STRIP_TAC THEN\r
 761     SUBGOAL_TAC "2ab_pos" `&0 < &2 * a * b`\r
 762     [ ASM_SIMP_TAC [REAL_LT_MUL_3; REAL_ARITH `&0 < &2`] ] THEN\r
 763     SUBGOAL_TAC "other_pos" `&0 <= &1 - ((a * a + b * b - c * c) / (&2 * a * b)) pow 2`\r
 764     [ SUBGOAL_THEN `((a * a + b * b - c * c) / (&2 * a * b)) pow 2 <= &1`\r
 765         (fun th -> MP_TAC th THEN REAL_ARITH_TAC) THEN\r
 766     ASM_SIMP_TAC [ABS_SQUARE_LE_1; REAL_ABS_BOUNDS; TRI_SQUARES_BOUNDS] ] THEN\r
 767     ASM_SIMP_TAC [SQRT_MUL_L; REAL_LT_IMP_LE; TRI_UPS_X_SQUARES] );;\r
 768 \r
 769   let ACS_ARCLENGTH = prove\r
 770    (`!a b c. (&0 < a) /\ (&0 < b) /\ (&0 <= c) /\ (c <= a + b) /\ (a <= b + c) /\ (b <= c + a) ==>\r
 771      arclength a b c = acs (((a * a) + (b * b) - (c * c)) / (&2 * a * b))`,\r
 772     REPEAT STRIP_TAC THEN ASM_SIMP_TAC [ATN2_ARCLENGTH; TRI_SQUARES_BOUNDS; acs_atn2] THEN\r
 773     SUBGOAL_TAC "2ab_pos" `&0 < &2 * a * b`\r
 774     [ ASM_SIMP_TAC [REAL_LT_MUL_3; REAL_ARITH `&0 < &2`] ] THEN\r
 775     SUBGOAL_THEN \r
 776       `(sqrt (ups_x (a * a) (b * b) (c * c)), a * a + b * b - c * c) =\r
 777        ((&2 * a * b) * sqrt (&1 - ((a * a + b * b - c * c) / (&2 * a * b)) pow 2),\r
 778         (&2 * a * b) * ((a * a + b * b - c * c) / (&2 * a * b)))`\r
 779       (fun th -> ASM_SIMP_TAC [ATN2_LMUL_EQ; th]) THEN \r
 780     ASM_SIMP_TAC [TRI_UPS_X_SQRT; TRI_LEMMA]);;\r
 781 \r
 782   let law_of_cosines = prove    \r
 783    (law_of_cosines_t,\r
 784     REPEAT STRIP_TAC THEN \r
 785     REWRITE_TAC [REAL_ARITH `&2 * a * b * x = (&2 * a * b) * x`] THEN\r
 786     ASM_SIMP_TAC [ACS_ARCLENGTH; TRI_SQUARES_BOUNDS; COS_ACS; TRI_LEMMA] THEN \r
 787     REAL_ARITH_TAC);;\r
 788 \r
 789   let law_of_sines =  prove\r
 790    (law_of_sines_t,\r
 791     REPEAT STRIP_TAC THEN\r
 792     REWRITE_TAC [REAL_ARITH `&2 * a * b * x = (&2 * a * b) * x`;\r
 793                  REAL_ARITH `x pow 2 = x * x` ] THEN\r
 794     ASM_SIMP_TAC [ACS_ARCLENGTH; TRI_SQUARES_BOUNDS; SIN_ACS; TRI_UPS_X_SQRT]);;\r
 795 \r
 796   (* ----------------------------------------------------------------------- *)\r
 797   (* Cross product properties.                                               *)\r
 798   (* ----------------------------------------------------------------------- *)\r
 799 \r
 800   let DIST_TRIANGLE_DETAILS = prove\r
 801          (`~(u = v) /\ ~(u = w) <=>\r
 802            &0 < dist(u,v) /\ &0 < dist(u,w) /\\r
 803      &0 <= dist(v,w) /\\r
 804      dist(v,w) <= dist(u,v) + dist(u,w) /\\r
 805      dist(u,v) <= dist(u,w) + dist(v,w) /\\r
 806      dist(u,w) <= dist(v,w) + dist(u,v)`,\r
 807                 NORM_ARITH_TAC);;\r
 808 \r
 809   let arcVarc = prove\r
 810          (arcVarc_t,\r
 811           SIMP_TAC [DIST_TRIANGLE_DETAILS;  arcV; ACS_ARCLENGTH] THEN\r
 812                 REPEAT STRIP_TAC THEN AP_TERM_TAC THEN \r
 813                 REWRITE_TAC [DOT_NORM_NEG; dist] THEN \r
 814                 let tha = NORM_ARITH `norm (v - u) = norm (u - v)` in\r
 815                 let thb = NORM_ARITH `norm (w - u) = norm (u - w)` in\r
 816                 let thc = NORM_ARITH `norm (v - u - (w - u)) = norm (v - w)` in\r
 817                 REWRITE_TAC [tha; thb; thc] THEN CONV_TAC REAL_FIELD);;\r
 818 \r
 819   let DIST_LAW_OF_COS = prove\r
 820          (`(dist(v:real^3,w)) pow 2 = (dist(u,v)) pow 2 + (dist(u,w)) pow 2 - \r
 821                                      &2 * (dist(u,v)) * (dist(u,w)) * cos (arcV u v w)`,\r
 822     ASM_CASES_TAC `~(u = v:real^3) /\ ~(u = w)` THEN POP_ASSUM MP_TAC THENL\r
 823                 [ ASM_SIMP_TAC [arcVarc] THEN \r
 824                   REWRITE_TAC [law_of_cosines; DIST_TRIANGLE_DETAILS];\r
 825                   REWRITE_TAC [TAUT `~(~A /\ ~B) <=> (A \/ B)`] THEN STRIP_TAC THEN \r
 826                         ASM_REWRITE_TAC [DIST_REFL; DIST_SYM] THEN REAL_ARITH_TAC]);;\r
 827 \r
 828   let DIST_L_ZERO = prove\r
 829          (`!v. dist(vec 0, v) = norm v`,\r
 830     NORM_ARITH_TAC);;\r
 831         \r
 832   (* I would like to change this to real^N but that means changing arcV to real^N *)\r
 833 \r
 834   let DOT_COS = prove \r
 835          (`u:real^3 dot v = (norm u) * (norm v) * cos (arcV (vec 0) u v)`,\r
 836     MP_TAC (INST [`vec 0:real^3`,`u:real^3`; \r
 837                               `u:real^3`,`v:real^3`; \r
 838                                                                   `v:real^3`,`w:real^3`] DIST_LAW_OF_COS) THEN  \r
 839                 SUBGOAL_THEN \r
 840                   `dist(u:real^3,v) pow 2 = \r
 841                    dist(vec 0, v) pow 2 + dist(vec 0, u) pow 2 - &2 * u dot v` \r
 842                         (fun th -> REWRITE_TAC [th; DIST_L_ZERO] THEN REAL_ARITH_TAC) THEN\r
 843                 REWRITE_TAC [NORM_POW_2; dist; DOT_RSUB; DOT_LSUB; \r
 844                              DOT_SYM; DOT_LZERO; DOT_RZERO] THEN\r
 845     REAL_ARITH_TAC);;\r
 846 \r
 847   (* DIMINDEX_3, FORALL_3, SUM_3, DOT_3, VECTOR_3, FORALL_VECTOR_3          *)\r
 848         (* are all very useful.  Any time you see a theorem you need with         *)\r
 849         (* 1 <= i /\ i <= dimindex(:3), first use INST_TYPE and then rewrite      *)\r
 850         (* with DIMINDEX_3 and FORALL_3 or see if it's in the list below.         *)\r
 851         \r
 852   let CART_EQ_3 = prove\r
 853    (`!x y. (x:A^3) = y <=> x$1 = y$1 /\ x$2 = y$2 /\ x$3 = y$3`,\r
 854           REWRITE_TAC [CART_EQ; DIMINDEX_3; FORALL_3]);;\r
 855         \r
 856         let LAMBDA_BETA_3 = prove\r
 857    (`((lambda) g:A^3) $1 = g 1 /\\r
 858            ((lambda) g:A^3) $2 = g 2 /\\r
 859                  ((lambda) g:A^3) $3 = g 3`,\r
 860     let th = REWRITE_RULE [DIMINDEX_3; FORALL_3] \r
 861                                       (INST_TYPE [`:3`,`:B`] LAMBDA_BETA) in\r
 862                 REWRITE_TAC [th]);;\r
 863 \r
 864   let VEC_COMPONENT_3 = prove\r
 865    (`!k. (vec k :real^3)$1 = &k /\ \r
 866                (vec k :real^3)$2 = &k /\ \r
 867                      (vec k :real^3)$3 = &k`,\r
 868     let th = REWRITE_RULE [DIMINDEX_3; FORALL_3] \r
 869                                       (INST_TYPE [`:3`,`:N`] VEC_COMPONENT) in\r
 870                 REWRITE_TAC [th]);;\r
 871 \r
 872   let VECTOR_ADD_COMPONENT_3 = prove\r
 873    (`!x:real^3 y. (x + y)$1 = x$1 + y$1 /\\r
 874                         (x + y)$2 = x$2 + y$2 /\\r
 875                                                                         (x + y)$3 = x$3 + y$3`,\r
 876                 let th = REWRITE_RULE [DIMINDEX_3; FORALL_3] \r
 877                                       (INST_TYPE [`:3`,`:N`] VECTOR_ADD_COMPONENT) in\r
 878                 REWRITE_TAC [th]);;\r
 879 \r
 880   let VECTOR_SUB_COMPONENT_3 = prove\r
 881    (`!x:real^3 y. (x - y)$1 = x$1 - y$1 /\\r
 882                         (x - y)$2 = x$2 - y$2 /\\r
 883                                                                         (x - y)$3 = x$3 - y$3`,\r
 884                 let th = REWRITE_RULE [DIMINDEX_3; FORALL_3] \r
 885                                       (INST_TYPE [`:3`,`:N`] VECTOR_SUB_COMPONENT) in\r
 886                 REWRITE_TAC [th]);;\r
 887 \r
 888   let VECTOR_NEG_COMPONENT_3 = prove\r
 889    (`!x:real^3. (--x)$1 = --(x$1) /\\r
 890                       (--x)$2 = --(x$2) /\\r
 891                                                                 (--x)$3 = --(x$3)`,\r
 892     let th = REWRITE_RULE [DIMINDEX_3; FORALL_3] \r
 893                                       (INST_TYPE [`:3`,`:N`] VECTOR_NEG_COMPONENT) in\r
 894                 REWRITE_TAC [th]);;\r
 895 \r
 896   let VECTOR_MUL_COMPONENT_3 = prove\r
 897    (`!c x:real^3. (c % x)$1 = c * x$1 /\\r
 898                         (c % x)$2 = c * x$2 /\\r
 899                                                                         (c % x)$3 = c * x$3`,\r
 900     let th = REWRITE_RULE [DIMINDEX_3; FORALL_3] \r
 901                                       (INST_TYPE [`:3`,`:N`] VECTOR_MUL_COMPONENT) in\r
 902                 REWRITE_TAC [th]);;\r
 903 \r
 904  (* COND_COMPONENT_3 - no need, COND_COMPONENT works fine. *)\r
 905 \r
 906   let BASIS_3 = prove\r
 907    (`(basis 1:real^3)$1 = &1 /\ (basis 1:real^3)$2 = &0 /\ (basis 1:real^3)$3 = &0 /\\r
 908            (basis 2:real^3)$1 = &0 /\ (basis 2:real^3)$2 = &1 /\ (basis 2:real^3)$3 = &0 /\\r
 909            (basis 3:real^3)$1 = &0 /\ (basis 3:real^3)$2 = &0 /\ (basis 3:real^3)$3 = &1`,\r
 910           REWRITE_TAC [basis; \r
 911                        REWRITE_RULE [DIMINDEX_3; FORALL_3] \r
 912                                                                         (INST_TYPE [`:3`,`:B`] LAMBDA_BETA)] THEN\r
 913           ARITH_TAC);;\r
 914 \r
 915   let COMPONENTS_3 = prove\r
 916          (`!v. v:real^3 = v$1 % basis 1 + v$2 % basis 2 + v$3 % basis 3`,\r
 917     REWRITE_TAC [CART_EQ_3; VECTOR_ADD_COMPONENT_3; \r
 918                              VECTOR_MUL_COMPONENT_3; BASIS_3] THEN REAL_ARITH_TAC);;\r
 919 \r
 920   let VECTOR_COMPONENTS_3 = prove\r
 921          (`!a b c. vector [a;b;c]:real^3 = a % basis 1 + b % basis 2 + c % basis 3`,\r
 922           let th = REWRITE_RULE [VECTOR_3] \r
 923                                       (ISPEC `vector [a;b;c]:real^3` COMPONENTS_3) in\r
 924     REWRITE_TAC [th]);;\r
 925 \r
 926   let cross_skew = prove\r
 927          (cross_skew_t,\r
 928           REWRITE_TAC [CART_EQ_3; CROSS_COMPONENTS; VECTOR_NEG_COMPONENT_3] THEN \r
 929                 REAL_ARITH_TAC);;\r
 930           \r
 931   let cross_triple = prove\r
 932          (cross_triple_t,\r
 933           REWRITE_TAC [ DOT_3; CROSS_COMPONENTS] THEN REAL_ARITH_TAC);;\r
 934   \r
 935         let NORM_CAUCHY_SCHWARZ_FRAC = prove\r
 936          (`!(u:real^N) v. ~(u = vec 0) /\ ~(v = vec 0) ==>\r
 937                  -- &1 <= (u dot v) / (norm u * norm v) /\\r
 938                  (u dot v) / (norm u * norm v) <= &1`,\r
 939                 REPEAT STRIP_TAC THEN\r
 940                 SUBGOAL_TAC "norm_pos" `&0 < norm (u:real^N) * norm (v:real^N)`\r
 941                 [ POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN \r
 942                   SIMP_TAC [GSYM NORM_POS_LT; IMP_IMP; REAL_LT_MUL] ] THEN\r
 943                 MP_TAC (SPECL [`u:real^N`;`v:real^N`] NORM_CAUCHY_SCHWARZ_ABS) THEN\r
 944                 ASM_SIMP_TAC [REAL_ABS_BOUNDS; REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ] THEN\r
 945                 REAL_ARITH_TAC);;\r
 946         \r
 947         let CROSS_LZERO = prove\r
 948          (`!x. (vec 0) cross x = vec 0`,\r
 949            REWRITE_TAC [CART_EQ_3; CROSS_COMPONENTS; VEC_COMPONENT_3] THEN \r
 950            REAL_ARITH_TAC);;\r
 951 \r
 952         let CROSS_RZERO = prove\r
 953          (`!x. x cross (vec 0) = vec 0`,\r
 954            REWRITE_TAC [CART_EQ_3; CROSS_COMPONENTS; VEC_COMPONENT_3] THEN \r
 955            REAL_ARITH_TAC);;\r
 956  \r
 957   let CROSS_SQUARED = prove\r
 958          (`!u v. (u cross v) dot (u cross v) = \r
 959                        (ups_x (u dot u) (v dot v) ((u - v) dot (u - v))) / &4`,\r
 960           REWRITE_TAC [DOT_3; CROSS_COMPONENTS; ups_x; VECTOR_SUB_COMPONENT_3] THEN\r
 961           REAL_ARITH_TAC);;\r
 962  \r
 963   let DIST_UPS_X_POS = prove\r
 964    (`~(u = v) /\ ~(u = w) ==>\r
 965            &0 <= ups_x (dist(u,v) pow 2) (dist(u,w) pow 2) (dist(v,w) pow 2)`,\r
 966                 REWRITE_TAC [DIST_TRIANGLE_DETAILS; TRI_UPS_X_POS; REAL_POW_2]);;\r
 967   \r
 968         let SQRT_DIV_R = prove\r
 969          (`&0 <= x /\ &0 <= y ==> sqrt (x) / y = sqrt (x/ (y pow 2)) /\ &0 <= x/(y pow 2)`,\r
 970                 SIMP_TAC [SQRT_DIV; REAL_LE_POW_2; POW_2_SQRT; REAL_LE_DIV]);;\r
 971         \r
 972   let NORM_CROSS = prove\r
 973          (`!u v. ~(vec 0 = u) /\ ~(vec 0 = v) ==>\r
 974                    norm (u cross v) = \r
 975                          sqrt (ups_x ((norm u) pow 2) \r
 976                                                        ((norm v) pow 2) \r
 977                                                                                          ((dist(u,v)) pow 2)) / &2`,\r
 978                 REPEAT GEN_TAC THEN DISCH_TAC THEN IMP_RES_THEN MP_TAC DIST_UPS_X_POS THEN\r
 979                 REWRITE_TAC [DIST_L_ZERO] THEN \r
 980                 SIMP_TAC[SQRT_DIV_R; REAL_ARITH `&0 <= &2`; REAL_ARITH `&2 pow 2 = &4`] THEN \r
 981                 DISCH_TAC THEN MATCH_MP_TAC (GSYM SQRT_UNIQUE) THEN \r
 982                 REWRITE_TAC [dist; NORM_POW_2; CROSS_SQUARED] THEN NORM_ARITH_TAC);;\r
 983                                 \r
 984         let VECTOR_LAW_OF_SINES = prove                 \r
 985          (`~(vec 0 = u:real^3) /\ ~(vec 0 = v) ==>\r
 986            &2 * (norm u) * (norm v) * sin (arcV (vec 0) u v) =\r
 987               sqrt (ups_x (norm u pow 2) (norm v pow 2) (dist (u,v) pow 2))`,\r
 988                  SIMP_TAC [arcVarc; DIST_TRIANGLE_DETAILS; law_of_sines; DIST_L_ZERO]);;        \r
 989                                                 \r
 990         let cross_mag = prove\r
 991          (cross_mag_t,\r
 992           REPEAT STRIP_TAC THEN \r
 993                 REWRITE_TAC [arcVarc; VECTOR_SUB_RZERO] THEN\r
 994                 ASM_CASES_TAC `(u:real^3) = vec 0 \/ (v:real^3) = vec 0` THENL\r
 995                 [ POP_ASSUM STRIP_ASSUME_TAC THEN \r
 996                   ASM_REWRITE_TAC [CROSS_LZERO; CROSS_RZERO; NORM_0] THEN REAL_ARITH_TAC ;\r
 997                         POP_ASSUM MP_TAC THEN \r
 998                         REWRITE_TAC [DE_MORGAN_THM; MESON [] `a = vec 0 <=> vec 0 = a`] THEN \r
 999                         SIMP_TAC [NORM_CROSS; GSYM VECTOR_LAW_OF_SINES] THEN REAL_ARITH_TAC ]);;\r
1000 \r
1001 \r
1002 \r
1003 end;;\r
1004  \r