author  kleing 
Mon, 29 Dec 2003 06:49:26 +0100  
changeset 14333  14f29eb097a3 
parent 14285  92ed032e83a1 
child 14642  2bfe5de2d1fa 
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 
; 
12879  168 
'classrel' nameref ('<'  subseteq) nameref 
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. 
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11017
diff
changeset

178 
\item [$\isarkeyword{classrel}~c@1 \subseteq c@2$] states a subclass relation 
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} 

244 
'consts' (constdecl +) 

245 
; 

12879  246 
'defs' ('(overloaded)')? (axmdecl prop +) 
7134  247 
; 
12879  248 
'constdefs' (constdecl prop +) 
7134  249 
; 
250 

12879  251 
constdecl: name '::' type mixfix? 
7134  252 
; 
253 
\end{rail} 

254 

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

7895  258 
to the constants declared. 
9308  259 

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

262 
form of equations admitted as constant definitions. 

9308  263 

264 
The $overloaded$ option declares definitions to be potentially overloaded. 

265 
Unless this option is given, a warning message would be issued for any 

266 
definitional equation with a more special type than that of the 

267 
corresponding constant declaration. 

12621  268 

269 
\item [$\CONSTDEFS~c::\sigma~eqn$] combines declarations and definitions of 

270 
constants, using the canonical name $c_def$ for the definitional axiom. 

7167  271 
\end{descr} 
7134  272 

273 

7981  274 
\subsection{Syntax and translations}\label{sec:syntrans} 
7134  275 

276 
\indexisarcmd{syntax}\indexisarcmd{translations} 

277 
\begin{matharray}{rcl} 

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

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

280 
\end{matharray} 

281 

10640  282 
\railalias{rightleftharpoons}{\isasymrightleftharpoons} 
283 
\railterm{rightleftharpoons} 

284 

285 
\railalias{rightharpoonup}{\isasymrightharpoonup} 

286 
\railterm{rightharpoonup} 

287 

288 
\railalias{leftharpoondown}{\isasymleftharpoondown} 

289 
\railterm{leftharpoondown} 

290 

7134  291 
\begin{rail} 
9727  292 
'syntax' ('(' ( name  'output'  name 'output' ) ')')? (constdecl +) 
7134  293 
; 
12879  294 
'translations' (transpat ('=='  '=>'  '<='  rightleftharpoons  rightharpoonup  leftharpoondown) transpat +) 
7134  295 
; 
296 
transpat: ('(' nameref ')')? string 

297 
; 

298 
\end{rail} 

299 

7167  300 
\begin{descr} 
13024  301 

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

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

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

308 
the input and output grammar. 

309 

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

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

314 
for parsing; the default is $logic$. 

7167  315 
\end{descr} 
7134  316 

317 

9605  318 
\subsection{Axioms and theorems}\label{sec:axmsthms} 
7134  319 

12618  320 
\indexisarcmd{axioms}\indexisarcmd{lemmas}\indexisarcmd{theorems} 
12621  321 
\begin{matharray}{rcll} 
322 
\isarcmd{axioms} & : & \isartrans{theory}{theory} & (axiomatic!) \\ 

12618  323 
\isarcmd{lemmas} & : & \isartrans{theory}{theory} \\ 
7134  324 
\isarcmd{theorems} & : & \isartrans{theory}{theory} \\ 
325 
\end{matharray} 

326 

327 
\begin{rail} 

12879  328 
'axioms' (axmdecl prop +) 
7134  329 
; 
12976  330 
('lemmas'  'theorems') locale? (thmdef? thmrefs + 'and') 
7134  331 
; 
332 
\end{rail} 

333 

7167  334 
\begin{descr} 
12976  335 

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

7134  339 

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

7175  341 
Everyday work is typically done the hard way, with proper definitions and 
13039  342 
proven theorems. 
12976  343 

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

347 
declare Simplifier rules, for example. 

348 

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

12976  351 

7167  352 
\end{descr} 
7134  353 

354 

7167  355 
\subsection{Name spaces} 
7134  356 

8726  357 
\indexisarcmd{global}\indexisarcmd{local}\indexisarcmd{hide} 
7134  358 
\begin{matharray}{rcl} 
359 
\isarcmd{global} & : & \isartrans{theory}{theory} \\ 

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

8726  361 
\isarcmd{hide} & : & \isartrans{theory}{theory} \\ 
7134  362 
\end{matharray} 
363 

8726  364 
\begin{rail} 
12879  365 
'hide' name (nameref + ) 
8726  366 
; 
367 
\end{rail} 

368 

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

7175  373 

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

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

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

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

8726  380 

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

382 
qualified names of the same base name are introduced. 

383 

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

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

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

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

12621  388 
full internal name. Unqualified (global) names may not be hidden. 
7167  389 
\end{descr} 
7134  390 

391 

7167  392 
\subsection{Incorporating ML code}\label{sec:ML} 
7134  393 

8682  394 
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{MLcommand} 
395 
\indexisarcmd{MLsetup}\indexisarcmd{setup} 

9199  396 
\indexisarcmd{methodsetup} 
7134  397 
\begin{matharray}{rcl} 
398 
\isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\ 

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

8682  400 
\isarcmd{ML_command} & : & \isartrans{\cdot}{\cdot} \\ 
7895  401 
\isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\ 
7175  402 
\isarcmd{setup} & : & \isartrans{theory}{theory} \\ 
9199  403 
\isarcmd{method_setup} & : & \isartrans{theory}{theory} \\ 
7134  404 
\end{matharray} 
405 

7895  406 
\railalias{MLsetup}{ML\_setup} 
407 
\railterm{MLsetup} 

408 

9199  409 
\railalias{methodsetup}{method\_setup} 
410 
\railterm{methodsetup} 

411 

8682  412 
\railalias{MLcommand}{ML\_command} 
413 
\railterm{MLcommand} 

414 

7134  415 
\begin{rail} 
12879  416 
'use' name 
7134  417 
; 
12879  418 
('ML'  MLcommand  MLsetup  'setup') text 
7134  419 
; 
12879  420 
methodsetup name '=' text text 
9199  421 
; 
7134  422 
\end{rail} 
423 

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

430 

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

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

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

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

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

439 

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

8547  443 
canonical way to initialize any objectlogic specific tools and packages 
444 
written in ML. 

9199  445 

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

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

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

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

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

451 
arguments, or a list of theorems, respectively. 

452 

453 
{\footnotesize 

454 
\begin{verbatim} 

9605  455 
Method.no_args (Method.METHOD (fn facts => foobar_tac)) 
456 
Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac)) 

10899  457 
Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac)) 
12618  458 
Method.thms_ctxt_args (fn thms => fn ctxt => 
459 
Method.METHOD (fn facts => foobar_tac)) 

9199  460 
\end{verbatim} 
461 
} 

462 

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

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

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

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

468 
tactic. 

7167  469 
\end{descr} 
7134  470 

471 

8250  472 
\subsection{Syntax translation functions} 
7134  473 

8250  474 
\indexisarcmd{parseasttranslation}\indexisarcmd{parsetranslation} 
475 
\indexisarcmd{printtranslation}\indexisarcmd{typedprinttranslation} 

476 
\indexisarcmd{printasttranslation}\indexisarcmd{tokentranslation} 

477 
\begin{matharray}{rcl} 

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

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

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

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

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

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

484 
\end{matharray} 

7134  485 

9273  486 
\railalias{parseasttranslation}{parse\_ast\_translation} 
487 
\railterm{parseasttranslation} 

488 

489 
\railalias{parsetranslation}{parse\_translation} 

490 
\railterm{parsetranslation} 

491 

492 
\railalias{printtranslation}{print\_translation} 

493 
\railterm{printtranslation} 

494 

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

496 
\railterm{typedprinttranslation} 

497 

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

499 
\railterm{printasttranslation} 

500 

501 
\railalias{tokentranslation}{token\_translation} 

502 
\railterm{tokentranslation} 

503 

504 
\begin{rail} 

505 
( parseasttranslation  parsetranslation  printtranslation  typedprinttranslation  

12879  506 
printasttranslation  tokentranslation ) text 
9273  507 
\end{rail} 
508 

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

13048  511 
single \railqtok{text} argument that refers to an ML expression of appropriate 
512 
type. 

8379  513 

514 
\begin{ttbox} 

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

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

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

518 
val typed_print_translation : 

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

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

521 
val token_translation : 

522 
(string * string * (string > string * real)) list 

523 
\end{ttbox} 

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

7134  525 

526 

527 
\subsection{Oracles} 

528 

529 
\indexisarcmd{oracle} 

530 
\begin{matharray}{rcl} 

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

532 
\end{matharray} 

533 

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

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

537 

7134  538 
\begin{rail} 
12879  539 
'oracle' name '=' text 
7134  540 
; 
541 
\end{rail} 

542 

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

7167  547 
\end{descr} 
7134  548 

549 

550 
\section{Proof commands} 

551 

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

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

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

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

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

567 
goal claimed next. 

7167  568 
\end{descr} 
7134  569 

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

572 
restricts the shape of wellformed proof texts to particular command 

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

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

7167  576 

12621  577 

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

7167  579 

7987  580 
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect} 
7895  581 
\indexisarcmd{txt}\indexisarcmd{txtraw} 
7134  582 
\begin{matharray}{rcl} 
8101  583 
\isarcmd{sect} & : & \isartrans{proof}{proof} \\ 
584 
\isarcmd{subsect} & : & \isartrans{proof}{proof} \\ 

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

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

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

7134  588 
\end{matharray} 
589 

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

593 
\railalias{txtraw}{txt\_raw} 

594 
\railterm{txtraw} 

7175  595 

7134  596 
\begin{rail} 
7895  597 
('sect'  'subsect'  'subsubsect'  'txt'  txtraw) text 
7134  598 
; 
599 
\end{rail} 

600 

601 

12621  602 
\subsection{Context elements}\label{sec:proofcontext} 
7134  603 

7315  604 
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def} 
7134  605 
\begin{matharray}{rcl} 
606 
\isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\ 

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

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

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

610 
\end{matharray} 

611 

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

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

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

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

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

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

7315  620 

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

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

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

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

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

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

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

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

630 
user. 

7315  631 

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

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

7175  636 

10686  637 
\railalias{equiv}{\isasymequiv} 
638 
\railterm{equiv} 

639 

7134  640 
\begin{rail} 
12879  641 
'fix' (vars + 'and') 
7134  642 
; 
12879  643 
('assume'  'presume') (props + 'and') 
7134  644 
; 
12879  645 
'def' thmdecl? \\ name ('=='  equiv) term termpat? 
7134  646 
; 
647 
\end{rail} 

648 

7167  649 
\begin{descr} 
13039  650 

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

13039  653 

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

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

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

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

7335  659 

660 
Several lists of assumptions may be given (separated by 

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

13039  663 

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

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

7431  668 

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

13039  670 

7167  671 
\end{descr} 
672 

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

7315  675 

7167  676 

677 
\subsection{Facts and forward chaining} 

678 

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

12966  680 
\indexisarcmd{using} 
7167  681 
\begin{matharray}{rcl} 
682 
\isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\ 

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

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

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

12966  686 
\isarcmd{using} & : & \isartrans{proof(prove)}{proof(prove)} \\ 
7167  687 
\end{matharray} 
688 

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

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

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

12966  697 

7167  698 
\begin{rail} 
12879  699 
'note' (thmdef? thmrefs + 'and') 
7167  700 
; 
12966  701 
('from'  'with'  'using') (thmrefs + 'and') 
7167  702 
; 
703 
\end{rail} 

704 

705 
\begin{descr} 

13039  706 

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

709 
right hand sides. 

13039  710 

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

13039  719 

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

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

722 

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

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

725 

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

7167  729 
\end{descr} 
730 

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

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

734 
empty list of theorems. 

9238  735 

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

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

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

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

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

742 

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

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

745 
the order of facts is less significant here. 

746 

7167  747 

12976  748 
\subsection{Goal statements}\label{sec:goals} 
7167  749 

12618  750 
\indexisarcmd{lemma}\indexisarcmd{theorem}\indexisarcmd{corollary} 
7167  751 
\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus} 
752 
\begin{matharray}{rcl} 

12618  753 
\isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\ 
7167  754 
\isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\ 
12618  755 
\isarcmd{corollary} & : & \isartrans{theory}{proof(prove)} \\ 
7987  756 
\isarcmd{have} & : & \isartrans{proof(state) ~~ proof(chain)}{proof(prove)} \\ 
757 
\isarcmd{show} & : & \isartrans{proof(state) ~~ proof(chain)}{proof(prove)} \\ 

7167  758 
\isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\ 
759 
\isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\ 

760 
\end{matharray} 

761 

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

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

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

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

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

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

12966  775 

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

778 
goal includes an explicit context specification for the subsequent 

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

780 
statement is explicitly marked by separate keywords (see also 

12966  781 
\S\ref{sec:locale}). 
12618  782 

7167  783 
\begin{rail} 
13016  784 
('lemma'  'theorem'  'corollary') locale? (goal  longgoal) 
7167  785 
; 
13016  786 
('have'  'show'  'hence'  'thus') goal 
7167  787 
; 
12966  788 

13016  789 
goal: (props + 'and') 
12621  790 
; 
13016  791 
longgoal: thmdecl? (contextelem *) 'shows' goal 
12621  792 
; 
7167  793 
\end{rail} 
794 

795 
\begin{descr} 

13039  796 

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

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

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

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

12618  803 

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

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

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

807 

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

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

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

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

812 
results within a proof body. 

813 

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

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

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

13039  817 
subproof of this $\SHOWNAME$ command). 
12618  818 

819 
To accommodate interactive debugging, resulting rules are printed before 

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

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

12618  823 

824 
\begin{ttbox} 

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

826 
\end{ttbox} 

13039  827 

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

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

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

831 

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

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

12618  834 

7167  835 
\end{descr} 
836 

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

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

13048  840 
$rule_context$\indexisarcase{rulecontext} case. 
10550  841 

842 
\medskip 

843 

844 
\begin{warn} 

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

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

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

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

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

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

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

855 
by stepwise refinement via emulation of traditional Isabelle tactic scripts 

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

857 
they are doing. 

10550  858 
\end{warn} 
8991  859 

7167  860 

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

862 

7175  863 
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by} 
864 
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry} 

865 
\begin{matharray}{rcl} 

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

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

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

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

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

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

872 
\end{matharray} 

873 

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

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

7167  883 
\end{enumerate} 
884 

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

888 
scripts that consist of numerous consecutive goal transformations, with 

889 
invisible effects. 

7167  890 

7175  891 
\medskip 
892 

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

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

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

13039  897 
document in an intelligible manner. 
7175  898 

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

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

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

7167  903 

904 
\begin{rail} 

12879  905 
'proof' method? 
7167  906 
; 
12879  907 
'qed' method? 
7167  908 
; 
12879  909 
'by' method method? 
7167  910 
; 
12879  911 
('.'  '..'  'sorry') 
7167  912 
; 
913 
\end{rail} 

914 

915 
\begin{descr} 

13039  916 

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

13039  919 

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

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

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

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

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

927 
context. Debugging such a situation might involve temporarily changing 

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

13039  929 
occurrences of $\ASSUMENAME$ by $\PRESUMENAME$. 
930 

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

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

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

936 

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

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

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

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

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

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

12618  949 

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

13039  951 
topdown proof development. 
8515  952 
\end{descr} 
953 

954 

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

956 

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

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

12621  960 
\ref{ch:logics}). 
8515  961 

13024  962 
\indexisarmeth{$$}\indexisarmeth{assumption} 
963 
\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{rules} 

12621  964 
\indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim} 
965 
\indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule} 

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

966 
\indexisaratt{OF}\indexisaratt{of}\indexisaratt{where} 
8515  967 
\begin{matharray}{rcl} 
13024  968 
 & : & \isarmeth \\ 
8515  969 
assumption & : & \isarmeth \\ 
970 
this & : & \isarmeth \\ 

971 
rule & : & \isarmeth \\ 

13024  972 
rules & : & \isarmeth \\[0.5ex] 
8515  973 
intro & : & \isaratt \\ 
974 
elim & : & \isaratt \\ 

975 
dest & : & \isaratt \\ 

13024  976 
rule & : & \isaratt \\[0.5ex] 
977 
OF & : & \isaratt \\ 

978 
of & : & \isaratt \\ 

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

979 
where & : & \isaratt \\ 
8515  980 
\end{matharray} 
981 

982 
\begin{rail} 

8547  983 
'rule' thmrefs? 
8515  984 
; 
13024  985 
'rules' ('!' ?) (rulemod *) 
986 
; 

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

988 
; 

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

990 
; 

991 
'rule' 'del' 

992 
; 

8515  993 
'OF' thmrefs 
994 
; 

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

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

998 
; 
8515  999 
\end{rail} 
1000 

1001 
\begin{descr} 

13024  1002 

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

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

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

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

13024  1008 

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

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

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

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

1014 
method at all. 

13024  1015 

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

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

8515  1023 

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

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

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

8515  1028 
\S\ref{sec:proofsteps}). 
13024  1029 

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

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

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

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

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

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

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

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

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

13039  1040 
number of rule premises will be taken into account here. 
1041 

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

13039  1044 
the latter will ignore rules declared with ``$?$'', while ``$!$'' are used 
13024  1045 
most aggressively. 
1046 

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

1050 

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

1052 

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

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

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

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

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

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

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

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

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

1063 
of a rule. 
13024  1064 

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

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

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

1067 
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

1068 
$?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

1069 
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

1070 
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

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

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

1073 

7315  1074 
\end{descr} 
1075 

1076 

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

1078 

1079 
\indexisarcmd{let} 

1080 
\begin{matharray}{rcl} 

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

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

1083 
\end{matharray} 

1084 

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

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

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

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

1092 
postfix position. 

7315  1093 

12621  1094 
Polymorphism of term bindings is handled in HindleyMilner style, similar to 
1095 
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

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

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

1098 
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

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

1101 

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

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

1103 

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

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

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

1108 
polymorphism. 

7315  1109 

1110 
\begin{rail} 

12879  1111 
'let' ((term + 'and') '=' term + 'and') 
7315  1112 
; 
1113 
\end{rail} 

1114 

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

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

1118 
\begin{descr} 

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

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

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

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

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

1124 
\end{descr} 

1125 

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

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

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

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

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

1134 
application of the latter are calculational proofs (see 

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

1136 

7315  1137 

7134  1138 
\subsection{Block structure} 
1139 

8896  1140 
\indexisarcmd{next}\indexisarcmd{\{}\indexisarcmd{\}} 
7397  1141 
\begin{matharray}{rcl} 
8448  1142 
\NEXT & : & \isartrans{proof(state)}{proof(state)} \\ 
7974  1143 
\BG & : & \isartrans{proof(state)}{proof(state)} \\ 
1144 
\EN & : & \isartrans{proof(state)}{proof(state)} \\ 

7397  1145 
\end{matharray} 
1146 

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

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

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

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

7167  1154 

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

1158 
\begin{descr} 

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

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

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

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

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

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

7167  1168 
\end{descr} 
7134  1169 

1170 

9605  1171 
\subsection{Emulating tactic scripts}\label{sec:tacticcommands} 
8515  1172 

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

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

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

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

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

1179 
used in scripts, too. 

8515  1180 

9605  1181 
\indexisarcmd{apply}\indexisarcmd{applyend}\indexisarcmd{done} 
8515  1182 
\indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back} 
9605  1183 
\indexisarcmd{declare} 
8515  1184 
\begin{matharray}{rcl} 
8533  1185 
\isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\ 
9605  1186 
\isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\ 
8946  1187 
\isarcmd{done}^* & : & \isartrans{proof(prove)}{proof(state)} \\ 
8533  1188 
\isarcmd{defer}^* & : & \isartrans{proof}{proof} \\ 
1189 
\isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\ 

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

9605  1191 
\isarcmd{declare}^* & : & \isartrans{theory}{theory} \\ 
8515  1192 
\end{matharray} 
1193 

1194 
\railalias{applyend}{apply\_end} 

1195 
\railterm{applyend} 

1196 

1197 
\begin{rail} 

12879  1198 
( 'apply'  applyend ) method 
8515  1199 
; 
12879  1200 
'defer' nat? 
8515  1201 
; 
12879  1202 
'prefer' nat 
8515  1203 
; 
12976  1204 
'declare' locale? (thmrefs + 'and') 
9605  1205 
; 
8515  1206 
\end{rail} 
1207 

1208 
\begin{descr} 

13042  1209 

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

1212 
applications may be given just as in tactic scripts. 

8515  1213 

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

8946  1217 

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

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

1221 

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

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

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

13039  1225 

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

1229 
scripts as well. 

9605  1230 

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

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

13039  1234 

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

9605  1238 

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

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

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

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

1244 
included in the theorem specification. 

13042  1245 

9006  1246 
\end{descr} 
1247 

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

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

9006  1251 

8515  1252 

1253 
\subsection{Metalinguistic features} 

1254 

1255 
\indexisarcmd{oops} 

1256 
\begin{matharray}{rcl} 

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

1258 
\end{matharray} 

1259 

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

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

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

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

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

13039  1265 
produce any result theorem  there is no intended claim to be able to 
1266 
complete the proof anyhow. 

8515  1267 

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

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

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

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

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

1273 
``$\OOPS$'' keyword. 

1274 

12618  1275 
\medskip The $\OOPS$ command is undoable, unlike $\isarkeyword{kill}$ (see 
13039  1276 
\S\ref{sec:history}). The effect is to get back to the theory just before the 
1277 
opening of the proof. 

8515  1278 

1279 

7134  1280 
\section{Other commands} 
1281 

9605  1282 
\subsection{Diagnostics} 
7134  1283 

10858  1284 
\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term} 
1285 
\indexisarcmd{prop}\indexisarcmd{typ} 

7134  1286 
\begin{matharray}{rcl} 
8515  1287 
\isarcmd{pr}^* & : & \isarkeep{\cdot} \\ 
1288 
\isarcmd{thm}^* & : & \isarkeep{theory~~proof} \\ 

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

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

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

13827
c690cb885db4
Documented prf / full_prf commands and antiquotations.
berghofe
parents:
13542
diff
changeset

1292 
\isarcmd{prf}^* & : & \isarkeep{theory~~proof} \\ 
c690cb885db4
Documented prf / full_prf commands and antiquotations.
berghofe
parents:
13542
diff
changeset

1293 
\isarcmd{full_prf}^* & : & \isarkeep{theory~~proof} \\ 
7134  1294 
\end{matharray} 
1295 

9605  1296 
These diagnostic commands assist interactive development. Note that $undo$ 
1297 
does not apply here, the theory or proof configuration is not changed. 

7335  1298 

7134  1299 
\begin{rail} 
9727  1300 
'pr' modes? nat? (',' nat)? 
7134  1301 
; 
12879  1302 
'thm' modes? thmrefs 
8485  1303 
; 
12879  1304 
'term' modes? term 
7134  1305 
; 
12879  1306 
'prop' modes? prop 