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