author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1478  2b8c2a7547ab 
child 2469  b50b8c0eec01 
permissions  rwrr 
1478  1 
(* Title: ZF/arith.thy 
0  2 
ID: $Id$ 
1478  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 

6 
Arithmetic operators and their definitions 

7 
*) 

8 

124  9 
Arith = Epsilon + "simpdata" + 
0  10 
consts 
1401  11 
rec :: [i, i, [i,i]=>i]=>i 
1478  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) 

0  17 

753  18 
defs 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

19 
rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))" 
0  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)" 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
6
diff
changeset

24 
mod_def "m mod n == transrec(m, %j f. if(j<n, j, f`(j#n)))" 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
6
diff
changeset

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