|
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
¤ Dauer der Verarbeitung: 0.20 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.
|
