Quelle complex_fun_ops.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Arithmetic Operations defined on functions [T->complex]
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            14/06/09  Initial Version
%     Version 1.1            16/03/11  Additional rewrites added (DRL)
%
%------------------------------------------------------------------------------
complex_fun_ops[T:TYPE]: THEORY

BEGIN

  IMPORTING polar,
            structures@const_fun_def[T,complex]

  f,f1,f2: VAR [T->complex]
  f3,n0f:  VAR [T->nzcomplex]
  x,y:     VAR T
  a:       VAR complex
  n0a:     VAR nzcomplex
  c:       VAR real

  Re(f): [T -> real] = lambda x: Re(f(x));
  Im(f): [T -> real] = lambda x: Im(f(x));

  Re_fun_rew: LEMMA Re(f)(x) = Re(f(x))
  Im_fun_rew: LEMMA Im(f)(x) = Im(f(x))

  AUTO_REWRITE+ Re_fun_rew
  AUTO_REWRITE+ Im_fun_rew

  +(f1, f2) : [T -> complex] = lambda x : f1(x) + f2(x);
  -(f1)     : [T -> complex] = lambda x : -f1(x);
  *(f1, f2) : [T -> complex] = lambda x : f1(x) * f2(x);
  *(a, f1)  : [T -> complex] = lambda x : a * f1(x);
  *(c, f1)  : [T -> complex] = lambda x : c * f1(x);
  -(f1, f2) : [T -> complex] = lambda x : f1(x) - f2(x);
  /(f1, f3) : [T -> complex] = lambda x : f1(x) / f3(x);
  /(f, n0a) : [T -> complex] = lambda x : f(x) / n0a;
  /(a, f3)  : [T -> complex] = lambda x : a / f3(x);
  /(c, f3)  : [T -> complex] = lambda x : c / f3(x);
  inv(f3)   : [T -> complex] = 1 / f3;
  sq(f)     : [T -> complex] = lambda x: sq(f(x));

  diff_function    : LEMMA f1 - f2 = f1 + (- f2)
  div_function     : LEMMA f1 / f3 = f1 * (1 /f3)
  scal_function    : LEMMA a * f1 = const_fun(a) * f1
  scaldiv_function : LEMMA a / f3 = const_fun(a) / f3
  negneg_function  : LEMMA - (- f1) = f1
  prod_def         : LEMMA *(f1,f2)   = (1/4)*(sq(f1+f2)-sq(f1-f2))

  conjugate(f): [T -> complex] = lambda x: conjugate(f(x));

  IMPORTING reals@real_fun_ops_aux[T]

  Re_fun_conjugate: LEMMA Re(conjugate(f)) = Re(f)
  Im_fun_conjugate: LEMMA Im(conjugate(f)) = -Im(f)

  AUTO_REWRITE+ Re_fun_conjugate
  AUTO_REWRITE+ Im_fun_conjugate

  sq_abs(f): [T -> nnreal]     = sq(Re(f)) + sq(Im(f))
  nz_fun_sq_abs_pos:  JUDGEMENT sq_abs(n0f) HAS_TYPE [T->posreal]

;
  abs(f1)   : [T->nonneg_real] = lambda x : abs(f1(x));
  complex_abs_nzfunction_pos: JUDGEMENT abs(n0f) HAS_TYPE [T->posreal]

  complex_abs_neg: LEMMA abs(-f) = abs(f)
  complex_abs_mul: LEMMA abs(f1*f2) = abs(f1)*abs(f2)

  Re_fun_add1: LEMMA Re(f1+f2) = Re(f1)+Re(f2)

  Re_fun_neg1: LEMMA Re(-f)    = -Re(f)

  Re_fun_sub1: LEMMA Re(f1-f2) = Re(f1)-Re(f2)

  Re_fun_mul1: LEMMA Re(f1*f2) = Re(f1)*Re(f2) - Im(f1)*Im(f2)
  Re_fun_mul2: LEMMA Re(a*f)   = Re(a)*Re(f) - Im(a)*Im(f)

  Re_fun_div1: LEMMA Re(f/n0f) = (Re(f)*Re(n0f) + Im(f)*Im(n0f))/sq_abs(n0f)
  Re_fun_div2: LEMMA Re(a/n0f) = (Re(a)*Re(n0f) + Im(a)*Im(n0f))/sq_abs(n0f)
  Re_fun_div3: LEMMA Re(f/n0a) = (Re(n0a)/sq_abs(n0a))*Re(f) +
                                 (Im(n0a)/sq_abs(n0a))*Im(f)

  Im_fun_add1: LEMMA Im(f1+f2) = Im(f1)+Im(f2)

  Im_fun_neg1: LEMMA Im(-f)    = -Im(f)

  Im_fun_sub1: LEMMA Im(f1-f2) = Im(f1)-Im(f2)

  Im_fun_mul1: LEMMA Im(f1*f2) = Im(f1)*Re(f2) + Re(f1)*Im(f2)
  Im_fun_mul2: LEMMA Im(a*f)   = Im(a)*Re(f) + Re(a)*Im(f)

  Im_fun_div1: LEMMA Im(f/n0f) = (Im(f)*Re(n0f) - Re(f)*Im(n0f))/sq_abs(n0f)
  Im_fun_div2: LEMMA Im(a/n0f) = (Im(a)*Re(n0f) - Re(a)*Im(n0f))/sq_abs(n0f)
  Im_fun_div3: LEMMA Im(f/n0a) = (Re(n0a)/sq_abs(n0a))*Im(f) -
                                 (Im(n0a)/sq_abs(n0a))*Re(f)

  AUTO_REWRITE+ complex_abs_neg
  AUTO_REWRITE+ complex_abs_mul
  AUTO_REWRITE+ Re_fun_add1
  AUTO_REWRITE+ Re_fun_neg1
  AUTO_REWRITE+ Re_fun_sub1
  AUTO_REWRITE+ Re_fun_mul1
  AUTO_REWRITE+ Re_fun_mul2
  AUTO_REWRITE+ Re_fun_div1
  AUTO_REWRITE+ Re_fun_div2
  AUTO_REWRITE+ Re_fun_div3
  AUTO_REWRITE+ Im_fun_add1
  AUTO_REWRITE+ Im_fun_neg1
  AUTO_REWRITE+ Im_fun_sub1
  AUTO_REWRITE+ Im_fun_mul1
  AUTO_REWRITE+ Im_fun_mul2
  AUTO_REWRITE+ Im_fun_div1
  AUTO_REWRITE+ Im_fun_div2
  AUTO_REWRITE+ Im_fun_div3
;
  =(f1,f2): bool = Re(f1) = Re(f2) AND Im(f1) = Im(f2);
  /=(f1,f2):bool = NOT (f1 = f2);

  c_fun_eq1: LEMMA f1  = f2 <=> Re(f1) = Re(f2) AND Im(f1) = Im(f2)
  c_fun_ne1: LEMMA f1 /= f2 <=> NOT (f1 = f2)

  AUTO_REWRITE+ c_fun_eq1
  AUTO_REWRITE+ c_fun_ne1

END complex_fun_ops

quality96%

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