問題タブ [isar]

二項演算子があるとしf :: "sT => sT => sT"ます。fWiki でここに示されている、クライン 4 グループの 4x4 乗法テーブルを実装するように定義したいと思います。

http://en.wikipedia.org/wiki/Klein_four-group

ここで試みているのは、16 エントリのテーブルを作成することだけです。まず、次のように 4 つの定数を定義します。

次に、テーブル内の 16 エントリを実装する関数を定義します。

私は Isar で通常のようなプログラミングを行う方法を知りません。Isabelle ユーザーのリストで、(特定の) プログラミングのような構造が言語で意図的に強調されていないと言われているのを見たことがあります。

先日、単純な不自然な関数を作成しようとしましたがif, then, else、ソース ファイルでの使用を見つけた後、 isar-ref.pdfでそれらのコマンドへの参照を見つけることができませんでした。

チュートリアルを見るdefinitionと、簡単な方法で関数を定義することがわかります。それ以外は、 を必要とする再帰関数と帰納関数に関する情報しか表示されずdatatype、私の状況はそれよりも単純です。

私自身のデバイスに任せた場合、datatype上記の 4 つの定数に対して a を定義してから、いくつかの変換関数を作成して、2 項演算子f :: sT => sT => sT. を使おうとして少しいじりましfunたが、単純な取引ではありませんでした。

私は少し実験をfun行いましたinductive

更新：プログラミングと証明が答えを見つける場所であるというコメントに応えて、ここにいくつかの資料を追加します。理想的な Stackoverflow 形式から外れているようです。

私はいくつかの基本的な実験を行いました。主にfunだけでなく、 も使用しましinductiveた。私は誘導をかなり早くあきらめました。簡単な例から得たエラーのタイプは次のとおりです。

私の掛け算九九は帰納的ではないので、それをinductive追うのに時間を費やすべきだとは思いませんでした.

ここでは「パターン マッチング」が重要なアイデアのように思われるので、 を試してみましfunた。fun以下は、標準の関数型のみを使用しようとしている、本当にめちゃくちゃなコードです。

その種のエラーが発生しました。プログラミングと証明で次のようなことを読みました。

「再帰関数は、データ型コンストラクターに対するパターン マッチングによって楽しく定義されます。

これらすべてが、初心者にfun必要な印象を与えますdatatype。その兄貴分まではfunction、私はそれについて知りません。

ここにあるようです。必要なのは、16 の基本ケースを持つ再帰関数だけであり、それが乗算表を定義します。

function答えは？

この質問を編集する際に、私functionは過去を思い出しましたfunction。

try の出力は、証明できることを示しています (更新: 実際には、証明ステップの 1 つだけを証明できることを示していると思います)。

それが何を意味するのかわかりません。私が知ってfunctionいるのは、矛盾を証明しようとしているからです。私はそれがそれほど文句を言わないことを知っているだけです。このfunctionように乗算表を定義する方法を使用する場合、私は満足しています。

それでも、私は議論型なのでfunction、チュートリアルで学びませんでした. 数か月前にリファレンス マニュアルでそれについて学びましたが、その使用方法についてはまだよくわかりません。

私はfunctionで証明した を持っていautoますが、幸いなことに機能はおそらく良くありません。functionそれはの謎に追加されます。Defining Recursive Functions in Isabelle/HOLfunctionに情報があり、 と を比較しています。funfunction

ただし、 or のような再帰的なデータ型を使用しない or の例は見たことがありませfunん。よく見ていなかったのかもしれません。functionnat'a list

冗長で申し訳ありませんが、これは直接的な質問にはなりませんが、A から B に人を直接連れて行く Isabelle のチュートリアルはありません。

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

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

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

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

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

Isabelle の証明には 2 つのスタイルがあります。

ステートメント、および新しい「構造化された」Isar スタイル。私自身、どちらも役に立つと思います。「apply」スタイルはより簡潔なので、興味のない技術的な補題には便利ですが、「構造化」スタイルは主要な定理に便利です。

あるスタイルから別のスタイルに切り替えるのが好きな場合もあります。「適用」スタイルから「構造化」スタイルへの切り替えは簡単です。

私の適用チェーンで。私の質問は、「構造化」スタイルから「適用」スタイルに戻すにはどうすればよいですか?

より具体的な例を挙げると、5 つのサブゴールがあるとします。最初の 2 つのサブゴールをディスパッチするために、いくつかの「適用」命令を発行します。次に、構造化された証明を開始して、3 番目の証明を省きます。サブゴールが 2 つ残っています。これらのスタイルを「適用」するにはどうすればよいですか?

next証明ケースで使用する例を作成する目的で、小さな証明を作成しました。

詳細を失うことなく、これを合理化できますか? 魔法のトリックを使用することは、私が望んでいることではありません。Isar の使用スタイルの改善は大歓迎です。

Isar ではassume、ゴールの前提を使用して、結論を構築することができます。

Isabelle/Isar Referenceに よると

これが の唯一の使用法ですかassume、つまり、ゴールの前提から事実を取得することですか?

更新：これは広すぎると考える人もいるので、私には理解できません。質問を再定式化しようとします。

このマニュアルでは、 の論理的な内容について説明していますassume。しかし、その使用法は何ですか？それは、ゴールの前提から事実を得た場合に限られますか？