7.4 Rewriting (1)

　このREWR_CONV(: thm -> term -> thm = )を先のdepth conversions(: conv -> conv = )のもとで用いれば，等式についてのtheoremから導ける限りのtermの書き換えが可能になります．
　例えば

# let tm = `(a + b) + ((c + d) + e) + f + g + h` ;;
val tm : term = `(a + b) + ((c + d) + e) + f + g + h`

の括弧を整理するには

# NUM_REDUCE_CONV tm;;
val it : thm =
|- (a + b) + ((c + d) + e) + f + g + h =
(a + b) + ((c + d) + e) + f + g + h

としても上手く行きませんので

# ADD_ASSOC;;
val it : thm = |- !m n p. m + n + p = (m + n) + p

というtheoremを繰り返し適用すれば

# TOP_DEPTH_CONV (REWR_CONV ADD_ASSOC) tm;;
val it : thm =
|- (a + b) + ((c + d) + e) + f + g + h =
((((((a + b) + c) + d) + e) + f) + g) + h

といった具合になり，括弧を消去したいなら

# GSYM ADD_ASSOC;;
val it : thm = |- !m n p. (m + n) + p = m + n + p
# TOP_DEPTH_CONV (REWR_CONV (GSYM ADD_ASSOC) ) tm;;
val it : thm =
|- (a + b) + ((c + d) + e) + f + g + h = a + b + c + d + e + f + g + h

とすればよいでしょう．ちなみに

# get_infix_status "+";;
val it : int * string = (16, "right")

ですから，右寄りの括弧は無視できます．

# `a + (b + ((c + d) + e) + f) + (g + h)` ;;
val it : term = `a + (b + ((c + d) + e) + f) + g + h`
# TOP_DEPTH_CONV (REWR_CONV (GSYM ADD_ASSOC) ) it;;
val it : thm =
|- a + (b + ((c + d) + e) + f) + g + h = a + b + c + d + e + f + g + h

　ここで用いたgeneralized symmetry GSYM(: thm -> thm = )は全称量化子越しに適用できる推論規則SYM(: thm -> thm = )です．