IndDef/Manual/paper.tex

63 {\small HOL} logic.  But certain recursive type definitions and function
205  relation on $\alpha$. (Here, a relation is represented by a curried function;
228 function
304 function that takes as an argument a list of rules and automatically proves the
313 The {\small ML} function that implements this principle of inductive definition
329 \noindent The first argument to this function is a boolean flag which indicates
333 needed because this {\small ML} function can be used to define classes of
360 function \verb!new_inductive_definition! automatically proves the existence of
371 The following example {\small HOL} session shows how the function
402 function with typical argument \verb!n!.  In general, the second
438 inductively-defined relation, but rather a function that maps an arbitrary
439 relation $R$ to an inductively-defined relation ${\sf Rtc}\;R$.  The function
453 curried function that is to be defined (in this case, $R$) to $n$ distinct
491 \noindent The first component of this pattern specifies that the function
539 \noindent where $R$ is a variable that stands for the function to be defined.
577 \noindent The first argument to this function is the rule \mbox{induction}
584 supplied as the second and third arguments to the function
588 $R$, the function described above returns a specialized rule induction tactic
721 This takes the form of an {\small ML} function:
729 \noindent The theorem argument to this function is expected to be a rule
746 \noindent When applied to this theorem, the function \verb!RULE_TAC! returns
763 function \verb!RULE_TAC!.  The result is a complete set of {\small HOL} tactics
768 function that maps rules stated as theorems to forward inference rules in
786 inference rule.  A function that \mbox{automatically} constructs such rules has
789 however, the author intends in future to add this function to the inductive
795 is an {\small ML} function that proves an \mbox{exhaustive} case analysis
797 and type of this function are:
805 \noindent The arguments to this function are the list of rules satisfied by an