# HG changeset patch
# User paulson
# Date 1025772832 -7200
# Node ID f504f5d284d304e10358396233f6860a11253437
# Parent  a73ab154f75cf54d1d8e77036d9dbc074d1c506d
reflection for rall and rex

diff -r a73ab154f75c -r f504f5d284d3 src/ZF/Constructible/Reflection.thy
--- a/src/ZF/Constructible/Reflection.thy	Thu Jul 04 10:52:33 2002 +0200
+++ b/src/ZF/Constructible/Reflection.thy	Thu Jul 04 10:53:52 2002 +0200
@@ -182,6 +182,8 @@
        simp_all add: Mset_mono_le Mset_cont Pair_in_Mset) 
 done
 
+subsection{*Packaging the Quantifier Reflection Rules*}
+
 lemma (in reflection) Ex_reflection_0:
      "Reflects(Cl,P0,Q0) 
       ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(P0,a), 
@@ -220,6 +222,23 @@
 by (rule All_reflection_0 [of _ "\<lambda>x. P(fst(x),snd(x))" 
                                 "\<lambda>a x. Q(a,fst(x),snd(x))", simplified])
 
+text{*And again, this time using class-bounded quantifiers*}
+
+theorem (in reflection) Rex_reflection [intro]:
+     "Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) 
+      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. P(fst(x),snd(x)), a), 
+                   \<lambda>x. \<exists>z[M]. P(x,z), 
+                   \<lambda>a x. \<exists>z\<in>Mset(a). Q(a,x,z))"
+by (unfold rex_def, blast) 
+
+theorem (in reflection) Rall_reflection [intro]:
+     "Reflects(Cl,  \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
+      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. ~P(fst(x),snd(x)), a), 
+                   \<lambda>x. \<forall>z[M]. P(x,z), 
+                   \<lambda>a x. \<forall>z\<in>Mset(a). Q(a,x,z))" 
+by (unfold rall_def, blast) 
+
+
 text{*No point considering bounded quantifiers, where reflection is trivial.*}