| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/series/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
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 ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28