src/ZF/Constructible/Rec_Separation.thy
changeset 13428 99e52e78eb65
parent 13422 af9bc8d87a75
child 13429 2232810416fc
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Sun Jul 28 21:09:37 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Mon Jul 29 00:57:16 2002 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  "M_trancl"}, @{text "M_wfrank"} and @{text "M_datatypes"}*}
     1.5  
     1.6  lemma eq_succ_imp_lt: "[|i = succ(j); Ord(i)|] ==> j<i"
     1.7 -by simp 
     1.8 +by simp
     1.9  
    1.10  subsection{*The Locale @{text "M_trancl"}*}
    1.11  
    1.12 @@ -15,69 +15,69 @@
    1.13  text{*First, The Defining Formula*}
    1.14  
    1.15  (* "rtran_closure_mem(M,A,r,p) ==
    1.16 -      \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M]. 
    1.17 +      \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M].
    1.18         omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
    1.19         (\<exists>f[M]. typed_function(M,n',A,f) &
    1.20 -	(\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
    1.21 -	  fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
    1.22 -	(\<forall>j[M]. j\<in>n --> 
    1.23 -	  (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M]. 
    1.24 -	    fun_apply(M,f,j,fj) & successor(M,j,sj) &
    1.25 -	    fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"*)
    1.26 +        (\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
    1.27 +          fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
    1.28 +        (\<forall>j[M]. j\<in>n -->
    1.29 +          (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M].
    1.30 +            fun_apply(M,f,j,fj) & successor(M,j,sj) &
    1.31 +            fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"*)
    1.32  constdefs rtran_closure_mem_fm :: "[i,i,i]=>i"
    1.33 - "rtran_closure_mem_fm(A,r,p) == 
    1.34 + "rtran_closure_mem_fm(A,r,p) ==
    1.35     Exists(Exists(Exists(
    1.36      And(omega_fm(2),
    1.37       And(Member(1,2),
    1.38        And(succ_fm(1,0),
    1.39         Exists(And(typed_function_fm(1, A#+4, 0),
    1.40 -	And(Exists(Exists(Exists(
    1.41 -	      And(pair_fm(2,1,p#+7), 
    1.42 -	       And(empty_fm(0),
    1.43 -		And(fun_apply_fm(3,0,2), fun_apply_fm(3,5,1))))))),
    1.44 -	    Forall(Implies(Member(0,3),
    1.45 -	     Exists(Exists(Exists(Exists(
    1.46 -	      And(fun_apply_fm(5,4,3),
    1.47 -	       And(succ_fm(4,2),
    1.48 -		And(fun_apply_fm(5,2,1),
    1.49 -		 And(pair_fm(3,1,0), Member(0,r#+9))))))))))))))))))))"
    1.50 +        And(Exists(Exists(Exists(
    1.51 +              And(pair_fm(2,1,p#+7),
    1.52 +               And(empty_fm(0),
    1.53 +                And(fun_apply_fm(3,0,2), fun_apply_fm(3,5,1))))))),
    1.54 +            Forall(Implies(Member(0,3),
    1.55 +             Exists(Exists(Exists(Exists(
    1.56 +              And(fun_apply_fm(5,4,3),
    1.57 +               And(succ_fm(4,2),
    1.58 +                And(fun_apply_fm(5,2,1),
    1.59 +                 And(pair_fm(3,1,0), Member(0,r#+9))))))))))))))))))))"
    1.60  
    1.61  
    1.62  lemma rtran_closure_mem_type [TC]:
    1.63   "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> rtran_closure_mem_fm(x,y,z) \<in> formula"
    1.64 -by (simp add: rtran_closure_mem_fm_def) 
    1.65 +by (simp add: rtran_closure_mem_fm_def)
    1.66  
    1.67  lemma arity_rtran_closure_mem_fm [simp]:
    1.68 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
    1.69 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
    1.70        ==> arity(rtran_closure_mem_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
    1.71 -by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac) 
    1.72 +by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac)
    1.73  
    1.74  lemma sats_rtran_closure_mem_fm [simp]:
    1.75     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    1.76 -    ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <-> 
    1.77 +    ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <->
    1.78          rtran_closure_mem(**A, nth(x,env), nth(y,env), nth(z,env))"
    1.79  by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def)
    1.80  
    1.81  lemma rtran_closure_mem_iff_sats:
    1.82 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
    1.83 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
    1.84            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
    1.85         ==> rtran_closure_mem(**A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)"
    1.86  by (simp add: sats_rtran_closure_mem_fm)
    1.87  
    1.88  theorem rtran_closure_mem_reflection:
    1.89 -     "REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)), 
    1.90 +     "REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)),
    1.91                 \<lambda>i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]"
    1.92  apply (simp only: rtran_closure_mem_def setclass_simps)
    1.93 -apply (intro FOL_reflections function_reflections fun_plus_reflections)  
    1.94 +apply (intro FOL_reflections function_reflections fun_plus_reflections)
    1.95  done
    1.96  
    1.97  text{*Separation for @{term "rtrancl(r)"}.*}
    1.98  lemma rtrancl_separation:
    1.99       "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))"
   1.100 -apply (rule separation_CollectI) 
   1.101 -apply (rule_tac A="{r,A,z}" in subset_LsetE, blast ) 
   1.102 +apply (rule separation_CollectI)
   1.103 +apply (rule_tac A="{r,A,z}" in subset_LsetE, blast )
   1.104  apply (rule ReflectsE [OF rtran_closure_mem_reflection], assumption)
   1.105 -apply (drule subset_Lset_ltD, assumption) 
   1.106 +apply (drule subset_Lset_ltD, assumption)
   1.107  apply (erule reflection_imp_L_separation)
   1.108    apply (simp_all add: lt_Ord2)
   1.109  apply (rule DPow_LsetI)
   1.110 @@ -89,38 +89,38 @@
   1.111  
   1.112  subsubsection{*Reflexive/Transitive Closure, Internalized*}
   1.113  
   1.114 -(*  "rtran_closure(M,r,s) == 
   1.115 +(*  "rtran_closure(M,r,s) ==
   1.116          \<forall>A[M]. is_field(M,r,A) -->
   1.117 - 	 (\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))" *)
   1.118 +         (\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))" *)
   1.119  constdefs rtran_closure_fm :: "[i,i]=>i"
   1.120 - "rtran_closure_fm(r,s) == 
   1.121 + "rtran_closure_fm(r,s) ==
   1.122     Forall(Implies(field_fm(succ(r),0),
   1.123                    Forall(Iff(Member(0,succ(succ(s))),
   1.124                               rtran_closure_mem_fm(1,succ(succ(r)),0)))))"
   1.125  
   1.126  lemma rtran_closure_type [TC]:
   1.127       "[| x \<in> nat; y \<in> nat |] ==> rtran_closure_fm(x,y) \<in> formula"
   1.128 -by (simp add: rtran_closure_fm_def) 
   1.129 +by (simp add: rtran_closure_fm_def)
   1.130  
   1.131  lemma arity_rtran_closure_fm [simp]:
   1.132 -     "[| x \<in> nat; y \<in> nat |] 
   1.133 +     "[| x \<in> nat; y \<in> nat |]
   1.134        ==> arity(rtran_closure_fm(x,y)) = succ(x) \<union> succ(y)"
   1.135  by (simp add: rtran_closure_fm_def succ_Un_distrib [symmetric] Un_ac)
   1.136  
   1.137  lemma sats_rtran_closure_fm [simp]:
   1.138     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   1.139 -    ==> sats(A, rtran_closure_fm(x,y), env) <-> 
   1.140 +    ==> sats(A, rtran_closure_fm(x,y), env) <->
   1.141          rtran_closure(**A, nth(x,env), nth(y,env))"
   1.142  by (simp add: rtran_closure_fm_def rtran_closure_def)
   1.143  
   1.144  lemma rtran_closure_iff_sats:
   1.145 -      "[| nth(i,env) = x; nth(j,env) = y; 
   1.146 +      "[| nth(i,env) = x; nth(j,env) = y;
   1.147            i \<in> nat; j \<in> nat; env \<in> list(A)|]
   1.148         ==> rtran_closure(**A, x, y) <-> sats(A, rtran_closure_fm(i,j), env)"
   1.149  by simp
   1.150  
   1.151  theorem rtran_closure_reflection:
   1.152 -     "REFLECTS[\<lambda>x. rtran_closure(L,f(x),g(x)), 
   1.153 +     "REFLECTS[\<lambda>x. rtran_closure(L,f(x),g(x)),
   1.154                 \<lambda>i x. rtran_closure(**Lset(i),f(x),g(x))]"
   1.155  apply (simp only: rtran_closure_def setclass_simps)
   1.156  apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection)
   1.157 @@ -132,35 +132,35 @@
   1.158  (*  "tran_closure(M,r,t) ==
   1.159           \<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *)
   1.160  constdefs tran_closure_fm :: "[i,i]=>i"
   1.161 - "tran_closure_fm(r,s) == 
   1.162 + "tran_closure_fm(r,s) ==
   1.163     Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))"
   1.164  
   1.165  lemma tran_closure_type [TC]:
   1.166       "[| x \<in> nat; y \<in> nat |] ==> tran_closure_fm(x,y) \<in> formula"
   1.167 -by (simp add: tran_closure_fm_def) 
   1.168 +by (simp add: tran_closure_fm_def)
   1.169  
   1.170  lemma arity_tran_closure_fm [simp]:
   1.171 -     "[| x \<in> nat; y \<in> nat |] 
   1.172 +     "[| x \<in> nat; y \<in> nat |]
   1.173        ==> arity(tran_closure_fm(x,y)) = succ(x) \<union> succ(y)"
   1.174  by (simp add: tran_closure_fm_def succ_Un_distrib [symmetric] Un_ac)
   1.175  
   1.176  lemma sats_tran_closure_fm [simp]:
   1.177     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   1.178 -    ==> sats(A, tran_closure_fm(x,y), env) <-> 
   1.179 +    ==> sats(A, tran_closure_fm(x,y), env) <->
   1.180          tran_closure(**A, nth(x,env), nth(y,env))"
   1.181  by (simp add: tran_closure_fm_def tran_closure_def)
   1.182  
   1.183  lemma tran_closure_iff_sats:
   1.184 -      "[| nth(i,env) = x; nth(j,env) = y; 
   1.185 +      "[| nth(i,env) = x; nth(j,env) = y;
   1.186            i \<in> nat; j \<in> nat; env \<in> list(A)|]
   1.187         ==> tran_closure(**A, x, y) <-> sats(A, tran_closure_fm(i,j), env)"
   1.188  by simp
   1.189  
   1.190  theorem tran_closure_reflection:
   1.191 -     "REFLECTS[\<lambda>x. tran_closure(L,f(x),g(x)), 
   1.192 +     "REFLECTS[\<lambda>x. tran_closure(L,f(x),g(x)),
   1.193                 \<lambda>i x. tran_closure(**Lset(i),f(x),g(x))]"
   1.194  apply (simp only: tran_closure_def setclass_simps)
   1.195 -apply (intro FOL_reflections function_reflections 
   1.196 +apply (intro FOL_reflections function_reflections
   1.197               rtran_closure_reflection composition_reflection)
   1.198  done
   1.199  
   1.200 @@ -168,60 +168,62 @@
   1.201  subsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*}
   1.202  
   1.203  lemma wellfounded_trancl_reflects:
   1.204 -  "REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L]. 
   1.205 -	         w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp,
   1.206 -   \<lambda>i x. \<exists>w \<in> Lset(i). \<exists>wx \<in> Lset(i). \<exists>rp \<in> Lset(i). 
   1.207 +  "REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
   1.208 +                 w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp,
   1.209 +   \<lambda>i x. \<exists>w \<in> Lset(i). \<exists>wx \<in> Lset(i). \<exists>rp \<in> Lset(i).
   1.210         w \<in> Z & pair(**Lset(i),w,x,wx) & tran_closure(**Lset(i),r,rp) &
   1.211         wx \<in> rp]"
   1.212 -by (intro FOL_reflections function_reflections fun_plus_reflections 
   1.213 +by (intro FOL_reflections function_reflections fun_plus_reflections
   1.214            tran_closure_reflection)
   1.215  
   1.216  
   1.217  lemma wellfounded_trancl_separation:
   1.218 -	 "[| L(r); L(Z) |] ==> 
   1.219 -	  separation (L, \<lambda>x. 
   1.220 -	      \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L]. 
   1.221 -	       w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)"
   1.222 -apply (rule separation_CollectI) 
   1.223 -apply (rule_tac A="{r,Z,z}" in subset_LsetE, blast ) 
   1.224 +         "[| L(r); L(Z) |] ==>
   1.225 +          separation (L, \<lambda>x.
   1.226 +              \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
   1.227 +               w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)"
   1.228 +apply (rule separation_CollectI)
   1.229 +apply (rule_tac A="{r,Z,z}" in subset_LsetE, blast )
   1.230  apply (rule ReflectsE [OF wellfounded_trancl_reflects], assumption)
   1.231 -apply (drule subset_Lset_ltD, assumption) 
   1.232 +apply (drule subset_Lset_ltD, assumption)
   1.233  apply (erule reflection_imp_L_separation)
   1.234    apply (simp_all add: lt_Ord2)
   1.235  apply (rule DPow_LsetI)
   1.236 -apply (rename_tac u) 
   1.237 +apply (rename_tac u)
   1.238  apply (rule bex_iff_sats conj_iff_sats)+
   1.239 -apply (rule_tac env = "[w,u,r,Z]" in mem_iff_sats) 
   1.240 +apply (rule_tac env = "[w,u,r,Z]" in mem_iff_sats)
   1.241  apply (rule sep_rules tran_closure_iff_sats | simp)+
   1.242  done
   1.243  
   1.244  
   1.245  subsubsection{*Instantiating the locale @{text M_trancl}*}
   1.246 -ML
   1.247 -{*
   1.248 -val rtrancl_separation = thm "rtrancl_separation";
   1.249 -val wellfounded_trancl_separation = thm "wellfounded_trancl_separation";
   1.250 +
   1.251 +theorem M_trancl_axioms_L: "M_trancl_axioms(L)"
   1.252 +  apply (rule M_trancl_axioms.intro)
   1.253 +   apply (assumption | rule
   1.254 +     rtrancl_separation wellfounded_trancl_separation)+
   1.255 +  done
   1.256  
   1.257 -
   1.258 -val m_trancl = [rtrancl_separation, wellfounded_trancl_separation];
   1.259 -
   1.260 -fun trancl_L th =
   1.261 -    kill_flex_triv_prems (m_trancl MRS (axioms_L th));
   1.262 +theorem M_trancl_L: "PROP M_trancl(L)"
   1.263 +  apply (rule M_trancl.intro)
   1.264 +    apply (rule M_triv_axioms_L)
   1.265 +   apply (rule M_axioms_axioms_L)
   1.266 +  apply (rule M_trancl_axioms_L)
   1.267 +  done
   1.268  
   1.269 -bind_thm ("iterates_abs", trancl_L (thm "M_trancl.iterates_abs"));
   1.270 -bind_thm ("rtran_closure_rtrancl", trancl_L (thm "M_trancl.rtran_closure_rtrancl"));
   1.271 -bind_thm ("rtrancl_closed", trancl_L (thm "M_trancl.rtrancl_closed"));
   1.272 -bind_thm ("rtrancl_abs", trancl_L (thm "M_trancl.rtrancl_abs"));
   1.273 -bind_thm ("trancl_closed", trancl_L (thm "M_trancl.trancl_closed"));
   1.274 -bind_thm ("trancl_abs", trancl_L (thm "M_trancl.trancl_abs"));
   1.275 -bind_thm ("wellfounded_on_trancl", trancl_L (thm "M_trancl.wellfounded_on_trancl"));
   1.276 -bind_thm ("wellfounded_trancl", trancl_L (thm "M_trancl.wellfounded_trancl"));
   1.277 -bind_thm ("wfrec_relativize", trancl_L (thm "M_trancl.wfrec_relativize"));
   1.278 -bind_thm ("trans_wfrec_relativize", trancl_L (thm "M_trancl.trans_wfrec_relativize"));
   1.279 -bind_thm ("trans_wfrec_abs", trancl_L (thm "M_trancl.trans_wfrec_abs"));
   1.280 -bind_thm ("trans_eq_pair_wfrec_iff", trancl_L (thm "M_trancl.trans_eq_pair_wfrec_iff"));
   1.281 -bind_thm ("eq_pair_wfrec_iff", trancl_L (thm "M_trancl.eq_pair_wfrec_iff"));
   1.282 -*}
   1.283 +lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L]
   1.284 +  and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L]
   1.285 +  and rtrancl_closed = M_trancl.rtrancl_closed [OF M_trancl_L]
   1.286 +  and rtrancl_abs = M_trancl.rtrancl_abs [OF M_trancl_L]
   1.287 +  and trancl_closed = M_trancl.trancl_closed [OF M_trancl_L]
   1.288 +  and trancl_abs = M_trancl.trancl_abs [OF M_trancl_L]
   1.289 +  and wellfounded_on_trancl = M_trancl.wellfounded_on_trancl [OF M_trancl_L]
   1.290 +  and wellfounded_trancl = M_trancl.wellfounded_trancl [OF M_trancl_L]
   1.291 +  and wfrec_relativize = M_trancl.wfrec_relativize [OF M_trancl_L]
   1.292 +  and trans_wfrec_relativize = M_trancl.trans_wfrec_relativize [OF M_trancl_L]
   1.293 +  and trans_wfrec_abs = M_trancl.trans_wfrec_abs [OF M_trancl_L]
   1.294 +  and trans_eq_pair_wfrec_iff = M_trancl.trans_eq_pair_wfrec_iff [OF M_trancl_L]
   1.295 +  and eq_pair_wfrec_iff = M_trancl.eq_pair_wfrec_iff [OF M_trancl_L]
   1.296  
   1.297  declare rtrancl_closed [intro,simp]
   1.298  declare rtrancl_abs [simp]
   1.299 @@ -232,17 +234,17 @@
   1.300  subsection{*Well-Founded Recursion!*}
   1.301  
   1.302  (* M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
   1.303 -   "M_is_recfun(M,MH,r,a,f) == 
   1.304 -     \<forall>z[M]. z \<in> f <-> 
   1.305 +   "M_is_recfun(M,MH,r,a,f) ==
   1.306 +     \<forall>z[M]. z \<in> f <->
   1.307              5      4       3       2       1           0
   1.308 -            (\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M]. 
   1.309 -	       pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) &
   1.310 +            (\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M].
   1.311 +               pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) &
   1.312                 pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
   1.313                 xa \<in> r & MH(x, f_r_sx, y))"
   1.314  *)
   1.315  
   1.316  constdefs is_recfun_fm :: "[[i,i,i]=>i, i, i, i]=>i"
   1.317 - "is_recfun_fm(p,r,a,f) == 
   1.318 + "is_recfun_fm(p,r,a,f) ==
   1.319     Forall(Iff(Member(0,succ(f)),
   1.320      Exists(Exists(Exists(Exists(Exists(Exists(
   1.321       And(pair_fm(5,4,6),
   1.322 @@ -254,39 +256,39 @@
   1.323  
   1.324  
   1.325  lemma is_recfun_type_0:
   1.326 -     "[| !!x y z. [| x \<in> nat; y \<in> nat; z \<in> nat |] ==> p(x,y,z) \<in> formula;  
   1.327 -         x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.328 +     "[| !!x y z. [| x \<in> nat; y \<in> nat; z \<in> nat |] ==> p(x,y,z) \<in> formula;
   1.329 +         x \<in> nat; y \<in> nat; z \<in> nat |]
   1.330        ==> is_recfun_fm(p,x,y,z) \<in> formula"
   1.331  apply (unfold is_recfun_fm_def)
   1.332  (*FIXME: FIND OUT why simp loops!*)
   1.333  apply typecheck
   1.334 -by simp 
   1.335 +by simp
   1.336  
   1.337  lemma is_recfun_type [TC]:
   1.338 -     "[| p(5,0,4) \<in> formula;  
   1.339 -         x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.340 +     "[| p(5,0,4) \<in> formula;
   1.341 +         x \<in> nat; y \<in> nat; z \<in> nat |]
   1.342        ==> is_recfun_fm(p,x,y,z) \<in> formula"
   1.343 -by (simp add: is_recfun_fm_def) 
   1.344 +by (simp add: is_recfun_fm_def)
   1.345  
   1.346  lemma arity_is_recfun_fm [simp]:
   1.347 -     "[| arity(p(5,0,4)) le 8; x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.348 +     "[| arity(p(5,0,4)) le 8; x \<in> nat; y \<in> nat; z \<in> nat |]
   1.349        ==> arity(is_recfun_fm(p,x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   1.350 -apply (frule lt_nat_in_nat, simp) 
   1.351 -apply (simp add: is_recfun_fm_def succ_Un_distrib [symmetric] ) 
   1.352 -apply (subst subset_Un_iff2 [of "arity(p(5,0,4))", THEN iffD1]) 
   1.353 -apply (rule le_imp_subset) 
   1.354 -apply (erule le_trans, simp) 
   1.355 -apply (simp add: succ_Un_distrib [symmetric] Un_ac) 
   1.356 +apply (frule lt_nat_in_nat, simp)
   1.357 +apply (simp add: is_recfun_fm_def succ_Un_distrib [symmetric] )
   1.358 +apply (subst subset_Un_iff2 [of "arity(p(5,0,4))", THEN iffD1])
   1.359 +apply (rule le_imp_subset)
   1.360 +apply (erule le_trans, simp)
   1.361 +apply (simp add: succ_Un_distrib [symmetric] Un_ac)
   1.362  done
   1.363  
   1.364  lemma sats_is_recfun_fm:
   1.365 -  assumes MH_iff_sats: 
   1.366 -      "!!x y z env. 
   1.367 -	 [| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   1.368 -	 ==> MH(nth(x,env), nth(y,env), nth(z,env)) <-> sats(A, p(x,y,z), env)"
   1.369 -  shows 
   1.370 +  assumes MH_iff_sats:
   1.371 +      "!!x y z env.
   1.372 +         [| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   1.373 +         ==> MH(nth(x,env), nth(y,env), nth(z,env)) <-> sats(A, p(x,y,z), env)"
   1.374 +  shows
   1.375        "[|x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   1.376 -       ==> sats(A, is_recfun_fm(p,x,y,z), env) <-> 
   1.377 +       ==> sats(A, is_recfun_fm(p,x,y,z), env) <->
   1.378             M_is_recfun(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
   1.379  by (simp add: is_recfun_fm_def M_is_recfun_def MH_iff_sats [THEN iff_sym])
   1.380  
   1.381 @@ -294,20 +296,20 @@
   1.382    "[| (!!x y z env. [| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   1.383                      ==> MH(nth(x,env), nth(y,env), nth(z,env)) <->
   1.384                          sats(A, p(x,y,z), env));
   1.385 -      nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.386 +      nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   1.387        i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   1.388 -   ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)" 
   1.389 +   ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)"
   1.390  by (simp add: sats_is_recfun_fm [of A MH])
   1.391  
   1.392  theorem is_recfun_reflection:
   1.393    assumes MH_reflection:
   1.394 -    "!!f g h. REFLECTS[\<lambda>x. MH(L, f(x), g(x), h(x)), 
   1.395 +    "!!f g h. REFLECTS[\<lambda>x. MH(L, f(x), g(x), h(x)),
   1.396                       \<lambda>i x. MH(**Lset(i), f(x), g(x), h(x))]"
   1.397 -  shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L), f(x), g(x), h(x)), 
   1.398 +  shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L), f(x), g(x), h(x)),
   1.399                 \<lambda>i x. M_is_recfun(**Lset(i), MH(**Lset(i)), f(x), g(x), h(x))]"
   1.400  apply (simp (no_asm_use) only: M_is_recfun_def setclass_simps)
   1.401 -apply (intro FOL_reflections function_reflections 
   1.402 -             restriction_reflection MH_reflection)  
   1.403 +apply (intro FOL_reflections function_reflections
   1.404 +             restriction_reflection MH_reflection)
   1.405  done
   1.406  
   1.407  text{*Currently, @{text sats}-theorems for higher-order operators don't seem
   1.408 @@ -315,12 +317,12 @@
   1.409  of the @{text MH}-term.*}
   1.410  theorem is_wfrec_reflection:
   1.411    assumes MH_reflection:
   1.412 -    "!!f g h. REFLECTS[\<lambda>x. MH(L, f(x), g(x), h(x)), 
   1.413 +    "!!f g h. REFLECTS[\<lambda>x. MH(L, f(x), g(x), h(x)),
   1.414                       \<lambda>i x. MH(**Lset(i), f(x), g(x), h(x))]"
   1.415 -  shows "REFLECTS[\<lambda>x. is_wfrec(L, MH(L), f(x), g(x), h(x)), 
   1.416 +  shows "REFLECTS[\<lambda>x. is_wfrec(L, MH(L), f(x), g(x), h(x)),
   1.417                 \<lambda>i x. is_wfrec(**Lset(i), MH(**Lset(i)), f(x), g(x), h(x))]"
   1.418  apply (simp (no_asm_use) only: is_wfrec_def setclass_simps)
   1.419 -apply (intro FOL_reflections MH_reflection is_recfun_reflection)  
   1.420 +apply (intro FOL_reflections MH_reflection is_recfun_reflection)
   1.421  done
   1.422  
   1.423  subsection{*The Locale @{text "M_wfrank"}*}
   1.424 @@ -331,23 +333,23 @@
   1.425   "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
   1.426                ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)),
   1.427        \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
   1.428 -         ~ (\<exists>f \<in> Lset(i). 
   1.429 -            M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), 
   1.430 +         ~ (\<exists>f \<in> Lset(i).
   1.431 +            M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y),
   1.432                          rplus, x, f))]"
   1.433 -by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection)  
   1.434 +by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection)
   1.435  
   1.436  lemma wfrank_separation:
   1.437       "L(r) ==>
   1.438        separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
   1.439           ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))"
   1.440 -apply (rule separation_CollectI) 
   1.441 -apply (rule_tac A="{r,z}" in subset_LsetE, blast ) 
   1.442 +apply (rule separation_CollectI)
   1.443 +apply (rule_tac A="{r,z}" in subset_LsetE, blast )
   1.444  apply (rule ReflectsE [OF wfrank_Reflects], assumption)
   1.445 -apply (drule subset_Lset_ltD, assumption) 
   1.446 +apply (drule subset_Lset_ltD, assumption)
   1.447  apply (erule reflection_imp_L_separation)
   1.448    apply (simp_all add: lt_Ord2, clarify)
   1.449  apply (rule DPow_LsetI)
   1.450 -apply (rename_tac u)  
   1.451 +apply (rename_tac u)
   1.452  apply (rule ball_iff_sats imp_iff_sats)+
   1.453  apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
   1.454  apply (rule sep_rules is_recfun_iff_sats | simp)+
   1.455 @@ -357,14 +359,14 @@
   1.456  subsubsection{*Replacement for @{term "wfrank"}*}
   1.457  
   1.458  lemma wfrank_replacement_Reflects:
   1.459 - "REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A & 
   1.460 + "REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A &
   1.461          (\<forall>rplus[L]. tran_closure(L,r,rplus) -->
   1.462 -         (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  & 
   1.463 +         (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  &
   1.464                          M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
   1.465                          is_range(L,f,y))),
   1.466 - \<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A & 
   1.467 + \<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A &
   1.468        (\<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
   1.469 -       (\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(**Lset(i),x,y,z)  & 
   1.470 +       (\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(**Lset(i),x,y,z)  &
   1.471           M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), rplus, x, f) &
   1.472           is_range(**Lset(i),f,y)))]"
   1.473  by (intro FOL_reflections function_reflections fun_plus_reflections
   1.474 @@ -373,24 +375,24 @@
   1.475  
   1.476  lemma wfrank_strong_replacement:
   1.477       "L(r) ==>
   1.478 -      strong_replacement(L, \<lambda>x z. 
   1.479 +      strong_replacement(L, \<lambda>x z.
   1.480           \<forall>rplus[L]. tran_closure(L,r,rplus) -->
   1.481 -         (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  & 
   1.482 +         (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  &
   1.483                          M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
   1.484                          is_range(L,f,y)))"
   1.485 -apply (rule strong_replacementI) 
   1.486 +apply (rule strong_replacementI)
   1.487  apply (rule rallI)
   1.488 -apply (rename_tac B)  
   1.489 -apply (rule separation_CollectI) 
   1.490 -apply (rule_tac A="{B,r,z}" in subset_LsetE, blast ) 
   1.491 +apply (rename_tac B)
   1.492 +apply (rule separation_CollectI)
   1.493 +apply (rule_tac A="{B,r,z}" in subset_LsetE, blast )
   1.494  apply (rule ReflectsE [OF wfrank_replacement_Reflects], assumption)
   1.495 -apply (drule subset_Lset_ltD, assumption) 
   1.496 +apply (drule subset_Lset_ltD, assumption)
   1.497  apply (erule reflection_imp_L_separation)
   1.498    apply (simp_all add: lt_Ord2)
   1.499  apply (rule DPow_LsetI)
   1.500 -apply (rename_tac u) 
   1.501 +apply (rename_tac u)
   1.502  apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+
   1.503 -apply (rule_tac env = "[x,u,B,r]" in mem_iff_sats) 
   1.504 +apply (rule_tac env = "[x,u,B,r]" in mem_iff_sats)
   1.505  apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+
   1.506  done
   1.507  
   1.508 @@ -398,36 +400,36 @@
   1.509  subsubsection{*Separation for Proving @{text Ord_wfrank_range}*}
   1.510  
   1.511  lemma Ord_wfrank_Reflects:
   1.512 - "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) --> 
   1.513 -          ~ (\<forall>f[L]. \<forall>rangef[L]. 
   1.514 + "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
   1.515 +          ~ (\<forall>f[L]. \<forall>rangef[L].
   1.516               is_range(L,f,rangef) -->
   1.517               M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
   1.518               ordinal(L,rangef)),
   1.519 -      \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) --> 
   1.520 -          ~ (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i). 
   1.521 +      \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
   1.522 +          ~ (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i).
   1.523               is_range(**Lset(i),f,rangef) -->
   1.524 -             M_is_recfun(**Lset(i), \<lambda>x f y. is_range(**Lset(i),f,y), 
   1.525 +             M_is_recfun(**Lset(i), \<lambda>x f y. is_range(**Lset(i),f,y),
   1.526                           rplus, x, f) -->
   1.527               ordinal(**Lset(i),rangef))]"
   1.528 -by (intro FOL_reflections function_reflections is_recfun_reflection 
   1.529 +by (intro FOL_reflections function_reflections is_recfun_reflection
   1.530            tran_closure_reflection ordinal_reflection)
   1.531  
   1.532  lemma  Ord_wfrank_separation:
   1.533       "L(r) ==>
   1.534        separation (L, \<lambda>x.
   1.535 -         \<forall>rplus[L]. tran_closure(L,r,rplus) --> 
   1.536 -          ~ (\<forall>f[L]. \<forall>rangef[L]. 
   1.537 +         \<forall>rplus[L]. tran_closure(L,r,rplus) -->
   1.538 +          ~ (\<forall>f[L]. \<forall>rangef[L].
   1.539               is_range(L,f,rangef) -->
   1.540               M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
   1.541 -             ordinal(L,rangef)))" 
   1.542 -apply (rule separation_CollectI) 
   1.543 -apply (rule_tac A="{r,z}" in subset_LsetE, blast ) 
   1.544 +             ordinal(L,rangef)))"
   1.545 +apply (rule separation_CollectI)
   1.546 +apply (rule_tac A="{r,z}" in subset_LsetE, blast )
   1.547  apply (rule ReflectsE [OF Ord_wfrank_Reflects], assumption)
   1.548 -apply (drule subset_Lset_ltD, assumption) 
   1.549 +apply (drule subset_Lset_ltD, assumption)
   1.550  apply (erule reflection_imp_L_separation)
   1.551    apply (simp_all add: lt_Ord2, clarify)
   1.552  apply (rule DPow_LsetI)
   1.553 -apply (rename_tac u)  
   1.554 +apply (rename_tac u)
   1.555  apply (rule ball_iff_sats imp_iff_sats)+
   1.556  apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
   1.557  apply (rule sep_rules is_recfun_iff_sats | simp)+
   1.558 @@ -435,40 +437,40 @@
   1.559  
   1.560  
   1.561  subsubsection{*Instantiating the locale @{text M_wfrank}*}
   1.562 -ML
   1.563 -{*
   1.564 -val wfrank_separation = thm "wfrank_separation";
   1.565 -val wfrank_strong_replacement = thm "wfrank_strong_replacement";
   1.566 -val Ord_wfrank_separation = thm "Ord_wfrank_separation";
   1.567 +
   1.568 +theorem M_wfrank_axioms_L: "M_wfrank_axioms(L)"
   1.569 +  apply (rule M_wfrank_axioms.intro)
   1.570 +  apply (assumption | rule
   1.571 +    wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+
   1.572 +  done
   1.573  
   1.574 -val m_wfrank = 
   1.575 -    [wfrank_separation, wfrank_strong_replacement, Ord_wfrank_separation];
   1.576 -
   1.577 -fun wfrank_L th =
   1.578 -    kill_flex_triv_prems (m_wfrank MRS (trancl_L th));
   1.579 -
   1.580 -
   1.581 +theorem M_wfrank_L: "PROP M_wfrank(L)"
   1.582 +  apply (rule M_wfrank.intro)
   1.583 +     apply (rule M_triv_axioms_L)
   1.584 +    apply (rule M_axioms_axioms_L)
   1.585 +   apply (rule M_trancl_axioms_L)
   1.586 +  apply (rule M_wfrank_axioms_L)
   1.587 +  done
   1.588  
   1.589 -bind_thm ("iterates_closed", wfrank_L (thm "M_wfrank.iterates_closed"));
   1.590 -bind_thm ("exists_wfrank", wfrank_L (thm "M_wfrank.exists_wfrank"));
   1.591 -bind_thm ("M_wellfoundedrank", wfrank_L (thm "M_wfrank.M_wellfoundedrank"));
   1.592 -bind_thm ("Ord_wfrank_range", wfrank_L (thm "M_wfrank.Ord_wfrank_range"));
   1.593 -bind_thm ("Ord_range_wellfoundedrank", wfrank_L (thm "M_wfrank.Ord_range_wellfoundedrank"));
   1.594 -bind_thm ("function_wellfoundedrank", wfrank_L (thm "M_wfrank.function_wellfoundedrank"));
   1.595 -bind_thm ("domain_wellfoundedrank", wfrank_L (thm "M_wfrank.domain_wellfoundedrank"));
   1.596 -bind_thm ("wellfoundedrank_type", wfrank_L (thm "M_wfrank.wellfoundedrank_type"));
   1.597 -bind_thm ("Ord_wellfoundedrank", wfrank_L (thm "M_wfrank.Ord_wellfoundedrank"));
   1.598 -bind_thm ("wellfoundedrank_eq", wfrank_L (thm "M_wfrank.wellfoundedrank_eq"));
   1.599 -bind_thm ("wellfoundedrank_lt", wfrank_L (thm "M_wfrank.wellfoundedrank_lt"));
   1.600 -bind_thm ("wellfounded_imp_subset_rvimage", wfrank_L (thm "M_wfrank.wellfounded_imp_subset_rvimage"));
   1.601 -bind_thm ("wellfounded_imp_wf", wfrank_L (thm "M_wfrank.wellfounded_imp_wf"));
   1.602 -bind_thm ("wellfounded_on_imp_wf_on", wfrank_L (thm "M_wfrank.wellfounded_on_imp_wf_on"));
   1.603 -bind_thm ("wf_abs", wfrank_L (thm "M_wfrank.wf_abs"));
   1.604 -bind_thm ("wf_on_abs", wfrank_L (thm "M_wfrank.wf_on_abs"));
   1.605 -bind_thm ("wfrec_replacement_iff", wfrank_L (thm "M_wfrank.wfrec_replacement_iff"));
   1.606 -bind_thm ("trans_wfrec_closed", wfrank_L (thm "M_wfrank.trans_wfrec_closed"));
   1.607 -bind_thm ("wfrec_closed", wfrank_L (thm "M_wfrank.wfrec_closed"));
   1.608 -*}
   1.609 +lemmas iterates_closed = M_wfrank.iterates_closed [OF M_wfrank_L]
   1.610 +  and exists_wfrank = M_wfrank.exists_wfrank [OF M_wfrank_L]
   1.611 +  and M_wellfoundedrank = M_wfrank.M_wellfoundedrank [OF M_wfrank_L]
   1.612 +  and Ord_wfrank_range = M_wfrank.Ord_wfrank_range [OF M_wfrank_L]
   1.613 +  and Ord_range_wellfoundedrank = M_wfrank.Ord_range_wellfoundedrank [OF M_wfrank_L]
   1.614 +  and function_wellfoundedrank = M_wfrank.function_wellfoundedrank [OF M_wfrank_L]
   1.615 +  and domain_wellfoundedrank = M_wfrank.domain_wellfoundedrank [OF M_wfrank_L]
   1.616 +  and wellfoundedrank_type = M_wfrank.wellfoundedrank_type [OF M_wfrank_L]
   1.617 +  and Ord_wellfoundedrank = M_wfrank.Ord_wellfoundedrank [OF M_wfrank_L]
   1.618 +  and wellfoundedrank_eq = M_wfrank.wellfoundedrank_eq [OF M_wfrank_L]
   1.619 +  and wellfoundedrank_lt = M_wfrank.wellfoundedrank_lt [OF M_wfrank_L]
   1.620 +  and wellfounded_imp_subset_rvimage = M_wfrank.wellfounded_imp_subset_rvimage [OF M_wfrank_L]
   1.621 +  and wellfounded_imp_wf = M_wfrank.wellfounded_imp_wf [OF M_wfrank_L]
   1.622 +  and wellfounded_on_imp_wf_on = M_wfrank.wellfounded_on_imp_wf_on [OF M_wfrank_L]
   1.623 +  and wf_abs = M_wfrank.wf_abs [OF M_wfrank_L]
   1.624 +  and wf_on_abs = M_wfrank.wf_on_abs [OF M_wfrank_L]
   1.625 +  and wfrec_replacement_iff = M_wfrank.wfrec_replacement_iff [OF M_wfrank_L]
   1.626 +  and trans_wfrec_closed = M_wfrank.trans_wfrec_closed [OF M_wfrank_L]
   1.627 +  and wfrec_closed = M_wfrank.wfrec_closed [OF M_wfrank_L]
   1.628  
   1.629  declare iterates_closed [intro,simp]
   1.630  declare Ord_wfrank_range [rule_format]
   1.631 @@ -481,9 +483,9 @@
   1.632  subsubsection{*Binary Products, Internalized*}
   1.633  
   1.634  constdefs cartprod_fm :: "[i,i,i]=>i"
   1.635 -(* "cartprod(M,A,B,z) == 
   1.636 -	\<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))" *)
   1.637 -    "cartprod_fm(A,B,z) == 
   1.638 +(* "cartprod(M,A,B,z) ==
   1.639 +        \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))" *)
   1.640 +    "cartprod_fm(A,B,z) ==
   1.641         Forall(Iff(Member(0,succ(z)),
   1.642                    Exists(And(Member(0,succ(succ(A))),
   1.643                           Exists(And(Member(0,succ(succ(succ(B)))),
   1.644 @@ -491,74 +493,74 @@
   1.645  
   1.646  lemma cartprod_type [TC]:
   1.647       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> cartprod_fm(x,y,z) \<in> formula"
   1.648 -by (simp add: cartprod_fm_def) 
   1.649 +by (simp add: cartprod_fm_def)
   1.650  
   1.651  lemma arity_cartprod_fm [simp]:
   1.652 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.653 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   1.654        ==> arity(cartprod_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   1.655 -by (simp add: cartprod_fm_def succ_Un_distrib [symmetric] Un_ac) 
   1.656 +by (simp add: cartprod_fm_def succ_Un_distrib [symmetric] Un_ac)
   1.657  
   1.658  lemma sats_cartprod_fm [simp]:
   1.659     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   1.660 -    ==> sats(A, cartprod_fm(x,y,z), env) <-> 
   1.661 +    ==> sats(A, cartprod_fm(x,y,z), env) <->
   1.662          cartprod(**A, nth(x,env), nth(y,env), nth(z,env))"
   1.663  by (simp add: cartprod_fm_def cartprod_def)
   1.664  
   1.665  lemma cartprod_iff_sats:
   1.666 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.667 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   1.668            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   1.669         ==> cartprod(**A, x, y, z) <-> sats(A, cartprod_fm(i,j,k), env)"
   1.670  by (simp add: sats_cartprod_fm)
   1.671  
   1.672  theorem cartprod_reflection:
   1.673 -     "REFLECTS[\<lambda>x. cartprod(L,f(x),g(x),h(x)), 
   1.674 +     "REFLECTS[\<lambda>x. cartprod(L,f(x),g(x),h(x)),
   1.675                 \<lambda>i x. cartprod(**Lset(i),f(x),g(x),h(x))]"
   1.676  apply (simp only: cartprod_def setclass_simps)
   1.677 -apply (intro FOL_reflections pair_reflection)  
   1.678 +apply (intro FOL_reflections pair_reflection)
   1.679  done
   1.680  
   1.681  
   1.682  subsubsection{*Binary Sums, Internalized*}
   1.683  
   1.684 -(* "is_sum(M,A,B,Z) == 
   1.685 -       \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M]. 
   1.686 +(* "is_sum(M,A,B,Z) ==
   1.687 +       \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M].
   1.688           3      2       1        0
   1.689         number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
   1.690         cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"  *)
   1.691  constdefs sum_fm :: "[i,i,i]=>i"
   1.692 -    "sum_fm(A,B,Z) == 
   1.693 +    "sum_fm(A,B,Z) ==
   1.694         Exists(Exists(Exists(Exists(
   1.695 -	And(number1_fm(2),
   1.696 +        And(number1_fm(2),
   1.697              And(cartprod_fm(2,A#+4,3),
   1.698                  And(upair_fm(2,2,1),
   1.699                      And(cartprod_fm(1,B#+4,0), union_fm(3,0,Z#+4)))))))))"
   1.700  
   1.701  lemma sum_type [TC]:
   1.702       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> sum_fm(x,y,z) \<in> formula"
   1.703 -by (simp add: sum_fm_def) 
   1.704 +by (simp add: sum_fm_def)
   1.705  
   1.706  lemma arity_sum_fm [simp]:
   1.707 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.708 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   1.709        ==> arity(sum_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   1.710 -by (simp add: sum_fm_def succ_Un_distrib [symmetric] Un_ac) 
   1.711 +by (simp add: sum_fm_def succ_Un_distrib [symmetric] Un_ac)
   1.712  
   1.713  lemma sats_sum_fm [simp]:
   1.714     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   1.715 -    ==> sats(A, sum_fm(x,y,z), env) <-> 
   1.716 +    ==> sats(A, sum_fm(x,y,z), env) <->
   1.717          is_sum(**A, nth(x,env), nth(y,env), nth(z,env))"
   1.718  by (simp add: sum_fm_def is_sum_def)
   1.719  
   1.720  lemma sum_iff_sats:
   1.721 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.722 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   1.723            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   1.724         ==> is_sum(**A, x, y, z) <-> sats(A, sum_fm(i,j,k), env)"
   1.725  by simp
   1.726  
   1.727  theorem sum_reflection:
   1.728 -     "REFLECTS[\<lambda>x. is_sum(L,f(x),g(x),h(x)), 
   1.729 +     "REFLECTS[\<lambda>x. is_sum(L,f(x),g(x),h(x)),
   1.730                 \<lambda>i x. is_sum(**Lset(i),f(x),g(x),h(x))]"
   1.731  apply (simp only: is_sum_def setclass_simps)
   1.732 -apply (intro FOL_reflections function_reflections cartprod_reflection)  
   1.733 +apply (intro FOL_reflections function_reflections cartprod_reflection)
   1.734  done
   1.735  
   1.736  
   1.737 @@ -570,11 +572,11 @@
   1.738  
   1.739  lemma quasinat_type [TC]:
   1.740       "x \<in> nat ==> quasinat_fm(x) \<in> formula"
   1.741 -by (simp add: quasinat_fm_def) 
   1.742 +by (simp add: quasinat_fm_def)
   1.743  
   1.744  lemma arity_quasinat_fm [simp]:
   1.745       "x \<in> nat ==> arity(quasinat_fm(x)) = succ(x)"
   1.746 -by (simp add: quasinat_fm_def succ_Un_distrib [symmetric] Un_ac) 
   1.747 +by (simp add: quasinat_fm_def succ_Un_distrib [symmetric] Un_ac)
   1.748  
   1.749  lemma sats_quasinat_fm [simp]:
   1.750     "[| x \<in> nat; env \<in> list(A)|]
   1.751 @@ -582,85 +584,85 @@
   1.752  by (simp add: quasinat_fm_def is_quasinat_def)
   1.753  
   1.754  lemma quasinat_iff_sats:
   1.755 -      "[| nth(i,env) = x; nth(j,env) = y; 
   1.756 +      "[| nth(i,env) = x; nth(j,env) = y;
   1.757            i \<in> nat; env \<in> list(A)|]
   1.758         ==> is_quasinat(**A, x) <-> sats(A, quasinat_fm(i), env)"
   1.759  by simp
   1.760  
   1.761  theorem quasinat_reflection:
   1.762 -     "REFLECTS[\<lambda>x. is_quasinat(L,f(x)), 
   1.763 +     "REFLECTS[\<lambda>x. is_quasinat(L,f(x)),
   1.764                 \<lambda>i x. is_quasinat(**Lset(i),f(x))]"
   1.765  apply (simp only: is_quasinat_def setclass_simps)
   1.766 -apply (intro FOL_reflections function_reflections)  
   1.767 +apply (intro FOL_reflections function_reflections)
   1.768  done
   1.769  
   1.770  
   1.771  subsubsection{*The Operator @{term is_nat_case}*}
   1.772  
   1.773  (* is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o"
   1.774 -    "is_nat_case(M, a, is_b, k, z) == 
   1.775 +    "is_nat_case(M, a, is_b, k, z) ==
   1.776         (empty(M,k) --> z=a) &
   1.777         (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
   1.778         (is_quasinat(M,k) | empty(M,z))" *)
   1.779  text{*The formula @{term is_b} has free variables 1 and 0.*}
   1.780  constdefs is_nat_case_fm :: "[i, [i,i]=>i, i, i]=>i"
   1.781 - "is_nat_case_fm(a,is_b,k,z) == 
   1.782 + "is_nat_case_fm(a,is_b,k,z) ==
   1.783      And(Implies(empty_fm(k), Equal(z,a)),
   1.784 -        And(Forall(Implies(succ_fm(0,succ(k)), 
   1.785 +        And(Forall(Implies(succ_fm(0,succ(k)),
   1.786                     Forall(Implies(Equal(0,succ(succ(z))), is_b(1,0))))),
   1.787              Or(quasinat_fm(k), empty_fm(z))))"
   1.788  
   1.789  lemma is_nat_case_type [TC]:
   1.790 -     "[| is_b(1,0) \<in> formula;  
   1.791 -         x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.792 +     "[| is_b(1,0) \<in> formula;
   1.793 +         x \<in> nat; y \<in> nat; z \<in> nat |]
   1.794        ==> is_nat_case_fm(x,is_b,y,z) \<in> formula"
   1.795 -by (simp add: is_nat_case_fm_def) 
   1.796 +by (simp add: is_nat_case_fm_def)
   1.797  
   1.798  lemma arity_is_nat_case_fm [simp]:
   1.799 -     "[| is_b(1,0) \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.800 -      ==> arity(is_nat_case_fm(x,is_b,y,z)) = 
   1.801 -          succ(x) \<union> succ(y) \<union> succ(z) \<union> (arity(is_b(1,0)) #- 2)" 
   1.802 -apply (subgoal_tac "arity(is_b(1,0)) \<in> nat")  
   1.803 +     "[| is_b(1,0) \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |]
   1.804 +      ==> arity(is_nat_case_fm(x,is_b,y,z)) =
   1.805 +          succ(x) \<union> succ(y) \<union> succ(z) \<union> (arity(is_b(1,0)) #- 2)"
   1.806 +apply (subgoal_tac "arity(is_b(1,0)) \<in> nat")
   1.807  apply typecheck
   1.808  (*FIXME: could nat_diff_split work?*)
   1.809  apply (auto simp add: diff_def raw_diff_succ is_nat_case_fm_def nat_imp_quasinat
   1.810                   succ_Un_distrib [symmetric] Un_ac
   1.811 -                 split: split_nat_case) 
   1.812 +                 split: split_nat_case)
   1.813  done
   1.814  
   1.815  lemma sats_is_nat_case_fm:
   1.816 -  assumes is_b_iff_sats: 
   1.817 -      "!!a b. [| a \<in> A; b \<in> A|] 
   1.818 +  assumes is_b_iff_sats:
   1.819 +      "!!a b. [| a \<in> A; b \<in> A|]
   1.820                ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, Cons(a,env)))"
   1.821 -  shows 
   1.822 +  shows
   1.823        "[|x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
   1.824 -       ==> sats(A, is_nat_case_fm(x,p,y,z), env) <-> 
   1.825 +       ==> sats(A, is_nat_case_fm(x,p,y,z), env) <->
   1.826             is_nat_case(**A, nth(x,env), is_b, nth(y,env), nth(z,env))"
   1.827 -apply (frule lt_length_in_nat, assumption)  
   1.828 +apply (frule lt_length_in_nat, assumption)
   1.829  apply (simp add: is_nat_case_fm_def is_nat_case_def is_b_iff_sats [THEN iff_sym])
   1.830  done
   1.831  
   1.832  lemma is_nat_case_iff_sats:
   1.833 -  "[| (!!a b. [| a \<in> A; b \<in> A|] 
   1.834 +  "[| (!!a b. [| a \<in> A; b \<in> A|]
   1.835                ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, Cons(a,env))));
   1.836 -      nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.837 +      nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   1.838        i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
   1.839 -   ==> is_nat_case(**A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)" 
   1.840 +   ==> is_nat_case(**A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)"
   1.841  by (simp add: sats_is_nat_case_fm [of A is_b])
   1.842  
   1.843  
   1.844  text{*The second argument of @{term is_b} gives it direct access to @{term x},
   1.845 -  which is essential for handling free variable references.  Without this 
   1.846 +  which is essential for handling free variable references.  Without this
   1.847    argument, we cannot prove reflection for @{term iterates_MH}.*}
   1.848  theorem is_nat_case_reflection:
   1.849    assumes is_b_reflection:
   1.850 -    "!!h f g. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x)), 
   1.851 +    "!!h f g. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x)),
   1.852                       \<lambda>i x. is_b(**Lset(i), h(x), f(x), g(x))]"
   1.853 -  shows "REFLECTS[\<lambda>x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)), 
   1.854 +  shows "REFLECTS[\<lambda>x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)),
   1.855                 \<lambda>i x. is_nat_case(**Lset(i), f(x), is_b(**Lset(i), x), g(x), h(x))]"
   1.856  apply (simp (no_asm_use) only: is_nat_case_def setclass_simps)
   1.857 -apply (intro FOL_reflections function_reflections 
   1.858 -             restriction_reflection is_b_reflection quasinat_reflection)  
   1.859 +apply (intro FOL_reflections function_reflections
   1.860 +             restriction_reflection is_b_reflection quasinat_reflection)
   1.861  done
   1.862  
   1.863  
   1.864 @@ -672,117 +674,117 @@
   1.865          is_nat_case(M, v, \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & isF(gm,u),
   1.866                      n, z)" *)
   1.867  constdefs iterates_MH_fm :: "[[i,i]=>i, i, i, i, i]=>i"
   1.868 - "iterates_MH_fm(isF,v,n,g,z) == 
   1.869 -    is_nat_case_fm(v, 
   1.870 -      \<lambda>m u. Exists(And(fun_apply_fm(succ(succ(succ(g))),succ(m),0), 
   1.871 -                     Forall(Implies(Equal(0,succ(succ(u))), isF(1,0))))), 
   1.872 + "iterates_MH_fm(isF,v,n,g,z) ==
   1.873 +    is_nat_case_fm(v,
   1.874 +      \<lambda>m u. Exists(And(fun_apply_fm(succ(succ(succ(g))),succ(m),0),
   1.875 +                     Forall(Implies(Equal(0,succ(succ(u))), isF(1,0))))),
   1.876        n, z)"
   1.877  
   1.878  lemma iterates_MH_type [TC]:
   1.879 -     "[| p(1,0) \<in> formula;  
   1.880 -         v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.881 +     "[| p(1,0) \<in> formula;
   1.882 +         v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
   1.883        ==> iterates_MH_fm(p,v,x,y,z) \<in> formula"
   1.884 -by (simp add: iterates_MH_fm_def) 
   1.885 +by (simp add: iterates_MH_fm_def)
   1.886  
   1.887  
   1.888  lemma arity_iterates_MH_fm [simp]:
   1.889 -     "[| p(1,0) \<in> formula; 
   1.890 -         v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.891 -      ==> arity(iterates_MH_fm(p,v,x,y,z)) = 
   1.892 +     "[| p(1,0) \<in> formula;
   1.893 +         v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
   1.894 +      ==> arity(iterates_MH_fm(p,v,x,y,z)) =
   1.895            succ(v) \<union> succ(x) \<union> succ(y) \<union> succ(z) \<union> (arity(p(1,0)) #- 4)"
   1.896  apply (subgoal_tac "arity(p(1,0)) \<in> nat")
   1.897  apply typecheck
   1.898  apply (simp add: nat_imp_quasinat iterates_MH_fm_def Un_ac
   1.899              split: split_nat_case, clarify)
   1.900  apply (rename_tac i j)
   1.901 -apply (drule eq_succ_imp_eq_m1, simp) 
   1.902 +apply (drule eq_succ_imp_eq_m1, simp)
   1.903  apply (drule eq_succ_imp_eq_m1, simp)
   1.904  apply (simp add: diff_Un_distrib succ_Un_distrib Un_ac diff_diff_left)
   1.905  done
   1.906  
   1.907  lemma sats_iterates_MH_fm:
   1.908 -  assumes is_F_iff_sats: 
   1.909 -      "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|] 
   1.910 +  assumes is_F_iff_sats:
   1.911 +      "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
   1.912                ==> is_F(a,b) <->
   1.913                    sats(A, p(1,0), Cons(b, Cons(a, Cons(c, Cons(d,env)))))"
   1.914 -  shows 
   1.915 +  shows
   1.916        "[|v \<in> nat; x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
   1.917 -       ==> sats(A, iterates_MH_fm(p,v,x,y,z), env) <-> 
   1.918 +       ==> sats(A, iterates_MH_fm(p,v,x,y,z), env) <->
   1.919             iterates_MH(**A, is_F, nth(v,env), nth(x,env), nth(y,env), nth(z,env))"
   1.920 -by (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm 
   1.921 +by (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm
   1.922                is_F_iff_sats [symmetric])
   1.923  
   1.924  lemma iterates_MH_iff_sats:
   1.925 -  "[| (!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|] 
   1.926 +  "[| (!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
   1.927                ==> is_F(a,b) <->
   1.928                    sats(A, p(1,0), Cons(b, Cons(a, Cons(c, Cons(d,env))))));
   1.929 -      nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.930 +      nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   1.931        i' \<in> nat; i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
   1.932 -   ==> iterates_MH(**A, is_F, v, x, y, z) <-> 
   1.933 +   ==> iterates_MH(**A, is_F, v, x, y, z) <->
   1.934         sats(A, iterates_MH_fm(p,i',i,j,k), env)"
   1.935 -apply (rule iff_sym) 
   1.936 -apply (rule iff_trans) 
   1.937 -apply (rule sats_iterates_MH_fm [of A is_F], blast, simp_all) 
   1.938 +apply (rule iff_sym)
   1.939 +apply (rule iff_trans)
   1.940 +apply (rule sats_iterates_MH_fm [of A is_F], blast, simp_all)
   1.941  done
   1.942  
   1.943  theorem iterates_MH_reflection:
   1.944    assumes p_reflection:
   1.945 -    "!!f g h. REFLECTS[\<lambda>x. p(L, f(x), g(x)), 
   1.946 +    "!!f g h. REFLECTS[\<lambda>x. p(L, f(x), g(x)),
   1.947                       \<lambda>i x. p(**Lset(i), f(x), g(x))]"
   1.948 - shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L), e(x), f(x), g(x), h(x)), 
   1.949 + shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L), e(x), f(x), g(x), h(x)),
   1.950                 \<lambda>i x. iterates_MH(**Lset(i), p(**Lset(i)), e(x), f(x), g(x), h(x))]"
   1.951  apply (simp (no_asm_use) only: iterates_MH_def)
   1.952  txt{*Must be careful: simplifying with @{text setclass_simps} above would
   1.953       change @{text "\<exists>gm[**Lset(i)]"} into @{text "\<exists>gm \<in> Lset(i)"}, when
   1.954       it would no longer match rule @{text is_nat_case_reflection}. *}
   1.955 -apply (rule is_nat_case_reflection) 
   1.956 +apply (rule is_nat_case_reflection)
   1.957  apply (simp (no_asm_use) only: setclass_simps)
   1.958  apply (intro FOL_reflections function_reflections is_nat_case_reflection
   1.959 -             restriction_reflection p_reflection)  
   1.960 +             restriction_reflection p_reflection)
   1.961  done
   1.962  
   1.963  
   1.964  
   1.965 -subsection{*@{term L} is Closed Under the Operator @{term list}*} 
   1.966 +subsection{*@{term L} is Closed Under the Operator @{term list}*}
   1.967  
   1.968  subsubsection{*The List Functor, Internalized*}
   1.969  
   1.970  constdefs list_functor_fm :: "[i,i,i]=>i"
   1.971 -(* "is_list_functor(M,A,X,Z) == 
   1.972 -        \<exists>n1[M]. \<exists>AX[M]. 
   1.973 +(* "is_list_functor(M,A,X,Z) ==
   1.974 +        \<exists>n1[M]. \<exists>AX[M].
   1.975           number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)" *)
   1.976 -    "list_functor_fm(A,X,Z) == 
   1.977 +    "list_functor_fm(A,X,Z) ==
   1.978         Exists(Exists(
   1.979 -	And(number1_fm(1),
   1.980 +        And(number1_fm(1),
   1.981              And(cartprod_fm(A#+2,X#+2,0), sum_fm(1,0,Z#+2)))))"
   1.982  
   1.983  lemma list_functor_type [TC]:
   1.984       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> list_functor_fm(x,y,z) \<in> formula"
   1.985 -by (simp add: list_functor_fm_def) 
   1.986 +by (simp add: list_functor_fm_def)
   1.987  
   1.988  lemma arity_list_functor_fm [simp]:
   1.989 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.990 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   1.991        ==> arity(list_functor_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   1.992 -by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac) 
   1.993 +by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac)
   1.994  
   1.995  lemma sats_list_functor_fm [simp]:
   1.996     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   1.997 -    ==> sats(A, list_functor_fm(x,y,z), env) <-> 
   1.998 +    ==> sats(A, list_functor_fm(x,y,z), env) <->
   1.999          is_list_functor(**A, nth(x,env), nth(y,env), nth(z,env))"
  1.1000  by (simp add: list_functor_fm_def is_list_functor_def)
  1.1001  
  1.1002  lemma list_functor_iff_sats:
  1.1003 -  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
  1.1004 +  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
  1.1005        i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
  1.1006     ==> is_list_functor(**A, x, y, z) <-> sats(A, list_functor_fm(i,j,k), env)"
  1.1007  by simp
  1.1008  
  1.1009  theorem list_functor_reflection:
  1.1010 -     "REFLECTS[\<lambda>x. is_list_functor(L,f(x),g(x),h(x)), 
  1.1011 +     "REFLECTS[\<lambda>x. is_list_functor(L,f(x),g(x),h(x)),
  1.1012                 \<lambda>i x. is_list_functor(**Lset(i),f(x),g(x),h(x))]"
  1.1013  apply (simp only: is_list_functor_def setclass_simps)
  1.1014  apply (intro FOL_reflections number1_reflection
  1.1015 -             cartprod_reflection sum_reflection)  
  1.1016 +             cartprod_reflection sum_reflection)
  1.1017  done
  1.1018  
  1.1019  
  1.1020 @@ -793,29 +795,29 @@
  1.1021     [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
  1.1022           is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)),
  1.1023      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
  1.1024 -         is_wfrec(**Lset(i), 
  1.1025 -                  iterates_MH(**Lset(i), 
  1.1026 +         is_wfrec(**Lset(i),
  1.1027 +                  iterates_MH(**Lset(i),
  1.1028                            is_list_functor(**Lset(i), A), 0), memsn, u, y))]"
  1.1029 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
  1.1030 -          iterates_MH_reflection list_functor_reflection) 
  1.1031 +by (intro FOL_reflections function_reflections is_wfrec_reflection
  1.1032 +          iterates_MH_reflection list_functor_reflection)
  1.1033  
  1.1034 -lemma list_replacement1: 
  1.1035 +lemma list_replacement1:
  1.1036     "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)"
  1.1037  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
  1.1038 -apply (rule strong_replacementI) 
  1.1039 +apply (rule strong_replacementI)
  1.1040  apply (rule rallI)
  1.1041 -apply (rename_tac B)   
  1.1042 -apply (rule separation_CollectI) 
  1.1043 -apply (insert nonempty) 
  1.1044 -apply (subgoal_tac "L(Memrel(succ(n)))") 
  1.1045 -apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast ) 
  1.1046 +apply (rename_tac B)
  1.1047 +apply (rule separation_CollectI)
  1.1048 +apply (insert nonempty)
  1.1049 +apply (subgoal_tac "L(Memrel(succ(n)))")
  1.1050 +apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast )
  1.1051  apply (rule ReflectsE [OF list_replacement1_Reflects], assumption)
  1.1052 -apply (drule subset_Lset_ltD, assumption) 
  1.1053 +apply (drule subset_Lset_ltD, assumption)
  1.1054  apply (erule reflection_imp_L_separation)
  1.1055    apply (simp_all add: lt_Ord2 Memrel_closed)
  1.1056 -apply (elim conjE) 
  1.1057 +apply (elim conjE)
  1.1058  apply (rule DPow_LsetI)
  1.1059 -apply (rename_tac v) 
  1.1060 +apply (rename_tac v)
  1.1061  apply (rule bex_iff_sats conj_iff_sats)+
  1.1062  apply (rule_tac env = "[u,v,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
  1.1063  apply (rule sep_rules | simp)+
  1.1064 @@ -832,34 +834,34 @@
  1.1065             is_wfrec (L, iterates_MH (L, is_list_functor(L, A), 0),
  1.1066                                msn, u, x)),
  1.1067      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
  1.1068 -         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). 
  1.1069 +         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i).
  1.1070            successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
  1.1071 -           is_wfrec (**Lset(i), 
  1.1072 +           is_wfrec (**Lset(i),
  1.1073                   iterates_MH (**Lset(i), is_list_functor(**Lset(i), A), 0),
  1.1074                       msn, u, x))]"
  1.1075 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
  1.1076 -          iterates_MH_reflection list_functor_reflection) 
  1.1077 +by (intro FOL_reflections function_reflections is_wfrec_reflection
  1.1078 +          iterates_MH_reflection list_functor_reflection)
  1.1079  
  1.1080  
  1.1081 -lemma list_replacement2: 
  1.1082 -   "L(A) ==> strong_replacement(L, 
  1.1083 -         \<lambda>n y. n\<in>nat & 
  1.1084 +lemma list_replacement2:
  1.1085 +   "L(A) ==> strong_replacement(L,
  1.1086 +         \<lambda>n y. n\<in>nat &
  1.1087                 (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
  1.1088 -               is_wfrec(L, iterates_MH(L,is_list_functor(L,A), 0), 
  1.1089 +               is_wfrec(L, iterates_MH(L,is_list_functor(L,A), 0),
  1.1090                          msn, n, y)))"
  1.1091 -apply (rule strong_replacementI) 
  1.1092 +apply (rule strong_replacementI)
  1.1093  apply (rule rallI)
  1.1094 -apply (rename_tac B)   
  1.1095 -apply (rule separation_CollectI) 
  1.1096 -apply (insert nonempty) 
  1.1097 -apply (rule_tac A="{A,B,z,0,nat}" in subset_LsetE) 
  1.1098 -apply (blast intro: L_nat) 
  1.1099 +apply (rename_tac B)
  1.1100 +apply (rule separation_CollectI)
  1.1101 +apply (insert nonempty)
  1.1102 +apply (rule_tac A="{A,B,z,0,nat}" in subset_LsetE)
  1.1103 +apply (blast intro: L_nat)
  1.1104  apply (rule ReflectsE [OF list_replacement2_Reflects], assumption)
  1.1105 -apply (drule subset_Lset_ltD, assumption) 
  1.1106 +apply (drule subset_Lset_ltD, assumption)
  1.1107  apply (erule reflection_imp_L_separation)
  1.1108    apply (simp_all add: lt_Ord2)
  1.1109  apply (rule DPow_LsetI)
  1.1110 -apply (rename_tac v) 
  1.1111 +apply (rename_tac v)
  1.1112  apply (rule bex_iff_sats conj_iff_sats)+
  1.1113  apply (rule_tac env = "[u,v,A,B,0,nat]" in mem_iff_sats)
  1.1114  apply (rule sep_rules | simp)+
  1.1115 @@ -868,21 +870,21 @@
  1.1116  done
  1.1117  
  1.1118  
  1.1119 -subsection{*@{term L} is Closed Under the Operator @{term formula}*} 
  1.1120 +subsection{*@{term L} is Closed Under the Operator @{term formula}*}
  1.1121  
  1.1122  subsubsection{*The Formula Functor, Internalized*}
  1.1123  
  1.1124  constdefs formula_functor_fm :: "[i,i]=>i"
  1.1125 -(*     "is_formula_functor(M,X,Z) == 
  1.1126 -        \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M]. 
  1.1127 +(*     "is_formula_functor(M,X,Z) ==
  1.1128 +        \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M].
  1.1129             4           3               2       1       0
  1.1130 -          omega(M,nat') & cartprod(M,nat',nat',natnat) & 
  1.1131 +          omega(M,nat') & cartprod(M,nat',nat',natnat) &
  1.1132            is_sum(M,natnat,natnat,natnatsum) &
  1.1133 -          cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) & 
  1.1134 -          is_sum(M,natnatsum,X3,Z)" *) 
  1.1135 -    "formula_functor_fm(X,Z) == 
  1.1136 +          cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) &
  1.1137 +          is_sum(M,natnatsum,X3,Z)" *)
  1.1138 +    "formula_functor_fm(X,Z) ==
  1.1139         Exists(Exists(Exists(Exists(Exists(
  1.1140 -	And(omega_fm(4),
  1.1141 +        And(omega_fm(4),
  1.1142           And(cartprod_fm(4,4,3),
  1.1143            And(sum_fm(3,3,2),
  1.1144             And(cartprod_fm(X#+5,X#+5,1),
  1.1145 @@ -890,26 +892,26 @@
  1.1146  
  1.1147  lemma formula_functor_type [TC]:
  1.1148       "[| x \<in> nat; y \<in> nat |] ==> formula_functor_fm(x,y) \<in> formula"
  1.1149 -by (simp add: formula_functor_fm_def) 
  1.1150 +by (simp add: formula_functor_fm_def)
  1.1151  
  1.1152  lemma sats_formula_functor_fm [simp]:
  1.1153     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
  1.1154 -    ==> sats(A, formula_functor_fm(x,y), env) <-> 
  1.1155 +    ==> sats(A, formula_functor_fm(x,y), env) <->
  1.1156          is_formula_functor(**A, nth(x,env), nth(y,env))"
  1.1157  by (simp add: formula_functor_fm_def is_formula_functor_def)
  1.1158  
  1.1159  lemma formula_functor_iff_sats:
  1.1160 -  "[| nth(i,env) = x; nth(j,env) = y; 
  1.1161 +  "[| nth(i,env) = x; nth(j,env) = y;
  1.1162        i \<in> nat; j \<in> nat; env \<in> list(A)|]
  1.1163     ==> is_formula_functor(**A, x, y) <-> sats(A, formula_functor_fm(i,j), env)"
  1.1164  by simp
  1.1165  
  1.1166  theorem formula_functor_reflection:
  1.1167 -     "REFLECTS[\<lambda>x. is_formula_functor(L,f(x),g(x)), 
  1.1168 +     "REFLECTS[\<lambda>x. is_formula_functor(L,f(x),g(x)),
  1.1169                 \<lambda>i x. is_formula_functor(**Lset(i),f(x),g(x))]"
  1.1170  apply (simp only: is_formula_functor_def setclass_simps)
  1.1171  apply (intro FOL_reflections omega_reflection
  1.1172 -             cartprod_reflection sum_reflection)  
  1.1173 +             cartprod_reflection sum_reflection)
  1.1174  done
  1.1175  
  1.1176  subsubsection{*Instances of Replacement for Formulas*}
  1.1177 @@ -919,28 +921,28 @@
  1.1178     [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
  1.1179           is_wfrec(L, iterates_MH(L, is_formula_functor(L), 0), memsn, u, y)),
  1.1180      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
  1.1181 -         is_wfrec(**Lset(i), 
  1.1182 -                  iterates_MH(**Lset(i), 
  1.1183 +         is_wfrec(**Lset(i),
  1.1184 +                  iterates_MH(**Lset(i),
  1.1185                            is_formula_functor(**Lset(i)), 0), memsn, u, y))]"
  1.1186 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
  1.1187 -          iterates_MH_reflection formula_functor_reflection) 
  1.1188 +by (intro FOL_reflections function_reflections is_wfrec_reflection
  1.1189 +          iterates_MH_reflection formula_functor_reflection)
  1.1190  
  1.1191 -lemma formula_replacement1: 
  1.1192 +lemma formula_replacement1:
  1.1193     "iterates_replacement(L, is_formula_functor(L), 0)"
  1.1194  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
  1.1195 -apply (rule strong_replacementI) 
  1.1196 +apply (rule strong_replacementI)
  1.1197  apply (rule rallI)
  1.1198 -apply (rename_tac B)   
  1.1199 -apply (rule separation_CollectI) 
  1.1200 -apply (insert nonempty) 
  1.1201 -apply (subgoal_tac "L(Memrel(succ(n)))") 
  1.1202 -apply (rule_tac A="{B,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast ) 
  1.1203 +apply (rename_tac B)
  1.1204 +apply (rule separation_CollectI)
  1.1205 +apply (insert nonempty)
  1.1206 +apply (subgoal_tac "L(Memrel(succ(n)))")
  1.1207 +apply (rule_tac A="{B,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast )
  1.1208  apply (rule ReflectsE [OF formula_replacement1_Reflects], assumption)
  1.1209 -apply (drule subset_Lset_ltD, assumption) 
  1.1210 +apply (drule subset_Lset_ltD, assumption)
  1.1211  apply (erule reflection_imp_L_separation)
  1.1212    apply (simp_all add: lt_Ord2 Memrel_closed)
  1.1213  apply (rule DPow_LsetI)
  1.1214 -apply (rename_tac v) 
  1.1215 +apply (rename_tac v)
  1.1216  apply (rule bex_iff_sats conj_iff_sats)+
  1.1217  apply (rule_tac env = "[u,v,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
  1.1218  apply (rule sep_rules | simp)+
  1.1219 @@ -957,34 +959,34 @@
  1.1220             is_wfrec (L, iterates_MH (L, is_formula_functor(L), 0),
  1.1221                                msn, u, x)),
  1.1222      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
  1.1223 -         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). 
  1.1224 +         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i).
  1.1225            successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
  1.1226 -           is_wfrec (**Lset(i), 
  1.1227 +           is_wfrec (**Lset(i),
  1.1228                   iterates_MH (**Lset(i), is_formula_functor(**Lset(i)), 0),
  1.1229                       msn, u, x))]"
  1.1230 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
  1.1231 -          iterates_MH_reflection formula_functor_reflection) 
  1.1232 +by (intro FOL_reflections function_reflections is_wfrec_reflection
  1.1233 +          iterates_MH_reflection formula_functor_reflection)
  1.1234  
  1.1235  
  1.1236 -lemma formula_replacement2: 
  1.1237 -   "strong_replacement(L, 
  1.1238 -         \<lambda>n y. n\<in>nat & 
  1.1239 +lemma formula_replacement2:
  1.1240 +   "strong_replacement(L,
  1.1241 +         \<lambda>n y. n\<in>nat &
  1.1242                 (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
  1.1243 -               is_wfrec(L, iterates_MH(L,is_formula_functor(L), 0), 
  1.1244 +               is_wfrec(L, iterates_MH(L,is_formula_functor(L), 0),
  1.1245                          msn, n, y)))"
  1.1246 -apply (rule strong_replacementI) 
  1.1247 +apply (rule strong_replacementI)
  1.1248  apply (rule rallI)
  1.1249 -apply (rename_tac B)   
  1.1250 -apply (rule separation_CollectI) 
  1.1251 -apply (insert nonempty) 
  1.1252 -apply (rule_tac A="{B,z,0,nat}" in subset_LsetE) 
  1.1253 -apply (blast intro: L_nat) 
  1.1254 +apply (rename_tac B)
  1.1255 +apply (rule separation_CollectI)
  1.1256 +apply (insert nonempty)
  1.1257 +apply (rule_tac A="{B,z,0,nat}" in subset_LsetE)
  1.1258 +apply (blast intro: L_nat)
  1.1259  apply (rule ReflectsE [OF formula_replacement2_Reflects], assumption)
  1.1260 -apply (drule subset_Lset_ltD, assumption) 
  1.1261 +apply (drule subset_Lset_ltD, assumption)
  1.1262  apply (erule reflection_imp_L_separation)
  1.1263    apply (simp_all add: lt_Ord2)
  1.1264  apply (rule DPow_LsetI)
  1.1265 -apply (rename_tac v) 
  1.1266 +apply (rename_tac v)
  1.1267  apply (rule bex_iff_sats conj_iff_sats)+
  1.1268  apply (rule_tac env = "[u,v,B,0,nat]" in mem_iff_sats)
  1.1269  apply (rule sep_rules | simp)+
  1.1270 @@ -1006,7 +1008,7 @@
  1.1271  
  1.1272  lemma Inl_type [TC]:
  1.1273       "[| x \<in> nat; z \<in> nat |] ==> Inl_fm(x,z) \<in> formula"
  1.1274 -by (simp add: Inl_fm_def) 
  1.1275 +by (simp add: Inl_fm_def)
  1.1276  
  1.1277  lemma sats_Inl_fm [simp]:
  1.1278     "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
  1.1279 @@ -1014,16 +1016,16 @@
  1.1280  by (simp add: Inl_fm_def is_Inl_def)
  1.1281  
  1.1282  lemma Inl_iff_sats:
  1.1283 -      "[| nth(i,env) = x; nth(k,env) = z; 
  1.1284 +      "[| nth(i,env) = x; nth(k,env) = z;
  1.1285            i \<in> nat; k \<in> nat; env \<in> list(A)|]
  1.1286         ==> is_Inl(**A, x, z) <-> sats(A, Inl_fm(i,k), env)"
  1.1287  by simp
  1.1288  
  1.1289  theorem Inl_reflection:
  1.1290 -     "REFLECTS[\<lambda>x. is_Inl(L,f(x),h(x)), 
  1.1291 +     "REFLECTS[\<lambda>x. is_Inl(L,f(x),h(x)),
  1.1292                 \<lambda>i x. is_Inl(**Lset(i),f(x),h(x))]"
  1.1293  apply (simp only: is_Inl_def setclass_simps)
  1.1294 -apply (intro FOL_reflections function_reflections)  
  1.1295 +apply (intro FOL_reflections function_reflections)
  1.1296  done
  1.1297  
  1.1298  
  1.1299 @@ -1035,7 +1037,7 @@
  1.1300  
  1.1301  lemma Inr_type [TC]:
  1.1302       "[| x \<in> nat; z \<in> nat |] ==> Inr_fm(x,z) \<in> formula"
  1.1303 -by (simp add: Inr_fm_def) 
  1.1304 +by (simp add: Inr_fm_def)
  1.1305  
  1.1306  lemma sats_Inr_fm [simp]:
  1.1307     "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
  1.1308 @@ -1043,16 +1045,16 @@
  1.1309  by (simp add: Inr_fm_def is_Inr_def)
  1.1310  
  1.1311  lemma Inr_iff_sats:
  1.1312 -      "[| nth(i,env) = x; nth(k,env) = z; 
  1.1313 +      "[| nth(i,env) = x; nth(k,env) = z;
  1.1314            i \<in> nat; k \<in> nat; env \<in> list(A)|]
  1.1315         ==> is_Inr(**A, x, z) <-> sats(A, Inr_fm(i,k), env)"
  1.1316  by simp
  1.1317  
  1.1318  theorem Inr_reflection:
  1.1319 -     "REFLECTS[\<lambda>x. is_Inr(L,f(x),h(x)), 
  1.1320 +     "REFLECTS[\<lambda>x. is_Inr(L,f(x),h(x)),
  1.1321                 \<lambda>i x. is_Inr(**Lset(i),f(x),h(x))]"
  1.1322  apply (simp only: is_Inr_def setclass_simps)
  1.1323 -apply (intro FOL_reflections function_reflections)  
  1.1324 +apply (intro FOL_reflections function_reflections)
  1.1325  done
  1.1326  
  1.1327  
  1.1328 @@ -1062,9 +1064,9 @@
  1.1329  
  1.1330  constdefs Nil_fm :: "i=>i"
  1.1331      "Nil_fm(x) == Exists(And(empty_fm(0), Inl_fm(0,succ(x))))"
  1.1332 - 
  1.1333 +
  1.1334  lemma Nil_type [TC]: "x \<in> nat ==> Nil_fm(x) \<in> formula"
  1.1335 -by (simp add: Nil_fm_def) 
  1.1336 +by (simp add: Nil_fm_def)
  1.1337  
  1.1338  lemma sats_Nil_fm [simp]:
  1.1339     "[| x \<in> nat; env \<in> list(A)|]
  1.1340 @@ -1077,10 +1079,10 @@
  1.1341  by simp
  1.1342  
  1.1343  theorem Nil_reflection:
  1.1344 -     "REFLECTS[\<lambda>x. is_Nil(L,f(x)), 
  1.1345 +     "REFLECTS[\<lambda>x. is_Nil(L,f(x)),
  1.1346                 \<lambda>i x. is_Nil(**Lset(i),f(x))]"
  1.1347  apply (simp only: is_Nil_def setclass_simps)
  1.1348 -apply (intro FOL_reflections function_reflections Inl_reflection)  
  1.1349 +apply (intro FOL_reflections function_reflections Inl_reflection)
  1.1350  done
  1.1351  
  1.1352  
  1.1353 @@ -1089,30 +1091,30 @@
  1.1354  
  1.1355  (*  "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)" *)
  1.1356  constdefs Cons_fm :: "[i,i,i]=>i"
  1.1357 -    "Cons_fm(a,l,Z) == 
  1.1358 +    "Cons_fm(a,l,Z) ==
  1.1359         Exists(And(pair_fm(succ(a),succ(l),0), Inr_fm(0,succ(Z))))"
  1.1360  
  1.1361  lemma Cons_type [TC]:
  1.1362       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Cons_fm(x,y,z) \<in> formula"
  1.1363 -by (simp add: Cons_fm_def) 
  1.1364 +by (simp add: Cons_fm_def)
  1.1365  
  1.1366  lemma sats_Cons_fm [simp]:
  1.1367     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
  1.1368 -    ==> sats(A, Cons_fm(x,y,z), env) <-> 
  1.1369 +    ==> sats(A, Cons_fm(x,y,z), env) <->
  1.1370         is_Cons(**A, nth(x,env), nth(y,env), nth(z,env))"
  1.1371  by (simp add: Cons_fm_def is_Cons_def)
  1.1372  
  1.1373  lemma Cons_iff_sats:
  1.1374 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
  1.1375 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
  1.1376            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
  1.1377         ==>is_Cons(**A, x, y, z) <-> sats(A, Cons_fm(i,j,k), env)"
  1.1378  by simp
  1.1379  
  1.1380  theorem Cons_reflection:
  1.1381 -     "REFLECTS[\<lambda>x. is_Cons(L,f(x),g(x),h(x)), 
  1.1382 +     "REFLECTS[\<lambda>x. is_Cons(L,f(x),g(x),h(x)),
  1.1383                 \<lambda>i x. is_Cons(**Lset(i),f(x),g(x),h(x))]"
  1.1384  apply (simp only: is_Cons_def setclass_simps)
  1.1385 -apply (intro FOL_reflections pair_reflection Inr_reflection)  
  1.1386 +apply (intro FOL_reflections pair_reflection Inr_reflection)
  1.1387  done
  1.1388  
  1.1389  subsubsection{*The Formula @{term is_quasilist}, Internalized*}
  1.1390 @@ -1120,11 +1122,11 @@
  1.1391  (* is_quasilist(M,xs) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))" *)
  1.1392  
  1.1393  constdefs quasilist_fm :: "i=>i"
  1.1394 -    "quasilist_fm(x) == 
  1.1395 +    "quasilist_fm(x) ==
  1.1396         Or(Nil_fm(x), Exists(Exists(Cons_fm(1,0,succ(succ(x))))))"
  1.1397 - 
  1.1398 +
  1.1399  lemma quasilist_type [TC]: "x \<in> nat ==> quasilist_fm(x) \<in> formula"
  1.1400 -by (simp add: quasilist_fm_def) 
  1.1401 +by (simp add: quasilist_fm_def)
  1.1402  
  1.1403  lemma sats_quasilist_fm [simp]:
  1.1404     "[| x \<in> nat; env \<in> list(A)|]
  1.1405 @@ -1137,10 +1139,10 @@
  1.1406  by simp
  1.1407  
  1.1408  theorem quasilist_reflection:
  1.1409 -     "REFLECTS[\<lambda>x. is_quasilist(L,f(x)), 
  1.1410 +     "REFLECTS[\<lambda>x. is_quasilist(L,f(x)),
  1.1411                 \<lambda>i x. is_quasilist(**Lset(i),f(x))]"
  1.1412  apply (simp only: is_quasilist_def setclass_simps)
  1.1413 -apply (intro FOL_reflections Nil_reflection Cons_reflection)  
  1.1414 +apply (intro FOL_reflections Nil_reflection Cons_reflection)
  1.1415  done
  1.1416  
  1.1417  
  1.1418 @@ -1149,19 +1151,19 @@
  1.1419  
  1.1420  subsubsection{*The Formula @{term is_tl}, Internalized*}
  1.1421  
  1.1422 -(*     "is_tl(M,xs,T) == 
  1.1423 +(*     "is_tl(M,xs,T) ==
  1.1424         (is_Nil(M,xs) --> T=xs) &
  1.1425         (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
  1.1426         (is_quasilist(M,xs) | empty(M,T))" *)
  1.1427  constdefs tl_fm :: "[i,i]=>i"
  1.1428 -    "tl_fm(xs,T) == 
  1.1429 +    "tl_fm(xs,T) ==
  1.1430         And(Implies(Nil_fm(xs), Equal(T,xs)),
  1.1431             And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(T#+2,0)))),
  1.1432                 Or(quasilist_fm(xs), empty_fm(T))))"
  1.1433  
  1.1434  lemma tl_type [TC]:
  1.1435       "[| x \<in> nat; y \<in> nat |] ==> tl_fm(x,y) \<in> formula"
  1.1436 -by (simp add: tl_fm_def) 
  1.1437 +by (simp add: tl_fm_def)
  1.1438  
  1.1439  lemma sats_tl_fm [simp]:
  1.1440     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
  1.1441 @@ -1175,11 +1177,11 @@
  1.1442  by simp
  1.1443  
  1.1444  theorem tl_reflection:
  1.1445 -     "REFLECTS[\<lambda>x. is_tl(L,f(x),g(x)), 
  1.1446 +     "REFLECTS[\<lambda>x. is_tl(L,f(x),g(x)),
  1.1447                 \<lambda>i x. is_tl(**Lset(i),f(x),g(x))]"
  1.1448  apply (simp only: is_tl_def setclass_simps)
  1.1449  apply (intro FOL_reflections Nil_reflection Cons_reflection
  1.1450 -             quasilist_reflection empty_reflection)  
  1.1451 +             quasilist_reflection empty_reflection)
  1.1452  done
  1.1453  
  1.1454  
  1.1455 @@ -1190,27 +1192,27 @@
  1.1456     [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
  1.1457           is_wfrec(L, iterates_MH(L, is_tl(L), z), memsn, u, y)),
  1.1458      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
  1.1459 -         is_wfrec(**Lset(i), 
  1.1460 -                  iterates_MH(**Lset(i), 
  1.1461 +         is_wfrec(**Lset(i),
  1.1462 +                  iterates_MH(**Lset(i),
  1.1463                            is_tl(**Lset(i)), z), memsn, u, y))]"
  1.1464 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
  1.1465 -          iterates_MH_reflection list_functor_reflection tl_reflection) 
  1.1466 +by (intro FOL_reflections function_reflections is_wfrec_reflection
  1.1467 +          iterates_MH_reflection list_functor_reflection tl_reflection)
  1.1468  
  1.1469 -lemma nth_replacement: 
  1.1470 +lemma nth_replacement:
  1.1471     "L(w) ==> iterates_replacement(L, %l t. is_tl(L,l,t), w)"
  1.1472  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
  1.1473 -apply (rule strong_replacementI) 
  1.1474 -apply (rule rallI)   
  1.1475 -apply (rule separation_CollectI) 
  1.1476 -apply (subgoal_tac "L(Memrel(succ(n)))") 
  1.1477 -apply (rule_tac A="{A,n,w,z,Memrel(succ(n))}" in subset_LsetE, blast ) 
  1.1478 +apply (rule strong_replacementI)
  1.1479 +apply (rule rallI)
  1.1480 +apply (rule separation_CollectI)
  1.1481 +apply (subgoal_tac "L(Memrel(succ(n)))")
  1.1482 +apply (rule_tac A="{A,n,w,z,Memrel(succ(n))}" in subset_LsetE, blast )
  1.1483  apply (rule ReflectsE [OF nth_replacement_Reflects], assumption)
  1.1484 -apply (drule subset_Lset_ltD, assumption) 
  1.1485 +apply (drule subset_Lset_ltD, assumption)
  1.1486  apply (erule reflection_imp_L_separation)
  1.1487    apply (simp_all add: lt_Ord2 Memrel_closed)
  1.1488 -apply (elim conjE) 
  1.1489 +apply (elim conjE)
  1.1490  apply (rule DPow_LsetI)
  1.1491 -apply (rename_tac v) 
  1.1492 +apply (rename_tac v)
  1.1493  apply (rule bex_iff_sats conj_iff_sats)+
  1.1494  apply (rule_tac env = "[u,v,A,z,w,Memrel(succ(n))]" in mem_iff_sats)
  1.1495  apply (rule sep_rules | simp)+
  1.1496 @@ -1221,27 +1223,29 @@
  1.1497  
  1.1498  
  1.1499  subsubsection{*Instantiating the locale @{text M_datatypes}*}
  1.1500 -ML
  1.1501 -{*
  1.1502 -val list_replacement1 = thm "list_replacement1"; 
  1.1503 -val list_replacement2 = thm "list_replacement2";
  1.1504 -val formula_replacement1 = thm "formula_replacement1";
  1.1505 -val formula_replacement2 = thm "formula_replacement2";
  1.1506 -val nth_replacement = thm "nth_replacement";
  1.1507 +
  1.1508 +theorem M_datatypes_axioms_L: "M_datatypes_axioms(L)"
  1.1509 +  apply (rule M_datatypes_axioms.intro)
  1.1510 +      apply (assumption | rule
  1.1511 +        list_replacement1 list_replacement2
  1.1512 +        formula_replacement1 formula_replacement2
  1.1513 +        nth_replacement)+
  1.1514 +  done
  1.1515  
  1.1516 -val m_datatypes = [list_replacement1, list_replacement2, 
  1.1517 -                   formula_replacement1, formula_replacement2, 
  1.1518 -                   nth_replacement];
  1.1519 -
  1.1520 -fun datatypes_L th =
  1.1521 -    kill_flex_triv_prems (m_datatypes MRS (wfrank_L th));
  1.1522 +theorem M_datatypes_L: "PROP M_datatypes(L)"
  1.1523 +  apply (rule M_datatypes.intro)
  1.1524 +      apply (rule M_triv_axioms_L)
  1.1525 +     apply (rule M_axioms_axioms_L)
  1.1526 +    apply (rule M_trancl_axioms_L)
  1.1527 +   apply (rule M_wfrank_axioms_L)
  1.1528 +  apply (rule M_datatypes_axioms_L)
  1.1529 +  done
  1.1530  
  1.1531 -bind_thm ("list_closed", datatypes_L (thm "M_datatypes.list_closed"));
  1.1532 -bind_thm ("formula_closed", datatypes_L (thm "M_datatypes.formula_closed"));
  1.1533 -bind_thm ("list_abs", datatypes_L (thm "M_datatypes.list_abs"));
  1.1534 -bind_thm ("formula_abs", datatypes_L (thm "M_datatypes.formula_abs"));
  1.1535 -bind_thm ("nth_abs", datatypes_L (thm "M_datatypes.nth_abs"));
  1.1536 -*}
  1.1537 +lemmas list_closed = M_datatypes.list_closed [OF M_datatypes_L]
  1.1538 +  and formula_closed = M_datatypes.formula_closed [OF M_datatypes_L]
  1.1539 +  and list_abs = M_datatypes.list_abs [OF M_datatypes_L]
  1.1540 +  and formula_abs = M_datatypes.formula_abs [OF M_datatypes_L]
  1.1541 +  and nth_abs = M_datatypes.nth_abs [OF M_datatypes_L]
  1.1542  
  1.1543  declare list_closed [intro,simp]
  1.1544  declare formula_closed [intro,simp]
  1.1545 @@ -1250,8 +1254,7 @@
  1.1546  declare nth_abs [simp]
  1.1547  
  1.1548  
  1.1549 -
  1.1550 -subsection{*@{term L} is Closed Under the Operator @{term eclose}*} 
  1.1551 +subsection{*@{term L} is Closed Under the Operator @{term eclose}*}
  1.1552  
  1.1553  subsubsection{*Instances of Replacement for @{term eclose}*}
  1.1554  
  1.1555 @@ -1260,28 +1263,28 @@
  1.1556     [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
  1.1557           is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)),
  1.1558      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
  1.1559 -         is_wfrec(**Lset(i), 
  1.1560 -                  iterates_MH(**Lset(i), big_union(**Lset(i)), A), 
  1.1561 +         is_wfrec(**Lset(i),
  1.1562 +                  iterates_MH(**Lset(i), big_union(**Lset(i)), A),
  1.1563                    memsn, u, y))]"
  1.1564 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
  1.1565 -          iterates_MH_reflection) 
  1.1566 +by (intro FOL_reflections function_reflections is_wfrec_reflection
  1.1567 +          iterates_MH_reflection)
  1.1568  
  1.1569 -lemma eclose_replacement1: 
  1.1570 +lemma eclose_replacement1:
  1.1571     "L(A) ==> iterates_replacement(L, big_union(L), A)"
  1.1572  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
  1.1573 -apply (rule strong_replacementI) 
  1.1574 +apply (rule strong_replacementI)
  1.1575  apply (rule rallI)
  1.1576 -apply (rename_tac B)   
  1.1577 -apply (rule separation_CollectI) 
  1.1578 -apply (subgoal_tac "L(Memrel(succ(n)))") 
  1.1579 -apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast ) 
  1.1580 +apply (rename_tac B)
  1.1581 +apply (rule separation_CollectI)
  1.1582 +apply (subgoal_tac "L(Memrel(succ(n)))")
  1.1583 +apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast )
  1.1584  apply (rule ReflectsE [OF eclose_replacement1_Reflects], assumption)
  1.1585 -apply (drule subset_Lset_ltD, assumption) 
  1.1586 +apply (drule subset_Lset_ltD, assumption)
  1.1587  apply (erule reflection_imp_L_separation)
  1.1588    apply (simp_all add: lt_Ord2 Memrel_closed)
  1.1589 -apply (elim conjE) 
  1.1590 +apply (elim conjE)
  1.1591  apply (rule DPow_LsetI)
  1.1592 -apply (rename_tac v) 
  1.1593 +apply (rename_tac v)
  1.1594  apply (rule bex_iff_sats conj_iff_sats)+
  1.1595  apply (rule_tac env = "[u,v,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
  1.1596  apply (rule sep_rules | simp)+
  1.1597 @@ -1298,33 +1301,33 @@
  1.1598             is_wfrec (L, iterates_MH (L, big_union(L), A),
  1.1599                                msn, u, x)),
  1.1600      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
  1.1601 -         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). 
  1.1602 +         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i).
  1.1603            successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
  1.1604 -           is_wfrec (**Lset(i), 
  1.1605 +           is_wfrec (**Lset(i),
  1.1606                   iterates_MH (**Lset(i), big_union(**Lset(i)), A),
  1.1607                       msn, u, x))]"
  1.1608 -by (intro FOL_reflections function_reflections is_wfrec_reflection 
  1.1609 -          iterates_MH_reflection) 
  1.1610 +by (intro FOL_reflections function_reflections is_wfrec_reflection
  1.1611 +          iterates_MH_reflection)
  1.1612  
  1.1613  
  1.1614 -lemma eclose_replacement2: 
  1.1615 -   "L(A) ==> strong_replacement(L, 
  1.1616 -         \<lambda>n y. n\<in>nat & 
  1.1617 +lemma eclose_replacement2:
  1.1618 +   "L(A) ==> strong_replacement(L,
  1.1619 +         \<lambda>n y. n\<in>nat &
  1.1620                 (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
  1.1621 -               is_wfrec(L, iterates_MH(L,big_union(L), A), 
  1.1622 +               is_wfrec(L, iterates_MH(L,big_union(L), A),
  1.1623                          msn, n, y)))"
  1.1624 -apply (rule strong_replacementI) 
  1.1625 +apply (rule strong_replacementI)
  1.1626  apply (rule rallI)
  1.1627 -apply (rename_tac B)   
  1.1628 -apply (rule separation_CollectI) 
  1.1629 -apply (rule_tac A="{A,B,z,nat}" in subset_LsetE) 
  1.1630 -apply (blast intro: L_nat) 
  1.1631 +apply (rename_tac B)
  1.1632 +apply (rule separation_CollectI)
  1.1633 +apply (rule_tac A="{A,B,z,nat}" in subset_LsetE)
  1.1634 +apply (blast intro: L_nat)
  1.1635  apply (rule ReflectsE [OF eclose_replacement2_Reflects], assumption)
  1.1636 -apply (drule subset_Lset_ltD, assumption) 
  1.1637 +apply (drule subset_Lset_ltD, assumption)
  1.1638  apply (erule reflection_imp_L_separation)
  1.1639    apply (simp_all add: lt_Ord2)
  1.1640  apply (rule DPow_LsetI)
  1.1641 -apply (rename_tac v) 
  1.1642 +apply (rename_tac v)
  1.1643  apply (rule bex_iff_sats conj_iff_sats)+
  1.1644  apply (rule_tac env = "[u,v,A,B,nat]" in mem_iff_sats)
  1.1645  apply (rule sep_rules | simp)+
  1.1646 @@ -1334,22 +1337,23 @@
  1.1647  
  1.1648  
  1.1649  subsubsection{*Instantiating the locale @{text M_eclose}*}
  1.1650 -ML
  1.1651 -{*
  1.1652 -val eclose_replacement1 = thm "eclose_replacement1"; 
  1.1653 -val eclose_replacement2 = thm "eclose_replacement2";
  1.1654  
  1.1655 -val m_eclose = [eclose_replacement1, eclose_replacement2];
  1.1656 +theorem M_eclose_axioms_L: "M_eclose_axioms(L)"
  1.1657 +  apply (rule M_eclose_axioms.intro)
  1.1658 +   apply (assumption | rule eclose_replacement1 eclose_replacement2)+
  1.1659 +  done
  1.1660  
  1.1661 -fun eclose_L th =
  1.1662 -    kill_flex_triv_prems (m_eclose MRS (datatypes_L th));
  1.1663 +theorem M_eclose_L: "PROP M_eclose(L)"
  1.1664 +  apply (rule M_eclose.intro)
  1.1665 +       apply (rule M_triv_axioms_L)
  1.1666 +      apply (rule M_axioms_axioms_L)
  1.1667 +     apply (rule M_trancl_axioms_L)
  1.1668 +    apply (rule M_wfrank_axioms_L)
  1.1669 +   apply (rule M_datatypes_axioms_L)
  1.1670 +  apply (rule M_eclose_axioms_L)
  1.1671 +  done
  1.1672  
  1.1673 -bind_thm ("eclose_closed", eclose_L (thm "M_eclose.eclose_closed"));
  1.1674 -bind_thm ("eclose_abs", eclose_L (thm "M_eclose.eclose_abs"));
  1.1675 -*}
  1.1676 -
  1.1677 -declare eclose_closed [intro,simp]
  1.1678 -declare eclose_abs [intro,simp]
  1.1679 -
  1.1680 +lemmas eclose_closed [intro, simp] = M_eclose.eclose_closed [OF M_eclose_L]
  1.1681 +  and eclose_abs [intro, simp] = M_eclose.eclose_abs [OF M_eclose_L]
  1.1682  
  1.1683  end