author  nipkow 
Wed, 04 Aug 2004 11:25:08 +0200  
changeset 15106  e8cef6993701 
parent 15027  d23887300b96 
child 16019  0e1405402d53 
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 
13616  105 
Asm_full_simp_tac} loop because the rewrite rule $f\,\Var{x} = 
4395  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 
13616  109 
very subtle cases of nontermination. For example, invoking 
110 
{\tt Asm_full_simp_tac} on 

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

111 
\begin{ttbox} 
13616  112 
{\out 1. [ P (f x); y = x; f x = f y ] ==> Q} 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

113 
\end{ttbox} 
13616  114 
gives rise to the infinite reduction sequence 
115 
\[ 

13693
77052bb8aed3
Removed obsolete section about reordering assumptions.
berghofe
parents:
13616
diff
changeset

116 
P\,(f\,x) \stackrel{f\,x = f\,y}{\longmapsto} P\,(f\,y) \stackrel{y = x}{\longmapsto} 
77052bb8aed3
Removed obsolete section about reordering assumptions.
berghofe
parents:
13616
diff
changeset

117 
P\,(f\,x) \stackrel{f\,x = f\,y}{\longmapsto} \cdots 
13616  118 
\] 
119 
whereas applying the same tactic to 

120 
\begin{ttbox} 

121 
{\out 1. [ y = x; f x = f y; P (f x) ] ==> Q} 

122 
\end{ttbox} 

123 
terminates. 

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

124 

4395  125 
\medskip 
126 

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

130 
enormous, especially since invocations of the simplifier are often 

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

132 

133 

134 
\subsection{Modifying the current simpset} 

135 
\begin{ttbox} 

136 
Addsimps : thm list > unit 

137 
Delsimps : thm list > unit 

138 
Addsimprocs : simproc list > unit 

139 
Delsimprocs : simproc list > unit 

140 
Addcongs : thm list > unit 

141 
Delcongs : thm list > unit 

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

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

145 

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

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

149 
(conditional) metaequalities. This form is derived automatically 

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

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

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

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

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset

154 
{\S}\ref{sec:simpcongs}. 
4395  155 

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

156 
\begin{ttdescription} 
4395  157 

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

159 
$thms$ to the current simpset. 

160 

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

162 
from $thms$ from the current simpset. 

163 

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

165 
procedures $procs$ to the current simpset. 

166 

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

168 
procedures $procs$ from the current simpset. 

169 

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

171 
current simpset. 

172 

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

175 

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

177 
current simpset. 

178 

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

4395  180 
current simpset. 
181 

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

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

183 

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

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

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

188 
added automatically! 

4395  189 

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

191 
explicitly adding or deleting theorems and simplification procedures. 

192 

193 
\medskip 

194 

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

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

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

199 
afterwards. Conversely, sometimes a rule needs 

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

201 
frequent additions or deletions may indicate a badly designed 

202 
simpset. 

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

203 

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

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

207 
deleted simplification rules because they are no longer wanted, 

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

5205  209 
the unwanted rules. After this union is formed, changes to 
210 
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

211 
\end{warn} 
104  212 

213 

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

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

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

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

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

220 
sensible defaults so that most simplifier calls specify only rewrite 

221 
rules or simplification procedures. Experienced users can exploit the 

222 
other components to streamline proofs in more sophisticated manners. 

223 

224 
\subsection{Inspecting simpsets} 

225 
\begin{ttbox} 

226 
print_ss : simpset > unit 

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

231 
unsafe_finish_tac : solver list\} 

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

234 

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

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

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

238 
simplification procedures and the patterns they are invoked on are 

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

240 
nonprintable. 

241 

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

244 
and unsafe solvers. 

245 

4395  246 
\end{ttdescription} 
247 

323  248 

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

251 
empty_ss : simpset 

252 
merge_ss : simpset * simpset > simpset 

253 
\end{ttbox} 

254 
\begin{ttdescription} 

255 

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

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

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

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

4395  261 

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

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

264 
simplification procedures and congruences. The other components 

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

267 
on that.}. 

4395  268 

269 
\end{ttdescription} 

270 

271 

272 
\subsection{Accessing the current simpset} 

5575  273 
\label{sec:accesscurrentsimpset} 
4395  274 

275 
\begin{ttbox} 

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

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

280 
print_simpset : theory > unit 

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

4395  283 
\end{ttbox} 
284 

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

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

287 
modified as follows. 

288 

289 
\begin{ttdescription} 

290 

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

292 
current theory context. 

293 

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

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

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

297 

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

299 
from theory $thy$. 

300 

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

302 
reference variable from theory $thy$. 

303 

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

306 

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

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

310 
applied on. 

311 

4395  312 
\end{ttdescription} 
313 

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

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

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

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

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

322 
\end{warn} 

323 

104  324 

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

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

329 
\end{ttbox} 

330 

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

332 
form of equality, for example: 

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

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

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

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

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

343 
function for extracting equalities from arbitrary theorems. For 

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset

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

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset

347 
this; see {\S}\ref{sec:setmksimps}. The function processes theorems 
4395  348 
added by \texttt{addsimps} as well as local assumptions. 
104  349 

4395  350 
\begin{ttdescription} 
351 

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

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

354 

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

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

357 

358 
\end{ttdescription} 

104  359 

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

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

364 

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

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

367 
\indexbold{higherorder pattern}\indexbold{pattern, higherorder} 

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

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

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

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

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

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

374 

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

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

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

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

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

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

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

382 
acceptable as a conditional rewrite rule since conditions can be 

383 
arbitrary terms. 

384 

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

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

387 
though. 

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

4395  391 

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

395 
delsimprocs : simpset * simproc list > simpset 

396 
\end{ttbox} 

397 

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

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

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

403 
operation, the simplifier may offer a simplification procedure the 

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

405 
specifically fashioned for particular situations, resulting in a more 

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

407 

408 

409 
\begin{ttdescription} 

410 

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

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

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

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

417 
\end{ttdescription} 

418 

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

421 
several relations of sums over natural numbers. 

422 

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

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

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

426 
\begin{ttbox} 

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

428 
by (Simp_tac 1); 

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

430 
\end{ttbox} 

431 

4395  432 

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

434 
\begin{ttbox} 

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

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

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

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

439 
\end{ttbox} 

440 

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

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

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

449 
\] 

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

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

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

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset

454 
{\S}~\ref{sec:simpsolver} below. 
698
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset

455 

4395  456 
\begin{ttdescription} 
457 

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

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

460 
depending on the underlying objectlogic. 

461 

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

463 
derived from $thms$. 

464 

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

466 
their internal form (conclusions using metaequality) to simpset 

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

468 
on. It should be rarely used directly. 

469 

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

471 
in internal form from simpset $ss$. 

472 

473 
\end{ttdescription} 

474 

475 
\medskip 

476 

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

478 
quantifiers also supplies contextual information, this time about the 

479 
bound variable: 

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

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

483 
&&\qquad\qquad 

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

485 
\end{eqnarray*} 

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

104  488 
\[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~ 
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset

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

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

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

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

496 
\] 

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

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

499 
to prove the goal. 

500 

501 

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

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

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

508 

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

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

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

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

104  515 

4395  516 
\begin{ttdescription} 
517 

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

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

520 
simplifier context expressed as a simpset. 

521 

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

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

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

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

526 

527 
\end{ttdescription} 

528 

529 
As an example, consider the following subgoaler: 

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

533 
resolve_tac (prems_of_ss ss) ORELSE' 

534 
asm_simp_tac ss; 

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

538 
if that fails. 

539 

104  540 

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

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

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

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

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

4395  548 
\end{ttbox} 
549 

7620  550 
A solver is a tactic that attempts to solve a subgoal after 
4395  551 
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

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

286  556 

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

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

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

561 
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

562 
contains extra variables. When a simplification tactic is to be 
3108  563 
combined with other provers, especially with the classical reasoner, 
4395  564 
it is important whether it can be considered safe or not. For this 
7620  565 
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

566 

3108  567 
The standard simplification strategy solely uses the unsafe solver, 
4395  568 
which is appropriate in most cases. For special applications where 
3108  569 
the simplification process is not allowed to instantiate unknowns 
4395  570 
within the goal, simplification starts with the safe solver, but may 
571 
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

572 
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

573 
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

574 
in other subgoals. 
4395  575 

576 
\begin{ttdescription} 

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

579 

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

582 

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

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

585 
which had already been present in $ss$. 

586 

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

588 
unsafe solver of $ss$. 

589 

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

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

592 
had already been present in $ss$. 

323  593 

4395  594 
\end{ttdescription} 
595 

596 
\medskip 

104  597 

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

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

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

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

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

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

605 
passed. 

606 

607 
\medskip 

608 

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset

609 
As explained in {\S}\ref{sec:simpsubgoaler}, the subgoaler is also used 
4395  610 
to solve the premises of congruence rules. These are usually of the 
611 
form $s = \Var{x}$, where $s$ needs to be simplified and $\Var{x}$ 

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

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

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

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

616 
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

617 
tactics like \texttt{blast_tac}. 
323  618 

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

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset

621 
$\neg\Var{Q}$. To cover this case, the solver could try resolving 
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset

622 
with the theorem $\neg False$. 
104  623 

4395  624 
\medskip 
625 

104  626 
\begin{warn} 
13938  627 
If a premise of a congruence rule cannot be proved, then the 
628 
congruence is ignored. This should only happen if the rule is 

629 
\emph{conditional}  that is, contains premises not of the form $t 

630 
= \Var{x}$; otherwise it indicates that some congruence rule, or 

631 
possibly the subgoaler or solver, is faulty. 

104  632 
\end{warn} 
633 

323  634 

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

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

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

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

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

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

648 
reverse order. 

649 

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

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

653 

654 
\begin{ttdescription} 

655 

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

4395  658 

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

661 
that had already been present in $ss$. 

662 

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

664 
from $ss$. 

4395  665 

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

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

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

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

4395  671 

672 
\end{ttdescription} 

673 

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

676 
for conditional expressions: 

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

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset

678 
\conj (\neg\Var{Q} \imp \Var{P}(\Var{y})) 
5549  679 
\] 
8136  680 
Another example is the elimination operator for Cartesian products (which 
681 
happens to be called~$split$): 

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

684 
\] 

685 

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

687 
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

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

689 
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

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

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

694 
\begin{warn} 

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

696 
\end{warn} 

697 

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

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

700 
is the first rule above: 

701 
\begin{ttbox} 

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

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

708 
\end{ttbox} 

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

104  711 

712 

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

715 
\begin{ttbox} 

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

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

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

720 
full_simp_tac : simpset > int > tactic 

721 
asm_full_simp_tac : simpset > int > tactic 

722 
safe_asm_full_simp_tac : simpset > int > tactic 

723 
\end{ttbox} 

2567  724 

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

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

726 
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

727 
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

728 
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

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

4395  731 
\begin{ttdescription} 
732 

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

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

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

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

736 
\item if $safe$ is {\tt true}, the safe solver is used as explained in 
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset

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

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

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

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

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

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

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

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

745 
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

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

747 

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

750 
the basic simplification tactics that work exactly like their 

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset

751 
namesakes in {\S}\ref{sec:simpfordummies}, except that they are 
4395  752 
explicitly supplied with a simpset. 
753 

754 
\end{ttdescription} 

104  755 

4395  756 
\medskip 
104  757 

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

760 
than their capitalized counterparts. For example 

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

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

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

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

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

770 

4395  771 
\medskip 
772 

773 
Also note that functions depending implicitly on the current theory 

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

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset

775 
{\S}\ref{sec:simpfordummies}) should be considered harmful outside of 
4395  776 
actual proof scripts. In particular, ML programs like theory 
777 
definition packages or special tactics should refer to simpsets only 

778 
explicitly, via the above tactics used in conjunction with 

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

780 

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

781 

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

784 
\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  785 
simplify : simpset > thm > thm 
786 
asm_simplify : simpset > thm > thm 

787 
full_simplify : simpset > thm > thm 

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

790 
Simplifier.asm_rewrite : simpset > cterm > thm 

791 
Simplifier.full_rewrite : simpset > cterm > thm 

792 
Simplifier.asm_full_rewrite : simpset > cterm > thm 

4395  793 
\end{ttbox} 
794 

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

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset

797 
tactics described in {\S}\ref{simptactics}, but affect the whole 
5370  798 
theorem instead of just a certain subgoal. Also note that the 
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset

799 
looper~/ solver process as described in {\S}\ref{sec:simplooper} and 
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset

800 
{\S}\ref{sec:simpsolver} is omitted in forward simplification. 
5370  801 

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

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

804 
argument. 

4395  805 

806 
\begin{warn} 

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

809 
internal interface to the simplifier for special utilities. 

4395  810 
\end{warn} 
811 

812 

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

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

819 
\item[add_0] 

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

821 
\item[add_Suc] 

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

823 
\item[induct] 

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

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

826 
\end{ttdescription} 

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

833 
\subsection{A trivial example} 

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

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

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

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

843 
base case and inductive step as two subgoals: 

844 
\begin{ttbox} 

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

847 
{\out m + 0 = m} 

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

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

850 
\end{ttbox} 

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

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

857 
\end{ttbox} 

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

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

864 
{\out No subgoals!} 

865 
\end{ttbox} 

866 

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

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

871 
that addition is commutative. 

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

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

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

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

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

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

886 
\end{ttbox} 

887 
Simplification solves the first subgoal, this time rewriting two 

888 
occurrences of~0: 

889 
\begin{ttbox} 

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

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

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

897 
subgoal: 

898 
\begin{ttbox} 

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

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

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

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

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

927 
{\out No subgoals!} 

928 
\end{ttbox} 

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

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

935 
{\out No subgoals!} 

936 
\end{ttbox} 

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

4557  939 

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

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

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

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

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

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

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

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

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

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

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

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

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

962 
\end{ttbox} 

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

964 
\begin{ttbox} 

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

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

969 
\end{ttbox} 

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

976 
{\out No subgoals!} 

977 
\end{ttbox} 

978 

286  979 

332  980 
\section{Permutative rewrite rules} 
323  981 
\index{rewrite rules!permutative(} 
982 

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

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

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

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

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

988 

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

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

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

993 
cases, but can be changed for special applications. 

994 

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

997 
\end{ttbox} 

4395  998 
\begin{ttdescription} 
999 

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

1001 
term order in simpset $ss$. 

1002 

1003 
\end{ttdescription} 

1004 

1005 
\medskip 

323  1006 

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

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

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

1011 
employs ordered rewriting. 

1012 

1013 
Permutative rewrite rules are added to simpsets just like other 

1014 
rewrite rules; the simplifier recognizes their special status 

1015 
automatically. They are most effective in the case of 

1016 
associativecommutative operators. (Associativity by itself is not 

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

1018 
following points in mind: 

323  1019 
\begin{itemize}\index{associativecommutative operators} 
4395  1020 

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

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

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

1024 
standard term order. 

323  1025 

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

1027 
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

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

1031 
lexicographically: 

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

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

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

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

1036 
such as boolean rings. 

1037 

3108  1038 
\subsection{Example: sums of natural numbers} 
4395  1039 

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

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

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

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

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

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

1047 
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

1048 
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

1049 
extend \texttt{Arith} as follows: 
323  1050 
\begin{ttbox} 
1051 
NatSum = Arith + 

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

1053 
primrec 
4245  1054 
"sum f 0 = 0" 
1055 
"sum f (Suc n) = f(n) + sum f n" 

323  1056 
end 
1057 
\end{ttbox} 

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

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

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

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

5205  1069 
Goal "2 * sum (\%i.i) (Suc n) = n * Suc n"; 
323  1070 
{\out Level 0} 
3108  1071 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
1072 
{\out 1. 2 * sum (\%i. i) (Suc n) = n * Suc n} 

323  1073 
\end{ttbox} 
3108  1074 
Induction should not be applied until the goal is in the simplest 
1075 
form: 

323  1076 
\begin{ttbox} 
4245  1077 
by (Simp_tac 1); 
323  1078 
{\out Level 1} 
3108  1079 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
1080 
{\out 1. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n} 

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

323  1084 
\begin{ttbox} 
4245  1085 
by (induct_tac "n" 1); 
323  1086 
{\out Level 2} 
3108  1087 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
1088 
{\out 1. 0 + (sum (\%i. i) 0 + sum (\%i. i) 0) = 0 * 0} 

323  1089 
\ttbreak 
4245  1090 
{\out 2. !!n. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n} 
8136  1091 
{\out ==> Suc n + (sum (\%i. i) (Suc n) + sum (\%i.\,i) (Suc n)) =} 
4245  1092 
{\out Suc n * Suc n} 
323  1093 
\end{ttbox} 
1094 
Simplification proves both subgoals immediately:\index{*ALLGOALS} 

1095 
\begin{ttbox} 

4245  1096 
by (ALLGOALS Asm_simp_tac); 
323  1097 
{\out Level 3} 
3108  1098 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
323  1099 
{\out No subgoals!} 
1100 
\end{ttbox} 

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

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

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

8136  1107 
{\out ==> n + (n + sum (\%i. i) n) + (n + (n + sum (\%i.\,i) n)) =} 
4245  1108 
{\out n + (n + (n + n * n))} 
323  1109 
\end{ttbox} 
1110 
Ordered rewriting proves this by sorting the lefthand side. Proving 

1111 
arithmetic theorems without ordered rewriting requires explicit use of 

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

1113 

1114 
Ordered rewriting is equally successful in proving 

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

1116 

1117 

1118 
\subsection{Reorienting equalities} 

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

1119 
Ordered rewriting with the derived rule \texttt{symmetry} can reverse 
4557  1120 
equations: 
323  1121 
\begin{ttbox} 
1122 
val symmetry = prove_goal HOL.thy "(x=y) = (y=x)" 

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

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

1126 
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

1127 
For example, ordered rewriting with \texttt{symmetry} can prove the goal 
323  1128 
\[ 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

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

1132 
conclusion by~$f(a)$. 

1133 

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset

1134 
Another example is the goal $\neg(t=u) \imp \neg(u=t)$. 
323  1135 
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

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

1139 

1140 
\index{rewrite rules!permutative)} 

1141 

1142 

4395  1143 
\section{*Coding simplification procedures} 
1144 
\begin{ttbox} 

13474  1145 
val Simplifier.simproc: Sign.sg > string > string list 
15027  1146 
> (Sign.sg > simpset > term > thm option) > simproc 
13474  1147 
val Simplifier.simproc_i: Sign.sg > string > term list 
15027  1148 
> (Sign.sg > simpset > term > thm option) > simproc 
4395  1149 
\end{ttbox} 
1150 

1151 
\begin{ttdescription} 

13477  1152 
\item[\ttindexbold{Simplifier.simproc}~$sign$~$name$~$lhss$~$proc$] makes 
1153 
$proc$ a simplification procedure for lefthand side patterns $lhss$. The 

1154 
name just serves as a comment. The function $proc$ may be invoked by the 

1155 
simplifier for redex positions matched by one of $lhss$ as described below 

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

1157 

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

1159 
\verb,Simplifier.simproc,, but takes welltyped terms as pattern argument. 

4395  1160 
\end{ttdescription} 
1161 

1162 
Simplification procedures are applied in a twostage process as 

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

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

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

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

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

1168 
\texttt{Some~$thm$}. 

1169 

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

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

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

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

1174 
automatic preprocessing of objectlevel equivalences. 

1175 

1176 
\medskip 

1177 

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

1179 
consider etaexpansion of pair abstraction (see also 

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

1181 
model checker syntax). 

1182 

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

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

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

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

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

1190 
\end{ttbox} 

1191 
Unfortunately, term rewriting using this rule directly would not 

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

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

1194 
making it rewrite only actual abstractions. The simplification 

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

1196 
\begin{ttbox} 

13474  1197 
val pair_eta_expand_proc = 
13477  1198 
Simplifier.simproc (Theory.sign_of (the_context ())) 
1199 
"pair_eta_expand" ["f::'a*'b=>'c"] 

1200 
(fn _ => fn _ => fn t => 

1201 
case t of Abs _ => Some (mk_meta_eq pair_eta_expand) 

1202 
 _ => None); 

4395  1203 
\end{ttbox} 
1204 
This is an example of using \texttt{pair_eta_expand_proc}: 

1205 
\begin{ttbox} 

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

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

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

1209 
\end{ttbox} 

1210 

1211 
\medskip 

1212 

1213 
In the above example the simplification procedure just did fine 

1214 
grained control over rule application, beyond higherorder pattern 

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

1216 
prove particular theorems depending on the current redex. 

1217 

1218 

7990  1219 
\section{*Setting up the Simplifier}\label{sec:settingupsimp} 
323  1220 
\index{simplification!setting up} 
286  1221 

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

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

1225 
Isabelle sources. 

286  1226 

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

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

1230 
\texttt{\$ISABELLE_HOME}): 

286  1231 
\begin{ttbox} 
6569  1232 
use "\~\relax\~\relax/src/Provers/simplifier.ML"; 
1233 
use "\~\relax\~\relax/src/Provers/splitter.ML"; 

286  1234 
\end{ttbox} 
1235 

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

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

1237 
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

1238 
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

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

1243 
\end{ttbox} 

323  1244 
Of course, you should only assert such rules if they are true for your 
286  1245 
particular logic. In Constructive Type Theory, equality is a ternary 
4395  1246 
relation of the form $a=b\in A$; the type~$A$ determines the meaning 
1247 
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

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

1251 
work for later variants of Constructive Type Theory that use 

323  1252 
intensional equality~\cite{nordstrom90}. 
286  1253 

1254 

1255 
\subsection{A collection of standard rewrite rules} 

4557  1256 

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

1258 
connectives. These include cancellation and associative laws. We 

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

9695  1260 
prover for intuitionistic FOL: 
286  1261 
\begin{ttbox} 
1262 
fun int_prove_fun s = 

1263 
(writeln s; 

1264 
prove_goal IFOL.thy s 

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

4395  1266 
(IntPr.fast_tac 1) ])); 
286  1267 
\end{ttbox} 
1268 
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

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

4395  1272 
val conj_simps = map int_prove_fun 
286  1273 
["P & True <> P", "True & P <> P", 
1274 
"P & False <> False", "False & P <> False", 

1275 
"P & P <> P", 

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

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

1278 
\end{ttbox} 

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

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

323  1281 
are merely bound to an \ML{} identifier, for user reference. 
286  1282 
\begin{ttbox} 
4395  1283 
val distrib_simps = map int_prove_fun 
286  1284 
["P & (Q  R) <> P&Q  P&R", 
1285 
"(Q  R) & P <> Q&P  R&P", 

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

1287 
\end{ttbox} 

1288 

1289 

1290 
\subsection{Functions for preprocessing the rewrite rules} 

323  1291 
\label{sec:setmksimps} 
4395  1292 
\begin{ttbox}\indexbold{*setmksimps} 
1293 
setmksimps : simpset * (thm > thm list) > simpset \hfill{\bf infix 4} 

1294 
\end{ttbox} 

286  1295 
The next step is to define the function for preprocessing rewrite rules. 
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1296 
This will be installed by calling \texttt{setmksimps} below. Preprocessing 
286  1297 
occurs whenever rewrite rules are added, whether by user command or 
1298 
automatically. Preprocessing involves extracting atomic rewrites at the 

1299 
objectlevel, then reflecting them to the metalevel. 

1300 

12725  1301 
To start, the function \texttt{gen_all} strips any metalevel 
12717  1302 
quantifiers from the front of the given theorem. 
5549  1303 

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

1304 
The function \texttt{atomize} analyses a theorem in order to extract 
286  1305 
atomic rewrite rules. The head of all the patterns, matched by the 
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1306 
wildcard~\texttt{_}, is the coercion function \texttt{Trueprop}. 
286  1307 
\begin{ttbox} 
1308 
fun atomize th = case concl_of th of 

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

1310 
atomize(th RS conjunct2) 

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

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

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

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

1315 
 _ => [th]; 

1316 
\end{ttbox} 

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

1318 
\begin{itemize} 

1319 
\item Conjunction: extract rewrites from both conjuncts. 

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

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

1322 
condition~$P$. 

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

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

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

1325 
\item \texttt{True} and \texttt{False} contain no useful rewrites. 
286  1326 
\item Anything else: return the theorem in a singleton list. 
1327 
\end{itemize} 

1328 
The resulting theorems are not literally atomic  they could be 

5549 