| author | oheimb |
| Wed, 12 Nov 1997 12:34:43 +0100 | |
| changeset 4206 | 688050e83d89 |
| parent 124 | 858ab9a9b047 |
| permissions | -rw-r--r-- |
| 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 |