cases/induct: tuned handling of facts ('consumes');
Thu, 30 Nov 2000 20:04:49 +0100
changeset 10549 5e19ae8d9582
parent 10548 e8c774c12105
child 10550 93ca45370c59
cases/induct: tuned handling of facts ('consumes');
--- a/doc-src/IsarRef/hol.tex	Thu Nov 30 20:04:16 2000 +0100
+++ b/doc-src/IsarRef/hol.tex	Thu Nov 30 20:04:49 2000 +0100
@@ -208,7 +208,7 @@
-\section{(Co)Inductive sets}
+\section{(Co)Inductive sets}\label{sec:inductive}
@@ -367,8 +367,24 @@
 $\vec\phi$.  Also note that local definitions may be expressed as $\All{\vec
   x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.
-\subsection{Declaring rules}
+Facts presented to either method are consumed according to the number of
+``major premises'' of the rule involved (see also \S\ref{sec:induct-att} and
+\S\ref{sec:cases}), which is usually $0$ for plain cases and induction rules
+of datatypes etc.\ and $1$ for rules of inductive sets and the like.  The
+remaining facts are inserted into the goal verbatim before the actual $cases$
+or $induct$ rule is applied (thus facts may be even passed through an
+Note that whenever facts are present, the default rule selection scheme would
+provide a ``set'' rule only, with the first fact consumed and the rest
+inserted into the goal.  In order to pass all facts into a ``type'' rule
+instead, one would have to specify this explicitly, e.g.\ by appending
+``$type: name$'' to the method argument.
+\subsection{Declaring rules}\label{sec:induct-att}
@@ -394,6 +410,10 @@
 Refer to the $case_names$ and $params$ attributes (see \S\ref{sec:cases}) to
 adjust names of cases and parameters of a rule.
+The $consumes$ declaration (cf.\ \S\ref{sec:cases}) is taken care of
+automatically (if none had been given already): $consumes~0$ is specified for
+``type'' rules and $consumes~1$ for ``set'' rules.
 \subsection{Emulating tactic scripts}\label{sec:induct_tac}