| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/trig_fnd/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 4 kB |
|
Quelle sincos_phase.pvs Sprache: PVS |
|||||||||
|
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.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28