![[PukiWiki]](image/knxmpen.png "[PukiWiki]")
HOL Light is a computer program to help users prove interesting mathematical theorems completely formally in higher order logic. It sets a very exacting standard of correctness, but provides a number of automated tools and pre-proved mathematical theorems (e.g. about arithmetic, basic set theory and real analysis) to save the user work. It is also fully programmable, so users can extend it with new theorems and inference rules without compromising its soundness.
名称は HOL のライト版のようであり，実際，Isabelle2013 のような強力な検索ツールも（デフォルトでは）付属せず，ProofPower のような大掛かりなインターフェイスも持ちませんが，本家 HOL の先駆的な数学ライブラリの作者が独立させた，Cambridge HOL ファミリー中，数学の公理論的構成という定理証明システム本来の目的に最も適したシステム，それが HOL Light です．
MathLibre (20130831) ではインストール済みです．それ以前のバージョンでは次を実行してください．
sudo apt-get install hol-light
（＊最新版を用いる場合は，適当なディレクトリで
svn co http://hol-light.googlecode.com/svn/trunk/ hol-light cd ./hol-light make
＊）
起動（初期ファイルのロードに１〜２分掛かります）
cd /usr/share/hol-light hol-light
（＊最新版を用いる場合は，make を実行したディレクトリに移動して
rlwrap ocaml -init ./hol.ml
＊）
数学的帰納法（まとめてコピペしても通りますが，１行ずつの方が過程が見易いです）
g `!n. ?x. x * x <= n /\ n < SUC x * SUC x`;; e INDUCT_TAC;; e(EXISTS_TAC`0` THEN ARITH_TAC);; e(POP_ASSUM MP_TAC THEN STRIP_TAC);; e(ASM_CASES_TAC`SUC n = SUC x * SUC x`);; e(EXISTS_TAC`SUC x` THEN ASM_ARITH_TAC);; e(EXISTS_TAC`x:num` THEN ASM_ARITH_TAC);; top_thm();;
余弦関数の３倍角公式
needs "Library/transc.ml";; g `!x. cos (&3 * x) = &4 * cos x pow 3 - &3 * cos x`;; e(GEN_TAC THEN SIMP_TAC[REAL_ARITH`&3 * x = x + x + x`;COS_ADD;SIN_ADD]);; e(MP_TAC(SPEC_ALL SIN_CIRCLE));; e(CONV_TAC REAL_RING);; top_thm();;
終了
#quit;;
