product_upto.pvs

product_upto[N: nat]: THEORY
%------------------------------------------------------------------------------
% The products theory introduces and defines properties of the product
% function that multiples an arbitrary function F: [upto(N) -> int] over a range
% from low to high
%
%  		           high
%		           ----
%  product(low, high, F) = |  |  F(j)
%		           |  |
%		         j = low
%
%  AUTHORS:
%
%    Rick Butler     NASA Langley Research Center           
%    Paul Miner      NASA Langley Research Center           
%
%------------------------------------------------------------------------------
BEGIN

  IMPORTING product[upto[N]]

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


  low, high, n, m: VAR upto[N]
  F: VAR function[upto[N] -> real]


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

  product_first_ge : THEOREM high >= low IMPLIES
                           product(low, high, F) = F(low) * product(low+1, high, F)

  product_last_ge  : THEOREM high >= low IMPLIES 
                          product(low, high, F) = product(low, high-1, F) * F(high)

  product_split_ge : THEOREM low-1 <= m AND m <= high IMPLIES 
                            product(low, high, F) = 
                                     product(low, m, F) * product(m+1, high, F)



% ---- Auto-rewrites


  ing: VAR negint
  product_0_neg: LEMMA product(0,ing,F) = 1
  AUTO_REWRITE+ product_0_neg


END product_upto