2 Material by J. Rute and T. Hales *)
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]);;
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
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]);;
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]);;
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`,
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]);;
41 (`!u v. ~(u = vec 0) /\ ~(v = vec 0) ==>
43 arcV (vec 0) ((inv (norm u)) % u) ((inv (norm v)) % v)`,
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
54 ASM_SIMP_TAC [ARCV_BILINEAR_L; ARCV_BILINEAR_R]);;
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);;
64 dihV (vec 0) (va - v0) (vb - v0) (vc - v0)`,
65 REWRITE_TAC [CONV_RULE KEP_REAL3_CONV dihV; VECTOR_SUB_RZERO]);;
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
75 VECTOR_ARITH `!x v. (s * s * x) % (v:real^3) = (s pow 2) % (x % v)` in
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]
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
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 [] ]);;
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
100 let COLLINEAR_TRANSLATE_3 = prove
101 (`collinear {u:real^N, v, w} <=> collinear {u - v0, v - v0, w - v0}`,
103 `collinear {u:real^N, v, w} <=> collinear {x - v0 | x IN {u, v, w}}`
104 [ REWRITE_TAC [GSYM COLLINEAR_TRANSLATE] ] THEN
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 [] );;
110 let COLLINEAR_ZERO = prove
111 (`collinear {u:real^N, v, w} <=> collinear {vec 0, v - u, w - u}`,
113 `vec 0 :real^N = u - u`
114 [ REWRITE_TAC [VECTOR_SUB_REFL] ] THEN
115 ASM_REWRITE_TAC [GSYM COLLINEAR_TRANSLATE_3]);;
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 [] );;
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
133 (ISPECL [`y:real^N dot y`;`x:real^N`] VECTOR_MUL_LCANCEL_IMP) THEN
135 `~((y:real^N) dot y = &0)` [ ASM_REWRITE_TAC [DOT_EQ_0] ] THEN
136 ASM_SIMP_TAC [VECTOR_MUL_ASSOC; REAL_DIV_LMUL] ] );;
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
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);;
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)`,
160 module Trig : Trigsig = struct
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]))
166 let trigAxiomProofB a_t = prove(a_t,
167 (MP_TAC trig_term) THEN (REWRITE_TAC[trig_term_list]) THEN
171 sin (arcV v0 vb vc) =
172 norm (((vc - v0) dot (vc - v0)) % (va - v0) -
173 ((va - v0) dot (vc - v0)) % (vc - v0))
175 cos (arcV v0 va vb) =
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]
190 (* yet unproven theorems:
192 module Trig : Trigsig = struct
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]))
198 let trigAxiomProofB a_t = prove(a_t,
199 (MP_TAC trig_term) THEN (REWRITE_TAC[trig_term_list]) THEN
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
222 (* let polar_coords = trigAxiomProofB polar_coords_t *)
223 (* let spherical_coord = trigAxiomProofB spherical_coord_t *)
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