new file Constructible/Satisfies_absolute.thy
authorpaulson
Tue Aug 13 11:03:11 2002 +0200 (2002-08-13)
changeset 134941c44289716ae
parent 13493 5aa68c051725
child 13495 af27202d6d1c
new file Constructible/Satisfies_absolute.thy
src/ZF/Constructible/ROOT.ML
src/ZF/Constructible/Satisfies_absolute.thy
src/ZF/IsaMakefile
     1.1 --- a/src/ZF/Constructible/ROOT.ML	Mon Aug 12 18:01:44 2002 +0200
     1.2 +++ b/src/ZF/Constructible/ROOT.ML	Tue Aug 13 11:03:11 2002 +0200
     1.3 @@ -8,7 +8,4 @@
     1.4  Build using	isatool usedir  -d pdf ZF Constructible
     1.5  *)
     1.6  
     1.7 -use_thy "Reflection";
     1.8 -use_thy "WF_absolute";
     1.9 -use_thy "Rec_Separation";
    1.10 -use_thy "Datatype_absolute";
    1.11 +use_thy "Satisfies_absolute";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/ZF/Constructible/Satisfies_absolute.thy	Tue Aug 13 11:03:11 2002 +0200
     2.3 @@ -0,0 +1,1060 @@
     2.4 +(*  Title:      ZF/Constructible/Satisfies_absolute.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   2002  University of Cambridge
     2.8 +*)
     2.9 +
    2.10 +theory Satisfies_absolute = Datatype_absolute + Rec_Separation: 
    2.11 +
    2.12 +
    2.13 +subsection{*More Internalizations*}
    2.14 +
    2.15 +lemma and_reflection:
    2.16 +     "REFLECTS[\<lambda>x. is_and(L,f(x),g(x),h(x)),
    2.17 +               \<lambda>i x. is_and(**Lset(i),f(x),g(x),h(x))]"
    2.18 +apply (simp only: is_and_def setclass_simps)
    2.19 +apply (intro FOL_reflections function_reflections)
    2.20 +done
    2.21 +
    2.22 +lemma not_reflection:
    2.23 +     "REFLECTS[\<lambda>x. is_not(L,f(x),g(x)),
    2.24 +               \<lambda>i x. is_not(**Lset(i),f(x),g(x))]"
    2.25 +apply (simp only: is_not_def setclass_simps)
    2.26 +apply (intro FOL_reflections function_reflections)
    2.27 +done
    2.28 +
    2.29 +subsubsection{*The Operator @{term is_lambda}*}
    2.30 +
    2.31 +text{*The two arguments of @{term p} are always 1, 0. Remember that
    2.32 + @{term p} will be enclosed by three quantifiers.*}
    2.33 +
    2.34 +(* is_lambda :: "[i=>o, i, [i,i]=>o, i] => o"
    2.35 +    "is_lambda(M, A, is_b, z) == 
    2.36 +       \<forall>p[M]. p \<in> z <->
    2.37 +        (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))" *)
    2.38 +constdefs lambda_fm :: "[i, i, i]=>i"
    2.39 + "lambda_fm(p,A,z) == 
    2.40 +    Forall(Iff(Member(0,succ(z)),
    2.41 +            Exists(Exists(And(Member(1,A#+3),
    2.42 +                           And(pair_fm(1,0,2), p))))))"
    2.43 +
    2.44 +text{*We call @{term p} with arguments x, y by equating them with 
    2.45 +  the corresponding quantified variables with de Bruijn indices 1, 0.*}
    2.46 +
    2.47 +lemma is_lambda_type [TC]:
    2.48 +     "[| p \<in> formula; x \<in> nat; y \<in> nat |] 
    2.49 +      ==> lambda_fm(p,x,y) \<in> formula"
    2.50 +by (simp add: lambda_fm_def) 
    2.51 +
    2.52 +lemma sats_lambda_fm:
    2.53 +  assumes is_b_iff_sats: 
    2.54 +      "!!a0 a1 a2. 
    2.55 +        [|a0\<in>A; a1\<in>A; a2\<in>A|] 
    2.56 +        ==> is_b(a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,env))))"
    2.57 +  shows 
    2.58 +      "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
    2.59 +       ==> sats(A, lambda_fm(p,x,y), env) <-> 
    2.60 +           is_lambda(**A, nth(x,env), is_b, nth(y,env))"
    2.61 +by (simp add: lambda_fm_def sats_is_recfun_fm is_lambda_def is_b_iff_sats [THEN iff_sym]) 
    2.62 +
    2.63 +
    2.64 +lemma is_lambda_iff_sats:
    2.65 +  assumes is_b_iff_sats: 
    2.66 +      "!!a0 a1 a2. 
    2.67 +        [|a0\<in>A; a1\<in>A; a2\<in>A|] 
    2.68 +        ==> is_b(a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,env))))"
    2.69 +  shows
    2.70 +  "[|nth(i,env) = x; nth(j,env) = y; 
    2.71 +      i \<in> nat; j \<in> nat; env \<in> list(A)|]
    2.72 +   ==> is_lambda(**A, x, is_b, y) <-> sats(A, lambda_fm(p,i,j), env)" 
    2.73 +by (simp add: sats_lambda_fm [OF is_b_iff_sats])
    2.74 +
    2.75 +theorem is_lambda_reflection:
    2.76 +  assumes is_b_reflection:
    2.77 +    "!!f' f g h. REFLECTS[\<lambda>x. is_b(L, f'(x), f(x), g(x)), 
    2.78 +                     \<lambda>i x. is_b(**Lset(i), f'(x), f(x), g(x))]"
    2.79 +  shows "REFLECTS[\<lambda>x. is_lambda(L, A(x), is_b(L,x), f(x)), 
    2.80 +               \<lambda>i x. is_lambda(**Lset(i), A(x), is_b(**Lset(i),x), f(x))]"
    2.81 +apply (simp (no_asm_use) only: is_lambda_def setclass_simps)
    2.82 +apply (intro FOL_reflections is_b_reflection pair_reflection)
    2.83 +done
    2.84 +
    2.85 +
    2.86 +subsubsection{*The Operator @{term is_Member}, Internalized*}
    2.87 +
    2.88 +(*    "is_Member(M,x,y,Z) ==
    2.89 +	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)" *)
    2.90 +constdefs Member_fm :: "[i,i,i]=>i"
    2.91 +    "Member_fm(x,y,Z) ==
    2.92 +       Exists(Exists(And(pair_fm(x#+2,y#+2,1), 
    2.93 +                      And(Inl_fm(1,0), Inl_fm(0,Z#+2)))))"
    2.94 +
    2.95 +lemma is_Member_type [TC]:
    2.96 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Member_fm(x,y,z) \<in> formula"
    2.97 +by (simp add: Member_fm_def)
    2.98 +
    2.99 +lemma sats_Member_fm [simp]:
   2.100 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   2.101 +    ==> sats(A, Member_fm(x,y,z), env) <->
   2.102 +        is_Member(**A, nth(x,env), nth(y,env), nth(z,env))"
   2.103 +by (simp add: Member_fm_def is_Member_def)
   2.104 +
   2.105 +lemma Member_iff_sats:
   2.106 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   2.107 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   2.108 +       ==> is_Member(**A, x, y, z) <-> sats(A, Member_fm(i,j,k), env)"
   2.109 +by (simp add: sats_Member_fm)
   2.110 +
   2.111 +theorem Member_reflection:
   2.112 +     "REFLECTS[\<lambda>x. is_Member(L,f(x),g(x),h(x)),
   2.113 +               \<lambda>i x. is_Member(**Lset(i),f(x),g(x),h(x))]"
   2.114 +apply (simp only: is_Member_def setclass_simps)
   2.115 +apply (intro FOL_reflections pair_reflection Inl_reflection)
   2.116 +done
   2.117 +
   2.118 +subsubsection{*The Operator @{term is_Equal}, Internalized*}
   2.119 +
   2.120 +(*    "is_Equal(M,x,y,Z) ==
   2.121 +	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)" *)
   2.122 +constdefs Equal_fm :: "[i,i,i]=>i"
   2.123 +    "Equal_fm(x,y,Z) ==
   2.124 +       Exists(Exists(And(pair_fm(x#+2,y#+2,1), 
   2.125 +                      And(Inr_fm(1,0), Inl_fm(0,Z#+2)))))"
   2.126 +
   2.127 +lemma is_Equal_type [TC]:
   2.128 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Equal_fm(x,y,z) \<in> formula"
   2.129 +by (simp add: Equal_fm_def)
   2.130 +
   2.131 +lemma sats_Equal_fm [simp]:
   2.132 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   2.133 +    ==> sats(A, Equal_fm(x,y,z), env) <->
   2.134 +        is_Equal(**A, nth(x,env), nth(y,env), nth(z,env))"
   2.135 +by (simp add: Equal_fm_def is_Equal_def)
   2.136 +
   2.137 +lemma Equal_iff_sats:
   2.138 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   2.139 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   2.140 +       ==> is_Equal(**A, x, y, z) <-> sats(A, Equal_fm(i,j,k), env)"
   2.141 +by (simp add: sats_Equal_fm)
   2.142 +
   2.143 +theorem Equal_reflection:
   2.144 +     "REFLECTS[\<lambda>x. is_Equal(L,f(x),g(x),h(x)),
   2.145 +               \<lambda>i x. is_Equal(**Lset(i),f(x),g(x),h(x))]"
   2.146 +apply (simp only: is_Equal_def setclass_simps)
   2.147 +apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection)
   2.148 +done
   2.149 +
   2.150 +subsubsection{*The Operator @{term is_Nand}, Internalized*}
   2.151 +
   2.152 +(*    "is_Nand(M,x,y,Z) ==
   2.153 +	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)" *)
   2.154 +constdefs Nand_fm :: "[i,i,i]=>i"
   2.155 +    "Nand_fm(x,y,Z) ==
   2.156 +       Exists(Exists(And(pair_fm(x#+2,y#+2,1), 
   2.157 +                      And(Inl_fm(1,0), Inr_fm(0,Z#+2)))))"
   2.158 +
   2.159 +lemma is_Nand_type [TC]:
   2.160 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Nand_fm(x,y,z) \<in> formula"
   2.161 +by (simp add: Nand_fm_def)
   2.162 +
   2.163 +lemma sats_Nand_fm [simp]:
   2.164 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   2.165 +    ==> sats(A, Nand_fm(x,y,z), env) <->
   2.166 +        is_Nand(**A, nth(x,env), nth(y,env), nth(z,env))"
   2.167 +by (simp add: Nand_fm_def is_Nand_def)
   2.168 +
   2.169 +lemma Nand_iff_sats:
   2.170 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   2.171 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   2.172 +       ==> is_Nand(**A, x, y, z) <-> sats(A, Nand_fm(i,j,k), env)"
   2.173 +by (simp add: sats_Nand_fm)
   2.174 +
   2.175 +theorem Nand_reflection:
   2.176 +     "REFLECTS[\<lambda>x. is_Nand(L,f(x),g(x),h(x)),
   2.177 +               \<lambda>i x. is_Nand(**Lset(i),f(x),g(x),h(x))]"
   2.178 +apply (simp only: is_Nand_def setclass_simps)
   2.179 +apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection)
   2.180 +done
   2.181 +
   2.182 +subsubsection{*The Operator @{term is_Forall}, Internalized*}
   2.183 +
   2.184 +(* "is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)" *)
   2.185 +constdefs Forall_fm :: "[i,i]=>i"
   2.186 +    "Forall_fm(x,Z) ==
   2.187 +       Exists(And(Inr_fm(succ(x),0), Inr_fm(0,succ(Z))))"
   2.188 +
   2.189 +lemma is_Forall_type [TC]:
   2.190 +     "[| x \<in> nat; y \<in> nat |] ==> Forall_fm(x,y) \<in> formula"
   2.191 +by (simp add: Forall_fm_def)
   2.192 +
   2.193 +lemma sats_Forall_fm [simp]:
   2.194 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   2.195 +    ==> sats(A, Forall_fm(x,y), env) <->
   2.196 +        is_Forall(**A, nth(x,env), nth(y,env))"
   2.197 +by (simp add: Forall_fm_def is_Forall_def)
   2.198 +
   2.199 +lemma Forall_iff_sats:
   2.200 +      "[| nth(i,env) = x; nth(j,env) = y; 
   2.201 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
   2.202 +       ==> is_Forall(**A, x, y) <-> sats(A, Forall_fm(i,j), env)"
   2.203 +by (simp add: sats_Forall_fm)
   2.204 +
   2.205 +theorem Forall_reflection:
   2.206 +     "REFLECTS[\<lambda>x. is_Forall(L,f(x),g(x)),
   2.207 +               \<lambda>i x. is_Forall(**Lset(i),f(x),g(x))]"
   2.208 +apply (simp only: is_Forall_def setclass_simps)
   2.209 +apply (intro FOL_reflections pair_reflection Inr_reflection)
   2.210 +done
   2.211 +
   2.212 +
   2.213 +subsubsection{*The Formula @{term is_formula_N}, Internalized*}
   2.214 +
   2.215 +(* "is_nth(M,n,l,Z) == 
   2.216 +      \<exists>X[M]. \<exists>sn[M]. \<exists>msn[M]. 
   2.217 +       2       1       0
   2.218 +       successor(M,n,sn) & membership(M,sn,msn) &
   2.219 +       is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) &
   2.220 +       is_hd(M,X,Z)" *)
   2.221 +
   2.222 +(* "is_formula_N(M,n,Z) == 
   2.223 +      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M]. 
   2.224 +          2       1       0
   2.225 +       empty(M,zero) & 
   2.226 +       successor(M,n,sn) & membership(M,sn,msn) &
   2.227 +       is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)" *) 
   2.228 +constdefs formula_N_fm :: "[i,i]=>i"
   2.229 +  "formula_N_fm(n,Z) == 
   2.230 +     Exists(Exists(Exists(
   2.231 +       And(empty_fm(2),
   2.232 +         And(succ_fm(n#+3,1),
   2.233 +          And(Memrel_fm(1,0),
   2.234 +              is_wfrec_fm(iterates_MH_fm(formula_functor_fm(1,0),7,2,1,0), 
   2.235 +                           0, n#+3, Z#+3)))))))"
   2.236 +
   2.237 +lemma formula_N_fm_type [TC]:
   2.238 + "[| x \<in> nat; y \<in> nat |] ==> formula_N_fm(x,y) \<in> formula"
   2.239 +by (simp add: formula_N_fm_def)
   2.240 +
   2.241 +lemma sats_formula_N_fm [simp]:
   2.242 +   "[| x < length(env); y < length(env); env \<in> list(A)|]
   2.243 +    ==> sats(A, formula_N_fm(x,y), env) <->
   2.244 +        is_formula_N(**A, nth(x,env), nth(y,env))"
   2.245 +apply (frule_tac x=y in lt_length_in_nat, assumption)  
   2.246 +apply (frule lt_length_in_nat, assumption)  
   2.247 +apply (simp add: formula_N_fm_def is_formula_N_def sats_is_wfrec_fm sats_iterates_MH_fm) 
   2.248 +done
   2.249 +
   2.250 +lemma formula_N_iff_sats:
   2.251 +      "[| nth(i,env) = x; nth(j,env) = y; 
   2.252 +          i < length(env); j < length(env); env \<in> list(A)|]
   2.253 +       ==> is_formula_N(**A, x, y) <-> sats(A, formula_N_fm(i,j), env)"
   2.254 +by (simp add: sats_formula_N_fm)
   2.255 +
   2.256 +theorem formula_N_reflection:
   2.257 +     "REFLECTS[\<lambda>x. is_formula_N(L, f(x), g(x)),  
   2.258 +               \<lambda>i x. is_formula_N(**Lset(i), f(x), g(x))]"
   2.259 +apply (simp only: is_formula_N_def setclass_simps)
   2.260 +apply (intro FOL_reflections function_reflections is_wfrec_reflection 
   2.261 +             iterates_MH_reflection formula_functor_reflection) 
   2.262 +done
   2.263 +
   2.264 +
   2.265 +
   2.266 +subsubsection{*The Predicate ``Is A Formula''*}
   2.267 +
   2.268 +(*  mem_formula(M,p) == 
   2.269 +      \<exists>n[M]. \<exists>formn[M]. 
   2.270 +       finite_ordinal(M,n) & is_formula_N(M,n,formn) & p \<in> formn *)
   2.271 +constdefs mem_formula_fm :: "i=>i"
   2.272 +    "mem_formula_fm(x) ==
   2.273 +       Exists(Exists(
   2.274 +         And(finite_ordinal_fm(1),
   2.275 +           And(formula_N_fm(1,0), Member(x#+2,0)))))"
   2.276 +
   2.277 +lemma mem_formula_type [TC]:
   2.278 +     "x \<in> nat ==> mem_formula_fm(x) \<in> formula"
   2.279 +by (simp add: mem_formula_fm_def)
   2.280 +
   2.281 +lemma sats_mem_formula_fm [simp]:
   2.282 +   "[| x \<in> nat; env \<in> list(A)|]
   2.283 +    ==> sats(A, mem_formula_fm(x), env) <-> mem_formula(**A, nth(x,env))"
   2.284 +by (simp add: mem_formula_fm_def mem_formula_def)
   2.285 +
   2.286 +lemma mem_formula_iff_sats:
   2.287 +      "[| nth(i,env) = x; nth(j,env) = y;
   2.288 +          i \<in> nat; env \<in> list(A)|]
   2.289 +       ==> mem_formula(**A, x) <-> sats(A, mem_formula_fm(i), env)"
   2.290 +by simp
   2.291 +
   2.292 +theorem mem_formula_reflection:
   2.293 +     "REFLECTS[\<lambda>x. mem_formula(L,f(x)),
   2.294 +               \<lambda>i x. mem_formula(**Lset(i),f(x))]"
   2.295 +apply (simp only: mem_formula_def setclass_simps)
   2.296 +apply (intro FOL_reflections finite_ordinal_reflection formula_N_reflection)
   2.297 +done
   2.298 +
   2.299 +
   2.300 +
   2.301 +subsubsection{*The Formula @{term is_depth}, Internalized*}
   2.302 +
   2.303 +(*    "is_depth(M,p,n) == 
   2.304 +       \<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M]. 
   2.305 +         2          1                0
   2.306 +        is_formula_N(M,n,formula_n) & p \<notin> formula_n &
   2.307 +        successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \<in> formula_sn" *)
   2.308 +constdefs depth_fm :: "[i,i]=>i"
   2.309 +  "depth_fm(p,n) == 
   2.310 +     Exists(Exists(Exists(
   2.311 +       And(formula_N_fm(n#+3,1),
   2.312 +         And(Neg(Member(p#+3,1)),
   2.313 +          And(succ_fm(n#+3,2),
   2.314 +           And(formula_N_fm(2,0), Member(p#+3,0))))))))"
   2.315 +
   2.316 +lemma depth_fm_type [TC]:
   2.317 + "[| x \<in> nat; y \<in> nat |] ==> depth_fm(x,y) \<in> formula"
   2.318 +by (simp add: depth_fm_def)
   2.319 +
   2.320 +lemma sats_depth_fm [simp]:
   2.321 +   "[| x \<in> nat; y < length(env); env \<in> list(A)|]
   2.322 +    ==> sats(A, depth_fm(x,y), env) <->
   2.323 +        is_depth(**A, nth(x,env), nth(y,env))"
   2.324 +apply (frule_tac x=y in lt_length_in_nat, assumption)  
   2.325 +apply (simp add: depth_fm_def is_depth_def) 
   2.326 +done
   2.327 +
   2.328 +lemma depth_iff_sats:
   2.329 +      "[| nth(i,env) = x; nth(j,env) = y; 
   2.330 +          i \<in> nat; j < length(env); env \<in> list(A)|]
   2.331 +       ==> is_depth(**A, x, y) <-> sats(A, depth_fm(i,j), env)"
   2.332 +by (simp add: sats_depth_fm)
   2.333 +
   2.334 +theorem depth_reflection:
   2.335 +     "REFLECTS[\<lambda>x. is_depth(L, f(x), g(x)),  
   2.336 +               \<lambda>i x. is_depth(**Lset(i), f(x), g(x))]"
   2.337 +apply (simp only: is_depth_def setclass_simps)
   2.338 +apply (intro FOL_reflections function_reflections formula_N_reflection) 
   2.339 +done
   2.340 +
   2.341 +
   2.342 +
   2.343 +subsubsection{*The Operator @{term is_formula_case}*}
   2.344 +
   2.345 +text{*The arguments of @{term is_a} are always 2, 1, 0, and the formula
   2.346 +      will be enclosed by three quantifiers.*}
   2.347 +
   2.348 +(* is_formula_case :: 
   2.349 +    "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
   2.350 +  "is_formula_case(M, is_a, is_b, is_c, is_d, v, z) == 
   2.351 +      (\<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> is_Member(M,x,y,v) --> is_a(x,y,z)) &
   2.352 +      (\<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> is_Equal(M,x,y,v) --> is_b(x,y,z)) &
   2.353 +      (\<forall>x[M]. \<forall>y[M]. x\<in>formula --> y\<in>formula --> 
   2.354 +                     is_Nand(M,x,y,v) --> is_c(x,y,z)) &
   2.355 +      (\<forall>x[M]. x\<in>formula --> is_Forall(M,x,v) --> is_d(x,z))" *)
   2.356 +
   2.357 +constdefs formula_case_fm :: "[i, i, i, i, i, i]=>i"
   2.358 + "formula_case_fm(is_a, is_b, is_c, is_d, v, z) == 
   2.359 +        And(Forall(Forall(Implies(finite_ordinal_fm(1), 
   2.360 +                           Implies(finite_ordinal_fm(0), 
   2.361 +                            Implies(Member_fm(1,0,v#+2), 
   2.362 +                             Forall(Implies(Equal(0,z#+3), is_a))))))),
   2.363 +        And(Forall(Forall(Implies(finite_ordinal_fm(1), 
   2.364 +                           Implies(finite_ordinal_fm(0), 
   2.365 +                            Implies(Equal_fm(1,0,v#+2), 
   2.366 +                             Forall(Implies(Equal(0,z#+3), is_b))))))),
   2.367 +        And(Forall(Forall(Implies(mem_formula_fm(1), 
   2.368 +                           Implies(mem_formula_fm(0), 
   2.369 +                            Implies(Nand_fm(1,0,v#+2), 
   2.370 +                             Forall(Implies(Equal(0,z#+3), is_c))))))),
   2.371 +        Forall(Implies(mem_formula_fm(0), 
   2.372 +                       Implies(Forall_fm(0,succ(v)), 
   2.373 +                             Forall(Implies(Equal(0,z#+2), is_d))))))))"
   2.374 +
   2.375 +
   2.376 +lemma is_formula_case_type [TC]:
   2.377 +     "[| is_a \<in> formula;  is_b \<in> formula;  is_c \<in> formula;  is_d \<in> formula;  
   2.378 +         x \<in> nat; y \<in> nat |] 
   2.379 +      ==> formula_case_fm(is_a, is_b, is_c, is_d, x, y) \<in> formula"
   2.380 +by (simp add: formula_case_fm_def)
   2.381 +
   2.382 +lemma sats_formula_case_fm:
   2.383 +  assumes is_a_iff_sats: 
   2.384 +      "!!a0 a1 a2. 
   2.385 +        [|a0\<in>A; a1\<in>A; a2\<in>A|]  
   2.386 +        ==> ISA(a2, a1, a0) <-> sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))"
   2.387 +  and is_b_iff_sats: 
   2.388 +      "!!a0 a1 a2. 
   2.389 +        [|a0\<in>A; a1\<in>A; a2\<in>A|]  
   2.390 +        ==> ISB(a2, a1, a0) <-> sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))"
   2.391 +  and is_c_iff_sats: 
   2.392 +      "!!a0 a1 a2. 
   2.393 +        [|a0\<in>A; a1\<in>A; a2\<in>A|]  
   2.394 +        ==> ISC(a2, a1, a0) <-> sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))"
   2.395 +  and is_d_iff_sats: 
   2.396 +      "!!a0 a1. 
   2.397 +        [|a0\<in>A; a1\<in>A|]  
   2.398 +        ==> ISD(a1, a0) <-> sats(A, is_d, Cons(a0,Cons(a1,env)))"
   2.399 +  shows 
   2.400 +      "[|x \<in> nat; y < length(env); env \<in> list(A)|]
   2.401 +       ==> sats(A, formula_case_fm(is_a,is_b,is_c,is_d,x,y), env) <->
   2.402 +           is_formula_case(**A, ISA, ISB, ISC, ISD, nth(x,env), nth(y,env))"
   2.403 +apply (frule_tac x=y in lt_length_in_nat, assumption)  
   2.404 +apply (simp add: formula_case_fm_def is_formula_case_def 
   2.405 +                 is_a_iff_sats [THEN iff_sym] is_b_iff_sats [THEN iff_sym]
   2.406 +                 is_c_iff_sats [THEN iff_sym] is_d_iff_sats [THEN iff_sym])
   2.407 +done
   2.408 +
   2.409 +lemma formula_case_iff_sats:
   2.410 +  assumes is_a_iff_sats: 
   2.411 +      "!!a0 a1 a2. 
   2.412 +        [|a0\<in>A; a1\<in>A; a2\<in>A|]  
   2.413 +        ==> ISA(a2, a1, a0) <-> sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))"
   2.414 +  and is_b_iff_sats: 
   2.415 +      "!!a0 a1 a2. 
   2.416 +        [|a0\<in>A; a1\<in>A; a2\<in>A|]  
   2.417 +        ==> ISB(a2, a1, a0) <-> sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))"
   2.418 +  and is_c_iff_sats: 
   2.419 +      "!!a0 a1 a2. 
   2.420 +        [|a0\<in>A; a1\<in>A; a2\<in>A|]  
   2.421 +        ==> ISC(a2, a1, a0) <-> sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))"
   2.422 +  and is_d_iff_sats: 
   2.423 +      "!!a0 a1. 
   2.424 +        [|a0\<in>A; a1\<in>A|]  
   2.425 +        ==> ISD(a1, a0) <-> sats(A, is_d, Cons(a0,Cons(a1,env)))"
   2.426 +  shows 
   2.427 +      "[|nth(i,env) = x; nth(j,env) = y; 
   2.428 +      i \<in> nat; j < length(env); env \<in> list(A)|]
   2.429 +       ==> is_formula_case(**A, ISA, ISB, ISC, ISD, x, y) <->
   2.430 +           sats(A, formula_case_fm(is_a,is_b,is_c,is_d,i,j), env)"
   2.431 +by (simp add: sats_formula_case_fm [OF is_a_iff_sats is_b_iff_sats 
   2.432 +                                       is_c_iff_sats is_d_iff_sats])
   2.433 +
   2.434 +
   2.435 +text{*The second argument of @{term is_a} gives it direct access to @{term x},
   2.436 +  which is essential for handling free variable references.  Treatment is
   2.437 +  based on that of @{text is_nat_case_reflection}.*}
   2.438 +theorem is_formula_case_reflection:
   2.439 +  assumes is_a_reflection:
   2.440 +    "!!h f g g'. REFLECTS[\<lambda>x. is_a(L, h(x), f(x), g(x), g'(x)),
   2.441 +                     \<lambda>i x. is_a(**Lset(i), h(x), f(x), g(x), g'(x))]"
   2.442 +  and is_b_reflection:
   2.443 +    "!!h f g g'. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x), g'(x)),
   2.444 +                     \<lambda>i x. is_b(**Lset(i), h(x), f(x), g(x), g'(x))]"
   2.445 +  and is_c_reflection:
   2.446 +    "!!h f g g'. REFLECTS[\<lambda>x. is_c(L, h(x), f(x), g(x), g'(x)),
   2.447 +                     \<lambda>i x. is_c(**Lset(i), h(x), f(x), g(x), g'(x))]"
   2.448 +  and is_d_reflection:
   2.449 +    "!!h f g g'. REFLECTS[\<lambda>x. is_d(L, h(x), f(x), g(x)),
   2.450 +                     \<lambda>i x. is_d(**Lset(i), h(x), f(x), g(x))]"
   2.451 +  shows "REFLECTS[\<lambda>x. is_formula_case(L, is_a(L,x), is_b(L,x), is_c(L,x), is_d(L,x), g(x), h(x)),
   2.452 +               \<lambda>i x. is_formula_case(**Lset(i), is_a(**Lset(i), x), is_b(**Lset(i), x), is_c(**Lset(i), x), is_d(**Lset(i), x), g(x), h(x))]"
   2.453 +apply (simp (no_asm_use) only: is_formula_case_def setclass_simps)
   2.454 +apply (intro FOL_reflections function_reflections finite_ordinal_reflection
   2.455 +         mem_formula_reflection
   2.456 +         Member_reflection Equal_reflection Nand_reflection Forall_reflection
   2.457 +         is_a_reflection is_b_reflection is_c_reflection is_d_reflection)
   2.458 +done
   2.459 +
   2.460 +
   2.461 +
   2.462 +subsection {*Absoluteness for @{term formula_rec}*}
   2.463 +
   2.464 +constdefs
   2.465 +
   2.466 +  formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i"
   2.467 +    --{* the instance of @{term formula_case} in @{term formula_rec}*}
   2.468 +   "formula_rec_case(a,b,c,d,h) ==
   2.469 +        formula_case (a, b,
   2.470 +                \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u, 
   2.471 +                              h ` succ(depth(v)) ` v),
   2.472 +                \<lambda>u. d(u, h ` succ(depth(u)) ` u))"
   2.473 +
   2.474 +  is_formula_rec :: "[i=>o, [i,i,i]=>o, 
   2.475 +                      [i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, 
   2.476 +                      i, i] => o"
   2.477 +    --{* predicate to relative the functional @{term formula_rec}*}
   2.478 +   "is_formula_rec(M,MH,a,b,c,d,p,z)  ==
   2.479 +    \<exists>i[M]. \<exists>f[M]. i = succ(depth(p)) & fun_apply(M,f,p,z) &
   2.480 +                  is_transrec(M,MH,i,f)"
   2.481 +
   2.482 +text{*Unfold @{term formula_rec} to @{term formula_rec_case}*}
   2.483 +lemma (in M_triv_axioms) formula_rec_eq2:
   2.484 +  "p \<in> formula ==>
   2.485 +   formula_rec(a,b,c,d,p) = 
   2.486 +   transrec (succ(depth(p)),
   2.487 +             \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h))) ` p"
   2.488 +by (simp add: formula_rec_eq  formula_rec_case_def)
   2.489 +
   2.490 +
   2.491 +text{*Sufficient conditions to relative the instance of @{term formula_case}
   2.492 +      in @{term formula_rec}*}
   2.493 +lemma (in M_datatypes) Relativize1_formula_rec_case:
   2.494 +     "[|Relativize2(M, nat, nat, is_a, a);
   2.495 +        Relativize2(M, nat, nat, is_b, b);
   2.496 +        Relativize2 (M, formula, formula, 
   2.497 +           is_c, \<lambda>u v. c(u, v, h`succ(depth(u))`u, h`succ(depth(v))`v));
   2.498 +        Relativize1(M, formula, 
   2.499 +           is_d, \<lambda>u. d(u, h ` succ(depth(u)) ` u));
   2.500 + 	M(h) |] 
   2.501 +      ==> Relativize1(M, formula,
   2.502 +                         is_formula_case (M, is_a, is_b, is_c, is_d),
   2.503 +                         formula_rec_case(a, b, c, d, h))"
   2.504 +apply (simp (no_asm) add: formula_rec_case_def Relativize1_def) 
   2.505 +apply (simp add: formula_case_abs) 
   2.506 +done
   2.507 +
   2.508 +
   2.509 +text{*This locale packages the premises of the following theorems,
   2.510 +      which is the normal purpose of locales.  It doesn't accumulate
   2.511 +      constraints on the class @{term M}, as in most of this deveopment.*}
   2.512 +locale M_formula_rec = M_eclose +
   2.513 +  fixes a and is_a and b and is_b and c and is_c and d and is_d and MH
   2.514 +  defines
   2.515 +      "MH(u::i,f,z) ==
   2.516 +	is_lambda
   2.517 +	 (M, formula, is_formula_case (M, is_a, is_b, is_c(f), is_d(f)), z)"
   2.518 +
   2.519 +  assumes a_closed: "[|x\<in>nat; y\<in>nat|] ==> M(a(x,y))"
   2.520 +      and a_rel:    "Relativize2(M, nat, nat, is_a, a)"
   2.521 +      and b_closed: "[|x\<in>nat; y\<in>nat|] ==> M(b(x,y))"
   2.522 +      and b_rel:    "Relativize2(M, nat, nat, is_b, b)"
   2.523 +      and c_closed: "[|x \<in> formula; y \<in> formula; M(gx); M(gy)|]
   2.524 +                     ==> M(c(x, y, gx, gy))"
   2.525 +      and c_rel:
   2.526 +         "M(f) ==> 
   2.527 +          Relativize2 (M, formula, formula, is_c(f),
   2.528 +             \<lambda>u v. c(u, v, f ` succ(depth(u)) ` u, f ` succ(depth(v)) ` v))"
   2.529 +      and d_closed: "[|x \<in> formula; M(gx)|] ==> M(d(x, gx))"
   2.530 +      and d_rel:
   2.531 +         "M(f) ==> 
   2.532 +          Relativize1(M, formula, is_d(f), \<lambda>u. d(u, f ` succ(depth(u)) ` u))"
   2.533 +      and fr_replace: "n \<in> nat ==> transrec_replacement(M,MH,n)"
   2.534 +      and fr_lam_replace:
   2.535 +           "M(g) ==>
   2.536 +            strong_replacement
   2.537 +	      (M, \<lambda>x y. x \<in> formula &
   2.538 +		  y = \<langle>x, formula_rec_case(a,b,c,d,g,x)\<rangle>)";
   2.539 +
   2.540 +lemma (in M_formula_rec) formula_rec_case_closed:
   2.541 +    "[|M(g); p \<in> formula|] ==> M(formula_rec_case(a, b, c, d, g, p))"
   2.542 +by (simp add: formula_rec_case_def a_closed b_closed c_closed d_closed) 
   2.543 +
   2.544 +lemma (in M_formula_rec) formula_rec_lam_closed:
   2.545 +    "M(g) ==> M(Lambda (formula, formula_rec_case(a,b,c,d,g)))"
   2.546 +by (simp add: lam_closed2 fr_lam_replace formula_rec_case_closed)
   2.547 +
   2.548 +lemma (in M_formula_rec) MH_rel2:
   2.549 +     "relativize2 (M, MH,
   2.550 +             \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h)))"
   2.551 +apply (simp add: relativize2_def MH_def, clarify) 
   2.552 +apply (rule lambda_abs2) 
   2.553 +apply (rule fr_lam_replace, assumption)
   2.554 +apply (rule Relativize1_formula_rec_case)  
   2.555 +apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed) 
   2.556 +done
   2.557 +
   2.558 +lemma (in M_formula_rec) fr_transrec_closed:
   2.559 +    "n \<in> nat
   2.560 +     ==> M(transrec
   2.561 +          (n, \<lambda>x h. Lambda(formula, formula_rec_case(a, b, c, d, h))))"
   2.562 +by (simp add: transrec_closed [OF fr_replace MH_rel2]  
   2.563 +              nat_into_M formula_rec_lam_closed) 
   2.564 +
   2.565 +text{*The main two results: @{term formula_rec} is absolute for @{term M}.*}
   2.566 +theorem (in M_formula_rec) formula_rec_closed:
   2.567 +    "p \<in> formula ==> M(formula_rec(a,b,c,d,p))"
   2.568 +by (simp add: formula_rec_eq2 fr_transrec_closed 
   2.569 +              transM [OF _ formula_closed])
   2.570 +
   2.571 +theorem (in M_formula_rec) formula_rec_abs:
   2.572 +  "[| p \<in> formula; M(z)|] 
   2.573 +   ==> is_formula_rec(M,MH,a,b,c,d,p,z) <-> z = formula_rec(a,b,c,d,p)" 
   2.574 +by (simp add: is_formula_rec_def formula_rec_eq2 transM [OF _ formula_closed]
   2.575 +              transrec_abs [OF fr_replace MH_rel2] 
   2.576 +              fr_transrec_closed formula_rec_lam_closed eq_commute)
   2.577 +
   2.578 +
   2.579 +subsection {*Absoluteness for the Function @{term satisfies}*}
   2.580 +
   2.581 +constdefs
   2.582 +  is_depth_apply :: "[i=>o,i,i,i] => o"
   2.583 +   --{*Merely a useful abbreviation for the sequel.*}
   2.584 +   "is_depth_apply(M,h,p,z) ==
   2.585 +    \<exists>dp[M]. \<exists>sdp[M]. \<exists>hsdp[M]. 
   2.586 +	dp \<in> nat & is_depth(M,p,dp) & successor(M,dp,sdp) &
   2.587 +	fun_apply(M,h,sdp,hsdp) & fun_apply(M,hsdp,p,z)"
   2.588 +
   2.589 +lemma (in M_datatypes) is_depth_apply_abs [simp]:
   2.590 +     "[|M(h); p \<in> formula; M(z)|] 
   2.591 +      ==> is_depth_apply(M,h,p,z) <-> z = h ` succ(depth(p)) ` p"
   2.592 +by (simp add: is_depth_apply_def formula_into_M depth_type eq_commute)
   2.593 +
   2.594 +lemma depth_apply_reflection:
   2.595 +     "REFLECTS[\<lambda>x. is_depth_apply(L,f(x),g(x),h(x)),
   2.596 +               \<lambda>i x. is_depth_apply(**Lset(i),f(x),g(x),h(x))]"
   2.597 +apply (simp only: is_depth_apply_def setclass_simps)
   2.598 +apply (intro FOL_reflections function_reflections depth_reflection)
   2.599 +done
   2.600 +
   2.601 +
   2.602 +text{*There is at present some redundancy between the relativizations in
   2.603 + e.g. @{text satisfies_is_a} and those in e.g. @{text Member_replacement}.*}
   2.604 +
   2.605 +text{*These constants let us instantiate the parameters @{term a}, @{term b},
   2.606 +      @{term c}, @{term d}, etc., of the locale @{text M_formula_rec}.*}
   2.607 +constdefs
   2.608 +  satisfies_a :: "[i,i,i]=>i"
   2.609 +   "satisfies_a(A) == 
   2.610 +    \<lambda>x y. \<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env))"
   2.611 +
   2.612 +  satisfies_is_a :: "[i=>o,i,i,i,i]=>o"
   2.613 +   "satisfies_is_a(M,A) == 
   2.614 +    \<lambda>x y. is_lambda(M, list(A), 
   2.615 +        \<lambda>env z. is_bool_of_o(M, \<exists>nx[M]. \<exists>ny[M]. 
   2.616 +                  is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & nx \<in> ny, z))"
   2.617 +
   2.618 +  satisfies_b :: "[i,i,i]=>i"
   2.619 +   "satisfies_b(A) ==
   2.620 +    \<lambda>x y. \<lambda>env \<in> list(A). bool_of_o (nth(x,env) = nth(y,env))"
   2.621 +
   2.622 +  satisfies_is_b :: "[i=>o,i,i,i,i]=>o"
   2.623 +   --{*We simplify the formula to have just @{term nx} rather than 
   2.624 +       introducing @{term ny} with  @{term "nx=ny"} *}
   2.625 +   "satisfies_is_b(M,A) == 
   2.626 +    \<lambda>x y. is_lambda(M, list(A), 
   2.627 +         \<lambda>env z. 
   2.628 +         is_bool_of_o(M, \<exists>nx[M]. is_nth(M,x,env,nx) & is_nth(M,y,env,nx), z))"
   2.629 + 
   2.630 +  satisfies_c :: "[i,i,i,i,i]=>i"
   2.631 +   "satisfies_c(A,p,q,rp,rq) == \<lambda>env \<in> list(A). not(rp ` env and rq ` env)"
   2.632 +
   2.633 +  satisfies_is_c :: "[i=>o,i,i,i,i,i]=>o"
   2.634 +   "satisfies_is_c(M,A,h) == 
   2.635 +    \<lambda>p q. is_lambda(M, list(A), 
   2.636 +        \<lambda>env z. \<exists>hp[M]. \<exists>hq[M]. 
   2.637 +		 (\<exists>rp[M]. is_depth_apply(M,h,p,rp) & fun_apply(M,rp,env,hp)) & 
   2.638 +		 (\<exists>rq[M]. is_depth_apply(M,h,q,rq) & fun_apply(M,rq,env,hq)) & 
   2.639 +                 (\<exists>pq[M]. is_and(M,hp,hq,pq) & is_not(M,pq,z)))"
   2.640 +
   2.641 +  satisfies_d :: "[i,i,i]=>i"
   2.642 +   "satisfies_d(A) 
   2.643 +    == \<lambda>p rp. \<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. rp ` (Cons(x,env)) = 1)"
   2.644 +
   2.645 +  satisfies_is_d :: "[i=>o,i,i,i,i]=>o"
   2.646 +   "satisfies_is_d(M,A,h) == 
   2.647 +    \<lambda>p. is_lambda(M, list(A), 
   2.648 +        \<lambda>env z. \<exists>rp[M]. is_depth_apply(M,h,p,rp) & 
   2.649 +           is_bool_of_o(M, 
   2.650 +                \<forall>x[M]. \<forall>xenv[M]. \<forall>hp[M]. 
   2.651 +                       x\<in>A --> is_Cons(M,x,env,xenv) --> 
   2.652 +                       fun_apply(M,rp,xenv,hp) --> number1(M,hp),
   2.653 +                  z))"
   2.654 +
   2.655 +  satisfies_MH :: "[i=>o,i,i,i,i]=>o"
   2.656 +   "satisfies_MH == 
   2.657 +    \<lambda>M A u f. is_lambda
   2.658 +	 (M, formula, 
   2.659 +          is_formula_case (M, satisfies_is_a(M,A), 
   2.660 +                           satisfies_is_b(M,A), 
   2.661 +                           satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)))"
   2.662 +
   2.663 +
   2.664 +text{*Further constraints on the class @{term M} in order to prove
   2.665 +      absoluteness for the constants defined above.  The ultimate goal
   2.666 +      is the absoluteness of the function @{term satisfies}. *}
   2.667 +locale M_satisfies = M_datatypes +
   2.668 + assumes 
   2.669 +   Member_replacement:
   2.670 +    "[|M(A); x \<in> nat; y \<in> nat|]
   2.671 +     ==> strong_replacement
   2.672 +	 (M, \<lambda>env z. \<exists>bo[M]. \<exists>nx[M]. \<exists>ny[M]. 
   2.673 +              env \<in> list(A) & is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & 
   2.674 +              is_bool_of_o(M, nx \<in> ny, bo) &
   2.675 +              pair(M, env, bo, z))"
   2.676 + and
   2.677 +   Equal_replacement:
   2.678 +    "[|M(A); x \<in> nat; y \<in> nat|]
   2.679 +     ==> strong_replacement
   2.680 +	 (M, \<lambda>env z. \<exists>bo[M]. \<exists>nx[M]. \<exists>ny[M]. 
   2.681 +              env \<in> list(A) & is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & 
   2.682 +              is_bool_of_o(M, nx = ny, bo) &
   2.683 +              pair(M, env, bo, z))"
   2.684 + and
   2.685 +   Nand_replacement:
   2.686 +    "[|M(A); M(rp); M(rq)|]
   2.687 +     ==> strong_replacement
   2.688 +	 (M, \<lambda>env z. \<exists>rpe[M]. \<exists>rqe[M]. \<exists>andpq[M]. \<exists>notpq[M]. 
   2.689 +               fun_apply(M,rp,env,rpe) & fun_apply(M,rq,env,rqe) & 
   2.690 +               is_and(M,rpe,rqe,andpq) & is_not(M,andpq,notpq) & 
   2.691 +               env \<in> list(A) & pair(M, env, notpq, z))"
   2.692 + and
   2.693 +  Forall_replacement:
   2.694 +   "[|M(A); M(rp)|]
   2.695 +    ==> strong_replacement
   2.696 +	(M, \<lambda>env z. \<exists>bo[M]. 
   2.697 +	      env \<in> list(A) & 
   2.698 +	      is_bool_of_o (M, 
   2.699 +			    \<forall>a[M]. \<forall>co[M]. \<forall>rpco[M]. 
   2.700 +			       a\<in>A --> is_Cons(M,a,env,co) -->
   2.701 +			       fun_apply(M,rp,co,rpco) --> number1(M, rpco), 
   2.702 +                            bo) &
   2.703 +	      pair(M,env,bo,z))"
   2.704 + and
   2.705 +  formula_rec_replacement: 
   2.706 +      --{*For the @{term transrec}*}
   2.707 +   "[|n \<in> nat; M(A)|] ==> transrec_replacement(M, satisfies_MH(M,A), n)"
   2.708 +(*NEEDS RELATIVIZATION?*)
   2.709 + and
   2.710 +  formula_rec_lambda_replacement:  
   2.711 +      --{*For the @{text "\<lambda>-abstraction"} in the @{term transrec} body*}
   2.712 +   "M(g) ==>
   2.713 +    strong_replacement (M, \<lambda>x y. x \<in> formula &
   2.714 +            y = \<langle>x, 
   2.715 +                 formula_rec_case(satisfies_a(A),
   2.716 +                                  satisfies_b(A),
   2.717 +                                  satisfies_c(A),
   2.718 +                                  satisfies_d(A), g, x)\<rangle>)"
   2.719 +
   2.720 +
   2.721 +lemma (in M_satisfies) Member_replacement':
   2.722 +    "[|M(A); x \<in> nat; y \<in> nat|]
   2.723 +     ==> strong_replacement
   2.724 +	 (M, \<lambda>env z. env \<in> list(A) &
   2.725 +		     z = \<langle>env, bool_of_o(nth(x, env) \<in> nth(y, env))\<rangle>)"
   2.726 +by (insert Member_replacement, simp) 
   2.727 +
   2.728 +lemma (in M_satisfies) Equal_replacement':
   2.729 +    "[|M(A); x \<in> nat; y \<in> nat|]
   2.730 +     ==> strong_replacement
   2.731 +	 (M, \<lambda>env z. env \<in> list(A) &
   2.732 +		     z = \<langle>env, bool_of_o(nth(x, env) = nth(y, env))\<rangle>)"
   2.733 +by (insert Equal_replacement, simp) 
   2.734 +
   2.735 +lemma (in M_satisfies) Nand_replacement':
   2.736 +    "[|M(A); M(rp); M(rq)|]
   2.737 +     ==> strong_replacement
   2.738 +	 (M, \<lambda>env z. env \<in> list(A) & z = \<langle>env, not(rp`env and rq`env)\<rangle>)"
   2.739 +by (insert Nand_replacement, simp) 
   2.740 +
   2.741 +lemma (in M_satisfies) Forall_replacement':
   2.742 +   "[|M(A); M(rp)|]
   2.743 +    ==> strong_replacement
   2.744 +	(M, \<lambda>env z.
   2.745 +	       env \<in> list(A) &
   2.746 +	       z = \<langle>env, bool_of_o (\<forall>a\<in>A. rp ` Cons(a,env) = 1)\<rangle>)"
   2.747 +by (insert Forall_replacement, simp) 
   2.748 +
   2.749 +lemma (in M_satisfies) a_closed:
   2.750 +     "[|M(A); x\<in>nat; y\<in>nat|] ==> M(satisfies_a(A,x,y))"
   2.751 +apply (simp add: satisfies_a_def) 
   2.752 +apply (blast intro: lam_closed2 Member_replacement') 
   2.753 +done
   2.754 +
   2.755 +lemma (in M_satisfies) a_rel:
   2.756 +     "M(A) ==> Relativize2(M, nat, nat, satisfies_is_a(M,A), satisfies_a(A))"
   2.757 +apply (simp add: Relativize2_def satisfies_is_a_def satisfies_a_def)
   2.758 +apply (simp add: lambda_abs2 [OF Member_replacement'] Relativize1_def)
   2.759 +done
   2.760 +
   2.761 +lemma (in M_satisfies) b_closed:
   2.762 +     "[|M(A); x\<in>nat; y\<in>nat|] ==> M(satisfies_b(A,x,y))"
   2.763 +apply (simp add: satisfies_b_def) 
   2.764 +apply (blast intro: lam_closed2 Equal_replacement') 
   2.765 +done
   2.766 +
   2.767 +lemma (in M_satisfies) b_rel:
   2.768 +     "M(A) ==> Relativize2(M, nat, nat, satisfies_is_b(M,A), satisfies_b(A))"
   2.769 +apply (simp add: Relativize2_def satisfies_is_b_def satisfies_b_def)
   2.770 +apply (simp add: lambda_abs2 [OF Equal_replacement'] Relativize1_def)
   2.771 +done
   2.772 +
   2.773 +lemma (in M_satisfies) c_closed:
   2.774 +     "[|M(A); x \<in> formula; y \<in> formula; M(rx); M(ry)|] 
   2.775 +      ==> M(satisfies_c(A,x,y,rx,ry))"
   2.776 +apply (simp add: satisfies_c_def) 
   2.777 +apply (rule lam_closed2) 
   2.778 +apply (rule Nand_replacement') 
   2.779 +apply (simp_all add: formula_into_M list_into_M [of _ A])
   2.780 +done
   2.781 +
   2.782 +lemma (in M_satisfies) c_rel:
   2.783 + "[|M(A); M(f)|] ==> 
   2.784 +  Relativize2 (M, formula, formula, 
   2.785 +               satisfies_is_c(M,A,f),
   2.786 +	       \<lambda>u v. satisfies_c(A, u, v, f ` succ(depth(u)) ` u, 
   2.787 +					  f ` succ(depth(v)) ` v))"
   2.788 +apply (simp add: Relativize2_def satisfies_is_c_def satisfies_c_def)
   2.789 +apply (simp add: lambda_abs2 [OF Nand_replacement' triv_Relativize1] 
   2.790 +                 formula_into_M)
   2.791 +done
   2.792 +
   2.793 +lemma (in M_satisfies) d_closed:
   2.794 +     "[|M(A); x \<in> formula; M(rx)|] ==> M(satisfies_d(A,x,rx))"
   2.795 +apply (simp add: satisfies_d_def) 
   2.796 +apply (rule lam_closed2) 
   2.797 +apply (rule Forall_replacement') 
   2.798 +apply (simp_all add: formula_into_M list_into_M [of _ A])
   2.799 +done
   2.800 +
   2.801 +lemma (in M_satisfies) d_rel:
   2.802 + "[|M(A); M(f)|] ==> 
   2.803 +  Relativize1(M, formula, satisfies_is_d(M,A,f), 
   2.804 +     \<lambda>u. satisfies_d(A, u, f ` succ(depth(u)) ` u))"
   2.805 +apply (simp del: rall_abs 
   2.806 +            add: Relativize1_def satisfies_is_d_def satisfies_d_def)
   2.807 +apply (simp add: lambda_abs2 [OF Forall_replacement' triv_Relativize1] 
   2.808 +                 formula_into_M)
   2.809 +done
   2.810 +
   2.811 +
   2.812 +lemma (in M_satisfies) fr_replace:
   2.813 +      "[|n \<in> nat; M(A)|] ==> transrec_replacement(M,satisfies_MH(M,A),n)" 
   2.814 +by (blast intro: formula_rec_replacement) 
   2.815 +
   2.816 +lemma (in M_satisfies) fr_lam_replace:
   2.817 +   "M(g) ==>
   2.818 +    strong_replacement (M, \<lambda>x y. x \<in> formula &
   2.819 +            y = \<langle>x, 
   2.820 +                 formula_rec_case(satisfies_a(A),
   2.821 +                                  satisfies_b(A),
   2.822 +                                  satisfies_c(A),
   2.823 +                                  satisfies_d(A), g, x)\<rangle>)"
   2.824 +by (blast intro: formula_rec_lambda_replacement)
   2.825 +
   2.826 +
   2.827 +
   2.828 +subsection{*Instantiating the Locale @{text "M_satisfies"}*}
   2.829 +
   2.830 +
   2.831 +subsubsection{*The @{term "Member"} Case*}
   2.832 +
   2.833 +lemma Member_Reflects:
   2.834 + "REFLECTS[\<lambda>u. \<exists>v[L]. v \<in> B \<and> (\<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L].
   2.835 +          v \<in> lstA \<and> is_nth(L,x,v,nx) \<and> is_nth(L,y,v,ny) \<and>
   2.836 +          is_bool_of_o(L, nx \<in> ny, bo) \<and> pair(L,v,bo,u)),
   2.837 +   \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i).
   2.838 +             v \<in> lstA \<and> is_nth(**Lset(i), x, v, nx) \<and> 
   2.839 +             is_nth(**Lset(i), y, v, ny) \<and>
   2.840 +          is_bool_of_o(**Lset(i), nx \<in> ny, bo) \<and> pair(**Lset(i), v, bo, u))]"
   2.841 +by (intro FOL_reflections function_reflections nth_reflection 
   2.842 +          bool_of_o_reflection)
   2.843 +
   2.844 +
   2.845 +lemma Member_replacement:
   2.846 +    "[|L(A); x \<in> nat; y \<in> nat|]
   2.847 +     ==> strong_replacement
   2.848 +	 (L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. 
   2.849 +              env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
   2.850 +              is_bool_of_o(L, nx \<in> ny, bo) &
   2.851 +              pair(L, env, bo, z))"
   2.852 +apply (frule list_closed) 
   2.853 +apply (rule strong_replacementI) 
   2.854 +apply (rule rallI)
   2.855 +apply (rename_tac B)  
   2.856 +apply (rule separation_CollectI) 
   2.857 +apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast ) 
   2.858 +apply (rule ReflectsE [OF Member_Reflects], assumption)
   2.859 +apply (drule subset_Lset_ltD, assumption) 
   2.860 +apply (erule reflection_imp_L_separation)
   2.861 +  apply (simp_all add: lt_Ord2)
   2.862 +apply (simp add: is_nth_def is_wfrec_def is_bool_of_o_def)
   2.863 +apply (rule DPow_LsetI)
   2.864 +apply (rename_tac u) 
   2.865 +apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
   2.866 +apply (rule_tac env = "[v,u,list(A),B,x,y,z]" in mem_iff_sats) 
   2.867 +apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats
   2.868 +            is_recfun_iff_sats hd_iff_sats tl_iff_sats quasinat_iff_sats
   2.869 +     | simp)+
   2.870 +done
   2.871 +
   2.872 +
   2.873 +subsubsection{*The @{term "Equal"} Case*}
   2.874 +
   2.875 +lemma Equal_Reflects:
   2.876 + "REFLECTS[\<lambda>u. \<exists>v[L]. v \<in> B \<and> (\<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L].
   2.877 +          v \<in> lstA \<and> is_nth(L, x, v, nx) \<and> is_nth(L, y, v, ny) \<and>
   2.878 +          is_bool_of_o(L, nx = ny, bo) \<and> pair(L, v, bo, u)),
   2.879 +   \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i).
   2.880 +             v \<in> lstA \<and> is_nth(**Lset(i), x, v, nx) \<and> 
   2.881 +             is_nth(**Lset(i), y, v, ny) \<and>
   2.882 +          is_bool_of_o(**Lset(i), nx = ny, bo) \<and> pair(**Lset(i), v, bo, u))]"
   2.883 +by (intro FOL_reflections function_reflections nth_reflection 
   2.884 +          bool_of_o_reflection)
   2.885 +
   2.886 +
   2.887 +lemma Equal_replacement:
   2.888 +    "[|L(A); x \<in> nat; y \<in> nat|]
   2.889 +     ==> strong_replacement
   2.890 +	 (L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. 
   2.891 +              env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
   2.892 +              is_bool_of_o(L, nx = ny, bo) &
   2.893 +              pair(L, env, bo, z))"
   2.894 +apply (frule list_closed) 
   2.895 +apply (rule strong_replacementI) 
   2.896 +apply (rule rallI)
   2.897 +apply (rename_tac B)  
   2.898 +apply (rule separation_CollectI) 
   2.899 +apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast ) 
   2.900 +apply (rule ReflectsE [OF Equal_Reflects], assumption)
   2.901 +apply (drule subset_Lset_ltD, assumption) 
   2.902 +apply (erule reflection_imp_L_separation)
   2.903 +  apply (simp_all add: lt_Ord2)
   2.904 +apply (simp add: is_nth_def is_wfrec_def is_bool_of_o_def)
   2.905 +apply (rule DPow_LsetI)
   2.906 +apply (rename_tac u) 
   2.907 +apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
   2.908 +apply (rule_tac env = "[v,u,list(A),B,x,y,z]" in mem_iff_sats) 
   2.909 +apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats
   2.910 +            is_recfun_iff_sats hd_iff_sats tl_iff_sats quasinat_iff_sats
   2.911 +     | simp)+
   2.912 +done
   2.913 +
   2.914 +subsubsection{*The @{term "Nand"} Case*}
   2.915 +
   2.916 +lemma Nand_Reflects:
   2.917 +    "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and>
   2.918 +	       (\<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L].
   2.919 +		 fun_apply(L, rp, u, rpe) \<and> fun_apply(L, rq, u, rqe) \<and>
   2.920 +		 is_and(L, rpe, rqe, andpq) \<and> is_not(L, andpq, notpq) \<and>
   2.921 +		 u \<in> list(A) \<and> pair(L, u, notpq, x)),
   2.922 +    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and>
   2.923 +     (\<exists>rpe \<in> Lset(i). \<exists>rqe \<in> Lset(i). \<exists>andpq \<in> Lset(i). \<exists>notpq \<in> Lset(i).
   2.924 +       fun_apply(**Lset(i), rp, u, rpe) \<and> fun_apply(**Lset(i), rq, u, rqe) \<and>
   2.925 +       is_and(**Lset(i), rpe, rqe, andpq) \<and> is_not(**Lset(i), andpq, notpq) \<and>
   2.926 +       u \<in> list(A) \<and> pair(**Lset(i), u, notpq, x))]"
   2.927 +apply (unfold is_and_def is_not_def) 
   2.928 +apply (intro FOL_reflections function_reflections)
   2.929 +done
   2.930 +
   2.931 +lemma Nand_replacement:
   2.932 +    "[|L(A); L(rp); L(rq)|]
   2.933 +     ==> strong_replacement
   2.934 +	 (L, \<lambda>env z. \<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L]. 
   2.935 +               fun_apply(L,rp,env,rpe) & fun_apply(L,rq,env,rqe) & 
   2.936 +               is_and(L,rpe,rqe,andpq) & is_not(L,andpq,notpq) & 
   2.937 +               env \<in> list(A) & pair(L, env, notpq, z))"
   2.938 +apply (frule list_closed) 
   2.939 +apply (rule strong_replacementI) 
   2.940 +apply (rule rallI)
   2.941 +apply (rename_tac B)  
   2.942 +apply (rule separation_CollectI) 
   2.943 +apply (rule_tac A="{list(A),B,rp,rq,z}" in subset_LsetE, blast ) 
   2.944 +apply (rule ReflectsE [OF Nand_Reflects], assumption)
   2.945 +apply (drule subset_Lset_ltD, assumption) 
   2.946 +apply (erule reflection_imp_L_separation)
   2.947 +  apply (simp_all add: lt_Ord2)
   2.948 +apply (simp add: is_and_def is_not_def)
   2.949 +apply (rule DPow_LsetI)
   2.950 +apply (rename_tac v) 
   2.951 +apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
   2.952 +apply (rule_tac env = "[u,v,list(A),B,rp,rq,z]" in mem_iff_sats) 
   2.953 +apply (rule sep_rules | simp)+
   2.954 +done
   2.955 +
   2.956 +
   2.957 +subsubsection{*The @{term "Forall"} Case*}
   2.958 +
   2.959 +lemma Forall_Reflects:
   2.960 + "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>bo[L]. u \<in> list(A) \<and>
   2.961 +                 is_bool_of_o (L,
   2.962 +     \<forall>a[L]. \<forall>co[L]. \<forall>rpco[L]. a \<in> A \<longrightarrow>
   2.963 +                is_Cons(L,a,u,co) \<longrightarrow> fun_apply(L,rp,co,rpco) \<longrightarrow> 
   2.964 +                number1(L,rpco),
   2.965 +                           bo) \<and> pair(L,u,bo,x)),
   2.966 + \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>bo \<in> Lset(i). u \<in> list(A) \<and>
   2.967 +        is_bool_of_o (**Lset(i),
   2.968 + \<forall>a \<in> Lset(i). \<forall>co \<in> Lset(i). \<forall>rpco \<in> Lset(i). a \<in> A \<longrightarrow>
   2.969 +	    is_Cons(**Lset(i),a,u,co) \<longrightarrow> fun_apply(**Lset(i),rp,co,rpco) \<longrightarrow> 
   2.970 +	    number1(**Lset(i),rpco),
   2.971 +		       bo) \<and> pair(**Lset(i),u,bo,x))]"
   2.972 +apply (unfold is_bool_of_o_def) 
   2.973 +apply (intro FOL_reflections function_reflections Cons_reflection)
   2.974 +done
   2.975 +
   2.976 +lemma Forall_replacement:
   2.977 +   "[|L(A); L(rp)|]
   2.978 +    ==> strong_replacement
   2.979 +	(L, \<lambda>env z. \<exists>bo[L]. 
   2.980 +	      env \<in> list(A) & 
   2.981 +	      is_bool_of_o (L, 
   2.982 +			    \<forall>a[L]. \<forall>co[L]. \<forall>rpco[L]. 
   2.983 +			       a\<in>A --> is_Cons(L,a,env,co) -->
   2.984 +			       fun_apply(L,rp,co,rpco) --> number1(L, rpco), 
   2.985 +                            bo) &
   2.986 +	      pair(L,env,bo,z))"
   2.987 +apply (frule list_closed) 
   2.988 +apply (rule strong_replacementI) 
   2.989 +apply (rule rallI)
   2.990 +apply (rename_tac B)  
   2.991 +apply (rule separation_CollectI) 
   2.992 +apply (rule_tac A="{A,list(A),B,rp,z}" in subset_LsetE, blast ) 
   2.993 +apply (rule ReflectsE [OF Forall_Reflects], assumption)
   2.994 +apply (drule subset_Lset_ltD, assumption) 
   2.995 +apply (erule reflection_imp_L_separation)
   2.996 +  apply (simp_all add: lt_Ord2)
   2.997 +apply (simp add: is_bool_of_o_def)
   2.998 +apply (rule DPow_LsetI)
   2.999 +apply (rename_tac v) 
  2.1000 +apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
  2.1001 +apply (rule_tac env = "[u,v,A,list(A),B,rp,z]" in mem_iff_sats)
  2.1002 +apply (rule sep_rules Cons_iff_sats | simp)+
  2.1003 +done
  2.1004 +
  2.1005 +subsubsection{*The @{term "transrec_replacement"} Case*}
  2.1006 +
  2.1007 +
  2.1008 +
  2.1009 +theorem satisfies_is_a_reflection:
  2.1010 +     "REFLECTS[\<lambda>x. satisfies_is_a(L,f(x),g(x),h(x),g'(x)),
  2.1011 +               \<lambda>i x. satisfies_is_a(**Lset(i),f(x),g(x),h(x),g'(x))]"
  2.1012 +apply (unfold satisfies_is_a_def) 
  2.1013 +apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection 
  2.1014 +             nth_reflection)
  2.1015 +done
  2.1016 +
  2.1017 +
  2.1018 +theorem satisfies_is_b_reflection:
  2.1019 +     "REFLECTS[\<lambda>x. satisfies_is_b(L,f(x),g(x),h(x),g'(x)),
  2.1020 +               \<lambda>i x. satisfies_is_b(**Lset(i),f(x),g(x),h(x),g'(x))]"
  2.1021 +apply (unfold satisfies_is_b_def) 
  2.1022 +apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection 
  2.1023 +             nth_reflection)
  2.1024 +done
  2.1025 +
  2.1026 +theorem satisfies_is_c_reflection:
  2.1027 +     "REFLECTS[\<lambda>x. satisfies_is_c(L,f(x),g(x),h(x),g'(x),h'(x)),
  2.1028 +               \<lambda>i x. satisfies_is_c(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
  2.1029 +apply (unfold satisfies_is_c_def ) 
  2.1030 +apply (intro FOL_reflections function_reflections is_lambda_reflection
  2.1031 +             bool_of_o_reflection not_reflection and_reflection
  2.1032 +             nth_reflection depth_apply_reflection)
  2.1033 +done
  2.1034 +
  2.1035 +theorem satisfies_is_d_reflection:
  2.1036 +     "REFLECTS[\<lambda>x. satisfies_is_d(L,f(x),g(x),h(x),g'(x)),
  2.1037 +               \<lambda>i x. satisfies_is_d(**Lset(i),f(x),g(x),h(x),g'(x))]"
  2.1038 +apply (unfold satisfies_is_d_def ) 
  2.1039 +apply (intro FOL_reflections function_reflections is_lambda_reflection
  2.1040 +             bool_of_o_reflection not_reflection and_reflection
  2.1041 +             nth_reflection depth_apply_reflection Cons_reflection)
  2.1042 +done
  2.1043 +
  2.1044 +
  2.1045 +lemma formula_rec_replacement_Reflects:
  2.1046 + "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L, u, y, x) \<and>
  2.1047 +             is_wfrec (L, satisfies_MH(L,A), mesa, u, y)),
  2.1048 +    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
  2.1049 +             is_wfrec (**Lset(i), satisfies_MH(**Lset(i),A), mesa, u, y))]"
  2.1050 +apply (unfold satisfies_MH_def) 
  2.1051 +apply (intro FOL_reflections function_reflections is_wfrec_reflection
  2.1052 +             is_lambda_reflection) 
  2.1053 +apply (simp only: is_formula_case_def) 
  2.1054 +apply (intro FOL_reflections finite_ordinal_reflection mem_formula_reflection
  2.1055 +          Member_reflection Equal_reflection Nand_reflection Forall_reflection
  2.1056 +          satisfies_is_a_reflection satisfies_is_b_reflection 
  2.1057 +          satisfies_is_c_reflection satisfies_is_d_reflection)
  2.1058 +done
  2.1059 +
  2.1060 +end
  2.1061 +
  2.1062 +
  2.1063 +
     3.1 --- a/src/ZF/IsaMakefile	Mon Aug 12 18:01:44 2002 +0200
     3.2 +++ b/src/ZF/IsaMakefile	Tue Aug 13 11:03:11 2002 +0200
     3.3 @@ -83,7 +83,7 @@
     3.4    Constructible/L_axioms.thy    Constructible/Wellorderings.thy \
     3.5    Constructible/MetaExists.thy  Constructible/Normal.thy \
     3.6    Constructible/Rec_Separation.thy Constructible/Separation.thy \
     3.7 -  Constructible/WF_absolute.thy \
     3.8 +  Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy \
     3.9    Constructible/Reflection.thy  Constructible/WFrec.thy \
    3.10    Constructible/document/root.tex
    3.11  	@$(ISATOOL) usedir -g true $(OUT)/ZF Constructible