author wenzelm Thu, 30 Nov 2000 20:04:49 +0100 changeset 10549 5e19ae8d9582 parent 10548 e8c774c12105 child 10550 93ca45370c59
cases/induct: tuned handling of facts ('consumes');
 doc-src/IsarRef/hol.tex file | annotate | diff | comparison | revisions
--- 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 @@
\end{rail}

-\section{(Co)Inductive sets}
+\section{(Co)Inductive sets}\label{sec:inductive}

\indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisaratt{mono}
\begin{matharray}{rcl}
@@ -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$.

+\medskip

-\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
+induction).
+
+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}

\indexisaratt{cases}\indexisaratt{induct}
\begin{matharray}{rcl}
@@ -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}