doc-src/Ref/document/simplifier.tex

+
+\chapter{Simplification}
+\label{chap:simplification}
+\index{simplification|(}
+
+This chapter describes Isabelle's generic simplification package.  It performs
+conditional and unconditional rewriting and uses contextual information
+(`local assumptions').  It provides several general hooks, which can provide
+automatic case splits during rewriting, for example.  The simplifier is
+already set up for many of Isabelle's logics: FOL, ZF, HOL, HOLCF.
+
+The first section is a quick introduction to the simplifier that
+should be sufficient to get started.  The later sections explain more
+advanced features.
+
+
+\section{Simplification for dummies}
+\label{sec:simp-for-dummies}
+
+Basic use of the simplifier is particularly easy because each theory
+is equipped with sensible default information controlling the rewrite
+process --- namely the implicit {\em current
+  simpset}\index{simpset!current}.  A suite of simple commands is
+provided that refer to the implicit simpset of the current theory
+context.
+
+\begin{warn}
+  Make sure that you are working within the correct theory context.
+  Executing proofs interactively, or loading them from ML files
+  without associated theories may require setting the current theory
+  manually via the \ttindex{context} command.
+\end{warn}
+
+\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
+trace_simp        : bool ref \hfill{\bf initially false}
+debug_simp        : bool ref \hfill{\bf initially false}
+\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}.}
+\item[set \ttindexbold{trace_simp};] makes the simplifier output internal
+  operations.  This includes rewrite steps, but also bookkeeping like
+  modifications of the simpset.
+\item[set \ttindexbold{debug_simp};] makes the simplifier output some extra
+  information about internal operations.  This includes any attempted
+  invocation of simplification procedures.
+\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.
+
+\medskip
+
+Using the simplifier effectively may take a bit of experimentation.
+Set the \verb$trace_simp$\index{tracing!of simplification} flag to get
+a better idea of what is going on.  The resulting output can be
+enormous, especially since invocations of the simplifier are often
+nested (e.g.\ when solving conditions of rewrite rules).
+
+
+\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
+  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{Inspecting simpsets}
+\begin{ttbox}
+print_ss : simpset -> unit
+rep_ss   : simpset -> \{mss        : meta_simpset, 
+                       subgoal_tac: simpset  -> int -> tactic,
+                       loop_tacs  : (string * (int -> tactic))list,
+                       finish_tac : solver list,
+                unsafe_finish_tac : solver list\}
+\end{ttbox}
+\begin{ttdescription}
+  
+\item[\ttindexbold{print_ss} $ss$;] displays the printable contents of
+  simpset $ss$.  This includes the rewrite rules and congruences in
+  their internal form expressed as meta-equalities.  The names of the
+  simplification procedures and the patterns they are invoked on are
+  also shown.  The other parts, functions and tactics, are
+  non-printable.
+
+\item[\ttindexbold{rep_ss} $ss$;] decomposes $ss$ as a record of its internal 
+  components, namely the meta_simpset, the subgoaler, the loop, and the safe
+  and unsafe solvers.
+
+\end{ttdescription}
+
+
+\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}
+delsimps : simpset * thm list -> simpset \hfill{\bf infix 4}
+\end{ttbox}
+
+\index{rewrite rules|(} Rewrite rules are theorems expressing some
+form of equality, for example:
+\begin{eqnarray*}
+  Suc(\Var{m}) + \Var{n} &=&      \Var{m} + Suc(\Var{n}) \\
+  \Var{P}\conj\Var{P}    &\bimp&  \Var{P} \\
+  \Var{A} \un \Var{B} &\equiv& \{x.x\in \Var{A} \disj x\in \Var{B}\}
+\end{eqnarray*}
+Conditional rewrites such as $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} =
+0$ are also permitted; the conditions can be arbitrary formulas.
+
+Internally, all rewrite rules are translated into meta-equalities,
+theorems with conclusion $lhs \equiv rhs$.  Each simpset contains a
+function for extracting equalities from arbitrary theorems.  For
+example, $\neg(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\}
+\equiv False$.  This function can be installed using
+\ttindex{setmksimps} but only the definer of a logic should need to do
+this; see {\S}\ref{sec:setmksimps}.  The function processes theorems
+added by \texttt{addsimps} as well as local assumptions.
+
+\begin{ttdescription}
+  
+\item[$ss$ \ttindexbold{addsimps} $thms$] adds rewrite rules derived
+  from $thms$ to the simpset $ss$.
+  
+\item[$ss$ \ttindexbold{delsimps} $thms$] deletes rewrite rules
+  derived from $thms$ from the simpset $ss$.
+
+\end{ttdescription}
+
+\begin{warn}
+  The simplifier will accept all standard rewrite rules: those where
+  all unknowns are of base type.  Hence ${\Var{i}+(\Var{j}+\Var{k})} =
+  {(\Var{i}+\Var{j})+\Var{k}}$ is OK.
+  
+  It will also deal gracefully with all rules whose left-hand sides
+  are so-called {\em higher-order patterns}~\cite{nipkow-patterns}.
+  \indexbold{higher-order pattern}\indexbold{pattern, higher-order}
+  These are terms in $\beta$-normal form (this will always be the case
+  unless you have done something strange) where each occurrence of an
+  unknown is of the form $\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are
+  distinct bound variables. Hence $(\forall x.\Var{P}(x) \land
+  \Var{Q}(x)) \bimp (\forall x.\Var{P}(x)) \land (\forall
+  x.\Var{Q}(x))$ is also OK, in both directions.
+  
+  In some rare cases the rewriter will even deal with quite general
+  rules: for example ${\Var{f}(\Var{x})\in range(\Var{f})} = True$
+  rewrites $g(a) \in range(g)$ to $True$, but will fail to match
+  $g(h(b)) \in range(\lambda x.g(h(x)))$.  However, you can replace
+  the offending subterms (in our case $\Var{f}(\Var{x})$, which is not
+  a pattern) by adding new variables and conditions: $\Var{y} =
+  \Var{f}(\Var{x}) \Imp \Var{y}\in range(\Var{f}) = True$ is
+  acceptable as a conditional rewrite rule since conditions can be
+  arbitrary terms.
+  
+  There is basically no restriction on the form of the right-hand
+  sides.  They may not contain extraneous term or type variables,
+  though.
+\end{warn}
+\index{rewrite rules|)}
+
+
+\subsection{*The subgoaler}\label{sec:simp-subgoaler}
+\begin{ttbox}
+setsubgoaler :
+  simpset *  (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4}
+prems_of_ss  : simpset -> thm list
+\end{ttbox}
+
+The subgoaler is the tactic used to solve subgoals arising out of
+conditional rewrite rules or congruence rules.  The default should be
+simplification itself.  Occasionally this strategy needs to be
+changed.  For example, if the premise of a conditional rule is an
+instance of its conclusion, as in $Suc(\Var{m}) < \Var{n} \Imp \Var{m}
+< \Var{n}$, the default strategy could loop.
+
+\begin{ttdescription}
+  
+\item[$ss$ \ttindexbold{setsubgoaler} $tacf$] sets the subgoaler of
+  $ss$ to $tacf$.  The function $tacf$ will be applied to the current
+  simplifier context expressed as a simpset.
+  
+\item[\ttindexbold{prems_of_ss} $ss$] retrieves the current set of
+  premises from simplifier context $ss$.  This may be non-empty only
+  if the simplifier has been told to utilize local assumptions in the
+  first place, e.g.\ if invoked via \texttt{asm_simp_tac}.
+
+\end{ttdescription}
+
+As an example, consider the following subgoaler:
+\begin{ttbox}
+fun subgoaler ss =
+    assume_tac ORELSE'
+    resolve_tac (prems_of_ss ss) ORELSE'
+    asm_simp_tac ss;
+\end{ttbox}
+This tactic first tries to solve the subgoal by assumption or by
+resolving with with one of the premises, calling simplification only
+if that fails.
+
+
+\subsection{*The solver}\label{sec:simp-solver}
+\begin{ttbox}
+mk_solver  : string -> (thm list -> int -> tactic) -> solver
+setSolver  : simpset * solver -> simpset \hfill{\bf infix 4}
+addSolver  : simpset * solver -> simpset \hfill{\bf infix 4}
+setSSolver : simpset * solver -> simpset \hfill{\bf infix 4}
+addSSolver : simpset * solver -> simpset \hfill{\bf infix 4}
+\end{ttbox}
+
+A solver is a tactic that attempts to solve a subgoal after
+simplification.  Typically it just proves trivial subgoals such as
+\texttt{True} and $t=t$.  It could use sophisticated means such as {\tt
+  blast_tac}, though that could make simplification expensive.
+To keep things more abstract, solvers are packaged up in type
+\texttt{solver}. The only way to create a solver is via \texttt{mk_solver}.
+
+Rewriting does not instantiate unknowns.  For example, rewriting
+cannot prove $a\in \Var{A}$ since this requires
+instantiating~$\Var{A}$.  The solver, however, is an arbitrary tactic
+and may instantiate unknowns as it pleases.  This is the only way the
+simplifier can handle a conditional rewrite rule whose condition
+contains extra variables.  When a simplification tactic is to be
+combined with other provers, especially with the classical reasoner,
+it is important whether it can be considered safe or not.  For this
+reason a simpset contains two solvers, a safe and an unsafe one.
+
+The standard simplification strategy solely uses the unsafe solver,
+which is appropriate in most cases.  For special applications where
+the simplification process is not allowed to instantiate unknowns
+within the goal, simplification starts with the safe solver, but may
+still apply the ordinary unsafe one in nested simplifications for
+conditional rules or congruences. Note that in this way the overall
+tactic is not totally safe:  it may instantiate unknowns that appear also 
+in other subgoals.
+
+\begin{ttdescription}
+\item[\ttindexbold{mk_solver} $s$ $tacf$] converts $tacf$ into a new solver;
+  the string $s$ is only attached as a comment and has no other significance.
+
+\item[$ss$ \ttindexbold{setSSolver} $tacf$] installs $tacf$ as the
+  \emph{safe} solver of $ss$.
+  
+\item[$ss$ \ttindexbold{addSSolver} $tacf$] adds $tacf$ as an
+  additional \emph{safe} solver; it will be tried after the solvers
+  which had already been present in $ss$.
+  
+\item[$ss$ \ttindexbold{setSolver} $tacf$] installs $tacf$ as the
+  unsafe solver of $ss$.
+  
+\item[$ss$ \ttindexbold{addSolver} $tacf$] adds $tacf$ as an
+  additional unsafe solver; it will be tried after the solvers which
+  had already been present in $ss$.
+
+\end{ttdescription}
+
+\medskip
+
+\index{assumptions!in simplification} The solver tactic is invoked
+with a list of theorems, namely assumptions that hold in the local
+context.  This may be non-empty only if the simplifier has been told
+to utilize local assumptions in the first place, e.g.\ if invoked via
+\texttt{asm_simp_tac}.  The solver is also presented the full goal
+including its assumptions in any case.  Thus it can use these (e.g.\ 
+by calling \texttt{assume_tac}), even if the list of premises is not
+passed.
+
+\medskip
+
+As explained in {\S}\ref{sec:simp-subgoaler}, the subgoaler is also used
+to solve the premises of congruence rules.  These are usually of the
+form $s = \Var{x}$, where $s$ needs to be simplified and $\Var{x}$
+needs to be instantiated with the result.  Typically, the subgoaler
+will invoke the simplifier at some point, which will eventually call
+the solver.  For this reason, solver tactics must be prepared to solve
+goals of the form $t = \Var{x}$, usually by reflexivity.  In
+particular, reflexivity should be tried before any of the fancy
+tactics like \texttt{blast_tac}.
+
+It may even happen that due to simplification the subgoal is no longer
+an equality.  For example $False \bimp \Var{Q}$ could be rewritten to
+$\neg\Var{Q}$.  To cover this case, the solver could try resolving
+with the theorem $\neg False$.
+
+\medskip
+
+\begin{warn}
+  If a premise of a congruence rule cannot be proved, then the
+  congruence is ignored.  This should only happen if the rule is
+  \emph{conditional} --- that is, contains premises not of the form $t
+  = \Var{x}$; otherwise it indicates that some congruence rule, or
+  possibly the subgoaler or solver, is faulty.
+\end{warn}
+
+
+\subsection{*The looper}\label{sec:simp-looper}
+\begin{ttbox}
+setloop   : simpset *           (int -> tactic)  -> simpset \hfill{\bf infix 4}
+addloop   : simpset * (string * (int -> tactic)) -> simpset \hfill{\bf infix 4}
+delloop   : simpset *  string                    -> simpset \hfill{\bf infix 4}
+addsplits : simpset * thm list -> simpset \hfill{\bf infix 4}
+delsplits : simpset * thm list -> simpset \hfill{\bf infix 4}
+\end{ttbox}
+
+The looper is a list of tactics that are applied after simplification, in case
+the solver failed to solve the simplified goal.  If the looper
+succeeds, the simplification process is started all over again.  Each
+of the subgoals generated by the looper is attacked in turn, in
+reverse order.
+
+A typical looper is \index{case splitting}: the expansion of a conditional.
+Another possibility is to apply an elimination rule on the
+assumptions.  More adventurous loopers could start an induction.
+
+\begin{ttdescription}
+  
+\item[$ss$ \ttindexbold{setloop} $tacf$] installs $tacf$ as the only looper
+  tactic of $ss$.
+  
+\item[$ss$ \ttindexbold{addloop} $(name,tacf)$] adds $tacf$ as an additional
+  looper tactic with name $name$; it will be tried after the looper tactics
+  that had already been present in $ss$.
+  
+\item[$ss$ \ttindexbold{delloop} $name$] deletes the looper tactic $name$
+  from $ss$.
+  
+\item[$ss$ \ttindexbold{addsplits} $thms$] adds
+  split tactics for $thms$ as additional looper tactics of $ss$.
+
+\item[$ss$ \ttindexbold{addsplits} $thms$] deletes the
+  split tactics for $thms$ from the looper tactics of $ss$.
+
+\end{ttdescription}
+
+The splitter replaces applications of a given function; the right-hand side
+of the replacement can be anything.  For example, here is a splitting rule
+for conditional expressions:
+\[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x}))
+\conj (\neg\Var{Q} \imp \Var{P}(\Var{y})) 
+\] 
+Another example is the elimination operator for Cartesian products (which
+happens to be called~$split$):  
+\[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} =
+\langle a,b\rangle \imp \Var{P}(\Var{f}(a,b))) 
+\] 
+
+For technical reasons, there is a distinction between case splitting in the 
+conclusion and in the premises of a subgoal. The former is done by
+\texttt{split_tac} with rules like \texttt{split_if} or \texttt{option.split}, 
+which do not split the subgoal, while the latter is done by 
+\texttt{split_asm_tac} with rules like \texttt{split_if_asm} or 
+\texttt{option.split_asm}, which split the subgoal.
+The operator \texttt{addsplits} automatically takes care of which tactic to
+call, analyzing the form of the rules given as argument.
+\begin{warn}
+Due to \texttt{split_asm_tac}, the simplifier may split subgoals!
+\end{warn}
+
+Case splits should be allowed only when necessary; they are expensive
+and hard to control.  Here is an example of use, where \texttt{split_if}
+is the first rule above:
+\begin{ttbox}
+by (simp_tac (simpset() 
+                 addloop ("split if", split_tac [split_if])) 1);
+\end{ttbox}
+Users would usually prefer the following shortcut using \texttt{addsplits}:
+\begin{ttbox}
+by (simp_tac (simpset() addsplits [split_if]) 1);
+\end{ttbox}
+Case-splitting on conditional expressions is usually beneficial, so it is
+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}
+
+\medskip
+
+Local modifications of simpsets within a proof are often much cleaner
+by using above tactics in conjunction with explicit simpsets, rather
+than their capitalized counterparts.  For example
+\begin{ttbox}
+Addsimps \(thms\);
+by (Simp_tac \(i\));
+Delsimps \(thms\);
+\end{ttbox}
+can be expressed more appropriately as
+\begin{ttbox}
+by (simp_tac (simpset() addsimps \(thms\)) \(i\));
+\end{ttbox}
+
+\medskip
+
+Also note that functions depending implicitly on the current theory
+context (like capital \texttt{Simp_tac} and the other commands of
+{\S}\ref{sec:simp-for-dummies}) should be considered harmful outside of
+actual proof scripts.  In particular, ML programs like theory
+definition packages or special tactics should refer to simpsets only
+explicitly, via the above tactics used in conjunction with
+\texttt{simpset_of} or the \texttt{SIMPSET} tacticals.
+
+
+\section{Forward rules and conversions}
+\index{simplification!forward rules}\index{simplification!conversions}
+\begin{ttbox}\index{*simplify}\index{*asm_simplify}\index{*full_simplify}\index{*asm_full_simplify}\index{*Simplifier.rewrite}\index{*Simplifier.asm_rewrite}\index{*Simplifier.full_rewrite}\index{*Simplifier.asm_full_rewrite}
+simplify          : simpset -> thm -> thm
+asm_simplify      : simpset -> thm -> thm
+full_simplify     : simpset -> thm -> thm
+asm_full_simplify : simpset -> thm -> thm\medskip
+Simplifier.rewrite           : simpset -> cterm -> thm
+Simplifier.asm_rewrite       : simpset -> cterm -> thm
+Simplifier.full_rewrite      : simpset -> cterm -> thm
+Simplifier.asm_full_rewrite  : simpset -> cterm -> thm
+\end{ttbox}
+
+The first four of these functions provide \emph{forward} rules for
+simplification.  Their effect is analogous to the corresponding
+tactics described in {\S}\ref{simp-tactics}, but affect the whole
+theorem instead of just a certain subgoal.  Also note that the
+looper~/ solver process as described in {\S}\ref{sec:simp-looper} and
+{\S}\ref{sec:simp-solver} is omitted in forward simplification.
+
+The latter four are \emph{conversions}, establishing proven equations
+of the form $t \equiv u$ where the l.h.s.\ $t$ has been given as
+argument.
+
+\begin{warn}
+  Forward simplification rules and conversions should be used rarely
+  in ordinary proof scripts.  The main intention is to provide an
+  internal interface to the simplifier for special utilities.
+\end{warn}
+
+
+\section{Permutative rewrite rules}
+\index{rewrite rules!permutative|(}
+
+A rewrite rule is {\bf permutative} if the left-hand side and right-hand
+side are the same up to renaming of variables.  The most common permutative
+rule is commutativity: $x+y = y+x$.  Other examples include $(x-y)-z =
+(x-z)-y$ in arithmetic and $insert(x,insert(y,A)) = insert(y,insert(x,A))$
+for sets.  Such rules are common enough to merit special attention.
+
+Because ordinary rewriting loops given such rules, the simplifier
+employs a special strategy, called {\bf ordered
+  rewriting}\index{rewriting!ordered}.  There is a standard
+lexicographic ordering on terms.  This should be perfectly OK in most
+cases, but can be changed for special applications.
+
+\begin{ttbox}
+settermless : simpset * (term * term -> bool) -> simpset \hfill{\bf infix 4}
+\end{ttbox}
+\begin{ttdescription}
+  
+\item[$ss$ \ttindexbold{settermless} $rel$] installs relation $rel$ as
+  term order in simpset $ss$.
+
+\end{ttdescription}
+
+\medskip
+
+A permutative rewrite rule is applied only if it decreases the given
+term with respect to this ordering.  For example, commutativity
+rewrites~$b+a$ to $a+b$, but then stops because $a+b$ is strictly less
+than $b+a$.  The Boyer-Moore theorem prover~\cite{bm88book} also
+employs ordered rewriting.
+
+Permutative rewrite rules are added to simpsets just like other
+rewrite rules; the simplifier recognizes their special status
+automatically.  They are most effective in the case of
+associative-commutative operators.  (Associativity by itself is not
+permutative.)  When dealing with an AC-operator~$f$, keep the
+following points in mind:
+\begin{itemize}\index{associative-commutative operators}
+  
+\item The associative law must always be oriented from left to right,
+  namely $f(f(x,y),z) = f(x,f(y,z))$.  The opposite orientation, if
+  used with commutativity, leads to looping in conjunction with the
+  standard term order.
+
+\item To complete your set of rewrite rules, you must add not just
+  associativity~(A) and commutativity~(C) but also a derived rule, {\bf
+    left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
+\end{itemize}
+Ordered rewriting with the combination of A, C, and~LC sorts a term
+lexicographically:
+\[\def\maps#1{\stackrel{#1}{\longmapsto}}
+ (b+c)+a \maps{A} b+(c+a) \maps{C} b+(a+c) \maps{LC} a+(b+c) \]
+Martin and Nipkow~\cite{martin-nipkow} discuss the theory and give many
+examples; other algebraic structures are amenable to ordered rewriting,
+such as boolean rings.
+
+\subsection{Example: sums of natural numbers}
+
+This example is again set in HOL (see \texttt{HOL/ex/NatSum}).  Theory
+\thydx{Arith} contains natural numbers arithmetic.  Its associated simpset
+contains many arithmetic laws including distributivity of~$\times$ over~$+$,
+while \texttt{add_ac} is a list consisting of the A, C and LC laws for~$+$ on
+type \texttt{nat}.  Let us prove the theorem
+\[ \sum@{i=1}^n i = n\times(n+1)/2. \]
+%
+A functional~\texttt{sum} represents the summation operator under the
+interpretation $\texttt{sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$.  We
+extend \texttt{Arith} as follows:
+\begin{ttbox}
+NatSum = Arith +
+consts sum     :: [nat=>nat, nat] => nat
+primrec 
+  "sum f 0 = 0"
+  "sum f (Suc n) = f(n) + sum f n"
+end
+\end{ttbox}
+The \texttt{primrec} declaration automatically adds rewrite rules for
+\texttt{sum} to the default simpset.  We now remove the
+\texttt{nat_cancel} simplification procedures (in order not to spoil
+the example) and insert the AC-rules for~$+$:
+\begin{ttbox}
+Delsimprocs nat_cancel;
+Addsimps add_ac;
+\end{ttbox}
+Our desired theorem now reads $\texttt{sum} \, (\lambda i.i) \, (n+1) =
+n\times(n+1)/2$.  The Isabelle goal has both sides multiplied by~$2$:
+\begin{ttbox}
+Goal "2 * sum (\%i.i) (Suc n) = n * Suc n";
+{\out Level 0}
+{\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
+{\out  1. 2 * sum (\%i. i) (Suc n) = n * Suc n}
+\end{ttbox}
+Induction should not be applied until the goal is in the simplest
+form:
+\begin{ttbox}
+by (Simp_tac 1);
+{\out Level 1}
+{\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
+{\out  1. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n}
+\end{ttbox}
+Ordered rewriting has sorted the terms in the left-hand side.  The
+subgoal is now ready for induction:
+\begin{ttbox}
+by (induct_tac "n" 1);
+{\out Level 2}
+{\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
+{\out  1. 0 + (sum (\%i. i) 0 + sum (\%i. i) 0) = 0 * 0}
+\ttbreak
+{\out  2. !!n. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n}
+{\out           ==> Suc n + (sum (\%i. i) (Suc n) + sum (\%i.\,i) (Suc n)) =}
+{\out               Suc n * Suc n}
+\end{ttbox}
+Simplification proves both subgoals immediately:\index{*ALLGOALS}
+\begin{ttbox}
+by (ALLGOALS Asm_simp_tac);
+{\out Level 3}
+{\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
+{\out No subgoals!}
+\end{ttbox}
+Simplification cannot prove the induction step if we omit \texttt{add_ac} from
+the simpset.  Observe that like terms have not been collected:
+\begin{ttbox}
+{\out Level 3}
+{\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
+{\out  1. !!n. n + sum (\%i. i) n + (n + sum (\%i. i) n) = n + n * n}
+{\out           ==> n + (n + sum (\%i. i) n) + (n + (n + sum (\%i.\,i) n)) =}
+{\out               n + (n + (n + n * n))}
+\end{ttbox}
+Ordered rewriting proves this by sorting the left-hand side.  Proving
+arithmetic theorems without ordered rewriting requires explicit use of
+commutativity.  This is tedious; try it and see!
+
+Ordered rewriting is equally successful in proving
+$\sum@{i=1}^n i^3 = n^2\times(n+1)^2/4$.
+
+
+\subsection{Re-orienting equalities}
+Ordered rewriting with the derived rule \texttt{symmetry} can reverse
+equations:
+\begin{ttbox}
+val symmetry = prove_goal HOL.thy "(x=y) = (y=x)"
+                 (fn _ => [Blast_tac 1]);
+\end{ttbox}
+This is frequently useful.  Assumptions of the form $s=t$, where $t$ occurs
+in the conclusion but not~$s$, can often be brought into the right form.
+For example, ordered rewriting with \texttt{symmetry} can prove the goal
+\[ f(a)=b \conj f(a)=c \imp b=c. \]
+Here \texttt{symmetry} reverses both $f(a)=b$ and $f(a)=c$
+because $f(a)$ is lexicographically greater than $b$ and~$c$.  These
+re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the
+conclusion by~$f(a)$. 
+
+Another example is the goal $\neg(t=u) \imp \neg(u=t)$.
+The differing orientations make this appear difficult to prove.  Ordered
+rewriting with \texttt{symmetry} makes the equalities agree.  (Without
+knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$
+or~$u=t$.)  Then the simplifier can prove the goal outright.
+
+\index{rewrite rules!permutative|)}
+
+
+\section{*Setting up the Simplifier}\label{sec:setting-up-simp}
+\index{simplification!setting up}
+
+Setting up the simplifier for new logics is complicated in the general case.
+This section describes how the simplifier is installed for intuitionistic
+first-order logic; the code is largely taken from {\tt FOL/simpdata.ML} of the
+Isabelle sources.
+
+The case splitting tactic, which resides on a separate files, is not part of
+Pure Isabelle.  It needs to be loaded explicitly by the object-logic as
+follows (below \texttt{\~\relax\~\relax} refers to \texttt{\$ISABELLE_HOME}):
+\begin{ttbox}
+use "\~\relax\~\relax/src/Provers/splitter.ML";
+\end{ttbox}
+
+Simplification requires converting object-equalities to meta-level rewrite
+rules.  This demands rules stating that equal terms and equivalent formulae
+are also equal at the meta-level.  The rule declaration part of the file
+\texttt{FOL/IFOL.thy} contains the two lines
+\begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem}
+eq_reflection   "(x=y)   ==> (x==y)"
+iff_reflection  "(P<->Q) ==> (P==Q)"
+\end{ttbox}
+Of course, you should only assert such rules if they are true for your
+particular logic.  In Constructive Type Theory, equality is a ternary
+relation of the form $a=b\in A$; the type~$A$ determines the meaning
+of the equality essentially as a partial equivalence relation.  The
+present simplifier cannot be used.  Rewriting in \texttt{CTT} uses
+another simplifier, which resides in the file {\tt
+  Provers/typedsimp.ML} and is not documented.  Even this does not
+work for later variants of Constructive Type Theory that use
+intensional equality~\cite{nordstrom90}.
+
+
+\subsection{A collection of standard rewrite rules}
+
+We first prove lots of standard rewrite rules about the logical
+connectives.  These include cancellation and associative laws.  We
+define a function that echoes the desired law and then supplies it the
+prover for intuitionistic FOL:
+\begin{ttbox}
+fun int_prove_fun s = 
+ (writeln s;  
+  prove_goal IFOL.thy s
+   (fn prems => [ (cut_facts_tac prems 1), 
+                  (IntPr.fast_tac 1) ]));
+\end{ttbox}
+The following rewrite rules about conjunction are a selection of those
+proved on \texttt{FOL/simpdata.ML}.  Later, these will be supplied to the
+standard simpset.
+\begin{ttbox}
+val conj_simps = map int_prove_fun
+ ["P & True <-> P",      "True & P <-> P",
+  "P & False <-> False", "False & P <-> False",
+  "P & P <-> P",
+  "P & ~P <-> False",    "~P & P <-> False",
+  "(P & Q) & R <-> P & (Q & R)"];
+\end{ttbox}
+The file also proves some distributive laws.  As they can cause exponential
+blowup, they will not be included in the standard simpset.  Instead they
+are merely bound to an \ML{} identifier, for user reference.
+\begin{ttbox}
+val distrib_simps  = map int_prove_fun
+ ["P & (Q | R) <-> P&Q | P&R", 
+  "(Q | R) & P <-> Q&P | R&P",
+  "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
+\end{ttbox}
+
+
+\subsection{Functions for preprocessing the rewrite rules}
+\label{sec:setmksimps}
+\begin{ttbox}\indexbold{*setmksimps}
+setmksimps : simpset * (thm -> thm list) -> simpset \hfill{\bf infix 4}
+\end{ttbox}
+The next step is to define the function for preprocessing rewrite rules.
+This will be installed by calling \texttt{setmksimps} below.  Preprocessing
+occurs whenever rewrite rules are added, whether by user command or
+automatically.  Preprocessing involves extracting atomic rewrites at the
+object-level, then reflecting them to the meta-level.
+
+To start, the function \texttt{gen_all} strips any meta-level
+quantifiers from the front of the given theorem.
+
+The function \texttt{atomize} analyses a theorem in order to extract
+atomic rewrite rules.  The head of all the patterns, matched by the
+wildcard~\texttt{_}, is the coercion function \texttt{Trueprop}.
+\begin{ttbox}
+fun atomize th = case concl_of th of 
+    _ $ (Const("op &",_) $ _ $ _)   => atomize(th RS conjunct1) \at
+                                       atomize(th RS conjunct2)
+  | _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)
+  | _ $ (Const("All",_) $ _)        => atomize(th RS spec)
+  | _ $ (Const("True",_))           => []
+  | _ $ (Const("False",_))          => []
+  | _                               => [th];
+\end{ttbox}
+There are several cases, depending upon the form of the conclusion:
+\begin{itemize}
+\item Conjunction: extract rewrites from both conjuncts.
+\item Implication: convert $P\imp Q$ to the meta-implication $P\Imp Q$ and
+  extract rewrites from~$Q$; these will be conditional rewrites with the
+  condition~$P$.
+\item Universal quantification: remove the quantifier, replacing the bound
+  variable by a schematic variable, and extract rewrites from the body.
+\item \texttt{True} and \texttt{False} contain no useful rewrites.
+\item Anything else: return the theorem in a singleton list.
+\end{itemize}
+The resulting theorems are not literally atomic --- they could be
+disjunctive, for example --- but are broken down as much as possible. 
+See the file \texttt{ZF/simpdata.ML} for a sophisticated translation of
+set-theoretic formulae into rewrite rules. 
+
+For standard situations like the above,
+there is a generic auxiliary function \ttindexbold{mk_atomize} that takes a 
+list of pairs $(name, thms)$, where $name$ is an operator name and
+$thms$ is a list of theorems to resolve with in case the pattern matches, 
+and returns a suitable \texttt{atomize} function.
+
+
+The simplified rewrites must now be converted into meta-equalities.  The
+rule \texttt{eq_reflection} converts equality rewrites, while {\tt
+  iff_reflection} converts if-and-only-if rewrites.  The latter possibility
+can arise in two other ways: the negative theorem~$\neg P$ is converted to
+$P\equiv\texttt{False}$, and any other theorem~$P$ is converted to
+$P\equiv\texttt{True}$.  The rules \texttt{iff_reflection_F} and {\tt
+  iff_reflection_T} accomplish this conversion.
+\begin{ttbox}
+val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
+val iff_reflection_F = P_iff_F RS iff_reflection;
+\ttbreak
+val P_iff_T = int_prove_fun "P ==> (P <-> True)";
+val iff_reflection_T = P_iff_T RS iff_reflection;
+\end{ttbox}
+The function \texttt{mk_eq} converts a theorem to a meta-equality
+using the case analysis described above.
+\begin{ttbox}
+fun mk_eq th = case concl_of th of
+    _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
+  | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
+  | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
+  | _                           => th RS iff_reflection_T;
+\end{ttbox}
+The 
+three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_eq} 
+will be composed together and supplied below to \texttt{setmksimps}.
+
+
+\subsection{Making the initial simpset}
+
+It is time to assemble these items.  The list \texttt{IFOL_simps} contains the
+default rewrite rules for intuitionistic first-order logic.  The first of
+these is the reflexive law expressed as the equivalence
+$(a=a)\bimp\texttt{True}$; the rewrite rule $a=a$ is clearly useless.
+\begin{ttbox}
+val IFOL_simps =
+   [refl RS P_iff_T] \at conj_simps \at disj_simps \at not_simps \at 
+    imp_simps \at iff_simps \at quant_simps;
+\end{ttbox}
+The list \texttt{triv_rls} contains trivial theorems for the solver.  Any
+subgoal that is simplified to one of these will be removed.
+\begin{ttbox}
+val notFalseI = int_prove_fun "~False";
+val triv_rls = [TrueI,refl,iff_refl,notFalseI];
+\end{ttbox}
+We also define the function \ttindex{mk_meta_cong} to convert the conclusion
+of congruence rules into meta-equalities.
+\begin{ttbox}
+fun mk_meta_cong rl = standard (mk_meta_eq (mk_meta_prems rl));
+\end{ttbox}
+%
+The basic simpset for intuitionistic FOL is \ttindexbold{FOL_basic_ss}.  It
+preprocess rewrites using 
+{\tt gen_all}, \texttt{atomize} and \texttt{mk_eq}.
+It solves simplified subgoals using \texttt{triv_rls} and assumptions, and by
+detecting contradictions.  It uses \ttindex{asm_simp_tac} to tackle subgoals
+of conditional rewrites.
+
+Other simpsets built from \texttt{FOL_basic_ss} will inherit these items.
+In particular, \ttindexbold{IFOL_ss}, which introduces {\tt
+  IFOL_simps} as rewrite rules.  \ttindexbold{FOL_ss} will later
+extend \texttt{IFOL_ss} with classical rewrite rules such as $\neg\neg
+P\bimp P$.
+\index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler}
+\index{*addsimps}\index{*addcongs}
+\begin{ttbox}
+fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls {\at} prems),
+                                 atac, etac FalseE];
+
+fun safe_solver prems = FIRST'[match_tac (triv_rls {\at} prems),
+                               eq_assume_tac, ematch_tac [FalseE]];
+
+val FOL_basic_ss =
+      empty_ss setsubgoaler asm_simp_tac
+               addsimprocs [defALL_regroup, defEX_regroup]
+               setSSolver   safe_solver
+               setSolver  unsafe_solver
+               setmksimps (map mk_eq o atomize o gen_all)
+               setmkcong mk_meta_cong;
+
+val IFOL_ss = 
+      FOL_basic_ss addsimps (IFOL_simps {\at} 
+                             int_ex_simps {\at} int_all_simps)
+                   addcongs [imp_cong];
+\end{ttbox}
+This simpset takes \texttt{imp_cong} as a congruence rule in order to use
+contextual information to simplify the conclusions of implications:
+\[ \List{\Var{P}\bimp\Var{P'};\; \Var{P'} \Imp \Var{Q}\bimp\Var{Q'}} \Imp
+   (\Var{P}\imp\Var{Q}) \bimp (\Var{P'}\imp\Var{Q'})
+\]
+By adding the congruence rule \texttt{conj_cong}, we could obtain a similar
+effect for conjunctions.
+
+
+\index{simplification|)}
+
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "ref"
+%%% End: