src/FOL/ex/Nat2.thy
author wenzelm
Sun, 26 Nov 2006 23:43:53 +0100
changeset 21539 c5cf9243ad62
parent 17245 1c519a3cca59
permissions -rw-r--r--
converted legacy ML scripts;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1473
e8d4606e6502 expanded tabs
clasohm
parents: 1322
diff changeset
     1
(*  Title:      FOL/ex/nat2.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1473
e8d4606e6502 expanded tabs
clasohm
parents: 1322
diff changeset
     3
    Author:     Tobias Nipkow
352
fd3ab8bcb69d removal of obsolete type-declaration syntax
lcp
parents: 0
diff changeset
     4
    Copyright   1994  University of Cambridge
0
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: 1473
diff changeset
     7
header {* Theory for examples of simplification and induction on the natural numbers *}
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
17245
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
     9
theory Nat2
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    10
imports FOL
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    11
begin
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    12
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    13
typedecl nat
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    14
arities nat :: "term"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
352
fd3ab8bcb69d removal of obsolete type-declaration syntax
lcp
parents: 0
diff changeset
    16
consts
17245
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    17
  succ :: "nat => nat"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    18
  pred :: "nat => nat"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    19
  0 :: nat    ("0")
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    20
  add :: "[nat,nat] => nat"    (infixr "+" 90)
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    21
  lt :: "[nat,nat] => o"    (infixr "<" 70)
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    22
  leq :: "[nat,nat] => o"    (infixr "<=" 70)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
17245
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    24
axioms
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    25
 pred_0:         "pred(0) = 0"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    26
 pred_succ:      "pred(succ(m)) = m"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
17245
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    28
 plus_0:         "0+n = n"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    29
 plus_succ:      "succ(m)+n = succ(m+n)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
17245
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    31
 nat_distinct1:  "~ 0=succ(n)"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    32
 nat_distinct2:  "~ succ(m)=0"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    33
 succ_inject:    "succ(m)=succ(n) <-> m=n"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    34
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    35
 leq_0:          "0 <= n"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    36
 leq_succ_succ:  "succ(m)<=succ(n) <-> m<=n"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    37
 leq_succ_0:     "~ succ(m) <= 0"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
17245
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    39
 lt_0_succ:      "0 < succ(n)"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    40
 lt_succ_succ:   "succ(m)<succ(n) <-> m<n"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    41
 lt_0:           "~ m < 0"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
17245
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    43
 nat_ind:        "[| P(0); ALL n. P(n)-->P(succ(n)) |] ==> All(P)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
17245
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    45
ML {* use_legacy_bindings (the_context ()) *}
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    46
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
end