Quelle  gcd.pvs

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