author  nipkow 
Wed, 04 Aug 2004 11:25:08 +0200  
changeset 15106  e8cef6993701 
parent 14955  08ee855c1d94 
child 15686  406a98ee8027 
permissions  rwrr 
7046  1 

13048  2 
\chapter{Basic language elements}\label{ch:puresyntax} 
7167  3 

13039  4 
Subsequently, we introduce the main part of Pure theory and proof commands, 
5 
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 

12879  8 
Isabelle or preinstalled in most object logics. Chapter~\ref{ch:logics} 
12621  9 
refers to objectlogic specific elements (mainly for HOL and ZF). 
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 

12618  16 
are subsequently marked by ``$^*$'', are often helpful when developing proof 
13039  17 
documents, while their use is discouraged for the final humanreadable 
18 
outcome. Typical examples are diagnostic commands that print terms or 

19 
theorems according to the current context; other commands emulate oldstyle 

20 
tactical theorem proving. 

7167  21 

7134  22 

12621  23 
\section{Theory commands} 
7134  24 

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

12621  27 
\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{context}\indexisarcmd{end} 
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 

12621  41 
The first ``real'' command of any theory has to be $\THEORY$, which starts a 
42 
new theory based on the merge of existing ones. Just preceding $\THEORY$, 

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

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

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

13039  46 
$\END$ command concludes a theory development; it has to be the very last 
47 
command of any theory file loaded in batchmode. The theory context may be 

12621  48 
also changed interactively by $\CONTEXT$ without creating a new theory. 
7134  49 

50 
\begin{rail} 

7895  51 
'header' text 
52 
; 

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

55 
'context' name 

56 
; 

57 

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

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

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

67 

12621  68 
\item [$\THEORY~A = B@1 + \cdots + B@n\colon$] starts a new theory $A$ based 
69 
on the merge of existing theories $B@1, \dots, B@n$. 

70 

71 
Due to inclusion of several ancestors, the overall theory structure emerging 

72 
in an Isabelle session forms a directed acyclic graph (DAG). Isabelle's 

73 
theory loader ensures that the sources contributing to the development graph 

74 
are always uptodate. Changed files are automatically reloaded when 

75 
processing theory headers interactively; batchmode explicitly distinguishes 

76 
\verb,update_thy, from \verb,use_thy,, see also \cite{isabelleref}. 

77 

78 
The optional $\isarkeyword{files}$ specification declares additional 

79 
dependencies on ML files. Files will be loaded immediately, unless the name 

80 
is put in parentheses, which merely documents the dependency to be resolved 

81 
later in the text (typically via explicit $\isarcmd{use}$ in the body text, 

82 
see \S\ref{sec:ML}). In reminiscence of the oldstyle theory system of 

83 
Isabelle, \texttt{$A$.thy} may be also accompanied by an additional file 

84 
\texttt{$A$.ML} consisting of ML code that is executed in the context of the 

85 
\emph{finished} theory $A$. That file should not be included in the 

86 
$\isarkeyword{files}$ dependency declaration, though. 

7134  87 

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

91 
loaded and uptodate. 

7175  92 

12621  93 
This command is occasionally useful for quick interactive experiments; 
94 
normally one should always commence a new context via $\THEORY$. 

95 

7167  96 
\item [$\END$] concludes the current theory definition or context switch. 
12621  97 
Note that this command cannot be undone, but the whole theory definition has 
98 
to be retracted. 

99 

7167  100 
\end{descr} 
7134  101 

102 

12621  103 
\subsection{Markup commands}\label{sec:markupthy} 
7134  104 

7895  105 
\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection} 
106 
\indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{textraw} 

7134  107 
\begin{matharray}{rcl} 
108 
\isarcmd{chapter} & : & \isartrans{theory}{theory} \\ 

7167  109 
\isarcmd{section} & : & \isartrans{theory}{theory} \\ 
7134  110 
\isarcmd{subsection} & : & \isartrans{theory}{theory} \\ 
111 
\isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\ 

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

7895  113 
\isarcmd{text_raw} & : & \isartrans{theory}{theory} \\ 
7134  114 
\end{matharray} 
115 

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

7134  120 

7895  121 
\railalias{textraw}{text\_raw} 
122 
\railterm{textraw} 

7134  123 

124 
\begin{rail} 

7895  125 
('chapter'  'section'  'subsection'  'subsubsection'  'text'  textraw) text 
7134  126 
; 
127 
\end{rail} 

128 

7167  129 
\begin{descr} 
7335  130 
\item [$\isarkeyword{chapter}$, $\isarkeyword{section}$, 
131 
$\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter 

132 
and section headings. 

7895  133 
\item [$\TEXT$] specifies paragraphs of plain text, including references to 
12618  134 
formal entities (see also \S\ref{sec:antiq} on ``antiquotations''). 
7895  135 
\item [$\isarkeyword{text_raw}$] inserts {\LaTeX} source into the output, 
136 
without additional markup. Thus the full range of document manipulations 

12618  137 
becomes available. 
7167  138 
\end{descr} 
7134  139 

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

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

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

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

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

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

7895  147 

8485  148 
\medskip 
149 

150 
Additional markup commands are available for proofs (see 

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

7895  154 

7134  155 

7135  156 
\subsection{Type classes and sorts}\label{sec:classes} 
7134  157 

158 
\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort} 

12621  159 
\begin{matharray}{rcll} 
7134  160 
\isarcmd{classes} & : & \isartrans{theory}{theory} \\ 
12621  161 
\isarcmd{classrel} & : & \isartrans{theory}{theory} & (axiomatic!) \\ 
7134  162 
\isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\ 
163 
\end{matharray} 

164 

165 
\begin{rail} 

12879  166 
'classes' (classdecl +) 
7134  167 
; 
14817  168 
'classrel' (nameref ('<'  subseteq) nameref + 'and') 
7134  169 
; 
12879  170 
'defaultsort' sort 
7134  171 
; 
172 
\end{rail} 

173 

7167  174 
\begin{descr} 
11100
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11017
diff
changeset

175 
\item [$\isarkeyword{classes}~c \subseteq \vec c$] declares class $c$ to be a 
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11017
diff
changeset

176 
subclass of existing classes $\vec c$. Cyclic class structures are ruled 
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11017
diff
changeset

177 
out. 
14817  178 
\item [$\isarkeyword{classrel}~c@1 \subseteq c@2$] states subclass relations 
11100
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11017
diff
changeset

179 
between existing classes $c@1$ and $c@2$. This is done axiomatically! The 
10223  180 
$\INSTANCE$ command (see \S\ref{sec:axclass}) provides a way to introduce 
181 
proven class relations. 

7134  182 
\item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for 
7895  183 
any type variables given without sort constraints. Usually, the default 
12621  184 
sort would be only changed when defining a new objectlogic. 
7167  185 
\end{descr} 
7134  186 

187 

7315  188 
\subsection{Primitive types and type abbreviations}\label{sec:typespure} 
7134  189 

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

12621  191 
\begin{matharray}{rcll} 
7134  192 
\isarcmd{types} & : & \isartrans{theory}{theory} \\ 
193 
\isarcmd{typedecl} & : & \isartrans{theory}{theory} \\ 

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

12621  195 
\isarcmd{arities} & : & \isartrans{theory}{theory} & (axiomatic!) \\ 
7134  196 
\end{matharray} 
197 

198 
\begin{rail} 

12879  199 
'types' (typespec '=' type infix? +) 
7134  200 
; 
12879  201 
'typedecl' typespec infix? 
7134  202 
; 
12879  203 
'nonterminals' (name +) 
7134  204 
; 
12879  205 
'arities' (nameref '::' arity +) 
7134  206 
; 
207 
\end{rail} 

208 

7167  209 
\begin{descr} 
13039  210 

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

7895  214 
syntactic abbreviations without any logical significance. Internally, type 
7981  215 
synonyms are fully expanded. 
13039  216 

7134  217 
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor 
13039  218 
$t$, intended as an actual logical type. Note that the Isabelle/HOL 
219 
objectlogic overrides $\isarkeyword{typedecl}$ by its own version 

220 
(\S\ref{sec:holtypedef}). 

221 

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

224 
Isabelle's inner syntax of terms or types. 

13039  225 

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

10223  228 
axiomatically! The $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a 
229 
way to introduce proven type arities. 

13039  230 

7167  231 
\end{descr} 
7134  232 

233 

7981  234 
\subsection{Constants and simple definitions}\label{sec:consts} 
7134  235 

7175  236 
\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl} 
7134  237 
\begin{matharray}{rcl} 
238 
\isarcmd{consts} & : & \isartrans{theory}{theory} \\ 

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

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

241 
\end{matharray} 

242 

243 
\begin{rail} 

14642  244 
'consts' ((name '::' type mixfix?) +) 
245 
; 

246 
'defs' ('(' 'overloaded' ')')? (axmdecl prop +) 

7134  247 
; 
14642  248 
\end{rail} 
249 

250 
\begin{rail} 

251 
'constdefs' structs? (constdecl? constdef +) 

7134  252 
; 
253 

14642  254 
structs: '(' 'structure' (vars + 'and') ')' 
255 
; 

256 
constdecl: (name '::' type) mixfix  (name '::' type)  name 'where'  mixfix 

257 
; 

258 
constdef: thmdecl? prop 

7134  259 
; 
260 
\end{rail} 

261 

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

7895  265 
to the constants declared. 
9308  266 

7335  267 
\item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for some 
268 
existing constant. See \cite[\S6]{isabelleref} for more details on the 

269 
form of equations admitted as constant definitions. 

9308  270 

14642  271 
The $(overloaded)$ option declares definitions to be potentially overloaded. 
9308  272 
Unless this option is given, a warning message would be issued for any 
273 
definitional equation with a more special type than that of the 

274 
corresponding constant declaration. 

12621  275 

14642  276 
\item [$\CONSTDEFS$] provides a streamlined combination of constants 
277 
declarations and definitions: typeinference takes care of the most general 

278 
typing of the given specification (the optional type constraint may refer to 

279 
typeinference dummies ``$_$'' as usual). The resulting type declaration 

280 
needs to agree with that of the specification; overloading is \emph{not} 

281 
supported here! 

282 

283 
The constant name may be omitted altogether, if neither type nor syntax 

284 
declarations are given. The canonical name of the definitional axiom for 

285 
constant $c$ will be $c_def$, unless specified otherwise. Also note that 

286 
the given list of specifications is processed in a strictly sequential 

287 
manner, with typechecking being performed independently. 

288 

289 
An optional initial context of $(structure)$ declarations admits use of 

290 
indexed syntax, using the special symbol \verb,\<index>, (printed as 

291 
``\i''). The latter concept is particularly useful with locales (see also 

292 
\S\ref{sec:locale}). 

7167  293 
\end{descr} 
7134  294 

295 

7981  296 
\subsection{Syntax and translations}\label{sec:syntrans} 
7134  297 

298 
\indexisarcmd{syntax}\indexisarcmd{translations} 

299 
\begin{matharray}{rcl} 

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

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

302 
\end{matharray} 

303 

10640  304 
\railalias{rightleftharpoons}{\isasymrightleftharpoons} 
305 
\railterm{rightleftharpoons} 

306 

307 
\railalias{rightharpoonup}{\isasymrightharpoonup} 

308 
\railterm{rightharpoonup} 

309 

310 
\railalias{leftharpoondown}{\isasymleftharpoondown} 

311 
\railterm{leftharpoondown} 

312 

7134  313 
\begin{rail} 
9727  314 
'syntax' ('(' ( name  'output'  name 'output' ) ')')? (constdecl +) 
7134  315 
; 
12879  316 
'translations' (transpat ('=='  '=>'  '<='  rightleftharpoons  rightharpoonup  leftharpoondown) transpat +) 
7134  317 
; 
318 
transpat: ('(' nameref ')')? string 

319 
; 

320 
\end{rail} 

321 

7167  322 
\begin{descr} 
13024  323 

7175  324 
\item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$, 
325 
except that the actual logical signature extension is omitted. Thus the 

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

7335  327 
arbitrary ways, independently of the logic. The $mode$ argument refers to 
13024  328 
the print mode that the grammar rules belong; unless the 
329 
$\isarkeyword{output}$ indicator is given, all productions are added both to 

330 
the input and output grammar. 

331 

7175  332 
\item [$\isarkeyword{translations}~rules$] specifies syntactic translation 
13024  333 
rules (i.e.\ macros): parse~/ print rules (\isasymrightleftharpoons), parse 
334 
rules (\isasymrightharpoonup), or print rules (\isasymleftharpoondown). 

335 
Translation patterns may be prefixed by the syntactic category to be used 

336 
for parsing; the default is $logic$. 

7167  337 
\end{descr} 
7134  338 

339 

9605  340 
\subsection{Axioms and theorems}\label{sec:axmsthms} 
7134  341 

12618  342 
\indexisarcmd{axioms}\indexisarcmd{lemmas}\indexisarcmd{theorems} 
12621  343 
\begin{matharray}{rcll} 
344 
\isarcmd{axioms} & : & \isartrans{theory}{theory} & (axiomatic!) \\ 

12618  345 
\isarcmd{lemmas} & : & \isartrans{theory}{theory} \\ 
7134  346 
\isarcmd{theorems} & : & \isartrans{theory}{theory} \\ 
347 
\end{matharray} 

348 

349 
\begin{rail} 

12879  350 
'axioms' (axmdecl prop +) 
7134  351 
; 
12976  352 
('lemmas'  'theorems') locale? (thmdef? thmrefs + 'and') 
7134  353 
; 
354 
\end{rail} 

355 

7167  356 
\begin{descr} 
12976  357 

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

7134  361 

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

7175  363 
Everyday work is typically done the hard way, with proper definitions and 
13039  364 
proven theorems. 
12976  365 

13024  366 
\item [$\isarkeyword{lemmas}~a = \vec b$] retrieves and stores existing facts 
12976  367 
in the theory context, or the specified locale (see also 
368 
\S\ref{sec:locale}). Typical applications would also involve attributes, to 

369 
declare Simplifier rules, for example. 

370 

12618  371 
\item [$\isarkeyword{theorems}$] is essentially the same as 
372 
$\isarkeyword{lemmas}$, but marks the result as a different kind of facts. 

12976  373 

7167  374 
\end{descr} 
7134  375 

376 

7167  377 
\subsection{Name spaces} 
7134  378 

8726  379 
\indexisarcmd{global}\indexisarcmd{local}\indexisarcmd{hide} 
7134  380 
\begin{matharray}{rcl} 
381 
\isarcmd{global} & : & \isartrans{theory}{theory} \\ 

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

8726  383 
\isarcmd{hide} & : & \isartrans{theory}{theory} \\ 
7134  384 
\end{matharray} 
385 

8726  386 
\begin{rail} 
12879  387 
'hide' name (nameref + ) 
8726  388 
; 
389 
\end{rail} 

390 

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

7175  395 

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

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

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

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

8726  402 

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

404 
qualified names of the same base name are introduced. 

405 

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

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

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

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

12621  410 
full internal name. Unqualified (global) names may not be hidden. 
7167  411 
\end{descr} 
7134  412 

413 

7167  414 
\subsection{Incorporating ML code}\label{sec:ML} 
7134  415 

8682  416 
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{MLcommand} 
417 
\indexisarcmd{MLsetup}\indexisarcmd{setup} 

9199  418 
\indexisarcmd{methodsetup} 
7134  419 
\begin{matharray}{rcl} 
420 
\isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\ 

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

8682  422 
\isarcmd{ML_command} & : & \isartrans{\cdot}{\cdot} \\ 
7895  423 
\isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\ 
7175  424 
\isarcmd{setup} & : & \isartrans{theory}{theory} \\ 
9199  425 
\isarcmd{method_setup} & : & \isartrans{theory}{theory} \\ 
7134  426 
\end{matharray} 
427 

7895  428 
\railalias{MLsetup}{ML\_setup} 
429 
\railterm{MLsetup} 

430 

9199  431 
\railalias{methodsetup}{method\_setup} 
432 
\railterm{methodsetup} 

433 

8682  434 
\railalias{MLcommand}{ML\_command} 
435 
\railterm{MLcommand} 

436 

7134  437 
\begin{rail} 
12879  438 
'use' name 
7134  439 
; 
12879  440 
('ML'  MLcommand  MLsetup  'setup') text 
7134  441 
; 
12879  442 
methodsetup name '=' text text 
9199  443 
; 
7134  444 
\end{rail} 
445 

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

452 

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

10858  455 
$\isarkeyword{use}$, but may not be changed. Note that the output of 
8682  456 
$\isarkeyword{ML_command}$ is less verbose than plain $\isarkeyword{ML}$. 
7895  457 

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

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

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

461 

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

8547  465 
canonical way to initialize any objectlogic specific tools and packages 
466 
written in ML. 

9199  467 

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

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

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

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

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

473 
arguments, or a list of theorems, respectively. 

474 

475 
{\footnotesize 

476 
\begin{verbatim} 

9605  477 
Method.no_args (Method.METHOD (fn facts => foobar_tac)) 
478 
Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac)) 

10899  479 
Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac)) 
12618  480 
Method.thms_ctxt_args (fn thms => fn ctxt => 
481 
Method.METHOD (fn facts => foobar_tac)) 

9199  482 
\end{verbatim} 
483 
} 

484 

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

13039  486 
above. Proper proof methods would do something appropriate with the list of 
487 
current facts, though. Singlerule methods usually do strict forwardchaining 

488 
(e.g.\ by using \texttt{Method.multi_resolves}), while automatic ones just 

489 
insert the facts using \texttt{Method.insert_tac} before applying the main 

490 
tactic. 

7167  491 
\end{descr} 
7134  492 

493 

8250  494 
\subsection{Syntax translation functions} 
7134  495 

8250  496 
\indexisarcmd{parseasttranslation}\indexisarcmd{parsetranslation} 
497 
\indexisarcmd{printtranslation}\indexisarcmd{typedprinttranslation} 

498 
\indexisarcmd{printasttranslation}\indexisarcmd{tokentranslation} 

499 
\begin{matharray}{rcl} 

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

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

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

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

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

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

506 
\end{matharray} 

7134  507 

9273  508 
\railalias{parseasttranslation}{parse\_ast\_translation} 
509 
\railterm{parseasttranslation} 

510 

511 
\railalias{parsetranslation}{parse\_translation} 

512 
\railterm{parsetranslation} 

513 

514 
\railalias{printtranslation}{print\_translation} 

515 
\railterm{printtranslation} 

516 

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

518 
\railterm{typedprinttranslation} 

519 

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

521 
\railterm{printasttranslation} 

522 

523 
\railalias{tokentranslation}{token\_translation} 

524 
\railterm{tokentranslation} 

525 

526 
\begin{rail} 

527 
( parseasttranslation  parsetranslation  printtranslation  typedprinttranslation  

14642  528 
printasttranslation ) ('(' 'advanced' ')')? text; 
529 

530 
tokentranslation text 

9273  531 
\end{rail} 
532 

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

13048  535 
single \railqtok{text} argument that refers to an ML expression of appropriate 
14642  536 
type, which are as follows by default: 
8379  537 

538 
\begin{ttbox} 

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

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

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

542 
val typed_print_translation : 

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

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

545 
val token_translation : 

546 
(string * string * (string > string * real)) list 

547 
\end{ttbox} 

14642  548 

549 
In case that the $(advanced)$ option is given, the corresponding translation 

550 
functions may depend on the signature of the current theory context. This 

551 
allows to implement advanced syntax mechanisms, as translations functions may 

552 
refer to specific theory declarations and auxiliary data. 

553 

554 
See also \cite[\S8]{isabelleref} for more information on the general concept 

555 
of syntax transformations in Isabelle. 

556 

557 
\begin{ttbox} 

558 
val parse_ast_translation: 

559 
(string * (Sign.sg > ast list > ast)) list 

560 
val parse_translation: 

561 
(string * (Sign.sg > term list > term)) list 

562 
val print_translation: 

563 
(string * (Sign.sg > term list > term)) list 

564 
val typed_print_translation: 

565 
(string * (Sign.sg > bool > typ > term list > term)) list 

566 
val print_ast_translation: 

567 
(string * (Sign.sg > ast list > ast)) list 

568 
\end{ttbox} 

7134  569 

570 

571 
\subsection{Oracles} 

572 

573 
\indexisarcmd{oracle} 

574 
\begin{matharray}{rcl} 

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

576 
\end{matharray} 

577 

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

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

581 

7134  582 
\begin{rail} 
12879  583 
'oracle' name '=' text 
7134  584 
; 
585 
\end{rail} 

586 

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

7167  591 
\end{descr} 
7134  592 

593 

594 
\section{Proof commands} 

595 

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

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

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

10858  605 
\item [$proof(state)$] is like a nested theory mode: the context may be 
7987  606 
augmented by \emph{stating} additional assumptions, intermediate results 
607 
etc. 

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

611 
goal claimed next. 

7167  612 
\end{descr} 
7134  613 

12621  614 
The proof mode indicator may be read as a verb telling the writer what kind of 
615 
operation may be performed next. The corresponding typings of proof commands 

616 
restricts the shape of wellformed proof texts to particular command 

617 
sequences. So dynamic arrangements of commands eventually turn out as static 

13039  618 
texts of a certain structure. Appendix~\ref{ap:refcard} gives a simplified 
619 
grammar of the overall (extensible) language emerging that way. 

7167  620 

12621  621 

622 
\subsection{Markup commands}\label{sec:markupprf} 

7167  623 

7987  624 
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect} 
7895  625 
\indexisarcmd{txt}\indexisarcmd{txtraw} 
7134  626 
\begin{matharray}{rcl} 
8101  627 
\isarcmd{sect} & : & \isartrans{proof}{proof} \\ 
628 
\isarcmd{subsect} & : & \isartrans{proof}{proof} \\ 

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

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

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

7134  632 
\end{matharray} 
633 

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

637 
\railalias{txtraw}{txt\_raw} 

638 
\railterm{txtraw} 

7175  639 

7134  640 
\begin{rail} 
7895  641 
('sect'  'subsect'  'subsubsect'  'txt'  txtraw) text 
7134  642 
; 
643 
\end{rail} 

644 

645 

12621  646 
\subsection{Context elements}\label{sec:proofcontext} 
7134  647 

7315  648 
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def} 
7134  649 
\begin{matharray}{rcl} 
650 
\isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\ 

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

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

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

654 
\end{matharray} 

655 

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

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

13039  659 
Introducing some \emph{arbitrary, but fixed} variable via ``$\FIX x$'' results 
660 
in a local value that may be used in the subsequent proof as any other 

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

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

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

7315  664 

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

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

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

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

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

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

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

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

674 
user. 

7315  675 

13039  676 
Local definitions, introduced by ``$\DEF{}{x \equiv t}$'', are achieved by 
677 
combining ``$\FIX x$'' with another version of assumption that causes any 

7987  678 
hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule. 
679 
Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$. 

7175  680 

10686  681 
\railalias{equiv}{\isasymequiv} 
682 
\railterm{equiv} 

683 

7134  684 
\begin{rail} 
12879  685 
'fix' (vars + 'and') 
7134  686 
; 
12879  687 
('assume'  'presume') (props + 'and') 
7134  688 
; 
12879  689 
'def' thmdecl? \\ name ('=='  equiv) term termpat? 
7134  690 
; 
691 
\end{rail} 

692 

7167  693 
\begin{descr} 
13039  694 

8547  695 
\item [$\FIX{\vec x}$] introduces local \emph{arbitrary, but fixed} variables 
696 
$\vec x$. 

13039  697 

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

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

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

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

7335  703 

704 
Several lists of assumptions may be given (separated by 

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

13039  707 

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

13039  710 
``$\DEF{}{x \equiv t}$'' abbreviates ``$\FIX{x}~\ASSUME{}{x \equiv t}$'', 
711 
with the resulting hypothetical equation solved by reflexivity. 

7431  712 

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

13039  714 

7167  715 
\end{descr} 
716 

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

7315  719 

7167  720 

721 
\subsection{Facts and forward chaining} 

722 

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

12966  724 
\indexisarcmd{using} 
7167  725 
\begin{matharray}{rcl} 
726 
\isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\ 

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

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

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

12966  730 
\isarcmd{using} & : & \isartrans{proof(prove)}{proof(prove)} \\ 
7167  731 
\end{matharray} 
732 

7319  733 
New facts are established either by assumption or proof of local statements. 
7335  734 
Any fact will usually be involved in further proofs, either as explicit 
8547  735 
arguments of proof methods, or when forward chaining towards the next goal via 
12966  736 
$\THEN$ (and variants); $\FROMNAME$ and $\WITHNAME$ are composite forms 
13039  737 
involving $\NOTENAME$. The $\USINGNAME$ elements augments the collection of 
738 
used facts \emph{after} a goal has been stated. Note that the special theorem 

739 
name $this$\indexisarthm{this} refers to the most recently established facts, 

740 
but only \emph{before} issuing a followup claim. 

12966  741 

7167  742 
\begin{rail} 
12879  743 
'note' (thmdef? thmrefs + 'and') 
7167  744 
; 
12966  745 
('from'  'with'  'using') (thmrefs + 'and') 
7167  746 
; 
747 
\end{rail} 

748 

749 
\begin{descr} 

13039  750 

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

753 
right hand sides. 

13039  754 

7167  755 
\item [$\THEN$] indicates forward chaining by the current facts in order to 
7895  756 
establish the goal to be claimed next. The initial proof method invoked to 
13039  757 
refine that will be offered the facts to do ``anything appropriate'' (see 
7895  758 
also \S\ref{sec:proofsteps}). For example, method $rule$ (see 
8515  759 
\S\ref{sec:puremethatt}) would typically do an elimination rather than an 
7895  760 
introduction. Automatic methods usually insert the facts into the goal 
8547  761 
state before operation. This provides a simple scheme to control relevance 
762 
of facts in automated proof search. 

13039  763 

764 
\item [$\FROM{\vec b}$] abbreviates ``$\NOTE{}{\vec b}~\THEN$''; thus $\THEN$ 

765 
is equivalent to ``$\FROM{this}$''. 

766 

767 
\item [$\WITH{\vec b}$] abbreviates ``$\FROM{\vec b~\AND~this}$''; thus the 

768 
forward chaining is from earlier facts together with the current ones. 

769 

12966  770 
\item [$\USING{\vec b}$] augments the facts being currently indicated for use 
13039  771 
by a subsequent refinement step (such as $\APPLYNAME$ or $\PROOFNAME$). 
772 

7167  773 
\end{descr} 
774 

13039  775 
Forward chaining with an empty list of theorems is the same as not chaining at 
776 
all. Thus ``$\FROM{nothing}$'' has no effect apart from entering 

777 
$prove(chain)$ mode, since $nothing$\indexisarthm{nothing} is bound to the 

778 
empty list of theorems. 

9238  779 

12966  780 
Basic proof methods (such as $rule$) expect multiple facts to be given in 
781 
their proper order, corresponding to a prefix of the premises of the rule 

782 
involved. Note that positions may be easily skipped using something like 

783 
$\FROM{\Text{\texttt{_}}~a~b}$, for example. This involves the trivial rule 

784 
$\PROP\psi \Imp \PROP\psi$, which happens to be bound in Isabelle/Pure as 

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

786 

787 
Automated methods (such as $simp$ or $auto$) just insert any given facts 

788 
before their usual operation. Depending on the kind of procedure involved, 

789 
the order of facts is less significant here. 

790 

7167  791 

12976  792 
\subsection{Goal statements}\label{sec:goals} 
7167  793 

12618  794 
\indexisarcmd{lemma}\indexisarcmd{theorem}\indexisarcmd{corollary} 
7167  795 
\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus} 
796 
\begin{matharray}{rcl} 

12618  797 
\isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\ 
7167  798 
\isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\ 
12618  799 
\isarcmd{corollary} & : & \isartrans{theory}{proof(prove)} \\ 
7987  800 
\isarcmd{have} & : & \isartrans{proof(state) ~~ proof(chain)}{proof(prove)} \\ 
801 
\isarcmd{show} & : & \isartrans{proof(state) ~~ proof(chain)}{proof(prove)} \\ 

7167  802 
\isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\ 
803 
\isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\ 

804 
\end{matharray} 

805 

12621  806 
From a theory context, proof mode is entered by an initial goal command such 
13039  807 
as $\LEMMANAME$, $\THEOREMNAME$, or $\COROLLARYNAME$. Within a proof, new 
808 
claims may be introduced locally as well; four variants are available here to 

12621  809 
indicate whether forward chaining of facts should be performed initially (via 
13039  810 
$\THEN$), and whether the final result is meant to solve some pending goal. 
12618  811 

812 
Goals may consist of multiple statements, resulting in a list of facts 

813 
eventually. A pending multigoal is internally represented as a metalevel 

13039  814 
conjunction (printed as \verb,&&,), which is usually split into the 
815 
corresponding number of subgoals prior to an initial method application, via 

12618  816 
$\PROOFNAME$ (\S\ref{sec:proofsteps}) or $\APPLYNAME$ 
13039  817 
(\S\ref{sec:tacticcommands}). The $induct$ method covered in 
818 
\S\ref{sec:casesinductmeth} acts on multiple claims simultaneously. 

12966  819 

13016  820 
Claims at the theory level may be either in short or long form. A short goal 
821 
merely consists of several simultaneous propositions (often just one). A long 

822 
goal includes an explicit context specification for the subsequent 

823 
conclusions, involving local parameters; here the role of each part of the 

824 
statement is explicitly marked by separate keywords (see also 

12966  825 
\S\ref{sec:locale}). 
12618  826 

7167  827 
\begin{rail} 
13016  828 
('lemma'  'theorem'  'corollary') locale? (goal  longgoal) 
7167  829 
; 
13016  830 
('have'  'show'  'hence'  'thus') goal 
7167  831 
; 
12966  832 

13016  833 
goal: (props + 'and') 
12621  834 
; 
13016  835 
longgoal: thmdecl? (contextelem *) 'shows' goal 
12621  836 
; 
7167  837 
\end{rail} 
838 

839 
\begin{descr} 

13039  840 

12618  841 
\item [$\LEMMA{a}{\vec\phi}$] enters proof mode with $\vec\phi$ as main goal, 
842 
eventually resulting in some fact $\turn \vec\phi$ to be put back into the 

13039  843 
theory context, or into the specified locale (cf.\ \S\ref{sec:locale}). An 
844 
additional \railnonterm{context} specification may build up an initial proof 

845 
context for the subsequent claim; this includes local definitions and syntax 

846 
as well, see the definition of $contextelem$ in \S\ref{sec:locale}. 

12618  847 

848 
\item [$\THEOREM{a}{\vec\phi}$ and $\COROLLARY{a}{\vec\phi}$] are essentially 

849 
the same as $\LEMMA{a}{\vec\phi}$, but the facts are internally marked as 

850 
being of a different kind. This discrimination acts like a formal comment. 

851 

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

853 
fact within the current logical context. This operation is completely 

854 
independent of any pending subgoals of an enclosing goal statements, so 

855 
$\HAVENAME$ may be freely used for experimental exploration of potential 

856 
results within a proof body. 

857 

858 
\item [$\SHOW{a}{\vec\phi}$] is like $\HAVE{a}{\vec\phi}$ plus a second stage 

859 
to refine some pending subgoal for each one of the finished result, after 

860 
having been exported into the corresponding context (at the head of the 

13039  861 
subproof of this $\SHOWNAME$ command). 
12618  862 

863 
To accommodate interactive debugging, resulting rules are printed before 

864 
being applied internally. Even more, interactive execution of $\SHOWNAME$ 

13039  865 
predicts potential failure and displays the resulting error as a warning 
866 
beforehand. Watch out for the following message: 

12618  867 

868 
\begin{ttbox} 

869 
Problem! Local statement will fail to solve any pending goal 

870 
\end{ttbox} 

13039  871 

872 
\item [$\HENCENAME$] abbreviates ``$\THEN~\HAVENAME$'', i.e.\ claims a local 

873 
goal to be proven by forward chaining the current facts. Note that 

874 
$\HENCENAME$ is also equivalent to ``$\FROM{this}~\HAVENAME$''. 

875 

876 
\item [$\THUSNAME$] abbreviates ``$\THEN~\SHOWNAME$''. Note that $\THUSNAME$ 

877 
is also equivalent to ``$\FROM{this}~\SHOWNAME$''. 

12618  878 

7167  879 
\end{descr} 
880 

13039  881 
Any goal statement causes some term abbreviations (such as $\Var{thesis}$) to 
882 
be bound automatically, see also \S\ref{sec:termabbrev}. Furthermore, the 

883 
local context of a (nonatomic) goal is provided via the 

13048  884 
$rule_context$\indexisarcase{rulecontext} case. 
10550  885 

886 
\medskip 

887 

888 
\begin{warn} 

889 
Isabelle/Isar suffers theorylevel goal statements to contain \emph{unbound 

890 
schematic variables}, although this does not conform to the aim of 

891 
humanreadable proof documents! The main problem with schematic goals is 

892 
that the actual outcome is usually hard to predict, depending on the 

13039  893 
behavior of the proof methods applied during the course of reasoning. Note 
10550  894 
that most semiautomated methods heavily depend on several kinds of implicit 
895 
rule declarations within the current theory context. As this would also 

896 
result in noncompositional checking of subproofs, \emph{local goals} are 

12618  897 
not allowed to be schematic at all. Nevertheless, schematic goals do have 
898 
their use in Prologstyle interactive synthesis of proven results, usually 

899 
by stepwise refinement via emulation of traditional Isabelle tactic scripts 

900 
(see also \S\ref{sec:tacticcommands}). In any case, users should know what 

901 
they are doing. 

10550  902 
\end{warn} 
8991  903 

7167  904 

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

906 

7175  907 
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by} 
908 
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry} 

909 
\begin{matharray}{rcl} 

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

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

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

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

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

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

916 
\end{matharray} 

917 

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

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

7167  927 
\end{enumerate} 
928 

13039  929 
The only other (proper) way to affect pending goals in a proof body is by 
12621  930 
$\SHOWNAME$, which involves an explicit statement of what is to be solved 
931 
eventually. Thus we avoid the fundamental problem of unstructured tactic 

932 
scripts that consist of numerous consecutive goal transformations, with 

933 
invisible effects. 

7167  934 

7175  935 
\medskip 
936 

12621  937 
As a general rule of thumb for good proof style, initial proof methods should 
938 
either solve the goal completely, or constitute some wellunderstood reduction 

939 
to new subgoals. Arbitrary automatic proof tools that are prone leave a 

940 
large number of badly structured subgoals are no help in continuing the proof 

13039  941 
document in an intelligible manner. 
7175  942 

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

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

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

7167  947 

948 
\begin{rail} 

12879  949 
'proof' method? 
7167  950 
; 
12879  951 
'qed' method? 
7167  952 
; 
12879  953 
'by' method method? 
7167  954 
; 
12879  955 
('.'  '..'  'sorry') 
7167  956 
; 
957 
\end{rail} 

958 

959 
\begin{descr} 

13039  960 

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

13039  963 

7335  964 
\item [$\QED{m@2}$] refines any remaining goals by proof method $m@2$ and 
7895  965 
concludes the subproof by assumption. If the goal had been $\SHOWNAME$ (or 
966 
$\THUSNAME$), some pending subgoal is solved as well by the rule resulting 

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

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

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

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

971 
context. Debugging such a situation might involve temporarily changing 

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

13039  973 
occurrences of $\ASSUMENAME$ by $\PRESUMENAME$. 
974 

7895  975 
\item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it 
13039  976 
abbreviates $\PROOF{m@1}~\QED{m@2}$, but with backtracking across both 
977 
methods. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done 

978 
by expanding its definition; in many cases $\PROOF{m@1}$ (or even 

979 
$\APPLY{m@1}$) is already sufficient to see the problem. 

980 

7895  981 
\item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it 
8515  982 
abbreviates $\BY{rule}$. 
13039  983 

7895  984 
\item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it 
8195  985 
abbreviates $\BY{this}$. 
13039  986 

12618  987 
\item [$\SORRY$] is a \emph{fake proof}\index{proof!fake} pretending to solve 
988 
the pending claim without further ado. This only works in interactive 

13039  989 
development, or if the \texttt{quick_and_dirty} flag is enabled. Facts 
990 
emerging from fake proofs are not the real thing. Internally, each theorem 

991 
container is tainted by an oracle invocation, which is indicated as 

992 
``$[!]$'' in the printed result. 

12618  993 

994 
The most important application of $\SORRY$ is to support experimentation and 

13039  995 
topdown proof development. 
8515  996 
\end{descr} 
997 

998 

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

1000 

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

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

12621  1004 
\ref{ch:logics}). 
8515  1005 

13024  1006 
\indexisarmeth{$$}\indexisarmeth{assumption} 
1007 
\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{rules} 

12621  1008 
\indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim} 
1009 
\indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule} 

14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13827
diff
changeset

1010 
\indexisaratt{OF}\indexisaratt{of}\indexisaratt{where} 
8515  1011 
\begin{matharray}{rcl} 
13024  1012 
 & : & \isarmeth \\ 
8515  1013 
assumption & : & \isarmeth \\ 
1014 
this & : & \isarmeth \\ 

1015 
rule & : & \isarmeth \\ 

13024  1016 
rules & : & \isarmeth \\[0.5ex] 
8515  1017 
intro & : & \isaratt \\ 
1018 
elim & : & \isaratt \\ 

1019 
dest & : & \isaratt \\ 

13024  1020 
rule & : & \isaratt \\[0.5ex] 
1021 
OF & : & \isaratt \\ 

1022 
of & : & \isaratt \\ 

14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13827
diff
changeset

1023 
where & : & \isaratt \\ 
8515  1024 
\end{matharray} 
1025 

1026 
\begin{rail} 

8547  1027 
'rule' thmrefs? 
8515  1028 
; 
13024  1029 
'rules' ('!' ?) (rulemod *) 
1030 
; 

1031 
rulemod: ('intro'  'elim'  'dest') ((('!'  ()  '?') nat?)  'del') ':' thmrefs 

1032 
; 

1033 
('intro'  'elim'  'dest') ('!'  ()  '?') nat? 

1034 
; 

1035 
'rule' 'del' 

1036 
; 

8515  1037 
'OF' thmrefs 
1038 
; 

8693  1039 
'of' insts ('concl' ':' insts)? 
8515  1040 
; 
14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13827
diff
changeset

1041 
'where' (name '=' term * 'and') 
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13827
diff
changeset

1042 
; 
8515  1043 
\end{rail} 
1044 

1045 
\begin{descr} 

13024  1046 

1047 
\item [``$$''] does nothing but insert the forward chaining facts as premises 

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

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

13039  1050 
\emph{donothing} proof step would be ``$\PROOF{}$'' rather than 
1051 
$\PROOFNAME$ alone. 

13024  1052 

13039  1053 
\item [$assumption$] solves some goal by a single assumption step. All given 
1054 
facts are guaranteed to participate in the refinement; this means there may 

1055 
be only $0$ or $1$ in the first place. Recall that $\QEDNAME$ (see 

1056 
\S\ref{sec:proofsteps}) already concludes any remaining subgoals by 

1057 
assumption, so structured proofs usually need not quote the $assumption$ 

1058 
method at all. 

13024  1059 

8515  1060 
\item [$this$] applies all of the current facts directly as rules. Recall 
13039  1061 
that ``$\DOT$'' (dot) abbreviates ``$\BY{this}$''. 
13024  1062 

8547  1063 
\item [$rule~\vec a$] applies some rule given as argument in backward manner; 
8515  1064 
facts are used to reduce the rule before applying it to the goal. Thus 
13039  1065 
$rule$ without facts is plain introduction, while with facts it becomes 
1066 
elimination. 

8515  1067 

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

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

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

8515  1072 
\S\ref{sec:proofsteps}). 
13024  1073 

1074 
\item [$rules$] performs intuitionistic proof search, depending on 

1075 
specifically declared rules from the context, or given as explicit 

1076 
arguments. Chained facts are inserted into the goal before commencing proof 

13039  1077 
search; ``$rules!$'' means to include the current $prems$ as well. 
13024  1078 

1079 
Rules need to be classified as $intro$, $elim$, or $dest$; here the ``$!$'' 

1080 
indicator refers to ``safe'' rules, which may be applied aggressively 

1081 
(without considering backtracking later). Rules declared with ``$?$'' are 

1082 
ignored in proof search (the singlestep $rule$ method still observes 

1083 
these). An explicit weight annotation may be given as well; otherwise the 

13039  1084 
number of rule premises will be taken into account here. 
1085 

13024  1086 
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and 
1087 
destruct rules, to be used with the $rule$ and $rules$ methods. Note that 

13039  1088 
the latter will ignore rules declared with ``$?$'', while ``$!$'' are used 
13024  1089 
most aggressively. 
1090 

13048  1091 
The classical reasoner (see \S\ref{sec:classical}) introduces its own 
13024  1092 
variants of these attributes; use qualified names to access the present 
1093 
versions of Isabelle/Pure, i.e.\ $Pure{\dtt}intro$ or $CPure{\dtt}intro$. 

1094 

1095 
\item [$rule~del$] undeclares introduction, elimination, or destruct rules. 

1096 

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

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

13039  1100 
effectively skipped by including ``$\_$'' (underscore) as argument. 
13024  1101 

14285
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14212
diff
changeset

1102 
\item [$of~\vec t$] performs positional instantiation of term 
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14212
diff
changeset

1103 
variables. The terms $\vec t$ are substituted for any schematic 
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14212
diff
changeset

1104 
variables occurring in a theorem from left to right; ``\texttt{_}'' 
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14212
diff
changeset

1105 
(underscore) indicates to skip a position. Arguments following a 
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14212
diff
changeset

1106 
``$concl\colon$'' specification refer to positions of the conclusion 
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14212
diff
changeset

1107 
of a rule. 
13024  1108 

14285
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14212
diff
changeset

1109 
\item [$where~\vec x = \vec t$] performs named instantiation of 
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14212
diff
changeset

1110 
schematic type and term variables occurring in a theorem. Schematic 
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14212
diff
changeset

1111 
variables have to be specified on the lefthand side (e.g.\ 
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14212
diff
changeset

1112 
$?x1\!.\!3$). The question mark may be omitted if the variable name 
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14212
diff
changeset

1113 
is neither a keyword nor contains a dot. Types are instantiated 
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14212
diff
changeset

1114 
before terms, and instantiations have to be written in that order. 
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14212
diff
changeset

1115 
Because type instantiations are inferred from term instantiations, 
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14212
diff
changeset

1116 
explicit type instantiations are seldom necessary. 
14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13827
diff
changeset

1117 

7315  1118 
\end{descr} 
1119 

1120 

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

1122 

1123 
\indexisarcmd{let} 

1124 
\begin{matharray}{rcl} 

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

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

1127 
\end{matharray} 

1128 

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

7987  1130 
or by annotating assumptions or goal statements with a list of patterns 
13039  1131 
``$\ISS{p@1\;\dots}{p@n}$''. In both cases, higherorder matching is invoked 
1132 
to bind extralogical term variables, which may be either named schematic 

7987  1133 
variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}'' 
1134 
(underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the 

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

1136 
postfix position. 

7315  1137 

12621  1138 
Polymorphism of term bindings is handled in HindleyMilner style, similar to 
1139 
ML. Type variables referring to local assumptions or open goal statements are 

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

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

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

1142 
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

1143 
incremental typeinference, as the user proceeds to build up the Isar proof 
13039  1144 
text from left to right. 
8620
3786d47f5570
support HindleyMilner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset

1145 

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

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

1147 

13039  1148 
Term abbreviations are quite different from local definitions as introduced 
1149 
via $\DEFNAME$ (see \S\ref{sec:proofcontext}). The latter are visible within 

1150 
the logic as actual equations, while abbreviations disappear during the input 

1151 
process just after type checking. Also note that $\DEFNAME$ does not support 

1152 
polymorphism. 

7315  1153 

1154 
\begin{rail} 

12879  1155 
'let' ((term + 'and') '=' term + 'and') 
7315  1156 
; 
1157 
\end{rail} 

1158 

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

12618  1160 
\railnonterm{proppat} (see \S\ref{sec:termdecls}). 
7315  1161 

1162 
\begin{descr} 

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

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

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

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

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

1168 
\end{descr} 

1169 

10160  1170 
Some \emph{automatic} term abbreviations\index{term abbreviations} for goals 
7988  1171 
and facts are available as well. For any open goal, 
10160  1172 
$\Var{thesis}$\indexisarvar{thesis} refers to its objectlevel statement, 
1173 
abstracted over any metalevel parameters (if present). Likewise, 

1174 
$\Var{this}$\indexisarvar{this} is bound for fact statements resulting from 

1175 
assumptions or finished goals. In case $\Var{this}$ refers to an objectlogic 

1176 
statement that is an application $f(t)$, then $t$ is bound to the special text 

1177 
variable ``$\dots$''\indexisarvar{\dots} (three dots). The canonical 

1178 
application of the latter are calculational proofs (see 

1179 
\S\ref{sec:calculation}). 

1180 

7315  1181 

7134  1182 
\subsection{Block structure} 
1183 

8896  1184 
\indexisarcmd{next}\indexisarcmd{\{}\indexisarcmd{\}} 
7397  1185 
\begin{matharray}{rcl} 
8448  1186 
\NEXT & : & \isartrans{proof(state)}{proof(state)} \\ 
7974  1187 
\BG & : & \isartrans{proof(state)}{proof(state)} \\ 
1188 
\EN & : & \isartrans{proof(state)}{proof(state)} \\ 

7397  1189 
\end{matharray} 
1190 

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

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

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

8448  1195 
different context within a subproof may be switched via $\NEXT$, which is 
13039  1196 
just a single blockclose followed by blockopen again. The effect of $\NEXT$ 
1197 
is to reset the local proof context; there is no goal focus involved here! 

7167  1198 

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

1202 
\begin{descr} 

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

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

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

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

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

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

7167  1212 
\end{descr} 
7134  1213 

1214 

9605  1215 
\subsection{Emulating tactic scripts}\label{sec:tacticcommands} 
8515  1216 

9605  1217 
The Isar provides separate commands to accommodate tacticstyle proof scripts 
1218 
within the same system. While being outside the orthodox Isar proof language, 

1219 
these might come in handy for interactive exploration and debugging, or even 

1220 
actual tactical proof within newstyle theories (to benefit from document 

1221 
preparation, for example). See also \S\ref{sec:tactics} for actual tactics, 

1222 
that have been encapsulated as proof methods. Proper proof methods may be 

1223 
used in scripts, too. 

8515  1224 

9605  1225 
\indexisarcmd{apply}\indexisarcmd{applyend}\indexisarcmd{done} 
8515  1226 
\indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back} 
9605  1227 
\indexisarcmd{declare} 
8515  1228 
\begin{matharray}{rcl} 
8533  1229 
\isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\ 
9605  1230 
\isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\ 
8946  1231 
\isarcmd{done}^* & : & \isartrans{proof(prove)}{proof(state)} \\ 
8533  1232 
\isarcmd{defer}^* & : & \isartrans{proof}{proof} \\ 
1233 
\isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\ 

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

9605  1235 
\isarcmd{declare}^* & : & \isartrans{theory}{theory} \\ 
8515  1236 
\end{matharray} 
1237 

1238 
\railalias{applyend}{apply\_end} 

1239 
\railterm{applyend} 

1240 

1241 
\begin{rail} 

12879  1242 
( 'apply'  applyend ) method 
8515  1243 
; 
12879  1244 
'defer' nat? 
8515  1245 
; 
12879  1246 
'prefer' nat 
8515  1247 
; 
12976  1248 
'declare' locale? (thmrefs + 'and') 
9605  1249 
; 
8515  1250 
\end{rail} 
1251 

1252 
\begin{descr} 

13042  1253 

10223  1254 
\item [$\APPLY{m}$] applies proof method $m$ in initial position, but unlike 
1255 
$\PROOFNAME$ it retains ``$proof(prove)$'' mode. Thus consecutive method 

1256 
applications may be given just as in tactic scripts. 

8515  1257 

8881  1258 
Facts are passed to $m$ as indicated by the goal's forwardchain mode, and 
10223  1259 
are \emph{consumed} afterwards. Thus any further $\APPLYNAME$ command would 
1260 
always work in a purely backward manner. 

8946  1261 

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

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

1265 

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

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

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

13039  1269 

9605  1270 
\item [$\isarkeyword{done}$] completes a proof script, provided that the 
13039  1271 
current goal state is solved completely. Note that actual structured proof 
1272 
commands (e.g.\ ``$\DOT$'' or $\SORRY$) may be used to conclude proof 

1273 
scripts as well. 

9605  1274 

8515  1275 
\item [$\isarkeyword{defer}~n$ and $\isarkeyword{prefer}~n$] shuffle the list 
1276 
of pending goals: $defer$ puts off goal $n$ to the end of the list ($n = 1$ 

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

13039  1278 

8515  1279 
\item [$\isarkeyword{back}$] does backtracking over the result sequence of 
13039  1280 
the latest proof command. Basically, any proof command may return multiple 
1281 
results. 

9605  1282 

1283 
\item [$\isarkeyword{declare}~thms$] declares theorems to the current theory 

12976  1284 
context (or the specified locale, see also \S\ref{sec:locale}). No theorem 
1285 
binding is involved here, unlike $\isarkeyword{theorems}$ or 

1286 
$\isarkeyword{lemmas}$ (cf.\ \S\ref{sec:axmsthms}), so 

1287 
$\isarkeyword{declare}$ only has the effect of applying attributes as 

1288 
included in the theorem specification. 

13042  1289 

9006  1290 
\end{descr} 
1291 

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

10223  1293 
$\APPLYNAME$. A few additional emulations of actual tactics are provided as 
1294 
well; these would be never used in actual structured proofs, of course. 

9006  1295 

8515  1296 

1297 
\subsection{Metalinguistic features} 

1298 

1299 
\indexisarcmd{oops} 

1300 
\begin{matharray}{rcl} 

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

1302 
\end{matharray} 

1303 

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

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

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