7046

1 

7167

2 
\chapter{Basic Isar elements}


3 


4 
Subsequently, we introduce most of the basic Isar theory and proof commands as


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


6 
elements as provided by generic tools and packages that are either part of

7175

7 
Pure Isabelle, or preloaded by most object logics (such as the Simplifier).

7167

8 
See chapter~\ref{ch:holtools} for actual objectlogic specific elements (for


9 
Isabelle/HOL).

7046

10 

7167

11 
\medskip


12 


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

7175

14 
\emph{improper commands} (indicated by $^*$). Some proof methods and


15 
attributes introduced later may be classified as improper as well. Improper


16 
Isar language elements might be helpful when developing proof documents, while


17 
their use is strongly discouraged for the final version. Typical examples are


18 
diagnostic commands that print terms or theorems according to the current


19 
context; other commands even emulate oldstyle tactical theorem proving, which


20 
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 


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


28 
\begin{matharray}{rcl}


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


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


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


32 
\end{matharray}


33 


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

7167

35 
interactively. Both actual theory specifications and proofs are handled

7175

36 
uniformly  occasionally definitional mechanisms even require some manual


37 
proof. In contrast, ``oldstyle'' Isabelle theories support batch processing


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

7134

39 


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

7175

41 
based on the merge of existing ones. The theory context may be also changed


42 
by $\CONTEXT$ without creating a new theory. In both cases, $\END$ concludes


43 
the theory development; it has to be the very last command of any proper


44 
theory file.

7134

45 


46 
\begin{rail}


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


48 
;


49 
'context' name


50 
;


51 
'end'


52 
;;


53 

7167

54 
filespecs: 'files' ((name  parname) +);

7134

55 
\end{rail}


56 

7167

57 
\begin{descr}

7134

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

7175

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


60 
that any of the base theories are properly loaded (and fully uptodate when


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


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


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


64 
also \S\ref{sec:ML}).

7134

65 

7167

66 
\item [$\CONTEXT~B$] enters an existing theory context $B$, basically in

7134

67 
readonly mode, so only a limited set of commands may be performed. Just as


68 
for $\THEORY$, the theory loader ensures that $B$ is loaded and uptodate.

7175

69 

7167

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

7175

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


72 
itself has to be retracted.

7167

73 
\end{descr}

7134

74 


75 

7167

76 
\subsection{Formal comments}\label{sec:formalcmtthy}

7134

77 

7167

78 
\indexisarcmd{title}\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}


79 
\indexisarcmd{subsubsection}\indexisarcmd{text}

7134

80 
\begin{matharray}{rcl}


81 
\isarcmd{title} & : & \isartrans{theory}{theory} \\


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

7167

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

7134

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


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


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


87 
\end{matharray}


88 

7167

89 
There are several commands to include \emph{formal comments} in theory


90 
specification (a few more are available for proofs, see


91 
\S\ref{sec:formalcmtprf}). In contrast to sourcelevel comments

7134

92 
\verb(*\dots\verb*), which are stripped at the lexical level, any text


93 
given as formal comment is meant to be part of the actual document.


94 
Consequently, it would be included in the final printed version.


95 


96 
Apart from plain prose, formal comments may also refer to logical entities of

7175

97 
the theory context (types, terms, theorems etc.). Proper processing of the


98 
text would then include some further consistency checks with the items


99 
declared in the current theory, e.g.\ typechecking of included


100 
terms.\footnote{The current version of Isabelle/Isar does not process formal

7134

101 
comments in any such way. This will be available as part of the automatic

7175

102 
theory and proof document preparation system (using (PDF){\LaTeX}) that is

7134

103 
planned for the near future.}


104 


105 
\begin{rail}


106 
'title' text text? text?


107 
;

7167

108 
('chapter'  'section'  'subsection'  'subsubsection'  'text') text

7134

109 
;


110 
\end{rail}


111 

7167

112 
\begin{descr}

7134

113 
\item [$\isarkeyword{title}~title~author~date$] specifies the document title

7175

114 
just as in typical {\LaTeX} documents.

7167

115 
\item [$\isarkeyword{chapter}~text$, $\isarkeyword{section}~text$,

7175

116 
$\isarkeyword{subsection}~text$, and $\isarkeyword{subsubsection}~text$]


117 
specify chapter and section headings.

7134

118 
\item [$\TEXT~text$] specifies an actual body of prose text, including

7175

119 
references to formal entities (the latter feature is not yet exploited in


120 
any way).

7167

121 
\end{descr}

7134

122 


123 

7135

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

7134

125 


126 
\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}


127 
\begin{matharray}{rcl}


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


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


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


131 
\end{matharray}


132 


133 
\begin{rail}

7167

134 
'classes' (classdecl comment? +)

7134

135 
;


136 
'classrel' nameref '<' nameref comment?


137 
;


138 
'defaultsort' sort comment?


139 
;


140 
\end{rail}


141 

7167

142 
\begin{descr}

7175

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


144 
subclass of existing classes $\vec c$. Cyclic class structures are ruled


145 
out.

7134

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


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

7175

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


149 
introduce proven class relations.

7134

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

7175

151 
any type variables input without sort constraints. Usually, the default

7134

152 
sort would be only changed when defining new logics.

7167

153 
\end{descr}

7134

154 


155 

7141

156 
\subsection{Types}\label{sec:typespure}

7134

157 


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


159 
\begin{matharray}{rcl}


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


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


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


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


164 
\end{matharray}


165 


166 
\begin{rail}


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


168 
;


169 
'typedecl' typespec infix? comment?


170 
;


171 
'nonterminals' (name +) comment?


172 
;


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


174 
;


175 
\end{rail}


176 

7167

177 
\begin{descr}

7134

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


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


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


181 
syntactic abbreviations, without any logical significance. Internally, type


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


183 
theorems.


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


185 
$t$, intended as an actual logical type. Note that some logics such as


186 
Isabelle/HOL provide their own version of $\isarkeyword{typedecl}$.

7175

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


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


189 
Isabelle's inner syntax of terms or types.

7134

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


191 
ordersorted signature of types by new type constructor arities. This is

7175

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


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

7167

194 
\end{descr}

7134

195 


196 


197 
\subsection{Constants and simple definitions}


198 

7175

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

7134

200 
\begin{matharray}{rcl}


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


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


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


204 
\end{matharray}


205 


206 
\begin{rail}


207 
'consts' (constdecl +)


208 
;


209 
'defs' (thmdecl? prop comment? +)


210 
;


211 
'constdefs' (constdecl prop comment? +)


212 
;


213 


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


215 
;


216 
\end{rail}


217 

7167

218 
\begin{descr}

7175

219 
\item [$\CONSTS~c::\sigma~\dots$] declares constant $c$ to have any instance


220 
of type scheme $\sigma$. The optional mixfix annotations may attach


221 
concrete syntax constants.

7134

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


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


224 
the form of equations admitted as constant definitions.

7175

225 
\item [$\isarkeyword{constdefs}~c::\sigma~eqn~\dots$] combines constant

7134

226 
declarations and definitions, using canonical name $c_def$ for the


227 
definitional axiom.

7167

228 
\end{descr}

7134

229 


230 

7167

231 
\subsection{Syntax and translations}

7134

232 


233 
\indexisarcmd{syntax}\indexisarcmd{translations}


234 
\begin{matharray}{rcl}


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


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


237 
\end{matharray}


238 


239 
\begin{rail}


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


241 
;


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


243 
;


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


245 
;


246 
\end{rail}


247 

7167

248 
\begin{descr}

7175

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


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


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


252 
arbitrary ways. The $mode$ argument refers to the print mode that the


253 
grammar rules belong; unless there is the \texttt{output} flag given, all


254 
productions are added both to the input and output grammar.


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


256 
rules (also known as \emph{macros}): parse/print rules (\texttt{==}), parse


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

7134

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


259 
\texttt{logic}.

7167

260 
\end{descr}

7134

261 


262 


263 
\subsection{Axioms and theorems}


264 


265 
\indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas}


266 
\begin{matharray}{rcl}


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


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


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


270 
\end{matharray}


271 


272 
\begin{rail}

7135

273 
'axioms' (axmdecl prop comment? +)

7134

274 
;


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


276 
;


277 
\end{rail}


278 

7167

279 
\begin{descr}

7134

280 
\item [$\isarkeyword{axioms}~name: \phi~\dots$] introduces arbitrary


281 
statements as logical axioms. In fact, axioms are ``axiomatic theorems'',

7175

282 
and may be referred just as any other theorem later.

7134

283 


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

7175

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

7134

286 
actual theorems.


287 
\item [$\isarkeyword{theorems}~name = thms$] stores lists of existing theorems

7175

288 
as $name$. Typical applications would also involve attributes (to augment


289 
the default simpset, for example).

7134

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


291 
tags the results as ``lemma''.

7167

292 
\end{descr}

7134

293 


294 

7167

295 
\subsection{Name spaces}

7134

296 

7167

297 
\indexisarcmd{global}\indexisarcmd{local}

7134

298 
\begin{matharray}{rcl}


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


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


301 
\end{matharray}


302 

7175

303 
Isabelle organizes any kind of names (of types, constants, theorems etc.) by


304 
hierarchically structured name spaces. Normally the user never has to control


305 
the behavior of name space entry by hand, yet the following commands provide


306 
some way to do so.


307 

7167

308 
\begin{descr}


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


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


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


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

7175

313 
base names only, until $\isarkeyword{local}$ is declared again.

7167

314 
\end{descr}

7134

315 


316 

7167

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

7134

318 


319 
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{setup}


320 
\begin{matharray}{rcl}


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


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

7175

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

7134

324 
\end{matharray}


325 


326 
\begin{rail}


327 
'use' name


328 
;


329 
'ML' text


330 
;


331 
'setup' text


332 
;


333 
\end{rail}


334 

7167

335 
\begin{descr}

7175

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


337 
The current theory context (if present) is passed down to the ML session.


338 
Furthermore, the file name is checked with the $\isarkeyword{files}$


339 
dependency declaration given in the theory header (see also


340 
\S\ref{sec:beginthy}).


341 
\item [$\isarkeyword{ML}~text$] reads and executes ML commands from $text$.


342 
The theory context is passed just as for $\isarkeyword{use}$.

7167

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

7175

344 
applying setup functions $text$, which has to be an ML expression of type


345 
$(theory \to theory)~list$. The $\isarkeyword{setup}$ command is the usual


346 
way to initialize objectlogic specific tools and packages written in ML.

7167

347 
\end{descr}

7134

348 


349 

7167

350 
\subsection{Syntax translation functions}

7134

351 

7167

352 
\indexisarcmd{parseasttranslation}\indexisarcmd{parsetranslation}


353 
\indexisarcmd{printtranslation}\indexisarcmd{typedprinttranslation}


354 
\indexisarcmd{printasttranslation}\indexisarcmd{tokentranslation}

7134

355 
\begin{matharray}{rcl}


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


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


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


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


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


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


362 
\end{matharray}


363 


364 
Syntax translation functions written in ML admit almost arbitrary


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


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


367 
appropriate type. See \cite[\S8]{isabelleref} for more information on syntax


368 
transformations.


369 


370 


371 
\subsection{Oracles}


372 


373 
\indexisarcmd{oracle}


374 
\begin{matharray}{rcl}


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


376 
\end{matharray}


377 

7175

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


379 
control completely  each theorem carries a derivation object recording any


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


381 

7134

382 
\begin{rail}


383 
'oracle' name '=' text comment?


384 
;


385 
\end{rail}


386 

7167

387 
\begin{descr}

7175

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


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


390 
term)$.

7167

391 
\end{descr}

7134

392 


393 


394 
\section{Proof commands}


395 

7167

396 
Proof commands provide transitions of Isar/VM machine configurations. There

7175

397 
are three different modes of operation.

7167

398 
\begin{descr}


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


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

7175

401 
($\approx$ tactic), and enter a subproof to establish the final result.

7167

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

7175

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


404 
\item [$proof(chain)$] is an intermediate mode between $proof(state)$ and


405 
$proof(prove)$: some existing facts have been just picked up in order to use


406 
them when refining the goal to be claimed next.

7167

407 
\end{descr}

7134

408 

7167

409 


410 
\subsection{Formal comments}\label{sec:formalcmtprf}


411 


412 
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect}\indexisarcmd{txt}

7134

413 
\begin{matharray}{rcl}

7167

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


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


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


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

7134

418 
\end{matharray}


419 

7175

420 
These formal comments in proof mode closely correspond to the ones of theory


421 
mode (see \S\ref{sec:formalcmtthy}).


422 

7134

423 
\begin{rail}

7167

424 
('sect'  'subsect'  'subsubsect'  'txt') text

7134

425 
;


426 
\end{rail}


427 


428 


429 
\subsection{Proof context}


430 


431 
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}\indexisarcmd{let}


432 
\begin{matharray}{rcl}


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


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


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


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


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


438 
\end{matharray}


439 

7175

440 
FIXME


441 

7134

442 
\begin{rail}


443 
'fix' (var +) comment?


444 
;

7175

445 
('assume'  'presume') thmdecl? \\ (prop proppat? +) comment?

7134

446 
;

7175

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

7134

448 
;


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


450 
;


451 


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


453 
;


454 
\end{rail}


455 

7167

456 
\begin{descr}


457 
\item [$\FIX{x}$] FIXME


458 
\item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] FIXME


459 
\item [$\DEF{a}{x \equiv t}$] FIXME


460 
\item [$\LET{\vec p = \vec t}$] FIXME


461 
\end{descr}


462 


463 


464 
\subsection{Facts and forward chaining}


465 


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


467 
\begin{matharray}{rcl}


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


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


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


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


472 
\end{matharray}


473 

7175

474 
FIXME


475 

7167

476 
\begin{rail}


477 
'note' thmdef? thmrefs comment?


478 
;


479 
'then' comment?


480 
;


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


482 
;


483 
\end{rail}


484 


485 
\begin{descr}

7175

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


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


488 
right hand sides.

7167

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

7175

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


491 
solve that will be offered these facts to do ``anything appropriate'' (see


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

7167

493 
\S\ref{sec:puremeth}) would do an elimination rather than an introduction.

7175

494 
\item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; also note that

7167

495 
$\THEN$ is equivalent to $\FROM{facts}$.

7175

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


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

7167

498 
\end{descr}


499 


500 


501 
\subsection{Goal statements}


502 


503 
\indexisarcmd{theorem}\indexisarcmd{lemma}


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


505 
\begin{matharray}{rcl}


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


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


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


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


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


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


512 
\end{matharray}


513 

7175

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


515 
and $\LEMMANAME$. New local goals may be claimed within proof mode: four


516 
variants are available, indicating whether the result is meant to solve some


517 
pending goal and whether forward chaining is employed.


518 

7167

519 
\begin{rail}


520 
('theorem'  'lemma') goal


521 
;


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


523 
;


524 


525 
goal: thmdecl? proppat comment?


526 
;


527 
\end{rail}


528 


529 
\begin{descr}


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

7175

531 
eventually resulting in some theorem $\turn \phi$, which will be stored in


532 
the theory.

7167

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


534 
``lemma''.


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


536 
theorem with the current assumption context as hypotheses.

7175

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


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

7167

539 
\item [$\HENCE{name}{\phi}$] abbreviates $\THEN~\HAVE{name}{\phi}$, i.e.\


540 
claims a local goal to be proven by forward chaining the current facts.


541 
\item [$\THUS{name}{\phi}$] abbreviates $\THEN~\SHOW{name}{\phi}$.


542 
\end{descr}


543 


544 


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


546 

7175

547 
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}


548 
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}


549 
\begin{matharray}{rcl}


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


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


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


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


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


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


556 
\end{matharray}


557 

7167

558 
Arbitrary goal refinements via tactics is considered harmful. Consequently


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


560 
\begin{enumerate}

7175

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


562 
intermediate goal to a number of subgoals that are to be solved later.


563 
Facts are passed to $m@1$ for forward chaining if so indicated by


564 
$proof(chain)$ mode.

7167

565 

7175

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

7167

567 
pending goals completely. No facts are passed to $m@2$.


568 
\end{enumerate}


569 


570 
The only other proper way to affect pending goals is by $\SHOWNAME$, which


571 
involves an explicit statement of what is solved.


572 

7175

573 
\medskip


574 

7167

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


576 
or constitute some wellunderstood deterministic reduction to new subgoals.


577 
Arbitrary automatic proof tools that are prone leave a large number of badly


578 
structured subgoals are no help in continuing the proof document in any

7175

579 
intelligible way. A much better technique would be to $\SHOWNAME$ some


580 
nontrivial reduction as an explicit rule, which is solved completely by some


581 
automated method, and then applied to some pending goal.

7167

582 

7175

583 
\medskip


584 


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


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


587 
or introduction rule according to the topmost symbol involved. The default


588 
terminal method is ``$finish$''; it solves all goals by assumption.

7167

589 


590 
\begin{rail}


591 
'proof' interest? meth? comment?


592 
;


593 
'qed' meth? comment?


594 
;


595 
'by' meth meth? comment?


596 
;


597 
('.'  '..'  'sorry') comment?


598 
;


599 


600 
meth: method interest?


601 
;


602 
\end{rail}


603 


604 
\begin{descr}

7175

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


606 
for forward chaining are passed if so indicated by $proof(chain)$.


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

7167

608 
concludes the subproof. If the goal had been $\SHOWNAME$, some pending


609 
subgoal is solved as well by the rule resulting from the result exported to

7175

610 
the enclosing goal context. Thus $\QEDNAME$ may fail for two reasons:


611 
either $m@2$ fails to solve all remaining goals completely, or the resulting


612 
rule does not resolve with any enclosing goal. Debugging such a situation


613 
might involve temporarily changing $\SHOWNAME$ into $\HAVENAME$, or


614 
weakening the local context by replacing $\ASSUMENAME$ by $\PRESUMENAME$.


615 
\item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}; it abbreviates


616 
$\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both methods.


617 
Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done by simply


618 
expanding the abbreviation by hand; note that $\PROOF{m@1}$ is usually


619 
sufficient to see what is going wrong.


620 
\item [$\DDOT$] is a \emph{default proof}; it abbreviates $\BY{default}$.


621 
\item [$\DOT$] is a \emph{trivial proof}, it abbreviates $\BY{}$, where


622 
method ``$$'' does nothing except inserting any facts into the proof state.

7167

623 
\item [$\isarkeyword{sorry}$] is a \emph{fake proof}; provided that


624 
\texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ pretends to solve


625 
the goal without much ado. Of course, the result is a fake theorem only,

7175

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


627 
as $[!]$ in the printed result. The main application of

7167

628 
$\isarkeyword{sorry}$ is to support topdown proof development.


629 
\end{descr}

7134

630 


631 


632 
\subsection{Block structure}


633 

7167

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


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


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


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


638 
different context within a subproof are typically switched via


639 
$\isarkeyword{next}$, which is just a single blockclose followed by


640 
blockopen again. Thus the effect of $\isarkeyword{next}$ is to reset the


641 
proof context to that of the head of the subproof. Note that there is no

7175

642 
goal focus involved here!

7167

643 

7175

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


645 
as well. These typically achieve a strong forward style of reasoning.

7167

646 

7134

647 
\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}


648 
\begin{matharray}{rcl}


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


650 
\isarcmd{\{\{} & : & \isartrans{proof(state)}{proof(state)} \\


651 
\isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\


652 
\end{matharray}


653 

7167

654 
\begin{descr}


655 
\item [$\isarkeyword{next}$] switches to a fresh block within a subproof,


656 
resetting the context to the initial one.


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


658 
close blocks. Any current facts pass through $\isarkeyword{\{\{}$


659 
unchanged, while $\isarkeyword{\}\}}$ causes them to be \emph{exported} into


660 
the enclosing context. Thus fixed variables are generalized, assumptions


661 
discharged, and local definitions eliminated.


662 
\end{descr}

7134

663 


664 
\subsection{Calculational proof}


665 


666 
\indexisarcmd{also}\indexisarcmd{finally}


667 
\begin{matharray}{rcl}


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


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


670 
\end{matharray}


671 

7175

672 
FIXME


673 

7134

674 
\begin{rail}


675 
('also'  'finally') transrules? comment?


676 
;


677 


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


679 
;


680 
\end{rail}


681 

7167

682 
\begin{descr}

7175

683 
\item [$\ALSO~(thms)$] FIXME


684 
\item [$\FINALLY~(thms)$] FIXME

7167

685 
\end{descr}

7134

686 


687 


688 


689 
\subsection{Improper proof steps}


690 

7175

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


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


693 
come in handy for exploring and debugging.

7167

694 


695 
\indexisarcmd{apply}\indexisarcmd{thenapply}\indexisarcmd{back}

7134

696 
\begin{matharray}{rcl}


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


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


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


700 
\end{matharray}


701 


702 
\railalias{thenapply}{then\_apply}


703 
\railterm{thenapply}


704 


705 
\begin{rail}


706 
'apply' method


707 
;


708 
thenapply method


709 
;


710 
'back'


711 
;


712 
\end{rail}


713 

7167

714 
\begin{descr}

7134

715 
\item [$ $] FIXME

7167

716 
\end{descr}

7134

717 


718 


719 
\section{Other commands}


720 


721 
\subsection{Diagnostics}


722 


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


724 
\begin{matharray}{rcl}


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


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


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


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


729 
\end{matharray}


730 


731 
\begin{rail}


732 
'typ' type


733 
;


734 
'term' term


735 
;


736 
'prop' prop


737 
;


738 
'thm' thmrefs


739 
;


740 
\end{rail}


741 

7167

742 
\begin{descr}

7134

743 
\item [$\isarkeyword{typ}~\tau$, $\isarkeyword{term}~t$,


744 
$\isarkeyword{prop}~\phi$] read and print types / terms / propositions


745 
according to the current theory or proof context.


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


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

7175

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


749 
theory or proof; the result is discarded.

7167

750 
\end{descr}

7134

751 


752 


753 
\subsection{System operations}


754 

7167

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


756 
\indexisarcmd{updatethy}\indexisarcmd{updatethyonly}

7134

757 
\begin{matharray}{rcl}


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


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


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


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


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


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


764 
\end{matharray}


765 

7167

766 
\begin{descr}

7134

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


768 
process.


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

7175

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


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


772 
theory given as $name$ argument. These commands are exactly the same as the


773 
corresponding ML functions (see also \cite[\S1 and \S6]{isabelleref}).


774 
Note that both the ML and Isar versions of these commands may load new and


775 
oldstyle theories alike.

7167

776 
\end{descr}

7134

777 


778 

7046

779 
%%% Local Variables:


780 
%%% mode: latex


781 
%%% TeXmaster: "isarref"


782 
%%% End:
