theorem-proving - Isabelle で Nitpick と Sledgehammer を一緒に呼び出す

Question

Isabelleで補題を述べるとき、私はしばしば とタイプnitpickします。次にsledgehammer、証明を自動的に見つけようと入力します。

私は疑問に思います: NitpickとSledgehammerを呼び出して、同時に実行することは可能ですか? Sledgehammerはすでに私の補題を多数の自動証明者に送っているので、それらの証明者の 1 つは実際にNitpickのような反例発見者ではないでしょうか?

Answer 1

tryIsabelleでコマンドを使用してみることができます。sledgehammer、、および他の多くのソルバー（、、、など）を並行して実行しnitpick、最初に終了したソルバーの結果を提供します。quickcheckautosimpforce

たとえば、次を実行します。

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

ハンマーからの結果を返します。