59 apply (rule_tac A="{A,z}" in subset_LsetE, blast ) |
59 apply (rule_tac A="{A,z}" in subset_LsetE, blast ) |
60 apply (rule ReflectsE [OF Inter_Reflects], assumption) |
60 apply (rule ReflectsE [OF Inter_Reflects], assumption) |
61 apply (drule subset_Lset_ltD, assumption) |
61 apply (drule subset_Lset_ltD, assumption) |
62 apply (erule reflection_imp_L_separation) |
62 apply (erule reflection_imp_L_separation) |
63 apply (simp_all add: lt_Ord2, clarify) |
63 apply (simp_all add: lt_Ord2, clarify) |
64 apply (rule DPowI2) |
64 apply (rule DPow_LsetI) |
65 apply (rule ball_iff_sats) |
65 apply (rule ball_iff_sats) |
66 apply (rule imp_iff_sats) |
66 apply (rule imp_iff_sats) |
67 apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats) |
67 apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats) |
68 apply (rule_tac i=0 and j=2 in mem_iff_sats) |
68 apply (rule_tac i=0 and j=2 in mem_iff_sats) |
69 apply (simp_all add: succ_Un_distrib [symmetric]) |
69 apply (simp_all add: succ_Un_distrib [symmetric]) |
84 apply (rule_tac A="{A,B,z}" in subset_LsetE, blast ) |
84 apply (rule_tac A="{A,B,z}" in subset_LsetE, blast ) |
85 apply (rule ReflectsE [OF cartprod_Reflects], assumption) |
85 apply (rule ReflectsE [OF cartprod_Reflects], assumption) |
86 apply (drule subset_Lset_ltD, assumption) |
86 apply (drule subset_Lset_ltD, assumption) |
87 apply (erule reflection_imp_L_separation) |
87 apply (erule reflection_imp_L_separation) |
88 apply (simp_all add: lt_Ord2, clarify) |
88 apply (simp_all add: lt_Ord2, clarify) |
89 apply (rule DPowI2) |
89 apply (rule DPow_LsetI) |
90 apply (rename_tac u) |
90 apply (rename_tac u) |
91 apply (rule bex_iff_sats) |
91 apply (rule bex_iff_sats) |
92 apply (rule conj_iff_sats) |
92 apply (rule conj_iff_sats) |
93 apply (rule_tac i=0 and j=2 and env="[x,u,A,B]" in mem_iff_sats, simp_all) |
93 apply (rule_tac i=0 and j=2 and env="[x,u,A,B]" in mem_iff_sats, simp_all) |
94 apply (rule sep_rules | simp)+ |
94 apply (rule sep_rules | simp)+ |
95 apply (simp_all add: succ_Un_distrib [symmetric]) |
|
96 done |
95 done |
97 |
96 |
98 subsection{*Separation for Image*} |
97 subsection{*Separation for Image*} |
99 |
98 |
100 lemma image_Reflects: |
99 lemma image_Reflects: |
109 apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) |
108 apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) |
110 apply (rule ReflectsE [OF image_Reflects], assumption) |
109 apply (rule ReflectsE [OF image_Reflects], assumption) |
111 apply (drule subset_Lset_ltD, assumption) |
110 apply (drule subset_Lset_ltD, assumption) |
112 apply (erule reflection_imp_L_separation) |
111 apply (erule reflection_imp_L_separation) |
113 apply (simp_all add: lt_Ord2, clarify) |
112 apply (simp_all add: lt_Ord2, clarify) |
114 apply (rule DPowI2) |
113 apply (rule DPow_LsetI) |
115 apply (rule bex_iff_sats) |
114 apply (rule bex_iff_sats) |
116 apply (rule conj_iff_sats) |
115 apply (rule conj_iff_sats) |
117 apply (rule_tac env="[p,y,A,r]" in mem_iff_sats) |
116 apply (rule_tac env="[p,y,A,r]" in mem_iff_sats) |
118 apply (rule sep_rules | simp)+ |
117 apply (rule sep_rules | simp)+ |
119 apply (simp_all add: succ_Un_distrib [symmetric]) |
|
120 done |
118 done |
121 |
119 |
122 |
120 |
123 subsection{*Separation for Converse*} |
121 subsection{*Separation for Converse*} |
124 |
122 |
135 apply (rule_tac A="{r,z}" in subset_LsetE, blast ) |
133 apply (rule_tac A="{r,z}" in subset_LsetE, blast ) |
136 apply (rule ReflectsE [OF converse_Reflects], assumption) |
134 apply (rule ReflectsE [OF converse_Reflects], assumption) |
137 apply (drule subset_Lset_ltD, assumption) |
135 apply (drule subset_Lset_ltD, assumption) |
138 apply (erule reflection_imp_L_separation) |
136 apply (erule reflection_imp_L_separation) |
139 apply (simp_all add: lt_Ord2, clarify) |
137 apply (simp_all add: lt_Ord2, clarify) |
140 apply (rule DPowI2) |
138 apply (rule DPow_LsetI) |
141 apply (rename_tac u) |
139 apply (rename_tac u) |
142 apply (rule bex_iff_sats) |
140 apply (rule bex_iff_sats) |
143 apply (rule conj_iff_sats) |
141 apply (rule conj_iff_sats) |
144 apply (rule_tac i=0 and j=2 and env="[p,u,r]" in mem_iff_sats, simp_all) |
142 apply (rule_tac i=0 and j=2 and env="[p,u,r]" in mem_iff_sats, simp_all) |
145 apply (rule sep_rules | simp)+ |
143 apply (rule sep_rules | simp)+ |
146 apply (simp_all add: succ_Un_distrib [symmetric]) |
|
147 done |
144 done |
148 |
145 |
149 |
146 |
150 subsection{*Separation for Restriction*} |
147 subsection{*Separation for Restriction*} |
151 |
148 |
160 apply (rule_tac A="{A,z}" in subset_LsetE, blast ) |
157 apply (rule_tac A="{A,z}" in subset_LsetE, blast ) |
161 apply (rule ReflectsE [OF restrict_Reflects], assumption) |
158 apply (rule ReflectsE [OF restrict_Reflects], assumption) |
162 apply (drule subset_Lset_ltD, assumption) |
159 apply (drule subset_Lset_ltD, assumption) |
163 apply (erule reflection_imp_L_separation) |
160 apply (erule reflection_imp_L_separation) |
164 apply (simp_all add: lt_Ord2, clarify) |
161 apply (simp_all add: lt_Ord2, clarify) |
165 apply (rule DPowI2) |
162 apply (rule DPow_LsetI) |
166 apply (rename_tac u) |
163 apply (rename_tac u) |
167 apply (rule bex_iff_sats) |
164 apply (rule bex_iff_sats) |
168 apply (rule conj_iff_sats) |
165 apply (rule conj_iff_sats) |
169 apply (rule_tac i=0 and j=2 and env="[x,u,A]" in mem_iff_sats, simp_all) |
166 apply (rule_tac i=0 and j=2 and env="[x,u,A]" in mem_iff_sats, simp_all) |
170 apply (rule sep_rules | simp)+ |
167 apply (rule sep_rules | simp)+ |
171 apply (simp_all add: succ_Un_distrib [symmetric]) |
|
172 done |
168 done |
173 |
169 |
174 |
170 |
175 subsection{*Separation for Composition*} |
171 subsection{*Separation for Composition*} |
176 |
172 |
192 apply (rule_tac A="{r,s,z}" in subset_LsetE, blast ) |
188 apply (rule_tac A="{r,s,z}" in subset_LsetE, blast ) |
193 apply (rule ReflectsE [OF comp_Reflects], assumption) |
189 apply (rule ReflectsE [OF comp_Reflects], assumption) |
194 apply (drule subset_Lset_ltD, assumption) |
190 apply (drule subset_Lset_ltD, assumption) |
195 apply (erule reflection_imp_L_separation) |
191 apply (erule reflection_imp_L_separation) |
196 apply (simp_all add: lt_Ord2, clarify) |
192 apply (simp_all add: lt_Ord2, clarify) |
197 apply (rule DPowI2) |
193 apply (rule DPow_LsetI) |
198 apply (rename_tac u) |
194 apply (rename_tac u) |
199 apply (rule bex_iff_sats)+ |
195 apply (rule bex_iff_sats)+ |
200 apply (rename_tac x y z) |
196 apply (rename_tac x y z) |
201 apply (rule conj_iff_sats) |
197 apply (rule conj_iff_sats) |
202 apply (rule_tac env="[z,y,x,u,r,s]" in pair_iff_sats) |
198 apply (rule_tac env="[z,y,x,u,r,s]" in pair_iff_sats) |
203 apply (rule sep_rules | simp)+ |
199 apply (rule sep_rules | simp)+ |
204 apply (simp_all add: succ_Un_distrib [symmetric]) |
|
205 done |
200 done |
206 |
201 |
207 subsection{*Separation for Predecessors in an Order*} |
202 subsection{*Separation for Predecessors in an Order*} |
208 |
203 |
209 lemma pred_Reflects: |
204 lemma pred_Reflects: |
217 apply (rule_tac A="{r,x,z}" in subset_LsetE, blast ) |
212 apply (rule_tac A="{r,x,z}" in subset_LsetE, blast ) |
218 apply (rule ReflectsE [OF pred_Reflects], assumption) |
213 apply (rule ReflectsE [OF pred_Reflects], assumption) |
219 apply (drule subset_Lset_ltD, assumption) |
214 apply (drule subset_Lset_ltD, assumption) |
220 apply (erule reflection_imp_L_separation) |
215 apply (erule reflection_imp_L_separation) |
221 apply (simp_all add: lt_Ord2, clarify) |
216 apply (simp_all add: lt_Ord2, clarify) |
222 apply (rule DPowI2) |
217 apply (rule DPow_LsetI) |
223 apply (rename_tac u) |
218 apply (rename_tac u) |
224 apply (rule bex_iff_sats) |
219 apply (rule bex_iff_sats) |
225 apply (rule conj_iff_sats) |
220 apply (rule conj_iff_sats) |
226 apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats) |
221 apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats) |
227 apply (rule sep_rules | simp)+ |
222 apply (rule sep_rules | simp)+ |
228 apply (simp_all add: succ_Un_distrib [symmetric]) |
|
229 done |
223 done |
230 |
224 |
231 |
225 |
232 subsection{*Separation for the Membership Relation*} |
226 subsection{*Separation for the Membership Relation*} |
233 |
227 |
242 apply (rule_tac A="{z}" in subset_LsetE, blast ) |
236 apply (rule_tac A="{z}" in subset_LsetE, blast ) |
243 apply (rule ReflectsE [OF Memrel_Reflects], assumption) |
237 apply (rule ReflectsE [OF Memrel_Reflects], assumption) |
244 apply (drule subset_Lset_ltD, assumption) |
238 apply (drule subset_Lset_ltD, assumption) |
245 apply (erule reflection_imp_L_separation) |
239 apply (erule reflection_imp_L_separation) |
246 apply (simp_all add: lt_Ord2) |
240 apply (simp_all add: lt_Ord2) |
247 apply (rule DPowI2) |
241 apply (rule DPow_LsetI) |
248 apply (rename_tac u) |
242 apply (rename_tac u) |
249 apply (rule bex_iff_sats conj_iff_sats)+ |
243 apply (rule bex_iff_sats conj_iff_sats)+ |
250 apply (rule_tac env = "[y,x,u]" in pair_iff_sats) |
244 apply (rule_tac env = "[y,x,u]" in pair_iff_sats) |
251 apply (rule sep_rules | simp)+ |
245 apply (rule sep_rules | simp)+ |
252 apply (simp_all add: succ_Un_distrib [symmetric]) |
|
253 done |
246 done |
254 |
247 |
255 |
248 |
256 subsection{*Replacement for FunSpace*} |
249 subsection{*Replacement for FunSpace*} |
257 |
250 |
276 apply (rule_tac A="{n,A,z}" in subset_LsetE, blast ) |
269 apply (rule_tac A="{n,A,z}" in subset_LsetE, blast ) |
277 apply (rule ReflectsE [OF funspace_succ_Reflects], assumption) |
270 apply (rule ReflectsE [OF funspace_succ_Reflects], assumption) |
278 apply (drule subset_Lset_ltD, assumption) |
271 apply (drule subset_Lset_ltD, assumption) |
279 apply (erule reflection_imp_L_separation) |
272 apply (erule reflection_imp_L_separation) |
280 apply (simp_all add: lt_Ord2) |
273 apply (simp_all add: lt_Ord2) |
281 apply (rule DPowI2) |
274 apply (rule DPow_LsetI) |
282 apply (rename_tac u) |
275 apply (rename_tac u) |
283 apply (rule bex_iff_sats) |
276 apply (rule bex_iff_sats) |
284 apply (rule conj_iff_sats) |
277 apply (rule conj_iff_sats) |
285 apply (rule_tac env = "[p,u,n,A]" in mem_iff_sats) |
278 apply (rule_tac env = "[p,u,n,A]" in mem_iff_sats) |
286 apply (rule sep_rules | simp)+ |
279 apply (rule sep_rules | simp)+ |
287 apply (simp_all add: succ_Un_distrib [symmetric]) |
|
288 done |
280 done |
289 |
281 |
290 |
282 |
291 subsection{*Separation for Order-Isomorphisms*} |
283 subsection{*Separation for Order-Isomorphisms*} |
292 |
284 |
305 apply (rule_tac A="{A,f,r,z}" in subset_LsetE, blast ) |
297 apply (rule_tac A="{A,f,r,z}" in subset_LsetE, blast ) |
306 apply (rule ReflectsE [OF well_ord_iso_Reflects], assumption) |
298 apply (rule ReflectsE [OF well_ord_iso_Reflects], assumption) |
307 apply (drule subset_Lset_ltD, assumption) |
299 apply (drule subset_Lset_ltD, assumption) |
308 apply (erule reflection_imp_L_separation) |
300 apply (erule reflection_imp_L_separation) |
309 apply (simp_all add: lt_Ord2) |
301 apply (simp_all add: lt_Ord2) |
310 apply (rule DPowI2) |
302 apply (rule DPow_LsetI) |
311 apply (rename_tac u) |
303 apply (rename_tac u) |
312 apply (rule imp_iff_sats) |
304 apply (rule imp_iff_sats) |
313 apply (rule_tac env = "[u,A,f,r]" in mem_iff_sats) |
305 apply (rule_tac env = "[u,A,f,r]" in mem_iff_sats) |
314 apply (rule sep_rules | simp)+ |
306 apply (rule sep_rules | simp)+ |
315 apply (simp_all add: succ_Un_distrib [symmetric]) |
|
316 done |
307 done |
317 |
308 |
318 |
309 |
319 subsection{*Separation for @{term "obase"}*} |
310 subsection{*Separation for @{term "obase"}*} |
320 |
311 |
337 apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) |
328 apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) |
338 apply (rule ReflectsE [OF obase_reflects], assumption) |
329 apply (rule ReflectsE [OF obase_reflects], assumption) |
339 apply (drule subset_Lset_ltD, assumption) |
330 apply (drule subset_Lset_ltD, assumption) |
340 apply (erule reflection_imp_L_separation) |
331 apply (erule reflection_imp_L_separation) |
341 apply (simp_all add: lt_Ord2) |
332 apply (simp_all add: lt_Ord2) |
342 apply (rule DPowI2) |
333 apply (rule DPow_LsetI) |
343 apply (rename_tac u) |
334 apply (rename_tac u) |
344 apply (rule bex_iff_sats) |
335 apply (rule bex_iff_sats) |
345 apply (rule conj_iff_sats) |
336 apply (rule conj_iff_sats) |
346 apply (rule_tac env = "[x,u,A,r]" in ordinal_iff_sats) |
337 apply (rule_tac env = "[x,u,A,r]" in ordinal_iff_sats) |
347 apply (rule sep_rules | simp)+ |
338 apply (rule sep_rules | simp)+ |
348 apply (simp_all add: succ_Un_distrib [symmetric]) |
|
349 done |
339 done |
350 |
340 |
351 |
341 |
352 subsection{*Separation for a Theorem about @{term "obase"}*} |
342 subsection{*Separation for a Theorem about @{term "obase"}*} |
353 |
343 |
373 apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) |
363 apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) |
374 apply (rule ReflectsE [OF obase_equals_reflects], assumption) |
364 apply (rule ReflectsE [OF obase_equals_reflects], assumption) |
375 apply (drule subset_Lset_ltD, assumption) |
365 apply (drule subset_Lset_ltD, assumption) |
376 apply (erule reflection_imp_L_separation) |
366 apply (erule reflection_imp_L_separation) |
377 apply (simp_all add: lt_Ord2) |
367 apply (simp_all add: lt_Ord2) |
378 apply (rule DPowI2) |
368 apply (rule DPow_LsetI) |
379 apply (rename_tac u) |
369 apply (rename_tac u) |
380 apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+ |
370 apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+ |
381 apply (rule_tac env = "[u,A,r]" in mem_iff_sats) |
371 apply (rule_tac env = "[u,A,r]" in mem_iff_sats) |
382 apply (rule sep_rules | simp)+ |
372 apply (rule sep_rules | simp)+ |
383 apply (simp_all add: succ_Un_distrib [symmetric]) |
|
384 done |
373 done |
385 |
374 |
386 |
375 |
387 subsection{*Replacement for @{term "omap"}*} |
376 subsection{*Replacement for @{term "omap"}*} |
388 |
377 |
410 apply (rule_tac A="{A,B,r,z}" in subset_LsetE, blast ) |
399 apply (rule_tac A="{A,B,r,z}" in subset_LsetE, blast ) |
411 apply (rule ReflectsE [OF omap_reflects], assumption) |
400 apply (rule ReflectsE [OF omap_reflects], assumption) |
412 apply (drule subset_Lset_ltD, assumption) |
401 apply (drule subset_Lset_ltD, assumption) |
413 apply (erule reflection_imp_L_separation) |
402 apply (erule reflection_imp_L_separation) |
414 apply (simp_all add: lt_Ord2) |
403 apply (simp_all add: lt_Ord2) |
415 apply (rule DPowI2) |
404 apply (rule DPow_LsetI) |
416 apply (rename_tac u) |
405 apply (rename_tac u) |
417 apply (rule bex_iff_sats conj_iff_sats)+ |
406 apply (rule bex_iff_sats conj_iff_sats)+ |
418 apply (rule_tac env = "[a,u,A,B,r]" in mem_iff_sats) |
407 apply (rule_tac env = "[a,u,A,B,r]" in mem_iff_sats) |
419 apply (rule sep_rules | simp)+ |
408 apply (rule sep_rules | simp)+ |
420 apply (simp_all add: succ_Un_distrib [symmetric]) |
|
421 done |
409 done |
422 |
410 |
423 |
411 |
424 subsection{*Separation for a Theorem about @{term "obase"}*} |
412 subsection{*Separation for a Theorem about @{term "obase"}*} |
425 |
413 |
446 apply (rule_tac A="{r,f,g,a,b,z}" in subset_LsetE, blast ) |
434 apply (rule_tac A="{r,f,g,a,b,z}" in subset_LsetE, blast ) |
447 apply (rule ReflectsE [OF is_recfun_reflects], assumption) |
435 apply (rule ReflectsE [OF is_recfun_reflects], assumption) |
448 apply (drule subset_Lset_ltD, assumption) |
436 apply (drule subset_Lset_ltD, assumption) |
449 apply (erule reflection_imp_L_separation) |
437 apply (erule reflection_imp_L_separation) |
450 apply (simp_all add: lt_Ord2) |
438 apply (simp_all add: lt_Ord2) |
451 apply (rule DPowI2) |
439 apply (rule DPow_LsetI) |
452 apply (rename_tac u) |
440 apply (rename_tac u) |
453 apply (rule bex_iff_sats conj_iff_sats)+ |
441 apply (rule bex_iff_sats conj_iff_sats)+ |
454 apply (rule_tac env = "[xa,u,r,f,g,a,b]" in pair_iff_sats) |
442 apply (rule_tac env = "[xa,u,r,f,g,a,b]" in pair_iff_sats) |
455 apply (rule sep_rules | simp)+ |
443 apply (rule sep_rules | simp)+ |
456 apply (simp_all add: succ_Un_distrib [symmetric]) |
|
457 done |
444 done |
458 |
445 |
459 |
446 |
460 subsection{*Instantiating the locale @{text M_axioms}*} |
447 subsection{*Instantiating the locale @{text M_axioms}*} |
461 text{*Separation (and Strong Replacement) for basic set-theoretic constructions |
448 text{*Separation (and Strong Replacement) for basic set-theoretic constructions |