3 \def\isabellecontext{Outer{\isacharunderscore}Syntax}%
12 \isacommand{theory}\isamarkupfalse%
13 \ Outer{\isacharunderscore}Syntax\isanewline
14 \isakeyword{imports}\ Main\isanewline
23 \isamarkupchapter{Outer syntax%
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:outer-lex}%
90 \begin{isamarkuptext}%
91 The outer lexical syntax consists of three main categories of
96 \item \emph{major keywords} --- the command names that are available
97 in the present logic session;
99 \item \emph{minor keywords} --- additional literal tokens required
100 by the syntax of commands;
102 \item \emph{named tokens} --- various categories of identifiers etc.
106 Major keywords and minor keywords are guaranteed to be disjoint.
107 This helps user-interfaces to determine the overall structure of a
108 theory text, without knowing the full details of command syntax.
109 Internally, there is some additional information about the kind of
110 major keywords, which approximates the command type (theory command,
113 Keywords override named tokens. For example, the presence of a
114 command called \verb|term| inhibits the identifier \verb|term|, but the string \verb|"term"| can be used instead.
115 By convention, the outer syntax always allows quoted strings in
116 addition to identifiers, wherever a named entity is expected.
118 When tokenizing a given input sequence, the lexer repeatedly takes
119 the longest prefix of the input that forms a valid token. Spaces,
120 tabs, newlines and formfeeds between tokens serve as explicit
123 \medskip The categories for named tokens are defined once and for
127 \begin{supertabular}{rcl}
128 \indexdef{}{syntax}{ident}\hypertarget{syntax.ident}{\hyperlink{syntax.ident}{\mbox{\isa{ident}}}} & = & \isa{{\isachardoublequote}letter\ quasiletter\isactrlsup {\isacharasterisk}{\isachardoublequote}} \\
129 \indexdef{}{syntax}{longident}\hypertarget{syntax.longident}{\hyperlink{syntax.longident}{\mbox{\isa{longident}}}} & = & \isa{{\isachardoublequote}ident{\isacharparenleft}{\isachardoublequote}}\verb|.|\isa{{\isachardoublequote}ident{\isacharparenright}\isactrlsup {\isacharplus}{\isachardoublequote}} \\
130 \indexdef{}{syntax}{symident}\hypertarget{syntax.symident}{\hyperlink{syntax.symident}{\mbox{\isa{symident}}}} & = & \isa{{\isachardoublequote}sym\isactrlsup {\isacharplus}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\|\verb|<|\isa{ident}\verb|>| \\
131 \indexdef{}{syntax}{nat}\hypertarget{syntax.nat}{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}} & = & \isa{{\isachardoublequote}digit\isactrlsup {\isacharplus}{\isachardoublequote}} \\
132 \indexdef{}{syntax}{var}\hypertarget{syntax.var}{\hyperlink{syntax.var}{\mbox{\isa{var}}}} & = & \verb|?|\isa{{\isachardoublequote}ident\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|?|\isa{ident}\verb|.|\isa{nat} \\
133 \indexdef{}{syntax}{typefree}\hypertarget{syntax.typefree}{\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}}} & = & \verb|'|\isa{ident} \\
134 \indexdef{}{syntax}{typevar}\hypertarget{syntax.typevar}{\hyperlink{syntax.typevar}{\mbox{\isa{typevar}}}} & = & \verb|?|\isa{{\isachardoublequote}typefree\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|?|\isa{typefree}\verb|.|\isa{nat} \\
135 \indexdef{}{syntax}{string}\hypertarget{syntax.string}{\hyperlink{syntax.string}{\mbox{\isa{string}}}} & = & \verb|"| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|"| \\
136 \indexdef{}{syntax}{altstring}\hypertarget{syntax.altstring}{\hyperlink{syntax.altstring}{\mbox{\isa{altstring}}}} & = & \verb|`| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|`| \\
137 \indexdef{}{syntax}{verbatim}\hypertarget{syntax.verbatim}{\hyperlink{syntax.verbatim}{\mbox{\isa{verbatim}}}} & = & \verb|{*| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|*|\verb|}| \\[1ex]
139 \isa{letter} & = & \isa{{\isachardoublequote}latin\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\|\verb|<|\isa{latin}\verb|>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\|\verb|<|\isa{{\isachardoublequote}latin\ latin{\isachardoublequote}}\verb|>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ greek\ \ {\isacharbar}{\isachardoublequote}} \\
140 & & \verb|\<^isub>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<^isup>| \\
141 \isa{quasiletter} & = & \isa{{\isachardoublequote}letter\ \ {\isacharbar}\ \ digit\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|'| \\
142 \isa{latin} & = & \verb|a|\isa{{\isachardoublequote}\ \ {\isacharbar}\ {\isasymdots}\ {\isacharbar}\ \ {\isachardoublequote}}\verb|z|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|A|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isasymdots}\ {\isacharbar}\ \ {\isachardoublequote}}\verb|Z| \\
143 \isa{digit} & = & \verb|0|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isasymdots}\ {\isacharbar}\ \ {\isachardoublequote}}\verb|9| \\
144 \isa{sym} & = & \verb|!|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|#|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|$|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|%|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|&|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|*|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|+|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|-|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|/|\isa{{\isachardoublequote}\ \ {\isacharbar}{\isachardoublequote}} \\
145 & & \verb|<|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|=|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|?|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|@|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|^|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb||\verb,|,\verb||\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|~| \\
146 \isa{greek} & = & \verb|\<alpha>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<beta>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<gamma>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<delta>|\isa{{\isachardoublequote}\ \ {\isacharbar}{\isachardoublequote}} \\
147 & & \verb|\<epsilon>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<zeta>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<eta>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<theta>|\isa{{\isachardoublequote}\ \ {\isacharbar}{\isachardoublequote}} \\
148 & & \verb|\<iota>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<kappa>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<mu>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<nu>|\isa{{\isachardoublequote}\ \ {\isacharbar}{\isachardoublequote}} \\
149 & & \verb|\<xi>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<pi>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<rho>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<sigma>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<tau>|\isa{{\isachardoublequote}\ \ {\isacharbar}{\isachardoublequote}} \\
150 & & \verb|\<upsilon>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<phi>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<chi>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<psi>|\isa{{\isachardoublequote}\ \ {\isacharbar}{\isachardoublequote}} \\
151 & & \verb|\<omega>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<Gamma>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<Delta>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<Theta>|\isa{{\isachardoublequote}\ \ {\isacharbar}{\isachardoublequote}} \\
152 & & \verb|\<Lambda>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<Xi>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<Pi>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<Sigma>|\isa{{\isachardoublequote}\ \ {\isacharbar}{\isachardoublequote}} \\
153 & & \verb|\<Upsilon>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<Phi>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<Psi>|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\<Omega>| \\
157 A \indexref{}{syntax}{var}\hyperlink{syntax.var}{\mbox{\isa{var}}} or \indexref{}{syntax}{typevar}\hyperlink{syntax.typevar}{\mbox{\isa{typevar}}} describes an unknown,
158 which is internally a pair of base name and index (ML type \verb|indexname|). These components are either separated by a dot as in
159 \isa{{\isachardoublequote}{\isacharquery}x{\isachardot}{\isadigit{1}}{\isachardoublequote}} or \isa{{\isachardoublequote}{\isacharquery}x{\isadigit{7}}{\isachardot}{\isadigit{3}}{\isachardoublequote}} or run together as in \isa{{\isachardoublequote}{\isacharquery}x{\isadigit{1}}{\isachardoublequote}}. The latter form is possible if the base name does not end
160 with digits. If the index is 0, it may be dropped altogether:
161 \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}} and \isa{{\isachardoublequote}{\isacharquery}x{\isadigit{0}}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isacharquery}x{\isachardot}{\isadigit{0}}{\isachardoublequote}} all refer to the
162 same unknown, with basename \isa{{\isachardoublequote}x{\isachardoublequote}} and index 0.
164 The syntax of \indexref{}{syntax}{string}\hyperlink{syntax.string}{\mbox{\isa{string}}} admits any characters, including
165 newlines; ``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) need to be escaped by a backslash; arbitrary
166 character codes may be specified as ``\verb|\|\isa{ddd}'',
167 with three decimal digits. Alternative strings according to
168 \indexref{}{syntax}{altstring}\hyperlink{syntax.altstring}{\mbox{\isa{altstring}}} are analogous, using single back-quotes
171 The body of \indexref{}{syntax}{verbatim}\hyperlink{syntax.verbatim}{\mbox{\isa{verbatim}}} may consist of any text not
172 containing ``\verb|*|\verb|}|''; this allows
173 convenient inclusion of quotes without further escapes. There is no
174 way to escape ``\verb|*|\verb|}|''. If the quoted
175 text is {\LaTeX} source, one may usually add some blank or comment
176 to avoid the critical character sequence.
178 Source comments take the form \verb|(*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*)| and may be nested, although the user-interface
179 might prevent this. Note that this form indicates source comments
180 only, which are stripped after lexical analysis of the input. The
181 Isar syntax also provides proper \emph{document comments} that are
182 considered as part of the text (see \secref{sec:comments}).
184 Common mathematical symbols such as \isa{{\isasymforall}} are represented in
185 Isabelle as \verb|\<forall>|. There are infinitely many Isabelle
186 symbols like this, although proper presentation is left to front-end
187 tools such as {\LaTeX} or Proof~General with the X-Symbol package.
188 A list of standard Isabelle symbols that work well with these tools
189 is given in \appref{app:symbols}. Note that \verb|\<lambda>| does
190 not belong to the \isa{letter} category, since it is already used
191 differently in the Pure term language.%
195 \isamarkupsection{Common syntax entities%
199 \begin{isamarkuptext}%
200 We now introduce several basic syntactic entities, such as names,
201 terms, and theorem specifications, which are factored out of the
202 actual Isar language elements to be described later.%
206 \isamarkupsubsection{Names%
210 \begin{isamarkuptext}%
211 Entity \railqtok{name} usually refers to any name of types,
212 constants, theorems etc.\ that are to be \emph{declared} or
213 \emph{defined} (so qualified identifiers are excluded here). Quoted
214 strings provide an escape for non-identifier names or those ruled
215 out by outer syntax keywords (e.g.\ quoted \verb|"let"|).
216 Already existing objects are usually referenced by
219 \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
220 \indexoutertoken{int}
222 name: ident | symident | string | nat
224 parname: '(' name ')'
226 nameref: name | longident
234 \isamarkupsubsection{Comments \label{sec:comments}%
238 \begin{isamarkuptext}%
239 Large chunks of plain \railqtok{text} are usually given
240 \railtok{verbatim}, i.e.\ enclosed in \verb|{|\verb|*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*|\verb|}|. For convenience,
241 any of the smaller text units conforming to \railqtok{nameref} are
242 admitted as well. A marginal \railnonterm{comment} is of the form
243 \verb|--| \railqtok{text}. Any number of these may occur
244 within Isabelle/Isar commands.
246 \indexoutertoken{text}\indexouternonterm{comment}
248 text: verbatim | nameref
256 \isamarkupsubsection{Type classes, sorts and arities%
260 \begin{isamarkuptext}%
261 Classes are specified by plain names. Sorts have a very simple
262 inner syntax, which is either a single class name \isa{c} or a
263 list \isa{{\isachardoublequote}{\isacharbraceleft}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isacharbraceright}{\isachardoublequote}} referring to the
264 intersection of these classes. The syntax of type arities is given
265 directly at the outer level.
267 \indexouternonterm{sort}\indexouternonterm{arity}
268 \indexouternonterm{classdecl}
270 classdecl: name (('<' | subseteq) (nameref + ','))?
274 arity: ('(' (sort + ',') ')')? sort
280 \isamarkupsubsection{Types and terms \label{sec:types-terms}%
284 \begin{isamarkuptext}%
285 The actual inner Isabelle syntax, that of types and terms of the
286 logic, is far too sophisticated in order to be modelled explicitly
287 at the outer theory level. Basically, any such entity has to be
288 quoted to turn it into a single token (the parsing and type-checking
289 is performed internally later). For convenience, a slightly more
290 liberal convention is adopted: quotes may be omitted for any type or
291 term that is already atomic at the outer level. For example, one
292 may just write \verb|x| instead of quoted \verb|"x"|.
293 Note that symbolic identifiers (e.g.\ \verb|++| or \isa{{\isachardoublequote}{\isasymforall}{\isachardoublequote}} are available as well, provided these have not been superseded
294 by commands or other keywords already (such as \verb|=| or
297 \indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
299 type: nameref | typefree | typevar
307 Positional instantiations are indicated by giving a sequence of
308 terms, or the placeholder ``\isa{{\isacharunderscore}}'' (underscore), which means to
311 \indexoutertoken{inst}\indexoutertoken{insts}
313 inst: underscore | term
319 Type declarations and definitions usually refer to
320 \railnonterm{typespec} on the left-hand side. This models basic
321 type constructor application at the outer syntax level. Note that
322 only plain postfix notation is available here, but no infixes.
324 \indexouternonterm{typespec}
326 typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
332 \isamarkupsubsection{Term patterns and declarations \label{sec:term-decls}%
336 \begin{isamarkuptext}%
337 Wherever explicit propositions (or term fragments) occur in a proof
338 text, casual binding of schematic term variables may be given
339 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}.
341 \indexouternonterm{termpat}\indexouternonterm{proppat}
343 termpat: '(' ('is' term +) ')'
345 proppat: '(' ('is' prop +) ')'
349 \medskip Declarations of local variables \isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}} and
350 logical propositions \isa{{\isachardoublequote}a\ {\isacharcolon}\ {\isasymphi}{\isachardoublequote}} represent different views on
351 the same principle of introducing a local scope. In practice, one
352 may usually omit the typing of \railnonterm{vars} (due to
353 type-inference), and the naming of propositions (due to implicit
354 references of current facts). In any case, Isar proof elements
355 usually admit to introduce multiple such items simultaneously.
357 \indexouternonterm{vars}\indexouternonterm{props}
359 vars: (name+) ('::' type)?
361 props: thmdecl? (prop proppat? +)
365 The treatment of multiple declarations corresponds to the
366 complementary focus of \railnonterm{vars} versus
367 \railnonterm{props}. In ``\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}}''
368 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.
369 Isar language elements that refer to \railnonterm{vars} or
370 \railnonterm{props} typically admit separate typings or namings via
371 another level of iteration, with explicit \indexref{}{keyword}{and}\hyperlink{keyword.and}{\mbox{\isa{\isakeyword{and}}}}
372 separators; e.g.\ see \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}} and \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} in
373 \secref{sec:proof-context}.%
377 \isamarkupsubsection{Attributes and theorems \label{sec:syn-att}%
381 \begin{isamarkuptext}%
382 Attributes have their own ``semi-inner'' syntax, in the sense
383 that input conforming to \railnonterm{args} below is parsed by the
384 attribute a second time. The attribute argument specifications may
385 be any sequence of atomic entities (identifiers, strings etc.), or
386 properly bracketed argument lists. Below \railqtok{atom} refers to
387 any atomic entity, including any \railtok{keyword} conforming to
390 \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
392 atom: nameref | typefree | typevar | var | nat | keyword
394 arg: atom | '(' args ')' | '[' args ']'
398 attributes: '[' (nameref args * ',') ']'
402 Theorem specifications come in several flavors:
403 \railnonterm{axmdecl} and \railnonterm{thmdecl} usually refer to
404 axioms, assumptions or results of goal statements, while
405 \railnonterm{thmdef} collects lists of existing theorems. Existing
406 theorems are given by \railnonterm{thmref} and
407 \railnonterm{thmrefs}, the former requires an actual singleton
410 There are three forms of theorem references:
413 \item named facts \isa{{\isachardoublequote}a{\isachardoublequote}},
415 \item selections from named facts \isa{{\isachardoublequote}a{\isacharparenleft}i{\isacharparenright}{\isachardoublequote}} or \isa{{\isachardoublequote}a{\isacharparenleft}j\ {\isacharminus}\ k{\isacharparenright}{\isachardoublequote}},
417 \item literal fact propositions using \indexref{}{syntax}{altstring}\hyperlink{syntax.altstring}{\mbox{\isa{altstring}}} syntax
418 \verb|`|\isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}\verb|`| (see also method
419 \indexref{}{method}{fact}\hyperlink{method.fact}{\mbox{\isa{fact}}}).
423 Any kind of theorem specification may include lists of attributes
424 both on the left and right hand sides; attributes are applied to any
425 immediately preceding fact. If names are omitted, the theorems are
426 not stored within the theorem database of the theory or proof
427 context, but any given attributes are applied nonetheless.
429 An extra pair of brackets around attributes (like ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbrackleft}simproc\ a{\isacharbrackright}{\isacharbrackright}{\isachardoublequote}}'') abbreviates a theorem reference involving an
430 internal dummy fact, which will be ignored later on. So only the
431 effect of the attribute on the background context will persist.
432 This form of in-place declarations is particularly useful with
433 commands like \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} and \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}.
435 \indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
436 \indexouternonterm{thmdef}\indexouternonterm{thmref}
437 \indexouternonterm{thmrefs}\indexouternonterm{selection}
439 axmdecl: name attributes? ':'
445 thmref: (nameref selection? | altstring) attributes? | '[' attributes ']'
450 thmbind: name attributes | name | attributes
452 selection: '(' ((nat | nat '-' nat?) + ',') ')'
463 \isacommand{end}\isamarkupfalse%
475 %%% TeX-master: "root"