|
0
|
1 |
(* Title: FOL/ex/nat2.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
352
|
4 |
Copyright 1994 University of Cambridge
|
|
0
|
5 |
|
|
|
6 |
Theory for examples of simplification and induction on the natural numbers
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Nat2 = FOL +
|
|
|
10 |
|
|
352
|
11 |
types nat
|
|
0
|
12 |
arities nat :: term
|
|
|
13 |
|
|
352
|
14 |
consts
|
|
|
15 |
succ,pred :: "nat => nat"
|
|
0
|
16 |
"0" :: "nat" ("0")
|
|
|
17 |
"+" :: "[nat,nat] => nat" (infixr 90)
|
|
|
18 |
"<","<=" :: "[nat,nat] => o" (infixr 70)
|
|
|
19 |
|
|
|
20 |
rules
|
|
|
21 |
pred_0 "pred(0) = 0"
|
|
|
22 |
pred_succ "pred(succ(m)) = m"
|
|
|
23 |
|
|
|
24 |
plus_0 "0+n = n"
|
|
|
25 |
plus_succ "succ(m)+n = succ(m+n)"
|
|
|
26 |
|
|
|
27 |
nat_distinct1 "~ 0=succ(n)"
|
|
|
28 |
nat_distinct2 "~ succ(m)=0"
|
|
|
29 |
succ_inject "succ(m)=succ(n) <-> m=n"
|
|
|
30 |
|
|
|
31 |
leq_0 "0 <= n"
|
|
|
32 |
leq_succ_succ "succ(m)<=succ(n) <-> m<=n"
|
|
|
33 |
leq_succ_0 "~ succ(m) <= 0"
|
|
|
34 |
|
|
|
35 |
lt_0_succ "0 < succ(n)"
|
|
|
36 |
lt_succ_succ "succ(m)<succ(n) <-> m<n"
|
|
|
37 |
lt_0 "~ m < 0"
|
|
|
38 |
|
|
|
39 |
nat_ind "[| P(0); ALL n. P(n)-->P(succ(n)) |] ==> All(P)"
|
|
|
40 |
end
|