abstract_max[T: TYPE, N: nat, size: [T -> upto[N]], P: pred[T]]: THEORY
%------------------------------------------------------------------------------
%
% The need for a function that returns the largest object that
% satisfies a particular predicate arises in many contexts. Thus it is
% useful to develop an "abstract" max theory that can be instantiated in
% multiple ways to provide different max functions. Such a theory must
% be parameterized by
%
% -------------------------------------------------------------------------
% | T: TYPE | the base type over which max is defined |
% | size:[T -> nat] | the size function by which objects are compared |
% | P: pred[T] | the property that the max function must satisfy |
% -------------------------------------------------------------------------
%
% Author:
%
% Ricky W. Butler NASA Langley
%
% Version 2.0 Last modified 10/21/97
%
% Maintained by:
%
% Rick Butler NASA Langley Research Center
% [email protected]
%
%------------------------------------------------------------------------------
BEGIN
ASSUMING
T_ne: ASSUMPTION EXISTS (t: T): P(t)
ENDASSUMING
IMPORTING max_upto
TP: TYPE = {t: T | P(t)}
n: VAR upto[N]
S,SS: VAR T
is_one(n): bool = (EXISTS (S: T): P(S) AND size(S) = n)
prep0: LEMMA nonempty?({n: upto[N] | is_one(n)})
max_f: upto[N] = max({n: upto[N] | is_one(n)})
prep1: LEMMA nonempty?({S: T | size(S) = max_f AND P(S)})
maximal?(S): bool = P(S) AND
(FORALL (SS: T): P(SS) IMPLIES size(S) >= size(SS))
max: {S: T | maximal?(S)}
max_def: LEMMA maximal?(max)
max_in : LEMMA P(max)
max_is_max: LEMMA P(SS) IMPLIES size(max) >= size(SS)
END abstract_max
¤ Dauer der Verarbeitung: 0.21 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.
|
