src/ZF/Constructible/Rec_Separation.thy
changeset 13409 d4ea094c650e
parent 13398 1cadd412da48
child 13418 7c0ba9dba978
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Mon Jul 22 13:55:44 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Tue Jul 23 15:07:12 2002 +0200
     1.3 @@ -1124,6 +1124,239 @@
     1.4  declare eclose_abs [intro,simp]
     1.5  
     1.6  
     1.7 +subsection{*Internalized Forms of Data Structuring Operators*}
     1.8 +
     1.9 +subsubsection{*The Formula @{term is_Inl}, Internalized*}
    1.10 +
    1.11 +(*  is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z) *)
    1.12 +constdefs Inl_fm :: "[i,i]=>i"
    1.13 +    "Inl_fm(a,z) == Exists(And(empty_fm(0), pair_fm(0,succ(a),succ(z))))"
    1.14 +
    1.15 +lemma Inl_type [TC]:
    1.16 +     "[| x \<in> nat; z \<in> nat |] ==> Inl_fm(x,z) \<in> formula"
    1.17 +by (simp add: Inl_fm_def) 
    1.18 +
    1.19 +lemma sats_Inl_fm [simp]:
    1.20 +   "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
    1.21 +    ==> sats(A, Inl_fm(x,z), env) <-> is_Inl(**A, nth(x,env), nth(z,env))"
    1.22 +by (simp add: Inl_fm_def is_Inl_def)
    1.23 +
    1.24 +lemma Inl_iff_sats:
    1.25 +      "[| nth(i,env) = x; nth(k,env) = z; 
    1.26 +          i \<in> nat; k \<in> nat; env \<in> list(A)|]
    1.27 +       ==> is_Inl(**A, x, z) <-> sats(A, Inl_fm(i,k), env)"
    1.28 +by simp
    1.29 +
    1.30 +theorem Inl_reflection:
    1.31 +     "REFLECTS[\<lambda>x. is_Inl(L,f(x),h(x)), 
    1.32 +               \<lambda>i x. is_Inl(**Lset(i),f(x),h(x))]"
    1.33 +apply (simp only: is_Inl_def setclass_simps)
    1.34 +apply (intro FOL_reflections function_reflections)  
    1.35 +done
    1.36 +
    1.37 +
    1.38 +subsubsection{*The Formula @{term is_Inr}, Internalized*}
    1.39 +
    1.40 +(*  is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z) *)
    1.41 +constdefs Inr_fm :: "[i,i]=>i"
    1.42 +    "Inr_fm(a,z) == Exists(And(number1_fm(0), pair_fm(0,succ(a),succ(z))))"
    1.43 +
    1.44 +lemma Inr_type [TC]:
    1.45 +     "[| x \<in> nat; z \<in> nat |] ==> Inr_fm(x,z) \<in> formula"
    1.46 +by (simp add: Inr_fm_def) 
    1.47 +
    1.48 +lemma sats_Inr_fm [simp]:
    1.49 +   "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
    1.50 +    ==> sats(A, Inr_fm(x,z), env) <-> is_Inr(**A, nth(x,env), nth(z,env))"
    1.51 +by (simp add: Inr_fm_def is_Inr_def)
    1.52 +
    1.53 +lemma Inr_iff_sats:
    1.54 +      "[| nth(i,env) = x; nth(k,env) = z; 
    1.55 +          i \<in> nat; k \<in> nat; env \<in> list(A)|]
    1.56 +       ==> is_Inr(**A, x, z) <-> sats(A, Inr_fm(i,k), env)"
    1.57 +by simp
    1.58 +
    1.59 +theorem Inr_reflection:
    1.60 +     "REFLECTS[\<lambda>x. is_Inr(L,f(x),h(x)), 
    1.61 +               \<lambda>i x. is_Inr(**Lset(i),f(x),h(x))]"
    1.62 +apply (simp only: is_Inr_def setclass_simps)
    1.63 +apply (intro FOL_reflections function_reflections)  
    1.64 +done
    1.65 +
    1.66 +
    1.67 +subsubsection{*The Formula @{term is_Nil}, Internalized*}
    1.68 +
    1.69 +(* is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs) *)
    1.70 +
    1.71 +constdefs Nil_fm :: "i=>i"
    1.72 +    "Nil_fm(x) == Exists(And(empty_fm(0), Inl_fm(0,succ(x))))"
    1.73 + 
    1.74 +lemma Nil_type [TC]: "x \<in> nat ==> Nil_fm(x) \<in> formula"
    1.75 +by (simp add: Nil_fm_def) 
    1.76 +
    1.77 +lemma sats_Nil_fm [simp]:
    1.78 +   "[| x \<in> nat; env \<in> list(A)|]
    1.79 +    ==> sats(A, Nil_fm(x), env) <-> is_Nil(**A, nth(x,env))"
    1.80 +by (simp add: Nil_fm_def is_Nil_def)
    1.81 +
    1.82 +lemma Nil_iff_sats:
    1.83 +      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
    1.84 +       ==> is_Nil(**A, x) <-> sats(A, Nil_fm(i), env)"
    1.85 +by simp
    1.86 +
    1.87 +theorem Nil_reflection:
    1.88 +     "REFLECTS[\<lambda>x. is_Nil(L,f(x)), 
    1.89 +               \<lambda>i x. is_Nil(**Lset(i),f(x))]"
    1.90 +apply (simp only: is_Nil_def setclass_simps)
    1.91 +apply (intro FOL_reflections function_reflections Inl_reflection)  
    1.92 +done
    1.93 +
    1.94 +
    1.95 +subsubsection{*The Formula @{term is_Nil}, Internalized*}
    1.96  
    1.97  
    1.98 +(*  "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)" *)
    1.99 +constdefs Cons_fm :: "[i,i,i]=>i"
   1.100 +    "Cons_fm(a,l,Z) == 
   1.101 +       Exists(And(pair_fm(succ(a),succ(l),0), Inr_fm(0,succ(Z))))"
   1.102 +
   1.103 +lemma Cons_type [TC]:
   1.104 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Cons_fm(x,y,z) \<in> formula"
   1.105 +by (simp add: Cons_fm_def) 
   1.106 +
   1.107 +lemma sats_Cons_fm [simp]:
   1.108 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   1.109 +    ==> sats(A, Cons_fm(x,y,z), env) <-> 
   1.110 +       is_Cons(**A, nth(x,env), nth(y,env), nth(z,env))"
   1.111 +by (simp add: Cons_fm_def is_Cons_def)
   1.112 +
   1.113 +lemma Cons_iff_sats:
   1.114 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.115 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   1.116 +       ==>is_Cons(**A, x, y, z) <-> sats(A, Cons_fm(i,j,k), env)"
   1.117 +by simp
   1.118 +
   1.119 +theorem Cons_reflection:
   1.120 +     "REFLECTS[\<lambda>x. is_Cons(L,f(x),g(x),h(x)), 
   1.121 +               \<lambda>i x. is_Cons(**Lset(i),f(x),g(x),h(x))]"
   1.122 +apply (simp only: is_Cons_def setclass_simps)
   1.123 +apply (intro FOL_reflections pair_reflection Inr_reflection)  
   1.124 +done
   1.125 +
   1.126 +subsubsection{*The Formula @{term is_quasilist}, Internalized*}
   1.127 +
   1.128 +(* is_quasilist(M,xs) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))" *)
   1.129 +
   1.130 +constdefs quasilist_fm :: "i=>i"
   1.131 +    "quasilist_fm(x) == 
   1.132 +       Or(Nil_fm(x), Exists(Exists(Cons_fm(1,0,succ(succ(x))))))"
   1.133 + 
   1.134 +lemma quasilist_type [TC]: "x \<in> nat ==> quasilist_fm(x) \<in> formula"
   1.135 +by (simp add: quasilist_fm_def) 
   1.136 +
   1.137 +lemma sats_quasilist_fm [simp]:
   1.138 +   "[| x \<in> nat; env \<in> list(A)|]
   1.139 +    ==> sats(A, quasilist_fm(x), env) <-> is_quasilist(**A, nth(x,env))"
   1.140 +by (simp add: quasilist_fm_def is_quasilist_def)
   1.141 +
   1.142 +lemma quasilist_iff_sats:
   1.143 +      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
   1.144 +       ==> is_quasilist(**A, x) <-> sats(A, quasilist_fm(i), env)"
   1.145 +by simp
   1.146 +
   1.147 +theorem quasilist_reflection:
   1.148 +     "REFLECTS[\<lambda>x. is_quasilist(L,f(x)), 
   1.149 +               \<lambda>i x. is_quasilist(**Lset(i),f(x))]"
   1.150 +apply (simp only: is_quasilist_def setclass_simps)
   1.151 +apply (intro FOL_reflections Nil_reflection Cons_reflection)  
   1.152 +done
   1.153 +
   1.154 +
   1.155 +subsection{*Absoluteness for the Function @{term nth}*}
   1.156 +
   1.157 +
   1.158 +subsubsection{*The Formula @{term is_tl}, Internalized*}
   1.159 +
   1.160 +(*     "is_tl(M,xs,T) == 
   1.161 +       (is_Nil(M,xs) --> T=xs) &
   1.162 +       (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
   1.163 +       (is_quasilist(M,xs) | empty(M,T))" *)
   1.164 +constdefs tl_fm :: "[i,i]=>i"
   1.165 +    "tl_fm(xs,T) == 
   1.166 +       And(Implies(Nil_fm(xs), Equal(T,xs)),
   1.167 +           And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(T#+2,0)))),
   1.168 +               Or(quasilist_fm(xs), empty_fm(T))))"
   1.169 +
   1.170 +lemma tl_type [TC]:
   1.171 +     "[| x \<in> nat; y \<in> nat |] ==> tl_fm(x,y) \<in> formula"
   1.172 +by (simp add: tl_fm_def) 
   1.173 +
   1.174 +lemma sats_tl_fm [simp]:
   1.175 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   1.176 +    ==> sats(A, tl_fm(x,y), env) <-> is_tl(**A, nth(x,env), nth(y,env))"
   1.177 +by (simp add: tl_fm_def is_tl_def)
   1.178 +
   1.179 +lemma tl_iff_sats:
   1.180 +      "[| nth(i,env) = x; nth(j,env) = y;
   1.181 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
   1.182 +       ==> is_tl(**A, x, y) <-> sats(A, tl_fm(i,j), env)"
   1.183 +by simp
   1.184 +
   1.185 +theorem tl_reflection:
   1.186 +     "REFLECTS[\<lambda>x. is_tl(L,f(x),g(x)), 
   1.187 +               \<lambda>i x. is_tl(**Lset(i),f(x),g(x))]"
   1.188 +apply (simp only: is_tl_def setclass_simps)
   1.189 +apply (intro FOL_reflections Nil_reflection Cons_reflection
   1.190 +             quasilist_reflection empty_reflection)  
   1.191 +done
   1.192 +
   1.193 +
   1.194 +subsubsection{*An Instance of Replacement for @{term nth}*}
   1.195 +
   1.196 +lemma nth_replacement_Reflects:
   1.197 + "REFLECTS
   1.198 +   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
   1.199 +         is_wfrec(L, iterates_MH(L, is_tl(L), z), memsn, u, y)),
   1.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>
   1.201 +         is_wfrec(**Lset(i), 
   1.202 +                  iterates_MH(**Lset(i), 
   1.203 +                          is_tl(**Lset(i)), z), memsn, u, y))]"
   1.204 +by (intro FOL_reflections function_reflections is_wfrec_reflection 
   1.205 +          iterates_MH_reflection list_functor_reflection tl_reflection) 
   1.206 +
   1.207 +lemma nth_replacement: 
   1.208 +   "L(w) ==> iterates_replacement(L, %l t. is_tl(L,l,t), w)"
   1.209 +apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
   1.210 +apply (rule strong_replacementI) 
   1.211 +apply (rule rallI)   
   1.212 +apply (rule separation_CollectI) 
   1.213 +apply (subgoal_tac "L(Memrel(succ(n)))") 
   1.214 +apply (rule_tac A="{A,n,w,z,Memrel(succ(n))}" in subset_LsetE, blast ) 
   1.215 +apply (rule ReflectsE [OF nth_replacement_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,z,w,Memrel(succ(n))]" in mem_iff_sats)
   1.224 +apply (rule sep_rules | simp)+
   1.225 +apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   1.226 +apply (rule sep_rules quasinat_iff_sats tl_iff_sats | simp)+
   1.227 +done
   1.228 +
   1.229 +ML
   1.230 +{*
   1.231 +bind_thm ("nth_abs_lemma", datatypes_L (thm "M_datatypes.nth_abs"));
   1.232 +*}
   1.233 +
   1.234 +text{*Instantiating theorem @{text nth_abs} for @{term L}*}
   1.235 +lemma nth_abs [simp]:
   1.236 +     "[|L(A); n \<in> nat; l \<in> list(A); L(Z)|] 
   1.237 +      ==> is_nth(L,n,l,Z) <-> Z = nth(n,l)"
   1.238 +apply (rule nth_abs_lemma)
   1.239 +apply (blast intro: nth_replacement transL list_closed, assumption+)
   1.240 +done
   1.241 +
   1.242  end