1475

1 
(* Title: HOL/wf.ML

923

2 
ID: $Id$

1475

3 
Author: Tobias Nipkow

923

4 
Copyright 1992 University of Cambridge


5 


6 
Wellfounded Recursion


7 
*)


8 


9 
WF = Trancl +

1558

10 


11 
constdefs


12 
wf :: "('a * 'a)set => bool"


13 
"wf(r) == (!P. (!x. (!y. (y,x):r > P(y)) > P(x)) > (!x.P(x)))"


14 


15 
cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"


16 
"cut f r x == (%y. if (y,x):r then f y else @z.True)"

923

17 

1558

18 
is_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"


19 
"is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"

923

20 

1558

21 
the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"


22 
"the_recfun r H a == (@f. is_recfun r H a f)"

923

23 

1558

24 
wfrec :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"


25 
"wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)


26 
r x) x)"

923

27 


28 
end
