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