9.1 Arithmetical decision procedures

■　prover ARITH_RULE(: term -> thm = )の:int版，:real版としてINT_ARITH，REAL_ARITHがあるわけですが，それらの特徴は
・代数的な並び替えなら非線形でも扱える

# INT_ARITH
`!a b a' b' D:int.
(a pow 2 - D * b pow 2) * (a' pow 2 - D * b' pow 2) =
(a * a' + D * b * b') pow 2 - D * (a * b' + a' * b) pow 2`;;
val it : thm =
|- !a b a' b' D.
(a pow 2 - D * b pow 2) * (a' pow 2 - D * b' pow 2) =
(a * a' + D * b * b') pow 2 - D * (a * b' + a' * b) pow 2

・線形多項式不等式は扱える

# REAL_ARITH `!a b x:real. a >= &2 * x + b <=> x <= ( a - b ) / &2`;;
val it : thm = |- !a b x. a >= &2 * x + b <=> x <= (a - b) / &2
# REAL_ARITH `!x y:real. abs(abs(x) - abs(y)) <= abs(x - y)`;;
val it : thm = |- !x y. abs (abs x - abs y) <= abs (x - y)

・線形多項式方程式は勿論扱える（次の例はPrologIIIのデモで有名になったものですが，HOL Lightは素朴に場合分けるだけなので，あなたよりも低速かも知れません．）

# REAL_ARITH
`!x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11:real.
x3 = abs(x2) - x1 /\
x4 = abs(x3) - x2 /\
x5 = abs(x4) - x3 /\
x6 = abs(x5) - x4 /\
x7 = abs(x6) - x5 /\
x8 = abs(x7) - x6 /\
x9 = abs(x8) - x7 /\
x10 = abs(x9) - x8 /\
x11 = abs(x10) - x9
==> x1 = x10 /\ x2 = x11`;;
val it : thm =
|- !x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11.
x3 = abs x2 - x1 /\
x4 = abs x3 - x2 /\
x5 = abs x4 - x3 /\
x6 = abs x5 - x4 /\
x7 = abs x6 - x5 /\
x8 = abs x7 - x6 /\
x9 = abs x8 - x7 /\
x10 = abs x9 - x8 /\
x11 = abs x10 - x9
==> x1 = x10 /\ x2 = x11

といったところです．

■　conversion NUM_REDUCE_CONV，INT_REDUCE_CONV，REAL_RAT_REDUCE_CONVは，theorem |- (引数のterm)=(それを簡約したもの) を返します．

# NUM_REDUCE_CONV `1-1=0`;;
val it : thm = |- 1 - 1 = 0 <=> T
# NUM_REDUCE_CONV `1-1`;;
val it : thm = |- 1 - 1 = 0
# NUM_REDUCE_CONV `1-1=0`;;
val it : thm = |- 1 - 1 = 0 <=> T
# NUM_REDUCE_CONV `a-a`;;
val it : thm = |- a - a = a - a
# NUM_REDUCE_CONV `a-a=0`;;
val it : thm = |- a - a = 0 <=> a - a = 0

# REAL_RAT_REDUCE_CONV `(&2 / &3) pow 100` ;;
val it : thm =
|- (&2 / &3) pow 100 =
&1267650600228229401496703205376 /
&515377520732011331036461129765621272702107522001

■　変数を含む場合には，conversion INT_POLY_CONV，REAL_POLY_CONV を用います．

# INT_POLY_CONV `(&1 + x:int) pow 5` ;;
val it : thm =
  |- (&1 + x) pow 5 =
     x pow 5 + &5 * x pow 4 + &10 * x pow 3 + &10 * x pow 2 + &5 * x + &1

# INT_POLY_CONV `(&1 + x) pow 5` ;;
val it : thm = |- (&1 + x) pow 5 = (&1 + x) pow 5

# REAL_POLY_CONV `(&1 + x) pow 5` ;;
val it : thm =
  |- (&1 + x) pow 5 =
     x pow 5 + &5 * x pow 4 + &10 * x pow 3 + &10 * x pow 2 + &5 * x + &1

# REAL_POLY_CONV `&8 * (a + b + c / &2) pow 3 - &6 * (a + b) * (&2 * b + c) * (c
 + &2 * a)` ;;
val it : thm =
  |- &8 * (a + b + c / &2) pow 3 - &6 * (a + b) * (&2 * b + c) * (c + &2 * a) =
     &8 * a pow 3 + &8 * b pow 3 + c pow 3