--- a/src/ZF/Constructible/Datatype_absolute.thy Wed Jul 24 16:16:44 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy Wed Jul 24 17:59:12 2002 +0200
@@ -499,7 +499,7 @@
"is_eclose(M,A,Z) == \<forall>u[M]. u \<in> Z <-> mem_eclose(M,A,u)"
-locale (open) M_eclose = M_wfrank +
+locale (open) M_eclose = M_datatypes +
assumes eclose_replacement1:
"M(A) ==> iterates_replacement(M, big_union(M), A)"
and eclose_replacement2:
@@ -569,22 +569,25 @@
@{text "trans_wfrec_abs"} rather than @{text "trans_wfrec_abs"},
which I haven't even proved yet. *}
theorem (in M_eclose) transrec_abs:
- "[|Ord(i); M(i); M(z);
- transrec_replacement(M,MH,i); relativize2(M,MH,H);
+ "[|transrec_replacement(M,MH,i); relativize2(M,MH,H);
+ Ord(i); M(i); M(z);
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)"
-by (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
+apply (rotate_tac 2)
+apply (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
+done
theorem (in M_eclose) transrec_closed:
- "[|Ord(i); M(i); M(z);
- transrec_replacement(M,MH,i); relativize2(M,MH,H);
+ "[|transrec_replacement(M,MH,i); relativize2(M,MH,H);
+ Ord(i); M(i);
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
==> M(transrec(i,H))"
-by (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
+apply (rotate_tac 2)
+apply (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
-
+done
subsection{*Absoluteness for the List Operator @{term length}*}
@@ -803,6 +806,17 @@
apply (simp add: non_formula_case)
done
+text{*Compared with @{text formula_case_closed'}, the premise on @{term p} is
+ stronger while the other premises are weaker, incorporating typing
+ information.*}
+lemma (in M_datatypes) formula_case_closed [intro,simp]:
+ "[|p \<in> formula;
+ \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(a(x,y));
+ \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(b(x,y));
+ \<forall>x[M]. \<forall>y[M]. x\<in>formula --> y\<in>formula --> M(c(x,y));
+ \<forall>x[M]. x\<in>formula --> M(d(x))|] ==> M(formula_case(a,b,c,d,p))"
+by (erule formula.cases, simp_all)
+
lemma (in M_triv_axioms) formula_case_abs [simp]:
"[| relativize2(M,is_a,a); relativize2(M,is_b,b);
relativize2(M,is_c,c); relativize1(M,is_d,d); M(p); M(z) |]
--- a/src/ZF/Constructible/L_axioms.thy Wed Jul 24 16:16:44 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy Wed Jul 24 17:59:12 2002 +0200
@@ -96,9 +96,7 @@
([transL, nonempty, upair_ax, Union_ax, power_ax, replacement, L_nat]
MRS (inst "M" "L" th));
-bind_thm ("ball_abs", triv_axioms_L (thm "M_triv_axioms.ball_abs"));
bind_thm ("rall_abs", triv_axioms_L (thm "M_triv_axioms.rall_abs"));
-bind_thm ("bex_abs", triv_axioms_L (thm "M_triv_axioms.bex_abs"));
bind_thm ("rex_abs", triv_axioms_L (thm "M_triv_axioms.rex_abs"));
bind_thm ("ball_iff_equiv", triv_axioms_L (thm "M_triv_axioms.ball_iff_equiv"));
bind_thm ("M_equalityI", triv_axioms_L (thm "M_triv_axioms.M_equalityI"));
@@ -144,9 +142,7 @@
bind_thm ("number3_abs", triv_axioms_L (thm "M_triv_axioms.number3_abs"));
*}
-declare ball_abs [simp]
declare rall_abs [simp]
-declare bex_abs [simp]
declare rex_abs [simp]
declare empty_abs [simp]
declare subset_abs [simp]
--- a/src/ZF/Constructible/Rec_Separation.thy Wed Jul 24 16:16:44 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy Wed Jul 24 17:59:12 2002 +0200
@@ -1114,7 +1114,7 @@
val m_eclose = [eclose_replacement1, eclose_replacement2];
fun eclose_L th =
- kill_flex_triv_prems (m_eclose MRS (wfrank_L th));
+ kill_flex_triv_prems (m_eclose MRS (datatypes_L th));
bind_thm ("eclose_closed", eclose_L (thm "M_eclose.eclose_closed"));
bind_thm ("eclose_abs", eclose_L (thm "M_eclose.eclose_abs"));
--- a/src/ZF/Constructible/Relative.thy Wed Jul 24 16:16:44 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy Wed Jul 24 17:59:12 2002 +0200
@@ -412,7 +412,7 @@
\<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*}
@@ -426,18 +426,10 @@
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)
@@ -453,6 +445,9 @@
"[| !!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)
@@ -505,6 +500,8 @@
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)
@@ -555,6 +552,8 @@
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)
@@ -621,11 +620,39 @@
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)
@@ -648,6 +675,8 @@
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)
@@ -693,7 +722,26 @@
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:
--- a/src/ZF/Constructible/WF_absolute.thy Wed Jul 24 16:16:44 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy Wed Jul 24 17:59:12 2002 +0200
@@ -568,7 +568,7 @@
apply (drule_tac x1=x and x="\<lambda>x\<in>r -`` {x}. wfrec(r, x, H)"
in rspec [THEN rspec])
apply (simp_all add: function_lam)
-apply (blast intro: dest: pair_components_in_M )
+apply (blast intro: lam_closed dest: pair_components_in_M )
done
text{*Eliminates one instance of replacement.*}