|
product_below[N: posnat]: THEORY %below(0) is an empty type
%------------------------------------------------------------------------------
% The products theory introduces and defines properties of the product
% function that multiples an arbitrary function F: [below(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[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] -> int]
% --------- 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_below
[ Verzeichnis aufwärts0.2unsichere Verbindung
Übersetzung europäischer Sprachen durch Browser
]
|
