| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/graphs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle abstract_min.pvs Sprache: 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 ¤ Dauer der Verarbeitung: 0.28 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28