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"