Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Forschung weltweit Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/complex_alt/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 4 kB

Quellcode-Bibliothek 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%

¤ 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.0.1Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.