IndDef/Manual/paper.tex

16 and Workshop on the HOL Theorem Proving System, 27--30 August 1991,
19 {\Large\bf A Package for Inductive Relation Definitions in HOL}\\
33 derived principle of definition in HOL, namely the introduction of relations
45 The HOL user community has a strong tradition of taking a purely {\it
51 rules of definition in the {\small HOL} logic---namely, constant definition,
60 in the {\small HOL} system and thus provides a facility for automating proofs
63 {\small HOL} logic.  But certain recursive type definitions and function
72 principle of definition in {\small HOL} for defining relations inductively by a
235 ${\sf Rtc}\;R$ can be defined in the {\small HOL} logic by the constant
259 defined formally in the {\small HOL} logic by a constant definition of the kind
266 {\small HOL} inference rule described below in section~\ref{newind}.
299 {\small HOL} by the derived inference rule described in the next section.
306 precisely, this derived {\small HOL} inference rule builds a term that denotes
371 The following example {\small HOL} session shows how the function
432 shows how this derived principle of inductive definition in {\small HOL} can
461 {\small HOL}.
500 The result of evaluating this inductive definition in {\small HOL} is the
559 The inductive definitions package in {\small HOL} includes a number of
580 {\small HOL}, the rule induction tactic is parameterized by functions that
647 HOL} subgoal package (see~\cite{description}) to set up an appropriate goal to
714 directly accessible in {\small HOL} by the tactic described in this section.
763 function \verb!RULE_TAC!.  The result is a complete set of {\small HOL} tactics
769 {\small HOL} (i.e.\ to {\small ML} functions).  For example, the transitivity
794 The final major component of the {\small HOL} package for inductive definitions
815 The following interaction with the {\small HOL} system shows the theorem proved
869 on this work is in preparation, and the {\small HOL} source code for the
878 \mbox{International}, {\it The HOL System: DESCRIPTION} (1991).