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}
%
%
%  >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}