Isabelle：阻止分裂元組

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

您必須從apply (simp del: split_paired_Ex)中刪除簡化器中的定理split_paired_Ex。對於元量詞!!，HOL量詞ALL和split_paired_all也有定理split_paired_All。