13 Recursive definitions
HOL Light上で関数を定義する道具としては，new_definition(: term -> thm =
# let fib = new_definition
`fib n = if n = 0 \/ n = 1 then 1 else fib(n - 1) + fib(n - 2)`;;
Exception: Failure "new_definition: term not closed".
のように帰納的定義には対応していません．
これに対して，define(: term -> thm =
# let fib = define
`fib n = if n = 0 \/ n = 1 then 1 else fib(n - 1) + fib(n - 2)`;;
val fib : thm =
|- fib n = (if n = 0 \/ n = 1 then 1 else fib (n - 1) + fib (n - 2))
のように受け付けてくれます．
ただし，thm_tacticなどで参照するには，性質の連言を
# let fib2 = define
`(fib2 0 = 1) /\
(fib2 1 = 1) /\
(fib2 (n + 2) = fib2(n) + fib2(n + 1))`;;
val fib2 : thm =
|- fib2 0 = 1 /\ fib2 1 = 1 /\ fib2 (n + 2) = fib2 n + fib2 (n + 1)
のように定義しておくのが便利です．
ここで注意したいのは，一般にthmは，その全称閉包と等価ですから，(fib2 n = fib2 (n - 1) + fib2 (n - 2))のようにするとfib2 0 = fib2 (0 - 1) + fib2 (0 - 2)，および，cutoffにより，fib2 0 = fib2 0 + fib2 0，つまり，fib2 0 = 0となり，連言がFとなってしまいます．
# let fib2 = define
`(fib2 0 = 1) /\
(fib2 1 = 1) /\
(fib2 n = fib2 (n - 1) + fib2 (n - 2))`;;
Exception: Failure "mk_abs: not a variable".
さらに，矛盾を含むか否かが自明でない場合にも
# let fusc = define
`(fusc 0 = 0) /\
(fusc 1 = 1) /\
(fusc (2 * n) = fusc(n)) /\
(fusc (2 * n + 1) = fusc(n) + fusc(n + 1))` ;;
Exception: Failure "new_specification: Assumptions not allowed in theorem".
のように拒絶されますので，このような場合には，まず，スマートではなくとも矛盾を含まない定義を
# let fusc_def = define
`(fusc (2 * n) = if n = 0 then 0 else fusc(n)) /\
(fusc (2 * n + 1) = if n = 0 then 1 else fusc(n) + fusc(n + 1))`;;
val fusc_def : thm =
|- fusc (2 * n) = (if n = 0 then 0 else fusc n) /\
fusc (2 * n + 1) = (if n = 0 then 1 else fusc n + fusc (n + 1))
のように与え，それを参照して形のよいthmを証明するとよいでしょう．
# let fusc = prove
(`fusc 0 = 0 /\
fusc 1 = 1 /\
fusc (2 * n) = fusc(n) /\
fusc (2 * n + 1) = fusc(n) + fusc(n + 1)`,
REWRITE_TAC[fusc_def] THEN
COND_CASES_TAC THEN
ASM_REWRITE_TAC[] THEN
MP_TAC(INST [`0`,`n:num`] fusc_def) THEN
ARITH_TAC);;
val fusc : thm =
|- fusc 0 = 0 /\
fusc 1 = 1 /\
fusc (2 * n) = fusc n /\
fusc (2 * n + 1) = fusc n + fusc (n + 1)
