Quellcode-Bibliothek atan2.pvs

atan2 : THEORY
%-----------------------------------------------------------------------------
%      atan2(x,y)
%      ----
%         - defines two-argument inverse tangent (arctangent): atan2
%
%      
%-----------------------------------------------------------------------------
BEGIN

  IMPORTING atan

  x,y,
  w,z   : VAR real
  a     : VAR {z:nnreal| z < 2*pi}
  nz    : VAR negreal
  pz    : VAR posreal

  %% Arc tangent of y/x taking into in account quadrants and indefinitions
  %% Polar angle of x + yI. 
  atan2(x:real,y:{z:real|x=0 => z/=0}): real
    = IF    x > 0 THEN IF y >= 0 THEN atan(y/x) ELSE 2*pi+atan(y/x) ENDIF
      ELSIF x = 0 THEN IF y >  0 THEN pi/2      ELSE 3*pi/2         ENDIF
                  ELSE pi + atan(y/x)                                    ENDIF

  atan2_0_2pi : LEMMA
    (x /= 0 OR y /= 0) IMPLIES
      (((x>=0 AND y>=0) => (0 <= atan2(x,y) AND atan2(x,y) <= pi/2))  AND
       ((x< 0 AND y>=0) => (pi/2 < atan2(x,y) AND atan2(x,y) <= pi)) AND
       ((x< 0 AND y< 0) => (pi < atan2(x,y)  AND atan2(x,y) < 3*pi/2)) AND
       ((x>=0 AND y< 0) => (3*pi/2 <= atan2(x,y)  AND atan2(x,y) < 2*pi)))

  atan2_ge_0_lt_2pi : LEMMA
    (x /= 0 OR y /= 0) IMPLIES
    atan2(x,y) >= 0 and
    atan2(x,y) < 2*pi

  nnreal_lt_2pi: NONEMPTY_TYPE = {x:nnreal | x < 2*pi} 

  JUDGEMENT atan2(x:real,y:{z:real|x=0 => z/=0}) HAS_TYPE nnreal_lt_2pi

  atan2_cancel_pos : LEMMA
    (x /= 0 OR y /= 0) IMPLIES atan2(x*pz,y*pz) = atan2(x,y)

  atan2_cancel_neg : LEMMA
    (x /= 0 OR y /= 0) IMPLIES
       atan2(x*nz,y*nz) =
           IF y > 0 OR (y = 0 AND x > 0) THEN atan2(x,y) + pi
                                         ELSE atan2(x,y) - pi ENDIF

  atan2_swap_pos : LEMMA
    x*y > 0 IMPLIES
    atan2(x,y) = atan2(y,x) + atan((y ^ 2 - x ^ 2) / (2 * (x * y)))

  atan2_swap_neg : LEMMA
    x*y < 0 IMPLIES
    atan2(x,y) =  atan2(y,x) + atan((y ^ 2 - x ^ 2) / (2 * (x * y))) + sign(x)*pi

  atan2_swap_zero : LEMMA
    (x = 0 AND y /= 0 IMPLIES
      atan2(x,y) = atan2(y,x) + pi/2) AND
    (y = 0 AND x /= 0 IMPLIES      
      atan2(x,y) = atan2(y,x) - pi/2)

  atan2_cos_sin : AXIOM
    atan2(cos(a),sin(a)) = a

  sin_atan2 : AXIOM
    (x /= 0 OR y /= 0) IMPLIES 
      sin(atan2(x,y)) = 
        IF x=0 THEN 
          IF y > 0 THEN 1 ELSE -1 ENDIF
        ELSE 
          LET yx = y/x IN 
          LET r = yx/sqrt((sq(yx)+1)) IN
            IF x > 0 THEN r
            ELSE -r
            ENDIF
        ENDIF

  cos_atan2 : AXIOM
    (x /= 0 OR y /= 0) IMPLIES
      cos(atan2(x,y)) = 
        IF x = 0 THEN 0 
        ELSE
          LET yx = y/x IN
          IF  x > 0 THEN 1/sqrt((sq(yx)+1)) 
          ELSE -1/sqrt((sq(yx)+1)) 
          ENDIF
        ENDIF

END atan2