7.4 Rewriting (2)

　さて，rewritingは数学においてごく普通の処理ですから，HOL Lightは，複数のtheoremsを合わせて参照する，より高度なrewriting conversionを提供します．
　その最も一般的なものが

GEN_REWRITE_CONV convl [th1; ...; thn]

(: (conv -> conv) -> thm list -> conv = )であり，基本的には

convl( (REWR_CONV th1) ORELSEC ... ORELSEC (REWR_CONV thn) )

と同じ働きですが，REWR_CONVでは使えなかった，連言のthmも参照できます．

ARITH;;
val it : thm =
|- (NUMERAL 0 = 0 /\ BIT0 _0 = _0) /\
...
(!m n. BIT1 m - BIT0 n = (if n <= m then BIT1 (m - n) else _0)) /\
(!m n. BIT1 m - BIT1 n = BIT0 (m - n))
# REWR_CONV ARITH `0+1+2`;;
Exception: Failure "dest_eq".
# GEN_REWRITE_CONV ONCE_DEPTH_CONV [ARITH] `0+1+2`;;
val it : thm = |- 0 + 1 + 2 = 0 + NUMERAL (BIT1 _0 + BIT0 (BIT1 _0))
# GEN_REWRITE_CONV DEPTH_CONV [ARITH] `0+1+2`;;
val it : thm = |- 0 + 1 + 2 = NUMERAL (_0 + BIT1 _0 + BIT0 (BIT1 _0))
# GEN_REWRITE_CONV TOP_DEPTH_CONV [ARITH] `0+1+2`;;
val it : thm = |- 0 + 1 + 2 = 3

　なお
・ONCE_DEPTH_CONV，DEPTH_CONVがtermの内側から外側への評価順
・TOP_DEPTH_CONVはtermの外側から内側への評価順
を指定していることに注意します．

■　上の例で用いた(GEN_REWRITE_CONV o TOP_DEPTH_CONV) はよく用いるので，PURE_REWRITE_CONV(: thm list -> conv = )としても定義されており，更に

# basic_rewrites();;
val it : thm list =
[|- FST (x,y) = x; |- SND (x,y) = y; |- FST x,SND x = x;
|- (if x = x then y else z) = y; |- (if T then t1 else t2) = t1;
|- (if F then t1 else t2) = t2; |- ~ ~t <=> t; |- (@y. y = x) = x;
|- x = x <=> T; |- (T <=> t) <=> t; |- (t <=> T) <=> t;
|- (F <=> t) <=> ~t; |- (t <=> F) <=> ~t; |- ~T <=> F; |- ~F <=> T;
|- T /\ t <=> t; |- t /\ T <=> t; |- F /\ t <=> F; |- t /\ F <=> F;
|- t /\ t <=> t; |- T \/ t <=> T; |- t \/ T <=> T; |- F \/ t <=> t;
|- t \/ F <=> t; |- t \/ t <=> t; |- T ==> t <=> t; |- t ==> T <=> T;
|- F ==> t <=> T; |- t ==> t <=> T; |- t ==> F <=> ~t; |- (!x. t) <=> t;
|- (?x. t) <=> t; |- (\x. f x) y = f y; |- x = x ==> p <=> p]

を常に参照するのが，REWRITE_CONV(: thm list -> conv = )です．同様に，最も内側のみを書き換える(GEN_REWRITE_CONV o ONCE_DEPTH_CONV)は，PURE_ONCE_REWRITE_CONV(: thm list -> conv = )としても定義され，ONCE_REWRITE_CONVもあります．

# PURE_REWRITE_CONV [ARITH] `0+1+2`;;
val it : thm = |- 0 + 1 + 2 = 3
# REWRITE_CONV [ARITH] `0+1+2`;;
val it : thm = |- 0 + 1 + 2 = 3

REWR_CONV(: thm -> term -> thm = )と比べるなら

# REWR_CONV ADD_SYM `0+1`;;
val it : thm = |- 0 + 1 = 1 + 0
# REWRITE_CONV [ADD_SYM] `0+1`;;
val it : thm = |- 0 + 1 = 1 + 0
# REWR_CONV ADD_SYM `0+1+2`;;
val it : thm = |- 0 + 1 + 2 = (1 + 2) + 0
# REWRITE_CONV [ADD_SYM] `0+1+2`;;
val it : thm = |- 0 + 1 + 2 = 0 + 2 + 1

のようになります．
　前回定義したtmの整理は，加法の結合則と交換則をまとめたtheorem ADD_AC(AC = associative and commutative)

ADD_AC;;

を参照すると

# ADD_AC;;
val it : thm =
|- m + n = n + m /\ (m + n) + p = m + n + p /\ m + n + p = n + m + p
# REWRITE_CONV [ADD_AC] tm;;
val it : thm =
|- (a + b) + ((c + d) + e) + f + g + h = a + b + c + d + e + f + g + h

のように行えます．
　さらに，先に定義したconvの結合関数THENCを用いて，REWRITE_CONV どうしを合成して

# LEFT_ADD_DISTRIB;;
val it : thm = |- !m n p. m * (n + p) = m * n + m * p
# RIGHT_ADD_DISTRIB;;
val it : thm = |- !m n p. (m + n) * p = m * p + n * p
# MULT_AC;;
val it : thm =
|- m * n = n * m /\ (m * n) * p = m * n * p /\ m * n * p = n * m * p

への参照を結合させた

let SOP_CONV =
REWRITE_CONV[
LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THENC
REWRITE_CONV[MULT_AC] THENC
REWRITE_CONV[ADD_AC];;

(: term -> thm = )を定義すると，積の和(SOP)への変換，所謂，展開のconversionになります．

# SOP_CONV`(a+b)*(c+d)`;;
val it : thm = |- (a + b) * (c + d) = a * c + a * d + b * c + b * d

　なお，数のhol_typeに応じて theorem INT_*_AC，REAL_*_AC もあります．