|
bounded_reals [T: TYPE FROM real]: THEORY
%------------------------------------------------------------------------
% Defines bounds and extrema for sets of reals or its subtypes
%
% Adapted by Rick Butler from the "real_sets" theory that was
% developed by Bruno Dutertre
%
% This theory defines four functions:
%
% sup: returns least upper bound of set with upper bound
% inf: returns greatest lower bound of set with lower bound
% max: returns maximal element of sets containing a maximum
% min: returns minimal element of sets containing a minimum
%
% NOTE. None of these functions are interpreted. Therefore, it is
% necessary to rewrite with the _def theorems or use TYPEPREDs.
% IT is usually easier to rewrite with the _def theoremsL
%
% sup_def : LEMMA sup(Su) = x IFF least_upper_bound(<=)(x, Su)
% inf_def : LEMMA inf(Sl) = x IFF greatest_lower_bound(<=)(x, Sl)
% max_def : LEMMA max(W) = t IFF maximum?(t, W)
% min_def : LEMMA min(X) = t IFF minimum?(t, X)
%
% This version uses revised prelude axioms in order to prevent the
% generation of superfluous "extend"s. These are in prelude_aux.
%
%------------------------------------------------------------------------
BEGIN
IMPORTING reals_complete_more[T]
n,x: VAR real
t: VAR T
E : VAR setof[T]
S: VAR (nonempty?[T])
% ------------- sup ---------------
above_bounded(E): bool = (EXISTS n: upper_bound(<=)(n, E))
sup_set: TYPE = { S | above_bounded(S) }
Su: VAR sup_set
sup_exists: LEMMA (EXISTS x: least_upper_bound(<=)(x, Su))
sup(Su): {x | least_upper_bound(<=)(x, Su)}
sup_def : LEMMA sup(Su) = x IFF least_upper_bound(<=)(x, Su)
in_set(x,S): bool = IF T_pred(x) THEN S(x) ELSE FALSE ENDIF
max_set: TYPE = {Su: sup_set | in_set(sup(Su),Su)}
W: VAR max_set
max(W): T = sup(W)
maximum?(t, S) : bool = S(t) AND upper_bound(<=)(t, S)
max_def : LEMMA max(W) = t IFF maximum?(t, W)
% ------------- inf ---------------
below_bounded(E): bool = (EXISTS n: lower_bound(<=)(n, E))
inf_set: TYPE = { S | below_bounded(S) }
Sl: VAR inf_set
inf_exists: LEMMA (EXISTS x: greatest_lower_bound(<=)(x, Sl))
inf(Sl): {x | greatest_lower_bound(<=)(x, Sl)}
inf_def : LEMMA inf(Sl) = x IFF greatest_lower_bound(<=)(x, Sl)
ext(Sl): set[real] = { x | IF T_pred(x) THEN Sl(x) ELSE FALSE ENDIF}
min_set: TYPE = {Sl: inf_set | ext(Sl)(inf(Sl))}
X: VAR min_set
min(X): T = inf(X)
minimum?(t, S) : bool = S(t) AND lower_bound(<=)(t, S)
min_def : LEMMA min(X) = t IFF minimum?(t, X)
END bounded_reals
¤ Dauer der Verarbeitung: 0.3 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.
|
