# HG changeset patch
# User paulson
# Date 1027526352 -7200
# Node ID 7c0ba9dba978a2809cc138fe9bee715f2d6c2fdb
# Parent  12cc77f90811835606946dc78d1059ee729a0e5b
tweaks, aiming towards relativization of "satisfies"

diff -r 12cc77f90811 -r 7c0ba9dba978 src/ZF/Constructible/Datatype_absolute.thy
--- 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) |] 
diff -r 12cc77f90811 -r 7c0ba9dba978 src/ZF/Constructible/L_axioms.thy
--- 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] 
diff -r 12cc77f90811 -r 7c0ba9dba978 src/ZF/Constructible/Rec_Separation.thy
--- 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"));
diff -r 12cc77f90811 -r 7c0ba9dba978 src/ZF/Constructible/Relative.thy
--- 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:
diff -r 12cc77f90811 -r 7c0ba9dba978 src/ZF/Constructible/WF_absolute.thy
--- 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.*}