|
%------------------------------------------------------------------------------
% Sqrare root properties of Complex Numbers.
%
% Author: David Lester, Manchester University
%
% Version 1.0 4/11/07 Initial version (DRL)
%------------------------------------------------------------------------------
complex_sqrt: THEORY
BEGIN
IMPORTING polar, trig@trig_basic, number_fields_sq
nnx: VAR nnreal
npx: VAR npreal
x,y,z: VAR complex
n0x,n0y,n0z: VAR nzcomplex
sqrt(z):complex = from_polar(sqrt(abs(z)),arg(z)/2)
sqrt_nz_is_nz : JUDGEMENT sqrt(n0z) HAS_TYPE nzcomplex
sqrt_nnz : LEMMA sqrt(nnx) = sqrt.sqrt(nnx)
sqrt_npz : LEMMA sqrt(npx) = i*sqrt.sqrt(-npx)
sqrt_0 : LEMMA sqrt(0) = 0
sqrt_1 : LEMMA sqrt(1) = 1
sqrt_neg1 : LEMMA sqrt(-1) = i
sqrt_eq_0 : LEMMA sqrt(z) = 0 IFF z = 0
sqrt_sq : LEMMA sqrt(sq(z)) = IF -pi/2 < arg(z) AND arg(z) <= pi/2
THEN z ELSE -z ENDIF
sq_sqrt : LEMMA sq(sqrt(z)) = z
sqrt_times: LEMMA sqrt(x*y) = IF -pi < arg(x)+arg(y) AND arg(x)+arg(y) <= pi
THEN sqrt(x)*sqrt(y)
ELSE -sqrt(x)*sqrt(y) ENDIF
sqrt_neg : LEMMA sqrt(-z) =
IF arg(z) <= 0 THEN i*sqrt(z) ELSE -i*sqrt(z) ENDIF
sqrt_inv : LEMMA sqrt(1/n0z)
= IF arg(n0z) = pi THEN -1/sqrt(n0z) ELSE 1/sqrt(n0z) ENDIF
sqrt_div : LEMMA sqrt(x/n0y)
= IF (arg(n0y) = pi & arg(x) > 0) OR
arg(n0y) = 0 OR
(-pi < arg(x)-arg(n0y) & arg(x)-arg(n0y) <= pi)
THEN sqrt(x) / sqrt(n0y) ELSE -sqrt(x) / sqrt(n0y) ENDIF
END complex_sqrt
¤ Dauer der Verarbeitung: 0.2 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.
|
