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