| feedback |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: PVSOriginal von: PVS© |
|
|
%------------------------------------------------------------------------------
% 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) ¤ |
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchenDie farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
