Isabelle Tutorial その3
2. Functional Programming in HOL
ここからはHOLでどのように関数プログラムを書き、どのように検証するのか見ていきます。Isabelle/HOLを使う目的はシステムをモデル化し検証することなので、関数を実行可能なかたちで定義する必要はないのですが、まずは実行可能な定義を書くことにします。ただし、HOLでは必ず全域的でなければならないことに注意してください。
2.1 An Introductory Theory
MLやHaskellと同じようにデータ型と関数を定義することができます。簡単なリストを定義しながら、方法を一つ一つ見ていきます。
theory ToyList imports Datatype begin
HOLには既にリストが定義されています。多くの場合Mainをインポートしますが、定義済みのリストもインポートしてしまうため、ここではDatatypeをインポートしています。次にデータ型を定義します。
datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65)
データ型listは二つの構成子NilとConsから成っています。Nilは空のリストであり、Consはリストの前に要素を一つ加える演算子です。例えばCons True (Cons False Nil)はbool list型の値です。それぞれの構成子に対して別表記も同時に定義しています。Nilの代わりに[]と、Cons x xsの代わりにx # xsと書けます。infixrは#が右結合であることを意味し、65は結合順位を表します。
次に二つの関数appとrevを定義します。
primrec app :: "’a list => ’a list => ’a list" (infixr "@" 65) where "[] @ ys = ys" | "(x # xs) @ ys = x # (xs @ ys)" primrec rev :: "’a list => ’a list" where "rev [] = []" | "rev (x # xs) = (rev xs) @ (x # [])"
primrecは原始再帰関数を定義します。appは二つのリストの連結、revは逆順のリストを返す関数です。定義は次の形になっています。
primrec 名前 :: 型 (オプション) where 等式 | ... | 等式
