1\chapter{Goal Directed Proof: Tactics and Tacticals} 2 3\label{tactics-and-tacticals} 4 5\index{tactics!purpose of|(} 6There are three primary devices that together make theorem proving practical 7in \HOL. All three originate with Milner 8\index{Milner, R.}\index{LCF@\LCF!Edinburgh} for Edinburgh \LCF. 9The first is the theory as 10a record of (among other things) facts already proved 11and thence available as lemmas 12\index{lemmas} 13without having to be re-proved. The second, 14the subject of Chapter~\ref{derived-rules}, is the 15derived rule of inference as a meta-language procedure that implements a 16broad pattern of inference, but that also, at each application, 17generates every primitive step of the proof. The third device is 18the tactic as a means of organizing the construction of proofs; 19and the use of tacticals for composing tactics. 20 21Even with recourse to derived inference rules, 22it is still surprisingly awkward to work forward, 23\index{forward proof!compared to goal directed} to find a chain of 24theorems that culminates in a desired theorem. This is in part because 25chains have no structure, while `proof efforts' do. For instance, if 26within one sequence, two chains of steps 27are to be combined in the end by conjunction, then 28one chain must follow or be interspersed with 29the other in the overall sequence. It can also be difficult to direct 30the proof toward its object when starting from 31only hypotheses (if any), lemmas (if any), 32axioms, and theorems following from no hypotheses 33(\eg\ by \ml{ASSUME} or \ml{REFL}). Likewise, it can be equally difficult 34to reconstruct 35\index{tactics!as documentation of proofs} 36the plan of the proof effort after the fact, from the 37linear sequence of theorems; the sequence is unhelpful as documentation. 38 39The idea of goal directed proof\index{goal directed proof search!reason for} is a simple one, well known in 40artificial intelligence: to organize the search\index{proof construction!as tree search} as a tree, and to reverse 41the process and {\it begin\/} with the objective. The goal is then 42decomposed, successively if necessary, 43into what one hopes are more tractable subgoals, each decomposition 44accompanied by a 45plan for translating the solution of subgoals into a solution of the goal. 46The choice of decomposition is an explicit way of expressing a proof 47`strategy'. 48\index{strategies, for proof} 49 50Thus, for example, instead of 51the linear sequencing of two branches of the proof of the conjunction, 52each branch starting from scratch, the proof task is organized 53as a tree search, starting with a conjunctive goal 54and decomposing it into the two conjunct subgoals (undertaken in optional 55order), with the intention of conjoining the two solutions when and if found. 56The proof itself, as a sequence of steps, is the same however it is found; 57the difference is in the search, and in the preservation, if required, of 58the structured proof plan. 59 60The representation of this idea in \LCF\ was Milner's inspiration; 61the idea is similarly central to theorem proving in \HOL. 62Although subgoaling theorem provers had already been built at the time, 63Milner's particular contribution was in formalizing the method for 64translating subgoals solutions to solutions of goals. 65 66 67 68%The tactics and tacticals in the \HOL{} system are derived from those in the 69%Cambridge \LCF\ system \cite{new-LCF-man} (which evolved 70%from the ones 71%in Edinburgh \LCF\ \cite{Edinburgh-LCF}). 72 73\section{Tactics, goals and justifications} 74\label{tactics} 75 76\index{goal directed proof search!concepts of|(} 77A \emph{tactic}% 78\index{proof steps, as ML function applications@proof steps, as \ML{} function applications} 79is an \ML{} function that when applied to a \emph{goal} 80\index{goals, in HOL system@goals, in \HOL{} system} 81reduces it to (i) a list\footnote{The ordering is necessary for selecting 82a tree search strategy.} of 83(sub)goals, along with (ii) a \emph{justification} 84\index{justifications, in goal-directed proof search} 85function mapping a list of theorems to a theorem. The idea is that 86the function justifies the decomposition of the goal. 87%that respectively {\it achieve\/} the (sub)goals 88%to a theorem that achieves the goal. 89A goal is an \ML{} value whose type is isomorphic 90to, but distinct from, the \ML{} abstract type \ml{thm} of theorems. 91That is, a goal is 92a list of terms ({\it assumptions\/}) 93\index{assumption list, of goal} paired with a term. 94\index{term component, of goal} 95These two components correspond, respectively, to the list of hypotheses 96and the conclusion of a theorem. The list of assumptions is a working 97record of facts that may be used in decomposing the goal. 98 99The relation of theorems to goals is achievement: 100\index{achievement, of goals} 101a theorem achieves a goal if the conclusion of the theorem 102is equal to the term part of the goal (up to $\alpha$-conversion), and 103if each hypothesis of the theorem is equal (up to $\alpha$-conversion, 104again) to some assumption of the goal. This definition assures that 105the theorem purporting to satisfy a goal does not depend on 106assumptions beyond the working assumptions of the goal. 107 108A justification is (rather confusingly) called 109a {\it proof\/} 110\index{proofs, in HOL logic@proofs, in \HOL{} logic!as ML function applications@as \ML{} function applications} 111\index{proof functions (same as justifications, validations)} 112in \HOL{}, following the \LCF{} usage; it is, as mentioned, 113an \ML{} function 114from a theorem list to a theorem. The \ML{} `proof' function 115corresponds to a proof 116\index{proofs, in HOL logic@proofs, in \HOL{} logic!as generated by tactics} in the 117logical sense (of a sequence of theorems depending on inference\index{inferences, in HOL logic@inferences, in \HOL{} logic!in goal-directed proof search} rules) 118only in that it must 119evaluate the \ML{} function corresponding 120to each inference rule on which the sequence depends 121in order to compute its \ml{thm}-valued result. (`Justification', or 122`validation', 123\index{validations} as is sometimes used, are less confusing terms for 124the \ML{} function in question.) 125The proof function, or justification, returned by a tactic is intended to map the 126list of theorems respectively achieving the subgoals to the 127theorem achieving the original goal; it justifies the decomposition 128into subgoals. 129 130A tactic is said to {\it solve\/} 131\index{solving, of goals} a goal if it reduces the goal to the 132empty set of subgoals. 133This depends, obviously, on there being at least one 134tactic that maps a goal to the empty subgoal list. The simplest 135tactic that does this is one that can recognize when a goal is 136achieved by an axiom or an existing theorem; in \HOL, the function 137\ml{ACCEPT\_TAC}\index{ACCEPT_TAC@\ml{ACCEPT\_TAC}} 138 does this. \ml{ACCEPT\_TAC} takes a theorem $th$ 139and produces a tactic that maps a value 140of type \ml{thm} to the empty list of subgoals. It justifies this 141`decomposition' by a proof function that maps the empty list of theorems 142to the theorem $th$. The use of this technical device, or other 143such tactics, ends the decomposition of subgoals, and allows the proof 144to be built up.\index{tactics!purpose of|)} 145 146Unlike theorems, goals need not be defined as an abstract type; they 147are transparent and can be constructed freely. Thus, an \ML{} type 148abbreviation is introduced for goals.\footnote{However, if goals were 149 an abstract type, the print abbreviation could be avoided where not 150 intended.}. The operations on goals are therefore just the ordinary 151pair selectors and constructor. 152Likewise, type abbreviations are introduced for justifications 153(proofs) and tactics. Conceptually, the following abbreviations are 154made in \HOL: 155 156\begin{hol} 157\index{goal@\ml{goal}} 158\index{tactic@\ml{tactic}} 159\index{proof@\ml{proof}} 160\index{tactics!ML type of@\ML{} type of} 161\begin{verbatim} 162 goal = term list * term 163 tactic = goal -> goal list * proof 164 proof = thm list -> thm 165\end{verbatim}\end{hol} 166 167\index{subgoals@\ml{subgoals}} In fact, the type 168\ml{goal~list~*~proof} is abbreviated in \ML{} to \ml{subgoals}, and 169the abbreviation of \ml{tactic} made indirectly through it. Thus, if 170$T$ is a tactic and $g$ is a goal, then applying $T$ to $g$ (\ie\ 171evaluating the \ML\ expression $T\ g$) results in an \ML{} value of 172type \ml{subgoals}, \ie\ a pair whose first component is a list of 173goals and whose second component has \ML{} type \ml{proof}. (The word 174`tactic' is occasionally used loosely to mean a tactic-valued 175function.) 176 177It does not follow, of course, from the type \ml{tactic} that a 178particular tactic is well-behaved. For example, 179suppose that 180$T\ g${\small\verb% = ([%}$g_1${\small\verb%;%}$\ldots 181${\small\verb%;%}$g_n${\small\verb%],%}$p${\small\verb%)%}, and that 182the subgoals $g_1$ , $\dots$, $g_n$ have been solved. 183That means that some 184theorems $th_1$ , $\dots$, $th_n$ have been proved 185such that each $th_i$ ($1\leq i\leq n$) achieves the goal $g_i$. 186The justification $p$ 187is intended to be a 188function that when applied to the list 189{\small\verb%[%}$th_1${\small\verb%;%}$\ldots${\small\verb%;%}$th_n${\small\verb%]%}, 190succeeds in returning a theorem, $th$, 191achieving the original goal $g$; but, of course, it might sometimes 192not succeed. If $p$ 193succeeds for every list of achieving theorems, then the tactic $T$ is 194said to be {\it valid\/}\index{validity, of tactics|(}. This does not guarantee, however, that 195the subgoals are solvable in the first place. If, in addition 196to being valid, a tactic always produces solvable subgoals from a 197solvable goal, it is called {\it strongly valid\/}. 198\index{strong validity, of tactics} 199 200Tactics can be perfectly useful without being 201strongly valid, or without 202even being valid; 203in fact, some of the most basic theorem proving strategies, expressed 204as tactics, are invalid or not strongly valid.\footnote{The subgoal 205 package, discussed in Section~\ref{sec:goalstack}, prevents the use of 206 invalid tactics when they are liable to result in unexpected 207 theorem results, but the \HOL{} system used directly allows 208 it.} 209An invalid tactic cannot result in the proof of false theorems; 210\index{consistency, of HOL logic@consistency, of \HOL{} logic|(} 211\index{security, in goal directed proof|(} 212theorems in \HOL{} are always the result of performing a proof in the 213basic logic, whether the proof is found by goal directed search 214or forward search.\footnote{`Invalid' is perhaps a misleading term, since 215 there is nothing logically amiss in the use of invalid tactics 216 or the theorems produced thereby; but the term has stuck over time.} 217However, an invalid tactic may produce an unintended theorem---one 218that does not achieve the original goal. The typical case is when a 219theorem purporting to achieve a goal actually depends on hypotheses 220that extend beyond the assumptions of the goal. The inconvenience to 221the \HOL{} user in this case is that the problem may be not 222immediately obvious; the default print format of theorems has 223hypotheses abbreviated as dots. Invalidity may also be the result of 224the failure 225\index{failure, of tactics|(} 226of the proof function, in the \ML{} sense of failure, when 227applied to a list of theorems (if, for example, the function were 228defined incorrectly); but again, no false theorems can result. 229Likewise, a tactic that is not strongly valid cannot result in a false 230theorem; the worst outcome of applying such a tactic is the production 231of unsolvable subgoals 232\index{consistency, of HOL logic@consistency, of \HOL{} logic|)} 233\index{security, in goal directed proof|)}\index{validity, of tactics|)}. 234 235Tactics are specified using the following notation: 236\index{notation!for specification of tactics} 237 238\begin{center} 239\begin{tabular}{c} \\ 240$\mathit{goal}$ \\ \hline \hline 241$\mathit{goal}_1\ \ \ \mathit{goal}_2 \ \ \ \ldots\ \ \ \mathit{goal}_n$ \\ 242\end{tabular} 243\end{center} 244 245\noindent For example, the 246tactic for decomposing conjunctions into 247two conjunct subgoals is called {\small\verb%CONJ_TAC%}. 248\index{CONJ_TAC@\ml{CONJ\_TAC}} It is described by: 249 250\begin{center} 251\begin{tabular}{c} \\ 252$ t_1${\small\verb% /\ %}$t_2$ \\ \hline \hline 253$t_1\ \ \ \ \ \ \ t_2$ \\ 254\end{tabular} 255\end{center} 256 257\noindent This indicates 258that {\small\verb%CONJ_TAC%} reduces a goal of the form 259{\small\verb%(%}$\Gamma${\small\verb%,%}$t_1${\small\verb%/\%}$t_2${\small\verb%)%} 260to subgoals 261{\small\verb%(%}$\Gamma${\small\verb%,%}$t_1${\small\verb%)%} and {\small\verb%(%}$\Gamma${\small\verb%,%}$t_2${\small\verb%)%}. 262The fact that the assumptions of the original goal 263are propagated unchanged to the two subgoals is indicated by the absence 264of assumptions in the notation. The notation gives no indication of the 265proof function. 266 267Another example is {\small\verb%INDUCT_TAC%}\index{INDUCT_TAC@\ml{INDUCT\_TAC}}\index{induction tactics}, 268the tactic for performing mathematical induction 269on the natural numbers: 270 271\begin{center} 272\begin{tabular}{c} \\ 273{\small\verb%!%}$n${\small\verb%.%}$t[n]$ \\ \hline \hline 274$t[${\small\verb%0%}$]$ {\small\verb% %} $\{t[n]\}\ t[${\small\verb%SUC %}$n]$ 275\end{tabular} 276\end{center} 277 278{\small\verb%INDUCT_TAC%} reduces a goal of the form 279{\small\verb%(%}$\Gamma${\small\verb%,!%}$n${\small\verb%.%}$t[n]${\small\verb%)%} to a basis subgoal 280{\small\verb%(%}$\Gamma${\small\verb%,%}$t[${\small\verb%0%}$]${\small\verb%)%} 281and an induction step subgoal 282{\small\verb%(%}$\Gamma\cup\{${\small\verb%%}$t[n]${\small\verb%%}$\}${\small\verb%,%}$t[${\small\verb%SUC %}$n]${\small\verb%)%}. 283The induction assumption 284is indicated in the tactic notation with set brackets. 285 286Tactics fail 287\index{failure, of tactics|)} 288(in the \ML{} sense) if they are applied to 289inappropriate 290goals. For example, {\small\verb%CONJ_TAC%} will fail if it is applied to a goal whose 291conclusion is not a conjunction. Some tactics never fail; for example 292{\small\verb%ALL_TAC%}\index{ALL_TAC@\ml{ALL\_TAC}} 293 294\begin{center} 295\begin{tabular}{c} \\ 296$t$ \\ \hline \hline 297$t$ 298\end{tabular} 299\end{center} 300 301\noindent is the identity tactic; 302\index{identity tactic} it reduces a goal 303{\small\verb%(%}$\Gamma${\small\verb%,%}$t${\small\verb%)%} 304to the single 305subgoal {\small\verb%(%}$\Gamma${\small\verb%,%}$t${\small\verb%)%}---\ie\ 306it has no effect. {\small\verb%ALL_TAC%} is useful for writing 307compound tactics, as discussed later (see Section~\ref{tacticals}). 308 309In just the way that the derived rule \ml{REWRITE\_RULE} 310\index{REWRITE_TAC@\ml{REWRITE\_TAC}|(} 311 is central 312to forward proof (Section~\ref{avra_rewrite}), the corresponding 313function \ml{REWRITE\_TAC} 314\index{rewriting!main tactic for|(} 315\index{rewriting!importance of, in goal directed proof|(} 316is central to goal 317directed proof. Given a goal and a list of equational theorems, 318\ml{REWRITE\_TAC} transforms the term component of the goal by 319applying the equations as left-to-right rewrites, recursively and 320to all depths, until no more changes can be made. Unless not 321required, the function includes as rewrites the same 322standard set of pre-proved tautologies 323\index{tautologies, in rewriting tactic} 324that \ml{REWRITE\_RULE} uses. 325By use of the tautologies, some subgoals can be solved 326internally by rewriting, and in that case, an empty list of subgoals 327is returned. The transformation of the goal is justified in each case by the 328appropriate chain of inferences. 329Rewriting often does a large share of the work in goal directed proof searches.\index{goal directed proof search!concepts of|)} 330\index{REWRITE_TAC@\ml{REWRITE\_TAC}|)} 331\index{rewriting!importance of, in goal directed proof|)} 332\index{rewriting!main tactic for|)} 333 334A simple example from list theory (Section~\ref{avra_list}) 335illustrates the use of tactics. 336A conjunctive goal is declared, and \ml{CONJ\_TAC} applied to it: 337 338\setcounter{sessioncount}{1} 339\begin{session}\begin{verbatim} 340- val g = ([]:term list,``(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])``); 341> val g = ([], ``(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])``) : 342 term list * term 343 344- val (gl1,p1) = CONJ_TAC g; 345> val gl1 = [([], ``HD[1;2;3] = 1``); ([], ``TL[1;2;3] = [2;3]``)] : 346 (term list * term) list 347 val p1 = fn : thm list -> thm 348\end{verbatim}\end{session} 349 350\noindent The subgoals are each rewritten, using the definitions of 351\ml{HD} and \ml{TL}: 352 353\begin{session}\begin{verbatim} 354- open listTheory 355 [...] 356 357- HD; 358> val it = |- !h t. HD (h::t) = h : thm 359 360- TL; 361> val it = |- !h t. TL (h::t) = t : thm 362 363- val (gl1_1,p1_1) = REWRITE_TAC[HD,TL](hd gl1); 364> val gl1_1 = [] : (term list * term) list 365 val p1_1 = fn : thm list -> thm 366 367- val (gl1_2,p1_2) = REWRITE_TAC[HD,TL](hd(tl gl1)); 368> val gl1_2 = [] : (term list * term) list 369 val p1_2 = fn : thm list -> thm 370\end{verbatim}\end{session} 371 372\noindent Both of the two subgoals are now solved, so the 373decomposition is complete and the proof can be built up in stages. 374First the theorems achieving the subgoals are proved, then from those, 375the theorem achieving the original goal: 376\vfill 377\newpage 378\begin{session}\begin{verbatim} 379- val th1 = p1_1[]; 380> val th1 = |- HD [1; 2; 3] = 1 : thm 381 382- val th2 = p1_2[]; 383> val th2 = |- TL [1; 2; 3] = [2; 3] : thm 384 385- p1[th1,th2]; 386> val it = |- (HD [1; 2; 3] = 1) /\ (TL [1; 2; 3] = [2;3]) : thm 387\end{verbatim}\end{session} 388 389\noindent Although only the theorems achieving the subgoals are `seen' here, 390the proof functions of the three tactic applications together perform 391the entire chain\index{goal directed proof search!generation of proofs by}\index{proofs, in HOL logic@proofs, in \HOL{} logic!as generated by tactics} 392 of inferences leading to the theorem achieving the goal. 393The same proof could be constructed by forward search, starting from 394the definitions of \ml{HD} and \ml{TL}, but not nearly as easily. 395 396The \HOL{} system provides a collection of pre-defined tactics (and 397\ml{tactic}-valued functions) that includes 398\ml{CONJ\_TAC}, \ml{INDUCT\_TAC}, \ml{ALL\_TAC} and 399\ml{REWRITE\_TAC}. The pre-defined tactics 400are adequate for many applications. In addition, there are two means of 401defining new tactics. 402\index{tactics!definition of new} 403Since a tactic\index{proof steps, as ML function applications@proof steps, as \ML{} function applications} is an \ML{} function, the user 404can define a new tactic directly in \ML. Definitions of this sort 405use \ML{} functions to construct the term part of the subgoals from 406the term part of the original goal (if any transformation is required); 407and they specify the justification, 408which expects a list of theorems achieving the subgoals and 409returns the theorem achieving (one hopes) the goal. 410The proof of the theorem is encoded in the definition of the justification 411 function; 412that is, the means for deriving the desired theorem from the theorems 413given. This typically involves references to axioms and 414primitive and defined inference rules, 415and is usually the more difficult part of the project. 416 417A 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}, 418whose definition in \HOL{} is as follows: 419 420\begin{hol} 421\index{CONJ_TAC@\ml{CONJ\_TAC}!ML implementation of@\ML{} implementation of} 422\begin{verbatim} 423 fun CONJ_TAC (asl,w) = 424 let val (l,r) = dest_conj w 425 in 426 ([(asl,l), (asl,r)],(fn [th1, th2] => CONJ th1 th2)) 427 end 428\end{verbatim}\end{hol} 429 430\noindent This shows how the subgoals are constructed, and how the 431proof function is specified in terms of the derived rule \ml{CONJ} 432(Section~\ref{avra_conj}). 433 434The second method is to compose 435\index{tactics!indirect implementation of} 436\index{tactics!compound} 437\index{proof construction} 438existing tactics by the use 439of \ML{} functions called {\it tacticals\/}. 440\index{tacticals} 441The tacticals provided in \HOL{} are listed in Section~\ref{tacticals}. 442For example, two existing tactics can be sequenced 443\index{sequencing!of tactics} 444\index{tactics!sequencing of} 445 by use of the 446tactical \ml{THEN}:\index{THEN@\ml{THEN}} 447if $T_1$ and 448$T_2$ are tactics, then the \ML{} expression $T_1${\small\verb% THEN %}$T_2$ 449evaluates to a tactic that first applies $T_1$ to a goal and then applies 450$T_2$ to each subgoal produced by $T_1$. The tactical {\small\verb%THEN%} is 451an infixed \ML{} function. Complex and powerful tactics can be 452constructed in this way; and new tacticals can also be defined, although 453this is unusual. 454 455The example from earlier 456is continued, to illustrate the use of the tactical \ml{THEN}: 457 458\begin{session}\begin{verbatim} 459- val (gl2,p2) = (CONJ_TAC THEN REWRITE_TAC [HD, TL])g; 460> val gl2 = [] : (term list * term) list 461 val p2 = fn : thm list -> thm 462 463- p2 []; 464> val it = |- (HD [1; 2; 3] = 1) /\ (TL [1; 2; 3] = [2; 3]) 465\end{verbatim}\end{session} 466 467\noindent The single tactic \ml{CONJ\_TAC THEN REWRITE\_TAC[HD;TL]} 468solves the goal in one single application. The chain of inference computed, 469however, is exactly the same as in the interactive proof; only the search is 470different. 471 472In general, the second method is both easier and more reliable. It is 473easier because it does not involve writing \ML{} procedures (usually 474rather complicated procedures); and more reliable because 475the composed tactics are valid 476\index{validity, of tactics} when the constituent tactics are valid, 477as a consequence of the way the tacticals are defined. Tactics written 478directly in \ML{} may fail 479\index{failure, of tactics!debugging} 480\index{failure, of tactics|(} 481\index{debugging, of tactics} 482\index{tactics!debugging of} 483in a variety of ways, and although, as usual, they cannot cause false 484theorems to appear, the failures can be difficult to understand and 485trace.\footnote{A possible extension to \HOL\ would be a `debugging 486 environment' for this class of tactic.} On the other hand, there are 487some proof strategies that cannot be implemented as compositions of 488existing tactics, and these have to be implemented directly in \ML. 489Certain sorts of inductions are an example of this; as well as tactics 490to support some personal styles of proof. 491 492Either sort of tactic can be difficult to apply by hand, as shown in 493the examples above. There can be a lot of book-keeping required to 494support such an activity. For this reason, most interactive 495theorem-proving uses the subgoal or goalstack package described in 496Section~\ref{sec:goalstack}. 497 498 499\subsection{Details of proving theorems} 500\label{using-tactics} 501 502When a theorem is proved that the user wishes to preserve for future use, 503it can be stored in the current theory 504by using the function \ml{save\_thm} (see Section~\ref{theoryprims}). 505 506To simplify the use of tactics there are three standard functions 507 508\index{TAC_PROOF@\ml{TAC\_PROOF}|pin} 509\index{prove_thm@\ml{prove\_thm}|pin} 510\index{PROVE@\ml{PROVE}|pin} 511\begin{holboxed}\begin{verbatim} 512 TAC_PROOF : (goal * tactic) -> thm 513 store_thm : (string * term * tactic) -> thm 514 prove : (term * tactic) -> thm 515\end{verbatim}\end{holboxed} 516 517\noindent \ml{TAC\_PROOF} takes a goal and a tactic, and applies the 518tactic to the goal; the goal can have assumptions. Executing 519\ml{store\_thm("foo",}$t$\ml{,}$T$\ml{)} proves the goal 520\ml{([],}$t$\ml{)} (\ie\ the goal with no assumptions and conclusion 521$t$) using tactic $T$ and saves the resulting theorem with name 522\ml{foo} in the current theory. Executing 523\ml{prove(}$t$\ml{,}$T$\ml{)} proves the goal \ml{([],}$t$\ml{)} using 524$T$ and returns the result without saving it. In all cases the 525evaluation fails if $T$ does not solve the goal. 526 527In short, \HOL{} provides a very general framework in which proof 528strategies can be designed, implemented, applied and tested. Tactics 529range from the very simple to the very advanced; in theory, a 530conventional automatic theorem prover could be expressed as a tactic or group 531of tactics. In contrast, some users never have need to go beyond the 532built in tactics of the system. The vital support that \HOL{} provides 533in all cases is the assurance that only theorems of the deductive system 534can be represented as theorems of the \HOL{} system---security is 535always preserved. 536 537\section{Some tactics built into HOL} 538\label{avra_builtin} 539 540This section contains a selection of the more commonly 541\index{tactics!list of some|(} 542used tactics in the \HOL{} system. (see \REFERENCE\ 543for the complete list, with fuller explanations.) 544 545It should be recalled that the \ML{} type \ml{thm\_tactic} abbreviates 546\ml{thm->tactic}, and the type \ml{conv} abbreviates \ml{term->thm}. 547 548\subsection{Acceptance of a theorem} 549 550 551\begin{holboxed}\index{ACCEPT_TAC@\ml{ACCEPT\_TAC}|pin} 552\begin{verbatim} 553 ACCEPT_TAC : thm_tactic 554\end{verbatim}\end{holboxed} 555 556\begin{itemize} 557 558\item{\bf Summary:} {\small\verb%ACCEPT_TAC %}$th$ 559is a tactic that solves any goal that is 560achieved by $th$. 561 562\index{forward proof!interfacing to goal directed} 563\item{\bf Use:} Incorporating forward proofs, or theorems already 564proved, into goal directed proofs. 565For example, one might reduce a goal $g$ to 566subgoals $g_1$, $\dots$, $g_n$ 567using a tactic $T$ and then prove theorems $th_1$ , $\dots$, $th_n$ 568respectively achieving 569these goals by forward proof. The tactic 570 571\[\ml{ T THENL[ACCEPT\_TAC }th_1\ml{;}\ldots\ml{;ACCEPT\_TAC }th_n\ml{]} 572\] 573 574would then solve $g$, where \ml{THENL} 575\index{THENL@\ml{THENL}} is the tactical that applies 576the respective elements of the tactic list to the subgoals produced 577by \ml{T} (see Section~\ref{avra_thenl}). 578 579\end{itemize} 580 581 582\subsection{Adding an assumption} 583 584\index{ASSUME_TAC@\ml{ASSUME\_TAC}|pin} 585\begin{holboxed}\begin{verbatim} 586 ASSUME_TAC : thm_tactic 587\end{verbatim}\end{holboxed} 588 589\begin{itemize} 590 591\item {\bf Summary:} {\small\verb%ASSUME_TAC |-%}$u$ adds $u$ as an assumption. 592\index{assumptions!tactic for adding} 593 594\begin{center} 595\begin{tabular}{c} \\ 596$t$ 597\\ \hline \hline 598$\{u\}t$ 599\\ 600\end{tabular} 601\end{center} 602 603\item{\bf Use:} Enriching the assumptions of a goal 604with definitions or previously proved theorems. 605 606\end{itemize} 607 608\subsection{Specialization}\index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!tactics for} 609 610\index{GEN_TAC@\ml{GEN\_TAC}|pin} 611\begin{holboxed}\begin{verbatim} 612 GEN_TAC : tactic 613\end{verbatim}\end{holboxed} 614 615\begin{itemize} 616 617\index{specialization tactic} 618\item{\bf Summary:} Specializes a universally quantified 619theorem to an arbitrary value. 620 621 622\begin{center} 623\begin{tabular}{c} \\ 624{\small\verb%!%}$x${\small\verb%.%}$t[x]$ 625\\ \hline \hline 626$t[x']$ 627\\ 628\end{tabular} 629\end{center} 630 631\noindent where $x'$ is a variant of $x$ 632not free in either goal or assumptions. 633 634\item{\bf Use:} Solving universally quantified goals. 635\ml{GEN\_TAC} is often the first step of a goal directed proof. 636{\small\verb%STRIP_TAC%} (see below) 637applies {\small\verb%GEN_TAC%} to universally quantified goals. 638\end{itemize} 639 640\subsection{Conjunction} 641 642\index{CONJ_TAC@\ml{CONJ\_TAC}|pin} 643\begin{holboxed}\begin{verbatim} 644 CONJ_TAC : tactic 645\end{verbatim}\end{holboxed} 646 647\begin{itemize} 648 649\index{conjunction, in HOL logic@conjunction, in \HOL{} logic!tactic for splitting of} 650\item{\bf Summary:} Splits a 651goal $t_1${\small\verb%/\%}$t_2$ into two 652subgoals, $t_1$ and $t_2$. 653 654\begin{center} 655\begin{tabular}{c} \\ 656$t_1${\small\verb% /\ %}$t_2$ 657\\ \hline \hline 658$t_1\ \ \ \ \ \ t_2$ 659\\ 660\end{tabular} 661\end{center} 662 663\item{\bf Use:} Solving conjunctive goals. 664{\small\verb%CONJ_TAC%} is invoked by {\small\verb%STRIP_TAC%} (see below). 665 666\end{itemize} 667 668\subsection{Discharging an assumption} 669\label{avradisch} 670 671\index{implication, in HOL logic@implication, in \HOL{} logic!tactics for} 672\index{DISCH_TAC@\ml{DISCH\_TAC}|pin} 673\begin{holboxed}\begin{verbatim} 674 DISCH_TAC : tactic 675\end{verbatim}\end{holboxed} 676 677\begin{itemize} 678 679\item{\bf Summary:} Moves the antecedant 680of an implicative goal into the assumptions, leaving the consequent 681as the term component. 682 683\begin{center} 684\begin{tabular}{c} \\ 685$u${\small\verb% ==> %}$v$ 686\\ \hline \hline 687$\{u\}v$ 688\\ 689\end{tabular} 690\end{center} 691 692 693\item{\bf Use:} Solving goals of the form 694$u${\small\verb% ==> %}$v$ 695by assuming $u$ and then solving 696$v$ under the assumption. 697{\small\verb%STRIP_TAC%} (see below) invokes 698{\small\verb%DISCH_TAC%} on implicative goals. 699\end{itemize} 700 701\subsection{Combined simple decompositions} 702 703\index{STRIP_TAC@\ml{STRIP\_TAC}|pin} 704\begin{holboxed}\begin{verbatim} 705 STRIP_TAC : tactic 706\end{verbatim}\end{holboxed} 707 708\begin{itemize} 709 710\item{\bf Summary:} Breaks a goal apart. 711{\small\verb%STRIP_TAC%} removes one outer connective from the goal, using 712{\small\verb%CONJ_TAC%}, {\small\verb%DISCH_TAC%}, {\small\verb%GEN_TAC%}, 713and other tactics. 714If the goal has the form $t_1${\small\verb%/\%}$\cdots${\small\verb%/\%}$t_n${\small\verb% ==> %}$t$ 715then {\small\verb%DISCH_TAC%} makes each $t_i$ into a separate assumption. 716 717\item{\bf Use:} Useful for splitting a goal up into manageable pieces. 718Often the best thing to do first is {\small\verb%REPEAT STRIP_TAC%}, 719where \ml{REPEAT} is the tactical that repeatedly applies a tactic 720until it fails (see Section~\ref{avra_repeat}). 721\end{itemize} 722 723 724 725\subsection{Substitution} 726 727\index{SUBST_TAC@\ml{SUBST\_TAC}|pin} 728\begin{holboxed}\begin{verbatim} 729 SUBST_TAC : thm list -> tactic 730\end{verbatim}\end{holboxed} 731 732\begin{itemize} 733 734\item{\bf Summary:} 735{\small\verb%SUBST_TAC[|-%}$u_1${\small\verb%=%}$v_1${\small\verb%;%}$\ldots${\small\verb%;|-%}$u_n${\small\verb%=%}$v_n${\small\verb%]%} 736changes\index{substitution, tactic for} each sub-term 737$t[u_1,\ldots ,u_n]$ of the goal to 738$t[v_1,\ldots ,v_n]$ 739by substitution. 740 741\item{\bf Use:} 742Useful in situations where {\small\verb%REWRITE_TAC%} 743\index{REWRITE_TAC@\ml{REWRITE\_TAC}} does too much, 744or would loop. 745\end{itemize} 746 747 748\subsection{Case analysis on a boolean term} 749\index{case analysis, in HOL logic@case analysis, in \HOL{} logic!tactics for|(} 750 751\index{ASM_CASES_TAC@\ml{ASM\_CASES\_TAC}|(} 752\begin{holboxed}\begin{verbatim} 753 ASM_CASES_TAC : term -> tactic 754\end{verbatim}\end{holboxed} 755 756\begin{itemize} 757 758\item{\bf Summary:} \ml{ASM\_CASES\_TAC} $u$ , where $u$ is a 759boolean-valued term, does case analysis on $u$. 760 761\begin{center} 762\begin{tabular}{c} \\ 763$t$ 764\\ \hline \hline 765$\{u\}t\ \ \ \ \ \{${\small\verb%~%}$u\}t$ 766\\ 767\end{tabular} 768\end{center} 769 770\item{\bf Use:} Case analysis. 771\end{itemize} 772\index{ASM_CASES_TAC@\ml{ASM\_CASES\_TAC}|)} 773 774\subsection{Case analysis on a disjunction} 775 776 777\begin{holboxed} 778\index{DISJ_CASES_TAC@\ml{DISJ\_CASES\_TAC}|pin} 779\index{disjunction, in HOL logic@disjunction, in \HOL{} logic!tactic for case splits on} 780\begin{verbatim} 781 DISJ_CASES_TAC : thm_tactic 782\end{verbatim}\end{holboxed} 783 784\begin{itemize} 785 786\item{\bf Summary:} 787{\small\verb%DISJ_CASES_TAC |- %}$u${\small\verb% \/ %}$v$ 788splits a goal into two cases: one with $u$ 789as an assumption 790and the other with $v$ as an assumption. 791 792\begin{center} 793\begin{tabular}{c} \\ 794$t$ 795\\ \hline \hline 796$\{u\}t\ \ \ \ \ \{v\}t$ 797\\ 798\end{tabular} 799\end{center} 800 801\item{\bf Use:} Case analysis. The 802tactic {\small\verb%ASM_CASES_TAC%} is defined in \ML{} by 803 804{\small\begin{verbatim} 805 let ASM_CASES_TAC t = DISJ_CASES_TAC(SPEC t EXCLUDED_MIDDLE) 806\end{verbatim}} 807 808 809\noindent where {\small\verb%EXCLUDED_MIDDLE%} is 810the theorem {\small\verb%|- !t. t \/ ~t%}. 811 812\end{itemize} 813\index{case analysis, in HOL logic@case analysis, in \HOL{} logic!tactics for|)} 814 815\subsection{Rewriting} 816\label{rewrite} 817 818\index{rewriting!main tactic for|(} 819\begin{holboxed} 820\index{REWRITE_TAC@\ml{REWRITE\_TAC}|pin} 821\begin{verbatim} 822 REWRITE_TAC : thm list -> tactic 823\end{verbatim}\end{holboxed} 824 825 826\begin{itemize} 827\item{\bf Summary:} {\small\verb%REWRITE_TAC[%}$th_1${\small\verb%;%}$\ldots${\small\verb%;%}$th_n${\small\verb%]%} 828transforms the term part of a goal by rewriting 829it with the given theorems $th_1$, $\dots$, $th_n$, 830and the set of pre-proved standard tautologies\index{tautologies, in rewriting tactic}. 831 832 833\begin{center} 834\begin{tabular}{c} \\ 835$\{t_1, \ldots , t_m\}t$ 836\\ \hline \hline 837$\{t_1, \ldots , t_m\}t'$ 838\\ 839\end{tabular} 840\end{center} 841 842\noindent where $t'$ is obtained from $t$ as described. 843 844\item{\bf Use:} Advancing goals by using definitions and 845previously proved theorems (lemmas).\index{lemmas} 846 847 848\item{\bf Some other rewriting tactics} (based on {\small\verb%REWRITE_TAC%}) are: 849\begin{enumerate} 850\item {\small\verb%ASM_REWRITE_TAC%}\index{ASM_REWRITE_TAC@\ml{ASM\_REWRITE\_TAC}} 851 adds the assumptions of the goal to the list of 852theorems used for rewriting. 853\index{PURE_ASM_REWRITE_TAC@\ml{PURE\_ASM\_REWRITE\_TAC}} 854\item {\small\verb%PURE_ASM_REWRITE_TAC%} is like {\small\verb%ASM_REWRITE_TAC%}, but it 855doesn't use any built-in rewrites. 856\index{PURE_REWRITE_TAC@\ml{PURE\_REWRITE\_TAC}} 857\item {\small\verb%PURE_REWRITE_TAC%} uses neither the assumptions nor the built-in rewrites. 858\index{FILTER_ASM_REWRITE_TAC@\ml{FILTER\_ASM\_REWRITE\_TAC}} 859\item {\small\verb%FILTER_ASM_REWRITE_TAC %}$p${\small\verb% [%}$th_1${\small\verb%;%}$\ldots${\small\verb%;%}$th_n${\small\verb%]%} 860simplifies the goal by rewriting 861it with the explicitly given theorems $th_1$ , $\dots$, $th_n$ , 862together with those 863assumptions of the goal which satisfy the predicate $p$ and also 864the standard rewrites. 865 866\end{enumerate} 867\end{itemize} 868 869\index{rewriting!main tactic for|)} 870 871 872\subsection{Resolution by Modus Ponens} 873 874\index{implication, in HOL logic@implication, in \HOL{} logic!tactics for} 875\index{IMP_RES_TAC@\ml{IMP\_RES\_TAC}|pin} 876\begin{holboxed}\begin{verbatim} 877 IMP_RES_TAC : thm -> tactic 878\end{verbatim}\end{holboxed} 879 880\begin{itemize} 881 882\index{resolution tactics} 883\item{\bf Summary:} {\small\verb%IMP_RES_TAC %}$th$ does a limited amount of 884automated theorem proving in the form of forward inference; it 885`resolves' the theorem $th$ with the 886assumptions of the goal 887and adds any new results to the assumptions. The specification for 888\ml{IMP\_RES\_TAC} is: 889 890 891\begin{center} 892\begin{tabular}{c} \\ 893$\{t_1,\ldots,t_m\}t$ 894\\ \hline \hline 895$\{t_1,\ldots,t_m,u_1,\ldots,u_n\}t$ 896\\ 897\end{tabular} 898\end{center} 899 900\noindent where $u_1$, $\dots$, $u_n$ 901are derived by `resolving' the theorem $th$ with the existing assumptions 902$t_1$, $\dots$, $t_m$. 903Resolution in \HOL{} is not classical resolution, but just Modus Ponens with 904one-way pattern matching (not unification) and term and type instantiation. The 905general case is where $th$ is of the canonical form 906 907$\ \ \ ${\small\verb%|- !%}$x_1$$\ldots x_p${\small\verb%.%}$v_1$ {\small\verb%==>%} $v_2$ {\small\verb%==>%} $\ldots$ {\small\verb%==>%} $v_q$ {\small\verb%==>%} $v$ 908 909\noindent {\small\verb%IMP_RES_TAC %}$th$ then tries to specialize $x_1$, 910$\dots$, $x_p$ in succession so that $v_1$, $\dots$, $v_q$ match members of 911$\{t_1,\ldots ,t_m\}$. Each time a match is found for some antecedent $v_i$, 912for $i$ successively equal to $1$, $2$, \dots, $q$, a term and type 913instantiation is made and the rule of Modus Ponens is applied. If all the 914antecedents $v_i$ (for $1 \leq i \leq q$) can be dismissed in this way, then 915the appropriate instance of $v$ is added to the assumptions. Otherwise, if only 916some initial sequence $v_1$, \dots, $v_k$ (for some $k$ where $1 < k < q$) of 917the assumptions can be dismissed, then the remaining implication: 918 919$\ \ \ ${\small\verb%|- %} $v_{k+1}$ {\small\verb%==>%} $\ldots$ {\small\verb%==>%} $v_q$ {\small\verb%==>%} $v$ 920 921\noindent is added to the assumptions. 922 923For a more detailed description of resolution and \ml{IMP\_RES\_TAC}, see 924\REFERENCE. (See also the Cambridge \LCF\ Manual \cite{new-LCF-man}.) 925 926\item{\bf Use:} Deriving new results from a previously proved implicative 927theorem, in combination with the current assumptions, so that subsequent 928tactics can use these new results. 929 930\end{itemize} 931 932 933 934 935\subsection{Identity} 936 937\index{ALL_TAC@\ml{ALL\_TAC}|pin} 938\begin{holboxed}\begin{verbatim} 939 ALL_TAC : tactic 940\end{verbatim}\end{holboxed} 941 942\begin{itemize} 943\index{identity tactic}\index{tactics!identity for} 944\index{THEN@\ml{THEN}} 945\item{\bf Summary:} The identity tactic for the tactical {\small\verb%THEN%} 946(see Section~\ref{tactics}). Useful for writing tactics. 947 948\item{\bf Use:} 949\begin{enumerate} 950\index{REPEAT@\ml{REPEAT}} 951\item Writing tacticals (see description of {\small\verb%REPEAT%} 952in Section~\ref{tacticals}). 953\index{THENL@\ml{THENL}} 954\item With {\small\verb%THENL%} (see Section~\ref{avra_thenl}); 955for example, if tactic $T$ produces two subgoals 956$T_1$ is to be applied to the first while 957nothing is to be done to the second, 958then $T${\small\verb% THENL[%}$T_1${\small\verb%;ALL_TAC]%} is the 959tactic required. 960\end{enumerate} 961\end{itemize} 962 963\subsection{Null} 964 965\index{NO_TAC@\ml{NO\_TAC}|pin} 966\begin{holboxed}\begin{verbatim} 967 NO_TAC : tactic 968\end{verbatim}\end{holboxed} 969 970\begin{itemize} 971\item{\bf Summary:} Tactic that always fails. 972 973\item{\bf Use:} Writing tacticals. 974\end{itemize} 975 976 977\subsection{Splitting logical equivalences} 978 979 980\begin{holboxed} 981\index{EQ_TAC@\ml{EQ\_TAC}|pin} 982\index{equality, in HOL logic@equality, in \HOL{} logic!tactic for splitting} 983\begin{verbatim} 984 EQ_TAC : tactic 985\end{verbatim}\end{holboxed} 986 987\begin{itemize} 988 989\item{\bf Summary:} 990{\small\verb%EQ_TAC%} 991splits an equational goal into two implications (the `if-case' and 992the `only-if' case): 993 994\begin{center} 995 996 997 998\begin{tabular}{c} \\ 999$u\ \ml{=}\ v$ 1000\\ \hline \hline 1001$u\ \ml{==>}\ v\ \ \ \ \ v\ \ml{==>}\ u$ 1002\\ 1003\end{tabular} 1004\end{center} 1005 1006\item{\bf Use:} Proving logical equivalences, \ie\ goals of the form 1007``$u$\ml{=}$v$'' where $u$ and $v$ are boolean terms. 1008 1009\end{itemize} 1010 1011\subsection{Solving existential goals} 1012 1013 1014\begin{holboxed} 1015\index{EXISTS_TAC@\ml{EXISTS\_TAC}|pin} 1016\index{existential quantifier, in HOL logic@existential quantifier, in \HOL{} logic!tactic for} 1017\begin{verbatim} 1018 EXISTS_TAC : term -> tactic 1019\end{verbatim}\end{holboxed} 1020 1021\begin{itemize} 1022 1023\item{\bf Summary:} 1024{\small\verb%EXISTS_TAC "%}$u${\small\verb%"%} 1025reduces an existential goal {\small\verb%!%}$x${\small\verb%. %}$t[x]$ 1026to the subgoal $t[u]$. 1027 1028\begin{center} 1029\begin{tabular}{c} \\ 1030$\ml{!}x\ml{.} t[x]$ 1031\\ \hline \hline 1032$t[u]$ 1033\\ 1034\end{tabular} 1035\end{center} 1036 1037\item{\bf Use:} Proving existential goals. 1038 1039\item{\bf Comment:} \ml{EXISTS\_TAC} is a crude way of solving 1040existential goals, but it is the only built-in tactic for this 1041purpose. A more powerful approach uses Prolog-style `logic variables' 1042(\ie\ meta-variables) 1043that can be progressively refined towards the eventual witness. 1044Implementing this requires goals to contain an environment giving the binding 1045of logic variables to terms. Details (in the context of \LCF) are given 1046in a paper by Stefan Soko\l owski \cite{Stefan}. 1047 1048\end{itemize} 1049\index{tactics!list of some|)} 1050 1051\section{Tacticals} 1052\label{tacticals} 1053 1054\index{tactics!tacticals for|(} 1055\index{tacticals|(} 1056\index{tacticals!list of some|(} 1057\index{tacticals!purpose of} 1058A {\it tactical\/} is not represented by a single \ML{} type, 1059but is in general 1060an \ML{} function that returns a tactic (or tactics) as result. 1061Tacticals may take parameters, and this is reflected in the variety of 1062\ML{} types that the built-in tacticals have. 1063Tacticals are used for building compound tactics.\index{compound tactics, in HOL system@compound tactics, in \HOL{} system} 1064\index{tactics!compound} 1065Some important tacticals in 1066the \HOL{} system 1067are listed below. 1068For a complete list of the tacticals in \HOL{} see \REFERENCE. 1069 1070\subsection{Alternation}\index{alternation!of tactics|(}\index{tactics!alternation of} 1071 1072\index{ORELSE@\ml{ORELSE}|pin} 1073\begin{holboxed}\begin{verbatim} 1074 ORELSE : tactic -> tactic -> tactic 1075\end{verbatim}\end{holboxed} 1076 1077 1078The tactical {\small\verb%ORELSE%} 1079is an \ML{} infix. If $T_1$ and $T_2$ are tactics, 1080\index{tacticals!for alternation} 1081then the \ML{} expression $T_1${\small\verb% ORELSE %}$T_2$ 1082evaluates to a tactic which applies $T_1$ unless that fails; 1083if it fails, 1084it applies $T_2$. \ml{ORELSE} is defined in \ML\ 1085as a curried infix by 1086 1087\begin{hol}\begin{verbatim} 1088 (T1 ORELSE T2) g = T1 g ? T2 g 1089\end{verbatim}\end{hol}\index{alternation!of tactics|)} 1090 1091 1092\subsection{First success} 1093 1094\index{FIRST@\ml{FIRST}|pin} 1095\begin{holboxed}\begin{verbatim} 1096 FIRST : tactic list -> tactic 1097\end{verbatim}\end{holboxed} 1098 1099The tactical \ml{FIRST} applies the first tactic, in a list 1100of tactics, that succeeds. 1101 1102\begin{hol}\begin{alltt} 1103 FIRST [\(T\sb{1}\);\(T\sb{2}\);\(\ldots\);\(T\sb{n}\)] = \(T\sb{1}\) ORELSE \(T\sb{2}\) ORELSE \(\ldots\) ORELSE \(T\sb{n}\) 1104\end{alltt}\end{hol} 1105 1106 1107 1108\subsection{Change detection} 1109 1110\index{CHANGED_TAC@\ml{CHANGED\_TAC}|pin} 1111\begin{holboxed}\begin{verbatim} 1112 CHANGED_TAC : tactic -> tactic 1113\end{verbatim}\end{holboxed} 1114 1115 1116\ml{CHANGED\_TAC\ $T$\ $g$} fails if the subgoals 1117produced by $T$ are just \ml{[$g$]}; otherwise it is equivalent 1118to $T\ g$. It is defined by the following, where 1119{\small\verb%set_equal : * list -> * list -> bool%} tests whether two lists 1120denote the same set (\ie\ contain the same elements). 1121 1122 1123\begin{hol}\begin{verbatim} 1124 letrec CHANGED_TAC tac g = 1125 let gl,p = tac g in 1126 if set_equal gl [g] then fail else (gl,p) 1127\end{verbatim}\end{hol} 1128 1129 1130 1131\subsection{Sequencing} 1132\index{sequencing!of tactics|(} 1133\index{tacticals!for sequencing|(} 1134\index{tactics!sequencing of|(} 1135\index{THEN@\ml{THEN}!ML implementation of@\ML{} implementation of|(} 1136 1137\begin{holboxed}\index{THEN@\ml{THEN}|pin} 1138\begin{verbatim} 1139 THEN : tactic -> tactic -> tactic 1140\end{verbatim}\end{holboxed} 1141 1142 1143The tactical {\small\verb%THEN%} is an \ML{} infix. If $T_1$ and $T_2$ are tactics, 1144then the \ML{} expression $T_1${\small\verb% THEN %}$T_2$ evaluates to a tactic 1145which first applies $T_1$ and then applies $T_2$ to each subgoal produced by 1146$T_1$. Its definition 1147 in \ML{} is complex (and due to Milner)\index{Milner, R.} but worth 1148understanding as an exercise in \ML. It is an \ML{} curried infix. 1149 1150\begin{hol}\begin{verbatim} 1151 let ((T1:tactic) THEN (T2:tactic)) g = 1152 let gl,p = T1 g 1153 in 1154 let gll,pl = split(map T2 gl) 1155 in 1156 (flat gll, (p o mapshape(map length gll)pl));; 1157\end{verbatim}\end{hol} 1158 1159\noindent Here are 1160the definitions of the \ML{} functions \ml{map}, \ml{split}, \ml{o}, 1161\ml{length}, \ml{flat} and \ml{mapshape}: 1162 1163%\begin{itemize} 1164\bigskip 1165 1166\index{map@\ml{map}} 1167{\small\verb%map : (* -> **) -> * list -> ** list%} 1168 1169\medskip 1170 1171\begin{hol}\begin{alltt} 1172 map \(f\) [\(x\sb{1}\);\(\ldots\);\(x\sb{n}\)] = [\(f\) \(x\sb{1}\);\(\ldots\);\(f\) \(x\sb{n}\)] 1173\end{alltt}\end{hol} 1174 1175\medskip 1176 1177\index{split@\ml{split}} 1178{\small\verb%split : (* # **) list -> (* list # ** list)%} 1179 1180\medskip 1181 1182\begin{hol}\begin{alltt}\ split[(\(x\sb{1}\),\(y\sb{1}\));\(\ldots\);(\(x\sb{n}\),\(y\sb{n}\))] = ([\(x\sb{1}\);\(\ldots\);\(x\sb{n}\)],[\(y\sb{1}\);\(\ldots\);\(y\sb{n}\)]) 1183\end{alltt}\end{hol} 1184 1185 1186\medskip 1187 1188{\small\verb%$o : ((* -> **) # (*** -> *)) -> *** -> **$%} 1189 (an infix)\index{function composition, in ML@function composition, in \ML} 1190 1191\medskip 1192 1193\begin{hol} 1194\begin{alltt} 1195 (\(f\) o \(g\)) \(x\) = \(f\)(\(g\) \(x\)) 1196\end{alltt}\end{hol} 1197\index{ function composition operator, in ML@{\small\verb+o+} (function composition operator, in \ML)} 1198 1199\medskip 1200 1201\index{length@\ml{length}} 1202{\small\verb%length : * list -> int%} 1203 1204\medskip 1205 1206\begin{hol}\begin{alltt} 1207 length[\(x\sb{1}\);\(\ldots\);\(x\sb{n}\)] = n 1208\end{alltt}\end{hol} 1209 1210\medskip 1211 1212 1213{\small\verb%flat : (* list) list -> * list%}\index{flat@\ml{flat}} 1214 1215 1216\medskip 1217 1218\begin{hol}\begin{alltt} 1219 flat[[\({x\sb{1}}\sb{1}\);\(\ldots\);\({x\sb{1}}\sb{m\sb{1}}\)];[\({x\sb{2}}\sb{1}\);\(\ldots\);\({x\sb{2}}\sb{m\sb{2}}\)];\(\ldots\);[\({x\sb{n}}\sb{1}\);\(\ldots\);\({x\sb{n}}\sb{m\sb{n}}\)]] = 1220 [\({x\sb{1}}\sb{1}\);\(\ldots\);\({x\sb{1}}\sb{m\sb{1}}\);\({x\sb{2}}\sb{1}\);\(\ldots\);\({x\sb{2}}\sb{m\sb{2}}\); \(\ldots\) ;\({x\sb{n}}\sb{1}\);\(\ldots\);\({x\sb{n}}\sb{m\sb{n}}\)] 1221\end{alltt}\end{hol} 1222 1223\medskip 1224 1225{\small\verb%mapshape : int list -> (* list -> **) list -> * list -> ** list%}\index{mapshape@\ml{mapshape}} 1226 1227 1228\medskip 1229 1230\begin{hol}\begin{alltt} 1231 mapshape 1232 [\(m\sb{1}\);\(\ldots\);\(m\sb{n}\)] 1233 [\(f\sb{1}\);\(\ldots\);\(f\sb{n}\)] 1234 [\({x\sb{1}}\sb{1}\);\(\ldots\);\({x\sb{1}}\sb{m\sb{1}}\);\({x\sb{2}}\sb{1}\);\(\ldots\);\({x\sb{2}}\sb{m\sb{2}}\); \(\ldots\) ;\({x\sb{n}}\sb{1}\);\(\ldots\);\({x\sb{n}}\sb{m\sb{n}}\)] = 1235 [\(f\sb{1}\)[\({x\sb{1}}\sb{1}\);\(\ldots\);\({x\sb{1}}\sb{m\sb{1}}\)];\(f\sb{2}\)[\({x\sb{2}}\sb{1}\);\(\ldots\);\({x\sb{2}}\sb{m\sb{2}}\)]; \(\ldots\) ;\(f\sb{n}\)[\({x\sb{n}}\sb{1}\);\(\ldots\);\({x\sb{n}}\sb{m\sb{n}}\)]] 1236\end{alltt}\end{hol} 1237 1238%\end{itemize} 1239 1240\bigskip 1241 1242Suppose \ml{$T_1\ g$ = ($gl$,$p$)} where \ml{$gl$=[$g_1$;$\ldots$;$g_n$]}. 1243Suppose also that 1244for $i$ between $1$ and $n$ it is the case that 1245\ml{$T_2\ g_i$ = ([${g_i}_1$;$\ldots$;${g_i}_{m_i}$],$p_i$)}. 1246Then \ml{split(map $T_2$ $gl$)} will evaluate to the 1247pair \ml{($gll$,$pl$)} of a subgoal list and a proof function, where 1248 1249\bigskip 1250 1251\ml{$gll$ = [[${g_1}_1$;$\ldots$;${g_1}_{m_1}$];[${g_2}_1$;$\ldots$;${g_2}_{m_2}$]; 1252$\ \ldots\ $;[${g_n}_1$;$\ldots$;${g_n}_{m_n}$]]} 1253 1254\bigskip 1255 1256\noindent and 1257\ml{$pl$ = [$p_1$;$\ldots$;$p_n$]}. Note that 1258 1259\bigskip 1260 1261\ml{map length $gll$ = [$m_1$;$\ldots$;$m_n$]} 1262 1263\bigskip 1264 1265\noindent and that 1266 1267\bigskip 1268 1269\ml{flat $gll$ = [${g_1}_1$;$\ldots$;${g_1}_{m_1}$;${g_2}_1$;$\ldots$;${g_2}_{m_2}$; 1270$\ \ldots\ $;${g_n}_1$;$\ldots$;${g_n}_{m_n}$]} 1271 1272\bigskip 1273 1274Suppose now that, for $i$ between $1$ and $n$, the theorems 1275${th_i}_1$, $\dots$, ${th_i}_{m_i}$ achieve 1276the goals ${g_i}_1$, $\dots$, ${g_i}_{m_i}$, respectively. 1277It will follow that if $T_2$ is valid 1278then for $i$ between $1$ and $n$ 1279the result of applying $p_i$ to the list of 1280theorems \ml{[${th_i}_1$;$\ldots$;${th_i}_{m_i}$]} 1281will be a theorem, $th_i$ say, which achieves 1282$g_i$. 1283Now if $T_1$ is valid then \ml{$p$[$th_1$;$\ldots$;$th_n$]} 1284will evaluate to a theorem, 1285$th$ say, 1286that achieves the goal $g$. Thus 1287 1288\begin{hol}\begin{alltt} 1289 \(p\) 1290 (mapshape 1291 (map length \(gll\)) 1292 \(pl\) 1293 [\({th\sb{1}}\sb{1}\);\(\ldots\);\({th\sb{1}}\sb{m\sb{1}}\);\({th\sb{2}}\sb{1}\);\(\ldots\);\({th\sb{2}}\sb{m\sb{2}}\);\(\ \ldots\ \) ;\({th\sb{n}}\sb{1}\);\(\ldots\);\({th\sb{n}}\sb{m\sb{n}}\)]) = 1294 1295 \(p\)([\(p\sb{1}\)[\({th\sb{1}}\sb{1}\);\(\ldots\);\({th\sb{1}}\sb{m\sb{1}}\)];\(p\sb{2}\)[\({th\sb{2}}\sb{1}\);\(\ldots\);\({th\sb{2}}\sb{m\sb{2}}\)];\(\ \ldots\ \);\(p\sb{n}\)[\({th\sb{n}}\sb{1}\);\(\ldots\);\({th\sb{n}}\sb{m\sb{n}}\)]]) = 1296 1297 \(p\)([\(th\sb{1}\);\(\ldots\);\(th\sb{n}\)]) = 1298 1299 \(th\) 1300\end{alltt}\end{hol} 1301 1302This shows that 1303\index{justifications, in goal-directed proof search!THEN example of@\ml{THEN} example of} 1304\index{proof functions (same as justifications, validations)!THEN example of@\ml{THEN} example of} 1305\ml{$p$ o mapshape(map length $gll$)$pl$} 1306is a function that, when 1307applied to a list of theorems respectively 1308achieving \ml{flat $gll$}, returns a theorem 1309(namely $th$) that achieves $g$.\index{sequencing!of tactics|)} 1310\index{tacticals!for sequencing|)} 1311\index{THEN@\ml{THEN}!ML implementation of@\ML{} implementation of|)} 1312 1313\subsection{Selective sequencing} 1314 1315\index{THENL@\ml{THENL}} 1316\begin{holboxed}\begin{verbatim} 1317 THENL : tactic -> tactic list -> tactic 1318\end{verbatim}\end{holboxed} 1319\label{avra_thenl} 1320 1321\index{selective sequencing tactical} 1322If tactic $T$ produces $n$ subgoals and $T_1$, $\dots$, 1323$T_n$ are tactics 1324then $T${\small\verb% THENL [%}$T_1${\small\verb%;%}$\ldots${\small\verb%;%}$T_n${\small\verb%]%} 1325is a tactic which first applies $T$ and then 1326applies $T_i$ to the $i$th subgoal produced by $T$. 1327The tactical {\small\verb%THENL%} is useful if one wants to apply different 1328tactics to different subgoals. 1329 1330Here is the definition of \ml{THENL}: 1331 1332\begin{hol}\begin{verbatim} 1333 let ((T:tactic) THENL (Tl:tactic list)) g = 1334 let gl,p = T g 1335 in 1336 let gll,pl = (split(map (\(T,g). T g) Tgl) 1337 where Tgl = combine(Tl,gl) ? failwith `THENL`) 1338 in 1339 (flat gll, (p o mapshape(map length gll)pl)) 1340\end{verbatim}\end{hol} 1341 1342\noindent The understanding of this procedure is left as an exercise!\index{tactics!sequencing of|)} 1343 1344\subsection{Successive application} 1345 1346 1347 1348\begin{holboxed} 1349\index{EVERY, the ML function@\ml{EVERY}, the \ML{} function|pin} 1350\begin{verbatim} 1351 EVERY : tactic list -> tactic 1352\end{verbatim}\end{holboxed} 1353 1354\index{tacticals!for successive application} 1355\index{successive application!tactical for} 1356The tactical \ml{EVERY} applies a list of tactics one after the other. 1357 1358 1359\begin{hol}\begin{alltt} 1360 EVERY [\(T\sb{1}\);\(T\sb{2}\);\(\ldots\);\(T\sb{n}\)] = \(T\sb{1}\) THEN \(T\sb{2}\) THEN \(\ldots\) THEN \(T\sb{n}\) 1361\end{alltt}\end{hol} 1362 1363 1364 1365\subsection{Repetition} 1366 1367\begin{holboxed}\index{REPEAT@\ml{REPEAT}|pin} 1368\begin{verbatim} 1369 REPEAT : tactic -> tactic 1370\end{verbatim}\end{holboxed} 1371\label{avra_repeat} 1372 1373If $T$ is a 1374tactic then {\small\verb%REPEAT %}$T$ is a tactic\index{tactics!repetition of} 1375\index{tacticals!for repetition}\index{repetition!of tactics} 1376that repeatedly applies 1377$T$ until it fails. It is defined in \ML{} by: 1378 1379{\small\baselineskip\HOLSpacing\begin{verbatim} 1380 letrec REPEAT T g = ((T THEN REPEAT T) ORELSE ALL_TAC) g 1381\end{verbatim}} 1382 1383\noindent (The extra argument {\small\verb%g%} is needed because \ML{} does not use 1384lazy evaluation.) 1385\index{tacticals|)} 1386\index{tacticals!list of some|)} 1387\index{tactics!tacticals for|)} 1388 1389\section{Tactics for manipulating assumptions} 1390\label{asm-manip} 1391 1392\index{tactics!for manipulating assumptions|(} 1393There are in general two kinds of tactics\index{tactics!term transforming}\index{tactics!assumption transforming} 1394 in \HOL: those that transform the 1395conclusion of a goal without affecting the assumptions, and those that 1396do (also or only) affect the assumptions. The various tactics that 1397rewrite\index{rewriting!main tactic for} 1398 are typical of the first class; those that do `resolution' 1399\index{resolution tactics} belong to 1400the second. Often, many of the steps of a proof in \HOL{} are carried 1401out `behind the scenes' on the assumptions, by tactics of the second sort. 1402A tactic that in some way changes the assumptions must also have a 1403justification that `knows how' to restore the corresponding hypotheses of 1404the theorem achieving the subgoal. All of this is explicit, and can be 1405examined by a user moving about the subgoal-proof tree.\footnote{The current 1406subgoal package makes this difficult, but the point still holds.} 1407Using these tactics in the most straightforward way, the assumptions at any 1408point in a goal-directed proof, \ie\ at any node in the subgoal tree, 1409\index{subgoal tree!in proof construction} 1410\index{tree of subgoals, in proof construction} form 1411an unordered record of every assumption made, but not yet dismissed, up to that 1412point. 1413 1414In practice, the straightforward use of assumption-changing 1415\index{assumptions!role of, in goal directed proof} 1416tactics, 1417with the tools currently provided in \HOL, presents at 1418least two difficulties. The first is that assumption sets can grow to an 1419unwieldy size, the number and/or length of terms making them difficult to 1420read. In addition, forward-search tactics such as resolution often add at least 1421some assumptions that are never subsequently used, and these have to be 1422carried along with the useful assumptions; the straightforward 1423method provides no ready way of intercepting their arrival. 1424Likewise, there is no straightforward way of discarding 1425\index{discarding assumptions} 1426\index{assumptions!discarding of, in proofs} 1427assumptions after they have been used and are merely adding to the clutter. 1428Although perhaps against the straightforward spirit, this is a perfectly valid 1429strategy, and 1430requires no more than a way of denoting 1431the specific assumptions to be discarded. That, however, 1432raises the more general problem of denoting\index{assumptions!denoting of, in proofs}\index{denoting assumptions} assumptions in the first place. 1433Assumptions are also denoted 1434so that they can be 1435manipulated: given as parameters, combined to draw inferences, \etc\ The only 1436straightforward way to denote them in the existing system is to supply 1437their quoted text. Though adequate, this 1438method may result in bulky \ML{} expressions; and it may take some effort to present the text 1439correctly (with necessary type information, \etc). 1440 1441As always in \HOL, there are quite a few ways around the various difficulties. 1442One approach, of course, is the one intended in the original 1443design of\index{LCF@\LCF!Edinburgh} Edinburgh \LCF, 1444and advocates the rationale for providing a full programming language, \ML, 1445\index{ML@\ML!purpose of, in HOL system@purpose of, in \HOL{} system} 1446rather than a simple proof command set: that is for the user to 1447implement new tactics in \ML. For example, resolution tactics can be adapted 1448by the user to add new assumptions more selectively; and case analysis tactics 1449to make direct replacements without adding case assumptions. 1450This, again, is adequate, but can involve the user in extensive amounts of 1451programming, and in debugging exercises for which there is no 1452system support. 1453 1454Short of implementing new tactics, two other standard 1455approaches are reflected in the current system. Both were originally 1456developed for Cambridge \LCF\ \cite{lcp-rewrite,new-LCF-man}; both reflect 1457fresh views of the assumptions; and both rely on tacticals\index{tacticals!purpose of} that transform 1458tactics. The two approaches are 1459partly but not completely complementary. 1460 1461The first 1462approach, described in this section, implicitly regards the assumption 1463set, already represented as a list, as a stack, with a {\it pop\/} 1464operation, so that the assumption at the top of the stack can be (i) discarded 1465and (ii) denoted without explicit quotation. (The corresponding {\it push\/} 1466adds new assumptions at the head of the list.) 1467The stack can be generalized to an array to allow for access to 1468arbitrary assumptions. 1469 1470The other approach, described in Section~\ref{tacont}, 1471gives a way of intercepting and manipulating results without them necessarily 1472being added as assumptions in the first place. The two approaches can 1473be combined in \HOL{} interactions. 1474 1475 1476\subsection{Theorem continuations with popping} 1477\label{avra_manip1} 1478 1479The first proof style, that of popping assumptions 1480\index{popping, of assumptions} 1481from the assumption `stack', 1482\index{assumptions!as stack} 1483\index{stack, of assumptions} 1484is illustrated using its main tool: the tactical \ml{POP\_ASSUM}. 1485 1486\index{POP_ASSUM@\ml{POP\_ASSUM}|pin} 1487\begin{holboxed}\begin{verbatim} 1488 POP_ASSUM : (thm -> tactic) -> tactic 1489\end{verbatim}\end{holboxed} 1490 1491\noindent Given a function $f$\ml{:thm -> tactic}, the tactic 1492\ml{POP\_ASSUM}\ $f$ applies $f$ to the (assumed) first 1493assumption of a goal (\ie\ to the top element of the assumption stack) 1494and then applies the tactic created thereby to the original goal 1495minus its top assumption: 1496 1497\begin{hol}\begin{alltt} 1498 POP_ASSUM \(f\) ([\(t\sb{1}\);\(\ldots\);\(t\sb{n}\)],\(t\)) = \(f\) (ASSUME \(t\sb{1}\)) ([\(t\sb{2}\);\(\ldots\);\(t\sb{n}\)],\(t\)) 1499\end{alltt}\end{hol} 1500 1501\noindent \ML{} functions such as $f$, 1502with type \ml{thm -> tactic}, abbreviated to \ml{thm\_tactic}, 1503\index{thm_tactic@\ml{thm\_tactic}} 1504are called theorem continuations, 1505\index{theorem continuations} suggesting the fact that they 1506take theorems and then continue the proof.\footnote{There is a superficial analogy 1507with continuations in denotational semantics.} 1508The use of \ml{POP\_ASSUM}\ can be illustrated by applying it 1509to a particular tactic, namely \ml{DISCH\_TAC} (Section~\ref{avradisch}). 1510 1511\index{DISCH_TAC@\ml{DISCH\_TAC}} 1512\begin{holboxed}\begin{verbatim} 1513 DISCH_TAC : tactic 1514\end{verbatim}\end{holboxed} 1515 1516\noindent On a goal whose conclusion is an implication $u \imp v$, 1517\ml{DISCH\_TAC} reflects the natural strategy of attempting to prove 1518$v$ under the assumption $u$, the discharged antecedent. For example, 1519suppose it were required to prove that $(n = 0) \imp (n\times n = n)$: 1520 1521\setcounter{sessioncount}{1} 1522\begin{session}\begin{verbatim} 1523#g "(n = 0) ==> (n * n = n)";; 1524"(n = 0) ==> (n * n = n)" 1525 1526() : void 1527 1528#e DISCH_TAC;; 1529OK.. 1530"n * n = n" 1531 [ "n = 0" ] 1532\end{verbatim}\end{session} 1533 1534\noindent Application of \ml{DISCH\_TAC} to the goal produces one subgoal, 1535as shown, with the added assumption. To engage the assumption 1536as a simple substitution, the tactic \ml{SUBST1\_TAC} is useful 1537(see \REFERENCE\ for details). 1538 1539 1540\index{SUBST1_TAC@\ml{SUBST1\_TAC}|pin} 1541\begin{holboxed}\begin{verbatim} 1542 SUBST1_TAC : thm_tactic 1543\end{verbatim}\end{holboxed} 1544 1545\noindent \ml{SUBST1\_TAC} expects a theorem with an equational conclusion, and 1546substitutes accordingly, into the conclusion of the goal. At this 1547point in the session, the tactical 1548\ml{POP\_ASSUM} is applied to 1549\ml{SUBST1\_TAC} to form a new tactic. 1550The new tactic is applied to the current subgoal. 1551 1552\begin{session}\begin{verbatim} 1553#top_goal();; 1554(["n = 0"], "n * n = n") : goal 1555 1556#e(POP_ASSUM SUBST1_TAC);; 1557OK.. 1558"0 * 0 = 0" 1559\end{verbatim}\end{session} 1560 1561\noindent The result, as shown, is that the assumption is used as a 1562substitution rule and then discarded. 1563\index{discarding assumptions} 1564\index{assumptions!discarding of, in proofs} 1565The one subgoal therefore has no 1566assumptions on its stack. The two tactics used thus far could be combined 1567into one using the tactical \ml{THEN}:\index{THEN@\ml{THEN}} 1568 1569\setcounter{sessioncount}{1} 1570\begin{session}\begin{verbatim} 1571#g "(n = 0) ==> (n * n = n)";; 1572"(n = 0) ==> (n * n = 0)" 1573 1574() : void 1575 1576#e(DISCH_TAC THEN POP_ASSUM SUBST1_TAC);; 1577OK.. 1578"0 * 0 = 0" 1579\end{verbatim}\end{session} 1580 1581\noindent The goal can now be solved by rewriting with a fact of arithmetic: 1582 1583\begin{session}\begin{verbatim} 1584#e(REWRITE_TAC[MULT_CLAUSES]);; 1585Theorem MULT_CLAUSES autoloaded from theory `arithmetic`. 1586MULT_CLAUSES = 1587|- !m n. 1588 (0 * m = 0) /\ 1589 (m * 0 = 0) /\ 1590 (1 * m = m) /\ 1591 (m * 1 = m) /\ 1592 ((SUC m) * n = (m * n) + n) /\ 1593 (m * (SUC n) = m + (m * n)) 1594 1595OK.. 1596goal proved 1597|- 0 * 0 = 0 1598|- (n = 0) ==> (n * n = n) 1599\end{verbatim}\end{session} 1600 1601\noindent A single tactic can, of course, be written to solve the goal: 1602 1603\setcounter{sessioncount}{1} 1604\begin{session}\begin{verbatim} 1605#g "(n = 0) ==> (n * n = n)";; 1606"(n = 0) ==> (n * n = n)" 1607 1608() : void 1609 1610#e(DISCH_TAC THEN POP_ASSUM SUBST1_TAC THEN REWRITE_TAC[MULT_CLAUSES]);; 1611Theorem MULT_CLAUSES autoloaded from theory `arithmetic`. 1612MULT_CLAUSES = 1613|- !m n. 1614 (0 * m = 0) /\ 1615 (m * 0 = 0) /\ 1616 (1 * m = m) /\ 1617 (m * 1 = m) /\ 1618 ((SUC m) * n = (m * n) + n) /\ 1619 (m * (SUC n) = m + (m * n)) 1620 1621OK.. 1622goal proved 1623|- (n = 0) ==> (n * n = n) 1624\end{verbatim}\end{session} 1625 1626This example illustrates how the tactical \ml{POP\_ASSUM} provides 1627access\index{assumptions!denoting of, in proofs} 1628\index{denoting assumptions} 1629to the top of the assumption `stack' (a capability that 1630is useful, obviously, only when the 1631most recently pushed assumption is the very one required). 1632To accomplish this access in the straightforward way would 1633require some more awkward 1634\index{assumptions!explicit} construct, with explicit assumptions: 1635 1636\setcounter{sessioncount}{1} 1637\begin{session}\begin{verbatim} 1638#g "(n = 0) ==> (n * n = n)";; 1639"(n = 0) ==> (n * n = n)" 1640 1641() : void 1642 1643#e(DISCH_TAC);; 1644OK.. 1645"n * n = n" 1646 [ "n = 0" ] 1647 1648() : void 1649 1650#e(SUBST1_TAC(ASSUME "n = 0"));; 1651OK.. 1652"0 * 0 = 0" 1653 [ "n = 0" ] 1654\end{verbatim}\end{session} 1655 1656In contrast to the above, the popping example also illustrates the 1657convenient disappearance of an assumption no longer required, by removing it 1658from the stack at the moment when it is accessed and used. This is valid 1659because any theorem that achieves the subgoal 1660will still achieve the original goal. Discarding\index{discarding assumptions}\index{assumptions!discarding of, in proofs} assumptions 1661is a separate issue from accessing them; 1662there could, if one liked, be another 1663tactical that produced a similar tactic on a theorem continuation 1664to \ml{POP\_ASSUM} but which did not pop the 1665stack. 1666 1667Finally, \ml{POP\_ASSUM} $f$ induces case splits where $f$ does. To prove 1668$(n=0 \disj n=1) \imp (n\times n = n)$, the function \ml{DISJ\_CASES\_TAC} 1669can be used. The tactic 1670 1671\ \ \ml{DISJ\_CASES\_TAC\ |- $p$}{\small\verb% \/ %}\ml{$q$} 1672 1673\noindent splits a goal into two subgoals that have 1674$p$ and $q$, respectively, as new assumptions. 1675 1676 1677\setcounter{sessioncount}{1} 1678\begin{session}\begin{verbatim} 1679#g "((n = 0) \/ (n = 1)) ==> (n * n = n)";; 1680"(n = 0) \/ (n = 1) ==> (n * n = n)" 1681 1682() : void 1683 1684#e DISCH_TAC;; 1685OK.. 1686"n * n = n" 1687 [ "(n = 0) \/ (n = 1)" ] 1688 1689() : void 1690 1691#backup();; 1692"(n = 0) \/ (n = 1) ==> (n * n = n)" 1693\end{verbatim}\end{session} 1694\vfill 1695\newpage 1696\begin{session}\begin{verbatim} 1697#e(DISCH_TAC THEN POP_ASSUM DISJ_CASES_TAC);; 1698OK.. 16992 subgoals 1700"n * n = n" 1701 [ "n = 1" ] 1702 1703"n * n = n" 1704 [ "n = 0" ] 1705 1706() : void 1707 1708#backup();; 1709"(n = 0) \/ (n = 1) ==> (n * n = n)" 1710 1711() : void 1712 1713#e(DISCH_TAC THEN POP_ASSUM DISJ_CASES_TAC THEN POP_ASSUM SUBST1_TAC);; 1714OK.. 17152 subgoals 1716"1 * 1 = 1" 1717 1718"0 * 0 = 0" 1719\end{verbatim}\end{session} 1720 1721As noted earlier, \ml{POP\_ASSUM} is useful when an assumption 1722is required that is still at the top of the stack, 1723as in the examples. However, it is often 1724necessary to access assumptions made at arbitrary previous times, in order to 1725give them as parameters, combine them, \etc\ The stack approach can be 1726extended to such cases by re-conceiving the stack as an array\index{assumptions!as array}\index{array, of assumptions}, and by 1727use of the tactical \ml{ASSUM\_LIST}:\index{ASSUM_LIST@\ml{ASSUM\_LIST}|(} 1728 1729\begin{hol}\begin{verbatim} 1730 ASSUM_LIST : (thm list -> tactic ) -> tactic 1731\end{verbatim}\end{hol} 1732 1733\noindent where 1734 1735\begin{hol}\begin{alltt} 1736 ASSUM_LIST \m{f} ([\m{t\sb{1}};...;\m{t\sb{n}}],\m{t}) = \m{f}([ASSUME \m{t\sb{1}};...;ASSUME \m{t\sb{n}}]) 1737\end{alltt}\end{hol} 1738 1739\noindent That is, given a function $f$, \ml{ASSUM\_LIST}$\ f$ forms a new tactic 1740by applying $f$ to the list of (assumed) assumptions of a goal, then applies 1741the resulting tactic to the goal. For example, a tactic of the form 1742{\small\verb%ASSUM_LIST (\thl.%}$\ f\ $\ml{(el\ $i$\ thl))} applies the 1743function $f$ to the $i$th assumption of a goal to produce a new tactic, then 1744applies the new tactic to the goal. 1745Again, \ml{ASSUM\_LIST REWRITE\_TAC} is a tactic that engages all of the 1746current assumptions as rewrite rules. 1747In this way, the array approach 1748enables arbitrary assumptions to be accessed; and in particular, 1749specific assumptions to be accessed by location using the function \ml{el}. 1750 1751To illustrate the use of \ml{ASSUM\_LIST}, suppose it were required to prove 1752something different: \index{ASSUM_LIST@\ml{ASSUM\_LIST}|)} 1753that $(\forall m.\ m + n = m) \imp (n \times n = n)$. Suppose 1754also that the arithmetic fact \ml{ADD\_INV\_{0}} is already known: namely, that 1755$\forall m\ n.\ (m + n = m) \imp (n = 0)$. After discharging the assumption, 1756the conclusion of the theorem \ml{ADD\_INV\_{0}} is imported as an 1757assumption, occupying first place in the array. 1758 1759\setcounter{sessioncount}{1} 1760\begin{session}\begin{verbatim} 1761#g "(!m. m + n = m) ==> (n * n = n)";; 1762"(!m. m + n = m) ==> (n * n = n)" 1763 1764() : void 1765 1766#e(DISCH_TAC);; 1767OK.. 1768"n * n = n" 1769 [ "!m. m + n = m" ] 1770 1771() : void 1772 1773#e(ASSUME_TAC ADD_INV_0);; 1774Theorem ADD_INV_0 autoloaded from theory `arithmetic`. 1775ADD_INV_0 = |- !m n. (m + n = m) ==> (n = 0) 1776 1777OK.. 1778"n * n = n" 1779 [ "!m. m + n = m" ] 1780 [ "!m n. (m + n = m) ==> (n = 0)" ] 1781\end{verbatim}\end{session} 1782 1783\noindent The problem is now to combine the two assumptions to produce the 1784obvious conclusion. That requires denoting 1785\index{denoting assumptions} 1786\index{assumptions!denoting of, in proofs} them, for which \ml{ASSUM\_LIST} 1787provides the means. Finally, 1788\ml{ASSUME\_TAC} places the conclusion of the new result in the assumptions. 1789(The \ML{} function \ml{el: int -> * list -> *} is used here to select a 1790numbered element of a list.) 1791 1792\begin{session}\begin{verbatim} 1793#e(ASSUM_LIST(\thl. ASSUME_TAC 1794 (MP (SPECL ["m:num";"n:num"] (el 1 thl)) 1795 (SPEC "m:num"(el 2 thl)))));; 1796##OK.. 1797"n * n = n" 1798 [ "!m. m + n = m" ] 1799 [ "!m n. (m + n = m) ==> (n = 0)" ] 1800 [ "n = 0" ] 1801\end{verbatim}\end{session} 1802 1803\noindent The goal can now be solved as in the previous example. 1804 1805To access the 1806two particular assumptions in the straightforward way would again require quoting 1807their text. To access all of them (to pass to \ml{REWRITE\_TAC}, for 1808instance) would require quoting all of them. 1809 1810\ml{ASSUM\_LIST} addresses the issue of accessing assumptions, 1811but not the issue of discarding them. A related function generalizes 1812\ml{POP\_ASSUM} to discard them as well: 1813 1814\begin{hol}\begin{verbatim} 1815 POP_ASSUM_LIST : (thm list -> tactic ) -> tactic 1816\end{verbatim}\end{hol} 1817 1818\noindent \ml{POP\_ASSUM\_LIST} 1819\index{POP_ASSUM_LIST@\ml{POP\_ASSUM\_LIST}} 1820resembles \ml{ASSUM\_LIST} except in removing 1821all of the old assumptions of the subgoal, the way that \ml{POP\_ASSUM} 1822removes the most recent. (Thus \ml{POP\_ASSUM} is no more than a special case 1823of \ml{POP\_ASSUM\_LIST} that selects the first element of those supplied 1824and re-assumes the others.) 1825 1826\begin{hol}\begin{alltt} 1827 POP_ASSUM_LIST \(f\) ([\(t\sb{1}\);\(\ \ldots\ \);\(t\sb{n}\)],\(t\)) = \(f\) [ASSUME \(t\sb{1}\);\(\ \ldots\ \);ASSUME \(t\sb{n}\)] ([],t) 1828\end{alltt}\end{hol} 1829 1830\noindent This is used when the existing assumptions have served 1831their purpose and can be discarded, as in the current example: 1832 1833\begin{session}\begin{verbatim} 1834#backup();; 1835"n * n = n" 1836 [ "!m. m + n = m" ] 1837 [ "!m n. (m + n = m) ==> (n = 0)" ] 1838 1839() : void 1840 1841#e(POP_ASSUM_LIST(\thl. ASSUME_TAC 1842 (MP (SPECL ["m:num";"n:num"] (el 1 thl)) 1843 (SPEC "m:num"(el 2 thl)))));; 1844##OK.. 1845"n * n = n" 1846 [ "n = 0" ] 1847\end{verbatim}\end{session} 1848 1849\noindent This leaves only the one assumption vital to solving the goal, 1850as before. In some contexts, the new result is required as an assumption, 1851but here it can be used immediately: 1852 1853\begin{session}\begin{verbatim} 1854#backup();; 1855"n * n = n" 1856 [ "!m. m + n = m" ] 1857 [ "!m n. (m + n = m) ==> (n = 0)" ] 1858 1859() : void 1860 1861#e(POP_ASSUM_LIST(\thl. SUBST1_TAC 1862 (MP (SPECL ["m:num";"n:num"] (el 1 thl)) 1863 (SPEC "m:num"(el 2 thl)))));; 1864##OK.. 1865"0 * 0 = 0" 1866\end{verbatim}\end{session} 1867 1868\noindent \ml{POP\_ASSUM\_LIST} can, of course, 1869take any function of appropriate 1870type, but is in fact often used in conjunction with the element-selecting 1871functions. Function composition occasionally allows a more 1872compact expression to be written. 1873 1874The array view (of which the stack view is a special case) 1875gives a way in which unnecessary assumptions can 1876be dropped, and assumptions can be accessed, individually if necessary, 1877using tacticals. 1878Although this approach can be effective, as illustrated, it does 1879tend to rely on the ordering of the representation of the assumption 1880\index{assumptions!importance of ordering of} set. 1881(That is, \ml{POP\_ASSUM} necessarily does, while the other two provide the 1882temptation!) A minor drawback of this reliance is that tactics are then 1883sensitive to changes that alter the order or composition of the assumptions; 1884for example, changes in the implementation of \HOL, modifications of 1885existing tactics, and so on. 1886However, that sensitivity is not so serious in any one incarnation of \HOL; 1887there is a logical viewpoint that regards the assumptions (sequents) as 1888ordered anyway. 1889A more serious problem is that order-sensitive tactics are meaningful 1890only during interactive sessions; to reconstruct the assumptions from 1891the \ML{} text and the original goal alone is generally difficult, 1892and more so when assumptions are denoted by location. 1893This means that (i) the resulting tactics cannot easily be generalized 1894for use in other contexts, and (ii) the \ML{} text does not supply 1895useful documentation 1896\index{tactics!as documentation of proofs} of the solution of the goal. 1897Also, as shown in the last example, it slightly unsatisfactory 1898to push and subsequently pop assumptions, especially in immediate succession, 1899where this could be avoided. 1900 1901Two other tacticals that can be used to manipulate the assumption list are 1902{\small\verb%FIRST_ASSUM%} and {\small\verb%EVERY_ASSUM%}. 1903These are characterized by: 1904 1905\index{FIRST_ASSUM@\ml{FIRST\_ASSUM}} 1906\index{EVERY_ASSUM@\ml{EVERY\_ASSUM}} 1907\begin{hol}\begin{alltt} 1908 FIRST_ASSUM \(f\) ([\(t\sb{1}\); \(\ldots\) ;\(t\sb{n}\)], \(t\)) = 1909 (\(f\)(ASSUME \(t\sb{1}\)) ORELSE \(\ldots\) ORELSE \(f\)(ASSUME \(t\sb{n}\))) ([\(t\sb{1}\); \(\ldots\) ;\(t\sb{n}\)], \(t\)) 1910 1911 EVERY_ASSUM \(f\) ([\(t\sb{1}\); \(\ldots\) ;\(t\sb{n}\)], \(t\)) = 1912 (\(f\)(ASSUME \(t\sb{1}\)) THEN \(\ldots\) THEN \(f\)(ASSUME \(t\sb{n}\))) ([\(t\sb{1}\); \(\ldots\) ;\(t\sb{n}\)], \(t\)) 1913\end{alltt}\end{hol} 1914 1915 1916\subsection{Theorem continuations without popping} 1917\label{tacont} 1918 1919The idea of the second approach is suggested by the way the array-style 1920tacticals\index{tacticals!purpose of} supply a list of theorems (the assumed assumptions) 1921to a function. These tacticals use the function to 1922infer new 1923results from the list of theorems, and then to do something with the 1924results. In some cases, 1925\eg\ the last example, the assumptions need never have been made in the 1926first place, which suggests a different use of tacticals. 1927The original example for \ml{POP\_ASSUM} 1928illustrates this: namely, to show that $(n = 0) \imp (n\times n = n)$. Here, 1929instead of discharging the antecedent by applying 1930\ml{DISCH\_TAC} to the goal, which adds the antecedent as an assumption 1931and returns the consequent as the conclusion, 1932and {\it then\/} supplying the (assumed) added assumption to the 1933theorem continuation \ml{SUBST1\_TAC} and 1934discarding it at the same time, 1935a tactical called \ml{DISCH\_THEN} is applied to \ml{SUBST1\_TAC} directly. 1936\ml{DISCH\_THEN} transforms \ml{SUBST1\_TAC} into 1937a new tactic: one that applies \ml{SUBST1\_TAC} directly to the (assumed) 1938antecedent, and the resulting tactic to a subgoal with no new 1939assumptions and the consequent as its conclusion: 1940\vfill 1941\newpage 1942 1943\setcounter{sessioncount}{1} 1944\begin{session}\begin{verbatim} 1945#DISCH_THEN;; 1946- : (thm_tactic -> tactic) 1947 1948#DISCH_THEN SUBST1_TAC;; 1949- : tactic 1950 1951#g "(n = 0) ==> (n * n = n)";; 1952"(n = 0) ==> (n * n = n)" 1953 1954() : void 1955 1956#e(DISCH_THEN SUBST1_TAC);; 1957OK.. 1958"0 * 0 = 0" 1959\end{verbatim}\end{session} 1960 1961\noindent This gives the same result as the stack method, but more 1962directly, with a more compact \ML{} expression, 1963and with the attractive feature that the term 1964$n=0$ is never an assumption, even for an interval of one step. 1965This technique is often used at the moment when results are available; 1966as above, where the result produced by discharging the antecedent can be 1967immediately passed to substitution. If the result were only needed 1968later, it {\it would\/} have to be held as an assumption. However, results 1969can be manipulated when they are available, and their results 1970either held as assumptions or used immediately. 1971For example, to prove $(0=n) \imp (n \times n = n)$, 1972the result $n=0$ could be reversed 1973immediately: 1974 1975\setcounter{sessioncount}{1} 1976\begin{session}\begin{verbatim} 1977#g "(0 = n) ==> (n * n = n)";; 1978"(0 = n) ==> (n * n = n)" 1979 1980() : void 1981 1982#e(DISCH_THEN(SUBST1_TAC o SYM));; 1983OK.. 1984"0 * 0 = 0" 1985\end{verbatim}\end{session} 1986 1987The justification of \ml{DISCH\_THEN SUBST1\_TAC} is easily constructed 1988from the justification of \ml{DISCH\_TAC} composed with the justification of 1989\ml{SUBST1\_TAC}. \index{assumptions!internal|(} 1990The term $n=0$ is assumed, to yield the 1991theorem that is passed to the theorem continuation \ml{SUBST1\_TAC}, 1992and it is accordingly discharged during the construction of the 1993actual proof; but the assumption happens 1994only internally 1995\index{assumptions!internal|)} to the tactic \ml{DISCH\_THEN SUBST1\_TAC}, and not 1996as a step in the tactical proof. In other words, the subgoal tree here 1997has one node fewer than before, when an explicit step (\ml{DISCH\_TAC}) 1998reflected the assumption. 1999 2000On the goal with the disjunctive antecedent, this method again 2001provides a compact tactic: 2002 2003\setcounter{sessioncount}{1} 2004\begin{session}\begin{verbatim} 2005#g "((n = 0) \/ (n = 1)) ==> (n * n = n)";; 2006"(n = 0) \/ (n = 1) ==> (n * n = n)" 2007 2008() : void 2009 2010#e(DISCH_THEN(DISJ_CASES_THEN SUBST1_TAC));; 2011OK.. 20122 subgoals 2013"1 * 1 = 1" 2014 2015"0 * 0 = 0" 2016\end{verbatim}\end{session} 2017 2018\noindent This avoids the repeated popping and pushing of the stack 2019solution, and likewise, gives a shorter \ML{} expression. Both give 2020a shorter expression than the direct method, which is: 2021 2022\begin{hol}\begin{verbatim} 2023 DISCH_TAC 2024 THEN DISJ_CASES_TAC(ASSUME "(n = 0) \/ (n = 1)") 2025 THENL[SUBST1_TAC(ASSUME "n = 0"); 2026 SUBST1_TAC(ASSUME "n = 1")] 2027\end{verbatim}\end{hol} 2028 2029To summarize, there are so far at least five ways to solve a goal 2030(and these are often combined in one interaction): 2031directly, using the stack view of the assumptions, 2032using the array view with or without discarding assumptions, and using a 2033tactical to intercept an assumption step. All of the following work 2034\index{assumptions!compared methods of handling} 2035on the goal $(n=0) \imp (n \times n = n)$: 2036 2037\begin{hol}\index{ASSUM_LIST@\ml{ASSUM\_LIST}} 2038\begin{verbatim} 2039 DISCH_TAC 2040 THEN SUBST1_TAC(ASSUME "n = 0") 2041 THEN REWRITE_TAC[MULT_CLAUSES] 2042 2043 DISCH_TAC 2044 THEN POP_ASSUM SUBST1_TAC 2045 THEN REWRITE_TAC[MULT_CLAUSES] 2046 2047 DISCH_TAC 2048 THEN ASSUM_LIST (SUBST1_TAC o el 1) 2049 THEN REWRITE_TAC[MULT_CLAUSES] 2050 2051 DISCH_TAC 2052 THEN POP_ASSUM_LIST (SUBST1_TAC o el 1) 2053 THEN REWRITE_TAC[MULT_CLAUSES] 2054 2055 DISCH_THEN SUBST1_TAC 2056 THEN REWRITE_TAC[MULT_CLAUSES] 2057\end{verbatim}\end{hol} 2058 2059\noindent Furthermore, all five induce the 2060same sequence of inferences leading to 2061the desired theorem; internally, no inference steps are saved by the 2062economies in the \ML{} text or the subgoal tree. In this sense, 2063the choice is entirely one of style and taste; 2064of how to organize the decomposition into subgoals. 2065The first expression illustrates the verbosity of denoting 2066assumptions by text (the goal with the 2067disjunctive antecedent gave a clearer 2068example); but also 2069the intelligibility of the resulting expression, which, of course, is all 2070that is saved of the interaction, aside from the final theorem. 2071The last expression 2072illustrates both the elegance and the inscrutibility of 2073using functions to manipulate intermediate results directly, rather than 2074as assumptions. 2075The middle three expressions 2076show how results can be used as assumptions (discarded when 2077redundant, if desired); and how 2078assumptions can be denoted without 2079recourse to their text. 2080It is a strength of the \LCF\ approach 2081\index{LCF@\LCF} to 2082theorem proving that many different proof styles are supported, 2083(all in a secure way) and indeed, can be studied in their own 2084right. 2085 2086\HOL{} provides several other theorem continuation functions analogous to 2087\ml{DISCH\_THEN} and \ml{DISJ\_CASES\_THEN}. 2088(Their names always end with 2089`\ml{\_THEN}', `\ml{\_THENL} or `\ml{\_THEN2}'.) 2090Some of these do convenient inferences for the user. 2091For example: 2092 2093\index{CHOOSE_THEN@\ml{CHOOSE\_THEN}|pin} 2094\begin{holboxed}\begin{verbatim} 2095 CHOOSE_THEN : thm_tactical 2096\end{verbatim}\end{holboxed} 2097 2098\noindent Where \ml{thm\_tactical} abbreviates 2099{\small\verb%thm_tactic -> tactic%}. 2100\ml{CHOOSE\_THEN\ $f$\ (|-\ ?$x$.$t[x]$)} 2101is a tactic that, given a goal, generates the subgoal 2102obtained 2103by applying $f$ to \ml{($t[x]$|-$t[x]$)}. The intuition is that if 2104\ml{|-\ ?$x$.$t[x]$} holds then \ml{|-\ $t[x]$} 2105holds for some value of $x$ (as long as the 2106variable $x$ is not free elsewhere in the theorem or current goal). 2107%(The choice of the witness is `understood' by the justification function.) 2108This gives an easy way of using existentially quantified theorems, 2109something that is otherwise awkward. 2110 2111The new method has other applications as well, including as an 2112implementation technique. 2113For example, 2114\index{tactics!indirect implementation of} 2115taking \ml{DISJ\_CASES\_THEN} as basic, \ml{DISJ\_CASES\_TAC} 2116can be defined by: 2117 2118\begin{hol}\begin{verbatim} 2119 let DISJ_CASES_TAC = DISJ_CASES_THEN ASSUME_TAC 2120\end{verbatim}\end{hol} 2121 2122\noindent Similarly, the method is useful for modifying existing tactics 2123(\eg\ resolution tactics) without 2124having to re-program them in \ML. This avoids the danger of 2125introducing tactics 2126whose justifications may fail, 2127\index{failure, of tactics} a particularly difficult problem to 2128track down; it is also much easier than starting from scratch. 2129 2130The main theorem continuation functions in the system are: 2131 2132\begin{hol}\begin{verbatim} 2133 ANTE_RES_THEN 2134 CHOOSE_THEN X_CHOOSE_THEN 2135 CONJUNCTS_THEN CONJUNCTS_THEN2 2136 DISJ_CASES_THEN DISJ_CASES_THEN2 DISJ_CASES_THENL 2137 DISCH_THEN 2138 IMP_RES_THEN 2139 RES_THEN 2140 STRIP_THM_THEN 2141 STRIP_GOAL_THEN 2142\end{verbatim}\end{hol} 2143 2144\noindent See \REFERENCE\ for full details. 2145\index{tactics!for manipulating assumptions|)} 2146 2147 2148 2149 2150 2151%%% Local Variables: 2152%%% mode: latex 2153%%% TeX-master: "description" 2154%%% End: 2155