Isabelle에서 Nitpick과 Sledgehammer를 함께 호출

Question

Isabelle에 보조 정리를 쓸 때, 나는 종종 nitpick을 입력하고, 반례를주지 않는다. 다음에 sledgehammer을 입력하면 증명을 자동으로 찾으려고 시도합니다.

이 궁금하다 : 그것은 가능하다 그들은 동시에 실행되도록 Nitpick 및 슬레지 해머를 호출? 슬레지 해머이 이미 자동 보조 장치에 내 보조 정리를 보내고 있기 때문에 보조 장치 중 하나는 실제로 Nitpick과 같은 반증자가 될 수 있습니까?

Answer 1

이사벨에서 try 명령을 사용해 볼 수 있습니다. sledgehammer, nitpick, quickcheck 및 기타 여러 솔버 (예 : auto, simp, force 등)가 병렬로 실행되어 완료된 첫 번째 결과를 제공합니다.

lemma "(a * (b + 1)) = (a * b + a)" 
    try 

은 정리가 일반적으로 사실이 아니다 것을 나타내는, nitpick에서 카운터 - 예를 반환합니다 다음 실행 예를 들어

. 유형의 제약 조건을 추가 :

lemma "((a :: nat) * (b + 1)) = (a * b + a)" 
    try 

지금 simp가 목표를 해결할 수 있음을 알리는 메시지를 반환합니다.

마지막으로, (HOL-Word에서 Word에서 사용 가능) 더 도전 32 word 유형으로 유형의 제약 조건을 변경 :

lemma "((a :: 32 word) * (b + 1)) = (a * b + a)" 
    try 

것은 쇠망에서 결과를 반환합니다.