src/HOL/Hoare/Arith2.thy
author berghofe
Fri Jul 24 13:03:20 1998 +0200 (1998-07-24)
changeset 5183 89f162de39cf
parent 4359 6f2986464280
child 8791 50b650d19641
permissions -rw-r--r--
Adapted to new datatype package.
clasohm@1476
     1
(*  Title:      HOL/Hoare/Arith2.thy
nipkow@1335
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Norbert Galm
nipkow@1335
     4
    Copyright   1995 TUM
nipkow@1335
     5
paulson@3372
     6
More arithmetic.  Much of this duplicates ex/Primes.
nipkow@1335
     7
*)
nipkow@1335
     8
nipkow@4359
     9
Arith2 = Power +
nipkow@1335
    10
clasohm@1558
    11
constdefs
clasohm@1476
    12
  cd      :: [nat, nat, nat] => bool
paulson@3372
    13
  "cd x m n  == x dvd m & x dvd n"
nipkow@1335
    14
clasohm@1558
    15
  gcd     :: [nat, nat] => nat
clasohm@1558
    16
  "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
nipkow@1335
    17
nipkow@4359
    18
consts fac     :: nat => nat
berghofe@5183
    19
berghofe@5183
    20
primrec
berghofe@5183
    21
  "fac 0 = Suc 0"
berghofe@5183
    22
  "fac(Suc n) = (Suc n)*fac(n)"
nipkow@1335
    23
nipkow@1335
    24
end