src/ZF/Constructible/WFrec.thy
changeset 21404 eb85850d3eb7
parent 21233 5a5c8ea5f66a
child 32960 69916a850301
     1.1 --- a/src/ZF/Constructible/WFrec.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/ZF/Constructible/WFrec.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -272,7 +272,7 @@
     1.4  subsection{*Relativization of the ZF Predicate @{term is_recfun}*}
     1.5  
     1.6  definition
     1.7 -  M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
     1.8 +  M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o" where
     1.9     "M_is_recfun(M,MH,r,a,f) == 
    1.10       \<forall>z[M]. z \<in> f <-> 
    1.11              (\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M]. 
    1.12 @@ -280,11 +280,13 @@
    1.13                 pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
    1.14                 xa \<in> r & MH(x, f_r_sx, y))"
    1.15  
    1.16 -  is_wfrec :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
    1.17 +definition
    1.18 +  is_wfrec :: "[i=>o, [i,i,i]=>o, i, i, i] => o" where
    1.19     "is_wfrec(M,MH,r,a,z) == 
    1.20        \<exists>f[M]. M_is_recfun(M,MH,r,a,f) & MH(a,f,z)"
    1.21  
    1.22 -  wfrec_replacement :: "[i=>o, [i,i,i]=>o, i] => o"
    1.23 +definition
    1.24 +  wfrec_replacement :: "[i=>o, [i,i,i]=>o, i] => o" where
    1.25     "wfrec_replacement(M,MH,r) ==
    1.26          strong_replacement(M, 
    1.27               \<lambda>x z. \<exists>y[M]. pair(M,x,y,z) & is_wfrec(M,MH,r,x,y))"