SSL sigma_below.pvs

sigma_below[N: posnat]: THEORY %below(0) is an empty type
%sigma_below[N: nat]: THEORY
%------------------------------------------------------------------------------
% The summations theory provides properties of the sigma 
% function that sums an arbitrary function F: [below[N] -> real] over a range
% from low to high
%
%             high
%           ----
%  sigma(low, high, F) =  \     F(j)
%           /
%           ----
%          j = low
%
%
%------------------------------------------------------------------------------


BEGIN

  IMPORTING sigma[below(N)]

  int_below: TYPE = {i:int | i < N}
  int_below_T_high: JUDGEMENT int_below SUBTYPE_OF T_high
  nat_is_T_low: JUDGEMENT nat SUBTYPE_OF T_low

  low :VAR nat
  high : VAR int_below 
  n, m, i: VAR below[N]
  F: VAR function[below[N] -> real]


%   play1: LEMMA FORALL (x: below[N]): EXISTS (j: below(N)): j <= x;
%   play2: LEMMA FORALL (x: below[N]): EXISTS (j: below(N)): x <= j;
%   AUTO_REWRITE+ play1, play2



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

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

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

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

% ---- Auto-rewrites


  nn: VAR negint
  sigma_0_neg: LEMMA sigma(0,nn,F) = 0
  AUTO_REWRITE+ sigma_0_neg



END sigma_below