# HG changeset patch
# User paulson
# Date 1028133025 -7200
# Node ID cdde97e1db1cf6a69ca9f8a61794e4ac2468d937
# Parent  2f98365f57a84a90c85c0dc6da4c23cbd0836f5c
some progress towards "satisfies"

diff -r 2f98365f57a8 -r cdde97e1db1c src/ZF/Constructible/Datatype_absolute.thy
--- a/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 31 17:42:38 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 31 18:30:25 2002 +0200
@@ -596,6 +596,14 @@
        transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
 done
 
+text{*Helps to prove instances of @{term transrec_replacement}*}
+lemma (in M_eclose) transrec_replacementI: 
+   "[|M(a);
+    strong_replacement (M, 
+                  \<lambda>x z. \<exists>y[M]. pair(M, x, y, z) \<and> is_wfrec(M,MH,Memrel(eclose({a})),x,y))|]
+    ==> transrec_replacement(M,MH,a)"
+by (simp add: transrec_replacement_def wfrec_replacement_def) 
+
 
 subsection{*Absoluteness for the List Operator @{term length}*}
 constdefs
diff -r 2f98365f57a8 -r cdde97e1db1c src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Wed Jul 31 17:42:38 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Wed Jul 31 18:30:25 2002 +0200
@@ -284,10 +284,27 @@
 apply (intro Imp_reflection All_reflection, assumption)
 done
 
+text{*This version handles an alternative form of the bounded quantifier
+      in the second argument of @{text REFLECTS}.*}
+theorem Rex_reflection':
+     "REFLECTS[ \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
+      ==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z[**Lset(a)]. Q(a,x,z)]"
+apply (unfold setclass_def rex_def)
+apply (erule Rex_reflection [unfolded rex_def Bex_def]) 
+done
+
+text{*As above.*}
+theorem Rall_reflection':
+     "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
+      ==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z[**Lset(a)]. Q(a,x,z)]"
+apply (unfold setclass_def rall_def)
+apply (erule Rall_reflection [unfolded rall_def Ball_def]) 
+done
+
 lemmas FOL_reflections =
         Triv_reflection Not_reflection And_reflection Or_reflection
         Imp_reflection Iff_reflection Ex_reflection All_reflection
-        Rex_reflection Rall_reflection
+        Rex_reflection Rall_reflection Rex_reflection' Rall_reflection'
 
 lemma ReflectsD:
      "[|REFLECTS[P,Q]; Ord(i)|]
diff -r 2f98365f57a8 -r cdde97e1db1c src/ZF/Constructible/Rec_Separation.thy
--- a/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 31 17:42:38 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 31 18:30:25 2002 +0200
@@ -1235,10 +1235,12 @@
 done
 
 theorem bool_of_o_reflection:
-     "REFLECTS[\<lambda>x. is_bool_of_o(L, P(x), f(x)),  
-               \<lambda>i x. is_bool_of_o(**Lset(i), P(x), f(x))]"
-apply (simp only: is_bool_of_o_def setclass_simps)
+     "REFLECTS [P(L), \<lambda>i. P(**Lset(i))] ==>
+      REFLECTS[\<lambda>x. is_bool_of_o(L, P(L,x), f(x)),  
+               \<lambda>i x. is_bool_of_o(**Lset(i), P(**Lset(i),x), f(x))]"
+apply (simp (no_asm) only: is_bool_of_o_def setclass_simps)
 apply (intro FOL_reflections function_reflections) 
+apply assumption+
 done
 
 
@@ -1407,5 +1409,6 @@
 
 lemmas eclose_closed [intro, simp] = M_eclose.eclose_closed [OF M_eclose_L]
   and eclose_abs [intro, simp] = M_eclose.eclose_abs [OF M_eclose_L]
+  and transrec_replacementI = M_eclose.transrec_replacementI [OF M_eclose_L]
 
 end
diff -r 2f98365f57a8 -r cdde97e1db1c src/ZF/Constructible/Separation.thy
--- a/src/ZF/Constructible/Separation.thy	Wed Jul 31 17:42:38 2002 +0200
+++ b/src/ZF/Constructible/Separation.thy	Wed Jul 31 18:30:25 2002 +0200
@@ -623,5 +623,7 @@
 declare Int_closed [intro, simp]
 declare is_funspace_abs [simp]
 declare finite_funspace_closed [intro, simp]
+declare membership_abs [simp] 
+declare Memrel_closed  [intro,simp]
 
 end