Top File of PVS trig_fnd Library
top: THEORY
%------------------------------------------------------------------------
%
% A Foundational Theory of Trigonometry
%
% by Cesar Munoz Langley ICASE Institute
% Victor Carreno NASA Langley
% Ricky Butler NASA Langley
% Gilles Dowek INRIA, Domaine de Voluceau
% Alfons Geser Langley ICASE Institute
% Ben Di Vito NASA Langley
% David Lester Manchester University
%
% Version 1.0 3/27/01
% Version 1.1 6/27/01 New lemmas added:
% --------------------------------
% tan_period, sin_k_pi , cos_2k_pi,
% cos_k_pi , sin_k_pi2, tan_k_pi,
% sin_eq_1 , cos_eq_1 , sin_eq_sin,
% cos_eq_cos, tan_eq_tan, sin_eq_pm1,
% cos_eq_pm1, and prelude_aux lemmas
%
% Version 1.2 6/28/01 Theory "trig_rew" added
%
% Version 1.3 10/27/03 Corrected, foundational theory
% (David Lester)
%
% Version 1.31 11/29/03 Renamed PI to pi (Cesar A. Munoz)
%
% Version 1.32 2/6/04 Theory "tan_approx" added (C. Munoz)
%
% Version 1.33 5/30/04 inverse equivalences done (DRL)
%
% Version 1.4 1/5/05 update to analysis name changes
%
% Version 1.5 4/21/05 atan2_props added and minor things
%
% Version 1.6 1/8/08 cleaned up types of inverse functions
%
% INDEX:
% ------
%
% trig_basic:
% -----------
% - definition of pi with c
% - definition of sin, cos, and tan
% - pythagorean properties: sq(sin(a)) + sq(cos(a)) = 1
% - sum and difference of two angles
% - double angle formulas
% - negative properties, e.g. sin(-a)
% - periodicity, e.g. sin(a) = sin(a + 2 * j * pi)
% - co-function identities, e.g. sin(pi/2 - a) = cos(a)
% - location of zeros of trig functions
%
% trig_values Lemma names
% ----------- ------------------------------------
% - trig functions at 0 : sin_0 , cos_0 , tan_0
% - trig functions at pi/6 : sin_pi6 , cos_pi6 , tan_pi6
% - trig functions at pi/4 : sin_pi4 , cos_pi4 , tan_pi4
% - trig functions at pi/3 : sin_pi3 , cos_pi3 , tan_pi3
% - trig functions at pi/2 : sin_pi2 , cos_pi2 , tan_pi2
% - trig functions at pi : sin_pi , cos_pi , tan_pi
% - trig functions at 2*pi/3 : sin_2pi3 , cos_2pi3 , tan_2pi3
% - trig functions at 3*pi/4 : sin_3pi4 , cos_3pi4 , tan_3pi4
% - trig functions at 5*pi/4 : sin_5pi4 , cos_5pi4 , tan_5pi4
%
% trig_ineq
% ---------
% - regions where functions are greater than 0
% - regions where functions are less than 0
% - regions where functions are increasing
% - regions where functions are decreasing
%
% trig_extra
% ----------
% - reduction theorems
% - sum and product identities
% - half-angle identities and zeros
% - triple angle formulas
%
% trig_approx
% -----------
% - taylor series approximations to trig functions:
% sin_approx(a,n): sum first n terms of taylor expansion of sin
% cos_approx(a,n): sum first n terms of taylor expansion of cos
%
% tan_approx
% ----------
% - taylor series approximations for tangent
%
%
% law_cosines
% -----------
% - the law of cosines in a coordinate geometry formulation
%
% trig_degree
% -----------
% - trig functions that take arguments in degrees: sind, cosd
% - defines conversions toRad, toDeg
%
% trig_inverses
% -------------
% - defines inverse trig functions: arcsin, arccos, and arctan
%
% trig_rew
% -------------
% - Experimental auto-rewrite-theory background library
%
% atan2
% ----
% - defines two-argument inverse tangent: atan2
%
%------------------------------------------------------------------------
BEGIN
IMPORTING trig_doc, % Some more documentation (Rationale)
trig, % typical needs
trig_full, % everything
% --------------------- The above import the following ------------------
trig_basic, % basic properties
trig_values, % values of functions for special arguments
trig_ineq, % trig inequalities
trig_extra, % sum and product, half-angle, reductions and zeros
exp_term,
trig_approx, % taylor series approximations to trig functions:
tan_approx, % Approximations for tangent
atan_approx, % Approximations for atan
law_cosines, % law of cosines
trig_degree, % conversions to degrees
trig_inverses, % inverse functions
trig_rew, % auto-rewrites
% ---------------------- Foundational Development -----------------------
sincos, % continuity and differentiability of sin, cos
acos, % arc cosine (from arc tangent)
asin, % arc sine (from arc tangent)
atan, % one-argument arc tangent (from integral)
atan_values, % special values of atan
atan2, % two-argument arc tangent
atan2_props, % additional properties of atan2
jatan2, % Java atan2
to2pi, % normalization of radians to 2pi
sincos_phase, % sin and cos from infinite series
sincos, % continuity, differentiality, and bounds
sincos_quad, % basic properties of sin cos
deriv_sincos, % convenient forms over T from real
integral_sincos, % convenient forms over T from real
integral_indef_sincos, % sin/cos indefinite integral properties
tan_quad % definiton of tan from atan
% ---- type simplifications
%
% NOTE: real_abs_lt_pi: NONEMPTY_TYPE = {x:real | abs(x) < pi/2} was
% renamed to real_abs_lt_pi2 which is much more conistent!!!
%
% in atan:
%
% >real_abs_lt_pi2: NONEMPTY_TYPE = {x | abs(x) < pi/2}
% real_abs_lt_pi2: NONEMPTY_TYPE = {x | -pi/2 < x AND x < pi/2}
%
% in asin:
%
% >real_abs_le1: NONEMPTY_TYPE = {x:real | abs(x) <= 1}
% >real_abs_lt1: NONEMPTY_TYPE = {x:real | abs(x) < 1}
% >real_abs_le_pi2: NONEMPTY_TYPE = {x:real | abs(x) <= pi/2}
% real_abs_le1: NONEMPTY_TYPE = {x:real | -1 <= x AND x <= 1}
% real_abs_lt1: NONEMPTY_TYPE = {x:real | -1 < x AND x < 1}
% real_abs_le_pi2: NONEMPTY_TYPE = {x:real | -pi/2 <= x AND x <= pi/2}
%
% in sincos_quad:
%
% >real_abs_lt_pi: NONEMPTY_TYPE = {x:real | abs(x) < pi/2}
% real_abs_lt_pi2: NONEMPTY_TYPE = {x:real | -pi/2 < x AND x < pi/2}
% NAME CHANGES made 7-21-08:
%
% sin_continuous2 --> sin_cont_fun
% cos_continuous2 --> cos_cont_fun
% sin_derivable2 --> sin_derivable_fun
% cos_derivable2 --> cos_derivable_fun
% acos_derivable2 --> acos_derivable_fun
% asin_derivable2 --> asin_derivable_fun
% sin_value_derivable2 --> sin_value_derivable_fun
% cos_value_derivable2 --> cos_value_derivable_fun
END top