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 % R.W.Butler@larc.nasa.gov % %------------------------------------------------------------------------------ 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