Quelle  deriv_sincos_ax.pvs   Sprache: PVS

deriv_sincos_ax[ T : TYPE FROM real ] : THEORY
BEGIN

   ASSUMING
     IMPORTING analysis@deriv_domain

     connected_domain: ASSUMPTION connected?[T]

     not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING


   AUTO_REWRITE+ connected_domain
   AUTO_REWRITE+ not_one_element

   IMPORTING trig@trig_basic, analysis@derivatives

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


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

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

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

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

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


END deriv_sincos_ax