author wenzelm Thu Oct 04 16:09:12 2001 +0200 (2001-10-04) changeset 11691 fc9bd420162c parent 11690 cb64368fb405 child 11692 6d15ae4b1123
induct/cases made generic, removed simplified/stripped options;
 doc-src/IsarRef/generic.tex file | annotate | diff | revisions doc-src/IsarRef/hol.tex file | annotate | diff | revisions
     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.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.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"

     2.1 --- a/doc-src/IsarRef/hol.tex	Thu Oct 04 16:07:43 2001 +0200
2.2 +++ b/doc-src/IsarRef/hol.tex	Thu Oct 04 16:09:12 2001 +0200
2.3 @@ -43,7 +43,7 @@
2.4  \end{descr}
2.5
2.6
2.7 -\section{Primitive types}
2.8 +\section{Primitive types}\label{sec:typedef}
2.9
2.10  \indexisarcmd{typedecl}\indexisarcmd{typedef}
2.11  \begin{matharray}{rcl}
2.12 @@ -140,7 +140,7 @@
2.13  \S\ref{sec:induct_tac}.
2.14
2.15
2.16 -\section{Recursive functions}
2.17 +\section{Recursive functions}\label{sec:recursion}
2.18
2.19  \indexisarcmd{primrec}\indexisarcmd{recdef}\indexisarcmd{recdef-tc}
2.20  \begin{matharray}{rcl}
2.21 @@ -278,190 +278,33 @@
2.22  HOL.
2.23
2.24
2.25 -\section{Proof by cases and induction}\label{sec:induct-method}
2.26 -%FIXME move to generic.tex
2.27 -
2.28 -\subsection{Proof methods}\label{sec:induct-method-proper}
2.29 +\section{Arithmetic}
2.30
2.31 -\indexisarmeth{cases}\indexisarmeth{induct}
2.32 +\indexisarmeth{arith}\indexisaratt{arith-split}
2.33  \begin{matharray}{rcl}
2.34 -  cases & : & \isarmeth \\
2.35 -  induct & : & \isarmeth \\
2.36 +  arith & : & \isarmeth \\
2.37 +  arith_split & : & \isaratt \\
2.38  \end{matharray}
2.39
2.40 -The $cases$ and $induct$ methods provide a uniform interface to case analysis
2.41 -and induction over datatypes, inductive sets, and recursive functions.  The
2.42 -corresponding rules may be specified and instantiated in a casual manner.
2.43 -Furthermore, these methods provide named local contexts that may be invoked
2.44 -via the $\CASENAME$ proof command within the subsequent proof text (cf.\
2.45 -\S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning
2.47 -
2.48  \begin{rail}
2.49 -  'cases' ('(' 'simplified' ')')? spec
2.50 -  ;
2.51 -  'induct' ('(' 'stripped' ')')? spec
2.52 -  ;
2.53 -
2.54 -  spec: open? args rule? params?
2.55 -  ;
2.56 -  open: '(' 'open' ')'
2.57 -  ;
2.58 -  args: (insts * 'and')
2.59 -  ;
2.60 -  rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
2.61 -  ;
2.62 -  params: 'of' ':' insts
2.63 +  'arith' '!'?
2.64    ;
2.65  \end{rail}
2.66
2.67 -\begin{descr}
2.68 -\item [$cases~insts~R~ps$] applies method $rule$ with an appropriate case
2.69 -  distinction theorem, instantiated to the subjects $insts$.  Symbolic case
2.70 -  names are bound according to the rule's local contexts.
2.71 -
2.72 -  The rule is determined as follows, according to the facts and arguments
2.73 -  passed to the $cases$ method:
2.74 -  \begin{matharray}{llll}
2.75 -    \Text{facts}    &       & \Text{arguments} & \Text{rule} \\\hline
2.76 -                    & cases &           & \Text{classical case split} \\
2.77 -                    & cases & t         & \Text{datatype exhaustion (type of $t$)} \\
2.78 -    \edrv a \in A   & cases & \dots     & \Text{inductive set elimination (of $A$)} \\
2.79 -    \dots           & cases & \dots ~ R & \Text{explicit rule $R$} \\
2.80 -  \end{matharray}
2.81 -
2.82 -  Several instantiations may be given, referring to the \emph{suffix} of
2.83 -  premises of the case rule; within each premise, the \emph{prefix} of
2.84 -  variables is instantiated.  In most situations, only a single term needs to
2.85 -  be specified; this refers to the first variable of the last premise (it is
2.86 -  usually the same for all cases).
2.87 -
2.88 -  Additional parameters may be specified as $ps$; these are applied after the
2.89 -  primary instantiation in the same manner as by the $of$ attribute (cf.\
2.90 -  \S\ref{sec:pure-meth-att}).  This feature is rarely needed in practice; a
2.91 -  typical application would be to specify additional arguments for rules
2.93 -  \S\ref{sec:inductive}).
2.94 +The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
2.95 +$real$).  Any current facts are inserted into the goal before running the
2.96 +procedure.  The !''~argument causes the full context of assumptions to be
2.97 +included.  The $arith_split$ attribute declares case split rules to be
2.98 +expanded before the arithmetic procedure is invoked.
2.99
2.100 -  The $simplified$ option causes obvious cases'' of the rule to be solved
2.101 -  beforehand, while the others are left unscathed.
2.102 -
2.103 -  The $open$ option causes the parameters of the new local contexts to be
2.104 -  exposed to the current proof context.  Thus local variables stemming from
2.105 -  distant parts of the theory development may be introduced in an implicit
2.106 -  manner, which can be quite confusing to the reader.  Furthermore, this
2.107 -  option may cause unwanted hiding of existing local variables, resulting in
2.108 -  less robust proof texts.
2.109 -
2.110 -\item [$induct~insts~R~ps$] is analogous to the $cases$ method, but refers to
2.111 -  induction rules, which are determined as follows:
2.112 -  \begin{matharray}{llll}
2.113 -    \Text{facts}    &        & \Text{arguments} & \Text{rule} \\\hline
2.114 -                    & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\
2.115 -    \edrv x \in A   & induct & \dots         & \Text{set induction (of $A$)} \\
2.116 -    \dots           & induct & \dots ~ R     & \Text{explicit rule $R$} \\
2.117 -  \end{matharray}
2.118 -
2.119 -  Several instantiations may be given, each referring to some part of a mutual
2.120 -  inductive definition or datatype --- only related partial induction rules
2.121 -  may be used together, though.  Any of the lists of terms $P, x, \dots$
2.122 -  refers to the \emph{suffix} of variables present in the induction rule.
2.123 -  This enables the writer to specify only induction variables, or both
2.124 -  predicates and variables, for example.
2.125 -
2.126 -  Additional parameters may be given in the same way as for $cases$.
2.127 -
2.128 -  The $stripped$ option causes implications and (bounded) universal
2.129 -  quantifiers to be removed from each new subgoal emerging from the
2.130 -  application of the induction rule.  This accommodates special applications
2.131 -  of strengthened induction predicates''.  This option is rarely needed, the
2.132 -  $induct$ method already handles proper rules appropriately by default.
2.133 -
2.134 -  The $open$ option has the same effect as for the $cases$ method, see above.
2.135 -\end{descr}
2.136 -
2.137 -Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
2.138 -determined by the instantiated rule \emph{before} it has been applied to the
2.139 -internal proof state.\footnote{As a general principle, Isar proof text may
2.140 -  never refer to parts of proof states directly.} Thus proper use of symbolic
2.141 -cases usually require the rule to be instantiated fully, as far as the
2.142 -emerging local contexts and subgoals are concerned.  In particular, for
2.143 -induction both the predicates and variables have to be specified.  Otherwise
2.144 -the $\CASENAME$ command would refuse to invoke cases containing schematic
2.145 -variables.  Furthermore the resulting local goal statement is bound to the
2.146 -term variable $\Var{case}$\indexisarvar{case} --- for each case where it is
2.147 -fully specified.
2.148 -
2.149 -The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named
2.150 -cases present in the current proof state.
2.151 -
2.152 -\medskip
2.153 -
2.154 -It is important to note that there is a fundamental difference of the $cases$
2.155 -and $induct$ methods in handling of non-atomic goal statements: $cases$ just
2.156 -applies a certain rule in backward fashion, splitting the result into new
2.157 -goals with the local contexts being augmented in a purely monotonic manner.
2.158 -
2.159 -In contrast, $induct$ passes the full goal statement through the recursive''
2.160 -course involved in the induction.  Thus the original statement is basically
2.161 -replaced by separate copies, corresponding to the induction hypotheses and
2.162 -conclusion; the original goal context is no longer available.  This behavior
2.163 -allows \emph{strengthened induction predicates} to be expressed concisely as
2.164 -meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp \psi$ to
2.165 -indicate variable'' parameters $\vec x$ and recursive'' assumptions
2.166 -$\vec\phi$.  Also note that local definitions may be expressed as $\All{\vec 2.167 - x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.
2.168 -
2.169 -\medskip
2.170 -
2.171 -Facts presented to either method are consumed according to the number of
2.172 -major premises'' of the rule involved (see also \S\ref{sec:induct-att} and
2.173 -\S\ref{sec:cases}), which is usually $0$ for plain cases and induction rules
2.174 -of datatypes etc.\ and $1$ for rules of inductive sets and the like.  The
2.175 -remaining facts are inserted into the goal verbatim before the actual $cases$
2.176 -or $induct$ rule is applied (thus facts may be even passed through an
2.177 -induction).
2.178 -
2.179 -Note that whenever facts are present, the default rule selection scheme would
2.180 -provide a set'' rule only, with the first fact consumed and the rest
2.181 -inserted into the goal.  In order to pass all facts into a type'' rule
2.182 -instead, one would have to specify this explicitly, e.g.\ by appending
2.183 -$type: name$'' to the method argument.
2.184 +Note that a simpler (but faster) version of arithmetic reasoning is already
2.185 +performed by the Simplifier.
2.186
2.187
2.188 -\subsection{Declaring rules}\label{sec:induct-att}
2.189 -
2.190 -\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}
2.191 -\begin{matharray}{rcl}
2.192 -  \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\
2.193 -  cases & : & \isaratt \\
2.194 -  induct & : & \isaratt \\
2.195 -\end{matharray}
2.196 -
2.197 -\begin{rail}
2.198 -  'cases' spec
2.199 -  ;
2.200 -  'induct' spec
2.201 -  ;
2.202 +\section{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}
2.203
2.204 -  spec: ('type' | 'set') ':' nameref
2.205 -  ;
2.206 -\end{rail}
2.207 -
2.208 -The $cases$ and $induct$ attributes augment the corresponding context of rules
2.209 -for reasoning about inductive sets and types.  The standard rules are already
2.210 -declared by HOL definitional packages.  For special applications, these may be
2.211 -replaced manually by variant versions.
2.212 -
2.213 -Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:cases}) to
2.214 -adjust names of cases and parameters of a rule.
2.215 -
2.216 -The $consumes$ declaration (cf.\ \S\ref{sec:cases}) is taken care of
2.217 -automatically (if none had been given already): $consumes~0$ is specified for
2.218 -type'' rules and $consumes~1$ for set'' rules.
2.219 -
2.220 -
2.221 -\subsection{Emulating tactic scripts}\label{sec:induct_tac}
2.222 +The following important tactical tools of Isabelle/HOL have been ported to
2.223 +Isar.  These should be never used in proper proof texts!
2.224
2.225  \indexisarmeth{case-tac}\indexisarmeth{induct-tac}
2.226  \indexisarmeth{ind-cases}\indexisarcmd{inductive-cases}
2.227 @@ -510,9 +353,7 @@
2.228
2.229  \item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
2.230    to the \texttt{mk_cases} operation.  Rules are simplified in an unrestricted
2.231 -  forward manner, unlike the proper $cases$ method (see
2.232 -  \S\ref{sec:induct-method-proper}) which requires simplified cases to be
2.233 -  solved completely.
2.234 +  forward manner.
2.235
2.236    While $ind_cases$ is a proof method to apply the result immediately as
2.237    elimination rules, $\isarkeyword{inductive_cases}$ provides case split
2.238 @@ -520,29 +361,6 @@
2.239  \end{descr}
2.240
2.241
2.242 -\section{Arithmetic}
2.243 -
2.244 -\indexisarmeth{arith}\indexisaratt{arith-split}
2.245 -\begin{matharray}{rcl}
2.246 -  arith & : & \isarmeth \\
2.247 -  arith_split & : & \isaratt \\
2.248 -\end{matharray}
2.249 -
2.250 -\begin{rail}
2.251 -  'arith' '!'?
2.252 -  ;
2.253 -\end{rail}
2.254 -
2.255 -The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
2.256 -$real$).  Any current facts are inserted into the goal before running the
2.257 -procedure.  The !''~argument causes the full context of assumptions to be
2.258 -included.  The $arith_split$ attribute declares case split rules to be
2.259 -expanded before the arithmetic procedure is invoked.
2.260 -
2.261 -Note that a simpler (but faster) version of arithmetic reasoning is already
2.262 -performed by the Simplifier.
2.263 -
2.264 -
2.265  %%% Local Variables:
2.266  %%% mode: latex
2.267  %%% TeX-master: "isar-ref"