src/ZF/Constructible/WF_absolute.thy
changeset 13348 374d05460db4
parent 13339 0f89104dd377
child 13350 626b79677dfa
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Thu Jul 11 10:48:30 2002 +0200
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Thu Jul 11 13:43:24 2002 +0200
     1.3 @@ -232,21 +232,30 @@
     1.4  rank function.*}
     1.5  
     1.6  
     1.7 -(*NEEDS RELATIVIZATION*)
     1.8  locale M_wfrank = M_trancl +
     1.9    assumes wfrank_separation:
    1.10       "M(r) ==>
    1.11        separation (M, \<lambda>x. 
    1.12 -         ~ (\<exists>f[M]. M_is_recfun(M, r^+, x, %mm x f y. y = range(f), f)))"
    1.13 - and wfrank_strong_replacement':
    1.14 +         \<forall>rplus[M]. tran_closure(M,r,rplus) -->
    1.15 +         ~ (\<exists>f[M]. M_is_recfun(M, rplus, x, %x f y. is_range(M,f,y), f)))"
    1.16 + and wfrank_strong_replacement:
    1.17       "M(r) ==>
    1.18 -      strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>f[M]. 
    1.19 -		  pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) &
    1.20 -		  y = range(f))"
    1.21 +      strong_replacement(M, \<lambda>x z. 
    1.22 +         \<forall>rplus[M]. tran_closure(M,r,rplus) -->
    1.23 +         (\<exists>y[M]. \<exists>f[M]. pair(M,x,y,z)  & 
    1.24 +                        M_is_recfun(M, rplus, x, %x f y. is_range(M,f,y), f) &
    1.25 +                        is_range(M,f,y)))"
    1.26   and Ord_wfrank_separation:
    1.27       "M(r) ==>
    1.28 -      separation (M, \<lambda>x. ~ (\<forall>f. M(f) \<longrightarrow>
    1.29 -                       is_recfun(r^+, x, \<lambda>x. range, f) \<longrightarrow> Ord(range(f))))" 
    1.30 +      separation (M, \<lambda>x.
    1.31 +         \<forall>rplus[M]. tran_closure(M,r,rplus) --> 
    1.32 +          ~ (\<forall>f[M]. \<forall>rangef[M]. 
    1.33 +             is_range(M,f,rangef) -->
    1.34 +             M_is_recfun(M, rplus, x, \<lambda>x f y. is_range(M,f,y), f) -->
    1.35 +             ordinal(M,rangef)))" 
    1.36 +
    1.37 +text{*Proving that the relativized instances of Separation or Replacement
    1.38 +agree with the "real" ones.*}
    1.39  
    1.40  lemma (in M_wfrank) wfrank_separation':
    1.41       "M(r) ==>
    1.42 @@ -256,6 +265,23 @@
    1.43  apply (simp add: is_recfun_iff_M [of concl: _ _ "%x. range", THEN iff_sym])
    1.44  done
    1.45  
    1.46 +lemma (in M_wfrank) wfrank_strong_replacement':
    1.47 +     "M(r) ==>
    1.48 +      strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>f[M]. 
    1.49 +		  pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) &
    1.50 +		  y = range(f))"
    1.51 +apply (insert wfrank_strong_replacement [of r])
    1.52 +apply (simp add: is_recfun_iff_M [of concl: _ _ "%x. range", THEN iff_sym])
    1.53 +done
    1.54 +
    1.55 +lemma (in M_wfrank) Ord_wfrank_separation':
    1.56 +     "M(r) ==>
    1.57 +      separation (M, \<lambda>x. 
    1.58 +         ~ (\<forall>f[M]. is_recfun(r^+, x, \<lambda>x. range, f) --> Ord(range(f))))" 
    1.59 +apply (insert Ord_wfrank_separation [of r])
    1.60 +apply (simp add: is_recfun_iff_M [of concl: _ _ "%x. range", THEN iff_sym])
    1.61 +done
    1.62 +
    1.63  text{*This function, defined using replacement, is a rank function for
    1.64  well-founded relations within the class M.*}
    1.65  constdefs
    1.66 @@ -290,11 +316,11 @@
    1.67  
    1.68  lemma (in M_wfrank) Ord_wfrank_range [rule_format]:
    1.69      "[| wellfounded(M,r); a\<in>A; M(r); M(A) |]
    1.70 -     ==> \<forall>f. M(f) --> is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))"
    1.71 +     ==> \<forall>f[M]. is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))"
    1.72  apply (drule wellfounded_trancl, assumption)
    1.73  apply (rule wellfounded_induct, assumption+)
    1.74    apply simp
    1.75 - apply (blast intro: Ord_wfrank_separation, clarify)
    1.76 + apply (blast intro: Ord_wfrank_separation', clarify)
    1.77  txt{*The reasoning in both cases is that we get @{term y} such that
    1.78     @{term "\<langle>y, x\<rangle> \<in> r^+"}.  We find that
    1.79     @{term "f`y = restrict(f, r^+ -`` {y})"}. *}
    1.80 @@ -314,7 +340,8 @@
    1.81      apply (simp add: trans_trancl trancl_subset_times)+
    1.82  apply (drule spec [THEN mp], assumption)
    1.83  apply (subgoal_tac "M(restrict(f, r^+ -`` {y}))")
    1.84 - apply (drule_tac x="restrict(f, r^+ -`` {y})" in spec)
    1.85 + apply (drule_tac x="restrict(f, r^+ -`` {y})" in rspec)
    1.86 +apply assumption
    1.87   apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
    1.88  apply (blast dest: pair_components_in_M)
    1.89  done