products/Sources/formale Sprachen/Coq/dev/v8-syntax image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: complex_lnexp.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% Complex logarithm and exponential  functions
%
%     Author: David Lester, Manchester University & NIA
%
%     Version 1.0            5/29/04   Initial version (DRL)
%------------------------------------------------------------------------------

complex_lnexp: THEORY

  BEGIN

  IMPORTING polar, trig@trig_ineq, trig_aux, lnexp@hyperbolic

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

  exp(z): nzcomplex = complex_(exp(Re(z))*cos(Im(z)),
                               exp(Re(z))*sin(Im(z)))

  Re_exp: LEMMA Re(exp(z)) = exp(Re(z))*cos(Im(z))
  Im_exp: LEMMA Im(exp(z)) = exp(Re(z))*sin(Im(z))

  AUTO_REWRITE+ Re_exp
  AUTO_REWRITE+ Im_exp

  exp_i_pi        : LEMMA exp(complex_i*pi) = -1
  exp_plus        : LEMMA exp(x+y)          = exp(x)*exp(y) 
  exp_negate      : LEMMA exp(-x)           = 1/exp(x)
  exp_minus       : LEMMA exp(x-y)          = exp(x)/exp(y) 
  exp_periodicity : LEMMA exp(x+(2*j*pi)*complex_i)   = exp(x)
  abs_exp         : LEMMA abs(exp(z))       = exp(Re(z))
  arg_exp         : LEMMA -pi < Im(z) AND Im(z) <= pi =>
                          arg(exp(z))       = Im(z)

  ln(n0z): complex = complex_(ln(abs(n0z)),arg(n0z))


  Re_ln: LEMMA Re(ln(n0z)) = ln(abs(n0z))
  Im_ln: LEMMA Im(ln(n0z)) = arg(n0z)

  AUTO_REWRITE+ Re_ln
  AUTO_REWRITE+ Im_ln
  AUTO_REWRITE+ abs_exp
  AUTO_REWRITE+ arg_exp

  ln_exp          : LEMMA (2*j-1)*pi < Im(z) AND Im(z) <= (2*j+1)*pi =>
                          ln(exp(z)) = z - (2*j*pi)*complex_i
  exp_ln          : LEMMA exp(ln(n0z)) = n0z
  ln_mult         : LEMMA ln(n0x*n0y)  = ln(n0x) + ln(n0y) -
                          LET r = arg(n0x)+arg(n0y) IN
                          IF    r >   pi THEN 2*pi
                          ELSIF r <= -pi THEN -2*pi
                                         ELSE 0 ENDIF*complex_i
  ln_inv          : LEMMA ln(1/n0x)   = IF arg(n0x) = pi THEN 2*pi
                                        ELSE 0 ENDIF*complex_i - ln(n0x)
  ln_div          : LEMMA ln(n0x/n0y)  = ln(n0x) - ln(n0y) -
                          LET r = arg(n0x)-arg(n0y) IN
                          IF    r >   pi THEN 2*pi
                          ELSIF r <= -pi THEN -2*pi
                                         ELSE 0 ENDIF*complex_i

  sin(z): complex = complex_(sin(Re(z))*cosh(Im(z)),-cos(Re(z))*sinh(Im(z)))
  cos(z): complex = complex_(cos(Re(z))*cosh(Im(z)),-sin(Re(z))*sinh(Im(z)))

  Re_sin: LEMMA Re(sin(z)) =  sin(Re(z))*cosh(Im(z))
  Im_sin: LEMMA Im(sin(z)) = -cos(Re(z))*sinh(Im(z))
  Re_cos: LEMMA Re(cos(z)) =  cos(Re(z))*cosh(Im(z))
  Im_cos: LEMMA Im(cos(z)) = -sin(Re(z))*sinh(Im(z))

  AUTO_REWRITE+ Re_sin
  AUTO_REWRITE+ Im_sin
  AUTO_REWRITE+ Re_cos
  AUTO_REWRITE+ Re_sin

  sinh(z):complex = (exp(z) - exp(-z))/2                                % 4.5.1
  cosh(z):complex = (exp(z) + exp(-z))/2                                % 4.5.2

  Re_sinh: LEMMA Re(sinh(z)) =  sinh(Re(z))*cos(Im(z))
  Im_sinh: LEMMA Im(sinh(z)) =  cosh(Re(z))*sin(Im(z))
  Re_cosh: LEMMA Re(cosh(z)) =  cosh(Re(z))*cos(Im(z))
  Im_cosh: LEMMA Im(cosh(z)) =  sinh(Re(z))*sin(Im(z))

  AUTO_REWRITE+ Re_sinh
  AUTO_REWRITE+ Im_sinh
  AUTO_REWRITE+ Re_cosh
  AUTO_REWRITE+ Im_cosh

  sinh_eq_0: LEMMA sinh(z) = 0 <=> EXISTS j: z = complex_i*(j*pi)
  cosh_eq_0: LEMMA cosh(z) = 0 <=> EXISTS j: z = complex_i*((j+1/2)*pi)

  Sinh?(z):bool = sinh(z) /= 0
  Cosh?(z):bool = cosh(z) /= 0

  sx,sy,sz: VAR (Sinh?)
  cx,cy,cz: VAR (Cosh?)

  tanh(cz):complex = sinh(cz)/cosh(cz)                                  % 4.5.3
  csch(sz):complex = 1/sinh(sz)                                         % 4.5.4
  sech(cz):complex = 1/cosh(cz)                                         % 4.5.5
  coth(sz):complex = cosh(sz)/sinh(sz)                                  % 4.5.6

% Special Values of the Hyperbolic Functions

  c_sinh_0: LEMMA sinh(complex_(0,0)) = 0                              % 4.5.61
  c_cosh_0: LEMMA cosh(complex_(0,0)) = 1                              % 4.5.61
  c_tanh_0: LEMMA tanh(complex_(0,0)) = 0                              % 4.5.61
  c_sech_0: LEMMA sech(complex_(0,0)) = 1                              % 4.5.61

% Relations between Hyperbolic Functions

  c_cosh_sinh_one:   LEMMA sq(cosh(z))  - sq(sinh(z))  = 1             % 4.5.16
  c_tanh_sech_one:   LEMMA sq(tanh(cz)) + sq(sech(cz)) = 1             % 4.5.17
  c_coth_csch_one:   LEMMA sq(coth(sz)) - sq(csch(sz)) = 1             % 4.5.18
  c_cosh_plus_sinh:  LEMMA cosh(z)      + sinh(z)      = exp(z)        % 4.5.19
  c_cosh_minus_sinh: LEMMA cosh(z)      - sinh(z)      = exp(-z)       % 4.5.20

% Negative Angle Formulas

  c_sinh_neg: LEMMA sinh(-z)  = -sinh(z)                               % 4.5.21
  c_cosh_neg: LEMMA cosh(-z)  =  cosh(z)                               % 4.5.22
  c_tanh_neg: LEMMA tanh(-cz) = -tanh(cz)                              % 4.5.23
  c_csch_neg: LEMMA csch(-sz) = -csch(sz)
  c_sech_neg: LEMMA sech(-cz) =  sech(cz)
  c_coth_neg: LEMMA coth(-sz) = -coth(sz)

  AUTO_REWRITE+ c_sinh_neg
  AUTO_REWRITE+ c_cosh_neg
  AUTO_REWRITE+ c_tanh_neg
  AUTO_REWRITE+ c_csch_neg
  AUTO_REWRITE+ c_sech_neg
  AUTO_REWRITE+ c_coth_neg

% Addition Formulas

  c_sinh_sum:  LEMMA sinh(x+y) = sinh(x)*cosh(y) + cosh(x)*sinh(y)     % 4.5.24
  c_sinh_diff: LEMMA sinh(x-y) = sinh(x)*cosh(y) - cosh(x)*sinh(y)
  c_cosh_sum:  LEMMA cosh(x+y) = cosh(x)*cosh(y) + sinh(x)*sinh(y)     % 4.5.25
  c_cosh_diff: LEMMA cosh(x-y) = cosh(x)*cosh(y) - sinh(x)*sinh(y)
%  c_tanh_sum:  LEMMA tanh(cx)*tanh(cy) /= -1 =>                        % 4.5.26
%                     tanh(cx+cy) = (tanh(cx)+tanh(cy))/(1+tanh(cx)*tanh(cy))

%  c_coth_sum:  LEMMA n0x+n0y /= 0 IMPLIES                              % 4.5.27
%                   coth(n0x+n0y)
%                             = (1+coth(n0x)*coth(n0y))/(coth(n0x)+coth(n0y))

% Half-angle Formulas

%  sinh_half:  LEMMA sinh(x/2) = LET y = sqrt((cosh(x)-1)/2) IN         % 4.5.28
%                                IF x >= 0 THEN y ELSE -y ENDIF
%  cosh_half:  LEMMA cosh(x/2) = sqrt((cosh(x)+1)/2)                    % 4.5.29
%  tanh_half1: LEMMA tanh(x/2) = LET y = sqrt((cosh(x)-1)/(cosh(x)+1))  % 4.5.30
%                                IN IF x >= 0 THEN y ELSE -y ENDIF
%  tanh_half2: LEMMA tanh(n0x/2) = (cosh(n0x)-1)/sinh(n0x)              % 4.5.30
%  tanh_half3: LEMMA tanh(x/2) = sinh(x)/(cosh(x)+1)                    % 4.5.30

% Multiple-angle Formulas

  c_sinh2x:     LEMMA sinh(2*x) = 2*sinh(x)*cosh(x)                    % 4.5.31
% sinh2x_B:   LEMMA sinh(2*x) = 2*tanh(x)/(1-sq(tanh(x)))              % 4.5.31
  c_cosh2x:     LEMMA cosh(2*x) = 2*sq(cosh(x))-1                      % 4.5.32
  c_cosh2x_B:   LEMMA cosh(2*x) = 2*sq(sinh(x))+1                      % 4.5.32
  c_cosh2x_C:   LEMMA cosh(2*x) = sq(cosh(x)) + sq(sinh(x))            % 4.5.32
%  tanh2x:     LEMMA tanh(2*x) = 2*tanh(x)/(1+sq(tanh(x)))              % 4.5.33
 % sinh3x:     LEMMA sinh(3*x) = 3*sinh(x) + 4*sinh(x)^3                % 4.5.34
 % cosh3x:     LEMMA cosh(3*x) = 4*cosh(x)^3-3*cosh(x)                  % 4.5.35
  c_sinh4x:     LEMMA sinh(4*x)                                        % 4.5.36
                              = 4*sinh(x)*cosh(x)*(sq(sinh(x)) + sq(cosh(x)))

  complex_sin_def: LEMMA sin(z) = -complex_i * sinh(complex_i*conjugate(z))
  complex_cos_def: LEMMA cos(z) = cosh(complex_i*z)

END complex_lnexp

[ zur Elbe Produktseite wechseln0.16Quellennavigators  Analyse erneut starten  ]