author  wenzelm 
Fri, 16 Jul 1999 22:24:42 +0200  
changeset 7024  44bd3c094fd6 
parent 6569  66c941ea1f01 
child 7620  8d721c3f4acb 
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} 

5776  693 
Users would usually prefer the following shortcut using \texttt{addsplits}: 
5549  694 
\begin{ttbox} 
695 
by (simp_tac (simpset() addsplits [split_if]) 1); 

696 
\end{ttbox} 

104  697 

698 

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

701 
\begin{ttbox} 

702 
simp_tac : simpset > int > tactic 

703 
asm_simp_tac : simpset > int > tactic 

704 
full_simp_tac : simpset > int > tactic 

705 
asm_full_simp_tac : simpset > int > tactic 

706 
safe_asm_full_simp_tac : simpset > int > tactic 

707 
\end{ttbox} 

2567  708 

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

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

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

713 
recursively before the rewrite rule is applied. 

104  714 

4395  715 
\begin{ttdescription} 
716 

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

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

719 
the basic simplification tactics that work exactly like their 

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

721 
explicitly supplied with a simpset. 

722 

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

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

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

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

727 
classical reasoner. It is rarely used directly. 

728 

729 
\end{ttdescription} 

104  730 

4395  731 
\medskip 
104  732 

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

735 
than their capitalized counterparts. For example 

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

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

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

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

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

745 

4395  746 
\medskip 
747 

748 
Also note that functions depending implicitly on the current theory 

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

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

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

752 
definition packages or special tactics should refer to simpsets only 

753 
explicitly, via the above tactics used in conjunction with 

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

755 

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

756 

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

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

762 
full_simplify : simpset > thm > thm 

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

765 
Simplifier.asm_rewrite : simpset > cterm > thm 

766 
Simplifier.full_rewrite : simpset > cterm > thm 

767 
Simplifier.asm_full_rewrite : simpset > cterm > thm 

4395  768 
\end{ttbox} 
769 

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

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

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

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

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

776 

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

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

779 
argument. 

4395  780 

781 
\begin{warn} 

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

784 
internal interface to the simplifier for special utilities. 

4395  785 
\end{warn} 
786 

787 

788 
\section{Examples of using the simplifier} 

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

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

794 
\item[add_0] 

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

796 
\item[add_Suc] 

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

798 
\item[induct] 

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

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

801 
\end{ttdescription} 

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

808 
\subsection{A trivial example} 

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

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

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

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

818 
base case and inductive step as two subgoals: 

819 
\begin{ttbox} 

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

822 
{\out m + 0 = m} 

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

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

825 
\end{ttbox} 

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

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

832 
\end{ttbox} 

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

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

839 
{\out No subgoals!} 

840 
\end{ttbox} 

841 

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

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

846 
that addition is commutative. 

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

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

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

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

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

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

861 
\end{ttbox} 

862 
Simplification solves the first subgoal, this time rewriting two 

863 
occurrences of~0: 

864 
\begin{ttbox} 

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

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

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

872 
subgoal: 

873 
\begin{ttbox} 

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

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

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

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

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

902 
{\out No subgoals!} 

903 
\end{ttbox} 

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

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

910 
{\out No subgoals!} 

911 
\end{ttbox} 

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

4557  914 

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

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

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

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

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

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

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

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

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

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

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

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

936 
\end{ttbox} 

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

938 
\begin{ttbox} 

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

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

943 
\end{ttbox} 

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

950 
{\out No subgoals!} 

951 
\end{ttbox} 

952 

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

955 
\index{assumptions!reordering} 

956 

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

959 
to be more effective. Given the subgoal 

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

964 
\begin{ttbox} 

965 
by (rotate_tac ~2 1); 

966 
\end{ttbox} 

967 
to obtain 

968 
\begin{ttbox} 

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

973 
\verb$Q(f a)$. 

1213  974 

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

976 
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

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

982 
\begin{ttbox} 

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

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

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

4395  990 
\end{warn} 
991 

286  992 

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

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

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

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

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

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

1001 

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

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

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

1006 
cases, but can be changed for special applications. 

1007 

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

1010 
\end{ttbox} 

4395  1011 
\begin{ttdescription} 
1012 

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

1014 
term order in simpset $ss$. 

1015 

1016 
\end{ttdescription} 

1017 

1018 
\medskip 

323  1019 

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

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

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

1024 
employs ordered rewriting. 

1025 

1026 
Permutative rewrite rules are added to simpsets just like other 

1027 
rewrite rules; the simplifier recognizes their special status 

1028 
automatically. They are most effective in the case of 

1029 
associativecommutative operators. (Associativity by itself is not 

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

1031 
following points in mind: 

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

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

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

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

1037 
standard term order. 

323  1038 

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

1040 
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

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

1044 
lexicographically: 

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

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

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

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

1049 
such as boolean rings. 

1050 

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

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

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

1055 
associated simpset contains many arithmetic laws including 

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

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

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

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

1061 
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

1062 
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

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

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

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

323  1070 
end 
1071 
\end{ttbox} 

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

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

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

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

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

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

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

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

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

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

1106 
{\out Suc n * Suc n} 

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

1109 
\begin{ttbox} 

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

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

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

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

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

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

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

1125 
arithmetic theorems without ordered rewriting requires explicit use of 

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

1127 

1128 
Ordered rewriting is equally successful in proving 

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

1130 

1131 

1132 
\subsection{Reorienting equalities} 

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

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

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

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

1140 
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

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

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

1146 
conclusion by~$f(a)$. 

1147 

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

1149 
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

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

1153 

1154 
\index{rewrite rules!permutative)} 

1155 

1156 

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

1159 
mk_simproc: string > cterm list > 

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

1161 
\end{ttbox} 

1162 

1163 
\begin{ttdescription} 

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

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

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

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

1168 
described below. 

1169 
\end{ttdescription} 

1170 

1171 
Simplification procedures are applied in a twostage process as 

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

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

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

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

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

1177 
\texttt{Some~$thm$}. 

1178 

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

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

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

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

1183 
automatic preprocessing of objectlevel equivalences. 

1184 

1185 
\medskip 

1186 

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

1188 
consider etaexpansion of pair abstraction (see also 

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

1190 
model checker syntax). 

1191 

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

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

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

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

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

1197 
is: 

1198 
\begin{ttbox} 

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

1200 
\end{ttbox} 

1201 
Unfortunately, term rewriting using this rule directly would not 

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

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

1204 
making it rewrite only actual abstractions. The simplification 

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

1206 
\begin{ttbox} 

1207 
local 

1208 
val lhss = 

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

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

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

1213 
 proc _ _ _ = None; 

1214 
in 

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

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

1219 
\begin{ttbox} 

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

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

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

1223 
\end{ttbox} 

1224 

1225 
\medskip 

1226 

1227 
In the above example the simplification procedure just did fine 

1228 
grained control over rule application, beyond higherorder pattern 

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

1230 
prove particular theorems depending on the current redex. 

1231 

1232 

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

286  1235 

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

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

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

286  1240 

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

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

1244 
\texttt{\$ISABELLE_HOME}): 

286  1245 
\begin{ttbox} 
6569  1246 
use "\~\relax\~\relax/src/Provers/simplifier.ML"; 
1247 
use "\~\relax\~\relax/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 

