Isabelle: stop simp from splitting a tuple

Question

How can I stop the simp method from splitting a tuple into its components?

Example. If I write

fun foo where "foo z = blah z" 
lemma "∃z :: nat × nat × nat × nat × nat. foo z"

the proof state is ∃z. foo z. If I then write

apply (simp)

the proof state becomes ∃a aa ab ac b. blah (a, aa, ab, ac, b). I like that simp has expanded foo into blah, but I would rather it kept my variable z as it is.

Answer 1

You have to remove the theorem split_paired_Ex from the simplifier as in apply (simp del: split_paired_Ex). There is also the theorem split_paired_All for the HOL quantifier ALL and split_paired_all for the meta-quantifier !!.