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

doc-src/IsarRef/pure.tex

author | wenzelm |

Fri Oct 29 16:48:55 1999 +0200 (1999-10-29) | |

changeset 7974 | 34245feb6e82 |

parent 7895 | 7c492d8bc8e3 |

child 7981 | 5120a2a15d06 |

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

improved;

2 \chapter{Basic Isar Language Elements}\label{ch:pure-syntax}

4 Subsequently, we introduce the main part of the basic Isar theory and proof

5 commands as provided by Isabelle/Pure. Chapter~\ref{ch:gen-tools} describes

6 further Isar elements provided by generic tools and packages (such as the

7 Simplifier) that are either part of Pure Isabelle or pre-loaded by most object

8 logics. Chapter~\ref{ch:hol-tools} refers to actual object-logic specific

9 elements of Isabelle/HOL.

11 \medskip

13 Isar commands may be either \emph{proper} document constructors, or

14 \emph{improper commands}. Some proof methods and attributes introduced later

15 are classified as improper as well. Improper Isar language elements, which

16 are subsequently marked by $^*$, are often helpful when developing proof

17 documents, while their use is usually discouraged for the final outcome.

18 Typical examples are diagnostic commands that print terms or theorems

19 according to the current context; other commands even emulate old-style

20 tactical theorem proving, which facilitates porting of legacy proof scripts.

23 \section{Theory commands}

25 \subsection{Defining theories}\label{sec:begin-thy}

27 \indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context}

28 \begin{matharray}{rcl}

29 \isarcmd{header} & : & \isarkeep{toplevel} \\

30 \isarcmd{theory} & : & \isartrans{\cdot}{theory} \\

31 \isarcmd{context}^* & : & \isartrans{\cdot}{theory} \\

32 \isarcmd{end} & : & \isartrans{theory}{\cdot} \\

33 \end{matharray}

35 Isabelle/Isar ``new-style'' theories are either defined via theory files or

36 interactively. Both actual theory specifications and proofs are handled

37 uniformly --- occasionally definitional mechanisms even require some explicit

38 proof as well. In contrast, ``old-style'' Isabelle theories support batch

39 processing only, with the proof scripts collected in separate ML files.

41 The first actual command of any theory has to be $\THEORY$, starting a new

42 theory based on the merge of existing ones. Just preceding $\THEORY$, there

43 may be an optional $\isarkeyword{header}$ declaration, which is relevant to

44 document preparation only; it acts very much like a special pre-theory markup

45 command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}). The theory

46 context may be also changed by $\CONTEXT$ without creating a new theory. In

47 both cases, $\END$ concludes the theory development; it has to be the very

48 last command in a theory file.

50 \begin{rail}

51 'header' text

52 ;

53 'theory' name '=' (name + '+') filespecs? ':'

54 ;

55 'context' name

56 ;

57 'end'

58 ;;

60 filespecs: 'files' ((name | parname) +);

61 \end{rail}

63 \begin{descr}

64 \item [$\isarkeyword{header}~text$] provides plain text markup just preceding

65 the formal begin of a theory. In actual document preparation the

66 corresponding {\LaTeX} macro \verb,\isamarkupheader, may be redefined to

67 produce chapter or section headings. See also \S\ref{sec:markup-thy} and

68 \S\ref{sec:markup-prf} for further markup commands.

70 \item [$\THEORY~A = B@1 + \cdots + B@n$] commences a new theory $A$ based on

71 existing ones $B@1 + \cdots + B@n$. Isabelle's theory loader system ensures

72 that any of the base theories are properly loaded (and fully up-to-date when

73 $\THEORY$ is executed interactively). The optional $\isarkeyword{files}$

74 specification declares additional dependencies on ML files. Unless put in

75 parentheses, any file will be loaded immediately via $\isarcmd{use}$ (see

76 also \S\ref{sec:ML}). The optional ML file \texttt{$A$.ML} that may be

77 associated with any theory should \emph{not} be included in

78 $\isarkeyword{files}$.

80 \item [$\CONTEXT~B$] enters an existing theory context, basically in read-only

81 mode, so only a limited set of commands may be performed. Just as for

82 $\THEORY$, the theory loader ensures that $B$ is loaded and up-to-date.

84 \item [$\END$] concludes the current theory definition or context switch.

85 Note that this command cannot be undone, instead the whole theory definition

86 has to be retracted.

87 \end{descr}

90 \subsection{Theory markup commands}\label{sec:markup-thy}

92 \indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}

93 \indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{text-raw}

94 \begin{matharray}{rcl}

95 \isarcmd{chapter} & : & \isartrans{theory}{theory} \\

96 \isarcmd{section} & : & \isartrans{theory}{theory} \\

97 \isarcmd{subsection} & : & \isartrans{theory}{theory} \\

98 \isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\

99 \isarcmd{text} & : & \isartrans{theory}{theory} \\

100 \isarcmd{text_raw} & : & \isartrans{theory}{theory} \\

101 \end{matharray}

103 Apart from formal comments (see \S\ref{sec:comments}), markup commands provide

104 another way to insert text into the document generated from a theory (see

105 \cite{isabelle-sys} for more information on Isabelle's document preparation

106 tools).

108 \railalias{textraw}{text\_raw}

109 \railterm{textraw}

111 \begin{rail}

112 ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text' | textraw) text

113 ;

114 \end{rail}

116 \begin{descr}

117 \item [$\isarkeyword{chapter}$, $\isarkeyword{section}$,

118 $\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter

119 and section headings.

120 \item [$\TEXT$] specifies paragraphs of plain text, including references to

121 formal entities.\footnote{The latter feature is not yet supported.

122 Nevertheless, any source text of the form

123 ``\texttt{\at\ttlbrace$\dots$\ttrbrace}'' should be considered as reserved

124 for future use.}

125 \item [$\isarkeyword{text_raw}$] inserts {\LaTeX} source into the output,

126 without additional markup. Thus the full range of document manipulations

127 becomes available. A typical application would be to emit

128 \verb,\begin{comment}, and \verb,\end{comment}, commands to exclude certain

129 parts from the final document.\footnote{This requires the \texttt{comment}

130 {\LaTeX} package to be included}

131 \end{descr}

133 Any markup command (except $\isarkeyword{text_raw}$) corresponds to a {\LaTeX}

134 macro with the name derived from \verb,\isamarkup, (e.g.\

135 \verb,\isamarkupchapter, for $\isarkeyword{chapter}$). The \railqtoken{text}

136 argument is passed to that macro unchanged, i.e.\ any {\LaTeX} commands may be

137 included here.

139 \medskip Further markup commands are available for proofs (see

140 \S\ref{sec:markup-prf}). Also note that the $\isarkeyword{header}$

141 declaration (see \S\ref{sec:begin-thy}) admits to insert document markup

142 elements just preceding the actual theory definition.

145 \subsection{Type classes and sorts}\label{sec:classes}

147 \indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}

148 \begin{matharray}{rcl}

149 \isarcmd{classes} & : & \isartrans{theory}{theory} \\

150 \isarcmd{classrel} & : & \isartrans{theory}{theory} \\

151 \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\

152 \end{matharray}

154 \begin{rail}

155 'classes' (classdecl comment? +)

156 ;

157 'classrel' nameref '<' nameref comment?

158 ;

159 'defaultsort' sort comment?

160 ;

161 \end{rail}

163 \begin{descr}

164 \item [$\isarkeyword{classes}~c<\vec c$] declares class $c$ to be a subclass

165 of existing classes $\vec c$. Cyclic class structures are ruled out.

166 \item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between

167 existing classes $c@1$ and $c@2$. This is done axiomatically! The

168 $\isarkeyword{instance}$ command (see \S\ref{sec:axclass}) provides a way to

169 introduce proven class relations.

170 \item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for

171 any type variables given without sort constraints. Usually, the default

172 sort would be only changed when defining new logics.

173 \end{descr}

176 \subsection{Primitive types and type abbreviations}\label{sec:types-pure}

178 \indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}

179 \begin{matharray}{rcl}

180 \isarcmd{types} & : & \isartrans{theory}{theory} \\

181 \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\

182 \isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\

183 \isarcmd{arities} & : & \isartrans{theory}{theory} \\

184 \end{matharray}

186 \begin{rail}

187 'types' (typespec '=' type infix? comment? +)

188 ;

189 'typedecl' typespec infix? comment?

190 ;

191 'nonterminals' (name +) comment?

192 ;

193 'arities' (nameref '::' arity comment? +)

194 ;

195 \end{rail}

197 \begin{descr}

198 \item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym}

199 $(\vec\alpha)t$ for existing type $\tau$. Unlike actual type definitions,

200 as are available in Isabelle/HOL for example, type synonyms are just purely

201 syntactic abbreviations without any logical significance. Internally, type

202 synonyms are fully expanded, as may be observed when printing terms or

203 theorems.

204 \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor

205 $t$, intended as an actual logical type. Note that object-logics such as

206 Isabelle/HOL override $\isarkeyword{typedecl}$ by their own version.

207 \item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors

208 $\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of

209 Isabelle's inner syntax of terms or types.

210 \item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's order-sorted

211 signature of types by new type constructor arities. This is done

212 axiomatically! The $\isarkeyword{instance}$ command (see

213 \S\ref{sec:axclass}) provides a way to introduce proven type arities.

214 \end{descr}

217 \subsection{Constants and simple definitions}

219 \indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl}

220 \begin{matharray}{rcl}

221 \isarcmd{consts} & : & \isartrans{theory}{theory} \\

222 \isarcmd{defs} & : & \isartrans{theory}{theory} \\

223 \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\

224 \end{matharray}

226 \begin{rail}

227 'consts' (constdecl +)

228 ;

229 'defs' (axmdecl prop comment? +)

230 ;

231 'constdefs' (constdecl prop comment? +)

232 ;

234 constdecl: name '::' type mixfix? comment?

235 ;

236 \end{rail}

238 \begin{descr}

239 \item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type

240 scheme $\sigma$. The optional mixfix annotations may attach concrete syntax

241 to the constants declared.

242 \item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for some

243 existing constant. See \cite[\S6]{isabelle-ref} for more details on the

244 form of equations admitted as constant definitions.

245 \item [$\isarkeyword{constdefs}~c::\sigma~eqn$] combines declarations and

246 definitions of constants, using canonical name $c_def$ for the definitional

247 axiom.

248 \end{descr}

251 \subsection{Syntax and translations}

253 \indexisarcmd{syntax}\indexisarcmd{translations}

254 \begin{matharray}{rcl}

255 \isarcmd{syntax} & : & \isartrans{theory}{theory} \\

256 \isarcmd{translations} & : & \isartrans{theory}{theory} \\

257 \end{matharray}

259 \begin{rail}

260 'syntax' ('(' name 'output'? ')')? (constdecl +)

261 ;

262 'translations' (transpat ('==' | '=>' | '<=') transpat comment? +)

263 ;

264 transpat: ('(' nameref ')')? string

265 ;

266 \end{rail}

268 \begin{descr}

269 \item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$,

270 except that the actual logical signature extension is omitted. Thus the

271 context free grammar of Isabelle's inner syntax may be augmented in

272 arbitrary ways, independently of the logic. The $mode$ argument refers to

273 the print mode that the grammar rules belong; unless there is the

274 \texttt{output} flag given, all productions are added both to the input and

275 output grammar.

276 \item [$\isarkeyword{translations}~rules$] specifies syntactic translation

277 rules (i.e.\ \emph{macros}): parse/print rules (\texttt{==}), parse rules

278 (\texttt{=>}), or print rules (\texttt{<=}). Translation patterns may be

279 prefixed by the syntactic category to be used for parsing; the default is

280 \texttt{logic}.

281 \end{descr}

284 \subsection{Axioms and theorems}

286 \indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas}

287 \begin{matharray}{rcl}

288 \isarcmd{axioms} & : & \isartrans{theory}{theory} \\

289 \isarcmd{theorems} & : & \isartrans{theory}{theory} \\

290 \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\

291 \end{matharray}

293 \begin{rail}

294 'axioms' (axmdecl prop comment? +)

295 ;

296 ('theorems' | 'lemmas') thmdef? thmrefs

297 ;

298 \end{rail}

300 \begin{descr}

301 \item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as

302 axioms of the meta-logic. In fact, axioms are ``axiomatic theorems'', and

303 may be referred later just as any other theorem.

305 Axioms are usually only introduced when declaring new logical systems.

306 Everyday work is typically done the hard way, with proper definitions and

307 actual theorems.

308 \item [$\isarkeyword{theorems}~a = \vec b$] stores lists of existing theorems.

309 Typical applications would also involve attributes, to augment the default

310 Simplifier context, for example.

311 \item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but

312 tags the results as ``lemma''.

313 \end{descr}

316 \subsection{Name spaces}

318 \indexisarcmd{global}\indexisarcmd{local}

319 \begin{matharray}{rcl}

320 \isarcmd{global} & : & \isartrans{theory}{theory} \\

321 \isarcmd{local} & : & \isartrans{theory}{theory} \\

322 \end{matharray}

324 Isabelle organizes any kind of name declarations (of types, constants,

325 theorems etc.) by hierarchically structured name spaces. Normally the user

326 never has to control the behavior of name space entry by hand, yet the

327 following commands provide some way to do so.

329 \begin{descr}

330 \item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current

331 name declaration mode. Initially, theories start in $\isarkeyword{local}$

332 mode, causing all names to be automatically qualified by the theory name.

333 Changing this to $\isarkeyword{global}$ causes all names to be declared

334 without the theory prefix, until $\isarkeyword{local}$ is declared again.

335 \end{descr}

338 \subsection{Incorporating ML code}\label{sec:ML}

340 \indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{ML-setup}\indexisarcmd{setup}

341 \begin{matharray}{rcl}

342 \isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\

343 \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\

344 \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\

345 \isarcmd{setup} & : & \isartrans{theory}{theory} \\

346 \end{matharray}

348 \railalias{MLsetup}{ML\_setup}

349 \railterm{MLsetup}

351 \begin{rail}

352 'use' name

353 ;

354 ('ML' | MLsetup | 'setup') text

355 ;

356 \end{rail}

358 \begin{descr}

359 \item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$.

360 The current theory context (if present) is passed down to the ML session,

361 but must not be modified. Furthermore, the file name is checked with the

362 $\isarkeyword{files}$ dependency declaration given in the theory header (see

363 also \S\ref{sec:begin-thy}).

365 \item [$\isarkeyword{ML}~text$] executes ML commands from $text$. The theory

366 context is passed in the same way as for $\isarkeyword{use}$.

368 \item [$\isarkeyword{ML_setup}~text$] executes ML commands from $text$. The

369 theory context is passed down to the ML session, and fetched back

370 afterwards. Thus $text$ may actually change the theory as a side effect.

372 \item [$\isarkeyword{setup}~text$] changes the current theory context by

373 applying setup functions from $text$, which has to refer to an ML expression

374 of type $(theory \to theory)~list$. The $\isarkeyword{setup}$ command is

375 the canonical way to initialize object-logic specific tools and packages

376 written in ML.

377 \end{descr}

380 \subsection{Syntax translation functions}

382 \indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}

383 \indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}

384 \indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}

385 \begin{matharray}{rcl}

386 \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\

387 \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\

388 \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\

389 \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\

390 \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\

391 \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\

392 \end{matharray}

394 Syntax translation functions written in ML admit almost arbitrary

395 manipulations of Isabelle's inner syntax. Any of the above commands have a

396 single \railqtoken{text} argument that refers to an ML expression of

397 appropriate type. See \cite[\S8]{isabelle-ref} for more information on syntax

398 transformations.

401 \subsection{Oracles}

403 \indexisarcmd{oracle}

404 \begin{matharray}{rcl}

405 \isarcmd{oracle} & : & \isartrans{theory}{theory} \\

406 \end{matharray}

408 Oracles provide an interface to external reasoning systems, without giving up

409 control completely --- each theorem carries a derivation object recording any

410 oracle invocation. See \cite[\S6]{isabelle-ref} for more information.

412 \begin{rail}

413 'oracle' name '=' text comment?

414 ;

415 \end{rail}

417 \begin{descr}

418 \item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML

419 function $text$, which has to be of type $Sign\mathord.sg \times

420 Object\mathord.T \to term$.

421 \end{descr}

424 \section{Proof commands}

426 Proof commands provide transitions of Isar/VM machine configurations, which

427 are block-structured, consisting of a stack of nodes with three main

428 components: logical proof context, current facts, and open goals. Isar/VM

429 transitions are \emph{typed} according to the following three three different

430 modes of operation:

431 \begin{descr}

432 \item [$proof(prove)$] means that a new goal has just been stated that is now

433 to be \emph{proven}; the next command may refine it by some proof method

434 (read: tactic), and enter a sub-proof to establish the actual result.

435 \item [$proof(state)$] is like an internal theory mode: the context may be

436 augmented by \emph{stating} additional assumptions, intermediate result etc.

437 \item [$proof(chain)$] is intermediate between $proof(state)$ and

438 $proof(prove)$: existing facts (i.e.\ the contents of $this$) have been just

439 picked up in order to be used when refining the goal claimed next.

440 \end{descr}

443 \subsection{Proof markup commands}\label{sec:markup-prf}

445 \indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect}

446 \indexisarcmd{txt}\indexisarcmd{txt-raw}

447 \begin{matharray}{rcl}

448 \isarcmd{sect} & : & \isartrans{proof(state)}{proof(state)} \\

449 \isarcmd{subsect} & : & \isartrans{proof(state)}{proof(state)} \\

450 \isarcmd{subsubsect} & : & \isartrans{proof(state)}{proof(state)} \\

451 \isarcmd{txt} & : & \isartrans{proof(state)}{proof(state)} \\

452 \isarcmd{txt_raw} & : & \isartrans{proof(state)}{proof(state)} \\

453 \end{matharray}

455 These markup commands for proof mode closely correspond to the ones of theory

456 mode (see \S\ref{sec:markup-thy}). Note that $\isarkeyword{txt_raw}$ is

457 special in the same way as $\isarkeyword{text_raw}$.

459 \railalias{txtraw}{txt\_raw}

460 \railterm{txtraw}

462 \begin{rail}

463 ('sect' | 'subsect' | 'subsubsect' | 'txt' | txtraw) text

464 ;

465 \end{rail}

468 \subsection{Proof context}\label{sec:proof-context}

470 \indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}

471 \begin{matharray}{rcl}

472 \isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\

473 \isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\

474 \isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\

475 \isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\

476 \end{matharray}

478 The logical proof context consists of fixed variables and assumptions. The

479 former closely correspond to Skolem constants, or meta-level universal

480 quantification as provided by the Isabelle/Pure logical framework.

481 Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in

482 a local object that may be used in the subsequent proof as any other variable

483 or constant. Furthermore, any result $\edrv \phi[x]$ exported from the

484 current context will be universally closed wrt.\ $x$ at the outermost level:

485 $\edrv \All x \phi$; this is expressed using Isabelle's meta-variables.

487 Similarly, introducing some assumption $\chi$ has two effects. On the one

488 hand, a local theorem is created that may be used as a fact in subsequent

489 proof steps. On the other hand, any result $\chi \drv \phi$ exported from the

490 context becomes conditional wrt.\ the assumption: $\edrv \chi \Imp \phi$.

491 Thus, solving an enclosing goal using such a result would basically introduce

492 a new subgoal stemming from the assumption. How this situation is handled

493 depends on the actual version of assumption command used: while $\ASSUMENAME$

494 insists on solving the subgoal by unification with some premise of the goal,

495 $\PRESUMENAME$ leaves the subgoal unchanged in order to be proved later by the

496 user.

498 Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by

499 combining $\FIX x$ with another kind of assumption that causes any

500 hypothetical equation $x \equiv t$ to be eliminated by reflexivity. Thus,

501 exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.

503 \begin{rail}

504 'fix' (vars + 'and') comment?

505 ;

506 ('assume' | 'presume') (assm comment? + 'and')

507 ;

508 'def' thmdecl? \\ var '==' term termpat? comment?

509 ;

511 var: name ('::' type)?

512 ;

513 vars: (name+) ('::' type)?

514 ;

515 assm: thmdecl? (prop proppat? +)

516 ;

517 \end{rail}

519 \begin{descr}

520 \item [$\FIX{x}$] introduces a local \emph{arbitrary, but fixed} variable $x$.

521 \item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] introduce local theorems

522 $\Phi$ by assumption. Subsequent results applied to an enclosing goal

523 (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ expects to be

524 able to unify with existing premises in the goal, while $\PRESUMENAME$

525 leaves $\Phi$ as new subgoals.

527 Several lists of assumptions may be given (separated by

528 $\isarkeyword{and}$); the resulting list of current facts consists of all of

529 these concatenated.

530 \item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.

531 In results exported from the context, $x$ is replaced by $t$. Basically,

532 $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\PRESUME{}{x \equiv t}$, with the

533 resulting hypothetical equation solved by reflexivity.

535 The default name for the definitional equation is $x_def$.

536 \end{descr}

538 The special name $prems$\indexisarthm{prems} refers to all assumptions of the

539 current context as a list of theorems.

542 \subsection{Facts and forward chaining}

544 \indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}

545 \begin{matharray}{rcl}

546 \isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\

547 \isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\

548 \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\

549 \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\

550 \end{matharray}

552 New facts are established either by assumption or proof of local statements.

553 Any fact will usually be involved in further proofs, either as explicit

554 arguments of proof methods or when forward chaining towards the next goal via

555 $\THEN$ (and variants). Note that the special theorem name

556 $this$.\indexisarthm{this} refers to the most recently established facts.

557 \begin{rail}

558 'note' thmdef? thmrefs comment?

559 ;

560 'then' comment?

561 ;

562 ('from' | 'with') thmrefs comment?

563 ;

564 \end{rail}

566 \begin{descr}

567 \item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result

568 as $a$. Note that attributes may be involved as well, both on the left and

569 right hand sides.

570 \item [$\THEN$] indicates forward chaining by the current facts in order to

571 establish the goal to be claimed next. The initial proof method invoked to

572 refine that will be offered the facts to do ``anything appropriate'' (cf.\

573 also \S\ref{sec:proof-steps}). For example, method $rule$ (see

574 \S\ref{sec:pure-meth}) would typically do an elimination rather than an

575 introduction. Automatic methods usually insert the facts into the goal

576 state before operation.

577 \item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is

578 equivalent to $\FROM{this}$.

579 \item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward

580 chaining is from earlier facts together with the current ones.

581 \end{descr}

583 Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth}) expect

584 multiple facts to be given in their proper order, corresponding to a prefix of

585 the premises of the rule involved. Note that positions may be easily skipped

586 using a form like $\FROM{\text{\texttt{_}}~a~b}$, for example. This involves

587 the trivial rule $\PROP\psi \Imp \PROP\psi$, which is bound in Isabelle/Pure

588 as ``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}}

591 \subsection{Goal statements}

593 \indexisarcmd{theorem}\indexisarcmd{lemma}

594 \indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}

595 \begin{matharray}{rcl}

596 \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\

597 \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\

598 \isarcmd{have} & : & \isartrans{proof(state)}{proof(prove)} \\

599 \isarcmd{show} & : & \isartrans{proof(state)}{proof(prove)} \\

600 \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\

601 \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\

602 \end{matharray}

604 Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$

605 and $\LEMMANAME$. New local goals may be claimed within proof mode as well.

606 Four variants are available, indicating whether the result is meant to solve

607 some pending goal and whether forward chaining is employed.

609 \begin{rail}

610 ('theorem' | 'lemma') goal

611 ;

612 ('have' | 'show' | 'hence' | 'thus') goal

613 ;

615 goal: thmdecl? proppat comment?

616 ;

617 \end{rail}

619 \begin{descr}

620 \item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal,

621 eventually resulting in some theorem $\turn \phi$ put back into the theory.

622 \item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as

623 ``lemma''.

624 \item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a

625 theorem with the current assumption context as hypotheses.

626 \item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some

627 pending goal with the result \emph{exported} into the corresponding context

628 (cf.\ \S\ref{sec:proof-context}).

629 \item [$\HENCENAME$] abbreviates $\THEN~\HAVENAME$, i.e.\ claims a local goal

630 to be proven by forward chaining the current facts. Note that $\HENCENAME$

631 is also equivalent to $\FROM{this}~\HAVENAME$.

632 \item [$\THUSNAME$] abbreviates $\THEN~\SHOWNAME$. Note that $\THUSNAME$ is

633 also equivalent to $\FROM{this}~\SHOWNAME$.

634 \end{descr}

637 \subsection{Initial and terminal proof steps}\label{sec:proof-steps}

639 \indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}

640 \indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}

641 \begin{matharray}{rcl}

642 \isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\

643 \isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\

644 \isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\

645 \isarcmd{.\,.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\

646 \isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\

647 \isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\

648 \end{matharray}

650 Arbitrary goal refinement via tactics is considered harmful. Consequently the

651 Isar framework admits proof methods to be invoked in two places only.

652 \begin{enumerate}

653 \item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated

654 goal to a number of sub-goals that are to be solved later. Facts are passed

655 to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode.

657 \item A \emph{terminal} conclusion step $\QED{m@2}$ solves any remaining goals

658 completely. No facts are passed to $m@2$.

659 \end{enumerate}

661 The only other proper way to affect pending goals is by $\SHOWNAME$ (or

662 $\THUSNAME$), which involves an explicit statement of what is to be solved.

664 \medskip

666 Also note that initial proof methods should either solve the goal completely,

667 or constitute some well-understood reduction to new sub-goals. Arbitrary

668 automatic proof tools that are prone leave a large number of badly structured

669 sub-goals are no help in continuing the proof document in any intelligible

670 way. A much better technique would be to $\SHOWNAME$ some non-trivial

671 reduction as an explicit rule, which is solved completely by some automated

672 method, and then applied to some pending goal.

674 \medskip

676 Unless given explicitly by the user, the default initial method is

677 ``$default$'', which is usually set up to apply a single standard elimination

678 or introduction rule according to the topmost symbol involved. There is no

679 separate default terminal method; in any case the final step is to solve all

680 remaining goals by assumption, though.

682 \begin{rail}

683 'proof' interest? meth? comment?

684 ;

685 'qed' meth? comment?

686 ;

687 'by' meth meth? comment?

688 ;

689 ('.' | '..' | 'sorry') comment?

690 ;

692 meth: method interest?

693 ;

694 \end{rail}

696 \begin{descr}

697 \item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for

698 forward chaining are passed if so indicated by $proof(chain)$ mode.

699 \item [$\QED{m@2}$] refines any remaining goals by proof method $m@2$ and

700 concludes the sub-proof by assumption. If the goal had been $\SHOWNAME$ (or

701 $\THUSNAME$), some pending sub-goal is solved as well by the rule resulting

702 from the result \emph{exported} into the enclosing goal context. Thus

703 $\QEDNAME$ may fail for two reasons: either $m@2$ fails, or the resulting

704 rule does not fit to any pending goal\footnote{This includes any additional

705 ``strong'' assumptions as introduced by $\ASSUMENAME$.} of the enclosing

706 context. Debugging such a situation might involve temporarily changing

707 $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing

708 some occurrences of $\ASSUMENAME$ by $\PRESUMENAME$.

709 \item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it

710 abbreviates $\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both

711 methods. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done

712 by expanding its definition; in many cases $\PROOF{m@1}$ is already

713 sufficient to see what is going wrong.

714 \item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it

715 abbreviates $\BY{default}$.

716 \item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it

717 abbreviates $\BY{assumption}$.

718 \item [$\isarkeyword{sorry}$] is a \emph{fake proof}\index{proof!fake};

719 provided that \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$

720 pretends to solve the goal without further ado. Of course, the result is a

721 fake theorem only, involving some oracle in its internal derivation object

722 (this is indicated as ``$[!]$'' in the printed result). The main

723 application of $\isarkeyword{sorry}$ is to support experimentation and

724 top-down proof development.

725 \end{descr}

728 \subsection{Improper proof steps}

730 The following commands emulate unstructured tactic scripts to some extent.

731 While these are anathema for writing proper Isar proof documents, they might

732 come in handy for interactive exploration and debugging.

734 \indexisarcmd{apply}\indexisarcmd{then-apply}\indexisarcmd{back}

735 \begin{matharray}{rcl}

736 \isarcmd{apply}^* & : & \isartrans{proof}{proof} \\

737 \isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\

738 \isarcmd{back}^* & : & \isartrans{proof}{proof} \\

739 \end{matharray}

741 \railalias{thenapply}{then\_apply}

742 \railterm{thenapply}

744 \begin{rail}

745 'apply' method

746 ;

747 thenapply method

748 ;

749 'back'

750 ;

751 \end{rail}

753 \begin{descr}

754 \item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in the plain old

755 tactic sense. Facts for forward chaining are reset.

756 \item [$\isarkeyword{then_apply}~(m)$] is similar to $\isarkeyword{apply}$,

757 but keeps the goal's facts.

758 \item [$\isarkeyword{back}$] does back-tracking over the result sequence of

759 the latest proof command.\footnote{Unlike the ML function \texttt{back}

760 \cite{isabelle-ref}, the Isar command does not search upwards for further

761 branch points.} Basically, any proof command may return multiple results.

762 \end{descr}

765 \subsection{Term abbreviations}\label{sec:term-abbrev}

767 \indexisarcmd{let}

768 \begin{matharray}{rcl}

769 \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\

770 \isarkeyword{is} & : & syntax \\

771 \end{matharray}

773 Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,

774 or by annotating assumptions or goal statements ($\ASSUMENAME$, $\SHOWNAME$

775 etc.) with a list of patterns $\ISS{p@1 \dots}{p@n}$. In both cases,

776 higher-order matching is invoked to bind extra-logical term variables, which

777 may be either named schematic variables of the form $\Var{x}$, or nameless

778 dummies ``\texttt{_}'' (underscore).\indexisarvar{_@\texttt{_}} Note that in

779 the $\LETNAME$ form the patterns occur on the left-hand side, while the

780 $\ISNAME$ patterns are in postfix position.

782 Term abbreviations are quite different from actual local definitions as

783 introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}). The latter are

784 visible within the logic as actual equations, while abbreviations disappear

785 during the input process just after type checking.

787 \begin{rail}

788 'let' ((term + 'as') '=' term comment? + 'and')

789 ;

790 \end{rail}

792 The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or

793 \railnonterm{proppat} (see \S\ref{sec:term-pats}).

795 \begin{descr}

796 \item [$\LET{\vec p = \vec t}$] binds any text variables in patters $\vec p$

797 by simultaneous higher-order matching against terms $\vec t$.

798 \item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the

799 preceding statement. Also note that $\ISNAME$ is not a separate command,

800 but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.).

801 \end{descr}

803 A few \emph{automatic} term abbreviations\index{automatic abbreviation} for

804 goals and facts are available as well. For any open goal,

805 $\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition

806 (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its

807 (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its

808 object-logical statement. The latter two abstract over any meta-level

809 parameters bound by $\Forall$.

811 Fact statements resulting from assumptions or finished goals are bound as

812 $\Var{this_prop}$\indexisarvar{this-prop},

813 $\Var{this_concl}$\indexisarvar{this-concl}, and

814 $\Var{this}$\indexisarvar{this}, similar to $\Var{thesis}$ above. In case

815 $\Var{this}$ refers to an object-logic statement that is an application

816 $f(t)$, then $t$ is bound to the special text variable

817 ``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of

818 this feature are calculational proofs (see \S\ref{sec:calculation}).

821 \subsection{Block structure}

823 \indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}

824 \begin{matharray}{rcl}

825 \isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\

826 \BG & : & \isartrans{proof(state)}{proof(state)} \\

827 \EN & : & \isartrans{proof(state)}{proof(state)} \\

828 \end{matharray}

830 While Isar is inherently block-structured, opening and closing blocks is

831 mostly handled rather casually, with little explicit user-intervention. Any

832 local goal statement automatically opens \emph{two} blocks, which are closed

833 again when concluding the sub-proof (by $\QEDNAME$ etc.). Sections of

834 different context within a sub-proof may be switched via $\isarkeyword{next}$,

835 which is just a single block-close followed by block-open again. Thus the

836 effect of $\isarkeyword{next}$ is a local reset the proof

837 context.\footnote{There is no goal focus involved here!}

839 For slightly more advanced applications, there are explicit block parentheses

840 as well. These typically achieve a stronger forward style of reasoning.

842 \begin{descr}

843 \item [$\isarkeyword{next}$] switches to a fresh block within a sub-proof,

844 resetting the local context to the initial one.

845 \item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and

846 close blocks. Any current facts pass through ``$\isarkeyword{\{\{}$''

847 unchanged, while ``$\isarkeyword{\}\}}$'' causes any result to be

848 \emph{exported} into the enclosing context. Thus fixed variables are

849 generalized, assumptions discharged, and local definitions unfolded (cf.\

850 \S\ref{sec:proof-context}). There is no difference of $\ASSUMENAME$ and

851 $\PRESUMENAME$ in this mode of forward reasoning --- in contrast to plain

852 backward reasoning with the result exported at $\SHOWNAME$ time.

853 \end{descr}

856 \section{Other commands}

858 \subsection{Diagnostics}

860 \indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ}

861 \begin{matharray}{rcl}

862 \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\

863 \isarcmd{term} & : & \isarkeep{theory~|~proof} \\

864 \isarcmd{prop} & : & \isarkeep{theory~|~proof} \\

865 \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\

866 \end{matharray}

868 These commands are not part of the actual Isabelle/Isar syntax, but assist

869 interactive development. Also note that $undo$ does not apply here, since the

870 theory or proof configuration is not changed.

872 \begin{rail}

873 'thm' thmrefs

874 ;

875 'term' term

876 ;

877 'prop' prop

878 ;

879 'typ' type

880 ;

881 \end{rail}

883 \begin{descr}

884 \item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current

885 theory or proof context. Note that any attributes included in the theorem

886 specifications are applied to a temporary context derived from the current

887 theory or proof; the result is discarded, i.e.\ attributes involved in

888 $thms$ do not have any permanent effect.

889 \item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-checks

890 and print terms or propositions according to the current theory or proof

891 context; the inferred type of $t$ is output as well. Note that these

892 commands are also useful in inspecting the current environment of term

893 abbreviations.

894 \item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic

895 according to the current theory or proof context.

896 \end{descr}

899 \subsection{System operations}

901 \indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only}

902 \indexisarcmd{update-thy}\indexisarcmd{update-thy-only}

903 \begin{matharray}{rcl}

904 \isarcmd{cd} & : & \isarkeep{\cdot} \\

905 \isarcmd{pwd} & : & \isarkeep{\cdot} \\

906 \isarcmd{use_thy} & : & \isarkeep{\cdot} \\

907 \isarcmd{use_thy_only} & : & \isarkeep{\cdot} \\

908 \isarcmd{update_thy} & : & \isarkeep{\cdot} \\

909 \isarcmd{update_thy_only} & : & \isarkeep{\cdot} \\

910 \end{matharray}

912 \begin{descr}

913 \item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle

914 process.

915 \item [$\isarkeyword{pwd}~$] prints the current working directory.

916 \item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$,

917 $\isarkeyword{update_thy}$, and $\isarkeyword{update_thy_only}$] load some

918 theory given as $name$ argument. These commands are basically the same as

919 the corresponding ML functions\footnote{For historic reasons, the original

920 ML versions also change the theory context to that of the theory loaded.}

921 (see also \cite[\S1,\S6]{isabelle-ref}). Note that both the ML and Isar

922 versions may load new- and old-style theories alike.

923 \end{descr}

925 Note that these system commands are scarcely used when working with the

926 Proof~General interface, since loading of theories is done fully

927 transparently.

929 %%% Local Variables:

930 %%% mode: latex

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

932 %%% End: