author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 124  858ab9a9b047 
permissions  rwrr 
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 

124  9 
Arith = Epsilon + "simpdata" + 
0  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 

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 