author  paulson 
Thu, 05 Feb 1998 10:26:59 +0100  
changeset 4597  a0bdee64194c 
parent 4560  83e1eec9cfeb 
child 4664  05d33fc7aa08 
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} 

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$, 

4557  58 
but also simplifies the assumptions one by one. Strictly working 
59 
from \emph{left to right}, it uses each assumption in the 

60 
simplification of those following. 

4395  61 

62 
\item[set \ttindexbold{trace_simp};] makes the simplifier output 

63 
internal operations. This includes rewrite steps, but also 

64 
bookkeeping like modifications of the simpset. 

65 
\end{ttdescription} 

66 

67 
\medskip 

68 

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

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

71 
of \texttt{Simp_tac} as follows: 

72 
\begin{ttbox} 

73 
context Arith.thy; 

74 
goal Arith.thy "0 + (x + 0) = x + 0 + 0"; 

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

75 
{\out 1. 0 + (x + 0) = x + 0 + 0} 
4395  76 
by (Simp_tac 1); 
77 
{\out Level 1} 

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

79 
{\out No subgoals!} 

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

80 
\end{ttbox} 
4395  81 

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

83 
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

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

85 

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

88 
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

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

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

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

93 

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

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

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

97 
\begin{ttbox} 
4395  98 
{\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

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

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

103 
terminate. Isabelle notices certain simple forms of nontermination, 

104 
but not this one. 

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

105 

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

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

107 
Since \verb$Asm_full_simp_tac$ works from left to right, it sometimes 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

108 
misses opportunities for simplification: given the subgoal 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

109 
\begin{ttbox} 
4395  110 
{\out [ P (f a); f a = t ] ==> \dots} 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

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

112 
\verb$Asm_full_simp_tac$ will not simplify the first assumption using the 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

113 
second but will leave the assumptions unchanged. See 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

114 
\S\ref{sec:reorderingasms} for ways around this problem. 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

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

116 

4395  117 
\medskip 
118 

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

122 
enormous, especially since invocations of the simplifier are often 

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

124 

125 

126 
\subsection{Modifying the current simpset} 

127 
\begin{ttbox} 

128 
Addsimps : thm list > unit 

129 
Delsimps : thm list > unit 

130 
Addsimprocs : simproc list > unit 

131 
Delsimprocs : simproc list > unit 

132 
Addcongs : thm list > unit 

133 
Delcongs : thm list > unit 

134 
\end{ttbox} 

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

135 

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

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

139 
(conditional) metaequalities. This form is derived automatically 

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

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

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

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

144 
\S\ref{sec:simpcongs}. 

145 

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

146 
\begin{ttdescription} 
4395  147 

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

149 
$thms$ to the current simpset. 

150 

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

152 
from $thms$ from the current simpset. 

153 

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

155 
procedures $procs$ to the current simpset. 

156 

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

158 
procedures $procs$ from the current simpset. 

159 

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

161 
current simpset. 

162 

163 
\item[\ttindexbold{Delcongs} $thms$;] deletes congruence rules to the 

164 
current simpset. 

165 

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

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

167 

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

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

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

172 
Ordinary definitions are not added automatically! 

173 

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

175 
explicitly adding or deleting theorems and simplification procedures. 

176 

177 
\medskip 

178 

179 
Good simpsets are hard to design. As a rule of thump, generally 

180 
useful ``simplification rules'' like $\Var{n}+0 = \Var{n}$ should be 

181 
added to the current simpset right after they have been proved. Those 

182 
of a more specific nature (e.g.\ the laws of de~Morgan, which alter 

183 
the structure of a formula) should only be added for specific proofs 

184 
and deleted again afterwards. Conversely, it may also happen that a 

185 
generally useful rule needs to be removed for a certain proof and is 

186 
added again afterwards. The need of frequent temporary additions or 

187 
deletions may indicate a badly designed simpset. 

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

188 

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

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

192 
deleted simplification rules because they are no longer wanted, 

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

194 
the unwanted rules. 

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

195 
\end{warn} 
104  196 

197 

286  198 
\section{Simplification sets}\index{simplification sets} 
4395  199 

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

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

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

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

204 
sensible defaults so that most simplifier calls specify only rewrite 

205 
rules or simplification procedures. Experienced users can exploit the 

206 
other components to streamline proofs in more sophisticated manners. 

207 

208 
\subsection{Inspecting simpsets} 

209 
\begin{ttbox} 

210 
print_ss : simpset > unit 

211 
\end{ttbox} 

212 
\begin{ttdescription} 

213 

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

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

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

217 
simplification procedures and the patterns they are invoked on are 

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

219 
nonprintable. 

220 

221 
\end{ttdescription} 

222 

323  223 

4395  224 
\subsection{Building simpsets} 
225 
\begin{ttbox} 

226 
empty_ss : simpset 

227 
merge_ss : simpset * simpset > simpset 

228 
\end{ttbox} 

229 
\begin{ttdescription} 

230 

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

232 
useful under normal circumstances because it doesn't contain 

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

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

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

236 
called \ttindexbold{HOL_basic_ss}. 

237 

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

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

240 
simplification procedures and congruences. The other components 

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

243 
on that.}. 

4395  244 

245 
\end{ttdescription} 

246 

247 

248 
\subsection{Accessing the current simpset} 

249 

250 
\begin{ttbox} 

251 
simpset : unit > simpset 

252 
simpset_ref : unit > simpset ref 

253 
simpset_of : theory > simpset 

254 
simpset_ref_of : theory > simpset ref 

255 
print_simpset : theory > unit 

256 
\end{ttbox} 

257 

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

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

260 
modified as follows. 

261 

262 
\begin{ttdescription} 

263 

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

265 
current theory context. 

266 

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

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

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

270 

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

272 
from theory $thy$. 

273 

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

275 
reference variable from theory $thy$. 

276 

277 
\item[\ttindexbold{print_simpset} $thy$;] prints the current simpset 

278 
of theory $thy$ in the same way as \texttt{print_ss}. 

279 

280 
\end{ttdescription} 

281 

104  282 

332  283 
\subsection{Rewrite rules} 
4395  284 
\begin{ttbox} 
285 
addsimps : simpset * thm list > simpset \hfill{\bf infix 4} 

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

287 
\end{ttbox} 

288 

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

290 
form of equality, for example: 

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

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

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

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

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

301 
function for extracting equalities from arbitrary theorems. For 

302 
example, $\neg(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\} 

303 
\equiv False$. This function can be installed using 

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

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

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

104  307 

4395  308 
\begin{ttdescription} 
309 

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

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

312 

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

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

315 

316 
\end{ttdescription} 

104  317 

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

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

322 

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

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

325 
\indexbold{higherorder pattern}\indexbold{pattern, higherorder} 

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

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

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

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

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

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

332 

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

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

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

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

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

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

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

340 
acceptable as a conditional rewrite rule since conditions can be 

341 
arbitrary terms. 

342 

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

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

345 
though. 

104  346 
\end{warn} 
332  347 
\index{rewrite rules)} 
348 

4395  349 

350 
\subsection{Simplification procedures} 

351 
\begin{ttbox} 

352 
addsimprocs : simpset * simproc list > simpset 

353 
delsimprocs : simpset * simproc list > simpset 

354 
\end{ttbox} 

355 

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

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

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

361 
operation, the simplifier may offer a simplification procedure the 

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

363 
specifically fashioned for particular situations, resulting in a more 

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

365 

366 

367 
\begin{ttdescription} 

368 

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

369 
\item[$ss$ \ttindexbold{addsimprocs} $procs$] adds the simplification 
4395  370 
procedures $procs$ to the current simpset. 
371 

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

372 
\item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes the simplification 
4395  373 
procedures $procs$ from the current simpset. 
374 

375 
\end{ttdescription} 

376 

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

379 
several relations of sums over natural numbers. 

380 

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

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

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

384 
\begin{ttbox} 

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

386 
by (Simp_tac 1); 

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

388 
\end{ttbox} 

389 

4395  390 

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

392 
\begin{ttbox} 

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

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

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

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

397 
\end{ttbox} 

398 

104  399 
Congruence rules are metaequalities of the form 
3108  400 
\[ \dots \Imp 
104  401 
f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}). 
402 
\] 

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

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

407 
\] 

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

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

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

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

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

413 

4395  414 
\begin{ttdescription} 
415 

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

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

418 
depending on the underlying objectlogic. 

419 

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

421 
derived from $thms$. 

422 

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

424 
their internal form (conclusions using metaequality) to simpset 

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

426 
on. It should be rarely used directly. 

427 

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

429 
in internal form from simpset $ss$. 

430 

431 
\end{ttdescription} 

432 

433 
\medskip 

434 

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

436 
quantifiers also supplies contextual information, this time about the 

437 
bound variable: 

286  438 
\begin{eqnarray*} 
439 
&&\List{\Var{A}=\Var{B};\; 

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

441 
&&\qquad\qquad 

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

443 
\end{eqnarray*} 

323  444 
The congruence rule for conditional expressions can supply contextual 
445 
information for simplifying the arms: 

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

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

449 
\] 

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

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

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

454 
\] 

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

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

457 
to prove the goal. 

458 

459 

4395  460 
\subsection{*The subgoaler}\label{sec:simpsubgoaler} 
461 
\begin{ttbox} 

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

463 
prems_of_ss : simpset > thm list 

464 
\end{ttbox} 

465 

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

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

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

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

104  472 

4395  473 
\begin{ttdescription} 
474 

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

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

477 
simplifier context expressed as a simpset. 

478 

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

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

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

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

483 

484 
\end{ttdescription} 

485 

486 
As an example, consider the following subgoaler: 

104  487 
\begin{ttbox} 
4395  488 
fun subgoaler ss = 
489 
assume_tac ORELSE' 

490 
resolve_tac (prems_of_ss ss) ORELSE' 

491 
asm_simp_tac ss; 

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

495 
if that fails. 

496 

104  497 

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

498 
\subsection{*The solver}\label{sec:simpsolver} 
4395  499 
\begin{ttbox} 
500 
setSolver : simpset * (thm list > int > tactic) > simpset \hfill{\bf infix 4} 

501 
addSolver : simpset * (thm list > int > tactic) > simpset \hfill{\bf infix 4} 

502 
setSSolver : simpset * (thm list > int > tactic) > simpset \hfill{\bf infix 4} 

503 
addSSolver : simpset * (thm list > int > tactic) > simpset \hfill{\bf infix 4} 

504 
\end{ttbox} 

505 

2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

506 
The solver is a pair of tactics that attempt to solve a subgoal after 
4395  507 
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

508 
\texttt{True} and $t=t$. It could use sophisticated means such as {\tt 
4395  509 
blast_tac}, though that could make simplification expensive. 
286  510 

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

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

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

515 
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

516 
contains extra variables. When a simplification tactic is to be 
3108  517 
combined with other provers, especially with the classical reasoner, 
4395  518 
it is important whether it can be considered safe or not. For this 
519 
reason the solver is split into a safe and an unsafe part. 

2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

520 

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

526 
conditional rules or congruences. 

527 

528 
\begin{ttdescription} 

529 

530 
\item[$ss$ \ttindexbold{setSSolver} $tacf$] installs $tacf$ as the 

531 
\emph{safe} solver of $ss$. 

532 

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

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

535 
which had already been present in $ss$. 

536 

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

538 
unsafe solver of $ss$. 

539 

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

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

542 
had already been present in $ss$. 

323  543 

4395  544 
\end{ttdescription} 
545 

546 
\medskip 

104  547 

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

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

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

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

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

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

555 
passed. 

556 

557 
\medskip 

558 

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

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

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

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

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

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

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

566 
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

567 
tactics like \texttt{blast_tac}. 
323  568 

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

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

572 
with the theorem $\neg False$. 

104  573 

4395  574 
\medskip 
575 

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

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

581 
the subgoaler or solver, is faulty. 

104  582 
\end{warn} 
583 

323  584 

4395  585 
\subsection{*The looper}\label{sec:simplooper} 
586 
\begin{ttbox} 

587 
setloop : simpset * (int > tactic) > simpset \hfill{\bf infix 4} 

588 
addloop : simpset * (int > tactic) > simpset \hfill{\bf infix 4} 

589 
addsplits : simpset * thm list > simpset \hfill{\bf infix 4} 

590 
\end{ttbox} 

591 

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

593 
the solver failed to solve the simplified goal. If the looper 

594 
succeeds, the simplification process is started all over again. Each 

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

596 
reverse order. 

597 

598 
A typical looper is case splitting: the expansion of a conditional. 

599 
Another possibility is to apply an elimination rule on the 

600 
assumptions. More adventurous loopers could start an induction. 

601 

602 
\begin{ttdescription} 

603 

604 
\item[$ss$ \ttindexbold{setloop} $tacf$] installs $tacf$ as the looper 

605 
of $ss$. 

606 

607 
\item[$ss$ \ttindexbold{addloop} $tacf$] adds $tacf$ as an additional 

608 
looper; it will be tried after the loopers which had already been 

609 
present in $ss$. 

610 

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

612 
\texttt{(split_tac~$thms$)} as an additional looper. 

613 

614 
\end{ttdescription} 

615 

104  616 

617 

4395  618 
\section{The simplification tactics}\label{simptactics} 
619 
\index{simplification!tactics}\index{tactics!simplification} 

620 
\begin{ttbox} 

621 
simp_tac : simpset > int > tactic 

622 
asm_simp_tac : simpset > int > tactic 

623 
full_simp_tac : simpset > int > tactic 

624 
asm_full_simp_tac : simpset > int > tactic 

625 
safe_asm_full_simp_tac : simpset > int > tactic 

626 
SIMPSET : (simpset > tactic) > tactic 

627 
SIMPSET' : (simpset > 'a > tactic) > 'a > tactic 

628 
\end{ttbox} 

2567  629 

4395  630 
These are the basic tactics that are underlying any actual 
631 
simplification work. The rewriting strategy is always strictly bottom 

632 
up, except for congruence rules, which are applied while descending 

633 
into a term. Conditions in conditional rewrite rules are solved 

634 
recursively before the rewrite rule is applied. 

104  635 

4395  636 
\begin{ttdescription} 
637 

638 
\item[\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac}, 

639 
\ttindexbold{full_simp_tac}, \ttindexbold{asm_full_simp_tac}] are 

640 
the basic simplification tactics that work exactly like their 

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

642 
explicitly supplied with a simpset. 

643 

644 
\item[\ttindexbold{safe_asm_full_simp_tac}] is like 

645 
\texttt{asm_full_simp_tac}, but uses the safe solver as explained in 

646 
\S\ref{sec:simpsolver}. This tactic is mainly intended for 

647 
building special tools, e.g.\ for combining the simplifier with the 

648 
classical reasoner. It is rarely used directly. 

649 

650 
\item[\ttindexbold{SIMPSET} $tacf$, \ttindexbold{SIMPSET'} $tacf'$] 

651 
are tacticals that make a tactic depend on the implicit current 

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

653 
applied on. 

104  654 

4395  655 
\end{ttdescription} 
104  656 

4395  657 
\medskip 
104  658 

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

661 
than their capitalized counterparts. For example 

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

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

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

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

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

671 

4395  672 
\medskip 
673 

674 
Also note that functions depending implicitly on the current theory 

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

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

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

678 
definition packages or special tactics should refer to simpsets only 

679 
explicitly, via the above tactics used in conjunction with 

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

681 

682 
\begin{warn} 

683 
There is a subtle difference between \texttt{(SIMPSET'~$tacf$)} and 

684 
\texttt{($tacf$~(simpset()))}. For example \texttt{(SIMPSET' 

685 
simp_tac)} would depend on the theory of the proof state it is 

686 
applied to, while \texttt{(simp_tac (simpset()))} implicitly refers 

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

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

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

690 
\end{warn} 

691 

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

692 

4395  693 
\section{Forward simplification rules} 
694 
\index{simplification!forward rules} 

695 
\begin{ttbox}\index{*simplify}\index{*asm_simplify}\index{*full_simplify}\index{*asm_full_simplify} 

696 
simplify : simpset > thm > thm 

697 
asm_simplify : simpset > thm > thm 

698 
full_simplify : simpset > thm > thm 

699 
asm_full_simplify : simpset > thm > thm 

700 
\end{ttbox} 

701 

4557  702 
These functions provide \emph{forward} rules for simplification. 
703 
Their effect is analogous to the corresponding tactics described in 

704 
\S\ref{simptactics}, but affect the whole theorem instead of just a 

705 
certain subgoal. Also note that the looper~/ solver process as 

706 
described in \S\ref{sec:simplooper} and \S\ref{sec:simpsolver} is 

707 
omitted in forward simplification. 

4395  708 

709 
\begin{warn} 

710 
Forward simplification should be used rarely in ordinary proof 

711 
scripts. It as mainly intended to provide an internal interface to 

4557  712 
the simplifier for special utilities. 
4395  713 
\end{warn} 
714 

715 

716 
\section{Examples of using the simplifier} 

3112  717 
\index{examples!of simplification} Assume we are working within {\tt 
718 
FOL} (cf.\ \texttt{FOL/ex/Nat}) and that 

323  719 
\begin{ttdescription} 
720 
\item[Nat.thy] 

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

722 
\item[add_0] 

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

724 
\item[add_Suc] 

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

726 
\item[induct] 

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

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

729 
\end{ttdescription} 

4395  730 
We augment the implicit simpset inherited from \texttt{Nat} with the 
4557  731 
basic rewrite rules for addition of natural numbers: 
104  732 
\begin{ttbox} 
3112  733 
Addsimps [add_0, add_Suc]; 
104  734 
\end{ttbox} 
323  735 

736 
\subsection{A trivial example} 

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

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

741 
{\out Level 0} 

742 
{\out m + 0 = m} 

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

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

746 
base case and inductive step as two subgoals: 

747 
\begin{ttbox} 

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

750 
{\out m + 0 = m} 

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

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

753 
\end{ttbox} 

286  754 
Simplification solves the first subgoal trivially: 
104  755 
\begin{ttbox} 
3112  756 
by (Simp_tac 1); 
104  757 
{\out Level 2} 
758 
{\out m + 0 = m} 

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

760 
\end{ttbox} 

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

3112  764 
by (Asm_simp_tac 1); 
104  765 
{\out Level 3} 
766 
{\out m + 0 = m} 

767 
{\out No subgoals!} 

768 
\end{ttbox} 

769 

323  770 
\subsection{An example of tracing} 
3108  771 
\index{tracing!of simplification(}\index{*trace_simp} 
4557  772 

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

774 
that addition is commutative. 

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

777 
{\out Level 0} 

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

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

286  780 
\end{ttbox} 
4557  781 
Performing induction on~$m$ yields two subgoals: 
286  782 
\begin{ttbox} 
104  783 
by (res_inst_tac [("n","m")] induct 1); 
784 
{\out Level 1} 

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

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

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

789 
\end{ttbox} 

790 
Simplification solves the first subgoal, this time rewriting two 

791 
occurrences of~0: 

792 
\begin{ttbox} 

3112  793 
by (Simp_tac 1); 
104  794 
{\out Level 2} 
795 
{\out m + Suc(n) = Suc(m + n)} 

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

104  798 
\end{ttbox} 
799 
Switching tracing on illustrates how the simplifier solves the remaining 

800 
subgoal: 

801 
\begin{ttbox} 

4395  802 
set trace_simp; 
3112  803 
by (Asm_simp_tac 1); 
323  804 
\ttbreak 
3112  805 
{\out Adding rewrite rule:} 
806 
{\out .x + Suc(n) == Suc(.x + n)} 

323  807 
\ttbreak 
104  808 
{\out Rewriting:} 
3112  809 
{\out Suc(.x) + Suc(n) == Suc(.x + Suc(n))} 
323  810 
\ttbreak 
104  811 
{\out Rewriting:} 
3112  812 
{\out .x + Suc(n) == Suc(.x + n)} 
323  813 
\ttbreak 
104  814 
{\out Rewriting:} 
3112  815 
{\out Suc(.x) + n == Suc(.x + n)} 
816 
\ttbreak 

817 
{\out Rewriting:} 

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

323  819 
\ttbreak 
104  820 
{\out Level 3} 
821 
{\out m + Suc(n) = Suc(m + n)} 

822 
{\out No subgoals!} 

823 
\end{ttbox} 

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

104  826 
\begin{ttbox} 
3112  827 
by (ALLGOALS Asm_simp_tac); 
104  828 
{\out Level 2} 
829 
{\out m + Suc(n) = Suc(m + n)} 

830 
{\out No subgoals!} 

831 
\end{ttbox} 

3108  832 
\index{tracing!of simplification)} 
104  833 

4557  834 

323  835 
\subsection{Free variables and simplification} 
4557  836 

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

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

104  839 
\begin{ttbox} 
840 
val [prem] = goal Nat.thy 

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

842 
{\out Level 0} 

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

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

323  845 
\ttbreak 
286  846 
{\out val prem = "f(Suc(?n)) = Suc(f(?n))} 
847 
{\out [!!n. f(Suc(n)) = Suc(f(n))]" : thm} 

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

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

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

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

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

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

857 
\end{ttbox} 

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

859 
\begin{ttbox} 

3112  860 
by (Simp_tac 1); 
104  861 
{\out Level 2} 
862 
{\out f(i + j) = i + f(j)} 

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

864 
\end{ttbox} 

3112  865 
The remaining subgoal requires rewriting by the premise, so we add it 
4395  866 
to the current simpset: 
104  867 
\begin{ttbox} 
4395  868 
by (asm_simp_tac (simpset() addsimps [prem]) 1); 
104  869 
{\out Level 3} 
870 
{\out f(i + j) = i + f(j)} 

871 
{\out No subgoals!} 

872 
\end{ttbox} 

873 

1213  874 
\subsection{Reordering assumptions} 
875 
\label{sec:reorderingasms} 

876 
\index{assumptions!reordering} 

877 

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

880 
to be more effective. Given the subgoal 

1213  881 
\begin{ttbox} 
882 
{\out 1. [ P(f(a)); Q; f(a) = t; R ] ==> S} 

883 
\end{ttbox} 

884 
we can rotate the assumptions two positions to the right 

885 
\begin{ttbox} 

886 
by (rotate_tac ~2 1); 

887 
\end{ttbox} 

888 
to obtain 

889 
\begin{ttbox} 

890 
{\out 1. [ f(a) = t; R; P(f(a)); Q ] ==> S} 

891 
\end{ttbox} 

892 
which enables \verb$asm_full_simp_tac$ to simplify \verb$P(f(a))$ to 

893 
\verb$P(t)$. 

894 

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

896 
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

897 
right end of the assumptions. In the above case rotation can be replaced by 
1213  898 
\begin{ttbox} 
899 
by (dres_inst_tac [("psi","P(f(a))")] asm_rl 1); 

900 
\end{ttbox} 

901 
which is more directed and leads to 

902 
\begin{ttbox} 

903 
{\out 1. [ Q; f(a) = t; R; P(f(a)) ] ==> S} 

904 
\end{ttbox} 

905 

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

908 
avoided. Future versions of \verb$asm_full_simp_tac$ may remove the 

909 
need for such manipulations. 

910 
\end{warn} 

911 

286  912 

332  913 
\section{Permutative rewrite rules} 
323  914 
\index{rewrite rules!permutative(} 
4395  915 
\begin{ttbox} 
916 
settermless : simpset * (term * term > bool) > simpset \hfill{\bf infix 4} 

917 
\end{ttbox} 

323  918 

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

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

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

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

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

924 

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

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

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

929 
cases, but can be changed for special applications. 

930 

931 
\begin{ttdescription} 

932 

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

934 
term order in simpset $ss$. 

935 

936 
\end{ttdescription} 

937 

938 
\medskip 

323  939 

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

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

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

944 
employs ordered rewriting. 

945 

946 
Permutative rewrite rules are added to simpsets just like other 

947 
rewrite rules; the simplifier recognizes their special status 

948 
automatically. They are most effective in the case of 

949 
associativecommutative operators. (Associativity by itself is not 

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

951 
following points in mind: 

323  952 
\begin{itemize}\index{associativecommutative operators} 
4395  953 

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

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

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

957 
standard term order. 

323  958 

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

960 
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

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

964 
lexicographically: 

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

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

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

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

969 
such as boolean rings. 

970 

3108  971 
\subsection{Example: sums of natural numbers} 
4395  972 

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

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

975 
associated simpset contains many arithmetic laws including 

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

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

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

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

981 
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

982 
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

983 
extend \texttt{Arith} as follows: 
323  984 
\begin{ttbox} 
985 
NatSum = Arith + 

1387  986 
consts sum :: [nat=>nat, nat] => nat 
4245  987 
primrec "sum" nat 
988 
"sum f 0 = 0" 

989 
"sum f (Suc n) = f(n) + sum f n" 

323  990 
end 
991 
\end{ttbox} 

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

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

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

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

3108  1003 
goal NatSum.thy "2 * sum (\%i.i) (Suc n) = n * Suc n"; 
323  1004 
{\out Level 0} 
3108  1005 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
1006 
{\out 1. 2 * sum (\%i. i) (Suc n) = n * Suc n} 

323  1007 
\end{ttbox} 
3108  1008 
Induction should not be applied until the goal is in the simplest 
1009 
form: 

323  1010 
\begin{ttbox} 
4245  1011 
by (Simp_tac 1); 
323  1012 
{\out Level 1} 
3108  1013 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
1014 
{\out 1. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n} 

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

323  1018 
\begin{ttbox} 
4245  1019 
by (induct_tac "n" 1); 
323  1020 
{\out Level 2} 
3108  1021 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
1022 
{\out 1. 0 + (sum (\%i. i) 0 + sum (\%i. i) 0) = 0 * 0} 

323  1023 
\ttbreak 
4245  1024 
{\out 2. !!n. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n} 
1025 
{\out ==> Suc n + (sum (\%i. i) (Suc n) + sum (\%i. i) (Suc n)) =} 

1026 
{\out Suc n * Suc n} 

323  1027 
\end{ttbox} 
1028 
Simplification proves both subgoals immediately:\index{*ALLGOALS} 

1029 
\begin{ttbox} 

4245  1030 
by (ALLGOALS Asm_simp_tac); 
323  1031 
{\out Level 3} 
3108  1032 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
323  1033 
{\out No subgoals!} 
1034 
\end{ttbox} 

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

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

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

1041 
{\out ==> n + (n + sum (\%i. i) n) + (n + (n + sum (\%i. i) n)) =} 

1042 
{\out n + (n + (n + n * n))} 

323  1043 
\end{ttbox} 
1044 
Ordered rewriting proves this by sorting the lefthand side. Proving 

1045 
arithmetic theorems without ordered rewriting requires explicit use of 

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

1047 

1048 
Ordered rewriting is equally successful in proving 

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

1050 

1051 

1052 
\subsection{Reorienting equalities} 

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

1053 
Ordered rewriting with the derived rule \texttt{symmetry} can reverse 
4557  1054 
equations: 
323  1055 
\begin{ttbox} 
1056 
val symmetry = prove_goal HOL.thy "(x=y) = (y=x)" 

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

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

1060 
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

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

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

1066 
conclusion by~$f(a)$. 

1067 

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

1069 
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

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

1073 

1074 
\index{rewrite rules!permutative)} 

1075 

1076 

4395  1077 
\section{*Coding simplification procedures} 
1078 
\begin{ttbox} 

1079 
mk_simproc: string > cterm list > 

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

1081 
\end{ttbox} 

1082 

1083 
\begin{ttdescription} 

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

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

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

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

1088 
described below. 

1089 
\end{ttdescription} 

1090 

1091 
Simplification procedures are applied in a twostage process as 

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

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

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

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

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

1097 
\texttt{Some~$thm$}. 

1098 

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

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

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

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

1103 
automatic preprocessing of objectlevel equivalences. 

1104 

1105 
\medskip 

1106 

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

1108 
consider etaexpansion of pair abstraction (see also 

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

1110 
model checker syntax). 

1111 

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

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

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

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

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

1117 
is: 

1118 
\begin{ttbox} 

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

1120 
\end{ttbox} 

1121 
Unfortunately, term rewriting using this rule directly would not 

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

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

1124 
making it rewrite only actual abstractions. The simplification 

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

1126 
\begin{ttbox} 

1127 
local 

1128 
val lhss = 

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

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

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

1133 
 proc _ _ _ = None; 

1134 
in 

4560  1135 
val pair_eta_expand_proc = mk_simproc "pair_eta_expand" lhss proc; 
4395  1136 
end; 
1137 
\end{ttbox} 

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

1139 
\begin{ttbox} 

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

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

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

1143 
\end{ttbox} 

1144 

1145 
\medskip 

1146 

1147 
In the above example the simplification procedure just did fine 

1148 
grained control over rule application, beyond higherorder pattern 

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

1150 
prove particular theorems depending on the current redex. 

1151 

1152 

323  1153 
\section{*Setting up the simplifier}\label{sec:settingupsimp} 
1154 
\index{simplification!setting up} 

286  1155 

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

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

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

286  1160 

323  1161 
The simplifier and the case splitting tactic, which reside on separate 
4395  1162 
files, are not part of Pure Isabelle. They must be loaded explicitly 
1163 
by the objectlogic as follows: 

286  1164 
\begin{ttbox} 
4395  1165 
use "$ISABELLE_HOME/src/Provers/simplifier.ML"; 
1166 
use "$ISABELLE_HOME/src/Provers/splitter.ML"; 

286  1167 
\end{ttbox} 
1168 

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

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

1170 
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

1171 
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

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

1176 
\end{ttbox} 

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

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

1184 
work for later variants of Constructive Type Theory that use 

323  1185 
intensional equality~\cite{nordstrom90}. 
286  1186 

1187 

1188 
\subsection{A collection of standard rewrite rules} 

4557  1189 

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

1191 
connectives. These include cancellation and associative laws. We 

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

1193 
prover for intuitionistic \FOL: 

286  1194 
\begin{ttbox} 
1195 
fun int_prove_fun s = 

1196 
(writeln s; 

1197 
prove_goal IFOL.thy s 

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

4395  1199 
(IntPr.fast_tac 1) ])); 
286  1200 
\end{ttbox} 
1201 
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

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

4395  1205 
val conj_simps = map int_prove_fun 
286  1206 
["P & True <> P", "True & P <> P", 
1207 
"P & False <> False", "False & P <> False", 

1208 
"P & P <> P", 

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

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

1211 
\end{ttbox} 

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

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

323  1214 
are merely bound to an \ML{} identifier, for user reference. 
286  1215 
\begin{ttbox} 
4395  1216 
val distrib_simps = map int_prove_fun 
286  1217 
["P & (Q  R) <> P&Q  P&R", 
1218 
"(Q  R) & P <> Q&P  R&P", 

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

1220 
\end{ttbox} 

1221 

1222 

1223 
\subsection{Functions for preprocessing the rewrite rules} 

323  1224 
\label{sec:setmksimps} 
4395  1225 
\begin{ttbox}\indexbold{*setmksimps} 
1226 
setmksimps : simpset * (thm > thm list) > simpset \hfill{\bf infix 4} 

1227 
\end{ttbox} 

286  1228 
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

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

1232 
objectlevel, then reflecting them to the metalevel. 

1233 

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

1234 
To start, the function \texttt{gen_all} strips any metalevel 
286  1235 
quantifiers from the front of the given theorem. Usually there are none 
1236 
anyway. 

1237 
\begin{ttbox} 

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

1239 
\end{ttbox} 

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

1240 
The function \texttt{atomize} analyses a theorem in order to extract 
286  1241 
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

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

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

1246 
atomize(th RS conjunct2) 

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

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

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

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

1251 
 _ => [th]; 

1252 
\end{ttbox} 

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

1254 
\begin{itemize} 

1255 
\item Conjunction: extract rewrites from both conjuncts. 

1256 

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

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

1259 
condition~$P$. 

1260 

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

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

1263 

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

1264 
\item \texttt{True} and \texttt{False} contain no useful rewrites. 
286  1265 

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

1267 
\end{itemize} 

1268 
The resulting theorems are not literally atomic  they could be 

323  1269 
disjunctive, for example  but are broken down as much as possible. See 
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1270 
the file \texttt{ZF/simpdata.ML} for a sophisticated translation of 
286  1271 
settheoretic formulae into rewrite rules. 
104  1272 

286  1273 
The simplified rewrites must now be converted into metaequalities. The 
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1274 
rule \texttt{eq_reflection} converts equality rewrites, while {\tt 
286  1275 
iff_reflection} converts ifandonlyif rewrites. The latter possibility 
1276 
can arise in two other ways: the negative theorem~$\neg P$ is converted to 

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

1277 
$P\equiv\texttt{False}$, and any other theorem~$P$ is converted to 
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1278 
$P\equiv\texttt{True}$. The rules \texttt{iff_reflection_F} and {\tt 
286  1279 
iff_reflection_T} accomplish this conversion. 
1280 
\begin{ttbox} 

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

1282 
val iff_reflection_F = P_iff_F RS iff_reflection; 

1283 
\ttbreak 

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

1285 
val iff_reflection_T = P_iff_T RS iff_reflection; 

1286 
\end{ttbox} 

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

1287 
The function \texttt{mk_meta_eq} converts a theorem to a metaequality 
286  1288 
using the case analysis described above. 
1289 
\begin{ttbox} 

1290 
fun mk_meta_eq th = case concl_of th of 

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

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

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

1294 
 _ => th RS iff_reflection_T; 

1295 
\end{ttbox} 

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

1296 
The three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_meta_eq} will 
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1297 
be composed together and supplied below to \texttt{setmksimps}. 
286  1298 

1299 

1300 
\subsection{Making the initial simpset} 

4395  1301 

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

1302 
It is time to assemble these items. We open module \texttt{Simplifier} 
4395  1303 
to gain direct access to its components. We define the infix operator 
1304 
\ttindex{addcongs} to insert congruence rules; given a list of 

1305 
theorems, it converts their conclusions into metaequalities and 

1306 
passes them to \ttindex{addeqcongs}. 

286  1307 
\begin{ttbox} 
1308 
open Simplifier; 

1309 
\ttbreak 

4395  1310 
infix 4 addcongs; 
286  1311 
fun ss addcongs congs = 
1312 
ss addeqcongs (congs RL [eq_reflection,iff_reflection]); 

1313 
\end{ttbox} 

4395  1314 
Furthermore, we define the infix operator \ttindex{addsplits} 
1315 
providing a convenient interface for adding split tactics. 

286  1316 
\begin{ttbox} 
4395  1317 
infix 4 addsplits; 
1318 
fun ss addsplits splits = ss addloop (split_tac splits); 

1319 
\end{ttbox} 

1320 

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

1321 
The list \texttt{IFOL_simps} contains the default rewrite rules for 
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1322 
intuitionistic firstorder logic. The first of these is the reflexive law 
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1323 
expressed as the equivalence $(a=a)\bimp\texttt{True}$; the rewrite rule $a=a$ is 
4395  1324 
clearly useless. 
1325 
\begin{ttbox} 

1326 
val IFOL_simps = 

1327 
[refl RS P_iff_T] \at conj_simps \at disj_simps \at not_simps \at 

1328 
imp_simps \at iff_simps \at quant_simps; 

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

1330 
The list \texttt{triv_rls} contains trivial theorems for the solver. Any 
286  1331 
subgoal that is simplified to one of these will be removed. 
1332 
\begin{ttbox} 

1333 
val notFalseI = int_prove_fun "~False"; 

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

1335 
\end{ttbox} 

323  1336 
% 
4395  1337 
The basic simpset for intuitionistic \FOL{} is 
1338 
\ttindexbold{FOL_basic_ss}. It preprocess rewrites using {\tt 

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

1339 
gen_all}, \texttt{atomize} and \texttt{mk_meta_eq}. It solves simplified 
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset

1340 
subgoals using \texttt{triv_rls} and assumptions, and by detecting 
4395  1341 
contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals of 
1342 
conditional rewrites. 

1343 

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

1344 
Other simpsets built from \texttt{FOL_basic_ss} will inherit these items. 
4395  1345 
In particular, \ttindexbold{IFOL_ss}, which introduces {\tt 
1346 
IFOL_simps} as rewrite rules. \ttindexbold{FOL_ss} will later 

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

1347 
extend \texttt{IFOL_ss} with classical rewrite rules such as $\neg\neg 