
diff -r cb64368fb405 -r fc9bd420162c doc-src/IsarRef/generic.tex
--- 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"




