author paulson Thu Jul 25 10:56:35 2002 +0200 (2002-07-25) changeset 13422 af9bc8d87a75 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.
```     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
```