# HG changeset patch
# User paulson
# Date 1035978258 -3600
# Node ID 22dce9134953726fc9b90664d4ce2b55f6903e88
# Parent  bc63c3b2b3e78faa9138218942d83df5916f31fd
simpler separation/replacement proofs

diff -r bc63c3b2b3e7 -r 22dce9134953 src/ZF/Constructible/DPow_absolute.thy
--- a/src/ZF/Constructible/DPow_absolute.thy	Wed Oct 30 12:18:23 2002 +0100
+++ b/src/ZF/Constructible/DPow_absolute.thy	Wed Oct 30 12:44:18 2002 +0100
@@ -181,7 +181,7 @@
 done
 
 
-subsection{*Additional Constraints on the Class Model @{term M}*}
+subsection{*A Locale for Relativizing the Operator @{term DPow'}*}
 
 locale M_DPow = M_satisfies +
  assumes sep:
@@ -242,12 +242,10 @@
 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 (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)+
+apply (rule gen_separation_multi [OF DPow_body_reflection, of "{A,env,p}"], 
+       auto intro: transL)
+apply (rule_tac env="[A,env,p]" in DPow_LsetI)
+apply (rule DPow_body_iff_sats sep_rules | simp)+
 done
 
 
@@ -276,14 +274,11 @@
                   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 (rename_tac B)
-apply (rule_tac u="{A,B}" in gen_separation [OF DPow_replacement_Reflects], 
-       simp)
-apply (drule mem_Lset_imp_subset_Lset, clarsimp)
+apply (rule_tac u="{A,B}" 
+         in gen_separation_multi [OF DPow_replacement_Reflects], 
+       auto)
 apply (unfold is_Collect_def) 
-apply (rule DPow_LsetI)
-apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,x,A,B]" in mem_iff_sats)
+apply (rule_tac env="[A,B]" in DPow_LsetI)
 apply (rule sep_rules mem_formula_iff_sats mem_list_iff_sats 
             DPow_body_iff_sats | simp)+
 done
@@ -452,13 +447,8 @@
              mem_list_reflection Collect_reflection DPow_body_reflection)
 done
 
-(*????????????????move up*)
 
-
-
-
-
-subsection{*Additional Constraints on the Class Model @{term M}*}
+subsection{*A Locale for Relativizing the Operator @{term Lset}*}
 
 constdefs
   transrec_body :: "[i=>o,i,i,i,i] => o"
@@ -510,7 +500,7 @@
 done
 
 
-
+text{*Relativization of the Operator @{term Lset}*}
 constdefs
 
   is_Lset :: "[i=>o, i, i] => o"
@@ -534,7 +524,6 @@
 
 subsection{*Instantiating the Locale @{text M_Lset}*}
 
-
 subsubsection{*The First Instance of Replacement*}
 
 lemma strong_rep_Reflects:
@@ -548,12 +537,9 @@
    "[|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 (rename_tac B)  
-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 (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[v,u,x,g,B]" in mem_iff_sats) 
+apply (rule_tac u="{x,g,B}" 
+         in gen_separation_multi [OF strong_rep_Reflects], auto)
+apply (rule_tac env="[x,g,B]" in DPow_LsetI)
 apply (rule sep_rules DPow'_iff_sats | simp)+
 done
 
@@ -590,13 +576,9 @@
 apply (rule transrec_replacementI, assumption)
 apply (unfold transrec_body_def)  
 apply (rule strong_replacementI)
-apply (rename_tac B)
 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 (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[v,x,j,B,Memrel(eclose({j}))]" in mem_iff_sats)
+         in gen_separation_multi [OF transrec_rep_Reflects], auto)
+apply (rule_tac env="[j,B,Memrel(eclose({j}))]" in DPow_LsetI)
 apply (rule sep_rules is_wfrec_iff_sats Replace_iff_sats DPow'_iff_sats | 
        simp)+
 done
diff -r bc63c3b2b3e7 -r 22dce9134953 src/ZF/Constructible/Datatype_absolute.thy
--- a/src/ZF/Constructible/Datatype_absolute.thy	Wed Oct 30 12:18:23 2002 +0100
+++ b/src/ZF/Constructible/Datatype_absolute.thy	Wed Oct 30 12:44:18 2002 +0100
@@ -120,16 +120,16 @@
         is_nat_case(M, v, \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & isF(gm,u),
                     n, z)"
 
+  is_iterates :: "[i=>o, [i,i]=>o, i, i, i] => o"
+    "is_iterates(M,isF,v,n,Z) == 
+      \<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
+                       is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)"
+
   iterates_replacement :: "[i=>o, [i,i]=>o, i] => o"
    "iterates_replacement(M,isF,v) ==
       \<forall>n[M]. n\<in>nat --> 
          wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))"
 
-  is_iterates :: "[i=>o, [i,i]=>o, i, i, i] => o"
-    "is_iterates(M,isF,v,n,Z) == 
-      \<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
-                       is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)"
-
 lemma (in M_basic) iterates_MH_abs:
   "[| relation1(M,isF,F); M(n); M(g); M(z) |] 
    ==> iterates_MH(M,isF,v,n,g,z) <-> z = nat_case(v, \<lambda>m. F(g`m), n)"
diff -r bc63c3b2b3e7 -r 22dce9134953 src/ZF/Constructible/Formula.thy
--- a/src/ZF/Constructible/Formula.thy	Wed Oct 30 12:18:23 2002 +0100
+++ b/src/ZF/Constructible/Formula.thy	Wed Oct 30 12:44:18 2002 +0100
@@ -246,12 +246,12 @@
 subsection{*Renaming Some de Bruijn Variables*}
 
 constdefs incr_var :: "[i,i]=>i"
-    "incr_var(x,lev) == if x<lev then x else succ(x)"
+    "incr_var(x,nq) == if x<nq then x else succ(x)"
 
-lemma incr_var_lt: "x<lev ==> incr_var(x,lev) = x"
+lemma incr_var_lt: "x<nq ==> incr_var(x,nq) = x"
 by (simp add: incr_var_def)
 
-lemma incr_var_le: "lev\<le>x ==> incr_var(x,lev) = succ(x)"
+lemma incr_var_le: "nq\<le>x ==> incr_var(x,nq) = succ(x)"
 apply (simp add: incr_var_def) 
 apply (blast dest: lt_trans1) 
 done
@@ -259,19 +259,19 @@
 consts   incr_bv :: "i=>i"
 primrec
   "incr_bv(Member(x,y)) = 
-      (\<lambda>lev \<in> nat. Member (incr_var(x,lev), incr_var(y,lev)))"
+      (\<lambda>nq \<in> nat. Member (incr_var(x,nq), incr_var(y,nq)))"
 
   "incr_bv(Equal(x,y)) = 
-      (\<lambda>lev \<in> nat. Equal (incr_var(x,lev), incr_var(y,lev)))"
+      (\<lambda>nq \<in> nat. Equal (incr_var(x,nq), incr_var(y,nq)))"
 
   "incr_bv(Nand(p,q)) =
-      (\<lambda>lev \<in> nat. Nand (incr_bv(p)`lev, incr_bv(q)`lev))"
+      (\<lambda>nq \<in> nat. Nand (incr_bv(p)`nq, incr_bv(q)`nq))"
 
   "incr_bv(Forall(p)) = 
-      (\<lambda>lev \<in> nat. Forall (incr_bv(p) ` succ(lev)))"
+      (\<lambda>nq \<in> nat. Forall (incr_bv(p) ` succ(nq)))"
 
 
-lemma [TC]: "x \<in> nat ==> incr_var(x,lev) \<in> nat"
+lemma [TC]: "x \<in> nat ==> incr_var(x,nq) \<in> nat"
 by (simp add: incr_var_def) 
 
 lemma incr_bv_type [TC]: "p \<in> formula ==> incr_bv(p) \<in> nat -> formula"
@@ -294,8 +294,8 @@
 
 (*the following two lemmas prevent huge case splits in arity_incr_bv_lemma*)
 lemma incr_var_lemma:
-     "[| x \<in> nat; y \<in> nat; lev \<le> x |]
-      ==> succ(x) \<union> incr_var(y,lev) = succ(x \<union> y)"
+     "[| x \<in> nat; y \<in> nat; nq \<le> x |]
+      ==> succ(x) \<union> incr_var(y,nq) = succ(x \<union> y)"
 apply (simp add: incr_var_def Ord_Un_if, auto)
   apply (blast intro: leI)
  apply (simp add: not_lt_iff_le)  
@@ -757,7 +757,7 @@
 subsubsection{* Unions *}
 
 lemma Union_in_Lset:
-     "X \<in> Lset(j) ==> Union(X) \<in> Lset(succ(j))"
+     "X \<in> Lset(i) ==> Union(X) \<in> Lset(succ(i))"
 apply (insert Transset_Lset)
 apply (rule LsetI [OF succI1])
 apply (simp add: Transset_def DPow_def) 
@@ -769,17 +769,8 @@
 apply (simp add: succ_Un_distrib [symmetric], blast) 
 done
 
-lemma Union_in_LLimit:
-     "[| X: Lset(i);  Limit(i) |] ==> Union(X) : Lset(i)"
-apply (rule Limit_LsetE, assumption+)
-apply (blast intro: Limit_has_succ lt_LsetI Union_in_Lset)
-done
-
 theorem Union_in_L: "L(X) ==> L(Union(X))"
-apply (simp add: L_def, clarify) 
-apply (drule Ord_imp_greater_Limit) 
-apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord) 
-done
+by (simp add: L_def, blast dest: Union_in_Lset) 
 
 subsubsection{* Finite sets and ordered pairs *}
 
diff -r bc63c3b2b3e7 -r 22dce9134953 src/ZF/Constructible/Rank_Separation.thy
--- a/src/ZF/Constructible/Rank_Separation.thy	Wed Oct 30 12:18:23 2002 +0100
+++ b/src/ZF/Constructible/Rank_Separation.thy	Wed Oct 30 12:44:18 2002 +0100
@@ -10,7 +10,8 @@
 
 
 text{*This theory proves all instances needed for locales
-       @{text "M_ordertype"} and  @{text "M_wfrank"}*}
+ @{text "M_ordertype"} and  @{text "M_wfrank"}.  But the material is not
+ needed for proving the relative consistency of AC.*}
 
 subsection{*The Locale @{text "M_ordertype"}*}
 
@@ -27,11 +28,9 @@
      "[| 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 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 (rule imp_iff_sats)
-apply (rule_tac env = "[x,A,f,r]" in mem_iff_sats)
+apply (rule gen_separation_multi [OF well_ord_iso_Reflects, of "{A,f,r}"], 
+       auto)
+apply (rule_tac env="[A,f,r]" in DPow_LsetI)
 apply (rule sep_rules | simp)+
 done
 
@@ -53,12 +52,9 @@
       ==> 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 gen_separation [OF obase_reflects, of "{A,r}"], simp)
-apply (drule mem_Lset_imp_subset_Lset, clarsimp)
-apply (rule DPow_LsetI)
-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)+
+apply (rule gen_separation_multi [OF obase_reflects, of "{A,r}"], auto)
+apply (rule_tac env="[A,r]" in DPow_LsetI)
+apply (rule ordinal_iff_sats sep_rules | simp)+
 done
 
 
@@ -81,11 +77,8 @@
                               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 gen_separation [OF obase_equals_reflects, of "{A,r}"], simp)
-apply (drule mem_Lset_imp_subset_Lset, clarsimp)
-apply (rule DPow_LsetI)
-apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+
-apply (rule_tac env = "[x,A,r]" in mem_iff_sats)
+apply (rule gen_separation_multi [OF obase_equals_reflects, of "{A,r}"], auto)
+apply (rule_tac env="[A,r]" in DPow_LsetI)
 apply (rule sep_rules | simp)+
 done
 
@@ -110,12 +103,8 @@
              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 (rename_tac B)
-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 (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[a,z,A,B,r]" in mem_iff_sats)
+apply (rule_tac u="{A,r,B}" in gen_separation_multi [OF omap_reflects], auto)
+apply (rule_tac env="[A,B,r]" in DPow_LsetI)
 apply (rule sep_rules | simp)+
 done
 
@@ -157,10 +146,8 @@
       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 gen_separation [OF wfrank_Reflects], simp)
-apply (rule DPow_LsetI)
-apply (rule ball_iff_sats imp_iff_sats)+
-apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats)
-apply (rule sep_rules is_recfun_iff_sats | simp)+
+apply (rule_tac env="[r]" in DPow_LsetI)
+apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+
 done
 
 
@@ -188,14 +175,11 @@
                         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_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 (rule bex_iff_sats ball_iff_sats conj_iff_sats)+
-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)+
+apply (rule_tac u="{r,B}" 
+         in gen_separation_multi [OF wfrank_replacement_Reflects], 
+       auto)
+apply (rule_tac env="[r,B]" in DPow_LsetI)
+apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+
 done
 
 
@@ -225,10 +209,8 @@
              M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
              ordinal(L,rangef)))"
 apply (rule gen_separation [OF Ord_wfrank_Reflects], simp)
-apply (rule DPow_LsetI)
-apply (rule ball_iff_sats imp_iff_sats)+
-apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats)
-apply (rule sep_rules is_recfun_iff_sats | simp)+
+apply (rule_tac env="[r]" in DPow_LsetI)
+apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+
 done
 
 
diff -r bc63c3b2b3e7 -r 22dce9134953 src/ZF/Constructible/Rec_Separation.thy
--- a/src/ZF/Constructible/Rec_Separation.thy	Wed Oct 30 12:18:23 2002 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy	Wed Oct 30 12:44:18 2002 +0100
@@ -75,11 +75,10 @@
 text{*Separation for @{term "rtrancl(r)"}.*}
 lemma rtrancl_separation:
      "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))"
-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 (rule_tac env = "[x,r,A]" in rtran_closure_mem_iff_sats)
-apply (rule sep_rules | simp)+
+apply (rule gen_separation_multi [OF rtran_closure_mem_reflection, of "{r,A}"],
+       auto)
+apply (rule_tac env="[r,A]" in DPow_LsetI)
+apply (rule rtran_closure_mem_iff_sats sep_rules | simp)+
 done
 
 
@@ -167,11 +166,9 @@
           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 gen_separation [OF wellfounded_trancl_reflects, of "{r,Z}"], simp)
-apply (drule mem_Lset_imp_subset_Lset, clarsimp)
-apply (rule DPow_LsetI)
-apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[w,x,r,Z]" in mem_iff_sats)
+apply (rule gen_separation_multi [OF wellfounded_trancl_reflects, of "{r,Z}"],
+       auto)
+apply (rule_tac env="[r,Z]" in DPow_LsetI)
 apply (rule sep_rules tran_closure_iff_sats | simp)+
 done
 
@@ -214,14 +211,10 @@
    "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 (rename_tac B)
 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 (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,x,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
+         in gen_separation_multi [OF list_replacement1_Reflects], 
+       auto simp add: nonempty)
+apply (rule_tac env="[B,A,n,0,Memrel(succ(n))]" in DPow_LsetI)
 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
@@ -240,14 +233,10 @@
    "L(A) ==> strong_replacement(L,
          \<lambda>n y. n\<in>nat & is_iterates(L, is_list_functor(L,A), 0, n, y))"
 apply (rule strong_replacementI)
-apply (rename_tac B)
 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 (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,x,A,B,0,nat]" in mem_iff_sats)
+         in gen_separation_multi [OF list_replacement2_Reflects], 
+       auto simp add: L_nat nonempty)
+apply (rule_tac env="[A,B,0,nat]" in DPow_LsetI)
 apply (rule sep_rules list_functor_iff_sats is_iterates_iff_sats | simp)+
 done
 
@@ -273,14 +262,10 @@
    "iterates_replacement(L, is_formula_functor(L), 0)"
 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
 apply (rule strong_replacementI)
-apply (rename_tac B)
 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 (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,x,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
+         in gen_separation_multi [OF formula_replacement1_Reflects], 
+       auto simp add: nonempty)
+apply (rule_tac env="[n,B,0,Memrel(succ(n))]" in DPow_LsetI)
 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
@@ -298,14 +283,10 @@
    "strong_replacement(L,
          \<lambda>n y. n\<in>nat & is_iterates(L, is_formula_functor(L), 0, n, y))"
 apply (rule strong_replacementI)
-apply (rename_tac B)
 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 (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,x,B,0,nat]" in mem_iff_sats)
+         in gen_separation_multi [OF formula_replacement2_Reflects], 
+       auto simp add: nonempty L_nat)
+apply (rule_tac env="[B,0,nat]" in DPow_LsetI)
 apply (rule sep_rules formula_functor_iff_sats is_iterates_iff_sats | simp)+
 done
 
@@ -368,13 +349,10 @@
    "L(w) ==> iterates_replacement(L, is_tl(L), w)"
 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
 apply (rule strong_replacementI)
-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 (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,x,A,w,Memrel(succ(n))]" in mem_iff_sats)
+apply (rule_tac u="{B,w,Memrel(succ(n))}" 
+         in gen_separation_multi [OF nth_replacement_Reflects], 
+       auto)
+apply (rule_tac env="[B,w,Memrel(succ(n))]" in DPow_LsetI)
 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
@@ -428,13 +406,9 @@
    "L(A) ==> iterates_replacement(L, big_union(L), A)"
 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
 apply (rule strong_replacementI)
-apply (rename_tac B)
 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 (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,x,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
+         in gen_separation_multi [OF eclose_replacement1_Reflects], auto)
+apply (rule_tac env="[B,A,n,Memrel(succ(n))]" in DPow_LsetI)
 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
@@ -452,13 +426,10 @@
    "L(A) ==> strong_replacement(L,
          \<lambda>n y. n\<in>nat & is_iterates(L, big_union(L), A, n, y))"
 apply (rule strong_replacementI)
-apply (rename_tac B)
 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 (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,x,A,B,nat]" in mem_iff_sats)
+         in gen_separation_multi [OF eclose_replacement2_Reflects],
+       auto simp add: L_nat)
+apply (rule_tac env="[A,B,nat]" in DPow_LsetI)
 apply (rule sep_rules is_iterates_iff_sats big_union_iff_sats | simp)+
 done
 
diff -r bc63c3b2b3e7 -r 22dce9134953 src/ZF/Constructible/Relative.thy
--- a/src/ZF/Constructible/Relative.thy	Wed Oct 30 12:18:23 2002 +0100
+++ b/src/ZF/Constructible/Relative.thy	Wed Oct 30 12:44:18 2002 +0100
@@ -627,7 +627,7 @@
 
 text{*Probably the premise and conclusion are equivalent*}
 lemma (in M_trivial) strong_replacementI [rule_format]:
-    "[| \<forall>A[M]. separation(M, %u. \<exists>x[M]. x\<in>A & P(x,u)) |]
+    "[| \<forall>B[M]. separation(M, %u. \<exists>x[M]. x\<in>B & P(x,u)) |]
      ==> strong_replacement(M,P)"
 apply (simp add: strong_replacement_def, clarify)
 apply (frule replacementD [OF replacement], assumption, clarify)
diff -r bc63c3b2b3e7 -r 22dce9134953 src/ZF/Constructible/Satisfies_absolute.thy
--- a/src/ZF/Constructible/Satisfies_absolute.thy	Wed Oct 30 12:18:23 2002 +0100
+++ b/src/ZF/Constructible/Satisfies_absolute.thy	Wed Oct 30 12:44:18 2002 +0100
@@ -8,6 +8,7 @@
 theory Satisfies_absolute = Datatype_absolute + Rec_Separation: 
 
 
+subsection {*More Internalization*}
 
 subsubsection{*The Formula @{term is_depth}, Internalized*}
 
@@ -823,14 +824,10 @@
               is_bool_of_o(L, nx \<in> ny, bo) &
               pair(L, env, bo, z))"
 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 (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[v,u,list(A),B,x,y]" in mem_iff_sats) 
+         in gen_separation_multi [OF Member_Reflects], 
+       auto simp add: nat_into_M list_closed)
+apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
 apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
 done
 
@@ -857,14 +854,10 @@
               is_bool_of_o(L, nx = ny, bo) &
               pair(L, env, bo, z))"
 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 (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[v,u,list(A),B,x,y]" in mem_iff_sats) 
+         in gen_separation_multi [OF Equal_Reflects], 
+       auto simp add: nat_into_M list_closed)
+apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
 apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
 done
 
@@ -893,13 +886,10 @@
                is_and(L,rpe,rqe,andpq) & is_not(L,andpq,notpq) & 
                env \<in> list(A) & pair(L, env, notpq, z))"
 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 (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,x,list(A),B,rp,rq]" in mem_iff_sats) 
+apply (rule_tac u="{list(A),B,rp,rq}" 
+         in gen_separation_multi [OF Nand_Reflects],
+       auto simp add: list_closed)
+apply (rule_tac env="[list(A),B,rp,rq]" in DPow_LsetI)
 apply (rule sep_rules is_and_iff_sats is_not_iff_sats | simp)+
 done
 
@@ -935,13 +925,10 @@
                             bo) &
 	      pair(L,env,bo,z))"
 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 (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,x,A,list(A),B,rp]" in mem_iff_sats)
+apply (rule_tac u="{A,list(A),B,rp}" 
+         in gen_separation_multi [OF Forall_Reflects],
+       auto simp add: list_closed)
+apply (rule_tac env="[A,list(A),B,rp]" in DPow_LsetI)
 apply (rule sep_rules is_bool_of_o_iff_sats Cons_iff_sats | simp)+
 done
 
@@ -960,14 +947,10 @@
    "[|n \<in> nat; L(A)|] ==> transrec_replacement(L, satisfies_MH(L,A), n)"
 apply (rule transrec_replacementI, simp add: nat_into_M) 
 apply (rule strong_replacementI)
-apply (rename_tac B)
 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 (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,x,A,n,B,Memrel(eclose({n}))]" in mem_iff_sats)
+         in gen_separation_multi [OF formula_rec_replacement_Reflects],
+       auto simp add: nat_into_M)
+apply (rule_tac env="[B,A,n,Memrel(eclose({n}))]" in DPow_LsetI)
 apply (rule sep_rules satisfies_MH_iff_sats is_wfrec_iff_sats | simp)+
 done
 
@@ -1006,13 +989,10 @@
                                   satisfies_is_d(L,A,g), x, c) &
              pair(L, x, c, y)))" 
 apply (rule strong_replacementI)
-apply (rename_tac B)
 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 (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,x,A,g,B]" in mem_iff_sats)
+         in gen_separation_multi [OF formula_rec_lambda_replacement_Reflects], 
+       auto)
+apply (rule_tac env="[A,g,B]" in DPow_LsetI)
 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 bc63c3b2b3e7 -r 22dce9134953 src/ZF/Constructible/Separation.thy
--- a/src/ZF/Constructible/Separation.thy	Wed Oct 30 12:18:23 2002 +0100
+++ b/src/ZF/Constructible/Separation.thy	Wed Oct 30 12:44:18 2002 +0100
@@ -51,7 +51,7 @@
 done
 
 text{*Encapsulates the standard proof script for proving instances of 
-Separation.  Typically @{term u} is a finite enumeration.*}
+      Separation.*}
 lemma gen_separation:
  assumes reflection: "REFLECTS [P,Q]"
      and Lu:         "L(u)"
@@ -65,7 +65,22 @@
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2, clarify)
 apply (rule collI)
-apply assumption;  
+apply assumption
+done
+
+text{*As above, but typically @{term u} is a finite enumeration such as
+  @{term "{a,b}"}; thus the new subgoal gets the assumption
+  @{term "{a,b} \<subseteq> Lset(i)"}, which is logically equivalent to 
+  @{term "a \<in> Lset(i)"} and @{term "b \<in> Lset(i)"}.*}
+lemma gen_separation_multi:
+ assumes reflection: "REFLECTS [P,Q]"
+     and Lu:         "L(u)"
+     and collI: "!!j. u \<subseteq> Lset(j)
+                \<Longrightarrow> Collect(Lset(j), Q(j)) \<in> DPow(Lset(j))"
+ shows "separation(L,P)"
+apply (rule gen_separation [OF reflection Lu])
+apply (drule mem_Lset_imp_subset_Lset)
+apply (erule collI) 
 done
 
 
@@ -80,6 +95,8 @@
      "L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A --> x\<in>y)"
 apply (rule gen_separation [OF Inter_Reflects], simp)
 apply (rule DPow_LsetI)
+ txt{*I leave this one example of a manual proof.  The tedium of manually
+      instantiating @{term i}, @{term j} and @{term env} is obvious. *}
 apply (rule ball_iff_sats)
 apply (rule imp_iff_sats)
 apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats)
@@ -96,9 +113,7 @@
 lemma Diff_separation:
      "L(B) ==> separation(L, \<lambda>x. x \<notin> B)"
 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_tac env="[B]" in DPow_LsetI)
 apply (rule sep_rules | simp)+
 done
 
@@ -113,12 +128,8 @@
 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 gen_separation [OF cartprod_Reflects, of "{A,B}"], simp)
-apply (drule mem_Lset_imp_subset_Lset, clarsimp)
-apply (rule DPow_LsetI)
-apply (rule bex_iff_sats)
-apply (rule conj_iff_sats)
-apply (rule_tac i=0 and j=2 and env="[x,z,A,B]" in mem_iff_sats, simp_all)
+apply (rule gen_separation_multi [OF cartprod_Reflects, of "{A,B}"], auto)
+apply (rule_tac env="[A,B]" in DPow_LsetI)
 apply (rule sep_rules | simp)+
 done
 
@@ -132,12 +143,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 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)
-apply (rule_tac env="[p,y,A,r]" in mem_iff_sats)
+apply (rule gen_separation_multi [OF image_Reflects, of "{A,r}"], auto)
+apply (rule_tac env="[A,r]" in DPow_LsetI)
 apply (rule sep_rules | simp)+
 done
 
@@ -154,10 +161,7 @@
      "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 gen_separation [OF converse_Reflects], simp)
-apply (rule DPow_LsetI)
-apply (rule bex_iff_sats)
-apply (rule conj_iff_sats)
-apply (rule_tac i=0 and j=2 and env="[p,z,r]" in mem_iff_sats, simp_all)
+apply (rule_tac env="[r]" in DPow_LsetI)
 apply (rule sep_rules | simp)+
 done
 
@@ -172,10 +176,7 @@
 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 gen_separation [OF restrict_Reflects], simp)
-apply (rule DPow_LsetI)
-apply (rule bex_iff_sats)
-apply (rule conj_iff_sats)
-apply (rule_tac i=0 and j=2 and env="[x,z,A]" in mem_iff_sats, simp_all)
+apply (rule_tac env="[A]" in DPow_LsetI)
 apply (rule sep_rules | simp)+
 done
 
@@ -196,15 +197,16 @@
       ==> 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 gen_separation [OF comp_Reflects, of "{r,s}"], simp)
-apply (drule mem_Lset_imp_subset_Lset, clarsimp)
-apply (rule DPow_LsetI)
-apply (rule bex_iff_sats)+
-apply (rule conj_iff_sats)
-apply (rule_tac env="[z,y,x,xz,r,s]" in pair_iff_sats)
+apply (rule gen_separation_multi [OF comp_Reflects, of "{r,s}"], auto)
+txt{*Subgoals after applying general ``separation'' rule:
+     @{subgoals[display,indent=0,margin=65]}*}
+apply (rule_tac env="[r,s]" in DPow_LsetI)
+txt{*Subgoals ready for automatic synthesis of a formula:
+     @{subgoals[display,indent=0,margin=65]}*}
 apply (rule sep_rules | simp)+
 done
 
+
 subsection{*Separation for Predecessors in an Order*}
 
 lemma pred_Reflects:
@@ -214,12 +216,8 @@
 
 lemma pred_separation:
      "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"
-apply (rule gen_separation [OF pred_Reflects, of "{r,x}"], simp)
-apply (drule mem_Lset_imp_subset_Lset, clarsimp)
-apply (rule DPow_LsetI)
-apply (rule bex_iff_sats)
-apply (rule conj_iff_sats)
-apply (rule_tac env = "[p,y,r,x]" in mem_iff_sats)
+apply (rule gen_separation_multi [OF pred_Reflects, of "{r,x}"], auto)
+apply (rule_tac env="[r,x]" in DPow_LsetI)
 apply (rule sep_rules | simp)+
 done
 
@@ -234,9 +232,7 @@
 lemma Memrel_separation:
      "separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
 apply (rule gen_separation [OF Memrel_Reflects nonempty])
-apply (rule DPow_LsetI)
-apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[y,x,z]" in pair_iff_sats)
+apply (rule_tac env="[]" in DPow_LsetI)
 apply (rule sep_rules | simp)+
 done
 
@@ -259,12 +255,9 @@
                 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_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 (rule bex_iff_sats)
-apply (rule conj_iff_sats)
-apply (rule_tac env = "[p,z,n,A]" in mem_iff_sats)
+apply (rule_tac u="{n,B}" in gen_separation_multi [OF funspace_succ_Reflects], 
+       auto)
+apply (rule_tac env="[n,B]" in DPow_LsetI)
 apply (rule sep_rules | simp)+
 done
 
@@ -290,11 +283,9 @@
                 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 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 (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[xa,x,r,f,g,a,b]" in pair_iff_sats)
+apply (rule gen_separation_multi [OF is_recfun_reflects, of "{r,f,g,a,b}"], 
+            auto)
+apply (rule_tac env="[r,f,g,a,b]" in DPow_LsetI)
 apply (rule sep_rules | simp)+
 done