9924
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{simp}%
|
17056
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
|
10 |
%
|
|
11 |
\endisatagtheory
|
|
12 |
{\isafoldtheory}%
|
|
13 |
%
|
|
14 |
\isadelimtheory
|
|
15 |
%
|
|
16 |
\endisadelimtheory
|
9933
|
17 |
%
|
11214
|
18 |
\isamarkupsubsection{Simplification Rules%
|
10397
|
19 |
}
|
11866
|
20 |
\isamarkuptrue%
|
9933
|
21 |
%
|
|
22 |
\begin{isamarkuptext}%
|
11458
|
23 |
\index{simplification rules}
|
|
24 |
To facilitate simplification,
|
|
25 |
the attribute \isa{{\isacharbrackleft}simp{\isacharbrackright}}\index{*simp (attribute)}
|
|
26 |
declares theorems to be simplification rules, which the simplifier
|
|
27 |
will use automatically. In addition, \isacommand{datatype} and
|
|
28 |
\isacommand{primrec} declarations (and a few others)
|
|
29 |
implicitly declare some simplification rules.
|
|
30 |
Explicit definitions are \emph{not} declared as
|
9933
|
31 |
simplification rules automatically!
|
|
32 |
|
11458
|
33 |
Nearly any theorem can become a simplification
|
|
34 |
rule. The simplifier will try to transform it into an equation.
|
|
35 |
For example, the theorem
|
|
36 |
\isa{{\isasymnot}\ P} is turned into \isa{P\ {\isacharequal}\ False}. The details
|
9933
|
37 |
are explained in \S\ref{sec:SimpHow}.
|
|
38 |
|
11458
|
39 |
The simplification attribute of theorems can be turned on and off:%
|
12489
|
40 |
\index{*simp del (attribute)}
|
9933
|
41 |
\begin{quote}
|
|
42 |
\isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp{\isacharbrackright}}\\
|
|
43 |
\isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp\ del{\isacharbrackright}}
|
|
44 |
\end{quote}
|
11309
|
45 |
Only equations that really simplify, like \isa{rev\
|
|
46 |
{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs} and
|
|
47 |
\isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\
|
|
48 |
{\isacharequal}\ xs}, should be declared as default simplification rules.
|
|
49 |
More specific ones should only be used selectively and should
|
|
50 |
not be made default. Distributivity laws, for example, alter
|
|
51 |
the structure of terms and can produce an exponential blow-up instead of
|
|
52 |
simplification. A default simplification rule may
|
|
53 |
need to be disabled in certain proofs. Frequent changes in the simplification
|
|
54 |
status of a theorem may indicate an unwise use of defaults.
|
9933
|
55 |
\begin{warn}
|
11458
|
56 |
Simplification can run forever, for example if both $f(x) = g(x)$ and
|
9933
|
57 |
$g(x) = f(x)$ are simplification rules. It is the user's responsibility not
|
|
58 |
to include simplification rules that can lead to nontermination, either on
|
|
59 |
their own or in combination with other simplification rules.
|
12332
|
60 |
\end{warn}
|
|
61 |
\begin{warn}
|
|
62 |
It is inadvisable to toggle the simplification attribute of a
|
12333
|
63 |
theorem from a parent theory $A$ in a child theory $B$ for good.
|
12332
|
64 |
The reason is that if some theory $C$ is based both on $B$ and (via a
|
13814
|
65 |
different path) on $A$, it is not defined what the simplification attribute
|
12332
|
66 |
of that theorem will be in $C$: it could be either.
|
9933
|
67 |
\end{warn}%
|
|
68 |
\end{isamarkuptext}%
|
11866
|
69 |
\isamarkuptrue%
|
9933
|
70 |
%
|
11458
|
71 |
\isamarkupsubsection{The {\tt\slshape simp} Method%
|
10397
|
72 |
}
|
11866
|
73 |
\isamarkuptrue%
|
9933
|
74 |
%
|
|
75 |
\begin{isamarkuptext}%
|
|
76 |
\index{*simp (method)|bold}
|
|
77 |
The general format of the simplification method is
|
|
78 |
\begin{quote}
|
|
79 |
\isa{simp} \textit{list of modifiers}
|
|
80 |
\end{quote}
|
10795
|
81 |
where the list of \emph{modifiers} fine tunes the behaviour and may
|
11309
|
82 |
be empty. Specific modifiers are discussed below. Most if not all of the
|
|
83 |
proofs seen so far could have been performed
|
9933
|
84 |
with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
|
10971
|
85 |
only the first subgoal and may thus need to be repeated --- use
|
11428
|
86 |
\methdx{simp_all} to simplify all subgoals.
|
11458
|
87 |
If nothing changes, \isa{simp} fails.%
|
9933
|
88 |
\end{isamarkuptext}%
|
11866
|
89 |
\isamarkuptrue%
|
9933
|
90 |
%
|
11214
|
91 |
\isamarkupsubsection{Adding and Deleting Simplification Rules%
|
10397
|
92 |
}
|
11866
|
93 |
\isamarkuptrue%
|
9933
|
94 |
%
|
|
95 |
\begin{isamarkuptext}%
|
11458
|
96 |
\index{simplification rules!adding and deleting}%
|
9933
|
97 |
If a certain theorem is merely needed in a few proofs by simplification,
|
|
98 |
we do not need to make it a global simplification rule. Instead we can modify
|
|
99 |
the set of simplification rules used in a simplification step by adding rules
|
|
100 |
to it and/or deleting rules from it. The two modifiers for this are
|
|
101 |
\begin{quote}
|
11458
|
102 |
\isa{add{\isacharcolon}} \textit{list of theorem names}\index{*add (modifier)}\\
|
|
103 |
\isa{del{\isacharcolon}} \textit{list of theorem names}\index{*del (modifier)}
|
9933
|
104 |
\end{quote}
|
11458
|
105 |
Or you can use a specific list of theorems and omit all others:
|
9933
|
106 |
\begin{quote}
|
11458
|
107 |
\isa{only{\isacharcolon}} \textit{list of theorem names}\index{*only (modifier)}
|
11309
|
108 |
\end{quote}
|
|
109 |
In this example, we invoke the simplifier, adding two distributive
|
|
110 |
laws:
|
|
111 |
\begin{quote}
|
|
112 |
\isacommand{apply}\isa{{\isacharparenleft}simp\ add{\isacharcolon}\ mod{\isacharunderscore}mult{\isacharunderscore}distrib\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}}
|
9933
|
113 |
\end{quote}%
|
|
114 |
\end{isamarkuptext}%
|
11866
|
115 |
\isamarkuptrue%
|
9933
|
116 |
%
|
11214
|
117 |
\isamarkupsubsection{Assumptions%
|
10397
|
118 |
}
|
11866
|
119 |
\isamarkuptrue%
|
9933
|
120 |
%
|
|
121 |
\begin{isamarkuptext}%
|
|
122 |
\index{simplification!with/of assumptions}
|
|
123 |
By default, assumptions are part of the simplification process: they are used
|
|
124 |
as simplification rules and are simplified themselves. For example:%
|
|
125 |
\end{isamarkuptext}%
|
17175
|
126 |
\isamarkuptrue%
|
|
127 |
\isacommand{lemma}\isamarkupfalse%
|
|
128 |
\ {\isachardoublequoteopen}{\isasymlbrakk}\ xs\ {\isacharat}\ zs\ {\isacharequal}\ ys\ {\isacharat}\ xs{\isacharsemicolon}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ ys\ {\isacharequal}\ zs{\isachardoublequoteclose}\isanewline
|
17056
|
129 |
%
|
|
130 |
\isadelimproof
|
|
131 |
%
|
|
132 |
\endisadelimproof
|
|
133 |
%
|
|
134 |
\isatagproof
|
17175
|
135 |
\isacommand{apply}\isamarkupfalse%
|
|
136 |
\ simp\isanewline
|
|
137 |
\isacommand{done}\isamarkupfalse%
|
|
138 |
%
|
17056
|
139 |
\endisatagproof
|
|
140 |
{\isafoldproof}%
|
|
141 |
%
|
|
142 |
\isadelimproof
|
|
143 |
%
|
|
144 |
\endisadelimproof
|
11866
|
145 |
%
|
9933
|
146 |
\begin{isamarkuptext}%
|
|
147 |
\noindent
|
|
148 |
The second assumption simplifies to \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn
|
|
149 |
simplifies the first assumption to \isa{zs\ {\isacharequal}\ ys}, thus reducing the
|
|
150 |
conclusion to \isa{ys\ {\isacharequal}\ ys} and hence to \isa{True}.
|
|
151 |
|
11458
|
152 |
In some cases, using the assumptions can lead to nontermination:%
|
9933
|
153 |
\end{isamarkuptext}%
|
17175
|
154 |
\isamarkuptrue%
|
|
155 |
\isacommand{lemma}\isamarkupfalse%
|
|
156 |
\ {\isachardoublequoteopen}{\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}{\isachardoublequoteclose}%
|
17056
|
157 |
\isadelimproof
|
|
158 |
%
|
|
159 |
\endisadelimproof
|
|
160 |
%
|
|
161 |
\isatagproof
|
16069
|
162 |
%
|
|
163 |
\begin{isamarkuptxt}%
|
|
164 |
\noindent
|
|
165 |
An unmodified application of \isa{simp} loops. The culprit is the
|
|
166 |
simplification rule \isa{f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}}, which is extracted from
|
|
167 |
the assumption. (Isabelle notices certain simple forms of
|
|
168 |
nontermination but not this one.) The problem can be circumvented by
|
|
169 |
telling the simplifier to ignore the assumptions:%
|
|
170 |
\end{isamarkuptxt}%
|
17175
|
171 |
\isamarkuptrue%
|
|
172 |
\isacommand{apply}\isamarkupfalse%
|
|
173 |
{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}\isanewline
|
|
174 |
\isacommand{done}\isamarkupfalse%
|
|
175 |
%
|
17056
|
176 |
\endisatagproof
|
|
177 |
{\isafoldproof}%
|
|
178 |
%
|
|
179 |
\isadelimproof
|
|
180 |
%
|
|
181 |
\endisadelimproof
|
11866
|
182 |
%
|
9933
|
183 |
\begin{isamarkuptext}%
|
|
184 |
\noindent
|
11458
|
185 |
Three modifiers influence the treatment of assumptions:
|
9933
|
186 |
\begin{description}
|
11458
|
187 |
\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\index{*no_asm (modifier)}
|
9933
|
188 |
means that assumptions are completely ignored.
|
11458
|
189 |
\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}}]\index{*no_asm_simp (modifier)}
|
9933
|
190 |
means that the assumptions are not simplified but
|
|
191 |
are used in the simplification of the conclusion.
|
11458
|
192 |
\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}]\index{*no_asm_use (modifier)}
|
9933
|
193 |
means that the assumptions are simplified but are not
|
|
194 |
used in the simplification of each other or the conclusion.
|
|
195 |
\end{description}
|
11458
|
196 |
Only one of the modifiers is allowed, and it must precede all
|
11309
|
197 |
other modifiers.
|
13623
|
198 |
%\begin{warn}
|
|
199 |
%Assumptions are simplified in a left-to-right fashion. If an
|
|
200 |
%assumption can help in simplifying one to the left of it, this may get
|
|
201 |
%overlooked. In such cases you have to rotate the assumptions explicitly:
|
|
202 |
%\isacommand{apply}@ {text"("}\methdx{rotate_tac}~$n$@ {text")"}
|
|
203 |
%causes a cyclic shift by $n$ positions from right to left, if $n$ is
|
|
204 |
%positive, and from left to right, if $n$ is negative.
|
|
205 |
%Beware that such rotations make proofs quite brittle.
|
|
206 |
%\end{warn}%
|
9933
|
207 |
\end{isamarkuptext}%
|
11866
|
208 |
\isamarkuptrue%
|
9933
|
209 |
%
|
11214
|
210 |
\isamarkupsubsection{Rewriting with Definitions%
|
10397
|
211 |
}
|
11866
|
212 |
\isamarkuptrue%
|
9933
|
213 |
%
|
|
214 |
\begin{isamarkuptext}%
|
11215
|
215 |
\label{sec:Simp-with-Defs}\index{simplification!with definitions}
|
11458
|
216 |
Constant definitions (\S\ref{sec:ConstDefinitions}) can be used as
|
|
217 |
simplification rules, but by default they are not: the simplifier does not
|
|
218 |
expand them automatically. Definitions are intended for introducing abstract
|
12584
|
219 |
concepts and not merely as abbreviations. Of course, we need to expand
|
11458
|
220 |
the definition initially, but once we have proved enough abstract properties
|
|
221 |
of the new constant, we can forget its original definition. This style makes
|
|
222 |
proofs more robust: if the definition has to be changed,
|
|
223 |
only the proofs of the abstract properties will be affected.
|
|
224 |
|
|
225 |
For example, given%
|
9933
|
226 |
\end{isamarkuptext}%
|
17175
|
227 |
\isamarkuptrue%
|
|
228 |
\isacommand{constdefs}\isamarkupfalse%
|
|
229 |
\ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
|
|
230 |
\ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}xor\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}%
|
9933
|
231 |
\begin{isamarkuptext}%
|
|
232 |
\noindent
|
|
233 |
we may want to prove%
|
|
234 |
\end{isamarkuptext}%
|
17175
|
235 |
\isamarkuptrue%
|
|
236 |
\isacommand{lemma}\isamarkupfalse%
|
|
237 |
\ {\isachardoublequoteopen}xor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequoteclose}%
|
17056
|
238 |
\isadelimproof
|
|
239 |
%
|
|
240 |
\endisadelimproof
|
|
241 |
%
|
|
242 |
\isatagproof
|
16069
|
243 |
%
|
|
244 |
\begin{isamarkuptxt}%
|
|
245 |
\noindent
|
|
246 |
Typically, we begin by unfolding some definitions:
|
|
247 |
\indexbold{definitions!unfolding}%
|
|
248 |
\end{isamarkuptxt}%
|
17175
|
249 |
\isamarkuptrue%
|
|
250 |
\isacommand{apply}\isamarkupfalse%
|
|
251 |
{\isacharparenleft}simp\ only{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}%
|
16069
|
252 |
\begin{isamarkuptxt}%
|
|
253 |
\noindent
|
|
254 |
In this particular case, the resulting goal
|
|
255 |
\begin{isabelle}%
|
|
256 |
\ {\isadigit{1}}{\isachardot}\ A\ {\isasymand}\ {\isasymnot}\ {\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ A\ {\isasymand}\ {\isasymnot}\ A%
|
|
257 |
\end{isabelle}
|
|
258 |
can be proved by simplification. Thus we could have proved the lemma outright by%
|
|
259 |
\end{isamarkuptxt}%
|
17175
|
260 |
\isamarkuptrue%
|
17056
|
261 |
%
|
|
262 |
\endisatagproof
|
|
263 |
{\isafoldproof}%
|
|
264 |
%
|
|
265 |
\isadelimproof
|
|
266 |
%
|
|
267 |
\endisadelimproof
|
|
268 |
%
|
|
269 |
\isadelimproof
|
|
270 |
%
|
|
271 |
\endisadelimproof
|
|
272 |
%
|
|
273 |
\isatagproof
|
17175
|
274 |
\isacommand{apply}\isamarkupfalse%
|
17181
|
275 |
{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}%
|
17056
|
276 |
\endisatagproof
|
|
277 |
{\isafoldproof}%
|
|
278 |
%
|
|
279 |
\isadelimproof
|
|
280 |
%
|
|
281 |
\endisadelimproof
|
11866
|
282 |
%
|
9933
|
283 |
\begin{isamarkuptext}%
|
|
284 |
\noindent
|
|
285 |
Of course we can also unfold definitions in the middle of a proof.
|
|
286 |
|
|
287 |
\begin{warn}
|
10971
|
288 |
If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
|
|
289 |
occurrences of $f$ with at least two arguments. This may be helpful for unfolding
|
|
290 |
$f$ selectively, but it may also get in the way. Defining
|
|
291 |
$f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$.
|
12473
|
292 |
\end{warn}
|
|
293 |
|
|
294 |
There is also the special method \isa{unfold}\index{*unfold (method)|bold}
|
|
295 |
which merely unfolds
|
|
296 |
one or several definitions, as in \isacommand{apply}\isa{(unfold xor_def)}.
|
12533
|
297 |
This is can be useful in situations where \isa{simp} does too much.
|
|
298 |
Warning: \isa{unfold} acts on all subgoals!%
|
9933
|
299 |
\end{isamarkuptext}%
|
11866
|
300 |
\isamarkuptrue%
|
9933
|
301 |
%
|
11214
|
302 |
\isamarkupsubsection{Simplifying {\tt\slshape let}-Expressions%
|
10397
|
303 |
}
|
11866
|
304 |
\isamarkuptrue%
|
9933
|
305 |
%
|
|
306 |
\begin{isamarkuptext}%
|
11458
|
307 |
\index{simplification!of \isa{let}-expressions}\index{*let expressions}%
|
|
308 |
Proving a goal containing \isa{let}-expressions almost invariably requires the
|
|
309 |
\isa{let}-con\-structs to be expanded at some point. Since
|
|
310 |
\isa{let}\ldots\isa{=}\ldots\isa{in}{\ldots} is just syntactic sugar for
|
|
311 |
the predefined constant \isa{Let}, expanding \isa{let}-constructs
|
|
312 |
means rewriting with \tdx{Let_def}:%
|
9933
|
313 |
\end{isamarkuptext}%
|
17175
|
314 |
\isamarkuptrue%
|
|
315 |
\isacommand{lemma}\isamarkupfalse%
|
|
316 |
\ {\isachardoublequoteopen}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequoteclose}\isanewline
|
17056
|
317 |
%
|
|
318 |
\isadelimproof
|
|
319 |
%
|
|
320 |
\endisadelimproof
|
|
321 |
%
|
|
322 |
\isatagproof
|
17175
|
323 |
\isacommand{apply}\isamarkupfalse%
|
|
324 |
{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}\isanewline
|
|
325 |
\isacommand{done}\isamarkupfalse%
|
|
326 |
%
|
17056
|
327 |
\endisatagproof
|
|
328 |
{\isafoldproof}%
|
|
329 |
%
|
|
330 |
\isadelimproof
|
|
331 |
%
|
|
332 |
\endisadelimproof
|
11866
|
333 |
%
|
9933
|
334 |
\begin{isamarkuptext}%
|
|
335 |
If, in a particular context, there is no danger of a combinatorial explosion
|
11458
|
336 |
of nested \isa{let}s, you could even simplify with \isa{Let{\isacharunderscore}def} by
|
9933
|
337 |
default:%
|
|
338 |
\end{isamarkuptext}%
|
17175
|
339 |
\isamarkuptrue%
|
|
340 |
\isacommand{declare}\isamarkupfalse%
|
|
341 |
\ Let{\isacharunderscore}def\ {\isacharbrackleft}simp{\isacharbrackright}%
|
11458
|
342 |
\isamarkupsubsection{Conditional Simplification Rules%
|
10397
|
343 |
}
|
11866
|
344 |
\isamarkuptrue%
|
9933
|
345 |
%
|
|
346 |
\begin{isamarkuptext}%
|
11458
|
347 |
\index{conditional simplification rules}%
|
9933
|
348 |
So far all examples of rewrite rules were equations. The simplifier also
|
|
349 |
accepts \emph{conditional} equations, for example%
|
|
350 |
\end{isamarkuptext}%
|
17175
|
351 |
\isamarkuptrue%
|
|
352 |
\isacommand{lemma}\isamarkupfalse%
|
|
353 |
\ hd{\isacharunderscore}Cons{\isacharunderscore}tl{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ \ {\isasymLongrightarrow}\ \ hd\ xs\ {\isacharhash}\ tl\ xs\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
|
17056
|
354 |
%
|
|
355 |
\isadelimproof
|
|
356 |
%
|
|
357 |
\endisadelimproof
|
|
358 |
%
|
|
359 |
\isatagproof
|
17175
|
360 |
\isacommand{apply}\isamarkupfalse%
|
|
361 |
{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp{\isacharparenright}\isanewline
|
|
362 |
\isacommand{done}\isamarkupfalse%
|
|
363 |
%
|
17056
|
364 |
\endisatagproof
|
|
365 |
{\isafoldproof}%
|
|
366 |
%
|
|
367 |
\isadelimproof
|
|
368 |
%
|
|
369 |
\endisadelimproof
|
11866
|
370 |
%
|
9933
|
371 |
\begin{isamarkuptext}%
|
|
372 |
\noindent
|
|
373 |
Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
|
|
374 |
sequence of methods. Assuming that the simplification rule
|
|
375 |
\isa{{\isacharparenleft}rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}}
|
10795
|
376 |
is present as well,
|
|
377 |
the lemma below is proved by plain simplification:%
|
9933
|
378 |
\end{isamarkuptext}%
|
17175
|
379 |
\isamarkuptrue%
|
|
380 |
\isacommand{lemma}\isamarkupfalse%
|
|
381 |
\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequoteclose}%
|
17056
|
382 |
\isadelimproof
|
|
383 |
%
|
|
384 |
\endisadelimproof
|
|
385 |
%
|
|
386 |
\isatagproof
|
|
387 |
%
|
|
388 |
\endisatagproof
|
|
389 |
{\isafoldproof}%
|
|
390 |
%
|
|
391 |
\isadelimproof
|
|
392 |
%
|
|
393 |
\endisadelimproof
|
11866
|
394 |
%
|
9933
|
395 |
\begin{isamarkuptext}%
|
|
396 |
\noindent
|
10795
|
397 |
The conditional equation \isa{hd{\isacharunderscore}Cons{\isacharunderscore}tl} above
|
9933
|
398 |
can simplify \isa{hd\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl\ {\isacharparenleft}rev\ xs{\isacharparenright}} to \isa{rev\ xs}
|
|
399 |
because the corresponding precondition \isa{rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}}
|
|
400 |
simplifies to \isa{xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}}, which is exactly the local
|
|
401 |
assumption of the subgoal.%
|
|
402 |
\end{isamarkuptext}%
|
11866
|
403 |
\isamarkuptrue%
|
9933
|
404 |
%
|
11214
|
405 |
\isamarkupsubsection{Automatic Case Splits%
|
10397
|
406 |
}
|
11866
|
407 |
\isamarkuptrue%
|
9933
|
408 |
%
|
|
409 |
\begin{isamarkuptext}%
|
11458
|
410 |
\label{sec:AutoCaseSplits}\indexbold{case splits}%
|
|
411 |
Goals containing \isa{if}-expressions\index{*if expressions!splitting of}
|
|
412 |
are usually proved by case
|
|
413 |
distinction on the boolean condition. Here is an example:%
|
9933
|
414 |
\end{isamarkuptext}%
|
17175
|
415 |
\isamarkuptrue%
|
|
416 |
\isacommand{lemma}\isamarkupfalse%
|
|
417 |
\ {\isachardoublequoteopen}{\isasymforall}xs{\isachardot}\ if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}%
|
17056
|
418 |
\isadelimproof
|
|
419 |
%
|
|
420 |
\endisadelimproof
|
|
421 |
%
|
|
422 |
\isatagproof
|
16069
|
423 |
%
|
|
424 |
\begin{isamarkuptxt}%
|
|
425 |
\noindent
|
|
426 |
The goal can be split by a special method, \methdx{split}:%
|
|
427 |
\end{isamarkuptxt}%
|
17175
|
428 |
\isamarkuptrue%
|
|
429 |
\isacommand{apply}\isamarkupfalse%
|
|
430 |
{\isacharparenleft}split\ split{\isacharunderscore}if{\isacharparenright}%
|
16069
|
431 |
\begin{isamarkuptxt}%
|
|
432 |
\noindent
|
|
433 |
\begin{isabelle}%
|
|
434 |
\ {\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}%
|
|
435 |
\end{isabelle}
|
|
436 |
where \tdx{split_if} is a theorem that expresses splitting of
|
|
437 |
\isa{if}s. Because
|
|
438 |
splitting the \isa{if}s is usually the right proof strategy, the
|
|
439 |
simplifier does it automatically. Try \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}}
|
|
440 |
on the initial goal above.
|
|
441 |
|
|
442 |
This splitting idea generalizes from \isa{if} to \sdx{case}.
|
|
443 |
Let us simplify a case analysis over lists:\index{*list.split (theorem)}%
|
|
444 |
\end{isamarkuptxt}%
|
17175
|
445 |
\isamarkuptrue%
|
17056
|
446 |
%
|
|
447 |
\endisatagproof
|
|
448 |
{\isafoldproof}%
|
|
449 |
%
|
|
450 |
\isadelimproof
|
|
451 |
%
|
|
452 |
\endisadelimproof
|
17175
|
453 |
\isacommand{lemma}\isamarkupfalse%
|
|
454 |
\ {\isachardoublequoteopen}{\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{\isachardoublequoteclose}\isanewline
|
17056
|
455 |
%
|
|
456 |
\isadelimproof
|
|
457 |
%
|
|
458 |
\endisadelimproof
|
|
459 |
%
|
|
460 |
\isatagproof
|
17175
|
461 |
\isacommand{apply}\isamarkupfalse%
|
|
462 |
{\isacharparenleft}split\ list{\isachardot}split{\isacharparenright}%
|
16069
|
463 |
\begin{isamarkuptxt}%
|
|
464 |
\begin{isabelle}%
|
|
465 |
\ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isacharparenright}\ {\isasymand}\isanewline
|
|
466 |
\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}%
|
|
467 |
\end{isabelle}
|
|
468 |
The simplifier does not split
|
|
469 |
\isa{case}-expressions, as it does \isa{if}-expressions,
|
|
470 |
because with recursive datatypes it could lead to nontermination.
|
|
471 |
Instead, the simplifier has a modifier
|
|
472 |
\isa{split}\index{*split (modifier)}
|
|
473 |
for adding splitting rules explicitly. The
|
|
474 |
lemma above can be proved in one step by%
|
|
475 |
\end{isamarkuptxt}%
|
17175
|
476 |
\isamarkuptrue%
|
17056
|
477 |
%
|
|
478 |
\endisatagproof
|
|
479 |
{\isafoldproof}%
|
|
480 |
%
|
|
481 |
\isadelimproof
|
|
482 |
%
|
|
483 |
\endisadelimproof
|
|
484 |
%
|
|
485 |
\isadelimproof
|
|
486 |
%
|
|
487 |
\endisadelimproof
|
|
488 |
%
|
|
489 |
\isatagproof
|
17175
|
490 |
\isacommand{apply}\isamarkupfalse%
|
17181
|
491 |
{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
|
17056
|
492 |
\endisatagproof
|
|
493 |
{\isafoldproof}%
|
|
494 |
%
|
|
495 |
\isadelimproof
|
|
496 |
%
|
|
497 |
\endisadelimproof
|
11866
|
498 |
%
|
9933
|
499 |
\begin{isamarkuptext}%
|
10668
|
500 |
\noindent
|
|
501 |
whereas \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} alone will not succeed.
|
9933
|
502 |
|
11458
|
503 |
Every datatype $t$ comes with a theorem
|
9933
|
504 |
$t$\isa{{\isachardot}split} which can be declared to be a \bfindex{split rule} either
|
11458
|
505 |
locally as above, or by giving it the \attrdx{split} attribute globally:%
|
9933
|
506 |
\end{isamarkuptext}%
|
17175
|
507 |
\isamarkuptrue%
|
|
508 |
\isacommand{declare}\isamarkupfalse%
|
|
509 |
\ list{\isachardot}split\ {\isacharbrackleft}split{\isacharbrackright}%
|
9933
|
510 |
\begin{isamarkuptext}%
|
|
511 |
\noindent
|
|
512 |
The \isa{split} attribute can be removed with the \isa{del} modifier,
|
|
513 |
either locally%
|
|
514 |
\end{isamarkuptext}%
|
17175
|
515 |
\isamarkuptrue%
|
17056
|
516 |
%
|
|
517 |
\isadelimproof
|
|
518 |
%
|
|
519 |
\endisadelimproof
|
|
520 |
%
|
|
521 |
\isatagproof
|
17175
|
522 |
\isacommand{apply}\isamarkupfalse%
|
17181
|
523 |
{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
|
17056
|
524 |
\endisatagproof
|
|
525 |
{\isafoldproof}%
|
|
526 |
%
|
|
527 |
\isadelimproof
|
|
528 |
%
|
|
529 |
\endisadelimproof
|
11866
|
530 |
%
|
9933
|
531 |
\begin{isamarkuptext}%
|
|
532 |
\noindent
|
|
533 |
or globally:%
|
|
534 |
\end{isamarkuptext}%
|
17175
|
535 |
\isamarkuptrue%
|
|
536 |
\isacommand{declare}\isamarkupfalse%
|
|
537 |
\ list{\isachardot}split\ {\isacharbrackleft}split\ del{\isacharbrackright}%
|
9933
|
538 |
\begin{isamarkuptext}%
|
11458
|
539 |
Polished proofs typically perform splitting within \isa{simp} rather than
|
|
540 |
invoking the \isa{split} method. However, if a goal contains
|
|
541 |
several \isa{if} and \isa{case} expressions,
|
|
542 |
the \isa{split} method can be
|
10668
|
543 |
helpful in selectively exploring the effects of splitting.
|
|
544 |
|
11458
|
545 |
The split rules shown above are intended to affect only the subgoal's
|
|
546 |
conclusion. If you want to split an \isa{if} or \isa{case}-expression
|
|
547 |
in the assumptions, you have to apply \tdx{split_if_asm} or
|
9933
|
548 |
$t$\isa{{\isachardot}split{\isacharunderscore}asm}:%
|
|
549 |
\end{isamarkuptext}%
|
17175
|
550 |
\isamarkuptrue%
|
|
551 |
\isacommand{lemma}\isamarkupfalse%
|
|
552 |
\ {\isachardoublequoteopen}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ else\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
|
17056
|
553 |
%
|
|
554 |
\isadelimproof
|
|
555 |
%
|
|
556 |
\endisadelimproof
|
|
557 |
%
|
|
558 |
\isatagproof
|
17175
|
559 |
\isacommand{apply}\isamarkupfalse%
|
|
560 |
{\isacharparenleft}split\ split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}%
|
16069
|
561 |
\begin{isamarkuptxt}%
|
|
562 |
\noindent
|
|
563 |
Unlike splitting the conclusion, this step creates two
|
|
564 |
separate subgoals, which here can be solved by \isa{simp{\isacharunderscore}all}:
|
|
565 |
\begin{isabelle}%
|
|
566 |
\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
|
|
567 |
\ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}%
|
|
568 |
\end{isabelle}
|
|
569 |
If you need to split both in the assumptions and the conclusion,
|
|
570 |
use $t$\isa{{\isachardot}splits} which subsumes $t$\isa{{\isachardot}split} and
|
|
571 |
$t$\isa{{\isachardot}split{\isacharunderscore}asm}. Analogously, there is \isa{if{\isacharunderscore}splits}.
|
|
572 |
|
|
573 |
\begin{warn}
|
|
574 |
The simplifier merely simplifies the condition of an
|
|
575 |
\isa{if}\index{*if expressions!simplification of} but not the
|
|
576 |
\isa{then} or \isa{else} parts. The latter are simplified only after the
|
|
577 |
condition reduces to \isa{True} or \isa{False}, or after splitting. The
|
|
578 |
same is true for \sdx{case}-expressions: only the selector is
|
|
579 |
simplified at first, until either the expression reduces to one of the
|
|
580 |
cases or it is split.
|
|
581 |
\end{warn}%
|
|
582 |
\end{isamarkuptxt}%
|
17175
|
583 |
\isamarkuptrue%
|
17056
|
584 |
%
|
|
585 |
\endisatagproof
|
|
586 |
{\isafoldproof}%
|
|
587 |
%
|
|
588 |
\isadelimproof
|
|
589 |
%
|
|
590 |
\endisadelimproof
|
9933
|
591 |
%
|
11214
|
592 |
\isamarkupsubsection{Tracing%
|
10397
|
593 |
}
|
11866
|
594 |
\isamarkuptrue%
|
9933
|
595 |
%
|
|
596 |
\begin{isamarkuptext}%
|
|
597 |
\indexbold{tracing the simplifier}
|
|
598 |
Using the simplifier effectively may take a bit of experimentation. Set the
|
16523
|
599 |
Proof General flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgmenu{Trace Simplifier} to get a better idea of what is going on:%
|
9933
|
600 |
\end{isamarkuptext}%
|
17175
|
601 |
\isamarkuptrue%
|
|
602 |
\isacommand{lemma}\isamarkupfalse%
|
|
603 |
\ {\isachardoublequoteopen}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
|
17056
|
604 |
%
|
|
605 |
\isadelimproof
|
|
606 |
%
|
|
607 |
\endisadelimproof
|
|
608 |
%
|
|
609 |
\isatagproof
|
17175
|
610 |
\isacommand{apply}\isamarkupfalse%
|
17181
|
611 |
{\isacharparenleft}simp{\isacharparenright}%
|
17056
|
612 |
\endisatagproof
|
|
613 |
{\isafoldproof}%
|
|
614 |
%
|
|
615 |
\isadelimproof
|
|
616 |
%
|
|
617 |
\endisadelimproof
|
11866
|
618 |
%
|
9933
|
619 |
\begin{isamarkuptext}%
|
|
620 |
\noindent
|
16523
|
621 |
produces the following trace in Proof General's \pgmenu{Trace} buffer:
|
9933
|
622 |
|
|
623 |
\begin{ttbox}\makeatother
|
16519
|
624 |
[1]Applying instance of rewrite rule "List.rev.simps_2":
|
16359
|
625 |
rev (?x1 # ?xs1) \(\equiv\) rev ?xs1 @ [?x1]
|
|
626 |
|
16519
|
627 |
[1]Rewriting:
|
16359
|
628 |
rev [a] \(\equiv\) rev [] @ [a]
|
|
629 |
|
16519
|
630 |
[1]Applying instance of rewrite rule "List.rev.simps_1":
|
16359
|
631 |
rev [] \(\equiv\) []
|
|
632 |
|
16519
|
633 |
[1]Rewriting:
|
16359
|
634 |
rev [] \(\equiv\) []
|
|
635 |
|
16519
|
636 |
[1]Applying instance of rewrite rule "List.op @.append_Nil":
|
16359
|
637 |
[] @ ?y \(\equiv\) ?y
|
|
638 |
|
16519
|
639 |
[1]Rewriting:
|
16359
|
640 |
[] @ [a] \(\equiv\) [a]
|
|
641 |
|
16519
|
642 |
[1]Applying instance of rewrite rule
|
16359
|
643 |
?x2 # ?t1 = ?t1 \(\equiv\) False
|
|
644 |
|
16519
|
645 |
[1]Rewriting:
|
16359
|
646 |
[a] = [] \(\equiv\) False
|
9933
|
647 |
\end{ttbox}
|
16359
|
648 |
The trace lists each rule being applied, both in its general form and
|
|
649 |
the instance being used. The \texttt{[}$i$\texttt{]} in front (where
|
16519
|
650 |
above $i$ is always \texttt{1}) indicates that we are inside the $i$th
|
|
651 |
invocation of the simplifier. Each attempt to apply a
|
16359
|
652 |
conditional rule shows the rule followed by the trace of the
|
|
653 |
(recursive!) simplification of the conditions, the latter prefixed by
|
|
654 |
\texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}.
|
|
655 |
Another source of recursive invocations of the simplifier are
|
|
656 |
proofs of arithmetic formulae.
|
9933
|
657 |
|
16359
|
658 |
Many other hints about the simplifier's actions may appear.
|
11309
|
659 |
|
16359
|
660 |
In more complicated cases, the trace can be very lengthy. Thus it is
|
16523
|
661 |
advisable to reset the \pgmenu{Trace Simplifier} flag after having
|
16359
|
662 |
obtained the desired trace.%
|
9933
|
663 |
\end{isamarkuptext}%
|
11866
|
664 |
\isamarkuptrue%
|
16519
|
665 |
%
|
16545
|
666 |
\isamarkupsubsection{Finding Theorems\label{sec:find}%
|
16519
|
667 |
}
|
|
668 |
\isamarkuptrue%
|
|
669 |
%
|
|
670 |
\begin{isamarkuptext}%
|
16523
|
671 |
\indexbold{finding theorems}\indexbold{searching theorems}
|
16560
|
672 |
Isabelle's large database of proved theorems
|
|
673 |
offers a powerful search engine. Its chief limitation is
|
16519
|
674 |
its restriction to the theories currently loaded.
|
|
675 |
|
|
676 |
\begin{pgnote}
|
16523
|
677 |
The search engine is started by clicking on Proof General's \pgmenu{Find} icon.
|
16519
|
678 |
You specify your search textually in the input buffer at the bottom
|
|
679 |
of the window.
|
|
680 |
\end{pgnote}
|
|
681 |
|
16560
|
682 |
The simplest form of search finds theorems containing specified
|
|
683 |
patterns. A pattern can be any term (even
|
|
684 |
a single identifier). It may contain ``\texttt{\_}'', a wildcard standing
|
|
685 |
for any term. Here are some
|
16519
|
686 |
examples:
|
|
687 |
\begin{ttbox}
|
|
688 |
length
|
|
689 |
"_ # _ = _ # _"
|
|
690 |
"_ + _"
|
|
691 |
"_ * (_ - (_::nat))"
|
|
692 |
\end{ttbox}
|
16560
|
693 |
Specifying types, as shown in the last example,
|
|
694 |
constrains searches involving overloaded operators.
|
16519
|
695 |
|
|
696 |
\begin{warn}
|
|
697 |
Always use ``\texttt{\_}'' rather than variable names: searching for
|
|
698 |
\texttt{"x + y"} will usually not find any matching theorems
|
16560
|
699 |
because they would need to contain \texttt{x} and~\texttt{y} literally.
|
|
700 |
When searching for infix operators, do not just type in the symbol,
|
|
701 |
such as~\texttt{+}, but a proper term such as \texttt{"_ + _"}.
|
|
702 |
This remark applies to more complicated syntaxes, too.
|
16519
|
703 |
\end{warn}
|
|
704 |
|
16560
|
705 |
If you are looking for rewrite rules (possibly conditional) that could
|
|
706 |
simplify some term, prefix the pattern with \texttt{simp:}.
|
16519
|
707 |
\begin{ttbox}
|
|
708 |
simp: "_ * (_ + _)"
|
|
709 |
\end{ttbox}
|
16560
|
710 |
This finds \emph{all} equations---not just those with a \isa{simp} attribute---whose conclusion has the form
|
16519
|
711 |
\begin{isabelle}%
|
|
712 |
\ \ \ \ \ {\isacharunderscore}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}\ {\isacharplus}\ {\isacharunderscore}{\isacharparenright}\ {\isacharequal}\ {\isasymdots}%
|
|
713 |
\end{isabelle}
|
16560
|
714 |
It only finds equations that can simplify the given pattern
|
|
715 |
at the root, not somewhere inside: for example, equations of the form
|
|
716 |
\isa{{\isacharunderscore}\ {\isacharplus}\ {\isacharunderscore}\ {\isacharequal}\ {\isasymdots}} do not match.
|
16519
|
717 |
|
16560
|
718 |
You may also search for theorems by name---you merely
|
|
719 |
need to specify a substring. For example, you could search for all
|
16519
|
720 |
commutativity theorems like this:
|
|
721 |
\begin{ttbox}
|
|
722 |
name: comm
|
|
723 |
\end{ttbox}
|
|
724 |
This retrieves all theorems whose name contains \texttt{comm}.
|
|
725 |
|
16560
|
726 |
Search criteria can also be negated by prefixing them with ``\texttt{-}''.
|
|
727 |
For example,
|
16519
|
728 |
\begin{ttbox}
|
16523
|
729 |
-name: List
|
16519
|
730 |
\end{ttbox}
|
16560
|
731 |
finds theorems whose name does not contain \texttt{List}. You can use this
|
|
732 |
to exclude particular theories from the search: the long name of
|
16519
|
733 |
a theorem contains the name of the theory it comes from.
|
|
734 |
|
16560
|
735 |
Finallly, different search criteria can be combined arbitrarily.
|
20144
|
736 |
The effect is conjuctive: Find returns the theorems that satisfy all of
|
16560
|
737 |
the criteria. For example,
|
16519
|
738 |
\begin{ttbox}
|
|
739 |
"_ + _" -"_ - _" -simp: "_ * (_ + _)" name: assoc
|
|
740 |
\end{ttbox}
|
16560
|
741 |
looks for theorems containing plus but not minus, and which do not simplify
|
|
742 |
\mbox{\isa{{\isacharunderscore}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}\ {\isacharplus}\ {\isacharunderscore}{\isacharparenright}}} at the root, and whose name contains \texttt{assoc}.
|
16523
|
743 |
|
16545
|
744 |
Further search criteria are explained in \S\ref{sec:find2}.
|
16519
|
745 |
|
16523
|
746 |
\begin{pgnote}
|
|
747 |
Proof General keeps a history of all your search expressions.
|
|
748 |
If you click on \pgmenu{Find}, you can use the arrow keys to scroll
|
|
749 |
through previous searches and just modify them. This saves you having
|
|
750 |
to type in lengthy expressions again and again.
|
|
751 |
\end{pgnote}%
|
16519
|
752 |
\end{isamarkuptext}%
|
17175
|
753 |
\isamarkuptrue%
|
17056
|
754 |
%
|
|
755 |
\isadelimtheory
|
|
756 |
%
|
|
757 |
\endisadelimtheory
|
|
758 |
%
|
|
759 |
\isatagtheory
|
|
760 |
%
|
|
761 |
\endisatagtheory
|
|
762 |
{\isafoldtheory}%
|
|
763 |
%
|
|
764 |
\isadelimtheory
|
|
765 |
%
|
|
766 |
\endisadelimtheory
|
9924
|
767 |
\end{isabellebody}%
|
|
768 |
%%% Local Variables:
|
|
769 |
%%% mode: latex
|
|
770 |
%%% TeX-master: "root"
|
|
771 |
%%% End:
|