author  wenzelm 
Fri, 16 Sep 2005 23:01:29 +0200  
changeset 17441  5b5feca0344a 
parent 12110  f8b4b11cd79d 
child 19761  5cd82054c2c6 
permissions  rwrr 
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
xsymbol support for Pi, Sigma, >, : (membership)
paulson
parents:
3837
diff
changeset

28 

e6e7205e9e91
xsymbol 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
xsymbol 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: "ab == rec(b, a, %u v. rec(v, 0, %x y. x))" 

35 
absdiff_def: "ab == (ab) #+ (ba)" 

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 