author  wenzelm 
Fri, 10 Nov 2000 19:02:37 +0100  
changeset 10432  3dfbc913d184 
parent 10318  e47c221beded 
child 10548  e8c774c12105 
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} 

143 
\indexisaratt{casenames}\indexisaratt{params} 

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 \\ 

149 
\end{matharray} 

150 

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

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

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

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

155 
inductive sets and types. 

156 

157 
\medskip 

158 

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

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

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

8483  163 

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

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

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

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

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

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

170 

171 
\medskip 

172 

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

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

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

177 
may be used in advanced case analysis later. 

8483  178 

179 
\railalias{casenames}{case\_names} 

180 
\railterm{casenames} 

181 

182 
\begin{rail} 

183 
'case' nameref attributes? 

184 
; 

185 
casenames (name + ) 

186 
; 

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

188 
; 

189 
\end{rail} 

8547  190 
%FIXME bug in rail 
8483  191 

192 
\begin{descr} 

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

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

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

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

9614  205 

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

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

8483  208 
\end{descr} 
209 

210 

9614  211 
\section{Generalized existence}\label{sec:obtain} 
7135  212 

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

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

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

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

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

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

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

225 
conclusion. 

8517  226 

227 
\begin{rail} 

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

229 
; 

230 
\end{rail} 

231 

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

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

237 
\quad \BG \\ 

238 
\qquad \FIX{thesis} \\ 

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

10154  242 
\quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\ 
7135  243 
\end{matharray} 
244 

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

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

8517  249 

250 
\medskip 

251 

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

253 
metalogical existential quantifiers and conjunctions. This concept has a 

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

255 
introduction) of objectlevel existentials and conjunctions, to elimination 

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

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

8517  259 

260 

10031  261 
\section{Miscellaneous methods and attributes}\label{sec:miscmethods} 
8517  262 

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

266 
\begin{matharray}{rcl} 

267 
unfold & : & \isarmeth \\ 

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

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

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

273 
succeed & : & \isarmeth \\ 

274 
fail & : & \isarmeth \\ 

275 
\end{matharray} 

7135  276 

277 
\begin{rail} 

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

281 

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

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

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

290 
and emulating tactic scripts. 

9614  291 

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

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

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

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

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

7167  302 
\end{descr} 
7135  303 

10318  304 
\indexisaratt{tagged}\indexisaratt{untagged} 
9614  305 
\indexisaratt{THEN}\indexisaratt{COMP} 
10318  306 
\indexisaratt{where}\indexisaratt{unfolded}\indexisaratt{folded} 
307 
\indexisaratt{standard}\indexisaratt{elimformat} 

308 
\indexisaratt{novars}\indexisaratt{exported} 

8517  309 
\begin{matharray}{rcl} 
9905  310 
tagged & : & \isaratt \\ 
311 
untagged & : & \isaratt \\[0.5ex] 

9614  312 
THEN & : & \isaratt \\ 
8517  313 
COMP & : & \isaratt \\[0.5ex] 
314 
where & : & \isaratt \\[0.5ex] 

9905  315 
unfolded & : & \isaratt \\ 
316 
folded & : & \isaratt \\[0.5ex] 

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

318 
elim_format & : & \isaratt \\ 
9936  319 
no_vars^* & : & \isaratt \\ 
9905  320 
exported^* & : & \isaratt \\ 
8517  321 
\end{matharray} 
322 

323 
\begin{rail} 

9905  324 
'tagged' (nameref+) 
8517  325 
; 
9905  326 
'untagged' name 
8517  327 
; 
10154  328 
('THEN'  'COMP') ('[' nat ']')? thmref 
8517  329 
; 
330 
'where' (name '=' term * 'and') 

331 
; 

9905  332 
('unfolded'  'folded') thmrefs 
8517  333 
; 
334 
\end{rail} 

335 

336 
\begin{descr} 

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

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

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

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

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

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

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

8517  352 
\item [$standard$] puts a theorem into the standard form of objectrules, just 
353 
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

354 
\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

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

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

8517  362 
\end{descr} 
7135  363 

364 

9606  365 
\section{Tactic emulations}\label{sec:tactics} 
366 

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

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

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

370 
dynamic instantiation within the scope of some subgoal. 

371 

372 
\begin{warn} 

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

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

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

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

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

378 
\end{warn} 

379 

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

381 
named $foo_tac$. 

382 

383 
\indexisarmeth{ruletac}\indexisarmeth{eruletac} 

384 
\indexisarmeth{druletac}\indexisarmeth{fruletac} 

385 
\indexisarmeth{cuttac}\indexisarmeth{thintac} 

9642  386 
\indexisarmeth{subgoaltac}\indexisarmeth{renametac} 
9614  387 
\indexisarmeth{rotatetac}\indexisarmeth{tactic} 
9606  388 
\begin{matharray}{rcl} 
389 
rule_tac^* & : & \isarmeth \\ 

390 
erule_tac^* & : & \isarmeth \\ 

391 
drule_tac^* & : & \isarmeth \\ 

392 
frule_tac^* & : & \isarmeth \\ 

393 
cut_tac^* & : & \isarmeth \\ 

394 
thin_tac^* & : & \isarmeth \\ 

395 
subgoal_tac^* & : & \isarmeth \\ 

9614  396 
rename_tac^* & : & \isarmeth \\ 
397 
rotate_tac^* & : & \isarmeth \\ 

9606  398 
tactic^* & : & \isarmeth \\ 
399 
\end{matharray} 

400 

401 
\railalias{ruletac}{rule\_tac} 

402 
\railterm{ruletac} 

403 

404 
\railalias{eruletac}{erule\_tac} 

405 
\railterm{eruletac} 

406 

407 
\railalias{druletac}{drule\_tac} 

408 
\railterm{druletac} 

409 

410 
\railalias{fruletac}{frule\_tac} 

411 
\railterm{fruletac} 

412 

413 
\railalias{cuttac}{cut\_tac} 

414 
\railterm{cuttac} 

415 

416 
\railalias{thintac}{thin\_tac} 

417 
\railterm{thintac} 

418 

419 
\railalias{subgoaltac}{subgoal\_tac} 

420 
\railterm{subgoaltac} 

421 

9614  422 
\railalias{renametac}{rename\_tac} 
423 
\railterm{renametac} 

424 

425 
\railalias{rotatetac}{rotate\_tac} 

426 
\railterm{rotatetac} 

427 

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

430 
( insts thmref  thmrefs ) 

431 
; 

432 
subgoaltac goalspec? (prop +) 

433 
; 

9614  434 
renametac goalspec? (name +) 
435 
; 

436 
rotatetac goalspec? int? 

437 
; 

9606  438 
'tactic' text 
439 
; 

440 

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

442 
; 

443 
\end{rail} 

444 

445 
\begin{descr} 

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

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

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

9614  449 

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

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

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

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

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

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

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

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

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

460 
\cite[\S3]{isabelleref}. 

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

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

463 
\cite[\S3]{isabelleref}. 

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

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

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

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

469 
\cite[\S3]{isabelleref}. 

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

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

473 
bound values: 

474 

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

476 
{\footnotesize\begin{verbatim} 

477 
val ctxt : Proof.context 

478 
val facts : thm list 

479 
val thm : string > thm 

480 
val thms : string > thm list 

481 
\end{verbatim}} 

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

483 
indicates any current facts for forwardchaining, and 

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

485 
theorems) from the context. 

486 
\end{descr} 

487 

488 

9614  489 
\section{The Simplifier}\label{sec:simplifier} 
7135  490 

7321  491 
\subsection{Simplification methods}\label{sec:simp} 
7315  492 

8483  493 
\indexisarmeth{simp}\indexisarmeth{simpall} 
7315  494 
\begin{matharray}{rcl} 
495 
simp & : & \isarmeth \\ 

8483  496 
simp_all & : & \isarmeth \\ 
7315  497 
\end{matharray} 
498 

8483  499 
\railalias{simpall}{simp\_all} 
500 
\railterm{simpall} 

501 

8704  502 
\railalias{noasm}{no\_asm} 
503 
\railterm{noasm} 

504 

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

506 
\railterm{noasmsimp} 

507 

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

509 
\railterm{noasmuse} 

510 

7315  511 
\begin{rail} 
8706  512 
('simp'  simpall) ('!' ?) opt? (simpmod * ) 
7315  513 
; 
514 

8811  515 
opt: '(' (noasm  noasmsimp  noasmuse) ')' 
8704  516 
; 
9711  517 
simpmod: ('add'  'del'  'only'  'cong' (()  'add'  'del')  
9847  518 
'split' (()  'add'  'del')) ':' thmrefs 
7315  519 
; 
520 
\end{rail} 

521 

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

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

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

530 

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

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

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

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

8483  535 
\item [$simp_all$] is similar to $simp$, but acts on all goals. 
7321  536 
\end{descr} 
537 

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

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

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

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

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

545 
should be used with some care, though. 

7321  546 

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

8704  553 
\texttt{full_simp_tac}). 
554 

555 
\medskip 

556 

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

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

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

8483  561 

562 

563 
\subsection{Declaring rules} 

564 

8667  565 
\indexisarcmd{printsimpset} 
8638  566 
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong} 
7321  567 
\begin{matharray}{rcl} 
10154  568 
print_simpset^* & : & \isarkeep{theory~~proof} \\ 
7321  569 
simp & : & \isaratt \\ 
9711  570 
cong & : & \isaratt \\ 
8483  571 
split & : & \isaratt \\ 
7321  572 
\end{matharray} 
573 

574 
\begin{rail} 

9711  575 
('simp'  'cong'  'split') (()  'add'  'del') 
7321  576 
; 
577 
\end{rail} 

578 

579 
\begin{descr} 

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

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

8547  583 
\item [$simp$] declares simplification rules. 
8638  584 
\item [$cong$] declares congruence rules. 
9711  585 
\item [$split$] declares case split rules. 
7321  586 
\end{descr} 
7319  587 

7315  588 

589 
\subsection{Forward simplification} 

590 

9905  591 
\indexisaratt{simplified} 
7315  592 
\begin{matharray}{rcl} 
9905  593 
simplified & : & \isaratt \\ 
7315  594 
\end{matharray} 
595 

9905  596 
\begin{rail} 
597 
'simplified' opt? 

598 
; 

599 

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

601 
; 

602 
\end{rail} 

7905  603 

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

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

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

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

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

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

611 

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

613 
experimentation only. 

614 
\end{descr} 

7315  615 

616 

9711  617 
\section{Basic equational reasoning}\label{sec:basiceq} 
9614  618 

9703  619 
\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}\indexisaratt{symmetric} 
9614  620 
\begin{matharray}{rcl} 
621 
subst & : & \isarmeth \\ 

622 
hypsubst^* & : & \isarmeth \\ 

9703  623 
split & : & \isarmeth \\ 
9614  624 
symmetric & : & \isaratt \\ 
625 
\end{matharray} 

626 

627 
\begin{rail} 

628 
'subst' thmref 

629 
; 

9799  630 
'split' ('(' 'asm' ')')? thmrefs 
9703  631 
; 
9614  632 
\end{rail} 
633 

634 
These methods and attributes provide basic facilities for equational reasoning 

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

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

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

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

639 

640 
\begin{descr} 

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

642 
which may be either a meta or object equality. 

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

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

647 

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

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

652 

653 

9847  654 
\section{The Classical Reasoner}\label{sec:classical} 
7135  655 

7335  656 
\subsection{Basic methods}\label{sec:classicalbasic} 
7321  657 

7974  658 
\indexisarmeth{rule}\indexisarmeth{intro} 
659 
\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction} 

7321  660 
\begin{matharray}{rcl} 
661 
rule & : & \isarmeth \\ 

662 
intro & : & \isarmeth \\ 

663 
elim & : & \isarmeth \\ 

664 
contradiction & : & \isarmeth \\ 

665 
\end{matharray} 

666 

667 
\begin{rail} 

8547  668 
('rule'  'intro'  'elim') thmrefs? 
7321  669 
; 
670 
\end{rail} 

671 

672 
\begin{descr} 

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

679 
\S\ref{sec:puremethatt}. 

9614  680 

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

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

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

687 
entering the actual subproof. 

9614  688 

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

691 
appear in either order. 

7321  692 
\end{descr} 
693 

694 

7981  695 
\subsection{Automated methods}\label{sec:classicalauto} 
7315  696 

9799  697 
\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow} 
698 
\indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify} 

7321  699 
\begin{matharray}{rcl} 
9780  700 
blast & : & \isarmeth \\ 
701 
fast & : & \isarmeth \\ 

9799  702 
slow & : & \isarmeth \\ 
9780  703 
best & : & \isarmeth \\ 
704 
safe & : & \isarmeth \\ 

705 
clarify & : & \isarmeth \\ 

7321  706 
\end{matharray} 
707 

708 
\begin{rail} 

7905  709 
'blast' ('!' ?) nat? (clamod * ) 
7321  710 
; 
9799  711 
('fast'  'slow'  'best'  'safe'  'clarify') ('!' ?) (clamod * ) 
7321  712 
; 
713 

9408  714 
clamod: (('intro'  'elim'  'dest') ('!'  ()  '?')  'del') ':' thmrefs 
7321  715 
; 
716 
\end{rail} 

717 

718 
\begin{descr} 

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

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

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

724 
facts). 

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

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

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

7321  729 
\end{descr} 
730 

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

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

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

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

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

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

7321  739 

7315  740 

9847  741 
\subsection{Combined automated methods}\label{sec:clasimp} 
7315  742 

9799  743 
\indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp} 
744 
\indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp} 

7321  745 
\begin{matharray}{rcl} 
9606  746 
auto & : & \isarmeth \\ 
7321  747 
force & : & \isarmeth \\ 
9438  748 
clarsimp & : & \isarmeth \\ 
9606  749 
fastsimp & : & \isarmeth \\ 
9799  750 
slowsimp & : & \isarmeth \\ 
751 
bestsimp & : & \isarmeth \\ 

7321  752 
\end{matharray} 
753 

754 
\begin{rail} 

9780  755 
'auto' '!'? (nat nat)? (clasimpmod * ) 
756 
; 

9799  757 
('force'  'clarsimp'  'fastsimp'  'slowsimp'  'bestsimp') '!'? (clasimpmod * ) 
7321  758 
; 
7315  759 

9711  760 
clasimpmod: ('simp' (()  'add'  'del'  'only')  
10031  761 
('cong'  'split') (()  'add'  'del')  
762 
'iff' (((()  'add') '?'?)  'del')  

9408  763 
(('intro'  'elim'  'dest') ('!'  ()  '?')  'del')) ':' thmrefs 
7321  764 
\end{rail} 
7315  765 

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

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

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

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

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

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

9614  775 

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

778 
included as well. 

7321  779 
\end{descr} 
780 

7987  781 

8483  782 
\subsection{Declaring rules}\label{sec:classicalmod} 
7135  783 

8667  784 
\indexisarcmd{printclaset} 
7391  785 
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} 
9936  786 
\indexisaratt{iff}\indexisaratt{rule} 
7321  787 
\begin{matharray}{rcl} 
10154  788 
print_claset^* & : & \isarkeep{theory~~proof} \\ 
7321  789 
intro & : & \isaratt \\ 
790 
elim & : & \isaratt \\ 

791 
dest & : & \isaratt \\ 

9936  792 
rule & : & \isaratt \\ 
7391  793 
iff & : & \isaratt \\ 
7321  794 
\end{matharray} 
7135  795 

7321  796 
\begin{rail} 
9408  797 
('intro'  'elim'  'dest') ('!'  ()  '?') 
7321  798 
; 
9936  799 
'rule' 'del' 
800 
; 

10031  801 
'iff' (((()  'add') '?'?)  'del') 
9936  802 
; 
7321  803 
\end{rail} 
7135  804 

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

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

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

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

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

814 
methods such as $rule$). 

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

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

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

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

821 

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

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

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

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

7321  826 
\end{descr} 
7135  827 

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

828 

9614  829 
%%% Local Variables: 
7135  830 
%%% mode: latex 
831 
%%% TeXmaster: "isarref" 

9614  832 
%%% End: 