\documentclass[twocolumn,fleqn,layout]{article} \usepackage{alltt} \pagestyle{plain} \flushbottom \sloppy \begin{document} \input{macros} \sloppy \twocolumn[{\scriptsize \parbox{100mm}{Preprint of a paper to appear in the Proceedings of the 1991 International Tutorial and Workshop on the HOL Theorem Proving System, 27--30 August 1991, Davis California (IEEE Computer Society Press).}}\vskip10mm \begin{center} {\Large\bf A Package for Inductive Relation Definitions in HOL}\\ \vskip24pt T.\ F.\ Melham\\ \vskip12pt University of Cambridge Computer Laboratory\\ New Museums Site, Pembroke Street\\ Cambridge, CB2 3QG, England.\\ \mbox{}\\ \vskip3mm \end{center}] \subsection*{\centering Abstract} {\it\sloppy This paper describes a set of theorem proving tools based on a new derived principle of definition in HOL, namely the introduction of relations inductively defined by a set of rules. Such inductive definitions abound in computer science. Example application areas \mbox{include} reasoning about structured operational semantics, type judgements, transition relations for process algebras, \mbox{reduction} relations, and compositional proof systems. The package described in this paper automates the derivation of certain inductive definitions involved in these applications and provides the basic tools needed for reasoning about the relations introduced by them.} \vskip12pt \section{Introduction} The HOL user community has a strong tradition of taking a purely {\it definitional\/} approach to using higher order logic. That is, the syntax of the logic is extended with new notation not simply by postulating axioms to give meaning to it, but rather by defining it in terms of existing expressions of the logic that already have the required semantics. The advantage of this approach, as opposed to the axiomatic method, is that each of the primitive rules of definition in the {\small HOL} logic---namely, constant definition, constant specification, and type definition---is guaranteed to preserve consistency. The disadvantage is that these rules admit only \mbox{definitions} that satisfy certain very restrictive rules of formation. Definitions expressed in any other form must always be justified formally by deriving them from equivalent, but possibly rather complex, primitive definitions. The {\small ML} metalanguage allows users to implement derived inference rules in the {\small HOL} system and thus provides a facility for automating proofs that justify derived rules of definition. For example, recursive \mbox{definitions} are not admitted by the primitive rules of definition of the {\small HOL} logic. But certain recursive type definitions and function definitions are supported in the system by derived inference rules written in {\small ML}~\cite{description,melham}. The details of the primitive definitions that underlie these rules are hidden from the user, and their {\small ML} implementations are highly optimized. So these \mbox{derived} principles of definition may simply be regarded as primitive by most users of the system. This paper describes a set of theorem-proving tools based on a new derived principle of definition in {\small HOL} for defining relations inductively by a set of rules. \mbox{Sections~\ref{ind-defs}} and~\ref{in-logic} give a general introduction to the class of inductive definitions handled by the package and explain the logical basis for these definitions. The remaining sections describe the {\small ML} functions provided by the package and briefly mention some applications for which the package can be used. \section{Inductive definitions}\label{ind-defs} The following is a simple but typical example of a relation defined inductively by a set of rules. (This example is taken from~\cite{pitts}.) Let $R \subseteq A \times A$ be a binary relation on a set $A$. The reflexive-transitive closure of $R$ can be defined to be the least relation $R^{*} \subseteq A \times A$ for which the following deduction rules hold. \medskip \[ \begin{array}[t]{@{}l} \hbox{{\small\bf R}\bf 1}\quad\Rule{}{R^{*}(x,y)}\;\; R(x,y) \\[6mm] \hbox{{\small\bf R}\bf 2}\quad\Rule{}{R^{*}(x,x)}\\[8mm] \hbox{{\small\bf R}\bf 3}\quad\Rule{R^{*}(x,z)\qquad R^{*}(z,y)} {R^{*}(x,y)} \end{array} \] \medskip \noindent These rules state precisely the properties required of the reflexive-transitive closure of the relation $R$. Rule {{\small\bf R}\bf 1} states that it must contain at least all the values in $R$; rule {{\small\bf R}\bf 2} states that it must be reflexive; and rule {{\small\bf R}\bf 3} states that it must be transitive. The reflexive-transitive closure $R^{*}$ may therefore simply be {\it defined\/} to be the least relation that satisfies these conditions. It then follows simply by definition that the rules {{\small\bf R}\bf 1}, {{\small\bf R}\bf 2} and {{\small\bf R}\bf 3} are in fact satisfied by $R^{*}$. Moreover, it follows immediately that $R^{*}$ is a subset of any other relation that satisfies these rules, since $R^{*}$ is defined to be the {\it least\/} such relation. This means that $R^{*}$ contains only those pairs of values that it must contain by virtue of satisfying the rules. As will be discussed below, this property gives rise to an induction principle for reasoning about the relation $R^{*}$. The definition given above is valid because the rules {{\small\bf R}\bf 1}, {{\small\bf R}\bf 2}, and {{\small\bf R}\bf 3} make only positive statements about the elements of $R^{*}$. This guarantees that the least relation satisfying these rules does exist. In particular, if the rules have this form, then one can show that the intersection of any set of relations that satisfy the rules also satisfies the rules. Moreover, at least one binary relation satisfies the rules, namely the maximal relation $A \times A$. The `least' or smallest relation that satisfies the rules may therefore legitimately be defined to be the intersection of all such relations. In general, an inductive definition of an $n$-place \mbox{relation} $R$ consists of a set of rules of the form: \smallskip \[ \Rule{R(t_1^1,\dots,t_n^1) \quad \cdots \quad R(t_1^i,\dots,t_n^i)} {R(t_1,\dots,t_n)}\;\;C_1\:\cdots\:C_j \] \smallskip \noindent The terms above the line are the {\it premisses\/} of the rule, each of which makes a positive assertion of membership in the relation $R$. The term below the line, called the {\it conclusion\/} of the rule, likewise asserts membership in $R$. The terms $C_1$,\dots,$C_j$ are {\it side conditions\/} on the rule; these may be arbitrary propositions not involving the relation $R$ being defined. A relation $R$ is {\it closed\/} under such a rule if whenever the premisses and side conditions hold, the conclusion also holds. The relation {\it inductively defined\/} by a collection of such rules is the least relation closed under all the rules. \subsection{Rule induction}\label{rule-ind} By virtue of its definition as the {\it least\/} relation closed under a set of rules, every inductively defined relation comes with an associated induction principle. This principle of {\it rule induction\/} is essential for many proofs involving such relations. (The term `rule induction' was coined by Glynn Winskel in~\cite{winskel}). The principle of rule induction for an inductively defined relation may be stated briefly as follows. Let $R$ be an $n$-place relation inductively defined by a set of rules, and suppose we wish to show that every element in $R$ has a certain property $P$: {\samepage \begin{equation}\label{fact1} \hbox{\rm if}\;\;R(x_1,\dots,x_n)\;\;\hbox{then}\;\;P[x_1,\dots,x_n] \end{equation} \noindent Since $R$ is} \pagebreak[3] the least relation closed under the rules, any relation $S$ which is also closed under the rules has the property that $R \subseteq S$. Now, let \[S = \{(x_1,\dots,x_n) \mid P[x_1,\dots,x_n]\}\] \noindent Then to prove the desired property of $R$, it suffices to show that the relation $S$ is closed under the rules that define $R$. For if the relation $S$ in fact is closed under the rules, then we have that $R \subseteq S$ and therefore that every element of $R$ has the defining property of $S$---i.e.\ statement~(\ref{fact1}) holds of the relation $R$. For the relation $R^{*}$ defined above, the principle of rule induction is stated as follows. In order to prove that a property $P[x,y]$ holds for all $x$ and $y$ for which $R^{*}(x,y)$, it suffices to show that: \begin{itemize} \item for all $x$ and $y$, $R(x,y)$ implies $P[x,y]$ \item for all $x$, $P[x,x]$ \item for all $x$, $y$, and $z$, $P[x,z]$ and $P[z,y]$ imply $P[x,y]$ \end{itemize} \noindent This is an inductive form of argument: if the property $P$ holds in the `base cases' corresponding to rules {{\small\bf R}\bf 1} and {{\small\bf R}\bf 2}, and if $P$ is preserved by the rule {{\small\bf R}\bf 3} (the `step case' of the induction), then every pair in $R^{*}$ has the property $P$. A similar induction principle holds for every relation inductively defined by a set of rules. \section{Inductive definitions in logic}\label{in-logic} Inductive definitions are based on the concept of a relation being closed under a set of rules. Since rules are essentially implications---{\it if\/} the premisses and side conditions hold, {\it then\/} the conclusion holds---it is straightforward to express this concept in logic. Consider, for example, the rules given above for reflexive-transitive closure. Let $R : \alpha{\rightarrow}\alpha{\rightarrow}bool$ be a fixed but arbitrary relation on $\alpha$. (Here, a relation is represented by a curried function; but we shall continue to speak loosely of a pair of values $x$ and $y$ as being `in' the relation $R$ when $R\;x\;y$ holds.) The following formula then asserts that a relation $P : \alpha{\rightarrow}\alpha{\rightarrow}bool$ is closed under the rules defining the reflexive-transitive closure of $R$: \smallskip \[\begin{array}[t]{@{}l} (\forall x\:y.\:R\;x\;y \supset P\;x\;y)\; \wedge \\ (\forall x.\:P\;x\;x)\; \wedge \\ (\forall x\:y.\:(\exists z.\:P\;x\;z \wedge P\;z\;y) \supset P\;x\;y) \end{array}\] \smallskip \noindent Each rule is expressed by a quantified implication of its conclusion by the conjunction of its premisses and side conditions. A rule with no side conditions or premisses is just represented by a universally quantified assertion of its conclusion. Closure of a relation under any set of rules of the form discussed above can be expressed in logic in a similar way. Using this method of expressing the notion of \mbox{closure} under a set of rules, one can define the {\it least\/} relation closed under a set of rules simply by taking the intersection of all such relations. For example, a function \[ {\sf Rtc} : (\alpha{\rightarrow}\alpha{\rightarrow}bool) \rightarrow (\alpha{\rightarrow}\alpha{\rightarrow}bool) \] \noindent that maps an arbitrary relation $R : \alpha{\rightarrow}\alpha{\rightarrow}bool$ to its reflexive-transitive closure ${\sf Rtc}\;R$ can be defined in the {\small HOL} logic by the constant definition: \[\vdash \begin{array}[t]{@{}l} \forall R\:x\:y.\:{\sf Rtc}\;R\;x\;y\;= \\ \quad\forall P.\:(\begin{array}[t]{@{}l} (\forall x\: y.\:R\;x\;y \supset P\;x\;y)\; \wedge \\ (\forall x.\:P\;x\;x)\; \wedge \\ (\forall x\: y.\:(\exists z.\:P\;x\;z \wedge P\;z\;y) \supset P\;x\;y)) \\ \quad\supset\\ P\;x\;y \end{array}\end{array}\] \noindent This definition states that a pair $x$ and $y$ is in the relation ${\sf Rtc}\;R$ exactly when it is in every relation $P$ closed under the rules for reflexive-transitive closure. That is, ${\sf Rtc}\;R$ is \mbox{defined} to be the intersection of all relations closed under these rules. As will be discussed in the section that follows, this indeed makes ${\sf Rtc}\;R$ the least such relation, as required. \subsection{Deriving the rules and rule induction} Any relation intended to be defined inductively by a set of rules can be defined formally in the {\small HOL} logic by a constant definition of the kind illustrated by the {\sf Rtc} example given above. Such a definition, however, merely introduces the relation as the intersection of all relations that satisfy the desired set of rules. The proof obligations of a derived principle of inductive definition are, first of all, to show that the resulting relation in fact does satisfy these rules, and secondly to show that it is indeed the least such relation. It is these proof obligations which are automated by the {\small HOL} inference rule described below in section~\ref{newind}. In the case of the simple reflexive-transitive closure example, the first proof obligation is to show that: \[ \begin{array}[t]{@{}l} \vdash \forall R\:x\:y.\:R\;x\;y \supset {\sf Rtc}\;R\;x\;y \\[2mm] \vdash \forall R\:x.\:{\sf Rtc}\;R\;x\;x \\[2mm] \vdash \forall R\:x\:y.\: (\exists z.\:{\sf Rtc}\;R\;x\;z \wedge {\sf Rtc}\;R\;z\;y) \supset {\sf Rtc}\;R\;x\;y \end{array}\] \noindent That is, one must prove that the rules {{\small\bf R}\bf 1}, {{\small\bf R}\bf 2}, and {{\small\bf R}\bf 3} follow from the somewhat indirect formal definition of the relation ${\sf Rtc}\;R$ given in the previous section. The second proof obligation is to show that ${\sf Rtc}\;R$ is the least relation that satisfies these rules: \[\vdash \begin{array}[t]{@{}l} \forall R\:P.\:\begin{array}[t]{@{}l} (\begin{array}[t]{@{}l} (\forall x\:y.\:R\;x\;y \supset P\;x\;y)\; \wedge \\ (\forall x.\:P\;x\;x)\; \wedge \\ (\forall x\:y.\:(\exists z.\:P\;x\;z \wedge P\;z\;y) \supset P\;x\;y))\end{array}\\ \quad\supset\\ \forall x\:y.\: {\sf Rtc}\;R\;x\;y \supset P\;x\;y \end{array}\end{array}\] \noindent This is the principle of rule induction for ${\sf Rtc}\;R$. These four theorems constitute a complete statement of the defining properties of reflexive-transitive closure. All four can be proved fully automatically in {\small HOL} by the derived inference rule described in the next section. \section{Automation}\label{newind} The main component of the inductive definitions package is an {\small ML} function that takes as an argument a list of rules and automatically proves the defining properties of the \mbox{relation} inductively defined by them. More precisely, this derived {\small HOL} inference rule builds a term that denotes the least relation closed under the rules using the intersection construction described in the previous section. A constant is then introduced (via a constant specification) to name this relation. The result is a set of theorems stating that the newly-defined relation is the least relation closed under the rules supplied by the user. The {\small ML} function that implements this principle of inductive definition is: \medskip \noindent\begin{tabular}{@{\hskip\mathindent}l@{\hskip4.6mm}l@{}} \verb!new_inductive_definition! & \mbox{} \\ \verb! : bool ->! & ({\it infix flag\/})\\ \verb! string ->! & ({\it defn.\ name\/})\\ \verb! (term # term list) ->! & ({\it pattern\/})\\ \verb! (term list # term) list ->! & ({\it rules\/})\\ \verb! (thm list # thm)! & ({\it result\/}) \end{tabular} \medskip \noindent The first argument to this function is a boolean flag which indicates if the constant that is defined is to have infix syntactic status. The second argument is the name under which the resulting definition will be saved on disk. The third argument is a `pattern' that supplies information which is needed because this {\small ML} function can be used to define classes of inductively defined relations, rather than just single instances of these relations. Details of the purpose and format of this pattern will be explained later. The final argument is a list of rules, each of which is represented by a pair of the form: \[ \hbox{\verb!([!}\, \hbox{\it premisses and side conditions\/}\,\hbox{\verb!], !} \hbox{\it conclusion\/}\hbox{\verb!)!} \] \noindent The first component is a list of the premisses and side conditions, which may be arranged in any order. The second component is the conclusion of the rule. Side conditions can be arbitrary boolean terms, provided they do not mention the relation being defined. The premisses and conclusion must be positive assertions of membership in the relation being defined. The precise form that these assertions must take is explained later, but roughly speaking the premisses and conclusion of a rule must be terms of form \verb!"!$R\;\,t_1\;\,\dots\;\,t_n$\verb!"!, where \[ R\; \hbox{\verb!:!}\; \sigma_1 \;\hbox{\verb!->!}\; \dots \;\hbox{\verb!->!}\; \sigma_n \;\hbox{\verb!->!}\; \hbox{\verb!bool!}\] \noindent is a variable representing the $n$-place relation that is to be defined, and each $t_i \hbox{\verb!:!} \sigma_i$ is an arbitrary term not containing $R$. Given an infix flag, a name, a pattern, and a list of rules, the {\small ML} function \verb!new_inductive_definition! automatically proves the existence of the least relation that satisfies these rules. A constant is then introduced to denote this relation using a constant specification, the result of which is saved on disk under the supplied name. The value returned is a pair consisting of a list of theorems which state that the newly-defined relation satisfies the rules, together with a \mbox{theorem} asserting rule induction for the relation. These theorems give a complete statement of the defining properties for the least relation closed under the specified set of rules. \subsection{A simple example} The following example {\small HOL} session shows how the function \verb!new_inductive_definition! can be used to inductively define the set of even natural numbers. \begin{session}\begin{verbatim} #let (rules,ind) = let Even = "Even:num->bool" in new_inductive_definition false `Even` ("^Even n", []) [ [ % ----------------------------- % ], "^Even 0" ; [ "^Even n" % ----------------------------- % ], "^Even (n+2)" ];; \end{verbatim}\end{session} \noindent The first rule in this definition states that \verb!0! is an even natural number, and the second rule states that if \verb!n! is even then \verb!n+2! is also even. (Antiquotation and {\small ML} comments are used to give a readable presentation of these rules.) Since the even natural numbers are \mbox{exactly} those numbers obtainable from zero by adding multiples of two, these rules inductively define `\verb!Even n!' such that it holds \mbox{precisely} when \verb!n! is even. The value supplied for the pattern in this example is the pair \verb!("Even n",[])!. The first component of this pair indicates that the constant to be defined, namely \verb!Even!, is a one-place function with typical argument \verb!n!. In general, the second component of a pattern is a non-empty list only when a {\it class\/} of relations is being defined (see below). In this example, {\verb!Even!} is a single inductively-defined predicate, and the list component of the pattern is therefore empty. When the definition shown in box 1 is evaluated, \verb!new_inductive_definition! automatically proves the existence of the least predicate closed under the given list of rules and then defines the constant \verb!Even! to denote this predicate. The following automatically-proved theorems about \verb!Even! are then returned: \begin{session}\begin{alltt} rules = [\(\vdash\) Even 0; \(\vdash\) \(\forall\,\)n. Even n \(\supset\) Even(n + 2)] : thm list ind = \(\vdash\) \(\forall\,\)P. P 0 \(\wedge\) (\(\forall\,\)n. P n \(\supset\) P(n + 2)) \(\supset\) \(\,\)(\(\forall\,\)n. Even n \(\supset\) P n) \end{alltt}\end{session} \noindent The theorems bound to the {\small ML} identifier \verb!rules! state that the required rules hold of the predicate \verb!Even!. And the rule induction theorem bound to \verb!ind! states that the set of numbers for which \verb!Even! holds is the least set that satisfies these rules. An analogous set of defining theorems can be proved automatically for any particular relation inductively defined by a list of rules. The next section shows how this derived principle of inductive definition in {\small HOL} can also be used to define a parameterized class of relations. \subsection{Defining a class of relations} The constant {\sf Rtc} defined in section~\ref{in-logic} is not itself an inductively-defined relation, but rather a function that maps an arbitrary relation $R$ to an inductively-defined relation ${\sf Rtc}\;R$. The function {\sf Rtc} therefore represents an entire class of inductively-defined relations, one for each possible value of $R$. The information that is required by the derived rule \verb!new_inductive_definition! in order to handle the definition of such functions is supplied by its pattern argument. In the general case, a pattern is a pair of the following form: \[\hbox{\verb!("!}R\;v_1\;\dots\;v_n\hbox{\verb!",!}\; \hbox{\verb!["!}v_i\hbox{\verb!";!}\dots\hbox{\verb!;"!}v_j\hbox{\verb!"])!} \] \noindent The first component of the pattern is an application of the $n$-place curried function that is to be defined (in this case, $R$) to $n$ distinct variables $v_1$, \dots, $v_n$. The second component is a list of those variables that occur at the positions in this application which correspond to the parameters of class of inductively-defined relations, rather than to the actual arguments to these relations. An example of the role of the pattern argument in defining a class of relations is provided by the following definition of reflexive-transitive closure in {\small HOL}. \begin{session}\begin{verbatim} #let (rules,ind) = let Rtc = "Rtc:(*->*->bool)->*->*->bool" in new_inductive_definition false `Rtc` ("^Rtc R x y", ["R:*->*->bool"]) [ [ "R (x:*) (y:*):bool" % ----------------------------- % ], "^Rtc R x y" ; [ %------------------------------ % ], "^Rtc R x x" ; [ "^Rtc R x z"; "^Rtc R z y" %------------------------------ % ], "^Rtc R x y" ];; \end{verbatim}\end{session} \noindent The pattern in this case is the pair: \medskip \noindent\hskip\mathindent\verb!("Rtc R x y", ["R:*->*->bool"])! \medskip \noindent The first component of this pattern specifies that the function \verb!Rtc! is to take three arguments in total---a \mbox{relation} \verb!R!, and two values \verb!x! and \verb!y!. The \mbox{second} part of the pattern (the list containing just \verb!R!) specifies that the relation argument \verb!R! is to be a parameter to the class of inductively-defined relations that will be represented by \verb!Rtc!. The remaining variables \verb!x! and \verb!y! are assumed to indicate the positions of actual arguments to the predicate that represents these relations. The result of evaluating this inductive definition in {\small HOL} is the following collection of theorems: \begin{session}\begin{alltt} rules = [\(\vdash\) \(\forall\,\)R x y. R x y \(\supset\) Rtc R x y; \(\vdash\) \(\forall\,\)R x. Rtc R x x; \(\vdash\) \(\forall\,\)R x y. (\(\exists\,\)z. Rtc R x z \(\wedge\) Rtc R z y) \(\supset\) Rtc R x y] : thm list ind = \(\vdash\) \(\forall\,\)R P. (\(\forall\,\)x y. R x y \(\supset\) P x y) \(\wedge\) (\(\forall\,\)x. P x x) \(\wedge\) (\(\forall\,\)x y. (\(\exists\,\)z. P x z \(\wedge\) P z y) \(\supset\) P x y) \(\supset\) (\(\forall\,\)x y. Rtc R x y \(\supset\) P x y) \end{alltt}\end{session} \noindent Here, the {\small ML} variable \verb!rules! has been bound to a list of theorems which state the three rules that inductively define the reflexive-transitive closure of a relation. The \mbox{theorem} \verb!ind! states the corresponding principle of rule induction for an inductively-defined relation \verb!Rtc R!. \subsection{Stating premisses and conclusions} In addition to the use of the pattern argument, the \verb!Rtc! example also illustrates a restriction on the form in which the premisses and conclusions of rules must be supplied to \verb!new_inductive_definition!. As was mentioned above, premisses and conclusions must be positive assertions of membership of the form \medskip \noindent\hskip\mathindent\verb!"!$R\;\,t_1\;\,\dots\;\,t_n$\verb!"! \medskip \noindent where $R$ is a variable that stands for the function to be defined. The restriction is that some of the terms among the arguments $t_1$, \dots, $t_n$ in such an \mbox{assertion} must be variables---namely, the terms that occur at \mbox{positions} which, according to the supplied pattern, \mbox{correspond} to the parameters of a class of relations. In particular, the terms that occur at these positions must be the same variables given in the pattern itself. The rules for reflexive-transitive closure shown in box 3 conform to this restriction. Here, the pattern indicates that in the typical assertion of membership \verb!"Rtc R x y"! (i.e.\ the first component of the pattern), the variable \verb!R! marks the position of a parameter to the class of relations to be defined. Every premiss and conclusion mentioned in the rules must therefore be a term of the form $\hbox{\verb!"Rtc R!}\;\,t_1\;\,t_2\hbox{\verb!"!}$, where the arguments $t_1$ and $t_2$ may be arbitrary terms but the parameter \verb!R! must be the variable given in the pattern. \section{A tactic for rule induction} The inductive definitions package in {\small HOL} includes a number of auxiliary functions that support reasoning about inductively-defined relations, in addition to the derived rule of definition itself. The most important of these is the following general tactic for goal-directed proofs by rule induction: \medskip \noindent\begin{tabular}{@{\hskip\mathindent}l@{\hskip12.7mm}l@{}} \verb!RULE_INDUCT_THEN! & \mbox{} \\ \verb! : thm ->! & ({\it induction thm\/})\\ \verb! (thm -> tactic) ->! & ({\it premiss cont.\/})\\ \verb! (thm -> tactic) ->! & ({\it side cond.\ cont.\/})\\ \verb! tactic! & ({\it result\/}) \end{tabular} \medskip \noindent The first argument to this function is the rule \mbox{induction} theorem returned by \verb!new_inductive_definition! for a given inductively-defined relation. Like the general structural induction tactic in {\small HOL}, the rule induction tactic is parameterized by functions that determine what is done with induction hypotheses. These may be either premisses or side conditions, and the user may wish to treat these two kinds of induction hypotheses differently. Two separate theorem continuations are therefore supplied as the second and third arguments to the function \verb!RULE_INDUCT_THEN!. Given the rule induction theorem for an inductively-defined $n$-ary relation $R$, the function described above returns a specialized rule induction tactic that reduces goals of the form: \[ \hbox{\verb!"!}\forall x_1\;\dots\;x_n\hbox{\verb!.!}\; R \;x_1\;\dots\;x_n \supset P[x_1,\dots,x_n]\hbox{\verb!"!} \] \noindent to the subgoal(s) of proving that the property $P$ is preserved by the rules that inductively define $R$. The rule induction theorem for \verb!Rtc!, for example, is: \begin{session}\begin{alltt} #ind;; \(\vdash\) \(\forall\,\)R P. (\(\forall\,\)x y. R x y \(\supset\) P x y) \(\wedge\) (\(\forall\,\)x. P x x) \(\wedge\) (\(\forall\,\)x y. (\(\exists\,\)z. P x z \(\wedge\) P z y) \(\supset\) P x y) \(\supset\) (\(\forall\,\)x y. Rtc R x y \(\supset\) P x y) \end{alltt}\end{session} \noindent A rule induction tactic for \verb!Rtc! can be constructed from this theorem by making the simple {\small ML} definition: \begin{session}\begin{alltt} #let Rtc_INDUCT_TAC = RULE_INDUCT_THEN ind ASSUME_TAC ASSUME_TAC;; Rtc_INDUCT_TAC = - : tactic \end{alltt}\end{session} \noindent The use of \verb!ASSUME_TAC! in this definition means that the induction hypotheses arising from the premisses and side conditions of the rules are to be added to the assumptions of the subgoals that are generated. The resulting rule induction tactic for \verb!Rtc! is described by: \bigskip \noindent\begin{tabular}{@{\hskip\mathindent}c@{}} $\Gamma\;\:$\verb!?-!$\;\:\forall x\:y$\verb!. Rtc!$\;R\;x\;y \supset P[x,y]$\\ \trule{62mm}\\ $\Gamma \cup \{R\;x\;y\}\;\:$\verb!?-!$\;\:P[x,y]$\\[1mm] $\Gamma\;\:$\verb!?-!$\;\:\forall x$\verb!.!$\;P[x,x]$\\[1mm] $\Gamma\;{\cup}\;\{P[x,z],\:P[z,y]\}\;\:$\verb!?-!$\;\:P[x,y]$ \end{tabular} \bigskip \noindent This tactic implements the induction scheme described above in section~\ref{rule-ind}. It reduces the goal of proving that a property $P[x,y]$ holds for all pairs $x$ and $y$ related by $\hbox{\verb!Rtc!}\;R$ to showing that this property is preserved by the rules that inductively define this relation. \subsection{An example} The following session shows how the rule induction tactic for \verb!Rtc! constructed in the previous section can be used to prove a simple theorem about this relation. The aim is to show that the reflexive-transitive closure of a symmetric relation is also symmetric. The proof begins by using the {\small HOL} subgoal package (see~\cite{description}) to set up an appropriate goal to be proved: \smallskip \begin{session}\begin{alltt} #set_goal (["\(\forall\,\)x:*. \(\forall\,\)y. R x y \(\supset\) R y x"], "\(\forall\,\)x:*. \(\forall\,\)y. Rtc R x y \(\supset\) Rtc R y x");; "\(\forall\,\)x y. Rtc R x y \(\supset\) Rtc R y x" [ "\(\forall\,\)x y. R x y \(\supset\) R y x" ] () : void \end{alltt}\end{session} \smallskip \noindent The assumption of the goal is that the relation \verb!R! is symmetric, and the conclusion states that the closure \verb!Rtc R! is also symmetric. The conclusion of the goal is in precisely the right form for a proof by rule induction using the induction tactic described above. Applying this tactic results in: \smallskip \begin{session}\begin{alltt} #expand Rtc_INDUCT_TAC;; OK.. 3 subgoals "Rtc R y x" {\rm({\it{subgoal 1\/}})} [ "\(\forall\,\)x y. R x y \(\supset\) R y x" ] [ "Rtc R z x" ] [ "Rtc R y z" ] "\(\forall\,\)x. Rtc R x x" \(\!\){\rm({\it{subgoal 2\/}})} [ "\(\forall\,\)x y. R x y \(\supset\) R y x" ] "Rtc R y x" {\rm({\it{subgoal 3\/}})} [ "\(\forall\,\)x y. R x y \(\supset\) R y x" ] [ "R x y" ] () : void \end{alltt}\end{session} \smallskip \noindent Subgoals 1 and 2 are trivial, since the relation \verb!Rtc R! is transitive and reflexive by definition. The tactic proofs for these subgoals can simply use the rules shown above in box~4. The proof of subgoal 3 is also easy. The proposition \verb!"R y x"! follows immediately from the two assumptions of the subgoal; and this proposition \mbox{together} with the fact that \bigskip \noindent\hskip\mathindent$\vdash\forall\,$\verb!R x y. R x y !$\supset $\verb! Rtc R x y! \bigskip \noindent directly entail the required conclusion. The proof sketched above is a trivial example of the kind of reasoning sometimes referred to as induction over the structure (or the depth) of derivations in a deductive system stated by a set of rules. This form of inductive \mbox{argument}, which is very common in certain \mbox{areas} of theory (for example, operational semantics and process algebras), is made directly accessible in {\small HOL} by the tactic described in this section. \section{Tactics and inference rules} In addition to the rule induction tactic described above, the inductive definitions package also provides mechanized support for generating tactics from the theorems that state the rules for an inductively-defined relation. This takes the form of an {\small ML} function: \medskip \noindent\hskip\mathindent\verb!RULE_TAC : thm -> tactic! \medskip \noindent The theorem argument to this function is expected to be a rule expressed in the form proved by the derived principle of inductive definition described in section~\ref{newind}. Given such a theorem, \verb!RULE_TAC! constructs a tactic that inverts the rule stated by it. The resulting tactic reduces goals that match the conclusion of the rule to subgoals consisting of the corresponding instances of its premisses and side conditions. Consider, for example, the theorem which states the transitivity rule for \verb!Rtc!: \[\vdash \forall\,\hbox{\verb!R x y. !}\begin{array}[t]{@{}l}% \hbox{\verb!(!}\exists\, \hbox{\verb!z. Rtc R x z !}\wedge\hbox{\verb! Rtc R z y)!}\\ \quad \supset \\ \hbox{\verb!Rtc R x y!} \end{array} \] \noindent When applied to this theorem, the function \verb!RULE_TAC! returns the tactic described by: \bigskip \noindent\begin{tabular}{@{\hskip\mathindent}c@{}} $\Gamma\;\:$\verb!?-!$\;\:$\verb!Rtc!$\;R\;x\;y$ \\ \trule{62mm}\\ $\Gamma\;\:$\verb!?-!$\;\:\exists z $\verb!.!$\;$\verb!Rtc!$\;R\;x\;z\;\:\wedge\;\;$\verb!Rtc!$\;R\;z\;y$ \end{tabular} \bigskip \noindent This tactic can then be used in goal-directed proofs about membership in the inductively-defined relation {\verb!Rtc!$\;R$}. The other two rules that define \verb!Rtc!$\;R$ can also be converted into tactics using the function \verb!RULE_TAC!. The result is a complete set of {\small HOL} tactics for goal-directed proofs in the deductive system comprising the three rules that define reflexive-transitive closure. It is intended that the inductive definitions package will also include a function that maps rules stated as theorems to forward inference rules in {\small HOL} (i.e.\ to {\small ML} functions). For example, the transitivity theorem shown above can be used to implement the following derived inference rule: \bigskip \noindent\begin{tabular}{@{\hskip\mathindent}c@{}} $\Gamma_1\;{\vdash}\;$\verb!Rtc!$\;R\;x\;z$\qquad $\Gamma_2\;{\vdash}\;$\verb!Rtc!$\;R\;z\;y$\\ \rrule{62mm}\\ $\Gamma_1 \cup \Gamma_2\;{\vdash}\;$\verb!Rtc!$\;R\;x\;y$ \end{tabular} \bigskip \noindent Any rule expressed as a theorem of the form proved by the derived principle of inductive definitions can likewise be converted into a forward inference rule. A function that \mbox{automatically} constructs such rules has not yet been implemented, partly because it has not been found necessary for the applications done so far (see section~\ref{appl}). For completeness, however, the author intends in future to add this function to the inductive definitions package. \section{Case analysis} The final major component of the {\small HOL} package for inductive definitions is an {\small ML} function that proves an \mbox{exhaustive} case analysis theorem for any given relation inductively defined by a set of rules. The name and type of this function are: \medskip \noindent\hskip\mathindent\verb!derive_cases_thm : (thm list # thm) -> thm! \medskip \noindent The arguments to this function are the list of rules satisfied by an inductively defined relation, together with its rule induction theorem. (These are precisely the defining theorems which are proved and returned by \verb!new_inductive_definition!.) When supplied with these theorems, \verb!derive_cases_thm! proves that if an assertion of membership in the relation holds, then it holds only by virtue of the fact that one of the rules can be used to derive it. This allows one to drive the rules that define a relation `backwards', inferring from the conclusion of one of the rules that the premisses and side conditions hold. The following interaction with the {\small HOL} system shows the theorem proved by \verb!derive_cases_thm! for the \verb!Rtc! example introduced above. The {\small ML} variables \verb!rules! and \verb!ind! are assumed to have the bindings shown above in box~4. \smallskip \begin{session}\begin{alltt} #derive_cases_thm (rules,ind);; \(\vdash\) \(\forall\,\)R x y. Rtc R x y \(\supset\) R x y \(\vee\) (y = x) \(\vee\) (\(\exists\,\)z. Rtc R x z \(\wedge\) Rtc R z y) \end{alltt}\end{session} \smallskip \noindent Roughly speaking, the resulting theorem states that if \verb!Rtc R x y! holds, then either: \begin{itemize} \item it is derivable by the inclusion rule {{\small\bf R}\bf 1}, in which case \verb!x! and \verb!y! are related by \verb!R!; or \item it is derivable by the reflexivity rule {{\small\bf R}\bf 2}, in which case \verb!x! and \verb!y! are equal; or \item it is derivable by the transitivity rule {{\small\bf R}\bf 3}, in which case there must be an intermediate value \verb!z! such that \verb!Rtc R x z! and \verb!Rtc R z y!. \end{itemize} \noindent A similar theorem can be proved automatically for any relation defined inductively using the package. Work is currently underway to strengthen this theorem from an implication to an equation, so that it can be used for rewriting. \section{Applications}\label{appl} In a joint project with Juanito Camilleri, a set of example proofs has been developed to illustrate the potential for applications of the inductive \mbox{definitions} package. These examples include: the definition of an operational semantics for a simple programming language and a proof that its evaluation relation is \mbox{deterministic}; the definition of a reduction relation for combinatory logic and a proof that it has the Church-Rosser property; a definition of \mbox{provability} in a Hilbert style proof system for minimal intuitionistic logic; the definition of a type system for combinatory logic and a proof of the Curry-Howard isomorphism for typed combinatory logic and minimal intuitionistic logic; and definitions of the trace and transition semantics for a simple process algebra, \mbox{together} with the proof of a formal statement of the relationship between them. A report on this work is in preparation, and the {\small HOL} source code for the examples will be made available to interested users. \newpage \begin{thebibliography}{9} \bibitem{description} DSTO, The University of Cambridge, and SRI \mbox{International}, {\it The HOL System: DESCRIPTION} (1991). \bibitem{melham} T.\ F.\ Melham, `Automating Recursive Type Definitions in Higher Order Logic', in: {\it Current Trends in Hardware Verification and Automated Theorem Proving\/}, edited by G.\ Birtwistle and P.A.\ Subrahmanyam (Springer-Verlag, 1989), pp.\ 341--386. \bibitem{pitts} A.\ M.\ Pitts, `Semantics of Programming Languages', unpublished lecture notes, University of Cambridge Computer Laboratory (October 1989). \bibitem{winskel} G.\ Winskel, `Introduction to the Formal Semantics of Programming Languages', unpublished lecture notes, University of Cambridge Computer Laboratory (October 1985). \end{thebibliography} \end{document}