Relativization and absoluteness for DPow!!
authorpaulson
Thu Aug 15 21:36:26 2002 +0200 (2002-08-15)
changeset 13503d93f41fe35d2
parent 13502 da43ebc02f17
child 13504 59066e97b551
Relativization and absoluteness for DPow!!
src/ZF/Constructible/DPow_absolute.thy
src/ZF/Constructible/Internalize.thy
src/ZF/Constructible/ROOT.ML
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/Satisfies_absolute.thy
src/ZF/IsaMakefile
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Constructible/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.41 +by (simp add: formula_rec_fm_def) 
    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.92 +by (simp add: satisfies_fm_def)
    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.105 +by (simp add: sats_satisfies_fm)
   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.164 +by (simp add: DPow_body_fm_def)
   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.219 +apply (simp add: DPow'_eq)
   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.21 +apply (simp add: M_is_recfun_def)
    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.54 +by (simp add: is_recfun_fm_def)
    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.115 +by (simp add: is_wfrec_fm_def) 
   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.169 +by (simp add: cartprod_fm_def)
   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.186 +by (simp add: sats_cartprod_fm)
   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.213 +by (simp add: sum_fm_def)
   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.248 +by (simp add: quasinat_fm_def)
   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.295 +by (simp add: is_nat_case_fm_def)
   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.350 +by (simp add: iterates_MH_fm_def)
   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.365 +apply (simp_all add: setclass_def)
   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.420 +by (simp add: eclose_n_fm_def)
   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.436 +by (simp add: sats_eclose_n_fm)
   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.460 +by (simp add: mem_eclose_fm_def)
   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.490 +by (simp add: is_eclose_fm_def)
   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.524 +by (simp add: list_functor_fm_def)
   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.572 +by (simp add: list_N_fm_def)
   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.588 +by (simp add: sats_list_N_fm)
   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.613 +by (simp add: mem_list_fm_def)
   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.643 +by (simp add: is_list_fm_def)
   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.684 +by (simp add: formula_functor_fm_def)
   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.726 +by (simp add: formula_N_fm_def)
   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.741 +by (simp add: sats_formula_N_fm)
   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.766 +by (simp add: mem_formula_fm_def)
   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.795 +by (simp add: is_formula_fm_def)
   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.839 +by (simp add: is_transrec_fm_def) 
   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.20 -apply (simp add: M_is_recfun_def)
    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.53 -by (simp add: is_recfun_fm_def)
    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.114 -by (simp add: is_wfrec_fm_def) 
   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.174 -by (simp add: cartprod_fm_def)
   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.191 -by (simp add: sats_cartprod_fm)
   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.218 -by (simp add: sum_fm_def)
   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.253 -by (simp add: quasinat_fm_def)
   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.300 -by (simp add: is_nat_case_fm_def)
   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.356 -by (simp add: iterates_MH_fm_def)
   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.371 -apply (simp_all add: setclass_def)
   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.422 -by (simp add: list_functor_fm_def)
   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.477 -by (simp add: formula_functor_fm_def)
   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.27 -by (simp add: list_N_fm_def)
    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.43 -by (simp add: sats_list_N_fm)
    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.68 -by (simp add: mem_list_fm_def)
    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.98 -by (simp add: is_list_fm_def)
    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.138 -by (simp add: formula_N_fm_def)
   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.153 -by (simp add: sats_formula_N_fm)
   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.178 -by (simp add: mem_formula_fm_def)
   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.207 -by (simp add: is_formula_fm_def)
   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 \