new rules for simplifying quantifiers with Sigma

--- a/src/ZF/OrderType.thy	Tue Jun 01 18:52:38 2004 +0200
+++ b/src/ZF/OrderType.thy	Wed Jun 02 17:35:08 2004 +0200
@@ -812,10 +812,11 @@
  prefer 2
  apply (simp add: Ord_ordertype well_ord_rmult well_ord_Memrel lt_Ord2)
 apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel lt_Ord2)
-apply (rule bexI)
-prefer 2 apply (blast elim!: ltE)
+apply (rule bexI [of _ i']) 
+apply (rule bexI [of _ j']) 
 apply (simp add: ordertype_pred_Pair_lemma ltI omult_def [symmetric])
 apply (simp add: lt_Ord lt_Ord2 raw_oadd_eq_oadd)
+apply (simp_all add: lt_def) 
 done
 
 lemma omult_unfold:

--- a/src/ZF/Ordinal.thy	Tue Jun 01 18:52:38 2004 +0200
+++ b/src/ZF/Ordinal.thy	Wed Jun 02 17:35:08 2004 +0200
@@ -293,7 +293,7 @@
 by (unfold Memrel_def, blast)
 
 lemma relation_Memrel: "relation(Memrel(A))"
-by (simp add: relation_def Memrel_def, blast)
+by (simp add: relation_def Memrel_def)
 
 (*The membership relation (as a set) is well-founded.
   Proof idea: show A<=B by applying the foundation axiom to A-B *)

--- a/src/ZF/pair.thy	Tue Jun 01 18:52:38 2004 +0200
+++ b/src/ZF/pair.thy	Wed Jun 02 17:35:08 2004 +0200
@@ -149,6 +149,18 @@
 lemma splitD: "split(R,<a,b>) ==> R(a,b)"
 by (simp add: split_def)
 
+text {*
+  \bigskip Complex rules for Sigma.
+*}
+
+lemma split_paired_Bex_Sigma [simp]:
+     "(\<exists>z \<in> Sigma(A,B). P(z)) <-> (\<exists>x \<in> A. \<exists>y \<in> B(x). P(<x,y>))"
+by blast
+
+lemma split_paired_Ball_Sigma [simp]:
+     "(\<forall>z \<in> Sigma(A,B). P(z)) <-> (\<forall>x \<in> A. \<forall>y \<in> B(x). P(<x,y>))"
+by blast
+
 ML
 {*
 val singleton_eq_iff = thm "singleton_eq_iff";