|
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
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
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.
|
