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.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.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.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.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.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.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.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.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.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
```