1335

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

1374

12 
divides :: [nat, nat] => bool (infixl 70)


13 
cd :: [nat, nat, nat] => bool


14 
gcd :: [nat, nat] => nat

1335

15 

1374

16 
pow :: [nat, nat] => nat (infixl 75)


17 
fac :: nat => nat

1335

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
