|
trig_extra : THEORY
%-----------------------------------------------------------------------------
% trig_extra
% ----------
% - reduction theorems
% - sum and product identities
% - half-angle identities and zeros
% - triple angle formulas
%-----------------------------------------------------------------------------
BEGIN
IMPORTING trig_basic, trig_values
a,b : VAR real
% ------------------------- Reduction Theorems -------------------------
sin_minus_2pi : LEMMA sin(a - 2*pi) = sin(a)
cos_minus_2pi : LEMMA cos(a - 2*pi) = cos(a)
tan_minus_2pi : LEMMA cos(a) /= 0 IMPLIES tan(a - 2*pi) = tan(a)
sin_minus_3pi2 : LEMMA sin(a - 3*pi/2) = cos(a)
cos_minus_3pi2 : LEMMA cos(a - 3*pi/2) = - sin(a)
tan_minus_3pi2 : LEMMA sin(a) /= 0 AND cos(a) /= 0
IMPLIES tan(a - 3*pi/2) = - 1/tan(a)
sin_minus_pi : LEMMA sin(a - pi) = - sin(a)
cos_minus_pi : LEMMA cos(a - pi) = - cos(a)
tan_minus_pi : LEMMA cos(a) /= 0 IMPLIES tan(a - pi) = tan(a)
sin_minus_pi2 : LEMMA sin(a - pi/2) = - cos(a)
cos_minus_pi2 : LEMMA cos(a - pi/2) = sin(a)
tan_minus_pi2 : LEMMA sin(a) /= 0 AND cos(a) /= 0
IMPLIES tan(a - pi/2) = - 1/tan(a)
sin_2pi_minus : LEMMA sin(2*pi - a) = - sin(a)
cos_2pi_minus : LEMMA cos(2*pi - a) = cos(a)
tan_2pi_minus : LEMMA sin(a) /= 0 AND cos(a) /= 0
IMPLIES tan(2*pi - a) = - tan(a)
sin_3pi2_minus : LEMMA sin(3*pi/2 - a) = - cos(a)
cos_3pi2_minus : LEMMA cos(3*pi/2 - a) = - sin(a)
tan_3pi2_minus : LEMMA sin(a) /= 0 AND cos(a) /= 0
IMPLIES tan(3*pi/2 - a) = 1/tan(a)
sin_pi_minus : LEMMA sin(pi - a) = sin(a)
cos_pi_minus : LEMMA cos(pi - a) = - cos(a)
tan_pi_minus : LEMMA cos(a) /= 0 IMPLIES tan(pi - a) = - tan(a)
sin_pi2_minus : LEMMA sin(pi/2 - a) = cos(a)
cos_pi2_minus : LEMMA cos(pi/2 - a) = sin(a)
tan_pi2_minus : LEMMA sin(a) /= 0 AND cos(a) /= 0
IMPLIES tan(pi/2 - a) = 1/tan(a)
% ------------------------- Sum and Product Formulas -------------------------
sin_times_cos : LEMMA sin(a)*cos(b) = (sin(a+b) + sin(a-b))/2
cos_times_cos : LEMMA cos(a)*cos(b) = (cos(a+b) + cos(a-b))/2
sin_times_sin : LEMMA sin(a)*sin(b) = (cos(a-b) - cos(a+b))/2
sin_sum : LEMMA sin(a) + sin(b) = 2 * sin((a+b)/2)*cos((a-b)/2)
sin_diff : LEMMA sin(a) - sin(b) = 2 * cos((a+b)/2)*sin((a-b)/2)
cos_sum : LEMMA cos(a) + cos(b) = 2 * cos((a+b)/2)*cos((a-b)/2)
cos_diff : LEMMA cos(a) - cos(b) = - 2 * sin((a+b)/2)*sin((a-b)/2)
tan_diff : LEMMA Tan?(a) AND Tan?(b) IMPLIES
tan(a) - tan(b) = sin(a-b)/(cos(a)*cos(b))
% ------------------------- Squares of sin and cos -------------------------
sq_sin : LEMMA sq(sin(a)) = (1-cos(2*a))/2
sq_cos : LEMMA sq(cos(a)) = (1+cos(2*a))/2
sin_half_zeroes : LEMMA sin(a/2) = 0 IFF 1-cos(a) = 0
cos_half_zeroes : LEMMA cos(a/2) = 0 IFF 1+cos(a) = 0
cos_half_zeroes2 : LEMMA cos(a/2) = 0 IMPLIES sin(a) = 0
sq_tan : LEMMA (1+cos(2*a)) /= 0
IMPLIES sq(tan(a)) = (1-cos(2*a))/(1+cos(2*a))
% ------------------------- Half Angle Formulas -------------------------
IMPORTING trig_ineq
sin_half : LEMMA
( 0 <= a/2 AND a/2 <= pi IMPLIES
sin(a/2) = sqrt((1-cos(a))/2)) AND
( pi <= a/2 AND a/2 <= 2*pi IMPLIES
sin(a/2) = -sqrt((1-cos(a))/2))
cos_half : LEMMA
( 0 <= a/2 AND a/2 <= pi/2 IMPLIES
cos(a/2) = sqrt((1+cos(a))/2)) AND
( pi/2 <= a/2 AND a/2 <= 3*pi/2 IMPLIES
cos(a/2) = -sqrt((1+cos(a))/2)) AND
( 3*pi/2 <= a/2 AND a/2 <= 2*pi IMPLIES
cos(a/2) = sqrt((1+cos(a))/2))
tan_half : LEMMA
cos(a) /= -1 IMPLIES tan(a/2) = sin(a)/(1 + cos(a))
tan_half2 : LEMMA
sin(a) /= 0 IMPLIES tan(a/2) = (1 - cos(a))/sin(a)
% ---------------------- Triple Angle Formulas ----------------------
sin_3a : LEMMA sin(3*a) = 3 * sin(a) - 4 * expt(sin(a),3)
cos_3a : LEMMA cos(3*a) = 4 * expt(cos(a),3) - 3 * cos(a)
% ---------------------- Base equations ---------------------
sin_eq_sin : LEMMA sin(a) = sin(b) <=>
(EXISTS (k: int): (a = b + 2*k*pi) OR (a = pi - b + 2*k*pi))
cos_eq_cos : LEMMA cos(a) = cos(b) <=>
(EXISTS (k: int): (a = b + 2*k*pi) OR (a = -b + 2*k*pi))
tan_eq_tan : LEMMA Tan?(a) AND Tan?(b) IMPLIES
( tan(a) = tan(b) <=> (EXISTS (k: int): (a = b + k*pi)) )
sin_cos_eq: LEMMA FORALL (a,b: {x:nnreal | x < 2*pi}):
sin(a) = sin(b) AND cos(a) = cos(b)
IMPLIES a = b
sin_eq_cos: LEMMA sin(a) = cos(a) IMPLIES (EXISTS (i:int): a = pi/4 + i*pi)
tan_eq_1 : LEMMA Tan?(a) AND tan(a) = 1 IMPLIES (EXISTS (i:int): a = pi/4 + i*pi)
i,j: VAR integer
sin_eq_pm1 : LEMMA sin(a) = (-1)^i IFF (EXISTS j: a = (i+2*j)*pi + pi/2)
cos_eq_pm1 : LEMMA cos(a) = (-1)^i IFF (EXISTS j: a = (i+2*j)*pi)
% --------------------- Superposition ----------------------
A,B: VAR real
C: VAR nzreal
x,y,del,W, alpha: VAR real
sin_plus_cos: LEMMA sq(C) = sq(A) + sq(B) AND sin(del) = B/C
AND cos(del) = A/C IMPLIES
A*sin(x) + B*cos(x) = C*sin(x+del)
spc_tan_prep: LEMMA A /= 0 AND Tan?(del) AND tan(del) = B/A AND
sq(C) = sq(A) + sq(B) IMPLIES
sq(sin(del)) = sq(B/C) AND sq(cos(del)) = sq(A/C)
IMPORTING atan2
sin_plus_cos_atan2: LEMMA
x /= 0 OR y /= 0 IMPLIES
x*sin(alpha) + y*cos(alpha) = sqrt(sq(x)+sq(y))*sin(alpha + atan2(x,y))
% sin_superpos: LEMMA A + B*cos(W) = C*cos(del) AND % need to find f:
% B*sin(W) = C*sin(del) % del = f(A,B,C,W)
% IMPLIES
% A*sin(x) + B*sin(x+W) = C*sin(x+del)
END trig_extra
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.18Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
