| products/sources/formale sprachen/PVS/pvs-patches/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: trig_basic.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
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 ¤ Dauer der Verarbeitung: 0.25 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.Bot Zugriff |
