7.1 Conversionals

　conversionsによる処理の優位性は，それらを制御して，より複雑なconversionを生成するconversionalと呼ばれる関数(: conv -> conv = )の存在にあります．

　今回はその中でも，複数のconversionsを組み合わせるものを紹介します．

■　まず，次に定義するTHENC関数

let (THENC) =
fun conv1 conv2 t ->
let th1 = conv1 t in
let th2 = conv2 (rand(concl th1)) in
TRANS th1 th2;;

は３変数関数ですが，curryingにより，第１，２引数に対する

conv1 THENC conv2 THENC conv3 ...;;

の書式が可能な２項演算子となり，例えば

# (BETA_CONV THENC NUM_REDUCE_CONV) `(\x.x+5*x)7`;;
val it : thm = |- (\x. x + 5 * x) 7 = 42

のようにconversionsを合成します．
　当然，合成されたconvの何れかが失敗すると，合成全体のconvも失敗します．

# (NUM_MULT_CONV THENC NUM_ADD_CONV) `1+2`;;
Exception: Failure "term_pmatch".

■　一方，conv1が失敗した時にconv2を実行，以下繰り返すようなconvを作るのが

conv1 ORELSEC conv2 ORELSEC conv3 ...;;

の書式が可能な２項演算子 ORELSEC です．

# (NUM_MULT_CONV ORELSEC NUM_ADD_CONV) `1+2`;;
val it : thm = |- 1 + 2 = 3

■　そして，TRY_CONV conv tは，convが成功したときはその結果を，失敗したときは|- t ==> t を返し，CHANGED_CONV conv t は，convが|- t ==> tを返したときに失敗し，その他のときはその結果を返す，ようなconvを作るconversionalです．

# TRY_CONV NUM_MULT_CONV `1*2`;;
val it : thm = |- 1 * 2 = 2
# NUM_MULT_CONV `1+2`;;
Exception: Failure "term_pmatch".
# TRY_CONV NUM_MULT_CONV `1+2`;;
val it : thm = |- 1 + 2 = 1 + 2

# NUM_REDUCE_CONV `x+1`;;
val it : thm = |- x + 1 = x + 1
# CHANGED_CONV NUM_REDUCE_CONV `x+1`;;
Exception: Failure "CHANGED_CONV".
# CHANGED_CONV NUM_REDUCE_CONV `2+1`;;
val it : thm = |- 2 + 1 = 3

■　REPEATC conv t は失敗するまで，convで得られた結果にconvを繰り返し適用します．

# BETA_CONV `(\x. (\y. x + y) 2) 1`;;
val it : thm = |- (\x. (\y. x + y) 2) 1 = (\y. 1 + y) 2
# REPEATC BETA_CONV `(\x. (\y. x + y) 2) 1`;;
val it : thm = |- (\x. (\y. x + y) 2) 1 = 1 + 2
# ( (REPEATC BETA_CONV) THENC NUM_ADD_CONV ) `(\x. (\y. x + y) 2) 1`;;
val it : thm = |- (\x. (\y. x + y) 2) 1 = 3