--- a/src/ZF/ex/Primes.thy Tue Jun 26 17:04:09 2001 +0200
+++ b/src/ZF/ex/Primes.thy Tue Jun 26 17:04:54 2001 +0200
@@ -8,23 +8,26 @@
Primes = Main +
consts
- dvd :: [i,i]=>o (infixl 70)
- gcd :: [i,i,i]=>o (* great common divisor *)
- egcd :: [i,i]=>i (* gcd by Euclid's algorithm *)
- coprime :: [i,i]=>o (* coprime definition *)
- prime :: i=>o (* prime definition *)
+ dvd :: [i,i]=>o (infixl 50)
+ is_gcd :: [i,i,i]=>o (* great common divisor *)
+ gcd :: [i,i]=>i (* gcd by Euclid's algorithm *)
defs
dvd_def "m dvd n == m \\<in> nat & n \\<in> nat & (\\<exists>k \\<in> nat. n = m#*k)"
- gcd_def "gcd(p,m,n) == ((p dvd m) & (p dvd n)) &
- (\\<forall>d. (d dvd m) & (d dvd n) --> d dvd p)"
+ is_gcd_def "is_gcd(p,m,n) == ((p dvd m) & (p dvd n)) &
+ (\\<forall>d\\<in>nat. (d dvd m) & (d dvd n) --> d dvd p)"
- egcd_def "egcd(m,n) ==
- transrec(n, %n f. \\<lambda>m \\<in> nat. if(n=0, m, f`(m mod n)`n)) ` m"
+ gcd_def "gcd(m,n) ==
+ transrec(natify(n),
+ %n f. \\<lambda>m \\<in> nat.
+ if n=0 then m else f`(m mod n)`n) ` natify(m)"
- coprime_def "coprime(m,n) == egcd(m,n) = 1"
-
- prime_def "prime(n) == (1<n) & (\\<forall>m \\<in> nat. 1<m & m<n --> ~(m dvd n))"
+constdefs
+ coprime :: [i,i]=>o (* coprime relation *)
+ "coprime(m,n) == gcd(m,n) = 1"
+
+ prime :: i (* set of prime numbers *)
+ "prime == {p \\<in> nat. 1<p & (\\<forall>m \\<in> nat. m dvd p --> m=1 | m=p)}"
end