3.4 Derived rules

　ここまでの道具だけで，自明でない定理を証明することはやや辛いです．しかし，HOL Lightには，強力な推論規則により自明でない定理を自動的に証明するproverが実装されています．
　その一つ，ARITH_RULE関数は，自然数（非負整数）の代数的な順序交換と線形不等式の処理のみで証明できる定理に対するproverです．

ARITH_RULE`(x-1)*(1+ x EXP 2 + x)=(x EXP 2 + x + 1)*(x-1)`;;
val it : thm = |- (x - 1) * (1 + x EXP 2 + x) = (x EXP 2 + x + 1) * (x - 1)
ARITH_RULE`x>=0`;;
val it : thm = |- x >= 0

　HOL Lightの本格的な証明は，こうした処理などを幾つも組み合わせて構成されるものであり，第８章以降で種々の例を挙げて行きますが，そのためにはもう少し準備が必要です．
　なお，チュートリアルの本節にある主な例は，Tutorial/all.mlに掲載されており

#use "Tutorial/all.ml";;

でロード，実行できますが，設定の関係で途中でリセットが必要なので，分割して実行するのが適当でしょう．