src/FOL/ex/NatClass.thy

UNIV now a constant; UNION1, INTER1 now translations and no longer have
separate rules for themselves

(*  Title:      FOL/ex/NatClass.thy
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

This is an abstract version of Nat.thy. Instead of axiomatizing a
single type "nat" we define the class of all these types (up to
isomorphism).

Note: The "rec" operator had to be made 'monomorphic', because class
axioms may not contain more than one type variable.
*)

NatClass = FOL +

consts
  "0"           :: 'a                                   ("0")
  Suc           :: 'a => 'a  
  rec           :: ['a, 'a, ['a, 'a] => 'a] => 'a  

axclass
  nat < term
  induct        "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
  Suc_inject    "Suc(m) = Suc(n) ==> m = n"
  Suc_neq_0     "Suc(m) = 0 ==> R"
  rec_0         "rec(0, a, f) = a"
  rec_Suc       "rec(Suc(m), a, f) = f(m, rec(m, a, f))"

consts
  "+"           :: "['a::nat, 'a] => 'a"                (infixl 60)

defs
  add_def       "m + n == rec(m, n, %x y. Suc(y))"

end