二項演算子があるとしf :: "sT => sT => sT"ます。fWiki でここに示されている、クライン 4 グループの 4x4 乗法テーブルを実装するように定義したいと思います。
http://en.wikipedia.org/wiki/Klein_four-group
ここで試みているのは、16 エントリのテーブルを作成することだけです。まず、次のように 4 つの定数を定義します。
consts
k_1::sT
k_a::sT
k_b::sT
k_ab::sT
次に、テーブル内の 16 エントリを実装する関数を定義します。
k_1 * k_1 = k_1
k_1 * k_a = k_a
...
k_ab * k_ab = k_1
私は Isar で通常のようなプログラミングを行う方法を知りません。Isabelle ユーザーのリストで、(特定の) プログラミングのような構造が言語で意図的に強調されていないと言われているのを見たことがあります。
先日、単純な不自然な関数を作成しようとしましたがif, then, else、ソース ファイルでの使用を見つけた後、 isar-ref.pdfでそれらのコマンドへの参照を見つけることができませんでした。
チュートリアルを見るdefinitionと、簡単な方法で関数を定義することがわかります。それ以外は、 を必要とする再帰関数と帰納関数に関する情報しか表示されずdatatype、私の状況はそれよりも単純です。
私自身のデバイスに任せた場合、datatype上記の 4 つの定数に対して a を定義してから、いくつかの変換関数を作成して、2 項演算子f :: sT => sT => sT. を使おうとして少しいじりましfunたが、単純な取引ではありませんでした。
私は少し実験をfun行いましたinductive
更新：プログラミングと証明が答えを見つける場所であるというコメントに応えて、ここにいくつかの資料を追加します。理想的な Stackoverflow 形式から外れているようです。
私はいくつかの基本的な実験を行いました。主にfunだけでなく、 も使用しましinductiveた。私は誘導をかなり早くあきらめました。簡単な例から得たエラーのタイプは次のとおりです。
consts
k1::sT
inductive k4gI :: "sT => sT => sT" where
"k4gI k1 k1 = k1"
--"OUTPUT ERROR:"
--{*Proofs for inductive predicate(s) "k4gI"
Ill-formed introduction rule ""
((k4gI k1 k1) = k1)
Conclusion of introduction rule must be an inductive predicate
*}
私の掛け算九九は帰納的ではないので、それをinductive追うのに時間を費やすべきだとは思いませんでした.
ここでは「パターン マッチング」が重要なアイデアのように思われるので、 を試してみましfunた。fun以下は、標準の関数型のみを使用しようとしている、本当にめちゃくちゃなコードです。
consts
k1::sT
fun k4gF :: "sT => sT => sT" where
"k4gF k1 k1 = k1"
--"OUTPUT ERROR:"
--"Malformed definition:
Non-constructor pattern not allowed in sequential mode.
((k4gF k1 k1) = k1)"
その種のエラーが発生しました。プログラミングと証明で次のようなことを読みました。
「再帰関数は、データ型コンストラクターに対するパターン マッチングによって楽しく定義されます。
これらすべてが、初心者にfun必要な印象を与えますdatatype。その兄貴分まではfunction、私はそれについて知りません。
ここにあるようです。必要なのは、16 の基本ケースを持つ再帰関数だけであり、それが乗算表を定義します。
function答えは？
この質問を編集する際に、私functionは過去を思い出しましたfunction。
consts
k1::sT
function k4gF :: "sT => sT => sT" where
"k4gF k1 k1 = k1"
try
try の出力は、証明できることを示しています (更新: 実際には、証明ステップの 1 つだけを証明できることを示していると思います)。
Trying "solve_direct", "quickcheck", "try0", "sledgehammer", and "nitpick"...
Timestamp: 00:47:27.
solve_direct: (((k1, k1) = (k1, k1)) ⟹ (k1 = k1)) can be solved directly with
HOL.arg_cong: ((?x = ?y) ⟹ ((?f ?x) = (?f ?y))) [name "HOL.arg_cong", kind "lemma"]
HOL.refl: (?t = ?t) [name "HOL.refl"]
MFZ.HOL⇣'eq⇣'is⇣'reflexive: (?r = ?r) [name "MFZ.HOL⇣'eq⇣'is⇣'reflexive", kind "theorem"]
MFZ.HOL_eq_is_reflexive: (?r = ?r) [name "MFZ.HOL_eq_is_reflexive", kind "lemma"]
Product_Type.Pair_inject:
(⟦((?a, ?b) = (?a', ?b')); (⟦(?a = ?a'); (?b = ?b')⟧ ⟹ ?R)⟧ ⟹ ?R)
[name "Product_Type.Pair_inject", kind "lemma"]
それが何を意味するのかわかりません。私が知ってfunctionいるのは、矛盾を証明しようとしているからです。私はそれがそれほど文句を言わないことを知っているだけです。このfunctionように乗算表を定義する方法を使用する場合、私は満足しています。
それでも、私は議論型なのでfunction、チュートリアルで学びませんでした. 数か月前にリファレンス マニュアルでそれについて学びましたが、その使用方法についてはまだよくわかりません。
私はfunctionで証明した を持っていautoますが、幸いなことに機能はおそらく良くありません。functionそれはの謎に追加されます。Defining Recursive Functions in Isabelle/HOLfunctionに情報があり、 と を比較しています。funfunction
ただし、 or のような再帰的なデータ型を使用しない or の例は見たことがありませfunん。よく見ていなかったのかもしれません。functionnat'a list
冗長で申し訳ありませんが、これは直接的な質問にはなりませんが、A から B に人を直接連れて行く Isabelle のチュートリアルはありません。