|
sincos_phase: THEORY
%------------------------------------------------------------------------------
%
% Definitions of sin and cos from infinite series
%
% David Lester Manchester University
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING sincos_quad
trig_phase: NONEMPTY_TYPE = {x:nnreal| x < 2*pi} CONTAINING 0
x,y: VAR trig_phase
px,py: VAR {x:posreal| x < 2*pi}
xa: VAR real_abs_le1
% Principle Phase [0,2*pi)
sin_phase(x:trig_phase):real_abs_le1
= LET i = floor((2*x)/pi) IN
IF i = 0 THEN sin_value(x)
ELSIF i = 1 THEN sin_value(pi-x)
ELSIF i = 2 THEN -sin_value(x-pi)
ELSE -sin_value(2*pi-x)
ENDIF
cos_phase(x:trig_phase):real_abs_le1
= LET i = floor(x/pi) IN
IF i = 0 THEN cos_value(x) ELSE cos_value(2*pi-x) ENDIF
phase_sin_q1: LEMMA floor((2*x)/pi) = 0 IFF 0 <= x AND x < pi/2
phase_sin_q2: LEMMA floor((2*x)/pi) = 1 IFF pi/2 <= x AND x < pi
phase_sin_q3: LEMMA floor((2*x)/pi) = 2 IFF pi <= x AND x < 3*pi/2
phase_sin_q4: LEMMA floor((2*x)/pi) = 3 IFF 3*pi/2 <= x AND x < 2*pi
phases_sin: LEMMA floor((2*x)/pi) = 0 OR floor((2*x)/pi) = 1 OR
floor((2*x)/pi) = 2 OR floor((2*x)/pi) = 3
sin_q1: LEMMA floor((2*x)/pi) = 0 => sin_phase(x) = sin_value(x)
sin_q2: LEMMA floor((2*x)/pi) = 1 => sin_phase(x) = cos_value(x-pi/2)
sin_q3: LEMMA floor((2*x)/pi) = 2 => sin_phase(x) = -sin_value(x-pi)
sin_q4: LEMMA floor((2*x)/pi) = 3 => sin_phase(x) = -cos_value(x-3*pi/2)
phase_cos_q1: LEMMA floor(x/pi) = 0 IFF 0 <= x AND x < pi
phase_cos_q2: LEMMA floor(x/pi) = 1 IFF pi <= x AND x < 2*pi
phases_cos: LEMMA floor(x/pi) = 0 OR floor(x/pi) = 1
cos_q1: LEMMA floor((2*x)/pi) = 0 => cos_phase(x) = cos_value(x)
cos_q2: LEMMA floor((2*x)/pi) = 1 => cos_phase(x) = -sin_value(x-pi/2)
cos_q3: LEMMA floor((2*x)/pi) = 2 => cos_phase(x) = -cos_value(x-pi)
cos_q4: LEMMA floor((2*x)/pi) = 3 => cos_phase(x) = sin_value(x-3*pi/2)
sin_h2: LEMMA floor(x/pi) = 1 => sin_phase(x) = -sin_phase(x-pi)
sin_h1: LEMMA floor(x/pi) = 0 => sin_phase(x) = -sin_phase(x+pi)
cos_h1: LEMMA floor(x/pi) = 0 => cos_phase(x) = -cos_phase(x+pi)
cos_h2: LEMMA floor(x/pi) = 1 => cos_phase(x) = -cos_phase(x-pi)
sin_phase_neg: LEMMA sin_phase(2*pi-px) = -sin_phase(px)
cos_phase_neg: LEMMA cos_phase(2*pi-px) = cos_phase(px)
sin_eqv_cos_phase: LEMMA
sin_phase(x) = IF x < 3*pi/2 THEN -cos_phase(pi/2+x)
ELSE -cos_phase(x-3*pi/2) ENDIF
cos_eqv_sin_phase: LEMMA
cos_phase(x) = IF x < 3*pi/2 THEN sin_phase(pi/2+x)
ELSE sin_phase(x-3*pi/2) ENDIF
sin_phase_inv: LEMMA
sin_phase(x) = IF x < pi THEN -sin_phase(x+pi) ELSE -sin_phase(x-pi) ENDIF
cos_phase_inv: LEMMA
cos_phase(x) = IF x < pi THEN -cos_phase(x+pi) ELSE -cos_phase(x-pi) ENDIF
sin_phase_3pi2: LEMMA sin_phase(3*pi/2) = -1
sin_phase_0: LEMMA sin_phase(0) = 0
sin_phase_pi4: LEMMA sin_phase(pi/4) = sqrt(1/2)
sin_phase_pi2: LEMMA sin_phase(pi/2) = 1
cos_phase_0: LEMMA cos_phase(0) = 1
cos_phase_pi4: LEMMA cos_phase(pi/4) = sqrt(1/2)
cos_phase_pi2: LEMMA cos_phase(pi/2) = 0
cos_phase_pi: LEMMA cos_phase(pi) = -1
sin_phase_asin: LEMMA IF xa < 0 THEN sin_phase(asin(xa)+2*pi)
ELSE sin_phase(asin(xa)) ENDIF = xa
cos_phase_acos: LEMMA cos_phase(acos(xa)) = xa
sin2_cos2_phase: LEMMA sq(sin_phase(x))+sq(cos_phase(x)) = 1
sin_phase_diff: LEMMA sin_phase(x)*cos_phase(y)-cos_phase(x)*sin_phase(y)
= IF x-y >= 0 THEN sin_phase(x-y) ELSE sin_phase(x-y+2*pi) ENDIF
cos_phase_sum: LEMMA cos_phase(x)*cos_phase(y)-sin_phase(x)*sin_phase(y)
= IF x+y < 2*pi THEN cos_phase(x+y) ELSE cos_phase(x+y-2*pi) ENDIF
cos_phase_diff: LEMMA cos_phase(x)*cos_phase(y)+sin_phase(x)*sin_phase(y)
= IF x-y >= 0 THEN cos_phase(x-y) ELSE cos_phase(x-y+2*pi) ENDIF
sin_phase_sum: LEMMA sin_phase(x)*cos_phase(y)+cos_phase(x)*sin_phase(y)
= IF x+y < 2*pi THEN sin_phase(x+y) ELSE sin_phase(x+y-2*pi) ENDIF
END sincos_phase
¤ Dauer der Verarbeitung: 0.18 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.
|
