author  wenzelm 
Sun, 15 Oct 2000 19:50:35 +0200  
changeset 10220  2a726de6e124 
parent 9712  e33422a2eb9c 
child 11162  9e2ec5f02217 
permissions  rwrr 
104  1 
%% $Id$ 
3950  2 
\chapter{Simplification} 
3 
\label{chap:simplification} 

104  4 
\index{simplification(} 
5 

9695  6 
This chapter describes Isabelle's generic simplification package. It performs 
7 
conditional and unconditional rewriting and uses contextual information 

8 
(`local assumptions'). It provides several general hooks, which can provide 

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

10 
already set up for many of Isabelle's logics: FOL, ZF, HOL, HOLCF. 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

11 

4395  12 
The first section is a quick introduction to the simplifier that 
13 
should be sufficient to get started. The later sections explain more 

14 
advanced features. 

15 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

16 

71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

17 
\section{Simplification for dummies} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

18 
\label{sec:simpfordummies} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

19 

4395  20 
Basic use of the simplifier is particularly easy because each theory 
4557  21 
is equipped with sensible default information controlling the rewrite 
22 
process  namely the implicit {\em current 

23 
simpset}\index{simpset!current}. A suite of simple commands is 

24 
provided that refer to the implicit simpset of the current theory 

25 
context. 

4395  26 

27 
\begin{warn} 

28 
Make sure that you are working within the correct theory context. 

29 
Executing proofs interactively, or loading them from ML files 

30 
without associated theories may require setting the current theory 

31 
manually via the \ttindex{context} command. 

32 
\end{warn} 

33 

34 
\subsection{Simplification tactics} \label{sec:simpfordummiestacs} 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

35 
\begin{ttbox} 
4395  36 
Simp_tac : int > tactic 
37 
Asm_simp_tac : int > tactic 

38 
Full_simp_tac : int > tactic 

39 
Asm_full_simp_tac : int > tactic 

40 
trace_simp : bool ref \hfill{\bf initially false} 

7920  41 
debug_simp : bool ref \hfill{\bf initially false} 
4395  42 
\end{ttbox} 
43 

44 
\begin{ttdescription} 

45 
\item[\ttindexbold{Simp_tac} $i$] simplifies subgoal~$i$ using the 

46 
current simpset. It may solve the subgoal completely if it has 

47 
become trivial, using the simpset's solver tactic. 

48 

49 
\item[\ttindexbold{Asm_simp_tac}]\index{assumptions!in simplification} 

50 
is like \verb$Simp_tac$, but extracts additional rewrite rules from 

51 
the local assumptions. 

52 

53 
\item[\ttindexbold{Full_simp_tac}] is like \verb$Simp_tac$, but also 

54 
simplifies the assumptions (without using the assumptions to 

55 
simplify each other or the actual goal). 

56 

57 
\item[\ttindexbold{Asm_full_simp_tac}] is like \verb$Asm_simp_tac$, 

4889  58 
but also simplifies the assumptions. In particular, assumptions can 
59 
simplify each other. 

60 
\footnote{\texttt{Asm_full_simp_tac} used to process the assumptions from 

61 
left to right. For backwards compatibilty reasons only there is now 

62 
\texttt{Asm_lr_simp_tac} that behaves like the old \texttt{Asm_full_simp_tac}.} 

7920  63 
\item[set \ttindexbold{trace_simp};] makes the simplifier output internal 
64 
operations. This includes rewrite steps, but also bookkeeping like 

65 
modifications of the simpset. 

66 
\item[set \ttindexbold{debug_simp};] makes the simplifier output some extra 

67 
information about internal operations. This includes any attempted 

68 
invocation of simplification procedures. 

4395  69 
\end{ttdescription} 
70 

71 
\medskip 

72 

9695  73 
As an example, consider the theory of arithmetic in HOL. The (rather trivial) 
74 
goal $0 + (x + 0) = x + 0 + 0$ can be solved by a single call of 

75 
\texttt{Simp_tac} as follows: 

4395  76 
\begin{ttbox} 
77 
context Arith.thy; 

5205  78 
Goal "0 + (x + 0) = x + 0 + 0"; 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

79 
{\out 1. 0 + (x + 0) = x + 0 + 0} 
4395  80 
by (Simp_tac 1); 
81 
{\out Level 1} 

82 
{\out 0 + (x + 0) = x + 0 + 0} 

83 
{\out No subgoals!} 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

84 
\end{ttbox} 
4395  85 

86 
The simplifier uses the current simpset of \texttt{Arith.thy}, which 

87 
contains suitable theorems like $\Var{n}+0 = \Var{n}$ and $0+\Var{n} = 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

88 
\Var{n}$. 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

89 

4395  90 
\medskip In many cases, assumptions of a subgoal are also needed in 
91 
the simplification process. For example, \texttt{x = 0 ==> x + x = 0} 

92 
is solved by \texttt{Asm_simp_tac} as follows: 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

93 
\begin{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

94 
{\out 1. x = 0 ==> x + x = 0} 
2479  95 
by (Asm_simp_tac 1); 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

96 
\end{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

97 

4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

98 
\medskip \texttt{Asm_full_simp_tac} is the most powerful of this quartet 
4395  99 
of tactics but may also loop where some of the others terminate. For 
100 
example, 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

101 
\begin{ttbox} 
4395  102 
{\out 1. ALL x. f x = g (f (g x)) ==> f 0 = f 0 + 0} 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

103 
\end{ttbox} 
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

104 
is solved by \texttt{Simp_tac}, but \texttt{Asm_simp_tac} and {\tt 
4395  105 
Asm_simp_tac} loop because the rewrite rule $f\,\Var{x} = 
106 
g\,(f\,(g\,\Var{x}))$ extracted from the assumption does not 

107 
terminate. Isabelle notices certain simple forms of nontermination, 

4889  108 
but not this one. Because assumptions may simplify each other, there can be 
109 
very subtle cases of nontermination. 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

110 

71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

111 
\begin{warn} 
4889  112 
\verb$Asm_full_simp_tac$ may miss opportunities to simplify an assumption 
113 
$A@i$ using an assumption $A@j$ in case $A@j$ is to the right of $A@i$. 

114 
For example, given the subgoal 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

115 
\begin{ttbox} 
4889  116 
{\out [ \dots f a \dots; P a; ALL x. P x > f x = g x ] ==> \dots} 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

117 
\end{ttbox} 
4889  118 
\verb$Asm_full_simp_tac$ will not simplify the \texttt{f a} on the left. 
119 
This problem can be overcome by reordering assumptions (see 

120 
\S\ref{sec:reorderingasms}). Future versions of \verb$Asm_full_simp_tac$ 

121 
will not suffer from this deficiency. 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

122 
\end{warn} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

123 

4395  124 
\medskip 
125 

3108  126 
Using the simplifier effectively may take a bit of experimentation. 
4395  127 
Set the \verb$trace_simp$\index{tracing!of simplification} flag to get 
128 
a better idea of what is going on. The resulting output can be 

129 
enormous, especially since invocations of the simplifier are often 

130 
nested (e.g.\ when solving conditions of rewrite rules). 

131 

132 

133 
\subsection{Modifying the current simpset} 

134 
\begin{ttbox} 

135 
Addsimps : thm list > unit 

136 
Delsimps : thm list > unit 

137 
Addsimprocs : simproc list > unit 

138 
Delsimprocs : simproc list > unit 

139 
Addcongs : thm list > unit 

140 
Delcongs : thm list > unit 

5549  141 
Addsplits : thm list > unit 
142 
Delsplits : thm list > unit 

4395  143 
\end{ttbox} 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

144 

4395  145 
Depending on the theory context, the \texttt{Add} and \texttt{Del} 
146 
functions manipulate basic components of the associated current 

147 
simpset. Internally, all rewrite rules have to be expressed as 

148 
(conditional) metaequalities. This form is derived automatically 

149 
from objectlevel equations that are supplied by the user. Another 

150 
source of rewrite rules are \emph{simplification procedures}, that is 

151 
\ML\ functions that produce suitable theorems on demand, depending on 

152 
the current redex. Congruences are a more advanced feature; see 

153 
\S\ref{sec:simpcongs}. 

154 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

155 
\begin{ttdescription} 
4395  156 

157 
\item[\ttindexbold{Addsimps} $thms$;] adds rewrite rules derived from 

158 
$thms$ to the current simpset. 

159 

160 
\item[\ttindexbold{Delsimps} $thms$;] deletes rewrite rules derived 

161 
from $thms$ from the current simpset. 

162 

163 
\item[\ttindexbold{Addsimprocs} $procs$;] adds simplification 

164 
procedures $procs$ to the current simpset. 

165 

166 
\item[\ttindexbold{Delsimprocs} $procs$;] deletes simplification 

167 
procedures $procs$ from the current simpset. 

168 

169 
\item[\ttindexbold{Addcongs} $thms$;] adds congruence rules to the 

170 
current simpset. 

171 

5549  172 
\item[\ttindexbold{Delcongs} $thms$;] deletes congruence rules from the 
173 
current simpset. 

174 

175 
\item[\ttindexbold{Addsplits} $thms$;] adds splitting rules to the 

176 
current simpset. 

177 

178 
\item[\ttindexbold{Delsplits} $thms$;] deletes splitting rules from the 

4395  179 
current simpset. 
180 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

181 
\end{ttdescription} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

182 

9695  183 
When a new theory is built, its implicit simpset is initialized by the union 
184 
of the respective simpsets of its parent theories. In addition, certain 

185 
theory definition constructs (e.g.\ \ttindex{datatype} and \ttindex{primrec} 

186 
in HOL) implicitly augment the current simpset. Ordinary definitions are not 

187 
added automatically! 

4395  188 

189 
It is up the user to manipulate the current simpset further by 

190 
explicitly adding or deleting theorems and simplification procedures. 

191 

192 
\medskip 

193 

5205  194 
Good simpsets are hard to design. Rules that obviously simplify, 
195 
like $\Var{n}+0 = \Var{n}$, should be added to the current simpset right after 

196 
they have been proved. More specific ones (such as distributive laws, which 

197 
duplicate subterms) should be added only for specific proofs and deleted 

198 
afterwards. Conversely, sometimes a rule needs 

199 
to be removed for a certain proof and restored afterwards. The need of 

200 
frequent additions or deletions may indicate a badly designed 

201 
simpset. 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

202 

71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

203 
\begin{warn} 
4395  204 
The union of the parent simpsets (as described above) is not always 
205 
a good starting point for the new theory. If some ancestors have 

206 
deleted simplification rules because they are no longer wanted, 

207 
while others have left those rules in, then the union will contain 

5205  208 
the unwanted rules. After this union is formed, changes to 
209 
a parent simpset have no effect on the child simpset. 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

210 
\end{warn} 
104  211 

212 

286  213 
\section{Simplification sets}\index{simplification sets} 
4395  214 

215 
The simplifier is controlled by information contained in {\bf 

216 
simpsets}. These consist of several components, including rewrite 

217 
rules, simplification procedures, congruence rules, and the subgoaler, 

218 
solver and looper tactics. The simplifier should be set up with 

219 
sensible defaults so that most simplifier calls specify only rewrite 

220 
rules or simplification procedures. Experienced users can exploit the 

221 
other components to streamline proofs in more sophisticated manners. 

222 

223 
\subsection{Inspecting simpsets} 

224 
\begin{ttbox} 

225 
print_ss : simpset > unit 

4889  226 
rep_ss : simpset > \{mss : meta_simpset, 
4664  227 
subgoal_tac: simpset > int > tactic, 
7620  228 
loop_tacs : (string * (int > tactic))list, 
229 
finish_tac : solver list, 

230 
unsafe_finish_tac : solver list\} 

4395  231 
\end{ttbox} 
232 
\begin{ttdescription} 

233 

234 
\item[\ttindexbold{print_ss} $ss$;] displays the printable contents of 

235 
simpset $ss$. This includes the rewrite rules and congruences in 

236 
their internal form expressed as metaequalities. The names of the 

237 
simplification procedures and the patterns they are invoked on are 

238 
also shown. The other parts, functions and tactics, are 

239 
nonprintable. 

240 

4664  241 
\item[\ttindexbold{rep_ss} $ss$;] decomposes $ss$ as a record of its internal 
242 
components, namely the meta_simpset, the subgoaler, the loop, and the safe 

243 
and unsafe solvers. 

244 

4395  245 
\end{ttdescription} 
246 

323  247 

4395  248 
\subsection{Building simpsets} 
249 
\begin{ttbox} 

250 
empty_ss : simpset 

251 
merge_ss : simpset * simpset > simpset 

252 
\end{ttbox} 

253 
\begin{ttdescription} 

254 

9695  255 
\item[\ttindexbold{empty_ss}] is the empty simpset. This is not very useful 
256 
under normal circumstances because it doesn't contain suitable tactics 

257 
(subgoaler etc.). When setting up the simplifier for a particular 

258 
objectlogic, one will typically define a more appropriate ``almost empty'' 

259 
simpset. For example, in HOL this is called \ttindexbold{HOL_basic_ss}. 

4395  260 

261 
\item[\ttindexbold{merge_ss} ($ss@1$, $ss@2$)] merges simpsets $ss@1$ 

262 
and $ss@2$ by building the union of their respective rewrite rules, 

263 
simplification procedures and congruences. The other components 

4557  264 
(tactics etc.) cannot be merged, though; they are taken from either 
265 
simpset\footnote{Actually from $ss@1$, but it would unwise to count 

266 
on that.}. 

4395  267 

268 
\end{ttdescription} 

269 

270 

271 
\subsection{Accessing the current simpset} 

5575  272 
\label{sec:accesscurrentsimpset} 
4395  273 

274 
\begin{ttbox} 

5575  275 
simpset : unit > simpset 
276 
simpset_ref : unit > simpset ref 

4395  277 
simpset_of : theory > simpset 
278 
simpset_ref_of : theory > simpset ref 

279 
print_simpset : theory > unit 

5575  280 
SIMPSET :(simpset > tactic) > tactic 
281 
SIMPSET' :(simpset > 'a > tactic) > 'a > tactic 

4395  282 
\end{ttbox} 
283 

284 
Each theory contains a current simpset\index{simpset!current} stored 

285 
within a private ML reference variable. This can be retrieved and 

286 
modified as follows. 

287 

288 
\begin{ttdescription} 

289 

290 
\item[\ttindexbold{simpset}();] retrieves the simpset value from the 

291 
current theory context. 

292 

293 
\item[\ttindexbold{simpset_ref}();] retrieves the simpset reference 

294 
variable from the current theory context. This can be assigned to 

295 
by using \texttt{:=} in ML. 

296 

297 
\item[\ttindexbold{simpset_of} $thy$;] retrieves the simpset value 

298 
from theory $thy$. 

299 

300 
\item[\ttindexbold{simpset_ref_of} $thy$;] retrieves the simpset 

301 
reference variable from theory $thy$. 

302 

5575  303 
\item[\ttindexbold{print_simpset} $thy$;] prints the current simpset 
304 
of theory $thy$ in the same way as \texttt{print_ss}. 

305 

5574  306 
\item[\ttindexbold{SIMPSET} $tacf$, \ttindexbold{SIMPSET'} $tacf'$] 
307 
are tacticals that make a tactic depend on the implicit current 

308 
simpset of the theory associated with the proof state they are 

309 
applied on. 

310 

4395  311 
\end{ttdescription} 
312 

5574  313 
\begin{warn} 
8136  314 
There is a small difference between \texttt{(SIMPSET'~$tacf$)} and 
315 
\texttt{($tacf\,$(simpset()))}. For example \texttt{(SIMPSET' 

5574  316 
simp_tac)} would depend on the theory of the proof state it is 
317 
applied to, while \texttt{(simp_tac (simpset()))} implicitly refers 

318 
to the current theory context. Both are usually the same in proof 

319 
scripts, provided that goals are only stated within the current 

320 
theory. Robust programs would not count on that, of course. 

321 
\end{warn} 

322 

104  323 

332  324 
\subsection{Rewrite rules} 
4395  325 
\begin{ttbox} 
326 
addsimps : simpset * thm list > simpset \hfill{\bf infix 4} 

327 
delsimps : simpset * thm list > simpset \hfill{\bf infix 4} 

328 
\end{ttbox} 

329 

330 
\index{rewrite rules(} Rewrite rules are theorems expressing some 

331 
form of equality, for example: 

323  332 
\begin{eqnarray*} 
333 
Suc(\Var{m}) + \Var{n} &=& \Var{m} + Suc(\Var{n}) \\ 

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

714  335 
\Var{A} \un \Var{B} &\equiv& \{x.x\in \Var{A} \disj x\in \Var{B}\} 
323  336 
\end{eqnarray*} 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

337 
Conditional rewrites such as $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} = 
4395  338 
0$ are also permitted; the conditions can be arbitrary formulas. 
104  339 

4395  340 
Internally, all rewrite rules are translated into metaequalities, 
341 
theorems with conclusion $lhs \equiv rhs$. Each simpset contains a 

342 
function for extracting equalities from arbitrary theorems. For 

9398
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

343 
example, $\lnot(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\} 
4395  344 
\equiv False$. This function can be installed using 
345 
\ttindex{setmksimps} but only the definer of a logic should need to do 

346 
this; see \S\ref{sec:setmksimps}. The function processes theorems 

347 
added by \texttt{addsimps} as well as local assumptions. 

104  348 

4395  349 
\begin{ttdescription} 
350 

351 
\item[$ss$ \ttindexbold{addsimps} $thms$] adds rewrite rules derived 

352 
from $thms$ to the simpset $ss$. 

353 

354 
\item[$ss$ \ttindexbold{delsimps} $thms$] deletes rewrite rules 

355 
derived from $thms$ from the simpset $ss$. 

356 

357 
\end{ttdescription} 

104  358 

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

362 
{(\Var{i}+\Var{j})+\Var{k}}$ is OK. 

363 

364 
It will also deal gracefully with all rules whose lefthand sides 

365 
are socalled {\em higherorder patterns}~\cite{nipkowpatterns}. 

366 
\indexbold{higherorder pattern}\indexbold{pattern, higherorder} 

367 
These are terms in $\beta$normal form (this will always be the case 

368 
unless you have done something strange) where each occurrence of an 

369 
unknown is of the form $\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are 

370 
distinct bound variables. Hence $(\forall x.\Var{P}(x) \land 

371 
\Var{Q}(x)) \bimp (\forall x.\Var{P}(x)) \land (\forall 

372 
x.\Var{Q}(x))$ is also OK, in both directions. 

373 

374 
In some rare cases the rewriter will even deal with quite general 

375 
rules: for example ${\Var{f}(\Var{x})\in range(\Var{f})} = True$ 

376 
rewrites $g(a) \in range(g)$ to $True$, but will fail to match 

377 
$g(h(b)) \in range(\lambda x.g(h(x)))$. However, you can replace 

378 
the offending subterms (in our case $\Var{f}(\Var{x})$, which is not 

379 
a pattern) by adding new variables and conditions: $\Var{y} = 

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

381 
acceptable as a conditional rewrite rule since conditions can be 

382 
arbitrary terms. 

383 

384 
There is basically no restriction on the form of the righthand 

385 
sides. They may not contain extraneous term or type variables, 

386 
though. 

104  387 
\end{warn} 
332  388 
\index{rewrite rules)} 
389 

4395  390 

4947  391 
\subsection{*Simplification procedures} 
4395  392 
\begin{ttbox} 
393 
addsimprocs : simpset * simproc list > simpset 

394 
delsimprocs : simpset * simproc list > simpset 

395 
\end{ttbox} 

396 

4557  397 
Simplification procedures are {\ML} objects of abstract type 
398 
\texttt{simproc}. Basically they are just functions that may produce 

4395  399 
\emph{proven} rewrite rules on demand. They are associated with 
400 
certain patterns that conceptually represent lefthand sides of 

401 
equations; these are shown by \texttt{print_ss}. During its 

402 
operation, the simplifier may offer a simplification procedure the 

403 
current redex and ask for a suitable rewrite rule. Thus rules may be 

404 
specifically fashioned for particular situations, resulting in a more 

405 
powerful mechanism than term rewriting by a fixed set of rules. 

406 

407 

408 
\begin{ttdescription} 

409 

4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

410 
\item[$ss$ \ttindexbold{addsimprocs} $procs$] adds the simplification 
4395  411 
procedures $procs$ to the current simpset. 
412 

4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

413 
\item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes the simplification 
4395  414 
procedures $procs$ from the current simpset. 
415 

416 
\end{ttdescription} 

417 

4557  418 
For example, simplification procedures \ttindexbold{nat_cancel} of 
419 
\texttt{HOL/Arith} cancel common summands and constant factors out of 

420 
several relations of sums over natural numbers. 

421 

422 
Consider the following goal, which after cancelling $a$ on both sides 

423 
contains a factor of $2$. Simplifying with the simpset of 

424 
\texttt{Arith.thy} will do the cancellation automatically: 

425 
\begin{ttbox} 

426 
{\out 1. x + a + x < y + y + 2 + a + a + a + a + a} 

427 
by (Simp_tac 1); 

428 
{\out 1. x < Suc (a + (a + y))} 

429 
\end{ttbox} 

430 

4395  431 

432 
\subsection{*Congruence rules}\index{congruence rules}\label{sec:simpcongs} 

433 
\begin{ttbox} 

434 
addcongs : simpset * thm list > simpset \hfill{\bf infix 4} 

435 
delcongs : simpset * thm list > simpset \hfill{\bf infix 4} 

436 
addeqcongs : simpset * thm list > simpset \hfill{\bf infix 4} 

437 
deleqcongs : simpset * thm list > simpset \hfill{\bf infix 4} 

438 
\end{ttbox} 

439 

104  440 
Congruence rules are metaequalities of the form 
3108  441 
\[ \dots \Imp 
104  442 
f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}). 
443 
\] 

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

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

448 
\] 

4395  449 
Given this rule, the simplifier assumes $Q@1$ and extracts rewrite 
450 
rules from it when simplifying~$P@2$. Such local assumptions are 

451 
effective for rewriting formulae such as $x=0\imp y+x=y$. The local 

452 
assumptions are also provided as theorems to the solver; see 

453 
\S~\ref{sec:simpsolver} below. 

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

454 

4395  455 
\begin{ttdescription} 
456 

457 
\item[$ss$ \ttindexbold{addcongs} $thms$] adds congruence rules to the 

458 
simpset $ss$. These are derived from $thms$ in an appropriate way, 

459 
depending on the underlying objectlogic. 

460 

461 
\item[$ss$ \ttindexbold{delcongs} $thms$] deletes congruence rules 

462 
derived from $thms$. 

463 

464 
\item[$ss$ \ttindexbold{addeqcongs} $thms$] adds congruence rules in 

465 
their internal form (conclusions using metaequality) to simpset 

466 
$ss$. This is the basic mechanism that \texttt{addcongs} is built 

467 
on. It should be rarely used directly. 

468 

469 
\item[$ss$ \ttindexbold{deleqcongs} $thms$] deletes congruence rules 

470 
in internal form from simpset $ss$. 

471 

472 
\end{ttdescription} 

473 

474 
\medskip 

475 

476 
Here are some more examples. The congruence rule for bounded 

477 
quantifiers also supplies contextual information, this time about the 

478 
bound variable: 

286  479 
\begin{eqnarray*} 
480 
&&\List{\Var{A}=\Var{B};\; 

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

482 
&&\qquad\qquad 

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

484 
\end{eqnarray*} 

323  485 
The congruence rule for conditional expressions can supply contextual 
486 
information for simplifying the arms: 

104  487 
\[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~ 
9398
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

488 
\lnot\Var{q} \Imp \Var{b}=\Var{d}} \Imp 
104  489 
if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d}) 
490 
\] 

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

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

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

495 
\] 

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

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

498 
to prove the goal. 

499 

500 

4395  501 
\subsection{*The subgoaler}\label{sec:simpsubgoaler} 
502 
\begin{ttbox} 

7990  503 
setsubgoaler : 
504 
simpset * (simpset > int > tactic) > simpset \hfill{\bf infix 4} 

4395  505 
prems_of_ss : simpset > thm list 
506 
\end{ttbox} 

507 

104  508 
The subgoaler is the tactic used to solve subgoals arising out of 
509 
conditional rewrite rules or congruence rules. The default should be 

4395  510 
simplification itself. Occasionally this strategy needs to be 
511 
changed. For example, if the premise of a conditional rule is an 

512 
instance of its conclusion, as in $Suc(\Var{m}) < \Var{n} \Imp \Var{m} 

513 
< \Var{n}$, the default strategy could loop. 

104  514 

4395  515 
\begin{ttdescription} 
516 

517 
\item[$ss$ \ttindexbold{setsubgoaler} $tacf$] sets the subgoaler of 

518 
$ss$ to $tacf$. The function $tacf$ will be applied to the current 

519 
simplifier context expressed as a simpset. 

520 

521 
\item[\ttindexbold{prems_of_ss} $ss$] retrieves the current set of 

522 
premises from simplifier context $ss$. This may be nonempty only 

523 
if the simplifier has been told to utilize local assumptions in the 

524 
first place, e.g.\ if invoked via \texttt{asm_simp_tac}. 

525 

526 
\end{ttdescription} 

527 

528 
As an example, consider the following subgoaler: 

104  529 
\begin{ttbox} 
4395  530 
fun subgoaler ss = 
531 
assume_tac ORELSE' 

532 
resolve_tac (prems_of_ss ss) ORELSE' 

533 
asm_simp_tac ss; 

104  534 
\end{ttbox} 
4395  535 
This tactic first tries to solve the subgoal by assumption or by 
536 
resolving with with one of the premises, calling simplification only 

537 
if that fails. 

538 

104  539 

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

540 
\subsection{*The solver}\label{sec:simpsolver} 
4395  541 
\begin{ttbox} 
7620  542 
mk_solver : string > (thm list > int > tactic) > solver 
543 
setSolver : simpset * solver > simpset \hfill{\bf infix 4} 

544 
addSolver : simpset * solver > simpset \hfill{\bf infix 4} 

545 
setSSolver : simpset * solver > simpset \hfill{\bf infix 4} 

546 
addSSolver : simpset * solver > simpset \hfill{\bf infix 4} 

4395  547 
\end{ttbox} 
548 

7620  549 
A solver is a tactic that attempts to solve a subgoal after 
4395  550 
simplification. Typically it just proves trivial subgoals such as 
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

551 
\texttt{True} and $t=t$. It could use sophisticated means such as {\tt 
4395  552 
blast_tac}, though that could make simplification expensive. 
7620  553 
To keep things more abstract, solvers are packaged up in type 
554 
\texttt{solver}. The only way to create a solver is via \texttt{mk_solver}. 

286  555 

3108  556 
Rewriting does not instantiate unknowns. For example, rewriting 
557 
cannot prove $a\in \Var{A}$ since this requires 

558 
instantiating~$\Var{A}$. The solver, however, is an arbitrary tactic 

559 
and may instantiate unknowns as it pleases. This is the only way the 

560 
simplifier can handle a conditional rewrite rule whose condition 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

561 
contains extra variables. When a simplification tactic is to be 
3108  562 
combined with other provers, especially with the classical reasoner, 
4395  563 
it is important whether it can be considered safe or not. For this 
7620  564 
reason a simpset contains two solvers, a safe and an unsafe one. 
2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

565 

3108  566 
The standard simplification strategy solely uses the unsafe solver, 
4395  567 
which is appropriate in most cases. For special applications where 
3108  568 
the simplification process is not allowed to instantiate unknowns 
4395  569 
within the goal, simplification starts with the safe solver, but may 
570 
still apply the ordinary unsafe one in nested simplifications for 

9398
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

571 
conditional rules or congruences. Note that in this way the overall 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

572 
tactic is not totally safe: it may instantiate unknowns that appear also 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

573 
in other subgoals. 
4395  574 

575 
\begin{ttdescription} 

7620  576 
\item[\ttindexbold{mk_solver} $s$ $tacf$] converts $tacf$ into a new solver; 
577 
the string $s$ is only attached as a comment and has no other significance. 

578 

4395  579 
\item[$ss$ \ttindexbold{setSSolver} $tacf$] installs $tacf$ as the 
580 
\emph{safe} solver of $ss$. 

581 

582 
\item[$ss$ \ttindexbold{addSSolver} $tacf$] adds $tacf$ as an 

583 
additional \emph{safe} solver; it will be tried after the solvers 

584 
which had already been present in $ss$. 

585 

586 
\item[$ss$ \ttindexbold{setSolver} $tacf$] installs $tacf$ as the 

587 
unsafe solver of $ss$. 

588 

589 
\item[$ss$ \ttindexbold{addSolver} $tacf$] adds $tacf$ as an 

590 
additional unsafe solver; it will be tried after the solvers which 

591 
had already been present in $ss$. 

323  592 

4395  593 
\end{ttdescription} 
594 

595 
\medskip 

104  596 

4395  597 
\index{assumptions!in simplification} The solver tactic is invoked 
598 
with a list of theorems, namely assumptions that hold in the local 

599 
context. This may be nonempty only if the simplifier has been told 

600 
to utilize local assumptions in the first place, e.g.\ if invoked via 

601 
\texttt{asm_simp_tac}. The solver is also presented the full goal 

602 
including its assumptions in any case. Thus it can use these (e.g.\ 

603 
by calling \texttt{assume_tac}), even if the list of premises is not 

604 
passed. 

605 

606 
\medskip 

607 

608 
As explained in \S\ref{sec:simpsubgoaler}, the subgoaler is also used 

609 
to solve the premises of congruence rules. These are usually of the 

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

611 
needs to be instantiated with the result. Typically, the subgoaler 

612 
will invoke the simplifier at some point, which will eventually call 

613 
the solver. For this reason, solver tactics must be prepared to solve 

614 
goals of the form $t = \Var{x}$, usually by reflexivity. In 

615 
particular, reflexivity should be tried before any of the fancy 

4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

616 
tactics like \texttt{blast_tac}. 
323  617 

3108  618 
It may even happen that due to simplification the subgoal is no longer 
619 
an equality. For example $False \bimp \Var{Q}$ could be rewritten to 

9398
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

620 
$\lnot\Var{Q}$. To cover this case, the solver could try resolving 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

621 
with the theorem $\lnot False$. 
104  622 

4395  623 
\medskip 
624 

104  625 
\begin{warn} 
4395  626 
If the simplifier aborts with the message \texttt{Failed congruence 
3108  627 
proof!}, then the subgoaler or solver has failed to prove a 
628 
premise of a congruence rule. This should never occur under normal 

629 
circumstances; it indicates that some congruence rule, or possibly 

630 
the subgoaler or solver, is faulty. 

104  631 
\end{warn} 
632 

323  633 

4395  634 
\subsection{*The looper}\label{sec:simplooper} 
635 
\begin{ttbox} 

5549  636 
setloop : simpset * (int > tactic) > simpset \hfill{\bf infix 4} 
637 
addloop : simpset * (string * (int > tactic)) > simpset \hfill{\bf infix 4} 

638 
delloop : simpset * string > simpset \hfill{\bf infix 4} 

4395  639 
addsplits : simpset * thm list > simpset \hfill{\bf infix 4} 
5549  640 
delsplits : simpset * thm list > simpset \hfill{\bf infix 4} 
4395  641 
\end{ttbox} 
642 

5549  643 
The looper is a list of tactics that are applied after simplification, in case 
4395  644 
the solver failed to solve the simplified goal. If the looper 
645 
succeeds, the simplification process is started all over again. Each 

646 
of the subgoals generated by the looper is attacked in turn, in 

647 
reverse order. 

648 

9398
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

649 
A typical looper is \index{case splitting}: the expansion of a conditional. 
4395  650 
Another possibility is to apply an elimination rule on the 
651 
assumptions. More adventurous loopers could start an induction. 

652 

653 
\begin{ttdescription} 

654 

5549  655 
\item[$ss$ \ttindexbold{setloop} $tacf$] installs $tacf$ as the only looper 
656 
tactic of $ss$. 

4395  657 

5549  658 
\item[$ss$ \ttindexbold{addloop} $(name,tacf)$] adds $tacf$ as an additional 
659 
looper tactic with name $name$; it will be tried after the looper tactics 

660 
that had already been present in $ss$. 

661 

662 
\item[$ss$ \ttindexbold{delloop} $name$] deletes the looper tactic $name$ 

663 
from $ss$. 

4395  664 

665 
\item[$ss$ \ttindexbold{addsplits} $thms$] adds 

5549  666 
split tactics for $thms$ as additional looper tactics of $ss$. 
667 

668 
\item[$ss$ \ttindexbold{addsplits} $thms$] deletes the 

669 
split tactics for $thms$ from the looper tactics of $ss$. 

4395  670 

671 
\end{ttdescription} 

672 

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

675 
for conditional expressions: 

676 
\[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x})) 

677 
\conj (\lnot\Var{Q} \imp \Var{P}(\Var{y})) 

678 
\] 

8136  679 
Another example is the elimination operator for Cartesian products (which 
680 
happens to be called~$split$): 

5549  681 
\[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} = 
682 
\langle a,b\rangle \imp \Var{P}(\Var{f}(a,b))) 

683 
\] 

684 

685 
For technical reasons, there is a distinction between case splitting in the 

686 
conclusion and in the premises of a subgoal. The former is done by 

9398
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

687 
\texttt{split_tac} with rules like \texttt{split_if} or \texttt{option.split}, 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

688 
which do not split the subgoal, while the latter is done by 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

689 
\texttt{split_asm_tac} with rules like \texttt{split_if_asm} or 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

690 
\texttt{option.split_asm}, which split the subgoal. 
5549  691 
The operator \texttt{addsplits} automatically takes care of which tactic to 
692 
call, analyzing the form of the rules given as argument. 

693 
\begin{warn} 

694 
Due to \texttt{split_asm_tac}, the simplifier may split subgoals! 

695 
\end{warn} 

696 

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

698 
and hard to control. Here is an example of use, where \texttt{split_if} 

699 
is the first rule above: 

700 
\begin{ttbox} 

8136  701 
by (simp_tac (simpset() 
702 
addloop ("split if", split_tac [split_if])) 1); 

5549  703 
\end{ttbox} 
5776  704 
Users would usually prefer the following shortcut using \texttt{addsplits}: 
5549  705 
\begin{ttbox} 
706 
by (simp_tac (simpset() addsplits [split_if]) 1); 

707 
\end{ttbox} 

8136  708 
Casesplitting on conditional expressions is usually beneficial, so it is 
709 
enabled by default in the objectlogics \texttt{HOL} and \texttt{FOL}. 

104  710 

711 

4395  712 
\section{The simplification tactics}\label{simptactics} 
713 
\index{simplification!tactics}\index{tactics!simplification} 

714 
\begin{ttbox} 

9398
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

715 
generic_simp_tac : bool > bool * bool * bool > 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

716 
simpset > int > tactic 
4395  717 
simp_tac : simpset > int > tactic 
718 
asm_simp_tac : simpset > int > tactic 

719 
full_simp_tac : simpset > int > tactic 

720 
asm_full_simp_tac : simpset > int > tactic 

721 
safe_asm_full_simp_tac : simpset > int > tactic 

722 
\end{ttbox} 

2567  723 

9398
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

724 
\texttt{generic_simp_tac} is the basic tactic that is underlying any actual 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

725 
simplification work. The others are just instantiations of it. The rewriting 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

726 
strategy is always strictly bottom up, except for congruence rules, 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

727 
which are applied while descending into a term. Conditions in conditional 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

728 
rewrite rules are solved recursively before the rewrite rule is applied. 
104  729 

4395  730 
\begin{ttdescription} 
731 

9398
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

732 
\item[\ttindexbold{generic_simp_tac} $safe$ ($simp\_asm$, $use\_asm$, $mutual$)] 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

733 
gives direct access to the various simplification modes: 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

734 
\begin{itemize} 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

735 
\item if $safe$ is {\tt true}, the safe solver is used as explained in 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

736 
\S\ref{sec:simpsolver}, 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

737 
\item $simp\_asm$ determines whether the local assumptions are simplified, 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

738 
\item $use\_asm$ determines whether the assumptions are used as local rewrite 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

739 
rules, and 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

740 
\item $mutual$ determines whether assumptions can simplify each other rather 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

741 
than being processed from left to right. 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

742 
\end{itemize} 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

743 
This generic interface is intended 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

744 
for building special tools, e.g.\ for combining the simplifier with the 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

745 
classical reasoner. It is rarely used directly. 
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

746 

4395  747 
\item[\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac}, 
748 
\ttindexbold{full_simp_tac}, \ttindexbold{asm_full_simp_tac}] are 

749 
the basic simplification tactics that work exactly like their 

750 
namesakes in \S\ref{sec:simpfordummies}, except that they are 

751 
explicitly supplied with a simpset. 

752 

753 
\end{ttdescription} 

104  754 

4395  755 
\medskip 
104  756 

4395  757 
Local modifications of simpsets within a proof are often much cleaner 
758 
by using above tactics in conjunction with explicit simpsets, rather 

759 
than their capitalized counterparts. For example 

1213  760 
\begin{ttbox} 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

761 
Addsimps \(thms\); 
2479  762 
by (Simp_tac \(i\)); 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

763 
Delsimps \(thms\); 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

764 
\end{ttbox} 
4395  765 
can be expressed more appropriately as 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

766 
\begin{ttbox} 
4395  767 
by (simp_tac (simpset() addsimps \(thms\)) \(i\)); 
1213  768 
\end{ttbox} 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

769 

4395  770 
\medskip 
771 

772 
Also note that functions depending implicitly on the current theory 

773 
context (like capital \texttt{Simp_tac} and the other commands of 

774 
\S\ref{sec:simpfordummies}) should be considered harmful outside of 

775 
actual proof scripts. In particular, ML programs like theory 

776 
definition packages or special tactics should refer to simpsets only 

777 
explicitly, via the above tactics used in conjunction with 

778 
\texttt{simpset_of} or the \texttt{SIMPSET} tacticals. 

779 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

780 

5370  781 
\section{Forward rules and conversions} 
782 
\index{simplification!forward rules}\index{simplification!conversions} 

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

4395  784 
simplify : simpset > thm > thm 
785 
asm_simplify : simpset > thm > thm 

786 
full_simplify : simpset > thm > thm 

5370  787 
asm_full_simplify : simpset > thm > thm\medskip 
788 
Simplifier.rewrite : simpset > cterm > thm 

789 
Simplifier.asm_rewrite : simpset > cterm > thm 

790 
Simplifier.full_rewrite : simpset > cterm > thm 

791 
Simplifier.asm_full_rewrite : simpset > cterm > thm 

4395  792 
\end{ttbox} 
793 

5370  794 
The first four of these functions provide \emph{forward} rules for 
795 
simplification. Their effect is analogous to the corresponding 

796 
tactics described in \S\ref{simptactics}, but affect the whole 

797 
theorem instead of just a certain subgoal. Also note that the 

798 
looper~/ solver process as described in \S\ref{sec:simplooper} and 

799 
\S\ref{sec:simpsolver} is omitted in forward simplification. 

800 

801 
The latter four are \emph{conversions}, establishing proven equations 

802 
of the form $t \equiv u$ where the l.h.s.\ $t$ has been given as 

803 
argument. 

4395  804 

805 
\begin{warn} 

5370  806 
Forward simplification rules and conversions should be used rarely 
807 
in ordinary proof scripts. The main intention is to provide an 

808 
internal interface to the simplifier for special utilities. 

4395  809 
\end{warn} 
810 

811 

7990  812 
\section{Examples of using the Simplifier} 
3112  813 
\index{examples!of simplification} Assume we are working within {\tt 
5205  814 
FOL} (see the file \texttt{FOL/ex/Nat}) and that 
323  815 
\begin{ttdescription} 
816 
\item[Nat.thy] 

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

818 
\item[add_0] 

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

820 
\item[add_Suc] 

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

822 
\item[induct] 

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

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

825 
\end{ttdescription} 

4395  826 
We augment the implicit simpset inherited from \texttt{Nat} with the 
4557  827 
basic rewrite rules for addition of natural numbers: 
104  828 
\begin{ttbox} 
3112  829 
Addsimps [add_0, add_Suc]; 
104  830 
\end{ttbox} 
323  831 

832 
\subsection{A trivial example} 

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

104  835 
\begin{ttbox} 
5205  836 
Goal "m+0 = m"; 
104  837 
{\out Level 0} 
838 
{\out m + 0 = m} 

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

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

842 
base case and inductive step as two subgoals: 

843 
\begin{ttbox} 

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

846 
{\out m + 0 = m} 

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

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

849 
\end{ttbox} 

286  850 
Simplification solves the first subgoal trivially: 
104  851 
\begin{ttbox} 
3112  852 
by (Simp_tac 1); 
104  853 
{\out Level 2} 
854 
{\out m + 0 = m} 

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

856 
\end{ttbox} 

3112  857 
The remaining subgoal requires \ttindex{Asm_simp_tac} in order to use the 
104  858 
induction hypothesis as a rewrite rule: 
859 
\begin{ttbox} 

3112  860 
by (Asm_simp_tac 1); 
104  861 
{\out Level 3} 
862 
{\out m + 0 = m} 

863 
{\out No subgoals!} 

864 
\end{ttbox} 

865 

323  866 
\subsection{An example of tracing} 
3108  867 
\index{tracing!of simplification(}\index{*trace_simp} 
4557  868 

869 
Let us prove a similar result involving more complex terms. We prove 

870 
that addition is commutative. 

104  871 
\begin{ttbox} 
5205  872 
Goal "m+Suc(n) = Suc(m+n)"; 
104  873 
{\out Level 0} 
874 
{\out m + Suc(n) = Suc(m + n)} 

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

286  876 
\end{ttbox} 
4557  877 
Performing induction on~$m$ yields two subgoals: 
286  878 
\begin{ttbox} 
104  879 
by (res_inst_tac [("n","m")] induct 1); 
880 
{\out Level 1} 

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

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

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

885 
\end{ttbox} 

886 
Simplification solves the first subgoal, this time rewriting two 

887 
occurrences of~0: 

888 
\begin{ttbox} 

3112  889 
by (Simp_tac 1); 
104  890 
{\out Level 2} 
891 
{\out m + Suc(n) = Suc(m + n)} 

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

104  894 
\end{ttbox} 
895 
Switching tracing on illustrates how the simplifier solves the remaining 

896 
subgoal: 

897 
\begin{ttbox} 

4395  898 
set trace_simp; 
3112  899 
by (Asm_simp_tac 1); 
323  900 
\ttbreak 
3112  901 
{\out Adding rewrite rule:} 
5370  902 
{\out .x + Suc n == Suc (.x + n)} 
323  903 
\ttbreak 
5370  904 
{\out Applying instance of rewrite rule:} 
905 
{\out ?m + Suc ?n == Suc (?m + ?n)} 

104  906 
{\out Rewriting:} 
5370  907 
{\out Suc .x + Suc n == Suc (Suc .x + n)} 
323  908 
\ttbreak 
5370  909 
{\out Applying instance of rewrite rule:} 
910 
{\out Suc ?m + ?n == Suc (?m + ?n)} 

104  911 
{\out Rewriting:} 
5370  912 
{\out Suc .x + n == Suc (.x + n)} 
323  913 
\ttbreak 
5370  914 
{\out Applying instance of rewrite rule:} 
915 
{\out Suc ?m + ?n == Suc (?m + ?n)} 

104  916 
{\out Rewriting:} 
5370  917 
{\out Suc .x + n == Suc (.x + n)} 
3112  918 
\ttbreak 
5370  919 
{\out Applying instance of rewrite rule:} 
920 
{\out ?x = ?x == True} 

3112  921 
{\out Rewriting:} 
5370  922 
{\out Suc (Suc (.x + n)) = Suc (Suc (.x + n)) == True} 
323  923 
\ttbreak 
104  924 
{\out Level 3} 
925 
{\out m + Suc(n) = Suc(m + n)} 

926 
{\out No subgoals!} 

927 
\end{ttbox} 

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

104  930 
\begin{ttbox} 
3112  931 
by (ALLGOALS Asm_simp_tac); 
104  932 
{\out Level 2} 
933 
{\out m + Suc(n) = Suc(m + n)} 

934 
{\out No subgoals!} 

935 
\end{ttbox} 

3108  936 
\index{tracing!of simplification)} 
104  937 

4557  938 

323  939 
\subsection{Free variables and simplification} 
4557  940 

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

942 
satisfying the law $f(Suc(\Var{n})) = Suc(f(\Var{n}))$: 

104  943 
\begin{ttbox} 
8136  944 
val [prem] = Goal 
945 
"(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)"; 

104  946 
{\out Level 0} 
947 
{\out f(i + j) = i + f(j)} 

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

323  949 
\ttbreak 
286  950 
{\out val prem = "f(Suc(?n)) = Suc(f(?n))} 
951 
{\out [!!n. f(Suc(n)) = Suc(f(n))]" : thm} 

323  952 
\end{ttbox} 
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

953 
In the theorem~\texttt{prem}, note that $f$ is a free variable while 
323  954 
$\Var{n}$ is a schematic variable. 
955 
\begin{ttbox} 

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

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

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

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

961 
\end{ttbox} 

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

963 
\begin{ttbox} 

3112  964 
by (Simp_tac 1); 
104  965 
{\out Level 2} 
966 
{\out f(i + j) = i + f(j)} 

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

968 
\end{ttbox} 

3112  969 
The remaining subgoal requires rewriting by the premise, so we add it 
4395  970 
to the current simpset: 
104  971 
\begin{ttbox} 
4395  972 
by (asm_simp_tac (simpset() addsimps [prem]) 1); 
104  973 
{\out Level 3} 
974 
{\out f(i + j) = i + f(j)} 

975 
{\out No subgoals!} 

976 
\end{ttbox} 

977 

1213  978 
\subsection{Reordering assumptions} 
979 
\label{sec:reorderingasms} 

980 
\index{assumptions!reordering} 

981 

4395  982 
As mentioned in \S\ref{sec:simpfordummiestacs}, 
983 
\ttindex{asm_full_simp_tac} may require the assumptions to be permuted 

984 
to be more effective. Given the subgoal 

1213  985 
\begin{ttbox} 
4889  986 
{\out 1. [ ALL x. P x > f x = g x; Q(f a); P a; R ] ==> S} 
1213  987 
\end{ttbox} 
988 
we can rotate the assumptions two positions to the right 

989 
\begin{ttbox} 

990 
by (rotate_tac ~2 1); 

991 
\end{ttbox} 

992 
to obtain 

993 
\begin{ttbox} 

4889  994 
{\out 1. [ P a; R; ALL x. P x > f x = g x; Q(f a) ] ==> S} 
1213  995 
\end{ttbox} 
4889  996 
which enables \verb$asm_full_simp_tac$ to simplify \verb$Q(f a)$ to 
997 
\verb$Q(g a)$ because now all required assumptions are to the left of 

998 
\verb$Q(f a)$. 

1213  999 

1000 
Since rotation alone cannot produce arbitrary permutations, you can also pick 

1001 
out a particular assumption which needs to be rewritten and move it the the 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

1002 
right end of the assumptions. In the above case rotation can be replaced by 
1213  1003 
\begin{ttbox} 
4889  1004 
by (dres_inst_tac [("psi","Q(f a)")] asm_rl 1); 
1213  1005 
\end{ttbox} 
1006 
which is more directed and leads to 

1007 
\begin{ttbox} 

4889  1008 
{\out 1. [ ALL x. P x > f x = g x; P a; R; Q(f a) ] ==> S} 
1213  1009 
\end{ttbox} 
1010 

4395  1011 
\begin{warn} 
1012 
Reordering assumptions usually leads to brittle proofs and should be 

4889  1013 
avoided. Future versions of \verb$asm_full_simp_tac$ will completely 
1014 
remove the need for such manipulations. 

4395  1015 
\end{warn} 
1016 

286  1017 

332  1018 
\section{Permutative rewrite rules} 
323  1019 
\index{rewrite rules!permutative(} 
1020 

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

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

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

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

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

1026 

4395  1027 
Because ordinary rewriting loops given such rules, the simplifier 
1028 
employs a special strategy, called {\bf ordered 

1029 
rewriting}\index{rewriting!ordered}. There is a standard 

1030 
lexicographic ordering on terms. This should be perfectly OK in most 

1031 
cases, but can be changed for special applications. 

1032 

4947  1033 
\begin{ttbox} 
1034 
settermless : simpset * (term * term > bool) > simpset \hfill{\bf infix 4} 

1035 
\end{ttbox} 

4395  1036 
\begin{ttdescription} 
1037 

1038 
\item[$ss$ \ttindexbold{settermless} $rel$] installs relation $rel$ as 

1039 
term order in simpset $ss$. 

1040 

1041 
\end{ttdescription} 

1042 

1043 
\medskip 

323  1044 

4395  1045 
A permutative rewrite rule is applied only if it decreases the given 
1046 
term with respect to this ordering. For example, commutativity 

1047 
rewrites~$b+a$ to $a+b$, but then stops because $a+b$ is strictly less 

1048 
than $b+a$. The BoyerMoore theorem prover~\cite{bm88book} also 

1049 
employs ordered rewriting. 

1050 

1051 
Permutative rewrite rules are added to simpsets just like other 

1052 
rewrite rules; the simplifier recognizes their special status 

1053 
automatically. They are most effective in the case of 

1054 
associativecommutative operators. (Associativity by itself is not 

1055 
permutative.) When dealing with an ACoperator~$f$, keep the 

1056 
following points in mind: 

323  1057 
\begin{itemize}\index{associativecommutative operators} 
4395  1058 

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

1060 
namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if 

1061 
used with commutativity, leads to looping in conjunction with the 

1062 
standard term order. 

323  1063 

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

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

4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1066 
leftcom\mut\ativ\ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$. 
323  1067 
\end{itemize} 
1068 
Ordered rewriting with the combination of A, C, and~LC sorts a term 

1069 
lexicographically: 

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

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

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

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

1074 
such as boolean rings. 

1075 

3108  1076 
\subsection{Example: sums of natural numbers} 
4395  1077 

9695  1078 
This example is again set in HOL (see \texttt{HOL/ex/NatSum}). Theory 
1079 
\thydx{Arith} contains natural numbers arithmetic. Its associated simpset 

1080 
contains many arithmetic laws including distributivity of~$\times$ over~$+$, 

1081 
while \texttt{add_ac} is a list consisting of the A, C and LC laws for~$+$ on 

1082 
type \texttt{nat}. Let us prove the theorem 

323  1083 
\[ \sum@{i=1}^n i = n\times(n+1)/2. \] 
1084 
% 

4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1085 
A functional~\texttt{sum} represents the summation operator under the 
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1086 
interpretation $\texttt{sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$. We 
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1087 
extend \texttt{Arith} as follows: 
323  1088 
\begin{ttbox} 
1089 
NatSum = Arith + 

1387  1090 
consts sum :: [nat=>nat, nat] => nat 
9445
6c93b1eb11f8
Corrected example which still used old primrec syntax.
berghofe
parents:
9398
diff
changeset

1091 
primrec 
4245  1092 
"sum f 0 = 0" 
1093 
"sum f (Suc n) = f(n) + sum f n" 

323  1094 
end 
1095 
\end{ttbox} 

4245  1096 
The \texttt{primrec} declaration automatically adds rewrite rules for 
4557  1097 
\texttt{sum} to the default simpset. We now remove the 
1098 
\texttt{nat_cancel} simplification procedures (in order not to spoil 

1099 
the example) and insert the ACrules for~$+$: 

323  1100 
\begin{ttbox} 
4557  1101 
Delsimprocs nat_cancel; 
4245  1102 
Addsimps add_ac; 
323  1103 
\end{ttbox} 
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1104 
Our desired theorem now reads $\texttt{sum} \, (\lambda i.i) \, (n+1) = 
323  1105 
n\times(n+1)/2$. The Isabelle goal has both sides multiplied by~$2$: 
1106 
\begin{ttbox} 

5205  1107 
Goal "2 * sum (\%i.i) (Suc n) = n * Suc n"; 
323  1108 
{\out Level 0} 
3108  1109 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
1110 
{\out 1. 2 * sum (\%i. i) (Suc n) = n * Suc n} 

323  1111 
\end{ttbox} 
3108  1112 
Induction should not be applied until the goal is in the simplest 
1113 
form: 

323  1114 
\begin{ttbox} 
4245  1115 
by (Simp_tac 1); 
323  1116 
{\out Level 1} 
3108  1117 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
1118 
{\out 1. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n} 

323  1119 
\end{ttbox} 
3108  1120 
Ordered rewriting has sorted the terms in the lefthand side. The 
1121 
subgoal is now ready for induction: 

323  1122 
\begin{ttbox} 
4245  1123 
by (induct_tac "n" 1); 
323  1124 
{\out Level 2} 
3108  1125 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
1126 
{\out 1. 0 + (sum (\%i. i) 0 + sum (\%i. i) 0) = 0 * 0} 

323  1127 
\ttbreak 
4245  1128 
{\out 2. !!n. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n} 
8136  1129 
{\out ==> Suc n + (sum (\%i. i) (Suc n) + sum (\%i.\,i) (Suc n)) =} 
4245  1130 
{\out Suc n * Suc n} 
323  1131 
\end{ttbox} 
1132 
Simplification proves both subgoals immediately:\index{*ALLGOALS} 

1133 
\begin{ttbox} 

4245  1134 
by (ALLGOALS Asm_simp_tac); 
323  1135 
{\out Level 3} 
3108  1136 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
323  1137 
{\out No subgoals!} 
1138 
\end{ttbox} 

4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1139 
Simplification cannot prove the induction step if we omit \texttt{add_ac} from 
4245  1140 
the simpset. Observe that like terms have not been collected: 
323  1141 
\begin{ttbox} 
4245  1142 
{\out Level 3} 
1143 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 

1144 
{\out 1. !!n. n + sum (\%i. i) n + (n + sum (\%i. i) n) = n + n * n} 

8136  1145 
{\out ==> n + (n + sum (\%i. i) n) + (n + (n + sum (\%i.\,i) n)) =} 
4245  1146 
{\out n + (n + (n + n * n))} 
323  1147 
\end{ttbox} 
1148 
Ordered rewriting proves this by sorting the lefthand side. Proving 

1149 
arithmetic theorems without ordered rewriting requires explicit use of 

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

1151 

1152 
Ordered rewriting is equally successful in proving 

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

1154 

1155 

1156 
\subsection{Reorienting equalities} 

4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1157 
Ordered rewriting with the derived rule \texttt{symmetry} can reverse 
4557  1158 
equations: 
323  1159 
\begin{ttbox} 
1160 
val symmetry = prove_goal HOL.thy "(x=y) = (y=x)" 

3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3112
diff
changeset

1161 
(fn _ => [Blast_tac 1]); 
323  1162 
\end{ttbox} 
1163 
This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs 

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

4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1165 
For example, ordered rewriting with \texttt{symmetry} can prove the goal 
323  1166 
\[ f(a)=b \conj f(a)=c \imp b=c. \] 
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1167 
Here \texttt{symmetry} reverses both $f(a)=b$ and $f(a)=c$ 
323  1168 
because $f(a)$ is lexicographically greater than $b$ and~$c$. These 
1169 
reoriented equations, as rewrite rules, replace $b$ and~$c$ in the 

1170 
conclusion by~$f(a)$. 

1171 

9398
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset

1172 
Another example is the goal $\lnot(t=u) \imp \lnot(u=t)$. 
323  1173 
The differing orientations make this appear difficult to prove. Ordered 
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1174 
rewriting with \texttt{symmetry} makes the equalities agree. (Without 
323  1175 
knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$ 
1176 
or~$u=t$.) Then the simplifier can prove the goal outright. 

1177 

1178 
\index{rewrite rules!permutative)} 

1179 

1180 

4395  1181 
\section{*Coding simplification procedures} 
1182 
\begin{ttbox} 

1183 
mk_simproc: string > cterm list > 

1184 
(Sign.sg > thm list > term > thm option) > simproc 

1185 
\end{ttbox} 

1186 

1187 
\begin{ttdescription} 

1188 
\item[\ttindexbold{mk_simproc}~$name$~$lhss$~$proc$] makes $proc$ a 

1189 
simplification procedure for lefthand side patterns $lhss$. The 

1190 
name just serves as a comment. The function $proc$ may be invoked 

1191 
by the simplifier for redex positions matched by one of $lhss$ as 

1192 
described below. 

1193 
\end{ttdescription} 

1194 

1195 
Simplification procedures are applied in a twostage process as 

1196 
follows: The simplifier tries to match the current redex position 

1197 
against any one of the $lhs$ patterns of any simplification procedure. 

1198 
If this succeeds, it invokes the corresponding {\ML} function, passing 

1199 
with the current signature, local assumptions and the (potential) 

1200 
redex. The result may be either \texttt{None} (indicating failure) or 

1201 
\texttt{Some~$thm$}. 

1202 

1203 
Any successful result is supposed to be a (possibly conditional) 

1204 
rewrite rule $t \equiv u$ that is applicable to the current redex. 

1205 
The rule will be applied just as any ordinary rewrite rule. It is 

1206 
expected to be already in \emph{internal form}, though, bypassing the 

1207 
automatic preprocessing of objectlevel equivalences. 

1208 

1209 
\medskip 

1210 

1211 
As an example of how to write your own simplification procedures, 

1212 
consider etaexpansion of pair abstraction (see also 

1213 
\texttt{HOL/Modelcheck/MCSyn} where this is used to provide external 

1214 
model checker syntax). 

1215 

9695  1216 
The HOL theory of tuples (see \texttt{HOL/Prod}) provides an operator 
1217 
\texttt{split} together with some concrete syntax supporting 

1218 
$\lambda\,(x,y).b$ abstractions. Assume that we would like to offer a tactic 

1219 
that rewrites any function $\lambda\,p.f\,p$ (where $p$ is of some pair type) 

1220 
to $\lambda\,(x,y).f\,(x,y)$. The corresponding rule is: 

4395  1221 
\begin{ttbox} 
1222 
pair_eta_expand: (f::'a*'b=>'c) = (\%(x, y). f (x, y)) 

1223 
\end{ttbox} 

1224 
Unfortunately, term rewriting using this rule directly would not 

1225 
terminate! We now use the simplification procedure mechanism in order 

1226 
to stop the simplifier from applying this rule over and over again, 

1227 
making it rewrite only actual abstractions. The simplification 

1228 
procedure \texttt{pair_eta_expand_proc} is defined as follows: 

1229 
\begin{ttbox} 

1230 
local 

1231 
val lhss = 

4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1232 
[read_cterm (sign_of Prod.thy) 
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1233 
("f::'a*'b=>'c", TVar (("'z", 0), []))]; 
4395  1234 
val rew = mk_meta_eq pair_eta_expand; \medskip 
1235 
fun proc _ _ (Abs _) = Some rew 

1236 
 proc _ _ _ = None; 

1237 
in 

4560  1238 
val pair_eta_expand_proc = mk_simproc "pair_eta_expand" lhss proc; 
4395  1239 
end; 
1240 
\end{ttbox} 

1241 
This is an example of using \texttt{pair_eta_expand_proc}: 

1242 
\begin{ttbox} 

1243 
{\out 1. P (\%p::'a * 'a. fst p + snd p + z)} 

1244 
by (simp_tac (simpset() addsimprocs [pair_eta_expand_proc]) 1); 

1245 
{\out 1. P (\%(x::'a,y::'a). x + y + z)} 

1246 
\end{ttbox} 

1247 

1248 
\medskip 

1249 

1250 
In the above example the simplification procedure just did fine 

1251 
grained control over rule application, beyond higherorder pattern 

1252 
matching. Usually, procedures would do some more work, in particular 

1253 
prove particular theorems depending on the current redex. 

1254 

1255 

7990  1256 
\section{*Setting up the Simplifier}\label{sec:settingupsimp} 
323  1257 
\index{simplification!setting up} 
286  1258 

9712  1259 
Setting up the simplifier for new logics is complicated in the general case. 
1260 
This section describes how the simplifier is installed for intuitionistic 

1261 
firstorder logic; the code is largely taken from {\tt FOL/simpdata.ML} of the 

1262 
Isabelle sources. 

286  1263 

6569  1264 
The simplifier and the case splitting tactic, which reside on separate files, 
1265 
are not part of Pure Isabelle. They must be loaded explicitly by the 

1266 
objectlogic as follows (below \texttt{\~\relax\~\relax} refers to 

1267 
\texttt{\$ISABELLE_HOME}): 

286  1268 
\begin{ttbox} 
6569  1269 
use "\~\relax\~\relax/src/Provers/simplifier.ML"; 
1270 
use "\~\relax\~\relax/src/Provers/splitter.ML"; 

286  1271 
\end{ttbox} 
1272 

4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1273 
Simplification requires converting objectequalities to metalevel rewrite 
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1274 
rules. This demands rules stating that equal terms and equivalent formulae 
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1275 
are also equal at the metalevel. The rule declaration part of the file 
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1276 
\texttt{FOL/IFOL.thy} contains the two lines 
323  1277 
\begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem} 
286  1278 
eq_reflection "(x=y) ==> (x==y)" 
1279 
iff_reflection "(P<>Q) ==> (P==Q)" 

1280 
\end{ttbox} 

323  1281 
Of course, you should only assert such rules if they are true for your 
286  1282 
particular logic. In Constructive Type Theory, equality is a ternary 
4395  1283 
relation of the form $a=b\in A$; the type~$A$ determines the meaning 
1284 
of the equality essentially as a partial equivalence relation. The 

4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1285 
present simplifier cannot be used. Rewriting in \texttt{CTT} uses 
4395  1286 
another simplifier, which resides in the file {\tt 
1287 
Provers/typedsimp.ML} and is not documented. Even this does not 

1288 
work for later variants of Constructive Type Theory that use 

323  1289 
intensional equality~\cite{nordstrom90}. 
286  1290 

1291 

1292 
\subsection{A collection of standard rewrite rules} 

4557  1293 

1294 
We first prove lots of standard rewrite rules about the logical 

1295 
connectives. These include cancellation and associative laws. We 

1296 
define a function that echoes the desired law and then supplies it the 

9695  1297 
prover for intuitionistic FOL: 
286  1298 
\begin{ttbox} 
1299 
fun int_prove_fun s = 

1300 
(writeln s; 

1301 
prove_goal IFOL.thy s 

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

4395  1303 
(IntPr.fast_tac 1) ])); 
286  1304 
\end{ttbox} 
1305 
The following rewrite rules about conjunction are a selection of those 

4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1306 
proved on \texttt{FOL/simpdata.ML}. Later, these will be supplied to the 
286  1307 
standard simpset. 
1308 
\begin{ttbox} 

4395  1309 
val conj_simps = map int_prove_fun 
286  1310 
["P & True <> P", "True & P <> P", 
1311 
"P & False <> False", "False & P <> False", 

1312 
"P & P <> P", 

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

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

1315 
\end{ttbox} 

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

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

323  1318 
are merely bound to an \ML{} identifier, for user reference. 
286  1319 
\begin{ttbox} 
4395  1320 
val distrib_simps = map int_prove_fun 
286  1321 
["P & (Q  R) <> P&Q  P&R", 
1322 
"(Q  R) & P <> Q&P  R&P", 

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

1324 
\end{ttbox} 

1325 

1326 

1327 
\subsection{Functions for preprocessing the rewrite rules} 

323  1328 
\label{sec:setmksimps} 
4395  1329 
\begin{ttbox}\indexbold{*setmksimps} 
1330 
setmksimps : simpset * (thm > thm list) > simpset \hfill{\bf infix 4} 

1331 
\end{ttbox} 
