author  wenzelm 
Tue, 04 Apr 2000 12:31:48 +0200  
changeset 8664  aa383eeb3359 
parent 8632  14a69a0e8679 
child 8682  82ebf8618e6b 
permissions  rwrr 
7046  1 

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

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

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

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

7046  10 

7167  11 
\medskip 
12 

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

7466  14 
\emph{improper commands}. Some proof methods and attributes introduced later 
15 
are classified as improper as well. Improper Isar language elements, which 

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

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

19 
current context; other commands even emulate oldstyle tactical theorem 

8547  20 
proving. 
7167  21 

7134  22 

23 
\section{Theory commands} 

24 

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

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

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

7134  33 
\end{matharray} 
34 

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

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

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

7134  40 

7895  41 
The first actual command of any theory has to be $\THEORY$, starting a new 
42 
theory based on the merge of existing ones. Just preceding $\THEORY$, there 

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

44 
document preparation only; it acts very much like a special pretheory markup 

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

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

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

8547  48 
last command of any theory file. 
7134  49 

50 
\begin{rail} 

7895  51 
'header' text 
52 
; 

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

55 
'context' name 

56 
; 

57 
'end' 

58 
;; 

59 

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

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

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

69 

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

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

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

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

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

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

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

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

7134  79 

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

83 
loaded and uptodate. 

7175  84 

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

7167  88 
\end{descr} 
7134  89 

90 

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

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

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

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

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

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

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

7134  108 

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

7134  111 

112 
\begin{rail} 

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

116 

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

120 
and section headings. 

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

123 
Nevertheless, any source text of the form 

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

125 
for future use.} 

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

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

128 
becomes available. A typical application would be to emit 

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

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

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

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 
8547  175 
sort would be only changed when defining new objectlogics. 
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 

8547  248 
definitions of constants, using the canonical name $c_def$ for the 
249 
definitional 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 
8547  275 
the print mode that the grammar rules belong; unless the \texttt{output} 
276 
flag is given, all productions are added both to the input and output 

277 
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 
8547  309 
actual proven theorems. 
7335  310 
\item [$\isarkeyword{theorems}~a = \vec b$] stores lists of existing theorems. 
8547  311 
Typical applications would also involve attributes, to declare Simplifier 
312 
rules, 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, 
8547  327 
theorems etc.) by separate hierarchically structured name spaces. Normally 
328 
the user never has to control the behavior of name space entry by hand, yet 

329 
the 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 

8547  377 
canonical way to initialize any objectlogic specific tools and packages 
378 
written 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 
8547  442 
transitions are \emph{typed} according to the following three different modes 
443 
of operation: 

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

8547  446 
to be \emph{proven}; the next command may refine it by some proof method, 
447 
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} 
8547  535 
\item [$\FIX{\vec x}$] introduces local \emph{arbitrary, but fixed} variables 
536 
$\vec x$. 

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

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

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

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

7335  542 

543 
Several lists of assumptions may be given (separated by 

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

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

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

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

7167  552 
\end{descr} 
553 

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

7315  556 

7167  557 

558 
\subsection{Facts and forward chaining} 

559 

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

561 
\begin{matharray}{rcl} 

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

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

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

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

566 
\end{matharray} 

567 

7319  568 
New facts are established either by assumption or proof of local statements. 
7335  569 
Any fact will usually be involved in further proofs, either as explicit 
8547  570 
arguments of proof methods, or when forward chaining towards the next goal via 
7335  571 
$\THEN$ (and variants). Note that the special theorem name 
7987  572 
$this$\indexisarthm{this} refers to the most recently established facts. 
7167  573 
\begin{rail} 
574 
'note' thmdef? thmrefs comment? 

575 
; 

576 
'then' comment? 

577 
; 

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

579 
; 

580 
\end{rail} 

581 

582 
\begin{descr} 

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

585 
right hand sides. 

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

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

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

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

7167  598 
\end{descr} 
599 

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

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

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

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

7389  607 

7167  608 

609 
\subsection{Goal statements} 

610 

611 
\indexisarcmd{theorem}\indexisarcmd{lemma} 

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

613 
\begin{matharray}{rcl} 

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

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

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

7167  618 
\isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\ 
619 
\isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\ 

620 
\end{matharray} 

621 

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

8547  625 
some pending goal or whether forward chaining is indicated. 
7175  626 

7167  627 
\begin{rail} 
628 
('theorem'  'lemma') goal 

629 
; 

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

631 
; 

632 

8632  633 
goal: thmdecl? prop proppat? comment? 
7167  634 
; 
635 
\end{rail} 

636 

637 
\begin{descr} 

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

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

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

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

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

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

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

7167  653 
\end{descr} 
654 

655 

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

657 

7175  658 
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by} 
659 
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry} 

660 
\begin{matharray}{rcl} 

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

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

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

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

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

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

667 
\end{matharray} 

668 

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

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

7167  678 
\end{enumerate} 
679 

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

7167  682 

7175  683 
\medskip 
684 

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

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

7987  689 
way. 
7167  690 

7175  691 
\medskip 
692 

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

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

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

7167  697 

698 
\begin{rail} 

699 
'proof' interest? meth? comment? 

700 
; 

701 
'qed' meth? comment? 

702 
; 

703 
'by' meth meth? comment? 

704 
; 

705 
('.'  '..'  'sorry') comment? 

706 
; 

707 

708 
meth: method interest? 

709 
; 

710 
\end{rail} 

711 

712 
\begin{descr} 

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

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

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

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

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

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

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

722 
context. Debugging such a situation might involve temporarily changing 

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

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

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

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

7895  728 
by expanding its definition; in many cases $\PROOF{m@1}$ is already 
7175  729 
sufficient to see what is going wrong. 
7895  730 
\item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it 
8515  731 
abbreviates $\BY{rule}$. 
7895  732 
\item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it 
8195  733 
abbreviates $\BY{this}$. 
8379  734 
\item [$\SORRY$] is a \emph{fake proof}\index{proof!fake}; provided that the 
735 
\texttt{quick_and_dirty} flag is enabled, $\SORRY$ pretends to solve the 

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

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

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

740 
\end{descr} 

741 

742 

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

744 

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

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

748 
\ref{ch:holtools}). 

8515  749 

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

751 
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} 

752 
\indexisaratt{OF}\indexisaratt{of} 

753 
\begin{matharray}{rcl} 

754 
assumption & : & \isarmeth \\ 

755 
this & : & \isarmeth \\ 

756 
rule & : & \isarmeth \\ 

757 
 & : & \isarmeth \\ 

758 
OF & : & \isaratt \\ 

759 
of & : & \isaratt \\ 

760 
intro & : & \isaratt \\ 

761 
elim & : & \isaratt \\ 

762 
dest & : & \isaratt \\ 

763 
delrule & : & \isaratt \\ 

764 
\end{matharray} 

765 

766 
\begin{rail} 

8547  767 
'rule' thmrefs? 
8515  768 
; 
769 
'OF' thmrefs 

770 
; 

771 
'of' (inst * ) ('concl' ':' (inst * ))? 

772 
; 

773 

774 
inst: underscore  term 

775 
; 

776 
\end{rail} 

777 

778 
\begin{descr} 

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

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

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

782 
remaining subgoals by assumption. 

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

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

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

788 
becomes \emph{elimination}. 

789 

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

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

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

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

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

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

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

799 
alone. 

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

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

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

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

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

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

808 
conclusion of a rule. 

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

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

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

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

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

814 
confusion! 

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

7315  816 
\end{descr} 
817 

818 

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

820 

821 
\indexisarcmd{let} 

822 
\begin{matharray}{rcl} 

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

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

825 
\end{matharray} 

826 

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

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

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

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

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

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

834 
postfix position. 

7315  835 

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

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

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

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

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

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

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

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

843 

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

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

845 

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

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

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

850 
does not support polymorphism. 
7315  851 

852 
\begin{rail} 

8664  853 
'let' ((term + 'and') '=' term comment? + 'and') 
7315  854 
; 
855 
\end{rail} 

856 

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

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

859 

860 
\begin{descr} 

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

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

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

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

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

866 
\end{descr} 

867 

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

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

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

8547  873 
objectlevel statement. The latter two abstract over any metalevel 
7987  874 
parameters. 
7315  875 

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

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

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

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

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

885 

7134  886 
\subsection{Block structure} 
887 

7397  888 
\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}} 
889 
\begin{matharray}{rcl} 

8448  890 
\NEXT & : & \isartrans{proof(state)}{proof(state)} \\ 
7974  891 
\BG & : & \isartrans{proof(state)}{proof(state)} \\ 
892 
\EN & : & \isartrans{proof(state)}{proof(state)} \\ 

7397  893 
\end{matharray} 
894 

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

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

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

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

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

902 
here! 

7167  903 

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

907 
\begin{descr} 

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

7167  910 
\item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and 
7895  911 
close blocks. Any current facts pass through ``$\isarkeyword{\{\{}$'' 
912 
unchanged, while ``$\isarkeyword{\}\}}$'' causes any result to be 

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

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

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

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

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

7167  918 
\end{descr} 
7134  919 

920 

8533  921 
\subsection{Emulating tactic scripts}\label{sec:tacticalproof} 
8515  922 

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

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

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

926 
tactical proof within newstyle theories (to benefit from document 

927 
preparation, for example). 

928 

929 
\indexisarcmd{apply}\indexisarcmd{applyend} 

930 
\indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back} 

931 
\indexisarmeth{tactic} 

8533  932 
\indexisarmeth{resinsttac}\indexisarmeth{eresinsttac} 
933 
\indexisarmeth{dresinsttac}\indexisarmeth{forwinsttac} 

934 
\indexisarmeth{subgoaltac} 

8515  935 
\begin{matharray}{rcl} 
8533  936 
\isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\ 
937 
\isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\ 

938 
\isarcmd{defer}^* & : & \isartrans{proof}{proof} \\ 

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

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

941 
tactic^* & : & \isarmeth \\ 

942 
res_inst_tac^* & : & \isarmeth \\ 

943 
eres_inst_tac^* & : & \isarmeth \\ 

944 
dres_inst_tac^* & : & \isarmeth \\ 

945 
forw_inst_tac^* & : & \isarmeth \\ 

946 
subgoal_tac^* & : & \isarmeth \\ 

8515  947 
\end{matharray} 
948 

949 
\railalias{applyend}{apply\_end} 

950 
\railterm{applyend} 

951 

8533  952 
\railalias{resinsttac}{res\_inst\_tac} 
953 
\railterm{resinsttac} 

954 

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

956 
\railterm{eresinsttac} 

957 

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

959 
\railterm{dresinsttac} 

960 

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

962 
\railterm{forwinsttac} 

963 

964 
\railalias{subgoaltac}{subgoal\_tac} 

965 
\railterm{subgoaltac} 

966 

8515  967 
\begin{rail} 
968 
'apply' method 

969 
; 

970 
applyend method 

971 
; 

972 
'defer' nat? 

973 
; 

974 
'prefer' nat 

975 
; 

976 
'tactic' text 

977 
; 

8533  978 
( resinsttac  eresinsttac  dresinsttac  forwinsttac ) goalspec? ((name '=' term) + 'and') 
979 
; 

980 
subgoaltac goalspec? prop 

981 
; 

8515  982 
\end{rail} 
983 

984 
\begin{descr} 

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

8515  987 
consecutive method applications may be given just as in tactic scripts. In 
988 
order to complete the proof properly, any of the actual structured proof 

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

990 

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

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

993 
though. 

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

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

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

997 

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

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

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

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

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

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

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

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

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

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

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

8547  1009 
\texttt{tactic}. Apart from the usual ML environment and the current 
8515  1010 
implicit theory context, the ML code may refer to the following locally 
1011 
bound values: 

1012 
%%FIXME ttbox produces too much trailing space (why?) 

1013 
{\footnotesize\begin{verbatim} 

1014 
val ctxt : Proof.context 

1015 
val facts : thm list 

1016 
val thm : string > thm 

1017 
val thms : string > thm list 

1018 
\end{verbatim}} 

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

1020 
indicates any current facts for forwardchaining, and 

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

1022 
theorems) from the context. 

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

1025 
\cite[\S3]{isabelleref}. 

1026 

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

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

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

1030 
abbreviations may not be included in the term specifications. 

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

1034 

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

1036 
as $subgoal_tac$. 

8515  1037 
\end{descr} 
1038 

1039 

1040 
\subsection{Metalinguistic features} 

1041 

1042 
\indexisarcmd{oops} 

1043 
\begin{matharray}{rcl} 

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

1045 
\end{matharray} 

1046 

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

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

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

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

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

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

1053 
proof anyhow. 

1054 

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

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

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

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

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

1060 
``$\OOPS$'' keyword. 

1061 

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

1064 
the opening of the proof. 

8515  1065 

1066 

7134  1067 
\section{Other commands} 
1068 

8448  1069 
\subsection{Diagnostics}\label{sec:diag} 
7134  1070 

8485  1071 
\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ} 
1072 
\indexisarcmd{printfacts}\indexisarcmd{printbinds} 

7134  1073 
\begin{matharray}{rcl} 
8515  1074 
\isarcmd{help}^* & : & \isarkeep{\cdot} \\ 
1075 
\isarcmd{pr}^* & : & \isarkeep{\cdot} \\ 

1076 
\isarcmd{thm}^* & : & \isarkeep{theory~~proof} \\ 

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

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

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

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

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

7134  1082 
\end{matharray} 
1083 

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

1086 
theory or proof configuration is not changed. 

1087 

7134  1088 
\begin{rail} 
8485  1089 
'pr' modes? nat? 
7134  1090 
; 
8485  1091 
'thm' modes? thmrefs 
1092 
; 

1093 
'term' modes? term 

7134  1094 
; 
8485  1095 
'prop' modes? prop 
7134  1096 
; 
8485  1097 
'typ' modes? type 
1098 
; 

1099 

1100 
modes: '(' (name + ) ')' 

7134  1101 
; 
1102 
\end{rail} 

1103 

7167  1104 
\begin{descr} 
8515  1105 
\item [$\isarkeyword{help}$] prints a list of available language elements. 
1106 
Note that methods and attributes depend on the current theory context. 

8485  1107 
\item [$\isarkeyword{pr}~n$] prints the current toplevel state, i.e.\ the 
1108 
theory identifier or proof state. The latter includes the proof context, 

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

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

1111 
leaves the value unchanged. 

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

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

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

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

1121 
abbreviations. 

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

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

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

1127 
the context. 

8485  1128 
\end{descr} 
1129 

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

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

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

1133 
features. 

1134 

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

1136 
current proof state with mathematical symbols and special characters 

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

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

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

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

1142 
some particular user interface configuration such as Proof~General 

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

1145 

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

1147 

1148 
\indexisarcmd{undo}\indexisarcmd{redo}\indexisarcmd{kill} 

1149 
\begin{matharray}{rcl} 

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

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

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

1153 
\end{matharray} 

1154 

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

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

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

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

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

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

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

1162 
undoable. 

1163 

1164 
\begin{warn} 

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

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

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

8485  1170 
\end{warn} 
1171 

8515  1172 
%FIXME remove 
1173 
% \begin{descr} 

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

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

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

1177 
% \end{descr} 

8485  1178 

8379  1179 

7134  1180 
\subsection{System operations} 
1181 

7167  1182 
\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{usethy}\indexisarcmd{usethyonly} 
1183 
\indexisarcmd{updatethy}\indexisarcmd{updatethyonly} 

7134  1184 
\begin{matharray}{rcl} 
8515  1185 
\isarcmd{cd}^* & : & \isarkeep{\cdot} \\ 
1186 
\isarcmd{pwd}^* & : & \isarkeep{\cdot} \\ 

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

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

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

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

7134  1191 
\end{matharray} 
1192 

7167  1193 
\begin{descr} 
7134  1194 
\item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle 
1195 
process. 

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

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

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

1203 
load new and oldstyle theories alike. 

7167  1204 
\end{descr} 
7134  1205 

7987  1206 
These system commands are scarcely used when working with the Proof~General 
1207 
interface, since loading of theories is done fully transparently. 

7134  1208 

8379  1209 

7046  1210 
%%% Local Variables: 
1211 
%%% mode: latex 

1212 
%%% TeXmaster: "isarref" 

1213 
%%% End: 