IT/Description/tactics.tex

7 in \HOL. All three originate with Milner
61 the idea is similarly central to theorem proving in \HOL.
68 %The tactics and tacticals in the \HOL{} system are derived from those in the
80 \index{goals, in HOL system@goals, in \HOL{} system}
110 \index{proofs, in HOL logic@proofs, in \HOL{} logic!as ML function applications@as \ML{} function applications}
112 in \HOL{}, following the \LCF{} usage; it is, as mentioned,
116 \index{proofs, in HOL logic@proofs, in \HOL{} logic!as generated by tactics} in the
117 logical sense (of a sequence of theorems depending on inference\index{inferences, in HOL logic@inferences, in \HOL{} logic!in goal-directed proof search} rules)
136 achieved by an axiom or an existing theorem; in \HOL, the function
154 made in \HOL:
207   theorem results, but the \HOL{} system used directly allows
210 \index{consistency, of HOL logic@consistency, of \HOL{} logic|(}
212 theorems in \HOL{} are always the result of performing a proof in the
221 the \HOL{} user in this case is that the problem may be not
232 \index{consistency, of HOL logic@consistency, of \HOL{} logic|)}
391 the entire chain\index{goal directed proof search!generation of proofs by}\index{proofs, in HOL logic@proofs, in \HOL{} logic!as generated by tactics}
396 The \HOL{} system provides a collection of pre-defined tactics (and
417 A simple example of a tactic written in \ML\index{proofs, in HOL logic@proofs, in \HOL{} logic!as ML function applications@as \ML{} function applications}\ is afforded by \ml{CONJ\_TAC},
418 whose definition in \HOL{} is as follows:
441 The tacticals provided in \HOL{} are listed in Section~\ref{tacticals}.
485 trace.\footnote{A possible extension to \HOL\ would be a `debugging
527 In short, \HOL{} provides a very general framework in which proof
532 built in tactics of the system.  The vital support that \HOL{} provides
534 can be represented as theorems of the \HOL{} system---security is
537 \section{Some tactics built into HOL}
542 used tactics in the \HOL{} system. (see \REFERENCE\
608 \subsection{Specialization}\index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!tactics for}
649 \index{conjunction, in HOL logic@conjunction, in \HOL{} logic!tactic for splitting of}
671 \index{implication, in HOL logic@implication, in \HOL{} logic!tactics for}
749 \index{case analysis, in HOL logic@case analysis, in \HOL{} logic!tactics for|(}
779 \index{disjunction, in HOL logic@disjunction, in \HOL{} logic!tactic for case splits on}
813 \index{case analysis, in HOL logic@case analysis, in \HOL{} logic!tactics for|)}
874 \index{implication, in HOL logic@implication, in \HOL{} logic!tactics for}
903 Resolution in \HOL{} is not classical resolution, but just Modus Ponens with
982 \index{equality, in HOL logic@equality, in \HOL{} logic!tactic for splitting}
1016 \index{existential quantifier, in HOL logic@existential quantifier, in \HOL{} logic!tactic for}
1063 Tacticals are used for building compound tactics.\index{compound tactics, in HOL system@compound tactics, in \HOL{} system}
1066 the \HOL{} system
1068 For a complete list of the tacticals in \HOL{} see \REFERENCE.
1394  in \HOL: those that transform the
1400 the second.  Often, many of the steps of a proof in \HOL{} are carried
1417 with the tools currently provided in \HOL, presents at
1441 As always in \HOL, there are quite a few ways around the various difficulties.
1445 \index{ML@\ML!purpose of, in HOL system@purpose of, in \HOL{} system}
1473 be combined in \HOL{} interactions.
1884 for example, changes in the implementation of \HOL, modifications of
1886 However, that sensitivity is not so serious in any one incarnation of \HOL;
2086 \HOL{} provides several other theorem continuation functions analogous to