1 (* Title: FOL/ex/Nat.thy |
1 (* Title: Sequents/LK/Nat |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1992 University of Cambridge |
4 Copyright 1999 University of Cambridge |
5 |
|
6 Examples for the manuals. |
|
7 |
5 |
8 Theory of the natural numbers: Peano's axioms, primitive recursion |
6 Theory of the natural numbers: Peano's axioms, primitive recursion |
9 *) |
7 *) |
10 |
8 |
11 Nat = LK + |
9 Nat = LK + |
15 Suc :: nat=>nat |
13 Suc :: nat=>nat |
16 rec :: [nat, 'a, [nat,'a]=>'a] => 'a |
14 rec :: [nat, 'a, [nat,'a]=>'a] => 'a |
17 "+" :: [nat, nat] => nat (infixl 60) |
15 "+" :: [nat, nat] => nat (infixl 60) |
18 |
16 |
19 rules |
17 rules |
20 induct "[| $H |- $E, P(0), $F; |
18 induct "[| $H |- $E, P(0), $F; |
21 !!x. $H |- $E, P(x) --> P(Suc(x)), $F |] ==> $H |- $E, P(n), $F" |
19 !!x. $H |- $E, P(x) --> P(Suc(x)), $F |] ==> $H |- $E, P(n), $F" |
|
20 |
22 Suc_inject "|- Suc(m)=Suc(n) --> m=n" |
21 Suc_inject "|- Suc(m)=Suc(n) --> m=n" |
23 Suc_neq_0 "|- Suc(m) ~= 0" |
22 Suc_neq_0 "|- Suc(m) ~= 0" |
24 rec_0 "|- rec(0,a,f) = a" |
23 rec_0 "|- rec(0,a,f) = a" |
25 rec_Suc "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))" |
24 rec_Suc "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))" |
26 add_def "m+n == rec(m, n, %x y. Suc(y))" |
25 add_def "m+n == rec(m, n, %x y. Suc(y))" |