src/ZF/Constructible/L_axioms.thy
changeset 13223 45be08fbdcff
child 13268 240509babf00
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Wed Jun 19 11:48:01 2002 +0200
     1.3 @@ -0,0 +1,129 @@
     1.4 +header {* The class L satisfies the axioms of ZF*}
     1.5 +
     1.6 +theory L_axioms = Formula + Relative:
     1.7 +
     1.8 +
     1.9 +text {* The class L satisfies the premises of locale @{text M_axioms} *}
    1.10 +
    1.11 +lemma transL: "[| y\<in>x; L(x) |] ==> L(y)"
    1.12 +apply (insert Transset_Lset) 
    1.13 +apply (simp add: Transset_def L_def, blast) 
    1.14 +done
    1.15 +
    1.16 +lemma nonempty: "L(0)"
    1.17 +apply (simp add: L_def) 
    1.18 +apply (blast intro: zero_in_Lset) 
    1.19 +done
    1.20 +
    1.21 +lemma upair_ax: "upair_ax(L)"
    1.22 +apply (simp add: upair_ax_def upair_def, clarify)
    1.23 +apply (rule_tac x="{x,y}" in exI)  
    1.24 +apply (simp add: doubleton_in_L) 
    1.25 +done
    1.26 +
    1.27 +lemma Union_ax: "Union_ax(L)"
    1.28 +apply (simp add: Union_ax_def big_union_def, clarify)
    1.29 +apply (rule_tac x="Union(x)" in exI)  
    1.30 +apply (simp add: Union_in_L, auto) 
    1.31 +apply (blast intro: transL) 
    1.32 +done
    1.33 +
    1.34 +lemma power_ax: "power_ax(L)"
    1.35 +apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify)
    1.36 +apply (rule_tac x="{y \<in> Pow(x). L(y)}" in exI)  
    1.37 +apply (simp add: LPow_in_L, auto)
    1.38 +apply (blast intro: transL) 
    1.39 +done
    1.40 +
    1.41 +subsubsection{*For L to satisfy Replacement *}
    1.42 +
    1.43 +(*Can't move these to Formula unless the definition of univalent is moved
    1.44 +there too!*)
    1.45 +
    1.46 +lemma LReplace_in_Lset:
    1.47 +     "[|X \<in> Lset(i); univalent(L,X,Q); Ord(i)|] 
    1.48 +      ==> \<exists>j. Ord(j) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Lset(j)"
    1.49 +apply (rule_tac x="\<Union>y \<in> Replace(X, %x y. Q(x,y) & L(y)). succ(lrank(y))" 
    1.50 +       in exI)
    1.51 +apply simp
    1.52 +apply clarify 
    1.53 +apply (rule_tac a="x" in UN_I)  
    1.54 + apply (simp_all add: Replace_iff univalent_def) 
    1.55 +apply (blast dest: transL L_I) 
    1.56 +done
    1.57 +
    1.58 +lemma LReplace_in_L: 
    1.59 +     "[|L(X); univalent(L,X,Q)|] 
    1.60 +      ==> \<exists>Y. L(Y) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Y"
    1.61 +apply (drule L_D, clarify) 
    1.62 +apply (drule LReplace_in_Lset, assumption+)
    1.63 +apply (blast intro: L_I Lset_in_Lset_succ)
    1.64 +done
    1.65 +
    1.66 +lemma replacement: "replacement(L,P)"
    1.67 +apply (simp add: replacement_def, clarify)
    1.68 +apply (frule LReplace_in_L, assumption+)
    1.69 +apply clarify 
    1.70 +apply (rule_tac x=Y in exI)   
    1.71 +apply (simp add: Replace_iff univalent_def, blast) 
    1.72 +done
    1.73 +
    1.74 +end
    1.75 +
    1.76 +(*
    1.77 +
    1.78 +  and Inter_separation:
    1.79 +     "L(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. L(y) --> x\<in>y)"
    1.80 +  and cartprod_separation:
    1.81 +     "[| L(A); L(B) |] 
    1.82 +      ==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. L(x) & L(y) & pair(M,x,y,z))"
    1.83 +  and image_separation:
    1.84 +     "[| L(A); L(r) |] 
    1.85 +      ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & (\<exists>x\<in>A. L(x) & pair(M,x,y,p)))"
    1.86 +  and vimage_separation:
    1.87 +     "[| L(A); L(r) |] 
    1.88 +      ==> separation(M, \<lambda>x. \<exists>p\<in>r. L(p) & (\<exists>y\<in>A. L(x) & pair(M,x,y,p)))"
    1.89 +  and converse_separation:
    1.90 +     "L(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. L(p) & (\<exists>x y. L(x) & L(y) & 
    1.91 +				     pair(M,x,y,p) & pair(M,y,x,z)))"
    1.92 +  and restrict_separation:
    1.93 +     "L(A) 
    1.94 +      ==> separation(M, \<lambda>z. \<exists>x\<in>A. L(x) & (\<exists>y. L(y) & pair(M,x,y,z)))"
    1.95 +  and comp_separation:
    1.96 +     "[| L(r); L(s) |]
    1.97 +      ==> separation(M, \<lambda>xz. \<exists>x y z. L(x) & L(y) & L(z) &
    1.98 +			   (\<exists>xy\<in>s. \<exists>yz\<in>r. L(xy) & L(yz) & 
    1.99 +		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz)))"
   1.100 +  and pred_separation:
   1.101 +     "[| L(r); L(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & pair(M,y,x,p))"
   1.102 +  and Memrel_separation:
   1.103 +     "separation(M, \<lambda>z. \<exists>x y. L(x) & L(y) & pair(M,x,y,z) \<and> x \<in> y)"
   1.104 +  and obase_separation:
   1.105 +     --{*part of the order type formalization*}
   1.106 +     "[| L(A); L(r) |] 
   1.107 +      ==> separation(M, \<lambda>a. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) & 
   1.108 +	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
   1.109 +	     order_isomorphism(M,par,r,x,mx,g))"
   1.110 +  and well_ord_iso_separation:
   1.111 +     "[| L(A); L(f); L(r) |] 
   1.112 +      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. L(y) \<and> (\<exists>p. L(p) \<and> 
   1.113 +		     fun_apply(M,f,x,y) \<and> pair(M,y,x,p) \<and> p \<in> r)))"
   1.114 +  and obase_equals_separation:
   1.115 +     "[| L(A); L(r) |] 
   1.116 +      ==> separation
   1.117 +      (M, \<lambda>x. x\<in>A --> ~(\<exists>y. L(y) & (\<exists>g. L(g) &
   1.118 +	      ordinal(M,y) & (\<exists>my pxr. L(my) & L(pxr) &
   1.119 +	      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
   1.120 +	      order_isomorphism(M,pxr,r,y,my,g)))))"
   1.121 +  and is_recfun_separation:
   1.122 +     --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
   1.123 +     "[| L(A); L(f); L(g); L(a); L(b) |] 
   1.124 +     ==> 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.125 +  and omap_replacement:
   1.126 +     "[| L(A); L(r) |] 
   1.127 +      ==> strong_replacement(M,
   1.128 +             \<lambda>a z. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) &
   1.129 +	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
   1.130 +	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
   1.131 +
   1.132 +*)
   1.133 \ No newline at end of file