問題タブ [isabelle]

帰納述語を定義するとき、どのパラメーターを固定し、どのパラメーターを固定しないかを選択できます。不自然な例として、次のことを考慮してください。

これを、1 つの固定パラメーターと 1 つの非固定パラメーターを持つ帰納的に定義されたセットに変換することは何とか可能ですか?

は次のエラー メッセージで拒否されます。

帰納述語バージョン (例: ) に基づいてセットを定義できることはわかっていますが、Foo P b = {(x, y). foo P b x x}帰納またはケース分析を適用する前に、常にそれを展開する必要があります (または、対応するルールを導入する必要がありますFoo。これは少し冗長に思えます)。 ）。

次のような構造のイザベル証明があります。

最初のケースは実際には数ページの長さなので、2 番目のケースを読むと、カジュアルな読者には、私自身でさえ、何をFalse指しているのかが明確ではなくなります。(まあ、実際には ですが、読み取りからではなく、インタラクティブな環境でのみです。たとえば、Isabelle/jEdit でカーソルを の後に置くと、[出力] パネルの "this" の下にcase False表示されます。)n ≠ 0

「False」ケースの仮定を明示的にすることを可能にする構文があるので、読者は IDE とやり取りしたり、proofキーワードまでスクロールしたりする必要はありませんが、仮定を適切な場所で見ることができますか?

これまでのところ、Isabelle で次のスタイルで矛盾による証明を書きました ( Jeremy Siekのパターンを使用):

ネストされた生の証明ブロックなしで機能する方法はあります{ ... }か?

私は、ドメインが自然数の有限の「インデックスセット」であり、そのイメージが最大値を定義できる何らかのタイプの関数として、ベクトルのカスタム実装を使用していますreal。たとえば、とを使用して 2 次元ベクトルを作成できvます。v 1 = 2.7v 3 = 4.2

3そのようなベクトルでは、上記の例で、最大コンポーネントのインデックスを教えてくれる「arg max」のような演算子を定義したいと思いますv。「arg max」のような演算子は、値を持つコンポーネントに適用されるタイブレーク関数をさらに受け入れるため、「the」インデックスと言っています。（背景はオークションでの入札です。）

私はMax、有限集合が次を使用して定義されていることを知ってfold1います(それがどのように機能するかはまだわかりません)。私はこれを試しましたが、それ自体は受け入れられましたが、私がやりたかった他のことにはうまくいきませんでした:

さらに、「arg max」のような演算子の特定のプロパティを証明したいことに注意してください。これには、誘導が必要になる可能性があります。finite_ne_induct有限集合上の帰納法の法則があることは知っています。わかりましたが、評価できるように演算子を定義できるようにしたいと思います（たとえば、具体的な有限集合を試す場合）が、評価します

期待される戻り値1を使用すると、次のエラーが発生します。

したがって、有限集合をリストに変換することにしました。リストでは、演算子を定義し、そのプロパティの一部を証明することができました (興味がある場合はコードを共有できます) list_nonempty_induct。

作業リストベースの定義は次のようになります。

有限集合のコンストラクターに対して関数を直接定義することに成功しませんでした。以下は機能しません。

エラーメッセージが表示されます

これは、リスト コンストラクターが として定義されているdatatypeのに対し、有限集合は単にinductiveスキームとして定義されているためでしょうか?

何であれ、この関数を有限集合上で定義する方法を知っていますか? 直接書き留めるか、折り畳み式のユーティリティ関数を使用しますか?

定理証明者の Isabelle に習い始めたのは 2～3 週間ほど前です。私はまだまったくの初心者で、チュートリアル「Isabelle/HOL でのプログラミングと証明」に取り組みました。

これまでに見つけた行列に関する唯一の助けは、HOL ライブラリのソース コードを調べることでした。

次に、行列に関するプロパティを証明する方法を学びたいと思います。行列のラムダ構文は、私にとってまだ新しいものです。Isabelle で行列を使用するためのチュートリアルまたは基本/中間の例はありますか?

私のイザベル理論では、定数係数を持つ行列があります。

転置行列を計算できます。

私の目には、後者は同等である必要があります

の定義によりtranspose。しかし、これは真実ではありません。ここで私のエラーは何ですか?

ちなみに、転置の定義は次のとおりです。

Isabelle で thf 経由でオブジェクト ロジックを作成するにはどうすればよいですか?

ドキュメントでオブジェクトロジックを作成することについて私が見つけたのは、

Isabelle/Isar リファレンス マニュアルに記載されています。

オブジェクト ロジックと、特に thf の使用について他に何を読むべきですか?

THF は、こちらの論文のように高次形式で型付けされます