(*  Title: 	FOL/ex/nat2.thy

     ID:         $Id$

     Author: 	Tobias Nipkow

     Copyright   1994  University of Cambridge

 Theory for examples of simplification and induction on the natural numbers

 *)

 Nat2 = FOL +

 types nat

 arities nat :: term

 consts

  succ,pred :: "nat => nat"

        "0" :: "nat"	("0")

        "+" :: "[nat,nat] => nat" (infixr 90)

   "<","<=" :: "[nat,nat] => o"   (infixr 70)

 rules

  pred_0		"pred(0) = 0"

  pred_succ	"pred(succ(m)) = m"

  plus_0		"0+n = n"

  plus_succ	"succ(m)+n = succ(m+n)"

  nat_distinct1	"~ 0=succ(n)"

  nat_distinct2	"~ succ(m)=0"

  succ_inject	"succ(m)=succ(n) <-> m=n"

  leq_0		"0 <= n"

  leq_succ_succ	"succ(m)<=succ(n) <-> m<=n"

  leq_succ_0	"~ succ(m) <= 0"

  lt_0_succ	"0 < succ(n)"

  lt_succ_succ	"succ(m)<succ(n) <-> m<n"

  lt_0 "~ m < 0"

  nat_ind	"[| P(0); ALL n. P(n)-->P(succ(n)) |] ==> All(P)"

 end