more and simpler separation proofs
authorpaulson
Mon Jul 08 17:51:56 2002 +0200 (2002-07-08)
changeset 13316d16629fd0f95
parent 13315 685499c73215
child 13317 bb74918cc0dd
more and simpler separation proofs
src/ZF/Constructible/Formula.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/Separation.thy
     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.5  by (simp add: satisfies.simps)
     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.17  by (simp add: sats_Exists_iff) 
    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.168    apply (simp_all add: lt_Ord2)
   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