src/FOL/ex/Nat.thy
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 352 fd3ab8bcb69d
permissions -rw-r--r--
Initial revision
     1 (*  Title: 	FOL/ex/nat.thy
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Examples for the manual "Introduction to Isabelle"
     7 
     8 Theory of the natural numbers: Peano's axioms, primitive recursion
     9 
    10 INCOMPATIBLE with nat2.thy, Nipkow's example
    11 *)
    12 
    13 Nat = FOL +
    14 types   nat 0
    15 arities nat         :: term
    16 consts  "0"         :: "nat"    ("0")
    17         Suc         :: "nat=>nat"
    18         rec         :: "[nat, 'a, [nat,'a]=>'a] => 'a"
    19         "+"         :: "[nat, nat] => nat"              (infixl 60)
    20 rules   induct      "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)"
    21         Suc_inject  "Suc(m)=Suc(n) ==> m=n"
    22         Suc_neq_0   "Suc(m)=0      ==> R"
    23         rec_0       "rec(0,a,f) = a"
    24         rec_Suc     "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
    25         add_def     "m+n == rec(m, n, %x y. Suc(y))"
    26 end