src/HOL/Hoare/Arith2.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 8791 50b650d19641
child 17278 f27456a2a975
permissions -rw-r--r--
hide many names from Datatype_Universe.

(*  Title:      HOL/Hoare/Arith2.thy
    ID:         $Id$
    Author:     Norbert Galm
    Copyright   1995 TUM

More arithmetic.  Much of this duplicates ex/Primes.
*)

Arith2 = Main +

constdefs
  cd      :: [nat, nat, nat] => bool
  "cd x m n  == x dvd m & x dvd n"

  gcd     :: [nat, nat] => nat
  "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"

consts fac     :: nat => nat

primrec
  "fac 0 = Suc 0"
  "fac(Suc n) = (Suc n)*fac(n)"

end