# 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]);