--- a/doc-src/TutorialI/Misc/simp.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Misc/simp.thy Fri Aug 03 18:04:55 2001 +0200
@@ -4,21 +4,24 @@
subsection{*Simplification Rules*}
-text{*\indexbold{simplification rule}
-To facilitate simplification, theorems can be declared to be simplification
-rules (by the attribute @{text"[simp]"}\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
+text{*\index{simplification rules}
+To facilitate simplification,
+the attribute @{text"[simp]"}\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
-@{prop"~P"} is automatically turned into @{prop"P = 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
+@{prop"~P"} is turned into @{prop"P = 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}@{text"[simp]"}\\
\isacommand{declare} \textit{theorem-name}@{text"[simp del]"}
@@ -34,14 +37,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}
-*}
+*}
-subsection{*The Simplification Method*}
+subsection{*The {\tt\slshape simp} Method*}
text{*\index{*simp (method)|bold}
The general format of the simplification method is
@@ -54,24 +57,24 @@
with @{text simp} instead of \isa{auto}, except that @{text simp} attacks
only the first subgoal and may thus need to be repeated --- use
\methdx{simp_all} to simplify all subgoals.
-Note that @{text simp} fails if nothing changes.
+If nothing changes, @{text simp} fails.
*}
subsection{*Adding and Deleting Simplification Rules*}
text{*
+\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}
-@{text"add:"} \textit{list of theorem names}\\
-@{text"del:"} \textit{list of theorem names}
+@{text"add:"} \textit{list of theorem names}\index{*add (modifier)}\\
+@{text"del:"} \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}
-@{text"only:"} \textit{list of theorem names}
+@{text"only:"} \textit{list of theorem names}\index{*only (modifier)}
\end{quote}
In this example, we invoke the simplifier, adding two distributive
laws:
@@ -96,38 +99,37 @@
simplifies the first assumption to @{term"zs = ys"}, thus reducing the
conclusion to @{term"ys = ys"} and hence to @{term"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:
*}
lemma "\<forall>x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []";
txt{*\noindent
-cannot be solved by an unmodified application of @{text"simp"} because the
-simplification rule @{term"f x = g (f (g x))"} 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 @{text"simp"} loops. The culprit is the
+simplification rule @{term"f x = g (f (g x))"}, 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:
*}
apply(simp (no_asm));
done
text{*\noindent
-There are three modifiers that influence the treatment of assumptions:
+Three modifiers influence the treatment of assumptions:
\begin{description}
-\item[@{text"(no_asm)"}]\indexbold{*no_asm}
+\item[@{text"(no_asm)"}]\index{*no_asm (modifier)}
means that assumptions are completely ignored.
-\item[@{text"(no_asm_simp)"}]\indexbold{*no_asm_simp}
+\item[@{text"(no_asm_simp)"}]\index{*no_asm_simp (modifier)}
means that the assumptions are not simplified but
are used in the simplification of the conclusion.
-\item[@{text"(no_asm_use)"}]\indexbold{*no_asm_use}
+\item[@{text"(no_asm_use)"}]\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 @{text"(no_asm_simp)"} and @{text"(no_asm_use)"} 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}
@@ -144,14 +146,17 @@
subsection{*Rewriting with Definitions*}
text{*\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 *}
constdefs xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
"xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)";
@@ -179,9 +184,6 @@
text{*\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
@@ -192,13 +194,12 @@
subsection{*Simplifying {\tt\slshape let}-Expressions*}
-text{*\index{simplification!of let-expressions}
-Proving a goal containing \sdx{let}-expressions almost invariably
-requires the @{text"let"}-con\-structs to be expanded at some point. Since
-@{text"let"}\ldots\isa{=}\ldots@{text"in"}{\ldots} is just syntactic sugar for a predefined constant
-(called @{term"Let"}), expanding @{text"let"}-constructs means rewriting with
-@{thm[source]Let_def}:
-*}
+text{*\index{simplification!of \isa{let}-expressions}\index{*let expressions}%
+Proving a goal containing \isa{let}-expressions almost invariably requires the
+@{text"let"}-con\-structs to be expanded at some point. Since
+@{text"let"}\ldots\isa{=}\ldots@{text"in"}{\ldots} is just syntactic sugar for
+the predefined constant @{term"Let"}, expanding @{text"let"}-constructs
+means rewriting with \tdx{Let_def}: *}
lemma "(let xs = [] in xs@ys@xs) = ys";
apply(simp add: Let_def);
@@ -206,14 +207,15 @@
text{*
If, in a particular context, there is no danger of a combinatorial explosion
-of nested @{text"let"}s one could even simlify with @{thm[source]Let_def} by
+of nested @{text"let"}s, you could even simplify with @{thm[source]Let_def} by
default:
*}
declare Let_def [simp]
-subsection{*Conditional Equations*}
+subsection{*Conditional Simplification Rules*}
text{*
+\index{conditional simplification rules}%
So far all examples of rewrite rules were equations. The simplifier also
accepts \emph{conditional} equations, for example
*}
@@ -245,15 +247,16 @@
subsection{*Automatic Case Splits*}
-text{*\label{sec:AutoCaseSplits}\indexbold{case splits}\index{*split (method, attr.)|(}
-Goals containing @{text"if"}-expressions are usually proved by case
-distinction on the condition of the @{text"if"}. For example the goal
+text{*\label{sec:AutoCaseSplits}\indexbold{case splits}%
+Goals containing @{text"if"}-expressions\index{*if expressions!splitting of}
+are usually proved by case
+distinction on the boolean condition. Here is an example:
*}
lemma "\<forall>xs. if xs = [] then rev xs = [] else rev xs \<noteq> []";
txt{*\noindent
-can be split by a special method @{text split}:
+The goal can be split by a special method, \methdx{split}:
*}
apply(split split_if)
@@ -262,23 +265,25 @@
@{subgoals[display,indent=0]}
where \tdx{split_if} is a theorem that expresses splitting of
@{text"if"}s. Because
-case-splitting on @{text"if"}s is almost always the right proof strategy, the
-simplifier performs it automatically. Try \isacommand{apply}@{text"(simp)"}
+splitting the @{text"if"}s is usually the right proof strategy, the
+simplifier does it automatically. Try \isacommand{apply}@{text"(simp)"}
on the initial goal above.
This splitting idea generalizes from @{text"if"} to \sdx{case}.
-Let us simplify a case analysis over lists:
+Let us simplify a case analysis over lists:\index{*list.split (theorem)}
*}(*<*)by simp(*>*)
lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
apply(split list.split);
txt{*
@{subgoals[display,indent=0]}
-In contrast to @{text"if"}-expressions, the simplifier does not split
-@{text"case"}-expressions by default because this can lead to nontermination
-in case of recursive datatypes. Therefore the simplifier has a modifier
-@{text split} for adding further splitting rules explicitly. This means the
-above lemma can be proved in one step by
+The simplifier does not split
+@{text"case"}-expressions, as it does @{text"if"}-expressions,
+because with recursive datatypes it could lead to nontermination.
+Instead, the simplifier has a modifier
+@{text split}\index{*split (modified)}
+for adding splitting rules explicitly. The
+lemma above can be proved in one step by
*}
(*<*)oops;
lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
@@ -288,9 +293,9 @@
text{*\noindent
whereas \isacommand{apply}@{text"(simp)"} alone will not succeed.
-In general, every datatype $t$ comes with a theorem
+Every datatype $t$ comes with a theorem
$t$@{text".split"} which can be declared to be a \bfindex{split rule} either
-locally as above, or by giving it the @{text"split"} attribute globally:
+locally as above, or by giving it the \attrdx{split} attribute globally:
*}
declare list.split [split]
@@ -312,65 +317,42 @@
declare list.split [split del]
text{*
-In polished proofs the @{text split} method is rarely used on its own
-but always as part of the simplifier. However, if a goal contains
-multiple splittable constructs, the @{text split} method can be
+Polished proofs typically perform splitting within @{text simp} rather than
+invoking the @{text split} method. However, if a goal contains
+several @{text if} and @{text case} expressions,
+the @{text 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 @{text"if"} or @{text"case"}-expression in
-the assumptions, you have to apply @{thm[source]split_if_asm} or
-$t$@{text".split_asm"}:
-*}
+The split rules shown above are intended to affect only the subgoal's
+conclusion. If you want to split an @{text"if"} or @{text"case"}-expression
+in the assumptions, you have to apply \tdx{split_if_asm} or
+$t$@{text".split_asm"}: *}
lemma "if xs = [] then ys \<noteq> [] else ys = [] \<Longrightarrow> xs @ ys \<noteq> []"
apply(split split_if_asm)
txt{*\noindent
-In contrast to splitting the conclusion, this actually creates two
-separate subgoals (which are solved by @{text"simp_all"}):
+Unlike splitting the conclusion, this step creates two
+separate subgoals, which here can be solved by @{text"simp_all"}:
@{subgoals[display,indent=0]}
If you need to split both in the assumptions and the conclusion,
use $t$@{text".splits"} which subsumes $t$@{text".split"} and
$t$@{text".split_asm"}. Analogously, there is @{thm[source]if_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}
*}
(*<*)
by(simp_all)
(*>*)
-subsection{*Arithmetic*}
-
-text{*\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
-*}
-
-lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
-(*<*)by(auto)(*>*)
-
-text{*\noindent
-is proved by simplification, whereas the only slightly more complex
-*}
-
-lemma "\<not> m < n \<and> m < n+1 \<Longrightarrow> m = n";
-(*<*)by(arith)(*>*)
-
-text{*\noindent
-is not proved by simplification and requires @{text arith}.
-*}
-
-
subsection{*Tracing*}
text{*\indexbold{tracing the simplifier}
Using the simplifier effectively may take a bit of experimentation. Set the
@@ -412,9 +394,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:
*}
ML "reset trace_simp";