8 Tactics and tacticals

　HOL Lightでは，CONJやMPといった推論規則を順次適用する証明作成も原理的には可能ですが，得られる中間結果の授受は少し退屈です．これに対して，証明したい論理式termをgoalとして，それを展開してより簡単なsubgoalsの証明に帰する，下から上への証明作成が自然な場合もあります．HOL Lightは，こうした下向き，上向きを織り交ぜた証明の構成の，goals tacticsに基づく，極めて一般的な方法をサポートしており，そのための簡単ながら便利な関数も提供します．以下，それらを少しずつ試して行きましょう．

　まず，重要なのはgoalという概念です．荒く言えば，それは証明すべき目標ですが，単なるtermではなく，種々の仮定を含んだものです．

　そして，HOL Lightは，goalを証明するためのgoalstackを作ります．すなわち，tactic と呼ばれる関数が，goalを推論規則を下から上に上る向きにsubgoalsのリストへ分解し，ユーザーがそのsubgoals全ての証明に成功すれば，tacticで遡った各推論規則が自動的に適用され，もとのgoalの証明が完成する仕組みです．