author  clasohm 
Tue, 16 Nov 1993 14:24:21 +0100  
changeset 124  858ab9a9b047 
parent 6  8ce8c4d13d4d 
child 435  ca5356bd315a 
permissions  rwrr 
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 

124  9 
Nat = Ord + Bool + "mono" + 
0  10 
consts 
11 
nat :: "i" 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

12 
nat_case :: "[i, i=>i, i]=>i" 
0  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 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

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 

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

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

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

26 
end 