Isabelle Tutorial その25

9. Advanced Simplification and Induction

9.1 Simplification

この節では、単純化に関してこれまで述べてこなかった部分を補足します。

9.1.1 Advanced Features

Congruence Rules.

P ==> QのQを単純化するのに前提Pを利用できます。==>ならば当然のように思えますが、他の演算子の場合も同様に文脈上の事実が使われます。文脈から得られる事実を使用するための規則を合同規則と言います。例えば次の規則は-->の合同規則です。

[| ?P = ?P'; ?P' ==> ?Q = ?Q' |] ==> (?P --> ?Q) = (?P' --> ?Q')　　　　(imp_cong)

限量子の合同規則は束縛変数に関する文脈情報を与えます。

[| ?A = ?B; !!x. x : ?B ==> ?P x = ?Q x |]
==> (ALL x:?A. ?P x) = (ALL x:?B. ?Q x)　　　　(ball_cong)

条件式の合同規則はthen節とelse節の単純化するための規則を与えます。

[| ?b = ?c; ?c ==> ?x = ?u; ~ ?c ==> ?y = ?v |]
==> (if ?b then ?x else ?y) = (if ?c then ?u else ?v)　　　　(if_cong)

条件式には次の合同規則もあり、こちらが条件式のデフォルトの合同規則になっています。

[| ?b = ?c; ?c ==> ?x = ?u; ~ ?c ==> ?y = ?v |]
==> (if ?b then ?x else ?y) = (if ?c then ?u else ?v)　　　　(if_weak_cong)

最初の項のみが単純化され、残りはそのままです。

独自の規則を合同規則にしたり無効にしたりするには、次のようにします。

declare theorem_name [cong]
declare theorem_name [cong del]

Permutative Rewrite Rules.

等式の右辺と左辺の変数が同じならば、並び替え規則と言います。もっとも一般的な並び替え規則はx + y = y + xのような交換律です。このような規則は無限に適用を続ける事ができますが、単純化では順序付き書換えと呼ばれる方法でこれを回避します。順序付きとは、項に対するある辞書式順序が小さくなる場合にのみルールが適用されることを言います。例えばb + aからa + bへは変換されますが、a + bの方が辞書式順序で小さいため、逆向きには書き換えられません。

並び替え規則は交換・結合律を満たす関数に対して効果的です。そのような関数を定義する場合、次のことに気を付けると良いでしょう。

結合律は左から右へ、つまりf(f(x, y), z) = f(x, f(y, z))の向きにします。
結合律(A)と交換律(C)に加えて左交換律(LC)、f(x, f(y, z)) = f(y, f(x, z))も定義します。

A、C、そしてLCによって次の例のように項が辞書式に並べ替えられます。

$f(f(b, c), a) \overset{\text{A}}{\rightarrow} f(b, f(c, a)) \overset{\text{C}}{\rightarrow} f(b, f(a, c)) \overset{\text{LC}}{\rightarrow} f(a, f(b, c))$

9.1.2 How the Simplifier Works

単純化はボトムアップに、つまり内側の項から先に行われます。また条件付きの場合は、条件が単純化によって証明できた場合にのみ適用されます。以下では更に特別な場合の単純化の振る舞いを説明します。

Higher-Order Patterns.

単純化ルールの左辺は高階パターンであることが求められており、スキーム変数の出現位置が制限されます。高階パターンの項はβ正規形であり、スキーム変数は?f x₁ ... x_nという形で出現します。もしスキーム変数が基本型ならば、引数の数は0です。よって、例えば?a + ?b + ?c = ?a + (?b + ?c)のようにすべてのスキーム変数の型が基本型であるような書換規則は、この制限を満たします。

もし左辺が高階パターンでない場合、それでも直接マッチする場合は規則が適用されます。例えば(?f ?x : range ?f) = Trueによってg a : range gからTrueに書き換えられますが、g(h b) : range (% x. g(h x))は失敗します。?f ?xを取り除き?y = ?f ?x ==> (?y : range ?f) = Trueとすることで改善しますが、完全な解決策とはなりません。

一方、右辺には制限がありません。

The Preprocessor.

定理を単純化ルールとして宣言すると、一つの等式から複数の等式に自動的に変形されます。例えばf x = g x & h x = k xは二つの単純化ルールf x = g xとh x = k xに分割されます。一般的に、入力された定理は次のように変形されます。

~P  |->  P = False
P --> Q  |->  P ==> Q
P & Q  |->  P, Q
ALL x. P x  |->  P ?x
ALL x : A. P x  |->  ?x : A ==> P ?x
if P then Q else R  |->  P ==> Q, ~P ==> R

これらの変形が終わった後、等式ではない項PはP = Trueに変形されます。例えば式

(p --> t = u & ~r) & s

は次の三つの式に変形されます。

p ==> t = u, p ==> r = False, s = True