Isabelle Tutorial その20
7.2 The Reflexive Transitive Closure
帰納的定義はパラメータを取り、集合を作るための関数とすることができます。また関係はペアの集合であることから、これも帰納的に定義できます。例として関係から反射推移閉包への写像関数を考えます。
inductive_set
rtc :: "('a * 'a) set => ('a * 'a) set" ("_*" [1000] 999)
for r :: "('a * 'a) set"
where
rtc_refl [iff]: "(x, x) : r*" |
rtc_step: "[| (x, y) : r; (y, z) : r* |] ==> (x, z) : r*"
定義は二つのルールからなります。反射律は明らかであり、オプションiffが付いています。二つ目のrtc_stepは、更に左側にrの関係を追加できることを表わしています。
上の定義は直感的に理解できそうですが、それでも推移律が成り立つかなど不確かな部分もあります。以降ではこの定義が、普通の方法で定義されたものと等しいことを確かめます。まず、次の補題を証明します。
lemma [intro]: "(x, y) : r ==> (x, y) : r*" by(blast intro: rtc_step)
定義の二つ目を導入規則として自動的に適用可能とすると、前提と結論の両方にrtcが含まれているため無限ループに陥る可能性がありますが、この新しい補題にはその心配がありません。そこでオプションintroを付けています。
推移律の証明には、帰納ルールrtc.inductが必要です。
[| (?x1.0, ?x2.0) : ?r*; !!x. ?P x x; !!x y z. [| (x, y) : ?r; (y, z) : ?r*; ?P y z |] ==> ?P x z |] ==> ?P ?x1.0 ?x2.0 (rtc.induct)
これは、(?x1.0, ?x2.0) : ?r*なる(?x1.0, ?x2.0)が?Pを満たすためには、帰納的定義において?Pが保存されていなければならないことを示しています。これを使用して、推移律を証明してみます。
lemma rtc_trans: "[| (x, y) : r*; (y, z) : r* |] ==> (x, z) : r*" apply(erule rtc.induct)
次のサブゴールが残りますが、残念ながらこれは証明できません。
1. !!x. (y, z) : r* ==> (x, z) : r*
eruleを使用すると、rtc.inductの最初の前提は、ゴールの最初の前提(x, y) : r*とマッチします。その結果、?Pは% u v. (u, z) : r*になり、上のサブゴールが作られます。xは結論に現れますが、yは現れていないのが問題です。そこで、次のようにゴールを変えます。
lemma rtc_trans [rule_format]: "(x, y) : r* ==> (y, z) : r* --> (x, z) : r*"
これは、次のヒューリスティクスに因ります。
(x1, ..., xn) : Rの規則帰納で証明する場合、xiを含む他の前提は-->を使用して結論に移動せよ。
帰納法に関する同じようなヒューリスティクスは9.2.1で説明します。証明が終わるとrule_formatによって-->が==>に変換されるので、元のゴールと同じ形になります。
apply(erule rtc.induct)
今回は次の二つのサブゴールが得られ、どちらも証明が可能です。
1. !!x. (x, z) : r* --> (x, z) : r*
2. !!x y za.
[| (x, y) : r; (y, za) : r*; (za, z) : r* --> (y, z) : r* |]
==> (za, z) : r* --> (x, z) : r*
apply(blast) apply(blast intro: rtc_step) done
r*が確かに反射推移閉包、つまりrを含む反射的かつ推移的な最小の関係になっていることを証明します。反射的かつ推移的な最小の関係は次のように形式化します。
inductive_set
rtc2 :: "('a * 'a) set => ('a * 'a) set"
for r :: "('a * 'a) set"
where
"(x, y) : r ==> (x, y) : rtc2 r" |
"(x, x) : rtc2 r" |
"[| (x, y) : rtc2 r; (y, z) : rtc2 r |] ==> (x, z) : rtc2 r"
そして二つの定義が等しいことは容易に証明できます。
lemma "(x, y) : rtc2 r ==> (x, y) : r*" apply(erule rtc2.induct) apply(blast) apply(blast) apply(blast intro: rtc_trans) done lemma "(x, y) : r* ==> (x, y) : rtc2 r" apply(erule rtc.induct) apply(blast intro: rtc2.intros) apply(blast intro: rtc2.intros) done
最初に反射推移閉包の定義をrtc2ではなくrtcにしたのは、rtcの定義の方が単純だからです。rtcの定義にはルールが二つしかなく、rtc_stepも推移律よりシンプルです。その結果rtc.inductもrtc2.inductよりも単純な形になっています。
Exercise 7.2.1
次の定理を証明します。
[| (x, y) : r*; (y, z) : r |] ==> (x, z) : r*
lemma [rule_format]: "(x, y) : r* ==> (y, z) : r --> (x, z) : r*" apply(erule rtc.induct) apply(blast) apply(blast intro: rtc_step) done
Exercise 7.2.2
rtc_stepをExercise 7.2.1の式に置き換えて定義したrtcを定義し、今節の証明をやり直してみます。
inductive_set
rtc :: "('a * 'a) set => ('a * 'a) set" ("_*" [1000] 999)
for r :: "('a * 'a) set"
where
rtc_refl [iff]: "(x, x) : r*" |
rtc_step: "[| (x, y) : r*; (y, z) : r |] ==> (x, z) : r*"
lemma [intro]: "(x, y) : r ==> (x, y) : r*"
by(blast intro: rtc_step)
lemma convert_rtc_step [rule_format]: "(y, z) : r* ==> (x, y) : r --> (x, z) : r*"
apply(erule rtc.induct)
apply(blast)
apply(blast intro: rtc_step)
done
lemma rtc_trans [rule_format]: "(x, y) : r* ==> (y, z) : r* --> (x, z) : r*"
apply(erule rtc.induct)
apply(simp)
apply(blast intro: convert_rtc_step)
done
inductive_set
rtc2 :: "('a * 'a) set => ('a * 'a) set"
for r :: "('a * 'a) set"
where
"(x, y) : r ==> (x, y) : rtc2 r" |
"(x, x) : rtc2 r" |
"[| (x, y) : rtc2 r; (y, z) : rtc2 r |] ==> (x, z) : rtc2 r"
lemma "(x, y) : rtc2 r ==> (x, y) : r*"
apply(erule rtc2.induct)
apply(blast)
apply(blast)
apply(blast intro: rtc_trans)
done
lemma "(x, y) : r* ==> (x, y) : rtc2 r"
apply(erule rtc.induct)
apply(blast intro: rtc2.intros)
apply(blast intro: rtc2.intros)
done
7.3 Advanced Inductive Definitions
帰納的定義の更なる表現方法とその使い方を見ていきます。
7.3.1 Universal Quantifiers in Introduction Rules
この節では基礎項の理論を作っていきます。基礎項とは定数と関数からなり、変数はありません。また簡単にするため、ここでは定数を引数が0個の関数とします。データ型gtermを、関数の型を引数として定義します。
datatype 'f gterm = Apply 'f "'f gterm list"
例として整数定数、一引数のマイナス記号、そして加算を定義してみます。
datatype integer_op = Number int | UnaryMinus | Plus
integer_op gtermはこのシンボル上の基礎項を表わします。
型構成子gtermは、集合上の関数に一般化できます。例えば、有限集合{Number 2, UnaryMinus, Plus}からなる基礎項の集合といったものを表わすことができます。
この考え方は帰納的なので、帰納的に定義することができます。前提の全称限量子は、全ての引数が帰納的に定義された集合の要素、つまりF上の基礎項であることを表わしています。
inductive_set gterms :: "'f set => 'f gterm set" for F :: "'f set" where step[intro!]: "[| ALL t : set args. t : gterms F; f : F |] ==> (Apply f args) : gterms F"
関数setは、リストを集合に変換する関数です。この定義を使った証明の例として、gtermsが単調であることを証明してみます。証明はclarifyを適用した後、gtermsに関する帰納法で証明します。
lemma gterms_mono: "F <= G ==> gterms F <= gterms G" apply(clarify) apply(erule gterms.induct) apply(blast) done
それぞれのシンボルに正しい数の引数が適用されているとき、その項を適格であるといいます。適格な基礎項のみを次のように定義できます。ただし、arityは各シンボルの正しい引数の数を表わす関数です。
inductive_set
well_formed_gterm :: "('f => nat) => 'f gterm set"
for arity :: "'f => nat"
where
step[intro!]: "[| ALL t : set args. t : well_formed_gterm arity;
length args = arity f |]
==> (Apply f args) : well_formed_gterm arity"
7.3.2 Alternative Definition Using a Monotone Function
帰納的定義の中で、帰納的に定義された集合を任意の単調関数を使って参照することができます。このパワフルな使い方を見るため、上の定義の全称限量子を使った項を、関数listsを使ったものに変えてみます。lists Aは集合Aの要素のみからなるリストの集合です。
inductive_set
well_formed_gterm' :: "('f => nat) => 'f gterm set"
for arity :: "'f => nat"
where
step[intro!]: "[| args : lists (well_formed_gterm' arity);
length args = arity f |]
==> (Apply f args) : well_formed_gterm' arity"
monos lists_mono
関数listsが単調であることを示すために、lists_monoを参照しています。*1
なぜ使用する関数は単調でなければならないのでしょうか。帰納的定義は構築の繰り返しを表わしており、その要素は導入規則を有限回適用した結果です。帰納的定義の中での要素の参照はポジティブでなければなりません。帰納ルールの適用によって前の適用結果を打ち消すことはできません。例えば偶数集合を次のように定義することはできません。
0 : even n ~= even ==> Suc n : even
この規則では、この集合が偶数集合であることが自明であるとは言えません。
関数listsを使用していますが、先ほどの導入規則の中での参照はポジティブと言えます。
args : lists (well_formed_gterm' arity)
この規則を適用しようとすると、先に作られた基礎項のみからリストargsを作り、新しい基礎項Apply f argsが得られます。listsが単調であることから、この新しい項を使った規則の適用も正しいことが保証されます。
7.3.3 A Proof of Equivalence
二つの基礎項の定義が一致することを、それぞれの方向の包含関係を証明することで確かめます。
lemma "well_formed_gterm arity <= well_formed_gterm' arity" apply(clarify) apply(erule well_formed_gterm.induct) apply(auto) done
証明は7.3.1のものと同様です。次に逆方向を見てみます。
lemma "well_formed_gterm' arity <= well_formed_gterm arity" apply(clarify) apply(erule well_formed_gterm'.induct) apply(auto) done
証明の手順はほとんど同じですが、帰納法を適用した結果のサブゴールは少し変わっています。
1. !!x args f.
[| args
: lists
(well_formed_gterm' arity Int {a. a : well_formed_gterm arity});
length args = arity f |]
==> Apply f args : well_formed_gterm arity
前提にはlistsが含まれています。このサブゴールは、listsの積集合上の分配則を使用して証明します。
listsp ((%x. x : ?A) Int (%x. x : ?B)) = (%x. x : lists ?A) Int (%x. x : lists ?B) (lists_Int_eq)
この規則により、先ほどの前提は次の二つに分かれます。
args : lists (well_formed_gterm' arity) args : lists (well_formed_gterm arity)
well_formed_gterm.stepにより残りは完了します。以上の証明手続きはautoのみで行われます。
以上は単調関数の使い方を示す典型的な例です。多くの単調関数は積集合上の分配則を満たします。特に片方向は必ず成り立ち、次の定理があります。
mono ?f ==> ?f (?A Int ?B) <= ?f ?A Int ?f ?B (mono_Int)
7.3.4 Another Example of Rule Inversion
gtermsが積集合上の分配則を満たすことを証明します。gtermsが単調であることは既に証明しているので、mono_Intから片方の包含関係は成り立ちます。逆方向について証明してみます。
lemma gterms_IntI: "t : gterms F ==> t : gterms G --> t : gterms (F Int G)"
証明しようとすると前提にApply f args : gterms Gが現れます。これは、規則の反転を使って解決します。
inductive_cases gterm_Apply_elim [elim!]: "Apply f args : gterms F"
結果は次のようになります。
[| Apply ?f ?args : gterms ?F; [| ALL t:set ?args. t : gterms ?F; ?f : ?F |] ==> ?P |] ==> ?P (gterm_Apply_elim)
このルールは前提のApply f argsをfとargsそれぞれに関するものに分けます。ループすることがないので、elim!を付けています。このルールを使って、先ほどの定理を証明できます。
lemma gterms_IntI [rule_format, intro!]: "t : gterms F ==> t : gterms G --> t : gterms (F Int G)" apply(erule gterms.induct) apply blast done
分配則は次のように証明できます。
lemma gterms_Int_eq [simp]: "gterms (F Int G) = gterms F Int gterms G" by(blast intro!: mono_Int monoI gterms_mono)
Exercise 7.3.1
関数シンボルからその型への写像関数をシグネチャといいます。関数の型を引数の型のリストと結果の方のペアとして、型整合な項のみの集合を定義します。
inductive_set
well_typed_gterm :: "('f => 't list * 't) => ('f gterm * 't) set"
for sig :: "('f => 't list * 't)"
where
step[intro!]: "[| ts : lists (well_typed_gterm sig);
args = (map fst) ts;
sig f = (map snd ts, rtype) |]
==> ((Apply f args), rtype) : well_typed_gterm sig"
*1:この定理はデフォルトで組み込まれているため、指定する必要はありません。ここではmonosの使い方を見るために記述しました。
