7.2 Depth conversions

　termの中に現れるtermのconversionには，個々のconvを適用する位置や回数，順序などを指定するconversional関数(: conv -> conv = )を用います．
　RAND_CONV conv tm における RAND_CONV は，tm内のrand tmにconvを適用します．例えば

rand `1 + 2 + 3`;;
val it : term = `2 + 3`
# NUM_ADD_CONV it;;
val it : thm = |- 2 + 3 = 5

なので

RAND_CONV NUM_ADD_CONV `1 + 2 + 3`;;
val it : thm = |- 1 + 2 + 3 = 1 + 5

となります．
　RATOR_CONV conv tm における RATOR_CONV は，tm内のrator tmにconvを適用します．例えば

# rator `(\x.x+3+2)1`;;
val it : term = `\x. x + 3 + 2`
# NUM_REDUCE_CONV it;;
val it : thm = |- (\x. x + 3 + 2) = (\x. x + 5)

なので

# RATOR_CONV NUM_REDUCE_CONV `(\x.x+3+2)1`;;
val it : thm = |- (\x. x + 3 + 2) 1 = (\x. x + 5) 1

となります．
　ABS_CONV conv `(\x.p)` は，|- (\x.p) = (\x. conv p) を返します．入力のtremがabs，さらに結果のthmも |- abs = abs であることに注意して下さい．

# ABS_CONV NUM_REDUCE_CONV `(\x.x+1+2)`;;
val it : thm = |- (\x. x + 1 + 2) = (\x. x + 3)

　同様に，BINDER_CONV は，binder一般の本体にconvを作用させます．

# BINDER_CONV NUM_REDUCE_CONV `\x.x+1+2`;;
val it : thm = |- (\x. x + 1 + 2) = (\x. x + 3)
# BINDER_CONV NUM_REDUCE_CONV `!x.x+1+4=y+2+3`;;
val it : thm = |- (!x. x + 1 + 4 = y + 2 + 3) <=> (!x. x + 5 = y + 5)

　LAND_CONV は，2項演算の左辺に対して，BINOP_CONV は，2項演算の両辺に対して，conv を作用させます．

# RATOR_CONV NUM_REDUCE_CONV `1+4=2+3`;;
val it : thm = |- 1 + 4 = 2 + 3 <=> 5 = 2 + 3
# LAND_CONV NUM_REDUCE_CONV `1+4=2+3`;;
val it : thm = |- 1 + 4 = 2 + 3 <=> 5 = 2 + 3
# RAND_CONV NUM_REDUCE_CONV `1+4=2+3`;;
val it : thm = |- 1 + 4 = 2 + 3 <=> 1 + 4 = 5
# BINOP_CONV NUM_REDUCE_CONV `1+4=2+3`;;
val it : thm = |- 1 + 4 = 2 + 3 <=> 5 = 5

　込み入ったconversionのターゲットの位置を指定するには，conv -> conv typeの関数を，左から順にoで結合します．

# (BINDER_CONV o LAND_CONV o RAND_CONV o RAND_CONV) NUM_REDUCE_CONV `?x.(x=1+2+1

1. 1<=>y=2+3)`;;

val it : thm =
|- (?x. x = 1 + 2 + 1 + 1 <=> y = 2 + 3) <=> (?x. x = 1 + 4 <=> y = 2 + 3)

とは言え，これはかなり面倒なので，tmをコピーし，作用させる位置を示すパターンのabsを作り，PAT_CONV abs tm とするのが便利です．

# PAT_CONV `(\t.(?x.(x=1+2+t<=>y=t)))` NUM_REDUCE_CONV `?x.(x=1+2+1+1<=>y=2+3)`;;
val it : thm =
|- (?x. x = 1 + 2 + 1 + 1 <=> y = 2 + 3) <=>
(?x. x = 1 + 2 + 2 <=> y = 5)

　最後に，より自動化されたconversionの制御関数（: conv -> conv = ）を挙げます．
　ONCE_DEPTH_CONV conv tm における ONCE_DEPTH_CONV は，tmの最も内側にあるterm(s)のみにconvを作用させます．

# ONCE_DEPTH_CONV NUM_ADD_CONV `1*((2+3)+(2+2)+6)+(7+8)`;;
val it : thm = |- 1 * ((2 + 3) + (2 + 2) + 6) + 7 + 8 = 1 * (5 + 4 + 6) + 15

それを失敗するまで繰り返すのがDEPTH_CONVです．

# DEPTH_CONV NUM_ADD_CONV `1*((2+3)+(2+2)+6)+(7+8)`;;
val it : thm = |- 1 * ((2 + 3) + (2 + 2) + 6) + 7 + 8 = 1 * 15 + 15