sigma_nat: THEORY %------------------------------------------------------------------------------ % The summations theory provides 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 % % % NOTE. Older versions of the library used a slightly more general % version of "sigma_first", namely for high >= low rather % than just high > low. The lemma "sigma_first_ge" has been % added here to facilitate the upgrade to the new library. % %------------------------------------------------------------------------------ BEGIN IMPORTING sigma[nat] low, high, n, m: VAR nat F: VAR function[nat -> real] % --------- Following Theorems Not Provable In Generic Framework ------- sigma_shift: THEOREM sigma(low+m,high+m,F) = sigma(low,high, (LAMBDA (n: nat): F(n+m))) sigma_shift_neg: THEOREM low - m >= 0 and low <= high IMPLIES sigma(low-m,high-m,F) = sigma(low,high, (LAMBDA n: IF n-m < 0 THEN 0 ELSE F(n-m) ENDIF)) sigma_shift_ng2: THEOREM low - m >= 0 and low <= high IMPLIES sigma(low-m,high-m,F) = sigma(low,high, (LAMBDA n: F(n~m))) sigma_first_ge : THEOREM high >= low IMPLIES % for upward compatibility sigma(low, high, F) = F(low) + sigma(low+1, high, F) END sigma_nat