author paulson Tue Jul 23 15:07:12 2002 +0200 (2002-07-23) changeset 13409 d4ea094c650e parent 13408 024af54a625c child 13410 f2cd09766864
Relativization and Separation for the function "nth"
```     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Mon Jul 22 13:55:44 2002 +0200
1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Tue Jul 23 15:07:12 2002 +0200
1.3 @@ -321,9 +321,9 @@
1.4    "l \<in> list(A) ==>
1.5     list_rec(a,g,l) =
1.6     transrec (succ(length(l)),
1.7 -      \<lambda>x h. Lambda (list_N(A,x),
1.8 -             list_case' (a,
1.9 -                \<lambda>a l. g(a, l, h ` succ(length(l)) ` l)))) ` l"
1.10 +      \<lambda>x h. Lambda (list(A),
1.11 +                    list_case' (a,
1.12 +                           \<lambda>a l. g(a, l, h ` succ(length(l)) ` l)))) ` l"
1.13  apply (induct_tac l)
1.14  apply (subst transrec, simp)
1.15  apply (subst transrec)
1.16 @@ -629,10 +629,6 @@
1.17  apply (simp add: tl'_Cons tl'_closed)
1.18  done
1.19
1.20 -locale (open) M_nth = M_datatypes +
1.21 - assumes nth_replacement1:
1.22 -   "M(xs) ==> iterates_replacement(M, %l t. is_tl(M,l,t), xs)"
1.23 -
1.24  text{*Immediate by type-checking*}
1.25  lemma (in M_datatypes) nth_closed [intro,simp]:
1.26       "[|xs \<in> list(A); n \<in> nat; M(A)|] ==> M(nth(n,xs))"
1.27 @@ -649,20 +645,18 @@
1.28         is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) &
1.29         is_hd(M,X,Z)"
1.30
1.31 -lemma (in M_nth) nth_abs [simp]:
1.32 -     "[|M(A); n \<in> nat; l \<in> list(A); M(Z)|]
1.33 +lemma (in M_datatypes) nth_abs [simp]:
1.34 +     "[|iterates_replacement(M, %l t. is_tl(M,l,t), l);
1.35 +        M(A); n \<in> nat; l \<in> list(A); M(Z)|]
1.36        ==> is_nth(M,n,l,Z) <-> Z = nth(n,l)"
1.37  apply (subgoal_tac "M(l)")
1.38   prefer 2 apply (blast intro: transM)
1.39 -apply (insert nth_replacement1)
1.40  apply (simp add: is_nth_def nth_eq_hd_iterates_tl nat_into_M
1.41                   tl'_closed iterates_tl'_closed
1.42                   iterates_abs [OF _ relativize1_tl])
1.43  done
1.44
1.45
1.46 -
1.47 -
1.48  subsection{*Relativization and Absoluteness for the @{term formula} Constructors*}
1.49
1.50  constdefs
1.51 @@ -912,35 +906,29 @@
1.52                       le_imp_subset formula_N_mono)
1.53  done
1.54
1.55 -lemma Nand_in_formula_N:
1.56 -    "[|p \<in> formula; q \<in> formula|]
1.57 -     ==> Nand(p,q) \<in> formula_N(succ(succ(depth(p))) \<union> succ(succ(depth(q))))"
1.58 -by (simp add: succ_Un_distrib [symmetric] formula_imp_formula_N le_Un_iff)
1.59 -
1.60 -
1.61  text{*Express @{term formula_rec} without using @{term rank} or @{term Vset},
1.62  neither of which is absolute.*}
1.63  lemma (in M_triv_axioms) formula_rec_eq:
1.64    "p \<in> formula ==>
1.65     formula_rec(a,b,c,d,p) =
1.66     transrec (succ(depth(p)),
1.67 -      \<lambda>x h. Lambda (formula_N(x),
1.68 +      \<lambda>x h. Lambda (formula,
1.69               formula_case' (a, b,
1.70                  \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u,
1.71                                h ` succ(depth(v)) ` v),
1.72                  \<lambda>u. d(u, h ` succ(depth(u)) ` u))))
1.73     ` p"
1.74  apply (induct_tac p)
1.75 -txt{*Base case for @{term Member}*}
1.76 -apply (subst transrec, simp)
1.77 -txt{*Base case for @{term Equal}*}
1.78 -apply (subst transrec, simp)
1.79 -txt{*Inductive step for @{term Nand}*}
1.80 -apply (subst transrec)
1.81 -apply (simp add: succ_Un_distrib Nand_in_formula_N)
1.82 +   txt{*Base case for @{term Member}*}
1.83 +   apply (subst transrec, simp add: formula.intros)
1.84 +  txt{*Base case for @{term Equal}*}
1.85 +  apply (subst transrec, simp add: formula.intros)
1.86 + txt{*Inductive step for @{term Nand}*}
1.87 + apply (subst transrec)
1.88 + apply (simp add: succ_Un_distrib formula.intros)
1.89  txt{*Inductive step for @{term Forall}*}
1.90  apply (subst transrec)
1.91 -apply (simp add: formula_imp_formula_N)
1.92 +apply (simp add: formula_imp_formula_N formula.intros)
1.93  done
1.94
1.95
```
```     2.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Mon Jul 22 13:55:44 2002 +0200
2.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Tue Jul 23 15:07:12 2002 +0200
2.3 @@ -1124,6 +1124,239 @@
2.4  declare eclose_abs [intro,simp]
2.5
2.6
2.7 +subsection{*Internalized Forms of Data Structuring Operators*}
2.8 +
2.9 +subsubsection{*The Formula @{term is_Inl}, Internalized*}
2.10 +
2.11 +(*  is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z) *)
2.12 +constdefs Inl_fm :: "[i,i]=>i"
2.13 +    "Inl_fm(a,z) == Exists(And(empty_fm(0), pair_fm(0,succ(a),succ(z))))"
2.14 +
2.15 +lemma Inl_type [TC]:
2.16 +     "[| x \<in> nat; z \<in> nat |] ==> Inl_fm(x,z) \<in> formula"
2.17 +by (simp add: Inl_fm_def)
2.18 +
2.19 +lemma sats_Inl_fm [simp]:
2.20 +   "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
2.21 +    ==> sats(A, Inl_fm(x,z), env) <-> is_Inl(**A, nth(x,env), nth(z,env))"
2.22 +by (simp add: Inl_fm_def is_Inl_def)
2.23 +
2.24 +lemma Inl_iff_sats:
2.25 +      "[| nth(i,env) = x; nth(k,env) = z;
2.26 +          i \<in> nat; k \<in> nat; env \<in> list(A)|]
2.27 +       ==> is_Inl(**A, x, z) <-> sats(A, Inl_fm(i,k), env)"
2.28 +by simp
2.29 +
2.30 +theorem Inl_reflection:
2.31 +     "REFLECTS[\<lambda>x. is_Inl(L,f(x),h(x)),
2.32 +               \<lambda>i x. is_Inl(**Lset(i),f(x),h(x))]"
2.33 +apply (simp only: is_Inl_def setclass_simps)
2.34 +apply (intro FOL_reflections function_reflections)
2.35 +done
2.36 +
2.37 +
2.38 +subsubsection{*The Formula @{term is_Inr}, Internalized*}
2.39 +
2.40 +(*  is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z) *)
2.41 +constdefs Inr_fm :: "[i,i]=>i"
2.42 +    "Inr_fm(a,z) == Exists(And(number1_fm(0), pair_fm(0,succ(a),succ(z))))"
2.43 +
2.44 +lemma Inr_type [TC]:
2.45 +     "[| x \<in> nat; z \<in> nat |] ==> Inr_fm(x,z) \<in> formula"
2.46 +by (simp add: Inr_fm_def)
2.47 +
2.48 +lemma sats_Inr_fm [simp]:
2.49 +   "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
2.50 +    ==> sats(A, Inr_fm(x,z), env) <-> is_Inr(**A, nth(x,env), nth(z,env))"
2.51 +by (simp add: Inr_fm_def is_Inr_def)
2.52 +
2.53 +lemma Inr_iff_sats:
2.54 +      "[| nth(i,env) = x; nth(k,env) = z;
2.55 +          i \<in> nat; k \<in> nat; env \<in> list(A)|]
2.56 +       ==> is_Inr(**A, x, z) <-> sats(A, Inr_fm(i,k), env)"
2.57 +by simp
2.58 +
2.59 +theorem Inr_reflection:
2.60 +     "REFLECTS[\<lambda>x. is_Inr(L,f(x),h(x)),
2.61 +               \<lambda>i x. is_Inr(**Lset(i),f(x),h(x))]"
2.62 +apply (simp only: is_Inr_def setclass_simps)
2.63 +apply (intro FOL_reflections function_reflections)
2.64 +done
2.65 +
2.66 +
2.67 +subsubsection{*The Formula @{term is_Nil}, Internalized*}
2.68 +
2.69 +(* is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs) *)
2.70 +
2.71 +constdefs Nil_fm :: "i=>i"
2.72 +    "Nil_fm(x) == Exists(And(empty_fm(0), Inl_fm(0,succ(x))))"
2.73 +
2.74 +lemma Nil_type [TC]: "x \<in> nat ==> Nil_fm(x) \<in> formula"
2.75 +by (simp add: Nil_fm_def)
2.76 +
2.77 +lemma sats_Nil_fm [simp]:
2.78 +   "[| x \<in> nat; env \<in> list(A)|]
2.79 +    ==> sats(A, Nil_fm(x), env) <-> is_Nil(**A, nth(x,env))"
2.80 +by (simp add: Nil_fm_def is_Nil_def)
2.81 +
2.82 +lemma Nil_iff_sats:
2.83 +      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
2.84 +       ==> is_Nil(**A, x) <-> sats(A, Nil_fm(i), env)"
2.85 +by simp
2.86 +
2.87 +theorem Nil_reflection:
2.88 +     "REFLECTS[\<lambda>x. is_Nil(L,f(x)),
2.89 +               \<lambda>i x. is_Nil(**Lset(i),f(x))]"
2.90 +apply (simp only: is_Nil_def setclass_simps)
2.91 +apply (intro FOL_reflections function_reflections Inl_reflection)
2.92 +done
2.93 +
2.94 +
2.95 +subsubsection{*The Formula @{term is_Nil}, Internalized*}
2.96
2.97
2.98 +(*  "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)" *)
2.99 +constdefs Cons_fm :: "[i,i,i]=>i"
2.100 +    "Cons_fm(a,l,Z) ==
2.101 +       Exists(And(pair_fm(succ(a),succ(l),0), Inr_fm(0,succ(Z))))"
2.102 +
2.103 +lemma Cons_type [TC]:
2.104 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Cons_fm(x,y,z) \<in> formula"
2.105 +by (simp add: Cons_fm_def)
2.106 +
2.107 +lemma sats_Cons_fm [simp]:
2.108 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
2.109 +    ==> sats(A, Cons_fm(x,y,z), env) <->
2.110 +       is_Cons(**A, nth(x,env), nth(y,env), nth(z,env))"
2.111 +by (simp add: Cons_fm_def is_Cons_def)
2.112 +
2.113 +lemma Cons_iff_sats:
2.114 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
2.115 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
2.116 +       ==>is_Cons(**A, x, y, z) <-> sats(A, Cons_fm(i,j,k), env)"
2.117 +by simp
2.118 +
2.119 +theorem Cons_reflection:
2.120 +     "REFLECTS[\<lambda>x. is_Cons(L,f(x),g(x),h(x)),
2.121 +               \<lambda>i x. is_Cons(**Lset(i),f(x),g(x),h(x))]"
2.122 +apply (simp only: is_Cons_def setclass_simps)
2.123 +apply (intro FOL_reflections pair_reflection Inr_reflection)
2.124 +done
2.125 +
2.126 +subsubsection{*The Formula @{term is_quasilist}, Internalized*}
2.127 +
2.128 +(* is_quasilist(M,xs) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))" *)
2.129 +
2.130 +constdefs quasilist_fm :: "i=>i"
2.131 +    "quasilist_fm(x) ==
2.132 +       Or(Nil_fm(x), Exists(Exists(Cons_fm(1,0,succ(succ(x))))))"
2.133 +
2.134 +lemma quasilist_type [TC]: "x \<in> nat ==> quasilist_fm(x) \<in> formula"
2.135 +by (simp add: quasilist_fm_def)
2.136 +
2.137 +lemma sats_quasilist_fm [simp]:
2.138 +   "[| x \<in> nat; env \<in> list(A)|]
2.139 +    ==> sats(A, quasilist_fm(x), env) <-> is_quasilist(**A, nth(x,env))"
2.140 +by (simp add: quasilist_fm_def is_quasilist_def)
2.141 +
2.142 +lemma quasilist_iff_sats:
2.143 +      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
2.144 +       ==> is_quasilist(**A, x) <-> sats(A, quasilist_fm(i), env)"
2.145 +by simp
2.146 +
2.147 +theorem quasilist_reflection:
2.148 +     "REFLECTS[\<lambda>x. is_quasilist(L,f(x)),
2.149 +               \<lambda>i x. is_quasilist(**Lset(i),f(x))]"
2.150 +apply (simp only: is_quasilist_def setclass_simps)
2.151 +apply (intro FOL_reflections Nil_reflection Cons_reflection)
2.152 +done
2.153 +
2.154 +
2.155 +subsection{*Absoluteness for the Function @{term nth}*}
2.156 +
2.157 +
2.158 +subsubsection{*The Formula @{term is_tl}, Internalized*}
2.159 +
2.160 +(*     "is_tl(M,xs,T) ==
2.161 +       (is_Nil(M,xs) --> T=xs) &
2.162 +       (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
2.163 +       (is_quasilist(M,xs) | empty(M,T))" *)
2.164 +constdefs tl_fm :: "[i,i]=>i"
2.165 +    "tl_fm(xs,T) ==
2.166 +       And(Implies(Nil_fm(xs), Equal(T,xs)),
2.167 +           And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(T#+2,0)))),
2.168 +               Or(quasilist_fm(xs), empty_fm(T))))"
2.169 +
2.170 +lemma tl_type [TC]:
2.171 +     "[| x \<in> nat; y \<in> nat |] ==> tl_fm(x,y) \<in> formula"
2.172 +by (simp add: tl_fm_def)
2.173 +
2.174 +lemma sats_tl_fm [simp]:
2.175 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
2.176 +    ==> sats(A, tl_fm(x,y), env) <-> is_tl(**A, nth(x,env), nth(y,env))"
2.177 +by (simp add: tl_fm_def is_tl_def)
2.178 +
2.179 +lemma tl_iff_sats:
2.180 +      "[| nth(i,env) = x; nth(j,env) = y;
2.181 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
2.182 +       ==> is_tl(**A, x, y) <-> sats(A, tl_fm(i,j), env)"
2.183 +by simp
2.184 +
2.185 +theorem tl_reflection:
2.186 +     "REFLECTS[\<lambda>x. is_tl(L,f(x),g(x)),
2.187 +               \<lambda>i x. is_tl(**Lset(i),f(x),g(x))]"
2.188 +apply (simp only: is_tl_def setclass_simps)
2.189 +apply (intro FOL_reflections Nil_reflection Cons_reflection
2.190 +             quasilist_reflection empty_reflection)
2.191 +done
2.192 +
2.193 +
2.194 +subsubsection{*An Instance of Replacement for @{term nth}*}
2.195 +
2.196 +lemma nth_replacement_Reflects:
2.197 + "REFLECTS
2.198 +   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
2.199 +         is_wfrec(L, iterates_MH(L, is_tl(L), z), memsn, u, y)),
2.200 +    \<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.201 +         is_wfrec(**Lset(i),
2.202 +                  iterates_MH(**Lset(i),
2.203 +                          is_tl(**Lset(i)), z), memsn, u, y))]"
2.204 +by (intro FOL_reflections function_reflections is_wfrec_reflection
2.205 +          iterates_MH_reflection list_functor_reflection tl_reflection)
2.206 +
2.207 +lemma nth_replacement:
2.208 +   "L(w) ==> iterates_replacement(L, %l t. is_tl(L,l,t), w)"
2.209 +apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
2.210 +apply (rule strong_replacementI)
2.211 +apply (rule rallI)
2.212 +apply (rule separation_CollectI)
2.213 +apply (subgoal_tac "L(Memrel(succ(n)))")
2.214 +apply (rule_tac A="{A,n,w,z,Memrel(succ(n))}" in subset_LsetE, blast )
2.215 +apply (rule ReflectsE [OF nth_replacement_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,z,w,Memrel(succ(n))]" in mem_iff_sats)
2.224 +apply (rule sep_rules | simp)+
2.225 +apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
2.226 +apply (rule sep_rules quasinat_iff_sats tl_iff_sats | simp)+
2.227 +done
2.228 +
2.229 +ML
2.230 +{*
2.231 +bind_thm ("nth_abs_lemma", datatypes_L (thm "M_datatypes.nth_abs"));
2.232 +*}
2.233 +
2.234 +text{*Instantiating theorem @{text nth_abs} for @{term L}*}
2.235 +lemma nth_abs [simp]:
2.236 +     "[|L(A); n \<in> nat; l \<in> list(A); L(Z)|]
2.237 +      ==> is_nth(L,n,l,Z) <-> Z = nth(n,l)"
2.238 +apply (rule nth_abs_lemma)
2.239 +apply (blast intro: nth_replacement transL list_closed, assumption+)
2.240 +done
2.241 +
2.242  end
```