src/HOL/Hoare/Arith2.thy
author berghofe
Tue Jun 25 13:11:29 1996 +0200 (1996-06-25)
changeset 1824 44254696843a
parent 1558 9c6ebfab4e05
child 3372 6e472c8f0011
permissions -rw-r--r--
Changed argument order of nat_rec.
     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 constdefs
    12   divides :: [nat, nat] => bool                             (infixl 70)
    13   "x divides n == 0<n & 0<x & (n mod x) = 0"
    14 
    15   cd      :: [nat, nat, nat] => bool
    16   "cd x m n  == x divides m & x divides n"
    17 
    18   gcd     :: [nat, nat] => nat
    19   "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
    20 
    21   pow     :: [nat, nat] => nat                              (infixl 75)
    22   "m pow n     == nat_rec (Suc 0) (%u v.m*v) n"
    23 
    24   fac     :: nat => nat
    25   "fac m       == nat_rec (Suc 0) (%u v.(Suc u)*v) m"
    26 
    27 end