src/FOL/ex/Nat.thy
 author clasohm Thu Sep 16 12:20:38 1993 +0200 (1993-09-16) changeset 0 a5a9c433f639 child 352 fd3ab8bcb69d permissions -rw-r--r--
Initial revision
```     1 (*  Title: 	FOL/ex/nat.thy
```
```     2     ID:         \$Id\$
```
```     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1992  University of Cambridge
```
```     5
```
```     6 Examples for the manual "Introduction to Isabelle"
```
```     7
```
```     8 Theory of the natural numbers: Peano's axioms, primitive recursion
```
```     9
```
```    10 INCOMPATIBLE with nat2.thy, Nipkow's example
```
```    11 *)
```
```    12
```
```    13 Nat = FOL +
```
```    14 types   nat 0
```
```    15 arities nat         :: term
```
```    16 consts  "0"         :: "nat"    ("0")
```
```    17         Suc         :: "nat=>nat"
```
```    18         rec         :: "[nat, 'a, [nat,'a]=>'a] => 'a"
```
```    19         "+"         :: "[nat, nat] => nat"              (infixl 60)
```
```    20 rules   induct      "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)"
```
```    21         Suc_inject  "Suc(m)=Suc(n) ==> m=n"
```
```    22         Suc_neq_0   "Suc(m)=0      ==> R"
```
```    23         rec_0       "rec(0,a,f) = a"
```
```    24         rec_Suc     "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
```
```    25         add_def     "m+n == rec(m, n, %x y. Suc(y))"
```
```    26 end
```