src/ZF/Arith.thy
 author clasohm Tue Feb 06 12:27:17 1996 +0100 (1996-02-06) changeset 1478 2b8c2a7547ab parent 1401 0c439768f45c child 2469 b50b8c0eec01 permissions -rw-r--r--
expanded tabs
```     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 + "simpdata" +
```
```    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 defs
```
```    19     rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
```
```    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
```