7046

1 

7895

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

7167

3 

7315

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


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

7895

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


7 
Simplifier) that are either part of Pure Isabelle or preloaded by most object


8 
logics. Chapter~\ref{ch:holtools} refers to actual objectlogic specific


9 
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


20 
proving, which facilitates porting of legacy proof scripts.

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

7134

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


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


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


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


48 
last command in a 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


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: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}

7981

131 
package to be included in {\LaTeX}.}

7167

132 
\end{descr}

7134

133 

7895

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

7981

135 
macro with the name prefixed by \verb,\isamarkup, (e.g.\

7895

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

7981

137 
argument is passed to that macro unchanged, i.e.\ further {\LaTeX} commands


138 
may be included here as well.

7895

139 

8485

140 
\medskip


141 


142 
Additional markup commands are available for proofs (see

7895

143 
\S\ref{sec:markupprf}). Also note that the $\isarkeyword{header}$


144 
declaration (see \S\ref{sec:beginthy}) admits to insert document markup


145 
elements just preceding the actual theory definition.


146 

7134

147 

7135

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

7134

149 


150 
\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}


151 
\begin{matharray}{rcl}


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


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


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


155 
\end{matharray}


156 


157 
\begin{rail}

7167

158 
'classes' (classdecl comment? +)

7134

159 
;


160 
'classrel' nameref '<' nameref comment?


161 
;


162 
'defaultsort' sort comment?


163 
;


164 
\end{rail}


165 

7167

166 
\begin{descr}

7335

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


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

7134

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


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

7895

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

7175

172 
introduce proven class relations.

7134

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

7895

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

7134

175 
sort would be only changed when defining new logics.

7167

176 
\end{descr}

7134

177 


178 

7315

179 
\subsection{Primitive types and type abbreviations}\label{sec:typespure}

7134

180 


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


182 
\begin{matharray}{rcl}


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


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


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


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


187 
\end{matharray}


188 


189 
\begin{rail}


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


191 
;


192 
'typedecl' typespec infix? comment?


193 
;


194 
'nonterminals' (name +) comment?


195 
;


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


197 
;


198 
\end{rail}


199 

7167

200 
\begin{descr}

7335

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

7134

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


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

7895

204 
syntactic abbreviations without any logical significance. Internally, type

7981

205 
synonyms are fully expanded.

7134

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

7895

207 
$t$, intended as an actual logical type. Note that objectlogics such as


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

7175

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


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


211 
Isabelle's inner syntax of terms or types.

7335

212 
\item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's ordersorted


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


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

7895

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

7167

216 
\end{descr}

7134

217 


218 

7981

219 
\subsection{Constants and simple definitions}\label{sec:consts}

7134

220 

7175

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

7134

222 
\begin{matharray}{rcl}


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


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


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


226 
\end{matharray}


227 


228 
\begin{rail}


229 
'consts' (constdecl +)


230 
;

7608

231 
'defs' (axmdecl prop comment? +)

7134

232 
;


233 
'constdefs' (constdecl prop comment? +)


234 
;


235 


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


237 
;


238 
\end{rail}


239 

7167

240 
\begin{descr}

7335

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


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

7895

243 
to the constants declared.

7335

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


245 
existing constant. See \cite[\S6]{isabelleref} for more details on the


246 
form of equations admitted as constant definitions.


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


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


249 
axiom.

7167

250 
\end{descr}

7134

251 


252 

7981

253 
\subsection{Syntax and translations}\label{sec:syntrans}

7134

254 


255 
\indexisarcmd{syntax}\indexisarcmd{translations}


256 
\begin{matharray}{rcl}


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


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


259 
\end{matharray}


260 


261 
\begin{rail}


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


263 
;


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


265 
;


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


267 
;


268 
\end{rail}


269 

7167

270 
\begin{descr}

7175

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


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


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

7335

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


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


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


277 
output grammar.

7175

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

7981

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

7895

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


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

7134

282 
\texttt{logic}.

7167

283 
\end{descr}

7134

284 


285 


286 
\subsection{Axioms and theorems}


287 


288 
\indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas}


289 
\begin{matharray}{rcl}


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


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


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


293 
\end{matharray}


294 


295 
\begin{rail}

7135

296 
'axioms' (axmdecl prop comment? +)

7134

297 
;


298 
('theorems'  'lemmas') thmdef? thmrefs


299 
;


300 
\end{rail}


301 

7167

302 
\begin{descr}

7335

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

7895

304 
axioms of the metalogic. In fact, axioms are ``axiomatic theorems'', and


305 
may be referred later just as any other theorem.

7134

306 


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

7175

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

7134

309 
actual theorems.

7335

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

7981

311 
Typical applications would also involve attributes, to augment the

7335

312 
Simplifier context, for example.

7134

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


314 
tags the results as ``lemma''.

7167

315 
\end{descr}

7134

316 


317 

7167

318 
\subsection{Name spaces}

7134

319 

7167

320 
\indexisarcmd{global}\indexisarcmd{local}

7134

321 
\begin{matharray}{rcl}


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


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


324 
\end{matharray}


325 

7895

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


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


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


329 
following commands provide some way to do so.

7175

330 

7167

331 
\begin{descr}


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


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


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

7895

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


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

7167

337 
\end{descr}

7134

338 


339 

7167

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

7134

341 

7895

342 
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{MLsetup}\indexisarcmd{setup}

7134

343 
\begin{matharray}{rcl}


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


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

7895

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

7175

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

7134

348 
\end{matharray}


349 

7895

350 
\railalias{MLsetup}{ML\_setup}


351 
\railterm{MLsetup}


352 

7134

353 
\begin{rail}


354 
'use' name


355 
;

7895

356 
('ML'  MLsetup  'setup') text

7134

357 
;


358 
\end{rail}


359 

7167

360 
\begin{descr}

7175

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

7466

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

7981

363 
but may not be modified. Furthermore, the file name is checked with the

7466

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


365 
also \S\ref{sec:beginthy}).


366 

7895

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


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


369 


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


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


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


373 

7167

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

8379

375 
applying $text$, which refers to an ML expression of type


376 
\texttt{(theory~>~theory)~list}. The $\isarkeyword{setup}$ command is the


377 
canonical way to initialize objectlogic specific tools and packages written


378 
in ML.

7167

379 
\end{descr}

7134

380 


381 

8250

382 
\subsection{Syntax translation functions}

7134

383 

8250

384 
\indexisarcmd{parseasttranslation}\indexisarcmd{parsetranslation}


385 
\indexisarcmd{printtranslation}\indexisarcmd{typedprinttranslation}


386 
\indexisarcmd{printasttranslation}\indexisarcmd{tokentranslation}


387 
\begin{matharray}{rcl}


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


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


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


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


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


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


394 
\end{matharray}

7134

395 

8250

396 
Syntax translation functions written in ML admit almost arbitrary


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


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

8379

399 
appropriate type.


400 


401 
\begin{ttbox}


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


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


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


405 
val typed_print_translation :


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


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


408 
val token_translation :


409 
(string * string * (string > string * real)) list


410 
\end{ttbox}


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

7134

412 


413 


414 
\subsection{Oracles}


415 


416 
\indexisarcmd{oracle}


417 
\begin{matharray}{rcl}


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


419 
\end{matharray}


420 

7175

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


422 
control completely  each theorem carries a derivation object recording any


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


424 

7134

425 
\begin{rail}


426 
'oracle' name '=' text comment?


427 
;


428 
\end{rail}


429 

7167

430 
\begin{descr}

7175

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

8379

432 
function $text$, which has to be of type


433 
\texttt{Sign.sg~*~Object.T~>~term}.

7167

434 
\end{descr}

7134

435 


436 


437 
\section{Proof commands}


438 

7987

439 
Proof commands perform transitions of Isar/VM machine configurations, which

7315

440 
are blockstructured, consisting of a stack of nodes with three main

7335

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


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


443 
modes of operation:

7167

444 
\begin{descr}


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


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

7895

447 
(read: tactic), and enter a subproof to establish the actual result.

7167

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

7987

449 
augmented by \emph{stating} additional assumptions, intermediate results


450 
etc.

7895

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

7987

452 
$proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$''


453 
register) have been just picked up in order to be used when refining the


454 
goal claimed next.

7167

455 
\end{descr}

7134

456 

7167

457 

7895

458 
\subsection{Proof markup commands}\label{sec:markupprf}

7167

459 

7987

460 
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect}

7895

461 
\indexisarcmd{txt}\indexisarcmd{txtraw}

7134

462 
\begin{matharray}{rcl}

8101

463 
\isarcmd{sect} & : & \isartrans{proof}{proof} \\


464 
\isarcmd{subsect} & : & \isartrans{proof}{proof} \\


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


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


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

7134

468 
\end{matharray}


469 

7895

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


471 
mode (see \S\ref{sec:markupthy}). Note that $\isarkeyword{txt_raw}$ is


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


473 


474 
\railalias{txtraw}{txt\_raw}


475 
\railterm{txtraw}

7175

476 

7134

477 
\begin{rail}

7895

478 
('sect'  'subsect'  'subsubsect'  'txt'  txtraw) text

7134

479 
;


480 
\end{rail}


481 


482 

7315

483 
\subsection{Proof context}\label{sec:proofcontext}

7134

484 

7315

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

7134

486 
\begin{matharray}{rcl}


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


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


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


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


491 
\end{matharray}


492 

7315

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


494 
former closely correspond to Skolem constants, or metalevel universal


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


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

7987

497 
a local value that may be used in the subsequent proof as any other variable

7895

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

7987

499 
context will be universally closed wrt.\ $x$ at the outermost level: $\edrv


500 
\All x \phi$ (this is expressed using Isabelle's metavariables).

7315

501 


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


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

7895

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


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


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


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


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


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


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


511 
user.

7315

512 

7319

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

7987

514 
combining $\FIX x$ with another version of assumption that causes any


515 
hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule.


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

7175

517 

7134

518 
\begin{rail}

7431

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

7134

520 
;

7315

521 
('assume'  'presume') (assm comment? + 'and')

7134

522 
;

7175

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

7134

524 
;


525 


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


527 
;

7458

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

7431

529 
;

7315

530 
assm: thmdecl? (prop proppat? +)


531 
;

7134

532 
\end{rail}


533 

7167

534 
\begin{descr}

7315

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


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

7335

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

7895

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

7335

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


540 
leaves $\Phi$ as new subgoals.


541 


542 
Several lists of assumptions may be given (separated by

7895

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


544 
these concatenated.

7315

545 
\item [$\DEF{a}{x \equiv t}$] introduces a local (nonpolymorphic) definition.


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

7987

547 
$\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\ASSUME{}{x \equiv t}$, with the

7335

548 
resulting hypothetical equation solved by reflexivity.

7431

549 


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

7167

551 
\end{descr}


552 

7895

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


554 
current context as a list of theorems.

7315

555 

7167

556 


557 
\subsection{Facts and forward chaining}


558 


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


560 
\begin{matharray}{rcl}


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


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


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


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


565 
\end{matharray}


566 

7319

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

7335

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


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


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

7987

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

7167

572 
\begin{rail}


573 
'note' thmdef? thmrefs comment?


574 
;


575 
'then' comment?


576 
;


577 
('from'  'with') thmrefs comment?


578 
;


579 
\end{rail}


580 


581 
\begin{descr}

7175

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


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


584 
right hand sides.

7167

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

7895

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


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


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


589 
\S\ref{sec:puremeth}) would typically do an elimination rather than an


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


591 
state before operation.

7335

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

7458

593 
equivalent to $\FROM{this}$.

7175

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


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

7167

596 
\end{descr}


597 

7389

598 
Basic proof methods (such as $rule$, see \S\ref{sec:puremeth}) expect

7895

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


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

7458

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

7895

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


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

7389

604 

7167

605 


606 
\subsection{Goal statements}


607 


608 
\indexisarcmd{theorem}\indexisarcmd{lemma}


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


610 
\begin{matharray}{rcl}


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


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

7987

613 
\isarcmd{have} & : & \isartrans{proof(state) ~~ proof(chain)}{proof(prove)} \\


614 
\isarcmd{show} & : & \isartrans{proof(state) ~~ proof(chain)}{proof(prove)} \\

7167

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


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


617 
\end{matharray}


618 

7175

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

7895

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


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

7987

622 
some pending goal or whether forward chaining is employed.

7175

623 

7167

624 
\begin{rail}


625 
('theorem'  'lemma') goal


626 
;


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


628 
;


629 


630 
goal: thmdecl? proppat comment?


631 
;


632 
\end{rail}


633 


634 
\begin{descr}

7335

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

7895

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

7987

637 
\item [$\LEMMA{a}{\phi}$] is similar to $\THEOREMNAME$, but tags the result as

7167

638 
``lemma''.

7335

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

7167

640 
theorem with the current assumption context as hypotheses.

7335

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

7895

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


643 
(cf.\ \S\ref{sec:proofcontext}).


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


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


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


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


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

7167

649 
\end{descr}


650 


651 


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


653 

7175

654 
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}


655 
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}


656 
\begin{matharray}{rcl}


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


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


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


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


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


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


663 
\end{matharray}


664 

7335

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


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

7167

667 
\begin{enumerate}

7175

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

7335

669 
goal to a number of subgoals that are to be solved later. Facts are passed

7895

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

7167

671 

7987

672 
\item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve


673 
remaining goals. No facts are passed to $m@2$.

7167

674 
\end{enumerate}


675 

7335

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


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

7167

678 

7175

679 
\medskip


680 

7167

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

7895

682 
or constitute some wellunderstood reduction to new subgoals. Arbitrary


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


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

7987

685 
way.


686 
%FIXME


687 
%A more appropriate technique would be to $\SHOWNAME$ some nontrivial


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


689 
%method, and then applied to some pending goal.

7167

690 

7175

691 
\medskip


692 


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


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

7458

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

7987

696 
separate default terminal method. In any case, any goals left after that are


697 
solved by assumption as the very last step.

7167

698 


699 
\begin{rail}


700 
'proof' interest? meth? comment?


701 
;


702 
'qed' meth? comment?


703 
;


704 
'by' meth meth? comment?


705 
;


706 
('.'  '..'  'sorry') comment?


707 
;


708 


709 
meth: method interest?


710 
;


711 
\end{rail}


712 


713 
\begin{descr}

7335

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


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


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

7895

717 
concludes the subproof by assumption. If the goal had been $\SHOWNAME$ (or


718 
$\THUSNAME$), some pending subgoal is solved as well by the rule resulting


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


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


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


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


723 
context. Debugging such a situation might involve temporarily changing


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


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


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

7987

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


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

7895

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

7175

730 
sufficient to see what is going wrong.

7895

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


732 
abbreviates $\BY{default}$.


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

8195

734 
abbreviates $\BY{this}$.

8379

735 
\item [$\SORRY$] is a \emph{fake proof}\index{proof!fake}; provided that the


736 
\texttt{quick_and_dirty} flag is enabled, $\SORRY$ pretends to solve the


737 
goal without further ado. Of course, the result is a fake theorem only,


738 
involving some oracle in its internal derivation object (this is indicated


739 
as ``$[!]$'' in the printed result). The main application of $\SORRY$ is to


740 
support experimentation and topdown proof development.

7315

741 
\end{descr}


742 


743 


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


745 


746 
\indexisarcmd{let}


747 
\begin{matharray}{rcl}


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


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


750 
\end{matharray}


751 


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

7987

753 
or by annotating assumptions or goal statements with a list of patterns


754 
$\ISS{p@1\;\dots}{p@n}$. In both cases, higherorder matching is invoked to


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


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


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


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


759 
postfix position.

7315

760 

7319

761 
Term abbreviations are quite different from actual local definitions as


762 
introduced via $\DEFNAME$ (see \S\ref{sec:proofcontext}). The latter are

7315

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


764 
during the input process just after type checking.


765 


766 
\begin{rail}


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


768 
;


769 
\end{rail}


770 


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


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


773 


774 
\begin{descr}


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


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


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


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


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


780 
\end{descr}


781 

7988

782 
A few \emph{automatic} term abbreviations\index{term abbreviations} for goals


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

7466

784 
$\Var{thesis_prop}$\indexisarvar{thesisprop} refers to the full proposition


785 
(which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesisconcl} to its


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

7335

787 
objectlogical statement. The latter two abstract over any metalevel

7987

788 
parameters.

7315

789 

7466

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


791 
$\Var{this_prop}$\indexisarvar{thisprop},


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


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


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

7895

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

7466

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

7987

797 
the latter are calculational proofs (see \S\ref{sec:calculation}).

7315

798 


799 

7134

800 
\subsection{Block structure}


801 

7397

802 
\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}


803 
\begin{matharray}{rcl}

8448

804 
\NEXT & : & \isartrans{proof(state)}{proof(state)} \\

7974

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


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

7397

807 
\end{matharray}


808 

7167

809 
While Isar is inherently blockstructured, opening and closing blocks is


810 
mostly handled rather casually, with little explicit userintervention. Any


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


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

8448

813 
different context within a subproof may be switched via $\NEXT$, which is


814 
just a single blockclose followed by blockopen again. Thus the effect of


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


816 
here!

7167

817 

7175

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

7895

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

7167

820 


821 
\begin{descr}

8448

822 
\item [$\NEXT$] switches to a fresh block within a subproof, resetting the


823 
local context to the initial one.

7167

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

7895

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


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


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


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


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


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


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

7167

832 
\end{descr}

7134

833 


834 


835 
\section{Other commands}


836 

8448

837 
\subsection{Diagnostics}\label{sec:diag}

7134

838 

8485

839 
\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ}


840 
\indexisarcmd{printfacts}\indexisarcmd{printbinds}

7134

841 
\begin{matharray}{rcl}

8485

842 
\isarcmd{pr} & : & \isarkeep{\cdot} \\

7974

843 
\isarcmd{thm} & : & \isarkeep{theory~~proof} \\

7134

844 
\isarcmd{term} & : & \isarkeep{theory~~proof} \\


845 
\isarcmd{prop} & : & \isarkeep{theory~~proof} \\

7974

846 
\isarcmd{typ} & : & \isarkeep{theory~~proof} \\

8379

847 
\isarcmd{print_facts} & : & \isarkeep{proof} \\


848 
\isarcmd{print_binds} & : & \isarkeep{proof} \\

7134

849 
\end{matharray}


850 

7335

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


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


853 
theory or proof configuration is not changed.


854 

7134

855 
\begin{rail}

8485

856 
'pr' modes? nat?

7134

857 
;

8485

858 
'thm' modes? thmrefs


859 
;


860 
'term' modes? term

7134

861 
;

8485

862 
'prop' modes? prop

7134

863 
;

8485

864 
'typ' modes? type


865 
;


866 


867 
modes: '(' (name + ) ')'

7134

868 
;


869 
\end{rail}


870 

7167

871 
\begin{descr}

8485

872 
\item [$\isarkeyword{pr}~n$] prints the current toplevel state, i.e.\ the


873 
theory identifier or proof state. The latter includes the proof context,


874 
current facts and goals. The optional argument $n$ affects the implicit


875 
limit of goals to be displayed, which is initially 10. Omitting the limit


876 
leaves the value unchanged.

7974

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


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


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


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


881 
$thms$ do not have any permanent effect.

7987

882 
\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, typecheck and


883 
print terms or propositions according to the current theory or proof

7895

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


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


886 
abbreviations.

7974

887 
\item [$\isarkeyword{typ}~\tau$] reads and prints types of the metalogic


888 
according to the current theory or proof context.

8379

889 
\item [$\isarkeyword{print_facts}$] prints any named facts of the current


890 
context, including assumptions and local results.


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


892 
the context.

8485

893 
\end{descr}


894 


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


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


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


898 
features.


899 


900 
\medskip


901 


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


903 
current proof state with mathematical symbols and special characters


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


905 
\cite{isabellesys}. The resulting text can be directly pasted into and


906 
\verb,\begin{isabelle},\dots\verb,\end{isabelle}, environment.


907 


908 
Note that $\isarkeyword{pr}~(latex)$ is sufficient to achieve the same output,


909 
if the current Isabelle session has the other modes already activated, say due


910 
to some particular user interface configuration such as Proof~General


911 
\cite{proofgeneral} with XSymbol mode \cite{FIXME}.


912 


913 


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


915 


916 
\indexisarcmd{undo}\indexisarcmd{redo}\indexisarcmd{kill}


917 
\begin{matharray}{rcl}


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


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


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


921 
\end{matharray}


922 


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


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


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


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


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


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


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


930 
undoable.


931 


932 
\begin{warn}


933 
History commands may not be used with user interfaces such as Proof~General


934 
\cite{proofgeneral}, which takes care of stepping forth and back itself.


935 
Interfering with manual $\isarkeyword{undo}$, $\isarkeyword{redo}$, or even


936 
$\isarkeyword{kill}$ commands would quickly result in utter confusion.


937 
\end{warn}


938 


939 
\begin{descr}


940 
\item [$\isarkeyword{undo}$] revokes the latest statetransforming command.


941 
\item [$\isarkeyword{redo}$] undos the latest $\isarkeyword{undo}$.


942 
\item [$\isarkeyword{kill}$] aborts the current history level.

7167

943 
\end{descr}

7134

944 


945 

8379

946 
\subsection{Metalinguistic features}


947 


948 
\indexisarcmd{oops}


949 
\begin{matharray}{rcl}


950 
\isarcmd{oops}^* & : & \isartrans{proof}{theory} \\


951 
\end{matharray}


952 


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


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


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


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


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


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


959 
proof anyhow.


960 


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


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


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


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


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


966 
``$\OOPS$'' keyword.


967 

8485

968 
\medskip The $\OOPS$ command is undoable, in contrast to $\isarkeyword{kill}$


969 
(see \S\ref{sec:history}). The effect is to get back to the theory


970 
\emph{before} the opening of the proof.


971 


972 
\begin{descr}


973 
\item [$\isarkeyword{oops}$] dismisses the current proof, leaving the text in


974 
as properly processed.


975 
\end{descr}


976 

8379

977 

7134

978 
\subsection{System operations}


979 

7167

980 
\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{usethy}\indexisarcmd{usethyonly}


981 
\indexisarcmd{updatethy}\indexisarcmd{updatethyonly}

7134

982 
\begin{matharray}{rcl}


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


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


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


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


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


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


989 
\end{matharray}


990 

7167

991 
\begin{descr}

7134

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


993 
process.


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

7175

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

7987

996 
$\isarkeyword{update_thy}$, $\isarkeyword{update_thy_only}$] load some

7895

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

7987

998 
the corresponding ML functions\footnote{The ML versions also change the


999 
implicit theory context to that of the theory loaded.} (see also


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


1001 
load new and oldstyle theories alike.

7167

1002 
\end{descr}

7134

1003 

7987

1004 
These system commands are scarcely used when working with the Proof~General


1005 
interface, since loading of theories is done fully transparently.

7134

1006 

8379

1007 


1008 
\subsection{Emulating tactic scripts}


1009 


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


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


1012 
come in handy for interactive exploration and debugging.


1013 


1014 
\indexisarcmd{apply}\indexisarcmd{applyend}\indexisarcmd{back}\indexisarmeth{tactic}


1015 
\begin{matharray}{rcl}


1016 
\isarcmd{apply} & : & \isartrans{proof(prove)}{proof(prove)} \\

8485

1017 
\isarcmd{apply_end} & : & \isartrans{proof(state)}{proof(state)} \\


1018 
\isarcmd{back} & : & \isartrans{proof}{proof} \\

8379

1019 
tactic & : & \isarmeth \\


1020 
\end{matharray}


1021 


1022 
\railalias{applyend}{apply\_end}


1023 
\railterm{applyend}


1024 


1025 
\begin{rail}


1026 
'apply' method


1027 
;


1028 
applyend method


1029 
;


1030 
'tactic' text


1031 
;


1032 
\end{rail}


1033 


1034 
\begin{descr}


1035 
\item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in an initial


1036 
position, but retains ``$prove$'' mode (unlike $\PROOFNAME$). Thus


1037 
consecutive method applications may be given just as in tactic scripts. In


1038 
order to complete the proof properly, any of the actual structured proof


1039 
commands (e.g.\ ``$\DOT$'') has to be given eventually.


1040 


1041 
Facts are passed to $m$ as indicated by the goal's forwardchain mode.


1042 
Common use of $\isarkeyword{apply}$ would be in a purely backward manner,


1043 
though.


1044 
\item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in


1045 
terminal position. Basically, this simulates a multistep tactic script for


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


1047 


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


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


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

8485

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


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


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


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

8379

1055 
\item [$tactic~text$] produces a proof method from any ML text of type


1056 
\texttt{tactic}. Apart from the usual ML environment, and the current


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


1058 
bound values:

8485

1059 
%%FIXME ttbox produces too much trailing space


1060 
{\footnotesize\begin{verbatim}

8379

1061 
val ctxt : Proof.context


1062 
val facts : thm list


1063 
val thm : string > thm


1064 
val thms : string > thm list

8485

1065 
\end{verbatim}}

8379

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


1067 
indicates any current facts for forwardchaining, and


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


1069 
theorems) from the context.


1070 
\end{descr}


1071 


1072 

7046

1073 
%%% Local Variables:


1074 
%%% mode: latex


1075 
%%% TeXmaster: "isarref"


1076 
%%% End:
