|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
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.
|
