summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/IsarRef/generic.tex

author | wenzelm |

Mon Feb 07 18:38:51 2000 +0100 (2000-02-07) | |

changeset 8203 | 2fcc6017cb72 |

parent 8195 | af2575a5c5ae |

child 8483 | b437907f9b26 |

permissions | -rw-r--r-- |

intro/elim/dest attributes: changed ! / !! flags to ? / ??;

2 \chapter{Generic Tools and Packages}\label{ch:gen-tools}

4 \section{Basic proof methods}\label{sec:pure-meth}

6 \indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}

7 \indexisarmeth{assumption}\indexisarmeth{this}

8 \indexisarmeth{fold}\indexisarmeth{unfold}

9 \indexisarmeth{rule}\indexisarmeth{erule}

10 \begin{matharray}{rcl}

11 - & : & \isarmeth \\

12 assumption & : & \isarmeth \\

13 this & : & \isarmeth \\

14 rule & : & \isarmeth \\

15 erule^* & : & \isarmeth \\[0.5ex]

16 fold & : & \isarmeth \\

17 unfold & : & \isarmeth \\[0.5ex]

18 succeed & : & \isarmeth \\

19 fail & : & \isarmeth \\

20 \end{matharray}

22 \begin{rail}

23 ('fold' | 'unfold' | 'rule' | 'erule') thmrefs

24 ;

25 \end{rail}

27 \begin{descr}

28 \item [``$-$''] does nothing but insert the forward chaining facts as premises

29 into the goal. Note that command $\PROOFNAME$ without any method actually

30 performs a single reduction step using the $rule$ method (see below); thus a

31 plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than

32 $\PROOFNAME$ alone.

33 \item [$assumption$] solves some goal by assumption. Any facts given are

34 guaranteed to participate in the refinement.

35 \item [$this$] applies the current facts directly as rules. Note that

36 ``$\DOT$'' (dot) abbreviates $\BY{this}$.

37 \item [$rule~thms$] applies some rule given as argument in backward manner;

38 facts are used to reduce the rule before applying it to the goal. Thus

39 $rule$ without facts is plain \emph{introduction}, while with facts it

40 becomes a (generalized) \emph{elimination}.

42 Note that the classical reasoner introduces another version of $rule$ that

43 is able to pick appropriate rules automatically, whenever $thms$ are omitted

44 (see \S\ref{sec:classical-basic}); that method is the default for

45 $\PROOFNAME$ steps. Note that ``$\DDOT$'' (double-dot) abbreviates

46 $\BY{default}$.

47 \item [$erule~thms$] is similar to $rule$, but applies rules by

48 elim-resolution. This is an improper method, mainly for experimentation and

49 porting of old scripts. Actual elimination proofs are usually done with

50 $rule$ (single step, involving facts) or $elim$ (repeated steps, see

51 \S\ref{sec:classical-basic}).

52 \item [$unfold~thms$ and $fold~thms$] expand and fold back again the given

53 meta-level definitions throughout all goals; any facts provided are inserted

54 into the goal and subject to rewriting as well.

55 \item [$succeed$] yields a single (unchanged) result; it is the identity of

56 the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).

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

58 ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).

59 \end{descr}

62 \section{Miscellaneous attributes}

64 \indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}

65 \indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}

66 \indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}

67 \indexisaratt{unfold}\indexisaratt{fold}

68 \begin{matharray}{rcl}

69 tag & : & \isaratt \\

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

71 OF & : & \isaratt \\

72 RS & : & \isaratt \\

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

74 of & : & \isaratt \\

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

76 unfold & : & \isaratt \\

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

78 standard & : & \isaratt \\

79 elimify & : & \isaratt \\

80 export^* & : & \isaratt \\

81 transfer & : & \isaratt \\[0.5ex]

82 \end{matharray}

84 \begin{rail}

85 ('tag' | 'untag') (nameref+)

86 ;

87 'OF' thmrefs

88 ;

89 ('RS' | 'COMP') nat? thmref

90 ;

91 'of' (inst * ) ('concl' ':' (inst * ))?

92 ;

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

94 ;

95 ('unfold' | 'fold') thmrefs

96 ;

98 inst: underscore | term

99 ;

100 \end{rail}

102 \begin{descr}

103 \item [$tag~tags$ and $untag~tags$] add and remove $tags$ of the theorem,

104 respectively. Tags may be any list of strings that serve as comment for

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

106 result).

107 \item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules. $OF$ applies

108 $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note

109 the reversed order). Note that premises may be skipped by including

110 ``$\_$'' (underscore) as argument.

112 $RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$

113 that skips the automatic lifting process that is normally intended (cf.\

114 \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}).

116 \item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named

117 instantiation, respectively. The terms given in $of$ are substituted for

118 any schematic variables occurring in a theorem from left to right;

119 ``\texttt{_}'' (underscore) indicates to skip a position. Arguments

120 following a ``$concl\colon$'' specification refer to positions of the

121 conclusion of a rule.

123 \item [$unfold~thms$ and $fold~thms$] expand and fold back again the given

124 meta-level definitions throughout a rule.

126 \item [$standard$] puts a theorem into the standard form of object-rules, just

127 as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).

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

130 ML function \texttt{make\_elim} (see \cite{isabelle-ref}).

132 \item [$export$] lifts a local result out of the current proof context,

133 generalizing all fixed variables and discharging all assumptions. Note that

134 (partial) export is usually done automatically behind the scenes. This

135 attribute is mainly for experimentation.

137 \item [$transfer$] promotes a theorem to the current theory context, which has

138 to enclose the former one. Normally, this is done automatically when rules

139 are joined by inference.

141 \end{descr}

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

146 \indexisarcmd{also}\indexisarcmd{finally}\indexisaratt{trans}

147 \begin{matharray}{rcl}

148 \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\

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

150 trans & : & \isaratt \\

151 \end{matharray}

153 Calculational proof is forward reasoning with implicit application of

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

155 an auxiliary register $calculation$\indexisarthm{calculation} for accumulating

156 results obtained by transitivity composed with the current result. Command

157 $\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the

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

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

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

161 $\HAVENAME$, $\SHOWNAME$ etc.

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

164 application with calculational proofs. It automatically refers to the

165 argument\footnote{The argument of a curried infix expression is its right-hand

166 side.} of the preceding statement.

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

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

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

171 being able to nest calculations, there is no separate \emph{begin-calculation}

172 command required.

174 \begin{rail}

175 ('also' | 'finally') transrules? comment?

176 ;

177 'trans' (() | 'add' ':' | 'del' ':') thmrefs

178 ;

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

181 ;

182 \end{rail}

184 \begin{descr}

185 \item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as

186 follows. The first occurrence of $\ALSO$ in some calculational thread

187 initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same

188 level of block-structure updates $calculation$ by some transitivity rule

189 applied to $calculation$ and $this$ (in that order). Transitivity rules are

190 picked from the current context plus those given as $thms$ (the latter have

191 precedence).

193 \item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as

194 $\ALSO$, and concludes the current calculational thread. The final result

195 is exhibited as fact for forward chaining towards the next goal. Basically,

196 $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that

197 ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and

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

199 calculational proofs.

201 \item [$trans$] maintains the set of transitivity rules of the theory or proof

202 context, by adding or deleting theorems (the default is to add).

203 \end{descr}

205 %FIXME

206 %See theory \texttt{HOL/Isar_examples/Group} for a simple application of

207 %calculations for basic equational reasoning.

208 %\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced

209 %calculational steps in combination with natural deduction.

212 \section{Axiomatic Type Classes}\label{sec:axclass}

214 \indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}

215 \begin{matharray}{rcl}

216 \isarcmd{axclass} & : & \isartrans{theory}{theory} \\

217 \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\

218 intro_classes & : & \isarmeth \\

219 \end{matharray}

221 Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}

222 interface to type classes (cf.~\S\ref{sec:classes}). Thus any object logic

223 may make use of this light-weight mechanism of abstract theories. See

224 \cite{Wenzel:1997:TPHOL} for more information. There is also a tutorial on

225 \emph{Using Axiomatic Type Classes in Isabelle} that is part of the standard

226 Isabelle documentation.

227 %FIXME cite

229 \begin{rail}

230 'axclass' classdecl (axmdecl prop comment? +)

231 ;

232 'instance' (nameref '<' nameref | nameref '::' simplearity) comment?

233 ;

234 \end{rail}

236 \begin{descr}

237 \item [$\isarkeyword{axclass}~c < \vec c~axms$] defines an axiomatic type

238 class as the intersection of existing classes, with additional axioms

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

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

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

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

243 class.

245 \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::

246 (\vec s)c$] setup up a goal stating the class relation or type arity. The

247 proof would usually proceed by $intro_classes$, and then establish the

248 characteristic theorems of the type classes involved. After finishing the

249 proof, the theory will be augmented by a type signature declaration

250 corresponding to the resulting theorem.

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

252 this theory.

253 \end{descr}

255 %FIXME

256 %See theory \texttt{HOL/Isar_examples/Group} for a simple example of using

257 %axiomatic type classes, including instantiation proofs.

260 \section{The Simplifier}

262 \subsection{Simplification methods}\label{sec:simp}

264 \indexisarmeth{simp}

265 \begin{matharray}{rcl}

266 simp & : & \isarmeth \\

267 \end{matharray}

269 \begin{rail}

270 'simp' ('!' ?) (simpmod * )

271 ;

273 simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs

274 ;

275 \end{rail}

277 \begin{descr}

278 \item [$simp$] invokes Isabelle's simplifier, after modifying the context by

279 adding or deleting rules as specified. The \railtoken{only} modifier first

280 removes all other rewrite rules and congruences, and then is like

281 \railtoken{add}. In contrast, \railtoken{other} ignores its arguments;

282 nevertheless there may be side-effects on the context via

283 attributes.\footnote{This provides a back door for arbitrary context

284 manipulation.}

286 The $simp$ method is based on \texttt{asm_full_simp_tac}

287 \cite[\S10]{isabelle-ref}, but is much better behaved in practice. Just the

288 local premises of the actual goal are involved by default. Additional facts

289 may be inserted via forward-chaining (using $\THEN$, $\FROMNAME$ etc.). The

290 full context of assumptions is only included in the $simp!$ version, which

291 should be used with care.

292 \end{descr}

294 \subsection{Modifying the context}

296 \indexisaratt{simp}

297 \begin{matharray}{rcl}

298 simp & : & \isaratt \\

299 \end{matharray}

301 \begin{rail}

302 'simp' (() | 'add' | 'del')

303 ;

304 \end{rail}

306 \begin{descr}

307 \item [$simp$] adds or deletes rules from the theory or proof context (the

308 default is to add).

309 \end{descr}

312 \subsection{Forward simplification}

314 \indexisaratt{simplify}\indexisaratt{asm-simplify}

315 \indexisaratt{full-simplify}\indexisaratt{asm-full-simplify}

316 \begin{matharray}{rcl}

317 simplify & : & \isaratt \\

318 asm_simplify & : & \isaratt \\

319 full_simplify & : & \isaratt \\

320 asm_full_simplify & : & \isaratt \\

321 \end{matharray}

323 These attributes provide forward rules for simplification, which should be

324 used only very rarely. There are no separate options for adding or deleting

325 simplification rules locally.

327 See the ML functions of the same name in \cite[\S10]{isabelle-ref} for more

328 information.

331 \section{The Classical Reasoner}

333 \subsection{Basic methods}\label{sec:classical-basic}

335 \indexisarmeth{rule}\indexisarmeth{intro}

336 \indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction}

337 \begin{matharray}{rcl}

338 rule & : & \isarmeth \\

339 intro & : & \isarmeth \\

340 elim & : & \isarmeth \\

341 contradiction & : & \isarmeth \\

342 \end{matharray}

344 \begin{rail}

345 ('rule' | 'intro' | 'elim') thmrefs

346 ;

347 \end{rail}

349 \begin{descr}

350 \item [$rule$] as offered by the classical reasoner is a refinement over the

351 primitive one (see \S\ref{sec:pure-meth}). In case that no rules are

352 provided as arguments, it automatically determines elimination and

353 introduction rules from the context (see also \S\ref{sec:classical-mod}).

354 In that form it is the default method for basic proof steps, such as

355 $\PROOFNAME$ and ``$\DDOT$'' (two dots).

357 \item [$intro$ and $elim$] repeatedly refine some goal by intro- or

358 elim-resolution, after having inserted any facts. Omitting the arguments

359 refers to any suitable rules from the context, otherwise only the explicitly

360 given ones may be applied. The latter form admits better control of what

361 actually happens, thus it is very appropriate as an initial method for

362 $\PROOFNAME$ that splits up certain connectives of the goal, before entering

363 the actual sub-proof.

365 \item [$contradiction$] solves some goal by contradiction, deriving any result

366 from both $\neg A$ and $A$. Facts, which are guaranteed to participate, may

367 appear in either order.

368 \end{descr}

371 \subsection{Automated methods}\label{sec:classical-auto}

373 \indexisarmeth{blast}

374 \indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow-best}

375 \begin{matharray}{rcl}

376 blast & : & \isarmeth \\

377 fast & : & \isarmeth \\

378 best & : & \isarmeth \\

379 slow & : & \isarmeth \\

380 slow_best & : & \isarmeth \\

381 \end{matharray}

383 \railalias{slowbest}{slow\_best}

384 \railterm{slowbest}

386 \begin{rail}

387 'blast' ('!' ?) nat? (clamod * )

388 ;

389 ('fast' | 'best' | 'slow' | slowbest) ('!' ?) (clamod * )

390 ;

392 clamod: (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del') ':' thmrefs

393 ;

394 \end{rail}

396 \begin{descr}

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

398 in \cite[\S11]{isabelle-ref}). The optional argument specifies a

399 user-supplied search bound (default 20).

400 \item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical

401 reasoner (see \cite[\S11]{isabelle-ref}, tactic \texttt{fast_tac} etc).

402 \end{descr}

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

405 rules. There semantics is analogous to the attributes given in

406 \S\ref{sec:classical-mod}. Facts provided by forward chaining are inserted

407 into the goal before doing the search. The ``!''~argument causes the full

408 context of assumptions to be included as well.\footnote{This is slightly less

409 hazardous than for the Simplifier (see \S\ref{sec:simp}).}

412 \subsection{Combined automated methods}

414 \indexisarmeth{auto}\indexisarmeth{force}

415 \begin{matharray}{rcl}

416 force & : & \isarmeth \\

417 auto & : & \isarmeth \\

418 \end{matharray}

420 \begin{rail}

421 ('force' | 'auto') ('!' ?) (clasimpmod * )

422 ;

424 clasimpmod: ('simp' ('add' | 'del' | 'only') | 'other' |

425 (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del')) ':' thmrefs

426 \end{rail}

428 \begin{descr}

429 \item [$force$ and $auto$] provide access to Isabelle's combined

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

431 \texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information. The

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

433 \S\ref{sec:classical-auto}. Just note that the ones related to the

434 Simplifier are prefixed by \railtoken{simp} here.

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

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

438 included as well.

439 \end{descr}

442 \subsection{Modifying the context}\label{sec:classical-mod}

444 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}

445 \indexisaratt{iff}\indexisaratt{delrule}

446 \begin{matharray}{rcl}

447 intro & : & \isaratt \\

448 elim & : & \isaratt \\

449 dest & : & \isaratt \\

450 iff & : & \isaratt \\

451 delrule & : & \isaratt \\

452 \end{matharray}

454 \begin{rail}

455 ('intro' | 'elim' | 'dest') (() | '?' | '??')

456 ;

457 \end{rail}

459 \begin{descr}

460 \item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,

461 respectively. By default, rules are considered as \emph{safe}, while a

462 single ``?'' classifies as \emph{unsafe}, and ``??'' as \emph{extra} (i.e.\

463 not applied in the search-oriented automated methods, but only in

464 single-step methods such as $rule$).

466 \item [$iff$] declares equations both as rewrite rules for the simplifier and

467 classical reasoning rules.

469 \item [$delrule$] deletes introduction or elimination rules from the context.

470 Note that destruction rules would have to be turned into elimination rules

471 first, e.g.\ by using the $elimify$ attribute.

472 \end{descr}

475 %%% Local Variables:

476 %%% mode: latex

477 %%% TeX-master: "isar-ref"

478 %%% End: