0

1 
(* Title: ZF/arith.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
Arithmetic operators and their definitions


7 
*)


8 


9 
Arith = Epsilon +


10 
consts


11 
rec :: "[i, i, [i,i]=>i]=>i"


12 
"#*" :: "[i,i]=>i" (infixl 70)


13 
div :: "[i,i]=>i" (infixl 70)


14 
mod :: "[i,i]=>i" (infixl 70)


15 
"#+" :: "[i,i]=>i" (infixl 65)


16 
"#" :: "[i,i]=>i" (infixl 65)


17 


18 
rules


19 
rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(n, a, %m. b(m, f`m)))"


20 


21 
add_def "m#+n == rec(m, n, %u v.succ(v))"


22 
diff_def "m#n == rec(n, m, %u v. rec(v, 0, %x y.x))"


23 
mult_def "m#*n == rec(m, 0, %u v. n #+ v)"


24 
mod_def "m mod n == transrec(m, %j f. if(j:n, j, f`(j#n)))"


25 
div_def "m div n == transrec(m, %j f. if(j:n, 0, succ(f`(j#n))))"


26 
end
