src/HOL/WF.thy
changeset 1558 9c6ebfab4e05
parent 1475 7f5a4cd08209
child 3320 3a5e4930fb77
     1.1 --- a/src/HOL/WF.thy	Wed Mar 06 14:19:39 1996 +0100
     1.2 +++ b/src/HOL/WF.thy	Fri Mar 08 13:11:09 1996 +0100
     1.3 @@ -7,23 +7,22 @@
     1.4  *)
     1.5  
     1.6  WF = Trancl +
     1.7 -consts
     1.8 - wf         :: "('a * 'a)set => bool"
     1.9 - cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
    1.10 - is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
    1.11 - the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
    1.12 - wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
    1.13 +
    1.14 +constdefs
    1.15 +  wf         :: "('a * 'a)set => bool"
    1.16 +  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
    1.17 +
    1.18 +  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
    1.19 +  "cut f r x == (%y. if (y,x):r then f y else @z.True)"
    1.20  
    1.21 -defs
    1.22 -  wf_def  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
    1.23 -  
    1.24 -  cut_def        "cut f r x == (%y. if (y,x):r then f y else @z.True)"
    1.25 +  is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
    1.26 +  "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"
    1.27  
    1.28 -  is_recfun_def  "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"
    1.29 +  the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
    1.30 +  "the_recfun r H a  == (@f. is_recfun r H a f)"
    1.31  
    1.32 -  the_recfun_def "the_recfun r H a  == (@f. is_recfun r H a f)"
    1.33 +  wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
    1.34 +  "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
    1.35 +                            r x)  x)"
    1.36  
    1.37 -  wfrec_def
    1.38 -    "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
    1.39 -                              r x)  x)"
    1.40  end