|
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 |