| author | wenzelm |
| Fri, 26 Oct 2001 14:02:58 +0200 | |
| changeset 11944 | 0594e63e6057 |
| parent 10467 | e6e7205e9e91 |
| child 12110 | f8b4b11cd79d |
| permissions | -rw-r--r-- |
| 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 |
|
|
10467
e6e7205e9e91
x-symbol support for Pi, Sigma, -->, : (membership)
paulson
parents:
3837
diff
changeset
|
17 |
syntax (symbols) |
|
e6e7205e9e91
x-symbol support for Pi, Sigma, -->, : (membership)
paulson
parents:
3837
diff
changeset
|
18 |
"op #*" :: [i, i] => i (infixr "#\\<times>" 70) |
|
e6e7205e9e91
x-symbol support for Pi, Sigma, -->, : (membership)
paulson
parents:
3837
diff
changeset
|
19 |
|
|
e6e7205e9e91
x-symbol support for Pi, Sigma, -->, : (membership)
paulson
parents:
3837
diff
changeset
|
20 |
syntax (HTML output) |
|
e6e7205e9e91
x-symbol support for Pi, Sigma, -->, : (membership)
paulson
parents:
3837
diff
changeset
|
21 |
"op #*" :: [i, i] => i (infixr "#\\<times>" 70) |
|
e6e7205e9e91
x-symbol support for Pi, Sigma, -->, : (membership)
paulson
parents:
3837
diff
changeset
|
22 |
|
| 0 | 23 |
rules |
| 3837 | 24 |
add_def "a#+b == rec(a, b, %u v. succ(v))" |
25 |
diff_def "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))" |
|
| 0 | 26 |
absdiff_def "a|-|b == (a-b) #+ (b-a)" |
27 |
mult_def "a#*b == rec(a, 0, %u v. b #+ v)" |
|
| 3837 | 28 |
mod_def "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))" |
29 |
div_def "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))" |
|
| 0 | 30 |
end |