author paulson Thu Aug 15 21:36:26 2002 +0200 (2002-08-15) changeset 13503 d93f41fe35d2 parent 13502 da43ebc02f17 child 13504 59066e97b551
Relativization and absoluteness for DPow!!
 src/ZF/Constructible/DPow_absolute.thy file | annotate | diff | revisions src/ZF/Constructible/Internalize.thy file | annotate | diff | revisions src/ZF/Constructible/ROOT.ML file | annotate | diff | revisions src/ZF/Constructible/Rec_Separation.thy file | annotate | diff | revisions src/ZF/Constructible/Satisfies_absolute.thy file | annotate | diff | revisions src/ZF/IsaMakefile file | annotate | diff | revisions
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/ZF/Constructible/DPow_absolute.thy	Thu Aug 15 21:36:26 2002 +0200
1.3 @@ -0,0 +1,319 @@
1.4 +(*  Title:      ZF/Constructible/DPow_absolute.thy
1.5 +    ID:         \$Id\$
1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 +    Copyright   2002  University of Cambridge
1.8 +*)
1.9 +
1.10 +header {*Absoluteness for the Definable Powerset Function*}
1.11 +
1.12 +
1.13 +theory DPow_absolute = Satisfies_absolute:
1.14 +
1.15 +
1.16 +subsection{*Preliminary Internalizations*}
1.17 +
1.18 +subsubsection{*The Operator @{term is_formula_rec}*}
1.19 +
1.20 +text{*The three arguments of @{term p} are always 2, 1, 0.  It is buried
1.21 +   within 11 quantifiers!!*}
1.22 +
1.23 +(* is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
1.24 +   "is_formula_rec(M,MH,p,z)  ==
1.25 +      \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) &
1.26 +       2       1      0
1.27 +             successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
1.28 +*)
1.29 +
1.30 +constdefs formula_rec_fm :: "[i, i, i]=>i"
1.31 + "formula_rec_fm(mh,p,z) ==
1.32 +    Exists(Exists(Exists(
1.33 +      And(finite_ordinal_fm(2),
1.34 +       And(depth_fm(p#+3,2),
1.35 +        And(succ_fm(2,1),
1.36 +          And(fun_apply_fm(0,p#+3,z#+3), is_transrec_fm(mh,1,0))))))))"
1.37 +
1.38 +lemma is_formula_rec_type [TC]:
1.39 +     "[| p \<in> formula; x \<in> nat; z \<in> nat |]
1.40 +      ==> formula_rec_fm(p,x,z) \<in> formula"
1.42 +
1.43 +lemma sats_formula_rec_fm:
1.44 +  assumes MH_iff_sats:
1.45 +      "!!a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10.
1.46 +        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A; a8\<in>A; a9\<in>A; a10\<in>A|]
1.47 +        ==> MH(a2, a1, a0) <->
1.48 +            sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,
1.49 +                          Cons(a4,Cons(a5,Cons(a6,Cons(a7,
1.50 +                                  Cons(a8,Cons(a9,Cons(a10,env))))))))))))"
1.51 +  shows
1.52 +      "[|x \<in> nat; z \<in> nat; env \<in> list(A)|]
1.53 +       ==> sats(A, formula_rec_fm(p,x,z), env) <->
1.54 +           is_formula_rec(**A, MH, nth(x,env), nth(z,env))"
1.55 +by (simp add: formula_rec_fm_def sats_is_transrec_fm is_formula_rec_def
1.56 +              MH_iff_sats [THEN iff_sym])
1.57 +
1.58 +lemma formula_rec_iff_sats:
1.59 +  assumes MH_iff_sats:
1.60 +      "!!a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10.
1.61 +        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A; a8\<in>A; a9\<in>A; a10\<in>A|]
1.62 +        ==> MH(a2, a1, a0) <->
1.63 +            sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,
1.64 +                          Cons(a4,Cons(a5,Cons(a6,Cons(a7,
1.65 +                                  Cons(a8,Cons(a9,Cons(a10,env))))))))))))"
1.66 +  shows
1.67 +  "[|nth(i,env) = x; nth(k,env) = z;
1.68 +      i \<in> nat; k \<in> nat; env \<in> list(A)|]
1.69 +   ==> is_formula_rec(**A, MH, x, z) <-> sats(A, formula_rec_fm(p,i,k), env)"
1.70 +by (simp add: sats_formula_rec_fm [OF MH_iff_sats])
1.71 +
1.72 +theorem formula_rec_reflection:
1.73 +  assumes MH_reflection:
1.74 +    "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)),
1.75 +                     \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
1.76 +  shows "REFLECTS[\<lambda>x. is_formula_rec(L, MH(L,x), f(x), h(x)),
1.77 +               \<lambda>i x. is_formula_rec(**Lset(i), MH(**Lset(i),x), f(x), h(x))]"
1.78 +apply (simp (no_asm_use) only: is_formula_rec_def setclass_simps)
1.79 +apply (intro FOL_reflections function_reflections fun_plus_reflections
1.80 +             depth_reflection is_transrec_reflection MH_reflection)
1.81 +done
1.82 +
1.83 +
1.84 +subsubsection{*The Operator @{term is_satisfies}*}
1.85 +
1.86 +(* is_satisfies(M,A,p,z) == is_formula_rec (M, satisfies_MH(M,A), p, z) *)
1.87 +constdefs satisfies_fm :: "[i,i,i]=>i"
1.88 +    "satisfies_fm(x) == formula_rec_fm (satisfies_MH_fm(x#+5#+6, 2, 1, 0))"
1.89 +
1.90 +lemma is_satisfies_type [TC]:
1.91 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> satisfies_fm(x,y,z) \<in> formula"
1.93 +
1.94 +lemma sats_satisfies_fm [simp]:
1.95 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.96 +    ==> sats(A, satisfies_fm(x,y,z), env) <->
1.97 +        is_satisfies(**A, nth(x,env), nth(y,env), nth(z,env))"
1.98 +by (simp add: satisfies_fm_def is_satisfies_def sats_satisfies_MH_fm
1.99 +              sats_formula_rec_fm)
1.100 +
1.101 +lemma satisfies_iff_sats:
1.102 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.103 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.104 +       ==> is_satisfies(**A, x, y, z) <-> sats(A, satisfies_fm(i,j,k), env)"
1.106 +
1.107 +theorem satisfies_reflection:
1.108 +     "REFLECTS[\<lambda>x. is_satisfies(L,f(x),g(x),h(x)),
1.109 +               \<lambda>i x. is_satisfies(**Lset(i),f(x),g(x),h(x))]"
1.110 +apply (simp only: is_satisfies_def setclass_simps)
1.111 +apply (intro formula_rec_reflection satisfies_MH_reflection)
1.112 +done
1.113 +
1.114 +
1.115 +subsection {*Relativization of the Operator @{term DPow'}*}
1.116 +
1.117 +lemma DPow'_eq:
1.118 +  "DPow'(A) = Replace(list(A) * formula,
1.119 +              %ep z. \<exists>env \<in> list(A). \<exists>p \<in> formula.
1.120 +                     ep = <env,p> & z = {x\<in>A. sats(A, p, Cons(x,env))})"
1.121 +apply (simp add: DPow'_def, blast)
1.122 +done
1.123 +
1.124 +
1.125 +constdefs
1.126 +  is_DPow_body :: "[i=>o,i,i,i,i] => o"
1.127 +   "is_DPow_body(M,A,env,p,x) ==
1.128 +      \<forall>n1[M]. \<forall>e[M]. \<forall>sp[M].
1.129 +             is_satisfies(M,A,p,sp) --> is_Cons(M,x,env,e) -->
1.130 +             fun_apply(M, sp, e, n1) --> number1(M, n1)"
1.131 +
1.132 +lemma (in M_satisfies) DPow_body_abs:
1.133 +    "[| M(A); env \<in> list(A); p \<in> formula; M(x) |]
1.134 +    ==> is_DPow_body(M,A,env,p,x) <-> sats(A, p, Cons(x,env))"
1.135 +apply (subgoal_tac "M(env)")
1.136 + apply (simp add: is_DPow_body_def satisfies_closed satisfies_abs)
1.137 +apply (blast dest: transM)
1.138 +done
1.139 +
1.140 +lemma (in M_satisfies) Collect_DPow_body_abs:
1.141 +    "[| M(A); env \<in> list(A); p \<in> formula |]
1.142 +    ==> Collect(A, is_DPow_body(M,A,env,p)) =
1.143 +        {x \<in> A. sats(A, p, Cons(x,env))}"
1.144 +by (simp add: DPow_body_abs transM [of _ A])
1.145 +
1.146 +
1.147 +subsubsection{*The Operator @{term is_DPow_body}, Internalized*}
1.148 +
1.149 +(* is_DPow_body(M,A,env,p,x) ==
1.150 +      \<forall>n1[M]. \<forall>e[M]. \<forall>sp[M].
1.151 +             is_satisfies(M,A,p,sp) --> is_Cons(M,x,env,e) -->
1.152 +             fun_apply(M, sp, e, n1) --> number1(M, n1) *)
1.153 +
1.154 +constdefs DPow_body_fm :: "[i,i,i,i]=>i"
1.155 + "DPow_body_fm(A,env,p,x) ==
1.156 +   Forall(Forall(Forall(
1.157 +     Implies(satisfies_fm(A#+3,p#+3,0),
1.158 +       Implies(Cons_fm(x#+3,env#+3,1),
1.159 +         Implies(fun_apply_fm(0,1,2), number1_fm(2)))))))"
1.160 +
1.161 +lemma is_DPow_body_type [TC]:
1.162 +     "[| A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
1.163 +      ==> DPow_body_fm(A,x,y,z) \<in> formula"
1.165 +
1.166 +lemma sats_DPow_body_fm [simp]:
1.167 +   "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.168 +    ==> sats(A, DPow_body_fm(u,x,y,z), env) <->
1.169 +        is_DPow_body(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
1.170 +by (simp add: DPow_body_fm_def is_DPow_body_def)
1.171 +
1.172 +lemma DPow_body_iff_sats:
1.173 +  "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
1.174 +      u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.175 +   ==> is_DPow_body(**A,nu,nx,ny,nz) <->
1.176 +       sats(A, DPow_body_fm(u,x,y,z), env)"
1.177 +by simp
1.178 +
1.179 +theorem DPow_body_reflection:
1.180 +     "REFLECTS[\<lambda>x. is_DPow_body(L,f(x),g(x),h(x),g'(x)),
1.181 +               \<lambda>i x. is_DPow_body(**Lset(i),f(x),g(x),h(x),g'(x))]"
1.182 +apply (unfold is_DPow_body_def)
1.183 +apply (intro FOL_reflections function_reflections extra_reflections
1.184 +             satisfies_reflection)
1.185 +done
1.186 +
1.187 +
1.188 +subsection{*Additional Constraints on the Class Model @{term M}*}
1.189 +
1.190 +locale M_DPow = M_satisfies +
1.191 + assumes sep:
1.192 +   "[| M(A); env \<in> list(A); p \<in> formula |]
1.193 +    ==> separation(M, \<lambda>x. is_DPow_body(M,A,env,p,x))"
1.194 + and rep:
1.195 +    "M(A)
1.196 +    ==> strong_replacement (M,
1.197 +         \<lambda>ep z. \<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
1.198 +                  pair(M,env,p,ep) &
1.199 +                  is_Collect(M, A, \<lambda>x. is_DPow_body(M,A,env,p,x), z))"
1.200 +
1.201 +lemma (in M_DPow) sep':
1.202 +   "[| M(A); env \<in> list(A); p \<in> formula |]
1.203 +    ==> separation(M, \<lambda>x. sats(A, p, Cons(x,env)))"
1.204 +by (insert sep [of A env p], simp add: DPow_body_abs)
1.205 +
1.206 +lemma (in M_DPow) rep':
1.207 +   "M(A)
1.208 +    ==> strong_replacement (M,
1.209 +         \<lambda>ep z. \<exists>env\<in>list(A). \<exists>p\<in>formula.
1.210 +                  ep = <env,p> & z = {x \<in> A . sats(A, p, Cons(x, env))})"
1.211 +by (insert rep [of A], simp add: Collect_DPow_body_abs)
1.212 +
1.213 +
1.214 +lemma univalent_pair_eq:
1.215 +     "univalent (M, A, \<lambda>xy z. \<exists>x\<in>B. \<exists>y\<in>C. xy = \<langle>x,y\<rangle> \<and> z = f(x,y))"
1.216 +by (simp add: univalent_def, blast)
1.217 +
1.218 +lemma (in M_DPow) DPow'_closed: "M(A) ==> M(DPow'(A))"
1.220 +apply (fast intro: rep' sep' univalent_pair_eq)
1.221 +done
1.222 +
1.223 +text{*Relativization of the Operator @{term DPow'}*}
1.224 +constdefs
1.225 +  is_DPow' :: "[i=>o,i,i] => o"
1.226 +    "is_DPow'(M,A,Z) ==
1.227 +       \<forall>X[M]. X \<in> Z <->
1.228 +         subset(M,X,A) &
1.229 +           (\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
1.230 +                    is_Collect(M, A, is_DPow_body(M,A,env,p), X))"
1.231 +
1.232 +lemma (in M_DPow) DPow'_abs:
1.233 +    "[|M(A); M(Z)|] ==> is_DPow'(M,A,Z) <-> Z = DPow'(A)"
1.234 +apply (rule iffI)
1.235 + prefer 2 apply (simp add: is_DPow'_def DPow'_def Collect_DPow_body_abs)
1.236 +apply (rule M_equalityI)
1.237 +apply (simp add: is_DPow'_def DPow'_def Collect_DPow_body_abs, assumption)
1.238 +apply (erule DPow'_closed)
1.239 +done
1.240 +
1.241 +
1.242 +subsection{*Instantiating the Locale @{text M_DPow}*}
1.243 +
1.244 +subsubsection{*The Instance of Separation*}
1.245 +
1.246 +lemma DPow_separation:
1.247 +    "[| L(A); env \<in> list(A); p \<in> formula |]
1.248 +     ==> separation(L, \<lambda>x. is_DPow_body(L,A,env,p,x))"
1.249 +apply (subgoal_tac "L(env) & L(p)")
1.250 + prefer 2 apply (blast intro: transL)
1.251 +apply (rule separation_CollectI)
1.252 +apply (rule_tac A="{A,env,p,z}" in subset_LsetE, blast )
1.253 +apply (rule ReflectsE [OF DPow_body_reflection], assumption)
1.254 +apply (drule subset_Lset_ltD, assumption)
1.255 +apply (erule reflection_imp_L_separation)
1.256 +  apply (simp_all add: lt_Ord2)
1.257 +apply (rule DPow_LsetI)
1.258 +apply (rule_tac env = "[x,A,env,p]" in DPow_body_iff_sats)
1.259 +apply (rule sep_rules | simp)+
1.260 +done
1.261 +
1.262 +
1.263 +
1.264 +subsubsection{*The Instance of Replacement*}
1.265 +
1.266 +lemma DPow_replacement_Reflects:
1.267 + "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B &
1.268 +             (\<exists>env[L]. \<exists>p[L].
1.269 +               mem_formula(L,p) & mem_list(L,A,env) & pair(L,env,p,u) &
1.270 +               is_Collect (L, A, is_DPow_body(L,A,env,p), x)),
1.271 +    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B &
1.272 +             (\<exists>env \<in> Lset(i). \<exists>p \<in> Lset(i).
1.273 +               mem_formula(**Lset(i),p) & mem_list(**Lset(i),A,env) &
1.274 +               pair(**Lset(i),env,p,u) &
1.275 +               is_Collect (**Lset(i), A, is_DPow_body(**Lset(i),A,env,p), x))]"
1.276 +apply (unfold is_Collect_def)
1.277 +apply (intro FOL_reflections function_reflections mem_formula_reflection
1.278 +          mem_list_reflection DPow_body_reflection)
1.279 +done
1.280 +
1.281 +lemma DPow_replacement:
1.282 +    "L(A)
1.283 +    ==> strong_replacement (L,
1.284 +         \<lambda>ep z. \<exists>env[L]. \<exists>p[L]. mem_formula(L,p) & mem_list(L,A,env) &
1.285 +                  pair(L,env,p,ep) &
1.286 +                  is_Collect(L, A, \<lambda>x. is_DPow_body(L,A,env,p,x), z))"
1.287 +apply (rule strong_replacementI)
1.288 +apply (rule rallI)
1.289 +apply (rename_tac B)
1.290 +apply (rule separation_CollectI)
1.291 +apply (rule_tac A="{A,B,z}" in subset_LsetE, blast)
1.292 +apply (rule ReflectsE [OF DPow_replacement_Reflects], assumption)
1.293 +apply (drule subset_Lset_ltD, assumption)
1.294 +apply (erule reflection_imp_L_separation)
1.295 +  apply (simp_all add: lt_Ord2)
1.296 +apply (rule DPow_LsetI)
1.297 +apply (rename_tac v)
1.298 +apply (unfold is_Collect_def)
1.299 +apply (rule bex_iff_sats conj_iff_sats)+
1.300 +apply (rule_tac env = "[u,v,A,B]" in mem_iff_sats)
1.301 +apply (rule sep_rules mem_formula_iff_sats mem_list_iff_sats
1.302 +            DPow_body_iff_sats | simp)+
1.303 +done
1.304 +
1.305 +
1.306 +subsubsection{*Actually Instantiating the Locale*}
1.307 +
1.308 +lemma M_DPow_axioms_L: "M_DPow_axioms(L)"
1.309 +  apply (rule M_DPow_axioms.intro)
1.310 +   apply (assumption | rule DPow_separation DPow_replacement)+
1.311 +  done
1.312 +
1.313 +theorem M_DPow_L: "PROP M_DPow(L)"
1.314 +  apply (rule M_DPow.intro)
1.315 +       apply (rule M_satisfies.axioms [OF M_satisfies_L])+
1.316 +  apply (rule M_DPow_axioms_L)
1.317 +  done
1.318 +
1.319 +lemmas DPow'_closed [intro, simp] = M_DPow.DPow'_closed [OF M_DPow_L]
1.320 +  and DPow'_abs [intro, simp] = M_DPow.DPow'_abs [OF M_DPow_L]
1.321 +
1.322 +end
```
```     2.1 --- a/src/ZF/Constructible/Internalize.thy	Wed Aug 14 14:33:26 2002 +0200
2.2 +++ b/src/ZF/Constructible/Internalize.thy	Thu Aug 15 21:36:26 2002 +0200
2.3 @@ -556,4 +556,879 @@
2.4      Member_iff_sats Equal_iff_sats Nand_iff_sats Forall_iff_sats
2.5      is_and_iff_sats is_or_iff_sats is_not_iff_sats
2.6
2.7 +
2.8 +subsection{*Well-Founded Recursion!*}
2.9 +
2.10 +
2.11 +text{*Alternative definition, minimizing nesting of quantifiers around MH*}
2.12 +lemma M_is_recfun_iff:
2.13 +   "M_is_recfun(M,MH,r,a,f) <->
2.14 +    (\<forall>z[M]. z \<in> f <->
2.15 +     (\<exists>x[M]. \<exists>f_r_sx[M]. \<exists>y[M].
2.16 +             MH(x, f_r_sx, y) & pair(M,x,y,z) &
2.17 +             (\<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M].
2.18 +                pair(M,x,a,xa) & upair(M,x,x,sx) &
2.19 +               pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
2.20 +               xa \<in> r)))"
2.22 +apply (rule rall_cong, blast)
2.23 +done
2.24 +
2.25 +
2.26 +(* M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
2.27 +   "M_is_recfun(M,MH,r,a,f) ==
2.28 +     \<forall>z[M]. z \<in> f <->
2.29 +               2      1           0
2.30 +new def     (\<exists>x[M]. \<exists>f_r_sx[M]. \<exists>y[M].
2.31 +             MH(x, f_r_sx, y) & pair(M,x,y,z) &
2.32 +             (\<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M].
2.33 +                pair(M,x,a,xa) & upair(M,x,x,sx) &
2.34 +               pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
2.35 +               xa \<in> r)"
2.36 +*)
2.37 +
2.38 +text{*The three arguments of @{term p} are always 2, 1, 0 and z*}
2.39 +constdefs is_recfun_fm :: "[i, i, i, i]=>i"
2.40 + "is_recfun_fm(p,r,a,f) ==
2.41 +   Forall(Iff(Member(0,succ(f)),
2.42 +    Exists(Exists(Exists(
2.43 +     And(p,
2.44 +      And(pair_fm(2,0,3),
2.45 +       Exists(Exists(Exists(
2.46 +	And(pair_fm(5,a#+7,2),
2.47 +	 And(upair_fm(5,5,1),
2.48 +	  And(pre_image_fm(r#+7,1,0),
2.49 +	   And(restriction_fm(f#+7,0,4), Member(2,r#+7)))))))))))))))"
2.50 +
2.51 +lemma is_recfun_type [TC]:
2.52 +     "[| p \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |]
2.53 +      ==> is_recfun_fm(p,x,y,z) \<in> formula"
2.55 +
2.56 +
2.57 +lemma sats_is_recfun_fm:
2.58 +  assumes MH_iff_sats:
2.59 +      "!!a0 a1 a2 a3.
2.60 +        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A|]
2.61 +        ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,env)))))"
2.62 +  shows
2.63 +      "[|x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
2.64 +       ==> sats(A, is_recfun_fm(p,x,y,z), env) <->
2.65 +           M_is_recfun(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
2.66 +by (simp add: is_recfun_fm_def M_is_recfun_iff MH_iff_sats [THEN iff_sym])
2.67 +
2.68 +lemma is_recfun_iff_sats:
2.69 +  assumes MH_iff_sats:
2.70 +      "!!a0 a1 a2 a3.
2.71 +        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A|]
2.72 +        ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,env)))))"
2.73 +  shows
2.74 +  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
2.75 +      i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
2.76 +   ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)"
2.77 +by (simp add: sats_is_recfun_fm [OF MH_iff_sats])
2.78 +
2.79 +text{*The additional variable in the premise, namely @{term f'}, is essential.
2.80 +It lets @{term MH} depend upon @{term x}, which seems often necessary.
2.81 +The same thing occurs in @{text is_wfrec_reflection}.*}
2.82 +theorem is_recfun_reflection:
2.83 +  assumes MH_reflection:
2.84 +    "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)),
2.85 +                     \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
2.86 +  shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L,x), f(x), g(x), h(x)),
2.87 +             \<lambda>i x. M_is_recfun(**Lset(i), MH(**Lset(i),x), f(x), g(x), h(x))]"
2.88 +apply (simp (no_asm_use) only: M_is_recfun_def setclass_simps)
2.89 +apply (intro FOL_reflections function_reflections
2.90 +             restriction_reflection MH_reflection)
2.91 +done
2.92 +
2.93 +subsubsection{*The Operator @{term is_wfrec}*}
2.94 +
2.95 +text{*The three arguments of @{term p} are always 2, 1, 0*}
2.96 +
2.97 +(* is_wfrec :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
2.98 +    "is_wfrec(M,MH,r,a,z) ==
2.99 +      \<exists>f[M]. M_is_recfun(M,MH,r,a,f) & MH(a,f,z)" *)
2.100 +constdefs is_wfrec_fm :: "[i, i, i, i]=>i"
2.101 + "is_wfrec_fm(p,r,a,z) ==
2.102 +    Exists(And(is_recfun_fm(p, succ(r), succ(a), 0),
2.103 +           Exists(Exists(Exists(Exists(
2.104 +             And(Equal(2,a#+5), And(Equal(1,4), And(Equal(0,z#+5), p)))))))))"
2.105 +
2.106 +text{*We call @{term p} with arguments a, f, z by equating them with
2.107 +  the corresponding quantified variables with de Bruijn indices 2, 1, 0.*}
2.108 +
2.109 +text{*There's an additional existential quantifier to ensure that the
2.110 +      environments in both calls to MH have the same length.*}
2.111 +
2.112 +lemma is_wfrec_type [TC]:
2.113 +     "[| p \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |]
2.114 +      ==> is_wfrec_fm(p,x,y,z) \<in> formula"
2.116 +
2.117 +lemma sats_is_wfrec_fm:
2.118 +  assumes MH_iff_sats:
2.119 +      "!!a0 a1 a2 a3 a4.
2.120 +        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A|]
2.121 +        ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
2.122 +  shows
2.123 +      "[|x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
2.124 +       ==> sats(A, is_wfrec_fm(p,x,y,z), env) <->
2.125 +           is_wfrec(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
2.126 +apply (frule_tac x=z in lt_length_in_nat, assumption)
2.127 +apply (frule lt_length_in_nat, assumption)
2.128 +apply (simp add: is_wfrec_fm_def sats_is_recfun_fm is_wfrec_def MH_iff_sats [THEN iff_sym], blast)
2.129 +done
2.130 +
2.131 +
2.132 +lemma is_wfrec_iff_sats:
2.133 +  assumes MH_iff_sats:
2.134 +      "!!a0 a1 a2 a3 a4.
2.135 +        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A|]
2.136 +        ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
2.137 +  shows
2.138 +  "[|nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
2.139 +      i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
2.140 +   ==> is_wfrec(**A, MH, x, y, z) <-> sats(A, is_wfrec_fm(p,i,j,k), env)"
2.141 +by (simp add: sats_is_wfrec_fm [OF MH_iff_sats])
2.142 +
2.143 +theorem is_wfrec_reflection:
2.144 +  assumes MH_reflection:
2.145 +    "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)),
2.146 +                     \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
2.147 +  shows "REFLECTS[\<lambda>x. is_wfrec(L, MH(L,x), f(x), g(x), h(x)),
2.148 +               \<lambda>i x. is_wfrec(**Lset(i), MH(**Lset(i),x), f(x), g(x), h(x))]"
2.149 +apply (simp (no_asm_use) only: is_wfrec_def setclass_simps)
2.150 +apply (intro FOL_reflections MH_reflection is_recfun_reflection)
2.151 +done
2.152 +
2.153 +
2.154 +subsection{*For Datatypes*}
2.155 +
2.156 +subsubsection{*Binary Products, Internalized*}
2.157 +
2.158 +constdefs cartprod_fm :: "[i,i,i]=>i"
2.159 +(* "cartprod(M,A,B,z) ==
2.160 +        \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))" *)
2.161 +    "cartprod_fm(A,B,z) ==
2.162 +       Forall(Iff(Member(0,succ(z)),
2.163 +                  Exists(And(Member(0,succ(succ(A))),
2.164 +                         Exists(And(Member(0,succ(succ(succ(B)))),
2.165 +                                    pair_fm(1,0,2)))))))"
2.166 +
2.167 +lemma cartprod_type [TC]:
2.168 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> cartprod_fm(x,y,z) \<in> formula"
2.170 +
2.171 +lemma arity_cartprod_fm [simp]:
2.172 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
2.173 +      ==> arity(cartprod_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
2.174 +by (simp add: cartprod_fm_def succ_Un_distrib [symmetric] Un_ac)
2.175 +
2.176 +lemma sats_cartprod_fm [simp]:
2.177 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
2.178 +    ==> sats(A, cartprod_fm(x,y,z), env) <->
2.179 +        cartprod(**A, nth(x,env), nth(y,env), nth(z,env))"
2.180 +by (simp add: cartprod_fm_def cartprod_def)
2.181 +
2.182 +lemma cartprod_iff_sats:
2.183 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
2.184 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
2.185 +       ==> cartprod(**A, x, y, z) <-> sats(A, cartprod_fm(i,j,k), env)"
2.187 +
2.188 +theorem cartprod_reflection:
2.189 +     "REFLECTS[\<lambda>x. cartprod(L,f(x),g(x),h(x)),
2.190 +               \<lambda>i x. cartprod(**Lset(i),f(x),g(x),h(x))]"
2.191 +apply (simp only: cartprod_def setclass_simps)
2.192 +apply (intro FOL_reflections pair_reflection)
2.193 +done
2.194 +
2.195 +
2.196 +subsubsection{*Binary Sums, Internalized*}
2.197 +
2.198 +(* "is_sum(M,A,B,Z) ==
2.199 +       \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M].
2.200 +         3      2       1        0
2.201 +       number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
2.202 +       cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"  *)
2.203 +constdefs sum_fm :: "[i,i,i]=>i"
2.204 +    "sum_fm(A,B,Z) ==
2.205 +       Exists(Exists(Exists(Exists(
2.206 +        And(number1_fm(2),
2.207 +            And(cartprod_fm(2,A#+4,3),
2.208 +                And(upair_fm(2,2,1),
2.209 +                    And(cartprod_fm(1,B#+4,0), union_fm(3,0,Z#+4)))))))))"
2.210 +
2.211 +lemma sum_type [TC]:
2.212 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> sum_fm(x,y,z) \<in> formula"
2.214 +
2.215 +lemma arity_sum_fm [simp]:
2.216 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
2.217 +      ==> arity(sum_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
2.218 +by (simp add: sum_fm_def succ_Un_distrib [symmetric] Un_ac)
2.219 +
2.220 +lemma sats_sum_fm [simp]:
2.221 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
2.222 +    ==> sats(A, sum_fm(x,y,z), env) <->
2.223 +        is_sum(**A, nth(x,env), nth(y,env), nth(z,env))"
2.224 +by (simp add: sum_fm_def is_sum_def)
2.225 +
2.226 +lemma sum_iff_sats:
2.227 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
2.228 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
2.229 +       ==> is_sum(**A, x, y, z) <-> sats(A, sum_fm(i,j,k), env)"
2.230 +by simp
2.231 +
2.232 +theorem sum_reflection:
2.233 +     "REFLECTS[\<lambda>x. is_sum(L,f(x),g(x),h(x)),
2.234 +               \<lambda>i x. is_sum(**Lset(i),f(x),g(x),h(x))]"
2.235 +apply (simp only: is_sum_def setclass_simps)
2.236 +apply (intro FOL_reflections function_reflections cartprod_reflection)
2.237 +done
2.238 +
2.239 +
2.240 +subsubsection{*The Operator @{term quasinat}*}
2.241 +
2.242 +(* "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))" *)
2.243 +constdefs quasinat_fm :: "i=>i"
2.244 +    "quasinat_fm(z) == Or(empty_fm(z), Exists(succ_fm(0,succ(z))))"
2.245 +
2.246 +lemma quasinat_type [TC]:
2.247 +     "x \<in> nat ==> quasinat_fm(x) \<in> formula"
2.249 +
2.250 +lemma arity_quasinat_fm [simp]:
2.251 +     "x \<in> nat ==> arity(quasinat_fm(x)) = succ(x)"
2.252 +by (simp add: quasinat_fm_def succ_Un_distrib [symmetric] Un_ac)
2.253 +
2.254 +lemma sats_quasinat_fm [simp]:
2.255 +   "[| x \<in> nat; env \<in> list(A)|]
2.256 +    ==> sats(A, quasinat_fm(x), env) <-> is_quasinat(**A, nth(x,env))"
2.257 +by (simp add: quasinat_fm_def is_quasinat_def)
2.258 +
2.259 +lemma quasinat_iff_sats:
2.260 +      "[| nth(i,env) = x; nth(j,env) = y;
2.261 +          i \<in> nat; env \<in> list(A)|]
2.262 +       ==> is_quasinat(**A, x) <-> sats(A, quasinat_fm(i), env)"
2.263 +by simp
2.264 +
2.265 +theorem quasinat_reflection:
2.266 +     "REFLECTS[\<lambda>x. is_quasinat(L,f(x)),
2.267 +               \<lambda>i x. is_quasinat(**Lset(i),f(x))]"
2.268 +apply (simp only: is_quasinat_def setclass_simps)
2.269 +apply (intro FOL_reflections function_reflections)
2.270 +done
2.271 +
2.272 +
2.273 +subsubsection{*The Operator @{term is_nat_case}*}
2.274 +text{*I could not get it to work with the more natural assumption that
2.275 + @{term is_b} takes two arguments.  Instead it must be a formula where 1 and 0
2.276 + stand for @{term m} and @{term b}, respectively.*}
2.277 +
2.278 +(* is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o"
2.279 +    "is_nat_case(M, a, is_b, k, z) ==
2.280 +       (empty(M,k) --> z=a) &
2.281 +       (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
2.282 +       (is_quasinat(M,k) | empty(M,z))" *)
2.283 +text{*The formula @{term is_b} has free variables 1 and 0.*}
2.284 +constdefs is_nat_case_fm :: "[i, i, i, i]=>i"
2.285 + "is_nat_case_fm(a,is_b,k,z) ==
2.286 +    And(Implies(empty_fm(k), Equal(z,a)),
2.287 +        And(Forall(Implies(succ_fm(0,succ(k)),
2.288 +                   Forall(Implies(Equal(0,succ(succ(z))), is_b)))),
2.289 +            Or(quasinat_fm(k), empty_fm(z))))"
2.290 +
2.291 +lemma is_nat_case_type [TC]:
2.292 +     "[| is_b \<in> formula;
2.293 +         x \<in> nat; y \<in> nat; z \<in> nat |]
2.294 +      ==> is_nat_case_fm(x,is_b,y,z) \<in> formula"
2.296 +
2.297 +lemma sats_is_nat_case_fm:
2.298 +  assumes is_b_iff_sats:
2.299 +      "!!a. a \<in> A ==> is_b(a,nth(z, env)) <->
2.300 +                      sats(A, p, Cons(nth(z,env), Cons(a, env)))"
2.301 +  shows
2.302 +      "[|x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
2.303 +       ==> sats(A, is_nat_case_fm(x,p,y,z), env) <->
2.304 +           is_nat_case(**A, nth(x,env), is_b, nth(y,env), nth(z,env))"
2.305 +apply (frule lt_length_in_nat, assumption)
2.306 +apply (simp add: is_nat_case_fm_def is_nat_case_def is_b_iff_sats [THEN iff_sym])
2.307 +done
2.308 +
2.309 +lemma is_nat_case_iff_sats:
2.310 +  "[| (!!a. a \<in> A ==> is_b(a,z) <->
2.311 +                      sats(A, p, Cons(z, Cons(a,env))));
2.312 +      nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
2.313 +      i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
2.314 +   ==> is_nat_case(**A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)"
2.315 +by (simp add: sats_is_nat_case_fm [of A is_b])
2.316 +
2.317 +
2.318 +text{*The second argument of @{term is_b} gives it direct access to @{term x},
2.319 +  which is essential for handling free variable references.  Without this
2.320 +  argument, we cannot prove reflection for @{term iterates_MH}.*}
2.321 +theorem is_nat_case_reflection:
2.322 +  assumes is_b_reflection:
2.323 +    "!!h f g. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x)),
2.324 +                     \<lambda>i x. is_b(**Lset(i), h(x), f(x), g(x))]"
2.325 +  shows "REFLECTS[\<lambda>x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)),
2.326 +               \<lambda>i x. is_nat_case(**Lset(i), f(x), is_b(**Lset(i), x), g(x), h(x))]"
2.327 +apply (simp (no_asm_use) only: is_nat_case_def setclass_simps)
2.328 +apply (intro FOL_reflections function_reflections
2.329 +             restriction_reflection is_b_reflection quasinat_reflection)
2.330 +done
2.331 +
2.332 +
2.333 +subsection{*The Operator @{term iterates_MH}, Needed for Iteration*}
2.334 +
2.335 +(*  iterates_MH :: "[i=>o, [i,i]=>o, i, i, i, i] => o"
2.336 +   "iterates_MH(M,isF,v,n,g,z) ==
2.337 +        is_nat_case(M, v, \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & isF(gm,u),
2.338 +                    n, z)" *)
2.339 +constdefs iterates_MH_fm :: "[i, i, i, i, i]=>i"
2.340 + "iterates_MH_fm(isF,v,n,g,z) ==
2.341 +    is_nat_case_fm(v,
2.342 +      Exists(And(fun_apply_fm(succ(succ(succ(g))),2,0),
2.343 +                     Forall(Implies(Equal(0,2), isF)))),
2.344 +      n, z)"
2.345 +
2.346 +lemma iterates_MH_type [TC]:
2.347 +     "[| p \<in> formula;
2.348 +         v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
2.349 +      ==> iterates_MH_fm(p,v,x,y,z) \<in> formula"
2.351 +
2.352 +lemma sats_iterates_MH_fm:
2.353 +  assumes is_F_iff_sats:
2.354 +      "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
2.355 +              ==> is_F(a,b) <->
2.356 +                  sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env)))))"
2.357 +  shows
2.358 +      "[|v \<in> nat; x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
2.359 +       ==> sats(A, iterates_MH_fm(p,v,x,y,z), env) <->
2.360 +           iterates_MH(**A, is_F, nth(v,env), nth(x,env), nth(y,env), nth(z,env))"
2.361 +apply (frule lt_length_in_nat, assumption)
2.362 +apply (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm
2.363 +              is_F_iff_sats [symmetric])
2.364 +apply (rule is_nat_case_cong)
2.366 +done
2.367 +
2.368 +lemma iterates_MH_iff_sats:
2.369 +  assumes is_F_iff_sats:
2.370 +      "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
2.371 +              ==> is_F(a,b) <->
2.372 +                  sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env)))))"
2.373 +  shows
2.374 +  "[| nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
2.375 +      i' \<in> nat; i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
2.376 +   ==> iterates_MH(**A, is_F, v, x, y, z) <->
2.377 +       sats(A, iterates_MH_fm(p,i',i,j,k), env)"
2.378 +by (simp add: sats_iterates_MH_fm [OF is_F_iff_sats])
2.379 +
2.380 +text{*The second argument of @{term p} gives it direct access to @{term x},
2.381 +  which is essential for handling free variable references.  Without this
2.382 +  argument, we cannot prove reflection for @{term list_N}.*}
2.383 +theorem iterates_MH_reflection:
2.384 +  assumes p_reflection:
2.385 +    "!!f g h. REFLECTS[\<lambda>x. p(L, h(x), f(x), g(x)),
2.386 +                     \<lambda>i x. p(**Lset(i), h(x), f(x), g(x))]"
2.387 + shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L,x), e(x), f(x), g(x), h(x)),
2.388 +               \<lambda>i x. iterates_MH(**Lset(i), p(**Lset(i),x), e(x), f(x), g(x), h(x))]"
2.389 +apply (simp (no_asm_use) only: iterates_MH_def)
2.390 +txt{*Must be careful: simplifying with @{text setclass_simps} above would
2.391 +     change @{text "\<exists>gm[**Lset(i)]"} into @{text "\<exists>gm \<in> Lset(i)"}, when
2.392 +     it would no longer match rule @{text is_nat_case_reflection}. *}
2.393 +apply (rule is_nat_case_reflection)
2.394 +apply (simp (no_asm_use) only: setclass_simps)
2.395 +apply (intro FOL_reflections function_reflections is_nat_case_reflection
2.396 +             restriction_reflection p_reflection)
2.397 +done
2.398 +
2.399 +
2.400 +
2.401 +subsubsection{*The Formula @{term is_eclose_n}, Internalized*}
2.402 +
2.403 +(* is_eclose_n(M,A,n,Z) ==
2.404 +      \<exists>sn[M]. \<exists>msn[M].
2.405 +       1       0
2.406 +       successor(M,n,sn) & membership(M,sn,msn) &
2.407 +       is_wfrec(M, iterates_MH(M, big_union(M), A), msn, n, Z) *)
2.408 +
2.409 +constdefs eclose_n_fm :: "[i,i,i]=>i"
2.410 +  "eclose_n_fm(A,n,Z) ==
2.411 +     Exists(Exists(
2.412 +      And(succ_fm(n#+2,1),
2.413 +       And(Memrel_fm(1,0),
2.414 +              is_wfrec_fm(iterates_MH_fm(big_union_fm(1,0),
2.415 +                                         A#+7, 2, 1, 0),
2.416 +                           0, n#+2, Z#+2)))))"
2.417 +
2.418 +lemma eclose_n_fm_type [TC]:
2.419 + "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> eclose_n_fm(x,y,z) \<in> formula"
2.421 +
2.422 +lemma sats_eclose_n_fm [simp]:
2.423 +   "[| x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
2.424 +    ==> sats(A, eclose_n_fm(x,y,z), env) <->
2.425 +        is_eclose_n(**A, nth(x,env), nth(y,env), nth(z,env))"
2.426 +apply (frule_tac x=z in lt_length_in_nat, assumption)
2.427 +apply (frule_tac x=y in lt_length_in_nat, assumption)
2.428 +apply (simp add: eclose_n_fm_def is_eclose_n_def sats_is_wfrec_fm
2.429 +                 sats_iterates_MH_fm)
2.430 +done
2.431 +
2.432 +lemma eclose_n_iff_sats:
2.433 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
2.434 +          i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
2.435 +       ==> is_eclose_n(**A, x, y, z) <-> sats(A, eclose_n_fm(i,j,k), env)"
2.437 +
2.438 +theorem eclose_n_reflection:
2.439 +     "REFLECTS[\<lambda>x. is_eclose_n(L, f(x), g(x), h(x)),
2.440 +               \<lambda>i x. is_eclose_n(**Lset(i), f(x), g(x), h(x))]"
2.441 +apply (simp only: is_eclose_n_def setclass_simps)
2.442 +apply (intro FOL_reflections function_reflections is_wfrec_reflection
2.443 +             iterates_MH_reflection)
2.444 +done
2.445 +
2.446 +
2.447 +subsubsection{*Membership in @{term "eclose(A)"}*}
2.448 +
2.449 +(* mem_eclose(M,A,l) ==
2.450 +      \<exists>n[M]. \<exists>eclosen[M].
2.451 +       finite_ordinal(M,n) & is_eclose_n(M,A,n,eclosen) & l \<in> eclosen *)
2.452 +constdefs mem_eclose_fm :: "[i,i]=>i"
2.453 +    "mem_eclose_fm(x,y) ==
2.454 +       Exists(Exists(
2.455 +         And(finite_ordinal_fm(1),
2.456 +           And(eclose_n_fm(x#+2,1,0), Member(y#+2,0)))))"
2.457 +
2.458 +lemma mem_eclose_type [TC]:
2.459 +     "[| x \<in> nat; y \<in> nat |] ==> mem_eclose_fm(x,y) \<in> formula"
2.461 +
2.462 +lemma sats_mem_eclose_fm [simp]:
2.463 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
2.464 +    ==> sats(A, mem_eclose_fm(x,y), env) <-> mem_eclose(**A, nth(x,env), nth(y,env))"
2.465 +by (simp add: mem_eclose_fm_def mem_eclose_def)
2.466 +
2.467 +lemma mem_eclose_iff_sats:
2.468 +      "[| nth(i,env) = x; nth(j,env) = y;
2.469 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
2.470 +       ==> mem_eclose(**A, x, y) <-> sats(A, mem_eclose_fm(i,j), env)"
2.471 +by simp
2.472 +
2.473 +theorem mem_eclose_reflection:
2.474 +     "REFLECTS[\<lambda>x. mem_eclose(L,f(x),g(x)),
2.475 +               \<lambda>i x. mem_eclose(**Lset(i),f(x),g(x))]"
2.476 +apply (simp only: mem_eclose_def setclass_simps)
2.477 +apply (intro FOL_reflections finite_ordinal_reflection eclose_n_reflection)
2.478 +done
2.479 +
2.480 +
2.481 +subsubsection{*The Predicate ``Is @{term "eclose(A)"}''*}
2.482 +
2.483 +(* is_eclose(M,A,Z) == \<forall>l[M]. l \<in> Z <-> mem_eclose(M,A,l) *)
2.484 +constdefs is_eclose_fm :: "[i,i]=>i"
2.485 +    "is_eclose_fm(A,Z) ==
2.486 +       Forall(Iff(Member(0,succ(Z)), mem_eclose_fm(succ(A),0)))"
2.487 +
2.488 +lemma is_eclose_type [TC]:
2.489 +     "[| x \<in> nat; y \<in> nat |] ==> is_eclose_fm(x,y) \<in> formula"
2.491 +
2.492 +lemma sats_is_eclose_fm [simp]:
2.493 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
2.494 +    ==> sats(A, is_eclose_fm(x,y), env) <-> is_eclose(**A, nth(x,env), nth(y,env))"
2.495 +by (simp add: is_eclose_fm_def is_eclose_def)
2.496 +
2.497 +lemma is_eclose_iff_sats:
2.498 +      "[| nth(i,env) = x; nth(j,env) = y;
2.499 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
2.500 +       ==> is_eclose(**A, x, y) <-> sats(A, is_eclose_fm(i,j), env)"
2.501 +by simp
2.502 +
2.503 +theorem is_eclose_reflection:
2.504 +     "REFLECTS[\<lambda>x. is_eclose(L,f(x),g(x)),
2.505 +               \<lambda>i x. is_eclose(**Lset(i),f(x),g(x))]"
2.506 +apply (simp only: is_eclose_def setclass_simps)
2.507 +apply (intro FOL_reflections mem_eclose_reflection)
2.508 +done
2.509 +
2.510 +
2.511 +subsubsection{*The List Functor, Internalized*}
2.512 +
2.513 +constdefs list_functor_fm :: "[i,i,i]=>i"
2.514 +(* "is_list_functor(M,A,X,Z) ==
2.515 +        \<exists>n1[M]. \<exists>AX[M].
2.516 +         number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)" *)
2.517 +    "list_functor_fm(A,X,Z) ==
2.518 +       Exists(Exists(
2.519 +        And(number1_fm(1),
2.520 +            And(cartprod_fm(A#+2,X#+2,0), sum_fm(1,0,Z#+2)))))"
2.521 +
2.522 +lemma list_functor_type [TC]:
2.523 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> list_functor_fm(x,y,z) \<in> formula"
2.525 +
2.526 +lemma arity_list_functor_fm [simp]:
2.527 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
2.528 +      ==> arity(list_functor_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
2.529 +by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac)
2.530 +
2.531 +lemma sats_list_functor_fm [simp]:
2.532 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
2.533 +    ==> sats(A, list_functor_fm(x,y,z), env) <->
2.534 +        is_list_functor(**A, nth(x,env), nth(y,env), nth(z,env))"
2.535 +by (simp add: list_functor_fm_def is_list_functor_def)
2.536 +
2.537 +lemma list_functor_iff_sats:
2.538 +  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
2.539 +      i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
2.540 +   ==> is_list_functor(**A, x, y, z) <-> sats(A, list_functor_fm(i,j,k), env)"
2.541 +by simp
2.542 +
2.543 +theorem list_functor_reflection:
2.544 +     "REFLECTS[\<lambda>x. is_list_functor(L,f(x),g(x),h(x)),
2.545 +               \<lambda>i x. is_list_functor(**Lset(i),f(x),g(x),h(x))]"
2.546 +apply (simp only: is_list_functor_def setclass_simps)
2.547 +apply (intro FOL_reflections number1_reflection
2.548 +             cartprod_reflection sum_reflection)
2.549 +done
2.550 +
2.551 +
2.552 +subsubsection{*The Formula @{term is_list_N}, Internalized*}
2.553 +
2.554 +(* "is_list_N(M,A,n,Z) ==
2.555 +      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M].
2.556 +       empty(M,zero) &
2.557 +       successor(M,n,sn) & membership(M,sn,msn) &
2.558 +       is_wfrec(M, iterates_MH(M, is_list_functor(M,A),zero), msn, n, Z)" *)
2.559 +
2.560 +constdefs list_N_fm :: "[i,i,i]=>i"
2.561 +  "list_N_fm(A,n,Z) ==
2.562 +     Exists(Exists(Exists(
2.563 +       And(empty_fm(2),
2.564 +         And(succ_fm(n#+3,1),
2.565 +          And(Memrel_fm(1,0),
2.566 +              is_wfrec_fm(iterates_MH_fm(list_functor_fm(A#+9#+3,1,0),
2.567 +                                         7,2,1,0),
2.568 +                           0, n#+3, Z#+3)))))))"
2.569 +
2.570 +lemma list_N_fm_type [TC]:
2.571 + "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> list_N_fm(x,y,z) \<in> formula"
2.573 +
2.574 +lemma sats_list_N_fm [simp]:
2.575 +   "[| x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
2.576 +    ==> sats(A, list_N_fm(x,y,z), env) <->
2.577 +        is_list_N(**A, nth(x,env), nth(y,env), nth(z,env))"
2.578 +apply (frule_tac x=z in lt_length_in_nat, assumption)
2.579 +apply (frule_tac x=y in lt_length_in_nat, assumption)
2.580 +apply (simp add: list_N_fm_def is_list_N_def sats_is_wfrec_fm
2.581 +                 sats_iterates_MH_fm)
2.582 +done
2.583 +
2.584 +lemma list_N_iff_sats:
2.585 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
2.586 +          i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
2.587 +       ==> is_list_N(**A, x, y, z) <-> sats(A, list_N_fm(i,j,k), env)"
2.589 +
2.590 +theorem list_N_reflection:
2.591 +     "REFLECTS[\<lambda>x. is_list_N(L, f(x), g(x), h(x)),
2.592 +               \<lambda>i x. is_list_N(**Lset(i), f(x), g(x), h(x))]"
2.593 +apply (simp only: is_list_N_def setclass_simps)
2.594 +apply (intro FOL_reflections function_reflections is_wfrec_reflection
2.595 +             iterates_MH_reflection list_functor_reflection)
2.596 +done
2.597 +
2.598 +
2.599 +
2.600 +subsubsection{*The Predicate ``Is A List''*}
2.601 +
2.602 +(* mem_list(M,A,l) ==
2.603 +      \<exists>n[M]. \<exists>listn[M].
2.604 +       finite_ordinal(M,n) & is_list_N(M,A,n,listn) & l \<in> listn *)
2.605 +constdefs mem_list_fm :: "[i,i]=>i"
2.606 +    "mem_list_fm(x,y) ==
2.607 +       Exists(Exists(
2.608 +         And(finite_ordinal_fm(1),
2.609 +           And(list_N_fm(x#+2,1,0), Member(y#+2,0)))))"
2.610 +
2.611 +lemma mem_list_type [TC]:
2.612 +     "[| x \<in> nat; y \<in> nat |] ==> mem_list_fm(x,y) \<in> formula"
2.614 +
2.615 +lemma sats_mem_list_fm [simp]:
2.616 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
2.617 +    ==> sats(A, mem_list_fm(x,y), env) <-> mem_list(**A, nth(x,env), nth(y,env))"
2.618 +by (simp add: mem_list_fm_def mem_list_def)
2.619 +
2.620 +lemma mem_list_iff_sats:
2.621 +      "[| nth(i,env) = x; nth(j,env) = y;
2.622 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
2.623 +       ==> mem_list(**A, x, y) <-> sats(A, mem_list_fm(i,j), env)"
2.624 +by simp
2.625 +
2.626 +theorem mem_list_reflection:
2.627 +     "REFLECTS[\<lambda>x. mem_list(L,f(x),g(x)),
2.628 +               \<lambda>i x. mem_list(**Lset(i),f(x),g(x))]"
2.629 +apply (simp only: mem_list_def setclass_simps)
2.630 +apply (intro FOL_reflections finite_ordinal_reflection list_N_reflection)
2.631 +done
2.632 +
2.633 +
2.634 +subsubsection{*The Predicate ``Is @{term "list(A)"}''*}
2.635 +
2.636 +(* is_list(M,A,Z) == \<forall>l[M]. l \<in> Z <-> mem_list(M,A,l) *)
2.637 +constdefs is_list_fm :: "[i,i]=>i"
2.638 +    "is_list_fm(A,Z) ==
2.639 +       Forall(Iff(Member(0,succ(Z)), mem_list_fm(succ(A),0)))"
2.640 +
2.641 +lemma is_list_type [TC]:
2.642 +     "[| x \<in> nat; y \<in> nat |] ==> is_list_fm(x,y) \<in> formula"
2.644 +
2.645 +lemma sats_is_list_fm [simp]:
2.646 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
2.647 +    ==> sats(A, is_list_fm(x,y), env) <-> is_list(**A, nth(x,env), nth(y,env))"
2.648 +by (simp add: is_list_fm_def is_list_def)
2.649 +
2.650 +lemma is_list_iff_sats:
2.651 +      "[| nth(i,env) = x; nth(j,env) = y;
2.652 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
2.653 +       ==> is_list(**A, x, y) <-> sats(A, is_list_fm(i,j), env)"
2.654 +by simp
2.655 +
2.656 +theorem is_list_reflection:
2.657 +     "REFLECTS[\<lambda>x. is_list(L,f(x),g(x)),
2.658 +               \<lambda>i x. is_list(**Lset(i),f(x),g(x))]"
2.659 +apply (simp only: is_list_def setclass_simps)
2.660 +apply (intro FOL_reflections mem_list_reflection)
2.661 +done
2.662 +
2.663 +
2.664 +subsubsection{*The Formula Functor, Internalized*}
2.665 +
2.666 +constdefs formula_functor_fm :: "[i,i]=>i"
2.667 +(*     "is_formula_functor(M,X,Z) ==
2.668 +        \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M].
2.669 +           4           3               2       1       0
2.670 +          omega(M,nat') & cartprod(M,nat',nat',natnat) &
2.671 +          is_sum(M,natnat,natnat,natnatsum) &
2.672 +          cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) &
2.673 +          is_sum(M,natnatsum,X3,Z)" *)
2.674 +    "formula_functor_fm(X,Z) ==
2.675 +       Exists(Exists(Exists(Exists(Exists(
2.676 +        And(omega_fm(4),
2.677 +         And(cartprod_fm(4,4,3),
2.678 +          And(sum_fm(3,3,2),
2.679 +           And(cartprod_fm(X#+5,X#+5,1),
2.680 +            And(sum_fm(1,X#+5,0), sum_fm(2,0,Z#+5)))))))))))"
2.681 +
2.682 +lemma formula_functor_type [TC]:
2.683 +     "[| x \<in> nat; y \<in> nat |] ==> formula_functor_fm(x,y) \<in> formula"
2.685 +
2.686 +lemma sats_formula_functor_fm [simp]:
2.687 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
2.688 +    ==> sats(A, formula_functor_fm(x,y), env) <->
2.689 +        is_formula_functor(**A, nth(x,env), nth(y,env))"
2.690 +by (simp add: formula_functor_fm_def is_formula_functor_def)
2.691 +
2.692 +lemma formula_functor_iff_sats:
2.693 +  "[| nth(i,env) = x; nth(j,env) = y;
2.694 +      i \<in> nat; j \<in> nat; env \<in> list(A)|]
2.695 +   ==> is_formula_functor(**A, x, y) <-> sats(A, formula_functor_fm(i,j), env)"
2.696 +by simp
2.697 +
2.698 +theorem formula_functor_reflection:
2.699 +     "REFLECTS[\<lambda>x. is_formula_functor(L,f(x),g(x)),
2.700 +               \<lambda>i x. is_formula_functor(**Lset(i),f(x),g(x))]"
2.701 +apply (simp only: is_formula_functor_def setclass_simps)
2.702 +apply (intro FOL_reflections omega_reflection
2.703 +             cartprod_reflection sum_reflection)
2.704 +done
2.705 +
2.706 +
2.707 +subsubsection{*The Formula @{term is_formula_N}, Internalized*}
2.708 +
2.709 +(* "is_formula_N(M,n,Z) ==
2.710 +      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M].
2.711 +          2       1       0
2.712 +       empty(M,zero) &
2.713 +       successor(M,n,sn) & membership(M,sn,msn) &
2.714 +       is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)" *)
2.715 +constdefs formula_N_fm :: "[i,i]=>i"
2.716 +  "formula_N_fm(n,Z) ==
2.717 +     Exists(Exists(Exists(
2.718 +       And(empty_fm(2),
2.719 +         And(succ_fm(n#+3,1),
2.720 +          And(Memrel_fm(1,0),
2.721 +              is_wfrec_fm(iterates_MH_fm(formula_functor_fm(1,0),7,2,1,0),
2.722 +                           0, n#+3, Z#+3)))))))"
2.723 +
2.724 +lemma formula_N_fm_type [TC]:
2.725 + "[| x \<in> nat; y \<in> nat |] ==> formula_N_fm(x,y) \<in> formula"
2.727 +
2.728 +lemma sats_formula_N_fm [simp]:
2.729 +   "[| x < length(env); y < length(env); env \<in> list(A)|]
2.730 +    ==> sats(A, formula_N_fm(x,y), env) <->
2.731 +        is_formula_N(**A, nth(x,env), nth(y,env))"
2.732 +apply (frule_tac x=y in lt_length_in_nat, assumption)
2.733 +apply (frule lt_length_in_nat, assumption)
2.734 +apply (simp add: formula_N_fm_def is_formula_N_def sats_is_wfrec_fm sats_iterates_MH_fm)
2.735 +done
2.736 +
2.737 +lemma formula_N_iff_sats:
2.738 +      "[| nth(i,env) = x; nth(j,env) = y;
2.739 +          i < length(env); j < length(env); env \<in> list(A)|]
2.740 +       ==> is_formula_N(**A, x, y) <-> sats(A, formula_N_fm(i,j), env)"
2.742 +
2.743 +theorem formula_N_reflection:
2.744 +     "REFLECTS[\<lambda>x. is_formula_N(L, f(x), g(x)),
2.745 +               \<lambda>i x. is_formula_N(**Lset(i), f(x), g(x))]"
2.746 +apply (simp only: is_formula_N_def setclass_simps)
2.747 +apply (intro FOL_reflections function_reflections is_wfrec_reflection
2.748 +             iterates_MH_reflection formula_functor_reflection)
2.749 +done
2.750 +
2.751 +
2.752 +
2.753 +subsubsection{*The Predicate ``Is A Formula''*}
2.754 +
2.755 +(*  mem_formula(M,p) ==
2.756 +      \<exists>n[M]. \<exists>formn[M].
2.757 +       finite_ordinal(M,n) & is_formula_N(M,n,formn) & p \<in> formn *)
2.758 +constdefs mem_formula_fm :: "i=>i"
2.759 +    "mem_formula_fm(x) ==
2.760 +       Exists(Exists(
2.761 +         And(finite_ordinal_fm(1),
2.762 +           And(formula_N_fm(1,0), Member(x#+2,0)))))"
2.763 +
2.764 +lemma mem_formula_type [TC]:
2.765 +     "x \<in> nat ==> mem_formula_fm(x) \<in> formula"
2.767 +
2.768 +lemma sats_mem_formula_fm [simp]:
2.769 +   "[| x \<in> nat; env \<in> list(A)|]
2.770 +    ==> sats(A, mem_formula_fm(x), env) <-> mem_formula(**A, nth(x,env))"
2.771 +by (simp add: mem_formula_fm_def mem_formula_def)
2.772 +
2.773 +lemma mem_formula_iff_sats:
2.774 +      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
2.775 +       ==> mem_formula(**A, x) <-> sats(A, mem_formula_fm(i), env)"
2.776 +by simp
2.777 +
2.778 +theorem mem_formula_reflection:
2.779 +     "REFLECTS[\<lambda>x. mem_formula(L,f(x)),
2.780 +               \<lambda>i x. mem_formula(**Lset(i),f(x))]"
2.781 +apply (simp only: mem_formula_def setclass_simps)
2.782 +apply (intro FOL_reflections finite_ordinal_reflection formula_N_reflection)
2.783 +done
2.784 +
2.785 +
2.786 +
2.787 +subsubsection{*The Predicate ``Is @{term "formula"}''*}
2.788 +
2.789 +(* is_formula(M,Z) == \<forall>p[M]. p \<in> Z <-> mem_formula(M,p) *)
2.790 +constdefs is_formula_fm :: "i=>i"
2.791 +    "is_formula_fm(Z) == Forall(Iff(Member(0,succ(Z)), mem_formula_fm(0)))"
2.792 +
2.793 +lemma is_formula_type [TC]:
2.794 +     "x \<in> nat ==> is_formula_fm(x) \<in> formula"
2.796 +
2.797 +lemma sats_is_formula_fm [simp]:
2.798 +   "[| x \<in> nat; env \<in> list(A)|]
2.799 +    ==> sats(A, is_formula_fm(x), env) <-> is_formula(**A, nth(x,env))"
2.800 +by (simp add: is_formula_fm_def is_formula_def)
2.801 +
2.802 +lemma is_formula_iff_sats:
2.803 +      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
2.804 +       ==> is_formula(**A, x) <-> sats(A, is_formula_fm(i), env)"
2.805 +by simp
2.806 +
2.807 +theorem is_formula_reflection:
2.808 +     "REFLECTS[\<lambda>x. is_formula(L,f(x)),
2.809 +               \<lambda>i x. is_formula(**Lset(i),f(x))]"
2.810 +apply (simp only: is_formula_def setclass_simps)
2.811 +apply (intro FOL_reflections mem_formula_reflection)
2.812 +done
2.813 +
2.814 +
2.815 +subsubsection{*The Operator @{term is_transrec}*}
2.816 +
2.817 +text{*The three arguments of @{term p} are always 2, 1, 0.  It is buried
2.818 +   within eight quantifiers!
2.819 +   We call @{term p} with arguments a, f, z by equating them with
2.820 +  the corresponding quantified variables with de Bruijn indices 2, 1, 0.*}
2.821 +
2.822 +(* is_transrec :: "[i=>o, [i,i,i]=>o, i, i] => o"
2.823 +   "is_transrec(M,MH,a,z) ==
2.824 +      \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M].
2.825 +       2       1         0
2.826 +       upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
2.827 +       is_wfrec(M,MH,mesa,a,z)" *)
2.828 +constdefs is_transrec_fm :: "[i, i, i]=>i"
2.829 + "is_transrec_fm(p,a,z) ==
2.830 +    Exists(Exists(Exists(
2.831 +      And(upair_fm(a#+3,a#+3,2),
2.832 +       And(is_eclose_fm(2,1),
2.833 +        And(Memrel_fm(1,0), is_wfrec_fm(p,0,a#+3,z#+3)))))))"
2.834 +
2.835 +
2.836 +lemma is_transrec_type [TC]:
2.837 +     "[| p \<in> formula; x \<in> nat; z \<in> nat |]
2.838 +      ==> is_transrec_fm(p,x,z) \<in> formula"
2.840 +
2.841 +lemma sats_is_transrec_fm:
2.842 +  assumes MH_iff_sats:
2.843 +      "!!a0 a1 a2 a3 a4 a5 a6 a7.
2.844 +        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A|]
2.845 +        ==> MH(a2, a1, a0) <->
2.846 +            sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,
2.847 +                          Cons(a4,Cons(a5,Cons(a6,Cons(a7,env)))))))))"
2.848 +  shows
2.849 +      "[|x < length(env); z < length(env); env \<in> list(A)|]
2.850 +       ==> sats(A, is_transrec_fm(p,x,z), env) <->
2.851 +           is_transrec(**A, MH, nth(x,env), nth(z,env))"
2.852 +apply (frule_tac x=z in lt_length_in_nat, assumption)
2.853 +apply (frule_tac x=x in lt_length_in_nat, assumption)
2.854 +apply (simp add: is_transrec_fm_def sats_is_wfrec_fm is_transrec_def MH_iff_sats [THEN iff_sym])
2.855 +done
2.856 +
2.857 +
2.858 +lemma is_transrec_iff_sats:
2.859 +  assumes MH_iff_sats:
2.860 +      "!!a0 a1 a2 a3 a4 a5 a6 a7.
2.861 +        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A|]
2.862 +        ==> MH(a2, a1, a0) <->
2.863 +            sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,
2.864 +                          Cons(a4,Cons(a5,Cons(a6,Cons(a7,env)))))))))"
2.865 +  shows
2.866 +  "[|nth(i,env) = x; nth(k,env) = z;
2.867 +      i < length(env); k < length(env); env \<in> list(A)|]
2.868 +   ==> is_transrec(**A, MH, x, z) <-> sats(A, is_transrec_fm(p,i,k), env)"
2.869 +by (simp add: sats_is_transrec_fm [OF MH_iff_sats])
2.870 +
2.871 +theorem is_transrec_reflection:
2.872 +  assumes MH_reflection:
2.873 +    "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)),
2.874 +                     \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
2.875 +  shows "REFLECTS[\<lambda>x. is_transrec(L, MH(L,x), f(x), h(x)),
2.876 +               \<lambda>i x. is_transrec(**Lset(i), MH(**Lset(i),x), f(x), h(x))]"
2.877 +apply (simp (no_asm_use) only: is_transrec_def setclass_simps)
2.878 +apply (intro FOL_reflections function_reflections MH_reflection
2.879 +             is_wfrec_reflection is_eclose_reflection)
2.880 +done
2.881 +
2.882  end
```
```     3.1 --- a/src/ZF/Constructible/ROOT.ML	Wed Aug 14 14:33:26 2002 +0200
3.2 +++ b/src/ZF/Constructible/ROOT.ML	Thu Aug 15 21:36:26 2002 +0200
3.3 @@ -8,4 +8,4 @@
3.4  Build using	isatool usedir  -d pdf ZF Constructible
3.5  *)
3.6
3.7 -use_thy "Satisfies_absolute";
3.8 +use_thy "DPow_absolute";
```
```     4.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Wed Aug 14 14:33:26 2002 +0200
4.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Aug 15 21:36:26 2002 +0200
4.3 @@ -234,151 +234,6 @@
4.4  declare trancl_abs [simp]
4.5
4.6
4.7 -subsection{*Well-Founded Recursion!*}
4.8 -
4.9 -
4.10 -text{*Alternative definition, minimizing nesting of quantifiers around MH*}
4.11 -lemma M_is_recfun_iff:
4.12 -   "M_is_recfun(M,MH,r,a,f) <->
4.13 -    (\<forall>z[M]. z \<in> f <->
4.14 -     (\<exists>x[M]. \<exists>f_r_sx[M]. \<exists>y[M].
4.15 -             MH(x, f_r_sx, y) & pair(M,x,y,z) &
4.16 -             (\<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M].
4.17 -                pair(M,x,a,xa) & upair(M,x,x,sx) &
4.18 -               pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
4.19 -               xa \<in> r)))"
4.21 -apply (rule rall_cong, blast)
4.22 -done
4.23 -
4.24 -
4.25 -(* M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
4.26 -   "M_is_recfun(M,MH,r,a,f) ==
4.27 -     \<forall>z[M]. z \<in> f <->
4.28 -               2      1           0
4.29 -new def     (\<exists>x[M]. \<exists>f_r_sx[M]. \<exists>y[M].
4.30 -             MH(x, f_r_sx, y) & pair(M,x,y,z) &
4.31 -             (\<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M].
4.32 -                pair(M,x,a,xa) & upair(M,x,x,sx) &
4.33 -               pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
4.34 -               xa \<in> r)"
4.35 -*)
4.36 -
4.37 -text{*The three arguments of @{term p} are always 2, 1, 0 and z*}
4.38 -constdefs is_recfun_fm :: "[i, i, i, i]=>i"
4.39 - "is_recfun_fm(p,r,a,f) ==
4.40 -   Forall(Iff(Member(0,succ(f)),
4.41 -    Exists(Exists(Exists(
4.42 -     And(p,
4.43 -      And(pair_fm(2,0,3),
4.44 -       Exists(Exists(Exists(
4.45 -	And(pair_fm(5,a#+7,2),
4.46 -	 And(upair_fm(5,5,1),
4.47 -	  And(pre_image_fm(r#+7,1,0),
4.48 -	   And(restriction_fm(f#+7,0,4), Member(2,r#+7)))))))))))))))"
4.49 -
4.50 -lemma is_recfun_type [TC]:
4.51 -     "[| p \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |]
4.52 -      ==> is_recfun_fm(p,x,y,z) \<in> formula"
4.54 -
4.55 -
4.56 -lemma sats_is_recfun_fm:
4.57 -  assumes MH_iff_sats:
4.58 -      "!!a0 a1 a2 a3.
4.59 -        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A|]
4.60 -        ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,env)))))"
4.61 -  shows
4.62 -      "[|x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
4.63 -       ==> sats(A, is_recfun_fm(p,x,y,z), env) <->
4.64 -           M_is_recfun(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
4.65 -by (simp add: is_recfun_fm_def M_is_recfun_iff MH_iff_sats [THEN iff_sym])
4.66 -
4.67 -lemma is_recfun_iff_sats:
4.68 -  assumes MH_iff_sats:
4.69 -      "!!a0 a1 a2 a3.
4.70 -        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A|]
4.71 -        ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,env)))))"
4.72 -  shows
4.73 -  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
4.74 -      i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
4.75 -   ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)"
4.76 -by (simp add: sats_is_recfun_fm [OF MH_iff_sats])
4.77 -
4.78 -text{*The additional variable in the premise, namely @{term f'}, is essential.
4.79 -It lets @{term MH} depend upon @{term x}, which seems often necessary.
4.80 -The same thing occurs in @{text is_wfrec_reflection}.*}
4.81 -theorem is_recfun_reflection:
4.82 -  assumes MH_reflection:
4.83 -    "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)),
4.84 -                     \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
4.85 -  shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L,x), f(x), g(x), h(x)),
4.86 -             \<lambda>i x. M_is_recfun(**Lset(i), MH(**Lset(i),x), f(x), g(x), h(x))]"
4.87 -apply (simp (no_asm_use) only: M_is_recfun_def setclass_simps)
4.88 -apply (intro FOL_reflections function_reflections
4.89 -             restriction_reflection MH_reflection)
4.90 -done
4.91 -
4.92 -subsubsection{*The Operator @{term is_wfrec}*}
4.93 -
4.94 -text{*The three arguments of @{term p} are always 2, 1, 0*}
4.95 -
4.96 -(* is_wfrec :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
4.97 -    "is_wfrec(M,MH,r,a,z) ==
4.98 -      \<exists>f[M]. M_is_recfun(M,MH,r,a,f) & MH(a,f,z)" *)
4.99 -constdefs is_wfrec_fm :: "[i, i, i, i]=>i"
4.100 - "is_wfrec_fm(p,r,a,z) ==
4.101 -    Exists(And(is_recfun_fm(p, succ(r), succ(a), 0),
4.102 -           Exists(Exists(Exists(Exists(
4.103 -             And(Equal(2,a#+5), And(Equal(1,4), And(Equal(0,z#+5), p)))))))))"
4.104 -
4.105 -text{*We call @{term p} with arguments a, f, z by equating them with
4.106 -  the corresponding quantified variables with de Bruijn indices 2, 1, 0.*}
4.107 -
4.108 -text{*There's an additional existential quantifier to ensure that the
4.109 -      environments in both calls to MH have the same length.*}
4.110 -
4.111 -lemma is_wfrec_type [TC]:
4.112 -     "[| p \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |]
4.113 -      ==> is_wfrec_fm(p,x,y,z) \<in> formula"
4.115 -
4.116 -lemma sats_is_wfrec_fm:
4.117 -  assumes MH_iff_sats:
4.118 -      "!!a0 a1 a2 a3 a4.
4.119 -        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A|]
4.120 -        ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
4.121 -  shows
4.122 -      "[|x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
4.123 -       ==> sats(A, is_wfrec_fm(p,x,y,z), env) <->
4.124 -           is_wfrec(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
4.125 -apply (frule_tac x=z in lt_length_in_nat, assumption)
4.126 -apply (frule lt_length_in_nat, assumption)
4.127 -apply (simp add: is_wfrec_fm_def sats_is_recfun_fm is_wfrec_def MH_iff_sats [THEN iff_sym], blast)
4.128 -done
4.129 -
4.130 -
4.131 -lemma is_wfrec_iff_sats:
4.132 -  assumes MH_iff_sats:
4.133 -      "!!a0 a1 a2 a3 a4.
4.134 -        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A|]
4.135 -        ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
4.136 -  shows
4.137 -  "[|nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
4.138 -      i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
4.139 -   ==> is_wfrec(**A, MH, x, y, z) <-> sats(A, is_wfrec_fm(p,i,j,k), env)"
4.140 -by (simp add: sats_is_wfrec_fm [OF MH_iff_sats])
4.141 -
4.142 -theorem is_wfrec_reflection:
4.143 -  assumes MH_reflection:
4.144 -    "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)),
4.145 -                     \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
4.146 -  shows "REFLECTS[\<lambda>x. is_wfrec(L, MH(L,x), f(x), g(x), h(x)),
4.147 -               \<lambda>i x. is_wfrec(**Lset(i), MH(**Lset(i),x), f(x), g(x), h(x))]"
4.148 -apply (simp (no_asm_use) only: is_wfrec_def setclass_simps)
4.149 -apply (intro FOL_reflections MH_reflection is_recfun_reflection)
4.150 -done
4.151 -
4.152  subsection{*The Locale @{text "M_wfrank"}*}
4.153
4.154  subsubsection{*Separation for @{term "wfrank"}*}
4.155 @@ -531,297 +386,8 @@
4.156  declare wf_on_abs [simp]
4.157
4.158
4.159 -subsection{*For Datatypes*}
4.160 -
4.161 -subsubsection{*Binary Products, Internalized*}
4.162 -
4.163 -constdefs cartprod_fm :: "[i,i,i]=>i"
4.164 -(* "cartprod(M,A,B,z) ==
4.165 -        \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))" *)
4.166 -    "cartprod_fm(A,B,z) ==
4.167 -       Forall(Iff(Member(0,succ(z)),
4.168 -                  Exists(And(Member(0,succ(succ(A))),
4.169 -                         Exists(And(Member(0,succ(succ(succ(B)))),
4.170 -                                    pair_fm(1,0,2)))))))"
4.171 -
4.172 -lemma cartprod_type [TC]:
4.173 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> cartprod_fm(x,y,z) \<in> formula"
4.175 -
4.176 -lemma arity_cartprod_fm [simp]:
4.177 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
4.178 -      ==> arity(cartprod_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
4.179 -by (simp add: cartprod_fm_def succ_Un_distrib [symmetric] Un_ac)
4.180 -
4.181 -lemma sats_cartprod_fm [simp]:
4.182 -   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
4.183 -    ==> sats(A, cartprod_fm(x,y,z), env) <->
4.184 -        cartprod(**A, nth(x,env), nth(y,env), nth(z,env))"
4.185 -by (simp add: cartprod_fm_def cartprod_def)
4.186 -
4.187 -lemma cartprod_iff_sats:
4.188 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
4.189 -          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
4.190 -       ==> cartprod(**A, x, y, z) <-> sats(A, cartprod_fm(i,j,k), env)"
4.192 -
4.193 -theorem cartprod_reflection:
4.194 -     "REFLECTS[\<lambda>x. cartprod(L,f(x),g(x),h(x)),
4.195 -               \<lambda>i x. cartprod(**Lset(i),f(x),g(x),h(x))]"
4.196 -apply (simp only: cartprod_def setclass_simps)
4.197 -apply (intro FOL_reflections pair_reflection)
4.198 -done
4.199 -
4.200 -
4.201 -subsubsection{*Binary Sums, Internalized*}
4.202 -
4.203 -(* "is_sum(M,A,B,Z) ==
4.204 -       \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M].
4.205 -         3      2       1        0
4.206 -       number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
4.207 -       cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"  *)
4.208 -constdefs sum_fm :: "[i,i,i]=>i"
4.209 -    "sum_fm(A,B,Z) ==
4.210 -       Exists(Exists(Exists(Exists(
4.211 -        And(number1_fm(2),
4.212 -            And(cartprod_fm(2,A#+4,3),
4.213 -                And(upair_fm(2,2,1),
4.214 -                    And(cartprod_fm(1,B#+4,0), union_fm(3,0,Z#+4)))))))))"
4.215 -
4.216 -lemma sum_type [TC]:
4.217 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> sum_fm(x,y,z) \<in> formula"
4.219 -
4.220 -lemma arity_sum_fm [simp]:
4.221 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
4.222 -      ==> arity(sum_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
4.223 -by (simp add: sum_fm_def succ_Un_distrib [symmetric] Un_ac)
4.224 -
4.225 -lemma sats_sum_fm [simp]:
4.226 -   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
4.227 -    ==> sats(A, sum_fm(x,y,z), env) <->
4.228 -        is_sum(**A, nth(x,env), nth(y,env), nth(z,env))"
4.229 -by (simp add: sum_fm_def is_sum_def)
4.230 -
4.231 -lemma sum_iff_sats:
4.232 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
4.233 -          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
4.234 -       ==> is_sum(**A, x, y, z) <-> sats(A, sum_fm(i,j,k), env)"
4.235 -by simp
4.236 -
4.237 -theorem sum_reflection:
4.238 -     "REFLECTS[\<lambda>x. is_sum(L,f(x),g(x),h(x)),
4.239 -               \<lambda>i x. is_sum(**Lset(i),f(x),g(x),h(x))]"
4.240 -apply (simp only: is_sum_def setclass_simps)
4.241 -apply (intro FOL_reflections function_reflections cartprod_reflection)
4.242 -done
4.243 -
4.244 -
4.245 -subsubsection{*The Operator @{term quasinat}*}
4.246 -
4.247 -(* "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))" *)
4.248 -constdefs quasinat_fm :: "i=>i"
4.249 -    "quasinat_fm(z) == Or(empty_fm(z), Exists(succ_fm(0,succ(z))))"
4.250 -
4.251 -lemma quasinat_type [TC]:
4.252 -     "x \<in> nat ==> quasinat_fm(x) \<in> formula"
4.254 -
4.255 -lemma arity_quasinat_fm [simp]:
4.256 -     "x \<in> nat ==> arity(quasinat_fm(x)) = succ(x)"
4.257 -by (simp add: quasinat_fm_def succ_Un_distrib [symmetric] Un_ac)
4.258 -
4.259 -lemma sats_quasinat_fm [simp]:
4.260 -   "[| x \<in> nat; env \<in> list(A)|]
4.261 -    ==> sats(A, quasinat_fm(x), env) <-> is_quasinat(**A, nth(x,env))"
4.262 -by (simp add: quasinat_fm_def is_quasinat_def)
4.263 -
4.264 -lemma quasinat_iff_sats:
4.265 -      "[| nth(i,env) = x; nth(j,env) = y;
4.266 -          i \<in> nat; env \<in> list(A)|]
4.267 -       ==> is_quasinat(**A, x) <-> sats(A, quasinat_fm(i), env)"
4.268 -by simp
4.269 -
4.270 -theorem quasinat_reflection:
4.271 -     "REFLECTS[\<lambda>x. is_quasinat(L,f(x)),
4.272 -               \<lambda>i x. is_quasinat(**Lset(i),f(x))]"
4.273 -apply (simp only: is_quasinat_def setclass_simps)
4.274 -apply (intro FOL_reflections function_reflections)
4.275 -done
4.276 -
4.277 -
4.278 -subsubsection{*The Operator @{term is_nat_case}*}
4.279 -text{*I could not get it to work with the more natural assumption that
4.280 - @{term is_b} takes two arguments.  Instead it must be a formula where 1 and 0
4.281 - stand for @{term m} and @{term b}, respectively.*}
4.282 -
4.283 -(* is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o"
4.284 -    "is_nat_case(M, a, is_b, k, z) ==
4.285 -       (empty(M,k) --> z=a) &
4.286 -       (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
4.287 -       (is_quasinat(M,k) | empty(M,z))" *)
4.288 -text{*The formula @{term is_b} has free variables 1 and 0.*}
4.289 -constdefs is_nat_case_fm :: "[i, i, i, i]=>i"
4.290 - "is_nat_case_fm(a,is_b,k,z) ==
4.291 -    And(Implies(empty_fm(k), Equal(z,a)),
4.292 -        And(Forall(Implies(succ_fm(0,succ(k)),
4.293 -                   Forall(Implies(Equal(0,succ(succ(z))), is_b)))),
4.294 -            Or(quasinat_fm(k), empty_fm(z))))"
4.295 -
4.296 -lemma is_nat_case_type [TC]:
4.297 -     "[| is_b \<in> formula;
4.298 -         x \<in> nat; y \<in> nat; z \<in> nat |]
4.299 -      ==> is_nat_case_fm(x,is_b,y,z) \<in> formula"
4.301 -
4.302 -lemma sats_is_nat_case_fm:
4.303 -  assumes is_b_iff_sats:
4.304 -      "!!a. a \<in> A ==> is_b(a,nth(z, env)) <->
4.305 -                      sats(A, p, Cons(nth(z,env), Cons(a, env)))"
4.306 -  shows
4.307 -      "[|x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
4.308 -       ==> sats(A, is_nat_case_fm(x,p,y,z), env) <->
4.309 -           is_nat_case(**A, nth(x,env), is_b, nth(y,env), nth(z,env))"
4.310 -apply (frule lt_length_in_nat, assumption)
4.311 -apply (simp add: is_nat_case_fm_def is_nat_case_def is_b_iff_sats [THEN iff_sym])
4.312 -done
4.313 -
4.314 -lemma is_nat_case_iff_sats:
4.315 -  "[| (!!a. a \<in> A ==> is_b(a,z) <->
4.316 -                      sats(A, p, Cons(z, Cons(a,env))));
4.317 -      nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
4.318 -      i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
4.319 -   ==> is_nat_case(**A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)"
4.320 -by (simp add: sats_is_nat_case_fm [of A is_b])
4.321 -
4.322 -
4.323 -text{*The second argument of @{term is_b} gives it direct access to @{term x},
4.324 -  which is essential for handling free variable references.  Without this
4.325 -  argument, we cannot prove reflection for @{term iterates_MH}.*}
4.326 -theorem is_nat_case_reflection:
4.327 -  assumes is_b_reflection:
4.328 -    "!!h f g. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x)),
4.329 -                     \<lambda>i x. is_b(**Lset(i), h(x), f(x), g(x))]"
4.330 -  shows "REFLECTS[\<lambda>x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)),
4.331 -               \<lambda>i x. is_nat_case(**Lset(i), f(x), is_b(**Lset(i), x), g(x), h(x))]"
4.332 -apply (simp (no_asm_use) only: is_nat_case_def setclass_simps)
4.333 -apply (intro FOL_reflections function_reflections
4.334 -             restriction_reflection is_b_reflection quasinat_reflection)
4.335 -done
4.336 -
4.337 -
4.338 -
4.339 -subsection{*The Operator @{term iterates_MH}, Needed for Iteration*}
4.340 -
4.341 -(*  iterates_MH :: "[i=>o, [i,i]=>o, i, i, i, i] => o"
4.342 -   "iterates_MH(M,isF,v,n,g,z) ==
4.343 -        is_nat_case(M, v, \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & isF(gm,u),
4.344 -                    n, z)" *)
4.345 -constdefs iterates_MH_fm :: "[i, i, i, i, i]=>i"
4.346 - "iterates_MH_fm(isF,v,n,g,z) ==
4.347 -    is_nat_case_fm(v,
4.348 -      Exists(And(fun_apply_fm(succ(succ(succ(g))),2,0),
4.349 -                     Forall(Implies(Equal(0,2), isF)))),
4.350 -      n, z)"
4.351 -
4.352 -lemma iterates_MH_type [TC]:
4.353 -     "[| p \<in> formula;
4.354 -         v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
4.355 -      ==> iterates_MH_fm(p,v,x,y,z) \<in> formula"
4.357 -
4.358 -lemma sats_iterates_MH_fm:
4.359 -  assumes is_F_iff_sats:
4.360 -      "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
4.361 -              ==> is_F(a,b) <->
4.362 -                  sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env)))))"
4.363 -  shows
4.364 -      "[|v \<in> nat; x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
4.365 -       ==> sats(A, iterates_MH_fm(p,v,x,y,z), env) <->
4.366 -           iterates_MH(**A, is_F, nth(v,env), nth(x,env), nth(y,env), nth(z,env))"
4.367 -apply (frule lt_length_in_nat, assumption)
4.368 -apply (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm
4.369 -              is_F_iff_sats [symmetric])
4.370 -apply (rule is_nat_case_cong)
4.372 -done
4.373 -
4.374 -lemma iterates_MH_iff_sats:
4.375 -  assumes is_F_iff_sats:
4.376 -      "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
4.377 -              ==> is_F(a,b) <->
4.378 -                  sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env)))))"
4.379 -  shows
4.380 -  "[| nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
4.381 -      i' \<in> nat; i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
4.382 -   ==> iterates_MH(**A, is_F, v, x, y, z) <->
4.383 -       sats(A, iterates_MH_fm(p,i',i,j,k), env)"
4.384 -by (simp add: sats_iterates_MH_fm [OF is_F_iff_sats])
4.385 -
4.386 -text{*The second argument of @{term p} gives it direct access to @{term x},
4.387 -  which is essential for handling free variable references.  Without this
4.388 -  argument, we cannot prove reflection for @{term list_N}.*}
4.389 -theorem iterates_MH_reflection:
4.390 -  assumes p_reflection:
4.391 -    "!!f g h. REFLECTS[\<lambda>x. p(L, h(x), f(x), g(x)),
4.392 -                     \<lambda>i x. p(**Lset(i), h(x), f(x), g(x))]"
4.393 - shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L,x), e(x), f(x), g(x), h(x)),
4.394 -               \<lambda>i x. iterates_MH(**Lset(i), p(**Lset(i),x), e(x), f(x), g(x), h(x))]"
4.395 -apply (simp (no_asm_use) only: iterates_MH_def)
4.396 -txt{*Must be careful: simplifying with @{text setclass_simps} above would
4.397 -     change @{text "\<exists>gm[**Lset(i)]"} into @{text "\<exists>gm \<in> Lset(i)"}, when
4.398 -     it would no longer match rule @{text is_nat_case_reflection}. *}
4.399 -apply (rule is_nat_case_reflection)
4.400 -apply (simp (no_asm_use) only: setclass_simps)
4.401 -apply (intro FOL_reflections function_reflections is_nat_case_reflection
4.402 -             restriction_reflection p_reflection)
4.403 -done
4.404 -
4.405 -
4.406 -
4.407  subsection{*@{term L} is Closed Under the Operator @{term list}*}
4.408
4.409 -subsubsection{*The List Functor, Internalized*}
4.410 -
4.411 -constdefs list_functor_fm :: "[i,i,i]=>i"
4.412 -(* "is_list_functor(M,A,X,Z) ==
4.413 -        \<exists>n1[M]. \<exists>AX[M].
4.414 -         number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)" *)
4.415 -    "list_functor_fm(A,X,Z) ==
4.416 -       Exists(Exists(
4.417 -        And(number1_fm(1),
4.418 -            And(cartprod_fm(A#+2,X#+2,0), sum_fm(1,0,Z#+2)))))"
4.419 -
4.420 -lemma list_functor_type [TC]:
4.421 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> list_functor_fm(x,y,z) \<in> formula"
4.423 -
4.424 -lemma arity_list_functor_fm [simp]:
4.425 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
4.426 -      ==> arity(list_functor_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
4.427 -by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac)
4.428 -
4.429 -lemma sats_list_functor_fm [simp]:
4.430 -   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
4.431 -    ==> sats(A, list_functor_fm(x,y,z), env) <->
4.432 -        is_list_functor(**A, nth(x,env), nth(y,env), nth(z,env))"
4.433 -by (simp add: list_functor_fm_def is_list_functor_def)
4.434 -
4.435 -lemma list_functor_iff_sats:
4.436 -  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
4.437 -      i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
4.438 -   ==> is_list_functor(**A, x, y, z) <-> sats(A, list_functor_fm(i,j,k), env)"
4.439 -by simp
4.440 -
4.441 -theorem list_functor_reflection:
4.442 -     "REFLECTS[\<lambda>x. is_list_functor(L,f(x),g(x),h(x)),
4.443 -               \<lambda>i x. is_list_functor(**Lset(i),f(x),g(x),h(x))]"
4.444 -apply (simp only: is_list_functor_def setclass_simps)
4.445 -apply (intro FOL_reflections number1_reflection
4.446 -             cartprod_reflection sum_reflection)
4.447 -done
4.448 -
4.449 -
4.450  subsubsection{*Instances of Replacement for Lists*}
4.451
4.452  lemma list_replacement1_Reflects:
4.453 @@ -904,48 +470,6 @@
4.454
4.455  subsection{*@{term L} is Closed Under the Operator @{term formula}*}
4.456
4.457 -subsubsection{*The Formula Functor, Internalized*}
4.458 -
4.459 -constdefs formula_functor_fm :: "[i,i]=>i"
4.460 -(*     "is_formula_functor(M,X,Z) ==
4.461 -        \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M].
4.462 -           4           3               2       1       0
4.463 -          omega(M,nat') & cartprod(M,nat',nat',natnat) &
4.464 -          is_sum(M,natnat,natnat,natnatsum) &
4.465 -          cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) &
4.466 -          is_sum(M,natnatsum,X3,Z)" *)
4.467 -    "formula_functor_fm(X,Z) ==
4.468 -       Exists(Exists(Exists(Exists(Exists(
4.469 -        And(omega_fm(4),
4.470 -         And(cartprod_fm(4,4,3),
4.471 -          And(sum_fm(3,3,2),
4.472 -           And(cartprod_fm(X#+5,X#+5,1),
4.473 -            And(sum_fm(1,X#+5,0), sum_fm(2,0,Z#+5)))))))))))"
4.474 -
4.475 -lemma formula_functor_type [TC]:
4.476 -     "[| x \<in> nat; y \<in> nat |] ==> formula_functor_fm(x,y) \<in> formula"
4.478 -
4.479 -lemma sats_formula_functor_fm [simp]:
4.480 -   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
4.481 -    ==> sats(A, formula_functor_fm(x,y), env) <->
4.482 -        is_formula_functor(**A, nth(x,env), nth(y,env))"
4.483 -by (simp add: formula_functor_fm_def is_formula_functor_def)
4.484 -
4.485 -lemma formula_functor_iff_sats:
4.486 -  "[| nth(i,env) = x; nth(j,env) = y;
4.487 -      i \<in> nat; j \<in> nat; env \<in> list(A)|]
4.488 -   ==> is_formula_functor(**A, x, y) <-> sats(A, formula_functor_fm(i,j), env)"
4.489 -by simp
4.490 -
4.491 -theorem formula_functor_reflection:
4.492 -     "REFLECTS[\<lambda>x. is_formula_functor(L,f(x),g(x)),
4.493 -               \<lambda>i x. is_formula_functor(**Lset(i),f(x),g(x))]"
4.494 -apply (simp only: is_formula_functor_def setclass_simps)
4.495 -apply (intro FOL_reflections omega_reflection
4.496 -             cartprod_reflection sum_reflection)
4.497 -done
4.498 -
4.499  subsubsection{*Instances of Replacement for Formulas*}
4.500
4.501  lemma formula_replacement1_Reflects:
```
```     5.1 --- a/src/ZF/Constructible/Satisfies_absolute.thy	Wed Aug 14 14:33:26 2002 +0200
5.2 +++ b/src/ZF/Constructible/Satisfies_absolute.thy	Thu Aug 15 21:36:26 2002 +0200
5.3 @@ -10,226 +10,6 @@
5.4
5.5
5.6
5.7 -subsubsection{*The Formula @{term is_list_N}, Internalized*}
5.8 -
5.9 -(* "is_list_N(M,A,n,Z) ==
5.10 -      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M].
5.11 -       empty(M,zero) &
5.12 -       successor(M,n,sn) & membership(M,sn,msn) &
5.13 -       is_wfrec(M, iterates_MH(M, is_list_functor(M,A),zero), msn, n, Z)" *)
5.14 -
5.15 -constdefs list_N_fm :: "[i,i,i]=>i"
5.16 -  "list_N_fm(A,n,Z) ==
5.17 -     Exists(Exists(Exists(
5.18 -       And(empty_fm(2),
5.19 -         And(succ_fm(n#+3,1),
5.20 -          And(Memrel_fm(1,0),
5.21 -              is_wfrec_fm(iterates_MH_fm(list_functor_fm(A#+9#+3,1,0),
5.22 -                                         7,2,1,0),
5.23 -                           0, n#+3, Z#+3)))))))"
5.24 -
5.25 -lemma list_N_fm_type [TC]:
5.26 - "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> list_N_fm(x,y,z) \<in> formula"
5.28 -
5.29 -lemma sats_list_N_fm [simp]:
5.30 -   "[| x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
5.31 -    ==> sats(A, list_N_fm(x,y,z), env) <->
5.32 -        is_list_N(**A, nth(x,env), nth(y,env), nth(z,env))"
5.33 -apply (frule_tac x=z in lt_length_in_nat, assumption)
5.34 -apply (frule_tac x=y in lt_length_in_nat, assumption)
5.35 -apply (simp add: list_N_fm_def is_list_N_def sats_is_wfrec_fm
5.36 -                 sats_iterates_MH_fm)
5.37 -done
5.38 -
5.39 -lemma list_N_iff_sats:
5.40 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
5.41 -          i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
5.42 -       ==> is_list_N(**A, x, y, z) <-> sats(A, list_N_fm(i,j,k), env)"
5.44 -
5.45 -theorem list_N_reflection:
5.46 -     "REFLECTS[\<lambda>x. is_list_N(L, f(x), g(x), h(x)),
5.47 -               \<lambda>i x. is_list_N(**Lset(i), f(x), g(x), h(x))]"
5.48 -apply (simp only: is_list_N_def setclass_simps)
5.49 -apply (intro FOL_reflections function_reflections is_wfrec_reflection
5.50 -             iterates_MH_reflection list_functor_reflection)
5.51 -done
5.52 -
5.53 -
5.54 -
5.55 -subsubsection{*The Predicate ``Is A List''*}
5.56 -
5.57 -(* mem_list(M,A,l) ==
5.58 -      \<exists>n[M]. \<exists>listn[M].
5.59 -       finite_ordinal(M,n) & is_list_N(M,A,n,listn) & l \<in> listn *)
5.60 -constdefs mem_list_fm :: "[i,i]=>i"
5.61 -    "mem_list_fm(x,y) ==
5.62 -       Exists(Exists(
5.63 -         And(finite_ordinal_fm(1),
5.64 -           And(list_N_fm(x#+2,1,0), Member(y#+2,0)))))"
5.65 -
5.66 -lemma mem_list_type [TC]:
5.67 -     "[| x \<in> nat; y \<in> nat |] ==> mem_list_fm(x,y) \<in> formula"
5.69 -
5.70 -lemma sats_mem_list_fm [simp]:
5.71 -   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
5.72 -    ==> sats(A, mem_list_fm(x,y), env) <-> mem_list(**A, nth(x,env), nth(y,env))"
5.73 -by (simp add: mem_list_fm_def mem_list_def)
5.74 -
5.75 -lemma mem_list_iff_sats:
5.76 -      "[| nth(i,env) = x; nth(j,env) = y;
5.77 -          i \<in> nat; j \<in> nat; env \<in> list(A)|]
5.78 -       ==> mem_list(**A, x, y) <-> sats(A, mem_list_fm(i,j), env)"
5.79 -by simp
5.80 -
5.81 -theorem mem_list_reflection:
5.82 -     "REFLECTS[\<lambda>x. mem_list(L,f(x),g(x)),
5.83 -               \<lambda>i x. mem_list(**Lset(i),f(x),g(x))]"
5.84 -apply (simp only: mem_list_def setclass_simps)
5.85 -apply (intro FOL_reflections finite_ordinal_reflection list_N_reflection)
5.86 -done
5.87 -
5.88 -
5.89 -subsubsection{*The Predicate ``Is @{term "list(A)"}''*}
5.90 -
5.91 -(* is_list(M,A,Z) == \<forall>l[M]. l \<in> Z <-> mem_list(M,A,l) *)
5.92 -constdefs is_list_fm :: "[i,i]=>i"
5.93 -    "is_list_fm(A,Z) ==
5.94 -       Forall(Iff(Member(0,succ(Z)), mem_list_fm(succ(A),0)))"
5.95 -
5.96 -lemma is_list_type [TC]:
5.97 -     "[| x \<in> nat; y \<in> nat |] ==> is_list_fm(x,y) \<in> formula"
5.99 -
5.100 -lemma sats_is_list_fm [simp]:
5.101 -   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
5.102 -    ==> sats(A, is_list_fm(x,y), env) <-> is_list(**A, nth(x,env), nth(y,env))"
5.103 -by (simp add: is_list_fm_def is_list_def)
5.104 -
5.105 -lemma is_list_iff_sats:
5.106 -      "[| nth(i,env) = x; nth(j,env) = y;
5.107 -          i \<in> nat; j \<in> nat; env \<in> list(A)|]
5.108 -       ==> is_list(**A, x, y) <-> sats(A, is_list_fm(i,j), env)"
5.109 -by simp
5.110 -
5.111 -theorem is_list_reflection:
5.112 -     "REFLECTS[\<lambda>x. is_list(L,f(x),g(x)),
5.113 -               \<lambda>i x. is_list(**Lset(i),f(x),g(x))]"
5.114 -apply (simp only: is_list_def setclass_simps)
5.115 -apply (intro FOL_reflections mem_list_reflection)
5.116 -done
5.117 -
5.118 -
5.119 -subsubsection{*The Formula @{term is_formula_N}, Internalized*}
5.120 -
5.121 -(* "is_formula_N(M,n,Z) ==
5.122 -      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M].
5.123 -          2       1       0
5.124 -       empty(M,zero) &
5.125 -       successor(M,n,sn) & membership(M,sn,msn) &
5.126 -       is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)" *)
5.127 -constdefs formula_N_fm :: "[i,i]=>i"
5.128 -  "formula_N_fm(n,Z) ==
5.129 -     Exists(Exists(Exists(
5.130 -       And(empty_fm(2),
5.131 -         And(succ_fm(n#+3,1),
5.132 -          And(Memrel_fm(1,0),
5.133 -              is_wfrec_fm(iterates_MH_fm(formula_functor_fm(1,0),7,2,1,0),
5.134 -                           0, n#+3, Z#+3)))))))"
5.135 -
5.136 -lemma formula_N_fm_type [TC]:
5.137 - "[| x \<in> nat; y \<in> nat |] ==> formula_N_fm(x,y) \<in> formula"
5.139 -
5.140 -lemma sats_formula_N_fm [simp]:
5.141 -   "[| x < length(env); y < length(env); env \<in> list(A)|]
5.142 -    ==> sats(A, formula_N_fm(x,y), env) <->
5.143 -        is_formula_N(**A, nth(x,env), nth(y,env))"
5.144 -apply (frule_tac x=y in lt_length_in_nat, assumption)
5.145 -apply (frule lt_length_in_nat, assumption)
5.146 -apply (simp add: formula_N_fm_def is_formula_N_def sats_is_wfrec_fm sats_iterates_MH_fm)
5.147 -done
5.148 -
5.149 -lemma formula_N_iff_sats:
5.150 -      "[| nth(i,env) = x; nth(j,env) = y;
5.151 -          i < length(env); j < length(env); env \<in> list(A)|]
5.152 -       ==> is_formula_N(**A, x, y) <-> sats(A, formula_N_fm(i,j), env)"
5.154 -
5.155 -theorem formula_N_reflection:
5.156 -     "REFLECTS[\<lambda>x. is_formula_N(L, f(x), g(x)),
5.157 -               \<lambda>i x. is_formula_N(**Lset(i), f(x), g(x))]"
5.158 -apply (simp only: is_formula_N_def setclass_simps)
5.159 -apply (intro FOL_reflections function_reflections is_wfrec_reflection
5.160 -             iterates_MH_reflection formula_functor_reflection)
5.161 -done
5.162 -
5.163 -
5.164 -
5.165 -subsubsection{*The Predicate ``Is A Formula''*}
5.166 -
5.167 -(*  mem_formula(M,p) ==
5.168 -      \<exists>n[M]. \<exists>formn[M].
5.169 -       finite_ordinal(M,n) & is_formula_N(M,n,formn) & p \<in> formn *)
5.170 -constdefs mem_formula_fm :: "i=>i"
5.171 -    "mem_formula_fm(x) ==
5.172 -       Exists(Exists(
5.173 -         And(finite_ordinal_fm(1),
5.174 -           And(formula_N_fm(1,0), Member(x#+2,0)))))"
5.175 -
5.176 -lemma mem_formula_type [TC]:
5.177 -     "x \<in> nat ==> mem_formula_fm(x) \<in> formula"
5.179 -
5.180 -lemma sats_mem_formula_fm [simp]:
5.181 -   "[| x \<in> nat; env \<in> list(A)|]
5.182 -    ==> sats(A, mem_formula_fm(x), env) <-> mem_formula(**A, nth(x,env))"
5.183 -by (simp add: mem_formula_fm_def mem_formula_def)
5.184 -
5.185 -lemma mem_formula_iff_sats:
5.186 -      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
5.187 -       ==> mem_formula(**A, x) <-> sats(A, mem_formula_fm(i), env)"
5.188 -by simp
5.189 -
5.190 -theorem mem_formula_reflection:
5.191 -     "REFLECTS[\<lambda>x. mem_formula(L,f(x)),
5.192 -               \<lambda>i x. mem_formula(**Lset(i),f(x))]"
5.193 -apply (simp only: mem_formula_def setclass_simps)
5.194 -apply (intro FOL_reflections finite_ordinal_reflection formula_N_reflection)
5.195 -done
5.196 -
5.197 -
5.198 -
5.199 -subsubsection{*The Predicate ``Is @{term "formula"}''*}
5.200 -
5.201 -(* is_formula(M,Z) == \<forall>p[M]. p \<in> Z <-> mem_formula(M,p) *)
5.202 -constdefs is_formula_fm :: "i=>i"
5.203 -    "is_formula_fm(Z) == Forall(Iff(Member(0,succ(Z)), mem_formula_fm(0)))"
5.204 -
5.205 -lemma is_formula_type [TC]:
5.206 -     "x \<in> nat ==> is_formula_fm(x) \<in> formula"
5.208 -
5.209 -lemma sats_is_formula_fm [simp]:
5.210 -   "[| x \<in> nat; env \<in> list(A)|]
5.211 -    ==> sats(A, is_formula_fm(x), env) <-> is_formula(**A, nth(x,env))"
5.212 -by (simp add: is_formula_fm_def is_formula_def)
5.213 -
5.214 -lemma is_formula_iff_sats:
5.215 -      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
5.216 -       ==> is_formula(**A, x) <-> sats(A, is_formula_fm(i), env)"
5.217 -by simp
5.218 -
5.219 -theorem is_formula_reflection:
5.220 -     "REFLECTS[\<lambda>x. is_formula(L,f(x)),
5.221 -               \<lambda>i x. is_formula(**Lset(i),f(x))]"
5.222 -apply (simp only: is_formula_def setclass_simps)
5.223 -apply (intro FOL_reflections mem_formula_reflection)
5.224 -done
5.225 -
5.226 -
5.227  subsubsection{*The Formula @{term is_depth}, Internalized*}
5.228
5.229  (*    "is_depth(M,p,n) ==
5.230 @@ -404,10 +184,10 @@
5.231                  \<lambda>u. d(u, h ` succ(depth(u)) ` u))"
5.232
5.233    is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
5.234 -    --{* predicate to relative the functional @{term formula_rec}*}
5.235 +    --{* predicate to relativize the functional @{term formula_rec}*}
5.236     "is_formula_rec(M,MH,p,z)  ==
5.237 -    \<exists>i[M]. \<exists>f[M]. i = succ(depth(p)) & fun_apply(M,f,p,z) &
5.238 -                  is_transrec(M,MH,i,f)"
5.239 +      \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) &
5.240 +             successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
5.241
5.242  text{*Unfold @{term formula_rec} to @{term formula_rec_case}*}
5.243  lemma (in M_triv_axioms) formula_rec_eq2:
5.244 @@ -503,7 +283,7 @@
5.245    "[| p \<in> formula; M(z)|]
5.246     ==> is_formula_rec(M,MH,p,z) <-> z = formula_rec(a,b,c,d,p)"
5.247  by (simp add: is_formula_rec_def formula_rec_eq2 transM [OF _ formula_closed]
5.248 -              transrec_abs [OF fr_replace MH_rel2]
5.249 +              transrec_abs [OF fr_replace MH_rel2] depth_type
5.250                fr_transrec_closed formula_rec_lam_closed eq_commute)
5.251
5.252
5.253 @@ -598,15 +378,7 @@
5.254                 z)"
5.255
5.256    is_satisfies :: "[i=>o,i,i,i]=>o"
5.257 -   "is_satisfies(M,A) ==
5.258 -      is_formula_rec (M, \<lambda>u f z.
5.259 -        \<forall>fml[M].
5.260 -           is_formula(M,fml) \<longrightarrow>
5.261 -           is_lambda
5.262 -            (M, fml,
5.263 -             is_formula_case
5.264 -              (M, satisfies_is_a(M,A), satisfies_is_b(M,A),
5.265 -               satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)), z))"
5.266 +   "is_satisfies(M,A) == is_formula_rec (M, satisfies_MH(M,A))"
5.267
5.268
5.269  text{*This lemma relates the fragments defined above to the original primitive
5.270 @@ -837,7 +609,7 @@
5.271    "[|M(A); M(z); p \<in> formula|]
5.272     ==> is_satisfies(M,A,p,z) <-> z = satisfies(A,p)"
5.273  by (simp only: M_formula_rec.formula_rec_abs [OF M_formula_rec_M]
5.274 -               satisfies_eq is_satisfies_def)
5.275 +               satisfies_eq is_satisfies_def satisfies_MH_def)
5.276
5.277
5.278  subsection{*Internalizations Needed to Instantiate @{text "M_satisfies"}*}
```
```     6.1 --- a/src/ZF/IsaMakefile	Wed Aug 14 14:33:26 2002 +0200
6.2 +++ b/src/ZF/IsaMakefile	Thu Aug 15 21:36:26 2002 +0200
6.3 @@ -78,7 +78,7 @@
6.4  ZF-Constructible: ZF \$(LOG)/ZF-Constructible.gz
6.5
6.6  \$(LOG)/ZF-Constructible.gz: \$(OUT)/ZF  Constructible/ROOT.ML \
6.7 -  Constructible/Datatype_absolute.thy\
6.8 +  Constructible/Datatype_absolute.thy Constructible/DPow_absolute.thy\
6.9    Constructible/Formula.thy Constructible/Internalize.thy \
6.10    Constructible/Relative.thy \
6.11    Constructible/L_axioms.thy    Constructible/Wellorderings.thy \
```