doc-src/IsarRef/Thy/document/Inner_Syntax.tex
author wenzelm
Fri Oct 29 11:49:56 2010 +0200 (2010-10-29)
changeset 40255 9ffbc25e1606
parent 39279 878d86983dc1
child 40406 313a24b66a8d
permissions -rw-r--r--
eliminated obsolete \_ escapes in rail environments;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Inner{\isacharunderscore}Syntax}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    11 \ Inner{\isacharunderscore}Syntax\isanewline
    12 \isakeyword{imports}\ Main\isanewline
    13 \isakeyword{begin}%
    14 \endisatagtheory
    15 {\isafoldtheory}%
    16 %
    17 \isadelimtheory
    18 %
    19 \endisadelimtheory
    20 %
    21 \isamarkupchapter{Inner syntax --- the term language \label{ch:inner-syntax}%
    22 }
    23 \isamarkuptrue%
    24 %
    25 \isamarkupsection{Printing logical entities%
    26 }
    27 \isamarkuptrue%
    28 %
    29 \isamarkupsubsection{Diagnostic commands%
    30 }
    31 \isamarkuptrue%
    32 %
    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}} \\
    42   \end{matharray}
    43 
    44   These diagnostic commands assist interactive development by printing
    45   internal logical entities in a human-readable fashion.
    46 
    47   \begin{rail}
    48     'typ' modes? type
    49     ;
    50     'term' modes? term
    51     ;
    52     'prop' modes? prop
    53     ;
    54     'thm' modes? thmrefs
    55     ;
    56     ( 'prf' | 'full_prf' ) modes? thmrefs?
    57     ;
    58     'pr' modes? nat?
    59     ;
    60 
    61     modes: '(' (name + ) ')'
    62     ;
    63   \end{rail}
    64 
    65   \begin{description}
    66 
    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.
    69 
    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.
    75 
    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.
    81 
    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).
    87 
    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
    91   there.
    92 
    93   \item \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isachardoublequote}} prints the current proof state
    94   (if present), including current facts and goals.  The optional limit
    95   arguments affect the number of goals to be displayed, which is
    96   initially 10.  Omitting limit value leaves the current setting
    97   unchanged.
    98 
    99   \end{description}
   100 
   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
   107   \cite{isabelle-sys}.
   108 
   109   Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
   110   systematic way to include formal items into the printed text
   111   document.%
   112 \end{isamarkuptext}%
   113 \isamarkuptrue%
   114 %
   115 \isamarkupsubsection{Details of printed content%
   116 }
   117 \isamarkuptrue%
   118 %
   119 \begin{isamarkuptext}%
   120 \begin{mldecls} 
   121     \indexdef{}{ML}{show\_types}\verb|show_types: bool Config.T| & default \verb|false| \\
   122     \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\
   123     \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & 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 Config.T| & default \verb|false| \\
   128     \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Config.T| & default \verb|true| \\
   129     \indexdef{}{ML}{Goal\_Display.goals\_limit}\verb|Goal_Display.goals_limit: int Config.T| & default \verb|10| \\
   130     \indexdef{}{ML}{Goal\_Display.show\_main\_goal}\verb|Goal_Display.show_main_goal: bool Config.T| & default \verb|false| \\
   131     \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool Config.T| & default \verb|false| \\
   132     \indexdef{}{ML}{show\_tags}\verb|show_tags: bool Config.T| & default \verb|false| \\
   133     \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Config.T| & default \verb|true| \\
   134   \end{mldecls}
   135 
   136   These global ML variables control the detail of information that is
   137   displayed for types, terms, theorems, goals etc.
   138 
   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}}}}.
   143 
   144   Batch-mode logic sessions may be configured by putting appropriate
   145   ML text directly into the \verb|ROOT.ML| file.
   146 
   147   \begin{description}
   148 
   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
   153   well.
   154 
   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.
   158 
   159   \item \verb|show_consts| controls printing of types of constants when
   160   displaying a goal state.
   161 
   162   Note that the output can be enormous, because polymorphic constants
   163   often occur at several different type instances.
   164 
   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.
   169 
   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.
   176 
   177   \item \verb|eta_contract| controls \isa{{\isachardoublequote}{\isasymeta}{\isachardoublequote}}-contracted printing of
   178   terms.
   179 
   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}}.
   184 
   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}.
   187 
   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.
   192 
   193   \item \verb|Goal_Display.goals_limit| controls the maximum number of
   194   subgoals to be shown in goal output.
   195 
   196   \item \verb|Goal_Display.show_main_goal| controls whether the main
   197   result to be proven should be displayed.  This information might be
   198   relevant for schematic goals, to inspect the current claim that has
   199   been synthesized so far.
   200 
   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.
   205 
   206   By setting \verb|show_hyps| to \verb|true|, output of \emph{all}
   207   hypotheses can be enforced, which is occasionally useful for
   208   diagnostic purposes.
   209 
   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}}}.
   213 
   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.
   217 
   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).
   223 
   224   \end{description}%
   225 \end{isamarkuptext}%
   226 \isamarkuptrue%
   227 %
   228 \isamarkupsubsection{Printing limits%
   229 }
   230 \isamarkuptrue%
   231 %
   232 \begin{isamarkuptext}%
   233 \begin{mldecls}
   234     \indexdef{}{ML}{Pretty.margin\_default}\verb|Pretty.margin_default: int Unsynchronized.ref| \\
   235     \indexdef{}{ML}{print\_depth}\verb|print_depth: int -> unit| \\
   236   \end{mldecls}
   237 
   238   These ML functions set limits for pretty printed text.
   239 
   240   \begin{description}
   241 
   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
   247   Isabelle/Scala.
   248 
   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.
   253 
   254   \end{description}%
   255 \end{isamarkuptext}%
   256 \isamarkuptrue%
   257 %
   258 \isamarkupsection{Mixfix annotations%
   259 }
   260 \isamarkuptrue%
   261 %
   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
   266   annotations.
   267 
   268   \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
   269   \begin{rail}
   270     infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')'
   271     ;
   272     mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
   273     ;
   274     structmixfix: mixfix | '(' 'structure' ')'
   275     ;
   276 
   277     prios: '[' (nat + ',') ']'
   278     ;
   279   \end{rail}
   280 
   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.
   290 
   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
   295   underscores.
   296 
   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.
   303 
   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.
   311 
   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
   315   entities.
   316 
   317   \begin{description}
   318 
   319   \item \isa{{\isachardoublequote}d{\isachardoublequote}} is a delimiter, namely a non-empty sequence of
   320   characters other than the following special characters:
   321 
   322   \smallskip
   323   \begin{tabular}{ll}
   324     \verb|'| & single quote \\
   325     \verb|_| & underscore \\
   326     \isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}} & index symbol \\
   327     \verb|(| & open parenthesis \\
   328     \verb|)| & close parenthesis \\
   329     \verb|/| & slash \\
   330   \end{tabular}
   331   \medskip
   332 
   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.
   336 
   337   A single quote followed by a blank separates delimiters, without
   338   affecting printing, but input tokens may have additional white space
   339   here.
   340 
   341   \item \verb|_| is an argument position, which stands for a
   342   certain syntactic category in the underlying grammar.
   343 
   344   \item \isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}} is an indexed argument position; this is the place
   345   where implicit structure arguments can be attached.
   346 
   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.
   349 
   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.
   355 
   356   \item \verb|)| closes a pretty printing block.
   357 
   358   \item \verb|//| forces a line break.
   359 
   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.
   363 
   364   \end{description}
   365 
   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.
   370 
   371   The general idea of pretty printing with blocks and breaks is also
   372   described in \cite{paulson-ml2}.%
   373 \end{isamarkuptext}%
   374 \isamarkuptrue%
   375 %
   376 \isamarkupsection{Explicit notation%
   377 }
   378 \isamarkuptrue%
   379 %
   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}} \\
   387   \end{matharray}
   388 
   389   \begin{rail}
   390     ('type_notation' | 'no_type_notation') target? mode? \\ (nameref mixfix + 'and')
   391     ;
   392     ('notation' | 'no_notation') target? mode? \\ (nameref structmixfix + 'and')
   393     ;
   394     'write' mode? (nameref structmixfix + 'and')
   395     ;
   396   \end{rail}
   397 
   398   \begin{description}
   399 
   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.
   403   
   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
   405   the present context.
   406 
   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.
   410   
   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
   413   context.
   414 
   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.
   417 
   418   \end{description}
   419 
   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.%
   423 \end{isamarkuptext}%
   424 \isamarkuptrue%
   425 %
   426 \isamarkupsection{The Pure syntax \label{sec:pure-syntax}%
   427 }
   428 \isamarkuptrue%
   429 %
   430 \isamarkupsubsection{Priority grammars \label{sec:priority-grammar}%
   431 }
   432 \isamarkuptrue%
   433 %
   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.
   443 
   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.
   450 
   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}}.
   455 
   456   \medskip The following grammar for arithmetic expressions
   457   demonstrates how binding power and associativity of operators can be
   458   enforced by priorities.
   459 
   460   \begin{center}
   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}} \\
   467   \end{tabular}
   468   \end{center}
   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.
   472 
   473   \medskip For clarity, grammars obey these conventions:
   474   \begin{itemize}
   475 
   476   \item All priorities must lie between 0 and 1000.
   477 
   478   \item Priority 0 on the right-hand side and priority 1000 on the
   479   left-hand side may be omitted.
   480 
   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.
   483 
   484   \item Alternatives are separated by \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}.
   485 
   486   \item Repetition is indicated by dots \isa{{\isachardoublequote}{\isacharparenleft}{\isasymdots}{\isacharparenright}{\isachardoublequote}} in an informal
   487   but obvious way.
   488 
   489   \end{itemize}
   490 
   491   Using these conventions, the example grammar specification above
   492   takes the form:
   493   \begin{center}
   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}} \\
   500   \end{tabular}
   501   \end{center}%
   502 \end{isamarkuptext}%
   503 \isamarkuptrue%
   504 %
   505 \isamarkupsubsection{The Pure grammar%
   506 }
   507 \isamarkuptrue%
   508 %
   509 \begin{isamarkuptext}%
   510 The priority grammar of the \isa{{\isachardoublequote}Pure{\isachardoublequote}} theory is defined as follows:
   511 
   512   %FIXME syntax for "index" (?)
   513   %FIXME "op" versions of ==> etc. (?)
   514 
   515   \begin{center}
   516   \begin{supertabular}{rclr}
   517 
   518   \indexdef{inner}{syntax}{any}\hypertarget{syntax.inner.any}{\hyperlink{syntax.inner.any}{\mbox{\isa{any}}}} & = & \isa{{\isachardoublequote}prop\ \ {\isacharbar}\ \ logic{\isachardoublequote}} \\\\
   519 
   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} \\\\
   536 
   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}} \\\\
   541 
   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|)| \\\\
   550 
   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}} \\\\
   554 
   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}} \\\\
   556 
   557   \indexdef{inner}{syntax}{pttrn}\hypertarget{syntax.inner.pttrn}{\hyperlink{syntax.inner.pttrn}{\mbox{\isa{pttrn}}}} & = & \isa{idt} \\\\
   558 
   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}} \\\\
   560 
   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}} \\\\
   571 
   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|}| \\
   574   \end{supertabular}
   575   \end{center}
   576 
   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:
   581 
   582   \begin{description}
   583 
   584   \item \indexref{inner}{syntax}{any}\hyperlink{syntax.inner.any}{\mbox{\isa{any}}} denotes any term.
   585 
   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}}}.
   591 
   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.
   595 
   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}}}.
   600 
   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.
   605 
   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}}}.
   609 
   610   \item \indexref{inner}{syntax}{idt}\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}} denotes identifiers, possibly
   611   constrained by types.
   612 
   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}}.
   615 
   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.
   621 
   622   \item \indexref{inner}{syntax}{type}\hyperlink{syntax.inner.type}{\mbox{\isa{type}}} denotes types of the meta-logic.
   623 
   624   \item \indexref{inner}{syntax}{sort}\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}} denotes meta-level sorts.
   625 
   626   \end{description}
   627 
   628   Here are some further explanations of certain syntax features.
   629 
   630   \begin{itemize}
   631 
   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.
   636 
   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.
   639 
   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}}.
   643 
   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.
   647 
   648   \item Dummy variables (written as underscore) may occur in different
   649   roles.
   650 
   651   \begin{description}
   652 
   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.
   656 
   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}}.
   660 
   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}}.
   663 
   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.
   669 
   670   \end{description}
   671 
   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}).
   677 
   678   \end{itemize}%
   679 \end{isamarkuptext}%
   680 \isamarkuptrue%
   681 %
   682 \isamarkupsection{Lexical matters \label{sec:inner-lex}%
   683 }
   684 \isamarkuptrue%
   685 %
   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:
   690 
   691   \begin{enumerate}
   692 
   693   \item \emph{delimiters} --- the literal tokens occurring in
   694   productions of the given priority grammar (cf.\
   695   \secref{sec:priority-grammar});
   696 
   697   \item \emph{named tokens} --- various categories of identifiers etc.
   698 
   699   \end{enumerate}
   700 
   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
   704   qualified names.
   705 
   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}).
   709 
   710   \begin{center}
   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}}} \\
   720 
   721     \indexdef{inner}{syntax}{xstr}\hypertarget{syntax.inner.xstr}{\hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}}} & = & \verb|''| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|''| \\
   722   \end{supertabular}
   723   \end{center}
   724 
   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).
   729 
   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.%
   733 \end{isamarkuptext}%
   734 \isamarkuptrue%
   735 %
   736 \isamarkupsection{Syntax and translations \label{sec:syn-trans}%
   737 }
   738 \isamarkuptrue%
   739 %
   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}} \\
   747   \end{matharray}
   748 
   749   \begin{rail}
   750     'nonterminals' (name +)
   751     ;
   752     ('syntax' | 'no_syntax') mode? (constdecl +)
   753     ;
   754     ('translations' | 'no_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
   755     ;
   756 
   757     mode: ('(' ( name | 'output' | name 'output' ) ')')
   758     ;
   759     transpat: ('(' nameref ')')? string
   760     ;
   761   \end{rail}
   762 
   763   \begin{description}
   764   
   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.
   768 
   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.
   776   
   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.
   780   
   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}.
   786   
   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.
   790 
   791   \end{description}%
   792 \end{isamarkuptext}%
   793 \isamarkuptrue%
   794 %
   795 \isamarkupsection{Syntax translation functions \label{sec:tr-funs}%
   796 }
   797 \isamarkuptrue%
   798 %
   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}} \\
   806   \end{matharray}
   807 
   808   \begin{rail}
   809   ( 'parse_ast_translation' | 'parse_translation' | 'print_translation' |
   810     'typed_print_translation' | 'print_ast_translation' ) ('(advanced)')? text
   811   ;
   812   \end{rail}
   813 
   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:
   818 
   819 %FIXME proper antiquotations
   820 \begin{ttbox}
   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
   827 \end{ttbox}
   828 
   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.
   834 
   835   See also \cite{isabelle-ref} for more information on the general
   836   concept of syntax transformations in Isabelle.
   837 
   838 %FIXME proper antiquotations
   839 \begin{ttbox}
   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
   850 \end{ttbox}%
   851 \end{isamarkuptext}%
   852 \isamarkuptrue%
   853 %
   854 \isamarkupsection{Inspecting the syntax%
   855 }
   856 \isamarkuptrue%
   857 %
   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}} \\
   861   \end{matharray}
   862 
   863   \begin{description}
   864 
   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.
   868 
   869   \begin{description}
   870 
   871   \item \isa{{\isachardoublequote}lexicon{\isachardoublequote}} lists the delimiters of the inner token
   872   language; see \secref{sec:inner-lex}.
   873 
   874   \item \isa{{\isachardoublequote}prods{\isachardoublequote}} lists the productions of the underlying
   875   priority grammar; see \secref{sec:priority-grammar}.
   876 
   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.
   880 
   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.
   886 
   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.
   893 
   894   \item \isa{{\isachardoublequote}print\ modes{\isachardoublequote}} lists the alternative print modes
   895   provided by this grammar; see \secref{sec:print-modes}.
   896 
   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}.
   899 
   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}.
   903 
   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}.
   907 
   908   \end{description}
   909   
   910   \end{description}%
   911 \end{isamarkuptext}%
   912 \isamarkuptrue%
   913 %
   914 \isadelimtheory
   915 %
   916 \endisadelimtheory
   917 %
   918 \isatagtheory
   919 \isacommand{end}\isamarkupfalse%
   920 %
   921 \endisatagtheory
   922 {\isafoldtheory}%
   923 %
   924 \isadelimtheory
   925 %
   926 \endisadelimtheory
   927 \isanewline
   928 \end{isabellebody}%
   929 %%% Local Variables:
   930 %%% mode: latex
   931 %%% TeX-master: "root"
   932 %%% End: