在Isabelle中一起調用Nitpick和大錘

Question

當我在Isabelle中聲明一個引理時，我經常輸入nitpick，如果這樣不能給我一個反例。 然後，我輸入sledgehammer以嘗試自動找到證明。

我想知道：是否有可能調用雞蛋裏挑骨頭和大錘讓他們同時運行？ 由於大錘已經將我的引理髮送給一堆自動證明者，那麼這些證明者中的哪一個實際上不能成爲反例子查找者，如Nitpick？

Answer 1

您可以嘗試在Isabelle中使用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是能夠解決的目標。

最後，改變類型約束更具挑戰性的32 word型（可從Word在HOL-Word）：

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

將大錘返回結果。