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


18 
add_def "a#+b == rec(a, b, %u v.succ(v))"


19 
diff_def "ab == rec(b, a, %u v.rec(v, 0, %x y.x))"


20 
absdiff_def "ab == (ab) #+ (ba)"


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
