Isabelle Tutorial その1

1. The Basics

1.1 Introduction

Isabelleは汎用的な証明支援器であり、高階論理に特化させたものがIsabelle/HOLです。私は数学屋さんではないので、高階論理って何？とかは深く考えず進みます。

1.2 Theories

Isabelleを使用して理論を構築していきます。理論とは、型、関数、定理の集まりです。理論Tを定義するには次のように書きます。

theory T
imports B₁, ..., B_n
begin
	宣言、定義、証明などなど
end

B₁, ..., B_nは既存の理論で、Tをこれらの上に構築していきます。オブジェクト指向プログラムのクラスの継承みないなものです。名前が衝突する場合は、T.fやB.fなどと書いて回避します。ファイル名はT.thyとします。

既存の理論ファイルは次のページで探すことができますし、Isabelleをインストールしたディレクトリのsrc/HOL/の下にもあります。

http://isabelle.in.tum.de/library/HOL/

1.3 Types, Terms and Formulae

HOLはMLはHaskellのような型システムを持つ型付き論理であり、boolやnatなどの型があります。listやsetなどの型構成子もあり、nat listは自然数のリスト型です。関数型は=>を使用します。T₁ => T₂ => T₃はT₁ => (T₂ => T₃)ですし、[T₁, ..., T_n] => TはT₁ => ... => T_n => Tの略です。'aは型変数を意味し、多相型のを表すのに使用します。

項も関数型プログラムとだいたい同じです。HOLは+のような中置記法の関数や、条件式を扱うことができます。

if b then t₁ else t₂ - いわゆるif式です。
let x = t in u - いわゆるlet式です。
case e of c₁ => e₁ | ... | c_n => e_n - いわゆるcase式です。

lambda式も扱えます。例えば% x. x + 1と書くことができます。

式(formulaを式と訳していいのかな？)はbool型の項です。True, False, ~(否定), &(論理積), |(論理和), -->(含意)などが使えます。等式は関数=を使います。=の型は'a => 'a => boolです。

限量子はALL x. P xやEX x. P xなどと書きます。EX! x. P xはPを満たす唯一の値があるという意味です。

多くの場合は型推論が働きますが、型を明示しなければならないときもあります。型はt::Tというように書きます。::は優先度が低いので、普段から(t::T)と括弧でくくる方がいいと思います。

他にも気を付けたいことを幾つか列挙します。

fが1引数の関数ならば、f t uはf (t u)ではなく(f t) uと解釈されます。
Isabelleは+のような中置関数も使えますが、前置記法の方が優先度が高いため、f x + yはf(x + y)ではなく(f x) + yと解釈されます。
~~=の優先度は低いため、~~P = Pは~~(P = P)と解釈されます。~~HOLではiffは等式で表します。一般的にiffの優先度は低いですが、=は高いです。よって~~P = Pは~~(P = P)と解釈されます。
if, let, case, lambda, 限量子なども優先度が低いので、括弧でくくる方がよいでしょう。
% x. xやALL x. x=xと書く時は、ドットの後ろにスペースを入れましょう。
識別子には先頭以外ならば_や'が使えます。

Proof Generalのオプションで、型や括弧を表示することもできます。