Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Cobol/Test-Suite/SQL P/     Datei vom 4.1.2008 mit Größe 15 kB image not shown  

Quelle  deriv_sincos.pvs   Sprache: unbekannt

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

   ASSUMING
     IMPORTING analysis@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@chain_rule, analysis@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@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


84%


[ Dauer der Verarbeitung: 0.5 Sekunden  (vorverarbeitet)  ]