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