author  lcp 
Tue, 21 Jun 1994 17:20:34 +0200  
changeset 435  ca5356bd315a 
parent 124  858ab9a9b047 
child 753  ec86863e87c8 
permissions  rwrr 
435  1 
(* Title: ZF/Nat.thy 
0  2 
ID: $Id$ 
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 
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 