author  wenzelm 
Thu, 06 Jul 2000 18:11:48 +0200  
changeset 9273  798673f65f02 
parent 9238  ad37b21c0dc6 
child 9308  4adf25becaa4 
permissions  rwrr 
7046  1 

7895  2 
\chapter{Basic Isar Language Elements}\label{ch:puresyntax} 
7167  3 

8515  4 
Subsequently, we introduce the main part of Pure Isar theory and proof 
8547  5 
commands, together with fundamental proof methods and attributes. 
8515  6 
Chapter~\ref{ch:gentools} describes further Isar elements provided by generic 
7 
tools and packages (such as the Simplifier) that are either part of Pure 

8 
Isabelle or preinstalled by most object logics. Chapter~\ref{ch:holtools} 

9 
refers to actual objectlogic specific elements of Isabelle/HOL. 

7046  10 

7167  11 
\medskip 
12 

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

7466  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 

7981  17 
documents, while their use is discouraged for the final outcome. Typical 
18 
examples are diagnostic commands that print terms or theorems according to the 

19 
current context; other commands even emulate oldstyle tactical theorem 

8547  20 
proving. 
7167  21 

7134  22 

23 
\section{Theory commands} 

24 

7167  25 
\subsection{Defining theories}\label{sec:beginthy} 
7134  26 

7895  27 
\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context} 
7134  28 
\begin{matharray}{rcl} 
7895  29 
\isarcmd{header} & : & \isarkeep{toplevel} \\ 
8510  30 
\isarcmd{theory} & : & \isartrans{toplevel}{theory} \\ 
31 
\isarcmd{context}^* & : & \isartrans{toplevel}{theory} \\ 

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

7134  33 
\end{matharray} 
34 

35 
Isabelle/Isar ``newstyle'' theories are either defined via theory files or 

7981  36 
interactively. Both theorylevel specifications and proofs are handled 
7335  37 
uniformly  occasionally definitional mechanisms even require some explicit 
38 
proof as well. In contrast, ``oldstyle'' Isabelle theories support batch 

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

7134  40 

7895  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 pretheory markup 

45 
command (cf.\ \S\ref{sec:markupthy} and \S\ref{sec:markupthy}). 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 

8547  48 
last command of any theory file. 
7134  49 

50 
\begin{rail} 

7895  51 
'header' text 
52 
; 

7134  53 
'theory' name '=' (name + '+') filespecs? ':' 
54 
; 

55 
'context' name 

56 
; 

57 
'end' 

58 
;; 

59 

7167  60 
filespecs: 'files' ((name  parname) +); 
7134  61 
\end{rail} 
62 

7167  63 
\begin{descr} 
7895  64 
\item [$\isarkeyword{header}~text$] provides plain text markup just preceding 
8547  65 
the formal beginning of a theory. In actual document preparation the 
7895  66 
corresponding {\LaTeX} macro \verb,\isamarkupheader, may be redefined to 
67 
produce chapter or section headings. See also \S\ref{sec:markupthy} and 

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

69 

7981  70 
\item [$\THEORY~A = B@1 + \cdots + B@n\colon$] commences a new theory $A$ 
71 
based on existing ones $B@1 + \cdots + B@n$. Isabelle's theory loader 

72 
system ensures that any of the base theories are properly loaded (and fully 

73 
uptodate when $\THEORY$ is executed interactively). The optional 

74 
$\isarkeyword{files}$ specification declares additional dependencies on ML 

75 
files. Unless put in parentheses, any file will be loaded immediately via 

76 
$\isarcmd{use}$ (see also \S\ref{sec:ML}). The optional ML file 

77 
\texttt{$A$.ML} that may be associated with any theory should \emph{not} be 

78 
included in $\isarkeyword{files}$, though. 

7134  79 

7895  80 
\item [$\CONTEXT~B$] enters an existing theory context, basically in readonly 
7981  81 
mode, so only a limited set of commands may be performed without destroying 
82 
the theory. Just as for $\THEORY$, the theory loader ensures that $B$ is 

83 
loaded and uptodate. 

7175  84 

7167  85 
\item [$\END$] concludes the current theory definition or context switch. 
7981  86 
Note that this command cannot be undone, but the whole theory definition has 
87 
to be retracted. 

7167  88 
\end{descr} 
7134  89 

90 

7895  91 
\subsection{Theory markup commands}\label{sec:markupthy} 
7134  92 

7895  93 
\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection} 
94 
\indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{textraw} 

7134  95 
\begin{matharray}{rcl} 
96 
\isarcmd{chapter} & : & \isartrans{theory}{theory} \\ 

7167  97 
\isarcmd{section} & : & \isartrans{theory}{theory} \\ 
7134  98 
\isarcmd{subsection} & : & \isartrans{theory}{theory} \\ 
99 
\isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\ 

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

7895  101 
\isarcmd{text_raw} & : & \isartrans{theory}{theory} \\ 
7134  102 
\end{matharray} 
103 

7895  104 
Apart from formal comments (see \S\ref{sec:comments}), markup commands provide 
7981  105 
a structured way to insert text into the document generated from a theory (see 
7895  106 
\cite{isabellesys} for more information on Isabelle's document preparation 
107 
tools). 

7134  108 

7895  109 
\railalias{textraw}{text\_raw} 
110 
\railterm{textraw} 

7134  111 

112 
\begin{rail} 

7895  113 
('chapter'  'section'  'subsection'  'subsubsection'  'text'  textraw) text 
7134  114 
; 
115 
\end{rail} 

116 

7167  117 
\begin{descr} 
7335  118 
\item [$\isarkeyword{chapter}$, $\isarkeyword{section}$, 
119 
$\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter 

120 
and section headings. 

7895  121 
\item [$\TEXT$] specifies paragraphs of plain text, including references to 
122 
formal entities.\footnote{The latter feature is not yet supported. 

123 
Nevertheless, any source text of the form 

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

125 
for future use.} 

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

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

128 
becomes available. A typical application would be to emit 

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

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

8547  131 
package to be included in {\LaTeX}, of course.} 
7167  132 
\end{descr} 
7134  133 

8684  134 
Any of these markup elements corresponds to a {\LaTeX} command with the name 
135 
prefixed by \verb,\isamarkup,. For the sectioning commands this is a plain 

136 
macro with a single argument, e.g.\ \verb,\isamarkupchapter{,\dots\verb,}, for 

137 
$\isarkeyword{chapter}$. The $\isarkeyword{text}$ markup results in a 

138 
{\LaTeX} environment \verb,\begin{isamarkuptext}, {\dots} 

139 
\verb,\end{isamarkuptext},, while $\isarkeyword{text_raw}$ causes the text 

140 
to be inserted directly into the {\LaTeX} source. 

7895  141 

8485  142 
\medskip 
143 

144 
Additional markup commands are available for proofs (see 

7895  145 
\S\ref{sec:markupprf}). Also note that the $\isarkeyword{header}$ 
8684  146 
declaration (see \S\ref{sec:beginthy}) admits to insert section markup just 
147 
preceding the actual theory definition. 

7895  148 

7134  149 

7135  150 
\subsection{Type classes and sorts}\label{sec:classes} 
7134  151 

152 
\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort} 

153 
\begin{matharray}{rcl} 

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

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

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

157 
\end{matharray} 

158 

159 
\begin{rail} 

7167  160 
'classes' (classdecl comment? +) 
7134  161 
; 
162 
'classrel' nameref '<' nameref comment? 

163 
; 

164 
'defaultsort' sort comment? 

165 
; 

166 
\end{rail} 

167 

7167  168 
\begin{descr} 
7335  169 
\item [$\isarkeyword{classes}~c<\vec c$] declares class $c$ to be a subclass 
170 
of existing classes $\vec c$. Cyclic class structures are ruled out. 

7134  171 
\item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between 
172 
existing classes $c@1$ and $c@2$. This is done axiomatically! The 

7895  173 
$\isarkeyword{instance}$ command (see \S\ref{sec:axclass}) provides a way to 
7175  174 
introduce proven class relations. 
7134  175 
\item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for 
7895  176 
any type variables given without sort constraints. Usually, the default 
8547  177 
sort would be only changed when defining new objectlogics. 
7167  178 
\end{descr} 
7134  179 

180 

7315  181 
\subsection{Primitive types and type abbreviations}\label{sec:typespure} 
7134  182 

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

184 
\begin{matharray}{rcl} 

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

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

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

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

189 
\end{matharray} 

190 

191 
\begin{rail} 

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

193 
; 

194 
'typedecl' typespec infix? comment? 

195 
; 

196 
'nonterminals' (name +) comment? 

197 
; 

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

199 
; 

200 
\end{rail} 

201 

7167  202 
\begin{descr} 
7335  203 
\item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym} 
7134  204 
$(\vec\alpha)t$ for existing type $\tau$. Unlike actual type definitions, 
205 
as are available in Isabelle/HOL for example, type synonyms are just purely 

7895  206 
syntactic abbreviations without any logical significance. Internally, type 
7981  207 
synonyms are fully expanded. 
7134  208 
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor 
7895  209 
$t$, intended as an actual logical type. Note that objectlogics such as 
210 
Isabelle/HOL override $\isarkeyword{typedecl}$ by their own version. 

7175  211 
\item [$\isarkeyword{nonterminals}~\vec c$] declares $0$ary type constructors 
212 
$\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of 

213 
Isabelle's inner syntax of terms or types. 

7335  214 
\item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's ordersorted 
215 
signature of types by new type constructor arities. This is done 

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

7895  217 
\S\ref{sec:axclass}) provides a way to introduce proven type arities. 
7167  218 
\end{descr} 
7134  219 

220 

7981  221 
\subsection{Constants and simple definitions}\label{sec:consts} 
7134  222 

7175  223 
\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl} 
7134  224 
\begin{matharray}{rcl} 
225 
\isarcmd{consts} & : & \isartrans{theory}{theory} \\ 

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

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

228 
\end{matharray} 

229 

230 
\begin{rail} 

231 
'consts' (constdecl +) 

232 
; 

7608  233 
'defs' (axmdecl prop comment? +) 
7134  234 
; 
235 
'constdefs' (constdecl prop comment? +) 

236 
; 

237 

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

239 
; 

240 
\end{rail} 

241 

7167  242 
\begin{descr} 
7335  243 
\item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type 
244 
scheme $\sigma$. The optional mixfix annotations may attach concrete syntax 

7895  245 
to the constants declared. 
7335  246 
\item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for some 
247 
existing constant. See \cite[\S6]{isabelleref} for more details on the 

248 
form of equations admitted as constant definitions. 

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

8547  250 
definitions of constants, using the canonical name $c_def$ for the 
251 
definitional axiom. 

7167  252 
\end{descr} 
7134  253 

254 

7981  255 
\subsection{Syntax and translations}\label{sec:syntrans} 
7134  256 

257 
\indexisarcmd{syntax}\indexisarcmd{translations} 

258 
\begin{matharray}{rcl} 

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

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

261 
\end{matharray} 

262 

263 
\begin{rail} 

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

265 
; 

266 
'translations' (transpat ('=='  '=>'  '<=') transpat comment? +) 

267 
; 

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

269 
; 

270 
\end{rail} 

271 

7167  272 
\begin{descr} 
7175  273 
\item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$, 
274 
except that the actual logical signature extension is omitted. Thus the 

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

7335  276 
arbitrary ways, independently of the logic. The $mode$ argument refers to 
8547  277 
the print mode that the grammar rules belong; unless the \texttt{output} 
278 
flag is given, all productions are added both to the input and output 

279 
grammar. 

7175  280 
\item [$\isarkeyword{translations}~rules$] specifies syntactic translation 
7981  281 
rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==}), parse rules 
7895  282 
(\texttt{=>}), or print rules (\texttt{<=}). Translation patterns may be 
283 
prefixed by the syntactic category to be used for parsing; the default is 

7134  284 
\texttt{logic}. 
7167  285 
\end{descr} 
7134  286 

287 

288 
\subsection{Axioms and theorems} 

289 

290 
\indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas} 

291 
\begin{matharray}{rcl} 

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

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

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

295 
\end{matharray} 

296 

297 
\begin{rail} 

7135  298 
'axioms' (axmdecl prop comment? +) 
7134  299 
; 
9199  300 
('theorems'  'lemmas') (thmdef? thmrefs comment? + 'and') 
7134  301 
; 
302 
\end{rail} 

303 

7167  304 
\begin{descr} 
7335  305 
\item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as 
7895  306 
axioms of the metalogic. In fact, axioms are ``axiomatic theorems'', and 
307 
may be referred later just as any other theorem. 

7134  308 

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

7175  310 
Everyday work is typically done the hard way, with proper definitions and 
8547  311 
actual proven theorems. 
7335  312 
\item [$\isarkeyword{theorems}~a = \vec b$] stores lists of existing theorems. 
8547  313 
Typical applications would also involve attributes, to declare Simplifier 
314 
rules, for example. 

7134  315 
\item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but 
316 
tags the results as ``lemma''. 

7167  317 
\end{descr} 
7134  318 

319 

7167  320 
\subsection{Name spaces} 
7134  321 

8726  322 
\indexisarcmd{global}\indexisarcmd{local}\indexisarcmd{hide} 
7134  323 
\begin{matharray}{rcl} 
324 
\isarcmd{global} & : & \isartrans{theory}{theory} \\ 

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

8726  326 
\isarcmd{hide} & : & \isartrans{theory}{theory} \\ 
7134  327 
\end{matharray} 
328 

8726  329 
\begin{rail} 
330 
'global' comment? 

331 
; 

332 
'local' comment? 

333 
; 

334 
'hide' name (nameref + ) comment? 

335 
; 

336 
\end{rail} 

337 

7895  338 
Isabelle organizes any kind of name declarations (of types, constants, 
8547  339 
theorems etc.) by separate hierarchically structured name spaces. Normally 
8726  340 
the user does not have to control the behavior of name spaces by hand, yet the 
341 
following commands provide some way to do so. 

7175  342 

7167  343 
\begin{descr} 
344 
\item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current 

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

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

7895  347 
Changing this to $\isarkeyword{global}$ causes all names to be declared 
348 
without the theory prefix, until $\isarkeyword{local}$ is declared again. 

8726  349 

350 
Note that global names are prone to get hidden accidently later, when 

351 
qualified names of the same base name are introduced. 

352 

353 
\item [$\isarkeyword{hide}~space~names$] removes declarations from a given 

354 
name space (which may be $class$, $type$, or $const$). Hidden objects 

355 
remain valid within the logic, but are inaccessible from user input. In 

356 
output, the special qualifier ``$\mathord?\mathord?$'' is prefixed to the 

357 
full internal name. 

358 

359 
Unqualified (global) names may not be hidden deliberately. 

7167  360 
\end{descr} 
7134  361 

362 

7167  363 
\subsection{Incorporating ML code}\label{sec:ML} 
7134  364 

8682  365 
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{MLcommand} 
366 
\indexisarcmd{MLsetup}\indexisarcmd{setup} 

9199  367 
\indexisarcmd{methodsetup} 
7134  368 
\begin{matharray}{rcl} 
369 
\isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\ 

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

8682  371 
\isarcmd{ML_command} & : & \isartrans{\cdot}{\cdot} \\ 
7895  372 
\isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\ 
7175  373 
\isarcmd{setup} & : & \isartrans{theory}{theory} \\ 
9199  374 
\isarcmd{method_setup} & : & \isartrans{theory}{theory} \\ 
7134  375 
\end{matharray} 
376 

7895  377 
\railalias{MLsetup}{ML\_setup} 
378 
\railterm{MLsetup} 

379 

9199  380 
\railalias{methodsetup}{method\_setup} 
381 
\railterm{methodsetup} 

382 

8682  383 
\railalias{MLcommand}{ML\_command} 
384 
\railterm{MLcommand} 

385 

7134  386 
\begin{rail} 
9273  387 
'use' name comment? 
7134  388 
; 
9273  389 
('ML'  MLcommand  MLsetup  'setup') text comment? 
7134  390 
; 
9199  391 
methodsetup name '=' text text comment? 
392 
; 

7134  393 
\end{rail} 
394 

7167  395 
\begin{descr} 
7175  396 
\item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$. 
7466  397 
The current theory context (if present) is passed down to the ML session, 
7981  398 
but may not be modified. Furthermore, the file name is checked with the 
7466  399 
$\isarkeyword{files}$ dependency declaration given in the theory header (see 
400 
also \S\ref{sec:beginthy}). 

401 

8682  402 
\item [$\isarkeyword{ML}~text$ and $\isarkeyword{ML_command}~text$] execute ML 
403 
commands from $text$. The theory context is passed in the same way as for 

404 
$\isarkeyword{use}$, but may not be changed. Note that 

405 
$\isarkeyword{ML_command}$ is less verbose than plain $\isarkeyword{ML}$. 

7895  406 

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

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

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

410 

7167  411 
\item [$\isarkeyword{setup}~text$] changes the current theory context by 
8379  412 
applying $text$, which refers to an ML expression of type 
413 
\texttt{(theory~>~theory)~list}. The $\isarkeyword{setup}$ command is the 

8547  414 
canonical way to initialize any objectlogic specific tools and packages 
415 
written in ML. 

9199  416 

417 
\item [$\isarkeyword{method_setup}~name = text~description$] defines a proof 

418 
method in the current theory. The given $text$ has to be an ML expression 

419 
of type \texttt{Args.src > Proof.context > Proof.method}. Parsing 

420 
concrete method syntax from \texttt{Args.src} input can be quite tedious in 

421 
general. The following simple examples are for methods without any explicit 

422 
arguments, or a list of theorems, respectively. 

423 

424 
{\footnotesize 

425 
\begin{verbatim} 

426 
Method.no_args (Method.METHOD (fn facts => foobar_tac)) 

427 
Method.thms_args (fn thms => (Method.METHOD (fn facts => foobar_tac))) 

428 
\end{verbatim} 

429 
} 

430 

431 
Note that mere tactic emulations may ignore the \texttt{facts} parameter 

432 
above. Proper proof methods would do something ``appropriate'' with the list 

433 
of current facts, though. Singlerule methods usually do strict 

434 
forwardchaining (e.g.\ by using \texttt{Method.multi_resolves}), while 

435 
automatic ones just insert the facts using \texttt{Method.insert_tac} before 

436 
applying the main tactic. 

7167  437 
\end{descr} 
7134  438 

439 

8250  440 
\subsection{Syntax translation functions} 
7134  441 

8250  442 
\indexisarcmd{parseasttranslation}\indexisarcmd{parsetranslation} 
443 
\indexisarcmd{printtranslation}\indexisarcmd{typedprinttranslation} 

444 
\indexisarcmd{printasttranslation}\indexisarcmd{tokentranslation} 

445 
\begin{matharray}{rcl} 

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

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

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

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

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

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

452 
\end{matharray} 

7134  453 

9273  454 
\railalias{parseasttranslation}{parse\_ast\_translation} 
455 
\railterm{parseasttranslation} 

456 

457 
\railalias{parsetranslation}{parse\_translation} 

458 
\railterm{parsetranslation} 

459 

460 
\railalias{printtranslation}{print\_translation} 

461 
\railterm{printtranslation} 

462 

463 
\railalias{typedprinttranslation}{typed\_print\_translation} 

464 
\railterm{typedprinttranslation} 

465 

466 
\railalias{printasttranslation}{print\_ast\_translation} 

467 
\railterm{printasttranslation} 

468 

469 
\railalias{tokentranslation}{token\_translation} 

470 
\railterm{tokentranslation} 

471 

472 
\begin{rail} 

473 
( parseasttranslation  parsetranslation  printtranslation  typedprinttranslation  

474 
printasttranslation  tokentranslation ) text comment? 

475 
\end{rail} 

476 

8250  477 
Syntax translation functions written in ML admit almost arbitrary 
478 
manipulations of Isabelle's inner syntax. Any of the above commands have a 

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

8379  480 
appropriate type. 
481 

482 
\begin{ttbox} 

483 
val parse_ast_translation : (string * (ast list > ast)) list 

484 
val parse_translation : (string * (term list > term)) list 

485 
val print_translation : (string * (term list > term)) list 

486 
val typed_print_translation : 

487 
(string * (bool > typ > term list > term)) list 

488 
val print_ast_translation : (string * (ast list > ast)) list 

489 
val token_translation : 

490 
(string * string * (string > string * real)) list 

491 
\end{ttbox} 

492 
See \cite[\S8]{isabelleref} for more information on syntax transformations. 

7134  493 

494 

495 
\subsection{Oracles} 

496 

497 
\indexisarcmd{oracle} 

498 
\begin{matharray}{rcl} 

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

500 
\end{matharray} 

501 

7175  502 
Oracles provide an interface to external reasoning systems, without giving up 
503 
control completely  each theorem carries a derivation object recording any 

504 
oracle invocation. See \cite[\S6]{isabelleref} for more information. 

505 

7134  506 
\begin{rail} 
507 
'oracle' name '=' text comment? 

508 
; 

509 
\end{rail} 

510 

7167  511 
\begin{descr} 
7175  512 
\item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML 
8379  513 
function $text$, which has to be of type 
514 
\texttt{Sign.sg~*~Object.T~>~term}. 

7167  515 
\end{descr} 
7134  516 

517 

518 
\section{Proof commands} 

519 

7987  520 
Proof commands perform transitions of Isar/VM machine configurations, which 
7315  521 
are blockstructured, consisting of a stack of nodes with three main 
7335  522 
components: logical proof context, current facts, and open goals. Isar/VM 
8547  523 
transitions are \emph{typed} according to the following three different modes 
524 
of operation: 

7167  525 
\begin{descr} 
526 
\item [$proof(prove)$] means that a new goal has just been stated that is now 

8547  527 
to be \emph{proven}; the next command may refine it by some proof method, 
528 
and enter a subproof to establish the actual result. 

7167  529 
\item [$proof(state)$] is like an internal theory mode: the context may be 
7987  530 
augmented by \emph{stating} additional assumptions, intermediate results 
531 
etc. 

7895  532 
\item [$proof(chain)$] is intermediate between $proof(state)$ and 
7987  533 
$proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$'' 
534 
register) have been just picked up in order to be used when refining the 

535 
goal claimed next. 

7167  536 
\end{descr} 
7134  537 

7167  538 

7895  539 
\subsection{Proof markup commands}\label{sec:markupprf} 
7167  540 

7987  541 
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect} 
7895  542 
\indexisarcmd{txt}\indexisarcmd{txtraw} 
7134  543 
\begin{matharray}{rcl} 
8101  544 
\isarcmd{sect} & : & \isartrans{proof}{proof} \\ 
545 
\isarcmd{subsect} & : & \isartrans{proof}{proof} \\ 

546 
\isarcmd{subsubsect} & : & \isartrans{proof}{proof} \\ 

547 
\isarcmd{txt} & : & \isartrans{proof}{proof} \\ 

548 
\isarcmd{txt_raw} & : & \isartrans{proof}{proof} \\ 

7134  549 
\end{matharray} 
550 

7895  551 
These markup commands for proof mode closely correspond to the ones of theory 
8684  552 
mode (see \S\ref{sec:markupthy}). 
7895  553 

554 
\railalias{txtraw}{txt\_raw} 

555 
\railterm{txtraw} 

7175  556 

7134  557 
\begin{rail} 
7895  558 
('sect'  'subsect'  'subsubsect'  'txt'  txtraw) text 
7134  559 
; 
560 
\end{rail} 

561 

562 

7315  563 
\subsection{Proof context}\label{sec:proofcontext} 
7134  564 

7315  565 
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def} 
7134  566 
\begin{matharray}{rcl} 
567 
\isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\ 

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

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

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

571 
\end{matharray} 

572 

7315  573 
The logical proof context consists of fixed variables and assumptions. The 
574 
former closely correspond to Skolem constants, or metalevel universal 

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

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

7987  577 
a local value that may be used in the subsequent proof as any other variable 
7895  578 
or constant. Furthermore, any result $\edrv \phi[x]$ exported from the 
7987  579 
context will be universally closed wrt.\ $x$ at the outermost level: $\edrv 
580 
\All x \phi$ (this is expressed using Isabelle's metavariables). 

7315  581 

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

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

7895  584 
proof steps. On the other hand, any result $\chi \drv \phi$ exported from the 
585 
context becomes conditional wrt.\ the assumption: $\edrv \chi \Imp \phi$. 

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

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

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

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

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

591 
user. 

7315  592 

7319  593 
Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by 
7987  594 
combining $\FIX x$ with another version of assumption that causes any 
595 
hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule. 

596 
Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$. 

7175  597 

7134  598 
\begin{rail} 
7431  599 
'fix' (vars + 'and') comment? 
7134  600 
; 
7315  601 
('assume'  'presume') (assm comment? + 'and') 
7134  602 
; 
7175  603 
'def' thmdecl? \\ var '==' term termpat? comment? 
7134  604 
; 
605 

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

607 
; 

7458  608 
vars: (name+) ('::' type)? 
7431  609 
; 
7315  610 
assm: thmdecl? (prop proppat? +) 
611 
; 

7134  612 
\end{rail} 
613 

7167  614 
\begin{descr} 
8547  615 
\item [$\FIX{\vec x}$] introduces local \emph{arbitrary, but fixed} variables 
616 
$\vec x$. 

8515  617 
\item [$\ASSUME{a}{\vec\phi}$ and $\PRESUME{a}{\vec\phi}$] introduce local 
618 
theorems $\vec\phi$ by assumption. Subsequent results applied to an 

619 
enclosing goal (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ 

620 
expects to be able to unify with existing premises in the goal, while 

621 
$\PRESUMENAME$ leaves $\vec\phi$ as new subgoals. 

7335  622 

623 
Several lists of assumptions may be given (separated by 

7895  624 
$\isarkeyword{and}$); the resulting list of current facts consists of all of 
625 
these concatenated. 

7315  626 
\item [$\DEF{a}{x \equiv t}$] introduces a local (nonpolymorphic) definition. 
627 
In results exported from the context, $x$ is replaced by $t$. Basically, 

7987  628 
$\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\ASSUME{}{x \equiv t}$, with the 
7335  629 
resulting hypothetical equation solved by reflexivity. 
7431  630 

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

7167  632 
\end{descr} 
633 

7895  634 
The special name $prems$\indexisarthm{prems} refers to all assumptions of the 
635 
current context as a list of theorems. 

7315  636 

7167  637 

638 
\subsection{Facts and forward chaining} 

639 

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

641 
\begin{matharray}{rcl} 

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

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

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

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

646 
\end{matharray} 

647 

7319  648 
New facts are established either by assumption or proof of local statements. 
7335  649 
Any fact will usually be involved in further proofs, either as explicit 
8547  650 
arguments of proof methods, or when forward chaining towards the next goal via 
7335  651 
$\THEN$ (and variants). Note that the special theorem name 
7987  652 
$this$\indexisarthm{this} refers to the most recently established facts. 
7167  653 
\begin{rail} 
9199  654 
'note' (thmdef? thmrefs comment? + 'and') 
7167  655 
; 
656 
'then' comment? 

657 
; 

9199  658 
('from'  'with') (thmrefs comment? + 'and') 
7167  659 
; 
660 
\end{rail} 

661 

662 
\begin{descr} 

7175  663 
\item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result 
664 
as $a$. Note that attributes may be involved as well, both on the left and 

665 
right hand sides. 

7167  666 
\item [$\THEN$] indicates forward chaining by the current facts in order to 
7895  667 
establish the goal to be claimed next. The initial proof method invoked to 
668 
refine that will be offered the facts to do ``anything appropriate'' (cf.\ 

669 
also \S\ref{sec:proofsteps}). For example, method $rule$ (see 

8515  670 
\S\ref{sec:puremethatt}) would typically do an elimination rather than an 
7895  671 
introduction. Automatic methods usually insert the facts into the goal 
8547  672 
state before operation. This provides a simple scheme to control relevance 
673 
of facts in automated proof search. 

7335  674 
\item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is 
7458  675 
equivalent to $\FROM{this}$. 
7175  676 
\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward 
677 
chaining is from earlier facts together with the current ones. 

7167  678 
\end{descr} 
679 

8515  680 
Basic proof methods (such as $rule$, see \S\ref{sec:puremethatt}) expect 
7895  681 
multiple facts to be given in their proper order, corresponding to a prefix of 
682 
the premises of the rule involved. Note that positions may be easily skipped 

8547  683 
using something like $\FROM{\text{\texttt{_}}~a~b}$, for example. This 
684 
involves the trivial rule $\PROP\psi \Imp \PROP\psi$, which happens to be 

685 
bound in Isabelle/Pure as ``\texttt{_}'' 

686 
(underscore).\indexisarthm{_@\texttt{_}} 

7389  687 

9238  688 
Forward chaining with an empty list of theorems is the same as not chaining. 
689 
Thus $\FROM{nothing}$ has no effect apart from entering $prove(chain)$ mode, 

690 
since $nothing$\indexisarthm{nothing} is bound to the empty list of facts. 

691 

7167  692 

693 
\subsection{Goal statements} 

694 

695 
\indexisarcmd{theorem}\indexisarcmd{lemma} 

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

697 
\begin{matharray}{rcl} 

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

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

7987  700 
\isarcmd{have} & : & \isartrans{proof(state) ~~ proof(chain)}{proof(prove)} \\ 
701 
\isarcmd{show} & : & \isartrans{proof(state) ~~ proof(chain)}{proof(prove)} \\ 

7167  702 
\isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\ 
703 
\isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\ 

704 
\end{matharray} 

705 

7175  706 
Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$ 
7895  707 
and $\LEMMANAME$. New local goals may be claimed within proof mode as well. 
708 
Four variants are available, indicating whether the result is meant to solve 

8547  709 
some pending goal or whether forward chaining is indicated. 
7175  710 

7167  711 
\begin{rail} 
712 
('theorem'  'lemma') goal 

713 
; 

714 
('have'  'show'  'hence'  'thus') goal 

715 
; 

716 

8632  717 
goal: thmdecl? prop proppat? comment? 
7167  718 
; 
719 
\end{rail} 

720 

721 
\begin{descr} 

7335  722 
\item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal, 
8547  723 
eventually resulting in some theorem $\turn \phi$ to be put back into the 
724 
theory. 

7987  725 
\item [$\LEMMA{a}{\phi}$] is similar to $\THEOREMNAME$, but tags the result as 
7167  726 
``lemma''. 
7335  727 
\item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a 
7167  728 
theorem with the current assumption context as hypotheses. 
7335  729 
\item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some 
7895  730 
pending goal with the result \emph{exported} into the corresponding context 
731 
(cf.\ \S\ref{sec:proofcontext}). 

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

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

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

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

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

7167  737 
\end{descr} 
738 

8991  739 
Note that any goal statement causes some term abbreviations (such as 
740 
$\Var{thesis}$, $\dots$) to be bound automatically, see also 

741 
\S\ref{sec:termabbrev}. Furthermore, the local context of a (nonatomic) 

742 
goal is provided via the case name $antecedent$\indexisarcase{antecedent}, see 

743 
also \S\ref{sec:cases}. 

744 

7167  745 

746 
\subsection{Initial and terminal proof steps}\label{sec:proofsteps} 

747 

7175  748 
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by} 
749 
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry} 

750 
\begin{matharray}{rcl} 

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

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

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

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

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

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

757 
\end{matharray} 

758 

8547  759 
Arbitrary goal refinement via tactics is considered harmful. Properly, the 
7335  760 
Isar framework admits proof methods to be invoked in two places only. 
7167  761 
\begin{enumerate} 
7175  762 
\item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated 
7335  763 
goal to a number of subgoals that are to be solved later. Facts are passed 
7895  764 
to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode. 
7167  765 

7987  766 
\item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve 
767 
remaining goals. No facts are passed to $m@2$. 

7167  768 
\end{enumerate} 
769 

8547  770 
The only other proper way to affect pending goals is by $\SHOWNAME$, which 
771 
involves an explicit statement of what is to be solved. 

7167  772 

7175  773 
\medskip 
774 

7167  775 
Also note that initial proof methods should either solve the goal completely, 
7895  776 
or constitute some wellunderstood reduction to new subgoals. Arbitrary 
777 
automatic proof tools that are prone leave a large number of badly structured 

778 
subgoals are no help in continuing the proof document in any intelligible 

7987  779 
way. 
7167  780 

7175  781 
\medskip 
782 

8547  783 
Unless given explicitly by the user, the default initial method is ``$rule$'', 
784 
which applies a single standard elimination or introduction rule according to 

785 
the topmost symbol involved. There is no separate default terminal method. 

786 
Any remaining goals are always solved by assumption in the very last step. 

7167  787 

788 
\begin{rail} 

789 
'proof' interest? meth? comment? 

790 
; 

791 
'qed' meth? comment? 

792 
; 

793 
'by' meth meth? comment? 

794 
; 

795 
('.'  '..'  'sorry') comment? 

796 
; 

797 

798 
meth: method interest? 

799 
; 

800 
\end{rail} 

801 

802 
\begin{descr} 

7335  803 
\item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for 
804 
forward chaining are passed if so indicated by $proof(chain)$ mode. 

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

7895  806 
concludes the subproof by assumption. If the goal had been $\SHOWNAME$ (or 
807 
$\THUSNAME$), some pending subgoal is solved as well by the rule resulting 

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

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

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

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

812 
context. Debugging such a situation might involve temporarily changing 

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

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

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

7987  816 
abbreviates $\PROOF{m@1}~\QED{m@2}$, with backtracking across both methods, 
817 
though. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done 

7895  818 
by expanding its definition; in many cases $\PROOF{m@1}$ is already 
7175  819 
sufficient to see what is going wrong. 
7895  820 
\item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it 
8515  821 
abbreviates $\BY{rule}$. 
7895  822 
\item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it 
8195  823 
abbreviates $\BY{this}$. 
8379  824 
\item [$\SORRY$] is a \emph{fake proof}\index{proof!fake}; provided that the 
825 
\texttt{quick_and_dirty} flag is enabled, $\SORRY$ pretends to solve the 

8515  826 
goal without further ado. Of course, the result would be a fake theorem 
827 
only, involving some oracle in its internal derivation object (this is 

828 
indicated as ``$[!]$'' in the printed result). The main application of 

829 
$\SORRY$ is to support experimentation and topdown proof development. 

830 
\end{descr} 

831 

832 

833 
\subsection{Fundamental methods and attributes}\label{sec:puremethatt} 

834 

8547  835 
The following proof methods and attributes refer to basic logical operations 
836 
of Isar. Further methods and attributes are provided by several generic and 

837 
objectlogic specific tools and packages (see chapters \ref{ch:gentools} and 

838 
\ref{ch:holtools}). 

8515  839 

840 
\indexisarmeth{assumption}\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{$$} 

841 
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} 

842 
\indexisaratt{OF}\indexisaratt{of} 

843 
\begin{matharray}{rcl} 

844 
assumption & : & \isarmeth \\ 

845 
this & : & \isarmeth \\ 

846 
rule & : & \isarmeth \\ 

847 
 & : & \isarmeth \\ 

848 
OF & : & \isaratt \\ 

849 
of & : & \isaratt \\ 

850 
intro & : & \isaratt \\ 

851 
elim & : & \isaratt \\ 

852 
dest & : & \isaratt \\ 

853 
delrule & : & \isaratt \\ 

854 
\end{matharray} 

855 

856 
\begin{rail} 

8547  857 
'rule' thmrefs? 
8515  858 
; 
859 
'OF' thmrefs 

860 
; 

8693  861 
'of' insts ('concl' ':' insts)? 
8515  862 
; 
863 
\end{rail} 

864 

865 
\begin{descr} 

866 
\item [$assumption$] solves some goal by a single assumption step. Any facts 

867 
given (${} \le 1$) are guaranteed to participate in the refinement. Recall 

868 
that $\QEDNAME$ (see \S\ref{sec:proofsteps}) already concludes any 

869 
remaining subgoals by assumption. 

870 
\item [$this$] applies all of the current facts directly as rules. Recall 

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

8547  872 
\item [$rule~\vec a$] applies some rule given as argument in backward manner; 
8515  873 
facts are used to reduce the rule before applying it to the goal. Thus 
874 
$rule$ without facts is plain \emph{introduction}, while with facts it 

875 
becomes \emph{elimination}. 

876 

8547  877 
When no arguments are given, the $rule$ method tries to pick appropriate 
878 
rules automatically, as declared in the current context using the $intro$, 

879 
$elim$, $dest$ attributes (see below). This is the default behavior of 

880 
$\PROOFNAME$ and ``$\DDOT$'' (doubledot) steps (see 

8515  881 
\S\ref{sec:proofsteps}). 
882 
\item [``$$''] does nothing but insert the forward chaining facts as premises 

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

884 
performs a single reduction step using the $rule$ method; thus a plain 

885 
\emph{donothing} proof step would be $\PROOF{}$ rather than $\PROOFNAME$ 

886 
alone. 

8547  887 
\item [$OF~\vec a$] applies some theorem to given rules $\vec a$ (in 
888 
parallel). This corresponds to the \texttt{MRS} operator in ML 

889 
\cite[\S5]{isabelleref}, but note the reversed order. Positions may be 

890 
skipped by including ``$\_$'' (underscore) as argument. 

891 
\item [$of~\vec t$] performs positional instantiation. The terms $\vec t$ are 

8515  892 
substituted for any schematic variables occurring in a theorem from left to 
893 
right; ``\texttt{_}'' (underscore) indicates to skip a position. Arguments 

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

895 
conclusion of a rule. 

896 
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and 

897 
destruct rules, respectively. Note that the classical reasoner (see 

898 
\S\ref{sec:classicalbasic}) introduces different versions of these 

899 
attributes, and the $rule$ method, too. In objectlogics with classical 

900 
reasoning enabled, the latter version should be used all the time to avoid 

901 
confusion! 

902 
\item [$delrule$] undeclares introduction or elimination rules. 

7315  903 
\end{descr} 
904 

905 

906 
\subsection{Term abbreviations}\label{sec:termabbrev} 

907 

908 
\indexisarcmd{let} 

909 
\begin{matharray}{rcl} 

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

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

912 
\end{matharray} 

913 

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

7987  915 
or by annotating assumptions or goal statements with a list of patterns 
916 
$\ISS{p@1\;\dots}{p@n}$. In both cases, higherorder matching is invoked to 

917 
bind extralogical term variables, which may be either named schematic 

918 
variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}'' 

919 
(underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the 

920 
patterns occur on the lefthand side, while the $\ISNAME$ patterns are in 

921 
postfix position. 

7315  922 

8620
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

923 
Polymorphism of term bindings is handled in HindleyMilner style, as in ML. 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

924 
Type variables referring to local assumptions or open goal statements are 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

925 
\emph{fixed}, while those of finished results or bound by $\LETNAME$ may occur 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

926 
in \emph{arbitrary} instances later. Even though actual polymorphism should 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

927 
be rarely used in practice, this mechanism is essential to achieve proper 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

928 
incremental typeinference, as the user proceeds to build up the Isar proof 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

929 
text. 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

930 

3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

931 
\medskip 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

932 

7319  933 
Term abbreviations are quite different from actual local definitions as 
934 
introduced via $\DEFNAME$ (see \S\ref{sec:proofcontext}). The latter are 

7315  935 
visible within the logic as actual equations, while abbreviations disappear 
8620
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

936 
during the input process just after type checking. Also note that $\DEFNAME$ 
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

937 
does not support polymorphism. 
7315  938 

939 
\begin{rail} 

8664  940 
'let' ((term + 'and') '=' term comment? + 'and') 
7315  941 
; 
942 
\end{rail} 

943 

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

945 
\railnonterm{proppat} (see \S\ref{sec:termpats}). 

946 

947 
\begin{descr} 

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

949 
by simultaneous higherorder matching against terms $\vec t$. 

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

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

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

953 
\end{descr} 

954 

7988  955 
A few \emph{automatic} term abbreviations\index{term abbreviations} for goals 
956 
and facts are available as well. For any open goal, 

7466  957 
$\Var{thesis_prop}$\indexisarvar{thesisprop} refers to the full proposition 
958 
(which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesisconcl} to its 

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

8547  960 
objectlevel statement. The latter two abstract over any metalevel 
7987  961 
parameters. 
7315  962 

7466  963 
Fact statements resulting from assumptions or finished goals are bound as 
964 
$\Var{this_prop}$\indexisarvar{thisprop}, 

965 
$\Var{this_concl}$\indexisarvar{thisconcl}, and 

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

967 
$\Var{this}$ refers to an objectlogic statement that is an application 

7895  968 
$f(t)$, then $t$ is bound to the special text variable 
7466  969 
``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of 
7987  970 
the latter are calculational proofs (see \S\ref{sec:calculation}). 
7315  971 

972 

7134  973 
\subsection{Block structure} 
974 

8896  975 
\indexisarcmd{next}\indexisarcmd{\{}\indexisarcmd{\}} 
7397  976 
\begin{matharray}{rcl} 
8448  977 
\NEXT & : & \isartrans{proof(state)}{proof(state)} \\ 
7974  978 
\BG & : & \isartrans{proof(state)}{proof(state)} \\ 
979 
\EN & : & \isartrans{proof(state)}{proof(state)} \\ 

7397  980 
\end{matharray} 
981 

9030  982 
\railalias{lbrace}{\ttlbrace} 
983 
\railterm{lbrace} 

984 

985 
\railalias{rbrace}{\ttrbrace} 

986 
\railterm{rbrace} 

987 

988 
\begin{rail} 

989 
'next' comment? 

990 
; 

991 
lbrace comment? 

992 
; 

993 
rbrace comment? 

994 
; 

995 
\end{rail} 

996 

7167  997 
While Isar is inherently blockstructured, opening and closing blocks is 
998 
mostly handled rather casually, with little explicit userintervention. Any 

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

1000 
again when concluding the subproof (by $\QEDNAME$ etc.). Sections of 

8448  1001 
different context within a subproof may be switched via $\NEXT$, which is 
1002 
just a single blockclose followed by blockopen again. Thus the effect of 

1003 
$\NEXT$ to reset the local proof context. There is no goal focus involved 

1004 
here! 

7167  1005 

7175  1006 
For slightly more advanced applications, there are explicit block parentheses 
7895  1007 
as well. These typically achieve a stronger forward style of reasoning. 
7167  1008 

1009 
\begin{descr} 

8448  1010 
\item [$\NEXT$] switches to a fresh block within a subproof, resetting the 
1011 
local context to the initial one. 

8896  1012 
\item [$\BG$ and $\EN$] explicitly open and close blocks. Any current facts 
1013 
pass through ``$\BG$'' unchanged, while ``$\EN$'' causes any result to be 

7895  1014 
\emph{exported} into the enclosing context. Thus fixed variables are 
1015 
generalized, assumptions discharged, and local definitions unfolded (cf.\ 

1016 
\S\ref{sec:proofcontext}). There is no difference of $\ASSUMENAME$ and 

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

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

7167  1019 
\end{descr} 
7134  1020 

1021 

8533  1022 
\subsection{Emulating tactic scripts}\label{sec:tacticalproof} 
8515  1023 

1024 
The following elements emulate unstructured tactic scripts to some extent. 

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

1026 
come in handy for interactive exploration and debugging, or even actual 

1027 
tactical proof within newstyle theories (to benefit from document 

1028 
preparation, for example). 

1029 

8946  1030 
\indexisarcmd{apply}\indexisarcmd{done}\indexisarcmd{applyend} 
8515  1031 
\indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back} 
1032 
\begin{matharray}{rcl} 

8533  1033 
\isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\ 
8946  1034 
\isarcmd{done}^* & : & \isartrans{proof(prove)}{proof(state)} \\ 
8533  1035 
\isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\ 
1036 
\isarcmd{defer}^* & : & \isartrans{proof}{proof} \\ 

1037 
\isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\ 

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

8515  1039 
\end{matharray} 
1040 

1041 
\railalias{applyend}{apply\_end} 

1042 
\railterm{applyend} 

1043 

1044 
\begin{rail} 

8682  1045 
'apply' method comment? 
8515  1046 
; 
8946  1047 
'done' comment? 
1048 
; 

8682  1049 
applyend method comment? 
8515  1050 
; 
8682  1051 
'defer' nat? comment? 
8515  1052 
; 
8682  1053 
'prefer' nat comment? 
8515  1054 
; 
9273  1055 
'back' comment? 
1056 
; 

8515  1057 
\end{rail} 
1058 

1059 
\begin{descr} 

8547  1060 
\item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in initial 
1061 
position, but unlike $\PROOFNAME$ it retains ``$proof(prove)$'' mode. Thus 

8946  1062 
consecutive method applications may be given just as in tactic scripts. 
8515  1063 

8881  1064 
Facts are passed to $m$ as indicated by the goal's forwardchain mode, and 
1065 
are \emph{consumed} afterwards. Thus any further $\isarkeyword{apply}$ 

1066 
command would always work in a purely backward manner. 

8946  1067 

1068 
\item [$\isarkeyword{done}$] completes a proof script, provided that the 

8947  1069 
current goal state is already solved completely. Note that actual 
1070 
structured proof commands (e.g.\ ``$\DOT$'' or $\SORRY$) may be used to 

1071 
conclude proof scripts as well. 

8881  1072 

8515  1073 
\item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in 
1074 
terminal position. Basically, this simulates a multistep tactic script for 

1075 
$\QEDNAME$, but may be given anywhere within the proof body. 

1076 

1077 
No facts are passed to $m$. Furthermore, the static context is that of the 

1078 
enclosing goal (as for actual $\QEDNAME$). Thus the proof method may not 

1079 
refer to any assumptions introduced in the current body, for example. 

1080 
\item [$\isarkeyword{defer}~n$ and $\isarkeyword{prefer}~n$] shuffle the list 

1081 
of pending goals: $defer$ puts off goal $n$ to the end of the list ($n = 1$ 

1082 
by default), while $prefer$ brings goal $n$ to the top. 

1083 
\item [$\isarkeyword{back}$] does backtracking over the result sequence of 

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

1085 
\cite{isabelleref}, the Isar command does not search upwards for further 

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

9006  1087 
\end{descr} 
1088 

1089 
Any proper Isar proof method may be used with tactic script commands such as 

1090 
$\isarkeyword{apply}$. A few additional emulations of actual tactics are 

1091 
provided as well; these would be never used in actual structured proofs, of 

1092 
course. 

1093 

1094 
\indexisarmeth{tactic}\indexisarmeth{insert} 

1095 
\indexisarmeth{resinsttac}\indexisarmeth{eresinsttac} 

1096 
\indexisarmeth{dresinsttac}\indexisarmeth{forwinsttac} 

1097 
\indexisarmeth{subgoaltac} 

1098 
\begin{matharray}{rcl} 

1099 
tactic^* & : & \isarmeth \\ 

1100 
insert^* & : & \isarmeth \\ 

1101 
res_inst_tac^* & : & \isarmeth \\ 

1102 
eres_inst_tac^* & : & \isarmeth \\ 

1103 
dres_inst_tac^* & : & \isarmeth \\ 

1104 
forw_inst_tac^* & : & \isarmeth \\ 

1105 
subgoal_tac^* & : & \isarmeth \\ 

1106 
\end{matharray} 

1107 

1108 
\railalias{resinsttac}{res\_inst\_tac} 

1109 
\railterm{resinsttac} 

1110 

1111 
\railalias{eresinsttac}{eres\_inst\_tac} 

1112 
\railterm{eresinsttac} 

1113 

1114 
\railalias{dresinsttac}{dres\_inst\_tac} 

1115 
\railterm{dresinsttac} 

1116 

1117 
\railalias{forwinsttac}{forw\_inst\_tac} 

1118 
\railterm{forwinsttac} 

1119 

1120 
\railalias{subgoaltac}{subgoal\_tac} 

1121 
\railterm{subgoaltac} 

1122 

1123 
\begin{rail} 

1124 
'tactic' text 

1125 
; 

1126 
'insert' thmrefs 

1127 
; 

1128 
( resinsttac  eresinsttac  dresinsttac  forwinsttac ) goalspec? \\ 

1129 
((name '=' term) + 'and') 'in' thmref 

1130 
; 

1131 
subgoaltac goalspec? prop 

1132 
; 

1133 
\end{rail} 

1134 

1135 
\begin{descr} 

8515  1136 
\item [$tactic~text$] produces a proof method from any ML text of type 
8547  1137 
\texttt{tactic}. Apart from the usual ML environment and the current 
8515  1138 
implicit theory context, the ML code may refer to the following locally 
1139 
bound values: 

9006  1140 

8515  1141 
%%FIXME ttbox produces too much trailing space (why?) 
1142 
{\footnotesize\begin{verbatim} 

1143 
val ctxt : Proof.context 

1144 
val facts : thm list 

1145 
val thm : string > thm 

1146 
val thms : string > thm list 

1147 
\end{verbatim}} 

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

1149 
indicates any current facts for forwardchaining, and 

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

1151 
theorems) from the context. 

8696  1152 
\item [$insert~\vec a$] inserts theorems as facts into all goals of the proof 
1153 
state; the current facts indicated for forward chaining are ignored! 

8533  1154 
\item [$res_inst_tac$ etc.] do resolution of rules with explicit 
1155 
instantiation. This works the same way as the corresponding ML tactics, see 

1156 
\cite[\S3]{isabelleref}. 

1157 

1158 
It is very important to note that the instantiations are read and 

1159 
typechecked according to the dynamic goal state, rather than the static 

1160 
proof context! In particular, locally fixed variables and term 

1161 
abbreviations may not be included in the term specifications. 

8547  1162 
\item [$subgoal_tac~\phi$] emulates the ML tactic of the same name, see 
8533  1163 
\cite[\S3]{isabelleref}. Syntactically, the given proposition is handled 
1164 
as the instantiations in $res_inst_tac$ etc. 

1165 

1166 
Note that the proper Isar command $\PRESUMENAME$ achieves a similar effect 

1167 
as $subgoal_tac$. 

8515  1168 
\end{descr} 
1169 

1170 

1171 
\subsection{Metalinguistic features} 

1172 

1173 
\indexisarcmd{oops} 

1174 
\begin{matharray}{rcl} 

1175 
\isarcmd{oops} & : & \isartrans{proof}{theory} \\ 

1176 
\end{matharray} 

1177 

1178 
The $\OOPS$ command discontinues the current proof attempt, while considering 

1179 
the partial proof text as properly processed. This is conceptually quite 

1180 
different from ``faking'' actual proofs via $\SORRY$ (see 

1181 
\S\ref{sec:proofsteps}): $\OOPS$ does not observe the proof structure at all, 

1182 
but goes back right to the theory level. Furthermore, $\OOPS$ does not 

1183 
produce any result theorem  there is no claim to be able to complete the 

1184 
proof anyhow. 

1185 

1186 
A typical application of $\OOPS$ is to explain Isar proofs \emph{within} the 

1187 
system itself, in conjunction with the document preparation tools of Isabelle 

1188 
described in \cite{isabellesys}. Thus partial or even wrong proof attempts 

1189 
can be discussed in a logically sound manner. Note that the Isabelle {\LaTeX} 

1190 
macros can be easily adapted to print something like ``$\dots$'' instead of an 

1191 
``$\OOPS$'' keyword. 

1192 

8547  1193 
\medskip The $\OOPS$ command is undoable, unlike $\isarkeyword{kill}$ (see 
1194 
\S\ref{sec:history}). The effect is to get back to the theory \emph{before} 

1195 
the opening of the proof. 

8515  1196 

1197 

7134  1198 
\section{Other commands} 
1199 

8448  1200 
\subsection{Diagnostics}\label{sec:diag} 
7134  1201 

8485  1202 
\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ} 
1203 
\indexisarcmd{printfacts}\indexisarcmd{printbinds} 

7134  1204 
\begin{matharray}{rcl} 
8515  1205 
\isarcmd{pr}^* & : & \isarkeep{\cdot} \\ 
1206 
\isarcmd{thm}^* & : & \isarkeep{theory~~proof} \\ 

1207 
\isarcmd{term}^* & : & \isarkeep{theory~~proof} \\ 

1208 
\isarcmd{prop}^* & : & \isarkeep{theory~~proof} \\ 

1209 
\isarcmd{typ}^* & : & \isarkeep{theory~~proof} \\ 

1210 
\isarcmd{print_facts}^* & : & \isarkeep{proof} \\ 

1211 
\isarcmd{print_binds}^* & : & \isarkeep{proof} \\ 

7134  1212 
\end{matharray} 
1213 

7335  1214 
These commands are not part of the actual Isabelle/Isar syntax, but assist 
1215 
interactive development. Also note that $undo$ does not apply here, since the 

1216 
theory or proof configuration is not changed. 

1217 

7134  1218 
\begin{rail} 
8485  1219 
'pr' modes? nat? 
7134  1220 
; 
8485  1221 
'thm' modes? thmrefs 
1222 
; 

1223 
'term' modes? term 

7134  1224 
; 
8485  1225 
'prop' modes? prop 
7134  1226 
; 
8485  1227 
'typ' modes? type 
1228 
; 

1229 

1230 
modes: '(' (name + ) ')' 

7134  1231 
; 
1232 
\end{rail} 

1233 

7167  1234 
\begin{descr} 
8883  1235 
\item [$\isarkeyword{pr}~n$] prints the current proof state (if present), 
1236 
including the proof context, current facts and goals. The optional argument 

1237 
$n$ affects the implicit limit of goals to be displayed, which is initially 

1238 
10. Omitting the limit leaves the current value unchanged. 

8547  1239 
\item [$\isarkeyword{thm}~\vec a$] retrieves theorems from the current theory 
1240 
or proof context. Note that any attributes included in the theorem 

7974  1241 
specifications are applied to a temporary context derived from the current 
8547  1242 
theory or proof; the result is discarded, i.e.\ attributes involved in $\vec 
1243 
a$ do not have any permanent effect. 

7987  1244 
\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, typecheck and 
1245 
print terms or propositions according to the current theory or proof 

7895  1246 
context; the inferred type of $t$ is output as well. Note that these 
1247 
commands are also useful in inspecting the current environment of term 

1248 
abbreviations. 

7974  1249 
\item [$\isarkeyword{typ}~\tau$] reads and prints types of the metalogic 
1250 
according to the current theory or proof context. 

8379  1251 
\item [$\isarkeyword{print_facts}$] prints any named facts of the current 
1252 
context, including assumptions and local results. 

1253 
\item [$\isarkeyword{print_binds}$] prints all term abbreviations present in 

1254 
the context. 

8485  1255 
\end{descr} 
1256 

1257 
The basic diagnostic commands above admit a list of $modes$ to be specified, 

1258 
which is appended to the current print mode (see also \cite{isabelleref}). 

1259 
Thus the output behavior may be modified according particular print mode 

1260 
features. 

1261 

1262 
For example, $\isarkeyword{pr}~(latex~xsymbols~symbols)$ would print the 

1263 
current proof state with mathematical symbols and special characters 

1264 
represented in {\LaTeX} source, according to the Isabelle style 

8547  1265 
\cite{isabellesys}. The resulting text can be directly pasted into a 
1266 
\verb,\begin{isabelle},\dots\verb,\end{isabelle}, environment. Note that 

1267 
$\isarkeyword{pr}~(latex)$ is sufficient to achieve the same output, if the 

1268 
current Isabelle session has the other modes already activated, say due to 

1269 
some particular user interface configuration such as Proof~General 

8510  1270 
\cite{proofgeneral,Aspinall:TACAS:2000} with XSymbol mode \cite{xsymbol}. 
8485  1271 

1272 

1273 
\subsection{History commands}\label{sec:history} 

1274 

1275 
\indexisarcmd{undo}\indexisarcmd{redo}\indexisarcmd{kill} 

1276 
\begin{matharray}{rcl} 

1277 
\isarcmd{undo}^{{*}{*}} & : & \isarkeep{\cdot} \\ 

1278 
\isarcmd{redo}^{{*}{*}} & : & \isarkeep{\cdot} \\ 

1279 
\isarcmd{kill}^{{*}{*}} & : & \isarkeep{\cdot} \\ 

1280 
\end{matharray} 

1281 

1282 
The Isabelle/Isar toplevel maintains a twostage history, for theory and 

1283 
proof state transformation. Basically, any command can be undone using 

1284 
$\isarkeyword{undo}$, excluding mere diagnostic elements. Its effect may be 

1285 
revoked via $\isarkeyword{redo}$, unless the corresponding the 

1286 
$\isarkeyword{undo}$ step has crossed the beginning of a proof or theory. The 

1287 
$\isarkeyword{kill}$ command aborts the current history node altogether, 

1288 
discontinuing a proof or even the whole theory. This operation is \emph{not} 

1289 
undoable. 

1290 

1291 
\begin{warn} 

8547  1292 
History commands should never be used with user interfaces such as 
1293 
Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes care of 

1294 
stepping forth and back itself. Interfering by manual $\isarkeyword{undo}$, 

8510  1295 
$\isarkeyword{redo}$, or even $\isarkeyword{kill}$ commands would quickly 
1296 
result in utter confusion. 

8485  1297 
\end{warn} 
1298 

8379  1299 

7134  1300 
\subsection{System operations} 
1301 

7167  1302 
\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{usethy}\indexisarcmd{usethyonly} 
1303 
\indexisarcmd{updatethy}\indexisarcmd{updatethyonly} 

7134  1304 
\begin{matharray}{rcl} 
8515  1305 
\isarcmd{cd}^* & : & \isarkeep{\cdot} \\ 
1306 
\isarcmd{pwd}^* & : & \isarkeep{\cdot} \\ 

1307 
\isarcmd{use_thy}^* & : & \isarkeep{\cdot} \\ 

1308 
\isarcmd{use_thy_only}^* & : & \isarkeep{\cdot} \\ 

1309 
\isarcmd{update_thy}^* & : & \isarkeep{\cdot} \\ 

1310 
\isarcmd{update_thy_only}^* & : & \isarkeep{\cdot} \\ 

7134  1311 
\end{matharray} 
1312 

7167  1313 
\begin{descr} 
7134  1314 
\item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle 
1315 
process. 

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

7175  1317 
\item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$, 
7987  1318 
$\isarkeyword{update_thy}$, $\isarkeyword{update_thy_only}$] load some 
7895  1319 
theory given as $name$ argument. These commands are basically the same as 
7987  1320 
the corresponding ML functions\footnote{The ML versions also change the 
1321 
implicit theory context to that of the theory loaded.} (see also 

1322 
\cite[\S1,\S6]{isabelleref}). Note that both the ML and Isar versions may 

1323 
load new and oldstyle theories alike. 
