1\chapter{The \HOL{} Logic}\label{HOLlogic} 2 3The \HOL{} system supports \emph{higher order logic}. 4This is a version of predicate calculus with three main extensions: 5 6\begin{itemize} 7\item Variables can range over functions and predicates (hence `higher order'). 8\item The logic is \emph{typed}. 9\item There is no separate syntactic category of \emph{formulae} (terms of type \ml{bool} fulfill that role). 10\end{itemize} 11 12In this chapter, we will give a brief overview of the notation used to write expressions of the \HOL{} logic in \ML{}, and also discuss some fundamental \HOL{} proof techniques. 13It is assumed the reader is familiar with predicate logic. 14The syntax and semantics of the particular logical system supported by \HOL{} is described in detail in \DESCRIPTION. 15Readers who wish to see \HOL{} in action, without the introduction to the finer details of \HOL's fundamentals, might like to skip ahead to Chapter~\ref{chap:euclid}. 16 17 18The table below summarizes a useful subset of the (ASCII) notation used in \HOL. 19 20\begin{center} 21\begin{tabular}{|l|l|l|l|} \hline 22\multicolumn{4}{|c|}{ } \\ 23\multicolumn{4}{|c|}{\bf Terms of the HOL Logic} \\ 24\multicolumn{4}{|c|}{ } \\ 25{\it Kind of term} & {\it \HOL{} notation} & 26{\it Standard notation} & 27{\it Description} \\ \hline 28 & & & \\ 29Truth & {\small\verb|T|} & $\top$ & {\it true}\\ \hline 30Falsity & {\small\verb|F|} & $\bot$ & {\it false}\\ \hline 31Negation & {\small\verb|~|}$t$ & $\neg t$ & {\it not}$\ t$\\ \hline 32Disjunction & $t_1${\small\verb|\/|}$t_2$ & $t_1\vee t_2$ & 33$t_1\ ${\it or}$\ t_2$ \\ \hline 34Conjunction & $t_1${\small\verb|/\|}$t_2$ & $t_1\wedge t_2$ & 35$t_1\ ${\it and}$\ t_2$ \\ \hline 36Implication & $t_1${\small\verb|==>|}$t_2$ & $t_1\imp t_2$ & 37$t_1\ ${\it implies}$\ t_2$ \\ \hline 38Equality & $t_1${\small\verb|=|}$t_2$ & $t_1 = t_2$ & 39$t_1\ ${\it equals}$\ t_2$ \\ \hline 40$\forall$-quantification & {\small\verb|!|}$x${\small\verb|.|}$t$ & 41$\uquant{x}t$ & {\it for\ all\ }$x: t$ \\ \hline 42$\exists$-quantification & {\small\verb|?|}$x${\small\verb|.|}$t$ & 43$\equant{x}\ t$ & {\it for\ some\ }$x: t$ \\ \hline 44$\hilbert$-term & {\small\verb|@|}$x${\small\verb|.|}$t$ & 45$\hquant{x}t$ & {\it an}$\ x\ ${\it such\ that:}$\ t$ \\ \hline 46Conditional & {\small\verb|if|} $t$ {\small\verb|then|} $t_1$ 47 {\small\verb|else|} $t_2$ & 48$(t\rightarrow t_1, t_2)$ & {\it if\ }$t${\it \ then\ }$t_1${\it\ else\ }$t_2$ 49 \\ \hline 50\end{tabular} 51\end{center}\label{logic-table} 52 53Terms of the \HOL{} logic are represented in \ML{} by an \emph{abstract type} called {\small\verb|term|}. 54They are normally input between double back-quote marks. 55For example, the expression \holtxt{``x /\bs{} y ==> z``} evaluates in \ML{} to a term representing $\holtxt{x} \land \holtxt{y} \Rightarrow \holtxt{z}$. 56Terms can be manipulated by various built-in \ML{} functions. 57For example, the \ML{} function \ml{dest\_imp} with \ML{} type \ml{term -> term * term} splits an implication into a pair of terms consisting of its antecedent and consequent, and the \ML\ function \ml{dest\_conj} of type \ml{term -> term * term} splits a conjunction into its two conjuncts.% 58\footnote{All of the examples below assume that the user is running \texttt{hol}, the executable for which is in the \texttt{bin/} directory. 59Depending on the system configuration, it is also possible that the ASCII notation used in the session examples that follow would be replaced by prettier Unicode notation: \holtxt{/\bs} replaced by $\land$ for example.} 60 61\setcounter{sessioncount}{0} 62\begin{session} 63\begin{verbatim} 64- ``x /\ y ==> z``; 65> val it = ``x /\ y ==> z`` : term 66 67- dest_imp it; 68> val it = (``x /\ y``, ``z``) : term * term 69 70- dest_conj(#1 it); 71> val it = (``x``, ``y``) : term * term 72\end{verbatim} 73\end{session} 74 75Terms of the \HOL{} logic are quite similar to \ML{} expressions, and this can at first be confusing. 76Indeed, terms of the logic have types similar to those of \ML{} expressions. 77For example, \holtxt{``(1,2)``} is an \ML{} expression with \ML{} type \ml{term}. 78The \HOL{} type of this term is \holtxt{num \# num}. 79By contrast, the \ML{} expression \ml{(``1``, ``2``)} has (\ML{}) type \ml{term * term}. 80 81\paragraph{Syntax of \HOL\ types} 82 83The types of \HOL{} terms form an \ML{} type called \ml{hol_type}. 84Expressions having the form \ml{``: $\cdots$ ``} evaluate to logical types. 85The built-in function \ml{type_of} has \ML{} type \ml{term->hol_type} and returns the logical type of a term. 86 87\begin{session} 88\begin{verbatim} 89- ``(1,2)``; 90> val it = ``(1,2)`` : term 91 92- type_of it; 93> val it = ``:num # num`` : hol_type 94 95- (``1``, ``2``); 96> val it = (``1``, ``2``) : term * term 97 98- type_of(#1 it); 99> val it = ``:num`` : hol_type 100\end{verbatim} 101\end{session} 102 103To try to minimise confusion between the logical types of \HOL{} terms and the \ML{} types of \ML{} expressions, the former will be referred to as \emph{object language types} and the latter as \emph{meta-language types}. 104For example, \ml{``(1,T)``} is an \ML{} expression that has meta-language type \ml{term} and evaluates to a term with object language type \ml{``:num\#bool``}. 105% 106\begin{session} 107\begin{verbatim} 108- ``(1,T)``; 109> val it = ``(1,T)`` : term 110 111- type_of it; 112> val it = ``:num # bool`` : hol_type 113\end{verbatim} 114\end{session} 115% 116\paragraph{Term constructors} 117\HOL{} terms can be input, as above, by using explicit \emph{quotation}, or they can be constructed by calling \ML{} constructor functions. 118The function \ml{mk_var} constructs a variable from a string and a type. 119In the example below, three variables of type {\small\verb|bool|} are constructed. 120These are used later. 121 122\begin{session} 123\begin{verbatim} 124- val x = mk_var("x", ``:bool``) 125 and y = mk_var("y", ``:bool``) 126 and z = mk_var("z", ``:bool``); 127> val x = ``x`` : term 128 val y = ``y`` : term 129 val z = ``z`` : term 130\end{verbatim} 131\end{session} 132 133The constructors \ml{mk_conj} and \ml{mk_imp} construct conjunctions and implications respectively. 134A large collection of term constructors and destructors is available for the core theories in \HOL. 135 136\begin{session} 137\begin{verbatim} 138- val t = mk_imp(mk_conj(x,y),z); 139> val t = ``x /\ y ==> z`` : term 140\end{verbatim} 141\end{session} 142 143\paragraph{Type checking} 144 145There are actually only four different kinds of term in \HOL: variables, constants, function applications (\ml{``$t_1$ $t_2$``}), and lambda abstractions (\ml{``\bs$x$.$t$``}). 146More complex terms, such as those we have already seen above, are just compositions of terms from this simple set. 147In order to understand the behaviour of the quotation parser, it is necessary to understand how the type checker infers types for the four basic term categories. 148 149Both variables and constants have a name and a type; the difference is that constants cannot be bound by quantifiers, and their type is fixed when they are declared (see below). 150When a quotation is entered into \HOL{}, the type checking algorithm uses the types of constants to infer the types of variables in the same quotation. 151For example, in the following case, the \HOL{} type checker used the known type \holtxt{bool->bool} of boolean negation (\holtxt{\td}) to deduce that the variable \holtxt{x} must have type \holtxt{bool}. 152 153\begin{session} 154\begin{verbatim} 155- ``~x``; 156> val it = ``~x`` : term 157\end{verbatim} 158\end{session} 159 160In the next two cases, the type of \ml{x} and \ml{y} cannot be 161deduced. 162(The default `scope' of type information for type checking is a single quotation, so a type in one quotation cannot affect the type-checking of another. 163Thus \ml{x} is not constrained to have the type \ml{bool} in the second quotation.) 164 165\begin{session} 166\begin{verbatim} 167- ``x``; 168<<HOL message: inventing new type variable names: 'a.>> 169> val it = ``x`` : Term.term 170 171- type_of it; 172> val it = ``:'a`` : hol_type 173 174- ``(x,y)``; 175<<HOL message: inventing new type variable names: 'a, 'b.>> 176> val it = ``(x,y)`` : term 177 178- type_of it; 179> val it = ``:'a # 'b`` : hol_type 180\end{verbatim} 181\end{session} 182 183If there is not enough contextually-determined type information to resolve the types of all variables in a quotation, then the system will guess different type variables for all the unconstrained variables. 184 185\paragraph{Type constraints} 186 187Alternatively, it is possible to explicitly indicate the required types by using the notation \ml{``$\mathit{term}$:$\mathit{type}$``}, as illustrated below. 188 189\begin{session} 190\begin{verbatim} 191- ``x:num``; 192> val it = ``x`` : term 193 194- type_of it; 195> val it = ``:num`` : hol_type 196\end{verbatim} 197\end{session} 198 199\paragraph{Function application types} 200 201An application $(t_1\ t_2)$ is well-typed if $t_1$ is a function with type $\tau_1 \to \tau_2$ and $t_2$ has type $\tau_1$. 202Contrarily, an application $(t_1\ t_2)$ is badly typed if $t_1$ is not a function: 203 204\begin{session} 205\begin{verbatim} 206- ``1 2``; 207 208Type inference failure: unable to infer a type for the application of 209 210(1 :num) 211 212to 213 214(2 :num) 215 216unification failure message: unify failed 217! Uncaught exception: 218! HOL_ERR 219\end{verbatim} 220\end{session} 221 222\noindent or if it is a function, but $t_2$ is not in its domain: 223 224\begin{session} 225\begin{verbatim} 226- ``~1``; 227 228Type inference failure: unable to infer a type for the application of 229 230$~ :bool -> bool 231 232at line 1, character 3 233 234to 235 236(1 :num) 237 238unification failure message: unify failed 239! Uncaught exception: 240! HOL_ERR 241\end{verbatim} 242\end{session} 243 244The dollar symbol in front of \holtxt{\td} indicates that the boolean negation constant has a special syntactic status (in this case a non-standard precedence). 245Putting \holtxt{\$} in front of any symbol causes the parser to ignore any special syntactic status (like being an infix) it might have. 246The same effect can be achieved by enclosing the symbol in parentheses. 247This is analogous to the way in which \texttt{op} is used in \ML. 248 249\begin{session} 250\begin{verbatim} 251- ``$==> t1 t2``; 252> val it = ``t1 ==> t2`` : term 253 254- ``(/\) t1 t2``; 255> val it = ``t1 /\ t2`` : term 256\end{verbatim} 257\end{session} 258 259\paragraph{Function types} 260 261Functions have types of the form \ml{$\sigma_1$->$\sigma_2$}, where $\sigma_1$ and $\sigma_2$ are the types of the domain and range of the function, respectively. 262 263\begin{session} 264\begin{verbatim} 265- type_of ``(==>)``; 266> val it = ``:bool -> bool -> bool`` : hol_type 267 268- type_of ``$+``; 269> val it = ``:num -> num -> num`` : hol_type 270\end{verbatim} 271\end{session} 272 273\noindent Again, both \holtxt{+} and \holtxt{==>} are infixes, so their use in contexts where they are not being used as such requires syntax-escaping. 274The session below illustrates the use of these constants as infixes; it also illustrates object language versus meta-language types. 275 276\begin{session} 277\begin{verbatim} 278- ``(x + 1, t1 ==> t2)``; 279> val it = ``(x + 1,t1 ==> t2)`` : term 280 281- type_of it; 282> val it = ``:num # bool`` : hol_type 283 284- (``x=1``, ``t1==>t2``); 285> val it = (``x = 1``, ``t1 ==> t2``) : term * term 286 287- (type_of (#1 it), type_of (#2 it)); 288> val it = (``:bool``, ``:bool``) : hol_type * hol_type 289\end{verbatim} 290\end{session} 291 292Lambda-terms, or $\lambda$-terms, denote functions. 293The symbol `\holtxt{\bs}' is used as an ASCII approximation to $\lambda$. 294Thus `{\small\verb|\|}$x$\ml{.}$t$' should be read as `$\lquant{x}t$'. 295For example, {\small\verb|``\x. x+1``|} is a term that denotes the function $n\mapsto n{+}1$. 296 297\begin{session} 298\begin{verbatim} 299- ``\x. x + 1``; 300> val it = ``\x. x + 1`` : term 301 302- type_of it; 303> val it = ``:num -> num`` : hol_type 304\end{verbatim} 305\end{session} 306 307Other binding symbols in the logic are its two most important quantifiers: \ml{!} and \ml{?}, universal and existential quantifiers. 308For example, the logical statement that every number is either even or odd might be phrased as 309\begin{verbatim} 310 !n. (n MOD 2 = 1) \/ (n MOD 2 = 0) 311\end{verbatim} 312while a version of Euclid's result about the infinitude of primes is: 313\begin{verbatim} 314 !n. ?p. prime p /\ p > n 315\end{verbatim} 316% 317Binding symbols such as these can be used over multiple `parameters' thus: 318\begin{session} 319\begin{verbatim} 320- ``\x y. (x, y * x)``; 321> val it = ``\x y. (x,y * x)`` : term 322 323- type_of it; 324> val it = ``:num -> num -> num # num`` : hol_type 325 326- ``!x y. x <= x + y``; 327> val it = ``!x y. x <= x + y`` : term 328\end{verbatim} 329\end{session} 330 331 332\section{Basic Proof in \HOL{}} 333 334\newcommand\tacticline{\hline \hline} 335\newenvironment{proofenumerate}{\begin{enumerate}}{\end{enumerate}} 336% proofenumerate is distinguished from a normal enumeration so that 337% h e v e a can spot these special cases and treat them better. 338 339\setcounter{sessioncount}{0} 340 341This section discusses the nature of proof in \HOL{}. 342For a logician, one definition of a formal proof is that it is a sequence, each of whose elements is either an \emph{axiom} or follows from earlier members of the sequence by a \emph{rule of inference}. 343A theorem is the last element of a proof. 344 345Theorems are represented in \HOL{} by values of an abstract type \ml{thm}. 346The only way to create theorems is by generating such a proof. 347In \HOL, following \LCF, this consists in applying \ML{} functions representing \emph{rules of inference} to axioms or previously generated theorems. 348The sequence of such applications directly corresponds to a logician's proof. 349 350There are five axioms of the \HOL{} logic and eight primitive inference rules. 351The axioms are bound to ML names. 352For example, the Law of Excluded Middle is bound to the \ML{} name \ml{BOOL_CASES_AX}:\footnote{% 353Note how the term-printer has rendered the equalities in the theorem with the \holtxt{<=>} symbol rather than \holtxt{=}. 354The underlying constant is the same, but the printing is a clue for the user that this is equality on boolean values. 355The parser accepts both \holtxt{<=>} and \holtxt{=} with boolean arguments; attempting to use \holtxt{<=>} on values that are not of boolean type (numbers, say) will result in a parse error.% 356} 357 358\begin{session} 359\begin{verbatim} 360- BOOL_CASES_AX; 361> val it = |- !t. (t <=> T) \/ (t <=> F) : thm 362\end{verbatim} 363\end{session} 364 365 366Theorems are printed with a preceding turnstile {\small\verb+|-+} as illustrated above; the symbol `{\small\verb|!|}' is the universal quantifier `$\forall$'. 367Rules of inference are \ML{} functions that return values of type \ml{thm}. 368An example of a rule of inference is {\it specialization\/} (or $\forall$-elimination). 369In standard `natural deduction' notation this is: 370 371\[ \frac{\Gamma\turn \uquant{x}t}{\Gamma\turn t[t'/x]}\] 372 373\begin{itemize} 374\item $t[t'/x]$ denotes the result of substituting $t'$ for free occurrences of $x$ in $t$, with the restriction that no free variables in $t'$ become bound after substitution. 375\end{itemize} 376 377\noindent This rule is represented in \ML{} by a function \ml{SPEC},% 378\footnote{\ml{SPEC} is not a primitive rule of inference in the HOL logic, but is a derived rule. 379Derived rules are described in Section~\ref{forward}.} 380which takes as arguments a term \ml{``$a$``} and a theorem \holtxt{|-~!$x.\,t[x]$} and returns the theorem \holtxt{|-~$t[a]$}, the result of substituting $a$ for $x$ in $t[x]$. 381 382\begin{session} 383\begin{verbatim} 384- val Th1 = BOOL_CASES_AX; 385> val Th1 = |- !t. (t <=> T) \/ (t <=> F) : thm 386 387- val Th2 = SPEC ``1 = 2`` Th1; 388> val Th2 = |- ((1 = 2) <=> T) \/ ((1 = 2) <=> F) : thm 389\end{verbatim} 390\end{session} 391 392This session consists of a proof of two steps: using an axiom and applying the rule \ml{SPEC}; it interactively performs the following proof: 393\begin{samepage} 394\begin{proofenumerate} 395\item $ \turn \uquant{t}\;\; t\Leftrightarrow\top \;\disj\; t\Leftrightarrow\bot$ \hfill 396[Axiom \ml{BOOL\_CASES\_AX}] 397\item $ \turn (1{=}2)\Leftrightarrow\top\ \disj\ (1{=}2)\Leftrightarrow\bot$\hfill [Specializing line 1 to `$1{=}2$'] 398\end{proofenumerate} 399\end{samepage} 400 401If the argument to an \ML{} function representing a rule of inference is of the wrong kind, or violates a condition of the rule, then the application fails. 402For example, $\ml{SPEC}\ t\ th$ will fail if $th$ is not of the form $\ml{|-\ !}x\ml{.}\cdots$ or if it is of this form but the type of $t$ is not the same as the type of $x$, or if the free variable restriction is not met. 403When one of the standard \ml{HOL\_ERR} exceptions is raised, more information about the failure can often be gained by using the \ml{Raise} function.% 404\footnote{The \ml{Raise} function passes on all of the exceptions it sees; it does not affect the semantics of the computation at all. 405However, when passed a \ml{HOL\_ERR} exception, it prints out some useful information before passing the exception on to the next level.} 406 407\begin{session} 408\begin{verbatim} 409- SPEC ``1=2`` Th2; 410! Uncaught exception: 411! HOL_ERR 412 413- SPEC ``1 = 2`` Th2 handle e => Raise e; 414 415Exception raised at Thm.SPEC: 416 417! Uncaught exception: 418! HOL_ERR 419\end{verbatim} 420\end{session} 421However, as this session illustrates, the failure message does not always indicate the exact reason for failure. 422Detailed failure conditions for rules of inference are given in \REFERENCE. 423 424A proof in the \HOL{} system is constructed by repeatedly applying inference rules to axioms or to previously proved theorems. 425Since proofs may consist of millions of steps, it is necessary to provide tools to make proof construction easier for the user. 426The proof generating tools in the \HOL{} system are just those of \LCF, and are described later. 427 428The general form of a theorem is $t_1,\ldots,t_n\;\ml{|-}\;t$, where $t_1$, $\ldots$ , $t_n$ are boolean terms called the {\it assumptions} and $t$ is a boolean term called the {\it conclusion\/}. 429Such a theorem asserts that if its assumptions are true then so is its conclusion. 430Its truth conditions are thus the same as those for the 431single term $(t_1\,\ml{/\bs}\ldots\ml{/\bs}\,t_n)\,\ml{==>}\,t$. 432Theorems with no assumptions are printed out in the form \ml{|-}$\ t$. 433 434The five axioms and eight primitive inference rules of the \HOL{} logic are described in detail in the document \DESCRIPTION. 435Every value of type \ml{thm} in the \HOL{} system can be obtained by repeatedly applying primitive inference rules to axioms. 436When the \HOL{} system is built, the eight primitive rules of inference are defined and the five axioms are bound to their \ML{} names. 437All other predefined theorems are proved using rules of inference as the system is made.\footnote{This is a slight over-simplification.} 438This is one of the reasons why building \ml{hol} takes so long. 439 440In the rest of this section, the process of \emph{forward proof}, which has just been sketched, is described in more detail. 441In Section~\ref{tactics} \emph{goal directed proof} is described, including the important notions of \emph{tactics} and \emph{tacticals}, due to Robin Milner. 442 443\section{Forward proof} 444\label{forward} 445 446Three of the primitive inference rules of the \HOL{} logic are 447\ml{ASSUME} (assumption introduction), \ml{DISCH} (discharging or 448assumption elimination) and \ml{MP} (Modus Ponens). These rules will 449be used to illustrate forward proof and the writing of derived rules. 450 451The inference rule \ml{ASSUME} generates theorems of the form \ml{$t$ 452 |- $t$}. Note, however, that the \ML{} printer prints each 453assumption as a dot (but this default can be changed; see below). The 454function \ml{dest\_thm} decomposes a theorem into a pair consisting of 455list of assumptions and the conclusion. 456 457\begin{session} 458\begin{verbatim} 459- val Th3 = ASSUME ``t1==>t2``;; 460> val Th3 = [.] |- t1 ==> t2 : thm 461 462- dest_thm Th3; 463> val it = ([``t1 ==> t2``], ``t1 ==> t2``) : term list * term 464\end{verbatim} 465\end{session} 466 467A sort of dual to \ml{ASSUME} is the primitive inference rule 468\ml{DISCH} (discharging, assumption elimination) which infers from 469a theorem of the form $\cdots t_1\cdots\ml{\ |-\ }t_2$ the new theorem 470$\cdots\ \cdots\ \ml{|-}\ t_1\ml{==>}t_2$. \ml{DISCH} takes as arguments 471the term to be discharged (\ie\ $t_1$) and the theorem from whose 472assumptions it is to be discharged and returns the result of the discharging. 473The following session illustrates this: 474 475\begin{session} 476\begin{verbatim} 477- val Th4 = DISCH ``t1==>t2`` Th3; 478> val Th4 = |- (t1 ==> t2) ==> t1 ==> t2 : thm 479\end{verbatim} 480\end{session} 481Note that the term being discharged need not be in the assumptions; in 482this case they will be unchanged. 483 484\begin{session} 485\begin{verbatim} 486- DISCH ``1=2`` Th3; 487> val it = [.] |- (1 = 2) ==> t1 ==> t2 : thm 488 489- dest_thm it; 490> val it = ([``t1 ==> t2``], ``(1 = 2) ==> t1 ==> t2``) : term list * term 491\end{verbatim} 492\end{session} 493 494In \HOL\, the rule \ml{MP} of Modus Ponens is specified in conventional notation by: 495\[ 496\frac{\Gamma_1 \turn t_1 \imp t_2 \qquad\qquad \Gamma_2\turn t_1} 497{\Gamma_1 \cup \Gamma_2 \turn t_2} 498\] 499The \ML{} function \ml{MP} takes argument theorems of the form 500\ml{$\cdots\ $|-$\ t_1$\ ==>\ $t_2$} and \ml{$\cdots\ $|-$\ t_1$} and 501returns \ml{$\cdots\ $|-$\ t_2$}. The next session illustrates the use 502of \ml{MP} and also a common error, namely not supplying the \HOL\ 503logic type checker with enough information. 504 505\begin{session} 506\begin{verbatim} 507- val Th5 = ASSUME ``t1``; 508<<HOL message: inventing new type variable names: 'a.>> 509! Uncaught exception: 510! HOL_ERR 511- val Th5 = ASSUME ``t1`` handle e => Raise e; 512<<HOL message: inventing new type variable names: 'a.>> 513 514Exception raised at Thm.ASSUME: 515not a proposition 516! Uncaught exception: 517! HOL_ERR 518 519- val Th5 = ASSUME ``t1:bool``; 520> val Th5 = [.] |- t1 : thm 521 522- val Th6 = MP Th3 Th5; 523> val Th6 = [..] |- t2 : thm 524\end{verbatim} 525\end{session} 526 527The hypotheses of \ml{Th6} can be inspected with the \ML{} function 528\ml{hyp}, which returns the list of assumptions of a theorem (the 529conclusion is returned by \ml{concl}). 530 531\begin{session} 532\begin{verbatim} 533- hyp Th6; 534> val it = [``t1 ==> t2``, ``t1``] : term list 535\end{verbatim} 536\end{session} 537 538\HOL{} can be made to print out hypotheses of theorems explicitly by setting the global flag \ml{show\_assums} to true. 539 540\begin{session} 541\begin{verbatim} 542- show_assums := true; 543> val it = () : unit 544 545- Th5; 546> val it = [t1] |- t1 : thm 547 548- Th6; 549> val it = [t1 ==> t2, t1] |- t2 : thm 550\end{verbatim} 551\end{session} 552 553 554\noindent Discharging \ml{Th6} twice establishes the theorem 555\ml{|-\ t1 ==> (t1==>t2) ==> t2}. 556 557\begin{session} 558\begin{verbatim} 559- val Th7 = DISCH ``t1==>t2`` Th6; 560> val Th7 = [t1] |- (t1 ==> t2) ==> t2 : thm 561 562- val Th8 = DISCH ``t1:bool`` Th7; 563> val Th8 = |- t1 ==> (t1 ==> t2) ==> t2 : thm 564\end{verbatim} 565\end{session} 566 567The sequence of theorems: \ml{Th3}, \ml{Th5}, \ml{Th6}, \ml{Th7}, \ml{Th8} constitutes a proof in \HOL{} of the theorem \ml{|-\ t1 ==> (t1 ==> t2) ==> t2}. 568In standard logical notation this proof could be written: 569 570\begin{proofenumerate} 571\item $ t_1\imp t_2\turn t_1\imp t_2$ \hfill 572[Assumption introduction] 573\item $ t_1\turn t_1$ \hfill 574[Assumption introduction] 575\item $ t_1\imp t_2,\ t_1 \turn t_2 $ \hfill 576[Modus Ponens applied to lines 1 and 2] 577\item $ t_1 \turn (t_1\imp t_2)\imp t_2$ \hfill 578[Discharging the first assumption of line 3] 579\item $ \turn t_1 \imp (t_1 \imp t_2) \imp t_2$ \hfill 580[Discharging the only assumption of line 4] 581\end{proofenumerate} 582 583\subsection{Derived rules} 584 585 586A \emph{proof from hypothesis} $th_1, \ldots, th_n$ is a sequence each of whose elements is either an axiom, or one of the hypotheses $th_i$, or follows from earlier elements by a rule of inference. 587 588For example, a proof of $\Gamma,\ t'\turn t$ from the hypothesis $\Gamma\turn t$ is: 589 590\begin{proofenumerate} 591\item $ t'\turn t'$ \hfill [Assumption introduction] 592\item $ \Gamma\turn t$ \hfill [Hypothesis] 593\item $ \Gamma\turn t'\imp t$ \hfill [Discharge $t'$ from line 2] 594\item $ \Gamma,\ t'\turn t$ \hfill [Modus Ponens applied to lines 3 and 1] 595\end{proofenumerate} 596 597\noindent This proof works for any hypothesis of the form $\Gamma\turn t$ 598and any boolean term $t'$ and shows that the result of adding an 599arbitrary hypothesis to a theorem is another theorem (because the four 600lines above can be added to any proof of $\Gamma\turn t$ to get a 601proof of $\Gamma,\ t'\turn t$).\footnote{This property of the logic is 602 called {\it monotonicity}.} For example, the next session uses this 603proof to add the hypothesis \ml{``t3``} to \ml{Th6}. 604 605\begin{session} 606\begin{verbatim} 607- val Th9 = ASSUME ``t3:bool``; 608> val Th9 = [t3] |- t3 : thm 609 610- val Th10 = DISCH ``t3:bool`` Th6; 611> val Th10 = [t1 ==> t2, t1] |- t3 ==> t2 : thm 612 613- val Th11 = MP Th10 Th9; 614> val Th11 = [t1 ==> t2, t1, t3] |- t2 : thm 615\end{verbatim} 616\end{session} 617 618 619 A {\it derived rule\/} is an \ML{} procedure that generates a proof 620 from given hypotheses each time it is invoked. The hypotheses are 621 the arguments of the rule. To illustrate this, a rule, called 622 \ml{ADD\_ASSUM}, will now be defined as an \ML{} procedure that 623 carries out the proof above. In standard notation this would be 624 described by: 625 626\[ \frac{\Gamma\turn t}{\Gamma,\ t'\turn t} \] 627 628\noindent The \ML{} definition is: 629 630\begin{session} 631\begin{verbatim} 632- fun ADD_ASSUM t th = let 633 val th9 = ASSUME t 634 val th10 = DISCH t th 635 in 636 MP th10 th9 637 end; 638> val ADD_ASSUM = fn : term -> thm -> thm 639 640- ADD_ASSUM ``t3:bool`` Th6; 641> val it = [t1, t1 ==> t2, t3] |- t2 : thm 642\end{verbatim} 643\end{session} 644 645\noindent The body of \ml{ADD\_ASSUM} has been coded to mirror the proof done 646in session~10 above, so as to show how an interactive proof can be 647generalized into a procedure. But \ml{ADD\_ASSUM} can be written much 648more concisely as: 649 650\begin{session} 651\begin{verbatim} 652- fun ADD_ASSUM t th = MP (DISCH t th) (ASSUME t); 653> val ADD_ASSUM = fn : term -> thm -> thm 654 655- ADD_ASSUM ``t3:bool`` Th6; 656val it = [t1 ==> t2, t1, t3] |- t2 : thm 657\end{verbatim} 658\end{session} 659 660Another example of a derived inference rule is \ml{UNDISCH}; this moves the antecedent of an implication to the assumptions. 661\[ 662\frac{\Gamma\turn t_1\imp t_2}{\Gamma,\ t_1\turn t_2} 663\] 664An \ML{} derived rule that implements this is: 665 666 667\begin{session} 668\begin{verbatim} 669- fun UNDISCH th = MP th (ASSUME(#1(dest_imp(concl th)))); 670> val UNDISCH = fn : thm -> thm 671 672- Th10; 673> val it = [t1 ==> t2, t1] |- t3 ==> t2 : thm 674 675- UNDISCH Th10; 676> val it = [t1, t1 ==> t2, t3] |- t2 : thm 677\end{verbatim} 678\end{session} 679 680\noindent Each time \ml{UNDISCH\ $\Gamma\turn t_1\imp t_2$} is executed, 681the following proof is performed: 682 683\begin{proofenumerate} 684\item $ t_1\turn t_1$ \hfill [Assumption introduction] 685\item $ \Gamma\turn t_1\imp t_2$ \hfill [Hypothesis] 686\item $ \Gamma,\ t_1\turn t_2$ \hfill [Modus Ponens applied to lines 2 and 1] 687\end{proofenumerate} 688 689The rules \ml{ADD\_ASSUM} and \ml{UNDISCH} are the first derived rules 690defined when the \HOL{} system is built. For a description of the main 691rules see the section on derived rules in \DESCRIPTION. 692 693\subsubsection{Rewriting} 694 695An interesting derived rule is \ml{REWRITE\_RULE}. This takes a list of 696equational theorems of the form: 697 698\[ 699\Gamma\turn (u_1 = v_1) \conj (u_2 = v_2) \conj \ldots\ \conj (u_n = v_n) 700\] 701and a theorem $\Delta\turn t$ and repeatedly replaces instances of $u_i$ in $t$ by the corresponding instance of $v_i$ until no further change occurs. 702The result is a theorem $\Gamma\cup\Delta\turn t'$ where $t'$ is the result of rewriting $t$ in this way. 703The session below illustrates the use of \ml{REWRITE\_RULE}. 704In it the list of equations is the value \ml{rewrite\_list} containing the pre-proved theorems \ml{ADD\_CLAUSES} and \ml{MULT\_CLAUSES}. 705These theorems are from the theory \ml{arithmetic}, so we must use a fully qualified name with the name of the theory as the first component to refer to them. 706(Alternatively, we could, as in the Euclid example of section~\ref{chap:euclid}, use \ml{open} to bring declare all of the values in the theory at the top level.) 707 708\begin{session} 709\begin{verbatim} 710- open arithmeticTheory; 711 ... 712 713- val rewrite_list = [ADD_CLAUSES,MULT_CLAUSES]; 714> val rewrite_list = 715 [ |- (0 + m = m) /\ (m + 0 = m) /\ (SUC m + n = SUC (m + n)) /\ 716 (m + SUC n = SUC (m + n)), 717 |- !m n. 718 (0 * m = 0) /\ (m * 0 = 0) /\ (1 * m = m) /\ (m * 1 = m) /\ 719 (SUC m * n = m * n + n) /\ (m * SUC n = m + m * n)] 720 : thm list 721\end{verbatim} 722\end{session} 723 724\begin{session} 725\begin{verbatim} 726- REWRITE_RULE rewrite_list (ASSUME ``(m+0)<(1*n)+(SUC 0)``); 727> val it = [m + 0 < 1 * n + SUC 0] |- m < SUC n : thm 728\end{verbatim} 729\end{session} 730 731\noindent 732This can then be rewritten using another pre-proved theorem 733\ml{LESS\_THM}, this one from the theory \ml{prim\_rec}: 734 735\begin{session} 736\begin{verbatim} 737- REWRITE_RULE [prim_recTheory.LESS_THM] it; 738> val it = [m + 0 < 1 * n + SUC 0] |- (m = n) \/ m < n : thm 739\end{verbatim} 740\end{session} 741 742\ml{REWRITE\_RULE} is not a primitive in \HOL, but is a derived rule. 743It is inherited from Cambridge \LCF\ and was implemented by Larry Paulson (see his paper \cite{lcp-rewrite} for details). 744In addition to the supplied equations, \ml{REWRITE\_RULE} has some built in standard simplifications: 745 746\begin{session} 747\begin{verbatim} 748- REWRITE_RULE [] (ASSUME ``(T /\ x) \/ F ==> F``); 749> val it = [T /\ x \/ F ==> F] |- ~x : thm 750\end{verbatim} 751\end{session} 752 753There are elaborate facilities in \HOL{} for producing customized rewriting tools which scan through terms in user programmed orders; \ml{REWRITE\_RULE} is the tip of an iceberg, see \DESCRIPTION\ for more details. 754 755\section{Goal Oriented Proof: Tactics and Tacticals} 756\label{backward}\label{tactics} 757 758The style of forward proof described in the previous section is 759unnatural and too `low level' for many applications. An important 760advance in proof generating methodology was made by Robin Milner in 761the early 1970s when he invented the notion of {\it tactics\/}. A 762tactic is a function that does two things. 763\begin{myenumerate} 764\item Splits a `goal' into `subgoals'. 765\item Keeps track of the reason why solving the subgoals will solve the goal. 766\end{myenumerate} 767 768\noindent Consider, for example, the rule of $\wedge$-introduction\footnote{In 769 higher order logic this is a derived rule; in first order logic it 770 is usually primitive. In HOL the rule is called {\tt CONJ} and its 771 derivation is given in \DESCRIPTION.} shown below: 772 773\[ \frac{\Gamma_1\turn 774t_1\qquad\qquad\qquad\Gamma_2\turn t_2}{\Gamma_1\cup\Gamma_2 \turn t_1\conj 775t_2} \] 776 777 778\noindent In \HOL, $\wedge$-introduction is represented by the \ML{} function 779\ml{CONJ}: 780 781\[\ml{CONJ}\ (\Gamma_1\turn t_1)\ (\Gamma_2\turn t_2) \ \ \leadsto\ 782\ (\Gamma_1\cup\Gamma_2\turn t_1\conj t_2)\] 783 784\noindent This is illustrated in the 785following new session (note that the session number has been reset to 786{\small\sl 1}: 787 788\setcounter{sessioncount}{0} 789\begin{session} 790\begin{verbatim} 791- show_assums := true; 792val it = () : unit 793 794- val Th1 = ASSUME ``A:bool`` and Th2 = ASSUME ``B:bool``; 795> val Th1 = [A] |- A : thm 796 val Th2 = [B] |- B : thm 797 798- val Th3 = CONJ Th1 Th2; 799> val Th3 = [A, B] |- A /\ B : thm 800\end{verbatim} 801\end{session} 802 803 Suppose the goal is to prove $A\conj B$, then this rule says that 804 it is sufficient to prove the two subgoals $A$ and $B$, because 805 from $\turn A$ and $\turn B$ the theorem $\turn A\conj B$ can be 806 deduced. Thus: 807 808\begin{myenumerate} 809\item To prove $\turn A \conj B$ it is sufficient to 810 prove $\turn A$ and $\turn B$. 811\item The justification for the reduction of the 812goal $\turn A \conj B$ to the two subgoals $\turn A$ 813and $\turn B$ is the rule of $\wedge$-introduction. 814\end{myenumerate} 815 816A \emph{goal} in \HOL{} is a pair \ml{([$t_1$,\ldots,$t_n$],$t$)} of \ML{} type \ml{term list~*~term}. 817An \emph{achievement} of such a goal is a theorem \ml{$t_1$,$\ldots$,$t_n$\ |-\ $t$}. 818A tactic is an \ML{} function that when applied to a goal generates subgoals together with a \emph{justification function} or {\it validation\/}, which will be an \ML{} derived inference rule, that can be used to infer an achievement of the original goal from achievements of the subgoals. 819 820If $T$ is a tactic (\ie\ an \ML{} function of type \ml{goal\,->\,(goal\,list\,*\,(thm\,list\,->\,thm))}) and $g$ is a goal, then applying $T$ to 821$g$ (\ie\ evaluating the \ML{} expression $T\ g$) will result in an 822object which is a pair whose first component is a list of goals and 823whose second component is a justification function, \ie\ a value with 824\ML{} type {\small\verb|thm list -> thm|}. 825 826An example tactic is \ml{CONJ\_TAC} which implements (i) and (ii) above. 827For example, consider the utterly trivial goal of showing \holtxt{T~/\bs{}~T}, where \ml{T} is a constant that stands for $\top$ (truth): 828 829\begin{session} 830\begin{verbatim} 831- val goal1 = ([]:term list, ``T /\ T``); 832> val goal1 = ([], ``T /\ T``) : term list * term 833 834- CONJ_TAC goal1; 835> val it = 836 ([([], ``T``), ([], ``T``)], fn) 837 : (term list * term) list * (thm list -> thm) 838 839- val (goal_list,just_fn) = it; 840> val goal_list = 841 [([], ``T``), ([], ``T``)] 842 : (term list * term) list 843 val just_fn = fn : thm list -> thm 844\end{verbatim} 845\end{session} 846 847\noindent \ml{CONJ\_TAC} has produced a goal list consisting of two identical 848subgoals of just showing \ml{([],"T")}. Now, there is a preproved 849theorem in \HOL, called \ml{TRUTH}, that achieves this goal: 850 851\begin{session} 852\begin{verbatim} 853- TRUTH; 854> val it = [] |- T : thm 855\end{verbatim} 856\end{session} 857 858\noindent Applying the justification function \ml{just\_fn} to a list 859of theorems achieving the goals in \ml{goal\_list} results 860in a theorem achieving the original goal: 861 862\begin{session} 863\begin{verbatim} 864- just_fn [TRUTH,TRUTH]; 865> val it = [] |- T /\ T : thm 866\end{verbatim} 867\end{session} 868 869 Although this example is trivial, it does illustrate the essential 870 idea of tactics. Note that tactics are not special 871 theorem-proving primitives; they are just \ML{} functions. For 872 example, the definition of \ml{CONJ\_TAC} is simply: 873 874\begin{hol} 875\begin{verbatim} 876 fun CONJ_TAC (asl,w) = let 877 val (l,r) = dest_conj w 878 in 879 ([(asl,l), (asl,r)], fn [th1,th2] => CONJ th1 th2) 880 end 881\end{verbatim} 882\end{hol} 883 884\noindent The function \ml{dest\_conj} splits a conjunction into its 885two conjuncts: If \ml{(asl,``$t_1$}{\small\verb|/\|}\ml{$t_2$``)} is a 886goal, then \ml{CONJ\_TAC} splits it into the list of two subgoals 887\ml{(asl,$t_1$)} and \ml{(asl,$t_2$)}. The justification function, 888{\small\verb|fn [th1,th2] => CONJ th1 th2|} takes a list 889\ml{[$th_1$,$th_2$]} of theorems and applies the rule \ml{CONJ} to 890$th_1$ and $th_2$. 891 892To summarize: if $T$ is a tactic and $g$ is a goal, then applying $T$ 893to $g$ will result in a pair whose first component is a list of goals 894and whose second component is a justification function, with \ML{} type 895{\small\verb|thm list -> thm|}. 896 897Suppose 898$T\ g${\small\verb| = ([|}$g_1${\small\verb|,|}$\ldots${\small\verb|,|}$g_n${\small\verb|],|}$p${\small\verb|)|}. 899The idea is that $g_1$ , $\ldots$ , $g_n$ are subgoals and $p$ is a 900`justification' of the reduction of goal $g$ to subgoals $g_1$ , 901$\ldots$ , $g_n$. Suppose further that the subgoals $g_1$ , $\ldots$ 902, $g_n$ have been solved. This would mean that theorems $th_1$ , 903$\ldots$ , $th_n$ had been proved such that each $th_i$ ($1\leq i\leq 904n$) `achieves' the goal $g_i$. The justification $p$ (produced by 905applying $T$ to $g$) is an \ML{} function which when applied to the 906list 907{\small\verb|[|}$th_1${\small\verb|,|}$\ldots${\small\verb|,|}$th_n${\small\verb|]|} 908returns a theorem, $th$, which `achieves' the original goal $g$. Thus 909$p$ is a function for converting a solution of the subgoals to a 910solution of the original goal. If $p$ does this successfully, then the 911tactic $T$ is called {\it valid\/}. Invalid tactics cannot result in 912the proof of invalid theorems; the worst they can do is result in 913insolvable goals or unintended theorems being proved. If $T$ were 914invalid and were used to reduce goal $g$ to subgoals $g_1$ , $\ldots$ 915, $g_n$, then effort might be spent proving theorems $th_1$ , $\ldots$ 916, $th_n$ to achieve the subgoals $g_1$ , $\ldots$ , $g_n$, only to 917find out after the work is done that this is a blind alley because 918$p${\small\verb|[|}$th_1${\small\verb|,|}$\ldots${\small\verb|,|}$th_n${\small\verb|]|} 919doesn't achieve $g$ (\ie\ it fails, or else it achieves some other 920goal). 921 922A theorem {\it achieves\/} a goal if the assumptions of the theorem are 923included in the assumptions of the goal {\it and\/} if the conclusion of the 924theorems is equal (up to the renaming of bound variables) to the conclusion of 925the goal. More precisely, a theorem 926\begin{center} 927$t_1$, $\dots$, $t_m${\small\verb% |- %}$t$ 928\end{center} 929 930\noindent achieves a goal 931\begin{center} 932{\small\verb|([|}$u_1${\small\verb|,|}$\ldots${\small\verb|,|}$u_n${\small\verb|],|}$u${\small\verb|)|} 933\end{center} 934 935\noindent if and only if $\{t_1,\ldots,t_m\}$ 936is a subset of $\{u_1,\ldots,u_n\}$ and $t$ is equal to $u$ (up to 937renaming of bound variables). For example, the goal 938{\small\verb|([``x=y``, ``y=z``, ``z=w``], ``x=z``)|} is achieved by 939the theorem {\small\verb+[x=y, y=z] |- x=z+} (the assumption 940{\small\verb|``z=w``|} is not needed). 941 942A tactic {\it solves\/} a goal if it reduces the goal 943to the empty list 944of subgoals. Thus $T$ solves $g$ if 945$T\ g${\small\verb| = ([],|}$p${\small\verb|)|}. 946If this is the case and if $T$ is valid, then $p${\small\verb|[]|} 947will evaluate to a theorem achieving $g$. 948Thus if $T$ solves $g$ then the \ML{} expression 949{\small\verb|snd(|}$T\ g${\small\verb|)[]|} evaluates to 950a theorem achieving $g$. 951 952Tactics are specified using the following notation: 953 954\begin{center} 955\begin{tabular}{c} \\ 956$goal$ \\ \tacticline 957$goal_1\ \ \ goal_2 \ \ \ \cdots\ \ \ goal_n$ \\ 958\end{tabular} 959\end{center} 960 961\noindent For example, a tactic called {\small\verb|CONJ_TAC|} is described by 962 963\newcommand\ttbs{\texttt{\symbol{"5C}}} 964\newcommand\ttland{\texttt{/\ttbs}} 965 966\begin{center} 967\begin{tabular}{lr} \\ 968\multicolumn{2}{c}{$t_1$ \ttland{} $t_2$} \\ \tacticline 969$t_1$ & $t_2$ \\ 970\end{tabular} 971\end{center} 972 973 974 975\noindent Thus {\small\verb|CONJ_TAC|} reduces a goal of the form 976{\small\verb|(|}$\Gamma${\small\verb|,``|}$t_1${\small\verb|/\|}$t_2${\small\verb|``)|} 977to subgoals 978{\small\verb|(|}$\Gamma${\small\verb|,``|}$t_1${\small\verb|``)|} and {\small\verb|(|}$\Gamma${\small\verb|,``|}$t_2${\small\verb|``)|}. 979The fact that the assumptions of the top-level goal 980are propagated unchanged to the two subgoals is indicated by the absence 981of assumptions in the notation. 982 983Another example is \ml{numLib.INDUCT_TAC},\footnote{Later, we will write \ml{INDUCT_TAC} on its own, without first prefixing it with \ml{numLib}. To allow this we must issue the command \ml{open~numLib}.} the tactic for 984doing mathematical induction on the natural numbers: 985 986\begin{center} 987\begin{tabular}{lr} \\ 988\multicolumn{2}{c}{\texttt{!}$n$\texttt{.}$t[n]$} \\ \tacticline 989$t[\texttt{0}]$ & $\quad\{t[n]\}\ t[\texttt{SUC}\;n]$ 990\end{tabular} 991\end{center} 992 993{\small\verb|INDUCT_TAC|} reduces a goal 994{\small\verb|(|}$\Gamma${\small\verb|,``!|}$n${\small\verb|.|}$t[n]${\small\verb|``)|} to a basis subgoal 995{\small\verb|(|}$\Gamma${\small\verb|,``|}$t[${\small\verb|0|}$]${\small\verb|``)|} 996and an induction step subgoal 997{\small\verb|(|}$\Gamma\cup\{${\small\verb|``|}$t[n]${\small\verb|``|}$\}${\small\verb|,``|}$t[${\small\verb|SUC |}$n]${\small\verb|``)|}. 998The extra induction assumption {\small\verb|``|}$t[n]${\small\verb|``|} 999is indicated in the tactic notation with set brackets. 1000 1001\begin{session} 1002\begin{verbatim} 1003- numLib.INDUCT_TAC([], ``!m n. m+n = n+m``); 1004> val it = 1005 ([([], ``!n. 0 + n = n + 0``), 1006 ([``!n. m + n = n + m``], ``!n. SUC m + n = n + SUC m``)], fn) 1007 : (term list * term) list * (thm list -> thm) 1008\end{verbatim} 1009\end{session} 1010 1011\noindent The first subgoal is the basis case and the second subgoal is 1012the step case. 1013 1014Tactics generally fail (in the \ML{} sense, \ie\ raise an exception) if 1015they are applied to inappropriate goals. For example, 1016{\small\verb|CONJ_TAC|} will fail if it is applied to a goal whose 1017conclusion is not a conjunction. Some tactics never fail, for example 1018{\small\verb|ALL_TAC|} 1019 1020\begin{center} 1021\begin{tabular}{c} \\ 1022$t$ \\ \tacticline 1023$t$ 1024\end{tabular} 1025\end{center} 1026 1027\noindent is the `identity tactic'; it reduces a goal 1028{\small\verb|(|}$\Gamma${\small\verb|,|}$t${\small\verb|)|} to the 1029single subgoal 1030{\small\verb|(|}$\Gamma${\small\verb|,|}$t${\small\verb|)|}---\ie\ it 1031has no effect. {\small\verb|ALL_TAC|} is useful for writing complex 1032tactics using tacticals. 1033 1034 1035\subsection{Using tactics to prove theorems} 1036\label{using-tactics} 1037 1038Suppose goal $g$ is to be solved. If $g$ is simple it might be 1039possible to immediately think up a tactic, $T$ say, which reduces it 1040to the empty list of subgoals. If this is the case then executing: 1041 1042$\ ${\small\verb| val (|}$gl${\small\verb|,|}$p${\small\verb|) = |}$T\ g$ 1043 1044\noindent will bind $p$ to a function which when applied to the empty list 1045of theorems yields a theorem $th$ achieving $g$. (The declaration 1046above will also bind $gl$ to the empty list of goals.) Thus a theorem 1047achieving $g$ can be computed by executing: 1048 1049$\ ${\small\verb| val |}$th${\small\verb| = |}$p${\small\verb|[]|} 1050 1051\noindent This will be illustrated using \ml{REWRITE\_TAC} which takes a list 1052of equations (empty in the example that follows) and tries to prove a goal 1053by rewriting with these equations together with 1054\ml{basic\_rewrites}: 1055 1056\begin{session} 1057\begin{verbatim} 1058- val goal2 = ([]:term list, ``T /\ x ==> x \/ (y /\ F)``); 1059> val goal2 = ([], ``T /\ x ==> x \/ y /\ F``) : (term list * term) 1060 1061- REWRITE_TAC [] goal2; 1062> val it = ([], fn) : (term list * term) list * (thm list -> thm) 1063 1064- #2 it []; 1065> val it = [] |- T /\ x ==> x \/ y /\ F : thm 1066\end{verbatim} 1067\end{session} 1068 1069\noindent Proved theorems are usually stored in the current theory 1070so that they can be used in subsequent sessions. 1071 1072The built-in function 1073 \ml{store\_thm} of 1074\ML{} type {\small\verb|(string * term * tactic) -> thm|} facilitates the use 1075of tactics: 1076{\small\verb|store_thm("foo",|}$t${\small\verb|,|}$T${\small\verb|)|} proves 1077the goal {\small\verb|([],|}$t${\small\verb|)|} (\ie\ the goal with no 1078assumptions and conclusion $t$) using tactic $T$ and saves the resulting 1079theorem with name {\small\verb|foo|} on the current theory. 1080 1081If the theorem is not to be saved, the function \ml{prove} of type 1082{\small\verb|(term * tactic) -> thm|} can be used. Evaluating 1083{\small\verb|prove(|}$t${\small\verb|,|}$T${\small\verb|)|} proves the goal 1084{\small\verb|([],|}$t${\small\verb|)|} using $T$ and returns the result without 1085saving it. In both cases the evaluation fails if $T$ does not solve the 1086goal {\small\verb|([],|}$t${\small\verb|)|}. 1087 1088When conducting a proof that involves many subgoals and tactics, it is necessary to keep track of all the justification functions and compose them in the correct order. 1089While this is feasible even in large proofs, it is tedious. 1090\HOL{} provides a package for building and traversing the tree of subgoals, stacking the justification functions and applying them properly; this package was originally implemented for \LCF\ by Larry Paulson. 1091Its use is demonstrated below in some of the example sessions, and in Chapter~\ref{chap:euclid}. 1092It is thoroughly documented in \DESCRIPTION. 1093(In short, the \ML{} function \ml{g} establishes a goal, and the \ML{} function \ml{e} applies a tactic to the current state of the goal.) 1094 1095\subsection{Tacticals} 1096\label{tacticals} 1097 1098A {\it tactical\/} is an \ML{} function that takes one or more tactics 1099as arguments, possibly with other arguments as well, and returns a 1100tactic as its result. The various parameters passed to tacticals are 1101reflected in the various \ML{} types that the built-in tacticals have. 1102Some important tacticals in the \HOL{} system are listed below. 1103 1104\subsubsection{\tt THENL : tactic -> tactic list -> tactic} 1105 1106If tactic $T$ produces $n$ subgoals and $T_1$, $\ldots$ , $T_n$ are tactics then \ml{$T$~THENL~[$T_1$,$\ldots$,$T_n$]} is a tactic which first applies $T$ and then applies $T_i$ to the $i$th subgoal produced by $T$. 1107The tactical \ml{THENL} is useful if one wants to do different things to different subgoals. 1108 1109\ml{THENL} can be illustrated by doing the proof of $\vdash \uquant{m}m+0=m$ in 1110one step. 1111 1112\setcounter{sessioncount}{0} 1113\begin{session} 1114\begin{verbatim} 1115- g `!m. m + 0 = m`; 1116> val it = 1117 Proof manager status: 1 proof. 1118 1. Incomplete: 1119 Initial goal: 1120 !m. m + 0 = m 1121 1122- e (INDUCT_TAC THENL [REWRITE_TAC[ADD], ASM_REWRITE_TAC[ADD]]); 1123OK.. 1124> val it = 1125 Initial goal proved. 1126 |- !m. m + 0 = m 1127\end{verbatim} 1128\end{session} 1129 1130\noindent The compound tactic \[ 1131\ml{INDUCT\_TAC~THENL~[REWRITE\_TAC~[ADD],~ASM\_REWRITE\_TAC~[ADD]]} 1132\] 1133first applies \ml{INDUCT_TAC} and then applies \ml{REWRITE\_TAC[ADD]} to the first subgoal (the basis) and \ml{ASM\_REWRITE\_TAC[ADD]} to the second subgoal (the step). 1134 1135The tactical {\small\verb|THENL|} is useful for doing different things 1136to different subgoals. The tactical \ml{THEN} can be used to apply the 1137same tactic to all subgoals. 1138 1139\subsubsection{\tt THEN : tactic -> tactic -> tactic}\label{THEN} 1140 1141The tactical {\small\verb|THEN|} is an \ML{} infix. If $T_1$ and $T_2$ 1142are tactics, then the \ML{} expression $T_1${\small\verb| THEN |}$T_2$ 1143evaluates to a tactic which first applies $T_1$ and then applies $T_2$ 1144to all the subgoals produced by $T_1$. 1145 1146In fact, \ml{ASM\_REWRITE\_TAC[ADD]} will solve the basis as well as 1147the step case of the induction for $\uquant{m}m+0=m$, so there is an 1148even simpler one-step proof than the one above: 1149\setcounter{sessioncount}{0} 1150\begin{session} 1151\begin{verbatim} 1152- g `!m. m+0 = m`; 1153> val it = 1154 Proof manager status: 1 proof. 1155 1. Incomplete: 1156 Initial goal: 1157 !m. m + 0 = m 1158 1159- e(INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]); 1160OK.. 1161> val it = 1162 Initial goal proved. 1163 |- !m. m + 0 = m 1164\end{verbatim} 1165\end{session} 1166 1167\noindent This is typical: it is common to use a single tactic for several 1168goals. Here, for example, are the first four consequences of the 1169definition \ml{ADD} of addition that are pre-proved when the built-in 1170theory \ml{arithmetic} \HOL{} is made. 1171 1172\begin{hol} 1173\begin{verbatim} 1174 val ADD_0 = prove ( 1175 ``!m. m + 0 = m``, 1176 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]); 1177\end{verbatim} 1178\end{hol} 1179 1180\begin{hol} 1181\begin{verbatim} 1182 val ADD_SUC = prove ( 1183 ``!m n. SUC(m + n) = m + SUC n``, 1184 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]); 1185\end{verbatim} 1186\end{hol} 1187 1188\begin{hol} 1189\begin{verbatim} 1190 val ADD_CLAUSES = prove ( 1191 ``(0 + m = m) /\ 1192 (m + 0 = m) /\ 1193 (SUC m + n = SUC(m + n)) /\ 1194 (m + SUC n = SUC(m + n))``, 1195 REWRITE_TAC[ADD, ADD_0, ADD_SUC]); 1196\end{verbatim} 1197\end{hol} 1198 1199\begin{hol} 1200\begin{verbatim} 1201 val ADD_COMM = prove ( 1202 ``!m n. m + n = n + m``, 1203 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_0, ADD, ADD_SUC]); 1204\end{verbatim} 1205\end{hol} 1206 1207 1208\noindent These proofs are performed when the \HOL{} system is made and the 1209theorems are saved in the theory \ml{arithmetic}. The complete list of 1210proofs for this built-in theory can be found in the file 1211\ml{src/num/theories/arithmeticScript.sml}. 1212 1213 1214\subsubsection{\tt ORELSE : tactic -> tactic -> tactic}\label{ORELSE} 1215 1216The tactical {\small\verb|ORELSE|} is an \ML{} infix. If $T_1$ and 1217$T_2$ are tactics, 1218%\index{tacticals!for alternation} 1219then $T_1${\small\verb| ORELSE |}$T_2$ evaluates to a tactic which 1220applies $T_1$ unless that fails; if it fails, it applies $T_2$. 1221\ml{ORELSE} is defined in \ML{} as a curried infix by\footnote{This is 1222 a minor simplification.} 1223 1224\begin{hol} 1225 {\small\verb|(|}$T_1${\small\verb| ORELSE |}$T_2${\small\verb|)|} $g$ 1226 {\small\verb|=|} $T_1\; g$ {\small\verb|handle _ =>|} $T_2\; g$ 1227\end{hol} 1228%\index{alternation!of tactics|)} 1229 1230\subsubsection{\tt REPEAT : tactic -> tactic} 1231 1232If $T$ is a tactic then {\small\verb|REPEAT |}$T$ is a tactic which 1233repeatedly applies $T$ until it fails. This can be illustrated in 1234conjunction with \ml{GEN\_TAC}, which is specified by: 1235 1236\begin{center} 1237\begin{tabular}{c} \\ 1238{\small\verb|!|}$x${\small\verb|.|}$t[x]$ 1239\\ \tacticline 1240$t[x']$ 1241\\ 1242\end{tabular} 1243\end{center} 1244 1245\begin{itemize} 1246\item Where $x'$ is a variant of $x$ 1247not free in the goal or the assumptions. 1248\end{itemize} 1249 1250\noindent \ml{GEN\_TAC} strips off one quantifier; 1251\ml{REPEAT\ GEN\_TAC} strips off all quantifiers: 1252 1253\begin{session} 1254\begin{verbatim} 1255- g `!x y z. x+(y+z) = (x+y)+z`; 1256> val it = 1257 Proof manager status: 1 proof. 1258 1. Incomplete: 1259 Initial goal: 1260 !x y z. x + (y + z) = x + y + z 1261 1262- e GEN_TAC; 1263OK.. 12641 subgoal: 1265> val it = 1266 !y z. x + (y + z) = x + y + z 1267 1268- e (REPEAT GEN_TAC); 1269OK.. 12701 subgoal: 1271> val it = 1272 x + (y + z) = x + y + z 1273\end{verbatim} 1274\end{session} 1275 1276\subsection{Some tactics built into \HOL{}} 1277 1278This section contains a summary of some of the tactics built into the 1279\HOL{} system (including those already discussed). The tactics given 1280here are those that are used in the parity checking example. 1281 1282\subsubsection{\tt REWRITE\_TAC : thm list -> tactic} 1283\label{rewrite} 1284 1285\begin{itemize} 1286\item{\bf Summary:} {\small\verb|REWRITE_TAC[|}$th_1${\small\verb|,|}$\ldots${\small\verb|,|}$th_n${\small\verb|]|} 1287simplifies the goal by rewriting 1288it with the explicitly given theorems $th_1$, $\ldots$ , $th_n$, 1289and various built-in rewriting rules. 1290 1291 1292\begin{center} 1293\begin{tabular}{c} \\ 1294$\{t_1, \ldots , t_m\}t$ 1295\\ \tacticline 1296$\{t_1, \ldots , t_m\}t'$ 1297\\ 1298\end{tabular} 1299\end{center} 1300 1301\noindent where $t'$ is obtained from $t$ by rewriting with 1302\begin{enumerate} 1303\item $th_1$, $\ldots$ , $th_n$ and 1304\item the standard rewrites held in the \ML{} variable {\small\verb|basic_rewrites|}. 1305\end{enumerate} 1306 1307\item{\bf Uses:} Simplifying goals using previously proved theorems. 1308 1309\item{\bf Other rewriting tactics}: 1310\begin{enumerate} 1311\item {\small\verb|ASM_REWRITE_TAC|} adds the assumptions of the goal 1312 to the list of theorems used for rewriting. 1313\item {\small\verb|PURE_REWRITE_TAC|} uses neither the assumptions nor 1314 the built-in rewrites. 1315\item {\small\verb|RW_TAC|} of type \ml{simpLib.simpset -> thm 1316 list -> tactic}. A \ml{simpset} is a special collection of 1317 rewriting theorems and other theorem-proving functionality. Values 1318 defined by \HOL{} include \ml{bossLib.std\_ss}, which has basic 1319 knowledge of the boolean connectives, \ml{bossLib.arith\_ss} which 1320 ``knows'' all about arithmetic, and \ml{HOLSimps.list\_ss}, which 1321 includes theorems appropriate for lists, pairs, and arithmetic. 1322 Additional theorems for rewriting can be added using the second 1323 argument of \ml{RW\_TAC}. 1324\end{enumerate} 1325\end{itemize} 1326 1327 1328\subsubsection{\tt CONJ\_TAC : tactic}\label{CONJTAC} 1329 1330\begin{itemize} 1331 1332\item{\bf Summary:} Splits a 1333goal {\small\verb|``|}$t_1${\small\verb|/\|}$t_2${\small\verb|``|} into two subgoals {\small\verb|``|}$t_1${\small\verb|``|} 1334and {\small\verb|``|}$t_2${\small\verb|``|}. 1335 1336\begin{center} 1337\begin{tabular}{lr} \\ 1338\multicolumn{2}{c}{$t_1$ \ttland{} $t_2$} \\ \tacticline 1339$t_1$ & $t_2$ \\ 1340\end{tabular} 1341\end{center} 1342 1343\item{\bf Uses:} Solving conjunctive goals. 1344\ml{CONJ_TAC} is invoked by \ml{STRIP_TAC} (see below). 1345 1346\end{itemize} 1347 1348\subsubsection{\tt EQ\_TAC : tactic}\label{EQTAC} 1349 1350 1351\begin{itemize} 1352 1353\item{\bf Summary:} 1354\ml{EQ_TAC} splits an equational goal into two implications (the `if-case' and the `only-if' case): 1355 1356\begin{center} 1357 1358 1359\begin{tabular}{lr} \\ 1360\multicolumn{2}{c}{$u\; \ml{=}\; v$} \\ \tacticline 1361$u\; \ml{==>}\; v$ & $\quad v\; \ml{==>}\; u$ \\ 1362\end{tabular} 1363\end{center} 1364 1365\item{\bf Use:} Proving logical equivalences, \ie\ goals of the form 1366``$u$\ml{=}$v$'' where $u$ and $v$ are boolean terms. 1367 1368\end{itemize} 1369 1370 1371 1372 1373\subsubsection{\tt DISCH\_TAC : tactic}\label{DISCHTAC} 1374 1375\begin{itemize} 1376 1377\item{\bf Summary:} Moves the antecedent 1378of an implicative goal into the assumptions. 1379 1380\begin{center} 1381\begin{tabular}{c} \\ 1382$u${\small\verb| ==> |}$v$ 1383\\ \tacticline 1384$\{u\}v$ 1385\\ 1386\end{tabular} 1387\end{center} 1388 1389 1390\item{\bf Uses:} Solving goals of the form \holtxt{$u$~==>~$v$} by assuming \holtxt{$u$} and then solving \holtxt{$v$}. 1391{\small\verb|STRIP_TAC|} (see below) will invoke {\small\verb|DISCH_TAC|} on implicative goals. 1392\end{itemize} 1393 1394\subsubsection{\tt GEN\_TAC : tactic} 1395 1396\begin{itemize} 1397 1398\item{\bf Summary:} Strips off one universal quantifier. 1399 1400 1401\begin{center} 1402\begin{tabular}{c} \\ 1403{\small\verb|!|}$x${\small\verb|.|}$t[x]$ 1404\\ \tacticline 1405$t[x']$ 1406\\ 1407\end{tabular} 1408\end{center} 1409 1410\noindent Where $x'$ is a variant of $x$ 1411not free in the goal or the assumptions. 1412 1413\item{\bf Uses:} Solving universally quantified goals. 1414{\small\verb|REPEAT GEN_TAC|} strips off all 1415universal quantifiers and is often the first thing one does in a proof. 1416{\small\verb|STRIP_TAC|} (see below) applies {\small\verb|GEN_TAC|} to universally quantified goals. 1417\end{itemize} 1418 1419 1420\subsubsection{\tt PROVE\_TAC : thm list -> tactic} 1421 1422\begin{itemize} 1423\item {\bf Summary:} Used to do first order reasoning, solving the 1424 goal completely if successful, failing otherwise. Using the 1425 provided theorems and the assumptions of the goal, 1426 {\small\verb|PROVE_TAC|} does a search for possible proofs of the 1427 goal. Eventually fails if the search fails to find a proof shorter 1428 than a reasonable depth. 1429\item {\bf Uses:} To finish a goal off when it is clear that it is a 1430 consequence of the assumptions and the provided theorems. 1431\end{itemize} 1432 1433 1434\subsubsection{\tt STRIP\_TAC : tactic} 1435 1436\begin{itemize} 1437 1438\item{\bf Summary:} Breaks a goal apart. {\small\verb|STRIP_TAC|} 1439 removes one outer connective from the goal, using 1440 {\small\verb|CONJ_TAC|}, {\small\verb|DISCH_TAC|}, 1441 {\small\verb|GEN_TAC|}, \etc\ If the goal is 1442$t_1${\small\verb|/\|}$\cdots${\small\verb|/\|}$t_n${\small\verb| ==> |}$t$ 1443then {\small\verb|STRIP_TAC|} makes each $t_i$ into a separate assumption. 1444 1445\item{\bf Uses:} Useful for splitting a goal up into manageable pieces. 1446Often the best thing to do first is {\small\verb|REPEAT STRIP_TAC|}. 1447\end{itemize} 1448 1449\subsubsection{\tt ACCEPT\_TAC : thm -> tactic}\label{ACCEPTTAC} 1450 1451 1452\begin{itemize} 1453 1454\item{\bf Summary:} {\small\verb|ACCEPT_TAC |}$th$ 1455is a tactic that solves any goal that is 1456achieved by $th$. 1457 1458\item{\bf Use:} Incorporating forward proofs, or theorems already 1459 proved, into goal directed proofs. For example, one might reduce a 1460 goal $g$ to subgoals $g_1$, $\dots$, $g_n$ using a tactic $T$ and 1461 then prove theorems $th_1$ , $\dots$, $th_n$ respectively achieving 1462 these goals by forward proof. The tactic 1463 1464\[\ml{ T THENL[ACCEPT\_TAC }th_1\ml{,}\ldots\ml{,ACCEPT\_TAC }th_n\ml{]} 1465\] 1466 1467would then solve $g$, where \ml{THENL} 1468%\index{THENL@\ml{THENL}} 1469is the tactical that applies the respective elements of the tactic 1470list to the subgoals produced by \ml{T}. 1471 1472\end{itemize} 1473 1474 1475 1476\subsubsection{\tt ALL\_TAC : tactic} 1477 1478\begin{itemize} 1479\item{\bf Summary:} Identity tactic for the tactical {\small\verb%THEN%} 1480(see \DESCRIPTION). 1481 1482\item{\bf Uses:} 1483\begin{enumerate} 1484\item Writing tacticals (see description of {\small\verb|REPEAT|} 1485in \DESCRIPTION). 1486\item With {\small\verb%THENL%}; for example, if tactic $T$ produces two subgoals 1487and we want to apply $T_1$ 1488to the first one but to do nothing to the second, then 1489the tactic to use is \ml{$T$~THENL[$T_1$,ALL_TAC]}. 1490\end{enumerate} 1491\end{itemize} 1492 1493\subsubsection{\tt NO\_TAC : tactic} 1494 1495\begin{itemize} 1496\item{\bf Summary:} Tactic that always fails. 1497 1498\item{\bf Uses:} Writing tacticals. 1499\end{itemize} 1500 1501%%% Local Variables: 1502%%% mode: latex 1503%%% TeX-master: "tutorial" 1504%%% End: 1505