508 |
508 |
509 text\<open>Relativization of the Operator @{term Lset}\<close> |
509 text\<open>Relativization of the Operator @{term Lset}\<close> |
510 |
510 |
511 definition |
511 definition |
512 is_Lset :: "[i=>o, i, i] => o" where |
512 is_Lset :: "[i=>o, i, i] => o" where |
513 \<comment>\<open>We can use the term language below because @{term is_Lset} will |
513 \<comment> \<open>We can use the term language below because @{term is_Lset} will |
514 not have to be internalized: it isn't used in any instance of |
514 not have to be internalized: it isn't used in any instance of |
515 separation.\<close> |
515 separation.\<close> |
516 "is_Lset(M,a,z) == is_transrec(M, %x f u. u = (\<Union>y\<in>x. DPow'(f`y)), a, z)" |
516 "is_Lset(M,a,z) == is_transrec(M, %x f u. u = (\<Union>y\<in>x. DPow'(f`y)), a, z)" |
517 |
517 |
518 lemma (in M_Lset) Lset_abs: |
518 lemma (in M_Lset) Lset_abs: |
568 is_Replace (##Lset(i), x, \<lambda>y z. |
568 is_Replace (##Lset(i), x, \<lambda>y z. |
569 \<exists>gy \<in> Lset(i). y \<in> x & fun_apply(##Lset(i),f,y,gy) & |
569 \<exists>gy \<in> Lset(i). y \<in> x & fun_apply(##Lset(i),f,y,gy) & |
570 is_DPow'(##Lset(i),gy,z), r) & |
570 is_DPow'(##Lset(i),gy,z), r) & |
571 big_union(##Lset(i),r,u), mr, v, y))]" |
571 big_union(##Lset(i),r,u), mr, v, y))]" |
572 apply (simp only: rex_setclass_is_bex [symmetric]) |
572 apply (simp only: rex_setclass_is_bex [symmetric]) |
573 \<comment>\<open>Convert \<open>\<exists>y\<in>Lset(i)\<close> to \<open>\<exists>y[##Lset(i)]\<close> within the body |
573 \<comment> \<open>Convert \<open>\<exists>y\<in>Lset(i)\<close> to \<open>\<exists>y[##Lset(i)]\<close> within the body |
574 of the @{term is_wfrec} application.\<close> |
574 of the @{term is_wfrec} application.\<close> |
575 apply (intro FOL_reflections function_reflections |
575 apply (intro FOL_reflections function_reflections |
576 is_wfrec_reflection Replace_reflection DPow'_reflection) |
576 is_wfrec_reflection Replace_reflection DPow'_reflection) |
577 done |
577 done |
578 |
578 |