src/HOL/Hoare/Arith2.thy
author clasohm
Mon Feb 05 21:29:06 1996 +0100 (1996-02-05)
changeset 1476 608483c2122a
parent 1374 5e407f2a3323
child 1558 9c6ebfab4e05
permissions -rw-r--r--
expanded tabs; incorporated Konrad's changes
     1 (*  Title:      HOL/Hoare/Arith2.thy
     2     ID:         $Id$
     3     Author:     Norbert Galm
     4     Copyright   1995 TUM
     5 
     6 More arithmetic.
     7 *)
     8 
     9 Arith2 = Arith +
    10 
    11 consts
    12   divides :: [nat, nat] => bool                 (infixl 70)
    13   cd      :: [nat, nat, nat] => bool
    14   gcd     :: [nat, nat] => nat
    15 
    16   pow     :: [nat, nat] => nat                  (infixl 75)
    17   fac     :: nat => nat
    18 
    19 defs
    20   divides_def   "x divides n == 0<n & 0<x & (n mod x) = 0"
    21   cd_def        "cd x m n  == x divides m & x divides n"
    22   gcd_def       "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
    23 
    24   pow_def       "m pow n     == nat_rec n (Suc 0) (%u v.m*v)"
    25   fac_def       "fac m       == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
    26 
    27 end