HOL Light入門その４

次に全称量化をとるまえの状態に戻します．

e( GEN_TAC );;

すると

val it : goalstack = 1 subgoal (1 total)

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

のように !m. が付かないものが改めて目標（サブゴール）となります．

さて，この式を証明するには，明らかにmが0のときとそれ以外のときとの場合分けですが，HOL Lightが誇る定理群にはうってつけの定理があり，それを見るけるには search 関数を用いて

search[`m = 0 \/ P`];;

と入力します．この[　]内は現在のサブゴールに近いものであるべきですが，そのものでは無理なので，後半を一般化しています．結果は５個の候補が表示されるはずです．