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