author wenzelm Fri, 12 Dec 1997 17:11:05 +0100 changeset 4395 a2b726277050 parent 4394 c24a1bbd3cf3 child 4396 d103e5e164f8
major update;
--- a/doc-src/Ref/simplifier.tex	Fri Dec 12 17:10:40 1997 +0100
+++ b/doc-src/Ref/simplifier.tex	Fri Dec 12 17:11:05 1997 +0100
@@ -3,204 +3,383 @@
\label{chap:simplification}
\index{simplification|(}

-This chapter describes Isabelle's generic simplification package, which
-provides a suite of simplification tactics.  It performs conditional and
-unconditional rewriting and uses contextual information (local
-assumptions').  It provides a few general hooks, which can provide
-automatic case splits during rewriting, for example.  The simplifier is set
-up for many of Isabelle's logics: \FOL, \ZF, \HOL\ and \HOLCF.
+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 next section is a quick introduction to the simplifier, the later
+The first section is a quick introduction to the simplifier that
+should be sufficient to get started.  The later sections explain more
+

\section{Simplification for dummies}
\label{sec:simp-for-dummies}

-In some logics (\FOL, {\HOL} and \ZF), the simplifier is particularly easy to
-use because it supports the concept of a {\em current
-  simpset}\index{simpset!current}.  This is a default set of simplification
-rules.  All commands are interpreted relative to the current simpset.  For
-example, in the theory of arithmetic the goal
+Basic use of the simplifier is particularly easy because each theory
+is equipped with an implicit {\em current
+  simpset}\index{simpset!current}.  This provides sensible default
+information in many cases.  A suite of commands refer to the implicit
+simpset of the current theory context.
+
+\begin{warn}
+  Make sure that you are working within the correct theory context.
+  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}
+\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 one by one.  Working from
+  \emph{left to right}, it uses each assumption in the simplification
+  of those following.
+
+\item[set \ttindexbold{trace_simp};] makes the simplifier output
+  internal operations.  This includes rewrite steps, but also
+  bookkeeping like modifications of the simpset.
+\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 Arith.thy "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}
-can be solved by a single
-\begin{ttbox}
-by (Simp_tac 1);
-\end{ttbox}
-The simplifier uses the current simpset, which in the case of arithmetic
-contains the required theorems $\Var{n}+0 = \Var{n}$ and $0+\Var{n} = + +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}$. -If assumptions of the subgoal are also needed in the simplification -process, as in +\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} -\end{ttbox} -then there is the more powerful -\begin{ttbox} by (Asm_simp_tac 1); \end{ttbox} -which solves the above goal. -There are four basic simplification tactics: -\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 solver. - -\item[\ttindexbold{Asm_simp_tac}]\index{assumptions!in simplification} - is like \verb$Simp_tac$, but extracts additional rewrite rules from the - assumptions. - -\item[\ttindexbold{Full_simp_tac}] is like \verb$Simp_tac$, but also - simplifies the assumptions (but 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 one by - one. {\em Working from left to right, it uses each assumption in the - simplification of those following.} -\end{ttdescription} - -{\tt Asm_full_simp_tac} is the most powerful of this quartet but may also -loop where some of the others terminate. For example, +\medskip {\tt 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} +{\out 1. ALL x. f x = g (f (g x)) ==> f 0 = f 0 + 0} \end{ttbox} -is solved by {\tt Simp_tac}, but {\tt Asm_simp_tac} and {\tt Asm_simp_tac} -loop because the rewrite rule$f(\Var{x}) = f(g(f(\Var{x})))$extracted from -the assumption does not terminate. Isabelle notices certain simple forms of -nontermination, but not this one. +is solved by {\tt Simp_tac}, but {\tt Asm_simp_tac} and {\tt + Asm_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. \begin{warn} Since \verb$Asm_full_simp_tac$works from left to right, it sometimes misses opportunities for simplification: given the subgoal \begin{ttbox} -{\out [| P(f(a)); f(a) = t |] ==> ...} +{\out [| P (f a); f a = t |] ==> \dots} \end{ttbox} \verb$Asm_full_simp_tac$will not simplify the first assumption using the second but will leave the assumptions unchanged. See \S\ref{sec:reordering-asms} for ways around this problem. \end{warn} +\medskip + Using the simplifier effectively may take a bit of experimentation. -\index{tracing!of simplification}\index{*trace_simp} The tactics can -be traced by setting \verb$trace_simp$. +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 +\end{ttbox} -There is not just one global current simpset, but one associated with each -theory as well. How are these simpset built up? -\begin{enumerate} -\item When loading {\tt T.thy}, the current simpset is initialized with the - union of the simpsets associated with all the ancestors of {\tt T}. In - addition, certain constructs in {\tt T} may add new rules to the simpset, - e.g.\ \ttindex{datatype} and \ttindex{primrec} in \HOL. Definitions are not - added automatically! -\item The script in {\tt T.ML} may manipulate the current simpset further by - explicitly adding/deleting theorems to/from it (see below). -\item After {\tt T.ML} has been read, the current simpset is associated with - theory {\tt T}. -\end{enumerate} -The current simpset is manipulated by -\begin{ttbox} -Addsimps, Delsimps: 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$thms$to the current simpset -\item[\ttindexbold{Delsimps}$thms$] deletes$thms$from the current simpset + +\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 to the + current simpset. + \end{ttdescription} -Generally useful simplification rules$\Var{n}+0 = \Var{n}$should be added -to the current simpset right after they have been proved. Those of a more -specific nature (e.g.\ the laws of de~Morgan, which alter the structure of a -formula) should only be added for specific proofs and deleted again -afterwards. Conversely, it may also happen that a generally useful rule needs -to be removed for a certain proof and is added again afterwards. Well -designed simpsets need few temporary additions or deletions. +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. As a rule of thump, generally +useful simplification rules'' like$\Var{n}+0 = \Var{n}$should be +added to the current simpset right after they have been proved. Those +of a more specific nature (e.g.\ the laws of de~Morgan, which alter +the structure of a formula) should only be added for specific proofs +and deleted again afterwards. Conversely, it may also happen that a +generally useful rule needs to be removed for a certain proof and is +added again afterwards. The need of frequent temporary additions or +deletions may indicate a badly designed simpset. \begin{warn} - The union of the ancestor simpsets (as described above) is not always a good - simpset 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. If the ancestor - simpsets differ in other components (the subgoaler, solver, looper or rule - preprocessor: see below), then you cannot be sure which version of that - component will be inherited. You may have to set the component explicitly - for the new theory's simpset by an assignment of the form - {\tt simpset := \dots}. -\end{warn} - -\begin{warn} - If you execute proofs interactively, or load them from an ML file without - associated {\tt .thy} file, you must set the current simpset by calling - \ttindex{set_current_thy}~{\tt"}$T${\tt"}, where$T$is the name of the - theory you want to work in. If you have just loaded$T$, this is not - necessary. + 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. \end{warn} \section{Simplification sets}\index{simplification sets} -The simplification tactics are controlled by {\bf simpsets}. These -consist of several components, including rewrite rules, congruence -rules, the subgoaler, the solver and the looper. The simplifier -should be set up with sensible defaults so that most simplifier calls -specify only rewrite rules. Experienced users can exploit the other -components to streamline proofs. + +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 +\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. + +\end{ttdescription} + -Logics like \HOL, which support a current -simpset\index{simpset!current}, store its value in an ML reference -variable called {\tt simpset}\index{simpset@{\tt simpset} ML value}. +\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 simply inherited + from either simpset. + +\end{ttdescription} + + +\subsection{Accessing the current simpset} + +\begin{ttbox} +simpset : unit -> simpset +simpset_ref : unit -> simpset ref +simpset_of : theory -> simpset +simpset_ref_of : theory -> simpset ref +print_simpset : theory -> unit +\end{ttbox} + +Each theory contains a current simpset\index{simpset!current} stored +within a private ML reference variable. This can be retrieved and +modified as follows. + +\begin{ttdescription} + +\item[\ttindexbold{simpset}();] retrieves the simpset value from the + current theory context. + +\item[\ttindexbold{simpset_ref}();] retrieves the simpset reference + variable from the current theory context. This can be assigned to + by using \texttt{:=} in ML. + +\item[\ttindexbold{simpset_of}$thy$;] retrieves the simpset value + from theory$thy$. + +\item[\ttindexbold{simpset_ref_of}$thy$;] retrieves the simpset + reference variable from theory$thy$. + +\item[\ttindexbold{print_simpset}$thy$;] prints the current simpset + of theory$thy$in the same way as \texttt{print_ss}. + +\end{ttdescription} + \subsection{Rewrite rules} -\index{rewrite rules|(} -Rewrite rules are theorems expressing some form of equality: +\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 permitted; the conditions can be arbitrary formulas. +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}.
-local assumptions.
+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

+\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 no restriction on the form of the right-hand sides.
+  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{*Congruence rules}\index{congruence rules}
+
+\subsection{Simplification procedures}
+\begin{ttbox}
+addsimprocs : simpset * simproc list -> simpset
+delsimprocs : simpset * simproc list -> simpset
+\end{ttbox}
+
+Simplification procedures are {\ML} functions that may produce
+\emph{proven} rewrite rules on demand.  They are associated with
+certain patterns that conceptually represent left-hand sides of
+equations; these are shown by \texttt{print_ss}.  During its
+operation, the simplifier may offer a simplification procedure the
+current redex and ask for a suitable rewrite rule.  Thus rules may be
+specifically fashioned for particular situations, resulting in a more
+powerful mechanism than term rewriting by a fixed set of rules.
+
+
+\begin{ttdescription}
+
+\item[$ss$ \ttindexbold{addsimprocs} $procs$] adds simplification
+  procedures $procs$ to the current simpset.
+
+\item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes simplification
+  procedures $procs$ from the current simpset.
+
+\end{ttdescription}
+
+
+\subsection{*Congruence rules}\index{congruence rules}\label{sec:simp-congs}
+\begin{ttbox}
+addcongs   : simpset * thm list -> simpset \hfill{\bf infix 4}
+delcongs   : simpset * thm list -> simpset \hfill{\bf infix 4}
+addeqcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
+deleqcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
+\end{ttbox}
+
Congruence rules are meta-equalities of the form
$\dots \Imp f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}). @@ -210,13 +389,36 @@ \[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}} \Imp (\Var{P@1} \imp \Var{P@2}) \equiv (\Var{Q@1} \imp \Var{Q@2})$
-Given this rule, the simplifier assumes $Q@1$ and extracts rewrite rules
-from it when simplifying~$P@2$.  Such local assumptions are effective for
-rewriting formulae such as $x=0\imp y+x=y$.  The local assumptions are also
-provided as theorems to the solver; see page~\pageref{sec:simp-solver} below.
+Given this rule, the simplifier assumes $Q@1$ and extracts rewrite
+rules from it when simplifying~$P@2$.  Such local assumptions are
+effective for rewriting formulae such as $x=0\imp y+x=y$.  The local
+assumptions are also provided as theorems to the solver; see
+\S~\ref{sec:simp-solver} below.

-Here are some more examples.  The congruence rule for bounded quantifiers
-also supplies contextual information, this time about the bound variable:
+\begin{ttdescription}
+
+\item[$ss$ \ttindexbold{addcongs} $thms$] adds congruence rules to the
+  simpset $ss$.  These are derived from $thms$ in an appropriate way,
+  depending on the underlying object-logic.
+
+\item[$ss$ \ttindexbold{delcongs} $thms$] deletes congruence rules
+  derived from $thms$.
+
+\item[$ss$ \ttindexbold{addeqcongs} $thms$] adds congruence rules in
+  their internal form (conclusions using meta-equality) to simpset
+  $ss$.  This is the basic mechanism that \texttt{addcongs} is built
+  on.  It should be rarely used directly.
+
+\item[$ss$ \ttindexbold{deleqcongs} $thms$] deletes congruence rules
+  in internal form from simpset $ss$.
+
+\end{ttdescription}
+
+\medskip
+
+Here are some more examples.  The congruence rule for bounded
+quantifiers also supplies contextual information, this time about the
+bound variable:
\begin{eqnarray*}
&&\List{\Var{A}=\Var{B};\;
\Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)} \Imp{} \\
@@ -238,41 +440,57 @@
This can make simplification much faster, but may require an extra case split
to prove the goal.

-Their conclusion must be a meta-equality, as in the examples above.  It is more
-natural to derive the rules with object-logic equality, for example
-$\List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}} - \Imp (\Var{P@1} \imp \Var{P@2}) \bimp (\Var{Q@1} \imp \Var{Q@2}), -$
-Each object-logic should define operators called \ttindex{addcongs} and
-\ttindex{delcongs} that expects object-equalities and translates them into
-meta-equalities.

-\subsection{*The subgoaler}
+\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.
+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.

-The subgoaler can be set explicitly with \ttindex{setsubgoaler}.  For
-example, the subgoaler
+\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 subgoal_tac ss = assume_tac ORELSE'
-                     resolve_tac (prems_of_ss ss) ORELSE'
-                     asm_simp_tac ss;
+fun subgoaler ss =
+    assume_tac ORELSE'
+    resolve_tac (prems_of_ss ss) ORELSE'
+    asm_simp_tac ss;
\end{ttbox}
-tries to solve the subgoal by assumption or with one of the premises, calling
-simplification only if that fails; here {\tt prems_of_ss} extracts the
-current premises from a simpset.
+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}
+setSolver  : simpset * (thm list -> int -> tactic) -> simpset \hfill{\bf infix 4}
+addSolver  : simpset * (thm list -> int -> tactic) -> simpset \hfill{\bf infix 4}
+setSSolver : simpset * (thm list -> int -> tactic) -> simpset \hfill{\bf infix 4}
+addSSolver : simpset * (thm list -> int -> tactic) -> simpset \hfill{\bf infix 4}
+\end{ttbox}
+
The solver is a pair of tactics that attempt to solve a subgoal after
-simplification.  Typically it just proves trivial subgoals such as {\tt
-  True} and $t=t$.  It could use sophisticated means such as {\tt
-  blast_tac}, though that could make simplification expensive.
+simplification.  Typically it just proves trivial subgoals such as
+{\tt True} and $t=t$.  It could use sophisticated means such as {\tt
+  blast_tac}, though that could make simplification expensive.

Rewriting does not instantiate unknowns.  For example, rewriting
cannot prove $a\in \Var{A}$ since this requires
@@ -281,43 +499,66 @@
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.  Therefore,
-the solver is split into a safe and an unsafe part.  Both parts can be
-set independently, using either \ttindex{setSSolver} with a safe
-tactic as argument, or \ttindex{setSolver} with an unsafe tactic.
+it is important whether it can be considered safe or not.  For this
+reason the solver is split into a safe and an unsafe part.

The standard simplification strategy solely uses the unsafe solver,
-which is appropriate in most cases.  But for special applications where
+which is appropriate in most cases.  For special applications where
the simplification process is not allowed to instantiate unknowns
-within the goal, the tactic \ttindexbold{safe_asm_full_simp_tac} is
-provided.  It uses the \emph{safe} solver for the current subgoal, but
-applies ordinary unsafe {\tt asm_full_simp_tac} for recursive internal
-simplifications (for conditional rules or congruences).
+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.
+
+\begin{ttdescription}
+
+\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$.

-\index{assumptions!in simplification}
-The tactic is presented with the full goal, including the asssumptions.
-Hence it can use those assumptions (say by calling {\tt assume_tac}) even
-inside {\tt simp_tac}, which otherwise does not use assumptions.  The
-solver is also supplied a list of theorems, namely assumptions that hold in
-the local context.
+\end{ttdescription}
+
+\medskip

-The subgoaler is also used to solve the premises of congruence rules, which
-are usually of the form $s = \Var{x}$, where $s$ needs to be simplified and
-$\Var{x}$ needs to be instantiated with the result.  Hence the subgoaler
-should call the simplifier at some point.  The simplifier will then call the
-solver, which must therefore 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 {\tt blast_tac}.
+\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 {\tt 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 the simplifier aborts with the message {\tt Failed congruence
+  If the simplifier aborts with the message \texttt{Failed congruence
proof!}, then the subgoaler or solver has failed to prove a
premise of a congruence rule.  This should never occur under normal
circumstances; it indicates that some congruence rule, or possibly
@@ -325,145 +566,138 @@
\end{warn}

-\subsection{*The looper}
-The looper is a tactic that is 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 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.  The looper is set with
+\subsection{*The looper}\label{sec:simp-looper}
+\begin{ttbox}
+setloop   : simpset * (int -> tactic) -> simpset \hfill{\bf infix 4}
+addloop   : simpset * (int -> tactic) -> simpset \hfill{\bf infix 4}
+addsplits : simpset * thm list -> simpset \hfill{\bf infix 4}
+\end{ttbox}
+
+The looper is a tactic that is 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 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 looper
+  of $ss$.
+
+\item[$ss$ \ttindexbold{addloop} $tacf$] adds $tacf$ as an additional
+  looper; it will be tried after the loopers which had already been
+  present in $ss$.
+
+\item[$ss$ \ttindexbold{addsplits} $thms$] adds
+  \texttt{(split_tac~$thms$)} as an additional looper.
+
+\end{ttdescription}
+

-\begin{figure}
-\index{*simpset ML type}
-\index{*empty_ss}
-\index{*rep_ss}
-\index{*prems_of_ss}
-\index{*setloop}
-\index{*setSSolver}
-\index{*setSolver}
-\index{*setsubgoaler}
-\index{*setmksimps}
-\index{*delsimps}
-\index{*deleqcongs}
-\index{*merge_ss}
-\index{*simpset}
-\index{*Delsimps}
-\index{*simp_tac}
-\index{*asm_simp_tac}
-\index{*full_simp_tac}
-\index{*asm_full_simp_tac}
-\index{*safe_asm_full_simp_tac}
-\index{*Simp_tac}
-\index{*Asm_simp_tac}
-\index{*Full_simp_tac}
-\index{*Asm_full_simp_tac}
+\section{The simplification tactics}\label{simp-tactics}
+\index{simplification!tactics}\index{tactics!simplification}
+\begin{ttbox}
+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
+SIMPSET                : (simpset -> tactic) -> tactic
+SIMPSET'               : (simpset -> 'a -> tactic) -> 'a -> tactic
+\end{ttbox}

-\begin{ttbox}
+These are the basic tactics that are underlying any actual
+simplification work.  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.

-signature SIMPLIFIER =
-sig
-  type simpset
-  val empty_ss: simpset
-  val rep_ss: simpset -> {\ttlbrace}simps: thm list, procs: string list,
-                          congs: thm list,
-                          subgoal_tac:        simpset -> int -> tactic,
-                          loop_tac:                      int -> tactic,
-                                 finish_tac: thm list -> int -> tactic,
-                          unsafe_finish_tac: thm list -> int -> tactic{\ttrbrace}
-  val setsubgoaler: simpset *  (simpset -> int -> tactic) -> simpset
-  val setloop:      simpset *             (int -> tactic) -> simpset
-  val addloop:      simpset *             (int -> tactic) -> simpset
-  val setSSolver:   simpset * (thm list -> int -> tactic) -> simpset
-  val addSSolver:   simpset * (thm list -> int -> tactic) -> simpset
-  val setSolver:    simpset * (thm list -> int -> tactic) -> simpset
-  val addSolver:    simpset * (thm list -> int -> tactic) -> simpset
-  val setmksimps:  simpset * (thm -> thm list) -> simpset
-  val addsimps:    simpset * thm list -> simpset
-  val delsimps:    simpset * thm list -> simpset
-  val addeqcongs:  simpset * thm list -> simpset
-  val deleqcongs:  simpset * thm list -> simpset
-  val merge_ss:    simpset * simpset -> simpset
-  val prems_of_ss: simpset -> thm list
-  val simpset:     simpset ref
-  val Addsimps: thm list -> unit
-  val Delsimps: thm list -> unit
-  val               simp_tac: simpset -> int -> tactic
-  val           asm_simp_tac: simpset -> int -> tactic
-  val          full_simp_tac: simpset -> int -> tactic
-  val      asm_full_simp_tac: simpset -> int -> tactic
-  val safe_asm_full_simp_tac: simpset -> int -> tactic
-  val               Simp_tac:            int -> tactic
-  val           Asm_simp_tac:            int -> tactic
-  val          Full_simp_tac:            int -> tactic
-  val      Asm_full_simp_tac:            int -> tactic
-end;
-\end{ttbox}
-\caption{The simplifier primitives} \label{SIMPLIFIER}
-\end{figure}
+\begin{ttdescription}
+
+\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.
+
+\item[\ttindexbold{safe_asm_full_simp_tac}] is like
+  \texttt{asm_full_simp_tac}, but uses the safe solver as explained in
+  \S\ref{sec:simp-solver}.  This tactic is mainly intended for
+  building special tools, e.g.\ for combining the simplifier with the
+  classical reasoner.  It is rarely used directly.
+
+\item[\ttindexbold{SIMPSET} $tacf$, \ttindexbold{SIMPSET'} $tacf'$]
+  are tacticals that make a tactic depend on the implicit current
+  simpset of the theory associated with the proof state they are
+  applied on.

+\end{ttdescription}

-\section{The simplification tactics}
-\label{simp-tactics}
-\index{simplification!tactics}
-\index{tactics!simplification}
+\medskip

-The actual simplification work is performed by the following basic tactics:
-\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac},
-\ttindexbold{full_simp_tac} and \ttindexbold{asm_full_simp_tac}.  They work
-exactly like their namesakes in \S\ref{sec:simp-for-dummies}, except that
-they are explicitly supplied with a simpset.  This is because the ones in
-\S\ref{sec:simp-for-dummies} are defined in terms of the ones above, e.g.
-\begin{ttbox}
-fun Simp_tac i = simp_tac (!simpset) i;
-\end{ttbox}
-where \ttindex{!simpset} is the current simpset\index{simpset!current}.
-
-The rewriting strategy of all four tactics is 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.
-
-simpset, while \ttindex{delsimps} deletes them.  They are used to
-\begin{ttbox}
-\end{ttbox}
-and can also be used directly, even in the presence of a current simpset.  For
-example
+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 compressed into
+can be expressed more appropriately as
\begin{ttbox}
-by (simp_tac (!simpset addsimps $$thms$$) $$i$$);
+by (simp_tac (simpset() addsimps $$thms$$) $$i$$);
\end{ttbox}

-The simpset associated with a particular theory can be retrieved via the name
-of the theory using the function
-\begin{ttbox}
-simpset_of: string -> simpset
-\end{ttbox}\index{*simpset_of}
+\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.
+
+\begin{warn}
+  There is a subtle difference between \texttt{(SIMPSET'~$tacf$)} and
+  \texttt{($tacf$~(simpset()))}.  For example \texttt{(SIMPSET'
+    simp_tac)} would depend on the theory of the proof state it is
+  applied to, while \texttt{(simp_tac (simpset()))} implicitly refers
+  to the current theory context.  Both are usually the same in proof
+  scripts, provided that goals are only stated within the current
+  theory.  Robust programs would not count on that, of course.
+\end{warn}
+

-To remind yourself of what is in a simpset, use the function \verb$rep_ss$ to
-return its simplification and congruence rules.
+\section{Forward simplification rules}
+\index{simplification!forward rules}
+\begin{ttbox}\index{*simplify}\index{*asm_simplify}\index{*full_simplify}\index{*asm_full_simplify}
+simplify          : simpset -> thm -> thm
+asm_simplify      : simpset -> thm -> thm
+full_simplify     : simpset -> thm -> thm
+asm_full_simplify : simpset -> thm -> thm
+\end{ttbox}
+
+These are forward rules, simplifying theorems in a similar way as the
+corresponding simplification tactics do.  The forward rules affect the whole

-\section{Examples using the simplifier}
+ subgoals of a proof state.  The
+looper~/ solver process as described in \S\ref{sec:simp-looper} and
+\S\ref{sec:simp-solver} does not apply here, though.
+
+\begin{warn}
+  Forward simplification should be used rarely in ordinary proof
+  scripts.  It as mainly intended to provide an internal interface to
+  the simplifier for ML coded special utilities.
+\end{warn}
+
+
+\section{Examples of using the simplifier}
\index{examples!of simplification} Assume we are working within {\tt
FOL} (cf.\ \texttt{FOL/ex/Nat}) and that
\begin{ttdescription}
@@ -477,8 +711,8 @@
is the induction rule $\List{\Var{P}(0);\; \Forall x. \Var{P}(x)\Imp \Var{P}(Suc(x))} \Imp \Var{P}(\Var{n})$.
\end{ttdescription}
-We augment the implicit simpset of {\FOL} with the basic rewrite rules
-for natural numbers:
+We augment the implicit simpset inherited from \texttt{Nat} with the
+basic rewrite rules for natural numbers:
\begin{ttbox}
\end{ttbox}
@@ -548,7 +782,7 @@
Switching tracing on illustrates how the simplifier solves the remaining
subgoal:
\begin{ttbox}
-trace_simp := true;
+set trace_simp;
by (Asm_simp_tac 1);
\ttbreak
@@ -610,14 +844,9 @@
{\out  1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
\end{ttbox}
The remaining subgoal requires rewriting by the premise, so we add it
-to the current simpset:\footnote{The previous simplifier required
-  congruence rules for function variables like~$f$ in order to
-  simplify their arguments.  It was more general than the current
-  simplifier, but harder to use and slower.  The present simplifier
-  can be given congruence rules to realize non-standard simplification
-  of a function's arguments, but this is seldom necessary.}
+to the current simpset:
\begin{ttbox}
-by (asm_simp_tac (!simpset addsimps [prem]) 1);
+by (asm_simp_tac (simpset() addsimps [prem]) 1);
{\out Level 3}
{\out f(i + j) = i + f(j)}
{\out No subgoals!}
@@ -627,8 +856,9 @@
\label{sec:reordering-asms}
\index{assumptions!reordering}

-As mentioned above, \ttindex{asm_full_simp_tac} may require the assumptions
-to be permuted to be more effective.  Given the subgoal
+As mentioned in \S\ref{sec:simp-for-dummies-tacs},
+\ttindex{asm_full_simp_tac} may require the assumptions to be permuted
+to be more effective.  Given the subgoal
\begin{ttbox}
{\out 1. [| P(f(a)); Q; f(a) = t; R |] ==> S}
\end{ttbox}
@@ -654,12 +884,18 @@
{\out 1. [| Q; f(a) = t; R; P(f(a)) |] ==> S}
\end{ttbox}

-Note that reordering assumptions usually leads to brittle proofs and should
-therefore be avoided.  Future versions of \verb$asm_full_simp_tac$ may remove
-the need for such manipulations.
+\begin{warn}
+  Reordering assumptions usually leads to brittle proofs and should be
+  avoided.  Future versions of \verb$asm_full_simp_tac$ may remove the
+  need for such manipulations.
+\end{warn}
+

\section{Permutative rewrite rules}
\index{rewrite rules!permutative|(}
+\begin{ttbox}
+settermless : simpset * (term * term -> bool) -> simpset \hfill{\bf infix 4}
+\end{ttbox}

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
@@ -667,24 +903,39 @@
(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. 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. +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{ttdescription} + +\item[$ss$\ttindexbold{settermless}$rel$] installs relation$rel$as + term order in simpset$ss$. + +\end{ttdescription} + +\medskip -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: +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! Future versions of Isabelle may remove - this restriction. + +\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 @@ -699,17 +950,18 @@ such as boolean rings. \subsection{Example: sums of natural numbers} -This example is 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 {\tt add_ac} is a list consisting of the -A, C and LC laws for~$+$on type \texttt{nat}. Let us prove the -theorem + +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 {\tt 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~{\tt sum} represents the summation operator under the interpretation${\tt sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$. We -extend {\tt Arith} using a theory file: +extend {\tt Arith} as follows: \begin{ttbox} NatSum = Arith + consts sum :: [nat=>nat, nat] => nat @@ -800,18 +1052,115 @@ \index{rewrite rules!permutative|)} +\section{*Coding simplification procedures} +\begin{ttbox} +mk_simproc: string -> cterm list -> + (Sign.sg -> thm list -> term -> thm option) -> simproc +\end{ttbox} + +\begin{ttdescription} +\item[\ttindexbold{mk_simproc}~$name$~$lhss$~$proc$] makes$proc$a + simplification procedure for left-hand side patterns$lhss$. The + name just serves as a comment. The function$proc$may be invoked + by the simplifier for redex positions matched by one of$lhss$as + described below. +\end{ttdescription} + +Simplification procedures are applied in a two-stage process as +follows: The simplifier tries to match the current redex position +against any one of the$lhs$patterns of any simplification procedure. +If this succeeds, it invokes the corresponding {\ML} function, passing +with the current signature, local assumptions and the (potential) +redex. The result may be either \texttt{None} (indicating failure) or +\texttt{Some~$thm$}. + +Any successful result is supposed to be a (possibly conditional) +rewrite rule$t \equiv u$that is applicable to the current redex. +The rule will be applied just as any ordinary rewrite rule. It is +expected to be already in \emph{internal form}, though, bypassing the +automatic preprocessing of object-level equivalences. + +\medskip + +As an example of how to write your own simplification procedures, +consider eta-expansion of pair abstraction (see also +\texttt{HOL/Modelcheck/MCSyn} where this is used to provide external +model checker syntax). + +The {\HOL} theory of tuples (see \texttt{HOL/Prod}) provides an +operator \texttt{split} together with some concrete syntax supporting +$\lambda\,(x,y).b$abstractions. Assume that we would like to offer a +tactic that rewrites any function$\lambda\,p.f\,p$(where$p$is of +some pair type) to$\lambda\,(x,y).f\,(x,y)$. The corresponding rule +is: +\begin{ttbox} +pair_eta_expand: (f::'a*'b=>'c) = (\%(x, y). f (x, y)) +\end{ttbox} +Unfortunately, term rewriting using this rule directly would not +terminate! We now use the simplification procedure mechanism in order +to stop the simplifier from applying this rule over and over again, +making it rewrite only actual abstractions. The simplification +procedure \texttt{pair_eta_expand_proc} is defined as follows: +\begin{ttbox} +local + val lhss = + [read_cterm (sign_of Prod.thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))]; + val rew = mk_meta_eq pair_eta_expand; \medskip + fun proc _ _ (Abs _) = Some rew + | proc _ _ _ = None; +in + val pair_eta_expand_proc = Simplifier.mk_simproc "pair_eta_expand" lhss proc; +end; +\end{ttbox} +This is an example of using \texttt{pair_eta_expand_proc}: +\begin{ttbox} +{\out 1. P (\%p::'a * 'a. fst p + snd p + z)} +by (simp_tac (simpset() addsimprocs [pair_eta_expand_proc]) 1); +{\out 1. P (\%(x::'a,y::'a). x + y + z)} +\end{ttbox} + +\medskip + +In the above example the simplification procedure just did fine +grained control over rule application, beyond higher-order pattern +matching. Usually, procedures would do some more work, in particular +prove particular theorems depending on the current redex. + +For example, simplification procedures \ttindexbold{nat_cancel} of +\texttt{HOL/Arith} cancel common summands and constant factors out of +several relations of sums over natural numbers. + +Consider the following goal, which after cancelling$a$on both sides +contains a factor of$2$. Simplifying with the simpset of +\texttt{Arith.thy} will do the cancellation automatically: +\begin{ttbox} +{\out 1. x + a + x < y + y + 2 + a + a + a + a + a} +by (Simp_tac 1); +{\out 1. x < Suc (a + (a + y))} +\end{ttbox} + +\medskip + +The {\ML} sources for these simplification procedures consist of a +generic part (files \texttt{cancel_sums.ML} and +\texttt{cancel_factor.ML} in \texttt{Provers/Arith}), and a +\texttt{HOL} specific part in \texttt{HOL/arith_data.ML}. + + \section{*Setting up the simplifier}\label{sec:setting-up-simp} \index{simplification!setting up} Setting up the simplifier for new logics is complicated. This section -describes how the simplifier is installed for intuitionistic first-order -logic; the code is largely taken from {\tt FOL/simpdata.ML}. +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 simplifier and the case splitting tactic, which reside on separate -files, are not part of Pure Isabelle. They must be loaded explicitly: +files, are not part of Pure Isabelle. They must be loaded explicitly +by the object-logic as follows: \begin{ttbox} -use "../Provers/simplifier.ML"; -use "../Provers/splitter.ML"; +use "$ISABELLE_HOME/src/Provers/simplifier.ML";
+use "$ISABELLE_HOME/src/Provers/splitter.ML"; \end{ttbox} Simplification works by reducing various object-equalities to @@ -824,11 +1173,12 @@ \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 {\tt CTT} uses another simplifier, -which resides in the file {\tt typedsimp.ML} and is not documented. Even -this does not work for later variants of Constructive Type Theory that use +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 {\tt 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}. @@ -842,13 +1192,13 @@ (writeln s; prove_goal IFOL.thy s (fn prems => [ (cut_facts_tac prems 1), - (Int.fast_tac 1) ])); + (IntPr.fast_tac 1) ])); \end{ttbox} The following rewrite rules about conjunction are a selection of those proved on {\tt FOL/simpdata.ML}. Later, these will be supplied to the standard simpset. \begin{ttbox} -val conj_rews = map int_prove_fun +val conj_simps = map int_prove_fun ["P & True <-> P", "True & P <-> P", "P & False <-> False", "False & P <-> False", "P & P <-> P", @@ -859,7 +1209,7 @@ 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_rews = map int_prove_fun +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)"]; @@ -868,7 +1218,9 @@ \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 {\tt setmksimps} below. Preprocessing occurs whenever rewrite rules are added, whether by user command or @@ -942,25 +1294,34 @@ \subsection{Making the initial simpset} -It is time to assemble these items. We open module {\tt Simplifier} to -gain access to its components. We define the infix operator -\ttindexbold{addcongs} to insert congruence rules; given a list of theorems, -it converts their conclusions into meta-equalities and passes them to -\ttindex{addeqcongs}. + +It is time to assemble these items. We open module {\tt Simplifier} +to gain direct access to its components. We define the infix operator +\ttindex{addcongs} to insert congruence rules; given a list of +theorems, it converts their conclusions into meta-equalities and +passes them to \ttindex{addeqcongs}. \begin{ttbox} open Simplifier; \ttbreak -infix addcongs; +infix 4 addcongs; fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection,iff_reflection]); \end{ttbox} -The list {\tt IFOL_rews} contains the default rewrite rules for first-order -logic. The first of these is the reflexive law expressed as the -equivalence$(a=a)\bimp{\tt True}$; the rewrite rule$a=a$is clearly useless. +Furthermore, we define the infix operator \ttindex{addsplits} +providing a convenient interface for adding split tactics. \begin{ttbox} -val IFOL_rews = - [refl RS P_iff_T] \at conj_rews \at disj_rews \at not_rews \at - imp_rews \at iff_rews \at quant_rews; +infix 4 addsplits; +fun ss addsplits splits = ss addloop (split_tac splits); +\end{ttbox} + +The list {\tt IFOL_simps} contains the default rewrite rules for +first-order logic. The first of these is the reflexive law expressed +as the equivalence$(a=a)\bimp{\tt 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 {\tt triv_rls} contains trivial theorems for the solver. Any subgoal that is simplified to one of these will be removed. @@ -969,28 +1330,35 @@ val triv_rls = [TrueI,refl,iff_refl,notFalseI]; \end{ttbox} % -The basic simpset for intuitionistic \FOL{} starts with \ttindex{empty_ss}. -It preprocess rewrites using {\tt gen_all}, {\tt atomize} and {\tt - mk_meta_eq}. It solves simplified subgoals using {\tt triv_rls} and -assumptions, and by detecting contradictions. -It uses \ttindex{asm_simp_tac} to tackle subgoals of -conditional rewrites. It takes {\tt IFOL_rews} as rewrite rules. -Other simpsets built from {\tt IFOL_ss} will inherit these items. -In particular, {\tt FOL_ss} extends {\tt IFOL_ss} with classical rewrite -rules such as$\neg\neg P\bimp P$. +The basic simpset for intuitionistic \FOL{} is +\ttindexbold{FOL_basic_ss}. It preprocess rewrites using {\tt + gen_all}, {\tt atomize} and {\tt mk_meta_eq}. It solves simplified +subgoals using {\tt triv_rls} and assumptions, and by detecting +contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals of +conditional rewrites. + +Other simpsets built from {\tt 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 {\tt IFOL_ss} with classical rewrite rules such as$\neg\neg
+P\bimp P\$.
\index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler}
\begin{ttbox}
-fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls \at prems),
+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),
+
+fun   safe_solver prems = FIRST'[match_tac (triv_rls {\at} prems),
eq_assume_tac, ematch_tac [FalseE]];
-val IFOL_ss = empty_ss setsubgoaler asm_simp_tac
-                       setSSolver   safe_solver
-                       setSolver  unsafe_solver
-                       setmksimps (map mk_meta_eq o atomize o gen_all)
+
+val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
+                            setSSolver   safe_solver
+                            setSolver  unsafe_solver
+                            setmksimps (map mk_meta_eq o atomize o gen_all);
+
+val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps {\at} int_ex_simps {\at} int_all_simps)
\end{ttbox}
This simpset takes {\tt imp_cong} as a congruence rule in order to use
contextual information to simplify the conclusions of implications:
@@ -1027,14 +1395,33 @@
\langle a,b\rangle \imp \Var{P}(\Var{f}(a,b)))
\]
Case splits should be allowed only when necessary; they are expensive
-and hard to control.  Here is a typical example of use, where {\tt
-  expand_if} is the first rule above:
+and hard to control.  Here is an example of use, where {\tt expand_if}
+is the first rule above:
\begin{ttbox}
-by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (simp_tac (simpset() addloop (split_tac [expand_if])) 1);
+\end{ttbox}
+Users would usually prefer the following shortcut using
+\begin{ttbox}
+by (simp_tac (simpset() addsplits [expand_if]) 1);
\end{ttbox}

+\subsection{Theory data for implicit simpsets}
+\begin{ttbox}\indexbold{*simpset_thy_data}
+simpset_thy_data: string * (object * (object -> object) *
+    (object * object -> object) * (Sign.sg -> object -> unit))
+\end{ttbox}
+
+Theory data for implicit simpsets has to be set up explicitly.  The
+simplifier already provides an appropriate data kind definition
+record.  This has to be installed into the base theory of any new
+object-logic as \ttindexbold{thy_data} within the \texttt{ML} section.
+
+This is done at the end of \texttt{IFOL.thy} as follows:
+\begin{ttbox}
+ML val thy_data = [Simplifier.simpset_thy_data];
+\end{ttbox}
+

\index{simplification|)}
-
-