Quelle atan2.pvs Sprache: PVS

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

  IMPORTING trig_basic, atan, asin, acos

  x,y   : 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 : LEMMA
    atan2(cos(a),sin(a)) = a

  sin_atan2 : LEMMA
    (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 : LEMMA
    (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

quality100%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.