"induct" method: handle proper rules;
Sun, 12 Nov 2000 14:48:25 +0100
changeset 10456 166fc12ce153
parent 10455 acfdc430f4cd
child 10457 dd669bda2b0c
"induct" method: handle proper rules;
--- 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.
@@ -349,6 +350,23 @@
 The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named
 cases present in the current proof state.
+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}