Quellcode-Bibliothek complex_sets.pvs

%------------------------------------------------------------------------------
% Set-valued complex functions
%
%     Author: David Lester, Manchester University & NIA
%
%     Version 1.0            4/12/07   Initial version (DRL)
%------------------------------------------------------------------------------

complex_sets: THEORY

BEGIN

  IMPORTING exp

  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

% Considerable notational and practical convenience can be obtained by using
% instead "Arg" to represent the set of all possible argument values.

% To bring elegance into this theory we define addition and unary and
% binary minus.
;
  -: MACRO [nonempty_set[real]->nonempty_set[real]]
      = (LAMBDA (X:nonempty_set[real]): {x | X(-x)});
  +: MACRO [nonempty_set[real],nonempty_set[real]->nonempty_set[real]]
      = (LAMBDA (X,Y:nonempty_set[real]): {z:real | EXISTS (x:(X),y:(Y)): z = x+y});
  -: MACRO [nonempty_set[real],nonempty_set[real]->nonempty_set[real]]
      = (LAMBDA (X,Y:nonempty_set[real]): {z:real | EXISTS (x:(X),y:(Y)): z = x-y});

  Arg(n0z): nonempty_set[real] = {x:real | EXISTS j: x = arg(n0z) + 2*j*pi}

  Arg_def:  LEMMA Arg(n0z) = {x:real | abs(n0z)*exp(x*i) = n0z}
  Arg_mult: LEMMA Arg(n0x*n0y) =  Arg(n0x) + Arg(n0y)
  Arg_inv:  LEMMA Arg(1/n0z)   = -Arg(n0z)
  Arg_div:  LEMMA Arg(n0x/n0y) =  Arg(n0x) - Arg(n0y)

END complex_sets