# HG changeset patch
# User paulson
# Date 1031756137 -7200
# Node ID 52a419210d5c3f6d5f47995ce82591d6589081c6
# Parent  40e4755e57f7c54b673eea6cf5f7c6ed01699c41
Streamlined proofs of instances of Separation

diff -r 40e4755e57f7 -r 52a419210d5c src/ZF/Constructible/DPow_absolute.thy
--- a/src/ZF/Constructible/DPow_absolute.thy	Wed Sep 11 16:53:59 2002 +0200
+++ b/src/ZF/Constructible/DPow_absolute.thy	Wed Sep 11 16:55:37 2002 +0200
@@ -243,14 +243,9 @@
 lemma DPow_separation:
     "[| L(A); env \<in> list(A); p \<in> formula |]
      ==> separation(L, \<lambda>x. is_DPow_body(L,A,env,p,x))"
-apply (subgoal_tac "L(env) & L(p)") 
- prefer 2 apply (blast intro: transL) 
-apply (rule separation_CollectI)
-apply (rule_tac A="{A,env,p,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF DPow_body_reflection], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
+apply (rule gen_separation [OF DPow_body_reflection, of "{A,env,p}"], 
+       blast intro: transL)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
 apply (rule_tac env = "[x,A,env,p]" in DPow_body_iff_sats)
 apply (rule sep_rules | simp)+
@@ -282,19 +277,14 @@
                   pair(L,env,p,ep) & 
                   is_Collect(L, A, \<lambda>x. is_DPow_body(L,A,env,p,x), z))"
 apply (rule strong_replacementI)
-apply (rule rallI)
 apply (rename_tac B)
-apply (rule separation_CollectI)
-apply (rule_tac A="{A,B,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF DPow_replacement_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
+apply (rule_tac u="{A,B}" in gen_separation [OF DPow_replacement_Reflects], 
+       simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
+apply (unfold is_Collect_def) 
 apply (rule DPow_LsetI)
-apply (rename_tac v)
-apply (unfold is_Collect_def) 
 apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,v,A,B]" in mem_iff_sats)
+apply (rule_tac env = "[u,x,A,B]" in mem_iff_sats)
 apply (rule sep_rules mem_formula_iff_sats mem_list_iff_sats 
             DPow_body_iff_sats | simp)+
 done
@@ -559,18 +549,12 @@
    "[|L(x); L(g)|] ==> strong_replacement(L, \<lambda>y z. transrec_body(L,g,x,y,z))"
 apply (unfold transrec_body_def)  
 apply (rule strong_replacementI) 
-apply (rule rallI)
 apply (rename_tac B)  
-apply (rule separation_CollectI) 
-apply (rule_tac A="{x,g,B,z}" in subset_LsetE, blast) 
-apply (rule ReflectsE [OF strong_rep_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption) 
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
+apply (rule_tac u="{x,g,B}" in gen_separation [OF strong_rep_Reflects], simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac u) 
 apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[v,u,x,g,B,z]" in mem_iff_sats) 
+apply (rule_tac env = "[v,u,x,g,B]" in mem_iff_sats) 
 apply (rule sep_rules DPow'_iff_sats | simp)+
 done
 
@@ -599,30 +583,21 @@
 done
 
 
-
 lemma transrec_rep: 
     "[|L(j)|]
     ==> transrec_replacement(L, \<lambda>x f u. 
               \<exists>r[L]. is_Replace(L, x, transrec_body(L,f,x), r) & 
                      big_union(L, r, u), j)"
-apply (subgoal_tac "L(Memrel(eclose({j})))")
- prefer 2 apply simp
 apply (rule transrec_replacementI, assumption)
+apply (unfold transrec_body_def)  
 apply (rule strong_replacementI)
-apply (unfold transrec_body_def)  
-apply (rule rallI)
 apply (rename_tac B)
-apply (rule separation_CollectI)
-apply (rule_tac A="{j,B,z,Memrel(eclose({j}))}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF transrec_rep_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2 Memrel_closed)
-apply (elim conjE)
+apply (rule_tac u="{j,B,Memrel(eclose({j}))}" 
+         in gen_separation [OF transrec_rep_Reflects], simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac w)
 apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[v,w,j,B,Memrel(eclose({j}))]" in mem_iff_sats)
+apply (rule_tac env = "[v,x,j,B,Memrel(eclose({j}))]" in mem_iff_sats)
 apply (rule sep_rules is_wfrec_iff_sats Replace_iff_sats DPow'_iff_sats | 
        simp)+
 done
diff -r 40e4755e57f7 -r 52a419210d5c src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Wed Sep 11 16:53:59 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Wed Sep 11 16:55:37 2002 +0200
@@ -127,7 +127,8 @@
   and successor_abs = M_trivial.successor_abs [OF M_trivial_L]
   and succ_in_M_iff = M_trivial.succ_in_M_iff [OF M_trivial_L]
   and separation_closed = M_trivial.separation_closed [OF M_trivial_L]
-  and strong_replacementI = M_trivial.strong_replacementI [OF M_trivial_L]
+  and strong_replacementI = 
+      M_trivial.strong_replacementI [OF M_trivial_L, rule_format]
   and strong_replacement_closed = M_trivial.strong_replacement_closed [OF M_trivial_L]
   and RepFun_closed = M_trivial.RepFun_closed [OF M_trivial_L]
   and lam_closed = M_trivial.lam_closed [OF M_trivial_L]
@@ -169,7 +170,6 @@
 declare successor_abs [simp]
 declare succ_in_M_iff [iff]
 declare separation_closed [intro, simp]
-declare strong_replacementI
 declare strong_replacement_closed [intro, simp]
 declare RepFun_closed [intro, simp]
 declare lam_closed [intro, simp]
diff -r 40e4755e57f7 -r 52a419210d5c src/ZF/Constructible/Rec_Separation.thy
--- a/src/ZF/Constructible/Rec_Separation.thy	Wed Sep 11 16:53:59 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy	Wed Sep 11 16:55:37 2002 +0200
@@ -71,7 +71,7 @@
        ==> rtran_closure_mem(**A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)"
 by (simp add: sats_rtran_closure_mem_fm)
 
-theorem rtran_closure_mem_reflection:
+lemma rtran_closure_mem_reflection:
      "REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)),
                \<lambda>i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]"
 apply (simp only: rtran_closure_mem_def setclass_simps)
@@ -81,15 +81,10 @@
 text{*Separation for @{term "rtrancl(r)"}.*}
 lemma rtrancl_separation:
      "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))"
-apply (rule separation_CollectI)
-apply (rule_tac A="{r,A,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF rtran_closure_mem_reflection], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
+apply (rule gen_separation [OF rtran_closure_mem_reflection, of "{r,A}"], simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac u)
-apply (rule_tac env = "[u,r,A]" in rtran_closure_mem_iff_sats)
+apply (rule_tac env = "[x,r,A]" in rtran_closure_mem_iff_sats)
 apply (rule sep_rules | simp)+
 done
 
@@ -183,22 +178,16 @@
 by (intro FOL_reflections function_reflections fun_plus_reflections
           tran_closure_reflection)
 
-
 lemma wellfounded_trancl_separation:
          "[| L(r); L(Z) |] ==>
           separation (L, \<lambda>x.
               \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
                w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)"
-apply (rule separation_CollectI)
-apply (rule_tac A="{r,Z,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF wellfounded_trancl_reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
+apply (rule gen_separation [OF wellfounded_trancl_reflects, of "{r,Z}"], simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac u)
 apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[w,u,r,Z]" in mem_iff_sats)
+apply (rule_tac env = "[w,x,r,Z]" in mem_iff_sats)
 apply (rule sep_rules tran_closure_iff_sats | simp)+
 done
 
@@ -251,17 +240,10 @@
      "L(r) ==>
       separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
          ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))"
-apply (rule separation_CollectI)
-apply (rule_tac A="{r,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF wfrank_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2, clarify)
+apply (rule gen_separation [OF wfrank_Reflects], simp)
 apply (rule DPow_LsetI)
-apply (rename_tac u)
 apply (rule ball_iff_sats imp_iff_sats)+
-apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
-apply (rule sep_rules | simp)+
+apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats)
 apply (rule sep_rules is_recfun_iff_sats | simp)+
 done
 
@@ -282,7 +264,6 @@
 by (intro FOL_reflections function_reflections fun_plus_reflections
              is_recfun_reflection tran_closure_reflection)
 
-
 lemma wfrank_strong_replacement:
      "L(r) ==>
       strong_replacement(L, \<lambda>x z.
@@ -291,19 +272,14 @@
                         M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
                         is_range(L,f,y)))"
 apply (rule strong_replacementI)
-apply (rule rallI)
-apply (rename_tac B)
-apply (rule separation_CollectI)
-apply (rule_tac A="{B,r,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF wfrank_replacement_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
+apply (rule_tac u="{r,A}" in gen_separation [OF wfrank_replacement_Reflects], 
+       simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac u)
 apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[x,u,B,r]" in mem_iff_sats)
-apply (rule sep_rules list.intros app_type tran_closure_iff_sats is_recfun_iff_sats | simp)+
+apply (rule_tac env = "[x,z,A,r]" in mem_iff_sats)
+apply (rule sep_rules list.intros app_type tran_closure_iff_sats 
+            is_recfun_iff_sats | simp)+
 done
 
 
@@ -332,16 +308,10 @@
              is_range(L,f,rangef) -->
              M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
              ordinal(L,rangef)))"
-apply (rule separation_CollectI)
-apply (rule_tac A="{r,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF Ord_wfrank_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2, clarify)
+apply (rule gen_separation [OF Ord_wfrank_Reflects], simp)
 apply (rule DPow_LsetI)
-apply (rename_tac u)
 apply (rule ball_iff_sats imp_iff_sats)+
-apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
+apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats)
 apply (rule sep_rules is_recfun_iff_sats | simp)+
 done
 
@@ -406,21 +376,14 @@
    "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)"
 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
 apply (rule strong_replacementI)
-apply (rule rallI)
 apply (rename_tac B)
-apply (rule separation_CollectI)
-apply (insert nonempty)
-apply (subgoal_tac "L(Memrel(succ(n)))")
-apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF list_replacement1_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2 Memrel_closed)
-apply (elim conjE)
+apply (rule_tac u="{B,A,n,0,Memrel(succ(n))}" 
+         in gen_separation [OF list_replacement1_Reflects], 
+       simp add: nonempty)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac v)
 apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,v,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
+apply (rule_tac env = "[u,x,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
 apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
 done
@@ -449,20 +412,14 @@
                is_wfrec(L, iterates_MH(L,is_list_functor(L,A), 0),
                         msn, n, y)))"
 apply (rule strong_replacementI)
-apply (rule rallI)
 apply (rename_tac B)
-apply (rule separation_CollectI)
-apply (insert nonempty)
-apply (rule_tac A="{A,B,z,0,nat}" in subset_LsetE)
-apply (blast intro: L_nat)
-apply (rule ReflectsE [OF list_replacement2_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
+apply (rule_tac u="{A,B,0,nat}" 
+         in gen_separation [OF list_replacement2_Reflects], 
+       simp add: L_nat nonempty)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac v)
 apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,v,A,B,0,nat]" in mem_iff_sats)
+apply (rule_tac env = "[u,x,A,B,0,nat]" in mem_iff_sats)
 apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
 done
@@ -487,20 +444,14 @@
    "iterates_replacement(L, is_formula_functor(L), 0)"
 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
 apply (rule strong_replacementI)
-apply (rule rallI)
 apply (rename_tac B)
-apply (rule separation_CollectI)
-apply (insert nonempty)
-apply (subgoal_tac "L(Memrel(succ(n)))")
-apply (rule_tac A="{B,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF formula_replacement1_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2 Memrel_closed)
+apply (rule_tac u="{B,n,0,Memrel(succ(n))}" 
+         in gen_separation [OF formula_replacement1_Reflects], 
+       simp add: nonempty)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac v)
 apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,v,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
+apply (rule_tac env = "[u,x,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
 apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
 done
@@ -528,20 +479,14 @@
                is_wfrec(L, iterates_MH(L,is_formula_functor(L), 0),
                         msn, n, y)))"
 apply (rule strong_replacementI)
-apply (rule rallI)
 apply (rename_tac B)
-apply (rule separation_CollectI)
-apply (insert nonempty)
-apply (rule_tac A="{B,z,0,nat}" in subset_LsetE)
-apply (blast intro: L_nat)
-apply (rule ReflectsE [OF formula_replacement2_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
+apply (rule_tac u="{B,0,nat}" 
+         in gen_separation [OF formula_replacement2_Reflects], 
+       simp add: nonempty L_nat)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac v)
 apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,v,B,0,nat]" in mem_iff_sats)
+apply (rule_tac env = "[u,x,B,0,nat]" in mem_iff_sats)
 apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
 done
@@ -609,25 +554,18 @@
    "L(w) ==> iterates_replacement(L, %l t. is_tl(L,l,t), w)"
 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
 apply (rule strong_replacementI)
-apply (rule rallI)
-apply (rule separation_CollectI)
-apply (subgoal_tac "L(Memrel(succ(n)))")
-apply (rule_tac A="{A,n,w,z,Memrel(succ(n))}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF nth_replacement_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2 Memrel_closed)
-apply (elim conjE)
+apply (rule_tac u="{A,n,w,Memrel(succ(n))}" 
+         in gen_separation [OF nth_replacement_Reflects], 
+       simp add: nonempty)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac v)
 apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,v,A,z,w,Memrel(succ(n))]" in mem_iff_sats)
+apply (rule_tac env = "[u,x,A,w,Memrel(succ(n))]" in mem_iff_sats)
 apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats
             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
 done
 
 
-
 subsubsection{*Instantiating the locale @{text M_datatypes}*}
 
 lemma M_datatypes_axioms_L: "M_datatypes_axioms(L)"
@@ -676,20 +614,13 @@
    "L(A) ==> iterates_replacement(L, big_union(L), A)"
 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
 apply (rule strong_replacementI)
-apply (rule rallI)
 apply (rename_tac B)
-apply (rule separation_CollectI)
-apply (subgoal_tac "L(Memrel(succ(n)))")
-apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF eclose_replacement1_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2 Memrel_closed)
-apply (elim conjE)
+apply (rule_tac u="{B,A,n,Memrel(succ(n))}" 
+         in gen_separation [OF eclose_replacement1_Reflects], simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac v)
 apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,v,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
+apply (rule_tac env = "[u,x,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
 apply (rule sep_rules iterates_MH_iff_sats is_nat_case_iff_sats
              is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
 done
@@ -718,19 +649,13 @@
                is_wfrec(L, iterates_MH(L,big_union(L), A),
                         msn, n, y)))"
 apply (rule strong_replacementI)
-apply (rule rallI)
 apply (rename_tac B)
-apply (rule separation_CollectI)
-apply (rule_tac A="{A,B,z,nat}" in subset_LsetE)
-apply (blast intro: L_nat)
-apply (rule ReflectsE [OF eclose_replacement2_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
+apply (rule_tac u="{A,B,nat}" 
+         in gen_separation [OF eclose_replacement2_Reflects], simp add: L_nat)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac v)
 apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,v,A,B,nat]" in mem_iff_sats)
+apply (rule_tac env = "[u,x,A,B,nat]" in mem_iff_sats)
 apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats
               is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
 done
diff -r 40e4755e57f7 -r 52a419210d5c src/ZF/Constructible/Satisfies_absolute.thy
--- a/src/ZF/Constructible/Satisfies_absolute.thy	Wed Sep 11 16:53:59 2002 +0200
+++ b/src/ZF/Constructible/Satisfies_absolute.thy	Wed Sep 11 16:55:37 2002 +0200
@@ -823,24 +823,16 @@
               env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
               is_bool_of_o(L, nx \<in> ny, bo) &
               pair(L, env, bo, z))"
-apply (frule list_closed) 
-apply (rule strong_replacementI) 
-apply (rule rallI)
-apply (rename_tac B)  
-apply (rule separation_CollectI) 
-apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast) 
-apply (rule ReflectsE [OF Member_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption) 
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
-apply (simp add: is_nth_def is_wfrec_def is_bool_of_o_def)
+apply (rule strong_replacementI)
+apply (rename_tac B)
+apply (rule_tac u="{list(A),B,x,y}" 
+         in gen_separation [OF Member_Reflects], 
+       simp add: nat_into_M list_closed)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac u) 
-apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[v,u,list(A),B,x,y,z]" in mem_iff_sats) 
-apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats
-            is_recfun_iff_sats hd_iff_sats tl_iff_sats quasinat_iff_sats
-     | simp)+
+apply (rule bex_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[v,u,list(A),B,x,y]" in mem_iff_sats) 
+apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
 done
 
 
@@ -865,24 +857,16 @@
               env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
               is_bool_of_o(L, nx = ny, bo) &
               pair(L, env, bo, z))"
-apply (frule list_closed) 
-apply (rule strong_replacementI) 
-apply (rule rallI)
-apply (rename_tac B)  
-apply (rule separation_CollectI) 
-apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast) 
-apply (rule ReflectsE [OF Equal_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption) 
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
-apply (simp add: is_nth_def is_wfrec_def is_bool_of_o_def)
+apply (rule strong_replacementI)
+apply (rename_tac B)
+apply (rule_tac u="{list(A),B,x,y}" 
+         in gen_separation [OF Equal_Reflects], 
+       simp add: nat_into_M list_closed)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac u) 
-apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[v,u,list(A),B,x,y,z]" in mem_iff_sats) 
-apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats
-            is_recfun_iff_sats hd_iff_sats tl_iff_sats quasinat_iff_sats
-     | simp)+
+apply (rule bex_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[v,u,list(A),B,x,y]" in mem_iff_sats) 
+apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
 done
 
 subsubsection{*The @{term "Nand"} Case*}
@@ -909,22 +893,15 @@
                fun_apply(L,rp,env,rpe) & fun_apply(L,rq,env,rqe) & 
                is_and(L,rpe,rqe,andpq) & is_not(L,andpq,notpq) & 
                env \<in> list(A) & pair(L, env, notpq, z))"
-apply (frule list_closed) 
-apply (rule strong_replacementI) 
-apply (rule rallI)
-apply (rename_tac B)  
-apply (rule separation_CollectI) 
-apply (rule_tac A="{list(A),B,rp,rq,z}" in subset_LsetE, blast) 
-apply (rule ReflectsE [OF Nand_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption) 
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
-apply (simp add: is_and_def is_not_def)
+apply (rule strong_replacementI)
+apply (rename_tac B)
+apply (rule_tac u="{list(A),B,rp,rq}" in gen_separation [OF Nand_Reflects],
+       simp add: list_closed)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac v) 
-apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,v,list(A),B,rp,rq,z]" in mem_iff_sats) 
-apply (rule sep_rules | simp)+
+apply (rule bex_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[u,x,list(A),B,rp,rq]" in mem_iff_sats) 
+apply (rule sep_rules is_and_iff_sats is_not_iff_sats | simp)+
 done
 
 
@@ -958,22 +935,15 @@
 			       fun_apply(L,rp,co,rpco) --> number1(L, rpco), 
                             bo) &
 	      pair(L,env,bo,z))"
-apply (frule list_closed) 
-apply (rule strong_replacementI) 
-apply (rule rallI)
-apply (rename_tac B)  
-apply (rule separation_CollectI) 
-apply (rule_tac A="{A,list(A),B,rp,z}" in subset_LsetE, blast) 
-apply (rule ReflectsE [OF Forall_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption) 
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
-apply (simp add: is_bool_of_o_def)
+apply (rule strong_replacementI)
+apply (rename_tac B)
+apply (rule_tac u="{A,list(A),B,rp}" in gen_separation [OF Forall_Reflects],
+       simp add: list_closed)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac v) 
-apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,v,A,list(A),B,rp,z]" in mem_iff_sats)
-apply (rule sep_rules Cons_iff_sats | simp)+
+apply (rule bex_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[u,x,A,list(A),B,rp]" in mem_iff_sats)
+apply (rule sep_rules is_bool_of_o_iff_sats Cons_iff_sats | simp)+
 done
 
 subsubsection{*The @{term "transrec_replacement"} Case*}
@@ -989,24 +959,16 @@
 lemma formula_rec_replacement: 
       --{*For the @{term transrec}*}
    "[|n \<in> nat; L(A)|] ==> transrec_replacement(L, satisfies_MH(L,A), n)"
-apply (subgoal_tac "L(Memrel(eclose({n})))")
- prefer 2 apply (simp add: nat_into_M) 
-apply (rule transrec_replacementI) 
-apply (simp add: nat_into_M) 
+apply (rule transrec_replacementI, simp add: nat_into_M) 
 apply (rule strong_replacementI)
-apply (rule rallI)
 apply (rename_tac B)
-apply (rule separation_CollectI)
-apply (rule_tac A="{B,A,n,z,Memrel(eclose({n}))}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF formula_rec_replacement_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2 Memrel_closed)
-apply (elim conjE)
+apply (rule_tac u="{B,A,n,Memrel(eclose({n}))}"
+         in gen_separation [OF formula_rec_replacement_Reflects],
+       simp add: nat_into_M)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac v)
 apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,v,A,n,B,Memrel(eclose({n}))]" in mem_iff_sats)
+apply (rule_tac env = "[u,x,A,n,B,Memrel(eclose({n}))]" in mem_iff_sats)
 apply (rule sep_rules satisfies_MH_iff_sats is_wfrec_iff_sats | simp)+
 done
 
@@ -1045,19 +1007,13 @@
                                   satisfies_is_d(L,A,g), x, c) &
              pair(L, x, c, y)))" 
 apply (rule strong_replacementI)
-apply (rule rallI)
 apply (rename_tac B)
-apply (rule separation_CollectI)
-apply (rule_tac A="{B,A,g,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF formula_rec_lambda_replacement_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2 Memrel_closed)
-apply (elim conjE)
+apply (rule_tac u="{B,A,g}"
+         in gen_separation [OF formula_rec_lambda_replacement_Reflects], simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac v)
 apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,v,A,g,B]" in mem_iff_sats)
+apply (rule_tac env = "[u,x,A,g,B]" in mem_iff_sats)
 apply (rule sep_rules mem_formula_iff_sats
           formula_case_iff_sats satisfies_is_a_iff_sats
           satisfies_is_b_iff_sats satisfies_is_c_iff_sats
diff -r 40e4755e57f7 -r 52a419210d5c src/ZF/Constructible/Separation.thy
--- a/src/ZF/Constructible/Separation.thy	Wed Sep 11 16:53:59 2002 +0200
+++ b/src/ZF/Constructible/Separation.thy	Wed Sep 11 16:55:37 2002 +0200
@@ -51,6 +51,24 @@
 apply (simp add: Lset_succ Collect_conj_in_DPow_Lset)
 done
 
+text{*Encapsulates the standard proof script for proving instances of 
+Separation.  Typically @{term u} is a finite enumeration.*}
+lemma gen_separation:
+ assumes reflection: "REFLECTS [P,Q]"
+     and Lu:         "L(u)"
+     and collI: "!!j. u \<in> Lset(j)
+                \<Longrightarrow> Collect(Lset(j), Q(j)) \<in> DPow(Lset(j))"
+ shows "separation(L,P)"
+apply (rule separation_CollectI)
+apply (rule_tac A="{u,z}" in subset_LsetE, blast intro: Lu)
+apply (rule ReflectsE [OF reflection], assumption)
+apply (drule subset_Lset_ltD, assumption)
+apply (erule reflection_imp_L_separation)
+  apply (simp_all add: lt_Ord2, clarify)
+apply (rule collI)
+apply assumption;  
+done
+
 
 subsection{*Separation for Intersection*}
 
@@ -61,12 +79,7 @@
 
 lemma Inter_separation:
      "L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A --> x\<in>y)"
-apply (rule separation_CollectI)
-apply (rule_tac A="{A,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF Inter_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2, clarify)
+apply (rule gen_separation [OF Inter_Reflects], simp)
 apply (rule DPow_LsetI)
 apply (rule ball_iff_sats)
 apply (rule imp_iff_sats)
@@ -83,13 +96,8 @@
 
 lemma Diff_separation:
      "L(B) ==> separation(L, \<lambda>x. x \<notin> B)"
-apply (rule separation_CollectI) 
-apply (rule_tac A="{B,z}" in subset_LsetE, blast) 
-apply (rule ReflectsE [OF Diff_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption) 
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2, clarify)
-apply (rule DPow_LsetI) 
+apply (rule gen_separation [OF Diff_Reflects], simp)
+apply (rule DPow_LsetI)
 apply (rule not_iff_sats) 
 apply (rule_tac env="[x,B]" in mem_iff_sats)
 apply (rule sep_rules | simp)+
@@ -106,17 +114,12 @@
 lemma cartprod_separation:
      "[| L(A); L(B) |]
       ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)))"
-apply (rule separation_CollectI)
-apply (rule_tac A="{A,B,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF cartprod_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2, clarify)
+apply (rule gen_separation [OF cartprod_Reflects, of "{A,B}"], simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac u)
 apply (rule bex_iff_sats)
 apply (rule conj_iff_sats)
-apply (rule_tac i=0 and j=2 and env="[x,u,A,B]" in mem_iff_sats, simp_all)
+apply (rule_tac i=0 and j=2 and env="[x,z,A,B]" in mem_iff_sats, simp_all)
 apply (rule sep_rules | simp)+
 done
 
@@ -130,12 +133,8 @@
 lemma image_separation:
      "[| L(A); L(r) |]
       ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)))"
-apply (rule separation_CollectI)
-apply (rule_tac A="{A,r,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF image_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2, clarify)
+apply (rule gen_separation [OF image_Reflects, of "{A,r}"], simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
 apply (rule bex_iff_sats)
 apply (rule conj_iff_sats)
@@ -155,17 +154,11 @@
 lemma converse_separation:
      "L(r) ==> separation(L,
          \<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)))"
-apply (rule separation_CollectI)
-apply (rule_tac A="{r,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF converse_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2, clarify)
+apply (rule gen_separation [OF converse_Reflects], simp)
 apply (rule DPow_LsetI)
-apply (rename_tac u)
 apply (rule bex_iff_sats)
 apply (rule conj_iff_sats)
-apply (rule_tac i=0 and j=2 and env="[p,u,r]" in mem_iff_sats, simp_all)
+apply (rule_tac i=0 and j=2 and env="[p,z,r]" in mem_iff_sats, simp_all)
 apply (rule sep_rules | simp)+
 done
 
@@ -179,17 +172,11 @@
 
 lemma restrict_separation:
    "L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))"
-apply (rule separation_CollectI)
-apply (rule_tac A="{A,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF restrict_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2, clarify)
+apply (rule gen_separation [OF restrict_Reflects], simp)
 apply (rule DPow_LsetI)
-apply (rename_tac u)
 apply (rule bex_iff_sats)
 apply (rule conj_iff_sats)
-apply (rule_tac i=0 and j=2 and env="[x,u,A]" in mem_iff_sats, simp_all)
+apply (rule_tac i=0 and j=2 and env="[x,z,A]" in mem_iff_sats, simp_all)
 apply (rule sep_rules | simp)+
 done
 
@@ -210,18 +197,12 @@
       ==> separation(L, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
                   pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
                   xy\<in>s & yz\<in>r)"
-apply (rule separation_CollectI)
-apply (rule_tac A="{r,s,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF comp_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2, clarify)
+apply (rule gen_separation [OF comp_Reflects, of "{r,s}"], simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac u)
 apply (rule bex_iff_sats)+
-apply (rename_tac x y z)
 apply (rule conj_iff_sats)
-apply (rule_tac env="[z,y,x,u,r,s]" in pair_iff_sats)
+apply (rule_tac env="[z,y,x,xz,r,s]" in pair_iff_sats)
 apply (rule sep_rules | simp)+
 done
 
@@ -234,17 +215,12 @@
 
 lemma pred_separation:
      "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"
-apply (rule separation_CollectI)
-apply (rule_tac A="{r,x,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF pred_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2, clarify)
+apply (rule gen_separation [OF pred_Reflects, of "{r,x}"], simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac u)
 apply (rule bex_iff_sats)
 apply (rule conj_iff_sats)
-apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats)
+apply (rule_tac env = "[p,y,r,x]" in mem_iff_sats)
 apply (rule sep_rules | simp)+
 done
 
@@ -258,16 +234,10 @@
 
 lemma Memrel_separation:
      "separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
-apply (rule separation_CollectI)
-apply (rule_tac A="{z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF Memrel_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
+apply (rule gen_separation [OF Memrel_Reflects nonempty])
 apply (rule DPow_LsetI)
-apply (rename_tac u)
 apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[y,x,u]" in pair_iff_sats)
+apply (rule_tac env = "[y,x,z]" in pair_iff_sats)
 apply (rule sep_rules | simp)+
 done
 
@@ -290,18 +260,12 @@
                 pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) &
                 upair(L,cnbf,cnbf,z))"
 apply (rule strong_replacementI)
-apply (rule rallI)
-apply (rule separation_CollectI)
-apply (rule_tac A="{n,A,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF funspace_succ_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
+apply (rule_tac u="{n,A}" in gen_separation [OF funspace_succ_Reflects], simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac u)
 apply (rule bex_iff_sats)
 apply (rule conj_iff_sats)
-apply (rule_tac env = "[p,u,n,A]" in mem_iff_sats)
+apply (rule_tac env = "[p,z,n,A]" in mem_iff_sats)
 apply (rule sep_rules | simp)+
 done
 
@@ -319,16 +283,11 @@
      "[| L(A); L(f); L(r) |]
       ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y[L]. (\<exists>p[L].
                      fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r)))"
-apply (rule separation_CollectI)
-apply (rule_tac A="{A,f,r,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF well_ord_iso_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
+apply (rule gen_separation [OF well_ord_iso_Reflects, of "{A,f,r}"], simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac u)
 apply (rule imp_iff_sats)
-apply (rule_tac env = "[u,A,f,r]" in mem_iff_sats)
+apply (rule_tac env = "[x,A,f,r]" in mem_iff_sats)
 apply (rule sep_rules | simp)+
 done
 
@@ -350,17 +309,11 @@
       ==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
              ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
              order_isomorphism(L,par,r,x,mx,g))"
-apply (rule separation_CollectI)
-apply (rule_tac A="{A,r,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF obase_reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
+apply (rule gen_separation [OF obase_reflects, of "{A,r}"], simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac u)
-apply (rule bex_iff_sats)
-apply (rule conj_iff_sats)
-apply (rule_tac env = "[x,u,A,r]" in ordinal_iff_sats)
+apply (rule bex_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[x,a,A,r]" in ordinal_iff_sats)
 apply (rule sep_rules | simp)+
 done
 
@@ -378,23 +331,17 @@
                 order_isomorphism(**Lset(i),pxr,r,y,my,g)))]"
 by (intro FOL_reflections function_reflections fun_plus_reflections)
 
-
 lemma obase_equals_separation:
      "[| L(A); L(r) |]
       ==> separation (L, \<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L].
                               ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
                               membership(L,y,my) & pred_set(L,A,x,r,pxr) &
                               order_isomorphism(L,pxr,r,y,my,g))))"
-apply (rule separation_CollectI)
-apply (rule_tac A="{A,r,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF obase_equals_reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
+apply (rule gen_separation [OF obase_equals_reflects, of "{A,r}"], simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac u)
 apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+
-apply (rule_tac env = "[u,A,r]" in mem_iff_sats)
+apply (rule_tac env = "[x,A,r]" in mem_iff_sats)
 apply (rule sep_rules | simp)+
 done
 
@@ -419,18 +366,12 @@
              ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
              pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
 apply (rule strong_replacementI)
-apply (rule rallI)
 apply (rename_tac B)
-apply (rule separation_CollectI)
-apply (rule_tac A="{A,B,r,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF omap_reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
+apply (rule_tac u="{A,r,B}" in gen_separation [OF omap_reflects], simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac u)
 apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[a,u,A,B,r]" in mem_iff_sats)
+apply (rule_tac env = "[a,z,A,B,r]" in mem_iff_sats)
 apply (rule sep_rules | simp)+
 done
 
@@ -456,16 +397,11 @@
                 pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r &
                 (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
                                    fx \<noteq> gx))"
-apply (rule separation_CollectI)
-apply (rule_tac A="{r,f,g,a,b,z}" in subset_LsetE, blast)
-apply (rule ReflectsE [OF is_recfun_reflects], assumption)
-apply (drule subset_Lset_ltD, assumption)
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
+apply (rule gen_separation [OF is_recfun_reflects, of "{r,f,g,a,b}"], simp)
+apply (drule mem_Lset_imp_subset_Lset, clarsimp)
 apply (rule DPow_LsetI)
-apply (rename_tac u)
 apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[xa,u,r,f,g,a,b]" in pair_iff_sats)
+apply (rule_tac env = "[xa,x,r,f,g,a,b]" in pair_iff_sats)
 apply (rule sep_rules | simp)+
 done