# HG changeset patch
# User oheimb
# Date 896792845 -7200
# Node ID 857dabe71d7238b5fe808e1b73e57aa621aa4404
# Parent  8f4dc836a2ead02e0f24eb1c192072066276c0b5
added split_etas

diff -r 8f4dc836a2ea -r 857dabe71d72 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Tue Jun 02 15:07:00 1998 +0200
+++ b/src/HOL/Prod.ML	Tue Jun 02 15:07:25 1998 +0200
@@ -142,6 +142,22 @@
 qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f"
   (K [rtac ext 1, split_all_tac 1, rtac split 1]);
 
+qed_goal "cond_split_eta" Prod.thy 
+	"!!f. (!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g"
+  (K [asm_simp_tac (simpset() addsimps [split_eta]) 1]);
+(*Addsimps [cond_split_eta];  with this version of split_eta, the simplifier 
+			      can eta-contract arbitrarily tupled functions.
+  Unfortunately, this renders some existing proofs very inefficient.
+                 stac split_eta does not work in general either. *)
+val split_etas = split_eta::map (fn s => prove_goal Prod.thy s 
+  (K [simp_tac (simpset() addsimps [cond_split_eta]) 1]))
+["(%(a,b,c    ). f(a,b,c    )) = f","(%(a,b,c,d    ). f(a,b,c,d    )) = f",
+ "(%(a,b,c,d,e). f(a,b,c,d,e)) = f","(%(a,b,c,d,e,g). f(a,b,c,d,e,g)) = f"];
+Addsimps split_etas; (* pragmatic solution *)
+
+Goal "(%(x,y,z).f(x,y,z)) = t";
+by(simp_tac (simpset() addsimps [cond_split_eta]) 1);
+
 qed_goal "split_beta" Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)"
 	(K [stac surjective_pairing 1, stac split 1, rtac refl 1]);