sigma_posnat: THEORY
%------------------------------------------------------------------------------
% The summations theory introduces and defines properties of the sigma 
% function that sums an arbitrary function F: [T -> real] over a range
% from low to high
%
%             high
%           ----
%  sigma(low, high, F) =  \     F(j)
%           /
%           ----
%          j = low
%
%------------------------------------------------------------------------------


BEGIN

  IMPORTING sigma[posnat]

  int_is_T_high: JUDGEMENT int SUBTYPE_OF T_high
  posnat_is_T_low : JUDGEMENT posnat SUBTYPE_OF T_low

  low, n, m: VAR posnat
  high: VAR int
  F: VAR function[posnat -> real]


% --------- Following Theorems Not Provable In Generic Framework -------

  sigma_shift:  THEOREM sigma(low+m,high+m,F) = 
                              sigma(low,high, (LAMBDA (n: posnat): F(n+m)))

  sigma_shift_neg:  THEOREM low - m > 0 IMPLIES 
                         sigma(low-m,high-m,F) = 
                             sigma(low,high, (LAMBDA n: IF n-m <= 0 THEN 0 
                                                        ELSE F(n-m) 
                                                        ENDIF))

  sigma_split_ge : THEOREM low-1 <= m AND m <= high IMPLIES 
                            sigma(low, high, F) = 
                                     sigma(low, m, F) + sigma(m+1, high, F)


END sigma_posnat