author  paulson 
Tue, 14 Nov 2000 13:26:48 +0100  
changeset 10467  e6e7205e9e91 
parent 3837  d7f033c74b38 
child 12110  f8b4b11cd79d 
permissions  rwrr 
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
xsymbol support for Pi, Sigma, >, : (membership)
paulson
parents:
3837
diff
changeset

17 
syntax (symbols) 
e6e7205e9e91
xsymbol support for Pi, Sigma, >, : (membership)
paulson
parents:
3837
diff
changeset

18 
"op #*" :: [i, i] => i (infixr "#\\<times>" 70) 
e6e7205e9e91
xsymbol support for Pi, Sigma, >, : (membership)
paulson
parents:
3837
diff
changeset

19 

e6e7205e9e91
xsymbol support for Pi, Sigma, >, : (membership)
paulson
parents:
3837
diff
changeset

20 
syntax (HTML output) 
e6e7205e9e91
xsymbol support for Pi, Sigma, >, : (membership)
paulson
parents:
3837
diff
changeset

21 
"op #*" :: [i, i] => i (infixr "#\\<times>" 70) 
e6e7205e9e91
xsymbol 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 "ab == rec(b, a, %u v. rec(v, 0, %x y. x))" 

0  26 
absdiff_def "ab == (ab) #+ (ba)" 
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 