1\documentclass[twocolumn,fleqn,layout]{article}
2\usepackage{alltt}
3
4\pagestyle{plain}
5\flushbottom
6\sloppy
7\begin{document}
8
9\input{macros}
10\sloppy
11
12
13
14\twocolumn[{\scriptsize \parbox{100mm}{Preprint of a paper
15to appear in the Proceedings of the 1991 International Tutorial
16and Workshop on the HOL Theorem Proving System, 27--30 August 1991,
17Davis California (IEEE Computer Society Press).}}\vskip10mm
18\begin{center}
19{\Large\bf A Package for Inductive Relation Definitions in HOL}\\
20\vskip24pt
21T.\ F.\ Melham\\
22\vskip12pt
23University of Cambridge Computer Laboratory\\
24New Museums Site, Pembroke Street\\
25Cambridge, CB2 3QG, England.\\
26\mbox{}\\
27\vskip3mm
28\end{center}]
29
30\subsection*{\centering Abstract}
31
32{\it\sloppy This paper describes a set of theorem proving tools based on a new
33derived principle of definition in HOL, namely the introduction of relations
34inductively defined by a set of rules.  Such inductive definitions abound in
35computer science. Example application areas \mbox{include} reasoning about
36structured operational semantics, type judgements, transition relations for
37process algebras, \mbox{reduction} relations, and compositional proof systems.
38The package described in this paper automates the derivation of certain
39inductive definitions involved in these applications and provides the basic
40tools needed for reasoning about the relations introduced by them.}
41
42\vskip12pt
43\section{Introduction}
44
45The HOL user community has a strong tradition of taking a purely {\it
46definitional\/} approach to using higher order logic. That is, the syntax of
47the logic is extended with new notation not simply by postulating axioms to
48give meaning to it, but rather by defining it in terms of existing expressions
49of the logic that already have the required semantics.  The advantage of this
50approach, as opposed to the axiomatic method, is that each of the primitive
51rules of definition in the {\small HOL} logic---namely, constant definition,
52constant specification, and type definition---is guaranteed to preserve
53consistency.  The disadvantage is that these rules admit only
54\mbox{definitions} that satisfy certain very restrictive rules of formation.
55Definitions expressed in any other form must always be justified formally by
56deriving them from equivalent, but possibly rather complex, primitive
57definitions.
58
59The {\small ML} metalanguage allows users to implement derived inference rules
60in the {\small HOL} system and thus provides a facility for automating proofs
61that justify derived rules of definition.  For example, recursive
62\mbox{definitions} are not admitted by the primitive rules of definition of the
63{\small HOL} logic.  But certain recursive type definitions and function
64definitions are supported in the system by derived inference rules written in
65{\small ML}~\cite{description,melham}.  The details of the primitive
66definitions that underlie these rules are hidden from the user, and their
67{\small ML} implementations are highly optimized. So these \mbox{derived}
68principles of definition may simply be regarded as primitive by most users of
69the system.
70
71This paper describes a set of theorem-proving tools based on a new derived
72principle of definition in {\small HOL} for defining relations inductively by a
73set of rules. \mbox{Sections~\ref{ind-defs}} and~\ref{in-logic} give a general
74introduction to the class of inductive definitions handled by the package and
75explain the logical basis for these definitions.  The remaining sections
76describe the {\small ML} functions provided by the package and briefly mention
77some applications for which the package can be used.
78
79\section{Inductive definitions}\label{ind-defs}
80
81The following is a simple but typical example of a relation defined inductively
82by a set of rules. (This example is taken from~\cite{pitts}.) Let $R \subseteq
83A \times A$ be a binary relation on a set $A$.  The reflexive-transitive
84closure of $R$ can be defined to be the least relation $R^{*} \subseteq A
85\times A$ for which the following deduction rules hold.
86
87\medskip
88
89\[ \begin{array}[t]{@{}l}
90   \hbox{{\small\bf R}\bf 1}\quad\Rule{}{R^{*}(x,y)}\;\; R(x,y) \\[6mm]
91   \hbox{{\small\bf R}\bf 2}\quad\Rule{}{R^{*}(x,x)}\\[8mm]
92   \hbox{{\small\bf R}\bf 3}\quad\Rule{R^{*}(x,z)\qquad R^{*}(z,y)}
93         {R^{*}(x,y)}
94\end{array} \]
95
96\medskip
97
98\noindent These rules state precisely the properties required of the
99reflexive-transitive closure of the relation $R$.  Rule {{\small\bf R}\bf 1}
100states that it must contain at least all the values in $R$; rule {{\small\bf
101R}\bf 2} states that it must be reflexive; and rule {{\small\bf R}\bf 3} states
102that it must be transitive.  The reflexive-transitive closure $R^{*}$ may
103therefore simply be {\it defined\/} to be the least relation that satisfies
104these conditions.  It then follows simply by definition that the rules
105{{\small\bf R}\bf 1}, {{\small\bf R}\bf 2} and {{\small\bf R}\bf 3} are in fact
106satisfied by $R^{*}$.  Moreover, it follows immediately that $R^{*}$ is a
107subset of any other relation that satisfies these rules, since $R^{*}$ is
108defined to be the {\it least\/} such relation.  This means that $R^{*}$
109contains only those pairs of values that it must contain by virtue of
110satisfying the rules. As will be discussed below, this property gives rise to
111an induction principle for reasoning about the relation $R^{*}$.
112
113The definition given above is valid because the rules {{\small\bf R}\bf 1},
114{{\small\bf R}\bf 2}, and {{\small\bf R}\bf 3} make only positive statements
115about the elements of $R^{*}$.  This guarantees that the least relation
116satisfying these rules does exist.  In particular, if the rules have this form,
117then one can show that the intersection of any set of relations that satisfy
118the rules also satisfies the rules.  Moreover, at least one binary relation
119satisfies the rules, namely the maximal relation $A \times A$. The `least' or
120smallest relation that satisfies the rules may therefore legitimately be
121defined to be the intersection of all such relations.
122
123In general, an inductive definition of an $n$-place \mbox{relation} $R$
124consists of a set of rules of the form:
125
126\smallskip
127
128\[ \Rule{R(t_1^1,\dots,t_n^1) \quad \cdots \quad R(t_1^i,\dots,t_n^i)}
129        {R(t_1,\dots,t_n)}\;\;C_1\:\cdots\:C_j \]
130
131\smallskip
132
133\noindent The terms above the line are the {\it premisses\/} of the rule, each
134of which makes a positive assertion of membership in the relation $R$.  The
135term below the line, called the {\it conclusion\/} of the rule, likewise
136asserts membership in $R$. The terms $C_1$,\dots,$C_j$ are {\it side
137conditions\/} on the rule; these may be arbitrary propositions not involving
138the relation $R$ being defined. A relation $R$ is {\it closed\/} under such a
139rule if whenever the premisses and side conditions hold, the conclusion also
140holds.  The relation {\it inductively defined\/} by a collection of such rules
141is the least relation closed under all the rules.
142
143\subsection{Rule induction}\label{rule-ind}
144
145By virtue of its definition as the {\it least\/} relation closed under a set of
146rules, every inductively defined relation comes with an associated induction
147principle.  This principle of {\it rule induction\/} is essential for many
148proofs involving such relations. (The term `rule induction' was coined by Glynn
149Winskel in~\cite{winskel}).
150
151The principle of rule induction for an inductively defined relation may be
152stated briefly as follows. Let $R$ be an $n$-place relation inductively defined
153by a set of rules, and suppose we wish to show that every element in $R$ has a
154certain property $P$:
155
156{\samepage
157\begin{equation}\label{fact1}
158\hbox{\rm
159if}\;\;R(x_1,\dots,x_n)\;\;\hbox{then}\;\;P[x_1,\dots,x_n]
160\end{equation}
161
162\noindent Since $R$ is} \pagebreak[3] the least relation closed under the
163rules, any relation $S$ which is also closed under the rules has the property
164that $R \subseteq S$.  Now, let
165
166\[S = \{(x_1,\dots,x_n) \mid P[x_1,\dots,x_n]\}\]
167
168\noindent Then to prove the desired property of $R$, it suffices to show that
169the relation $S$ is closed under the rules that define $R$. For if the relation
170$S$ in fact is closed under the rules, then we have that $R \subseteq S$ and
171therefore that every element of $R$ has the defining property of $S$---i.e.\
172statement~(\ref{fact1}) holds of the relation $R$.
173
174For the relation $R^{*}$ defined above, the principle of rule induction is
175stated as follows. In order to prove that a property $P[x,y]$ holds for all
176$x$ and $y$ for which $R^{*}(x,y)$, it suffices to show that:
177
178\begin{itemize}
179
180\item for all $x$ and $y$, $R(x,y)$ implies $P[x,y]$
181
182\item for all $x$, $P[x,x]$
183
184\item for all $x$, $y$, and $z$, $P[x,z]$ and $P[z,y]$ imply $P[x,y]$
185
186\end{itemize}
187
188\noindent This is an inductive form of argument: if the property $P$ holds in
189the `base cases' corresponding to rules {{\small\bf R}\bf 1} and {{\small\bf
190R}\bf 2}, and if $P$ is preserved by the rule {{\small\bf R}\bf 3} (the `step
191case' of the induction), then every pair in $R^{*}$ has the property $P$.  A
192similar induction principle holds for every relation inductively defined by a
193set of rules.
194
195\section{Inductive definitions in logic}\label{in-logic}
196
197
198Inductive definitions are based on the concept of a relation being closed under
199a set of rules.  Since rules are essentially implications---{\it if\/} the
200premisses and side conditions hold, {\it then\/} the conclusion holds---it is
201straightforward to express this concept in logic.
202
203Consider, for example, the rules given above for reflexive-transitive closure.
204Let $R : \alpha{\rightarrow}\alpha{\rightarrow}bool$ be a fixed but arbitrary
205 relation on $\alpha$. (Here, a relation is represented by a curried function;
206but we shall continue to speak loosely of a pair of values $x$ and $y$ as being
207`in' the relation $R$ when $R\;x\;y$ holds.)  The following formula then
208asserts that a relation $P : \alpha{\rightarrow}\alpha{\rightarrow}bool$ is
209closed under the rules defining the reflexive-transitive closure of $R$:
210
211\smallskip
212\[\begin{array}[t]{@{}l}
213 (\forall x\:y.\:R\;x\;y \supset P\;x\;y)\; \wedge \\
214 (\forall x.\:P\;x\;x)\; \wedge \\
215 (\forall x\:y.\:(\exists z.\:P\;x\;z \wedge P\;z\;y) \supset P\;x\;y)
216\end{array}\]
217\smallskip
218
219\noindent Each rule is expressed by a quantified implication of its conclusion
220by the conjunction of its premisses and side conditions.  A rule with no side
221conditions or premisses is just represented by a universally quantified
222assertion of its conclusion. Closure of a relation under any set of rules of
223the form discussed above can be expressed in logic in a similar way.
224
225Using this method of expressing the notion of \mbox{closure} under a set of
226rules, one can define the {\it least\/} relation closed under a set of rules
227simply by taking the intersection of all such relations.  For example, a
228function
229
230\[ {\sf Rtc} : (\alpha{\rightarrow}\alpha{\rightarrow}bool) \rightarrow
231(\alpha{\rightarrow}\alpha{\rightarrow}bool) \]
232
233\noindent that maps an arbitrary relation $R :
234\alpha{\rightarrow}\alpha{\rightarrow}bool$ to its reflexive-transitive closure
235${\sf Rtc}\;R$ can be defined in the {\small HOL} logic by the constant
236definition:
237
238\[\vdash \begin{array}[t]{@{}l}
239\forall R\:x\:y.\:{\sf Rtc}\;R\;x\;y\;= \\
240\quad\forall P.\:(\begin{array}[t]{@{}l}
241  (\forall x\: y.\:R\;x\;y \supset P\;x\;y)\; \wedge \\
242  (\forall x.\:P\;x\;x)\; \wedge \\
243  (\forall x\: y.\:(\exists z.\:P\;x\;z \wedge P\;z\;y) \supset P\;x\;y)) \\
244\quad\supset\\
245P\;x\;y
246\end{array}\end{array}\]
247
248\noindent This definition states that a pair $x$ and $y$ is in the relation
249${\sf Rtc}\;R$ exactly when it is in every relation $P$ closed under the rules
250for reflexive-transitive closure. That is, ${\sf Rtc}\;R$ is \mbox{defined} to
251be the intersection of all relations closed under these rules.  As will be
252discussed in the section that follows, this indeed makes ${\sf Rtc}\;R$ the
253least such relation, as required.
254
255
256\subsection{Deriving the rules and rule induction}
257
258Any relation intended to be defined inductively by a set of rules can be
259defined formally in the {\small HOL} logic by a constant definition of the kind
260illustrated by the {\sf Rtc} example given above.  Such a definition, however,
261merely introduces the relation as the intersection of all relations that
262satisfy the desired set of rules.  The proof obligations of a derived principle
263of inductive definition are, first of all, to show that the resulting relation
264in fact does satisfy these rules, and secondly to show that it is indeed the
265least such relation.  It is these proof obligations which are automated by the
266{\small HOL} inference rule described below in section~\ref{newind}.
267
268In the case of the simple reflexive-transitive closure example, the first proof
269obligation is to show that:
270
271\[ \begin{array}[t]{@{}l}
272   \vdash \forall R\:x\:y.\:R\;x\;y \supset {\sf Rtc}\;R\;x\;y \\[2mm]
273   \vdash \forall R\:x.\:{\sf Rtc}\;R\;x\;x \\[2mm]
274   \vdash \forall R\:x\:y.\:
275        (\exists z.\:{\sf Rtc}\;R\;x\;z \wedge {\sf Rtc}\;R\;z\;y) \supset
276        {\sf Rtc}\;R\;x\;y
277\end{array}\]
278
279\noindent That is, one must prove that the rules {{\small\bf R}\bf 1},
280{{\small\bf R}\bf 2}, and {{\small\bf R}\bf 3} follow from the somewhat
281indirect formal definition of the relation ${\sf Rtc}\;R$ given in the previous
282section.  The second proof obligation is to show that ${\sf Rtc}\;R$ is the
283least relation that satisfies these rules:
284
285\[\vdash \begin{array}[t]{@{}l}
286\forall R\:P.\:\begin{array}[t]{@{}l}
287  (\begin{array}[t]{@{}l}
288  (\forall x\:y.\:R\;x\;y \supset P\;x\;y)\; \wedge \\
289  (\forall x.\:P\;x\;x)\; \wedge \\
290  (\forall x\:y.\:(\exists z.\:P\;x\;z \wedge P\;z\;y)
291    \supset P\;x\;y))\end{array}\\
292\quad\supset\\
293\forall x\:y.\: {\sf Rtc}\;R\;x\;y \supset P\;x\;y
294\end{array}\end{array}\]
295
296\noindent This is the principle of rule induction for ${\sf Rtc}\;R$.  These
297four theorems constitute a complete statement of the defining properties of
298reflexive-transitive closure. All four can be proved fully automatically in
299{\small HOL} by the derived inference rule described in the next section.
300
301\section{Automation}\label{newind}
302
303The main component of the inductive definitions package is an {\small ML}
304function that takes as an argument a list of rules and automatically proves the
305defining properties of the \mbox{relation} inductively defined by them.  More
306precisely, this derived {\small HOL} inference rule builds a term that denotes
307the least relation closed under the rules using the intersection construction
308described in the previous section.  A constant is then introduced (via a
309constant specification) to name this relation.  The result is a set of theorems
310stating that the newly-defined relation is the least relation closed under the
311rules supplied by the user.
312
313The {\small ML} function that implements this principle of inductive definition
314is:
315
316\medskip
317
318\noindent\begin{tabular}{@{\hskip\mathindent}l@{\hskip4.6mm}l@{}}
319\verb!new_inductive_definition! & \mbox{} \\
320\verb! : bool ->! & ({\it infix flag\/})\\
321\verb!   string ->! & ({\it defn.\ name\/})\\
322\verb!   (term # term list) ->! & ({\it pattern\/})\\
323\verb!   (term list # term) list ->! & ({\it rules\/})\\
324\verb!   (thm list # thm)! & ({\it result\/})
325\end{tabular}
326
327\medskip
328
329\noindent The first argument to this function is a boolean flag which indicates
330if the constant that is defined is to have infix syntactic status.  The second
331argument is the name under which the resulting definition will be saved on
332disk.  The third argument is a `pattern' that supplies information which is
333needed because this {\small ML} function can be used to define classes of
334inductively defined relations, rather than just single instances of these
335relations. Details of the purpose and format of this pattern will be explained
336later.  The final argument is a list of rules, each of which is represented by
337a pair of the form:
338
339\[ \hbox{\verb!([!}\,
340\hbox{\it premisses and side conditions\/}\,\hbox{\verb!], !}
341 \hbox{\it conclusion\/}\hbox{\verb!)!} \]
342
343\noindent The first component is a list of the premisses and side conditions,
344which may be arranged in any order.  The second component is the conclusion of
345the rule.  Side conditions can be arbitrary boolean terms, provided they do not
346mention the relation being defined.  The premisses and conclusion must be
347positive assertions of membership in the relation being defined.  The precise
348form that these assertions must take is explained later, but roughly speaking
349the premisses and conclusion of a rule must be terms of form
350\verb!"!$R\;\,t_1\;\,\dots\;\,t_n$\verb!"!, where
351
352\[ R\; \hbox{\verb!:!}\; \sigma_1 \;\hbox{\verb!->!}\; \dots
353\;\hbox{\verb!->!}\; \sigma_n \;\hbox{\verb!->!}\; \hbox{\verb!bool!}\]
354
355\noindent is a variable representing the $n$-place relation that is to be
356defined, and each $t_i \hbox{\verb!:!} \sigma_i$ is an arbitrary term not
357containing $R$.
358
359Given an infix flag, a name, a pattern, and a list of rules, the {\small ML}
360function \verb!new_inductive_definition! automatically proves the existence of
361the least relation that satisfies these rules.  A constant is then introduced
362to denote this relation using a constant specification, the result of which is
363saved on disk under the supplied name. The value returned is a pair consisting
364of a list of theorems which state that the newly-defined relation satisfies the
365rules, together with a \mbox{theorem} asserting rule induction for the
366relation.  These theorems give a complete statement of the defining properties
367for the least relation closed under the specified set of rules.
368
369\subsection{A simple example}
370
371The following example {\small HOL} session shows how the function
372\verb!new_inductive_definition! can be used to inductively define the set of
373even natural numbers.
374
375\begin{session}\begin{verbatim}
376#let (rules,ind) =
377   let Even = "Even:num->bool" in
378   new_inductive_definition false `Even`
379   ("^Even n", [])
380
381   [ [
382     % ----------------------------- % ],
383                 "^Even 0"           ;
384
385     [           "^Even n"
386     % ----------------------------- % ],
387               "^Even (n+2)"        ];;
388\end{verbatim}\end{session}
389
390
391\noindent The first rule in this definition states that \verb!0! is an even
392natural number, and the second rule states that if \verb!n! is even then
393\verb!n+2! is also even.  (Antiquotation and {\small ML} comments are used to
394give a readable presentation of these rules.)  Since the even natural numbers
395are \mbox{exactly} those numbers obtainable from zero by adding multiples of
396two, these rules inductively define `\verb!Even n!' such that it holds
397\mbox{precisely} when \verb!n! is even.
398
399The value supplied for the pattern in this example is the pair
400\verb!("Even n",[])!.  The first component of this pair indicates that
401the constant to be defined, namely \verb!Even!, is a one-place
402function with typical argument \verb!n!.  In general, the second
403component of a pattern is a non-empty list only when a {\it class\/}
404of relations is being defined (see below).  In this example,
405{\verb!Even!} is a single inductively-defined predicate, and the list
406component of the pattern is therefore empty.
407
408
409When the definition shown in box 1 is evaluated,
410\verb!new_inductive_definition! automatically proves the existence of the least
411predicate closed under the given list of rules and then defines the constant
412\verb!Even! to denote this predicate.  The following automatically-proved
413theorems about \verb!Even! are then returned:
414
415\begin{session}\begin{alltt}
416rules =
417[\(\vdash\) Even 0;
418 \(\vdash\) \(\forall\,\)n. Even n \(\supset\) Even(n + 2)] : thm list
419ind =
420\(\vdash\) \(\forall\,\)P. P 0 \(\wedge\) (\(\forall\,\)n. P n \(\supset\) P(n + 2)) \(\supset\)
421      \(\,\)(\(\forall\,\)n. Even n \(\supset\) P n)
422\end{alltt}\end{session}
423
424
425\noindent The theorems bound to the {\small ML} identifier \verb!rules! state
426that the required rules hold of the predicate \verb!Even!. And the rule
427induction theorem bound to \verb!ind! states that the set of numbers for which
428\verb!Even! holds is the least set that satisfies these rules.
429
430An analogous set of defining theorems can be proved automatically for any
431particular relation inductively defined by a list of rules.  The next section
432shows how this derived principle of inductive definition in {\small HOL} can
433also be used to define a parameterized class of relations.
434
435\subsection{Defining a class of relations}
436
437The constant {\sf Rtc} defined in section~\ref{in-logic} is not itself an
438inductively-defined relation, but rather a function that maps an arbitrary
439relation $R$ to an inductively-defined relation ${\sf Rtc}\;R$.  The function
440{\sf Rtc} therefore represents an entire class of inductively-defined
441relations, one for each possible value of $R$.
442
443The information that is required by the derived rule
444\verb!new_inductive_definition! in order to handle the definition of such
445functions is supplied by its pattern argument.  In the general case, a pattern
446is a pair of the following form:
447
448\[\hbox{\verb!("!}R\;v_1\;\dots\;v_n\hbox{\verb!",!}\;
449 \hbox{\verb!["!}v_i\hbox{\verb!";!}\dots\hbox{\verb!;"!}v_j\hbox{\verb!"])!}
450\]
451
452\noindent The first component of the pattern is an application of the $n$-place
453curried function that is to be defined (in this case, $R$) to $n$ distinct
454variables $v_1$, \dots, $v_n$.  The second component is a list of those
455variables that occur at the positions in this application which correspond to
456the parameters of class of inductively-defined relations, rather than to the
457actual arguments to these relations.
458
459An example of the role of the pattern argument in defining a class of relations
460is provided by the following definition of reflexive-transitive closure in
461{\small HOL}.
462
463\begin{session}\begin{verbatim}
464#let (rules,ind) =
465   let Rtc = "Rtc:(*->*->bool)->*->*->bool"
466 in
467   new_inductive_definition false `Rtc`
468   ("^Rtc R x y", ["R:*->*->bool"])
469
470   [ [      "R (x:*) (y:*):bool"
471     % ----------------------------- % ],
472               "^Rtc R x y"          ;
473
474     [
475     %------------------------------ % ],
476               "^Rtc R x x"          ;
477
478     [  "^Rtc R x z";  "^Rtc R z y"
479     %------------------------------ % ],
480               "^Rtc R x y"          ];;
481\end{verbatim}\end{session}
482
483\noindent The pattern in this case is the pair:
484
485\medskip
486
487\noindent\hskip\mathindent\verb!("Rtc R x y", ["R:*->*->bool"])!
488
489\medskip
490
491\noindent The first component of this pattern specifies that the function
492\verb!Rtc! is to take three arguments in total---a \mbox{relation} \verb!R!,
493and two values \verb!x! and \verb!y!.  The \mbox{second} part of the pattern
494(the list containing just \verb!R!) specifies that the relation argument
495\verb!R! is to be a parameter to the class of inductively-defined relations
496that will be represented by \verb!Rtc!.  The remaining variables \verb!x! and
497\verb!y! are assumed to indicate the positions of actual arguments to the
498predicate that represents these relations.
499
500The result of evaluating this inductive definition in {\small HOL} is the
501following collection of theorems:
502
503\begin{session}\begin{alltt}
504rules =
505[\(\vdash\) \(\forall\,\)R x y. R x y \(\supset\) Rtc R x y;
506 \(\vdash\) \(\forall\,\)R x. Rtc R x x;
507 \(\vdash\) \(\forall\,\)R x y. (\(\exists\,\)z. Rtc R x z \(\wedge\) Rtc R z y)
508              \(\supset\)
509            Rtc R x y] : thm list
510ind =
511\(\vdash\) \(\forall\,\)R P.
512   (\(\forall\,\)x y. R x y \(\supset\) P x y) \(\wedge\)
513   (\(\forall\,\)x. P x x) \(\wedge\)
514   (\(\forall\,\)x y. (\(\exists\,\)z. P x z \(\wedge\) P z y) \(\supset\) P x y)
515      \(\supset\)
516   (\(\forall\,\)x y. Rtc R x y \(\supset\) P x y)
517\end{alltt}\end{session}
518
519\noindent Here, the {\small ML} variable \verb!rules! has been bound to a list
520of theorems which state the three rules that inductively define the
521reflexive-transitive closure of a relation.  The \mbox{theorem} \verb!ind!
522states the corresponding principle of rule induction for an inductively-defined
523relation \verb!Rtc R!.
524
525\subsection{Stating premisses and conclusions}
526
527In addition to the use of the pattern argument, the \verb!Rtc! example also
528illustrates a restriction on the form in which the premisses and conclusions of
529rules must be supplied to \verb!new_inductive_definition!.  As was mentioned
530above, premisses and conclusions must be positive assertions of membership of
531the form
532
533\medskip
534
535\noindent\hskip\mathindent\verb!"!$R\;\,t_1\;\,\dots\;\,t_n$\verb!"!
536
537\medskip
538
539\noindent where $R$ is a variable that stands for the function to be defined.
540The restriction is that some of the terms among the arguments $t_1$, \dots,
541$t_n$ in such an \mbox{assertion} must be variables---namely, the terms that
542occur at \mbox{positions} which, according to the supplied pattern,
543\mbox{correspond} to the parameters of a class of relations.  In particular,
544the terms that occur at these positions must be the same variables given in the
545pattern itself.
546
547The rules for reflexive-transitive closure shown in box 3 conform to
548this restriction.  Here, the pattern indicates that in the typical
549assertion of membership \verb!"Rtc R x y"! (i.e.\ the first component
550of the pattern), the variable \verb!R! marks the position of a
551parameter to the class of relations to be defined.  Every premiss and
552conclusion mentioned in the rules must therefore be a term of the form
553$\hbox{\verb!"Rtc R!}\;\,t_1\;\,t_2\hbox{\verb!"!}$, where the
554arguments $t_1$ and $t_2$ may be arbitrary terms but the parameter
555\verb!R! must be the variable given in the pattern.
556
557\section{A tactic for rule induction}
558
559The inductive definitions package in {\small HOL} includes a number of
560auxiliary functions that support reasoning about inductively-defined relations,
561in addition to the derived rule of definition itself.  The most important of
562these is the following general tactic for goal-directed proofs by rule
563induction:
564
565\medskip
566
567\noindent\begin{tabular}{@{\hskip\mathindent}l@{\hskip12.7mm}l@{}}
568\verb!RULE_INDUCT_THEN! & \mbox{} \\
569\verb! : thm ->! & ({\it induction thm\/})\\
570\verb!   (thm -> tactic) ->! & ({\it premiss cont.\/})\\
571\verb!   (thm -> tactic) ->! & ({\it side cond.\ cont.\/})\\
572\verb!   tactic! & ({\it result\/})
573\end{tabular}
574
575\medskip
576
577\noindent The first argument to this function is the rule \mbox{induction}
578theorem returned by \verb!new_inductive_definition! for a given
579inductively-defined relation.  Like the general structural induction tactic in
580{\small HOL}, the rule induction tactic is parameterized by functions that
581determine what is done with induction hypotheses. These may be either premisses
582or side conditions, and the user may wish to treat these two kinds of induction
583hypotheses differently. Two separate theorem continuations are therefore
584supplied as the second and third arguments to the function
585\verb!RULE_INDUCT_THEN!.
586
587Given the rule induction theorem for an inductively-defined $n$-ary relation
588$R$, the function described above returns a specialized rule induction tactic
589that reduces goals of the form:
590
591\[ \hbox{\verb!"!}\forall x_1\;\dots\;x_n\hbox{\verb!.!}\;
592  R \;x_1\;\dots\;x_n \supset P[x_1,\dots,x_n]\hbox{\verb!"!} \]
593
594\noindent to the subgoal(s) of proving that the property $P$ is preserved by
595the rules that inductively define $R$.  The rule induction theorem for
596\verb!Rtc!, for example, is:
597
598\begin{session}\begin{alltt}
599#ind;;
600\(\vdash\) \(\forall\,\)R P.
601   (\(\forall\,\)x y. R x y \(\supset\) P x y) \(\wedge\)
602   (\(\forall\,\)x. P x x) \(\wedge\)
603   (\(\forall\,\)x y. (\(\exists\,\)z. P x z \(\wedge\) P z y) \(\supset\) P x y)
604      \(\supset\)
605   (\(\forall\,\)x y. Rtc R x y \(\supset\) P x y)
606\end{alltt}\end{session}
607
608\noindent A rule induction tactic for \verb!Rtc! can be constructed from this
609theorem by making the simple {\small ML} definition:
610
611\begin{session}\begin{alltt}
612#let Rtc_INDUCT_TAC =
613   RULE_INDUCT_THEN ind
614      ASSUME_TAC ASSUME_TAC;;
615Rtc_INDUCT_TAC = - : tactic
616\end{alltt}\end{session}
617
618\noindent The use of \verb!ASSUME_TAC! in this definition means that the
619induction hypotheses arising from the premisses and side conditions of the
620rules are to be added to the assumptions of the subgoals that are generated.
621The resulting rule induction tactic for \verb!Rtc!  is described by:
622
623\bigskip
624
625\noindent\begin{tabular}{@{\hskip\mathindent}c@{}}
626$\Gamma\;\:$\verb!?-!$\;\:\forall x\:y$\verb!. Rtc!$\;R\;x\;y \supset P[x,y]$\\
627\trule{62mm}\\
628$\Gamma \cup \{R\;x\;y\}\;\:$\verb!?-!$\;\:P[x,y]$\\[1mm]
629$\Gamma\;\:$\verb!?-!$\;\:\forall x$\verb!.!$\;P[x,x]$\\[1mm]
630$\Gamma\;{\cup}\;\{P[x,z],\:P[z,y]\}\;\:$\verb!?-!$\;\:P[x,y]$
631\end{tabular}
632
633\bigskip
634
635\noindent This tactic implements the induction scheme described above in
636section~\ref{rule-ind}. It reduces the goal of proving that a property $P[x,y]$
637holds for all pairs $x$ and $y$ related by $\hbox{\verb!Rtc!}\;R$ to showing
638that this property is preserved by the rules that inductively define this
639relation.
640
641\subsection{An example}
642
643The following session shows how the rule induction tactic for \verb!Rtc!
644constructed in the previous section can be used to prove a simple theorem about
645this relation.  The aim is to show that the reflexive-transitive closure of a
646symmetric relation is also symmetric.  The proof begins by using the {\small
647HOL} subgoal package (see~\cite{description}) to set up an appropriate goal to
648be proved:
649
650\smallskip
651
652\begin{session}\begin{alltt}
653#set_goal
654   (["\(\forall\,\)x:*. \(\forall\,\)y. R x y \(\supset\) R y x"],
655     "\(\forall\,\)x:*. \(\forall\,\)y. Rtc R x y \(\supset\) Rtc R y x");;
656"\(\forall\,\)x y. Rtc R x y \(\supset\) Rtc R y x"
657    [ "\(\forall\,\)x y. R x y \(\supset\) R y x" ]
658
659() : void
660\end{alltt}\end{session}
661
662\smallskip
663
664\noindent The assumption of the goal is that the relation \verb!R! is
665symmetric, and the conclusion states that the closure \verb!Rtc R! is also
666symmetric.  The conclusion of the goal is in precisely the right form for a
667proof by rule induction using the induction tactic described above.  Applying
668this tactic results in:
669
670\smallskip
671
672\begin{session}\begin{alltt}
673#expand Rtc_INDUCT_TAC;;
674OK..
6753 subgoals
676"Rtc R y x"                       {\rm({\it{subgoal 1\/}})}
677    [ "\(\forall\,\)x y. R x y \(\supset\) R y x" ]
678    [ "Rtc R z x" ]
679    [ "Rtc R y z" ]
680
681"\(\forall\,\)x. Rtc R x x"                   \(\!\){\rm({\it{subgoal 2\/}})}
682    [ "\(\forall\,\)x y. R x y \(\supset\) R y x" ]
683
684"Rtc R y x"                       {\rm({\it{subgoal 3\/}})}
685    [ "\(\forall\,\)x y. R x y \(\supset\) R y x" ]
686    [ "R x y" ]
687
688() : void
689\end{alltt}\end{session}
690
691\smallskip
692
693\noindent Subgoals 1 and 2 are trivial, since the relation \verb!Rtc R! is
694transitive and reflexive by definition. The tactic proofs for these subgoals
695can simply use the rules shown above in box~4. The proof of subgoal 3 is also
696easy. The proposition \verb!"R y x"! follows immediately from the two
697assumptions of the subgoal; and this proposition \mbox{together} with the fact
698that
699
700\bigskip
701
702\noindent\hskip\mathindent$\vdash\forall\,$\verb!R x y. R x y !$\supset
703$\verb! Rtc R x y!
704
705\bigskip
706
707\noindent directly entail the required conclusion.
708
709The proof sketched above is a trivial example of the kind of reasoning
710sometimes referred to as induction over the structure (or the depth) of
711derivations in a deductive system stated by a set of rules.  This form of
712inductive \mbox{argument}, which is very common in certain \mbox{areas} of
713theory (for example, operational semantics and process algebras), is made
714directly accessible in {\small HOL} by the tactic described in this section.
715
716\section{Tactics and inference rules}
717
718In addition to the rule induction tactic described above, the inductive
719definitions package also provides mechanized support for generating tactics
720from the theorems that state the rules for an inductively-defined relation.
721This takes the form of an {\small ML} function:
722
723\medskip
724
725\noindent\hskip\mathindent\verb!RULE_TAC : thm -> tactic!
726
727\medskip
728
729\noindent The theorem argument to this function is expected to be a rule
730expressed in the form proved by the derived principle of inductive definition
731described in section~\ref{newind}. Given such a theorem, \verb!RULE_TAC!
732constructs a tactic that inverts the rule stated by it.  The resulting tactic
733reduces goals that match the conclusion of the rule to subgoals consisting of
734the corresponding instances of its premisses and side conditions.
735
736Consider, for example, the theorem which states the transitivity rule for
737\verb!Rtc!:
738
739\[\vdash \forall\,\hbox{\verb!R x y. !}\begin{array}[t]{@{}l}%
740\hbox{\verb!(!}\exists\,
741\hbox{\verb!z. Rtc R x z !}\wedge\hbox{\verb! Rtc R z y)!}\\
742\quad \supset \\
743\hbox{\verb!Rtc R x y!}
744\end{array} \]
745
746\noindent When applied to this theorem, the function \verb!RULE_TAC! returns
747the tactic described by:
748
749\bigskip
750
751\noindent\begin{tabular}{@{\hskip\mathindent}c@{}}
752$\Gamma\;\:$\verb!?-!$\;\:$\verb!Rtc!$\;R\;x\;y$ \\
753\trule{62mm}\\
754$\Gamma\;\:$\verb!?-!$\;\:\exists z
755$\verb!.!$\;$\verb!Rtc!$\;R\;x\;z\;\:\wedge\;\;$\verb!Rtc!$\;R\;z\;y$
756\end{tabular}
757
758\bigskip
759
760\noindent This tactic can then be used in goal-directed proofs about membership
761in the inductively-defined relation {\verb!Rtc!$\;R$}.  The other two rules
762that define \verb!Rtc!$\;R$ can also be converted into tactics using the
763function \verb!RULE_TAC!.  The result is a complete set of {\small HOL} tactics
764for goal-directed proofs in the deductive system comprising the three rules
765that define reflexive-transitive closure.
766
767It is intended that the inductive definitions package will also include a
768function that maps rules stated as theorems to forward inference rules in
769{\small HOL} (i.e.\ to {\small ML} functions).  For example, the transitivity
770theorem shown above can be used to implement the following derived
771inference rule:
772
773\bigskip
774
775\noindent\begin{tabular}{@{\hskip\mathindent}c@{}}
776$\Gamma_1\;{\vdash}\;$\verb!Rtc!$\;R\;x\;z$\qquad
777$\Gamma_2\;{\vdash}\;$\verb!Rtc!$\;R\;z\;y$\\
778\rrule{62mm}\\
779$\Gamma_1 \cup \Gamma_2\;{\vdash}\;$\verb!Rtc!$\;R\;x\;y$
780\end{tabular}
781
782\bigskip
783
784\noindent Any rule expressed as a theorem of the form proved by the derived
785principle of inductive definitions can likewise be converted into a forward
786inference rule.  A function that \mbox{automatically} constructs such rules has
787not yet been implemented, partly because it has not been found necessary for
788the applications done so far (see section~\ref{appl}).  For completeness,
789however, the author intends in future to add this function to the inductive
790definitions package.
791
792\section{Case analysis}
793
794The final major component of the {\small HOL} package for inductive definitions
795is an {\small ML} function that proves an \mbox{exhaustive} case analysis
796theorem for any given relation inductively defined by a set of rules.  The name
797and type of this function are:
798
799\medskip
800
801\noindent\hskip\mathindent\verb!derive_cases_thm : (thm list # thm) -> thm!
802
803\medskip
804
805\noindent The arguments to this function are the list of rules satisfied by an
806inductively defined relation, together with its rule induction theorem. (These
807are precisely the defining theorems which are proved and returned by
808\verb!new_inductive_definition!.)  When supplied with these theorems,
809\verb!derive_cases_thm! proves that if an assertion of membership in the
810relation holds, then it holds only by virtue of the fact that one of the rules
811can be used to derive it.  This allows one to drive the rules that define a
812relation `backwards', inferring from the conclusion of one of the rules that
813the premisses and side conditions hold.
814
815The following interaction with the {\small HOL} system shows the theorem proved
816by \verb!derive_cases_thm! for the \verb!Rtc! example introduced above.  The
817{\small ML} variables \verb!rules! and \verb!ind! are assumed to have the
818bindings shown above in box~4.
819
820\smallskip
821
822\begin{session}\begin{alltt}
823#derive_cases_thm (rules,ind);;
824\(\vdash\) \(\forall\,\)R x y.
825    Rtc R x y \(\supset\)
826      R x y   \(\vee\)
827      (y = x) \(\vee\)
828      (\(\exists\,\)z. Rtc R x z \(\wedge\) Rtc R z y)
829\end{alltt}\end{session}
830
831\smallskip
832
833\noindent Roughly speaking, the resulting theorem states that if
834\verb!Rtc R x y! holds, then either:
835
836\begin{itemize}
837
838\item it is derivable by the inclusion rule {{\small\bf R}\bf 1}, in which
839case \verb!x! and \verb!y! are related by \verb!R!; or
840
841\item it is derivable by the reflexivity rule {{\small\bf R}\bf 2}, in which
842case \verb!x! and \verb!y! are equal; or
843
844\item it is derivable by the transitivity rule {{\small\bf R}\bf 3}, in which
845case there must be an intermediate value \verb!z! such that \verb!Rtc R x z!
846and \verb!Rtc R z y!.
847
848\end{itemize}
849
850\noindent A similar theorem can be proved automatically for any relation
851defined inductively using the package. Work is currently underway to strengthen
852this theorem from an implication to an equation, so that it can be used for
853rewriting.
854
855\section{Applications}\label{appl}
856
857In a joint project with Juanito Camilleri, a set of example proofs has
858been developed to illustrate the potential for applications of the inductive
859\mbox{definitions} package.  These examples include: the definition of an
860operational semantics for a simple programming language and a proof that its
861evaluation relation is \mbox{deterministic}; the definition of a reduction
862relation for combinatory logic and a proof that it has the Church-Rosser
863property; a definition of \mbox{provability} in a Hilbert style proof system
864for minimal intuitionistic logic; the definition of a type system for
865combinatory logic and a proof of the Curry-Howard isomorphism for typed
866combinatory logic and minimal intuitionistic logic; and definitions of the
867trace and transition semantics for a simple process algebra, \mbox{together}
868with the proof of a formal statement of the relationship between them. A report
869on this work is in preparation, and the {\small HOL} source code for the
870examples will be made available to interested users.
871
872\newpage
873
874\begin{thebibliography}{9}
875
876\bibitem{description}
877DSTO, The University of Cambridge, and SRI
878\mbox{International}, {\it The HOL System: DESCRIPTION} (1991).
879
880\bibitem{melham}
881T.\ F.\ Melham, `Automating Recursive Type Definitions
882in Higher Order Logic',
883in: {\it Current Trends in Hardware Verification and
884Automated Theorem Proving\/}, edited by G.\ Birtwistle
885and P.A.\ Subrahmanyam
886(Springer-Verlag, 1989), pp.\ 341--386.
887
888\bibitem{pitts}
889A.\ M.\ Pitts, `Semantics of Programming Languages',
890unpublished lecture notes, University of Cambridge Computer Laboratory
891(October 1989).
892
893\bibitem{winskel}
894G.\ Winskel, `Introduction to the Formal Semantics of
895Programming Languages', unpublished lecture notes, University of Cambridge
896Computer Laboratory (October 1985).
897
898\end{thebibliography}
899
900\end{document}
901