%
\begin{isabellebody}%
\def\isabellecontext{simp}%
\isamarkupfalse%
%
\isamarkupsubsection{Simplification Rules%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\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!
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:%
\index{*simp del (attribute)}
\begin{quote}
\isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp{\isacharbrackright}}\\
\isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp\ del{\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{\isacharcolon}} \textit{list of theorem names}\index{*add (modifier)}\\
\isa{del{\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{\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{{\isacharparenleft}simp\ add{\isacharcolon}\ mod{\isacharunderscore}mult{\isacharunderscore}distrib\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\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}\ {\isachardoublequote}{\isasymlbrakk}\ xs\ {\isacharat}\ zs\ {\isacharequal}\ ys\ {\isacharat}\ xs{\isacharsemicolon}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ ys\ {\isacharequal}\ zs{\isachardoublequote}\isanewline
\isamarkupfalse%
\isacommand{apply}\ simp\isanewline
\isamarkupfalse%
\isacommand{done}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
The second assumption simplifies to \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn
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, using the assumptions can lead to nontermination:%
\end{isamarkuptext}%
\isamarkuptrue%
\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}\isamarkupfalse%
%
\begin{isamarkuptxt}%
\noindent
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}%
\isamarkuptrue%
\isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}\isanewline
\isamarkupfalse%
\isacommand{done}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
Three modifiers influence the treatment of assumptions:
\begin{description}
\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}}]\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}}]\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.
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{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}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
we may want to prove%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}xor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptxt}%
\noindent
Typically, we begin by unfolding some definitions:
\indexbold{definitions!unfolding}%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptxt}%
\noindent
In this particular case, the resulting goal
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ A\ {\isasymand}\ {\isasymnot}\ {\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ A\ {\isasymand}\ {\isasymnot}\ A%
\end{isabelle}
can be proved by simplification. Thus we could have proved the lemma outright by%
\end{isamarkuptxt}%
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
\isamarkupfalse%
%
\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}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}\isanewline
\isamarkupfalse%
\isacommand{done}\isamarkupfalse%
%
\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{\isacharunderscore}def} by
default:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{declare}\ Let{\isacharunderscore}def\ {\isacharbrackleft}simp{\isacharbrackright}\isamarkupfalse%
%
\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}\ hd{\isacharunderscore}Cons{\isacharunderscore}tl{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ \ {\isasymLongrightarrow}\ \ hd\ xs\ {\isacharhash}\ tl\ xs\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp{\isacharparenright}\isanewline
\isamarkupfalse%
\isacommand{done}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
sequence of methods. Assuming that the simplification rule
\isa{{\isacharparenleft}rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}}
is present as well,
the lemma below is proved by plain simplification:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
The conditional equation \isa{hd{\isacharunderscore}Cons{\isacharunderscore}tl} above
can simplify \isa{hd\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl\ {\isacharparenleft}rev\ xs{\isacharparenright}} to \isa{rev\ xs}
because the corresponding precondition \isa{rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}}
simplifies to \isa{xs\ {\isasymnoteq}\ {\isacharbrackleft}{\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}\ {\isachardoublequote}{\isasymforall}xs{\isachardot}\ if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptxt}%
\noindent
The goal can be split by a special method, \methdx{split}:%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}if{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptxt}%
\noindent
\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 \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{{\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:\index{*list.split (theorem)}%
\end{isamarkuptxt}%
\isamarkuptrue%
\isamarkupfalse%
\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
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}split\ list{\isachardot}split{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptxt}%
\begin{isabelle}%
\ {\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}
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%
\isamarkupfalse%
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
whereas \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} alone will not succeed.
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 \attrdx{split} attribute globally:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{declare}\ list{\isachardot}split\ {\isacharbrackleft}split{\isacharbrackright}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
The \isa{split} attribute can be removed with the \isa{del} modifier,
either locally%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
or globally:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{declare}\ list{\isachardot}split\ {\isacharbrackleft}split\ del{\isacharbrackright}\isamarkupfalse%
%
\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{{\isachardot}split{\isacharunderscore}asm}:%
\end{isamarkuptext}%
\isamarkuptrue%
\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
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptxt}%
\noindent
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}%
\end{isabelle}
If you need to split both in the assumptions and the conclusion,
use $t$\isa{{\isachardot}splits} which subsumes $t$\isa{{\isachardot}split} and
$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}\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%
\isamarkupfalse%
%
\isamarkupsubsection{Tracing%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\indexbold{tracing the simplifier}
Using the simplifier effectively may take a bit of experimentation. Set the
Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Trace Simplifier} to get a better idea of what is going on:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
produces the following trace in Proof General's \textsf{Trace} buffer:
\begin{ttbox}\makeatother
[0]Applying instance of rewrite rule "List.rev.simps_2":
rev (?x1 # ?xs1) \(\equiv\) rev ?xs1 @ [?x1]
[0]Rewriting:
rev [a] \(\equiv\) rev [] @ [a]
[0]Applying instance of rewrite rule "List.rev.simps_1":
rev [] \(\equiv\) []
[0]Rewriting:
rev [] \(\equiv\) []
[0]Applying instance of rewrite rule "List.op @.append_Nil":
[] @ ?y \(\equiv\) ?y
[0]Rewriting:
[] @ [a] \(\equiv\) [a]
[0]Applying instance of rewrite rule
?x2 # ?t1 = ?t1 \(\equiv\) False
[0]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{0}) indicates that we are inside the $i$th
recursive 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.
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 \textsf{Trace Simplifier} flag after having
obtained the desired trace.%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: