src/ZF/Constructible/Rec_Separation.thy
changeset 13496 6f0c57def6d5
parent 13493 5aa68c051725
child 13503 d93f41fe35d2
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Tue Aug 13 12:16:14 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Tue Aug 13 17:42:34 2002 +0200
     1.3 @@ -2,13 +2,11 @@
     1.4      ID:         $Id$
     1.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6      Copyright   2002  University of Cambridge
     1.7 -
     1.8 -FIXME: define nth_fm and prove its "sats" theorem
     1.9  *)
    1.10  
    1.11  header {*Separation for Facts About Recursion*}
    1.12  
    1.13 -theory Rec_Separation = Separation + Datatype_absolute:
    1.14 +theory Rec_Separation = Separation + Internalize:
    1.15  
    1.16  text{*This theory proves all instances needed for locales @{text
    1.17  "M_trancl"}, @{text "M_wfrank"} and @{text "M_datatypes"}*}
    1.18 @@ -305,13 +303,7 @@
    1.19    "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
    1.20        i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
    1.21     ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)"
    1.22 -apply (rule iff_sym) 
    1.23 -apply (rule iff_trans)
    1.24 -apply (rule sats_is_recfun_fm [of A MH]) 
    1.25 -apply (rule MH_iff_sats, simp_all) 
    1.26 -done
    1.27 -(*FIXME: surely proof can be improved?*)
    1.28 -
    1.29 +by (simp add: sats_is_recfun_fm [OF MH_iff_sats]) 
    1.30  
    1.31  text{*The additional variable in the premise, namely @{term f'}, is essential.
    1.32  It lets @{term MH} depend upon @{term x}, which seems often necessary.
    1.33 @@ -754,28 +746,27 @@
    1.34  apply (simp_all add: setclass_def)
    1.35  done
    1.36  
    1.37 -
    1.38  lemma iterates_MH_iff_sats:
    1.39 -  "[| (!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
    1.40 +  assumes is_F_iff_sats:
    1.41 +      "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
    1.42                ==> is_F(a,b) <->
    1.43 -                  sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env))))));
    1.44 -      nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
    1.45 +                  sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env)))))"
    1.46 +  shows 
    1.47 +  "[| nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
    1.48        i' \<in> nat; i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
    1.49     ==> iterates_MH(**A, is_F, v, x, y, z) <->
    1.50         sats(A, iterates_MH_fm(p,i',i,j,k), env)"
    1.51 -apply (rule iff_sym) 
    1.52 -apply (rule iff_trans)
    1.53 -apply (rule sats_iterates_MH_fm [of A is_F], blast, simp_all) 
    1.54 -done
    1.55 -(*FIXME: surely proof can be improved?*)
    1.56 +by (simp add: sats_iterates_MH_fm [OF is_F_iff_sats]) 
    1.57  
    1.58 -
    1.59 +text{*The second argument of @{term p} gives it direct access to @{term x},
    1.60 +  which is essential for handling free variable references.  Without this
    1.61 +  argument, we cannot prove reflection for @{term list_N}.*}
    1.62  theorem iterates_MH_reflection:
    1.63    assumes p_reflection:
    1.64 -    "!!f g h. REFLECTS[\<lambda>x. p(L, f(x), g(x)),
    1.65 -                     \<lambda>i x. p(**Lset(i), f(x), g(x))]"
    1.66 - shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L), e(x), f(x), g(x), h(x)),
    1.67 -               \<lambda>i x. iterates_MH(**Lset(i), p(**Lset(i)), e(x), f(x), g(x), h(x))]"
    1.68 +    "!!f g h. REFLECTS[\<lambda>x. p(L, h(x), f(x), g(x)),
    1.69 +                     \<lambda>i x. p(**Lset(i), h(x), f(x), g(x))]"
    1.70 + shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L,x), e(x), f(x), g(x), h(x)),
    1.71 +               \<lambda>i x. iterates_MH(**Lset(i), p(**Lset(i),x), e(x), f(x), g(x), h(x))]"
    1.72  apply (simp (no_asm_use) only: iterates_MH_def)
    1.73  txt{*Must be careful: simplifying with @{text setclass_simps} above would
    1.74       change @{text "\<exists>gm[**Lset(i)]"} into @{text "\<exists>gm \<in> Lset(i)"}, when
    1.75 @@ -1035,229 +1026,6 @@
    1.76  for @{term "list(A)"}.  It was a cut-and-paste job! *}
    1.77  
    1.78  
    1.79 -subsection{*Internalized Forms of Data Structuring Operators*}
    1.80 -
    1.81 -subsubsection{*The Formula @{term is_Inl}, Internalized*}
    1.82 -
    1.83 -(*  is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z) *)
    1.84 -constdefs Inl_fm :: "[i,i]=>i"
    1.85 -    "Inl_fm(a,z) == Exists(And(empty_fm(0), pair_fm(0,succ(a),succ(z))))"
    1.86 -
    1.87 -lemma Inl_type [TC]:
    1.88 -     "[| x \<in> nat; z \<in> nat |] ==> Inl_fm(x,z) \<in> formula"
    1.89 -by (simp add: Inl_fm_def)
    1.90 -
    1.91 -lemma sats_Inl_fm [simp]:
    1.92 -   "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
    1.93 -    ==> sats(A, Inl_fm(x,z), env) <-> is_Inl(**A, nth(x,env), nth(z,env))"
    1.94 -by (simp add: Inl_fm_def is_Inl_def)
    1.95 -
    1.96 -lemma Inl_iff_sats:
    1.97 -      "[| nth(i,env) = x; nth(k,env) = z;
    1.98 -          i \<in> nat; k \<in> nat; env \<in> list(A)|]
    1.99 -       ==> is_Inl(**A, x, z) <-> sats(A, Inl_fm(i,k), env)"
   1.100 -by simp
   1.101 -
   1.102 -theorem Inl_reflection:
   1.103 -     "REFLECTS[\<lambda>x. is_Inl(L,f(x),h(x)),
   1.104 -               \<lambda>i x. is_Inl(**Lset(i),f(x),h(x))]"
   1.105 -apply (simp only: is_Inl_def setclass_simps)
   1.106 -apply (intro FOL_reflections function_reflections)
   1.107 -done
   1.108 -
   1.109 -
   1.110 -subsubsection{*The Formula @{term is_Inr}, Internalized*}
   1.111 -
   1.112 -(*  is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z) *)
   1.113 -constdefs Inr_fm :: "[i,i]=>i"
   1.114 -    "Inr_fm(a,z) == Exists(And(number1_fm(0), pair_fm(0,succ(a),succ(z))))"
   1.115 -
   1.116 -lemma Inr_type [TC]:
   1.117 -     "[| x \<in> nat; z \<in> nat |] ==> Inr_fm(x,z) \<in> formula"
   1.118 -by (simp add: Inr_fm_def)
   1.119 -
   1.120 -lemma sats_Inr_fm [simp]:
   1.121 -   "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
   1.122 -    ==> sats(A, Inr_fm(x,z), env) <-> is_Inr(**A, nth(x,env), nth(z,env))"
   1.123 -by (simp add: Inr_fm_def is_Inr_def)
   1.124 -
   1.125 -lemma Inr_iff_sats:
   1.126 -      "[| nth(i,env) = x; nth(k,env) = z;
   1.127 -          i \<in> nat; k \<in> nat; env \<in> list(A)|]
   1.128 -       ==> is_Inr(**A, x, z) <-> sats(A, Inr_fm(i,k), env)"
   1.129 -by simp
   1.130 -
   1.131 -theorem Inr_reflection:
   1.132 -     "REFLECTS[\<lambda>x. is_Inr(L,f(x),h(x)),
   1.133 -               \<lambda>i x. is_Inr(**Lset(i),f(x),h(x))]"
   1.134 -apply (simp only: is_Inr_def setclass_simps)
   1.135 -apply (intro FOL_reflections function_reflections)
   1.136 -done
   1.137 -
   1.138 -
   1.139 -subsubsection{*The Formula @{term is_Nil}, Internalized*}
   1.140 -
   1.141 -(* is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs) *)
   1.142 -
   1.143 -constdefs Nil_fm :: "i=>i"
   1.144 -    "Nil_fm(x) == Exists(And(empty_fm(0), Inl_fm(0,succ(x))))"
   1.145 -
   1.146 -lemma Nil_type [TC]: "x \<in> nat ==> Nil_fm(x) \<in> formula"
   1.147 -by (simp add: Nil_fm_def)
   1.148 -
   1.149 -lemma sats_Nil_fm [simp]:
   1.150 -   "[| x \<in> nat; env \<in> list(A)|]
   1.151 -    ==> sats(A, Nil_fm(x), env) <-> is_Nil(**A, nth(x,env))"
   1.152 -by (simp add: Nil_fm_def is_Nil_def)
   1.153 -
   1.154 -lemma Nil_iff_sats:
   1.155 -      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
   1.156 -       ==> is_Nil(**A, x) <-> sats(A, Nil_fm(i), env)"
   1.157 -by simp
   1.158 -
   1.159 -theorem Nil_reflection:
   1.160 -     "REFLECTS[\<lambda>x. is_Nil(L,f(x)),
   1.161 -               \<lambda>i x. is_Nil(**Lset(i),f(x))]"
   1.162 -apply (simp only: is_Nil_def setclass_simps)
   1.163 -apply (intro FOL_reflections function_reflections Inl_reflection)
   1.164 -done
   1.165 -
   1.166 -
   1.167 -subsubsection{*The Formula @{term is_Cons}, Internalized*}
   1.168 -
   1.169 -
   1.170 -(*  "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)" *)
   1.171 -constdefs Cons_fm :: "[i,i,i]=>i"
   1.172 -    "Cons_fm(a,l,Z) ==
   1.173 -       Exists(And(pair_fm(succ(a),succ(l),0), Inr_fm(0,succ(Z))))"
   1.174 -
   1.175 -lemma Cons_type [TC]:
   1.176 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Cons_fm(x,y,z) \<in> formula"
   1.177 -by (simp add: Cons_fm_def)
   1.178 -
   1.179 -lemma sats_Cons_fm [simp]:
   1.180 -   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   1.181 -    ==> sats(A, Cons_fm(x,y,z), env) <->
   1.182 -       is_Cons(**A, nth(x,env), nth(y,env), nth(z,env))"
   1.183 -by (simp add: Cons_fm_def is_Cons_def)
   1.184 -
   1.185 -lemma Cons_iff_sats:
   1.186 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   1.187 -          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   1.188 -       ==>is_Cons(**A, x, y, z) <-> sats(A, Cons_fm(i,j,k), env)"
   1.189 -by simp
   1.190 -
   1.191 -theorem Cons_reflection:
   1.192 -     "REFLECTS[\<lambda>x. is_Cons(L,f(x),g(x),h(x)),
   1.193 -               \<lambda>i x. is_Cons(**Lset(i),f(x),g(x),h(x))]"
   1.194 -apply (simp only: is_Cons_def setclass_simps)
   1.195 -apply (intro FOL_reflections pair_reflection Inr_reflection)
   1.196 -done
   1.197 -
   1.198 -subsubsection{*The Formula @{term is_quasilist}, Internalized*}
   1.199 -
   1.200 -(* is_quasilist(M,xs) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))" *)
   1.201 -
   1.202 -constdefs quasilist_fm :: "i=>i"
   1.203 -    "quasilist_fm(x) ==
   1.204 -       Or(Nil_fm(x), Exists(Exists(Cons_fm(1,0,succ(succ(x))))))"
   1.205 -
   1.206 -lemma quasilist_type [TC]: "x \<in> nat ==> quasilist_fm(x) \<in> formula"
   1.207 -by (simp add: quasilist_fm_def)
   1.208 -
   1.209 -lemma sats_quasilist_fm [simp]:
   1.210 -   "[| x \<in> nat; env \<in> list(A)|]
   1.211 -    ==> sats(A, quasilist_fm(x), env) <-> is_quasilist(**A, nth(x,env))"
   1.212 -by (simp add: quasilist_fm_def is_quasilist_def)
   1.213 -
   1.214 -lemma quasilist_iff_sats:
   1.215 -      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
   1.216 -       ==> is_quasilist(**A, x) <-> sats(A, quasilist_fm(i), env)"
   1.217 -by simp
   1.218 -
   1.219 -theorem quasilist_reflection:
   1.220 -     "REFLECTS[\<lambda>x. is_quasilist(L,f(x)),
   1.221 -               \<lambda>i x. is_quasilist(**Lset(i),f(x))]"
   1.222 -apply (simp only: is_quasilist_def setclass_simps)
   1.223 -apply (intro FOL_reflections Nil_reflection Cons_reflection)
   1.224 -done
   1.225 -
   1.226 -
   1.227 -subsection{*Absoluteness for the Function @{term nth}*}
   1.228 -
   1.229 -
   1.230 -subsubsection{*The Formula @{term is_hd}, Internalized*}
   1.231 -
   1.232 -(*   "is_hd(M,xs,H) == 
   1.233 -       (is_Nil(M,xs) --> empty(M,H)) &
   1.234 -       (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
   1.235 -       (is_quasilist(M,xs) | empty(M,H))" *)
   1.236 -constdefs hd_fm :: "[i,i]=>i"
   1.237 -    "hd_fm(xs,H) == 
   1.238 -       And(Implies(Nil_fm(xs), empty_fm(H)),
   1.239 -           And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(H#+2,1)))),
   1.240 -               Or(quasilist_fm(xs), empty_fm(H))))"
   1.241 -
   1.242 -lemma hd_type [TC]:
   1.243 -     "[| x \<in> nat; y \<in> nat |] ==> hd_fm(x,y) \<in> formula"
   1.244 -by (simp add: hd_fm_def) 
   1.245 -
   1.246 -lemma sats_hd_fm [simp]:
   1.247 -   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   1.248 -    ==> sats(A, hd_fm(x,y), env) <-> is_hd(**A, nth(x,env), nth(y,env))"
   1.249 -by (simp add: hd_fm_def is_hd_def)
   1.250 -
   1.251 -lemma hd_iff_sats:
   1.252 -      "[| nth(i,env) = x; nth(j,env) = y;
   1.253 -          i \<in> nat; j \<in> nat; env \<in> list(A)|]
   1.254 -       ==> is_hd(**A, x, y) <-> sats(A, hd_fm(i,j), env)"
   1.255 -by simp
   1.256 -
   1.257 -theorem hd_reflection:
   1.258 -     "REFLECTS[\<lambda>x. is_hd(L,f(x),g(x)), 
   1.259 -               \<lambda>i x. is_hd(**Lset(i),f(x),g(x))]"
   1.260 -apply (simp only: is_hd_def setclass_simps)
   1.261 -apply (intro FOL_reflections Nil_reflection Cons_reflection
   1.262 -             quasilist_reflection empty_reflection)  
   1.263 -done
   1.264 -
   1.265 -
   1.266 -subsubsection{*The Formula @{term is_tl}, Internalized*}
   1.267 -
   1.268 -(*     "is_tl(M,xs,T) ==
   1.269 -       (is_Nil(M,xs) --> T=xs) &
   1.270 -       (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
   1.271 -       (is_quasilist(M,xs) | empty(M,T))" *)
   1.272 -constdefs tl_fm :: "[i,i]=>i"
   1.273 -    "tl_fm(xs,T) ==
   1.274 -       And(Implies(Nil_fm(xs), Equal(T,xs)),
   1.275 -           And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(T#+2,0)))),
   1.276 -               Or(quasilist_fm(xs), empty_fm(T))))"
   1.277 -
   1.278 -lemma tl_type [TC]:
   1.279 -     "[| x \<in> nat; y \<in> nat |] ==> tl_fm(x,y) \<in> formula"
   1.280 -by (simp add: tl_fm_def)
   1.281 -
   1.282 -lemma sats_tl_fm [simp]:
   1.283 -   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   1.284 -    ==> sats(A, tl_fm(x,y), env) <-> is_tl(**A, nth(x,env), nth(y,env))"
   1.285 -by (simp add: tl_fm_def is_tl_def)
   1.286 -
   1.287 -lemma tl_iff_sats:
   1.288 -      "[| nth(i,env) = x; nth(j,env) = y;
   1.289 -          i \<in> nat; j \<in> nat; env \<in> list(A)|]
   1.290 -       ==> is_tl(**A, x, y) <-> sats(A, tl_fm(i,j), env)"
   1.291 -by simp
   1.292 -
   1.293 -theorem tl_reflection:
   1.294 -     "REFLECTS[\<lambda>x. is_tl(L,f(x),g(x)),
   1.295 -               \<lambda>i x. is_tl(**Lset(i),f(x),g(x))]"
   1.296 -apply (simp only: is_tl_def setclass_simps)
   1.297 -apply (intro FOL_reflections Nil_reflection Cons_reflection
   1.298 -             quasilist_reflection empty_reflection)
   1.299 -done
   1.300 -
   1.301 -
   1.302  subsubsection{*The Formula @{term is_nth}, Internalized*}
   1.303  
   1.304  (* "is_nth(M,n,l,Z) == 
   1.305 @@ -1299,14 +1067,6 @@
   1.306               iterates_MH_reflection hd_reflection tl_reflection) 
   1.307  done
   1.308  
   1.309 -theorem bool_of_o_reflection:
   1.310 -     "REFLECTS [P(L), \<lambda>i. P(**Lset(i))] ==>
   1.311 -      REFLECTS[\<lambda>x. is_bool_of_o(L, P(L,x), f(x)),  
   1.312 -               \<lambda>i x. is_bool_of_o(**Lset(i), P(**Lset(i),x), f(x))]"
   1.313 -apply (simp (no_asm) only: is_bool_of_o_def setclass_simps)
   1.314 -apply (intro FOL_reflections function_reflections, assumption+)
   1.315 -done
   1.316 -
   1.317  
   1.318  subsubsection{*An Instance of Replacement for @{term nth}*}
   1.319