src/ZF/Constructible/Relative.thy
changeset 13418 7c0ba9dba978
parent 13397 6e5f4d911435
child 13423 7ec771711c09
     1.1 --- a/src/ZF/Constructible/Relative.thy	Wed Jul 24 16:16:44 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Wed Jul 24 17:59:12 2002 +0200
     1.3 @@ -412,7 +412,7 @@
     1.4  	\<forall>p[M]. p \<in> r <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>A & x\<in>y & pair(M,x,y,p)))"
     1.5  
     1.6  
     1.7 -subsection{*Absoluteness for a transitive class model*}
     1.8 +subsection{*Introducing a Transitive Class Model*}
     1.9  
    1.10  text{*The class M is assumed to be transitive and to satisfy some
    1.11        relativized ZF axioms*}
    1.12 @@ -426,18 +426,10 @@
    1.13        and replacement:      "replacement(M,P)"
    1.14        and M_nat [iff]:      "M(nat)"           (*i.e. the axiom of infinity*)
    1.15  
    1.16 -lemma (in M_triv_axioms) ball_abs [simp]: 
    1.17 -     "M(A) ==> (\<forall>x\<in>A. M(x) --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
    1.18 -by (blast intro: transM) 
    1.19 -
    1.20  lemma (in M_triv_axioms) rall_abs [simp]: 
    1.21       "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
    1.22  by (blast intro: transM) 
    1.23  
    1.24 -lemma (in M_triv_axioms) bex_abs [simp]: 
    1.25 -     "M(A) ==> (\<exists>x\<in>A. M(x) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
    1.26 -by (blast intro: transM) 
    1.27 -
    1.28  lemma (in M_triv_axioms) rex_abs [simp]: 
    1.29       "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))" 
    1.30  by (blast intro: transM) 
    1.31 @@ -453,6 +445,9 @@
    1.32       "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"
    1.33  by (blast intro!: equalityI dest: transM) 
    1.34  
    1.35 +
    1.36 +subsubsection{*Trivial Absoluteness Proofs: Empty Set, Pairs, etc.*}
    1.37 +
    1.38  lemma (in M_triv_axioms) empty_abs [simp]: 
    1.39       "M(z) ==> empty(M,z) <-> z=0"
    1.40  apply (simp add: empty_def)
    1.41 @@ -505,6 +500,8 @@
    1.42  apply (blast dest: transM) 
    1.43  done
    1.44  
    1.45 +subsubsection{*Absoluteness for Unions and Intersections*}
    1.46 +
    1.47  lemma (in M_triv_axioms) union_abs [simp]: 
    1.48       "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"
    1.49  apply (simp add: union_def) 
    1.50 @@ -555,6 +552,8 @@
    1.51  apply (blast intro: transM) 
    1.52  done
    1.53  
    1.54 +subsubsection{*Absoluteness for Separation and Replacement*}
    1.55 +
    1.56  lemma (in M_triv_axioms) separation_closed [intro,simp]:
    1.57       "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
    1.58  apply (insert separation, simp add: separation_def) 
    1.59 @@ -621,11 +620,39 @@
    1.60  apply (auto dest: transM  simp add: Replace_conj_eq univalent_def) 
    1.61  done
    1.62  
    1.63 -lemma (in M_triv_axioms) lam_closed [intro,simp]:
    1.64 +subsubsection {*Absoluteness for @{term Lambda}*}
    1.65 +
    1.66 +constdefs
    1.67 + is_lambda :: "[i=>o, i, [i,i]=>o, i] => o"
    1.68 +    "is_lambda(M, A, is_b, z) == 
    1.69 +       \<forall>p[M]. p \<in> z <->
    1.70 +        (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))"
    1.71 +
    1.72 +lemma (in M_triv_axioms) lam_closed:
    1.73       "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
    1.74        ==> M(\<lambda>x\<in>A. b(x))"
    1.75  by (simp add: lam_def, blast intro: RepFun_closed dest: transM) 
    1.76  
    1.77 +text{*Better than @{text lam_closed}: has the formula @{term "x\<in>A"}*}
    1.78 +lemma (in M_triv_axioms) lam_closed2:
    1.79 +  "[|strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
    1.80 +     M(A); \<forall>m[M]. m\<in>A --> M(b(m))|] ==> M(Lambda(A,b))"
    1.81 +apply (simp add: lam_def)
    1.82 +apply (blast intro: RepFun_closed2 dest: transM)  
    1.83 +done
    1.84 +
    1.85 +lemma (in M_triv_axioms) lambda_abs2 [simp]: 
    1.86 +     "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
    1.87 +         relativize1(M,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |] 
    1.88 +      ==> is_lambda(M,A,is_b,z) <-> z = Lambda(A,b)"
    1.89 +apply (simp add: relativize1_def is_lambda_def)
    1.90 +apply (rule iffI)
    1.91 + prefer 2 apply (simp add: lam_def) 
    1.92 +apply (rule M_equalityI)
    1.93 +  apply (simp add: lam_def) 
    1.94 + apply (simp add: lam_closed2)+
    1.95 +done
    1.96 +
    1.97  lemma (in M_triv_axioms) image_abs [simp]: 
    1.98       "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
    1.99  apply (simp add: image_def)
   1.100 @@ -648,6 +675,8 @@
   1.101  apply (blast dest: transM) 
   1.102  done
   1.103  
   1.104 +subsubsection{*Absoluteness for the Natural Numbers*}
   1.105 +
   1.106  lemma (in M_triv_axioms) nat_into_M [intro]:
   1.107       "n \<in> nat ==> M(n)"
   1.108  by (induct n rule: nat_induct, simp_all)
   1.109 @@ -693,7 +722,26 @@
   1.110  by (simp add: Inr_def)
   1.111  
   1.112  
   1.113 -subsection{*Absoluteness for ordinals*}
   1.114 +subsection {*Absoluteness for Booleans*}
   1.115 +
   1.116 +lemma (in M_triv_axioms) bool_of_o_closed:
   1.117 +     "M(bool_of_o(P))"
   1.118 +by (simp add: bool_of_o_def) 
   1.119 +
   1.120 +lemma (in M_triv_axioms) and_closed:
   1.121 +     "[| M(p); M(q) |] ==> M(p and q)"
   1.122 +by (simp add: and_def cond_def) 
   1.123 +
   1.124 +lemma (in M_triv_axioms) or_closed:
   1.125 +     "[| M(p); M(q) |] ==> M(p or q)"
   1.126 +by (simp add: or_def cond_def) 
   1.127 +
   1.128 +lemma (in M_triv_axioms) not_closed:
   1.129 +     "M(p) ==> M(not(p))"
   1.130 +by (simp add: Bool.not_def cond_def) 
   1.131 +
   1.132 +
   1.133 +subsection{*Absoluteness for Ordinals*}
   1.134  text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
   1.135  
   1.136  lemma (in M_triv_axioms) lt_closed: