Added the assumption nth_replacement to locale M_datatypes.
authorpaulson
Thu Jul 25 10:56:35 2002 +0200 (2002-07-25)
changeset 13422af9bc8d87a75
parent 13421 8fcdf4a26468
child 13423 7ec771711c09
Added the assumption nth_replacement to locale M_datatypes.
Moved up its proof to make it available for the instantiation of that locale.
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Rec_Separation.thy
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 24 22:15:55 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 25 10:56:35 2002 +0200
     1.3 @@ -379,7 +379,9 @@
     1.4                 (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
     1.5                 is_wfrec(M, iterates_MH(M,is_formula_functor(M), 0), 
     1.6                          msn, n, y)))"
     1.7 -
     1.8 +  and nth_replacement:
     1.9 +   "M(l) ==> iterates_replacement(M, %l t. is_tl(M,l,t), l)"
    1.10 +        
    1.11  
    1.12  subsubsection{*Absoluteness of the List Construction*}
    1.13  
    1.14 @@ -649,14 +651,13 @@
    1.15         is_hd(M,X,Z)"
    1.16   
    1.17  lemma (in M_datatypes) nth_abs [simp]:
    1.18 -     "[|iterates_replacement(M, %l t. is_tl(M,l,t), l);
    1.19 -        M(A); n \<in> nat; l \<in> list(A); M(Z)|] 
    1.20 +     "[|M(A); n \<in> nat; l \<in> list(A); M(Z)|] 
    1.21        ==> is_nth(M,n,l,Z) <-> Z = nth(n,l)"
    1.22  apply (subgoal_tac "M(l)") 
    1.23   prefer 2 apply (blast intro: transM)
    1.24  apply (simp add: is_nth_def nth_eq_hd_iterates_tl nat_into_M
    1.25                   tl'_closed iterates_tl'_closed 
    1.26 -                 iterates_abs [OF _ relativize1_tl])
    1.27 +                 iterates_abs [OF _ relativize1_tl] nth_replacement)
    1.28  done
    1.29  
    1.30  
     2.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 24 22:15:55 2002 +0200
     2.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Jul 25 10:56:35 2002 +0200
     2.3 @@ -996,134 +996,6 @@
     2.4  for @{term "list(A)"}.  It was a cut-and-paste job! *}
     2.5  
     2.6  
     2.7 -subsubsection{*Instantiating the locale @{text M_datatypes}*}
     2.8 -ML
     2.9 -{*
    2.10 -val list_replacement1 = thm "list_replacement1"; 
    2.11 -val list_replacement2 = thm "list_replacement2";
    2.12 -val formula_replacement1 = thm "formula_replacement1";
    2.13 -val formula_replacement2 = thm "formula_replacement2";
    2.14 -
    2.15 -val m_datatypes = [list_replacement1, list_replacement2, 
    2.16 -                   formula_replacement1, formula_replacement2];
    2.17 -
    2.18 -fun datatypes_L th =
    2.19 -    kill_flex_triv_prems (m_datatypes MRS (wfrank_L th));
    2.20 -
    2.21 -bind_thm ("list_closed", datatypes_L (thm "M_datatypes.list_closed"));
    2.22 -bind_thm ("formula_closed", datatypes_L (thm "M_datatypes.formula_closed"));
    2.23 -bind_thm ("list_abs", datatypes_L (thm "M_datatypes.list_abs"));
    2.24 -bind_thm ("formula_abs", datatypes_L (thm "M_datatypes.formula_abs"));
    2.25 -*}
    2.26 -
    2.27 -declare list_closed [intro,simp]
    2.28 -declare formula_closed [intro,simp]
    2.29 -declare list_abs [intro,simp]
    2.30 -declare formula_abs [intro,simp]
    2.31 -
    2.32 -
    2.33 -
    2.34 -subsection{*@{term L} is Closed Under the Operator @{term eclose}*} 
    2.35 -
    2.36 -subsubsection{*Instances of Replacement for @{term eclose}*}
    2.37 -
    2.38 -lemma eclose_replacement1_Reflects:
    2.39 - "REFLECTS
    2.40 -   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
    2.41 -         is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)),
    2.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>
    2.43 -         is_wfrec(**Lset(i), 
    2.44 -                  iterates_MH(**Lset(i), big_union(**Lset(i)), A), 
    2.45 -                  memsn, u, y))]"
    2.46 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
    2.47 -          iterates_MH_reflection) 
    2.48 -
    2.49 -lemma eclose_replacement1: 
    2.50 -   "L(A) ==> iterates_replacement(L, big_union(L), A)"
    2.51 -apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
    2.52 -apply (rule strong_replacementI) 
    2.53 -apply (rule rallI)
    2.54 -apply (rename_tac B)   
    2.55 -apply (rule separation_CollectI) 
    2.56 -apply (subgoal_tac "L(Memrel(succ(n)))") 
    2.57 -apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast ) 
    2.58 -apply (rule ReflectsE [OF eclose_replacement1_Reflects], assumption)
    2.59 -apply (drule subset_Lset_ltD, assumption) 
    2.60 -apply (erule reflection_imp_L_separation)
    2.61 -  apply (simp_all add: lt_Ord2 Memrel_closed)
    2.62 -apply (elim conjE) 
    2.63 -apply (rule DPow_LsetI)
    2.64 -apply (rename_tac v) 
    2.65 -apply (rule bex_iff_sats conj_iff_sats)+
    2.66 -apply (rule_tac env = "[u,v,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
    2.67 -apply (rule sep_rules | simp)+
    2.68 -txt{*Can't get sat rules to work for higher-order operators, so just expand them!*}
    2.69 -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
    2.70 -apply (rule sep_rules big_union_iff_sats quasinat_iff_sats | simp)+
    2.71 -done
    2.72 -
    2.73 -
    2.74 -lemma eclose_replacement2_Reflects:
    2.75 - "REFLECTS
    2.76 -   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
    2.77 -         (\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and>
    2.78 -           is_wfrec (L, iterates_MH (L, big_union(L), A),
    2.79 -                              msn, u, x)),
    2.80 -    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
    2.81 -         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). 
    2.82 -          successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
    2.83 -           is_wfrec (**Lset(i), 
    2.84 -                 iterates_MH (**Lset(i), big_union(**Lset(i)), A),
    2.85 -                     msn, u, x))]"
    2.86 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
    2.87 -          iterates_MH_reflection) 
    2.88 -
    2.89 -
    2.90 -lemma eclose_replacement2: 
    2.91 -   "L(A) ==> strong_replacement(L, 
    2.92 -         \<lambda>n y. n\<in>nat & 
    2.93 -               (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
    2.94 -               is_wfrec(L, iterates_MH(L,big_union(L), A), 
    2.95 -                        msn, n, y)))"
    2.96 -apply (rule strong_replacementI) 
    2.97 -apply (rule rallI)
    2.98 -apply (rename_tac B)   
    2.99 -apply (rule separation_CollectI) 
   2.100 -apply (rule_tac A="{A,B,z,nat}" in subset_LsetE) 
   2.101 -apply (blast intro: L_nat) 
   2.102 -apply (rule ReflectsE [OF eclose_replacement2_Reflects], assumption)
   2.103 -apply (drule subset_Lset_ltD, assumption) 
   2.104 -apply (erule reflection_imp_L_separation)
   2.105 -  apply (simp_all add: lt_Ord2)
   2.106 -apply (rule DPow_LsetI)
   2.107 -apply (rename_tac v) 
   2.108 -apply (rule bex_iff_sats conj_iff_sats)+
   2.109 -apply (rule_tac env = "[u,v,A,B,nat]" in mem_iff_sats)
   2.110 -apply (rule sep_rules | simp)+
   2.111 -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   2.112 -apply (rule sep_rules big_union_iff_sats quasinat_iff_sats | simp)+
   2.113 -done
   2.114 -
   2.115 -
   2.116 -subsubsection{*Instantiating the locale @{text M_eclose}*}
   2.117 -ML
   2.118 -{*
   2.119 -val eclose_replacement1 = thm "eclose_replacement1"; 
   2.120 -val eclose_replacement2 = thm "eclose_replacement2";
   2.121 -
   2.122 -val m_eclose = [eclose_replacement1, eclose_replacement2];
   2.123 -
   2.124 -fun eclose_L th =
   2.125 -    kill_flex_triv_prems (m_eclose MRS (datatypes_L th));
   2.126 -
   2.127 -bind_thm ("eclose_closed", eclose_L (thm "M_eclose.eclose_closed"));
   2.128 -bind_thm ("eclose_abs", eclose_L (thm "M_eclose.eclose_abs"));
   2.129 -*}
   2.130 -
   2.131 -declare eclose_closed [intro,simp]
   2.132 -declare eclose_abs [intro,simp]
   2.133 -
   2.134 -
   2.135  subsection{*Internalized Forms of Data Structuring Operators*}
   2.136  
   2.137  subsubsection{*The Formula @{term is_Inl}, Internalized*}
   2.138 @@ -1212,7 +1084,7 @@
   2.139  done
   2.140  
   2.141  
   2.142 -subsubsection{*The Formula @{term is_Nil}, Internalized*}
   2.143 +subsubsection{*The Formula @{term is_Cons}, Internalized*}
   2.144  
   2.145  
   2.146  (*  "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)" *)
   2.147 @@ -1346,17 +1218,138 @@
   2.148  apply (rule sep_rules quasinat_iff_sats tl_iff_sats | simp)+
   2.149  done
   2.150  
   2.151 +
   2.152 +
   2.153 +subsubsection{*Instantiating the locale @{text M_datatypes}*}
   2.154  ML
   2.155  {*
   2.156 -bind_thm ("nth_abs_lemma", datatypes_L (thm "M_datatypes.nth_abs"));
   2.157 +val list_replacement1 = thm "list_replacement1"; 
   2.158 +val list_replacement2 = thm "list_replacement2";
   2.159 +val formula_replacement1 = thm "formula_replacement1";
   2.160 +val formula_replacement2 = thm "formula_replacement2";
   2.161 +val nth_replacement = thm "nth_replacement";
   2.162 +
   2.163 +val m_datatypes = [list_replacement1, list_replacement2, 
   2.164 +                   formula_replacement1, formula_replacement2, 
   2.165 +                   nth_replacement];
   2.166 +
   2.167 +fun datatypes_L th =
   2.168 +    kill_flex_triv_prems (m_datatypes MRS (wfrank_L th));
   2.169 +
   2.170 +bind_thm ("list_closed", datatypes_L (thm "M_datatypes.list_closed"));
   2.171 +bind_thm ("formula_closed", datatypes_L (thm "M_datatypes.formula_closed"));
   2.172 +bind_thm ("list_abs", datatypes_L (thm "M_datatypes.list_abs"));
   2.173 +bind_thm ("formula_abs", datatypes_L (thm "M_datatypes.formula_abs"));
   2.174 +bind_thm ("nth_abs", datatypes_L (thm "M_datatypes.nth_abs"));
   2.175  *}
   2.176  
   2.177 -text{*Instantiating theorem @{text nth_abs} for @{term L}*}
   2.178 -lemma nth_abs [simp]:
   2.179 -     "[|L(A); n \<in> nat; l \<in> list(A); L(Z)|] 
   2.180 -      ==> is_nth(L,n,l,Z) <-> Z = nth(n,l)"
   2.181 -apply (rule nth_abs_lemma)
   2.182 -apply (blast intro: nth_replacement transL list_closed, assumption+)
   2.183 +declare list_closed [intro,simp]
   2.184 +declare formula_closed [intro,simp]
   2.185 +declare list_abs [simp]
   2.186 +declare formula_abs [simp]
   2.187 +declare nth_abs [simp]
   2.188 +
   2.189 +
   2.190 +
   2.191 +subsection{*@{term L} is Closed Under the Operator @{term eclose}*} 
   2.192 +
   2.193 +subsubsection{*Instances of Replacement for @{term eclose}*}
   2.194 +
   2.195 +lemma eclose_replacement1_Reflects:
   2.196 + "REFLECTS
   2.197 +   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
   2.198 +         is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)),
   2.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>
   2.200 +         is_wfrec(**Lset(i), 
   2.201 +                  iterates_MH(**Lset(i), big_union(**Lset(i)), A), 
   2.202 +                  memsn, u, y))]"
   2.203 +by (intro FOL_reflections function_reflections is_wfrec_reflection 
   2.204 +          iterates_MH_reflection) 
   2.205 +
   2.206 +lemma eclose_replacement1: 
   2.207 +   "L(A) ==> iterates_replacement(L, big_union(L), A)"
   2.208 +apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
   2.209 +apply (rule strong_replacementI) 
   2.210 +apply (rule rallI)
   2.211 +apply (rename_tac B)   
   2.212 +apply (rule separation_CollectI) 
   2.213 +apply (subgoal_tac "L(Memrel(succ(n)))") 
   2.214 +apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast ) 
   2.215 +apply (rule ReflectsE [OF eclose_replacement1_Reflects], assumption)
   2.216 +apply (drule subset_Lset_ltD, assumption) 
   2.217 +apply (erule reflection_imp_L_separation)
   2.218 +  apply (simp_all add: lt_Ord2 Memrel_closed)
   2.219 +apply (elim conjE) 
   2.220 +apply (rule DPow_LsetI)
   2.221 +apply (rename_tac v) 
   2.222 +apply (rule bex_iff_sats conj_iff_sats)+
   2.223 +apply (rule_tac env = "[u,v,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
   2.224 +apply (rule sep_rules | simp)+
   2.225 +txt{*Can't get sat rules to work for higher-order operators, so just expand them!*}
   2.226 +apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   2.227 +apply (rule sep_rules big_union_iff_sats quasinat_iff_sats | simp)+
   2.228  done
   2.229  
   2.230 +
   2.231 +lemma eclose_replacement2_Reflects:
   2.232 + "REFLECTS
   2.233 +   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
   2.234 +         (\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and>
   2.235 +           is_wfrec (L, iterates_MH (L, big_union(L), A),
   2.236 +                              msn, u, x)),
   2.237 +    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
   2.238 +         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). 
   2.239 +          successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
   2.240 +           is_wfrec (**Lset(i), 
   2.241 +                 iterates_MH (**Lset(i), big_union(**Lset(i)), A),
   2.242 +                     msn, u, x))]"
   2.243 +by (intro FOL_reflections function_reflections is_wfrec_reflection 
   2.244 +          iterates_MH_reflection) 
   2.245 +
   2.246 +
   2.247 +lemma eclose_replacement2: 
   2.248 +   "L(A) ==> strong_replacement(L, 
   2.249 +         \<lambda>n y. n\<in>nat & 
   2.250 +               (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
   2.251 +               is_wfrec(L, iterates_MH(L,big_union(L), A), 
   2.252 +                        msn, n, y)))"
   2.253 +apply (rule strong_replacementI) 
   2.254 +apply (rule rallI)
   2.255 +apply (rename_tac B)   
   2.256 +apply (rule separation_CollectI) 
   2.257 +apply (rule_tac A="{A,B,z,nat}" in subset_LsetE) 
   2.258 +apply (blast intro: L_nat) 
   2.259 +apply (rule ReflectsE [OF eclose_replacement2_Reflects], assumption)
   2.260 +apply (drule subset_Lset_ltD, assumption) 
   2.261 +apply (erule reflection_imp_L_separation)
   2.262 +  apply (simp_all add: lt_Ord2)
   2.263 +apply (rule DPow_LsetI)
   2.264 +apply (rename_tac v) 
   2.265 +apply (rule bex_iff_sats conj_iff_sats)+
   2.266 +apply (rule_tac env = "[u,v,A,B,nat]" in mem_iff_sats)
   2.267 +apply (rule sep_rules | simp)+
   2.268 +apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   2.269 +apply (rule sep_rules big_union_iff_sats quasinat_iff_sats | simp)+
   2.270 +done
   2.271 +
   2.272 +
   2.273 +subsubsection{*Instantiating the locale @{text M_eclose}*}
   2.274 +ML
   2.275 +{*
   2.276 +val eclose_replacement1 = thm "eclose_replacement1"; 
   2.277 +val eclose_replacement2 = thm "eclose_replacement2";
   2.278 +
   2.279 +val m_eclose = [eclose_replacement1, eclose_replacement2];
   2.280 +
   2.281 +fun eclose_L th =
   2.282 +    kill_flex_triv_prems (m_eclose MRS (datatypes_L th));
   2.283 +
   2.284 +bind_thm ("eclose_closed", eclose_L (thm "M_eclose.eclose_closed"));
   2.285 +bind_thm ("eclose_abs", eclose_L (thm "M_eclose.eclose_abs"));
   2.286 +*}
   2.287 +
   2.288 +declare eclose_closed [intro,simp]
   2.289 +declare eclose_abs [intro,simp]
   2.290 +
   2.291 +
   2.292  end