author  wenzelm 
Sat, 01 Jul 2000 19:58:59 +0200  
changeset 9232  96722b04f2ae 
parent 9005  67fb61748d35 
child 9408  d3d56e1d2ec1 
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 

8904  6 
%FIXME 
7 
%  qualified names 

8 
%  class intro rules; 

9 
%  class axioms; 

10 

8517  11 
\indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{introclasses} 
7167  12 
\begin{matharray}{rcl} 
8517  13 
\isarcmd{axclass} & : & \isartrans{theory}{theory} \\ 
14 
\isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\ 

15 
intro_classes & : & \isarmeth \\ 

7167  16 
\end{matharray} 
17 

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

8547  20 
may make use of this lightweight mechanism of abstract theories 
8901  21 
\cite{Wenzel:1997:TPHOL}. There is also a tutorial on using axiomatic type 
22 
classes in isabelle \cite{isabelleaxclass} that is part of the standard 

23 
Isabelle documentation. 

8517  24 

7167  25 
\begin{rail} 
8517  26 
'axclass' classdecl (axmdecl prop comment? +) 
27 
; 

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

7167  29 
; 
30 
\end{rail} 

31 

32 
\begin{descr} 

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

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

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

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

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

39 
class. 

7321  40 

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

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

46 
corresponding to the resulting theorem. 

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

48 
this theory. 

7167  49 
\end{descr} 
50 

7315  51 

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

53 

8619  54 
\indexisarcmd{also}\indexisarcmd{finally} 
55 
\indexisarcmd{moreover}\indexisarcmd{ultimately} 

56 
\indexisaratt{trans} 

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

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

8619  60 
\isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\ 
61 
\isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\ 

7315  62 
trans & : & \isaratt \\ 
63 
\end{matharray} 

64 

65 
Calculational proof is forward reasoning with implicit application of 

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

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

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

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

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

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

75 
$calculation$ without applying any rules yet. 

7315  76 

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

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

80 
preceding statement. 

7315  81 

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

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

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

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

86 
command required. 

87 

8619  88 
\medskip 
89 

90 
The Isar calculation proof commands may be defined as 

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

92 
blockstructure has been suppressed.} 

93 
\begin{matharray}{rcl} 

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

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

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

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

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

99 
\end{matharray} 

100 

7315  101 
\begin{rail} 
102 
('also'  'finally') transrules? comment? 

103 
; 

8619  104 
('moreover'  'ultimately') comment? 
105 
; 

8507  106 
'trans' (()  'add'  'del') 
7315  107 
; 
108 

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

110 
; 

111 
\end{rail} 

112 

113 
\begin{descr} 

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

7315  121 

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

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

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

128 
calculational proofs. 

7315  129 

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

132 

8547  133 
\item [$trans$] declares theorems as transitivity rules. 
7315  134 
\end{descr} 
135 

136 

8483  137 
\section{Named local contexts (cases)}\label{sec:cases} 
138 

139 
\indexisarcmd{case}\indexisarcmd{printcases} 

140 
\indexisaratt{casenames}\indexisaratt{params} 

141 
\begin{matharray}{rcl} 

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

8517  143 
\isarcmd{print_cases}^* & : & \isarkeep{proof} \\ 
8483  144 
case_names & : & \isaratt \\ 
145 
params & : & \isaratt \\ 

146 
\end{matharray} 

147 

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

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

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

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

152 
inductive sets and types. 

153 

154 
\medskip 

155 

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

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

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

8483  160 

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

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

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

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

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

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

167 

168 
\medskip 

169 

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

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

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

174 
may be used in advanced case analysis later. 

8483  175 

176 
\railalias{casenames}{case\_names} 

177 
\railterm{casenames} 

178 

179 
\begin{rail} 

180 
'case' nameref attributes? 

181 
; 

182 
casenames (name + ) 

183 
; 

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

185 
; 

186 
\end{rail} 

8547  187 
%FIXME bug in rail 
8483  188 

189 
\begin{descr} 

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

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

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

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

8483  202 
\end{descr} 
203 

204 

8517  205 
\section{Generalized existence} 
7135  206 

8517  207 
\indexisarcmd{obtain} 
7135  208 
\begin{matharray}{rcl} 
8517  209 
\isarcmd{obtain} & : & \isartrans{proof(prove)}{proof(state)} \\ 
210 
\end{matharray} 

211 

212 
Generalized existence reasoning means that additional elements with certain 

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

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

215 

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

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

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

8517  220 

221 
\begin{rail} 

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

223 
; 

224 
\end{rail} 

225 

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

229 
\begin{matharray}{l} 

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

231 
\quad \PROOF{succeed} \\ 

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

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

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

235 
\quad \NEXT \\ 

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

7135  237 
\end{matharray} 
238 

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

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

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

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

8517  245 

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

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

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

8517  250 

251 
\medskip 

252 

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

254 
metalogical existential quantifiers and conjunctions. This concept has a 

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

256 
introduction) of objectlevel existentials and conjunctions, to elimination 

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

258 

259 

260 
\section{Miscellaneous methods and attributes} 

261 

262 
\indexisarmeth{unfold}\indexisarmeth{fold} 

263 
\indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule} 

264 
\indexisarmeth{fail}\indexisarmeth{succeed} 

265 
\begin{matharray}{rcl} 

266 
unfold & : & \isarmeth \\ 

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

268 
erule^* & : & \isarmeth \\ 

269 
drule^* & : & \isarmeth \\ 

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

271 
succeed & : & \isarmeth \\ 

272 
fail & : & \isarmeth \\ 

273 
\end{matharray} 

7135  274 

275 
\begin{rail} 

8517  276 
('fold'  'unfold'  'erule'  'drule'  'frule') thmrefs 
7135  277 
; 
278 
\end{rail} 

279 

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

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

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

288 
and emulating tactic scripts. 

7335  289 

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

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

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

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

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

7167  298 
\end{descr} 
7135  299 

8517  300 

301 
\indexisaratt{standard} 

302 
\indexisaratt{elimify} 

9232  303 
\indexisaratt{novars} 
8517  304 

305 
\indexisaratt{RS}\indexisaratt{COMP} 

306 
\indexisaratt{where} 

307 
\indexisaratt{tag}\indexisaratt{untag} 

308 
\indexisaratt{export} 

309 
\indexisaratt{unfold}\indexisaratt{fold} 

310 
\begin{matharray}{rcl} 

311 
tag & : & \isaratt \\ 

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

313 
RS & : & \isaratt \\ 

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

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

316 
unfold & : & \isaratt \\ 

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

318 
standard & : & \isaratt \\ 

319 
elimify & : & \isaratt \\ 

9232  320 
no_vars & : & \isaratt \\ 
8517  321 
export^* & : & \isaratt \\ 
322 
\end{matharray} 

323 

324 
\begin{rail} 

325 
'tag' (nameref+) 

326 
; 

327 
'untag' name 

328 
; 

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

330 
; 

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

332 
; 

333 
('unfold'  'fold') thmrefs 

334 
; 

335 
\end{rail} 

336 

337 
\begin{descr} 

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

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

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

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

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

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

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

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

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

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

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

351 

8547  352 
\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given 
8517  353 
metalevel definitions throughout a rule. 
354 

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

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

357 

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

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

360 

9232  361 
\item [$no_vars$] replaces schematic variables by free ones; this is mainly 
362 
for tuning output of pretty printed theorems. 

363 

8517  364 
\item [$export$] lifts a local result out of the current proof context, 
365 
generalizing all fixed variables and discharging all assumptions. Note that 

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

8517  368 

369 
\end{descr} 

7135  370 

371 

372 
\section{The Simplifier} 

373 

7321  374 
\subsection{Simplification methods}\label{sec:simp} 
7315  375 

8483  376 
\indexisarmeth{simp}\indexisarmeth{simpall} 
7315  377 
\begin{matharray}{rcl} 
378 
simp & : & \isarmeth \\ 

8483  379 
simp_all & : & \isarmeth \\ 
7315  380 
\end{matharray} 
381 

8483  382 
\railalias{simpall}{simp\_all} 
383 
\railterm{simpall} 

384 

8704  385 
\railalias{noasm}{no\_asm} 
386 
\railterm{noasm} 

387 

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

389 
\railterm{noasmsimp} 

390 

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

392 
\railterm{noasmuse} 

393 

7315  394 
\begin{rail} 
8706  395 
('simp'  simpall) ('!' ?) opt? (simpmod * ) 
7315  396 
; 
397 

8811  398 
opt: '(' (noasm  noasmsimp  noasmuse) ')' 
8704  399 
; 
8483  400 
simpmod: ('add'  'del'  'only'  'split' (()  'add'  'del')  'other') ':' thmrefs 
7315  401 
; 
402 
\end{rail} 

403 

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

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

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

414 

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

8483  418 
\item [$simp_all$] is similar to $simp$, but acts on all goals. 
7321  419 
\end{descr} 
420 

8704  421 
By default, the Simplifier methods are based on \texttt{asm_full_simp_tac} 
8706  422 
internally \cite[\S10]{isabelleref}, which means that assumptions are both 
423 
simplified as well as used in simplifying the conclusion. In structured 

424 
proofs this is usually quite well behaved in practice: just the local premises 

425 
of the actual goal are involved, additional facts may inserted via explicit 

426 
forwardchaining (using $\THEN$, $\FROMNAME$ etc.). The full context of 

427 
assumptions is only included if the ``$!$'' (bang) argument is given, which 

428 
should be used with some care, though. 

7321  429 

8704  430 
Additional Simplifier options may be specified to tune the behavior even 
8811  431 
further: $(no_asm)$ means assumptions are ignored completely (cf.\ 
432 
\texttt{simp_tac}), $(no_asm_simp)$ means assumptions are used in the 

8704  433 
simplification of the conclusion but are not themselves simplified (cf.\ 
8811  434 
\texttt{asm_simp_tac}), and $(no_asm_use)$ means assumptions are simplified 
435 
but are not used in the simplification of each other or the conclusion (cf. 

8704  436 
\texttt{full_simp_tac}). 
437 

438 
\medskip 

439 

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

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

442 
applying \texttt{split_tac} can be simulated by 

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

8483  444 

445 

446 
\subsection{Declaring rules} 

447 

8667  448 
\indexisarcmd{printsimpset} 
8638  449 
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong} 
7321  450 
\begin{matharray}{rcl} 
8667  451 
print_simpset & : & \isarkeep{theory~~proof} \\ 
7321  452 
simp & : & \isaratt \\ 
8483  453 
split & : & \isaratt \\ 
8638  454 
cong & : & \isaratt \\ 
7321  455 
\end{matharray} 
456 

457 
\begin{rail} 

8638  458 
('simp'  'split'  'cong') (()  'add'  'del') 
7321  459 
; 
460 
\end{rail} 

461 

462 
\begin{descr} 

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

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

8547  466 
\item [$simp$] declares simplification rules. 
467 
\item [$split$] declares split rules. 

8638  468 
\item [$cong$] declares congruence rules. 
7321  469 
\end{descr} 
7319  470 

7315  471 

472 
\subsection{Forward simplification} 

473 

7391  474 
\indexisaratt{simplify}\indexisaratt{asmsimplify} 
475 
\indexisaratt{fullsimplify}\indexisaratt{asmfullsimplify} 

7315  476 
\begin{matharray}{rcl} 
477 
simplify & : & \isaratt \\ 

478 
asm_simplify & : & \isaratt \\ 

479 
full_simplify & : & \isaratt \\ 

480 
asm_full_simplify & : & \isaratt \\ 

481 
\end{matharray} 

482 

7321  483 
These attributes provide forward rules for simplification, which should be 
8547  484 
used only very rarely. There are no separate options for declaring 
7905  485 
simplification rules locally. 
486 

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

488 
information. 

7315  489 

490 

7135  491 
\section{The Classical Reasoner} 
492 

7335  493 
\subsection{Basic methods}\label{sec:classicalbasic} 
7321  494 

7974  495 
\indexisarmeth{rule}\indexisarmeth{intro} 
496 
\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction} 

7321  497 
\begin{matharray}{rcl} 
498 
rule & : & \isarmeth \\ 

499 
intro & : & \isarmeth \\ 

500 
elim & : & \isarmeth \\ 

501 
contradiction & : & \isarmeth \\ 

502 
\end{matharray} 

503 

504 
\begin{rail} 

8547  505 
('rule'  'intro'  'elim') thmrefs? 
7321  506 
; 
507 
\end{rail} 

508 

509 
\begin{descr} 

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

516 
\S\ref{sec:puremethatt}. 

7321  517 

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

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

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

524 
entering the actual subproof. 

7458  525 

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

528 
appear in either order. 

7321  529 
\end{descr} 
530 

531 

7981  532 
\subsection{Automated methods}\label{sec:classicalauto} 
7315  533 

7321  534 
\indexisarmeth{blast} 
7391  535 
\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slowbest} 
7321  536 
\begin{matharray}{rcl} 
537 
blast & : & \isarmeth \\ 

538 
fast & : & \isarmeth \\ 

539 
best & : & \isarmeth \\ 

540 
slow & : & \isarmeth \\ 

541 
slow_best & : & \isarmeth \\ 

542 
\end{matharray} 

543 

544 
\railalias{slowbest}{slow\_best} 

545 
\railterm{slowbest} 

546 

547 
\begin{rail} 

7905  548 
'blast' ('!' ?) nat? (clamod * ) 
7321  549 
; 
7905  550 
('fast'  'best'  'slow'  slowbest) ('!' ?) (clamod * ) 
7321  551 
; 
552 

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

553 
clamod: (('intro'  'elim'  'dest') (()  '?'  '??')  'del') ':' thmrefs 
7321  554 
; 
555 
\end{rail} 

556 

557 
\begin{descr} 

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

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

7335  562 
reasoner (see \cite[\S11]{isabelleref}, tactic \texttt{fast_tac} etc). 
7321  563 
\end{descr} 
564 

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

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

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

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

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

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

7321  573 

7315  574 

7981  575 
\subsection{Combined automated methods} 
7315  576 

7321  577 
\indexisarmeth{auto}\indexisarmeth{force} 
578 
\begin{matharray}{rcl} 

579 
force & : & \isarmeth \\ 

580 
auto & : & \isarmeth \\ 

581 
\end{matharray} 

582 

583 
\begin{rail} 

7905  584 
('force'  'auto') ('!' ?) (clasimpmod * ) 
7321  585 
; 
7315  586 

8483  587 
clasimpmod: ('simp' (()  'add'  'del'  'only')  'other'  
588 
('split' (()  'add'  'del'))  

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

589 
(('intro'  'elim'  'dest') (()  '?'  '??')  'del')) ':' thmrefs 
7321  590 
\end{rail} 
7315  591 

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

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

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

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

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

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

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

602 
included as well. 

7321  603 
\end{descr} 
604 

7987  605 

8483  606 
\subsection{Declaring rules}\label{sec:classicalmod} 
7135  607 

8667  608 
\indexisarcmd{printclaset} 
7391  609 
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} 
610 
\indexisaratt{iff}\indexisaratt{delrule} 

7321  611 
\begin{matharray}{rcl} 
8667  612 
print_claset & : & \isarkeep{theory~~proof} \\ 
7321  613 
intro & : & \isaratt \\ 
614 
elim & : & \isaratt \\ 

615 
dest & : & \isaratt \\ 

7391  616 
iff & : & \isaratt \\ 
7321  617 
delrule & : & \isaratt \\ 
618 
\end{matharray} 

7135  619 

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

621 
('intro'  'elim'  'dest') (()  '?'  '??') 
7321  622 
; 
8638  623 
'iff' (()  'add'  'del') 
7321  624 
\end{rail} 
7135  625 

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

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

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

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

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

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

7335  635 

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

7391  638 

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

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

7135  643 

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

644 

7135  645 
%%% Local Variables: 
646 
%%% mode: latex 

647 
%%% TeXmaster: "isarref" 

648 
%%% End: 