0

1 
(* Title: ZF/wf.thy


2 
ID: $Id$


3 
Author: Tobias Nipkow and Lawrence C Paulson


4 
Copyright 1992 University of Cambridge


5 


6 
Wellfounded Recursion


7 
*)


8 


9 
WF = Trancl +


10 
consts


11 
wf :: "i=>o"


12 
wftrec,wfrec :: "[i, i, [i,i]=>i] =>i"


13 
is_recfun :: "[i, i, [i,i]=>i, i] =>o"


14 
the_recfun :: "[i, i, [i,i]=>i] =>i"


15 


16 
rules


17 
(*r is a wellfounded relation*)


18 
wf_def "wf(r) == ALL Z. Z=0  (EX x:Z. ALL y. <y,x>:r > ~ y:Z)"


19 


20 
is_recfun_def "is_recfun(r,a,H,f) == \


21 
\ (f = (lam x: r``{a}. H(x, restrict(f, r``{x}))))"


22 


23 
the_recfun_def "the_recfun(r,a,H) == (THE f.is_recfun(r,a,H,f))"


24 


25 
wftrec_def "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"


26 


27 
(*public version. Does not require r to be transitive*)


28 
wfrec_def "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r``{x})))"


29 


30 
end
