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.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.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.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.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.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.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})));
```