author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 8882  9df44a4f1bf7 
permissions  rwrr 
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" 

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

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

15 
acyclic :: "('a*'a)set => bool" 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

16 
"acyclic r == !x. (x,x) ~: r^+" 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

17 

1558  18 
cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" 
3320  19 
"cut f r x == (%y. if (y,x):r then f y else arbitrary)" 
923  20 

1558  21 
is_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool" 
22 
"is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)" 

923  23 

1558  24 
the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b" 
25 
"the_recfun r H a == (@f. is_recfun r H a f)" 

923  26 

1558  27 
wfrec :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b" 
28 
"wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x) 

29 
r x) x)" 

923  30 

31 
end 