1478

1 
(* Title: ZF/Nat.thy

0

2 
ID: $Id$

1478

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

435

4 
Copyright 1994 University of Cambridge

0

5 


6 
Natural numbers in ZermeloFraenkel Set Theory


7 
*)


8 

435

9 
Nat = Ordinal + Bool + "mono" +

0

10 
consts

1478

11 
nat :: i

1401

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


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

0

14 

753

15 
defs

0

16 


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


18 


19 
nat_case_def

1478

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

0

21 


22 
nat_rec_def

1478

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


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

0

25 


26 
end
