問題タブ [isabelle]

多くの場合sledgehammer、証明を見つけるという問題が発生しますが、それを挿入しても終了しません。sledgehammerIsabelle の最も重要な部分の 1 つだと思いますが、証明が失敗すると面倒になります。

Sledgehammerのチュートリアルには、「なぜ Metis は証明の再構築に失敗するのか?」という小さな章があります。

それはリストします：

1. isar_proofs各ステップが によって正当化される段階的な Isar 証明を取得するオプションを試してくださいmetis。ステップはかなり小さいので、 metis再生できる可能性が高くなります。
2. smtの代わりに証明方法を試してくださいmetis。通常はより強力ですが、証明を再生するために Z3 を使用できるようにするか、SMT ソルバーを信頼するか、証明書を使用する必要があります。
3. 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、、、、 、を介して、必要な事実を渡しながら、blastまたは証明メソッドを試してください。autounfoldingusingintro:elim:dest:simp:

問題は、最初のオプションでは証明がより冗長になり、手動の介入が必要になることです。2 番目のオプションはほとんど機能しません。

では、3 番目のオプションはどうでしょうか。適用できる簡単なヒューリスティックはありますか?

unfoldingとはどう違いusingますか？また、失敗した証明からintro:、elim:、およびを使用する方法に関するベスト プラクティスはありますか?dest:metis

部分的な例

証明の最初の行は取るに足らないように見えるので、削除したいと思います。最初の行を削除してsledgehammerも証明は見つかりますが、この見つかった証明は失敗します (終了しません)。

最近、イザベルの定理証明器を使い始めました。別の補題を証明したいので、HOL ライブラリにある補題「det_linear_row_setsum」で使用されているものとは異なる表記法を使用したいと思います。より具体的には、「χ i 」ではなく「χ ij 表記」を使用したいと考えています。しばらくの間、同等の式を定式化しようとしてきましたが、まだわかりませんでした。

..

という名前の Isabelle 理論ファイルがありますJohn.thy。友人に見せたいのですが、友人は Isabelle を持っておらず、生の.thyファイルを読むのは簡単ではありません。Isabelle ライブラリ (このようなもの: http://isabelle.in.tum.de/library/HOL/Finite_Set.html ) で、かなり構文が強調表示されている Web ページをいくつか見たことがあります。そのように。

では、どうやって作ることができJohn.htmlますか？私はドキュメンテーションを見てきましたが、すべてのビルドファイルやメイクファイルなど、かなり恐ろしく難しいように見えます。これを行う最も簡単な方法を親切な魂が説明できますか?

というレコード タイプを作成しgraph、適切な「のサブグラフである」関係を定義しました。ordグラフのセットとサブグラフの関係が一緒になって順序を形成すること、つまりクラスのインスタンスであることを示したいと思います。しかし、私はそれを機能させることができません。これが私の最小限の作業例です：

エラーが発生します：

Type unification failed: No type arity graph_ext :: ord"

instantiation graph :: ordや などを入力してみinstantiation graph_ext :: ordましたが、何もうまくいかないようです。何か案は？

イザベル理論 (HOL セッションなど) の HTML ドキュメントを生成したいのですが、証明は含めません。

つまり、 http://isabelle.in.tum.de/library/HOL/Nat.htmlのようなページを作成したい のですが、たとえば、

私だけが見たい

その理由は、利用可能な定理を調べるために HTML ページを使用しているからですが、その場合、証明は気を散らすだけです。(PDF を生成するときにプルーフを省略できることは知っていますが、特に HTML ドキュメントに興味があります。)

自然数のベクトルの最大値を見つけたいです。ただし、ベクトル (つまり、「vec」) は、セットまたはリストとは異なる型です。vec の型のレベリングやリフティング、再帰関数の定義など、うまくいかないアイデアをいくつか考えました。

ベクトルの最大値を取得するために提案する解決策は何ですか?

ときどき<statement> solve_direct(通常は を介し​​て呼び出し<statement> tryます) は多数のライブラリ定理をリストし、「現在の目標は次の方法で直接解決できます: …」と述べています。

<theorem>を の検索結果の 1 つとすると、solve_directほとんどの場合、 を証明でき<statement> by (rule theorem)ます。

ただし、そのような証明が受け入れられない場合があり、その結果、「最初の証明方法を適用できませんでした」というエラー メッセージが表示されます。

によって見つかった定理を再利用するための一般的な別の手法はありsolve_directますか?

それとも個々の状況によるのでしょうか？最小限の例を作成して、この質問に添付することができます。

Isabelle には、quick_and_dirtyでプルーフをスキップできるモードがありますsorry。jEdit ではデフォルトで有効になっており、デフォルトでは無効になっていますisabelle build。設定を変更するにはどうすればよいですか

• jEdit で (対話的に、またはコマンド ライン パラメーターを使用して)、
• の場合isabelle build、コマンド ラインから、
• についてisabelle buildは、ROOTファイル内にそれぞれ。

また、Isabelle に、できれば jEdit でインタラクティブに、「現在の理論とその親のどの補題がsorry"を使用して証明されているか?

（Googleで見つけたメーリングリストの投稿とは対照的に、常に最新の回答があることを期待して、ここでこれを尋ねています。）