Streamlined proofs of instances of Separation
authorpaulson
Wed Sep 11 16:55:37 2002 +0200 (2002-09-11)
changeset 1356652a419210d5c
parent 13565 40e4755e57f7
child 13567 7f5bf04095bd
Streamlined proofs of instances of Separation
src/ZF/Constructible/DPow_absolute.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/Satisfies_absolute.thy
src/ZF/Constructible/Separation.thy
     1.1 --- a/src/ZF/Constructible/DPow_absolute.thy	Wed Sep 11 16:53:59 2002 +0200
     1.2 +++ b/src/ZF/Constructible/DPow_absolute.thy	Wed Sep 11 16:55:37 2002 +0200
     1.3 @@ -243,14 +243,9 @@
     1.4  lemma DPow_separation:
     1.5      "[| L(A); env \<in> list(A); p \<in> formula |]
     1.6       ==> separation(L, \<lambda>x. is_DPow_body(L,A,env,p,x))"
     1.7 -apply (subgoal_tac "L(env) & L(p)") 
     1.8 - prefer 2 apply (blast intro: transL) 
     1.9 -apply (rule separation_CollectI)
    1.10 -apply (rule_tac A="{A,env,p,z}" in subset_LsetE, blast)
    1.11 -apply (rule ReflectsE [OF DPow_body_reflection], assumption)
    1.12 -apply (drule subset_Lset_ltD, assumption)
    1.13 -apply (erule reflection_imp_L_separation)
    1.14 -  apply (simp_all add: lt_Ord2)
    1.15 +apply (rule gen_separation [OF DPow_body_reflection, of "{A,env,p}"], 
    1.16 +       blast intro: transL)
    1.17 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    1.18  apply (rule DPow_LsetI)
    1.19  apply (rule_tac env = "[x,A,env,p]" in DPow_body_iff_sats)
    1.20  apply (rule sep_rules | simp)+
    1.21 @@ -282,19 +277,14 @@
    1.22                    pair(L,env,p,ep) & 
    1.23                    is_Collect(L, A, \<lambda>x. is_DPow_body(L,A,env,p,x), z))"
    1.24  apply (rule strong_replacementI)
    1.25 -apply (rule rallI)
    1.26  apply (rename_tac B)
    1.27 -apply (rule separation_CollectI)
    1.28 -apply (rule_tac A="{A,B,z}" in subset_LsetE, blast)
    1.29 -apply (rule ReflectsE [OF DPow_replacement_Reflects], assumption)
    1.30 -apply (drule subset_Lset_ltD, assumption)
    1.31 -apply (erule reflection_imp_L_separation)
    1.32 -  apply (simp_all add: lt_Ord2)
    1.33 +apply (rule_tac u="{A,B}" in gen_separation [OF DPow_replacement_Reflects], 
    1.34 +       simp)
    1.35 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    1.36 +apply (unfold is_Collect_def) 
    1.37  apply (rule DPow_LsetI)
    1.38 -apply (rename_tac v)
    1.39 -apply (unfold is_Collect_def) 
    1.40  apply (rule bex_iff_sats conj_iff_sats)+
    1.41 -apply (rule_tac env = "[u,v,A,B]" in mem_iff_sats)
    1.42 +apply (rule_tac env = "[u,x,A,B]" in mem_iff_sats)
    1.43  apply (rule sep_rules mem_formula_iff_sats mem_list_iff_sats 
    1.44              DPow_body_iff_sats | simp)+
    1.45  done
    1.46 @@ -559,18 +549,12 @@
    1.47     "[|L(x); L(g)|] ==> strong_replacement(L, \<lambda>y z. transrec_body(L,g,x,y,z))"
    1.48  apply (unfold transrec_body_def)  
    1.49  apply (rule strong_replacementI) 
    1.50 -apply (rule rallI)
    1.51  apply (rename_tac B)  
    1.52 -apply (rule separation_CollectI) 
    1.53 -apply (rule_tac A="{x,g,B,z}" in subset_LsetE, blast) 
    1.54 -apply (rule ReflectsE [OF strong_rep_Reflects], assumption)
    1.55 -apply (drule subset_Lset_ltD, assumption) 
    1.56 -apply (erule reflection_imp_L_separation)
    1.57 -  apply (simp_all add: lt_Ord2)
    1.58 +apply (rule_tac u="{x,g,B}" in gen_separation [OF strong_rep_Reflects], simp)
    1.59 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    1.60  apply (rule DPow_LsetI)
    1.61 -apply (rename_tac u) 
    1.62  apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
    1.63 -apply (rule_tac env = "[v,u,x,g,B,z]" in mem_iff_sats) 
    1.64 +apply (rule_tac env = "[v,u,x,g,B]" in mem_iff_sats) 
    1.65  apply (rule sep_rules DPow'_iff_sats | simp)+
    1.66  done
    1.67  
    1.68 @@ -599,30 +583,21 @@
    1.69  done
    1.70  
    1.71  
    1.72 -
    1.73  lemma transrec_rep: 
    1.74      "[|L(j)|]
    1.75      ==> transrec_replacement(L, \<lambda>x f u. 
    1.76                \<exists>r[L]. is_Replace(L, x, transrec_body(L,f,x), r) & 
    1.77                       big_union(L, r, u), j)"
    1.78 -apply (subgoal_tac "L(Memrel(eclose({j})))")
    1.79 - prefer 2 apply simp
    1.80  apply (rule transrec_replacementI, assumption)
    1.81 +apply (unfold transrec_body_def)  
    1.82  apply (rule strong_replacementI)
    1.83 -apply (unfold transrec_body_def)  
    1.84 -apply (rule rallI)
    1.85  apply (rename_tac B)
    1.86 -apply (rule separation_CollectI)
    1.87 -apply (rule_tac A="{j,B,z,Memrel(eclose({j}))}" in subset_LsetE, blast)
    1.88 -apply (rule ReflectsE [OF transrec_rep_Reflects], assumption)
    1.89 -apply (drule subset_Lset_ltD, assumption)
    1.90 -apply (erule reflection_imp_L_separation)
    1.91 -  apply (simp_all add: lt_Ord2 Memrel_closed)
    1.92 -apply (elim conjE)
    1.93 +apply (rule_tac u="{j,B,Memrel(eclose({j}))}" 
    1.94 +         in gen_separation [OF transrec_rep_Reflects], simp)
    1.95 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    1.96  apply (rule DPow_LsetI)
    1.97 -apply (rename_tac w)
    1.98  apply (rule bex_iff_sats conj_iff_sats)+
    1.99 -apply (rule_tac env = "[v,w,j,B,Memrel(eclose({j}))]" in mem_iff_sats)
   1.100 +apply (rule_tac env = "[v,x,j,B,Memrel(eclose({j}))]" in mem_iff_sats)
   1.101  apply (rule sep_rules is_wfrec_iff_sats Replace_iff_sats DPow'_iff_sats | 
   1.102         simp)+
   1.103  done
     2.1 --- a/src/ZF/Constructible/L_axioms.thy	Wed Sep 11 16:53:59 2002 +0200
     2.2 +++ b/src/ZF/Constructible/L_axioms.thy	Wed Sep 11 16:55:37 2002 +0200
     2.3 @@ -127,7 +127,8 @@
     2.4    and successor_abs = M_trivial.successor_abs [OF M_trivial_L]
     2.5    and succ_in_M_iff = M_trivial.succ_in_M_iff [OF M_trivial_L]
     2.6    and separation_closed = M_trivial.separation_closed [OF M_trivial_L]
     2.7 -  and strong_replacementI = M_trivial.strong_replacementI [OF M_trivial_L]
     2.8 +  and strong_replacementI = 
     2.9 +      M_trivial.strong_replacementI [OF M_trivial_L, rule_format]
    2.10    and strong_replacement_closed = M_trivial.strong_replacement_closed [OF M_trivial_L]
    2.11    and RepFun_closed = M_trivial.RepFun_closed [OF M_trivial_L]
    2.12    and lam_closed = M_trivial.lam_closed [OF M_trivial_L]
    2.13 @@ -169,7 +170,6 @@
    2.14  declare successor_abs [simp]
    2.15  declare succ_in_M_iff [iff]
    2.16  declare separation_closed [intro, simp]
    2.17 -declare strong_replacementI
    2.18  declare strong_replacement_closed [intro, simp]
    2.19  declare RepFun_closed [intro, simp]
    2.20  declare lam_closed [intro, simp]
     3.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Wed Sep 11 16:53:59 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Wed Sep 11 16:55:37 2002 +0200
     3.3 @@ -71,7 +71,7 @@
     3.4         ==> rtran_closure_mem(**A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)"
     3.5  by (simp add: sats_rtran_closure_mem_fm)
     3.6  
     3.7 -theorem rtran_closure_mem_reflection:
     3.8 +lemma rtran_closure_mem_reflection:
     3.9       "REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)),
    3.10                 \<lambda>i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]"
    3.11  apply (simp only: rtran_closure_mem_def setclass_simps)
    3.12 @@ -81,15 +81,10 @@
    3.13  text{*Separation for @{term "rtrancl(r)"}.*}
    3.14  lemma rtrancl_separation:
    3.15       "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))"
    3.16 -apply (rule separation_CollectI)
    3.17 -apply (rule_tac A="{r,A,z}" in subset_LsetE, blast)
    3.18 -apply (rule ReflectsE [OF rtran_closure_mem_reflection], assumption)
    3.19 -apply (drule subset_Lset_ltD, assumption)
    3.20 -apply (erule reflection_imp_L_separation)
    3.21 -  apply (simp_all add: lt_Ord2)
    3.22 +apply (rule gen_separation [OF rtran_closure_mem_reflection, of "{r,A}"], simp)
    3.23 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    3.24  apply (rule DPow_LsetI)
    3.25 -apply (rename_tac u)
    3.26 -apply (rule_tac env = "[u,r,A]" in rtran_closure_mem_iff_sats)
    3.27 +apply (rule_tac env = "[x,r,A]" in rtran_closure_mem_iff_sats)
    3.28  apply (rule sep_rules | simp)+
    3.29  done
    3.30  
    3.31 @@ -183,22 +178,16 @@
    3.32  by (intro FOL_reflections function_reflections fun_plus_reflections
    3.33            tran_closure_reflection)
    3.34  
    3.35 -
    3.36  lemma wellfounded_trancl_separation:
    3.37           "[| L(r); L(Z) |] ==>
    3.38            separation (L, \<lambda>x.
    3.39                \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
    3.40                 w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)"
    3.41 -apply (rule separation_CollectI)
    3.42 -apply (rule_tac A="{r,Z,z}" in subset_LsetE, blast)
    3.43 -apply (rule ReflectsE [OF wellfounded_trancl_reflects], assumption)
    3.44 -apply (drule subset_Lset_ltD, assumption)
    3.45 -apply (erule reflection_imp_L_separation)
    3.46 -  apply (simp_all add: lt_Ord2)
    3.47 +apply (rule gen_separation [OF wellfounded_trancl_reflects, of "{r,Z}"], simp)
    3.48 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    3.49  apply (rule DPow_LsetI)
    3.50 -apply (rename_tac u)
    3.51  apply (rule bex_iff_sats conj_iff_sats)+
    3.52 -apply (rule_tac env = "[w,u,r,Z]" in mem_iff_sats)
    3.53 +apply (rule_tac env = "[w,x,r,Z]" in mem_iff_sats)
    3.54  apply (rule sep_rules tran_closure_iff_sats | simp)+
    3.55  done
    3.56  
    3.57 @@ -251,17 +240,10 @@
    3.58       "L(r) ==>
    3.59        separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
    3.60           ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))"
    3.61 -apply (rule separation_CollectI)
    3.62 -apply (rule_tac A="{r,z}" in subset_LsetE, blast)
    3.63 -apply (rule ReflectsE [OF wfrank_Reflects], assumption)
    3.64 -apply (drule subset_Lset_ltD, assumption)
    3.65 -apply (erule reflection_imp_L_separation)
    3.66 -  apply (simp_all add: lt_Ord2, clarify)
    3.67 +apply (rule gen_separation [OF wfrank_Reflects], simp)
    3.68  apply (rule DPow_LsetI)
    3.69 -apply (rename_tac u)
    3.70  apply (rule ball_iff_sats imp_iff_sats)+
    3.71 -apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
    3.72 -apply (rule sep_rules | simp)+
    3.73 +apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats)
    3.74  apply (rule sep_rules is_recfun_iff_sats | simp)+
    3.75  done
    3.76  
    3.77 @@ -282,7 +264,6 @@
    3.78  by (intro FOL_reflections function_reflections fun_plus_reflections
    3.79               is_recfun_reflection tran_closure_reflection)
    3.80  
    3.81 -
    3.82  lemma wfrank_strong_replacement:
    3.83       "L(r) ==>
    3.84        strong_replacement(L, \<lambda>x z.
    3.85 @@ -291,19 +272,14 @@
    3.86                          M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
    3.87                          is_range(L,f,y)))"
    3.88  apply (rule strong_replacementI)
    3.89 -apply (rule rallI)
    3.90 -apply (rename_tac B)
    3.91 -apply (rule separation_CollectI)
    3.92 -apply (rule_tac A="{B,r,z}" in subset_LsetE, blast)
    3.93 -apply (rule ReflectsE [OF wfrank_replacement_Reflects], assumption)
    3.94 -apply (drule subset_Lset_ltD, assumption)
    3.95 -apply (erule reflection_imp_L_separation)
    3.96 -  apply (simp_all add: lt_Ord2)
    3.97 +apply (rule_tac u="{r,A}" in gen_separation [OF wfrank_replacement_Reflects], 
    3.98 +       simp)
    3.99 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   3.100  apply (rule DPow_LsetI)
   3.101 -apply (rename_tac u)
   3.102  apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+
   3.103 -apply (rule_tac env = "[x,u,B,r]" in mem_iff_sats)
   3.104 -apply (rule sep_rules list.intros app_type tran_closure_iff_sats is_recfun_iff_sats | simp)+
   3.105 +apply (rule_tac env = "[x,z,A,r]" in mem_iff_sats)
   3.106 +apply (rule sep_rules list.intros app_type tran_closure_iff_sats 
   3.107 +            is_recfun_iff_sats | simp)+
   3.108  done
   3.109  
   3.110  
   3.111 @@ -332,16 +308,10 @@
   3.112               is_range(L,f,rangef) -->
   3.113               M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
   3.114               ordinal(L,rangef)))"
   3.115 -apply (rule separation_CollectI)
   3.116 -apply (rule_tac A="{r,z}" in subset_LsetE, blast)
   3.117 -apply (rule ReflectsE [OF Ord_wfrank_Reflects], assumption)
   3.118 -apply (drule subset_Lset_ltD, assumption)
   3.119 -apply (erule reflection_imp_L_separation)
   3.120 -  apply (simp_all add: lt_Ord2, clarify)
   3.121 +apply (rule gen_separation [OF Ord_wfrank_Reflects], simp)
   3.122  apply (rule DPow_LsetI)
   3.123 -apply (rename_tac u)
   3.124  apply (rule ball_iff_sats imp_iff_sats)+
   3.125 -apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
   3.126 +apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats)
   3.127  apply (rule sep_rules is_recfun_iff_sats | simp)+
   3.128  done
   3.129  
   3.130 @@ -406,21 +376,14 @@
   3.131     "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)"
   3.132  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
   3.133  apply (rule strong_replacementI)
   3.134 -apply (rule rallI)
   3.135  apply (rename_tac B)
   3.136 -apply (rule separation_CollectI)
   3.137 -apply (insert nonempty)
   3.138 -apply (subgoal_tac "L(Memrel(succ(n)))")
   3.139 -apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast)
   3.140 -apply (rule ReflectsE [OF list_replacement1_Reflects], assumption)
   3.141 -apply (drule subset_Lset_ltD, assumption)
   3.142 -apply (erule reflection_imp_L_separation)
   3.143 -  apply (simp_all add: lt_Ord2 Memrel_closed)
   3.144 -apply (elim conjE)
   3.145 +apply (rule_tac u="{B,A,n,0,Memrel(succ(n))}" 
   3.146 +         in gen_separation [OF list_replacement1_Reflects], 
   3.147 +       simp add: nonempty)
   3.148 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   3.149  apply (rule DPow_LsetI)
   3.150 -apply (rename_tac v)
   3.151  apply (rule bex_iff_sats conj_iff_sats)+
   3.152 -apply (rule_tac env = "[u,v,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
   3.153 +apply (rule_tac env = "[u,x,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
   3.154  apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
   3.155              is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   3.156  done
   3.157 @@ -449,20 +412,14 @@
   3.158                 is_wfrec(L, iterates_MH(L,is_list_functor(L,A), 0),
   3.159                          msn, n, y)))"
   3.160  apply (rule strong_replacementI)
   3.161 -apply (rule rallI)
   3.162  apply (rename_tac B)
   3.163 -apply (rule separation_CollectI)
   3.164 -apply (insert nonempty)
   3.165 -apply (rule_tac A="{A,B,z,0,nat}" in subset_LsetE)
   3.166 -apply (blast intro: L_nat)
   3.167 -apply (rule ReflectsE [OF list_replacement2_Reflects], assumption)
   3.168 -apply (drule subset_Lset_ltD, assumption)
   3.169 -apply (erule reflection_imp_L_separation)
   3.170 -  apply (simp_all add: lt_Ord2)
   3.171 +apply (rule_tac u="{A,B,0,nat}" 
   3.172 +         in gen_separation [OF list_replacement2_Reflects], 
   3.173 +       simp add: L_nat nonempty)
   3.174 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   3.175  apply (rule DPow_LsetI)
   3.176 -apply (rename_tac v)
   3.177  apply (rule bex_iff_sats conj_iff_sats)+
   3.178 -apply (rule_tac env = "[u,v,A,B,0,nat]" in mem_iff_sats)
   3.179 +apply (rule_tac env = "[u,x,A,B,0,nat]" in mem_iff_sats)
   3.180  apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
   3.181              is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   3.182  done
   3.183 @@ -487,20 +444,14 @@
   3.184     "iterates_replacement(L, is_formula_functor(L), 0)"
   3.185  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
   3.186  apply (rule strong_replacementI)
   3.187 -apply (rule rallI)
   3.188  apply (rename_tac B)
   3.189 -apply (rule separation_CollectI)
   3.190 -apply (insert nonempty)
   3.191 -apply (subgoal_tac "L(Memrel(succ(n)))")
   3.192 -apply (rule_tac A="{B,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast)
   3.193 -apply (rule ReflectsE [OF formula_replacement1_Reflects], assumption)
   3.194 -apply (drule subset_Lset_ltD, assumption)
   3.195 -apply (erule reflection_imp_L_separation)
   3.196 -  apply (simp_all add: lt_Ord2 Memrel_closed)
   3.197 +apply (rule_tac u="{B,n,0,Memrel(succ(n))}" 
   3.198 +         in gen_separation [OF formula_replacement1_Reflects], 
   3.199 +       simp add: nonempty)
   3.200 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   3.201  apply (rule DPow_LsetI)
   3.202 -apply (rename_tac v)
   3.203  apply (rule bex_iff_sats conj_iff_sats)+
   3.204 -apply (rule_tac env = "[u,v,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
   3.205 +apply (rule_tac env = "[u,x,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
   3.206  apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
   3.207              is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   3.208  done
   3.209 @@ -528,20 +479,14 @@
   3.210                 is_wfrec(L, iterates_MH(L,is_formula_functor(L), 0),
   3.211                          msn, n, y)))"
   3.212  apply (rule strong_replacementI)
   3.213 -apply (rule rallI)
   3.214  apply (rename_tac B)
   3.215 -apply (rule separation_CollectI)
   3.216 -apply (insert nonempty)
   3.217 -apply (rule_tac A="{B,z,0,nat}" in subset_LsetE)
   3.218 -apply (blast intro: L_nat)
   3.219 -apply (rule ReflectsE [OF formula_replacement2_Reflects], assumption)
   3.220 -apply (drule subset_Lset_ltD, assumption)
   3.221 -apply (erule reflection_imp_L_separation)
   3.222 -  apply (simp_all add: lt_Ord2)
   3.223 +apply (rule_tac u="{B,0,nat}" 
   3.224 +         in gen_separation [OF formula_replacement2_Reflects], 
   3.225 +       simp add: nonempty L_nat)
   3.226 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   3.227  apply (rule DPow_LsetI)
   3.228 -apply (rename_tac v)
   3.229  apply (rule bex_iff_sats conj_iff_sats)+
   3.230 -apply (rule_tac env = "[u,v,B,0,nat]" in mem_iff_sats)
   3.231 +apply (rule_tac env = "[u,x,B,0,nat]" in mem_iff_sats)
   3.232  apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
   3.233              is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   3.234  done
   3.235 @@ -609,25 +554,18 @@
   3.236     "L(w) ==> iterates_replacement(L, %l t. is_tl(L,l,t), w)"
   3.237  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
   3.238  apply (rule strong_replacementI)
   3.239 -apply (rule rallI)
   3.240 -apply (rule separation_CollectI)
   3.241 -apply (subgoal_tac "L(Memrel(succ(n)))")
   3.242 -apply (rule_tac A="{A,n,w,z,Memrel(succ(n))}" in subset_LsetE, blast)
   3.243 -apply (rule ReflectsE [OF nth_replacement_Reflects], assumption)
   3.244 -apply (drule subset_Lset_ltD, assumption)
   3.245 -apply (erule reflection_imp_L_separation)
   3.246 -  apply (simp_all add: lt_Ord2 Memrel_closed)
   3.247 -apply (elim conjE)
   3.248 +apply (rule_tac u="{A,n,w,Memrel(succ(n))}" 
   3.249 +         in gen_separation [OF nth_replacement_Reflects], 
   3.250 +       simp add: nonempty)
   3.251 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   3.252  apply (rule DPow_LsetI)
   3.253 -apply (rename_tac v)
   3.254  apply (rule bex_iff_sats conj_iff_sats)+
   3.255 -apply (rule_tac env = "[u,v,A,z,w,Memrel(succ(n))]" in mem_iff_sats)
   3.256 +apply (rule_tac env = "[u,x,A,w,Memrel(succ(n))]" in mem_iff_sats)
   3.257  apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats
   3.258              is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   3.259  done
   3.260  
   3.261  
   3.262 -
   3.263  subsubsection{*Instantiating the locale @{text M_datatypes}*}
   3.264  
   3.265  lemma M_datatypes_axioms_L: "M_datatypes_axioms(L)"
   3.266 @@ -676,20 +614,13 @@
   3.267     "L(A) ==> iterates_replacement(L, big_union(L), A)"
   3.268  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
   3.269  apply (rule strong_replacementI)
   3.270 -apply (rule rallI)
   3.271  apply (rename_tac B)
   3.272 -apply (rule separation_CollectI)
   3.273 -apply (subgoal_tac "L(Memrel(succ(n)))")
   3.274 -apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast)
   3.275 -apply (rule ReflectsE [OF eclose_replacement1_Reflects], assumption)
   3.276 -apply (drule subset_Lset_ltD, assumption)
   3.277 -apply (erule reflection_imp_L_separation)
   3.278 -  apply (simp_all add: lt_Ord2 Memrel_closed)
   3.279 -apply (elim conjE)
   3.280 +apply (rule_tac u="{B,A,n,Memrel(succ(n))}" 
   3.281 +         in gen_separation [OF eclose_replacement1_Reflects], simp)
   3.282 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   3.283  apply (rule DPow_LsetI)
   3.284 -apply (rename_tac v)
   3.285  apply (rule bex_iff_sats conj_iff_sats)+
   3.286 -apply (rule_tac env = "[u,v,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
   3.287 +apply (rule_tac env = "[u,x,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
   3.288  apply (rule sep_rules iterates_MH_iff_sats is_nat_case_iff_sats
   3.289               is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
   3.290  done
   3.291 @@ -718,19 +649,13 @@
   3.292                 is_wfrec(L, iterates_MH(L,big_union(L), A),
   3.293                          msn, n, y)))"
   3.294  apply (rule strong_replacementI)
   3.295 -apply (rule rallI)
   3.296  apply (rename_tac B)
   3.297 -apply (rule separation_CollectI)
   3.298 -apply (rule_tac A="{A,B,z,nat}" in subset_LsetE)
   3.299 -apply (blast intro: L_nat)
   3.300 -apply (rule ReflectsE [OF eclose_replacement2_Reflects], assumption)
   3.301 -apply (drule subset_Lset_ltD, assumption)
   3.302 -apply (erule reflection_imp_L_separation)
   3.303 -  apply (simp_all add: lt_Ord2)
   3.304 +apply (rule_tac u="{A,B,nat}" 
   3.305 +         in gen_separation [OF eclose_replacement2_Reflects], simp add: L_nat)
   3.306 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   3.307  apply (rule DPow_LsetI)
   3.308 -apply (rename_tac v)
   3.309  apply (rule bex_iff_sats conj_iff_sats)+
   3.310 -apply (rule_tac env = "[u,v,A,B,nat]" in mem_iff_sats)
   3.311 +apply (rule_tac env = "[u,x,A,B,nat]" in mem_iff_sats)
   3.312  apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats
   3.313                is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
   3.314  done
     4.1 --- a/src/ZF/Constructible/Satisfies_absolute.thy	Wed Sep 11 16:53:59 2002 +0200
     4.2 +++ b/src/ZF/Constructible/Satisfies_absolute.thy	Wed Sep 11 16:55:37 2002 +0200
     4.3 @@ -823,24 +823,16 @@
     4.4                env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
     4.5                is_bool_of_o(L, nx \<in> ny, bo) &
     4.6                pair(L, env, bo, z))"
     4.7 -apply (frule list_closed) 
     4.8 -apply (rule strong_replacementI) 
     4.9 -apply (rule rallI)
    4.10 -apply (rename_tac B)  
    4.11 -apply (rule separation_CollectI) 
    4.12 -apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast) 
    4.13 -apply (rule ReflectsE [OF Member_Reflects], assumption)
    4.14 -apply (drule subset_Lset_ltD, assumption) 
    4.15 -apply (erule reflection_imp_L_separation)
    4.16 -  apply (simp_all add: lt_Ord2)
    4.17 -apply (simp add: is_nth_def is_wfrec_def is_bool_of_o_def)
    4.18 +apply (rule strong_replacementI)
    4.19 +apply (rename_tac B)
    4.20 +apply (rule_tac u="{list(A),B,x,y}" 
    4.21 +         in gen_separation [OF Member_Reflects], 
    4.22 +       simp add: nat_into_M list_closed)
    4.23 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    4.24  apply (rule DPow_LsetI)
    4.25 -apply (rename_tac u) 
    4.26 -apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
    4.27 -apply (rule_tac env = "[v,u,list(A),B,x,y,z]" in mem_iff_sats) 
    4.28 -apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats
    4.29 -            is_recfun_iff_sats hd_iff_sats tl_iff_sats quasinat_iff_sats
    4.30 -     | simp)+
    4.31 +apply (rule bex_iff_sats conj_iff_sats)+
    4.32 +apply (rule_tac env = "[v,u,list(A),B,x,y]" in mem_iff_sats) 
    4.33 +apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
    4.34  done
    4.35  
    4.36  
    4.37 @@ -865,24 +857,16 @@
    4.38                env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
    4.39                is_bool_of_o(L, nx = ny, bo) &
    4.40                pair(L, env, bo, z))"
    4.41 -apply (frule list_closed) 
    4.42 -apply (rule strong_replacementI) 
    4.43 -apply (rule rallI)
    4.44 -apply (rename_tac B)  
    4.45 -apply (rule separation_CollectI) 
    4.46 -apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast) 
    4.47 -apply (rule ReflectsE [OF Equal_Reflects], assumption)
    4.48 -apply (drule subset_Lset_ltD, assumption) 
    4.49 -apply (erule reflection_imp_L_separation)
    4.50 -  apply (simp_all add: lt_Ord2)
    4.51 -apply (simp add: is_nth_def is_wfrec_def is_bool_of_o_def)
    4.52 +apply (rule strong_replacementI)
    4.53 +apply (rename_tac B)
    4.54 +apply (rule_tac u="{list(A),B,x,y}" 
    4.55 +         in gen_separation [OF Equal_Reflects], 
    4.56 +       simp add: nat_into_M list_closed)
    4.57 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    4.58  apply (rule DPow_LsetI)
    4.59 -apply (rename_tac u) 
    4.60 -apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
    4.61 -apply (rule_tac env = "[v,u,list(A),B,x,y,z]" in mem_iff_sats) 
    4.62 -apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats
    4.63 -            is_recfun_iff_sats hd_iff_sats tl_iff_sats quasinat_iff_sats
    4.64 -     | simp)+
    4.65 +apply (rule bex_iff_sats conj_iff_sats)+
    4.66 +apply (rule_tac env = "[v,u,list(A),B,x,y]" in mem_iff_sats) 
    4.67 +apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
    4.68  done
    4.69  
    4.70  subsubsection{*The @{term "Nand"} Case*}
    4.71 @@ -909,22 +893,15 @@
    4.72                 fun_apply(L,rp,env,rpe) & fun_apply(L,rq,env,rqe) & 
    4.73                 is_and(L,rpe,rqe,andpq) & is_not(L,andpq,notpq) & 
    4.74                 env \<in> list(A) & pair(L, env, notpq, z))"
    4.75 -apply (frule list_closed) 
    4.76 -apply (rule strong_replacementI) 
    4.77 -apply (rule rallI)
    4.78 -apply (rename_tac B)  
    4.79 -apply (rule separation_CollectI) 
    4.80 -apply (rule_tac A="{list(A),B,rp,rq,z}" in subset_LsetE, blast) 
    4.81 -apply (rule ReflectsE [OF Nand_Reflects], assumption)
    4.82 -apply (drule subset_Lset_ltD, assumption) 
    4.83 -apply (erule reflection_imp_L_separation)
    4.84 -  apply (simp_all add: lt_Ord2)
    4.85 -apply (simp add: is_and_def is_not_def)
    4.86 +apply (rule strong_replacementI)
    4.87 +apply (rename_tac B)
    4.88 +apply (rule_tac u="{list(A),B,rp,rq}" in gen_separation [OF Nand_Reflects],
    4.89 +       simp add: list_closed)
    4.90 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    4.91  apply (rule DPow_LsetI)
    4.92 -apply (rename_tac v) 
    4.93 -apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
    4.94 -apply (rule_tac env = "[u,v,list(A),B,rp,rq,z]" in mem_iff_sats) 
    4.95 -apply (rule sep_rules | simp)+
    4.96 +apply (rule bex_iff_sats conj_iff_sats)+
    4.97 +apply (rule_tac env = "[u,x,list(A),B,rp,rq]" in mem_iff_sats) 
    4.98 +apply (rule sep_rules is_and_iff_sats is_not_iff_sats | simp)+
    4.99  done
   4.100  
   4.101  
   4.102 @@ -958,22 +935,15 @@
   4.103  			       fun_apply(L,rp,co,rpco) --> number1(L, rpco), 
   4.104                              bo) &
   4.105  	      pair(L,env,bo,z))"
   4.106 -apply (frule list_closed) 
   4.107 -apply (rule strong_replacementI) 
   4.108 -apply (rule rallI)
   4.109 -apply (rename_tac B)  
   4.110 -apply (rule separation_CollectI) 
   4.111 -apply (rule_tac A="{A,list(A),B,rp,z}" in subset_LsetE, blast) 
   4.112 -apply (rule ReflectsE [OF Forall_Reflects], assumption)
   4.113 -apply (drule subset_Lset_ltD, assumption) 
   4.114 -apply (erule reflection_imp_L_separation)
   4.115 -  apply (simp_all add: lt_Ord2)
   4.116 -apply (simp add: is_bool_of_o_def)
   4.117 +apply (rule strong_replacementI)
   4.118 +apply (rename_tac B)
   4.119 +apply (rule_tac u="{A,list(A),B,rp}" in gen_separation [OF Forall_Reflects],
   4.120 +       simp add: list_closed)
   4.121 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   4.122  apply (rule DPow_LsetI)
   4.123 -apply (rename_tac v) 
   4.124 -apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
   4.125 -apply (rule_tac env = "[u,v,A,list(A),B,rp,z]" in mem_iff_sats)
   4.126 -apply (rule sep_rules Cons_iff_sats | simp)+
   4.127 +apply (rule bex_iff_sats conj_iff_sats)+
   4.128 +apply (rule_tac env = "[u,x,A,list(A),B,rp]" in mem_iff_sats)
   4.129 +apply (rule sep_rules is_bool_of_o_iff_sats Cons_iff_sats | simp)+
   4.130  done
   4.131  
   4.132  subsubsection{*The @{term "transrec_replacement"} Case*}
   4.133 @@ -989,24 +959,16 @@
   4.134  lemma formula_rec_replacement: 
   4.135        --{*For the @{term transrec}*}
   4.136     "[|n \<in> nat; L(A)|] ==> transrec_replacement(L, satisfies_MH(L,A), n)"
   4.137 -apply (subgoal_tac "L(Memrel(eclose({n})))")
   4.138 - prefer 2 apply (simp add: nat_into_M) 
   4.139 -apply (rule transrec_replacementI) 
   4.140 -apply (simp add: nat_into_M) 
   4.141 +apply (rule transrec_replacementI, simp add: nat_into_M) 
   4.142  apply (rule strong_replacementI)
   4.143 -apply (rule rallI)
   4.144  apply (rename_tac B)
   4.145 -apply (rule separation_CollectI)
   4.146 -apply (rule_tac A="{B,A,n,z,Memrel(eclose({n}))}" in subset_LsetE, blast)
   4.147 -apply (rule ReflectsE [OF formula_rec_replacement_Reflects], assumption)
   4.148 -apply (drule subset_Lset_ltD, assumption)
   4.149 -apply (erule reflection_imp_L_separation)
   4.150 -  apply (simp_all add: lt_Ord2 Memrel_closed)
   4.151 -apply (elim conjE)
   4.152 +apply (rule_tac u="{B,A,n,Memrel(eclose({n}))}"
   4.153 +         in gen_separation [OF formula_rec_replacement_Reflects],
   4.154 +       simp add: nat_into_M)
   4.155 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   4.156  apply (rule DPow_LsetI)
   4.157 -apply (rename_tac v)
   4.158  apply (rule bex_iff_sats conj_iff_sats)+
   4.159 -apply (rule_tac env = "[u,v,A,n,B,Memrel(eclose({n}))]" in mem_iff_sats)
   4.160 +apply (rule_tac env = "[u,x,A,n,B,Memrel(eclose({n}))]" in mem_iff_sats)
   4.161  apply (rule sep_rules satisfies_MH_iff_sats is_wfrec_iff_sats | simp)+
   4.162  done
   4.163  
   4.164 @@ -1045,19 +1007,13 @@
   4.165                                    satisfies_is_d(L,A,g), x, c) &
   4.166               pair(L, x, c, y)))" 
   4.167  apply (rule strong_replacementI)
   4.168 -apply (rule rallI)
   4.169  apply (rename_tac B)
   4.170 -apply (rule separation_CollectI)
   4.171 -apply (rule_tac A="{B,A,g,z}" in subset_LsetE, blast)
   4.172 -apply (rule ReflectsE [OF formula_rec_lambda_replacement_Reflects], assumption)
   4.173 -apply (drule subset_Lset_ltD, assumption)
   4.174 -apply (erule reflection_imp_L_separation)
   4.175 -  apply (simp_all add: lt_Ord2 Memrel_closed)
   4.176 -apply (elim conjE)
   4.177 +apply (rule_tac u="{B,A,g}"
   4.178 +         in gen_separation [OF formula_rec_lambda_replacement_Reflects], simp)
   4.179 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   4.180  apply (rule DPow_LsetI)
   4.181 -apply (rename_tac v)
   4.182  apply (rule bex_iff_sats conj_iff_sats)+
   4.183 -apply (rule_tac env = "[u,v,A,g,B]" in mem_iff_sats)
   4.184 +apply (rule_tac env = "[u,x,A,g,B]" in mem_iff_sats)
   4.185  apply (rule sep_rules mem_formula_iff_sats
   4.186            formula_case_iff_sats satisfies_is_a_iff_sats
   4.187            satisfies_is_b_iff_sats satisfies_is_c_iff_sats
     5.1 --- a/src/ZF/Constructible/Separation.thy	Wed Sep 11 16:53:59 2002 +0200
     5.2 +++ b/src/ZF/Constructible/Separation.thy	Wed Sep 11 16:55:37 2002 +0200
     5.3 @@ -51,6 +51,24 @@
     5.4  apply (simp add: Lset_succ Collect_conj_in_DPow_Lset)
     5.5  done
     5.6  
     5.7 +text{*Encapsulates the standard proof script for proving instances of 
     5.8 +Separation.  Typically @{term u} is a finite enumeration.*}
     5.9 +lemma gen_separation:
    5.10 + assumes reflection: "REFLECTS [P,Q]"
    5.11 +     and Lu:         "L(u)"
    5.12 +     and collI: "!!j. u \<in> Lset(j)
    5.13 +                \<Longrightarrow> Collect(Lset(j), Q(j)) \<in> DPow(Lset(j))"
    5.14 + shows "separation(L,P)"
    5.15 +apply (rule separation_CollectI)
    5.16 +apply (rule_tac A="{u,z}" in subset_LsetE, blast intro: Lu)
    5.17 +apply (rule ReflectsE [OF reflection], assumption)
    5.18 +apply (drule subset_Lset_ltD, assumption)
    5.19 +apply (erule reflection_imp_L_separation)
    5.20 +  apply (simp_all add: lt_Ord2, clarify)
    5.21 +apply (rule collI)
    5.22 +apply assumption;  
    5.23 +done
    5.24 +
    5.25  
    5.26  subsection{*Separation for Intersection*}
    5.27  
    5.28 @@ -61,12 +79,7 @@
    5.29  
    5.30  lemma Inter_separation:
    5.31       "L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A --> x\<in>y)"
    5.32 -apply (rule separation_CollectI)
    5.33 -apply (rule_tac A="{A,z}" in subset_LsetE, blast)
    5.34 -apply (rule ReflectsE [OF Inter_Reflects], assumption)
    5.35 -apply (drule subset_Lset_ltD, assumption)
    5.36 -apply (erule reflection_imp_L_separation)
    5.37 -  apply (simp_all add: lt_Ord2, clarify)
    5.38 +apply (rule gen_separation [OF Inter_Reflects], simp)
    5.39  apply (rule DPow_LsetI)
    5.40  apply (rule ball_iff_sats)
    5.41  apply (rule imp_iff_sats)
    5.42 @@ -83,13 +96,8 @@
    5.43  
    5.44  lemma Diff_separation:
    5.45       "L(B) ==> separation(L, \<lambda>x. x \<notin> B)"
    5.46 -apply (rule separation_CollectI) 
    5.47 -apply (rule_tac A="{B,z}" in subset_LsetE, blast) 
    5.48 -apply (rule ReflectsE [OF Diff_Reflects], assumption)
    5.49 -apply (drule subset_Lset_ltD, assumption) 
    5.50 -apply (erule reflection_imp_L_separation)
    5.51 -  apply (simp_all add: lt_Ord2, clarify)
    5.52 -apply (rule DPow_LsetI) 
    5.53 +apply (rule gen_separation [OF Diff_Reflects], simp)
    5.54 +apply (rule DPow_LsetI)
    5.55  apply (rule not_iff_sats) 
    5.56  apply (rule_tac env="[x,B]" in mem_iff_sats)
    5.57  apply (rule sep_rules | simp)+
    5.58 @@ -106,17 +114,12 @@
    5.59  lemma cartprod_separation:
    5.60       "[| L(A); L(B) |]
    5.61        ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)))"
    5.62 -apply (rule separation_CollectI)
    5.63 -apply (rule_tac A="{A,B,z}" in subset_LsetE, blast)
    5.64 -apply (rule ReflectsE [OF cartprod_Reflects], assumption)
    5.65 -apply (drule subset_Lset_ltD, assumption)
    5.66 -apply (erule reflection_imp_L_separation)
    5.67 -  apply (simp_all add: lt_Ord2, clarify)
    5.68 +apply (rule gen_separation [OF cartprod_Reflects, of "{A,B}"], simp)
    5.69 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    5.70  apply (rule DPow_LsetI)
    5.71 -apply (rename_tac u)
    5.72  apply (rule bex_iff_sats)
    5.73  apply (rule conj_iff_sats)
    5.74 -apply (rule_tac i=0 and j=2 and env="[x,u,A,B]" in mem_iff_sats, simp_all)
    5.75 +apply (rule_tac i=0 and j=2 and env="[x,z,A,B]" in mem_iff_sats, simp_all)
    5.76  apply (rule sep_rules | simp)+
    5.77  done
    5.78  
    5.79 @@ -130,12 +133,8 @@
    5.80  lemma image_separation:
    5.81       "[| L(A); L(r) |]
    5.82        ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)))"
    5.83 -apply (rule separation_CollectI)
    5.84 -apply (rule_tac A="{A,r,z}" in subset_LsetE, blast)
    5.85 -apply (rule ReflectsE [OF image_Reflects], assumption)
    5.86 -apply (drule subset_Lset_ltD, assumption)
    5.87 -apply (erule reflection_imp_L_separation)
    5.88 -  apply (simp_all add: lt_Ord2, clarify)
    5.89 +apply (rule gen_separation [OF image_Reflects, of "{A,r}"], simp)
    5.90 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    5.91  apply (rule DPow_LsetI)
    5.92  apply (rule bex_iff_sats)
    5.93  apply (rule conj_iff_sats)
    5.94 @@ -155,17 +154,11 @@
    5.95  lemma converse_separation:
    5.96       "L(r) ==> separation(L,
    5.97           \<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)))"
    5.98 -apply (rule separation_CollectI)
    5.99 -apply (rule_tac A="{r,z}" in subset_LsetE, blast)
   5.100 -apply (rule ReflectsE [OF converse_Reflects], assumption)
   5.101 -apply (drule subset_Lset_ltD, assumption)
   5.102 -apply (erule reflection_imp_L_separation)
   5.103 -  apply (simp_all add: lt_Ord2, clarify)
   5.104 +apply (rule gen_separation [OF converse_Reflects], simp)
   5.105  apply (rule DPow_LsetI)
   5.106 -apply (rename_tac u)
   5.107  apply (rule bex_iff_sats)
   5.108  apply (rule conj_iff_sats)
   5.109 -apply (rule_tac i=0 and j=2 and env="[p,u,r]" in mem_iff_sats, simp_all)
   5.110 +apply (rule_tac i=0 and j=2 and env="[p,z,r]" in mem_iff_sats, simp_all)
   5.111  apply (rule sep_rules | simp)+
   5.112  done
   5.113  
   5.114 @@ -179,17 +172,11 @@
   5.115  
   5.116  lemma restrict_separation:
   5.117     "L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))"
   5.118 -apply (rule separation_CollectI)
   5.119 -apply (rule_tac A="{A,z}" in subset_LsetE, blast)
   5.120 -apply (rule ReflectsE [OF restrict_Reflects], assumption)
   5.121 -apply (drule subset_Lset_ltD, assumption)
   5.122 -apply (erule reflection_imp_L_separation)
   5.123 -  apply (simp_all add: lt_Ord2, clarify)
   5.124 +apply (rule gen_separation [OF restrict_Reflects], simp)
   5.125  apply (rule DPow_LsetI)
   5.126 -apply (rename_tac u)
   5.127  apply (rule bex_iff_sats)
   5.128  apply (rule conj_iff_sats)
   5.129 -apply (rule_tac i=0 and j=2 and env="[x,u,A]" in mem_iff_sats, simp_all)
   5.130 +apply (rule_tac i=0 and j=2 and env="[x,z,A]" in mem_iff_sats, simp_all)
   5.131  apply (rule sep_rules | simp)+
   5.132  done
   5.133  
   5.134 @@ -210,18 +197,12 @@
   5.135        ==> separation(L, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
   5.136                    pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
   5.137                    xy\<in>s & yz\<in>r)"
   5.138 -apply (rule separation_CollectI)
   5.139 -apply (rule_tac A="{r,s,z}" in subset_LsetE, blast)
   5.140 -apply (rule ReflectsE [OF comp_Reflects], assumption)
   5.141 -apply (drule subset_Lset_ltD, assumption)
   5.142 -apply (erule reflection_imp_L_separation)
   5.143 -  apply (simp_all add: lt_Ord2, clarify)
   5.144 +apply (rule gen_separation [OF comp_Reflects, of "{r,s}"], simp)
   5.145 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   5.146  apply (rule DPow_LsetI)
   5.147 -apply (rename_tac u)
   5.148  apply (rule bex_iff_sats)+
   5.149 -apply (rename_tac x y z)
   5.150  apply (rule conj_iff_sats)
   5.151 -apply (rule_tac env="[z,y,x,u,r,s]" in pair_iff_sats)
   5.152 +apply (rule_tac env="[z,y,x,xz,r,s]" in pair_iff_sats)
   5.153  apply (rule sep_rules | simp)+
   5.154  done
   5.155  
   5.156 @@ -234,17 +215,12 @@
   5.157  
   5.158  lemma pred_separation:
   5.159       "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"
   5.160 -apply (rule separation_CollectI)
   5.161 -apply (rule_tac A="{r,x,z}" in subset_LsetE, blast)
   5.162 -apply (rule ReflectsE [OF pred_Reflects], assumption)
   5.163 -apply (drule subset_Lset_ltD, assumption)
   5.164 -apply (erule reflection_imp_L_separation)
   5.165 -  apply (simp_all add: lt_Ord2, clarify)
   5.166 +apply (rule gen_separation [OF pred_Reflects, of "{r,x}"], simp)
   5.167 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   5.168  apply (rule DPow_LsetI)
   5.169 -apply (rename_tac u)
   5.170  apply (rule bex_iff_sats)
   5.171  apply (rule conj_iff_sats)
   5.172 -apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats)
   5.173 +apply (rule_tac env = "[p,y,r,x]" in mem_iff_sats)
   5.174  apply (rule sep_rules | simp)+
   5.175  done
   5.176  
   5.177 @@ -258,16 +234,10 @@
   5.178  
   5.179  lemma Memrel_separation:
   5.180       "separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
   5.181 -apply (rule separation_CollectI)
   5.182 -apply (rule_tac A="{z}" in subset_LsetE, blast)
   5.183 -apply (rule ReflectsE [OF Memrel_Reflects], assumption)
   5.184 -apply (drule subset_Lset_ltD, assumption)
   5.185 -apply (erule reflection_imp_L_separation)
   5.186 -  apply (simp_all add: lt_Ord2)
   5.187 +apply (rule gen_separation [OF Memrel_Reflects nonempty])
   5.188  apply (rule DPow_LsetI)
   5.189 -apply (rename_tac u)
   5.190  apply (rule bex_iff_sats conj_iff_sats)+
   5.191 -apply (rule_tac env = "[y,x,u]" in pair_iff_sats)
   5.192 +apply (rule_tac env = "[y,x,z]" in pair_iff_sats)
   5.193  apply (rule sep_rules | simp)+
   5.194  done
   5.195  
   5.196 @@ -290,18 +260,12 @@
   5.197                  pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) &
   5.198                  upair(L,cnbf,cnbf,z))"
   5.199  apply (rule strong_replacementI)
   5.200 -apply (rule rallI)
   5.201 -apply (rule separation_CollectI)
   5.202 -apply (rule_tac A="{n,A,z}" in subset_LsetE, blast)
   5.203 -apply (rule ReflectsE [OF funspace_succ_Reflects], assumption)
   5.204 -apply (drule subset_Lset_ltD, assumption)
   5.205 -apply (erule reflection_imp_L_separation)
   5.206 -  apply (simp_all add: lt_Ord2)
   5.207 +apply (rule_tac u="{n,A}" in gen_separation [OF funspace_succ_Reflects], simp)
   5.208 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   5.209  apply (rule DPow_LsetI)
   5.210 -apply (rename_tac u)
   5.211  apply (rule bex_iff_sats)
   5.212  apply (rule conj_iff_sats)
   5.213 -apply (rule_tac env = "[p,u,n,A]" in mem_iff_sats)
   5.214 +apply (rule_tac env = "[p,z,n,A]" in mem_iff_sats)
   5.215  apply (rule sep_rules | simp)+
   5.216  done
   5.217  
   5.218 @@ -319,16 +283,11 @@
   5.219       "[| L(A); L(f); L(r) |]
   5.220        ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y[L]. (\<exists>p[L].
   5.221                       fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r)))"
   5.222 -apply (rule separation_CollectI)
   5.223 -apply (rule_tac A="{A,f,r,z}" in subset_LsetE, blast)
   5.224 -apply (rule ReflectsE [OF well_ord_iso_Reflects], assumption)
   5.225 -apply (drule subset_Lset_ltD, assumption)
   5.226 -apply (erule reflection_imp_L_separation)
   5.227 -  apply (simp_all add: lt_Ord2)
   5.228 +apply (rule gen_separation [OF well_ord_iso_Reflects, of "{A,f,r}"], simp)
   5.229 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   5.230  apply (rule DPow_LsetI)
   5.231 -apply (rename_tac u)
   5.232  apply (rule imp_iff_sats)
   5.233 -apply (rule_tac env = "[u,A,f,r]" in mem_iff_sats)
   5.234 +apply (rule_tac env = "[x,A,f,r]" in mem_iff_sats)
   5.235  apply (rule sep_rules | simp)+
   5.236  done
   5.237  
   5.238 @@ -350,17 +309,11 @@
   5.239        ==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
   5.240               ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
   5.241               order_isomorphism(L,par,r,x,mx,g))"
   5.242 -apply (rule separation_CollectI)
   5.243 -apply (rule_tac A="{A,r,z}" in subset_LsetE, blast)
   5.244 -apply (rule ReflectsE [OF obase_reflects], assumption)
   5.245 -apply (drule subset_Lset_ltD, assumption)
   5.246 -apply (erule reflection_imp_L_separation)
   5.247 -  apply (simp_all add: lt_Ord2)
   5.248 +apply (rule gen_separation [OF obase_reflects, of "{A,r}"], simp)
   5.249 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   5.250  apply (rule DPow_LsetI)
   5.251 -apply (rename_tac u)
   5.252 -apply (rule bex_iff_sats)
   5.253 -apply (rule conj_iff_sats)
   5.254 -apply (rule_tac env = "[x,u,A,r]" in ordinal_iff_sats)
   5.255 +apply (rule bex_iff_sats conj_iff_sats)+
   5.256 +apply (rule_tac env = "[x,a,A,r]" in ordinal_iff_sats)
   5.257  apply (rule sep_rules | simp)+
   5.258  done
   5.259  
   5.260 @@ -378,23 +331,17 @@
   5.261                  order_isomorphism(**Lset(i),pxr,r,y,my,g)))]"
   5.262  by (intro FOL_reflections function_reflections fun_plus_reflections)
   5.263  
   5.264 -
   5.265  lemma obase_equals_separation:
   5.266       "[| L(A); L(r) |]
   5.267        ==> separation (L, \<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L].
   5.268                                ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
   5.269                                membership(L,y,my) & pred_set(L,A,x,r,pxr) &
   5.270                                order_isomorphism(L,pxr,r,y,my,g))))"
   5.271 -apply (rule separation_CollectI)
   5.272 -apply (rule_tac A="{A,r,z}" in subset_LsetE, blast)
   5.273 -apply (rule ReflectsE [OF obase_equals_reflects], assumption)
   5.274 -apply (drule subset_Lset_ltD, assumption)
   5.275 -apply (erule reflection_imp_L_separation)
   5.276 -  apply (simp_all add: lt_Ord2)
   5.277 +apply (rule gen_separation [OF obase_equals_reflects, of "{A,r}"], simp)
   5.278 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   5.279  apply (rule DPow_LsetI)
   5.280 -apply (rename_tac u)
   5.281  apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+
   5.282 -apply (rule_tac env = "[u,A,r]" in mem_iff_sats)
   5.283 +apply (rule_tac env = "[x,A,r]" in mem_iff_sats)
   5.284  apply (rule sep_rules | simp)+
   5.285  done
   5.286  
   5.287 @@ -419,18 +366,12 @@
   5.288               ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
   5.289               pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
   5.290  apply (rule strong_replacementI)
   5.291 -apply (rule rallI)
   5.292  apply (rename_tac B)
   5.293 -apply (rule separation_CollectI)
   5.294 -apply (rule_tac A="{A,B,r,z}" in subset_LsetE, blast)
   5.295 -apply (rule ReflectsE [OF omap_reflects], assumption)
   5.296 -apply (drule subset_Lset_ltD, assumption)
   5.297 -apply (erule reflection_imp_L_separation)
   5.298 -  apply (simp_all add: lt_Ord2)
   5.299 +apply (rule_tac u="{A,r,B}" in gen_separation [OF omap_reflects], simp)
   5.300 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   5.301  apply (rule DPow_LsetI)
   5.302 -apply (rename_tac u)
   5.303  apply (rule bex_iff_sats conj_iff_sats)+
   5.304 -apply (rule_tac env = "[a,u,A,B,r]" in mem_iff_sats)
   5.305 +apply (rule_tac env = "[a,z,A,B,r]" in mem_iff_sats)
   5.306  apply (rule sep_rules | simp)+
   5.307  done
   5.308  
   5.309 @@ -456,16 +397,11 @@
   5.310                  pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r &
   5.311                  (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
   5.312                                     fx \<noteq> gx))"
   5.313 -apply (rule separation_CollectI)
   5.314 -apply (rule_tac A="{r,f,g,a,b,z}" in subset_LsetE, blast)
   5.315 -apply (rule ReflectsE [OF is_recfun_reflects], assumption)
   5.316 -apply (drule subset_Lset_ltD, assumption)
   5.317 -apply (erule reflection_imp_L_separation)
   5.318 -  apply (simp_all add: lt_Ord2)
   5.319 +apply (rule gen_separation [OF is_recfun_reflects, of "{r,f,g,a,b}"], simp)
   5.320 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   5.321  apply (rule DPow_LsetI)
   5.322 -apply (rename_tac u)
   5.323  apply (rule bex_iff_sats conj_iff_sats)+
   5.324 -apply (rule_tac env = "[xa,u,r,f,g,a,b]" in pair_iff_sats)
   5.325 +apply (rule_tac env = "[xa,x,r,f,g,a,b]" in pair_iff_sats)
   5.326  apply (rule sep_rules | simp)+
   5.327  done
   5.328