src/ZF/Constructible/WF_absolute.thy
changeset 13254 5146ccaedf42
parent 13251 74cb2af8811e
child 13268 240509babf00
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Fri Jun 28 11:24:36 2002 +0200
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Fri Jun 28 11:25:46 2002 +0200
     1.3 @@ -303,8 +303,7 @@
     1.4   apply (rule univalent_is_recfun)
     1.5     apply (blast intro: wellfounded_trancl)
     1.6    apply (rule trans_trancl)
     1.7 - apply (simp add: trancl_subset_times)
     1.8 -apply blast
     1.9 + apply (simp add: trancl_subset_times, blast)
    1.10  done
    1.11  
    1.12  lemma (in M_recursion) Ord_wfrank_range [rule_format]:
    1.13 @@ -312,9 +311,8 @@
    1.14       ==> \<forall>f. M(f) --> is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))"
    1.15  apply (drule wellfounded_trancl, assumption)
    1.16  apply (rule wellfounded_induct, assumption+)
    1.17 -  apply (simp add:);
    1.18 - apply (blast intro: Ord_wfrank_separation);
    1.19 -apply (clarify)
    1.20 +  apply simp
    1.21 + apply (blast intro: Ord_wfrank_separation, clarify)
    1.22  txt{*The reasoning in both cases is that we get @{term y} such that
    1.23     @{term "\<langle>y, x\<rangle> \<in> r^+"}.  We find that
    1.24     @{term "f`y = restrict(f, r^+ -`` {y})"}. *}
    1.25 @@ -488,4 +486,142 @@
    1.26       "[|relation(r); M(r); M(A)|] ==> wellfounded_on(M,A,r) <-> wf[A](r)"
    1.27  by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized)
    1.28  
    1.29 +
    1.30 +text{*absoluteness for wfrec-defined functions.*}
    1.31 +
    1.32 +(*first use is_recfun, then M_is_recfun*)
    1.33 +
    1.34 +lemma (in M_trancl) wfrec_relativize:
    1.35 +  "[|wf(r); M(a); M(r);  
    1.36 +     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
    1.37 +          pair(M,x,y,z) & 
    1.38 +          is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & 
    1.39 +          y = H(x, restrict(g, r -`` {x}))); 
    1.40 +     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
    1.41 +   ==> wfrec(r,a,H) = z <-> 
    1.42 +       (\<exists>f. M(f) & is_recfun(r^+, a, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) & 
    1.43 +            z = H(a,restrict(f,r-``{a})))"
    1.44 +apply (frule wf_trancl) 
    1.45 +apply (simp add: wftrec_def wfrec_def, safe)
    1.46 + apply (frule wf_exists_is_recfun 
    1.47 +              [of concl: "r^+" a "\<lambda>x f. H(x, restrict(f, r -`` {x}))"]) 
    1.48 +      apply (simp_all add: trans_trancl function_restrictI trancl_subset_times)
    1.49 + apply (clarify, rule_tac x=f in exI) 
    1.50 + apply (simp_all add: the_recfun_eq trans_trancl trancl_subset_times)
    1.51 +done
    1.52 +
    1.53 +
    1.54 +text{*Assuming @{term r} is transitive simplifies the occurrences of @{text H}.
    1.55 +      The premise @{term "relation(r)"} is necessary 
    1.56 +      before we can replace @{term "r^+"} by @{term r}. *}
    1.57 +theorem (in M_trancl) trans_wfrec_relativize:
    1.58 +  "[|wf(r);  trans(r);  relation(r);  M(r);  M(a);
    1.59 +     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
    1.60 +                pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
    1.61 +     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
    1.62 +   ==> wfrec(r,a,H) = z <-> (\<exists>f. M(f) & is_recfun(r,a,H,f) & z = H(a,f))" 
    1.63 +by (simp cong: is_recfun_cong
    1.64 +         add: wfrec_relativize trancl_eq_r
    1.65 +               is_recfun_restrict_idem domain_restrict_idem)
    1.66 +
    1.67 +
    1.68 +lemma (in M_trancl) trans_eq_pair_wfrec_iff:
    1.69 +  "[|wf(r);  trans(r); relation(r); M(r);  M(y); 
    1.70 +     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
    1.71 +                pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
    1.72 +     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
    1.73 +   ==> y = <x, wfrec(r, x, H)> <-> 
    1.74 +       (\<exists>f. M(f) & is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
    1.75 +apply safe  
    1.76 + apply (simp add: trans_wfrec_relativize [THEN iff_sym]) 
    1.77 +txt{*converse direction*}
    1.78 +apply (rule sym)
    1.79 +apply (simp add: trans_wfrec_relativize, blast) 
    1.80 +done
    1.81 +
    1.82 +
    1.83 +subsection{*M is closed under well-founded recursion*}
    1.84 +
    1.85 +text{*Lemma with the awkward premise mentioning @{text wfrec}.*}
    1.86 +lemma (in M_recursion) wfrec_closed_lemma [rule_format]:
    1.87 +     "[|wf(r); M(r); 
    1.88 +        strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
    1.89 +        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
    1.90 +      ==> M(a) --> M(wfrec(r,a,H))"
    1.91 +apply (rule_tac a=a in wf_induct, assumption+)
    1.92 +apply (subst wfrec, assumption, clarify)
    1.93 +apply (drule_tac x1=x and x="\<lambda>x\<in>r -`` {x}. wfrec(r, x, H)" 
    1.94 +       in rspec [THEN rspec]) 
    1.95 +apply (simp_all add: function_lam) 
    1.96 +apply (blast intro: dest: pair_components_in_M ) 
    1.97 +done
    1.98 +
    1.99 +text{*Eliminates one instance of replacement.*}
   1.100 +lemma (in M_recursion) wfrec_replacement_iff:
   1.101 +     "strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   1.102 +                pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)) <->
   1.103 +      strong_replacement(M, 
   1.104 +           \<lambda>x y. \<exists>f. M(f) & is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
   1.105 +apply simp 
   1.106 +apply (rule strong_replacement_cong, blast) 
   1.107 +done
   1.108 +
   1.109 +text{*Useful version for transitive relations*}
   1.110 +theorem (in M_recursion) trans_wfrec_closed:
   1.111 +     "[|wf(r); trans(r); relation(r); M(r); M(a);
   1.112 +        strong_replacement(M, 
   1.113 +             \<lambda>x z. \<exists>y g. M(y) & M(g) &
   1.114 +                    pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
   1.115 +        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   1.116 +      ==> M(wfrec(r,a,H))"
   1.117 +apply (frule wfrec_replacement_iff [THEN iffD1]) 
   1.118 +apply (rule wfrec_closed_lemma, assumption+) 
   1.119 +apply (simp_all add: wfrec_replacement_iff trans_eq_pair_wfrec_iff) 
   1.120 +done
   1.121 +
   1.122 +section{*Absoluteness without assuming transitivity*}
   1.123 +lemma (in M_trancl) eq_pair_wfrec_iff:
   1.124 +  "[|wf(r);  M(r);  M(y); 
   1.125 +     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   1.126 +          pair(M,x,y,z) & 
   1.127 +          is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & 
   1.128 +          y = H(x, restrict(g, r -`` {x}))); 
   1.129 +     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.130 +   ==> y = <x, wfrec(r, x, H)> <-> 
   1.131 +       (\<exists>f. M(f) & is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) & 
   1.132 +            y = <x, H(x,restrict(f,r-``{x}))>)"
   1.133 +apply safe  
   1.134 + apply (simp add: wfrec_relativize [THEN iff_sym]) 
   1.135 +txt{*converse direction*}
   1.136 +apply (rule sym)
   1.137 +apply (simp add: wfrec_relativize, blast) 
   1.138 +done
   1.139 +
   1.140 +lemma (in M_recursion) wfrec_closed_lemma [rule_format]:
   1.141 +     "[|wf(r); M(r); 
   1.142 +        strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
   1.143 +        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   1.144 +      ==> M(a) --> M(wfrec(r,a,H))"
   1.145 +apply (rule_tac a=a in wf_induct, assumption+)
   1.146 +apply (subst wfrec, assumption, clarify)
   1.147 +apply (drule_tac x1=x and x="\<lambda>x\<in>r -`` {x}. wfrec(r, x, H)" 
   1.148 +       in rspec [THEN rspec]) 
   1.149 +apply (simp_all add: function_lam) 
   1.150 +apply (blast intro: dest: pair_components_in_M ) 
   1.151 +done
   1.152 +
   1.153 +text{*Full version not assuming transitivity, but maybe not very useful.*}
   1.154 +theorem (in M_recursion) wfrec_closed:
   1.155 +     "[|wf(r); M(r); M(a);
   1.156 +     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   1.157 +          pair(M,x,y,z) & 
   1.158 +          is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & 
   1.159 +          y = H(x, restrict(g, r -`` {x}))); 
   1.160 +        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   1.161 +      ==> M(wfrec(r,a,H))"
   1.162 +apply (frule wfrec_replacement_iff [THEN iffD1]) 
   1.163 +apply (rule wfrec_closed_lemma, assumption+) 
   1.164 +apply (simp_all add: eq_pair_wfrec_iff) 
   1.165 +done
   1.166 +
   1.167  end