summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

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. \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}