# HG changeset patch
# User paulson
# Date 935571199 -7200
# Node ID 1b4d7a851b343e6d4945573ab19090d530dd0030
# Parent  b275ae194e5a876186df0a27b577d4529d1d656a
split_paired_Eps and lemmas

diff -r b275ae194e5a -r 1b4d7a851b34 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Wed Aug 25 10:45:41 1999 +0200
+++ b/src/HOL/Prod.ML	Wed Aug 25 10:53:19 1999 +0200
@@ -111,11 +111,17 @@
 qed "split";
 Addsimps [split];
 
-Goal "split Pair p = p";
-by (pair_tac "p" 1);
+(*Subsumes the old split_Pair when f is the identity function*)
+Goal "split (%x y. f(x,y)) = f";
+by (rtac ext 1);
+by (pair_tac "x" 1);
 by (Simp_tac 1);
-qed "split_Pair";
-(*unused: val surjective_pairing2 = split_Pair RS sym;*)
+qed "split_Pair_apply";
+
+(*Can't be added to simpset: loops!*)
+Goal "(SOME x. P x) = (SOME (a,b). P(a,b))";
+by (simp_tac (simpset() addsimps [split_Pair_apply]) 1);
+qed "split_paired_Eps";
 
 Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
 by (split_all_tac 1);