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