author  wenzelm 
Wed, 27 Dec 2000 18:26:32 +0100  
changeset 10741  e56ac1863f2c 
parent 10627  dc3eff1b7556 
child 10858  479dad7b3b41 
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} 

10223  33 
\item [$\AXCLASS~c < \vec c~axms$] defines an axiomatic type class as the 
34 
intersection of existing classes, with additional axioms holding. Class 

35 
axioms may not contain more than one type variable. The class axioms (with 

36 
implicit sort constraints added) are bound to the given names. Furthermore 

37 
a class introduction rule is generated, which is employed by method 

38 
$intro_classes$ to support instantiation proofs of this class. 

39 

40 
\item [$\INSTANCE~c@1 < c@2$ and $\INSTANCE~t :: (\vec s)c$] setup a goal 

41 
stating a class relation or type arity. The proof would usually proceed by 

42 
$intro_classes$, and then establish the characteristic theorems of the type 

43 
classes involved. After finishing the proof, the theory will be augmented 

44 
by a type signature declaration corresponding to the resulting theorem. 

8517  45 
\item [$intro_classes$] repeatedly expands all class introduction rules of 
46 
this theory. 

7167  47 
\end{descr} 
48 

7315  49 

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

51 

8619  52 
\indexisarcmd{also}\indexisarcmd{finally} 
53 
\indexisarcmd{moreover}\indexisarcmd{ultimately} 

9606  54 
\indexisarcmd{printtransrules}\indexisaratt{trans} 
7315  55 
\begin{matharray}{rcl} 
56 
\isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\ 

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

8619  58 
\isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\ 
59 
\isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\ 

10154  60 
\isarcmd{print_trans_rules}^* & : & \isarkeep{theory~~proof} \\ 
7315  61 
trans & : & \isaratt \\ 
62 
\end{matharray} 

63 

64 
Calculational proof is forward reasoning with implicit application of 

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

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

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

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

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

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

74 
$calculation$ without applying any rules yet. 

7315  75 

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

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

79 
preceding statement. 

7315  80 

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

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

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

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

85 
command required. 

86 

8619  87 
\medskip 
88 

89 
The Isar calculation proof commands may be defined as 

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

91 
blockstructure has been suppressed.} 

92 
\begin{matharray}{rcl} 

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

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

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

98 
\end{matharray} 

99 

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

102 
; 

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

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

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

109 
; 

110 
\end{rail} 

111 

112 
\begin{descr} 

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

9614  120 

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

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

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

127 
calculational proofs. 

9614  128 

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

9614  131 

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

9614  134 

8547  135 
\item [$trans$] declares theorems as transitivity rules. 
9614  136 

7315  137 
\end{descr} 
138 

139 

8483  140 
\section{Named local contexts (cases)}\label{sec:cases} 
141 

142 
\indexisarcmd{case}\indexisarcmd{printcases} 

10548  143 
\indexisaratt{casenames}\indexisaratt{params}\indexisaratt{consumes} 
8483  144 
\begin{matharray}{rcl} 
145 
\isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\ 

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

10548  149 
consumes & : & \isaratt \\ 
8483  150 
\end{matharray} 
151 

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

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

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

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

156 
inductive sets and types. 

157 

158 
\medskip 

159 

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

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

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

8483  164 

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

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

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

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

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

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

171 

172 
\medskip 

173 

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

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

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

178 
may be used in advanced case analysis later. 

8483  179 

180 
\railalias{casenames}{case\_names} 

181 
\railterm{casenames} 

182 

183 
\begin{rail} 

184 
'case' nameref attributes? 

185 
; 

186 
casenames (name + ) 

187 
; 

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

189 
; 

10548  190 
'consumes' nat? 
191 
; 

8483  192 
\end{rail} 
8547  193 
%FIXME bug in rail 
8483  194 

195 
\begin{descr} 

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

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

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

8483  203 
\item [$case_names~\vec c$] declares names for the local contexts of premises 
10627  204 
of some theorem; $\vec c$ refers to the \emph{suffix} of the list of 
205 
premises. 

8483  206 
\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of 
8547  207 
premises $1, \dots, n$ of some theorem. An empty list of names may be given 
208 
to skip positions, leaving the present parameters unchanged. 

9614  209 

210 
Note that the default usage of case rules does \emph{not} directly expose 

211 
parameters to the proof context (see also \S\ref{sec:inductmethodproper}). 

10548  212 
\item [$consumes~n$] declares the number of ``major premises'' of a rule, 
213 
i.e.\ the number of facts to be consumed when it is applied by an 

214 
appropriate proof method (cf.\ \S\ref{sec:inductmethod}). The default 

215 
value of $consumes$ is $n = 1$, which is appropriate for the usual kind of 

216 
cases and induction rules for inductive sets (cf.\ \S\ref{sec:inductive}). 

217 
Rules without any $consumes$ declaration given are treated as if 

218 
$consumes~0$ had been specified. 

219 

220 
Note that explicit $consumes$ declarations are only rarely needed; this is 

221 
already taken care of automatically by the higherlevel $cases$ and $induct$ 

222 
declarations, see also \S\ref{sec:inductatt}. 

8483  223 
\end{descr} 
224 

225 

9614  226 
\section{Generalized existence}\label{sec:obtain} 
7135  227 

8517  228 
\indexisarcmd{obtain} 
7135  229 
\begin{matharray}{rcl} 
9480  230 
\isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\ 
8517  231 
\end{matharray} 
232 

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

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

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

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

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

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

240 
conclusion. 

8517  241 

242 
\begin{rail} 

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

244 
; 

245 
\end{rail} 

246 

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

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

252 
\quad \BG \\ 

253 
\qquad \FIX{thesis} \\ 

10160  254 
\qquad \ASSUME{that~[simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\ 
9480  255 
\qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\ 
256 
\quad \EN \\ 

10154  257 
\quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\ 
7135  258 
\end{matharray} 
259 

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

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

8517  264 

265 
\medskip 

266 

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

268 
metalogical existential quantifiers and conjunctions. This concept has a 

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

270 
introduction) of objectlevel existentials and conjunctions, to elimination 

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

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

8517  274 

275 

10031  276 
\section{Miscellaneous methods and attributes}\label{sec:miscmethods} 
8517  277 

9606  278 
\indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert} 
8517  279 
\indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule} 
280 
\indexisarmeth{fail}\indexisarmeth{succeed} 

281 
\begin{matharray}{rcl} 

282 
unfold & : & \isarmeth \\ 

10741  283 
fold & : & \isarmeth \\ 
284 
insert & : & \isarmeth \\[0.5ex] 

8517  285 
erule^* & : & \isarmeth \\ 
286 
drule^* & : & \isarmeth \\ 

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

288 
succeed & : & \isarmeth \\ 

289 
fail & : & \isarmeth \\ 

290 
\end{matharray} 

7135  291 

292 
\begin{rail} 

10741  293 
('fold'  'unfold'  'insert') thmrefs 
294 
; 

295 
('erule'  'drule'  'frule') ('('nat')')? thmrefs 

7135  296 
; 
297 
\end{rail} 

298 

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

10741  303 
\item [$insert~\vec a$] inserts theorems as facts into all goals of the proof 
304 
state. Note that current facts indicated for forward chaining are ignored. 

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

8517  307 
elimresolution, destructresolution, and forwardresolution, respectively 
10741  308 
\cite{isabelleref}. The optional natural number argument (default $0$) 
309 
specifies additional assumption steps to be performed. 

310 

311 
Note that these methods are improper ones, mainly serving for 

312 
experimentation and tactic script emulation. Different modes of basic rule 

313 
application are usually expressed in Isar at the proof language level, 

314 
rather than via implicit proof state manipulations. For example, a proper 

315 
singlestep elimination would be done using the basic $rule$ method, with 

316 
forward chaining of current facts. 

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

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

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

7167  321 
\end{descr} 
7135  322 

10318  323 
\indexisaratt{tagged}\indexisaratt{untagged} 
9614  324 
\indexisaratt{THEN}\indexisaratt{COMP} 
10318  325 
\indexisaratt{where}\indexisaratt{unfolded}\indexisaratt{folded} 
326 
\indexisaratt{standard}\indexisaratt{elimformat} 

327 
\indexisaratt{novars}\indexisaratt{exported} 

8517  328 
\begin{matharray}{rcl} 
9905  329 
tagged & : & \isaratt \\ 
330 
untagged & : & \isaratt \\[0.5ex] 

9614  331 
THEN & : & \isaratt \\ 
8517  332 
COMP & : & \isaratt \\[0.5ex] 
333 
where & : & \isaratt \\[0.5ex] 

9905  334 
unfolded & : & \isaratt \\ 
335 
folded & : & \isaratt \\[0.5ex] 

8517  336 
standard & : & \isaratt \\ 
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9936
diff
changeset

337 
elim_format & : & \isaratt \\ 
9936  338 
no_vars^* & : & \isaratt \\ 
9905  339 
exported^* & : & \isaratt \\ 
8517  340 
\end{matharray} 
341 

342 
\begin{rail} 

9905  343 
'tagged' (nameref+) 
8517  344 
; 
9905  345 
'untagged' name 
8517  346 
; 
10154  347 
('THEN'  'COMP') ('[' nat ']')? thmref 
8517  348 
; 
349 
'where' (name '=' term * 'and') 

350 
; 

9905  351 
('unfolded'  'folded') thmrefs 
8517  352 
; 
353 
\end{rail} 

354 

355 
\begin{descr} 

9905  356 
\item [$tagged~name~args$ and $untagged~name$] add and remove $tags$ of some 
8517  357 
theorem. Tags may be any list of strings that serve as comment for some 
358 
tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the 

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

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

9614  361 
\item [$THEN~n~a$ and $COMP~n~a$] compose rules. $THEN$ resolves with the 
362 
$n$th premise of $a$; the $COMP$ version skips the automatic lifting 

8547  363 
process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in 
364 
\cite[\S5]{isabelleref}). 

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

8517  368 
have to be specified (e.g.\ $\Var{x@3}$). 
9905  369 
\item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the 
370 
given metalevel definitions throughout a rule. 

8517  371 
\item [$standard$] puts a theorem into the standard form of objectrules, just 
372 
as the ML function \texttt{standard} (see \cite[\S5]{isabelleref}). 

9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9936
diff
changeset

373 
\item [$elim_format$] turns a destruction rule into elimination rule format; 
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9936
diff
changeset

374 
see also the ML function \texttt{make\_elim} (see \cite{isabelleref}). 
9232  375 
\item [$no_vars$] replaces schematic variables by free ones; this is mainly 
376 
for tuning output of pretty printed theorems. 

9905  377 
\item [$exported$] lifts a local result out of the current proof context, 
8517  378 
generalizing all fixed variables and discharging all assumptions. Note that 
8547  379 
proper incremental export is already done as part of the basic Isar 
380 
machinery. This attribute is mainly for experimentation. 

8517  381 
\end{descr} 
7135  382 

383 

9606  384 
\section{Tactic emulations}\label{sec:tactics} 
385 

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

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

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

389 
dynamic instantiation within the scope of some subgoal. 

390 

391 
\begin{warn} 

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

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

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

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

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

397 
\end{warn} 

398 

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

400 
named $foo_tac$. 

401 

402 
\indexisarmeth{ruletac}\indexisarmeth{eruletac} 

403 
\indexisarmeth{druletac}\indexisarmeth{fruletac} 

404 
\indexisarmeth{cuttac}\indexisarmeth{thintac} 

9642  405 
\indexisarmeth{subgoaltac}\indexisarmeth{renametac} 
9614  406 
\indexisarmeth{rotatetac}\indexisarmeth{tactic} 
9606  407 
\begin{matharray}{rcl} 
408 
rule_tac^* & : & \isarmeth \\ 

409 
erule_tac^* & : & \isarmeth \\ 

410 
drule_tac^* & : & \isarmeth \\ 

411 
frule_tac^* & : & \isarmeth \\ 

412 
cut_tac^* & : & \isarmeth \\ 

413 
thin_tac^* & : & \isarmeth \\ 

414 
subgoal_tac^* & : & \isarmeth \\ 

9614  415 
rename_tac^* & : & \isarmeth \\ 
416 
rotate_tac^* & : & \isarmeth \\ 

9606  417 
tactic^* & : & \isarmeth \\ 
418 
\end{matharray} 

419 

420 
\railalias{ruletac}{rule\_tac} 

421 
\railterm{ruletac} 

422 

423 
\railalias{eruletac}{erule\_tac} 

424 
\railterm{eruletac} 

425 

426 
\railalias{druletac}{drule\_tac} 

427 
\railterm{druletac} 

428 

429 
\railalias{fruletac}{frule\_tac} 

430 
\railterm{fruletac} 

431 

432 
\railalias{cuttac}{cut\_tac} 

433 
\railterm{cuttac} 

434 

435 
\railalias{thintac}{thin\_tac} 

436 
\railterm{thintac} 

437 

438 
\railalias{subgoaltac}{subgoal\_tac} 

439 
\railterm{subgoaltac} 

440 

9614  441 
\railalias{renametac}{rename\_tac} 
442 
\railterm{renametac} 

443 

444 
\railalias{rotatetac}{rotate\_tac} 

445 
\railterm{rotatetac} 

446 

9606  447 
\begin{rail} 
448 
( ruletac  eruletac  druletac  fruletac  cuttac  thintac ) goalspec? 

449 
( insts thmref  thmrefs ) 

450 
; 

451 
subgoaltac goalspec? (prop +) 

452 
; 

9614  453 
renametac goalspec? (name +) 
454 
; 

455 
rotatetac goalspec? int? 

456 
; 

9606  457 
'tactic' text 
458 
; 

459 

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

461 
; 

462 
\end{rail} 

463 

464 
\begin{descr} 

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

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

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

9614  468 

9606  469 
Note that multiple rules may be only given there is no instantiation. Then 
470 
$rule_tac$ is the same as \texttt{resolve_tac} in ML (see 

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

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

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

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

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

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

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

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

479 
\cite[\S3]{isabelleref}. 

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

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

482 
\cite[\S3]{isabelleref}. 

9614  483 
\item [$rename_tac~\vec x$] renames parameters of a goal according to the list 
484 
$\vec x$, which refers to the \emph{suffix} of variables. 

485 
\item [$rotate_tac~n$] rotates the assumptions of a goal by $n$ positions: 

486 
from right to left if $n$ is positive, and from left to right if $n$ is 

487 
negative; the default value is $1$. See also \texttt{rotate_tac} in 

488 
\cite[\S3]{isabelleref}. 

9606  489 
\item [$tactic~text$] produces a proof method from any ML text of type 
490 
\texttt{tactic}. Apart from the usual ML environment and the current 

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

492 
bound values: 

493 

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

495 
{\footnotesize\begin{verbatim} 

496 
val ctxt : Proof.context 

497 
val facts : thm list 

498 
val thm : string > thm 

499 
val thms : string > thm list 

500 
\end{verbatim}} 

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

502 
indicates any current facts for forwardchaining, and 

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

504 
theorems) from the context. 

505 
\end{descr} 

506 

507 

9614  508 
\section{The Simplifier}\label{sec:simplifier} 
7135  509 

7321  510 
\subsection{Simplification methods}\label{sec:simp} 
7315  511 

8483  512 
\indexisarmeth{simp}\indexisarmeth{simpall} 
7315  513 
\begin{matharray}{rcl} 
514 
simp & : & \isarmeth \\ 

8483  515 
simp_all & : & \isarmeth \\ 
7315  516 
\end{matharray} 
517 

8483  518 
\railalias{simpall}{simp\_all} 
519 
\railterm{simpall} 

520 

8704  521 
\railalias{noasm}{no\_asm} 
522 
\railterm{noasm} 

523 

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

525 
\railterm{noasmsimp} 

526 

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

528 
\railterm{noasmuse} 

529 

7315  530 
\begin{rail} 
8706  531 
('simp'  simpall) ('!' ?) opt? (simpmod * ) 
7315  532 
; 
533 

8811  534 
opt: '(' (noasm  noasmsimp  noasmuse) ')' 
8704  535 
; 
9711  536 
simpmod: ('add'  'del'  'only'  'cong' (()  'add'  'del')  
9847  537 
'split' (()  'add'  'del')) ':' thmrefs 
7315  538 
; 
539 
\end{rail} 

540 

7321  541 
\begin{descr} 
8547  542 
\item [$simp$] invokes Isabelle's simplifier, after declaring additional rules 
8594  543 
according to the arguments given. Note that the \railtterm{only} modifier 
8547  544 
first removes all other rewrite rules, congruences, and looper tactics 
8594  545 
(including splits), and then behaves like \railtterm{add}. 
9711  546 

547 
\medskip The \railtterm{cong} modifiers add or delete Simplifier congruence 

548 
rules (see also \cite{isabelleref}), the default is to add. 

549 

550 
\medskip The \railtterm{split} modifiers add or delete rules for the 

551 
Splitter (see also \cite{isabelleref}), the default is to add. This works 

552 
only if the Simplifier method has been properly setup to include the 

553 
Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already). 

8483  554 
\item [$simp_all$] is similar to $simp$, but acts on all goals. 
7321  555 
\end{descr} 
556 

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

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

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

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

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

564 
should be used with some care, though. 

7321  565 

8704  566 
Additional Simplifier options may be specified to tune the behavior even 
9614  567 
further: $(no_asm)$ means assumptions are ignored completely (cf.\ 
8811  568 
\texttt{simp_tac}), $(no_asm_simp)$ means assumptions are used in the 
9614  569 
simplification of the conclusion but are not themselves simplified (cf.\ 
8811  570 
\texttt{asm_simp_tac}), and $(no_asm_use)$ means assumptions are simplified 
571 
but are not used in the simplification of each other or the conclusion (cf. 

8704  572 
\texttt{full_simp_tac}). 
573 

574 
\medskip 

575 

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

9711  577 
The effect of repeatedly applying \texttt{split_tac} can be simulated by 
578 
$(simp~only\colon~split\colon~\vec a)$. There is also a separate $split$ 

579 
method available for singlestep case splitting, see \S\ref{sec:basiceq}. 

8483  580 

581 

582 
\subsection{Declaring rules} 

583 

8667  584 
\indexisarcmd{printsimpset} 
8638  585 
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong} 
7321  586 
\begin{matharray}{rcl} 
10154  587 
print_simpset^* & : & \isarkeep{theory~~proof} \\ 
7321  588 
simp & : & \isaratt \\ 
9711  589 
cong & : & \isaratt \\ 
8483  590 
split & : & \isaratt \\ 
7321  591 
\end{matharray} 
592 

593 
\begin{rail} 

9711  594 
('simp'  'cong'  'split') (()  'add'  'del') 
7321  595 
; 
596 
\end{rail} 

597 

598 
\begin{descr} 

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

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

8547  602 
\item [$simp$] declares simplification rules. 
8638  603 
\item [$cong$] declares congruence rules. 
9711  604 
\item [$split$] declares case split rules. 
7321  605 
\end{descr} 
7319  606 

7315  607 

608 
\subsection{Forward simplification} 

609 

9905  610 
\indexisaratt{simplified} 
7315  611 
\begin{matharray}{rcl} 
9905  612 
simplified & : & \isaratt \\ 
7315  613 
\end{matharray} 
614 

9905  615 
\begin{rail} 
616 
'simplified' opt? 

617 
; 

618 

619 
opt: '(' (noasm  noasmsimp  noasmuse) ')' 

620 
; 

621 
\end{rail} 

7905  622 

9905  623 
\begin{descr} 
624 
\item [$simplified$] causes a theorem to be simplified according to the 

625 
current Simplifier context (there are no separate arguments for declaring 

626 
additional rules). By default the result is fully simplified, including 

627 
assumptions and conclusion. The options $no_asm$ etc.\ restrict the 

628 
Simplifier in the same way as the for the $simp$ method (see 

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

630 

631 
The $simplified$ operation should be used only very rarely, usually for 

632 
experimentation only. 

633 
\end{descr} 

7315  634 

635 

9711  636 
\section{Basic equational reasoning}\label{sec:basiceq} 
9614  637 

9703  638 
\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}\indexisaratt{symmetric} 
9614  639 
\begin{matharray}{rcl} 
640 
subst & : & \isarmeth \\ 

641 
hypsubst^* & : & \isarmeth \\ 

9703  642 
split & : & \isarmeth \\ 
9614  643 
symmetric & : & \isaratt \\ 
644 
\end{matharray} 

645 

646 
\begin{rail} 

647 
'subst' thmref 

648 
; 

9799  649 
'split' ('(' 'asm' ')')? thmrefs 
9703  650 
; 
9614  651 
\end{rail} 
652 

653 
These methods and attributes provide basic facilities for equational reasoning 

654 
that are intended for specialized applications only. Normally, single step 

655 
reasoning would be performed by calculation (see \S\ref{sec:calculation}), 

656 
while the Simplifier is the canonical tool for automated normalization (see 

657 
\S\ref{sec:simplifier}). 

658 

659 
\begin{descr} 

660 
\item [$subst~thm$] performs a single substitution step using rule $thm$, 

661 
which may be either a meta or object equality. 

662 
\item [$hypsubst$] performs substitution using some assumption. 

9703  663 
\item [$split~thms$] performs singlestep case splitting using rules $thms$. 
9799  664 
By default, splitting is performed in the conclusion of a goal; the $asm$ 
665 
option indicates to operate on assumptions instead. 

666 

9703  667 
Note that the $simp$ method already involves repeated application of split 
668 
rules as declared in the current context (see \S\ref{sec:simp}). 

9614  669 
\item [$symmetric$] applies the symmetry rule of meta or object equality. 
670 
\end{descr} 

671 

672 

9847  673 
\section{The Classical Reasoner}\label{sec:classical} 
7135  674 

7335  675 
\subsection{Basic methods}\label{sec:classicalbasic} 
7321  676 

7974  677 
\indexisarmeth{rule}\indexisarmeth{intro} 
678 
\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction} 

7321  679 
\begin{matharray}{rcl} 
680 
rule & : & \isarmeth \\ 

681 
intro & : & \isarmeth \\ 

682 
elim & : & \isarmeth \\ 

683 
contradiction & : & \isarmeth \\ 

684 
\end{matharray} 

685 

686 
\begin{rail} 

8547  687 
('rule'  'intro'  'elim') thmrefs? 
7321  688 
; 
689 
\end{rail} 

690 

691 
\begin{descr} 

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

698 
\S\ref{sec:puremethatt}. 

9614  699 

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

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

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

706 
entering the actual subproof. 

9614  707 

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

710 
appear in either order. 

7321  711 
\end{descr} 
712 

713 

7981  714 
\subsection{Automated methods}\label{sec:classicalauto} 
7315  715 

9799  716 
\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow} 
717 
\indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify} 

7321  718 
\begin{matharray}{rcl} 
9780  719 
blast & : & \isarmeth \\ 
720 
fast & : & \isarmeth \\ 

9799  721 
slow & : & \isarmeth \\ 
9780  722 
best & : & \isarmeth \\ 
723 
safe & : & \isarmeth \\ 

724 
clarify & : & \isarmeth \\ 

7321  725 
\end{matharray} 
726 

727 
\begin{rail} 

7905  728 
'blast' ('!' ?) nat? (clamod * ) 
7321  729 
; 
9799  730 
('fast'  'slow'  'best'  'safe'  'clarify') ('!' ?) (clamod * ) 
7321  731 
; 
732 

9408  733 
clamod: (('intro'  'elim'  'dest') ('!'  ()  '?')  'del') ':' thmrefs 
7321  734 
; 
735 
\end{rail} 

736 

737 
\begin{descr} 

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

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

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

743 
facts). 

9799  744 
\item [$fast$, $slow$, $best$, $safe$, and $clarify$] refer to the generic 
745 
classical reasoner. See \texttt{fast_tac}, \texttt{slow_tac}, 

746 
\texttt{best_tac}, \texttt{safe_tac}, and \texttt{clarify_tac} in 

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

7321  748 
\end{descr} 
749 

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

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

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

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

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

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

7321  758 

7315  759 

9847  760 
\subsection{Combined automated methods}\label{sec:clasimp} 
7315  761 

9799  762 
\indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp} 
763 
\indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp} 

7321  764 
\begin{matharray}{rcl} 
9606  765 
auto & : & \isarmeth \\ 
7321  766 
force & : & \isarmeth \\ 
9438  767 
clarsimp & : & \isarmeth \\ 
9606  768 
fastsimp & : & \isarmeth \\ 
9799  769 
slowsimp & : & \isarmeth \\ 
770 
bestsimp & : & \isarmeth \\ 

7321  771 
\end{matharray} 
772 

773 
\begin{rail} 

9780  774 
'auto' '!'? (nat nat)? (clasimpmod * ) 
775 
; 

9799  776 
('force'  'clarsimp'  'fastsimp'  'slowsimp'  'bestsimp') '!'? (clasimpmod * ) 
7321  777 
; 
7315  778 

9711  779 
clasimpmod: ('simp' (()  'add'  'del'  'only')  
10031  780 
('cong'  'split') (()  'add'  'del')  
781 
'iff' (((()  'add') '?'?)  'del')  

9408  782 
(('intro'  'elim'  'dest') ('!'  ()  '?')  'del')) ':' thmrefs 
7321  783 
\end{rail} 
7315  784 

7321  785 
\begin{descr} 
9799  786 
\item [$auto$, $force$, $clarsimp$, $fastsimp$, $slowsimp$, and $bestsimp$] 
787 
provide access to Isabelle's combined simplification and classical reasoning 

788 
tactics. These correspond to \texttt{auto_tac}, \texttt{force_tac}, 

789 
\texttt{clarsimp_tac}, and Classical Reasoner tactics with the Simplifier 

790 
added as wrapper, see \cite[\S11]{isabelleref} for more information. The 

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

9606  792 
\S\ref{sec:classicalauto}. Just note that the ones related to the 
793 
Simplifier are prefixed by \railtterm{simp} here. 

9614  794 

7987  795 
Facts provided by forward chaining are inserted into the goal before doing 
796 
the search. The ``!''~argument causes the full context of assumptions to be 

797 
included as well. 

7321  798 
\end{descr} 
799 

7987  800 

8483  801 
\subsection{Declaring rules}\label{sec:classicalmod} 
7135  802 

8667  803 
\indexisarcmd{printclaset} 
7391  804 
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} 
9936  805 
\indexisaratt{iff}\indexisaratt{rule} 
7321  806 
\begin{matharray}{rcl} 
10154  807 
print_claset^* & : & \isarkeep{theory~~proof} \\ 
7321  808 
intro & : & \isaratt \\ 
809 
elim & : & \isaratt \\ 

810 
dest & : & \isaratt \\ 

9936  811 
rule & : & \isaratt \\ 
7391  812 
iff & : & \isaratt \\ 
7321  813 
\end{matharray} 
7135  814 

7321  815 
\begin{rail} 
9408  816 
('intro'  'elim'  'dest') ('!'  ()  '?') 
7321  817 
; 
9936  818 
'rule' 'del' 
819 
; 

10031  820 
'iff' (((()  'add') '?'?)  'del') 
9936  821 
; 
7321  822 
\end{rail} 
7135  823 

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

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

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

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

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

833 
methods such as $rule$). 

9936  834 
\item [$rule~del$] deletes introduction, elimination, or destruct rules from 
835 
the context. 

10031  836 
\item [$iff$] declares equivalence rules to the context. The default behavior 
837 
is to declare a rewrite rule to the Simplifier, and the two corresponding 

838 
implications to the Classical Reasoner (as ``safe'' rules that are used 

839 
aggressively, which would normally be indicated by ``!''). 

840 

841 
The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only, 

842 
and omits the Simplifier declaration. Thus the declaration does not have 

843 
any effect on automated proof tools, but only on simple methods such as 

844 
$rule$ (see \S\ref{sec:miscmethods}). 

7321  845 
\end{descr} 
7135  846 

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

847 

9614  848 
%%% Local Variables: 
7135  849 
%%% mode: latex 
850 
%%% TeXmaster: "isarref" 

9614  851 
%%% End: 