author  wenzelm 
Thu, 16 Mar 2000 00:26:44 +0100  
changeset 8483  b437907f9b26 
parent 8203  2fcc6017cb72 
child 8507  d22fcea34cb7 
permissions  rwrr 
7135  1 

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

7315  4 
\section{Basic proof methods}\label{sec:puremeth} 
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{donothing} 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:classicalbasic}); that method is the default for 

45 
$\PROOFNAME$ steps. Note that ``$\DDOT$'' (doubledot) abbreviates 

7897  46 
$\BY{default}$. 
7321  47 
\item [$erule~thms$] is similar to $rule$, but applies rules by 
48 
elimresolution. 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:classicalbasic}). 
7335  52 
\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given 
7987  53 
metalevel 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:synmeth}). 
7987  57 
\item [$fail$] yields an empty result sequence; it is the identity of the 
7897  58 
``\texttt{}'' method combinator (cf.\ \S\ref{sec:synmeth}). 
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]{isabelleref}, 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]{isabelleref}). 

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 
metalevel definitions throughout a rule. 

7321  125 

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

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

128 

7897  129 
\item [$elimify$] turns an destruction rule into an elimination, just as the 
130 
ML function \texttt{make\_elim} (see \cite{isabelleref}). 

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 righthand 

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{begincalculation} 

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 blockstructure 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 

8483  212 
\section{Named local contexts (cases)}\label{sec:cases} 
213 

214 
\indexisarcmd{case}\indexisarcmd{printcases} 

215 
\indexisaratt{casenames}\indexisaratt{params} 

216 
\begin{matharray}{rcl} 

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

218 
\isarcmd{print_cases} & : & \isarkeep{proof} \\[0.5ex] 

219 
case_names & : & \isaratt \\ 

220 
params & : & \isaratt \\ 

221 
\end{matharray} 

222 

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

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

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

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

227 
inductive sets and types. 

228 

229 
\medskip 

230 

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

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

233 
named ``cases'' of the form $c\colon \vec x, \vec \chi$. Then the effect of 

234 
$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\chi}$. 

235 

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

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

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

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

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

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

242 

243 
\medskip 

244 

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

246 
proof method and the corresponding rule support this. Case names and 

247 
parameters of basic rules may be declared by hand as well, by using 

248 
appropriate attributes. Thus variant versions of rules that have been derived 

249 
manually may be used in advanced case analysis later. 

250 

251 
\railalias{casenames}{case\_names} 

252 
\railterm{casenames} 

253 

254 
\begin{rail} 

255 
'case' nameref attributes? 

256 
; 

257 
casenames (name + ) 

258 
; 

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

260 
; 

261 
\end{rail} 

262 

263 
\begin{descr} 

264 
\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \chi$, 

265 
as provided by an appropriate proof method (such as $cases$ and $induct$, 

266 
see \S\ref{sec:inductmethod}). The command $\CASE{c}$ abbreviates 

267 
$\FIX{\vec x}~\ASSUME{c}{\vec\chi}$. 

268 
\item [$\isarkeyword{print_cases}$] prints all local contexts of the current 

269 
goal context, using Isar proof language notation. This is a diagnostic 

270 
command; $undo$ does not apply. 

271 
\item [$case_names~\vec c$] declares names for the local contexts of premises 

272 
of some theorem ($\vec c$ refers to the \emph{suffix} of the list premises). 

273 
\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of 

274 
premises $1, \dots, n$ of some theorem. An empty list of names be be given 

275 
to skip positions, leaving the corresponding parameters unchanged. 

276 
\end{descr} 

277 

278 

7135  279 
\section{Axiomatic Type Classes}\label{sec:axclass} 
280 

7356  281 
\indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{introclasses} 
7135  282 
\begin{matharray}{rcl} 
283 
\isarcmd{axclass} & : & \isartrans{theory}{theory} \\ 

284 
\isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\ 

7356  285 
intro_classes & : & \isarmeth \\ 
7135  286 
\end{matharray} 
287 

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

290 
may make use of this lightweight mechanism of abstract theories. See 

291 
\cite{Wenzel:1997:TPHOL} for more information. There is also a tutorial on 

292 
\emph{Using Axiomatic Type Classes in Isabelle} that is part of the standard 

293 
Isabelle documentation. 

7335  294 
%FIXME cite 
7135  295 

296 
\begin{rail} 

297 
'axclass' classdecl (axmdecl prop comment? +) 

298 
; 

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

300 
; 

301 
\end{rail} 

302 

7167  303 
\begin{descr} 
7335  304 
\item [$\isarkeyword{axclass}~c < \vec c~axms$] defines an axiomatic type 
305 
class as the intersection of existing classes, with additional axioms 

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

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

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

7987  309 
employed by method $intro_classes$ to support instantiation proofs of this 
7335  310 
class. 
311 

312 
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t :: 

313 
(\vec s)c$] setup up a goal stating the class relation or type arity. The 

7987  314 
proof would usually proceed by $intro_classes$, and then establish the 
315 
characteristic theorems of the type classes involved. After finishing the 

316 
proof, the theory will be augmented by a type signature declaration 

317 
corresponding to the resulting theorem. 

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

7466  319 
this theory. 
7167  320 
\end{descr} 
7135  321 

7987  322 
%FIXME 
323 
%See theory \texttt{HOL/Isar_examples/Group} for a simple example of using 

324 
%axiomatic type classes, including instantiation proofs. 

7135  325 

326 

327 
\section{The Simplifier} 

328 

7321  329 
\subsection{Simplification methods}\label{sec:simp} 
7315  330 

8483  331 
\indexisarmeth{simp}\indexisarmeth{simpall} 
7315  332 
\begin{matharray}{rcl} 
333 
simp & : & \isarmeth \\ 

8483  334 
simp_all & : & \isarmeth \\ 
7315  335 
\end{matharray} 
336 

8483  337 
\railalias{simpall}{simp\_all} 
338 
\railterm{simpall} 

339 

7315  340 
\begin{rail} 
8483  341 
('simp'  simpall) ('!' ?) (simpmod * ) 
7315  342 
; 
343 

8483  344 
simpmod: ('add'  'del'  'only'  'split' (()  'add'  'del')  'other') ':' thmrefs 
7315  345 
; 
346 
\end{rail} 

347 

7321  348 
\begin{descr} 
7897  349 
\item [$simp$] invokes Isabelle's simplifier, after modifying the context by 
350 
adding or deleting rules as specified. The \railtoken{only} modifier first 

8483  351 
removes all other rewrite rules, congruences, and looper tactics (including 
352 
splits), and then behaves like \railtoken{add}. 

7321  353 

8483  354 
The \railtoken{split} modifiers add or delete rules for the Splitter (see 
355 
also \cite{isabelleref}), the default is to add. This works only if the 

356 
Simplifier method has been properly setup to include the Splitter (all major 

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

358 

359 
The \railtoken{other} modifier ignores its arguments. Nevertheless there 

360 
may be sideeffects on the context via attributes.\footnote{This provides a 

361 
back door for arbitrary context manipulation.} 

362 

363 
\item [$simp_all$] is similar to $simp$, but acts on all goals. 

7321  364 
\end{descr} 
365 

8483  366 
The $simp$ methods are based on \texttt{asm_full_simp_tac} 
367 
\cite[\S10]{isabelleref}, but is much better behaved in practice. Just the 

368 
local premises of the actual goal are involved by default. Additional facts 

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

370 
full context of assumptions is only included in the $simp!$ versions, which 

371 
should be used with some care, though. 

7321  372 

8483  373 
Note that there is no separate $split$ method. The effect of 
374 
\texttt{split_tac} can be simulated via $(simp~only\colon~split\colon~thms)$. 

375 

376 

377 
\subsection{Declaring rules} 

378 

379 
\indexisaratt{simp}\indexisaratt{split} 

7321  380 
\begin{matharray}{rcl} 
381 
simp & : & \isaratt \\ 

8483  382 
split & : & \isaratt \\ 
7321  383 
\end{matharray} 
384 

385 
\begin{rail} 

8483  386 
('simp'  'split') (()  'add'  'del') 
7321  387 
; 
388 
\end{rail} 

389 

390 
\begin{descr} 

7466  391 
\item [$simp$] adds or deletes rules from the theory or proof context (the 
392 
default is to add). 

8483  393 
\item [$split$] is similar to $simp$, but refers to split rules. 
7321  394 
\end{descr} 
7319  395 

7315  396 

397 
\subsection{Forward simplification} 

398 

7391  399 
\indexisaratt{simplify}\indexisaratt{asmsimplify} 
400 
\indexisaratt{fullsimplify}\indexisaratt{asmfullsimplify} 

7315  401 
\begin{matharray}{rcl} 
402 
simplify & : & \isaratt \\ 

403 
asm_simplify & : & \isaratt \\ 

404 
full_simplify & : & \isaratt \\ 

405 
asm_full_simplify & : & \isaratt \\ 

406 
\end{matharray} 

407 

7321  408 
These attributes provide forward rules for simplification, which should be 
7905  409 
used only very rarely. There are no separate options for adding or deleting 
410 
simplification rules locally. 

411 

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

413 
information. 

7315  414 

415 

7135  416 
\section{The Classical Reasoner} 
417 

7335  418 
\subsection{Basic methods}\label{sec:classicalbasic} 
7321  419 

7974  420 
\indexisarmeth{rule}\indexisarmeth{intro} 
421 
\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction} 

7321  422 
\begin{matharray}{rcl} 
423 
rule & : & \isarmeth \\ 

424 
intro & : & \isarmeth \\ 

425 
elim & : & \isarmeth \\ 

426 
contradiction & : & \isarmeth \\ 

427 
\end{matharray} 

428 

429 
\begin{rail} 

430 
('rule'  'intro'  'elim') thmrefs 

431 
; 

432 
\end{rail} 

433 

434 
\begin{descr} 

7466  435 
\item [$rule$] as offered by the classical reasoner is a refinement over the 
7905  436 
primitive one (see \S\ref{sec:puremeth}). In case that no rules are 
7466  437 
provided as arguments, it automatically determines elimination and 
7321  438 
introduction rules from the context (see also \S\ref{sec:classicalmod}). 
7335  439 
In that form it is the default method for basic proof steps, such as 
440 
$\PROOFNAME$ and ``$\DDOT$'' (two dots). 

7321  441 

7466  442 
\item [$intro$ and $elim$] repeatedly refine some goal by intro or 
7905  443 
elimresolution, after having inserted any facts. Omitting the arguments 
7321  444 
refers to any suitable rules from the context, otherwise only the explicitly 
7335  445 
given ones may be applied. The latter form admits better control of what 
446 
actually happens, thus it is very appropriate as an initial method for 

447 
$\PROOFNAME$ that splits up certain connectives of the goal, before entering 

7987  448 
the actual subproof. 
7458  449 

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

452 
appear in either order. 

7321  453 
\end{descr} 
454 

455 

7981  456 
\subsection{Automated methods}\label{sec:classicalauto} 
7315  457 

7321  458 
\indexisarmeth{blast} 
7391  459 
\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slowbest} 
7321  460 
\begin{matharray}{rcl} 
461 
blast & : & \isarmeth \\ 

462 
fast & : & \isarmeth \\ 

463 
best & : & \isarmeth \\ 

464 
slow & : & \isarmeth \\ 

465 
slow_best & : & \isarmeth \\ 

466 
\end{matharray} 

467 

468 
\railalias{slowbest}{slow\_best} 

469 
\railterm{slowbest} 

470 

471 
\begin{rail} 

7905  472 
'blast' ('!' ?) nat? (clamod * ) 
7321  473 
; 
7905  474 
('fast'  'best'  'slow'  slowbest) ('!' ?) (clamod * ) 
7321  475 
; 
476 

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

477 
clamod: (('intro'  'elim'  'dest') (()  '?'  '??')  'del') ':' thmrefs 
7321  478 
; 
479 
\end{rail} 

480 

481 
\begin{descr} 

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

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

7335  486 
reasoner (see \cite[\S11]{isabelleref}, tactic \texttt{fast_tac} etc). 
7321  487 
\end{descr} 
488 

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

490 
rules. There semantics is analogous to the attributes given in 

7987  491 
\S\ref{sec:classicalmod}. Facts provided by forward chaining are inserted 
492 
into the goal before doing the search. The ``!''~argument causes the full 

493 
context of assumptions to be included as well.\footnote{This is slightly less 

494 
hazardous than for the Simplifier (see \S\ref{sec:simp}).} 

7321  495 

7315  496 

7981  497 
\subsection{Combined automated methods} 
7315  498 

7321  499 
\indexisarmeth{auto}\indexisarmeth{force} 
500 
\begin{matharray}{rcl} 

501 
force & : & \isarmeth \\ 

502 
auto & : & \isarmeth \\ 

503 
\end{matharray} 

504 

505 
\begin{rail} 

7905  506 
('force'  'auto') ('!' ?) (clasimpmod * ) 
7321  507 
; 
7315  508 

8483  509 
clasimpmod: ('simp' (()  'add'  'del'  'only')  'other'  
510 
('split' (()  'add'  'del'))  

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

511 
(('intro'  'elim'  'dest') (()  '?'  '??')  'del')) ':' thmrefs 
7321  512 
\end{rail} 
7315  513 

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

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

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

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

7905  519 
\S\ref{sec:classicalauto}. Just note that the ones related to the 
520 
Simplifier are prefixed by \railtoken{simp} here. 

7987  521 

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

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

524 
included as well. 

7321  525 
\end{descr} 
526 

7987  527 

8483  528 
\subsection{Declaring rules}\label{sec:classicalmod} 
7135  529 

7391  530 
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} 
531 
\indexisaratt{iff}\indexisaratt{delrule} 

7321  532 
\begin{matharray}{rcl} 
533 
intro & : & \isaratt \\ 

534 
elim & : & \isaratt \\ 

535 
dest & : & \isaratt \\ 

7391  536 
iff & : & \isaratt \\ 
7321  537 
delrule & : & \isaratt \\ 
538 
\end{matharray} 

7135  539 

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

541 
('intro'  'elim'  'dest') (()  '?'  '??') 
7321  542 
; 
543 
\end{rail} 

7135  544 

7321  545 
\begin{descr} 
7335  546 
\item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules, 
547 
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

548 
single ``?'' classifies as \emph{unsafe}, and ``??'' as \emph{extra} (i.e.\ 
7990  549 
not applied in the searchoriented automated methods, but only in 
550 
singlestep methods such as $rule$). 

7335  551 

7391  552 
\item [$iff$] declares equations both as rewrite rules for the simplifier and 
553 
classical reasoning rules. 

554 

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

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

7135  559 

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

560 

7135  561 
%%% Local Variables: 
562 
%%% mode: latex 

563 
%%% TeXmaster: "isarref" 

564 
%%% End: 