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