bounded_reals [T: TYPEFROM 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
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.
