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;
wenzelm@28762
     1
%
wenzelm@28762
     2
\begin{isabellebody}%
wenzelm@28762
     3
\def\isabellecontext{Inner{\isacharunderscore}Syntax}%
wenzelm@28762
     4
%
wenzelm@28762
     5
\isadelimtheory
wenzelm@28762
     6
%
wenzelm@28762
     7
\endisadelimtheory
wenzelm@28762
     8
%
wenzelm@28762
     9
\isatagtheory
wenzelm@28762
    10
\isacommand{theory}\isamarkupfalse%
wenzelm@28762
    11
\ Inner{\isacharunderscore}Syntax\isanewline
wenzelm@28762
    12
\isakeyword{imports}\ Main\isanewline
wenzelm@28762
    13
\isakeyword{begin}%
wenzelm@28762
    14
\endisatagtheory
wenzelm@28762
    15
{\isafoldtheory}%
wenzelm@28762
    16
%
wenzelm@28762
    17
\isadelimtheory
wenzelm@28762
    18
%
wenzelm@28762
    19
\endisadelimtheory
wenzelm@28762
    20
%
wenzelm@28762
    21
\isamarkupchapter{Inner syntax --- the term language \label{ch:inner-syntax}%
wenzelm@28762
    22
}
wenzelm@28762
    23
\isamarkuptrue%
wenzelm@28762
    24
%
wenzelm@28762
    25
\isamarkupsection{Printing logical entities%
wenzelm@28762
    26
}
wenzelm@28762
    27
\isamarkuptrue%
wenzelm@28762
    28
%
wenzelm@28762
    29
\isamarkupsubsection{Diagnostic commands%
wenzelm@28762
    30
}
wenzelm@28762
    31
\isamarkuptrue%
wenzelm@28762
    32
%
wenzelm@28762
    33
\begin{isamarkuptext}%
wenzelm@28762
    34
\begin{matharray}{rcl}
wenzelm@28762
    35
    \indexdef{}{command}{typ}\hypertarget{command.typ}{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
wenzelm@28762
    36
    \indexdef{}{command}{term}\hypertarget{command.term}{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
wenzelm@28762
    37
    \indexdef{}{command}{prop}\hypertarget{command.prop}{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
wenzelm@28762
    38
    \indexdef{}{command}{thm}\hypertarget{command.thm}{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
wenzelm@28762
    39
    \indexdef{}{command}{prf}\hypertarget{command.prf}{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
wenzelm@28762
    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}} \\
wenzelm@28762
    41
    \indexdef{}{command}{pr}\hypertarget{command.pr}{\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
wenzelm@28762
    42
  \end{matharray}
wenzelm@28762
    43
wenzelm@28762
    44
  These diagnostic commands assist interactive development by printing
wenzelm@28762
    45
  internal logical entities in a human-readable fashion.
wenzelm@28762
    46
wenzelm@28762
    47
  \begin{rail}
wenzelm@28762
    48
    'typ' modes? type
wenzelm@28762
    49
    ;
wenzelm@28762
    50
    'term' modes? term
wenzelm@28762
    51
    ;
wenzelm@28762
    52
    'prop' modes? prop
wenzelm@28762
    53
    ;
wenzelm@28762
    54
    'thm' modes? thmrefs
wenzelm@28762
    55
    ;
wenzelm@40255
    56
    ( 'prf' | 'full_prf' ) modes? thmrefs?
wenzelm@28762
    57
    ;
wenzelm@39165
    58
    'pr' modes? nat?
wenzelm@28762
    59
    ;
wenzelm@28762
    60
wenzelm@28762
    61
    modes: '(' (name + ) ')'
wenzelm@28762
    62
    ;
wenzelm@28762
    63
  \end{rail}
wenzelm@28762
    64
wenzelm@28762
    65
  \begin{description}
wenzelm@28762
    66
wenzelm@28762
    67
  \item \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isasymtau}} reads and prints types of the
wenzelm@28762
    68
  meta-logic according to the current theory or proof context.
wenzelm@28762
    69
wenzelm@28762
    70
  \item \hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}~\isa{t} and \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isasymphi}}
wenzelm@28762
    71
  read, type-check and print terms or propositions according to the
wenzelm@28762
    72
  current theory or proof context; the inferred type of \isa{t} is
wenzelm@28762
    73
  output as well.  Note that these commands are also useful in
wenzelm@28762
    74
  inspecting the current environment of term abbreviations.
wenzelm@28762
    75
wenzelm@28762
    76
  \item \hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} retrieves
wenzelm@28762
    77
  theorems from the current theory or proof context.  Note that any
wenzelm@28762
    78
  attributes included in the theorem specifications are applied to a
wenzelm@28762
    79
  temporary context derived from the current theory or proof; the
wenzelm@28762
    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.
wenzelm@28762
    81
wenzelm@28762
    82
  \item \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}} displays the (compact) proof term of the
wenzelm@28762
    83
  current proof state (if present), or of the given theorems. Note
wenzelm@28762
    84
  that this requires proof terms to be switched on for the current
wenzelm@28762
    85
  object logic (see the ``Proof terms'' section of the Isabelle
wenzelm@28762
    86
  reference manual for information on how to do this).
wenzelm@28762
    87
wenzelm@28762
    88
  \item \hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}} is like \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}, but displays
wenzelm@28762
    89
  the full proof term, i.e.\ also displays information omitted in the
wenzelm@28762
    90
  compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders
wenzelm@28762
    91
  there.
wenzelm@28762
    92
wenzelm@39165
    93
  \item \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isachardoublequote}} prints the current proof state
wenzelm@39165
    94
  (if present), including current facts and goals.  The optional limit
wenzelm@39165
    95
  arguments affect the number of goals to be displayed, which is
wenzelm@39165
    96
  initially 10.  Omitting limit value leaves the current setting
wenzelm@39165
    97
  unchanged.
wenzelm@28762
    98
wenzelm@28762
    99
  \end{description}
wenzelm@28762
   100
wenzelm@28762
   101
  All of the diagnostic commands above admit a list of \isa{modes}
wenzelm@28762
   102
  to be specified, which is appended to the current print mode (see
wenzelm@28762
   103
  also \cite{isabelle-ref}).  Thus the output behavior may be modified
wenzelm@28762
   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
wenzelm@28762
   105
  with mathematical symbols and special characters represented in
wenzelm@28762
   106
  {\LaTeX} source, according to the Isabelle style
wenzelm@28762
   107
  \cite{isabelle-sys}.
wenzelm@28762
   108
wenzelm@28762
   109
  Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
wenzelm@28762
   110
  systematic way to include formal items into the printed text
wenzelm@28762
   111
  document.%
wenzelm@28762
   112
\end{isamarkuptext}%
wenzelm@28762
   113
\isamarkuptrue%
wenzelm@28762
   114
%
wenzelm@28762
   115
\isamarkupsubsection{Details of printed content%
wenzelm@28762
   116
}
wenzelm@28762
   117
\isamarkuptrue%
wenzelm@28762
   118
%
wenzelm@28762
   119
\begin{isamarkuptext}%
wenzelm@28762
   120
\begin{mldecls} 
wenzelm@39134
   121
    \indexdef{}{ML}{show\_types}\verb|show_types: bool Config.T| & default \verb|false| \\
wenzelm@39134
   122
    \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\
wenzelm@39050
   123
    \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\
wenzelm@32836
   124
    \indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\
wenzelm@32836
   125
    \indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\
wenzelm@32836
   126
    \indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\
wenzelm@39137
   127
    \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Config.T| & default \verb|false| \\
wenzelm@39130
   128
    \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Config.T| & default \verb|true| \\
wenzelm@39130
   129
    \indexdef{}{ML}{Goal\_Display.goals\_limit}\verb|Goal_Display.goals_limit: int Config.T| & default \verb|10| \\
wenzelm@39130
   130
    \indexdef{}{ML}{Goal\_Display.show\_main\_goal}\verb|Goal_Display.show_main_goal: bool Config.T| & default \verb|false| \\
wenzelm@39279
   131
    \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool Config.T| & default \verb|false| \\
wenzelm@39279
   132
    \indexdef{}{ML}{show\_tags}\verb|show_tags: bool Config.T| & default \verb|false| \\
wenzelm@38980
   133
    \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Config.T| & default \verb|true| \\
wenzelm@28762
   134
  \end{mldecls}
wenzelm@28762
   135
wenzelm@28762
   136
  These global ML variables control the detail of information that is
wenzelm@28762
   137
  displayed for types, terms, theorems, goals etc.
wenzelm@28762
   138
wenzelm@28762
   139
  In interactive sessions, the user interface usually manages these
wenzelm@28762
   140
  global parameters of the Isabelle process, even with some concept of
wenzelm@28762
   141
  persistence.  Nonetheless it is occasionally useful to manipulate ML
wenzelm@28762
   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}}}}.
wenzelm@28762
   143
wenzelm@28762
   144
  Batch-mode logic sessions may be configured by putting appropriate
wenzelm@28762
   145
  ML text directly into the \verb|ROOT.ML| file.
wenzelm@28762
   146
wenzelm@28762
   147
  \begin{description}
wenzelm@28762
   148
wenzelm@28762
   149
  \item \verb|show_types| and \verb|show_sorts| control printing of type
wenzelm@28762
   150
  constraints for term variables, and sort constraints for type
wenzelm@28762
   151
  variables.  By default, neither of these are shown in output.  If
wenzelm@28762
   152
  \verb|show_sorts| is set to \verb|true|, types are always shown as
wenzelm@28762
   153
  well.
wenzelm@28762
   154
wenzelm@28762
   155
  Note that displaying types and sorts may explain why a polymorphic
wenzelm@28762
   156
  inference rule fails to resolve with some goal, or why a rewrite
wenzelm@28762
   157
  rule does not apply as expected.
wenzelm@28762
   158
wenzelm@28762
   159
  \item \verb|show_consts| controls printing of types of constants when
wenzelm@28762
   160
  displaying a goal state.
wenzelm@28762
   161
wenzelm@28762
   162
  Note that the output can be enormous, because polymorphic constants
wenzelm@28762
   163
  often occur at several different type instances.
wenzelm@28762
   164
wenzelm@28762
   165
  \item \verb|long_names|, \verb|short_names|, and \verb|unique_names|
wenzelm@28762
   166
  control the way of printing fully qualified internal names in
wenzelm@28762
   167
  external form.  See also \secref{sec:antiq} for the document
wenzelm@28762
   168
  antiquotation options of the same names.
wenzelm@28762
   169
wenzelm@28762
   170
  \item \verb|show_brackets| controls bracketing in pretty printed
wenzelm@28762
   171
  output.  If set to \verb|true|, all sub-expressions of the pretty
wenzelm@28762
   172
  printing tree will be parenthesized, even if this produces malformed
wenzelm@28762
   173
  term syntax!  This crude way of showing the internal structure of
wenzelm@28762
   174
  pretty printed entities may occasionally help to diagnose problems
wenzelm@28762
   175
  with operator priorities, for example.
wenzelm@28762
   176
wenzelm@28762
   177
  \item \verb|eta_contract| controls \isa{{\isachardoublequote}{\isasymeta}{\isachardoublequote}}-contracted printing of
wenzelm@28762
   178
  terms.
wenzelm@28762
   179
wenzelm@28762
   180
  The \isa{{\isasymeta}}-contraction law asserts \isa{{\isachardoublequote}{\isacharparenleft}{\isasymlambda}x{\isachardot}\ f\ x{\isacharparenright}\ {\isasymequiv}\ f{\isachardoublequote}},
wenzelm@28762
   181
  provided \isa{x} is not free in \isa{f}.  It asserts
wenzelm@28762
   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
wenzelm@28762
   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}}.
wenzelm@28762
   184
wenzelm@28762
   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}}
wenzelm@28762
   186
  appears simply as \isa{F}.
wenzelm@28762
   187
wenzelm@28762
   188
  Note that the distinction between a term and its \isa{{\isasymeta}}-expanded
wenzelm@28762
   189
  form occasionally matters.  While higher-order resolution and
wenzelm@28762
   190
  rewriting operate modulo \isa{{\isachardoublequote}{\isasymalpha}{\isasymbeta}{\isasymeta}{\isachardoublequote}}-conversion, some other tools
wenzelm@28762
   191
  might look at terms more discretely.
wenzelm@28762
   192
wenzelm@39130
   193
  \item \verb|Goal_Display.goals_limit| controls the maximum number of
wenzelm@39130
   194
  subgoals to be shown in goal output.
wenzelm@28762
   195
wenzelm@39130
   196
  \item \verb|Goal_Display.show_main_goal| controls whether the main
wenzelm@39130
   197
  result to be proven should be displayed.  This information might be
wenzelm@39130
   198
  relevant for schematic goals, to inspect the current claim that has
wenzelm@39130
   199
  been synthesized so far.
wenzelm@28762
   200
wenzelm@28762
   201
  \item \verb|show_hyps| controls printing of implicit hypotheses of
wenzelm@28762
   202
  local facts.  Normally, only those hypotheses are displayed that are
wenzelm@28762
   203
  \emph{not} covered by the assumptions of the current context: this
wenzelm@28762
   204
  situation indicates a fault in some tool being used.
wenzelm@28762
   205
wenzelm@28762
   206
  By setting \verb|show_hyps| to \verb|true|, output of \emph{all}
wenzelm@28762
   207
  hypotheses can be enforced, which is occasionally useful for
wenzelm@28762
   208
  diagnostic purposes.
wenzelm@28762
   209
wenzelm@28762
   210
  \item \verb|show_tags| controls printing of extra annotations within
wenzelm@28762
   211
  theorems, such as internal position information, or the case names
wenzelm@28762
   212
  being attached by the attribute \hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}}.
wenzelm@28762
   213
wenzelm@28762
   214
  Note that the \hyperlink{attribute.tagged}{\mbox{\isa{tagged}}} and \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}
wenzelm@28762
   215
  attributes provide low-level access to the collection of tags
wenzelm@28762
   216
  associated with a theorem.
wenzelm@28762
   217
wenzelm@28762
   218
  \item \verb|show_question_marks| controls printing of question marks
wenzelm@28762
   219
  for schematic variables, such as \isa{{\isacharquery}x}.  Only the leading
wenzelm@28762
   220
  question mark is affected, the remaining text is unchanged
wenzelm@28762
   221
  (including proper markup for schematic variables that might be
wenzelm@28762
   222
  relevant for user interfaces).
wenzelm@28762
   223
wenzelm@28762
   224
  \end{description}%
wenzelm@28762
   225
\end{isamarkuptext}%
wenzelm@28762
   226
\isamarkuptrue%
wenzelm@28762
   227
%
wenzelm@28762
   228
\isamarkupsubsection{Printing limits%
wenzelm@28762
   229
}
wenzelm@28762
   230
\isamarkuptrue%
wenzelm@28762
   231
%
wenzelm@28762
   232
\begin{isamarkuptext}%
wenzelm@28762
   233
\begin{mldecls}
wenzelm@36745
   234
    \indexdef{}{ML}{Pretty.margin\_default}\verb|Pretty.margin_default: int Unsynchronized.ref| \\
wenzelm@30121
   235
    \indexdef{}{ML}{print\_depth}\verb|print_depth: int -> unit| \\
wenzelm@28762
   236
  \end{mldecls}
wenzelm@28762
   237
wenzelm@28762
   238
  These ML functions set limits for pretty printed text.
wenzelm@28762
   239
wenzelm@28762
   240
  \begin{description}
wenzelm@28762
   241
wenzelm@36745
   242
  \item \verb|Pretty.margin_default| indicates the global default for
wenzelm@36745
   243
  the right margin of the built-in pretty printer, with initial value
wenzelm@36745
   244
  76.  Note that user-interfaces typically control margins
wenzelm@36745
   245
  automatically when resizing windows, or even bypass the formatting
wenzelm@36745
   246
  engine of Isabelle/ML altogether and do it within the front end via
wenzelm@36745
   247
  Isabelle/Scala.
wenzelm@28762
   248
wenzelm@28762
   249
  \item \verb|print_depth|~\isa{n} limits the printing depth of the
wenzelm@28762
   250
  ML toplevel pretty printer; the precise effect depends on the ML
wenzelm@28762
   251
  compiler and run-time system.  Typically \isa{n} should be less
wenzelm@28762
   252
  than 10.  Bigger values such as 100--1000 are useful for debugging.
wenzelm@28762
   253
wenzelm@28762
   254
  \end{description}%
wenzelm@28762
   255
\end{isamarkuptext}%
wenzelm@28762
   256
\isamarkuptrue%
wenzelm@28762
   257
%
wenzelm@28762
   258
\isamarkupsection{Mixfix annotations%
wenzelm@28762
   259
}
wenzelm@28762
   260
\isamarkuptrue%
wenzelm@28762
   261
%
wenzelm@28762
   262
\begin{isamarkuptext}%
wenzelm@28762
   263
Mixfix annotations specify concrete \emph{inner syntax} of
wenzelm@35351
   264
  Isabelle types and terms.  Locally fixed parameters in toplevel
wenzelm@35351
   265
  theorem statements, locale specifications etc.\ also admit mixfix
wenzelm@35351
   266
  annotations.
wenzelm@28762
   267
wenzelm@28762
   268
  \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
wenzelm@28762
   269
  \begin{rail}
wenzelm@28762
   270
    infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')'
wenzelm@28762
   271
    ;
wenzelm@28762
   272
    mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
wenzelm@28762
   273
    ;
wenzelm@28762
   274
    structmixfix: mixfix | '(' 'structure' ')'
wenzelm@28762
   275
    ;
wenzelm@28762
   276
wenzelm@28762
   277
    prios: '[' (nat + ',') ']'
wenzelm@28762
   278
    ;
wenzelm@28762
   279
  \end{rail}
wenzelm@28762
   280
wenzelm@28762
   281
  Here the \railtok{string} specifications refer to the actual mixfix
wenzelm@28762
   282
  template, which may include literal text, spacing, blocks, and
wenzelm@28762
   283
  arguments (denoted by ``\isa{{\isacharunderscore}}''); the special symbol
wenzelm@28762
   284
  ``\verb|\<index>|'' (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}'') represents an index
wenzelm@28762
   285
  argument that specifies an implicit structure reference (see also
wenzelm@28762
   286
  \secref{sec:locale}).  Infix and binder declarations provide common
wenzelm@28762
   287
  abbreviations for particular mixfix declarations.  So in practice,
wenzelm@28762
   288
  mixfix templates mostly degenerate to literal text for concrete
wenzelm@28762
   289
  syntax, such as ``\verb|++|'' for an infix symbol.
wenzelm@28762
   290
wenzelm@28762
   291
  \medskip In full generality, mixfix declarations work as follows.
wenzelm@28762
   292
  Suppose a constant \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymtau}\isactrlsub n\ {\isasymRightarrow}\ {\isasymtau}{\isachardoublequote}} is
wenzelm@28762
   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
wenzelm@28762
   294
  delimiters that surround argument positions as indicated by
wenzelm@28762
   295
  underscores.
wenzelm@28762
   296
wenzelm@28762
   297
  Altogether this determines a production for a context-free priority
wenzelm@28762
   298
  grammar, where for each argument \isa{{\isachardoublequote}i{\isachardoublequote}} the syntactic category
wenzelm@28762
   299
  is determined by \isa{{\isachardoublequote}{\isasymtau}\isactrlsub i{\isachardoublequote}} (with priority \isa{{\isachardoublequote}p\isactrlsub i{\isachardoublequote}}), and
wenzelm@28762
   300
  the result category is determined from \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} (with
wenzelm@28762
   301
  priority \isa{{\isachardoublequote}p{\isachardoublequote}}).  Priority specifications are optional, with
wenzelm@28762
   302
  default 0 for arguments and 1000 for the result.
wenzelm@28762
   303
wenzelm@28762
   304
  Since \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} may be again a function type, the constant
wenzelm@28762
   305
  type scheme may have more argument positions than the mixfix
wenzelm@28762
   306
  pattern.  Printing a nested application \isa{{\isachardoublequote}c\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub m{\isachardoublequote}} for
wenzelm@28762
   307
  \isa{{\isachardoublequote}m\ {\isachargreater}\ n{\isachardoublequote}} works by attaching concrete notation only to the
wenzelm@28762
   308
  innermost part, essentially by printing \isa{{\isachardoublequote}{\isacharparenleft}c\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isacharparenright}\ {\isasymdots}\ t\isactrlsub m{\isachardoublequote}}
wenzelm@28762
   309
  instead.  If a term has fewer arguments than specified in the mixfix
wenzelm@28762
   310
  template, the concrete syntax is ignored.
wenzelm@28762
   311
wenzelm@28762
   312
  \medskip A mixfix template may also contain additional directives
wenzelm@28762
   313
  for pretty printing, notably spaces, blocks, and breaks.  The
wenzelm@28762
   314
  general template format is a sequence over any of the following
wenzelm@28762
   315
  entities.
wenzelm@28762
   316
wenzelm@28762
   317
  \begin{description}
wenzelm@28762
   318
wenzelm@28762
   319
  \item \isa{{\isachardoublequote}d{\isachardoublequote}} is a delimiter, namely a non-empty sequence of
wenzelm@28762
   320
  characters other than the following special characters:
wenzelm@28762
   321
wenzelm@28762
   322
  \smallskip
wenzelm@28762
   323
  \begin{tabular}{ll}
wenzelm@28762
   324
    \verb|'| & single quote \\
wenzelm@28762
   325
    \verb|_| & underscore \\
wenzelm@28762
   326
    \isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}} & index symbol \\
wenzelm@28762
   327
    \verb|(| & open parenthesis \\
wenzelm@28762
   328
    \verb|)| & close parenthesis \\
wenzelm@28762
   329
    \verb|/| & slash \\
wenzelm@28762
   330
  \end{tabular}
wenzelm@28762
   331
  \medskip
wenzelm@28762
   332
wenzelm@28762
   333
  \item \verb|'| escapes the special meaning of these
wenzelm@28762
   334
  meta-characters, producing a literal version of the following
wenzelm@28762
   335
  character, unless that is a blank.
wenzelm@28762
   336
wenzelm@28762
   337
  A single quote followed by a blank separates delimiters, without
wenzelm@28762
   338
  affecting printing, but input tokens may have additional white space
wenzelm@28762
   339
  here.
wenzelm@28762
   340
wenzelm@28762
   341
  \item \verb|_| is an argument position, which stands for a
wenzelm@28762
   342
  certain syntactic category in the underlying grammar.
wenzelm@28762
   343
wenzelm@28762
   344
  \item \isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}} is an indexed argument position; this is the place
wenzelm@28762
   345
  where implicit structure arguments can be attached.
wenzelm@28762
   346
wenzelm@28762
   347
  \item \isa{{\isachardoublequote}s{\isachardoublequote}} is a non-empty sequence of spaces for printing.
wenzelm@28762
   348
  This and the following specifications do not affect parsing at all.
wenzelm@28762
   349
wenzelm@28762
   350
  \item \verb|(|\isa{n} opens a pretty printing block.  The
wenzelm@28762
   351
  optional number specifies how much indentation to add when a line
wenzelm@28762
   352
  break occurs within the block.  If the parenthesis is not followed
wenzelm@28762
   353
  by digits, the indentation defaults to 0.  A block specified via
wenzelm@28762
   354
  \verb|(00| is unbreakable.
wenzelm@28762
   355
wenzelm@28762
   356
  \item \verb|)| closes a pretty printing block.
wenzelm@28762
   357
wenzelm@28762
   358
  \item \verb|//| forces a line break.
wenzelm@28762
   359
wenzelm@28762
   360
  \item \verb|/|\isa{s} allows a line break.  Here \isa{s}
wenzelm@28762
   361
  stands for the string of spaces (zero or more) right after the
wenzelm@28762
   362
  slash.  These spaces are printed if the break is \emph{not} taken.
wenzelm@28762
   363
wenzelm@28762
   364
  \end{description}
wenzelm@28762
   365
wenzelm@28762
   366
  For example, the template \verb|(_ +/ _)| specifies an infix
wenzelm@28762
   367
  operator.  There are two argument positions; the delimiter
wenzelm@28762
   368
  \verb|+| is preceded by a space and followed by a space or
wenzelm@28762
   369
  line break; the entire phrase is a pretty printing block.
wenzelm@28762
   370
wenzelm@28762
   371
  The general idea of pretty printing with blocks and breaks is also
wenzelm@28762
   372
  described in \cite{paulson-ml2}.%
wenzelm@28762
   373
\end{isamarkuptext}%
wenzelm@28762
   374
\isamarkuptrue%
wenzelm@28762
   375
%
wenzelm@35414
   376
\isamarkupsection{Explicit notation%
wenzelm@28762
   377
}
wenzelm@28762
   378
\isamarkuptrue%
wenzelm@28762
   379
%
wenzelm@28762
   380
\begin{isamarkuptext}%
wenzelm@28762
   381
\begin{matharray}{rcll}
wenzelm@35414
   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}} \\
wenzelm@35414
   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}} \\
wenzelm@28762
   384
    \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
wenzelm@28762
   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}} \\
wenzelm@36508
   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}} \\
wenzelm@28762
   387
  \end{matharray}
wenzelm@28762
   388
wenzelm@28762
   389
  \begin{rail}
wenzelm@40255
   390
    ('type_notation' | 'no_type_notation') target? mode? \\ (nameref mixfix + 'and')
wenzelm@35414
   391
    ;
wenzelm@40255
   392
    ('notation' | 'no_notation') target? mode? \\ (nameref structmixfix + 'and')
wenzelm@28762
   393
    ;
wenzelm@36508
   394
    'write' mode? (nameref structmixfix + 'and')
wenzelm@36508
   395
    ;
wenzelm@28762
   396
  \end{rail}
wenzelm@28762
   397
wenzelm@28762
   398
  \begin{description}
wenzelm@28762
   399
wenzelm@35414
   400
  \item \hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix
wenzelm@35414
   401
  syntax with an existing type constructor.  The arity of the
wenzelm@35414
   402
  constructor is retrieved from the context.
wenzelm@35414
   403
  
wenzelm@35414
   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
wenzelm@35414
   405
  the present context.
wenzelm@35414
   406
wenzelm@28762
   407
  \item \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix
wenzelm@35414
   408
  syntax with an existing constant or fixed variable.  The type
wenzelm@35414
   409
  declaration of the given entity is retrieved from the context.
wenzelm@28762
   410
  
wenzelm@28762
   411
  \item \hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}},
wenzelm@28762
   412
  but removes the specified syntax annotation from the present
wenzelm@28762
   413
  context.
wenzelm@28762
   414
wenzelm@36508
   415
  \item \hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but
wenzelm@36508
   416
  works within an Isar proof body.
wenzelm@36508
   417
wenzelm@35414
   418
  \end{description}
wenzelm@35414
   419
wenzelm@36508
   420
  Note that the more primitive commands \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} and
wenzelm@36508
   421
  \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}} (\secref{sec:syn-trans}) provide raw access
wenzelm@36508
   422
  to the syntax tables of a global theory.%
wenzelm@28762
   423
\end{isamarkuptext}%
wenzelm@28762
   424
\isamarkuptrue%
wenzelm@28762
   425
%
wenzelm@28762
   426
\isamarkupsection{The Pure syntax \label{sec:pure-syntax}%
wenzelm@28762
   427
}
wenzelm@28762
   428
\isamarkuptrue%
wenzelm@28762
   429
%
wenzelm@28762
   430
\isamarkupsubsection{Priority grammars \label{sec:priority-grammar}%
wenzelm@28762
   431
}
wenzelm@28762
   432
\isamarkuptrue%
wenzelm@28762
   433
%
wenzelm@28762
   434
\begin{isamarkuptext}%
wenzelm@28762
   435
A context-free grammar consists of a set of \emph{terminal
wenzelm@28762
   436
  symbols}, a set of \emph{nonterminal symbols} and a set of
wenzelm@28762
   437
  \emph{productions}.  Productions have the form \isa{{\isachardoublequote}A\ {\isacharequal}\ {\isasymgamma}{\isachardoublequote}},
wenzelm@28762
   438
  where \isa{A} is a nonterminal and \isa{{\isasymgamma}} is a string of
wenzelm@28762
   439
  terminals and nonterminals.  One designated nonterminal is called
wenzelm@28762
   440
  the \emph{root symbol}.  The language defined by the grammar
wenzelm@28762
   441
  consists of all strings of terminals that can be derived from the
wenzelm@28762
   442
  root symbol by applying productions as rewrite rules.
wenzelm@28762
   443
wenzelm@28762
   444
  The standard Isabelle parser for inner syntax uses a \emph{priority
wenzelm@28762
   445
  grammar}.  Each nonterminal is decorated by an integer priority:
wenzelm@28762
   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
wenzelm@28762
   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
wenzelm@28762
   448
  priority grammar can be translated into a normal context-free
wenzelm@28762
   449
  grammar by introducing new nonterminals and productions.
wenzelm@28762
   450
wenzelm@28762
   451
  \medskip Formally, a set of context free productions \isa{G}
wenzelm@28762
   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.
wenzelm@28762
   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}
wenzelm@28762
   454
  contains some production \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup q\isactrlsup {\isacharparenright}\ {\isacharequal}\ {\isasymgamma}{\isachardoublequote}} for \isa{{\isachardoublequote}p\ {\isasymle}\ q{\isachardoublequote}}.
wenzelm@28762
   455
wenzelm@28762
   456
  \medskip The following grammar for arithmetic expressions
wenzelm@28762
   457
  demonstrates how binding power and associativity of operators can be
wenzelm@28762
   458
  enforced by priorities.
wenzelm@28762
   459
wenzelm@28762
   460
  \begin{center}
wenzelm@28762
   461
  \begin{tabular}{rclr}
wenzelm@28762
   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|)| \\
wenzelm@28762
   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| \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   467
  \end{tabular}
wenzelm@28762
   468
  \end{center}
wenzelm@28762
   469
  The choice of priorities determines that \verb|-| binds
wenzelm@28762
   470
  tighter than \verb|*|, which binds tighter than \verb|+|.  Furthermore \verb|+| associates to the left and
wenzelm@28762
   471
  \verb|*| to the right.
wenzelm@28762
   472
wenzelm@28762
   473
  \medskip For clarity, grammars obey these conventions:
wenzelm@28762
   474
  \begin{itemize}
wenzelm@28762
   475
wenzelm@28762
   476
  \item All priorities must lie between 0 and 1000.
wenzelm@28762
   477
wenzelm@28762
   478
  \item Priority 0 on the right-hand side and priority 1000 on the
wenzelm@28762
   479
  left-hand side may be omitted.
wenzelm@28762
   480
wenzelm@28762
   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
wenzelm@28762
   482
  a column on the far right.
wenzelm@28762
   483
wenzelm@28762
   484
  \item Alternatives are separated by \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}.
wenzelm@28762
   485
wenzelm@28762
   486
  \item Repetition is indicated by dots \isa{{\isachardoublequote}{\isacharparenleft}{\isasymdots}{\isacharparenright}{\isachardoublequote}} in an informal
wenzelm@28762
   487
  but obvious way.
wenzelm@28762
   488
wenzelm@28762
   489
  \end{itemize}
wenzelm@28762
   490
wenzelm@28762
   491
  Using these conventions, the example grammar specification above
wenzelm@28762
   492
  takes the form:
wenzelm@28762
   493
  \begin{center}
wenzelm@28762
   494
  \begin{tabular}{rclc}
wenzelm@28762
   495
    \isa{A} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \verb|(| \isa{A} \verb|)| \\
wenzelm@28762
   496
              & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|0| & \qquad\qquad \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   499
              & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|-| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28762
   500
  \end{tabular}
wenzelm@28762
   501
  \end{center}%
wenzelm@28762
   502
\end{isamarkuptext}%
wenzelm@28762
   503
\isamarkuptrue%
wenzelm@28762
   504
%
wenzelm@28762
   505
\isamarkupsubsection{The Pure grammar%
wenzelm@28762
   506
}
wenzelm@28762
   507
\isamarkuptrue%
wenzelm@28762
   508
%
wenzelm@28762
   509
\begin{isamarkuptext}%
wenzelm@28762
   510
The priority grammar of the \isa{{\isachardoublequote}Pure{\isachardoublequote}} theory is defined as follows:
wenzelm@28762
   511
wenzelm@28762
   512
  %FIXME syntax for "index" (?)
wenzelm@28762
   513
  %FIXME "op" versions of ==> etc. (?)
wenzelm@28762
   514
wenzelm@28762
   515
  \begin{center}
wenzelm@28762
   516
  \begin{supertabular}{rclr}
wenzelm@28762
   517
wenzelm@28762
   518
  \indexdef{inner}{syntax}{any}\hypertarget{syntax.inner.any}{\hyperlink{syntax.inner.any}{\mbox{\isa{any}}}} & = & \isa{{\isachardoublequote}prop\ \ {\isacharbar}\ \ logic{\isachardoublequote}} \\\\
wenzelm@28762
   519
wenzelm@28762
   520
  \indexdef{inner}{syntax}{prop}\hypertarget{syntax.inner.prop}{\hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}} & = & \verb|(| \isa{prop} \verb|)| \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28857
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   530
    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|!!| \isa{idts} \verb|.| \isa{prop} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28762
   531
    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} \isa{idts} \verb|.| \isa{prop} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28762
   532
    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|OFCLASS| \verb|(| \isa{type} \verb|,| \isa{logic} \verb|)| \\
wenzelm@28762
   533
    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|SORT_CONSTRAINT| \verb|(| \isa{type} \verb|)| \\
wenzelm@28857
   534
    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|TERM| \isa{logic} \\
wenzelm@28762
   535
    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|PROP| \isa{aprop} \\\\
wenzelm@28762
   536
wenzelm@28857
   537
  \indexdef{inner}{syntax}{aprop}\hypertarget{syntax.inner.aprop}{\hyperlink{syntax.inner.aprop}{\mbox{\isa{aprop}}}} & = & \verb|(| \isa{aprop} \verb|)| \\
wenzelm@28857
   538
    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ var\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|...| \\
wenzelm@28857
   539
    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|CONST| \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|CONST| \isa{{\isachardoublequote}longid{\isachardoublequote}} \\
wenzelm@28762
   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}} \\\\
wenzelm@28762
   541
wenzelm@28762
   542
  \indexdef{inner}{syntax}{logic}\hypertarget{syntax.inner.logic}{\hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}}} & = & \verb|(| \isa{logic} \verb|)| \\
wenzelm@28762
   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}} \\
wenzelm@28762
   544
    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ var\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|...| \\
wenzelm@28857
   545
    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|CONST| \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|CONST| \isa{{\isachardoublequote}longid{\isachardoublequote}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   549
    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|TYPE| \verb|(| \isa{type} \verb|)| \\\\
wenzelm@28762
   550
wenzelm@28762
   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|_| \\
wenzelm@28762
   552
    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{id} \verb|::| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
wenzelm@28762
   553
    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|_| \verb|::| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\\\
wenzelm@28762
   554
wenzelm@28762
   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}} \\\\
wenzelm@28762
   556
wenzelm@28762
   557
  \indexdef{inner}{syntax}{pttrn}\hypertarget{syntax.inner.pttrn}{\hyperlink{syntax.inner.pttrn}{\mbox{\isa{pttrn}}}} & = & \isa{idt} \\\\
wenzelm@28762
   558
wenzelm@28762
   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}} \\\\
wenzelm@28762
   560
wenzelm@28762
   561
  \indexdef{inner}{syntax}{type}\hypertarget{syntax.inner.type}{\hyperlink{syntax.inner.type}{\mbox{\isa{type}}}} & = & \verb|(| \isa{type} \verb|)| \\
wenzelm@28762
   562
    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}tid\ \ {\isacharbar}\ \ tvar\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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} \\
wenzelm@29746
   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}} \\
wenzelm@29746
   566
    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|(| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|)| \isa{longid} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\\\
wenzelm@28762
   571
wenzelm@29746
   572
  \indexdef{inner}{syntax}{sort}\hypertarget{syntax.inner.sort}{\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}}} & = & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|{}| \\
wenzelm@29746
   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|}| \\
wenzelm@28762
   574
  \end{supertabular}
wenzelm@28762
   575
  \end{center}
wenzelm@28762
   576
wenzelm@28762
   577
  \medskip Here literal terminals are printed \verb|verbatim|;
wenzelm@28762
   578
  see also \secref{sec:inner-lex} for further token categories of the
wenzelm@28762
   579
  inner syntax.  The meaning of the nonterminals defined by the above
wenzelm@28762
   580
  grammar is as follows:
wenzelm@28762
   581
wenzelm@28762
   582
  \begin{description}
wenzelm@28762
   583
wenzelm@28762
   584
  \item \indexref{inner}{syntax}{any}\hyperlink{syntax.inner.any}{\mbox{\isa{any}}} denotes any term.
wenzelm@28762
   585
wenzelm@28762
   586
  \item \indexref{inner}{syntax}{prop}\hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}} denotes meta-level propositions,
wenzelm@28762
   587
  which are terms of type \isa{prop}.  The syntax of such formulae of
wenzelm@28762
   588
  the meta-logic is carefully distinguished from usual conventions for
wenzelm@28762
   589
  object-logics.  In particular, plain \isa{{\isachardoublequote}{\isasymlambda}{\isachardoublequote}}-term notation is
wenzelm@28762
   590
  \emph{not} recognized as \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}.
wenzelm@28762
   591
wenzelm@28762
   592
  \item \indexref{inner}{syntax}{aprop}\hyperlink{syntax.inner.aprop}{\mbox{\isa{aprop}}} denotes atomic propositions, which
wenzelm@28762
   593
  are embedded into regular \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}} by means of an
wenzelm@28762
   594
  explicit \verb|PROP| token.
wenzelm@28762
   595
wenzelm@28762
   596
  Terms of type \isa{prop} with non-constant head, e.g.\ a plain
wenzelm@28762
   597
  variable, are printed in this form.  Constants that yield type \isa{prop} are expected to provide their own concrete syntax; otherwise
wenzelm@28762
   598
  the printed version will appear like \hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}} and
wenzelm@28762
   599
  cannot be parsed again as \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}.
wenzelm@28762
   600
wenzelm@28762
   601
  \item \indexref{inner}{syntax}{logic}\hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}} denotes arbitrary terms of a
wenzelm@28762
   602
  logical type, excluding type \isa{prop}.  This is the main
wenzelm@28762
   603
  syntactic category of object-logic entities, covering plain \isa{{\isasymlambda}}-term notation (variables, abstraction, application), plus
wenzelm@28762
   604
  anything defined by the user.
wenzelm@28762
   605
wenzelm@28762
   606
  When specifying notation for logical entities, all logical types
wenzelm@28762
   607
  (excluding \isa{prop}) are \emph{collapsed} to this single category
wenzelm@28762
   608
  of \hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}}.
wenzelm@28762
   609
wenzelm@28762
   610
  \item \indexref{inner}{syntax}{idt}\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}} denotes identifiers, possibly
wenzelm@28762
   611
  constrained by types.
wenzelm@28762
   612
wenzelm@28762
   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
wenzelm@28762
   614
  iterated binders, such as \isa{{\isachardoublequote}{\isasymlambda}{\isachardoublequote}} or \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}}.
wenzelm@28762
   615
wenzelm@28762
   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}}}
wenzelm@28762
   617
  denote patterns for abstraction, cases bindings etc.  In Pure, these
wenzelm@28762
   618
  categories start as a merely copy of \hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}} and
wenzelm@28762
   619
  \hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}, respectively.  Object-logics may add
wenzelm@28762
   620
  additional productions for binding forms.
wenzelm@28762
   621
wenzelm@28762
   622
  \item \indexref{inner}{syntax}{type}\hyperlink{syntax.inner.type}{\mbox{\isa{type}}} denotes types of the meta-logic.
wenzelm@28762
   623
wenzelm@28762
   624
  \item \indexref{inner}{syntax}{sort}\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}} denotes meta-level sorts.
wenzelm@28762
   625
wenzelm@28762
   626
  \end{description}
wenzelm@28762
   627
wenzelm@28762
   628
  Here are some further explanations of certain syntax features.
wenzelm@28762
   629
wenzelm@28762
   630
  \begin{itemize}
wenzelm@28762
   631
wenzelm@28762
   632
  \item In \hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}, note that \isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ nat\ y{\isachardoublequote}} is
wenzelm@28762
   633
  parsed as \isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}nat\ y{\isacharparenright}{\isachardoublequote}}, treating \isa{y} like a type
wenzelm@28762
   634
  constructor applied to \isa{nat}.  To avoid this interpretation,
wenzelm@28762
   635
  write \isa{{\isachardoublequote}{\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}\ y{\isachardoublequote}} with explicit parentheses.
wenzelm@28762
   636
wenzelm@28762
   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
wenzelm@28762
   638
  sequence of identifiers.
wenzelm@28762
   639
wenzelm@28762
   640
  \item Type constraints for terms bind very weakly.  For example,
wenzelm@28762
   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
wenzelm@28762
   642
  input is likely to be ambiguous.  The correct form is \isa{{\isachardoublequote}x\ {\isacharless}\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}{\isachardoublequote}}.
wenzelm@28762
   643
wenzelm@28762
   644
  \item Constraints may be either written with two literal colons
wenzelm@28762
   645
  ``\verb|::|'' or the double-colon symbol \verb|\<Colon>|,
wenzelm@28762
   646
  which actually looks exactly the same in some {\LaTeX} styles.
wenzelm@28762
   647
wenzelm@28762
   648
  \item Dummy variables (written as underscore) may occur in different
wenzelm@28762
   649
  roles.
wenzelm@28762
   650
wenzelm@28762
   651
  \begin{description}
wenzelm@28762
   652
wenzelm@28762
   653
  \item A type ``\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}'' or ``\isa{{\isachardoublequote}{\isacharunderscore}\ {\isacharcolon}{\isacharcolon}\ sort{\isachardoublequote}}'' acts like an
wenzelm@28762
   654
  anonymous inference parameter, which is filled-in according to the
wenzelm@28762
   655
  most general type produced by the type-checking phase.
wenzelm@28762
   656
wenzelm@28762
   657
  \item A bound ``\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}'' refers to a vacuous abstraction, where
wenzelm@28762
   658
  the body does not refer to the binding introduced here.  As in the
wenzelm@28762
   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}}.
wenzelm@28762
   660
wenzelm@28762
   661
  \item A free ``\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}'' refers to an implicit outer binding.
wenzelm@28762
   662
  Higher definitional packages usually allow forms like \isa{{\isachardoublequote}f\ x\ {\isacharunderscore}\ {\isacharequal}\ x{\isachardoublequote}}.
wenzelm@28762
   663
wenzelm@28762
   664
  \item A schematic ``\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}'' (within a term pattern, see
wenzelm@28762
   665
  \secref{sec:term-decls}) refers to an anonymous variable that is
wenzelm@28762
   666
  implicitly abstracted over its context of locally bound variables.
wenzelm@28762
   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
wenzelm@28762
   668
  using both bound and schematic dummies.
wenzelm@28762
   669
wenzelm@28762
   670
  \end{description}
wenzelm@28762
   671
wenzelm@28762
   672
  \item The three literal dots ``\verb|...|'' may be also
wenzelm@28762
   673
  written as ellipsis symbol \verb|\<dots>|.  In both cases this
wenzelm@28762
   674
  refers to a special schematic variable, which is bound in the
wenzelm@28762
   675
  context.  This special term abbreviation works nicely with
wenzelm@28762
   676
  calculational reasoning (\secref{sec:calculation}).
wenzelm@28762
   677
wenzelm@28762
   678
  \end{itemize}%
wenzelm@28762
   679
\end{isamarkuptext}%
wenzelm@28762
   680
\isamarkuptrue%
wenzelm@28762
   681
%
wenzelm@28762
   682
\isamarkupsection{Lexical matters \label{sec:inner-lex}%
wenzelm@28762
   683
}
wenzelm@28762
   684
\isamarkuptrue%
wenzelm@28762
   685
%
wenzelm@28762
   686
\begin{isamarkuptext}%
wenzelm@28762
   687
The inner lexical syntax vaguely resembles the outer one
wenzelm@28762
   688
  (\secref{sec:outer-lex}), but some details are different.  There are
wenzelm@28762
   689
  two main categories of inner syntax tokens:
wenzelm@28762
   690
wenzelm@28762
   691
  \begin{enumerate}
wenzelm@28762
   692
wenzelm@28762
   693
  \item \emph{delimiters} --- the literal tokens occurring in
wenzelm@28762
   694
  productions of the given priority grammar (cf.\
wenzelm@28762
   695
  \secref{sec:priority-grammar});
wenzelm@28762
   696
wenzelm@28762
   697
  \item \emph{named tokens} --- various categories of identifiers etc.
wenzelm@28762
   698
wenzelm@28762
   699
  \end{enumerate}
wenzelm@28762
   700
wenzelm@28762
   701
  Delimiters override named tokens and may thus render certain
wenzelm@28762
   702
  identifiers inaccessible.  Sometimes the logical context admits
wenzelm@28762
   703
  alternative ways to refer to the same entity, potentially via
wenzelm@28762
   704
  qualified names.
wenzelm@28762
   705
wenzelm@28762
   706
  \medskip The categories for named tokens are defined once and for
wenzelm@28762
   707
  all as follows, reusing some categories of the outer token syntax
wenzelm@28762
   708
  (\secref{sec:outer-lex}).
wenzelm@28762
   709
wenzelm@28762
   710
  \begin{center}
wenzelm@28762
   711
  \begin{supertabular}{rcl}
wenzelm@28762
   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}}} \\
wenzelm@28762
   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}}} \\
wenzelm@28762
   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}}} \\
wenzelm@28762
   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}}} \\
wenzelm@28762
   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}}} \\
wenzelm@28762
   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}}} \\
wenzelm@29158
   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}}} \\
wenzelm@28762
   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}}} \\
wenzelm@28762
   720
wenzelm@28762
   721
    \indexdef{inner}{syntax}{xstr}\hypertarget{syntax.inner.xstr}{\hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}}} & = & \verb|''| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|''| \\
wenzelm@28762
   722
  \end{supertabular}
wenzelm@28762
   723
  \end{center}
wenzelm@28762
   724
wenzelm@29158
   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
wenzelm@29158
   726
  not used in Pure.  Object-logics may implement numerals and string
wenzelm@29158
   727
  constants by adding appropriate syntax declarations, together with
wenzelm@29158
   728
  some translation functions (e.g.\ see Isabelle/HOL).
wenzelm@29158
   729
wenzelm@29158
   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
wenzelm@29158
   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
wenzelm@29158
   732
  syntax tree holds a syntactic constant instead of a free variable.%
wenzelm@28762
   733
\end{isamarkuptext}%
wenzelm@28762
   734
\isamarkuptrue%
wenzelm@28762
   735
%
wenzelm@28762
   736
\isamarkupsection{Syntax and translations \label{sec:syn-trans}%
wenzelm@28762
   737
}
wenzelm@28762
   738
\isamarkuptrue%
wenzelm@28762
   739
%
wenzelm@28762
   740
\begin{isamarkuptext}%
wenzelm@28762
   741
\begin{matharray}{rcl}
wenzelm@28762
   742
    \indexdef{}{command}{nonterminals}\hypertarget{command.nonterminals}{\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
wenzelm@28762
   743
    \indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   745
    \indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   747
  \end{matharray}
wenzelm@28762
   748
wenzelm@28762
   749
  \begin{rail}
wenzelm@28762
   750
    'nonterminals' (name +)
wenzelm@28762
   751
    ;
wenzelm@40255
   752
    ('syntax' | 'no_syntax') mode? (constdecl +)
wenzelm@28762
   753
    ;
wenzelm@40255
   754
    ('translations' | 'no_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
wenzelm@28762
   755
    ;
wenzelm@28762
   756
wenzelm@28762
   757
    mode: ('(' ( name | 'output' | name 'output' ) ')')
wenzelm@28762
   758
    ;
wenzelm@28762
   759
    transpat: ('(' nameref ')')? string
wenzelm@28762
   760
    ;
wenzelm@28762
   761
  \end{rail}
wenzelm@28762
   762
wenzelm@28762
   763
  \begin{description}
wenzelm@28762
   764
  
wenzelm@28762
   765
  \item \hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}~\isa{c} declares a type
wenzelm@28762
   766
  constructor \isa{c} (without arguments) to act as purely syntactic
wenzelm@28762
   767
  type: a nonterminal symbol of the inner syntax.
wenzelm@28762
   768
wenzelm@28762
   769
  \item \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}} is similar to
wenzelm@28762
   770
  \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{decls}, except that the actual logical
wenzelm@28762
   771
  signature extension is omitted.  Thus the context free grammar of
wenzelm@28762
   772
  Isabelle's inner syntax may be augmented in arbitrary ways,
wenzelm@28762
   773
  independently of the logic.  The \isa{mode} argument refers to the
wenzelm@28762
   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
wenzelm@28762
   775
  input and output grammar.
wenzelm@28762
   776
  
wenzelm@28762
   777
  \item \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}} removes grammar
wenzelm@28762
   778
  declarations (and translations) resulting from \isa{decls}, which
wenzelm@28762
   779
  are interpreted in the same manner as for \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} above.
wenzelm@28762
   780
  
wenzelm@28762
   781
  \item \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules} specifies syntactic
wenzelm@28762
   782
  translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isachardoublequote}{\isasymrightleftharpoons}{\isachardoublequote}}),
wenzelm@28762
   783
  parse rules (\isa{{\isachardoublequote}{\isasymrightharpoonup}{\isachardoublequote}}), or print rules (\isa{{\isachardoublequote}{\isasymleftharpoondown}{\isachardoublequote}}).
wenzelm@28762
   784
  Translation patterns may be prefixed by the syntactic category to be
wenzelm@28762
   785
  used for parsing; the default is \isa{logic}.
wenzelm@28762
   786
  
wenzelm@28762
   787
  \item \hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}~\isa{rules} removes syntactic
wenzelm@28762
   788
  translation rules, which are interpreted in the same manner as for
wenzelm@28762
   789
  \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} above.
wenzelm@28762
   790
wenzelm@28762
   791
  \end{description}%
wenzelm@28762
   792
\end{isamarkuptext}%
wenzelm@28762
   793
\isamarkuptrue%
wenzelm@28762
   794
%
wenzelm@28762
   795
\isamarkupsection{Syntax translation functions \label{sec:tr-funs}%
wenzelm@28762
   796
}
wenzelm@28762
   797
\isamarkuptrue%
wenzelm@28762
   798
%
wenzelm@28762
   799
\begin{isamarkuptext}%
wenzelm@28762
   800
\begin{matharray}{rcl}
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   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}} \\
wenzelm@28762
   806
  \end{matharray}
wenzelm@28762
   807
wenzelm@28762
   808
  \begin{rail}
wenzelm@40255
   809
  ( 'parse_ast_translation' | 'parse_translation' | 'print_translation' |
wenzelm@40255
   810
    'typed_print_translation' | 'print_ast_translation' ) ('(advanced)')? text
wenzelm@28762
   811
  ;
wenzelm@28762
   812
  \end{rail}
wenzelm@28762
   813
wenzelm@28762
   814
  Syntax translation functions written in ML admit almost arbitrary
wenzelm@28762
   815
  manipulations of Isabelle's inner syntax.  Any of the above commands
wenzelm@28762
   816
  have a single \railqtok{text} argument that refers to an ML
wenzelm@28762
   817
  expression of appropriate type, which are as follows by default:
wenzelm@28762
   818
wenzelm@28762
   819
%FIXME proper antiquotations
wenzelm@28762
   820
\begin{ttbox}
wenzelm@28762
   821
val parse_ast_translation   : (string * (ast list -> ast)) list
wenzelm@28762
   822
val parse_translation       : (string * (term list -> term)) list
wenzelm@28762
   823
val print_translation       : (string * (term list -> term)) list
wenzelm@28762
   824
val typed_print_translation :
wenzelm@28762
   825
  (string * (bool -> typ -> term list -> term)) list
wenzelm@28762
   826
val print_ast_translation   : (string * (ast list -> ast)) list
wenzelm@28762
   827
\end{ttbox}
wenzelm@28762
   828
wenzelm@28762
   829
  If the \isa{{\isachardoublequote}{\isacharparenleft}advanced{\isacharparenright}{\isachardoublequote}} option is given, the corresponding
wenzelm@28762
   830
  translation functions may depend on the current theory or proof
wenzelm@28762
   831
  context.  This allows to implement advanced syntax mechanisms, as
wenzelm@28762
   832
  translations functions may refer to specific theory declarations or
wenzelm@28762
   833
  auxiliary proof data.
wenzelm@28762
   834
wenzelm@30397
   835
  See also \cite{isabelle-ref} for more information on the general
wenzelm@30397
   836
  concept of syntax transformations in Isabelle.
wenzelm@28762
   837
wenzelm@28762
   838
%FIXME proper antiquotations
wenzelm@28762
   839
\begin{ttbox}
wenzelm@28762
   840
val parse_ast_translation:
wenzelm@28762
   841
  (string * (Proof.context -> ast list -> ast)) list
wenzelm@28762
   842
val parse_translation:
wenzelm@28762
   843
  (string * (Proof.context -> term list -> term)) list
wenzelm@28762
   844
val print_translation:
wenzelm@28762
   845
  (string * (Proof.context -> term list -> term)) list
wenzelm@28762
   846
val typed_print_translation:
wenzelm@28762
   847
  (string * (Proof.context -> bool -> typ -> term list -> term)) list
wenzelm@28762
   848
val print_ast_translation:
wenzelm@28762
   849
  (string * (Proof.context -> ast list -> ast)) list
wenzelm@28762
   850
\end{ttbox}%
wenzelm@28762
   851
\end{isamarkuptext}%
wenzelm@28762
   852
\isamarkuptrue%
wenzelm@28762
   853
%
wenzelm@28762
   854
\isamarkupsection{Inspecting the syntax%
wenzelm@28762
   855
}
wenzelm@28762
   856
\isamarkuptrue%
wenzelm@28762
   857
%
wenzelm@28762
   858
\begin{isamarkuptext}%
wenzelm@28762
   859
\begin{matharray}{rcl}
wenzelm@28762
   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}} \\
wenzelm@28762
   861
  \end{matharray}
wenzelm@28762
   862
wenzelm@28762
   863
  \begin{description}
wenzelm@28762
   864
wenzelm@28762
   865
  \item \hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}} prints the inner syntax of the
wenzelm@28762
   866
  current context.  The output can be quite large; the most important
wenzelm@28762
   867
  sections are explained below.
wenzelm@28762
   868
wenzelm@28762
   869
  \begin{description}
wenzelm@28762
   870
wenzelm@28762
   871
  \item \isa{{\isachardoublequote}lexicon{\isachardoublequote}} lists the delimiters of the inner token
wenzelm@28762
   872
  language; see \secref{sec:inner-lex}.
wenzelm@28762
   873
wenzelm@28762
   874
  \item \isa{{\isachardoublequote}prods{\isachardoublequote}} lists the productions of the underlying
wenzelm@28762
   875
  priority grammar; see \secref{sec:priority-grammar}.
wenzelm@28762
   876
wenzelm@28762
   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
wenzelm@28762
   878
  \isa{{\isachardoublequote}{\isasymdots}\ {\isacharequal}{\isachargreater}\ name{\isachardoublequote}}.  These names later become the heads of parse
wenzelm@28762
   879
  trees; they also guide the pretty printer.
wenzelm@28762
   880
wenzelm@28762
   881
  Productions without such parse tree names are called \emph{copy
wenzelm@28762
   882
  productions}.  Their right-hand side must have exactly one
wenzelm@28762
   883
  nonterminal symbol (or named token).  The parser does not create a
wenzelm@28762
   884
  new parse tree node for copy productions, but simply returns the
wenzelm@28762
   885
  parse tree of the right-hand symbol.
wenzelm@28762
   886
wenzelm@28762
   887
  If the right-hand side of a copy production consists of a single
wenzelm@28762
   888
  nonterminal without any delimiters, then it is called a \emph{chain
wenzelm@28762
   889
  production}.  Chain productions act as abbreviations: conceptually,
wenzelm@28762
   890
  they are removed from the grammar by adding new productions.
wenzelm@28762
   891
  Priority information attached to chain productions is ignored; only
wenzelm@28762
   892
  the dummy value \isa{{\isachardoublequote}{\isacharminus}{\isadigit{1}}{\isachardoublequote}} is displayed.
wenzelm@28762
   893
wenzelm@28857
   894
  \item \isa{{\isachardoublequote}print\ modes{\isachardoublequote}} lists the alternative print modes
wenzelm@28762
   895
  provided by this grammar; see \secref{sec:print-modes}.
wenzelm@28762
   896
wenzelm@28762
   897
  \item \isa{{\isachardoublequote}parse{\isacharunderscore}rules{\isachardoublequote}} and \isa{{\isachardoublequote}print{\isacharunderscore}rules{\isachardoublequote}} relate to
wenzelm@28762
   898
  syntax translations (macros); see \secref{sec:syn-trans}.
wenzelm@28762
   899
wenzelm@28762
   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
wenzelm@28762
   901
  translation functions for abstract syntax trees, which are only
wenzelm@28762
   902
  required in very special situations; see \secref{sec:tr-funs}.
wenzelm@28762
   903
wenzelm@28762
   904
  \item \isa{{\isachardoublequote}parse{\isacharunderscore}translation{\isachardoublequote}} and \isa{{\isachardoublequote}print{\isacharunderscore}translation{\isachardoublequote}}
wenzelm@28762
   905
  list the sets of constants that invoke regular translation
wenzelm@28762
   906
  functions; see \secref{sec:tr-funs}.
wenzelm@28762
   907
wenzelm@28762
   908
  \end{description}
wenzelm@28762
   909
  
wenzelm@28762
   910
  \end{description}%
wenzelm@28762
   911
\end{isamarkuptext}%
wenzelm@28762
   912
\isamarkuptrue%
wenzelm@28762
   913
%
wenzelm@28762
   914
\isadelimtheory
wenzelm@28762
   915
%
wenzelm@28762
   916
\endisadelimtheory
wenzelm@28762
   917
%
wenzelm@28762
   918
\isatagtheory
wenzelm@28762
   919
\isacommand{end}\isamarkupfalse%
wenzelm@28762
   920
%
wenzelm@28762
   921
\endisatagtheory
wenzelm@28762
   922
{\isafoldtheory}%
wenzelm@28762
   923
%
wenzelm@28762
   924
\isadelimtheory
wenzelm@28762
   925
%
wenzelm@28762
   926
\endisadelimtheory
wenzelm@28762
   927
\isanewline
wenzelm@28762
   928
\end{isabellebody}%
wenzelm@28762
   929
%%% Local Variables:
wenzelm@28762
   930
%%% mode: latex
wenzelm@28762
   931
%%% TeX-master: "root"
wenzelm@28762
   932
%%% End: