SSL bounded_reals.pvs Sprache: PVS

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

quality100%

¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.