230 \<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(**Lset(i),x,y,z) & x \<in> y]" |
230 \<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(**Lset(i),x,y,z) & x \<in> y]" |
231 by (intro FOL_reflections function_reflections) |
231 by (intro FOL_reflections function_reflections) |
232 |
232 |
233 lemma Memrel_separation: |
233 lemma Memrel_separation: |
234 "separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)" |
234 "separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)" |
235 apply (rule separation_CollectI) |
235 apply (rule separation_CollectI) |
236 apply (rule_tac A="{z}" in subset_LsetE, blast ) |
236 apply (rule_tac A="{z}" in subset_LsetE, blast ) |
237 apply (rule ReflectsE [OF Memrel_Reflects], assumption) |
237 apply (rule ReflectsE [OF Memrel_Reflects], assumption) |
238 apply (drule subset_Lset_ltD, assumption) |
238 apply (drule subset_Lset_ltD, assumption) |
239 apply (erule reflection_imp_L_separation) |
239 apply (erule reflection_imp_L_separation) |
240 apply (simp_all add: lt_Ord2) |
240 apply (simp_all add: lt_Ord2) |
241 apply (rule DPow_LsetI) |
241 apply (rule DPow_LsetI) |
242 apply (rename_tac u) |
242 apply (rename_tac u) |
243 apply (rule bex_iff_sats conj_iff_sats)+ |
243 apply (rule bex_iff_sats conj_iff_sats)+ |
244 apply (rule_tac env = "[y,x,u]" in pair_iff_sats) |
244 apply (rule_tac env = "[y,x,u]" in pair_iff_sats) |
245 apply (rule sep_rules | simp)+ |
245 apply (rule sep_rules | simp)+ |
246 done |
246 done |
247 |
247 |
248 |
248 |
249 subsection{*Replacement for FunSpace*} |
249 subsection{*Replacement for FunSpace*} |
250 |
250 |
251 lemma funspace_succ_Reflects: |
251 lemma funspace_succ_Reflects: |
252 "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>A & (\<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L]. |
252 "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>A & (\<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L]. |
253 pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) & |
253 pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) & |
254 upair(L,cnbf,cnbf,z)), |
254 upair(L,cnbf,cnbf,z)), |
255 \<lambda>i z. \<exists>p \<in> Lset(i). p\<in>A & (\<exists>f \<in> Lset(i). \<exists>b \<in> Lset(i). |
255 \<lambda>i z. \<exists>p \<in> Lset(i). p\<in>A & (\<exists>f \<in> Lset(i). \<exists>b \<in> Lset(i). |
256 \<exists>nb \<in> Lset(i). \<exists>cnbf \<in> Lset(i). |
256 \<exists>nb \<in> Lset(i). \<exists>cnbf \<in> Lset(i). |
257 pair(**Lset(i),f,b,p) & pair(**Lset(i),n,b,nb) & |
257 pair(**Lset(i),f,b,p) & pair(**Lset(i),n,b,nb) & |
258 is_cons(**Lset(i),nb,f,cnbf) & upair(**Lset(i),cnbf,cnbf,z))]" |
258 is_cons(**Lset(i),nb,f,cnbf) & upair(**Lset(i),cnbf,cnbf,z))]" |
259 by (intro FOL_reflections function_reflections) |
259 by (intro FOL_reflections function_reflections) |
260 |
260 |
261 lemma funspace_succ_replacement: |
261 lemma funspace_succ_replacement: |
262 "L(n) ==> |
262 "L(n) ==> |
263 strong_replacement(L, \<lambda>p z. \<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L]. |
263 strong_replacement(L, \<lambda>p z. \<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L]. |
264 pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) & |
264 pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) & |
265 upair(L,cnbf,cnbf,z))" |
265 upair(L,cnbf,cnbf,z))" |
266 apply (rule strong_replacementI) |
266 apply (rule strong_replacementI) |
267 apply (rule rallI) |
267 apply (rule rallI) |
268 apply (rule separation_CollectI) |
268 apply (rule separation_CollectI) |
269 apply (rule_tac A="{n,A,z}" in subset_LsetE, blast ) |
269 apply (rule_tac A="{n,A,z}" in subset_LsetE, blast ) |
270 apply (rule ReflectsE [OF funspace_succ_Reflects], assumption) |
270 apply (rule ReflectsE [OF funspace_succ_Reflects], assumption) |
271 apply (drule subset_Lset_ltD, assumption) |
271 apply (drule subset_Lset_ltD, assumption) |
272 apply (erule reflection_imp_L_separation) |
272 apply (erule reflection_imp_L_separation) |
273 apply (simp_all add: lt_Ord2) |
273 apply (simp_all add: lt_Ord2) |
274 apply (rule DPow_LsetI) |
274 apply (rule DPow_LsetI) |
275 apply (rename_tac u) |
275 apply (rename_tac u) |
276 apply (rule bex_iff_sats) |
276 apply (rule bex_iff_sats) |
277 apply (rule conj_iff_sats) |
277 apply (rule conj_iff_sats) |
278 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) |
279 apply (rule sep_rules | simp)+ |
279 apply (rule sep_rules | simp)+ |
280 done |
280 done |
281 |
281 |
282 |
282 |
283 subsection{*Separation for Order-Isomorphisms*} |
283 subsection{*Separation for Order-Isomorphisms*} |
284 |
284 |
285 lemma well_ord_iso_Reflects: |
285 lemma well_ord_iso_Reflects: |
286 "REFLECTS[\<lambda>x. x\<in>A --> |
286 "REFLECTS[\<lambda>x. x\<in>A --> |
287 (\<exists>y[L]. \<exists>p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r), |
287 (\<exists>y[L]. \<exists>p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r), |
288 \<lambda>i x. x\<in>A --> (\<exists>y \<in> Lset(i). \<exists>p \<in> Lset(i). |
288 \<lambda>i x. x\<in>A --> (\<exists>y \<in> Lset(i). \<exists>p \<in> Lset(i). |
289 fun_apply(**Lset(i),f,x,y) & pair(**Lset(i),y,x,p) & p \<in> r)]" |
289 fun_apply(**Lset(i),f,x,y) & pair(**Lset(i),y,x,p) & p \<in> r)]" |
290 by (intro FOL_reflections function_reflections) |
290 by (intro FOL_reflections function_reflections) |
291 |
291 |
292 lemma well_ord_iso_separation: |
292 lemma well_ord_iso_separation: |
293 "[| L(A); L(f); L(r) |] |
293 "[| L(A); L(f); L(r) |] |
294 ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y[L]. (\<exists>p[L]. |
294 ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y[L]. (\<exists>p[L]. |
295 fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r)))" |
295 fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r)))" |
296 apply (rule separation_CollectI) |
296 apply (rule separation_CollectI) |
297 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 ) |
298 apply (rule ReflectsE [OF well_ord_iso_Reflects], assumption) |
298 apply (rule ReflectsE [OF well_ord_iso_Reflects], assumption) |
299 apply (drule subset_Lset_ltD, assumption) |
299 apply (drule subset_Lset_ltD, assumption) |
300 apply (erule reflection_imp_L_separation) |
300 apply (erule reflection_imp_L_separation) |
301 apply (simp_all add: lt_Ord2) |
301 apply (simp_all add: lt_Ord2) |
302 apply (rule DPow_LsetI) |
302 apply (rule DPow_LsetI) |
303 apply (rename_tac u) |
303 apply (rename_tac u) |
304 apply (rule imp_iff_sats) |
304 apply (rule imp_iff_sats) |
305 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) |
306 apply (rule sep_rules | simp)+ |
306 apply (rule sep_rules | simp)+ |
307 done |
307 done |
308 |
308 |
309 |
309 |
310 subsection{*Separation for @{term "obase"}*} |
310 subsection{*Separation for @{term "obase"}*} |
311 |
311 |
312 lemma obase_reflects: |
312 lemma obase_reflects: |
313 "REFLECTS[\<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
313 "REFLECTS[\<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
314 ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) & |
314 ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) & |
315 order_isomorphism(L,par,r,x,mx,g), |
315 order_isomorphism(L,par,r,x,mx,g), |
316 \<lambda>i a. \<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). \<exists>par \<in> Lset(i). |
316 \<lambda>i a. \<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). \<exists>par \<in> Lset(i). |
317 ordinal(**Lset(i),x) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) & |
317 ordinal(**Lset(i),x) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) & |
318 order_isomorphism(**Lset(i),par,r,x,mx,g)]" |
318 order_isomorphism(**Lset(i),par,r,x,mx,g)]" |
319 by (intro FOL_reflections function_reflections fun_plus_reflections) |
319 by (intro FOL_reflections function_reflections fun_plus_reflections) |
320 |
320 |
321 lemma obase_separation: |
321 lemma obase_separation: |
322 --{*part of the order type formalization*} |
322 --{*part of the order type formalization*} |
323 "[| L(A); L(r) |] |
323 "[| L(A); L(r) |] |
324 ==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
324 ==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
325 ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) & |
325 ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) & |
326 order_isomorphism(L,par,r,x,mx,g))" |
326 order_isomorphism(L,par,r,x,mx,g))" |
327 apply (rule separation_CollectI) |
327 apply (rule separation_CollectI) |
328 apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) |
328 apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) |
329 apply (rule ReflectsE [OF obase_reflects], assumption) |
329 apply (rule ReflectsE [OF obase_reflects], assumption) |
330 apply (drule subset_Lset_ltD, assumption) |
330 apply (drule subset_Lset_ltD, assumption) |
331 apply (erule reflection_imp_L_separation) |
331 apply (erule reflection_imp_L_separation) |
332 apply (simp_all add: lt_Ord2) |
332 apply (simp_all add: lt_Ord2) |
333 apply (rule DPow_LsetI) |
333 apply (rule DPow_LsetI) |
334 apply (rename_tac u) |
334 apply (rename_tac u) |
335 apply (rule bex_iff_sats) |
335 apply (rule bex_iff_sats) |
336 apply (rule conj_iff_sats) |
336 apply (rule conj_iff_sats) |
337 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) |
338 apply (rule sep_rules | simp)+ |
338 apply (rule sep_rules | simp)+ |
339 done |
339 done |
340 |
340 |
341 |
341 |
342 subsection{*Separation for a Theorem about @{term "obase"}*} |
342 subsection{*Separation for a Theorem about @{term "obase"}*} |
343 |
343 |
344 lemma obase_equals_reflects: |
344 lemma obase_equals_reflects: |
345 "REFLECTS[\<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L]. |
345 "REFLECTS[\<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L]. |
346 ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L]. |
346 ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L]. |
347 membership(L,y,my) & pred_set(L,A,x,r,pxr) & |
347 membership(L,y,my) & pred_set(L,A,x,r,pxr) & |
348 order_isomorphism(L,pxr,r,y,my,g))), |
348 order_isomorphism(L,pxr,r,y,my,g))), |
349 \<lambda>i x. x\<in>A --> ~(\<exists>y \<in> Lset(i). \<exists>g \<in> Lset(i). |
349 \<lambda>i x. x\<in>A --> ~(\<exists>y \<in> Lset(i). \<exists>g \<in> Lset(i). |
350 ordinal(**Lset(i),y) & (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i). |
350 ordinal(**Lset(i),y) & (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i). |
351 membership(**Lset(i),y,my) & pred_set(**Lset(i),A,x,r,pxr) & |
351 membership(**Lset(i),y,my) & pred_set(**Lset(i),A,x,r,pxr) & |
352 order_isomorphism(**Lset(i),pxr,r,y,my,g)))]" |
352 order_isomorphism(**Lset(i),pxr,r,y,my,g)))]" |
353 by (intro FOL_reflections function_reflections fun_plus_reflections) |
353 by (intro FOL_reflections function_reflections fun_plus_reflections) |
354 |
354 |
355 |
355 |
356 lemma obase_equals_separation: |
356 lemma obase_equals_separation: |
357 "[| L(A); L(r) |] |
357 "[| L(A); L(r) |] |
358 ==> separation (L, \<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L]. |
358 ==> separation (L, \<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L]. |
359 ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L]. |
359 ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L]. |
360 membership(L,y,my) & pred_set(L,A,x,r,pxr) & |
360 membership(L,y,my) & pred_set(L,A,x,r,pxr) & |
361 order_isomorphism(L,pxr,r,y,my,g))))" |
361 order_isomorphism(L,pxr,r,y,my,g))))" |
362 apply (rule separation_CollectI) |
362 apply (rule separation_CollectI) |
363 apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) |
363 apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) |
364 apply (rule ReflectsE [OF obase_equals_reflects], assumption) |
364 apply (rule ReflectsE [OF obase_equals_reflects], assumption) |
365 apply (drule subset_Lset_ltD, assumption) |
365 apply (drule subset_Lset_ltD, assumption) |
366 apply (erule reflection_imp_L_separation) |
366 apply (erule reflection_imp_L_separation) |
367 apply (simp_all add: lt_Ord2) |
367 apply (simp_all add: lt_Ord2) |
368 apply (rule DPow_LsetI) |
368 apply (rule DPow_LsetI) |
369 apply (rename_tac u) |
369 apply (rename_tac u) |
370 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)+ |
371 apply (rule_tac env = "[u,A,r]" in mem_iff_sats) |
371 apply (rule_tac env = "[u,A,r]" in mem_iff_sats) |
372 apply (rule sep_rules | simp)+ |
372 apply (rule sep_rules | simp)+ |
373 done |
373 done |
374 |
374 |
375 |
375 |
376 subsection{*Replacement for @{term "omap"}*} |
376 subsection{*Replacement for @{term "omap"}*} |
377 |
377 |
378 lemma omap_reflects: |
378 lemma omap_reflects: |
379 "REFLECTS[\<lambda>z. \<exists>a[L]. a\<in>B & (\<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
379 "REFLECTS[\<lambda>z. \<exists>a[L]. a\<in>B & (\<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
380 ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & |
380 ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & |
381 pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g)), |
381 pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g)), |
382 \<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). |
382 \<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). |
383 \<exists>par \<in> Lset(i). |
383 \<exists>par \<in> Lset(i). |
384 ordinal(**Lset(i),x) & pair(**Lset(i),a,x,z) & |
384 ordinal(**Lset(i),x) & pair(**Lset(i),a,x,z) & |
385 membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) & |
385 membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) & |
386 order_isomorphism(**Lset(i),par,r,x,mx,g))]" |
386 order_isomorphism(**Lset(i),par,r,x,mx,g))]" |
387 by (intro FOL_reflections function_reflections fun_plus_reflections) |
387 by (intro FOL_reflections function_reflections fun_plus_reflections) |
388 |
388 |
389 lemma omap_replacement: |
389 lemma omap_replacement: |
390 "[| L(A); L(r) |] |
390 "[| L(A); L(r) |] |
391 ==> strong_replacement(L, |
391 ==> strong_replacement(L, |
392 \<lambda>a z. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
392 \<lambda>a z. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
393 ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & |
393 ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & |
394 pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))" |
394 pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))" |
395 apply (rule strong_replacementI) |
395 apply (rule strong_replacementI) |
396 apply (rule rallI) |
396 apply (rule rallI) |
397 apply (rename_tac B) |
397 apply (rename_tac B) |
398 apply (rule separation_CollectI) |
398 apply (rule separation_CollectI) |
399 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 ) |
400 apply (rule ReflectsE [OF omap_reflects], assumption) |
400 apply (rule ReflectsE [OF omap_reflects], assumption) |
401 apply (drule subset_Lset_ltD, assumption) |
401 apply (drule subset_Lset_ltD, assumption) |
402 apply (erule reflection_imp_L_separation) |
402 apply (erule reflection_imp_L_separation) |
403 apply (simp_all add: lt_Ord2) |
403 apply (simp_all add: lt_Ord2) |
404 apply (rule DPow_LsetI) |
404 apply (rule DPow_LsetI) |
405 apply (rename_tac u) |
405 apply (rename_tac u) |
406 apply (rule bex_iff_sats conj_iff_sats)+ |
406 apply (rule bex_iff_sats conj_iff_sats)+ |
407 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) |
408 apply (rule sep_rules | simp)+ |
408 apply (rule sep_rules | simp)+ |
409 done |
409 done |
410 |
410 |
411 |
411 |
412 subsection{*Separation for a Theorem about @{term "obase"}*} |
412 subsection{*Separation for a Theorem about @{term "obase"}*} |
413 |
413 |
414 lemma is_recfun_reflects: |
414 lemma is_recfun_reflects: |
415 "REFLECTS[\<lambda>x. \<exists>xa[L]. \<exists>xb[L]. |
415 "REFLECTS[\<lambda>x. \<exists>xa[L]. \<exists>xb[L]. |
416 pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r & |
416 pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r & |
417 (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & |
417 (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & |
418 fx \<noteq> gx), |
418 fx \<noteq> gx), |
419 \<lambda>i x. \<exists>xa \<in> Lset(i). \<exists>xb \<in> Lset(i). |
419 \<lambda>i x. \<exists>xa \<in> Lset(i). \<exists>xb \<in> Lset(i). |
420 pair(**Lset(i),x,a,xa) & xa \<in> r & pair(**Lset(i),x,b,xb) & xb \<in> r & |
420 pair(**Lset(i),x,a,xa) & xa \<in> r & pair(**Lset(i),x,b,xb) & xb \<in> r & |
421 (\<exists>fx \<in> Lset(i). \<exists>gx \<in> Lset(i). fun_apply(**Lset(i),f,x,fx) & |
421 (\<exists>fx \<in> Lset(i). \<exists>gx \<in> Lset(i). fun_apply(**Lset(i),f,x,fx) & |
422 fun_apply(**Lset(i),g,x,gx) & fx \<noteq> gx)]" |
422 fun_apply(**Lset(i),g,x,gx) & fx \<noteq> gx)]" |
423 by (intro FOL_reflections function_reflections fun_plus_reflections) |
423 by (intro FOL_reflections function_reflections fun_plus_reflections) |
424 |
424 |
425 lemma is_recfun_separation: |
425 lemma is_recfun_separation: |
426 --{*for well-founded recursion*} |
426 --{*for well-founded recursion*} |
427 "[| L(r); L(f); L(g); L(a); L(b) |] |
427 "[| L(r); L(f); L(g); L(a); L(b) |] |
428 ==> separation(L, |
428 ==> separation(L, |
429 \<lambda>x. \<exists>xa[L]. \<exists>xb[L]. |
429 \<lambda>x. \<exists>xa[L]. \<exists>xb[L]. |
430 pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r & |
430 pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r & |
431 (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & |
431 (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & |
432 fx \<noteq> gx))" |
432 fx \<noteq> gx))" |
433 apply (rule separation_CollectI) |
433 apply (rule separation_CollectI) |
434 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 ) |
435 apply (rule ReflectsE [OF is_recfun_reflects], assumption) |
435 apply (rule ReflectsE [OF is_recfun_reflects], assumption) |
436 apply (drule subset_Lset_ltD, assumption) |
436 apply (drule subset_Lset_ltD, assumption) |
437 apply (erule reflection_imp_L_separation) |
437 apply (erule reflection_imp_L_separation) |
438 apply (simp_all add: lt_Ord2) |
438 apply (simp_all add: lt_Ord2) |
439 apply (rule DPow_LsetI) |
439 apply (rule DPow_LsetI) |
440 apply (rename_tac u) |
440 apply (rename_tac u) |
441 apply (rule bex_iff_sats conj_iff_sats)+ |
441 apply (rule bex_iff_sats conj_iff_sats)+ |
442 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) |
443 apply (rule sep_rules | simp)+ |
443 apply (rule sep_rules | simp)+ |
444 done |
444 done |
445 |
445 |
446 |
446 |
447 subsection{*Instantiating the locale @{text M_axioms}*} |
447 subsection{*Instantiating the locale @{text M_axioms}*} |
448 text{*Separation (and Strong Replacement) for basic set-theoretic constructions |
448 text{*Separation (and Strong Replacement) for basic set-theoretic constructions |
449 such as intersection, Cartesian Product and image.*} |
449 such as intersection, Cartesian Product and image.*} |
450 |
450 |
451 ML |
451 theorem M_axioms_axioms_L: "M_axioms_axioms(L)" |
452 {* |
452 apply (rule M_axioms_axioms.intro) |
453 val Inter_separation = thm "Inter_separation"; |
453 apply (assumption | rule |
454 val cartprod_separation = thm "cartprod_separation"; |
454 Inter_separation cartprod_separation image_separation |
455 val image_separation = thm "image_separation"; |
455 converse_separation restrict_separation |
456 val converse_separation = thm "converse_separation"; |
456 comp_separation pred_separation Memrel_separation |
457 val restrict_separation = thm "restrict_separation"; |
457 funspace_succ_replacement well_ord_iso_separation |
458 val comp_separation = thm "comp_separation"; |
458 obase_separation obase_equals_separation |
459 val pred_separation = thm "pred_separation"; |
459 omap_replacement is_recfun_separation)+ |
460 val Memrel_separation = thm "Memrel_separation"; |
460 done |
461 val funspace_succ_replacement = thm "funspace_succ_replacement"; |
461 |
462 val well_ord_iso_separation = thm "well_ord_iso_separation"; |
462 theorem M_axioms_L: "PROP M_axioms(L)" |
463 val obase_separation = thm "obase_separation"; |
463 apply (rule M_axioms.intro) |
464 val obase_equals_separation = thm "obase_equals_separation"; |
464 apply (rule M_triv_axioms_L) |
465 val omap_replacement = thm "omap_replacement"; |
465 apply (rule M_axioms_axioms_L) |
466 val is_recfun_separation = thm "is_recfun_separation"; |
466 done |
467 |
467 |
468 val m_axioms = |
468 lemmas cartprod_iff = M_axioms.cartprod_iff [OF M_axioms_L] |
469 [Inter_separation, cartprod_separation, image_separation, |
469 and cartprod_closed = M_axioms.cartprod_closed [OF M_axioms_L] |
470 converse_separation, restrict_separation, comp_separation, |
470 and sum_closed = M_axioms.sum_closed [OF M_axioms_L] |
471 pred_separation, Memrel_separation, funspace_succ_replacement, |
471 and M_converse_iff = M_axioms.M_converse_iff [OF M_axioms_L] |
472 well_ord_iso_separation, obase_separation, |
472 and converse_closed = M_axioms.converse_closed [OF M_axioms_L] |
473 obase_equals_separation, omap_replacement, is_recfun_separation] |
473 and converse_abs = M_axioms.converse_abs [OF M_axioms_L] |
474 |
474 and image_closed = M_axioms.image_closed [OF M_axioms_L] |
475 fun axioms_L th = |
475 and vimage_abs = M_axioms.vimage_abs [OF M_axioms_L] |
476 kill_flex_triv_prems (m_axioms MRS (triv_axioms_L th)); |
476 and vimage_closed = M_axioms.vimage_closed [OF M_axioms_L] |
477 |
477 and domain_abs = M_axioms.domain_abs [OF M_axioms_L] |
478 bind_thm ("cartprod_iff", axioms_L (thm "M_axioms.cartprod_iff")); |
478 and domain_closed = M_axioms.domain_closed [OF M_axioms_L] |
479 bind_thm ("cartprod_closed", axioms_L (thm "M_axioms.cartprod_closed")); |
479 and range_abs = M_axioms.range_abs [OF M_axioms_L] |
480 bind_thm ("sum_closed", axioms_L (thm "M_axioms.sum_closed")); |
480 and range_closed = M_axioms.range_closed [OF M_axioms_L] |
481 bind_thm ("M_converse_iff", axioms_L (thm "M_axioms.M_converse_iff")); |
481 and field_abs = M_axioms.field_abs [OF M_axioms_L] |
482 bind_thm ("converse_closed", axioms_L (thm "M_axioms.converse_closed")); |
482 and field_closed = M_axioms.field_closed [OF M_axioms_L] |
483 bind_thm ("converse_abs", axioms_L (thm "M_axioms.converse_abs")); |
483 and relation_abs = M_axioms.relation_abs [OF M_axioms_L] |
484 bind_thm ("image_closed", axioms_L (thm "M_axioms.image_closed")); |
484 and function_abs = M_axioms.function_abs [OF M_axioms_L] |
485 bind_thm ("vimage_abs", axioms_L (thm "M_axioms.vimage_abs")); |
485 and apply_closed = M_axioms.apply_closed [OF M_axioms_L] |
486 bind_thm ("vimage_closed", axioms_L (thm "M_axioms.vimage_closed")); |
486 and apply_abs = M_axioms.apply_abs [OF M_axioms_L] |
487 bind_thm ("domain_abs", axioms_L (thm "M_axioms.domain_abs")); |
487 and typed_function_abs = M_axioms.typed_function_abs [OF M_axioms_L] |
488 bind_thm ("domain_closed", axioms_L (thm "M_axioms.domain_closed")); |
488 and injection_abs = M_axioms.injection_abs [OF M_axioms_L] |
489 bind_thm ("range_abs", axioms_L (thm "M_axioms.range_abs")); |
489 and surjection_abs = M_axioms.surjection_abs [OF M_axioms_L] |
490 bind_thm ("range_closed", axioms_L (thm "M_axioms.range_closed")); |
490 and bijection_abs = M_axioms.bijection_abs [OF M_axioms_L] |
491 bind_thm ("field_abs", axioms_L (thm "M_axioms.field_abs")); |
491 and M_comp_iff = M_axioms.M_comp_iff [OF M_axioms_L] |
492 bind_thm ("field_closed", axioms_L (thm "M_axioms.field_closed")); |
492 and comp_closed = M_axioms.comp_closed [OF M_axioms_L] |
493 bind_thm ("relation_abs", axioms_L (thm "M_axioms.relation_abs")); |
493 and composition_abs = M_axioms.composition_abs [OF M_axioms_L] |
494 bind_thm ("function_abs", axioms_L (thm "M_axioms.function_abs")); |
494 and restriction_is_function = M_axioms.restriction_is_function [OF M_axioms_L] |
495 bind_thm ("apply_closed", axioms_L (thm "M_axioms.apply_closed")); |
495 and restriction_abs = M_axioms.restriction_abs [OF M_axioms_L] |
496 bind_thm ("apply_abs", axioms_L (thm "M_axioms.apply_abs")); |
496 and M_restrict_iff = M_axioms.M_restrict_iff [OF M_axioms_L] |
497 bind_thm ("typed_function_abs", axioms_L (thm "M_axioms.typed_function_abs")); |
497 and restrict_closed = M_axioms.restrict_closed [OF M_axioms_L] |
498 bind_thm ("injection_abs", axioms_L (thm "M_axioms.injection_abs")); |
498 and Inter_abs = M_axioms.Inter_abs [OF M_axioms_L] |
499 bind_thm ("surjection_abs", axioms_L (thm "M_axioms.surjection_abs")); |
499 and Inter_closed = M_axioms.Inter_closed [OF M_axioms_L] |
500 bind_thm ("bijection_abs", axioms_L (thm "M_axioms.bijection_abs")); |
500 and Int_closed = M_axioms.Int_closed [OF M_axioms_L] |
501 bind_thm ("M_comp_iff", axioms_L (thm "M_axioms.M_comp_iff")); |
501 and finite_fun_closed = M_axioms.finite_fun_closed [OF M_axioms_L] |
502 bind_thm ("comp_closed", axioms_L (thm "M_axioms.comp_closed")); |
502 and is_funspace_abs = M_axioms.is_funspace_abs [OF M_axioms_L] |
503 bind_thm ("composition_abs", axioms_L (thm "M_axioms.composition_abs")); |
503 and succ_fun_eq2 = M_axioms.succ_fun_eq2 [OF M_axioms_L] |
504 bind_thm ("restriction_is_function", axioms_L (thm "M_axioms.restriction_is_function")); |
504 and funspace_succ = M_axioms.funspace_succ [OF M_axioms_L] |
505 bind_thm ("restriction_abs", axioms_L (thm "M_axioms.restriction_abs")); |
505 and finite_funspace_closed = M_axioms.finite_funspace_closed [OF M_axioms_L] |
506 bind_thm ("M_restrict_iff", axioms_L (thm "M_axioms.M_restrict_iff")); |
506 |
507 bind_thm ("restrict_closed", axioms_L (thm "M_axioms.restrict_closed")); |
507 lemmas is_recfun_equal = M_axioms.is_recfun_equal [OF M_axioms_L] |
508 bind_thm ("Inter_abs", axioms_L (thm "M_axioms.Inter_abs")); |
508 and is_recfun_cut = M_axioms.is_recfun_cut [OF M_axioms_L] |
509 bind_thm ("Inter_closed", axioms_L (thm "M_axioms.Inter_closed")); |
509 and is_recfun_functional = M_axioms.is_recfun_functional [OF M_axioms_L] |
510 bind_thm ("Int_closed", axioms_L (thm "M_axioms.Int_closed")); |
510 and is_recfun_relativize = M_axioms.is_recfun_relativize [OF M_axioms_L] |
511 bind_thm ("finite_fun_closed", axioms_L (thm "M_axioms.finite_fun_closed")); |
511 and is_recfun_restrict = M_axioms.is_recfun_restrict [OF M_axioms_L] |
512 bind_thm ("is_funspace_abs", axioms_L (thm "M_axioms.is_funspace_abs")); |
512 and univalent_is_recfun = M_axioms.univalent_is_recfun [OF M_axioms_L] |
513 bind_thm ("succ_fun_eq2", axioms_L (thm "M_axioms.succ_fun_eq2")); |
513 and exists_is_recfun_indstep = M_axioms.exists_is_recfun_indstep [OF M_axioms_L] |
514 bind_thm ("funspace_succ", axioms_L (thm "M_axioms.funspace_succ")); |
514 and wellfounded_exists_is_recfun = M_axioms.wellfounded_exists_is_recfun [OF M_axioms_L] |
515 bind_thm ("finite_funspace_closed", axioms_L (thm "M_axioms.finite_funspace_closed")); |
515 and wf_exists_is_recfun = M_axioms.wf_exists_is_recfun [OF M_axioms_L] |
516 *} |
516 and is_recfun_abs = M_axioms.is_recfun_abs [OF M_axioms_L] |
517 |
517 and irreflexive_abs = M_axioms.irreflexive_abs [OF M_axioms_L] |
518 ML |
518 and transitive_rel_abs = M_axioms.transitive_rel_abs [OF M_axioms_L] |
519 {* |
519 and linear_rel_abs = M_axioms.linear_rel_abs [OF M_axioms_L] |
520 bind_thm ("is_recfun_equal", axioms_L (thm "M_axioms.is_recfun_equal")); |
520 and wellordered_is_trans_on = M_axioms.wellordered_is_trans_on [OF M_axioms_L] |
521 bind_thm ("is_recfun_cut", axioms_L (thm "M_axioms.is_recfun_cut")); |
521 and wellordered_is_linear = M_axioms.wellordered_is_linear [OF M_axioms_L] |
522 bind_thm ("is_recfun_functional", axioms_L (thm "M_axioms.is_recfun_functional")); |
522 and wellordered_is_wellfounded_on = M_axioms.wellordered_is_wellfounded_on [OF M_axioms_L] |
523 bind_thm ("is_recfun_relativize", axioms_L (thm "M_axioms.is_recfun_relativize")); |
523 and wellfounded_imp_wellfounded_on = M_axioms.wellfounded_imp_wellfounded_on [OF M_axioms_L] |
524 bind_thm ("is_recfun_restrict", axioms_L (thm "M_axioms.is_recfun_restrict")); |
524 and wellfounded_on_subset_A = M_axioms.wellfounded_on_subset_A [OF M_axioms_L] |
525 bind_thm ("univalent_is_recfun", axioms_L (thm "M_axioms.univalent_is_recfun")); |
525 and wellfounded_on_iff_wellfounded = M_axioms.wellfounded_on_iff_wellfounded [OF M_axioms_L] |
526 bind_thm ("exists_is_recfun_indstep", axioms_L (thm "M_axioms.exists_is_recfun_indstep")); |
526 and wellfounded_on_imp_wellfounded = M_axioms.wellfounded_on_imp_wellfounded [OF M_axioms_L] |
527 bind_thm ("wellfounded_exists_is_recfun", axioms_L (thm "M_axioms.wellfounded_exists_is_recfun")); |
527 and wellfounded_on_field_imp_wellfounded = M_axioms.wellfounded_on_field_imp_wellfounded [OF M_axioms_L] |
528 bind_thm ("wf_exists_is_recfun", axioms_L (thm "M_axioms.wf_exists_is_recfun")); |
528 and wellfounded_iff_wellfounded_on_field = M_axioms.wellfounded_iff_wellfounded_on_field [OF M_axioms_L] |
529 bind_thm ("is_recfun_abs", axioms_L (thm "M_axioms.is_recfun_abs")); |
529 and wellfounded_induct = M_axioms.wellfounded_induct [OF M_axioms_L] |
530 bind_thm ("irreflexive_abs", axioms_L (thm "M_axioms.irreflexive_abs")); |
530 and wellfounded_on_induct = M_axioms.wellfounded_on_induct [OF M_axioms_L] |
531 bind_thm ("transitive_rel_abs", axioms_L (thm "M_axioms.transitive_rel_abs")); |
531 and wellfounded_on_induct2 = M_axioms.wellfounded_on_induct2 [OF M_axioms_L] |
532 bind_thm ("linear_rel_abs", axioms_L (thm "M_axioms.linear_rel_abs")); |
532 and linear_imp_relativized = M_axioms.linear_imp_relativized [OF M_axioms_L] |
533 bind_thm ("wellordered_is_trans_on", axioms_L (thm "M_axioms.wellordered_is_trans_on")); |
533 and trans_on_imp_relativized = M_axioms.trans_on_imp_relativized [OF M_axioms_L] |
534 bind_thm ("wellordered_is_linear", axioms_L (thm "M_axioms.wellordered_is_linear")); |
534 and wf_on_imp_relativized = M_axioms.wf_on_imp_relativized [OF M_axioms_L] |
535 bind_thm ("wellordered_is_wellfounded_on", axioms_L (thm "M_axioms.wellordered_is_wellfounded_on")); |
535 and wf_imp_relativized = M_axioms.wf_imp_relativized [OF M_axioms_L] |
536 bind_thm ("wellfounded_imp_wellfounded_on", axioms_L (thm "M_axioms.wellfounded_imp_wellfounded_on")); |
536 and well_ord_imp_relativized = M_axioms.well_ord_imp_relativized [OF M_axioms_L] |
537 bind_thm ("wellfounded_on_subset_A", axioms_L (thm "M_axioms.wellfounded_on_subset_A")); |
537 and order_isomorphism_abs = M_axioms.order_isomorphism_abs [OF M_axioms_L] |
538 bind_thm ("wellfounded_on_iff_wellfounded", axioms_L (thm "M_axioms.wellfounded_on_iff_wellfounded")); |
538 and pred_set_abs = M_axioms.pred_set_abs [OF M_axioms_L] |
539 bind_thm ("wellfounded_on_imp_wellfounded", axioms_L (thm "M_axioms.wellfounded_on_imp_wellfounded")); |
539 |
540 bind_thm ("wellfounded_on_field_imp_wellfounded", axioms_L (thm "M_axioms.wellfounded_on_field_imp_wellfounded")); |
540 lemmas pred_closed = M_axioms.pred_closed [OF M_axioms_L] |
541 bind_thm ("wellfounded_iff_wellfounded_on_field", axioms_L (thm "M_axioms.wellfounded_iff_wellfounded_on_field")); |
541 and membership_abs = M_axioms.membership_abs [OF M_axioms_L] |
542 bind_thm ("wellfounded_induct", axioms_L (thm "M_axioms.wellfounded_induct")); |
542 and M_Memrel_iff = M_axioms.M_Memrel_iff [OF M_axioms_L] |
543 bind_thm ("wellfounded_on_induct", axioms_L (thm "M_axioms.wellfounded_on_induct")); |
543 and Memrel_closed = M_axioms.Memrel_closed [OF M_axioms_L] |
544 bind_thm ("wellfounded_on_induct2", axioms_L (thm "M_axioms.wellfounded_on_induct2")); |
544 and wellordered_iso_predD = M_axioms.wellordered_iso_predD [OF M_axioms_L] |
545 bind_thm ("linear_imp_relativized", axioms_L (thm "M_axioms.linear_imp_relativized")); |
545 and wellordered_iso_pred_eq = M_axioms.wellordered_iso_pred_eq [OF M_axioms_L] |
546 bind_thm ("trans_on_imp_relativized", axioms_L (thm "M_axioms.trans_on_imp_relativized")); |
546 and wellfounded_on_asym = M_axioms.wellfounded_on_asym [OF M_axioms_L] |
547 bind_thm ("wf_on_imp_relativized", axioms_L (thm "M_axioms.wf_on_imp_relativized")); |
547 and wellordered_asym = M_axioms.wellordered_asym [OF M_axioms_L] |
548 bind_thm ("wf_imp_relativized", axioms_L (thm "M_axioms.wf_imp_relativized")); |
548 and ord_iso_pred_imp_lt = M_axioms.ord_iso_pred_imp_lt [OF M_axioms_L] |
549 bind_thm ("well_ord_imp_relativized", axioms_L (thm "M_axioms.well_ord_imp_relativized")); |
549 and obase_iff = M_axioms.obase_iff [OF M_axioms_L] |
550 bind_thm ("order_isomorphism_abs", axioms_L (thm "M_axioms.order_isomorphism_abs")); |
550 and omap_iff = M_axioms.omap_iff [OF M_axioms_L] |
551 bind_thm ("pred_set_abs", axioms_L (thm "M_axioms.pred_set_abs")); |
551 and omap_unique = M_axioms.omap_unique [OF M_axioms_L] |
552 *} |
552 and omap_yields_Ord = M_axioms.omap_yields_Ord [OF M_axioms_L] |
553 |
553 and otype_iff = M_axioms.otype_iff [OF M_axioms_L] |
554 ML |
554 and otype_eq_range = M_axioms.otype_eq_range [OF M_axioms_L] |
555 {* |
555 and Ord_otype = M_axioms.Ord_otype [OF M_axioms_L] |
556 bind_thm ("pred_closed", axioms_L (thm "M_axioms.pred_closed")); |
556 and domain_omap = M_axioms.domain_omap [OF M_axioms_L] |
557 bind_thm ("membership_abs", axioms_L (thm "M_axioms.membership_abs")); |
557 and omap_subset = M_axioms.omap_subset [OF M_axioms_L] |
558 bind_thm ("M_Memrel_iff", axioms_L (thm "M_axioms.M_Memrel_iff")); |
558 and omap_funtype = M_axioms.omap_funtype [OF M_axioms_L] |
559 bind_thm ("Memrel_closed", axioms_L (thm "M_axioms.Memrel_closed")); |
559 and wellordered_omap_bij = M_axioms.wellordered_omap_bij [OF M_axioms_L] |
560 bind_thm ("wellordered_iso_predD", axioms_L (thm "M_axioms.wellordered_iso_predD")); |
560 and omap_ord_iso = M_axioms.omap_ord_iso [OF M_axioms_L] |
561 bind_thm ("wellordered_iso_pred_eq", axioms_L (thm "M_axioms.wellordered_iso_pred_eq")); |
561 and Ord_omap_image_pred = M_axioms.Ord_omap_image_pred [OF M_axioms_L] |
562 bind_thm ("wellfounded_on_asym", axioms_L (thm "M_axioms.wellfounded_on_asym")); |
562 and restrict_omap_ord_iso = M_axioms.restrict_omap_ord_iso [OF M_axioms_L] |
563 bind_thm ("wellordered_asym", axioms_L (thm "M_axioms.wellordered_asym")); |
563 and obase_equals = M_axioms.obase_equals [OF M_axioms_L] |
564 bind_thm ("ord_iso_pred_imp_lt", axioms_L (thm "M_axioms.ord_iso_pred_imp_lt")); |
564 and omap_ord_iso_otype = M_axioms.omap_ord_iso_otype [OF M_axioms_L] |
565 bind_thm ("obase_iff", axioms_L (thm "M_axioms.obase_iff")); |
565 and obase_exists = M_axioms.obase_exists [OF M_axioms_L] |
566 bind_thm ("omap_iff", axioms_L (thm "M_axioms.omap_iff")); |
566 and omap_exists = M_axioms.omap_exists [OF M_axioms_L] |
567 bind_thm ("omap_unique", axioms_L (thm "M_axioms.omap_unique")); |
567 and otype_exists = M_axioms.otype_exists [OF M_axioms_L] |
568 bind_thm ("omap_yields_Ord", axioms_L (thm "M_axioms.omap_yields_Ord")); |
568 and omap_ord_iso_otype' = M_axioms.omap_ord_iso_otype' [OF M_axioms_L] |
569 bind_thm ("otype_iff", axioms_L (thm "M_axioms.otype_iff")); |
569 and ordertype_exists = M_axioms.ordertype_exists [OF M_axioms_L] |
570 bind_thm ("otype_eq_range", axioms_L (thm "M_axioms.otype_eq_range")); |
570 and relativized_imp_well_ord = M_axioms.relativized_imp_well_ord [OF M_axioms_L] |
571 bind_thm ("Ord_otype", axioms_L (thm "M_axioms.Ord_otype")); |
571 and well_ord_abs = M_axioms.well_ord_abs [OF M_axioms_L] |
572 bind_thm ("domain_omap", axioms_L (thm "M_axioms.domain_omap")); |
572 |
573 bind_thm ("omap_subset", axioms_L (thm "M_axioms.omap_subset")); |
|
574 bind_thm ("omap_funtype", axioms_L (thm "M_axioms.omap_funtype")); |
|
575 bind_thm ("wellordered_omap_bij", axioms_L (thm "M_axioms.wellordered_omap_bij")); |
|
576 bind_thm ("omap_ord_iso", axioms_L (thm "M_axioms.omap_ord_iso")); |
|
577 bind_thm ("Ord_omap_image_pred", axioms_L (thm "M_axioms.Ord_omap_image_pred")); |
|
578 bind_thm ("restrict_omap_ord_iso", axioms_L (thm "M_axioms.restrict_omap_ord_iso")); |
|
579 bind_thm ("obase_equals", axioms_L (thm "M_axioms.obase_equals")); |
|
580 bind_thm ("omap_ord_iso_otype", axioms_L (thm "M_axioms.omap_ord_iso_otype")); |
|
581 bind_thm ("obase_exists", axioms_L (thm "M_axioms.obase_exists")); |
|
582 bind_thm ("omap_exists", axioms_L (thm "M_axioms.omap_exists")); |
|
583 bind_thm ("otype_exists", axioms_L (thm "M_axioms.otype_exists")); |
|
584 bind_thm ("omap_ord_iso_otype", axioms_L (thm "M_axioms.omap_ord_iso_otype")); |
|
585 bind_thm ("ordertype_exists", axioms_L (thm "M_axioms.ordertype_exists")); |
|
586 bind_thm ("relativized_imp_well_ord", axioms_L (thm "M_axioms.relativized_imp_well_ord")); |
|
587 bind_thm ("well_ord_abs", axioms_L (thm "M_axioms.well_ord_abs")); |
|
588 *} |
|
589 |
573 |
590 declare cartprod_closed [intro,simp] |
574 declare cartprod_closed [intro,simp] |
591 declare sum_closed [intro,simp] |
575 declare sum_closed [intro,simp] |
592 declare converse_closed [intro,simp] |
576 declare converse_closed [intro,simp] |
593 declare converse_abs [simp] |
577 declare converse_abs [simp] |