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