src/ZF/Constructible/WF_absolute.thy
changeset 13268 240509babf00
parent 13254 5146ccaedf42
child 13269 3ba9be497c33
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Mon Jul 01 18:10:53 2002 +0200
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Mon Jul 01 18:16:18 2002 +0200
     1.3 @@ -1,5 +1,20 @@
     1.4  theory WF_absolute = WFrec:
     1.5  
     1.6 +(*????move to Wellorderings.thy*)
     1.7 +lemma (in M_axioms) wellfounded_on_field_imp_wellfounded:
     1.8 +     "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)"
     1.9 +by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast)
    1.10 +
    1.11 +lemma (in M_axioms) wellfounded_iff_wellfounded_on_field:
    1.12 +     "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)"
    1.13 +by (blast intro: wellfounded_imp_wellfounded_on
    1.14 +                 wellfounded_on_field_imp_wellfounded)
    1.15 +
    1.16 +lemma (in M_axioms) wellfounded_on_subset_A:
    1.17 +     "[| wellfounded_on(M,A,r);  B<=A |] ==> wellfounded_on(M,B,r)"
    1.18 +by (simp add: wellfounded_on_def, blast)
    1.19 +
    1.20 +
    1.21  subsection{*Every well-founded relation is a subset of some inverse image of
    1.22        an ordinal*}
    1.23  
    1.24 @@ -127,7 +142,7 @@
    1.25  
    1.26    tran_closure :: "[i=>o,i,i] => o"
    1.27      "tran_closure(M,r,t) ==
    1.28 -         \<exists>s. M(s) & rtran_closure(M,r,s) & composition(M,r,s,t)"
    1.29 +         \<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)"
    1.30  
    1.31  
    1.32  locale M_trancl = M_axioms +
    1.33 @@ -135,11 +150,14 @@
    1.34    assumes rtrancl_separation:
    1.35       "[| M(r); M(A) |] ==>
    1.36  	separation
    1.37 -	   (M, \<lambda>p. \<exists>n\<in>nat. \<exists>f \<in> succ(n) -> A.
    1.38 -                    (\<exists>x y. p = <x,y> &  f`0 = x & f`n = y) &
    1.39 -                          (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r))"
    1.40 +	   (M, \<lambda>p. \<exists>n[M]. n\<in>nat & 
    1.41 +                    (\<exists>f[M]. 
    1.42 +                     f \<in> succ(n) -> A &
    1.43 +                     (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) &  
    1.44 +                           f`0 = x & f`n = y) &
    1.45 +                           (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)))"
    1.46        and wellfounded_trancl_separation:
    1.47 -     "[| M(r); M(Z) |] ==> separation (M, \<lambda>x. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z)"
    1.48 +     "[| M(r); M(Z) |] ==> separation (M, \<lambda>x. \<exists>w[M]. w \<in> Z & \<langle>w,x\<rangle> \<in> r^+)"
    1.49  
    1.50  
    1.51  lemma (in M_trancl) rtran_closure_rtrancl:
    1.52 @@ -165,7 +183,7 @@
    1.53  apply (insert rtrancl_separation [of r "field(r)"])
    1.54  apply (simp add: rtrancl_alt_eq_rtrancl [symmetric]
    1.55                   rtrancl_alt_def field_closed typed_apply_abs apply_closed
    1.56 -                 Ord_succ_mem_iff M_nat
    1.57 +                 Ord_succ_mem_iff M_nat nat_into_M
    1.58                   nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype)
    1.59  done
    1.60  
    1.61 @@ -215,11 +233,10 @@
    1.62  apply (simp add: wellfounded_on_def)
    1.63  apply (safe intro!: equalityI)
    1.64  apply (rename_tac Z x)
    1.65 -apply (subgoal_tac "M({x\<in>A. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z})")
    1.66 +apply (subgoal_tac "M({x\<in>A. \<exists>w[M]. w \<in> Z & \<langle>w,x\<rangle> \<in> r^+})")
    1.67   prefer 2
    1.68 - apply (simp add: wellfounded_trancl_separation)
    1.69 -apply (drule_tac x = "{x\<in>A. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z}" in spec)
    1.70 -apply safe
    1.71 + apply (blast intro: wellfounded_trancl_separation) 
    1.72 +apply (drule_tac x = "{x\<in>A. \<exists>w[M]. w \<in> Z & \<langle>w,x\<rangle> \<in> r^+}" in spec, safe)
    1.73  apply (blast dest: transM, simp)
    1.74  apply (rename_tac y w)
    1.75  apply (drule_tac x=w in bspec, assumption, clarify)
    1.76 @@ -228,22 +245,6 @@
    1.77   apply blast
    1.78  done
    1.79  
    1.80 -(*????move to Wellorderings.thy*)
    1.81 -lemma (in M_axioms) wellfounded_on_field_imp_wellfounded:
    1.82 -     "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)"
    1.83 -by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast)
    1.84 -
    1.85 -lemma (in M_axioms) wellfounded_iff_wellfounded_on_field:
    1.86 -     "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)"
    1.87 -by (blast intro: wellfounded_imp_wellfounded_on
    1.88 -                 wellfounded_on_field_imp_wellfounded)
    1.89 -
    1.90 -lemma (in M_axioms) wellfounded_on_subset_A:
    1.91 -     "[| wellfounded_on(M,A,r);  B<=A |] ==> wellfounded_on(M,B,r)"
    1.92 -by (simp add: wellfounded_on_def, blast)
    1.93 -
    1.94 -
    1.95 -
    1.96  lemma (in M_trancl) wellfounded_trancl:
    1.97       "[|wellfounded(M,r); M(r)|] ==> wellfounded(M,r^+)"
    1.98  apply (rotate_tac -1)
    1.99 @@ -259,14 +260,14 @@
   1.100  
   1.101  
   1.102  (*NEEDS RELATIVIZATION*)
   1.103 -locale M_recursion = M_trancl +
   1.104 +locale M_wfrank = M_trancl +
   1.105    assumes wfrank_separation':
   1.106       "M(r) ==>
   1.107  	separation
   1.108 -	   (M, \<lambda>x. ~ (\<exists>f. M(f) & is_recfun(r^+, x, %x f. range(f), f)))"
   1.109 +	   (M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r^+, x, %x f. range(f), f)))"
   1.110   and wfrank_strong_replacement':
   1.111       "M(r) ==>
   1.112 -      strong_replacement(M, \<lambda>x z. \<exists>y f. M(y) & M(f) &
   1.113 +      strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>f[M]. 
   1.114  		  pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) &
   1.115  		  y = range(f))"
   1.116   and Ord_wfrank_separation:
   1.117 @@ -279,13 +280,13 @@
   1.118  constdefs
   1.119   wellfoundedrank :: "[i=>o,i,i] => i"
   1.120      "wellfoundedrank(M,r,A) ==
   1.121 -        {p. x\<in>A, \<exists>y f. M(y) & M(f) &
   1.122 +        {p. x\<in>A, \<exists>y[M]. \<exists>f[M]. 
   1.123                         p = <x,y> & is_recfun(r^+, x, %x f. range(f), f) &
   1.124                         y = range(f)}"
   1.125  
   1.126 -lemma (in M_recursion) exists_wfrank:
   1.127 +lemma (in M_wfrank) exists_wfrank:
   1.128      "[| wellfounded(M,r); M(a); M(r) |]
   1.129 -     ==> \<exists>f. M(f) & is_recfun(r^+, a, %x f. range(f), f)"
   1.130 +     ==> \<exists>f[M]. is_recfun(r^+, a, %x f. range(f), f)"
   1.131  apply (rule wellfounded_exists_is_recfun)
   1.132        apply (blast intro: wellfounded_trancl)
   1.133       apply (rule trans_trancl)
   1.134 @@ -294,7 +295,7 @@
   1.135  apply (simp_all add: trancl_subset_times)
   1.136  done
   1.137  
   1.138 -lemma (in M_recursion) M_wellfoundedrank:
   1.139 +lemma (in M_wfrank) M_wellfoundedrank:
   1.140      "[| wellfounded(M,r); M(r); M(A) |] ==> M(wellfoundedrank(M,r,A))"
   1.141  apply (insert wfrank_strong_replacement' [of r])
   1.142  apply (simp add: wellfoundedrank_def)
   1.143 @@ -306,7 +307,7 @@
   1.144   apply (simp add: trancl_subset_times, blast)
   1.145  done
   1.146  
   1.147 -lemma (in M_recursion) Ord_wfrank_range [rule_format]:
   1.148 +lemma (in M_wfrank) Ord_wfrank_range [rule_format]:
   1.149      "[| wellfounded(M,r); a\<in>A; M(r); M(A) |]
   1.150       ==> \<forall>f. M(f) --> is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))"
   1.151  apply (drule wellfounded_trancl, assumption)
   1.152 @@ -337,7 +338,7 @@
   1.153  apply (blast dest: pair_components_in_M)
   1.154  done
   1.155  
   1.156 -lemma (in M_recursion) Ord_range_wellfoundedrank:
   1.157 +lemma (in M_wfrank) Ord_range_wellfoundedrank:
   1.158      "[| wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A) |]
   1.159       ==> Ord (range(wellfoundedrank(M,r,A)))"
   1.160  apply (frule wellfounded_trancl, assumption)
   1.161 @@ -349,23 +350,23 @@
   1.162   apply (blast intro: Ord_wfrank_range)
   1.163  txt{*We still must show that the range is a transitive set.*}
   1.164  apply (simp add: Transset_def, clarify, simp)
   1.165 -apply (rename_tac x i f u)
   1.166 +apply (rename_tac x f i u)
   1.167  apply (frule is_recfun_imp_in_r, assumption)
   1.168  apply (subgoal_tac "M(u) & M(i) & M(x)")
   1.169   prefer 2 apply (blast dest: transM, clarify)
   1.170  apply (rule_tac a=u in rangeI)
   1.171  apply (rule ReplaceI)
   1.172 -  apply (rule_tac x=i in exI, simp)
   1.173 -  apply (rule_tac x="restrict(f, r^+ -`` {u})" in exI)
   1.174 -  apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2)
   1.175 - apply blast
   1.176 +  apply (rule_tac x=i in rexI, simp)
   1.177 +   apply (rule_tac x="restrict(f, r^+ -`` {u})" in rexI)
   1.178 +    apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2)
   1.179 +   apply (simp, simp, blast) 
   1.180  txt{*Unicity requirement of Replacement*}
   1.181  apply clarify
   1.182  apply (frule apply_recfun2, assumption)
   1.183  apply (simp add: trans_trancl is_recfun_cut)+
   1.184  done
   1.185  
   1.186 -lemma (in M_recursion) function_wellfoundedrank:
   1.187 +lemma (in M_wfrank) function_wellfoundedrank:
   1.188      "[| wellfounded(M,r); M(r); M(A)|]
   1.189       ==> function(wellfoundedrank(M,r,A))"
   1.190  apply (simp add: wellfoundedrank_def function_def, clarify)
   1.191 @@ -375,7 +376,7 @@
   1.192      apply (simp_all add: trancl_subset_times trans_trancl)
   1.193  done
   1.194  
   1.195 -lemma (in M_recursion) domain_wellfoundedrank:
   1.196 +lemma (in M_wfrank) domain_wellfoundedrank:
   1.197      "[| wellfounded(M,r); M(r); M(A)|]
   1.198       ==> domain(wellfoundedrank(M,r,A)) = A"
   1.199  apply (simp add: wellfoundedrank_def function_def)
   1.200 @@ -384,9 +385,9 @@
   1.201  apply (frule_tac a=x in exists_wfrank, assumption+, clarify)
   1.202  apply (rule domainI)
   1.203  apply (rule ReplaceI)
   1.204 -  apply (rule_tac x="range(f)" in exI)
   1.205 +  apply (rule_tac x="range(f)" in rexI)
   1.206    apply simp
   1.207 -  apply (rule_tac x=f in exI, blast, assumption)
   1.208 +  apply (rule_tac x=f in rexI, blast, simp_all)
   1.209  txt{*Uniqueness (for Replacement): repeated above!*}
   1.210  apply clarify
   1.211  apply (drule is_recfun_functional, assumption)
   1.212 @@ -394,7 +395,7 @@
   1.213      apply (simp_all add: trancl_subset_times trans_trancl)
   1.214  done
   1.215  
   1.216 -lemma (in M_recursion) wellfoundedrank_type:
   1.217 +lemma (in M_wfrank) wellfoundedrank_type:
   1.218      "[| wellfounded(M,r);  M(r); M(A)|]
   1.219       ==> wellfoundedrank(M,r,A) \<in> A -> range(wellfoundedrank(M,r,A))"
   1.220  apply (frule function_wellfoundedrank [of r A], assumption+)
   1.221 @@ -404,13 +405,13 @@
   1.222  apply (simp add: domain_wellfoundedrank)
   1.223  done
   1.224  
   1.225 -lemma (in M_recursion) Ord_wellfoundedrank:
   1.226 +lemma (in M_wfrank) Ord_wellfoundedrank:
   1.227      "[| wellfounded(M,r); a \<in> A; r \<subseteq> A*A;  M(r); M(A) |]
   1.228       ==> Ord(wellfoundedrank(M,r,A) ` a)"
   1.229  by (blast intro: apply_funtype [OF wellfoundedrank_type]
   1.230                   Ord_in_Ord [OF Ord_range_wellfoundedrank])
   1.231  
   1.232 -lemma (in M_recursion) wellfoundedrank_eq:
   1.233 +lemma (in M_wfrank) wellfoundedrank_eq:
   1.234       "[| is_recfun(r^+, a, %x. range, f);
   1.235           wellfounded(M,r);  a \<in> A; M(f); M(r); M(A)|]
   1.236        ==> wellfoundedrank(M,r,A) ` a = range(f)"
   1.237 @@ -418,9 +419,9 @@
   1.238   prefer 2 apply (blast intro: wellfoundedrank_type)
   1.239  apply (simp add: wellfoundedrank_def)
   1.240  apply (rule ReplaceI)
   1.241 -  apply (rule_tac x="range(f)" in exI)
   1.242 +  apply (rule_tac x="range(f)" in rexI) 
   1.243    apply blast
   1.244 - apply assumption
   1.245 + apply simp_all
   1.246  txt{*Unicity requirement of Replacement*}
   1.247  apply clarify
   1.248  apply (drule is_recfun_functional, assumption)
   1.249 @@ -429,7 +430,7 @@
   1.250  done
   1.251  
   1.252  
   1.253 -lemma (in M_recursion) wellfoundedrank_lt:
   1.254 +lemma (in M_wfrank) wellfoundedrank_lt:
   1.255       "[| <a,b> \<in> r;
   1.256           wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A)|]
   1.257        ==> wellfoundedrank(M,r,A) ` a < wellfoundedrank(M,r,A) ` b"
   1.258 @@ -454,7 +455,7 @@
   1.259  done
   1.260  
   1.261  
   1.262 -lemma (in M_recursion) wellfounded_imp_subset_rvimage:
   1.263 +lemma (in M_wfrank) wellfounded_imp_subset_rvimage:
   1.264       "[|wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|]
   1.265        ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
   1.266  apply (rule_tac x="range(wellfoundedrank(M,r,A))" in exI)
   1.267 @@ -465,12 +466,12 @@
   1.268  apply (blast intro: apply_rangeI wellfoundedrank_type)
   1.269  done
   1.270  
   1.271 -lemma (in M_recursion) wellfounded_imp_wf:
   1.272 +lemma (in M_wfrank) wellfounded_imp_wf:
   1.273       "[|wellfounded(M,r); relation(r); M(r)|] ==> wf(r)"
   1.274  by (blast dest!: relation_field_times_field wellfounded_imp_subset_rvimage
   1.275            intro: wf_rvimage_Ord [THEN wf_subset])
   1.276  
   1.277 -lemma (in M_recursion) wellfounded_on_imp_wf_on:
   1.278 +lemma (in M_wfrank) wellfounded_on_imp_wf_on:
   1.279       "[|wellfounded_on(M,A,r); relation(r); M(r); M(A)|] ==> wf[A](r)"
   1.280  apply (simp add: wellfounded_on_iff_wellfounded wf_on_def)
   1.281  apply (rule wellfounded_imp_wf)
   1.282 @@ -478,11 +479,11 @@
   1.283  done
   1.284  
   1.285  
   1.286 -theorem (in M_recursion) wf_abs [simp]:
   1.287 +theorem (in M_wfrank) wf_abs [simp]:
   1.288       "[|relation(r); M(r)|] ==> wellfounded(M,r) <-> wf(r)"
   1.289  by (blast intro: wellfounded_imp_wf wf_imp_relativized)
   1.290  
   1.291 -theorem (in M_recursion) wf_on_abs [simp]:
   1.292 +theorem (in M_wfrank) wf_on_abs [simp]:
   1.293       "[|relation(r); M(r); M(A)|] ==> wellfounded_on(M,A,r) <-> wf[A](r)"
   1.294  by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized)
   1.295  
   1.296 @@ -493,20 +494,20 @@
   1.297  
   1.298  lemma (in M_trancl) wfrec_relativize:
   1.299    "[|wf(r); M(a); M(r);  
   1.300 -     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   1.301 +     strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
   1.302            pair(M,x,y,z) & 
   1.303            is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & 
   1.304            y = H(x, restrict(g, r -`` {x}))); 
   1.305       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.306     ==> wfrec(r,a,H) = z <-> 
   1.307 -       (\<exists>f. M(f) & is_recfun(r^+, a, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) & 
   1.308 +       (\<exists>f[M]. is_recfun(r^+, a, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) & 
   1.309              z = H(a,restrict(f,r-``{a})))"
   1.310  apply (frule wf_trancl) 
   1.311  apply (simp add: wftrec_def wfrec_def, safe)
   1.312   apply (frule wf_exists_is_recfun 
   1.313                [of concl: "r^+" a "\<lambda>x f. H(x, restrict(f, r -`` {x}))"]) 
   1.314        apply (simp_all add: trans_trancl function_restrictI trancl_subset_times)
   1.315 - apply (clarify, rule_tac x=f in exI) 
   1.316 + apply (clarify, rule_tac x=x in rexI) 
   1.317   apply (simp_all add: the_recfun_eq trans_trancl trancl_subset_times)
   1.318  done
   1.319  
   1.320 @@ -516,10 +517,10 @@
   1.321        before we can replace @{term "r^+"} by @{term r}. *}
   1.322  theorem (in M_trancl) trans_wfrec_relativize:
   1.323    "[|wf(r);  trans(r);  relation(r);  M(r);  M(a);
   1.324 -     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   1.325 +     strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
   1.326                  pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
   1.327       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.328 -   ==> wfrec(r,a,H) = z <-> (\<exists>f. M(f) & is_recfun(r,a,H,f) & z = H(a,f))" 
   1.329 +   ==> wfrec(r,a,H) = z <-> (\<exists>f[M]. is_recfun(r,a,H,f) & z = H(a,f))" 
   1.330  by (simp cong: is_recfun_cong
   1.331           add: wfrec_relativize trancl_eq_r
   1.332                 is_recfun_restrict_idem domain_restrict_idem)
   1.333 @@ -527,11 +528,11 @@
   1.334  
   1.335  lemma (in M_trancl) trans_eq_pair_wfrec_iff:
   1.336    "[|wf(r);  trans(r); relation(r); M(r);  M(y); 
   1.337 -     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   1.338 +     strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
   1.339                  pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
   1.340       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.341     ==> y = <x, wfrec(r, x, H)> <-> 
   1.342 -       (\<exists>f. M(f) & is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
   1.343 +       (\<exists>f[M]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
   1.344  apply safe  
   1.345   apply (simp add: trans_wfrec_relativize [THEN iff_sym]) 
   1.346  txt{*converse direction*}
   1.347 @@ -543,7 +544,7 @@
   1.348  subsection{*M is closed under well-founded recursion*}
   1.349  
   1.350  text{*Lemma with the awkward premise mentioning @{text wfrec}.*}
   1.351 -lemma (in M_recursion) wfrec_closed_lemma [rule_format]:
   1.352 +lemma (in M_wfrank) wfrec_closed_lemma [rule_format]:
   1.353       "[|wf(r); M(r); 
   1.354          strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
   1.355          \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   1.356 @@ -557,20 +558,20 @@
   1.357  done
   1.358  
   1.359  text{*Eliminates one instance of replacement.*}
   1.360 -lemma (in M_recursion) wfrec_replacement_iff:
   1.361 -     "strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   1.362 +lemma (in M_wfrank) wfrec_replacement_iff:
   1.363 +     "strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M]. 
   1.364                  pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)) <->
   1.365        strong_replacement(M, 
   1.366 -           \<lambda>x y. \<exists>f. M(f) & is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
   1.367 +           \<lambda>x y. \<exists>f[M]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
   1.368  apply simp 
   1.369  apply (rule strong_replacement_cong, blast) 
   1.370  done
   1.371  
   1.372  text{*Useful version for transitive relations*}
   1.373 -theorem (in M_recursion) trans_wfrec_closed:
   1.374 +theorem (in M_wfrank) trans_wfrec_closed:
   1.375       "[|wf(r); trans(r); relation(r); M(r); M(a);
   1.376          strong_replacement(M, 
   1.377 -             \<lambda>x z. \<exists>y g. M(y) & M(g) &
   1.378 +             \<lambda>x z. \<exists>y[M]. \<exists>g[M].
   1.379                      pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
   1.380          \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   1.381        ==> M(wfrec(r,a,H))"
   1.382 @@ -582,13 +583,13 @@
   1.383  section{*Absoluteness without assuming transitivity*}
   1.384  lemma (in M_trancl) eq_pair_wfrec_iff:
   1.385    "[|wf(r);  M(r);  M(y); 
   1.386 -     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   1.387 +     strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
   1.388            pair(M,x,y,z) & 
   1.389            is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & 
   1.390            y = H(x, restrict(g, r -`` {x}))); 
   1.391       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.392     ==> y = <x, wfrec(r, x, H)> <-> 
   1.393 -       (\<exists>f. M(f) & is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) & 
   1.394 +       (\<exists>f[M]. is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) & 
   1.395              y = <x, H(x,restrict(f,r-``{x}))>)"
   1.396  apply safe  
   1.397   apply (simp add: wfrec_relativize [THEN iff_sym]) 
   1.398 @@ -597,7 +598,7 @@
   1.399  apply (simp add: wfrec_relativize, blast) 
   1.400  done
   1.401  
   1.402 -lemma (in M_recursion) wfrec_closed_lemma [rule_format]:
   1.403 +lemma (in M_wfrank) wfrec_closed_lemma [rule_format]:
   1.404       "[|wf(r); M(r); 
   1.405          strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
   1.406          \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   1.407 @@ -611,9 +612,9 @@
   1.408  done
   1.409  
   1.410  text{*Full version not assuming transitivity, but maybe not very useful.*}
   1.411 -theorem (in M_recursion) wfrec_closed:
   1.412 +theorem (in M_wfrank) wfrec_closed:
   1.413       "[|wf(r); M(r); M(a);
   1.414 -     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   1.415 +     strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
   1.416            pair(M,x,y,z) & 
   1.417            is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & 
   1.418            y = H(x, restrict(g, r -`` {x})));