1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{simp}% |
3 \def\isabellecontext{simp}% |
4 \isanewline |
4 % |
5 \isacommand{theory}\ simp\ {\isacharequal}\ Main{\isacharcolon}\isanewline |
5 \isamarkupsubsubsection{Simplification rules} |
6 \isanewline |
6 % |
7 \isacommand{end}\isanewline |
7 \begin{isamarkuptext}% |
|
8 \indexbold{simplification rule} |
|
9 To facilitate simplification, theorems can be declared to be simplification |
|
10 rules (with the help of the attribute \isa{{\isacharbrackleft}simp{\isacharbrackright}}\index{*simp |
|
11 (attribute)}), in which case proofs by simplification make use of these |
|
12 rules automatically. In addition the constructs \isacommand{datatype} and |
|
13 \isacommand{primrec} (and a few others) invisibly declare useful |
|
14 simplification rules. Explicit definitions are \emph{not} declared |
|
15 simplification rules automatically! |
|
16 |
|
17 Not merely equations but pretty much any theorem can become a simplification |
|
18 rule. The simplifier will try to make sense of it. For example, a theorem |
|
19 \isa{{\isasymnot}\ P} is automatically turned into \isa{P\ {\isacharequal}\ False}. The details |
|
20 are explained in \S\ref{sec:SimpHow}. |
|
21 |
|
22 The simplification attribute of theorems can be turned on and off as follows: |
|
23 \begin{quote} |
|
24 \isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp{\isacharbrackright}}\\ |
|
25 \isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp\ del{\isacharbrackright}} |
|
26 \end{quote} |
|
27 As a rule of thumb, equations that really simplify (like \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs} and \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ 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 \end{isamarkuptext}% |
|
41 % |
|
42 \isamarkupsubsubsection{The simplification method} |
|
43 % |
|
44 \begin{isamarkuptext}% |
|
45 \index{*simp (method)|bold} |
|
46 The general format of the simplification method is |
|
47 \begin{quote} |
|
48 \isa{simp} \textit{list of modifiers} |
|
49 \end{quote} |
|
50 where the list of \emph{modifiers} helps to fine tune the behaviour and may |
|
51 be empty. Most if not all of the proofs seen so far could have been performed |
|
52 with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks |
|
53 only the first subgoal and may thus need to be repeated---use |
|
54 \isaindex{simp_all} to simplify all subgoals. |
|
55 Note that \isa{simp} fails if nothing changes.% |
|
56 \end{isamarkuptext}% |
|
57 % |
|
58 \isamarkupsubsubsection{Adding and deleting simplification rules} |
|
59 % |
|
60 \begin{isamarkuptext}% |
|
61 If a certain theorem is merely needed in a few proofs by simplification, |
|
62 we do not need to make it a global simplification rule. Instead we can modify |
|
63 the set of simplification rules used in a simplification step by adding rules |
|
64 to it and/or deleting rules from it. The two modifiers for this are |
|
65 \begin{quote} |
|
66 \isa{add{\isacharcolon}} \textit{list of theorem names}\\ |
|
67 \isa{del{\isacharcolon}} \textit{list of theorem names} |
|
68 \end{quote} |
|
69 In case you want to use only a specific list of theorems and ignore all |
|
70 others: |
|
71 \begin{quote} |
|
72 \isa{only{\isacharcolon}} \textit{list of theorem names} |
|
73 \end{quote}% |
|
74 \end{isamarkuptext}% |
|
75 % |
|
76 \isamarkupsubsubsection{Assumptions} |
|
77 % |
|
78 \begin{isamarkuptext}% |
|
79 \index{simplification!with/of assumptions} |
|
80 By default, assumptions are part of the simplification process: they are used |
|
81 as simplification rules and are simplified themselves. For example:% |
|
82 \end{isamarkuptext}% |
|
83 \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ xs\ {\isacharat}\ zs\ {\isacharequal}\ ys\ {\isacharat}\ xs{\isacharsemicolon}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ ys\ {\isacharequal}\ zs{\isachardoublequote}\isanewline |
|
84 \isacommand{by}\ simp% |
|
85 \begin{isamarkuptext}% |
|
86 \noindent |
|
87 The second assumption simplifies to \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn |
|
88 simplifies the first assumption to \isa{zs\ {\isacharequal}\ ys}, thus reducing the |
|
89 conclusion to \isa{ys\ {\isacharequal}\ ys} and hence to \isa{True}. |
|
90 |
|
91 In some cases this may be too much of a good thing and may lead to |
|
92 nontermination:% |
|
93 \end{isamarkuptext}% |
|
94 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}% |
|
95 \begin{isamarkuptxt}% |
|
96 \noindent |
|
97 cannot be solved by an unmodified application of \isa{simp} because the |
|
98 simplification rule \isa{f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}} extracted from the assumption |
|
99 does not terminate. Isabelle notices certain simple forms of |
|
100 nontermination but not this one. The problem can be circumvented by |
|
101 explicitly telling the simplifier to ignore the assumptions:% |
|
102 \end{isamarkuptxt}% |
|
103 \isacommand{by}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}% |
|
104 \begin{isamarkuptext}% |
|
105 \noindent |
|
106 There are three options that influence the treatment of assumptions: |
|
107 \begin{description} |
|
108 \item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\indexbold{*no_asm} |
|
109 means that assumptions are completely ignored. |
|
110 \item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}}]\indexbold{*no_asm_simp} |
|
111 means that the assumptions are not simplified but |
|
112 are used in the simplification of the conclusion. |
|
113 \item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}]\indexbold{*no_asm_use} |
|
114 means that the assumptions are simplified but are not |
|
115 used in the simplification of each other or the conclusion. |
|
116 \end{description} |
|
117 Neither \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} nor \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} allow to simplify |
|
118 the above problematic subgoal. |
|
119 |
|
120 Note that only one of the above options is allowed, and it must precede all |
|
121 other arguments.% |
|
122 \end{isamarkuptext}% |
|
123 % |
|
124 \isamarkupsubsubsection{Rewriting with definitions} |
|
125 % |
|
126 \begin{isamarkuptext}% |
|
127 \index{simplification!with definitions} |
|
128 Constant definitions (\S\ref{sec:ConstDefinitions}) can |
|
129 be used as simplification rules, but by default they are not. Hence the |
|
130 simplifier does not expand them automatically, just as it should be: |
|
131 definitions are introduced for the purpose of abbreviating complex |
|
132 concepts. Of course we need to expand the definitions initially to derive |
|
133 enough lemmas that characterize the concept sufficiently for us to forget the |
|
134 original definition. For example, given% |
|
135 \end{isamarkuptext}% |
|
136 \isacommand{constdefs}\ exor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline |
|
137 \ \ \ \ \ \ \ \ \ {\isachardoublequote}exor\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}% |
|
138 \begin{isamarkuptext}% |
|
139 \noindent |
|
140 we may want to prove% |
|
141 \end{isamarkuptext}% |
|
142 \isacommand{lemma}\ {\isachardoublequote}exor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}% |
|
143 \begin{isamarkuptxt}% |
|
144 \noindent |
|
145 Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to |
|
146 get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}% |
|
147 \end{isamarkuptxt}% |
|
148 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}exor{\isacharunderscore}def{\isacharparenright}% |
|
149 \begin{isamarkuptxt}% |
|
150 \noindent |
|
151 In this particular case, the resulting goal |
|
152 \begin{isabelle} |
|
153 ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A% |
|
154 \end{isabelle} |
|
155 can be proved by simplification. Thus we could have proved the lemma outright% |
|
156 \end{isamarkuptxt}% |
|
157 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}% |
|
158 \begin{isamarkuptext}% |
|
159 \noindent |
|
160 Of course we can also unfold definitions in the middle of a proof. |
|
161 |
|
162 You should normally not turn a definition permanently into a simplification |
|
163 rule because this defeats the whole purpose of an abbreviation. |
|
164 |
|
165 \begin{warn} |
|
166 If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand |
|
167 occurrences of $f$ with at least two arguments. Thus it is safer to define |
|
168 $f$~\isasymequiv~\isasymlambda$x\,y.\;t$. |
|
169 \end{warn}% |
|
170 \end{isamarkuptext}% |
|
171 % |
|
172 \isamarkupsubsubsection{Simplifying let-expressions} |
|
173 % |
|
174 \begin{isamarkuptext}% |
|
175 \index{simplification!of let-expressions} |
|
176 Proving a goal containing \isaindex{let}-expressions almost invariably |
|
177 requires the \isa{let}-con\-structs to be expanded at some point. Since |
|
178 \isa{let}-\isa{in} is just syntactic sugar for a predefined constant |
|
179 (called \isa{Let}), expanding \isa{let}-constructs means rewriting with |
|
180 \isa{Let{\isacharunderscore}def}:% |
|
181 \end{isamarkuptext}% |
|
182 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline |
|
183 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}% |
|
184 \begin{isamarkuptext}% |
|
185 If, in a particular context, there is no danger of a combinatorial explosion |
|
186 of nested \isa{let}s one could even simlify with \isa{Let{\isacharunderscore}def} by |
|
187 default:% |
|
188 \end{isamarkuptext}% |
|
189 \isacommand{declare}\ Let{\isacharunderscore}def\ {\isacharbrackleft}simp{\isacharbrackright}% |
|
190 \isamarkupsubsubsection{Conditional equations} |
|
191 % |
|
192 \begin{isamarkuptext}% |
|
193 So far all examples of rewrite rules were equations. The simplifier also |
|
194 accepts \emph{conditional} equations, for example% |
|
195 \end{isamarkuptext}% |
|
196 \isacommand{lemma}\ hd{\isacharunderscore}Cons{\isacharunderscore}tl{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ \ {\isasymLongrightarrow}\ \ hd\ xs\ {\isacharhash}\ tl\ xs\ {\isacharequal}\ xs{\isachardoublequote}\isanewline |
|
197 \isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp{\isacharparenright}% |
|
198 \begin{isamarkuptext}% |
|
199 \noindent |
|
200 Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a |
|
201 sequence of methods. Assuming that the simplification rule |
|
202 \isa{{\isacharparenleft}rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}} |
|
203 is present as well,% |
|
204 \end{isamarkuptext}% |
|
205 \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}% |
|
206 \begin{isamarkuptext}% |
|
207 \noindent |
|
208 is proved by plain simplification: |
|
209 the conditional equation \isa{hd{\isacharunderscore}Cons{\isacharunderscore}tl} above |
|
210 can simplify \isa{hd\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl\ {\isacharparenleft}rev\ xs{\isacharparenright}} to \isa{rev\ xs} |
|
211 because the corresponding precondition \isa{rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}} |
|
212 simplifies to \isa{xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}}, which is exactly the local |
|
213 assumption of the subgoal.% |
|
214 \end{isamarkuptext}% |
|
215 % |
|
216 \isamarkupsubsubsection{Automatic case splits} |
|
217 % |
|
218 \begin{isamarkuptext}% |
|
219 \indexbold{case splits}\index{*split|(} |
|
220 Goals containing \isa{if}-expressions are usually proved by case |
|
221 distinction on the condition of the \isa{if}. For example the goal% |
|
222 \end{isamarkuptext}% |
|
223 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}xs{\isachardot}\ if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}% |
|
224 \begin{isamarkuptxt}% |
|
225 \noindent |
|
226 can be split into |
|
227 \begin{isabelle} |
|
228 ~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[]) |
|
229 \end{isabelle} |
|
230 by a degenerate form of simplification% |
|
231 \end{isamarkuptxt}% |
|
232 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}% |
|
233 \begin{isamarkuptext}% |
|
234 \noindent |
|
235 where no simplification rules are included (\isa{only{\isacharcolon}} is followed by the |
|
236 empty list of theorems) but the rule \isaindexbold{split_if} for |
|
237 splitting \isa{if}s is added (via the modifier \isa{split{\isacharcolon}}). Because |
|
238 case-splitting on \isa{if}s is almost always the right proof strategy, the |
|
239 simplifier performs it automatically. Try \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} |
|
240 on the initial goal above. |
|
241 |
|
242 This splitting idea generalizes from \isa{if} to \isaindex{case}:% |
|
243 \end{isamarkuptext}% |
|
244 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}% |
|
245 \begin{isamarkuptxt}% |
|
246 \noindent |
|
247 becomes |
|
248 \begin{isabelle}\makeatother |
|
249 ~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline |
|
250 ~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs) |
|
251 \end{isabelle} |
|
252 by typing% |
|
253 \end{isamarkuptxt}% |
|
254 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}% |
|
255 \begin{isamarkuptext}% |
|
256 \noindent |
|
257 In contrast to \isa{if}-expressions, the simplifier does not split |
|
258 \isa{case}-expressions by default because this can lead to nontermination |
|
259 in case of recursive datatypes. Again, if the \isa{only{\isacharcolon}} modifier is |
|
260 dropped, the above goal is solved,% |
|
261 \end{isamarkuptext}% |
|
262 \isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}% |
|
263 \begin{isamarkuptext}% |
|
264 \noindent% |
|
265 which \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} alone will not do. |
|
266 |
|
267 In general, every datatype $t$ comes with a theorem |
|
268 $t$\isa{{\isachardot}split} which can be declared to be a \bfindex{split rule} either |
|
269 locally as above, or by giving it the \isa{split} attribute globally:% |
|
270 \end{isamarkuptext}% |
|
271 \isacommand{declare}\ list{\isachardot}split\ {\isacharbrackleft}split{\isacharbrackright}% |
|
272 \begin{isamarkuptext}% |
|
273 \noindent |
|
274 The \isa{split} attribute can be removed with the \isa{del} modifier, |
|
275 either locally% |
|
276 \end{isamarkuptext}% |
|
277 \isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}% |
|
278 \begin{isamarkuptext}% |
|
279 \noindent |
|
280 or globally:% |
|
281 \end{isamarkuptext}% |
|
282 \isacommand{declare}\ list{\isachardot}split\ {\isacharbrackleft}split\ del{\isacharbrackright}% |
|
283 \begin{isamarkuptext}% |
|
284 The above split rules intentionally only affect the conclusion of a |
|
285 subgoal. If you want to split an \isa{if} or \isa{case}-expression in |
|
286 the assumptions, you have to apply \isa{split{\isacharunderscore}if{\isacharunderscore}asm} or |
|
287 $t$\isa{{\isachardot}split{\isacharunderscore}asm}:% |
|
288 \end{isamarkuptext}% |
|
289 \isacommand{lemma}\ {\isachardoublequote}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isacharat}\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
|
290 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}% |
|
291 \begin{isamarkuptext}% |
|
292 \noindent |
|
293 In contrast to splitting the conclusion, this actually creates two |
|
294 separate subgoals (which are solved by \isa{simp{\isacharunderscore}all}): |
|
295 \begin{isabelle} |
|
296 \ \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 |
|
297 \ \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} |
|
298 \end{isabelle} |
|
299 If you need to split both in the assumptions and the conclusion, |
|
300 use $t$\isa{{\isachardot}splits} which subsumes $t$\isa{{\isachardot}split} and |
|
301 $t$\isa{{\isachardot}split{\isacharunderscore}asm}. Analogously, there is \isa{if{\isacharunderscore}splits}. |
|
302 |
|
303 \begin{warn} |
|
304 The simplifier merely simplifies the condition of an \isa{if} but not the |
|
305 \isa{then} or \isa{else} parts. The latter are simplified only after the |
|
306 condition reduces to \isa{True} or \isa{False}, or after splitting. The |
|
307 same is true for \isaindex{case}-expressions: only the selector is |
|
308 simplified at first, until either the expression reduces to one of the |
|
309 cases or it is split. |
|
310 \end{warn} |
|
311 |
|
312 \index{*split|)}% |
|
313 \end{isamarkuptext}% |
|
314 % |
|
315 \isamarkupsubsubsection{Arithmetic} |
|
316 % |
|
317 \begin{isamarkuptext}% |
|
318 \index{arithmetic} |
|
319 The simplifier routinely solves a small class of linear arithmetic formulae |
|
320 (over type \isa{nat} and other numeric types): it only takes into account |
|
321 assumptions and conclusions that are (possibly negated) (in)equalities |
|
322 (\isa{{\isacharequal}}, \isasymle, \isa{{\isacharless}}) and it only knows about addition. Thus% |
|
323 \end{isamarkuptext}% |
|
324 \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}% |
|
325 \begin{isamarkuptext}% |
|
326 \noindent |
|
327 is proved by simplification, whereas the only slightly more complex% |
|
328 \end{isamarkuptext}% |
|
329 \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}% |
|
330 \begin{isamarkuptext}% |
|
331 \noindent |
|
332 is not proved by simplification and requires \isa{arith}.% |
|
333 \end{isamarkuptext}% |
|
334 % |
|
335 \isamarkupsubsubsection{Tracing} |
|
336 % |
|
337 \begin{isamarkuptext}% |
|
338 \indexbold{tracing the simplifier} |
|
339 Using the simplifier effectively may take a bit of experimentation. Set the |
|
340 \isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going |
|
341 on:% |
|
342 \end{isamarkuptext}% |
|
343 \isacommand{ML}\ {\isachardoublequote}set\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline |
|
344 \isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
|
345 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}% |
|
346 \begin{isamarkuptext}% |
|
347 \noindent |
|
348 produces the trace |
|
349 |
|
350 \begin{ttbox}\makeatother |
|
351 Applying instance of rewrite rule: |
|
352 rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1] |
|
353 Rewriting: |
|
354 rev [x] == rev [] @ [x] |
|
355 Applying instance of rewrite rule: |
|
356 rev [] == [] |
|
357 Rewriting: |
|
358 rev [] == [] |
|
359 Applying instance of rewrite rule: |
|
360 [] @ ?y == ?y |
|
361 Rewriting: |
|
362 [] @ [x] == [x] |
|
363 Applying instance of rewrite rule: |
|
364 ?x3 \# ?t3 = ?t3 == False |
|
365 Rewriting: |
|
366 [x] = [] == False |
|
367 \end{ttbox} |
|
368 |
|
369 In more complicated cases, the trace can be quite lenghty, especially since |
|
370 invocations of the simplifier are often nested (e.g.\ when solving conditions |
|
371 of rewrite rules). Thus it is advisable to reset it:% |
|
372 \end{isamarkuptext}% |
|
373 \isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline |
8 \end{isabellebody}% |
374 \end{isabellebody}% |
9 %%% Local Variables: |
375 %%% Local Variables: |
10 %%% mode: latex |
376 %%% mode: latex |
11 %%% TeX-master: "root" |
377 %%% TeX-master: "root" |
12 %%% End: |
378 %%% End: |