simpler separation/replacement proofs
authorpaulson
Wed Oct 30 12:44:18 2002 +0100 (2002-10-30)
changeset 1368722dce9134953
parent 13686 bc63c3b2b3e7
child 13688 a0b16d42d489
simpler separation/replacement proofs
src/ZF/Constructible/DPow_absolute.thy
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Formula.thy
src/ZF/Constructible/Rank_Separation.thy
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/Satisfies_absolute.thy
src/ZF/Constructible/Separation.thy
     1.1 --- a/src/ZF/Constructible/DPow_absolute.thy	Wed Oct 30 12:18:23 2002 +0100
     1.2 +++ b/src/ZF/Constructible/DPow_absolute.thy	Wed Oct 30 12:44:18 2002 +0100
     1.3 @@ -181,7 +181,7 @@
     1.4  done
     1.5  
     1.6  
     1.7 -subsection{*Additional Constraints on the Class Model @{term M}*}
     1.8 +subsection{*A Locale for Relativizing the Operator @{term DPow'}*}
     1.9  
    1.10  locale M_DPow = M_satisfies +
    1.11   assumes sep:
    1.12 @@ -242,12 +242,10 @@
    1.13  lemma DPow_separation:
    1.14      "[| L(A); env \<in> list(A); p \<in> formula |]
    1.15       ==> separation(L, \<lambda>x. is_DPow_body(L,A,env,p,x))"
    1.16 -apply (rule gen_separation [OF DPow_body_reflection, of "{A,env,p}"], 
    1.17 -       blast intro: transL)
    1.18 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    1.19 -apply (rule DPow_LsetI)
    1.20 -apply (rule_tac env = "[x,A,env,p]" in DPow_body_iff_sats)
    1.21 -apply (rule sep_rules | simp)+
    1.22 +apply (rule gen_separation_multi [OF DPow_body_reflection, of "{A,env,p}"], 
    1.23 +       auto intro: transL)
    1.24 +apply (rule_tac env="[A,env,p]" in DPow_LsetI)
    1.25 +apply (rule DPow_body_iff_sats sep_rules | simp)+
    1.26  done
    1.27  
    1.28  
    1.29 @@ -276,14 +274,11 @@
    1.30                    pair(L,env,p,ep) & 
    1.31                    is_Collect(L, A, \<lambda>x. is_DPow_body(L,A,env,p,x), z))"
    1.32  apply (rule strong_replacementI)
    1.33 -apply (rename_tac B)
    1.34 -apply (rule_tac u="{A,B}" in gen_separation [OF DPow_replacement_Reflects], 
    1.35 -       simp)
    1.36 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    1.37 +apply (rule_tac u="{A,B}" 
    1.38 +         in gen_separation_multi [OF DPow_replacement_Reflects], 
    1.39 +       auto)
    1.40  apply (unfold is_Collect_def) 
    1.41 -apply (rule DPow_LsetI)
    1.42 -apply (rule bex_iff_sats conj_iff_sats)+
    1.43 -apply (rule_tac env = "[u,x,A,B]" in mem_iff_sats)
    1.44 +apply (rule_tac env="[A,B]" in DPow_LsetI)
    1.45  apply (rule sep_rules mem_formula_iff_sats mem_list_iff_sats 
    1.46              DPow_body_iff_sats | simp)+
    1.47  done
    1.48 @@ -452,13 +447,8 @@
    1.49               mem_list_reflection Collect_reflection DPow_body_reflection)
    1.50  done
    1.51  
    1.52 -(*????????????????move up*)
    1.53  
    1.54 -
    1.55 -
    1.56 -
    1.57 -
    1.58 -subsection{*Additional Constraints on the Class Model @{term M}*}
    1.59 +subsection{*A Locale for Relativizing the Operator @{term Lset}*}
    1.60  
    1.61  constdefs
    1.62    transrec_body :: "[i=>o,i,i,i,i] => o"
    1.63 @@ -510,7 +500,7 @@
    1.64  done
    1.65  
    1.66  
    1.67 -
    1.68 +text{*Relativization of the Operator @{term Lset}*}
    1.69  constdefs
    1.70  
    1.71    is_Lset :: "[i=>o, i, i] => o"
    1.72 @@ -534,7 +524,6 @@
    1.73  
    1.74  subsection{*Instantiating the Locale @{text M_Lset}*}
    1.75  
    1.76 -
    1.77  subsubsection{*The First Instance of Replacement*}
    1.78  
    1.79  lemma strong_rep_Reflects:
    1.80 @@ -548,12 +537,9 @@
    1.81     "[|L(x); L(g)|] ==> strong_replacement(L, \<lambda>y z. transrec_body(L,g,x,y,z))"
    1.82  apply (unfold transrec_body_def)  
    1.83  apply (rule strong_replacementI) 
    1.84 -apply (rename_tac B)  
    1.85 -apply (rule_tac u="{x,g,B}" in gen_separation [OF strong_rep_Reflects], simp)
    1.86 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    1.87 -apply (rule DPow_LsetI)
    1.88 -apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
    1.89 -apply (rule_tac env = "[v,u,x,g,B]" in mem_iff_sats) 
    1.90 +apply (rule_tac u="{x,g,B}" 
    1.91 +         in gen_separation_multi [OF strong_rep_Reflects], auto)
    1.92 +apply (rule_tac env="[x,g,B]" in DPow_LsetI)
    1.93  apply (rule sep_rules DPow'_iff_sats | simp)+
    1.94  done
    1.95  
    1.96 @@ -590,13 +576,9 @@
    1.97  apply (rule transrec_replacementI, assumption)
    1.98  apply (unfold transrec_body_def)  
    1.99  apply (rule strong_replacementI)
   1.100 -apply (rename_tac B)
   1.101  apply (rule_tac u="{j,B,Memrel(eclose({j}))}" 
   1.102 -         in gen_separation [OF transrec_rep_Reflects], simp)
   1.103 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   1.104 -apply (rule DPow_LsetI)
   1.105 -apply (rule bex_iff_sats conj_iff_sats)+
   1.106 -apply (rule_tac env = "[v,x,j,B,Memrel(eclose({j}))]" in mem_iff_sats)
   1.107 +         in gen_separation_multi [OF transrec_rep_Reflects], auto)
   1.108 +apply (rule_tac env="[j,B,Memrel(eclose({j}))]" in DPow_LsetI)
   1.109  apply (rule sep_rules is_wfrec_iff_sats Replace_iff_sats DPow'_iff_sats | 
   1.110         simp)+
   1.111  done
     2.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Wed Oct 30 12:18:23 2002 +0100
     2.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Wed Oct 30 12:44:18 2002 +0100
     2.3 @@ -120,16 +120,16 @@
     2.4          is_nat_case(M, v, \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & isF(gm,u),
     2.5                      n, z)"
     2.6  
     2.7 +  is_iterates :: "[i=>o, [i,i]=>o, i, i, i] => o"
     2.8 +    "is_iterates(M,isF,v,n,Z) == 
     2.9 +      \<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
    2.10 +                       is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)"
    2.11 +
    2.12    iterates_replacement :: "[i=>o, [i,i]=>o, i] => o"
    2.13     "iterates_replacement(M,isF,v) ==
    2.14        \<forall>n[M]. n\<in>nat --> 
    2.15           wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))"
    2.16  
    2.17 -  is_iterates :: "[i=>o, [i,i]=>o, i, i, i] => o"
    2.18 -    "is_iterates(M,isF,v,n,Z) == 
    2.19 -      \<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
    2.20 -                       is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)"
    2.21 -
    2.22  lemma (in M_basic) iterates_MH_abs:
    2.23    "[| relation1(M,isF,F); M(n); M(g); M(z) |] 
    2.24     ==> iterates_MH(M,isF,v,n,g,z) <-> z = nat_case(v, \<lambda>m. F(g`m), n)"
     3.1 --- a/src/ZF/Constructible/Formula.thy	Wed Oct 30 12:18:23 2002 +0100
     3.2 +++ b/src/ZF/Constructible/Formula.thy	Wed Oct 30 12:44:18 2002 +0100
     3.3 @@ -246,12 +246,12 @@
     3.4  subsection{*Renaming Some de Bruijn Variables*}
     3.5  
     3.6  constdefs incr_var :: "[i,i]=>i"
     3.7 -    "incr_var(x,lev) == if x<lev then x else succ(x)"
     3.8 +    "incr_var(x,nq) == if x<nq then x else succ(x)"
     3.9  
    3.10 -lemma incr_var_lt: "x<lev ==> incr_var(x,lev) = x"
    3.11 +lemma incr_var_lt: "x<nq ==> incr_var(x,nq) = x"
    3.12  by (simp add: incr_var_def)
    3.13  
    3.14 -lemma incr_var_le: "lev\<le>x ==> incr_var(x,lev) = succ(x)"
    3.15 +lemma incr_var_le: "nq\<le>x ==> incr_var(x,nq) = succ(x)"
    3.16  apply (simp add: incr_var_def) 
    3.17  apply (blast dest: lt_trans1) 
    3.18  done
    3.19 @@ -259,19 +259,19 @@
    3.20  consts   incr_bv :: "i=>i"
    3.21  primrec
    3.22    "incr_bv(Member(x,y)) = 
    3.23 -      (\<lambda>lev \<in> nat. Member (incr_var(x,lev), incr_var(y,lev)))"
    3.24 +      (\<lambda>nq \<in> nat. Member (incr_var(x,nq), incr_var(y,nq)))"
    3.25  
    3.26    "incr_bv(Equal(x,y)) = 
    3.27 -      (\<lambda>lev \<in> nat. Equal (incr_var(x,lev), incr_var(y,lev)))"
    3.28 +      (\<lambda>nq \<in> nat. Equal (incr_var(x,nq), incr_var(y,nq)))"
    3.29  
    3.30    "incr_bv(Nand(p,q)) =
    3.31 -      (\<lambda>lev \<in> nat. Nand (incr_bv(p)`lev, incr_bv(q)`lev))"
    3.32 +      (\<lambda>nq \<in> nat. Nand (incr_bv(p)`nq, incr_bv(q)`nq))"
    3.33  
    3.34    "incr_bv(Forall(p)) = 
    3.35 -      (\<lambda>lev \<in> nat. Forall (incr_bv(p) ` succ(lev)))"
    3.36 +      (\<lambda>nq \<in> nat. Forall (incr_bv(p) ` succ(nq)))"
    3.37  
    3.38  
    3.39 -lemma [TC]: "x \<in> nat ==> incr_var(x,lev) \<in> nat"
    3.40 +lemma [TC]: "x \<in> nat ==> incr_var(x,nq) \<in> nat"
    3.41  by (simp add: incr_var_def) 
    3.42  
    3.43  lemma incr_bv_type [TC]: "p \<in> formula ==> incr_bv(p) \<in> nat -> formula"
    3.44 @@ -294,8 +294,8 @@
    3.45  
    3.46  (*the following two lemmas prevent huge case splits in arity_incr_bv_lemma*)
    3.47  lemma incr_var_lemma:
    3.48 -     "[| x \<in> nat; y \<in> nat; lev \<le> x |]
    3.49 -      ==> succ(x) \<union> incr_var(y,lev) = succ(x \<union> y)"
    3.50 +     "[| x \<in> nat; y \<in> nat; nq \<le> x |]
    3.51 +      ==> succ(x) \<union> incr_var(y,nq) = succ(x \<union> y)"
    3.52  apply (simp add: incr_var_def Ord_Un_if, auto)
    3.53    apply (blast intro: leI)
    3.54   apply (simp add: not_lt_iff_le)  
    3.55 @@ -757,7 +757,7 @@
    3.56  subsubsection{* Unions *}
    3.57  
    3.58  lemma Union_in_Lset:
    3.59 -     "X \<in> Lset(j) ==> Union(X) \<in> Lset(succ(j))"
    3.60 +     "X \<in> Lset(i) ==> Union(X) \<in> Lset(succ(i))"
    3.61  apply (insert Transset_Lset)
    3.62  apply (rule LsetI [OF succI1])
    3.63  apply (simp add: Transset_def DPow_def) 
    3.64 @@ -769,17 +769,8 @@
    3.65  apply (simp add: succ_Un_distrib [symmetric], blast) 
    3.66  done
    3.67  
    3.68 -lemma Union_in_LLimit:
    3.69 -     "[| X: Lset(i);  Limit(i) |] ==> Union(X) : Lset(i)"
    3.70 -apply (rule Limit_LsetE, assumption+)
    3.71 -apply (blast intro: Limit_has_succ lt_LsetI Union_in_Lset)
    3.72 -done
    3.73 -
    3.74  theorem Union_in_L: "L(X) ==> L(Union(X))"
    3.75 -apply (simp add: L_def, clarify) 
    3.76 -apply (drule Ord_imp_greater_Limit) 
    3.77 -apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord) 
    3.78 -done
    3.79 +by (simp add: L_def, blast dest: Union_in_Lset) 
    3.80  
    3.81  subsubsection{* Finite sets and ordered pairs *}
    3.82  
     4.1 --- a/src/ZF/Constructible/Rank_Separation.thy	Wed Oct 30 12:18:23 2002 +0100
     4.2 +++ b/src/ZF/Constructible/Rank_Separation.thy	Wed Oct 30 12:44:18 2002 +0100
     4.3 @@ -10,7 +10,8 @@
     4.4  
     4.5  
     4.6  text{*This theory proves all instances needed for locales
     4.7 -       @{text "M_ordertype"} and  @{text "M_wfrank"}*}
     4.8 + @{text "M_ordertype"} and  @{text "M_wfrank"}.  But the material is not
     4.9 + needed for proving the relative consistency of AC.*}
    4.10  
    4.11  subsection{*The Locale @{text "M_ordertype"}*}
    4.12  
    4.13 @@ -27,11 +28,9 @@
    4.14       "[| L(A); L(f); L(r) |]
    4.15        ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y[L]. (\<exists>p[L].
    4.16                       fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r)))"
    4.17 -apply (rule gen_separation [OF well_ord_iso_Reflects, of "{A,f,r}"], simp)
    4.18 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    4.19 -apply (rule DPow_LsetI)
    4.20 -apply (rule imp_iff_sats)
    4.21 -apply (rule_tac env = "[x,A,f,r]" in mem_iff_sats)
    4.22 +apply (rule gen_separation_multi [OF well_ord_iso_Reflects, of "{A,f,r}"], 
    4.23 +       auto)
    4.24 +apply (rule_tac env="[A,f,r]" in DPow_LsetI)
    4.25  apply (rule sep_rules | simp)+
    4.26  done
    4.27  
    4.28 @@ -53,12 +52,9 @@
    4.29        ==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
    4.30               ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
    4.31               order_isomorphism(L,par,r,x,mx,g))"
    4.32 -apply (rule gen_separation [OF obase_reflects, of "{A,r}"], simp)
    4.33 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    4.34 -apply (rule DPow_LsetI)
    4.35 -apply (rule bex_iff_sats conj_iff_sats)+
    4.36 -apply (rule_tac env = "[x,a,A,r]" in ordinal_iff_sats)
    4.37 -apply (rule sep_rules | simp)+
    4.38 +apply (rule gen_separation_multi [OF obase_reflects, of "{A,r}"], auto)
    4.39 +apply (rule_tac env="[A,r]" in DPow_LsetI)
    4.40 +apply (rule ordinal_iff_sats sep_rules | simp)+
    4.41  done
    4.42  
    4.43  
    4.44 @@ -81,11 +77,8 @@
    4.45                                ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
    4.46                                membership(L,y,my) & pred_set(L,A,x,r,pxr) &
    4.47                                order_isomorphism(L,pxr,r,y,my,g))))"
    4.48 -apply (rule gen_separation [OF obase_equals_reflects, of "{A,r}"], simp)
    4.49 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    4.50 -apply (rule DPow_LsetI)
    4.51 -apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+
    4.52 -apply (rule_tac env = "[x,A,r]" in mem_iff_sats)
    4.53 +apply (rule gen_separation_multi [OF obase_equals_reflects, of "{A,r}"], auto)
    4.54 +apply (rule_tac env="[A,r]" in DPow_LsetI)
    4.55  apply (rule sep_rules | simp)+
    4.56  done
    4.57  
    4.58 @@ -110,12 +103,8 @@
    4.59               ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
    4.60               pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
    4.61  apply (rule strong_replacementI)
    4.62 -apply (rename_tac B)
    4.63 -apply (rule_tac u="{A,r,B}" in gen_separation [OF omap_reflects], simp)
    4.64 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    4.65 -apply (rule DPow_LsetI)
    4.66 -apply (rule bex_iff_sats conj_iff_sats)+
    4.67 -apply (rule_tac env = "[a,z,A,B,r]" in mem_iff_sats)
    4.68 +apply (rule_tac u="{A,r,B}" in gen_separation_multi [OF omap_reflects], auto)
    4.69 +apply (rule_tac env="[A,B,r]" in DPow_LsetI)
    4.70  apply (rule sep_rules | simp)+
    4.71  done
    4.72  
    4.73 @@ -157,10 +146,8 @@
    4.74        separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
    4.75           ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))"
    4.76  apply (rule gen_separation [OF wfrank_Reflects], simp)
    4.77 -apply (rule DPow_LsetI)
    4.78 -apply (rule ball_iff_sats imp_iff_sats)+
    4.79 -apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats)
    4.80 -apply (rule sep_rules is_recfun_iff_sats | simp)+
    4.81 +apply (rule_tac env="[r]" in DPow_LsetI)
    4.82 +apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+
    4.83  done
    4.84  
    4.85  
    4.86 @@ -188,14 +175,11 @@
    4.87                          M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
    4.88                          is_range(L,f,y)))"
    4.89  apply (rule strong_replacementI)
    4.90 -apply (rule_tac u="{r,A}" in gen_separation [OF wfrank_replacement_Reflects], 
    4.91 -       simp)
    4.92 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    4.93 -apply (rule DPow_LsetI)
    4.94 -apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+
    4.95 -apply (rule_tac env = "[x,z,A,r]" in mem_iff_sats)
    4.96 -apply (rule sep_rules list.intros app_type tran_closure_iff_sats 
    4.97 -            is_recfun_iff_sats | simp)+
    4.98 +apply (rule_tac u="{r,B}" 
    4.99 +         in gen_separation_multi [OF wfrank_replacement_Reflects], 
   4.100 +       auto)
   4.101 +apply (rule_tac env="[r,B]" in DPow_LsetI)
   4.102 +apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+
   4.103  done
   4.104  
   4.105  
   4.106 @@ -225,10 +209,8 @@
   4.107               M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
   4.108               ordinal(L,rangef)))"
   4.109  apply (rule gen_separation [OF Ord_wfrank_Reflects], simp)
   4.110 -apply (rule DPow_LsetI)
   4.111 -apply (rule ball_iff_sats imp_iff_sats)+
   4.112 -apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats)
   4.113 -apply (rule sep_rules is_recfun_iff_sats | simp)+
   4.114 +apply (rule_tac env="[r]" in DPow_LsetI)
   4.115 +apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+
   4.116  done
   4.117  
   4.118  
     5.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Wed Oct 30 12:18:23 2002 +0100
     5.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Wed Oct 30 12:44:18 2002 +0100
     5.3 @@ -75,11 +75,10 @@
     5.4  text{*Separation for @{term "rtrancl(r)"}.*}
     5.5  lemma rtrancl_separation:
     5.6       "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))"
     5.7 -apply (rule gen_separation [OF rtran_closure_mem_reflection, of "{r,A}"], simp)
     5.8 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
     5.9 -apply (rule DPow_LsetI)
    5.10 -apply (rule_tac env = "[x,r,A]" in rtran_closure_mem_iff_sats)
    5.11 -apply (rule sep_rules | simp)+
    5.12 +apply (rule gen_separation_multi [OF rtran_closure_mem_reflection, of "{r,A}"],
    5.13 +       auto)
    5.14 +apply (rule_tac env="[r,A]" in DPow_LsetI)
    5.15 +apply (rule rtran_closure_mem_iff_sats sep_rules | simp)+
    5.16  done
    5.17  
    5.18  
    5.19 @@ -167,11 +166,9 @@
    5.20            separation (L, \<lambda>x.
    5.21                \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
    5.22                 w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)"
    5.23 -apply (rule gen_separation [OF wellfounded_trancl_reflects, of "{r,Z}"], simp)
    5.24 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    5.25 -apply (rule DPow_LsetI)
    5.26 -apply (rule bex_iff_sats conj_iff_sats)+
    5.27 -apply (rule_tac env = "[w,x,r,Z]" in mem_iff_sats)
    5.28 +apply (rule gen_separation_multi [OF wellfounded_trancl_reflects, of "{r,Z}"],
    5.29 +       auto)
    5.30 +apply (rule_tac env="[r,Z]" in DPow_LsetI)
    5.31  apply (rule sep_rules tran_closure_iff_sats | simp)+
    5.32  done
    5.33  
    5.34 @@ -214,14 +211,10 @@
    5.35     "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)"
    5.36  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
    5.37  apply (rule strong_replacementI)
    5.38 -apply (rename_tac B)
    5.39  apply (rule_tac u="{B,A,n,0,Memrel(succ(n))}" 
    5.40 -         in gen_separation [OF list_replacement1_Reflects], 
    5.41 -       simp add: nonempty)
    5.42 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    5.43 -apply (rule DPow_LsetI)
    5.44 -apply (rule bex_iff_sats conj_iff_sats)+
    5.45 -apply (rule_tac env = "[u,x,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
    5.46 +         in gen_separation_multi [OF list_replacement1_Reflects], 
    5.47 +       auto simp add: nonempty)
    5.48 +apply (rule_tac env="[B,A,n,0,Memrel(succ(n))]" in DPow_LsetI)
    5.49  apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
    5.50              is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
    5.51  done
    5.52 @@ -240,14 +233,10 @@
    5.53     "L(A) ==> strong_replacement(L,
    5.54           \<lambda>n y. n\<in>nat & is_iterates(L, is_list_functor(L,A), 0, n, y))"
    5.55  apply (rule strong_replacementI)
    5.56 -apply (rename_tac B)
    5.57  apply (rule_tac u="{A,B,0,nat}" 
    5.58 -         in gen_separation [OF list_replacement2_Reflects], 
    5.59 -       simp add: L_nat nonempty)
    5.60 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    5.61 -apply (rule DPow_LsetI)
    5.62 -apply (rule bex_iff_sats conj_iff_sats)+
    5.63 -apply (rule_tac env = "[u,x,A,B,0,nat]" in mem_iff_sats)
    5.64 +         in gen_separation_multi [OF list_replacement2_Reflects], 
    5.65 +       auto simp add: L_nat nonempty)
    5.66 +apply (rule_tac env="[A,B,0,nat]" in DPow_LsetI)
    5.67  apply (rule sep_rules list_functor_iff_sats is_iterates_iff_sats | simp)+
    5.68  done
    5.69  
    5.70 @@ -273,14 +262,10 @@
    5.71     "iterates_replacement(L, is_formula_functor(L), 0)"
    5.72  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
    5.73  apply (rule strong_replacementI)
    5.74 -apply (rename_tac B)
    5.75  apply (rule_tac u="{B,n,0,Memrel(succ(n))}" 
    5.76 -         in gen_separation [OF formula_replacement1_Reflects], 
    5.77 -       simp add: nonempty)
    5.78 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    5.79 -apply (rule DPow_LsetI)
    5.80 -apply (rule bex_iff_sats conj_iff_sats)+
    5.81 -apply (rule_tac env = "[u,x,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
    5.82 +         in gen_separation_multi [OF formula_replacement1_Reflects], 
    5.83 +       auto simp add: nonempty)
    5.84 +apply (rule_tac env="[n,B,0,Memrel(succ(n))]" in DPow_LsetI)
    5.85  apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
    5.86              is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
    5.87  done
    5.88 @@ -298,14 +283,10 @@
    5.89     "strong_replacement(L,
    5.90           \<lambda>n y. n\<in>nat & is_iterates(L, is_formula_functor(L), 0, n, y))"
    5.91  apply (rule strong_replacementI)
    5.92 -apply (rename_tac B)
    5.93  apply (rule_tac u="{B,0,nat}" 
    5.94 -         in gen_separation [OF formula_replacement2_Reflects], 
    5.95 -       simp add: nonempty L_nat)
    5.96 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    5.97 -apply (rule DPow_LsetI)
    5.98 -apply (rule bex_iff_sats conj_iff_sats)+
    5.99 -apply (rule_tac env = "[u,x,B,0,nat]" in mem_iff_sats)
   5.100 +         in gen_separation_multi [OF formula_replacement2_Reflects], 
   5.101 +       auto simp add: nonempty L_nat)
   5.102 +apply (rule_tac env="[B,0,nat]" in DPow_LsetI)
   5.103  apply (rule sep_rules formula_functor_iff_sats is_iterates_iff_sats | simp)+
   5.104  done
   5.105  
   5.106 @@ -368,13 +349,10 @@
   5.107     "L(w) ==> iterates_replacement(L, is_tl(L), w)"
   5.108  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
   5.109  apply (rule strong_replacementI)
   5.110 -apply (rule_tac u="{A,n,w,Memrel(succ(n))}" 
   5.111 -         in gen_separation [OF nth_replacement_Reflects], 
   5.112 -       simp add: nonempty)
   5.113 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   5.114 -apply (rule DPow_LsetI)
   5.115 -apply (rule bex_iff_sats conj_iff_sats)+
   5.116 -apply (rule_tac env = "[u,x,A,w,Memrel(succ(n))]" in mem_iff_sats)
   5.117 +apply (rule_tac u="{B,w,Memrel(succ(n))}" 
   5.118 +         in gen_separation_multi [OF nth_replacement_Reflects], 
   5.119 +       auto)
   5.120 +apply (rule_tac env="[B,w,Memrel(succ(n))]" in DPow_LsetI)
   5.121  apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats
   5.122              is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   5.123  done
   5.124 @@ -428,13 +406,9 @@
   5.125     "L(A) ==> iterates_replacement(L, big_union(L), A)"
   5.126  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
   5.127  apply (rule strong_replacementI)
   5.128 -apply (rename_tac B)
   5.129  apply (rule_tac u="{B,A,n,Memrel(succ(n))}" 
   5.130 -         in gen_separation [OF eclose_replacement1_Reflects], simp)
   5.131 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   5.132 -apply (rule DPow_LsetI)
   5.133 -apply (rule bex_iff_sats conj_iff_sats)+
   5.134 -apply (rule_tac env = "[u,x,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
   5.135 +         in gen_separation_multi [OF eclose_replacement1_Reflects], auto)
   5.136 +apply (rule_tac env="[B,A,n,Memrel(succ(n))]" in DPow_LsetI)
   5.137  apply (rule sep_rules iterates_MH_iff_sats is_nat_case_iff_sats
   5.138               is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
   5.139  done
   5.140 @@ -452,13 +426,10 @@
   5.141     "L(A) ==> strong_replacement(L,
   5.142           \<lambda>n y. n\<in>nat & is_iterates(L, big_union(L), A, n, y))"
   5.143  apply (rule strong_replacementI)
   5.144 -apply (rename_tac B)
   5.145  apply (rule_tac u="{A,B,nat}" 
   5.146 -         in gen_separation [OF eclose_replacement2_Reflects], simp add: L_nat)
   5.147 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   5.148 -apply (rule DPow_LsetI)
   5.149 -apply (rule bex_iff_sats conj_iff_sats)+
   5.150 -apply (rule_tac env = "[u,x,A,B,nat]" in mem_iff_sats)
   5.151 +         in gen_separation_multi [OF eclose_replacement2_Reflects],
   5.152 +       auto simp add: L_nat)
   5.153 +apply (rule_tac env="[A,B,nat]" in DPow_LsetI)
   5.154  apply (rule sep_rules is_iterates_iff_sats big_union_iff_sats | simp)+
   5.155  done
   5.156  
     6.1 --- a/src/ZF/Constructible/Relative.thy	Wed Oct 30 12:18:23 2002 +0100
     6.2 +++ b/src/ZF/Constructible/Relative.thy	Wed Oct 30 12:44:18 2002 +0100
     6.3 @@ -627,7 +627,7 @@
     6.4  
     6.5  text{*Probably the premise and conclusion are equivalent*}
     6.6  lemma (in M_trivial) strong_replacementI [rule_format]:
     6.7 -    "[| \<forall>A[M]. separation(M, %u. \<exists>x[M]. x\<in>A & P(x,u)) |]
     6.8 +    "[| \<forall>B[M]. separation(M, %u. \<exists>x[M]. x\<in>B & P(x,u)) |]
     6.9       ==> strong_replacement(M,P)"
    6.10  apply (simp add: strong_replacement_def, clarify)
    6.11  apply (frule replacementD [OF replacement], assumption, clarify)
     7.1 --- a/src/ZF/Constructible/Satisfies_absolute.thy	Wed Oct 30 12:18:23 2002 +0100
     7.2 +++ b/src/ZF/Constructible/Satisfies_absolute.thy	Wed Oct 30 12:44:18 2002 +0100
     7.3 @@ -8,6 +8,7 @@
     7.4  theory Satisfies_absolute = Datatype_absolute + Rec_Separation: 
     7.5  
     7.6  
     7.7 +subsection {*More Internalization*}
     7.8  
     7.9  subsubsection{*The Formula @{term is_depth}, Internalized*}
    7.10  
    7.11 @@ -823,14 +824,10 @@
    7.12                is_bool_of_o(L, nx \<in> ny, bo) &
    7.13                pair(L, env, bo, z))"
    7.14  apply (rule strong_replacementI)
    7.15 -apply (rename_tac B)
    7.16  apply (rule_tac u="{list(A),B,x,y}" 
    7.17 -         in gen_separation [OF Member_Reflects], 
    7.18 -       simp add: nat_into_M list_closed)
    7.19 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    7.20 -apply (rule DPow_LsetI)
    7.21 -apply (rule bex_iff_sats conj_iff_sats)+
    7.22 -apply (rule_tac env = "[v,u,list(A),B,x,y]" in mem_iff_sats) 
    7.23 +         in gen_separation_multi [OF Member_Reflects], 
    7.24 +       auto simp add: nat_into_M list_closed)
    7.25 +apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
    7.26  apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
    7.27  done
    7.28  
    7.29 @@ -857,14 +854,10 @@
    7.30                is_bool_of_o(L, nx = ny, bo) &
    7.31                pair(L, env, bo, z))"
    7.32  apply (rule strong_replacementI)
    7.33 -apply (rename_tac B)
    7.34  apply (rule_tac u="{list(A),B,x,y}" 
    7.35 -         in gen_separation [OF Equal_Reflects], 
    7.36 -       simp add: nat_into_M list_closed)
    7.37 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    7.38 -apply (rule DPow_LsetI)
    7.39 -apply (rule bex_iff_sats conj_iff_sats)+
    7.40 -apply (rule_tac env = "[v,u,list(A),B,x,y]" in mem_iff_sats) 
    7.41 +         in gen_separation_multi [OF Equal_Reflects], 
    7.42 +       auto simp add: nat_into_M list_closed)
    7.43 +apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
    7.44  apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
    7.45  done
    7.46  
    7.47 @@ -893,13 +886,10 @@
    7.48                 is_and(L,rpe,rqe,andpq) & is_not(L,andpq,notpq) & 
    7.49                 env \<in> list(A) & pair(L, env, notpq, z))"
    7.50  apply (rule strong_replacementI)
    7.51 -apply (rename_tac B)
    7.52 -apply (rule_tac u="{list(A),B,rp,rq}" in gen_separation [OF Nand_Reflects],
    7.53 -       simp add: list_closed)
    7.54 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    7.55 -apply (rule DPow_LsetI)
    7.56 -apply (rule bex_iff_sats conj_iff_sats)+
    7.57 -apply (rule_tac env = "[u,x,list(A),B,rp,rq]" in mem_iff_sats) 
    7.58 +apply (rule_tac u="{list(A),B,rp,rq}" 
    7.59 +         in gen_separation_multi [OF Nand_Reflects],
    7.60 +       auto simp add: list_closed)
    7.61 +apply (rule_tac env="[list(A),B,rp,rq]" in DPow_LsetI)
    7.62  apply (rule sep_rules is_and_iff_sats is_not_iff_sats | simp)+
    7.63  done
    7.64  
    7.65 @@ -935,13 +925,10 @@
    7.66                              bo) &
    7.67  	      pair(L,env,bo,z))"
    7.68  apply (rule strong_replacementI)
    7.69 -apply (rename_tac B)
    7.70 -apply (rule_tac u="{A,list(A),B,rp}" in gen_separation [OF Forall_Reflects],
    7.71 -       simp add: list_closed)
    7.72 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    7.73 -apply (rule DPow_LsetI)
    7.74 -apply (rule bex_iff_sats conj_iff_sats)+
    7.75 -apply (rule_tac env = "[u,x,A,list(A),B,rp]" in mem_iff_sats)
    7.76 +apply (rule_tac u="{A,list(A),B,rp}" 
    7.77 +         in gen_separation_multi [OF Forall_Reflects],
    7.78 +       auto simp add: list_closed)
    7.79 +apply (rule_tac env="[A,list(A),B,rp]" in DPow_LsetI)
    7.80  apply (rule sep_rules is_bool_of_o_iff_sats Cons_iff_sats | simp)+
    7.81  done
    7.82  
    7.83 @@ -960,14 +947,10 @@
    7.84     "[|n \<in> nat; L(A)|] ==> transrec_replacement(L, satisfies_MH(L,A), n)"
    7.85  apply (rule transrec_replacementI, simp add: nat_into_M) 
    7.86  apply (rule strong_replacementI)
    7.87 -apply (rename_tac B)
    7.88  apply (rule_tac u="{B,A,n,Memrel(eclose({n}))}"
    7.89 -         in gen_separation [OF formula_rec_replacement_Reflects],
    7.90 -       simp add: nat_into_M)
    7.91 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    7.92 -apply (rule DPow_LsetI)
    7.93 -apply (rule bex_iff_sats conj_iff_sats)+
    7.94 -apply (rule_tac env = "[u,x,A,n,B,Memrel(eclose({n}))]" in mem_iff_sats)
    7.95 +         in gen_separation_multi [OF formula_rec_replacement_Reflects],
    7.96 +       auto simp add: nat_into_M)
    7.97 +apply (rule_tac env="[B,A,n,Memrel(eclose({n}))]" in DPow_LsetI)
    7.98  apply (rule sep_rules satisfies_MH_iff_sats is_wfrec_iff_sats | simp)+
    7.99  done
   7.100  
   7.101 @@ -1006,13 +989,10 @@
   7.102                                    satisfies_is_d(L,A,g), x, c) &
   7.103               pair(L, x, c, y)))" 
   7.104  apply (rule strong_replacementI)
   7.105 -apply (rename_tac B)
   7.106  apply (rule_tac u="{B,A,g}"
   7.107 -         in gen_separation [OF formula_rec_lambda_replacement_Reflects], simp)
   7.108 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   7.109 -apply (rule DPow_LsetI)
   7.110 -apply (rule bex_iff_sats conj_iff_sats)+
   7.111 -apply (rule_tac env = "[u,x,A,g,B]" in mem_iff_sats)
   7.112 +         in gen_separation_multi [OF formula_rec_lambda_replacement_Reflects], 
   7.113 +       auto)
   7.114 +apply (rule_tac env="[A,g,B]" in DPow_LsetI)
   7.115  apply (rule sep_rules mem_formula_iff_sats
   7.116            formula_case_iff_sats satisfies_is_a_iff_sats
   7.117            satisfies_is_b_iff_sats satisfies_is_c_iff_sats
     8.1 --- a/src/ZF/Constructible/Separation.thy	Wed Oct 30 12:18:23 2002 +0100
     8.2 +++ b/src/ZF/Constructible/Separation.thy	Wed Oct 30 12:44:18 2002 +0100
     8.3 @@ -51,7 +51,7 @@
     8.4  done
     8.5  
     8.6  text{*Encapsulates the standard proof script for proving instances of 
     8.7 -Separation.  Typically @{term u} is a finite enumeration.*}
     8.8 +      Separation.*}
     8.9  lemma gen_separation:
    8.10   assumes reflection: "REFLECTS [P,Q]"
    8.11       and Lu:         "L(u)"
    8.12 @@ -65,7 +65,22 @@
    8.13  apply (erule reflection_imp_L_separation)
    8.14    apply (simp_all add: lt_Ord2, clarify)
    8.15  apply (rule collI)
    8.16 -apply assumption;  
    8.17 +apply assumption
    8.18 +done
    8.19 +
    8.20 +text{*As above, but typically @{term u} is a finite enumeration such as
    8.21 +  @{term "{a,b}"}; thus the new subgoal gets the assumption
    8.22 +  @{term "{a,b} \<subseteq> Lset(i)"}, which is logically equivalent to 
    8.23 +  @{term "a \<in> Lset(i)"} and @{term "b \<in> Lset(i)"}.*}
    8.24 +lemma gen_separation_multi:
    8.25 + assumes reflection: "REFLECTS [P,Q]"
    8.26 +     and Lu:         "L(u)"
    8.27 +     and collI: "!!j. u \<subseteq> Lset(j)
    8.28 +                \<Longrightarrow> Collect(Lset(j), Q(j)) \<in> DPow(Lset(j))"
    8.29 + shows "separation(L,P)"
    8.30 +apply (rule gen_separation [OF reflection Lu])
    8.31 +apply (drule mem_Lset_imp_subset_Lset)
    8.32 +apply (erule collI) 
    8.33  done
    8.34  
    8.35  
    8.36 @@ -80,6 +95,8 @@
    8.37       "L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A --> x\<in>y)"
    8.38  apply (rule gen_separation [OF Inter_Reflects], simp)
    8.39  apply (rule DPow_LsetI)
    8.40 + txt{*I leave this one example of a manual proof.  The tedium of manually
    8.41 +      instantiating @{term i}, @{term j} and @{term env} is obvious. *}
    8.42  apply (rule ball_iff_sats)
    8.43  apply (rule imp_iff_sats)
    8.44  apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats)
    8.45 @@ -96,9 +113,7 @@
    8.46  lemma Diff_separation:
    8.47       "L(B) ==> separation(L, \<lambda>x. x \<notin> B)"
    8.48  apply (rule gen_separation [OF Diff_Reflects], simp)
    8.49 -apply (rule DPow_LsetI)
    8.50 -apply (rule not_iff_sats) 
    8.51 -apply (rule_tac env="[x,B]" in mem_iff_sats)
    8.52 +apply (rule_tac env="[B]" in DPow_LsetI)
    8.53  apply (rule sep_rules | simp)+
    8.54  done
    8.55  
    8.56 @@ -113,12 +128,8 @@
    8.57  lemma cartprod_separation:
    8.58       "[| L(A); L(B) |]
    8.59        ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)))"
    8.60 -apply (rule gen_separation [OF cartprod_Reflects, of "{A,B}"], simp)
    8.61 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    8.62 -apply (rule DPow_LsetI)
    8.63 -apply (rule bex_iff_sats)
    8.64 -apply (rule conj_iff_sats)
    8.65 -apply (rule_tac i=0 and j=2 and env="[x,z,A,B]" in mem_iff_sats, simp_all)
    8.66 +apply (rule gen_separation_multi [OF cartprod_Reflects, of "{A,B}"], auto)
    8.67 +apply (rule_tac env="[A,B]" in DPow_LsetI)
    8.68  apply (rule sep_rules | simp)+
    8.69  done
    8.70  
    8.71 @@ -132,12 +143,8 @@
    8.72  lemma image_separation:
    8.73       "[| L(A); L(r) |]
    8.74        ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)))"
    8.75 -apply (rule gen_separation [OF image_Reflects, of "{A,r}"], simp)
    8.76 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
    8.77 -apply (rule DPow_LsetI)
    8.78 -apply (rule bex_iff_sats)
    8.79 -apply (rule conj_iff_sats)
    8.80 -apply (rule_tac env="[p,y,A,r]" in mem_iff_sats)
    8.81 +apply (rule gen_separation_multi [OF image_Reflects, of "{A,r}"], auto)
    8.82 +apply (rule_tac env="[A,r]" in DPow_LsetI)
    8.83  apply (rule sep_rules | simp)+
    8.84  done
    8.85  
    8.86 @@ -154,10 +161,7 @@
    8.87       "L(r) ==> separation(L,
    8.88           \<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)))"
    8.89  apply (rule gen_separation [OF converse_Reflects], simp)
    8.90 -apply (rule DPow_LsetI)
    8.91 -apply (rule bex_iff_sats)
    8.92 -apply (rule conj_iff_sats)
    8.93 -apply (rule_tac i=0 and j=2 and env="[p,z,r]" in mem_iff_sats, simp_all)
    8.94 +apply (rule_tac env="[r]" in DPow_LsetI)
    8.95  apply (rule sep_rules | simp)+
    8.96  done
    8.97  
    8.98 @@ -172,10 +176,7 @@
    8.99  lemma restrict_separation:
   8.100     "L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))"
   8.101  apply (rule gen_separation [OF restrict_Reflects], simp)
   8.102 -apply (rule DPow_LsetI)
   8.103 -apply (rule bex_iff_sats)
   8.104 -apply (rule conj_iff_sats)
   8.105 -apply (rule_tac i=0 and j=2 and env="[x,z,A]" in mem_iff_sats, simp_all)
   8.106 +apply (rule_tac env="[A]" in DPow_LsetI)
   8.107  apply (rule sep_rules | simp)+
   8.108  done
   8.109  
   8.110 @@ -196,15 +197,16 @@
   8.111        ==> separation(L, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
   8.112                    pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
   8.113                    xy\<in>s & yz\<in>r)"
   8.114 -apply (rule gen_separation [OF comp_Reflects, of "{r,s}"], simp)
   8.115 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   8.116 -apply (rule DPow_LsetI)
   8.117 -apply (rule bex_iff_sats)+
   8.118 -apply (rule conj_iff_sats)
   8.119 -apply (rule_tac env="[z,y,x,xz,r,s]" in pair_iff_sats)
   8.120 +apply (rule gen_separation_multi [OF comp_Reflects, of "{r,s}"], auto)
   8.121 +txt{*Subgoals after applying general ``separation'' rule:
   8.122 +     @{subgoals[display,indent=0,margin=65]}*}
   8.123 +apply (rule_tac env="[r,s]" in DPow_LsetI)
   8.124 +txt{*Subgoals ready for automatic synthesis of a formula:
   8.125 +     @{subgoals[display,indent=0,margin=65]}*}
   8.126  apply (rule sep_rules | simp)+
   8.127  done
   8.128  
   8.129 +
   8.130  subsection{*Separation for Predecessors in an Order*}
   8.131  
   8.132  lemma pred_Reflects:
   8.133 @@ -214,12 +216,8 @@
   8.134  
   8.135  lemma pred_separation:
   8.136       "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"
   8.137 -apply (rule gen_separation [OF pred_Reflects, of "{r,x}"], simp)
   8.138 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   8.139 -apply (rule DPow_LsetI)
   8.140 -apply (rule bex_iff_sats)
   8.141 -apply (rule conj_iff_sats)
   8.142 -apply (rule_tac env = "[p,y,r,x]" in mem_iff_sats)
   8.143 +apply (rule gen_separation_multi [OF pred_Reflects, of "{r,x}"], auto)
   8.144 +apply (rule_tac env="[r,x]" in DPow_LsetI)
   8.145  apply (rule sep_rules | simp)+
   8.146  done
   8.147  
   8.148 @@ -234,9 +232,7 @@
   8.149  lemma Memrel_separation:
   8.150       "separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
   8.151  apply (rule gen_separation [OF Memrel_Reflects nonempty])
   8.152 -apply (rule DPow_LsetI)
   8.153 -apply (rule bex_iff_sats conj_iff_sats)+
   8.154 -apply (rule_tac env = "[y,x,z]" in pair_iff_sats)
   8.155 +apply (rule_tac env="[]" in DPow_LsetI)
   8.156  apply (rule sep_rules | simp)+
   8.157  done
   8.158  
   8.159 @@ -259,12 +255,9 @@
   8.160                  pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) &
   8.161                  upair(L,cnbf,cnbf,z))"
   8.162  apply (rule strong_replacementI)
   8.163 -apply (rule_tac u="{n,A}" in gen_separation [OF funspace_succ_Reflects], simp)
   8.164 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   8.165 -apply (rule DPow_LsetI)
   8.166 -apply (rule bex_iff_sats)
   8.167 -apply (rule conj_iff_sats)
   8.168 -apply (rule_tac env = "[p,z,n,A]" in mem_iff_sats)
   8.169 +apply (rule_tac u="{n,B}" in gen_separation_multi [OF funspace_succ_Reflects], 
   8.170 +       auto)
   8.171 +apply (rule_tac env="[n,B]" in DPow_LsetI)
   8.172  apply (rule sep_rules | simp)+
   8.173  done
   8.174  
   8.175 @@ -290,11 +283,9 @@
   8.176                  pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r &
   8.177                  (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
   8.178                                     fx \<noteq> gx))"
   8.179 -apply (rule gen_separation [OF is_recfun_reflects, of "{r,f,g,a,b}"], simp)
   8.180 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   8.181 -apply (rule DPow_LsetI)
   8.182 -apply (rule bex_iff_sats conj_iff_sats)+
   8.183 -apply (rule_tac env = "[xa,x,r,f,g,a,b]" in pair_iff_sats)
   8.184 +apply (rule gen_separation_multi [OF is_recfun_reflects, of "{r,f,g,a,b}"], 
   8.185 +            auto)
   8.186 +apply (rule_tac env="[r,f,g,a,b]" in DPow_LsetI)
   8.187  apply (rule sep_rules | simp)+
   8.188  done
   8.189