summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/Ref/simplifier.tex

author | wenzelm |

Sat Jan 12 16:37:58 2002 +0100 (2002-01-12 ago) | |

changeset 12725 | 7ede865e1fe5 |

parent 12717 | 2d6b5e22e05d |

child 13474 | f326c5d97d76 |

permissions | -rw-r--r-- |

renamed forall_elim_vars_safe to gen_all;

1 %% $Id$

2 \chapter{Simplification}

3 \label{chap:simplification}

4 \index{simplification|(}

6 This chapter describes Isabelle's generic simplification package. It performs

7 conditional and unconditional rewriting and uses contextual information

8 (`local assumptions'). It provides several general hooks, which can provide

9 automatic case splits during rewriting, for example. The simplifier is

10 already set up for many of Isabelle's logics: FOL, ZF, HOL, HOLCF.

12 The first section is a quick introduction to the simplifier that

13 should be sufficient to get started. The later sections explain more

14 advanced features.

17 \section{Simplification for dummies}

18 \label{sec:simp-for-dummies}

20 Basic use of the simplifier is particularly easy because each theory

21 is equipped with sensible default information controlling the rewrite

22 process --- namely the implicit {\em current

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

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

25 context.

27 \begin{warn}

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

29 Executing proofs interactively, or loading them from ML files

30 without associated theories may require setting the current theory

31 manually via the \ttindex{context} command.

32 \end{warn}

34 \subsection{Simplification tactics} \label{sec:simp-for-dummies-tacs}

35 \begin{ttbox}

36 Simp_tac : int -> tactic

37 Asm_simp_tac : int -> tactic

38 Full_simp_tac : int -> tactic

39 Asm_full_simp_tac : int -> tactic

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

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

42 \end{ttbox}

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.

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.

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).

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

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}.}

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

64 operations. This includes rewrite steps, but also bookkeeping like

65 modifications of the simpset.

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

67 information about internal operations. This includes any attempted

68 invocation of simplification procedures.

69 \end{ttdescription}

71 \medskip

73 As an example, consider the theory of arithmetic in HOL. The (rather trivial)

74 goal $0 + (x + 0) = x + 0 + 0$ can be solved by a single call of

75 \texttt{Simp_tac} as follows:

76 \begin{ttbox}

77 context Arith.thy;

78 Goal "0 + (x + 0) = x + 0 + 0";

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

80 by (Simp_tac 1);

81 {\out Level 1}

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

83 {\out No subgoals!}

84 \end{ttbox}

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

87 contains suitable theorems like $\Var{n}+0 = \Var{n}$ and $0+\Var{n} =

88 \Var{n}$.

90 \medskip In many cases, assumptions of a subgoal are also needed in

91 the simplification process. For example, \texttt{x = 0 ==> x + x = 0}

92 is solved by \texttt{Asm_simp_tac} as follows:

93 \begin{ttbox}

94 {\out 1. x = 0 ==> x + x = 0}

95 by (Asm_simp_tac 1);

96 \end{ttbox}

98 \medskip \texttt{Asm_full_simp_tac} is the most powerful of this quartet

99 of tactics but may also loop where some of the others terminate. For

100 example,

101 \begin{ttbox}

102 {\out 1. ALL x. f x = g (f (g x)) ==> f 0 = f 0 + 0}

103 \end{ttbox}

104 is solved by \texttt{Simp_tac}, but \texttt{Asm_simp_tac} and {\tt

105 Asm_simp_tac} loop because the rewrite rule $f\,\Var{x} =

106 g\,(f\,(g\,\Var{x}))$ extracted from the assumption does not

107 terminate. Isabelle notices certain simple forms of nontermination,

108 but not this one. Because assumptions may simplify each other, there can be

109 very subtle cases of nontermination.

111 \begin{warn}

112 \verb$Asm_full_simp_tac$ may miss opportunities to simplify an assumption

113 $A@i$ using an assumption $A@j$ in case $A@j$ is to the right of $A@i$.

114 For example, given the subgoal

115 \begin{ttbox}

116 {\out [| \dots f a \dots; P a; ALL x. P x --> f x = g x |] ==> \dots}

117 \end{ttbox}

118 \verb$Asm_full_simp_tac$ will not simplify the \texttt{f a} on the left.

119 This problem can be overcome by reordering assumptions (see

120 {\S}\ref{sec:reordering-asms}). Future versions of \verb$Asm_full_simp_tac$

121 will not suffer from this deficiency.

122 \end{warn}

124 \medskip

126 Using the simplifier effectively may take a bit of experimentation.

127 Set the \verb$trace_simp$\index{tracing!of simplification} flag to get

128 a better idea of what is going on. The resulting output can be

129 enormous, especially since invocations of the simplifier are often

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

133 \subsection{Modifying the current simpset}

134 \begin{ttbox}

135 Addsimps : thm list -> unit

136 Delsimps : thm list -> unit

137 Addsimprocs : simproc list -> unit

138 Delsimprocs : simproc list -> unit

139 Addcongs : thm list -> unit

140 Delcongs : thm list -> unit

141 Addsplits : thm list -> unit

142 Delsplits : thm list -> unit

143 \end{ttbox}

145 Depending on the theory context, the \texttt{Add} and \texttt{Del}

146 functions manipulate basic components of the associated current

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

148 (conditional) meta-equalities. This form is derived automatically

149 from object-level equations that are supplied by the user. Another

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

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

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

153 {\S}\ref{sec:simp-congs}.

155 \begin{ttdescription}

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

158 $thms$ to the current simpset.

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

161 from $thms$ from the current simpset.

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

164 procedures $procs$ to the current simpset.

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

167 procedures $procs$ from the current simpset.

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

170 current simpset.

172 \item[\ttindexbold{Delcongs} $thms$;] deletes congruence rules from the

173 current simpset.

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

176 current simpset.

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

179 current simpset.

181 \end{ttdescription}

183 When a new theory is built, its implicit simpset is initialized by the union

184 of the respective simpsets of its parent theories. In addition, certain

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

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

187 added automatically!

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

190 explicitly adding or deleting theorems and simplification procedures.

192 \medskip

194 Good simpsets are hard to design. Rules that obviously simplify,

195 like $\Var{n}+0 = \Var{n}$, should be added to the current simpset right after

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

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

198 afterwards. Conversely, sometimes a rule needs

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

200 frequent additions or deletions may indicate a badly designed

201 simpset.

203 \begin{warn}

204 The union of the parent simpsets (as described above) is not always

205 a good starting point for the new theory. If some ancestors have

206 deleted simplification rules because they are no longer wanted,

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

208 the unwanted rules. After this union is formed, changes to

209 a parent simpset have no effect on the child simpset.

210 \end{warn}

213 \section{Simplification sets}\index{simplification sets}

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

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

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

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

219 sensible defaults so that most simplifier calls specify only rewrite

220 rules or simplification procedures. Experienced users can exploit the

221 other components to streamline proofs in more sophisticated manners.

223 \subsection{Inspecting simpsets}

224 \begin{ttbox}

225 print_ss : simpset -> unit

226 rep_ss : simpset -> \{mss : meta_simpset,

227 subgoal_tac: simpset -> int -> tactic,

228 loop_tacs : (string * (int -> tactic))list,

229 finish_tac : solver list,

230 unsafe_finish_tac : solver list\}

231 \end{ttbox}

232 \begin{ttdescription}

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

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

236 their internal form expressed as meta-equalities. The names of the

237 simplification procedures and the patterns they are invoked on are

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

239 non-printable.

241 \item[\ttindexbold{rep_ss} $ss$;] decomposes $ss$ as a record of its internal

242 components, namely the meta_simpset, the subgoaler, the loop, and the safe

243 and unsafe solvers.

245 \end{ttdescription}

248 \subsection{Building simpsets}

249 \begin{ttbox}

250 empty_ss : simpset

251 merge_ss : simpset * simpset -> simpset

252 \end{ttbox}

253 \begin{ttdescription}

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

256 under normal circumstances because it doesn't contain suitable tactics

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

258 object-logic, one will typically define a more appropriate ``almost empty''

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

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

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

263 simplification procedures and congruences. The other components

264 (tactics etc.) cannot be merged, though; they are taken from either

265 simpset\footnote{Actually from $ss@1$, but it would unwise to count

266 on that.}.

268 \end{ttdescription}

271 \subsection{Accessing the current simpset}

272 \label{sec:access-current-simpset}

274 \begin{ttbox}

275 simpset : unit -> simpset

276 simpset_ref : unit -> simpset ref

277 simpset_of : theory -> simpset

278 simpset_ref_of : theory -> simpset ref

279 print_simpset : theory -> unit

280 SIMPSET :(simpset -> tactic) -> tactic

281 SIMPSET' :(simpset -> 'a -> tactic) -> 'a -> tactic

282 \end{ttbox}

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

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

286 modified as follows.

288 \begin{ttdescription}

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

291 current theory context.

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

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

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

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

298 from theory $thy$.

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

301 reference variable from theory $thy$.

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

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

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

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

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

309 applied on.

311 \end{ttdescription}

313 \begin{warn}

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

315 \texttt{($tacf\,$(simpset()))}. For example \texttt{(SIMPSET'

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

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

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

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

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

321 \end{warn}

324 \subsection{Rewrite rules}

325 \begin{ttbox}

326 addsimps : simpset * thm list -> simpset \hfill{\bf infix 4}

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

328 \end{ttbox}

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

331 form of equality, for example:

332 \begin{eqnarray*}

333 Suc(\Var{m}) + \Var{n} &=& \Var{m} + Suc(\Var{n}) \\

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

335 \Var{A} \un \Var{B} &\equiv& \{x.x\in \Var{A} \disj x\in \Var{B}\}

336 \end{eqnarray*}

337 Conditional rewrites such as $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} =

338 0$ are also permitted; the conditions can be arbitrary formulas.

340 Internally, all rewrite rules are translated into meta-equalities,

341 theorems with conclusion $lhs \equiv rhs$. Each simpset contains a

342 function for extracting equalities from arbitrary theorems. For

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

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

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

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

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

349 \begin{ttdescription}

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

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

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

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

357 \end{ttdescription}

359 \begin{warn}

360 The simplifier will accept all standard rewrite rules: those where

361 all unknowns are of base type. Hence ${\Var{i}+(\Var{j}+\Var{k})} =

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

364 It will also deal gracefully with all rules whose left-hand sides

365 are so-called {\em higher-order patterns}~\cite{nipkow-patterns}.

366 \indexbold{higher-order pattern}\indexbold{pattern, higher-order}

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

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

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

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

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

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

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

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

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

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

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

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

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

381 acceptable as a conditional rewrite rule since conditions can be

382 arbitrary terms.

384 There is basically no restriction on the form of the right-hand

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

386 though.

387 \end{warn}

388 \index{rewrite rules|)}

391 \subsection{*Simplification procedures}

392 \begin{ttbox}

393 addsimprocs : simpset * simproc list -> simpset

394 delsimprocs : simpset * simproc list -> simpset

395 \end{ttbox}

397 Simplification procedures are {\ML} objects of abstract type

398 \texttt{simproc}. Basically they are just functions that may produce

399 \emph{proven} rewrite rules on demand. They are associated with

400 certain patterns that conceptually represent left-hand sides of

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

402 operation, the simplifier may offer a simplification procedure the

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

404 specifically fashioned for particular situations, resulting in a more

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

408 \begin{ttdescription}

410 \item[$ss$ \ttindexbold{addsimprocs} $procs$] adds the simplification

411 procedures $procs$ to the current simpset.

413 \item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes the simplification

414 procedures $procs$ from the current simpset.

416 \end{ttdescription}

418 For example, simplification procedures \ttindexbold{nat_cancel} of

419 \texttt{HOL/Arith} cancel common summands and constant factors out of

420 several relations of sums over natural numbers.

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

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

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

425 \begin{ttbox}

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

427 by (Simp_tac 1);

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

429 \end{ttbox}

432 \subsection{*Congruence rules}\index{congruence rules}\label{sec:simp-congs}

433 \begin{ttbox}

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

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

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

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

438 \end{ttbox}

440 Congruence rules are meta-equalities of the form

441 \[ \dots \Imp

442 f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}).

443 \]

444 This governs the simplification of the arguments of~$f$. For

445 example, some arguments can be simplified under additional assumptions:

446 \[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}}

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

448 \]

449 Given this rule, the simplifier assumes $Q@1$ and extracts rewrite

450 rules from it when simplifying~$P@2$. Such local assumptions are

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

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

453 {\S}~\ref{sec:simp-solver} below.

455 \begin{ttdescription}

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

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

459 depending on the underlying object-logic.

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

462 derived from $thms$.

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

465 their internal form (conclusions using meta-equality) to simpset

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

467 on. It should be rarely used directly.

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

470 in internal form from simpset $ss$.

472 \end{ttdescription}

474 \medskip

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

477 quantifiers also supplies contextual information, this time about the

478 bound variable:

479 \begin{eqnarray*}

480 &&\List{\Var{A}=\Var{B};\;

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

482 &&\qquad\qquad

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

484 \end{eqnarray*}

485 The congruence rule for conditional expressions can supply contextual

486 information for simplifying the arms:

487 \[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~

488 \neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp

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

490 \]

491 A congruence rule can also {\em prevent\/} simplification of some arguments.

492 Here is an alternative congruence rule for conditional expressions:

493 \[ \Var{p}=\Var{q} \Imp

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

495 \]

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

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

498 to prove the goal.

501 \subsection{*The subgoaler}\label{sec:simp-subgoaler}

502 \begin{ttbox}

503 setsubgoaler :

504 simpset * (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4}

505 prems_of_ss : simpset -> thm list

506 \end{ttbox}

508 The subgoaler is the tactic used to solve subgoals arising out of

509 conditional rewrite rules or congruence rules. The default should be

510 simplification itself. Occasionally this strategy needs to be

511 changed. For example, if the premise of a conditional rule is an

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

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

515 \begin{ttdescription}

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

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

519 simplifier context expressed as a simpset.

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

522 premises from simplifier context $ss$. This may be non-empty only

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

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

526 \end{ttdescription}

528 As an example, consider the following subgoaler:

529 \begin{ttbox}

530 fun subgoaler ss =

531 assume_tac ORELSE'

532 resolve_tac (prems_of_ss ss) ORELSE'

533 asm_simp_tac ss;

534 \end{ttbox}

535 This tactic first tries to solve the subgoal by assumption or by

536 resolving with with one of the premises, calling simplification only

537 if that fails.

540 \subsection{*The solver}\label{sec:simp-solver}

541 \begin{ttbox}

542 mk_solver : string -> (thm list -> int -> tactic) -> solver

543 setSolver : simpset * solver -> simpset \hfill{\bf infix 4}

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

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

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

547 \end{ttbox}

549 A solver is a tactic that attempts to solve a subgoal after

550 simplification. Typically it just proves trivial subgoals such as

551 \texttt{True} and $t=t$. It could use sophisticated means such as {\tt

552 blast_tac}, though that could make simplification expensive.

553 To keep things more abstract, solvers are packaged up in type

554 \texttt{solver}. The only way to create a solver is via \texttt{mk_solver}.

556 Rewriting does not instantiate unknowns. For example, rewriting

557 cannot prove $a\in \Var{A}$ since this requires

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

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

560 simplifier can handle a conditional rewrite rule whose condition

561 contains extra variables. When a simplification tactic is to be

562 combined with other provers, especially with the classical reasoner,

563 it is important whether it can be considered safe or not. For this

564 reason a simpset contains two solvers, a safe and an unsafe one.

566 The standard simplification strategy solely uses the unsafe solver,

567 which is appropriate in most cases. For special applications where

568 the simplification process is not allowed to instantiate unknowns

569 within the goal, simplification starts with the safe solver, but may

570 still apply the ordinary unsafe one in nested simplifications for

571 conditional rules or congruences. Note that in this way the overall

572 tactic is not totally safe: it may instantiate unknowns that appear also

573 in other subgoals.

575 \begin{ttdescription}

576 \item[\ttindexbold{mk_solver} $s$ $tacf$] converts $tacf$ into a new solver;

577 the string $s$ is only attached as a comment and has no other significance.

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

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

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

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

584 which had already been present in $ss$.

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

587 unsafe solver of $ss$.

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

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

591 had already been present in $ss$.

593 \end{ttdescription}

595 \medskip

597 \index{assumptions!in simplification} The solver tactic is invoked

598 with a list of theorems, namely assumptions that hold in the local

599 context. This may be non-empty only if the simplifier has been told

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

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

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

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

604 passed.

606 \medskip

608 As explained in {\S}\ref{sec:simp-subgoaler}, the subgoaler is also used

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

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

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

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

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

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

615 particular, reflexivity should be tried before any of the fancy

616 tactics like \texttt{blast_tac}.

618 It may even happen that due to simplification the subgoal is no longer

619 an equality. For example $False \bimp \Var{Q}$ could be rewritten to

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

621 with the theorem $\neg False$.

623 \medskip

625 \begin{warn}

626 If the simplifier aborts with the message \texttt{Failed congruence

627 proof!}, then the subgoaler or solver has failed to prove a

628 premise of a congruence rule. This should never occur under normal

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

630 the subgoaler or solver, is faulty.

631 \end{warn}

634 \subsection{*The looper}\label{sec:simp-looper}

635 \begin{ttbox}

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

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

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

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

640 delsplits : simpset * thm list -> simpset \hfill{\bf infix 4}

641 \end{ttbox}

643 The looper is a list of tactics that are applied after simplification, in case

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

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

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

647 reverse order.

649 A typical looper is \index{case splitting}: the expansion of a conditional.

650 Another possibility is to apply an elimination rule on the

651 assumptions. More adventurous loopers could start an induction.

653 \begin{ttdescription}

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

656 tactic of $ss$.

658 \item[$ss$ \ttindexbold{addloop} $(name,tacf)$] adds $tacf$ as an additional

659 looper tactic with name $name$; it will be tried after the looper tactics

660 that had already been present in $ss$.

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

663 from $ss$.

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

666 split tactics for $thms$ as additional looper tactics of $ss$.

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

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

671 \end{ttdescription}

673 The splitter replaces applications of a given function; the right-hand side

674 of the replacement can be anything. For example, here is a splitting rule

675 for conditional expressions:

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

677 \conj (\neg\Var{Q} \imp \Var{P}(\Var{y}))

678 \]

679 Another example is the elimination operator for Cartesian products (which

680 happens to be called~$split$):

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

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

683 \]

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

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

687 \texttt{split_tac} with rules like \texttt{split_if} or \texttt{option.split},

688 which do not split the subgoal, while the latter is done by

689 \texttt{split_asm_tac} with rules like \texttt{split_if_asm} or

690 \texttt{option.split_asm}, which split the subgoal.

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

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

693 \begin{warn}

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

695 \end{warn}

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

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

699 is the first rule above:

700 \begin{ttbox}

701 by (simp_tac (simpset()

702 addloop ("split if", split_tac [split_if])) 1);

703 \end{ttbox}

704 Users would usually prefer the following shortcut using \texttt{addsplits}:

705 \begin{ttbox}

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

707 \end{ttbox}

708 Case-splitting on conditional expressions is usually beneficial, so it is

709 enabled by default in the object-logics \texttt{HOL} and \texttt{FOL}.

712 \section{The simplification tactics}\label{simp-tactics}

713 \index{simplification!tactics}\index{tactics!simplification}

714 \begin{ttbox}

715 generic_simp_tac : bool -> bool * bool * bool ->

716 simpset -> int -> tactic

717 simp_tac : simpset -> int -> tactic

718 asm_simp_tac : simpset -> int -> tactic

719 full_simp_tac : simpset -> int -> tactic

720 asm_full_simp_tac : simpset -> int -> tactic

721 safe_asm_full_simp_tac : simpset -> int -> tactic

722 \end{ttbox}

724 \texttt{generic_simp_tac} is the basic tactic that is underlying any actual

725 simplification work. The others are just instantiations of it. The rewriting

726 strategy is always strictly bottom up, except for congruence rules,

727 which are applied while descending into a term. Conditions in conditional

728 rewrite rules are solved recursively before the rewrite rule is applied.

730 \begin{ttdescription}

732 \item[\ttindexbold{generic_simp_tac} $safe$ ($simp\_asm$, $use\_asm$, $mutual$)]

733 gives direct access to the various simplification modes:

734 \begin{itemize}

735 \item if $safe$ is {\tt true}, the safe solver is used as explained in

736 {\S}\ref{sec:simp-solver},

737 \item $simp\_asm$ determines whether the local assumptions are simplified,

738 \item $use\_asm$ determines whether the assumptions are used as local rewrite

739 rules, and

740 \item $mutual$ determines whether assumptions can simplify each other rather

741 than being processed from left to right.

742 \end{itemize}

743 This generic interface is intended

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

745 classical reasoner. It is rarely used directly.

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

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

749 the basic simplification tactics that work exactly like their

750 namesakes in {\S}\ref{sec:simp-for-dummies}, except that they are

751 explicitly supplied with a simpset.

753 \end{ttdescription}

755 \medskip

757 Local modifications of simpsets within a proof are often much cleaner

758 by using above tactics in conjunction with explicit simpsets, rather

759 than their capitalized counterparts. For example

760 \begin{ttbox}

761 Addsimps \(thms\);

762 by (Simp_tac \(i\));

763 Delsimps \(thms\);

764 \end{ttbox}

765 can be expressed more appropriately as

766 \begin{ttbox}

767 by (simp_tac (simpset() addsimps \(thms\)) \(i\));

768 \end{ttbox}

770 \medskip

772 Also note that functions depending implicitly on the current theory

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

774 {\S}\ref{sec:simp-for-dummies}) should be considered harmful outside of

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

776 definition packages or special tactics should refer to simpsets only

777 explicitly, via the above tactics used in conjunction with

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

781 \section{Forward rules and conversions}

782 \index{simplification!forward rules}\index{simplification!conversions}

783 \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}

784 simplify : simpset -> thm -> thm

785 asm_simplify : simpset -> thm -> thm

786 full_simplify : simpset -> thm -> thm

787 asm_full_simplify : simpset -> thm -> thm\medskip

788 Simplifier.rewrite : simpset -> cterm -> thm

789 Simplifier.asm_rewrite : simpset -> cterm -> thm

790 Simplifier.full_rewrite : simpset -> cterm -> thm

791 Simplifier.asm_full_rewrite : simpset -> cterm -> thm

792 \end{ttbox}

794 The first four of these functions provide \emph{forward} rules for

795 simplification. Their effect is analogous to the corresponding

796 tactics described in {\S}\ref{simp-tactics}, but affect the whole

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

798 looper~/ solver process as described in {\S}\ref{sec:simp-looper} and

799 {\S}\ref{sec:simp-solver} is omitted in forward simplification.

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

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

803 argument.

805 \begin{warn}

806 Forward simplification rules and conversions should be used rarely

807 in ordinary proof scripts. The main intention is to provide an

808 internal interface to the simplifier for special utilities.

809 \end{warn}

812 \section{Examples of using the Simplifier}

813 \index{examples!of simplification} Assume we are working within {\tt

814 FOL} (see the file \texttt{FOL/ex/Nat}) and that

815 \begin{ttdescription}

816 \item[Nat.thy]

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

818 \item[add_0]

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

820 \item[add_Suc]

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

822 \item[induct]

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

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

825 \end{ttdescription}

826 We augment the implicit simpset inherited from \texttt{Nat} with the

827 basic rewrite rules for addition of natural numbers:

828 \begin{ttbox}

829 Addsimps [add_0, add_Suc];

830 \end{ttbox}

832 \subsection{A trivial example}

833 Proofs by induction typically involve simplification. Here is a proof

834 that~0 is a right identity:

835 \begin{ttbox}

836 Goal "m+0 = m";

837 {\out Level 0}

838 {\out m + 0 = m}

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

840 \end{ttbox}

841 The first step is to perform induction on the variable~$m$. This returns a

842 base case and inductive step as two subgoals:

843 \begin{ttbox}

844 by (res_inst_tac [("n","m")] induct 1);

845 {\out Level 1}

846 {\out m + 0 = m}

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

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

849 \end{ttbox}

850 Simplification solves the first subgoal trivially:

851 \begin{ttbox}

852 by (Simp_tac 1);

853 {\out Level 2}

854 {\out m + 0 = m}

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

856 \end{ttbox}

857 The remaining subgoal requires \ttindex{Asm_simp_tac} in order to use the

858 induction hypothesis as a rewrite rule:

859 \begin{ttbox}

860 by (Asm_simp_tac 1);

861 {\out Level 3}

862 {\out m + 0 = m}

863 {\out No subgoals!}

864 \end{ttbox}

866 \subsection{An example of tracing}

867 \index{tracing!of simplification|(}\index{*trace_simp}

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

870 that addition is commutative.

871 \begin{ttbox}

872 Goal "m+Suc(n) = Suc(m+n)";

873 {\out Level 0}

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

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

876 \end{ttbox}

877 Performing induction on~$m$ yields two subgoals:

878 \begin{ttbox}

879 by (res_inst_tac [("n","m")] induct 1);

880 {\out Level 1}

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

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

883 {\out 2. !!x. x + Suc(n) = Suc(x + n) ==>}

884 {\out Suc(x) + Suc(n) = Suc(Suc(x) + n)}

885 \end{ttbox}

886 Simplification solves the first subgoal, this time rewriting two

887 occurrences of~0:

888 \begin{ttbox}

889 by (Simp_tac 1);

890 {\out Level 2}

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

892 {\out 1. !!x. x + Suc(n) = Suc(x + n) ==>}

893 {\out Suc(x) + Suc(n) = Suc(Suc(x) + n)}

894 \end{ttbox}

895 Switching tracing on illustrates how the simplifier solves the remaining

896 subgoal:

897 \begin{ttbox}

898 set trace_simp;

899 by (Asm_simp_tac 1);

900 \ttbreak

901 {\out Adding rewrite rule:}

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

903 \ttbreak

904 {\out Applying instance of rewrite rule:}

905 {\out ?m + Suc ?n == Suc (?m + ?n)}

906 {\out Rewriting:}

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

908 \ttbreak

909 {\out Applying instance of rewrite rule:}

910 {\out Suc ?m + ?n == Suc (?m + ?n)}

911 {\out Rewriting:}

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

913 \ttbreak

914 {\out Applying instance of rewrite rule:}

915 {\out Suc ?m + ?n == Suc (?m + ?n)}

916 {\out Rewriting:}

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

918 \ttbreak

919 {\out Applying instance of rewrite rule:}

920 {\out ?x = ?x == True}

921 {\out Rewriting:}

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

923 \ttbreak

924 {\out Level 3}

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

926 {\out No subgoals!}

927 \end{ttbox}

928 Many variations are possible. At Level~1 (in either example) we could have

929 solved both subgoals at once using the tactical \ttindex{ALLGOALS}:

930 \begin{ttbox}

931 by (ALLGOALS Asm_simp_tac);

932 {\out Level 2}

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

934 {\out No subgoals!}

935 \end{ttbox}

936 \index{tracing!of simplification|)}

939 \subsection{Free variables and simplification}

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

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

943 \begin{ttbox}

944 val [prem] = Goal

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

946 {\out Level 0}

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

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

949 \ttbreak

950 {\out val prem = "f(Suc(?n)) = Suc(f(?n))}

951 {\out [!!n. f(Suc(n)) = Suc(f(n))]" : thm}

952 \end{ttbox}

953 In the theorem~\texttt{prem}, note that $f$ is a free variable while

954 $\Var{n}$ is a schematic variable.

955 \begin{ttbox}

956 by (res_inst_tac [("n","i")] induct 1);

957 {\out Level 1}

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

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

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

961 \end{ttbox}

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

963 \begin{ttbox}

964 by (Simp_tac 1);

965 {\out Level 2}

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

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

968 \end{ttbox}

969 The remaining subgoal requires rewriting by the premise, so we add it

970 to the current simpset:

971 \begin{ttbox}

972 by (asm_simp_tac (simpset() addsimps [prem]) 1);

973 {\out Level 3}

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

975 {\out No subgoals!}

976 \end{ttbox}

978 \subsection{Reordering assumptions}

979 \label{sec:reordering-asms}

980 \index{assumptions!reordering}

982 As mentioned in {\S}\ref{sec:simp-for-dummies-tacs},

983 \ttindex{asm_full_simp_tac} may require the assumptions to be permuted

984 to be more effective. Given the subgoal

985 \begin{ttbox}

986 {\out 1. [| ALL x. P x --> f x = g x; Q(f a); P a; R |] ==> S}

987 \end{ttbox}

988 we can rotate the assumptions two positions to the right

989 \begin{ttbox}

990 by (rotate_tac ~2 1);

991 \end{ttbox}

992 to obtain

993 \begin{ttbox}

994 {\out 1. [| P a; R; ALL x. P x --> f x = g x; Q(f a) |] ==> S}

995 \end{ttbox}

996 which enables \verb$asm_full_simp_tac$ to simplify \verb$Q(f a)$ to

997 \verb$Q(g a)$ because now all required assumptions are to the left of

998 \verb$Q(f a)$.

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

1001 out a particular assumption which needs to be rewritten and move it the the

1002 right end of the assumptions. In the above case rotation can be replaced by

1003 \begin{ttbox}

1004 by (dres_inst_tac [("psi","Q(f a)")] asm_rl 1);

1005 \end{ttbox}

1006 which is more directed and leads to

1007 \begin{ttbox}

1008 {\out 1. [| ALL x. P x --> f x = g x; P a; R; Q(f a) |] ==> S}

1009 \end{ttbox}

1011 \begin{warn}

1012 Reordering assumptions usually leads to brittle proofs and should be

1013 avoided. Future versions of \verb$asm_full_simp_tac$ will completely

1014 remove the need for such manipulations.

1015 \end{warn}

1018 \section{Permutative rewrite rules}

1019 \index{rewrite rules!permutative|(}

1021 A rewrite rule is {\bf permutative} if the left-hand side and right-hand

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

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

1024 (x-z)-y$ in arithmetic and $insert(x,insert(y,A)) = insert(y,insert(x,A))$

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

1027 Because ordinary rewriting loops given such rules, the simplifier

1028 employs a special strategy, called {\bf ordered

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

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

1031 cases, but can be changed for special applications.

1033 \begin{ttbox}

1034 settermless : simpset * (term * term -> bool) -> simpset \hfill{\bf infix 4}

1035 \end{ttbox}

1036 \begin{ttdescription}

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

1039 term order in simpset $ss$.

1041 \end{ttdescription}

1043 \medskip

1045 A permutative rewrite rule is applied only if it decreases the given

1046 term with respect to this ordering. For example, commutativity

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

1048 than $b+a$. The Boyer-Moore theorem prover~\cite{bm88book} also

1049 employs ordered rewriting.

1051 Permutative rewrite rules are added to simpsets just like other

1052 rewrite rules; the simplifier recognizes their special status

1053 automatically. They are most effective in the case of

1054 associative-commutative operators. (Associativity by itself is not

1055 permutative.) When dealing with an AC-operator~$f$, keep the

1056 following points in mind:

1057 \begin{itemize}\index{associative-commutative operators}

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

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

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

1062 standard term order.

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

1065 associativity~(A) and commutativity~(C) but also a derived rule, {\bf

1066 left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.

1067 \end{itemize}

1068 Ordered rewriting with the combination of A, C, and~LC sorts a term

1069 lexicographically:

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

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

1072 Martin and Nipkow~\cite{martin-nipkow} discuss the theory and give many

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

1074 such as boolean rings.

1076 \subsection{Example: sums of natural numbers}

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

1079 \thydx{Arith} contains natural numbers arithmetic. Its associated simpset

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

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

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

1083 \[ \sum@{i=1}^n i = n\times(n+1)/2. \]

1084 %

1085 A functional~\texttt{sum} represents the summation operator under the

1086 interpretation $\texttt{sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$. We

1087 extend \texttt{Arith} as follows:

1088 \begin{ttbox}

1089 NatSum = Arith +

1090 consts sum :: [nat=>nat, nat] => nat

1091 primrec

1092 "sum f 0 = 0"

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

1094 end

1095 \end{ttbox}

1096 The \texttt{primrec} declaration automatically adds rewrite rules for

1097 \texttt{sum} to the default simpset. We now remove the

1098 \texttt{nat_cancel} simplification procedures (in order not to spoil

1099 the example) and insert the AC-rules for~$+$:

1100 \begin{ttbox}

1101 Delsimprocs nat_cancel;

1102 Addsimps add_ac;

1103 \end{ttbox}

1104 Our desired theorem now reads $\texttt{sum} \, (\lambda i.i) \, (n+1) =

1105 n\times(n+1)/2$. The Isabelle goal has both sides multiplied by~$2$:

1106 \begin{ttbox}

1107 Goal "2 * sum (\%i.i) (Suc n) = n * Suc n";

1108 {\out Level 0}

1109 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}

1110 {\out 1. 2 * sum (\%i. i) (Suc n) = n * Suc n}

1111 \end{ttbox}

1112 Induction should not be applied until the goal is in the simplest

1113 form:

1114 \begin{ttbox}

1115 by (Simp_tac 1);

1116 {\out Level 1}

1117 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}

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

1119 \end{ttbox}

1120 Ordered rewriting has sorted the terms in the left-hand side. The

1121 subgoal is now ready for induction:

1122 \begin{ttbox}

1123 by (induct_tac "n" 1);

1124 {\out Level 2}

1125 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}

1126 {\out 1. 0 + (sum (\%i. i) 0 + sum (\%i. i) 0) = 0 * 0}

1127 \ttbreak

1128 {\out 2. !!n. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n}

1129 {\out ==> Suc n + (sum (\%i. i) (Suc n) + sum (\%i.\,i) (Suc n)) =}

1130 {\out Suc n * Suc n}

1131 \end{ttbox}

1132 Simplification proves both subgoals immediately:\index{*ALLGOALS}

1133 \begin{ttbox}

1134 by (ALLGOALS Asm_simp_tac);

1135 {\out Level 3}

1136 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}

1137 {\out No subgoals!}

1138 \end{ttbox}

1139 Simplification cannot prove the induction step if we omit \texttt{add_ac} from

1140 the simpset. Observe that like terms have not been collected:

1141 \begin{ttbox}

1142 {\out Level 3}

1143 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}

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

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

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

1147 \end{ttbox}

1148 Ordered rewriting proves this by sorting the left-hand side. Proving

1149 arithmetic theorems without ordered rewriting requires explicit use of

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

1152 Ordered rewriting is equally successful in proving

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

1156 \subsection{Re-orienting equalities}

1157 Ordered rewriting with the derived rule \texttt{symmetry} can reverse

1158 equations:

1159 \begin{ttbox}

1160 val symmetry = prove_goal HOL.thy "(x=y) = (y=x)"

1161 (fn _ => [Blast_tac 1]);

1162 \end{ttbox}

1163 This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs

1164 in the conclusion but not~$s$, can often be brought into the right form.

1165 For example, ordered rewriting with \texttt{symmetry} can prove the goal

1166 \[ f(a)=b \conj f(a)=c \imp b=c. \]

1167 Here \texttt{symmetry} reverses both $f(a)=b$ and $f(a)=c$

1168 because $f(a)$ is lexicographically greater than $b$ and~$c$. These

1169 re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the

1170 conclusion by~$f(a)$.

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

1173 The differing orientations make this appear difficult to prove. Ordered

1174 rewriting with \texttt{symmetry} makes the equalities agree. (Without

1175 knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$

1176 or~$u=t$.) Then the simplifier can prove the goal outright.

1178 \index{rewrite rules!permutative|)}

1181 \section{*Coding simplification procedures}

1182 \begin{ttbox}

1183 mk_simproc: string -> cterm list ->

1184 (Sign.sg -> thm list -> term -> thm option) -> simproc

1185 \end{ttbox}

1187 \begin{ttdescription}

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

1189 simplification procedure for left-hand side patterns $lhss$. The

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

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

1192 described below.

1193 \end{ttdescription}

1195 Simplification procedures are applied in a two-stage process as

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

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

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

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

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

1201 \texttt{Some~$thm$}.

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

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

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

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

1207 automatic preprocessing of object-level equivalences.

1209 \medskip

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

1212 consider eta-expansion of pair abstraction (see also

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

1214 model checker syntax).

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

1217 \texttt{split} together with some concrete syntax supporting

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

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

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

1221 \begin{ttbox}

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

1223 \end{ttbox}

1224 Unfortunately, term rewriting using this rule directly would not

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

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

1227 making it rewrite only actual abstractions. The simplification

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

1229 \begin{ttbox}

1230 local

1231 val lhss =

1232 [read_cterm (sign_of Prod.thy)

1233 ("f::'a*'b=>'c", TVar (("'z", 0), []))];

1234 val rew = mk_meta_eq pair_eta_expand; \medskip

1235 fun proc _ _ (Abs _) = Some rew

1236 | proc _ _ _ = None;

1237 in

1238 val pair_eta_expand_proc = mk_simproc "pair_eta_expand" lhss proc;

1239 end;

1240 \end{ttbox}

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

1242 \begin{ttbox}

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

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

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

1246 \end{ttbox}

1248 \medskip

1250 In the above example the simplification procedure just did fine

1251 grained control over rule application, beyond higher-order pattern

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

1253 prove particular theorems depending on the current redex.

1256 \section{*Setting up the Simplifier}\label{sec:setting-up-simp}

1257 \index{simplification!setting up}

1259 Setting up the simplifier for new logics is complicated in the general case.

1260 This section describes how the simplifier is installed for intuitionistic

1261 first-order logic; the code is largely taken from {\tt FOL/simpdata.ML} of the

1262 Isabelle sources.

1264 The simplifier and the case splitting tactic, which reside on separate files,

1265 are not part of Pure Isabelle. They must be loaded explicitly by the

1266 object-logic as follows (below \texttt{\~\relax\~\relax} refers to

1267 \texttt{\$ISABELLE_HOME}):

1268 \begin{ttbox}

1269 use "\~\relax\~\relax/src/Provers/simplifier.ML";

1270 use "\~\relax\~\relax/src/Provers/splitter.ML";

1271 \end{ttbox}

1273 Simplification requires converting object-equalities to meta-level rewrite

1274 rules. This demands rules stating that equal terms and equivalent formulae

1275 are also equal at the meta-level. The rule declaration part of the file

1276 \texttt{FOL/IFOL.thy} contains the two lines

1277 \begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem}

1278 eq_reflection "(x=y) ==> (x==y)"

1279 iff_reflection "(P<->Q) ==> (P==Q)"

1280 \end{ttbox}

1281 Of course, you should only assert such rules if they are true for your

1282 particular logic. In Constructive Type Theory, equality is a ternary

1283 relation of the form $a=b\in A$; the type~$A$ determines the meaning

1284 of the equality essentially as a partial equivalence relation. The

1285 present simplifier cannot be used. Rewriting in \texttt{CTT} uses

1286 another simplifier, which resides in the file {\tt

1287 Provers/typedsimp.ML} and is not documented. Even this does not

1288 work for later variants of Constructive Type Theory that use

1289 intensional equality~\cite{nordstrom90}.

1292 \subsection{A collection of standard rewrite rules}

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

1295 connectives. These include cancellation and associative laws. We

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

1297 prover for intuitionistic FOL:

1298 \begin{ttbox}

1299 fun int_prove_fun s =

1300 (writeln s;

1301 prove_goal IFOL.thy s

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

1303 (IntPr.fast_tac 1) ]));

1304 \end{ttbox}

1305 The following rewrite rules about conjunction are a selection of those

1306 proved on \texttt{FOL/simpdata.ML}. Later, these will be supplied to the

1307 standard simpset.

1308 \begin{ttbox}

1309 val conj_simps = map int_prove_fun

1310 ["P & True <-> P", "True & P <-> P",

1311 "P & False <-> False", "False & P <-> False",

1312 "P & P <-> P",

1313 "P & ~P <-> False", "~P & P <-> False",

1314 "(P & Q) & R <-> P & (Q & R)"];

1315 \end{ttbox}

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

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

1318 are merely bound to an \ML{} identifier, for user reference.

1319 \begin{ttbox}

1320 val distrib_simps = map int_prove_fun

1321 ["P & (Q | R) <-> P&Q | P&R",

1322 "(Q | R) & P <-> Q&P | R&P",

1323 "(P | Q --> R) <-> (P --> R) & (Q --> R)"];

1324 \end{ttbox}

1327 \subsection{Functions for preprocessing the rewrite rules}

1328 \label{sec:setmksimps}

1329 \begin{ttbox}\indexbold{*setmksimps}

1330 setmksimps : simpset * (thm -> thm list) -> simpset \hfill{\bf infix 4}

1331 \end{ttbox}

1332 The next step is to define the function for preprocessing rewrite rules.

1333 This will be installed by calling \texttt{setmksimps} below. Preprocessing

1334 occurs whenever rewrite rules are added, whether by user command or

1335 automatically. Preprocessing involves extracting atomic rewrites at the

1336 object-level, then reflecting them to the meta-level.

1338 To start, the function \texttt{gen_all} strips any meta-level

1339 quantifiers from the front of the given theorem.

1341 The function \texttt{atomize} analyses a theorem in order to extract

1342 atomic rewrite rules. The head of all the patterns, matched by the

1343 wildcard~\texttt{_}, is the coercion function \texttt{Trueprop}.

1344 \begin{ttbox}

1345 fun atomize th = case concl_of th of

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

1347 atomize(th RS conjunct2)

1348 | _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)

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

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

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

1352 | _ => [th];

1353 \end{ttbox}

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

1355 \begin{itemize}

1356 \item Conjunction: extract rewrites from both conjuncts.

1357 \item Implication: convert $P\imp Q$ to the meta-implication $P\Imp Q$ and

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

1359 condition~$P$.

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

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

1362 \item \texttt{True} and \texttt{False} contain no useful rewrites.

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

1364 \end{itemize}

1365 The resulting theorems are not literally atomic --- they could be

1366 disjunctive, for example --- but are broken down as much as possible.

1367 See the file \texttt{ZF/simpdata.ML} for a sophisticated translation of

1368 set-theoretic formulae into rewrite rules.

1370 For standard situations like the above,

1371 there is a generic auxiliary function \ttindexbold{mk_atomize} that takes a

1372 list of pairs $(name, thms)$, where $name$ is an operator name and

1373 $thms$ is a list of theorems to resolve with in case the pattern matches,

1374 and returns a suitable \texttt{atomize} function.

1377 The simplified rewrites must now be converted into meta-equalities. The

1378 rule \texttt{eq_reflection} converts equality rewrites, while {\tt

1379 iff_reflection} converts if-and-only-if rewrites. The latter possibility

1380 can arise in two other ways: the negative theorem~$\neg P$ is converted to

1381 $P\equiv\texttt{False}$, and any other theorem~$P$ is converted to

1382 $P\equiv\texttt{True}$. The rules \texttt{iff_reflection_F} and {\tt

1383 iff_reflection_T} accomplish this conversion.

1384 \begin{ttbox}

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

1386 val iff_reflection_F = P_iff_F RS iff_reflection;

1387 \ttbreak

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

1389 val iff_reflection_T = P_iff_T RS iff_reflection;

1390 \end{ttbox}

1391 The function \texttt{mk_eq} converts a theorem to a meta-equality

1392 using the case analysis described above.

1393 \begin{ttbox}

1394 fun mk_eq th = case concl_of th of

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

1396 | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection

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

1398 | _ => th RS iff_reflection_T;

1399 \end{ttbox}

1400 The

1401 three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_eq}

1402 will be composed together and supplied below to \texttt{setmksimps}.

1405 \subsection{Making the initial simpset}

1407 It is time to assemble these items. The list \texttt{IFOL_simps} contains the

1408 default rewrite rules for intuitionistic first-order logic. The first of

1409 these is the reflexive law expressed as the equivalence

1410 $(a=a)\bimp\texttt{True}$; the rewrite rule $a=a$ is clearly useless.

1411 \begin{ttbox}

1412 val IFOL_simps =

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

1414 imp_simps \at iff_simps \at quant_simps;

1415 \end{ttbox}

1416 The list \texttt{triv_rls} contains trivial theorems for the solver. Any

1417 subgoal that is simplified to one of these will be removed.

1418 \begin{ttbox}

1419 val notFalseI = int_prove_fun "~False";

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

1421 \end{ttbox}

1422 We also define the function \ttindex{mk_meta_cong} to convert the conclusion

1423 of congruence rules into meta-equalities.

1424 \begin{ttbox}

1425 fun mk_meta_cong rl = standard (mk_meta_eq (mk_meta_prems rl));

1426 \end{ttbox}

1427 %

1428 The basic simpset for intuitionistic FOL is \ttindexbold{FOL_basic_ss}. It

1429 preprocess rewrites using

1430 {\tt gen_all}, \texttt{atomize} and \texttt{mk_eq}.

1431 It solves simplified subgoals using \texttt{triv_rls} and assumptions, and by

1432 detecting contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals

1433 of conditional rewrites.

1435 Other simpsets built from \texttt{FOL_basic_ss} will inherit these items.

1436 In particular, \ttindexbold{IFOL_ss}, which introduces {\tt

1437 IFOL_simps} as rewrite rules. \ttindexbold{FOL_ss} will later

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

1439 P\bimp P$.

1440 \index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler}

1441 \index{*addsimps}\index{*addcongs}

1442 \begin{ttbox}

1443 fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls {\at} prems),

1444 atac, etac FalseE];

1446 fun safe_solver prems = FIRST'[match_tac (triv_rls {\at} prems),

1447 eq_assume_tac, ematch_tac [FalseE]];

1449 val FOL_basic_ss =

1450 empty_ss setsubgoaler asm_simp_tac

1451 addsimprocs [defALL_regroup, defEX_regroup]

1452 setSSolver safe_solver

1453 setSolver unsafe_solver

1454 setmksimps (map mk_eq o atomize o gen_all)

1455 setmkcong mk_meta_cong;

1457 val IFOL_ss =

1458 FOL_basic_ss addsimps (IFOL_simps {\at}

1459 int_ex_simps {\at} int_all_simps)

1460 addcongs [imp_cong];

1461 \end{ttbox}

1462 This simpset takes \texttt{imp_cong} as a congruence rule in order to use

1463 contextual information to simplify the conclusions of implications:

1464 \[ \List{\Var{P}\bimp\Var{P'};\; \Var{P'} \Imp \Var{Q}\bimp\Var{Q'}} \Imp

1465 (\Var{P}\imp\Var{Q}) \bimp (\Var{P'}\imp\Var{Q'})

1466 \]

1467 By adding the congruence rule \texttt{conj_cong}, we could obtain a similar

1468 effect for conjunctions.

1471 \subsection{Splitter setup}\index{simplification!setting up the splitter}

1473 To set up case splitting, we have to call the \ML{} functor \ttindex{

1474 SplitterFun}, which takes the argument signature \texttt{SPLITTER_DATA}.

1475 So we prove the theorem \texttt{meta_eq_to_iff} below and store it, together

1476 with the \texttt{mk_eq} function described above and several standard

1477 theorems, in the structure \texttt{SplitterData}. Calling the functor with

1478 this data yields a new instantiation of the splitter for our logic.

1479 \begin{ttbox}

1480 val meta_eq_to_iff = prove_goal IFOL.thy "x==y ==> x<->y"

1481 (fn [prem] => [rewtac prem, rtac iffI 1, atac 1, atac 1]);

1482 \ttbreak

1483 structure SplitterData =

1484 struct

1485 structure Simplifier = Simplifier

1486 val mk_eq = mk_eq

1487 val meta_eq_to_iff = meta_eq_to_iff

1488 val iffD = iffD2

1489 val disjE = disjE

1490 val conjE = conjE

1491 val exE = exE

1492 val contrapos = contrapos

1493 val contrapos2 = contrapos2

1494 val notnotD = notnotD

1495 end;

1496 \ttbreak

1497 structure Splitter = SplitterFun(SplitterData);

1498 \end{ttbox}

1501 \subsection{Theory setup}\index{simplification!setting up the theory}

1502 \begin{ttbox}\indexbold{*Simplifier.setup}\index{*setup!simplifier}

1503 Simplifier.setup: (theory -> theory) list

1504 \end{ttbox}

1506 Advanced theory related features of the simplifier (e.g.\ implicit

1507 simpset support) have to be set up explicitly. The simplifier already

1508 provides a suitable setup function definition. This has to be

1509 installed into the base theory of any new object-logic via a

1510 \texttt{setup} declaration.

1512 For example, this is done in \texttt{FOL/IFOL.thy} as follows:

1513 \begin{ttbox}

1514 setup Simplifier.setup

1515 \end{ttbox}

1518 \index{simplification|)}

1521 %%% Local Variables:

1522 %%% mode: latex

1523 %%% TeX-master: "ref"

1524 %%% End: