more separation instances
authorpaulson
Fri Jul 05 11:47:44 2002 +0200 (2002-07-05)
changeset 1330443ef6c6dd906
parent 13303 60301202f91b
child 13305 f88d0c363582
more separation instances
src/ZF/Constructible/L_axioms.thy
     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Fri Jul 05 11:44:20 2002 +0200
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Fri Jul 05 11:47:44 2002 +0200
     1.3 @@ -619,43 +619,67 @@
     1.4  apply (simp_all add: succ_Un_distrib [symmetric])
     1.5  done
     1.6  
     1.7 +subsubsection{*Separation for Predecessors in an Order*}
     1.8 +
     1.9 +lemma pred_Reflects:
    1.10 +     "L_Reflects(?Cl, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p),
    1.11 +                    \<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(**Lset(i),y,x,p))"
    1.12 +by fast
    1.13 +
    1.14 +lemma pred_separation:
    1.15 +     "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"
    1.16 +apply (rule separation_CollectI) 
    1.17 +apply (rule_tac A="{r,x,z}" in subset_LsetE, blast ) 
    1.18 +apply (rule ReflectsE [OF pred_Reflects], assumption)
    1.19 +apply (drule subset_Lset_ltD, assumption) 
    1.20 +apply (erule reflection_imp_L_separation)
    1.21 +  apply (simp_all add: lt_Ord2, clarify)
    1.22 +apply (rule DPowI2)
    1.23 +apply (rename_tac u) 
    1.24 +apply (rule bex_iff_sats)
    1.25 +apply (rule conj_iff_sats)
    1.26 +apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats) 
    1.27 +apply (blast intro: nth_0 nth_ConsI) 
    1.28 +apply (blast intro: nth_0 nth_ConsI, simp) 
    1.29 +apply (rule pair_iff_sats)
    1.30 +apply (blast intro: nth_0 nth_ConsI) 
    1.31 +apply (blast intro: nth_0 nth_ConsI) 
    1.32 +apply (blast intro: nth_0 nth_ConsI, simp_all)
    1.33 +apply (simp_all add: succ_Un_distrib [symmetric])
    1.34 +done
    1.35 +
    1.36 +
    1.37 +subsubsection{*Separation for the Membership Relation*}
    1.38 +
    1.39 +lemma Memrel_Reflects:
    1.40 +     "L_Reflects(?Cl, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y,
    1.41 +            \<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(**Lset(i),x,y,z) & x \<in> y)"
    1.42 +by fast
    1.43 +
    1.44 +lemma Memrel_separation:
    1.45 +     "separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
    1.46 +apply (rule separation_CollectI) 
    1.47 +apply (rule_tac A="{z}" in subset_LsetE, blast ) 
    1.48 +apply (rule ReflectsE [OF Memrel_Reflects], assumption)
    1.49 +apply (drule subset_Lset_ltD, assumption) 
    1.50 +apply (erule reflection_imp_L_separation)
    1.51 +  apply (simp_all add: lt_Ord2)
    1.52 +apply (rule DPowI2)
    1.53 +apply (rename_tac u) 
    1.54 +apply (rule bex_iff_sats)+
    1.55 +apply (rule conj_iff_sats)
    1.56 +apply (rule_tac env = "[y,x,u]" in pair_iff_sats) 
    1.57 +apply (blast intro: nth_0 nth_ConsI) 
    1.58 +apply (blast intro: nth_0 nth_ConsI) 
    1.59 +apply (blast intro: nth_0 nth_ConsI, simp_all) 
    1.60 +apply (rule mem_iff_sats)
    1.61 +apply (blast intro: nth_0 nth_ConsI) 
    1.62 +apply (blast intro: nth_0 nth_ConsI)
    1.63 +apply (simp_all add: succ_Un_distrib [symmetric])
    1.64 +done
    1.65 +
    1.66 +
    1.67  
    1.68  
    1.69  
    1.70  end
    1.71 -
    1.72 -(*
    1.73 -
    1.74 -  and pred_separation:
    1.75 -     "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p\<in>r. L(p) & pair(L,y,x,p))"
    1.76 -  and Memrel_separation:
    1.77 -     "separation(L, \<lambda>z. \<exists>x y. L(x) & L(y) & pair(L,x,y,z) \<and> x \<in> y)"
    1.78 -  and obase_separation:
    1.79 -     --{*part of the order type formalization*}
    1.80 -     "[| L(A); L(r) |] 
    1.81 -      ==> separation(L, \<lambda>a. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) & 
    1.82 -	     ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
    1.83 -	     order_isomorphism(L,par,r,x,mx,g))"
    1.84 -  and well_ord_iso_separation:
    1.85 -     "[| L(A); L(f); L(r) |] 
    1.86 -      ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y. L(y) \<and> (\<exists>p. L(p) \<and> 
    1.87 -		     fun_apply(L,f,x,y) \<and> pair(L,y,x,p) \<and> p \<in> r)))"
    1.88 -  and obase_equals_separation:
    1.89 -     "[| L(A); L(r) |] 
    1.90 -      ==> separation
    1.91 -      (L, \<lambda>x. x\<in>A --> ~(\<exists>y. L(y) & (\<exists>g. L(g) &
    1.92 -	      ordinal(L,y) & (\<exists>my pxr. L(my) & L(pxr) &
    1.93 -	      membership(L,y,my) & pred_set(L,A,x,r,pxr) &
    1.94 -	      order_isomorphism(L,pxr,r,y,my,g)))))"
    1.95 -  and is_recfun_separation:
    1.96 -     --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
    1.97 -     "[| L(A); L(f); L(g); L(a); L(b) |] 
    1.98 -     ==> separation(L, \<lambda>x. x \<in> A --> \<langle>x,a\<rangle> \<in> r \<and> \<langle>x,b\<rangle> \<in> r \<and> f`x \<noteq> g`x)"
    1.99 -  and omap_replacement:
   1.100 -     "[| L(A); L(r) |] 
   1.101 -      ==> strong_replacement(L,
   1.102 -             \<lambda>a z. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) &
   1.103 -	     ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & 
   1.104 -	     pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
   1.105 -
   1.106 -*)
   1.107 \ No newline at end of file