SSL sum.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% 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