|
product_nat: THEORY
%------------------------------------------------------------------------------
% The products theory introduces and defines properties of the product
% function that multiples an arbitrary function F: [nat -> 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[nat]
int_is_T_high: JUDGEMENT int SUBTYPE_OF T_high
nat_is_T_low : JUDGEMENT nat SUBTYPE_OF T_low
high, i: VAR int
low, n, m: VAR nat
F: VAR function[nat -> int]
% --------- Following Theorems Not Provable In Generic Framework -------
product_shift: THEOREM product(low+m,high+m,F) =
product(low,high, (LAMBDA (n: nat): F(n+m)))
product_shift_neg: THEOREM low - m >= 0 IMPLIES
product(low-m,high-m,F) =
product(low,high, (LAMBDA n: IF n-m < 0 THEN 0
ELSE F(n-m)
ENDIF))
product_shift_ng2: THEOREM low - m >= 0 IMPLIES
product(low-m,high-m,F) =
product(low,high, (LAMBDA n: F(n~m)))
product_shift_i: THEOREM 0 <= low + i IMPLIES
product(low+i,high+i,F) =
product(low,high, (LAMBDA (n: nat): IF n < low THEN 0
ELSE F(n+i) ENDIF))
% These next two are now trivial instatiations of the updated framework.
product_first_ge : THEOREM high >= low IMPLIES % slightly more general
product(low, high, F) = F(low) * product(low+1, high, F)
product_split_ge : THEOREM low-1 <= i AND i <= high IMPLIES
product(low, high, F) =
product(low, i, F) * product(i+1, high, F)
% ---- Auto-rewrites
ing: VAR negint
product_0_neg: LEMMA product(0,ing,F) = 1
AUTO_REWRITE+ product_0_neg
END product_nat
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
