author  clasohm 
Mon, 05 Feb 1996 21:27:16 +0100  
changeset 1475  7f5a4cd08209 
parent 1276  42ccfd3e1fb4 
child 1558  9c6ebfab4e05 
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 + 

10 
consts 

1475  11 
wf :: "('a * 'a)set => bool" 
12 
cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" 

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

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

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

923  16 

17 
defs 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
965
diff
changeset

18 
wf_def "wf(r) == (!P. (!x. (!y. (y,x):r > P(y)) > P(x)) > (!x.P(x)))" 
923  19 

1475  20 
cut_def "cut f r x == (%y. if (y,x):r then f y else @z.True)" 
923  21 

1475  22 
is_recfun_def "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)" 
923  23 

1475  24 
the_recfun_def "the_recfun r H a == (@f. is_recfun r H a f)" 
923  25 

1475  26 
wfrec_def 
27 
"wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x) 

28 
r x) x)" 

923  29 
end 