author | wenzelm |
Fri, 16 Sep 2005 23:01:29 +0200 | |
changeset 17441 | 5b5feca0344a |
parent 12110 | f8b4b11cd79d |
child 19761 | 5cd82054c2c6 |
permissions | -rw-r--r-- |
17441 | 1 |
(* Title: CTT/Arith.thy |
0 | 2 |
ID: $Id$ |
1474 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1991 University of Cambridge |
5 |
*) |
|
6 |
||
17441 | 7 |
header {* Arithmetic operators and their definitions *} |
8 |
||
9 |
theory Arith |
|
10 |
imports Bool |
|
11 |
begin |
|
0 | 12 |
|
17441 | 13 |
text {* |
14 |
Proves about elementary arithmetic: addition, multiplication, etc. |
|
15 |
Tests definitions and simplifier. |
|
16 |
*} |
|
17 |
||
18 |
consts |
|
19 |
"#+" :: "[i,i]=>i" (infixr 65) |
|
20 |
"-" :: "[i,i]=>i" (infixr 65) |
|
21 |
"|-|" :: "[i,i]=>i" (infixr 65) |
|
22 |
"#*" :: "[i,i]=>i" (infixr 70) |
|
23 |
div :: "[i,i]=>i" (infixr 70) |
|
24 |
mod :: "[i,i]=>i" (infixr 70) |
|
0 | 25 |
|
12110
f8b4b11cd79d
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
10467
diff
changeset
|
26 |
syntax (xsymbols) |
17441 | 27 |
"op #*" :: "[i, i] => i" (infixr "#\<times>" 70) |
10467
e6e7205e9e91
x-symbol support for Pi, Sigma, -->, : (membership)
paulson
parents:
3837
diff
changeset
|
28 |
|
e6e7205e9e91
x-symbol support for Pi, Sigma, -->, : (membership)
paulson
parents:
3837
diff
changeset
|
29 |
syntax (HTML output) |
17441 | 30 |
"op #*" :: "[i, i] => i" (infixr "#\<times>" 70) |
10467
e6e7205e9e91
x-symbol support for Pi, Sigma, -->, : (membership)
paulson
parents:
3837
diff
changeset
|
31 |
|
17441 | 32 |
defs |
33 |
add_def: "a#+b == rec(a, b, %u v. succ(v))" |
|
34 |
diff_def: "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))" |
|
35 |
absdiff_def: "a|-|b == (a-b) #+ (b-a)" |
|
36 |
mult_def: "a#*b == rec(a, 0, %u v. b #+ v)" |
|
37 |
mod_def: "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))" |
|
38 |
div_def: "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))" |
|
39 |
||
40 |
ML {* use_legacy_bindings (the_context ()) *} |
|
41 |
||
0 | 42 |
end |