src/Doc/Isar_Ref/Inner_Syntax.thy
changeset 62106 d6af554512d7
parent 61997 4d9518c3d031
child 62107 f74a33b14200
     1.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Jan 08 19:46:30 2016 +0100
     1.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Jan 08 20:06:48 2016 +0100
     1.3 @@ -6,26 +6,25 @@
     1.4  
     1.5  chapter \<open>Inner syntax --- the term language \label{ch:inner-syntax}\<close>
     1.6  
     1.7 -text \<open>The inner syntax of Isabelle provides concrete notation for
     1.8 -  the main entities of the logical framework, notably \<open>\<lambda>\<close>-terms with types and type classes.  Applications may either
     1.9 -  extend existing syntactic categories by additional notation, or
    1.10 -  define new sub-languages that are linked to the standard term
    1.11 -  language via some explicit markers.  For example \<^verbatim>\<open>FOO\<close>~\<open>foo\<close> could
    1.12 -  embed the syntax corresponding for some
    1.13 -  user-defined nonterminal \<open>foo\<close> --- within the bounds of the
    1.14 -  given lexical syntax of Isabelle/Pure.
    1.15 +text \<open>
    1.16 +  The inner syntax of Isabelle provides concrete notation for the main
    1.17 +  entities of the logical framework, notably \<open>\<lambda>\<close>-terms with types and type
    1.18 +  classes. Applications may either extend existing syntactic categories by
    1.19 +  additional notation, or define new sub-languages that are linked to the
    1.20 +  standard term language via some explicit markers. For example \<^verbatim>\<open>FOO\<close>~\<open>foo\<close>
    1.21 +  could embed the syntax corresponding for some user-defined nonterminal \<open>foo\<close>
    1.22 +  --- within the bounds of the given lexical syntax of Isabelle/Pure.
    1.23  
    1.24 -  The most basic way to specify concrete syntax for logical entities
    1.25 -  works via mixfix annotations (\secref{sec:mixfix}), which may be
    1.26 -  usually given as part of the original declaration or via explicit
    1.27 -  notation commands later on (\secref{sec:notation}).  This already
    1.28 -  covers many needs of concrete syntax without having to understand
    1.29 -  the full complexity of inner syntax layers.
    1.30 +  The most basic way to specify concrete syntax for logical entities works via
    1.31 +  mixfix annotations (\secref{sec:mixfix}), which may be usually given as part
    1.32 +  of the original declaration or via explicit notation commands later on
    1.33 +  (\secref{sec:notation}). This already covers many needs of concrete syntax
    1.34 +  without having to understand the full complexity of inner syntax layers.
    1.35  
    1.36 -  Further details of the syntax engine involves the classical
    1.37 -  distinction of lexical language versus context-free grammar (see
    1.38 -  \secref{sec:pure-syntax}), and various mechanisms for \<^emph>\<open>syntax
    1.39 -  transformations\<close> (see \secref{sec:syntax-transformations}).
    1.40 +  Further details of the syntax engine involves the classical distinction of
    1.41 +  lexical language versus context-free grammar (see \secref{sec:pure-syntax}),
    1.42 +  and various mechanisms for \<^emph>\<open>syntax transformations\<close> (see
    1.43 +  \secref{sec:syntax-transformations}).
    1.44  \<close>
    1.45  
    1.46  
    1.47 @@ -63,43 +62,39 @@
    1.48      @{syntax_def modes}: '(' (@{syntax name} + ) ')'
    1.49    \<close>}
    1.50  
    1.51 -  \<^descr> @{command "typ"}~\<open>\<tau>\<close> reads and prints a type expression
    1.52 -  according to the current context.
    1.53 +  \<^descr> @{command "typ"}~\<open>\<tau>\<close> reads and prints a type expression according to the
    1.54 +  current context.
    1.55  
    1.56 -  \<^descr> @{command "typ"}~\<open>\<tau> :: s\<close> uses type-inference to
    1.57 -  determine the most general way to make \<open>\<tau>\<close> conform to sort
    1.58 -  \<open>s\<close>.  For concrete \<open>\<tau>\<close> this checks if the type
    1.59 -  belongs to that sort.  Dummy type parameters ``\<open>_\<close>''
    1.60 -  (underscore) are assigned to fresh type variables with most general
    1.61 -  sorts, according the the principles of type-inference.
    1.62 +  \<^descr> @{command "typ"}~\<open>\<tau> :: s\<close> uses type-inference to determine the most
    1.63 +  general way to make \<open>\<tau>\<close> conform to sort \<open>s\<close>. For concrete \<open>\<tau>\<close> this checks if
    1.64 +  the type belongs to that sort. Dummy type parameters ``\<open>_\<close>'' (underscore)
    1.65 +  are assigned to fresh type variables with most general sorts, according the
    1.66 +  the principles of type-inference.
    1.67  
    1.68 -  \<^descr> @{command "term"}~\<open>t\<close> and @{command "prop"}~\<open>\<phi>\<close>
    1.69 -  read, type-check and print terms or propositions according to the
    1.70 -  current theory or proof context; the inferred type of \<open>t\<close> is
    1.71 -  output as well.  Note that these commands are also useful in
    1.72 -  inspecting the current environment of term abbreviations.
    1.73 +    \<^descr> @{command "term"}~\<open>t\<close> and @{command "prop"}~\<open>\<phi>\<close> read, type-check and
    1.74 +    print terms or propositions according to the current theory or proof
    1.75 +    context; the inferred type of \<open>t\<close> is output as well. Note that these
    1.76 +    commands are also useful in inspecting the current environment of term
    1.77 +    abbreviations.
    1.78  
    1.79 -  \<^descr> @{command "thm"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> retrieves
    1.80 -  theorems from the current theory or proof context.  Note that any
    1.81 -  attributes included in the theorem specifications are applied to a
    1.82 -  temporary context derived from the current theory or proof; the
    1.83 -  result is discarded, i.e.\ attributes involved in \<open>a\<^sub>1,
    1.84 -  \<dots>, a\<^sub>n\<close> do not have any permanent effect.
    1.85 +    \<^descr> @{command "thm"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> retrieves theorems from the current theory
    1.86 +    or proof context. Note that any attributes included in the theorem
    1.87 +    specifications are applied to a temporary context derived from the current
    1.88 +    theory or proof; the result is discarded, i.e.\ attributes involved in
    1.89 +    \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> do not have any permanent effect.
    1.90  
    1.91 -  \<^descr> @{command "prf"} displays the (compact) proof term of the
    1.92 -  current proof state (if present), or of the given theorems. Note
    1.93 -  that this requires proof terms to be switched on for the current
    1.94 -  object logic (see the ``Proof terms'' section of the Isabelle
    1.95 -  reference manual for information on how to do this).
    1.96 +    \<^descr> @{command "prf"} displays the (compact) proof term of the current proof
    1.97 +    state (if present), or of the given theorems. Note that this requires
    1.98 +    proof terms to be switched on for the current object logic (see the
    1.99 +    ``Proof terms'' section of the Isabelle reference manual for information
   1.100 +    on how to do this).
   1.101  
   1.102 -  \<^descr> @{command "full_prf"} is like @{command "prf"}, but displays
   1.103 -  the full proof term, i.e.\ also displays information omitted in the
   1.104 -  compact proof term, which is denoted by ``\<open>_\<close>'' placeholders
   1.105 -  there.
   1.106 +    \<^descr> @{command "full_prf"} is like @{command "prf"}, but displays the full
   1.107 +    proof term, i.e.\ also displays information omitted in the compact proof
   1.108 +    term, which is denoted by ``\<open>_\<close>'' placeholders there.
   1.109  
   1.110 -  \<^descr> @{command "print_state"} prints the current proof state (if
   1.111 -  present), including current facts and goals.
   1.112 -
   1.113 +    \<^descr> @{command "print_state"} prints the current proof state (if present),
   1.114 +    including current facts and goals.
   1.115  
   1.116    All of the diagnostic commands above admit a list of \<open>modes\<close> to be
   1.117    specified, which is appended to the current print mode; see also
   1.118 @@ -109,9 +104,8 @@
   1.119    symbols and special characters represented in {\LaTeX} source, according to
   1.120    the Isabelle style @{cite "isabelle-system"}.
   1.121  
   1.122 -  Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
   1.123 -  systematic way to include formal items into the printed text
   1.124 -  document.
   1.125 +  Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more systematic
   1.126 +  way to include formal items into the printed text document.
   1.127  \<close>
   1.128  
   1.129  
   1.130 @@ -137,100 +131,90 @@
   1.131    \end{tabular}
   1.132    \<^medskip>
   1.133  
   1.134 -  These configuration options control the detail of information that
   1.135 -  is displayed for types, terms, theorems, goals etc.  See also
   1.136 +  These configuration options control the detail of information that is
   1.137 +  displayed for types, terms, theorems, goals etc. See also
   1.138    \secref{sec:config}.
   1.139  
   1.140 -  \<^descr> @{attribute show_markup} controls direct inlining of markup
   1.141 -  into the printed representation of formal entities --- notably type
   1.142 -  and sort constraints.  This enables Prover IDE users to retrieve
   1.143 -  that information via tooltips or popups while hovering with the
   1.144 -  mouse over the output window, for example.  Consequently, this
   1.145 -  option is enabled by default for Isabelle/jEdit.
   1.146 +  \<^descr> @{attribute show_markup} controls direct inlining of markup into the
   1.147 +  printed representation of formal entities --- notably type and sort
   1.148 +  constraints. This enables Prover IDE users to retrieve that information via
   1.149 +  tooltips or popups while hovering with the mouse over the output window, for
   1.150 +  example. Consequently, this option is enabled by default for Isabelle/jEdit.
   1.151  
   1.152 -  \<^descr> @{attribute show_types} and @{attribute show_sorts} control
   1.153 -  printing of type constraints for term variables, and sort
   1.154 -  constraints for type variables.  By default, neither of these are
   1.155 -  shown in output.  If @{attribute show_sorts} is enabled, types are
   1.156 -  always shown as well.  In Isabelle/jEdit, manual setting of these
   1.157 -  options is normally not required thanks to @{attribute show_markup}
   1.158 -  above.
   1.159 +  \<^descr> @{attribute show_types} and @{attribute show_sorts} control printing of
   1.160 +  type constraints for term variables, and sort constraints for type
   1.161 +  variables. By default, neither of these are shown in output. If @{attribute
   1.162 +  show_sorts} is enabled, types are always shown as well. In Isabelle/jEdit,
   1.163 +  manual setting of these options is normally not required thanks to
   1.164 +  @{attribute show_markup} above.
   1.165  
   1.166 -  Note that displaying types and sorts may explain why a polymorphic
   1.167 -  inference rule fails to resolve with some goal, or why a rewrite
   1.168 -  rule does not apply as expected.
   1.169 -
   1.170 -  \<^descr> @{attribute show_consts} controls printing of types of
   1.171 -  constants when displaying a goal state.
   1.172 +  Note that displaying types and sorts may explain why a polymorphic inference
   1.173 +  rule fails to resolve with some goal, or why a rewrite rule does not apply
   1.174 +  as expected.
   1.175  
   1.176 -  Note that the output can be enormous, because polymorphic constants
   1.177 -  often occur at several different type instances.
   1.178 +  \<^descr> @{attribute show_consts} controls printing of types of constants when
   1.179 +  displaying a goal state.
   1.180  
   1.181 -  \<^descr> @{attribute show_abbrevs} controls folding of constant
   1.182 -  abbreviations.
   1.183 +  Note that the output can be enormous, because polymorphic constants often
   1.184 +  occur at several different type instances.
   1.185 +
   1.186 +  \<^descr> @{attribute show_abbrevs} controls folding of constant abbreviations.
   1.187  
   1.188 -  \<^descr> @{attribute show_brackets} controls bracketing in pretty
   1.189 -  printed output.  If enabled, all sub-expressions of the pretty
   1.190 -  printing tree will be parenthesized, even if this produces malformed
   1.191 -  term syntax!  This crude way of showing the internal structure of
   1.192 -  pretty printed entities may occasionally help to diagnose problems
   1.193 -  with operator priorities, for example.
   1.194 +  \<^descr> @{attribute show_brackets} controls bracketing in pretty printed output.
   1.195 +  If enabled, all sub-expressions of the pretty printing tree will be
   1.196 +  parenthesized, even if this produces malformed term syntax! This crude way
   1.197 +  of showing the internal structure of pretty printed entities may
   1.198 +  occasionally help to diagnose problems with operator priorities, for
   1.199 +  example.
   1.200  
   1.201 -  \<^descr> @{attribute names_long}, @{attribute names_short}, and
   1.202 -  @{attribute names_unique} control the way of printing fully
   1.203 -  qualified internal names in external form.  See also
   1.204 -  \secref{sec:antiq} for the document antiquotation options of the
   1.205 -  same names.
   1.206 +  \<^descr> @{attribute names_long}, @{attribute names_short}, and @{attribute
   1.207 +  names_unique} control the way of printing fully qualified internal names in
   1.208 +  external form. See also \secref{sec:antiq} for the document antiquotation
   1.209 +  options of the same names.
   1.210  
   1.211 -  \<^descr> @{attribute eta_contract} controls \<open>\<eta>\<close>-contracted
   1.212 -  printing of terms.
   1.213 +  \<^descr> @{attribute eta_contract} controls \<open>\<eta>\<close>-contracted printing of terms.
   1.214  
   1.215 -  The \<open>\<eta>\<close>-contraction law asserts @{prop "(\<lambda>x. f x) \<equiv> f"},
   1.216 -  provided \<open>x\<close> is not free in \<open>f\<close>.  It asserts
   1.217 -  \<^emph>\<open>extensionality\<close> of functions: @{prop "f \<equiv> g"} if @{prop "f x \<equiv>
   1.218 -  g x"} for all \<open>x\<close>.  Higher-order unification frequently puts
   1.219 -  terms into a fully \<open>\<eta>\<close>-expanded form.  For example, if \<open>F\<close> has type \<open>(\<tau> \<Rightarrow> \<tau>) \<Rightarrow> \<tau>\<close> then its expanded form is @{term
   1.220 -  "\<lambda>h. F (\<lambda>x. h x)"}.
   1.221 +  The \<open>\<eta>\<close>-contraction law asserts @{prop "(\<lambda>x. f x) \<equiv> f"}, provided \<open>x\<close> is not
   1.222 +  free in \<open>f\<close>. It asserts \<^emph>\<open>extensionality\<close> of functions: @{prop "f \<equiv> g"} if
   1.223 +  @{prop "f x \<equiv> g x"} for all \<open>x\<close>. Higher-order unification frequently puts
   1.224 +  terms into a fully \<open>\<eta>\<close>-expanded form. For example, if \<open>F\<close> has type \<open>(\<tau> \<Rightarrow> \<tau>)
   1.225 +  \<Rightarrow> \<tau>\<close> then its expanded form is @{term "\<lambda>h. F (\<lambda>x. h x)"}.
   1.226  
   1.227 -  Enabling @{attribute eta_contract} makes Isabelle perform \<open>\<eta>\<close>-contractions before printing, so that @{term "\<lambda>h. F (\<lambda>x. h x)"}
   1.228 -  appears simply as \<open>F\<close>.
   1.229 +  Enabling @{attribute eta_contract} makes Isabelle perform \<open>\<eta>\<close>-contractions
   1.230 +  before printing, so that @{term "\<lambda>h. F (\<lambda>x. h x)"} appears simply as \<open>F\<close>.
   1.231  
   1.232 -  Note that the distinction between a term and its \<open>\<eta>\<close>-expanded
   1.233 -  form occasionally matters.  While higher-order resolution and
   1.234 -  rewriting operate modulo \<open>\<alpha>\<beta>\<eta>\<close>-conversion, some other tools
   1.235 -  might look at terms more discretely.
   1.236 +  Note that the distinction between a term and its \<open>\<eta>\<close>-expanded form
   1.237 +  occasionally matters. While higher-order resolution and rewriting operate
   1.238 +  modulo \<open>\<alpha>\<beta>\<eta>\<close>-conversion, some other tools might look at terms more
   1.239 +  discretely.
   1.240  
   1.241 -  \<^descr> @{attribute goals_limit} controls the maximum number of
   1.242 -  subgoals to be printed.
   1.243 +  \<^descr> @{attribute goals_limit} controls the maximum number of subgoals to be
   1.244 +  printed.
   1.245  
   1.246 -  \<^descr> @{attribute show_main_goal} controls whether the main result
   1.247 -  to be proven should be displayed.  This information might be
   1.248 -  relevant for schematic goals, to inspect the current claim that has
   1.249 -  been synthesized so far.
   1.250 +  \<^descr> @{attribute show_main_goal} controls whether the main result to be proven
   1.251 +  should be displayed. This information might be relevant for schematic goals,
   1.252 +  to inspect the current claim that has been synthesized so far.
   1.253  
   1.254 -  \<^descr> @{attribute show_hyps} controls printing of implicit
   1.255 -  hypotheses of local facts.  Normally, only those hypotheses are
   1.256 -  displayed that are \<^emph>\<open>not\<close> covered by the assumptions of the
   1.257 -  current context: this situation indicates a fault in some tool being
   1.258 -  used.
   1.259 +  \<^descr> @{attribute show_hyps} controls printing of implicit hypotheses of local
   1.260 +  facts. Normally, only those hypotheses are displayed that are \<^emph>\<open>not\<close> covered
   1.261 +  by the assumptions of the current context: this situation indicates a fault
   1.262 +  in some tool being used.
   1.263  
   1.264 -  By enabling @{attribute show_hyps}, output of \<^emph>\<open>all\<close> hypotheses
   1.265 -  can be enforced, which is occasionally useful for diagnostic
   1.266 -  purposes.
   1.267 +  By enabling @{attribute show_hyps}, output of \<^emph>\<open>all\<close> hypotheses can be
   1.268 +  enforced, which is occasionally useful for diagnostic purposes.
   1.269  
   1.270 -  \<^descr> @{attribute show_tags} controls printing of extra annotations
   1.271 -  within theorems, such as internal position information, or the case
   1.272 -  names being attached by the attribute @{attribute case_names}.
   1.273 +  \<^descr> @{attribute show_tags} controls printing of extra annotations within
   1.274 +  theorems, such as internal position information, or the case names being
   1.275 +  attached by the attribute @{attribute case_names}.
   1.276  
   1.277 -  Note that the @{attribute tagged} and @{attribute untagged}
   1.278 -  attributes provide low-level access to the collection of tags
   1.279 -  associated with a theorem.
   1.280 +  Note that the @{attribute tagged} and @{attribute untagged} attributes
   1.281 +  provide low-level access to the collection of tags associated with a
   1.282 +  theorem.
   1.283  
   1.284 -  \<^descr> @{attribute show_question_marks} controls printing of question
   1.285 -  marks for schematic variables, such as \<open>?x\<close>.  Only the leading
   1.286 -  question mark is affected, the remaining text is unchanged
   1.287 -  (including proper markup for schematic variables that might be
   1.288 -  relevant for user interfaces).
   1.289 +  \<^descr> @{attribute show_question_marks} controls printing of question marks for
   1.290 +  schematic variables, such as \<open>?x\<close>. Only the leading question mark is
   1.291 +  affected, the remaining text is unchanged (including proper markup for
   1.292 +  schematic variables that might be relevant for user interfaces).
   1.293  \<close>
   1.294  
   1.295  
   1.296 @@ -242,62 +226,58 @@
   1.297      @{index_ML Print_Mode.with_modes: "string list -> ('a -> 'b) -> 'a -> 'b"} \\
   1.298    \end{mldecls}
   1.299  
   1.300 -  The \<^emph>\<open>print mode\<close> facility allows to modify various operations
   1.301 -  for printing.  Commands like @{command typ}, @{command term},
   1.302 -  @{command thm} (see \secref{sec:print-diag}) take additional print
   1.303 -  modes as optional argument.  The underlying ML operations are as
   1.304 -  follows.
   1.305 +  The \<^emph>\<open>print mode\<close> facility allows to modify various operations for printing.
   1.306 +  Commands like @{command typ}, @{command term}, @{command thm} (see
   1.307 +  \secref{sec:print-diag}) take additional print modes as optional argument.
   1.308 +  The underlying ML operations are as follows.
   1.309  
   1.310 -  \<^descr> @{ML "print_mode_value ()"} yields the list of currently
   1.311 -  active print mode names.  This should be understood as symbolic
   1.312 -  representation of certain individual features for printing (with
   1.313 -  precedence from left to right).
   1.314 +    \<^descr> @{ML "print_mode_value ()"} yields the list of currently active print
   1.315 +    mode names. This should be understood as symbolic representation of
   1.316 +    certain individual features for printing (with precedence from left to
   1.317 +    right).
   1.318  
   1.319 -  \<^descr> @{ML Print_Mode.with_modes}~\<open>modes f x\<close> evaluates
   1.320 -  \<open>f x\<close> in an execution context where the print mode is
   1.321 -  prepended by the given \<open>modes\<close>.  This provides a thread-safe
   1.322 -  way to augment print modes.  It is also monotonic in the set of mode
   1.323 -  names: it retains the default print mode that certain
   1.324 -  user-interfaces might have installed for their proper functioning!
   1.325 -
   1.326 +    \<^descr> @{ML Print_Mode.with_modes}~\<open>modes f x\<close> evaluates \<open>f x\<close> in an execution
   1.327 +    context where the print mode is prepended by the given \<open>modes\<close>. This
   1.328 +    provides a thread-safe way to augment print modes. It is also monotonic in
   1.329 +    the set of mode names: it retains the default print mode that certain
   1.330 +    user-interfaces might have installed for their proper functioning!
   1.331  
   1.332    \<^medskip>
   1.333 -  The pretty printer for inner syntax maintains alternative
   1.334 -  mixfix productions for any print mode name invented by the user, say
   1.335 -  in commands like @{command notation} or @{command abbreviation}.
   1.336 -  Mode names can be arbitrary, but the following ones have a specific
   1.337 -  meaning by convention:
   1.338 +  The pretty printer for inner syntax maintains alternative mixfix productions
   1.339 +  for any print mode name invented by the user, say in commands like @{command
   1.340 +  notation} or @{command abbreviation}. Mode names can be arbitrary, but the
   1.341 +  following ones have a specific meaning by convention:
   1.342  
   1.343 -  \<^item> \<^verbatim>\<open>""\<close> (the empty string): default mode;
   1.344 -  implicitly active as last element in the list of modes.
   1.345 +    \<^item> \<^verbatim>\<open>""\<close> (the empty string): default mode; implicitly active as last
   1.346 +    element in the list of modes.
   1.347  
   1.348 -  \<^item> \<^verbatim>\<open>input\<close>: dummy print mode that is never active; may
   1.349 -  be used to specify notation that is only available for input.
   1.350 +    \<^item> \<^verbatim>\<open>input\<close>: dummy print mode that is never active; may be used to specify
   1.351 +    notation that is only available for input.
   1.352  
   1.353 -  \<^item> \<^verbatim>\<open>internal\<close> dummy print mode that is never active;
   1.354 -  used internally in Isabelle/Pure.
   1.355 +    \<^item> \<^verbatim>\<open>internal\<close> dummy print mode that is never active; used internally in
   1.356 +    Isabelle/Pure.
   1.357  
   1.358 -  \<^item> \<^verbatim>\<open>ASCII\<close>: prefer ASCII art over mathematical symbols.
   1.359 +    \<^item> \<^verbatim>\<open>ASCII\<close>: prefer ASCII art over mathematical symbols.
   1.360  
   1.361 -  \<^item> \<^verbatim>\<open>latex\<close>: additional mode that is active in {\LaTeX}
   1.362 -  document preparation of Isabelle theory sources; allows to provide
   1.363 -  alternative output notation.
   1.364 +    \<^item> \<^verbatim>\<open>latex\<close>: additional mode that is active in {\LaTeX} document
   1.365 +    preparation of Isabelle theory sources; allows to provide alternative
   1.366 +    output notation.
   1.367  \<close>
   1.368  
   1.369  
   1.370  section \<open>Mixfix annotations \label{sec:mixfix}\<close>
   1.371  
   1.372 -text \<open>Mixfix annotations specify concrete \<^emph>\<open>inner syntax\<close> of
   1.373 -  Isabelle types and terms.  Locally fixed parameters in toplevel
   1.374 -  theorem statements, locale and class specifications also admit
   1.375 -  mixfix annotations in a fairly uniform manner.  A mixfix annotation
   1.376 -  describes the concrete syntax, the translation to abstract
   1.377 -  syntax, and the pretty printing.  Special case annotations provide a
   1.378 -  simple means of specifying infix operators and binders.
   1.379 +text \<open>
   1.380 +  Mixfix annotations specify concrete \<^emph>\<open>inner syntax\<close> of Isabelle types and
   1.381 +  terms. Locally fixed parameters in toplevel theorem statements, locale and
   1.382 +  class specifications also admit mixfix annotations in a fairly uniform
   1.383 +  manner. A mixfix annotation describes the concrete syntax, the translation
   1.384 +  to abstract syntax, and the pretty printing. Special case annotations
   1.385 +  provide a simple means of specifying infix operators and binders.
   1.386  
   1.387 -  Isabelle mixfix syntax is inspired by {\OBJ} @{cite OBJ}.  It allows
   1.388 -  to specify any context-free priority grammar, which is more general
   1.389 -  than the fixity declarations of ML and Prolog.
   1.390 +  Isabelle mixfix syntax is inspired by {\OBJ} @{cite OBJ}. It allows to
   1.391 +  specify any context-free priority grammar, which is more general than the
   1.392 +  fixity declarations of ML and Prolog.
   1.393  
   1.394    @{rail \<open>
   1.395      @{syntax_def mixfix}: '('
   1.396 @@ -311,52 +291,48 @@
   1.397      prios: '[' (@{syntax nat} + ',') ']'
   1.398    \<close>}
   1.399  
   1.400 -  The string given as \<open>template\<close> may include literal text,
   1.401 -  spacing, blocks, and arguments (denoted by ``\<open>_\<close>''); the
   1.402 -  special symbol ``\<^verbatim>\<open>\<index>\<close>'' (printed as ``\<open>\<index>\<close>'')
   1.403 -  represents an index argument that specifies an implicit @{keyword
   1.404 -  "structure"} reference (see also \secref{sec:locale}).  Only locally
   1.405 -  fixed variables may be declared as @{keyword "structure"}.
   1.406 +  The string given as \<open>template\<close> may include literal text, spacing, blocks,
   1.407 +  and arguments (denoted by ``\<open>_\<close>''); the special symbol ``\<^verbatim>\<open>\<index>\<close>'' (printed as
   1.408 +  ``\<open>\<index>\<close>'') represents an index argument that specifies an implicit @{keyword
   1.409 +  "structure"} reference (see also \secref{sec:locale}). Only locally fixed
   1.410 +  variables may be declared as @{keyword "structure"}.
   1.411  
   1.412 -  Infix and binder declarations provide common abbreviations for
   1.413 -  particular mixfix declarations.  So in practice, mixfix templates
   1.414 -  mostly degenerate to literal text for concrete syntax, such as
   1.415 -  ``\<^verbatim>\<open>++\<close>'' for an infix symbol.
   1.416 +  Infix and binder declarations provide common abbreviations for particular
   1.417 +  mixfix declarations. So in practice, mixfix templates mostly degenerate to
   1.418 +  literal text for concrete syntax, such as ``\<^verbatim>\<open>++\<close>'' for an infix symbol.
   1.419  \<close>
   1.420  
   1.421  
   1.422  subsection \<open>The general mixfix form\<close>
   1.423  
   1.424 -text \<open>In full generality, mixfix declarations work as follows.
   1.425 -  Suppose a constant \<open>c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>\<close> is annotated by
   1.426 -  \<open>(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)\<close>, where \<open>mixfix\<close> is a string
   1.427 -  \<open>d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n\<close> consisting of delimiters that surround
   1.428 -  argument positions as indicated by underscores.
   1.429 +text \<open>
   1.430 +  In full generality, mixfix declarations work as follows. Suppose a constant
   1.431 +  \<open>c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>\<close> is annotated by \<open>(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)\<close>, where
   1.432 +  \<open>mixfix\<close> is a string \<open>d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n\<close> consisting of delimiters that
   1.433 +  surround argument positions as indicated by underscores.
   1.434  
   1.435 -  Altogether this determines a production for a context-free priority
   1.436 -  grammar, where for each argument \<open>i\<close> the syntactic category
   1.437 -  is determined by \<open>\<tau>\<^sub>i\<close> (with priority \<open>p\<^sub>i\<close>), and the
   1.438 -  result category is determined from \<open>\<tau>\<close> (with priority \<open>p\<close>).  Priority specifications are optional, with default 0 for
   1.439 -  arguments and 1000 for the result.\<^footnote>\<open>Omitting priorities is
   1.440 -  prone to syntactic ambiguities unless the delimiter tokens determine
   1.441 -  fully bracketed notation, as in \<open>if _ then _ else _ fi\<close>.\<close>
   1.442 +  Altogether this determines a production for a context-free priority grammar,
   1.443 +  where for each argument \<open>i\<close> the syntactic category is determined by \<open>\<tau>\<^sub>i\<close>
   1.444 +  (with priority \<open>p\<^sub>i\<close>), and the result category is determined from \<open>\<tau>\<close> (with
   1.445 +  priority \<open>p\<close>). Priority specifications are optional, with default 0 for
   1.446 +  arguments and 1000 for the result.\<^footnote>\<open>Omitting priorities is prone to
   1.447 +  syntactic ambiguities unless the delimiter tokens determine fully bracketed
   1.448 +  notation, as in \<open>if _ then _ else _ fi\<close>.\<close>
   1.449  
   1.450 -  Since \<open>\<tau>\<close> may be again a function type, the constant
   1.451 -  type scheme may have more argument positions than the mixfix
   1.452 -  pattern.  Printing a nested application \<open>c t\<^sub>1 \<dots> t\<^sub>m\<close> for
   1.453 -  \<open>m > n\<close> works by attaching concrete notation only to the
   1.454 -  innermost part, essentially by printing \<open>(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m\<close>
   1.455 -  instead.  If a term has fewer arguments than specified in the mixfix
   1.456 +  Since \<open>\<tau>\<close> may be again a function type, the constant type scheme may have
   1.457 +  more argument positions than the mixfix pattern. Printing a nested
   1.458 +  application \<open>c t\<^sub>1 \<dots> t\<^sub>m\<close> for \<open>m > n\<close> works by attaching concrete notation
   1.459 +  only to the innermost part, essentially by printing \<open>(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m\<close>
   1.460 +  instead. If a term has fewer arguments than specified in the mixfix
   1.461    template, the concrete syntax is ignored.
   1.462  
   1.463    \<^medskip>
   1.464 -  A mixfix template may also contain additional directives
   1.465 -  for pretty printing, notably spaces, blocks, and breaks.  The
   1.466 -  general template format is a sequence over any of the following
   1.467 -  entities.
   1.468 +  A mixfix template may also contain additional directives for pretty
   1.469 +  printing, notably spaces, blocks, and breaks. The general template format is
   1.470 +  a sequence over any of the following entities.
   1.471  
   1.472 -  \<^descr> \<open>d\<close> is a delimiter, namely a non-empty sequence of
   1.473 -  characters other than the following special characters:
   1.474 +  \<^descr> \<open>d\<close> is a delimiter, namely a non-empty sequence of characters other than
   1.475 +  the following special characters:
   1.476  
   1.477    \<^medskip>
   1.478    \begin{tabular}{ll}
   1.479 @@ -369,47 +345,45 @@
   1.480    \end{tabular}
   1.481    \<^medskip>
   1.482  
   1.483 -  \<^descr> \<^verbatim>\<open>'\<close> escapes the special meaning of these
   1.484 -  meta-characters, producing a literal version of the following
   1.485 -  character, unless that is a blank.
   1.486 +  \<^descr> \<^verbatim>\<open>'\<close> escapes the special meaning of these meta-characters, producing a
   1.487 +  literal version of the following character, unless that is a blank.
   1.488  
   1.489 -  A single quote followed by a blank separates delimiters, without
   1.490 -  affecting printing, but input tokens may have additional white space
   1.491 -  here.
   1.492 +  A single quote followed by a blank separates delimiters, without affecting
   1.493 +  printing, but input tokens may have additional white space here.
   1.494  
   1.495 -  \<^descr> \<^verbatim>\<open>_\<close> is an argument position, which stands for a
   1.496 -  certain syntactic category in the underlying grammar.
   1.497 +  \<^descr> \<^verbatim>\<open>_\<close> is an argument position, which stands for a certain syntactic
   1.498 +  category in the underlying grammar.
   1.499  
   1.500 -  \<^descr> \<open>\<index>\<close> is an indexed argument position; this is the place
   1.501 -  where implicit structure arguments can be attached.
   1.502 -
   1.503 -  \<^descr> \<open>s\<close> is a non-empty sequence of spaces for printing.
   1.504 -  This and the following specifications do not affect parsing at all.
   1.505 +  \<^descr> \<open>\<index>\<close> is an indexed argument position; this is the place where implicit
   1.506 +  structure arguments can be attached.
   1.507  
   1.508 -  \<^descr> \<^verbatim>\<open>(\<close>\<open>n\<close> opens a pretty printing block.  The
   1.509 -  optional number specifies how much indentation to add when a line
   1.510 -  break occurs within the block.  If the parenthesis is not followed
   1.511 -  by digits, the indentation defaults to 0.  A block specified via
   1.512 -  \<^verbatim>\<open>(00\<close> is unbreakable.
   1.513 +  \<^descr> \<open>s\<close> is a non-empty sequence of spaces for printing. This and the following
   1.514 +  specifications do not affect parsing at all.
   1.515 +
   1.516 +  \<^descr> \<^verbatim>\<open>(\<close>\<open>n\<close> opens a pretty printing block. The optional number specifies how
   1.517 +  much indentation to add when a line break occurs within the block. If the
   1.518 +  parenthesis is not followed by digits, the indentation defaults to 0. A
   1.519 +  block specified via \<^verbatim>\<open>(00\<close> is unbreakable.
   1.520  
   1.521    \<^descr> \<^verbatim>\<open>)\<close> closes a pretty printing block.
   1.522  
   1.523    \<^descr> \<^verbatim>\<open>//\<close> forces a line break.
   1.524  
   1.525 -  \<^descr> \<^verbatim>\<open>/\<close>\<open>s\<close> allows a line break.  Here \<open>s\<close>
   1.526 -  stands for the string of spaces (zero or more) right after the
   1.527 -  slash.  These spaces are printed if the break is \<^emph>\<open>not\<close> taken.
   1.528 +  \<^descr> \<^verbatim>\<open>/\<close>\<open>s\<close> allows a line break. Here \<open>s\<close> stands for the string of spaces
   1.529 +  (zero or more) right after the slash. These spaces are printed if the break
   1.530 +  is \<^emph>\<open>not\<close> taken.
   1.531  
   1.532  
   1.533 -  The general idea of pretty printing with blocks and breaks is also
   1.534 -  described in @{cite "paulson-ml2"}; it goes back to @{cite "Oppen:1980"}.
   1.535 +  The general idea of pretty printing with blocks and breaks is also described
   1.536 +  in @{cite "paulson-ml2"}; it goes back to @{cite "Oppen:1980"}.
   1.537  \<close>
   1.538  
   1.539  
   1.540  subsection \<open>Infixes\<close>
   1.541  
   1.542 -text \<open>Infix operators are specified by convenient short forms that
   1.543 -  abbreviate general mixfix annotations as follows:
   1.544 +text \<open>
   1.545 +  Infix operators are specified by convenient short forms that abbreviate
   1.546 +  general mixfix annotations as follows:
   1.547  
   1.548    \begin{center}
   1.549    \begin{tabular}{lll}
   1.550 @@ -427,35 +401,33 @@
   1.551    \end{tabular}
   1.552    \end{center}
   1.553  
   1.554 -  The mixfix template \<^verbatim>\<open>"(_\<close>~\<open>sy\<close>\<^verbatim>\<open>/ _)"\<close>
   1.555 -  specifies two argument positions; the delimiter is preceded by a
   1.556 -  space and followed by a space or line break; the entire phrase is a
   1.557 -  pretty printing block.
   1.558 +  The mixfix template \<^verbatim>\<open>"(_\<close>~\<open>sy\<close>\<^verbatim>\<open>/ _)"\<close> specifies two argument positions;
   1.559 +  the delimiter is preceded by a space and followed by a space or line break;
   1.560 +  the entire phrase is a pretty printing block.
   1.561  
   1.562 -  The alternative notation \<^verbatim>\<open>op\<close>~\<open>sy\<close> is introduced
   1.563 -  in addition.  Thus any infix operator may be written in prefix form
   1.564 -  (as in ML), independently of the number of arguments in the term.
   1.565 +  The alternative notation \<^verbatim>\<open>op\<close>~\<open>sy\<close> is introduced in addition. Thus any
   1.566 +  infix operator may be written in prefix form (as in ML), independently of
   1.567 +  the number of arguments in the term.
   1.568  \<close>
   1.569  
   1.570  
   1.571  subsection \<open>Binders\<close>
   1.572  
   1.573 -text \<open>A \<^emph>\<open>binder\<close> is a variable-binding construct such as a
   1.574 -  quantifier.  The idea to formalize \<open>\<forall>x. b\<close> as \<open>All
   1.575 -  (\<lambda>x. b)\<close> for \<open>All :: ('a \<Rightarrow> bool) \<Rightarrow> bool\<close> already goes back
   1.576 -  to @{cite church40}.  Isabelle declarations of certain higher-order
   1.577 -  operators may be annotated with @{keyword_def "binder"} annotations
   1.578 -  as follows:
   1.579 +text \<open>
   1.580 +  A \<^emph>\<open>binder\<close> is a variable-binding construct such as a quantifier. The idea
   1.581 +  to formalize \<open>\<forall>x. b\<close> as \<open>All (\<lambda>x. b)\<close> for \<open>All :: ('a \<Rightarrow> bool) \<Rightarrow> bool\<close>
   1.582 +  already goes back to @{cite church40}. Isabelle declarations of certain
   1.583 +  higher-order operators may be annotated with @{keyword_def "binder"}
   1.584 +  annotations as follows:
   1.585  
   1.586    \begin{center}
   1.587    \<open>c ::\<close>~\<^verbatim>\<open>"\<close>\<open>(\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2) \<Rightarrow> \<tau>\<^sub>3\<close>\<^verbatim>\<open>"  (\<close>@{keyword "binder"}~\<^verbatim>\<open>"\<close>\<open>sy\<close>\<^verbatim>\<open>" [\<close>\<open>p\<close>\<^verbatim>\<open>]\<close>~\<open>q\<close>\<^verbatim>\<open>)\<close>
   1.588    \end{center}
   1.589  
   1.590 -  This introduces concrete binder syntax \<open>sy x. b\<close>, where
   1.591 -  \<open>x\<close> is a bound variable of type \<open>\<tau>\<^sub>1\<close>, the body \<open>b\<close> has type \<open>\<tau>\<^sub>2\<close> and the whole term has type \<open>\<tau>\<^sub>3\<close>.
   1.592 -  The optional integer \<open>p\<close> specifies the syntactic priority of
   1.593 -  the body; the default is \<open>q\<close>, which is also the priority of
   1.594 -  the whole construct.
   1.595 +  This introduces concrete binder syntax \<open>sy x. b\<close>, where \<open>x\<close> is a bound
   1.596 +  variable of type \<open>\<tau>\<^sub>1\<close>, the body \<open>b\<close> has type \<open>\<tau>\<^sub>2\<close> and the whole term has
   1.597 +  type \<open>\<tau>\<^sub>3\<close>. The optional integer \<open>p\<close> specifies the syntactic priority of the
   1.598 +  body; the default is \<open>q\<close>, which is also the priority of the whole construct.
   1.599  
   1.600    Internally, the binder syntax is expanded to something like this:
   1.601    \begin{center}
   1.602 @@ -464,17 +436,18 @@
   1.603  
   1.604    Here @{syntax (inner) idts} is the nonterminal symbol for a list of
   1.605    identifiers with optional type constraints (see also
   1.606 -  \secref{sec:pure-grammar}).  The mixfix template \<^verbatim>\<open>"(3\<close>\<open>sy\<close>\<^verbatim>\<open>_./ _)"\<close>
   1.607 -  defines argument positions
   1.608 -  for the bound identifiers and the body, separated by a dot with
   1.609 -  optional line break; the entire phrase is a pretty printing block of
   1.610 -  indentation level 3.  Note that there is no extra space after \<open>sy\<close>, so it needs to be included user specification if the binder
   1.611 -  syntax ends with a token that may be continued by an identifier
   1.612 -  token at the start of @{syntax (inner) idts}.
   1.613 +  \secref{sec:pure-grammar}). The mixfix template \<^verbatim>\<open>"(3\<close>\<open>sy\<close>\<^verbatim>\<open>_./ _)"\<close> defines
   1.614 +  argument positions for the bound identifiers and the body, separated by a
   1.615 +  dot with optional line break; the entire phrase is a pretty printing block
   1.616 +  of indentation level 3. Note that there is no extra space after \<open>sy\<close>, so it
   1.617 +  needs to be included user specification if the binder syntax ends with a
   1.618 +  token that may be continued by an identifier token at the start of @{syntax
   1.619 +  (inner) idts}.
   1.620  
   1.621 -  Furthermore, a syntax translation to transforms \<open>c_binder x\<^sub>1
   1.622 -  \<dots> x\<^sub>n b\<close> into iterated application \<open>c (\<lambda>x\<^sub>1. \<dots> c (\<lambda>x\<^sub>n. b)\<dots>)\<close>.
   1.623 -  This works in both directions, for parsing and printing.\<close>
   1.624 +  Furthermore, a syntax translation to transforms \<open>c_binder x\<^sub>1 \<dots> x\<^sub>n b\<close> into
   1.625 +  iterated application \<open>c (\<lambda>x\<^sub>1. \<dots> c (\<lambda>x\<^sub>n. b)\<dots>)\<close>. This works in both
   1.626 +  directions, for parsing and printing.
   1.627 +\<close>
   1.628  
   1.629  
   1.630  section \<open>Explicit notation \label{sec:notation}\<close>
   1.631 @@ -488,12 +461,11 @@
   1.632      @{command_def "write"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
   1.633    \end{matharray}
   1.634  
   1.635 -  Commands that introduce new logical entities (terms or types)
   1.636 -  usually allow to provide mixfix annotations on the spot, which is
   1.637 -  convenient for default notation.  Nonetheless, the syntax may be
   1.638 -  modified later on by declarations for explicit notation.  This
   1.639 -  allows to add or delete mixfix annotations for of existing logical
   1.640 -  entities within the current context.
   1.641 +  Commands that introduce new logical entities (terms or types) usually allow
   1.642 +  to provide mixfix annotations on the spot, which is convenient for default
   1.643 +  notation. Nonetheless, the syntax may be modified later on by declarations
   1.644 +  for explicit notation. This allows to add or delete mixfix annotations for
   1.645 +  of existing logical entities within the current context.
   1.646  
   1.647    @{rail \<open>
   1.648      (@@{command type_notation} | @@{command no_type_notation}) @{syntax mode}? \<newline>
   1.649 @@ -505,24 +477,22 @@
   1.650      @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and')
   1.651    \<close>}
   1.652  
   1.653 -  \<^descr> @{command "type_notation"}~\<open>c (mx)\<close> associates mixfix
   1.654 -  syntax with an existing type constructor.  The arity of the
   1.655 -  constructor is retrieved from the context.
   1.656 +  \<^descr> @{command "type_notation"}~\<open>c (mx)\<close> associates mixfix syntax with an
   1.657 +  existing type constructor. The arity of the constructor is retrieved from
   1.658 +  the context.
   1.659  
   1.660 -  \<^descr> @{command "no_type_notation"} is similar to @{command
   1.661 -  "type_notation"}, but removes the specified syntax annotation from
   1.662 -  the present context.
   1.663 +  \<^descr> @{command "no_type_notation"} is similar to @{command "type_notation"},
   1.664 +  but removes the specified syntax annotation from the present context.
   1.665  
   1.666 -  \<^descr> @{command "notation"}~\<open>c (mx)\<close> associates mixfix
   1.667 -  syntax with an existing constant or fixed variable.  The type
   1.668 -  declaration of the given entity is retrieved from the context.
   1.669 +  \<^descr> @{command "notation"}~\<open>c (mx)\<close> associates mixfix syntax with an existing
   1.670 +  constant or fixed variable. The type declaration of the given entity is
   1.671 +  retrieved from the context.
   1.672  
   1.673 -  \<^descr> @{command "no_notation"} is similar to @{command "notation"},
   1.674 -  but removes the specified syntax annotation from the present
   1.675 -  context.
   1.676 +  \<^descr> @{command "no_notation"} is similar to @{command "notation"}, but removes
   1.677 +  the specified syntax annotation from the present context.
   1.678  
   1.679 -  \<^descr> @{command "write"} is similar to @{command "notation"}, but
   1.680 -  works within an Isar proof body.
   1.681 +  \<^descr> @{command "write"} is similar to @{command "notation"}, but works within
   1.682 +  an Isar proof body.
   1.683  \<close>
   1.684  
   1.685  
   1.686 @@ -530,26 +500,24 @@
   1.687  
   1.688  subsection \<open>Lexical matters \label{sec:inner-lex}\<close>
   1.689  
   1.690 -text \<open>The inner lexical syntax vaguely resembles the outer one
   1.691 -  (\secref{sec:outer-lex}), but some details are different.  There are
   1.692 -  two main categories of inner syntax tokens:
   1.693 +text \<open>
   1.694 +  The inner lexical syntax vaguely resembles the outer one
   1.695 +  (\secref{sec:outer-lex}), but some details are different. There are two main
   1.696 +  categories of inner syntax tokens:
   1.697  
   1.698 -  \<^enum> \<^emph>\<open>delimiters\<close> --- the literal tokens occurring in
   1.699 -  productions of the given priority grammar (cf.\
   1.700 -  \secref{sec:priority-grammar});
   1.701 +  \<^enum> \<^emph>\<open>delimiters\<close> --- the literal tokens occurring in productions of the given
   1.702 +  priority grammar (cf.\ \secref{sec:priority-grammar});
   1.703  
   1.704    \<^enum> \<^emph>\<open>named tokens\<close> --- various categories of identifiers etc.
   1.705  
   1.706  
   1.707 -  Delimiters override named tokens and may thus render certain
   1.708 -  identifiers inaccessible.  Sometimes the logical context admits
   1.709 -  alternative ways to refer to the same entity, potentially via
   1.710 -  qualified names.
   1.711 +  Delimiters override named tokens and may thus render certain identifiers
   1.712 +  inaccessible. Sometimes the logical context admits alternative ways to refer
   1.713 +  to the same entity, potentially via qualified names.
   1.714  
   1.715    \<^medskip>
   1.716 -  The categories for named tokens are defined once and for
   1.717 -  all as follows, reusing some categories of the outer token syntax
   1.718 -  (\secref{sec:outer-lex}).
   1.719 +  The categories for named tokens are defined once and for all as follows,
   1.720 +  reusing some categories of the outer token syntax (\secref{sec:outer-lex}).
   1.721  
   1.722    \begin{center}
   1.723    \begin{supertabular}{rcl}
   1.724 @@ -581,32 +549,30 @@
   1.725  
   1.726  subsection \<open>Priority grammars \label{sec:priority-grammar}\<close>
   1.727  
   1.728 -text \<open>A context-free grammar consists of a set of \<^emph>\<open>terminal
   1.729 -  symbols\<close>, a set of \<^emph>\<open>nonterminal symbols\<close> and a set of
   1.730 -  \<^emph>\<open>productions\<close>.  Productions have the form \<open>A = \<gamma>\<close>,
   1.731 -  where \<open>A\<close> is a nonterminal and \<open>\<gamma>\<close> is a string of
   1.732 -  terminals and nonterminals.  One designated nonterminal is called
   1.733 -  the \<^emph>\<open>root symbol\<close>.  The language defined by the grammar
   1.734 -  consists of all strings of terminals that can be derived from the
   1.735 -  root symbol by applying productions as rewrite rules.
   1.736 +text \<open>
   1.737 +  A context-free grammar consists of a set of \<^emph>\<open>terminal symbols\<close>, a set of
   1.738 +  \<^emph>\<open>nonterminal symbols\<close> and a set of \<^emph>\<open>productions\<close>. Productions have the
   1.739 +  form \<open>A = \<gamma>\<close>, where \<open>A\<close> is a nonterminal and \<open>\<gamma>\<close> is a string of terminals
   1.740 +  and nonterminals. One designated nonterminal is called the \<^emph>\<open>root symbol\<close>.
   1.741 +  The language defined by the grammar consists of all strings of terminals
   1.742 +  that can be derived from the root symbol by applying productions as rewrite
   1.743 +  rules.
   1.744  
   1.745 -  The standard Isabelle parser for inner syntax uses a \<^emph>\<open>priority
   1.746 -  grammar\<close>.  Each nonterminal is decorated by an integer priority:
   1.747 -  \<open>A\<^sup>(\<^sup>p\<^sup>)\<close>.  In a derivation, \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> may be rewritten
   1.748 -  using a production \<open>A\<^sup>(\<^sup>q\<^sup>) = \<gamma>\<close> only if \<open>p \<le> q\<close>.  Any
   1.749 -  priority grammar can be translated into a normal context-free
   1.750 -  grammar by introducing new nonterminals and productions.
   1.751 +  The standard Isabelle parser for inner syntax uses a \<^emph>\<open>priority grammar\<close>.
   1.752 +  Each nonterminal is decorated by an integer priority: \<open>A\<^sup>(\<^sup>p\<^sup>)\<close>. In a
   1.753 +  derivation, \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> may be rewritten using a production \<open>A\<^sup>(\<^sup>q\<^sup>) = \<gamma>\<close> only
   1.754 +  if \<open>p \<le> q\<close>. Any priority grammar can be translated into a normal
   1.755 +  context-free grammar by introducing new nonterminals and productions.
   1.756  
   1.757    \<^medskip>
   1.758 -  Formally, a set of context free productions \<open>G\<close>
   1.759 -  induces a derivation relation \<open>\<longrightarrow>\<^sub>G\<close> as follows.  Let \<open>\<alpha>\<close> and \<open>\<beta>\<close> denote strings of terminal or nonterminal symbols.
   1.760 -  Then \<open>\<alpha> A\<^sup>(\<^sup>p\<^sup>) \<beta> \<longrightarrow>\<^sub>G \<alpha> \<gamma> \<beta>\<close> holds if and only if \<open>G\<close>
   1.761 +  Formally, a set of context free productions \<open>G\<close> induces a derivation
   1.762 +  relation \<open>\<longrightarrow>\<^sub>G\<close> as follows. Let \<open>\<alpha>\<close> and \<open>\<beta>\<close> denote strings of terminal or
   1.763 +  nonterminal symbols. Then \<open>\<alpha> A\<^sup>(\<^sup>p\<^sup>) \<beta> \<longrightarrow>\<^sub>G \<alpha> \<gamma> \<beta>\<close> holds if and only if \<open>G\<close>
   1.764    contains some production \<open>A\<^sup>(\<^sup>q\<^sup>) = \<gamma>\<close> for \<open>p \<le> q\<close>.
   1.765  
   1.766    \<^medskip>
   1.767 -  The following grammar for arithmetic expressions
   1.768 -  demonstrates how binding power and associativity of operators can be
   1.769 -  enforced by priorities.
   1.770 +  The following grammar for arithmetic expressions demonstrates how binding
   1.771 +  power and associativity of operators can be enforced by priorities.
   1.772  
   1.773    \begin{center}
   1.774    \begin{tabular}{rclr}
   1.775 @@ -617,28 +583,25 @@
   1.776    \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>=\<close> & \<^verbatim>\<open>-\<close> \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> \\
   1.777    \end{tabular}
   1.778    \end{center}
   1.779 -  The choice of priorities determines that \<^verbatim>\<open>-\<close> binds
   1.780 -  tighter than \<^verbatim>\<open>*\<close>, which binds tighter than \<^verbatim>\<open>+\<close>.
   1.781 -  Furthermore \<^verbatim>\<open>+\<close> associates to the left and
   1.782 -  \<^verbatim>\<open>*\<close> to the right.
   1.783 +  The choice of priorities determines that \<^verbatim>\<open>-\<close> binds tighter than \<^verbatim>\<open>*\<close>, which
   1.784 +  binds tighter than \<^verbatim>\<open>+\<close>. Furthermore \<^verbatim>\<open>+\<close> associates to the left and \<^verbatim>\<open>*\<close> to
   1.785 +  the right.
   1.786  
   1.787    \<^medskip>
   1.788    For clarity, grammars obey these conventions:
   1.789  
   1.790 -  \<^item> All priorities must lie between 0 and 1000.
   1.791 +    \<^item> All priorities must lie between 0 and 1000.
   1.792  
   1.793 -  \<^item> Priority 0 on the right-hand side and priority 1000 on the
   1.794 -  left-hand side may be omitted.
   1.795 +    \<^item> Priority 0 on the right-hand side and priority 1000 on the left-hand
   1.796 +    side may be omitted.
   1.797  
   1.798 -  \<^item> The production \<open>A\<^sup>(\<^sup>p\<^sup>) = \<alpha>\<close> is written as \<open>A = \<alpha>
   1.799 -  (p)\<close>, i.e.\ the priority of the left-hand side actually appears in
   1.800 -  a column on the far right.
   1.801 +    \<^item> The production \<open>A\<^sup>(\<^sup>p\<^sup>) = \<alpha>\<close> is written as \<open>A = \<alpha> (p)\<close>, i.e.\ the
   1.802 +    priority of the left-hand side actually appears in a column on the far
   1.803 +    right.
   1.804  
   1.805 -  \<^item> Alternatives are separated by \<open>|\<close>.
   1.806 +    \<^item> Alternatives are separated by \<open>|\<close>.
   1.807  
   1.808 -  \<^item> Repetition is indicated by dots \<open>(\<dots>)\<close> in an informal
   1.809 -  but obvious way.
   1.810 -
   1.811 +    \<^item> Repetition is indicated by dots \<open>(\<dots>)\<close> in an informal but obvious way.
   1.812  
   1.813    Using these conventions, the example grammar specification above
   1.814    takes the form:
   1.815 @@ -656,8 +619,9 @@
   1.816  
   1.817  subsection \<open>The Pure grammar \label{sec:pure-grammar}\<close>
   1.818  
   1.819 -text \<open>The priority grammar of the \<open>Pure\<close> theory is defined
   1.820 -  approximately like this:
   1.821 +text \<open>
   1.822 +  The priority grammar of the \<open>Pure\<close> theory is defined approximately like
   1.823 +  this:
   1.824  
   1.825    \begin{center}
   1.826    \begin{supertabular}{rclr}
   1.827 @@ -729,55 +693,54 @@
   1.828    \end{center}
   1.829  
   1.830    \<^medskip>
   1.831 -  Here literal terminals are printed \<^verbatim>\<open>verbatim\<close>;
   1.832 -  see also \secref{sec:inner-lex} for further token categories of the
   1.833 -  inner syntax.  The meaning of the nonterminals defined by the above
   1.834 -  grammar is as follows:
   1.835 +  Here literal terminals are printed \<^verbatim>\<open>verbatim\<close>; see also
   1.836 +  \secref{sec:inner-lex} for further token categories of the inner syntax. The
   1.837 +  meaning of the nonterminals defined by the above grammar is as follows:
   1.838  
   1.839    \<^descr> @{syntax_ref (inner) any} denotes any term.
   1.840  
   1.841 -  \<^descr> @{syntax_ref (inner) prop} denotes meta-level propositions,
   1.842 -  which are terms of type @{typ prop}.  The syntax of such formulae of
   1.843 -  the meta-logic is carefully distinguished from usual conventions for
   1.844 -  object-logics.  In particular, plain \<open>\<lambda>\<close>-term notation is
   1.845 -  \<^emph>\<open>not\<close> recognized as @{syntax (inner) prop}.
   1.846 +  \<^descr> @{syntax_ref (inner) prop} denotes meta-level propositions, which are
   1.847 +  terms of type @{typ prop}. The syntax of such formulae of the meta-logic is
   1.848 +  carefully distinguished from usual conventions for object-logics. In
   1.849 +  particular, plain \<open>\<lambda>\<close>-term notation is \<^emph>\<open>not\<close> recognized as @{syntax (inner)
   1.850 +  prop}.
   1.851  
   1.852 -  \<^descr> @{syntax_ref (inner) aprop} denotes atomic propositions, which
   1.853 -  are embedded into regular @{syntax (inner) prop} by means of an
   1.854 -  explicit \<^verbatim>\<open>PROP\<close> token.
   1.855 +  \<^descr> @{syntax_ref (inner) aprop} denotes atomic propositions, which are
   1.856 +  embedded into regular @{syntax (inner) prop} by means of an explicit \<^verbatim>\<open>PROP\<close>
   1.857 +  token.
   1.858  
   1.859 -  Terms of type @{typ prop} with non-constant head, e.g.\ a plain
   1.860 -  variable, are printed in this form.  Constants that yield type @{typ
   1.861 -  prop} are expected to provide their own concrete syntax; otherwise
   1.862 -  the printed version will appear like @{syntax (inner) logic} and
   1.863 -  cannot be parsed again as @{syntax (inner) prop}.
   1.864 +  Terms of type @{typ prop} with non-constant head, e.g.\ a plain variable,
   1.865 +  are printed in this form. Constants that yield type @{typ prop} are expected
   1.866 +  to provide their own concrete syntax; otherwise the printed version will
   1.867 +  appear like @{syntax (inner) logic} and cannot be parsed again as @{syntax
   1.868 +  (inner) prop}.
   1.869  
   1.870 -  \<^descr> @{syntax_ref (inner) logic} denotes arbitrary terms of a
   1.871 -  logical type, excluding type @{typ prop}.  This is the main
   1.872 -  syntactic category of object-logic entities, covering plain \<open>\<lambda>\<close>-term notation (variables, abstraction, application), plus
   1.873 -  anything defined by the user.
   1.874 +  \<^descr> @{syntax_ref (inner) logic} denotes arbitrary terms of a logical type,
   1.875 +  excluding type @{typ prop}. This is the main syntactic category of
   1.876 +  object-logic entities, covering plain \<open>\<lambda>\<close>-term notation (variables,
   1.877 +  abstraction, application), plus anything defined by the user.
   1.878  
   1.879 -  When specifying notation for logical entities, all logical types
   1.880 -  (excluding @{typ prop}) are \<^emph>\<open>collapsed\<close> to this single category
   1.881 -  of @{syntax (inner) logic}.
   1.882 +  When specifying notation for logical entities, all logical types (excluding
   1.883 +  @{typ prop}) are \<^emph>\<open>collapsed\<close> to this single category of @{syntax (inner)
   1.884 +  logic}.
   1.885  
   1.886 -  \<^descr> @{syntax_ref (inner) index} denotes an optional index term for
   1.887 -  indexed syntax.  If omitted, it refers to the first @{keyword_ref
   1.888 -  "structure"} variable in the context.  The special dummy ``\<open>\<index>\<close>'' serves as pattern variable in mixfix annotations that
   1.889 -  introduce indexed notation.
   1.890 +  \<^descr> @{syntax_ref (inner) index} denotes an optional index term for indexed
   1.891 +  syntax. If omitted, it refers to the first @{keyword_ref "structure"}
   1.892 +  variable in the context. The special dummy ``\<open>\<index>\<close>'' serves as pattern
   1.893 +  variable in mixfix annotations that introduce indexed notation.
   1.894  
   1.895 -  \<^descr> @{syntax_ref (inner) idt} denotes identifiers, possibly
   1.896 -  constrained by types.
   1.897 +  \<^descr> @{syntax_ref (inner) idt} denotes identifiers, possibly constrained by
   1.898 +  types.
   1.899  
   1.900 -  \<^descr> @{syntax_ref (inner) idts} denotes a sequence of @{syntax_ref
   1.901 -  (inner) idt}.  This is the most basic category for variables in
   1.902 -  iterated binders, such as \<open>\<lambda>\<close> or \<open>\<And>\<close>.
   1.903 +  \<^descr> @{syntax_ref (inner) idts} denotes a sequence of @{syntax_ref (inner)
   1.904 +  idt}. This is the most basic category for variables in iterated binders,
   1.905 +  such as \<open>\<lambda>\<close> or \<open>\<And>\<close>.
   1.906  
   1.907 -  \<^descr> @{syntax_ref (inner) pttrn} and @{syntax_ref (inner) pttrns}
   1.908 -  denote patterns for abstraction, cases bindings etc.  In Pure, these
   1.909 -  categories start as a merely copy of @{syntax (inner) idt} and
   1.910 -  @{syntax (inner) idts}, respectively.  Object-logics may add
   1.911 -  additional productions for binding forms.
   1.912 +  \<^descr> @{syntax_ref (inner) pttrn} and @{syntax_ref (inner) pttrns} denote
   1.913 +  patterns for abstraction, cases bindings etc. In Pure, these categories
   1.914 +  start as a merely copy of @{syntax (inner) idt} and @{syntax (inner) idts},
   1.915 +  respectively. Object-logics may add additional productions for binding
   1.916 +  forms.
   1.917  
   1.918    \<^descr> @{syntax_ref (inner) type} denotes types of the meta-logic.
   1.919  
   1.920 @@ -786,58 +749,52 @@
   1.921  
   1.922    Here are some further explanations of certain syntax features.
   1.923  
   1.924 -  \<^item> In @{syntax (inner) idts}, note that \<open>x :: nat y\<close> is
   1.925 -  parsed as \<open>x :: (nat y)\<close>, treating \<open>y\<close> like a type
   1.926 -  constructor applied to \<open>nat\<close>.  To avoid this interpretation,
   1.927 -  write \<open>(x :: nat) y\<close> with explicit parentheses.
   1.928 +  \<^item> In @{syntax (inner) idts}, note that \<open>x :: nat y\<close> is parsed as \<open>x :: (nat
   1.929 +  y)\<close>, treating \<open>y\<close> like a type constructor applied to \<open>nat\<close>. To avoid this
   1.930 +  interpretation, write \<open>(x :: nat) y\<close> with explicit parentheses.
   1.931  
   1.932 -  \<^item> Similarly, \<open>x :: nat y :: nat\<close> is parsed as \<open>x ::
   1.933 -  (nat y :: nat)\<close>.  The correct form is \<open>(x :: nat) (y ::
   1.934 -  nat)\<close>, or \<open>(x :: nat) y :: nat\<close> if \<open>y\<close> is last in the
   1.935 -  sequence of identifiers.
   1.936 +  \<^item> Similarly, \<open>x :: nat y :: nat\<close> is parsed as \<open>x :: (nat y :: nat)\<close>. The
   1.937 +  correct form is \<open>(x :: nat) (y :: nat)\<close>, or \<open>(x :: nat) y :: nat\<close> if \<open>y\<close> is
   1.938 +  last in the sequence of identifiers.
   1.939  
   1.940 -  \<^item> Type constraints for terms bind very weakly.  For example,
   1.941 -  \<open>x < y :: nat\<close> is normally parsed as \<open>(x < y) ::
   1.942 -  nat\<close>, unless \<open><\<close> has a very low priority, in which case the
   1.943 -  input is likely to be ambiguous.  The correct form is \<open>x < (y
   1.944 -  :: nat)\<close>.
   1.945 +  \<^item> Type constraints for terms bind very weakly. For example, \<open>x < y :: nat\<close>
   1.946 +  is normally parsed as \<open>(x < y) :: nat\<close>, unless \<open><\<close> has a very low priority,
   1.947 +  in which case the input is likely to be ambiguous. The correct form is \<open>x <
   1.948 +  (y :: nat)\<close>.
   1.949  
   1.950    \<^item> Dummy variables (written as underscore) may occur in different
   1.951    roles.
   1.952  
   1.953 -    \<^descr> A type ``\<open>_\<close>'' or ``\<open>_ :: sort\<close>'' acts like an
   1.954 -    anonymous inference parameter, which is filled-in according to the
   1.955 -    most general type produced by the type-checking phase.
   1.956 +    \<^descr> A type ``\<open>_\<close>'' or ``\<open>_ :: sort\<close>'' acts like an anonymous inference
   1.957 +    parameter, which is filled-in according to the most general type produced
   1.958 +    by the type-checking phase.
   1.959  
   1.960 -    \<^descr> A bound ``\<open>_\<close>'' refers to a vacuous abstraction, where
   1.961 -    the body does not refer to the binding introduced here.  As in the
   1.962 -    term @{term "\<lambda>x _. x"}, which is \<open>\<alpha>\<close>-equivalent to \<open>\<lambda>x y. x\<close>.
   1.963 +    \<^descr> A bound ``\<open>_\<close>'' refers to a vacuous abstraction, where the body does not
   1.964 +    refer to the binding introduced here. As in the term @{term "\<lambda>x _. x"},
   1.965 +    which is \<open>\<alpha>\<close>-equivalent to \<open>\<lambda>x y. x\<close>.
   1.966  
   1.967 -    \<^descr> A free ``\<open>_\<close>'' refers to an implicit outer binding.
   1.968 -    Higher definitional packages usually allow forms like \<open>f x _
   1.969 -    = x\<close>.
   1.970 +    \<^descr> A free ``\<open>_\<close>'' refers to an implicit outer binding. Higher definitional
   1.971 +    packages usually allow forms like \<open>f x _ = x\<close>.
   1.972  
   1.973 -    \<^descr> A schematic ``\<open>_\<close>'' (within a term pattern, see
   1.974 -    \secref{sec:term-decls}) refers to an anonymous variable that is
   1.975 -    implicitly abstracted over its context of locally bound variables.
   1.976 -    For example, this allows pattern matching of \<open>{x. f x = g
   1.977 -    x}\<close> against \<open>{x. _ = _}\<close>, or even \<open>{_. _ = _}\<close> by
   1.978 +    \<^descr> A schematic ``\<open>_\<close>'' (within a term pattern, see \secref{sec:term-decls})
   1.979 +    refers to an anonymous variable that is implicitly abstracted over its
   1.980 +    context of locally bound variables. For example, this allows pattern
   1.981 +    matching of \<open>{x. f x = g x}\<close> against \<open>{x. _ = _}\<close>, or even \<open>{_. _ = _}\<close> by
   1.982      using both bound and schematic dummies.
   1.983  
   1.984 -  \<^descr> The three literal dots ``\<^verbatim>\<open>...\<close>'' may be also
   1.985 -  written as ellipsis symbol \<^verbatim>\<open>\<dots>\<close>.  In both cases this
   1.986 -  refers to a special schematic variable, which is bound in the
   1.987 -  context.  This special term abbreviation works nicely with
   1.988 +  \<^descr> The three literal dots ``\<^verbatim>\<open>...\<close>'' may be also written as ellipsis symbol
   1.989 +  \<^verbatim>\<open>\<dots>\<close>. In both cases this refers to a special schematic variable, which is
   1.990 +  bound in the context. This special term abbreviation works nicely with
   1.991    calculational reasoning (\secref{sec:calculation}).
   1.992  
   1.993 -  \<^descr> \<^verbatim>\<open>CONST\<close> ensures that the given identifier is treated
   1.994 -  as constant term, and passed through the parse tree in fully
   1.995 -  internalized form.  This is particularly relevant for translation
   1.996 -  rules (\secref{sec:syn-trans}), notably on the RHS.
   1.997 +  \<^descr> \<^verbatim>\<open>CONST\<close> ensures that the given identifier is treated as constant term,
   1.998 +  and passed through the parse tree in fully internalized form. This is
   1.999 +  particularly relevant for translation rules (\secref{sec:syn-trans}),
  1.1000 +  notably on the RHS.
  1.1001  
  1.1002 -  \<^descr> \<^verbatim>\<open>XCONST\<close> is similar to \<^verbatim>\<open>CONST\<close>, but
  1.1003 -  retains the constant name as given.  This is only relevant to
  1.1004 -  translation rules (\secref{sec:syn-trans}), notably on the LHS.
  1.1005 +  \<^descr> \<^verbatim>\<open>XCONST\<close> is similar to \<^verbatim>\<open>CONST\<close>, but retains the constant name as given.
  1.1006 +  This is only relevant to translation rules (\secref{sec:syn-trans}), notably
  1.1007 +  on the LHS.
  1.1008  \<close>
  1.1009  
  1.1010  
  1.1011 @@ -848,46 +805,45 @@
  1.1012      @{command_def "print_syntax"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
  1.1013    \end{matharray}
  1.1014  
  1.1015 -  \<^descr> @{command "print_syntax"} prints the inner syntax of the
  1.1016 -  current context.  The output can be quite large; the most important
  1.1017 -  sections are explained below.
  1.1018 +  \<^descr> @{command "print_syntax"} prints the inner syntax of the current context.
  1.1019 +  The output can be quite large; the most important sections are explained
  1.1020 +  below.
  1.1021  
  1.1022 -    \<^descr> \<open>lexicon\<close> lists the delimiters of the inner token
  1.1023 -    language; see \secref{sec:inner-lex}.
  1.1024 -
  1.1025 -    \<^descr> \<open>prods\<close> lists the productions of the underlying
  1.1026 -    priority grammar; see \secref{sec:priority-grammar}.
  1.1027 +    \<^descr> \<open>lexicon\<close> lists the delimiters of the inner token language; see
  1.1028 +    \secref{sec:inner-lex}.
  1.1029  
  1.1030 -    The nonterminal \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is rendered in plain text as \<open>A[p]\<close>; delimiters are quoted.  Many productions have an extra
  1.1031 -    \<open>\<dots> => name\<close>.  These names later become the heads of parse
  1.1032 -    trees; they also guide the pretty printer.
  1.1033 +    \<^descr> \<open>prods\<close> lists the productions of the underlying priority grammar; see
  1.1034 +    \secref{sec:priority-grammar}.
  1.1035  
  1.1036 -    Productions without such parse tree names are called \<^emph>\<open>copy
  1.1037 -    productions\<close>.  Their right-hand side must have exactly one
  1.1038 -    nonterminal symbol (or named token).  The parser does not create a
  1.1039 -    new parse tree node for copy productions, but simply returns the
  1.1040 -    parse tree of the right-hand symbol.
  1.1041 +    The nonterminal \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is rendered in plain text as \<open>A[p]\<close>; delimiters
  1.1042 +    are quoted. Many productions have an extra \<open>\<dots> => name\<close>. These names later
  1.1043 +    become the heads of parse trees; they also guide the pretty printer.
  1.1044 +
  1.1045 +    Productions without such parse tree names are called \<^emph>\<open>copy productions\<close>.
  1.1046 +    Their right-hand side must have exactly one nonterminal symbol (or named
  1.1047 +    token). The parser does not create a new parse tree node for copy
  1.1048 +    productions, but simply returns the parse tree of the right-hand symbol.
  1.1049  
  1.1050      If the right-hand side of a copy production consists of a single
  1.1051      nonterminal without any delimiters, then it is called a \<^emph>\<open>chain
  1.1052 -    production\<close>.  Chain productions act as abbreviations: conceptually,
  1.1053 -    they are removed from the grammar by adding new productions.
  1.1054 -    Priority information attached to chain productions is ignored; only
  1.1055 -    the dummy value \<open>-1\<close> is displayed.
  1.1056 +    production\<close>. Chain productions act as abbreviations: conceptually, they
  1.1057 +    are removed from the grammar by adding new productions. Priority
  1.1058 +    information attached to chain productions is ignored; only the dummy value
  1.1059 +    \<open>-1\<close> is displayed.
  1.1060  
  1.1061 -    \<^descr> \<open>print modes\<close> lists the alternative print modes
  1.1062 -    provided by this grammar; see \secref{sec:print-modes}.
  1.1063 +    \<^descr> \<open>print modes\<close> lists the alternative print modes provided by this
  1.1064 +    grammar; see \secref{sec:print-modes}.
  1.1065  
  1.1066 -    \<^descr> \<open>parse_rules\<close> and \<open>print_rules\<close> relate to
  1.1067 -    syntax translations (macros); see \secref{sec:syn-trans}.
  1.1068 +    \<^descr> \<open>parse_rules\<close> and \<open>print_rules\<close> relate to syntax translations (macros);
  1.1069 +    see \secref{sec:syn-trans}.
  1.1070  
  1.1071 -    \<^descr> \<open>parse_ast_translation\<close> and \<open>print_ast_translation\<close> list sets of constants that invoke
  1.1072 -    translation functions for abstract syntax trees, which are only
  1.1073 -    required in very special situations; see \secref{sec:tr-funs}.
  1.1074 +    \<^descr> \<open>parse_ast_translation\<close> and \<open>print_ast_translation\<close> list sets of
  1.1075 +    constants that invoke translation functions for abstract syntax trees,
  1.1076 +    which are only required in very special situations; see
  1.1077 +    \secref{sec:tr-funs}.
  1.1078  
  1.1079 -    \<^descr> \<open>parse_translation\<close> and \<open>print_translation\<close>
  1.1080 -    list the sets of constants that invoke regular translation
  1.1081 -    functions; see \secref{sec:tr-funs}.
  1.1082 +    \<^descr> \<open>parse_translation\<close> and \<open>print_translation\<close> list the sets of constants
  1.1083 +    that invoke regular translation functions; see \secref{sec:tr-funs}.
  1.1084  \<close>
  1.1085  
  1.1086  
  1.1087 @@ -899,37 +855,36 @@
  1.1088      @{attribute_def syntax_ambiguity_limit} & : & \<open>attribute\<close> & default \<open>10\<close> \\
  1.1089    \end{tabular}
  1.1090  
  1.1091 -  Depending on the grammar and the given input, parsing may be
  1.1092 -  ambiguous.  Isabelle lets the Earley parser enumerate all possible
  1.1093 -  parse trees, and then tries to make the best out of the situation.
  1.1094 -  Terms that cannot be type-checked are filtered out, which often
  1.1095 -  leads to a unique result in the end.  Unlike regular type
  1.1096 -  reconstruction, which is applied to the whole collection of input
  1.1097 -  terms simultaneously, the filtering stage only treats each given
  1.1098 -  term in isolation.  Filtering is also not attempted for individual
  1.1099 +  Depending on the grammar and the given input, parsing may be ambiguous.
  1.1100 +  Isabelle lets the Earley parser enumerate all possible parse trees, and then
  1.1101 +  tries to make the best out of the situation. Terms that cannot be
  1.1102 +  type-checked are filtered out, which often leads to a unique result in the
  1.1103 +  end. Unlike regular type reconstruction, which is applied to the whole
  1.1104 +  collection of input terms simultaneously, the filtering stage only treats
  1.1105 +  each given term in isolation. Filtering is also not attempted for individual
  1.1106    types or raw ASTs (as required for @{command translations}).
  1.1107  
  1.1108 -  Certain warning or error messages are printed, depending on the
  1.1109 -  situation and the given configuration options.  Parsing ultimately
  1.1110 -  fails, if multiple results remain after the filtering phase.
  1.1111 +  Certain warning or error messages are printed, depending on the situation
  1.1112 +  and the given configuration options. Parsing ultimately fails, if multiple
  1.1113 +  results remain after the filtering phase.
  1.1114  
  1.1115 -  \<^descr> @{attribute syntax_ambiguity_warning} controls output of
  1.1116 -  explicit warning messages about syntax ambiguity.
  1.1117 +  \<^descr> @{attribute syntax_ambiguity_warning} controls output of explicit warning
  1.1118 +  messages about syntax ambiguity.
  1.1119  
  1.1120 -  \<^descr> @{attribute syntax_ambiguity_limit} determines the number of
  1.1121 -  resulting parse trees that are shown as part of the printed message
  1.1122 -  in case of an ambiguity.
  1.1123 +  \<^descr> @{attribute syntax_ambiguity_limit} determines the number of resulting
  1.1124 +  parse trees that are shown as part of the printed message in case of an
  1.1125 +  ambiguity.
  1.1126  \<close>
  1.1127  
  1.1128  
  1.1129  section \<open>Syntax transformations \label{sec:syntax-transformations}\<close>
  1.1130  
  1.1131 -text \<open>The inner syntax engine of Isabelle provides separate
  1.1132 -  mechanisms to transform parse trees either via rewrite systems on
  1.1133 -  first-order ASTs (\secref{sec:syn-trans}), or ML functions on ASTs
  1.1134 -  or syntactic \<open>\<lambda>\<close>-terms (\secref{sec:tr-funs}).  This works
  1.1135 -  both for parsing and printing, as outlined in
  1.1136 -  \figref{fig:parse-print}.
  1.1137 +text \<open>
  1.1138 +  The inner syntax engine of Isabelle provides separate mechanisms to
  1.1139 +  transform parse trees either via rewrite systems on first-order ASTs
  1.1140 +  (\secref{sec:syn-trans}), or ML functions on ASTs or syntactic \<open>\<lambda>\<close>-terms
  1.1141 +  (\secref{sec:tr-funs}). This works both for parsing and printing, as
  1.1142 +  outlined in \figref{fig:parse-print}.
  1.1143  
  1.1144    \begin{figure}[htbp]
  1.1145    \begin{center}
  1.1146 @@ -954,137 +909,129 @@
  1.1147    \caption{Parsing and printing with translations}\label{fig:parse-print}
  1.1148    \end{figure}
  1.1149  
  1.1150 -  These intermediate syntax tree formats eventually lead to a pre-term
  1.1151 -  with all names and binding scopes resolved, but most type
  1.1152 -  information still missing.  Explicit type constraints might be given by
  1.1153 -  the user, or implicit position information by the system --- both
  1.1154 -  need to be passed-through carefully by syntax transformations.
  1.1155 +  These intermediate syntax tree formats eventually lead to a pre-term with
  1.1156 +  all names and binding scopes resolved, but most type information still
  1.1157 +  missing. Explicit type constraints might be given by the user, or implicit
  1.1158 +  position information by the system --- both need to be passed-through
  1.1159 +  carefully by syntax transformations.
  1.1160  
  1.1161 -  Pre-terms are further processed by the so-called \<^emph>\<open>check\<close> and
  1.1162 -  \<^emph>\<open>uncheck\<close> phases that are intertwined with type-inference (see
  1.1163 -  also @{cite "isabelle-implementation"}).  The latter allows to operate
  1.1164 -  on higher-order abstract syntax with proper binding and type
  1.1165 -  information already available.
  1.1166 +  Pre-terms are further processed by the so-called \<^emph>\<open>check\<close> and \<^emph>\<open>uncheck\<close>
  1.1167 +  phases that are intertwined with type-inference (see also @{cite
  1.1168 +  "isabelle-implementation"}). The latter allows to operate on higher-order
  1.1169 +  abstract syntax with proper binding and type information already available.
  1.1170  
  1.1171 -  As a rule of thumb, anything that manipulates bindings of variables
  1.1172 -  or constants needs to be implemented as syntax transformation (see
  1.1173 -  below).  Anything else is better done via check/uncheck: a prominent
  1.1174 -  example application is the @{command abbreviation} concept of
  1.1175 -  Isabelle/Pure.\<close>
  1.1176 +  As a rule of thumb, anything that manipulates bindings of variables or
  1.1177 +  constants needs to be implemented as syntax transformation (see below).
  1.1178 +  Anything else is better done via check/uncheck: a prominent example
  1.1179 +  application is the @{command abbreviation} concept of Isabelle/Pure.
  1.1180 +\<close>
  1.1181  
  1.1182  
  1.1183  subsection \<open>Abstract syntax trees \label{sec:ast}\<close>
  1.1184  
  1.1185 -text \<open>The ML datatype @{ML_type Ast.ast} explicitly represents the
  1.1186 -  intermediate AST format that is used for syntax rewriting
  1.1187 -  (\secref{sec:syn-trans}).  It is defined in ML as follows:
  1.1188 +text \<open>
  1.1189 +  The ML datatype @{ML_type Ast.ast} explicitly represents the intermediate
  1.1190 +  AST format that is used for syntax rewriting (\secref{sec:syn-trans}). It is
  1.1191 +  defined in ML as follows:
  1.1192    @{verbatim [display]
  1.1193  \<open>datatype ast =
  1.1194    Constant of string |
  1.1195    Variable of string |
  1.1196    Appl of ast list\<close>}
  1.1197  
  1.1198 -  An AST is either an atom (constant or variable) or a list of (at
  1.1199 -  least two) subtrees.  Occasional diagnostic output of ASTs uses
  1.1200 -  notation that resembles S-expression of LISP.  Constant atoms are
  1.1201 -  shown as quoted strings, variable atoms as non-quoted strings and
  1.1202 -  applications as a parenthesized list of subtrees.  For example, the
  1.1203 -  AST
  1.1204 +  An AST is either an atom (constant or variable) or a list of (at least two)
  1.1205 +  subtrees. Occasional diagnostic output of ASTs uses notation that resembles
  1.1206 +  S-expression of LISP. Constant atoms are shown as quoted strings, variable
  1.1207 +  atoms as non-quoted strings and applications as a parenthesized list of
  1.1208 +  subtrees. For example, the AST
  1.1209    @{ML [display] \<open>Ast.Appl [Ast.Constant "_abs", Ast.Variable "x", Ast.Variable "t"]\<close>}
  1.1210 -  is pretty-printed as \<^verbatim>\<open>("_abs" x t)\<close>.  Note that
  1.1211 -  \<^verbatim>\<open>()\<close> and \<^verbatim>\<open>(x)\<close> are excluded as ASTs, because
  1.1212 -  they have too few subtrees.
  1.1213 +  is pretty-printed as \<^verbatim>\<open>("_abs" x t)\<close>. Note that \<^verbatim>\<open>()\<close> and \<^verbatim>\<open>(x)\<close> are
  1.1214 +  excluded as ASTs, because they have too few subtrees.
  1.1215  
  1.1216    \<^medskip>
  1.1217 -  AST application is merely a pro-forma mechanism to indicate
  1.1218 -  certain syntactic structures.  Thus \<^verbatim>\<open>(c a b)\<close> could mean
  1.1219 -  either term application or type application, depending on the
  1.1220 -  syntactic context.
  1.1221 +  AST application is merely a pro-forma mechanism to indicate certain
  1.1222 +  syntactic structures. Thus \<^verbatim>\<open>(c a b)\<close> could mean either term application or
  1.1223 +  type application, depending on the syntactic context.
  1.1224  
  1.1225 -  Nested application like \<^verbatim>\<open>(("_abs" x t) u)\<close> is also
  1.1226 -  possible, but ASTs are definitely first-order: the syntax constant
  1.1227 -  \<^verbatim>\<open>"_abs"\<close> does not bind the \<^verbatim>\<open>x\<close> in any way.
  1.1228 -  Proper bindings are introduced in later stages of the term syntax,
  1.1229 -  where \<^verbatim>\<open>("_abs" x t)\<close> becomes an @{ML Abs} node and
  1.1230 -  occurrences of \<^verbatim>\<open>x\<close> in \<^verbatim>\<open>t\<close> are replaced by bound
  1.1231 -  variables (represented as de-Bruijn indices).
  1.1232 +  Nested application like \<^verbatim>\<open>(("_abs" x t) u)\<close> is also possible, but ASTs are
  1.1233 +  definitely first-order: the syntax constant \<^verbatim>\<open>"_abs"\<close> does not bind the \<^verbatim>\<open>x\<close>
  1.1234 +  in any way. Proper bindings are introduced in later stages of the term
  1.1235 +  syntax, where \<^verbatim>\<open>("_abs" x t)\<close> becomes an @{ML Abs} node and occurrences of
  1.1236 +  \<^verbatim>\<open>x\<close> in \<^verbatim>\<open>t\<close> are replaced by bound variables (represented as de-Bruijn
  1.1237 +  indices).
  1.1238  \<close>
  1.1239  
  1.1240  
  1.1241  subsubsection \<open>AST constants versus variables\<close>
  1.1242  
  1.1243 -text \<open>Depending on the situation --- input syntax, output syntax,
  1.1244 -  translation patterns --- the distinction of atomic ASTs as @{ML
  1.1245 -  Ast.Constant} versus @{ML Ast.Variable} serves slightly different
  1.1246 -  purposes.
  1.1247 +text \<open>
  1.1248 +  Depending on the situation --- input syntax, output syntax, translation
  1.1249 +  patterns --- the distinction of atomic ASTs as @{ML Ast.Constant} versus
  1.1250 +  @{ML Ast.Variable} serves slightly different purposes.
  1.1251  
  1.1252 -  Input syntax of a term such as \<open>f a b = c\<close> does not yet
  1.1253 -  indicate the scopes of atomic entities \<open>f, a, b, c\<close>: they
  1.1254 -  could be global constants or local variables, even bound ones
  1.1255 -  depending on the context of the term.  @{ML Ast.Variable} leaves
  1.1256 -  this choice still open: later syntax layers (or translation
  1.1257 -  functions) may capture such a variable to determine its role
  1.1258 -  specifically, to make it a constant, bound variable, free variable
  1.1259 -  etc.  In contrast, syntax translations that introduce already known
  1.1260 -  constants would rather do it via @{ML Ast.Constant} to prevent
  1.1261 -  accidental re-interpretation later on.
  1.1262 +  Input syntax of a term such as \<open>f a b = c\<close> does not yet indicate the scopes
  1.1263 +  of atomic entities \<open>f, a, b, c\<close>: they could be global constants or local
  1.1264 +  variables, even bound ones depending on the context of the term. @{ML
  1.1265 +  Ast.Variable} leaves this choice still open: later syntax layers (or
  1.1266 +  translation functions) may capture such a variable to determine its role
  1.1267 +  specifically, to make it a constant, bound variable, free variable etc. In
  1.1268 +  contrast, syntax translations that introduce already known constants would
  1.1269 +  rather do it via @{ML Ast.Constant} to prevent accidental re-interpretation
  1.1270 +  later on.
  1.1271  
  1.1272 -  Output syntax turns term constants into @{ML Ast.Constant} and
  1.1273 -  variables (free or schematic) into @{ML Ast.Variable}.  This
  1.1274 -  information is precise when printing fully formal \<open>\<lambda>\<close>-terms.
  1.1275 +  Output syntax turns term constants into @{ML Ast.Constant} and variables
  1.1276 +  (free or schematic) into @{ML Ast.Variable}. This information is precise
  1.1277 +  when printing fully formal \<open>\<lambda>\<close>-terms.
  1.1278  
  1.1279    \<^medskip>
  1.1280 -  AST translation patterns (\secref{sec:syn-trans}) that
  1.1281 -  represent terms cannot distinguish constants and variables
  1.1282 -  syntactically.  Explicit indication of \<open>CONST c\<close> inside the
  1.1283 -  term language is required, unless \<open>c\<close> is known as special
  1.1284 -  \<^emph>\<open>syntax constant\<close> (see also @{command syntax}).  It is also
  1.1285 -  possible to use @{command syntax} declarations (without mixfix
  1.1286 -  annotation) to enforce that certain unqualified names are always
  1.1287 -  treated as constant within the syntax machinery.
  1.1288 +  AST translation patterns (\secref{sec:syn-trans}) that represent terms
  1.1289 +  cannot distinguish constants and variables syntactically. Explicit
  1.1290 +  indication of \<open>CONST c\<close> inside the term language is required, unless \<open>c\<close> is
  1.1291 +  known as special \<^emph>\<open>syntax constant\<close> (see also @{command syntax}). It is also
  1.1292 +  possible to use @{command syntax} declarations (without mixfix annotation)
  1.1293 +  to enforce that certain unqualified names are always treated as constant
  1.1294 +  within the syntax machinery.
  1.1295  
  1.1296 -  The situation is simpler for ASTs that represent types or sorts,
  1.1297 -  since the concrete syntax already distinguishes type variables from
  1.1298 -  type constants (constructors).  So \<open>('a, 'b) foo\<close>
  1.1299 -  corresponds to an AST application of some constant for \<open>foo\<close>
  1.1300 -  and variable arguments for \<open>'a\<close> and \<open>'b\<close>.  Note that
  1.1301 -  the postfix application is merely a feature of the concrete syntax,
  1.1302 -  while in the AST the constructor occurs in head position.\<close>
  1.1303 +  The situation is simpler for ASTs that represent types or sorts, since the
  1.1304 +  concrete syntax already distinguishes type variables from type constants
  1.1305 +  (constructors). So \<open>('a, 'b) foo\<close> corresponds to an AST application of some
  1.1306 +  constant for \<open>foo\<close> and variable arguments for \<open>'a\<close> and \<open>'b\<close>. Note that the
  1.1307 +  postfix application is merely a feature of the concrete syntax, while in the
  1.1308 +  AST the constructor occurs in head position.
  1.1309 +\<close>
  1.1310  
  1.1311  
  1.1312  subsubsection \<open>Authentic syntax names\<close>
  1.1313  
  1.1314 -text \<open>Naming constant entities within ASTs is another delicate
  1.1315 -  issue.  Unqualified names are resolved in the name space tables in
  1.1316 -  the last stage of parsing, after all translations have been applied.
  1.1317 -  Since syntax transformations do not know about this later name
  1.1318 -  resolution, there can be surprises in boundary cases.
  1.1319 +text \<open>
  1.1320 +  Naming constant entities within ASTs is another delicate issue. Unqualified
  1.1321 +  names are resolved in the name space tables in the last stage of parsing,
  1.1322 +  after all translations have been applied. Since syntax transformations do
  1.1323 +  not know about this later name resolution, there can be surprises in
  1.1324 +  boundary cases.
  1.1325  
  1.1326 -  \<^emph>\<open>Authentic syntax names\<close> for @{ML Ast.Constant} avoid this
  1.1327 -  problem: the fully-qualified constant name with a special prefix for
  1.1328 -  its formal category (\<open>class\<close>, \<open>type\<close>, \<open>const\<close>, \<open>fixed\<close>) represents the information faithfully
  1.1329 -  within the untyped AST format.  Accidental overlap with free or
  1.1330 -  bound variables is excluded as well.  Authentic syntax names work
  1.1331 -  implicitly in the following situations:
  1.1332 +  \<^emph>\<open>Authentic syntax names\<close> for @{ML Ast.Constant} avoid this problem: the
  1.1333 +  fully-qualified constant name with a special prefix for its formal category
  1.1334 +  (\<open>class\<close>, \<open>type\<close>, \<open>const\<close>, \<open>fixed\<close>) represents the information faithfully
  1.1335 +  within the untyped AST format. Accidental overlap with free or bound
  1.1336 +  variables is excluded as well. Authentic syntax names work implicitly in the
  1.1337 +  following situations:
  1.1338  
  1.1339 -  \<^item> Input of term constants (or fixed variables) that are
  1.1340 -  introduced by concrete syntax via @{command notation}: the
  1.1341 -  correspondence of a particular grammar production to some known term
  1.1342 -  entity is preserved.
  1.1343 +    \<^item> Input of term constants (or fixed variables) that are introduced by
  1.1344 +    concrete syntax via @{command notation}: the correspondence of a
  1.1345 +    particular grammar production to some known term entity is preserved.
  1.1346  
  1.1347 -  \<^item> Input of type constants (constructors) and type classes ---
  1.1348 -  thanks to explicit syntactic distinction independently on the
  1.1349 -  context.
  1.1350 +    \<^item> Input of type constants (constructors) and type classes --- thanks to
  1.1351 +    explicit syntactic distinction independently on the context.
  1.1352  
  1.1353 -  \<^item> Output of term constants, type constants, type classes ---
  1.1354 -  this information is already available from the internal term to be
  1.1355 -  printed.
  1.1356 -
  1.1357 +    \<^item> Output of term constants, type constants, type classes --- this
  1.1358 +    information is already available from the internal term to be printed.
  1.1359  
  1.1360 -  In other words, syntax transformations that operate on input terms
  1.1361 -  written as prefix applications are difficult to make robust.
  1.1362 -  Luckily, this case rarely occurs in practice, because syntax forms
  1.1363 -  to be translated usually correspond to some concrete notation.\<close>
  1.1364 +  In other words, syntax transformations that operate on input terms written
  1.1365 +  as prefix applications are difficult to make robust. Luckily, this case
  1.1366 +  rarely occurs in practice, because syntax forms to be translated usually
  1.1367 +  correspond to some concrete notation.
  1.1368 +\<close>
  1.1369  
  1.1370  
  1.1371  subsection \<open>Raw syntax and translations \label{sec:syn-trans}\<close>
  1.1372 @@ -1101,14 +1048,13 @@
  1.1373    \end{tabular}
  1.1374    \<^medskip>
  1.1375  
  1.1376 -  Unlike mixfix notation for existing formal entities
  1.1377 -  (\secref{sec:notation}), raw syntax declarations provide full access
  1.1378 -  to the priority grammar of the inner syntax, without any sanity
  1.1379 -  checks.  This includes additional syntactic categories (via
  1.1380 -  @{command nonterminal}) and free-form grammar productions (via
  1.1381 -  @{command syntax}).  Additional syntax translations (or macros, via
  1.1382 -  @{command translations}) are required to turn resulting parse trees
  1.1383 -  into proper representations of formal entities again.
  1.1384 +  Unlike mixfix notation for existing formal entities (\secref{sec:notation}),
  1.1385 +  raw syntax declarations provide full access to the priority grammar of the
  1.1386 +  inner syntax, without any sanity checks. This includes additional syntactic
  1.1387 +  categories (via @{command nonterminal}) and free-form grammar productions
  1.1388 +  (via @{command syntax}). Additional syntax translations (or macros, via
  1.1389 +  @{command translations}) are required to turn resulting parse trees into
  1.1390 +  proper representations of formal entities again.
  1.1391  
  1.1392    @{rail \<open>
  1.1393      @@{command nonterminal} (@{syntax name} + @'and')
  1.1394 @@ -1126,193 +1072,177 @@
  1.1395      transpat: ('(' @{syntax nameref} ')')? @{syntax string}
  1.1396    \<close>}
  1.1397  
  1.1398 -  \<^descr> @{command "nonterminal"}~\<open>c\<close> declares a type
  1.1399 -  constructor \<open>c\<close> (without arguments) to act as purely syntactic
  1.1400 -  type: a nonterminal symbol of the inner syntax.
  1.1401 +  \<^descr> @{command "nonterminal"}~\<open>c\<close> declares a type constructor \<open>c\<close> (without
  1.1402 +  arguments) to act as purely syntactic type: a nonterminal symbol of the
  1.1403 +  inner syntax.
  1.1404  
  1.1405 -  \<^descr> @{command "syntax"}~\<open>(mode) c :: \<sigma> (mx)\<close> augments the
  1.1406 -  priority grammar and the pretty printer table for the given print
  1.1407 -  mode (default \<^verbatim>\<open>""\<close>). An optional keyword @{keyword_ref
  1.1408 -  "output"} means that only the pretty printer table is affected.
  1.1409 +  \<^descr> @{command "syntax"}~\<open>(mode) c :: \<sigma> (mx)\<close> augments the priority grammar and
  1.1410 +  the pretty printer table for the given print mode (default \<^verbatim>\<open>""\<close>). An
  1.1411 +  optional keyword @{keyword_ref "output"} means that only the pretty printer
  1.1412 +  table is affected.
  1.1413  
  1.1414 -  Following \secref{sec:mixfix}, the mixfix annotation \<open>mx =
  1.1415 -  template ps q\<close> together with type \<open>\<sigma> = \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>\<close> and
  1.1416 -  specify a grammar production.  The \<open>template\<close> contains
  1.1417 -  delimiter tokens that surround \<open>n\<close> argument positions
  1.1418 -  (\<^verbatim>\<open>_\<close>).  The latter correspond to nonterminal symbols
  1.1419 -  \<open>A\<^sub>i\<close> derived from the argument types \<open>\<tau>\<^sub>i\<close> as
  1.1420 -  follows:
  1.1421 +  Following \secref{sec:mixfix}, the mixfix annotation \<open>mx = template ps q\<close>
  1.1422 +  together with type \<open>\<sigma> = \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>\<close> and specify a grammar production.
  1.1423 +  The \<open>template\<close> contains delimiter tokens that surround \<open>n\<close> argument
  1.1424 +  positions (\<^verbatim>\<open>_\<close>). The latter correspond to nonterminal symbols \<open>A\<^sub>i\<close> derived
  1.1425 +  from the argument types \<open>\<tau>\<^sub>i\<close> as follows:
  1.1426  
  1.1427      \<^item> \<open>prop\<close> if \<open>\<tau>\<^sub>i = prop\<close>
  1.1428  
  1.1429 -    \<^item> \<open>logic\<close> if \<open>\<tau>\<^sub>i = (\<dots>)\<kappa>\<close> for logical type
  1.1430 -    constructor \<open>\<kappa> \<noteq> prop\<close>
  1.1431 +    \<^item> \<open>logic\<close> if \<open>\<tau>\<^sub>i = (\<dots>)\<kappa>\<close> for logical type constructor \<open>\<kappa> \<noteq> prop\<close>
  1.1432  
  1.1433      \<^item> \<open>any\<close> if \<open>\<tau>\<^sub>i = \<alpha>\<close> for type variables
  1.1434  
  1.1435 -    \<^item> \<open>\<kappa>\<close> if \<open>\<tau>\<^sub>i = \<kappa>\<close> for nonterminal \<open>\<kappa>\<close>
  1.1436 -    (syntactic type constructor)
  1.1437 +    \<^item> \<open>\<kappa>\<close> if \<open>\<tau>\<^sub>i = \<kappa>\<close> for nonterminal \<open>\<kappa>\<close> (syntactic type constructor)
  1.1438  
  1.1439 -  Each \<open>A\<^sub>i\<close> is decorated by priority \<open>p\<^sub>i\<close> from the
  1.1440 -  given list \<open>ps\<close>; missing priorities default to 0.
  1.1441 +  Each \<open>A\<^sub>i\<close> is decorated by priority \<open>p\<^sub>i\<close> from the given list \<open>ps\<close>; missing
  1.1442 +  priorities default to 0.
  1.1443  
  1.1444 -  The resulting nonterminal of the production is determined similarly
  1.1445 -  from type \<open>\<tau>\<close>, with priority \<open>q\<close> and default 1000.
  1.1446 +  The resulting nonterminal of the production is determined similarly from
  1.1447 +  type \<open>\<tau>\<close>, with priority \<open>q\<close> and default 1000.
  1.1448  
  1.1449    \<^medskip>
  1.1450 -  Parsing via this production produces parse trees \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close> for the argument slots.  The resulting parse tree is
  1.1451 -  composed as \<open>c t\<^sub>1 \<dots> t\<^sub>n\<close>, by using the syntax constant \<open>c\<close> of the syntax declaration.
  1.1452 +  Parsing via this production produces parse trees \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close> for the
  1.1453 +  argument slots. The resulting parse tree is composed as \<open>c t\<^sub>1 \<dots> t\<^sub>n\<close>, by
  1.1454 +  using the syntax constant \<open>c\<close> of the syntax declaration.
  1.1455  
  1.1456 -  Such syntactic constants are invented on the spot, without formal
  1.1457 -  check wrt.\ existing declarations.  It is conventional to use plain
  1.1458 -  identifiers prefixed by a single underscore (e.g.\ \<open>_foobar\<close>).  Names should be chosen with care, to avoid clashes
  1.1459 -  with other syntax declarations.
  1.1460 +  Such syntactic constants are invented on the spot, without formal check
  1.1461 +  wrt.\ existing declarations. It is conventional to use plain identifiers
  1.1462 +  prefixed by a single underscore (e.g.\ \<open>_foobar\<close>). Names should be chosen
  1.1463 +  with care, to avoid clashes with other syntax declarations.
  1.1464  
  1.1465    \<^medskip>
  1.1466 -  The special case of copy production is specified by \<open>c =\<close>~\<^verbatim>\<open>""\<close> (empty string).
  1.1467 -  It means that the resulting parse tree \<open>t\<close> is copied directly, without any
  1.1468 -  further decoration.
  1.1469 +  The special case of copy production is specified by \<open>c =\<close>~\<^verbatim>\<open>""\<close> (empty
  1.1470 +  string). It means that the resulting parse tree \<open>t\<close> is copied directly,
  1.1471 +  without any further decoration.
  1.1472  
  1.1473 -  \<^descr> @{command "no_syntax"}~\<open>(mode) decls\<close> removes grammar
  1.1474 -  declarations (and translations) resulting from \<open>decls\<close>, which
  1.1475 -  are interpreted in the same manner as for @{command "syntax"} above.
  1.1476 +  \<^descr> @{command "no_syntax"}~\<open>(mode) decls\<close> removes grammar declarations (and
  1.1477 +  translations) resulting from \<open>decls\<close>, which are interpreted in the same
  1.1478 +  manner as for @{command "syntax"} above.
  1.1479 +
  1.1480 +  \<^descr> @{command "translations"}~\<open>rules\<close> specifies syntactic translation rules
  1.1481 +  (i.e.\ macros) as first-order rewrite rules on ASTs (\secref{sec:ast}). The
  1.1482 +  theory context maintains two independent lists translation rules: parse
  1.1483 +  rules (\<^verbatim>\<open>=>\<close> or \<open>\<rightharpoonup>\<close>) and print rules (\<^verbatim>\<open><=\<close> or \<open>\<leftharpoondown>\<close>). For convenience, both
  1.1484 +  can be specified simultaneously as parse~/ print rules (\<^verbatim>\<open>==\<close> or \<open>\<rightleftharpoons>\<close>).
  1.1485  
  1.1486 -  \<^descr> @{command "translations"}~\<open>rules\<close> specifies syntactic
  1.1487 -  translation rules (i.e.\ macros) as first-order rewrite rules on
  1.1488 -  ASTs (\secref{sec:ast}).  The theory context maintains two
  1.1489 -  independent lists translation rules: parse rules (\<^verbatim>\<open>=>\<close>
  1.1490 -  or \<open>\<rightharpoonup>\<close>) and print rules (\<^verbatim>\<open><=\<close> or \<open>\<leftharpoondown>\<close>).
  1.1491 -  For convenience, both can be specified simultaneously as parse~/
  1.1492 -  print rules (\<^verbatim>\<open>==\<close> or \<open>\<rightleftharpoons>\<close>).
  1.1493 +  Translation patterns may be prefixed by the syntactic category to be used
  1.1494 +  for parsing; the default is \<open>logic\<close> which means that regular term syntax is
  1.1495 +  used. Both sides of the syntax translation rule undergo parsing and parse
  1.1496 +  AST translations \secref{sec:tr-funs}, in order to perform some fundamental
  1.1497 +  normalization like \<open>\<lambda>x y. b \<leadsto> \<lambda>x. \<lambda>y. b\<close>, but other AST translation rules
  1.1498 +  are \<^emph>\<open>not\<close> applied recursively here.
  1.1499  
  1.1500 -  Translation patterns may be prefixed by the syntactic category to be
  1.1501 -  used for parsing; the default is \<open>logic\<close> which means that
  1.1502 -  regular term syntax is used.  Both sides of the syntax translation
  1.1503 -  rule undergo parsing and parse AST translations
  1.1504 -  \secref{sec:tr-funs}, in order to perform some fundamental
  1.1505 -  normalization like \<open>\<lambda>x y. b \<leadsto> \<lambda>x. \<lambda>y. b\<close>, but other AST
  1.1506 -  translation rules are \<^emph>\<open>not\<close> applied recursively here.
  1.1507 -
  1.1508 -  When processing AST patterns, the inner syntax lexer runs in a
  1.1509 -  different mode that allows identifiers to start with underscore.
  1.1510 -  This accommodates the usual naming convention for auxiliary syntax
  1.1511 -  constants --- those that do not have a logical counter part --- by
  1.1512 -  allowing to specify arbitrary AST applications within the term
  1.1513 -  syntax, independently of the corresponding concrete syntax.
  1.1514 +  When processing AST patterns, the inner syntax lexer runs in a different
  1.1515 +  mode that allows identifiers to start with underscore. This accommodates the
  1.1516 +  usual naming convention for auxiliary syntax constants --- those that do not
  1.1517 +  have a logical counter part --- by allowing to specify arbitrary AST
  1.1518 +  applications within the term syntax, independently of the corresponding
  1.1519 +  concrete syntax.
  1.1520  
  1.1521    Atomic ASTs are distinguished as @{ML Ast.Constant} versus @{ML
  1.1522 -  Ast.Variable} as follows: a qualified name or syntax constant
  1.1523 -  declared via @{command syntax}, or parse tree head of concrete
  1.1524 -  notation becomes @{ML Ast.Constant}, anything else @{ML
  1.1525 -  Ast.Variable}.  Note that \<open>CONST\<close> and \<open>XCONST\<close> within
  1.1526 -  the term language (\secref{sec:pure-grammar}) allow to enforce
  1.1527 -  treatment as constants.
  1.1528 +  Ast.Variable} as follows: a qualified name or syntax constant declared via
  1.1529 +  @{command syntax}, or parse tree head of concrete notation becomes @{ML
  1.1530 +  Ast.Constant}, anything else @{ML Ast.Variable}. Note that \<open>CONST\<close> and
  1.1531 +  \<open>XCONST\<close> within the term language (\secref{sec:pure-grammar}) allow to
  1.1532 +  enforce treatment as constants.
  1.1533  
  1.1534 -  AST rewrite rules \<open>(lhs, rhs)\<close> need to obey the following
  1.1535 -  side-conditions:
  1.1536 +  AST rewrite rules \<open>(lhs, rhs)\<close> need to obey the following side-conditions:
  1.1537  
  1.1538 -    \<^item> Rules must be left linear: \<open>lhs\<close> must not contain
  1.1539 -    repeated variables.\<^footnote>\<open>The deeper reason for this is that AST
  1.1540 -    equality is not well-defined: different occurrences of the ``same''
  1.1541 -    AST could be decorated differently by accidental type-constraints or
  1.1542 -    source position information, for example.\<close>
  1.1543 +    \<^item> Rules must be left linear: \<open>lhs\<close> must not contain repeated
  1.1544 +    variables.\<^footnote>\<open>The deeper reason for this is that AST equality is not
  1.1545 +    well-defined: different occurrences of the ``same'' AST could be decorated
  1.1546 +    differently by accidental type-constraints or source position information,
  1.1547 +    for example.\<close>
  1.1548  
  1.1549      \<^item> Every variable in \<open>rhs\<close> must also occur in \<open>lhs\<close>.
  1.1550  
  1.1551 -  \<^descr> @{command "no_translations"}~\<open>rules\<close> removes syntactic
  1.1552 -  translation rules, which are interpreted in the same manner as for
  1.1553 -  @{command "translations"} above.
  1.1554 +  \<^descr> @{command "no_translations"}~\<open>rules\<close> removes syntactic translation rules,
  1.1555 +  which are interpreted in the same manner as for @{command "translations"}
  1.1556 +  above.
  1.1557  
  1.1558 -  \<^descr> @{attribute syntax_ast_trace} and @{attribute
  1.1559 -  syntax_ast_stats} control diagnostic output in the AST normalization
  1.1560 -  process, when translation rules are applied to concrete input or
  1.1561 -  output.
  1.1562 +  \<^descr> @{attribute syntax_ast_trace} and @{attribute syntax_ast_stats} control
  1.1563 +  diagnostic output in the AST normalization process, when translation rules
  1.1564 +  are applied to concrete input or output.
  1.1565  
  1.1566  
  1.1567 -  Raw syntax and translations provides a slightly more low-level
  1.1568 -  access to the grammar and the form of resulting parse trees.  It is
  1.1569 -  often possible to avoid this untyped macro mechanism, and use
  1.1570 -  type-safe @{command abbreviation} or @{command notation} instead.
  1.1571 -  Some important situations where @{command syntax} and @{command
  1.1572 -  translations} are really need are as follows:
  1.1573 +  Raw syntax and translations provides a slightly more low-level access to the
  1.1574 +  grammar and the form of resulting parse trees. It is often possible to avoid
  1.1575 +  this untyped macro mechanism, and use type-safe @{command abbreviation} or
  1.1576 +  @{command notation} instead. Some important situations where @{command
  1.1577 +  syntax} and @{command translations} are really need are as follows:
  1.1578  
  1.1579 -  \<^item> Iterated replacement via recursive @{command translations}.
  1.1580 -  For example, consider list enumeration @{term "[a, b, c, d]"} as
  1.1581 -  defined in theory @{theory List} in Isabelle/HOL.
  1.1582 +  \<^item> Iterated replacement via recursive @{command translations}. For example,
  1.1583 +  consider list enumeration @{term "[a, b, c, d]"} as defined in theory
  1.1584 +  @{theory List} in Isabelle/HOL.
  1.1585  
  1.1586 -  \<^item> Change of binding status of variables: anything beyond the
  1.1587 -  built-in @{keyword "binder"} mixfix annotation requires explicit
  1.1588 -  syntax translations.  For example, consider list filter
  1.1589 -  comprehension @{term "[x \<leftarrow> xs . P]"} as defined in theory @{theory
  1.1590 -  List} in Isabelle/HOL.
  1.1591 +  \<^item> Change of binding status of variables: anything beyond the built-in
  1.1592 +  @{keyword "binder"} mixfix annotation requires explicit syntax translations.
  1.1593 +  For example, consider list filter comprehension @{term "[x \<leftarrow> xs . P]"} as
  1.1594 +  defined in theory @{theory List} in Isabelle/HOL.
  1.1595  \<close>
  1.1596  
  1.1597  
  1.1598  subsubsection \<open>Applying translation rules\<close>
  1.1599  
  1.1600 -text \<open>As a term is being parsed or printed, an AST is generated as
  1.1601 -  an intermediate form according to \figref{fig:parse-print}.  The AST
  1.1602 -  is normalized by applying translation rules in the manner of a
  1.1603 -  first-order term rewriting system.  We first examine how a single
  1.1604 -  rule is applied.
  1.1605 +text \<open>
  1.1606 +  As a term is being parsed or printed, an AST is generated as an intermediate
  1.1607 +  form according to \figref{fig:parse-print}. The AST is normalized by
  1.1608 +  applying translation rules in the manner of a first-order term rewriting
  1.1609 +  system. We first examine how a single rule is applied.
  1.1610  
  1.1611 -  Let \<open>t\<close> be the abstract syntax tree to be normalized and
  1.1612 -  \<open>(lhs, rhs)\<close> some translation rule.  A subtree \<open>u\<close>
  1.1613 -  of \<open>t\<close> is called \<^emph>\<open>redex\<close> if it is an instance of \<open>lhs\<close>; in this case the pattern \<open>lhs\<close> is said to match the
  1.1614 -  object \<open>u\<close>.  A redex matched by \<open>lhs\<close> may be
  1.1615 -  replaced by the corresponding instance of \<open>rhs\<close>, thus
  1.1616 -  \<^emph>\<open>rewriting\<close> the AST \<open>t\<close>.  Matching requires some notion
  1.1617 -  of \<^emph>\<open>place-holders\<close> in rule patterns: @{ML Ast.Variable} serves
  1.1618 -  this purpose.
  1.1619 +  Let \<open>t\<close> be the abstract syntax tree to be normalized and \<open>(lhs, rhs)\<close> some
  1.1620 +  translation rule. A subtree \<open>u\<close> of \<open>t\<close> is called \<^emph>\<open>redex\<close> if it is an
  1.1621 +  instance of \<open>lhs\<close>; in this case the pattern \<open>lhs\<close> is said to match the
  1.1622 +  object \<open>u\<close>. A redex matched by \<open>lhs\<close> may be replaced by the corresponding
  1.1623 +  instance of \<open>rhs\<close>, thus \<^emph>\<open>rewriting\<close> the AST \<open>t\<close>. Matching requires some
  1.1624 +  notion of \<^emph>\<open>place-holders\<close> in rule patterns: @{ML Ast.Variable} serves this
  1.1625 +  purpose.
  1.1626  
  1.1627 -  More precisely, the matching of the object \<open>u\<close> against the
  1.1628 -  pattern \<open>lhs\<close> is performed as follows:
  1.1629 +  More precisely, the matching of the object \<open>u\<close> against the pattern \<open>lhs\<close> is
  1.1630 +  performed as follows:
  1.1631  
  1.1632 -  \<^item> Objects of the form @{ML Ast.Variable}~\<open>x\<close> or @{ML
  1.1633 -  Ast.Constant}~\<open>x\<close> are matched by pattern @{ML
  1.1634 -  Ast.Constant}~\<open>x\<close>.  Thus all atomic ASTs in the object are
  1.1635 -  treated as (potential) constants, and a successful match makes them
  1.1636 -  actual constants even before name space resolution (see also
  1.1637 -  \secref{sec:ast}).
  1.1638 +    \<^item> Objects of the form @{ML Ast.Variable}~\<open>x\<close> or @{ML Ast.Constant}~\<open>x\<close> are
  1.1639 +    matched by pattern @{ML Ast.Constant}~\<open>x\<close>. Thus all atomic ASTs in the
  1.1640 +    object are treated as (potential) constants, and a successful match makes
  1.1641 +    them actual constants even before name space resolution (see also
  1.1642 +    \secref{sec:ast}).
  1.1643  
  1.1644 -  \<^item> Object \<open>u\<close> is matched by pattern @{ML
  1.1645 -  Ast.Variable}~\<open>x\<close>, binding \<open>x\<close> to \<open>u\<close>.
  1.1646 +    \<^item> Object \<open>u\<close> is matched by pattern @{ML Ast.Variable}~\<open>x\<close>, binding \<open>x\<close> to
  1.1647 +    \<open>u\<close>.
  1.1648  
  1.1649 -  \<^item> Object @{ML Ast.Appl}~\<open>us\<close> is matched by @{ML
  1.1650 -  Ast.Appl}~\<open>ts\<close> if \<open>us\<close> and \<open>ts\<close> have the
  1.1651 -  same length and each corresponding subtree matches.
  1.1652 +    \<^item> Object @{ML Ast.Appl}~\<open>us\<close> is matched by @{ML Ast.Appl}~\<open>ts\<close> if \<open>us\<close> and
  1.1653 +    \<open>ts\<close> have the same length and each corresponding subtree matches.
  1.1654  
  1.1655 -  \<^item> In every other case, matching fails.
  1.1656 +    \<^item> In every other case, matching fails.
  1.1657  
  1.1658 -
  1.1659 -  A successful match yields a substitution that is applied to \<open>rhs\<close>, generating the instance that replaces \<open>u\<close>.
  1.1660 +  A successful match yields a substitution that is applied to \<open>rhs\<close>,
  1.1661 +  generating the instance that replaces \<open>u\<close>.
  1.1662  
  1.1663 -  Normalizing an AST involves repeatedly applying translation rules
  1.1664 -  until none are applicable.  This works yoyo-like: top-down,
  1.1665 -  bottom-up, top-down, etc.  At each subtree position, rules are
  1.1666 -  chosen in order of appearance in the theory definitions.
  1.1667 +  Normalizing an AST involves repeatedly applying translation rules until none
  1.1668 +  are applicable. This works yoyo-like: top-down, bottom-up, top-down, etc. At
  1.1669 +  each subtree position, rules are chosen in order of appearance in the theory
  1.1670 +  definitions.
  1.1671  
  1.1672 -  The configuration options @{attribute syntax_ast_trace} and
  1.1673 -  @{attribute syntax_ast_stats} might help to understand this process
  1.1674 -  and diagnose problems.
  1.1675 +  The configuration options @{attribute syntax_ast_trace} and @{attribute
  1.1676 +  syntax_ast_stats} might help to understand this process and diagnose
  1.1677 +  problems.
  1.1678  
  1.1679    \begin{warn}
  1.1680 -  If syntax translation rules work incorrectly, the output of
  1.1681 -  @{command_ref print_syntax} with its \<^emph>\<open>rules\<close> sections reveals the
  1.1682 -  actual internal forms of AST pattern, without potentially confusing
  1.1683 -  concrete syntax.  Recall that AST constants appear as quoted strings
  1.1684 -  and variables without quotes.
  1.1685 +  If syntax translation rules work incorrectly, the output of @{command_ref
  1.1686 +  print_syntax} with its \<^emph>\<open>rules\<close> sections reveals the actual internal forms
  1.1687 +  of AST pattern, without potentially confusing concrete syntax. Recall that
  1.1688 +  AST constants appear as quoted strings and variables without quotes.
  1.1689    \end{warn}
  1.1690  
  1.1691    \begin{warn}
  1.1692 -  If @{attribute_ref eta_contract} is set to \<open>true\<close>, terms
  1.1693 -  will be \<open>\<eta>\<close>-contracted \<^emph>\<open>before\<close> the AST rewriter sees
  1.1694 -  them.  Thus some abstraction nodes needed for print rules to match
  1.1695 -  may vanish.  For example, \<open>Ball A (\<lambda>x. P x)\<close> would contract
  1.1696 -  to \<open>Ball A P\<close> and the standard print rule would fail to
  1.1697 -  apply.  This problem can be avoided by hand-written ML translation
  1.1698 -  functions (see also \secref{sec:tr-funs}), which is in fact the same
  1.1699 -  mechanism used in built-in @{keyword "binder"} declarations.
  1.1700 +  If @{attribute_ref eta_contract} is set to \<open>true\<close>, terms will be
  1.1701 +  \<open>\<eta>\<close>-contracted \<^emph>\<open>before\<close> the AST rewriter sees them. Thus some abstraction
  1.1702 +  nodes needed for print rules to match may vanish. For example, \<open>Ball A (\<lambda>x.
  1.1703 +  P x)\<close> would contract to \<open>Ball A P\<close> and the standard print rule would fail to
  1.1704 +  apply. This problem can be avoided by hand-written ML translation functions
  1.1705 +  (see also \secref{sec:tr-funs}), which is in fact the same mechanism used in
  1.1706 +  built-in @{keyword "binder"} declarations.
  1.1707    \end{warn}
  1.1708  \<close>
  1.1709  
  1.1710 @@ -1347,10 +1277,9 @@
  1.1711     @@{ML_antiquotation syntax_const}) name
  1.1712    \<close>}
  1.1713  
  1.1714 -  \<^descr> @{command parse_translation} etc. declare syntax translation
  1.1715 -  functions to the theory.  Any of these commands have a single
  1.1716 -  @{syntax text} argument that refers to an ML expression of
  1.1717 -  appropriate type as follows:
  1.1718 +  \<^descr> @{command parse_translation} etc. declare syntax translation functions to
  1.1719 +  the theory. Any of these commands have a single @{syntax text} argument that
  1.1720 +  refers to an ML expression of appropriate type as follows:
  1.1721  
  1.1722    \<^medskip>
  1.1723    {\footnotesize
  1.1724 @@ -1368,110 +1297,108 @@
  1.1725    \end{tabular}}
  1.1726    \<^medskip>
  1.1727  
  1.1728 -  The argument list consists of \<open>(c, tr)\<close> pairs, where \<open>c\<close> is the syntax name of the formal entity involved, and \<open>tr\<close> a function that translates a syntax form \<open>c args\<close> into
  1.1729 -  \<open>tr ctxt args\<close> (depending on the context).  The Isabelle/ML
  1.1730 -  naming convention for parse translations is \<open>c_tr\<close> and for
  1.1731 -  print translations \<open>c_tr'\<close>.
  1.1732 +  The argument list consists of \<open>(c, tr)\<close> pairs, where \<open>c\<close> is the syntax name
  1.1733 +  of the formal entity involved, and \<open>tr\<close> a function that translates a syntax
  1.1734 +  form \<open>c args\<close> into \<open>tr ctxt args\<close> (depending on the context). The
  1.1735 +  Isabelle/ML naming convention for parse translations is \<open>c_tr\<close> and for print
  1.1736 +  translations \<open>c_tr'\<close>.
  1.1737  
  1.1738    The @{command_ref print_syntax} command displays the sets of names
  1.1739 -  associated with the translation functions of a theory under \<open>parse_ast_translation\<close> etc.
  1.1740 +  associated with the translation functions of a theory under
  1.1741 +  \<open>parse_ast_translation\<close> etc.
  1.1742  
  1.1743 -  \<^descr> \<open>@{class_syntax c}\<close>, \<open>@{type_syntax c}\<close>,
  1.1744 -  \<open>@{const_syntax c}\<close> inline the authentic syntax name of the
  1.1745 -  given formal entities into the ML source.  This is the
  1.1746 -  fully-qualified logical name prefixed by a special marker to
  1.1747 -  indicate its kind: thus different logical name spaces are properly
  1.1748 -  distinguished within parse trees.
  1.1749 +  \<^descr> \<open>@{class_syntax c}\<close>, \<open>@{type_syntax c}\<close>, \<open>@{const_syntax c}\<close> inline the
  1.1750 +  authentic syntax name of the given formal entities into the ML source. This
  1.1751 +  is the fully-qualified logical name prefixed by a special marker to indicate
  1.1752 +  its kind: thus different logical name spaces are properly distinguished
  1.1753 +  within parse trees.
  1.1754  
  1.1755 -  \<^descr> \<open>@{const_syntax c}\<close> inlines the name \<open>c\<close> of
  1.1756 -  the given syntax constant, having checked that it has been declared
  1.1757 -  via some @{command syntax} commands within the theory context.  Note
  1.1758 -  that the usual naming convention makes syntax constants start with
  1.1759 -  underscore, to reduce the chance of accidental clashes with other
  1.1760 -  names occurring in parse trees (unqualified constants etc.).
  1.1761 +  \<^descr> \<open>@{const_syntax c}\<close> inlines the name \<open>c\<close> of the given syntax constant,
  1.1762 +  having checked that it has been declared via some @{command syntax} commands
  1.1763 +  within the theory context. Note that the usual naming convention makes
  1.1764 +  syntax constants start with underscore, to reduce the chance of accidental
  1.1765 +  clashes with other names occurring in parse trees (unqualified constants
  1.1766 +  etc.).
  1.1767  \<close>
  1.1768  
  1.1769  
  1.1770  subsubsection \<open>The translation strategy\<close>
  1.1771  
  1.1772 -text \<open>The different kinds of translation functions are invoked during
  1.1773 -  the transformations between parse trees, ASTs and syntactic terms
  1.1774 -  (cf.\ \figref{fig:parse-print}).  Whenever a combination of the form
  1.1775 -  \<open>c x\<^sub>1 \<dots> x\<^sub>n\<close> is encountered, and a translation function
  1.1776 -  \<open>f\<close> of appropriate kind is declared for \<open>c\<close>, the
  1.1777 -  result is produced by evaluation of \<open>f [x\<^sub>1, \<dots>, x\<^sub>n]\<close> in ML.
  1.1778 +text \<open>
  1.1779 +  The different kinds of translation functions are invoked during the
  1.1780 +  transformations between parse trees, ASTs and syntactic terms (cf.\
  1.1781 +  \figref{fig:parse-print}). Whenever a combination of the form \<open>c x\<^sub>1 \<dots> x\<^sub>n\<close>
  1.1782 +  is encountered, and a translation function \<open>f\<close> of appropriate kind is
  1.1783 +  declared for \<open>c\<close>, the result is produced by evaluation of \<open>f [x\<^sub>1, \<dots>, x\<^sub>n]\<close>
  1.1784 +  in ML.
  1.1785  
  1.1786 -  For AST translations, the arguments \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> are ASTs.  A
  1.1787 -  combination has the form @{ML "Ast.Constant"}~\<open>c\<close> or @{ML
  1.1788 -  "Ast.Appl"}~\<open>[\<close>@{ML Ast.Constant}~\<open>c, x\<^sub>1, \<dots>, x\<^sub>n]\<close>.
  1.1789 -  For term translations, the arguments are terms and a combination has
  1.1790 -  the form @{ML Const}~\<open>(c, \<tau>)\<close> or @{ML Const}~\<open>(c, \<tau>)
  1.1791 -  $ x\<^sub>1 $ \<dots> $ x\<^sub>n\<close>.  Terms allow more sophisticated transformations
  1.1792 -  than ASTs do, typically involving abstractions and bound
  1.1793 -  variables. \<^emph>\<open>Typed\<close> print translations may even peek at the type
  1.1794 -  \<open>\<tau>\<close> of the constant they are invoked on, although some
  1.1795 -  information might have been suppressed for term output already.
  1.1796 +  For AST translations, the arguments \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> are ASTs. A combination
  1.1797 +  has the form @{ML "Ast.Constant"}~\<open>c\<close> or @{ML "Ast.Appl"}~\<open>[\<close>@{ML
  1.1798 +  Ast.Constant}~\<open>c, x\<^sub>1, \<dots>, x\<^sub>n]\<close>. For term translations, the arguments are
  1.1799 +  terms and a combination has the form @{ML Const}~\<open>(c, \<tau>)\<close> or @{ML
  1.1800 +  Const}~\<open>(c, \<tau>) $ x\<^sub>1 $ \<dots> $ x\<^sub>n\<close>. Terms allow more sophisticated
  1.1801 +  transformations than ASTs do, typically involving abstractions and bound
  1.1802 +  variables. \<^emph>\<open>Typed\<close> print translations may even peek at the type \<open>\<tau>\<close> of the
  1.1803 +  constant they are invoked on, although some information might have been
  1.1804 +  suppressed for term output already.
  1.1805  
  1.1806 -  Regardless of whether they act on ASTs or terms, translation
  1.1807 -  functions called during the parsing process differ from those for
  1.1808 -  printing in their overall behaviour:
  1.1809 +  Regardless of whether they act on ASTs or terms, translation functions
  1.1810 +  called during the parsing process differ from those for printing in their
  1.1811 +  overall behaviour:
  1.1812  
  1.1813 -  \<^descr>[Parse translations] are applied bottom-up.  The arguments are
  1.1814 -  already in translated form.  The translations must not fail;
  1.1815 -  exceptions trigger an error message.  There may be at most one
  1.1816 -  function associated with any syntactic name.
  1.1817 +    \<^descr>[Parse translations] are applied bottom-up. The arguments are already in
  1.1818 +    translated form. The translations must not fail; exceptions trigger an
  1.1819 +    error message. There may be at most one function associated with any
  1.1820 +    syntactic name.
  1.1821  
  1.1822 -  \<^descr>[Print translations] are applied top-down.  They are supplied
  1.1823 -  with arguments that are partly still in internal form.  The result
  1.1824 -  again undergoes translation; therefore a print translation should
  1.1825 -  not introduce as head the very constant that invoked it.  The
  1.1826 -  function may raise exception @{ML Match} to indicate failure; in
  1.1827 -  this event it has no effect.  Multiple functions associated with
  1.1828 -  some syntactic name are tried in the order of declaration in the
  1.1829 -  theory.
  1.1830 +    \<^descr>[Print translations] are applied top-down. They are supplied with
  1.1831 +    arguments that are partly still in internal form. The result again
  1.1832 +    undergoes translation; therefore a print translation should not introduce
  1.1833 +    as head the very constant that invoked it. The function may raise
  1.1834 +    exception @{ML Match} to indicate failure; in this event it has no effect.
  1.1835 +    Multiple functions associated with some syntactic name are tried in the
  1.1836 +    order of declaration in the theory.
  1.1837  
  1.1838 -
  1.1839 -  Only constant atoms --- constructor @{ML Ast.Constant} for ASTs and
  1.1840 -  @{ML Const} for terms --- can invoke translation functions.  This
  1.1841 -  means that parse translations can only be associated with parse tree
  1.1842 -  heads of concrete syntax, or syntactic constants introduced via
  1.1843 -  other translations.  For plain identifiers within the term language,
  1.1844 -  the status of constant versus variable is not yet know during
  1.1845 -  parsing.  This is in contrast to print translations, where constants
  1.1846 -  are explicitly known from the given term in its fully internal form.
  1.1847 +  Only constant atoms --- constructor @{ML Ast.Constant} for ASTs and @{ML
  1.1848 +  Const} for terms --- can invoke translation functions. This means that parse
  1.1849 +  translations can only be associated with parse tree heads of concrete
  1.1850 +  syntax, or syntactic constants introduced via other translations. For plain
  1.1851 +  identifiers within the term language, the status of constant versus variable
  1.1852 +  is not yet know during parsing. This is in contrast to print translations,
  1.1853 +  where constants are explicitly known from the given term in its fully
  1.1854 +  internal form.
  1.1855  \<close>
  1.1856  
  1.1857  
  1.1858  subsection \<open>Built-in syntax transformations\<close>
  1.1859  
  1.1860  text \<open>
  1.1861 -  Here are some further details of the main syntax transformation
  1.1862 -  phases of \figref{fig:parse-print}.
  1.1863 +  Here are some further details of the main syntax transformation phases of
  1.1864 +  \figref{fig:parse-print}.
  1.1865  \<close>
  1.1866  
  1.1867  
  1.1868  subsubsection \<open>Transforming parse trees to ASTs\<close>
  1.1869  
  1.1870 -text \<open>The parse tree is the raw output of the parser.  It is
  1.1871 -  transformed into an AST according to some basic scheme that may be
  1.1872 -  augmented by AST translation functions as explained in
  1.1873 -  \secref{sec:tr-funs}.
  1.1874 +text \<open>
  1.1875 +  The parse tree is the raw output of the parser. It is transformed into an
  1.1876 +  AST according to some basic scheme that may be augmented by AST translation
  1.1877 +  functions as explained in \secref{sec:tr-funs}.
  1.1878  
  1.1879    The parse tree is constructed by nesting the right-hand sides of the
  1.1880 -  productions used to recognize the input.  Such parse trees are
  1.1881 -  simply lists of tokens and constituent parse trees, the latter
  1.1882 -  representing the nonterminals of the productions.  Ignoring AST
  1.1883 -  translation functions, parse trees are transformed to ASTs by
  1.1884 -  stripping out delimiters and copy productions, while retaining some
  1.1885 -  source position information from input tokens.
  1.1886 +  productions used to recognize the input. Such parse trees are simply lists
  1.1887 +  of tokens and constituent parse trees, the latter representing the
  1.1888 +  nonterminals of the productions. Ignoring AST translation functions, parse
  1.1889 +  trees are transformed to ASTs by stripping out delimiters and copy
  1.1890 +  productions, while retaining some source position information from input
  1.1891 +  tokens.
  1.1892  
  1.1893 -  The Pure syntax provides predefined AST translations to make the
  1.1894 -  basic \<open>\<lambda>\<close>-term structure more apparent within the
  1.1895 -  (first-order) AST representation, and thus facilitate the use of
  1.1896 -  @{command translations} (see also \secref{sec:syn-trans}).  This
  1.1897 -  covers ordinary term application, type application, nested
  1.1898 -  abstraction, iterated meta implications and function types.  The
  1.1899 -  effect is illustrated on some representative input strings is as
  1.1900 +  The Pure syntax provides predefined AST translations to make the basic
  1.1901 +  \<open>\<lambda>\<close>-term structure more apparent within the (first-order) AST
  1.1902 +  representation, and thus facilitate the use of @{command translations} (see
  1.1903 +  also \secref{sec:syn-trans}). This covers ordinary term application, type
  1.1904 +  application, nested abstraction, iterated meta implications and function
  1.1905 +  types. The effect is illustrated on some representative input strings is as
  1.1906    follows:
  1.1907  
  1.1908    \begin{center}
  1.1909 @@ -1489,85 +1416,83 @@
  1.1910    \end{center}
  1.1911  
  1.1912    Note that type and sort constraints may occur in further places ---
  1.1913 -  translations need to be ready to cope with them.  The built-in
  1.1914 -  syntax transformation from parse trees to ASTs insert additional
  1.1915 -  constraints that represent source positions.
  1.1916 +  translations need to be ready to cope with them. The built-in syntax
  1.1917 +  transformation from parse trees to ASTs insert additional constraints that
  1.1918 +  represent source positions.
  1.1919  \<close>
  1.1920  
  1.1921  
  1.1922  subsubsection \<open>Transforming ASTs to terms\<close>
  1.1923  
  1.1924 -text \<open>After application of macros (\secref{sec:syn-trans}), the AST
  1.1925 -  is transformed into a term.  This term still lacks proper type
  1.1926 -  information, but it might contain some constraints consisting of
  1.1927 -  applications with head \<^verbatim>\<open>_constrain\<close>, where the second
  1.1928 -  argument is a type encoded as a pre-term within the syntax.  Type
  1.1929 -  inference later introduces correct types, or indicates type errors
  1.1930 -  in the input.
  1.1931 +text \<open>
  1.1932 +  After application of macros (\secref{sec:syn-trans}), the AST is transformed
  1.1933 +  into a term. This term still lacks proper type information, but it might
  1.1934 +  contain some constraints consisting of applications with head \<^verbatim>\<open>_constrain\<close>,
  1.1935 +  where the second argument is a type encoded as a pre-term within the syntax.
  1.1936 +  Type inference later introduces correct types, or indicates type errors in
  1.1937 +  the input.
  1.1938  
  1.1939 -  Ignoring parse translations, ASTs are transformed to terms by
  1.1940 -  mapping AST constants to term constants, AST variables to term
  1.1941 -  variables or constants (according to the name space), and AST
  1.1942 -  applications to iterated term applications.
  1.1943 +  Ignoring parse translations, ASTs are transformed to terms by mapping AST
  1.1944 +  constants to term constants, AST variables to term variables or constants
  1.1945 +  (according to the name space), and AST applications to iterated term
  1.1946 +  applications.
  1.1947  
  1.1948 -  The outcome is still a first-order term.  Proper abstractions and
  1.1949 -  bound variables are introduced by parse translations associated with
  1.1950 -  certain syntax constants.  Thus \<^verbatim>\<open>("_abs" x x)\<close> eventually
  1.1951 -  becomes a de-Bruijn term \<^verbatim>\<open>Abs ("x", _, Bound 0)\<close>.
  1.1952 +  The outcome is still a first-order term. Proper abstractions and bound
  1.1953 +  variables are introduced by parse translations associated with certain
  1.1954 +  syntax constants. Thus \<^verbatim>\<open>("_abs" x x)\<close> eventually becomes a de-Bruijn term
  1.1955 +  \<^verbatim>\<open>Abs ("x", _, Bound 0)\<close>.
  1.1956  \<close>
  1.1957  
  1.1958  
  1.1959  subsubsection \<open>Printing of terms\<close>
  1.1960  
  1.1961 -text \<open>The output phase is essentially the inverse of the input
  1.1962 -  phase.  Terms are translated via abstract syntax trees into
  1.1963 -  pretty-printed text.
  1.1964 +text \<open>
  1.1965 +  The output phase is essentially the inverse of the input phase. Terms are
  1.1966 +  translated via abstract syntax trees into pretty-printed text.
  1.1967  
  1.1968    Ignoring print translations, the transformation maps term constants,
  1.1969    variables and applications to the corresponding constructs on ASTs.
  1.1970 -  Abstractions are mapped to applications of the special constant
  1.1971 -  \<^verbatim>\<open>_abs\<close> as seen before.  Type constraints are represented
  1.1972 -  via special \<^verbatim>\<open>_constrain\<close> forms, according to various
  1.1973 -  policies of type annotation determined elsewhere.  Sort constraints
  1.1974 -  of type variables are handled in a similar fashion.
  1.1975 +  Abstractions are mapped to applications of the special constant \<^verbatim>\<open>_abs\<close> as
  1.1976 +  seen before. Type constraints are represented via special \<^verbatim>\<open>_constrain\<close>
  1.1977 +  forms, according to various policies of type annotation determined
  1.1978 +  elsewhere. Sort constraints of type variables are handled in a similar
  1.1979 +  fashion.
  1.1980  
  1.1981 -  After application of macros (\secref{sec:syn-trans}), the AST is
  1.1982 -  finally pretty-printed.  The built-in print AST translations reverse
  1.1983 -  the corresponding parse AST translations.
  1.1984 +  After application of macros (\secref{sec:syn-trans}), the AST is finally
  1.1985 +  pretty-printed. The built-in print AST translations reverse the
  1.1986 +  corresponding parse AST translations.
  1.1987  
  1.1988    \<^medskip>
  1.1989    For the actual printing process, the priority grammar
  1.1990 -  (\secref{sec:priority-grammar}) plays a vital role: productions are
  1.1991 -  used as templates for pretty printing, with argument slots stemming
  1.1992 -  from nonterminals, and syntactic sugar stemming from literal tokens.
  1.1993 +  (\secref{sec:priority-grammar}) plays a vital role: productions are used as
  1.1994 +  templates for pretty printing, with argument slots stemming from
  1.1995 +  nonterminals, and syntactic sugar stemming from literal tokens.
  1.1996  
  1.1997 -  Each AST application with constant head \<open>c\<close> and arguments
  1.1998 -  \<open>t\<^sub>1\<close>, \dots, \<open>t\<^sub>n\<close> (for \<open>n = 0\<close> the AST is
  1.1999 -  just the constant \<open>c\<close> itself) is printed according to the
  1.2000 -  first grammar production of result name \<open>c\<close>.  The required
  1.2001 -  syntax priority of the argument slot is given by its nonterminal
  1.2002 -  \<open>A\<^sup>(\<^sup>p\<^sup>)\<close>.  The argument \<open>t\<^sub>i\<close> that corresponds to the
  1.2003 -  position of \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is printed recursively, and then put in
  1.2004 -  parentheses \<^emph>\<open>if\<close> its priority \<open>p\<close> requires this.  The
  1.2005 -  resulting output is concatenated with the syntactic sugar according
  1.2006 -  to the grammar production.
  1.2007 +  Each AST application with constant head \<open>c\<close> and arguments \<open>t\<^sub>1\<close>, \dots,
  1.2008 +  \<open>t\<^sub>n\<close> (for \<open>n = 0\<close> the AST is just the constant \<open>c\<close> itself) is printed
  1.2009 +  according to the first grammar production of result name \<open>c\<close>. The required
  1.2010 +  syntax priority of the argument slot is given by its nonterminal \<open>A\<^sup>(\<^sup>p\<^sup>)\<close>.
  1.2011 +  The argument \<open>t\<^sub>i\<close> that corresponds to the position of \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is printed
  1.2012 +  recursively, and then put in parentheses \<^emph>\<open>if\<close> its priority \<open>p\<close> requires
  1.2013 +  this. The resulting output is concatenated with the syntactic sugar
  1.2014 +  according to the grammar production.
  1.2015  
  1.2016 -  If an AST application \<open>(c x\<^sub>1 \<dots> x\<^sub>m)\<close> has more arguments than
  1.2017 -  the corresponding production, it is first split into \<open>((c x\<^sub>1
  1.2018 -  \<dots> x\<^sub>n) x\<^sub>n\<^sub>+\<^sub>1 \<dots> x\<^sub>m)\<close> and then printed recursively as above.
  1.2019 +  If an AST application \<open>(c x\<^sub>1 \<dots> x\<^sub>m)\<close> has more arguments than the
  1.2020 +  corresponding production, it is first split into \<open>((c x\<^sub>1 \<dots> x\<^sub>n) x\<^sub>n\<^sub>+\<^sub>1 \<dots>
  1.2021 +  x\<^sub>m)\<close> and then printed recursively as above.
  1.2022  
  1.2023 -  Applications with too few arguments or with non-constant head or
  1.2024 -  without a corresponding production are printed in prefix-form like
  1.2025 -  \<open>f t\<^sub>1 \<dots> t\<^sub>n\<close> for terms.
  1.2026 +  Applications with too few arguments or with non-constant head or without a
  1.2027 +  corresponding production are printed in prefix-form like \<open>f t\<^sub>1 \<dots> t\<^sub>n\<close> for
  1.2028 +  terms.
  1.2029  
  1.2030 -  Multiple productions associated with some name \<open>c\<close> are tried
  1.2031 -  in order of appearance within the grammar.  An occurrence of some
  1.2032 -  AST variable \<open>x\<close> is printed as \<open>x\<close> outright.
  1.2033 +  Multiple productions associated with some name \<open>c\<close> are tried in order of
  1.2034 +  appearance within the grammar. An occurrence of some AST variable \<open>x\<close> is
  1.2035 +  printed as \<open>x\<close> outright.
  1.2036  
  1.2037    \<^medskip>
  1.2038 -  White space is \<^emph>\<open>not\<close> inserted automatically.  If
  1.2039 -  blanks (or breaks) are required to separate tokens, they need to be
  1.2040 -  specified in the mixfix declaration (\secref{sec:mixfix}).
  1.2041 +  White space is \<^emph>\<open>not\<close> inserted automatically. If blanks (or breaks) are
  1.2042 +  required to separate tokens, they need to be specified in the mixfix
  1.2043 +  declaration (\secref{sec:mixfix}).
  1.2044  \<close>
  1.2045  
  1.2046  end