author  paulson 
Wed, 07 Oct 1998 10:31:30 +0200  
changeset 5619  76a8c72e3fd4 
parent 5575  9ea449586464 
child 5776  3bcc29d0c783 
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$, 

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

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

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

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

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

65 
bookkeeping like modifications of the simpset. 

66 
\end{ttdescription} 

67 

68 
\medskip 

69 

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

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

72 
of \texttt{Simp_tac} as follows: 

73 
\begin{ttbox} 

74 
context Arith.thy; 

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

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

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

80 
{\out No subgoals!} 

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

81 
\end{ttbox} 
4395  82 

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

84 
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

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

86 

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

89 
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

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

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

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

94 

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

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

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

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

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

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

104 
terminate. Isabelle notices certain simple forms of nontermination, 

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

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

107 

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

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

111 
For example, given the subgoal 

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

112 
\begin{ttbox} 
4889  113 
{\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

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

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

118 
will not suffer from this deficiency. 

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

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

120 

4395  121 
\medskip 
122 

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

126 
enormous, especially since invocations of the simplifier are often 

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

128 

129 

130 
\subsection{Modifying the current simpset} 

131 
\begin{ttbox} 

132 
Addsimps : thm list > unit 

133 
Delsimps : thm list > unit 

134 
Addsimprocs : simproc list > unit 

135 
Delsimprocs : simproc list > unit 

136 
Addcongs : thm list > unit 

137 
Delcongs : thm list > unit 

5549  138 
Addsplits : thm list > unit 
139 
Delsplits : thm list > unit 

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

141 

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

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

145 
(conditional) metaequalities. This form is derived automatically 

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

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

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

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

150 
\S\ref{sec:simpcongs}. 

151 

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

152 
\begin{ttdescription} 
4395  153 

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

155 
$thms$ to the current simpset. 

156 

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

158 
from $thms$ from the current simpset. 

159 

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

161 
procedures $procs$ to the current simpset. 

162 

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

164 
procedures $procs$ from the current simpset. 

165 

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

167 
current simpset. 

168 

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

171 

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

173 
current simpset. 

174 

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

4395  176 
current simpset. 
177 

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

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

179 

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

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

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

184 
Ordinary definitions are not added automatically! 

185 

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

187 
explicitly adding or deleting theorems and simplification procedures. 

188 

189 
\medskip 

190 

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

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

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

195 
afterwards. Conversely, sometimes a rule needs 

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

197 
frequent additions or deletions may indicate a badly designed 

198 
simpset. 

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

199 

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

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

203 
deleted simplification rules because they are no longer wanted, 

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

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

207 
\end{warn} 
104  208 

209 

286  210 
\section{Simplification sets}\index{simplification sets} 
4395  211 

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

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

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

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

216 
sensible defaults so that most simplifier calls specify only rewrite 

217 
rules or simplification procedures. Experienced users can exploit the 

218 
other components to streamline proofs in more sophisticated manners. 

219 

220 
\subsection{Inspecting simpsets} 

221 
\begin{ttbox} 

222 
print_ss : simpset > unit 

4889  223 
rep_ss : simpset > \{mss : meta_simpset, 
4664  224 
subgoal_tac: simpset > int > tactic, 
225 
loop_tac : int > tactic, 

226 
finish_tac : thm list > int > tactic, 

4889  227 
unsafe_finish_tac : thm list > int > tactic\} 
4395  228 
\end{ttbox} 
229 
\begin{ttdescription} 

230 

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

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

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

234 
simplification procedures and the patterns they are invoked on are 

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

236 
nonprintable. 

237 

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

240 
and unsafe solvers. 

241 

4395  242 
\end{ttdescription} 
243 

323  244 

4395  245 
\subsection{Building simpsets} 
246 
\begin{ttbox} 

247 
empty_ss : simpset 

248 
merge_ss : simpset * simpset > simpset 

249 
\end{ttbox} 

250 
\begin{ttdescription} 

251 

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

253 
useful under normal circumstances because it doesn't contain 

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

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

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

257 
called \ttindexbold{HOL_basic_ss}. 

258 

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

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

261 
simplification procedures and congruences. The other components 

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

264 
on that.}. 

4395  265 

266 
\end{ttdescription} 

267 

268 

269 
\subsection{Accessing the current simpset} 

5575  270 
\label{sec:accesscurrentsimpset} 
4395  271 

272 
\begin{ttbox} 

5575  273 
simpset : unit > simpset 
274 
simpset_ref : unit > simpset ref 

4395  275 
simpset_of : theory > simpset 
276 
simpset_ref_of : theory > simpset ref 

277 
print_simpset : theory > unit 

5575  278 
SIMPSET :(simpset > tactic) > tactic 
279 
SIMPSET' :(simpset > 'a > tactic) > 'a > tactic 

4395  280 
\end{ttbox} 
281 

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

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

284 
modified as follows. 

285 

286 
\begin{ttdescription} 

287 

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

289 
current theory context. 

290 

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

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

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

294 

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

296 
from theory $thy$. 

297 

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

299 
reference variable from theory $thy$. 

300 

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

303 

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

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

307 
applied on. 

308 

4395  309 
\end{ttdescription} 
310 

5574  311 
\begin{warn} 
312 
There is a subtle difference between \texttt{(SIMPSET'~$tacf$)} and 

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

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

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

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

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

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

319 
\end{warn} 

320 

104  321 

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

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

326 
\end{ttbox} 

327 

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

329 
form of equality, for example: 

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

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

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

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

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

340 
function for extracting equalities from arbitrary theorems. For 

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

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

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

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

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

104  346 

4395  347 
\begin{ttdescription} 
348 

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

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

351 

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

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

354 

355 
\end{ttdescription} 

104  356 

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

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

361 

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

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

364 
\indexbold{higherorder pattern}\indexbold{pattern, higherorder} 

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

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

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

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

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

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

371 

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

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

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

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

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

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

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

379 
acceptable as a conditional rewrite rule since conditions can be 

380 
arbitrary terms. 

381 

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

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

384 
though. 

104  385 
\end{warn} 
332  386 
\index{rewrite rules)} 
387 

4395  388 

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

392 
delsimprocs : simpset * simproc list > simpset 

393 
\end{ttbox} 

394 

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

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

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

400 
operation, the simplifier may offer a simplification procedure the 

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

402 
specifically fashioned for particular situations, resulting in a more 

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

404 

405 

406 
\begin{ttdescription} 

407 

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

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

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

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

414 
\end{ttdescription} 

415 

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

418 
several relations of sums over natural numbers. 

419 

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

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

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

423 
\begin{ttbox} 

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

425 
by (Simp_tac 1); 

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

427 
\end{ttbox} 

428 

4395  429 

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

431 
\begin{ttbox} 

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

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

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

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

436 
\end{ttbox} 

437 

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

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

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

446 
\] 

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

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

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

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

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

452 

4395  453 
\begin{ttdescription} 
454 

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

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

457 
depending on the underlying objectlogic. 

458 

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

460 
derived from $thms$. 

461 

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

463 
their internal form (conclusions using metaequality) to simpset 

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

465 
on. It should be rarely used directly. 

466 

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

468 
in internal form from simpset $ss$. 

469 

470 
\end{ttdescription} 

471 

472 
\medskip 

473 

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

475 
quantifiers also supplies contextual information, this time about the 

476 
bound variable: 

286  477 
\begin{eqnarray*} 
478 
&&\List{\Var{A}=\Var{B};\; 

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

480 
&&\qquad\qquad 

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

482 
\end{eqnarray*} 

323  483 
The congruence rule for conditional expressions can supply contextual 
484 
information for simplifying the arms: 

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

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

488 
\] 

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

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

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

493 
\] 

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

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

496 
to prove the goal. 

497 

498 

4395  499 
\subsection{*The subgoaler}\label{sec:simpsubgoaler} 
500 
\begin{ttbox} 

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

502 
prems_of_ss : simpset > thm list 

503 
\end{ttbox} 

504 

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

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

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

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

104  511 

4395  512 
\begin{ttdescription} 
513 

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

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

516 
simplifier context expressed as a simpset. 

517 

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

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

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

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

522 

523 
\end{ttdescription} 

524 

525 
As an example, consider the following subgoaler: 

104  526 
\begin{ttbox} 
4395  527 
fun subgoaler ss = 
528 
assume_tac ORELSE' 

529 
resolve_tac (prems_of_ss ss) ORELSE' 

530 
asm_simp_tac ss; 

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

534 
if that fails. 

535 

104  536 

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

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

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

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

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

543 
\end{ttbox} 

544 

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

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

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

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

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

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

554 
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

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

559 

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

565 
conditional rules or congruences. 

566 

567 
\begin{ttdescription} 

568 

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

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

571 

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

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

574 
which had already been present in $ss$. 

575 

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

577 
unsafe solver of $ss$. 

578 

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

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

581 
had already been present in $ss$. 

323  582 

4395  583 
\end{ttdescription} 
584 

585 
\medskip 

104  586 

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

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

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

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

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

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

594 
passed. 

595 

596 
\medskip 

597 

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

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

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

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

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

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

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

605 
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

606 
tactics like \texttt{blast_tac}. 
323  607 

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

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

611 
with the theorem $\neg False$. 

104  612 

4395  613 
\medskip 
614 

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

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

620 
the subgoaler or solver, is faulty. 

104  621 
\end{warn} 
622 

323  623 

4395  624 
\subsection{*The looper}\label{sec:simplooper} 
625 
\begin{ttbox} 

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

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

4395  629 
addsplits : simpset * thm list > simpset \hfill{\bf infix 4} 
5549  630 
delsplits : simpset * thm list > simpset \hfill{\bf infix 4} 
4395  631 
\end{ttbox} 
632 

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

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

637 
reverse order. 

638 

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

640 
Another possibility is to apply an elimination rule on the 

641 
assumptions. More adventurous loopers could start an induction. 

642 

643 
\begin{ttdescription} 

644 

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

4395  647 

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

650 
that had already been present in $ss$. 

651 

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

653 
from $ss$. 

4395  654 

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

5549  656 
split tactics for $thms$ as additional looper tactics of $ss$. 
657 

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

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

4395  660 

661 
\end{ttdescription} 

662 

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

665 
for conditional expressions: 

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

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

668 
\] 

669 
Another example is the elimination operator (which happens to be 

670 
called~$split$) for Cartesian products: 

671 
\[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} = 

672 
\langle a,b\rangle \imp \Var{P}(\Var{f}(a,b))) 

673 
\] 

674 

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

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

677 
\texttt{split_tac} with rules like \texttt{split_if}, 

678 
which does not split the subgoal, while the latter is done by 

679 
\texttt{split_asm_tac} with rules like \texttt{split_if_asm}, 

680 
which splits the subgoal. 

681 
The operator \texttt{addsplits} automatically takes care of which tactic to 

682 
call, analyzing the form of the rules given as argument. 

683 
\begin{warn} 

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

685 
\end{warn} 

686 

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

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

689 
is the first rule above: 

690 
\begin{ttbox} 

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

692 
\end{ttbox} 

693 
Users would usually prefer the following shortcut using 

694 
\ttindex{addsplits}: 

695 
\begin{ttbox} 

696 
by (simp_tac (simpset() addsplits [split_if]) 1); 

697 
\end{ttbox} 

104  698 

699 

4395  700 
\section{The simplification tactics}\label{simptactics} 
701 
\index{simplification!tactics}\index{tactics!simplification} 

702 
\begin{ttbox} 

703 
simp_tac : simpset > int > tactic 

704 
asm_simp_tac : simpset > int > tactic 

705 
full_simp_tac : simpset > int > tactic 

706 
asm_full_simp_tac : simpset > int > tactic 

707 
safe_asm_full_simp_tac : simpset > int > tactic 

708 
\end{ttbox} 

2567  709 

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

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

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

714 
recursively before the rewrite rule is applied. 

104  715 

4395  716 
\begin{ttdescription} 
717 

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

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

720 
the basic simplification tactics that work exactly like their 

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

722 
explicitly supplied with a simpset. 

723 

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

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

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

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

728 
classical reasoner. It is rarely used directly. 

729 

730 
\end{ttdescription} 

104  731 

4395  732 
\medskip 
104  733 

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

736 
than their capitalized counterparts. For example 

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

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

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

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

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

746 

4395  747 
\medskip 
748 

749 
Also note that functions depending implicitly on the current theory 

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

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

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

753 
definition packages or special tactics should refer to simpsets only 

754 
explicitly, via the above tactics used in conjunction with 

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

756 

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

757 

5370  758 
\section{Forward rules and conversions} 
759 
\index{simplification!forward rules}\index{simplification!conversions} 

760 
\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  761 
simplify : simpset > thm > thm 
762 
asm_simplify : simpset > thm > thm 

763 
full_simplify : simpset > thm > thm 

5370  764 
asm_full_simplify : simpset > thm > thm\medskip 
765 
Simplifier.rewrite : simpset > cterm > thm 

766 
Simplifier.asm_rewrite : simpset > cterm > thm 

767 
Simplifier.full_rewrite : simpset > cterm > thm 

768 
Simplifier.asm_full_rewrite : simpset > cterm > thm 

4395  769 
\end{ttbox} 
770 

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

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

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

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

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

777 

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

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

780 
argument. 

4395  781 

782 
\begin{warn} 

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

785 
internal interface to the simplifier for special utilities. 

4395  786 
\end{warn} 
787 

788 

789 
\section{Examples of using the simplifier} 

3112  790 
\index{examples!of simplification} Assume we are working within {\tt 
5205  791 
FOL} (see the file \texttt{FOL/ex/Nat}) and that 
323  792 
\begin{ttdescription} 
793 
\item[Nat.thy] 

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

795 
\item[add_0] 

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

797 
\item[add_Suc] 

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

799 
\item[induct] 

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

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

802 
\end{ttdescription} 

4395  803 
We augment the implicit simpset inherited from \texttt{Nat} with the 
4557  804 
basic rewrite rules for addition of natural numbers: 
104  805 
\begin{ttbox} 
3112  806 
Addsimps [add_0, add_Suc]; 
104  807 
\end{ttbox} 
323  808 

809 
\subsection{A trivial example} 

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

104  812 
\begin{ttbox} 
5205  813 
Goal "m+0 = m"; 
104  814 
{\out Level 0} 
815 
{\out m + 0 = m} 

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

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

819 
base case and inductive step as two subgoals: 

820 
\begin{ttbox} 

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

823 
{\out m + 0 = m} 

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

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

826 
\end{ttbox} 

286  827 
Simplification solves the first subgoal trivially: 
104  828 
\begin{ttbox} 
3112  829 
by (Simp_tac 1); 
104  830 
{\out Level 2} 
831 
{\out m + 0 = m} 

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

833 
\end{ttbox} 

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

3112  837 
by (Asm_simp_tac 1); 
104  838 
{\out Level 3} 
839 
{\out m + 0 = m} 

840 
{\out No subgoals!} 

841 
\end{ttbox} 

842 

323  843 
\subsection{An example of tracing} 
3108  844 
\index{tracing!of simplification(}\index{*trace_simp} 
4557  845 

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

847 
that addition is commutative. 

104  848 
\begin{ttbox} 
5205  849 
Goal "m+Suc(n) = Suc(m+n)"; 
104  850 
{\out Level 0} 
851 
{\out m + Suc(n) = Suc(m + n)} 

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

286  853 
\end{ttbox} 
4557  854 
Performing induction on~$m$ yields two subgoals: 
286  855 
\begin{ttbox} 
104  856 
by (res_inst_tac [("n","m")] induct 1); 
857 
{\out Level 1} 

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

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

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

862 
\end{ttbox} 

863 
Simplification solves the first subgoal, this time rewriting two 

864 
occurrences of~0: 

865 
\begin{ttbox} 

3112  866 
by (Simp_tac 1); 
104  867 
{\out Level 2} 
868 
{\out m + Suc(n) = Suc(m + n)} 

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

104  871 
\end{ttbox} 
872 
Switching tracing on illustrates how the simplifier solves the remaining 

873 
subgoal: 

874 
\begin{ttbox} 

4395  875 
set trace_simp; 
3112  876 
by (Asm_simp_tac 1); 
323  877 
\ttbreak 
3112  878 
{\out Adding rewrite rule:} 
5370  879 
{\out .x + Suc n == Suc (.x + n)} 
323  880 
\ttbreak 
5370  881 
{\out Applying instance of rewrite rule:} 
882 
{\out ?m + Suc ?n == Suc (?m + ?n)} 

104  883 
{\out Rewriting:} 
5370  884 
{\out Suc .x + Suc n == Suc (Suc .x + n)} 
323  885 
\ttbreak 
5370  886 
{\out Applying instance of rewrite rule:} 
887 
{\out Suc ?m + ?n == Suc (?m + ?n)} 

104  888 
{\out Rewriting:} 
5370  889 
{\out Suc .x + n == Suc (.x + n)} 
323  890 
\ttbreak 
5370  891 
{\out Applying instance of rewrite rule:} 
892 
{\out Suc ?m + ?n == Suc (?m + ?n)} 

104  893 
{\out Rewriting:} 
5370  894 
{\out Suc .x + n == Suc (.x + n)} 
3112  895 
\ttbreak 
5370  896 
{\out Applying instance of rewrite rule:} 
897 
{\out ?x = ?x == True} 

3112  898 
{\out Rewriting:} 
5370  899 
{\out Suc (Suc (.x + n)) = Suc (Suc (.x + n)) == True} 
323  900 
\ttbreak 
104  901 
{\out Level 3} 
902 
{\out m + Suc(n) = Suc(m + n)} 

903 
{\out No subgoals!} 

904 
\end{ttbox} 

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

104  907 
\begin{ttbox} 
3112  908 
by (ALLGOALS Asm_simp_tac); 
104  909 
{\out Level 2} 
910 
{\out m + Suc(n) = Suc(m + n)} 

911 
{\out No subgoals!} 

912 
\end{ttbox} 

3108  913 
\index{tracing!of simplification)} 
104  914 

4557  915 

323  916 
\subsection{Free variables and simplification} 
4557  917 

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

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

104  920 
\begin{ttbox} 
5205  921 
val [prem] = Goal "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)"; 
104  922 
{\out Level 0} 
923 
{\out f(i + j) = i + f(j)} 

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

323  925 
\ttbreak 
286  926 
{\out val prem = "f(Suc(?n)) = Suc(f(?n))} 
927 
{\out [!!n. f(Suc(n)) = Suc(f(n))]" : thm} 

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

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

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

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

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

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

937 
\end{ttbox} 

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

939 
\begin{ttbox} 

3112  940 
by (Simp_tac 1); 
104  941 
{\out Level 2} 
942 
{\out f(i + j) = i + f(j)} 

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

944 
\end{ttbox} 

3112  945 
The remaining subgoal requires rewriting by the premise, so we add it 
4395  946 
to the current simpset: 
104  947 
\begin{ttbox} 
4395  948 
by (asm_simp_tac (simpset() addsimps [prem]) 1); 
104  949 
{\out Level 3} 
950 
{\out f(i + j) = i + f(j)} 

951 
{\out No subgoals!} 

952 
\end{ttbox} 

953 

1213  954 
\subsection{Reordering assumptions} 
955 
\label{sec:reorderingasms} 

956 
\index{assumptions!reordering} 

957 

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

960 
to be more effective. Given the subgoal 

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

965 
\begin{ttbox} 

966 
by (rotate_tac ~2 1); 

967 
\end{ttbox} 

968 
to obtain 

969 
\begin{ttbox} 

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

974 
\verb$Q(f a)$. 

1213  975 

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

977 
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

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

983 
\begin{ttbox} 

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

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

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

4395  991 
\end{warn} 
992 

286  993 

332  994 
\section{Permutative rewrite rules} 
323  995 
\index{rewrite rules!permutative(} 
996 

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

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

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

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

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

1002 

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

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

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

1007 
cases, but can be changed for special applications. 

1008 

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

1011 
\end{ttbox} 

4395  1012 
\begin{ttdescription} 
1013 

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

1015 
term order in simpset $ss$. 

1016 

1017 
\end{ttdescription} 

1018 

1019 
\medskip 

323  1020 

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

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

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

1025 
employs ordered rewriting. 

1026 

1027 
Permutative rewrite rules are added to simpsets just like other 

1028 
rewrite rules; the simplifier recognizes their special status 

1029 
automatically. They are most effective in the case of 

1030 
associativecommutative operators. (Associativity by itself is not 

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

1032 
following points in mind: 

323  1033 
\begin{itemize}\index{associativecommutative operators} 
4395  1034 

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

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

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

1038 
standard term order. 

323  1039 

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

1041 
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

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

1045 
lexicographically: 

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

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

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

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

1050 
such as boolean rings. 

1051 

3108  1052 
\subsection{Example: sums of natural numbers} 
4395  1053 

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

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

1056 
associated simpset contains many arithmetic laws including 

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

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

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

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

1062 
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

1063 
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

1064 
extend \texttt{Arith} as follows: 
323  1065 
\begin{ttbox} 
1066 
NatSum = Arith + 

1387  1067 
consts sum :: [nat=>nat, nat] => nat 
4245  1068 
primrec "sum" nat 
1069 
"sum f 0 = 0" 

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

323  1071 
end 
1072 
\end{ttbox} 

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

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

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

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

5205  1084 
Goal "2 * sum (\%i.i) (Suc n) = n * Suc n"; 
323  1085 
{\out Level 0} 
3108  1086 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
1087 
{\out 1. 2 * sum (\%i. i) (Suc n) = n * Suc n} 

323  1088 
\end{ttbox} 
3108  1089 
Induction should not be applied until the goal is in the simplest 
1090 
form: 

323  1091 
\begin{ttbox} 
4245  1092 
by (Simp_tac 1); 
323  1093 
{\out Level 1} 
3108  1094 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
1095 
{\out 1. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n} 

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

323  1099 
\begin{ttbox} 
4245  1100 
by (induct_tac "n" 1); 
323  1101 
{\out Level 2} 
3108  1102 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
1103 
{\out 1. 0 + (sum (\%i. i) 0 + sum (\%i. i) 0) = 0 * 0} 

323  1104 
\ttbreak 
4245  1105 
{\out 2. !!n. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n} 
1106 
{\out ==> Suc n + (sum (\%i. i) (Suc n) + sum (\%i. i) (Suc n)) =} 

1107 
{\out Suc n * Suc n} 

323  1108 
\end{ttbox} 
1109 
Simplification proves both subgoals immediately:\index{*ALLGOALS} 

1110 
\begin{ttbox} 

4245  1111 
by (ALLGOALS Asm_simp_tac); 
323  1112 
{\out Level 3} 
3108  1113 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
323  1114 
{\out No subgoals!} 
1115 
\end{ttbox} 

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

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

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

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

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

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

1126 
arithmetic theorems without ordered rewriting requires explicit use of 

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

1128 

1129 
Ordered rewriting is equally successful in proving 

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

1131 

1132 

1133 
\subsection{Reorienting equalities} 

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

1134 
Ordered rewriting with the derived rule \texttt{symmetry} can reverse 
4557  1135 
equations: 
323  1136 
\begin{ttbox} 
1137 
val symmetry = prove_goal HOL.thy "(x=y) = (y=x)" 

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

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

1141 
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

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

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

1147 
conclusion by~$f(a)$. 

1148 

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

1150 
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

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

1154 

1155 
\index{rewrite rules!permutative)} 

1156 

1157 

4395  1158 
\section{*Coding simplification procedures} 
1159 
\begin{ttbox} 

1160 
mk_simproc: string > cterm list > 

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

1162 
\end{ttbox} 

1163 

1164 
\begin{ttdescription} 

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

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

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

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

1169 
described below. 

1170 
\end{ttdescription} 

1171 

1172 
Simplification procedures are applied in a twostage process as 

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

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

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

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

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

1178 
\texttt{Some~$thm$}. 

1179 

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

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

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

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

1184 
automatic preprocessing of objectlevel equivalences. 

1185 

1186 
\medskip 

1187 

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

1189 
consider etaexpansion of pair abstraction (see also 

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

1191 
model checker syntax). 

1192 

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

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

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

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

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

1198 
is: 

1199 
\begin{ttbox} 

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

1201 
\end{ttbox} 

1202 
Unfortunately, term rewriting using this rule directly would not 

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

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

1205 
making it rewrite only actual abstractions. The simplification 

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

1207 
\begin{ttbox} 

1208 
local 

1209 
val lhss = 

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

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

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

1214 
 proc _ _ _ = None; 

1215 
in 

4560  1216 
val pair_eta_expand_proc = mk_simproc "pair_eta_expand" lhss proc; 
4395  1217 
end; 
1218 
\end{ttbox} 

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

1220 
\begin{ttbox} 

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

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

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

1224 
\end{ttbox} 

1225 

1226 
\medskip 

1227 

1228 
In the above example the simplification procedure just did fine 

1229 
grained control over rule application, beyond higherorder pattern 

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

1231 
prove particular theorems depending on the current redex. 

1232 

1233 

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

286  1236 

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

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

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

286  1241 

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

286  1245 
\begin{ttbox} 
4395  1246 
use "$ISABELLE_HOME/src/Provers/simplifier.ML"; 
1247 
use "$ISABELLE_HOME/src/Provers/splitter.ML"; 

286  1248 
\end{ttbox} 
1249 

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

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

1251 
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

1252 
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

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

1257 
\end{ttbox} 

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

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

1265 
work for later variants of Constructive Type Theory that use 

323  1266 
intensional equality~\cite{nordstrom90}. 
286  1267 

1268 

1269 
\subsection{A collection of standard rewrite rules} 

4557  1270 

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

1272 
connectives. These include cancellation and associative laws. We 

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

1274 
prover for intuitionistic \FOL: 

286  1275 
\begin{ttbox} 
1276 
fun int_prove_fun s = 

1277 
(writeln s; 

1278 
prove_goal IFOL.thy s 

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

4395  1280 
(IntPr.fast_tac 1) ])); 
286  1281 
\end{ttbox} 
1282 
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

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

4395  1286 
val conj_simps = map int_prove_fun 
286  1287 
["P & True <> P", "True & P <> P", 
1288 
"P & False <> False", "False & P <> False", 

1289 
"P & P <> P", 

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

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

1292 
\end{ttbox} 

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

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

323  1295 
are merely bound to an \ML{} identifier, for user reference. 
286  1296 
\begin{ttbox} 
4395  1297 
val distrib_simps = map int_prove_fun 
286  1298 
["P & (Q  R) <> P&Q  P&R", 
1299 
"(Q  R) & P <> Q&P  R&P", 

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

1301 
\end{ttbox} 

1302 

1303 

1304 
\subsection{Functions for preprocessing the rewrite rules} 

323  1305 
\label{sec:setmksimps} 
4395  1306 
\begin{ttbox}\indexbold{*setmksimps} 
1307 
setmksimps : simpset * (thm > thm list) > simpset \hfill{\bf infix 4} 

1308 
\end{ttbox} 

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

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

1313 
objectlevel, then reflecting them to the metalevel. 

1314 

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

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

1318 
\begin{ttbox} 

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

1320 
\end{ttbox} 

5549  1321 

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

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

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

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

1328 
atomize(th RS conjunct2) 

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

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

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

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

1333 
 _ => [th]; 

1334 
\end{ttbox} 

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

1336 
\begin{itemize} 

1337 
\item Conjunction: extract rewrites from both conjuncts. 

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

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