author | paulson |
Fri, 30 May 1997 15:23:49 +0200 | |
changeset 3376 | 0cc2eaa8b0f9 |
parent 3242 | 406ae5ced4e9 |
child 3495 | 04739732b13e |
permissions | -rw-r--r-- |
1804 | 1 |
(* Title: HOL/ex/Primes.thy |
2 |
ID: $Id$ |
|
3 |
Author: Christophe Tabacznyj and Lawrence C Paulson |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
3376 | 6 |
The Greatest Common Divisor and Euclid's algorithm |
1804 | 7 |
*) |
8 |
||
3376 | 9 |
Primes = Divides + WF_Rel + |
1804 | 10 |
consts |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
1804
diff
changeset
|
11 |
is_gcd :: [nat,nat,nat]=>bool (*gcd as a relation*) |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
1804
diff
changeset
|
12 |
gcd :: "nat*nat=>nat" (*Euclid's algorithm *) |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
1804
diff
changeset
|
13 |
coprime :: [nat,nat]=>bool |
3376 | 14 |
prime :: nat set |
1804 | 15 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
1804
diff
changeset
|
16 |
recdef gcd "measure ((%(x,y).y) ::nat*nat=>nat)" |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
1804
diff
changeset
|
17 |
"gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
1804
diff
changeset
|
18 |
|
1804 | 19 |
defs |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
1804
diff
changeset
|
20 |
is_gcd_def "is_gcd p m n == p dvd m & p dvd n & |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
1804
diff
changeset
|
21 |
(ALL d. d dvd m & d dvd n --> d dvd p)" |
1804 | 22 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
1804
diff
changeset
|
23 |
coprime_def "coprime m n == gcd(m,n) = 1" |
1804 | 24 |
|
3376 | 25 |
prime_def "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}" |
1804 | 26 |
|
27 |
end |