5.4 Definitions

　HOL Lightでは新たなconstant（固定された数や関数など）を定義することもできます．それにはnew_definition関数を用いて，その定義をtheoremにすればよいのです．

let def_of_wordlimit = new_definition `wordlimit = 2 EXP 32`;;
val def_of_wordlimit : thm = |- wordlimit = 2 EXP 32
def_of_wordlimit;;
val it : thm = |- wordlimit = 2 EXP 32

ただし，既にHOL Lightにおいて異なるとされるものを同じconstantにしようとすると

ARITH_RULE`~(2 EXP 32=2 EXP 64)`;;
val it : thm = |- ~(2 EXP 32 = 2 EXP 64)
let def_of_wordlimit = new_definition `wordlimit = 2 EXP 64`;;
Exception: Failure "new_basic_definition".

と叱られます．
　このような場合は，数のcontantではなく，関数のconstantとして定義すれば上手く行きます．

let def_of_wordlimitfun = new_definition `wordlimitfun n = 2 EXP n`;;
val def_of_wordlimitfun : thm = |- !n. wordlimitfun n = 2 EXP n