src/ZF/Constructible/WF_absolute.thy
changeset 13634 99a593b49b04
parent 13615 449a70d88b38
child 13647 7f6f0ffc45c3
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Tue Oct 08 14:09:18 2002 +0200
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Wed Oct 09 11:07:13 2002 +0200
     1.3 @@ -1,68 +1,12 @@
     1.4  (*  Title:      ZF/Constructible/WF_absolute.thy
     1.5      ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   2002  University of Cambridge
     1.8  *)
     1.9  
    1.10  header {*Absoluteness for Well-Founded Relations and Well-Founded Recursion*}
    1.11  
    1.12  theory WF_absolute = WFrec:
    1.13  
    1.14 -subsection{*Every well-founded relation is a subset of some inverse image of
    1.15 -      an ordinal*}
    1.16 -
    1.17 -lemma wf_rvimage_Ord: "Ord(i) \<Longrightarrow> wf(rvimage(A, f, Memrel(i)))"
    1.18 -by (blast intro: wf_rvimage wf_Memrel)
    1.19 -
    1.20 -
    1.21 -constdefs
    1.22 -  wfrank :: "[i,i]=>i"
    1.23 -    "wfrank(r,a) == wfrec(r, a, %x f. \<Union>y \<in> r-``{x}. succ(f`y))"
    1.24 -
    1.25 -constdefs
    1.26 -  wftype :: "i=>i"
    1.27 -    "wftype(r) == \<Union>y \<in> range(r). succ(wfrank(r,y))"
    1.28 -
    1.29 -lemma wfrank: "wf(r) ==> wfrank(r,a) = (\<Union>y \<in> r-``{a}. succ(wfrank(r,y)))"
    1.30 -by (subst wfrank_def [THEN def_wfrec], simp_all)
    1.31 -
    1.32 -lemma Ord_wfrank: "wf(r) ==> Ord(wfrank(r,a))"
    1.33 -apply (rule_tac a=a in wf_induct, assumption)
    1.34 -apply (subst wfrank, assumption)
    1.35 -apply (rule Ord_succ [THEN Ord_UN], blast)
    1.36 -done
    1.37 -
    1.38 -lemma wfrank_lt: "[|wf(r); <a,b> \<in> r|] ==> wfrank(r,a) < wfrank(r,b)"
    1.39 -apply (rule_tac a1 = b in wfrank [THEN ssubst], assumption)
    1.40 -apply (rule UN_I [THEN ltI])
    1.41 -apply (simp add: Ord_wfrank vimage_iff)+
    1.42 -done
    1.43 -
    1.44 -lemma Ord_wftype: "wf(r) ==> Ord(wftype(r))"
    1.45 -by (simp add: wftype_def Ord_wfrank)
    1.46 -
    1.47 -lemma wftypeI: "\<lbrakk>wf(r);  x \<in> field(r)\<rbrakk> \<Longrightarrow> wfrank(r,x) \<in> wftype(r)"
    1.48 -apply (simp add: wftype_def)
    1.49 -apply (blast intro: wfrank_lt [THEN ltD])
    1.50 -done
    1.51 -
    1.52 -
    1.53 -lemma wf_imp_subset_rvimage:
    1.54 -     "[|wf(r); r \<subseteq> A*A|] ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
    1.55 -apply (rule_tac x="wftype(r)" in exI)
    1.56 -apply (rule_tac x="\<lambda>x\<in>A. wfrank(r,x)" in exI)
    1.57 -apply (simp add: Ord_wftype, clarify)
    1.58 -apply (frule subsetD, assumption, clarify)
    1.59 -apply (simp add: rvimage_iff wfrank_lt [THEN ltD])
    1.60 -apply (blast intro: wftypeI)
    1.61 -done
    1.62 -
    1.63 -theorem wf_iff_subset_rvimage:
    1.64 -  "relation(r) ==> wf(r) <-> (\<exists>i f A. Ord(i) & r <= rvimage(A, f, Memrel(i)))"
    1.65 -by (blast dest!: relation_field_times_field wf_imp_subset_rvimage
    1.66 -          intro: wf_rvimage_Ord [THEN wf_subset])
    1.67 -
    1.68 -
    1.69  subsection{*Transitive closure without fixedpoints*}
    1.70  
    1.71  constdefs
    1.72 @@ -236,271 +180,6 @@
    1.73  rank function.*}
    1.74  
    1.75  
    1.76 -locale M_wfrank = M_trancl +
    1.77 -  assumes wfrank_separation:
    1.78 -     "M(r) ==>
    1.79 -      separation (M, \<lambda>x. 
    1.80 -         \<forall>rplus[M]. tran_closure(M,r,rplus) -->
    1.81 -         ~ (\<exists>f[M]. M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f)))"
    1.82 - and wfrank_strong_replacement:
    1.83 -     "M(r) ==>
    1.84 -      strong_replacement(M, \<lambda>x z. 
    1.85 -         \<forall>rplus[M]. tran_closure(M,r,rplus) -->
    1.86 -         (\<exists>y[M]. \<exists>f[M]. pair(M,x,y,z)  & 
    1.87 -                        M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f) &
    1.88 -                        is_range(M,f,y)))"
    1.89 - and Ord_wfrank_separation:
    1.90 -     "M(r) ==>
    1.91 -      separation (M, \<lambda>x.
    1.92 -         \<forall>rplus[M]. tran_closure(M,r,rplus) --> 
    1.93 -          ~ (\<forall>f[M]. \<forall>rangef[M]. 
    1.94 -             is_range(M,f,rangef) -->
    1.95 -             M_is_recfun(M, \<lambda>x f y. is_range(M,f,y), rplus, x, f) -->
    1.96 -             ordinal(M,rangef)))" 
    1.97 -
    1.98 -text{*Proving that the relativized instances of Separation or Replacement
    1.99 -agree with the "real" ones.*}
   1.100 -
   1.101 -lemma (in M_wfrank) wfrank_separation':
   1.102 -     "M(r) ==>
   1.103 -      separation
   1.104 -	   (M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r^+, x, %x f. range(f), f)))"
   1.105 -apply (insert wfrank_separation [of r])
   1.106 -apply (simp add: relativize2_def is_recfun_abs [of "%x. range"])
   1.107 -done
   1.108 -
   1.109 -lemma (in M_wfrank) wfrank_strong_replacement':
   1.110 -     "M(r) ==>
   1.111 -      strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>f[M]. 
   1.112 -		  pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) &
   1.113 -		  y = range(f))"
   1.114 -apply (insert wfrank_strong_replacement [of r])
   1.115 -apply (simp add: relativize2_def is_recfun_abs [of "%x. range"])
   1.116 -done
   1.117 -
   1.118 -lemma (in M_wfrank) Ord_wfrank_separation':
   1.119 -     "M(r) ==>
   1.120 -      separation (M, \<lambda>x. 
   1.121 -         ~ (\<forall>f[M]. is_recfun(r^+, x, \<lambda>x. range, f) --> Ord(range(f))))" 
   1.122 -apply (insert Ord_wfrank_separation [of r])
   1.123 -apply (simp add: relativize2_def is_recfun_abs [of "%x. range"])
   1.124 -done
   1.125 -
   1.126 -text{*This function, defined using replacement, is a rank function for
   1.127 -well-founded relations within the class M.*}
   1.128 -constdefs
   1.129 - wellfoundedrank :: "[i=>o,i,i] => i"
   1.130 -    "wellfoundedrank(M,r,A) ==
   1.131 -        {p. x\<in>A, \<exists>y[M]. \<exists>f[M]. 
   1.132 -                       p = <x,y> & is_recfun(r^+, x, %x f. range(f), f) &
   1.133 -                       y = range(f)}"
   1.134 -
   1.135 -lemma (in M_wfrank) exists_wfrank:
   1.136 -    "[| wellfounded(M,r); M(a); M(r) |]
   1.137 -     ==> \<exists>f[M]. is_recfun(r^+, a, %x f. range(f), f)"
   1.138 -apply (rule wellfounded_exists_is_recfun)
   1.139 -      apply (blast intro: wellfounded_trancl)
   1.140 -     apply (rule trans_trancl)
   1.141 -    apply (erule wfrank_separation')
   1.142 -   apply (erule wfrank_strong_replacement')
   1.143 -apply (simp_all add: trancl_subset_times)
   1.144 -done
   1.145 -
   1.146 -lemma (in M_wfrank) M_wellfoundedrank:
   1.147 -    "[| wellfounded(M,r); M(r); M(A) |] ==> M(wellfoundedrank(M,r,A))"
   1.148 -apply (insert wfrank_strong_replacement' [of r])
   1.149 -apply (simp add: wellfoundedrank_def)
   1.150 -apply (rule strong_replacement_closed)
   1.151 -   apply assumption+
   1.152 - apply (rule univalent_is_recfun)
   1.153 -   apply (blast intro: wellfounded_trancl)
   1.154 -  apply (rule trans_trancl)
   1.155 - apply (simp add: trancl_subset_times) 
   1.156 -apply (blast dest: transM) 
   1.157 -done
   1.158 -
   1.159 -lemma (in M_wfrank) Ord_wfrank_range [rule_format]:
   1.160 -    "[| wellfounded(M,r); a\<in>A; M(r); M(A) |]
   1.161 -     ==> \<forall>f[M]. is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))"
   1.162 -apply (drule wellfounded_trancl, assumption)
   1.163 -apply (rule wellfounded_induct, assumption, erule (1) transM)
   1.164 -  apply simp
   1.165 - apply (blast intro: Ord_wfrank_separation', clarify)
   1.166 -txt{*The reasoning in both cases is that we get @{term y} such that
   1.167 -   @{term "\<langle>y, x\<rangle> \<in> r^+"}.  We find that
   1.168 -   @{term "f`y = restrict(f, r^+ -`` {y})"}. *}
   1.169 -apply (rule OrdI [OF _ Ord_is_Transset])
   1.170 - txt{*An ordinal is a transitive set...*}
   1.171 - apply (simp add: Transset_def)
   1.172 - apply clarify
   1.173 - apply (frule apply_recfun2, assumption)
   1.174 - apply (force simp add: restrict_iff)
   1.175 -txt{*...of ordinals.  This second case requires the induction hyp.*}
   1.176 -apply clarify
   1.177 -apply (rename_tac i y)
   1.178 -apply (frule apply_recfun2, assumption)
   1.179 -apply (frule is_recfun_imp_in_r, assumption)
   1.180 -apply (frule is_recfun_restrict)
   1.181 -    (*simp_all won't work*)
   1.182 -    apply (simp add: trans_trancl trancl_subset_times)+
   1.183 -apply (drule spec [THEN mp], assumption)
   1.184 -apply (subgoal_tac "M(restrict(f, r^+ -`` {y}))")
   1.185 - apply (drule_tac x="restrict(f, r^+ -`` {y})" in rspec)
   1.186 -apply assumption
   1.187 - apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
   1.188 -apply (blast dest: pair_components_in_M)
   1.189 -done
   1.190 -
   1.191 -lemma (in M_wfrank) Ord_range_wellfoundedrank:
   1.192 -    "[| wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A) |]
   1.193 -     ==> Ord (range(wellfoundedrank(M,r,A)))"
   1.194 -apply (frule wellfounded_trancl, assumption)
   1.195 -apply (frule trancl_subset_times)
   1.196 -apply (simp add: wellfoundedrank_def)
   1.197 -apply (rule OrdI [OF _ Ord_is_Transset])
   1.198 - prefer 2
   1.199 - txt{*by our previous result the range consists of ordinals.*}
   1.200 - apply (blast intro: Ord_wfrank_range)
   1.201 -txt{*We still must show that the range is a transitive set.*}
   1.202 -apply (simp add: Transset_def, clarify, simp)
   1.203 -apply (rename_tac x i f u)
   1.204 -apply (frule is_recfun_imp_in_r, assumption)
   1.205 -apply (subgoal_tac "M(u) & M(i) & M(x)")
   1.206 - prefer 2 apply (blast dest: transM, clarify)
   1.207 -apply (rule_tac a=u in rangeI)
   1.208 -apply (rule_tac x=u in ReplaceI)
   1.209 -  apply simp 
   1.210 -  apply (rule_tac x="restrict(f, r^+ -`` {u})" in rexI)
   1.211 -   apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2)
   1.212 -  apply simp 
   1.213 -apply blast 
   1.214 -txt{*Unicity requirement of Replacement*}
   1.215 -apply clarify
   1.216 -apply (frule apply_recfun2, assumption)
   1.217 -apply (simp add: trans_trancl is_recfun_cut)
   1.218 -done
   1.219 -
   1.220 -lemma (in M_wfrank) function_wellfoundedrank:
   1.221 -    "[| wellfounded(M,r); M(r); M(A)|]
   1.222 -     ==> function(wellfoundedrank(M,r,A))"
   1.223 -apply (simp add: wellfoundedrank_def function_def, clarify)
   1.224 -txt{*Uniqueness: repeated below!*}
   1.225 -apply (drule is_recfun_functional, assumption)
   1.226 -     apply (blast intro: wellfounded_trancl)
   1.227 -    apply (simp_all add: trancl_subset_times trans_trancl)
   1.228 -done
   1.229 -
   1.230 -lemma (in M_wfrank) domain_wellfoundedrank:
   1.231 -    "[| wellfounded(M,r); M(r); M(A)|]
   1.232 -     ==> domain(wellfoundedrank(M,r,A)) = A"
   1.233 -apply (simp add: wellfoundedrank_def function_def)
   1.234 -apply (rule equalityI, auto)
   1.235 -apply (frule transM, assumption)
   1.236 -apply (frule_tac a=x in exists_wfrank, assumption+, clarify)
   1.237 -apply (rule_tac b="range(f)" in domainI)
   1.238 -apply (rule_tac x=x in ReplaceI)
   1.239 -  apply simp 
   1.240 -  apply (rule_tac x=f in rexI, blast, simp_all)
   1.241 -txt{*Uniqueness (for Replacement): repeated above!*}
   1.242 -apply clarify
   1.243 -apply (drule is_recfun_functional, assumption)
   1.244 -    apply (blast intro: wellfounded_trancl)
   1.245 -    apply (simp_all add: trancl_subset_times trans_trancl)
   1.246 -done
   1.247 -
   1.248 -lemma (in M_wfrank) wellfoundedrank_type:
   1.249 -    "[| wellfounded(M,r);  M(r); M(A)|]
   1.250 -     ==> wellfoundedrank(M,r,A) \<in> A -> range(wellfoundedrank(M,r,A))"
   1.251 -apply (frule function_wellfoundedrank [of r A], assumption+)
   1.252 -apply (frule function_imp_Pi)
   1.253 - apply (simp add: wellfoundedrank_def relation_def)
   1.254 - apply blast
   1.255 -apply (simp add: domain_wellfoundedrank)
   1.256 -done
   1.257 -
   1.258 -lemma (in M_wfrank) Ord_wellfoundedrank:
   1.259 -    "[| wellfounded(M,r); a \<in> A; r \<subseteq> A*A;  M(r); M(A) |]
   1.260 -     ==> Ord(wellfoundedrank(M,r,A) ` a)"
   1.261 -by (blast intro: apply_funtype [OF wellfoundedrank_type]
   1.262 -                 Ord_in_Ord [OF Ord_range_wellfoundedrank])
   1.263 -
   1.264 -lemma (in M_wfrank) wellfoundedrank_eq:
   1.265 -     "[| is_recfun(r^+, a, %x. range, f);
   1.266 -         wellfounded(M,r);  a \<in> A; M(f); M(r); M(A)|]
   1.267 -      ==> wellfoundedrank(M,r,A) ` a = range(f)"
   1.268 -apply (rule apply_equality)
   1.269 - prefer 2 apply (blast intro: wellfoundedrank_type)
   1.270 -apply (simp add: wellfoundedrank_def)
   1.271 -apply (rule ReplaceI)
   1.272 -  apply (rule_tac x="range(f)" in rexI) 
   1.273 -  apply blast
   1.274 - apply simp_all
   1.275 -txt{*Unicity requirement of Replacement*}
   1.276 -apply clarify
   1.277 -apply (drule is_recfun_functional, assumption)
   1.278 -    apply (blast intro: wellfounded_trancl)
   1.279 -    apply (simp_all add: trancl_subset_times trans_trancl)
   1.280 -done
   1.281 -
   1.282 -
   1.283 -lemma (in M_wfrank) wellfoundedrank_lt:
   1.284 -     "[| <a,b> \<in> r;
   1.285 -         wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A)|]
   1.286 -      ==> wellfoundedrank(M,r,A) ` a < wellfoundedrank(M,r,A) ` b"
   1.287 -apply (frule wellfounded_trancl, assumption)
   1.288 -apply (subgoal_tac "a\<in>A & b\<in>A")
   1.289 - prefer 2 apply blast
   1.290 -apply (simp add: lt_def Ord_wellfoundedrank, clarify)
   1.291 -apply (frule exists_wfrank [of concl: _ b], erule (1) transM, assumption)
   1.292 -apply clarify
   1.293 -apply (rename_tac fb)
   1.294 -apply (frule is_recfun_restrict [of concl: "r^+" a])
   1.295 -    apply (rule trans_trancl, assumption)
   1.296 -   apply (simp_all add: r_into_trancl trancl_subset_times)
   1.297 -txt{*Still the same goal, but with new @{text is_recfun} assumptions.*}
   1.298 -apply (simp add: wellfoundedrank_eq)
   1.299 -apply (frule_tac a=a in wellfoundedrank_eq, assumption+)
   1.300 -   apply (simp_all add: transM [of a])
   1.301 -txt{*We have used equations for wellfoundedrank and now must use some
   1.302 -    for  @{text is_recfun}. *}
   1.303 -apply (rule_tac a=a in rangeI)
   1.304 -apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff
   1.305 -                 r_into_trancl apply_recfun r_into_trancl)
   1.306 -done
   1.307 -
   1.308 -
   1.309 -lemma (in M_wfrank) wellfounded_imp_subset_rvimage:
   1.310 -     "[|wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|]
   1.311 -      ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
   1.312 -apply (rule_tac x="range(wellfoundedrank(M,r,A))" in exI)
   1.313 -apply (rule_tac x="wellfoundedrank(M,r,A)" in exI)
   1.314 -apply (simp add: Ord_range_wellfoundedrank, clarify)
   1.315 -apply (frule subsetD, assumption, clarify)
   1.316 -apply (simp add: rvimage_iff wellfoundedrank_lt [THEN ltD])
   1.317 -apply (blast intro: apply_rangeI wellfoundedrank_type)
   1.318 -done
   1.319 -
   1.320 -lemma (in M_wfrank) wellfounded_imp_wf:
   1.321 -     "[|wellfounded(M,r); relation(r); M(r)|] ==> wf(r)"
   1.322 -by (blast dest!: relation_field_times_field wellfounded_imp_subset_rvimage
   1.323 -          intro: wf_rvimage_Ord [THEN wf_subset])
   1.324 -
   1.325 -lemma (in M_wfrank) wellfounded_on_imp_wf_on:
   1.326 -     "[|wellfounded_on(M,A,r); relation(r); M(r); M(A)|] ==> wf[A](r)"
   1.327 -apply (simp add: wellfounded_on_iff_wellfounded wf_on_def)
   1.328 -apply (rule wellfounded_imp_wf)
   1.329 -apply (simp_all add: relation_def)
   1.330 -done
   1.331 -
   1.332 -
   1.333 -theorem (in M_wfrank) wf_abs [simp]:
   1.334 -     "[|relation(r); M(r)|] ==> wellfounded(M,r) <-> wf(r)"
   1.335 -by (blast intro: wellfounded_imp_wf wf_imp_relativized)
   1.336 -
   1.337 -theorem (in M_wfrank) wf_on_abs [simp]:
   1.338 -     "[|relation(r); M(r); M(A)|] ==> wellfounded_on(M,A,r) <-> wf[A](r)"
   1.339 -by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized)
   1.340 -
   1.341  
   1.342  text{*absoluteness for wfrec-defined functions.*}
   1.343  
   1.344 @@ -531,7 +210,7 @@
   1.345        before we can replace @{term "r^+"} by @{term r}. *}
   1.346  theorem (in M_trancl) trans_wfrec_relativize:
   1.347    "[|wf(r);  trans(r);  relation(r);  M(r);  M(a);
   1.348 -     wfrec_replacement(M,MH,r);  relativize2(M,MH,H);
   1.349 +     wfrec_replacement(M,MH,r);  relation2(M,MH,H);
   1.350       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.351     ==> wfrec(r,a,H) = z <-> (\<exists>f[M]. is_recfun(r,a,H,f) & z = H(a,f))" 
   1.352  apply (frule wfrec_replacement', assumption+) 
   1.353 @@ -542,15 +221,15 @@
   1.354  
   1.355  theorem (in M_trancl) trans_wfrec_abs:
   1.356    "[|wf(r);  trans(r);  relation(r);  M(r);  M(a);  M(z);
   1.357 -     wfrec_replacement(M,MH,r);  relativize2(M,MH,H);
   1.358 +     wfrec_replacement(M,MH,r);  relation2(M,MH,H);
   1.359       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.360     ==> is_wfrec(M,MH,r,a,z) <-> z=wfrec(r,a,H)" 
   1.361 -apply (simp add: trans_wfrec_relativize [THEN iff_sym] is_wfrec_abs, blast) 
   1.362 -done
   1.363 +by (simp add: trans_wfrec_relativize [THEN iff_sym] is_wfrec_abs, blast) 
   1.364 +
   1.365  
   1.366  lemma (in M_trancl) trans_eq_pair_wfrec_iff:
   1.367    "[|wf(r);  trans(r); relation(r); M(r);  M(y); 
   1.368 -     wfrec_replacement(M,MH,r);  relativize2(M,MH,H);
   1.369 +     wfrec_replacement(M,MH,r);  relation2(M,MH,H);
   1.370       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.371     ==> y = <x, wfrec(r, x, H)> <-> 
   1.372         (\<exists>f[M]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
   1.373 @@ -565,7 +244,7 @@
   1.374  subsection{*M is closed under well-founded recursion*}
   1.375  
   1.376  text{*Lemma with the awkward premise mentioning @{text wfrec}.*}
   1.377 -lemma (in M_wfrank) wfrec_closed_lemma [rule_format]:
   1.378 +lemma (in M_trancl) wfrec_closed_lemma [rule_format]:
   1.379       "[|wf(r); M(r); 
   1.380          strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
   1.381          \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   1.382 @@ -579,7 +258,7 @@
   1.383  done
   1.384  
   1.385  text{*Eliminates one instance of replacement.*}
   1.386 -lemma (in M_wfrank) wfrec_replacement_iff:
   1.387 +lemma (in M_trancl) wfrec_replacement_iff:
   1.388       "strong_replacement(M, \<lambda>x z. 
   1.389            \<exists>y[M]. pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g))) <->
   1.390        strong_replacement(M, 
   1.391 @@ -589,9 +268,9 @@
   1.392  done
   1.393  
   1.394  text{*Useful version for transitive relations*}
   1.395 -theorem (in M_wfrank) trans_wfrec_closed:
   1.396 +theorem (in M_trancl) trans_wfrec_closed:
   1.397       "[|wf(r); trans(r); relation(r); M(r); M(a);
   1.398 -       wfrec_replacement(M,MH,r);  relativize2(M,MH,H);
   1.399 +       wfrec_replacement(M,MH,r);  relation2(M,MH,H);
   1.400          \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   1.401        ==> M(wfrec(r,a,H))"
   1.402  apply (frule wfrec_replacement', assumption+) 
   1.403 @@ -619,10 +298,10 @@
   1.404  done
   1.405  
   1.406  text{*Full version not assuming transitivity, but maybe not very useful.*}
   1.407 -theorem (in M_wfrank) wfrec_closed:
   1.408 +theorem (in M_trancl) wfrec_closed:
   1.409       "[|wf(r); M(r); M(a);
   1.410          wfrec_replacement(M,MH,r^+);  
   1.411 -        relativize2(M,MH, \<lambda>x f. H(x, restrict(f, r -`` {x})));
   1.412 +        relation2(M,MH, \<lambda>x f. H(x, restrict(f, r -`` {x})));
   1.413          \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   1.414        ==> M(wfrec(r,a,H))"
   1.415  apply (frule wfrec_replacement'