# HG changeset patch
# User wenzelm
# Date 974036905 -3600
# Node ID 166fc12ce153117ede9cb5171aef65b4a6df31f8
# Parent  acfdc430f4cd9ef9b2d3c30cd06bc5b036df04d8
"induct" method: handle proper rules;

diff -r acfdc430f4cd -r 166fc12ce153 doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Sun Nov 12 14:46:16 2000 +0100
+++ b/doc-src/IsarRef/hol.tex	Sun Nov 12 14:48:25 2000 +0100
@@ -330,8 +330,9 @@
   
   The $stripped$ option causes implications and (bounded) universal
   quantifiers to be removed from each new subgoal emerging from the
-  application of the induction rule.  This accommodates typical
-  ``strengthening of induction'' predicates.
+  application of the induction rule.  This accommodates special applications
+  of ``strengthened induction predicates''.  This option is rarely needed, the
+  $induct$ method already handles proper rules appropriately by default.
   
   The $open$ option has the same effect as for the $cases$ method, see above.
 \end{descr}
@@ -349,6 +350,23 @@
 The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named
 cases present in the current proof state.
 
+\medskip
+
+It is important to note that there is a fundamental difference of the $cases$
+and $induct$ methods in handling of non-atomic goal statements: $cases$ just
+applies a certain rule in backward fashion, splitting the result into new
+goals with the local contexts being augmented in a purely monotonic manner.
+
+In contrast, $induct$ passes the full goal statement through the ``recursive''
+course involved in the induction.  Thus the original statement is basically
+replaced by separate copies, corresponding to the induction hypotheses and
+conclusion; the original goal context is no longer available.  This behavior
+allows \emph{strengthened induction predicates} to be expressed concisely as
+meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp \psi$ to
+indicate ``variable'' parameters $\vec x$ and ``recursive'' assumptions
+$\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}