doc-src/Ref/simplifier.tex

ZF/ord/Ord_Un,Ord_Int,Un_upper1_le,Un_upper2_le: new

%% $Id$
\chapter{Simplification} \label{simp-chap}
\index{simplification|(}


This chapter describes Isabelle's generic simplification package, which
provides a suite of simplification tactics.  This rewriting package is less
general than its predecessor --- it works only for the equality relation,
not arbitrary preorders --- but it is fast and flexible.  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: {\tt FOL}, {\tt ZF},
{\tt LCF} and {\tt HOL}.


\section{Simplification sets}
\index{simplification sets} 

The simplification tactics are controlled by {\bf simpsets}.  These consist
of five components: rewrite rules, congruence rules, the subgoaler, the
solver and the looper.  Normally, the simplifier is set up with sensible
defaults, so that most simplifier calls specify only rewrite rules.
Sophisticated usage of the other components can be highly effective, but
most users should never worry about them.

\subsection{Rewrite rules}\index{rewrite rules}

Rewrite rules are theorems like $Suc(\Var{m}) + \Var{n} = \Var{m} +
Suc(\Var{n})$, $\Var{P}\conj\Var{P} \bimp \Var{P}$, or $\Var{A} \union \Var{B}
\equiv \{x.x\in A \disj x\in B\}$.  {\bf Conditional} rewrites such as
$\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} = 0$ are permitted; the conditions
can be arbitrary terms.  The infix operation \ttindex{addsimps} adds new
rewrite rules, while \ttindex{delsimps} deletes rewrite rules from a
simpset.

Theorems added via \ttindex{addsimps} need not be equalities to start with.
Each simpset contains a (user-definable) function for extracting equalities
from arbitrary theorems.  For example $\neg(x\in \{\})$ could be turned
into $x\in \{\} \equiv False$.  This function can be set with
\ttindex{setmksimps} but only the definer of a logic should need to do
this.  Exceptionally, one may want to install a selective version of
\ttindex{mksimps} in order to filter out looping rewrite rules arising from
local assumptions (see below).

Internally, all rewrite rules are translated into meta-equalities:
theorems with conclusion $lhs \equiv rhs$.  To this end every simpset contains
a function of type \verb$thm -> thm list$ to extract a list
of meta-equalities from a given theorem.

\begin{warn}\index{rewrite rules}
  The left-hand side of a rewrite rule must look like a first-order term:
  after eta-contraction, none of its unknowns should have arguments.  Hence
  ${\Var{i}+(\Var{j}+\Var{k})} = {(\Var{i}+\Var{j})+\Var{k}}$ and $\neg(\forall
  x.\Var{P}(x)) \bimp (\exists x.\neg\Var{P}(x))$ are acceptable, whereas
  $\Var{f}(\Var{x})\in {\tt range}(\Var{f}) = True$ is not.  However, you can
  replace the offending subterms by new variables and conditions: $\Var{y} =
  \Var{f}(\Var{x}) \Imp \Var{y}\in {\tt range}(\Var{f}) = True$ is again
  acceptable.
\end{warn}

\subsection {Congruence rules}\index{congruence rules}
Congruence rules are meta-equalities of the form
\[ \List{\dots} \Imp
   f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}).
\]
They control the simplification of the arguments of certain constants.  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})
\]
This rule assumes $Q@1$ and any rewrite rules it implies, while
simplifying~$P@2$.  Such ``local'' assumptions are effective for rewriting
formulae such as $x=0\imp y+x=y$.  The next example makes similar use of
such contextual information in bounded quantifiers:
\[ \List{\Var{A}=\Var{B};\; \Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)}
   \Imp (\forall x\in \Var{A}.\Var{P}(x)) = (\forall x\in \Var{B}.\Var{Q}(x))
\]
This congruence rule supplies contextual information for simplifying the
arms of a conditional expressions:
\[ \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 suppress simplification of certain 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.  

Congruence rules are added using \ttindex{addeqcongs}.  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}),
\]
So each object-logic should provide an alternative combinator
\ttindex{addcongs} that expects object-equalities and translates them into
meta-equalities.

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

The subgoaler can be set explicitly with \ttindex{setsubgoaler}.  For
example, the subgoaler
\begin{ttbox}
fun subgoal_tac ss = resolve_tac (prems_of_ss ss) ORELSE' 
                     asm_simp_tac ss;
\end{ttbox}
tries to solve the subgoal with one of the premises and calls
simplification only if that fails; here {\tt prems_of_ss} extracts the
current premises from a simpset.

\subsection{The solver} \index{solver}
The solver attempts to solve a subgoal after simplification, say by
recognizing it as a tautology. It can be set with \ttindex{setsolver}.
Occasionally, simplification on its own is not enough to reduce the subgoal
to a tautology; additional means, like \verb$fast_tac$, may be necessary.

\begin{warn}
  Rewriting does not instantiate unknowns.  Trying to rewrite $a\in
  \Var{A}$ with the rule $\Var{x}\in \{\Var{x}\}$ leads nowhere.  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.
\end{warn}

\begin{warn}
  If you want to supply your own subgoaler or solver, read on.  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 fast_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}$, in which case the
  solver must also try resolving with the theorem $\neg False$.

  If the simplifier aborts with the message {\tt Failed congruence proof!},
  it is due to the subgoaler or solver who failed to prove a premise of a
  congruence rule.
\end{warn}

\subsection{The looper} \index{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 
\ttindex{setloop}.


\begin{figure}
\indexbold{*SIMPLIFIER}
\begin{ttbox}
infix addsimps addeqcongs delsimps
      setsubgoaler setsolver setloop setmksimps;

signature SIMPLIFIER =
sig
  type simpset
  val simp_tac:          simpset -> int -> tactic
  val asm_simp_tac:      simpset -> int -> tactic
  val asm_full_simp_tac: simpset -> int -> tactic\smallskip
  val addeqcongs:   simpset * thm list -> simpset
  val addsimps:     simpset * thm list -> simpset
  val delsimps:     simpset * thm list -> simpset
  val empty_ss:     simpset
  val merge_ss:     simpset * simpset -> simpset
  val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
  val setsolver:    simpset * (thm list -> int -> tactic) -> simpset
  val setloop:      simpset * (int -> tactic) -> simpset
  val setmksimps:   simpset * (thm -> thm list) -> simpset
  val prems_of_ss:  simpset -> thm list
  val rep_ss:       simpset -> \{simps: thm list, congs: thm list\}
end;
\end{ttbox}
\caption{The signature \ttindex{SIMPLIFIER}} \label{SIMPLIFIER}
\end{figure}


\section{The simplification tactics} \label{simp-tactics}
\index{simplification!tactics|bold}
\index{tactics!simplification|bold}

The actual simplification work is performed by the following tactics.  The
rewriting strategy 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.

There are three basic simplification tactics:
\begin{description}
\item[\ttindexbold{simp_tac} $ss$ $i$] simplifies subgoal~$i$ using the rules
  in~$ss$.  It may solve the subgoal completely if it has become trivial,
  using the solver.
  
\item[\ttindexbold{asm_simp_tac}] is like \verb$simp_tac$, but also uses
  assumptions as additional rewrite rules.

\item[\ttindexbold{asm_full_simp_tac}] is like \verb$asm_simp_tac$, but also
  simplifies the assumptions one by one, using each assumption in the
  simplification of the following ones.
\end{description}
Using the simplifier effectively may take a bit of experimentation.  The
tactics can be traced with the ML command \verb$trace_simp := true$.  To
remind yourself of what is in a simpset, use the function \verb$rep_ss$ to
return its simplification and congruence rules.

\section{Example: using the simplifier}
\index{simplification!example}
Assume we are working within {\tt FOL} and that
\begin{description}
\item[\tt Nat.thy] is a theory including the constants $0$, $Suc$ and $+$,
\item[\tt add_0] is the rewrite rule $0+n = n$,
\item[\tt add_Suc] is the rewrite rule $Suc(m)+n = Suc(m+n)$,
\item[\tt induct] is the induction rule
$\List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n)$.
\item[\tt FOL_ss] is a basic simpset for {\tt FOL}.\footnote
{These examples reside on the file {\tt FOL/ex/nat.ML}.} 
\end{description}

We create a simpset for natural numbers by extending~{\tt FOL_ss}:
\begin{ttbox}
val add_ss = FOL_ss addsimps [add_0, add_Suc];
\end{ttbox}
Proofs by induction typically involve simplification:
\begin{ttbox}
goal Nat.thy "m+0 = m";
{\out Level 0}
{\out m + 0 = m}
{\out  1. m + 0 = m}
\ttbreak
by (res_inst_tac [("n","m")] induct 1);
{\out Level 1}
{\out m + 0 = m}
{\out  1. 0 + 0 = 0}
{\out  2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
\end{ttbox}
Simplification solves the first subgoal:
\begin{ttbox}
by (simp_tac add_ss 1);
{\out Level 2}
{\out m + 0 = m}
{\out  1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
\end{ttbox}
The remaining subgoal requires \ttindex{asm_simp_tac} in order to use the
induction hypothesis as a rewrite rule:
\begin{ttbox}
by (asm_simp_tac add_ss 1);
{\out Level 3}
{\out m + 0 = m}
{\out No subgoals!}
\end{ttbox}

\medskip
The next proof is similar.
\begin{ttbox}
goal Nat.thy "m+Suc(n) = Suc(m+n)";
{\out Level 0}
{\out m + Suc(n) = Suc(m + n)}
{\out  1. m + Suc(n) = Suc(m + n)}
\ttbreak
by (res_inst_tac [("n","m")] induct 1);
{\out Level 1}
{\out m + Suc(n) = Suc(m + n)}
{\out  1. 0 + Suc(n) = Suc(0 + n)}
{\out  2. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)}
\ttbreak
by (simp_tac add_ss 1);
{\out Level 2}
{\out m + Suc(n) = Suc(m + n)}
{\out  1. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)}
\end{ttbox}
Switching tracing on illustrates how the simplifier solves the remaining
subgoal: 
\begin{ttbox}
trace_simp := true;
by (asm_simp_tac add_ss 1);
{\out Rewriting:}
{\out Suc(x) + Suc(n) == Suc(x + Suc(n))}
{\out Rewriting:}
{\out x + Suc(n) == Suc(x + n)}
{\out Rewriting:}
{\out Suc(x) + n == Suc(x + n)}
{\out Rewriting:}
{\out Suc(Suc(x + n)) = Suc(Suc(x + n)) == True}
{\out Level 3}
{\out m + Suc(n) = Suc(m + n)}
{\out No subgoals!}
\end{ttbox}
As usual, many variations are possible.  At Level~1 we could have solved
both subgoals at once using the tactical \ttindex{ALLGOALS}:
\begin{ttbox}
by (ALLGOALS (asm_simp_tac add_ss));
{\out Level 2}
{\out m + Suc(n) = Suc(m + n)}
{\out No subgoals!}
\end{ttbox}

\medskip
Here is a conjecture to be proved for an arbitrary function~$f$ satisfying
the law $f(Suc(n)) = Suc(f(n))$:\footnote{The previous
  simplifier required congruence rules for such function variables in
  order to simplify their arguments.  The present simplifier can be given
  congruence rules to realize non-standard simplification of a function's
  arguments, but this is seldom necessary.}
\begin{ttbox}
val [prem] = goal Nat.thy
    "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
{\out Level 0}
{\out f(i + j) = i + f(j)}
{\out  1. f(i + j) = i + f(j)}
{\out val prem = "f(Suc(?n)) = Suc(f(?n))  [!!n. f(Suc(n)) = Suc(f(n))]" : thm}
\ttbreak
by (res_inst_tac [("n","i")] induct 1);
{\out Level 1}
{\out f(i + j) = i + f(j)}
{\out  1. f(0 + j) = 0 + f(j)}
{\out  2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
\end{ttbox}
We simplify each subgoal in turn.  The first one is trivial:
\begin{ttbox}
by (simp_tac add_ss 1);
{\out Level 2}
{\out f(i + j) = i + f(j)}
{\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
{\tt add_ss}: 
\begin{ttbox}
by (asm_simp_tac (add_ss addsimps [prem]) 1);
{\out Level 3}
{\out f(i + j) = i + f(j)}
{\out No subgoals!}
\end{ttbox}

No documentation is available on setting up the simplifier for new logics.
Please consult {\tt FOL/simpdata.ML} to see how this is done, and {\tt
  FOL/simpdata.ML} for a fairly sophisticated translation of formulae into
rewrite rules.

%%\section{Setting up the simplifier} \label{SimpFun-input}
%%Should be written!


\index{simplification|)}