\chapter{The \HOL{} Logic}\label{HOLlogic} The \HOL{} system supports \emph{higher order logic}. This is a version of predicate calculus with three main extensions: \begin{itemize} \item Variables can range over functions and predicates (hence `higher order'). \item The logic is \emph{typed}. \item There is no separate syntactic category of \emph{formulae} (terms of type \ml{bool} fulfill that role). \end{itemize} In 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. It is assumed the reader is familiar with predicate logic. The syntax and semantics of the particular logical system supported by \HOL{} is described in detail in \DESCRIPTION. Readers 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}. The table below summarizes a useful subset of the (ASCII) notation used in \HOL. \begin{center} \begin{tabular}{|l|l|l|l|} \hline \multicolumn{4}{|c|}{ } \\ \multicolumn{4}{|c|}{\bf Terms of the HOL Logic} \\ \multicolumn{4}{|c|}{ } \\ {\it Kind of term} & {\it \HOL{} notation} & {\it Standard notation} & {\it Description} \\ \hline & & & \\ Truth & {\small\verb|T|} & $\top$ & {\it true}\\ \hline Falsity & {\small\verb|F|} & $\bot$ & {\it false}\\ \hline Negation & {\small\verb|~|}$t$ & $\neg t$ & {\it not}$\ t$\\ \hline Disjunction & $t_1${\small\verb|\/|}$t_2$ & $t_1\vee t_2$ & $t_1\ ${\it or}$\ t_2$ \\ \hline Conjunction & $t_1${\small\verb|/\|}$t_2$ & $t_1\wedge t_2$ & $t_1\ ${\it and}$\ t_2$ \\ \hline Implication & $t_1${\small\verb|==>|}$t_2$ & $t_1\imp t_2$ & $t_1\ ${\it implies}$\ t_2$ \\ \hline Equality & $t_1${\small\verb|=|}$t_2$ & $t_1 = t_2$ & $t_1\ ${\it equals}$\ t_2$ \\ \hline $\forall$-quantification & {\small\verb|!|}$x${\small\verb|.|}$t$ & $\uquant{x}t$ & {\it for\ all\ }$x: t$ \\ \hline $\exists$-quantification & {\small\verb|?|}$x${\small\verb|.|}$t$ & $\equant{x}\ t$ & {\it for\ some\ }$x: t$ \\ \hline $\hilbert$-term & {\small\verb|@|}$x${\small\verb|.|}$t$ & $\hquant{x}t$ & {\it an}$\ x\ ${\it such\ that:}$\ t$ \\ \hline Conditional & {\small\verb|if|} $t$ {\small\verb|then|} $t_1$ {\small\verb|else|} $t_2$ & $(t\rightarrow t_1, t_2)$ & {\it if\ }$t${\it \ then\ }$t_1${\it\ else\ }$t_2$ \\ \hline \end{tabular} \end{center}\label{logic-table} Terms of the \HOL{} logic are represented in \ML{} by an \emph{abstract type} called {\small\verb|term|}. They are normally input between double back-quote marks. For example, the expression \holtxt{``x /\bs{} y ==> z``} evaluates in \ML{} to a term representing $\holtxt{x} \land \holtxt{y} \Rightarrow \holtxt{z}$. Terms can be manipulated by various built-in \ML{} functions. For 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.% \footnote{All of the examples below assume that the user is running \texttt{hol}, the executable for which is in the \texttt{bin/} directory. Depending 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.} \setcounter{sessioncount}{0} \begin{session} \begin{verbatim} - ``x /\ y ==> z``; > val it = ``x /\ y ==> z`` : term - dest_imp it; > val it = (``x /\ y``, ``z``) : term * term - dest_conj(#1 it); > val it = (``x``, ``y``) : term * term \end{verbatim} \end{session} Terms of the \HOL{} logic are quite similar to \ML{} expressions, and this can at first be confusing. Indeed, terms of the logic have types similar to those of \ML{} expressions. For example, \holtxt{``(1,2)``} is an \ML{} expression with \ML{} type \ml{term}. The \HOL{} type of this term is \holtxt{num \# num}. By contrast, the \ML{} expression \ml{(``1``, ``2``)} has (\ML{}) type \ml{term * term}. \paragraph{Syntax of \HOL\ types} The types of \HOL{} terms form an \ML{} type called \ml{hol_type}. Expressions having the form \ml{``: $\cdots$ ``} evaluate to logical types. The built-in function \ml{type_of} has \ML{} type \ml{term->hol_type} and returns the logical type of a term. \begin{session} \begin{verbatim} - ``(1,2)``; > val it = ``(1,2)`` : term - type_of it; > val it = ``:num # num`` : hol_type - (``1``, ``2``); > val it = (``1``, ``2``) : term * term - type_of(#1 it); > val it = ``:num`` : hol_type \end{verbatim} \end{session} To 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}. For 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``}. % \begin{session} \begin{verbatim} - ``(1,T)``; > val it = ``(1,T)`` : term - type_of it; > val it = ``:num # bool`` : hol_type \end{verbatim} \end{session} % \paragraph{Term constructors} \HOL{} terms can be input, as above, by using explicit \emph{quotation}, or they can be constructed by calling \ML{} constructor functions. The function \ml{mk_var} constructs a variable from a string and a type. In the example below, three variables of type {\small\verb|bool|} are constructed. These are used later. \begin{session} \begin{verbatim} - val x = mk_var("x", ``:bool``) and y = mk_var("y", ``:bool``) and z = mk_var("z", ``:bool``); > val x = ``x`` : term val y = ``y`` : term val z = ``z`` : term \end{verbatim} \end{session} The constructors \ml{mk_conj} and \ml{mk_imp} construct conjunctions and implications respectively. A large collection of term constructors and destructors is available for the core theories in \HOL. \begin{session} \begin{verbatim} - val t = mk_imp(mk_conj(x,y),z); > val t = ``x /\ y ==> z`` : term \end{verbatim} \end{session} \paragraph{Type checking} There 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$``}). More complex terms, such as those we have already seen above, are just compositions of terms from this simple set. In 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. Both 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). When 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. For 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}. \begin{session} \begin{verbatim} - ``~x``; > val it = ``~x`` : term \end{verbatim} \end{session} In the next two cases, the type of \ml{x} and \ml{y} cannot be deduced. (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. Thus \ml{x} is not constrained to have the type \ml{bool} in the second quotation.) \begin{session} \begin{verbatim} - ``x``; <> > val it = ``x`` : Term.term - type_of it; > val it = ``:'a`` : hol_type - ``(x,y)``; <> > val it = ``(x,y)`` : term - type_of it; > val it = ``:'a # 'b`` : hol_type \end{verbatim} \end{session} If 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. \paragraph{Type constraints} Alternatively, it is possible to explicitly indicate the required types by using the notation \ml{``$\mathit{term}$:$\mathit{type}$``}, as illustrated below. \begin{session} \begin{verbatim} - ``x:num``; > val it = ``x`` : term - type_of it; > val it = ``:num`` : hol_type \end{verbatim} \end{session} \paragraph{Function application types} An 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$. Contrarily, an application $(t_1\ t_2)$ is badly typed if $t_1$ is not a function: \begin{session} \begin{verbatim} - ``1 2``; Type inference failure: unable to infer a type for the application of (1 :num) to (2 :num) unification failure message: unify failed ! Uncaught exception: ! HOL_ERR \end{verbatim} \end{session} \noindent or if it is a function, but $t_2$ is not in its domain: \begin{session} \begin{verbatim} - ``~1``; Type inference failure: unable to infer a type for the application of $~ :bool -> bool at line 1, character 3 to (1 :num) unification failure message: unify failed ! Uncaught exception: ! HOL_ERR \end{verbatim} \end{session} The 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). Putting \holtxt{\$} in front of any symbol causes the parser to ignore any special syntactic status (like being an infix) it might have. The same effect can be achieved by enclosing the symbol in parentheses. This is analogous to the way in which \texttt{op} is used in \ML. \begin{session} \begin{verbatim} - ``$==> t1 t2``; > val it = ``t1 ==> t2`` : term - ``(/\) t1 t2``; > val it = ``t1 /\ t2`` : term \end{verbatim} \end{session} \paragraph{Function types} Functions 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. \begin{session} \begin{verbatim} - type_of ``(==>)``; > val it = ``:bool -> bool -> bool`` : hol_type - type_of ``$+``; > val it = ``:num -> num -> num`` : hol_type \end{verbatim} \end{session} \noindent Again, both \holtxt{+} and \holtxt{==>} are infixes, so their use in contexts where they are not being used as such requires syntax-escaping. The session below illustrates the use of these constants as infixes; it also illustrates object language versus meta-language types. \begin{session} \begin{verbatim} - ``(x + 1, t1 ==> t2)``; > val it = ``(x + 1,t1 ==> t2)`` : term - type_of it; > val it = ``:num # bool`` : hol_type - (``x=1``, ``t1==>t2``); > val it = (``x = 1``, ``t1 ==> t2``) : term * term - (type_of (#1 it), type_of (#2 it)); > val it = (``:bool``, ``:bool``) : hol_type * hol_type \end{verbatim} \end{session} Lambda-terms, or $\lambda$-terms, denote functions. The symbol `\holtxt{\bs}' is used as an ASCII approximation to $\lambda$. Thus `{\small\verb|\|}$x$\ml{.}$t$' should be read as `$\lquant{x}t$'. For example, {\small\verb|``\x. x+1``|} is a term that denotes the function $n\mapsto n{+}1$. \begin{session} \begin{verbatim} - ``\x. x + 1``; > val it = ``\x. x + 1`` : term - type_of it; > val it = ``:num -> num`` : hol_type \end{verbatim} \end{session} Other binding symbols in the logic are its two most important quantifiers: \ml{!} and \ml{?}, universal and existential quantifiers. For example, the logical statement that every number is either even or odd might be phrased as \begin{verbatim} !n. (n MOD 2 = 1) \/ (n MOD 2 = 0) \end{verbatim} while a version of Euclid's result about the infinitude of primes is: \begin{verbatim} !n. ?p. prime p /\ p > n \end{verbatim} % Binding symbols such as these can be used over multiple `parameters' thus: \begin{session} \begin{verbatim} - ``\x y. (x, y * x)``; > val it = ``\x y. (x,y * x)`` : term - type_of it; > val it = ``:num -> num -> num # num`` : hol_type - ``!x y. x <= x + y``; > val it = ``!x y. x <= x + y`` : term \end{verbatim} \end{session} \section{Basic Proof in \HOL{}} \newcommand\tacticline{\hline \hline} \newenvironment{proofenumerate}{\begin{enumerate}}{\end{enumerate}} % proofenumerate is distinguished from a normal enumeration so that % h e v e a can spot these special cases and treat them better. \setcounter{sessioncount}{0} This section discusses the nature of proof in \HOL{}. For 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}. A theorem is the last element of a proof. Theorems are represented in \HOL{} by values of an abstract type \ml{thm}. The only way to create theorems is by generating such a proof. In \HOL, following \LCF, this consists in applying \ML{} functions representing \emph{rules of inference} to axioms or previously generated theorems. The sequence of such applications directly corresponds to a logician's proof. There are five axioms of the \HOL{} logic and eight primitive inference rules. The axioms are bound to ML names. For example, the Law of Excluded Middle is bound to the \ML{} name \ml{BOOL_CASES_AX}:\footnote{% Note how the term-printer has rendered the equalities in the theorem with the \holtxt{<=>} symbol rather than \holtxt{=}. The underlying constant is the same, but the printing is a clue for the user that this is equality on boolean values. The 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.% } \begin{session} \begin{verbatim} - BOOL_CASES_AX; > val it = |- !t. (t <=> T) \/ (t <=> F) : thm \end{verbatim} \end{session} Theorems are printed with a preceding turnstile {\small\verb+|-+} as illustrated above; the symbol `{\small\verb|!|}' is the universal quantifier `$\forall$'. Rules of inference are \ML{} functions that return values of type \ml{thm}. An example of a rule of inference is {\it specialization\/} (or $\forall$-elimination). In standard `natural deduction' notation this is: \[ \frac{\Gamma\turn \uquant{x}t}{\Gamma\turn t[t'/x]}\] \begin{itemize} \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. \end{itemize} \noindent This rule is represented in \ML{} by a function \ml{SPEC},% \footnote{\ml{SPEC} is not a primitive rule of inference in the HOL logic, but is a derived rule. Derived rules are described in Section~\ref{forward}.} which 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]$. \begin{session} \begin{verbatim} - val Th1 = BOOL_CASES_AX; > val Th1 = |- !t. (t <=> T) \/ (t <=> F) : thm - val Th2 = SPEC ``1 = 2`` Th1; > val Th2 = |- ((1 = 2) <=> T) \/ ((1 = 2) <=> F) : thm \end{verbatim} \end{session} This session consists of a proof of two steps: using an axiom and applying the rule \ml{SPEC}; it interactively performs the following proof: \begin{samepage} \begin{proofenumerate} \item $ \turn \uquant{t}\;\; t\Leftrightarrow\top \;\disj\; t\Leftrightarrow\bot$ \hfill [Axiom \ml{BOOL\_CASES\_AX}] \item $ \turn (1{=}2)\Leftrightarrow\top\ \disj\ (1{=}2)\Leftrightarrow\bot$\hfill [Specializing line 1 to `$1{=}2$'] \end{proofenumerate} \end{samepage} If 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. For 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. When 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.% \footnote{The \ml{Raise} function passes on all of the exceptions it sees; it does not affect the semantics of the computation at all. However, when passed a \ml{HOL\_ERR} exception, it prints out some useful information before passing the exception on to the next level.} \begin{session} \begin{verbatim} - SPEC ``1=2`` Th2; ! Uncaught exception: ! HOL_ERR - SPEC ``1 = 2`` Th2 handle e => Raise e; Exception raised at Thm.SPEC: ! Uncaught exception: ! HOL_ERR \end{verbatim} \end{session} However, as this session illustrates, the failure message does not always indicate the exact reason for failure. Detailed failure conditions for rules of inference are given in \REFERENCE. A proof in the \HOL{} system is constructed by repeatedly applying inference rules to axioms or to previously proved theorems. Since proofs may consist of millions of steps, it is necessary to provide tools to make proof construction easier for the user. The proof generating tools in the \HOL{} system are just those of \LCF, and are described later. The 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\/}. Such a theorem asserts that if its assumptions are true then so is its conclusion. Its truth conditions are thus the same as those for the single term $(t_1\,\ml{/\bs}\ldots\ml{/\bs}\,t_n)\,\ml{==>}\,t$. Theorems with no assumptions are printed out in the form \ml{|-}$\ t$. The five axioms and eight primitive inference rules of the \HOL{} logic are described in detail in the document \DESCRIPTION. Every value of type \ml{thm} in the \HOL{} system can be obtained by repeatedly applying primitive inference rules to axioms. When the \HOL{} system is built, the eight primitive rules of inference are defined and the five axioms are bound to their \ML{} names. All other predefined theorems are proved using rules of inference as the system is made.\footnote{This is a slight over-simplification.} This is one of the reasons why building \ml{hol} takes so long. In the rest of this section, the process of \emph{forward proof}, which has just been sketched, is described in more detail. In Section~\ref{tactics} \emph{goal directed proof} is described, including the important notions of \emph{tactics} and \emph{tacticals}, due to Robin Milner. \section{Forward proof} \label{forward} Three of the primitive inference rules of the \HOL{} logic are \ml{ASSUME} (assumption introduction), \ml{DISCH} (discharging or assumption elimination) and \ml{MP} (Modus Ponens). These rules will be used to illustrate forward proof and the writing of derived rules. The inference rule \ml{ASSUME} generates theorems of the form \ml{$t$ |- $t$}. Note, however, that the \ML{} printer prints each assumption as a dot (but this default can be changed; see below). The function \ml{dest\_thm} decomposes a theorem into a pair consisting of list of assumptions and the conclusion. \begin{session} \begin{verbatim} - val Th3 = ASSUME ``t1==>t2``;; > val Th3 = [.] |- t1 ==> t2 : thm - dest_thm Th3; > val it = ([``t1 ==> t2``], ``t1 ==> t2``) : term list * term \end{verbatim} \end{session} A sort of dual to \ml{ASSUME} is the primitive inference rule \ml{DISCH} (discharging, assumption elimination) which infers from a theorem of the form $\cdots t_1\cdots\ml{\ |-\ }t_2$ the new theorem $\cdots\ \cdots\ \ml{|-}\ t_1\ml{==>}t_2$. \ml{DISCH} takes as arguments the term to be discharged (\ie\ $t_1$) and the theorem from whose assumptions it is to be discharged and returns the result of the discharging. The following session illustrates this: \begin{session} \begin{verbatim} - val Th4 = DISCH ``t1==>t2`` Th3; > val Th4 = |- (t1 ==> t2) ==> t1 ==> t2 : thm \end{verbatim} \end{session} Note that the term being discharged need not be in the assumptions; in this case they will be unchanged. \begin{session} \begin{verbatim} - DISCH ``1=2`` Th3; > val it = [.] |- (1 = 2) ==> t1 ==> t2 : thm - dest_thm it; > val it = ([``t1 ==> t2``], ``(1 = 2) ==> t1 ==> t2``) : term list * term \end{verbatim} \end{session} In \HOL\, the rule \ml{MP} of Modus Ponens is specified in conventional notation by: \[ \frac{\Gamma_1 \turn t_1 \imp t_2 \qquad\qquad \Gamma_2\turn t_1} {\Gamma_1 \cup \Gamma_2 \turn t_2} \] The \ML{} function \ml{MP} takes argument theorems of the form \ml{$\cdots\ $|-$\ t_1$\ ==>\ $t_2$} and \ml{$\cdots\ $|-$\ t_1$} and returns \ml{$\cdots\ $|-$\ t_2$}. The next session illustrates the use of \ml{MP} and also a common error, namely not supplying the \HOL\ logic type checker with enough information. \begin{session} \begin{verbatim} - val Th5 = ASSUME ``t1``; <> ! Uncaught exception: ! HOL_ERR - val Th5 = ASSUME ``t1`` handle e => Raise e; <> Exception raised at Thm.ASSUME: not a proposition ! Uncaught exception: ! HOL_ERR - val Th5 = ASSUME ``t1:bool``; > val Th5 = [.] |- t1 : thm - val Th6 = MP Th3 Th5; > val Th6 = [..] |- t2 : thm \end{verbatim} \end{session} The hypotheses of \ml{Th6} can be inspected with the \ML{} function \ml{hyp}, which returns the list of assumptions of a theorem (the conclusion is returned by \ml{concl}). \begin{session} \begin{verbatim} - hyp Th6; > val it = [``t1 ==> t2``, ``t1``] : term list \end{verbatim} \end{session} \HOL{} can be made to print out hypotheses of theorems explicitly by setting the global flag \ml{show\_assums} to true. \begin{session} \begin{verbatim} - show_assums := true; > val it = () : unit - Th5; > val it = [t1] |- t1 : thm - Th6; > val it = [t1 ==> t2, t1] |- t2 : thm \end{verbatim} \end{session} \noindent Discharging \ml{Th6} twice establishes the theorem \ml{|-\ t1 ==> (t1==>t2) ==> t2}. \begin{session} \begin{verbatim} - val Th7 = DISCH ``t1==>t2`` Th6; > val Th7 = [t1] |- (t1 ==> t2) ==> t2 : thm - val Th8 = DISCH ``t1:bool`` Th7; > val Th8 = |- t1 ==> (t1 ==> t2) ==> t2 : thm \end{verbatim} \end{session} The 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}. In standard logical notation this proof could be written: \begin{proofenumerate} \item $ t_1\imp t_2\turn t_1\imp t_2$ \hfill [Assumption introduction] \item $ t_1\turn t_1$ \hfill [Assumption introduction] \item $ t_1\imp t_2,\ t_1 \turn t_2 $ \hfill [Modus Ponens applied to lines 1 and 2] \item $ t_1 \turn (t_1\imp t_2)\imp t_2$ \hfill [Discharging the first assumption of line 3] \item $ \turn t_1 \imp (t_1 \imp t_2) \imp t_2$ \hfill [Discharging the only assumption of line 4] \end{proofenumerate} \subsection{Derived rules} A \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. For example, a proof of $\Gamma,\ t'\turn t$ from the hypothesis $\Gamma\turn t$ is: \begin{proofenumerate} \item $ t'\turn t'$ \hfill [Assumption introduction] \item $ \Gamma\turn t$ \hfill [Hypothesis] \item $ \Gamma\turn t'\imp t$ \hfill [Discharge $t'$ from line 2] \item $ \Gamma,\ t'\turn t$ \hfill [Modus Ponens applied to lines 3 and 1] \end{proofenumerate} \noindent This proof works for any hypothesis of the form $\Gamma\turn t$ and any boolean term $t'$ and shows that the result of adding an arbitrary hypothesis to a theorem is another theorem (because the four lines above can be added to any proof of $\Gamma\turn t$ to get a proof of $\Gamma,\ t'\turn t$).\footnote{This property of the logic is called {\it monotonicity}.} For example, the next session uses this proof to add the hypothesis \ml{``t3``} to \ml{Th6}. \begin{session} \begin{verbatim} - val Th9 = ASSUME ``t3:bool``; > val Th9 = [t3] |- t3 : thm - val Th10 = DISCH ``t3:bool`` Th6; > val Th10 = [t1 ==> t2, t1] |- t3 ==> t2 : thm - val Th11 = MP Th10 Th9; > val Th11 = [t1 ==> t2, t1, t3] |- t2 : thm \end{verbatim} \end{session} A {\it derived rule\/} is an \ML{} procedure that generates a proof from given hypotheses each time it is invoked. The hypotheses are the arguments of the rule. To illustrate this, a rule, called \ml{ADD\_ASSUM}, will now be defined as an \ML{} procedure that carries out the proof above. In standard notation this would be described by: \[ \frac{\Gamma\turn t}{\Gamma,\ t'\turn t} \] \noindent The \ML{} definition is: \begin{session} \begin{verbatim} - fun ADD_ASSUM t th = let val th9 = ASSUME t val th10 = DISCH t th in MP th10 th9 end; > val ADD_ASSUM = fn : term -> thm -> thm - ADD_ASSUM ``t3:bool`` Th6; > val it = [t1, t1 ==> t2, t3] |- t2 : thm \end{verbatim} \end{session} \noindent The body of \ml{ADD\_ASSUM} has been coded to mirror the proof done in session~10 above, so as to show how an interactive proof can be generalized into a procedure. But \ml{ADD\_ASSUM} can be written much more concisely as: \begin{session} \begin{verbatim} - fun ADD_ASSUM t th = MP (DISCH t th) (ASSUME t); > val ADD_ASSUM = fn : term -> thm -> thm - ADD_ASSUM ``t3:bool`` Th6; val it = [t1 ==> t2, t1, t3] |- t2 : thm \end{verbatim} \end{session} Another example of a derived inference rule is \ml{UNDISCH}; this moves the antecedent of an implication to the assumptions. \[ \frac{\Gamma\turn t_1\imp t_2}{\Gamma,\ t_1\turn t_2} \] An \ML{} derived rule that implements this is: \begin{session} \begin{verbatim} - fun UNDISCH th = MP th (ASSUME(#1(dest_imp(concl th)))); > val UNDISCH = fn : thm -> thm - Th10; > val it = [t1 ==> t2, t1] |- t3 ==> t2 : thm - UNDISCH Th10; > val it = [t1, t1 ==> t2, t3] |- t2 : thm \end{verbatim} \end{session} \noindent Each time \ml{UNDISCH\ $\Gamma\turn t_1\imp t_2$} is executed, the following proof is performed: \begin{proofenumerate} \item $ t_1\turn t_1$ \hfill [Assumption introduction] \item $ \Gamma\turn t_1\imp t_2$ \hfill [Hypothesis] \item $ \Gamma,\ t_1\turn t_2$ \hfill [Modus Ponens applied to lines 2 and 1] \end{proofenumerate} The rules \ml{ADD\_ASSUM} and \ml{UNDISCH} are the first derived rules defined when the \HOL{} system is built. For a description of the main rules see the section on derived rules in \DESCRIPTION. \subsubsection{Rewriting} An interesting derived rule is \ml{REWRITE\_RULE}. This takes a list of equational theorems of the form: \[ \Gamma\turn (u_1 = v_1) \conj (u_2 = v_2) \conj \ldots\ \conj (u_n = v_n) \] and 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. The result is a theorem $\Gamma\cup\Delta\turn t'$ where $t'$ is the result of rewriting $t$ in this way. The session below illustrates the use of \ml{REWRITE\_RULE}. In it the list of equations is the value \ml{rewrite\_list} containing the pre-proved theorems \ml{ADD\_CLAUSES} and \ml{MULT\_CLAUSES}. These 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. (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.) \begin{session} \begin{verbatim} - open arithmeticTheory; ... - val rewrite_list = [ADD_CLAUSES,MULT_CLAUSES]; > val rewrite_list = [ |- (0 + m = m) /\ (m + 0 = m) /\ (SUC m + n = SUC (m + n)) /\ (m + SUC n = SUC (m + n)), |- !m n. (0 * m = 0) /\ (m * 0 = 0) /\ (1 * m = m) /\ (m * 1 = m) /\ (SUC m * n = m * n + n) /\ (m * SUC n = m + m * n)] : thm list \end{verbatim} \end{session} \begin{session} \begin{verbatim} - REWRITE_RULE rewrite_list (ASSUME ``(m+0)<(1*n)+(SUC 0)``); > val it = [m + 0 < 1 * n + SUC 0] |- m < SUC n : thm \end{verbatim} \end{session} \noindent This can then be rewritten using another pre-proved theorem \ml{LESS\_THM}, this one from the theory \ml{prim\_rec}: \begin{session} \begin{verbatim} - REWRITE_RULE [prim_recTheory.LESS_THM] it; > val it = [m + 0 < 1 * n + SUC 0] |- (m = n) \/ m < n : thm \end{verbatim} \end{session} \ml{REWRITE\_RULE} is not a primitive in \HOL, but is a derived rule. It is inherited from Cambridge \LCF\ and was implemented by Larry Paulson (see his paper \cite{lcp-rewrite} for details). In addition to the supplied equations, \ml{REWRITE\_RULE} has some built in standard simplifications: \begin{session} \begin{verbatim} - REWRITE_RULE [] (ASSUME ``(T /\ x) \/ F ==> F``); > val it = [T /\ x \/ F ==> F] |- ~x : thm \end{verbatim} \end{session} There 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. \section{Goal Oriented Proof: Tactics and Tacticals} \label{backward}\label{tactics} The style of forward proof described in the previous section is unnatural and too `low level' for many applications. An important advance in proof generating methodology was made by Robin Milner in the early 1970s when he invented the notion of {\it tactics\/}. A tactic is a function that does two things. \begin{myenumerate} \item Splits a `goal' into `subgoals'. \item Keeps track of the reason why solving the subgoals will solve the goal. \end{myenumerate} \noindent Consider, for example, the rule of $\wedge$-introduction\footnote{In higher order logic this is a derived rule; in first order logic it is usually primitive. In HOL the rule is called {\tt CONJ} and its derivation is given in \DESCRIPTION.} shown below: \[ \frac{\Gamma_1\turn t_1\qquad\qquad\qquad\Gamma_2\turn t_2}{\Gamma_1\cup\Gamma_2 \turn t_1\conj t_2} \] \noindent In \HOL, $\wedge$-introduction is represented by the \ML{} function \ml{CONJ}: \[\ml{CONJ}\ (\Gamma_1\turn t_1)\ (\Gamma_2\turn t_2) \ \ \leadsto\ \ (\Gamma_1\cup\Gamma_2\turn t_1\conj t_2)\] \noindent This is illustrated in the following new session (note that the session number has been reset to {\small\sl 1}: \setcounter{sessioncount}{0} \begin{session} \begin{verbatim} - show_assums := true; val it = () : unit - val Th1 = ASSUME ``A:bool`` and Th2 = ASSUME ``B:bool``; > val Th1 = [A] |- A : thm val Th2 = [B] |- B : thm - val Th3 = CONJ Th1 Th2; > val Th3 = [A, B] |- A /\ B : thm \end{verbatim} \end{session} Suppose the goal is to prove $A\conj B$, then this rule says that it is sufficient to prove the two subgoals $A$ and $B$, because from $\turn A$ and $\turn B$ the theorem $\turn A\conj B$ can be deduced. Thus: \begin{myenumerate} \item To prove $\turn A \conj B$ it is sufficient to prove $\turn A$ and $\turn B$. \item The justification for the reduction of the goal $\turn A \conj B$ to the two subgoals $\turn A$ and $\turn B$ is the rule of $\wedge$-introduction. \end{myenumerate} A \emph{goal} in \HOL{} is a pair \ml{([$t_1$,\ldots,$t_n$],$t$)} of \ML{} type \ml{term list~*~term}. An \emph{achievement} of such a goal is a theorem \ml{$t_1$,$\ldots$,$t_n$\ |-\ $t$}. A 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. If $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 $g$ (\ie\ evaluating the \ML{} expression $T\ g$) will result in an object which is a pair whose first component is a list of goals and whose second component is a justification function, \ie\ a value with \ML{} type {\small\verb|thm list -> thm|}. An example tactic is \ml{CONJ\_TAC} which implements (i) and (ii) above. For example, consider the utterly trivial goal of showing \holtxt{T~/\bs{}~T}, where \ml{T} is a constant that stands for $\top$ (truth): \begin{session} \begin{verbatim} - val goal1 = ([]:term list, ``T /\ T``); > val goal1 = ([], ``T /\ T``) : term list * term - CONJ_TAC goal1; > val it = ([([], ``T``), ([], ``T``)], fn) : (term list * term) list * (thm list -> thm) - val (goal_list,just_fn) = it; > val goal_list = [([], ``T``), ([], ``T``)] : (term list * term) list val just_fn = fn : thm list -> thm \end{verbatim} \end{session} \noindent \ml{CONJ\_TAC} has produced a goal list consisting of two identical subgoals of just showing \ml{([],"T")}. Now, there is a preproved theorem in \HOL, called \ml{TRUTH}, that achieves this goal: \begin{session} \begin{verbatim} - TRUTH; > val it = [] |- T : thm \end{verbatim} \end{session} \noindent Applying the justification function \ml{just\_fn} to a list of theorems achieving the goals in \ml{goal\_list} results in a theorem achieving the original goal: \begin{session} \begin{verbatim} - just_fn [TRUTH,TRUTH]; > val it = [] |- T /\ T : thm \end{verbatim} \end{session} Although this example is trivial, it does illustrate the essential idea of tactics. Note that tactics are not special theorem-proving primitives; they are just \ML{} functions. For example, the definition of \ml{CONJ\_TAC} is simply: \begin{hol} \begin{verbatim} fun CONJ_TAC (asl,w) = let val (l,r) = dest_conj w in ([(asl,l), (asl,r)], fn [th1,th2] => CONJ th1 th2) end \end{verbatim} \end{hol} \noindent The function \ml{dest\_conj} splits a conjunction into its two conjuncts: If \ml{(asl,``$t_1$}{\small\verb|/\|}\ml{$t_2$``)} is a goal, then \ml{CONJ\_TAC} splits it into the list of two subgoals \ml{(asl,$t_1$)} and \ml{(asl,$t_2$)}. The justification function, {\small\verb|fn [th1,th2] => CONJ th1 th2|} takes a list \ml{[$th_1$,$th_2$]} of theorems and applies the rule \ml{CONJ} to $th_1$ and $th_2$. To summarize: if $T$ is a tactic and $g$ is a goal, then applying $T$ to $g$ will result in a pair whose first component is a list of goals and whose second component is a justification function, with \ML{} type {\small\verb|thm list -> thm|}. Suppose $T\ g${\small\verb| = ([|}$g_1${\small\verb|,|}$\ldots${\small\verb|,|}$g_n${\small\verb|],|}$p${\small\verb|)|}. The idea is that $g_1$ , $\ldots$ , $g_n$ are subgoals and $p$ is a `justification' of the reduction of goal $g$ to subgoals $g_1$ , $\ldots$ , $g_n$. Suppose further that the subgoals $g_1$ , $\ldots$ , $g_n$ have been solved. This would mean that theorems $th_1$ , $\ldots$ , $th_n$ had been proved such that each $th_i$ ($1\leq i\leq n$) `achieves' the goal $g_i$. The justification $p$ (produced by applying $T$ to $g$) is an \ML{} function which when applied to the list {\small\verb|[|}$th_1${\small\verb|,|}$\ldots${\small\verb|,|}$th_n${\small\verb|]|} returns a theorem, $th$, which `achieves' the original goal $g$. Thus $p$ is a function for converting a solution of the subgoals to a solution of the original goal. If $p$ does this successfully, then the tactic $T$ is called {\it valid\/}. Invalid tactics cannot result in the proof of invalid theorems; the worst they can do is result in insolvable goals or unintended theorems being proved. If $T$ were invalid and were used to reduce goal $g$ to subgoals $g_1$ , $\ldots$ , $g_n$, then effort might be spent proving theorems $th_1$ , $\ldots$ , $th_n$ to achieve the subgoals $g_1$ , $\ldots$ , $g_n$, only to find out after the work is done that this is a blind alley because $p${\small\verb|[|}$th_1${\small\verb|,|}$\ldots${\small\verb|,|}$th_n${\small\verb|]|} doesn't achieve $g$ (\ie\ it fails, or else it achieves some other goal). A theorem {\it achieves\/} a goal if the assumptions of the theorem are included in the assumptions of the goal {\it and\/} if the conclusion of the theorems is equal (up to the renaming of bound variables) to the conclusion of the goal. More precisely, a theorem \begin{center} $t_1$, $\dots$, $t_m${\small\verb% |- %}$t$ \end{center} \noindent achieves a goal \begin{center} {\small\verb|([|}$u_1${\small\verb|,|}$\ldots${\small\verb|,|}$u_n${\small\verb|],|}$u${\small\verb|)|} \end{center} \noindent if and only if $\{t_1,\ldots,t_m\}$ is a subset of $\{u_1,\ldots,u_n\}$ and $t$ is equal to $u$ (up to renaming of bound variables). For example, the goal {\small\verb|([``x=y``, ``y=z``, ``z=w``], ``x=z``)|} is achieved by the theorem {\small\verb+[x=y, y=z] |- x=z+} (the assumption {\small\verb|``z=w``|} is not needed). A tactic {\it solves\/} a goal if it reduces the goal to the empty list of subgoals. Thus $T$ solves $g$ if $T\ g${\small\verb| = ([],|}$p${\small\verb|)|}. If this is the case and if $T$ is valid, then $p${\small\verb|[]|} will evaluate to a theorem achieving $g$. Thus if $T$ solves $g$ then the \ML{} expression {\small\verb|snd(|}$T\ g${\small\verb|)[]|} evaluates to a theorem achieving $g$. Tactics are specified using the following notation: \begin{center} \begin{tabular}{c} \\ $goal$ \\ \tacticline $goal_1\ \ \ goal_2 \ \ \ \cdots\ \ \ goal_n$ \\ \end{tabular} \end{center} \noindent For example, a tactic called {\small\verb|CONJ_TAC|} is described by \newcommand\ttbs{\texttt{\symbol{"5C}}} \newcommand\ttland{\texttt{/\ttbs}} \begin{center} \begin{tabular}{lr} \\ \multicolumn{2}{c}{$t_1$ \ttland{} $t_2$} \\ \tacticline $t_1$ & $t_2$ \\ \end{tabular} \end{center} \noindent Thus {\small\verb|CONJ_TAC|} reduces a goal of the form {\small\verb|(|}$\Gamma${\small\verb|,``|}$t_1${\small\verb|/\|}$t_2${\small\verb|``)|} to subgoals {\small\verb|(|}$\Gamma${\small\verb|,``|}$t_1${\small\verb|``)|} and {\small\verb|(|}$\Gamma${\small\verb|,``|}$t_2${\small\verb|``)|}. The fact that the assumptions of the top-level goal are propagated unchanged to the two subgoals is indicated by the absence of assumptions in the notation. Another 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 doing mathematical induction on the natural numbers: \begin{center} \begin{tabular}{lr} \\ \multicolumn{2}{c}{\texttt{!}$n$\texttt{.}$t[n]$} \\ \tacticline $t[\texttt{0}]$ & $\quad\{t[n]\}\ t[\texttt{SUC}\;n]$ \end{tabular} \end{center} {\small\verb|INDUCT_TAC|} reduces a goal {\small\verb|(|}$\Gamma${\small\verb|,``!|}$n${\small\verb|.|}$t[n]${\small\verb|``)|} to a basis subgoal {\small\verb|(|}$\Gamma${\small\verb|,``|}$t[${\small\verb|0|}$]${\small\verb|``)|} and an induction step subgoal {\small\verb|(|}$\Gamma\cup\{${\small\verb|``|}$t[n]${\small\verb|``|}$\}${\small\verb|,``|}$t[${\small\verb|SUC |}$n]${\small\verb|``)|}. The extra induction assumption {\small\verb|``|}$t[n]${\small\verb|``|} is indicated in the tactic notation with set brackets. \begin{session} \begin{verbatim} - numLib.INDUCT_TAC([], ``!m n. m+n = n+m``); > val it = ([([], ``!n. 0 + n = n + 0``), ([``!n. m + n = n + m``], ``!n. SUC m + n = n + SUC m``)], fn) : (term list * term) list * (thm list -> thm) \end{verbatim} \end{session} \noindent The first subgoal is the basis case and the second subgoal is the step case. Tactics generally fail (in the \ML{} sense, \ie\ raise an exception) if they are applied to inappropriate goals. For example, {\small\verb|CONJ_TAC|} will fail if it is applied to a goal whose conclusion is not a conjunction. Some tactics never fail, for example {\small\verb|ALL_TAC|} \begin{center} \begin{tabular}{c} \\ $t$ \\ \tacticline $t$ \end{tabular} \end{center} \noindent is the `identity tactic'; it reduces a goal {\small\verb|(|}$\Gamma${\small\verb|,|}$t${\small\verb|)|} to the single subgoal {\small\verb|(|}$\Gamma${\small\verb|,|}$t${\small\verb|)|}---\ie\ it has no effect. {\small\verb|ALL_TAC|} is useful for writing complex tactics using tacticals. \subsection{Using tactics to prove theorems} \label{using-tactics} Suppose goal $g$ is to be solved. If $g$ is simple it might be possible to immediately think up a tactic, $T$ say, which reduces it to the empty list of subgoals. If this is the case then executing: $\ ${\small\verb| val (|}$gl${\small\verb|,|}$p${\small\verb|) = |}$T\ g$ \noindent will bind $p$ to a function which when applied to the empty list of theorems yields a theorem $th$ achieving $g$. (The declaration above will also bind $gl$ to the empty list of goals.) Thus a theorem achieving $g$ can be computed by executing: $\ ${\small\verb| val |}$th${\small\verb| = |}$p${\small\verb|[]|} \noindent This will be illustrated using \ml{REWRITE\_TAC} which takes a list of equations (empty in the example that follows) and tries to prove a goal by rewriting with these equations together with \ml{basic\_rewrites}: \begin{session} \begin{verbatim} - val goal2 = ([]:term list, ``T /\ x ==> x \/ (y /\ F)``); > val goal2 = ([], ``T /\ x ==> x \/ y /\ F``) : (term list * term) - REWRITE_TAC [] goal2; > val it = ([], fn) : (term list * term) list * (thm list -> thm) - #2 it []; > val it = [] |- T /\ x ==> x \/ y /\ F : thm \end{verbatim} \end{session} \noindent Proved theorems are usually stored in the current theory so that they can be used in subsequent sessions. The built-in function \ml{store\_thm} of \ML{} type {\small\verb|(string * term * tactic) -> thm|} facilitates the use of tactics: {\small\verb|store_thm("foo",|}$t${\small\verb|,|}$T${\small\verb|)|} proves the goal {\small\verb|([],|}$t${\small\verb|)|} (\ie\ the goal with no assumptions and conclusion $t$) using tactic $T$ and saves the resulting theorem with name {\small\verb|foo|} on the current theory. If the theorem is not to be saved, the function \ml{prove} of type {\small\verb|(term * tactic) -> thm|} can be used. Evaluating {\small\verb|prove(|}$t${\small\verb|,|}$T${\small\verb|)|} proves the goal {\small\verb|([],|}$t${\small\verb|)|} using $T$ and returns the result without saving it. In both cases the evaluation fails if $T$ does not solve the goal {\small\verb|([],|}$t${\small\verb|)|}. When 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. While this is feasible even in large proofs, it is tedious. \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. Its use is demonstrated below in some of the example sessions, and in Chapter~\ref{chap:euclid}. It is thoroughly documented in \DESCRIPTION. (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.) \subsection{Tacticals} \label{tacticals} A {\it tactical\/} is an \ML{} function that takes one or more tactics as arguments, possibly with other arguments as well, and returns a tactic as its result. The various parameters passed to tacticals are reflected in the various \ML{} types that the built-in tacticals have. Some important tacticals in the \HOL{} system are listed below. \subsubsection{\tt THENL : tactic -> tactic list -> tactic} If 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$. The tactical \ml{THENL} is useful if one wants to do different things to different subgoals. \ml{THENL} can be illustrated by doing the proof of $\vdash \uquant{m}m+0=m$ in one step. \setcounter{sessioncount}{0} \begin{session} \begin{verbatim} - g `!m. m + 0 = m`; > val it = Proof manager status: 1 proof. 1. Incomplete: Initial goal: !m. m + 0 = m - e (INDUCT_TAC THENL [REWRITE_TAC[ADD], ASM_REWRITE_TAC[ADD]]); OK.. > val it = Initial goal proved. |- !m. m + 0 = m \end{verbatim} \end{session} \noindent The compound tactic \[ \ml{INDUCT\_TAC~THENL~[REWRITE\_TAC~[ADD],~ASM\_REWRITE\_TAC~[ADD]]} \] first 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). The tactical {\small\verb|THENL|} is useful for doing different things to different subgoals. The tactical \ml{THEN} can be used to apply the same tactic to all subgoals. \subsubsection{\tt THEN : tactic -> tactic -> tactic}\label{THEN} The tactical {\small\verb|THEN|} is an \ML{} infix. If $T_1$ and $T_2$ are tactics, then the \ML{} expression $T_1${\small\verb| THEN |}$T_2$ evaluates to a tactic which first applies $T_1$ and then applies $T_2$ to all the subgoals produced by $T_1$. In fact, \ml{ASM\_REWRITE\_TAC[ADD]} will solve the basis as well as the step case of the induction for $\uquant{m}m+0=m$, so there is an even simpler one-step proof than the one above: \setcounter{sessioncount}{0} \begin{session} \begin{verbatim} - g `!m. m+0 = m`; > val it = Proof manager status: 1 proof. 1. Incomplete: Initial goal: !m. m + 0 = m - e(INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]); OK.. > val it = Initial goal proved. |- !m. m + 0 = m \end{verbatim} \end{session} \noindent This is typical: it is common to use a single tactic for several goals. Here, for example, are the first four consequences of the definition \ml{ADD} of addition that are pre-proved when the built-in theory \ml{arithmetic} \HOL{} is made. \begin{hol} \begin{verbatim} val ADD_0 = prove ( ``!m. m + 0 = m``, INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]); \end{verbatim} \end{hol} \begin{hol} \begin{verbatim} val ADD_SUC = prove ( ``!m n. SUC(m + n) = m + SUC n``, INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]); \end{verbatim} \end{hol} \begin{hol} \begin{verbatim} val ADD_CLAUSES = prove ( ``(0 + m = m) /\ (m + 0 = m) /\ (SUC m + n = SUC(m + n)) /\ (m + SUC n = SUC(m + n))``, REWRITE_TAC[ADD, ADD_0, ADD_SUC]); \end{verbatim} \end{hol} \begin{hol} \begin{verbatim} val ADD_COMM = prove ( ``!m n. m + n = n + m``, INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_0, ADD, ADD_SUC]); \end{verbatim} \end{hol} \noindent These proofs are performed when the \HOL{} system is made and the theorems are saved in the theory \ml{arithmetic}. The complete list of proofs for this built-in theory can be found in the file \ml{src/num/theories/arithmeticScript.sml}. \subsubsection{\tt ORELSE : tactic -> tactic -> tactic}\label{ORELSE} The tactical {\small\verb|ORELSE|} is an \ML{} infix. If $T_1$ and $T_2$ are tactics, %\index{tacticals!for alternation} then $T_1${\small\verb| ORELSE |}$T_2$ evaluates to a tactic which applies $T_1$ unless that fails; if it fails, it applies $T_2$. \ml{ORELSE} is defined in \ML{} as a curried infix by\footnote{This is a minor simplification.} \begin{hol} {\small\verb|(|}$T_1${\small\verb| ORELSE |}$T_2${\small\verb|)|} $g$ {\small\verb|=|} $T_1\; g$ {\small\verb|handle _ =>|} $T_2\; g$ \end{hol} %\index{alternation!of tactics|)} \subsubsection{\tt REPEAT : tactic -> tactic} If $T$ is a tactic then {\small\verb|REPEAT |}$T$ is a tactic which repeatedly applies $T$ until it fails. This can be illustrated in conjunction with \ml{GEN\_TAC}, which is specified by: \begin{center} \begin{tabular}{c} \\ {\small\verb|!|}$x${\small\verb|.|}$t[x]$ \\ \tacticline $t[x']$ \\ \end{tabular} \end{center} \begin{itemize} \item Where $x'$ is a variant of $x$ not free in the goal or the assumptions. \end{itemize} \noindent \ml{GEN\_TAC} strips off one quantifier; \ml{REPEAT\ GEN\_TAC} strips off all quantifiers: \begin{session} \begin{verbatim} - g `!x y z. x+(y+z) = (x+y)+z`; > val it = Proof manager status: 1 proof. 1. Incomplete: Initial goal: !x y z. x + (y + z) = x + y + z - e GEN_TAC; OK.. 1 subgoal: > val it = !y z. x + (y + z) = x + y + z - e (REPEAT GEN_TAC); OK.. 1 subgoal: > val it = x + (y + z) = x + y + z \end{verbatim} \end{session} \subsection{Some tactics built into \HOL{}} This section contains a summary of some of the tactics built into the \HOL{} system (including those already discussed). The tactics given here are those that are used in the parity checking example. \subsubsection{\tt REWRITE\_TAC : thm list -> tactic} \label{rewrite} \begin{itemize} \item{\bf Summary:} {\small\verb|REWRITE_TAC[|}$th_1${\small\verb|,|}$\ldots${\small\verb|,|}$th_n${\small\verb|]|} simplifies the goal by rewriting it with the explicitly given theorems $th_1$, $\ldots$ , $th_n$, and various built-in rewriting rules. \begin{center} \begin{tabular}{c} \\ $\{t_1, \ldots , t_m\}t$ \\ \tacticline $\{t_1, \ldots , t_m\}t'$ \\ \end{tabular} \end{center} \noindent where $t'$ is obtained from $t$ by rewriting with \begin{enumerate} \item $th_1$, $\ldots$ , $th_n$ and \item the standard rewrites held in the \ML{} variable {\small\verb|basic_rewrites|}. \end{enumerate} \item{\bf Uses:} Simplifying goals using previously proved theorems. \item{\bf Other rewriting tactics}: \begin{enumerate} \item {\small\verb|ASM_REWRITE_TAC|} adds the assumptions of the goal to the list of theorems used for rewriting. \item {\small\verb|PURE_REWRITE_TAC|} uses neither the assumptions nor the built-in rewrites. \item {\small\verb|RW_TAC|} of type \ml{simpLib.simpset -> thm list -> tactic}. A \ml{simpset} is a special collection of rewriting theorems and other theorem-proving functionality. Values defined by \HOL{} include \ml{bossLib.std\_ss}, which has basic knowledge of the boolean connectives, \ml{bossLib.arith\_ss} which ``knows'' all about arithmetic, and \ml{HOLSimps.list\_ss}, which includes theorems appropriate for lists, pairs, and arithmetic. Additional theorems for rewriting can be added using the second argument of \ml{RW\_TAC}. \end{enumerate} \end{itemize} \subsubsection{\tt CONJ\_TAC : tactic}\label{CONJTAC} \begin{itemize} \item{\bf Summary:} Splits a goal {\small\verb|``|}$t_1${\small\verb|/\|}$t_2${\small\verb|``|} into two subgoals {\small\verb|``|}$t_1${\small\verb|``|} and {\small\verb|``|}$t_2${\small\verb|``|}. \begin{center} \begin{tabular}{lr} \\ \multicolumn{2}{c}{$t_1$ \ttland{} $t_2$} \\ \tacticline $t_1$ & $t_2$ \\ \end{tabular} \end{center} \item{\bf Uses:} Solving conjunctive goals. \ml{CONJ_TAC} is invoked by \ml{STRIP_TAC} (see below). \end{itemize} \subsubsection{\tt EQ\_TAC : tactic}\label{EQTAC} \begin{itemize} \item{\bf Summary:} \ml{EQ_TAC} splits an equational goal into two implications (the `if-case' and the `only-if' case): \begin{center} \begin{tabular}{lr} \\ \multicolumn{2}{c}{$u\; \ml{=}\; v$} \\ \tacticline $u\; \ml{==>}\; v$ & $\quad v\; \ml{==>}\; u$ \\ \end{tabular} \end{center} \item{\bf Use:} Proving logical equivalences, \ie\ goals of the form ``$u$\ml{=}$v$'' where $u$ and $v$ are boolean terms. \end{itemize} \subsubsection{\tt DISCH\_TAC : tactic}\label{DISCHTAC} \begin{itemize} \item{\bf Summary:} Moves the antecedent of an implicative goal into the assumptions. \begin{center} \begin{tabular}{c} \\ $u${\small\verb| ==> |}$v$ \\ \tacticline $\{u\}v$ \\ \end{tabular} \end{center} \item{\bf Uses:} Solving goals of the form \holtxt{$u$~==>~$v$} by assuming \holtxt{$u$} and then solving \holtxt{$v$}. {\small\verb|STRIP_TAC|} (see below) will invoke {\small\verb|DISCH_TAC|} on implicative goals. \end{itemize} \subsubsection{\tt GEN\_TAC : tactic} \begin{itemize} \item{\bf Summary:} Strips off one universal quantifier. \begin{center} \begin{tabular}{c} \\ {\small\verb|!|}$x${\small\verb|.|}$t[x]$ \\ \tacticline $t[x']$ \\ \end{tabular} \end{center} \noindent Where $x'$ is a variant of $x$ not free in the goal or the assumptions. \item{\bf Uses:} Solving universally quantified goals. {\small\verb|REPEAT GEN_TAC|} strips off all universal quantifiers and is often the first thing one does in a proof. {\small\verb|STRIP_TAC|} (see below) applies {\small\verb|GEN_TAC|} to universally quantified goals. \end{itemize} \subsubsection{\tt PROVE\_TAC : thm list -> tactic} \begin{itemize} \item {\bf Summary:} Used to do first order reasoning, solving the goal completely if successful, failing otherwise. Using the provided theorems and the assumptions of the goal, {\small\verb|PROVE_TAC|} does a search for possible proofs of the goal. Eventually fails if the search fails to find a proof shorter than a reasonable depth. \item {\bf Uses:} To finish a goal off when it is clear that it is a consequence of the assumptions and the provided theorems. \end{itemize} \subsubsection{\tt STRIP\_TAC : tactic} \begin{itemize} \item{\bf Summary:} Breaks a goal apart. {\small\verb|STRIP_TAC|} removes one outer connective from the goal, using {\small\verb|CONJ_TAC|}, {\small\verb|DISCH_TAC|}, {\small\verb|GEN_TAC|}, \etc\ If the goal is $t_1${\small\verb|/\|}$\cdots${\small\verb|/\|}$t_n${\small\verb| ==> |}$t$ then {\small\verb|STRIP_TAC|} makes each $t_i$ into a separate assumption. \item{\bf Uses:} Useful for splitting a goal up into manageable pieces. Often the best thing to do first is {\small\verb|REPEAT STRIP_TAC|}. \end{itemize} \subsubsection{\tt ACCEPT\_TAC : thm -> tactic}\label{ACCEPTTAC} \begin{itemize} \item{\bf Summary:} {\small\verb|ACCEPT_TAC |}$th$ is a tactic that solves any goal that is achieved by $th$. \item{\bf Use:} Incorporating forward proofs, or theorems already proved, into goal directed proofs. For example, one might reduce a goal $g$ to subgoals $g_1$, $\dots$, $g_n$ using a tactic $T$ and then prove theorems $th_1$ , $\dots$, $th_n$ respectively achieving these goals by forward proof. The tactic \[\ml{ T THENL[ACCEPT\_TAC }th_1\ml{,}\ldots\ml{,ACCEPT\_TAC }th_n\ml{]} \] would then solve $g$, where \ml{THENL} %\index{THENL@\ml{THENL}} is the tactical that applies the respective elements of the tactic list to the subgoals produced by \ml{T}. \end{itemize} \subsubsection{\tt ALL\_TAC : tactic} \begin{itemize} \item{\bf Summary:} Identity tactic for the tactical {\small\verb%THEN%} (see \DESCRIPTION). \item{\bf Uses:} \begin{enumerate} \item Writing tacticals (see description of {\small\verb|REPEAT|} in \DESCRIPTION). \item With {\small\verb%THENL%}; for example, if tactic $T$ produces two subgoals and we want to apply $T_1$ to the first one but to do nothing to the second, then the tactic to use is \ml{$T$~THENL[$T_1$,ALL_TAC]}. \end{enumerate} \end{itemize} \subsubsection{\tt NO\_TAC : tactic} \begin{itemize} \item{\bf Summary:} Tactic that always fails. \item{\bf Uses:} Writing tacticals. \end{itemize} %%% Local Variables: %%% mode: latex %%% TeX-master: "tutorial" %%% End: