author paulson Tue Aug 13 17:42:34 2002 +0200 (2002-08-13) changeset 13496 6f0c57def6d5 parent 13495 af27202d6d1c child 13497 defb74f6a5bc
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
the new theory Internalize.thy
 src/ZF/Constructible/Internalize.thy file | annotate | diff | revisions src/ZF/Constructible/L_axioms.thy file | annotate | diff | revisions src/ZF/Constructible/Rec_Separation.thy file | annotate | diff | revisions src/ZF/Constructible/Satisfies_absolute.thy file | annotate | diff | revisions src/ZF/IsaMakefile file | annotate | diff | revisions
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/ZF/Constructible/Internalize.thy	Tue Aug 13 17:42:34 2002 +0200
1.3 @@ -0,0 +1,559 @@
1.4 +theory Internalize = L_axioms + Datatype_absolute:
1.5 +
1.6 +subsection{*Internalized Forms of Data Structuring Operators*}
1.7 +
1.8 +subsubsection{*The Formula @{term is_Inl}, Internalized*}
1.9 +
1.10 +(*  is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z) *)
1.11 +constdefs Inl_fm :: "[i,i]=>i"
1.12 +    "Inl_fm(a,z) == Exists(And(empty_fm(0), pair_fm(0,succ(a),succ(z))))"
1.13 +
1.14 +lemma Inl_type [TC]:
1.15 +     "[| x \<in> nat; z \<in> nat |] ==> Inl_fm(x,z) \<in> formula"
1.17 +
1.18 +lemma sats_Inl_fm [simp]:
1.19 +   "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
1.20 +    ==> sats(A, Inl_fm(x,z), env) <-> is_Inl(**A, nth(x,env), nth(z,env))"
1.21 +by (simp add: Inl_fm_def is_Inl_def)
1.22 +
1.23 +lemma Inl_iff_sats:
1.24 +      "[| nth(i,env) = x; nth(k,env) = z;
1.25 +          i \<in> nat; k \<in> nat; env \<in> list(A)|]
1.26 +       ==> is_Inl(**A, x, z) <-> sats(A, Inl_fm(i,k), env)"
1.27 +by simp
1.28 +
1.29 +theorem Inl_reflection:
1.30 +     "REFLECTS[\<lambda>x. is_Inl(L,f(x),h(x)),
1.31 +               \<lambda>i x. is_Inl(**Lset(i),f(x),h(x))]"
1.32 +apply (simp only: is_Inl_def setclass_simps)
1.33 +apply (intro FOL_reflections function_reflections)
1.34 +done
1.35 +
1.36 +
1.37 +subsubsection{*The Formula @{term is_Inr}, Internalized*}
1.38 +
1.39 +(*  is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z) *)
1.40 +constdefs Inr_fm :: "[i,i]=>i"
1.41 +    "Inr_fm(a,z) == Exists(And(number1_fm(0), pair_fm(0,succ(a),succ(z))))"
1.42 +
1.43 +lemma Inr_type [TC]:
1.44 +     "[| x \<in> nat; z \<in> nat |] ==> Inr_fm(x,z) \<in> formula"
1.46 +
1.47 +lemma sats_Inr_fm [simp]:
1.48 +   "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
1.49 +    ==> sats(A, Inr_fm(x,z), env) <-> is_Inr(**A, nth(x,env), nth(z,env))"
1.50 +by (simp add: Inr_fm_def is_Inr_def)
1.51 +
1.52 +lemma Inr_iff_sats:
1.53 +      "[| nth(i,env) = x; nth(k,env) = z;
1.54 +          i \<in> nat; k \<in> nat; env \<in> list(A)|]
1.55 +       ==> is_Inr(**A, x, z) <-> sats(A, Inr_fm(i,k), env)"
1.56 +by simp
1.57 +
1.58 +theorem Inr_reflection:
1.59 +     "REFLECTS[\<lambda>x. is_Inr(L,f(x),h(x)),
1.60 +               \<lambda>i x. is_Inr(**Lset(i),f(x),h(x))]"
1.61 +apply (simp only: is_Inr_def setclass_simps)
1.62 +apply (intro FOL_reflections function_reflections)
1.63 +done
1.64 +
1.65 +
1.66 +subsubsection{*The Formula @{term is_Nil}, Internalized*}
1.67 +
1.68 +(* is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs) *)
1.69 +
1.70 +constdefs Nil_fm :: "i=>i"
1.71 +    "Nil_fm(x) == Exists(And(empty_fm(0), Inl_fm(0,succ(x))))"
1.72 +
1.73 +lemma Nil_type [TC]: "x \<in> nat ==> Nil_fm(x) \<in> formula"
1.75 +
1.76 +lemma sats_Nil_fm [simp]:
1.77 +   "[| x \<in> nat; env \<in> list(A)|]
1.78 +    ==> sats(A, Nil_fm(x), env) <-> is_Nil(**A, nth(x,env))"
1.79 +by (simp add: Nil_fm_def is_Nil_def)
1.80 +
1.81 +lemma Nil_iff_sats:
1.82 +      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
1.83 +       ==> is_Nil(**A, x) <-> sats(A, Nil_fm(i), env)"
1.84 +by simp
1.85 +
1.86 +theorem Nil_reflection:
1.87 +     "REFLECTS[\<lambda>x. is_Nil(L,f(x)),
1.88 +               \<lambda>i x. is_Nil(**Lset(i),f(x))]"
1.89 +apply (simp only: is_Nil_def setclass_simps)
1.90 +apply (intro FOL_reflections function_reflections Inl_reflection)
1.91 +done
1.92 +
1.93 +
1.94 +subsubsection{*The Formula @{term is_Cons}, Internalized*}
1.95 +
1.96 +
1.97 +(*  "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)" *)
1.98 +constdefs Cons_fm :: "[i,i,i]=>i"
1.99 +    "Cons_fm(a,l,Z) ==
1.100 +       Exists(And(pair_fm(succ(a),succ(l),0), Inr_fm(0,succ(Z))))"
1.101 +
1.102 +lemma Cons_type [TC]:
1.103 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Cons_fm(x,y,z) \<in> formula"
1.105 +
1.106 +lemma sats_Cons_fm [simp]:
1.107 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.108 +    ==> sats(A, Cons_fm(x,y,z), env) <->
1.109 +       is_Cons(**A, nth(x,env), nth(y,env), nth(z,env))"
1.110 +by (simp add: Cons_fm_def is_Cons_def)
1.111 +
1.112 +lemma Cons_iff_sats:
1.113 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.114 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.115 +       ==>is_Cons(**A, x, y, z) <-> sats(A, Cons_fm(i,j,k), env)"
1.116 +by simp
1.117 +
1.118 +theorem Cons_reflection:
1.119 +     "REFLECTS[\<lambda>x. is_Cons(L,f(x),g(x),h(x)),
1.120 +               \<lambda>i x. is_Cons(**Lset(i),f(x),g(x),h(x))]"
1.121 +apply (simp only: is_Cons_def setclass_simps)
1.122 +apply (intro FOL_reflections pair_reflection Inr_reflection)
1.123 +done
1.124 +
1.125 +subsubsection{*The Formula @{term is_quasilist}, Internalized*}
1.126 +
1.127 +(* is_quasilist(M,xs) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))" *)
1.128 +
1.129 +constdefs quasilist_fm :: "i=>i"
1.130 +    "quasilist_fm(x) ==
1.131 +       Or(Nil_fm(x), Exists(Exists(Cons_fm(1,0,succ(succ(x))))))"
1.132 +
1.133 +lemma quasilist_type [TC]: "x \<in> nat ==> quasilist_fm(x) \<in> formula"
1.135 +
1.136 +lemma sats_quasilist_fm [simp]:
1.137 +   "[| x \<in> nat; env \<in> list(A)|]
1.138 +    ==> sats(A, quasilist_fm(x), env) <-> is_quasilist(**A, nth(x,env))"
1.139 +by (simp add: quasilist_fm_def is_quasilist_def)
1.140 +
1.141 +lemma quasilist_iff_sats:
1.142 +      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
1.143 +       ==> is_quasilist(**A, x) <-> sats(A, quasilist_fm(i), env)"
1.144 +by simp
1.145 +
1.146 +theorem quasilist_reflection:
1.147 +     "REFLECTS[\<lambda>x. is_quasilist(L,f(x)),
1.148 +               \<lambda>i x. is_quasilist(**Lset(i),f(x))]"
1.149 +apply (simp only: is_quasilist_def setclass_simps)
1.150 +apply (intro FOL_reflections Nil_reflection Cons_reflection)
1.151 +done
1.152 +
1.153 +
1.154 +subsection{*Absoluteness for the Function @{term nth}*}
1.155 +
1.156 +
1.157 +subsubsection{*The Formula @{term is_hd}, Internalized*}
1.158 +
1.159 +(*   "is_hd(M,xs,H) ==
1.160 +       (is_Nil(M,xs) --> empty(M,H)) &
1.161 +       (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
1.162 +       (is_quasilist(M,xs) | empty(M,H))" *)
1.163 +constdefs hd_fm :: "[i,i]=>i"
1.164 +    "hd_fm(xs,H) ==
1.165 +       And(Implies(Nil_fm(xs), empty_fm(H)),
1.166 +           And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(H#+2,1)))),
1.167 +               Or(quasilist_fm(xs), empty_fm(H))))"
1.168 +
1.169 +lemma hd_type [TC]:
1.170 +     "[| x \<in> nat; y \<in> nat |] ==> hd_fm(x,y) \<in> formula"
1.172 +
1.173 +lemma sats_hd_fm [simp]:
1.174 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
1.175 +    ==> sats(A, hd_fm(x,y), env) <-> is_hd(**A, nth(x,env), nth(y,env))"
1.176 +by (simp add: hd_fm_def is_hd_def)
1.177 +
1.178 +lemma hd_iff_sats:
1.179 +      "[| nth(i,env) = x; nth(j,env) = y;
1.180 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
1.181 +       ==> is_hd(**A, x, y) <-> sats(A, hd_fm(i,j), env)"
1.182 +by simp
1.183 +
1.184 +theorem hd_reflection:
1.185 +     "REFLECTS[\<lambda>x. is_hd(L,f(x),g(x)),
1.186 +               \<lambda>i x. is_hd(**Lset(i),f(x),g(x))]"
1.187 +apply (simp only: is_hd_def setclass_simps)
1.188 +apply (intro FOL_reflections Nil_reflection Cons_reflection
1.189 +             quasilist_reflection empty_reflection)
1.190 +done
1.191 +
1.192 +
1.193 +subsubsection{*The Formula @{term is_tl}, Internalized*}
1.194 +
1.195 +(*     "is_tl(M,xs,T) ==
1.196 +       (is_Nil(M,xs) --> T=xs) &
1.197 +       (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
1.198 +       (is_quasilist(M,xs) | empty(M,T))" *)
1.199 +constdefs tl_fm :: "[i,i]=>i"
1.200 +    "tl_fm(xs,T) ==
1.201 +       And(Implies(Nil_fm(xs), Equal(T,xs)),
1.202 +           And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(T#+2,0)))),
1.203 +               Or(quasilist_fm(xs), empty_fm(T))))"
1.204 +
1.205 +lemma tl_type [TC]:
1.206 +     "[| x \<in> nat; y \<in> nat |] ==> tl_fm(x,y) \<in> formula"
1.208 +
1.209 +lemma sats_tl_fm [simp]:
1.210 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
1.211 +    ==> sats(A, tl_fm(x,y), env) <-> is_tl(**A, nth(x,env), nth(y,env))"
1.212 +by (simp add: tl_fm_def is_tl_def)
1.213 +
1.214 +lemma tl_iff_sats:
1.215 +      "[| nth(i,env) = x; nth(j,env) = y;
1.216 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
1.217 +       ==> is_tl(**A, x, y) <-> sats(A, tl_fm(i,j), env)"
1.218 +by simp
1.219 +
1.220 +theorem tl_reflection:
1.221 +     "REFLECTS[\<lambda>x. is_tl(L,f(x),g(x)),
1.222 +               \<lambda>i x. is_tl(**Lset(i),f(x),g(x))]"
1.223 +apply (simp only: is_tl_def setclass_simps)
1.224 +apply (intro FOL_reflections Nil_reflection Cons_reflection
1.225 +             quasilist_reflection empty_reflection)
1.226 +done
1.227 +
1.228 +
1.229 +subsubsection{*The Operator @{term is_bool_of_o}*}
1.230 +
1.231 +(*   is_bool_of_o :: "[i=>o, o, i] => o"
1.232 +   "is_bool_of_o(M,P,z) == (P & number1(M,z)) | (~P & empty(M,z))" *)
1.233 +
1.234 +text{*The formula @{term p} has no free variables.*}
1.235 +constdefs bool_of_o_fm :: "[i, i]=>i"
1.236 + "bool_of_o_fm(p,z) ==
1.237 +    Or(And(p,number1_fm(z)),
1.238 +       And(Neg(p),empty_fm(z)))"
1.239 +
1.240 +lemma is_bool_of_o_type [TC]:
1.241 +     "[| p \<in> formula; z \<in> nat |] ==> bool_of_o_fm(p,z) \<in> formula"
1.243 +
1.244 +lemma sats_bool_of_o_fm:
1.245 +  assumes p_iff_sats: "P <-> sats(A, p, env)"
1.246 +  shows
1.247 +      "[|z \<in> nat; env \<in> list(A)|]
1.248 +       ==> sats(A, bool_of_o_fm(p,z), env) <->
1.249 +           is_bool_of_o(**A, P, nth(z,env))"
1.250 +by (simp add: bool_of_o_fm_def is_bool_of_o_def p_iff_sats [THEN iff_sym])
1.251 +
1.252 +lemma is_bool_of_o_iff_sats:
1.253 +  "[| P <-> sats(A, p, env); nth(k,env) = z; k \<in> nat; env \<in> list(A)|]
1.254 +   ==> is_bool_of_o(**A, P, z) <-> sats(A, bool_of_o_fm(p,k), env)"
1.256 +
1.257 +theorem bool_of_o_reflection:
1.258 +     "REFLECTS [P(L), \<lambda>i. P(**Lset(i))] ==>
1.259 +      REFLECTS[\<lambda>x. is_bool_of_o(L, P(L,x), f(x)),
1.260 +               \<lambda>i x. is_bool_of_o(**Lset(i), P(**Lset(i),x), f(x))]"
1.261 +apply (simp (no_asm) only: is_bool_of_o_def setclass_simps)
1.262 +apply (intro FOL_reflections function_reflections, assumption+)
1.263 +done
1.264 +
1.265 +
1.266 +subsection{*More Internalizations*}
1.267 +
1.268 +subsubsection{*The Operator @{term is_lambda}*}
1.269 +
1.270 +text{*The two arguments of @{term p} are always 1, 0. Remember that
1.271 + @{term p} will be enclosed by three quantifiers.*}
1.272 +
1.273 +(* is_lambda :: "[i=>o, i, [i,i]=>o, i] => o"
1.274 +    "is_lambda(M, A, is_b, z) ==
1.275 +       \<forall>p[M]. p \<in> z <->
1.276 +        (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))" *)
1.277 +constdefs lambda_fm :: "[i, i, i]=>i"
1.278 + "lambda_fm(p,A,z) ==
1.279 +    Forall(Iff(Member(0,succ(z)),
1.280 +            Exists(Exists(And(Member(1,A#+3),
1.281 +                           And(pair_fm(1,0,2), p))))))"
1.282 +
1.283 +text{*We call @{term p} with arguments x, y by equating them with
1.284 +  the corresponding quantified variables with de Bruijn indices 1, 0.*}
1.285 +
1.286 +lemma is_lambda_type [TC]:
1.287 +     "[| p \<in> formula; x \<in> nat; y \<in> nat |]
1.288 +      ==> lambda_fm(p,x,y) \<in> formula"
1.290 +
1.291 +lemma sats_lambda_fm:
1.292 +  assumes is_b_iff_sats:
1.293 +      "!!a0 a1 a2.
1.294 +        [|a0\<in>A; a1\<in>A; a2\<in>A|]
1.295 +        ==> is_b(a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,env))))"
1.296 +  shows
1.297 +      "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
1.298 +       ==> sats(A, lambda_fm(p,x,y), env) <->
1.299 +           is_lambda(**A, nth(x,env), is_b, nth(y,env))"
1.300 +by (simp add: lambda_fm_def is_lambda_def is_b_iff_sats [THEN iff_sym])
1.301 +
1.302 +lemma is_lambda_iff_sats:
1.303 +  assumes is_b_iff_sats:
1.304 +      "!!a0 a1 a2.
1.305 +        [|a0\<in>A; a1\<in>A; a2\<in>A|]
1.306 +        ==> is_b(a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,env))))"
1.307 +  shows
1.308 +  "[|nth(i,env) = x; nth(j,env) = y;
1.309 +      i \<in> nat; j \<in> nat; env \<in> list(A)|]
1.310 +   ==> is_lambda(**A, x, is_b, y) <-> sats(A, lambda_fm(p,i,j), env)"
1.311 +by (simp add: sats_lambda_fm [OF is_b_iff_sats])
1.312 +
1.313 +theorem is_lambda_reflection:
1.314 +  assumes is_b_reflection:
1.315 +    "!!f' f g h. REFLECTS[\<lambda>x. is_b(L, f'(x), f(x), g(x)),
1.316 +                     \<lambda>i x. is_b(**Lset(i), f'(x), f(x), g(x))]"
1.317 +  shows "REFLECTS[\<lambda>x. is_lambda(L, A(x), is_b(L,x), f(x)),
1.318 +               \<lambda>i x. is_lambda(**Lset(i), A(x), is_b(**Lset(i),x), f(x))]"
1.319 +apply (simp (no_asm_use) only: is_lambda_def setclass_simps)
1.320 +apply (intro FOL_reflections is_b_reflection pair_reflection)
1.321 +done
1.322 +
1.323 +subsubsection{*The Operator @{term is_Member}, Internalized*}
1.324 +
1.325 +(*    "is_Member(M,x,y,Z) ==
1.326 +	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)" *)
1.327 +constdefs Member_fm :: "[i,i,i]=>i"
1.328 +    "Member_fm(x,y,Z) ==
1.329 +       Exists(Exists(And(pair_fm(x#+2,y#+2,1),
1.330 +                      And(Inl_fm(1,0), Inl_fm(0,Z#+2)))))"
1.331 +
1.332 +lemma is_Member_type [TC]:
1.333 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Member_fm(x,y,z) \<in> formula"
1.335 +
1.336 +lemma sats_Member_fm [simp]:
1.337 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.338 +    ==> sats(A, Member_fm(x,y,z), env) <->
1.339 +        is_Member(**A, nth(x,env), nth(y,env), nth(z,env))"
1.340 +by (simp add: Member_fm_def is_Member_def)
1.341 +
1.342 +lemma Member_iff_sats:
1.343 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.344 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.345 +       ==> is_Member(**A, x, y, z) <-> sats(A, Member_fm(i,j,k), env)"
1.347 +
1.348 +theorem Member_reflection:
1.349 +     "REFLECTS[\<lambda>x. is_Member(L,f(x),g(x),h(x)),
1.350 +               \<lambda>i x. is_Member(**Lset(i),f(x),g(x),h(x))]"
1.351 +apply (simp only: is_Member_def setclass_simps)
1.352 +apply (intro FOL_reflections pair_reflection Inl_reflection)
1.353 +done
1.354 +
1.355 +subsubsection{*The Operator @{term is_Equal}, Internalized*}
1.356 +
1.357 +(*    "is_Equal(M,x,y,Z) ==
1.358 +	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)" *)
1.359 +constdefs Equal_fm :: "[i,i,i]=>i"
1.360 +    "Equal_fm(x,y,Z) ==
1.361 +       Exists(Exists(And(pair_fm(x#+2,y#+2,1),
1.362 +                      And(Inr_fm(1,0), Inl_fm(0,Z#+2)))))"
1.363 +
1.364 +lemma is_Equal_type [TC]:
1.365 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Equal_fm(x,y,z) \<in> formula"
1.367 +
1.368 +lemma sats_Equal_fm [simp]:
1.369 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.370 +    ==> sats(A, Equal_fm(x,y,z), env) <->
1.371 +        is_Equal(**A, nth(x,env), nth(y,env), nth(z,env))"
1.372 +by (simp add: Equal_fm_def is_Equal_def)
1.373 +
1.374 +lemma Equal_iff_sats:
1.375 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.376 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.377 +       ==> is_Equal(**A, x, y, z) <-> sats(A, Equal_fm(i,j,k), env)"
1.379 +
1.380 +theorem Equal_reflection:
1.381 +     "REFLECTS[\<lambda>x. is_Equal(L,f(x),g(x),h(x)),
1.382 +               \<lambda>i x. is_Equal(**Lset(i),f(x),g(x),h(x))]"
1.383 +apply (simp only: is_Equal_def setclass_simps)
1.384 +apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection)
1.385 +done
1.386 +
1.387 +subsubsection{*The Operator @{term is_Nand}, Internalized*}
1.388 +
1.389 +(*    "is_Nand(M,x,y,Z) ==
1.390 +	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)" *)
1.391 +constdefs Nand_fm :: "[i,i,i]=>i"
1.392 +    "Nand_fm(x,y,Z) ==
1.393 +       Exists(Exists(And(pair_fm(x#+2,y#+2,1),
1.394 +                      And(Inl_fm(1,0), Inr_fm(0,Z#+2)))))"
1.395 +
1.396 +lemma is_Nand_type [TC]:
1.397 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Nand_fm(x,y,z) \<in> formula"
1.399 +
1.400 +lemma sats_Nand_fm [simp]:
1.401 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.402 +    ==> sats(A, Nand_fm(x,y,z), env) <->
1.403 +        is_Nand(**A, nth(x,env), nth(y,env), nth(z,env))"
1.404 +by (simp add: Nand_fm_def is_Nand_def)
1.405 +
1.406 +lemma Nand_iff_sats:
1.407 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.408 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.409 +       ==> is_Nand(**A, x, y, z) <-> sats(A, Nand_fm(i,j,k), env)"
1.411 +
1.412 +theorem Nand_reflection:
1.413 +     "REFLECTS[\<lambda>x. is_Nand(L,f(x),g(x),h(x)),
1.414 +               \<lambda>i x. is_Nand(**Lset(i),f(x),g(x),h(x))]"
1.415 +apply (simp only: is_Nand_def setclass_simps)
1.416 +apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection)
1.417 +done
1.418 +
1.419 +subsubsection{*The Operator @{term is_Forall}, Internalized*}
1.420 +
1.421 +(* "is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)" *)
1.422 +constdefs Forall_fm :: "[i,i]=>i"
1.423 +    "Forall_fm(x,Z) ==
1.424 +       Exists(And(Inr_fm(succ(x),0), Inr_fm(0,succ(Z))))"
1.425 +
1.426 +lemma is_Forall_type [TC]:
1.427 +     "[| x \<in> nat; y \<in> nat |] ==> Forall_fm(x,y) \<in> formula"
1.429 +
1.430 +lemma sats_Forall_fm [simp]:
1.431 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
1.432 +    ==> sats(A, Forall_fm(x,y), env) <->
1.433 +        is_Forall(**A, nth(x,env), nth(y,env))"
1.434 +by (simp add: Forall_fm_def is_Forall_def)
1.435 +
1.436 +lemma Forall_iff_sats:
1.437 +      "[| nth(i,env) = x; nth(j,env) = y;
1.438 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
1.439 +       ==> is_Forall(**A, x, y) <-> sats(A, Forall_fm(i,j), env)"
1.441 +
1.442 +theorem Forall_reflection:
1.443 +     "REFLECTS[\<lambda>x. is_Forall(L,f(x),g(x)),
1.444 +               \<lambda>i x. is_Forall(**Lset(i),f(x),g(x))]"
1.445 +apply (simp only: is_Forall_def setclass_simps)
1.446 +apply (intro FOL_reflections pair_reflection Inr_reflection)
1.447 +done
1.448 +
1.449 +
1.450 +subsubsection{*The Operator @{term is_and}, Internalized*}
1.451 +
1.452 +(* is_and(M,a,b,z) == (number1(M,a)  & z=b) |
1.453 +                       (~number1(M,a) & empty(M,z)) *)
1.454 +constdefs and_fm :: "[i,i,i]=>i"
1.455 +    "and_fm(a,b,z) ==
1.456 +       Or(And(number1_fm(a), Equal(z,b)),
1.457 +          And(Neg(number1_fm(a)),empty_fm(z)))"
1.458 +
1.459 +lemma is_and_type [TC]:
1.460 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> and_fm(x,y,z) \<in> formula"
1.462 +
1.463 +lemma sats_and_fm [simp]:
1.464 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.465 +    ==> sats(A, and_fm(x,y,z), env) <->
1.466 +        is_and(**A, nth(x,env), nth(y,env), nth(z,env))"
1.467 +by (simp add: and_fm_def is_and_def)
1.468 +
1.469 +lemma is_and_iff_sats:
1.470 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.471 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.472 +       ==> is_and(**A, x, y, z) <-> sats(A, and_fm(i,j,k), env)"
1.473 +by simp
1.474 +
1.475 +theorem is_and_reflection:
1.476 +     "REFLECTS[\<lambda>x. is_and(L,f(x),g(x),h(x)),
1.477 +               \<lambda>i x. is_and(**Lset(i),f(x),g(x),h(x))]"
1.478 +apply (simp only: is_and_def setclass_simps)
1.479 +apply (intro FOL_reflections function_reflections)
1.480 +done
1.481 +
1.482 +
1.483 +subsubsection{*The Operator @{term is_or}, Internalized*}
1.484 +
1.485 +(* is_or(M,a,b,z) == (number1(M,a)  & number1(M,z)) |
1.486 +                     (~number1(M,a) & z=b) *)
1.487 +
1.488 +constdefs or_fm :: "[i,i,i]=>i"
1.489 +    "or_fm(a,b,z) ==
1.490 +       Or(And(number1_fm(a), number1_fm(z)),
1.491 +          And(Neg(number1_fm(a)), Equal(z,b)))"
1.492 +
1.493 +lemma is_or_type [TC]:
1.494 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> or_fm(x,y,z) \<in> formula"
1.496 +
1.497 +lemma sats_or_fm [simp]:
1.498 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.499 +    ==> sats(A, or_fm(x,y,z), env) <->
1.500 +        is_or(**A, nth(x,env), nth(y,env), nth(z,env))"
1.501 +by (simp add: or_fm_def is_or_def)
1.502 +
1.503 +lemma is_or_iff_sats:
1.504 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.505 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.506 +       ==> is_or(**A, x, y, z) <-> sats(A, or_fm(i,j,k), env)"
1.507 +by simp
1.508 +
1.509 +theorem is_or_reflection:
1.510 +     "REFLECTS[\<lambda>x. is_or(L,f(x),g(x),h(x)),
1.511 +               \<lambda>i x. is_or(**Lset(i),f(x),g(x),h(x))]"
1.512 +apply (simp only: is_or_def setclass_simps)
1.513 +apply (intro FOL_reflections function_reflections)
1.514 +done
1.515 +
1.516 +
1.517 +
1.518 +subsubsection{*The Operator @{term is_not}, Internalized*}
1.519 +
1.520 +(* is_not(M,a,z) == (number1(M,a)  & empty(M,z)) |
1.521 +                     (~number1(M,a) & number1(M,z)) *)
1.522 +constdefs not_fm :: "[i,i]=>i"
1.523 +    "not_fm(a,z) ==
1.524 +       Or(And(number1_fm(a), empty_fm(z)),
1.525 +          And(Neg(number1_fm(a)), number1_fm(z)))"
1.526 +
1.527 +lemma is_not_type [TC]:
1.528 +     "[| x \<in> nat; z \<in> nat |] ==> not_fm(x,z) \<in> formula"
1.530 +
1.531 +lemma sats_is_not_fm [simp]:
1.532 +   "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
1.533 +    ==> sats(A, not_fm(x,z), env) <-> is_not(**A, nth(x,env), nth(z,env))"
1.534 +by (simp add: not_fm_def is_not_def)
1.535 +
1.536 +lemma is_not_iff_sats:
1.537 +      "[| nth(i,env) = x; nth(k,env) = z;
1.538 +          i \<in> nat; k \<in> nat; env \<in> list(A)|]
1.539 +       ==> is_not(**A, x, z) <-> sats(A, not_fm(i,k), env)"
1.540 +by simp
1.541 +
1.542 +theorem is_not_reflection:
1.543 +     "REFLECTS[\<lambda>x. is_not(L,f(x),g(x)),
1.544 +               \<lambda>i x. is_not(**Lset(i),f(x),g(x))]"
1.545 +apply (simp only: is_not_def setclass_simps)
1.546 +apply (intro FOL_reflections function_reflections)
1.547 +done
1.548 +
1.549 +
1.550 +lemmas extra_reflections =
1.551 +    Inl_reflection Inr_reflection Nil_reflection Cons_reflection
1.552 +    quasilist_reflection hd_reflection tl_reflection bool_of_o_reflection
1.553 +    is_lambda_reflection Member_reflection Equal_reflection Nand_reflection
1.554 +    Forall_reflection is_and_reflection is_or_reflection is_not_reflection
1.555 +
1.556 +lemmas extra_iff_sats =
1.557 +    Inl_iff_sats Inr_iff_sats Nil_iff_sats Cons_iff_sats quasilist_iff_sats
1.558 +    hd_iff_sats tl_iff_sats is_bool_of_o_iff_sats is_lambda_iff_sats
1.559 +    Member_iff_sats Equal_iff_sats Nand_iff_sats Forall_iff_sats
1.560 +    is_and_iff_sats is_or_iff_sats is_not_iff_sats
1.561 +
1.562 +end
```
```     2.1 --- a/src/ZF/Constructible/L_axioms.thy	Tue Aug 13 12:16:14 2002 +0200
2.2 +++ b/src/ZF/Constructible/L_axioms.thy	Tue Aug 13 17:42:34 2002 +0200
2.3 @@ -1539,14 +1539,14 @@
2.4          typed_function_reflection composition_reflection
2.5          injection_reflection surjection_reflection
2.6          bijection_reflection restriction_reflection
2.7 -        order_isomorphism_reflection
2.8 +        order_isomorphism_reflection finite_ordinal_reflection
2.9          ordinal_reflection limit_ordinal_reflection omega_reflection
2.10
2.11  lemmas fun_plus_iff_sats =
2.12          typed_function_iff_sats composition_iff_sats
2.13          injection_iff_sats surjection_iff_sats
2.14          bijection_iff_sats restriction_iff_sats
2.15 -        order_isomorphism_iff_sats
2.16 +        order_isomorphism_iff_sats finite_ordinal_iff_sats
2.17          ordinal_iff_sats limit_ordinal_iff_sats omega_iff_sats
2.18
2.19  end
```
```     3.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Tue Aug 13 12:16:14 2002 +0200
3.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Tue Aug 13 17:42:34 2002 +0200
3.3 @@ -2,13 +2,11 @@
3.4      ID:         \$Id\$
3.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3.6      Copyright   2002  University of Cambridge
3.7 -
3.8 -FIXME: define nth_fm and prove its "sats" theorem
3.9  *)
3.10
3.12
3.13 -theory Rec_Separation = Separation + Datatype_absolute:
3.14 +theory Rec_Separation = Separation + Internalize:
3.15
3.16  text{*This theory proves all instances needed for locales @{text
3.17  "M_trancl"}, @{text "M_wfrank"} and @{text "M_datatypes"}*}
3.18 @@ -305,13 +303,7 @@
3.19    "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
3.20        i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
3.21     ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)"
3.22 -apply (rule iff_sym)
3.23 -apply (rule iff_trans)
3.24 -apply (rule sats_is_recfun_fm [of A MH])
3.25 -apply (rule MH_iff_sats, simp_all)
3.26 -done
3.27 -(*FIXME: surely proof can be improved?*)
3.28 -
3.29 +by (simp add: sats_is_recfun_fm [OF MH_iff_sats])
3.30
3.31  text{*The additional variable in the premise, namely @{term f'}, is essential.
3.32  It lets @{term MH} depend upon @{term x}, which seems often necessary.
3.33 @@ -754,28 +746,27 @@
3.35  done
3.36
3.37 -
3.38  lemma iterates_MH_iff_sats:
3.39 -  "[| (!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
3.40 +  assumes is_F_iff_sats:
3.41 +      "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
3.42                ==> is_F(a,b) <->
3.43 -                  sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env))))));
3.44 -      nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
3.45 +                  sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env)))))"
3.46 +  shows
3.47 +  "[| nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
3.48        i' \<in> nat; i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
3.49     ==> iterates_MH(**A, is_F, v, x, y, z) <->
3.50         sats(A, iterates_MH_fm(p,i',i,j,k), env)"
3.51 -apply (rule iff_sym)
3.52 -apply (rule iff_trans)
3.53 -apply (rule sats_iterates_MH_fm [of A is_F], blast, simp_all)
3.54 -done
3.55 -(*FIXME: surely proof can be improved?*)
3.56 +by (simp add: sats_iterates_MH_fm [OF is_F_iff_sats])
3.57
3.58 -
3.59 +text{*The second argument of @{term p} gives it direct access to @{term x},
3.60 +  which is essential for handling free variable references.  Without this
3.61 +  argument, we cannot prove reflection for @{term list_N}.*}
3.62  theorem iterates_MH_reflection:
3.63    assumes p_reflection:
3.64 -    "!!f g h. REFLECTS[\<lambda>x. p(L, f(x), g(x)),
3.65 -                     \<lambda>i x. p(**Lset(i), f(x), g(x))]"
3.66 - shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L), e(x), f(x), g(x), h(x)),
3.67 -               \<lambda>i x. iterates_MH(**Lset(i), p(**Lset(i)), e(x), f(x), g(x), h(x))]"
3.68 +    "!!f g h. REFLECTS[\<lambda>x. p(L, h(x), f(x), g(x)),
3.69 +                     \<lambda>i x. p(**Lset(i), h(x), f(x), g(x))]"
3.70 + shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L,x), e(x), f(x), g(x), h(x)),
3.71 +               \<lambda>i x. iterates_MH(**Lset(i), p(**Lset(i),x), e(x), f(x), g(x), h(x))]"
3.72  apply (simp (no_asm_use) only: iterates_MH_def)
3.73  txt{*Must be careful: simplifying with @{text setclass_simps} above would
3.74       change @{text "\<exists>gm[**Lset(i)]"} into @{text "\<exists>gm \<in> Lset(i)"}, when
3.75 @@ -1035,229 +1026,6 @@
3.76  for @{term "list(A)"}.  It was a cut-and-paste job! *}
3.77
3.78
3.79 -subsection{*Internalized Forms of Data Structuring Operators*}
3.80 -
3.81 -subsubsection{*The Formula @{term is_Inl}, Internalized*}
3.82 -
3.83 -(*  is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z) *)
3.84 -constdefs Inl_fm :: "[i,i]=>i"
3.85 -    "Inl_fm(a,z) == Exists(And(empty_fm(0), pair_fm(0,succ(a),succ(z))))"
3.86 -
3.87 -lemma Inl_type [TC]:
3.88 -     "[| x \<in> nat; z \<in> nat |] ==> Inl_fm(x,z) \<in> formula"
3.90 -
3.91 -lemma sats_Inl_fm [simp]:
3.92 -   "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
3.93 -    ==> sats(A, Inl_fm(x,z), env) <-> is_Inl(**A, nth(x,env), nth(z,env))"
3.94 -by (simp add: Inl_fm_def is_Inl_def)
3.95 -
3.96 -lemma Inl_iff_sats:
3.97 -      "[| nth(i,env) = x; nth(k,env) = z;
3.98 -          i \<in> nat; k \<in> nat; env \<in> list(A)|]
3.99 -       ==> is_Inl(**A, x, z) <-> sats(A, Inl_fm(i,k), env)"
3.100 -by simp
3.101 -
3.102 -theorem Inl_reflection:
3.103 -     "REFLECTS[\<lambda>x. is_Inl(L,f(x),h(x)),
3.104 -               \<lambda>i x. is_Inl(**Lset(i),f(x),h(x))]"
3.105 -apply (simp only: is_Inl_def setclass_simps)
3.106 -apply (intro FOL_reflections function_reflections)
3.107 -done
3.108 -
3.109 -
3.110 -subsubsection{*The Formula @{term is_Inr}, Internalized*}
3.111 -
3.112 -(*  is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z) *)
3.113 -constdefs Inr_fm :: "[i,i]=>i"
3.114 -    "Inr_fm(a,z) == Exists(And(number1_fm(0), pair_fm(0,succ(a),succ(z))))"
3.115 -
3.116 -lemma Inr_type [TC]:
3.117 -     "[| x \<in> nat; z \<in> nat |] ==> Inr_fm(x,z) \<in> formula"
3.119 -
3.120 -lemma sats_Inr_fm [simp]:
3.121 -   "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
3.122 -    ==> sats(A, Inr_fm(x,z), env) <-> is_Inr(**A, nth(x,env), nth(z,env))"
3.123 -by (simp add: Inr_fm_def is_Inr_def)
3.124 -
3.125 -lemma Inr_iff_sats:
3.126 -      "[| nth(i,env) = x; nth(k,env) = z;
3.127 -          i \<in> nat; k \<in> nat; env \<in> list(A)|]
3.128 -       ==> is_Inr(**A, x, z) <-> sats(A, Inr_fm(i,k), env)"
3.129 -by simp
3.130 -
3.131 -theorem Inr_reflection:
3.132 -     "REFLECTS[\<lambda>x. is_Inr(L,f(x),h(x)),
3.133 -               \<lambda>i x. is_Inr(**Lset(i),f(x),h(x))]"
3.134 -apply (simp only: is_Inr_def setclass_simps)
3.135 -apply (intro FOL_reflections function_reflections)
3.136 -done
3.137 -
3.138 -
3.139 -subsubsection{*The Formula @{term is_Nil}, Internalized*}
3.140 -
3.141 -(* is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs) *)
3.142 -
3.143 -constdefs Nil_fm :: "i=>i"
3.144 -    "Nil_fm(x) == Exists(And(empty_fm(0), Inl_fm(0,succ(x))))"
3.145 -
3.146 -lemma Nil_type [TC]: "x \<in> nat ==> Nil_fm(x) \<in> formula"
3.148 -
3.149 -lemma sats_Nil_fm [simp]:
3.150 -   "[| x \<in> nat; env \<in> list(A)|]
3.151 -    ==> sats(A, Nil_fm(x), env) <-> is_Nil(**A, nth(x,env))"
3.152 -by (simp add: Nil_fm_def is_Nil_def)
3.153 -
3.154 -lemma Nil_iff_sats:
3.155 -      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
3.156 -       ==> is_Nil(**A, x) <-> sats(A, Nil_fm(i), env)"
3.157 -by simp
3.158 -
3.159 -theorem Nil_reflection:
3.160 -     "REFLECTS[\<lambda>x. is_Nil(L,f(x)),
3.161 -               \<lambda>i x. is_Nil(**Lset(i),f(x))]"
3.162 -apply (simp only: is_Nil_def setclass_simps)
3.163 -apply (intro FOL_reflections function_reflections Inl_reflection)
3.164 -done
3.165 -
3.166 -
3.167 -subsubsection{*The Formula @{term is_Cons}, Internalized*}
3.168 -
3.169 -
3.170 -(*  "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)" *)
3.171 -constdefs Cons_fm :: "[i,i,i]=>i"
3.172 -    "Cons_fm(a,l,Z) ==
3.173 -       Exists(And(pair_fm(succ(a),succ(l),0), Inr_fm(0,succ(Z))))"
3.174 -
3.175 -lemma Cons_type [TC]:
3.176 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Cons_fm(x,y,z) \<in> formula"
3.178 -
3.179 -lemma sats_Cons_fm [simp]:
3.180 -   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
3.181 -    ==> sats(A, Cons_fm(x,y,z), env) <->
3.182 -       is_Cons(**A, nth(x,env), nth(y,env), nth(z,env))"
3.183 -by (simp add: Cons_fm_def is_Cons_def)
3.184 -
3.185 -lemma Cons_iff_sats:
3.186 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
3.187 -          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
3.188 -       ==>is_Cons(**A, x, y, z) <-> sats(A, Cons_fm(i,j,k), env)"
3.189 -by simp
3.190 -
3.191 -theorem Cons_reflection:
3.192 -     "REFLECTS[\<lambda>x. is_Cons(L,f(x),g(x),h(x)),
3.193 -               \<lambda>i x. is_Cons(**Lset(i),f(x),g(x),h(x))]"
3.194 -apply (simp only: is_Cons_def setclass_simps)
3.195 -apply (intro FOL_reflections pair_reflection Inr_reflection)
3.196 -done
3.197 -
3.198 -subsubsection{*The Formula @{term is_quasilist}, Internalized*}
3.199 -
3.200 -(* is_quasilist(M,xs) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))" *)
3.201 -
3.202 -constdefs quasilist_fm :: "i=>i"
3.203 -    "quasilist_fm(x) ==
3.204 -       Or(Nil_fm(x), Exists(Exists(Cons_fm(1,0,succ(succ(x))))))"
3.205 -
3.206 -lemma quasilist_type [TC]: "x \<in> nat ==> quasilist_fm(x) \<in> formula"
3.208 -
3.209 -lemma sats_quasilist_fm [simp]:
3.210 -   "[| x \<in> nat; env \<in> list(A)|]
3.211 -    ==> sats(A, quasilist_fm(x), env) <-> is_quasilist(**A, nth(x,env))"
3.212 -by (simp add: quasilist_fm_def is_quasilist_def)
3.213 -
3.214 -lemma quasilist_iff_sats:
3.215 -      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
3.216 -       ==> is_quasilist(**A, x) <-> sats(A, quasilist_fm(i), env)"
3.217 -by simp
3.218 -
3.219 -theorem quasilist_reflection:
3.220 -     "REFLECTS[\<lambda>x. is_quasilist(L,f(x)),
3.221 -               \<lambda>i x. is_quasilist(**Lset(i),f(x))]"
3.222 -apply (simp only: is_quasilist_def setclass_simps)
3.223 -apply (intro FOL_reflections Nil_reflection Cons_reflection)
3.224 -done
3.225 -
3.226 -
3.227 -subsection{*Absoluteness for the Function @{term nth}*}
3.228 -
3.229 -
3.230 -subsubsection{*The Formula @{term is_hd}, Internalized*}
3.231 -
3.232 -(*   "is_hd(M,xs,H) ==
3.233 -       (is_Nil(M,xs) --> empty(M,H)) &
3.234 -       (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
3.235 -       (is_quasilist(M,xs) | empty(M,H))" *)
3.236 -constdefs hd_fm :: "[i,i]=>i"
3.237 -    "hd_fm(xs,H) ==
3.238 -       And(Implies(Nil_fm(xs), empty_fm(H)),
3.239 -           And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(H#+2,1)))),
3.240 -               Or(quasilist_fm(xs), empty_fm(H))))"
3.241 -
3.242 -lemma hd_type [TC]:
3.243 -     "[| x \<in> nat; y \<in> nat |] ==> hd_fm(x,y) \<in> formula"
3.245 -
3.246 -lemma sats_hd_fm [simp]:
3.247 -   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
3.248 -    ==> sats(A, hd_fm(x,y), env) <-> is_hd(**A, nth(x,env), nth(y,env))"
3.249 -by (simp add: hd_fm_def is_hd_def)
3.250 -
3.251 -lemma hd_iff_sats:
3.252 -      "[| nth(i,env) = x; nth(j,env) = y;
3.253 -          i \<in> nat; j \<in> nat; env \<in> list(A)|]
3.254 -       ==> is_hd(**A, x, y) <-> sats(A, hd_fm(i,j), env)"
3.255 -by simp
3.256 -
3.257 -theorem hd_reflection:
3.258 -     "REFLECTS[\<lambda>x. is_hd(L,f(x),g(x)),
3.259 -               \<lambda>i x. is_hd(**Lset(i),f(x),g(x))]"
3.260 -apply (simp only: is_hd_def setclass_simps)
3.261 -apply (intro FOL_reflections Nil_reflection Cons_reflection
3.262 -             quasilist_reflection empty_reflection)
3.263 -done
3.264 -
3.265 -
3.266 -subsubsection{*The Formula @{term is_tl}, Internalized*}
3.267 -
3.268 -(*     "is_tl(M,xs,T) ==
3.269 -       (is_Nil(M,xs) --> T=xs) &
3.270 -       (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
3.271 -       (is_quasilist(M,xs) | empty(M,T))" *)
3.272 -constdefs tl_fm :: "[i,i]=>i"
3.273 -    "tl_fm(xs,T) ==
3.274 -       And(Implies(Nil_fm(xs), Equal(T,xs)),
3.275 -           And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(T#+2,0)))),
3.276 -               Or(quasilist_fm(xs), empty_fm(T))))"
3.277 -
3.278 -lemma tl_type [TC]:
3.279 -     "[| x \<in> nat; y \<in> nat |] ==> tl_fm(x,y) \<in> formula"
3.281 -
3.282 -lemma sats_tl_fm [simp]:
3.283 -   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
3.284 -    ==> sats(A, tl_fm(x,y), env) <-> is_tl(**A, nth(x,env), nth(y,env))"
3.285 -by (simp add: tl_fm_def is_tl_def)
3.286 -
3.287 -lemma tl_iff_sats:
3.288 -      "[| nth(i,env) = x; nth(j,env) = y;
3.289 -          i \<in> nat; j \<in> nat; env \<in> list(A)|]
3.290 -       ==> is_tl(**A, x, y) <-> sats(A, tl_fm(i,j), env)"
3.291 -by simp
3.292 -
3.293 -theorem tl_reflection:
3.294 -     "REFLECTS[\<lambda>x. is_tl(L,f(x),g(x)),
3.295 -               \<lambda>i x. is_tl(**Lset(i),f(x),g(x))]"
3.296 -apply (simp only: is_tl_def setclass_simps)
3.297 -apply (intro FOL_reflections Nil_reflection Cons_reflection
3.298 -             quasilist_reflection empty_reflection)
3.299 -done
3.300 -
3.301 -
3.302  subsubsection{*The Formula @{term is_nth}, Internalized*}
3.303
3.304  (* "is_nth(M,n,l,Z) ==
3.305 @@ -1299,14 +1067,6 @@
3.306               iterates_MH_reflection hd_reflection tl_reflection)
3.307  done
3.308
3.309 -theorem bool_of_o_reflection:
3.310 -     "REFLECTS [P(L), \<lambda>i. P(**Lset(i))] ==>
3.311 -      REFLECTS[\<lambda>x. is_bool_of_o(L, P(L,x), f(x)),
3.312 -               \<lambda>i x. is_bool_of_o(**Lset(i), P(**Lset(i),x), f(x))]"
3.313 -apply (simp (no_asm) only: is_bool_of_o_def setclass_simps)
3.314 -apply (intro FOL_reflections function_reflections, assumption+)
3.315 -done
3.316 -
3.317
3.318  subsubsection{*An Instance of Replacement for @{term nth}*}
3.319
```
```     4.1 --- a/src/ZF/Constructible/Satisfies_absolute.thy	Tue Aug 13 12:16:14 2002 +0200
4.2 +++ b/src/ZF/Constructible/Satisfies_absolute.thy	Tue Aug 13 17:42:34 2002 +0200
4.3 @@ -4,218 +4,126 @@
4.4      Copyright   2002  University of Cambridge
4.5  *)
4.6
4.7 +header {*Absoluteness for the Satisfies Relation on Formulas*}
4.8 +
4.9  theory Satisfies_absolute = Datatype_absolute + Rec_Separation:
4.10
4.11
4.12 -subsection{*More Internalizations*}
4.13 +
4.14 +subsubsection{*The Formula @{term is_list_N}, Internalized*}
4.15
4.16 -lemma and_reflection:
4.17 -     "REFLECTS[\<lambda>x. is_and(L,f(x),g(x),h(x)),
4.18 -               \<lambda>i x. is_and(**Lset(i),f(x),g(x),h(x))]"
4.19 -apply (simp only: is_and_def setclass_simps)
4.20 -apply (intro FOL_reflections function_reflections)
4.21 -done
4.22 +(* "is_list_N(M,A,n,Z) ==
4.23 +      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M].
4.24 +       empty(M,zero) &
4.25 +       successor(M,n,sn) & membership(M,sn,msn) &
4.26 +       is_wfrec(M, iterates_MH(M, is_list_functor(M,A),zero), msn, n, Z)" *)
4.27 +
4.28 +constdefs list_N_fm :: "[i,i,i]=>i"
4.29 +  "list_N_fm(A,n,Z) ==
4.30 +     Exists(Exists(Exists(
4.31 +       And(empty_fm(2),
4.32 +         And(succ_fm(n#+3,1),
4.33 +          And(Memrel_fm(1,0),
4.34 +              is_wfrec_fm(iterates_MH_fm(list_functor_fm(A#+9#+3,1,0),
4.35 +                                         7,2,1,0),
4.36 +                           0, n#+3, Z#+3)))))))"
4.37
4.38 -lemma not_reflection:
4.39 -     "REFLECTS[\<lambda>x. is_not(L,f(x),g(x)),
4.40 -               \<lambda>i x. is_not(**Lset(i),f(x),g(x))]"
4.41 -apply (simp only: is_not_def setclass_simps)
4.42 -apply (intro FOL_reflections function_reflections)
4.43 +lemma list_N_fm_type [TC]:
4.44 + "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> list_N_fm(x,y,z) \<in> formula"
4.46 +
4.47 +lemma sats_list_N_fm [simp]:
4.48 +   "[| x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
4.49 +    ==> sats(A, list_N_fm(x,y,z), env) <->
4.50 +        is_list_N(**A, nth(x,env), nth(y,env), nth(z,env))"
4.51 +apply (frule_tac x=z in lt_length_in_nat, assumption)
4.52 +apply (frule_tac x=y in lt_length_in_nat, assumption)
4.53 +apply (simp add: list_N_fm_def is_list_N_def sats_is_wfrec_fm
4.54 +                 sats_iterates_MH_fm)
4.55  done
4.56
4.57 -subsubsection{*The Operator @{term is_lambda}*}
4.58 -
4.59 -text{*The two arguments of @{term p} are always 1, 0. Remember that
4.60 - @{term p} will be enclosed by three quantifiers.*}
4.61 -
4.62 -(* is_lambda :: "[i=>o, i, [i,i]=>o, i] => o"
4.63 -    "is_lambda(M, A, is_b, z) ==
4.64 -       \<forall>p[M]. p \<in> z <->
4.65 -        (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))" *)
4.66 -constdefs lambda_fm :: "[i, i, i]=>i"
4.67 - "lambda_fm(p,A,z) ==
4.68 -    Forall(Iff(Member(0,succ(z)),
4.69 -            Exists(Exists(And(Member(1,A#+3),
4.70 -                           And(pair_fm(1,0,2), p))))))"
4.71 -
4.72 -text{*We call @{term p} with arguments x, y by equating them with
4.73 -  the corresponding quantified variables with de Bruijn indices 1, 0.*}
4.74 -
4.75 -lemma is_lambda_type [TC]:
4.76 -     "[| p \<in> formula; x \<in> nat; y \<in> nat |]
4.77 -      ==> lambda_fm(p,x,y) \<in> formula"
4.79 +lemma list_N_iff_sats:
4.80 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
4.81 +          i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
4.82 +       ==> is_list_N(**A, x, y, z) <-> sats(A, list_N_fm(i,j,k), env)"
4.84
4.85 -lemma sats_lambda_fm:
4.86 -  assumes is_b_iff_sats:
4.87 -      "!!a0 a1 a2.
4.88 -        [|a0\<in>A; a1\<in>A; a2\<in>A|]
4.89 -        ==> is_b(a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,env))))"
4.90 -  shows
4.91 -      "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
4.92 -       ==> sats(A, lambda_fm(p,x,y), env) <->
4.93 -           is_lambda(**A, nth(x,env), is_b, nth(y,env))"
4.94 -by (simp add: lambda_fm_def sats_is_recfun_fm is_lambda_def is_b_iff_sats [THEN iff_sym])
4.95 -
4.96 -
4.97 -lemma is_lambda_iff_sats:
4.98 -  assumes is_b_iff_sats:
4.99 -      "!!a0 a1 a2.
4.100 -        [|a0\<in>A; a1\<in>A; a2\<in>A|]
4.101 -        ==> is_b(a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,env))))"
4.102 -  shows
4.103 -  "[|nth(i,env) = x; nth(j,env) = y;
4.104 -      i \<in> nat; j \<in> nat; env \<in> list(A)|]
4.105 -   ==> is_lambda(**A, x, is_b, y) <-> sats(A, lambda_fm(p,i,j), env)"
4.106 -by (simp add: sats_lambda_fm [OF is_b_iff_sats])
4.107 -
4.108 -theorem is_lambda_reflection:
4.109 -  assumes is_b_reflection:
4.110 -    "!!f' f g h. REFLECTS[\<lambda>x. is_b(L, f'(x), f(x), g(x)),
4.111 -                     \<lambda>i x. is_b(**Lset(i), f'(x), f(x), g(x))]"
4.112 -  shows "REFLECTS[\<lambda>x. is_lambda(L, A(x), is_b(L,x), f(x)),
4.113 -               \<lambda>i x. is_lambda(**Lset(i), A(x), is_b(**Lset(i),x), f(x))]"
4.114 -apply (simp (no_asm_use) only: is_lambda_def setclass_simps)
4.115 -apply (intro FOL_reflections is_b_reflection pair_reflection)
4.116 +theorem list_N_reflection:
4.117 +     "REFLECTS[\<lambda>x. is_list_N(L, f(x), g(x), h(x)),
4.118 +               \<lambda>i x. is_list_N(**Lset(i), f(x), g(x), h(x))]"
4.119 +apply (simp only: is_list_N_def setclass_simps)
4.120 +apply (intro FOL_reflections function_reflections is_wfrec_reflection
4.121 +             iterates_MH_reflection list_functor_reflection)
4.122  done
4.123
4.124
4.125 -subsubsection{*The Operator @{term is_Member}, Internalized*}
4.126 +
4.127 +subsubsection{*The Predicate ``Is A List''*}
4.128
4.129 -(*    "is_Member(M,x,y,Z) ==
4.130 -	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)" *)
4.131 -constdefs Member_fm :: "[i,i,i]=>i"
4.132 -    "Member_fm(x,y,Z) ==
4.133 -       Exists(Exists(And(pair_fm(x#+2,y#+2,1),
4.134 -                      And(Inl_fm(1,0), Inl_fm(0,Z#+2)))))"
4.135 +(* mem_list(M,A,l) ==
4.136 +      \<exists>n[M]. \<exists>listn[M].
4.137 +       finite_ordinal(M,n) & is_list_N(M,A,n,listn) & l \<in> listn *)
4.138 +constdefs mem_list_fm :: "[i,i]=>i"
4.139 +    "mem_list_fm(x,y) ==
4.140 +       Exists(Exists(
4.141 +         And(finite_ordinal_fm(1),
4.142 +           And(list_N_fm(x#+2,1,0), Member(y#+2,0)))))"
4.143
4.144 -lemma is_Member_type [TC]:
4.145 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Member_fm(x,y,z) \<in> formula"
4.147 +lemma mem_list_type [TC]:
4.148 +     "[| x \<in> nat; y \<in> nat |] ==> mem_list_fm(x,y) \<in> formula"
4.150
4.151 -lemma sats_Member_fm [simp]:
4.152 -   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
4.153 -    ==> sats(A, Member_fm(x,y,z), env) <->
4.154 -        is_Member(**A, nth(x,env), nth(y,env), nth(z,env))"
4.155 -by (simp add: Member_fm_def is_Member_def)
4.156 +lemma sats_mem_list_fm [simp]:
4.157 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
4.158 +    ==> sats(A, mem_list_fm(x,y), env) <-> mem_list(**A, nth(x,env), nth(y,env))"
4.159 +by (simp add: mem_list_fm_def mem_list_def)
4.160
4.161 -lemma Member_iff_sats:
4.162 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
4.163 -          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
4.164 -       ==> is_Member(**A, x, y, z) <-> sats(A, Member_fm(i,j,k), env)"
4.166 +lemma mem_list_iff_sats:
4.167 +      "[| nth(i,env) = x; nth(j,env) = y;
4.168 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
4.169 +       ==> mem_list(**A, x, y) <-> sats(A, mem_list_fm(i,j), env)"
4.170 +by simp
4.171
4.172 -theorem Member_reflection:
4.173 -     "REFLECTS[\<lambda>x. is_Member(L,f(x),g(x),h(x)),
4.174 -               \<lambda>i x. is_Member(**Lset(i),f(x),g(x),h(x))]"
4.175 -apply (simp only: is_Member_def setclass_simps)
4.176 -apply (intro FOL_reflections pair_reflection Inl_reflection)
4.177 +theorem mem_list_reflection:
4.178 +     "REFLECTS[\<lambda>x. mem_list(L,f(x),g(x)),
4.179 +               \<lambda>i x. mem_list(**Lset(i),f(x),g(x))]"
4.180 +apply (simp only: mem_list_def setclass_simps)
4.181 +apply (intro FOL_reflections finite_ordinal_reflection list_N_reflection)
4.182  done
4.183
4.184 -subsubsection{*The Operator @{term is_Equal}, Internalized*}
4.185
4.186 -(*    "is_Equal(M,x,y,Z) ==
4.187 -	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)" *)
4.188 -constdefs Equal_fm :: "[i,i,i]=>i"
4.189 -    "Equal_fm(x,y,Z) ==
4.190 -       Exists(Exists(And(pair_fm(x#+2,y#+2,1),
4.191 -                      And(Inr_fm(1,0), Inl_fm(0,Z#+2)))))"
4.192 -
4.193 -lemma is_Equal_type [TC]:
4.194 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Equal_fm(x,y,z) \<in> formula"
4.196 -
4.197 -lemma sats_Equal_fm [simp]:
4.198 -   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
4.199 -    ==> sats(A, Equal_fm(x,y,z), env) <->
4.200 -        is_Equal(**A, nth(x,env), nth(y,env), nth(z,env))"
4.201 -by (simp add: Equal_fm_def is_Equal_def)
4.202 +subsubsection{*The Predicate ``Is @{term "list(A)"}''*}
4.203
4.204 -lemma Equal_iff_sats:
4.205 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
4.206 -          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
4.207 -       ==> is_Equal(**A, x, y, z) <-> sats(A, Equal_fm(i,j,k), env)"
4.209 -
4.210 -theorem Equal_reflection:
4.211 -     "REFLECTS[\<lambda>x. is_Equal(L,f(x),g(x),h(x)),
4.212 -               \<lambda>i x. is_Equal(**Lset(i),f(x),g(x),h(x))]"
4.213 -apply (simp only: is_Equal_def setclass_simps)
4.214 -apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection)
4.215 -done
4.216 +(* is_list(M,A,Z) == \<forall>l[M]. l \<in> Z <-> mem_list(M,A,l) *)
4.217 +constdefs is_list_fm :: "[i,i]=>i"
4.218 +    "is_list_fm(A,Z) ==
4.219 +       Forall(Iff(Member(0,succ(Z)), mem_list_fm(succ(A),0)))"
4.220
4.221 -subsubsection{*The Operator @{term is_Nand}, Internalized*}
4.222 -
4.223 -(*    "is_Nand(M,x,y,Z) ==
4.224 -	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)" *)
4.225 -constdefs Nand_fm :: "[i,i,i]=>i"
4.226 -    "Nand_fm(x,y,Z) ==
4.227 -       Exists(Exists(And(pair_fm(x#+2,y#+2,1),
4.228 -                      And(Inl_fm(1,0), Inr_fm(0,Z#+2)))))"
4.229 -
4.230 -lemma is_Nand_type [TC]:
4.231 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Nand_fm(x,y,z) \<in> formula"
4.233 +lemma is_list_type [TC]:
4.234 +     "[| x \<in> nat; y \<in> nat |] ==> is_list_fm(x,y) \<in> formula"
4.236
4.237 -lemma sats_Nand_fm [simp]:
4.238 -   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
4.239 -    ==> sats(A, Nand_fm(x,y,z), env) <->
4.240 -        is_Nand(**A, nth(x,env), nth(y,env), nth(z,env))"
4.241 -by (simp add: Nand_fm_def is_Nand_def)
4.242 -
4.243 -lemma Nand_iff_sats:
4.244 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
4.245 -          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
4.246 -       ==> is_Nand(**A, x, y, z) <-> sats(A, Nand_fm(i,j,k), env)"
4.248 -
4.249 -theorem Nand_reflection:
4.250 -     "REFLECTS[\<lambda>x. is_Nand(L,f(x),g(x),h(x)),
4.251 -               \<lambda>i x. is_Nand(**Lset(i),f(x),g(x),h(x))]"
4.252 -apply (simp only: is_Nand_def setclass_simps)
4.253 -apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection)
4.254 -done
4.255 -
4.256 -subsubsection{*The Operator @{term is_Forall}, Internalized*}
4.257 +lemma sats_is_list_fm [simp]:
4.258 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
4.259 +    ==> sats(A, is_list_fm(x,y), env) <-> is_list(**A, nth(x,env), nth(y,env))"
4.260 +by (simp add: is_list_fm_def is_list_def)
4.261
4.262 -(* "is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)" *)
4.263 -constdefs Forall_fm :: "[i,i]=>i"
4.264 -    "Forall_fm(x,Z) ==
4.265 -       Exists(And(Inr_fm(succ(x),0), Inr_fm(0,succ(Z))))"
4.266 -
4.267 -lemma is_Forall_type [TC]:
4.268 -     "[| x \<in> nat; y \<in> nat |] ==> Forall_fm(x,y) \<in> formula"
4.270 +lemma is_list_iff_sats:
4.271 +      "[| nth(i,env) = x; nth(j,env) = y;
4.272 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
4.273 +       ==> is_list(**A, x, y) <-> sats(A, is_list_fm(i,j), env)"
4.274 +by simp
4.275
4.276 -lemma sats_Forall_fm [simp]:
4.277 -   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
4.278 -    ==> sats(A, Forall_fm(x,y), env) <->
4.279 -        is_Forall(**A, nth(x,env), nth(y,env))"
4.280 -by (simp add: Forall_fm_def is_Forall_def)
4.281 -
4.282 -lemma Forall_iff_sats:
4.283 -      "[| nth(i,env) = x; nth(j,env) = y;
4.284 -          i \<in> nat; j \<in> nat; env \<in> list(A)|]
4.285 -       ==> is_Forall(**A, x, y) <-> sats(A, Forall_fm(i,j), env)"
4.287 -
4.288 -theorem Forall_reflection:
4.289 -     "REFLECTS[\<lambda>x. is_Forall(L,f(x),g(x)),
4.290 -               \<lambda>i x. is_Forall(**Lset(i),f(x),g(x))]"
4.291 -apply (simp only: is_Forall_def setclass_simps)
4.292 -apply (intro FOL_reflections pair_reflection Inr_reflection)
4.293 +theorem is_list_reflection:
4.294 +     "REFLECTS[\<lambda>x. is_list(L,f(x),g(x)),
4.295 +               \<lambda>i x. is_list(**Lset(i),f(x),g(x))]"
4.296 +apply (simp only: is_list_def setclass_simps)
4.297 +apply (intro FOL_reflections mem_list_reflection)
4.298  done
4.299
4.300
4.301  subsubsection{*The Formula @{term is_formula_N}, Internalized*}
4.302
4.303 -(* "is_nth(M,n,l,Z) ==
4.304 -      \<exists>X[M]. \<exists>sn[M]. \<exists>msn[M].
4.305 -       2       1       0
4.306 -       successor(M,n,sn) & membership(M,sn,msn) &
4.307 -       is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) &
4.308 -       is_hd(M,X,Z)" *)
4.309 -
4.310  (* "is_formula_N(M,n,Z) ==
4.311        \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M].
4.312            2       1       0
4.313 @@ -281,8 +189,7 @@
4.314  by (simp add: mem_formula_fm_def mem_formula_def)
4.315
4.316  lemma mem_formula_iff_sats:
4.317 -      "[| nth(i,env) = x; nth(j,env) = y;
4.318 -          i \<in> nat; env \<in> list(A)|]
4.319 +      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
4.320         ==> mem_formula(**A, x) <-> sats(A, mem_formula_fm(i), env)"
4.321  by simp
4.322
4.323 @@ -295,6 +202,34 @@
4.324
4.325
4.326
4.327 +subsubsection{*The Predicate ``Is @{term "formula"}''*}
4.328 +
4.329 +(* is_formula(M,Z) == \<forall>p[M]. p \<in> Z <-> mem_formula(M,p) *)
4.330 +constdefs is_formula_fm :: "i=>i"
4.331 +    "is_formula_fm(Z) == Forall(Iff(Member(0,succ(Z)), mem_formula_fm(0)))"
4.332 +
4.333 +lemma is_formula_type [TC]:
4.334 +     "x \<in> nat ==> is_formula_fm(x) \<in> formula"
4.336 +
4.337 +lemma sats_is_formula_fm [simp]:
4.338 +   "[| x \<in> nat; env \<in> list(A)|]
4.339 +    ==> sats(A, is_formula_fm(x), env) <-> is_formula(**A, nth(x,env))"
4.340 +by (simp add: is_formula_fm_def is_formula_def)
4.341 +
4.342 +lemma is_formula_iff_sats:
4.343 +      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
4.344 +       ==> is_formula(**A, x) <-> sats(A, is_formula_fm(i), env)"
4.345 +by simp
4.346 +
4.347 +theorem is_formula_reflection:
4.348 +     "REFLECTS[\<lambda>x. is_formula(L,f(x)),
4.349 +               \<lambda>i x. is_formula(**Lset(i),f(x))]"
4.350 +apply (simp only: is_formula_def setclass_simps)
4.351 +apply (intro FOL_reflections mem_formula_reflection)
4.352 +done
4.353 +
4.354 +
4.355  subsubsection{*The Formula @{term is_depth}, Internalized*}
4.356
4.357  (*    "is_depth(M,p,n) ==
4.358 @@ -580,7 +515,7 @@
4.359     --{*Merely a useful abbreviation for the sequel.*}
4.360     "is_depth_apply(M,h,p,z) ==
4.361      \<exists>dp[M]. \<exists>sdp[M]. \<exists>hsdp[M].
4.362 -	dp \<in> nat & is_depth(M,p,dp) & successor(M,dp,sdp) &
4.363 +	finite_ordinal(M,dp) & is_depth(M,p,dp) & successor(M,dp,sdp) &
4.364  	fun_apply(M,h,sdp,hsdp) & fun_apply(M,hsdp,p,z)"
4.365
4.366  lemma (in M_datatypes) is_depth_apply_abs [simp]:
4.367 @@ -588,12 +523,6 @@
4.368        ==> is_depth_apply(M,h,p,z) <-> z = h ` succ(depth(p)) ` p"
4.369  by (simp add: is_depth_apply_def formula_into_M depth_type eq_commute)
4.370
4.371 -lemma depth_apply_reflection:
4.372 -     "REFLECTS[\<lambda>x. is_depth_apply(L,f(x),g(x),h(x)),
4.373 -               \<lambda>i x. is_depth_apply(**Lset(i),f(x),g(x),h(x))]"
4.374 -apply (simp only: is_depth_apply_def setclass_simps)
4.375 -apply (intro FOL_reflections function_reflections depth_reflection)
4.376 -done
4.377
4.378
4.379  text{*There is at present some redundancy between the relativizations in
4.380 @@ -608,9 +537,12 @@
4.381
4.382    satisfies_is_a :: "[i=>o,i,i,i,i]=>o"
4.383     "satisfies_is_a(M,A) ==
4.384 -    \<lambda>x y. is_lambda(M, list(A),
4.385 -        \<lambda>env z. is_bool_of_o(M, \<exists>nx[M]. \<exists>ny[M].
4.386 -                  is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & nx \<in> ny, z))"
4.387 +    \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) -->
4.388 +             is_lambda(M, lA,
4.389 +		\<lambda>env z. is_bool_of_o(M,
4.390 +                      \<exists>nx[M]. \<exists>ny[M].
4.391 + 		       is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & nx \<in> ny, z),
4.392 +                zz)"
4.393
4.394    satisfies_b :: "[i,i,i]=>i"
4.395     "satisfies_b(A) ==
4.396 @@ -620,20 +552,23 @@
4.397     --{*We simplify the formula to have just @{term nx} rather than
4.398         introducing @{term ny} with  @{term "nx=ny"} *}
4.399     "satisfies_is_b(M,A) ==
4.400 -    \<lambda>x y. is_lambda(M, list(A),
4.401 -         \<lambda>env z.
4.402 -         is_bool_of_o(M, \<exists>nx[M]. is_nth(M,x,env,nx) & is_nth(M,y,env,nx), z))"
4.403 +    \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) -->
4.404 +             is_lambda(M, lA,
4.405 +                \<lambda>env z. is_bool_of_o(M,
4.406 +                      \<exists>nx[M]. is_nth(M,x,env,nx) & is_nth(M,y,env,nx), z),
4.407 +                zz)"
4.408
4.409    satisfies_c :: "[i,i,i,i,i]=>i"
4.410     "satisfies_c(A,p,q,rp,rq) == \<lambda>env \<in> list(A). not(rp ` env and rq ` env)"
4.411
4.412    satisfies_is_c :: "[i=>o,i,i,i,i,i]=>o"
4.413     "satisfies_is_c(M,A,h) ==
4.414 -    \<lambda>p q. is_lambda(M, list(A),
4.415 -        \<lambda>env z. \<exists>hp[M]. \<exists>hq[M].
4.416 +    \<lambda>p q zz. \<forall>lA[M]. is_list(M,A,lA) -->
4.417 +             is_lambda(M, lA, \<lambda>env z. \<exists>hp[M]. \<exists>hq[M].
4.418  		 (\<exists>rp[M]. is_depth_apply(M,h,p,rp) & fun_apply(M,rp,env,hp)) &
4.419  		 (\<exists>rq[M]. is_depth_apply(M,h,q,rq) & fun_apply(M,rq,env,hq)) &
4.420 -                 (\<exists>pq[M]. is_and(M,hp,hq,pq) & is_not(M,pq,z)))"
4.421 +                 (\<exists>pq[M]. is_and(M,hp,hq,pq) & is_not(M,pq,z)),
4.422 +                zz)"
4.423
4.424    satisfies_d :: "[i,i,i]=>i"
4.425     "satisfies_d(A)
4.426 @@ -641,21 +576,27 @@
4.427
4.428    satisfies_is_d :: "[i=>o,i,i,i,i]=>o"
4.429     "satisfies_is_d(M,A,h) ==
4.430 -    \<lambda>p. is_lambda(M, list(A),
4.431 -        \<lambda>env z. \<exists>rp[M]. is_depth_apply(M,h,p,rp) &
4.432 -           is_bool_of_o(M,
4.433 -                \<forall>x[M]. \<forall>xenv[M]. \<forall>hp[M].
4.434 -                       x\<in>A --> is_Cons(M,x,env,xenv) -->
4.435 -                       fun_apply(M,rp,xenv,hp) --> number1(M,hp),
4.436 -                  z))"
4.437 +    \<lambda>p zz. \<forall>lA[M]. is_list(M,A,lA) -->
4.438 +             is_lambda(M, lA,
4.439 +                \<lambda>env z. \<exists>rp[M]. is_depth_apply(M,h,p,rp) &
4.440 +                    is_bool_of_o(M,
4.441 +                           \<forall>x[M]. \<forall>xenv[M]. \<forall>hp[M].
4.442 +                              x\<in>A --> is_Cons(M,x,env,xenv) -->
4.443 +                              fun_apply(M,rp,xenv,hp) --> number1(M,hp),
4.444 +                  z),
4.445 +               zz)"
4.446
4.447    satisfies_MH :: "[i=>o,i,i,i,i]=>o"
4.448 +    --{*The variable @{term u} is unused, but gives @{term satisfies_MH}
4.449 +        the correct arity.*}
4.450     "satisfies_MH ==
4.451 -    \<lambda>M A u f. is_lambda
4.452 -	 (M, formula,
4.453 -          is_formula_case (M, satisfies_is_a(M,A),
4.454 -                           satisfies_is_b(M,A),
4.455 -                           satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)))"
4.456 +    \<lambda>M A u f zz.
4.457 +         \<forall>fml[M]. is_formula(M,fml) -->
4.458 +             is_lambda (M, fml,
4.459 +               is_formula_case (M, satisfies_is_a(M,A),
4.460 +                                satisfies_is_b(M,A),
4.461 +                                satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)),
4.462 +               zz)"
4.463
4.464
4.465  text{*Further constraints on the class @{term M} in order to prove
4.466 @@ -1003,39 +944,305 @@
4.467
4.468
4.469
4.470 +subsubsection{*The Operator @{term is_depth_apply}, Internalized*}
4.471 +
4.472 +(* is_depth_apply(M,h,p,z) ==
4.473 +    \<exists>dp[M]. \<exists>sdp[M]. \<exists>hsdp[M].
4.474 +      2        1         0
4.475 +	finite_ordinal(M,dp) & is_depth(M,p,dp) & successor(M,dp,sdp) &
4.476 +	fun_apply(M,h,sdp,hsdp) & fun_apply(M,hsdp,p,z) *)
4.477 +constdefs depth_apply_fm :: "[i,i,i]=>i"
4.478 +    "depth_apply_fm(h,p,z) ==
4.479 +       Exists(Exists(Exists(
4.480 +        And(finite_ordinal_fm(2),
4.481 +         And(depth_fm(p#+3,2),
4.482 +          And(succ_fm(2,1),
4.483 +           And(fun_apply_fm(h#+3,1,0), fun_apply_fm(0,p#+3,z#+3))))))))"
4.484 +
4.485 +lemma depth_apply_type [TC]:
4.486 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> depth_apply_fm(x,y,z) \<in> formula"
4.488 +
4.489 +lemma sats_depth_apply_fm [simp]:
4.490 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
4.491 +    ==> sats(A, depth_apply_fm(x,y,z), env) <->
4.492 +        is_depth_apply(**A, nth(x,env), nth(y,env), nth(z,env))"
4.493 +by (simp add: depth_apply_fm_def is_depth_apply_def)
4.494 +
4.495 +lemma depth_apply_iff_sats:
4.496 +    "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
4.497 +        i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
4.498 +     ==> is_depth_apply(**A, x, y, z) <-> sats(A, depth_apply_fm(i,j,k), env)"
4.499 +by simp
4.500 +
4.501 +lemma depth_apply_reflection:
4.502 +     "REFLECTS[\<lambda>x. is_depth_apply(L,f(x),g(x),h(x)),
4.503 +               \<lambda>i x. is_depth_apply(**Lset(i),f(x),g(x),h(x))]"
4.504 +apply (simp only: is_depth_apply_def setclass_simps)
4.505 +apply (intro FOL_reflections function_reflections depth_reflection
4.506 +             finite_ordinal_reflection)
4.507 +done
4.508 +
4.509 +
4.510 +subsubsection{*The Operator @{term satisfies_is_a}, Internalized*}
4.511 +
4.512 +(* satisfies_is_a(M,A) ==
4.513 +    \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) -->
4.514 +             is_lambda(M, lA,
4.515 +		\<lambda>env z. is_bool_of_o(M,
4.516 +                      \<exists>nx[M]. \<exists>ny[M].
4.517 + 		       is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & nx \<in> ny, z),
4.518 +                zz)  *)
4.519 +
4.520 +constdefs satisfies_is_a_fm :: "[i,i,i,i]=>i"
4.521 + "satisfies_is_a_fm(A,x,y,z) ==
4.522 +   Forall(
4.523 +     Implies(is_list_fm(succ(A),0),
4.524 +       lambda_fm(
4.525 +         bool_of_o_fm(Exists(
4.526 +                       Exists(And(nth_fm(x#+6,3,1),
4.527 +                               And(nth_fm(y#+6,3,0),
4.528 +                                   Member(1,0))))), 0),
4.529 +         0, succ(z))))"
4.530 +
4.531 +lemma satisfies_is_a_type [TC]:
4.532 +     "[| A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
4.533 +      ==> satisfies_is_a_fm(A,x,y,z) \<in> formula"
4.535 +
4.536 +lemma sats_satisfies_is_a_fm [simp]:
4.537 +   "[| u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
4.538 +    ==> sats(A, satisfies_is_a_fm(u,x,y,z), env) <->
4.539 +        satisfies_is_a(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
4.540 +apply (frule_tac x=x in lt_length_in_nat, assumption)
4.541 +apply (frule_tac x=y in lt_length_in_nat, assumption)
4.542 +apply (simp add: satisfies_is_a_fm_def satisfies_is_a_def sats_lambda_fm
4.543 +                 sats_bool_of_o_fm)
4.544 +done
4.545 +
4.546 +lemma satisfies_is_a_iff_sats:
4.547 +  "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
4.548 +      u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
4.549 +   ==> satisfies_is_a(**A,nu,nx,ny,nz) <->
4.550 +       sats(A, satisfies_is_a_fm(u,x,y,z), env)"
4.551 +by simp
4.552 +
4.553  theorem satisfies_is_a_reflection:
4.554       "REFLECTS[\<lambda>x. satisfies_is_a(L,f(x),g(x),h(x),g'(x)),
4.555                 \<lambda>i x. satisfies_is_a(**Lset(i),f(x),g(x),h(x),g'(x))]"
4.556  apply (unfold satisfies_is_a_def)
4.557  apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection
4.558 -             nth_reflection)
4.559 +             nth_reflection is_list_reflection)
4.560  done
4.561
4.562
4.563 +subsubsection{*The Operator @{term satisfies_is_b}, Internalized*}
4.564 +
4.565 +(* satisfies_is_b(M,A) ==
4.566 +    \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) -->
4.567 +             is_lambda(M, lA,
4.568 +                \<lambda>env z. is_bool_of_o(M,
4.569 +                      \<exists>nx[M]. is_nth(M,x,env,nx) & is_nth(M,y,env,nx), z),
4.570 +                zz) *)
4.571 +
4.572 +constdefs satisfies_is_b_fm :: "[i,i,i,i]=>i"
4.573 + "satisfies_is_b_fm(A,x,y,z) ==
4.574 +   Forall(
4.575 +     Implies(is_list_fm(succ(A),0),
4.576 +       lambda_fm(
4.577 +         bool_of_o_fm(Exists(And(nth_fm(x#+5,2,0), nth_fm(y#+5,2,0))), 0),
4.578 +         0, succ(z))))"
4.579 +
4.580 +lemma satisfies_is_b_type [TC]:
4.581 +     "[| A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
4.582 +      ==> satisfies_is_b_fm(A,x,y,z) \<in> formula"
4.584 +
4.585 +lemma sats_satisfies_is_b_fm [simp]:
4.586 +   "[| u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
4.587 +    ==> sats(A, satisfies_is_b_fm(u,x,y,z), env) <->
4.588 +        satisfies_is_b(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
4.589 +apply (frule_tac x=x in lt_length_in_nat, assumption)
4.590 +apply (frule_tac x=y in lt_length_in_nat, assumption)
4.591 +apply (simp add: satisfies_is_b_fm_def satisfies_is_b_def sats_lambda_fm
4.592 +                 sats_bool_of_o_fm)
4.593 +done
4.594 +
4.595 +lemma satisfies_is_b_iff_sats:
4.596 +  "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
4.597 +      u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
4.598 +   ==> satisfies_is_b(**A,nu,nx,ny,nz) <->
4.599 +       sats(A, satisfies_is_b_fm(u,x,y,z), env)"
4.600 +by simp
4.601 +
4.602  theorem satisfies_is_b_reflection:
4.603       "REFLECTS[\<lambda>x. satisfies_is_b(L,f(x),g(x),h(x),g'(x)),
4.604                 \<lambda>i x. satisfies_is_b(**Lset(i),f(x),g(x),h(x),g'(x))]"
4.605  apply (unfold satisfies_is_b_def)
4.606  apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection
4.607 -             nth_reflection)
4.608 +             nth_reflection is_list_reflection)
4.609  done
4.610
4.611 +
4.612 +subsubsection{*The Operator @{term satisfies_is_c}, Internalized*}
4.613 +
4.614 +(* satisfies_is_c(M,A,h) ==
4.615 +    \<lambda>p q zz. \<forall>lA[M]. is_list(M,A,lA) -->
4.616 +             is_lambda(M, lA, \<lambda>env z. \<exists>hp[M]. \<exists>hq[M].
4.617 +		 (\<exists>rp[M]. is_depth_apply(M,h,p,rp) & fun_apply(M,rp,env,hp)) &
4.618 +		 (\<exists>rq[M]. is_depth_apply(M,h,q,rq) & fun_apply(M,rq,env,hq)) &
4.619 +                 (\<exists>pq[M]. is_and(M,hp,hq,pq) & is_not(M,pq,z)),
4.620 +                zz) *)
4.621 +
4.622 +constdefs satisfies_is_c_fm :: "[i,i,i,i,i]=>i"
4.623 + "satisfies_is_c_fm(A,h,p,q,zz) ==
4.624 +   Forall(
4.625 +     Implies(is_list_fm(succ(A),0),
4.626 +       lambda_fm(
4.627 +         Exists(Exists(
4.628 +          And(Exists(And(depth_apply_fm(h#+7,p#+7,0), fun_apply_fm(0,4,2))),
4.629 +          And(Exists(And(depth_apply_fm(h#+7,q#+7,0), fun_apply_fm(0,4,1))),
4.630 +              Exists(And(and_fm(2,1,0), not_fm(0,3))))))),
4.631 +         0, succ(zz))))"
4.632 +
4.633 +lemma satisfies_is_c_type [TC]:
4.634 +     "[| A \<in> nat; h \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
4.635 +      ==> satisfies_is_c_fm(A,h,x,y,z) \<in> formula"
4.637 +
4.638 +lemma sats_satisfies_is_c_fm [simp]:
4.639 +   "[| u \<in> nat; v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
4.640 +    ==> sats(A, satisfies_is_c_fm(u,v,x,y,z), env) <->
4.641 +        satisfies_is_c(**A, nth(u,env), nth(v,env), nth(x,env),
4.642 +                            nth(y,env), nth(z,env))"
4.643 +by (simp add: satisfies_is_c_fm_def satisfies_is_c_def sats_lambda_fm)
4.644 +
4.645 +lemma satisfies_is_c_iff_sats:
4.646 +  "[| nth(u,env) = nu; nth(v,env) = nv; nth(x,env) = nx; nth(y,env) = ny;
4.647 +      nth(z,env) = nz;
4.648 +      u \<in> nat; v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
4.649 +   ==> satisfies_is_c(**A,nu,nv,nx,ny,nz) <->
4.650 +       sats(A, satisfies_is_c_fm(u,v,x,y,z), env)"
4.651 +by simp
4.652 +
4.653  theorem satisfies_is_c_reflection:
4.654       "REFLECTS[\<lambda>x. satisfies_is_c(L,f(x),g(x),h(x),g'(x),h'(x)),
4.655                 \<lambda>i x. satisfies_is_c(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
4.656 -apply (unfold satisfies_is_c_def )
4.657 +apply (unfold satisfies_is_c_def)
4.658  apply (intro FOL_reflections function_reflections is_lambda_reflection
4.659 -             bool_of_o_reflection not_reflection and_reflection
4.660 -             nth_reflection depth_apply_reflection)
4.661 +             extra_reflections nth_reflection depth_apply_reflection
4.662 +             is_list_reflection)
4.663  done
4.664
4.665 +subsubsection{*The Operator @{term satisfies_is_d}, Internalized*}
4.666 +
4.667 +(* satisfies_is_d(M,A,h) ==
4.668 +    \<lambda>p zz. \<forall>lA[M]. is_list(M,A,lA) -->
4.669 +             is_lambda(M, lA,
4.670 +                \<lambda>env z. \<exists>rp[M]. is_depth_apply(M,h,p,rp) &
4.671 +                    is_bool_of_o(M,
4.672 +                           \<forall>x[M]. \<forall>xenv[M]. \<forall>hp[M].
4.673 +                              x\<in>A --> is_Cons(M,x,env,xenv) -->
4.674 +                              fun_apply(M,rp,xenv,hp) --> number1(M,hp),
4.675 +                  z),
4.676 +               zz) *)
4.677 +
4.678 +constdefs satisfies_is_d_fm :: "[i,i,i,i]=>i"
4.679 + "satisfies_is_d_fm(A,h,p,zz) ==
4.680 +   Forall(
4.681 +     Implies(is_list_fm(succ(A),0),
4.682 +       lambda_fm(
4.683 +         Exists(
4.684 +           And(depth_apply_fm(h#+5,p#+5,0),
4.685 +               bool_of_o_fm(
4.686 +                Forall(Forall(Forall(
4.687 +                 Implies(Member(2,A#+8),
4.688 +                  Implies(Cons_fm(2,5,1),
4.689 +                   Implies(fun_apply_fm(3,1,0), number1_fm(0))))))), 1))),
4.690 +         0, succ(zz))))"
4.691 +
4.692 +lemma satisfies_is_d_type [TC]:
4.693 +     "[| A \<in> nat; h \<in> nat; x \<in> nat; z \<in> nat |]
4.694 +      ==> satisfies_is_d_fm(A,h,x,z) \<in> formula"
4.696 +
4.697 +lemma sats_satisfies_is_d_fm [simp]:
4.698 +   "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
4.699 +    ==> sats(A, satisfies_is_d_fm(u,x,y,z), env) <->
4.700 +        satisfies_is_d(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
4.701 +by (simp add: satisfies_is_d_fm_def satisfies_is_d_def sats_lambda_fm
4.702 +              sats_bool_of_o_fm)
4.703 +
4.704 +lemma satisfies_is_d_iff_sats:
4.705 +  "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
4.706 +      u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
4.707 +   ==> satisfies_is_d(**A,nu,nx,ny,nz) <->
4.708 +       sats(A, satisfies_is_d_fm(u,x,y,z), env)"
4.709 +by simp
4.710 +
4.711  theorem satisfies_is_d_reflection:
4.712       "REFLECTS[\<lambda>x. satisfies_is_d(L,f(x),g(x),h(x),g'(x)),
4.713                 \<lambda>i x. satisfies_is_d(**Lset(i),f(x),g(x),h(x),g'(x))]"
4.714  apply (unfold satisfies_is_d_def )
4.715  apply (intro FOL_reflections function_reflections is_lambda_reflection
4.716 -             bool_of_o_reflection not_reflection and_reflection
4.717 -             nth_reflection depth_apply_reflection Cons_reflection)
4.718 +             extra_reflections nth_reflection depth_apply_reflection
4.719 +             is_list_reflection)
4.720 +done
4.721 +
4.722 +
4.723 +subsubsection{*The Operator @{term satisfies_MH}, Internalized*}
4.724 +
4.725 +(* satisfies_MH ==
4.726 +    \<lambda>M A u f zz.
4.727 +         \<forall>fml[M]. is_formula(M,fml) -->
4.728 +             is_lambda (M, fml,
4.729 +               is_formula_case (M, satisfies_is_a(M,A),
4.730 +                                satisfies_is_b(M,A),
4.731 +                                satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)),
4.732 +               zz) *)
4.733 +
4.734 +constdefs satisfies_MH_fm :: "[i,i,i,i]=>i"
4.735 + "satisfies_MH_fm(A,u,f,zz) ==
4.736 +   Forall(
4.737 +     Implies(is_formula_fm(0),
4.738 +       lambda_fm(
4.739 +         formula_case_fm(satisfies_is_a_fm(A#+7,2,1,0),
4.740 +                         satisfies_is_b_fm(A#+7,2,1,0),
4.741 +                         satisfies_is_c_fm(A#+7,f#+7,2,1,0),
4.742 +                         satisfies_is_d_fm(A#+6,f#+6,1,0),
4.743 +                         1, 0),
4.744 +         0, succ(zz))))"
4.745 +
4.746 +lemma satisfies_MH_type [TC]:
4.747 +     "[| A \<in> nat; u \<in> nat; x \<in> nat; z \<in> nat |]
4.748 +      ==> satisfies_MH_fm(A,u,x,z) \<in> formula"
4.750 +
4.751 +lemma sats_satisfies_MH_fm [simp]:
4.752 +   "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
4.753 +    ==> sats(A, satisfies_MH_fm(u,x,y,z), env) <->
4.754 +        satisfies_MH(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
4.755 +by (simp add: satisfies_MH_fm_def satisfies_MH_def sats_lambda_fm
4.756 +              sats_formula_case_fm)
4.757 +
4.758 +lemma satisfies_MH_iff_sats:
4.759 +  "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
4.760 +      u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
4.761 +   ==> satisfies_MH(**A,nu,nx,ny,nz) <->
4.762 +       sats(A, satisfies_MH_fm(u,x,y,z), env)"
4.763 +by simp
4.764 +
4.765 +lemmas satisfies_reflections =
4.766 +       is_lambda_reflection is_formula_reflection
4.767 +       is_formula_case_reflection
4.768 +       satisfies_is_a_reflection satisfies_is_b_reflection
4.769 +       satisfies_is_c_reflection satisfies_is_d_reflection
4.770 +
4.771 +theorem satisfies_MH_reflection:
4.772 +     "REFLECTS[\<lambda>x. satisfies_MH(L,f(x),g(x),h(x),g'(x)),
4.773 +               \<lambda>i x. satisfies_MH(**Lset(i),f(x),g(x),h(x),g'(x))]"
4.774 +apply (unfold satisfies_MH_def)
4.775 +apply (intro FOL_reflections satisfies_reflections)
4.776  done
4.777
4.778
4.779 @@ -1044,17 +1251,32 @@
4.780               is_wfrec (L, satisfies_MH(L,A), mesa, u, y)),
4.781      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
4.782               is_wfrec (**Lset(i), satisfies_MH(**Lset(i),A), mesa, u, y))]"
4.783 -apply (unfold satisfies_MH_def)
4.784 -apply (intro FOL_reflections function_reflections is_wfrec_reflection
4.785 -             is_lambda_reflection)
4.786 -apply (simp only: is_formula_case_def)
4.787 -apply (intro FOL_reflections finite_ordinal_reflection mem_formula_reflection
4.788 -          Member_reflection Equal_reflection Nand_reflection Forall_reflection
4.789 -          satisfies_is_a_reflection satisfies_is_b_reflection
4.790 -          satisfies_is_c_reflection satisfies_is_d_reflection)
4.791 +by (intro FOL_reflections function_reflections satisfies_MH_reflection
4.792 +          is_wfrec_reflection)
4.793 +
4.794 +lemma formula_rec_replacement:
4.795 +      --{*For the @{term transrec}*}
4.796 +   "[|n \<in> nat; L(A)|] ==> transrec_replacement(L, satisfies_MH(L,A), n)"
4.797 +apply (subgoal_tac "L(Memrel(eclose({n})))")
4.798 + prefer 2 apply (simp add: nat_into_M)
4.799 +apply (rule transrec_replacementI)
4.801 +apply (rule strong_replacementI)
4.802 +apply (rule rallI)
4.803 +apply (rename_tac B)
4.804 +apply (rule separation_CollectI)
4.805 +apply (rule_tac A="{B,A,n,z,Memrel(eclose({n}))}" in subset_LsetE, blast )
4.806 +apply (rule ReflectsE [OF formula_rec_replacement_Reflects], assumption)
4.807 +apply (drule subset_Lset_ltD, assumption)
4.808 +apply (erule reflection_imp_L_separation)
4.809 +  apply (simp_all add: lt_Ord2 Memrel_closed)
4.810 +apply (elim conjE)
4.811 +apply (rule DPow_LsetI)
4.812 +apply (rename_tac v)
4.813 +apply (rule bex_iff_sats conj_iff_sats)+
4.814 +apply (rule_tac env = "[u,v,A,n,B,Memrel(eclose({n}))]" in mem_iff_sats)
4.815 +apply (rule sep_rules | simp)+
4.816 +apply (rule sep_rules satisfies_MH_iff_sats is_wfrec_iff_sats | simp)+
4.817  done
4.818
4.819  end
4.820 -
4.821 -
4.822 -
```
```     5.1 --- a/src/ZF/IsaMakefile	Tue Aug 13 12:16:14 2002 +0200
5.2 +++ b/src/ZF/IsaMakefile	Tue Aug 13 17:42:34 2002 +0200
5.3 @@ -79,7 +79,8 @@
5.4
5.5  \$(LOG)/ZF-Constructible.gz: \$(OUT)/ZF  Constructible/ROOT.ML \
5.6    Constructible/Datatype_absolute.thy\
5.7 -  Constructible/Formula.thy     Constructible/Relative.thy \
5.8 +  Constructible/Formula.thy Constructible/Internalize.thy \
5.9 +  Constructible/Relative.thy \
5.10    Constructible/L_axioms.thy    Constructible/Wellorderings.thy \
5.11    Constructible/MetaExists.thy  Constructible/Normal.thy \
5.12    Constructible/Rec_Separation.thy Constructible/Separation.thy \
```