SSL sigma_int.pvs

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


BEGIN

  IMPORTING sigma[int]

  int_is_T_high: JUDGEMENT int SUBTYPE_OF T_high
  int_is_T_low : JUDGEMENT int SUBTYPE_OF T_low

  low, high, i, j, m: VAR int
  F: VAR function[int -> real]


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

  sigma_shift    :  THEOREM sigma(low+j,high+j,F) = 
                              sigma(low,high, (LAMBDA (i: int): F(i+j)))


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


  sigma_first_ge : THEOREM high >= low IMPLIES
                           sigma(low, high, F) = F(low) + sigma(low+1, high, F)

  sigma_mid_ge  : THEOREM high >= i AND i >= low IMPLIES 
                          sigma(low, high, F) = sigma(low, i-1, F) + F(i) +
                                                sigma(i+1, high, F) 

  sigma_last_ge  : THEOREM high >= low IMPLIES 
                          sigma(low, high, F) = sigma(low, high-1, F) + F(high)


END sigma_int