FDL > PVS > Prelude > rationals : Theory

PVS-2.4 prelude.pvs

 rationals defines the rational numbers as an uninterpreted subtype of real.
 The basic number operations are redeclared in order to specify that
 they are closed, e.g. the sum of two rationals is a rational.

rationals : THEORY
BEGIN

rational : NONEMPTY_TYPE FROM real

%%
rational_pred: [real- > boolean] ;

%%
rational_nonempty: AXIOM

rat : NONEMPTY_TYPE = rational

rational?((n:number)): bool = real pred(n) AND rational pred(n);

%%(TCC) nonzero_rational_TCC1: OBLIGATION

nonzero rational : NONEMPTY_TYPE = {(r:rational) | r /= 0} CONTAINING 1

nzrat : NONEMPTY_TYPE = nonzero rational

nzrat is nzreal: JUDGEMENT nonzero rational SUBTYPE_OF nonzero real

x: VAR rat

y: VAR rat

n0z: VAR nzrat

closed plus: AXIOM rational pred(x + y)

closed minus: AXIOM rational pred(x - y)

closed times: AXIOM rational pred(x * y)

closed divides: AXIOM rational pred(x / n0z)

closed neg: AXIOM rational pred(-x)

%%(TCC) rat_plus_rat_is_rat: OBLIGATION

rat plus rat is rat: JUDGEMENT +(x, y) HAS_TYPE rat

%%(TCC) rat_minus_rat_is_rat: OBLIGATION

rat minus rat is rat: JUDGEMENT -(x, y) HAS_TYPE rat

%%(TCC) rat_times_rat_is_rat: OBLIGATION

rat times rat is rat: JUDGEMENT *(x, y) HAS_TYPE rat

%%(TCC) rat_div_nzrat_is_rat: OBLIGATION

rat div nzrat is rat: JUDGEMENT /(x, n0z) HAS_TYPE rat

%%(TCC) minus_rat_is_rat: OBLIGATION

minus rat is rat: JUDGEMENT -(x) HAS_TYPE rat

nonneg rat : NONEMPTY_TYPE = {(r:rational) | r > = 0} CONTAINING 0

nonpos rat : NONEMPTY_TYPE = {(r:rational) | r < = 0} CONTAINING 0

posrat : NONEMPTY_TYPE = {(r:nonneg rat) | r > 0} CONTAINING 1

negrat : NONEMPTY_TYPE = {(r:nonpos rat) | r < 0} CONTAINING -1

nnrat : NONEMPTY_TYPE = nonneg rat

nprat : NONEMPTY_TYPE = nonpos rat

nnx: VAR nonneg rat

nny: VAR nonneg rat

npx: VAR nonpos rat

npy: VAR nonpos rat

px: VAR posrat

py: VAR posrat

nx: VAR negrat

ny: VAR negrat

n0x: VAR nzrat

n0y: VAR nzrat

nnrat is nnreal: JUDGEMENT nonneg rat SUBTYPE_OF nonneg real

nprat is npreal: JUDGEMENT nonpos rat SUBTYPE_OF nonpos real

posrat is posreal: JUDGEMENT posrat SUBTYPE_OF posreal

negrat is negreal: JUDGEMENT negrat SUBTYPE_OF negreal

%%(TCC) posrat_is_nzrat: OBLIGATION

posrat is nzrat: JUDGEMENT posrat SUBTYPE_OF nzrat

%%(TCC) negrat_is_nzrat: OBLIGATION

negrat is nzrat: JUDGEMENT negrat SUBTYPE_OF nzrat

%%(TCC) nzrat_times_nzrat_is_nzrat: OBLIGATION

nzrat times nzrat is nzrat: JUDGEMENT *(n0x, n0y) HAS_TYPE nzrat

%%(TCC) nzrat_div_nzrat_is_nzrat: OBLIGATION

nzrat div nzrat is nzrat: JUDGEMENT /(n0x, n0y) HAS_TYPE nzrat

%%(TCC) minus_nzrat_is_nzrat: OBLIGATION

minus nzrat is nzrat: JUDGEMENT -(n0x) HAS_TYPE nzrat

%%(TCC) nnrat_plus_nnrat_is_nnrat: OBLIGATION

nnrat plus nnrat is nnrat: JUDGEMENT +(nnx, nny) HAS_TYPE nonneg rat

%%(TCC) nnrat_times_nnrat_is_nnrat: OBLIGATION

nnrat times nnrat is nnrat: JUDGEMENT *(nnx, nny) HAS_TYPE nonneg rat

%%(TCC) nnrat_div_posrat_is_nnrat: OBLIGATION

nnrat div posrat is nnrat: JUDGEMENT /(nnx, py) HAS_TYPE nonneg rat

%%(TCC) nnrrat_div_negrat_is_nprat: OBLIGATION

nnrrat div negrat is nprat: JUDGEMENT /(nnx, ny) HAS_TYPE nprat

%%(TCC) nprat_plus_nprat_is_nprat: OBLIGATION

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

%%(TCC) nprat_times_nprat_is_nnrat: OBLIGATION

nprat times nprat is nnrat: JUDGEMENT *(npx, npy) HAS_TYPE nnrat

%%(TCC) nprat_div_posrat_is_nprat: OBLIGATION

nprat div posrat is nprat: JUDGEMENT /(npx, py) HAS_TYPE nprat

%%(TCC) nprat_div_negrat_is_nnrat: OBLIGATION

nprat div negrat is nnrat: JUDGEMENT /(npx, ny) HAS_TYPE nnrat

%%(TCC) posrat_plus_nnrat_is_posrat: OBLIGATION

posrat plus nnrat is posrat: JUDGEMENT +(px, nny) HAS_TYPE posrat

%%(TCC) nnrat_plus_posrat_is_posrat: OBLIGATION

nnrat plus posrat is posrat: JUDGEMENT +(nnx, py) HAS_TYPE posrat

%%(TCC) posrat_times_posrat_is_posrat: OBLIGATION

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

%%(TCC) posrat_div_posrat_is_posrat: OBLIGATION

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

%%(TCC) negrat_plus_negrat_is_negrat: OBLIGATION

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

%%(TCC) negrat_times_negrat_is_posrat: OBLIGATION

negrat times negrat is posrat: JUDGEMENT *(nx, ny) HAS_TYPE posrat

%%(TCC) negrat_div_negrat_is_posrat: OBLIGATION

negrat div negrat is posrat: JUDGEMENT /(nx, ny) HAS_TYPE posrat

END rationals