NASA logo

+ Contact NASA



  • + HOME
  • + WELCOME
  • + QUICK PAGE
  • + PHILOSOPHY
  • + TEAM
  • + RESEARCH
  • + LINKS

  • 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
    

    The tag [*] identifies links that are outside the NASA domain