|
%------------------------------------------------------------------------------
% sin/cos
%
% Author: David Lester, Manchester University
%
% Version 1.0 18/2/09 Initial Release Version
%------------------------------------------------------------------------------
sincosx: THEORY
BEGIN
IMPORTING prelude_aux, atanx, trig_fnd@sincos, trig_fnd@trig_values,
reals@factorial_props, trig_fnd@trig_approx, remx
n,p: VAR nat
x: VAR real
cx: VAR cauchy_real
real_3pi16: TYPE+ = {x | -3*pi/16 < x & x < 3*pi/16} CONTAINING 0
cauchy_real_3pi16?(c:[nat->int]):bool
=EXISTS (x:real_3pi16): cauchy_prop(x,c)
cauchy_real_3pi16: TYPE+=(cauchy_real_3pi16?) CONTAINING (LAMBDA p:0)
nnsreal: TYPE+ = {x | 0 <= x & x < 1/2} CONTAINING 0
cauchy_nnsreal?(c:[nat->int]):bool = EXISTS (x:nnsreal): cauchy_prop(x,c)
cauchy_nnsreal: TYPE+=(cauchy_nnsreal?) CONTAINING (LAMBDA p:0)
JUDGEMENT nnsreal SUBTYPE_OF nnreal
JUDGEMENT cauchy_nnsreal SUBTYPE_OF cauchy_real
JUDGEMENT cauchy_real_3pi16 SUBTYPE_OF cauchy_real
sx: VAR real_3pi16
snx: VAR nnsreal
csx: VAR cauchy_real_3pi16
ssx: VAR ssmallreal
cssx: VAR cauchy_ssmallreal
csnx: VAR cauchy_nnsreal
cauchy_sin_series(n):cauchy_real
= cauchy_div(cauchy_int((-1)^n),cauchy_int(factorial(2*n+1)))
cauchy_cos_series(n):cauchy_real
= cauchy_div(cauchy_int((-1)^n),cauchy_int(factorial(2*n)))
sin_series_lemma: LEMMA cauchy_prop(sin_term(1)(n), cauchy_sin_series(n))
cos_series_lemma: LEMMA cauchy_prop(cos_term(1)(n), cauchy_cos_series(n))
cauchy_sin_drx(csnx): cauchy_real
= (LAMBDA p: round(cauchy_powerseries(csnx,cauchy_sin_series,p+2)(p+2)/4))
cauchy_cos_drx(csnx): cauchy_real
= (LAMBDA p: round(cauchy_powerseries(csnx,cauchy_cos_series,p+2)(p+2)/4))
sin_drx_lemma: LEMMA cauchy_prop(snx,csnx) AND snx /= 0 =>
cauchy_prop(sin(sqrt(snx))/sqrt(snx),cauchy_sin_drx(csnx))
cauchy_sin_dr(csx): cauchy_real
= cauchy_mul(csx,cauchy_sin_drx(cauchy_mul(csx,csx)))
cauchy_cos_dr(csx): cauchy_real = cauchy_cos_drx(cauchy_mul(csx,csx))
sin_dr_lemma: LEMMA cauchy_prop(sx,csx) =>
cauchy_prop(sin(sx),cauchy_sin_dr(csx))
cos_dr_lemma: LEMMA cauchy_prop(sx,csx) =>
cauchy_prop(cos(sx),cauchy_cos_dr(csx))
cauchy_sin(cx): cauchy_real
= LET p2 = cauchy_div2n(cauchy_pi,2),
s2 = cauchy_sqrt(cauchy_div2n(cauchy_int(1),1)),
s = round(cauchy_div(cx,p2)(2)/4),
n = remx(8)(s),
cy = cauchy_sub(cx, cauchy_mul(p2, cauchy_int(s))),
sin = cauchy_sin_dr(cy),
cos = cauchy_cos_dr(cy)
IN IF n = 0 THEN sin
ELSIF n = 1 THEN cauchy_mul(s2, cauchy_add(cos, sin))
ELSIF n = 2 THEN cos
ELSIF n = 3 THEN cauchy_mul(s2, cauchy_sub(cos, sin))
ELSIF n = 4 THEN cauchy_neg(sin)
ELSIF n = 5 THEN cauchy_neg(cauchy_mul(s2, cauchy_add(cos, sin)))
ELSIF n = 6 THEN cauchy_neg(cos)
ELSE cauchy_neg(cauchy_mul(s2, cauchy_sub(cos, sin)))
ENDIF
sin_lemma: LEMMA cauchy_prop(x,cx) => cauchy_prop(sin(x),cauchy_sin(cx))
cauchy_cos(cx): cauchy_real
= LET p2 = cauchy_div2n(cauchy_pi,2),
s2 = cauchy_sqrt(cauchy_div2n(cauchy_int(1),1)),
s = round(cauchy_div(cx,p2)(2)/4),
n = remx(8)(s),
cy = cauchy_sub(cx, cauchy_mul(p2, cauchy_int(s))),
sin = cauchy_sin_dr(cy),
cos = cauchy_cos_dr(cy)
IN IF n = 0 THEN cos
ELSIF n = 1 THEN cauchy_mul(s2, cauchy_sub(cos, sin))
ELSIF n = 2 THEN cauchy_neg(sin)
ELSIF n = 3 THEN cauchy_neg(cauchy_mul(s2, cauchy_add(cos, sin)))
ELSIF n = 4 THEN cauchy_neg(cos)
ELSIF n = 5 THEN cauchy_neg(cauchy_mul(s2, cauchy_sub(cos, sin)))
ELSIF n = 6 THEN sin
ELSE cauchy_mul(s2, cauchy_add(cos, sin))
ENDIF
cos_lemma: LEMMA cauchy_prop(x,cx) => cauchy_prop(cos(x),cauchy_cos(cx))
END sincosx
¤ Dauer der Verarbeitung: 0.0 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.
|
