legacy/oldtrig/trig_old.ml

   1 (* cut from trig.ml.
   2    Material by J. Rute and T. Hales *)
   3
   4
   5 (*** work in progress
   6
   7   prove
   8          (`!u v w. arcV u v w = arcV (vec 0) (v - u) (w - u)`,
   9            REWRITE_TAC [CONV_RULE KEP_REAL3_CONV arcV; VECTOR_SUB_RZERO]);;
  10
  11   let ARCV_BILINEAR_L = prove
  12          (`!(u:real^N) v s. ~(u = vec 0) /\ ~(v = vec 0) /\ &0 < s ==>
  13              arcV (vec 0) (s % u) v = arcV (vec 0) u v`,
  14           REWRITE_TAC [REAL_ARITH `!x. &0 < x <=> ~(&0 = x) /\ &0 <= x`] THEN
  15                 REWRITE_TAC [GSYM NORM_POS_LT] THEN     REPEAT STRIP_TAC THEN
  16                 REWRITE
  17 _TAC [CONV_RULE KEP_REAL3_CONV arcV; VECTOR_SUB_RZERO; DOT_LMUL;
  18                              NORM_MUL; GSYM REAL_MUL_ASSOC] THEN
  19                 SUBGOAL_TAC "norm_pos" `&0 < norm (u:real^N) * norm (v:real^N)`
  20                  [MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC []] THEN
  21                 SUBGOAL_TAC "norm_nonzero" `~(&0 = norm (u:real^N) * norm (v:real^N))`
  22                  [POP_ASSUM MP_TAC THEN REAL_ARITH_TAC] THEN
  23                 SUBGOAL_TAC "stuff" `abs s = s`
  24                  [ASM_REWRITE_TAC [REAL_ABS_REFL]] THEN
  25                 ASM_SIMP_TAC [GSYM REAL_DIV_MUL2]);;
  26
  27         let ARCV_SYM = prove
  28          (`!(u:real^N) v w. arcV u v w = arcV u w v`,
  29          REWRITE_TAC [CONV_RULE KEP_REAL3_CONV arcV; DOT_SYM; REAL_MUL_SYM]);;
  30
  31   let ARCV_BILINEAR_R = prove
  32          (`!(u:real^N) v s. ~(u = vec 0) /\ ~(v = vec 0) /\ &0 < s ==>
  33              arcV (vec 0) u (s % v) = arcV (vec 0) u v`,
  34                 REPEAT STRIP_TAC THEN
  35                 SUBGOAL_TAC "switch" `arcV (vec 0) (u:real^N) (s % v) = arcV (vec 0) (s % v)    u`
  36                  [REWRITE_TAC [ARCV_SYM]] THEN
  37                 POP_ASSUM SUBST1_TAC THEN ASM_SIMP_TAC [ARCV_BILINEAR_L; ARCV_SYM]);;
  38
  39
  40   prove
  41          (`!u v. ~(u = vec 0) /\ ~(v = vec 0) ==>
  42               arcV (vec 0) u v =
  43                           arcV (vec 0) ((inv (norm u)) % u) ((inv (norm v)) % v)`,
  44                 REPEAT STRIP_TAC THEN
  45                 SUBGOAL_TAC "u" `&0 < inv (norm (u:real^3))`
  46                 [ REPEAT (POP_ASSUM MP_TAC) THEN
  47                   SIMP_TAC [GSYM NORM_POS_LT; REAL_LT_INV] ] THEN
  48                 SUBGOAL_TAC "v" `&0 < inv (norm (v:real^3))`
  49                 [ REPEAT (POP_ASSUM MP_TAC) THEN
  50                   SIMP_TAC [GSYM NORM_POS_LT; REAL_LT_INV] ] THEN
  51                 SUBGOAL_TAC "vv" `~(inv (norm v) % (v:real^3) = vec 0)`
  52                 [ ASM_REWRITE_TAC [VECTOR_MUL_EQ_0] THEN POP_ASSUM MP_TAC THEN
  53                   REAL_ARITH_TAC ] THEN
  54     ASM_SIMP_TAC [ARCV_BILINEAR_L; ARCV_BILINEAR_R]);;
  55
  56   prove
  57          (`!v:real^N. ~(v = vec 0) ==> norm((inv (norm v)) % v) = &1`,
  58           REWRITE_TAC [NORM_MUL; REAL_ABS_INV; REAL_ABS_NORM; GSYM NORM_POS_LT] THEN
  59                 CONV_TAC REAL_FIELD);;
  60
  61         prove
  62          (`!v0 va vb vc.
  63             dihV v0 va vb vc =
  64                   dihV (vec 0) (va - v0) (vb - v0) (vc - v0)`,
  65           REWRITE_TAC [CONV_RULE KEP_REAL3_CONV dihV; VECTOR_SUB_RZERO]);;
  66
  67   prove
  68          (`!va vb vc s. ~(va = vec 0) /\ ~(vb = vec 0) /\ ~(vb = vec 0) /\ &0 < s ==>
  69              dihV (vec 0) (s % va) vb vc = dihV (vec 0) va vb vc`,
  70                 REWRITE_TAC [REAL_ARITH `!x. &0 < x <=> ~(&0 = x) /\ &0 <= x`] THEN
  71                 REWRITE_TAC [GSYM NORM_POS_LT] THEN     REPEAT STRIP_TAC THEN
  72                 REWRITE_TAC [CONV_RULE KEP_REAL3_CONV dihV; VECTOR_SUB_RZERO; DOT_LMUL;
  73                              DOT_RMUL; NORM_MUL; GSYM REAL_MUL_ASSOC; VECTOR_MUL_ASSOC] THEN
  74                 let thm1 =
  75                         VECTOR_ARITH `!x v. (s * s * x) % (v:real^3) = (s pow 2) % (x % v)` in
  76                 let thm2 =
  77                         VECTOR_ARITH `!x v. (s * x * s) % (v:real^3) = (s pow 2) % (x % v)` in
  78                 REWRITE_TAC [thm1; thm2; GSYM VECTOR_SUB_LDISTRIB]
  79                 );;
  80
  81   let COLLINEAR_TRANSLATE = prove
  82          (`collinear (s:real^N->bool) <=> collinear {v - v0 | v IN s}`,
  83           REWRITE_TAC [collinear; IN_ELIM_THM] THEN EQ_TAC THEN STRIP_TAC THEN
  84                 EXISTS_TAC `u :real^N` THEN REPEAT STRIP_TAC THENL
  85                 [ ASM_SIMP_TAC [VECTOR_ARITH `!u:real^N v w. u - w - (v - w) = u - v`] ;
  86                   ONCE_REWRITE_TAC [VECTOR_ARITH `x:real^N - y = (x - v0) - (y - v0)`] THEN
  87                   SUBGOAL_THEN
  88                           `(?v:real^N. v IN s /\ x - v0 = v - v0) /\
  89                                  (?v. v IN s /\ y - v0 = v - v0)`
  90               (fun th -> ASM_SIMP_TAC [th]) THEN
  91                         STRIP_TAC THENL [EXISTS_TAC `x:real^N`; EXISTS_TAC `y:real^N`] THEN
  92                         ASM_REWRITE_TAC [] ]);;
  93
  94         let SET_MAP_3 = prove
  95          (`{f x | x IN {a, b, c}} = {f a, f b, f c}`,
  96           REWRITE_TAC [EXTENSION; IN_ELIM_THM;
  97                              SET_RULE `x IN {a, b, c} <=> (x = a \/ x = b \/ x = c)`] THEN
  98                 MESON_TAC []);;
  99
 100         let COLLINEAR_TRANSLATE_3 = prove
 101          (`collinear {u:real^N, v, w} <=> collinear {u - v0, v - v0, w - v0}`,
 102           SUBGOAL_TAC "step1"
 103                   `collinear {u:real^N, v, w} <=> collinear {x - v0 | x IN {u, v, w}}`
 104                   [ REWRITE_TAC [GSYM COLLINEAR_TRANSLATE] ] THEN
 105                 SUBGOAL_TAC "step2"
 106                   `{x - v0 | x:real^N IN {u, v, w}} = {u - v0, v - v0, w - v0}`
 107                         [ REWRITE_TAC [SET_MAP_3] ] THEN
 108                 ASM_REWRITE_TAC [] );;
 109
 110         let COLLINEAR_ZERO = prove
 111          (`collinear {u:real^N, v, w} <=> collinear {vec 0, v - u, w - u}`,
 112           SUBGOAL_TAC "zero"
 113                   `vec 0 :real^N = u - u`
 114                         [ REWRITE_TAC [VECTOR_SUB_REFL] ] THEN
 115                 ASM_REWRITE_TAC [GSYM COLLINEAR_TRANSLATE_3]);;
 116
 117   let COLLINEAR_SYM = prove
 118          (`collinear {vec 0: real^N, x, y} <=> collinear {vec 0: real^N, y, x}`,
 119           AP_TERM_TAC THEN SET_TAC [] );;
 120
 121   let COLLINEAR_FACT = prove
 122          (`collinear {vec 0: real^N, x, y} <=>
 123            ((y dot y) % x = (x dot y) % y)`,
 124                 ONCE_REWRITE_TAC [COLLINEAR_SYM] THEN EQ_TAC THENL
 125                 [ REWRITE_TAC [COLLINEAR_LEMMA] THEN STRIP_TAC THEN
 126                   ASM_REWRITE_TAC [DOT_LZERO; DOT_RZERO; VECTOR_MUL_LZERO;
 127                                    VECTOR_MUL_RZERO; VECTOR_MUL_ASSOC;
 128                                                                                          DOT_LMUL; REAL_MUL_SYM];
 129                         REWRITE_TAC [COLLINEAR_LEMMA;
 130                                      TAUT `A \/ B \/ C <=> ((~A /\ ~B) ==> C)`] THEN
 131                         REPEAT STRIP_TAC THEN EXISTS_TAC `(x:real^N dot y) / (y dot y)` THEN
 132                         MATCH_MP_TAC
 133                           (ISPECL [`y:real^N dot y`;`x:real^N`] VECTOR_MUL_LCANCEL_IMP) THEN
 134                         SUBGOAL_TAC "zero"
 135                           `~((y:real^N) dot y = &0)` [ ASM_REWRITE_TAC [DOT_EQ_0] ] THEN
 136                         ASM_SIMP_TAC [VECTOR_MUL_ASSOC; REAL_DIV_LMUL] ] );;
 137
 138
 139   let COLLINEAR_NOT_ZERO = prove
 140          (`~collinear {u:real^N, v, w} ==> ~(vec 0 = v - u) /\ ~(vec 0 = w - u)`,
 141           ONCE_REWRITE_TAC [COLLINEAR_ZERO] THEN REWRITE_TAC [COLLINEAR_LEMMA] THEN
 142                 MESON_TAC [] );;
 143
 144         let COS_ARCV = prove
 145          (`~(vec 0 = u:real^3) /\ ~(vec 0 = v) ==>
 146            cos (arcV (vec 0) u v)       = (u dot v) / (norm u * norm v)`,
 147                 REWRITE_TAC [DOT_COS;
 148                              MESON [NORM_EQ_0] `!v. vec 0 = v <=> norm v = &0`] THEN
 149           CONV_TAC REAL_FIELD);;
 150
 151
 152         prove
 153          (`~(collinear {v0:real^3,va,vc}) /\ ~(collinear {v0,vb,vc}) ==>
 154     (let gamma = dihV v0 vc va vb in
 155      let a = arcV v0 vb vc in
 156      let b = arcV v0 va vc in
 157      let c = arcV v0 va vb in
 158        cos(gamma) pow 2 = ((cos(c) - cos(a)*cos(b))/(sin(a)*sin(b))) pow 2)`,
 159
 160 module Trig : Trigsig = struct
 161
 162   let trigAxiomProofA a_t = prove(a_t,
 163       (MP_TAC trig_term) THEN (REWRITE_TAC[trig_term_list]) THEN
 164       (DISCH_THEN (fun t-> ASM_REWRITE_TAC[t]))
 165       )
 166   let trigAxiomProofB a_t = prove(a_t,
 167       (MP_TAC trig_term) THEN (REWRITE_TAC[trig_term_list]) THEN
 168       (REPEAT STRIP_TAC)
 169       )
 170
 171                 sin (arcV v0 vb vc) =
 172                 norm (((vc - v0) dot (vc - v0)) % (va - v0) -
 173           ((va - v0) dot (vc - v0)) % (vc - v0))
 174
 175                 cos (arcV v0 va vb) =
 176
 177
 178   prove
 179          (spherical_loc_t,
 180           REWRITE_TAC [COLLINEAR_ZERO ;COLLINEAR_FACT] THEN
 181                 ONCE_REWRITE_TAC [VECTOR_ARITH `a = b <=> vec 0 = a - b`] THEN
 182                 REPEAT STRIP_TAC THEN
 183                 REPEAT (CONV_TAC let_CONV) THEN
 184                 REWRITE_TAC [CONV_RULE KEP_REAL3_CONV dihV] THEN
 185                 ASM_SIMP_TAC [COS_ARCV ; COLLINEAR_NOT_ZERO]
 186
 187 ***)
 188
 189
 190         (* yet unproven theorems:
 191
 192 module Trig : Trigsig = struct
 193
 194   let trigAxiomProofA a_t = prove(a_t,
 195       (MP_TAC trig_term) THEN (REWRITE_TAC[trig_term_list]) THEN
 196       (DISCH_THEN (fun t-> ASM_REWRITE_TAC[t]))
 197       )
 198   let trigAxiomProofB a_t = prove(a_t,
 199       (MP_TAC trig_term) THEN (REWRITE_TAC[trig_term_list]) THEN
 200       (REPEAT STRIP_TAC)
 201       )
 202
 203   let  spherical_loc = trigAxiomProofB   spherical_loc_t
 204   let  spherical_loc2 = trigAxiomProofB   spherical_loc2_t
 205   let  dih_formula = trigAxiomProofB   dih_formula_t
 206   let  dih_x_acs = trigAxiomProofB   dih_x_acs_t
 207   let  beta_cone = trigAxiomProofB   beta_cone_t
 208   let  euler_triangle = trigAxiomProofB   euler_triangle_t
 209   let  polar_cycle_rotate = trigAxiomProofB   polar_cycle_rotate_t
 210   let  thetaij = trigAxiomProofB   thetaij_t
 211   let  thetapq_wind = trigAxiomProofB   thetapq_wind_t
 212   let  zenith = trigAxiomProofB   zenith_t
 213   let  polar_coord_zenith = trigAxiomProofB   polar_coord_zenith_t
 214   let  azim_pair = trigAxiomProofB   azim_pair_t
 215   let  azim_cycle_sum = trigAxiomProofB   azim_cycle_sum_t
 216   let  dih_azim = trigAxiomProofB   dih_azim_t
 217   let  sph_triangle_ineq = trigAxiomProofB   sph_triangle_ineq_t
 218   let  sph_triangle_ineq_sum = trigAxiomProofB   sph_triangle_ineq_sum_t
 219   let  azim = trigAxiomProofB   azim_t
 220         *)
 221
 222 (*  let  polar_coords = trigAxiomProofB   polar_coords_t  *)
 223 (*  let  spherical_coord = trigAxiomProofB   spherical_coord_t *)
 224 (* [deprecated]
 225   let  aff_insert_sym = trigAxiomProofB   aff_insert_sym_t
 226   let  aff_sgn_insert_sym_gt = trigAxiomProofB   aff_sgn_insert_sym_gt_t
 227   let  aff_sgn_insert_sym_ge = trigAxiomProofB   aff_sgn_insert_sym_ge_t
 228   let  aff_sgn_insert_sym_lt = trigAxiomProofB   aff_sgn_insert_sym_lt_t
 229   let  aff_sgn_insert_sym_le = trigAxiomProofB   aff_sgn_insert_sym_le_t
 230   let  azim_hyp = trigAxiomProofB   azim_hyp_t
 231   let  azim_cycle_hyp = trigAxiomProofB   azim_cycle_hyp_t
 232   let  aff = trigAxiomProofA   aff_t
 233   let  aff_gt = trigAxiomProofB   aff_gt_t
 234   let  aff_ge = trigAxiomProofB   aff_ge_t
 235   let  aff_lt = trigAxiomProofB   aff_lt_t
 236   let  aff_le = trigAxiomProofB   aff_le_t
 237   let  azim_cycle = trigAxiomProofB   azim_cycle_t
 238 *)
 239
 240 end;;
 241
 242
 243