author paulson Mon Jul 08 17:51:56 2002 +0200 (2002-07-08) changeset 13316 d16629fd0f95 parent 13315 685499c73215 child 13317 bb74918cc0dd
more and simpler separation proofs
 src/ZF/Constructible/Formula.thy file | annotate | diff | revisions src/ZF/Constructible/L_axioms.thy file | annotate | diff | revisions src/ZF/Constructible/Relative.thy file | annotate | diff | revisions src/ZF/Constructible/Separation.thy file | annotate | diff | revisions
```     1.1 --- a/src/ZF/Constructible/Formula.thy	Mon Jul 08 17:24:07 2002 +0200
1.2 +++ b/src/ZF/Constructible/Formula.thy	Mon Jul 08 17:51:56 2002 +0200
1.3 @@ -130,6 +130,11 @@
1.4         ==> (x=y) <-> sats(A, Equal(i,j), env)"
1.6
1.7 +lemma not_iff_sats:
1.8 +      "[| P <-> sats(A,p,env); env \<in> list(A)|]
1.9 +       ==> (~P) <-> sats(A, Neg(p), env)"
1.10 +by simp
1.11 +
1.12  lemma conj_iff_sats:
1.13        "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
1.14         ==> (P & Q) <-> sats(A, And(p,q), env)"
1.15 @@ -165,6 +170,10 @@
1.16         ==> (\<exists>x\<in>A. P(x)) <-> sats(A, Exists(p), env)"
1.18
1.19 +lemmas FOL_iff_sats =
1.20 +        mem_iff_sats equal_iff_sats not_iff_sats conj_iff_sats
1.21 +        disj_iff_sats imp_iff_sats iff_iff_sats imp_iff_sats ball_iff_sats
1.22 +        bex_iff_sats
1.23
1.24  constdefs incr_var :: "[i,i]=>i"
1.25      "incr_var(x,lev) == if x<lev then x else succ(x)"
```
```     2.1 --- a/src/ZF/Constructible/L_axioms.thy	Mon Jul 08 17:24:07 2002 +0200
2.2 +++ b/src/ZF/Constructible/L_axioms.thy	Mon Jul 08 17:51:56 2002 +0200
2.3 @@ -309,8 +309,7 @@
2.4       "[| REFLECTS[P,Q]; Ord(i);
2.5           !!j. [|i<j;  \<forall>x \<in> Lset(j). P(x) <-> Q(j,x)|] ==> R |]
2.6        ==> R"
2.7 -apply (drule ReflectsD, assumption)
2.8 -apply blast
2.9 +apply (drule ReflectsD, assumption, blast)
2.10  done
2.11
2.12  lemma Collect_mem_eq: "{x\<in>A. x\<in>B} = A \<inter> B";
2.13 @@ -1084,4 +1083,15 @@
2.14  apply (intro FOL_reflection function_reflection bijection_reflection)
2.15  done
2.16
2.17 +lemmas fun_plus_reflection =
2.18 +        typed_function_reflection injection_reflection surjection_reflection
2.19 +        bijection_reflection order_isomorphism_reflection
2.20 +
2.21 +lemmas fun_plus_iff_sats = upair_iff_sats pair_iff_sats union_iff_sats
2.22 +	cons_iff_sats fun_apply_iff_sats ordinal_iff_sats Memrel_iff_sats
2.23 +	pred_set_iff_sats domain_iff_sats range_iff_sats image_iff_sats
2.24 +	relation_iff_sats function_iff_sats typed_function_iff_sats
2.25 +        injection_iff_sats surjection_iff_sats bijection_iff_sats
2.26 +        order_isomorphism_iff_sats
2.27 +
2.28  end
```
```     3.1 --- a/src/ZF/Constructible/Relative.thy	Mon Jul 08 17:24:07 2002 +0200
3.2 +++ b/src/ZF/Constructible/Relative.thy	Mon Jul 08 17:51:56 2002 +0200
3.3 @@ -753,11 +753,10 @@
3.4  	     order_isomorphism(M,par,r,x,mx,g))"
3.5    and obase_equals_separation:
3.6       "[| M(A); M(r) |]
3.7 -      ==> separation
3.8 -      (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M].
3.9 -	      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M].
3.10 -	      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
3.11 -	      order_isomorphism(M,pxr,r,y,my,g))))"
3.12 +      ==> separation (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M].
3.13 +			      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M].
3.14 +			      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
3.15 +			      order_isomorphism(M,pxr,r,y,my,g))))"
3.16    and omap_replacement:
3.17       "[| M(A); M(r) |]
3.18        ==> strong_replacement(M,
```
```     4.1 --- a/src/ZF/Constructible/Separation.thy	Mon Jul 08 17:24:07 2002 +0200
4.2 +++ b/src/ZF/Constructible/Separation.thy	Mon Jul 08 17:51:56 2002 +0200
4.3 @@ -6,6 +6,8 @@
4.4  lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x"
4.5  by simp
4.6
4.7 +lemmas nth_rules = nth_0 nth_ConsI nat_0I nat_succI
4.8 +lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats fun_plus_iff_sats
4.9
4.10  lemma Collect_conj_in_DPow:
4.11       "[| {x\<in>A. P(x)} \<in> DPow(A);  {x\<in>A. Q(x)} \<in> DPow(A) |]
4.12 @@ -41,7 +43,7 @@
4.13  done
4.14
4.15
4.16 -subsubsection{*Separation for Intersection*}
4.17 +subsection{*Separation for Intersection*}
4.18
4.19  lemma Inter_Reflects:
4.20       "REFLECTS[\<lambda>x. \<forall>y[L]. y\<in>A --> x \<in> y,
4.21 @@ -64,7 +66,7 @@
4.22  apply (simp_all add: succ_Un_distrib [symmetric])
4.23  done
4.24
4.25 -subsubsection{*Separation for Cartesian Product*}
4.26 +subsection{*Separation for Cartesian Product*}
4.27
4.28  lemma cartprod_Reflects [simplified]:
4.29       "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)),
4.30 @@ -86,16 +88,11 @@
4.31  apply (rule bex_iff_sats)
4.32  apply (rule conj_iff_sats)
4.33  apply (rule_tac i=0 and j=2 and env="[x,u,A,B]" in mem_iff_sats, simp_all)
4.34 -apply (rule bex_iff_sats)
4.35 -apply (rule conj_iff_sats)
4.36 -apply (rule mem_iff_sats)
4.37 -apply (blast intro: nth_0 nth_ConsI)
4.38 -apply (blast intro: nth_0 nth_ConsI, simp_all)
4.39 -apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats)
4.40 +apply (rule sep_rules | simp)+
4.41  apply (simp_all add: succ_Un_distrib [symmetric])
4.42  done
4.43
4.44 -subsubsection{*Separation for Image*}
4.45 +subsection{*Separation for Image*}
4.46
4.47  text{*No @{text simplified} here: it simplifies the occurrence of
4.48        the predicate @{term pair}!*}
4.49 @@ -118,22 +115,12 @@
4.50  apply (rule bex_iff_sats)
4.51  apply (rule conj_iff_sats)
4.52  apply (rule_tac env="[p,y,A,r]" in mem_iff_sats)
4.53 -apply (blast intro: nth_0 nth_ConsI)
4.54 -apply (blast intro: nth_0 nth_ConsI, simp_all)
4.55 -apply (rule bex_iff_sats)
4.56 -apply (rule conj_iff_sats)
4.57 -apply (rule mem_iff_sats)
4.58 -apply (blast intro: nth_0 nth_ConsI)
4.59 -apply (blast intro: nth_0 nth_ConsI, simp_all)
4.60 -apply (rule pair_iff_sats)
4.61 -apply (blast intro: nth_0 nth_ConsI)
4.62 -apply (blast intro: nth_0 nth_ConsI)
4.63 -apply (blast intro: nth_0 nth_ConsI)
4.64 +apply (rule sep_rules | simp)+
4.65  apply (simp_all add: succ_Un_distrib [symmetric])
4.66  done
4.67
4.68
4.69 -subsubsection{*Separation for Converse*}
4.70 +subsection{*Separation for Converse*}
4.71
4.72  lemma converse_Reflects:
4.73    "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)),
4.74 @@ -155,19 +142,12 @@
4.75  apply (rule bex_iff_sats)
4.76  apply (rule conj_iff_sats)
4.77  apply (rule_tac i=0 and j="2" and env="[p,u,r]" in mem_iff_sats, simp_all)
4.78 -apply (rule bex_iff_sats)
4.79 -apply (rule bex_iff_sats)
4.80 -apply (rule conj_iff_sats)
4.81 -apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats, simp_all)
4.82 -apply (rule pair_iff_sats)
4.83 -apply (blast intro: nth_0 nth_ConsI)
4.84 -apply (blast intro: nth_0 nth_ConsI)
4.85 -apply (blast intro: nth_0 nth_ConsI)
4.86 +apply (rule sep_rules | simp)+
4.87  apply (simp_all add: succ_Un_distrib [symmetric])
4.88  done
4.89
4.90
4.91 -subsubsection{*Separation for Restriction*}
4.92 +subsection{*Separation for Restriction*}
4.93
4.94  lemma restrict_Reflects:
4.95       "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)),
4.96 @@ -187,13 +167,12 @@
4.97  apply (rule bex_iff_sats)
4.98  apply (rule conj_iff_sats)
4.99  apply (rule_tac i=0 and j="2" and env="[x,u,A]" in mem_iff_sats, simp_all)
4.100 -apply (rule bex_iff_sats)
4.101 -apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats)
4.102 +apply (rule sep_rules | simp)+
4.103  apply (simp_all add: succ_Un_distrib [symmetric])
4.104  done
4.105
4.106
4.107 -subsubsection{*Separation for Composition*}
4.108 +subsection{*Separation for Composition*}
4.109
4.110  lemma comp_Reflects:
4.111       "REFLECTS[\<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
4.112 @@ -221,32 +200,11 @@
4.113  apply (rename_tac x y z)
4.114  apply (rule conj_iff_sats)
4.115  apply (rule_tac env="[z,y,x,u,r,s]" in pair_iff_sats)
4.116 -apply (blast intro: nth_0 nth_ConsI)
4.117 -apply (blast intro: nth_0 nth_ConsI)
4.118 -apply (blast intro: nth_0 nth_ConsI, simp_all)
4.119 -apply (rule bex_iff_sats)
4.120 -apply (rule conj_iff_sats)
4.121 -apply (rule pair_iff_sats)
4.122 -apply (blast intro: nth_0 nth_ConsI)
4.123 -apply (blast intro: nth_0 nth_ConsI)
4.124 -apply (blast intro: nth_0 nth_ConsI, simp_all)
4.125 -apply (rule bex_iff_sats)
4.126 -apply (rule conj_iff_sats)
4.127 -apply (rule pair_iff_sats)
4.128 -apply (blast intro: nth_0 nth_ConsI)
4.129 -apply (blast intro: nth_0 nth_ConsI)
4.130 -apply (blast intro: nth_0 nth_ConsI, simp_all)
4.131 -apply (rule conj_iff_sats)
4.132 -apply (rule mem_iff_sats)
4.133 -apply (blast intro: nth_0 nth_ConsI)
4.134 -apply (blast intro: nth_0 nth_ConsI, simp)
4.135 -apply (rule mem_iff_sats)
4.136 -apply (blast intro: nth_0 nth_ConsI)
4.137 -apply (blast intro: nth_0 nth_ConsI)
4.138 +apply (rule sep_rules | simp)+
4.139  apply (simp_all add: succ_Un_distrib [symmetric])
4.140  done
4.141
4.142 -subsubsection{*Separation for Predecessors in an Order*}
4.143 +subsection{*Separation for Predecessors in an Order*}
4.144
4.145  lemma pred_Reflects:
4.146       "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p),
4.147 @@ -266,17 +224,12 @@
4.148  apply (rule bex_iff_sats)
4.149  apply (rule conj_iff_sats)
4.150  apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats)
4.151 -apply (blast intro: nth_0 nth_ConsI)
4.152 -apply (blast intro: nth_0 nth_ConsI, simp)
4.153 -apply (rule pair_iff_sats)
4.154 -apply (blast intro: nth_0 nth_ConsI)
4.155 -apply (blast intro: nth_0 nth_ConsI)
4.156 -apply (blast intro: nth_0 nth_ConsI, simp_all)
4.157 +apply (rule sep_rules | simp)+
4.158  apply (simp_all add: succ_Un_distrib [symmetric])
4.159  done
4.160
4.161
4.162 -subsubsection{*Separation for the Membership Relation*}
4.163 +subsection{*Separation for the Membership Relation*}
4.164
4.165  lemma Memrel_Reflects:
4.166       "REFLECTS[\<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y,
4.167 @@ -293,20 +246,14 @@
4.169  apply (rule DPowI2)
4.170  apply (rename_tac u)
4.171 -apply (rule bex_iff_sats)+
4.172 -apply (rule conj_iff_sats)
4.173 +apply (rule bex_iff_sats conj_iff_sats)+
4.174  apply (rule_tac env = "[y,x,u]" in pair_iff_sats)
4.175 -apply (blast intro: nth_0 nth_ConsI)
4.176 -apply (blast intro: nth_0 nth_ConsI)
4.177 -apply (blast intro: nth_0 nth_ConsI, simp_all)
4.178 -apply (rule mem_iff_sats)
4.179 -apply (blast intro: nth_0 nth_ConsI)
4.180 -apply (blast intro: nth_0 nth_ConsI)
4.181 +apply (rule sep_rules | simp)+
4.182  apply (simp_all add: succ_Un_distrib [symmetric])
4.183  done
4.184
4.185
4.186 -subsubsection{*Replacement for FunSpace*}
4.187 +subsection{*Replacement for FunSpace*}
4.188
4.189  lemma funspace_succ_Reflects:
4.190   "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>A & (\<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L].
4.191 @@ -336,34 +283,12 @@
4.192  apply (rule bex_iff_sats)
4.193  apply (rule conj_iff_sats)
4.194  apply (rule_tac env = "[x,u,n,A]" in mem_iff_sats)
4.195 -apply (blast intro: nth_0 nth_ConsI)
4.196 -apply (blast intro: nth_0 nth_ConsI, simp_all)
4.197 -apply (rule conj_iff_sats bex_iff_sats)+
4.198 -apply (rule pair_iff_sats)
4.199 -apply (blast intro: nth_0 nth_ConsI)
4.200 -apply (blast intro: nth_0 nth_ConsI)
4.201 -apply (blast intro: nth_0 nth_ConsI, simp_all)
4.202 -apply (rule bex_iff_sats)
4.203 -apply (rule conj_iff_sats)
4.204 -apply (rule pair_iff_sats)
4.205 -apply (blast intro: nth_0 nth_ConsI)
4.206 -apply (blast intro: nth_0 nth_ConsI)
4.207 -apply (blast intro: nth_0 nth_ConsI, simp_all)
4.208 -apply (rule bex_iff_sats)
4.209 -apply (rule conj_iff_sats)
4.210 -apply (rule cons_iff_sats)
4.211 -apply (blast intro!: nth_0 nth_ConsI)
4.212 -apply (blast intro!: nth_0 nth_ConsI)
4.213 -apply (blast intro!: nth_0 nth_ConsI, simp_all)
4.214 -apply (rule upair_iff_sats)
4.215 -apply (blast intro: nth_0 nth_ConsI)
4.216 -apply (blast intro: nth_0 nth_ConsI)
4.217 -apply (blast intro: nth_0 nth_ConsI)
4.218 +apply (rule sep_rules | simp)+
4.219  apply (simp_all add: succ_Un_distrib [symmetric])
4.220  done
4.221
4.222
4.223 -subsubsection{*Separation for Order-Isomorphisms*}
4.224 +subsection{*Separation for Order-Isomorphisms*}
4.225
4.226  lemma well_ord_iso_Reflects:
4.227    "REFLECTS[\<lambda>x. x\<in>A -->
4.228 @@ -386,23 +311,112 @@
4.229  apply (rename_tac u)
4.230  apply (rule imp_iff_sats)
4.231  apply (rule_tac env = "[u,A,f,r]" in mem_iff_sats)
4.232 -apply (blast intro: nth_0 nth_ConsI)
4.233 -apply (blast intro: nth_0 nth_ConsI, simp_all)
4.234 +apply (rule sep_rules | simp)+
4.235 +apply (simp_all add: succ_Un_distrib [symmetric])
4.236 +done
4.237 +
4.238 +
4.239 +subsection{*Separation for @{term "obase"}*}
4.240 +
4.241 +lemma obase_reflects:
4.242 +  "REFLECTS[\<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
4.243 +	     ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
4.244 +	     order_isomorphism(L,par,r,x,mx,g),
4.245 +        \<lambda>i a. \<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). \<exists>par \<in> Lset(i).
4.246 +	     ordinal(**Lset(i),x) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
4.247 +	     order_isomorphism(**Lset(i),par,r,x,mx,g)]"
4.248 +by (intro FOL_reflection function_reflection fun_plus_reflection)
4.249 +
4.250 +lemma obase_separation:
4.251 +     --{*part of the order type formalization*}
4.252 +     "[| L(A); L(r) |]
4.253 +      ==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
4.254 +	     ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
4.255 +	     order_isomorphism(L,par,r,x,mx,g))"
4.256 +apply (rule separation_CollectI)
4.257 +apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
4.258 +apply (rule ReflectsE [OF obase_reflects], assumption)
4.259 +apply (drule subset_Lset_ltD, assumption)
4.260 +apply (erule reflection_imp_L_separation)
4.261 +  apply (simp_all add: lt_Ord2)
4.262 +apply (rule DPowI2)
4.263 +apply (rename_tac u)
4.264  apply (rule bex_iff_sats)
4.265  apply (rule conj_iff_sats)
4.266 -apply (rule fun_apply_iff_sats)
4.267 -apply (blast intro: nth_0 nth_ConsI)
4.268 -apply (blast intro: nth_0 nth_ConsI)
4.269 -apply (blast intro: nth_0 nth_ConsI, simp_all)
4.270 -apply (rule bex_iff_sats)
4.271 -apply (rule conj_iff_sats)
4.272 -apply (rule pair_iff_sats)
4.273 -apply (blast intro: nth_0 nth_ConsI)
4.274 -apply (blast intro: nth_0 nth_ConsI)
4.275 -apply (blast intro: nth_0 nth_ConsI, simp_all)
4.276 -apply (rule mem_iff_sats)
4.277 -apply (blast intro: nth_0 nth_ConsI)
4.278 -apply (blast intro: nth_0 nth_ConsI)
4.279 +apply (rule_tac env = "[x,u,A,r]" in ordinal_iff_sats)
4.280 +apply (rule sep_rules | simp)+
4.281 +apply (simp_all add: succ_Un_distrib [symmetric])
4.282 +done
4.283 +
4.284 +
4.285 +subsection{*Separation for @{term "well_ord_iso"}*}
4.286 +
4.287 +lemma obase_equals_reflects:
4.288 +  "REFLECTS[\<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L].
4.289 +		ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
4.290 +		membership(L,y,my) & pred_set(L,A,x,r,pxr) &
4.291 +		order_isomorphism(L,pxr,r,y,my,g))),
4.292 +	\<lambda>i x. x\<in>A --> ~(\<exists>y \<in> Lset(i). \<exists>g \<in> Lset(i).
4.293 +		ordinal(**Lset(i),y) & (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i).
4.294 +		membership(**Lset(i),y,my) & pred_set(**Lset(i),A,x,r,pxr) &
4.295 +		order_isomorphism(**Lset(i),pxr,r,y,my,g)))]"
4.296 +by (intro FOL_reflection function_reflection fun_plus_reflection)
4.297 +
4.298 +
4.299 +lemma obase_equals_separation:
4.300 +     "[| L(A); L(r) |]
4.301 +      ==> separation (L, \<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L].
4.302 +			      ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
4.303 +			      membership(L,y,my) & pred_set(L,A,x,r,pxr) &
4.304 +			      order_isomorphism(L,pxr,r,y,my,g))))"
4.305 +apply (rule separation_CollectI)
4.306 +apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
4.307 +apply (rule ReflectsE [OF obase_equals_reflects], assumption)
4.308 +apply (drule subset_Lset_ltD, assumption)
4.309 +apply (erule reflection_imp_L_separation)
4.310 +  apply (simp_all add: lt_Ord2)
4.311 +apply (rule DPowI2)
4.312 +apply (rename_tac u)
4.313 +apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+
4.314 +apply (rule_tac env = "[u,A,r]" in mem_iff_sats)
4.315 +apply (rule sep_rules | simp)+
4.316 +apply (simp_all add: succ_Un_distrib [symmetric])
4.317 +done
4.318 +
4.319 +
4.320 +subsection{*Replacement for @{term "omap"}*}
4.321 +
4.322 +lemma omap_reflects:
4.323 + "REFLECTS[\<lambda>z. \<exists>a[L]. a\<in>B & (\<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
4.324 +     ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
4.325 +     pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g)),
4.326 + \<lambda>i z. \<exists>a \<in> Lset(i). a\<in>B & (\<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i).
4.327 +        \<exists>par \<in> Lset(i).
4.328 +	 ordinal(**Lset(i),x) & pair(**Lset(i),a,x,z) &
4.329 +         membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
4.330 +         order_isomorphism(**Lset(i),par,r,x,mx,g))]"
4.331 +by (intro FOL_reflection function_reflection fun_plus_reflection)
4.332 +
4.333 +lemma omap_replacement:
4.334 +     "[| L(A); L(r) |]
4.335 +      ==> strong_replacement(L,
4.336 +             \<lambda>a z. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
4.337 +	     ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
4.338 +	     pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
4.339 +apply (rule strong_replacementI)
4.340 +apply (rule rallI)
4.341 +apply (rename_tac B)
4.342 +apply (rule separation_CollectI)
4.343 +apply (rule_tac A="{A,B,r,z}" in subset_LsetE, blast )
4.344 +apply (rule ReflectsE [OF omap_reflects], assumption)
4.345 +apply (drule subset_Lset_ltD, assumption)
4.346 +apply (erule reflection_imp_L_separation)
4.347 +  apply (simp_all add: lt_Ord2)
4.348 +apply (rule DPowI2)
4.349 +apply (rename_tac u)
4.350 +apply (rule bex_iff_sats conj_iff_sats)+
4.351 +apply (rule_tac env = "[x,u,A,B,r]" in mem_iff_sats)
4.352 +apply (rule sep_rules | simp)+
4.353  apply (simp_all add: succ_Un_distrib [symmetric])
4.354  done
4.355
```