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元量词也有定理!!。