src/ZF/Constructible/Rec_Separation.thy
changeset 13422 af9bc8d87a75
parent 13418 7c0ba9dba978
child 13428 99e52e78eb65
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 24 22:15:55 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Jul 25 10:56:35 2002 +0200
     1.3 @@ -996,134 +996,6 @@
     1.4  for @{term "list(A)"}.  It was a cut-and-paste job! *}
     1.5  
     1.6  
     1.7 -subsubsection{*Instantiating the locale @{text M_datatypes}*}
     1.8 -ML
     1.9 -{*
    1.10 -val list_replacement1 = thm "list_replacement1"; 
    1.11 -val list_replacement2 = thm "list_replacement2";
    1.12 -val formula_replacement1 = thm "formula_replacement1";
    1.13 -val formula_replacement2 = thm "formula_replacement2";
    1.14 -
    1.15 -val m_datatypes = [list_replacement1, list_replacement2, 
    1.16 -                   formula_replacement1, formula_replacement2];
    1.17 -
    1.18 -fun datatypes_L th =
    1.19 -    kill_flex_triv_prems (m_datatypes MRS (wfrank_L th));
    1.20 -
    1.21 -bind_thm ("list_closed", datatypes_L (thm "M_datatypes.list_closed"));
    1.22 -bind_thm ("formula_closed", datatypes_L (thm "M_datatypes.formula_closed"));
    1.23 -bind_thm ("list_abs", datatypes_L (thm "M_datatypes.list_abs"));
    1.24 -bind_thm ("formula_abs", datatypes_L (thm "M_datatypes.formula_abs"));
    1.25 -*}
    1.26 -
    1.27 -declare list_closed [intro,simp]
    1.28 -declare formula_closed [intro,simp]
    1.29 -declare list_abs [intro,simp]
    1.30 -declare formula_abs [intro,simp]
    1.31 -
    1.32 -
    1.33 -
    1.34 -subsection{*@{term L} is Closed Under the Operator @{term eclose}*} 
    1.35 -
    1.36 -subsubsection{*Instances of Replacement for @{term eclose}*}
    1.37 -
    1.38 -lemma eclose_replacement1_Reflects:
    1.39 - "REFLECTS
    1.40 -   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
    1.41 -         is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)),
    1.42 -    \<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.43 -         is_wfrec(**Lset(i), 
    1.44 -                  iterates_MH(**Lset(i), big_union(**Lset(i)), A), 
    1.45 -                  memsn, u, y))]"
    1.46 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
    1.47 -          iterates_MH_reflection) 
    1.48 -
    1.49 -lemma eclose_replacement1: 
    1.50 -   "L(A) ==> iterates_replacement(L, big_union(L), A)"
    1.51 -apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
    1.52 -apply (rule strong_replacementI) 
    1.53 -apply (rule rallI)
    1.54 -apply (rename_tac B)   
    1.55 -apply (rule separation_CollectI) 
    1.56 -apply (subgoal_tac "L(Memrel(succ(n)))") 
    1.57 -apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast ) 
    1.58 -apply (rule ReflectsE [OF eclose_replacement1_Reflects], assumption)
    1.59 -apply (drule subset_Lset_ltD, assumption) 
    1.60 -apply (erule reflection_imp_L_separation)
    1.61 -  apply (simp_all add: lt_Ord2 Memrel_closed)
    1.62 -apply (elim conjE) 
    1.63 -apply (rule DPow_LsetI)
    1.64 -apply (rename_tac v) 
    1.65 -apply (rule bex_iff_sats conj_iff_sats)+
    1.66 -apply (rule_tac env = "[u,v,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
    1.67 -apply (rule sep_rules | simp)+
    1.68 -txt{*Can't get sat rules to work for higher-order operators, so just expand them!*}
    1.69 -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
    1.70 -apply (rule sep_rules big_union_iff_sats quasinat_iff_sats | simp)+
    1.71 -done
    1.72 -
    1.73 -
    1.74 -lemma eclose_replacement2_Reflects:
    1.75 - "REFLECTS
    1.76 -   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
    1.77 -         (\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and>
    1.78 -           is_wfrec (L, iterates_MH (L, big_union(L), A),
    1.79 -                              msn, u, x)),
    1.80 -    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
    1.81 -         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). 
    1.82 -          successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
    1.83 -           is_wfrec (**Lset(i), 
    1.84 -                 iterates_MH (**Lset(i), big_union(**Lset(i)), A),
    1.85 -                     msn, u, x))]"
    1.86 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
    1.87 -          iterates_MH_reflection) 
    1.88 -
    1.89 -
    1.90 -lemma eclose_replacement2: 
    1.91 -   "L(A) ==> strong_replacement(L, 
    1.92 -         \<lambda>n y. n\<in>nat & 
    1.93 -               (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
    1.94 -               is_wfrec(L, iterates_MH(L,big_union(L), A), 
    1.95 -                        msn, n, y)))"
    1.96 -apply (rule strong_replacementI) 
    1.97 -apply (rule rallI)
    1.98 -apply (rename_tac B)   
    1.99 -apply (rule separation_CollectI) 
   1.100 -apply (rule_tac A="{A,B,z,nat}" in subset_LsetE) 
   1.101 -apply (blast intro: L_nat) 
   1.102 -apply (rule ReflectsE [OF eclose_replacement2_Reflects], assumption)
   1.103 -apply (drule subset_Lset_ltD, assumption) 
   1.104 -apply (erule reflection_imp_L_separation)
   1.105 -  apply (simp_all add: lt_Ord2)
   1.106 -apply (rule DPow_LsetI)
   1.107 -apply (rename_tac v) 
   1.108 -apply (rule bex_iff_sats conj_iff_sats)+
   1.109 -apply (rule_tac env = "[u,v,A,B,nat]" in mem_iff_sats)
   1.110 -apply (rule sep_rules | simp)+
   1.111 -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   1.112 -apply (rule sep_rules big_union_iff_sats quasinat_iff_sats | simp)+
   1.113 -done
   1.114 -
   1.115 -
   1.116 -subsubsection{*Instantiating the locale @{text M_eclose}*}
   1.117 -ML
   1.118 -{*
   1.119 -val eclose_replacement1 = thm "eclose_replacement1"; 
   1.120 -val eclose_replacement2 = thm "eclose_replacement2";
   1.121 -
   1.122 -val m_eclose = [eclose_replacement1, eclose_replacement2];
   1.123 -
   1.124 -fun eclose_L th =
   1.125 -    kill_flex_triv_prems (m_eclose MRS (datatypes_L th));
   1.126 -
   1.127 -bind_thm ("eclose_closed", eclose_L (thm "M_eclose.eclose_closed"));
   1.128 -bind_thm ("eclose_abs", eclose_L (thm "M_eclose.eclose_abs"));
   1.129 -*}
   1.130 -
   1.131 -declare eclose_closed [intro,simp]
   1.132 -declare eclose_abs [intro,simp]
   1.133 -
   1.134 -
   1.135  subsection{*Internalized Forms of Data Structuring Operators*}
   1.136  
   1.137  subsubsection{*The Formula @{term is_Inl}, Internalized*}
   1.138 @@ -1212,7 +1084,7 @@
   1.139  done
   1.140  
   1.141  
   1.142 -subsubsection{*The Formula @{term is_Nil}, Internalized*}
   1.143 +subsubsection{*The Formula @{term is_Cons}, Internalized*}
   1.144  
   1.145  
   1.146  (*  "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)" *)
   1.147 @@ -1346,17 +1218,138 @@
   1.148  apply (rule sep_rules quasinat_iff_sats tl_iff_sats | simp)+
   1.149  done
   1.150  
   1.151 +
   1.152 +
   1.153 +subsubsection{*Instantiating the locale @{text M_datatypes}*}
   1.154  ML
   1.155  {*
   1.156 -bind_thm ("nth_abs_lemma", datatypes_L (thm "M_datatypes.nth_abs"));
   1.157 +val list_replacement1 = thm "list_replacement1"; 
   1.158 +val list_replacement2 = thm "list_replacement2";
   1.159 +val formula_replacement1 = thm "formula_replacement1";
   1.160 +val formula_replacement2 = thm "formula_replacement2";
   1.161 +val nth_replacement = thm "nth_replacement";
   1.162 +
   1.163 +val m_datatypes = [list_replacement1, list_replacement2, 
   1.164 +                   formula_replacement1, formula_replacement2, 
   1.165 +                   nth_replacement];
   1.166 +
   1.167 +fun datatypes_L th =
   1.168 +    kill_flex_triv_prems (m_datatypes MRS (wfrank_L th));
   1.169 +
   1.170 +bind_thm ("list_closed", datatypes_L (thm "M_datatypes.list_closed"));
   1.171 +bind_thm ("formula_closed", datatypes_L (thm "M_datatypes.formula_closed"));
   1.172 +bind_thm ("list_abs", datatypes_L (thm "M_datatypes.list_abs"));
   1.173 +bind_thm ("formula_abs", datatypes_L (thm "M_datatypes.formula_abs"));
   1.174 +bind_thm ("nth_abs", datatypes_L (thm "M_datatypes.nth_abs"));
   1.175  *}
   1.176  
   1.177 -text{*Instantiating theorem @{text nth_abs} for @{term L}*}
   1.178 -lemma nth_abs [simp]:
   1.179 -     "[|L(A); n \<in> nat; l \<in> list(A); L(Z)|] 
   1.180 -      ==> is_nth(L,n,l,Z) <-> Z = nth(n,l)"
   1.181 -apply (rule nth_abs_lemma)
   1.182 -apply (blast intro: nth_replacement transL list_closed, assumption+)
   1.183 +declare list_closed [intro,simp]
   1.184 +declare formula_closed [intro,simp]
   1.185 +declare list_abs [simp]
   1.186 +declare formula_abs [simp]
   1.187 +declare nth_abs [simp]
   1.188 +
   1.189 +
   1.190 +
   1.191 +subsection{*@{term L} is Closed Under the Operator @{term eclose}*} 
   1.192 +
   1.193 +subsubsection{*Instances of Replacement for @{term eclose}*}
   1.194 +
   1.195 +lemma eclose_replacement1_Reflects:
   1.196 + "REFLECTS
   1.197 +   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
   1.198 +         is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)),
   1.199 +    \<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.200 +         is_wfrec(**Lset(i), 
   1.201 +                  iterates_MH(**Lset(i), big_union(**Lset(i)), A), 
   1.202 +                  memsn, u, y))]"
   1.203 +by (intro FOL_reflections function_reflections is_wfrec_reflection 
   1.204 +          iterates_MH_reflection) 
   1.205 +
   1.206 +lemma eclose_replacement1: 
   1.207 +   "L(A) ==> iterates_replacement(L, big_union(L), A)"
   1.208 +apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
   1.209 +apply (rule strong_replacementI) 
   1.210 +apply (rule rallI)
   1.211 +apply (rename_tac B)   
   1.212 +apply (rule separation_CollectI) 
   1.213 +apply (subgoal_tac "L(Memrel(succ(n)))") 
   1.214 +apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast ) 
   1.215 +apply (rule ReflectsE [OF eclose_replacement1_Reflects], assumption)
   1.216 +apply (drule subset_Lset_ltD, assumption) 
   1.217 +apply (erule reflection_imp_L_separation)
   1.218 +  apply (simp_all add: lt_Ord2 Memrel_closed)
   1.219 +apply (elim conjE) 
   1.220 +apply (rule DPow_LsetI)
   1.221 +apply (rename_tac v) 
   1.222 +apply (rule bex_iff_sats conj_iff_sats)+
   1.223 +apply (rule_tac env = "[u,v,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
   1.224 +apply (rule sep_rules | simp)+
   1.225 +txt{*Can't get sat rules to work for higher-order operators, so just expand them!*}
   1.226 +apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   1.227 +apply (rule sep_rules big_union_iff_sats quasinat_iff_sats | simp)+
   1.228  done
   1.229  
   1.230 +
   1.231 +lemma eclose_replacement2_Reflects:
   1.232 + "REFLECTS
   1.233 +   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
   1.234 +         (\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and>
   1.235 +           is_wfrec (L, iterates_MH (L, big_union(L), A),
   1.236 +                              msn, u, x)),
   1.237 +    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
   1.238 +         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). 
   1.239 +          successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
   1.240 +           is_wfrec (**Lset(i), 
   1.241 +                 iterates_MH (**Lset(i), big_union(**Lset(i)), A),
   1.242 +                     msn, u, x))]"
   1.243 +by (intro FOL_reflections function_reflections is_wfrec_reflection 
   1.244 +          iterates_MH_reflection) 
   1.245 +
   1.246 +
   1.247 +lemma eclose_replacement2: 
   1.248 +   "L(A) ==> strong_replacement(L, 
   1.249 +         \<lambda>n y. n\<in>nat & 
   1.250 +               (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
   1.251 +               is_wfrec(L, iterates_MH(L,big_union(L), A), 
   1.252 +                        msn, n, y)))"
   1.253 +apply (rule strong_replacementI) 
   1.254 +apply (rule rallI)
   1.255 +apply (rename_tac B)   
   1.256 +apply (rule separation_CollectI) 
   1.257 +apply (rule_tac A="{A,B,z,nat}" in subset_LsetE) 
   1.258 +apply (blast intro: L_nat) 
   1.259 +apply (rule ReflectsE [OF eclose_replacement2_Reflects], assumption)
   1.260 +apply (drule subset_Lset_ltD, assumption) 
   1.261 +apply (erule reflection_imp_L_separation)
   1.262 +  apply (simp_all add: lt_Ord2)
   1.263 +apply (rule DPow_LsetI)
   1.264 +apply (rename_tac v) 
   1.265 +apply (rule bex_iff_sats conj_iff_sats)+
   1.266 +apply (rule_tac env = "[u,v,A,B,nat]" in mem_iff_sats)
   1.267 +apply (rule sep_rules | simp)+
   1.268 +apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   1.269 +apply (rule sep_rules big_union_iff_sats quasinat_iff_sats | simp)+
   1.270 +done
   1.271 +
   1.272 +
   1.273 +subsubsection{*Instantiating the locale @{text M_eclose}*}
   1.274 +ML
   1.275 +{*
   1.276 +val eclose_replacement1 = thm "eclose_replacement1"; 
   1.277 +val eclose_replacement2 = thm "eclose_replacement2";
   1.278 +
   1.279 +val m_eclose = [eclose_replacement1, eclose_replacement2];
   1.280 +
   1.281 +fun eclose_L th =
   1.282 +    kill_flex_triv_prems (m_eclose MRS (datatypes_L th));
   1.283 +
   1.284 +bind_thm ("eclose_closed", eclose_L (thm "M_eclose.eclose_closed"));
   1.285 +bind_thm ("eclose_abs", eclose_L (thm "M_eclose.eclose_abs"));
   1.286 +*}
   1.287 +
   1.288 +declare eclose_closed [intro,simp]
   1.289 +declare eclose_abs [intro,simp]
   1.290 +
   1.291 +
   1.292  end