FDL > PVS > Prelude > real_types : Theory

PVS-2.4 prelude.pvs

 reals_types declares some useful subtypes of the reals and some
 associated judgements.

real_types : THEORY
BEGIN

x: VAR real

nonneg real : NONEMPTY_TYPE = {(x:real) | x > = 0} CONTAINING 0

nonpos real : NONEMPTY_TYPE = {(x:real) | x < = 0} CONTAINING 0

posreal : NONEMPTY_TYPE = {(x:nonneg real) | x > 0} CONTAINING 1

negreal : NONEMPTY_TYPE = {(x:nonpos real) | x < 0} CONTAINING -1

nnreal : TYPE = nonneg real

npreal : TYPE = nonpos real

%%(TCC) posreal_is_nzreal: OBLIGATION

posreal is nzreal: JUDGEMENT posreal SUBTYPE_OF nzreal

%%(TCC) negreal_is_nzreal: OBLIGATION

negreal is nzreal: JUDGEMENT negreal SUBTYPE_OF nzreal

nzx: VAR nzreal

nzy: VAR nzreal

px: VAR posreal

py: VAR posreal

nx: VAR negreal

ny: VAR negreal

nnx: VAR nonneg real

nny: VAR nonneg real

npx: VAR nonpos real

npy: VAR nonpos real

nonneg real add closed: LEMMA (nnx + nny) > = 0

nonpos real add closed: LEMMA (npx + npy) < = 0

negreal add closed: LEMMA (nx + ny) < 0

nonneg real mult closed: LEMMA (nnx * nny) > = 0

%%(TCC) nzreal_times_nzreal_is_nzreal: OBLIGATION

nzreal times nzreal is nzreal: JUDGEMENT *(nzx, nzy) HAS_TYPE nzreal

%%(TCC) nzreal_div_nzreal_is_nzreal: OBLIGATION

nzreal div nzreal is nzreal: JUDGEMENT /(nzx, nzy) HAS_TYPE nzreal

%%(TCC) minus_nzreal_is_nzreal: OBLIGATION

minus nzreal is nzreal: JUDGEMENT -(nzx) HAS_TYPE nzreal

%%(TCC) nnreal_plus_nnreal_is_nnreal: OBLIGATION

nnreal plus nnreal is nnreal: JUDGEMENT +(nnx, nny) HAS_TYPE nnreal

%%(TCC) nnreal_times_nnreal_is_nnreal: OBLIGATION

nnreal times nnreal is nnreal: JUDGEMENT *(nnx, nny) HAS_TYPE nnreal

%%(TCC) nnreal_div_posreal_is_nnreal: OBLIGATION

nnreal div posreal is nnreal: JUDGEMENT /(nnx, py) HAS_TYPE nnreal

%%(TCC) nnreal_div_negreal_is_npreal: OBLIGATION

nnreal div negreal is npreal: JUDGEMENT /(nnx, ny) HAS_TYPE npreal

%%(TCC) npreal_plus_npreal_is_npreal: OBLIGATION

npreal plus npreal is npreal: JUDGEMENT +(npx, npy) HAS_TYPE npreal

%%(TCC) npreal_times_npreal_is_nnreal: OBLIGATION

npreal times npreal is nnreal: JUDGEMENT *(npx, npy) HAS_TYPE nnreal

%%(TCC) npreal_div_posreal_is_npreal: OBLIGATION

npreal div posreal is npreal: JUDGEMENT /(npx, py) HAS_TYPE npreal

%%(TCC) npreal_div_negreal_is_nnreal: OBLIGATION

npreal div negreal is nnreal: JUDGEMENT /(npx, ny) HAS_TYPE nnreal

%%(TCC) posreal_plus_nnreal_is_posreal: OBLIGATION

posreal plus nnreal is posreal: JUDGEMENT +(px, nny) HAS_TYPE posreal

%%(TCC) nnreal_plus_posreal_is_posreal: OBLIGATION

nnreal plus posreal is posreal: JUDGEMENT +(nnx, py) HAS_TYPE posreal

%%(TCC) posreal_times_posreal_is_posreal: OBLIGATION

posreal times posreal is posreal: JUDGEMENT *(px, py) HAS_TYPE posreal

%%(TCC) posreal_div_posreal_is_posreal: OBLIGATION

posreal div posreal is posreal: JUDGEMENT /(px, py) HAS_TYPE posreal

%%(TCC) negreal_plus_negreal_is_negreal: OBLIGATION

negreal plus negreal is negreal: JUDGEMENT +(nx, ny) HAS_TYPE negreal

%%(TCC) negreal_times_negreal_is_posreal: OBLIGATION

negreal times negreal is posreal: JUDGEMENT *(nx, ny) HAS_TYPE posreal

%%(TCC) negreal_div_negreal_is_posreal: OBLIGATION

negreal div negreal is posreal: JUDGEMENT /(nx, ny) HAS_TYPE posreal

END real_types