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


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


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


14 
\emph{improper commands} (indicated by $^*$). Improper commands might be


15 
helpful when developing proof documents, while their use is strongly


16 
discouraged for the final outcome. Typical examples are diagnostic commands


17 
that print terms or theorems according to the current context; other commands


18 
even emulate oldstyle tactical theorem proving, which facilitates porting of


19 
legacy proof scripts.


20 

7134

21 


22 
\section{Theory commands}


23 

7167

24 
\subsection{Defining theories}\label{sec:beginthy}

7134

25 


26 
\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context}


27 
\begin{matharray}{rcl}


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


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


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


31 
\end{matharray}


32 


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

7167

34 
interactively. Both actual theory specifications and proofs are handled


35 
uniformly  occasionally definitional mechanisms even require some proof.


36 
In contrast, ``oldstyle'' Isabelle theories support batch processing only,


37 
with the proof scripts collected in separate ML files.

7134

38 


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

7167

40 
based on the merge of existing ones. The theory context may be changed by


41 
$\CONTEXT$ without creating a new theory. In both cases $\END$ concludes the


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


43 
file.

7134

44 


45 
\begin{rail}


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


47 
;


48 
'context' name


49 
;


50 
'end'


51 
;;


52 

7167

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

7134

54 
\end{rail}


55 

7167

56 
\begin{descr}

7134

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


58 
existing ones $B@1 + \cdots + B@n$. Note that Isabelle's theory loader


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

7167

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


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


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


63 
via $\isarcmd{use}$ (see also \S\ref{sec:ML}).

7134

64 

7167

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

7134

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


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


68 

7167

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


70 
\end{descr}

7134

71 


72 

7167

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

7134

74 

7167

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


76 
\indexisarcmd{subsubsection}\indexisarcmd{text}

7134

77 
\begin{matharray}{rcl}


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


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

7167

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

7134

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


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


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


84 
\end{matharray}


85 

7167

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


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


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

7134

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


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


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


92 


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


94 
the current theory context (types, terms, theorems etc.). Proper processing


95 
of the text would then include some further consistency checks with the items


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


97 
\footnote{The current version of Isabelle/Isar does not process formal


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


99 
theory and proof document preparation system (via (PDF)LaTeX) that is


100 
planned for the near future.}


101 


102 
\begin{rail}


103 
'title' text text? text?


104 
;

7167

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

7134

106 
;


107 
\end{rail}


108 

7167

109 
\begin{descr}

7134

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


111 
just as in typical LaTeX documents.

7167

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


113 
$\isarkeyword{subsection}~text$, $\isarkeyword{subsubsection}~text$] specify


114 
chapter and subsection headings.

7134

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


116 
references to formal entities.\footnote{The latter feature is not yet


117 
exploited in any way.}

7167

118 
\end{descr}

7134

119 


120 

7135

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

7134

122 


123 
\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}


124 
\begin{matharray}{rcl}


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


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


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


128 
\end{matharray}


129 


130 
\begin{rail}

7167

131 
'classes' (classdecl comment? +)

7134

132 
;


133 
'classrel' nameref '<' nameref comment?


134 
;


135 
'defaultsort' sort comment?


136 
;


137 
\end{rail}


138 

7167

139 
\begin{descr}

7134

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


141 
subclass of existing classes $cs$. Cyclic class structures are ruled out.


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


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


144 
$\isarkeyword{instance}$ command provides a way introduce proven class


145 
relations (see \S\ref{sec:axclass}).


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


147 
any type variables input without sort constraints. Typically, the default


148 
sort would be only changed when defining new logics.

7167

149 
\end{descr}

7134

150 


151 

7141

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

7134

153 


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


155 
\begin{matharray}{rcl}


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


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


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


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


160 
\end{matharray}


161 


162 
\begin{rail}


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


164 
;


165 
'typedecl' typespec infix? comment?


166 
;


167 
'nonterminals' (name +) comment?


168 
;


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


170 
;


171 
\end{rail}


172 

7167

173 
\begin{descr}

7134

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


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


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


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


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


179 
theorems.


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


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


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


183 
\item [$\isarkeyword{nonterminals}~c~\dots$] declares $0$ary type


184 
constructors $c$ to act as purely syntactic types, i.e.\ nonterminal symbols


185 
of Isabelle's inner syntax of terms or types.


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


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


188 
done axiomatically! The $\isarkeyword{instance}$ command provides a way


189 
introduce proven type arities (see \S\ref{sec:axclass}).

7167

190 
\end{descr}

7134

191 


192 


193 
\subsection{Constants and simple definitions}


194 


195 
\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}


196 
\begin{matharray}{rcl}


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


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


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


200 
\end{matharray}


201 


202 
\begin{rail}


203 
'consts' (constdecl +)


204 
;


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


206 
;


207 
'constdefs' (constdecl prop comment? +)


208 
;


209 


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


211 
;


212 
\end{rail}


213 

7167

214 
\begin{descr}

7134

215 
\item [$\CONSTS~c::\tau~\dots$] declares constant $c$ to have any instance of


216 
type scheme $\tau$. The optional mixfix annotations may attach concrete


217 
syntax to the constant.


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


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


220 
the form of equations admitted as constant definitions.


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


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


223 
definitional axiom.

7167

224 
\end{descr}

7134

225 


226 

7167

227 
\subsection{Syntax and translations}

7134

228 


229 
\indexisarcmd{syntax}\indexisarcmd{translations}


230 
\begin{matharray}{rcl}


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


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


233 
\end{matharray}


234 


235 
\begin{rail}


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


237 
;


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


239 
;


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


241 
;


242 
\end{rail}


243 

7167

244 
\begin{descr}

7134

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


246 
except the actual logical signature extension. Thus the context free


247 
grammar of Isabelle's inner syntax may be augmented in arbitrary ways. The


248 
$mode$ argument refers to the print mode that the grammar rules belong;


249 
unless there is the \texttt{output} flag given, all productions are added


250 
both to the input and output grammar.


251 
\item [$\isarkeyword{translations}~rule~\dots$] specifies syntactic


252 
translation rules (macros): parse/print rules (\texttt{==}), parse rules


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


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


255 
\texttt{logic}.

7167

256 
\end{descr}

7134

257 


258 


259 
\subsection{Axioms and theorems}


260 


261 
\indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas}


262 
\begin{matharray}{rcl}


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


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


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


266 
\end{matharray}


267 


268 
\begin{rail}

7135

269 
'axioms' (axmdecl prop comment? +)

7134

270 
;


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


272 
;


273 
\end{rail}


274 

7167

275 
\begin{descr}

7134

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


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


278 
and may be referred as any other theorems later.


279 


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


281 
Everyday work is normally done the hard way, with proper definitions and


282 
actual theorems.


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


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


285 
the default simpset, for example.


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


287 
tags the results as ``lemma''.

7167

288 
\end{descr}

7134

289 


290 

7167

291 
\subsection{Name spaces}

7134

292 

7167

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


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


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


296 
some way to do so.


297 


298 
\indexisarcmd{global}\indexisarcmd{local}

7134

299 
\begin{matharray}{rcl}


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


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


302 
\end{matharray}


303 

7167

304 
\begin{descr}


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


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


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


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


309 
base names only.


310 
\end{descr}

7134

311 


312 

7167

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

7134

314 


315 
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{setup}


316 
\begin{matharray}{rcl}


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


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


319 
\isarcmd{setup} & : & \isartrans{\cdot}{\cdot} \\


320 
\end{matharray}


321 


322 
\begin{rail}


323 
'use' name


324 
;


325 
'ML' text


326 
;


327 
'setup' text


328 
;


329 
\end{rail}


330 

7167

331 
\begin{descr}


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


333 
The current theory context as passed down to the ML session. Furthermore,


334 
the file name is checked with the dependency declarations given in the


335 
theory header (see also \S\ref{sec:beginthy}).


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


337 
The theory context is passed just as in $\isarkeyword{use}$.


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


339 
applying setup functions $text$ (which has to be an ML expression of type


340 
$(theory > theory)~list$. The $\isarkeyword{setup}$ is the usual way to


341 
initialize objectlogic specific tools and packages written in ML.


342 
\end{descr}

7134

343 


344 

7167

345 
\subsection{Syntax translation functions}

7134

346 

7167

347 
\indexisarcmd{parseasttranslation}\indexisarcmd{parsetranslation}


348 
\indexisarcmd{printtranslation}\indexisarcmd{typedprinttranslation}


349 
\indexisarcmd{printasttranslation}\indexisarcmd{tokentranslation}

7134

350 
\begin{matharray}{rcl}


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


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


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


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


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


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


357 
\end{matharray}


358 


359 
Syntax translation functions written in ML admit almost arbitrary


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


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


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


363 
transformations.


364 


365 


366 
\subsection{Oracles}


367 


368 
\indexisarcmd{oracle}


369 
\begin{matharray}{rcl}


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


371 
\end{matharray}


372 


373 
\begin{rail}


374 
'oracle' name '=' text comment?


375 
;


376 
\end{rail}


377 

7167

378 
\begin{descr}

7134

379 
\item [$\isarkeyword{oracle}~name=text$] FIXME

7167

380 
\end{descr}

7134

381 


382 


383 
\section{Proof commands}


384 

7167

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


386 
are three different kinds of operation:


387 
\begin{descr}


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


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


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


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


392 
augmented by \emph{stating} additional assumptions, intermediate result;


393 
\item [$proof(chain)$] indicates an intermediate mode between $proof(state)$


394 
and $proof(state)$: some already established facts have been just picked up


395 
in order to use them when refining the subsequent goal.


396 
\end{descr}

7134

397 

7167

398 


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


400 


401 
The following formal comments in proof mode closely correspond to the ones of


402 
theory mode (see \S\ref{sec:formalcmtthy} for more information).


403 


404 
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect}\indexisarcmd{txt}

7134

405 
\begin{matharray}{rcl}

7167

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


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


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


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

7134

410 
\end{matharray}


411 


412 
\begin{rail}

7167

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

7134

414 
;


415 
\end{rail}


416 


417 


418 
\subsection{Proof context}


419 

7167

420 
FIXME


421 

7134

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


423 
\begin{matharray}{rcl}


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


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


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


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


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


429 
\end{matharray}


430 


431 
\begin{rail}


432 
'fix' (var +) comment?


433 
;


434 
('assume'  'presume') thmdecl? (proppat +) comment?


435 
;


436 
'def' thmdecl? var '==' termpat comment?


437 
;


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


439 
;


440 


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


442 
;


443 
\end{rail}


444 

7167

445 
\begin{descr}


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


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


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


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


450 
\end{descr}


451 


452 


453 
\subsection{Facts and forward chaining}


454 


455 
FIXME


456 


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


458 
\begin{matharray}{rcl}


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


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


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


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


463 
\end{matharray}


464 


465 
\begin{rail}


466 
'note' thmdef? thmrefs comment?


467 
;


468 
'then' comment?


469 
;


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


471 
;


472 
\end{rail}


473 


474 
\begin{descr}


475 
\item [$\NOTE{a}{bs}$] recalls existing facts $bs$, binding the result as $a$


476 
(and $facts$). Note that attributes may be involved as well, both on the


477 
left and right hand side.


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


479 
establish the subsequent goal. The initial proof method invoked to solve


480 
that will be offered these facts to do anything ``appropriate'' (see also


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


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


483 
\item [$\FROM{bs}$] abbreviates $\NOTE{facts}{bs}~\THEN$; also note that


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


485 
\item [$\WITH{bs}$] abbreviates $\FROM{bs~facts}$; thus the forward chaining


486 
is from earlier facts together with the current ones.


487 
\end{descr}


488 


489 


490 
\subsection{Goal statements}


491 


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


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


494 
variants indicate whether the result is meant to solve some pending goal and


495 
whether forward chaining is employed.


496 


497 
\indexisarcmd{theorem}\indexisarcmd{lemma}


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


499 
\begin{matharray}{rcl}


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


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


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


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


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


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


506 
\end{matharray}


507 


508 
\begin{rail}


509 
('theorem'  'lemma') goal


510 
;


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


512 
;


513 


514 
goal: thmdecl? proppat comment?


515 
;


516 
\end{rail}


517 


518 
\begin{descr}


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


520 
eventually resulting in some theorem $\turn \phi$, which stored in the


521 
theory.


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


523 
``lemma''.


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


525 
theorem with the current assumption context as hypotheses.


526 
\item [$\SHOW{name}{\phi}$] same as $\HAVE{name}{\phi}$, but solves some


527 
pending goal with the result exported to the enclosing assumption context.


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


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


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


531 
\end{descr}


532 


533 


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


535 


536 
Arbitrary goal refinements via tactics is considered harmful. Consequently


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


538 
\begin{enumerate}


539 
\item An \emph{initial} refinement step (via $\PROOF{m@1}$) reduces a newly


540 
stated intermediate goal to a number of subgoals that are to be solved


541 
subsequently. Facts are passed to $m@1$ for forward chaining if so


542 
indicated by $proof(chain)$ mode.


543 


544 
\item A \emph{terminal} conclusion step (via $\QED{m@2}$)) solves any remaining


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


546 
\end{enumerate}


547 


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


549 
involves an explicit statement of what is solved.


550 


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


552 
or constitute some wellunderstood deterministic reduction to new subgoals.


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


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


555 
intelligible way. A much better technique is to $\SHOWNAME$ some nontrivial


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


557 
method, and then applied to some pending goal.


558 


559 
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}


560 
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}


561 
\begin{matharray}{rcl}


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


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


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


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


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


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


568 
\end{matharray}


569 


570 
\begin{rail}


571 
'proof' interest? meth? comment?


572 
;


573 
'qed' meth? comment?


574 
;


575 
'by' meth meth? comment?


576 
;


577 
('.'  '..'  'sorry') comment?


578 
;


579 


580 
meth: method interest?


581 
;


582 
\end{rail}


583 


584 
\begin{descr}


585 
\item [$\PROOF{m}$] refines the pending goal by proof method $m$ (facts for


586 
forward chaining are passed if indicated by $proof(chain)$).


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


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


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


590 
the enclosing goal context.


591 


592 
Thus $\QEDNAME$ may fail for two reasons: either $m$ fails to solve all


593 
remaining goals completely, or the resulting rule does not resolve with any


594 
enclosing goal. Debugging such a situation might involve temporarily


595 
changing $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by


596 
replacing $\ASSUMENAME$ by $\PRESUMENAME$.


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


598 
$\PROOF{m@1}~\QED{m@2}$, automatically backtracking across both methods.


599 


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


601 
expanding the abbreviation by hand; usually $\PROOF{m@1}$ is already


602 
sufficient to see what goes wrong.


603 
\item [$\isarkeyword{..}$] is a \emph{default proof}; it abbreviates


604 
$\BY{default}{finish}$, where method $default$ usually applies a single


605 
elimination or introduction rule according to the topmost symbol, and


606 
$finish$ solves all goals by assumption.


607 
\item [$\isarkeyword{.}$] is a \emph{trivial proof}, it abbreviates


608 
$\BY{}{finish}$, where method $$ does nothing except inserting any facts


609 
into the proof state.


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


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


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


613 
involving some oracle in its internal derivation object. Note that this is


614 
indicated as \texttt{[!]} in the printed result. The main application of


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


616 
\end{descr}

7134

617 


618 


619 
\subsection{Block structure}


620 

7167

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


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


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


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


625 
different context within a subproof are typically switched via


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


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


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


629 
goal focus involved!


630 


631 
There are explicit block parentheses as well. These typically achieve a


632 
strong forward style of reasoning.


633 

7134

634 
\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}


635 
\begin{matharray}{rcl}


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


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


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


639 
\end{matharray}


640 

7167

641 
\begin{descr}


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


643 
resetting the context to the initial one.


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


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


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


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


648 
discharged, and local definitions eliminated.


649 
\end{descr}

7134

650 


651 
\subsection{Calculational proof}


652 


653 
\indexisarcmd{also}\indexisarcmd{finally}


654 
\begin{matharray}{rcl}


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


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


657 
\end{matharray}


658 


659 
\begin{rail}


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


661 
;


662 


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


664 
;


665 
\end{rail}


666 

7167

667 
\begin{descr}

7134

668 
\item [$ $] FIXME

7167

669 
\end{descr}

7134

670 


671 


672 


673 
\subsection{Improper proof steps}


674 

7167

675 
The following commands emulate tactic scripts to some extent. While these are


676 
anathema for writing proper Isar proof documents, they might come in handy for


677 
exploring and debugging.


678 


679 
\indexisarcmd{apply}\indexisarcmd{thenapply}\indexisarcmd{back}

7134

680 
\begin{matharray}{rcl}


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


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


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


684 
\end{matharray}


685 


686 
\railalias{thenapply}{then\_apply}


687 
\railterm{thenapply}


688 


689 
\begin{rail}


690 
'apply' method


691 
;


692 
thenapply method


693 
;


694 
'back'


695 
;


696 
\end{rail}


697 

7167

698 
\begin{descr}

7134

699 
\item [$ $] FIXME

7167

700 
\end{descr}

7134

701 


702 


703 
\section{Other commands}


704 


705 
\subsection{Diagnostics}


706 


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


708 
\begin{matharray}{rcl}


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


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


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


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


713 
\end{matharray}


714 


715 
\begin{rail}


716 
'typ' type


717 
;


718 
'term' term


719 
;


720 
'prop' prop


721 
;


722 
'thm' thmrefs


723 
;


724 
\end{rail}


725 

7167

726 
\begin{descr}

7134

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


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


729 
according to the current theory or proof context.


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


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


732 
specifications are applied to a temporary proof context derived from the


733 
current theory or proof; the resulting context is discarded.

7167

734 
\end{descr}

7134

735 


736 


737 
\subsection{System operations}


738 

7167

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


740 
\indexisarcmd{updatethy}\indexisarcmd{updatethyonly}

7134

741 
\begin{matharray}{rcl}


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


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


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


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


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


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


748 
\end{matharray}


749 

7167

750 
\begin{descr}

7134

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


752 
process.


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


754 
\item [$\isarkeyword{use_thy}~name$, $\isarkeyword{use_thy_only}~name$,


755 
$\isarkeyword{update_thy}~name$, $\isarkeyword{update_thy_only}~name$] load


756 
theory files. These commands are exactly the same as the corresponding ML


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

7167

758 
\end{descr}

7134

759 


760 

7046

761 
%%% Local Variables:


762 
%%% mode: latex


763 
%%% TeXmaster: "isarref"


764 
%%% End:
