src/HOL/WF.thy
changeset 1475 7f5a4cd08209
parent 1276 42ccfd3e1fb4
child 1558 9c6ebfab4e05
     1.1 --- a/src/HOL/WF.thy	Mon Feb 05 14:44:09 1996 +0100
     1.2 +++ b/src/HOL/WF.thy	Mon Feb 05 21:27:16 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	HOL/WF.thy
     1.5 +(*  Title:      HOL/wf.ML
     1.6      ID:         $Id$
     1.7 -    Author: 	Tobias Nipkow
     1.8 +    Author:     Tobias Nipkow
     1.9      Copyright   1992  University of Cambridge
    1.10  
    1.11  Well-founded Recursion
    1.12 @@ -8,23 +8,22 @@
    1.13  
    1.14  WF = Trancl +
    1.15  consts
    1.16 -   wf		:: "('a * 'a)set => bool"
    1.17 -   cut		:: "['a => 'b, ('a * 'a)set, 'a] => 'a => 'b"
    1.18 -   wftrec,wfrec	:: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b] => 'b"
    1.19 -   is_recfun	:: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b, 'a=>'b] => bool"
    1.20 -   the_recfun	:: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b] => 'a=>'b"
    1.21 + wf         :: "('a * 'a)set => bool"
    1.22 + cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
    1.23 + is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
    1.24 + the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
    1.25 + wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
    1.26  
    1.27  defs
    1.28    wf_def  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
    1.29    
    1.30 -  cut_def 	 "cut f r x == (%y. if (y,x):r then f y else @z.True)"
    1.31 +  cut_def        "cut f r x == (%y. if (y,x):r then f y else @z.True)"
    1.32  
    1.33 -  is_recfun_def  "is_recfun r a H f == (f = cut (%x.(H x (cut f r x))) r a)"
    1.34 -
    1.35 -  the_recfun_def "the_recfun r a H == (@f.is_recfun r a H f)"
    1.36 +  is_recfun_def  "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"
    1.37  
    1.38 -  wftrec_def     "wftrec r a H == H a (the_recfun r a H)"
    1.39 +  the_recfun_def "the_recfun r H a  == (@f. is_recfun r H a f)"
    1.40  
    1.41 -  (*version not requiring transitivity*)
    1.42 -  wfrec_def	"wfrec r a H == wftrec (trancl r) a (%x f.(H x (cut f r x)))"
    1.43 +  wfrec_def
    1.44 +    "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
    1.45 +                              r x)  x)"
    1.46  end