2 \chapter{Basic Isar Language Elements}\label{ch:pure-syntax}
4 Subsequently, we introduce the main part of the basic Isar theory and proof
5 commands as provided by Isabelle/Pure. Chapter~\ref{ch:gen-tools} describes
6 further Isar elements provided by generic tools and packages (such as the
7 Simplifier) that are either part of Pure Isabelle or pre-loaded by most object
8 logics. Chapter~\ref{ch:hol-tools} refers to actual object-logic specific
9 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
20 proving, which facilitates porting of legacy proof scripts.
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{\cdot}{theory} \\
31 \isarcmd{context}^* & : & \isartrans{\cdot}{theory} \\
32 \isarcmd{end} & : & \isartrans{theory}{\cdot} \\
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 in a 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 begin 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}.}
134 Any markup command (except $\isarkeyword{text_raw}$) corresponds to a {\LaTeX}
135 macro with the name prefixed by \verb,\isamarkup, (e.g.\
136 \verb,\isamarkupchapter, for $\isarkeyword{chapter}$). The \railqtoken{text}
137 argument is passed to that macro unchanged, i.e.\ further {\LaTeX} commands
138 may be included here as well.
140 \medskip Additional markup commands are available for proofs (see
141 \S\ref{sec:markup-prf}). Also note that the $\isarkeyword{header}$
142 declaration (see \S\ref{sec:begin-thy}) admits to insert document markup
143 elements just preceding the actual theory definition.
146 \subsection{Type classes and sorts}\label{sec:classes}
148 \indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
149 \begin{matharray}{rcl}
150 \isarcmd{classes} & : & \isartrans{theory}{theory} \\
151 \isarcmd{classrel} & : & \isartrans{theory}{theory} \\
152 \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\
156 'classes' (classdecl comment? +)
158 'classrel' nameref '<' nameref comment?
160 'defaultsort' sort comment?
165 \item [$\isarkeyword{classes}~c<\vec c$] declares class $c$ to be a subclass
166 of existing classes $\vec c$. Cyclic class structures are ruled out.
167 \item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between
168 existing classes $c@1$ and $c@2$. This is done axiomatically! The
169 $\isarkeyword{instance}$ command (see \S\ref{sec:axclass}) provides a way to
170 introduce proven class relations.
171 \item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
172 any type variables given without sort constraints. Usually, the default
173 sort would be only changed when defining new logics.
177 \subsection{Primitive types and type abbreviations}\label{sec:types-pure}
179 \indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
180 \begin{matharray}{rcl}
181 \isarcmd{types} & : & \isartrans{theory}{theory} \\
182 \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
183 \isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\
184 \isarcmd{arities} & : & \isartrans{theory}{theory} \\
188 'types' (typespec '=' type infix? comment? +)
190 'typedecl' typespec infix? comment?
192 'nonterminals' (name +) comment?
194 'arities' (nameref '::' arity comment? +)
199 \item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym}
200 $(\vec\alpha)t$ for existing type $\tau$. Unlike actual type definitions,
201 as are available in Isabelle/HOL for example, type synonyms are just purely
202 syntactic abbreviations without any logical significance. Internally, type
203 synonyms are fully expanded.
204 \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor
205 $t$, intended as an actual logical type. Note that object-logics such as
206 Isabelle/HOL override $\isarkeyword{typedecl}$ by their own version.
207 \item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors
208 $\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of
209 Isabelle's inner syntax of terms or types.
210 \item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's order-sorted
211 signature of types by new type constructor arities. This is done
212 axiomatically! The $\isarkeyword{instance}$ command (see
213 \S\ref{sec:axclass}) provides a way to introduce proven type arities.
217 \subsection{Constants and simple definitions}\label{sec:consts}
219 \indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl}
220 \begin{matharray}{rcl}
221 \isarcmd{consts} & : & \isartrans{theory}{theory} \\
222 \isarcmd{defs} & : & \isartrans{theory}{theory} \\
223 \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
227 'consts' (constdecl +)
229 'defs' (axmdecl prop comment? +)
231 'constdefs' (constdecl prop comment? +)
234 constdecl: name '::' type mixfix? comment?
239 \item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type
240 scheme $\sigma$. The optional mixfix annotations may attach concrete syntax
241 to the constants declared.
242 \item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for some
243 existing constant. See \cite[\S6]{isabelle-ref} for more details on the
244 form of equations admitted as constant definitions.
245 \item [$\isarkeyword{constdefs}~c::\sigma~eqn$] combines declarations and
246 definitions of constants, using canonical name $c_def$ for the definitional
251 \subsection{Syntax and translations}\label{sec:syn-trans}
253 \indexisarcmd{syntax}\indexisarcmd{translations}
254 \begin{matharray}{rcl}
255 \isarcmd{syntax} & : & \isartrans{theory}{theory} \\
256 \isarcmd{translations} & : & \isartrans{theory}{theory} \\
260 'syntax' ('(' name 'output'? ')')? (constdecl +)
262 'translations' (transpat ('==' | '=>' | '<=') transpat comment? +)
264 transpat: ('(' nameref ')')? string
269 \item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$,
270 except that the actual logical signature extension is omitted. Thus the
271 context free grammar of Isabelle's inner syntax may be augmented in
272 arbitrary ways, independently of the logic. The $mode$ argument refers to
273 the print mode that the grammar rules belong; unless there is the
274 \texttt{output} flag given, all productions are added both to the input and
276 \item [$\isarkeyword{translations}~rules$] specifies syntactic translation
277 rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==}), parse rules
278 (\texttt{=>}), or print rules (\texttt{<=}). Translation patterns may be
279 prefixed by the syntactic category to be used for parsing; the default is
284 \subsection{Axioms and theorems}
286 \indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas}
287 \begin{matharray}{rcl}
288 \isarcmd{axioms} & : & \isartrans{theory}{theory} \\
289 \isarcmd{theorems} & : & \isartrans{theory}{theory} \\
290 \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
294 'axioms' (axmdecl prop comment? +)
296 ('theorems' | 'lemmas') thmdef? thmrefs
301 \item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as
302 axioms of the meta-logic. In fact, axioms are ``axiomatic theorems'', and
303 may be referred later just as any other theorem.
305 Axioms are usually only introduced when declaring new logical systems.
306 Everyday work is typically done the hard way, with proper definitions and
308 \item [$\isarkeyword{theorems}~a = \vec b$] stores lists of existing theorems.
309 Typical applications would also involve attributes, to augment the
310 Simplifier context, for example.
311 \item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but
312 tags the results as ``lemma''.
316 \subsection{Name spaces}
318 \indexisarcmd{global}\indexisarcmd{local}
319 \begin{matharray}{rcl}
320 \isarcmd{global} & : & \isartrans{theory}{theory} \\
321 \isarcmd{local} & : & \isartrans{theory}{theory} \\
324 Isabelle organizes any kind of name declarations (of types, constants,
325 theorems etc.) by hierarchically structured name spaces. Normally the user
326 never has to control the behavior of name space entry by hand, yet the
327 following commands provide some way to do so.
330 \item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current
331 name declaration mode. Initially, theories start in $\isarkeyword{local}$
332 mode, causing all names to be automatically qualified by the theory name.
333 Changing this to $\isarkeyword{global}$ causes all names to be declared
334 without the theory prefix, until $\isarkeyword{local}$ is declared again.
338 \subsection{Incorporating ML code}\label{sec:ML}
340 \indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{ML-setup}\indexisarcmd{setup}
341 \begin{matharray}{rcl}
342 \isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\
343 \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
344 \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
345 \isarcmd{setup} & : & \isartrans{theory}{theory} \\
348 \railalias{MLsetup}{ML\_setup}
354 ('ML' | MLsetup | 'setup') text
359 \item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$.
360 The current theory context (if present) is passed down to the ML session,
361 but may not be modified. Furthermore, the file name is checked with the
362 $\isarkeyword{files}$ dependency declaration given in the theory header (see
363 also \S\ref{sec:begin-thy}).
365 \item [$\isarkeyword{ML}~text$] executes ML commands from $text$. The theory
366 context is passed in the same way as for $\isarkeyword{use}$.
368 \item [$\isarkeyword{ML_setup}~text$] executes ML commands from $text$. The
369 theory context is passed down to the ML session, and fetched back
370 afterwards. Thus $text$ may actually change the theory as a side effect.
372 \item [$\isarkeyword{setup}~text$] changes the current theory context by
373 applying $text$, which refers to an ML expression of type $(theory \to
374 theory)~list$. The $\isarkeyword{setup}$ command is the canonical way to
375 initialize object-logic specific tools and packages written in ML.
380 %\subsection{Syntax translation functions}
382 %\indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}
383 %\indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}
384 %\indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}
385 %\begin{matharray}{rcl}
386 % \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
387 % \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
388 % \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
389 % \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
390 % \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
391 % \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
394 %Syntax translation functions written in ML admit almost arbitrary
395 %manipulations of Isabelle's inner syntax. Any of the above commands have a
396 %single \railqtoken{text} argument that refers to an ML expression of
397 %appropriate type. See \cite[\S8]{isabelle-ref} for more information on syntax
403 \indexisarcmd{oracle}
404 \begin{matharray}{rcl}
405 \isarcmd{oracle} & : & \isartrans{theory}{theory} \\
408 Oracles provide an interface to external reasoning systems, without giving up
409 control completely --- each theorem carries a derivation object recording any
410 oracle invocation. See \cite[\S6]{isabelle-ref} for more information.
413 'oracle' name '=' text comment?
418 \item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML
419 function $text$, which has to be of type $Sign\mathord.sg \times
420 Object\mathord.T \to term$.
424 \section{Proof commands}
426 Proof commands perform transitions of Isar/VM machine configurations, which
427 are block-structured, consisting of a stack of nodes with three main
428 components: logical proof context, current facts, and open goals. Isar/VM
429 transitions are \emph{typed} according to the following three three different
432 \item [$proof(prove)$] means that a new goal has just been stated that is now
433 to be \emph{proven}; the next command may refine it by some proof method
434 (read: tactic), and enter a sub-proof to establish the actual result.
435 \item [$proof(state)$] is like an internal theory mode: the context may be
436 augmented by \emph{stating} additional assumptions, intermediate results
438 \item [$proof(chain)$] is intermediate between $proof(state)$ and
439 $proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$''
440 register) have been just picked up in order to be used when refining the
445 \subsection{Proof markup commands}\label{sec:markup-prf}
447 \indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect}
448 \indexisarcmd{txt}\indexisarcmd{txt-raw}
449 \begin{matharray}{rcl}
450 \isarcmd{sect} & : & \isartrans{proof(state)}{proof(state)} \\
451 \isarcmd{subsect} & : & \isartrans{proof(state)}{proof(state)} \\
452 \isarcmd{subsubsect} & : & \isartrans{proof(state)}{proof(state)} \\
453 \isarcmd{txt} & : & \isartrans{proof(state)}{proof(state)} \\
454 \isarcmd{txt_raw} & : & \isartrans{proof(state)}{proof(state)} \\
457 These markup commands for proof mode closely correspond to the ones of theory
458 mode (see \S\ref{sec:markup-thy}). Note that $\isarkeyword{txt_raw}$ is
459 special in the same way as $\isarkeyword{text_raw}$.
461 \railalias{txtraw}{txt\_raw}
465 ('sect' | 'subsect' | 'subsubsect' | 'txt' | txtraw) text
470 \subsection{Proof context}\label{sec:proof-context}
472 \indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}
473 \begin{matharray}{rcl}
474 \isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\
475 \isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\
476 \isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\
477 \isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\
480 The logical proof context consists of fixed variables and assumptions. The
481 former closely correspond to Skolem constants, or meta-level universal
482 quantification as provided by the Isabelle/Pure logical framework.
483 Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in
484 a local value that may be used in the subsequent proof as any other variable
485 or constant. Furthermore, any result $\edrv \phi[x]$ exported from the
486 context will be universally closed wrt.\ $x$ at the outermost level: $\edrv
487 \All x \phi$ (this is expressed using Isabelle's meta-variables).
489 Similarly, introducing some assumption $\chi$ has two effects. On the one
490 hand, a local theorem is created that may be used as a fact in subsequent
491 proof steps. On the other hand, any result $\chi \drv \phi$ exported from the
492 context becomes conditional wrt.\ the assumption: $\edrv \chi \Imp \phi$.
493 Thus, solving an enclosing goal using such a result would basically introduce
494 a new subgoal stemming from the assumption. How this situation is handled
495 depends on the actual version of assumption command used: while $\ASSUMENAME$
496 insists on solving the subgoal by unification with some premise of the goal,
497 $\PRESUMENAME$ leaves the subgoal unchanged in order to be proved later by the
500 Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by
501 combining $\FIX x$ with another version of assumption that causes any
502 hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule.
503 Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
506 'fix' (vars + 'and') comment?
508 ('assume' | 'presume') (assm comment? + 'and')
510 'def' thmdecl? \\ var '==' term termpat? comment?
513 var: name ('::' type)?
515 vars: (name+) ('::' type)?
517 assm: thmdecl? (prop proppat? +)
522 \item [$\FIX{x}$] introduces a local \emph{arbitrary, but fixed} variable $x$.
523 \item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] introduce local theorems
524 $\Phi$ by assumption. Subsequent results applied to an enclosing goal
525 (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ expects to be
526 able to unify with existing premises in the goal, while $\PRESUMENAME$
527 leaves $\Phi$ as new subgoals.
529 Several lists of assumptions may be given (separated by
530 $\isarkeyword{and}$); the resulting list of current facts consists of all of
532 \item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
533 In results exported from the context, $x$ is replaced by $t$. Basically,
534 $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\ASSUME{}{x \equiv t}$, with the
535 resulting hypothetical equation solved by reflexivity.
537 The default name for the definitional equation is $x_def$.
540 The special name $prems$\indexisarthm{prems} refers to all assumptions of the
541 current context as a list of theorems.
544 \subsection{Facts and forward chaining}
546 \indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
547 \begin{matharray}{rcl}
548 \isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\
549 \isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\
550 \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\
551 \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
554 New facts are established either by assumption or proof of local statements.
555 Any fact will usually be involved in further proofs, either as explicit
556 arguments of proof methods or when forward chaining towards the next goal via
557 $\THEN$ (and variants). Note that the special theorem name
558 $this$\indexisarthm{this} refers to the most recently established facts.
560 'note' thmdef? thmrefs comment?
564 ('from' | 'with') thmrefs comment?
569 \item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result
570 as $a$. Note that attributes may be involved as well, both on the left and
572 \item [$\THEN$] indicates forward chaining by the current facts in order to
573 establish the goal to be claimed next. The initial proof method invoked to
574 refine that will be offered the facts to do ``anything appropriate'' (cf.\
575 also \S\ref{sec:proof-steps}). For example, method $rule$ (see
576 \S\ref{sec:pure-meth}) would typically do an elimination rather than an
577 introduction. Automatic methods usually insert the facts into the goal
578 state before operation.
579 \item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is
580 equivalent to $\FROM{this}$.
581 \item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward
582 chaining is from earlier facts together with the current ones.
585 Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth}) expect
586 multiple facts to be given in their proper order, corresponding to a prefix of
587 the premises of the rule involved. Note that positions may be easily skipped
588 using a form like $\FROM{\text{\texttt{_}}~a~b}$, for example. This involves
589 the trivial rule $\PROP\psi \Imp \PROP\psi$, which is bound in Isabelle/Pure
590 as ``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}}
593 \subsection{Goal statements}
595 \indexisarcmd{theorem}\indexisarcmd{lemma}
596 \indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
597 \begin{matharray}{rcl}
598 \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
599 \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
600 \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
601 \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
602 \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
603 \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
606 Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$
607 and $\LEMMANAME$. New local goals may be claimed within proof mode as well.
608 Four variants are available, indicating whether the result is meant to solve
609 some pending goal or whether forward chaining is employed.
612 ('theorem' | 'lemma') goal
614 ('have' | 'show' | 'hence' | 'thus') goal
617 goal: thmdecl? proppat comment?
622 \item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal,
623 eventually resulting in some theorem $\turn \phi$ put back into the theory.
624 \item [$\LEMMA{a}{\phi}$] is similar to $\THEOREMNAME$, but tags the result as
626 \item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a
627 theorem with the current assumption context as hypotheses.
628 \item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some
629 pending goal with the result \emph{exported} into the corresponding context
630 (cf.\ \S\ref{sec:proof-context}).
631 \item [$\HENCENAME$] abbreviates $\THEN~\HAVENAME$, i.e.\ claims a local goal
632 to be proven by forward chaining the current facts. Note that $\HENCENAME$
633 is also equivalent to $\FROM{this}~\HAVENAME$.
634 \item [$\THUSNAME$] abbreviates $\THEN~\SHOWNAME$. Note that $\THUSNAME$ is
635 also equivalent to $\FROM{this}~\SHOWNAME$.
639 \subsection{Initial and terminal proof steps}\label{sec:proof-steps}
641 \indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}
642 \indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}
643 \begin{matharray}{rcl}
644 \isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\
645 \isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
646 \isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
647 \isarcmd{.\,.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
648 \isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
649 \isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
652 Arbitrary goal refinement via tactics is considered harmful. Consequently the
653 Isar framework admits proof methods to be invoked in two places only.
655 \item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated
656 goal to a number of sub-goals that are to be solved later. Facts are passed
657 to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode.
659 \item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve
660 remaining goals. No facts are passed to $m@2$.
663 The only other proper way to affect pending goals is by $\SHOWNAME$ (or
664 $\THUSNAME$), which involves an explicit statement of what is to be solved.
668 Also note that initial proof methods should either solve the goal completely,
669 or constitute some well-understood reduction to new sub-goals. Arbitrary
670 automatic proof tools that are prone leave a large number of badly structured
671 sub-goals are no help in continuing the proof document in any intelligible
674 %A more appropriate technique would be to $\SHOWNAME$ some non-trivial
675 %reduction as an explicit rule, which is solved completely by some automated
676 %method, and then applied to some pending goal.
680 Unless given explicitly by the user, the default initial method is
681 ``$default$'', which is usually set up to apply a single standard elimination
682 or introduction rule according to the topmost symbol involved. There is no
683 separate default terminal method. In any case, any goals left after that are
684 solved by assumption as the very last step.
687 'proof' interest? meth? comment?
691 'by' meth meth? comment?
693 ('.' | '..' | 'sorry') comment?
696 meth: method interest?
701 \item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for
702 forward chaining are passed if so indicated by $proof(chain)$ mode.
703 \item [$\QED{m@2}$] refines any remaining goals by proof method $m@2$ and
704 concludes the sub-proof by assumption. If the goal had been $\SHOWNAME$ (or
705 $\THUSNAME$), some pending sub-goal is solved as well by the rule resulting
706 from the result \emph{exported} into the enclosing goal context. Thus
707 $\QEDNAME$ may fail for two reasons: either $m@2$ fails, or the resulting
708 rule does not fit to any pending goal\footnote{This includes any additional
709 ``strong'' assumptions as introduced by $\ASSUMENAME$.} of the enclosing
710 context. Debugging such a situation might involve temporarily changing
711 $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing
712 some occurrences of $\ASSUMENAME$ by $\PRESUMENAME$.
713 \item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it
714 abbreviates $\PROOF{m@1}~\QED{m@2}$, with backtracking across both methods,
715 though. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
716 by expanding its definition; in many cases $\PROOF{m@1}$ is already
717 sufficient to see what is going wrong.
718 \item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it
719 abbreviates $\BY{default}$.
720 \item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
721 abbreviates $\BY{assumption}$.
722 \item [$\isarkeyword{sorry}$] is a \emph{fake proof}\index{proof!fake};
723 provided that the \texttt{quick_and_dirty} flag is enabled,
724 $\isarkeyword{sorry}$ pretends to solve the goal without further ado. Of
725 course, the result is a fake theorem only, involving some oracle in its
726 internal derivation object (this is indicated as ``$[!]$'' in the printed
727 result). The main application of $\isarkeyword{sorry}$ is to support
728 experimentation and top-down proof development.
732 \subsection{Improper proof steps}
734 The following commands emulate unstructured tactic scripts to some extent.
735 While these are anathema for writing proper Isar proof documents, they might
736 come in handy for interactive exploration and debugging.
738 \indexisarcmd{apply}\indexisarcmd{then-apply}\indexisarcmd{back}
739 \begin{matharray}{rcl}
740 \isarcmd{apply}^* & : & \isartrans{proof}{proof} \\
741 \isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\
742 \isarcmd{back}^* & : & \isartrans{proof}{proof} \\
745 \railalias{thenapply}{then\_apply}
758 \item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in the plain old
759 tactic sense. Facts for forward chaining are reset.
760 \item [$\isarkeyword{then_apply}~(m)$] is similar to $\isarkeyword{apply}$,
761 but keeps the goal's facts.
762 \item [$\isarkeyword{back}$] does back-tracking over the result sequence of
763 the latest proof command.\footnote{Unlike the ML function \texttt{back}
764 \cite{isabelle-ref}, the Isar command does not search upwards for further
765 branch points.} Basically, any proof command may return multiple results.
769 \subsection{Term abbreviations}\label{sec:term-abbrev}
772 \begin{matharray}{rcl}
773 \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\
774 \isarkeyword{is} & : & syntax \\
777 Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,
778 or by annotating assumptions or goal statements with a list of patterns
779 $\ISS{p@1\;\dots}{p@n}$. In both cases, higher-order matching is invoked to
780 bind extra-logical term variables, which may be either named schematic
781 variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}''
782 (underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the
783 patterns occur on the left-hand side, while the $\ISNAME$ patterns are in
786 Term abbreviations are quite different from actual local definitions as
787 introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}). The latter are
788 visible within the logic as actual equations, while abbreviations disappear
789 during the input process just after type checking.
792 'let' ((term + 'as') '=' term comment? + 'and')
796 The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or
797 \railnonterm{proppat} (see \S\ref{sec:term-pats}).
800 \item [$\LET{\vec p = \vec t}$] binds any text variables in patters $\vec p$
801 by simultaneous higher-order matching against terms $\vec t$.
802 \item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the
803 preceding statement. Also note that $\ISNAME$ is not a separate command,
804 but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.).
807 A few \emph{automatic} term abbreviations\index{automatic abbreviation} for
808 goals and facts are available as well. For any open goal,
809 $\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition
810 (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its
811 (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its
812 object-logical statement. The latter two abstract over any meta-level
815 Fact statements resulting from assumptions or finished goals are bound as
816 $\Var{this_prop}$\indexisarvar{this-prop},
817 $\Var{this_concl}$\indexisarvar{this-concl}, and
818 $\Var{this}$\indexisarvar{this}, similar to $\Var{thesis}$ above. In case
819 $\Var{this}$ refers to an object-logic statement that is an application
820 $f(t)$, then $t$ is bound to the special text variable
821 ``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of
822 the latter are calculational proofs (see \S\ref{sec:calculation}).
825 \subsection{Block structure}
827 \indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}
828 \begin{matharray}{rcl}
829 \isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\
830 \BG & : & \isartrans{proof(state)}{proof(state)} \\
831 \EN & : & \isartrans{proof(state)}{proof(state)} \\
834 While Isar is inherently block-structured, opening and closing blocks is
835 mostly handled rather casually, with little explicit user-intervention. Any
836 local goal statement automatically opens \emph{two} blocks, which are closed
837 again when concluding the sub-proof (by $\QEDNAME$ etc.). Sections of
838 different context within a sub-proof may be switched via $\isarkeyword{next}$,
839 which is just a single block-close followed by block-open again. Thus the
840 effect of $\isarkeyword{next}$ to reset the local proof context. There is no
841 goal focus involved here!
843 For slightly more advanced applications, there are explicit block parentheses
844 as well. These typically achieve a stronger forward style of reasoning.
847 \item [$\isarkeyword{next}$] switches to a fresh block within a sub-proof,
848 resetting the local context to the initial one.
849 \item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and
850 close blocks. Any current facts pass through ``$\isarkeyword{\{\{}$''
851 unchanged, while ``$\isarkeyword{\}\}}$'' causes any result to be
852 \emph{exported} into the enclosing context. Thus fixed variables are
853 generalized, assumptions discharged, and local definitions unfolded (cf.\
854 \S\ref{sec:proof-context}). There is no difference of $\ASSUMENAME$ and
855 $\PRESUMENAME$ in this mode of forward reasoning --- in contrast to plain
856 backward reasoning with the result exported at $\SHOWNAME$ time.
860 \section{Other commands}
862 \subsection{Diagnostics}
864 \indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ}
865 \begin{matharray}{rcl}
866 \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\
867 \isarcmd{term} & : & \isarkeep{theory~|~proof} \\
868 \isarcmd{prop} & : & \isarkeep{theory~|~proof} \\
869 \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\
872 These commands are not part of the actual Isabelle/Isar syntax, but assist
873 interactive development. Also note that $undo$ does not apply here, since the
874 theory or proof configuration is not changed.
888 \item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current
889 theory or proof context. Note that any attributes included in the theorem
890 specifications are applied to a temporary context derived from the current
891 theory or proof; the result is discarded, i.e.\ attributes involved in
892 $thms$ do not have any permanent effect.
893 \item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-check and
894 print terms or propositions according to the current theory or proof
895 context; the inferred type of $t$ is output as well. Note that these
896 commands are also useful in inspecting the current environment of term
898 \item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic
899 according to the current theory or proof context.
903 \subsection{System operations}
905 \indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only}
906 \indexisarcmd{update-thy}\indexisarcmd{update-thy-only}
907 \begin{matharray}{rcl}
908 \isarcmd{cd} & : & \isarkeep{\cdot} \\
909 \isarcmd{pwd} & : & \isarkeep{\cdot} \\
910 \isarcmd{use_thy} & : & \isarkeep{\cdot} \\
911 \isarcmd{use_thy_only} & : & \isarkeep{\cdot} \\
912 \isarcmd{update_thy} & : & \isarkeep{\cdot} \\
913 \isarcmd{update_thy_only} & : & \isarkeep{\cdot} \\
917 \item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle
919 \item [$\isarkeyword{pwd}~$] prints the current working directory.
920 \item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$,
921 $\isarkeyword{update_thy}$, $\isarkeyword{update_thy_only}$] load some
922 theory given as $name$ argument. These commands are basically the same as
923 the corresponding ML functions\footnote{The ML versions also change the
924 implicit theory context to that of the theory loaded.} (see also
925 \cite[\S1,\S6]{isabelle-ref}). Note that both the ML and Isar versions may
926 load new- and old-style theories alike.
929 These system commands are scarcely used when working with the Proof~General
930 interface, since loading of theories is done fully transparently.
934 %%% TeX-master: "isar-ref"