3 \def\isabellecontext{syntax}%
12 \isacommand{theory}\isamarkupfalse%
13 \ {\isachardoublequoteopen}syntax{\isachardoublequoteclose}\isanewline
14 \isakeyword{imports}\ CPure\isanewline
23 \isamarkupchapter{Syntax primitives%
27 \begin{isamarkuptext}%
28 The rather generic framework of Isabelle/Isar syntax emerges from
29 three main syntactic categories: \emph{commands} of the top-level
30 Isar engine (covering theory and proof elements), \emph{methods} for
31 general goal refinements (analogous to traditional ``tactics''), and
32 \emph{attributes} for operations on facts (within a certain
33 context). Subsequently we give a reference of basic syntactic
34 entities underlying Isabelle/Isar syntax in a bottom-up manner.
35 Concrete theory and proof language elements will be introduced later
38 \medskip In order to get started with writing well-formed
39 Isabelle/Isar documents, the most important aspect to be noted is
40 the difference of \emph{inner} versus \emph{outer} syntax. Inner
41 syntax is that of Isabelle types and terms of the logic, while outer
42 syntax is that of Isabelle/Isar theory sources (specifications and
43 proofs). As a general rule, inner syntax entities may occur only as
44 \emph{atomic entities} within outer syntax. For example, the string
45 \verb|"x + y"| and identifier \verb|z| are legal term
46 specifications within a theory, while \verb|x + y| without
49 Printed theory documents usually omit quotes to gain readability
50 (this is a matter of {\LaTeX} macro setup, say via \verb|\isabellestyle|, see also \cite{isabelle-sys}). Experienced
51 users of Isabelle/Isar may easily reconstruct the lost technical
52 information, while mere readers need not care about quotes at all.
54 \medskip Isabelle/Isar input may contain any number of input
55 termination characters ``\verb|;|'' (semicolon) to separate
56 commands explicitly. This is particularly useful in interactive
57 shell sessions to make clear where the current command is intended
58 to end. Otherwise, the interpreter loop will continue to issue a
59 secondary prompt ``\verb|#|'' until an end-of-command is
60 clearly recognized from the input syntax, e.g.\ encounter of the
63 More advanced interfaces such as Proof~General \cite{proofgeneral}
64 do not require explicit semicolons, the amount of input text is
65 determined automatically by inspecting the present content of the
66 Emacs text buffer. In the printed presentation of Isabelle/Isar
67 documents semicolons are omitted altogether for readability.
70 Proof~General requires certain syntax classification tables in
71 order to achieve properly synchronized interaction with the
72 Isabelle/Isar process. These tables need to be consistent with
73 the Isabelle version and particular logic image to be used in a
74 running session (common object-logics may well change the outer
75 syntax). The standard setup should work correctly with any of the
76 ``official'' logic images derived from Isabelle/HOL (including
77 HOLCF etc.). Users of alternative logics may need to tell
78 Proof~General explicitly, e.g.\ by giving an option \verb|-k ZF|
79 (in conjunction with \verb|-l ZF|, to specify the default
80 logic image). Note that option \verb|-L| does both
81 of this at the same time.
86 \isamarkupsection{Lexical matters \label{sec:lex-syntax}%
90 \begin{isamarkuptext}%
91 The Isabelle/Isar outer syntax provides token classes as presented
92 below; most of these coincide with the inner lexical syntax as
93 presented in \cite{isabelle-ref}.
95 \begin{matharray}{rcl}
96 \indexdef{}{syntax}{ident}\hypertarget{syntax.ident}{\hyperlink{syntax.ident}{\mbox{\isa{ident}}}} & = & letter\,quasiletter^* \\
97 \indexdef{}{syntax}{longident}\hypertarget{syntax.longident}{\hyperlink{syntax.longident}{\mbox{\isa{longident}}}} & = & ident (\verb,.,ident)^+ \\
98 \indexdef{}{syntax}{symident}\hypertarget{syntax.symident}{\hyperlink{syntax.symident}{\mbox{\isa{symident}}}} & = & sym^+ ~|~ \verb,\,\verb,<,ident\verb,>, \\
99 \indexdef{}{syntax}{nat}\hypertarget{syntax.nat}{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}} & = & digit^+ \\
100 \indexdef{}{syntax}{var}\hypertarget{syntax.var}{\hyperlink{syntax.var}{\mbox{\isa{var}}}} & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
101 \indexdef{}{syntax}{typefree}\hypertarget{syntax.typefree}{\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}}} & = & \verb,',ident \\
102 \indexdef{}{syntax}{typevar}\hypertarget{syntax.typevar}{\hyperlink{syntax.typevar}{\mbox{\isa{typevar}}}} & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
103 \indexdef{}{syntax}{string}\hypertarget{syntax.string}{\hyperlink{syntax.string}{\mbox{\isa{string}}}} & = & \verb,", ~\dots~ \verb,", \\
104 \indexdef{}{syntax}{altstring}\hypertarget{syntax.altstring}{\hyperlink{syntax.altstring}{\mbox{\isa{altstring}}}} & = & \backquote ~\dots~ \backquote \\
105 \indexdef{}{syntax}{verbatim}\hypertarget{syntax.verbatim}{\hyperlink{syntax.verbatim}{\mbox{\isa{verbatim}}}} & = & \verb,{*, ~\dots~ \verb,*,\verb,}, \\[1ex]
107 letter & = & latin ~|~ \verb,\,\verb,<,latin\verb,>, ~|~ \verb,\,\verb,<,latin\,latin\verb,>, ~|~ greek ~|~ \\
108 & & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
109 quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
110 latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
111 digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
112 sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~
113 \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \\
114 & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
115 \verb,^, ~|~ \verb,_, ~|~ \verb,|, ~|~ \verb,~, \\
116 greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
117 & & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
118 & & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
119 & & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~|~ \verb,\<tau>, ~| \\
120 & & \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<chi>, ~|~ \verb,\<psi>, ~| \\
121 & & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\
122 & & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\
123 & & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
126 The syntax of \hyperlink{syntax.string}{\mbox{\isa{string}}} admits any characters, including
127 newlines; ``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) need to be escaped by a backslash; arbitrary
128 character codes may be specified as ``\verb|\|\isa{ddd}'',
129 with three decimal digits. Alternative strings according to
130 \hyperlink{syntax.altstring}{\mbox{\isa{altstring}}} are analogous, using single back-quotes instead.
131 The body of \hyperlink{syntax.verbatim}{\mbox{\isa{verbatim}}} may consist of any text not
132 containing ``\verb|*|\verb|}|''; this allows
133 convenient inclusion of quotes without further escapes. The greek
134 letters do \emph{not} include \verb|\<lambda>|, which is already used
135 differently in the meta-logic.
137 Common mathematical symbols such as \isa{{\isasymforall}} are represented in
138 Isabelle as \verb|\<forall>|. There are infinitely many Isabelle
139 symbols like this, although proper presentation is left to front-end
140 tools such as {\LaTeX} or Proof~General with the X-Symbol package.
141 A list of standard Isabelle symbols that work well with these tools
142 is given in \cite[appendix~A]{isabelle-sys}.
144 Source comments take the form \verb|(*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*)| and may be nested, although user-interface
145 tools might prevent this. Note that this form indicates source
146 comments only, which are stripped after lexical analysis of the
147 input. The Isar document syntax also provides formal comments that
148 are considered as part of the text (see \secref{sec:comments}).%
152 \isamarkupsection{Common syntax entities%
156 \begin{isamarkuptext}%
157 We now introduce several basic syntactic entities, such as names,
158 terms, and theorem specifications, which are factored out of the
159 actual Isar language elements to be described later.%
163 \isamarkupsubsection{Names%
167 \begin{isamarkuptext}%
168 Entity \railqtok{name} usually refers to any name of types,
169 constants, theorems etc.\ that are to be \emph{declared} or
170 \emph{defined} (so qualified identifiers are excluded here). Quoted
171 strings provide an escape for non-identifier names or those ruled
172 out by outer syntax keywords (e.g.\ quoted \verb|"let"|).
173 Already existing objects are usually referenced by
176 \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
177 \indexoutertoken{int}
179 name: ident | symident | string | nat
181 parname: '(' name ')'
183 nameref: name | longident
191 \isamarkupsubsection{Comments \label{sec:comments}%
195 \begin{isamarkuptext}%
196 Large chunks of plain \railqtok{text} are usually given
197 \railtok{verbatim}, i.e.\ enclosed in \verb|{|\verb|*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*|\verb|}|. For convenience,
198 any of the smaller text units conforming to \railqtok{nameref} are
199 admitted as well. A marginal \railnonterm{comment} is of the form
200 \verb|--| \railqtok{text}. Any number of these may occur
201 within Isabelle/Isar commands.
203 \indexoutertoken{text}\indexouternonterm{comment}
205 text: verbatim | nameref
213 \isamarkupsubsection{Type classes, sorts and arities%
217 \begin{isamarkuptext}%
218 Classes are specified by plain names. Sorts have a very simple
219 inner syntax, which is either a single class name \isa{c} or a
220 list \isa{{\isachardoublequote}{\isacharbraceleft}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isacharbraceright}{\isachardoublequote}} referring to the
221 intersection of these classes. The syntax of type arities is given
222 directly at the outer level.
224 \indexouternonterm{sort}\indexouternonterm{arity}
225 \indexouternonterm{classdecl}
227 classdecl: name (('<' | subseteq) (nameref + ','))?
231 arity: ('(' (sort + ',') ')')? sort
237 \isamarkupsubsection{Types and terms \label{sec:types-terms}%
241 \begin{isamarkuptext}%
242 The actual inner Isabelle syntax, that of types and terms of the
243 logic, is far too sophisticated in order to be modelled explicitly
244 at the outer theory level. Basically, any such entity has to be
245 quoted to turn it into a single token (the parsing and type-checking
246 is performed internally later). For convenience, a slightly more
247 liberal convention is adopted: quotes may be omitted for any type or
248 term that is already atomic at the outer level. For example, one
249 may just write \verb|x| instead of quoted \verb|"x"|.
250 Note that symbolic identifiers (e.g.\ \verb|++| or \isa{{\isachardoublequote}{\isasymforall}{\isachardoublequote}} are available as well, provided these have not been superseded
251 by commands or other keywords already (such as \verb|=| or
254 \indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
256 type: nameref | typefree | typevar
264 Positional instantiations are indicated by giving a sequence of
265 terms, or the placeholder ``\isa{{\isacharunderscore}}'' (underscore), which means to
268 \indexoutertoken{inst}\indexoutertoken{insts}
270 inst: underscore | term
276 Type declarations and definitions usually refer to
277 \railnonterm{typespec} on the left-hand side. This models basic
278 type constructor application at the outer syntax level. Note that
279 only plain postfix notation is available here, but no infixes.
281 \indexouternonterm{typespec}
283 typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
289 \isamarkupsubsection{Mixfix annotations%
293 \begin{isamarkuptext}%
294 Mixfix annotations specify concrete \emph{inner} syntax of Isabelle
295 types and terms. Some commands such as \hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}} (see
296 \secref{sec:types-pure}) admit infixes only, while \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}} (see \secref{sec:consts}) and \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} (see
297 \secref{sec:syn-trans}) support the full range of general mixfixes
300 \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
302 infix: '(' ('infix' | 'infixl' | 'infixr') string? nat ')'
304 mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
306 structmixfix: mixfix | '(' 'structure' ')'
309 prios: '[' (nat + ',') ']'
313 Here the \railtok{string} specifications refer to the actual mixfix
314 template (see also \cite{isabelle-ref}), which may include literal
315 text, spacing, blocks, and arguments (denoted by ``\isa{{\isacharunderscore}}''); the
316 special symbol ``\verb|\<index>|'' (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}'')
317 represents an index argument that specifies an implicit structure
318 reference (see also \secref{sec:locale}). Infix and binder
319 declarations provide common abbreviations for particular mixfix
320 declarations. So in practice, mixfix templates mostly degenerate to
321 literal text for concrete syntax, such as ``\verb|++|'' for
322 an infix symbol, or ``\verb|++|\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}'' for an infix of
323 an implicit structure.%
327 \isamarkupsubsection{Proof methods \label{sec:syn-meth}%
331 \begin{isamarkuptext}%
332 Proof methods are either basic ones, or expressions composed of
333 methods via ``\verb|,|'' (sequential composition),
334 ``\verb||\verb,|,\verb||'' (alternative choices), ``\verb|?|''
335 (try), ``\verb|+|'' (repeat at least once), ``\verb|[|\isa{n}\verb|]|'' (restriction to first \isa{n}
336 sub-goals, with default \isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}}). In practice, proof
337 methods are usually just a comma separated list of
338 \railqtok{nameref}~\railnonterm{args} specifications. Note that
339 parentheses may be dropped for single method specifications (with no
342 \indexouternonterm{method}
344 method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
346 methods: (nameref args | method) + (',' | '|')
350 Proper Isar proof methods do \emph{not} admit arbitrary goal
351 addressing, but refer either to the first sub-goal or all sub-goals
352 uniformly. The goal restriction operator ``\isa{{\isachardoublequote}{\isacharbrackleft}n{\isacharbrackright}{\isachardoublequote}}''
353 evaluates a method expression within a sandbox consisting of the
354 first \isa{n} sub-goals (which need to exist). For example, the
355 method ``\isa{{\isachardoublequote}simp{\isacharunderscore}all{\isacharbrackleft}{\isadigit{3}}{\isacharbrackright}{\isachardoublequote}}'' simplifies the first three
356 sub-goals, while ``\isa{{\isachardoublequote}{\isacharparenleft}rule\ foo{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}}'' simplifies all
357 new goals that emerge from applying rule \isa{{\isachardoublequote}foo{\isachardoublequote}} to the
358 originally first one.
360 Improper methods, notably tactic emulations, offer a separate
361 low-level goal addressing scheme as explicit argument to the
362 individual tactic being involved. Here ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbang}{\isacharbrackright}{\isachardoublequote}}'' refers to
363 all goals, and ``\isa{{\isachardoublequote}{\isacharbrackleft}n{\isacharminus}{\isacharbrackright}{\isachardoublequote}}'' to all goals starting from \isa{{\isachardoublequote}n{\isachardoublequote}}.
365 \indexouternonterm{goalspec}
367 goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
373 \isamarkupsubsection{Attributes and theorems \label{sec:syn-att}%
377 \begin{isamarkuptext}%
378 Attributes (and proof methods, see \secref{sec:syn-meth}) have their
379 own ``semi-inner'' syntax, in the sense that input conforming to
380 \railnonterm{args} below is parsed by the attribute a second time.
381 The attribute argument specifications may be any sequence of atomic
382 entities (identifiers, strings etc.), or properly bracketed argument
383 lists. Below \railqtok{atom} refers to any atomic entity, including
384 any \railtok{keyword} conforming to \railtok{symident}.
386 \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
388 atom: nameref | typefree | typevar | var | nat | keyword
390 arg: atom | '(' args ')' | '[' args ']'
394 attributes: '[' (nameref args * ',') ']'
398 Theorem specifications come in several flavors:
399 \railnonterm{axmdecl} and \railnonterm{thmdecl} usually refer to
400 axioms, assumptions or results of goal statements, while
401 \railnonterm{thmdef} collects lists of existing theorems. Existing
402 theorems are given by \railnonterm{thmref} and
403 \railnonterm{thmrefs}, the former requires an actual singleton
406 There are three forms of theorem references:
409 \item named facts \isa{{\isachardoublequote}a{\isachardoublequote}},
411 \item selections from named facts \isa{{\isachardoublequote}a{\isacharparenleft}i{\isacharparenright}{\isachardoublequote}} or \isa{{\isachardoublequote}a{\isacharparenleft}j\ {\isacharminus}\ k{\isacharparenright}{\isachardoublequote}},
413 \item literal fact propositions using \indexref{}{syntax}{altstring}\hyperlink{syntax.altstring}{\mbox{\isa{altstring}}} syntax
414 \verb|`|\isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}\verb|`| (see also method
415 \indexref{}{method}{fact}\hyperlink{method.fact}{\mbox{\isa{fact}}} in \secref{sec:pure-meth-att}).
419 Any kind of theorem specification may include lists of attributes
420 both on the left and right hand sides; attributes are applied to any
421 immediately preceding fact. If names are omitted, the theorems are
422 not stored within the theorem database of the theory or proof
423 context, but any given attributes are applied nonetheless.
425 An extra pair of brackets around attributes (like ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbrackleft}simproc\ a{\isacharbrackright}{\isacharbrackright}{\isachardoublequote}}'') abbreviates a theorem reference involving an
426 internal dummy fact, which will be ignored later on. So only the
427 effect of the attribute on the background context will persist.
428 This form of in-place declarations is particularly useful with
429 commands like \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} and \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}.
431 \indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
432 \indexouternonterm{thmdef}\indexouternonterm{thmref}
433 \indexouternonterm{thmrefs}\indexouternonterm{selection}
435 axmdecl: name attributes? ':'
441 thmref: (nameref selection? | altstring) attributes? | '[' attributes ']'
446 thmbind: name attributes | name | attributes
448 selection: '(' ((nat | nat '-' nat?) + ',') ')'
454 \isamarkupsubsection{Term patterns and declarations \label{sec:term-decls}%
458 \begin{isamarkuptext}%
459 Wherever explicit propositions (or term fragments) occur in a proof
460 text, casual binding of schematic term variables may be given
461 specified via patterns of the form ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}''. This works both for \railqtok{term} and \railqtok{prop}.
463 \indexouternonterm{termpat}\indexouternonterm{proppat}
465 termpat: '(' ('is' term +) ')'
467 proppat: '(' ('is' prop +) ')'
471 \medskip Declarations of local variables \isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}} and
472 logical propositions \isa{{\isachardoublequote}a\ {\isacharcolon}\ {\isasymphi}{\isachardoublequote}} represent different views on
473 the same principle of introducing a local scope. In practice, one
474 may usually omit the typing of \railnonterm{vars} (due to
475 type-inference), and the naming of propositions (due to implicit
476 references of current facts). In any case, Isar proof elements
477 usually admit to introduce multiple such items simultaneously.
479 \indexouternonterm{vars}\indexouternonterm{props}
481 vars: (name+) ('::' type)?
483 props: thmdecl? (prop proppat? +)
487 The treatment of multiple declarations corresponds to the
488 complementary focus of \railnonterm{vars} versus
489 \railnonterm{props}. In ``\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}}''
490 the typing refers to all variables, while in \isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}} the naming refers to all propositions collectively.
491 Isar language elements that refer to \railnonterm{vars} or
492 \railnonterm{props} typically admit separate typings or namings via
493 another level of iteration, with explicit \indexref{}{keyword}{and}\hyperlink{keyword.and}{\mbox{\isa{\isakeyword{and}}}}
494 separators; e.g.\ see \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}} and \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} in
495 \secref{sec:proof-context}.%
499 \isamarkupsubsection{Antiquotations \label{sec:antiq}%
503 \begin{isamarkuptext}%
504 \begin{matharray}{rcl}
505 \indexdef{}{antiquotation}{theory}\hypertarget{antiquotation.theory}{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isarantiq \\
506 \indexdef{}{antiquotation}{thm}\hypertarget{antiquotation.thm}{\hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}} & : & \isarantiq \\
507 \indexdef{}{antiquotation}{prop}\hypertarget{antiquotation.prop}{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isarantiq \\
508 \indexdef{}{antiquotation}{term}\hypertarget{antiquotation.term}{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}} & : & \isarantiq \\
509 \indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isarantiq \\
510 \indexdef{}{antiquotation}{abbrev}\hypertarget{antiquotation.abbrev}{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}} & : & \isarantiq \\
511 \indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \isarantiq \\
512 \indexdef{}{antiquotation}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isarantiq \\
513 \indexdef{}{antiquotation}{thm\_style}\hypertarget{antiquotation.thm_style}{\hyperlink{antiquotation.thm_style}{\mbox{\isa{thm{\isacharunderscore}style}}}} & : & \isarantiq \\
514 \indexdef{}{antiquotation}{term\_style}\hypertarget{antiquotation.term_style}{\hyperlink{antiquotation.term_style}{\mbox{\isa{term{\isacharunderscore}style}}}} & : & \isarantiq \\
515 \indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isarantiq \\
516 \indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isarantiq \\
517 \indexdef{}{antiquotation}{subgoals}\hypertarget{antiquotation.subgoals}{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}} & : & \isarantiq \\
518 \indexdef{}{antiquotation}{prf}\hypertarget{antiquotation.prf}{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}} & : & \isarantiq \\
519 \indexdef{}{antiquotation}{full\_prf}\hypertarget{antiquotation.full_prf}{\hyperlink{antiquotation.full_prf}{\mbox{\isa{full{\isacharunderscore}prf}}}} & : & \isarantiq \\
520 \indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isarantiq \\
521 \indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML_type}{\hyperlink{antiquotation.ML_type}{\mbox{\isa{ML{\isacharunderscore}type}}}} & : & \isarantiq \\
522 \indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML_struct}{\hyperlink{antiquotation.ML_struct}{\mbox{\isa{ML{\isacharunderscore}struct}}}} & : & \isarantiq \\
525 The text body of formal comments (see also \secref{sec:comments})
526 may contain antiquotations of logical entities, such as theorems,
527 terms and types, which are to be presented in the final output
528 produced by the Isabelle document preparation system (see also
529 \secref{sec:document-prep}).
531 Thus embedding of ``\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}{\isachardoublequote}}''
532 within a text block would cause
533 \isa{{\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharplus}\ x} to appear in the final {\LaTeX} document. Also note that theorem
534 antiquotations may involve attributes as well. For example,
535 \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ sym\ {\isacharbrackleft}no{\isacharunderscore}vars{\isacharbrackright}{\isacharbraceright}{\isachardoublequote}} would print the theorem's
536 statement where all schematic variables have been replaced by fixed
537 ones, which are easier to read.
540 atsign lbrace antiquotation rbrace
544 'theory' options name |
545 'thm' options thmrefs |
546 'prop' options prop |
547 'term' options term |
548 'const' options term |
549 'abbrev' options term |
550 'typeof' options term |
552 'thm\_style' options name thmref |
553 'term\_style' options name term |
554 'text' options name |
557 'prf' options thmrefs |
558 'full\_prf' options thmrefs |
560 'ML\_type' options name |
561 'ML\_struct' options name
563 options: '[' (option * ',') ']'
565 option: name | name '=' name
569 Note that the syntax of antiquotations may \emph{not} include source
570 comments \verb|(*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*)| or verbatim
571 text \verb|{|\verb|*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*|\verb|}|.
575 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}theory\ A{\isacharbraceright}{\isachardoublequote}}] prints the name \isa{{\isachardoublequote}A{\isachardoublequote}}, which is
576 guaranteed to refer to a valid ancestor theory in the current
579 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints theorems
580 \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. Note that attribute specifications
581 may be included as well (see also \secref{sec:syn-att}); the
582 \indexref{}{attribute}{no\_vars}\hyperlink{attribute.no_vars}{\mbox{\isa{no{\isacharunderscore}vars}}} rule (see \secref{sec:misc-meth-att}) would
583 be particularly useful to suppress printing of schematic variables.
585 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}}] prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
587 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}{\isachardoublequote}}] prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}.
589 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}const\ c{\isacharbraceright}{\isachardoublequote}}] prints a logical or syntactic constant
590 \isa{{\isachardoublequote}c{\isachardoublequote}}.
592 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}abbrev\ c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints a constant
593 abbreviation \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ rhs{\isachardoublequote}} as defined in
596 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typeof\ t{\isacharbraceright}{\isachardoublequote}}] prints the type of a well-typed term
597 \isa{{\isachardoublequote}t{\isachardoublequote}}.
599 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}}] prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
601 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm{\isacharunderscore}style\ s\ a{\isacharbraceright}{\isachardoublequote}}] prints theorem \isa{a},
602 previously applying a style \isa{s} to it (see below).
604 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term{\isacharunderscore}style\ s\ t{\isacharbraceright}{\isachardoublequote}}] prints a well-typed term \isa{t} after applying a style \isa{s} to it (see below).
606 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}text\ s{\isacharbraceright}{\isachardoublequote}}] prints uninterpreted source text \isa{s}. This is particularly useful to print portions of text according
607 to the Isabelle {\LaTeX} output style, without demanding
608 well-formedness (e.g.\ small pieces of terms that should not be
609 parsed or type-checked yet).
611 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}}] prints the current \emph{dynamic} goal
612 state. This is mainly for support of tactic-emulation scripts
613 within Isar --- presentation of goal states does not conform to
614 actual human-readable proof documents.
616 Please do not include goal states into document output unless you
617 really know what you are doing!
619 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}subgoals{\isacharbraceright}{\isachardoublequote}}] is similar to \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}}, but
620 does not print the main goal.
622 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints the (compact)
623 proof terms corresponding to the theorems \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. Note that this requires proof terms to be switched on
624 for the current object logic (see the ``Proof terms'' section of the
625 Isabelle reference manual for information on how to do this).
627 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}full{\isacharunderscore}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] is like \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}, but displays the full proof terms,
628 i.e.\ also displays information omitted in the compact proof term,
629 which is denoted by ``\isa{{\isacharunderscore}}'' placeholders there.
631 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML\ s{\isacharbraceright}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML{\isacharunderscore}type\ s{\isacharbraceright}{\isachardoublequote}}, and \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML{\isacharunderscore}struct\ s{\isacharbraceright}{\isachardoublequote}}] check text \isa{s} as ML value, type, and
632 structure, respectively. The source is displayed verbatim.
636 \medskip The following standard styles for use with \isa{thm{\isacharunderscore}style} and \isa{term{\isacharunderscore}style} are available:
640 \item [\isa{lhs}] extracts the first argument of any application
641 form with at least two arguments -- typically meta-level or
642 object-level equality, or any other binary relation.
644 \item [\isa{rhs}] is like \isa{lhs}, but extracts the second
647 \item [\isa{{\isachardoublequote}concl{\isachardoublequote}}] extracts the conclusion \isa{C} from a rule
648 in Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}.
650 \item [\isa{{\isachardoublequote}prem{\isadigit{1}}{\isachardoublequote}}, \dots, \isa{{\isachardoublequote}prem{\isadigit{9}}{\isachardoublequote}}] extract premise
651 number \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isadigit{9}}{\isachardoublequote}}, respectively, from from a rule in
652 Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}
657 The following options are available to tune the output. Note that most of
658 these coincide with ML flags of the same names (see also \cite{isabelle-ref}).
662 \item[\isa{{\isachardoublequote}show{\isacharunderscore}types\ {\isacharequal}\ bool{\isachardoublequote}} and \isa{{\isachardoublequote}show{\isacharunderscore}sorts\ {\isacharequal}\ bool{\isachardoublequote}}]
663 control printing of explicit type and sort constraints.
665 \item[\isa{{\isachardoublequote}show{\isacharunderscore}structs\ {\isacharequal}\ bool{\isachardoublequote}}] controls printing of implicit
668 \item[\isa{{\isachardoublequote}long{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] forces names of types and
669 constants etc.\ to be printed in their fully qualified internal
672 \item[\isa{{\isachardoublequote}short{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] forces names of types and
673 constants etc.\ to be printed unqualified. Note that internalizing
674 the output again in the current context may well yield a different
677 \item[\isa{{\isachardoublequote}unique{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] determines whether the printed
678 version of qualified names should be made sufficiently long to avoid
679 overlap with names declared further back. Set to \isa{false} for
682 \item[\isa{{\isachardoublequote}eta{\isacharunderscore}contract\ {\isacharequal}\ bool{\isachardoublequote}}] prints terms in \isa{{\isasymeta}}-contracted form.
684 \item[\isa{{\isachardoublequote}display\ {\isacharequal}\ bool{\isachardoublequote}}] indicates if the text is to be
685 output as multi-line ``display material'', rather than a small piece
686 of text without line breaks (which is the default).
688 \item[\isa{{\isachardoublequote}break\ {\isacharequal}\ bool{\isachardoublequote}}] controls line breaks in non-display
691 \item[\isa{{\isachardoublequote}quotes\ {\isacharequal}\ bool{\isachardoublequote}}] indicates if the output should be
692 enclosed in double quotes.
694 \item[\isa{{\isachardoublequote}mode\ {\isacharequal}\ name{\isachardoublequote}}] adds \isa{name} to the print mode to
695 be used for presentation (see also \cite{isabelle-ref}). Note that
696 the standard setup for {\LaTeX} output is already present by
697 default, including the modes \isa{latex} and \isa{xsymbols}.
699 \item[\isa{{\isachardoublequote}margin\ {\isacharequal}\ nat{\isachardoublequote}} and \isa{{\isachardoublequote}indent\ {\isacharequal}\ nat{\isachardoublequote}}] change the
700 margin or indentation for pretty printing of display material.
702 \item[\isa{{\isachardoublequote}source\ {\isacharequal}\ bool{\isachardoublequote}}] prints the source text of the
703 antiquotation arguments, rather than the actual value. Note that
704 this does not affect well-formedness checks of \hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}, \hyperlink{antiquotation.term}{\mbox{\isa{term}}}, etc. (only the \hyperlink{antiquotation.text}{\mbox{\isa{text}}} antiquotation admits arbitrary output).
706 \item[\isa{{\isachardoublequote}goals{\isacharunderscore}limit\ {\isacharequal}\ nat{\isachardoublequote}}] determines the maximum number of
709 \item[\isa{{\isachardoublequote}locale\ {\isacharequal}\ name{\isachardoublequote}}] specifies an alternative locale
710 context used for evaluating and printing the subsequent argument.
714 For boolean flags, ``\isa{{\isachardoublequote}name\ {\isacharequal}\ true{\isachardoublequote}}'' may be abbreviated as
715 ``\isa{name}''. All of the above flags are disabled by default,
716 unless changed from ML.
718 \medskip Note that antiquotations do not only spare the author from
719 tedious typing of logical entities, but also achieve some degree of
720 consistency-checking of informal explanations with formal
721 developments: well-formedness of terms and types with respect to the
722 current theory or proof context is ensured here.%
726 \isamarkupsubsection{Tagged commands \label{sec:tags}%
730 \begin{isamarkuptext}%
731 Each Isabelle/Isar command may be decorated by presentation tags:
733 \indexouternonterm{tags}
737 tag: '\%' (ident | string)
740 The tags \isa{{\isachardoublequote}theory{\isachardoublequote}}, \isa{{\isachardoublequote}proof{\isachardoublequote}}, \isa{{\isachardoublequote}ML{\isachardoublequote}} are already
741 pre-declared for certain classes of commands:
746 \isa{{\isachardoublequote}theory{\isachardoublequote}} & theory begin/end \\
747 \isa{{\isachardoublequote}proof{\isachardoublequote}} & all proof commands \\
748 \isa{{\isachardoublequote}ML{\isachardoublequote}} & all commands involving ML code \\
751 \medskip The Isabelle document preparation system (see also
752 \cite{isabelle-sys}) allows tagged command regions to be presented
753 specifically, e.g.\ to fold proof texts, or drop parts of the text
756 For example ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}invisible\ auto{\isachardoublequote}}'' would
757 cause that piece of proof to be treated as \isa{invisible} instead
758 of \isa{{\isachardoublequote}proof{\isachardoublequote}} (the default), which may be either show or hidden
759 depending on the document setup. In contrast, ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}visible\ auto{\isachardoublequote}}'' would force this text to be shown
762 Explicit tag specifications within a proof apply to all subsequent
763 commands of the same level of nesting. For example, ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharpercent}visible\ {\isasymdots}{\isachardoublequote}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}'' would force the
764 whole sub-proof to be typeset as \isa{visible} (unless some of its
765 parts are tagged differently).%
774 \isacommand{end}\isamarkupfalse%
786 %%% TeX-master: "root"