--- a/src/Doc/IsarRef/Generic.thy Sat Nov 03 21:31:40 2012 +0100
+++ b/src/Doc/IsarRef/Generic.thy Sun Nov 04 19:05:34 2012 +0100
@@ -496,6 +496,7 @@
\end{tabular}
\end{center}
+ %FIXME move?
\medskip The Splitter package is usually configured to work as part
of the Simplifier. The effect of repeatedly applying @{ML
split_tac} can be simulated by ``@{text "(simp only: split:
@@ -504,6 +505,95 @@
*}
+subsubsection {* Examples *}
+
+text {* We consider basic algebraic simplifications in Isabelle/HOL.
+ The rather trivial goal @{prop "0 + (x + 0) = x + 0 + 0"} looks like
+ a good candidate to be solved by a single call of @{method simp}:
+*}
+
+lemma "0 + (x + 0) = x + 0 + 0" apply simp? oops
+
+text {* The above attempt \emph{fails}, because @{term "0"} and @{term
+ "op +"} in the HOL library are declared as generic type class
+ operations, without stating any algebraic laws yet. More specific
+ types are required to get access to certain standard simplifications
+ of the theory context, e.g.\ like this: *}
+
+lemma fixes x :: nat shows "0 + (x + 0) = x + 0 + 0" by simp
+lemma fixes x :: int shows "0 + (x + 0) = x + 0 + 0" by simp
+lemma fixes x :: "'a :: monoid_add" shows "0 + (x + 0) = x + 0 + 0" by simp
+
+text {*
+ \medskip In many cases, assumptions of a subgoal are also needed in
+ the simplification process. For example:
+*}
+
+lemma fixes x :: nat shows "x = 0 \<Longrightarrow> x + x = 0" by simp
+lemma fixes x :: nat assumes "x = 0" shows "x + x = 0" apply simp oops
+lemma fixes x :: nat assumes "x = 0" shows "x + x = 0" using assms by simp
+
+text {* As seen above, local assumptions that shall contribute to
+ simplification need to be part of the subgoal already, or indicated
+ explicitly for use by the subsequent method invocation. Both too
+ little or too much information can make simplification fail, for
+ different reasons.
+
+ In the next example the malicious assumption @{prop "\<And>x::nat. f x =
+ g (f (g x))"} does not contribute to solve the problem, but makes
+ the default @{method simp} method loop: the rewrite rule @{text "f
+ ?x \<equiv> g (f (g ?x))"} extracted from the assumption does not
+ terminate. The Simplifier notices certain simple forms of
+ nontermination, but not this one. The problem can be solved
+ nonetheless, by ignoring assumptions via special options as
+ explained before:
+*}
+
+lemma "(\<And>x::nat. f x = g (f (g x))) \<Longrightarrow> f 0 = f 0 + 0"
+ by (simp (no_asm))
+
+text {* The latter form is typical for long unstructured proof
+ scripts, where the control over the goal content is limited. In
+ structured proofs it is usually better to avoid pushing too many
+ facts into the goal state in the first place. Assumptions in the
+ Isar proof context do not intrude the reasoning if not used
+ explicitly. This is illustrated for a toplevel statement and a
+ local proof body as follows:
+*}
+
+lemma
+ assumes "\<And>x::nat. f x = g (f (g x))"
+ shows "f 0 = f 0 + 0" by simp
+
+notepad
+begin
+ assume "\<And>x::nat. f x = g (f (g x))"
+ have "f 0 = f 0 + 0" by simp
+end
+
+text {* \medskip Because assumptions may simplify each other, there
+ can be very subtle cases of nontermination. For example, the regular
+ @{method simp} method applied to @{prop "P (f x) \<Longrightarrow> y = x \<Longrightarrow> f x = f y
+ \<Longrightarrow> Q"} gives rise to the infinite reduction sequence
+ \[
+ @{text "P (f x)"} \stackrel{@{text "f x \<equiv> f y"}}{\longmapsto}
+ @{text "P (f y)"} \stackrel{@{text "y \<equiv> x"}}{\longmapsto}
+ @{text "P (f x)"} \stackrel{@{text "f x \<equiv> f y"}}{\longmapsto} \cdots
+ \]
+ whereas applying the same to @{prop "y = x \<Longrightarrow> f x = f y \<Longrightarrow> P (f x) \<Longrightarrow>
+ Q"} terminates (without solving the goal):
+*}
+
+lemma "y = x \<Longrightarrow> f x = f y \<Longrightarrow> P (f x) \<Longrightarrow> Q"
+ apply simp
+ oops
+
+text {* See also \secref{sec:simp-config} for options to enable
+ Simplifier trace mode, which often helps to diagnose problems with
+ rewrite systems.
+*}
+
+
subsection {* Declaring rules \label{sec:simp-rules} *}
text {*
--- a/src/Doc/Ref/document/simplifier.tex Sat Nov 03 21:31:40 2012 +0100
+++ b/src/Doc/Ref/document/simplifier.tex Sun Nov 04 19:05:34 2012 +0100
@@ -7,90 +7,6 @@
\section{Simplification for dummies}
\label{sec:simp-for-dummies}
-\subsection{Simplification tactics} \label{sec:simp-for-dummies-tacs}
-\begin{ttbox}
-Simp_tac : int -> tactic
-Asm_simp_tac : int -> tactic
-Full_simp_tac : int -> tactic
-Asm_full_simp_tac : int -> tactic
-\end{ttbox}
-
-\begin{ttdescription}
-\item[\ttindexbold{Simp_tac} $i$] simplifies subgoal~$i$ using the
- current simpset. It may solve the subgoal completely if it has
- become trivial, using the simpset's solver tactic.
-
-\item[\ttindexbold{Asm_simp_tac}]\index{assumptions!in simplification}
- is like \verb$Simp_tac$, but extracts additional rewrite rules from
- the local assumptions.
-
-\item[\ttindexbold{Full_simp_tac}] is like \verb$Simp_tac$, but also
- simplifies the assumptions (without using the assumptions to
- simplify each other or the actual goal).
-
-\item[\ttindexbold{Asm_full_simp_tac}] is like \verb$Asm_simp_tac$,
- but also simplifies the assumptions. In particular, assumptions can
- simplify each other.
-\footnote{\texttt{Asm_full_simp_tac} used to process the assumptions from
- left to right. For backwards compatibilty reasons only there is now
- \texttt{Asm_lr_simp_tac} that behaves like the old \texttt{Asm_full_simp_tac}.}
-\end{ttdescription}
-
-\medskip
-
-As an example, consider the theory of arithmetic in HOL. The (rather trivial)
-goal $0 + (x + 0) = x + 0 + 0$ can be solved by a single call of
-\texttt{Simp_tac} as follows:
-\begin{ttbox}
-context Arith.thy;
-Goal "0 + (x + 0) = x + 0 + 0";
-{\out 1. 0 + (x + 0) = x + 0 + 0}
-by (Simp_tac 1);
-{\out Level 1}
-{\out 0 + (x + 0) = x + 0 + 0}
-{\out No subgoals!}
-\end{ttbox}
-
-The simplifier uses the current simpset of \texttt{Arith.thy}, which
-contains suitable theorems like $\Var{n}+0 = \Var{n}$ and $0+\Var{n} =
-\Var{n}$.
-
-\medskip In many cases, assumptions of a subgoal are also needed in
-the simplification process. For example, \texttt{x = 0 ==> x + x = 0}
-is solved by \texttt{Asm_simp_tac} as follows:
-\begin{ttbox}
-{\out 1. x = 0 ==> x + x = 0}
-by (Asm_simp_tac 1);
-\end{ttbox}
-
-\medskip \texttt{Asm_full_simp_tac} is the most powerful of this quartet
-of tactics but may also loop where some of the others terminate. For
-example,
-\begin{ttbox}
-{\out 1. ALL x. f x = g (f (g x)) ==> f 0 = f 0 + 0}
-\end{ttbox}
-is solved by \texttt{Simp_tac}, but \texttt{Asm_simp_tac} and {\tt
- Asm_full_simp_tac} loop because the rewrite rule $f\,\Var{x} =
-g\,(f\,(g\,\Var{x}))$ extracted from the assumption does not
-terminate. Isabelle notices certain simple forms of nontermination,
-but not this one. Because assumptions may simplify each other, there can be
-very subtle cases of nontermination. For example, invoking
-{\tt Asm_full_simp_tac} on
-\begin{ttbox}
-{\out 1. [| P (f x); y = x; f x = f y |] ==> Q}
-\end{ttbox}
-gives rise to the infinite reduction sequence
-\[
-P\,(f\,x) \stackrel{f\,x = f\,y}{\longmapsto} P\,(f\,y) \stackrel{y = x}{\longmapsto}
-P\,(f\,x) \stackrel{f\,x = f\,y}{\longmapsto} \cdots
-\]
-whereas applying the same tactic to
-\begin{ttbox}
-{\out 1. [| y = x; f x = f y; P (f x) |] ==> Q}
-\end{ttbox}
-terminates.
-
-
\subsection{Modifying the current simpset}
\begin{ttbox}
Addsimps : thm list -> unit