|
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
¤ Dauer der Verarbeitung: 0.24 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
