doc-src/IsarRef/Thy/Inner_Syntax.thy
author wenzelm
Fri Feb 17 15:42:26 2012 +0100 (2012-02-17)
changeset 46512 4f9f61f9b535
parent 46506 c7faa011bfa7
child 48113 1c4500446ba4
permissions -rw-r--r--
simplified configuration options for syntax ambiguity;
     1 theory Inner_Syntax
     2 imports Base Main
     3 begin
     4 
     5 chapter {* Inner syntax --- the term language \label{ch:inner-syntax} *}
     6 
     7 text {* The inner syntax of Isabelle provides concrete notation for
     8   the main entities of the logical framework, notably @{text
     9   "\<lambda>"}-terms with types and type classes.  Applications may either
    10   extend existing syntactic categories by additional notation, or
    11   define new sub-languages that are linked to the standard term
    12   language via some explicit markers.  For example @{verbatim
    13   FOO}~@{text "foo"} could embed the syntax corresponding for some
    14   user-defined nonterminal @{text "foo"} --- within the bounds of the
    15   given lexical syntax of Isabelle/Pure.
    16 
    17   The most basic way to specify concrete syntax for logical entities
    18   works via mixfix annotations (\secref{sec:mixfix}), which may be
    19   usually given as part of the original declaration or via explicit
    20   notation commands later on (\secref{sec:notation}).  This already
    21   covers many needs of concrete syntax without having to understand
    22   the full complexity of inner syntax layers.
    23 
    24   Further details of the syntax engine involves the classical
    25   distinction of lexical language versus context-free grammar (see
    26   \secref{sec:pure-syntax}), and various mechanisms for \emph{syntax
    27   translations} --- either as rewrite systems on first-order ASTs
    28   (\secref{sec:syn-trans}) or ML functions on ASTs or @{text
    29   "\<lambda>"}-terms that represent parse trees (\secref{sec:tr-funs}).
    30 *}
    31 
    32 
    33 section {* Printing logical entities *}
    34 
    35 subsection {* Diagnostic commands \label{sec:print-diag} *}
    36 
    37 text {*
    38   \begin{matharray}{rcl}
    39     @{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    40     @{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    41     @{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    42     @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    43     @{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    44     @{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    45     @{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
    46   \end{matharray}
    47 
    48   These diagnostic commands assist interactive development by printing
    49   internal logical entities in a human-readable fashion.
    50 
    51   @{rail "
    52     @@{command typ} @{syntax modes}? @{syntax type}
    53     ;
    54     @@{command term} @{syntax modes}? @{syntax term}
    55     ;
    56     @@{command prop} @{syntax modes}? @{syntax prop}
    57     ;
    58     @@{command thm} @{syntax modes}? @{syntax thmrefs}
    59     ;
    60     ( @@{command prf} | @@{command full_prf} ) @{syntax modes}? @{syntax thmrefs}?
    61     ;
    62     @@{command pr} @{syntax modes}? @{syntax nat}?
    63     ;
    64 
    65     @{syntax_def modes}: '(' (@{syntax name} + ) ')'
    66   "}
    67 
    68   \begin{description}
    69 
    70   \item @{command "typ"}~@{text \<tau>} reads and prints types of the
    71   meta-logic according to the current theory or proof context.
    72 
    73   \item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}
    74   read, type-check and print terms or propositions according to the
    75   current theory or proof context; the inferred type of @{text t} is
    76   output as well.  Note that these commands are also useful in
    77   inspecting the current environment of term abbreviations.
    78 
    79   \item @{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} retrieves
    80   theorems from the current theory or proof context.  Note that any
    81   attributes included in the theorem specifications are applied to a
    82   temporary context derived from the current theory or proof; the
    83   result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1,
    84   \<dots>, a\<^sub>n"} do not have any permanent effect.
    85 
    86   \item @{command "prf"} displays the (compact) proof term of the
    87   current proof state (if present), or of the given theorems. Note
    88   that this requires proof terms to be switched on for the current
    89   object logic (see the ``Proof terms'' section of the Isabelle
    90   reference manual for information on how to do this).
    91 
    92   \item @{command "full_prf"} is like @{command "prf"}, but displays
    93   the full proof term, i.e.\ also displays information omitted in the
    94   compact proof term, which is denoted by ``@{text _}'' placeholders
    95   there.
    96 
    97   \item @{command "pr"}~@{text "goals"} prints the current proof state
    98   (if present), including current facts and goals.  The optional limit
    99   arguments affect the number of goals to be displayed, which is
   100   initially 10.  Omitting limit value leaves the current setting
   101   unchanged.
   102 
   103   \end{description}
   104 
   105   All of the diagnostic commands above admit a list of @{text modes}
   106   to be specified, which is appended to the current print mode; see
   107   also \secref{sec:print-modes}.  Thus the output behavior may be
   108   modified according particular print mode features.  For example,
   109   @{command "pr"}~@{text "(latex xsymbols)"} would print the current
   110   proof state with mathematical symbols and special characters
   111   represented in {\LaTeX} source, according to the Isabelle style
   112   \cite{isabelle-sys}.
   113 
   114   Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
   115   systematic way to include formal items into the printed text
   116   document.
   117 *}
   118 
   119 
   120 subsection {* Details of printed content *}
   121 
   122 text {*
   123   \begin{tabular}{rcll}
   124     @{attribute_def show_types} & : & @{text attribute} & default @{text false} \\
   125     @{attribute_def show_sorts} & : & @{text attribute} & default @{text false} \\
   126     @{attribute_def show_consts} & : & @{text attribute} & default @{text false} \\
   127     @{attribute_def show_abbrevs} & : & @{text attribute} & default @{text true} \\
   128     @{attribute_def show_brackets} & : & @{text attribute} & default @{text false} \\
   129     @{attribute_def names_long} & : & @{text attribute} & default @{text false} \\
   130     @{attribute_def names_short} & : & @{text attribute} & default @{text false} \\
   131     @{attribute_def names_unique} & : & @{text attribute} & default @{text true} \\
   132     @{attribute_def eta_contract} & : & @{text attribute} & default @{text true} \\
   133     @{attribute_def goals_limit} & : & @{text attribute} & default @{text 10} \\
   134     @{attribute_def show_main_goal} & : & @{text attribute} & default @{text false} \\
   135     @{attribute_def show_hyps} & : & @{text attribute} & default @{text false} \\
   136     @{attribute_def show_tags} & : & @{text attribute} & default @{text false} \\
   137     @{attribute_def show_question_marks} & : & @{text attribute} & default @{text true} \\
   138   \end{tabular}
   139   \medskip
   140 
   141   These configuration options control the detail of information that
   142   is displayed for types, terms, theorems, goals etc.  See also
   143   \secref{sec:config}.
   144 
   145   \begin{description}
   146 
   147   \item @{attribute show_types} and @{attribute show_sorts} control
   148   printing of type constraints for term variables, and sort
   149   constraints for type variables.  By default, neither of these are
   150   shown in output.  If @{attribute show_sorts} is enabled, types are
   151   always shown as well.
   152 
   153   Note that displaying types and sorts may explain why a polymorphic
   154   inference rule fails to resolve with some goal, or why a rewrite
   155   rule does not apply as expected.
   156 
   157   \item @{attribute show_consts} controls printing of types of
   158   constants when displaying a goal state.
   159 
   160   Note that the output can be enormous, because polymorphic constants
   161   often occur at several different type instances.
   162 
   163   \item @{attribute show_abbrevs} controls folding of constant
   164   abbreviations.
   165 
   166   \item @{attribute show_brackets} controls bracketing in pretty
   167   printed output.  If enabled, all sub-expressions of the pretty
   168   printing tree will be parenthesized, even if this produces malformed
   169   term syntax!  This crude way of showing the internal structure of
   170   pretty printed entities may occasionally help to diagnose problems
   171   with operator priorities, for example.
   172 
   173   \item @{attribute names_long}, @{attribute names_short}, and
   174   @{attribute names_unique} control the way of printing fully
   175   qualified internal names in external form.  See also
   176   \secref{sec:antiq} for the document antiquotation options of the
   177   same names.
   178 
   179   \item @{attribute eta_contract} controls @{text "\<eta>"}-contracted
   180   printing of terms.
   181 
   182   The @{text \<eta>}-contraction law asserts @{prop "(\<lambda>x. f x) \<equiv> f"},
   183   provided @{text x} is not free in @{text f}.  It asserts
   184   \emph{extensionality} of functions: @{prop "f \<equiv> g"} if @{prop "f x \<equiv>
   185   g x"} for all @{text x}.  Higher-order unification frequently puts
   186   terms into a fully @{text \<eta>}-expanded form.  For example, if @{text
   187   F} has type @{text "(\<tau> \<Rightarrow> \<tau>) \<Rightarrow> \<tau>"} then its expanded form is @{term
   188   "\<lambda>h. F (\<lambda>x. h x)"}.
   189 
   190   Enabling @{attribute eta_contract} makes Isabelle perform @{text
   191   \<eta>}-contractions before printing, so that @{term "\<lambda>h. F (\<lambda>x. h x)"}
   192   appears simply as @{text F}.
   193 
   194   Note that the distinction between a term and its @{text \<eta>}-expanded
   195   form occasionally matters.  While higher-order resolution and
   196   rewriting operate modulo @{text "\<alpha>\<beta>\<eta>"}-conversion, some other tools
   197   might look at terms more discretely.
   198 
   199   \item @{attribute goals_limit} controls the maximum number of
   200   subgoals to be shown in goal output.
   201 
   202   \item @{attribute show_main_goal} controls whether the main result
   203   to be proven should be displayed.  This information might be
   204   relevant for schematic goals, to inspect the current claim that has
   205   been synthesized so far.
   206 
   207   \item @{attribute show_hyps} controls printing of implicit
   208   hypotheses of local facts.  Normally, only those hypotheses are
   209   displayed that are \emph{not} covered by the assumptions of the
   210   current context: this situation indicates a fault in some tool being
   211   used.
   212 
   213   By enabling @{attribute show_hyps}, output of \emph{all} hypotheses
   214   can be enforced, which is occasionally useful for diagnostic
   215   purposes.
   216 
   217   \item @{attribute show_tags} controls printing of extra annotations
   218   within theorems, such as internal position information, or the case
   219   names being attached by the attribute @{attribute case_names}.
   220 
   221   Note that the @{attribute tagged} and @{attribute untagged}
   222   attributes provide low-level access to the collection of tags
   223   associated with a theorem.
   224 
   225   \item @{attribute show_question_marks} controls printing of question
   226   marks for schematic variables, such as @{text ?x}.  Only the leading
   227   question mark is affected, the remaining text is unchanged
   228   (including proper markup for schematic variables that might be
   229   relevant for user interfaces).
   230 
   231   \end{description}
   232 *}
   233 
   234 
   235 subsection {* Alternative print modes \label{sec:print-modes} *}
   236 
   237 text {*
   238   \begin{mldecls}
   239     @{index_ML print_mode_value: "unit -> string list"} \\
   240     @{index_ML Print_Mode.with_modes: "string list -> ('a -> 'b) -> 'a -> 'b"} \\
   241   \end{mldecls}
   242 
   243   The \emph{print mode} facility allows to modify various operations
   244   for printing.  Commands like @{command typ}, @{command term},
   245   @{command thm} (see \secref{sec:print-diag}) take additional print
   246   modes as optional argument.  The underlying ML operations are as
   247   follows.
   248 
   249   \begin{description}
   250 
   251   \item @{ML "print_mode_value ()"} yields the list of currently
   252   active print mode names.  This should be understood as symbolic
   253   representation of certain individual features for printing (with
   254   precedence from left to right).
   255 
   256   \item @{ML Print_Mode.with_modes}~@{text "modes f x"} evaluates
   257   @{text "f x"} in an execution context where the print mode is
   258   prepended by the given @{text "modes"}.  This provides a thread-safe
   259   way to augment print modes.  It is also monotonic in the set of mode
   260   names: it retains the default print mode that certain
   261   user-interfaces might have installed for their proper functioning!
   262 
   263   \end{description}
   264 
   265   \begin{warn}
   266   The old global reference @{ML print_mode} should never be used
   267   directly in applications.  Its main reason for being publicly
   268   accessible is to support historic versions of Proof~General.
   269   \end{warn}
   270 
   271   \medskip The pretty printer for inner syntax maintains alternative
   272   mixfix productions for any print mode name invented by the user, say
   273   in commands like @{command notation} or @{command abbreviation}.
   274   Mode names can be arbitrary, but the following ones have a specific
   275   meaning by convention:
   276 
   277   \begin{itemize}
   278 
   279   \item @{verbatim "\"\""} (the empty string): default mode;
   280   implicitly active as last element in the list of modes.
   281 
   282   \item @{verbatim input}: dummy print mode that is never active; may
   283   be used to specify notation that is only available for input.
   284 
   285   \item @{verbatim internal} dummy print mode that is never active;
   286   used internally in Isabelle/Pure.
   287 
   288   \item @{verbatim xsymbols}: enable proper mathematical symbols
   289   instead of ASCII art.\footnote{This traditional mode name stems from
   290   the ``X-Symbol'' package for old versions Proof~General with XEmacs,
   291   although that package has been superseded by Unicode in recent
   292   years.}
   293 
   294   \item @{verbatim HTML}: additional mode that is active in HTML
   295   presentation of Isabelle theory sources; allows to provide
   296   alternative output notation.
   297 
   298   \item @{verbatim latex}: additional mode that is active in {\LaTeX}
   299   document preparation of Isabelle theory sources; allows to provide
   300   alternative output notation.
   301 
   302   \end{itemize}
   303 *}
   304 
   305 
   306 subsection {* Printing limits *}
   307 
   308 text {*
   309   \begin{mldecls}
   310     @{index_ML Pretty.margin_default: "int Unsynchronized.ref"} \\
   311     @{index_ML print_depth: "int -> unit"} \\
   312   \end{mldecls}
   313 
   314   These ML functions set limits for pretty printed text.
   315 
   316   \begin{description}
   317 
   318   \item @{ML Pretty.margin_default} indicates the global default for
   319   the right margin of the built-in pretty printer, with initial value
   320   76.  Note that user-interfaces typically control margins
   321   automatically when resizing windows, or even bypass the formatting
   322   engine of Isabelle/ML altogether and do it within the front end via
   323   Isabelle/Scala.
   324 
   325   \item @{ML print_depth}~@{text n} limits the printing depth of the
   326   ML toplevel pretty printer; the precise effect depends on the ML
   327   compiler and run-time system.  Typically @{text n} should be less
   328   than 10.  Bigger values such as 100--1000 are useful for debugging.
   329 
   330   \end{description}
   331 *}
   332 
   333 
   334 section {* Mixfix annotations \label{sec:mixfix} *}
   335 
   336 text {* Mixfix annotations specify concrete \emph{inner syntax} of
   337   Isabelle types and terms.  Locally fixed parameters in toplevel
   338   theorem statements, locale and class specifications also admit
   339   mixfix annotations in a fairly uniform manner.  A mixfix annotation
   340   describes describes the concrete syntax, the translation to abstract
   341   syntax, and the pretty printing.  Special case annotations provide a
   342   simple means of specifying infix operators and binders.
   343 
   344   Isabelle mixfix syntax is inspired by {\OBJ} \cite{OBJ}.  It allows
   345   to specify any context-free priority grammar, which is more general
   346   than the fixity declarations of ML and Prolog.
   347 
   348   @{rail "
   349     @{syntax_def mixfix}: '(' mfix ')'
   350     ;
   351     @{syntax_def struct_mixfix}: '(' ( mfix | @'structure' ) ')'
   352     ;
   353 
   354     mfix: @{syntax template} prios? @{syntax nat}? |
   355       (@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} |
   356       @'binder' @{syntax template} prios? @{syntax nat}
   357     ;
   358     template: string
   359     ;
   360     prios: '[' (@{syntax nat} + ',') ']'
   361   "}
   362 
   363   The string given as @{text template} may include literal text,
   364   spacing, blocks, and arguments (denoted by ``@{text _}''); the
   365   special symbol ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'')
   366   represents an index argument that specifies an implicit structure
   367   reference (see also \secref{sec:locale}).  Infix and binder
   368   declarations provide common abbreviations for particular mixfix
   369   declarations.  So in practice, mixfix templates mostly degenerate to
   370   literal text for concrete syntax, such as ``@{verbatim "++"}'' for
   371   an infix symbol.
   372 *}
   373 
   374 
   375 subsection {* The general mixfix form *}
   376 
   377 text {* In full generality, mixfix declarations work as follows.
   378   Suppose a constant @{text "c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} is annotated by
   379   @{text "(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)"}, where @{text "mixfix"} is a string
   380   @{text "d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n"} consisting of delimiters that surround
   381   argument positions as indicated by underscores.
   382 
   383   Altogether this determines a production for a context-free priority
   384   grammar, where for each argument @{text "i"} the syntactic category
   385   is determined by @{text "\<tau>\<^sub>i"} (with priority @{text "p\<^sub>i"}), and the
   386   result category is determined from @{text "\<tau>"} (with priority @{text
   387   "p"}).  Priority specifications are optional, with default 0 for
   388   arguments and 1000 for the result.\footnote{Omitting priorities is
   389   prone to syntactic ambiguities unless the delimiter tokens determine
   390   fully bracketed notation, as in @{text "if _ then _ else _ fi"}.}
   391 
   392   Since @{text "\<tau>"} may be again a function type, the constant
   393   type scheme may have more argument positions than the mixfix
   394   pattern.  Printing a nested application @{text "c t\<^sub>1 \<dots> t\<^sub>m"} for
   395   @{text "m > n"} works by attaching concrete notation only to the
   396   innermost part, essentially by printing @{text "(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m"}
   397   instead.  If a term has fewer arguments than specified in the mixfix
   398   template, the concrete syntax is ignored.
   399 
   400   \medskip A mixfix template may also contain additional directives
   401   for pretty printing, notably spaces, blocks, and breaks.  The
   402   general template format is a sequence over any of the following
   403   entities.
   404 
   405   \begin{description}
   406 
   407   \item @{text "d"} is a delimiter, namely a non-empty sequence of
   408   characters other than the following special characters:
   409 
   410   \smallskip
   411   \begin{tabular}{ll}
   412     @{verbatim "'"} & single quote \\
   413     @{verbatim "_"} & underscore \\
   414     @{text "\<index>"} & index symbol \\
   415     @{verbatim "("} & open parenthesis \\
   416     @{verbatim ")"} & close parenthesis \\
   417     @{verbatim "/"} & slash \\
   418   \end{tabular}
   419   \medskip
   420 
   421   \item @{verbatim "'"} escapes the special meaning of these
   422   meta-characters, producing a literal version of the following
   423   character, unless that is a blank.
   424 
   425   A single quote followed by a blank separates delimiters, without
   426   affecting printing, but input tokens may have additional white space
   427   here.
   428 
   429   \item @{verbatim "_"} is an argument position, which stands for a
   430   certain syntactic category in the underlying grammar.
   431 
   432   \item @{text "\<index>"} is an indexed argument position; this is the place
   433   where implicit structure arguments can be attached.
   434 
   435   \item @{text "s"} is a non-empty sequence of spaces for printing.
   436   This and the following specifications do not affect parsing at all.
   437 
   438   \item @{verbatim "("}@{text n} opens a pretty printing block.  The
   439   optional number specifies how much indentation to add when a line
   440   break occurs within the block.  If the parenthesis is not followed
   441   by digits, the indentation defaults to 0.  A block specified via
   442   @{verbatim "(00"} is unbreakable.
   443 
   444   \item @{verbatim ")"} closes a pretty printing block.
   445 
   446   \item @{verbatim "//"} forces a line break.
   447 
   448   \item @{verbatim "/"}@{text s} allows a line break.  Here @{text s}
   449   stands for the string of spaces (zero or more) right after the
   450   slash.  These spaces are printed if the break is \emph{not} taken.
   451 
   452   \end{description}
   453 
   454   The general idea of pretty printing with blocks and breaks is also
   455   described in \cite{paulson-ml2}; it goes back to \cite{Oppen:1980}.
   456 *}
   457 
   458 
   459 subsection {* Infixes *}
   460 
   461 text {* Infix operators are specified by convenient short forms that
   462   abbreviate general mixfix annotations as follows:
   463 
   464   \begin{center}
   465   \begin{tabular}{lll}
   466 
   467   @{verbatim "("}@{keyword_def "infix"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"}
   468   & @{text "\<mapsto>"} &
   469   @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p + 1"}@{verbatim ", "}@{text "p + 1"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\
   470   @{verbatim "("}@{keyword_def "infixl"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"}
   471   & @{text "\<mapsto>"} &
   472   @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p"}@{verbatim ", "}@{text "p + 1"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\
   473   @{verbatim "("}@{keyword_def "infixr"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"}
   474   & @{text "\<mapsto>"} &
   475   @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p + 1"}@{verbatim ", "}@{text "p"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\
   476 
   477   \end{tabular}
   478   \end{center}
   479 
   480   The mixfix template @{verbatim "\"(_ "}@{text sy}@{verbatim "/ _)\""}
   481   specifies two argument positions; the delimiter is preceded by a
   482   space and followed by a space or line break; the entire phrase is a
   483   pretty printing block.
   484 
   485   The alternative notation @{verbatim "op"}~@{text sy} is introduced
   486   in addition.  Thus any infix operator may be written in prefix form
   487   (as in ML), independently of the number of arguments in the term.
   488 *}
   489 
   490 
   491 subsection {* Binders *}
   492 
   493 text {* A \emph{binder} is a variable-binding construct such as a
   494   quantifier.  The idea to formalize @{text "\<forall>x. b"} as @{text "All
   495   (\<lambda>x. b)"} for @{text "All :: ('a \<Rightarrow> bool) \<Rightarrow> bool"} already goes back
   496   to \cite{church40}.  Isabelle declarations of certain higher-order
   497   operators may be annotated with @{keyword_def "binder"} annotations
   498   as follows:
   499 
   500   \begin{center}
   501   @{text "c :: "}@{verbatim "\""}@{text "(\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2) \<Rightarrow> \<tau>\<^sub>3"}@{verbatim "\"  ("}@{keyword "binder"}@{verbatim " \""}@{text "sy"}@{verbatim "\" ["}@{text "p"}@{verbatim "] "}@{text "q"}@{verbatim ")"}
   502   \end{center}
   503 
   504   This introduces concrete binder syntax @{text "sy x. b"}, where
   505   @{text x} is a bound variable of type @{text "\<tau>\<^sub>1"}, the body @{text
   506   b} has type @{text "\<tau>\<^sub>2"} and the whole term has type @{text "\<tau>\<^sub>3"}.
   507   The optional integer @{text p} specifies the syntactic priority of
   508   the body; the default is @{text "q"}, which is also the priority of
   509   the whole construct.
   510 
   511   Internally, the binder syntax is expanded to something like this:
   512   \begin{center}
   513   @{text "c_binder :: "}@{verbatim "\""}@{text "idts \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3"}@{verbatim "\"  (\"(3"}@{text sy}@{verbatim "_./ _)\" [0, "}@{text "p"}@{verbatim "] "}@{text "q"}@{verbatim ")"}
   514   \end{center}
   515 
   516   Here @{syntax (inner) idts} is the nonterminal symbol for a list of
   517   identifiers with optional type constraints (see also
   518   \secref{sec:pure-grammar}).  The mixfix template @{verbatim
   519   "\"(3"}@{text sy}@{verbatim "_./ _)\""} defines argument positions
   520   for the bound identifiers and the body, separated by a dot with
   521   optional line break; the entire phrase is a pretty printing block of
   522   indentation level 3.  Note that there is no extra space after @{text
   523   "sy"}, so it needs to be included user specification if the binder
   524   syntax ends with a token that may be continued by an identifier
   525   token at the start of @{syntax (inner) idts}.
   526 
   527   Furthermore, a syntax translation to transforms @{text "c_binder x\<^sub>1
   528   \<dots> x\<^sub>n b"} into iterated application @{text "c (\<lambda>x\<^sub>1. \<dots> c (\<lambda>x\<^sub>n. b)\<dots>)"}.
   529   This works in both directions, for parsing and printing.  *}
   530 
   531 
   532 section {* Explicit notation \label{sec:notation} *}
   533 
   534 text {*
   535   \begin{matharray}{rcll}
   536     @{command_def "type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   537     @{command_def "no_type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   538     @{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   539     @{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   540     @{command_def "write"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
   541   \end{matharray}
   542 
   543   Commands that introduce new logical entities (terms or types)
   544   usually allow to provide mixfix annotations on the spot, which is
   545   convenient for default notation.  Nonetheless, the syntax may be
   546   modified later on by declarations for explicit notation.  This
   547   allows to add or delete mixfix annotations for of existing logical
   548   entities within the current context.
   549 
   550   @{rail "
   551     (@@{command type_notation} | @@{command no_type_notation}) @{syntax target}?
   552       @{syntax mode}? \\ (@{syntax nameref} @{syntax mixfix} + @'and')
   553     ;
   554     (@@{command notation} | @@{command no_notation}) @{syntax target}? @{syntax mode}? \\
   555       (@{syntax nameref} @{syntax struct_mixfix} + @'and')
   556     ;
   557     @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax struct_mixfix} + @'and')
   558   "}
   559 
   560   \begin{description}
   561 
   562   \item @{command "type_notation"}~@{text "c (mx)"} associates mixfix
   563   syntax with an existing type constructor.  The arity of the
   564   constructor is retrieved from the context.
   565 
   566   \item @{command "no_type_notation"} is similar to @{command
   567   "type_notation"}, but removes the specified syntax annotation from
   568   the present context.
   569 
   570   \item @{command "notation"}~@{text "c (mx)"} associates mixfix
   571   syntax with an existing constant or fixed variable.  The type
   572   declaration of the given entity is retrieved from the context.
   573 
   574   \item @{command "no_notation"} is similar to @{command "notation"},
   575   but removes the specified syntax annotation from the present
   576   context.
   577 
   578   \item @{command "write"} is similar to @{command "notation"}, but
   579   works within an Isar proof body.
   580 
   581   \end{description}
   582 *}
   583 
   584 
   585 section {* The Pure syntax \label{sec:pure-syntax} *}
   586 
   587 subsection {* Lexical matters \label{sec:inner-lex} *}
   588 
   589 text {* The inner lexical syntax vaguely resembles the outer one
   590   (\secref{sec:outer-lex}), but some details are different.  There are
   591   two main categories of inner syntax tokens:
   592 
   593   \begin{enumerate}
   594 
   595   \item \emph{delimiters} --- the literal tokens occurring in
   596   productions of the given priority grammar (cf.\
   597   \secref{sec:priority-grammar});
   598 
   599   \item \emph{named tokens} --- various categories of identifiers etc.
   600 
   601   \end{enumerate}
   602 
   603   Delimiters override named tokens and may thus render certain
   604   identifiers inaccessible.  Sometimes the logical context admits
   605   alternative ways to refer to the same entity, potentially via
   606   qualified names.
   607 
   608   \medskip The categories for named tokens are defined once and for
   609   all as follows, reusing some categories of the outer token syntax
   610   (\secref{sec:outer-lex}).
   611 
   612   \begin{center}
   613   \begin{supertabular}{rcl}
   614     @{syntax_def (inner) id} & = & @{syntax_ref ident} \\
   615     @{syntax_def (inner) longid} & = & @{syntax_ref longident} \\
   616     @{syntax_def (inner) var} & = & @{syntax_ref var} \\
   617     @{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\
   618     @{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\
   619     @{syntax_def (inner) num_token} & = & @{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat} \\
   620     @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
   621     @{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text "  |  "}@{verbatim "#-"}@{syntax_ref nat} \\
   622 
   623     @{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
   624   \end{supertabular}
   625   \end{center}
   626 
   627   The token categories @{syntax (inner) num_token}, @{syntax (inner)
   628   float_token}, @{syntax (inner) xnum_token}, and @{syntax (inner)
   629   str_token} are not used in Pure.  Object-logics may implement numerals
   630   and string constants by adding appropriate syntax declarations,
   631   together with some translation functions (e.g.\ see Isabelle/HOL).
   632 
   633   The derived categories @{syntax_def (inner) num_const}, @{syntax_def
   634   (inner) float_const}, and @{syntax_def (inner) num_const} provide
   635   robust access to the respective tokens: the syntax tree holds a
   636   syntactic constant instead of a free variable.
   637 *}
   638 
   639 
   640 subsection {* Priority grammars \label{sec:priority-grammar} *}
   641 
   642 text {* A context-free grammar consists of a set of \emph{terminal
   643   symbols}, a set of \emph{nonterminal symbols} and a set of
   644   \emph{productions}.  Productions have the form @{text "A = \<gamma>"},
   645   where @{text A} is a nonterminal and @{text \<gamma>} is a string of
   646   terminals and nonterminals.  One designated nonterminal is called
   647   the \emph{root symbol}.  The language defined by the grammar
   648   consists of all strings of terminals that can be derived from the
   649   root symbol by applying productions as rewrite rules.
   650 
   651   The standard Isabelle parser for inner syntax uses a \emph{priority
   652   grammar}.  Each nonterminal is decorated by an integer priority:
   653   @{text "A\<^sup>(\<^sup>p\<^sup>)"}.  In a derivation, @{text "A\<^sup>(\<^sup>p\<^sup>)"} may be rewritten
   654   using a production @{text "A\<^sup>(\<^sup>q\<^sup>) = \<gamma>"} only if @{text "p \<le> q"}.  Any
   655   priority grammar can be translated into a normal context-free
   656   grammar by introducing new nonterminals and productions.
   657 
   658   \medskip Formally, a set of context free productions @{text G}
   659   induces a derivation relation @{text "\<longrightarrow>\<^sub>G"} as follows.  Let @{text
   660   \<alpha>} and @{text \<beta>} denote strings of terminal or nonterminal symbols.
   661   Then @{text "\<alpha> A\<^sup>(\<^sup>p\<^sup>) \<beta> \<longrightarrow>\<^sub>G \<alpha> \<gamma> \<beta>"} holds if and only if @{text G}
   662   contains some production @{text "A\<^sup>(\<^sup>q\<^sup>) = \<gamma>"} for @{text "p \<le> q"}.
   663 
   664   \medskip The following grammar for arithmetic expressions
   665   demonstrates how binding power and associativity of operators can be
   666   enforced by priorities.
   667 
   668   \begin{center}
   669   \begin{tabular}{rclr}
   670   @{text "A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "="} & @{verbatim "("} @{text "A\<^sup>(\<^sup>0\<^sup>)"} @{verbatim ")"} \\
   671   @{text "A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "="} & @{verbatim 0} \\
   672   @{text "A\<^sup>(\<^sup>0\<^sup>)"} & @{text "="} & @{text "A\<^sup>(\<^sup>0\<^sup>)"} @{verbatim "+"} @{text "A\<^sup>(\<^sup>1\<^sup>)"} \\
   673   @{text "A\<^sup>(\<^sup>2\<^sup>)"} & @{text "="} & @{text "A\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "*"} @{text "A\<^sup>(\<^sup>2\<^sup>)"} \\
   674   @{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "="} & @{verbatim "-"} @{text "A\<^sup>(\<^sup>3\<^sup>)"} \\
   675   \end{tabular}
   676   \end{center}
   677   The choice of priorities determines that @{verbatim "-"} binds
   678   tighter than @{verbatim "*"}, which binds tighter than @{verbatim
   679   "+"}.  Furthermore @{verbatim "+"} associates to the left and
   680   @{verbatim "*"} to the right.
   681 
   682   \medskip For clarity, grammars obey these conventions:
   683   \begin{itemize}
   684 
   685   \item All priorities must lie between 0 and 1000.
   686 
   687   \item Priority 0 on the right-hand side and priority 1000 on the
   688   left-hand side may be omitted.
   689 
   690   \item The production @{text "A\<^sup>(\<^sup>p\<^sup>) = \<alpha>"} is written as @{text "A = \<alpha>
   691   (p)"}, i.e.\ the priority of the left-hand side actually appears in
   692   a column on the far right.
   693 
   694   \item Alternatives are separated by @{text "|"}.
   695 
   696   \item Repetition is indicated by dots @{text "(\<dots>)"} in an informal
   697   but obvious way.
   698 
   699   \end{itemize}
   700 
   701   Using these conventions, the example grammar specification above
   702   takes the form:
   703   \begin{center}
   704   \begin{tabular}{rclc}
   705     @{text A} & @{text "="} & @{verbatim "("} @{text A} @{verbatim ")"} \\
   706               & @{text "|"} & @{verbatim 0} & \qquad\qquad \\
   707               & @{text "|"} & @{text A} @{verbatim "+"} @{text "A\<^sup>(\<^sup>1\<^sup>)"} & @{text "(0)"} \\
   708               & @{text "|"} & @{text "A\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "*"} @{text "A\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
   709               & @{text "|"} & @{verbatim "-"} @{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
   710   \end{tabular}
   711   \end{center}
   712 *}
   713 
   714 
   715 subsection {* The Pure grammar \label{sec:pure-grammar} *}
   716 
   717 text {* The priority grammar of the @{text "Pure"} theory is defined
   718   approximately like this:
   719 
   720   \begin{center}
   721   \begin{supertabular}{rclr}
   722 
   723   @{syntax_def (inner) any} & = & @{text "prop  |  logic"} \\\\
   724 
   725   @{syntax_def (inner) prop} & = & @{verbatim "("} @{text prop} @{verbatim ")"} \\
   726     & @{text "|"} & @{text "prop\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\
   727     & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
   728     & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{text "\<equiv>"} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
   729     & @{text "|"} & @{text "prop\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "&&&"} @{text "prop\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
   730     & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
   731     & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
   732     & @{text "|"} & @{verbatim "[|"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{verbatim "|]"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
   733     & @{text "|"} & @{text "\<lbrakk>"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{text "\<rbrakk>"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
   734     & @{text "|"} & @{verbatim "!!"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\
   735     & @{text "|"} & @{text "\<And>"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\
   736     & @{text "|"} & @{verbatim OFCLASS} @{verbatim "("} @{text type} @{verbatim ","} @{text logic} @{verbatim ")"} \\
   737     & @{text "|"} & @{verbatim SORT_CONSTRAINT} @{verbatim "("} @{text type} @{verbatim ")"} \\
   738     & @{text "|"} & @{verbatim TERM} @{text logic} \\
   739     & @{text "|"} & @{verbatim PROP} @{text aprop} \\\\
   740 
   741   @{syntax_def (inner) aprop} & = & @{verbatim "("} @{text aprop} @{verbatim ")"} \\
   742     & @{text "|"} & @{text "id  |  longid  |  var  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "..."} \\
   743     & @{text "|"} & @{verbatim CONST} @{text "id  |  "}@{verbatim CONST} @{text "longid"} \\
   744     & @{text "|"} & @{verbatim XCONST} @{text "id  |  "}@{verbatim XCONST} @{text "longid"} \\
   745     & @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)  any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\\\
   746 
   747   @{syntax_def (inner) logic} & = & @{verbatim "("} @{text logic} @{verbatim ")"} \\
   748     & @{text "|"} & @{text "logic\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\
   749     & @{text "|"} & @{text "id  |  longid  |  var  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "..."} \\
   750     & @{text "|"} & @{verbatim CONST} @{text "id  |  "}@{verbatim CONST} @{text "longid"} \\
   751     & @{text "|"} & @{verbatim XCONST} @{text "id  |  "}@{verbatim XCONST} @{text "longid"} \\
   752     & @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)  any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\
   753     & @{text "|"} & @{text "\<struct> index\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} \\
   754     & @{text "|"} & @{verbatim "%"} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
   755     & @{text "|"} & @{text \<lambda>} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
   756     & @{text "|"} & @{verbatim op} @{verbatim "=="}@{text "  |  "}@{verbatim op} @{text "\<equiv>"}@{text "  |  "}@{verbatim op} @{verbatim "&&&"} \\
   757     & @{text "|"} & @{verbatim op} @{verbatim "==>"}@{text "  |  "}@{verbatim op} @{text "\<Longrightarrow>"} \\
   758     & @{text "|"} & @{verbatim TYPE} @{verbatim "("} @{text type} @{verbatim ")"} \\\\
   759 
   760   @{syntax_def (inner) idt} & = & @{verbatim "("} @{text idt} @{verbatim ")"}@{text "  |  id  |  "}@{verbatim "_"} \\
   761     & @{text "|"} & @{text id} @{verbatim "::"} @{text type} & @{text "(0)"} \\
   762     & @{text "|"} & @{verbatim "_"} @{verbatim "::"} @{text type} & @{text "(0)"} \\\\
   763 
   764   @{syntax_def (inner) index} & = & @{verbatim "\<^bsub>"} @{text "logic\<^sup>(\<^sup>0\<^sup>)"} @{verbatim "\<^esub>"}@{text "  |  |  \<index>"} \\\\
   765 
   766   @{syntax_def (inner) idts} & = & @{text "idt  |  idt\<^sup>(\<^sup>1\<^sup>) idts"} & @{text "(0)"} \\\\
   767 
   768   @{syntax_def (inner) pttrn} & = & @{text idt} \\\\
   769 
   770   @{syntax_def (inner) pttrns} & = & @{text "pttrn  |  pttrn\<^sup>(\<^sup>1\<^sup>) pttrns"} & @{text "(0)"} \\\\
   771 
   772   @{syntax_def (inner) type} & = & @{verbatim "("} @{text type} @{verbatim ")"} \\
   773     & @{text "|"} & @{text "tid  |  tvar  |  "}@{verbatim "_"} \\
   774     & @{text "|"} & @{text "tid"} @{verbatim "::"} @{text "sort  |  tvar  "}@{verbatim "::"} @{text "sort  |  "}@{verbatim "_"} @{verbatim "::"} @{text "sort"} \\
   775     & @{text "|"} & @{text "type_name  |  type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) type_name"} \\
   776     & @{text "|"} & @{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text type_name} \\
   777     & @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\
   778     & @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\
   779     & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\
   780     & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\
   781   @{syntax_def (inner) type_name} & = & @{text "id  |  longid"} \\\\
   782 
   783   @{syntax_def (inner) sort} & = & @{syntax class_name}~@{text "  |  "}@{verbatim "{}"} \\
   784     & @{text "|"} & @{verbatim "{"} @{syntax class_name} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{syntax class_name} @{verbatim "}"} \\
   785   @{syntax_def (inner) class_name} & = & @{text "id  |  longid"} \\
   786   \end{supertabular}
   787   \end{center}
   788 
   789   \medskip Here literal terminals are printed @{verbatim "verbatim"};
   790   see also \secref{sec:inner-lex} for further token categories of the
   791   inner syntax.  The meaning of the nonterminals defined by the above
   792   grammar is as follows:
   793 
   794   \begin{description}
   795 
   796   \item @{syntax_ref (inner) any} denotes any term.
   797 
   798   \item @{syntax_ref (inner) prop} denotes meta-level propositions,
   799   which are terms of type @{typ prop}.  The syntax of such formulae of
   800   the meta-logic is carefully distinguished from usual conventions for
   801   object-logics.  In particular, plain @{text "\<lambda>"}-term notation is
   802   \emph{not} recognized as @{syntax (inner) prop}.
   803 
   804   \item @{syntax_ref (inner) aprop} denotes atomic propositions, which
   805   are embedded into regular @{syntax (inner) prop} by means of an
   806   explicit @{verbatim PROP} token.
   807 
   808   Terms of type @{typ prop} with non-constant head, e.g.\ a plain
   809   variable, are printed in this form.  Constants that yield type @{typ
   810   prop} are expected to provide their own concrete syntax; otherwise
   811   the printed version will appear like @{syntax (inner) logic} and
   812   cannot be parsed again as @{syntax (inner) prop}.
   813 
   814   \item @{syntax_ref (inner) logic} denotes arbitrary terms of a
   815   logical type, excluding type @{typ prop}.  This is the main
   816   syntactic category of object-logic entities, covering plain @{text
   817   \<lambda>}-term notation (variables, abstraction, application), plus
   818   anything defined by the user.
   819 
   820   When specifying notation for logical entities, all logical types
   821   (excluding @{typ prop}) are \emph{collapsed} to this single category
   822   of @{syntax (inner) logic}.
   823 
   824   \item @{syntax_ref (inner) index} denotes an optional index term for
   825   indexed syntax.  If omitted, it refers to the first @{keyword
   826   "structure"} variable in the context.  The special dummy ``@{text
   827   "\<index>"}'' serves as pattern variable in mixfix annotations that
   828   introduce indexed notation.
   829 
   830   \item @{syntax_ref (inner) idt} denotes identifiers, possibly
   831   constrained by types.
   832 
   833   \item @{syntax_ref (inner) idts} denotes a sequence of @{syntax_ref
   834   (inner) idt}.  This is the most basic category for variables in
   835   iterated binders, such as @{text "\<lambda>"} or @{text "\<And>"}.
   836 
   837   \item @{syntax_ref (inner) pttrn} and @{syntax_ref (inner) pttrns}
   838   denote patterns for abstraction, cases bindings etc.  In Pure, these
   839   categories start as a merely copy of @{syntax (inner) idt} and
   840   @{syntax (inner) idts}, respectively.  Object-logics may add
   841   additional productions for binding forms.
   842 
   843   \item @{syntax_ref (inner) type} denotes types of the meta-logic.
   844 
   845   \item @{syntax_ref (inner) sort} denotes meta-level sorts.
   846 
   847   \end{description}
   848 
   849   Here are some further explanations of certain syntax features.
   850 
   851   \begin{itemize}
   852 
   853   \item In @{syntax (inner) idts}, note that @{text "x :: nat y"} is
   854   parsed as @{text "x :: (nat y)"}, treating @{text y} like a type
   855   constructor applied to @{text nat}.  To avoid this interpretation,
   856   write @{text "(x :: nat) y"} with explicit parentheses.
   857 
   858   \item Similarly, @{text "x :: nat y :: nat"} is parsed as @{text "x ::
   859   (nat y :: nat)"}.  The correct form is @{text "(x :: nat) (y ::
   860   nat)"}, or @{text "(x :: nat) y :: nat"} if @{text y} is last in the
   861   sequence of identifiers.
   862 
   863   \item Type constraints for terms bind very weakly.  For example,
   864   @{text "x < y :: nat"} is normally parsed as @{text "(x < y) ::
   865   nat"}, unless @{text "<"} has a very low priority, in which case the
   866   input is likely to be ambiguous.  The correct form is @{text "x < (y
   867   :: nat)"}.
   868 
   869   \item Constraints may be either written with two literal colons
   870   ``@{verbatim "::"}'' or the double-colon symbol @{verbatim "\<Colon>"},
   871   which actually looks exactly the same in some {\LaTeX} styles.
   872 
   873   \item Dummy variables (written as underscore) may occur in different
   874   roles.
   875 
   876   \begin{description}
   877 
   878   \item A type ``@{text "_"}'' or ``@{text "_ :: sort"}'' acts like an
   879   anonymous inference parameter, which is filled-in according to the
   880   most general type produced by the type-checking phase.
   881 
   882   \item A bound ``@{text "_"}'' refers to a vacuous abstraction, where
   883   the body does not refer to the binding introduced here.  As in the
   884   term @{term "\<lambda>x _. x"}, which is @{text "\<alpha>"}-equivalent to @{text
   885   "\<lambda>x y. x"}.
   886 
   887   \item A free ``@{text "_"}'' refers to an implicit outer binding.
   888   Higher definitional packages usually allow forms like @{text "f x _
   889   = x"}.
   890 
   891   \item A schematic ``@{text "_"}'' (within a term pattern, see
   892   \secref{sec:term-decls}) refers to an anonymous variable that is
   893   implicitly abstracted over its context of locally bound variables.
   894   For example, this allows pattern matching of @{text "{x. f x = g
   895   x}"} against @{text "{x. _ = _}"}, or even @{text "{_. _ = _}"} by
   896   using both bound and schematic dummies.
   897 
   898   \end{description}
   899 
   900   \item The three literal dots ``@{verbatim "..."}'' may be also
   901   written as ellipsis symbol @{verbatim "\<dots>"}.  In both cases this
   902   refers to a special schematic variable, which is bound in the
   903   context.  This special term abbreviation works nicely with
   904   calculational reasoning (\secref{sec:calculation}).
   905 
   906   \item @{verbatim CONST} ensures that the given identifier is treated
   907   as constant term, and passed through the parse tree in fully
   908   internalized form.  This is particularly relevant for translation
   909   rules (\secref{sec:syn-trans}), notably on the RHS.
   910 
   911   \item @{verbatim XCONST} is similar to @{verbatim CONST}, but
   912   retains the constant name as given.  This is only relevant to
   913   translation rules (\secref{sec:syn-trans}), notably on the LHS.
   914 
   915   \end{itemize}
   916 *}
   917 
   918 
   919 subsection {* Inspecting the syntax *}
   920 
   921 text {*
   922   \begin{matharray}{rcl}
   923     @{command_def "print_syntax"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   924   \end{matharray}
   925 
   926   \begin{description}
   927 
   928   \item @{command "print_syntax"} prints the inner syntax of the
   929   current context.  The output can be quite large; the most important
   930   sections are explained below.
   931 
   932   \begin{description}
   933 
   934   \item @{text "lexicon"} lists the delimiters of the inner token
   935   language; see \secref{sec:inner-lex}.
   936 
   937   \item @{text "prods"} lists the productions of the underlying
   938   priority grammar; see \secref{sec:priority-grammar}.
   939 
   940   The nonterminal @{text "A\<^sup>(\<^sup>p\<^sup>)"} is rendered in plain text as @{text
   941   "A[p]"}; delimiters are quoted.  Many productions have an extra
   942   @{text "\<dots> => name"}.  These names later become the heads of parse
   943   trees; they also guide the pretty printer.
   944 
   945   Productions without such parse tree names are called \emph{copy
   946   productions}.  Their right-hand side must have exactly one
   947   nonterminal symbol (or named token).  The parser does not create a
   948   new parse tree node for copy productions, but simply returns the
   949   parse tree of the right-hand symbol.
   950 
   951   If the right-hand side of a copy production consists of a single
   952   nonterminal without any delimiters, then it is called a \emph{chain
   953   production}.  Chain productions act as abbreviations: conceptually,
   954   they are removed from the grammar by adding new productions.
   955   Priority information attached to chain productions is ignored; only
   956   the dummy value @{text "-1"} is displayed.
   957 
   958   \item @{text "print modes"} lists the alternative print modes
   959   provided by this grammar; see \secref{sec:print-modes}.
   960 
   961   \item @{text "parse_rules"} and @{text "print_rules"} relate to
   962   syntax translations (macros); see \secref{sec:syn-trans}.
   963 
   964   \item @{text "parse_ast_translation"} and @{text
   965   "print_ast_translation"} list sets of constants that invoke
   966   translation functions for abstract syntax trees, which are only
   967   required in very special situations; see \secref{sec:tr-funs}.
   968 
   969   \item @{text "parse_translation"} and @{text "print_translation"}
   970   list the sets of constants that invoke regular translation
   971   functions; see \secref{sec:tr-funs}.
   972 
   973   \end{description}
   974 
   975   \end{description}
   976 *}
   977 
   978 
   979 subsection {* Ambiguity of parsed expressions *}
   980 
   981 text {*
   982   \begin{tabular}{rcll}
   983     @{attribute_def syntax_ambiguity_warning} & : & @{text attribute} & default @{text true} \\
   984     @{attribute_def syntax_ambiguity_limit} & : & @{text attribute} & default @{text 10} \\
   985   \end{tabular}
   986 
   987   Depending on the grammar and the given input, parsing may be
   988   ambiguous.  Isabelle lets the Earley parser enumerate all possible
   989   parse trees, and then tries to make the best out of the situation.
   990   Terms that cannot be type-checked are filtered out, which often
   991   leads to a unique result in the end.  Unlike regular type
   992   reconstruction, which is applied to the whole collection of input
   993   terms simultaneously, the filtering stage only treats each given
   994   term in isolation.  Filtering is also not attempted for individual
   995   types or raw ASTs (as required for @{command translations}).
   996 
   997   Certain warning or error messages are printed, depending on the
   998   situation and the given configuration options.  Parsing ultimately
   999   fails, if multiple results remain after the filtering phase.
  1000 
  1001   \begin{description}
  1002 
  1003   \item @{attribute syntax_ambiguity_warning} controls output of
  1004   explicit warning messages about syntax ambiguity.
  1005 
  1006   \item @{attribute syntax_ambiguity_limit} determines the number of
  1007   resulting parse trees that are shown as part of the printed message
  1008   in case of an ambiguity.
  1009 
  1010   \end{description}
  1011 *}
  1012 
  1013 
  1014 section {* Raw syntax and translations \label{sec:syn-trans} *}
  1015 
  1016 text {*
  1017   \begin{matharray}{rcl}
  1018     @{command_def "nonterminal"} & : & @{text "theory \<rightarrow> theory"} \\
  1019     @{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\
  1020     @{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\
  1021     @{command_def "translations"} & : & @{text "theory \<rightarrow> theory"} \\
  1022     @{command_def "no_translations"} & : & @{text "theory \<rightarrow> theory"} \\
  1023   \end{matharray}
  1024 
  1025   Unlike mixfix notation for existing formal entities
  1026   (\secref{sec:notation}), raw syntax declarations provide full access
  1027   to the priority grammar of the inner syntax.  This includes
  1028   additional syntactic categories (via @{command nonterminal}) and
  1029   free-form grammar productions (via @{command syntax}).  Additional
  1030   syntax translations (or macros, via @{command translations}) are
  1031   required to turn resulting parse trees into proper representations
  1032   of formal entities again.
  1033 
  1034   @{rail "
  1035     @@{command nonterminal} (@{syntax name} + @'and')
  1036     ;
  1037     (@@{command syntax} | @@{command no_syntax}) @{syntax mode}? (constdecl +)
  1038     ;
  1039     (@@{command translations} | @@{command no_translations})
  1040       (transpat ('==' | '=>' | '<=' | '\<rightleftharpoons>' | '\<rightharpoonup>' | '\<leftharpoondown>') transpat +)
  1041     ;
  1042 
  1043     constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
  1044     ;
  1045     mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')')
  1046     ;
  1047     transpat: ('(' @{syntax nameref} ')')? @{syntax string}
  1048   "}
  1049 
  1050   \begin{description}
  1051 
  1052   \item @{command "nonterminal"}~@{text c} declares a type
  1053   constructor @{text c} (without arguments) to act as purely syntactic
  1054   type: a nonterminal symbol of the inner syntax.
  1055 
  1056   \item @{command "syntax"}~@{text "(mode) c :: \<sigma> (mx)"} augments the
  1057   priority grammar and the pretty printer table for the given print
  1058   mode (default @{verbatim "\"\""}). An optional keyword @{keyword_ref
  1059   "output"} means that only the pretty printer table is affected.
  1060 
  1061   Following \secref{sec:mixfix}, the mixfix annotation @{text "mx =
  1062   template ps q"} together with type @{text "\<sigma> = \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} and
  1063   specify a grammar production.  The @{text template} contains
  1064   delimiter tokens that surround @{text "n"} argument positions
  1065   (@{verbatim "_"}).  The latter correspond to nonterminal symbols
  1066   @{text "A\<^sub>i"} derived from the argument types @{text "\<tau>\<^sub>i"} as
  1067   follows:
  1068   \begin{itemize}
  1069 
  1070   \item @{text "prop"} if @{text "\<tau>\<^sub>i = prop"}
  1071 
  1072   \item @{text "logic"} if @{text "\<tau>\<^sub>i = (\<dots>)\<kappa>"} for logical type
  1073   constructor @{text "\<kappa> \<noteq> prop"}
  1074 
  1075   \item @{text any} if @{text "\<tau>\<^sub>i = \<alpha>"} for type variables
  1076 
  1077   \item @{text "\<kappa>"} if @{text "\<tau>\<^sub>i = \<kappa>"} for nonterminal @{text "\<kappa>"}
  1078   (syntactic type constructor)
  1079 
  1080   \end{itemize}
  1081 
  1082   Each @{text "A\<^sub>i"} is decorated by priority @{text "p\<^sub>i"} from the
  1083   given list @{text "ps"}; misssing priorities default to 0.
  1084 
  1085   The resulting nonterminal of the production is determined similarly
  1086   from type @{text "\<tau>"}, with priority @{text "q"} and default 1000.
  1087 
  1088   \medskip Parsing via this production produces parse trees @{text
  1089   "t\<^sub>1, \<dots>, t\<^sub>n"} for the argument slots.  The resulting parse tree is
  1090   composed as @{text "c t\<^sub>1 \<dots> t\<^sub>n"}, by using the syntax constant @{text
  1091   "c"} of the syntax declaration.
  1092 
  1093   Such syntactic constants are invented on the spot, without formal
  1094   check wrt.\ existing declarations.  It is conventional to use plain
  1095   identifiers prefixed by a single underscore (e.g.\ @{text
  1096   "_foobar"}).  Names should be chosen with care, to avoid clashes
  1097   with unrelated syntax declarations.
  1098 
  1099   \medskip The special case of copy production is specified by @{text
  1100   "c = "}@{verbatim "\"\""} (empty string).  It means that the
  1101   resulting parse tree @{text "t"} is copied directly, without any
  1102   further decoration.
  1103 
  1104   \item @{command "no_syntax"}~@{text "(mode) decls"} removes grammar
  1105   declarations (and translations) resulting from @{text decls}, which
  1106   are interpreted in the same manner as for @{command "syntax"} above.
  1107 
  1108   \item @{command "translations"}~@{text rules} specifies syntactic
  1109   translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}),
  1110   parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}).
  1111   Translation patterns may be prefixed by the syntactic category to be
  1112   used for parsing; the default is @{text logic}.
  1113 
  1114   \item @{command "no_translations"}~@{text rules} removes syntactic
  1115   translation rules, which are interpreted in the same manner as for
  1116   @{command "translations"} above.
  1117 
  1118   \end{description}
  1119 
  1120   Raw syntax and translations provides a slightly more low-level
  1121   access to the grammar and the form of resulting parse trees.  It is
  1122   often possible to avoid this untyped macro mechanism, and use
  1123   type-safe @{command abbreviation} or @{command notation} instead.
  1124   Some important situations where @{command syntax} and @{command
  1125   translations} are really need are as follows:
  1126 
  1127   \begin{itemize}
  1128 
  1129   \item Iterated replacement via recursive @{command translations}.
  1130   For example, consider list enumeration @{term "[a, b, c, d]"} as
  1131   defined in theory @{theory List} in Isabelle/HOL.
  1132 
  1133   \item Change of binding status of variables: anything beyond the
  1134   built-in @{keyword "binder"} mixfix annotation requires explicit
  1135   syntax translations.  For example, consider list filter
  1136   comprehension @{term "[x \<leftarrow> xs . P]"} as defined in theory @{theory
  1137   List} in Isabelle/HOL.
  1138 
  1139   \end{itemize}
  1140 *}
  1141 
  1142 
  1143 section {* Syntax translation functions \label{sec:tr-funs} *}
  1144 
  1145 text {*
  1146   \begin{matharray}{rcl}
  1147     @{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
  1148     @{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\
  1149     @{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
  1150     @{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
  1151     @{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
  1152   \end{matharray}
  1153 
  1154   @{rail "
  1155   ( @@{command parse_ast_translation} | @@{command parse_translation} |
  1156     @@{command print_translation} | @@{command typed_print_translation} |
  1157     @@{command print_ast_translation}) ('(' @'advanced' ')')? @{syntax text}
  1158   "}
  1159 
  1160   Syntax translation functions written in ML admit almost arbitrary
  1161   manipulations of Isabelle's inner syntax.  Any of the above commands
  1162   have a single @{syntax text} argument that refers to an ML
  1163   expression of appropriate type, which are as follows by default:
  1164 
  1165 %FIXME proper antiquotations
  1166 \begin{ttbox}
  1167 val parse_ast_translation   : (string * (ast list -> ast)) list
  1168 val parse_translation       : (string * (term list -> term)) list
  1169 val print_translation       : (string * (term list -> term)) list
  1170 val typed_print_translation : (string * (typ -> term list -> term)) list
  1171 val print_ast_translation   : (string * (ast list -> ast)) list
  1172 \end{ttbox}
  1173 
  1174   If the @{text "(advanced)"} option is given, the corresponding
  1175   translation functions may depend on the current theory or proof
  1176   context.  This allows to implement advanced syntax mechanisms, as
  1177   translations functions may refer to specific theory declarations or
  1178   auxiliary proof data.
  1179 
  1180 %FIXME proper antiquotations
  1181 \begin{ttbox}
  1182 val parse_ast_translation:
  1183   (string * (Proof.context -> ast list -> ast)) list
  1184 val parse_translation:
  1185   (string * (Proof.context -> term list -> term)) list
  1186 val print_translation:
  1187   (string * (Proof.context -> term list -> term)) list
  1188 val typed_print_translation:
  1189   (string * (Proof.context -> typ -> term list -> term)) list
  1190 val print_ast_translation:
  1191   (string * (Proof.context -> ast list -> ast)) list
  1192 \end{ttbox}
  1193 
  1194   \medskip See also the chapter on ``Syntax Transformations'' in old
  1195   \cite{isabelle-ref} for further details on translations on parse
  1196   trees.
  1197 *}
  1198 
  1199 end