(* Title: HOL/Nat.thy
ID: $Id$
Author: Tobias Nipkow, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Definition of types ind and nat.
Type nat is defined as a set Nat over type ind.
*)
Nat = WF +
types
ind
nat
arities
ind, nat :: term
instance
nat :: ord
consts
Zero_Rep :: "ind"
Suc_Rep :: "ind => ind"
Nat :: "ind set"
Rep_Nat :: "nat => ind"
Abs_Nat :: "ind => nat"
Suc :: "nat => nat"
nat_case :: "['a, nat=>'a, nat] =>'a"
pred_nat :: "(nat * nat) set"
nat_rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
"0" :: "nat" ("0")
translations
"case p of 0 => a | Suc(y) => b" == "nat_case(a, %y.b, p)"
rules
(*the axiom of infinity in 2 parts*)
inj_Suc_Rep "inj(Suc_Rep)"
Suc_Rep_not_Zero_Rep "~(Suc_Rep(x) = Zero_Rep)"
Nat_def "Nat == lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"
(*faking a type definition...*)
Rep_Nat "Rep_Nat(n): Nat"
Rep_Nat_inverse "Abs_Nat(Rep_Nat(n)) = n"
Abs_Nat_inverse "i: Nat ==> Rep_Nat(Abs_Nat(i)) = i"
(*defining the abstract constants*)
Zero_def "0 == Abs_Nat(Zero_Rep)"
Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
(*nat operations and recursion*)
nat_case_def "nat_case(a,f,n) == @z. (n=0 --> z=a) \
\ & (!x. n=Suc(x) --> z=f(x))"
pred_nat_def "pred_nat == {p. ? n. p = <n, Suc(n)>}"
less_def "m<n == <m,n>:trancl(pred_nat)"
le_def "m<=(n::nat) == ~(n<m)"
nat_rec_def "nat_rec(n,c,d) == wfrec(pred_nat, n, \
\ nat_case(%g.c, %m g. d(m,g(m))))"
end