doc-src/IsarRef/hol.tex
changeset 7507 e70255cb1035
parent 7466 7df66ce6508a
child 7987 d9aef93c0e32
equal deleted 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