4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 |
5 |
6 Arithmetic operators and their definitions |
6 Arithmetic operators and their definitions |
7 *) |
7 *) |
8 |
8 |
9 Arith = Epsilon + |
9 Arith = Univ + |
10 |
10 |
11 setup setup_datatypes |
11 constdefs |
|
12 pred :: i=>i (*inverse of succ*) |
|
13 "pred(y) == THE x. y = succ(x)" |
12 |
14 |
13 (*The natural numbers as a datatype*) |
15 natify :: i=>i (*coerces non-nats to nats*) |
14 rep_datatype |
16 "natify == Vrecursor(%f a. if a = succ(pred(a)) then succ(f`pred(a)) |
15 elim natE |
17 else 0)" |
16 induct nat_induct |
|
17 case_eqns nat_case_0, nat_case_succ |
|
18 recursor_eqns recursor_0, recursor_succ |
|
19 |
|
20 |
18 |
21 consts |
19 consts |
22 "#*" :: [i,i]=>i (infixl 70) |
20 "##*" :: [i,i]=>i (infixl 70) |
23 div :: [i,i]=>i (infixl 70) |
21 "##+" :: [i,i]=>i (infixl 65) |
24 mod :: [i,i]=>i (infixl 70) |
22 "##-" :: [i,i]=>i (infixl 65) |
25 "#+" :: [i,i]=>i (infixl 65) |
|
26 "#-" :: [i,i]=>i (infixl 65) |
|
27 |
23 |
28 primrec |
24 primrec |
29 add_0 "0 #+ n = n" |
25 raw_add_0 "0 ##+ n = n" |
30 add_succ "succ(m) #+ n = succ(m #+ n)" |
26 raw_add_succ "succ(m) ##+ n = succ(m ##+ n)" |
31 |
27 |
32 primrec |
28 primrec |
33 diff_0 "m #- 0 = m" |
29 raw_diff_0 "m ##- 0 = m" |
34 diff_SUCC "m #- succ(n) = nat_case(0, %x. x, m #- n)" |
30 raw_diff_succ "m ##- succ(n) = nat_case(0, %x. x, m ##- n)" |
35 |
31 |
36 primrec |
32 primrec |
37 mult_0 "0 #* n = 0" |
33 raw_mult_0 "0 ##* n = 0" |
38 mult_succ "succ(m) #* n = n #+ (m #* n)" |
34 raw_mult_succ "succ(m) ##* n = n ##+ (m ##* n)" |
39 |
35 |
40 defs |
36 constdefs |
41 mod_def "m mod n == transrec(m, %j f. if j<n then j else f`(j#-n))" |
37 add :: [i,i]=>i (infixl "#+" 65) |
42 div_def "m div n == transrec(m, %j f. if j<n then 0 else succ(f`(j#-n)))" |
38 "m #+ n == natify(m) ##+ natify(n)" |
|
39 |
|
40 diff :: [i,i]=>i (infixl "#-" 65) |
|
41 "m #- n == natify(m) ##- natify(n)" |
|
42 |
|
43 mult :: [i,i]=>i (infixl "#*" 70) |
|
44 "m #* n == natify(m) ##* natify(n)" |
|
45 |
|
46 div :: [i,i]=>i (infixl "div" 70) |
|
47 "m div n == transrec(m, %j f. if j<n then 0 else succ(f`(j#-n)))" |
|
48 |
|
49 mod :: [i,i]=>i (infixl "mod" 70) |
|
50 "m mod n == transrec(m, %j f. if j<n then j else f`(j#-n))" |
|
51 |
43 end |
52 end |