Quellcode-Bibliothek 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

quality94%

¤ 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.0.14Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.