author paulson Wed, 31 Jul 2002 18:30:25 +0200 changeset 13440 cdde97e1db1c parent 13439 2f98365f57a8 child 13441 d6d620639243
some progress towards "satisfies"
```--- 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)"
+

subsection{*Absoluteness for the List Operator @{term length}*}
constdefs```
```--- 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)|]```
```--- 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```
```--- 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```