|
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.1 Sekunden
(vorverarbeitet)
¤
|
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.
|
