# HG changeset patch # User wenzelm # Date 1352055113 -3600 # Node ID 7c01dc2dcb8c92868070778877de6ba1698a8964 # Parent e08cc8b2056496107bb2a1dc45ef8ff893070846 more on Simplifier rules, based on old material; diff -r e08cc8b20564 -r 7c01dc2dcb8c src/Doc/IsarRef/Generic.thy --- 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 \ 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 \ ?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} *} diff -r e08cc8b20564 -r 7c01dc2dcb8c src/Doc/Ref/document/simplifier.tex --- 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