3 \def\isabellecontext{pure}%
12 \isacommand{theory}\isamarkupfalse%
14 \isakeyword{imports}\ CPure\isanewline
23 \isamarkupchapter{Basic language elements \label{ch:pure-syntax}%
27 \begin{isamarkuptext}%
28 Subsequently, we introduce the main part of Pure theory and proof
29 commands, together with fundamental proof methods and attributes.
30 \Chref{ch:gen-tools} describes further Isar elements provided by
31 generic tools and packages (such as the Simplifier) that are either
32 part of Pure Isabelle or pre-installed in most object logics.
33 \Chref{ch:logics} refers to object-logic specific elements (mainly
36 \medskip Isar commands may be either \emph{proper} document
37 constructors, or \emph{improper commands}. Some proof methods and
38 attributes introduced later are classified as improper as well.
39 Improper Isar language elements, which are subsequently marked by
40 ``\isa{\isactrlsup {\isacharasterisk}}'', are often helpful when developing proof
41 documents, while their use is discouraged for the final
42 human-readable outcome. Typical examples are diagnostic commands
43 that print terms or theorems according to the current context; other
44 commands emulate old-style tactical theorem proving.%
48 \isamarkupsection{Theory commands%
52 \isamarkupsubsection{Defining theories \label{sec:begin-thy}%
56 \begin{isamarkuptext}%
57 \begin{matharray}{rcl}
58 \indexdef{}{command}{header}\mbox{\isa{\isacommand{header}}} & : & \isarkeep{toplevel} \\
59 \indexdef{}{command}{theory}\mbox{\isa{\isacommand{theory}}} & : & \isartrans{toplevel}{theory} \\
60 \indexdef{}{command}{end}\mbox{\isa{\isacommand{end}}} & : & \isartrans{theory}{toplevel} \\
63 Isabelle/Isar theories are defined via theory, which contain both
64 specifications and proofs; occasionally definitional mechanisms also
65 require some explicit proof.
67 The first ``real'' command of any theory has to be \mbox{\isa{\isacommand{theory}}}, which starts a new theory based on the merge of existing
68 ones. Just preceding the \mbox{\isa{\isacommand{theory}}} keyword, there may be
69 an optional \mbox{\isa{\isacommand{header}}} declaration, which is relevant to
70 document preparation only; it acts very much like a special
71 pre-theory markup command (cf.\ \secref{sec:markup-thy} and
72 \secref{sec:markup-thy}). The \mbox{\isa{\isacommand{end}}} command concludes a
73 theory development; it has to be the very last command of any theory
74 file loaded in batch-mode.
79 'theory' name 'imports' (name +) uses? 'begin'
82 uses: 'uses' ((name | parname) +);
87 \item [\mbox{\isa{\isacommand{header}}}~\isa{text}] provides plain text
88 markup just preceding the formal beginning of a theory. In actual
89 document preparation the corresponding {\LaTeX} macro \verb|\isamarkupheader| may be redefined to produce chapter or section
90 headings. See also \secref{sec:markup-thy} and
91 \secref{sec:markup-prf} for further markup commands.
93 \item [\mbox{\isa{\isacommand{theory}}}~\isa{A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}}] starts a new theory \isa{A} based on the
94 merge of existing theories \isa{B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n}.
96 Due to inclusion of several ancestors, the overall theory structure
97 emerging in an Isabelle session forms a directed acyclic graph
98 (DAG). Isabelle's theory loader ensures that the sources
99 contributing to the development graph are always up-to-date.
100 Changed files are automatically reloaded when processing theory
103 The optional \indexdef{}{keyword}{uses}\mbox{\isa{\isakeyword{uses}}} specification declares additional
104 dependencies on extra files (usually ML sources). Files will be
105 loaded immediately (as ML), unless the name is put in parentheses,
106 which merely documents the dependency to be resolved later in the
107 text (typically via explicit \indexref{}{command}{use}\mbox{\isa{\isacommand{use}}} in the body text,
108 see \secref{sec:ML}).
110 \item [\mbox{\isa{\isacommand{end}}}] concludes the current theory definition or
117 \isamarkupsubsection{Markup commands \label{sec:markup-thy}%
121 \begin{isamarkuptext}%
122 \begin{matharray}{rcl}
123 \indexdef{}{command}{chapter}\mbox{\isa{\isacommand{chapter}}} & : & \isarkeep{local{\dsh}theory} \\
124 \indexdef{}{command}{section}\mbox{\isa{\isacommand{section}}} & : & \isarkeep{local{\dsh}theory} \\
125 \indexdef{}{command}{subsection}\mbox{\isa{\isacommand{subsection}}} & : & \isarkeep{local{\dsh}theory} \\
126 \indexdef{}{command}{subsubsection}\mbox{\isa{\isacommand{subsubsection}}} & : & \isarkeep{local{\dsh}theory} \\
127 \indexdef{}{command}{text}\mbox{\isa{\isacommand{text}}} & : & \isarkeep{local{\dsh}theory} \\
128 \indexdef{}{command}{text-raw}\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}} & : & \isarkeep{local{\dsh}theory} \\
131 Apart from formal comments (see \secref{sec:comments}), markup
132 commands provide a structured way to insert text into the document
133 generated from a theory (see \cite{isabelle-sys} for more
134 information on Isabelle's document preparation tools).
137 ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
145 \item [\mbox{\isa{\isacommand{chapter}}}, \mbox{\isa{\isacommand{section}}}, \mbox{\isa{\isacommand{subsection}}}, and \mbox{\isa{\isacommand{subsubsection}}}] mark chapter and
148 \item [\mbox{\isa{\isacommand{text}}}] specifies paragraphs of plain text.
150 \item [\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}] inserts {\LaTeX} source into the
151 output, without additional markup. Thus the full range of document
152 manipulations becomes available.
156 The \isa{text} argument of these markup commands (except for
157 \mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}) may contain references to formal entities
158 (``antiquotations'', see also \secref{sec:antiq}). These are
159 interpreted in the present theory context, or the named \isa{target}.
161 Any of these markup elements corresponds to a {\LaTeX} command with
162 the name prefixed by \verb|\isamarkup|. For the sectioning
163 commands this is a plain macro with a single argument, e.g.\
164 \verb|\isamarkupchapter{|\isa{{\isasymdots}}\verb|}| for
165 \mbox{\isa{\isacommand{chapter}}}. The \mbox{\isa{\isacommand{text}}} markup results in a
166 {\LaTeX} environment \verb|\begin{isamarkuptext}| \isa{{\isasymdots}} \verb|\end{isamarkuptext}|, while \mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}
167 causes the text to be inserted directly into the {\LaTeX} source.
169 \medskip Additional markup commands are available for proofs (see
170 \secref{sec:markup-prf}). Also note that the \indexref{}{command}{header}\mbox{\isa{\isacommand{header}}} declaration (see \secref{sec:begin-thy}) admits to insert
171 section markup just preceding the actual theory definition.%
175 \isamarkupsubsection{Type classes and sorts \label{sec:classes}%
179 \begin{isamarkuptext}%
180 \begin{matharray}{rcll}
181 \indexdef{}{command}{classes}\mbox{\isa{\isacommand{classes}}} & : & \isartrans{theory}{theory} \\
182 \indexdef{}{command}{classrel}\mbox{\isa{\isacommand{classrel}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
183 \indexdef{}{command}{defaultsort}\mbox{\isa{\isacommand{defaultsort}}} & : & \isartrans{theory}{theory} \\
184 \indexdef{}{command}{class-deps}\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}} & : & \isarkeep{theory~|~proof} \\
188 'classes' (classdecl +)
190 'classrel' (nameref ('<' | subseteq) nameref + 'and')
198 \item [\mbox{\isa{\isacommand{classes}}}~\isa{c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n}]
199 declares class \isa{c} to be a subclass of existing classes \isa{c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n}. Cyclic class structures are not permitted.
201 \item [\mbox{\isa{\isacommand{classrel}}}~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}}] states
202 subclass relations between existing classes \isa{c\isactrlsub {\isadigit{1}}} and
203 \isa{c\isactrlsub {\isadigit{2}}}. This is done axiomatically! The \indexref{}{command}{instance}\mbox{\isa{\isacommand{instance}}} command (see \secref{sec:axclass}) provides a way to
204 introduce proven class relations.
206 \item [\mbox{\isa{\isacommand{defaultsort}}}~\isa{s}] makes sort \isa{s} the
207 new default sort for any type variables given without sort
208 constraints. Usually, the default sort would be only changed when
209 defining a new object-logic.
211 \item [\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}] visualizes the subclass relation,
212 using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
218 \isamarkupsubsection{Primitive types and type abbreviations \label{sec:types-pure}%
222 \begin{isamarkuptext}%
223 \begin{matharray}{rcll}
224 \indexdef{}{command}{types}\mbox{\isa{\isacommand{types}}} & : & \isartrans{theory}{theory} \\
225 \indexdef{}{command}{typedecl}\mbox{\isa{\isacommand{typedecl}}} & : & \isartrans{theory}{theory} \\
226 \indexdef{}{command}{nonterminals}\mbox{\isa{\isacommand{nonterminals}}} & : & \isartrans{theory}{theory} \\
227 \indexdef{}{command}{arities}\mbox{\isa{\isacommand{arities}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
231 'types' (typespec '=' type infix? +)
233 'typedecl' typespec infix?
235 'nonterminals' (name +)
237 'arities' (nameref '::' arity +)
243 \item [\mbox{\isa{\isacommand{types}}}~\isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ {\isasymtau}}]
244 introduces \emph{type synonym} \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t}
245 for existing type \isa{{\isasymtau}}. Unlike actual type definitions, as
246 are available in Isabelle/HOL for example, type synonyms are just
247 purely syntactic abbreviations without any logical significance.
248 Internally, type synonyms are fully expanded.
250 \item [\mbox{\isa{\isacommand{typedecl}}}~\isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t}]
251 declares a new type constructor \isa{t}, intended as an actual
252 logical type (of the object-logic, if available).
254 \item [\mbox{\isa{\isacommand{nonterminals}}}~\isa{c}] declares type
255 constructors \isa{c} (without arguments) to act as purely
256 syntactic types, i.e.\ nonterminal symbols of Isabelle's inner
257 syntax of terms or types.
259 \item [\mbox{\isa{\isacommand{arities}}}~\isa{t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s}] augments Isabelle's order-sorted signature of types by new type
260 constructor arities. This is done axiomatically! The \indexref{}{command}{instance}\mbox{\isa{\isacommand{instance}}} command (see \S\ref{sec:axclass}) provides a way to
261 introduce proven type arities.
267 \isamarkupsubsection{Primitive constants and definitions \label{sec:consts}%
271 \begin{isamarkuptext}%
272 Definitions essentially express abbreviations within the logic. The
273 simplest form of a definition is \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isasymequiv}\ t}, where \isa{c} is a newly declared constant. Isabelle also allows derived forms
274 where the arguments of \isa{c} appear on the left, abbreviating a
275 prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t} may be
276 written more conveniently as \isa{c\ x\ y\ {\isasymequiv}\ t}. Moreover,
277 definitions may be weakened by adding arbitrary pre-conditions:
278 \isa{A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t}.
280 \medskip The built-in well-formedness conditions for definitional
285 \item Arguments (on the left-hand side) must be distinct variables.
287 \item All variables on the right-hand side must also appear on the
290 \item All type variables on the right-hand side must also appear on
291 the left-hand side; this prohibits \isa{{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymequiv}\ length\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ list{\isacharparenright}} for example.
293 \item The definition must not be recursive. Most object-logics
294 provide definitional principles that can be used to express
299 Overloading means that a constant being declared as \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl} may be defined separately on type instances \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl} for each type constructor \isa{t}. The right-hand side may mention overloaded constants
300 recursively at type instances corresponding to the immediate
301 argument types \isa{{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n}. Incomplete
302 specification patterns impose global constraints on all occurrences,
303 e.g.\ \isa{d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}} on the left-hand side means that all
304 corresponding occurrences on some right-hand side need to be an
305 instance of this, general \isa{d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}} will be disallowed.
307 \begin{matharray}{rcl}
308 \indexdef{}{command}{consts}\mbox{\isa{\isacommand{consts}}} & : & \isartrans{theory}{theory} \\
309 \indexdef{}{command}{defs}\mbox{\isa{\isacommand{defs}}} & : & \isartrans{theory}{theory} \\
310 \indexdef{}{command}{constdefs}\mbox{\isa{\isacommand{constdefs}}} & : & \isartrans{theory}{theory} \\
314 'consts' ((name '::' type mixfix?) +)
316 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
321 'constdefs' structs? (constdecl? constdef +)
324 structs: '(' 'structure' (vars + 'and') ')'
326 constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
328 constdef: thmdecl? prop
334 \item [\mbox{\isa{\isacommand{consts}}}~\isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}] declares constant
335 \isa{c} to have any instance of type scheme \isa{{\isasymsigma}}. The
336 optional mixfix annotations may attach concrete syntax to the
339 \item [\mbox{\isa{\isacommand{defs}}}~\isa{name{\isacharcolon}\ eqn}] introduces \isa{eqn}
340 as a definitional axiom for some existing constant.
342 The \isa{{\isacharparenleft}unchecked{\isacharparenright}} option disables global dependency checks
343 for this definition, which is occasionally useful for exotic
344 overloading. It is at the discretion of the user to avoid malformed
345 theory specifications!
347 The \isa{{\isacharparenleft}overloaded{\isacharparenright}} option declares definitions to be
348 potentially overloaded. Unless this option is given, a warning
349 message would be issued for any definitional equation with a more
350 special type than that of the corresponding constant declaration.
352 \item [\mbox{\isa{\isacommand{constdefs}}}] provides a streamlined combination of
353 constants declarations and definitions: type-inference takes care of
354 the most general typing of the given specification (the optional
355 type constraint may refer to type-inference dummies ``\isa{{\isacharunderscore}}'' as usual). The resulting type declaration needs to agree with
356 that of the specification; overloading is \emph{not} supported here!
358 The constant name may be omitted altogether, if neither type nor
359 syntax declarations are given. The canonical name of the
360 definitional axiom for constant \isa{c} will be \isa{c{\isacharunderscore}def},
361 unless specified otherwise. Also note that the given list of
362 specifications is processed in a strictly sequential manner, with
363 type-checking being performed independently.
365 An optional initial context of \isa{{\isacharparenleft}structure{\isacharparenright}} declarations
366 admits use of indexed syntax, using the special symbol \verb|\<index>| (printed as ``\isa{{\isasymindex}}''). The latter concept is
367 particularly useful with locales (see also \S\ref{sec:locale}).
373 \isamarkupsubsection{Syntax and translations \label{sec:syn-trans}%
377 \begin{isamarkuptext}%
378 \begin{matharray}{rcl}
379 \indexdef{}{command}{syntax}\mbox{\isa{\isacommand{syntax}}} & : & \isartrans{theory}{theory} \\
380 \indexdef{}{command}{no-syntax}\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}} & : & \isartrans{theory}{theory} \\
381 \indexdef{}{command}{translations}\mbox{\isa{\isacommand{translations}}} & : & \isartrans{theory}{theory} \\
382 \indexdef{}{command}{no-translations}\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}} & : & \isartrans{theory}{theory} \\
385 \railalias{rightleftharpoons}{\isasymrightleftharpoons}
386 \railterm{rightleftharpoons}
388 \railalias{rightharpoonup}{\isasymrightharpoonup}
389 \railterm{rightharpoonup}
391 \railalias{leftharpoondown}{\isasymleftharpoondown}
392 \railterm{leftharpoondown}
395 ('syntax' | 'no\_syntax') mode? (constdecl +)
397 ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
400 mode: ('(' ( name | 'output' | name 'output' ) ')')
402 transpat: ('(' nameref ')')? string
408 \item [\mbox{\isa{\isacommand{syntax}}}~\isa{{\isacharparenleft}mode{\isacharparenright}\ decls}] is similar to
409 \mbox{\isa{\isacommand{consts}}}~\isa{decls}, except that the actual logical
410 signature extension is omitted. Thus the context free grammar of
411 Isabelle's inner syntax may be augmented in arbitrary ways,
412 independently of the logic. The \isa{mode} argument refers to the
413 print mode that the grammar rules belong; unless the \indexref{}{keyword}{output}\mbox{\isa{\isakeyword{output}}} indicator is given, all productions are added both to the
414 input and output grammar.
416 \item [\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}~\isa{{\isacharparenleft}mode{\isacharparenright}\ decls}] removes
417 grammar declarations (and translations) resulting from \isa{decls}, which are interpreted in the same manner as for \mbox{\isa{\isacommand{syntax}}} above.
419 \item [\mbox{\isa{\isacommand{translations}}}~\isa{rules}] specifies syntactic
420 translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isasymrightleftharpoons}}),
421 parse rules (\isa{{\isasymrightharpoonup}}), or print rules (\isa{{\isasymleftharpoondown}}).
422 Translation patterns may be prefixed by the syntactic category to be
423 used for parsing; the default is \isa{logic}.
425 \item [\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}~\isa{rules}] removes syntactic
426 translation rules, which are interpreted in the same manner as for
427 \mbox{\isa{\isacommand{translations}}} above.
433 \isamarkupsubsection{Axioms and theorems \label{sec:axms-thms}%
437 \begin{isamarkuptext}%
438 \begin{matharray}{rcll}
439 \indexdef{}{command}{axioms}\mbox{\isa{\isacommand{axioms}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
440 \indexdef{}{command}{lemmas}\mbox{\isa{\isacommand{lemmas}}} & : & \isarkeep{local{\dsh}theory} \\
441 \indexdef{}{command}{theorems}\mbox{\isa{\isacommand{theorems}}} & : & isarkeep{local{\dsh}theory} \\
445 'axioms' (axmdecl prop +)
447 ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
453 \item [\mbox{\isa{\isacommand{axioms}}}~\isa{a{\isacharcolon}\ {\isasymphi}}] introduces arbitrary
454 statements as axioms of the meta-logic. In fact, axioms are
455 ``axiomatic theorems'', and may be referred later just as any other
458 Axioms are usually only introduced when declaring new logical
459 systems. Everyday work is typically done the hard way, with proper
460 definitions and proven theorems.
462 \item [\mbox{\isa{\isacommand{lemmas}}}~\isa{a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n}]
463 retrieves and stores existing facts in the theory context, or the
464 specified target context (see also \secref{sec:target}). Typical
465 applications would also involve attributes, to declare Simplifier
468 \item [\mbox{\isa{\isacommand{theorems}}}] is essentially the same as \mbox{\isa{\isacommand{lemmas}}}, but marks the result as a different kind of facts.
474 \isamarkupsubsection{Name spaces%
478 \begin{isamarkuptext}%
479 \begin{matharray}{rcl}
480 \indexdef{}{command}{global}\mbox{\isa{\isacommand{global}}} & : & \isartrans{theory}{theory} \\
481 \indexdef{}{command}{local}\mbox{\isa{\isacommand{local}}} & : & \isartrans{theory}{theory} \\
482 \indexdef{}{command}{hide}\mbox{\isa{\isacommand{hide}}} & : & \isartrans{theory}{theory} \\
486 'hide' ('(open)')? name (nameref + )
490 Isabelle organizes any kind of name declarations (of types,
491 constants, theorems etc.) by separate hierarchically structured name
492 spaces. Normally the user does not have to control the behavior of
493 name spaces by hand, yet the following commands provide some way to
498 \item [\mbox{\isa{\isacommand{global}}} and \mbox{\isa{\isacommand{local}}}] change the
499 current name declaration mode. Initially, theories start in
500 \mbox{\isa{\isacommand{local}}} mode, causing all names to be automatically
501 qualified by the theory name. Changing this to \mbox{\isa{\isacommand{global}}}
502 causes all names to be declared without the theory prefix, until
503 \mbox{\isa{\isacommand{local}}} is declared again.
505 Note that global names are prone to get hidden accidently later,
506 when qualified names of the same base name are introduced.
508 \item [\mbox{\isa{\isacommand{hide}}}~\isa{space\ names}] fully removes
509 declarations from a given name space (which may be \isa{class},
510 \isa{type}, \isa{const}, or \isa{fact}); with the \isa{{\isacharparenleft}open{\isacharparenright}} option, only the base name is hidden. Global
511 (unqualified) names may never be hidden.
513 Note that hiding name space accesses has no impact on logical
514 declarations -- they remain valid internally. Entities that are no
515 longer accessible to the user are printed with the special qualifier
516 ``\isa{{\isacharquery}{\isacharquery}}'' prefixed to the full internal name.
522 \isamarkupsubsection{Incorporating ML code \label{sec:ML}%
526 \begin{isamarkuptext}%
527 \begin{matharray}{rcl}
528 \indexdef{}{command}{use}\mbox{\isa{\isacommand{use}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
529 \indexdef{}{command}{ML}\mbox{\isa{\isacommand{ML}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
530 \indexdef{}{command}{ML-val}\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}} & : & \isartrans{\cdot}{\cdot} \\
531 \indexdef{}{command}{ML-command}\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}} & : & \isartrans{\cdot}{\cdot} \\
532 \indexdef{}{command}{setup}\mbox{\isa{\isacommand{setup}}} & : & \isartrans{theory}{theory} \\
533 \indexdef{}{command}{method-setup}\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}} & : & \isartrans{theory}{theory} \\
539 ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text
541 'method\_setup' name '=' text text
547 \item [\mbox{\isa{\isacommand{use}}}~\isa{file}] reads and executes ML
548 commands from \isa{file}. The current theory context is passed
549 down to the ML toplevel and may be modified, using \verb|Context.>>| or derived ML commands. The file name is checked with
550 the \indexref{}{keyword}{uses}\mbox{\isa{\isakeyword{uses}}} dependency declaration given in the theory
551 header (see also \secref{sec:begin-thy}).
553 \item [\mbox{\isa{\isacommand{ML}}}~\isa{text}] is similar to \mbox{\isa{\isacommand{use}}}, but executes ML commands directly from the given \isa{text}.
555 \item [\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}} and \mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}] are
556 diagnostic versions of \mbox{\isa{\isacommand{ML}}}, which means that the context
557 may not be updated. \mbox{\isa{\isacommand{ML{\isacharunderscore}val}}} echos the bindings produced
558 at the ML toplevel, but \mbox{\isa{\isacommand{ML{\isacharunderscore}command}}} is silent.
560 \item [\mbox{\isa{\isacommand{setup}}}~\isa{text}] changes the current theory
561 context by applying \isa{text}, which refers to an ML expression
562 of type \verb|theory -> theory|. This enables to initialize
563 any object-logic specific tools and packages written in ML, for
566 \item [\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}~\isa{name\ {\isacharequal}\ text\ description}]
567 defines a proof method in the current theory. The given \isa{text} has to be an ML expression of type \verb|Args.src ->|\isasep\isanewline%
568 \verb| Proof.context -> Proof.method|. Parsing concrete method syntax
569 from \verb|Args.src| input can be quite tedious in general. The
570 following simple examples are for methods without any explicit
571 arguments, or a list of theorems, respectively.
573 %FIXME proper antiquotations
576 Method.no_args (Method.METHOD (fn facts => foobar_tac))
577 Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
578 Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
579 Method.thms_ctxt_args (fn thms => fn ctxt =>
580 Method.METHOD (fn facts => foobar_tac))
584 Note that mere tactic emulations may ignore the \isa{facts}
585 parameter above. Proper proof methods would do something
586 appropriate with the list of current facts, though. Single-rule
587 methods usually do strict forward-chaining (e.g.\ by using \verb|Drule.multi_resolves|), while automatic ones just insert the facts
588 using \verb|Method.insert_tac| before applying the main tactic.
594 \isamarkupsubsection{Syntax translation functions%
598 \begin{isamarkuptext}%
599 \begin{matharray}{rcl}
600 \indexdef{}{command}{parse-ast-translation}\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
601 \indexdef{}{command}{parse-translation}\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
602 \indexdef{}{command}{print-translation}\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
603 \indexdef{}{command}{typed-print-translation}\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
604 \indexdef{}{command}{print-ast-translation}\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
605 \indexdef{}{command}{token-translation}\mbox{\isa{\isacommand{token{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
609 ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
610 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
613 'token\_translation' text
617 Syntax translation functions written in ML admit almost arbitrary
618 manipulations of Isabelle's inner syntax. Any of the above commands
619 have a single \railqtok{text} argument that refers to an ML
620 expression of appropriate type, which are as follows by default:
622 %FIXME proper antiquotations
624 val parse_ast_translation : (string * (ast list -> ast)) list
625 val parse_translation : (string * (term list -> term)) list
626 val print_translation : (string * (term list -> term)) list
627 val typed_print_translation :
628 (string * (bool -> typ -> term list -> term)) list
629 val print_ast_translation : (string * (ast list -> ast)) list
630 val token_translation :
631 (string * string * (string -> string * real)) list
634 If the \isa{{\isacharparenleft}advanced{\isacharparenright}} option is given, the corresponding
635 translation functions may depend on the current theory or proof
636 context. This allows to implement advanced syntax mechanisms, as
637 translations functions may refer to specific theory declarations or
638 auxiliary proof data.
640 See also \cite[\S8]{isabelle-ref} for more information on the
641 general concept of syntax transformations in Isabelle.
643 %FIXME proper antiquotations
645 val parse_ast_translation:
646 (string * (Context.generic -> ast list -> ast)) list
647 val parse_translation:
648 (string * (Context.generic -> term list -> term)) list
649 val print_translation:
650 (string * (Context.generic -> term list -> term)) list
651 val typed_print_translation:
652 (string * (Context.generic -> bool -> typ -> term list -> term)) list
653 val print_ast_translation:
654 (string * (Context.generic -> ast list -> ast)) list
659 \isamarkupsubsection{Oracles%
663 \begin{isamarkuptext}%
664 \begin{matharray}{rcl}
665 \indexdef{}{command}{oracle}\mbox{\isa{\isacommand{oracle}}} & : & \isartrans{theory}{theory} \\
668 The oracle interface promotes a given ML function \verb|theory -> T -> term| to \verb|theory -> T -> thm|, for some
669 type \verb|T| given by the user. This acts like an infinitary
670 specification of axioms -- there is no internal check of the
671 correctness of the results! The inference kernel records oracle
672 invocations within the internal derivation object of theorems, and
673 the pretty printer attaches ``\isa{{\isacharbrackleft}{\isacharbang}{\isacharbrackright}}'' to indicate results
674 that are not fully checked by Isabelle inferences.
677 'oracle' name '(' type ')' '=' text
683 \item [\mbox{\isa{\isacommand{oracle}}}~\isa{name\ {\isacharparenleft}type{\isacharparenright}\ {\isacharequal}\ text}] turns the
684 given ML expression \isa{text} of type
685 \verb|theory ->|~\isa{type}~\verb|-> term| into an
687 \verb|theory ->|~\isa{type}~\verb|-> thm|, which is
688 bound to the global identifier \verb|name|.
694 \isamarkupsection{Proof commands%
698 \begin{isamarkuptext}%
699 Proof commands perform transitions of Isar/VM machine
700 configurations, which are block-structured, consisting of a stack of
701 nodes with three main components: logical proof context, current
702 facts, and open goals. Isar/VM transitions are \emph{typed}
703 according to the following three different modes of operation:
707 \item [\isa{proof{\isacharparenleft}prove{\isacharparenright}}] means that a new goal has just been
708 stated that is now to be \emph{proven}; the next command may refine
709 it by some proof method, and enter a sub-proof to establish the
712 \item [\isa{proof{\isacharparenleft}state{\isacharparenright}}] is like a nested theory mode: the
713 context may be augmented by \emph{stating} additional assumptions,
714 intermediate results etc.
716 \item [\isa{proof{\isacharparenleft}chain{\isacharparenright}}] is intermediate between \isa{proof{\isacharparenleft}state{\isacharparenright}} and \isa{proof{\isacharparenleft}prove{\isacharparenright}}: existing facts (i.e.\
717 the contents of the special ``\indexref{}{fact}{this}\mbox{\isa{this}}'' register) have been
718 just picked up in order to be used when refining the goal claimed
723 The proof mode indicator may be read as a verb telling the writer
724 what kind of operation may be performed next. The corresponding
725 typings of proof commands restricts the shape of well-formed proof
726 texts to particular command sequences. So dynamic arrangements of
727 commands eventually turn out as static texts of a certain structure.
728 \Appref{ap:refcard} gives a simplified grammar of the overall
729 (extensible) language emerging that way.%
733 \isamarkupsubsection{Markup commands \label{sec:markup-prf}%
737 \begin{isamarkuptext}%
738 \begin{matharray}{rcl}
739 \indexdef{}{command}{sect}\mbox{\isa{\isacommand{sect}}} & : & \isartrans{proof}{proof} \\
740 \indexdef{}{command}{subsect}\mbox{\isa{\isacommand{subsect}}} & : & \isartrans{proof}{proof} \\
741 \indexdef{}{command}{subsubsect}\mbox{\isa{\isacommand{subsubsect}}} & : & \isartrans{proof}{proof} \\
742 \indexdef{}{command}{txt}\mbox{\isa{\isacommand{txt}}} & : & \isartrans{proof}{proof} \\
743 \indexdef{}{command}{txt-raw}\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}} & : & \isartrans{proof}{proof} \\
746 These markup commands for proof mode closely correspond to the ones
747 of theory mode (see \S\ref{sec:markup-thy}).
750 ('sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
756 \isamarkupsubsection{Context elements \label{sec:proof-context}%
760 \begin{isamarkuptext}%
761 \begin{matharray}{rcl}
762 \indexdef{}{command}{fix}\mbox{\isa{\isacommand{fix}}} & : & \isartrans{proof(state)}{proof(state)} \\
763 \indexdef{}{command}{assume}\mbox{\isa{\isacommand{assume}}} & : & \isartrans{proof(state)}{proof(state)} \\
764 \indexdef{}{command}{presume}\mbox{\isa{\isacommand{presume}}} & : & \isartrans{proof(state)}{proof(state)} \\
765 \indexdef{}{command}{def}\mbox{\isa{\isacommand{def}}} & : & \isartrans{proof(state)}{proof(state)} \\
768 The logical proof context consists of fixed variables and
769 assumptions. The former closely correspond to Skolem constants, or
770 meta-level universal quantification as provided by the Isabelle/Pure
771 logical framework. Introducing some \emph{arbitrary, but fixed}
772 variable via ``\mbox{\isa{\isacommand{fix}}}~\isa{x}'' results in a local value
773 that may be used in the subsequent proof as any other variable or
774 constant. Furthermore, any result \isa{{\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} exported from
775 the context will be universally closed wrt.\ \isa{x} at the
776 outermost level: \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} (this is expressed in normal
777 form using Isabelle's meta-variables).
779 Similarly, introducing some assumption \isa{{\isasymchi}} has two effects.
780 On the one hand, a local theorem is created that may be used as a
781 fact in subsequent proof steps. On the other hand, any result
782 \isa{{\isasymchi}\ {\isasymturnstile}\ {\isasymphi}} exported from the context becomes conditional wrt.\
783 the assumption: \isa{{\isasymturnstile}\ {\isasymchi}\ {\isasymLongrightarrow}\ {\isasymphi}}. Thus, solving an enclosing goal
784 using such a result would basically introduce a new subgoal stemming
785 from the assumption. How this situation is handled depends on the
786 version of assumption command used: while \mbox{\isa{\isacommand{assume}}}
787 insists on solving the subgoal by unification with some premise of
788 the goal, \mbox{\isa{\isacommand{presume}}} leaves the subgoal unchanged in order
789 to be proved later by the user.
791 Local definitions, introduced by ``\mbox{\isa{\isacommand{def}}}~\isa{x\ {\isasymequiv}\ t}'', are achieved by combining ``\mbox{\isa{\isacommand{fix}}}~\isa{x}'' with
792 another version of assumption that causes any hypothetical equation
793 \isa{x\ {\isasymequiv}\ t} to be eliminated by the reflexivity rule. Thus,
794 exporting some result \isa{x\ {\isasymequiv}\ t\ {\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} yields \isa{{\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}t{\isacharbrackright}}.
796 \railalias{equiv}{\isasymequiv}
802 ('assume' | 'presume') (props + 'and')
806 def: thmdecl? \\ name ('==' | equiv) term termpat?
812 \item [\mbox{\isa{\isacommand{fix}}}~\isa{x}] introduces a local variable
813 \isa{x} that is \emph{arbitrary, but fixed.}
815 \item [\mbox{\isa{\isacommand{assume}}}~\isa{a{\isacharcolon}\ {\isasymphi}} and \mbox{\isa{\isacommand{presume}}}~\isa{a{\isacharcolon}\ {\isasymphi}}] introduce a local fact \isa{{\isasymphi}\ {\isasymturnstile}\ {\isasymphi}} by
816 assumption. Subsequent results applied to an enclosing goal (e.g.\
817 by \indexref{}{command}{show}\mbox{\isa{\isacommand{show}}}) are handled as follows: \mbox{\isa{\isacommand{assume}}} expects to be able to unify with existing premises in the
818 goal, while \mbox{\isa{\isacommand{presume}}} leaves \isa{{\isasymphi}} as new subgoals.
820 Several lists of assumptions may be given (separated by
821 \indexref{}{keyword}{and}\mbox{\isa{\isakeyword{and}}}; the resulting list of current facts consists
822 of all of these concatenated.
824 \item [\mbox{\isa{\isacommand{def}}}~\isa{x\ {\isasymequiv}\ t}] introduces a local
825 (non-polymorphic) definition. In results exported from the context,
826 \isa{x} is replaced by \isa{t}. Basically, ``\mbox{\isa{\isacommand{def}}}~\isa{x\ {\isasymequiv}\ t}'' abbreviates ``\mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{x\ {\isasymequiv}\ t}'', with the resulting
827 hypothetical equation solved by reflexivity.
829 The default name for the definitional equation is \isa{x{\isacharunderscore}def}.
830 Several simultaneous definitions may be given at the same time.
834 The special name \indexref{}{fact}{prems}\mbox{\isa{prems}} refers to all assumptions of the
835 current context as a list of theorems. This feature should be used
836 with great care! It is better avoided in final proof texts.%
840 \isamarkupsubsection{Facts and forward chaining%
844 \begin{isamarkuptext}%
845 \begin{matharray}{rcl}
846 \indexdef{}{command}{note}\mbox{\isa{\isacommand{note}}} & : & \isartrans{proof(state)}{proof(state)} \\
847 \indexdef{}{command}{then}\mbox{\isa{\isacommand{then}}} & : & \isartrans{proof(state)}{proof(chain)} \\
848 \indexdef{}{command}{from}\mbox{\isa{\isacommand{from}}} & : & \isartrans{proof(state)}{proof(chain)} \\
849 \indexdef{}{command}{with}\mbox{\isa{\isacommand{with}}} & : & \isartrans{proof(state)}{proof(chain)} \\
850 \indexdef{}{command}{using}\mbox{\isa{\isacommand{using}}} & : & \isartrans{proof(prove)}{proof(prove)} \\
851 \indexdef{}{command}{unfolding}\mbox{\isa{\isacommand{unfolding}}} & : & \isartrans{proof(prove)}{proof(prove)} \\
854 New facts are established either by assumption or proof of local
855 statements. Any fact will usually be involved in further proofs,
856 either as explicit arguments of proof methods, or when forward
857 chaining towards the next goal via \mbox{\isa{\isacommand{then}}} (and variants);
858 \mbox{\isa{\isacommand{from}}} and \mbox{\isa{\isacommand{with}}} are composite forms
859 involving \mbox{\isa{\isacommand{note}}}. The \mbox{\isa{\isacommand{using}}} elements
860 augments the collection of used facts \emph{after} a goal has been
861 stated. Note that the special theorem name \indexref{}{fact}{this}\mbox{\isa{this}} refers
862 to the most recently established facts, but only \emph{before}
863 issuing a follow-up claim.
866 'note' (thmdef? thmrefs + 'and')
868 ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
874 \item [\mbox{\isa{\isacommand{note}}}~\isa{a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n}]
875 recalls existing facts \isa{b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub n}, binding
876 the result as \isa{a}. Note that attributes may be involved as
877 well, both on the left and right hand sides.
879 \item [\mbox{\isa{\isacommand{then}}}] indicates forward chaining by the current
880 facts in order to establish the goal to be claimed next. The
881 initial proof method invoked to refine that will be offered the
882 facts to do ``anything appropriate'' (see also
883 \secref{sec:proof-steps}). For example, method \indexref{}{method}{rule}\mbox{\isa{rule}}
884 (see \secref{sec:pure-meth-att}) would typically do an elimination
885 rather than an introduction. Automatic methods usually insert the
886 facts into the goal state before operation. This provides a simple
887 scheme to control relevance of facts in automated proof search.
889 \item [\mbox{\isa{\isacommand{from}}}~\isa{b}] abbreviates ``\mbox{\isa{\isacommand{note}}}~\isa{b}~\mbox{\isa{\isacommand{then}}}''; thus \mbox{\isa{\isacommand{then}}} is
890 equivalent to ``\mbox{\isa{\isacommand{from}}}~\isa{this}''.
892 \item [\mbox{\isa{\isacommand{with}}}~\isa{b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n}]
893 abbreviates ``\mbox{\isa{\isacommand{from}}}~\isa{b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n\ {\isasymAND}\ this}''; thus the forward chaining is from earlier facts together
894 with the current ones.
896 \item [\mbox{\isa{\isacommand{using}}}~\isa{b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n}] augments
897 the facts being currently indicated for use by a subsequent
898 refinement step (such as \indexref{}{command}{apply}\mbox{\isa{\isacommand{apply}}} or \indexref{}{command}{proof}\mbox{\isa{\isacommand{proof}}}).
900 \item [\mbox{\isa{\isacommand{unfolding}}}~\isa{b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n}] is
901 structurally similar to \mbox{\isa{\isacommand{using}}}, but unfolds definitional
902 equations \isa{b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ b\isactrlsub n} throughout the goal state
907 Forward chaining with an empty list of theorems is the same as not
908 chaining at all. Thus ``\mbox{\isa{\isacommand{from}}}~\isa{nothing}'' has no
909 effect apart from entering \isa{prove{\isacharparenleft}chain{\isacharparenright}} mode, since
910 \indexref{}{fact}{nothing}\mbox{\isa{nothing}} is bound to the empty list of theorems.
912 Basic proof methods (such as \indexref{}{method}{rule}\mbox{\isa{rule}}) expect multiple
913 facts to be given in their proper order, corresponding to a prefix
914 of the premises of the rule involved. Note that positions may be
915 easily skipped using something like \mbox{\isa{\isacommand{from}}}~\isa{{\isacharunderscore}\ {\isasymAND}\ a\ {\isasymAND}\ b}, for example. This involves the trivial rule
916 \isa{PROP\ {\isasympsi}\ {\isasymLongrightarrow}\ PROP\ {\isasympsi}}, which is bound in Isabelle/Pure as
917 ``\indexref{}{fact}{-}\mbox{\isa{{\isacharunderscore}}}'' (underscore).
919 Automated methods (such as \mbox{\isa{simp}} or \mbox{\isa{auto}}) just
920 insert any given facts before their usual operation. Depending on
921 the kind of procedure involved, the order of facts is less
926 \isamarkupsubsection{Goal statements \label{sec:goals}%
930 \begin{isamarkuptext}%
931 \begin{matharray}{rcl}
932 \isarcmd{lemma} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
933 \isarcmd{theorem} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
934 \isarcmd{corollary} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
935 \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
936 \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
937 \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
938 \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
939 \isarcmd{print_statement}^* & : & \isarkeep{theory~|~proof} \\
942 From a theory context, proof mode is entered by an initial goal
943 command such as \mbox{\isa{\isacommand{lemma}}}, \mbox{\isa{\isacommand{theorem}}}, or
944 \mbox{\isa{\isacommand{corollary}}}. Within a proof, new claims may be
945 introduced locally as well; four variants are available here to
946 indicate whether forward chaining of facts should be performed
947 initially (via \indexref{}{command}{then}\mbox{\isa{\isacommand{then}}}), and whether the final result
948 is meant to solve some pending goal.
950 Goals may consist of multiple statements, resulting in a list of
951 facts eventually. A pending multi-goal is internally represented as
952 a meta-level conjunction (printed as \isa{{\isacharampersand}{\isacharampersand}}), which is usually
953 split into the corresponding number of sub-goals prior to an initial
954 method application, via \indexref{}{command}{proof}\mbox{\isa{\isacommand{proof}}}
955 (\secref{sec:proof-steps}) or \indexref{}{command}{apply}\mbox{\isa{\isacommand{apply}}}
956 (\secref{sec:tactic-commands}). The \indexref{}{method}{induct}\mbox{\isa{induct}} method
957 covered in \secref{sec:cases-induct} acts on multiple claims
960 Claims at the theory level may be either in short or long form. A
961 short goal merely consists of several simultaneous propositions
962 (often just one). A long goal includes an explicit context
963 specification for the subsequent conclusion, involving local
964 parameters and assumptions. Here the role of each part of the
965 statement is explicitly marked by separate keywords (see also
966 \secref{sec:locale}); the local assumptions being introduced here
967 are available as \indexref{}{fact}{assms}\mbox{\isa{assms}} in the proof. Moreover, there
968 are two kinds of conclusions: \indexdef{}{element}{shows}\mbox{\isa{shows}} states several
969 simultaneous propositions (essentially a big conjunction), while
970 \indexdef{}{element}{obtains}\mbox{\isa{obtains}} claims several simultaneous simultaneous
971 contexts of (essentially a big disjunction of eliminated parameters
972 and assumptions, cf.\ \secref{sec:obtain}).
975 ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
977 ('have' | 'show' | 'hence' | 'thus') goal
979 'print\_statement' modes? thmrefs
982 goal: (props + 'and')
984 longgoal: thmdecl? (contextelem *) conclusion
986 conclusion: 'shows' goal | 'obtains' (parname? case + '|')
988 case: (vars + 'and') 'where' (props + 'and')
994 \item [\mbox{\isa{\isacommand{lemma}}}~\isa{a{\isacharcolon}\ {\isasymphi}}] enters proof mode with
995 \isa{{\isasymphi}} as main goal, eventually resulting in some fact \isa{{\isasymturnstile}\ {\isasymphi}} to be put back into the target context. An additional
996 \railnonterm{context} specification may build up an initial proof
997 context for the subsequent claim; this includes local definitions
998 and syntax as well, see the definition of \mbox{\isa{contextelem}} in
1001 \item [\mbox{\isa{\isacommand{theorem}}}~\isa{a{\isacharcolon}\ {\isasymphi}} and \mbox{\isa{\isacommand{corollary}}}~\isa{a{\isacharcolon}\ {\isasymphi}}] are essentially the same as \mbox{\isa{\isacommand{lemma}}}~\isa{a{\isacharcolon}\ {\isasymphi}}, but the facts are internally marked as
1002 being of a different kind. This discrimination acts like a formal
1005 \item [\mbox{\isa{\isacommand{have}}}~\isa{a{\isacharcolon}\ {\isasymphi}}] claims a local goal,
1006 eventually resulting in a fact within the current logical context.
1007 This operation is completely independent of any pending sub-goals of
1008 an enclosing goal statements, so \mbox{\isa{\isacommand{have}}} may be freely
1009 used for experimental exploration of potential results within a
1012 \item [\mbox{\isa{\isacommand{show}}}~\isa{a{\isacharcolon}\ {\isasymphi}}] is like \mbox{\isa{\isacommand{have}}}~\isa{a{\isacharcolon}\ {\isasymphi}} plus a second stage to refine some pending
1013 sub-goal for each one of the finished result, after having been
1014 exported into the corresponding context (at the head of the
1015 sub-proof of this \mbox{\isa{\isacommand{show}}} command).
1017 To accommodate interactive debugging, resulting rules are printed
1018 before being applied internally. Even more, interactive execution
1019 of \mbox{\isa{\isacommand{show}}} predicts potential failure and displays the
1020 resulting error as a warning beforehand. Watch out for the
1023 %FIXME proper antiquitation
1025 Problem! Local statement will fail to solve any pending goal
1028 \item [\mbox{\isa{\isacommand{hence}}}] abbreviates ``\mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{have}}}'', i.e.\ claims a local goal to be proven by forward
1029 chaining the current facts. Note that \mbox{\isa{\isacommand{hence}}} is also
1030 equivalent to ``\mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{have}}}''.
1032 \item [\mbox{\isa{\isacommand{thus}}}] abbreviates ``\mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{show}}}''. Note that \mbox{\isa{\isacommand{thus}}} is also equivalent to
1033 ``\mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{show}}}''.
1035 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}statement}}}~\isa{a}] prints facts from the
1036 current theory or proof context in long statement form, according to
1037 the syntax for \mbox{\isa{\isacommand{lemma}}} given above.
1041 Any goal statement causes some term abbreviations (such as
1042 \indexref{}{variable}{?thesis}\mbox{\isa{{\isacharquery}thesis}}) to be bound automatically, see also
1043 \secref{sec:term-abbrev}. Furthermore, the local context of a
1044 (non-atomic) goal is provided via the \indexref{}{case}{rule-context}\mbox{\isa{rule{\isacharunderscore}context}} case.
1046 The optional case names of \indexref{}{element}{obtains}\mbox{\isa{obtains}} have a twofold
1047 meaning: (1) during the of this claim they refer to the the local
1048 context introductions, (2) the resulting rule is annotated
1049 accordingly to support symbolic case splits when used with the
1050 \indexref{}{method}{cases}\mbox{\isa{cases}} method (cf. \secref{sec:cases-induct}).
1055 Isabelle/Isar suffers theory-level goal statements to contain
1056 \emph{unbound schematic variables}, although this does not conform
1057 to the aim of human-readable proof documents! The main problem
1058 with schematic goals is that the actual outcome is usually hard to
1059 predict, depending on the behavior of the proof methods applied
1060 during the course of reasoning. Note that most semi-automated
1061 methods heavily depend on several kinds of implicit rule
1062 declarations within the current theory context. As this would
1063 also result in non-compositional checking of sub-proofs,
1064 \emph{local goals} are not allowed to be schematic at all.
1065 Nevertheless, schematic goals do have their use in Prolog-style
1066 interactive synthesis of proven results, usually by stepwise
1067 refinement via emulation of traditional Isabelle tactic scripts
1068 (see also \secref{sec:tactic-commands}). In any case, users
1069 should know what they are doing.
1071 \end{isamarkuptext}%
1074 \isamarkupsubsection{Initial and terminal proof steps \label{sec:proof-steps}%
1078 \begin{isamarkuptext}%
1079 \begin{matharray}{rcl}
1080 \indexdef{}{command}{proof}\mbox{\isa{\isacommand{proof}}} & : & \isartrans{proof(prove)}{proof(state)} \\
1081 \indexdef{}{command}{qed}\mbox{\isa{\isacommand{qed}}} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
1082 \indexdef{}{command}{by}\mbox{\isa{\isacommand{by}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
1083 \indexdef{}{command}{..}\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
1084 \indexdef{}{command}{.}\mbox{\isa{\isacommand{{\isachardot}}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
1085 \indexdef{}{command}{sorry}\mbox{\isa{\isacommand{sorry}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
1088 Arbitrary goal refinement via tactics is considered harmful.
1089 Structured proof composition in Isar admits proof methods to be
1090 invoked in two places only.
1094 \item An \emph{initial} refinement step \indexref{}{command}{proof}\mbox{\isa{\isacommand{proof}}}~\isa{m\isactrlsub {\isadigit{1}}} reduces a newly stated goal to a number
1095 of sub-goals that are to be solved later. Facts are passed to
1096 \isa{m\isactrlsub {\isadigit{1}}} for forward chaining, if so indicated by \isa{proof{\isacharparenleft}chain{\isacharparenright}} mode.
1098 \item A \emph{terminal} conclusion step \indexref{}{command}{qed}\mbox{\isa{\isacommand{qed}}}~\isa{m\isactrlsub {\isadigit{2}}} is intended to solve remaining goals. No facts are
1099 passed to \isa{m\isactrlsub {\isadigit{2}}}.
1103 The only other (proper) way to affect pending goals in a proof body
1104 is by \indexref{}{command}{show}\mbox{\isa{\isacommand{show}}}, which involves an explicit statement of
1105 what is to be solved eventually. Thus we avoid the fundamental
1106 problem of unstructured tactic scripts that consist of numerous
1107 consecutive goal transformations, with invisible effects.
1109 \medskip As a general rule of thumb for good proof style, initial
1110 proof methods should either solve the goal completely, or constitute
1111 some well-understood reduction to new sub-goals. Arbitrary
1112 automatic proof tools that are prone leave a large number of badly
1113 structured sub-goals are no help in continuing the proof document in
1114 an intelligible manner.
1116 Unless given explicitly by the user, the default initial method is
1117 ``\indexref{}{method}{rule}\mbox{\isa{rule}}'', which applies a single standard elimination
1118 or introduction rule according to the topmost symbol involved.
1119 There is no separate default terminal method. Any remaining goals
1120 are always solved by assumption in the very last step.
1129 ('.' | '..' | 'sorry')
1135 \item [\mbox{\isa{\isacommand{proof}}}~\isa{m\isactrlsub {\isadigit{1}}}] refines the goal by
1136 proof method \isa{m\isactrlsub {\isadigit{1}}}; facts for forward chaining are
1137 passed if so indicated by \isa{proof{\isacharparenleft}chain{\isacharparenright}} mode.
1139 \item [\mbox{\isa{\isacommand{qed}}}~\isa{m\isactrlsub {\isadigit{2}}}] refines any remaining
1140 goals by proof method \isa{m\isactrlsub {\isadigit{2}}} and concludes the
1141 sub-proof by assumption. If the goal had been \isa{show} (or
1142 \isa{thus}), some pending sub-goal is solved as well by the rule
1143 resulting from the result \emph{exported} into the enclosing goal
1144 context. Thus \isa{qed} may fail for two reasons: either \isa{m\isactrlsub {\isadigit{2}}} fails, or the resulting rule does not fit to any
1145 pending goal\footnote{This includes any additional ``strong''
1146 assumptions as introduced by \mbox{\isa{\isacommand{assume}}}.} of the enclosing
1147 context. Debugging such a situation might involve temporarily
1148 changing \mbox{\isa{\isacommand{show}}} into \mbox{\isa{\isacommand{have}}}, or weakening the
1149 local context by replacing occurrences of \mbox{\isa{\isacommand{assume}}} by
1150 \mbox{\isa{\isacommand{presume}}}.
1152 \item [\mbox{\isa{\isacommand{by}}}~\isa{m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}}] is a
1153 \emph{terminal proof}\index{proof!terminal}; it abbreviates
1154 \mbox{\isa{\isacommand{proof}}}~\isa{m\isactrlsub {\isadigit{1}}}~\isa{qed}~\isa{m\isactrlsub {\isadigit{2}}}, but with backtracking across both methods. Debugging
1155 an unsuccessful \mbox{\isa{\isacommand{by}}}~\isa{m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}}
1156 command can be done by expanding its definition; in many cases
1157 \mbox{\isa{\isacommand{proof}}}~\isa{m\isactrlsub {\isadigit{1}}} (or even \isa{apply}~\isa{m\isactrlsub {\isadigit{1}}}) is already sufficient to see the
1160 \item [``\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}''] is a \emph{default
1161 proof}\index{proof!default}; it abbreviates \mbox{\isa{\isacommand{by}}}~\isa{rule}.
1163 \item [``\mbox{\isa{\isacommand{{\isachardot}}}}''] is a \emph{trivial
1164 proof}\index{proof!trivial}; it abbreviates \mbox{\isa{\isacommand{by}}}~\isa{this}.
1166 \item [\mbox{\isa{\isacommand{sorry}}}] is a \emph{fake proof}\index{proof!fake}
1167 pretending to solve the pending claim without further ado. This
1168 only works in interactive development, or if the \verb|quick_and_dirty| flag is enabled (in ML). Facts emerging from fake
1169 proofs are not the real thing. Internally, each theorem container
1170 is tainted by an oracle invocation, which is indicated as ``\isa{{\isacharbrackleft}{\isacharbang}{\isacharbrackright}}'' in the printed result.
1172 The most important application of \mbox{\isa{\isacommand{sorry}}} is to support
1173 experimentation and top-down proof development.
1176 \end{isamarkuptext}%
1179 \isamarkupsubsection{Fundamental methods and attributes \label{sec:pure-meth-att}%
1183 \begin{isamarkuptext}%
1184 The following proof methods and attributes refer to basic logical
1185 operations of Isar. Further methods and attributes are provided by
1186 several generic and object-logic specific tools and packages (see
1187 \chref{ch:gen-tools} and \chref{ch:logics}).
1189 \begin{matharray}{rcl}
1190 \indexdef{}{method}{-}\mbox{\isa{{\isacharminus}}} & : & \isarmeth \\
1191 \indexdef{}{method}{fact}\mbox{\isa{fact}} & : & \isarmeth \\
1192 \indexdef{}{method}{assumption}\mbox{\isa{assumption}} & : & \isarmeth \\
1193 \indexdef{}{method}{this}\mbox{\isa{this}} & : & \isarmeth \\
1194 \indexdef{}{method}{rule}\mbox{\isa{rule}} & : & \isarmeth \\
1195 \indexdef{}{method}{iprover}\mbox{\isa{iprover}} & : & \isarmeth \\[0.5ex]
1196 \indexdef{}{attribute}{intro}\mbox{\isa{intro}} & : & \isaratt \\
1197 \indexdef{}{attribute}{elim}\mbox{\isa{elim}} & : & \isaratt \\
1198 \indexdef{}{attribute}{dest}\mbox{\isa{dest}} & : & \isaratt \\
1199 \indexdef{}{attribute}{rule}\mbox{\isa{rule}} & : & \isaratt \\[0.5ex]
1200 \indexdef{}{attribute}{OF}\mbox{\isa{OF}} & : & \isaratt \\
1201 \indexdef{}{attribute}{of}\mbox{\isa{of}} & : & \isaratt \\
1202 \indexdef{}{attribute}{where}\mbox{\isa{where}} & : & \isaratt \\
1210 'iprover' ('!' ?) (rulemod *)
1212 rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
1214 ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
1220 'of' insts ('concl' ':' insts)?
1222 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
1228 \item [``\mbox{\isa{{\isacharminus}}}'' (minus)] does nothing but insert the
1229 forward chaining facts as premises into the goal. Note that command
1230 \indexref{}{command}{proof}\mbox{\isa{\isacommand{proof}}} without any method actually performs a single
1231 reduction step using the \indexref{}{method}{rule}\mbox{\isa{rule}} method; thus a plain
1232 \emph{do-nothing} proof step would be ``\mbox{\isa{\isacommand{proof}}}~\isa{{\isacharminus}}'' rather than \mbox{\isa{\isacommand{proof}}} alone.
1234 \item [\mbox{\isa{fact}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] composes
1235 some fact from \isa{a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n} (or implicitly from
1236 the current proof context) modulo unification of schematic type and
1237 term variables. The rule structure is not taken into account, i.e.\
1238 meta-level implication is considered atomic. This is the same
1239 principle underlying literal facts (cf.\ \secref{sec:syn-att}):
1240 ``\mbox{\isa{\isacommand{have}}}~\isa{{\isasymphi}}~\mbox{\isa{\isacommand{by}}}~\isa{fact}'' is
1241 equivalent to ``\mbox{\isa{\isacommand{note}}}~\verb|`|\isa{{\isasymphi}}\verb|`|'' provided that \isa{{\isasymturnstile}\ {\isasymphi}} is an instance of some known
1242 \isa{{\isasymturnstile}\ {\isasymphi}} in the proof context.
1244 \item [\mbox{\isa{assumption}}] solves some goal by a single assumption
1245 step. All given facts are guaranteed to participate in the
1246 refinement; this means there may be only 0 or 1 in the first place.
1247 Recall that \mbox{\isa{\isacommand{qed}}} (\secref{sec:proof-steps}) already
1248 concludes any remaining sub-goals by assumption, so structured
1249 proofs usually need not quote the \mbox{\isa{assumption}} method at
1252 \item [\mbox{\isa{this}}] applies all of the current facts directly as
1253 rules. Recall that ``\mbox{\isa{\isacommand{{\isachardot}}}}'' (dot) abbreviates ``\mbox{\isa{\isacommand{by}}}~\isa{this}''.
1255 \item [\mbox{\isa{rule}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] applies some
1256 rule given as argument in backward manner; facts are used to reduce
1257 the rule before applying it to the goal. Thus \mbox{\isa{rule}}
1258 without facts is plain introduction, while with facts it becomes
1261 When no arguments are given, the \mbox{\isa{rule}} method tries to pick
1262 appropriate rules automatically, as declared in the current context
1263 using the \mbox{\isa{intro}}, \mbox{\isa{elim}}, \mbox{\isa{dest}}
1264 attributes (see below). This is the default behavior of \mbox{\isa{\isacommand{proof}}} and ``\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}'' (double-dot) steps (see
1265 \secref{sec:proof-steps}).
1267 \item [\mbox{\isa{iprover}}] performs intuitionistic proof search,
1268 depending on specifically declared rules from the context, or given
1269 as explicit arguments. Chained facts are inserted into the goal
1270 before commencing proof search; ``\mbox{\isa{iprover}}\isa{{\isacharbang}}''
1271 means to include the current \mbox{\isa{prems}} as well.
1273 Rules need to be classified as \mbox{\isa{intro}}, \mbox{\isa{elim}}, or \mbox{\isa{dest}}; here the ``\isa{{\isacharbang}}'' indicator
1274 refers to ``safe'' rules, which may be applied aggressively (without
1275 considering back-tracking later). Rules declared with ``\isa{{\isacharquery}}'' are ignored in proof search (the single-step \mbox{\isa{rule}}
1276 method still observes these). An explicit weight annotation may be
1277 given as well; otherwise the number of rule premises will be taken
1280 \item [\mbox{\isa{intro}}, \mbox{\isa{elim}}, and \mbox{\isa{dest}}]
1281 declare introduction, elimination, and destruct rules, to be used
1282 with the \mbox{\isa{rule}} and \mbox{\isa{iprover}} methods. Note that
1283 the latter will ignore rules declared with ``\isa{{\isacharquery}}'', while
1284 ``\isa{{\isacharbang}}'' are used most aggressively.
1286 The classical reasoner (see \secref{sec:classical}) introduces its
1287 own variants of these attributes; use qualified names to access the
1288 present versions of Isabelle/Pure, i.e.\ \mbox{\isa{Pure{\isachardot}intro}}.
1290 \item [\mbox{\isa{rule}}~\isa{del}] undeclares introduction,
1291 elimination, or destruct rules.
1293 \item [\mbox{\isa{OF}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] applies some
1294 theorem to all of the given rules \isa{a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n}
1295 (in parallel). This corresponds to the \verb|op MRS| operation in
1296 ML, but note the reversed order. Positions may be effectively
1297 skipped by including ``\isa{{\isacharunderscore}}'' (underscore) as argument.
1299 \item [\mbox{\isa{of}}~\isa{t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n}] performs
1300 positional instantiation of term variables. The terms \isa{t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n} are substituted for any schematic
1301 variables occurring in a theorem from left to right; ``\isa{{\isacharunderscore}}'' (underscore) indicates to skip a position. Arguments following
1302 a ``\mbox{\isa{\isakeyword{concl}}}\isa{{\isacharcolon}}'' specification refer to positions
1303 of the conclusion of a rule.
1305 \item [\mbox{\isa{where}}~\isa{x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isacharequal}\ t\isactrlsub n}] performs named instantiation of schematic
1306 type and term variables occurring in a theorem. Schematic variables
1307 have to be specified on the left-hand side (e.g.\ \isa{{\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{3}}}).
1308 The question mark may be omitted if the variable name is a plain
1309 identifier without index. As type instantiations are inferred from
1310 term instantiations, explicit type instantiations are seldom
1314 \end{isamarkuptext}%
1317 \isamarkupsubsection{Term abbreviations \label{sec:term-abbrev}%
1321 \begin{isamarkuptext}%
1322 \begin{matharray}{rcl}
1323 \indexdef{}{command}{let}\mbox{\isa{\isacommand{let}}} & : & \isartrans{proof(state)}{proof(state)} \\
1324 \indexdef{}{keyword}{is}\mbox{\isa{\isakeyword{is}}} & : & syntax \\
1327 Abbreviations may be either bound by explicit \mbox{\isa{\isacommand{let}}}~\isa{p\ {\isasymequiv}\ t} statements, or by annotating assumptions or
1328 goal statements with a list of patterns ``\isa{{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}}''. In both cases, higher-order matching is invoked to
1329 bind extra-logical term variables, which may be either named
1330 schematic variables of the form \isa{{\isacharquery}x}, or nameless dummies
1331 ``\mbox{\isa{{\isacharunderscore}}}'' (underscore). Note that in the \mbox{\isa{\isacommand{let}}}
1332 form the patterns occur on the left-hand side, while the \mbox{\isa{\isakeyword{is}}} patterns are in postfix position.
1334 Polymorphism of term bindings is handled in Hindley-Milner style,
1335 similar to ML. Type variables referring to local assumptions or
1336 open goal statements are \emph{fixed}, while those of finished
1337 results or bound by \mbox{\isa{\isacommand{let}}} may occur in \emph{arbitrary}
1338 instances later. Even though actual polymorphism should be rarely
1339 used in practice, this mechanism is essential to achieve proper
1340 incremental type-inference, as the user proceeds to build up the
1341 Isar proof text from left to right.
1343 \medskip Term abbreviations are quite different from local
1344 definitions as introduced via \mbox{\isa{\isacommand{def}}} (see
1345 \secref{sec:proof-context}). The latter are visible within the
1346 logic as actual equations, while abbreviations disappear during the
1347 input process just after type checking. Also note that \mbox{\isa{\isacommand{def}}} does not support polymorphism.
1350 'let' ((term + 'and') '=' term + 'and')
1354 The syntax of \mbox{\isa{\isakeyword{is}}} patterns follows \railnonterm{termpat}
1355 or \railnonterm{proppat} (see \secref{sec:term-decls}).
1359 \item [\mbox{\isa{\isacommand{let}}}~\isa{p\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ p\isactrlsub n\ {\isacharequal}\ t\isactrlsub n}] binds any text variables in patterns \isa{p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n} by simultaneous higher-order matching
1360 against terms \isa{t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n}.
1362 \item [\isa{{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}}] resembles \mbox{\isa{\isacommand{let}}}, but matches \isa{p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n} against the
1363 preceding statement. Also note that \mbox{\isa{\isakeyword{is}}} is not a
1364 separate command, but part of others (such as \mbox{\isa{\isacommand{assume}}},
1365 \mbox{\isa{\isacommand{have}}} etc.).
1369 Some \emph{implicit} term abbreviations\index{term abbreviations}
1370 for goals and facts are available as well. For any open goal,
1371 \indexref{}{variable}{thesis}\mbox{\isa{thesis}} refers to its object-level statement,
1372 abstracted over any meta-level parameters (if present). Likewise,
1373 \indexref{}{variable}{this}\mbox{\isa{this}} is bound for fact statements resulting from
1374 assumptions or finished goals. In case \mbox{\isa{this}} refers to
1375 an object-logic statement that is an application \isa{f\ t}, then
1376 \isa{t} is bound to the special text variable ``\mbox{\isa{{\isasymdots}}}''
1377 (three dots). The canonical application of this convenience are
1378 calculational proofs (see \secref{sec:calculation}).%
1379 \end{isamarkuptext}%
1382 \isamarkupsubsection{Block structure%
1386 \begin{isamarkuptext}%
1387 \begin{matharray}{rcl}
1388 \indexdef{}{command}{next}\mbox{\isa{\isacommand{next}}} & : & \isartrans{proof(state)}{proof(state)} \\
1389 \indexdef{}{command}{\{}\mbox{\isa{\isacommand{{\isacharbraceleft}}}} & : & \isartrans{proof(state)}{proof(state)} \\
1390 \indexdef{}{command}{\}}\mbox{\isa{\isacommand{{\isacharbraceright}}}} & : & \isartrans{proof(state)}{proof(state)} \\
1393 While Isar is inherently block-structured, opening and closing
1394 blocks is mostly handled rather casually, with little explicit
1395 user-intervention. Any local goal statement automatically opens
1396 \emph{two} internal blocks, which are closed again when concluding
1397 the sub-proof (by \mbox{\isa{\isacommand{qed}}} etc.). Sections of different
1398 context within a sub-proof may be switched via \mbox{\isa{\isacommand{next}}},
1399 which is just a single block-close followed by block-open again.
1400 The effect of \mbox{\isa{\isacommand{next}}} is to reset the local proof context;
1401 there is no goal focus involved here!
1403 For slightly more advanced applications, there are explicit block
1404 parentheses as well. These typically achieve a stronger forward
1409 \item [\mbox{\isa{\isacommand{next}}}] switches to a fresh block within a
1410 sub-proof, resetting the local context to the initial one.
1412 \item [\mbox{\isa{\isacommand{{\isacharbraceleft}}}} and \mbox{\isa{\isacommand{{\isacharbraceright}}}}] explicitly open and close
1413 blocks. Any current facts pass through ``\mbox{\isa{\isacommand{{\isacharbraceleft}}}}''
1414 unchanged, while ``\mbox{\isa{\isacommand{{\isacharbraceright}}}}'' causes any result to be
1415 \emph{exported} into the enclosing context. Thus fixed variables
1416 are generalized, assumptions discharged, and local definitions
1417 unfolded (cf.\ \secref{sec:proof-context}). There is no difference
1418 of \mbox{\isa{\isacommand{assume}}} and \mbox{\isa{\isacommand{presume}}} in this mode of
1419 forward reasoning --- in contrast to plain backward reasoning with
1420 the result exported at \mbox{\isa{\isacommand{show}}} time.
1423 \end{isamarkuptext}%
1426 \isamarkupsubsection{Emulating tactic scripts \label{sec:tactic-commands}%
1430 \begin{isamarkuptext}%
1431 The Isar provides separate commands to accommodate tactic-style
1432 proof scripts within the same system. While being outside the
1433 orthodox Isar proof language, these might come in handy for
1434 interactive exploration and debugging, or even actual tactical proof
1435 within new-style theories (to benefit from document preparation, for
1436 example). See also \secref{sec:tactics} for actual tactics, that
1437 have been encapsulated as proof methods. Proper proof methods may
1438 be used in scripts, too.
1440 \begin{matharray}{rcl}
1441 \indexdef{}{command}{apply}\mbox{\isa{\isacommand{apply}}}^* & : & \isartrans{proof(prove)}{proof(prove)} \\
1442 \indexdef{}{command}{apply-end}\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}^* & : & \isartrans{proof(state)}{proof(state)} \\
1443 \indexdef{}{command}{done}\mbox{\isa{\isacommand{done}}}^* & : & \isartrans{proof(prove)}{proof(state)} \\
1444 \indexdef{}{command}{defer}\mbox{\isa{\isacommand{defer}}}^* & : & \isartrans{proof}{proof} \\
1445 \indexdef{}{command}{prefer}\mbox{\isa{\isacommand{prefer}}}^* & : & \isartrans{proof}{proof} \\
1446 \indexdef{}{command}{back}\mbox{\isa{\isacommand{back}}}^* & : & \isartrans{proof}{proof} \\
1450 ( 'apply' | 'apply\_end' ) method
1460 \item [\mbox{\isa{\isacommand{apply}}}~\isa{m}] applies proof method \isa{m}
1461 in initial position, but unlike \mbox{\isa{\isacommand{proof}}} it retains
1462 ``\isa{proof{\isacharparenleft}prove{\isacharparenright}}'' mode. Thus consecutive method
1463 applications may be given just as in tactic scripts.
1465 Facts are passed to \isa{m} as indicated by the goal's
1466 forward-chain mode, and are \emph{consumed} afterwards. Thus any
1467 further \mbox{\isa{\isacommand{apply}}} command would always work in a purely
1470 \item [\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}~\isa{m}] applies proof method
1471 \isa{m} as if in terminal position. Basically, this simulates a
1472 multi-step tactic script for \mbox{\isa{\isacommand{qed}}}, but may be given
1473 anywhere within the proof body.
1475 No facts are passed to \mbox{\isa{m}} here. Furthermore, the static
1476 context is that of the enclosing goal (as for actual \mbox{\isa{\isacommand{qed}}}). Thus the proof method may not refer to any assumptions
1477 introduced in the current body, for example.
1479 \item [\mbox{\isa{\isacommand{done}}}] completes a proof script, provided that
1480 the current goal state is solved completely. Note that actual
1481 structured proof commands (e.g.\ ``\mbox{\isa{\isacommand{{\isachardot}}}}'' or \mbox{\isa{\isacommand{sorry}}}) may be used to conclude proof scripts as well.
1483 \item [\mbox{\isa{\isacommand{defer}}}~\isa{n} and \mbox{\isa{\isacommand{prefer}}}~\isa{n}] shuffle the list of pending goals: \mbox{\isa{\isacommand{defer}}} puts off
1484 sub-goal \isa{n} to the end of the list (\isa{n\ {\isacharequal}\ {\isadigit{1}}} by
1485 default), while \mbox{\isa{\isacommand{prefer}}} brings sub-goal \isa{n} to the
1488 \item [\mbox{\isa{\isacommand{back}}}] does back-tracking over the result
1489 sequence of the latest proof command. Basically, any proof command
1490 may return multiple results.
1494 Any proper Isar proof method may be used with tactic script commands
1495 such as \mbox{\isa{\isacommand{apply}}}. A few additional emulations of actual
1496 tactics are provided as well; these would be never used in actual
1497 structured proofs, of course.%
1498 \end{isamarkuptext}%
1501 \isamarkupsubsection{Meta-linguistic features%
1505 \begin{isamarkuptext}%
1506 \begin{matharray}{rcl}
1507 \indexdef{}{command}{oops}\mbox{\isa{\isacommand{oops}}} & : & \isartrans{proof}{theory} \\
1510 The \mbox{\isa{\isacommand{oops}}} command discontinues the current proof
1511 attempt, while considering the partial proof text as properly
1512 processed. This is conceptually quite different from ``faking''
1513 actual proofs via \indexref{}{command}{sorry}\mbox{\isa{\isacommand{sorry}}} (see
1514 \secref{sec:proof-steps}): \mbox{\isa{\isacommand{oops}}} does not observe the
1515 proof structure at all, but goes back right to the theory level.
1516 Furthermore, \mbox{\isa{\isacommand{oops}}} does not produce any result theorem
1517 --- there is no intended claim to be able to complete the proof
1520 A typical application of \mbox{\isa{\isacommand{oops}}} is to explain Isar proofs
1521 \emph{within} the system itself, in conjunction with the document
1522 preparation tools of Isabelle described in \cite{isabelle-sys}.
1523 Thus partial or even wrong proof attempts can be discussed in a
1524 logically sound manner. Note that the Isabelle {\LaTeX} macros can
1525 be easily adapted to print something like ``\isa{{\isasymdots}}'' instead of
1526 the keyword ``\mbox{\isa{\isacommand{oops}}}''.
1528 \medskip The \mbox{\isa{\isacommand{oops}}} command is undo-able, unlike
1529 \indexref{}{command}{kill}\mbox{\isa{\isacommand{kill}}} (see \secref{sec:history}). The effect is to
1530 get back to the theory just before the opening of the proof.%
1531 \end{isamarkuptext}%
1534 \isamarkupsection{Other commands%
1538 \isamarkupsubsection{Diagnostics%
1542 \begin{isamarkuptext}%
1543 \begin{matharray}{rcl}
1544 \isarcmd{pr}^* & : & \isarkeep{\cdot} \\
1545 \isarcmd{thm}^* & : & \isarkeep{theory~|~proof} \\
1546 \isarcmd{term}^* & : & \isarkeep{theory~|~proof} \\
1547 \isarcmd{prop}^* & : & \isarkeep{theory~|~proof} \\
1548 \isarcmd{typ}^* & : & \isarkeep{theory~|~proof} \\
1549 \isarcmd{prf}^* & : & \isarkeep{theory~|~proof} \\
1550 \isarcmd{full_prf}^* & : & \isarkeep{theory~|~proof} \\
1553 These diagnostic commands assist interactive development. Note that
1554 \mbox{\isa{\isacommand{undo}}} does not apply here, the theory or proof
1555 configuration is not changed.
1558 'pr' modes? nat? (',' nat)?
1560 'thm' modes? thmrefs
1568 'prf' modes? thmrefs?
1570 'full\_prf' modes? thmrefs?
1573 modes: '(' (name + ) ')'
1579 \item [\mbox{\isa{\isacommand{pr}}}~\isa{goals{\isacharcomma}\ prems}] prints the current
1580 proof state (if present), including the proof context, current facts
1581 and goals. The optional limit arguments affect the number of goals
1582 and premises to be displayed, which is initially 10 for both.
1583 Omitting limit values leaves the current setting unchanged.
1585 \item [\mbox{\isa{\isacommand{thm}}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] retrieves
1586 theorems from the current theory or proof context. Note that any
1587 attributes included in the theorem specifications are applied to a
1588 temporary context derived from the current theory or proof; the
1589 result is discarded, i.e.\ attributes involved in \isa{a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n} do not have any permanent effect.
1591 \item [\mbox{\isa{\isacommand{term}}}~\isa{t} and \mbox{\isa{\isacommand{prop}}}~\isa{{\isasymphi}}]
1592 read, type-check and print terms or propositions according to the
1593 current theory or proof context; the inferred type of \isa{t} is
1594 output as well. Note that these commands are also useful in
1595 inspecting the current environment of term abbreviations.
1597 \item [\mbox{\isa{\isacommand{typ}}}~\isa{{\isasymtau}}] reads and prints types of the
1598 meta-logic according to the current theory or proof context.
1600 \item [\mbox{\isa{\isacommand{prf}}}] displays the (compact) proof term of the
1601 current proof state (if present), or of the given theorems. Note
1602 that this requires proof terms to be switched on for the current
1603 object logic (see the ``Proof terms'' section of the Isabelle
1604 reference manual for information on how to do this).
1606 \item [\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}] is like \mbox{\isa{\isacommand{prf}}}, but displays
1607 the full proof term, i.e.\ also displays information omitted in the
1608 compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders
1613 All of the diagnostic commands above admit a list of \isa{modes}
1614 to be specified, which is appended to the current print mode (see
1615 also \cite{isabelle-ref}). Thus the output behavior may be modified
1616 according particular print mode features. For example, \mbox{\isa{\isacommand{pr}}}~\isa{{\isacharparenleft}latex\ xsymbols\ symbols{\isacharparenright}} would print the current
1617 proof state with mathematical symbols and special characters
1618 represented in {\LaTeX} source, according to the Isabelle style
1619 \cite{isabelle-sys}.
1621 Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
1622 systematic way to include formal items into the printed text
1624 \end{isamarkuptext}%
1627 \isamarkupsubsection{Inspecting the context%
1631 \begin{isamarkuptext}%
1632 \begin{matharray}{rcl}
1633 \indexdef{}{command}{print-commands}\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}^* & : & \isarkeep{\cdot} \\
1634 \indexdef{}{command}{print-theory}\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}^* & : & \isarkeep{theory~|~proof} \\
1635 \indexdef{}{command}{print-syntax}\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}^* & : & \isarkeep{theory~|~proof} \\
1636 \indexdef{}{command}{print-methods}\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}^* & : & \isarkeep{theory~|~proof} \\
1637 \indexdef{}{command}{print-attributes}\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}^* & : & \isarkeep{theory~|~proof} \\
1638 \indexdef{}{command}{print-theorems}\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}^* & : & \isarkeep{theory~|~proof} \\
1639 \indexdef{}{command}{find-theorems}\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}^* & : & \isarkeep{theory~|~proof} \\
1640 \indexdef{}{command}{thms-deps}\mbox{\isa{\isacommand{thms{\isacharunderscore}deps}}}^* & : & \isarkeep{theory~|~proof} \\
1641 \indexdef{}{command}{print-facts}\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}^* & : & \isarkeep{proof} \\
1642 \indexdef{}{command}{print-binds}\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}^* & : & \isarkeep{proof} \\
1646 'print\_theory' ( '!'?)
1649 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
1651 criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
1652 'simp' ':' term | term)
1658 These commands print certain parts of the theory and proof context.
1659 Note that there are some further ones available, such as for the set
1660 of rules declared for simplifications.
1664 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}] prints Isabelle's outer theory
1665 syntax, including keywords and command.
1667 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}] prints the main logical content of
1668 the theory context; the ``\isa{{\isacharbang}}'' option indicates extra
1671 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}] prints the inner syntax of types
1672 and terms, depending on the current context. The output can be very
1673 verbose, including grammar tables and syntax translation rules. See
1674 \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's
1677 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}] prints all proof methods
1678 available in the current theory context.
1680 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}] prints all attributes
1681 available in the current theory context.
1683 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}] prints theorems resulting from
1686 \item [\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}~\isa{criteria}] retrieves facts
1687 from the theory or proof context matching all of given search
1688 criteria. The criterion \isa{name{\isacharcolon}\ p} selects all theorems
1689 whose fully qualified name matches pattern \isa{p}, which may
1690 contain ``\isa{{\isacharasterisk}}'' wildcards. The criteria \isa{intro},
1691 \isa{elim}, and \isa{dest} select theorems that match the
1692 current goal as introduction, elimination or destruction rules,
1693 respectively. The criterion \isa{simp{\isacharcolon}\ t} selects all rewrite
1694 rules whose left-hand side matches the given term. The criterion
1695 term \isa{t} selects all theorems that contain the pattern \isa{t} -- as usual, patterns may contain occurrences of the dummy
1696 ``\isa{{\isacharunderscore}}'', schematic variables, and type constraints.
1698 Criteria can be preceded by ``\isa{{\isacharminus}}'' to select theorems that
1699 do \emph{not} match. Note that giving the empty list of criteria
1700 yields \emph{all} currently known facts. An optional limit for the
1701 number of printed facts may be given; the default is 40. By
1702 default, duplicates are removed from the search result. Use
1703 \mbox{\isa{\isakeyword{with{\isacharunderscore}dups}}} to display duplicates.
1705 \item [\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}]
1706 visualizes dependencies of facts, using Isabelle's graph browser
1707 tool (see also \cite{isabelle-sys}).
1709 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}] prints all local facts of the
1710 current context, both named and unnamed ones.
1712 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}] prints all term abbreviations
1713 present in the context.
1716 \end{isamarkuptext}%
1719 \isamarkupsubsection{History commands \label{sec:history}%
1723 \begin{isamarkuptext}%
1724 \begin{matharray}{rcl}
1725 \indexdef{}{command}{undo}\mbox{\isa{\isacommand{undo}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
1726 \indexdef{}{command}{redo}\mbox{\isa{\isacommand{redo}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
1727 \indexdef{}{command}{kill}\mbox{\isa{\isacommand{kill}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
1730 The Isabelle/Isar top-level maintains a two-stage history, for
1731 theory and proof state transformation. Basically, any command can
1732 be undone using \mbox{\isa{\isacommand{undo}}}, excluding mere diagnostic
1733 elements. Its effect may be revoked via \mbox{\isa{\isacommand{redo}}}, unless
1734 the corresponding \mbox{\isa{\isacommand{undo}}} step has crossed the beginning
1735 of a proof or theory. The \mbox{\isa{\isacommand{kill}}} command aborts the
1736 current history node altogether, discontinuing a proof or even the
1737 whole theory. This operation is \emph{not} undo-able.
1740 History commands should never be used with user interfaces such as
1741 Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
1742 care of stepping forth and back itself. Interfering by manual
1743 \mbox{\isa{\isacommand{undo}}}, \mbox{\isa{\isacommand{redo}}}, or even \mbox{\isa{\isacommand{kill}}}
1744 commands would quickly result in utter confusion.
1746 \end{isamarkuptext}%
1749 \isamarkupsubsection{System operations%
1753 \begin{isamarkuptext}%
1754 \begin{matharray}{rcl}
1755 \indexdef{}{command}{cd}\mbox{\isa{\isacommand{cd}}}^* & : & \isarkeep{\cdot} \\
1756 \indexdef{}{command}{pwd}\mbox{\isa{\isacommand{pwd}}}^* & : & \isarkeep{\cdot} \\
1757 \indexdef{}{command}{use-thy}\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}^* & : & \isarkeep{\cdot} \\
1758 \indexdef{}{command}{display-drafts}\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}^* & : & \isarkeep{\cdot} \\
1759 \indexdef{}{command}{print-drafts}\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}^* & : & \isarkeep{\cdot} \\
1763 ('cd' | 'use\_thy' | 'update\_thy') name
1765 ('display\_drafts' | 'print\_drafts') (name +)
1771 \item [\mbox{\isa{\isacommand{cd}}}~\isa{path}] changes the current directory
1772 of the Isabelle process.
1774 \item [\mbox{\isa{\isacommand{pwd}}}] prints the current working directory.
1776 \item [\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}~\isa{A}] preload theory \isa{A}.
1777 These system commands are scarcely used when working interactively,
1778 since loading of theories is done automatically as required.
1780 \item [\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}~\isa{paths} and \mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}~\isa{paths}] perform simple output of a given list
1781 of raw source files. Only those symbols that do not require
1782 additional {\LaTeX} packages are displayed properly, everything else
1786 \end{isamarkuptext}%
1794 \isacommand{end}\isamarkupfalse%
1804 %%% Local Variables:
1806 %%% TeX-master: "root"