--- a/doc-src/TutorialI/Misc/document/simp.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex Tue Jul 17 13:46:21 2001 +0200
@@ -57,7 +57,7 @@
proofs seen so far could have been performed
with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
only the first subgoal and may thus need to be repeated --- use
-\isaindex{simp_all} to simplify all subgoals.
+\methdx{simp_all} to simplify all subgoals.
Note that \isa{simp} fails if nothing changes.%
\end{isamarkuptext}%
%
@@ -138,7 +138,7 @@
Assumptions are simplified in a left-to-right fashion. If an
assumption can help in simplifying one to the left of it, this may get
overlooked. In such cases you have to rotate the assumptions explicitly:
-\isacommand{apply}\isa{{\isacharparenleft}rotate{\isacharunderscore}tac}~$n$\isa{{\isacharparenright}}\indexbold{*rotate_tac}
+\isacommand{apply}\isa{{\isacharparenleft}}\methdx{rotate_tac}~$n$\isa{{\isacharparenright}}
causes a cyclic shift by $n$ positions from right to left, if $n$ is
positive, and from left to right, if $n$ is negative.
Beware that such rotations make proofs quite brittle.
@@ -167,8 +167,8 @@
\isacommand{lemma}\ {\isachardoublequote}xor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
-Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
-get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}%
+Typically, we begin by unfolding some definitions:
+\indexbold{definitions!unfolding}%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}xor{\isacharunderscore}def{\isacharparenright}%
\begin{isamarkuptxt}%
@@ -200,7 +200,7 @@
%
\begin{isamarkuptext}%
\index{simplification!of let-expressions}
-Proving a goal containing \isaindex{let}-expressions almost invariably
+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
@@ -262,13 +262,13 @@
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymforall}xs{\isachardot}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}%
\end{isabelle}
-where \isaindexbold{split_if} is a theorem that expresses splitting of
+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}}
on the initial goal above.
-This splitting idea generalizes from \isa{if} to \isaindex{case}.
+This splitting idea generalizes from \isa{if} to \sdx{case}.
Let us simplify a case analysis over lists:%
\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
@@ -334,7 +334,7 @@
The simplifier merely simplifies the condition of an \isa{if} 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 \isaindex{case}-expressions: only the selector is
+ 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.)|)}%
@@ -344,7 +344,7 @@
}
%
\begin{isamarkuptext}%
-\index{arithmetic}
+\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
@@ -367,7 +367,8 @@
\begin{isamarkuptext}%
\indexbold{tracing the simplifier}
Using the simplifier effectively may take a bit of experimentation. Set the
-\isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going
+\isa{trace_simp}\index{*trace_simp (flag)} flag\index{flags}
+to get a better idea of what is going
on:%
\end{isamarkuptext}%
\isacommand{ML}\ {\isachardoublequote}set\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline