\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{Accessing the current simpset}

\label{sec:access-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

SIMPSET        :(simpset ->       tactic) ->       tactic

SIMPSET'       :(simpset -> 'a -> tactic) -> 'a -> tactic

\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}.

\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}

\begin{warn}

  There is a small 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}

\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{*Simplification procedures}

\begin{ttbox}

addsimprocs : simpset * simproc list -> simpset

delsimprocs : simpset * simproc list -> simpset

\end{ttbox}

Simplification procedures are {\ML} objects of abstract type

\texttt{simproc}.  Basically they are just 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 the simplification

  procedures $procs$ to the current simpset.

\item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes the simplification

  procedures $procs$ from the current simpset.

\end{ttdescription}

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}

\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}).

\]

This governs the simplification of the arguments of~$f$.  For

example, some arguments can be simplified under additional assumptions:

\[ \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

{\S}~\ref{sec:simp-solver} below.

\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{} \\

 &&\qquad\qquad

    (\forall x\in \Var{A}.\Var{P}(x)) = (\forall x\in \Var{B}.\Var{Q}(x))

\end{eqnarray*}

The congruence rule for conditional expressions can supply contextual

information for simplifying the arms:

\[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~

         \neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp

   if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d})

\]

A congruence rule can also {\em prevent\/} simplification of some arguments.

Here is an alternative congruence rule for conditional expressions:

\[ \Var{p}=\Var{q} \Imp

   if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{a},\Var{b})

\]

Only the first argument is simplified; the others remain unchanged.

This can make simplification much faster, but may require an extra case split

to prove the goal.  

\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{*Coding simplification procedures}

\begin{ttbox}

  val Simplifier.simproc: Sign.sg -> string -> string list

    -> (Sign.sg -> simpset -> term -> thm option) -> simproc

  val Simplifier.simproc_i: Sign.sg -> string -> term list

    -> (Sign.sg -> simpset -> term -> thm option) -> simproc

\end{ttbox}

\begin{ttdescription}

\item[\ttindexbold{Simplifier.simproc}~$sign$~$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

  (which are be specified as strings to be read as terms).

\item[\ttindexbold{Simplifier.simproc_i}] is similar to

  \verb,Simplifier.simproc,, but takes well-typed terms as pattern argument.

\end{ttdescription}