FDL > PVS > Number Theory > divisibility : Theory

PVS-2.4 number theory/divisibility.pvs

divisibility : THEORY
BEGIN

IMPORTING mod nt

n: VAR nat

n1: VAR nat

n2: VAR nat

m: VAR posnat

m1: VAR posnat

m2: VAR posnat

i: VAR int

j: VAR int

k: VAR int

ip: VAR int

jp: VAR int

nn: VAR nzint

mm: VAR nzint

ii: VAR nzint

jj: VAR nzint

kk: VAR nzint

divides(mm, i): bool = EXISTS (k:int) : i = (mm * k);

divides lt: LEMMA (i /= 0) IMPLIES divides(mm, i) IMPLIES (mm < = abs(i))

divides lt abs: LEMMA divides(mm, ii) IMPLIES (abs(mm) < = abs(ii))

divides mod: LEMMA divides(m, i) = (mod(i, m) = 0)

divides sym: LEMMA divides(mm, ii) = divides(mm, -ii)

divides plus 1: LEMMA (mm > 1) IMPLIES divides(mm, ii) IMPLIES (NOT divides(mm, ii + 1))

IMPORTING min posnat

%%(TCC) lcm_TCC1: OBLIGATION

lcm(m1, m2): int = min({(k:posnat) | divides(m1, k) AND divides(m2, k)});

IMPORTING max bounded posnat

gcd noem: LEMMA nonempty?({(k:posnat) | divides(k, i) AND divides(k, j)})

gcd prep: LEMMA FORALL (i:int), (j:{(jj:int) | (i = 0) = > (jj /= 0)} ) : EXISTS (UB:posnat) : FORALL (y:({(k:posnat) | divides(k, i) AND divides(k, j)}) ) : y < = UB

END divisibility