doc-src/IsarRef/generic.tex
changeset 11691 fc9bd420162c
parent 11469 57b072f00626
child 12618 43a97a2155d0
     1.1 --- a/doc-src/IsarRef/generic.tex	Thu Oct 04 16:07:43 2001 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Thu Oct 04 16:09:12 2001 +0200
     1.3 @@ -854,6 +854,182 @@
     1.4  \end{descr}
     1.5  
     1.6  
     1.7 +\section{Proof by cases and induction}\label{sec:induct-method}
     1.8 +
     1.9 +\subsection{Proof methods}\label{sec:induct-method-proper}
    1.10 +
    1.11 +\indexisarmeth{cases}\indexisarmeth{induct}
    1.12 +\begin{matharray}{rcl}
    1.13 +  cases & : & \isarmeth \\
    1.14 +  induct & : & \isarmeth \\
    1.15 +\end{matharray}
    1.16 +
    1.17 +The $cases$ and $induct$ methods provide a uniform interface to case analysis
    1.18 +and induction over datatypes, inductive sets, and recursive functions.  The
    1.19 +corresponding rules may be specified and instantiated in a casual manner.
    1.20 +Furthermore, these methods provide named local contexts that may be invoked
    1.21 +via the $\CASENAME$ proof command within the subsequent proof text (cf.\ 
    1.22 +\S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning
    1.23 +about large specifications.
    1.24 +
    1.25 +Note that the full spectrum of this generic functionality is currently only
    1.26 +supported by Isabelle/HOL, when used in conjunction with advanced definitional
    1.27 +packages (see especially \S\ref{sec:datatype} and \S\ref{sec:inductive}).
    1.28 +
    1.29 +\begin{rail}
    1.30 +  'cases' spec
    1.31 +  ;
    1.32 +  'induct' spec
    1.33 +  ;
    1.34 +
    1.35 +  spec: open? args rule? params?
    1.36 +  ;
    1.37 +  open: '(' 'open' ')'
    1.38 +  ;
    1.39 +  args: (insts * 'and') 
    1.40 +  ;
    1.41 +  rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
    1.42 +  ;
    1.43 +  params: 'of' ':' insts
    1.44 +  ;
    1.45 +\end{rail}
    1.46 +
    1.47 +\begin{descr}
    1.48 +\item [$cases~insts~R~ps$] applies method $rule$ with an appropriate case
    1.49 +  distinction theorem, instantiated to the subjects $insts$.  Symbolic case
    1.50 +  names are bound according to the rule's local contexts.
    1.51 +  
    1.52 +  The rule is determined as follows, according to the facts and arguments
    1.53 +  passed to the $cases$ method:
    1.54 +  \begin{matharray}{llll}
    1.55 +    \Text{facts}    &       & \Text{arguments} & \Text{rule} \\\hline
    1.56 +                    & cases &           & \Text{classical case split} \\
    1.57 +                    & cases & t         & \Text{datatype exhaustion (type of $t$)} \\
    1.58 +    \edrv a \in A   & cases & \dots     & \Text{inductive set elimination (of $A$)} \\
    1.59 +    \dots           & cases & \dots ~ R & \Text{explicit rule $R$} \\
    1.60 +  \end{matharray}
    1.61 +  
    1.62 +  Several instantiations may be given, referring to the \emph{suffix} of
    1.63 +  premises of the case rule; within each premise, the \emph{prefix} of
    1.64 +  variables is instantiated.  In most situations, only a single term needs to
    1.65 +  be specified; this refers to the first variable of the last premise (it is
    1.66 +  usually the same for all cases).
    1.67 +  
    1.68 +  Additional parameters may be specified as $ps$; these are applied after the
    1.69 +  primary instantiation in the same manner as by the $of$ attribute (cf.\ 
    1.70 +  \S\ref{sec:pure-meth-att}).  This feature is rarely needed in practice; a
    1.71 +  typical application would be to specify additional arguments for rules
    1.72 +  stemming from parameterized inductive definitions (see also
    1.73 +  \S\ref{sec:inductive}).
    1.74 +  
    1.75 +  The $open$ option causes the parameters of the new local contexts to be
    1.76 +  exposed to the current proof context.  Thus local variables stemming from
    1.77 +  distant parts of the theory development may be introduced in an implicit
    1.78 +  manner, which can be quite confusing to the reader.  Furthermore, this
    1.79 +  option may cause unwanted hiding of existing local variables, resulting in
    1.80 +  less robust proof texts.
    1.81 +  
    1.82 +\item [$induct~insts~R~ps$] is analogous to the $cases$ method, but refers to
    1.83 +  induction rules, which are determined as follows:
    1.84 +  \begin{matharray}{llll}
    1.85 +    \Text{facts}    &        & \Text{arguments} & \Text{rule} \\\hline
    1.86 +                    & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\
    1.87 +    \edrv x \in A   & induct & \dots         & \Text{set induction (of $A$)} \\
    1.88 +    \dots           & induct & \dots ~ R     & \Text{explicit rule $R$} \\
    1.89 +  \end{matharray}
    1.90 +  
    1.91 +  Several instantiations may be given, each referring to some part of a mutual
    1.92 +  inductive definition or datatype --- only related partial induction rules
    1.93 +  may be used together, though.  Any of the lists of terms $P, x, \dots$
    1.94 +  refers to the \emph{suffix} of variables present in the induction rule.
    1.95 +  This enables the writer to specify only induction variables, or both
    1.96 +  predicates and variables, for example.
    1.97 +  
    1.98 +  Additional parameters (including the $open$ option) may be given in the same
    1.99 +  way as for $cases$, see above.
   1.100 +\end{descr}
   1.101 +
   1.102 +Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
   1.103 +determined by the instantiated rule \emph{before} it has been applied to the
   1.104 +internal proof state.\footnote{As a general principle, Isar proof text may
   1.105 +  never refer to parts of proof states directly.} Thus proper use of symbolic
   1.106 +cases usually require the rule to be instantiated fully, as far as the
   1.107 +emerging local contexts and subgoals are concerned.  In particular, for
   1.108 +induction both the predicates and variables have to be specified.  Otherwise
   1.109 +the $\CASENAME$ command would refuse to invoke cases containing schematic
   1.110 +variables.  Furthermore the resulting local goal statement is bound to the
   1.111 +term variable $\Var{case}$\indexisarvar{case} --- for each case where it is
   1.112 +fully specified.
   1.113 +
   1.114 +The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named
   1.115 +cases present in the current proof state.
   1.116 +
   1.117 +\medskip
   1.118 +
   1.119 +It is important to note that there is a fundamental difference of the $cases$
   1.120 +and $induct$ methods in handling of non-atomic goal statements: $cases$ just
   1.121 +applies a certain rule in backward fashion, splitting the result into new
   1.122 +goals with the local contexts being augmented in a purely monotonic manner.
   1.123 +
   1.124 +In contrast, $induct$ passes the full goal statement through the ``recursive''
   1.125 +course involved in the induction.  Thus the original statement is basically
   1.126 +replaced by separate copies, corresponding to the induction hypotheses and
   1.127 +conclusion; the original goal context is no longer available.  This behavior
   1.128 +allows \emph{strengthened induction predicates} to be expressed concisely as
   1.129 +meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp \psi$ to
   1.130 +indicate ``variable'' parameters $\vec x$ and ``recursive'' assumptions
   1.131 +$\vec\phi$.  Also note that local definitions may be expressed as $\All{\vec
   1.132 +  x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.
   1.133 +
   1.134 +\medskip
   1.135 +
   1.136 +Facts presented to either method are consumed according to the number of
   1.137 +``major premises'' of the rule involved (see also \S\ref{sec:induct-att} and
   1.138 +\S\ref{sec:cases}), which is usually $0$ for plain cases and induction rules
   1.139 +of datatypes etc.\ and $1$ for rules of inductive sets and the like.  The
   1.140 +remaining facts are inserted into the goal verbatim before the actual $cases$
   1.141 +or $induct$ rule is applied (thus facts may be even passed through an
   1.142 +induction).
   1.143 +
   1.144 +Note that whenever facts are present, the default rule selection scheme would
   1.145 +provide a ``set'' rule only, with the first fact consumed and the rest
   1.146 +inserted into the goal.  In order to pass all facts into a ``type'' rule
   1.147 +instead, one would have to specify this explicitly, e.g.\ by appending
   1.148 +``$type: name$'' to the method argument.
   1.149 +
   1.150 +
   1.151 +\subsection{Declaring rules}\label{sec:induct-att}
   1.152 +
   1.153 +\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}
   1.154 +\begin{matharray}{rcl}
   1.155 +  \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\
   1.156 +  cases & : & \isaratt \\
   1.157 +  induct & : & \isaratt \\
   1.158 +\end{matharray}
   1.159 +
   1.160 +\begin{rail}
   1.161 +  'cases' spec
   1.162 +  ;
   1.163 +  'induct' spec
   1.164 +  ;
   1.165 +
   1.166 +  spec: ('type' | 'set') ':' nameref
   1.167 +  ;
   1.168 +\end{rail}
   1.169 +
   1.170 +The $cases$ and $induct$ attributes augment the corresponding context of rules
   1.171 +for reasoning about inductive sets and types.  The standard rules are already
   1.172 +declared by advanced definitional packages.  For special applications, these
   1.173 +may be replaced manually by variant versions.
   1.174 +
   1.175 +Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:cases}) to
   1.176 +adjust names of cases and parameters of a rule.
   1.177 +
   1.178 +The $consumes$ declaration (cf.\ \S\ref{sec:cases}) is taken care of
   1.179 +automatically (if none had been given already): $consumes~0$ is specified for
   1.180 +``type'' rules and $consumes~1$ for ``set'' rules.
   1.181 +
   1.182 +
   1.183  %%% Local Variables:
   1.184  %%% mode: latex
   1.185  %%% TeX-master: "isar-ref"