IT/Description/tactics.tex

78 \index{proof steps, as ML function applications@proof steps, as \ML{} function applications}
79 is an \ML{} function that when applied to a \emph{goal}
85 function mapping a list of theorems to a theorem.  The idea is that
86 the function justifies the decomposition of the goal.
110 \index{proofs, in HOL logic@proofs, in \HOL{} logic!as ML function applications@as \ML{} function applications}
113 an \ML{} function
114 from a theorem list to a theorem.  The \ML{} `proof' function
119 evaluate the \ML{} function corresponding
124 the \ML{} function in question.)
125 The proof function, or justification, returned by a tactic is intended to map the
136 achieved by an axiom or an existing theorem; in \HOL, the function
141 `decomposition' by a proof function that maps the empty list of theorems
175 function.)
188 function that when applied to the list
226 of the proof function, in the \ML{} sense of failure, when
227 applied to a list of theorems (if, for example, the function were
265 proof function.
313 function \ml{REWRITE\_TAC}
321 required, the function includes as rewrites the same
403 Since a tactic\index{proof steps, as ML function applications@proof steps, as \ML{} function applications} is an \ML{} function, the user
411  function;
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},
431 proof function is specified in terms of the derived rule \ml{CONJ}
451 an infixed \ML{} function. Complex and powerful tactics can be
504 by using the function \ml{save\_thm} (see Section~\ref{theoryprims}).
1060 an \ML{} function that returns a tactic (or tactics) as result.
1189  (an infix)\index{function composition, in ML@function composition, in \ML}
1197 \index{ function composition operator, in ML@{\small\verb+o+} (function composition operator, in \ML)}
1247 pair \ml{($gll$,$pl$)} of a subgoal list and a proof function, where
1306 is a function that, when
1349 \index{EVERY, the ML function@\ml{EVERY}, the \ML{} function|pin}
1491 \noindent Given a function $f$\ml{:thm -> tactic}, the tactic
1668 $(n=0 \disj n=1) \imp (n\times n = n)$, the function \ml{DISJ\_CASES\_TAC}
1739 \noindent That is, given a function $f$, \ml{ASSUM\_LIST}$\ f$ forms a new tactic
1743 function $f$ to the $i$th assumption of a goal to produce a new tactic, then
1749 specific assumptions to be accessed by location using the function \ml{el}.
1789 (The \ML{} function \ml{el: int -> * list -> *} is used here to select a
1811 but not the issue of discarding them.  A related function generalizes
1869 take any function of appropriate
1921 to a function.  These tacticals use the function to
2107 %(The choice of the witness is `understood' by the justification function.)