--- a/src/Doc/IsarRef/Generic.thy Sun Nov 04 19:05:34 2012 +0100
+++ b/src/Doc/IsarRef/Generic.thy Sun Nov 04 19:51:53 2012 +0100
@@ -441,6 +441,11 @@
include the Splitter (all major object logics such HOL, HOLCF, FOL,
ZF do this already).
+ There is also a separate @{method_ref split} method available for
+ single-step case splitting. The effect of repeatedly applying
+ @{text "(split thms)"} can be imitated by ``@{text "(simp only:
+ split: thms)"}''.
+
\medskip The @{text cong} modifiers add or delete Simplifier
congruence rules (see also \secref{sec:simp-rules}); the default is
to add.
@@ -470,7 +475,7 @@
\begin{center}
\small
- \begin{tabular}{|l|l|p{0.3\textwidth}|}
+ \begin{supertabular}{|l|l|p{0.3\textwidth}|}
\hline
Isar method & ML tactic & behavior \\\hline
@@ -493,15 +498,8 @@
mode: an assumption is only used for simplifying assumptions which
are to the right of it \\\hline
- \end{tabular}
+ \end{supertabular}
\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:
- a\<^sub>1 \<dots> a\<^sub>n)"}''. There is also a separate @{text split}
- method available for single-step case splitting.
*}
@@ -626,7 +624,13 @@
simpset and the context of the problem being simplified may lead to
unexpected results.
- \item @{attribute simp} declares simplification rules.
+ \item @{attribute simp} declares simplification rules, by adding or
+ deleting them from the simpset within the theory or proof context.
+
+ Internally, all rewrite rules have to be expressed as Pure
+ equalities, potentially with some conditions of arbitrary form.
+ Such rewrite rules in Pure are derived automatically from
+ object-level equations that are supplied by the user.
\item @{attribute split} declares case split rules.
@@ -670,6 +674,37 @@
case split over the condition @{text "?q"} to prove the goal.
\end{description}
+
+ The implicit simpset of the theory context is propagated
+ monotonically through the theory hierarchy: forming a new theory,
+ the union of the simpsets of its imports are taken as starting
+ point. Also note that definitional packages like @{command
+ "datatype"}, @{command "primrec"}, @{command "fun"} routinely
+ declare Simplifier rules to the target context, while plain
+ @{command "definition"} is an exception in \emph{not} declaring
+ anything.
+
+ \medskip It is up the user to manipulate the current simpset further
+ by explicitly adding or deleting theorems as simplification rules,
+ or installing other tools via simplification procedures
+ (\secref{sec:simproc}). Good simpsets are hard to design. Rules
+ that obviously simplify, like @{text "?n + 0 \<equiv> ?n"} are good
+ candidates for the implicit simpset, unless a special
+ non-normalizing behavior of certain operations is intended. More
+ specific rules (such as distributive laws, which duplicate subterms)
+ should be added only for specific proof steps. Conversely,
+ sometimes a rule needs to be deleted just for some part of a proof.
+ The need of frequent additions or deletions may indicate a poorly
+ designed simpset.
+
+ \begin{warn}
+ The union of simpsets from theory imports (as described above) is
+ not always a good starting point for the new theory. If some
+ ancestors have deleted simplification rules because they are no
+ longer wanted, while others have left those rules in, then the union
+ will contain the unwanted rules, and thus have to be deleted again
+ in the theory body.
+ \end{warn}
*}
--- a/src/Doc/Ref/document/simplifier.tex Sun Nov 04 19:05:34 2012 +0100
+++ b/src/Doc/Ref/document/simplifier.tex Sun Nov 04 19:51:53 2012 +0100
@@ -3,90 +3,6 @@
\label{chap:simplification}
\index{simplification|(}
-
-\section{Simplification for dummies}
-\label{sec:simp-for-dummies}
-
-\subsection{Modifying the current simpset}
-\begin{ttbox}
-Addsimps : thm list -> unit
-Delsimps : thm list -> unit
-Addsimprocs : simproc list -> unit
-Delsimprocs : simproc list -> unit
-Addcongs : thm list -> unit
-Delcongs : thm list -> unit
-Addsplits : thm list -> unit
-Delsplits : thm list -> unit
-\end{ttbox}
-
-Depending on the theory context, the \texttt{Add} and \texttt{Del}
-functions manipulate basic components of the associated current
-simpset. Internally, all rewrite rules have to be expressed as
-(conditional) meta-equalities. This form is derived automatically
-from object-level equations that are supplied by the user. Another
-source of rewrite rules are \emph{simplification procedures}, that is
-\ML\ functions that produce suitable theorems on demand, depending on
-the current redex. Congruences are a more advanced feature; see
-{\S}\ref{sec:simp-congs}.
-
-\begin{ttdescription}
-
-\item[\ttindexbold{Addsimps} $thms$;] adds rewrite rules derived from
- $thms$ to the current simpset.
-
-\item[\ttindexbold{Delsimps} $thms$;] deletes rewrite rules derived
- from $thms$ from the current simpset.
-
-\item[\ttindexbold{Addsimprocs} $procs$;] adds simplification
- procedures $procs$ to the current simpset.
-
-\item[\ttindexbold{Delsimprocs} $procs$;] deletes simplification
- procedures $procs$ from the current simpset.
-
-\item[\ttindexbold{Addcongs} $thms$;] adds congruence rules to the
- current simpset.
-
-\item[\ttindexbold{Delcongs} $thms$;] deletes congruence rules from the
- current simpset.
-
-\item[\ttindexbold{Addsplits} $thms$;] adds splitting rules to the
- current simpset.
-
-\item[\ttindexbold{Delsplits} $thms$;] deletes splitting rules from the
- current simpset.
-
-\end{ttdescription}
-
-When a new theory is built, its implicit simpset is initialized by the union
-of the respective simpsets of its parent theories. In addition, certain
-theory definition constructs (e.g.\ \ttindex{datatype} and \ttindex{primrec}
-in HOL) implicitly augment the current simpset. Ordinary definitions are not
-added automatically!
-
-It is up the user to manipulate the current simpset further by
-explicitly adding or deleting theorems and simplification procedures.
-
-\medskip
-
-Good simpsets are hard to design. Rules that obviously simplify,
-like $\Var{n}+0 = \Var{n}$, should be added to the current simpset right after
-they have been proved. More specific ones (such as distributive laws, which
-duplicate subterms) should be added only for specific proofs and deleted
-afterwards. Conversely, sometimes a rule needs
-to be removed for a certain proof and restored afterwards. The need of
-frequent additions or deletions may indicate a badly designed
-simpset.
-
-\begin{warn}
- The union of the parent simpsets (as described above) is not always
- a good starting point for the new theory. If some ancestors have
- deleted simplification rules because they are no longer wanted,
- while others have left those rules in, then the union will contain
- the unwanted rules. After this union is formed, changes to
- a parent simpset have no effect on the child simpset.
-\end{warn}
-
-
\section{Simplification sets}\index{simplification sets}
The simplifier is controlled by information contained in {\bf