Quelle  primes.pvs

primes: THEORY
%------------------------------------------------------------------------------
%
% A prime number is a natural number that has exactly two divisors 1 and itself.
%
% AUTHOR: Rick Butler
%
% NOTE: prime? returns false for negative integers
%
%-------------------------------------------------------------------------------
BEGIN

   IMPORTING divides_lems,factorial

   m: VAR posnat
   N,n: VAR nat

   prime?(i: int): bool = (FORALL (j: posnat): j /= 1 AND j /= i IMPLIES
                              NOT divides(j,i)) 
                            AND i > 1               %% 1 is not a prime number by def

   prime_rew  : LEMMA prime?(n) = ((FORALL (j: posnat): j > 1 AND j < n IMPLIES
                                     NOT divides(j,n)) AND n > 1)

   prime_gt_1 : LEMMA prime?(n) IMPLIES n > 1


  % Also known as Euclid's lemma:

   prime_divides_prod: LEMMA prime?(n) IMPLIES FORALL (i,j:int):
     divides(n,i*j) IMPLIES (divides(n,i) OR divides(n,j))

   prime_divides_factorial: LEMMA prime?(n) IMPLIES 
     (divides(n,factorial(N))
      IFF
      N>=n)

   prod_primes_divides: LEMMA FORALL (m,n:nat,j:int):
     prime?(n) AND prime?(m) AND divides(m,j) AND divides(n,j)
     AND n/=m
     IMPLIES
     divides(m*n,j)


   prime_2    : LEMMA prime?(2)
   prime_3    : LEMMA prime?(3)
   prime_5    : LEMMA prime?(5)
   prime_7    : LEMMA prime?(7)

%  AUTO_REWRITE+ prime_gt_1

END primes