src/FOL/ex/Nat.thy
author wenzelm
Sat, 03 Sep 2005 17:15:51 +0200
changeset 17245 1c519a3cca59
parent 3115 24ed05500380
child 19819 14de4d05d275
permissions -rw-r--r--
converted to Isar theory format;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3115
24ed05500380 tuned comments;
wenzelm
parents: 1473
diff changeset
     1
(*  Title:      FOL/ex/Nat.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1473
e8d4606e6502 expanded tabs
clasohm
parents: 1322
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
17245
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
     7
header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
     8
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
     9
theory Nat
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    10
imports FOL
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    11
begin
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    12
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    13
typedecl nat
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    14
arities nat :: "term"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    15
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    16
consts
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    17
  0 :: nat    ("0")
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    18
  Suc :: "nat => nat"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    19
  rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    20
  add :: "[nat, nat] => nat"    (infixl "+" 60)
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    21
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    22
axioms
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    23
  induct:      "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    24
  Suc_inject:  "Suc(m)=Suc(n) ==> m=n"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    25
  Suc_neq_0:   "Suc(m)=0      ==> R"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    26
  rec_0:       "rec(0,a,f) = a"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    27
  rec_Suc:     "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    28
  add_def:     "m+n == rec(m, n, %x y. Suc(y))"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    29
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    30
ML {* use_legacy_bindings (the_context ()) *}
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 3115
diff changeset
    31
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
end