equal
deleted
inserted
replaced
1 (* Title: FOL/ex/nat2.thy |
1 (* Title: FOL/ex/nat2.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1991 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Theory for examples of simplification and induction on the natural numbers |
6 Theory for examples of simplification and induction on the natural numbers |
7 *) |
7 *) |
8 |
8 |
9 Nat2 = FOL + |
9 Nat2 = FOL + |
10 |
10 |
11 types nat 0 |
11 types nat |
12 arities nat :: term |
12 arities nat :: term |
13 |
13 |
14 consts succ,pred :: "nat => nat" |
14 consts |
|
15 succ,pred :: "nat => nat" |
15 "0" :: "nat" ("0") |
16 "0" :: "nat" ("0") |
16 "+" :: "[nat,nat] => nat" (infixr 90) |
17 "+" :: "[nat,nat] => nat" (infixr 90) |
17 "<","<=" :: "[nat,nat] => o" (infixr 70) |
18 "<","<=" :: "[nat,nat] => o" (infixr 70) |
18 |
19 |
19 rules |
20 rules |