3.3 Theorems

　述語論理のformulaに当たるtermのhol_typeは

`x+1

であり

`2+2=5`;;
val it : term = `2 + 2 = 5`

もhol_typeがboolのtermです．
　これまでの例からも判る通り，HOL Lightは入力されたtermを直ちには評価しません（Mathematicaなら
2+2は4，2+2=5はFalseと返すところです）．評価にはその関数を明示して，例えば

REFL `x:real`;;
val it : thm = |- x = x

のようにします．これは，hol_typeがrealのterm xに反射律 REFL を適用して，|- x = xというthm（定理）を得たものです．
　数理論理と同じく，p1,...,pn|-pは，HOL Lightが知っているaxioms（公理）とrules（推論規則）および，仮定p1,...,pnからpが証明可能であることを表し，|-pは仮定なしでpが証明可能であるということです．仮定の付いたthmの簡単な例には，自分自身から自分を導く規則 ASSUME を用いた

ASSUME `1=2`;;
val it : thm = 1 = 2 |- 1 = 2

があります．
　termに対するsubstに当たる，thmに含まれる自由変数への代入関数が INST です．書き忘れていましたが，一般に関数の書式の確認には，引数なしで関数を呼びます．

subst;;
val it : (term * term) list -> term -> term =
INST;;
val it : (term * term) list -> thm -> thm =

この(term * term) listとは

[`1`,`(x:num)`];;

のようなlistであり，その要素は

(`1`, `(x:num)`)

というtermとtermの順序対で

let th1 = ASSUME `(x+1)+x=2`;;
val th1 : thm = (x + 1) + x = 2 |- (x + 1) + x = 2

に対して

INST [`1`,`(x:num)`] th1;;
val it : thm = (1 + 1) + 1 = 2 |- (1 + 1) + 1 = 2

のように用いますが，substとは異なり，代入できるのは変数に対してのみで，例えば

INST [`1`,`(x:num)+1`] th1;;
Exception: Failure "dest_var: not a variable".

と叱られます．
　thmの結論であるtermを取り出す関数がconcl関数であり，例えば

ASSUME`x=1`;;
val it : thm = x = 1 |- x = 1
concl it;;
val it : term = `x = 1`

のようになります．
　一般にHOL Lightは，証明そのものを出力しませんが，Proofrecordingディレクトリには，Coqのような外部システムへの変換ツールがあります．