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
```