3 \def\isabellecontext{Inner{\isacharunderscore}Syntax}%
10 \isacommand{theory}\isamarkupfalse%
11 \ Inner{\isacharunderscore}Syntax\isanewline
12 \isakeyword{imports}\ Main\isanewline
21 \isamarkupchapter{Inner syntax --- the term language \label{ch:inner-syntax}%
25 \isamarkupsection{Printing logical entities%
29 \isamarkupsubsection{Diagnostic commands%
33 \begin{isamarkuptext}%
34 \begin{matharray}{rcl}
35 \indexdef{}{command}{typ}\hypertarget{command.typ}{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
36 \indexdef{}{command}{term}\hypertarget{command.term}{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
37 \indexdef{}{command}{prop}\hypertarget{command.prop}{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
38 \indexdef{}{command}{thm}\hypertarget{command.thm}{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
39 \indexdef{}{command}{prf}\hypertarget{command.prf}{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
40 \indexdef{}{command}{full\_prf}\hypertarget{command.full-prf}{\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
41 \indexdef{}{command}{pr}\hypertarget{command.pr}{\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
44 These diagnostic commands assist interactive development by printing
45 internal logical entities in a human-readable fashion.
56 ( 'prf' | 'full\_prf' ) modes? thmrefs?
58 'pr' modes? nat? (',' nat)?
61 modes: '(' (name + ) ')'
67 \item \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isasymtau}} reads and prints types of the
68 meta-logic according to the current theory or proof context.
70 \item \hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}~\isa{t} and \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isasymphi}}
71 read, type-check and print terms or propositions according to the
72 current theory or proof context; the inferred type of \isa{t} is
73 output as well. Note that these commands are also useful in
74 inspecting the current environment of term abbreviations.
76 \item \hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} retrieves
77 theorems from the current theory or proof context. Note that any
78 attributes included in the theorem specifications are applied to a
79 temporary context derived from the current theory or proof; the
80 result is discarded, i.e.\ attributes involved in \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}} do not have any permanent effect.
82 \item \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}} displays the (compact) proof term of the
83 current proof state (if present), or of the given theorems. Note
84 that this requires proof terms to be switched on for the current
85 object logic (see the ``Proof terms'' section of the Isabelle
86 reference manual for information on how to do this).
88 \item \hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}} is like \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}, but displays
89 the full proof term, i.e.\ also displays information omitted in the
90 compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders
93 \item \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isacharcomma}\ prems{\isachardoublequote}} prints the current
94 proof state (if present), including the proof context, current facts
95 and goals. The optional limit arguments affect the number of goals
96 and premises to be displayed, which is initially 10 for both.
97 Omitting limit values leaves the current setting unchanged.
101 All of the diagnostic commands above admit a list of \isa{modes}
102 to be specified, which is appended to the current print mode (see
103 also \cite{isabelle-ref}). Thus the output behavior may be modified
104 according particular print mode features. For example, \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}{\isacharparenleft}latex\ xsymbols{\isacharparenright}{\isachardoublequote}} would print the current proof state
105 with mathematical symbols and special characters represented in
106 {\LaTeX} source, according to the Isabelle style
109 Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
110 systematic way to include formal items into the printed text
115 \isamarkupsubsection{Details of printed content%
119 \begin{isamarkuptext}%
121 \indexdef{}{ML}{show\_types}\verb|show_types: bool Unsynchronized.ref| & default \verb|false| \\
122 \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Unsynchronized.ref| & default \verb|false| \\
123 \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Unsynchronized.ref| & default \verb|false| \\
124 \indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\
125 \indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\
126 \indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\
127 \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Unsynchronized.ref| & default \verb|false| \\
128 \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Unsynchronized.ref| & default \verb|true| \\
129 \indexdef{}{ML}{goals\_limit}\verb|goals_limit: int Unsynchronized.ref| & default \verb|10| \\
130 \indexdef{}{ML}{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool Unsynchronized.ref| & default \verb|false| \\
131 \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool Unsynchronized.ref| & default \verb|false| \\
132 \indexdef{}{ML}{show\_tags}\verb|show_tags: bool Unsynchronized.ref| & default \verb|false| \\
133 \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Unsynchronized.ref| & default \verb|true| \\
136 These global ML variables control the detail of information that is
137 displayed for types, terms, theorems, goals etc.
139 In interactive sessions, the user interface usually manages these
140 global parameters of the Isabelle process, even with some concept of
141 persistence. Nonetheless it is occasionally useful to manipulate ML
142 variables directly, e.g.\ using \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} or \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}.
144 Batch-mode logic sessions may be configured by putting appropriate
145 ML text directly into the \verb|ROOT.ML| file.
149 \item \verb|show_types| and \verb|show_sorts| control printing of type
150 constraints for term variables, and sort constraints for type
151 variables. By default, neither of these are shown in output. If
152 \verb|show_sorts| is set to \verb|true|, types are always shown as
155 Note that displaying types and sorts may explain why a polymorphic
156 inference rule fails to resolve with some goal, or why a rewrite
157 rule does not apply as expected.
159 \item \verb|show_consts| controls printing of types of constants when
160 displaying a goal state.
162 Note that the output can be enormous, because polymorphic constants
163 often occur at several different type instances.
165 \item \verb|long_names|, \verb|short_names|, and \verb|unique_names|
166 control the way of printing fully qualified internal names in
167 external form. See also \secref{sec:antiq} for the document
168 antiquotation options of the same names.
170 \item \verb|show_brackets| controls bracketing in pretty printed
171 output. If set to \verb|true|, all sub-expressions of the pretty
172 printing tree will be parenthesized, even if this produces malformed
173 term syntax! This crude way of showing the internal structure of
174 pretty printed entities may occasionally help to diagnose problems
175 with operator priorities, for example.
177 \item \verb|eta_contract| controls \isa{{\isachardoublequote}{\isasymeta}{\isachardoublequote}}-contracted printing of
180 The \isa{{\isasymeta}}-contraction law asserts \isa{{\isachardoublequote}{\isacharparenleft}{\isasymlambda}x{\isachardot}\ f\ x{\isacharparenright}\ {\isasymequiv}\ f{\isachardoublequote}},
181 provided \isa{x} is not free in \isa{f}. It asserts
182 \emph{extensionality} of functions: \isa{{\isachardoublequote}f\ {\isasymequiv}\ g{\isachardoublequote}} if \isa{{\isachardoublequote}f\ x\ {\isasymequiv}\ g\ x{\isachardoublequote}} for all \isa{x}. Higher-order unification frequently puts
183 terms into a fully \isa{{\isasymeta}}-expanded form. For example, if \isa{F} has type \isa{{\isachardoublequote}{\isacharparenleft}{\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}{\isacharparenright}\ {\isasymRightarrow}\ {\isasymtau}{\isachardoublequote}} then its expanded form is \isa{{\isachardoublequote}{\isasymlambda}h{\isachardot}\ F\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ h\ x{\isacharparenright}{\isachardoublequote}}.
185 Setting \verb|eta_contract| makes Isabelle perform \isa{{\isasymeta}}-contractions before printing, so that \isa{{\isachardoublequote}{\isasymlambda}h{\isachardot}\ F\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ h\ x{\isacharparenright}{\isachardoublequote}}
186 appears simply as \isa{F}.
188 Note that the distinction between a term and its \isa{{\isasymeta}}-expanded
189 form occasionally matters. While higher-order resolution and
190 rewriting operate modulo \isa{{\isachardoublequote}{\isasymalpha}{\isasymbeta}{\isasymeta}{\isachardoublequote}}-conversion, some other tools
191 might look at terms more discretely.
193 \item \verb|goals_limit| controls the maximum number of subgoals to
194 be shown in goal output.
196 \item \verb|Proof.show_main_goal| controls whether the main result to
197 be proven should be displayed. This information might be relevant
198 for schematic goals, to inspect the current claim that has been
201 \item \verb|show_hyps| controls printing of implicit hypotheses of
202 local facts. Normally, only those hypotheses are displayed that are
203 \emph{not} covered by the assumptions of the current context: this
204 situation indicates a fault in some tool being used.
206 By setting \verb|show_hyps| to \verb|true|, output of \emph{all}
207 hypotheses can be enforced, which is occasionally useful for
210 \item \verb|show_tags| controls printing of extra annotations within
211 theorems, such as internal position information, or the case names
212 being attached by the attribute \hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}}.
214 Note that the \hyperlink{attribute.tagged}{\mbox{\isa{tagged}}} and \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}
215 attributes provide low-level access to the collection of tags
216 associated with a theorem.
218 \item \verb|show_question_marks| controls printing of question marks
219 for schematic variables, such as \isa{{\isacharquery}x}. Only the leading
220 question mark is affected, the remaining text is unchanged
221 (including proper markup for schematic variables that might be
222 relevant for user interfaces).
228 \isamarkupsubsection{Printing limits%
232 \begin{isamarkuptext}%
234 \indexdef{}{ML}{Pretty.margin\_default}\verb|Pretty.margin_default: int Unsynchronized.ref| \\
235 \indexdef{}{ML}{print\_depth}\verb|print_depth: int -> unit| \\
238 These ML functions set limits for pretty printed text.
242 \item \verb|Pretty.margin_default| indicates the global default for
243 the right margin of the built-in pretty printer, with initial value
244 76. Note that user-interfaces typically control margins
245 automatically when resizing windows, or even bypass the formatting
246 engine of Isabelle/ML altogether and do it within the front end via
249 \item \verb|print_depth|~\isa{n} limits the printing depth of the
250 ML toplevel pretty printer; the precise effect depends on the ML
251 compiler and run-time system. Typically \isa{n} should be less
252 than 10. Bigger values such as 100--1000 are useful for debugging.
258 \isamarkupsection{Mixfix annotations%
262 \begin{isamarkuptext}%
263 Mixfix annotations specify concrete \emph{inner syntax} of
264 Isabelle types and terms. Locally fixed parameters in toplevel
265 theorem statements, locale specifications etc.\ also admit mixfix
268 \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
270 infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')'
272 mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
274 structmixfix: mixfix | '(' 'structure' ')'
277 prios: '[' (nat + ',') ']'
281 Here the \railtok{string} specifications refer to the actual mixfix
282 template, which may include literal text, spacing, blocks, and
283 arguments (denoted by ``\isa{{\isacharunderscore}}''); the special symbol
284 ``\verb|\<index>|'' (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}'') represents an index
285 argument that specifies an implicit structure reference (see also
286 \secref{sec:locale}). Infix and binder declarations provide common
287 abbreviations for particular mixfix declarations. So in practice,
288 mixfix templates mostly degenerate to literal text for concrete
289 syntax, such as ``\verb|++|'' for an infix symbol.
291 \medskip In full generality, mixfix declarations work as follows.
292 Suppose a constant \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymtau}\isactrlsub n\ {\isasymRightarrow}\ {\isasymtau}{\isachardoublequote}} is
293 annotated by \isa{{\isachardoublequote}{\isacharparenleft}mixfix\ {\isacharbrackleft}p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n{\isacharbrackright}\ p{\isacharparenright}{\isachardoublequote}}, where \isa{{\isachardoublequote}mixfix{\isachardoublequote}} is a string \isa{{\isachardoublequote}d\isactrlsub {\isadigit{0}}\ {\isacharunderscore}\ d\isactrlsub {\isadigit{1}}\ {\isacharunderscore}\ {\isasymdots}\ {\isacharunderscore}\ d\isactrlsub n{\isachardoublequote}} consisting of
294 delimiters that surround argument positions as indicated by
297 Altogether this determines a production for a context-free priority
298 grammar, where for each argument \isa{{\isachardoublequote}i{\isachardoublequote}} the syntactic category
299 is determined by \isa{{\isachardoublequote}{\isasymtau}\isactrlsub i{\isachardoublequote}} (with priority \isa{{\isachardoublequote}p\isactrlsub i{\isachardoublequote}}), and
300 the result category is determined from \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} (with
301 priority \isa{{\isachardoublequote}p{\isachardoublequote}}). Priority specifications are optional, with
302 default 0 for arguments and 1000 for the result.
304 Since \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} may be again a function type, the constant
305 type scheme may have more argument positions than the mixfix
306 pattern. Printing a nested application \isa{{\isachardoublequote}c\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub m{\isachardoublequote}} for
307 \isa{{\isachardoublequote}m\ {\isachargreater}\ n{\isachardoublequote}} works by attaching concrete notation only to the
308 innermost part, essentially by printing \isa{{\isachardoublequote}{\isacharparenleft}c\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isacharparenright}\ {\isasymdots}\ t\isactrlsub m{\isachardoublequote}}
309 instead. If a term has fewer arguments than specified in the mixfix
310 template, the concrete syntax is ignored.
312 \medskip A mixfix template may also contain additional directives
313 for pretty printing, notably spaces, blocks, and breaks. The
314 general template format is a sequence over any of the following
319 \item \isa{{\isachardoublequote}d{\isachardoublequote}} is a delimiter, namely a non-empty sequence of
320 characters other than the following special characters:
324 \verb|'| & single quote \\
325 \verb|_| & underscore \\
326 \isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}} & index symbol \\
327 \verb|(| & open parenthesis \\
328 \verb|)| & close parenthesis \\
333 \item \verb|'| escapes the special meaning of these
334 meta-characters, producing a literal version of the following
335 character, unless that is a blank.
337 A single quote followed by a blank separates delimiters, without
338 affecting printing, but input tokens may have additional white space
341 \item \verb|_| is an argument position, which stands for a
342 certain syntactic category in the underlying grammar.
344 \item \isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}} is an indexed argument position; this is the place
345 where implicit structure arguments can be attached.
347 \item \isa{{\isachardoublequote}s{\isachardoublequote}} is a non-empty sequence of spaces for printing.
348 This and the following specifications do not affect parsing at all.
350 \item \verb|(|\isa{n} opens a pretty printing block. The
351 optional number specifies how much indentation to add when a line
352 break occurs within the block. If the parenthesis is not followed
353 by digits, the indentation defaults to 0. A block specified via
354 \verb|(00| is unbreakable.
356 \item \verb|)| closes a pretty printing block.
358 \item \verb|//| forces a line break.
360 \item \verb|/|\isa{s} allows a line break. Here \isa{s}
361 stands for the string of spaces (zero or more) right after the
362 slash. These spaces are printed if the break is \emph{not} taken.
366 For example, the template \verb|(_ +/ _)| specifies an infix
367 operator. There are two argument positions; the delimiter
368 \verb|+| is preceded by a space and followed by a space or
369 line break; the entire phrase is a pretty printing block.
371 The general idea of pretty printing with blocks and breaks is also
372 described in \cite{paulson-ml2}.%
376 \isamarkupsection{Explicit notation%
380 \begin{isamarkuptext}%
381 \begin{matharray}{rcll}
382 \indexdef{}{command}{type\_notation}\hypertarget{command.type-notation}{\hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
383 \indexdef{}{command}{no\_type\_notation}\hypertarget{command.no-type-notation}{\hyperlink{command.no-type-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}type{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
384 \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
385 \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
386 \indexdef{}{command}{write}\hypertarget{command.write}{\hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
390 ('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and')
392 ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
394 'write' mode? (nameref structmixfix + 'and')
400 \item \hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix
401 syntax with an existing type constructor. The arity of the
402 constructor is retrieved from the context.
404 \item \hyperlink{command.no-type-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}type{\isacharunderscore}notation}}}} is similar to \hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}, but removes the specified syntax annotation from
407 \item \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix
408 syntax with an existing constant or fixed variable. The type
409 declaration of the given entity is retrieved from the context.
411 \item \hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}},
412 but removes the specified syntax annotation from the present
415 \item \hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but
416 works within an Isar proof body.
420 Note that the more primitive commands \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} and
421 \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}} (\secref{sec:syn-trans}) provide raw access
422 to the syntax tables of a global theory.%
426 \isamarkupsection{The Pure syntax \label{sec:pure-syntax}%
430 \isamarkupsubsection{Priority grammars \label{sec:priority-grammar}%
434 \begin{isamarkuptext}%
435 A context-free grammar consists of a set of \emph{terminal
436 symbols}, a set of \emph{nonterminal symbols} and a set of
437 \emph{productions}. Productions have the form \isa{{\isachardoublequote}A\ {\isacharequal}\ {\isasymgamma}{\isachardoublequote}},
438 where \isa{A} is a nonterminal and \isa{{\isasymgamma}} is a string of
439 terminals and nonterminals. One designated nonterminal is called
440 the \emph{root symbol}. The language defined by the grammar
441 consists of all strings of terminals that can be derived from the
442 root symbol by applying productions as rewrite rules.
444 The standard Isabelle parser for inner syntax uses a \emph{priority
445 grammar}. Each nonterminal is decorated by an integer priority:
446 \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup p\isactrlsup {\isacharparenright}{\isachardoublequote}}. In a derivation, \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup p\isactrlsup {\isacharparenright}{\isachardoublequote}} may be rewritten
447 using a production \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup q\isactrlsup {\isacharparenright}\ {\isacharequal}\ {\isasymgamma}{\isachardoublequote}} only if \isa{{\isachardoublequote}p\ {\isasymle}\ q{\isachardoublequote}}. Any
448 priority grammar can be translated into a normal context-free
449 grammar by introducing new nonterminals and productions.
451 \medskip Formally, a set of context free productions \isa{G}
452 induces a derivation relation \isa{{\isachardoublequote}{\isasymlongrightarrow}\isactrlsub G{\isachardoublequote}} as follows. Let \isa{{\isasymalpha}} and \isa{{\isasymbeta}} denote strings of terminal or nonterminal symbols.
453 Then \isa{{\isachardoublequote}{\isasymalpha}\ A\isactrlsup {\isacharparenleft}\isactrlsup p\isactrlsup {\isacharparenright}\ {\isasymbeta}\ {\isasymlongrightarrow}\isactrlsub G\ {\isasymalpha}\ {\isasymgamma}\ {\isasymbeta}{\isachardoublequote}} holds if and only if \isa{G}
454 contains some production \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup q\isactrlsup {\isacharparenright}\ {\isacharequal}\ {\isasymgamma}{\isachardoublequote}} for \isa{{\isachardoublequote}p\ {\isasymle}\ q{\isachardoublequote}}.
456 \medskip The following grammar for arithmetic expressions
457 demonstrates how binding power and associativity of operators can be
458 enforced by priorities.
461 \begin{tabular}{rclr}
462 \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \verb|(| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|)| \\
463 \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \verb|0| \\
464 \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|+| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \\
465 \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|*| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \\
466 \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \verb|-| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \\
469 The choice of priorities determines that \verb|-| binds
470 tighter than \verb|*|, which binds tighter than \verb|+|. Furthermore \verb|+| associates to the left and
471 \verb|*| to the right.
473 \medskip For clarity, grammars obey these conventions:
476 \item All priorities must lie between 0 and 1000.
478 \item Priority 0 on the right-hand side and priority 1000 on the
479 left-hand side may be omitted.
481 \item The production \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup p\isactrlsup {\isacharparenright}\ {\isacharequal}\ {\isasymalpha}{\isachardoublequote}} is written as \isa{{\isachardoublequote}A\ {\isacharequal}\ {\isasymalpha}\ {\isacharparenleft}p{\isacharparenright}{\isachardoublequote}}, i.e.\ the priority of the left-hand side actually appears in
482 a column on the far right.
484 \item Alternatives are separated by \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}.
486 \item Repetition is indicated by dots \isa{{\isachardoublequote}{\isacharparenleft}{\isasymdots}{\isacharparenright}{\isachardoublequote}} in an informal
491 Using these conventions, the example grammar specification above
494 \begin{tabular}{rclc}
495 \isa{A} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \verb|(| \isa{A} \verb|)| \\
496 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|0| & \qquad\qquad \\
497 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{A} \verb|+| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
498 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|*| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\
499 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|-| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\
505 \isamarkupsubsection{The Pure grammar%
509 \begin{isamarkuptext}%
510 The priority grammar of the \isa{{\isachardoublequote}Pure{\isachardoublequote}} theory is defined as follows:
512 %FIXME syntax for "index" (?)
513 %FIXME "op" versions of ==> etc. (?)
516 \begin{supertabular}{rclr}
518 \indexdef{inner}{syntax}{any}\hypertarget{syntax.inner.any}{\hyperlink{syntax.inner.any}{\mbox{\isa{any}}}} & = & \isa{{\isachardoublequote}prop\ \ {\isacharbar}\ \ logic{\isachardoublequote}} \\\\
520 \indexdef{inner}{syntax}{prop}\hypertarget{syntax.inner.prop}{\hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}} & = & \verb|(| \isa{prop} \verb|)| \\
521 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{4}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|::| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\
522 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|=?=| \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\
523 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|==| \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\
524 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\
525 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|&&&| \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\
526 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|==>| \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}} \\
527 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}} \\
528 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[|\verb,|,\verb|| \isa{prop} \verb|;| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|;| \isa{prop} \verb||\verb,|,\verb|]| \verb|==>| \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}} \\
529 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlbrakk}{\isachardoublequote}} \isa{prop} \verb|;| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|;| \isa{prop} \isa{{\isachardoublequote}{\isasymrbrakk}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}} \\
530 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|!!| \isa{idts} \verb|.| \isa{prop} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
531 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} \isa{idts} \verb|.| \isa{prop} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
532 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|OFCLASS| \verb|(| \isa{type} \verb|,| \isa{logic} \verb|)| \\
533 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|SORT_CONSTRAINT| \verb|(| \isa{type} \verb|)| \\
534 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|TERM| \isa{logic} \\
535 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|PROP| \isa{aprop} \\\\
537 \indexdef{inner}{syntax}{aprop}\hypertarget{syntax.inner.aprop}{\hyperlink{syntax.inner.aprop}{\mbox{\isa{aprop}}}} & = & \verb|(| \isa{aprop} \verb|)| \\
538 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ var\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|...| \\
539 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|CONST| \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|CONST| \isa{{\isachardoublequote}longid{\isachardoublequote}} \\
540 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}logic\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ \ any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ {\isasymdots}\ any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}{\isachardoublequote}} \\\\
542 \indexdef{inner}{syntax}{logic}\hypertarget{syntax.inner.logic}{\hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}}} & = & \verb|(| \isa{logic} \verb|)| \\
543 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}logic\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{4}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|::| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\
544 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ var\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|...| \\
545 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|CONST| \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|CONST| \isa{{\isachardoublequote}longid{\isachardoublequote}} \\
546 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}logic\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ \ any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ {\isasymdots}\ any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}{\isachardoublequote}} \\
547 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|%| \isa{pttrns} \verb|.| \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\
548 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isasymlambda}} \isa{pttrns} \verb|.| \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\
549 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|TYPE| \verb|(| \isa{type} \verb|)| \\\\
551 \indexdef{inner}{syntax}{idt}\hypertarget{syntax.inner.idt}{\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}}} & = & \verb|(| \isa{idt} \verb|)|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \\
552 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{id} \verb|::| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
553 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|_| \verb|::| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\\\
555 \indexdef{inner}{syntax}{idts}\hypertarget{syntax.inner.idts}{\hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}} & = & \isa{{\isachardoublequote}idt\ \ {\isacharbar}\ \ idt\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}\ idts{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\\\
557 \indexdef{inner}{syntax}{pttrn}\hypertarget{syntax.inner.pttrn}{\hyperlink{syntax.inner.pttrn}{\mbox{\isa{pttrn}}}} & = & \isa{idt} \\\\
559 \indexdef{inner}{syntax}{pttrns}\hypertarget{syntax.inner.pttrns}{\hyperlink{syntax.inner.pttrns}{\mbox{\isa{pttrns}}}} & = & \isa{{\isachardoublequote}pttrn\ \ {\isacharbar}\ \ pttrn\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}\ pttrns{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\\\
561 \indexdef{inner}{syntax}{type}\hypertarget{syntax.inner.type}{\hyperlink{syntax.inner.type}{\mbox{\isa{type}}}} & = & \verb|(| \isa{type} \verb|)| \\
562 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}tid\ \ {\isacharbar}\ \ tvar\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \\
563 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}tid{\isachardoublequote}} \verb|::| \isa{{\isachardoublequote}sort\ \ {\isacharbar}\ \ tvar\ \ {\isachardoublequote}}\verb|::| \isa{{\isachardoublequote}sort\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \verb|::| \isa{{\isachardoublequote}sort{\isachardoublequote}} \\
564 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|(| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|)| \isa{id} \\
565 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}longid\ \ {\isacharbar}\ \ type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ longid{\isachardoublequote}} \\
566 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|(| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|)| \isa{longid} \\
567 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|=>| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
568 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymRightarrow}{\isachardoublequote}} \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
569 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|]| \verb|=>| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
570 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|]| \isa{{\isachardoublequote}{\isasymRightarrow}{\isachardoublequote}} \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\\\
572 \indexdef{inner}{syntax}{sort}\hypertarget{syntax.inner.sort}{\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}}} & = & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|{}| \\
573 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|{| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|}| \\
577 \medskip Here literal terminals are printed \verb|verbatim|;
578 see also \secref{sec:inner-lex} for further token categories of the
579 inner syntax. The meaning of the nonterminals defined by the above
580 grammar is as follows:
584 \item \indexref{inner}{syntax}{any}\hyperlink{syntax.inner.any}{\mbox{\isa{any}}} denotes any term.
586 \item \indexref{inner}{syntax}{prop}\hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}} denotes meta-level propositions,
587 which are terms of type \isa{prop}. The syntax of such formulae of
588 the meta-logic is carefully distinguished from usual conventions for
589 object-logics. In particular, plain \isa{{\isachardoublequote}{\isasymlambda}{\isachardoublequote}}-term notation is
590 \emph{not} recognized as \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}.
592 \item \indexref{inner}{syntax}{aprop}\hyperlink{syntax.inner.aprop}{\mbox{\isa{aprop}}} denotes atomic propositions, which
593 are embedded into regular \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}} by means of an
594 explicit \verb|PROP| token.
596 Terms of type \isa{prop} with non-constant head, e.g.\ a plain
597 variable, are printed in this form. Constants that yield type \isa{prop} are expected to provide their own concrete syntax; otherwise
598 the printed version will appear like \hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}} and
599 cannot be parsed again as \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}.
601 \item \indexref{inner}{syntax}{logic}\hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}} denotes arbitrary terms of a
602 logical type, excluding type \isa{prop}. This is the main
603 syntactic category of object-logic entities, covering plain \isa{{\isasymlambda}}-term notation (variables, abstraction, application), plus
604 anything defined by the user.
606 When specifying notation for logical entities, all logical types
607 (excluding \isa{prop}) are \emph{collapsed} to this single category
608 of \hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}}.
610 \item \indexref{inner}{syntax}{idt}\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}} denotes identifiers, possibly
611 constrained by types.
613 \item \indexref{inner}{syntax}{idts}\hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}} denotes a sequence of \indexref{inner}{syntax}{idt}\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}}. This is the most basic category for variables in
614 iterated binders, such as \isa{{\isachardoublequote}{\isasymlambda}{\isachardoublequote}} or \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}}.
616 \item \indexref{inner}{syntax}{pttrn}\hyperlink{syntax.inner.pttrn}{\mbox{\isa{pttrn}}} and \indexref{inner}{syntax}{pttrns}\hyperlink{syntax.inner.pttrns}{\mbox{\isa{pttrns}}}
617 denote patterns for abstraction, cases bindings etc. In Pure, these
618 categories start as a merely copy of \hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}} and
619 \hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}, respectively. Object-logics may add
620 additional productions for binding forms.
622 \item \indexref{inner}{syntax}{type}\hyperlink{syntax.inner.type}{\mbox{\isa{type}}} denotes types of the meta-logic.
624 \item \indexref{inner}{syntax}{sort}\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}} denotes meta-level sorts.
628 Here are some further explanations of certain syntax features.
632 \item In \hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}, note that \isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ nat\ y{\isachardoublequote}} is
633 parsed as \isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}nat\ y{\isacharparenright}{\isachardoublequote}}, treating \isa{y} like a type
634 constructor applied to \isa{nat}. To avoid this interpretation,
635 write \isa{{\isachardoublequote}{\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}\ y{\isachardoublequote}} with explicit parentheses.
637 \item Similarly, \isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ nat\ y\ {\isacharcolon}{\isacharcolon}\ nat{\isachardoublequote}} is parsed as \isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}nat\ y\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}{\isachardoublequote}}. The correct form is \isa{{\isachardoublequote}{\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}{\isachardoublequote}}, or \isa{{\isachardoublequote}{\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}\ y\ {\isacharcolon}{\isacharcolon}\ nat{\isachardoublequote}} if \isa{y} is last in the
638 sequence of identifiers.
640 \item Type constraints for terms bind very weakly. For example,
641 \isa{{\isachardoublequote}x\ {\isacharless}\ y\ {\isacharcolon}{\isacharcolon}\ nat{\isachardoublequote}} is normally parsed as \isa{{\isachardoublequote}{\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}\ {\isacharcolon}{\isacharcolon}\ nat{\isachardoublequote}}, unless \isa{{\isachardoublequote}{\isacharless}{\isachardoublequote}} has a very low priority, in which case the
642 input is likely to be ambiguous. The correct form is \isa{{\isachardoublequote}x\ {\isacharless}\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}{\isachardoublequote}}.
644 \item Constraints may be either written with two literal colons
645 ``\verb|::|'' or the double-colon symbol \verb|\<Colon>|,
646 which actually looks exactly the same in some {\LaTeX} styles.
648 \item Dummy variables (written as underscore) may occur in different
653 \item A type ``\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}'' or ``\isa{{\isachardoublequote}{\isacharunderscore}\ {\isacharcolon}{\isacharcolon}\ sort{\isachardoublequote}}'' acts like an
654 anonymous inference parameter, which is filled-in according to the
655 most general type produced by the type-checking phase.
657 \item A bound ``\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}'' refers to a vacuous abstraction, where
658 the body does not refer to the binding introduced here. As in the
659 term \isa{{\isachardoublequote}{\isasymlambda}x\ {\isacharunderscore}{\isachardot}\ x{\isachardoublequote}}, which is \isa{{\isachardoublequote}{\isasymalpha}{\isachardoublequote}}-equivalent to \isa{{\isachardoublequote}{\isasymlambda}x\ y{\isachardot}\ x{\isachardoublequote}}.
661 \item A free ``\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}'' refers to an implicit outer binding.
662 Higher definitional packages usually allow forms like \isa{{\isachardoublequote}f\ x\ {\isacharunderscore}\ {\isacharequal}\ x{\isachardoublequote}}.
664 \item A schematic ``\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}'' (within a term pattern, see
665 \secref{sec:term-decls}) refers to an anonymous variable that is
666 implicitly abstracted over its context of locally bound variables.
667 For example, this allows pattern matching of \isa{{\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ f\ x\ {\isacharequal}\ g\ x{\isacharbraceright}{\isachardoublequote}} against \isa{{\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharunderscore}{\isacharbraceright}{\isachardoublequote}}, or even \isa{{\isachardoublequote}{\isacharbraceleft}{\isacharunderscore}{\isachardot}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharunderscore}{\isacharbraceright}{\isachardoublequote}} by
668 using both bound and schematic dummies.
672 \item The three literal dots ``\verb|...|'' may be also
673 written as ellipsis symbol \verb|\<dots>|. In both cases this
674 refers to a special schematic variable, which is bound in the
675 context. This special term abbreviation works nicely with
676 calculational reasoning (\secref{sec:calculation}).
682 \isamarkupsection{Lexical matters \label{sec:inner-lex}%
686 \begin{isamarkuptext}%
687 The inner lexical syntax vaguely resembles the outer one
688 (\secref{sec:outer-lex}), but some details are different. There are
689 two main categories of inner syntax tokens:
693 \item \emph{delimiters} --- the literal tokens occurring in
694 productions of the given priority grammar (cf.\
695 \secref{sec:priority-grammar});
697 \item \emph{named tokens} --- various categories of identifiers etc.
701 Delimiters override named tokens and may thus render certain
702 identifiers inaccessible. Sometimes the logical context admits
703 alternative ways to refer to the same entity, potentially via
706 \medskip The categories for named tokens are defined once and for
707 all as follows, reusing some categories of the outer token syntax
708 (\secref{sec:outer-lex}).
711 \begin{supertabular}{rcl}
712 \indexdef{inner}{syntax}{id}\hypertarget{syntax.inner.id}{\hyperlink{syntax.inner.id}{\mbox{\isa{id}}}} & = & \indexref{}{syntax}{ident}\hyperlink{syntax.ident}{\mbox{\isa{ident}}} \\
713 \indexdef{inner}{syntax}{longid}\hypertarget{syntax.inner.longid}{\hyperlink{syntax.inner.longid}{\mbox{\isa{longid}}}} & = & \indexref{}{syntax}{longident}\hyperlink{syntax.longident}{\mbox{\isa{longident}}} \\
714 \indexdef{inner}{syntax}{var}\hypertarget{syntax.inner.var}{\hyperlink{syntax.inner.var}{\mbox{\isa{var}}}} & = & \indexref{}{syntax}{var}\hyperlink{syntax.var}{\mbox{\isa{var}}} \\
715 \indexdef{inner}{syntax}{tid}\hypertarget{syntax.inner.tid}{\hyperlink{syntax.inner.tid}{\mbox{\isa{tid}}}} & = & \indexref{}{syntax}{typefree}\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}} \\
716 \indexdef{inner}{syntax}{tvar}\hypertarget{syntax.inner.tvar}{\hyperlink{syntax.inner.tvar}{\mbox{\isa{tvar}}}} & = & \indexref{}{syntax}{typevar}\hyperlink{syntax.typevar}{\mbox{\isa{typevar}}} \\
717 \indexdef{inner}{syntax}{num}\hypertarget{syntax.inner.num}{\hyperlink{syntax.inner.num}{\mbox{\isa{num}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
718 \indexdef{inner}{syntax}{float\_token}\hypertarget{syntax.inner.float-token}{\hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isacharunderscore}token}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\verb|.|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\verb|.|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
719 \indexdef{inner}{syntax}{xnum}\hypertarget{syntax.inner.xnum}{\hyperlink{syntax.inner.xnum}{\mbox{\isa{xnum}}}} & = & \verb|#|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|#-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
721 \indexdef{inner}{syntax}{xstr}\hypertarget{syntax.inner.xstr}{\hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}}} & = & \verb|''| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|''| \\
725 The token categories \hyperlink{syntax.inner.num}{\mbox{\isa{num}}}, \hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isacharunderscore}token}}}, \hyperlink{syntax.inner.xnum}{\mbox{\isa{xnum}}}, and \hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}} are
726 not used in Pure. Object-logics may implement numerals and string
727 constants by adding appropriate syntax declarations, together with
728 some translation functions (e.g.\ see Isabelle/HOL).
730 The derived categories \indexdef{inner}{syntax}{num\_const}\hypertarget{syntax.inner.num-const}{\hyperlink{syntax.inner.num-const}{\mbox{\isa{num{\isacharunderscore}const}}}} and
731 \indexdef{inner}{syntax}{float\_const}\hypertarget{syntax.inner.float-const}{\hyperlink{syntax.inner.float-const}{\mbox{\isa{float{\isacharunderscore}const}}}} provide robust access to \hyperlink{syntax.inner.num}{\mbox{\isa{num}}}, and \hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isacharunderscore}token}}}, respectively: the
732 syntax tree holds a syntactic constant instead of a free variable.%
736 \isamarkupsection{Syntax and translations \label{sec:syn-trans}%
740 \begin{isamarkuptext}%
741 \begin{matharray}{rcl}
742 \indexdef{}{command}{nonterminals}\hypertarget{command.nonterminals}{\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
743 \indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
744 \indexdef{}{command}{no\_syntax}\hypertarget{command.no-syntax}{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
745 \indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
746 \indexdef{}{command}{no\_translations}\hypertarget{command.no-translations}{\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
750 'nonterminals' (name +)
752 ('syntax' | 'no\_syntax') mode? (constdecl +)
754 ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
757 mode: ('(' ( name | 'output' | name 'output' ) ')')
759 transpat: ('(' nameref ')')? string
765 \item \hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}~\isa{c} declares a type
766 constructor \isa{c} (without arguments) to act as purely syntactic
767 type: a nonterminal symbol of the inner syntax.
769 \item \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}} is similar to
770 \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{decls}, except that the actual logical
771 signature extension is omitted. Thus the context free grammar of
772 Isabelle's inner syntax may be augmented in arbitrary ways,
773 independently of the logic. The \isa{mode} argument refers to the
774 print mode that the grammar rules belong; unless the \indexref{}{keyword}{output}\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}} indicator is given, all productions are added both to the
775 input and output grammar.
777 \item \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}} removes grammar
778 declarations (and translations) resulting from \isa{decls}, which
779 are interpreted in the same manner as for \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} above.
781 \item \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules} specifies syntactic
782 translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isachardoublequote}{\isasymrightleftharpoons}{\isachardoublequote}}),
783 parse rules (\isa{{\isachardoublequote}{\isasymrightharpoonup}{\isachardoublequote}}), or print rules (\isa{{\isachardoublequote}{\isasymleftharpoondown}{\isachardoublequote}}).
784 Translation patterns may be prefixed by the syntactic category to be
785 used for parsing; the default is \isa{logic}.
787 \item \hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}~\isa{rules} removes syntactic
788 translation rules, which are interpreted in the same manner as for
789 \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} above.
795 \isamarkupsection{Syntax translation functions \label{sec:tr-funs}%
799 \begin{isamarkuptext}%
800 \begin{matharray}{rcl}
801 \indexdef{}{command}{parse\_ast\_translation}\hypertarget{command.parse-ast-translation}{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
802 \indexdef{}{command}{parse\_translation}\hypertarget{command.parse-translation}{\hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
803 \indexdef{}{command}{print\_translation}\hypertarget{command.print-translation}{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
804 \indexdef{}{command}{typed\_print\_translation}\hypertarget{command.typed-print-translation}{\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
805 \indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print-ast-translation}{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
809 ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
810 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
814 Syntax translation functions written in ML admit almost arbitrary
815 manipulations of Isabelle's inner syntax. Any of the above commands
816 have a single \railqtok{text} argument that refers to an ML
817 expression of appropriate type, which are as follows by default:
819 %FIXME proper antiquotations
821 val parse_ast_translation : (string * (ast list -> ast)) list
822 val parse_translation : (string * (term list -> term)) list
823 val print_translation : (string * (term list -> term)) list
824 val typed_print_translation :
825 (string * (bool -> typ -> term list -> term)) list
826 val print_ast_translation : (string * (ast list -> ast)) list
829 If the \isa{{\isachardoublequote}{\isacharparenleft}advanced{\isacharparenright}{\isachardoublequote}} option is given, the corresponding
830 translation functions may depend on the current theory or proof
831 context. This allows to implement advanced syntax mechanisms, as
832 translations functions may refer to specific theory declarations or
833 auxiliary proof data.
835 See also \cite{isabelle-ref} for more information on the general
836 concept of syntax transformations in Isabelle.
838 %FIXME proper antiquotations
840 val parse_ast_translation:
841 (string * (Proof.context -> ast list -> ast)) list
842 val parse_translation:
843 (string * (Proof.context -> term list -> term)) list
844 val print_translation:
845 (string * (Proof.context -> term list -> term)) list
846 val typed_print_translation:
847 (string * (Proof.context -> bool -> typ -> term list -> term)) list
848 val print_ast_translation:
849 (string * (Proof.context -> ast list -> ast)) list
854 \isamarkupsection{Inspecting the syntax%
858 \begin{isamarkuptext}%
859 \begin{matharray}{rcl}
860 \indexdef{}{command}{print\_syntax}\hypertarget{command.print-syntax}{\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
865 \item \hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}} prints the inner syntax of the
866 current context. The output can be quite large; the most important
867 sections are explained below.
871 \item \isa{{\isachardoublequote}lexicon{\isachardoublequote}} lists the delimiters of the inner token
872 language; see \secref{sec:inner-lex}.
874 \item \isa{{\isachardoublequote}prods{\isachardoublequote}} lists the productions of the underlying
875 priority grammar; see \secref{sec:priority-grammar}.
877 The nonterminal \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup p\isactrlsup {\isacharparenright}{\isachardoublequote}} is rendered in plain text as \isa{{\isachardoublequote}A{\isacharbrackleft}p{\isacharbrackright}{\isachardoublequote}}; delimiters are quoted. Many productions have an extra
878 \isa{{\isachardoublequote}{\isasymdots}\ {\isacharequal}{\isachargreater}\ name{\isachardoublequote}}. These names later become the heads of parse
879 trees; they also guide the pretty printer.
881 Productions without such parse tree names are called \emph{copy
882 productions}. Their right-hand side must have exactly one
883 nonterminal symbol (or named token). The parser does not create a
884 new parse tree node for copy productions, but simply returns the
885 parse tree of the right-hand symbol.
887 If the right-hand side of a copy production consists of a single
888 nonterminal without any delimiters, then it is called a \emph{chain
889 production}. Chain productions act as abbreviations: conceptually,
890 they are removed from the grammar by adding new productions.
891 Priority information attached to chain productions is ignored; only
892 the dummy value \isa{{\isachardoublequote}{\isacharminus}{\isadigit{1}}{\isachardoublequote}} is displayed.
894 \item \isa{{\isachardoublequote}print\ modes{\isachardoublequote}} lists the alternative print modes
895 provided by this grammar; see \secref{sec:print-modes}.
897 \item \isa{{\isachardoublequote}parse{\isacharunderscore}rules{\isachardoublequote}} and \isa{{\isachardoublequote}print{\isacharunderscore}rules{\isachardoublequote}} relate to
898 syntax translations (macros); see \secref{sec:syn-trans}.
900 \item \isa{{\isachardoublequote}parse{\isacharunderscore}ast{\isacharunderscore}translation{\isachardoublequote}} and \isa{{\isachardoublequote}print{\isacharunderscore}ast{\isacharunderscore}translation{\isachardoublequote}} list sets of constants that invoke
901 translation functions for abstract syntax trees, which are only
902 required in very special situations; see \secref{sec:tr-funs}.
904 \item \isa{{\isachardoublequote}parse{\isacharunderscore}translation{\isachardoublequote}} and \isa{{\isachardoublequote}print{\isacharunderscore}translation{\isachardoublequote}}
905 list the sets of constants that invoke regular translation
906 functions; see \secref{sec:tr-funs}.
919 \isacommand{end}\isamarkupfalse%
931 %%% TeX-master: "root"