src/HOL/Recdef.thy
changeset 35416 d8d7d1b785af
parent 32462 c33faa289520
child 37767 a2b7a20d6ea3
     1.1 --- a/src/HOL/Recdef.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Recdef.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -27,15 +27,17 @@
     1.4    wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
     1.5              wfrec_rel R F x (F g x)"
     1.6  
     1.7 -constdefs
     1.8 -  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
     1.9 +definition
    1.10 +  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" where
    1.11    "cut f r x == (%y. if (y,x):r then f y else undefined)"
    1.12  
    1.13 -  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
    1.14 +definition
    1.15 +  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" where
    1.16    "adm_wf R F == ALL f g x.
    1.17       (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
    1.18  
    1.19 -  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
    1.20 +definition
    1.21 +  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where
    1.22    [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    1.23  
    1.24  subsection{*Well-Founded Recursion*}