問題タブ [isabelle]

いくつかの述語があるとしましょう

そしてそれinductive以上

最初のパラメータ「a_b」の誘導性は固定です。"a_b" はタプルで、やや見苦しい構文になります。残念ながら isabelle は、私が のようなものを書くことを許可していませんfor "(a,b)"。

この帰納的述語に対して、より適切な導入規則と帰納規則を作成するにはどうすればよいでしょうか?

のような定義済み定数 (再帰関数または定義用) を含む理論ファイルをインポートする場合f、現在の理論ファイルでそのような定数を非表示にするにはどうすればよいですか? fつまり、それが自由変数であることを確認したいのです。インポートしたファイルを変更したくありません。

まず、型クラスについてよく知らなくても、型クラスを使用できない場合や方法を理解していない場合を除き、型クラスは型の表記法をオーバーロードするための最良の方法のようです。私は型クラスを使用していません。

\<in>第二に、\<times>、*、\<union>、 など、すべての型に意味を持つ演算子の表記法をオーバーライドしたくないと確信しています。

ただし、このような演算子+は type には意味がありませんがsT、これは最初のポイントにつながります。最終的には+、 type に複数の意味を持たsT => sT => sTせたいと考えていますが、それは実現しないと思います。

例の 4 つのバージョン

私の質問を具体的にし、問題を抱えているのは私だけではないことを示すために、クラインのコースから簡単な例を取り上げます。ファイルはDemo14.thyです。

例の 4 つのバージョンの後、「4 番目の例では、警告を取り除くことができますか?」と尋ねます。

彼は、警告もエラーも出さない単純な例から始めます。

彼は\<cdot>.

\<cdot>彼をに変更する+と、エラーが発生します。

HOL ソースを調べたところ、 type 、特に特定の型クラスに対して+が定義されていることがわかりました。('a => 'a => 'a)

semi2単独に固有のものではないことを確認するために変更する'aと、警告のみが表示されます。

私が本当に気にかけているのは、この 4 番目のバージョンです。挿入したにもかかわらず、警告が表示され(x::sT)ます。

警告は次のとおりです。

まとめと質問

私自身は、次のように要約しています。 演算子+は多くの場所で定義されており、特に type に対して定義されており'a => 'a => 'a、これは一般に に対しても定義されていsT => sT => sTます。そのため、証明者は多くの作業を行い、 my がtype に対して定義されているsemi4唯一の場所であることを最終的に把握した後、それを使用させてくれます。+sT => sT => sT

サマリーがわかりませsemi4んが、警告が表示されないように修正できますか?

(注: 例を考えると、数学的には の*代わりに記号を使用する方が理にかなっています+が、*オーバーライドしたくない表記になります。)

二項演算子があるとし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 のチュートリアルはありません。

これは、 Isabelle のコード生成: コンテナーの抽象化レンマ? のフォローアップです。:

the_question次の理論でコードを生成したい：

問題は、 の式がsmaller抽象化関数に言及しているため、コード生成に適していないことsmallです。

私の最後の質問に対する Andreas の回答とデータの洗練に関する論文によると、次のステップは、小さな数のセットの型を導入しsmaller、その型の定義を作成することです。

smaller'実行可能になりました。私が理解していることから、上の操作を次の操作として再定義する必要がありますsmall list。small_list

の見栄えの良いコード式を定義できますthe_question。しかし、 の定義はsmall_list_all抽象化モーフィズムに言及しているため、コード生成には適していませんsmall。small_list_all実行可能にする方法を教えてください。

a_pred(問題は実際に再帰的な のコード方程式で実際に発生するため、のコード方程式を展開できないことに注意してくださいa_pred。また、実行時に不変条件を再チェックすることを含むハックを避けたいと思います。)