Quelle  atan2_props.pvs

atan2_props: THEORY
BEGIN

  IMPORTING atan2, trig_ineq

  atan2_is_0:    LEMMA FORALL (x:real,y:{z:real | x = 0 => z/=0}):
                           atan2(x,y) =   0    IFF (x > 0 AND y = 0)

  atan2_is_pi2:  LEMMA FORALL (x:real,y:{z:real | x = 0 => z/=0}):
                           atan2(x,y) =   pi/2 IFF (x = 0 AND y > 0)

  atan2_is_pi:   LEMMA FORALL (x:real,y:{z:real | x = 0 => z/=0}):
                           atan2(x,y) =   pi   IFF (x < 0 AND y = 0)

  atan2_is_3pi2: LEMMA FORALL (x:real,y:{z:real | x = 0 => z/=0}):
                           atan2(x,y) = 3*pi/2 IFF (x = 0 AND y < 0)

  atan2_quad1:   LEMMA FORALL (x:real,y:{z:real | x = 0 => z/=0}):
                           (0 < atan2(x,y) AND atan2(x,y) < pi/2) IFF
                                                              (x > 0 AND y > 0)

  atan2_quad2:   LEMMA FORALL (x:real,y:{z:real | x = 0 => z/=0}):
                           (pi/2 < atan2(x,y) AND atan2(x,y) < pi) IFF
                                                              (x < 0 AND y > 0)

  atan2_quad3:   LEMMA FORALL (x:real,y:{z:real | x = 0 => z/=0}):
                           (pi < atan2(x,y) AND atan2(x,y) < 3*pi/2) IFF
                                                              (x < 0 AND y < 0)

  atan2_quad4:   LEMMA FORALL (x:real,y:{z:real | x = 0 => z/=0}):
                           (3*pi/2 < atan2(x,y) AND atan2(x,y) < 2*pi) IFF
                                                              (x > 0 AND y < 0)

  %% ------------ atan2 values -------------------------------------


   IMPORTING trig_values, atan_values

   nzx: VAR nzreal

   atan2_0x      : LEMMA atan2(0,nzx) = IF nzx > 0 THEN pi/2 ELSE 3*pi/2 ENDIF
   atan2_x0      : LEMMA atan2(nzx,0) = IF nzx > 0 THEN 0 ELSE pi ENDIF

   atan2_11      : LEMMA atan2(1,1) = pi/4
   atan2_m11     : LEMMA atan2(-1,1) = 3*pi/4
   atan2_1m1     : LEMMA atan2(1,-1) = 7*pi/4
   atan2_m1m1    : LEMMA atan2(-1,-1) = 5*pi/4


   atan2_1sqrt3  : LEMMA atan2(1,sqrt(3)) = pi/3
   atan2_sqrt3   : LEMMA atan2(sqrt(3),1) = pi/6


   atan2_m1sqrt3 : LEMMA atan2(-1,sqrt(3)) = 2*pi/3
   atan2_sqrt3m1 : LEMMA atan2(sqrt(3),-1) = 11*pi/6


END atan2_props