Quelle  integral_indef_sincos.pvs   Sprache: PVS

integral_indef_sincos[T: TYPE+ FROM real]: THEORY
%------------------------------------------------------------------------------
%
%   Integration results for the kinematics library
%
%    Provides: the connection between the calculation of the position
%              during a turn and the integration of speed values
%
%    Authors: Radu Siminiceanu    National Institute of Aerospace
%             Rick Butler         NASA Langley
%
%------------------------------------------------------------------------------
BEGIN

   ASSUMING
      IMPORTING analysis_ax@deriv_domain_def

      connected_domain : ASSUMPTION connected?[T]

      not_one_element : ASSUMPTION not_one_element?[T]

      T_pred0         : ASSUMPTION T_pred(0)

   ENDASSUMING

   IMPORTING sincos,
         deriv_sincos, 
      analysis_ax@fundamental_theorem,
      analysis_ax@chain_rule,
      analysis_ax@composition_continuous,
      analysis_ax@continuous_lambda,
      analysis_ax@derivatives_lam,
      analysis_ax@indefinite_integral
      

   alpha, theta, k, a, b, v: VAR real
   w : VAR nzreal
   t0, t1, t2: VAR T

   derivable_sin_lin: LEMMA a /=0 IMPLIES
    derivable?(LAMBDA (t: T): k / a * sin(a*t + b))

   derivable_cos_lin: LEMMA a /=0 IMPLIES
    derivable?(LAMBDA (t: T): k / a * cos(a*t + b))

   deriv_sin_lin: LEMMA a /= 0 IMPLIES
        deriv[T](LAMBDA (t: T): k*sin(b+a*t)) =  
             (LAMBDA (u: T): k*a*cos(b+a*u))
  
   deriv_cos_lin: LEMMA a /= 0 IMPLIES
        deriv[T](LAMBDA (t: T): -k*cos(b+a*t)) = 
             (LAMBDA (u: T): k*a*sin(b+a*u))

   cos_lin_integrable: LEMMA alpha /= 0 
                    IMPLIES integrable?[T](LAMBDA (t: T): k * cos(theta + alpha * t))

   sin_lin_integrable: LEMMA alpha /=0 
         IMPLIES integrable?[T](LAMBDA (t: T): k * sin(theta + alpha * t))

   integral_sin: LEMMA (EXISTS (c:real):
       integral[T](LAMBDA (t: T): v*sin(theta + w*t)) = (LAMBDA (t: T): -(v/w)*cos(theta + w*t)) + const_fun(c))

   integral_cos: LEMMA (EXISTS (c:real):
       integral[T](LAMBDA (t: T): v*cos(theta + w*t)) = (LAMBDA (t: T): (v/w)*sin(theta + w*t)) + const_fun(c))


   Integral_sin: LEMMA
    Integral(t1, t2, (LAMBDA (t: T): v*sin(theta + w*t))) = -(v/w)*(cos(theta + w*t2) - cos(theta + w*t1))

   Integral_cos: LEMMA
    Integral(t1, t2, (LAMBDA (t: T): v*cos(theta + w*t))) = (v/w)*(sin(theta + w*t2) - sin(theta + w*t1))
  
END integral_indef_sincos