author  wenzelm 
Thu, 13 Apr 2000 15:02:02 +0200  
changeset 8704  f76f41f24c44 
parent 8667  4230d17073ea 
child 8706  d81088481ec6 
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 

8619  50 
\indexisarcmd{also}\indexisarcmd{finally} 
51 
\indexisarcmd{moreover}\indexisarcmd{ultimately} 

52 
\indexisaratt{trans} 

7315  53 
\begin{matharray}{rcl} 
54 
\isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\ 

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

8619  56 
\isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\ 
57 
\isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\ 

7315  58 
trans & : & \isaratt \\ 
59 
\end{matharray} 

60 

61 
Calculational proof is forward reasoning with implicit application of 

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

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

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

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

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

8619  69 
$\HAVENAME$, $\SHOWNAME$ etc. The $\MOREOVER$ and $\ULTIMATELY$ commands are 
70 
similar to $\ALSO$ and $\FINALLY$, but only collect further results in 

71 
$calculation$ without applying any rules yet. 

7315  72 

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

8619  74 
application with calculational proofs. It refers to the argument\footnote{The 
75 
argument of a curried infix expression is its righthand side.} of the 

76 
preceding statement. 

7315  77 

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

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

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

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

82 
command required. 

83 

8619  84 
\medskip 
85 

86 
The Isar calculation proof commands may be defined as 

87 
follows:\footnote{Internal bookkeeping such as proper handling of 

88 
blockstructure has been suppressed.} 

89 
\begin{matharray}{rcl} 

90 
\ALSO@0 & \equiv & \NOTE{calculation}{this} \\ 

91 
\ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\ 

92 
\FINALLY & \equiv & \ALSO~\FROM{calculation} \\ 

93 
\MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\ 

94 
\ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\ 

95 
\end{matharray} 

96 

7315  97 
\begin{rail} 
98 
('also'  'finally') transrules? comment? 

99 
; 

8619  100 
('moreover'  'ultimately') comment? 
101 
; 

8507  102 
'trans' (()  'add'  'del') 
7315  103 
; 
104 

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

106 
; 

107 
\end{rail} 

108 

109 
\begin{descr} 

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

7315  117 

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

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

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

124 
calculational proofs. 

7315  125 

8619  126 
\item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$, 
127 
but collect results only, without applying rules. 

128 

8547  129 
\item [$trans$] declares theorems as transitivity rules. 
7315  130 
\end{descr} 
131 

132 

8483  133 
\section{Named local contexts (cases)}\label{sec:cases} 
134 

135 
\indexisarcmd{case}\indexisarcmd{printcases} 

136 
\indexisaratt{casenames}\indexisaratt{params} 

137 
\begin{matharray}{rcl} 

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

8517  139 
\isarcmd{print_cases}^* & : & \isarkeep{proof} \\ 
8483  140 
case_names & : & \isaratt \\ 
141 
params & : & \isaratt \\ 

142 
\end{matharray} 

143 

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

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

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

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

148 
inductive sets and types. 

149 

150 
\medskip 

151 

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

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

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

8483  156 

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

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

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

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

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

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

163 

164 
\medskip 

165 

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

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

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

170 
may be used in advanced case analysis later. 

8483  171 

172 
\railalias{casenames}{case\_names} 

173 
\railterm{casenames} 

174 

175 
\begin{rail} 

176 
'case' nameref attributes? 

177 
; 

178 
casenames (name + ) 

179 
; 

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

181 
; 

182 
\end{rail} 

8547  183 
%FIXME bug in rail 
8483  184 

185 
\begin{descr} 

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

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

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

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

8483  198 
\end{descr} 
199 

200 

8517  201 
\section{Generalized existence} 
7135  202 

8517  203 
\indexisarcmd{obtain} 
7135  204 
\begin{matharray}{rcl} 
8517  205 
\isarcmd{obtain} & : & \isartrans{proof(prove)}{proof(state)} \\ 
206 
\end{matharray} 

207 

208 
Generalized existence reasoning means that additional elements with certain 

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

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

211 

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

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

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

8517  216 

217 
\begin{rail} 

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

219 
; 

220 
\end{rail} 

221 

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

225 
\begin{matharray}{l} 

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

227 
\quad \PROOF{succeed} \\ 

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

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

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

231 
\quad \NEXT \\ 

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

7135  233 
\end{matharray} 
234 

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

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

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

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

8517  241 

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

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

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

8517  246 

247 
\medskip 

248 

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

250 
metalogical existential quantifiers and conjunctions. This concept has a 

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

252 
introduction) of objectlevel existentials and conjunctions, to elimination 

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

254 

255 

256 
\section{Miscellaneous methods and attributes} 

257 

258 
\indexisarmeth{unfold}\indexisarmeth{fold} 

259 
\indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule} 

260 
\indexisarmeth{fail}\indexisarmeth{succeed} 

261 
\begin{matharray}{rcl} 

262 
unfold & : & \isarmeth \\ 

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

264 
erule^* & : & \isarmeth \\ 

265 
drule^* & : & \isarmeth \\ 

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

267 
succeed & : & \isarmeth \\ 

268 
fail & : & \isarmeth \\ 

269 
\end{matharray} 

7135  270 

271 
\begin{rail} 

8517  272 
('fold'  'unfold'  'erule'  'drule'  'frule') thmrefs 
7135  273 
; 
274 
\end{rail} 

275 

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

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

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

284 
and emulating tactic scripts. 

7335  285 

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

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

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

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

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

7167  294 
\end{descr} 
7135  295 

8517  296 

297 
\indexisaratt{standard} 

298 
\indexisaratt{elimify} 

299 

300 
\indexisaratt{RS}\indexisaratt{COMP} 

301 
\indexisaratt{where} 

302 
\indexisaratt{tag}\indexisaratt{untag} 

303 
\indexisaratt{transfer} 

304 
\indexisaratt{export} 

305 
\indexisaratt{unfold}\indexisaratt{fold} 

306 
\begin{matharray}{rcl} 

307 
tag & : & \isaratt \\ 

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

309 
RS & : & \isaratt \\ 

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

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

312 
unfold & : & \isaratt \\ 

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

314 
standard & : & \isaratt \\ 

315 
elimify & : & \isaratt \\ 

316 
export^* & : & \isaratt \\ 

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

318 
\end{matharray} 

319 

320 
\begin{rail} 

321 
'tag' (nameref+) 

322 
; 

323 
'untag' name 

324 
; 

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

326 
; 

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

328 
; 

329 
('unfold'  'fold') thmrefs 

330 
; 

331 
\end{rail} 

332 

333 
\begin{descr} 

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

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

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

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

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

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

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

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

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

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

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

347 

8547  348 
\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given 
8517  349 
metalevel definitions throughout a rule. 
350 

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

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

353 

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

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

356 

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

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

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

8517  361 

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

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

8517  365 

366 
\end{descr} 

7135  367 

368 

369 
\section{The Simplifier} 

370 

7321  371 
\subsection{Simplification methods}\label{sec:simp} 
7315  372 

8483  373 
\indexisarmeth{simp}\indexisarmeth{simpall} 
7315  374 
\begin{matharray}{rcl} 
375 
simp & : & \isarmeth \\ 

8483  376 
simp_all & : & \isarmeth \\ 
7315  377 
\end{matharray} 
378 

8483  379 
\railalias{simpall}{simp\_all} 
380 
\railterm{simpall} 

381 

8704  382 
\railalias{noasm}{no\_asm} 
383 
\railterm{noasm} 

384 

385 
\railalias{noasmsimp}{no\_asm\_simp} 

386 
\railterm{noasmsimp} 

387 

388 
\railalias{noasmuse}{no\_asm\_use} 

389 
\railterm{noasmuse} 

390 

7315  391 
\begin{rail} 
8704  392 
('simp'  simpall) ('!' ?) simpopt? (simpmod * ) 
7315  393 
; 
394 

8704  395 
simpopt: (noasm  noasmsimp  noasmuse) ':' 
396 
; 

8483  397 
simpmod: ('add'  'del'  'only'  'split' (()  'add'  'del')  'other') ':' thmrefs 
7315  398 
; 
399 
\end{rail} 

400 

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

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

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

411 

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

8483  415 
\item [$simp_all$] is similar to $simp$, but acts on all goals. 
7321  416 
\end{descr} 
417 

8704  418 
By default, the Simplifier methods are based on \texttt{asm_full_simp_tac} 
419 
internally \cite[\S10]{isabelleref}. In structured proofs this is usually 

420 
quite well behaved in practice: just the local premises of the actual goal are 

421 
involved, additional facts may inserted via explicit forwardchaining (using 

422 
$\THEN$, $\FROMNAME$ etc.). The full context of assumptions is only included 

423 
if the ``$!$'' (bang) argument is given, which should be used with some care, 

424 
though. 

7321  425 

8704  426 
Additional Simplifier options may be specified to tune the behavior even 
427 
further: $no_asm$ means assumptions are ignored completely (cf.\ 

428 
\texttt{simp_tac}), $no_asm_simp$ means assumptions are used in the 

429 
simplification of the conclusion but are not themselves simplified (cf.\ 

430 
\texttt{asm_simp_tac}), and $no_asm_use$ means assumptions are simplified but 

431 
are not used in the simplification of each other or the conclusion (cf. 

432 
\texttt{full_simp_tac}). 

433 

434 
\medskip 

435 

436 
The Splitter package is usually configured to work as part of the Simplifier. 

437 
There is no separate $split$ method available. The effect of repeatedly 

438 
applying \texttt{split_tac} can be simulated by 

439 
$(simp~only\colon~split\colon~\vec a)$. 

8483  440 

441 

442 
\subsection{Declaring rules} 

443 

8667  444 
\indexisarcmd{printsimpset} 
8638  445 
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong} 
7321  446 
\begin{matharray}{rcl} 
8667  447 
print_simpset & : & \isarkeep{theory~~proof} \\ 
7321  448 
simp & : & \isaratt \\ 
8483  449 
split & : & \isaratt \\ 
8638  450 
cong & : & \isaratt \\ 
7321  451 
\end{matharray} 
452 

453 
\begin{rail} 

8638  454 
('simp'  'split'  'cong') (()  'add'  'del') 
7321  455 
; 
456 
\end{rail} 

457 

458 
\begin{descr} 

8667  459 
\item [$print_simpset$] prints the collection of rules declared to the 
460 
Simplifier, which is also known as ``simpset'' internally 

461 
\cite{isabelleref}. This is a diagnostic command; $undo$ does not apply. 

8547  462 
\item [$simp$] declares simplification rules. 
463 
\item [$split$] declares split rules. 

8638  464 
\item [$cong$] declares congruence rules. 
7321  465 
\end{descr} 
7319  466 

7315  467 

468 
\subsection{Forward simplification} 

469 

7391  470 
\indexisaratt{simplify}\indexisaratt{asmsimplify} 
471 
\indexisaratt{fullsimplify}\indexisaratt{asmfullsimplify} 

7315  472 
\begin{matharray}{rcl} 
473 
simplify & : & \isaratt \\ 

474 
asm_simplify & : & \isaratt \\ 

475 
full_simplify & : & \isaratt \\ 

476 
asm_full_simplify & : & \isaratt \\ 

477 
\end{matharray} 

478 

7321  479 
These attributes provide forward rules for simplification, which should be 
8547  480 
used only very rarely. There are no separate options for declaring 
7905  481 
simplification rules locally. 
482 

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

484 
information. 

7315  485 

486 

7135  487 
\section{The Classical Reasoner} 
488 

7335  489 
\subsection{Basic methods}\label{sec:classicalbasic} 
7321  490 

7974  491 
\indexisarmeth{rule}\indexisarmeth{intro} 
492 
\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction} 

7321  493 
\begin{matharray}{rcl} 
494 
rule & : & \isarmeth \\ 

495 
intro & : & \isarmeth \\ 

496 
elim & : & \isarmeth \\ 

497 
contradiction & : & \isarmeth \\ 

498 
\end{matharray} 

499 

500 
\begin{rail} 

8547  501 
('rule'  'intro'  'elim') thmrefs? 
7321  502 
; 
503 
\end{rail} 

504 

505 
\begin{descr} 

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

512 
\S\ref{sec:puremethatt}. 

7321  513 

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

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

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

520 
entering the actual subproof. 

7458  521 

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

524 
appear in either order. 

7321  525 
\end{descr} 
526 

527 

7981  528 
\subsection{Automated methods}\label{sec:classicalauto} 
7315  529 

7321  530 
\indexisarmeth{blast} 
7391  531 
\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slowbest} 
7321  532 
\begin{matharray}{rcl} 
533 
blast & : & \isarmeth \\ 

534 
fast & : & \isarmeth \\ 

535 
best & : & \isarmeth \\ 

536 
slow & : & \isarmeth \\ 

537 
slow_best & : & \isarmeth \\ 

538 
\end{matharray} 

539 

540 
\railalias{slowbest}{slow\_best} 

541 
\railterm{slowbest} 

542 

543 
\begin{rail} 

7905  544 
'blast' ('!' ?) nat? (clamod * ) 
7321  545 
; 
7905  546 
('fast'  'best'  'slow'  slowbest) ('!' ?) (clamod * ) 
7321  547 
; 
548 

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

549 
clamod: (('intro'  'elim'  'dest') (()  '?'  '??')  'del') ':' thmrefs 
7321  550 
; 
551 
\end{rail} 

552 

553 
\begin{descr} 

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

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

7335  558 
reasoner (see \cite[\S11]{isabelleref}, tactic \texttt{fast_tac} etc). 
7321  559 
\end{descr} 
560 

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

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

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

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

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

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

7321  569 

7315  570 

7981  571 
\subsection{Combined automated methods} 
7315  572 

7321  573 
\indexisarmeth{auto}\indexisarmeth{force} 
574 
\begin{matharray}{rcl} 

575 
force & : & \isarmeth \\ 

576 
auto & : & \isarmeth \\ 

577 
\end{matharray} 

578 

579 
\begin{rail} 

7905  580 
('force'  'auto') ('!' ?) (clasimpmod * ) 
7321  581 
; 
7315  582 

8483  583 
clasimpmod: ('simp' (()  'add'  'del'  'only')  'other'  
584 
('split' (()  'add'  'del'))  

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

585 
(('intro'  'elim'  'dest') (()  '?'  '??')  'del')) ':' thmrefs 
7321  586 
\end{rail} 
7315  587 

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

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

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

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

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

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

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

598 
included as well. 

7321  599 
\end{descr} 
600 

7987  601 

8483  602 
\subsection{Declaring rules}\label{sec:classicalmod} 
7135  603 

8667  604 
\indexisarcmd{printclaset} 
7391  605 
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} 
606 
\indexisaratt{iff}\indexisaratt{delrule} 

7321  607 
\begin{matharray}{rcl} 
8667  608 
print_claset & : & \isarkeep{theory~~proof} \\ 
7321  609 
intro & : & \isaratt \\ 
610 
elim & : & \isaratt \\ 

611 
dest & : & \isaratt \\ 

7391  612 
iff & : & \isaratt \\ 
7321  613 
delrule & : & \isaratt \\ 
614 
\end{matharray} 

7135  615 

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

617 
('intro'  'elim'  'dest') (()  '?'  '??') 
7321  618 
; 
8638  619 
'iff' (()  'add'  'del') 
7321  620 
\end{rail} 
7135  621 

7321  622 
\begin{descr} 
8667  623 
\item [$print_claset$] prints the collection of rules declared to the 
624 
Classical Reasoner, which is also known as ``simpset'' internally 

625 
\cite{isabelleref}. This is a diagnostic command; $undo$ does not apply. 

8517  626 
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and 
627 
destruct rules, respectively. By default, rules are considered as 

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

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

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

7335  631 

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

7391  634 

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

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

7135  639 

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

640 

7135  641 
%%% Local Variables: 
642 
%%% mode: latex 

643 
%%% TeXmaster: "isarref" 

644 
%%% End: 