11 begin |
11 begin |
12 |
12 |
13 subsection {* Arithmetic operators and their definitions *} |
13 subsection {* Arithmetic operators and their definitions *} |
14 |
14 |
15 definition |
15 definition |
16 add :: "[i,i]=>i" (infixr "#+" 65) |
16 add :: "[i,i]=>i" (infixr "#+" 65) where |
17 "a#+b == rec(a, b, %u v. succ(v))" |
17 "a#+b == rec(a, b, %u v. succ(v))" |
18 |
18 |
19 diff :: "[i,i]=>i" (infixr "-" 65) |
19 definition |
|
20 diff :: "[i,i]=>i" (infixr "-" 65) where |
20 "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))" |
21 "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))" |
21 |
22 |
22 absdiff :: "[i,i]=>i" (infixr "|-|" 65) |
23 definition |
|
24 absdiff :: "[i,i]=>i" (infixr "|-|" 65) where |
23 "a|-|b == (a-b) #+ (b-a)" |
25 "a|-|b == (a-b) #+ (b-a)" |
24 |
26 |
25 mult :: "[i,i]=>i" (infixr "#*" 70) |
27 definition |
|
28 mult :: "[i,i]=>i" (infixr "#*" 70) where |
26 "a#*b == rec(a, 0, %u v. b #+ v)" |
29 "a#*b == rec(a, 0, %u v. b #+ v)" |
27 |
30 |
28 mod :: "[i,i]=>i" (infixr "mod" 70) |
31 definition |
|
32 mod :: "[i,i]=>i" (infixr "mod" 70) where |
29 "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))" |
33 "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))" |
30 |
34 |
31 div :: "[i,i]=>i" (infixr "div" 70) |
35 definition |
|
36 div :: "[i,i]=>i" (infixr "div" 70) where |
32 "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))" |
37 "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))" |
33 |
38 |
34 |
39 |
35 notation (xsymbols) |
40 notation (xsymbols) |
36 mult (infixr "#\<times>" 70) |
41 mult (infixr "#\<times>" 70) |