src/ZF/Constructible/Rec_Separation.thy
changeset 13363 c26eeb000470
parent 13352 3cd767f8d78b
child 13385 31df66ca0780
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Tue Jul 16 16:28:49 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Tue Jul 16 16:29:36 2002 +0200
     1.3 @@ -1,10 +1,13 @@
     1.4 -header{*Separation for the Absoluteness of Recursion*}
     1.5 +header{*Separation for Facts About Recursion*}
     1.6  
     1.7 -theory Rec_Separation = Separation:
     1.8 +theory Rec_Separation = Separation + Datatype_absolute:
     1.9  
    1.10  text{*This theory proves all instances needed for locales @{text
    1.11  "M_trancl"}, @{text "M_wfrank"} and @{text "M_datatypes"}*}
    1.12  
    1.13 +lemma eq_succ_imp_lt: "[|i = succ(j); Ord(i)|] ==> j<i"
    1.14 +by simp 
    1.15 +
    1.16  subsection{*The Locale @{text "M_trancl"}*}
    1.17  
    1.18  subsubsection{*Separation for Reflexive/Transitive Closure*}
    1.19 @@ -194,6 +197,40 @@
    1.20  apply (simp_all add: succ_Un_distrib [symmetric])
    1.21  done
    1.22  
    1.23 +
    1.24 +subsubsection{*Instantiating the locale @{text M_trancl}*}
    1.25 +ML
    1.26 +{*
    1.27 +val rtrancl_separation = thm "rtrancl_separation";
    1.28 +val wellfounded_trancl_separation = thm "wellfounded_trancl_separation";
    1.29 +
    1.30 +
    1.31 +val m_trancl = [rtrancl_separation, wellfounded_trancl_separation];
    1.32 +
    1.33 +fun trancl_L th =
    1.34 +    kill_flex_triv_prems (m_trancl MRS (axioms_L th));
    1.35 +
    1.36 +bind_thm ("iterates_abs", trancl_L (thm "M_trancl.iterates_abs"));
    1.37 +bind_thm ("rtran_closure_rtrancl", trancl_L (thm "M_trancl.rtran_closure_rtrancl"));
    1.38 +bind_thm ("rtrancl_closed", trancl_L (thm "M_trancl.rtrancl_closed"));
    1.39 +bind_thm ("rtrancl_abs", trancl_L (thm "M_trancl.rtrancl_abs"));
    1.40 +bind_thm ("trancl_closed", trancl_L (thm "M_trancl.trancl_closed"));
    1.41 +bind_thm ("trancl_abs", trancl_L (thm "M_trancl.trancl_abs"));
    1.42 +bind_thm ("wellfounded_on_trancl", trancl_L (thm "M_trancl.wellfounded_on_trancl"));
    1.43 +bind_thm ("wellfounded_trancl", trancl_L (thm "M_trancl.wellfounded_trancl"));
    1.44 +bind_thm ("wfrec_relativize", trancl_L (thm "M_trancl.wfrec_relativize"));
    1.45 +bind_thm ("trans_wfrec_relativize", trancl_L (thm "M_trancl.trans_wfrec_relativize"));
    1.46 +bind_thm ("trans_wfrec_abs", trancl_L (thm "M_trancl.trans_wfrec_abs"));
    1.47 +bind_thm ("trans_eq_pair_wfrec_iff", trancl_L (thm "M_trancl.trans_eq_pair_wfrec_iff"));
    1.48 +bind_thm ("eq_pair_wfrec_iff", trancl_L (thm "M_trancl.eq_pair_wfrec_iff"));
    1.49 +*}
    1.50 +
    1.51 +declare rtrancl_closed [intro,simp]
    1.52 +declare rtrancl_abs [simp]
    1.53 +declare trancl_closed [intro,simp]
    1.54 +declare trancl_abs [simp]
    1.55 +
    1.56 +
    1.57  subsection{*Well-Founded Recursion!*}
    1.58  
    1.59  (* M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
    1.60 @@ -275,7 +312,22 @@
    1.61               restriction_reflection MH_reflection)  
    1.62  done
    1.63  
    1.64 -subsection{*Separation for  @{term "wfrank"}*}
    1.65 +text{*Currently, @{text sats}-theorems for higher-order operators don't seem
    1.66 +useful.  Reflection theorems do work, though.  This one avoids the repetition
    1.67 +of the @{text MH}-term.*}
    1.68 +theorem is_wfrec_reflection:
    1.69 +  assumes MH_reflection:
    1.70 +    "!!f g h. REFLECTS[\<lambda>x. MH(L, f(x), g(x), h(x)), 
    1.71 +                     \<lambda>i x. MH(**Lset(i), f(x), g(x), h(x))]"
    1.72 +  shows "REFLECTS[\<lambda>x. is_wfrec(L, MH(L), f(x), g(x), h(x)), 
    1.73 +               \<lambda>i x. is_wfrec(**Lset(i), MH(**Lset(i)), f(x), g(x), h(x))]"
    1.74 +apply (simp (no_asm_use) only: is_wfrec_def setclass_simps)
    1.75 +apply (intro FOL_reflections MH_reflection is_recfun_reflection)  
    1.76 +done
    1.77 +
    1.78 +subsection{*The Locale @{text "M_wfrank"}*}
    1.79 +
    1.80 +subsubsection{*Separation for @{term "wfrank"}*}
    1.81  
    1.82  lemma wfrank_Reflects:
    1.83   "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
    1.84 @@ -305,7 +357,7 @@
    1.85  done
    1.86  
    1.87  
    1.88 -subsection{*Replacement for @{term "wfrank"}*}
    1.89 +subsubsection{*Replacement for @{term "wfrank"}*}
    1.90  
    1.91  lemma wfrank_replacement_Reflects:
    1.92   "REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A & 
    1.93 @@ -347,7 +399,7 @@
    1.94  done
    1.95  
    1.96  
    1.97 -subsection{*Separation for  @{term "wfrank"}*}
    1.98 +subsubsection{*Separation for Proving @{text Ord_wfrank_range}*}
    1.99  
   1.100  lemma Ord_wfrank_Reflects:
   1.101   "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) --> 
   1.102 @@ -387,4 +439,438 @@
   1.103  done
   1.104  
   1.105  
   1.106 +subsubsection{*Instantiating the locale @{text M_wfrank}*}
   1.107 +ML
   1.108 +{*
   1.109 +val wfrank_separation = thm "wfrank_separation";
   1.110 +val wfrank_strong_replacement = thm "wfrank_strong_replacement";
   1.111 +val Ord_wfrank_separation = thm "Ord_wfrank_separation";
   1.112 +
   1.113 +val m_wfrank = 
   1.114 +    [wfrank_separation, wfrank_strong_replacement, Ord_wfrank_separation];
   1.115 +
   1.116 +fun wfrank_L th =
   1.117 +    kill_flex_triv_prems (m_wfrank MRS (trancl_L th));
   1.118 +
   1.119 +
   1.120 +
   1.121 +bind_thm ("iterates_closed", wfrank_L (thm "M_wfrank.iterates_closed"));
   1.122 +bind_thm ("exists_wfrank", wfrank_L (thm "M_wfrank.exists_wfrank"));
   1.123 +bind_thm ("M_wellfoundedrank", wfrank_L (thm "M_wfrank.M_wellfoundedrank"));
   1.124 +bind_thm ("Ord_wfrank_range", wfrank_L (thm "M_wfrank.Ord_wfrank_range"));
   1.125 +bind_thm ("Ord_range_wellfoundedrank", wfrank_L (thm "M_wfrank.Ord_range_wellfoundedrank"));
   1.126 +bind_thm ("function_wellfoundedrank", wfrank_L (thm "M_wfrank.function_wellfoundedrank"));
   1.127 +bind_thm ("domain_wellfoundedrank", wfrank_L (thm "M_wfrank.domain_wellfoundedrank"));
   1.128 +bind_thm ("wellfoundedrank_type", wfrank_L (thm "M_wfrank.wellfoundedrank_type"));
   1.129 +bind_thm ("Ord_wellfoundedrank", wfrank_L (thm "M_wfrank.Ord_wellfoundedrank"));
   1.130 +bind_thm ("wellfoundedrank_eq", wfrank_L (thm "M_wfrank.wellfoundedrank_eq"));
   1.131 +bind_thm ("wellfoundedrank_lt", wfrank_L (thm "M_wfrank.wellfoundedrank_lt"));
   1.132 +bind_thm ("wellfounded_imp_subset_rvimage", wfrank_L (thm "M_wfrank.wellfounded_imp_subset_rvimage"));
   1.133 +bind_thm ("wellfounded_imp_wf", wfrank_L (thm "M_wfrank.wellfounded_imp_wf"));
   1.134 +bind_thm ("wellfounded_on_imp_wf_on", wfrank_L (thm "M_wfrank.wellfounded_on_imp_wf_on"));
   1.135 +bind_thm ("wf_abs", wfrank_L (thm "M_wfrank.wf_abs"));
   1.136 +bind_thm ("wf_on_abs", wfrank_L (thm "M_wfrank.wf_on_abs"));
   1.137 +bind_thm ("wfrec_replacement_iff", wfrank_L (thm "M_wfrank.wfrec_replacement_iff"));
   1.138 +bind_thm ("trans_wfrec_closed", wfrank_L (thm "M_wfrank.trans_wfrec_closed"));
   1.139 +bind_thm ("wfrec_closed", wfrank_L (thm "M_wfrank.wfrec_closed"));
   1.140 +*}
   1.141 +
   1.142 +declare iterates_closed [intro,simp]
   1.143 +declare Ord_wfrank_range [rule_format]
   1.144 +declare wf_abs [simp]
   1.145 +declare wf_on_abs [simp]
   1.146 +
   1.147 +
   1.148 +subsection{*For Datatypes*}
   1.149 +
   1.150 +subsubsection{*Binary Products, Internalized*}
   1.151 +
   1.152 +constdefs cartprod_fm :: "[i,i,i]=>i"
   1.153 +(* "cartprod(M,A,B,z) == 
   1.154 +	\<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))" *)
   1.155 +    "cartprod_fm(A,B,z) == 
   1.156 +       Forall(Iff(Member(0,succ(z)),
   1.157 +                  Exists(And(Member(0,succ(succ(A))),
   1.158 +                         Exists(And(Member(0,succ(succ(succ(B)))),
   1.159 +                                    pair_fm(1,0,2)))))))"
   1.160 +
   1.161 +lemma cartprod_type [TC]:
   1.162 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> cartprod_fm(x,y,z) \<in> formula"
   1.163 +by (simp add: cartprod_fm_def) 
   1.164 +
   1.165 +lemma arity_cartprod_fm [simp]:
   1.166 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.167 +      ==> arity(cartprod_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   1.168 +by (simp add: cartprod_fm_def succ_Un_distrib [symmetric] Un_ac) 
   1.169 +
   1.170 +lemma sats_cartprod_fm [simp]:
   1.171 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   1.172 +    ==> sats(A, cartprod_fm(x,y,z), env) <-> 
   1.173 +        cartprod(**A, nth(x,env), nth(y,env), nth(z,env))"
   1.174 +by (simp add: cartprod_fm_def cartprod_def)
   1.175 +
   1.176 +lemma cartprod_iff_sats:
   1.177 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.178 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   1.179 +       ==> cartprod(**A, x, y, z) <-> sats(A, cartprod_fm(i,j,k), env)"
   1.180 +by (simp add: sats_cartprod_fm)
   1.181 +
   1.182 +theorem cartprod_reflection:
   1.183 +     "REFLECTS[\<lambda>x. cartprod(L,f(x),g(x),h(x)), 
   1.184 +               \<lambda>i x. cartprod(**Lset(i),f(x),g(x),h(x))]"
   1.185 +apply (simp only: cartprod_def setclass_simps)
   1.186 +apply (intro FOL_reflections pair_reflection)  
   1.187 +done
   1.188 +
   1.189 +
   1.190 +subsubsection{*Binary Sums, Internalized*}
   1.191 +
   1.192 +(* "is_sum(M,A,B,Z) == 
   1.193 +       \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M]. 
   1.194 +         3      2       1        0
   1.195 +       number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
   1.196 +       cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"  *)
   1.197 +constdefs sum_fm :: "[i,i,i]=>i"
   1.198 +    "sum_fm(A,B,Z) == 
   1.199 +       Exists(Exists(Exists(Exists(
   1.200 +	And(number1_fm(2),
   1.201 +            And(cartprod_fm(2,A#+4,3),
   1.202 +                And(upair_fm(2,2,1),
   1.203 +                    And(cartprod_fm(1,B#+4,0), union_fm(3,0,Z#+4)))))))))"
   1.204 +
   1.205 +lemma sum_type [TC]:
   1.206 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> sum_fm(x,y,z) \<in> formula"
   1.207 +by (simp add: sum_fm_def) 
   1.208 +
   1.209 +lemma arity_sum_fm [simp]:
   1.210 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.211 +      ==> arity(sum_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   1.212 +by (simp add: sum_fm_def succ_Un_distrib [symmetric] Un_ac) 
   1.213 +
   1.214 +lemma sats_sum_fm [simp]:
   1.215 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   1.216 +    ==> sats(A, sum_fm(x,y,z), env) <-> 
   1.217 +        is_sum(**A, nth(x,env), nth(y,env), nth(z,env))"
   1.218 +by (simp add: sum_fm_def is_sum_def)
   1.219 +
   1.220 +lemma sum_iff_sats:
   1.221 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.222 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   1.223 +       ==> is_sum(**A, x, y, z) <-> sats(A, sum_fm(i,j,k), env)"
   1.224 +by simp
   1.225 +
   1.226 +theorem sum_reflection:
   1.227 +     "REFLECTS[\<lambda>x. is_sum(L,f(x),g(x),h(x)), 
   1.228 +               \<lambda>i x. is_sum(**Lset(i),f(x),g(x),h(x))]"
   1.229 +apply (simp only: is_sum_def setclass_simps)
   1.230 +apply (intro FOL_reflections function_reflections cartprod_reflection)  
   1.231 +done
   1.232 +
   1.233 +
   1.234 +subsubsection{*The List Functor, Internalized*}
   1.235 +
   1.236 +constdefs list_functor_fm :: "[i,i,i]=>i"
   1.237 +(* "is_list_functor(M,A,X,Z) == 
   1.238 +        \<exists>n1[M]. \<exists>AX[M]. 
   1.239 +         number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)" *)
   1.240 +    "list_functor_fm(A,X,Z) == 
   1.241 +       Exists(Exists(
   1.242 +	And(number1_fm(1),
   1.243 +            And(cartprod_fm(A#+2,X#+2,0), sum_fm(1,0,Z#+2)))))"
   1.244 +
   1.245 +lemma list_functor_type [TC]:
   1.246 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> list_functor_fm(x,y,z) \<in> formula"
   1.247 +by (simp add: list_functor_fm_def) 
   1.248 +
   1.249 +lemma arity_list_functor_fm [simp]:
   1.250 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.251 +      ==> arity(list_functor_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   1.252 +by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac) 
   1.253 +
   1.254 +lemma sats_list_functor_fm [simp]:
   1.255 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   1.256 +    ==> sats(A, list_functor_fm(x,y,z), env) <-> 
   1.257 +        is_list_functor(**A, nth(x,env), nth(y,env), nth(z,env))"
   1.258 +by (simp add: list_functor_fm_def is_list_functor_def)
   1.259 +
   1.260 +lemma list_functor_iff_sats:
   1.261 +  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.262 +      i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   1.263 +   ==> is_list_functor(**A, x, y, z) <-> sats(A, list_functor_fm(i,j,k), env)"
   1.264 +by simp
   1.265 +
   1.266 +theorem list_functor_reflection:
   1.267 +     "REFLECTS[\<lambda>x. is_list_functor(L,f(x),g(x),h(x)), 
   1.268 +               \<lambda>i x. is_list_functor(**Lset(i),f(x),g(x),h(x))]"
   1.269 +apply (simp only: is_list_functor_def setclass_simps)
   1.270 +apply (intro FOL_reflections number1_reflection
   1.271 +             cartprod_reflection sum_reflection)  
   1.272 +done
   1.273 +
   1.274 +subsubsection{*The Operator @{term quasinat}*}
   1.275 +
   1.276 +(* "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))" *)
   1.277 +constdefs quasinat_fm :: "i=>i"
   1.278 +    "quasinat_fm(z) == Or(empty_fm(z), Exists(succ_fm(0,succ(z))))"
   1.279 +
   1.280 +lemma quasinat_type [TC]:
   1.281 +     "x \<in> nat ==> quasinat_fm(x) \<in> formula"
   1.282 +by (simp add: quasinat_fm_def) 
   1.283 +
   1.284 +lemma arity_quasinat_fm [simp]:
   1.285 +     "x \<in> nat ==> arity(quasinat_fm(x)) = succ(x)"
   1.286 +by (simp add: quasinat_fm_def succ_Un_distrib [symmetric] Un_ac) 
   1.287 +
   1.288 +lemma sats_quasinat_fm [simp]:
   1.289 +   "[| x \<in> nat; env \<in> list(A)|]
   1.290 +    ==> sats(A, quasinat_fm(x), env) <-> is_quasinat(**A, nth(x,env))"
   1.291 +by (simp add: quasinat_fm_def is_quasinat_def)
   1.292 +
   1.293 +lemma quasinat_iff_sats:
   1.294 +      "[| nth(i,env) = x; nth(j,env) = y; 
   1.295 +          i \<in> nat; env \<in> list(A)|]
   1.296 +       ==> is_quasinat(**A, x) <-> sats(A, quasinat_fm(i), env)"
   1.297 +by simp
   1.298 +
   1.299 +theorem quasinat_reflection:
   1.300 +     "REFLECTS[\<lambda>x. is_quasinat(L,f(x)), 
   1.301 +               \<lambda>i x. is_quasinat(**Lset(i),f(x))]"
   1.302 +apply (simp only: is_quasinat_def setclass_simps)
   1.303 +apply (intro FOL_reflections function_reflections)  
   1.304 +done
   1.305 +
   1.306 +
   1.307 +subsubsection{*The Operator @{term is_nat_case}*}
   1.308 +
   1.309 +(* is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o"
   1.310 +    "is_nat_case(M, a, is_b, k, z) == 
   1.311 +       (empty(M,k) --> z=a) &
   1.312 +       (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
   1.313 +       (is_quasinat(M,k) | empty(M,z))" *)
   1.314 +text{*The formula @{term is_b} has free variables 1 and 0.*}
   1.315 +constdefs is_nat_case_fm :: "[i, [i,i]=>i, i, i]=>i"
   1.316 + "is_nat_case_fm(a,is_b,k,z) == 
   1.317 +    And(Implies(empty_fm(k), Equal(z,a)),
   1.318 +        And(Forall(Implies(succ_fm(0,succ(k)), 
   1.319 +                   Forall(Implies(Equal(0,succ(succ(z))), is_b(1,0))))),
   1.320 +            Or(quasinat_fm(k), empty_fm(z))))"
   1.321 +
   1.322 +lemma is_nat_case_type [TC]:
   1.323 +     "[| is_b(1,0) \<in> formula;  
   1.324 +         x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.325 +      ==> is_nat_case_fm(x,is_b,y,z) \<in> formula"
   1.326 +by (simp add: is_nat_case_fm_def) 
   1.327 +
   1.328 +lemma arity_is_nat_case_fm [simp]:
   1.329 +     "[| is_b(1,0) \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.330 +      ==> arity(is_nat_case_fm(x,is_b,y,z)) = 
   1.331 +          succ(x) \<union> succ(y) \<union> succ(z) \<union> (arity(is_b(1,0)) #- 2)" 
   1.332 +apply (subgoal_tac "arity(is_b(1,0)) \<in> nat")  
   1.333 +apply typecheck
   1.334 +(*FIXME: could nat_diff_split work?*)
   1.335 +apply (auto simp add: diff_def raw_diff_succ is_nat_case_fm_def nat_imp_quasinat
   1.336 +                 succ_Un_distrib [symmetric] Un_ac
   1.337 +                 split: split_nat_case) 
   1.338 +done
   1.339 +
   1.340 +lemma sats_is_nat_case_fm:
   1.341 +  assumes is_b_iff_sats: 
   1.342 +      "!!a b. [| a \<in> A; b \<in> A|] 
   1.343 +              ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, Cons(a,env)))"
   1.344 +  shows 
   1.345 +      "[|x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
   1.346 +       ==> sats(A, is_nat_case_fm(x,p,y,z), env) <-> 
   1.347 +           is_nat_case(**A, nth(x,env), is_b, nth(y,env), nth(z,env))"
   1.348 +apply (frule lt_length_in_nat, assumption)  
   1.349 +apply (simp add: is_nat_case_fm_def is_nat_case_def is_b_iff_sats [THEN iff_sym])
   1.350 +done
   1.351 +
   1.352 +lemma is_nat_case_iff_sats:
   1.353 +  "[| (!!a b. [| a \<in> A; b \<in> A|] 
   1.354 +              ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, Cons(a,env))));
   1.355 +      nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.356 +      i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
   1.357 +   ==> is_nat_case(**A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)" 
   1.358 +by (simp add: sats_is_nat_case_fm [of A is_b])
   1.359 +
   1.360 +
   1.361 +text{*The second argument of @{term is_b} gives it direct access to @{term x},
   1.362 +  which is essential for handling free variable references.  Without this 
   1.363 +  argument, we cannot prove reflection for @{term iterates_MH}.*}
   1.364 +theorem is_nat_case_reflection:
   1.365 +  assumes is_b_reflection:
   1.366 +    "!!h f g. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x)), 
   1.367 +                     \<lambda>i x. is_b(**Lset(i), h(x), f(x), g(x))]"
   1.368 +  shows "REFLECTS[\<lambda>x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)), 
   1.369 +               \<lambda>i x. is_nat_case(**Lset(i), f(x), is_b(**Lset(i), x), g(x), h(x))]"
   1.370 +apply (simp (no_asm_use) only: is_nat_case_def setclass_simps)
   1.371 +apply (intro FOL_reflections function_reflections 
   1.372 +             restriction_reflection is_b_reflection quasinat_reflection)  
   1.373 +done
   1.374 +
   1.375 +
   1.376 +
   1.377 +subsection{*The Operator @{term iterates_MH}, Needed for Iteration*}
   1.378 +
   1.379 +(*  iterates_MH :: "[i=>o, [i,i]=>o, i, i, i, i] => o"
   1.380 +   "iterates_MH(M,isF,v,n,g,z) ==
   1.381 +        is_nat_case(M, v, \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & isF(gm,u),
   1.382 +                    n, z)" *)
   1.383 +constdefs iterates_MH_fm :: "[[i,i]=>i, i, i, i, i]=>i"
   1.384 + "iterates_MH_fm(isF,v,n,g,z) == 
   1.385 +    is_nat_case_fm(v, 
   1.386 +      \<lambda>m u. Exists(And(fun_apply_fm(succ(succ(succ(g))),succ(m),0), 
   1.387 +                     Forall(Implies(Equal(0,succ(succ(u))), isF(1,0))))), 
   1.388 +      n, z)"
   1.389 +
   1.390 +lemma iterates_MH_type [TC]:
   1.391 +     "[| p(1,0) \<in> formula;  
   1.392 +         v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.393 +      ==> iterates_MH_fm(p,v,x,y,z) \<in> formula"
   1.394 +by (simp add: iterates_MH_fm_def) 
   1.395 +
   1.396 +
   1.397 +lemma arity_iterates_MH_fm [simp]:
   1.398 +     "[| p(1,0) \<in> formula; 
   1.399 +         v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.400 +      ==> arity(iterates_MH_fm(p,v,x,y,z)) = 
   1.401 +          succ(v) \<union> succ(x) \<union> succ(y) \<union> succ(z) \<union> (arity(p(1,0)) #- 4)"
   1.402 +apply (subgoal_tac "arity(p(1,0)) \<in> nat")
   1.403 +apply typecheck
   1.404 +apply (simp add: nat_imp_quasinat iterates_MH_fm_def Un_ac
   1.405 +            split: split_nat_case, clarify)
   1.406 +apply (rename_tac i j)
   1.407 +apply (drule eq_succ_imp_eq_m1, simp) 
   1.408 +apply (drule eq_succ_imp_eq_m1, simp)
   1.409 +apply (simp add: diff_Un_distrib succ_Un_distrib Un_ac diff_diff_left)
   1.410 +done
   1.411 +
   1.412 +lemma sats_iterates_MH_fm:
   1.413 +  assumes is_F_iff_sats: 
   1.414 +      "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|] 
   1.415 +              ==> is_F(a,b) <->
   1.416 +                  sats(A, p(1,0), Cons(b, Cons(a, Cons(c, Cons(d,env)))))"
   1.417 +  shows 
   1.418 +      "[|v \<in> nat; x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
   1.419 +       ==> sats(A, iterates_MH_fm(p,v,x,y,z), env) <-> 
   1.420 +           iterates_MH(**A, is_F, nth(v,env), nth(x,env), nth(y,env), nth(z,env))"
   1.421 +by (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm 
   1.422 +              is_F_iff_sats [symmetric])
   1.423 +
   1.424 +lemma iterates_MH_iff_sats:
   1.425 +  "[| (!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|] 
   1.426 +              ==> is_F(a,b) <->
   1.427 +                  sats(A, p(1,0), Cons(b, Cons(a, Cons(c, Cons(d,env))))));
   1.428 +      nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.429 +      i' \<in> nat; i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
   1.430 +   ==> iterates_MH(**A, is_F, v, x, y, z) <-> 
   1.431 +       sats(A, iterates_MH_fm(p,i',i,j,k), env)"
   1.432 +apply (rule iff_sym) 
   1.433 +apply (rule iff_trans) 
   1.434 +apply (rule sats_iterates_MH_fm [of A is_F], blast, simp_all) 
   1.435 +done
   1.436 +
   1.437 +theorem iterates_MH_reflection:
   1.438 +  assumes p_reflection:
   1.439 +    "!!f g h. REFLECTS[\<lambda>x. p(L, f(x), g(x)), 
   1.440 +                     \<lambda>i x. p(**Lset(i), f(x), g(x))]"
   1.441 + shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L), e(x), f(x), g(x), h(x)), 
   1.442 +               \<lambda>i x. iterates_MH(**Lset(i), p(**Lset(i)), e(x), f(x), g(x), h(x))]"
   1.443 +apply (simp (no_asm_use) only: iterates_MH_def)
   1.444 +txt{*Must be careful: simplifying with @{text setclass_simps} above would
   1.445 +     change @{text "\<exists>gm[**Lset(i)]"} into @{text "\<exists>gm \<in> Lset(i)"}, when
   1.446 +     it would no longer match rule @{text is_nat_case_reflection}. *}
   1.447 +apply (rule is_nat_case_reflection) 
   1.448 +apply (simp (no_asm_use) only: setclass_simps)
   1.449 +apply (intro FOL_reflections function_reflections is_nat_case_reflection
   1.450 +             restriction_reflection p_reflection)  
   1.451 +done
   1.452 +
   1.453 +
   1.454 +
   1.455 +subsection{*@{term L} is Closed Under the Operator @{term list}*} 
   1.456 +
   1.457 +
   1.458 +lemma list_replacement1_Reflects:
   1.459 + "REFLECTS
   1.460 +   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
   1.461 +         is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)),
   1.462 +    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
   1.463 +         is_wfrec(**Lset(i), 
   1.464 +                  iterates_MH(**Lset(i), 
   1.465 +                          is_list_functor(**Lset(i), A), 0), memsn, u, y))]"
   1.466 +by (intro FOL_reflections function_reflections is_wfrec_reflection 
   1.467 +          iterates_MH_reflection list_functor_reflection) 
   1.468 +
   1.469 +lemma list_replacement1: 
   1.470 +   "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)"
   1.471 +apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
   1.472 +apply (rule strong_replacementI) 
   1.473 +apply (rule rallI)
   1.474 +apply (rename_tac B)   
   1.475 +apply (rule separation_CollectI) 
   1.476 +apply (insert nonempty) 
   1.477 +apply (subgoal_tac "L(Memrel(succ(n)))") 
   1.478 +apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast ) 
   1.479 +apply (rule ReflectsE [OF list_replacement1_Reflects], assumption)
   1.480 +apply (drule subset_Lset_ltD, assumption) 
   1.481 +apply (erule reflection_imp_L_separation)
   1.482 +  apply (simp_all add: lt_Ord2)
   1.483 +apply (rule DPowI2)
   1.484 +apply (rename_tac v) 
   1.485 +apply (rule bex_iff_sats conj_iff_sats)+
   1.486 +apply (rule_tac env = "[u,v,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
   1.487 +apply (rule sep_rules | simp)+
   1.488 +txt{*Can't get sat rules to work for higher-order operators, so just expand them!*}
   1.489 +apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   1.490 +apply (rule sep_rules list_functor_iff_sats quasinat_iff_sats | simp)+
   1.491 +apply (simp_all add: succ_Un_distrib [symmetric] Memrel_closed)
   1.492 +done
   1.493 +
   1.494 +
   1.495 +lemma list_replacement2_Reflects:
   1.496 + "REFLECTS
   1.497 +   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
   1.498 +         (\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and>
   1.499 +           is_wfrec (L, iterates_MH (L, is_list_functor(L, A), 0),
   1.500 +                              msn, u, x)),
   1.501 +    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
   1.502 +         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). 
   1.503 +          successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
   1.504 +           is_wfrec (**Lset(i), 
   1.505 +                 iterates_MH (**Lset(i), is_list_functor(**Lset(i), A), 0),
   1.506 +                     msn, u, x))]"
   1.507 +by (intro FOL_reflections function_reflections is_wfrec_reflection 
   1.508 +          iterates_MH_reflection list_functor_reflection) 
   1.509 +
   1.510 +
   1.511 +lemma list_replacement2: 
   1.512 +   "L(A) ==> strong_replacement(L, 
   1.513 +         \<lambda>n y. n\<in>nat & 
   1.514 +               (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
   1.515 +               is_wfrec(L, iterates_MH(L,is_list_functor(L,A), 0), 
   1.516 +                        msn, n, y)))"
   1.517 +apply (rule strong_replacementI) 
   1.518 +apply (rule rallI)
   1.519 +apply (rename_tac B)   
   1.520 +apply (rule separation_CollectI) 
   1.521 +apply (insert nonempty) 
   1.522 +apply (rule_tac A="{A,B,z,0,nat}" in subset_LsetE) 
   1.523 +apply (blast intro: L_nat) 
   1.524 +apply (rule ReflectsE [OF list_replacement2_Reflects], assumption)
   1.525 +apply (drule subset_Lset_ltD, assumption) 
   1.526 +apply (erule reflection_imp_L_separation)
   1.527 +  apply (simp_all add: lt_Ord2)
   1.528 +apply (rule DPowI2)
   1.529 +apply (rename_tac v) 
   1.530 +apply (rule bex_iff_sats conj_iff_sats)+
   1.531 +apply (rule_tac env = "[u,v,A,B,0,nat]" in mem_iff_sats)
   1.532 +apply (rule sep_rules | simp)+
   1.533 +apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   1.534 +apply (rule sep_rules list_functor_iff_sats quasinat_iff_sats | simp)+
   1.535 +apply (simp_all add: succ_Un_distrib [symmetric] Memrel_closed)
   1.536 +done
   1.537 +
   1.538 +
   1.539 +
   1.540  end