| author | paulson |
| Fri, 25 Sep 1998 14:05:13 +0200 | |
| changeset 5565 | 301a3a4d3dc7 |
| parent 3840 | e0baea4d485a |
| child 6070 | 032babd0120b |
| permissions | -rw-r--r-- |
| 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 |
||
| 2469 | 9 |
Arith = Epsilon + |
| 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 |
|
| 3840 | 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))" |
|
| 0 | 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 |