# HG changeset patch
# User wenzelm
# Date 1352052334 -3600
# Node ID e08cc8b2056496107bb2a1dc45ef8ff893070846
# Parent  7e491da6bcbde2f7dae1057bf3953642ba091abf
refurbished Simplifier examples;

diff -r 7e491da6bcbd -r e08cc8b20564 src/Doc/IsarRef/Generic.thy
--- 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 {*
diff -r 7e491da6bcbd -r e08cc8b20564 src/Doc/Ref/document/simplifier.tex
--- 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