(* cut from trig.ml.
Material by J. Rute and T. Hales *)
(*** work in progress
prove
(`!u v w. arcV u v w = arcV (vec 0) (v - u) (w - u)`,
REWRITE_TAC [CONV_RULE KEP_REAL3_CONV arcV; VECTOR_SUB_RZERO]);;
let ARCV_BILINEAR_L = prove
(`!(u:real^N) v s. ~(u = vec 0) /\ ~(v = vec 0) /\ &0 < s ==>
arcV (vec 0) (s % u) v = arcV (vec 0) u v`,
REWRITE_TAC [REAL_ARITH `!x. &0 < x <=> ~(&0 = x) /\ &0 <= x`] THEN
REWRITE_TAC [GSYM NORM_POS_LT] THEN REPEAT STRIP_TAC THEN
REWRITE
_TAC [CONV_RULE KEP_REAL3_CONV arcV; VECTOR_SUB_RZERO; DOT_LMUL;
NORM_MUL; GSYM REAL_MUL_ASSOC] THEN
SUBGOAL_TAC "norm_pos" `&0 < norm (u:real^N) * norm (v:real^N)`
[MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC []] THEN
SUBGOAL_TAC "norm_nonzero" `~(&0 = norm (u:real^N) * norm (v:real^N))`
[POP_ASSUM MP_TAC THEN REAL_ARITH_TAC] THEN
SUBGOAL_TAC "stuff" `abs s = s`
[ASM_REWRITE_TAC [REAL_ABS_REFL]] THEN
ASM_SIMP_TAC [GSYM REAL_DIV_MUL2]);;
let ARCV_SYM = prove
(`!(u:real^N) v w. arcV u v w = arcV u w v`,
REWRITE_TAC [CONV_RULE KEP_REAL3_CONV arcV; DOT_SYM; REAL_MUL_SYM]);;
let ARCV_BILINEAR_R = prove
(`!(u:real^N) v s. ~(u = vec 0) /\ ~(v = vec 0) /\ &0 < s ==>
arcV (vec 0) u (s % v) = arcV (vec 0) u v`,
REPEAT STRIP_TAC THEN
SUBGOAL_TAC "switch" `arcV (vec 0) (u:real^N) (s % v) = arcV (vec 0) (s % v) u`
[REWRITE_TAC [ARCV_SYM]] THEN
POP_ASSUM SUBST1_TAC THEN ASM_SIMP_TAC [ARCV_BILINEAR_L; ARCV_SYM]);;
prove
(`!u v. ~(u = vec 0) /\ ~(v = vec 0) ==>
arcV (vec 0) u v =
arcV (vec 0) ((inv (norm u)) % u) ((inv (norm v)) % v)`,
REPEAT STRIP_TAC THEN
SUBGOAL_TAC "u" `&0 < inv (norm (u:real^3))`
[ REPEAT (POP_ASSUM MP_TAC) THEN
SIMP_TAC [GSYM NORM_POS_LT; REAL_LT_INV] ] THEN
SUBGOAL_TAC "v" `&0 < inv (norm (v:real^3))`
[ REPEAT (POP_ASSUM MP_TAC) THEN
SIMP_TAC [GSYM NORM_POS_LT; REAL_LT_INV] ] THEN
SUBGOAL_TAC "vv" `~(inv (norm v) % (v:real^3) = vec 0)`
[ ASM_REWRITE_TAC [VECTOR_MUL_EQ_0] THEN POP_ASSUM MP_TAC THEN
REAL_ARITH_TAC ] THEN
ASM_SIMP_TAC [ARCV_BILINEAR_L; ARCV_BILINEAR_R]);;
prove
(`!v:real^N. ~(v = vec 0) ==> norm((inv (norm v)) % v) = &1`,
REWRITE_TAC [NORM_MUL; REAL_ABS_INV; REAL_ABS_NORM; GSYM NORM_POS_LT] THEN
CONV_TAC REAL_FIELD);;
prove
(`!v0 va vb vc.
dihV v0 va vb vc =
dihV (vec 0) (va - v0) (vb - v0) (vc - v0)`,
REWRITE_TAC [CONV_RULE KEP_REAL3_CONV dihV; VECTOR_SUB_RZERO]);;
prove
(`!va vb vc s. ~(va = vec 0) /\ ~(vb = vec 0) /\ ~(vb = vec 0) /\ &0 < s ==>
dihV (vec 0) (s % va) vb vc = dihV (vec 0) va vb vc`,
REWRITE_TAC [REAL_ARITH `!x. &0 < x <=> ~(&0 = x) /\ &0 <= x`] THEN
REWRITE_TAC [GSYM NORM_POS_LT] THEN REPEAT STRIP_TAC THEN
REWRITE_TAC [CONV_RULE KEP_REAL3_CONV dihV; VECTOR_SUB_RZERO; DOT_LMUL;
DOT_RMUL; NORM_MUL; GSYM REAL_MUL_ASSOC; VECTOR_MUL_ASSOC] THEN
let thm1 =
VECTOR_ARITH `!x v. (s * s * x) % (v:real^3) = (s pow 2) % (x % v)` in
let thm2 =
VECTOR_ARITH `!x v. (s * x * s) % (v:real^3) = (s pow 2) % (x % v)` in
REWRITE_TAC [thm1; thm2; GSYM VECTOR_SUB_LDISTRIB]
);;
let COLLINEAR_TRANSLATE = prove
(`collinear (s:real^N->bool) <=> collinear {v - v0 | v IN s}`,
REWRITE_TAC [collinear; IN_ELIM_THM] THEN EQ_TAC THEN STRIP_TAC THEN
EXISTS_TAC `u :real^N` THEN REPEAT STRIP_TAC THENL
[ ASM_SIMP_TAC [VECTOR_ARITH `!u:real^N v w. u - w - (v - w) = u - v`] ;
ONCE_REWRITE_TAC [VECTOR_ARITH `x:real^N - y = (x - v0) - (y - v0)`] THEN
SUBGOAL_THEN
`(?v:real^N. v IN s /\ x - v0 = v - v0) /\
(?v. v IN s /\ y - v0 = v - v0)`
(fun th -> ASM_SIMP_TAC [th]) THEN
STRIP_TAC THENL [EXISTS_TAC `x:real^N`; EXISTS_TAC `y:real^N`] THEN
ASM_REWRITE_TAC [] ]);;
let SET_MAP_3 = prove
(`{f x | x IN {a, b, c}} = {f a, f b, f c}`,
REWRITE_TAC [EXTENSION; IN_ELIM_THM;
SET_RULE `x IN {a, b, c} <=> (x = a \/ x = b \/ x = c)`] THEN
MESON_TAC []);;
let COLLINEAR_TRANSLATE_3 = prove
(`collinear {u:real^N, v, w} <=> collinear {u - v0, v - v0, w - v0}`,
SUBGOAL_TAC "step1"
`collinear {u:real^N, v, w} <=> collinear {x - v0 | x IN {u, v, w}}`
[ REWRITE_TAC [GSYM COLLINEAR_TRANSLATE] ] THEN
SUBGOAL_TAC "step2"
`{x - v0 | x:real^N IN {u, v, w}} = {u - v0, v - v0, w - v0}`
[ REWRITE_TAC [SET_MAP_3] ] THEN
ASM_REWRITE_TAC [] );;
let COLLINEAR_ZERO = prove
(`collinear {u:real^N, v, w} <=> collinear {vec 0, v - u, w - u}`,
SUBGOAL_TAC "zero"
`vec 0 :real^N = u - u`
[ REWRITE_TAC [VECTOR_SUB_REFL] ] THEN
ASM_REWRITE_TAC [GSYM COLLINEAR_TRANSLATE_3]);;
let COLLINEAR_SYM = prove
(`collinear {vec 0: real^N, x, y} <=> collinear {vec 0: real^N, y, x}`,
AP_TERM_TAC THEN SET_TAC [] );;
let COLLINEAR_FACT = prove
(`collinear {vec 0: real^N, x, y} <=>
((y dot y) % x = (x dot y) % y)`,
ONCE_REWRITE_TAC [COLLINEAR_SYM] THEN EQ_TAC THENL
[ REWRITE_TAC [COLLINEAR_LEMMA] THEN STRIP_TAC THEN
ASM_REWRITE_TAC [DOT_LZERO; DOT_RZERO; VECTOR_MUL_LZERO;
VECTOR_MUL_RZERO; VECTOR_MUL_ASSOC;
DOT_LMUL; REAL_MUL_SYM];
REWRITE_TAC [COLLINEAR_LEMMA;
TAUT `A \/ B \/ C <=> ((~A /\ ~B) ==> C)`] THEN
REPEAT STRIP_TAC THEN EXISTS_TAC `(x:real^N dot y) / (y dot y)` THEN
MATCH_MP_TAC
(ISPECL [`y:real^N dot y`;`x:real^N`] VECTOR_MUL_LCANCEL_IMP) THEN
SUBGOAL_TAC "zero"
`~((y:real^N) dot y = &0)` [ ASM_REWRITE_TAC [DOT_EQ_0] ] THEN
ASM_SIMP_TAC [VECTOR_MUL_ASSOC; REAL_DIV_LMUL] ] );;
let COLLINEAR_NOT_ZERO = prove
(`~collinear {u:real^N, v, w} ==> ~(vec 0 = v - u) /\ ~(vec 0 = w - u)`,
ONCE_REWRITE_TAC [COLLINEAR_ZERO] THEN REWRITE_TAC [COLLINEAR_LEMMA] THEN
MESON_TAC [] );;
let COS_ARCV = prove
(`~(vec 0 = u:real^3) /\ ~(vec 0 = v) ==>
cos (arcV (vec 0) u v) = (u dot v) / (norm u * norm v)`,
REWRITE_TAC [DOT_COS;
MESON [NORM_EQ_0] `!v. vec 0 = v <=> norm v = &0`] THEN
CONV_TAC REAL_FIELD);;
prove
(`~(collinear {v0:real^3,va,vc}) /\ ~(collinear {v0,vb,vc}) ==>
(let gamma = dihV v0 vc va vb in
let a = arcV v0 vb vc in
let b = arcV v0 va vc in
let c = arcV v0 va vb in
cos(gamma) pow 2 = ((cos(c) - cos(a)*cos(b))/(sin(a)*sin(b))) pow 2)`,
module Trig : Trigsig = struct
let trigAxiomProofA a_t = prove(a_t,
(MP_TAC trig_term) THEN (REWRITE_TAC[trig_term_list]) THEN
(DISCH_THEN (fun t-> ASM_REWRITE_TAC[t]))
)
let trigAxiomProofB a_t = prove(a_t,
(MP_TAC trig_term) THEN (REWRITE_TAC[trig_term_list]) THEN
(REPEAT STRIP_TAC)
)
sin (arcV v0 vb vc) =
norm (((vc - v0) dot (vc - v0)) % (va - v0) -
((va - v0) dot (vc - v0)) % (vc - v0))
cos (arcV v0 va vb) =
prove
(spherical_loc_t,
REWRITE_TAC [COLLINEAR_ZERO ;COLLINEAR_FACT] THEN
ONCE_REWRITE_TAC [VECTOR_ARITH `a = b <=> vec 0 = a - b`] THEN
REPEAT STRIP_TAC THEN
REPEAT (CONV_TAC let_CONV) THEN
REWRITE_TAC [CONV_RULE KEP_REAL3_CONV dihV] THEN
ASM_SIMP_TAC [COS_ARCV ; COLLINEAR_NOT_ZERO]
***)
(* yet unproven theorems:
module Trig : Trigsig = struct
let trigAxiomProofA a_t = prove(a_t,
(MP_TAC trig_term) THEN (REWRITE_TAC[trig_term_list]) THEN
(DISCH_THEN (fun t-> ASM_REWRITE_TAC[t]))
)
let trigAxiomProofB a_t = prove(a_t,
(MP_TAC trig_term) THEN (REWRITE_TAC[trig_term_list]) THEN
(REPEAT STRIP_TAC)
)
let spherical_loc = trigAxiomProofB spherical_loc_t
let spherical_loc2 = trigAxiomProofB spherical_loc2_t
let dih_formula = trigAxiomProofB dih_formula_t
let dih_x_acs = trigAxiomProofB dih_x_acs_t
let beta_cone = trigAxiomProofB beta_cone_t
let euler_triangle = trigAxiomProofB euler_triangle_t
let polar_cycle_rotate = trigAxiomProofB polar_cycle_rotate_t
let thetaij = trigAxiomProofB thetaij_t
let thetapq_wind = trigAxiomProofB thetapq_wind_t
let zenith = trigAxiomProofB zenith_t
let polar_coord_zenith = trigAxiomProofB polar_coord_zenith_t
let azim_pair = trigAxiomProofB azim_pair_t
let azim_cycle_sum = trigAxiomProofB azim_cycle_sum_t
let dih_azim = trigAxiomProofB dih_azim_t
let sph_triangle_ineq = trigAxiomProofB sph_triangle_ineq_t
let sph_triangle_ineq_sum = trigAxiomProofB sph_triangle_ineq_sum_t
let azim = trigAxiomProofB azim_t
*)
(* let polar_coords = trigAxiomProofB polar_coords_t *)
(* let spherical_coord = trigAxiomProofB spherical_coord_t *)
(* [deprecated]
let aff_insert_sym = trigAxiomProofB aff_insert_sym_t
let aff_sgn_insert_sym_gt = trigAxiomProofB aff_sgn_insert_sym_gt_t
let aff_sgn_insert_sym_ge = trigAxiomProofB aff_sgn_insert_sym_ge_t
let aff_sgn_insert_sym_lt = trigAxiomProofB aff_sgn_insert_sym_lt_t
let aff_sgn_insert_sym_le = trigAxiomProofB aff_sgn_insert_sym_le_t
let azim_hyp = trigAxiomProofB azim_hyp_t
let azim_cycle_hyp = trigAxiomProofB azim_cycle_hyp_t
let aff = trigAxiomProofA aff_t
let aff_gt = trigAxiomProofB aff_gt_t
let aff_ge = trigAxiomProofB aff_ge_t
let aff_lt = trigAxiomProofB aff_lt_t
let aff_le = trigAxiomProofB aff_le_t
let azim_cycle = trigAxiomProofB azim_cycle_t
*)
end;;