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

doc-src/TutorialI/Misc/simp.thy

author | nipkow |

Wed Dec 13 09:39:53 2000 +0100 (2000-12-13) | |

changeset 10654 | 458068404143 |

parent 10362 | c6b197ccf1f1 |

child 10788 | ea48dd8b0232 |

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

*** empty log message ***

1 (*<*)

2 theory simp = Main:

3 (*>*)

5 subsubsection{*Simplification rules*}

7 text{*\indexbold{simplification rule}

8 To facilitate simplification, theorems can be declared to be simplification

9 rules (with the help of the attribute @{text"[simp]"}\index{*simp

10 (attribute)}), in which case proofs by simplification make use of these

11 rules automatically. In addition the constructs \isacommand{datatype} and

12 \isacommand{primrec} (and a few others) invisibly declare useful

13 simplification rules. Explicit definitions are \emph{not} declared

14 simplification rules automatically!

16 Not merely equations but pretty much any theorem can become a simplification

17 rule. The simplifier will try to make sense of it. For example, a theorem

18 @{prop"~P"} is automatically turned into @{prop"P = False"}. The details

19 are explained in \S\ref{sec:SimpHow}.

21 The simplification attribute of theorems can be turned on and off as follows:

22 \begin{quote}

23 \isacommand{declare} \textit{theorem-name}@{text"[simp]"}\\

24 \isacommand{declare} \textit{theorem-name}@{text"[simp del]"}

25 \end{quote}

26 As a rule of thumb, equations that really simplify (like @{prop"rev(rev xs) =

27 xs"} and @{prop"xs @ [] = xs"}) should be made simplification

28 rules. Those of a more specific nature (e.g.\ distributivity laws, which

29 alter the structure of terms considerably) should only be used selectively,

30 i.e.\ they should not be default simplification rules. Conversely, it may

31 also happen that a simplification rule needs to be disabled in certain

32 proofs. Frequent changes in the simplification status of a theorem may

33 indicate a badly designed theory.

34 \begin{warn}

35 Simplification may not terminate, for example if both $f(x) = g(x)$ and

36 $g(x) = f(x)$ are simplification rules. It is the user's responsibility not

37 to include simplification rules that can lead to nontermination, either on

38 their own or in combination with other simplification rules.

39 \end{warn}

40 *}

42 subsubsection{*The simplification method*}

44 text{*\index{*simp (method)|bold}

45 The general format of the simplification method is

46 \begin{quote}

47 @{text simp} \textit{list of modifiers}

48 \end{quote}

49 where the list of \emph{modifiers} helps to fine tune the behaviour and may

50 be empty. Most if not all of the proofs seen so far could have been performed

51 with @{text simp} instead of \isa{auto}, except that @{text simp} attacks

52 only the first subgoal and may thus need to be repeated---use

53 \isaindex{simp_all} to simplify all subgoals.

54 Note that @{text simp} fails if nothing changes.

55 *}

57 subsubsection{*Adding and deleting simplification rules*}

59 text{*

60 If a certain theorem is merely needed in a few proofs by simplification,

61 we do not need to make it a global simplification rule. Instead we can modify

62 the set of simplification rules used in a simplification step by adding rules

63 to it and/or deleting rules from it. The two modifiers for this are

64 \begin{quote}

65 @{text"add:"} \textit{list of theorem names}\\

66 @{text"del:"} \textit{list of theorem names}

67 \end{quote}

68 In case you want to use only a specific list of theorems and ignore all

69 others:

70 \begin{quote}

71 @{text"only:"} \textit{list of theorem names}

72 \end{quote}

73 *}

75 subsubsection{*Assumptions*}

77 text{*\index{simplification!with/of assumptions}

78 By default, assumptions are part of the simplification process: they are used

79 as simplification rules and are simplified themselves. For example:

80 *}

82 lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs";

83 apply simp;

84 done

86 text{*\noindent

87 The second assumption simplifies to @{term"xs = []"}, which in turn

88 simplifies the first assumption to @{term"zs = ys"}, thus reducing the

89 conclusion to @{term"ys = ys"} and hence to @{term"True"}.

91 In some cases this may be too much of a good thing and may lead to

92 nontermination:

93 *}

95 lemma "\<forall>x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []";

97 txt{*\noindent

98 cannot be solved by an unmodified application of @{text"simp"} because the

99 simplification rule @{term"f x = g (f (g x))"} extracted from the assumption

100 does not terminate. Isabelle notices certain simple forms of

101 nontermination but not this one. The problem can be circumvented by

102 explicitly telling the simplifier to ignore the assumptions:

103 *}

105 apply(simp (no_asm));

106 done

108 text{*\noindent

109 There are three options that influence the treatment of assumptions:

110 \begin{description}

111 \item[@{text"(no_asm)"}]\indexbold{*no_asm}

112 means that assumptions are completely ignored.

113 \item[@{text"(no_asm_simp)"}]\indexbold{*no_asm_simp}

114 means that the assumptions are not simplified but

115 are used in the simplification of the conclusion.

116 \item[@{text"(no_asm_use)"}]\indexbold{*no_asm_use}

117 means that the assumptions are simplified but are not

118 used in the simplification of each other or the conclusion.

119 \end{description}

120 Neither @{text"(no_asm_simp)"} nor @{text"(no_asm_use)"} allow to simplify

121 the above problematic subgoal.

123 Note that only one of the above options is allowed, and it must precede all

124 other arguments.

125 *}

127 subsubsection{*Rewriting with definitions*}

129 text{*\index{simplification!with definitions}

130 Constant definitions (\S\ref{sec:ConstDefinitions}) can

131 be used as simplification rules, but by default they are not. Hence the

132 simplifier does not expand them automatically, just as it should be:

133 definitions are introduced for the purpose of abbreviating complex

134 concepts. Of course we need to expand the definitions initially to derive

135 enough lemmas that characterize the concept sufficiently for us to forget the

136 original definition. For example, given

137 *}

139 constdefs exor :: "bool \<Rightarrow> bool \<Rightarrow> bool"

140 "exor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)";

142 text{*\noindent

143 we may want to prove

144 *}

146 lemma "exor A (\<not>A)";

148 txt{*\noindent

149 Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to

150 get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}

151 *}

153 apply(simp only:exor_def);

155 txt{*\noindent

156 In this particular case, the resulting goal

157 @{subgoals[display,indent=0]}

158 can be proved by simplification. Thus we could have proved the lemma outright by

159 *}(*<*)oops;lemma "exor A (\<not>A)";(*>*)

160 apply(simp add: exor_def)

161 (*<*)done(*>*)

162 text{*\noindent

163 Of course we can also unfold definitions in the middle of a proof.

165 You should normally not turn a definition permanently into a simplification

166 rule because this defeats the whole purpose of an abbreviation.

168 \begin{warn}

169 If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand

170 occurrences of $f$ with at least two arguments. Thus it is safer to define

171 $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.

172 \end{warn}

173 *}

175 subsubsection{*Simplifying let-expressions*}

177 text{*\index{simplification!of let-expressions}

178 Proving a goal containing \isaindex{let}-expressions almost invariably

179 requires the @{text"let"}-con\-structs to be expanded at some point. Since

180 @{text"let"}-@{text"in"} is just syntactic sugar for a predefined constant

181 (called @{term"Let"}), expanding @{text"let"}-constructs means rewriting with

182 @{thm[source]Let_def}:

183 *}

185 lemma "(let xs = [] in xs@ys@xs) = ys";

186 apply(simp add: Let_def);

187 done

189 text{*

190 If, in a particular context, there is no danger of a combinatorial explosion

191 of nested @{text"let"}s one could even simlify with @{thm[source]Let_def} by

192 default:

193 *}

194 declare Let_def [simp]

196 subsubsection{*Conditional equations*}

198 text{*

199 So far all examples of rewrite rules were equations. The simplifier also

200 accepts \emph{conditional} equations, for example

201 *}

203 lemma hd_Cons_tl[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs";

204 apply(case_tac xs, simp, simp);

205 done

207 text{*\noindent

208 Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a

209 sequence of methods. Assuming that the simplification rule

210 @{term"(rev xs = []) = (xs = [])"}

211 is present as well,

212 *}

214 lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs";

215 (*<*)

216 by(simp);

217 (*>*)

218 text{*\noindent

219 is proved by plain simplification:

220 the conditional equation @{thm[source]hd_Cons_tl} above

221 can simplify @{term"hd(rev xs) # tl(rev xs)"} to @{term"rev xs"}

222 because the corresponding precondition @{term"rev xs ~= []"}

223 simplifies to @{term"xs ~= []"}, which is exactly the local

224 assumption of the subgoal.

225 *}

228 subsubsection{*Automatic case splits*}

230 text{*\indexbold{case splits}\index{*split (method, attr.)|(}

231 Goals containing @{text"if"}-expressions are usually proved by case

232 distinction on the condition of the @{text"if"}. For example the goal

233 *}

235 lemma "\<forall>xs. if xs = [] then rev xs = [] else rev xs \<noteq> []";

237 txt{*\noindent

238 can be split by a special method @{text split}:

239 *}

241 apply(split split_if)

243 txt{*\noindent

244 @{subgoals[display,indent=0]}

245 where \isaindexbold{split_if} is a theorem that expresses splitting of

246 @{text"if"}s. Because

247 case-splitting on @{text"if"}s is almost always the right proof strategy, the

248 simplifier performs it automatically. Try \isacommand{apply}@{text"(simp)"}

249 on the initial goal above.

251 This splitting idea generalizes from @{text"if"} to \isaindex{case}:

252 *}(*<*)by simp(*>*)

253 lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";

254 apply(split list.split);

256 txt{*

257 @{subgoals[display,indent=0]}

258 In contrast to @{text"if"}-expressions, the simplifier does not split

259 @{text"case"}-expressions by default because this can lead to nontermination

260 in case of recursive datatypes. Therefore the simplifier has a modifier

261 @{text split} for adding further splitting rules explicitly. This means the

262 above lemma can be proved in one step by

263 *}

264 (*<*)oops;

265 lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";

266 (*>*)

267 apply(simp split: list.split);

268 (*<*)done(*>*)

269 text{*\noindent

270 whereas \isacommand{apply}@{text"(simp)"} alone will not succeed.

272 In general, every datatype $t$ comes with a theorem

273 $t$@{text".split"} which can be declared to be a \bfindex{split rule} either

274 locally as above, or by giving it the @{text"split"} attribute globally:

275 *}

277 declare list.split [split]

279 text{*\noindent

280 The @{text"split"} attribute can be removed with the @{text"del"} modifier,

281 either locally

282 *}

283 (*<*)

284 lemma "dummy=dummy";

285 (*>*)

286 apply(simp split del: split_if);

287 (*<*)

288 oops;

289 (*>*)

290 text{*\noindent

291 or globally:

292 *}

293 declare list.split [split del]

295 text{*

296 In polished proofs the @{text split} method is rarely used on its own

297 but always as part of the simplifier. However, if a goal contains

298 multiple splittable constructs, the @{text split} method can be

299 helpful in selectively exploring the effects of splitting.

301 The above split rules intentionally only affect the conclusion of a

302 subgoal. If you want to split an @{text"if"} or @{text"case"}-expression in

303 the assumptions, you have to apply @{thm[source]split_if_asm} or

304 $t$@{text".split_asm"}:

305 *}

307 lemma "if xs = [] then ys \<noteq> [] else ys = [] \<Longrightarrow> xs @ ys \<noteq> []"

308 apply(split split_if_asm)

310 txt{*\noindent

311 In contrast to splitting the conclusion, this actually creates two

312 separate subgoals (which are solved by @{text"simp_all"}):

313 @{subgoals[display,indent=0]}

314 If you need to split both in the assumptions and the conclusion,

315 use $t$@{text".splits"} which subsumes $t$@{text".split"} and

316 $t$@{text".split_asm"}. Analogously, there is @{thm[source]if_splits}.

318 \begin{warn}

319 The simplifier merely simplifies the condition of an \isa{if} but not the

320 \isa{then} or \isa{else} parts. The latter are simplified only after the

321 condition reduces to \isa{True} or \isa{False}, or after splitting. The

322 same is true for \isaindex{case}-expressions: only the selector is

323 simplified at first, until either the expression reduces to one of the

324 cases or it is split.

325 \end{warn}\index{*split (method, attr.)|)}

326 *}

327 (*<*)

328 by(simp_all)

329 (*>*)

331 subsubsection{*Arithmetic*}

333 text{*\index{arithmetic}

334 The simplifier routinely solves a small class of linear arithmetic formulae

335 (over type \isa{nat} and other numeric types): it only takes into account

336 assumptions and conclusions that are (possibly negated) (in)equalities

337 (@{text"="}, \isasymle, @{text"<"}) and it only knows about addition. Thus

338 *}

340 lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"

341 (*<*)by(auto)(*>*)

343 text{*\noindent

344 is proved by simplification, whereas the only slightly more complex

345 *}

347 lemma "\<not> m < n \<and> m < n+1 \<Longrightarrow> m = n";

348 (*<*)by(arith)(*>*)

350 text{*\noindent

351 is not proved by simplification and requires @{text arith}.

352 *}

355 subsubsection{*Tracing*}

356 text{*\indexbold{tracing the simplifier}

357 Using the simplifier effectively may take a bit of experimentation. Set the

358 \isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going

359 on:

360 *}

362 ML "set trace_simp";

363 lemma "rev [a] = []";

364 apply(simp);

365 (*<*)oops(*>*)

367 text{*\noindent

368 produces the trace

370 \begin{ttbox}\makeatother

371 Applying instance of rewrite rule:

372 rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]

373 Rewriting:

374 rev [x] == rev [] @ [x]

375 Applying instance of rewrite rule:

376 rev [] == []

377 Rewriting:

378 rev [] == []

379 Applying instance of rewrite rule:

380 [] @ ?y == ?y

381 Rewriting:

382 [] @ [x] == [x]

383 Applying instance of rewrite rule:

384 ?x3 \# ?t3 = ?t3 == False

385 Rewriting:

386 [x] = [] == False

387 \end{ttbox}

389 In more complicated cases, the trace can be quite lenghty, especially since

390 invocations of the simplifier are often nested (e.g.\ when solving conditions

391 of rewrite rules). Thus it is advisable to reset it:

392 *}

394 ML "reset trace_simp";

396 (*<*)

397 end

398 (*>*)