sum_hack  % [ parameters ]
  : THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Some stuff that will eventually be loaded from a library,
%  once the PVS library mechanism works.
  i,j,k:var nat
  F: var [nat->real]

  Sum(j,F):recursive real =
   if j=0 then 0 else F(j-1)+Sum(j-1,F) endif
   measure j

  F1,F2: var [nat->nonneg_real]

  Sum_nonneg: lemma  Sum(j,F1)>=0

%%%%%%% Modif S. Boldo
%  JUDGEMENT Sum HAS_TYPE [nat,[nat->nonneg_real]->nonneg_real]
%%%%%%% Fin modif  

  Sum_zero: lemma Sum(j,F1)=0 iff forall (i:below(j)): F1(i)=0

  Sum_pos: lemma  Sum(j,F1)>0 iff (exists (i:below(j)): F1(i)>0)

  Sum_le:  lemma (forall (i:below(j)): F1(i) <= F2(i)) => Sum(j,F1)<=Sum(j,F2)

  Sum_ge1: lemma (exists (i:below(j)): F1(i)>=1) => Sum(j,F1)>=1

  pz: var posreal

  Sum_ge: lemma (exists (i:below(j)): F1(i)>= pz) => Sum(j,F1)>=pz

  Sum_split: lemma forall (i:upto(j)):
    Sum(j,F) = Sum(i,F) + Sum(j-i,lambda k: F(k+i)) 

  END sum_hack