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;
wenzelm@17481
     1
(*  Title:      Sequents/LK/Nat.thy
paulson@7091
     2
    ID:         $Id$
paulson@7091
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@7095
     4
    Copyright   1999  University of Cambridge
paulson@7091
     5
*)
paulson@7091
     6
wenzelm@17481
     7
header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
wenzelm@17481
     8
wenzelm@17481
     9
theory Nat
wenzelm@17481
    10
imports LK
wenzelm@17481
    11
begin
wenzelm@17481
    12
wenzelm@17481
    13
typedecl nat
wenzelm@17481
    14
arities nat :: "term"
paulson@7091
    15
consts  "0" :: nat      ("0")
wenzelm@17481
    16
        Suc :: "nat=>nat"
wenzelm@17481
    17
        rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
wenzelm@17481
    18
        "+" :: "[nat, nat] => nat"                (infixl 60)
paulson@7091
    19
wenzelm@17481
    20
axioms
wenzelm@17481
    21
  induct:  "[| $H |- $E, P(0), $F;
paulson@7123
    22
              !!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F"
paulson@7095
    23
wenzelm@17481
    24
  Suc_inject:  "|- Suc(m)=Suc(n) --> m=n"
wenzelm@17481
    25
  Suc_neq_0:   "|- Suc(m) ~= 0"
wenzelm@17481
    26
  rec_0:       "|- rec(0,a,f) = a"
wenzelm@17481
    27
  rec_Suc:     "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
wenzelm@17481
    28
  add_def:     "m+n == rec(m, n, %x y. Suc(y))"
wenzelm@17481
    29
wenzelm@17481
    30
ML {* use_legacy_bindings (the_context ()) *}
wenzelm@17481
    31
paulson@7091
    32
end