Isabelle Tutorial その16
6. Sets, Functions and Relations
この章では集合、関数、関係を見ていきます。集合は、例えば言語理論や計算理論、状態遷移機械など計算機科学における形式化にも有用です。Isabelleは、集合計算が含まれる多くの式も自動証明します。
このドキュメントで全ての定理を紹介することはできません。幾つかの重要な定理のみを紹介していきます。
6.1 Sets
HOLの集合は型付きです。集合に含まれる要素は全て同じ型であり、この型をtとすると、集合自身の型はt setとなります。
まず、積集合、和集合、補集合から見ていきます。次に、帰属関係とその否定も見ていきます。
積集合に関する推論規則を見てみます。*1
[|?c : ?A; ?c : ?B|] ==> ?c : ?A Int ?B (IntI) ?c : ?A Int ?B ==> ?c : ?A (IntD1) ?c : ?A Int ?B ==> ?c : ?B (IntD2)
次は、補集合に関する定理です。
(?c : - ?A) ==> (?c ~: ?A) (Compl_iff) - (?A Un ?B) ==> - ?A Int - ?B (Compl_Un)
集合の差は、その集合と別の集合の補集合との積で表わせます。ここでは、空集合と全体集合も登場します。
?A Int (?B - ?A) = {} (Diff_disjoint)
?A Un - ?A = UNIV (Compl_partision)
部分集合の定義を見ます。
(!!x. x : ?A ==> x : ?B) ==> ?A <= ?B (subsetI) [|?A <= ?B; ?c : ?A|] ==> ?c : ?B (subsetD)
blastを使用すると次のような定理を証明することができます。
(?A Un ?B <= ?C) = (?A <= ?C & ?B <= ?C) (Un_subset_iff)
自動証明可能な別の例を見てみます。
lemma "(A <= - B) = (B <= - A)" by blast
演算子<=は様々な型にオーバーロードされているため、この式は型が定まらず証明できません。型が集合であることを指定すると、この式は証明できます。
lemma "((A::'a set) <= - B) = (B <= - A)"
二つの集合が同じ要素を持っているならば、その集合は等しいです。外延的同値は次の定理で表わされます。
(!! x. (x : ?A) = (x : ?B)) ==> ?A = ?B (set_ext)
次の定理は集合の同値関係を二つの方向に分けます。
[|?A <= ?B; ?B <= ?A|] ==> ?A = ?B (equalityI) [|?A = ?B; [|?A <= ?B; ?B <= ?A|] ==> ?P|] ==> ?P (equalityE)
6.1.1 Finite Set Notation
有限集合はinsertで表わせます。
insert ?a ?A = {?a} Un ?A (insert_is_Un)
有限集合{a, b}はinsert a (insert b {})の略記です。有限集合に関する多くのことが自動的に証明できます。
lemma "{a, b} Un {c, d} = {a, b, c, d}"
by blast
ただし、想像通りにはいかない場合もあります。次の証明を見てみます。
lemma "{a, b} Int {b, c} = {b}"
apply auto
証明は失敗し、b = cがサブゴールとして残ります*2。これは、変数は全て異なるという前提をおいていないためです。次のようにすると証明できます。
lemma "{a, b} Int {b, c} = (if a = c then {a, b} else {b})"
apply simp
by blast
blastはif式を場合分けできないため、先にsimpで場合分けしてからblastを使用しました。autoやforceならば1ステップで証明が可能です。
6.1.2 Set Comprehension
集合の内包表現{x. P}はPを満たすxから成る集合を表わします。次の二つの定理は集合の内包表現と帰属関係との関係を表わします。
(?a : {x. ?P x}) = ?P ?a (mem_Collect_eq)
{x. x : ?A} = ?A (Collect_mem_eq)
これらの定理によって次が証明できます。
lemma "{x. P x | x : A} = {x. P x} Un A"
lemma "{x. P x --> Q x} = - {x. P x} Un {x. Q x}"
Isabelleでは次の例のように、さらに汎用的な内包表現の記述ができます。
lemma "{p * q | p q. p : prime & q : prime} =
{z. EX p q. z = p * q & p : prime & q : prime}"
右辺は左辺の単なる略記です。
6.1.3 Binding Operators
集合を値域として全称限量や存在限量を使用できます。全称限量に対する推論規則は次のようになります。
(!! x. x : ?A ==> ?P x) ==> ALL x : ?A. ?P x (ballI) [|ALL x : ?A. ?P x; ?x : ?A|] ==> ?P ?x (bspec)
同様に、存在限量に対する推論規則は次のようになります。
[|?P ?x; ?x : ?A|] ==> EX x : ?A. ?P x (bexI) [|EX x : ?A. ?P x; !!x. [|x : ?A; ?P x|] ==> ?Q|] ==> ?Q (bexE)
和集合も与えられた集合上に使用できます。UN x : A. Bと記述でき、次の定義が成り立ちます。
[|?a : ?A; ?b : ?B ?a|] ==> ?b : (UN x : ?A. ?B x) (UN_I) [|?b : (UN x : ?A. ?B x); !!x. [|x : ?A; ?b : ?B x|] ==> ?R|] ==> ?R (UN_E)
集合の集合の和をUnion Cと書くこともできます。
(?A : Union ?C) = (EX X : ?C. ?A : X) (Union_iff)
積集合も同様に使用でき、INT x : A. BやInter Cと書きます。
(?b : (INT x : ?A. ?B x)) = (ALL x : ?A. ?b : ?B x) (INT_iff) (?A : Inter ?C) = (ALL X : ?C. ?A : X) (Inter_iff)
内包表現の内部表現にはCollectが使われており、証明のゴールなどにこれが現れることがあります。例えばCollect Pは{x. P x}と同じです。限量子に対しても同様で、All PはALL x. P xと、Ex PはEX x. P xと、Ball A PはALL x : A. P xと、Bex A PはEX x : A. P xと同じです。また、EpsはSOME x. P xはと同じです。
6.1.4 Finiteness and Cardinality
述語finiteは有限集合かどうかを表わします。Isabelle/HOLには有限性と濃度(card)に関する多くの定理があります。
[|finite ?A; finite ?B|] ==> card ?A + card ?B = card (?A Un ?B) + card (?A Int ?B) (card_Un_Int) finite ?A ==> card (Pow ?A) = 2 ^ card ?A (card_Pow)
6.2 Functions
6.2.1 Function Basics
二つの関数が等しいとは、同じ引数に対して同じ値を返す場合です。これを関数の外延的同値といいます。
(!! x. ?f x = ?g x) ==> ?f = ?g (ext)
関数の更新は状態機械のモデリングに便利です。更新に関する多くの定理がありますが、特に次の単純化ルールをが定義されています。
(?f(?x := ?y)) ?z = (if ?z = ?x then ?y else ?f ?z) (fun_upd_apply)
二つ、あるいはそれ以上の連続する更新の略記が、次の定理の左辺に現れています。
?f(?x := ?y, ?x := ?z) = ?f(?x := ?z) (fun_upd_upd)
恒等関数と合成も定義されています。
id = (% x. x) (id_def) ?f o ?g = (% x. ?f (?g x)) (o_def)
恒等関数と合成に関しても多くの定理があります。例として合成の結合律を示します。
?f o (?g o ?h) = ?f o ?g o ?h (o_assoc)
6.2.2 Injections, Surjections, Bijections
inj_on ?f ?A == ALL x : ?A. ALL y : ?A. ?f x = ?f y --> x = y (inj_on_def) surj ?f == ALL y. EX x. y = ?f x (surj_def) bij ?f == inj ?f & surj ?f (bij_def)
inj_onの第二引数は、関数がその集合の上で単射であることを表わしています。また、inj fはinj_on f UNIVの略記です。
invは逆関数を表わします。invに関する定理を幾つか示します。
inj ?f ==> inv ?f (?f ?x) = ?x (inv_f_f) surj ?f ==> ?f (inv ?f ?y) = ?y (surj_f_inv_f) bij ?f ==> inv (inv ?f) = ?f (inv_inv_eq)
これらを含む式の証明は難しいです。次の例は簡単そうですが、自動証明はできません。
lemma "inj f ==> (f o g = f o h) = (g = h)" apply(simp add: expand_fun_eq inj_on_def) apply(auto) done
証明には次の定理が必要です。
(?f = ?g) = (ALL x. ?f x = ?g x) (expand_fun_eq)
証明の最初のステップは関数の外延的同値、単射及び合成の定義を使用しています。
6.2.3 Function Image
関数による集合の像は非常に便利な概念であり、次のように定義されています。
?f ` ?A = {y. EX x : ?A. y = ?f x} (image_def)
像に関する定理を幾つか示します。
(?f o ?g) ` ?r = ?f ` ?g ` ?r (image_compose) ?f ` (?A Un ?B) = ?f ` ?A Un ?f ` ?B (image_Un) inj ?f ==> ?f ` (?A Int ?B) = ?f ` ?A Int ?f ` ?B (image_Int)
像を含む式は自動証明できるかもしれません。例えば次の補題は自動証明可能です。
lemma "f ` A Un g ` A = (UN x : A. {f x, g x})"
lemma "f ` {(x, y). P x y} = {f (x, y) | x y. P x y}"
値域は、その関数が取り得る値の集合であり、全体集合の像と見ることもできます。定数rangeは定義されておらず、代わりにrangeはUNIVの像の略記として定義されています。
range ?f == ?f ` UNIV
rangeに対する定理もありますが、多くの場合、像の定理を使用する方が良いと思います。
逆像は次のように定義されています。
?f -` ?B == {x. ?f x : ?B} (vimage_def)
最後に、逆像に関する定理の例を示します。
?f -` (- ?A) = - ?f -` ?A (vimage_Compl)
6.3 Relations
関係はペアの集合です。よって集合に関する演算子がそのまま使用できます。さらに、関係のための演算子も用意されています。
6.3.1 Relation Basics
恒等関係は次のように定義されています。
Id == {p. EX x. p = (x, x)} (Id_def)
関係の合成もあります。
?r O ?s == {(x, z). EX y. (x, y) : ?r & (y, z) : ?s} (rel_comp_def)
恒等関係と合成に関して次の定理があります。
?R O Id = ?R (R_O_Id)
合成は単調であり、例えば次のような定理があります。
[| ?r' <= ?r; ?s' <= ?s |] ==> ?r' O ?s' <= ?r O ?s (rel_comp_mono)
関係の逆は二つのオペランドを入れ替えます。
((?a, ?b) : ?r^-1) = ((?b, ?a) : ?r) (converse_iff)
次は逆関係と合成に関する代表的な定理です。
(?r O ?s)^-1 = ?s^-1 O ?r^-1 (converse_rel_comp)
関係による集合の像は関数の場合と同じように定義されています。
(?b : ?r `` ?A) = (EX x : ?A. (x, ?b) : ?r) (Image_iff)
関係の定義域と値域は一般的な方法で定義されています。
(?a : Domain ?r) = (EX y. (?a, y) : ?r) (Domain_iff) (?a : Range ?r) = (EX y. (y, ?a) : ?r) (Range_iff)
関係の合成の繰り返しも定義されており、^を使用します。
6.3.2 The Reflexive and Transitive Closure
関係rの反射推移閉包はr^*と書きます。
?r^* = Id Un ?r^* O ?r (rtrancl_unfold)
導入規則となる三つの定理を示します。
(?a, ?a) : ?r^* (rtrancl_refl) ?p : ?r ==> ?p : ?r^* (r_into_rtrancl) [|(?a, ?b) : ?r^*; (?b, ?c) : ?r^*|] ==> (?a, ?c) : ?r^* (rtrancl_trans)
反射推移閉包に関する帰納ルールもあります。
[|(?a, ?b) : ?r^*; ?P ?a; !!y z. [|(?a, y) : ?r^*; (y, z) : ?r; ?P y|] ==> ?P z|] ==> ?P ?b (rtrancl_induct)
次は反射推移閉包の冪等性です。
(?r^*)^* = ?r^* (rtrancl_idemp)
推移閉包は*の代わりに+を使用します。推移閉包には二つの導入規則があります。
(?a, ?b) : ?r ==> (?a, ?b) : ?r^+ (r_into_trancl) [|(?a, ?b) : ?r^+; (?b, ?c) : ?r^+|] ==> (?a, ?c) : ?r^+ (trancl_trans)
次の定理は推移閉包と逆関係の順序を入れ替えることができることを示しています。
(?r^-1)^+ = (?r^+)^-1 (trancl_converse)
6.3.3 A Sample Proof
反射推移閉包と逆関係も順序を入れ替えることができます。ここではこれを証明してみます。それぞれの方向を別に証明することにし、一つ目は次のようになります。
lemma rtrancl_converseD: "(x, y) : ((r^-1)^*) ==> (y, x) : (r^*)" apply(erule rtrancl_induct) apply(rule rtrancl_refl) apply(blast intro: rtrancl_trans) done
最初のステップは帰納法を適用しており、次のサブゴールが残ります。
1. (x, x) : r^* 2. !!y z. [| (x, y) : (r^-1)^*; (y, z) : r^-1; (y, x) : r^* |] ==> (z, x) : r^*
一つ目は反射律そのものです。二つ目は前提の逆関係を取り除き、(z, y) : rに変換してから上の導入規則を適用することで証明できます。逆方向の証明は次のようになります。
lemma rtrancl_converseI: "(y, x) : r^* ==> (x, y) : (r^-1)^*" apply(erule rtrancl_induct) apply(rule rtrancl_refl) apply(blast intro: rtrancl_trans) done
最後に、二つの補題を繋ぎます。
lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1" by(auto intro: rtrancl_converseI dest: rtrancl_converseD)
この証明はblastではうまくいきません。証明の過程で、次のサブゴールが現れます。
1. !!x. x : (r^-1)^* ==> x : (r^*)^-1
xが変数でありペアではないため、このサブゴールにrtrancl_converseDを適用できません。simpやblastではこれ以上先へ進めませんが、clarifyを使用すると次のようになります。
1. !!a b. (a, b) : (r^-1)^* ==> (b, a) : r^*
xがペア(a, b)に置き換えられ、rtrancl_converseDが適用できるようになります。force、auto、fastそしてbestでも同様の置き換えが行われます。
