7 Conversions and rewriting
HOL Lightは，あるtermが別のtermと等価である（:numなどの場合は=，:boolの場合は<=>で結ばれる）ことを，体系的な変形を経て示す為，様々なconversionsを提供します．
conversionはterm -> thm typeの関数で，typeはARITH_RULEやMESON[]などのproverと同じですが，与えられたterm tmに対して，tmと等価なterm tm'を自動生成して，|- tm=tm'を返えしてくれます．
例えば，先に述べたREFL(: term -> thm =
もう少し面白い例は，先のBETA，INSTの組合せを一気に行うconversion関数 BETA_CONV です．
# INST[`y:num`,`x:num`](BETA`(\x.x+1)x`);;
val it : thm = |- (\x. x + 1) y = y + 1# BETA_CONV`(\x.x+1)y`;;
val it : thm = |- (\x. x + 1) y = y + 1
自然数の和差積商などのtermを評価するconversion関数の例としては，NUM_*_CONVがあり
# NUM_ADD_CONV `12 + 4` ;;
val it : thm = |- 12 + 4 = 16
# NUM_SUB_CONV `12 - 4` ;;
val it : thm = |- 12 - 4 = 8
# NUM_SUB_CONV `12 - 15` ;;
val it : thm = |- 12 - 15 = 0
# NUM_MULT_CONV `12 * 4` ;;
val it : thm = |- 12 * 4 = 48
# NUM_EXP_CONV `12 EXP 4` ;;
val it : thm = |- 12 EXP 4 = 20736
# NUM_FACT_CONV `FACT 10` ;;
val it : thm = |- FACT 10 = 3628800
# NUM_DIV_CONV `12 DIV 4` ;;
val it : thm = |- 12 DIV 4 = 3
# NUM_MOD_CONV `12 MOD 4` ;;
val it : thm = |- 12 MOD 4 = 0
# NUM_MOD_CONV `12 MOD 5` ;;
val it : thm = |- 12 MOD 5 = 2
# NUM_MAX_CONV `MAX 12 5` ;;
val it : thm = |- MAX 12 5 = 12
# NUM_MIN_CONV `MIN 12 5` ;;
val it : thm = |- MIN 12 5 = 5
# NUM_SUC_CONV `SUC 12` ;;
val it : thm = |- SUC 12 = 13
# NUM_PRE_CONV `PRE 12` ;;
val it : thm = |- PRE 12 = 11
# NUM_PRE_CONV `PRE 0` ;;
val it : thm = |- PRE 0 = 0
などとなり，これらを区別なく行うのが NUM_RED_CONV，これらの組合せにも適用できる一般的なものが NUM_REDUCE_CONV です．
# NUM_REDUCE_CONV `(1 + 2) * 3 DIV 2` ;;
val it : thm = |- (1 + 2) * 3 DIV 2 = 3
# NUM_REDUCE_CONV `((1 + 2) * 3 ) DIV 2` ;;
val it : thm = |- ((1 + 2) * 3) DIV 2 = 4
:realをドメインとする同様のconversionsは，REAL_RAT_*_CONVとして提供されます．
# REAL_RAT_REDUCE_CONV `&4 pow 10000 / &2 pow 20000 `;;
val it : thm = |- &4 pow 10000 / &2 pow 20000 = &1
:intに対しては，REAL_INT_ADD_CONV，REAL_INT_REDUCE_CONVがあります．
