author  wenzelm 
Mon, 27 Mar 2000 18:10:11 +0200  
changeset 8594  d2e2a3df6871 
parent 8547  93b8685d004b 
child 8619  63a0e1502e41 
permissions  rwrr 
7135  1 

7167  2 
\chapter{Generic Tools and Packages}\label{ch:gentools} 
3 

8517  4 
\section{Axiomatic Type Classes}\label{sec:axclass} 
7167  5 

8517  6 
\indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{introclasses} 
7167  7 
\begin{matharray}{rcl} 
8517  8 
\isarcmd{axclass} & : & \isartrans{theory}{theory} \\ 
9 
\isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\ 

10 
intro_classes & : & \isarmeth \\ 

7167  11 
\end{matharray} 
12 

8517  13 
Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional} 
14 
interface to type classes (cf.~\S\ref{sec:classes}). Thus any object logic 

8547  15 
may make use of this lightweight mechanism of abstract theories 
16 
\cite{Wenzel:1997:TPHOL}. There is also a tutorial on \emph{Using Axiomatic 

17 
Type Classes in Isabelle} that is part of the standard Isabelle 

18 
documentation. 

8517  19 
%FIXME cite 
20 

7167  21 
\begin{rail} 
8517  22 
'axclass' classdecl (axmdecl prop comment? +) 
23 
; 

24 
'instance' (nameref '<' nameref  nameref '::' simplearity) comment? 

7167  25 
; 
26 
\end{rail} 

27 

28 
\begin{descr} 

8517  29 
\item [$\isarkeyword{axclass}~c < \vec c~axms$] defines an axiomatic type 
30 
class as the intersection of existing classes, with additional axioms 

31 
holding. Class axioms may not contain more than one type variable. The 

32 
class axioms (with implicit sort constraints added) are bound to the given 

33 
names. Furthermore a class introduction rule is generated, which is 

34 
employed by method $intro_classes$ to support instantiation proofs of this 

35 
class. 

7321  36 

8517  37 
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t :: 
8547  38 
(\vec s)c$] setup a goal stating a class relation or type arity. The proof 
39 
would usually proceed by $intro_classes$, and then establish the 

8517  40 
characteristic theorems of the type classes involved. After finishing the 
41 
proof, the theory will be augmented by a type signature declaration 

42 
corresponding to the resulting theorem. 

43 
\item [$intro_classes$] repeatedly expands all class introduction rules of 

44 
this theory. 

7167  45 
\end{descr} 
46 

7315  47 

48 
\section{Calculational proof}\label{sec:calculation} 

49 

50 
\indexisarcmd{also}\indexisarcmd{finally}\indexisaratt{trans} 

51 
\begin{matharray}{rcl} 

52 
\isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\ 

53 
\isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\ 

54 
trans & : & \isaratt \\ 

55 
\end{matharray} 

56 

57 
Calculational proof is forward reasoning with implicit application of 

58 
transitivity rules (such those of $=$, $\le$, $<$). Isabelle/Isar maintains 

7391  59 
an auxiliary register $calculation$\indexisarthm{calculation} for accumulating 
7897  60 
results obtained by transitivity composed with the current result. Command 
61 
$\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the 

62 
final $calculation$ by forward chaining towards the next goal statement. Both 

63 
commands require valid current facts, i.e.\ may occur only after commands that 

64 
produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of 

65 
$\HAVENAME$, $\SHOWNAME$ etc. 

7315  66 

67 
Also note that the automatic term abbreviation ``$\dots$'' has its canonical 

68 
application with calculational proofs. It automatically refers to the 

69 
argument\footnote{The argument of a curried infix expression is its righthand 

70 
side.} of the preceding statement. 

71 

72 
Isabelle/Isar calculations are implicitly subject to block structure in the 

73 
sense that new threads of calculational reasoning are commenced for any new 

74 
block (as opened by a local goal, for example). This means that, apart from 

75 
being able to nest calculations, there is no separate \emph{begincalculation} 

76 
command required. 

77 

78 
\begin{rail} 

79 
('also'  'finally') transrules? comment? 

80 
; 

8507  81 
'trans' (()  'add'  'del') 
7315  82 
; 
83 

84 
transrules: '(' thmrefs ')' interest? 

85 
; 

86 
\end{rail} 

87 

88 
\begin{descr} 

8547  89 
\item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as 
7315  90 
follows. The first occurrence of $\ALSO$ in some calculational thread 
7905  91 
initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same 
7335  92 
level of blockstructure updates $calculation$ by some transitivity rule 
7458  93 
applied to $calculation$ and $this$ (in that order). Transitivity rules are 
8547  94 
picked from the current context plus those given as explicit arguments (the 
95 
latter have precedence). 

7315  96 

8547  97 
\item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as 
7315  98 
$\ALSO$, and concludes the current calculational thread. The final result 
99 
is exhibited as fact for forward chaining towards the next goal. Basically, 

7987  100 
$\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that 
101 
``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and 

102 
``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding 

103 
calculational proofs. 

7315  104 

8547  105 
\item [$trans$] declares theorems as transitivity rules. 
7315  106 
\end{descr} 
107 

108 

8483  109 
\section{Named local contexts (cases)}\label{sec:cases} 
110 

111 
\indexisarcmd{case}\indexisarcmd{printcases} 

112 
\indexisaratt{casenames}\indexisaratt{params} 

113 
\begin{matharray}{rcl} 

114 
\isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\ 

8517  115 
\isarcmd{print_cases}^* & : & \isarkeep{proof} \\ 
8483  116 
case_names & : & \isaratt \\ 
117 
params & : & \isaratt \\ 

118 
\end{matharray} 

119 

120 
Basically, Isar proof contexts are built up explicitly using commands like 

121 
$\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proofcontext}). In typical 

122 
verification tasks this can become hard to manage, though. In particular, a 

123 
large number of local contexts may emerge from case analysis or induction over 

124 
inductive sets and types. 

125 

126 
\medskip 

127 

128 
The $\CASENAME$ command provides a shorthand to refer to certain parts of 

129 
logical context symbolically. Proof methods may provide an environment of 

8507  130 
named ``cases'' of the form $c\colon \vec x, \vec \phi$. Then the effect of 
131 
$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$. 

8483  132 

133 
It is important to note that $\CASENAME$ does \emph{not} provide any means to 

134 
peek at the current goal state, which is treated as strictly nonobservable in 

135 
Isar! Instead, the cases considered here usually emerge in a canonical way 

136 
from certain pieces of specification that appear in the theory somewhere else 

137 
(e.g.\ in an inductive definition, or recursive function). See also 

138 
\S\ref{sec:inductmethod} for more details of how this works in HOL. 

139 

140 
\medskip 

141 

142 
Named cases may be exhibited in the current proof context only if both the 

8547  143 
proof method and the rules involved support this. Case names and parameters 
144 
of basic rules may be declared by hand as well, by using appropriate 

145 
attributes. Thus variant versions of rules that have been derived manually 

146 
may be used in advanced case analysis later. 

8483  147 

148 
\railalias{casenames}{case\_names} 

149 
\railterm{casenames} 

150 

151 
\begin{rail} 

152 
'case' nameref attributes? 

153 
; 

154 
casenames (name + ) 

155 
; 

156 
'params' ((name * ) + 'and') 

157 
; 

158 
\end{rail} 

8547  159 
%FIXME bug in rail 
8483  160 

161 
\begin{descr} 

8507  162 
\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$, 
8547  163 
as provided by an appropriate proof method (such as $cases$ and $induct$ in 
164 
Isabelle/HOL, see \S\ref{sec:inductmethod}). The command $\CASE{c}$ 

165 
abbreviates $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$. 

8483  166 
\item [$\isarkeyword{print_cases}$] prints all local contexts of the current 
8547  167 
state, using Isar proof language notation. This is a diagnostic command; 
168 
$undo$ does not apply. 

8483  169 
\item [$case_names~\vec c$] declares names for the local contexts of premises 
8547  170 
of some theorem; $\vec c$ refers to the \emph{suffix} of the list premises. 
8483  171 
\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of 
8547  172 
premises $1, \dots, n$ of some theorem. An empty list of names may be given 
173 
to skip positions, leaving the present parameters unchanged. 

8483  174 
\end{descr} 
175 

176 

8517  177 
\section{Generalized existence} 
7135  178 

8517  179 
\indexisarcmd{obtain} 
7135  180 
\begin{matharray}{rcl} 
8517  181 
\isarcmd{obtain} & : & \isartrans{proof(prove)}{proof(state)} \\ 
182 
\end{matharray} 

183 

184 
Generalized existence reasoning means that additional elements with certain 

185 
properties are introduced, together with a soundness proof of that context 

186 
change (the rest of the main goal is left unchanged). 

187 

8547  188 
Syntactically, the $\OBTAINNAME$ language element is like an initial proof 
189 
method to the present goal, followed by a proof of its additional claim, 

190 
followed by the actual context commands (using the syntax of $\FIXNAME$ and 

191 
$\ASSUMENAME$, see \S\ref{sec:proofcontext}). 

8517  192 

193 
\begin{rail} 

194 
'obtain' (vars + 'and') comment? \\ 'where' (assm comment? + 'and') 

195 
; 

196 
\end{rail} 

197 

8547  198 
$\OBTAINNAME$ is defined as a derived Isar command as follows; here the 
8517  199 
preceding goal shall be $\psi$, with (optional) facts $\vec b$ indicated for 
200 
forward chaining. 

201 
\begin{matharray}{l} 

202 
\OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[0.5ex] 

203 
\quad \PROOF{succeed} \\ 

204 
\qquad \DEF{}{thesis \equiv \psi} \\ 

205 
\qquad \PRESUME{that}{\All{\vec x} \vec\phi \Imp thesis} \\ 

206 
\qquad \FROM{\vec b}~\SHOW{}{thesis}~~\langle proof\rangle \\ 

207 
\quad \NEXT \\ 

208 
\qquad \FIX{\vec x}~\ASSUME{a}{\vec\phi} \\ 

7135  209 
\end{matharray} 
210 

8517  211 
Typically, the soundness proof is relatively straightforward, often just by 
212 
canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or 

213 
$\BY{blast}$ (see \S\ref{sec:classicalauto}). Note that the ``$that$'' 

214 
presumption above is usually declared as simplification and (unsafe) 

8547  215 
introduction rule, depending on the objectlogic's policy, 
216 
though.\footnote{HOL and HOLCF do this already.} 

8517  217 

218 
The original goal statement is wrapped into a local definition in order to 

219 
avoid any automated tools descending into it. Usually, any statement would 

8547  220 
admit the intended reduction anyway; only in very rare cases $thesis_def$ has 
221 
to be expanded to complete the soundness proof. 

8517  222 

223 
\medskip 

224 

225 
In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be 

226 
metalogical existential quantifiers and conjunctions. This concept has a 

227 
broad range of useful applications, ranging from plain elimination (or even 

228 
introduction) of objectlevel existentials and conjunctions, to elimination 

229 
over results of symbolic evaluation of recursive definitions, for example. 

230 

231 

232 
\section{Miscellaneous methods and attributes} 

233 

234 
\indexisarmeth{unfold}\indexisarmeth{fold} 

235 
\indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule} 

236 
\indexisarmeth{fail}\indexisarmeth{succeed} 

237 
\begin{matharray}{rcl} 

238 
unfold & : & \isarmeth \\ 

239 
fold & : & \isarmeth \\[0.5ex] 

240 
erule^* & : & \isarmeth \\ 

241 
drule^* & : & \isarmeth \\ 

242 
frule^* & : & \isarmeth \\[0.5ex] 

243 
succeed & : & \isarmeth \\ 

244 
fail & : & \isarmeth \\ 

245 
\end{matharray} 

7135  246 

247 
\begin{rail} 

8517  248 
('fold'  'unfold'  'erule'  'drule'  'frule') thmrefs 
7135  249 
; 
250 
\end{rail} 

251 

7167  252 
\begin{descr} 
8547  253 
\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given 
8517  254 
metalevel definitions throughout all goals; any facts provided are inserted 
255 
into the goal and subject to rewriting as well. 

8547  256 
\item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the 
257 
basic $rule$ method (see \S\ref{sec:puremethatt}), but apply rules by 

8517  258 
elimresolution, destructresolution, and forwardresolution, respectively 
259 
\cite{isabelleref}. These are improper method, mainly for experimentation 

260 
and emulating tactic scripts. 

7335  261 

8517  262 
Different modes of basic rule application are usually expressed in Isar at 
263 
the proof language level, rather than via implicit proof state 

8547  264 
manipulations. For example, a proper singlestep elimination would be done 
8517  265 
using the basic $rule$ method, with forward chaining of current facts. 
266 
\item [$succeed$] yields a single (unchanged) result; it is the identity of 

267 
the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:synmeth}). 

268 
\item [$fail$] yields an empty result sequence; it is the identity of the 

269 
``\texttt{}'' method combinator (cf.\ \S\ref{sec:synmeth}). 

7167  270 
\end{descr} 
7135  271 

8517  272 

273 
\indexisaratt{standard} 

274 
\indexisaratt{elimify} 

275 

276 
\indexisaratt{RS}\indexisaratt{COMP} 

277 
\indexisaratt{where} 

278 
\indexisaratt{tag}\indexisaratt{untag} 

279 
\indexisaratt{transfer} 

280 
\indexisaratt{export} 

281 
\indexisaratt{unfold}\indexisaratt{fold} 

282 
\begin{matharray}{rcl} 

283 
tag & : & \isaratt \\ 

284 
untag & : & \isaratt \\[0.5ex] 

285 
RS & : & \isaratt \\ 

286 
COMP & : & \isaratt \\[0.5ex] 

287 
where & : & \isaratt \\[0.5ex] 

288 
unfold & : & \isaratt \\ 

289 
fold & : & \isaratt \\[0.5ex] 

290 
standard & : & \isaratt \\ 

291 
elimify & : & \isaratt \\ 

292 
export^* & : & \isaratt \\ 

293 
transfer & : & \isaratt \\[0.5ex] 

294 
\end{matharray} 

295 

296 
\begin{rail} 

297 
'tag' (nameref+) 

298 
; 

299 
'untag' name 

300 
; 

301 
('RS'  'COMP') nat? thmref 

302 
; 

303 
'where' (name '=' term * 'and') 

304 
; 

305 
('unfold'  'fold') thmrefs 

306 
; 

307 
\end{rail} 

308 

309 
\begin{descr} 

310 
\item [$tag~name~args$ and $untag~name$] add and remove $tags$ of some 

311 
theorem. Tags may be any list of strings that serve as comment for some 

312 
tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the 

313 
result). The first string is considered the tag name, the rest its 

314 
arguments. Note that untag removes any tags of the same name. 

8547  315 
\item [$RS~n~a$ and $COMP~n~a$] compose rules. $RS$ resolves with the $n$th 
316 
premise of $a$; $COMP$ is a version of $RS$ that skips the automatic lifting 

317 
process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in 

318 
\cite[\S5]{isabelleref}). 

8517  319 
\item [$where~\vec x = \vec t$] perform named instantiation of schematic 
320 
variables occurring in a theorem. Unlike instantiation tactics (such as 

321 
\texttt{res_inst_tac}, see \cite{isabelleref}), actual schematic variables 

322 
have to be specified (e.g.\ $\Var{x@3}$). 

323 

8547  324 
\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given 
8517  325 
metalevel definitions throughout a rule. 
326 

327 
\item [$standard$] puts a theorem into the standard form of objectrules, just 

328 
as the ML function \texttt{standard} (see \cite[\S5]{isabelleref}). 

329 

330 
\item [$elimify$] turns an destruction rule into an elimination, just as the 

331 
ML function \texttt{make\_elim} (see \cite{isabelleref}). 

332 

333 
\item [$export$] lifts a local result out of the current proof context, 

334 
generalizing all fixed variables and discharging all assumptions. Note that 

8547  335 
proper incremental export is already done as part of the basic Isar 
336 
machinery. This attribute is mainly for experimentation. 

8517  337 

338 
\item [$transfer$] promotes a theorem to the current theory context, which has 

8547  339 
to enclose the former one. This is done automatically whenever rules are 
340 
joined by inference. 

8517  341 

342 
\end{descr} 

7135  343 

344 

345 
\section{The Simplifier} 

346 

7321  347 
\subsection{Simplification methods}\label{sec:simp} 
7315  348 

8483  349 
\indexisarmeth{simp}\indexisarmeth{simpall} 
7315  350 
\begin{matharray}{rcl} 
351 
simp & : & \isarmeth \\ 

8483  352 
simp_all & : & \isarmeth \\ 
7315  353 
\end{matharray} 
354 

8483  355 
\railalias{simpall}{simp\_all} 
356 
\railterm{simpall} 

357 

7315  358 
\begin{rail} 
8483  359 
('simp'  simpall) ('!' ?) (simpmod * ) 
7315  360 
; 
361 

8483  362 
simpmod: ('add'  'del'  'only'  'split' (()  'add'  'del')  'other') ':' thmrefs 
7315  363 
; 
364 
\end{rail} 

365 

7321  366 
\begin{descr} 
8547  367 
\item [$simp$] invokes Isabelle's simplifier, after declaring additional rules 
8594  368 
according to the arguments given. Note that the \railtterm{only} modifier 
8547  369 
first removes all other rewrite rules, congruences, and looper tactics 
8594  370 
(including splits), and then behaves like \railtterm{add}. 
7321  371 

8594  372 
The \railtterm{split} modifiers add or delete rules for the Splitter (see 
8483  373 
also \cite{isabelleref}), the default is to add. This works only if the 
374 
Simplifier method has been properly setup to include the Splitter (all major 

375 
object logics such HOL, HOLCF, FOL, ZF do this already). 

376 

8594  377 
The \railtterm{other} modifier ignores its arguments. Nevertheless, 
8547  378 
additional kinds of rules may be declared by including appropriate 
379 
attributes in the specification. 

8483  380 
\item [$simp_all$] is similar to $simp$, but acts on all goals. 
7321  381 
\end{descr} 
382 

8547  383 
Internally, the $simp$ method is based on \texttt{asm_full_simp_tac} 
8483  384 
\cite[\S10]{isabelleref}, but is much better behaved in practice. Just the 
385 
local premises of the actual goal are involved by default. Additional facts 

386 
may be inserted via forwardchaining (using $\THEN$, $\FROMNAME$ etc.). The 

8547  387 
full context of assumptions is only included in the $simp!$ version, which 
8483  388 
should be used with some care, though. 
7321  389 

8483  390 
Note that there is no separate $split$ method. The effect of 
8547  391 
\texttt{split_tac} can be simulated by $(simp~only\colon~split\colon~\vec a)$. 
8483  392 

393 

394 
\subsection{Declaring rules} 

395 

396 
\indexisaratt{simp}\indexisaratt{split} 

7321  397 
\begin{matharray}{rcl} 
398 
simp & : & \isaratt \\ 

8483  399 
split & : & \isaratt \\ 
7321  400 
\end{matharray} 
401 

402 
\begin{rail} 

8483  403 
('simp'  'split') (()  'add'  'del') 
7321  404 
; 
405 
\end{rail} 

406 

407 
\begin{descr} 

8547  408 
\item [$simp$] declares simplification rules. 
409 
\item [$split$] declares split rules. 

7321  410 
\end{descr} 
7319  411 

7315  412 

413 
\subsection{Forward simplification} 

414 

7391  415 
\indexisaratt{simplify}\indexisaratt{asmsimplify} 
416 
\indexisaratt{fullsimplify}\indexisaratt{asmfullsimplify} 

7315  417 
\begin{matharray}{rcl} 
418 
simplify & : & \isaratt \\ 

419 
asm_simplify & : & \isaratt \\ 

420 
full_simplify & : & \isaratt \\ 

421 
asm_full_simplify & : & \isaratt \\ 

422 
\end{matharray} 

423 

7321  424 
These attributes provide forward rules for simplification, which should be 
8547  425 
used only very rarely. There are no separate options for declaring 
7905  426 
simplification rules locally. 
427 

428 
See the ML functions of the same name in \cite[\S10]{isabelleref} for more 

429 
information. 

7315  430 

431 

7135  432 
\section{The Classical Reasoner} 
433 

7335  434 
\subsection{Basic methods}\label{sec:classicalbasic} 
7321  435 

7974  436 
\indexisarmeth{rule}\indexisarmeth{intro} 
437 
\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction} 

7321  438 
\begin{matharray}{rcl} 
439 
rule & : & \isarmeth \\ 

440 
intro & : & \isarmeth \\ 

441 
elim & : & \isarmeth \\ 

442 
contradiction & : & \isarmeth \\ 

443 
\end{matharray} 

444 

445 
\begin{rail} 

8547  446 
('rule'  'intro'  'elim') thmrefs? 
7321  447 
; 
448 
\end{rail} 

449 

450 
\begin{descr} 

7466  451 
\item [$rule$] as offered by the classical reasoner is a refinement over the 
8517  452 
primitive one (see \S\ref{sec:puremethatt}). In case that no rules are 
7466  453 
provided as arguments, it automatically determines elimination and 
7321  454 
introduction rules from the context (see also \S\ref{sec:classicalmod}). 
8517  455 
This is made the default method for basic proof steps, such as $\PROOFNAME$ 
456 
and ``$\DDOT$'' (two dots), see also \S\ref{sec:proofsteps} and 

457 
\S\ref{sec:puremethatt}. 

7321  458 

7466  459 
\item [$intro$ and $elim$] repeatedly refine some goal by intro or 
7905  460 
elimresolution, after having inserted any facts. Omitting the arguments 
8547  461 
refers to any suitable rules declared in the context, otherwise only the 
462 
explicitly given ones may be applied. The latter form admits better control 

463 
of what actually happens, thus it is very appropriate as an initial method 

464 
for $\PROOFNAME$ that splits up certain connectives of the goal, before 

465 
entering the actual subproof. 

7458  466 

7466  467 
\item [$contradiction$] solves some goal by contradiction, deriving any result 
468 
from both $\neg A$ and $A$. Facts, which are guaranteed to participate, may 

469 
appear in either order. 

7321  470 
\end{descr} 
471 

472 

7981  473 
\subsection{Automated methods}\label{sec:classicalauto} 
7315  474 

7321  475 
\indexisarmeth{blast} 
7391  476 
\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slowbest} 
7321  477 
\begin{matharray}{rcl} 
478 
blast & : & \isarmeth \\ 

479 
fast & : & \isarmeth \\ 

480 
best & : & \isarmeth \\ 

481 
slow & : & \isarmeth \\ 

482 
slow_best & : & \isarmeth \\ 

483 
\end{matharray} 

484 

485 
\railalias{slowbest}{slow\_best} 

486 
\railterm{slowbest} 

487 

488 
\begin{rail} 

7905  489 
'blast' ('!' ?) nat? (clamod * ) 
7321  490 
; 
7905  491 
('fast'  'best'  'slow'  slowbest) ('!' ?) (clamod * ) 
7321  492 
; 
493 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8195
diff
changeset

494 
clamod: (('intro'  'elim'  'dest') (()  '?'  '??')  'del') ':' thmrefs 
7321  495 
; 
496 
\end{rail} 

497 

498 
\begin{descr} 

499 
\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac} 

7335  500 
in \cite[\S11]{isabelleref}). The optional argument specifies a 
7321  501 
usersupplied search bound (default 20). 
502 
\item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical 

7335  503 
reasoner (see \cite[\S11]{isabelleref}, tactic \texttt{fast_tac} etc). 
7321  504 
\end{descr} 
505 

506 
Any of above methods support additional modifiers of the context of classical 

8517  507 
rules. Their semantics is analogous to the attributes given in 
8547  508 
\S\ref{sec:classicalmod}. Facts provided by forward chaining are 
509 
inserted\footnote{These methods usually cannot make proper use of actual rules 

510 
inserted that way, though.} into the goal before doing the search. The 

511 
``!''~argument causes the full context of assumptions to be included as well. 

512 
This is slightly less hazardous than for the Simplifier (see 

513 
\S\ref{sec:simp}). 

7321  514 

7315  515 

7981  516 
\subsection{Combined automated methods} 
7315  517 

7321  518 
\indexisarmeth{auto}\indexisarmeth{force} 
519 
\begin{matharray}{rcl} 

520 
force & : & \isarmeth \\ 

521 
auto & : & \isarmeth \\ 

522 
\end{matharray} 

523 

524 
\begin{rail} 

7905  525 
('force'  'auto') ('!' ?) (clasimpmod * ) 
7321  526 
; 
7315  527 

8483  528 
clasimpmod: ('simp' (()  'add'  'del'  'only')  'other'  
529 
('split' (()  'add'  'del'))  

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8195
diff
changeset

530 
(('intro'  'elim'  'dest') (()  '?'  '??')  'del')) ':' thmrefs 
7321  531 
\end{rail} 
7315  532 

7321  533 
\begin{descr} 
534 
\item [$force$ and $auto$] provide access to Isabelle's combined 

535 
simplification and classical reasoning tactics. See \texttt{force_tac} and 

536 
\texttt{auto_tac} in \cite[\S11]{isabelleref} for more information. The 

537 
modifier arguments correspond to those given in \S\ref{sec:simp} and 

7905  538 
\S\ref{sec:classicalauto}. Just note that the ones related to the 
8594  539 
Simplifier are prefixed by \railtterm{simp} here. 
7987  540 

541 
Facts provided by forward chaining are inserted into the goal before doing 

542 
the search. The ``!''~argument causes the full context of assumptions to be 

543 
included as well. 

7321  544 
\end{descr} 
545 

7987  546 

8483  547 
\subsection{Declaring rules}\label{sec:classicalmod} 
7135  548 

7391  549 
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} 
550 
\indexisaratt{iff}\indexisaratt{delrule} 

7321  551 
\begin{matharray}{rcl} 
552 
intro & : & \isaratt \\ 

553 
elim & : & \isaratt \\ 

554 
dest & : & \isaratt \\ 

7391  555 
iff & : & \isaratt \\ 
7321  556 
delrule & : & \isaratt \\ 
557 
\end{matharray} 

7135  558 

7321  559 
\begin{rail} 
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8195
diff
changeset

560 
('intro'  'elim'  'dest') (()  '?'  '??') 
7321  561 
; 
562 
\end{rail} 

7135  563 

7321  564 
\begin{descr} 
8517  565 
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and 
566 
destruct rules, respectively. By default, rules are considered as 

567 
\emph{safe}, while a single ``?'' classifies as \emph{unsafe}, and ``??'' as 

568 
\emph{extra} (i.e.\ not applied in the searchoriented automated methods, 

569 
but only in singlestep methods such as $rule$). 

7335  570 

8547  571 
\item [$iff$] declares equations both as rules for the Simplifier and 
572 
Classical Reasoner. 

7391  573 

7335  574 
\item [$delrule$] deletes introduction or elimination rules from the context. 
575 
Note that destruction rules would have to be turned into elimination rules 

7321  576 
first, e.g.\ by using the $elimify$ attribute. 
577 
\end{descr} 

7135  578 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8195
diff
changeset

579 

7135  580 
%%% Local Variables: 
581 
%%% mode: latex 

582 
%%% TeXmaster: "isarref" 

583 
%%% End: 