miniscoping for class-bounded quantifiers (rall and rex)

--- a/src/ZF/OrdQuant.thy	Wed Jul 03 14:52:57 2002 +0200
+++ b/src/ZF/OrdQuant.thy	Thu Jul 04 10:50:24 2002 +0200
@@ -135,7 +135,8 @@
 
 (*Congruence rule for rewriting*)
 lemma oall_cong [cong]:
-    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')"
+    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] 
+     ==> oall(a, %x. P(x)) <-> oall(a', %x. P'(x))"
 by (simp add: oall_def)
 
 
@@ -158,7 +159,8 @@
 done
 
 lemma oex_cong [cong]:
-    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] ==> oex(a,P) <-> oex(a',P')"
+    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] 
+     ==> oex(a, %x. P(x)) <-> oex(a', %x. P'(x))"
 apply (simp add: oex_def cong add: conj_cong)
 done
 
@@ -231,7 +233,8 @@
 
 (*Congruence rule for rewriting*)
 lemma rall_cong [cong]:
-    "(!!x. M(x) ==> P(x) <-> P'(x)) ==> rall(M,P) <-> rall(M,P')"
+    "(!!x. M(x) ==> P(x) <-> P'(x)) 
+     ==> rall(M, %x. P(x)) <-> rall(M, %x. P'(x))"
 by (simp add: rall_def)
 
 (*** Relativized existential quantifier ***)
@@ -255,9 +258,16 @@
 by (simp add: rex_def)
 
 lemma rex_cong [cong]:
-    "(!!x. M(x) ==> P(x) <-> P'(x)) ==> rex(M,P) <-> rex(M,P')"
+    "(!!x. M(x) ==> P(x) <-> P'(x)) 
+     ==> rex(M, %x. P(x)) <-> rex(M, %x. P'(x))"
 by (simp add: rex_def cong: conj_cong)
 
+lemma rall_is_ball [simp]: "(\<forall>x[%z. z\<in>A]. P(x)) <-> (\<forall>x\<in>A. P(x))"
+by blast
+
+lemma rex_is_bex [simp]: "(\<exists>x[%z. z\<in>A]. P(x)) <-> (\<exists>x\<in>A. P(x))"
+by blast
+
 lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (ALL x[M]. P(x))";
 by (simp add: rall_def atomize_all atomize_imp)
 
@@ -276,7 +286,7 @@
      "(ALL x[M]. P --> Q(x)) <-> (P --> (ALL x[M]. Q(x)))"
 by blast+
 
-lemmas rall_simps = rall_simps1 rall_simps2
+lemmas rall_simps [simp] = rall_simps1 rall_simps2
 
 lemma rall_conj_distrib:
     "(ALL x[M]. P(x) & Q(x)) <-> ((ALL x[M]. P(x)) & (ALL x[M]. Q(x)))"
@@ -295,7 +305,7 @@
      "(EX x[M]. P --> Q(x)) <-> (((ALL x[M]. False) | P) --> (EX x[M]. Q(x)))"
 by blast+
 
-lemmas rex_simps = rex_simps1 rex_simps2
+lemmas rex_simps [simp] = rex_simps1 rex_simps2
 
 lemma rex_disj_distrib:
     "(EX x[M]. P(x) | Q(x)) <-> ((EX x[M]. P(x)) | (EX x[M]. Q(x)))"