Quelle  abstract_min.pvs

abstract_min[T: TYPE, size: [T -> nat], P: pred[T]]: THEORY
%------------------------------------------------------------------------------
%
%  The need for a function that returns the smallest object that
%  satisfies a particular predicate arises in many contexts.  Thus it is
%  useful to develop an "abstract" min theory that can be instantiated in
%  multiple ways to provide different min functions.  Such a theory must
%  be parameterized by
%
%    -------------------------------------------------------------------------
%    | T: TYPE          | the base type over which min is defined            |
%    | size:[T -> nat]  | the size function by which objects are compared    |
%    | P: pred[T]       | the property that the min 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 min_nat

   n: VAR nat
   S,SS: VAR T

   is_one(n): bool = (EXISTS (S: T): P(S) AND size(S) = n)

   prep0: LEMMA nonempty?({n: nat | is_one(n)})

   min_f: nat = min({n: nat | is_one(n)})

   prep1: LEMMA nonempty?({S: T | size(S) = min_f AND P(S)})

   minimal?(S): bool = P(S) AND 
                       (FORALL (SS: T): P(SS) IMPLIES size(S) <= size(SS))

   min: {S: T | minimal?(S)} 


   min_def: LEMMA minimal?(min)

   min_in : LEMMA P(min) 

   min_is_min: LEMMA P(SS) IMPLIES size(min) <= size(SS) 


END abstract_min