author  lcp 
Wed, 03 May 1995 16:30:39 +0200  
changeset 1101  b9594fe65d89 
parent 714  015ec0a9563a 
child 1213  a8f6d0fa2a59 
permissions  rwrr 
104  1 
%% $Id$ 
2 
\chapter{Simplification} \label{simpchap} 

3 
\index{simplification(} 

4 

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

323  6 
provides a suite of simplification tactics. It performs conditional and 
7 
unconditional rewriting and uses contextual information (`local 

8 
assumptions'). It provides a few general hooks, which can provide 

9 
automatic case splits during rewriting, for example. The simplifier is set 

10 
up for many of Isabelle's logics: {\tt FOL}, {\tt ZF}, {\tt LCF} and {\tt 

11 
HOL}. 

104  12 

13 

286  14 
\section{Simplification sets}\index{simplification sets} 
104  15 
The simplification tactics are controlled by {\bf simpsets}. These consist 
16 
of five components: rewrite rules, congruence rules, the subgoaler, the 

323  17 
solver and the looper. The simplifier should be set up with sensible 
18 
defaults so that most simplifier calls specify only rewrite rules. 

19 
Experienced users can exploit the other components to streamline proofs. 

20 

104  21 

332  22 
\subsection{Rewrite rules} 
23 
\index{rewrite rules(} 

323  24 
Rewrite rules are theorems expressing some form of equality: 
25 
\begin{eqnarray*} 

26 
Suc(\Var{m}) + \Var{n} &=& \Var{m} + Suc(\Var{n}) \\ 

27 
\Var{P}\conj\Var{P} &\bimp& \Var{P} \\ 

714  28 
\Var{A} \un \Var{B} &\equiv& \{x.x\in \Var{A} \disj x\in \Var{B}\} 
323  29 
\end{eqnarray*} 
30 
{\bf Conditional} rewrites such as $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} = 

31 
0$ are permitted; the conditions can be arbitrary terms. The infix 

32 
operation \ttindex{addsimps} adds new rewrite rules, while 

33 
\ttindex{delsimps} deletes rewrite rules from a simpset. 

104  34 

323  35 
Internally, all rewrite rules are translated into metaequalities, theorems 
36 
with conclusion $lhs \equiv rhs$. Each simpset contains a function for 

37 
extracting equalities from arbitrary theorems. For example, 

38 
$\neg(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\} \equiv 

39 
False$. This function can be installed using \ttindex{setmksimps} but only 

40 
the definer of a logic should need to do this; see \S\ref{sec:setmksimps}. 

41 
The function processes theorems added by \ttindex{addsimps} as well as 

42 
local assumptions. 

104  43 

44 

332  45 
\begin{warn} 
1101  46 
The simplifier will accept all standard rewrite rules: those 
47 
where all unknowns are of base type. Hence ${\Var{i}+(\Var{j}+\Var{k})} = 

714  48 
{(\Var{i}+\Var{j})+\Var{k}}$ is ok. 
49 

50 
It will also deal gracefully with all rules whose lefthand sides are 

51 
socalled {\em higherorder patterns}~\cite{NipkowLICS93}. These are terms 

52 
in $\beta$normal form (this will always be the case unless you have done 

53 
something strange) where each occurrence of an unknown is of the form 

54 
$\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are distinct bound variables. 

55 
Hence $(\forall x.\Var{P}(x) \land \Var{Q}(x)) \bimp (\forall x.\Var{P}(x)) 

56 
\land (\forall x.\Var{Q}(x))$ is also ok, in both directions. 

57 

58 
In some rare cases the rewriter will even deal with quite general rules: for 

59 
example ${\Var{f}(\Var{x})\in range(\Var{f})} = True$ rewrites $g(a) \in 

60 
range(g)$ to $True$, but will fail to match $g(h(b)) \in range(\lambda 

61 
x.g(h(x)))$. However, you can replace the offending subterms (in our case 

62 
$\Var{f}(\Var{x})$, which is not a pattern) by adding new variables and 

63 
conditions: $\Var{y} = \Var{f}(\Var{x}) \Imp \Var{y}\in range(\Var{f}) 

64 
= True$ is acceptable as a conditional rewrite rule since conditions can 

65 
be arbitrary terms. 

66 

67 
There is no restriction on the form of the righthand sides. 

104  68 
\end{warn} 
69 

332  70 
\index{rewrite rules)} 
71 

72 
\subsection{*Congruence rules}\index{congruence rules} 

104  73 
Congruence rules are metaequalities of the form 
74 
\[ \List{\dots} \Imp 

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

76 
\] 

323  77 
This governs the simplification of the arguments of~$f$. For 
104  78 
example, some arguments can be simplified under additional assumptions: 
79 
\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}} 

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

81 
\] 

323  82 
Given this rule, the simplifier assumes $Q@1$ and extracts rewrite rules 
83 
from it when simplifying~$P@2$. Such local assumptions are effective for 

698
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset

84 
rewriting formulae such as $x=0\imp y+x=y$. The local assumptions are also 
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset

85 
provided as theorems to the solver; see page~\pageref{sec:simpsolver} below. 
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset

86 

23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset

87 
Here are some more examples. The congruence rule for bounded quantifiers 
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset

88 
also supplies contextual information, this time about the bound variable: 
286  89 
\begin{eqnarray*} 
90 
&&\List{\Var{A}=\Var{B};\; 

91 
\Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)} \Imp{} \\ 

92 
&&\qquad\qquad 

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

94 
\end{eqnarray*} 

323  95 
The congruence rule for conditional expressions can supply contextual 
96 
information for simplifying the arms: 

104  97 
\[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~ 
98 
\neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp 

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

100 
\] 

698
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset

101 
A congruence rule can also {\em prevent\/} simplification of some arguments. 
104  102 
Here is an alternative congruence rule for conditional expressions: 
103 
\[ \Var{p}=\Var{q} \Imp 

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

105 
\] 

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

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

108 
to prove the goal. 

109 

286  110 
Congruence rules are added using \ttindexbold{addeqcongs}. Their conclusion 
104  111 
must be a metaequality, as in the examples above. It is more 
112 
natural to derive the rules with objectlogic equality, for example 

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

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

115 
\] 

286  116 
Each objectlogic should define an operator called \ttindex{addcongs} that 
117 
expects objectequalities and translates them into metaequalities. 

104  118 

323  119 
\subsection{*The subgoaler} 
104  120 
The subgoaler is the tactic used to solve subgoals arising out of 
121 
conditional rewrite rules or congruence rules. The default should be 

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

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

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

125 
default strategy could loop. 

126 

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

128 
example, the subgoaler 

129 
\begin{ttbox} 

332  130 
fun subgoal_tac ss = assume_tac ORELSE' 
131 
resolve_tac (prems_of_ss ss) ORELSE' 

104  132 
asm_simp_tac ss; 
133 
\end{ttbox} 

332  134 
tries to solve the subgoal by assumption or with one of the premises, calling 
104  135 
simplification only if that fails; here {\tt prems_of_ss} extracts the 
136 
current premises from a simpset. 

137 

698
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset

138 
\subsection{*The solver}\label{sec:simpsolver} 
286  139 
The solver is a tactic that attempts to solve a subgoal after 
140 
simplification. Typically it just proves trivial subgoals such as {\tt 

323  141 
True} and $t=t$. It could use sophisticated means such as {\tt 
142 
fast_tac}, though that could make simplification expensive. The solver 

143 
is set using \ttindex{setsolver}. 

286  144 

323  145 
Rewriting does not instantiate unknowns. For example, rewriting cannot 
146 
prove $a\in \Var{A}$ since this requires instantiating~$\Var{A}$. The 

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

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

149 
rewrite rule whose condition contains extra variables. 

150 

151 
\index{assumptions!in simplification} 

286  152 
The tactic is presented with the full goal, including the asssumptions. 
153 
Hence it can use those assumptions (say by calling {\tt assume_tac}) even 

154 
inside {\tt simp_tac}, which otherwise does not use assumptions. The 

155 
solver is also supplied a list of theorems, namely assumptions that hold in 

156 
the local context. 

104  157 

323  158 
The subgoaler is also used to solve the premises of congruence rules, which 
159 
are usually of the form $s = \Var{x}$, where $s$ needs to be simplified and 

160 
$\Var{x}$ needs to be instantiated with the result. Hence the subgoaler 

161 
should call the simplifier at some point. The simplifier will then call the 

162 
solver, which must therefore be prepared to solve goals of the form $t = 

163 
\Var{x}$, usually by reflexivity. In particular, reflexivity should be 

164 
tried before any of the fancy tactics like {\tt fast_tac}. 

165 

166 
It may even happen that, due to simplification, the subgoal is no longer an 

167 
equality. For example $False \bimp \Var{Q}$ could be rewritten to 

168 
$\neg\Var{Q}$. To cover this case, the solver could try resolving with the 

169 
theorem $\neg False$. 

104  170 

171 
\begin{warn} 

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

323  173 
then the subgoaler or solver has failed to prove a premise of a 
698
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset

174 
congruence rule. This should never occur; it indicates that some 
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset

175 
congruence rule, or possibly the subgoaler or solver, is faulty. 
104  176 
\end{warn} 
177 

323  178 

179 
\subsection{*The looper} 

104  180 
The looper is a tactic that is applied after simplification, in case the 
181 
solver failed to solve the simplified goal. If the looper succeeds, the 

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

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

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

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

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

187 
\ttindex{setloop}. 

188 

189 

190 
\begin{figure} 

323  191 
\index{*simpset ML type} 
192 
\index{*simp_tac} 

193 
\index{*asm_simp_tac} 

194 
\index{*asm_full_simp_tac} 

195 
\index{*addeqcongs} 

196 
\index{*addsimps} 

197 
\index{*delsimps} 

198 
\index{*empty_ss} 

199 
\index{*merge_ss} 

200 
\index{*setsubgoaler} 

201 
\index{*setsolver} 

202 
\index{*setloop} 

203 
\index{*setmksimps} 

204 
\index{*prems_of_ss} 

205 
\index{*rep_ss} 

104  206 
\begin{ttbox} 
207 
infix addsimps addeqcongs delsimps 

208 
setsubgoaler setsolver setloop setmksimps; 

209 

210 
signature SIMPLIFIER = 

211 
sig 

212 
type simpset 

213 
val simp_tac: simpset > int > tactic 

214 
val asm_simp_tac: simpset > int > tactic 

133  215 
val asm_full_simp_tac: simpset > int > tactic\smallskip 
216 
val addeqcongs: simpset * thm list > simpset 

217 
val addsimps: simpset * thm list > simpset 

218 
val delsimps: simpset * thm list > simpset 

104  219 
val empty_ss: simpset 
220 
val merge_ss: simpset * simpset > simpset 

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

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

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

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

225 
val prems_of_ss: simpset > thm list 

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

227 
end; 

228 
\end{ttbox} 

323  229 
\caption{The simplifier primitives} \label{SIMPLIFIER} 
104  230 
\end{figure} 
231 

232 

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

323  234 
\index{simplification!tactics} 
235 
\index{tactics!simplification} 

104  236 

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

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

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

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

241 

242 
There are three basic simplification tactics: 

323  243 
\begin{ttdescription} 
104  244 
\item[\ttindexbold{simp_tac} $ss$ $i$] simplifies subgoal~$i$ using the rules 
245 
in~$ss$. It may solve the subgoal completely if it has become trivial, 

246 
using the solver. 

247 

323  248 
\item[\ttindexbold{asm_simp_tac}]\index{assumptions!in simplification} 
249 
is like \verb$simp_tac$, but extracts additional rewrite rules from the 

250 
assumptions. 

104  251 

332  252 
\item[\ttindexbold{asm_full_simp_tac}] 
253 
is like \verb$asm_simp_tac$, but also simplifies the assumptions one by 

254 
one. Working from left to right, it uses each assumption in the 

255 
simplification of those following. 

323  256 
\end{ttdescription} 
104  257 
Using the simplifier effectively may take a bit of experimentation. The 
258 
tactics can be traced with the ML command \verb$trace_simp := true$. To 

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

260 
return its simplification and congruence rules. 

261 

286  262 
\section{Examples using the simplifier} 
323  263 
\index{examples!of simplification} 
104  264 
Assume we are working within {\tt FOL} and that 
323  265 
\begin{ttdescription} 
266 
\item[Nat.thy] 

267 
is a theory including the constants $0$, $Suc$ and $+$, 

268 
\item[add_0] 

269 
is the rewrite rule $0+\Var{n} = \Var{n}$, 

270 
\item[add_Suc] 

271 
is the rewrite rule $Suc(\Var{m})+\Var{n} = Suc(\Var{m}+\Var{n})$, 

272 
\item[induct] 

273 
is the induction rule $\List{\Var{P}(0);\; \Forall x. \Var{P}(x)\Imp 

274 
\Var{P}(Suc(x))} \Imp \Var{P}(\Var{n})$. 

275 
\item[FOL_ss] 

276 
is a basic simpset for {\tt FOL}.% 

332  277 
\footnote{These examples reside on the file {\tt FOL/ex/Nat.ML}.} 
323  278 
\end{ttdescription} 
104  279 

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

281 
\begin{ttbox} 

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

283 
\end{ttbox} 

323  284 

285 
\subsection{A trivial example} 

286  286 
Proofs by induction typically involve simplification. Here is a proof 
287 
that~0 is a right identity: 

104  288 
\begin{ttbox} 
289 
goal Nat.thy "m+0 = m"; 

290 
{\out Level 0} 

291 
{\out m + 0 = m} 

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

286  293 
\end{ttbox} 
294 
The first step is to perform induction on the variable~$m$. This returns a 

295 
base case and inductive step as two subgoals: 

296 
\begin{ttbox} 

104  297 
by (res_inst_tac [("n","m")] induct 1); 
298 
{\out Level 1} 

299 
{\out m + 0 = m} 

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

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

302 
\end{ttbox} 

286  303 
Simplification solves the first subgoal trivially: 
104  304 
\begin{ttbox} 
305 
by (simp_tac add_ss 1); 

306 
{\out Level 2} 

307 
{\out m + 0 = m} 

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

309 
\end{ttbox} 

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

311 
induction hypothesis as a rewrite rule: 

312 
\begin{ttbox} 

313 
by (asm_simp_tac add_ss 1); 

314 
{\out Level 3} 

315 
{\out m + 0 = m} 

316 
{\out No subgoals!} 

317 
\end{ttbox} 

318 

323  319 
\subsection{An example of tracing} 
320 
Let us prove a similar result involving more complex terms. The two 

321 
equations together can be used to prove that addition is commutative. 

104  322 
\begin{ttbox} 
323 
goal Nat.thy "m+Suc(n) = Suc(m+n)"; 

324 
{\out Level 0} 

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

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

286  327 
\end{ttbox} 
328 
We again perform induction on~$m$ and get two subgoals: 

329 
\begin{ttbox} 

104  330 
by (res_inst_tac [("n","m")] induct 1); 
331 
{\out Level 1} 

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

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

286  334 
{\out 2. !!x. x + Suc(n) = Suc(x + n) ==>} 
335 
{\out Suc(x) + Suc(n) = Suc(Suc(x) + n)} 

336 
\end{ttbox} 

337 
Simplification solves the first subgoal, this time rewriting two 

338 
occurrences of~0: 

339 
\begin{ttbox} 

104  340 
by (simp_tac add_ss 1); 
341 
{\out Level 2} 

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

286  343 
{\out 1. !!x. x + Suc(n) = Suc(x + n) ==>} 
344 
{\out Suc(x) + Suc(n) = Suc(Suc(x) + n)} 

104  345 
\end{ttbox} 
346 
Switching tracing on illustrates how the simplifier solves the remaining 

347 
subgoal: 

348 
\begin{ttbox} 

349 
trace_simp := true; 

350 
by (asm_simp_tac add_ss 1); 

323  351 
\ttbreak 
104  352 
{\out Rewriting:} 
353 
{\out Suc(x) + Suc(n) == Suc(x + Suc(n))} 

323  354 
\ttbreak 
104  355 
{\out Rewriting:} 
356 
{\out x + Suc(n) == Suc(x + n)} 

323  357 
\ttbreak 
104  358 
{\out Rewriting:} 
359 
{\out Suc(x) + n == Suc(x + n)} 

323  360 
\ttbreak 
104  361 
{\out Rewriting:} 
362 
{\out Suc(Suc(x + n)) = Suc(Suc(x + n)) == True} 

323  363 
\ttbreak 
104  364 
{\out Level 3} 
365 
{\out m + Suc(n) = Suc(m + n)} 

366 
{\out No subgoals!} 

367 
\end{ttbox} 

286  368 
Many variations are possible. At Level~1 (in either example) we could have 
369 
solved both subgoals at once using the tactical \ttindex{ALLGOALS}: 

104  370 
\begin{ttbox} 
371 
by (ALLGOALS (asm_simp_tac add_ss)); 

372 
{\out Level 2} 

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

374 
{\out No subgoals!} 

375 
\end{ttbox} 

376 

323  377 
\subsection{Free variables and simplification} 
104  378 
Here is a conjecture to be proved for an arbitrary function~$f$ satisfying 
323  379 
the law $f(Suc(\Var{n})) = Suc(f(\Var{n}))$: 
104  380 
\begin{ttbox} 
381 
val [prem] = goal Nat.thy 

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

383 
{\out Level 0} 

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

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

323  386 
\ttbreak 
286  387 
{\out val prem = "f(Suc(?n)) = Suc(f(?n))} 
388 
{\out [!!n. f(Suc(n)) = Suc(f(n))]" : thm} 

323  389 
\end{ttbox} 
390 
In the theorem~{\tt prem}, note that $f$ is a free variable while 

391 
$\Var{n}$ is a schematic variable. 

392 
\begin{ttbox} 

104  393 
by (res_inst_tac [("n","i")] induct 1); 
394 
{\out Level 1} 

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

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

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

398 
\end{ttbox} 

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

400 
\begin{ttbox} 

401 
by (simp_tac add_ss 1); 

402 
{\out Level 2} 

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

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

405 
\end{ttbox} 

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

323  407 
{\tt add_ss}:% 
408 
\footnote{The previous simplifier required congruence rules for function 

409 
variables like~$f$ in order to simplify their arguments. It was more 

410 
general than the current simplifier, but harder to use and slower. The 

411 
present simplifier can be given congruence rules to realize nonstandard 

412 
simplification of a function's arguments, but this is seldom necessary.} 

104  413 
\begin{ttbox} 
414 
by (asm_simp_tac (add_ss addsimps [prem]) 1); 

415 
{\out Level 3} 

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

417 
{\out No subgoals!} 

418 
\end{ttbox} 

419 

286  420 

332  421 
\section{Permutative rewrite rules} 
323  422 
\index{rewrite rules!permutative(} 
423 

424 
A rewrite rule is {\bf permutative} if the lefthand side and righthand 

425 
side are the same up to renaming of variables. The most common permutative 

426 
rule is commutativity: $x+y = y+x$. Other examples include $(xy)z = 

427 
(xz)y$ in arithmetic and $insert(x,insert(y,A)) = insert(y,insert(x,A))$ 

428 
for sets. Such rules are common enough to merit special attention. 

429 

430 
Because ordinary rewriting loops given such rules, the simplifier employs a 

431 
special strategy, called {\bf ordered rewriting}\index{rewriting!ordered}. 

432 
There is a builtin lexicographic ordering on terms. A permutative rewrite 

433 
rule is applied only if it decreases the given term with respect to this 

434 
ordering. For example, commutativity rewrites~$b+a$ to $a+b$, but then 

435 
stops because $a+b$ is strictly less than $b+a$. The BoyerMoore theorem 

436 
prover~\cite{bm88book} also employs ordered rewriting. 

437 

438 
Permutative rewrite rules are added to simpsets just like other rewrite 

439 
rules; the simplifier recognizes their special status automatically. They 

440 
are most effective in the case of associativecommutative operators. 

441 
(Associativity by itself is not permutative.) When dealing with an 

442 
ACoperator~$f$, keep the following points in mind: 

443 
\begin{itemize}\index{associativecommutative operators} 

444 
\item The associative law must always be oriented from left to right, namely 

445 
$f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if used with 

446 
commutativity, leads to looping! Future versions of Isabelle may remove 

447 
this restriction. 

448 

449 
\item To complete your set of rewrite rules, you must add not just 

450 
associativity~(A) and commutativity~(C) but also a derived rule, {\bf 

451 
leftcommutativity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$. 

452 
\end{itemize} 

453 
Ordered rewriting with the combination of A, C, and~LC sorts a term 

454 
lexicographically: 

455 
\[\def\maps#1{\stackrel{#1}{\longmapsto}} 

456 
(b+c)+a \maps{A} b+(c+a) \maps{C} b+(a+c) \maps{LC} a+(b+c) \] 

457 
Martin and Nipkow~\cite{martinnipkow} discuss the theory and give many 

458 
examples; other algebraic structures are amenable to ordered rewriting, 

459 
such as boolean rings. 

460 

461 
\subsection{Example: sums of integers} 

462 
This example is set in Isabelle's higherorder logic. Theory 

463 
\thydx{Arith} contains the theory of arithmetic. The simpset {\tt 

464 
arith_ss} contains many arithmetic laws including distributivity 

465 
of~$\times$ over~$+$, while {\tt add_ac} is a list consisting of the A, C 

466 
and LC laws for~$+$. Let us prove the theorem 

467 
\[ \sum@{i=1}^n i = n\times(n+1)/2. \] 

468 
% 

469 
A functional~{\tt sum} represents the summation operator under the 

470 
interpretation ${\tt sum}(f,n+1) = \sum@{i=0}^n f(i)$. We extend {\tt 

471 
Arith} using a theory file: 

472 
\begin{ttbox} 

473 
NatSum = Arith + 

474 
consts sum :: "[nat=>nat, nat] => nat" 

475 
rules sum_0 "sum(f,0) = 0" 

476 
sum_Suc "sum(f,Suc(n)) = f(n) + sum(f,n)" 

477 
end 

478 
\end{ttbox} 

332  479 
After declaring {\tt open NatSum}, we make the required simpset by adding 
323  480 
the ACrules for~$+$ and the axioms for~{\tt sum}: 
481 
\begin{ttbox} 

482 
val natsum_ss = arith_ss addsimps ([sum_0,sum_Suc] \at add_ac); 

483 
{\out val natsum_ss = SS \{\ldots\} : simpset} 

484 
\end{ttbox} 

485 
Our desired theorem now reads ${\tt sum}(\lambda i.i,n+1) = 

486 
n\times(n+1)/2$. The Isabelle goal has both sides multiplied by~$2$: 

487 
\begin{ttbox} 

488 
goal NatSum.thy "Suc(Suc(0))*sum(\%i.i,Suc(n)) = n*Suc(n)"; 

489 
{\out Level 0} 

490 
{\out Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)} 

491 
{\out 1. Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)} 

492 
\end{ttbox} 

493 
Induction should not be applied until the goal is in the simplest form: 

494 
\begin{ttbox} 

495 
by (simp_tac natsum_ss 1); 

496 
{\out Level 1} 

497 
{\out Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)} 

498 
{\out 1. n + (n + (sum(\%i. i, n) + sum(\%i. i, n))) = n + n * n} 

499 
\end{ttbox} 

500 
Ordered rewriting has sorted the terms in the lefthand side. 

501 
The subgoal is now ready for induction: 

502 
\begin{ttbox} 

503 
by (nat_ind_tac "n" 1); 

504 
{\out Level 2} 

505 
{\out Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)} 

506 
{\out 1. 0 + (0 + (sum(\%i. i, 0) + sum(\%i. i, 0))) = 0 + 0 * 0} 

507 
\ttbreak 

508 
{\out 2. !!n1. n1 + (n1 + (sum(\%i. i, n1) + sum(\%i. i, n1))) =} 

509 
{\out n1 + n1 * n1 ==>} 

510 
{\out Suc(n1) +} 

511 
{\out (Suc(n1) + (sum(\%i. i, Suc(n1)) + sum(\%i. i, Suc(n1)))) =} 

512 
{\out Suc(n1) + Suc(n1) * Suc(n1)} 

513 
\end{ttbox} 

514 
Simplification proves both subgoals immediately:\index{*ALLGOALS} 

515 
\begin{ttbox} 

516 
by (ALLGOALS (asm_simp_tac natsum_ss)); 

517 
{\out Level 3} 

518 
{\out Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)} 

519 
{\out No subgoals!} 

520 
\end{ttbox} 

521 
If we had omitted {\tt add_ac} from the simpset, simplification would have 

522 
failed to prove the induction step: 

523 
\begin{ttbox} 

524 
Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n) 

525 
1. !!n1. n1 + (n1 + (sum(\%i. i, n1) + sum(\%i. i, n1))) = 

526 
n1 + n1 * n1 ==> 

527 
n1 + (n1 + (n1 + sum(\%i. i, n1) + (n1 + sum(\%i. i, n1)))) = 

528 
n1 + (n1 + (n1 + n1 * n1)) 

529 
\end{ttbox} 

530 
Ordered rewriting proves this by sorting the lefthand side. Proving 

531 
arithmetic theorems without ordered rewriting requires explicit use of 

532 
commutativity. This is tedious; try it and see! 

533 

534 
Ordered rewriting is equally successful in proving 

535 
$\sum@{i=1}^n i^3 = n^2\times(n+1)^2/4$. 

536 

537 

538 
\subsection{Reorienting equalities} 

539 
Ordered rewriting with the derived rule {\tt symmetry} can reverse equality 

540 
signs: 

541 
\begin{ttbox} 

542 
val symmetry = prove_goal HOL.thy "(x=y) = (y=x)" 

543 
(fn _ => [fast_tac HOL_cs 1]); 

544 
\end{ttbox} 

545 
This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs 

546 
in the conclusion but not~$s$, can often be brought into the right form. 

547 
For example, ordered rewriting with {\tt symmetry} can prove the goal 

548 
\[ f(a)=b \conj f(a)=c \imp b=c. \] 

549 
Here {\tt symmetry} reverses both $f(a)=b$ and $f(a)=c$ 

550 
because $f(a)$ is lexicographically greater than $b$ and~$c$. These 

551 
reoriented equations, as rewrite rules, replace $b$ and~$c$ in the 

552 
conclusion by~$f(a)$. 

553 

554 
Another example is the goal $\neg(t=u) \imp \neg(u=t)$. 

555 
The differing orientations make this appear difficult to prove. Ordered 

556 
rewriting with {\tt symmetry} makes the equalities agree. (Without 

557 
knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$ 

558 
or~$u=t$.) Then the simplifier can prove the goal outright. 

559 

560 
\index{rewrite rules!permutative)} 

561 

562 

563 
\section{*Setting up the simplifier}\label{sec:settingupsimp} 

564 
\index{simplification!setting up} 

286  565 

566 
Setting up the simplifier for new logics is complicated. This section 

323  567 
describes how the simplifier is installed for intuitionistic firstorder 
568 
logic; the code is largely taken from {\tt FOL/simpdata.ML}. 

286  569 

323  570 
The simplifier and the case splitting tactic, which reside on separate 
571 
files, are not part of Pure Isabelle. They must be loaded explicitly: 

286  572 
\begin{ttbox} 
573 
use "../Provers/simplifier.ML"; 

574 
use "../Provers/splitter.ML"; 

575 
\end{ttbox} 

576 

577 
Simplification works by reducing various objectequalities to 

323  578 
metaequality. It requires rules stating that equal terms and equivalent 
579 
formulae are also equal at the metalevel. The rule declaration part of 

580 
the file {\tt FOL/ifol.thy} contains the two lines 

581 
\begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem} 

286  582 
eq_reflection "(x=y) ==> (x==y)" 
583 
iff_reflection "(P<>Q) ==> (P==Q)" 

584 
\end{ttbox} 

323  585 
Of course, you should only assert such rules if they are true for your 
286  586 
particular logic. In Constructive Type Theory, equality is a ternary 
587 
relation of the form $a=b\in A$; the type~$A$ determines the meaning of the 

332  588 
equality essentially as a partial equivalence relation. The present 
323  589 
simplifier cannot be used. Rewriting in {\tt CTT} uses another simplifier, 
590 
which resides in the file {\tt typedsimp.ML} and is not documented. Even 

591 
this does not work for later variants of Constructive Type Theory that use 

592 
intensional equality~\cite{nordstrom90}. 

286  593 

594 

595 
\subsection{A collection of standard rewrite rules} 

596 
The file begins by proving lots of standard rewrite rules about the logical 

323  597 
connectives. These include cancellation and associative laws. To prove 
598 
them easily, it defines a function that echoes the desired law and then 

286  599 
supplies it the theorem prover for intuitionistic \FOL: 
600 
\begin{ttbox} 

601 
fun int_prove_fun s = 

602 
(writeln s; 

603 
prove_goal IFOL.thy s 

604 
(fn prems => [ (cut_facts_tac prems 1), 

605 
(Int.fast_tac 1) ])); 

606 
\end{ttbox} 

607 
The following rewrite rules about conjunction are a selection of those 

608 
proved on {\tt FOL/simpdata.ML}. Later, these will be supplied to the 

609 
standard simpset. 

610 
\begin{ttbox} 

611 
val conj_rews = map int_prove_fun 

612 
["P & True <> P", "True & P <> P", 

613 
"P & False <> False", "False & P <> False", 

614 
"P & P <> P", 

615 
"P & ~P <> False", "~P & P <> False", 

616 
"(P & Q) & R <> P & (Q & R)"]; 

617 
\end{ttbox} 

618 
The file also proves some distributive laws. As they can cause exponential 

619 
blowup, they will not be included in the standard simpset. Instead they 

323  620 
are merely bound to an \ML{} identifier, for user reference. 
286  621 
\begin{ttbox} 
622 
val distrib_rews = map int_prove_fun 

623 
["P & (Q  R) <> P&Q  P&R", 

624 
"(Q  R) & P <> Q&P  R&P", 

625 
"(P  Q > R) <> (P > R) & (Q > R)"]; 

626 
\end{ttbox} 

627 

628 

629 
\subsection{Functions for preprocessing the rewrite rules} 

323  630 
\label{sec:setmksimps} 
631 
% 

286  632 
The next step is to define the function for preprocessing rewrite rules. 
633 
This will be installed by calling {\tt setmksimps} below. Preprocessing 

634 
occurs whenever rewrite rules are added, whether by user command or 

635 
automatically. Preprocessing involves extracting atomic rewrites at the 

636 
objectlevel, then reflecting them to the metalevel. 

637 

638 
To start, the function {\tt gen_all} strips any metalevel 

639 
quantifiers from the front of the given theorem. Usually there are none 

640 
anyway. 

641 
\begin{ttbox} 

642 
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; 

643 
\end{ttbox} 

644 
The function {\tt atomize} analyses a theorem in order to extract 

645 
atomic rewrite rules. The head of all the patterns, matched by the 

646 
wildcard~{\tt _}, is the coercion function {\tt Trueprop}. 

647 
\begin{ttbox} 

648 
fun atomize th = case concl_of th of 

649 
_ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) \at 

650 
atomize(th RS conjunct2) 

651 
 _ $ (Const("op >",_) $ _ $ _) => atomize(th RS mp) 

652 
 _ $ (Const("All",_) $ _) => atomize(th RS spec) 

653 
 _ $ (Const("True",_)) => [] 

654 
 _ $ (Const("False",_)) => [] 

655 
 _ => [th]; 

656 
\end{ttbox} 

657 
There are several cases, depending upon the form of the conclusion: 

658 
\begin{itemize} 

659 
\item Conjunction: extract rewrites from both conjuncts. 

660 

661 
\item Implication: convert $P\imp Q$ to the metaimplication $P\Imp Q$ and 

662 
extract rewrites from~$Q$; these will be conditional rewrites with the 

663 
condition~$P$. 

664 

665 
\item Universal quantification: remove the quantifier, replacing the bound 

666 
variable by a schematic variable, and extract rewrites from the body. 

667 

668 
\item {\tt True} and {\tt False} contain no useful rewrites. 

669 

670 
\item Anything else: return the theorem in a singleton list. 

671 
\end{itemize} 

672 
The resulting theorems are not literally atomic  they could be 

323  673 
disjunctive, for example  but are broken down as much as possible. See 
286  674 
the file {\tt ZF/simpdata.ML} for a sophisticated translation of 
675 
settheoretic formulae into rewrite rules. 

104  676 

286  677 
The simplified rewrites must now be converted into metaequalities. The 
323  678 
rule {\tt eq_reflection} converts equality rewrites, while {\tt 
286  679 
iff_reflection} converts ifandonlyif rewrites. The latter possibility 
680 
can arise in two other ways: the negative theorem~$\neg P$ is converted to 

323  681 
$P\equiv{\tt False}$, and any other theorem~$P$ is converted to 
286  682 
$P\equiv{\tt True}$. The rules {\tt iff_reflection_F} and {\tt 
683 
iff_reflection_T} accomplish this conversion. 

684 
\begin{ttbox} 

685 
val P_iff_F = int_prove_fun "~P ==> (P <> False)"; 

686 
val iff_reflection_F = P_iff_F RS iff_reflection; 

687 
\ttbreak 

688 
val P_iff_T = int_prove_fun "P ==> (P <> True)"; 

689 
val iff_reflection_T = P_iff_T RS iff_reflection; 

690 
\end{ttbox} 

691 
The function {\tt mk_meta_eq} converts a theorem to a metaequality 

692 
using the case analysis described above. 

693 
\begin{ttbox} 

694 
fun mk_meta_eq th = case concl_of th of 

695 
_ $ (Const("op =",_)$_$_) => th RS eq_reflection 

696 
 _ $ (Const("op <>",_)$_$_) => th RS iff_reflection 

697 
 _ $ (Const("Not",_)$_) => th RS iff_reflection_F 

698 
 _ => th RS iff_reflection_T; 

699 
\end{ttbox} 

700 
The three functions {\tt gen_all}, {\tt atomize} and {\tt mk_meta_eq} will 

701 
be composed together and supplied below to {\tt setmksimps}. 

702 

703 

704 
\subsection{Making the initial simpset} 

705 
It is time to assemble these items. We open module {\tt Simplifier} to 

323  706 
gain access to its components. We define the infix operator 
707 
\ttindexbold{addcongs} to insert congruence rules; given a list of theorems, 

708 
it converts their conclusions into metaequalities and passes them to 

709 
\ttindex{addeqcongs}. 

286  710 
\begin{ttbox} 
711 
open Simplifier; 

712 
\ttbreak 

713 
infix addcongs; 

714 
fun ss addcongs congs = 

715 
ss addeqcongs (congs RL [eq_reflection,iff_reflection]); 

716 
\end{ttbox} 

717 
The list {\tt IFOL_rews} contains the default rewrite rules for firstorder 

718 
logic. The first of these is the reflexive law expressed as the 

323  719 
equivalence $(a=a)\bimp{\tt True}$; the rewrite rule $a=a$ is clearly useless. 
286  720 
\begin{ttbox} 
721 
val IFOL_rews = 

722 
[refl RS P_iff_T] \at conj_rews \at disj_rews \at not_rews \at 

723 
imp_rews \at iff_rews \at quant_rews; 

724 
\end{ttbox} 

725 
The list {\tt triv_rls} contains trivial theorems for the solver. Any 

726 
subgoal that is simplified to one of these will be removed. 

727 
\begin{ttbox} 

728 
val notFalseI = int_prove_fun "~False"; 

729 
val triv_rls = [TrueI,refl,iff_refl,notFalseI]; 

730 
\end{ttbox} 

323  731 
% 
286  732 
The basic simpset for intuitionistic \FOL{} starts with \ttindex{empty_ss}. 
733 
It preprocess rewrites using {\tt gen_all}, {\tt atomize} and {\tt 

734 
mk_meta_eq}. It solves simplified subgoals using {\tt triv_rls} and 

735 
assumptions. It uses \ttindex{asm_simp_tac} to tackle subgoals of 

736 
conditional rewrites. It takes {\tt IFOL_rews} as rewrite rules. 

737 
Other simpsets built from {\tt IFOL_ss} will inherit these items. 

323  738 
In particular, {\tt FOL_ss} extends {\tt IFOL_ss} with classical rewrite 
739 
rules such as $\neg\neg P\bimp P$. 

286  740 
\index{*setmksimps}\index{*setsolver}\index{*setsubgoaler} 
741 
\index{*addsimps}\index{*addcongs} 

742 
\begin{ttbox} 

743 
val IFOL_ss = 

744 
empty_ss 

745 
setmksimps (map mk_meta_eq o atomize o gen_all) 

746 
setsolver (fn prems => resolve_tac (triv_rls \at prems) ORELSE' 

747 
assume_tac) 

748 
setsubgoaler asm_simp_tac 

749 
addsimps IFOL_rews 

750 
addcongs [imp_cong]; 

751 
\end{ttbox} 

752 
This simpset takes {\tt imp_cong} as a congruence rule in order to use 

753 
contextual information to simplify the conclusions of implications: 

754 
\[ \List{\Var{P}\bimp\Var{P'};\; \Var{P'} \Imp \Var{Q}\bimp\Var{Q'}} \Imp 

755 
(\Var{P}\imp\Var{Q}) \bimp (\Var{P'}\imp\Var{Q'}) 

756 
\] 

757 
By adding the congruence rule {\tt conj_cong}, we could obtain a similar 

758 
effect for conjunctions. 

759 

760 

761 
\subsection{Case splitting} 

323  762 
To set up case splitting, we must prove the theorem below and pass it to 
763 
\ttindexbold{mk_case_split_tac}. The tactic \ttindexbold{split_tac} uses 

764 
{\tt mk_meta_eq}, defined above, to convert the splitting rules to 

765 
metaequalities. 

286  766 
\begin{ttbox} 
767 
val meta_iffD = 

768 
prove_goal FOL.thy "[ P==Q; Q ] ==> P" 

769 
(fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]) 

770 
\ttbreak 

771 
fun split_tac splits = 

772 
mk_case_split_tac meta_iffD (map mk_meta_eq splits); 

773 
\end{ttbox} 

774 
% 

323  775 
The splitter replaces applications of a given function; the righthand side 
776 
of the replacement can be anything. For example, here is a splitting rule 

777 
for conditional expressions: 

286  778 
\[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x})) 
779 
\conj (\lnot\Var{Q} \imp \Var{P}(\Var{y})) 

780 
\] 

323  781 
Another example is the elimination operator (which happens to be 
782 
called~$split$) for Cartesian products: 

286  783 
\[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} = 
784 
\langle a,b\rangle \imp \Var{P}(\Var{f}(a,b))) 

785 
\] 

786 
Case splits should be allowed only when necessary; they are expensive 

787 
and hard to control. Here is a typical example of use, where {\tt 

788 
expand_if} is the first rule above: 

789 
\begin{ttbox} 

790 
by (simp_tac (prop_rec_ss setloop (split_tac [expand_if])) 1); 

791 
\end{ttbox} 

792 

104  793 

794 

795 
\index{simplification)} 

796 

286  797 