Relativization and Separation for the function "nth"
authorpaulson
Tue Jul 23 15:07:12 2002 +0200 (2002-07-23)
changeset 13409d4ea094c650e
parent 13408 024af54a625c
child 13410 f2cd09766864
Relativization and Separation for the function "nth"
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Rec_Separation.thy
     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