doc-src/TutorialI/document/simp.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/document/simp.tex	Thu Jul 26 17:16:02 2012 +0200
@@ -0,0 +1,799 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{simp}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupsubsection{Simplification Rules%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\index{simplification rules}
+To facilitate simplification,  
+the attribute \isa{{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\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!
+
+Nearly any theorem can become a simplification
+rule. The simplifier will try to transform it into an equation.  
+For example, the theorem
+\isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P} is turned into \isa{P\ {\isaliteral{3D}{\isacharequal}}\ False}. The details
+are explained in \S\ref{sec:SimpHow}.
+
+The simplification attribute of theorems can be turned on and off:%
+\index{*simp del (attribute)}
+\begin{quote}
+\isacommand{declare} \textit{theorem-name}\isa{{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}}\\
+\isacommand{declare} \textit{theorem-name}\isa{{\isaliteral{5B}{\isacharbrackleft}}simp\ del{\isaliteral{5D}{\isacharbrackright}}}
+\end{quote}
+Only equations that really simplify, like \isa{rev\
+{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs} and
+\isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\
+{\isacharequal}\ xs}, should be declared as default simplification rules. 
+More specific ones should only be used selectively and should
+not be made default.  Distributivity laws, for example, alter
+the structure of terms and can produce an exponential blow-up instead of
+simplification.  A default simplification rule may
+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 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}
+\begin{warn}
+  It is inadvisable to toggle the simplification attribute of a
+  theorem from a parent theory $A$ in a child theory $B$ for good.
+  The reason is that if some theory $C$ is based both on $B$ and (via a
+  different path) on $A$, it is not defined what the simplification attribute
+  of that theorem will be in $C$: it could be either.
+\end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{The {\tt\slshape simp}  Method%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\index{*simp (method)|bold}
+The general format of the simplification method is
+\begin{quote}
+\isa{simp} \textit{list of modifiers}
+\end{quote}
+where the list of \emph{modifiers} fine tunes the behaviour and may
+be empty. Specific modifiers are discussed below.  Most if not all of the
+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
+\methdx{simp_all} to simplify all subgoals.
+If nothing changes, \isa{simp} fails.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Adding and Deleting Simplification Rules%
+}
+\isamarkuptrue%
+%
+\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{\isaliteral{3A}{\isacharcolon}}} \textit{list of theorem names}\index{*add (modifier)}\\
+\isa{del{\isaliteral{3A}{\isacharcolon}}} \textit{list of theorem names}\index{*del (modifier)}
+\end{quote}
+Or you can use a specific list of theorems and omit all others:
+\begin{quote}
+\isa{only{\isaliteral{3A}{\isacharcolon}}} \textit{list of theorem names}\index{*only (modifier)}
+\end{quote}
+In this example, we invoke the simplifier, adding two distributive
+laws:
+\begin{quote}
+\isacommand{apply}\isa{{\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ mod{\isaliteral{5F}{\isacharunderscore}}mult{\isaliteral{5F}{\isacharunderscore}}distrib\ add{\isaliteral{5F}{\isacharunderscore}}mult{\isaliteral{5F}{\isacharunderscore}}distrib{\isaliteral{29}{\isacharparenright}}}
+\end{quote}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Assumptions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\index{simplification!with/of assumptions}
+By default, assumptions are part of the simplification process: they are used
+as simplification rules and are simplified themselves. For example:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ xs\ {\isaliteral{40}{\isacharat}}\ zs\ {\isaliteral{3D}{\isacharequal}}\ ys\ {\isaliteral{40}{\isacharat}}\ xs{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{40}{\isacharat}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ zs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ simp\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+The second assumption simplifies to \isa{xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}, which in turn
+simplifies the first assumption to \isa{zs\ {\isaliteral{3D}{\isacharequal}}\ ys}, thus reducing the
+conclusion to \isa{ys\ {\isaliteral{3D}{\isacharequal}}\ ys} and hence to \isa{True}.
+
+In some cases, using the assumptions can lead to nontermination:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{3D}{\isacharequal}}\ g\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}g\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+\noindent
+An unmodified application of \isa{simp} loops.  The culprit is the
+simplification rule \isa{f\ x\ {\isaliteral{3D}{\isacharequal}}\ g\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}g\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\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}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}simp\ {\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+Three modifiers influence the treatment of assumptions:
+\begin{description}
+\item[\isa{{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{29}{\isacharparenright}}}]\index{*no_asm (modifier)}
+ means that assumptions are completely ignored.
+\item[\isa{{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{29}{\isacharparenright}}}]\index{*no_asm_simp (modifier)}
+ means that the assumptions are not simplified but
+  are used in the simplification of the conclusion.
+\item[\isa{{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}use{\isaliteral{29}{\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}
+Only one of the modifiers is allowed, and it must precede all
+other modifiers.
+%\begin{warn}
+%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}@ {text"("}\methdx{rotate_tac}~$n$@ {text")"}
+%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.
+%\end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Rewriting with Definitions%
+}
+\isamarkuptrue%
+%
+\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: the simplifier does not
+expand them automatically.  Definitions are intended for introducing abstract
+concepts and not merely as abbreviations.  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}%
+\isamarkuptrue%
+\isacommand{definition}\isamarkupfalse%
+\ xor\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}xor\ A\ B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+\noindent
+we may want to prove%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}xor\ A\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+\noindent
+Typically, we begin by unfolding some definitions:
+\indexbold{definitions!unfolding}%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}simp\ only{\isaliteral{3A}{\isacharcolon}}\ xor{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\noindent
+In this particular case, the resulting goal
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A%
+\end{isabelle}
+can be proved by simplification. Thus we could have proved the lemma outright by%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ xor{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+Of course we can also unfold definitions in the middle of a proof.
+
+\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
+  $f$ selectively, but it may also get in the way. Defining
+  $f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$.
+\end{warn}
+
+There is also the special method \isa{unfold}\index{*unfold (method)|bold}
+which merely unfolds
+one or several definitions, as in \isacommand{apply}\isa{(unfold xor_def)}.
+This is can be useful in situations where \isa{simp} does too much.
+Warning: \isa{unfold} acts on all subgoals!%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Simplifying {\tt\slshape let}-Expressions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\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}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}let\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ in\ xs{\isaliteral{40}{\isacharat}}ys{\isaliteral{40}{\isacharat}}xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ Let{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+If, in a particular context, there is no danger of a combinatorial explosion
+of nested \isa{let}s, you could even simplify with \isa{Let{\isaliteral{5F}{\isacharunderscore}}def} by
+default:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{declare}\isamarkupfalse%
+\ Let{\isaliteral{5F}{\isacharunderscore}}def\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}%
+\isamarkupsubsection{Conditional Simplification Rules%
+}
+\isamarkuptrue%
+%
+\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}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ hd{\isaliteral{5F}{\isacharunderscore}}Cons{\isaliteral{5F}{\isacharunderscore}}tl{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \ hd\ xs\ {\isaliteral{23}{\isacharhash}}\ tl\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}case{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
+sequence of methods. Assuming that the simplification rule
+\isa{{\isaliteral{28}{\isacharparenleft}}rev\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}}
+is present as well,
+the lemma below is proved by plain simplification:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ hd{\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ tl{\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+The conditional equation \isa{hd{\isaliteral{5F}{\isacharunderscore}}Cons{\isaliteral{5F}{\isacharunderscore}}tl} above
+can simplify \isa{hd\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ tl\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}} to \isa{rev\ xs}
+because the corresponding precondition \isa{rev\ xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}
+simplifies to \isa{xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}, which is exactly the local
+assumption of the subgoal.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Automatic Case Splits%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\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}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}xs{\isaliteral{2E}{\isachardot}}\ if\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ then\ rev\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ else\ rev\ xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+\noindent
+The goal can be split by a special method, \methdx{split}:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}split\ split{\isaliteral{5F}{\isacharunderscore}}if{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\noindent
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}xs{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ rev\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ rev\ xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+where \tdx{split_if} is a theorem that expresses splitting of
+\isa{if}s. Because
+splitting the \isa{if}s is usually the right proof strategy, the
+simplifier does it automatically.  Try \isacommand{apply}\isa{{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}}
+on the initial goal above.
+
+This splitting idea generalizes from \isa{if} to \sdx{case}.
+Let us simplify a case analysis over lists:\index{*list.split (theorem)}%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}case\ xs\ of\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ zs\ {\isaliteral{7C}{\isacharbar}}\ y{\isaliteral{23}{\isacharhash}}ys\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ y{\isaliteral{23}{\isacharhash}}{\isaliteral{28}{\isacharparenleft}}ys{\isaliteral{40}{\isacharat}}zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs{\isaliteral{40}{\isacharat}}zs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}split\ list{\isaliteral{2E}{\isachardot}}split{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ zs\ {\isaliteral{3D}{\isacharequal}}\ xs\ {\isaliteral{40}{\isacharat}}\ zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ }{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}a\ list{\isaliteral{2E}{\isachardot}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{23}{\isacharhash}}\ list\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ a\ {\isaliteral{23}{\isacharhash}}\ list\ {\isaliteral{40}{\isacharat}}\ zs\ {\isaliteral{3D}{\isacharequal}}\ xs\ {\isaliteral{40}{\isacharat}}\ zs{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+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 (modifier)} 
+for adding splitting rules explicitly.  The
+lemma above can be proved in one step by%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}simp\ split{\isaliteral{3A}{\isacharcolon}}\ list{\isaliteral{2E}{\isachardot}}split{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+whereas \isacommand{apply}\isa{{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}} alone will not succeed.
+
+Every datatype $t$ comes with a theorem
+$t$\isa{{\isaliteral{2E}{\isachardot}}split} which can be declared to be a \bfindex{split rule} either
+locally as above, or by giving it the \attrdx{split} attribute globally:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{declare}\isamarkupfalse%
+\ list{\isaliteral{2E}{\isachardot}}split\ {\isaliteral{5B}{\isacharbrackleft}}split{\isaliteral{5D}{\isacharbrackright}}%
+\begin{isamarkuptext}%
+\noindent
+The \isa{split} attribute can be removed with the \isa{del} modifier,
+either locally%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}simp\ split\ del{\isaliteral{3A}{\isacharcolon}}\ split{\isaliteral{5F}{\isacharunderscore}}if{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+or globally:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{declare}\isamarkupfalse%
+\ list{\isaliteral{2E}{\isachardot}}split\ {\isaliteral{5B}{\isacharbrackleft}}split\ del{\isaliteral{5D}{\isacharbrackright}}%
+\begin{isamarkuptext}%
+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 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{{\isaliteral{2E}{\isachardot}}split{\isaliteral{5F}{\isacharunderscore}}asm}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}if\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ then\ ys\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ else\ ys\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ xs\ {\isaliteral{40}{\isacharat}}\ ys\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}split\ split{\isaliteral{5F}{\isacharunderscore}}if{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\noindent
+Unlike splitting the conclusion, this step creates two
+separate subgoals, which here can be solved by \isa{simp{\isaliteral{5F}{\isacharunderscore}}all}:
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\ ys\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ xs\ {\isaliteral{40}{\isacharat}}\ ys\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
+\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ xs\ {\isaliteral{40}{\isacharat}}\ ys\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}%
+\end{isabelle}
+If you need to split both in the assumptions and the conclusion,
+use $t$\isa{{\isaliteral{2E}{\isachardot}}splits} which subsumes $t$\isa{{\isaliteral{2E}{\isachardot}}split} and
+$t$\isa{{\isaliteral{2E}{\isachardot}}split{\isaliteral{5F}{\isacharunderscore}}asm}. Analogously, there is \isa{if{\isaliteral{5F}{\isacharunderscore}}splits}.
+
+\begin{warn}
+  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}%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsection{Tracing%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\indexbold{tracing the simplifier}
+Using the simplifier effectively may take a bit of experimentation.  Set the
+Proof General flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgmenu{Trace Simplifier} to get a better idea of what is going on:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}rev\ {\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+produces the following trace in Proof General's \pgmenu{Trace} buffer:
+
+\begin{ttbox}\makeatother
+[1]Applying instance of rewrite rule "List.rev.simps_2":
+rev (?x1 # ?xs1) \(\equiv\) rev ?xs1 @ [?x1]
+
+[1]Rewriting:
+rev [a] \(\equiv\) rev [] @ [a]
+
+[1]Applying instance of rewrite rule "List.rev.simps_1":
+rev [] \(\equiv\) []
+
+[1]Rewriting:
+rev [] \(\equiv\) []
+
+[1]Applying instance of rewrite rule "List.op @.append_Nil":
+[] @ ?y \(\equiv\) ?y
+
+[1]Rewriting:
+[] @ [a] \(\equiv\) [a]
+
+[1]Applying instance of rewrite rule
+?x2 # ?t1 = ?t1 \(\equiv\) False
+
+[1]Rewriting:
+[a] = [] \(\equiv\) False
+\end{ttbox}
+The trace lists each rule being applied, both in its general form and
+the instance being used. The \texttt{[}$i$\texttt{]} in front (where
+above $i$ is always \texttt{1}) indicates that we are inside the $i$th
+invocation of the simplifier. Each attempt to apply a
+conditional rule shows the rule followed by the trace of the
+(recursive!) simplification of the conditions, the latter prefixed by
+\texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}.
+Another source of recursive invocations of the simplifier are
+proofs of arithmetic formulae. By default, recursive invocations are not shown,
+you must increase the trace depth via \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgmenu{Trace Simplifier Depth}.
+
+Many other hints about the simplifier's actions may appear.
+
+In more complicated cases, the trace can be very lengthy.  Thus it is
+advisable to reset the \pgmenu{Trace Simplifier} flag after having
+obtained the desired trace.
+Since this is easily forgotten (and may have the unpleasant effect of
+swamping the interface with trace information), here is how you can switch
+the trace on locally in a proof:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{using}\isamarkupfalse%
+\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5F}{\isacharunderscore}}trace{\isaliteral{3D}{\isacharequal}}true{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
+\isacommand{apply}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+Within the current proof, all simplifications in subsequent proof steps
+will be traced, but the text reminds you to remove the \isa{using} clause
+after it has done its job.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Finding Theorems\label{sec:find}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\indexbold{finding theorems}\indexbold{searching theorems}
+Isabelle's large database of proved theorems 
+offers a powerful search engine. Its chief limitation is
+its restriction to the theories currently loaded.
+
+\begin{pgnote}
+The search engine is started by clicking on Proof General's \pgmenu{Find} icon.
+You specify your search textually in the input buffer at the bottom
+of the window.
+\end{pgnote}
+
+The simplest form of search finds theorems containing specified
+patterns.  A pattern can be any term (even
+a single identifier).  It may contain ``\texttt{\_}'', a wildcard standing
+for any term. Here are some
+examples:
+\begin{ttbox}
+length
+"_ # _ = _ # _"
+"_ + _"
+"_ * (_ - (_::nat))"
+\end{ttbox}
+Specifying types, as shown in the last example, 
+constrains searches involving overloaded operators.
+
+\begin{warn}
+Always use ``\texttt{\_}'' rather than variable names: searching for
+\texttt{"x + y"} will usually not find any matching theorems
+because they would need to contain \texttt{x} and~\texttt{y} literally.
+When searching for infix operators, do not just type in the symbol,
+such as~\texttt{+}, but a proper term such as \texttt{"_ + _"}.
+This remark applies to more complicated syntaxes, too.
+\end{warn}
+
+If you are looking for rewrite rules (possibly conditional) that could
+simplify some term, prefix the pattern with \texttt{simp:}.
+\begin{ttbox}
+simp: "_ * (_ + _)"
+\end{ttbox}
+This finds \emph{all} equations---not just those with a \isa{simp} attribute---whose conclusion has the form
+\begin{isabelle}%
+\ \ \ \ \ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}%
+\end{isabelle}
+It only finds equations that can simplify the given pattern
+at the root, not somewhere inside: for example, equations of the form
+\isa{{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}} do not match.
+
+You may also search for theorems by name---you merely
+need to specify a substring. For example, you could search for all
+commutativity theorems like this:
+\begin{ttbox}
+name: comm
+\end{ttbox}
+This retrieves all theorems whose name contains \texttt{comm}.
+
+Search criteria can also be negated by prefixing them with ``\texttt{-}''.
+For example,
+\begin{ttbox}
+-name: List
+\end{ttbox}
+finds theorems whose name does not contain \texttt{List}. You can use this
+to exclude particular theories from the search: the long name of
+a theorem contains the name of the theory it comes from.
+
+Finallly, different search criteria can be combined arbitrarily. 
+The effect is conjuctive: Find returns the theorems that satisfy all of
+the criteria. For example,
+\begin{ttbox}
+"_ + _"  -"_ - _"  -simp: "_ * (_ + _)"  name: assoc
+\end{ttbox}
+looks for theorems containing plus but not minus, and which do not simplify
+\mbox{\isa{{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}}} at the root, and whose name contains \texttt{assoc}.
+
+Further search criteria are explained in \S\ref{sec:find2}.
+
+\begin{pgnote}
+Proof General keeps a history of all your search expressions.
+If you click on \pgmenu{Find}, you can use the arrow keys to scroll
+through previous searches and just modify them. This saves you having
+to type in lengthy expressions again and again.
+\end{pgnote}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: