author  wenzelm 
Mon, 14 Aug 2000 18:49:23 +0200  
changeset 9606  1bf495402ae9 
parent 9480  7afb808b6b3e 
child 9614  8ca1fc75230e 
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} 

9606  56 
\indexisarcmd{printtransrules}\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)} \\ 

9606  62 
\isarcmd{print_trans_rules} & : & \isarkeep{theory~~proof} \\ 
7315  63 
trans & : & \isaratt \\ 
64 
\end{matharray} 

65 

66 
Calculational proof is forward reasoning with implicit application of 

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

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

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

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

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

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

76 
$calculation$ without applying any rules yet. 

7315  77 

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

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

81 
preceding statement. 

7315  82 

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

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

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

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

87 
command required. 

88 

8619  89 
\medskip 
90 

91 
The Isar calculation proof commands may be defined as 

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

93 
blockstructure has been suppressed.} 

94 
\begin{matharray}{rcl} 

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

9606  96 
\ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\[0.5ex] 
8619  97 
\FINALLY & \equiv & \ALSO~\FROM{calculation} \\ 
98 
\MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\ 

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

100 
\end{matharray} 

101 

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

104 
; 

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

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

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

111 
; 

112 
\end{rail} 

113 

114 
\begin{descr} 

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

7315  122 

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

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

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

129 
calculational proofs. 

7315  130 

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

133 

9606  134 
\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity 
135 
rules declared in the current context. 

136 

8547  137 
\item [$trans$] declares theorems as transitivity rules. 
9606  138 

7315  139 
\end{descr} 
140 

141 

8483  142 
\section{Named local contexts (cases)}\label{sec:cases} 
143 

144 
\indexisarcmd{case}\indexisarcmd{printcases} 

145 
\indexisaratt{casenames}\indexisaratt{params} 

146 
\begin{matharray}{rcl} 

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

8517  148 
\isarcmd{print_cases}^* & : & \isarkeep{proof} \\ 
8483  149 
case_names & : & \isaratt \\ 
150 
params & : & \isaratt \\ 

151 
\end{matharray} 

152 

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

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

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

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

157 
inductive sets and types. 

158 

159 
\medskip 

160 

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

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

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

8483  165 

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

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

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

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

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

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

172 

173 
\medskip 

174 

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

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

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

179 
may be used in advanced case analysis later. 

8483  180 

181 
\railalias{casenames}{case\_names} 

182 
\railterm{casenames} 

183 

184 
\begin{rail} 

185 
'case' nameref attributes? 

186 
; 

187 
casenames (name + ) 

188 
; 

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

190 
; 

191 
\end{rail} 

8547  192 
%FIXME bug in rail 
8483  193 

194 
\begin{descr} 

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

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

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

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

8483  207 
\end{descr} 
208 

209 

8517  210 
\section{Generalized existence} 
7135  211 

8517  212 
\indexisarcmd{obtain} 
7135  213 
\begin{matharray}{rcl} 
9480  214 
\isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\ 
8517  215 
\end{matharray} 
216 

9480  217 
Generalized existence means that additional elements with certain properties 
218 
may introduced in the current context. Technically, the $\OBTAINNAME$ 

219 
language element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see 

220 
also see \S\ref{sec:proofcontext}), together with a soundness proof of its 

221 
additional claim. According to the nature of existential reasoning, 

222 
assumptions get eliminated from any result exported from the context later, 

223 
provided that the corresponding parameters do \emph{not} occur in the 

224 
conclusion. 

8517  225 

226 
\begin{rail} 

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

228 
; 

229 
\end{rail} 

230 

9480  231 
$\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$ 
232 
shall refer to (optional) facts indicated for forward chaining. 

8517  233 
\begin{matharray}{l} 
9480  234 
\langle facts~\vec b\rangle \\ 
235 
\OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex] 

236 
\quad \BG \\ 

237 
\qquad \FIX{thesis} \\ 

238 
\qquad \ASSUME{that [simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\ 

239 
\qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\ 

240 
\quad \EN \\ 

9606  241 
\quad \FIX{\vec x}~\ASSUMENAME^{\ast}~{a}~{\vec\phi} \\ 
7135  242 
\end{matharray} 
243 

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

9480  246 
$\BY{blast}$ (see \S\ref{sec:classicalauto}). Accordingly, the ``$that$'' 
247 
reduction above is declared as simplification and introduction rule. 

8517  248 

249 
\medskip 

250 

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

252 
metalogical existential quantifiers and conjunctions. This concept has a 

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

254 
introduction) of objectlevel existentials and conjunctions, to elimination 

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

9480  256 
Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$, 
257 
where the result is treated as an assumption. 

8517  258 

259 

260 
\section{Miscellaneous methods and attributes} 

261 

9606  262 
\indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert} 
8517  263 
\indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule} 
264 
\indexisarmeth{fail}\indexisarmeth{succeed} 

265 
\begin{matharray}{rcl} 

266 
unfold & : & \isarmeth \\ 

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

9606  268 
insert^* & : & \isarmeth \\[0.5ex] 
8517  269 
erule^* & : & \isarmeth \\ 
270 
drule^* & : & \isarmeth \\ 

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

272 
succeed & : & \isarmeth \\ 

273 
fail & : & \isarmeth \\ 

274 
\end{matharray} 

7135  275 

276 
\begin{rail} 

9606  277 
('fold'  'unfold'  'insert'  'erule'  'drule'  'frule') thmrefs 
7135  278 
; 
279 
\end{rail} 

280 

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

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

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

289 
and emulating tactic scripts. 

7335  290 

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

8547  293 
manipulations. For example, a proper singlestep elimination would be done 
8517  294 
using the basic $rule$ method, with forward chaining of current facts. 
9606  295 
\item [$insert~\vec a$] inserts theorems as facts into all goals of the proof 
296 
state. Note that current facts indicated for forward chaining are ignored. 

8517  297 
\item [$succeed$] yields a single (unchanged) result; it is the identity of 
298 
the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:synmeth}). 

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

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

7167  301 
\end{descr} 
7135  302 

8517  303 

304 
\indexisaratt{standard} 

305 
\indexisaratt{elimify} 

9232  306 
\indexisaratt{novars} 
8517  307 

308 
\indexisaratt{RS}\indexisaratt{COMP} 

309 
\indexisaratt{where} 

310 
\indexisaratt{tag}\indexisaratt{untag} 

311 
\indexisaratt{export} 

312 
\indexisaratt{unfold}\indexisaratt{fold} 

313 
\begin{matharray}{rcl} 

314 
tag & : & \isaratt \\ 

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

316 
RS & : & \isaratt \\ 

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

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

319 
unfold & : & \isaratt \\ 

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

321 
standard & : & \isaratt \\ 

322 
elimify & : & \isaratt \\ 

9232  323 
no_vars & : & \isaratt \\ 
8517  324 
export^* & : & \isaratt \\ 
325 
\end{matharray} 

326 

327 
\begin{rail} 

328 
'tag' (nameref+) 

329 
; 

330 
'untag' name 

331 
; 

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

333 
; 

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

335 
; 

336 
('unfold'  'fold') thmrefs 

337 
; 

338 
\end{rail} 

339 

340 
\begin{descr} 

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

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

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

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

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

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

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

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

8517  350 
\item [$where~\vec x = \vec t$] perform named instantiation of schematic 
9606  351 
variables occurring in a theorem. Unlike instantiation tactics such as 
352 
$rule_tac$ (see \S\ref{sec:tacticcommands}), actual schematic variables 

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

8547  355 
\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given 
8517  356 
metalevel definitions throughout a rule. 
357 

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

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

360 

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

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

363 

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

366 

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

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

8517  371 

372 
\end{descr} 

7135  373 

374 

9606  375 
\section{Tactic emulations}\label{sec:tactics} 
376 

377 
The following improper proof methods emulate traditional tactics. These admit 

378 
direct access to the goal state, which is normally considered harmful! In 

379 
particular, this may involve both numbered goal addressing (default 1), and 

380 
dynamic instantiation within the scope of some subgoal. 

381 

382 
\begin{warn} 

383 
Dynamic instantiations are read and typechecked according to a subgoal of 

384 
the current dynamic goal state, rather than the static proof context! In 

385 
particular, locally fixed variables and term abbreviations may not be 

386 
included in the term specifications. Thus schematic variables are left to 

387 
be solved by unification with certain parts of the subgoal involved. 

388 
\end{warn} 

389 

390 
Note that the tactic emulation proof methods in Isabelle/Isar are consistently 

391 
named $foo_tac$. 

392 

393 
\indexisarmeth{ruletac}\indexisarmeth{eruletac} 

394 
\indexisarmeth{druletac}\indexisarmeth{fruletac} 

395 
\indexisarmeth{cuttac}\indexisarmeth{thintac} 

396 
\indexisarmeth{subgoaltac}\indexisarmeth{tactic} 

397 
\begin{matharray}{rcl} 

398 
rule_tac^* & : & \isarmeth \\ 

399 
erule_tac^* & : & \isarmeth \\ 

400 
drule_tac^* & : & \isarmeth \\ 

401 
frule_tac^* & : & \isarmeth \\ 

402 
cut_tac^* & : & \isarmeth \\ 

403 
thin_tac^* & : & \isarmeth \\ 

404 
subgoal_tac^* & : & \isarmeth \\ 

405 
tactic^* & : & \isarmeth \\ 

406 
\end{matharray} 

407 

408 
\railalias{ruletac}{rule\_tac} 

409 
\railterm{ruletac} 

410 

411 
\railalias{eruletac}{erule\_tac} 

412 
\railterm{eruletac} 

413 

414 
\railalias{druletac}{drule\_tac} 

415 
\railterm{druletac} 

416 

417 
\railalias{fruletac}{frule\_tac} 

418 
\railterm{fruletac} 

419 

420 
\railalias{cuttac}{cut\_tac} 

421 
\railterm{cuttac} 

422 

423 
\railalias{thintac}{thin\_tac} 

424 
\railterm{thintac} 

425 

426 
\railalias{subgoaltac}{subgoal\_tac} 

427 
\railterm{subgoaltac} 

428 

429 
\begin{rail} 

430 
( ruletac  eruletac  druletac  fruletac  cuttac  thintac ) goalspec? 

431 
( insts thmref  thmrefs ) 

432 
; 

433 
subgoaltac goalspec? (prop +) 

434 
; 

435 
'tactic' text 

436 
; 

437 

438 
insts: ((name '=' term) + 'and') 'in' 

439 
; 

440 
\end{rail} 

441 

442 
\begin{descr} 

443 
\item [$rule_tac$ etc.] do resolution of rules with explicit instantiation. 

444 
This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see 

445 
\cite[\S3]{isabelleref}). 

446 

447 
Note that multiple rules may be only given there is no instantiation. Then 

448 
$rule_tac$ is the same as \texttt{resolve_tac} in ML (see 

449 
\cite[\S3]{isabelleref}). 

450 
\item [$cut_tac$] inserts facts into the proof state as assumption of a 

451 
subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelleref}. Note 

452 
that the scope of schmatic variables is spread over the main goal statement. 

453 
Instantiations may be given as well, see also ML tactic 

454 
\texttt{cut_inst_tac} in \cite[\S3]{isabelleref}. 

455 
\item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note 

456 
that $\phi$ may contain schematic variables. See also \texttt{thin_tac} in 

457 
\cite[\S3]{isabelleref}. 

458 
\item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal. See 

459 
also \texttt{subgoal_tac} and \texttt{subgoals_tac} in 

460 
\cite[\S3]{isabelleref}. 

461 
\item [$tactic~text$] produces a proof method from any ML text of type 

462 
\texttt{tactic}. Apart from the usual ML environment and the current 

463 
implicit theory context, the ML code may refer to the following locally 

464 
bound values: 

465 

466 
%%FIXME ttbox produces too much trailing space (why?) 

467 
{\footnotesize\begin{verbatim} 

468 
val ctxt : Proof.context 

469 
val facts : thm list 

470 
val thm : string > thm 

471 
val thms : string > thm list 

472 
\end{verbatim}} 

473 
Here \texttt{ctxt} refers to the current proof context, \texttt{facts} 

474 
indicates any current facts for forwardchaining, and 

475 
\texttt{thm}~/~\texttt{thms} retrieve named facts (including global 

476 
theorems) from the context. 

477 
\end{descr} 

478 

479 

7135  480 
\section{The Simplifier} 
481 

7321  482 
\subsection{Simplification methods}\label{sec:simp} 
7315  483 

8483  484 
\indexisarmeth{simp}\indexisarmeth{simpall} 
7315  485 
\begin{matharray}{rcl} 
486 
simp & : & \isarmeth \\ 

8483  487 
simp_all & : & \isarmeth \\ 
7315  488 
\end{matharray} 
489 

8483  490 
\railalias{simpall}{simp\_all} 
491 
\railterm{simpall} 

492 

8704  493 
\railalias{noasm}{no\_asm} 
494 
\railterm{noasm} 

495 

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

497 
\railterm{noasmsimp} 

498 

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

500 
\railterm{noasmuse} 

501 

7315  502 
\begin{rail} 
8706  503 
('simp'  simpall) ('!' ?) opt? (simpmod * ) 
7315  504 
; 
505 

8811  506 
opt: '(' (noasm  noasmsimp  noasmuse) ')' 
8704  507 
; 
8483  508 
simpmod: ('add'  'del'  'only'  'split' (()  'add'  'del')  'other') ':' thmrefs 
7315  509 
; 
510 
\end{rail} 

511 

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

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

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

522 

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

8483  526 
\item [$simp_all$] is similar to $simp$, but acts on all goals. 
7321  527 
\end{descr} 
528 

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

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

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

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

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

536 
should be used with some care, though. 

7321  537 

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

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

8704  544 
\texttt{full_simp_tac}). 
545 

546 
\medskip 

547 

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

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

550 
applying \texttt{split_tac} can be simulated by 

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

8483  552 

553 

554 
\subsection{Declaring rules} 

555 

8667  556 
\indexisarcmd{printsimpset} 
8638  557 
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong} 
7321  558 
\begin{matharray}{rcl} 
8667  559 
print_simpset & : & \isarkeep{theory~~proof} \\ 
7321  560 
simp & : & \isaratt \\ 
8483  561 
split & : & \isaratt \\ 
8638  562 
cong & : & \isaratt \\ 
7321  563 
\end{matharray} 
564 

565 
\begin{rail} 

8638  566 
('simp'  'split'  'cong') (()  'add'  'del') 
7321  567 
; 
568 
\end{rail} 

569 

570 
\begin{descr} 

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

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

8547  574 
\item [$simp$] declares simplification rules. 
575 
\item [$split$] declares split rules. 

8638  576 
\item [$cong$] declares congruence rules. 
7321  577 
\end{descr} 
7319  578 

7315  579 

580 
\subsection{Forward simplification} 

581 

7391  582 
\indexisaratt{simplify}\indexisaratt{asmsimplify} 
583 
\indexisaratt{fullsimplify}\indexisaratt{asmfullsimplify} 

7315  584 
\begin{matharray}{rcl} 
585 
simplify & : & \isaratt \\ 

586 
asm_simplify & : & \isaratt \\ 

587 
full_simplify & : & \isaratt \\ 

588 
asm_full_simplify & : & \isaratt \\ 

589 
\end{matharray} 

590 

7321  591 
These attributes provide forward rules for simplification, which should be 
8547  592 
used only very rarely. There are no separate options for declaring 
7905  593 
simplification rules locally. 
594 

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

596 
information. 

7315  597 

598 

7135  599 
\section{The Classical Reasoner} 
600 

7335  601 
\subsection{Basic methods}\label{sec:classicalbasic} 
7321  602 

7974  603 
\indexisarmeth{rule}\indexisarmeth{intro} 
604 
\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction} 

7321  605 
\begin{matharray}{rcl} 
606 
rule & : & \isarmeth \\ 

607 
intro & : & \isarmeth \\ 

608 
elim & : & \isarmeth \\ 

609 
contradiction & : & \isarmeth \\ 

610 
\end{matharray} 

611 

612 
\begin{rail} 

8547  613 
('rule'  'intro'  'elim') thmrefs? 
7321  614 
; 
615 
\end{rail} 

616 

617 
\begin{descr} 

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

624 
\S\ref{sec:puremethatt}. 

7321  625 

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

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

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

632 
entering the actual subproof. 

7458  633 

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

636 
appear in either order. 

7321  637 
\end{descr} 
638 

639 

7981  640 
\subsection{Automated methods}\label{sec:classicalauto} 
7315  641 

9438  642 
\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{clarify} 
7321  643 
\begin{matharray}{rcl} 
644 
blast & : & \isarmeth \\ 

645 
fast & : & \isarmeth \\ 

646 
best & : & \isarmeth \\ 

9438  647 
clarify & : & \isarmeth \\ 
7321  648 
\end{matharray} 
649 

650 
\begin{rail} 

7905  651 
'blast' ('!' ?) nat? (clamod * ) 
7321  652 
; 
9438  653 
('fast'  'best'  'clarify') ('!' ?) (clamod * ) 
7321  654 
; 
655 

9408  656 
clamod: (('intro'  'elim'  'dest') ('!'  ()  '?')  'del') ':' thmrefs 
7321  657 
; 
658 
\end{rail} 

659 

660 
\begin{descr} 

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

7335  662 
in \cite[\S11]{isabelleref}). The optional argument specifies a 
9606  663 
usersupplied search bound (default 20). Note that $blast$ is the only 
664 
classical proof procedure in Isabelle that can handle actual objectlogic 

665 
rules as local assumptions ($fast$ etc.\ would just ignore nonatomic 

666 
facts). 

9438  667 
\item [$fast$, $best$, and $clarify$] refer to the generic classical reasoner. 
668 
See \texttt{fast_tac}, \texttt{best_tac}, and \texttt{clarify_tac} in 

669 
\cite[\S11]{isabelleref} for more information. 

7321  670 
\end{descr} 
671 

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

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

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

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

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

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

7321  680 

7315  681 

7981  682 
\subsection{Combined automated methods} 
7315  683 

9606  684 
\indexisarmeth{auto}\indexisarmeth{force} 
685 
\indexisarmeth{clarsimp}\indexisarmeth{fastsimp} 

7321  686 
\begin{matharray}{rcl} 
9606  687 
auto & : & \isarmeth \\ 
7321  688 
force & : & \isarmeth \\ 
9438  689 
clarsimp & : & \isarmeth \\ 
9606  690 
fastsimp & : & \isarmeth \\ 
7321  691 
\end{matharray} 
692 

693 
\begin{rail} 

9606  694 
('auto'  'force'  'clarsimp'  'fastsimp') ('!' ?) (clasimpmod * ) 
7321  695 
; 
7315  696 

8483  697 
clasimpmod: ('simp' (()  'add'  'del'  'only')  'other'  
698 
('split' (()  'add'  'del'))  

9408  699 
(('intro'  'elim'  'dest') ('!'  ()  '?')  'del')) ':' thmrefs 
7321  700 
\end{rail} 
7315  701 

7321  702 
\begin{descr} 
9606  703 
\item [$auto$, $force$, $clarsimp$, $fastsimp$] provide access to Isabelle's 
704 
combined simplification and classical reasoning tactics. These correspond 

705 
to \texttt{auto_tac}, \texttt{force_tac}, \texttt{clarsimp_tac}, and 

706 
\texttt{fast_tac} (with the Simplifier added as wrapper), see 

707 
\cite[\S11]{isabelleref} for more information. The modifier arguments 

708 
correspond to those given in \S\ref{sec:simp} and 

709 
\S\ref{sec:classicalauto}. Just note that the ones related to the 

710 
Simplifier are prefixed by \railtterm{simp} here. 

7987  711 

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

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

714 
included as well. 

7321  715 
\end{descr} 
716 

7987  717 

8483  718 
\subsection{Declaring rules}\label{sec:classicalmod} 
7135  719 

8667  720 
\indexisarcmd{printclaset} 
7391  721 
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} 
722 
\indexisaratt{iff}\indexisaratt{delrule} 

7321  723 
\begin{matharray}{rcl} 
8667  724 
print_claset & : & \isarkeep{theory~~proof} \\ 
7321  725 
intro & : & \isaratt \\ 
726 
elim & : & \isaratt \\ 

727 
dest & : & \isaratt \\ 

7391  728 
iff & : & \isaratt \\ 
7321  729 
delrule & : & \isaratt \\ 
730 
\end{matharray} 

7135  731 

7321  732 
\begin{rail} 
9408  733 
('intro'  'elim'  'dest') ('!'  ()  '?') 
7321  734 
; 
8638  735 
'iff' (()  'add'  'del') 
7321  736 
\end{rail} 
7135  737 

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

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

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

9408  744 
\emph{unsafe} (i.e.\ not applied blindly without backtracking), while a 
745 
single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not 

746 
applied in the searchoriented automated methods, but only in singlestep 

747 
methods such as $rule$). 

7335  748 

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

7391  751 

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

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

7135  756 

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

757 

7135  758 
%%% Local Variables: 
759 
%%% mode: latex 

760 
%%% TeXmaster: "isarref" 

761 
%%% End: 