Quelle  trig_fun.pvs   Sprache: PVS

trig_fun: THEORY
%----------------------------------------------------------------------------
%
% Definition of trigonometric functions
%
% Developed  by Ricky W. Butler      NASA Langley Research Center
% 
%      Version 1.0    last modified 10/02/00
%
%
%----------------------------------------------------------------------------

BEGIN

   IMPORTING power_series_conv, ints@factorial, analysis@deriv_domain

   AUTO_REWRITE- abs_0
   AUTO_REWRITE- abs_nat

   n: VAR nat
   x: VAR real

   c1,c2: VAR nat
   useful_prep: LEMMA convergent?(series(LAMBDA n: (abs(x))^n/factorial(n))) 


   altsign_prep: LEMMA (-1) ^ n = -1 OR (-1) ^ n = 1

   altsign(n: nat): {i: int | i = -1 OR i = 1} = IF even?(n) THEN (-1)^(n/2)
                                                 ELSE (-1)^((n-1)/2)
                                                 ENDIF

   abs_altsign: LEMMA abs(altsign(n)) = 1

   sin_coef(n): real = if even?(n) then 0 else altsign(n)/factorial(n) endif

   cos_coef(n): real = if even?(n) then altsign(n)/factorial(n) else 0 endif 


%  ----- convergent?(powerseries(sin_coef)(x)) ----

   sin_conv: LEMMA conv_powerseries?[real](sin_coef) 
                         
   sin(x): real = inf_sum(powerseq(sin_coef,x))

%  ----- convergent?(powerseries(cos_coef)(x)) ----

   cos_conv: LEMMA conv_powerseries?[real](cos_coef) 

   cos(x): real = inf_sum(powerseq(cos_coef,x))

   tan_domain: TYPE = {x: real | cos(x) /= 0}

   tan(x:tan_domain): real = sin(x)/cos(x)

   sin_0: LEMMA sin(0) = 0

   cos_0: LEMMA cos(0) = 1

    

END trig_fun