Quelle  abstract_min.pvs

abstract_min[T: TYPE, f: [T -> nat], P: pred[T]]: THEORY
BEGIN

   ASSUMING

   T_ne: ASSUMPTION EXISTS (t: T): P(t)

   ENDASSUMING

   IMPORTING min_nat

   TP: TYPE = {t: T | P(t)}


   n: VAR nat

   S,SS: VAR T

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

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

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

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

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

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


   min_def: LEMMA minimal?(min)

   min_in : LEMMA P(min) 

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


END abstract_min