9 HOL’s number systems

　今回は，HOL Lightにおける数の体系のお話です．
　これまでも多くの例で扱ってきたhol_typeが:numであり，これは自然数（非負整数）全体の集合でした．同様に，hol.mlのロードだけで利用できる:int，:realは整数，実数全体の集合であり

#use "./Complex/make.ml";;

により導入される:complexは複素数全体の集合です．

■　:numはデフォルトの数のhol_typeで，初期状態では

# type_of`a+b`;;
val it : hol_type = `:num`

であり，所謂，自然数の割り算における

　商　DIV
　余り　MOD

も扱えます．
　:numの元の証明は

# ARITH_RULE `1 + 2 EXP 3 - 4 * 5 DIV 6 = 9`;;
val it : thm = |- 1 + 2 EXP 3 - 4 * 5 DIV 6 = 9

計算は

# NUM_REDUCE_CONV `1 + 2 EXP 3 - 4 * 5 DIV 6`;;
val it : thm = |- 1 + 2 EXP 3 - 4 * 5 DIV 6 = 9

とできますが，cutoff，つまり

# ARITH_RULE `a <= b ==> a - b = 0`;;
val it : thm = |- a <= b ==> a - b = 0

# ARITH_RULE `a-b+b=a`;;
Exception: Failure "linear_ineqs: no contradiction".

# ARITH_RULE `a>=b ==> (a-b)+b=a`;;
val it : thm = |- a >= b ==> a - b + b = a

# NUM_REDUCE_CONV `1-2+2`;;
val it : thm = |- 1 - 2 + 2 = 2

という性質で，-を含んだ:numの元の計算は慎重に進めねばなりません．

■　略した際の数のhol.typeの設定を変えるには

# prioritize_real();;
val it : unit = ()
# type_of`a+b`;;
val it : hol_type = `:real`
# prioritize_int();;
val it : unit = ()
# type_of`a+b`;;
val it : hol_type = `:int`
# prioritize_num();;
val it : unit = ()
# type_of`a+b`;;
val it : hol_type = `:num`

のようにします．勿論，使用時に明示すれば

# prioritize_num();;
val it : unit = ()
# type_of`a+(b:int)`;;
val it : hol_type = `:int`
# type_of`(a:real)+b`;;
val it : hol_type = `:real`

となります．

■　:int，;realでは

# prioritize_int();;
val it : unit = ()
# INT_REDUCE_CONV `&1- &2+ &2`;;
val it : thm = |- &1 - &2 + &2 = &1
# INT_ARITH `&1- &2+ &2= &1`;;
val it : thm = |- &1 - &2 + &2 = &1

# prioritize_real();;
val it : unit = ()
# REAL_RAT_REDUCE_CONV `&0- &2/ &2`;;
val it : thm = |- &0 - &2 / &2 = -- &1
# REAL_ARITH `&0- &2/ &2= -- &1`;;
val it : thm = |- &0 - &2 / &2 = -- &1

のように普通の計算ができるわけですが，各数は，:numからの包含写像&の像なので，左の+-*/=などと結合しないよう，&の前にスペースが必要です．また

　`a`の反数は`-- a`
　指数関数はpow

と記し，絶対値関数absや2変数関数max，minも使えます．