src/Sequents/LK/Nat.thy
author wenzelm
Sun Sep 18 15:20:08 2005 +0200 (2005-09-18)
changeset 17481 75166ebb619b
parent 7123 4ab38de3fd20
child 21426 87ac12bed1ab
permissions -rw-r--r--
converted to Isar theory format;
     1 (*  Title:      Sequents/LK/Nat.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1999  University of Cambridge
     5 *)
     6 
     7 header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
     8 
     9 theory Nat
    10 imports LK
    11 begin
    12 
    13 typedecl nat
    14 arities nat :: "term"
    15 consts  "0" :: nat      ("0")
    16         Suc :: "nat=>nat"
    17         rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
    18         "+" :: "[nat, nat] => nat"                (infixl 60)
    19 
    20 axioms
    21   induct:  "[| $H |- $E, P(0), $F;
    22               !!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F"
    23 
    24   Suc_inject:  "|- Suc(m)=Suc(n) --> m=n"
    25   Suc_neq_0:   "|- Suc(m) ~= 0"
    26   rec_0:       "|- rec(0,a,f) = a"
    27   rec_Suc:     "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
    28   add_def:     "m+n == rec(m, n, %x y. Suc(y))"
    29 
    30 ML {* use_legacy_bindings (the_context ()) *}
    31 
    32 end