Isabelle Tutorial その5
2.6 Some Basic Types
2.6.1 Natural Numbers
自然数を表す型natは構成子0とSucで定義されています。case式を使った例を示します。
case n of 0 => 0 | Suc m => m
primrec sum :: "nat => nat" where "sum 0 = 0" | "sum (Suc n) = Suc n + sum n" lemma "sum n + sum n = n * (Suc n)" apply(induct_tac n) apply(auto) done
+, -, *, div, mod, min, max, <=, <などが定義されています。最小値演算LEASTも定義されています。例えば(LEAST n. 0 < n) = Suc 0です。
定数0や1、演算子+, -, <などはオーバーロードされています。よって、単にx + 0 = xと書いても型が決まりません。必要に応じてx + 0 = (x::nat)と書く必要があります。Sucはオーバーロードされていないため、自然数であると型推論することができます。
メソッドautoとsimp(後から登場します)は簡単な計算を解くことができます。
lemma "[| ~ m < n ; m < n + (1::nat) |] ==> m = n"
ただし限量子、多くの論理結合子、加算以外の算術演算子は解けません。よって次の補題をautoまたはsimpで解くことはできません*1。
lemma "m ~= (n::nat) ==> m < n | n < m"
メソッドarithは最初のサブゴールをlinear arithmetic formulaとして証明をしようとします。linear arithmetic formulaには通常の論理結合子、関係=, <, <=, そして演算子+, -, min, maxが含まれます。
例えば次の証明はk * kをアトミックに扱えるため、arithで証明できます。
lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))" apply(arith)
しかし次の証明は乗算の性質が必要なため、arithを使うことができません。
lemma "n*n = n+1 ==> n=0"
2.6.2 Pairs
HOLには順序付きペアもあります。関数fstとsndはそれぞれペアの一つ目と二つ目を取り出す関数です。タプルはネストしたペアで表し、(a1, a2, a3)は(a1, (a2, a3))を表します。
unitは一つの値()のみを値として持つ型です。これは0要素の積と見ることができます。また、積はデータ型であり、induct_tacやcase_tacを使って分解することができます。
2.6.3 Datatype option
オプション型は以下のように定義されています。
datatype 'a option = None | Some 'a
例えば計算結果として、エラーが発生した場合はNone、値を返す場合はSome vで表すなどの使い方ができます。もちろんそのために新しいデータ型を定義することもできますが、optionを使った方がシンプルに表わせます。
2.7 Definitions
既にある構文に別名を付けることができます。
2.7.1 Type Synonyms
typesコマンドを使用して型に別名を付けることができます。
types number = nat
gate = "bool => bool => bool"
('a, 'b) alist = "('a * 'b) list"
これは理論を読みやすくするために使います。Isabelleの出力では元の型に展開されます。
2.8 The Definitional Approach
例えばf(n) = f(n) + 1といった公理を導入すると、簡単に矛盾を導きだすことができます。このような危険を回避するため、公理を使ったアプローチよりも定義を使ったアプローチを推奨しており、Isabelleはそのための便利なコマンドを用意し、内部でうまく処理しています。が、一般的なユーザは内部の動作まで気にする必要はないでしょう。
