src/HOL/Hoare/Arith2.thy
author paulson
Fri May 30 15:21:21 1997 +0200 (1997-05-30)
changeset 3372 6e472c8f0011
parent 1824 44254696843a
child 3842 b55686a7b22c
permissions -rw-r--r--
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
     1 (*  Title:      HOL/Hoare/Arith2.thy
     2     ID:         $Id$
     3     Author:     Norbert Galm
     4     Copyright   1995 TUM
     5 
     6 More arithmetic.  Much of this duplicates ex/Primes.
     7 *)
     8 
     9 Arith2 = Divides +
    10 
    11 constdefs
    12   cd      :: [nat, nat, nat] => bool
    13   "cd x m n  == x dvd m & x dvd n"
    14 
    15   gcd     :: [nat, nat] => nat
    16   "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
    17 
    18   pow     :: [nat, nat] => nat                              (infixl 75)
    19   "m pow n     == nat_rec (Suc 0) (%u v.m*v) n"
    20 
    21   fac     :: nat => nat
    22   "fac m       == nat_rec (Suc 0) (%u v.(Suc u)*v) m"
    23 
    24 end