|
gcd: THEORY
%------------------------------------------------------------------------------
% Author: Alfons Geser, HTWK Leipzig, Germany
% Ricky W. Butler, NASA Langley
% Date: May, 2009
%
% Anthony N (March 2012)
%------------------------------------------------------------------------------
BEGIN
IMPORTING divides_lems, mod_lems
IMPORTING div %% for proof
n,m: VAR nat
nn,mm: VAR posnat
p, q, l: VAR posint
i,j,k,ip,jp: VAR int
ii,jj,kk: VAR nzint
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)})
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
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)
gcd_lt_nat : LEMMA (n /= 0) IMPLIES
gcd(n,m) <= n
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)
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))
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))
gcd_same : LEMMA gcd(p, p) = p
gcd_minus: LEMMA p /= q IMPLIES gcd(p, q) = gcd(p, q - p)
gcd_times: LEMMA gcd(p * l, q * l) = gcd(p, q) * l
%
% relatively_prime
%
rel_prime(i:int,j: {jj:int| i=0 => jj /= 0}): bool = (gcd(i,j) = 1)
rel_prime_lem: LEMMA (i /= 0 OR j /= 0) IMPLIES
( rel_prime(i,j)
IFF (EXISTS (n,m: int): 1 = m*i + n*j) )
% Bezouts: LEMMA gcd(a,b) = d IMPLIES
% EXISTS (j,k: int): a*j+b*k = d
rel_prime_div_prod: LEMMA (i/=0 OR j/=0) IMPLIES
rel_prime(i,j) AND divides(i,j*k) IMPLIES divides(i,k)
rel_prime_sym: LEMMA (i/=0 OR j/=0) IMPLIES rel_prime(i,j) = rel_prime(j,i)
rel_prime_mult_right: LEMMA (i/=0 OR j/=0) AND (i/=0 OR k/=0)
AND rel_prime(i,j) AND rel_prime(i,k) IMPLIES rel_prime(i,j*k)
rel_prime_mult_left: LEMMA (i/=0 OR j/=0) AND (j/=0 OR k/=0)
AND rel_prime(i,j) AND rel_prime(k,j) IMPLIES rel_prime(i*k,j)
%
% Euclid's algorithm
%
compute_gcd(i:int,j:{jj:int| i=0 => jj /= 0}): RECURSIVE {kj: posnat | kj = gcd(i,j)} =
IF i<0 THEN compute_gcd(-i,j)
ELSIF j<0 THEN compute_gcd(i,-j)
ELSIF i=0 THEN j
ELSIF j=0 THEN i
ELSIF i<j THEN compute_gcd(j,i)
ELSE
(LET rem = mod(i,j) IN
IF rem = 0 THEN j ELSE compute_gcd(j,rem) ENDIF)
ENDIF
MEASURE (IF i<0 AND j<0 THEN -i-j+3
ELSIF i<0 THEN -i+j+2
ELSIF j<0 THEN i-j+2
ELSIF i<j THEN i+j+1
ELSE i+j ENDIF)
% Inverse
IMPORTING pigeonhole
rel_prime_inverse: LEMMA
m>1 AND rel_prime(n,m) IMPLIES
FORALL (q:below(m)): EXISTS (k:below(m)): mod(n*k,m) = q
END gcd
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
