7135
|
1 |
|
7167
|
2 |
\chapter{Generic Tools and Packages}\label{ch:gen-tools}
|
|
3 |
|
7315
|
4 |
\section{Basic proof methods}\label{sec:pure-meth}
|
7167
|
5 |
|
|
6 |
\indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption}
|
7458
|
7 |
\indexisarmeth{fold}\indexisarmeth{unfold}
|
7167
|
8 |
\indexisarmeth{rule}\indexisarmeth{erule}
|
|
9 |
\begin{matharray}{rcl}
|
|
10 |
- & : & \isarmeth \\
|
|
11 |
assumption & : & \isarmeth \\
|
7321
|
12 |
rule & : & \isarmeth \\
|
|
13 |
erule^* & : & \isarmeth \\[0.5ex]
|
7167
|
14 |
fold & : & \isarmeth \\
|
7321
|
15 |
unfold & : & \isarmeth \\[0.5ex]
|
7335
|
16 |
succeed & : & \isarmeth \\
|
7321
|
17 |
fail & : & \isarmeth \\
|
7167
|
18 |
\end{matharray}
|
|
19 |
|
|
20 |
\begin{rail}
|
|
21 |
('fold' | 'unfold' | 'rule' | 'erule') thmrefs
|
|
22 |
;
|
|
23 |
\end{rail}
|
|
24 |
|
|
25 |
\begin{descr}
|
7321
|
26 |
\item [``$-$''] does nothing but insert the forward chaining facts as premises
|
7335
|
27 |
into the goal. Note that command $\PROOFNAME$ without any method actually
|
|
28 |
performs a single reduction step using the $rule$ method (see below); thus a
|
|
29 |
plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than
|
|
30 |
$\PROOFNAME$ alone.
|
7466
|
31 |
\item [$assumption$] solves some goal by assumption. Any facts given are
|
7897
|
32 |
guaranteed to participate in the refinement. Note that ``$\DOT$'' (dot)
|
|
33 |
abbreviates $\BY{assumption}$.
|
7321
|
34 |
\item [$rule~thms$] applies some rule given as argument in backward manner;
|
|
35 |
facts are used to reduce the rule before applying it to the goal. Thus
|
|
36 |
$rule$ without facts is plain \emph{introduction}, while with facts it
|
7897
|
37 |
becomes a (generalized) \emph{elimination}.
|
7321
|
38 |
|
|
39 |
Note that the classical reasoner introduces another version of $rule$ that
|
|
40 |
is able to pick appropriate rules automatically, whenever explicit $thms$
|
7335
|
41 |
are omitted (see \S\ref{sec:classical-basic}); that method is the default
|
7897
|
42 |
for $\PROOFNAME$ steps. Note that ``$\DDOT$'' (double-dot) abbreviates
|
|
43 |
$\BY{default}$.
|
7321
|
44 |
\item [$erule~thms$] is similar to $rule$, but applies rules by
|
|
45 |
elim-resolution. This is an improper method, mainly for experimentation and
|
7335
|
46 |
porting of old scripts. Actual elimination proofs are usually done with
|
7897
|
47 |
$rule$ (single step, involving facts) or $elim$ (repeated steps, see
|
7321
|
48 |
\S\ref{sec:classical-basic}).
|
7335
|
49 |
\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
|
7526
|
50 |
meta-level definitions throughout all goals; any facts provided are
|
|
51 |
\emph{ignored}.
|
7335
|
52 |
\item [$succeed$] yields a single (unchanged) result; it is the identify of
|
7897
|
53 |
the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
|
7321
|
54 |
\item [$fail$] yields an empty result sequence; it is the identify of the
|
7897
|
55 |
``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
|
7321
|
56 |
\end{descr}
|
7167
|
57 |
|
7315
|
58 |
|
|
59 |
\section{Miscellaneous attributes}
|
|
60 |
|
7167
|
61 |
\indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}
|
|
62 |
\indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}
|
|
63 |
\indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
|
|
64 |
\begin{matharray}{rcl}
|
|
65 |
tag & : & \isaratt \\
|
7321
|
66 |
untag & : & \isaratt \\[0.5ex]
|
|
67 |
OF & : & \isaratt \\
|
7167
|
68 |
RS & : & \isaratt \\
|
7321
|
69 |
COMP & : & \isaratt \\[0.5ex]
|
7335
|
70 |
of & : & \isaratt \\
|
|
71 |
where & : & \isaratt \\[0.5ex]
|
7167
|
72 |
standard & : & \isaratt \\
|
|
73 |
elimify & : & \isaratt \\
|
7335
|
74 |
export^* & : & \isaratt \\
|
7167
|
75 |
transfer & : & \isaratt \\
|
|
76 |
\end{matharray}
|
|
77 |
|
|
78 |
\begin{rail}
|
|
79 |
('tag' | 'untag') (nameref+)
|
|
80 |
;
|
|
81 |
'OF' thmrefs
|
|
82 |
;
|
7321
|
83 |
('RS' | 'COMP') nat? thmref
|
7167
|
84 |
;
|
7175
|
85 |
'of' (inst * ) ('concl' ':' (inst * ))?
|
7167
|
86 |
;
|
7321
|
87 |
'where' (name '=' term * 'and')
|
|
88 |
;
|
7167
|
89 |
|
|
90 |
inst: underscore | term
|
|
91 |
;
|
|
92 |
\end{rail}
|
|
93 |
|
|
94 |
\begin{descr}
|
7897
|
95 |
\item [$tag~tags$ and $untag~tags$] add and remove $tags$ of the theorem,
|
7321
|
96 |
respectively. Tags may be any list of strings that serve as comment for
|
7897
|
97 |
some tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
|
7321
|
98 |
result).
|
|
99 |
\item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules. $OF$ applies
|
|
100 |
$thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
|
7396
|
101 |
the reversed order). Note that premises may be skipped by including $\_$
|
|
102 |
(underscore) as argument.
|
|
103 |
|
|
104 |
$RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$
|
|
105 |
that does not include the automatic lifting process that is normally
|
7897
|
106 |
intended (cf.\ \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}).
|
7321
|
107 |
|
7466
|
108 |
\item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named
|
7335
|
109 |
instantiation, respectively. The terms given in $of$ are substituted for
|
|
110 |
any schematic variables occurring in a theorem from left to right;
|
|
111 |
``\texttt{_}'' (underscore) indicates to skip a position.
|
7321
|
112 |
|
|
113 |
\item [$standard$] puts a theorem into the standard form of object-rules, just
|
|
114 |
as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
|
|
115 |
|
7897
|
116 |
\item [$elimify$] turns an destruction rule into an elimination, just as the
|
|
117 |
ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
|
7321
|
118 |
|
|
119 |
\item [$export$] lifts a local result out of the current proof context,
|
7335
|
120 |
generalizing all fixed variables and discharging all assumptions. Note that
|
|
121 |
(partial) export is usually done automatically behind the scenes. This
|
|
122 |
attribute is mainly for experimentation.
|
7321
|
123 |
|
|
124 |
\item [$transfer$] promotes a theorem to the current theory context, which has
|
|
125 |
to enclose the former one. Normally, this is done automatically when rules
|
|
126 |
are joined by inference.
|
|
127 |
|
7167
|
128 |
\end{descr}
|
|
129 |
|
7315
|
130 |
|
|
131 |
\section{Calculational proof}\label{sec:calculation}
|
|
132 |
|
|
133 |
\indexisarcmd{also}\indexisarcmd{finally}\indexisaratt{trans}
|
|
134 |
\begin{matharray}{rcl}
|
|
135 |
\isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
136 |
\isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
|
|
137 |
trans & : & \isaratt \\
|
|
138 |
\end{matharray}
|
|
139 |
|
|
140 |
Calculational proof is forward reasoning with implicit application of
|
|
141 |
transitivity rules (such those of $=$, $\le$, $<$). Isabelle/Isar maintains
|
7391
|
142 |
an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
|
7897
|
143 |
results obtained by transitivity composed with the current result. Command
|
|
144 |
$\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the
|
|
145 |
final $calculation$ by forward chaining towards the next goal statement. Both
|
|
146 |
commands require valid current facts, i.e.\ may occur only after commands that
|
|
147 |
produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of
|
|
148 |
$\HAVENAME$, $\SHOWNAME$ etc.
|
7315
|
149 |
|
|
150 |
Also note that the automatic term abbreviation ``$\dots$'' has its canonical
|
|
151 |
application with calculational proofs. It automatically refers to the
|
|
152 |
argument\footnote{The argument of a curried infix expression is its right-hand
|
|
153 |
side.} of the preceding statement.
|
|
154 |
|
|
155 |
Isabelle/Isar calculations are implicitly subject to block structure in the
|
|
156 |
sense that new threads of calculational reasoning are commenced for any new
|
|
157 |
block (as opened by a local goal, for example). This means that, apart from
|
|
158 |
being able to nest calculations, there is no separate \emph{begin-calculation}
|
|
159 |
command required.
|
|
160 |
|
|
161 |
\begin{rail}
|
|
162 |
('also' | 'finally') transrules? comment?
|
|
163 |
;
|
|
164 |
'trans' (() | 'add' ':' | 'del' ':') thmrefs
|
|
165 |
;
|
|
166 |
|
|
167 |
transrules: '(' thmrefs ')' interest?
|
|
168 |
;
|
|
169 |
\end{rail}
|
|
170 |
|
|
171 |
\begin{descr}
|
|
172 |
\item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as
|
|
173 |
follows. The first occurrence of $\ALSO$ in some calculational thread
|
7458
|
174 |
initialises $calculation$ by $this$. Any subsequent $\ALSO$ on the same
|
7335
|
175 |
level of block-structure updates $calculation$ by some transitivity rule
|
7458
|
176 |
applied to $calculation$ and $this$ (in that order). Transitivity rules are
|
|
177 |
picked from the current context plus those given as $thms$ (the latter have
|
|
178 |
precedence).
|
7315
|
179 |
|
|
180 |
\item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
|
|
181 |
$\ALSO$, and concludes the current calculational thread. The final result
|
|
182 |
is exhibited as fact for forward chaining towards the next goal. Basically,
|
7897
|
183 |
$\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Typical proof
|
|
184 |
idioms are``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
|
|
185 |
``$\FINALLY~\HAVE{}{\phi}~\DOT$''.
|
7315
|
186 |
|
7335
|
187 |
\item [$trans$] maintains the set of transitivity rules of the theory or proof
|
|
188 |
context, by adding or deleting theorems (the default is to add).
|
7315
|
189 |
\end{descr}
|
|
190 |
|
7897
|
191 |
%FIXME
|
|
192 |
%See theory \texttt{HOL/Isar_examples/Group} for a simple application of
|
|
193 |
%calculations for basic equational reasoning.
|
|
194 |
%\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced
|
|
195 |
%calculational steps in combination with natural deduction.
|
7315
|
196 |
|
|
197 |
|
7135
|
198 |
\section{Axiomatic Type Classes}\label{sec:axclass}
|
|
199 |
|
7356
|
200 |
\indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}
|
7135
|
201 |
\begin{matharray}{rcl}
|
|
202 |
\isarcmd{axclass} & : & \isartrans{theory}{theory} \\
|
|
203 |
\isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
|
7356
|
204 |
intro_classes & : & \isarmeth \\
|
7135
|
205 |
\end{matharray}
|
|
206 |
|
|
207 |
Axiomatic type classes are provided by Isabelle/Pure as a purely
|
|
208 |
\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}). Thus
|
|
209 |
any object logic may make use of this light-weight mechanism for abstract
|
|
210 |
theories. See \cite{Wenzel:1997:TPHOL} for more information. There is also a
|
|
211 |
tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of
|
|
212 |
the standard Isabelle documentation.
|
7335
|
213 |
%FIXME cite
|
7135
|
214 |
|
|
215 |
\begin{rail}
|
|
216 |
'axclass' classdecl (axmdecl prop comment? +)
|
|
217 |
;
|
|
218 |
'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
|
|
219 |
;
|
|
220 |
\end{rail}
|
|
221 |
|
7167
|
222 |
\begin{descr}
|
7335
|
223 |
\item [$\isarkeyword{axclass}~c < \vec c~axms$] defines an axiomatic type
|
|
224 |
class as the intersection of existing classes, with additional axioms
|
|
225 |
holding. Class axioms may not contain more than one type variable. The
|
|
226 |
class axioms (with implicit sort constraints added) are bound to the given
|
|
227 |
names. Furthermore a class introduction rule is generated, which is
|
7356
|
228 |
employed by method $intro_classes$ in support instantiation proofs of this
|
7335
|
229 |
class.
|
|
230 |
|
|
231 |
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::
|
|
232 |
(\vec s)c$] setup up a goal stating the class relation or type arity. The
|
7356
|
233 |
proof would usually proceed by the $intro_classes$ method, and then
|
7335
|
234 |
establish the characteristic theorems of the type classes involved. After
|
|
235 |
finishing the proof the theory will be augmented by a type signature
|
|
236 |
declaration corresponding to the resulting theorem.
|
7897
|
237 |
\item [$intro_classes$] repeatedly expands the class introduction rules of
|
7466
|
238 |
this theory.
|
7167
|
239 |
\end{descr}
|
7135
|
240 |
|
7319
|
241 |
See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
|
|
242 |
axiomatic type classes, including instantiation proofs.
|
7135
|
243 |
|
|
244 |
|
|
245 |
\section{The Simplifier}
|
|
246 |
|
7321
|
247 |
\subsection{Simplification methods}\label{sec:simp}
|
7315
|
248 |
|
7897
|
249 |
\indexisarmeth{simp}
|
7315
|
250 |
\begin{matharray}{rcl}
|
|
251 |
simp & : & \isarmeth \\
|
|
252 |
\end{matharray}
|
|
253 |
|
|
254 |
\begin{rail}
|
7897
|
255 |
'simp' (simpmod * )
|
7315
|
256 |
;
|
|
257 |
|
|
258 |
simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
|
|
259 |
;
|
|
260 |
\end{rail}
|
|
261 |
|
7321
|
262 |
\begin{descr}
|
7897
|
263 |
\item [$simp$] invokes Isabelle's simplifier, after modifying the context by
|
|
264 |
adding or deleting rules as specified. The \railtoken{only} modifier first
|
|
265 |
removes all other rewrite rules and congruences, and then is like
|
|
266 |
\railtoken{add}. In contrast, \railtoken{other} ignores its arguments;
|
7466
|
267 |
nevertheless there may be side-effects on the context via attributes. This
|
|
268 |
provides a back door for arbitrary context manipulation.
|
7321
|
269 |
|
7897
|
270 |
The $simp$ method is based on \texttt{asm_full_simp_tac} (see also
|
|
271 |
\cite[\S10]{isabelle-ref}), but is much better behaved in practice. Only
|
|
272 |
the local premises of the actual goal are involved by default. Additional
|
|
273 |
facts may be insert via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).
|
|
274 |
The full context of assumptions is
|
|
275 |
|
|
276 |
; $simp$ removes any premises of the goal, before
|
7466
|
277 |
inserting the goal facts; $asm_simp$ leaves the premises. Thus $asm_simp$
|
|
278 |
may refer to premises that are not explicitly spelled out, potentially
|
|
279 |
obscuring the reasoning. The plain $simp$ method is more faithful in the
|
|
280 |
sense that, apart from the rewrite rules of the current context, \emph{at
|
|
281 |
most} the explicitly provided facts may participate in the simplification.
|
7321
|
282 |
\end{descr}
|
|
283 |
|
|
284 |
\subsection{Modifying the context}
|
|
285 |
|
|
286 |
\indexisaratt{simp}
|
|
287 |
\begin{matharray}{rcl}
|
|
288 |
simp & : & \isaratt \\
|
|
289 |
\end{matharray}
|
|
290 |
|
|
291 |
\begin{rail}
|
|
292 |
'simp' (() | 'add' | 'del')
|
|
293 |
;
|
|
294 |
\end{rail}
|
|
295 |
|
|
296 |
\begin{descr}
|
7466
|
297 |
\item [$simp$] adds or deletes rules from the theory or proof context (the
|
|
298 |
default is to add).
|
7321
|
299 |
\end{descr}
|
7319
|
300 |
|
7315
|
301 |
|
|
302 |
\subsection{Forward simplification}
|
|
303 |
|
7391
|
304 |
\indexisaratt{simplify}\indexisaratt{asm-simplify}
|
|
305 |
\indexisaratt{full-simplify}\indexisaratt{asm-full-simplify}
|
7315
|
306 |
\begin{matharray}{rcl}
|
|
307 |
simplify & : & \isaratt \\
|
|
308 |
asm_simplify & : & \isaratt \\
|
|
309 |
full_simplify & : & \isaratt \\
|
|
310 |
asm_full_simplify & : & \isaratt \\
|
|
311 |
\end{matharray}
|
|
312 |
|
7321
|
313 |
These attributes provide forward rules for simplification, which should be
|
7335
|
314 |
used only very rarely. See the ML functions of the same name in
|
7321
|
315 |
\cite[\S10]{isabelle-ref} for more information.
|
7315
|
316 |
|
|
317 |
|
7135
|
318 |
\section{The Classical Reasoner}
|
|
319 |
|
7335
|
320 |
\subsection{Basic methods}\label{sec:classical-basic}
|
7321
|
321 |
|
|
322 |
\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
|
|
323 |
\begin{matharray}{rcl}
|
|
324 |
rule & : & \isarmeth \\
|
|
325 |
intro & : & \isarmeth \\
|
|
326 |
elim & : & \isarmeth \\
|
|
327 |
contradiction & : & \isarmeth \\
|
|
328 |
\end{matharray}
|
|
329 |
|
|
330 |
\begin{rail}
|
|
331 |
('rule' | 'intro' | 'elim') thmrefs
|
|
332 |
;
|
|
333 |
\end{rail}
|
|
334 |
|
|
335 |
\begin{descr}
|
7466
|
336 |
\item [$rule$] as offered by the classical reasoner is a refinement over the
|
|
337 |
primitive one (see \S\ref{sec:pure-meth}). In the case that no rules are
|
|
338 |
provided as arguments, it automatically determines elimination and
|
7321
|
339 |
introduction rules from the context (see also \S\ref{sec:classical-mod}).
|
7335
|
340 |
In that form it is the default method for basic proof steps, such as
|
|
341 |
$\PROOFNAME$ and ``$\DDOT$'' (two dots).
|
7321
|
342 |
|
7466
|
343 |
\item [$intro$ and $elim$] repeatedly refine some goal by intro- or
|
7321
|
344 |
elim-resolution, after having inserted the facts. Omitting the arguments
|
|
345 |
refers to any suitable rules from the context, otherwise only the explicitly
|
7335
|
346 |
given ones may be applied. The latter form admits better control of what
|
|
347 |
actually happens, thus it is very appropriate as an initial method for
|
|
348 |
$\PROOFNAME$ that splits up certain connectives of the goal, before entering
|
|
349 |
the sub-proof.
|
7458
|
350 |
|
7466
|
351 |
\item [$contradiction$] solves some goal by contradiction, deriving any result
|
|
352 |
from both $\neg A$ and $A$. Facts, which are guaranteed to participate, may
|
|
353 |
appear in either order.
|
7321
|
354 |
\end{descr}
|
|
355 |
|
|
356 |
|
|
357 |
\subsection{Automatic methods}\label{sec:classical-auto}
|
7315
|
358 |
|
7321
|
359 |
\indexisarmeth{blast}
|
7391
|
360 |
\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow-best}
|
7321
|
361 |
\begin{matharray}{rcl}
|
|
362 |
blast & : & \isarmeth \\
|
|
363 |
fast & : & \isarmeth \\
|
|
364 |
best & : & \isarmeth \\
|
|
365 |
slow & : & \isarmeth \\
|
|
366 |
slow_best & : & \isarmeth \\
|
|
367 |
\end{matharray}
|
|
368 |
|
|
369 |
\railalias{slowbest}{slow\_best}
|
|
370 |
\railterm{slowbest}
|
|
371 |
|
|
372 |
\begin{rail}
|
|
373 |
'blast' nat? (clamod * )
|
|
374 |
;
|
|
375 |
('fast' | 'best' | 'slow' | slowbest) (clamod * )
|
|
376 |
;
|
|
377 |
|
|
378 |
clamod: (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del') ':' thmrefs
|
|
379 |
;
|
|
380 |
\end{rail}
|
|
381 |
|
|
382 |
\begin{descr}
|
|
383 |
\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
|
7335
|
384 |
in \cite[\S11]{isabelle-ref}). The optional argument specifies a
|
7321
|
385 |
user-supplied search bound (default 20).
|
|
386 |
\item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical
|
7335
|
387 |
reasoner (see \cite[\S11]{isabelle-ref}, tactic \texttt{fast_tac} etc).
|
7321
|
388 |
\end{descr}
|
|
389 |
|
|
390 |
Any of above methods support additional modifiers of the context of classical
|
|
391 |
rules. There semantics is analogous to the attributes given in
|
|
392 |
\S\ref{sec:classical-mod}.
|
|
393 |
|
7315
|
394 |
|
|
395 |
\subsection{Combined automatic methods}
|
|
396 |
|
7321
|
397 |
\indexisarmeth{auto}\indexisarmeth{force}
|
|
398 |
\begin{matharray}{rcl}
|
|
399 |
force & : & \isarmeth \\
|
|
400 |
auto & : & \isarmeth \\
|
|
401 |
\end{matharray}
|
|
402 |
|
|
403 |
\begin{rail}
|
|
404 |
('force' | 'auto') (clasimpmod * )
|
|
405 |
;
|
7315
|
406 |
|
7321
|
407 |
clasimpmod: ('simp' ('add' | 'del' | 'only') | other |
|
|
408 |
(('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs
|
|
409 |
\end{rail}
|
7315
|
410 |
|
7321
|
411 |
\begin{descr}
|
|
412 |
\item [$force$ and $auto$] provide access to Isabelle's combined
|
|
413 |
simplification and classical reasoning tactics. See \texttt{force_tac} and
|
|
414 |
\texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information. The
|
|
415 |
modifier arguments correspond to those given in \S\ref{sec:simp} and
|
7335
|
416 |
\S\ref{sec:classical-auto}. Note that the ones related to the Simplifier
|
|
417 |
are prefixed by \railtoken{simp} here.
|
7321
|
418 |
\end{descr}
|
|
419 |
|
|
420 |
\subsection{Modifying the context}\label{sec:classical-mod}
|
7135
|
421 |
|
7391
|
422 |
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
|
|
423 |
\indexisaratt{iff}\indexisaratt{delrule}
|
7321
|
424 |
\begin{matharray}{rcl}
|
|
425 |
intro & : & \isaratt \\
|
|
426 |
elim & : & \isaratt \\
|
|
427 |
dest & : & \isaratt \\
|
7391
|
428 |
iff & : & \isaratt \\
|
7321
|
429 |
delrule & : & \isaratt \\
|
|
430 |
\end{matharray}
|
7135
|
431 |
|
7321
|
432 |
\begin{rail}
|
|
433 |
('intro' | 'elim' | 'dest') (() | '!' | '!!')
|
|
434 |
;
|
|
435 |
\end{rail}
|
7135
|
436 |
|
7321
|
437 |
\begin{descr}
|
7335
|
438 |
\item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,
|
|
439 |
respectively. By default, rules are considered as \emph{safe}, while a
|
|
440 |
single ``!'' classifies as \emph{unsafe}, and ``!!'' as \emph{extra} (i.e.\
|
7466
|
441 |
not applied in the search-oriented automatic methods, but only $rule$).
|
7335
|
442 |
|
7391
|
443 |
\item [$iff$] declares equations both as rewrite rules for the simplifier and
|
|
444 |
classical reasoning rules.
|
|
445 |
|
7335
|
446 |
\item [$delrule$] deletes introduction or elimination rules from the context.
|
|
447 |
Note that destruction rules would have to be turned into elimination rules
|
7321
|
448 |
first, e.g.\ by using the $elimify$ attribute.
|
|
449 |
\end{descr}
|
7135
|
450 |
|
|
451 |
|
|
452 |
%%% Local Variables:
|
|
453 |
%%% mode: latex
|
|
454 |
%%% TeX-master: "isar-ref"
|
|
455 |
%%% End:
|