src/Sequents/LK/Nat.thy
 changeset 17481 75166ebb619b parent 7123 4ab38de3fd20 child 21426 87ac12bed1ab
```     1.1 --- a/src/Sequents/LK/Nat.thy	Sun Sep 18 14:25:48 2005 +0200
1.2 +++ b/src/Sequents/LK/Nat.thy	Sun Sep 18 15:20:08 2005 +0200
1.3 @@ -1,26 +1,32 @@
1.4 -(*  Title:      Sequents/LK/Nat
1.5 +(*  Title:      Sequents/LK/Nat.thy
1.6      ID:         \$Id\$
1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.8      Copyright   1999  University of Cambridge
1.9 -
1.10 -Theory of the natural numbers: Peano's axioms, primitive recursion
1.11  *)
1.12
1.13 -Nat = LK +
1.14 -types   nat
1.15 -arities nat :: term
1.16 +header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
1.17 +
1.18 +theory Nat
1.19 +imports LK
1.20 +begin
1.21 +
1.22 +typedecl nat
1.23 +arities nat :: "term"
1.24  consts  "0" :: nat      ("0")
1.25 -        Suc :: nat=>nat
1.26 -        rec :: [nat, 'a, [nat,'a]=>'a] => 'a
1.27 -        "+" :: [nat, nat] => nat                (infixl 60)
1.28 +        Suc :: "nat=>nat"
1.29 +        rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
1.30 +        "+" :: "[nat, nat] => nat"                (infixl 60)
1.31
1.32 -rules
1.33 -  induct  "[| \$H |- \$E, P(0), \$F;
1.34 +axioms
1.35 +  induct:  "[| \$H |- \$E, P(0), \$F;
1.36                !!x. \$H, P(x) |- \$E, P(Suc(x)), \$F |] ==> \$H |- \$E, P(n), \$F"
1.37
1.38 -  Suc_inject  "|- Suc(m)=Suc(n) --> m=n"
1.39 -  Suc_neq_0   "|- Suc(m) ~= 0"
1.40 -  rec_0       "|- rec(0,a,f) = a"
1.41 -  rec_Suc     "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
1.42 -  add_def     "m+n == rec(m, n, %x y. Suc(y))"
1.43 +  Suc_inject:  "|- Suc(m)=Suc(n) --> m=n"
1.44 +  Suc_neq_0:   "|- Suc(m) ~= 0"
1.45 +  rec_0:       "|- rec(0,a,f) = a"
1.46 +  rec_Suc:     "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
1.47 +  add_def:     "m+n == rec(m, n, %x y. Suc(y))"
1.48 +
1.49 +ML {* use_legacy_bindings (the_context ()) *}
1.50 +
1.51  end
```