Quelle polar.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Polar coordinate complex numbers
%
%     Author: David Lester, Manchester University & NIA
%
%     Version 1.0            5/29/04   Initial version (DRL)
%     Version 1.1            4/10/07   abs_i, arg_i added (DRL)
%
%     Narkawicz              12/2013 +
%------------------------------------------------------------------------------

polar: THEORY

  BEGIN

  IMPORTING arithmetic, reals@sqrt, trig@atan2,
            trig@atan2_props,
            number_fields_sq

  argrng: TYPE+ = {x:real | -pi < x & x <= pi} CONTAINING 0

  z,z1,z2:     VAR complex
  n0x,n0y,n0z: VAR nzcomplex
  nnx:         VAR nnreal
  nx:          VAR negreal
  r,x,y:       VAR real
  j:           VAR int
  theta:       VAR argrng

  nzreal_is_nzcomplex: JUDGEMENT nzreal SUBTYPE_OF nzcomplex

  abs(z):nnreal = sqrt(z*conjugate(z))

  abs_def:       LEMMA abs(z) = sqrt(sq.sq(Re(z))+sq.sq(Im(z)))
  abs_real_rew:  LEMMA abs(r) = real_defs.abs(r)
  abs_imag_rew:  LEMMA abs(r*i) = real_defs.abs(r)

  abs_nzcomplex: LEMMA abs(n0z) > 0
  abs_nz_iff_nz: LEMMA abs(z) > 0 IFF z /= 0
  abs_is_0:      LEMMA abs(z) = 0 IFF z  = 0

  abs_neg:       LEMMA abs(-z)      = abs(z)
  abs_mult:      LEMMA abs(z1*z2)   = abs(z1)*abs(z2)
  abs_inv:       LEMMA abs(1/n0z)   = 1/abs(n0z)
  abs_div:       LEMMA abs(z/n0z)   = abs(z)/abs(n0z)
  abs_triangle:  LEMMA abs(z1+z2)  <= abs(z1) + abs(z2)
  abs_triangle_minus: LEMMA abs(z1-z2)>=abs(z1)-abs(z2)
  abs_abs:       LEMMA abs(abs(z))  = abs(z)
  abs_i:         LEMMA abs(i)       = 1

% Lemmata "abs_is_0", "abs_neg" and "abs_triangle" suffice to demonstrate
% that the complex numbers form a (normed) metric space, with metric
% "d(x,y) = abs(x-y)".

% We define a complex number's principal argument value as "arg", note:
% lower case "a" for a real number.
%
% Observe unpleasant formulation of properties to cope with multiples of 2*pi.

  arg(z):argrng = IF    z = 0     THEN 0
                  ELSIF Im(z) < 0 THEN atan2(Re(z),Im(z)) - 2*pi
                                  ELSE atan2(Re(z),Im(z))        ENDIF

  arg_is_0_nz: LEMMA arg(n0z) =  0    IFF (Re(n0z) >  0 AND Im(n0z) = 0)
  arg_is_0:    LEMMA arg(z)   =  0    IFF (Re(z)   >= 0 AND Im(z)   = 0)
  arg_is_pi2:  LEMMA arg(z)   =  pi/2 IFF (Re(z)   =  0 AND Im(z)   > 0)
  arg_is_pi:   LEMMA arg(z)   =  pi   IFF (Re(z)   <  0 AND Im(z)   = 0)
  arg_is_mpi2: LEMMA arg(z)   = -pi/2 IFF (Re(z)   =  0 AND Im(z)   < 0)

  arg_lt_0:    LEMMA arg(z) < 0 IFF Im(z) < 0
  arg_p_lt_pi: LEMMA (0 < arg(z) AND arg(z) < pi) IFF Im(z) > 0
  arg_gt_0:    LEMMA arg(z) > 0 IFF (Im(z) > 0 OR (Im(z) = 0 AND Re(z) < 0))

  arg_div_abs: LEMMA arg(n0x) = arg(n0x/abs(n0x))
  Re_cos_abs1: LEMMA abs(n0x) = 1 IMPLIES Re(n0x) = cos(arg(n0x))
  Im_sin_abs1: LEMMA abs(n0x) = 1 IMPLIES Im(n0x) = sin(arg(n0x))

  arg_nnreal: LEMMA arg(nnx) = 0
  arg_nreal:  LEMMA arg(nx)  = pi
  arg_i:      LEMMA arg(i)   = pi/2

  arg_neg:  LEMMA arg(-n0x)    = IF 0 < arg(n0x) THEN arg(n0x) - pi
                                                 ELSE arg(n0x) + pi ENDIF
  arg_mult: LEMMA arg(n0x*n0y) = LET r = arg(n0x)+arg(n0y) IN
                                 IF    r >   pi THEN r-2*pi
                                 ELSIF r <= -pi THEN r+2*pi
                                                ELSE r      ENDIF
  arg_inv:  LEMMA arg(1/n0z)   = IF    arg(n0z) = 0  THEN 0
                                 ELSIF arg(n0z) = pi THEN pi
                                                     ELSE -arg(n0z) ENDIF
  arg_div:  LEMMA arg(n0x/n0y) = LET r = arg(n0x)-arg(n0y) IN
                                 IF    r >   pi THEN r-2*pi
                                 ELSIF r <= -pi THEN r+2*pi
                                                ELSE r      ENDIF

  polar(z):[nnreal,argrng]      = (abs(z),arg(z))
  rectangular(z):[real,real]    = (Re(z),Im(z))
  from_polar(r,theta):complex   = r*cos(theta) + r*sin(theta)*i
  from_rectangular(x,y):complex = x + y*i

  arg_from_polar: LEMMA r>0 AND -pi < theta AND theta<=pi IMPLIES
    arg(from_polar(r,theta))=theta

  idempotent_rectangular: LEMMA z   = from_rectangular(rectangular(z))
  idempotent_polar      : LEMMA n0z = from_polar(polar(n0z))

  END polar

quality92%

¤ Dauer der Verarbeitung: 0.13 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.