--- a/src/Doc/IsarRef/Generic.thy Wed Nov 07 16:45:33 2012 +0100
+++ b/src/Doc/IsarRef/Generic.thy Wed Nov 07 21:43:02 2012 +0100
@@ -385,11 +385,17 @@
simplification strategy, or incorporate other proof tools that solve
sub-problems, produce rewrite rules on demand etc.
+ The rewriting strategy is always strictly bottom up, except for
+ congruence rules, which are applied while descending into a term.
+ Conditions in conditional rewrite rules are solved recursively
+ before the rewrite rule is applied.
+
The default Simplifier setup of major object logics (HOL, HOLCF,
FOL, ZF) makes the Simplifier ready for immediate use, without
engaging into the internal structures. Thus it serves as
general-purpose proof tool with the main focus on equational
- reasoning, and a bit more than that. *}
+ reasoning, and a bit more than that.
+*}
subsection {* Simplification methods \label{sec:simp-meth} *}
--- a/src/Doc/Ref/document/simplifier.tex Wed Nov 07 16:45:33 2012 +0100
+++ b/src/Doc/Ref/document/simplifier.tex Wed Nov 07 21:43:02 2012 +0100
@@ -1,41 +1,9 @@
\chapter{Simplification}
\label{chap:simplification}
-\index{simplification|(}
\section{Simplification sets}\index{simplification sets}
-The simplifier is controlled by information contained in {\bf
- simpsets}. These consist of several components, including rewrite
-rules, simplification procedures, congruence rules, and the subgoaler,
-solver and looper tactics. The simplifier should be set up with
-sensible defaults so that most simplifier calls specify only rewrite
-rules or simplification procedures. Experienced users can exploit the
-other components to streamline proofs in more sophisticated manners.
-
-\subsection{Building simpsets}
-\begin{ttbox}
-empty_ss : simpset
-merge_ss : simpset * simpset -> simpset
-\end{ttbox}
-\begin{ttdescription}
-
-\item[\ttindexbold{empty_ss}] is the empty simpset. This is not very useful
- under normal circumstances because it doesn't contain suitable tactics
- (subgoaler etc.). When setting up the simplifier for a particular
- object-logic, one will typically define a more appropriate ``almost empty''
- simpset. For example, in HOL this is called \ttindexbold{HOL_basic_ss}.
-
-\item[\ttindexbold{merge_ss} ($ss@1$, $ss@2$)] merges simpsets $ss@1$
- and $ss@2$ by building the union of their respective rewrite rules,
- simplification procedures and congruences. The other components
- (tactics etc.) cannot be merged, though; they are taken from either
- simpset\footnote{Actually from $ss@1$, but it would unwise to count
- on that.}.
-
-\end{ttdescription}
-
-
\subsection{Rewrite rules}
\begin{ttbox}
addsimps : simpset * thm list -> simpset \hfill{\bf infix 4}
@@ -314,50 +282,6 @@
enabled by default in the object-logics \texttt{HOL} and \texttt{FOL}.
-\section{The simplification tactics}\label{simp-tactics}
-\index{simplification!tactics}\index{tactics!simplification}
-\begin{ttbox}
-generic_simp_tac : bool -> bool * bool * bool ->
- simpset -> int -> tactic
-simp_tac : simpset -> int -> tactic
-asm_simp_tac : simpset -> int -> tactic
-full_simp_tac : simpset -> int -> tactic
-asm_full_simp_tac : simpset -> int -> tactic
-safe_asm_full_simp_tac : simpset -> int -> tactic
-\end{ttbox}
-
-\texttt{generic_simp_tac} is the basic tactic that is underlying any actual
-simplification work. The others are just instantiations of it. The rewriting
-strategy is always strictly bottom up, except for congruence rules,
-which are applied while descending into a term. Conditions in conditional
-rewrite rules are solved recursively before the rewrite rule is applied.
-
-\begin{ttdescription}
-
-\item[\ttindexbold{generic_simp_tac} $safe$ ($simp\_asm$, $use\_asm$, $mutual$)]
- gives direct access to the various simplification modes:
- \begin{itemize}
- \item if $safe$ is {\tt true}, the safe solver is used as explained in
- {\S}\ref{sec:simp-solver},
- \item $simp\_asm$ determines whether the local assumptions are simplified,
- \item $use\_asm$ determines whether the assumptions are used as local rewrite
- rules, and
- \item $mutual$ determines whether assumptions can simplify each other rather
- than being processed from left to right.
- \end{itemize}
- This generic interface is intended
- for building special tools, e.g.\ for combining the simplifier with the
- classical reasoner. It is rarely used directly.
-
-\item[\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac},
- \ttindexbold{full_simp_tac}, \ttindexbold{asm_full_simp_tac}] are
- the basic simplification tactics that work exactly like their
- namesakes in {\S}\ref{sec:simp-for-dummies}, except that they are
- explicitly supplied with a simpset.
-
-\end{ttdescription}
-
-
\section{Permutative rewrite rules}
\index{rewrite rules!permutative|(}