|
sincos_def: THEORY
%----------------------------------------------------------------------------
% Defining sin, cos and tan. And making the connections with the inverses.
%
% David R Lester 30/5/04
%----------------------------------------------------------------------------
BEGIN
IMPORTING sincos_phase, tan_quad
a: VAR real
%------------------------------------------------------------------------------
% the following ripped out of trig_basic and placed here...
trig_range : TYPE = {a | -1 <= a AND a <= 1}
x: VAR trig_range
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 : JUDGEMENT sin(a) HAS_TYPE trig_range
cos_range : JUDGEMENT cos(a) HAS_TYPE trig_range
sin_range_ax: LEMMA -1 <= sin(a) AND sin(a) <= 1
cos_range_ax: LEMMA -1 <= cos(a) AND cos(a) <= 1
Tan?(a) : bool = cos(a) /= 0
tan(a:(Tan?)) : real = sin(a)/cos(a)
%------------------------------------------------------------------------------
tan_rew: LEMMA FORALL (a:(Tan?)): sin(a)/cos(a) = tan(a)
% Range reduction equivalences:
sin_sin_phase: LEMMA 0 <= a AND a < 2*pi IMPLIES sin(a) = sin_phase(a)
cos_cos_phase: LEMMA 0 <= a AND a < 2*pi IMPLIES cos(a) = cos_phase(a)
sin_sin_value: LEMMA -pi/2 <= a AND a <= pi/2 IMPLIES sin(a) = sin_value(a)
cos_cos_value: LEMMA 0 <= a AND a <= pi IMPLIES cos(a) = cos_value(a)
tan_value_TCC: LEMMA -pi/2 < a AND a < pi/2 IMPLIES Tan?(a)
tan_tan_value: LEMMA -pi/2 < a AND a < pi/2 IMPLIES tan(a) = tan_value(a)
sin_asin: LEMMA sin(asin(x)) = x
cos_acos: LEMMA cos(acos(x)) = x
tan_atan: LEMMA tan(atan(a)) = a
asin_sin: LEMMA FORALL (x:real_abs_le_pi2): asin(sin(x)) = x
acos_cos: LEMMA FORALL (x:nnreal_le_pi): acos(cos(x)) = x
atan_tan: LEMMA FORALL (x:real_abs_lt_pi2): atan(tan(x)) = x
END sincos_def
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot
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
|
