이사벨 (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도 있습니다.