author  wenzelm 
Fri, 17 Mar 2000 22:50:41 +0100  
changeset 8507  d22fcea34cb7 
parent 8483  b437907f9b26 
child 8517  062e6cd78534 
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} 

8507  85 
'tag' (nameref+) 
86 
; 

87 
'untag' name 

7167  88 
; 
89 
'OF' thmrefs 

90 
; 

7321  91 
('RS'  'COMP') nat? thmref 
7167  92 
; 
7175  93 
'of' (inst * ) ('concl' ':' (inst * ))? 
7167  94 
; 
7321  95 
'where' (name '=' term * 'and') 
96 
; 

7990  97 
('unfold'  'fold') thmrefs 
98 
; 

7167  99 

100 
inst: underscore  term 

101 
; 

102 
\end{rail} 

103 

104 
\begin{descr} 

8507  105 
\item [$tag~name~args$ and $untag~name$] add and remove $tags$ of some 
106 
theorem. Tags may be any list of strings that serve as comment for some 

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

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

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

7321  110 
\item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules. $OF$ applies 
111 
$thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelleref}, but note 

7987  112 
the reversed order). Note that premises may be skipped by including 
113 
``$\_$'' (underscore) as argument. 

7396  114 

115 
$RS$ resolves with the $n$th premise of $thm$; $COMP$ is a version of $RS$ 

7987  116 
that skips the automatic lifting process that is normally intended (cf.\ 
117 
\texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelleref}). 

7321  118 

7466  119 
\item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named 
7335  120 
instantiation, respectively. The terms given in $of$ are substituted for 
121 
any schematic variables occurring in a theorem from left to right; 

7990  122 
``\texttt{_}'' (underscore) indicates to skip a position. Arguments 
123 
following a ``$concl\colon$'' specification refer to positions of the 

124 
conclusion of a rule. 

125 

126 
\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given 

127 
metalevel definitions throughout a rule. 

7321  128 

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

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

131 

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

7321  134 

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

7335  136 
generalizing all fixed variables and discharging all assumptions. Note that 
137 
(partial) export is usually done automatically behind the scenes. This 

138 
attribute is mainly for experimentation. 

7321  139 

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

141 
to enclose the former one. Normally, this is done automatically when rules 

142 
are joined by inference. 

143 

7167  144 
\end{descr} 
145 

7315  146 

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

148 

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

150 
\begin{matharray}{rcl} 

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

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

153 
trans & : & \isaratt \\ 

154 
\end{matharray} 

155 

156 
Calculational proof is forward reasoning with implicit application of 

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

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

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

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

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

164 
$\HAVENAME$, $\SHOWNAME$ etc. 

7315  165 

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

167 
application with calculational proofs. It automatically refers to the 

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

169 
side.} of the preceding statement. 

170 

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

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

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

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

175 
command required. 

176 

177 
\begin{rail} 

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

179 
; 

8507  180 
'trans' (()  'add'  'del') 
7315  181 
; 
182 

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

184 
; 

185 
\end{rail} 

186 

187 
\begin{descr} 

188 
\item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as 

189 
follows. The first occurrence of $\ALSO$ in some calculational thread 

7905  190 
initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same 
7335  191 
level of blockstructure updates $calculation$ by some transitivity rule 
7458  192 
applied to $calculation$ and $this$ (in that order). Transitivity rules are 
193 
picked from the current context plus those given as $thms$ (the latter have 

194 
precedence). 

7315  195 

196 
\item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as 

197 
$\ALSO$, and concludes the current calculational thread. The final result 

198 
is exhibited as fact for forward chaining towards the next goal. Basically, 

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

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

202 
calculational proofs. 

7315  203 

7335  204 
\item [$trans$] maintains the set of transitivity rules of the theory or proof 
205 
context, by adding or deleting theorems (the default is to add). 

7315  206 
\end{descr} 
207 

7897  208 
%FIXME 
209 
%See theory \texttt{HOL/Isar_examples/Group} for a simple application of 

210 
%calculations for basic equational reasoning. 

211 
%\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced 

212 
%calculational steps in combination with natural deduction. 

7315  213 

214 

8483  215 
\section{Named local contexts (cases)}\label{sec:cases} 
216 

217 
\indexisarcmd{case}\indexisarcmd{printcases} 

218 
\indexisaratt{casenames}\indexisaratt{params} 

219 
\begin{matharray}{rcl} 

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

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

222 
case_names & : & \isaratt \\ 

223 
params & : & \isaratt \\ 

224 
\end{matharray} 

225 

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

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

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

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

230 
inductive sets and types. 

231 

232 
\medskip 

233 

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

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

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

8483  238 

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

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

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

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

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

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

245 

246 
\medskip 

247 

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

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

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

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

252 
manually may be used in advanced case analysis later. 

253 

254 
\railalias{casenames}{case\_names} 

255 
\railterm{casenames} 

256 

257 
\begin{rail} 

258 
'case' nameref attributes? 

259 
; 

260 
casenames (name + ) 

261 
; 

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

263 
; 

264 
\end{rail} 

265 

266 
\begin{descr} 

8507  267 
\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$, 
8483  268 
as provided by an appropriate proof method (such as $cases$ and $induct$, 
269 
see \S\ref{sec:inductmethod}). The command $\CASE{c}$ abbreviates 

8507  270 
$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$. 
8483  271 
\item [$\isarkeyword{print_cases}$] prints all local contexts of the current 
272 
goal context, using Isar proof language notation. This is a diagnostic 

273 
command; $undo$ does not apply. 

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

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

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

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

278 
to skip positions, leaving the corresponding parameters unchanged. 

279 
\end{descr} 

280 

281 

7135  282 
\section{Axiomatic Type Classes}\label{sec:axclass} 
283 

7356  284 
\indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{introclasses} 
7135  285 
\begin{matharray}{rcl} 
286 
\isarcmd{axclass} & : & \isartrans{theory}{theory} \\ 

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

7356  288 
intro_classes & : & \isarmeth \\ 
7135  289 
\end{matharray} 
290 

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

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

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

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

296 
Isabelle documentation. 

7335  297 
%FIXME cite 
7135  298 

299 
\begin{rail} 

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

301 
; 

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

303 
; 

304 
\end{rail} 

305 

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

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

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

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

7987  312 
employed by method $intro_classes$ to support instantiation proofs of this 
7335  313 
class. 
314 

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

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

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

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

320 
corresponding to the resulting theorem. 

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

7466  322 
this theory. 
7167  323 
\end{descr} 
7135  324 

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

327 
%axiomatic type classes, including instantiation proofs. 

7135  328 

329 

330 
\section{The Simplifier} 

331 

7321  332 
\subsection{Simplification methods}\label{sec:simp} 
7315  333 

8483  334 
\indexisarmeth{simp}\indexisarmeth{simpall} 
7315  335 
\begin{matharray}{rcl} 
336 
simp & : & \isarmeth \\ 

8483  337 
simp_all & : & \isarmeth \\ 
7315  338 
\end{matharray} 
339 

8483  340 
\railalias{simpall}{simp\_all} 
341 
\railterm{simpall} 

342 

7315  343 
\begin{rail} 
8483  344 
('simp'  simpall) ('!' ?) (simpmod * ) 
7315  345 
; 
346 

8483  347 
simpmod: ('add'  'del'  'only'  'split' (()  'add'  'del')  'other') ':' thmrefs 
7315  348 
; 
349 
\end{rail} 

350 

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

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

7321  356 

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

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

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

361 

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

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

364 
back door for arbitrary context manipulation.} 

365 

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

7321  367 
\end{descr} 
368 

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

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

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

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

374 
should be used with some care, though. 

7321  375 

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

378 

379 

380 
\subsection{Declaring rules} 

381 

382 
\indexisaratt{simp}\indexisaratt{split} 

7321  383 
\begin{matharray}{rcl} 
384 
simp & : & \isaratt \\ 

8483  385 
split & : & \isaratt \\ 
7321  386 
\end{matharray} 
387 

388 
\begin{rail} 

8483  389 
('simp'  'split') (()  'add'  'del') 
7321  390 
; 
391 
\end{rail} 

392 

393 
\begin{descr} 

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

8483  396 
\item [$split$] is similar to $simp$, but refers to split rules. 
7321  397 
\end{descr} 
7319  398 

7315  399 

400 
\subsection{Forward simplification} 

401 

7391  402 
\indexisaratt{simplify}\indexisaratt{asmsimplify} 
403 
\indexisaratt{fullsimplify}\indexisaratt{asmfullsimplify} 

7315  404 
\begin{matharray}{rcl} 
405 
simplify & : & \isaratt \\ 

406 
asm_simplify & : & \isaratt \\ 

407 
full_simplify & : & \isaratt \\ 

408 
asm_full_simplify & : & \isaratt \\ 

409 
\end{matharray} 

410 

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

414 

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

416 
information. 

7315  417 

418 

7135  419 
\section{The Classical Reasoner} 
420 

7335  421 
\subsection{Basic methods}\label{sec:classicalbasic} 
7321  422 

7974  423 
\indexisarmeth{rule}\indexisarmeth{intro} 
424 
\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction} 

7321  425 
\begin{matharray}{rcl} 
426 
rule & : & \isarmeth \\ 

427 
intro & : & \isarmeth \\ 

428 
elim & : & \isarmeth \\ 

429 
contradiction & : & \isarmeth \\ 

430 
\end{matharray} 

431 

432 
\begin{rail} 

433 
('rule'  'intro'  'elim') thmrefs 

434 
; 

435 
\end{rail} 

436 

437 
\begin{descr} 

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

7321  444 

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

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

7987  451 
the actual subproof. 
7458  452 

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

455 
appear in either order. 

7321  456 
\end{descr} 
457 

458 

7981  459 
\subsection{Automated methods}\label{sec:classicalauto} 
7315  460 

7321  461 
\indexisarmeth{blast} 
7391  462 
\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slowbest} 
7321  463 
\begin{matharray}{rcl} 
464 
blast & : & \isarmeth \\ 

465 
fast & : & \isarmeth \\ 

466 
best & : & \isarmeth \\ 

467 
slow & : & \isarmeth \\ 

468 
slow_best & : & \isarmeth \\ 

469 
\end{matharray} 

470 

471 
\railalias{slowbest}{slow\_best} 

472 
\railterm{slowbest} 

473 

474 
\begin{rail} 

7905  475 
'blast' ('!' ?) nat? (clamod * ) 
7321  476 
; 
7905  477 
('fast'  'best'  'slow'  slowbest) ('!' ?) (clamod * ) 
7321  478 
; 
479 

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

480 
clamod: (('intro'  'elim'  'dest') (()  '?'  '??')  'del') ':' thmrefs 
7321  481 
; 
482 
\end{rail} 

483 

484 
\begin{descr} 

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

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

7335  489 
reasoner (see \cite[\S11]{isabelleref}, tactic \texttt{fast_tac} etc). 
7321  490 
\end{descr} 
491 

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

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

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

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

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

7321  498 

7315  499 

7981  500 
\subsection{Combined automated methods} 
7315  501 

7321  502 
\indexisarmeth{auto}\indexisarmeth{force} 
503 
\begin{matharray}{rcl} 

504 
force & : & \isarmeth \\ 

505 
auto & : & \isarmeth \\ 

506 
\end{matharray} 

507 

508 
\begin{rail} 

7905  509 
('force'  'auto') ('!' ?) (clasimpmod * ) 
7321  510 
; 
7315  511 

8483  512 
clasimpmod: ('simp' (()  'add'  'del'  'only')  'other'  
513 
('split' (()  'add'  'del'))  

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

514 
(('intro'  'elim'  'dest') (()  '?'  '??')  'del')) ':' thmrefs 
7321  515 
\end{rail} 
7315  516 

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

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

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

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

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

7987  524 

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

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

527 
included as well. 

7321  528 
\end{descr} 
529 

7987  530 

8483  531 
\subsection{Declaring rules}\label{sec:classicalmod} 
7135  532 

7391  533 
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} 
534 
\indexisaratt{iff}\indexisaratt{delrule} 

7321  535 
\begin{matharray}{rcl} 
536 
intro & : & \isaratt \\ 

537 
elim & : & \isaratt \\ 

538 
dest & : & \isaratt \\ 

7391  539 
iff & : & \isaratt \\ 
7321  540 
delrule & : & \isaratt \\ 
541 
\end{matharray} 

7135  542 

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

544 
('intro'  'elim'  'dest') (()  '?'  '??') 
7321  545 
; 
546 
\end{rail} 

7135  547 

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

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

7335  554 

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

557 

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

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

7135  562 

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

563 

7135  564 
%%% Local Variables: 
565 
%%% mode: latex 

566 
%%% TeXmaster: "isarref" 

567 
%%% End: 