Isabelle Tutorial その24

Isabelle

8.5 Introducing New Types

多くの場合は定義済みの型boolや=>とそれらの組み合わせで事が足りますが、稀にこれらでは表わせない高度な型が必要になる場合があります。そのような場合に必要となる型の導入方法を紹介します。

8.5.1 Declaring New Types

typedeclは詳細を定義する事なく新たな型の名前を宣言します。これは6.6の例で既に見ました。

typedecl my_new_type

関係する型に型パラメータを導入することで、typedeclによる型宣言は除去する事ができます。どちらを使っても本質的な違いはなく、違いは読みやすさのみです。

宣言した型にプロパティを付けたい場合は、公理として宣言する事ができます。

axioms just_one: "EX x::my_new_type. ALL y. x = y"

しかし、この方法は矛盾する公理を宣言する可能性があるため推奨はしません。

8.5.2 Defining New Types

より汎用的で安全な型の定義するにはtypedefを使います。datatypeを始めとする、他の型の定義手段はすべてtypedefに基づいています。簡単に言うと、既にある型の要素の部分集合を値とする新たな型を定義する事ができます。

例として、三つの値を持つ型を定義してみます。要素は自然数の最初の三つの値を使って表わします。

typedef three = "{0::nat, 1, 2}"

HOLの型は非空でなければならないため、少なくとも一つはその要素がある事を保証しなければなりません。typedefはこの制限の証明を要求してきます。今回の例の場合、この制限を満たす事は自明です。

 1. EX x. x : {0, 1, 2}

apply(rule_tac x = 0 in exI)
by simp

この型定義によって新たな型threeが導入されます。さらにその値は、集合{0, 1, 2}と1対1の関係です。これを表わすために、次の定数が同時に定義されます。

three :: nat set
Rep_three :: three => nat
Abs_three :: nat => three

また定数threeも定義されます。

three == {0, 1, 2}　　　　(three_def)

最後に、typedefはRep_threeが全射であり、Abs_threeとRep_threeが逆関係になっていることを明示します。

Rep_three ?x : three　　　　　　　　　　　　　　　　(Rep_three)
Abs_three (Rep_three ?x) = ?x　　　　　　　　　　　 (Rep_three_inverse)
?y : three ==> Rep_three (Abs_three ?y) = ?y　　　　(Abs_three_inverse)

次のステップは、この新しい型に対する基本的な関数を定義する事です。どのような関数を用意するかは定義する型に因りますが、次のような戦略をとると良いでしょう。

  • 他のすべての関数を表わすのに十分、かつできるだけ少ない基本関数のみを定義せよ。
  • 二つのレベルを行き来するために、AbsとRepを使って表わした型を表現するための関数を定義せよ。

今回の例では、threeの三つの要素それぞれに名前を定義すれば十分です。

definition A :: three where "A == Abs_three 0"
definition B :: three where "B == Abs_three 1"
definition C :: three where "C == Abs_three 2"

型threeを毎回natに変換していては大変です。そこでA、BそしてCのみで書かれたthreeに関する十分な定理を用意し、抽象レベルを上げる必要があります。簡単な例として、A、B、Cがすべて異なり、かつそれが型の要素のすべてである事を証明します。

Isabelleは予めいくつかの役立つ補題を用意しています。最初の二つはRep_threeとAbs_threeが単射である事を表わしています。

(Rep_three ?x = Rep_three ?y) = (?x = ?y)　　　　　　　　　　　　　　　　　　　　 (Rep_three_inject)
[| ?x : three; ?y : three |] ==> (Abs_three ?x = Abs_three ?y) = (?x = ?y)　　　　(Abs_three_inject)

次の定理はx::threeをAbs_three(y::nat)に、またyをRep_three xに置き換えます。

[| ?y : three; !!x. ?y = Rep_three x ==> ?P |] ==> ?P　　　　 (Rep_three_cases)
(!!y. [| ?x = Abs_three y; y : three |] ==> ?P) ==> ?P　　　　(Abs_three_cases)
[| ?y : three; !!x. ?P (Rep_three x) |] ==> ?P ?y　　　　　　 (Rep_three_induct)
(!!y. y : three ==> ?P (Abs_three y)) ==> ?P ?x　　　　　　　 (Abs_three_induct)

A、B、Cがすべて異なることの証明は、それぞれの定義を展開し、さらにAbs_threeが単射である事を用いて証明できます。

lemma "A ~= B & B ~= A & A ~= C & C ~= A & B ~= C & C ~= B"
by(simp add: Abs_three_inject A_def B_def C_def three_def)

A、B、Cが型の要素のすべてである事は、場合分けルールとして表わすのが良いでしょう。

lemma three_cases: "[| P A; P B; P C |] ==> P x"

証明は帰納法を使用して進めます。

apply(induct_tac x)

 1. !!y. [| P A; P B; P C; y : three |] ==> P (Abs_three y)

three_defによってy = 0 | y = 1 | y = 2が導かれ、場合分けするとそれぞれのサブゴールは自明になります。

apply(auto simp add: three_def A_def B_def C_def)
done

ところで、今回の例は次の一行で代用できます。

datatype better_three = A | B | C

実際、datatypeはおおよそ上の例と同じようなことを内部で行います。