%------------------------------------------------------------------------------
% 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