|
%------------------------------------------------------------------------------
% Arithmetic Operations defined on functions [T->real]
%
% Author: David Lester, Manchester University
%
% Version 1.0 14/06/09 Initial Version
%------------------------------------------------------------------------------
real_fun_ops_aux[T:TYPE]: THEORY
BEGIN
IMPORTING real_fun_ops, sq
f,f1,f2: VAR [T->real]
f3: VAR [T -> nzreal]
F: VAR sequence[[T->real]]
x,y: VAR T
nnc: VAR nnreal
npc: VAR npreal
a,c: VAR real
n,i: VAR nat
sq(f): [T->nnreal] = lambda x: sq(f(x))
min(f1,f2):[T->real] = lambda x: min(f1(x),f2(x))
max(f1,f2):[T->real] = lambda x: max(f1(x),f2(x))
minus(f): [T->nnreal] = lambda x: -min(f(x),0)
plus(f): [T->nnreal] = lambda x: max(f(x),0)
maximum(F,n): RECURSIVE [T->real]
= IF n = 0 THEN F(0) ELSE max(F(n),maximum(F,n-1)) ENDIF MEASURE n
minimum(F,n): RECURSIVE [T->real]
= IF n = 0 THEN F(0) ELSE min(F(n),minimum(F,n-1)) ENDIF MEASURE n
plus_minus_def: LEMMA f = plus(f) - minus(f)
max_plus_min: LEMMA max(f1,f2)+min(f1,f2) = f1+f2
max_minus_min: LEMMA max(f1,f2)-min(f1,f2) = abs(f1-f2)
max_def: LEMMA max(f1,f2) = (1/2)*(f1+f2+abs(f1-f2))
min_def: LEMMA min(f1,f2) = (1/2)*(f1+f2-abs(f1-f2))
prod_def: LEMMA *(f1,f2) = (1/4)*(sq(f1+f2)-sq(f1-f2))
plus_plus: LEMMA plus(plus(f)) = plus(f)
plus_minus: LEMMA plus(minus(f)) = minus(f)
minus_plus: LEMMA minus(plus(f)) = const_fun(0)
minus_minus: LEMMA minus(minus(f)) = const_fun(0)
plus_scal: LEMMA plus(c*f) = IF c>=0 THEN c*plus(f) ELSE -c*minus(f) ENDIF
minus_scal: LEMMA minus(c*f) = IF c>=0 THEN c*minus(f) ELSE -c*plus(f) ENDIF
maximum_def1: LEMMA i <= n => FORALL x: F(i)(x) <= maximum(F,n)(x)
maximum_def2: LEMMA EXISTS i: i <= n AND maximum(F,n)(x) = F(i)(x)
minimum_def1: LEMMA i <= n => FORALL x: minimum(F,n)(x) <= F(i)(x)
minimum_def2: LEMMA EXISTS i: i <= n AND minimum(F,n)(x) = F(i)(x)
END real_fun_ops_aux
¤ Dauer der Verarbeitung: 0.16 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.
|
