src/ZF/arith.thy
 changeset 0 a5a9c433f639 child 6 8ce8c4d13d4d
equal inserted replaced
-1:000000000000 0:a5a9c433f639
`       `
`     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`