Quelle polar.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Polar representation of Complex
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            5/29/04   Initial version (DRL)
%------------------------------------------------------------------------------

polar: THEORY

BEGIN

  IMPORTING complex_types, reals@sqrt, trig@atan2, trig@atan2_props

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

  z,z1,z2:     VAR complex
  n0x,n0y,n0z: VAR nzcomplex
  nzx:         VAR nzreal
  r,x,y:       VAR real
  j:           VAR int
  theta:       VAR argrng

  abs(z):nnreal = sqrt(sq_abs(z))

  abs_def:       LEMMA abs(z) = sqrt(sq(Re(z))+sq(Im(z)))
  abs_def2:      LEMMA abs(z) = sqrt(sq_abs(z))

  abs_nzcomplex: JUDGEMENT abs(n0z) HAS_TYPE posreal
  abs_nz_iff_nz: LEMMA abs(z) > 0 <=> z /= 0
  abs_is_0:      LEMMA abs(z) = 0 <=> 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_abs:       LEMMA abs(abs(z))    = abs(z)
  abs_i:         LEMMA abs(complex_i) = 1
  abs_div2:      LEMMA abs(z/nzx)     = abs(z)/abs(nzx)
  abs_div3:      LEMMA abs(x/n0z)     = abs(x)/abs(n0z)

  AUTO_REWRITE+ abs_neg
  AUTO_REWRITE+ abs_mult
  AUTO_REWRITE+ abs_inv
  AUTO_REWRITE+ abs_div
  AUTO_REWRITE+ abs_abs
  AUTO_REWRITE+ abs_i
  AUTO_REWRITE+ abs_div2
  AUTO_REWRITE+ abs_div3

  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    <=> (Re(n0z) >  0 AND Im(n0z) = 0)
  arg_is_0:    LEMMA arg(z)   =  0    <=> (Re(z)   >= 0 AND Im(z)   = 0)
  arg_is_pi2:  LEMMA arg(z)   =  pi/2 <=> (Re(z)   =  0 AND Im(z)   > 0)
  arg_is_pi:   LEMMA arg(z)   =  pi   <=> (Re(z)   <  0 AND Im(z)   = 0)
  arg_is_mpi2: LEMMA arg(z)   = -pi/2 <=> (Re(z)   =  0 AND Im(z)   < 0)

  arg_lt_0:    LEMMA arg(z) < 0 <=> Im(z) < 0
  arg_p_lt_pi: LEMMA (0 < arg(z) AND arg(z) < pi) <=> Im(z) > 0
  arg_gt_0:    LEMMA arg(z) > 0 <=> (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 => Re(n0x) = cos(arg(n0x))
  Im_sin_abs1: LEMMA abs(n0x) = 1 => Im(n0x) = sin(arg(n0x))
  abs_cos_arg: LEMMA abs(z) * cos(arg(z)) = Re(z)
  abs_sin_arg: LEMMA abs(z) * sin(arg(z)) = Im(z)

  arg_nnreal: LEMMA Im(z) = 0 AND Re(z) >= 0 => arg(z) = 0
  arg_nreal:  LEMMA Im(z) = 0 AND Re(z) <  0 => arg(z) = pi
  arg_i:      LEMMA arg(complex_i) = pi/2

  arg_neg:  LEMMA arg(-n0x)    = IF 0 < arg(n0x) THEN arg(n0x) - pi
                                                 ELSE arg(n0x) + pi ENDIF
  arg_conjugate:
            LEMMA arg(conjugate(z)) = IF arg(z) = 0 OR arg(z) = pi THEN arg(z)
                                              ELSE -arg(z) 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)*complex_i
  from_rectangular(x,y):complex = x + y*complex_i

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

END polar

quality100%

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