diff -r 279da0358aa9 -r 09a6c44a48ea doc-src/TutorialI/Misc/document/simp.tex --- a/doc-src/TutorialI/Misc/document/simp.tex Thu Jul 26 18:23:38 2001 +0200 +++ b/doc-src/TutorialI/Misc/document/simp.tex Fri Aug 03 18:04:55 2001 +0200 @@ -6,21 +6,24 @@ } % \begin{isamarkuptext}% -\indexbold{simplification rule} -To facilitate simplification, theorems can be declared to be simplification -rules (by the attribute \isa{{\isacharbrackleft}simp{\isacharbrackright}}\index{*simp - (attribute)}), in which case proofs by simplification make use of these -rules automatically. In addition the constructs \isacommand{datatype} and -\isacommand{primrec} (and a few others) invisibly declare useful -simplification rules. Explicit definitions are \emph{not} declared +\index{simplification rules} +To facilitate simplification, +the attribute \isa{{\isacharbrackleft}simp{\isacharbrackright}}\index{*simp (attribute)} +declares theorems to be simplification rules, which the simplifier +will use automatically. In addition, \isacommand{datatype} and +\isacommand{primrec} declarations (and a few others) +implicitly declare some simplification rules. +Explicit definitions are \emph{not} declared as simplification rules automatically! -Not merely equations but pretty much any theorem can become a simplification -rule. The simplifier will try to make sense of it. For example, a theorem -\isa{{\isasymnot}\ P} is automatically turned into \isa{P\ {\isacharequal}\ False}. The details +Nearly any theorem can become a simplification +rule. The simplifier will try to transform it into an equation. +For example, the theorem +\isa{{\isasymnot}\ P} is turned into \isa{P\ {\isacharequal}\ False}. The details are explained in \S\ref{sec:SimpHow}. -The simplification attribute of theorems can be turned on and off as follows: +The simplification attribute of theorems can be turned on and off:% +\index{*simp del (attribute)}\REMARK{need to index attributes!switching off??} \begin{quote} \isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp{\isacharbrackright}}\\ \isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp\ del{\isacharbrackright}} @@ -36,14 +39,14 @@ need to be disabled in certain proofs. Frequent changes in the simplification status of a theorem may indicate an unwise use of defaults. \begin{warn} - Simplification may run forever, for example if both $f(x) = g(x)$ and + Simplification can run forever, for example if both $f(x) = g(x)$ and $g(x) = f(x)$ are simplification rules. It is the user's responsibility not to include simplification rules that can lead to nontermination, either on their own or in combination with other simplification rules. \end{warn}% \end{isamarkuptext}% % -\isamarkupsubsection{The Simplification Method% +\isamarkupsubsection{The {\tt\slshape simp} Method% } % \begin{isamarkuptext}% @@ -58,25 +61,25 @@ with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks only the first subgoal and may thus need to be repeated --- use \methdx{simp_all} to simplify all subgoals. -Note that \isa{simp} fails if nothing changes.% +If nothing changes, \isa{simp} fails.% \end{isamarkuptext}% % \isamarkupsubsection{Adding and Deleting Simplification Rules% } % \begin{isamarkuptext}% +\index{simplification rules!adding and deleting}% If a certain theorem is merely needed in a few proofs by simplification, we do not need to make it a global simplification rule. Instead we can modify the set of simplification rules used in a simplification step by adding rules to it and/or deleting rules from it. The two modifiers for this are \begin{quote} -\isa{add{\isacharcolon}} \textit{list of theorem names}\\ -\isa{del{\isacharcolon}} \textit{list of theorem names} +\isa{add{\isacharcolon}} \textit{list of theorem names}\index{*add (modifier)}\\ +\isa{del{\isacharcolon}} \textit{list of theorem names}\index{*del (modifier)} \end{quote} -In case you want to use only a specific list of theorems and ignore all -others: +Or you can use a specific list of theorems and omit all others: \begin{quote} -\isa{only{\isacharcolon}} \textit{list of theorem names} +\isa{only{\isacharcolon}} \textit{list of theorem names}\index{*only (modifier)} \end{quote} In this example, we invoke the simplifier, adding two distributive laws: @@ -102,36 +105,35 @@ simplifies the first assumption to \isa{zs\ {\isacharequal}\ ys}, thus reducing the conclusion to \isa{ys\ {\isacharequal}\ ys} and hence to \isa{True}. -In some cases this may be too much of a good thing and may lead to -nontermination:% +In some cases, using the assumptions can lead to nontermination:% \end{isamarkuptext}% \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent -cannot be solved by an unmodified application of \isa{simp} because the -simplification rule \isa{f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}} extracted from the assumption -does not terminate. Isabelle notices certain simple forms of -nontermination but not this one. The problem can be circumvented by -explicitly telling the simplifier to ignore the assumptions:% +An unmodified application of \isa{simp} loops. The culprit is the +simplification rule \isa{f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}}, which is extracted from +the assumption. (Isabelle notices certain simple forms of +nontermination but not this one.) The problem can be circumvented by +telling the simplifier to ignore the assumptions:% \end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}\isanewline \isacommand{done}% \begin{isamarkuptext}% \noindent -There are three modifiers that influence the treatment of assumptions: +Three modifiers influence the treatment of assumptions: \begin{description} -\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\indexbold{*no_asm} +\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\index{*no_asm (modifier)} means that assumptions are completely ignored. -\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}}]\indexbold{*no_asm_simp} +\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}}]\index{*no_asm_simp (modifier)} means that the assumptions are not simplified but are used in the simplification of the conclusion. -\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}]\indexbold{*no_asm_use} +\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}]\index{*no_asm_use (modifier)} means that the assumptions are simplified but are not used in the simplification of each other or the conclusion. \end{description} Both \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} and \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} run forever on the problematic subgoal above. -Note that only one of the modifiers is allowed, and it must precede all +Only one of the modifiers is allowed, and it must precede all other modifiers. \begin{warn} @@ -150,13 +152,17 @@ % \begin{isamarkuptext}% \label{sec:Simp-with-Defs}\index{simplification!with definitions} -Constant definitions (\S\ref{sec:ConstDefinitions}) can -be used as simplification rules, but by default they are not. Hence the -simplifier does not expand them automatically, just as it should be: -definitions are introduced for the purpose of abbreviating complex -concepts. Of course we need to expand the definitions initially to derive -enough lemmas that characterize the concept sufficiently for us to forget the -original definition. For example, given% +Constant definitions (\S\ref{sec:ConstDefinitions}) can be used as +simplification rules, but by default they are not: the simplifier does not +expand them automatically. Definitions are intended for introducing abstract +concepts and not merely as abbreviations. (Contrast with syntax +translations, \S\ref{sec:def-translations}.) Of course, we need to expand +the definition initially, but once we have proved enough abstract properties +of the new constant, we can forget its original definition. This style makes +proofs more robust: if the definition has to be changed, +only the proofs of the abstract properties will be affected. + +For example, given% \end{isamarkuptext}% \isacommand{constdefs}\ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline \ \ \ \ \ \ \ \ \ {\isachardoublequote}xor\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}% @@ -184,9 +190,6 @@ \noindent Of course we can also unfold definitions in the middle of a proof. -You should normally not turn a definition permanently into a simplification -rule because this defeats the whole purpose. - \begin{warn} If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold occurrences of $f$ with at least two arguments. This may be helpful for unfolding @@ -199,26 +202,27 @@ } % \begin{isamarkuptext}% -\index{simplification!of let-expressions} -Proving a goal containing \sdx{let}-expressions almost invariably -requires the \isa{let}-con\-structs to be expanded at some point. Since -\isa{let}\ldots\isa{=}\ldots\isa{in}{\ldots} is just syntactic sugar for a predefined constant -(called \isa{Let}), expanding \isa{let}-constructs means rewriting with -\isa{Let{\isacharunderscore}def}:% +\index{simplification!of \isa{let}-expressions}\index{*let expressions}% +Proving a goal containing \isa{let}-expressions almost invariably requires the +\isa{let}-con\-structs to be expanded at some point. Since +\isa{let}\ldots\isa{=}\ldots\isa{in}{\ldots} is just syntactic sugar for +the predefined constant \isa{Let}, expanding \isa{let}-constructs +means rewriting with \tdx{Let_def}:% \end{isamarkuptext}% \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}\isanewline \isacommand{done}% \begin{isamarkuptext}% If, in a particular context, there is no danger of a combinatorial explosion -of nested \isa{let}s one could even simlify with \isa{Let{\isacharunderscore}def} by +of nested \isa{let}s, you could even simplify with \isa{Let{\isacharunderscore}def} by default:% \end{isamarkuptext}% \isacommand{declare}\ Let{\isacharunderscore}def\ {\isacharbrackleft}simp{\isacharbrackright}% -\isamarkupsubsection{Conditional Equations% +\isamarkupsubsection{Conditional Simplification Rules% } % \begin{isamarkuptext}% +\index{conditional simplification rules}% So far all examples of rewrite rules were equations. The simplifier also accepts \emph{conditional} equations, for example% \end{isamarkuptext}% @@ -247,14 +251,15 @@ } % \begin{isamarkuptext}% -\label{sec:AutoCaseSplits}\indexbold{case splits}\index{*split (method, attr.)|(} -Goals containing \isa{if}-expressions are usually proved by case -distinction on the condition of the \isa{if}. For example the goal% +\label{sec:AutoCaseSplits}\indexbold{case splits}% +Goals containing \isa{if}-expressions\index{*if expressions!splitting of} +are usually proved by case +distinction on the boolean condition. Here is an example:% \end{isamarkuptext}% \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}xs{\isachardot}\ if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent -can be split by a special method \isa{split}:% +The goal can be split by a special method, \methdx{split}:% \end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}if{\isacharparenright}% \begin{isamarkuptxt}% @@ -264,12 +269,12 @@ \end{isabelle} where \tdx{split_if} is a theorem that expresses splitting of \isa{if}s. Because -case-splitting on \isa{if}s is almost always the right proof strategy, the -simplifier performs it automatically. Try \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} +splitting the \isa{if}s is usually the right proof strategy, the +simplifier does it automatically. Try \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} on the initial goal above. This splitting idea generalizes from \isa{if} to \sdx{case}. -Let us simplify a case analysis over lists:% +Let us simplify a case analysis over lists:\index{*list.split (theorem)}% \end{isamarkuptxt}% \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}split\ list{\isachardot}split{\isacharparenright}% @@ -278,20 +283,22 @@ \ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isacharparenright}\ {\isasymand}\isanewline \isaindent{\ {\isadigit{1}}{\isachardot}\ }{\isacharparenleft}{\isasymforall}a\ list{\isachardot}\ xs\ {\isacharequal}\ a\ {\isacharhash}\ list\ {\isasymlongrightarrow}\ a\ {\isacharhash}\ list\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isacharparenright}% \end{isabelle} -In contrast to \isa{if}-expressions, the simplifier does not split -\isa{case}-expressions by default because this can lead to nontermination -in case of recursive datatypes. Therefore the simplifier has a modifier -\isa{split} for adding further splitting rules explicitly. This means the -above lemma can be proved in one step by% +The simplifier does not split +\isa{case}-expressions, as it does \isa{if}-expressions, +because with recursive datatypes it could lead to nontermination. +Instead, the simplifier has a modifier +\isa{split}\index{*split (modified)} +for adding splitting rules explicitly. The +lemma above can be proved in one step by% \end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}% \begin{isamarkuptext}% \noindent whereas \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} alone will not succeed. -In general, every datatype $t$ comes with a theorem +Every datatype $t$ comes with a theorem $t$\isa{{\isachardot}split} which can be declared to be a \bfindex{split rule} either -locally as above, or by giving it the \isa{split} attribute globally:% +locally as above, or by giving it the \attrdx{split} attribute globally:% \end{isamarkuptext}% \isacommand{declare}\ list{\isachardot}split\ {\isacharbrackleft}split{\isacharbrackright}% \begin{isamarkuptext}% @@ -306,22 +313,23 @@ \end{isamarkuptext}% \isacommand{declare}\ list{\isachardot}split\ {\isacharbrackleft}split\ del{\isacharbrackright}% \begin{isamarkuptext}% -In polished proofs the \isa{split} method is rarely used on its own -but always as part of the simplifier. However, if a goal contains -multiple splittable constructs, the \isa{split} method can be +Polished proofs typically perform splitting within \isa{simp} rather than +invoking the \isa{split} method. However, if a goal contains +several \isa{if} and \isa{case} expressions, +the \isa{split} method can be helpful in selectively exploring the effects of splitting. -The above split rules intentionally only affect the conclusion of a -subgoal. If you want to split an \isa{if} or \isa{case}-expression in -the assumptions, you have to apply \isa{split{\isacharunderscore}if{\isacharunderscore}asm} or +The split rules shown above are intended to affect only the subgoal's +conclusion. If you want to split an \isa{if} or \isa{case}-expression +in the assumptions, you have to apply \tdx{split_if_asm} or $t$\isa{{\isachardot}split{\isacharunderscore}asm}:% \end{isamarkuptext}% \isacommand{lemma}\ {\isachardoublequote}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ else\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}% \begin{isamarkuptxt}% \noindent -In contrast to splitting the conclusion, this actually creates two -separate subgoals (which are solved by \isa{simp{\isacharunderscore}all}): +Unlike splitting the conclusion, this step creates two +separate subgoals, which here can be solved by \isa{simp{\isacharunderscore}all}: \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline \ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}% @@ -331,36 +339,16 @@ $t$\isa{{\isachardot}split{\isacharunderscore}asm}. Analogously, there is \isa{if{\isacharunderscore}splits}. \begin{warn} - The simplifier merely simplifies the condition of an \isa{if} but not the + The simplifier merely simplifies the condition of an + \isa{if}\index{*if expressions!simplification of} but not the \isa{then} or \isa{else} parts. The latter are simplified only after the condition reduces to \isa{True} or \isa{False}, or after splitting. The same is true for \sdx{case}-expressions: only the selector is simplified at first, until either the expression reduces to one of the cases or it is split. -\end{warn}\index{*split (method, attr.)|)}% +\end{warn}% \end{isamarkuptxt}% % -\isamarkupsubsection{Arithmetic% -} -% -\begin{isamarkuptext}% -\index{linear arithmetic} -The simplifier routinely solves a small class of linear arithmetic formulae -(over type \isa{nat} and other numeric types): it only takes into account -assumptions and conclusions that are relations -($=$, $\le$, $<$, possibly negated) and it only knows about addition. Thus% -\end{isamarkuptext}% -\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}% -\begin{isamarkuptext}% -\noindent -is proved by simplification, whereas the only slightly more complex% -\end{isamarkuptext}% -\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}% -\begin{isamarkuptext}% -\noindent -is not proved by simplification and requires \isa{arith}.% -\end{isamarkuptext}% -% \isamarkupsubsection{Tracing% } % @@ -403,9 +391,9 @@ each of the rule's conditions. Many other hints about the simplifier's actions will appear. -In more complicated cases, the trace can be quite lengthy, especially since -invocations of the simplifier are often nested (e.g.\ when solving conditions -of rewrite rules). Thus it is advisable to reset it:% +In more complicated cases, the trace can be quite lengthy. Invocations of the +simplifier are often nested, for instance when solving conditions of rewrite +rules. Thus it is advisable to reset it:% \end{isamarkuptext}% \isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline \end{isabellebody}%