Quelle  trig_degree.pvs

trig_degree : THEORY
%-----------------------------------------------------------------------------
%      trig_degree
%      -----------
%         - trig functions that take arguments in degrees: sind, cosd
%         - defines conversions toRad, toDeg
%
%  CHANGES
%     - SIN_pos and COS_pos renamed sind_bound and cosd_bound
%-----------------------------------------------------------------------------
BEGIN
  IMPORTING trig_basic,trig_approx,trig_ineq

  a : VAR real
  n : VAR posnat

  toRad(a)      : real = a*pi/180

  toDeg(a)      : real = a*180/pi

  rad_deg       : LEMMA toRad(toDeg(a)) = a

  deg_rad       : LEMMA toDeg(toRad(a)) = a

  sind(a)       : real = sin(toRad(a))

  cosd(a)       : real = cos(toRad(a))

  tand(a:real|Tan?(toRad(a))) : real = tan(toRad(a))

  sq_sin_cos_d_one : LEMMA  sq(sind(a)) + sq(cosd(a)) = 1

  sind_bounds : LEMMA 0 <= a AND a <= 90 IMPLIES
                      sind(a) >= sin_lb(a*pi_lb/180,n)

  cosd_bounds : LEMMA  0 <= a AND a <= 90 IMPLIES
                      cosd(a) <= cos_ub(a*pi_lb/180,n) 

END trig_degree