|
1474
|
1 |
(* Title: CTT/arith
|
|
0
|
2 |
ID: $Id$
|
|
1474
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
0
|
4 |
Copyright 1991 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Arithmetic operators and their definitions
|
|
|
7 |
|
|
|
8 |
Proves about elementary arithmetic: addition, multiplication, etc.
|
|
|
9 |
Tests definitions and simplifier.
|
|
|
10 |
*)
|
|
|
11 |
|
|
|
12 |
Arith = CTT +
|
|
|
13 |
|
|
1474
|
14 |
consts "#+","-","|-|" :: "[i,i]=>i" (infixr 65)
|
|
|
15 |
"#*",div,mod :: "[i,i]=>i" (infixr 70)
|
|
0
|
16 |
|
|
|
17 |
rules
|
|
3837
|
18 |
add_def "a#+b == rec(a, b, %u v. succ(v))"
|
|
|
19 |
diff_def "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"
|
|
0
|
20 |
absdiff_def "a|-|b == (a-b) #+ (b-a)"
|
|
|
21 |
mult_def "a#*b == rec(a, 0, %u v. b #+ v)"
|
|
3837
|
22 |
mod_def "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
|
|
|
23 |
div_def "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
|
|
0
|
24 |
end
|