author | paulson |
Tue, 23 May 2000 18:08:52 +0200 | |
changeset 8936 | a1c426541757 |
parent 8698 | 8812dad6ef12 |
child 9824 | c6eee0626d28 |
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 |
3495
04739732b13e
New comments on how to deal with unproved termination conditions
paulson
parents:
3376
diff
changeset
|
7 |
|
8698 | 8 |
The "simpset" clause in the recdef declaration used to be necessary when the |
9 |
two lemmas where not part of the default simpset. |
|
1804 | 10 |
*) |
11 |
||
6455 | 12 |
Primes = Main + |
1804 | 13 |
consts |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
1804
diff
changeset
|
14 |
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
|
15 |
gcd :: "nat*nat=>nat" (*Euclid's algorithm *) |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
1804
diff
changeset
|
16 |
coprime :: [nat,nat]=>bool |
3376 | 17 |
prime :: nat set |
1804 | 18 |
|
3495
04739732b13e
New comments on how to deal with unproved termination conditions
paulson
parents:
3376
diff
changeset
|
19 |
recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)" |
6455 | 20 |
(* simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]" *) |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
1804
diff
changeset
|
21 |
"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
|
22 |
|
1804 | 23 |
defs |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
1804
diff
changeset
|
24 |
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
|
25 |
(ALL d. d dvd m & d dvd n --> d dvd p)" |
1804 | 26 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
1804
diff
changeset
|
27 |
coprime_def "coprime m n == gcd(m,n) = 1" |
1804 | 28 |
|
3376 | 29 |
prime_def "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}" |
1804 | 30 |
|
31 |
end |