author  wenzelm 
Thu, 03 Jan 2002 17:48:02 +0100  
changeset 12621  48cafea0684b 
parent 12618  43a97a2155d0 
child 12879  8e1cae1de136 
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 

12621  8 
Isabelle or preinstalled by most object logics. Chapter~\ref{ch:logics} 
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} 

7167  165 
'classes' (classdecl comment? +) 
7134  166 
; 
11100
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11017
diff
changeset

167 
'classrel' nameref ('<'  subseteq) nameref comment? 
7134  168 
; 
169 
'defaultsort' sort comment? 

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} 

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

199 
; 

200 
'typedecl' typespec infix? comment? 

201 
; 

202 
'nonterminals' (name +) comment? 

203 
; 

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

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 
; 

9308  239 
'defs' ('(overloaded)')? (axmdecl prop comment? +) 
7134  240 
; 
241 
'constdefs' (constdecl prop comment? +) 

242 
; 

243 

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

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 
; 
10640  287 
'translations' (transpat ('=='  '=>'  '<='  rightleftharpoons  rightharpoonup  leftharpoondown) transpat comment? +) 
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} 

7135  320 
'axioms' (axmdecl prop comment? +) 
7134  321 
; 
12618  322 
('lemmas'  'theorems') (thmdef? thmrefs comment? + '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} 
352 
'global' comment? 

353 
; 

354 
'local' comment? 

355 
; 

356 
'hide' name (nameref + ) comment? 

357 
; 

358 
\end{rail} 

359 

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

7175  364 

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

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

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

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

8726  371 

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

373 
qualified names of the same base name are introduced. 

374 

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

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

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

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

12621  379 
full internal name. Unqualified (global) names may not be hidden. 
7167  380 
\end{descr} 
7134  381 

382 

7167  383 
\subsection{Incorporating ML code}\label{sec:ML} 
7134  384 

8682  385 
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{MLcommand} 
386 
\indexisarcmd{MLsetup}\indexisarcmd{setup} 

9199  387 
\indexisarcmd{methodsetup} 
7134  388 
\begin{matharray}{rcl} 
389 
\isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\ 

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

8682  391 
\isarcmd{ML_command} & : & \isartrans{\cdot}{\cdot} \\ 
7895  392 
\isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\ 
7175  393 
\isarcmd{setup} & : & \isartrans{theory}{theory} \\ 
9199  394 
\isarcmd{method_setup} & : & \isartrans{theory}{theory} \\ 
7134  395 
\end{matharray} 
396 

7895  397 
\railalias{MLsetup}{ML\_setup} 
398 
\railterm{MLsetup} 

399 

9199  400 
\railalias{methodsetup}{method\_setup} 
401 
\railterm{methodsetup} 

402 

8682  403 
\railalias{MLcommand}{ML\_command} 
404 
\railterm{MLcommand} 

405 

7134  406 
\begin{rail} 
9273  407 
'use' name comment? 
7134  408 
; 
9273  409 
('ML'  MLcommand  MLsetup  'setup') text comment? 
7134  410 
; 
9199  411 
methodsetup name '=' text text comment? 
412 
; 

7134  413 
\end{rail} 
414 

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

421 

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

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

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

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

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

430 

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

8547  434 
canonical way to initialize any objectlogic specific tools and packages 
435 
written in ML. 

9199  436 

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

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

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

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

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

442 
arguments, or a list of theorems, respectively. 

443 

444 
{\footnotesize 

445 
\begin{verbatim} 

9605  446 
Method.no_args (Method.METHOD (fn facts => foobar_tac)) 
447 
Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac)) 

10899  448 
Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac)) 
12618  449 
Method.thms_ctxt_args (fn thms => fn ctxt => 
450 
Method.METHOD (fn facts => foobar_tac)) 

9199  451 
\end{verbatim} 
452 
} 

453 

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

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

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

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

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

459 
applying the main tactic. 

7167  460 
\end{descr} 
7134  461 

462 

8250  463 
\subsection{Syntax translation functions} 
7134  464 

8250  465 
\indexisarcmd{parseasttranslation}\indexisarcmd{parsetranslation} 
466 
\indexisarcmd{printtranslation}\indexisarcmd{typedprinttranslation} 

467 
\indexisarcmd{printasttranslation}\indexisarcmd{tokentranslation} 

468 
\begin{matharray}{rcl} 

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

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

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

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

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

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

475 
\end{matharray} 

7134  476 

9273  477 
\railalias{parseasttranslation}{parse\_ast\_translation} 
478 
\railterm{parseasttranslation} 

479 

480 
\railalias{parsetranslation}{parse\_translation} 

481 
\railterm{parsetranslation} 

482 

483 
\railalias{printtranslation}{print\_translation} 

484 
\railterm{printtranslation} 

485 

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

487 
\railterm{typedprinttranslation} 

488 

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

490 
\railterm{printasttranslation} 

491 

492 
\railalias{tokentranslation}{token\_translation} 

493 
\railterm{tokentranslation} 

494 

495 
\begin{rail} 

496 
( parseasttranslation  parsetranslation  printtranslation  typedprinttranslation  

497 
printasttranslation  tokentranslation ) text comment? 

498 
\end{rail} 

499 

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

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

8379  503 
appropriate type. 
504 

505 
\begin{ttbox} 

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

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

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

509 
val typed_print_translation : 

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

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

512 
val token_translation : 

513 
(string * string * (string > string * real)) list 

514 
\end{ttbox} 

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

7134  516 

517 

518 
\subsection{Oracles} 

519 

520 
\indexisarcmd{oracle} 

521 
\begin{matharray}{rcl} 

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

523 
\end{matharray} 

524 

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

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

528 

7134  529 
\begin{rail} 
530 
'oracle' name '=' text comment? 

531 
; 

532 
\end{rail} 

533 

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

7167  538 
\end{descr} 
7134  539 

540 

541 
\section{Proof commands} 

542 

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

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

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

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

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

558 
goal claimed next. 

7167  559 
\end{descr} 
7134  560 

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

563 
restricts the shape of wellformed proof texts to particular command 

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

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

566 
(extensible) language emerging that way. 

7167  567 

12621  568 

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

7167  570 

7987  571 
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect} 
7895  572 
\indexisarcmd{txt}\indexisarcmd{txtraw} 
7134  573 
\begin{matharray}{rcl} 
8101  574 
\isarcmd{sect} & : & \isartrans{proof}{proof} \\ 
575 
\isarcmd{subsect} & : & \isartrans{proof}{proof} \\ 

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

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

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

7134  579 
\end{matharray} 
580 

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

584 
\railalias{txtraw}{txt\_raw} 

585 
\railterm{txtraw} 

7175  586 

7134  587 
\begin{rail} 
7895  588 
('sect'  'subsect'  'subsubsect'  'txt'  txtraw) text 
7134  589 
; 
590 
\end{rail} 

591 

592 

12621  593 
\subsection{Context elements}\label{sec:proofcontext} 
7134  594 

7315  595 
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def} 
7134  596 
\begin{matharray}{rcl} 
597 
\isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\ 

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

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

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

601 
\end{matharray} 

602 

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

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

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

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

7315  611 

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

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

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

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

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

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

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

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

621 
user. 

7315  622 

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

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

7175  627 

10686  628 
\railalias{equiv}{\isasymequiv} 
629 
\railterm{equiv} 

630 

7134  631 
\begin{rail} 
12618  632 
'fix' (vars comment? + 'and') 
7134  633 
; 
12618  634 
('assume'  'presume') (props comment? + 'and') 
7134  635 
; 
10686  636 
'def' thmdecl? \\ name ('=='  equiv) term termpat? comment? 
7134  637 
; 
638 
\end{rail} 

639 

7167  640 
\begin{descr} 
8547  641 
\item [$\FIX{\vec x}$] introduces local \emph{arbitrary, but fixed} variables 
642 
$\vec x$. 

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

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

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

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

7335  648 

649 
Several lists of assumptions may be given (separated by 

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

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

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

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

7167  658 
\end{descr} 
659 

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

7315  662 

7167  663 

664 
\subsection{Facts and forward chaining} 

665 

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

667 
\begin{matharray}{rcl} 

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

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

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

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

672 
\end{matharray} 

673 

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

683 
; 

9199  684 
('from'  'with') (thmrefs comment? + 'and') 
7167  685 
; 
686 
\end{rail} 

687 

688 
\begin{descr} 

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

691 
right hand sides. 

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

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

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

7335  700 
\item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is 
7458  701 
equivalent to $\FROM{this}$. 
10858  702 
\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~this}$; thus the forward 
7175  703 
chaining is from earlier facts together with the current ones. 
7167  704 
\end{descr} 
705 

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

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

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

7389  713 

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

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

7167  718 

719 
\subsection{Goal statements} 

720 

12618  721 
\indexisarcmd{lemma}\indexisarcmd{theorem}\indexisarcmd{corollary} 
7167  722 
\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus} 
723 
\begin{matharray}{rcl} 

12618  724 
\isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\ 
7167  725 
\isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\ 
12618  726 
\isarcmd{corollary} & : & \isartrans{theory}{proof(prove)} \\ 
7987  727 
\isarcmd{have} & : & \isartrans{proof(state) ~~ proof(chain)}{proof(prove)} \\ 
728 
\isarcmd{show} & : & \isartrans{proof(state) ~~ proof(chain)}{proof(prove)} \\ 

7167  729 
\isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\ 
730 
\isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\ 

731 
\end{matharray} 

732 

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

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

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

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

12618  738 

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

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

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

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

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

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

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

746 
multiple claims simultaneously.} 

747 

7167  748 
\begin{rail} 
12621  749 
('lemma'  'theorem'  'corollary') goalprefix goal 
7167  750 
; 
751 
('have'  'show'  'hence'  'thus') goal 

752 
; 

753 

12618  754 
goal: (props comment? + 'and') 
7167  755 
; 
12621  756 

757 
goalprefix: thmdecl? locale? context? 

758 
; 

759 
locale: '(' 'in' name ')' 

760 
; 

761 
context: '(' (contextelem +) ')' 

762 
; 

7167  763 
\end{rail} 
764 

765 
\begin{descr} 

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

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

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

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

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

12618  773 

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

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

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

777 

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

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

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

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

782 
results within a proof body. 

783 

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

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

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

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

788 

789 
To accommodate interactive debugging, resulting rules are printed before 

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

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

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

793 

794 
\begin{ttbox} 

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

796 
\end{ttbox} 

797 

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

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

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

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

7167  803 
\end{descr} 
804 

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

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

10550  810 

811 
\medskip 

812 

813 
\begin{warn} 

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

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

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

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

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

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

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

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

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

824 
by stepwise refinement via emulation of traditional Isabelle tactic scripts 

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

826 
they are doing. 

10550  827 
\end{warn} 
8991  828 

7167  829 

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

831 

7175  832 
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by} 
833 
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry} 

834 
\begin{matharray}{rcl} 

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

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

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

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

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

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

841 
\end{matharray} 

842 

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

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

7167  852 
\end{enumerate} 
853 

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

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

857 
scripts that consist of numerous consecutive goal transformations, with 

858 
invisible effects. 

7167  859 

7175  860 
\medskip 
861 

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

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

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

866 
document in any intelligible way. 

7175  867 

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

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

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

7167  872 

873 
\begin{rail} 

874 
'proof' interest? meth? comment? 

875 
; 

876 
'qed' meth? comment? 

877 
; 

878 
'by' meth meth? comment? 

879 
; 

880 
('.'  '..'  'sorry') comment? 

881 
; 

882 

883 
meth: method interest? 

884 
; 

885 
\end{rail} 

886 

887 
\begin{descr} 

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

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

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

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

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

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

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

897 
context. Debugging such a situation might involve temporarily changing 

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

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

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

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

7895  903 
by expanding its definition; in many cases $\PROOF{m@1}$ is already 
7175  904 
sufficient to see what is going wrong. 
7895  905 
\item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it 
8515  906 
abbreviates $\BY{rule}$. 
7895  907 
\item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it 
8195  908 
abbreviates $\BY{this}$. 
12618  909 
\item [$\SORRY$] is a \emph{fake proof}\index{proof!fake} pretending to solve 
910 
the pending claim without further ado. This only works in interactive 

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

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

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

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

915 

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

917 
topdown proof development in a simple manner. 

8515  918 
\end{descr} 
919 

920 

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

922 

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

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

12621  926 
\ref{ch:logics}). 
8515  927 

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

929 
\indexisaratt{OF}\indexisaratt{of} 

12621  930 
\indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim} 
931 
\indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule} 

8515  932 
\begin{matharray}{rcl} 
933 
assumption & : & \isarmeth \\ 

934 
this & : & \isarmeth \\ 

935 
rule & : & \isarmeth \\ 

936 
 & : & \isarmeth \\ 

937 
OF & : & \isaratt \\ 

938 
of & : & \isaratt \\ 

939 
intro & : & \isaratt \\ 

940 
elim & : & \isaratt \\ 

941 
dest & : & \isaratt \\ 

9936  942 
rule & : & \isaratt \\ 
8515  943 
\end{matharray} 
944 

12621  945 
%FIXME intro!, intro, intro? 
946 

8515  947 
\begin{rail} 
8547  948 
'rule' thmrefs? 
8515  949 
; 
950 
'OF' thmrefs 

951 
; 

8693  952 
'of' insts ('concl' ':' insts)? 
8515  953 
; 
9936  954 
'rule' 'del' 
955 
; 

8515  956 
\end{rail} 
957 

958 
\begin{descr} 

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

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

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

962 
remaining subgoals by assumption. 

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

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

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

968 
becomes \emph{elimination}. 

969 

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

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

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

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

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

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

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

979 
alone. 

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

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

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

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

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

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

988 
conclusion of a rule. 

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

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

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

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

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

994 
confusion! 

9936  995 
\item [$rule~del$] undeclares introduction, elimination, or destruct rules. 
7315  996 
\end{descr} 
997 

998 

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

1000 

1001 
\indexisarcmd{let} 

1002 
\begin{matharray}{rcl} 

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

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

1005 
\end{matharray} 

1006 

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

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

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

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

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

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

1014 
postfix position. 

7315  1015 

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

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

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

1020 
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

1021 
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

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

1023 

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

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

1025 

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

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

1029 
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

1030 
does not support polymorphism. 
7315  1031 

1032 
\begin{rail} 

8664  1033 
'let' ((term + 'and') '=' term comment? + 'and') 
7315  1034 
; 
1035 
\end{rail} 

1036 

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

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

1040 
\begin{descr} 

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

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

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

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

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

1046 
\end{descr} 

1047 

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

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

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

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

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

1056 
application of the latter are calculational proofs (see 

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

1058 

7315  1059 

7134  1060 
\subsection{Block structure} 
1061 

8896  1062 
\indexisarcmd{next}\indexisarcmd{\{}\indexisarcmd{\}} 
7397  1063 
\begin{matharray}{rcl} 
8448  1064 
\NEXT & : & \isartrans{proof(state)}{proof(state)} \\ 
7974  1065 
\BG & : & \isartrans{proof(state)}{proof(state)} \\ 
1066 
\EN & : & \isartrans{proof(state)}{proof(state)} \\ 

7397  1067 
\end{matharray} 
1068 

9030  1069 
\railalias{lbrace}{\ttlbrace} 
1070 
\railterm{lbrace} 

1071 

1072 
\railalias{rbrace}{\ttrbrace} 

1073 
\railterm{rbrace} 

1074 

1075 
\begin{rail} 

1076 
'next' comment? 

1077 
; 

1078 
lbrace comment? 

1079 
; 

1080 
rbrace comment? 

1081 
; 

1082 
\end{rail} 

1083 

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

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

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

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

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

1091 
here! 

7167  1092 

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

1096 
\begin{descr} 

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

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

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

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

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

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

7167  1106 
\end{descr} 
7134  1107 

1108 

9605  1109 
\subsection{Emulating tactic scripts}\label{sec:tacticcommands} 
8515  1110 

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

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

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

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

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

1117 
used in scripts, too. 

8515  1118 

9605  1119 
\indexisarcmd{apply}\indexisarcmd{applyend}\indexisarcmd{done} 
8515  1120 
\indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back} 
9605  1121 
\indexisarcmd{declare} 
8515  1122 
\begin{matharray}{rcl} 
8533  1123 
\isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\ 
9605  1124 
\isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\ 
8946  1125 
\isarcmd{done}^* & : & \isartrans{proof(prove)}{proof(state)} \\ 
8533  1126 
\isarcmd{defer}^* & : & \isartrans{proof}{proof} \\ 
1127 
\isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\ 

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

9605  1129 
\isarcmd{declare}^* & : & \isartrans{theory}{theory} \\ 
8515  1130 
\end{matharray} 
1131 

1132 
\railalias{applyend}{apply\_end} 

1133 
\railterm{applyend} 

1134 

1135 
\begin{rail} 

9605  1136 
( 'apply'  applyend ) method comment? 
8515  1137 
; 
8946  1138 
'done' comment? 
1139 
; 

8682  1140 
'defer' nat? comment? 
8515  1141 
; 
8682  1142 
'prefer' nat comment? 
8515  1143 
; 
9273  1144 
'back' comment? 
1145 
; 

9605  1146 
'declare' thmrefs comment? 
1147 
; 

8515  1148 
\end{rail} 
1149 

1150 
\begin{descr} 

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

1153 
applications may be given just as in tactic scripts. 

8515  1154 

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

8946  1158 

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

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

1162 

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

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

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

9605  1166 

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

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

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

1170 
conclude proof scripts as well. 

1171 

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

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

9605  1175 

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

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

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

9605  1180 

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

1182 
context. No theorem binding is involved here, unlike 

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

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

1185 
applying attributes as included in the theorem specification. 

9006  1186 
\end{descr} 
1187 

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

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

9006  1191 

8515  1192 

1193 
\subsection{Metalinguistic features} 

1194 

1195 
\indexisarcmd{oops} 

1196 
\begin{matharray}{rcl} 

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

1198 
\end{matharray} 

1199 

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

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

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

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

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

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

1206 
proof anyhow. 

1207 

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

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

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

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

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

1213 
``$\OOPS$'' keyword. 

1214 

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

8515  1218 

1219 

7134  1220 
\section{Other commands} 
1221 

9605  1222 
\subsection{Diagnostics} 
7134  1223 

10858  1224 
\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term} 
1225 
\indexisarcmd{prop}\indexisarcmd{typ} 

7134  1226 
\begin{matharray}{rcl} 
8515  1227 
\isarcmd{pr}^* & : & \isarkeep{\cdot} \\ 
1228 
\isarcmd{thm}^* & : & \isarkeep{theory~~proof} \\ 

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

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

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

7134  1232 
\end{matharray} 
1233 

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

7335  1236 

7134  1237 
\begin{rail} 
9727  1238 
'pr' modes? nat? (',' nat)? 
7134  1239 
; 
10584  1240 
'thm' modes? thmrefs comment? 
8485  1241 
; 
10584  1242 
'term' modes? term comment? 
7134  1243 
; 
10584  1244 
'prop' modes? prop comment? 
7134  1245 
; 
10584  1246 
'typ' modes? type comment? 
8485  1247 
; 
1248 

1249 
modes: '(' (name + ) ')' 

7134  1250 
; 
1251 
\end{rail} 

1252 

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

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

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

1258 
current setting unchanged. 

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

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

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

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

1268 
abbreviations. 

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

9605  1271 
\end{descr} 
1272 

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

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

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

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

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

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

1279 
\cite{isabellesys}. 

1280 

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

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

1283 

1284 

1285 
\subsection{Inspecting the context} 

1286 

1287 
\indexisarcmd{printfacts}\indexisarcmd{printbinds} 

1288 
\indexisarcmd{printcommands}\indexisarcmd{printsyntax} 

1289 
\indexisarcmd{printmethods}\indexisarcmd{printattributes} 

10858  1290 
\indexisarcmd{thmscontaining}\indexisarcmd{thmdeps} 
1291 
\indexisarcmd{printtheorems} 

9605  1292 
\begin{matharray}{rcl} 
1293 
\isarcmd{print_commands}^* & : & \isarkeep{\cdot} \\ 

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

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

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

10858  1297 
\isarcmd{print_theorems}^* & : & \isarkeep{theory~~proof} \\ 
1298 
\isarcmd{thms_containing}^* & : & \isarkeep{theory~~proof} \\ 

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

9605  1300 
\isarcmd{print_facts}^* & : & \isarkeep{proof} \\ 
1301 
\isarcmd{print_binds}^* & : & \isarkeep{proof} \\ 

1302 
\end{matharray} 

1303 

10858  1304 
\railalias{thmscontaining}{thms\_containing} 
1305 
\railterm{thmscontaining} 

1306 

1307 
\railalias{thmdeps}{thm\_deps} 

1308 
\railterm{thmdeps} 

1309 

1310 
\begin{rail} 

11017  1311 
thmscontaining (term * ) 
10858  1312 
; 
1313 
thmdeps thmrefs 
