author  wenzelm 
Tue, 12 Feb 2002 20:33:03 +0100  
changeset 12879  8e1cae1de136 
parent 12621  48cafea0684b 
child 12966  6373b4d09325 
permissions  rwrr 
7046  1 

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

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

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 
7981  17 
documents, while their use is discouraged for the final outcome. Typical 
18 
examples are diagnostic commands that print terms or theorems according to the 

12621  19 
current context; other commands emulate oldstyle tactical theorem proving. 
7167  20 

7134  21 

12621  22 
\section{Theory commands} 
7134  23 

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

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

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

7134  32 
\end{matharray} 
33 

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

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

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

7134  39 

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

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

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

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

45 
$\END$ commands concludes a theory development; it has to be the very last 

46 
command of any theory file to loaded in batchmode. The theory context may be 

47 
also changed interactively by $\CONTEXT$ without creating a new theory. 

7134  48 

49 
\begin{rail} 

7895  50 
'header' text 
51 
; 

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

54 
'context' name 

55 
; 

56 

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

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

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

66 

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

69 

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

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

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

73 
are always uptodate. Changed files are automatically reloaded when 

74 
processing theory headers interactively; batchmode explicitly distinguishes 

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

76 

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

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

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

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

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

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

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

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

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

7134  86 

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

90 
loaded and uptodate. 

7175  91 

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

94 

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

98 

7167  99 
\end{descr} 
7134  100 

101 

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

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

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

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

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

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

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

7134  119 

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

7134  122 

123 
\begin{rail} 

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

127 

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

131 
and section headings. 

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

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

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

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

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

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

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

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

7895  146 

8485  147 
\medskip 
148 

149 
Additional markup commands are available for proofs (see 

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

7895  153 

7134  154 

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

157 
\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort} 

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

163 

164 
\begin{rail} 

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

172 

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

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

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

176 
out. 
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11017
diff
changeset

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

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

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

186 

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

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

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

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

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

197 
\begin{rail} 

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

207 

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

7895  212 
syntactic abbreviations without any logical significance. Internally, type 
7981  213 
synonyms are fully expanded. 
7134  214 
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor 
7895  215 
$t$, intended as an actual logical type. Note that objectlogics such as 
216 
Isabelle/HOL override $\isarkeyword{typedecl}$ by their own version. 

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

219 
Isabelle's inner syntax of terms or types. 

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

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

7167  224 
\end{descr} 
7134  225 

226 

7981  227 
\subsection{Constants and simple definitions}\label{sec:consts} 
7134  228 

7175  229 
\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl} 
7134  230 
\begin{matharray}{rcl} 
231 
\isarcmd{consts} & : & \isartrans{theory}{theory} \\ 

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

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

234 
\end{matharray} 

235 

236 
\begin{rail} 

237 
'consts' (constdecl +) 

238 
; 

12879  239 
'defs' ('(overloaded)')? (axmdecl prop +) 
7134  240 
; 
12879  241 
'constdefs' (constdecl prop +) 
7134  242 
; 
243 

12879  244 
constdecl: name '::' type mixfix? 
7134  245 
; 
246 
\end{rail} 

247 

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

7895  251 
to the constants declared. 
9308  252 

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

255 
form of equations admitted as constant definitions. 

9308  256 

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

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

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

260 
corresponding constant declaration. 

12621  261 

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

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

7167  264 
\end{descr} 
7134  265 

266 

7981  267 
\subsection{Syntax and translations}\label{sec:syntrans} 
7134  268 

269 
\indexisarcmd{syntax}\indexisarcmd{translations} 

270 
\begin{matharray}{rcl} 

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

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

273 
\end{matharray} 

274 

10640  275 
\railalias{rightleftharpoons}{\isasymrightleftharpoons} 
276 
\railterm{rightleftharpoons} 

277 

278 
\railalias{rightharpoonup}{\isasymrightharpoonup} 

279 
\railterm{rightharpoonup} 

280 

281 
\railalias{leftharpoondown}{\isasymleftharpoondown} 

282 
\railterm{leftharpoondown} 

283 

7134  284 
\begin{rail} 
9727  285 
'syntax' ('(' ( name  'output'  name 'output' ) ')')? (constdecl +) 
7134  286 
; 
12879  287 
'translations' (transpat ('=='  '=>'  '<='  rightleftharpoons  rightharpoonup  leftharpoondown) transpat +) 
7134  288 
; 
289 
transpat: ('(' nameref ')')? string 

290 
; 

291 
\end{rail} 

292 

7167  293 
\begin{descr} 
7175  294 
\item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$, 
295 
except that the actual logical signature extension is omitted. Thus the 

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

7335  297 
arbitrary ways, independently of the logic. The $mode$ argument refers to 
8547  298 
the print mode that the grammar rules belong; unless the \texttt{output} 
299 
flag is given, all productions are added both to the input and output 

300 
grammar. 

7175  301 
\item [$\isarkeyword{translations}~rules$] specifies syntactic translation 
10640  302 
rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==} or 
303 
\isasymrightleftharpoons), parse rules (\texttt{=>} or 

304 
\isasymrightharpoonup), or print rules (\texttt{<=} or 

305 
\isasymleftharpoondown). Translation patterns may be prefixed by the 

306 
syntactic category to be used for parsing; the default is \texttt{logic}. 

7167  307 
\end{descr} 
7134  308 

309 

9605  310 
\subsection{Axioms and theorems}\label{sec:axmsthms} 
7134  311 

12618  312 
\indexisarcmd{axioms}\indexisarcmd{lemmas}\indexisarcmd{theorems} 
12621  313 
\begin{matharray}{rcll} 
314 
\isarcmd{axioms} & : & \isartrans{theory}{theory} & (axiomatic!) \\ 

12618  315 
\isarcmd{lemmas} & : & \isartrans{theory}{theory} \\ 
7134  316 
\isarcmd{theorems} & : & \isartrans{theory}{theory} \\ 
317 
\end{matharray} 

318 

319 
\begin{rail} 

12879  320 
'axioms' (axmdecl prop +) 
7134  321 
; 
12879  322 
('lemmas'  'theorems') (thmdef? thmrefs + 'and') 
7134  323 
; 
324 
\end{rail} 

325 

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

7134  330 

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

7175  332 
Everyday work is typically done the hard way, with proper definitions and 
8547  333 
actual proven theorems. 
12618  334 
\item [$\isarkeyword{lemmas}~a = \vec b$] stores existing facts. Typical 
335 
applications would also involve attributes, to declare Simplifier rules, for 

336 
example. 

337 
\item [$\isarkeyword{theorems}$] is essentially the same as 

338 
$\isarkeyword{lemmas}$, but marks the result as a different kind of facts. 

7167  339 
\end{descr} 
7134  340 

341 

7167  342 
\subsection{Name spaces} 
7134  343 

8726  344 
\indexisarcmd{global}\indexisarcmd{local}\indexisarcmd{hide} 
7134  345 
\begin{matharray}{rcl} 
346 
\isarcmd{global} & : & \isartrans{theory}{theory} \\ 

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

8726  348 
\isarcmd{hide} & : & \isartrans{theory}{theory} \\ 
7134  349 
\end{matharray} 
350 

8726  351 
\begin{rail} 
12879  352 
'hide' name (nameref + ) 
8726  353 
; 
354 
\end{rail} 

355 

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

7175  360 

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

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

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

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

8726  367 

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

369 
qualified names of the same base name are introduced. 

370 

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

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

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

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

12621  375 
full internal name. Unqualified (global) names may not be hidden. 
7167  376 
\end{descr} 
7134  377 

378 

7167  379 
\subsection{Incorporating ML code}\label{sec:ML} 
7134  380 

8682  381 
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{MLcommand} 
382 
\indexisarcmd{MLsetup}\indexisarcmd{setup} 

9199  383 
\indexisarcmd{methodsetup} 
7134  384 
\begin{matharray}{rcl} 
385 
\isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\ 

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

8682  387 
\isarcmd{ML_command} & : & \isartrans{\cdot}{\cdot} \\ 
7895  388 
\isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\ 
7175  389 
\isarcmd{setup} & : & \isartrans{theory}{theory} \\ 
9199  390 
\isarcmd{method_setup} & : & \isartrans{theory}{theory} \\ 
7134  391 
\end{matharray} 
392 

7895  393 
\railalias{MLsetup}{ML\_setup} 
394 
\railterm{MLsetup} 

395 

9199  396 
\railalias{methodsetup}{method\_setup} 
397 
\railterm{methodsetup} 

398 

8682  399 
\railalias{MLcommand}{ML\_command} 
400 
\railterm{MLcommand} 

401 

7134  402 
\begin{rail} 
12879  403 
'use' name 
7134  404 
; 
12879  405 
('ML'  MLcommand  MLsetup  'setup') text 
7134  406 
; 
12879  407 
methodsetup name '=' text text 
9199  408 
; 
7134  409 
\end{rail} 
410 

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

417 

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

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

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

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

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

426 

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

8547  430 
canonical way to initialize any objectlogic specific tools and packages 
431 
written in ML. 

9199  432 

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

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

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

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

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

438 
arguments, or a list of theorems, respectively. 

439 

440 
{\footnotesize 

441 
\begin{verbatim} 

9605  442 
Method.no_args (Method.METHOD (fn facts => foobar_tac)) 
443 
Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac)) 

10899  444 
Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac)) 
12618  445 
Method.thms_ctxt_args (fn thms => fn ctxt => 
446 
Method.METHOD (fn facts => foobar_tac)) 

9199  447 
\end{verbatim} 
448 
} 

449 

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

451 
above. Proper proof methods would do something ``appropriate'' with the list 

452 
of current facts, though. Singlerule methods usually do strict 

453 
forwardchaining (e.g.\ by using \texttt{Method.multi_resolves}), while 

454 
automatic ones just insert the facts using \texttt{Method.insert_tac} before 

455 
applying the main tactic. 

7167  456 
\end{descr} 
7134  457 

458 

8250  459 
\subsection{Syntax translation functions} 
7134  460 

8250  461 
\indexisarcmd{parseasttranslation}\indexisarcmd{parsetranslation} 
462 
\indexisarcmd{printtranslation}\indexisarcmd{typedprinttranslation} 

463 
\indexisarcmd{printasttranslation}\indexisarcmd{tokentranslation} 

464 
\begin{matharray}{rcl} 

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

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

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

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

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

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

471 
\end{matharray} 

7134  472 

9273  473 
\railalias{parseasttranslation}{parse\_ast\_translation} 
474 
\railterm{parseasttranslation} 

475 

476 
\railalias{parsetranslation}{parse\_translation} 

477 
\railterm{parsetranslation} 

478 

479 
\railalias{printtranslation}{print\_translation} 

480 
\railterm{printtranslation} 

481 

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

483 
\railterm{typedprinttranslation} 

484 

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

486 
\railterm{printasttranslation} 

487 

488 
\railalias{tokentranslation}{token\_translation} 

489 
\railterm{tokentranslation} 

490 

491 
\begin{rail} 

492 
( parseasttranslation  parsetranslation  printtranslation  typedprinttranslation  

12879  493 
printasttranslation  tokentranslation ) text 
9273  494 
\end{rail} 
495 

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

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

8379  499 
appropriate type. 
500 

501 
\begin{ttbox} 

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

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

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

505 
val typed_print_translation : 

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

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

508 
val token_translation : 

509 
(string * string * (string > string * real)) list 

510 
\end{ttbox} 

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

7134  512 

513 

514 
\subsection{Oracles} 

515 

516 
\indexisarcmd{oracle} 

517 
\begin{matharray}{rcl} 

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

519 
\end{matharray} 

520 

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

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

524 

7134  525 
\begin{rail} 
12879  526 
'oracle' name '=' text 
7134  527 
; 
528 
\end{rail} 

529 

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

7167  534 
\end{descr} 
7134  535 

536 

537 
\section{Proof commands} 

538 

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

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

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

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

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

554 
goal claimed next. 

7167  555 
\end{descr} 
7134  556 

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

559 
restricts the shape of wellformed proof texts to particular command 

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

561 
texts. Appendix~\ref{ap:refcard} gives a simplified grammar of the overall 

562 
(extensible) language emerging that way. 

7167  563 

12621  564 

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

7167  566 

7987  567 
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect} 
7895  568 
\indexisarcmd{txt}\indexisarcmd{txtraw} 
7134  569 
\begin{matharray}{rcl} 
8101  570 
\isarcmd{sect} & : & \isartrans{proof}{proof} \\ 
571 
\isarcmd{subsect} & : & \isartrans{proof}{proof} \\ 

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

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

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

7134  575 
\end{matharray} 
576 

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

580 
\railalias{txtraw}{txt\_raw} 

581 
\railterm{txtraw} 

7175  582 

7134  583 
\begin{rail} 
7895  584 
('sect'  'subsect'  'subsubsect'  'txt'  txtraw) text 
7134  585 
; 
586 
\end{rail} 

587 

588 

12621  589 
\subsection{Context elements}\label{sec:proofcontext} 
7134  590 

7315  591 
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def} 
7134  592 
\begin{matharray}{rcl} 
593 
\isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\ 

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

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

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

597 
\end{matharray} 

598 

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

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

602 
Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in 

7987  603 
a local value that may be used in the subsequent proof as any other variable 
7895  604 
or constant. Furthermore, any result $\edrv \phi[x]$ exported from the 
7987  605 
context will be universally closed wrt.\ $x$ at the outermost level: $\edrv 
606 
\All x \phi$ (this is expressed using Isabelle's metavariables). 

7315  607 

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

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

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

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

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

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

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

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

617 
user. 

7315  618 

7319  619 
Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by 
7987  620 
combining $\FIX x$ with another version of assumption that causes any 
621 
hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule. 

622 
Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$. 

7175  623 

10686  624 
\railalias{equiv}{\isasymequiv} 
625 
\railterm{equiv} 

626 

7134  627 
\begin{rail} 
12879  628 
'fix' (vars + 'and') 
7134  629 
; 
12879  630 
('assume'  'presume') (props + 'and') 
7134  631 
; 
12879  632 
'def' thmdecl? \\ name ('=='  equiv) term termpat? 
7134  633 
; 
634 
\end{rail} 

635 

7167  636 
\begin{descr} 
8547  637 
\item [$\FIX{\vec x}$] introduces local \emph{arbitrary, but fixed} variables 
638 
$\vec x$. 

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

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

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

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

7335  644 

645 
Several lists of assumptions may be given (separated by 

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

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

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

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

7167  654 
\end{descr} 
655 

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

7315  658 

7167  659 

660 
\subsection{Facts and forward chaining} 

661 

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

663 
\begin{matharray}{rcl} 

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

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

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

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

668 
\end{matharray} 

669 

7319  670 
New facts are established either by assumption or proof of local statements. 
7335  671 
Any fact will usually be involved in further proofs, either as explicit 
8547  672 
arguments of proof methods, or when forward chaining towards the next goal via 
7335  673 
$\THEN$ (and variants). Note that the special theorem name 
7987  674 
$this$\indexisarthm{this} refers to the most recently established facts. 
7167  675 
\begin{rail} 
12879  676 
'note' (thmdef? thmrefs + 'and') 
7167  677 
; 
12879  678 
('from'  'with') (thmrefs + 'and') 
7167  679 
; 
680 
\end{rail} 

681 

682 
\begin{descr} 

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

685 
right hand sides. 

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

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

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

7335  694 
\item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is 
7458  695 
equivalent to $\FROM{this}$. 
10858  696 
\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~this}$; thus the forward 
7175  697 
chaining is from earlier facts together with the current ones. 
7167  698 
\end{descr} 
699 

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

9695  703 
using something like $\FROM{\Text{\texttt{_}}~a~b}$, for example. This 
8547  704 
involves the trivial rule $\PROP\psi \Imp \PROP\psi$, which happens to be 
705 
bound in Isabelle/Pure as ``\texttt{_}'' 

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

7389  707 

9238  708 
Forward chaining with an empty list of theorems is the same as not chaining. 
709 
Thus $\FROM{nothing}$ has no effect apart from entering $prove(chain)$ mode, 

12621  710 
since $nothing$\indexisarthm{nothing} is bound to the empty list of theorems. 
9238  711 

7167  712 

713 
\subsection{Goal statements} 

714 

12618  715 
\indexisarcmd{lemma}\indexisarcmd{theorem}\indexisarcmd{corollary} 
7167  716 
\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus} 
717 
\begin{matharray}{rcl} 

12618  718 
\isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\ 
7167  719 
\isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\ 
12618  720 
\isarcmd{corollary} & : & \isartrans{theory}{proof(prove)} \\ 
7987  721 
\isarcmd{have} & : & \isartrans{proof(state) ~~ proof(chain)}{proof(prove)} \\ 
722 
\isarcmd{show} & : & \isartrans{proof(state) ~~ proof(chain)}{proof(prove)} \\ 

7167  723 
\isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\ 
724 
\isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\ 

725 
\end{matharray} 

726 

12621  727 
From a theory context, proof mode is entered by an initial goal command such 
728 
as $\LEMMANAME$, $\THEOREMNAME$, $\COROLLARYNAME$. Within a proof, new claims 

729 
may be introduced locally as well; four variants are available here to 

730 
indicate whether forward chaining of facts should be performed initially (via 

731 
$\THEN$), and whether the emerging result is meant to solve some pending goal. 

12618  732 

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

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

735 
conjunction (printed as \verb,&&,), which is automatically split into the 

736 
corresponding number of subgoals prior to any initial method application, via 

737 
$\PROOFNAME$ (\S\ref{sec:proofsteps}) or $\APPLYNAME$ 

738 
(\S\ref{sec:tacticcommands}).\footnote{Deviating from the latter principle, 

739 
the $induct$ method covered in \S\ref{sec:casesinductmeth} acts on 

740 
multiple claims simultaneously.} 

741 

7167  742 
\begin{rail} 
12621  743 
('lemma'  'theorem'  'corollary') goalprefix goal 
7167  744 
; 
745 
('have'  'show'  'hence'  'thus') goal 

746 
; 

747 

12879  748 
goal: (props + 'and') 
7167  749 
; 
12621  750 

751 
goalprefix: thmdecl? locale? context? 

752 
; 

753 
locale: '(' 'in' name ')' 

754 
; 

755 
context: '(' (contextelem +) ')' 

756 
; 

7167  757 
\end{rail} 
758 

759 
\begin{descr} 

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

762 
theory context, and optionally into the specified locale, cf.\ 

763 
\S\ref{sec:locale}. An additional \railnonterm{context} specification may 

764 
build an initial proof context for the subsequent claim; this may include 

12621  765 
local definitions and syntax as well, see the definition of $contextelem$ in 
766 
\S\ref{sec:locale}. 

12618  767 

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

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

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

771 

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

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

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

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

776 
results within a proof body. 

777 

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

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

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

781 
subproof that the $\SHOWNAME$ command belongs to). 

782 

783 
To accommodate interactive debugging, resulting rules are printed before 

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

785 
predicts potential failure after finishing its proof, and displays the 

786 
resulting error message as a warning beforehand, adding this header: 

787 

788 
\begin{ttbox} 

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

790 
\end{ttbox} 

791 

7895  792 
\item [$\HENCENAME$] abbreviates $\THEN~\HAVENAME$, i.e.\ claims a local goal 
793 
to be proven by forward chaining the current facts. Note that $\HENCENAME$ 

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

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

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

7167  797 
\end{descr} 
798 

10550  799 
Any goal statement causes some term abbreviations (such as $\Var{thesis}$, 
800 
$\dots$) to be bound automatically, see also \S\ref{sec:termabbrev}. 

11549  801 
Furthermore, the local context of a (nonatomic) goal is provided via the 
12618  802 
$rule_context$\indexisarcase{rulecontext} case, see also 
803 
\S\ref{sec:rulecases}. 

10550  804 

805 
\medskip 

806 

807 
\begin{warn} 

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

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

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

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

812 
behavior of the actual proof methods applied during the reasoning. Note 

813 
that most semiautomated methods heavily depend on several kinds of implicit 

814 
rule declarations within the current theory context. As this would also 

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

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

818 
by stepwise refinement via emulation of traditional Isabelle tactic scripts 

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

820 
they are doing. 

10550  821 
\end{warn} 
8991  822 

7167  823 

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

825 

7175  826 
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by} 
827 
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry} 

828 
\begin{matharray}{rcl} 

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

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

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

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

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

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

835 
\end{matharray} 

836 

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

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

7167  846 
\end{enumerate} 
847 

12621  848 
The only other proper way to affect pending goals in a proof body is by 
849 
$\SHOWNAME$, which involves an explicit statement of what is to be solved 

850 
eventually. Thus we avoid the fundamental problem of unstructured tactic 

851 
scripts that consist of numerous consecutive goal transformations, with 

852 
invisible effects. 

7167  853 

7175  854 
\medskip 
855 

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

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

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

860 
document in any intelligible way. 

7175  861 

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

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

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

7167  866 

867 
\begin{rail} 

12879  868 
'proof' method? 
7167  869 
; 
12879  870 
'qed' method? 
7167  871 
; 
12879  872 
'by' method method? 
7167  873 
; 
12879  874 
('.'  '..'  'sorry') 
7167  875 
; 
876 
\end{rail} 

877 

878 
\begin{descr} 

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

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

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

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

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

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

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

888 
context. Debugging such a situation might involve temporarily changing 

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

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

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

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

7895  894 
by expanding its definition; in many cases $\PROOF{m@1}$ is already 
7175  895 
sufficient to see what is going wrong. 
7895  896 
\item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it 
8515  897 
abbreviates $\BY{rule}$. 
7895  898 
\item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it 
8195  899 
abbreviates $\BY{this}$. 
12618  900 
\item [$\SORRY$] is a \emph{fake proof}\index{proof!fake} pretending to solve 
901 
the pending claim without further ado. This only works in interactive 

902 
development, or if the \texttt{quick_and_dirty} flag is enabled. Certainly, 

903 
any facts emerging from fake proofs are not the real thing. Internally, 

904 
each theorem container is tainted by an oracle invocation, which is 

905 
indicated as ``$[!]$'' in the printed result. 

906 

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

908 
topdown proof development in a simple manner. 

8515  909 
\end{descr} 
910 

911 

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

913 

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

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

12621  917 
\ref{ch:logics}). 
8515  918 

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

920 
\indexisaratt{OF}\indexisaratt{of} 

12621  921 
\indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim} 
922 
\indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule} 

8515  923 
\begin{matharray}{rcl} 
924 
assumption & : & \isarmeth \\ 

925 
this & : & \isarmeth \\ 

926 
rule & : & \isarmeth \\ 

927 
 & : & \isarmeth \\ 

928 
OF & : & \isaratt \\ 

929 
of & : & \isaratt \\ 

930 
intro & : & \isaratt \\ 

931 
elim & : & \isaratt \\ 

932 
dest & : & \isaratt \\ 

9936  933 
rule & : & \isaratt \\ 
8515  934 
\end{matharray} 
935 

12621  936 
%FIXME intro!, intro, intro? 
937 

8515  938 
\begin{rail} 
8547  939 
'rule' thmrefs? 
8515  940 
; 
941 
'OF' thmrefs 

942 
; 

8693  943 
'of' insts ('concl' ':' insts)? 
8515  944 
; 
9936  945 
'rule' 'del' 
946 
; 

8515  947 
\end{rail} 
948 

949 
\begin{descr} 

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

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

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

953 
remaining subgoals by assumption. 

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

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

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

959 
becomes \emph{elimination}. 

960 

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

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

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

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

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

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

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

970 
alone. 

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

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

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

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

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

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

979 
conclusion of a rule. 

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

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

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

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

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

985 
confusion! 

9936  986 
\item [$rule~del$] undeclares introduction, elimination, or destruct rules. 
7315  987 
\end{descr} 
988 

989 

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

991 

992 
\indexisarcmd{let} 

993 
\begin{matharray}{rcl} 

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

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

996 
\end{matharray} 

997 

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

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

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

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

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

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

1005 
postfix position. 

7315  1006 

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

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

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

1011 
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

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

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

1014 

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

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

1016 

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

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

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

1021 
does not support polymorphism. 
7315  1022 

1023 
\begin{rail} 

12879  1024 
'let' ((term + 'and') '=' term + 'and') 
7315  1025 
; 
1026 
\end{rail} 

1027 

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

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

1031 
\begin{descr} 

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

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

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

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

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

1037 
\end{descr} 

1038 

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

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

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

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

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

1047 
application of the latter are calculational proofs (see 

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

1049 

7315  1050 

7134  1051 
\subsection{Block structure} 
1052 

8896  1053 
\indexisarcmd{next}\indexisarcmd{\{}\indexisarcmd{\}} 
7397  1054 
\begin{matharray}{rcl} 
8448  1055 
\NEXT & : & \isartrans{proof(state)}{proof(state)} \\ 
7974  1056 
\BG & : & \isartrans{proof(state)}{proof(state)} \\ 
1057 
\EN & : & \isartrans{proof(state)}{proof(state)} \\ 

7397  1058 
\end{matharray} 
1059 

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

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

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

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

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

1067 
here! 

7167  1068 

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

1072 
\begin{descr} 

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

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

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

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

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

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

7167  1082 
\end{descr} 
7134  1083 

1084 

9605  1085 
\subsection{Emulating tactic scripts}\label{sec:tacticcommands} 
8515  1086 

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

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

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

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

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

1093 
used in scripts, too. 

8515  1094 

9605  1095 
\indexisarcmd{apply}\indexisarcmd{applyend}\indexisarcmd{done} 
8515  1096 
\indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back} 
9605  1097 
\indexisarcmd{declare} 
8515  1098 
\begin{matharray}{rcl} 
8533  1099 
\isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\ 
9605  1100 
\isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\ 
8946  1101 
\isarcmd{done}^* & : & \isartrans{proof(prove)}{proof(state)} \\ 
8533  1102 
\isarcmd{defer}^* & : & \isartrans{proof}{proof} \\ 
1103 
\isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\ 

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

9605  1105 
\isarcmd{declare}^* & : & \isartrans{theory}{theory} \\ 
8515  1106 
\end{matharray} 
1107 

1108 
\railalias{applyend}{apply\_end} 

1109 
\railterm{applyend} 

1110 

1111 
\begin{rail} 

12879  1112 
( 'apply'  applyend ) method 
8515  1113 
; 
12879  1114 
'defer' nat? 
8515  1115 
; 
12879  1116 
'prefer' nat 
8515  1117 
; 
12879  1118 
'declare' thmrefs 
9605  1119 
; 
8515  1120 
\end{rail} 
1121 

1122 
\begin{descr} 

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

1125 
applications may be given just as in tactic scripts. 

8515  1126 

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

8946  1130 

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

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

1134 

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

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

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

9605  1138 

1139 
\item [$\isarkeyword{done}$] completes a proof script, provided that the 

1140 
current goal state is already solved completely. Note that actual 

1141 
structured proof commands (e.g.\ ``$\DOT$'' or $\SORRY$) may be used to 

1142 
conclude proof scripts as well. 

1143 

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

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

9605  1147 

8515  1148 
\item [$\isarkeyword{back}$] does backtracking over the result sequence of 
1149 
the latest proof command.\footnote{Unlike the ML function \texttt{back} 

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

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

9605  1152 

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

1154 
context. No theorem binding is involved here, unlike 

1155 
$\isarkeyword{theorems}$ or $\isarkeyword{lemmas}$ (cf.\ 

1156 
\S\ref{sec:axmsthms}). So $\isarkeyword{declare}$ only has the effect of 

1157 
applying attributes as included in the theorem specification. 

9006  1158 
\end{descr} 
1159 

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

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

9006  1163 

8515  1164 

1165 
\subsection{Metalinguistic features} 

1166 

1167 
\indexisarcmd{oops} 

1168 
\begin{matharray}{rcl} 

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

1170 
\end{matharray} 

1171 

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

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

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

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

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

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

1178 
proof anyhow. 

1179 

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

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

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

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

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

1185 
``$\OOPS$'' keyword. 

1186 

12618  1187 
\medskip The $\OOPS$ command is undoable, unlike $\isarkeyword{kill}$ (see 
8547  1188 
\S\ref{sec:history}). The effect is to get back to the theory \emph{before} 
1189 
the opening of the proof. 

8515  1190 

1191 

7134  1192 
\section{Other commands} 
1193 

9605  1194 
\subsection{Diagnostics} 
7134  1195 

10858  1196 
\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term} 
1197 
\indexisarcmd{prop}\indexisarcmd{typ} 

7134  1198 
\begin{matharray}{rcl} 
8515  1199 
\isarcmd{pr}^* & : & \isarkeep{\cdot} \\ 
1200 
\isarcmd{thm}^* & : & \isarkeep{theory~~proof} \\ 

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

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

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

7134  1204 
\end{matharray} 
1205 

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

7335  1208 

7134  1209 
\begin{rail} 
9727  1210 
'pr' modes? nat? (',' nat)? 
7134  1211 
; 
12879  1212 
'thm' modes? thmrefs 
8485  1213 
; 
12879  1214 
'term' modes? term 
7134  1215 
; 
12879  1216 
'prop' modes? prop 
7134  1217 
; 
12879  1218 
'typ' modes? type 
8485  1219 
; 
1220 

1221 
modes: '(' (name + ) ')' 

7134  1222 
; 
1223 
\end{rail} 

1224 

7167  1225 
\begin{descr} 
9727  1226 
\item [$\isarkeyword{pr}~goals, prems$] prints the current proof state (if 
1227 
present), including the proof context, current facts and goals. The 

1228 
optional limit arguments affect the number of goals and premises to be 

1229 
displayed, which is initially 10 for both. Omitting limit values leaves the 

1230 
current setting unchanged. 

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

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

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

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

1240 
abbreviations. 

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

9605  1243 
\end{descr} 
1244 

1245 
All of the diagnostic commands above admit a list of $modes$ to be specified, 

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

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

1248 
features. For example, $\isarkeyword{pr}~(latex~xsymbols~symbols)$ would 

1249 
print the current proof state with mathematical symbols and special characters 

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

1251 
\cite{isabellesys}. 

1252 

1253 
Note that antiquotations (cf.\ \S\ref{sec:antiq}) provide a more systematic 

1254 
way to include formal items into the printed text document. 

1255 

1256 

1257 
\subsection{Inspecting the context} 

1258 

1259 
\indexisarcmd{printfacts}\indexisarcmd{printbinds} 

1260 
\indexisarcmd{printcommands}\indexisarcmd{printsyntax} 

1261 
\indexisarcmd{printmethods}\indexisarcmd{printattributes} 

10858  1262 
\indexisarcmd{thmscontaining}\indexisarcmd{thmdeps} 
1263 
\indexisarcmd{printtheorems} 

9605  1264 
\begin{matharray}{rcl} 
1265 
\isarcmd{print_commands}^* & : & \isarkeep{\cdot} \\ 

1266 
\isarcmd{print_syntax}^* & : & \isarkeep{theory~~proof} \\ 

1267 
\isarcmd{print_methods}^* & : & \isarkeep{theory~~proof} \\ 

1268 
\isarcmd{print_attributes}^* & : & \isarkeep{theory~~proof} \\ 

10858  1269 
\isarcmd{print_theorems}^* & : & \isarkeep{theory~~proof} \\ 
1270 
\isarcmd{thms_containing}^* & : & \isarkeep{theory~~proof} \\ 

1271 
\isarcmd{thms_deps}^* & : & \isarkeep{theory~~proof} \\ 

9605  1272 
\isarcmd{print_facts}^* & : & \isarkeep{proof} \\ 
1273 
\isarcmd{print_binds}^* & : & \isarkeep{proof} \\ 

1274 
\end{matharray} 

1275 

10858  1276 
\railalias{thmscontaining}{thms\_containing} 
1277 
\railterm{thmscontaining} 

1278 

1279 
\railalias{thmdeps}{thm\_deps} 

1280 
\railterm{thmdeps} 

1281 

1282 
\begin{rail} 

11017  1283 
thmscontaining (term * ) 
10858  1284 
; 
1285 
thmdeps thmrefs 

1286 
; 

1287 
\end{rail} 

1288 

1289 
These commands print certain parts of the theory and proof context. Note that 

1290 
there are some further ones available, such as for the set of rules declared 

1291 
for simplifications. 

9605  1292 

1293 
\begin{descr} 

1294 
\item [$\isarkeyword{print_commands}$] prints Isabelle's outer theory syntax, 

1295 
including keywords and command. 

1296 
\item [$\isarkeyword{print_syntax}$] prints the inner syntax of types and 

1297 
terms, depending on the current context. The output can be very verbose, 

1298 
including grammar tables and syntax translation rules. See \cite[\S7, 

1299 
\S8]{isabelleref} for further information on Isabelle's inner syntax. 

10858  1300 
\item [$\isarkeyword{print_methods}$] prints all proof methods available in 
1301 
the current theory context. 

1302 
\item [$\isarkeyword{print_attributes}$] prints all attributes available in 

1303 
the current theory context. 

1304 
\item [$\isarkeyword{print_theorems}$] prints theorems available in the 

1305 
current theory context. In interactive mode this actually refers to the 

1306 
theorems left by the last transaction; this allows to inspect the result of 

1307 
advanced definitional packages, such as $\isarkeyword{datatype}$. 

11017  1308 
\item [$\isarkeyword{thms_containing}~\vec t$] retrieves theorems from the 
1309 
theory context containing all of the constants occurring in the terms $\vec 

1310 
t$. Note that giving the empty list yields \emph{all} theorems of the 
