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.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.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.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.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.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.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.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.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'
```