Isabelle/Isar（その１）

　Isabelle/HOLはHOLのラッパーですが，HOLにはない「推論規則による（危うげな部分も含む）マッチング」が特徴です．ただしかつてのapply-doneによるタクティック列挙の証明は，現在は構造化された言語Isar上でのエミュレーションとなっており，証明のスタイルは，システムが生成するサブゴールを人間が復唱したのち逐次証明する，悪く言えば迂遠，良く言えば修正が容易で読み易い？もの（Isar＝Isabelle/HOL上のMisarではなく，Intelligible semi-automated reasoning．http://isabelle.in.tum.de/Isar/）に移行，結果として多様な証明が書けるシステムとなっています．
　apply-doneスタイルの証明についてはチュートリアルの翻訳（http://d.hatena.ne.jp/caeruiro/20100314/1268569131）がありますので，ここではIsarの特徴的な部分を中心に述べて行きます
　まずは，インストールスクリプト（for Linux）．次を端末にコピー＆ペーストしてください．

cd ~
echo "export Z3_NON_COMMERCIAL=yes
export ISABELLE_CSDP=/usr/bin/csdp
export PATH=$PATH:~/Isabelle2013/bin/" > ~/.bashrc
source ~/.bashrc
sudo apt-get update
sudo apt-get install coinor-csdp
wget http://isabelle.in.tum.de/dist/Isabelle2013_linux.tar.gz
tar -xzf ~/Isabelle2013_linux.tar.gz

ユーザーホームディレクトリにIsabelle2013というイザベルホームディレクトリが出来，準備完了です．あとは

isabelle jedit

とすれば

のように初回起動時にPUREとHOLロジックのイメージが生成された後に，jeditが立ち上がります．メニューを日本語にするにはC+F12でオプションを表示，Generalにある言語で日本語を選択（反映には再起動），フォントはText-Areaで調整できます．


インターフェイスとしては他に，レスポンス抜群のtty

お約束のemacs/Proof-General

があり，後者は

のように入力直後のコマンドが通るか自動的に判定させることもできますが．．．jeditはその上を行く「自動評価環境」です．


すなわち，カーソル行に対するシステムの出力が自動的に表示されるため，評価を指示するキー操作は全く不要，人間は証明を書き続けるのみです（jeditの頑張り具合はプラグインメニューのIsabelleにあるMonitor panelで確認できます）．

　なお，Windowsへのインストールは，http://isabelle.in.tum.de/dist/Isabelle2013.exeをダウンロード，実行するとデスクトップにIsabelle2013というイザベラホームディレクトリと，jdeitへのリンクが出来るのでクリックすれば，初回のみ

のようにイメージが生成された後に，jeditが立ち上がります．