sigma[ii,jj: nat]: THEORY %------------------------------------------------------------------------------ % The summations theory introduces and defines properties of the sigma % function that sums an arbitrary function F: [subrange(ii,jj) -> real] over % a range from low to high % % high % ---- % sigma(low, high, F) = \ F(j) % / % ---- % j = low % %------------------------------------------------------------------------------ BEGIN low, high,l,h: VAR subrange(ii,jj) m,n: VAR nat i: VAR subrange(ii,jj) rng: VAR nat x,B: VAR real F, G: VAR function[subrange(ii,jj) -> real] sigma(low, high, F): RECURSIVE real = IF low > high THEN 0 ELSIF high = low THEN F(low) ELSE F(high) + sigma(low, high-1, F) ENDIF MEASURE (LAMBDA low, high, F: high) sigma_sum : THEOREM sigma(low, high, F) + sigma(low, high, G) = sigma(low, high, (LAMBDA i: F(i) + G(i))) sigma_diff : THEOREM low <= m AND m < high IMPLIES sigma(low, high, F) - sigma(low, m, F) = sigma(m + 1, high, F) sigma_diff_neg: THEOREM low <= m AND m < high IMPLIES sigma(low, m, F) - sigma(low, high, F) = - sigma(m + 1, high, F) sigma_split : THEOREM low <= m AND m < high IMPLIES sigma(low, high, F) = sigma(low, m, F) + sigma(m+1, high, F) sigma_first : THEOREM high > low IMPLIES sigma(low, high, F) = F(low) + sigma(low+1, high, F) sigma_eq_arg : THEOREM sigma(low, low, F) = F(low) sigma_const : THEOREM sigma(low, high, (LAMBDA i: x)) = IF high >= low THEN (high-low+1) * x ELSE 0 ENDIF sigma_mult : THEOREM sigma(low, high, (LAMBDA i: x * F(i))) = x * sigma(low, high, F) sigma_bound : THEOREM low <= high AND (FORALL i: i >= low AND i <= high IMPLIES F(i) <= B) IMPLIES sigma(low, high, F) <= B*abs(high-low+1) sigma_abs : THEOREM abs(sigma(low, high, F)) <= sigma(low, high, LAMBDA i: abs(F(i))) restrict(F, low, high): function[subrange(ii,jj) -> real] = (LAMBDA i: IF i < low OR i > high THEN 0 ELSE F(i) ENDIF ) sigma_restrict : THEOREM l <= low AND h >= high IMPLIES sigma(low,high,F) = sigma(low,high,restrict(F,l,h)) sigma_restrict_eq: THEOREM restrict(F,low,high) = restrict(G,low,high) IMPLIES sigma(low,high,F) = sigma(low,high,G) sigma_eq: THEOREM (FORALL (n: subrange(low,high)): F(n) = G(n)) IMPLIES sigma(low,high,F) = sigma(low,high,G) sigma_nonneg : THEOREM (FORALL i: F(i) >= 0) IMPLIES sigma(low, high, F) >= 0 sigma_nonpos : THEOREM (FORALL i: F(i) <= 0) IMPLIES sigma(low, high, F) <= 0 Fnnr: VAR function[subrange(ii,jj) -> nonneg_real] Fnpr: VAR function[subrange(ii,jj) -> nonpos_real] Fnat: VAR function[subrange(ii,jj) -> nat] Fnni: VAR function[subrange(ii,jj) -> nonneg_int] Fnpi: VAR function[subrange(ii,jj) -> nonpos_int] Fn: VAR function[subrange(ii,jj) -> nat] JUDGEMENT sigma(low,high,Fnnr) HAS_TYPE nonneg_real JUDGEMENT sigma(low,high,Fnpr) HAS_TYPE nonpos_real JUDGEMENT sigma(low,high,Fnat) HAS_TYPE nat JUDGEMENT sigma(low,high,Fnni) HAS_TYPE nonneg_int JUDGEMENT sigma(low,high,Fnpi) HAS_TYPE nonpos_int JUDGEMENT sigma(low,high,Fn) HAS_TYPE nat sigma_nonnegfun_eq_0: LEMMA sigma(low,high,Fnnr) = 0 AND low <= i AND i <= high IMPLIES Fnnr(i) = 0 END sigma