0

1 
(* Title: ZF/nat.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
Natural numbers in ZermeloFraenkel Set Theory


7 
*)


8 


9 
Nat = Ord + Bool +


10 
consts


11 
nat :: "i"


12 
nat_case :: "[i, i, i=>i]=>i"


13 
nat_rec :: "[i, i, [i,i]=>i]=>i"


14 


15 
rules


16 


17 
nat_def "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"


18 


19 
nat_case_def


20 
"nat_case(k,a,b) == THE y. k=0 & y=a  (EX x. k=succ(x) & y=b(x))"


21 


22 
nat_rec_def


23 
"nat_rec(k,a,b) == \


24 
\ wfrec(Memrel(nat), k, %n f. nat_case(n, a, %m. b(m, f`m)))"


25 


26 
end
