src/ZF/Constructible/Separation.thy
author wenzelm
Mon Jul 29 00:57:16 2002 +0200 (2002-07-29)
changeset 13428 99e52e78eb65
parent 13385 31df66ca0780
child 13429 2232810416fc
permissions -rw-r--r--
eliminate open locales and special ML code;
     1 header{*Early Instances of Separation and Strong Replacement*}
     2 
     3 theory Separation = L_axioms + WF_absolute:
     4 
     5 text{*This theory proves all instances needed for locale @{text "M_axioms"}*}
     6 
     7 text{*Helps us solve for de Bruijn indices!*}
     8 lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x"
     9 by simp
    10 
    11 lemmas nth_rules = nth_0 nth_ConsI nat_0I nat_succI
    12 lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats function_iff_sats
    13                    fun_plus_iff_sats
    14 
    15 lemma Collect_conj_in_DPow:
    16      "[| {x\<in>A. P(x)} \<in> DPow(A);  {x\<in>A. Q(x)} \<in> DPow(A) |]
    17       ==> {x\<in>A. P(x) & Q(x)} \<in> DPow(A)"
    18 by (simp add: Int_in_DPow Collect_Int_Collect_eq [symmetric])
    19 
    20 lemma Collect_conj_in_DPow_Lset:
    21      "[|z \<in> Lset(j); {x \<in> Lset(j). P(x)} \<in> DPow(Lset(j))|]
    22       ==> {x \<in> Lset(j). x \<in> z & P(x)} \<in> DPow(Lset(j))"
    23 apply (frule mem_Lset_imp_subset_Lset)
    24 apply (simp add: Collect_conj_in_DPow Collect_mem_eq
    25                  subset_Int_iff2 elem_subset_in_DPow)
    26 done
    27 
    28 lemma separation_CollectI:
    29      "(\<And>z. L(z) ==> L({x \<in> z . P(x)})) ==> separation(L, \<lambda>x. P(x))"
    30 apply (unfold separation_def, clarify)
    31 apply (rule_tac x="{x\<in>z. P(x)}" in rexI)
    32 apply simp_all
    33 done
    34 
    35 text{*Reduces the original comprehension to the reflected one*}
    36 lemma reflection_imp_L_separation:
    37       "[| \<forall>x\<in>Lset(j). P(x) <-> Q(x);
    38           {x \<in> Lset(j) . Q(x)} \<in> DPow(Lset(j));
    39           Ord(j);  z \<in> Lset(j)|] ==> L({x \<in> z . P(x)})"
    40 apply (rule_tac i = "succ(j)" in L_I)
    41  prefer 2 apply simp
    42 apply (subgoal_tac "{x \<in> z. P(x)} = {x \<in> Lset(j). x \<in> z & (Q(x))}")
    43  prefer 2
    44  apply (blast dest: mem_Lset_imp_subset_Lset)
    45 apply (simp add: Lset_succ Collect_conj_in_DPow_Lset)
    46 done
    47 
    48 
    49 subsection{*Separation for Intersection*}
    50 
    51 lemma Inter_Reflects:
    52      "REFLECTS[\<lambda>x. \<forall>y[L]. y\<in>A --> x \<in> y,
    53                \<lambda>i x. \<forall>y\<in>Lset(i). y\<in>A --> x \<in> y]"
    54 by (intro FOL_reflections)
    55 
    56 lemma Inter_separation:
    57      "L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A --> x\<in>y)"
    58 apply (rule separation_CollectI)
    59 apply (rule_tac A="{A,z}" in subset_LsetE, blast )
    60 apply (rule ReflectsE [OF Inter_Reflects], assumption)
    61 apply (drule subset_Lset_ltD, assumption)
    62 apply (erule reflection_imp_L_separation)
    63   apply (simp_all add: lt_Ord2, clarify)
    64 apply (rule DPow_LsetI)
    65 apply (rule ball_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)
    68 apply (rule_tac i=0 and j=2 in mem_iff_sats)
    69 apply (simp_all add: succ_Un_distrib [symmetric])
    70 done
    71 
    72 subsection{*Separation for Cartesian Product*}
    73 
    74 lemma cartprod_Reflects:
    75      "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)),
    76                 \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B &
    77                                    pair(**Lset(i),x,y,z))]"
    78 by (intro FOL_reflections function_reflections)
    79 
    80 lemma cartprod_separation:
    81      "[| L(A); L(B) |]
    82       ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)))"
    83 apply (rule separation_CollectI)
    84 apply (rule_tac A="{A,B,z}" in subset_LsetE, blast )
    85 apply (rule ReflectsE [OF cartprod_Reflects], assumption)
    86 apply (drule subset_Lset_ltD, assumption)
    87 apply (erule reflection_imp_L_separation)
    88   apply (simp_all add: lt_Ord2, clarify)
    89 apply (rule DPow_LsetI)
    90 apply (rename_tac u)
    91 apply (rule bex_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)
    94 apply (rule sep_rules | simp)+
    95 done
    96 
    97 subsection{*Separation for Image*}
    98 
    99 lemma image_Reflects:
   100      "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)),
   101            \<lambda>i y. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). x\<in>A & pair(**Lset(i),x,y,p))]"
   102 by (intro FOL_reflections function_reflections)
   103 
   104 lemma image_separation:
   105      "[| L(A); L(r) |]
   106       ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)))"
   107 apply (rule separation_CollectI)
   108 apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
   109 apply (rule ReflectsE [OF image_Reflects], assumption)
   110 apply (drule subset_Lset_ltD, assumption)
   111 apply (erule reflection_imp_L_separation)
   112   apply (simp_all add: lt_Ord2, clarify)
   113 apply (rule DPow_LsetI)
   114 apply (rule bex_iff_sats)
   115 apply (rule conj_iff_sats)
   116 apply (rule_tac env="[p,y,A,r]" in mem_iff_sats)
   117 apply (rule sep_rules | simp)+
   118 done
   119 
   120 
   121 subsection{*Separation for Converse*}
   122 
   123 lemma converse_Reflects:
   124   "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)),
   125      \<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i).
   126                      pair(**Lset(i),x,y,p) & pair(**Lset(i),y,x,z))]"
   127 by (intro FOL_reflections function_reflections)
   128 
   129 lemma converse_separation:
   130      "L(r) ==> separation(L,
   131          \<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)))"
   132 apply (rule separation_CollectI)
   133 apply (rule_tac A="{r,z}" in subset_LsetE, blast )
   134 apply (rule ReflectsE [OF converse_Reflects], assumption)
   135 apply (drule subset_Lset_ltD, assumption)
   136 apply (erule reflection_imp_L_separation)
   137   apply (simp_all add: lt_Ord2, clarify)
   138 apply (rule DPow_LsetI)
   139 apply (rename_tac u)
   140 apply (rule bex_iff_sats)
   141 apply (rule conj_iff_sats)
   142 apply (rule_tac i=0 and j=2 and env="[p,u,r]" in mem_iff_sats, simp_all)
   143 apply (rule sep_rules | simp)+
   144 done
   145 
   146 
   147 subsection{*Separation for Restriction*}
   148 
   149 lemma restrict_Reflects:
   150      "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)),
   151         \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(**Lset(i),x,y,z))]"
   152 by (intro FOL_reflections function_reflections)
   153 
   154 lemma restrict_separation:
   155    "L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))"
   156 apply (rule separation_CollectI)
   157 apply (rule_tac A="{A,z}" in subset_LsetE, blast )
   158 apply (rule ReflectsE [OF restrict_Reflects], assumption)
   159 apply (drule subset_Lset_ltD, assumption)
   160 apply (erule reflection_imp_L_separation)
   161   apply (simp_all add: lt_Ord2, clarify)
   162 apply (rule DPow_LsetI)
   163 apply (rename_tac u)
   164 apply (rule bex_iff_sats)
   165 apply (rule conj_iff_sats)
   166 apply (rule_tac i=0 and j=2 and env="[x,u,A]" in mem_iff_sats, simp_all)
   167 apply (rule sep_rules | simp)+
   168 done
   169 
   170 
   171 subsection{*Separation for Composition*}
   172 
   173 lemma comp_Reflects:
   174      "REFLECTS[\<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
   175                   pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
   176                   xy\<in>s & yz\<in>r,
   177         \<lambda>i xz. \<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). \<exists>z\<in>Lset(i). \<exists>xy\<in>Lset(i). \<exists>yz\<in>Lset(i).
   178                   pair(**Lset(i),x,z,xz) & pair(**Lset(i),x,y,xy) &
   179                   pair(**Lset(i),y,z,yz) & xy\<in>s & yz\<in>r]"
   180 by (intro FOL_reflections function_reflections)
   181 
   182 lemma comp_separation:
   183      "[| L(r); L(s) |]
   184       ==> separation(L, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
   185                   pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
   186                   xy\<in>s & yz\<in>r)"
   187 apply (rule separation_CollectI)
   188 apply (rule_tac A="{r,s,z}" in subset_LsetE, blast )
   189 apply (rule ReflectsE [OF comp_Reflects], assumption)
   190 apply (drule subset_Lset_ltD, assumption)
   191 apply (erule reflection_imp_L_separation)
   192   apply (simp_all add: lt_Ord2, clarify)
   193 apply (rule DPow_LsetI)
   194 apply (rename_tac u)
   195 apply (rule bex_iff_sats)+
   196 apply (rename_tac x y z)
   197 apply (rule conj_iff_sats)
   198 apply (rule_tac env="[z,y,x,u,r,s]" in pair_iff_sats)
   199 apply (rule sep_rules | simp)+
   200 done
   201 
   202 subsection{*Separation for Predecessors in an Order*}
   203 
   204 lemma pred_Reflects:
   205      "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p),
   206                     \<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(**Lset(i),y,x,p)]"
   207 by (intro FOL_reflections function_reflections)
   208 
   209 lemma pred_separation:
   210      "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"
   211 apply (rule separation_CollectI)
   212 apply (rule_tac A="{r,x,z}" in subset_LsetE, blast )
   213 apply (rule ReflectsE [OF pred_Reflects], assumption)
   214 apply (drule subset_Lset_ltD, assumption)
   215 apply (erule reflection_imp_L_separation)
   216   apply (simp_all add: lt_Ord2, clarify)
   217 apply (rule DPow_LsetI)
   218 apply (rename_tac u)
   219 apply (rule bex_iff_sats)
   220 apply (rule conj_iff_sats)
   221 apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats)
   222 apply (rule sep_rules | simp)+
   223 done
   224 
   225 
   226 subsection{*Separation for the Membership Relation*}
   227 
   228 lemma Memrel_Reflects:
   229      "REFLECTS[\<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,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)
   232 
   233 lemma Memrel_separation:
   234      "separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
   235 apply (rule separation_CollectI)
   236 apply (rule_tac A="{z}" in subset_LsetE, blast )
   237 apply (rule ReflectsE [OF Memrel_Reflects], assumption)
   238 apply (drule subset_Lset_ltD, assumption)
   239 apply (erule reflection_imp_L_separation)
   240   apply (simp_all add: lt_Ord2)
   241 apply (rule DPow_LsetI)
   242 apply (rename_tac u)
   243 apply (rule bex_iff_sats conj_iff_sats)+
   244 apply (rule_tac env = "[y,x,u]" in pair_iff_sats)
   245 apply (rule sep_rules | simp)+
   246 done
   247 
   248 
   249 subsection{*Replacement for FunSpace*}
   250 
   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].
   253             pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) &
   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).
   256               \<exists>nb \<in> Lset(i). \<exists>cnbf \<in> Lset(i).
   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))]"
   259 by (intro FOL_reflections function_reflections)
   260 
   261 lemma funspace_succ_replacement:
   262      "L(n) ==>
   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) &
   265                 upair(L,cnbf,cnbf,z))"
   266 apply (rule strong_replacementI)
   267 apply (rule rallI)
   268 apply (rule separation_CollectI)
   269 apply (rule_tac A="{n,A,z}" in subset_LsetE, blast )
   270 apply (rule ReflectsE [OF funspace_succ_Reflects], assumption)
   271 apply (drule subset_Lset_ltD, assumption)
   272 apply (erule reflection_imp_L_separation)
   273   apply (simp_all add: lt_Ord2)
   274 apply (rule DPow_LsetI)
   275 apply (rename_tac u)
   276 apply (rule bex_iff_sats)
   277 apply (rule conj_iff_sats)
   278 apply (rule_tac env = "[p,u,n,A]" in mem_iff_sats)
   279 apply (rule sep_rules | simp)+
   280 done
   281 
   282 
   283 subsection{*Separation for Order-Isomorphisms*}
   284 
   285 lemma well_ord_iso_Reflects:
   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),
   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)]"
   290 by (intro FOL_reflections function_reflections)
   291 
   292 lemma well_ord_iso_separation:
   293      "[| L(A); L(f); L(r) |]
   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)))"
   296 apply (rule separation_CollectI)
   297 apply (rule_tac A="{A,f,r,z}" in subset_LsetE, blast )
   298 apply (rule ReflectsE [OF well_ord_iso_Reflects], assumption)
   299 apply (drule subset_Lset_ltD, assumption)
   300 apply (erule reflection_imp_L_separation)
   301   apply (simp_all add: lt_Ord2)
   302 apply (rule DPow_LsetI)
   303 apply (rename_tac u)
   304 apply (rule imp_iff_sats)
   305 apply (rule_tac env = "[u,A,f,r]" in mem_iff_sats)
   306 apply (rule sep_rules | simp)+
   307 done
   308 
   309 
   310 subsection{*Separation for @{term "obase"}*}
   311 
   312 lemma obase_reflects:
   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) &
   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).
   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)]"
   319 by (intro FOL_reflections function_reflections fun_plus_reflections)
   320 
   321 lemma obase_separation:
   322      --{*part of the order type formalization*}
   323      "[| L(A); L(r) |]
   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) &
   326              order_isomorphism(L,par,r,x,mx,g))"
   327 apply (rule separation_CollectI)
   328 apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
   329 apply (rule ReflectsE [OF obase_reflects], assumption)
   330 apply (drule subset_Lset_ltD, assumption)
   331 apply (erule reflection_imp_L_separation)
   332   apply (simp_all add: lt_Ord2)
   333 apply (rule DPow_LsetI)
   334 apply (rename_tac u)
   335 apply (rule bex_iff_sats)
   336 apply (rule conj_iff_sats)
   337 apply (rule_tac env = "[x,u,A,r]" in ordinal_iff_sats)
   338 apply (rule sep_rules | simp)+
   339 done
   340 
   341 
   342 subsection{*Separation for a Theorem about @{term "obase"}*}
   343 
   344 lemma obase_equals_reflects:
   345   "REFLECTS[\<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L].
   346                 ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
   347                 membership(L,y,my) & pred_set(L,A,x,r,pxr) &
   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).
   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) &
   352                 order_isomorphism(**Lset(i),pxr,r,y,my,g)))]"
   353 by (intro FOL_reflections function_reflections fun_plus_reflections)
   354 
   355 
   356 lemma obase_equals_separation:
   357      "[| L(A); L(r) |]
   358       ==> separation (L, \<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L].
   359                               ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
   360                               membership(L,y,my) & pred_set(L,A,x,r,pxr) &
   361                               order_isomorphism(L,pxr,r,y,my,g))))"
   362 apply (rule separation_CollectI)
   363 apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
   364 apply (rule ReflectsE [OF obase_equals_reflects], assumption)
   365 apply (drule subset_Lset_ltD, assumption)
   366 apply (erule reflection_imp_L_separation)
   367   apply (simp_all add: lt_Ord2)
   368 apply (rule DPow_LsetI)
   369 apply (rename_tac u)
   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)
   372 apply (rule sep_rules | simp)+
   373 done
   374 
   375 
   376 subsection{*Replacement for @{term "omap"}*}
   377 
   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].
   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)),
   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).
   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) &
   386          order_isomorphism(**Lset(i),par,r,x,mx,g))]"
   387 by (intro FOL_reflections function_reflections fun_plus_reflections)
   388 
   389 lemma omap_replacement:
   390      "[| L(A); L(r) |]
   391       ==> strong_replacement(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) &
   394              pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
   395 apply (rule strong_replacementI)
   396 apply (rule rallI)
   397 apply (rename_tac B)
   398 apply (rule separation_CollectI)
   399 apply (rule_tac A="{A,B,r,z}" in subset_LsetE, blast )
   400 apply (rule ReflectsE [OF omap_reflects], assumption)
   401 apply (drule subset_Lset_ltD, assumption)
   402 apply (erule reflection_imp_L_separation)
   403   apply (simp_all add: lt_Ord2)
   404 apply (rule DPow_LsetI)
   405 apply (rename_tac u)
   406 apply (rule bex_iff_sats conj_iff_sats)+
   407 apply (rule_tac env = "[a,u,A,B,r]" in mem_iff_sats)
   408 apply (rule sep_rules | simp)+
   409 done
   410 
   411 
   412 subsection{*Separation for a Theorem about @{term "obase"}*}
   413 
   414 lemma is_recfun_reflects:
   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 &
   417                 (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
   418                                    fx \<noteq> gx),
   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 &
   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)]"
   423 by (intro FOL_reflections function_reflections fun_plus_reflections)
   424 
   425 lemma is_recfun_separation:
   426      --{*for well-founded recursion*}
   427      "[| L(r); L(f); L(g); L(a); L(b) |]
   428      ==> separation(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 &
   431                 (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
   432                                    fx \<noteq> gx))"
   433 apply (rule separation_CollectI)
   434 apply (rule_tac A="{r,f,g,a,b,z}" in subset_LsetE, blast )
   435 apply (rule ReflectsE [OF is_recfun_reflects], assumption)
   436 apply (drule subset_Lset_ltD, assumption)
   437 apply (erule reflection_imp_L_separation)
   438   apply (simp_all add: lt_Ord2)
   439 apply (rule DPow_LsetI)
   440 apply (rename_tac u)
   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)
   443 apply (rule sep_rules | simp)+
   444 done
   445 
   446 
   447 subsection{*Instantiating the locale @{text M_axioms}*}
   448 text{*Separation (and Strong Replacement) for basic set-theoretic constructions
   449 such as intersection, Cartesian Product and image.*}
   450 
   451 theorem M_axioms_axioms_L: "M_axioms_axioms(L)"
   452   apply (rule M_axioms_axioms.intro)
   453                apply (assumption | rule
   454                  Inter_separation cartprod_separation image_separation
   455                  converse_separation restrict_separation
   456                  comp_separation pred_separation Memrel_separation
   457                  funspace_succ_replacement well_ord_iso_separation
   458                  obase_separation obase_equals_separation
   459                  omap_replacement is_recfun_separation)+
   460   done
   461   
   462 theorem M_axioms_L: "PROP M_axioms(L)"
   463   apply (rule M_axioms.intro)
   464    apply (rule M_triv_axioms_L)
   465   apply (rule M_axioms_axioms_L)
   466   done
   467 
   468 lemmas cartprod_iff = M_axioms.cartprod_iff [OF M_axioms_L]
   469   and cartprod_closed = M_axioms.cartprod_closed [OF M_axioms_L]
   470   and sum_closed = M_axioms.sum_closed [OF M_axioms_L]
   471   and M_converse_iff = M_axioms.M_converse_iff [OF M_axioms_L]
   472   and converse_closed = M_axioms.converse_closed [OF M_axioms_L]
   473   and converse_abs = M_axioms.converse_abs [OF M_axioms_L]
   474   and image_closed = M_axioms.image_closed [OF M_axioms_L]
   475   and vimage_abs = M_axioms.vimage_abs [OF M_axioms_L]
   476   and vimage_closed = M_axioms.vimage_closed [OF M_axioms_L]
   477   and domain_abs = M_axioms.domain_abs [OF M_axioms_L]
   478   and domain_closed = M_axioms.domain_closed [OF M_axioms_L]
   479   and range_abs = M_axioms.range_abs [OF M_axioms_L]
   480   and range_closed = M_axioms.range_closed [OF M_axioms_L]
   481   and field_abs = M_axioms.field_abs [OF M_axioms_L]
   482   and field_closed = M_axioms.field_closed [OF M_axioms_L]
   483   and relation_abs = M_axioms.relation_abs [OF M_axioms_L]
   484   and function_abs = M_axioms.function_abs [OF M_axioms_L]
   485   and apply_closed = M_axioms.apply_closed [OF M_axioms_L]
   486   and apply_abs = M_axioms.apply_abs [OF M_axioms_L]
   487   and typed_function_abs = M_axioms.typed_function_abs [OF M_axioms_L]
   488   and injection_abs = M_axioms.injection_abs [OF M_axioms_L]
   489   and surjection_abs = M_axioms.surjection_abs [OF M_axioms_L]
   490   and bijection_abs = M_axioms.bijection_abs [OF M_axioms_L]
   491   and M_comp_iff = M_axioms.M_comp_iff [OF M_axioms_L]
   492   and comp_closed = M_axioms.comp_closed [OF M_axioms_L]
   493   and composition_abs = M_axioms.composition_abs [OF M_axioms_L]
   494   and restriction_is_function = M_axioms.restriction_is_function [OF M_axioms_L]
   495   and restriction_abs = M_axioms.restriction_abs [OF M_axioms_L]
   496   and M_restrict_iff = M_axioms.M_restrict_iff [OF M_axioms_L]
   497   and restrict_closed = M_axioms.restrict_closed [OF M_axioms_L]
   498   and Inter_abs = M_axioms.Inter_abs [OF M_axioms_L]
   499   and Inter_closed = M_axioms.Inter_closed [OF M_axioms_L]
   500   and Int_closed = M_axioms.Int_closed [OF M_axioms_L]
   501   and finite_fun_closed = M_axioms.finite_fun_closed [OF M_axioms_L]
   502   and is_funspace_abs = M_axioms.is_funspace_abs [OF M_axioms_L]
   503   and succ_fun_eq2 = M_axioms.succ_fun_eq2 [OF M_axioms_L]
   504   and funspace_succ = M_axioms.funspace_succ [OF M_axioms_L]
   505   and finite_funspace_closed = M_axioms.finite_funspace_closed [OF M_axioms_L]
   506 
   507 lemmas is_recfun_equal = M_axioms.is_recfun_equal [OF M_axioms_L]
   508   and is_recfun_cut = M_axioms.is_recfun_cut [OF M_axioms_L]
   509   and is_recfun_functional = M_axioms.is_recfun_functional [OF M_axioms_L]
   510   and is_recfun_relativize = M_axioms.is_recfun_relativize [OF M_axioms_L]
   511   and is_recfun_restrict = M_axioms.is_recfun_restrict [OF M_axioms_L]
   512   and univalent_is_recfun = M_axioms.univalent_is_recfun [OF M_axioms_L]
   513   and exists_is_recfun_indstep = M_axioms.exists_is_recfun_indstep [OF M_axioms_L]
   514   and wellfounded_exists_is_recfun = M_axioms.wellfounded_exists_is_recfun [OF M_axioms_L]
   515   and wf_exists_is_recfun = M_axioms.wf_exists_is_recfun [OF M_axioms_L]
   516   and is_recfun_abs = M_axioms.is_recfun_abs [OF M_axioms_L]
   517   and irreflexive_abs = M_axioms.irreflexive_abs [OF M_axioms_L]
   518   and transitive_rel_abs = M_axioms.transitive_rel_abs [OF M_axioms_L]
   519   and linear_rel_abs = M_axioms.linear_rel_abs [OF M_axioms_L]
   520   and wellordered_is_trans_on = M_axioms.wellordered_is_trans_on [OF M_axioms_L]
   521   and wellordered_is_linear = M_axioms.wellordered_is_linear [OF M_axioms_L]
   522   and wellordered_is_wellfounded_on = M_axioms.wellordered_is_wellfounded_on [OF M_axioms_L]
   523   and wellfounded_imp_wellfounded_on = M_axioms.wellfounded_imp_wellfounded_on [OF M_axioms_L]
   524   and wellfounded_on_subset_A = M_axioms.wellfounded_on_subset_A [OF M_axioms_L]
   525   and wellfounded_on_iff_wellfounded = M_axioms.wellfounded_on_iff_wellfounded [OF M_axioms_L]
   526   and wellfounded_on_imp_wellfounded = M_axioms.wellfounded_on_imp_wellfounded [OF M_axioms_L]
   527   and wellfounded_on_field_imp_wellfounded = M_axioms.wellfounded_on_field_imp_wellfounded [OF M_axioms_L]
   528   and wellfounded_iff_wellfounded_on_field = M_axioms.wellfounded_iff_wellfounded_on_field [OF M_axioms_L]
   529   and wellfounded_induct = M_axioms.wellfounded_induct [OF M_axioms_L]
   530   and wellfounded_on_induct = M_axioms.wellfounded_on_induct [OF M_axioms_L]
   531   and wellfounded_on_induct2 = M_axioms.wellfounded_on_induct2 [OF M_axioms_L]
   532   and linear_imp_relativized = M_axioms.linear_imp_relativized [OF M_axioms_L]
   533   and trans_on_imp_relativized = M_axioms.trans_on_imp_relativized [OF M_axioms_L]
   534   and wf_on_imp_relativized = M_axioms.wf_on_imp_relativized [OF M_axioms_L]
   535   and wf_imp_relativized = M_axioms.wf_imp_relativized [OF M_axioms_L]
   536   and well_ord_imp_relativized = M_axioms.well_ord_imp_relativized [OF M_axioms_L]
   537   and order_isomorphism_abs = M_axioms.order_isomorphism_abs [OF M_axioms_L]
   538   and pred_set_abs = M_axioms.pred_set_abs [OF M_axioms_L]
   539 
   540 lemmas pred_closed = M_axioms.pred_closed [OF M_axioms_L]
   541   and membership_abs = M_axioms.membership_abs [OF M_axioms_L]
   542   and M_Memrel_iff = M_axioms.M_Memrel_iff [OF M_axioms_L]
   543   and Memrel_closed = M_axioms.Memrel_closed [OF M_axioms_L]
   544   and wellordered_iso_predD = M_axioms.wellordered_iso_predD [OF M_axioms_L]
   545   and wellordered_iso_pred_eq = M_axioms.wellordered_iso_pred_eq [OF M_axioms_L]
   546   and wellfounded_on_asym = M_axioms.wellfounded_on_asym [OF M_axioms_L]
   547   and wellordered_asym = M_axioms.wellordered_asym [OF M_axioms_L]
   548   and ord_iso_pred_imp_lt = M_axioms.ord_iso_pred_imp_lt [OF M_axioms_L]
   549   and obase_iff = M_axioms.obase_iff [OF M_axioms_L]
   550   and omap_iff = M_axioms.omap_iff [OF M_axioms_L]
   551   and omap_unique = M_axioms.omap_unique [OF M_axioms_L]
   552   and omap_yields_Ord = M_axioms.omap_yields_Ord [OF M_axioms_L]
   553   and otype_iff = M_axioms.otype_iff [OF M_axioms_L]
   554   and otype_eq_range = M_axioms.otype_eq_range [OF M_axioms_L]
   555   and Ord_otype = M_axioms.Ord_otype [OF M_axioms_L]
   556   and domain_omap = M_axioms.domain_omap [OF M_axioms_L]
   557   and omap_subset = M_axioms.omap_subset [OF M_axioms_L]
   558   and omap_funtype = M_axioms.omap_funtype [OF M_axioms_L]
   559   and wellordered_omap_bij = M_axioms.wellordered_omap_bij [OF M_axioms_L]
   560   and omap_ord_iso = M_axioms.omap_ord_iso [OF M_axioms_L]
   561   and Ord_omap_image_pred = M_axioms.Ord_omap_image_pred [OF M_axioms_L]
   562   and restrict_omap_ord_iso = M_axioms.restrict_omap_ord_iso [OF M_axioms_L]
   563   and obase_equals = M_axioms.obase_equals [OF M_axioms_L]
   564   and omap_ord_iso_otype = M_axioms.omap_ord_iso_otype [OF M_axioms_L]
   565   and obase_exists = M_axioms.obase_exists [OF M_axioms_L]
   566   and omap_exists = M_axioms.omap_exists [OF M_axioms_L]
   567   and otype_exists = M_axioms.otype_exists [OF M_axioms_L]
   568   and omap_ord_iso_otype' = M_axioms.omap_ord_iso_otype' [OF M_axioms_L]
   569   and ordertype_exists = M_axioms.ordertype_exists [OF M_axioms_L]
   570   and relativized_imp_well_ord = M_axioms.relativized_imp_well_ord [OF M_axioms_L]
   571   and well_ord_abs = M_axioms.well_ord_abs [OF M_axioms_L]
   572 
   573 
   574 declare cartprod_closed [intro,simp]
   575 declare sum_closed [intro,simp]
   576 declare converse_closed [intro,simp]
   577 declare converse_abs [simp]
   578 declare image_closed [intro,simp]
   579 declare vimage_abs [simp]
   580 declare vimage_closed [intro,simp]
   581 declare domain_abs [simp]
   582 declare domain_closed [intro,simp]
   583 declare range_abs [simp]
   584 declare range_closed [intro,simp]
   585 declare field_abs [simp]
   586 declare field_closed [intro,simp]
   587 declare relation_abs [simp]
   588 declare function_abs [simp]
   589 declare apply_closed [intro,simp]
   590 declare typed_function_abs [simp]
   591 declare injection_abs [simp]
   592 declare surjection_abs [simp]
   593 declare bijection_abs [simp]
   594 declare comp_closed [intro,simp]
   595 declare composition_abs [simp]
   596 declare restriction_abs [simp]
   597 declare restrict_closed [intro,simp]
   598 declare Inter_abs [simp]
   599 declare Inter_closed [intro,simp]
   600 declare Int_closed [intro,simp]
   601 declare is_funspace_abs [simp]
   602 declare finite_funspace_closed [intro,simp]
   603 
   604 end