equal
deleted
inserted
replaced
|
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 |