FDL > PVS > Number Theory > div_nt_alt : Theory

PVS-2.4 number theory/div nt alt.pvs

div_nt_alt : THEORY
BEGIN

IMPORTING div nt

n: VAR nat

m: VAR posnat

%%(TCC) natdiv_TCC1: OBLIGATION

%%(TCC) natdiv_TCC2: OBLIGATION

natdiv(n, m) : RECURSIVE nat =
IF n > = m THEN 1 + natdiv(n - m, m) ELSE 0 ENDIF
MEASURE LAMBDA n, m : n ;

i: VAR int

k: VAR int

j: VAR nonzero integer

is multiple(i, j): bool = EXISTS k : i = (k * j);

rdiv(i, j): integer = IF sgn(i) = sgn(j) THEN natdiv(abs(i), abs(j)) ELSE IF is multiple(i, j) THEN -natdiv(abs(i), abs(j)) ELSE (-natdiv(abs(i), abs(j))) - 1 ENDIF ENDIF;

floor is natdiv: LEMMA natdiv(n, m) = floor(n / m)

rdiv lem: LEMMA div(i, j) = rdiv(i, j)

END div_nt_alt