IndDef/Manual/paper.tex

15 to appear in the Proceedings of the 1991 International Tutorial
46 definitional\/} approach to using higher order logic. That is, the syntax of
47 the logic is extended with new notation not simply by postulating axioms to
48 give meaning to it, but rather by defining it in terms of existing expressions
50 approach, as opposed to the axiomatic method, is that each of the primitive
52 constant specification, and type definition---is guaranteed to preserve
59 The {\small ML} metalanguage allows users to implement derived inference rules
74 introduction to the class of inductive definitions handled by the package and
84 closure of $R$ can be defined to be the least relation $R^{*} \subseteq A
103 therefore simply be {\it defined\/} to be the least relation that satisfies
108 defined to be the {\it least\/} such relation.  This means that $R^{*}$
110 satisfying the rules. As will be discussed below, this property gives rise to
121 defined to be the intersection of all such relations.
153 by a set of rules, and suppose we wish to show that every element in $R$ has a
168 \noindent Then to prove the desired property of $R$, it suffices to show that
175 stated 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:
189 the `base cases' corresponding to rules {{\small\bf R}\bf 1} and {{\small\bf
201 straightforward to express this concept in logic.
206 but we shall continue to speak loosely of a pair of values $x$ and $y$ as being
234 \alpha{\rightarrow}\alpha{\rightarrow}bool$ to its reflexive-transitive closure
250 for reflexive-transitive closure. That is, ${\sf Rtc}\;R$ is \mbox{defined} to
258 Any relation intended to be defined inductively by a set of rules can be
263 of inductive definition are, first of all, to show that the resulting relation
264 in fact does satisfy these rules, and secondly to show that it is indeed the
269 obligation is to show that:
282 section.  The second proof obligation is to show that ${\sf Rtc}\;R$ is the
309 constant specification) to name this relation.  The result is a set of theorems
329 \noindent The first argument to this function is a boolean flag which indicates
330 if the constant that is defined is to have infix syntactic status.  The second
333 needed because this {\small ML} function can be used to define classes of
355 \noindent is a variable representing the $n$-place relation that is to be
362 to denote this relation using a constant specification, the result of which is
372 \verb!new_inductive_definition! can be used to inductively define the set of
393 \verb!n+2! is also even.  (Antiquotation and {\small ML} comments are used to
401 the constant to be defined, namely \verb!Even!, is a one-place
412 \verb!Even! to denote this predicate.  The following automatically-proved
425 \noindent The theorems bound to the {\small ML} identifier \verb!rules! state
427 induction theorem bound to \verb!ind! states that the set of numbers for which
433 also be used to define a parameterized class of relations.
439 relation $R$ to an inductively-defined relation ${\sf Rtc}\;R$.  The function
444 \verb!new_inductive_definition! in order to handle the definition of such
453 curried function that is to be defined (in this case, $R$) to $n$ distinct
455 variables that occur at the positions in this application which correspond to
456 the parameters of class of inductively-defined relations, rather than to the
457 actual arguments to these relations.
492 \verb!Rtc! is to take three arguments in total---a \mbox{relation} \verb!R!,
495 \verb!R! is to be a parameter to the class of inductively-defined relations
497 \verb!y! are assumed to indicate the positions of actual arguments to the
519 \noindent Here, the {\small ML} variable \verb!rules! has been bound to a list
527 In addition to the use of the pattern argument, the \verb!Rtc! example also
529 rules must be supplied to \verb!new_inductive_definition!.  As was mentioned
539 \noindent where $R$ is a variable that stands for the function to be defined.
542 occur at \mbox{positions} which, according to the supplied pattern,
543 \mbox{correspond} to the parameters of a class of relations.  In particular,
547 The rules for reflexive-transitive closure shown in box 3 conform to
551 parameter to the class of relations to be defined.  Every premiss and
561 in addition to the derived rule of definition itself.  The most important of
577 \noindent The first argument to this function is the rule \mbox{induction}
582 or side conditions, and the user may wish to treat these two kinds of induction
584 supplied as the second and third arguments to the function
594 \noindent to the subgoal(s) of proving that the property $P$ is preserved by
620 rules are to be added to the assumptions of the subgoals that are generated.
637 holds for all pairs $x$ and $y$ related by $\hbox{\verb!Rtc!}\;R$ to showing
644 constructed in the previous section can be used to prove a simple theorem about
645 this relation.  The aim is to show that the reflexive-transitive closure of a
647 HOL} subgoal package (see~\cite{description}) to set up an appropriate goal to
710 sometimes referred to as induction over the structure (or the depth) of
718 In addition to the rule induction tactic described above, the inductive
729 \noindent The theorem argument to this function is expected to be a rule
733 reduces goals that match the conclusion of the rule to subgoals consisting of
746 \noindent When applied to this theorem, the function \verb!RULE_TAC! returns
768 function that maps rules stated as theorems to forward inference rules in
769 {\small HOL} (i.e.\ to {\small ML} functions).  For example, the transitivity
770 theorem shown above can be used to implement the following derived
789 however, the author intends in future to add this function to the inductive
805 \noindent The arguments to this function are the list of rules satisfied by an
811 can be used to derive it.  This allows one to drive the rules that define a
817 {\small ML} variables \verb!rules! and \verb!ind! are assumed to have the
851 defined inductively using the package. Work is currently underway to strengthen
852 this theorem from an implication to an equation, so that it can be used for
858 been developed to illustrate the potential for applications of the inductive
870 examples will be made available to interested users.
894 G.\ Winskel, `Introduction to the Formal Semantics of