author  wenzelm 
Wed, 04 Oct 2000 21:06:01 +0200  
changeset 10154  05d6ccb2f536 
parent 10031  12fd0fcf755a 
child 10160  bb8f9412fec6 
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. 

9614  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)} \\ 

10154  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). 

9614  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. 

9614  130 

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

9614  133 

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

9614  136 

8547  137 
\item [$trans$] declares theorems as transitivity rules. 
9614  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. 

9614  207 

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

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

8483  210 
\end{descr} 
211 

212 

9614  213 
\section{Generalized existence}\label{sec:obtain} 
7135  214 

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

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

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

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

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

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

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

227 
conclusion. 

8517  228 

229 
\begin{rail} 

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

231 
; 

232 
\end{rail} 

233 

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

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

239 
\quad \BG \\ 

240 
\qquad \FIX{thesis} \\ 

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

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

243 
\quad \EN \\ 

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

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

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

8517  251 

252 
\medskip 

253 

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

255 
metalogical existential quantifiers and conjunctions. This concept has a 

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

257 
introduction) of objectlevel existentials and conjunctions, to elimination 

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

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

8517  261 

262 

10031  263 
\section{Miscellaneous methods and attributes}\label{sec:miscmethods} 
8517  264 

9606  265 
\indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert} 
8517  266 
\indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule} 
267 
\indexisarmeth{fail}\indexisarmeth{succeed} 

268 
\begin{matharray}{rcl} 

269 
unfold & : & \isarmeth \\ 

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

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

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

275 
succeed & : & \isarmeth \\ 

276 
fail & : & \isarmeth \\ 

277 
\end{matharray} 

7135  278 

279 
\begin{rail} 

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

283 

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

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

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

292 
and emulating tactic scripts. 

9614  293 

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

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

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

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

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

7167  304 
\end{descr} 
7135  305 

8517  306 

307 
\indexisaratt{standard} 

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

308 
\indexisaratt{elimformat} 
9232  309 
\indexisaratt{novars} 
8517  310 

9614  311 
\indexisaratt{THEN}\indexisaratt{COMP} 
9905  312 
\indexisaratt{where}\indexisaratt{tagged}\indexisaratt{untagged} 
313 
\indexisaratt{unfolded}\indexisaratt{folded}\indexisaratt{exported} 

8517  314 
\begin{matharray}{rcl} 
9905  315 
tagged & : & \isaratt \\ 
316 
untagged & : & \isaratt \\[0.5ex] 

9614  317 
THEN & : & \isaratt \\ 
8517  318 
COMP & : & \isaratt \\[0.5ex] 
319 
where & : & \isaratt \\[0.5ex] 

9905  320 
unfolded & : & \isaratt \\ 
321 
folded & : & \isaratt \\[0.5ex] 

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

323 
elim_format & : & \isaratt \\ 
9936  324 
no_vars^* & : & \isaratt \\ 
9905  325 
exported^* & : & \isaratt \\ 
8517  326 
\end{matharray} 
327 

328 
\begin{rail} 

9905  329 
'tagged' (nameref+) 
8517  330 
; 
9905  331 
'untagged' name 
8517  332 
; 
10154  333 
('THEN'  'COMP') ('[' nat ']')? thmref 
8517  334 
; 
335 
'where' (name '=' term * 'and') 

336 
; 

9905  337 
('unfolded'  'folded') thmrefs 
8517  338 
; 
339 
\end{rail} 

340 

341 
\begin{descr} 

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

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

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

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

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

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

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

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

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

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

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

8517  367 
\end{descr} 
7135  368 

369 

9606  370 
\section{Tactic emulations}\label{sec:tactics} 
371 

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

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

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

375 
dynamic instantiation within the scope of some subgoal. 

376 

377 
\begin{warn} 

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

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

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

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

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

383 
\end{warn} 

384 

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

386 
named $foo_tac$. 

387 

388 
\indexisarmeth{ruletac}\indexisarmeth{eruletac} 

389 
\indexisarmeth{druletac}\indexisarmeth{fruletac} 

390 
\indexisarmeth{cuttac}\indexisarmeth{thintac} 

9642  391 
\indexisarmeth{subgoaltac}\indexisarmeth{renametac} 
9614  392 
\indexisarmeth{rotatetac}\indexisarmeth{tactic} 
9606  393 
\begin{matharray}{rcl} 
394 
rule_tac^* & : & \isarmeth \\ 

395 
erule_tac^* & : & \isarmeth \\ 

396 
drule_tac^* & : & \isarmeth \\ 

397 
frule_tac^* & : & \isarmeth \\ 

398 
cut_tac^* & : & \isarmeth \\ 

399 
thin_tac^* & : & \isarmeth \\ 

400 
subgoal_tac^* & : & \isarmeth \\ 

9614  401 
rename_tac^* & : & \isarmeth \\ 
402 
rotate_tac^* & : & \isarmeth \\ 

9606  403 
tactic^* & : & \isarmeth \\ 
404 
\end{matharray} 

405 

406 
\railalias{ruletac}{rule\_tac} 

407 
\railterm{ruletac} 

408 

409 
\railalias{eruletac}{erule\_tac} 

410 
\railterm{eruletac} 

411 

412 
\railalias{druletac}{drule\_tac} 

413 
\railterm{druletac} 

414 

415 
\railalias{fruletac}{frule\_tac} 

416 
\railterm{fruletac} 

417 

418 
\railalias{cuttac}{cut\_tac} 

419 
\railterm{cuttac} 

420 

421 
\railalias{thintac}{thin\_tac} 

422 
\railterm{thintac} 

423 

424 
\railalias{subgoaltac}{subgoal\_tac} 

425 
\railterm{subgoaltac} 

426 

9614  427 
\railalias{renametac}{rename\_tac} 
428 
\railterm{renametac} 

429 

430 
\railalias{rotatetac}{rotate\_tac} 

431 
\railterm{rotatetac} 

432 

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

435 
( insts thmref  thmrefs ) 

436 
; 

437 
subgoaltac goalspec? (prop +) 

438 
; 

9614  439 
renametac goalspec? (name +) 
440 
; 

441 
rotatetac goalspec? int? 

442 
; 

9606  443 
'tactic' text 
444 
; 

445 

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

447 
; 

448 
\end{rail} 

449 

450 
\begin{descr} 

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

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

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

9614  454 

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

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

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

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

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

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

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

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

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

465 
\cite[\S3]{isabelleref}. 

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

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

468 
\cite[\S3]{isabelleref}. 

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

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

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

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

474 
\cite[\S3]{isabelleref}. 

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

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

478 
bound values: 

479 

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

481 
{\footnotesize\begin{verbatim} 

482 
val ctxt : Proof.context 

483 
val facts : thm list 

484 
val thm : string > thm 

485 
val thms : string > thm list 

486 
\end{verbatim}} 

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

488 
indicates any current facts for forwardchaining, and 

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

490 
theorems) from the context. 

491 
\end{descr} 

492 

493 

9614  494 
\section{The Simplifier}\label{sec:simplifier} 
7135  495 

7321  496 
\subsection{Simplification methods}\label{sec:simp} 
7315  497 

8483  498 
\indexisarmeth{simp}\indexisarmeth{simpall} 
7315  499 
\begin{matharray}{rcl} 
500 
simp & : & \isarmeth \\ 

8483  501 
simp_all & : & \isarmeth \\ 
7315  502 
\end{matharray} 
503 

8483  504 
\railalias{simpall}{simp\_all} 
505 
\railterm{simpall} 

506 

8704  507 
\railalias{noasm}{no\_asm} 
508 
\railterm{noasm} 

509 

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

511 
\railterm{noasmsimp} 

512 

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

514 
\railterm{noasmuse} 

515 

7315  516 
\begin{rail} 
8706  517 
('simp'  simpall) ('!' ?) opt? (simpmod * ) 
7315  518 
; 
519 

8811  520 
opt: '(' (noasm  noasmsimp  noasmuse) ')' 
8704  521 
; 
9711  522 
simpmod: ('add'  'del'  'only'  'cong' (()  'add'  'del')  
9847  523 
'split' (()  'add'  'del')) ':' thmrefs 
7315  524 
; 
525 
\end{rail} 

526 

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

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

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

535 

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

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

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

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

8483  540 
\item [$simp_all$] is similar to $simp$, but acts on all goals. 
7321  541 
\end{descr} 
542 

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

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

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

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

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

550 
should be used with some care, though. 

7321  551 

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

8704  558 
\texttt{full_simp_tac}). 
559 

560 
\medskip 

561 

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

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

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

8483  566 

567 

568 
\subsection{Declaring rules} 

569 

8667  570 
\indexisarcmd{printsimpset} 
8638  571 
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong} 
7321  572 
\begin{matharray}{rcl} 
10154  573 
print_simpset^* & : & \isarkeep{theory~~proof} \\ 
7321  574 
simp & : & \isaratt \\ 
9711  575 
cong & : & \isaratt \\ 
8483  576 
split & : & \isaratt \\ 
7321  577 
\end{matharray} 
578 

579 
\begin{rail} 

9711  580 
('simp'  'cong'  'split') (()  'add'  'del') 
7321  581 
; 
582 
\end{rail} 

583 

584 
\begin{descr} 

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

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

8547  588 
\item [$simp$] declares simplification rules. 
8638  589 
\item [$cong$] declares congruence rules. 
9711  590 
\item [$split$] declares case split rules. 
7321  591 
\end{descr} 
7319  592 

7315  593 

594 
\subsection{Forward simplification} 

595 

9905  596 
\indexisaratt{simplified} 
7315  597 
\begin{matharray}{rcl} 
9905  598 
simplified & : & \isaratt \\ 
7315  599 
\end{matharray} 
600 

9905  601 
\begin{rail} 
602 
'simplified' opt? 

603 
; 

604 

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

606 
; 

607 
\end{rail} 

7905  608 

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

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

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

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

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

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

616 

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

618 
experimentation only. 

619 
\end{descr} 

7315  620 

621 

9711  622 
\section{Basic equational reasoning}\label{sec:basiceq} 
9614  623 

9703  624 
\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}\indexisaratt{symmetric} 
9614  625 
\begin{matharray}{rcl} 
626 
subst & : & \isarmeth \\ 

627 
hypsubst^* & : & \isarmeth \\ 

9703  628 
split & : & \isarmeth \\ 
9614  629 
symmetric & : & \isaratt \\ 
630 
\end{matharray} 

631 

632 
\begin{rail} 

633 
'subst' thmref 

634 
; 

9799  635 
'split' ('(' 'asm' ')')? thmrefs 
9703  636 
; 
9614  637 
\end{rail} 
638 

639 
These methods and attributes provide basic facilities for equational reasoning 

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

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

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

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

644 

645 
\begin{descr} 

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

647 
which may be either a meta or object equality. 

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

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

652 

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

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

657 

658 

9847  659 
\section{The Classical Reasoner}\label{sec:classical} 
7135  660 

7335  661 
\subsection{Basic methods}\label{sec:classicalbasic} 
7321  662 

7974  663 
\indexisarmeth{rule}\indexisarmeth{intro} 
664 
\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction} 

7321  665 
\begin{matharray}{rcl} 
666 
rule & : & \isarmeth \\ 

667 
intro & : & \isarmeth \\ 

668 
elim & : & \isarmeth \\ 

669 
contradiction & : & \isarmeth \\ 

670 
\end{matharray} 

671 

672 
\begin{rail} 

8547  673 
('rule'  'intro'  'elim') thmrefs? 
7321  674 
; 
675 
\end{rail} 

676 

677 
\begin{descr} 

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

684 
\S\ref{sec:puremethatt}. 

9614  685 

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

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

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

692 
entering the actual subproof. 

9614  693 

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

696 
appear in either order. 

7321  697 
\end{descr} 
698 

699 

7981  700 
\subsection{Automated methods}\label{sec:classicalauto} 
7315  701 

9799  702 
\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow} 
703 
\indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify} 

7321  704 
\begin{matharray}{rcl} 
9780  705 
blast & : & \isarmeth \\ 
706 
fast & : & \isarmeth \\ 

9799  707 
slow & : & \isarmeth \\ 
9780  708 
best & : & \isarmeth \\ 
709 
safe & : & \isarmeth \\ 

710 
clarify & : & \isarmeth \\ 

7321  711 
\end{matharray} 
712 

713 
\begin{rail} 

7905  714 
'blast' ('!' ?) nat? (clamod * ) 
7321  715 
; 
9799  716 
('fast'  'slow'  'best'  'safe'  'clarify') ('!' ?) (clamod * ) 
7321  717 
; 
718 

9408  719 
clamod: (('intro'  'elim'  'dest') ('!'  ()  '?')  'del') ':' thmrefs 
7321  720 
; 
721 
\end{rail} 

722 

723 
\begin{descr} 

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

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

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

729 
facts). 

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

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

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

7321  734 
\end{descr} 
735 

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

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

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

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

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

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

7321  744 

7315  745 

9847  746 
\subsection{Combined automated methods}\label{sec:clasimp} 
7315  747 

9799  748 
\indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp} 
749 
\indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp} 

7321  750 
\begin{matharray}{rcl} 
9606  751 
auto & : & \isarmeth \\ 
7321  752 
force & : & \isarmeth \\ 
9438  753 
clarsimp & : & \isarmeth \\ 
9606  754 
fastsimp & : & \isarmeth \\ 
9799  755 
slowsimp & : & \isarmeth \\ 
756 
bestsimp & : & \isarmeth \\ 

7321  757 
\end{matharray} 
758 

759 
\begin{rail} 

9780  760 
'auto' '!'? (nat nat)? (clasimpmod * ) 
761 
; 

9799  762 
('force'  'clarsimp'  'fastsimp'  'slowsimp'  'bestsimp') '!'? (clasimpmod * ) 
7321  763 
; 
7315  764 

9711  765 
clasimpmod: ('simp' (()  'add'  'del'  'only')  
10031  766 
('cong'  'split') (()  'add'  'del')  
767 
'iff' (((()  'add') '?'?)  'del')  

9408  768 
(('intro'  'elim'  'dest') ('!'  ()  '?')  'del')) ':' thmrefs 
7321  769 
\end{rail} 
7315  770 

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

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

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

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

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

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

9614  780 

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

783 
included as well. 

7321  784 
\end{descr} 
785 

7987  786 

8483  787 
\subsection{Declaring rules}\label{sec:classicalmod} 
7135  788 

8667  789 
\indexisarcmd{printclaset} 
7391  790 
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} 
9936  791 
\indexisaratt{iff}\indexisaratt{rule} 
7321  792 
\begin{matharray}{rcl} 
10154  793 
print_claset^* & : & \isarkeep{theory~~proof} \\ 
7321  794 
intro & : & \isaratt \\ 
795 
elim & : & \isaratt \\ 

796 
dest & : & \isaratt \\ 

9936  797 
rule & : & \isaratt \\ 
7391  798 
iff & : & \isaratt \\ 
7321  799 
\end{matharray} 
7135  800 

7321  801 
\begin{rail} 
9408  802 
('intro'  'elim'  'dest') ('!'  ()  '?') 
7321  803 
; 
9936  804 
'rule' 'del' 
805 
; 

10031  806 
'iff' (((()  'add') '?'?)  'del') 
9936  807 
; 
7321  808 
\end{rail} 
7135  809 

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

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

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

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

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

819 
methods such as $rule$). 

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

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

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

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

826 

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

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

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

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

7321  831 
\end{descr} 
7135  832 

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

833 

9614  834 
%%% Local Variables: 
7135  835 
%%% mode: latex 
836 
%%% TeXmaster: "isarref" 

9614  837 
%%% End: 