In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
authorpaulson
Tue Aug 13 17:42:34 2002 +0200 (2002-08-13)
changeset 134966f0c57def6d5
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
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/Satisfies_absolute.thy
src/ZF/IsaMakefile
     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.16 +by (simp add: Inl_fm_def)
    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.45 +by (simp add: Inr_fm_def)
    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.74 +by (simp add: Nil_fm_def)
    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.104 +by (simp add: Cons_fm_def)
   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.134 +by (simp add: quasilist_fm_def)
   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.171 +by (simp add: hd_fm_def) 
   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.207 +by (simp add: tl_fm_def)
   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.242 +by (simp add: bool_of_o_fm_def)
   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.255 +by (simp add: sats_bool_of_o_fm)
   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.289 +by (simp add: lambda_fm_def) 
   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.334 +by (simp add: Member_fm_def)
   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.346 +by (simp add: sats_Member_fm)
   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.366 +by (simp add: Equal_fm_def)
   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.378 +by (simp add: sats_Equal_fm)
   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.398 +by (simp add: Nand_fm_def)
   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.410 +by (simp add: sats_Nand_fm)
   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.428 +by (simp add: Forall_fm_def)
   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.440 +by (simp add: sats_Forall_fm)
   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.461 +by (simp add: and_fm_def)
   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.495 +by (simp add: or_fm_def)
   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.529 +by (simp add: not_fm_def)
   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.11  header {*Separation for Facts About Recursion*}
    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.34  apply (simp_all add: setclass_def)
    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.89 -by (simp add: Inl_fm_def)
    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.118 -by (simp add: Inr_fm_def)
   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.147 -by (simp add: Nil_fm_def)
   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.177 -by (simp add: Cons_fm_def)
   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.207 -by (simp add: quasilist_fm_def)
   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.244 -by (simp add: hd_fm_def) 
   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.280 -by (simp add: tl_fm_def)
   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.45 +by (simp add: list_N_fm_def)
    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.78 -by (simp add: lambda_fm_def) 
    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.83 +by (simp add: sats_list_N_fm)
    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.146 -by (simp add: Member_fm_def)
   4.147 +lemma mem_list_type [TC]:
   4.148 +     "[| x \<in> nat; y \<in> nat |] ==> mem_list_fm(x,y) \<in> formula"
   4.149 +by (simp add: mem_list_fm_def)
   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.165 -by (simp add: sats_Member_fm)
   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.195 -by (simp add: Equal_fm_def)
   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.208 -by (simp add: sats_Equal_fm)
   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.232 -by (simp add: Nand_fm_def)
   4.233 +lemma is_list_type [TC]:
   4.234 +     "[| x \<in> nat; y \<in> nat |] ==> is_list_fm(x,y) \<in> formula"
   4.235 +by (simp add: is_list_fm_def)
   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.247 -by (simp add: sats_Nand_fm)
   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.269 -by (simp add: Forall_fm_def)
   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.286 -by (simp add: sats_Forall_fm)
   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.335 +by (simp add: is_formula_fm_def)
   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.487 +by (simp add: depth_apply_fm_def)
   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.534 +by (simp add: satisfies_is_a_fm_def)
   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.583 +by (simp add: satisfies_is_b_fm_def)
   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.636 +by (simp add: satisfies_is_c_fm_def)
   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.695 +by (simp add: satisfies_is_d_fm_def)
   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.749 +by (simp add: satisfies_MH_fm_def)
   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.800 +apply (simp add: nat_into_M) 
   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 \