Isabelleに入門した

κeenです。連休中にIsabelleを少しばかり触ったのでその時のまとめを。

Isabelleって?

公式。定理証明支援系の一つ。SML処理系の1つ、Poly/MLで書かれている。 どうやらHOL(Higher Order Logic)に焦点を当てているようだが詳しいことは分かっていない。

あと、Linuxが正式にはGNU/LinuxというようにIsabelleもIsabelle/Isar/HOLと言うべきらしいが、まだよく分かっていない。

インストール

公式サイトからダウンロード出来るが、後述のProofGeneralの関係上Isabelle2014をインストールする。

エディタ設定

ProofGeneralを使う。恐らくGitHub版を使った方がいい。設定は1行

(load (expand-file-name "/path/to/ProofGeneral/generic/proof-site") nil t)

と書くだけ。多分prettify-symbol-modeも自動でonになる。(なってなかったらなんか適当に設定しておこう。global-prettify-symbols-modeとかで。) Isabelleの古いドキュメントを見てるとX-Symbolsモードなるものが出てくるが、恐らく現在のprettify-symbol-modeだと思う。

はじめる

このチュートリアルを進めている。まだ途中。タクティックもtactic_indautoしか知らない。

とりあえず拡張子は.thyにしとくとEmacsが認識してくれる。

所感

Coqを触ったことあるとそれなりにスムーズに入れた。ただしダブルクォートはキモい。 Coqも3つくらいの言語が混ってるらしいのでその内のGallinaの部分をクォートで囲っている感じなのだろうか。 クォートの部分はHOLがどうのこうの言ってた気がする。

まだどんなことが出来るのか分からないのでCoqの方がマシじゃんという感想しかない。

困ったところ

チュートリアル中に数学記号が出てくる。∀とか∃とか¬とか。断りもなしにソースコード中にも。 最初、組版の都合上置き換えたのだろうとCoqのようにforall, exists, notと打っていたがエラーになった。じゃあ、とユニコードで打ってみてもエラーになった。 結局、TeXのようにコマンドを入力するとWYSIWYGのようにシンボルになるらしい。 さらにややこしいことにEmacsに特定のシーケンスでキーを入力するとそのコマンドを挿入してくれる機能がついている。

とりあえず今のところ分かっているものをまとめる

見た目 Emacsでの入力 実際のタグ
\forall <forall>
\exists <exists>
¬ \not <not>
\and, / <and>
\or, \/ <or>
\Rightarrow, => <Rightarrow>
\rightarrow, -> <rightarrow>
\equiv, == <equiv>
\noteq, ~= <noteq>

なんかそれっぽい記号を連ねてみたら色々出てきた。けどユニコード入力出来ないから載せれないw。

逆引きしたい。見た目からコマンドを知りたい。

なんかまとまりないけどそんな所で。頭痛い。

Written by κeen