Top File of PVS trig Library

 
top: THEORY
%------------------------------------------------------------------------
%
% An Axiomatic Theory of Trigonometry (Demonstrated to be sound in trig_fnd
%                                      library)
%
%       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
% 
%      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/23/04              atan2 added (D Lester)
%
%      Version 1.34   5/30/04              atan/asin/acos added (D Lester)
%
%      Version 1.4    4/15/05              approx made consistent with trig_fnd
%
% INDEX:
% ------
%
%
%     trig_basic:
%     -----------
%         - definition of pi with crude upper and lower bounds
%         - 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_inv
%      -------------
%         - provides interface to atan, asin, acos, atan2
%
%      -------------
%         - defines inverse trig functions: arcsin, arccos, and arctan 
%
%      trig_rew
%      -------------
%         - Experimental auto-rewrite-theory background library
%
%
%------------------------------------------------------------------------

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
             trig_approx,   % taylor series approximations to trig functions:
             tan_approx,    % approximatan2_propsations fprior tangent
             law_cosines,   % law of cosines
             trig_degree,   % conversions to degrees
             trig_inverses, % interface to atan, asin, acos, atan2
             trig_rew,      % auto-rewrites
             asin,          % asin properties
             acos,          % acos properties
             atan,          % atan properties
             atan_values,   % atan for specific values
             atan2,         % two-argument arc tangent
             atan2_props,   % additional properties of atan2 and values
             jatan2,        % Java atan2

             to2pi,         % normalization of radians to 2pi

             sincos,        % continuity, derivablility of sin, cos
             deriv_sincos,
             integral_sincos,
             integral_indef_sincos

END top

The tag identifies links that are outside the NASA domain