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 

124

9 
Epsilon = Nat + "mono" +

0

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
