isabelle - Isabelle: simp がタプルを分割するのを止める

Question

simpメソッドがタプルをコンポーネントに分割しないようにするにはどうすればよいですか?

例。私が書くなら

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

証明状態は良好です∃z. foo z。私がそれから書くなら

apply (simp)

証明状態になり∃a aa ab ac b. blah (a, aa, ab, ac, b)ます。simpに展開fooされているのが好きですがblah、変数zをそのままにしておきたいと思います。

Answer 1

split_paired_Exのように単純化器から定理を削除する必要がありapply (simp del: split_paired_Ex)ます。split_paired_AllHOL量指定子ALLとsplit_paired_allメタ量指定子の定理もあり!!ます。