--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Ref/document/simplifier.tex Tue Aug 28 18:57:32 2012 +0200
@@ -0,0 +1,1032 @@
+
+\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: