doc-src/IsarRef/hol.tex
 changeset 7507 e70255cb1035 parent 7466 7df66ce6508a child 7987 d9aef93c0e32
equal inserted replaced
7506:08a88d4ebd54 7507:e70255cb1035
   156 \begin{matharray}{rcl}
   156 \begin{matharray}{rcl}
   157   induct & : & \isarmeth \\
   157   induct & : & \isarmeth \\
   158 \end{matharray}
   158 \end{matharray}
   159
   159
   160 The $induct$ method provides a uniform interface to induction over datatypes,
   160 The $induct$ method provides a uniform interface to induction over datatypes,
   161 inductive sets, and recursive functions.  Basically, it is just an interface
   161 inductive sets, recursive functions etc.  Basically, it is just an interface
   162 to the $rule$ method applied to appropriate instances of the corresponding
   162 to the $rule$ method applied to appropriate instances of the corresponding
   163 induction rules.
   163 induction rules.
   164
   164
   165 \begin{rail}
   165 \begin{rail}
   166   'induct' (inst * 'and') kind?
   166   'induct' (inst * 'and') kind?
   167   ;
   167   ;
   168
   168
   169   inst: term term?
   169   inst: term term?
   170   ;
   170   ;
   171   kind: ('type' | 'set' | 'function') ':' nameref
   171   kind: ('type' | 'set' | 'function' | 'rule') ':' nameref
   172   ;
   172   ;
   173 \end{rail}
   173 \end{rail}
   174
   174
   175 \begin{descr}
   175 \begin{descr}
   176 \item [$induct~insts~kind$] abbreviates method $rule~R$, where $R$ is the
   176 \item [$induct~insts~kind$] abbreviates method $rule~R$, where $R$ is the
   177   induction rule of the type~/ set~/ function specified by $kind$ and
   177   induction rule specified by $kind$ and instantiated by $insts$.  The rule is
   178   instantiated by $insts$.  The latter either consists of pairs $P$ $x$
   178   either that of some type, set, or recursive function (defined via TFL), or
   179   (induction predicate and variable), where $P$ is optional.  If $kind$ is
   179   given explicitly.

   180

   181   The instantiation basically consists of a list of $P$ $x$ (induction

   182   predicate and variable) specifications, where $P$ is optional.  If $kind$ is
   180   omitted, the default is to pick a datatype induction rule according to the
   183   omitted, the default is to pick a datatype induction rule according to the
   181   type of some induction variable, which may not be omitted that case.
   184   type of some induction variable, which may not be omitted that case.
   182 \end{descr}
   185 \end{descr}
   183
   186
   184
   187