Quellcode-Bibliothek to2pi.pvs

to2pi :THEORY
BEGIN

  IMPORTING atan2, 
            trig_ineq,
     reals@abs_lems

  a,b   : VAR real
  alpha : VAR nnreal_lt_2pi
  beta  : VAR real
  k     : VAR int

  to2pi(a) : nnreal_lt_2pi =
    LET n = floor(a/(2*pi)) IN
    a - 2*n*pi

  to2pi_id : LEMMA
    to2pi(alpha) = alpha

  to2pi_period : LEMMA
    to2pi(a) = to2pi(a+2*k*pi)

  sin_id_to2pi : LEMMA
    sin(to2pi(a)) = sin(a)

  cos_id_to2pi : LEMMA
    cos(to2pi(a)) = cos(a)

  to2pi_to2pi : LEMMA
    to2pi(to2pi(a)+b) = to2pi(a+b)

  to2pi_to2pi_sub : LEMMA
    to2pi(b-to2pi(a)) = to2pi(b-a)

  to2pi_neg : LEMMA
    -2*pi <= a AND a < 0 IMPLIES to2pi(a) = a+2*pi

  to2pi_equal : LEMMA
    to2pi(a) = to2pi(b) IMPLIES
      EXISTS(k:int): a = b + k*2*pi

  to2pi_to2pi_add : LEMMA
    to2pi(to2pi(a)+b) = to2pi(a+b)

  to2pi_closed_diff :  LEMMA
    abs(to2pi(a) - to2pi(b)) < 2*pi

  to2pi_eq: LEMMA
    FORALL (k: int): a = b + 2*k*pi IMPLIES
    to2pi(a) = to2pi(b)

  to2pi_sep : LEMMA
    a < b AND b < a + 2*pi IMPLIES 
    ((EXISTS (k:int): (a < 2*k*pi AND 2*k*pi <= b))
     OR
     (EXISTS (k: int): (2*k*pi <= a AND b < 2*(k+1)*pi)))

  sin_gt_to2pi : LEMMA
    -pi/2 <= b AND b <= pi/2 IMPLIES
   (sin(a) > sin(b) IFF b < to2pi(a+pi/2)-pi/2 AND to2pi(a+pi/2)-pi/2 < pi-b)

  sin_lt_to2pi : LEMMA
    -pi/2 <= b AND b <= pi/2 IMPLIES
   (sin(a) < sin(b) IFF b > to2pi(a+pi/2)-pi/2 OR to2pi(a+pi/2)-pi/2 > pi-b)

  sin_ge_to2pi : LEMMA
    -pi/2 <= b AND b <= pi/2 IMPLIES
   (sin(a) >= sin(b) IFF b <= to2pi(a+pi/2)-pi/2 AND to2pi(a+pi/2)-pi/2 <= pi-b)

  cos_pos_to2pi : LEMMA
    cos(a) > 0 IFF -pi/2 < to2pi(a+pi/2)-pi/2 AND to2pi(a+pi/2)-pi/2 < pi/2

  cos_nneg_to2pi : LEMMA
    cos(a) >= 0 IFF -pi/2 <= to2pi(a+pi/2)-pi/2 AND to2pi(a+pi/2)-pi/2 <= pi/2

END to2pi