author  berghofe 
Tue, 25 Jul 2000 18:43:52 +0200  
changeset 9445  6c93b1eb11f8 
parent 9398  0ee9b2819155 
child 9695  ec7d7f877712 
permissions  rwrr 
104  1 
%% $Id$ 
3950  2 
\chapter{Simplification} 
3 
\label{chap:simplification} 

104  4 
\index{simplification(} 
5 

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

8 
information (`local assumptions'). It provides several general hooks, 

9 
which can provide automatic case splits during rewriting, for example. 

10 
The simplifier is already set up for many of Isabelle's logics: \FOL, 

11 
\ZF, \HOL, \HOLCF. 

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

12 

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

15 
advanced features. 

16 

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

17 

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

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

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

20 

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

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

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

26 
context. 

4395  27 

28 
\begin{warn} 

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

30 
Executing proofs interactively, or loading them from ML files 

31 
without associated theories may require setting the current theory 

32 
manually via the \ttindex{context} command. 

33 
\end{warn} 

34 

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

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

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

39 
Full_simp_tac : int > tactic 

40 
Asm_full_simp_tac : int > tactic 

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

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

45 
\begin{ttdescription} 

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

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

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

49 

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

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

52 
the local assumptions. 

53 

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

55 
simplifies the assumptions (without using the assumptions to 

56 
simplify each other or the actual goal). 

57 

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

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

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

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

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

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

66 
modifications of the simpset. 

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

68 
information about internal operations. This includes any attempted 

69 
invocation of simplification procedures. 

4395  70 
\end{ttdescription} 
71 

72 
\medskip 

73 

74 
As an example, consider the theory of arithmetic in \HOL. The (rather 

75 
trivial) goal $0 + (x + 0) = x + 0 + 0$ can be solved by a single call 

76 
of \texttt{Simp_tac} as follows: 

77 
\begin{ttbox} 

78 
context Arith.thy; 

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

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

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

84 
{\out No subgoals!} 

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

85 
\end{ttbox} 
4395  86 

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

88 
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

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

90 

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

93 
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

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

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

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

98 

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

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

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

102 
\begin{ttbox} 
4395  103 
{\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

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

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

108 
terminate. Isabelle notices certain simple forms of nontermination, 

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

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

111 

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

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

115 
For example, given the subgoal 

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

116 
\begin{ttbox} 
4889  117 
{\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

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

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

122 
will not suffer from this deficiency. 

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

123 
\end{warn} 
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 

154 
\S\ref{sec:simpcongs}. 

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 

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

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

187 
\ttindex{primrec} in \HOL) implicitly augment the current simpset. 

188 
Ordinary definitions are not added automatically! 

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 

256 
\item[\ttindexbold{empty_ss}] is the empty simpset. This is not very 

257 
useful under normal circumstances because it doesn't contain 

258 
suitable tactics (subgoaler etc.). When setting up the simplifier 

259 
for a particular objectlogic, one will typically define a more 

260 
appropriate ``almost empty'' simpset. For example, in \HOL\ this is 

261 
called \ttindexbold{HOL_basic_ss}. 

262 

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

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

265 
simplification procedures and congruences. The other components 

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

268 
on that.}. 

4395  269 

270 
\end{ttdescription} 

271 

272 

273 
\subsection{Accessing the current simpset} 

5575  274 
\label{sec:accesscurrentsimpset} 
4395  275 

276 
\begin{ttbox} 

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

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

281 
print_simpset : theory > unit 

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

4395  284 
\end{ttbox} 
285 

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

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

288 
modified as follows. 

289 

290 
\begin{ttdescription} 

291 

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

293 
current theory context. 

294 

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

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

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

298 

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

300 
from theory $thy$. 

301 

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

303 
reference variable from theory $thy$. 

304 

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

307 

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

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

311 
applied on. 

312 

4395  313 
\end{ttdescription} 
314 

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

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

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

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

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

323 
\end{warn} 

324 

104  325 

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

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

330 
\end{ttbox} 

331 

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

333 
form of equality, for example: 

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

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

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

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

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

344 
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

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

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

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

104  350 

4395  351 
\begin{ttdescription} 
352 

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

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

355 

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

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

358 

359 
\end{ttdescription} 

104  360 

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

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

365 

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

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

368 
\indexbold{higherorder pattern}\indexbold{pattern, higherorder} 

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

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

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

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

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

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

375 

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

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

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

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

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

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

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

383 
acceptable as a conditional rewrite rule since conditions can be 

384 
arbitrary terms. 

385 

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

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

388 
though. 

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

4395  392 

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

396 
delsimprocs : simpset * simproc list > simpset 

397 
\end{ttbox} 

398 

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

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

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

404 
operation, the simplifier may offer a simplification procedure the 

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

406 
specifically fashioned for particular situations, resulting in a more 

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

408 

409 

410 
\begin{ttdescription} 

411 

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

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

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

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

418 
\end{ttdescription} 

419 

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

422 
several relations of sums over natural numbers. 

423 

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

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

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

427 
\begin{ttbox} 

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

429 
by (Simp_tac 1); 

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

431 
\end{ttbox} 

432 

4395  433 

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

435 
\begin{ttbox} 

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

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

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

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

440 
\end{ttbox} 

441 

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

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

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

450 
\] 

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

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

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

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

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

456 

4395  457 
\begin{ttdescription} 
458 

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

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

461 
depending on the underlying objectlogic. 

462 

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

464 
derived from $thms$. 

465 

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

467 
their internal form (conclusions using metaequality) to simpset 

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

469 
on. It should be rarely used directly. 

470 

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

472 
in internal form from simpset $ss$. 

473 

474 
\end{ttdescription} 

475 

476 
\medskip 

477 

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

479 
quantifiers also supplies contextual information, this time about the 

480 
bound variable: 

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

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

484 
&&\qquad\qquad 

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

486 
\end{eqnarray*} 

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

104  489 
\[ \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

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

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

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

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

497 
\] 

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

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

500 
to prove the goal. 

501 

502 

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

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

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

509 

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

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

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

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

104  516 

4395  517 
\begin{ttdescription} 
518 

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

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

521 
simplifier context expressed as a simpset. 

522 

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

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

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

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

527 

528 
\end{ttdescription} 

529 

530 
As an example, consider the following subgoaler: 

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

534 
resolve_tac (prems_of_ss ss) ORELSE' 

535 
asm_simp_tac ss; 

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

539 
if that fails. 

540 

104  541 

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

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

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

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

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

4395  549 
\end{ttbox} 
550 

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

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

286  557 

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

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

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

562 
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

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

567 

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

573 
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

574 
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

575 
in other subgoals. 
4395  576 

577 
\begin{ttdescription} 

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

580 

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

583 

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

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

586 
which had already been present in $ss$. 

587 

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

589 
unsafe solver of $ss$. 

590 

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

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

593 
had already been present in $ss$. 

323  594 

4395  595 
\end{ttdescription} 
596 

597 
\medskip 

104  598 

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

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

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

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

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

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

606 
passed. 

607 

608 
\medskip 

609 

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

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

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

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

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

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

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

617 
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

618 
tactics like \texttt{blast_tac}. 
323  619 

3108  620 
It may even happen that due to simplification the subgoal is no longer 
621 
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

622 
$\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

623 
with the theorem $\lnot False$. 
104  624 

4395  625 
\medskip 
626 

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

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

632 
the subgoaler or solver, is faulty. 

104  633 
\end{warn} 
634 

323  635 

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

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

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

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

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

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

649 
reverse order. 

650 

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

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

654 

655 
\begin{ttdescription} 

656 

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

4395  659 

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

662 
that had already been present in $ss$. 

663 

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

665 
from $ss$. 

4395  666 

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

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

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

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

4395  672 

673 
\end{ttdescription} 

674 

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

677 
for conditional expressions: 

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

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

680 
\] 

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

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

685 
\] 

686 

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

688 
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

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

690 
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

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

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

695 
\begin{warn} 

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

697 
\end{warn} 

698 

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

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

701 
is the first rule above: 

702 
\begin{ttbox} 

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

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

709 
\end{ttbox} 

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

104  712 

713 

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

716 
\begin{ttbox} 

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

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

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

721 
full_simp_tac : simpset > int > tactic 

722 
asm_full_simp_tac : simpset > int > tactic 

723 
safe_asm_full_simp_tac : simpset > int > tactic 

724 
\end{ttbox} 

2567  725 

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

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

727 
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

728 
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

729 
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

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

4395  732 
\begin{ttdescription} 
733 

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

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

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

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

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

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

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

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

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

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

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

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

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

746 
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

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

748 

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

751 
the basic simplification tactics that work exactly like their 

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

753 
explicitly supplied with a simpset. 

754 

755 
\end{ttdescription} 

104  756 

4395  757 
\medskip 
104  758 

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

761 
than their capitalized counterparts. For example 

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

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

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

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

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

771 

4395  772 
\medskip 
773 

774 
Also note that functions depending implicitly on the current theory 

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

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

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

778 
definition packages or special tactics should refer to simpsets only 

779 
explicitly, via the above tactics used in conjunction with 

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

781 

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

782 

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

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

788 
full_simplify : simpset > thm > thm 

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

791 
Simplifier.asm_rewrite : simpset > cterm > thm 

792 
Simplifier.full_rewrite : simpset > cterm > thm 

793 
Simplifier.asm_full_rewrite : simpset > cterm > thm 

4395  794 
\end{ttbox} 
795 

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

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

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

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

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

802 

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

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

805 
argument. 

4395  806 

807 
\begin{warn} 

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

810 
internal interface to the simplifier for special utilities. 

4395  811 
\end{warn} 
812 

813 

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

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

820 
\item[add_0] 

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

822 
\item[add_Suc] 

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

824 
\item[induct] 

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

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

827 
\end{ttdescription} 

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

834 
\subsection{A trivial example} 

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

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

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

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

844 
base case and inductive step as two subgoals: 

845 
\begin{ttbox} 

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

848 
{\out m + 0 = m} 

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

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

851 
\end{ttbox} 

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

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

858 
\end{ttbox} 

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

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

865 
{\out No subgoals!} 

866 
\end{ttbox} 

867 

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

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

872 
that addition is commutative. 

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

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

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

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

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

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

887 
\end{ttbox} 

888 
Simplification solves the first subgoal, this time rewriting two 

889 
occurrences of~0: 

890 
\begin{ttbox} 

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

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

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

898 
subgoal: 

899 
\begin{ttbox} 

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

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

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

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

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

928 
{\out No subgoals!} 

929 
\end{ttbox} 

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

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

936 
{\out No subgoals!} 

937 
\end{ttbox} 

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

4557  940 

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

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

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

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

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

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

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

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

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

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

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

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

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

963 
\end{ttbox} 

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

965 
\begin{ttbox} 

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

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

970 
\end{ttbox} 

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

977 
{\out No subgoals!} 

978 
\end{ttbox} 

979 

1213  980 
\subsection{Reordering assumptions} 
981 
\label{sec:reorderingasms} 

982 
\index{assumptions!reordering} 

983 

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

986 
to be more effective. Given the subgoal 

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

991 
\begin{ttbox} 

992 
by (rotate_tac ~2 1); 

993 
\end{ttbox} 

994 
to obtain 

995 
\begin{ttbox} 

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

1000 
\verb$Q(f a)$. 

1213  1001 

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

1003 
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

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

1009 
\begin{ttbox} 

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

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

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

4395  1017 
\end{warn} 
1018 

286  1019 

332  1020 
\section{Permutative rewrite rules} 
323  1021 
\index{rewrite rules!permutative(} 
1022 

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

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

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

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

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

1028 

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

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

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

1033 
cases, but can be changed for special applications. 

1034 

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

1037 
\end{ttbox} 

4395  1038 
\begin{ttdescription} 
1039 

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

1041 
term order in simpset $ss$. 

1042 

1043 
\end{ttdescription} 

1044 

1045 
\medskip 

323  1046 

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

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

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

1051 
employs ordered rewriting. 

1052 

1053 
Permutative rewrite rules are added to simpsets just like other 

1054 
rewrite rules; the simplifier recognizes their special status 

1055 
automatically. They are most effective in the case of 

1056 
associativecommutative operators. (Associativity by itself is not 

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

1058 
following points in mind: 

323  1059 
\begin{itemize}\index{associativecommutative operators} 
4395  1060 

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

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

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

1064 
standard term order. 

323  1065 

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

1067 
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

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

1071 
lexicographically: 

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

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

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

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

1076 
such as boolean rings. 

1077 

3108  1078 
\subsection{Example: sums of natural numbers} 
4395  1079 

1080 
This example is again set in \HOL\ (see \texttt{HOL/ex/NatSum}). 

1081 
Theory \thydx{Arith} contains natural numbers arithmetic. Its 

1082 
associated simpset contains many arithmetic laws including 

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

1083 
distributivity of~$\times$ over~$+$, while \texttt{add_ac} is a list 
4395  1084 
consisting of the A, C and LC laws for~$+$ on type \texttt{nat}. Let 
1085 
us prove the theorem 

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

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

1088 
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

1089 
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

1090 
extend \texttt{Arith} as follows: 
323  1091 
\begin{ttbox} 
1092 
NatSum = Arith + 

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

1094 
primrec 
4245  1095 
"sum f 0 = 0" 
1096 
"sum f (Suc n) = f(n) + sum f n" 

323  1097 
end 
1098 
\end{ttbox} 

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

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

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

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

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

323  1114 
\end{ttbox} 
3108  1115 
Induction should not be applied until the goal is in the simplest 
1116 
form: 

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

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

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

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

1136 
\begin{ttbox} 

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

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

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

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

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

1152 
arithmetic theorems without ordered rewriting requires explicit use of 

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

1154 

1155 
Ordered rewriting is equally successful in proving 

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

1157 

1158 

1159 
\subsection{Reorienting equalities} 

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

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

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

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

1167 
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

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

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

1173 
conclusion by~$f(a)$. 

1174 

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

1175 
Another example is the goal $\lnot(t=u) \imp \lnot(u=t)$. 
323  1176 
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

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

1180 

1181 
\index{rewrite rules!permutative)} 

1182 

1183 

4395  1184 
\section{*Coding simplification procedures} 
1185 
\begin{ttbox} 

1186 
mk_simproc: string > cterm list > 

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

1188 
\end{ttbox} 

1189 

1190 
\begin{ttdescription} 

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

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

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

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

1195 
described below. 

1196 
\end{ttdescription} 

1197 

1198 
Simplification procedures are applied in a twostage process as 

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

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

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

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

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

1204 
\texttt{Some~$thm$}. 

1205 

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

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

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

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

1210 
automatic preprocessing of objectlevel equivalences. 

1211 

1212 
\medskip 

1213 

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

1215 
consider etaexpansion of pair abstraction (see also 

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

1217 
model checker syntax). 

1218 

1219 
The {\HOL} theory of tuples (see \texttt{HOL/Prod}) provides an 

1220 
operator \texttt{split} together with some concrete syntax supporting 

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

1222 
tactic that rewrites any function $\lambda\,p.f\,p$ (where $p$ is of 

1223 
some pair type) to $\lambda\,(x,y).f\,(x,y)$. The corresponding rule 

1224 
is: 

1225 
\begin{ttbox} 

1226 
pair_eta_expand: (f::'a*'b=>'c) = (\%(x, y). f (x, y)) 

1227 
\end{ttbox} 

1228 
Unfortunately, term rewriting using this rule directly would not 

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

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

1231 
making it rewrite only actual abstractions. The simplification 

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

1233 
\begin{ttbox} 

1234 
local 

1235 
val lhss = 

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

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

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

1240 
 proc _ _ _ = None; 

1241 
in 

4560  1242 
val pair_eta_expand_proc = mk_simproc "pair_eta_expand" lhss proc; 
4395  1243 
end; 
1244 
\end{ttbox} 

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

1246 
\begin{ttbox} 

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

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

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

1250 
\end{ttbox} 

1251 

1252 
\medskip 

1253 

1254 
In the above example the simplification procedure just did fine 

1255 
grained control over rule application, beyond higherorder pattern 

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

1257 
prove particular theorems depending on the current redex. 

1258 

1259 

7990  1260 
\section{*Setting up the Simplifier}\label{sec:settingupsimp} 
323  1261 
\index{simplification!setting up} 
286  1262 

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

4395  1264 
describes how the simplifier is installed for intuitionistic 
1265 
firstorder logic; the code is largely taken from {\tt 

1266 
FOL/simpdata.ML} of the Isabelle sources. 

286  1267 

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

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

1271 
\texttt{\$ISABELLE_HOME}): 

286  1272 
\begin{ttbox} 
6569  1273 
use "\~\relax\~\relax/src/Provers/simplifier.ML"; 
1274 
use "\~\relax\~\relax/src/Provers/splitter.ML"; 

286  1275 
\end{ttbox} 
1276 

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

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

1278 
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

1279 
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

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

1284 
\end{ttbox} 

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

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

1292 
work for later variants of Constructive Type Theory that use 

323  1293 
intensional equality~\cite{nordstrom90}. 
286  1294 

1295 

1296 
\subsection{A collection of standard rewrite rules} 

4557  1297 

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

1299 
connectives. These include cancellation and associative laws. We 

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

1301 
prover for intuitionistic \FOL: 

286  1302 
\begin{ttbox} 
1303 
fun int_prove_fun s = 

1304 
(writeln s; 

1305 
prove_goal IFOL.thy s 

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

4395  1307 
(IntPr.fast_tac 1) ])); 
286  1308 
\end{ttbox} 
1309 
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

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

4395  1313 
val conj_simps = map int_prove_fun 
286  1314 
["P & True <> P", "True & P <> P", 
1315 
"P & False <> False", "False & P <> False", 

1316 
"P & P <> P", 

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

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

1319 
\end{ttbox} 

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

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

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

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

1328 
\end{ttbox} 

1329 

1330 

1331 
\subsection{Functions for preprocessing the rewrite rules} 

323  1332 
\label{sec:setmksimps} 
4395  1333 
\begin{ttbox}\indexbold{*setmksimps} 
a2b726277050
major update;
wenzel 