src/ZF/Constructible/Separation.thy
changeset 13316 d16629fd0f95
parent 13314 84b9de3cbc91
child 13319 23de7b3af453
     1.1 --- a/src/ZF/Constructible/Separation.thy	Mon Jul 08 17:24:07 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Separation.thy	Mon Jul 08 17:51:56 2002 +0200
     1.3 @@ -6,6 +6,8 @@
     1.4  lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x"
     1.5  by simp
     1.6  
     1.7 +lemmas nth_rules = nth_0 nth_ConsI nat_0I nat_succI
     1.8 +lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats fun_plus_iff_sats
     1.9  
    1.10  lemma Collect_conj_in_DPow:
    1.11       "[| {x\<in>A. P(x)} \<in> DPow(A);  {x\<in>A. Q(x)} \<in> DPow(A) |] 
    1.12 @@ -41,7 +43,7 @@
    1.13  done
    1.14  
    1.15  
    1.16 -subsubsection{*Separation for Intersection*}
    1.17 +subsection{*Separation for Intersection*}
    1.18  
    1.19  lemma Inter_Reflects:
    1.20       "REFLECTS[\<lambda>x. \<forall>y[L]. y\<in>A --> x \<in> y, 
    1.21 @@ -64,7 +66,7 @@
    1.22  apply (simp_all add: succ_Un_distrib [symmetric])
    1.23  done
    1.24  
    1.25 -subsubsection{*Separation for Cartesian Product*}
    1.26 +subsection{*Separation for Cartesian Product*}
    1.27  
    1.28  lemma cartprod_Reflects [simplified]:
    1.29       "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)),
    1.30 @@ -86,16 +88,11 @@
    1.31  apply (rule bex_iff_sats) 
    1.32  apply (rule conj_iff_sats)
    1.33  apply (rule_tac i=0 and j=2 and env="[x,u,A,B]" in mem_iff_sats, simp_all)
    1.34 -apply (rule bex_iff_sats) 
    1.35 -apply (rule conj_iff_sats)
    1.36 -apply (rule mem_iff_sats)
    1.37 -apply (blast intro: nth_0 nth_ConsI) 
    1.38 -apply (blast intro: nth_0 nth_ConsI, simp_all)
    1.39 -apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats)
    1.40 +apply (rule sep_rules | simp)+
    1.41  apply (simp_all add: succ_Un_distrib [symmetric])
    1.42  done
    1.43  
    1.44 -subsubsection{*Separation for Image*}
    1.45 +subsection{*Separation for Image*}
    1.46  
    1.47  text{*No @{text simplified} here: it simplifies the occurrence of 
    1.48        the predicate @{term pair}!*}
    1.49 @@ -118,22 +115,12 @@
    1.50  apply (rule bex_iff_sats) 
    1.51  apply (rule conj_iff_sats)
    1.52  apply (rule_tac env="[p,y,A,r]" in mem_iff_sats)
    1.53 -apply (blast intro: nth_0 nth_ConsI) 
    1.54 -apply (blast intro: nth_0 nth_ConsI, simp_all)
    1.55 -apply (rule bex_iff_sats) 
    1.56 -apply (rule conj_iff_sats)
    1.57 -apply (rule mem_iff_sats)
    1.58 -apply (blast intro: nth_0 nth_ConsI) 
    1.59 -apply (blast intro: nth_0 nth_ConsI, simp_all)
    1.60 -apply (rule pair_iff_sats)
    1.61 -apply (blast intro: nth_0 nth_ConsI) 
    1.62 -apply (blast intro: nth_0 nth_ConsI) 
    1.63 -apply (blast intro: nth_0 nth_ConsI)
    1.64 +apply (rule sep_rules | simp)+
    1.65  apply (simp_all add: succ_Un_distrib [symmetric])
    1.66  done
    1.67  
    1.68  
    1.69 -subsubsection{*Separation for Converse*}
    1.70 +subsection{*Separation for Converse*}
    1.71  
    1.72  lemma converse_Reflects:
    1.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)),
    1.74 @@ -155,19 +142,12 @@
    1.75  apply (rule bex_iff_sats) 
    1.76  apply (rule conj_iff_sats)
    1.77  apply (rule_tac i=0 and j="2" and env="[p,u,r]" in mem_iff_sats, simp_all)
    1.78 -apply (rule bex_iff_sats) 
    1.79 -apply (rule bex_iff_sats) 
    1.80 -apply (rule conj_iff_sats)
    1.81 -apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats, simp_all)
    1.82 -apply (rule pair_iff_sats)
    1.83 -apply (blast intro: nth_0 nth_ConsI) 
    1.84 -apply (blast intro: nth_0 nth_ConsI) 
    1.85 -apply (blast intro: nth_0 nth_ConsI)
    1.86 +apply (rule sep_rules | simp)+
    1.87  apply (simp_all add: succ_Un_distrib [symmetric])
    1.88  done
    1.89  
    1.90  
    1.91 -subsubsection{*Separation for Restriction*}
    1.92 +subsection{*Separation for Restriction*}
    1.93  
    1.94  lemma restrict_Reflects:
    1.95       "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)),
    1.96 @@ -187,13 +167,12 @@
    1.97  apply (rule bex_iff_sats) 
    1.98  apply (rule conj_iff_sats)
    1.99  apply (rule_tac i=0 and j="2" and env="[x,u,A]" in mem_iff_sats, simp_all)
   1.100 -apply (rule bex_iff_sats) 
   1.101 -apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats)
   1.102 +apply (rule sep_rules | simp)+
   1.103  apply (simp_all add: succ_Un_distrib [symmetric])
   1.104  done
   1.105  
   1.106  
   1.107 -subsubsection{*Separation for Composition*}
   1.108 +subsection{*Separation for Composition*}
   1.109  
   1.110  lemma comp_Reflects:
   1.111       "REFLECTS[\<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L]. 
   1.112 @@ -221,32 +200,11 @@
   1.113  apply (rename_tac x y z)  
   1.114  apply (rule conj_iff_sats)
   1.115  apply (rule_tac env="[z,y,x,u,r,s]" in pair_iff_sats)
   1.116 -apply (blast intro: nth_0 nth_ConsI) 
   1.117 -apply (blast intro: nth_0 nth_ConsI) 
   1.118 -apply (blast intro: nth_0 nth_ConsI, simp_all)
   1.119 -apply (rule bex_iff_sats) 
   1.120 -apply (rule conj_iff_sats)
   1.121 -apply (rule pair_iff_sats)
   1.122 -apply (blast intro: nth_0 nth_ConsI) 
   1.123 -apply (blast intro: nth_0 nth_ConsI) 
   1.124 -apply (blast intro: nth_0 nth_ConsI, simp_all)
   1.125 -apply (rule bex_iff_sats) 
   1.126 -apply (rule conj_iff_sats)
   1.127 -apply (rule pair_iff_sats)
   1.128 -apply (blast intro: nth_0 nth_ConsI) 
   1.129 -apply (blast intro: nth_0 nth_ConsI) 
   1.130 -apply (blast intro: nth_0 nth_ConsI, simp_all) 
   1.131 -apply (rule conj_iff_sats)
   1.132 -apply (rule mem_iff_sats) 
   1.133 -apply (blast intro: nth_0 nth_ConsI) 
   1.134 -apply (blast intro: nth_0 nth_ConsI, simp) 
   1.135 -apply (rule mem_iff_sats) 
   1.136 -apply (blast intro: nth_0 nth_ConsI) 
   1.137 -apply (blast intro: nth_0 nth_ConsI)
   1.138 +apply (rule sep_rules | simp)+
   1.139  apply (simp_all add: succ_Un_distrib [symmetric])
   1.140  done
   1.141  
   1.142 -subsubsection{*Separation for Predecessors in an Order*}
   1.143 +subsection{*Separation for Predecessors in an Order*}
   1.144  
   1.145  lemma pred_Reflects:
   1.146       "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p),
   1.147 @@ -266,17 +224,12 @@
   1.148  apply (rule bex_iff_sats)
   1.149  apply (rule conj_iff_sats)
   1.150  apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats) 
   1.151 -apply (blast intro: nth_0 nth_ConsI) 
   1.152 -apply (blast intro: nth_0 nth_ConsI, simp) 
   1.153 -apply (rule pair_iff_sats)
   1.154 -apply (blast intro: nth_0 nth_ConsI) 
   1.155 -apply (blast intro: nth_0 nth_ConsI) 
   1.156 -apply (blast intro: nth_0 nth_ConsI, simp_all)
   1.157 +apply (rule sep_rules | simp)+
   1.158  apply (simp_all add: succ_Un_distrib [symmetric])
   1.159  done
   1.160  
   1.161  
   1.162 -subsubsection{*Separation for the Membership Relation*}
   1.163 +subsection{*Separation for the Membership Relation*}
   1.164  
   1.165  lemma Memrel_Reflects:
   1.166       "REFLECTS[\<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y,
   1.167 @@ -293,20 +246,14 @@
   1.168    apply (simp_all add: lt_Ord2)
   1.169  apply (rule DPowI2)
   1.170  apply (rename_tac u) 
   1.171 -apply (rule bex_iff_sats)+
   1.172 -apply (rule conj_iff_sats)
   1.173 +apply (rule bex_iff_sats conj_iff_sats)+
   1.174  apply (rule_tac env = "[y,x,u]" in pair_iff_sats) 
   1.175 -apply (blast intro: nth_0 nth_ConsI) 
   1.176 -apply (blast intro: nth_0 nth_ConsI) 
   1.177 -apply (blast intro: nth_0 nth_ConsI, simp_all) 
   1.178 -apply (rule mem_iff_sats)
   1.179 -apply (blast intro: nth_0 nth_ConsI) 
   1.180 -apply (blast intro: nth_0 nth_ConsI)
   1.181 +apply (rule sep_rules | simp)+
   1.182  apply (simp_all add: succ_Un_distrib [symmetric])
   1.183  done
   1.184  
   1.185  
   1.186 -subsubsection{*Replacement for FunSpace*}
   1.187 +subsection{*Replacement for FunSpace*}
   1.188  		
   1.189  lemma funspace_succ_Reflects:
   1.190   "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>A & (\<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L]. 
   1.191 @@ -336,34 +283,12 @@
   1.192  apply (rule bex_iff_sats)
   1.193  apply (rule conj_iff_sats)
   1.194  apply (rule_tac env = "[x,u,n,A]" in mem_iff_sats) 
   1.195 -apply (blast intro: nth_0 nth_ConsI) 
   1.196 -apply (blast intro: nth_0 nth_ConsI, simp_all) 
   1.197 -apply (rule conj_iff_sats bex_iff_sats)+
   1.198 -apply (rule pair_iff_sats) 
   1.199 -apply (blast intro: nth_0 nth_ConsI) 
   1.200 -apply (blast intro: nth_0 nth_ConsI) 
   1.201 -apply (blast intro: nth_0 nth_ConsI, simp_all) 
   1.202 -apply (rule bex_iff_sats)
   1.203 -apply (rule conj_iff_sats)
   1.204 -apply (rule pair_iff_sats) 
   1.205 -apply (blast intro: nth_0 nth_ConsI) 
   1.206 -apply (blast intro: nth_0 nth_ConsI) 
   1.207 -apply (blast intro: nth_0 nth_ConsI, simp_all) 
   1.208 -apply (rule bex_iff_sats)
   1.209 -apply (rule conj_iff_sats)
   1.210 -apply (rule cons_iff_sats) 
   1.211 -apply (blast intro!: nth_0 nth_ConsI) 
   1.212 -apply (blast intro!: nth_0 nth_ConsI) 
   1.213 -apply (blast intro!: nth_0 nth_ConsI, simp_all)
   1.214 -apply (rule upair_iff_sats) 
   1.215 -apply (blast intro: nth_0 nth_ConsI) 
   1.216 -apply (blast intro: nth_0 nth_ConsI) 
   1.217 -apply (blast intro: nth_0 nth_ConsI) 
   1.218 +apply (rule sep_rules | simp)+
   1.219  apply (simp_all add: succ_Un_distrib [symmetric])
   1.220  done
   1.221  
   1.222  
   1.223 -subsubsection{*Separation for Order-Isomorphisms*}
   1.224 +subsection{*Separation for Order-Isomorphisms*}
   1.225  
   1.226  lemma well_ord_iso_Reflects:
   1.227    "REFLECTS[\<lambda>x. x\<in>A --> 
   1.228 @@ -386,23 +311,112 @@
   1.229  apply (rename_tac u) 
   1.230  apply (rule imp_iff_sats)
   1.231  apply (rule_tac env = "[u,A,f,r]" in mem_iff_sats) 
   1.232 -apply (blast intro: nth_0 nth_ConsI) 
   1.233 -apply (blast intro: nth_0 nth_ConsI, simp_all) 
   1.234 +apply (rule sep_rules | simp)+
   1.235 +apply (simp_all add: succ_Un_distrib [symmetric])
   1.236 +done
   1.237 +
   1.238 +
   1.239 +subsection{*Separation for @{term "obase"}*}
   1.240 +
   1.241 +lemma obase_reflects:
   1.242 +  "REFLECTS[\<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. 
   1.243 +	     ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
   1.244 +	     order_isomorphism(L,par,r,x,mx,g),
   1.245 +        \<lambda>i a. \<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). \<exists>par \<in> Lset(i). 
   1.246 +	     ordinal(**Lset(i),x) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
   1.247 +	     order_isomorphism(**Lset(i),par,r,x,mx,g)]"
   1.248 +by (intro FOL_reflection function_reflection fun_plus_reflection)
   1.249 +
   1.250 +lemma obase_separation:
   1.251 +     --{*part of the order type formalization*}
   1.252 +     "[| L(A); L(r) |] 
   1.253 +      ==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. 
   1.254 +	     ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
   1.255 +	     order_isomorphism(L,par,r,x,mx,g))"
   1.256 +apply (rule separation_CollectI) 
   1.257 +apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) 
   1.258 +apply (rule ReflectsE [OF obase_reflects], assumption)
   1.259 +apply (drule subset_Lset_ltD, assumption) 
   1.260 +apply (erule reflection_imp_L_separation)
   1.261 +  apply (simp_all add: lt_Ord2)
   1.262 +apply (rule DPowI2)
   1.263 +apply (rename_tac u) 
   1.264  apply (rule bex_iff_sats)
   1.265  apply (rule conj_iff_sats)
   1.266 -apply (rule fun_apply_iff_sats) 
   1.267 -apply (blast intro: nth_0 nth_ConsI) 
   1.268 -apply (blast intro: nth_0 nth_ConsI) 
   1.269 -apply (blast intro: nth_0 nth_ConsI, simp_all) 
   1.270 -apply (rule bex_iff_sats)
   1.271 -apply (rule conj_iff_sats)
   1.272 -apply (rule pair_iff_sats) 
   1.273 -apply (blast intro: nth_0 nth_ConsI) 
   1.274 -apply (blast intro: nth_0 nth_ConsI) 
   1.275 -apply (blast intro: nth_0 nth_ConsI, simp_all) 
   1.276 -apply (rule mem_iff_sats)
   1.277 -apply (blast intro: nth_0 nth_ConsI) 
   1.278 -apply (blast intro: nth_0 nth_ConsI)
   1.279 +apply (rule_tac env = "[x,u,A,r]" in ordinal_iff_sats) 
   1.280 +apply (rule sep_rules | simp)+
   1.281 +apply (simp_all add: succ_Un_distrib [symmetric])
   1.282 +done
   1.283 +
   1.284 +
   1.285 +subsection{*Separation for @{term "well_ord_iso"}*}
   1.286 +
   1.287 +lemma obase_equals_reflects:
   1.288 +  "REFLECTS[\<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L]. 
   1.289 +		ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L]. 
   1.290 +		membership(L,y,my) & pred_set(L,A,x,r,pxr) &
   1.291 +		order_isomorphism(L,pxr,r,y,my,g))),
   1.292 +	\<lambda>i x. x\<in>A --> ~(\<exists>y \<in> Lset(i). \<exists>g \<in> Lset(i). 
   1.293 +		ordinal(**Lset(i),y) & (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i). 
   1.294 +		membership(**Lset(i),y,my) & pred_set(**Lset(i),A,x,r,pxr) &
   1.295 +		order_isomorphism(**Lset(i),pxr,r,y,my,g)))]"
   1.296 +by (intro FOL_reflection function_reflection fun_plus_reflection)
   1.297 +
   1.298 +
   1.299 +lemma obase_equals_separation:
   1.300 +     "[| L(A); L(r) |] 
   1.301 +      ==> separation (L, \<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L]. 
   1.302 +			      ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L]. 
   1.303 +			      membership(L,y,my) & pred_set(L,A,x,r,pxr) &
   1.304 +			      order_isomorphism(L,pxr,r,y,my,g))))"
   1.305 +apply (rule separation_CollectI) 
   1.306 +apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) 
   1.307 +apply (rule ReflectsE [OF obase_equals_reflects], assumption)
   1.308 +apply (drule subset_Lset_ltD, assumption) 
   1.309 +apply (erule reflection_imp_L_separation)
   1.310 +  apply (simp_all add: lt_Ord2)
   1.311 +apply (rule DPowI2)
   1.312 +apply (rename_tac u) 
   1.313 +apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+
   1.314 +apply (rule_tac env = "[u,A,r]" in mem_iff_sats) 
   1.315 +apply (rule sep_rules | simp)+
   1.316 +apply (simp_all add: succ_Un_distrib [symmetric])
   1.317 +done
   1.318 +
   1.319 +
   1.320 +subsection{*Replacement for @{term "omap"}*}
   1.321 +
   1.322 +lemma omap_reflects:
   1.323 + "REFLECTS[\<lambda>z. \<exists>a[L]. a\<in>B & (\<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. 
   1.324 +     ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & 
   1.325 +     pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g)),
   1.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). 
   1.327 +        \<exists>par \<in> Lset(i). 
   1.328 +	 ordinal(**Lset(i),x) & pair(**Lset(i),a,x,z) & 
   1.329 +         membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) & 
   1.330 +         order_isomorphism(**Lset(i),par,r,x,mx,g))]"
   1.331 +by (intro FOL_reflection function_reflection fun_plus_reflection)
   1.332 +
   1.333 +lemma omap_replacement:
   1.334 +     "[| L(A); L(r) |] 
   1.335 +      ==> strong_replacement(L,
   1.336 +             \<lambda>a z. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. 
   1.337 +	     ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & 
   1.338 +	     pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
   1.339 +apply (rule strong_replacementI) 
   1.340 +apply (rule rallI)
   1.341 +apply (rename_tac B)  
   1.342 +apply (rule separation_CollectI) 
   1.343 +apply (rule_tac A="{A,B,r,z}" in subset_LsetE, blast ) 
   1.344 +apply (rule ReflectsE [OF omap_reflects], assumption)
   1.345 +apply (drule subset_Lset_ltD, assumption) 
   1.346 +apply (erule reflection_imp_L_separation)
   1.347 +  apply (simp_all add: lt_Ord2)
   1.348 +apply (rule DPowI2)
   1.349 +apply (rename_tac u) 
   1.350 +apply (rule bex_iff_sats conj_iff_sats)+
   1.351 +apply (rule_tac env = "[x,u,A,B,r]" in mem_iff_sats) 
   1.352 +apply (rule sep_rules | simp)+
   1.353  apply (simp_all add: succ_Un_distrib [symmetric])
   1.354  done
   1.355