2 \chapter{Basic Isar Language Elements}\label{ch:pure-syntax}
4 Subsequently, we introduce the main part of Pure Isar theory and proof
5 commands, together with fundamental proof methods and attributes.
6 Chapter~\ref{ch:gen-tools} describes further Isar elements provided by generic
7 tools and packages (such as the Simplifier) that are either part of Pure
8 Isabelle or pre-installed by most object logics. Chapter~\ref{ch:hol-tools}
9 refers to actual object-logic specific elements of Isabelle/HOL.
13 Isar commands may be either \emph{proper} document constructors, or
14 \emph{improper commands}. Some proof methods and attributes introduced later
15 are classified as improper as well. Improper Isar language elements, which
16 are subsequently marked by $^*$, are often helpful when developing proof
17 documents, while their use is discouraged for the final outcome. Typical
18 examples are diagnostic commands that print terms or theorems according to the
19 current context; other commands even emulate old-style tactical theorem
23 \section{Theory commands}
25 \subsection{Defining theories}\label{sec:begin-thy}
27 \indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context}
28 \begin{matharray}{rcl}
29 \isarcmd{header} & : & \isarkeep{toplevel} \\
30 \isarcmd{theory} & : & \isartrans{toplevel}{theory} \\
31 \isarcmd{context}^* & : & \isartrans{toplevel}{theory} \\
32 \isarcmd{end} & : & \isartrans{theory}{toplevel} \\
35 Isabelle/Isar ``new-style'' theories are either defined via theory files or
36 interactively. Both theory-level specifications and proofs are handled
37 uniformly --- occasionally definitional mechanisms even require some explicit
38 proof as well. In contrast, ``old-style'' Isabelle theories support batch
39 processing only, with the proof scripts collected in separate ML files.
41 The first actual command of any theory has to be $\THEORY$, starting a new
42 theory based on the merge of existing ones. Just preceding $\THEORY$, there
43 may be an optional $\isarkeyword{header}$ declaration, which is relevant to
44 document preparation only; it acts very much like a special pre-theory markup
45 command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}). The theory
46 context may be also changed by $\CONTEXT$ without creating a new theory. In
47 both cases, $\END$ concludes the theory development; it has to be the very
48 last command of any theory file.
53 'theory' name '=' (name + '+') filespecs? ':'
60 filespecs: 'files' ((name | parname) +);
64 \item [$\isarkeyword{header}~text$] provides plain text markup just preceding
65 the formal beginning of a theory. In actual document preparation the
66 corresponding {\LaTeX} macro \verb,\isamarkupheader, may be redefined to
67 produce chapter or section headings. See also \S\ref{sec:markup-thy} and
68 \S\ref{sec:markup-prf} for further markup commands.
70 \item [$\THEORY~A = B@1 + \cdots + B@n\colon$] commences a new theory $A$
71 based on existing ones $B@1 + \cdots + B@n$. Isabelle's theory loader
72 system ensures that any of the base theories are properly loaded (and fully
73 up-to-date when $\THEORY$ is executed interactively). The optional
74 $\isarkeyword{files}$ specification declares additional dependencies on ML
75 files. Unless put in parentheses, any file will be loaded immediately via
76 $\isarcmd{use}$ (see also \S\ref{sec:ML}). The optional ML file
77 \texttt{$A$.ML} that may be associated with any theory should \emph{not} be
78 included in $\isarkeyword{files}$, though.
80 \item [$\CONTEXT~B$] enters an existing theory context, basically in read-only
81 mode, so only a limited set of commands may be performed without destroying
82 the theory. Just as for $\THEORY$, the theory loader ensures that $B$ is
83 loaded and up-to-date.
85 \item [$\END$] concludes the current theory definition or context switch.
86 Note that this command cannot be undone, but the whole theory definition has
91 \subsection{Theory markup commands}\label{sec:markup-thy}
93 \indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}
94 \indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{text-raw}
95 \begin{matharray}{rcl}
96 \isarcmd{chapter} & : & \isartrans{theory}{theory} \\
97 \isarcmd{section} & : & \isartrans{theory}{theory} \\
98 \isarcmd{subsection} & : & \isartrans{theory}{theory} \\
99 \isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\
100 \isarcmd{text} & : & \isartrans{theory}{theory} \\
101 \isarcmd{text_raw} & : & \isartrans{theory}{theory} \\
104 Apart from formal comments (see \S\ref{sec:comments}), markup commands provide
105 a structured way to insert text into the document generated from a theory (see
106 \cite{isabelle-sys} for more information on Isabelle's document preparation
109 \railalias{textraw}{text\_raw}
113 ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text' | textraw) text
118 \item [$\isarkeyword{chapter}$, $\isarkeyword{section}$,
119 $\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter
120 and section headings.
121 \item [$\TEXT$] specifies paragraphs of plain text, including references to
122 formal entities.\footnote{The latter feature is not yet supported.
123 Nevertheless, any source text of the form
124 ``\texttt{\at\ttlbrace$\dots$\ttrbrace}'' should be considered as reserved
126 \item [$\isarkeyword{text_raw}$] inserts {\LaTeX} source into the output,
127 without additional markup. Thus the full range of document manipulations
128 becomes available. A typical application would be to emit
129 \verb,\begin{comment}, and \verb,\end{comment}, commands to exclude certain
130 parts from the final document.\footnote{This requires the \texttt{comment}
131 package to be included in {\LaTeX}, of course.}
134 Any of these markup elements corresponds to a {\LaTeX} command with the name
135 prefixed by \verb,\isamarkup,. For the sectioning commands this is a plain
136 macro with a single argument, e.g.\ \verb,\isamarkupchapter{,\dots\verb,}, for
137 $\isarkeyword{chapter}$. The $\isarkeyword{text}$ markup results in a
138 {\LaTeX} environment \verb,\begin{isamarkuptext}, {\dots}
139 \verb,\end{isamarkuptext},, while $\isarkeyword{text_raw}$ causes the text
140 to be inserted directly into the {\LaTeX} source.
144 Additional markup commands are available for proofs (see
145 \S\ref{sec:markup-prf}). Also note that the $\isarkeyword{header}$
146 declaration (see \S\ref{sec:begin-thy}) admits to insert section markup just
147 preceding the actual theory definition.
150 \subsection{Type classes and sorts}\label{sec:classes}
152 \indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
153 \begin{matharray}{rcl}
154 \isarcmd{classes} & : & \isartrans{theory}{theory} \\
155 \isarcmd{classrel} & : & \isartrans{theory}{theory} \\
156 \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\
160 'classes' (classdecl comment? +)
162 'classrel' nameref ('<' | subseteq) nameref comment?
164 'defaultsort' sort comment?
169 \item [$\isarkeyword{classes}~c \subseteq \vec c$] declares class $c$ to be a
170 subclass of existing classes $\vec c$. Cyclic class structures are ruled
172 \item [$\isarkeyword{classrel}~c@1 \subseteq c@2$] states a subclass relation
173 between existing classes $c@1$ and $c@2$. This is done axiomatically! The
174 $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a way to introduce
175 proven class relations.
176 \item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
177 any type variables given without sort constraints. Usually, the default
178 sort would be only changed when defining new object-logics.
182 \subsection{Primitive types and type abbreviations}\label{sec:types-pure}
184 \indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
185 \begin{matharray}{rcl}
186 \isarcmd{types} & : & \isartrans{theory}{theory} \\
187 \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
188 \isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\
189 \isarcmd{arities} & : & \isartrans{theory}{theory} \\
193 'types' (typespec '=' type infix? comment? +)
195 'typedecl' typespec infix? comment?
197 'nonterminals' (name +) comment?
199 'arities' (nameref '::' arity comment? +)
204 \item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym}
205 $(\vec\alpha)t$ for existing type $\tau$. Unlike actual type definitions,
206 as are available in Isabelle/HOL for example, type synonyms are just purely
207 syntactic abbreviations without any logical significance. Internally, type
208 synonyms are fully expanded.
209 \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor
210 $t$, intended as an actual logical type. Note that object-logics such as
211 Isabelle/HOL override $\isarkeyword{typedecl}$ by their own version.
212 \item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors
213 $\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of
214 Isabelle's inner syntax of terms or types.
215 \item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's order-sorted
216 signature of types by new type constructor arities. This is done
217 axiomatically! The $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a
218 way to introduce proven type arities.
222 \subsection{Constants and simple definitions}\label{sec:consts}
224 \indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl}
225 \begin{matharray}{rcl}
226 \isarcmd{consts} & : & \isartrans{theory}{theory} \\
227 \isarcmd{defs} & : & \isartrans{theory}{theory} \\
228 \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
232 'consts' (constdecl +)
234 'defs' ('(overloaded)')? (axmdecl prop comment? +)
236 'constdefs' (constdecl prop comment? +)
239 constdecl: name '::' type mixfix? comment?
244 \item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type
245 scheme $\sigma$. The optional mixfix annotations may attach concrete syntax
246 to the constants declared.
248 \item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for some
249 existing constant. See \cite[\S6]{isabelle-ref} for more details on the
250 form of equations admitted as constant definitions.
252 The $overloaded$ option declares definitions to be potentially overloaded.
253 Unless this option is given, a warning message would be issued for any
254 definitional equation with a more special type than that of the
255 corresponding constant declaration.
257 \item [$\isarkeyword{constdefs}~c::\sigma~eqn$] combines declarations and
258 definitions of constants, using the canonical name $c_def$ for the
263 \subsection{Syntax and translations}\label{sec:syn-trans}
265 \indexisarcmd{syntax}\indexisarcmd{translations}
266 \begin{matharray}{rcl}
267 \isarcmd{syntax} & : & \isartrans{theory}{theory} \\
268 \isarcmd{translations} & : & \isartrans{theory}{theory} \\
271 \railalias{rightleftharpoons}{\isasymrightleftharpoons}
272 \railterm{rightleftharpoons}
274 \railalias{rightharpoonup}{\isasymrightharpoonup}
275 \railterm{rightharpoonup}
277 \railalias{leftharpoondown}{\isasymleftharpoondown}
278 \railterm{leftharpoondown}
281 'syntax' ('(' ( name | 'output' | name 'output' ) ')')? (constdecl +)
283 'translations' (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat comment? +)
285 transpat: ('(' nameref ')')? string
290 \item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$,
291 except that the actual logical signature extension is omitted. Thus the
292 context free grammar of Isabelle's inner syntax may be augmented in
293 arbitrary ways, independently of the logic. The $mode$ argument refers to
294 the print mode that the grammar rules belong; unless the \texttt{output}
295 flag is given, all productions are added both to the input and output
297 \item [$\isarkeyword{translations}~rules$] specifies syntactic translation
298 rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==} or
299 \isasymrightleftharpoons), parse rules (\texttt{=>} or
300 \isasymrightharpoonup), or print rules (\texttt{<=} or
301 \isasymleftharpoondown). Translation patterns may be prefixed by the
302 syntactic category to be used for parsing; the default is \texttt{logic}.
306 \subsection{Axioms and theorems}\label{sec:axms-thms}
308 \indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas}
309 \begin{matharray}{rcl}
310 \isarcmd{axioms} & : & \isartrans{theory}{theory} \\
311 \isarcmd{theorems} & : & \isartrans{theory}{theory} \\
312 \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
316 'axioms' (axmdecl prop comment? +)
318 ('theorems' | 'lemmas') (thmdef? thmrefs comment? + 'and')
323 \item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as
324 axioms of the meta-logic. In fact, axioms are ``axiomatic theorems'', and
325 may be referred later just as any other theorem.
327 Axioms are usually only introduced when declaring new logical systems.
328 Everyday work is typically done the hard way, with proper definitions and
329 actual proven theorems.
330 \item [$\isarkeyword{theorems}~a = \vec b$] stores lists of existing theorems.
331 Typical applications would also involve attributes, to declare Simplifier
333 \item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but
334 tags the results as ``lemma''.
338 \subsection{Name spaces}
340 \indexisarcmd{global}\indexisarcmd{local}\indexisarcmd{hide}
341 \begin{matharray}{rcl}
342 \isarcmd{global} & : & \isartrans{theory}{theory} \\
343 \isarcmd{local} & : & \isartrans{theory}{theory} \\
344 \isarcmd{hide} & : & \isartrans{theory}{theory} \\
352 'hide' name (nameref + ) comment?
356 Isabelle organizes any kind of name declarations (of types, constants,
357 theorems etc.) by separate hierarchically structured name spaces. Normally
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.
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.
365 Changing this to $\isarkeyword{global}$ causes all names to be declared
366 without the theory prefix, until $\isarkeyword{local}$ is declared again.
368 Note that global names are prone to get hidden accidently later, when
369 qualified names of the same base name are introduced.
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
377 Unqualified (global) names may not be hidden deliberately.
381 \subsection{Incorporating ML code}\label{sec:ML}
383 \indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{ML-command}
384 \indexisarcmd{ML-setup}\indexisarcmd{setup}
385 \indexisarcmd{method-setup}
386 \begin{matharray}{rcl}
387 \isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\
388 \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
389 \isarcmd{ML_command} & : & \isartrans{\cdot}{\cdot} \\
390 \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
391 \isarcmd{setup} & : & \isartrans{theory}{theory} \\
392 \isarcmd{method_setup} & : & \isartrans{theory}{theory} \\
395 \railalias{MLsetup}{ML\_setup}
398 \railalias{methodsetup}{method\_setup}
399 \railterm{methodsetup}
401 \railalias{MLcommand}{ML\_command}
407 ('ML' | MLcommand | MLsetup | 'setup') text comment?
409 methodsetup name '=' text text comment?
414 \item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$.
415 The current theory context (if present) is passed down to the ML session,
416 but may not be modified. Furthermore, the file name is checked with the
417 $\isarkeyword{files}$ dependency declaration given in the theory header (see
418 also \S\ref{sec:begin-thy}).
420 \item [$\isarkeyword{ML}~text$ and $\isarkeyword{ML_command}~text$] execute ML
421 commands from $text$. The theory context is passed in the same way as for
422 $\isarkeyword{use}$, but may not be changed. Note that the output of
423 $\isarkeyword{ML_command}$ is less verbose than plain $\isarkeyword{ML}$.
425 \item [$\isarkeyword{ML_setup}~text$] executes ML commands from $text$. The
426 theory context is passed down to the ML session, and fetched back
427 afterwards. Thus $text$ may actually change the theory as a side effect.
429 \item [$\isarkeyword{setup}~text$] changes the current theory context by
430 applying $text$, which refers to an ML expression of type
431 \texttt{(theory~->~theory)~list}. The $\isarkeyword{setup}$ command is the
432 canonical way to initialize any object-logic specific tools and packages
435 \item [$\isarkeyword{method_setup}~name = text~description$] defines a proof
436 method in the current theory. The given $text$ has to be an ML expression
437 of type \texttt{Args.src -> Proof.context -> Proof.method}. Parsing
438 concrete method syntax from \texttt{Args.src} input can be quite tedious in
439 general. The following simple examples are for methods without any explicit
440 arguments, or a list of theorems, respectively.
444 Method.no_args (Method.METHOD (fn facts => foobar_tac))
445 Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
446 Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
447 Method.thms_ctxt_args (fn thms => fn ctxt => Method.METHOD (fn facts => foobar_tac))
451 Note that mere tactic emulations may ignore the \texttt{facts} parameter
452 above. Proper proof methods would do something ``appropriate'' with the list
453 of current facts, though. Single-rule methods usually do strict
454 forward-chaining (e.g.\ by using \texttt{Method.multi_resolves}), while
455 automatic ones just insert the facts using \texttt{Method.insert_tac} before
456 applying the main tactic.
460 \subsection{Syntax translation functions}
462 \indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}
463 \indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}
464 \indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}
465 \begin{matharray}{rcl}
466 \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
467 \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
468 \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
469 \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
470 \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
471 \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
474 \railalias{parseasttranslation}{parse\_ast\_translation}
475 \railterm{parseasttranslation}
477 \railalias{parsetranslation}{parse\_translation}
478 \railterm{parsetranslation}
480 \railalias{printtranslation}{print\_translation}
481 \railterm{printtranslation}
483 \railalias{typedprinttranslation}{typed\_print\_translation}
484 \railterm{typedprinttranslation}
486 \railalias{printasttranslation}{print\_ast\_translation}
487 \railterm{printasttranslation}
489 \railalias{tokentranslation}{token\_translation}
490 \railterm{tokentranslation}
493 ( parseasttranslation | parsetranslation | printtranslation | typedprinttranslation |
494 printasttranslation | tokentranslation ) text comment?
497 Syntax translation functions written in ML admit almost arbitrary
498 manipulations of Isabelle's inner syntax. Any of the above commands have a
499 single \railqtoken{text} argument that refers to an ML expression of
503 val parse_ast_translation : (string * (ast list -> ast)) list
504 val parse_translation : (string * (term list -> term)) list
505 val print_translation : (string * (term list -> term)) list
506 val typed_print_translation :
507 (string * (bool -> typ -> term list -> term)) list
508 val print_ast_translation : (string * (ast list -> ast)) list
509 val token_translation :
510 (string * string * (string -> string * real)) list
512 See \cite[\S8]{isabelle-ref} for more information on syntax transformations.
517 \indexisarcmd{oracle}
518 \begin{matharray}{rcl}
519 \isarcmd{oracle} & : & \isartrans{theory}{theory} \\
522 Oracles provide an interface to external reasoning systems, without giving up
523 control completely --- each theorem carries a derivation object recording any
524 oracle invocation. See \cite[\S6]{isabelle-ref} for more information.
527 'oracle' name '=' text comment?
532 \item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML
533 function $text$, which has to be of type
534 \texttt{Sign.sg~*~Object.T~->~term}.
538 \section{Proof commands}
540 Proof commands perform transitions of Isar/VM machine configurations, which
541 are block-structured, consisting of a stack of nodes with three main
542 components: logical proof context, current facts, and open goals. Isar/VM
543 transitions are \emph{typed} according to the following three different modes
546 \item [$proof(prove)$] means that a new goal has just been stated that is now
547 to be \emph{proven}; the next command may refine it by some proof method,
548 and enter a sub-proof to establish the actual result.
549 \item [$proof(state)$] is like a nested theory mode: the context may be
550 augmented by \emph{stating} additional assumptions, intermediate results
552 \item [$proof(chain)$] is intermediate between $proof(state)$ and
553 $proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$''
554 register) have been just picked up in order to be used when refining the
559 \subsection{Proof markup commands}\label{sec:markup-prf}
561 \indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect}
562 \indexisarcmd{txt}\indexisarcmd{txt-raw}
563 \begin{matharray}{rcl}
564 \isarcmd{sect} & : & \isartrans{proof}{proof} \\
565 \isarcmd{subsect} & : & \isartrans{proof}{proof} \\
566 \isarcmd{subsubsect} & : & \isartrans{proof}{proof} \\
567 \isarcmd{txt} & : & \isartrans{proof}{proof} \\
568 \isarcmd{txt_raw} & : & \isartrans{proof}{proof} \\
571 These markup commands for proof mode closely correspond to the ones of theory
572 mode (see \S\ref{sec:markup-thy}).
574 \railalias{txtraw}{txt\_raw}
578 ('sect' | 'subsect' | 'subsubsect' | 'txt' | txtraw) text
583 \subsection{Proof context}\label{sec:proof-context}
585 \indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}
586 \begin{matharray}{rcl}
587 \isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\
588 \isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\
589 \isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\
590 \isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\
593 The logical proof context consists of fixed variables and assumptions. The
594 former closely correspond to Skolem constants, or meta-level universal
595 quantification as provided by the Isabelle/Pure logical framework.
596 Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in
597 a local value that may be used in the subsequent proof as any other variable
598 or constant. Furthermore, any result $\edrv \phi[x]$ exported from the
599 context will be universally closed wrt.\ $x$ at the outermost level: $\edrv
600 \All x \phi$ (this is expressed using Isabelle's meta-variables).
602 Similarly, introducing some assumption $\chi$ has two effects. On the one
603 hand, a local theorem is created that may be used as a fact in subsequent
604 proof steps. On the other hand, any result $\chi \drv \phi$ exported from the
605 context becomes conditional wrt.\ the assumption: $\edrv \chi \Imp \phi$.
606 Thus, solving an enclosing goal using such a result would basically introduce
607 a new subgoal stemming from the assumption. How this situation is handled
608 depends on the actual version of assumption command used: while $\ASSUMENAME$
609 insists on solving the subgoal by unification with some premise of the goal,
610 $\PRESUMENAME$ leaves the subgoal unchanged in order to be proved later by the
613 Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by
614 combining $\FIX x$ with another version of assumption that causes any
615 hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule.
616 Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
618 \railalias{equiv}{\isasymequiv}
622 'fix' (vars + 'and') comment?
624 ('assume' | 'presume') (assm comment? + 'and')
626 'def' thmdecl? \\ name ('==' | equiv) term termpat? comment?
629 var: name ('::' type)?
631 vars: (name+) ('::' type)?
633 assm: thmdecl? (prop proppat? +)
638 \item [$\FIX{\vec x}$] introduces local \emph{arbitrary, but fixed} variables
640 \item [$\ASSUME{a}{\vec\phi}$ and $\PRESUME{a}{\vec\phi}$] introduce local
641 theorems $\vec\phi$ by assumption. Subsequent results applied to an
642 enclosing goal (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$
643 expects to be able to unify with existing premises in the goal, while
644 $\PRESUMENAME$ leaves $\vec\phi$ as new subgoals.
646 Several lists of assumptions may be given (separated by
647 $\isarkeyword{and}$); the resulting list of current facts consists of all of
649 \item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
650 In results exported from the context, $x$ is replaced by $t$. Basically,
651 $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\ASSUME{}{x \equiv t}$, with the
652 resulting hypothetical equation solved by reflexivity.
654 The default name for the definitional equation is $x_def$.
657 The special name $prems$\indexisarthm{prems} refers to all assumptions of the
658 current context as a list of theorems.
661 \subsection{Facts and forward chaining}
663 \indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
664 \begin{matharray}{rcl}
665 \isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\
666 \isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\
667 \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\
668 \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
671 New facts are established either by assumption or proof of local statements.
672 Any fact will usually be involved in further proofs, either as explicit
673 arguments of proof methods, or when forward chaining towards the next goal via
674 $\THEN$ (and variants). Note that the special theorem name
675 $this$\indexisarthm{this} refers to the most recently established facts.
677 'note' (thmdef? thmrefs comment? + 'and')
681 ('from' | 'with') (thmrefs comment? + 'and')
686 \item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result
687 as $a$. Note that attributes may be involved as well, both on the left and
689 \item [$\THEN$] indicates forward chaining by the current facts in order to
690 establish the goal to be claimed next. The initial proof method invoked to
691 refine that will be offered the facts to do ``anything appropriate'' (cf.\
692 also \S\ref{sec:proof-steps}). For example, method $rule$ (see
693 \S\ref{sec:pure-meth-att}) would typically do an elimination rather than an
694 introduction. Automatic methods usually insert the facts into the goal
695 state before operation. This provides a simple scheme to control relevance
696 of facts in automated proof search.
697 \item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is
698 equivalent to $\FROM{this}$.
699 \item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~this}$; thus the forward
700 chaining is from earlier facts together with the current ones.
703 Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth-att}) expect
704 multiple facts to be given in their proper order, corresponding to a prefix of
705 the premises of the rule involved. Note that positions may be easily skipped
706 using something like $\FROM{\Text{\texttt{_}}~a~b}$, for example. This
707 involves the trivial rule $\PROP\psi \Imp \PROP\psi$, which happens to be
708 bound in Isabelle/Pure as ``\texttt{_}''
709 (underscore).\indexisarthm{_@\texttt{_}}
711 Forward chaining with an empty list of theorems is the same as not chaining.
712 Thus $\FROM{nothing}$ has no effect apart from entering $prove(chain)$ mode,
713 since $nothing$\indexisarthm{nothing} is bound to the empty list of facts.
716 \subsection{Goal statements}
718 \indexisarcmd{theorem}\indexisarcmd{lemma}
719 \indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
720 \begin{matharray}{rcl}
721 \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
722 \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
723 \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
724 \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
725 \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
726 \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
729 Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$
730 and $\LEMMANAME$. New local goals may be claimed within proof mode as well.
731 Four variants are available, indicating whether the result is meant to solve
732 some pending goal or whether forward chaining is indicated.
735 ('theorem' | 'lemma') goal
737 ('have' | 'show' | 'hence' | 'thus') goal
740 goal: thmdecl? prop proppat? comment?
745 \item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal,
746 eventually resulting in some theorem $\turn \phi$ to be put back into the
748 \item [$\LEMMA{a}{\phi}$] is similar to $\THEOREMNAME$, but tags the result as
750 \item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a
751 theorem with the current assumption context as hypotheses.
752 \item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some
753 pending goal with the result \emph{exported} into the corresponding context
754 (cf.\ \S\ref{sec:proof-context}).
755 \item [$\HENCENAME$] abbreviates $\THEN~\HAVENAME$, i.e.\ claims a local goal
756 to be proven by forward chaining the current facts. Note that $\HENCENAME$
757 is also equivalent to $\FROM{this}~\HAVENAME$.
758 \item [$\THUSNAME$] abbreviates $\THEN~\SHOWNAME$. Note that $\THUSNAME$ is
759 also equivalent to $\FROM{this}~\SHOWNAME$.
762 Any goal statement causes some term abbreviations (such as $\Var{thesis}$,
763 $\dots$) to be bound automatically, see also \S\ref{sec:term-abbrev}.
764 Furthermore, the local context of a (non-atomic) goal is provided via the
765 $rule_context$\indexisarcase{rule-context} case, see also \S\ref{sec:cases}.
770 Isabelle/Isar suffers theory-level goal statements to contain \emph{unbound
771 schematic variables}, although this does not conform to the aim of
772 human-readable proof documents! The main problem with schematic goals is
773 that the actual outcome is usually hard to predict, depending on the
774 behavior of the actual proof methods applied during the reasoning. Note
775 that most semi-automated methods heavily depend on several kinds of implicit
776 rule declarations within the current theory context. As this would also
777 result in non-compositional checking of sub-proofs, \emph{local goals} are
778 not allowed to be schematic at all.
780 Nevertheless, schematic goals do have their use in Prolog-style interactive
781 synthesis of proven results, usually by stepwise refinement via emulation of
782 traditional Isabelle tactic scripts (see also \S\ref{sec:tactic-commands}).
783 In any case, users should know what they are doing!
787 \subsection{Initial and terminal proof steps}\label{sec:proof-steps}
789 \indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}
790 \indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}
791 \begin{matharray}{rcl}
792 \isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\
793 \isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
794 \isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
795 \isarcmd{.\,.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
796 \isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
797 \isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
800 Arbitrary goal refinement via tactics is considered harmful. Properly, the
801 Isar framework admits proof methods to be invoked in two places only.
803 \item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated
804 goal to a number of sub-goals that are to be solved later. Facts are passed
805 to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode.
807 \item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve
808 remaining goals. No facts are passed to $m@2$.
811 The only other proper way to affect pending goals is by $\SHOWNAME$, which
812 involves an explicit statement of what is to be solved.
816 Also note that initial proof methods should either solve the goal completely,
817 or constitute some well-understood reduction to new sub-goals. Arbitrary
818 automatic proof tools that are prone leave a large number of badly structured
819 sub-goals are no help in continuing the proof document in any intelligible
824 Unless given explicitly by the user, the default initial method is ``$rule$'',
825 which applies a single standard elimination or introduction rule according to
826 the topmost symbol involved. There is no separate default terminal method.
827 Any remaining goals are always solved by assumption in the very last step.
830 'proof' interest? meth? comment?
834 'by' meth meth? comment?
836 ('.' | '..' | 'sorry') comment?
839 meth: method interest?
844 \item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for
845 forward chaining are passed if so indicated by $proof(chain)$ mode.
846 \item [$\QED{m@2}$] refines any remaining goals by proof method $m@2$ and
847 concludes the sub-proof by assumption. If the goal had been $\SHOWNAME$ (or
848 $\THUSNAME$), some pending sub-goal is solved as well by the rule resulting
849 from the result \emph{exported} into the enclosing goal context. Thus
850 $\QEDNAME$ may fail for two reasons: either $m@2$ fails, or the resulting
851 rule does not fit to any pending goal\footnote{This includes any additional
852 ``strong'' assumptions as introduced by $\ASSUMENAME$.} of the enclosing
853 context. Debugging such a situation might involve temporarily changing
854 $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing
855 some occurrences of $\ASSUMENAME$ by $\PRESUMENAME$.
856 \item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it
857 abbreviates $\PROOF{m@1}~\QED{m@2}$, with backtracking across both methods,
858 though. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
859 by expanding its definition; in many cases $\PROOF{m@1}$ is already
860 sufficient to see what is going wrong.
861 \item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it
862 abbreviates $\BY{rule}$.
863 \item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
864 abbreviates $\BY{this}$.
865 \item [$\SORRY$] is a \emph{fake proof}\index{proof!fake}; provided that the
866 \texttt{quick_and_dirty} flag is enabled, $\SORRY$ pretends to solve the
867 goal without further ado. Of course, the result would be a fake theorem
868 only, involving some oracle in its internal derivation object (this is
869 indicated as ``$[!]$'' in the printed result). The main application of
870 $\SORRY$ is to support experimentation and top-down proof development.
874 \subsection{Fundamental methods and attributes}\label{sec:pure-meth-att}
876 The following proof methods and attributes refer to basic logical operations
877 of Isar. Further methods and attributes are provided by several generic and
878 object-logic specific tools and packages (see chapters \ref{ch:gen-tools} and
881 \indexisarmeth{assumption}\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{$-$}
882 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{rule}
883 \indexisaratt{OF}\indexisaratt{of}
884 \begin{matharray}{rcl}
885 assumption & : & \isarmeth \\
886 this & : & \isarmeth \\
887 rule & : & \isarmeth \\
891 intro & : & \isaratt \\
892 elim & : & \isaratt \\
893 dest & : & \isaratt \\
894 rule & : & \isaratt \\
902 'of' insts ('concl' ':' insts)?
909 \item [$assumption$] solves some goal by a single assumption step. Any facts
910 given (${} \le 1$) are guaranteed to participate in the refinement. Recall
911 that $\QEDNAME$ (see \S\ref{sec:proof-steps}) already concludes any
912 remaining sub-goals by assumption.
913 \item [$this$] applies all of the current facts directly as rules. Recall
914 that ``$\DOT$'' (dot) abbreviates $\BY{this}$.
915 \item [$rule~\vec a$] applies some rule given as argument in backward manner;
916 facts are used to reduce the rule before applying it to the goal. Thus
917 $rule$ without facts is plain \emph{introduction}, while with facts it
918 becomes \emph{elimination}.
920 When no arguments are given, the $rule$ method tries to pick appropriate
921 rules automatically, as declared in the current context using the $intro$,
922 $elim$, $dest$ attributes (see below). This is the default behavior of
923 $\PROOFNAME$ and ``$\DDOT$'' (double-dot) steps (see
924 \S\ref{sec:proof-steps}).
925 \item [``$-$''] does nothing but insert the forward chaining facts as premises
926 into the goal. Note that command $\PROOFNAME$ without any method actually
927 performs a single reduction step using the $rule$ method; thus a plain
928 \emph{do-nothing} proof step would be $\PROOF{-}$ rather than $\PROOFNAME$
930 \item [$OF~\vec a$] applies some theorem to given rules $\vec a$ (in
931 parallel). This corresponds to the \texttt{MRS} operator in ML
932 \cite[\S5]{isabelle-ref}, but note the reversed order. Positions may be
933 skipped by including ``$\_$'' (underscore) as argument.
934 \item [$of~\vec t$] performs positional instantiation. The terms $\vec t$ are
935 substituted for any schematic variables occurring in a theorem from left to
936 right; ``\texttt{_}'' (underscore) indicates to skip a position. Arguments
937 following a ``$concl\colon$'' specification refer to positions of the
938 conclusion of a rule.
939 \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
940 destruct rules, respectively. Note that the classical reasoner (see
941 \S\ref{sec:classical-basic}) introduces different versions of these
942 attributes, and the $rule$ method, too. In object-logics with classical
943 reasoning enabled, the latter version should be used all the time to avoid
945 \item [$rule~del$] undeclares introduction, elimination, or destruct rules.
949 \subsection{Term abbreviations}\label{sec:term-abbrev}
952 \begin{matharray}{rcl}
953 \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\
954 \isarkeyword{is} & : & syntax \\
957 Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,
958 or by annotating assumptions or goal statements with a list of patterns
959 $\ISS{p@1\;\dots}{p@n}$. In both cases, higher-order matching is invoked to
960 bind extra-logical term variables, which may be either named schematic
961 variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}''
962 (underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the
963 patterns occur on the left-hand side, while the $\ISNAME$ patterns are in
966 Polymorphism of term bindings is handled in Hindley-Milner style, as in ML.
967 Type variables referring to local assumptions or open goal statements are
968 \emph{fixed}, while those of finished results or bound by $\LETNAME$ may occur
969 in \emph{arbitrary} instances later. Even though actual polymorphism should
970 be rarely used in practice, this mechanism is essential to achieve proper
971 incremental type-inference, as the user proceeds to build up the Isar proof
976 Term abbreviations are quite different from actual local definitions as
977 introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}). The latter are
978 visible within the logic as actual equations, while abbreviations disappear
979 during the input process just after type checking. Also note that $\DEFNAME$
980 does not support polymorphism.
983 'let' ((term + 'and') '=' term comment? + 'and')
987 The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or
988 \railnonterm{proppat} (see \S\ref{sec:term-pats}).
991 \item [$\LET{\vec p = \vec t}$] binds any text variables in patters $\vec p$
992 by simultaneous higher-order matching against terms $\vec t$.
993 \item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the
994 preceding statement. Also note that $\ISNAME$ is not a separate command,
995 but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.).
998 Some \emph{automatic} term abbreviations\index{term abbreviations} for goals
999 and facts are available as well. For any open goal,
1000 $\Var{thesis}$\indexisarvar{thesis} refers to its object-level statement,
1001 abstracted over any meta-level parameters (if present). Likewise,
1002 $\Var{this}$\indexisarvar{this} is bound for fact statements resulting from
1003 assumptions or finished goals. In case $\Var{this}$ refers to an object-logic
1004 statement that is an application $f(t)$, then $t$ is bound to the special text
1005 variable ``$\dots$''\indexisarvar{\dots} (three dots). The canonical
1006 application of the latter are calculational proofs (see
1007 \S\ref{sec:calculation}).
1011 % A few \emph{automatic} term abbreviations\index{term abbreviations} for goals
1012 % and facts are available as well. For any open goal,
1013 % $\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition
1014 % (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its
1015 % (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its
1016 % object-level statement. The latter two abstract over any meta-level
1019 % Fact statements resulting from assumptions or finished goals are bound as
1020 % $\Var{this_prop}$\indexisarvar{this-prop},
1021 % $\Var{this_concl}$\indexisarvar{this-concl}, and
1022 % $\Var{this}$\indexisarvar{this}, similar to $\Var{thesis}$ above. In case
1023 % $\Var{this}$ refers to an object-logic statement that is an application
1024 % $f(t)$, then $t$ is bound to the special text variable
1025 % ``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of
1026 % the latter are calculational proofs (see \S\ref{sec:calculation}).
1029 \subsection{Block structure}
1031 \indexisarcmd{next}\indexisarcmd{\{}\indexisarcmd{\}}
1032 \begin{matharray}{rcl}
1033 \NEXT & : & \isartrans{proof(state)}{proof(state)} \\
1034 \BG & : & \isartrans{proof(state)}{proof(state)} \\
1035 \EN & : & \isartrans{proof(state)}{proof(state)} \\
1038 \railalias{lbrace}{\ttlbrace}
1041 \railalias{rbrace}{\ttrbrace}
1053 While Isar is inherently block-structured, opening and closing blocks is
1054 mostly handled rather casually, with little explicit user-intervention. Any
1055 local goal statement automatically opens \emph{two} blocks, which are closed
1056 again when concluding the sub-proof (by $\QEDNAME$ etc.). Sections of
1057 different context within a sub-proof may be switched via $\NEXT$, which is
1058 just a single block-close followed by block-open again. Thus the effect of
1059 $\NEXT$ to reset the local proof context. There is no goal focus involved
1062 For slightly more advanced applications, there are explicit block parentheses
1063 as well. These typically achieve a stronger forward style of reasoning.
1066 \item [$\NEXT$] switches to a fresh block within a sub-proof, resetting the
1067 local context to the initial one.
1068 \item [$\BG$ and $\EN$] explicitly open and close blocks. Any current facts
1069 pass through ``$\BG$'' unchanged, while ``$\EN$'' causes any result to be
1070 \emph{exported} into the enclosing context. Thus fixed variables are
1071 generalized, assumptions discharged, and local definitions unfolded (cf.\
1072 \S\ref{sec:proof-context}). There is no difference of $\ASSUMENAME$ and
1073 $\PRESUMENAME$ in this mode of forward reasoning --- in contrast to plain
1074 backward reasoning with the result exported at $\SHOWNAME$ time.
1078 \subsection{Emulating tactic scripts}\label{sec:tactic-commands}
1080 The Isar provides separate commands to accommodate tactic-style proof scripts
1081 within the same system. While being outside the orthodox Isar proof language,
1082 these might come in handy for interactive exploration and debugging, or even
1083 actual tactical proof within new-style theories (to benefit from document
1084 preparation, for example). See also \S\ref{sec:tactics} for actual tactics,
1085 that have been encapsulated as proof methods. Proper proof methods may be
1086 used in scripts, too.
1088 \indexisarcmd{apply}\indexisarcmd{apply-end}\indexisarcmd{done}
1089 \indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back}
1090 \indexisarcmd{declare}
1091 \begin{matharray}{rcl}
1092 \isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\
1093 \isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\
1094 \isarcmd{done}^* & : & \isartrans{proof(prove)}{proof(state)} \\
1095 \isarcmd{defer}^* & : & \isartrans{proof}{proof} \\
1096 \isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\
1097 \isarcmd{back}^* & : & \isartrans{proof}{proof} \\
1098 \isarcmd{declare}^* & : & \isartrans{theory}{theory} \\
1101 \railalias{applyend}{apply\_end}
1105 ( 'apply' | applyend ) method comment?
1109 'defer' nat? comment?
1111 'prefer' nat comment?
1115 'declare' thmrefs comment?
1120 \item [$\APPLY{m}$] applies proof method $m$ in initial position, but unlike
1121 $\PROOFNAME$ it retains ``$proof(prove)$'' mode. Thus consecutive method
1122 applications may be given just as in tactic scripts.
1124 Facts are passed to $m$ as indicated by the goal's forward-chain mode, and
1125 are \emph{consumed} afterwards. Thus any further $\APPLYNAME$ command would
1126 always work in a purely backward manner.
1128 \item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in
1129 terminal position. Basically, this simulates a multi-step tactic script for
1130 $\QEDNAME$, but may be given anywhere within the proof body.
1132 No facts are passed to $m$. Furthermore, the static context is that of the
1133 enclosing goal (as for actual $\QEDNAME$). Thus the proof method may not
1134 refer to any assumptions introduced in the current body, for example.
1136 \item [$\isarkeyword{done}$] completes a proof script, provided that the
1137 current goal state is already solved completely. Note that actual
1138 structured proof commands (e.g.\ ``$\DOT$'' or $\SORRY$) may be used to
1139 conclude proof scripts as well.
1141 \item [$\isarkeyword{defer}~n$ and $\isarkeyword{prefer}~n$] shuffle the list
1142 of pending goals: $defer$ puts off goal $n$ to the end of the list ($n = 1$
1143 by default), while $prefer$ brings goal $n$ to the top.
1145 \item [$\isarkeyword{back}$] does back-tracking over the result sequence of
1146 the latest proof command.\footnote{Unlike the ML function \texttt{back}
1147 \cite{isabelle-ref}, the Isar command does not search upwards for further
1148 branch points.} Basically, any proof command may return multiple results.
1150 \item [$\isarkeyword{declare}~thms$] declares theorems to the current theory
1151 context. No theorem binding is involved here, unlike
1152 $\isarkeyword{theorems}$ or $\isarkeyword{lemmas}$ (cf.\
1153 \S\ref{sec:axms-thms}). So $\isarkeyword{declare}$ only has the effect of
1154 applying attributes as included in the theorem specification.
1157 Any proper Isar proof method may be used with tactic script commands such as
1158 $\APPLYNAME$. A few additional emulations of actual tactics are provided as
1159 well; these would be never used in actual structured proofs, of course.
1162 \subsection{Meta-linguistic features}
1165 \begin{matharray}{rcl}
1166 \isarcmd{oops} & : & \isartrans{proof}{theory} \\
1169 The $\OOPS$ command discontinues the current proof attempt, while considering
1170 the partial proof text as properly processed. This is conceptually quite
1171 different from ``faking'' actual proofs via $\SORRY$ (see
1172 \S\ref{sec:proof-steps}): $\OOPS$ does not observe the proof structure at all,
1173 but goes back right to the theory level. Furthermore, $\OOPS$ does not
1174 produce any result theorem --- there is no claim to be able to complete the
1177 A typical application of $\OOPS$ is to explain Isar proofs \emph{within} the
1178 system itself, in conjunction with the document preparation tools of Isabelle
1179 described in \cite{isabelle-sys}. Thus partial or even wrong proof attempts
1180 can be discussed in a logically sound manner. Note that the Isabelle {\LaTeX}
1181 macros can be easily adapted to print something like ``$\dots$'' instead of an
1182 ``$\OOPS$'' keyword.
1184 \medskip The $\OOPS$ command is undoable, unlike $\isarkeyword{kill}$ (see
1185 \S\ref{sec:history}). The effect is to get back to the theory \emph{before}
1186 the opening of the proof.
1189 \section{Other commands}
1191 \subsection{Diagnostics}
1193 \indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term}
1194 \indexisarcmd{prop}\indexisarcmd{typ}
1195 \begin{matharray}{rcl}
1196 \isarcmd{pr}^* & : & \isarkeep{\cdot} \\
1197 \isarcmd{thm}^* & : & \isarkeep{theory~|~proof} \\
1198 \isarcmd{term}^* & : & \isarkeep{theory~|~proof} \\
1199 \isarcmd{prop}^* & : & \isarkeep{theory~|~proof} \\
1200 \isarcmd{typ}^* & : & \isarkeep{theory~|~proof} \\
1203 These diagnostic commands assist interactive development. Note that $undo$
1204 does not apply here, the theory or proof configuration is not changed.
1207 'pr' modes? nat? (',' nat)?
1209 'thm' modes? thmrefs comment?
1211 'term' modes? term comment?
1213 'prop' modes? prop comment?
1215 'typ' modes? type comment?
1218 modes: '(' (name + ) ')'
1223 \item [$\isarkeyword{pr}~goals, prems$] prints the current proof state (if
1224 present), including the proof context, current facts and goals. The
1225 optional limit arguments affect the number of goals and premises to be
1226 displayed, which is initially 10 for both. Omitting limit values leaves the
1227 current setting unchanged.
1228 \item [$\isarkeyword{thm}~\vec a$] retrieves theorems from the current theory
1229 or proof context. Note that any attributes included in the theorem
1230 specifications are applied to a temporary context derived from the current
1231 theory or proof; the result is discarded, i.e.\ attributes involved in $\vec
1232 a$ do not have any permanent effect.
1233 \item [$\isarkeyword{term}~t$ and $\isarkeyword{prop}~\phi$] read, type-check
1234 and print terms or propositions according to the current theory or proof
1235 context; the inferred type of $t$ is output as well. Note that these
1236 commands are also useful in inspecting the current environment of term
1238 \item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic
1239 according to the current theory or proof context.
1242 All of the diagnostic commands above admit a list of $modes$ to be specified,
1243 which is appended to the current print mode (see also \cite{isabelle-ref}).
1244 Thus the output behavior may be modified according particular print mode
1245 features. For example, $\isarkeyword{pr}~(latex~xsymbols~symbols)$ would
1246 print the current proof state with mathematical symbols and special characters
1247 represented in {\LaTeX} source, according to the Isabelle style
1248 \cite{isabelle-sys}.
1250 Note that antiquotations (cf.\ \S\ref{sec:antiq}) provide a more systematic
1251 way to include formal items into the printed text document.
1254 \subsection{Inspecting the context}
1256 \indexisarcmd{print-facts}\indexisarcmd{print-binds}
1257 \indexisarcmd{print-commands}\indexisarcmd{print-syntax}
1258 \indexisarcmd{print-methods}\indexisarcmd{print-attributes}
1259 \indexisarcmd{thms-containing}\indexisarcmd{thm-deps}
1260 \indexisarcmd{print-theorems}
1261 \begin{matharray}{rcl}
1262 \isarcmd{print_commands}^* & : & \isarkeep{\cdot} \\
1263 \isarcmd{print_syntax}^* & : & \isarkeep{theory~|~proof} \\
1264 \isarcmd{print_methods}^* & : & \isarkeep{theory~|~proof} \\
1265 \isarcmd{print_attributes}^* & : & \isarkeep{theory~|~proof} \\
1266 \isarcmd{print_theorems}^* & : & \isarkeep{theory~|~proof} \\
1267 \isarcmd{thms_containing}^* & : & \isarkeep{theory~|~proof} \\
1268 \isarcmd{thms_deps}^* & : & \isarkeep{theory~|~proof} \\
1269 \isarcmd{print_facts}^* & : & \isarkeep{proof} \\
1270 \isarcmd{print_binds}^* & : & \isarkeep{proof} \\
1273 \railalias{thmscontaining}{thms\_containing}
1274 \railterm{thmscontaining}
1276 \railalias{thmdeps}{thm\_deps}
1280 thmscontaining (term * )
1286 These commands print certain parts of the theory and proof context. Note that
1287 there are some further ones available, such as for the set of rules declared
1288 for simplifications.
1291 \item [$\isarkeyword{print_commands}$] prints Isabelle's outer theory syntax,
1292 including keywords and command.
1293 \item [$\isarkeyword{print_syntax}$] prints the inner syntax of types and
1294 terms, depending on the current context. The output can be very verbose,
1295 including grammar tables and syntax translation rules. See \cite[\S7,
1296 \S8]{isabelle-ref} for further information on Isabelle's inner syntax.
1297 \item [$\isarkeyword{print_methods}$] prints all proof methods available in
1298 the current theory context.
1299 \item [$\isarkeyword{print_attributes}$] prints all attributes available in
1300 the current theory context.
1301 \item [$\isarkeyword{print_theorems}$] prints theorems available in the
1302 current theory context. In interactive mode this actually refers to the
1303 theorems left by the last transaction; this allows to inspect the result of
1304 advanced definitional packages, such as $\isarkeyword{datatype}$.
1305 \item [$\isarkeyword{thms_containing}~\vec t$] retrieves theorems from the
1306 theory context containing all of the constants occurring in the terms $\vec
1307 t$. Note that giving the empty list yields \emph{all} theorems of the
1309 \item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of theorems
1310 and lemmas, using Isabelle's graph browser tool (see also
1311 \cite{isabelle-sys}).
1312 \item [$\isarkeyword{print_facts}$] prints any named facts of the current
1313 context, including assumptions and local results.
1314 \item [$\isarkeyword{print_binds}$] prints all term abbreviations present in
1319 \subsection{History commands}\label{sec:history}
1321 \indexisarcmd{undo}\indexisarcmd{redo}\indexisarcmd{kill}
1322 \begin{matharray}{rcl}
1323 \isarcmd{undo}^{{*}{*}} & : & \isarkeep{\cdot} \\
1324 \isarcmd{redo}^{{*}{*}} & : & \isarkeep{\cdot} \\
1325 \isarcmd{kill}^{{*}{*}} & : & \isarkeep{\cdot} \\
1328 The Isabelle/Isar top-level maintains a two-stage history, for theory and
1329 proof state transformation. Basically, any command can be undone using
1330 $\isarkeyword{undo}$, excluding mere diagnostic elements. Its effect may be
1331 revoked via $\isarkeyword{redo}$, unless the corresponding
1332 $\isarkeyword{undo}$ step has crossed the beginning of a proof or theory. The
1333 $\isarkeyword{kill}$ command aborts the current history node altogether,
1334 discontinuing a proof or even the whole theory. This operation is \emph{not}
1338 History commands should never be used with user interfaces such as
1339 Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes care of
1340 stepping forth and back itself. Interfering by manual $\isarkeyword{undo}$,
1341 $\isarkeyword{redo}$, or even $\isarkeyword{kill}$ commands would quickly
1342 result in utter confusion.
1346 \subsection{System operations}
1348 \indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only}
1349 \indexisarcmd{update-thy}\indexisarcmd{update-thy-only}
1350 \begin{matharray}{rcl}
1351 \isarcmd{cd}^* & : & \isarkeep{\cdot} \\
1352 \isarcmd{pwd}^* & : & \isarkeep{\cdot} \\
1353 \isarcmd{use_thy}^* & : & \isarkeep{\cdot} \\
1354 \isarcmd{use_thy_only}^* & : & \isarkeep{\cdot} \\
1355 \isarcmd{update_thy}^* & : & \isarkeep{\cdot} \\
1356 \isarcmd{update_thy_only}^* & : & \isarkeep{\cdot} \\
1360 \item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle
1362 \item [$\isarkeyword{pwd}~$] prints the current working directory.
1363 \item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$,
1364 $\isarkeyword{update_thy}$, $\isarkeyword{update_thy_only}$] load some
1365 theory given as $name$ argument. These commands are basically the same as
1366 the corresponding ML functions\footnote{The ML versions also change the
1367 implicit theory context to that of the theory loaded.} (see also
1368 \cite[\S1,\S6]{isabelle-ref}). Note that both the ML and Isar versions may
1369 load new- and old-style theories alike.
1372 These system commands are scarcely used when working with the Proof~General
1373 interface, since loading of theories is done fully transparently.
1376 %%% Local Variables:
1378 %%% TeX-master: "isar-ref"