# HG changeset patch
# User oheimb
# Date 959960792 -7200
# Node ID 1056cbbaeb29f87c1aebaca1d456af6d93f55759
# Parent  9c1118619d6ce02c9b7b8b16af55a3a372c23f6d
added split_eta_SetCompr2 (also to simpset), generalized SetCompr_Sigma_eq

diff -r 9c1118619d6c -r 1056cbbaeb29 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Fri Jun 02 17:46:16 2000 +0200
+++ b/src/HOL/Prod.ML	Fri Jun 02 17:46:32 2000 +0200
@@ -141,12 +141,6 @@
 by (rtac (prem RS arg_cong) 1);
 qed "split_weak_cong";
 
-Goal "(%u. ? x y. u = (x, y) & P (x, y)) = P"; 
-by (rtac ext 1);
-by (Fast_tac 1);
-qed "split_eta_SetCompr";
-Addsimps [split_eta_SetCompr];
-
 Goal "(%(x,y). f(x,y)) = f";
 by (rtac ext 1);
 by (split_all_tac 1);
@@ -287,6 +281,18 @@
 AddSIs [splitI, splitI2, splitI2', mem_splitI, mem_splitI2];
 AddSEs [splitE, splitE', mem_splitE];
 
+Goal "(%u. ? x y. u = (x, y) & P (x, y)) = P"; 
+by (rtac ext 1);
+by (Fast_tac 1);
+qed "split_eta_SetCompr";
+Addsimps [split_eta_SetCompr];
+
+Goal "(%u. ? x y. u = (x, y) & P x y) = split P"; 
+br ext 1;
+by (Fast_tac 1);
+qed "split_eta_SetCompr2";
+Addsimps [split_eta_SetCompr2];
+
 (* allows simplifications of nested splits in case of independent predicates *)
 Goal "(%(a,b). P & Q a b) = (%ab. P & split Q ab)";
 by (rtac ext 1);
@@ -435,7 +441,7 @@
 by (blast_tac (claset() addEs [equalityE]) 1);
 qed "Times_eq_cancel2";
 
-Goal "{(x,y) |x y. P x & Q x y} = (SIGMA x:Collect P. Collect (Q x))";
+Goal "Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))";
 by (Fast_tac 1);
 qed "SetCompr_Sigma_eq";