| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMSL/pacemakerSL/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 3 kB |
|
Quellcode-Bibliothek trig_basic.pvs Sprache: PVS |
|||||||||
|
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 Axiomatic Version % edited from trig_basic in the "trig_fnd" librart % GOAL: To reduce the amount of stuff that has to be imported %----------------------------------------------------------------------------- BEGIN IMPORTING reals@sqrt %, sincos_phase a,b,c,d : VAR real nnc : VAR nonneg_real j : VAR integer % pi_lb : real = 314/100 % pi_ub : real = 315/100 pi_lb : posreal = 31415926/10000000 pi_ub : posreal = 31415927/10000000 pi : {r:posreal | r > pi_lb AND r < pi_ub} %% ADDED %% % pi_bound : JUDGEMENT pi HAS_TYPE {r:posreal | pi_lb <= r AND r <= pi_ub} % -------------------- definition of sin and cos -------------------- trig_range : TYPE = {a | -1 <= a AND a <= 1} trig_phase : TYPE+ = {x:nnreal| x < 2*pi} CONTAINING 0 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: AXIOM -1 <= sin(a) AND sin(a) <= 1 cos_range_ax: AXIOM -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 : AXIOM 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 : AXIOM cos(0) = 1 sin_0 : LEMMA sin(0) = 0 sin_pi2 : AXIOM sin(pi/2) = 1 cos_pi2 : LEMMA cos(pi/2) = 0 tan_0 : LEMMA tan(0) = 0 % --------------------- Negative Properties ---------------------- sin_neg : AXIOM sin(-a) = -sin(a) cos_neg : AXIOM cos(-a) = cos(a) tan_neg : LEMMA FORALL(a:(Tan?)): tan(-a) = -tan(a) % -------------------- Co-Function Identities ----------------------- cos_sin : AXIOM 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 : AXIOM sin(pi) = 0 cos_pi : AXIOM 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 : AXIOM sin(2*pi) = 0 cos_2pi : AXIOM cos(2*pi) = 1 tan_2pi : LEMMA tan(2*pi) = 0 % ----------------- Sum and Difference of Two Angles ---------------- sin_plus : AXIOM 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) sin_pi_minus: LEMMA sin(pi - a) = sin(a) cos_pi_minus: LEMMA cos(pi - a) = -cos(a) 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 : AXIOM 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 : AXIOM 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 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) tan_eq_0 : LEMMA FORALL (a: (Tan?)): (tan(a) = 0 IFF EXISTS (i: int): a = i * pi) % ---------------------- 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 ¤ 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.0.12Bemerkung: (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28