src/ZF/Constructible/L_axioms.thy
author paulson
Mon Jul 01 18:16:18 2002 +0200 (2002-07-01)
changeset 13268 240509babf00
parent 13223 45be08fbdcff
child 13269 3ba9be497c33
permissions -rw-r--r--
more use of relativized quantifiers
list_closed
     1 header {* The class L satisfies the axioms of ZF*}
     2 
     3 theory L_axioms = Formula + Relative:
     4 
     5 
     6 text {* The class L satisfies the premises of locale @{text M_axioms} *}
     7 
     8 lemma transL: "[| y\<in>x; L(x) |] ==> L(y)"
     9 apply (insert Transset_Lset) 
    10 apply (simp add: Transset_def L_def, blast) 
    11 done
    12 
    13 lemma nonempty: "L(0)"
    14 apply (simp add: L_def) 
    15 apply (blast intro: zero_in_Lset) 
    16 done
    17 
    18 lemma upair_ax: "upair_ax(L)"
    19 apply (simp add: upair_ax_def upair_def, clarify)
    20 apply (rule_tac x="{x,y}" in exI)  
    21 apply (simp add: doubleton_in_L) 
    22 done
    23 
    24 lemma Union_ax: "Union_ax(L)"
    25 apply (simp add: Union_ax_def big_union_def, clarify)
    26 apply (rule_tac x="Union(x)" in exI)  
    27 apply (simp add: Union_in_L, auto) 
    28 apply (blast intro: transL) 
    29 done
    30 
    31 lemma power_ax: "power_ax(L)"
    32 apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify)
    33 apply (rule_tac x="{y \<in> Pow(x). L(y)}" in exI)  
    34 apply (simp add: LPow_in_L, auto)
    35 apply (blast intro: transL) 
    36 done
    37 
    38 subsubsection{*For L to satisfy Replacement *}
    39 
    40 (*Can't move these to Formula unless the definition of univalent is moved
    41 there too!*)
    42 
    43 lemma LReplace_in_Lset:
    44      "[|X \<in> Lset(i); univalent(L,X,Q); Ord(i)|] 
    45       ==> \<exists>j. Ord(j) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Lset(j)"
    46 apply (rule_tac x="\<Union>y \<in> Replace(X, %x y. Q(x,y) & L(y)). succ(lrank(y))" 
    47        in exI)
    48 apply simp
    49 apply clarify 
    50 apply (rule_tac a="x" in UN_I)  
    51  apply (simp_all add: Replace_iff univalent_def) 
    52 apply (blast dest: transL L_I) 
    53 done
    54 
    55 lemma LReplace_in_L: 
    56      "[|L(X); univalent(L,X,Q)|] 
    57       ==> \<exists>Y. L(Y) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Y"
    58 apply (drule L_D, clarify) 
    59 apply (drule LReplace_in_Lset, assumption+)
    60 apply (blast intro: L_I Lset_in_Lset_succ)
    61 done
    62 
    63 lemma replacement: "replacement(L,P)"
    64 apply (simp add: replacement_def, clarify)
    65 apply (frule LReplace_in_L, assumption+, clarify) 
    66 apply (rule_tac x=Y in exI)   
    67 apply (simp add: Replace_iff univalent_def, blast) 
    68 done
    69 
    70 end
    71 
    72 (*
    73 
    74   and Inter_separation:
    75      "L(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. L(y) --> x\<in>y)"
    76   and cartprod_separation:
    77      "[| L(A); L(B) |] 
    78       ==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. L(x) & L(y) & pair(M,x,y,z))"
    79   and image_separation:
    80      "[| L(A); L(r) |] 
    81       ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & (\<exists>x\<in>A. L(x) & pair(M,x,y,p)))"
    82   and vimage_separation:
    83      "[| L(A); L(r) |] 
    84       ==> separation(M, \<lambda>x. \<exists>p\<in>r. L(p) & (\<exists>y\<in>A. L(x) & pair(M,x,y,p)))"
    85   and converse_separation:
    86      "L(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. L(p) & (\<exists>x y. L(x) & L(y) & 
    87 				     pair(M,x,y,p) & pair(M,y,x,z)))"
    88   and restrict_separation:
    89      "L(A) 
    90       ==> separation(M, \<lambda>z. \<exists>x\<in>A. L(x) & (\<exists>y. L(y) & pair(M,x,y,z)))"
    91   and comp_separation:
    92      "[| L(r); L(s) |]
    93       ==> separation(M, \<lambda>xz. \<exists>x y z. L(x) & L(y) & L(z) &
    94 			   (\<exists>xy\<in>s. \<exists>yz\<in>r. L(xy) & L(yz) & 
    95 		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz)))"
    96   and pred_separation:
    97      "[| L(r); L(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & pair(M,y,x,p))"
    98   and Memrel_separation:
    99      "separation(M, \<lambda>z. \<exists>x y. L(x) & L(y) & pair(M,x,y,z) \<and> x \<in> y)"
   100   and obase_separation:
   101      --{*part of the order type formalization*}
   102      "[| L(A); L(r) |] 
   103       ==> separation(M, \<lambda>a. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) & 
   104 	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
   105 	     order_isomorphism(M,par,r,x,mx,g))"
   106   and well_ord_iso_separation:
   107      "[| L(A); L(f); L(r) |] 
   108       ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. L(y) \<and> (\<exists>p. L(p) \<and> 
   109 		     fun_apply(M,f,x,y) \<and> pair(M,y,x,p) \<and> p \<in> r)))"
   110   and obase_equals_separation:
   111      "[| L(A); L(r) |] 
   112       ==> separation
   113       (M, \<lambda>x. x\<in>A --> ~(\<exists>y. L(y) & (\<exists>g. L(g) &
   114 	      ordinal(M,y) & (\<exists>my pxr. L(my) & L(pxr) &
   115 	      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
   116 	      order_isomorphism(M,pxr,r,y,my,g)))))"
   117   and is_recfun_separation:
   118      --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
   119      "[| L(A); L(f); L(g); L(a); L(b) |] 
   120      ==> 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)"
   121   and omap_replacement:
   122      "[| L(A); L(r) |] 
   123       ==> strong_replacement(M,
   124              \<lambda>a z. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) &
   125 	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
   126 	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
   127 
   128 *)