--- a/doc-src/TutorialI/Misc/simp.thy Tue Sep 12 10:50:29 2000 +0200
+++ b/doc-src/TutorialI/Misc/simp.thy Tue Sep 12 14:59:44 2000 +0200
@@ -1,4 +1,411 @@
-
+(*<*)
theory simp = Main:
+(*>*)
+subsubsection{*Simplification rules*}
+
+text{*\indexbold{simplification rule}
+To facilitate simplification, theorems can be declared to be simplification
+rules (with the help of 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
+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
+are explained in \S\ref{sec:SimpHow}.
+
+The simplification attribute of theorems can be turned on and off as follows:
+\begin{quote}
+\isacommand{declare} \textit{theorem-name}@{text"[simp]"}\\
+\isacommand{declare} \textit{theorem-name}@{text"[simp del]"}
+\end{quote}
+As a rule of thumb, equations that really simplify (like @{prop"rev(rev xs) =
+ xs"} and @{prop"xs @ [] = xs"}) should be made simplification
+rules. Those of a more specific nature (e.g.\ distributivity laws, which
+alter the structure of terms considerably) should only be used selectively,
+i.e.\ they should not be default simplification rules. Conversely, it may
+also happen that a simplification rule needs to be disabled in certain
+proofs. Frequent changes in the simplification status of a theorem may
+indicate a badly designed theory.
+\begin{warn}
+ Simplification may not terminate, 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}
+*}
+
+subsubsection{*The simplification method*}
+
+text{*\index{*simp (method)|bold}
+The general format of the simplification method is
+\begin{quote}
+@{text simp} \textit{list of modifiers}
+\end{quote}
+where the list of \emph{modifiers} helps to fine tune the behaviour and may
+be empty. Most if not all of the proofs seen so far could have been performed
+with @{text simp} instead of \isa{auto}, except that @{text simp} attacks
+only the first subgoal and may thus need to be repeated---use
+\isaindex{simp_all} to simplify all subgoals.
+Note that @{text simp} fails if nothing changes.
+*}
+
+subsubsection{*Adding and deleting simplification rules*}
+
+text{*
+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}
+\end{quote}
+In case you want to use only a specific list of theorems and ignore all
+others:
+\begin{quote}
+@{text"only:"} \textit{list of theorem names}
+\end{quote}
+*}
+
+subsubsection{*Assumptions*}
+
+text{*\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:
+*}
+
+lemma "\\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \\<rbrakk> \\<Longrightarrow> ys = zs";
+by simp;
+
+text{*\noindent
+The second assumption simplifies to @{term"xs = []"}, which in turn
+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:
+*}
+
+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:
+*}
+
+by(simp (no_asm));
+
+text{*\noindent
+There are three options that influence the treatment of assumptions:
+\begin{description}
+\item[@{text"(no_asm)"}]\indexbold{*no_asm}
+ means that assumptions are completely ignored.
+\item[@{text"(no_asm_simp)"}]\indexbold{*no_asm_simp}
+ 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}
+ means that the assumptions are simplified but are not
+ used in the simplification of each other or the conclusion.
+\end{description}
+Neither @{text"(no_asm_simp)"} nor @{text"(no_asm_use)"} allow to simplify
+the above problematic subgoal.
+
+Note that only one of the above options is allowed, and it must precede all
+other arguments.
+*}
+
+subsubsection{*Rewriting with definitions*}
+
+text{*\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
+*}
+
+constdefs exor :: "bool \\<Rightarrow> bool \\<Rightarrow> bool"
+ "exor A B \\<equiv> (A \\<and> \\<not>B) \\<or> (\\<not>A \\<and> B)";
+
+text{*\noindent
+we may want to prove
+*}
+
+lemma "exor A (\\<not>A)";
+
+txt{*\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}
+*}
+
+apply(simp only:exor_def);
+
+txt{*\noindent
+In this particular case, the resulting goal
+\begin{isabelle}
+~1.~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
+*}(*<*)oops;lemma "exor A (\\<not>A)";(*>*)
+by(simp add: exor_def)
+
+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 of an abbreviation.
+
+\begin{warn}
+ If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
+ occurrences of $f$ with at least two arguments. Thus it is safer to define
+ $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
+\end{warn}
+*}
+
+subsubsection{*Simplifying let-expressions*}
+
+text{*\index{simplification!of let-expressions}
+Proving a goal containing \isaindex{let}-expressions almost invariably
+requires the @{text"let"}-con\-structs to be expanded at some point. Since
+@{text"let"}-@{text"in"} is just syntactic sugar for a predefined constant
+(called @{term"Let"}), expanding @{text"let"}-constructs means rewriting with
+@{thm[source]Let_def}:
+*}
+
+lemma "(let xs = [] in xs@ys@xs) = ys";
+by(simp add: Let_def);
+
+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
+default:
+*}
+declare Let_def [simp]
+
+subsubsection{*Conditional equations*}
+
+text{*
+So far all examples of rewrite rules were equations. The simplifier also
+accepts \emph{conditional} equations, for example
+*}
+
+lemma hd_Cons_tl[simp]: "xs \\<noteq> [] \\<Longrightarrow> hd xs # tl xs = xs";
+by(case_tac xs, simp, simp);
+
+text{*\noindent
+Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
+sequence of methods. Assuming that the simplification rule
+@{term"(rev xs = []) = (xs = [])"}
+is present as well,
+*}
+
+lemma "xs \\<noteq> [] \\<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs";
+(*<*)
+by(simp);
+(*>*)
+text{*\noindent
+is proved by plain simplification:
+the conditional equation @{thm[source]hd_Cons_tl} above
+can simplify @{term"hd(rev xs) # tl(rev xs)"} to @{term"rev xs"}
+because the corresponding precondition @{term"rev xs ~= []"}
+simplifies to @{term"xs ~= []"}, which is exactly the local
+assumption of the subgoal.
+*}
+
+
+subsubsection{*Automatic case splits*}
+
+text{*\indexbold{case splits}\index{*split|(}
+Goals containing @{text"if"}-expressions are usually proved by case
+distinction on the condition of the @{text"if"}. For example the goal
+*}
+
+lemma "\\<forall>xs. if xs = [] then rev xs = [] else rev xs \\<noteq> []";
+
+txt{*\noindent
+can be split into
+\begin{isabelle}
+~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])
+\end{isabelle}
+by a degenerate form of simplification
+*}
+
+apply(simp only: split: split_if);
+(*<*)oops;(*>*)
+
+text{*\noindent
+where no simplification rules are included (@{text"only:"} is followed by the
+empty list of theorems) but the rule \isaindexbold{split_if} for
+splitting @{text"if"}s is added (via the modifier @{text"split:"}). Because
+case-splitting on @{text"if"}s is almost always the right proof strategy, the
+simplifier performs it automatically. Try \isacommand{apply}@{text"(simp)"}
+on the initial goal above.
+
+This splitting idea generalizes from @{text"if"} to \isaindex{case}:
+*}
+
+lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs";
+txt{*\noindent
+becomes
+\begin{isabelle}\makeatother
+~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
+~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)
+\end{isabelle}
+by typing
+*}
+
+apply(simp only: split: list.split);
+(*<*)oops;(*>*)
+
+text{*\noindent
+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. Again, if the @{text"only:"} modifier is
+dropped, the above goal is solved,
+*}
+(*<*)
+lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs";
+(*>*)
+by(simp split: list.split);
+
+text{*\noindent%
+which \isacommand{apply}@{text"(simp)"} alone will not do.
+
+In general, 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:
+*}
+
+declare list.split [split]
+
+text{*\noindent
+The @{text"split"} attribute can be removed with the @{text"del"} modifier,
+either locally
+*}
+(*<*)
+lemma "dummy=dummy";
+(*>*)
+apply(simp split del: split_if);
+(*<*)
+oops;
+(*>*)
+text{*\noindent
+or globally:
+*}
+declare list.split [split del]
+
+text{*
+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"}:
+*}
+
+lemma "if xs = [] then ys ~= [] else ys = [] ==> xs @ ys ~= []"
+apply(simp only: split: split_if_asm);
+(*<*)
+by(simp_all)
+(*>*)
+
+text{*\noindent
+In contrast to splitting the conclusion, this actually creates two
+separate subgoals (which are solved by @{text"simp_all"}):
+\begin{isabelle}
+\ \isadigit{1}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
+\ \isadigit{2}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{xs}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}
+\end{isabelle}
+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
+ \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
+ simplified at first, until either the expression reduces to one of the
+ cases or it is split.
+\end{warn}
+
+\index{*split|)}
+*}
+
+
+subsubsection{*Arithmetic*}
+
+text{*\index{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 (possibly negated) (in)equalities
+(@{text"="}, \isasymle, @{text"<"}) 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}.
+*}
+
+
+subsubsection{*Tracing*}
+text{*\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
+on:
+*}
+
+ML "set trace_simp";
+lemma "rev [a] = []";
+apply(simp);
+(*<*)oops(*>*)
+
+text{*\noindent
+produces the trace
+
+\begin{ttbox}\makeatother
+Applying instance of rewrite rule:
+rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
+Rewriting:
+rev [x] == rev [] @ [x]
+Applying instance of rewrite rule:
+rev [] == []
+Rewriting:
+rev [] == []
+Applying instance of rewrite rule:
+[] @ ?y == ?y
+Rewriting:
+[] @ [x] == [x]
+Applying instance of rewrite rule:
+?x3 \# ?t3 = ?t3 == False
+Rewriting:
+[x] = [] == False
+\end{ttbox}
+
+In more complicated cases, the trace can be quite lenghty, especially since
+invocations of the simplifier are often nested (e.g.\ when solving conditions
+of rewrite rules). Thus it is advisable to reset it:
+*}
+
+ML "reset trace_simp";
+
+(*<*)
end
+(*>*)