equal
deleted
inserted
replaced
|
1 (* Title: CTT/arith |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
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 |
|
14 consts "#+","-","|-|" :: "[i,i]=>i" (infixr 65) |
|
15 "#*",div,mod :: "[i,i]=>i" (infixr 70) |
|
16 |
|
17 rules |
|
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))" |
|
20 absdiff_def "a|-|b == (a-b) #+ (b-a)" |
|
21 mult_def "a#*b == rec(a, 0, %u v. b #+ v)" |
|
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))" |
|
24 end |