104

1 
%% $Id$


2 
\chapter{Simplification} \label{simpchap}


3 
\index{simplification(}


4 


5 


6 
This chapter describes Isabelle's generic simplification package, which


7 
provides a suite of simplification tactics. This rewriting package is less


8 
general than its predecessor  it works only for the equality relation,


9 
not arbitrary preorders  but it is fast and flexible. It performs


10 
conditional and unconditional rewriting and uses contextual information


11 
(``local assumptions''). It provides a few general hooks, which can


12 
provide automatic case splits during rewriting, for example. The


13 
simplifier is set up for many of Isabelle's logics: {\tt FOL}, {\tt ZF},


14 
{\tt LCF} and {\tt HOL}.


15 


16 


17 
\section{Simplification sets}


18 
\index{simplification sets}


19 


20 
The simplification tactics are controlled by {\bf simpsets}. These consist


21 
of five components: rewrite rules, congruence rules, the subgoaler, the


22 
solver and the looper. Normally, the simplifier is set up with sensible


23 
defaults, so that most simplifier calls specify only rewrite rules.


24 
Sophisticated usage of the other components can be highly effective, but


25 
most users should never worry about them.


26 


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


28 


29 
Rewrite rules are theorems like $Suc(\Var{m}) + \Var{n} = \Var{m} +

122

30 
Suc(\Var{n})$, $\Var{P}\conj\Var{P} \bimp \Var{P}$, or $\Var{A} \union \Var{B}

104

31 
\equiv \{x.x\in A \disj x\in B\}$. {\bf Conditional} rewrites such as


32 
$\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} = 0$ are permitted; the conditions


33 
can be arbitrary terms. The infix operation \ttindex{addsimps} adds new


34 
rewrite rules, while \ttindex{delsimps} deletes rewrite rules from a


35 
simpset.


36 


37 
Theorems added via \ttindex{addsimps} need not be equalities to start with.


38 
Each simpset contains a (userdefinable) function for extracting equalities


39 
from arbitrary theorems. For example $\neg(x\in \{\})$ could be turned


40 
into $x\in \{\} \equiv False$. This function can be set with


41 
\ttindex{setmksimps} but only the definer of a logic should need to do


42 
this. Exceptionally, one may want to install a selective version of


43 
\ttindex{mksimps} in order to filter out looping rewrite rules arising from


44 
local assumptions (see below).


45 


46 
Internally, all rewrite rules are translated into metaequalities:


47 
theorems with conclusion $lhs \equiv rhs$. To this end every simpset contains


48 
a function of type \verb$thm > thm list$ to extract a list


49 
of metaequalities from a given theorem.


50 


51 
\begin{warn}\index{rewrite rules}


52 
The lefthand side of a rewrite rule must look like a firstorder term:


53 
after etacontraction, none of its unknowns should have arguments. Hence


54 
${\Var{i}+(\Var{j}+\Var{k})} = {(\Var{i}+\Var{j})+\Var{k}}$ and $\neg(\forall


55 
x.\Var{P}(x)) \bimp (\exists x.\neg\Var{P}(x))$ are acceptable, whereas


56 
$\Var{f}(\Var{x})\in {\tt range}(\Var{f}) = True$ is not. However, you can


57 
replace the offending subterms by new variables and conditions: $\Var{y} =


58 
\Var{f}(\Var{x}) \Imp \Var{y}\in {\tt range}(\Var{f}) = True$ is again


59 
acceptable.


60 
\end{warn}


61 


62 
\subsection {Congruence rules}\index{congruence rules}


63 
Congruence rules are metaequalities of the form


64 
\[ \List{\dots} \Imp


65 
f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}).


66 
\]


67 
They control the simplification of the arguments of certain constants. For


68 
example, some arguments can be simplified under additional assumptions:


69 
\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}}


70 
\Imp (\Var{P@1} \imp \Var{P@2}) \equiv (\Var{Q@1} \imp \Var{Q@2})


71 
\]


72 
This rule assumes $Q@1$ and any rewrite rules it implies, while


73 
simplifying~$P@2$. Such ``local'' assumptions are effective for rewriting


74 
formulae such as $x=0\imp y+x=y$. The next example makes similar use of


75 
such contextual information in bounded quantifiers:


76 
\[ \List{\Var{A}=\Var{B};\; \Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)}


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


78 
\]


79 
This congruence rule supplies contextual information for simplifying the


80 
arms of a conditional expressions:


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


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


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


84 
\]


85 


86 
A congruence rule can also suppress simplification of certain arguments.


87 
Here is an alternative congruence rule for conditional expressions:


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


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


90 
\]


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


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


93 
to prove the goal.


94 


95 
Congruence rules are added using \ttindex{addeqcongs}. Their conclusion


96 
must be a metaequality, as in the examples above. It is more


97 
natural to derive the rules with objectlogic equality, for example


98 
\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}}


99 
\Imp (\Var{P@1} \imp \Var{P@2}) \bimp (\Var{Q@1} \imp \Var{Q@2}),


100 
\]


101 
So each objectlogic should provide an alternative combinator


102 
\ttindex{addcongs} that expects objectequalities and translates them into


103 
metaequalities.


104 


105 
\subsection{The subgoaler} \index{subgoaler}


106 
The subgoaler is the tactic used to solve subgoals arising out of


107 
conditional rewrite rules or congruence rules. The default should be


108 
simplification itself. Occasionally this strategy needs to be changed. For


109 
example, if the premise of a conditional rule is an instance of its


110 
conclusion, as in $Suc(\Var{m}) < \Var{n} \Imp \Var{m} < \Var{n}$, the


111 
default strategy could loop.


112 


113 
The subgoaler can be set explicitly with \ttindex{setsubgoaler}. For


114 
example, the subgoaler


115 
\begin{ttbox}


116 
fun subgoal_tac ss = resolve_tac (prems_of_ss ss) ORELSE'


117 
asm_simp_tac ss;


118 
\end{ttbox}


119 
tries to solve the subgoal with one of the premises and calls


120 
simplification only if that fails; here {\tt prems_of_ss} extracts the


121 
current premises from a simpset.


122 


123 
\subsection{The solver} \index{solver}


124 
The solver attempts to solve a subgoal after simplification, say by


125 
recognizing it as a tautology. It can be set with \ttindex{setsolver}.


126 
Occasionally, simplification on its own is not enough to reduce the subgoal


127 
to a tautology; additional means, like \verb$fast_tac$, may be necessary.


128 


129 
\begin{warn}


130 
Rewriting does not instantiate unknowns. Trying to rewrite $a\in


131 
\Var{A}$ with the rule $\Var{x}\in \{\Var{x}\}$ leads nowhere. The


132 
solver, however, is an arbitrary tactic and may instantiate unknowns as


133 
it pleases. This is the only way the simplifier can handle a conditional


134 
rewrite rule whose condition contains extra variables.


135 
\end{warn}


136 


137 
\begin{warn}


138 
If you want to supply your own subgoaler or solver, read on. The subgoaler


139 
is also used to solve the premises of congruence rules, which are usually


140 
of the form $s = \Var{x}$, where $s$ needs to be simplified and $\Var{x}$


141 
needs to be instantiated with the result. Hence the subgoaler should call


142 
the simplifier at some point. The simplifier will then call the solver,


143 
which must therefore be prepared to solve goals of the form $t = \Var{x}$,


144 
usually by reflexivity. In particular, reflexivity should be tried before


145 
any of the fancy tactics like {\tt fast_tac}. It may even happen that, due


146 
to simplification, the subgoal is no longer an equality. For example $False


147 
\bimp \Var{Q}$ could be rewritten to $\neg\Var{Q}$, in which case the


148 
solver must also try resolving with the theorem $\neg False$.


149 


150 
If the simplifier aborts with the message {\tt Failed congruence proof!},


151 
it is due to the subgoaler or solver who failed to prove a premise of a


152 
congruence rule.


153 
\end{warn}


154 


155 
\subsection{The looper} \index{looper}


156 
The looper is a tactic that is applied after simplification, in case the


157 
solver failed to solve the simplified goal. If the looper succeeds, the


158 
simplification process is started all over again. Each of the subgoals


159 
generated by the looper is attacked in turn, in reverse order. A


160 
typical looper is case splitting: the expansion of a conditional. Another


161 
possibility is to apply an elimination rule on the assumptions. More


162 
adventurous loopers could start an induction. The looper is set with


163 
\ttindex{setloop}.


164 


165 


166 
\begin{figure}


167 
\indexbold{*SIMPLIFIER}


168 
\begin{ttbox}


169 
infix addsimps addeqcongs delsimps


170 
setsubgoaler setsolver setloop setmksimps;


171 


172 
signature SIMPLIFIER =


173 
sig


174 
type simpset


175 
val simp_tac: simpset > int > tactic


176 
val asm_simp_tac: simpset > int > tactic


177 
val asm_full_simp_tac: simpset > int > tactic


178 
val addeqcongs: simpset * thm list > simpset


179 
val addsimps: simpset * thm list > simpset


180 
val delsimps: simpset * thm list > simpset


181 
val empty_ss: simpset


182 
val merge_ss: simpset * simpset > simpset


183 
val setsubgoaler: simpset * (simpset > int > tactic) > simpset


184 
val setsolver: simpset * (thm list > int > tactic) > simpset


185 
val setloop: simpset * (int > tactic) > simpset


186 
val setmksimps: simpset * (thm > thm list) > simpset


187 
val prems_of_ss: simpset > thm list


188 
val rep_ss: simpset > \{simps: thm list, congs: thm list\}


189 
end;


190 
\end{ttbox}


191 
\caption{The signature \ttindex{SIMPLIFIER}} \label{SIMPLIFIER}


192 
\end{figure}


193 


194 


195 
\section{The simplification tactics} \label{simptactics}


196 
\index{simplification!tacticsbold}


197 
\index{tactics!simplificationbold}


198 


199 
The actual simplification work is performed by the following tactics. The


200 
rewriting strategy is strictly bottom up, except for congruence rules, which


201 
are applied while descending into a term. Conditions in conditional rewrite


202 
rules are solved recursively before the rewrite rule is applied.


203 


204 
There are three basic simplification tactics:


205 
\begin{description}


206 
\item[\ttindexbold{simp_tac} $ss$ $i$] simplifies subgoal~$i$ using the rules


207 
in~$ss$. It may solve the subgoal completely if it has become trivial,


208 
using the solver.


209 


210 
\item[\ttindexbold{asm_simp_tac}] is like \verb$simp_tac$, but also uses


211 
assumptions as additional rewrite rules.


212 


213 
\item[\ttindexbold{asm_full_simp_tac}] is like \verb$asm_simp_tac$, but also


214 
simplifies the assumptions one by one, using each assumption in the


215 
simplification of the following ones.


216 
\end{description}


217 
Using the simplifier effectively may take a bit of experimentation. The


218 
tactics can be traced with the ML command \verb$trace_simp := true$. To


219 
remind yourself of what is in a simpset, use the function \verb$rep_ss$ to


220 
return its simplification and congruence rules.


221 


222 
\section{Example: using the simplifier}


223 
\index{simplification!example}


224 
Assume we are working within {\tt FOL} and that


225 
\begin{description}


226 
\item[\tt Nat.thy] is a theory including the constants $0$, $Suc$ and $+$,


227 
\item[\tt add_0] is the rewrite rule $0+n = n$,


228 
\item[\tt add_Suc] is the rewrite rule $Suc(m)+n = Suc(m+n)$,


229 
\item[\tt induct] is the induction rule


230 
$\List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n)$.


231 
\item[\tt FOL_ss] is a basic simpset for {\tt FOL}.\footnote


232 
{These examples reside on the file {\tt FOL/ex/nat.ML}.}


233 
\end{description}


234 


235 
We create a simpset for natural numbers by extending~{\tt FOL_ss}:


236 
\begin{ttbox}


237 
val add_ss = FOL_ss addsimps [add_0, add_Suc];


238 
\end{ttbox}


239 
Proofs by induction typically involve simplification:


240 
\begin{ttbox}


241 
goal Nat.thy "m+0 = m";


242 
{\out Level 0}


243 
{\out m + 0 = m}


244 
{\out 1. m + 0 = m}


245 
\ttbreak


246 
by (res_inst_tac [("n","m")] induct 1);


247 
{\out Level 1}


248 
{\out m + 0 = m}


249 
{\out 1. 0 + 0 = 0}


250 
{\out 2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}


251 
\end{ttbox}


252 
Simplification solves the first subgoal:


253 
\begin{ttbox}


254 
by (simp_tac add_ss 1);


255 
{\out Level 2}


256 
{\out m + 0 = m}


257 
{\out 1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}


258 
\end{ttbox}


259 
The remaining subgoal requires \ttindex{asm_simp_tac} in order to use the


260 
induction hypothesis as a rewrite rule:


261 
\begin{ttbox}


262 
by (asm_simp_tac add_ss 1);


263 
{\out Level 3}


264 
{\out m + 0 = m}


265 
{\out No subgoals!}


266 
\end{ttbox}


267 


268 
\medskip


269 
The next proof is similar.


270 
\begin{ttbox}


271 
goal Nat.thy "m+Suc(n) = Suc(m+n)";


272 
{\out Level 0}


273 
{\out m + Suc(n) = Suc(m + n)}


274 
{\out 1. m + Suc(n) = Suc(m + n)}


275 
\ttbreak


276 
by (res_inst_tac [("n","m")] induct 1);


277 
{\out Level 1}


278 
{\out m + Suc(n) = Suc(m + n)}


279 
{\out 1. 0 + Suc(n) = Suc(0 + n)}


280 
{\out 2. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)}


281 
\ttbreak


282 
by (simp_tac add_ss 1);


283 
{\out Level 2}


284 
{\out m + Suc(n) = Suc(m + n)}


285 
{\out 1. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)}


286 
\end{ttbox}


287 
Switching tracing on illustrates how the simplifier solves the remaining


288 
subgoal:


289 
\begin{ttbox}


290 
trace_simp := true;


291 
by (asm_simp_tac add_ss 1);


292 
{\out Rewriting:}


293 
{\out Suc(x) + Suc(n) == Suc(x + Suc(n))}


294 
{\out Rewriting:}


295 
{\out x + Suc(n) == Suc(x + n)}


296 
{\out Rewriting:}


297 
{\out Suc(x) + n == Suc(x + n)}


298 
{\out Rewriting:}


299 
{\out Suc(Suc(x + n)) = Suc(Suc(x + n)) == True}


300 
{\out Level 3}


301 
{\out m + Suc(n) = Suc(m + n)}


302 
{\out No subgoals!}


303 
\end{ttbox}


304 
As usual, many variations are possible. At Level~1 we could have solved


305 
both subgoals at once using the tactical \ttindex{ALLGOALS}:


306 
\begin{ttbox}


307 
by (ALLGOALS (asm_simp_tac add_ss));


308 
{\out Level 2}


309 
{\out m + Suc(n) = Suc(m + n)}


310 
{\out No subgoals!}


311 
\end{ttbox}


312 


313 
\medskip


314 
Here is a conjecture to be proved for an arbitrary function~$f$ satisfying


315 
the law $f(Suc(n)) = Suc(f(n))$:\footnote{The previous


316 
simplifier required congruence rules for such function variables in


317 
order to simplify their arguments. The present simplifier can be given


318 
congruence rules to realize nonstandard simplification of a function's


319 
arguments, but this is seldom necessary.}


320 
\begin{ttbox}


321 
val [prem] = goal Nat.thy


322 
"(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";


323 
{\out Level 0}


324 
{\out f(i + j) = i + f(j)}


325 
{\out 1. f(i + j) = i + f(j)}


326 
{\out val prem = "f(Suc(?n)) = Suc(f(?n)) [!!n. f(Suc(n)) = Suc(f(n))]" : thm}


327 
\ttbreak


328 
by (res_inst_tac [("n","i")] induct 1);


329 
{\out Level 1}


330 
{\out f(i + j) = i + f(j)}


331 
{\out 1. f(0 + j) = 0 + f(j)}


332 
{\out 2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}


333 
\end{ttbox}


334 
We simplify each subgoal in turn. The first one is trivial:


335 
\begin{ttbox}


336 
by (simp_tac add_ss 1);


337 
{\out Level 2}


338 
{\out f(i + j) = i + f(j)}


339 
{\out 1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}


340 
\end{ttbox}


341 
The remaining subgoal requires rewriting by the premise, so we add it to


342 
{\tt add_ss}:


343 
\begin{ttbox}


344 
by (asm_simp_tac (add_ss addsimps [prem]) 1);


345 
{\out Level 3}


346 
{\out f(i + j) = i + f(j)}


347 
{\out No subgoals!}


348 
\end{ttbox}


349 


350 
No documentation is available on setting up the simplifier for new logics.


351 
Please consult {\tt FOL/simpdata.ML} to see how this is done, and {\tt


352 
FOL/simpdata.ML} for a fairly sophisticated translation of formulae into


353 
rewrite rules.


354 


355 
%%\section{Setting up the simplifier} \label{SimpFuninput}


356 
%%Should be written!


357 


358 


359 
\index{simplification)}


360 
