FDL > PVS > Number Theory > gcd : Theory

PVS-2.4 number theory/gcd.pvs

gcd : THEORY
BEGIN

IMPORTING divisibility

n: VAR nat

m: VAR nat

nn: VAR posnat

mm: VAR posnat

i: VAR int

j: VAR int

k: VAR int

ip: VAR int

jp: VAR int

ii: VAR nzint

jj: VAR nzint

kk: VAR nzint

%%(TCC) gcd_TCC1: OBLIGATION

gcd((i:int), (j:{(jj:int) | (i = 0) = > (jj /= 0)} )): {(k:posnat) | divides(k, i) AND divides(k, j)} = max({(k:posnat) | divides(k, i) AND divides(k, j)});

%%(TCC) gcd_divides_TCC1: OBLIGATION

gcd divides: LEMMA ((i /= 0) OR (j /= 0)) IMPLIES (divides(gcd(i, j), i) AND divides(gcd(i, j), j))

gcd is max: LEMMA (((i /= 0) OR (j /= 0)) AND divides(kk, i) AND divides(kk, j)) IMPLIES (kk < = gcd(i, j))

gcd def: LEMMA ((i /= 0) OR (j /= 0)) IMPLIES ((gcd(i, j) = nn) IFF ((divides(nn, i) AND divides(nn, j)) AND (FORALL mm : (divides(mm, i) AND divides(mm, j)) IMPLIES (mm < = nn))))

gcd 0 pos: LEMMA gcd(0, mm) = mm

%%(TCC) gcd_abs_TCC1: OBLIGATION

gcd abs: LEMMA ((i /= 0) OR (j /= 0)) IMPLIES (gcd(i, j) = gcd(abs(i), abs(j)))

gcd 0 neg: LEMMA gcd(0, -mm) = mm

gcd sym: LEMMA ((i /= 0) OR (j /= 0)) IMPLIES (gcd(i, j) = gcd(j, i))

%%(TCC) gcd_lt_nat_TCC1: OBLIGATION

gcd lt nat: LEMMA (n /= 0) IMPLIES (gcd(n, m) < = n)

%%(TCC) gcd_lt_TCC1: OBLIGATION

gcd lt: LEMMA ((i /= 0) AND (j /= 0)) IMPLIES (gcd(i, j) < = min(abs(i), abs(j)))

gcd 0: LEMMA gcd(0, ii) = abs(ii)

%%(TCC) gcd_mod_TCC1: OBLIGATION

%%(TCC) gcd_mod_TCC2: OBLIGATION

gcd mod: LEMMA (i /= 0) IMPLIES (gcd(mod(j, i), i) = gcd(i, j))

gcd mod div: LEMMA (i /= 0) IMPLIES divides(gcd(i, j), mod(j, i))

%%(TCC) gcd_factors_nat_TCC1: OBLIGATION

gcd factors nat: LEMMA ((n /= 0) OR (m /= 0)) IMPLIES (EXISTS ip, jp : gcd(n, m) = ((ip * n) + (jp * m)))

gcd factors: LEMMA ((i /= 0) OR (j /= 0)) IMPLIES (EXISTS ip, jp : gcd(i, j) = ((ip * i) + (jp * j)))

divides gcd: LEMMA (((i /= 0) OR (j /= 0)) AND divides(kk, i) AND divides(kk, j)) IMPLIES divides(kk, gcd(i, j))

END gcd