author  clasohm 
Thu, 16 Sep 1993 12:20:38 +0200  
changeset 0  a5a9c433f639 
child 124  858ab9a9b047 
permissions  rwrr 
0  1 
(* Title: ZF/epsilon.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
Epsilon induction and recursion 

7 
*) 

8 

9 
Epsilon = Nat + 

10 
consts 

11 
eclose,rank :: "i=>i" 

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

13 

14 
rules 

15 
eclose_def "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))" 

16 
transrec_def "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)" 

17 
rank_def "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))" 

18 
end 