src/HOL/ex/Primes.thy
 author paulson Wed Nov 05 13:23:46 1997 +0100 (1997-11-05) changeset 4153 e534c4c32d54 parent 3495 04739732b13e child 5184 9b8547a9496a permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
```     1 (*  Title:      HOL/ex/Primes.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Christophe Tabacznyj and Lawrence C Paulson
```
```     4     Copyright   1996  University of Cambridge
```
```     5
```
```     6 The Greatest Common Divisor and Euclid's algorithm
```
```     7
```
```     8 The "simpset" clause in the recdef declaration is omitted on purpose:
```
```     9 	in order to demonstrate the treatment of definitions that have
```
```    10 	unproved termination conditions.  Restoring the clause lets
```
```    11 	Isabelle prove those conditions.
```
```    12 *)
```
```    13
```
```    14 Primes = Divides + WF_Rel +
```
```    15 consts
```
```    16   is_gcd  :: [nat,nat,nat]=>bool          (*gcd as a relation*)
```
```    17   gcd     :: "nat*nat=>nat"               (*Euclid's algorithm *)
```
```    18   coprime :: [nat,nat]=>bool
```
```    19   prime   :: nat set
```
```    20
```
```    21 recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)"
```
```    22 (*  simpset "!simpset addsimps [mod_less_divisor, zero_less_eq]" *)
```
```    23     "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
```
```    24
```
```    25 defs
```
```    26   is_gcd_def  "is_gcd p m n == p dvd m  &  p dvd n  &
```
```    27                                (ALL d. d dvd m & d dvd n --> d dvd p)"
```
```    28
```
```    29   coprime_def "coprime m n == gcd(m,n) = 1"
```
```    30
```
```    31   prime_def   "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
```
```    32
```
```    33 end
```