|
%------------------------------------------------------------------------------
% Summation
%
% Author: David Lester, Manchester University
%
% Version 1.0 18/2/09 Initial Release Version
%------------------------------------------------------------------------------
sum: THEORY
BEGIN
IMPORTING prelude_aux, prelude_A4, appendix, cauchy, unique, power,
reals@sigma[nat]
x,y: VAR real
xs,ys: VAR [nat-> real]
p,p1,n,m: VAR nat
X,Y,i,j: VAR int
pn: VAR posnat
cxs: VAR [nat->cauchy_real]
cauchys_to_reals (cxs,p): [nat->real] = (LAMBDA (m:nat): (cxs(m))(p)*2^-p)
sum_lemma2: LEMMA
(FORALL (n:nat): cauchy_prop(xs(n),cxs(n))) =>
abs(sigma(0,n,xs) - sigma(0,n,cauchys_to_reals(cxs,p))) < (n+1)*2^-p
cauchy_sum_aux (cxs:[nat->cauchy_real],n,p:nat): RECURSIVE int
= (IF n = 0 THEN cxs(0)(p) ELSE cauchy_sum_aux(cxs,n-1,p) + cxs(n)(p) ENDIF)
MEASURE (LAMBDA cxs,n,p: n)
sum_lemma3: LEMMA cauchy_sum_aux(cxs,n,p)*2^-p
= sigma(0,n,cauchys_to_reals(cxs,p))
cauchy_sum_type_int (cxs:[nat->cauchy_real],n,p:nat): int
= round(cauchy_sum_aux(cxs,n,p+floor_log2(n+1)+2)/2^(floor_log2(n+1)+2))
sum_lemma4: LEMMA
abs(sigma(0,n,cauchys_to_reals(cxs,p+floor(log2(n+1))+2))
- cauchy_sum_type_int(cxs,n,p)*2^-p) <= 2^-(p+1)
sum_lemma5: LEMMA (FORALL (n:nat): cauchy_prop(xs(n),cxs(n))) =>
abs(sigma(0,n,xs) - cauchy_sum_type_int(cxs,n,p)*2^-p) < 2^-p
cauchys_prop(xs:[nat -> real], cs:[nat -> cauchy_real]): bool
= (FORALL (n:nat): cauchy_prop(xs(n), cs(n)))
cauchys_real? (cs:[nat->cauchy_real]):bool
= EXISTS (xs:[nat -> real]): cauchys_prop(xs,cs)
cauchys_real: NONEMPTY_TYPE = (cauchys_real?)
CONTAINING (LAMBDA n: LAMBDA p:0)
cauchy_sum (cxs:cauchys_real,n): cauchy_real
= (LAMBDA p: cauchy_sum_type_int(cxs,n,p))
sum_lemma: LEMMA (FORALL (n:nat): cauchy_prop(xs(n),cxs(n))) =>
cauchy_prop(sigma(0,m,xs), cauchy_sum(cxs,m))
END sum
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.19Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
