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