Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bounded_reals.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.