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