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