author | paulson |
Mon, 21 May 2001 14:36:24 +0200 | |
changeset 11316 | b4e71bd751e4 |
parent 9548 | 15bee2731e43 |
child 11382 | a816fead971a |
permissions | -rw-r--r-- |
1792
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
1 |
(* Title: ZF/ex/Primes.thy |
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
3 |
Author: Christophe Tabacznyj and Lawrence C Paulson |
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
4 |
Copyright 1996 University of Cambridge |
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
5 |
|
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
6 |
The "divides" relation, the greatest common divisor and Euclid's algorithm |
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
7 |
*) |
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
8 |
|
9548 | 9 |
Primes = Main + |
1792
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
10 |
consts |
1793 | 11 |
dvd :: [i,i]=>o (infixl 70) |
12 |
gcd :: [i,i,i]=>o (* great common divisor *) |
|
13 |
egcd :: [i,i]=>i (* gcd by Euclid's algorithm *) |
|
14 |
coprime :: [i,i]=>o (* coprime definition *) |
|
15 |
prime :: i=>o (* prime definition *) |
|
1792
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
16 |
|
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
17 |
defs |
11316 | 18 |
dvd_def "m dvd n == m \\<in> nat & n \\<in> nat & (\\<exists>k \\<in> nat. n = m#*k)" |
1792
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
19 |
|
1793 | 20 |
gcd_def "gcd(p,m,n) == ((p dvd m) & (p dvd n)) & |
11316 | 21 |
(\\<forall>d. (d dvd m) & (d dvd n) --> d dvd p)" |
1792
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
22 |
|
1793 | 23 |
egcd_def "egcd(m,n) == |
11316 | 24 |
transrec(n, %n f. \\<lambda>m \\<in> nat. if(n=0, m, f`(m mod n)`n)) ` m" |
1792
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
25 |
|
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
26 |
coprime_def "coprime(m,n) == egcd(m,n) = 1" |
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
27 |
|
11316 | 28 |
prime_def "prime(n) == (1<n) & (\\<forall>m \\<in> nat. 1<m & m<n --> ~(m dvd n))" |
1792
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
29 |
|
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
30 |
end |