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:
23 \isacommand{declare} \textit{theorem-name}@{text"[simp]"}\\
24 \isacommand{declare} \textit{theorem-name}@{text"[simp del]"}
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.
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.
42 subsubsection{*The simplification method*}
44 text{*\index{*simp (method)|bold}
45 The general format of the simplification method is
47 @{text simp} \textit{list of modifiers}
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.
57 subsubsection{*Adding and deleting simplification rules*}
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
65 @{text"add:"} \textit{list of theorem names}\\
66 @{text"del:"} \textit{list of theorem names}
68 In case you want to use only a specific list of theorems and ignore all
71 @{text"only:"} \textit{list of theorem names}
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:
82 lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs";
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
95 lemma "\<forall>x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []";
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:
105 apply(simp (no_asm));
109 There are three options that influence the treatment of assumptions:
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.
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
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
139 constdefs exor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
140 "exor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)";
146 lemma "exor A (\<not>A)";
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}
153 apply(simp only:exor_def);
156 In this particular case, the resulting goal
158 ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
160 can be proved by simplification. Thus we could have proved the lemma outright by
161 *}(*<*)oops;lemma "exor A (\<not>A)";(*>*)
162 apply(simp add: exor_def)
165 Of course we can also unfold definitions in the middle of a proof.
167 You should normally not turn a definition permanently into a simplification
168 rule because this defeats the whole purpose of an abbreviation.
171 If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
172 occurrences of $f$ with at least two arguments. Thus it is safer to define
173 $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
177 subsubsection{*Simplifying let-expressions*}
179 text{*\index{simplification!of let-expressions}
180 Proving a goal containing \isaindex{let}-expressions almost invariably
181 requires the @{text"let"}-con\-structs to be expanded at some point. Since
182 @{text"let"}-@{text"in"} is just syntactic sugar for a predefined constant
183 (called @{term"Let"}), expanding @{text"let"}-constructs means rewriting with
184 @{thm[source]Let_def}:
187 lemma "(let xs = [] in xs@ys@xs) = ys";
188 apply(simp add: Let_def);
192 If, in a particular context, there is no danger of a combinatorial explosion
193 of nested @{text"let"}s one could even simlify with @{thm[source]Let_def} by
196 declare Let_def [simp]
198 subsubsection{*Conditional equations*}
201 So far all examples of rewrite rules were equations. The simplifier also
202 accepts \emph{conditional} equations, for example
205 lemma hd_Cons_tl[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs";
206 apply(case_tac xs, simp, simp);
210 Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
211 sequence of methods. Assuming that the simplification rule
212 @{term"(rev xs = []) = (xs = [])"}
216 lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs";
221 is proved by plain simplification:
222 the conditional equation @{thm[source]hd_Cons_tl} above
223 can simplify @{term"hd(rev xs) # tl(rev xs)"} to @{term"rev xs"}
224 because the corresponding precondition @{term"rev xs ~= []"}
225 simplifies to @{term"xs ~= []"}, which is exactly the local
226 assumption of the subgoal.
230 subsubsection{*Automatic case splits*}
232 text{*\indexbold{case splits}\index{*split|(}
233 Goals containing @{text"if"}-expressions are usually proved by case
234 distinction on the condition of the @{text"if"}. For example the goal
237 lemma "\<forall>xs. if xs = [] then rev xs = [] else rev xs \<noteq> []";
242 ~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])
244 by a degenerate form of simplification
247 apply(simp only: split: split_if);
251 where no simplification rules are included (@{text"only:"} is followed by the
252 empty list of theorems) but the rule \isaindexbold{split_if} for
253 splitting @{text"if"}s is added (via the modifier @{text"split:"}). Because
254 case-splitting on @{text"if"}s is almost always the right proof strategy, the
255 simplifier performs it automatically. Try \isacommand{apply}@{text"(simp)"}
256 on the initial goal above.
258 This splitting idea generalizes from @{text"if"} to \isaindex{case}:
261 lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
264 \begin{isabelle}\makeatother
265 ~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
266 ~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)
271 apply(simp only: split: list.split);
275 In contrast to @{text"if"}-expressions, the simplifier does not split
276 @{text"case"}-expressions by default because this can lead to nontermination
277 in case of recursive datatypes. Again, if the @{text"only:"} modifier is
278 dropped, the above goal is solved,
281 lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
283 apply(simp split: list.split);
286 which \isacommand{apply}@{text"(simp)"} alone will not do.
288 In general, every datatype $t$ comes with a theorem
289 $t$@{text".split"} which can be declared to be a \bfindex{split rule} either
290 locally as above, or by giving it the @{text"split"} attribute globally:
293 declare list.split [split]
296 The @{text"split"} attribute can be removed with the @{text"del"} modifier,
302 apply(simp split del: split_if);
309 declare list.split [split del]
312 The above split rules intentionally only affect the conclusion of a
313 subgoal. If you want to split an @{text"if"} or @{text"case"}-expression in
314 the assumptions, you have to apply @{thm[source]split_if_asm} or
315 $t$@{text".split_asm"}:
318 lemma "if xs = [] then ys ~= [] else ys = [] ==> xs @ ys ~= []"
319 apply(simp only: split: split_if_asm);
325 In contrast to splitting the conclusion, this actually creates two
326 separate subgoals (which are solved by @{text"simp_all"}):
328 \ \isadigit{1}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
329 \ \isadigit{2}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{xs}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}
331 If you need to split both in the assumptions and the conclusion,
332 use $t$@{text".splits"} which subsumes $t$@{text".split"} and
333 $t$@{text".split_asm"}. Analogously, there is @{thm[source]if_splits}.
336 The simplifier merely simplifies the condition of an \isa{if} but not the
337 \isa{then} or \isa{else} parts. The latter are simplified only after the
338 condition reduces to \isa{True} or \isa{False}, or after splitting. The
339 same is true for \isaindex{case}-expressions: only the selector is
340 simplified at first, until either the expression reduces to one of the
341 cases or it is split.
348 subsubsection{*Arithmetic*}
350 text{*\index{arithmetic}
351 The simplifier routinely solves a small class of linear arithmetic formulae
352 (over type \isa{nat} and other numeric types): it only takes into account
353 assumptions and conclusions that are (possibly negated) (in)equalities
354 (@{text"="}, \isasymle, @{text"<"}) and it only knows about addition. Thus
357 lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
361 is proved by simplification, whereas the only slightly more complex
364 lemma "\<not> m < n \<and> m < n+1 \<Longrightarrow> m = n";
368 is not proved by simplification and requires @{text arith}.
372 subsubsection{*Tracing*}
373 text{*\indexbold{tracing the simplifier}
374 Using the simplifier effectively may take a bit of experimentation. Set the
375 \isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going
380 lemma "rev [a] = []";
387 \begin{ttbox}\makeatother
388 Applying instance of rewrite rule:
389 rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
391 rev [x] == rev [] @ [x]
392 Applying instance of rewrite rule:
396 Applying instance of rewrite rule:
400 Applying instance of rewrite rule:
401 ?x3 \# ?t3 = ?t3 == False
406 In more complicated cases, the trace can be quite lenghty, especially since
407 invocations of the simplifier are often nested (e.g.\ when solving conditions
408 of rewrite rules). Thus it is advisable to reset it:
411 ML "reset trace_simp";