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