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.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"

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.46 -about large specifications. 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.92 - stemming from parameterized inductive definitions (see also 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"