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


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
