src/ZF/Constructible/L_axioms.thy
changeset 13269 3ba9be497c33
parent 13268 240509babf00
child 13291 a73ab154f75c
     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Mon Jul 01 18:16:18 2002 +0200
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Tue Jul 02 13:28:08 2002 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  header {* The class L satisfies the axioms of ZF*}
     1.5  
     1.6 -theory L_axioms = Formula + Relative:
     1.7 +theory L_axioms = Formula + Relative + Reflection:
     1.8  
     1.9  
    1.10  text {* The class L satisfies the premises of locale @{text M_axioms} *}
    1.11 @@ -72,57 +72,57 @@
    1.12  (*
    1.13  
    1.14    and Inter_separation:
    1.15 -     "L(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. L(y) --> x\<in>y)"
    1.16 +     "L(A) ==> separation(L, \<lambda>x. \<forall>y\<in>A. L(y) --> x\<in>y)"
    1.17    and cartprod_separation:
    1.18       "[| L(A); L(B) |] 
    1.19 -      ==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. L(x) & L(y) & pair(M,x,y,z))"
    1.20 +      ==> separation(L, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. L(x) & L(y) & pair(L,x,y,z))"
    1.21    and image_separation:
    1.22       "[| L(A); L(r) |] 
    1.23 -      ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & (\<exists>x\<in>A. L(x) & pair(M,x,y,p)))"
    1.24 +      ==> separation(L, \<lambda>y. \<exists>p\<in>r. L(p) & (\<exists>x\<in>A. L(x) & pair(L,x,y,p)))"
    1.25    and vimage_separation:
    1.26       "[| L(A); L(r) |] 
    1.27 -      ==> separation(M, \<lambda>x. \<exists>p\<in>r. L(p) & (\<exists>y\<in>A. L(x) & pair(M,x,y,p)))"
    1.28 +      ==> separation(L, \<lambda>x. \<exists>p\<in>r. L(p) & (\<exists>y\<in>A. L(x) & pair(L,x,y,p)))"
    1.29    and converse_separation:
    1.30 -     "L(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. L(p) & (\<exists>x y. L(x) & L(y) & 
    1.31 -				     pair(M,x,y,p) & pair(M,y,x,z)))"
    1.32 +     "L(r) ==> separation(L, \<lambda>z. \<exists>p\<in>r. L(p) & (\<exists>x y. L(x) & L(y) & 
    1.33 +				     pair(L,x,y,p) & pair(L,y,x,z)))"
    1.34    and restrict_separation:
    1.35       "L(A) 
    1.36 -      ==> separation(M, \<lambda>z. \<exists>x\<in>A. L(x) & (\<exists>y. L(y) & pair(M,x,y,z)))"
    1.37 +      ==> separation(L, \<lambda>z. \<exists>x\<in>A. L(x) & (\<exists>y. L(y) & pair(L,x,y,z)))"
    1.38    and comp_separation:
    1.39       "[| L(r); L(s) |]
    1.40 -      ==> separation(M, \<lambda>xz. \<exists>x y z. L(x) & L(y) & L(z) &
    1.41 +      ==> separation(L, \<lambda>xz. \<exists>x y z. L(x) & L(y) & L(z) &
    1.42  			   (\<exists>xy\<in>s. \<exists>yz\<in>r. L(xy) & L(yz) & 
    1.43 -		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz)))"
    1.44 +		  pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz)))"
    1.45    and pred_separation:
    1.46 -     "[| L(r); L(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & pair(M,y,x,p))"
    1.47 +     "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p\<in>r. L(p) & pair(L,y,x,p))"
    1.48    and Memrel_separation:
    1.49 -     "separation(M, \<lambda>z. \<exists>x y. L(x) & L(y) & pair(M,x,y,z) \<and> x \<in> y)"
    1.50 +     "separation(L, \<lambda>z. \<exists>x y. L(x) & L(y) & pair(L,x,y,z) \<and> x \<in> y)"
    1.51    and obase_separation:
    1.52       --{*part of the order type formalization*}
    1.53       "[| L(A); L(r) |] 
    1.54 -      ==> separation(M, \<lambda>a. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) & 
    1.55 -	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
    1.56 -	     order_isomorphism(M,par,r,x,mx,g))"
    1.57 +      ==> separation(L, \<lambda>a. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) & 
    1.58 +	     ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
    1.59 +	     order_isomorphism(L,par,r,x,mx,g))"
    1.60    and well_ord_iso_separation:
    1.61       "[| L(A); L(f); L(r) |] 
    1.62 -      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. L(y) \<and> (\<exists>p. L(p) \<and> 
    1.63 -		     fun_apply(M,f,x,y) \<and> pair(M,y,x,p) \<and> p \<in> r)))"
    1.64 +      ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y. L(y) \<and> (\<exists>p. L(p) \<and> 
    1.65 +		     fun_apply(L,f,x,y) \<and> pair(L,y,x,p) \<and> p \<in> r)))"
    1.66    and obase_equals_separation:
    1.67       "[| L(A); L(r) |] 
    1.68        ==> separation
    1.69 -      (M, \<lambda>x. x\<in>A --> ~(\<exists>y. L(y) & (\<exists>g. L(g) &
    1.70 -	      ordinal(M,y) & (\<exists>my pxr. L(my) & L(pxr) &
    1.71 -	      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
    1.72 -	      order_isomorphism(M,pxr,r,y,my,g)))))"
    1.73 +      (L, \<lambda>x. x\<in>A --> ~(\<exists>y. L(y) & (\<exists>g. L(g) &
    1.74 +	      ordinal(L,y) & (\<exists>my pxr. L(my) & L(pxr) &
    1.75 +	      membership(L,y,my) & pred_set(L,A,x,r,pxr) &
    1.76 +	      order_isomorphism(L,pxr,r,y,my,g)))))"
    1.77    and is_recfun_separation:
    1.78       --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
    1.79       "[| L(A); L(f); L(g); L(a); L(b) |] 
    1.80 -     ==> separation(M, \<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.81 +     ==> 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.82    and omap_replacement:
    1.83       "[| L(A); L(r) |] 
    1.84 -      ==> strong_replacement(M,
    1.85 +      ==> strong_replacement(L,
    1.86               \<lambda>a z. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) &
    1.87 -	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
    1.88 -	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
    1.89 +	     ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & 
    1.90 +	     pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
    1.91  
    1.92  *)
    1.93 \ No newline at end of file