src/ZF/Constructible/Relative.thy

   membership :: "[i=>o,i,i] => o" --{*membership relation*}
     "membership(M,A,r) == 
 	\<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)))"
 
 
-subsection{*Absoluteness for a transitive class model*}
+subsection{*Introducing a Transitive Class Model*}
 
 text{*The class M is assumed to be transitive and to satisfy some
       relativized ZF axioms*}
 locale (open) M_triv_axioms =
   fixes M

       and Union_ax:	    "Union_ax(M)"
       and power_ax:         "power_ax(M)"
       and replacement:      "replacement(M,P)"
       and M_nat [iff]:      "M(nat)"           (*i.e. the axiom of infinity*)
 
-lemma (in M_triv_axioms) ball_abs [simp]: 
-     "M(A) ==> (\<forall>x\<in>A. M(x) --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
-by (blast intro: transM) 
-
 lemma (in M_triv_axioms) rall_abs [simp]: 
      "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
-by (blast intro: transM) 
-
-lemma (in M_triv_axioms) bex_abs [simp]: 
-     "M(A) ==> (\<exists>x\<in>A. M(x) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
 by (blast intro: transM) 
 
 lemma (in M_triv_axioms) rex_abs [simp]: 
      "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))" 
 by (blast intro: transM) 

 text{*Simplifies proofs of equalities when there's an iff-equality
       available for rewriting, universally quantified over M. *}
 lemma (in M_triv_axioms) M_equalityI: 
      "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"
 by (blast intro!: equalityI dest: transM) 
+
+
+subsubsection{*Trivial Absoluteness Proofs: Empty Set, Pairs, etc.*}
 
 lemma (in M_triv_axioms) empty_abs [simp]: 
      "M(z) ==> empty(M,z) <-> z=0"
 apply (simp add: empty_def)
 apply (blast intro: transM) 

 apply (rule iffI) 
  apply (blast intro!: equalityI intro: transM dest!: rspec) 
 apply (blast dest: transM) 
 done
 
+subsubsection{*Absoluteness for Unions and Intersections*}
+
 lemma (in M_triv_axioms) union_abs [simp]: 
      "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"
 apply (simp add: union_def) 
 apply (blast intro: transM) 
 done

 lemma (in M_triv_axioms) succ_in_M_iff [iff]:
      "M(succ(a)) <-> M(a)"
 apply (simp add: succ_def) 
 apply (blast intro: transM) 
 done
+
+subsubsection{*Absoluteness for Separation and Replacement*}
 
 lemma (in M_triv_axioms) separation_closed [intro,simp]:
      "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
 apply (insert separation, simp add: separation_def) 
 apply (drule rspec, assumption, clarify) 

 apply (simp add: RepFun_def)
 apply (frule strong_replacement_closed, assumption)
 apply (auto dest: transM  simp add: Replace_conj_eq univalent_def) 
 done
 
-lemma (in M_triv_axioms) lam_closed [intro,simp]:
+subsubsection {*Absoluteness for @{term Lambda}*}
+
+constdefs
+ is_lambda :: "[i=>o, i, [i,i]=>o, i] => o"
+    "is_lambda(M, A, is_b, z) == 
+       \<forall>p[M]. p \<in> z <->
+        (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))"
+
+lemma (in M_triv_axioms) lam_closed:
      "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
       ==> M(\<lambda>x\<in>A. b(x))"
 by (simp add: lam_def, blast intro: RepFun_closed dest: transM) 
+
+text{*Better than @{text lam_closed}: has the formula @{term "x\<in>A"}*}
+lemma (in M_triv_axioms) lam_closed2:
+  "[|strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
+     M(A); \<forall>m[M]. m\<in>A --> M(b(m))|] ==> M(Lambda(A,b))"
+apply (simp add: lam_def)
+apply (blast intro: RepFun_closed2 dest: transM)  
+done
+
+lemma (in M_triv_axioms) lambda_abs2 [simp]: 
+     "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
+         relativize1(M,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |] 
+      ==> is_lambda(M,A,is_b,z) <-> z = Lambda(A,b)"
+apply (simp add: relativize1_def is_lambda_def)
+apply (rule iffI)
+ prefer 2 apply (simp add: lam_def) 
+apply (rule M_equalityI)
+  apply (simp add: lam_def) 
+ apply (simp add: lam_closed2)+
+done
 
 lemma (in M_triv_axioms) image_abs [simp]: 
      "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
 apply (simp add: image_def)
 apply (rule iffI) 

 lemma (in M_triv_axioms) powerset_imp_subset_Pow: 
      "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"
 apply (simp add: powerset_def) 
 apply (blast dest: transM) 
 done
+
+subsubsection{*Absoluteness for the Natural Numbers*}
 
 lemma (in M_triv_axioms) nat_into_M [intro]:
      "n \<in> nat ==> M(n)"
 by (induct n rule: nat_induct, simp_all)
 

 lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
      "M(Inr(a)) <-> M(a)"
 by (simp add: Inr_def)
 
 
-subsection{*Absoluteness for ordinals*}
+subsection {*Absoluteness for Booleans*}
+
+lemma (in M_triv_axioms) bool_of_o_closed:
+     "M(bool_of_o(P))"
+by (simp add: bool_of_o_def) 
+
+lemma (in M_triv_axioms) and_closed:
+     "[| M(p); M(q) |] ==> M(p and q)"
+by (simp add: and_def cond_def) 
+
+lemma (in M_triv_axioms) or_closed:
+     "[| M(p); M(q) |] ==> M(p or q)"
+by (simp add: or_def cond_def) 
+
+lemma (in M_triv_axioms) not_closed:
+     "M(p) ==> M(not(p))"
+by (simp add: Bool.not_def cond_def) 
+
+
+subsection{*Absoluteness for Ordinals*}
 text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
 
 lemma (in M_triv_axioms) lt_closed:
      "[| j<i; M(i) |] ==> M(j)" 
 by (blast dest: ltD intro: transM)