Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: trig_fun.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.