11 types nat |
11 types nat |
12 arities nat :: term |
12 arities nat :: term |
13 |
13 |
14 consts |
14 consts |
15 succ,pred :: nat => nat |
15 succ,pred :: nat => nat |
16 "0" :: nat ("0") |
16 "0" :: nat ("0") |
17 "+" :: [nat,nat] => nat (infixr 90) |
17 "+" :: [nat,nat] => nat (infixr 90) |
18 "<","<=" :: [nat,nat] => o (infixr 70) |
18 "<","<=" :: [nat,nat] => o (infixr 70) |
19 |
19 |
20 rules |
20 rules |
21 pred_0 "pred(0) = 0" |
21 pred_0 "pred(0) = 0" |
22 pred_succ "pred(succ(m)) = m" |
22 pred_succ "pred(succ(m)) = m" |
23 |
23 |
24 plus_0 "0+n = n" |
24 plus_0 "0+n = n" |
25 plus_succ "succ(m)+n = succ(m+n)" |
25 plus_succ "succ(m)+n = succ(m+n)" |
26 |
26 |
27 nat_distinct1 "~ 0=succ(n)" |
27 nat_distinct1 "~ 0=succ(n)" |
28 nat_distinct2 "~ succ(m)=0" |
28 nat_distinct2 "~ succ(m)=0" |
29 succ_inject "succ(m)=succ(n) <-> m=n" |
29 succ_inject "succ(m)=succ(n) <-> m=n" |
30 |
30 |
31 leq_0 "0 <= n" |
31 leq_0 "0 <= n" |
32 leq_succ_succ "succ(m)<=succ(n) <-> m<=n" |
32 leq_succ_succ "succ(m)<=succ(n) <-> m<=n" |
33 leq_succ_0 "~ succ(m) <= 0" |
33 leq_succ_0 "~ succ(m) <= 0" |
34 |
34 |
35 lt_0_succ "0 < succ(n)" |
35 lt_0_succ "0 < succ(n)" |
36 lt_succ_succ "succ(m)<succ(n) <-> m<n" |
36 lt_succ_succ "succ(m)<succ(n) <-> m<n" |
37 lt_0 "~ m < 0" |
37 lt_0 "~ m < 0" |
38 |
38 |
39 nat_ind "[| P(0); ALL n. P(n)-->P(succ(n)) |] ==> All(P)" |
39 nat_ind "[| P(0); ALL n. P(n)-->P(succ(n)) |] ==> All(P)" |
40 end |
40 end |