Isabelle Tutorial その12

5.10 Description Operators

HOLには二つの記述演算子があります。確定記述はその式を満たす唯一の値を表わします。不確定記述はその式を満たす任意の値を表わします。

5.10.1 Definite Description

確定記述は伝統的にιx. P(x)と書きます。これは、P(x)を満たす値が唯一ならばその値を、それ以外の場合は任意の値を表わします。IsabelleではιのかわりにTHEを使用します。THEについて、次の規則があります。

[|?P ?a; !!x. ?P x ==> x = ?a|] ==> (THE x. ?P x) = ?a　　　　(the_equality)

Pを満たす最小の値を表わす演算子は次のように定義できます。

(LEAST x. P x) = (THE x. P x & (ALL y. P y --> x <= y))

次の定理を証明してみます。

theorem Least_equality: "[|P (k::nat); ALL x. P x --> k <= x|] ==> (LEAST x. P x) = k"
apply(simp add: Least_def)

最初のステップはLEASTの定義を展開しただけです。

 1. [| P k; ALL x. P x --> k <= x |]
    ==> (THE x. P x & (ALL y. P y --> x <= y)) = k

次に、the_equalityを使用します。

apply(rule the_equality)

 1. [| P k; ALL x. P x --> k <= x |] ==> P k & (ALL y. P y --> k <= y)
 2. !!x. [| P k; ALL x. P x --> k <= x; P x & (ALL y. P y --> x <= y) |]
         ==> x = k

the_equalityを使用すると、サブゴールは解が存在することと、それが唯一であることの二つとなります。一つ目の証明は自明です。二つ目の証明には反対称性に関する次の定理が必要です。

[|?x <= ?y; ?y <= ?x|] ==> ?x = ?y　　　　(order_antisym)

次のステップで証明が完了します。

by(auto intro: order_antisym)

5.10.2 Indefinite Description

不確定記述は伝統的にεx. P(x)と書き、P(x)を満たす値が存在するならばその中の任意の値を表わします。IsabelleではεのかわりにSOMEを使用します。

逆関数を表わすinvはSOMEを使用して定義されています。

inv f == % y. SOME x. f x = y　　　　(inv_def)

fが単射ではない場合もあるので、THEではなくSOMEを使用しなければなりません。例えば、inv SucがSucの逆関数になっていることを次のように証明できます。

lemma "inv Suc (Suc n) = n"
by(simp add: inv_def)

左辺は展開され、SOME x. Suc x = Suc nになり、SOME x. x = n、さらにはnになります。この証明では値が唯一に決まるため、SOMEを確定記述として扱っています。実際、SOMEには次の規則があります。

[|?P ?a; !!x. ?P x ==> x = ?a|] ==> (SOME x. ?P x) = ?a　　　　(some_equality)

また、SOMEには次の規則もあります。

?P ?x ==> ?P (SOME x. ?P x)　　　　　　　　　　　　　　　　(someI)
[|?P ?a; !!x. ?P x ==> ?Q x|] ==> ?Q (SOME x. ?P x)　　　　(someI2)

次に、例として選択公理を証明します。

theorem axiom_of_choice: "(ALL x. EX y. P x y) ==> EX f. ALL x. P x (f x)"
apply(rule exI, rule allI)

 1. !!x. ALL x. EX y. P x y ==> P x (?f x)

導入規則を適用しました。続けて除去規則も適用します。

apply(drule spec, erule exE)

 1. !!x y. P (?x2 x) y ==> P x (?f x)

someIを使用すると?fは% x. SOME y. P x yとなります。さらに、?x2 xをxとすることで、証明が完了します。

by(rule someI)

5.11 Some Proofs That Fail

正しくない定理を証明することで、どのように証明が失敗するかを見てみます。まずは、存在限量子と論理積の分配法則を証明してみます。

lemma "(EX x. P x) & (EX x. Q x) ==> EX x. P x & Q x"

まずは前提の論理積と存在限量子を除去します。

apply(erule conjE)
apply(erule exE)

 1. !!x. [| EX x. Q x; P x |] ==> EX x. P x & Q x

さらに存在限量子を除去すると、存在限量子の除去規則の条件により、新たな束縛変数が導入されます。

apply(erule exE)

 1. !!x xa. [| P x; Q xa |] ==> EX x. P x & Q x

結論の存在限量子に導入規則を適用するとスキーム変数が二カ所に現れますが、同じスキーム変数は同じ値と単一化しなければなりません。

apply(rule exI)
apply(rule conjI)

 1. !!x xa. [| P x; Q xa |] ==> P (?x3 x xa)
 2. !!x xa. [| P x; Q xa |] ==> Q (?x3 x xa)

一つ目のサブゴールにassumptionを適用すると、?x3 x xaはxに束縛され、二つ目のサブゴールは証明できなくなります。

apply assumption

 1. !!x xa. [| P x; Q xa |] ==> Q x

次は、束縛変数とスキーム変数の関係を見てみます。

lemma "ALL y. R y y ==> EX x. ALL y. R x y"

まず、exIを適用します。サブゴールには、スキーム変数?xが含まれています。

apply(rule exI)

 1. ALL y. R y y ==> ALL y. R ?x y

一見assumptionを適用できそうに見えますが、束縛変数が補足されるため、?xをyと単一化することはできません。証明を続けてみます。allIを使用して結論から全称限量子とともにyも取り除こうとしますが、yは今度はメタ全称限量子の束縛変数となります。

apply(rule allI)

 1. !!y. ALL y. R y y ==> R ?x y

specを適用すると、次のサブゴールが残ります。

apply(drule spec)

 1. !!y. R (?z2 y) (?z2 y) ==> R ?x y

明らかに?z2 yがyと単一化しなければなりませんが、前と同じようにyと?xを単一化することはできません。よってこの定理は証明できません。