Quellcode-Bibliothek deriv_sincos.pvs

deriv_sincos[ T : TYPE FROM real ] : THEORY
%------------------------------------------------------------------------------
%  Convenient forms of sin cos derivatives.
%
%      Rick Butler 4/1/2010
%------------------------------------------------------------------------------
BEGIN

   ASSUMING
     IMPORTING analysis_ax@deriv_domain

     connected_domain: ASSUMPTION connected?[T]

     not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING

   deriv_domain: LEMMA deriv_domain?[T]


   IMPORTING sincos, analysis_ax@chain_rule, analysis_ax@composition_continuous

   a,b,t: VAR T
   k,alpha: VAR real

   sin_continuous: LEMMA
       continuous?[T](LAMBDA (x: T): k * sin(alpha * x))

   cos_continuous: LEMMA
       continuous?[T](LAMBDA (x: T): k * cos(alpha * x))

   sin_derivable: LEMMA
       derivable?[T](LAMBDA (x: T): k * sin(alpha * x))

   cos_derivable: LEMMA
       derivable?[T](LAMBDA (x: T): k * cos(alpha * x))

   IMPORTING analysis_ax@derivatives_lam[T]

   deriv_sin: LEMMA alpha /= 0 IMPLIES
       deriv[T](LAMBDA (x:T): k*sin(alpha*x)) =  
            (LAMBDA (t: T): k*alpha*cos(alpha*t))
  
   deriv_cos: LEMMA alpha /= 0 IMPLIES
       deriv[T](LAMBDA (x:T): k*cos(alpha*x)) = 
            (LAMBDA (t: T): -k*alpha*sin(alpha*t))

END deriv_sincos