FDL > PVS > Prelude > bounded_real_defs : Theory

PVS-2.4 prelude.pvs

bounded_real_defs : THEORY
BEGIN

x: VAR real

y: VAR real

S: VAR (nonempty?[real])

upper bound?(x, S): bool = FORALL (s:(S) ) : s < = x;

upper bound?(S)(x): bool = upper bound?(x, S);

lower bound?(x, S): bool = FORALL (s:(S) ) : x < = s;

lower bound?(S)(x): bool = lower bound?(x, S);

least upper bound?(x, S): bool = upper bound?(x, S) AND (FORALL y : upper bound?(y, S) IMPLIES (x < = y));

least upper bound?(S)(x): bool = least upper bound?(x, S);

greatest lower bound?(x, S): bool = lower bound?(x, S) AND (FORALL y : lower bound?(y, S) IMPLIES (y < = x));

greatest lower bound?(S)(x): bool = greatest lower bound?(x, S);

real complete: AXIOM FORALL S : (EXISTS y : upper bound?(y, S)) IMPLIES (EXISTS y : least upper bound?(y, S))

real lower complete: LEMMA FORALL S : (EXISTS y : lower bound?(y, S)) IMPLIES (EXISTS x : greatest lower bound?(x, S))

bounded above?(S): bool = EXISTS x : upper bound?(x, S);

bounded below?(S): bool = EXISTS x : lower bound?(x, S);

bounded?(S): bool = bounded above?(S) AND bounded below?(S);

bounded set : TYPE = (bounded?)

SA: VAR (bounded above?)

lub exists: LEMMA EXISTS x : least upper bound?(x, SA)

%%(TCC) lub_TCC1: OBLIGATION

lub(SA): {x | least upper bound?(x, SA)} ;

lub lem: LEMMA (lub(SA) = x) IFF least upper bound?(x, SA)

SB: VAR (bounded below?)

glb exists: LEMMA EXISTS x : greatest lower bound?(x, SB)

%%(TCC) glb_TCC1: OBLIGATION

glb(SB): {x | greatest lower bound?(x, SB)} ;

glb lem: LEMMA (glb(SB) = x) IFF greatest lower bound?(x, SB)

END bounded_real_defs