|
real_fun_ops [ T : TYPE ] : THEORY
%------------------------------------------%
% Operations on functions : [ T -> real] %
%------------------------------------------%
BEGIN
f, f1, f2 : VAR [T -> real]
f3 : VAR [T -> nzreal]
a : VAR real
x, y : VAR T
const_fun(a) : [T -> real] = LAMBDA x : a ;
+(f1, f2) : [T -> real] = LAMBDA x : f1(x) + f2(x);
-(f1) : [T -> real] = LAMBDA x : -f1(x);
*(f1, f2) : [T -> real] = LAMBDA x : f1(x) * f2(x);
*(a, f1) : [T -> real] = LAMBDA x : a * f1(x);
-(f1, f2) : [T -> real] = LAMBDA x : f1(x) - f2(x);
/(f1, f3) : [T -> real] = LAMBDA x : f1(x) / f3(x);
/(a, f3) : [T -> real] = LAMBDA x : a / f3(x);
inv(f3) : [T -> real] = 1 / f3;
abs(f1) : [T -> nonneg_real] = LAMBDA x : abs(f1(x));
n: VAR nat
^(f,n) : [T -> real] = (LAMBDA (t:T): f(t)^n)
%------------------
% Rewrite rules
%------------------
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
END real_fun_ops
¤ Dauer der Verarbeitung: 0.14 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.
|
