src/FOL/ex/Nat2.thy
changeset 22822 c1a6a2159e69
parent 22821 15b2e7ec1f3b
child 22823 fa9ff469247f
     1.1 --- a/src/FOL/ex/Nat2.thy	Fri Apr 27 14:21:23 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,47 +0,0 @@
     1.4 -(*  Title:      FOL/ex/nat2.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Tobias Nipkow
     1.7 -    Copyright   1994  University of Cambridge
     1.8 -*)
     1.9 -
    1.10 -header {* Theory for examples of simplification and induction on the natural numbers *}
    1.11 -
    1.12 -theory Nat2
    1.13 -imports FOL
    1.14 -begin
    1.15 -
    1.16 -typedecl nat
    1.17 -arities nat :: "term"
    1.18 -
    1.19 -consts
    1.20 -  succ :: "nat => nat"
    1.21 -  pred :: "nat => nat"
    1.22 -  0 :: nat    ("0")
    1.23 -  add :: "[nat,nat] => nat"    (infixr "+" 90)
    1.24 -  lt :: "[nat,nat] => o"    (infixr "<" 70)
    1.25 -  leq :: "[nat,nat] => o"    (infixr "<=" 70)
    1.26 -
    1.27 -axioms
    1.28 - pred_0:         "pred(0) = 0"
    1.29 - pred_succ:      "pred(succ(m)) = m"
    1.30 -
    1.31 - plus_0:         "0+n = n"
    1.32 - plus_succ:      "succ(m)+n = succ(m+n)"
    1.33 -
    1.34 - nat_distinct1:  "~ 0=succ(n)"
    1.35 - nat_distinct2:  "~ succ(m)=0"
    1.36 - succ_inject:    "succ(m)=succ(n) <-> m=n"
    1.37 -
    1.38 - leq_0:          "0 <= n"
    1.39 - leq_succ_succ:  "succ(m)<=succ(n) <-> m<=n"
    1.40 - leq_succ_0:     "~ succ(m) <= 0"
    1.41 -
    1.42 - lt_0_succ:      "0 < succ(n)"
    1.43 - lt_succ_succ:   "succ(m)<succ(n) <-> m<n"
    1.44 - lt_0:           "~ m < 0"
    1.45 -
    1.46 - nat_ind:        "[| P(0); ALL n. P(n)-->P(succ(n)) |] ==> All(P)"
    1.47 -
    1.48 -ML {* use_legacy_bindings (the_context ()) *}
    1.49 -
    1.50 -end