HOL Light入門その３

では証明を書いていきましょう．簡単過ぎるのもおもしろくないので

任意の自然数 m に対して m=0 または 3^mを3で割った余りが0

の証明からはじめます．まずこれを論理式に直して，目標（ゴール）に設定します．

g `!m. m = 0 \/ 3 EXP m MOD 3 = 0`;;

g というのはゴールを設定する関数，それに続く，` と ` とで挟まれた部分が証明すべき式（HOL Lightではフォーミュラではなくタームと呼びます）であり

! は全称記号，mは量化される変数，.は仕切り，
\/はまたは，3 EXP m は 3^m，そして，
一般に a MOD b は自然数 a を自然数 b で割った余り

を表しています．このようにHOL Lightでは括弧が略せる場合があり，例えば

g ( `!m.(m = 0 \/ (3 EXP m) MOD 3 = 0)` );;

などと入力しても

val it : goalstack = 1 subgoal (1 total)

`!m. m = 0 \/ 3 EXP m MOD 3 = 0`

のように簡潔に表示されます．それと今更ですが行末は ; が２つです．