--- a/doc-src/IsarRef/generic.tex Thu Oct 04 16:07:43 2001 +0200
+++ b/doc-src/IsarRef/generic.tex Thu Oct 04 16:09:12 2001 +0200
@@ -854,6 +854,182 @@
\end{descr}
+\section{Proof by cases and induction}\label{sec:induct-method}
+
+\subsection{Proof methods}\label{sec:induct-method-proper}
+
+\indexisarmeth{cases}\indexisarmeth{induct}
+\begin{matharray}{rcl}
+ cases & : & \isarmeth \\
+ induct & : & \isarmeth \\
+\end{matharray}
+
+The $cases$ and $induct$ methods provide a uniform interface to case analysis
+and induction over datatypes, inductive sets, and recursive functions. The
+corresponding rules may be specified and instantiated in a casual manner.
+Furthermore, these methods provide named local contexts that may be invoked
+via the $\CASENAME$ proof command within the subsequent proof text (cf.\
+\S\ref{sec:cases}). This accommodates compact proof texts even when reasoning
+about large specifications.
+
+Note that the full spectrum of this generic functionality is currently only
+supported by Isabelle/HOL, when used in conjunction with advanced definitional
+packages (see especially \S\ref{sec:datatype} and \S\ref{sec:inductive}).
+
+\begin{rail}
+ 'cases' spec
+ ;
+ 'induct' spec
+ ;
+
+ spec: open? args rule? params?
+ ;
+ open: '(' 'open' ')'
+ ;
+ args: (insts * 'and')
+ ;
+ rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
+ ;
+ params: 'of' ':' insts
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$cases~insts~R~ps$] applies method $rule$ with an appropriate case
+ distinction theorem, instantiated to the subjects $insts$. Symbolic case
+ names are bound according to the rule's local contexts.
+
+ The rule is determined as follows, according to the facts and arguments
+ passed to the $cases$ method:
+ \begin{matharray}{llll}
+ \Text{facts} & & \Text{arguments} & \Text{rule} \\\hline
+ & cases & & \Text{classical case split} \\
+ & cases & t & \Text{datatype exhaustion (type of $t$)} \\
+ \edrv a \in A & cases & \dots & \Text{inductive set elimination (of $A$)} \\
+ \dots & cases & \dots ~ R & \Text{explicit rule $R$} \\
+ \end{matharray}
+
+ Several instantiations may be given, referring to the \emph{suffix} of
+ premises of the case rule; within each premise, the \emph{prefix} of
+ variables is instantiated. In most situations, only a single term needs to
+ be specified; this refers to the first variable of the last premise (it is
+ usually the same for all cases).
+
+ Additional parameters may be specified as $ps$; these are applied after the
+ primary instantiation in the same manner as by the $of$ attribute (cf.\
+ \S\ref{sec:pure-meth-att}). This feature is rarely needed in practice; a
+ typical application would be to specify additional arguments for rules
+ stemming from parameterized inductive definitions (see also
+ \S\ref{sec:inductive}).
+
+ The $open$ option causes the parameters of the new local contexts to be
+ exposed to the current proof context. Thus local variables stemming from
+ distant parts of the theory development may be introduced in an implicit
+ manner, which can be quite confusing to the reader. Furthermore, this
+ option may cause unwanted hiding of existing local variables, resulting in
+ less robust proof texts.
+
+\item [$induct~insts~R~ps$] is analogous to the $cases$ method, but refers to
+ induction rules, which are determined as follows:
+ \begin{matharray}{llll}
+ \Text{facts} & & \Text{arguments} & \Text{rule} \\\hline
+ & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\
+ \edrv x \in A & induct & \dots & \Text{set induction (of $A$)} \\
+ \dots & induct & \dots ~ R & \Text{explicit rule $R$} \\
+ \end{matharray}
+
+ Several instantiations may be given, each referring to some part of a mutual
+ inductive definition or datatype --- only related partial induction rules
+ may be used together, though. Any of the lists of terms $P, x, \dots$
+ refers to the \emph{suffix} of variables present in the induction rule.
+ This enables the writer to specify only induction variables, or both
+ predicates and variables, for example.
+
+ Additional parameters (including the $open$ option) may be given in the same
+ way as for $cases$, see above.
+\end{descr}
+
+Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
+determined by the instantiated rule \emph{before} it has been applied to the
+internal proof state.\footnote{As a general principle, Isar proof text may
+ never refer to parts of proof states directly.} Thus proper use of symbolic
+cases usually require the rule to be instantiated fully, as far as the
+emerging local contexts and subgoals are concerned. In particular, for
+induction both the predicates and variables have to be specified. Otherwise
+the $\CASENAME$ command would refuse to invoke cases containing schematic
+variables. Furthermore the resulting local goal statement is bound to the
+term variable $\Var{case}$\indexisarvar{case} --- for each case where it is
+fully specified.
+
+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$.
+
+\medskip
+
+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}
+
+\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}
+\begin{matharray}{rcl}
+ \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\
+ cases & : & \isaratt \\
+ induct & : & \isaratt \\
+\end{matharray}
+
+\begin{rail}
+ 'cases' spec
+ ;
+ 'induct' spec
+ ;
+
+ spec: ('type' | 'set') ':' nameref
+ ;
+\end{rail}
+
+The $cases$ and $induct$ attributes augment the corresponding context of rules
+for reasoning about inductive sets and types. The standard rules are already
+declared by advanced definitional packages. For special applications, these
+may be replaced manually by variant versions.
+
+Refer to the $case_names$ and $ps$ 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.
+
+
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "isar-ref"