|
trig_basic : THEORY
%-----------------------------------------------------------------------------
% trig_basic:
% -----------
% - definition of pi with crude upper and lower bounds
% - definition of sin, cos, and tan
% - pythagorean properties: sq(sin(a)) + sq(cos(a)) = 1
% - sum and difference of two angles
% - double angle formulas
% - negative properties, e.g. sin(-a)
% - periodicity, e.g. sin(a) = sin(a + 2 * j * pi)
% - co-function identities, e.g. sin(pi/2 - a) = cos(a)
% - location of zeros of trig functions
%
% Version 1.1 27/10/03 Foundational Version David Lester
%
% CHANGES
% - Oct 21 2004 (C. Munoz) Moved pi_lb, pi_ub, pi_bound to atan_approx
%
%-----------------------------------------------------------------------------
BEGIN
IMPORTING reals@sqrt, sincos_def, atan_approx
a,b,c,d : VAR real
nnc : VAR nonneg_real
j : VAR integer
% This is now in atan_approx.pvs
%
% pi_lb : real = 31415926/10000000
%
% pi_ub : real = 31415927/10000000
%
% pi_bound : JUDGEMENT pi HAS_TYPE {r:posreal | pi_lb < r AND r < pi_ub}
% -------------------- definition of sin and cos --------------------
%
% This is now in sincos_def.pvs
%
% trig_range : TYPE = {a | -1 <= a AND a <= 1}
%
% sin(x:real) : real = sin_phase(x-2*pi*floor(x/(2*pi)))
% cos(x:real) : real = cos_phase(x-2*pi*floor(x/(2*pi)))
%
% sin_range_ax: LEMMA -1 <= sin(a) AND sin(a) <= 1
% cos_range_ax: LEMMA -1 <= cos(a) AND cos(a) <= 1
%
% sin_range : JUDGEMENT sin(a) HAS_TYPE trig_range
% cos_range : JUDGEMENT cos(a) HAS_TYPE trig_range
%
% Tan?(a) : bool = cos(a) /= 0
%
% tan(a:(Tan?)) : real = sin(a)/cos(a)
% -------------------- Pythagorean Property --------------------
sin2_cos2 : LEMMA sq(sin(a)) + sq(cos(a)) = 1
cos2 : LEMMA sq(cos(a)) = 1 - sq(sin(a))
sin2 : LEMMA sq(sin(a)) = 1 - sq(cos(a))
% --------------------- Basic Values ----------------------------
cos_0 : LEMMA cos(0) = 1
sin_0 : LEMMA sin(0) = 0
sin_pi2 : LEMMA sin(pi/2) = 1
cos_pi2 : LEMMA cos(pi/2) = 0
tan_0 : LEMMA tan(0) = 0
% --------------------- Negative Properties ----------------------
sin_neg : LEMMA sin(-a) = -sin(a)
cos_neg : LEMMA cos(-a) = cos(a)
tan_neg : LEMMA FORALL(a:(Tan?)): tan(-a) = -tan(a)
% -------------------- Co-Function Identities -----------------------
cos_sin : LEMMA cos(a) = sin(a+pi/2)
sin_cos : LEMMA sin(a) = -cos(a+pi/2)
sin_shift : LEMMA sin(pi/2 - a) = cos(a)
cos_shift : LEMMA cos(pi/2 - a) = sin(a)
% --------------------- Arguments involving pi ---------------------
neg_cos : LEMMA -cos(a) = cos(a+pi)
neg_sin : LEMMA -sin(a) = sin(a+pi)
sin_pi : LEMMA sin(pi) = 0
cos_pi : LEMMA cos(pi) = -1
tan_pi : LEMMA tan(pi) = 0
sin_3pi2 : LEMMA sin(3*pi/2) = -1
cos_3pi2 : LEMMA cos(3*pi/2) = 0
sin_2pi : LEMMA sin(2*pi) = 0
cos_2pi : LEMMA cos(2*pi) = 1
tan_2pi : LEMMA tan(2*pi) = 0
% ----------------- Sum and Difference of Two Angles ----------------
sin_plus : LEMMA sin(a + b) = sin(a)*cos(b) + cos(a)*sin(b)
sin_minus : LEMMA sin(a - b) = sin(a)*cos(b) - sin(b)*cos(a)
cos_plus : LEMMA cos(a + b) = cos(a)*cos(b) - sin(a)*sin(b)
cos_minus : LEMMA cos(a - b) = cos(a)*cos(b) + sin(a)*sin(b)
tan_plus : LEMMA Tan?(a) AND Tan?(b) AND Tan?(a+b) AND
tan(a) * tan(b) /= 1 IMPLIES
tan(a + b) = (tan(a) + tan(b))/(1 - tan(a)*tan(b))
tan_minus : LEMMA Tan?(a) AND Tan?(b) AND Tan?(a-b) AND
tan(a) * tan(b) /= -1 IMPLIES
tan(a - b) = (tan(a) - tan(b))/(1 + tan(a)*tan(b))
arc_sin_cos : LEMMA sq(a)+sq(b)=sq(c) IMPLIES
EXISTS d: a = c*cos(d) AND b = c*sin(d)
pythagorean : LEMMA sq(a)+sq(b)=sq(nnc) IMPLIES
EXISTS(alpha:real): nnc=a*cos(alpha)+b*sin(alpha)
% -------------------- Double Angle Formulas --------------------
sin_2a : LEMMA sin(2*a) = 2 * sin(a) * cos(a)
cos_2a : LEMMA cos(2*a) = cos(a)*cos(a) - sin(a)*sin(a)
cos_2a_cos : LEMMA cos(2*a) = 2 * cos(a)*cos(a) - 1
cos_2a_sin : LEMMA cos(2*a) = 1 - 2 * sin(a)*sin(a)
tan_2a : LEMMA Tan?(a) AND Tan?(2*a) AND
tan(a) * tan(a) /= 1 IMPLIES
tan(2*a) = 2 * tan(a)/(1 - tan(a) * tan(a))
% ------------------------- Periodicity -----------------------------
% IMPORTING reals@prelude_aux_reals
n: VAR nat
k: VAR integer
sin_period : LEMMA sin(a) = sin(a + 2 * j * pi)
cos_period : LEMMA cos(a) = cos(a + 2 * j * pi)
tan_period : LEMMA Tan?(a) IMPLIES tan(a) = tan(a + j * pi)
sin_k_pi : LEMMA sin(k*pi) = 0
cos_2k_pi : LEMMA cos(2*k*pi) = 1
cos_k_pi : LEMMA cos(k*pi) = (-1)^(k)
sin_k_pi2 : LEMMA sin(k*pi + pi/2) = (-1)^k
tan_k_pi : LEMMA tan(k*pi) = 0
% -------------------- Characterization of zeroes -------------------
sin_eq_0_2pi : COROLLARY 0 <= a AND a <= 2*pi IMPLIES
(sin(a)=0 IFF a=0 OR a=pi OR a=2*pi)
cos_eq_0_2pi : COROLLARY 0 <= a AND a <= 2*pi IMPLIES
(cos(a)=0 IFF a=pi/2 OR a=3*pi/2)
sin_eq_0 : LEMMA sin(a) = 0 IFF EXISTS (i: int): a = i * pi
cos_eq_0 : LEMMA cos(a) = 0 IFF EXISTS (i: int): a = i * pi + pi/2
% ---------------------- Maximum Points -----------------------------
sin_eq_1 : LEMMA sin(a) = 1 IFF EXISTS (i: int): a = 2 * i * pi + pi/2
cos_eq_1 : LEMMA cos(a) = 1 IFF EXISTS (i: int): a = 2 * i * pi
END trig_basic
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
