doc-src/Logics/defining.tex

tuned;

+
−%% $Id$
+
−%%  \([a-zA-Z][a-zA-Z]}\.\) \([^ ]\)             \1  \2
+
−%%  @\([a-z0-9]\)       ^{(\1)}
+
−
+
−\newcommand\rmindex[1]{{#1}\index{#1}\@}
+
−\newcommand\mtt[1]{\mbox{\tt #1}}
+
−\newcommand\ttfct[1]{\mathop{\mtt{#1}}\nolimits}
+
−\newcommand\ttapp{\mathrel{\hbox{\tt\$}}}
+
−\newcommand\Constant{\ttfct{Constant}}
+
−\newcommand\Variable{\ttfct{Variable}}
+
−\newcommand\Appl[1]{\ttfct{Appl}\mathopen{\mtt[}#1\mathclose{\mtt]}}
+
−\newcommand\AST{{\sc ast}}
+
−\let\rew=\longrightarrow
+
−
+
−
+
−\chapter{Defining Logics} \label{Defining-Logics}
+
−
+
−This chapter explains how to define new formal systems --- in particular,
+
−their concrete syntax.  While Isabelle can be regarded as a theorem prover
+
−for set theory, higher-order logic or the sequent calculus, its
+
−distinguishing feature is support for the definition of new logics.
+
−
+
−Isabelle logics are hierarchies of theories, which are described and
+
−illustrated in {\em Introduction to Isabelle}.  That material, together
+
−with the theory files provided in the examples directories, should suffice
+
−for all simple applications.  The easiest way to define a new theory is by
+
−modifying a copy of an existing theory.
+
−
+
−This chapter is intended for experienced Isabelle users.  It documents all
+
−aspects of theories concerned with syntax: mixfix declarations, pretty
+
−printing, macros and translation functions.  The extended examples of
+
−\S\ref{sec:min_logics} demonstrate the logical aspects of the definition of
+
−theories.  Sections marked with * are highly technical and might be skipped
+
−on the first reading.
+
−
+
−
+
−\section{Priority grammars} \label{sec:priority_grammars}
+
−\index{grammars!priority|(} 
+
−
+
−The syntax of an Isabelle logic is specified by a {\bf priority grammar}.
+
−A context-free grammar\index{grammars!context-free} contains a set of
+
−productions of the form $A=\gamma$, where $A$ is a nonterminal and
+
−$\gamma$, the right-hand side, is a string of terminals and nonterminals.
+
−Isabelle uses an extended format permitting {\bf priorities}, or
+
−precedences.  Each nonterminal is decorated by an integer priority, as
+
−in~$A^{(p)}$.  A nonterminal $A^{(p)}$ in a derivation may be replaced
+
−using a production $A^{(q)} = \gamma$ only if $p \le q$.  Any priority
+
−grammar can be translated into a normal context free grammar by introducing
+
−new nonterminals and productions.
+
−
+
−Formally, a set of context free productions $G$ induces a derivation
+
−relation $\rew@G$.  Let $\alpha$ and $\beta$ denote strings of terminal or
+
−nonterminal symbols.  Then
+
−\[ \alpha\, A^{(p)}\, \beta ~\rew@G~ \alpha\,\gamma\,\beta \] 
+
−if and only if $G$ contains some production $A^{(q)}=\gamma$ for~$q\ge p$.
+
−
+
−The following simple grammar for arithmetic expressions demonstrates how
+
−binding power and associativity of operators can be enforced by priorities.
+
−\begin{center}
+
−\begin{tabular}{rclr}
+
−  $A^{(9)}$ & = & {\tt0} \\
+
−  $A^{(9)}$ & = & {\tt(} $A^{(0)}$ {\tt)} \\
+
−  $A^{(0)}$ & = & $A^{(0)}$ {\tt+} $A^{(1)}$ \\
+
−  $A^{(2)}$ & = & $A^{(3)}$ {\tt*} $A^{(2)}$ \\
+
−  $A^{(3)}$ & = & {\tt-} $A^{(3)}$
+
−\end{tabular}
+
−\end{center}
+
−The choice of priorities determines that {\tt -} binds tighter than {\tt *},
+
−which binds tighter than {\tt +}.  Furthermore {\tt +} associates to the
+
−left and {\tt *} to the right.
+
−
+
−To minimize the number of subscripts, we adopt the following conventions:
+
−\begin{itemize}
+
−\item All priorities $p$ must be in the range $0 \leq p \leq max_pri$ for
+
−  some fixed integer $max_pri$.
+
−\item Priority $0$ on the right-hand side and priority $max_pri$ on the
+
−  left-hand side may be omitted.
+
−\end{itemize}
+
−The production $A^{(p)} = \alpha$ is written as $A = \alpha~(p)$;
+
−the priority of the left-hand side actually appears in a column on the far
+
−right.  Finally, alternatives may be separated by $|$, and repetition
+
−indicated by \dots.
+
−
+
−Using these conventions and assuming $max_pri=9$, the grammar takes the form
+
−\begin{center}
+
−\begin{tabular}{rclc}
+
−$A$ & = & {\tt0} & \hspace*{4em} \\
+
− & $|$ & {\tt(} $A$ {\tt)} \\
+
− & $|$ & $A$ {\tt+} $A^{(1)}$ & (0) \\
+
− & $|$ & $A^{(3)}$ {\tt*} $A^{(2)}$ & (2) \\
+
− & $|$ & {\tt-} $A^{(3)}$ & (3)
+
−\end{tabular}
+
−\end{center}
+
−\index{grammars!priority|)}
+
−
+
−
+
−\begin{figure}
+
−\begin{center}
+
−\begin{tabular}{rclc}
+
−$prop$ &=& \ttindex{PROP} $aprop$ ~~$|$~~ {\tt(} $prop$ {\tt)} \\
+
−     &$|$& $logic^{(3)}$ \ttindex{==} $logic^{(2)}$ & (2) \\
+
−     &$|$& $logic^{(3)}$ \ttindex{=?=} $logic^{(2)}$ & (2) \\
+
−     &$|$& $prop^{(2)}$ \ttindex{==>} $prop^{(1)}$ & (1) \\
+
−     &$|$& {\tt[|} $prop$ {\tt;} \dots {\tt;} $prop$ {\tt|]} {\tt==>} $prop^{(1)}$ & (1) \\
+
−     &$|$& {\tt!!} $idts$ {\tt.} $prop$ & (0) \\\\
+
−$logic$ &=& $prop$ ~~$|$~~ $fun$ \\\\
+
−$aprop$ &=& $id$ ~~$|$~~ $var$
+
−    ~~$|$~~ $fun^{(max_pri)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\\\
+
−$fun$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $fun$ {\tt)} \\
+
−    &$|$& $fun^{(max_pri)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\
+
−    &$|$& $fun^{(max_pri)}$ {\tt::} $type$ \\
+
−    &$|$& \ttindex{\%} $idts$ {\tt.} $logic$ & (0) \\\\
+
−$idts$ &=& $idt$ ~~$|$~~ $idt^{(1)}$ $idts$ \\\\
+
−$idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\
+
−    &$|$& $id$ \ttindex{::} $type$ & (0) \\\\
+
−$type$ &=& $tid$ ~~$|$~~ $tvar$ ~~$|$~~ $tid$ {\tt::} $sort$
+
−  ~~$|$~~ $tvar$ {\tt::} $sort$ \\
+
−     &$|$& $id$ ~~$|$~~ $type^{(max_pri)}$ $id$
+
−                ~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $id$ \\
+
−     &$|$& $type^{(1)}$ \ttindex{=>} $type$ & (0) \\
+
−     &$|$& {\tt[}  $type$ {\tt,} \dots {\tt,} $type$ {\tt]} {\tt=>} $type$&(0)\\
+
−     &$|$& {\tt(} $type$ {\tt)} \\\\
+
−$sort$ &=& $id$ ~~$|$~~ {\tt\ttlbrace\ttrbrace}
+
−                ~~$|$~~ {\tt\ttlbrace} $id$ {\tt,} \dots {\tt,} $id$ {\tt\ttrbrace}
+
−\end{tabular}\index{*"!"!}\index{*"["|}\index{*"|"]}
+
−\indexbold{type@$type$} \indexbold{sort@$sort$} \indexbold{idt@$idt$}
+
−\indexbold{idts@$idts$} \indexbold{logic@$logic$} \indexbold{prop@$prop$}
+
−\indexbold{fun@$fun$}
+
−\end{center}
+
−\caption{Meta-logic syntax}\label{fig:pure_gram}
+
−\end{figure}
+
−
+
−
+
−\section{The Pure syntax} \label{sec:basic_syntax}
+
−\index{syntax!Pure|(}
+
−
+
−At the root of all object-logics lies the Pure theory,\index{theory!Pure}
+
−bound to the \ML{} identifier \ttindex{Pure.thy}.  It contains, among many
+
−other things, the Pure syntax. An informal account of this basic syntax
+
−(meta-logic, types, \ldots) may be found in {\em Introduction to Isabelle}.
+
−A more precise description using a priority grammar is shown in
+
−Fig.\ts\ref{fig:pure_gram}.  The following nonterminals are defined:
+
−\begin{description}
+
−  \item[$prop$] Terms of type $prop$.  These are formulae of the meta-logic.
+
−
+
−  \item[$aprop$] Atomic propositions.  These typically include the
+
−    judgement forms of the object-logic; its definition introduces a
+
−    meta-level predicate for each judgement form.
+
−
+
−  \item[$logic$] Terms whose type belongs to class $logic$.  Initially,
+
−    this category contains just $prop$.  As the syntax is extended by new
+
−    object-logics, more productions for $logic$ are added automatically
+
−    (see below).
+
−
+
−  \item[$fun$] Terms potentially of function type.
+
−
+
−  \item[$type$] Types of the meta-logic.
+
−
+
−  \item[$idts$] A list of identifiers, possibly constrained by types.  
+
−\end{description}
+
−
+
−\begin{warn}
+
−  Note that \verb|x::nat y| is parsed as \verb|x::(nat y)|, treating {\tt
+
−    y} like a type constructor applied to {\tt nat}.  The likely result is
+
−  an error message.  To avoid this interpretation, use parentheses and
+
−  write \verb|(x::nat) y|.
+
−
+
−  Similarly, \verb|x::nat y::nat| is parsed as \verb|x::(nat y::nat)| and
+
−  yields a syntax error.  The correct form is \verb|(x::nat) (y::nat)|.
+
−\end{warn}
+
−
+
−\subsection{Logical types and default syntax}\label{logical-types}
+
−Isabelle's representation of mathematical languages is based on the typed
+
−$\lambda$-calculus.  All logical types, namely those of class $logic$, are
+
−automatically equipped with a basic syntax of types, identifiers,
+
−variables, parentheses, $\lambda$-abstractions and applications.  
+
−
+
−More precisely, for each type constructor $ty$ with arity $(\vec{s})c$,
+
−where $c$ is a subclass of $logic$, several productions are added:
+
−\begin{center}
+
−\begin{tabular}{rclc}
+
−$ty$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $ty$ {\tt)} \\
+
−  &$|$& $fun^{(max_pri)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)}\\
+
−  &$|$& $ty^{(max_pri)}$ {\tt::} $type$\\\\
+
−$logic$ &=& $ty$
+
−\end{tabular}
+
−\end{center}
+
−
+
−
+
−\subsection{Lexical matters}
+
−The parser does not process input strings directly.  It operates on token
+
−lists provided by Isabelle's \bfindex{lexer}.  There are two kinds of
+
−tokens: \bfindex{delimiters} and \bfindex{name tokens}.
+
−
+
−Delimiters can be regarded as reserved words of the syntax.  You can
+
−add new ones when extending theories.  In Fig.\ts\ref{fig:pure_gram} they
+
−appear in typewriter font, for example {\tt ==}, {\tt =?=} and
+
−{\tt PROP}\@.
+
−
+
−Name tokens have a predefined syntax.  The lexer distinguishes four
+
−disjoint classes of names: \rmindex{identifiers}, \rmindex{unknowns}, type
+
−identifiers\index{identifiers!type}, type unknowns\index{unknowns!type}.
+
−They are denoted by $id$\index{id@$id$}, $var$\index{var@$var$},
+
−$tid$\index{tid@$tid$}, $tvar$\index{tvar@$tvar$}, respectively.  Typical
+
−examples are {\tt x}, {\tt ?x7}, {\tt 'a}, {\tt ?'a3}.  Here is the precise
+
−syntax:
+
−\begin{eqnarray*}
+
−id        & =   & letter~quasiletter^* \\
+
−var       & =   & \mbox{\tt ?}id ~~|~~ \mbox{\tt ?}id\mbox{\tt .}nat \\
+
−tid     & =   & \mbox{\tt '}id \\
+
−tvar      & =   & \mbox{\tt ?}tid ~~|~~
+
−                  \mbox{\tt ?}tid\mbox{\tt .}nat \\[1ex]
+
−letter    & =   & \mbox{one of {\tt a}\dots {\tt z} {\tt A}\dots {\tt Z}} \\
+
−digit     & =   & \mbox{one of {\tt 0}\dots {\tt 9}} \\
+
−quasiletter & =  & letter ~~|~~ digit ~~|~~ \mbox{\tt _} ~~|~~ \mbox{\tt '} \\
+
−nat       & =   & digit^+
+
−\end{eqnarray*}
+
−A $var$ or $tvar$ describes an unknown, which is internally a pair
+
−of base name and index (\ML\ type \ttindex{indexname}).  These components are
+
−either separated by a dot as in {\tt ?x.1} or {\tt ?x7.3} or
+
−run together as in {\tt ?x1}.  The latter form is possible if the
+
−base name does not end with digits.  If the index is 0, it may be dropped
+
−altogether: {\tt ?x} abbreviates both {\tt ?x0} and {\tt ?x.0}.
+
−
+
−The lexer repeatedly takes the maximal prefix of the input string that
+
−forms a valid token.  A maximal prefix that is both a delimiter and a name
+
−is treated as a delimiter.  Spaces, tabs and newlines are separators; they
+
−never occur within tokens.
+
−
+
−Delimiters need not be separated by white space.  For example, if {\tt -}
+
−is a delimiter but {\tt --} is not, then the string {\tt --} is treated as
+
−two consecutive occurrences of the token~{\tt -}.  In contrast, \ML\ 
+
−treats {\tt --} as a single symbolic name.  The consequence of Isabelle's
+
−more liberal scheme is that the same string may be parsed in different ways
+
−after extending the syntax: after adding {\tt --} as a delimiter, the input
+
−{\tt --} is treated as a single token.
+
−
+
−Name tokens are terminal symbols, strictly speaking, but we can generally
+
−regard them as nonterminals.  This is because a name token carries with it
+
−useful information, the name.  Delimiters, on the other hand, are nothing
+
−but than syntactic sugar.
+
−
+
−
+
−\subsection{*Inspecting the syntax}
+
−\begin{ttbox}
+
−syn_of              : theory -> Syntax.syntax
+
−Syntax.print_syntax : Syntax.syntax -> unit
+
−Syntax.print_gram   : Syntax.syntax -> unit
+
−Syntax.print_trans  : Syntax.syntax -> unit
+
−\end{ttbox}
+
−The abstract type \ttindex{Syntax.syntax} allows manipulation of syntaxes
+
−in \ML.  You can display values of this type by calling the following
+
−functions:
+
−\begin{description}
+
−\item[\ttindexbold{syn_of} {\it thy}] returns the syntax of the Isabelle
+
−  theory~{\it thy} as an \ML\ value.
+
−
+
−\item[\ttindexbold{Syntax.print_syntax} {\it syn}] shows virtually all
+
−  information contained in the syntax {\it syn}.  The displayed output can
+
−  be large.  The following two functions are more selective.
+
−
+
−\item[\ttindexbold{Syntax.print_gram} {\it syn}] shows the grammar part
+
−  of~{\it syn}, namely the lexicon, roots and productions.
+
−
+
−\item[\ttindexbold{Syntax.print_trans} {\it syn}] shows the translation
+
−  part of~{\it syn}, namely the constants, parse/print macros and
+
−  parse/print translations.
+
−\end{description}
+
−
+
−Let us demonstrate these functions by inspecting Pure's syntax.  Even that
+
−is too verbose to display in full.
+
−\begin{ttbox}
+
−Syntax.print_syntax (syn_of Pure.thy);
+
−{\out lexicon: "!!" "\%" "(" ")" "," "." "::" ";" "==" "==>" \dots}
+
−{\out roots: logic type fun prop}
+
−{\out prods:}
+
−{\out   type = tid  (1000)}
+
−{\out   type = tvar  (1000)}
+
−{\out   type = id  (1000)}
+
−{\out   type = tid "::" sort[0]  => "_ofsort" (1000)}
+
−{\out   type = tvar "::" sort[0]  => "_ofsort" (1000)}
+
−{\out   \vdots}
+
−\ttbreak
+
−{\out consts: "_K" "_appl" "_aprop" "_args" "_asms" "_bigimpl" \dots}
+
−{\out parse_ast_translation: "_appl" "_bigimpl" "_bracket"}
+
−{\out   "_idtyp" "_lambda" "_tapp" "_tappl"}
+
−{\out parse_rules:}
+
−{\out parse_translation: "!!" "_K" "_abs" "_aprop"}
+
−{\out print_translation: "all"}
+
−{\out print_rules:}
+
−{\out print_ast_translation: "==>" "_abs" "_idts" "fun"}
+
−\end{ttbox}
+
−
+
−As you can see, the output is divided into labeled sections.  The grammar
+
−is represented by {\tt lexicon}, {\tt roots} and {\tt prods}.  The rest
+
−refers to syntactic translations and macro expansion.  Here is an
+
−explanation of the various sections.
+
−\begin{description}
+
−  \item[\ttindex{lexicon}] lists the delimiters used for lexical
+
−    analysis.\index{delimiters} 
+
−
+
−  \item[\ttindex{roots}] lists the grammar's nonterminal symbols.  You must
+
−    name the desired root when calling lower level functions or specifying
+
−    macros.  Higher level functions usually expect a type and derive the
+
−    actual root as described in~\S\ref{sec:grammar}.
+
−
+
−  \item[\ttindex{prods}] lists the productions of the priority grammar.
+
−    The nonterminal $A^{(n)}$ is rendered in {\sc ascii} as {\tt $A$[$n$]}.
+
−    Each delimiter is quoted.  Some productions are shown with {\tt =>} and
+
−    an attached string.  These strings later become the heads of parse
+
−    trees; they also play a vital role when terms are printed (see
+
−    \S\ref{sec:asts}).
+
−
+
−    Productions with no strings attached are called {\bf copy
+
−      productions}\indexbold{productions!copy}.  Their right-hand side must
+
−    have exactly one nonterminal symbol (or name token).  The parser does
+
−    not create a new parse tree node for copy productions, but simply
+
−    returns the parse tree of the right-hand symbol.
+
−
+
−    If the right-hand side consists of a single nonterminal with no
+
−    delimiters, then the copy production is called a {\bf chain
+
−      production}\indexbold{productions!chain}.  Chain productions should
+
−    be seen as abbreviations: conceptually, they are removed from the
+
−    grammar by adding new productions.  Priority information
+
−    attached to chain productions is ignored, only the dummy value $-1$ is
+
−    displayed.
+
−
+
−  \item[\ttindex{consts}, \ttindex{parse_rules}, \ttindex{print_rules}]
+
−    relate to macros (see \S\ref{sec:macros}).
+
−
+
−  \item[\ttindex{parse_ast_translation}, \ttindex{print_ast_translation}]
+
−    list sets of constants that invoke translation functions for abstract
+
−    syntax trees.  Section \S\ref{sec:asts} below discusses this obscure
+
−    matter. 
+
−
+
−  \item[\ttindex{parse_translation}, \ttindex{print_translation}] list sets
+
−    of constants that invoke translation functions for terms (see
+
−    \S\ref{sec:tr_funs}).
+
−\end{description}
+
−\index{syntax!Pure|)}
+
−
+
−
+
−\section{Mixfix declarations} \label{sec:mixfix}
+
−\index{mixfix declaration|(} 
+
−
+
−When defining a theory, you declare new constants by giving their names,
+
−their type, and an optional {\bf mixfix annotation}.  Mixfix annotations
+
−allow you to extend Isabelle's basic $\lambda$-calculus syntax with
+
−readable notation.  They can express any context-free priority grammar.
+
−Isabelle syntax definitions are inspired by \OBJ~\cite{OBJ}; they are more
+
−general than the priority declarations of \ML\ and Prolog.  
+
−
+
−A mixfix annotation defines a production of the priority grammar.  It
+
−describes the concrete syntax, the translation to abstract syntax, and the
+
−pretty printing.  Special case annotations provide a simple means of
+
−specifying infix operators, binders and so forth.
+
−
+
−\subsection{Grammar productions}\label{sec:grammar}
+
−Let us examine the treatment of the production
+
−\[ A^{(p)}= w@0\, A@1^{(p@1)}\, w@1\, A@2^{(p@2)}\, \ldots\,  
+
−                  A@n^{(p@n)}\, w@n. \]
+
−Here $A@i^{(p@i)}$ is a nonterminal with priority~$p@i$ for $i=1$,
+
−\ldots,~$n$, while $w@0$, \ldots,~$w@n$ are strings of terminals.
+
−In the corresponding mixfix annotation, the priorities are given separately
+
−as $[p@1,\ldots,p@n]$ and~$p$.  The nonterminal symbols are identified with
+
−types~$\tau$, $\tau@1$, \ldots,~$\tau@n$ respectively, and the production's
+
−effect on nonterminals is expressed as the function type
+
−\[ [\tau@1, \ldots, \tau@n]\To \tau. \]
+
−Finally, the template
+
−\[ w@0  \;_\; w@1 \;_\; \ldots \;_\; w@n \]
+
−describes the strings of terminals.
+
−
+
−A simple type is typically declared for each nonterminal symbol.  In
+
−first-order logic, type~$i$ stands for terms and~$o$ for formulae.  Only
+
−the outermost type constructor is taken into account.  For example, any
+
−type of the form $\sigma list$ stands for a list;  productions may refer
+
−to the symbol {\tt list} and will apply lists of any type.
+
−
+
−The symbol associated with a type is called its {\bf root} since it may
+
−serve as the root of a parse tree.  Precisely, the root of $(\tau@1, \dots,
+
−\tau@n)ty$ is $ty$, where $\tau@1$, \ldots, $\tau@n$ are types and $ty$ is
+
−a type constructor.  Type infixes are a special case of this; in
+
−particular, the root of $\tau@1 \To \tau@2$ is {\tt fun}.  Finally, the
+
−root of a type variable is {\tt logic}; general productions might
+
−refer to this nonterminal.
+
−
+
−Identifying nonterminals with types allows a constant's type to specify
+
−syntax as well.  We can declare the function~$f$ to have type $[\tau@1,
+
−\ldots, \tau@n]\To \tau$ and, through a mixfix annotation, specify the
+
−layout of the function's $n$ arguments.  The constant's name, in this
+
−case~$f$, will also serve as the label in the abstract syntax tree.  There
+
−are two exceptions to this treatment of constants:
+
−\begin{enumerate}
+
−  \item A production need not map directly to a logical function.  In this
+
−    case, you must declare a constant whose purpose is purely syntactic.
+
−    By convention such constants begin with the symbol~{\tt\at}, 
+
−    ensuring that they can never be written in formulae.
+
−
+
−  \item A copy production has no associated constant.
+
−\end{enumerate}
+
−There is something artificial about this representation of productions,
+
−but it is convenient, particularly for simple theory extensions.
+
−
+
−\subsection{The general mixfix form}
+
−Here is a detailed account of the general \bfindex{mixfix declaration} as
+
−it may occur within the {\tt consts} section of a {\tt .thy} file.
+
−\begin{center}
+
−  {\tt "$c$" ::\ "$\sigma$" ("$template$" $ps$ $p$)}
+
−\end{center}
+
−This constant declaration and mixfix annotation is interpreted as follows:
+
−\begin{itemize}
+
−\item The string {\tt "$c$"} is the name of the constant associated with
+
−  the production.  If $c$ is empty (given as~{\tt ""}) then this is a copy
+
−  production.\index{productions!copy} Otherwise, parsing an instance of the
+
−  phrase $template$ generates the \AST{} {\tt ("$c$" $a@1$ $\ldots$
+
−    $a@n$)}, where $a@i$ is the \AST{} generated by parsing the $i$-th
+
−  argument.
+
−
+
−  \item The constant $c$, if non-empty, is declared to have type $\sigma$.
+
−
+
−  \item The string $template$ specifies the right-hand side of
+
−    the production.  It has the form
+
−    \[ w@0 \;_\; w@1 \;_\; \ldots \;_\; w@n, \] 
+
−    where each occurrence of \ttindex{_} denotes an
+
−    argument\index{argument!mixfix} position and the~$w@i$ do not
+
−    contain~{\tt _}.  (If you want a literal~{\tt _} in the concrete
+
−    syntax, you must escape it as described below.)  The $w@i$ may
+
−    consist of \rmindex{delimiters}, spaces or \rmindex{pretty
+
−      printing} annotations (see below).
+
−
+
−  \item The type $\sigma$ specifies the production's nonterminal symbols (or name
+
−    tokens).  If $template$ is of the form above then $\sigma$ must be a
+
−    function type with at least~$n$ argument positions, say $\sigma =
+
−    [\tau@1, \dots, \tau@n] \To \tau$.  Nonterminal symbols are derived
+
−    from the type $\tau@1$, \ldots,~$\tau@n$, $\tau$ as described above.
+
−    Any of these may be function types; the corresponding root is then {\tt
+
−      fun}. 
+
−
+
−  \item The optional list~$ps$ may contain at most $n$ integers, say {\tt
+
−      [$p@1$, $\ldots$, $p@m$]}, where $p@i$ is the minimal
+
−    priority\indexbold{priorities} required of any phrase that may appear
+
−    as the $i$-th argument.  Missing priorities default to~$0$.
+
−
+
−  \item The integer $p$ is the priority of this production.  If omitted, it
+
−    defaults to the maximal priority.
+
−
+
−    Priorities, or precedences, range between $0$ and
+
−    $max_pri$\indexbold{max_pri@$max_pri$} (= 1000).
+
−\end{itemize}
+
−
+
−The declaration {\tt $c$ ::\ "$\sigma$" ("$template$")} specifies no
+
−priorities.  The resulting production puts no priority constraints on any
+
−of its arguments and has maximal priority itself.  Omitting priorities in
+
−this manner will introduce syntactic ambiguities unless the production's
+
−right-hand side is fully bracketed, as in \verb|"if _ then _ else _ fi"|.
+
−
+
−\begin{warn}
+
−  Theories must sometimes declare types for purely syntactic purposes.  One
+
−  example is {\tt type}, the built-in type of types.  This is a `type of
+
−  all types' in the syntactic sense only.  Do not declare such types under
+
−  {\tt arities} as belonging to class $logic$, for that would allow their
+
−  use in arbitrary Isabelle expressions~(\S\ref{logical-types}).
+
−\end{warn}
+
−
+
−\subsection{Example: arithmetic expressions}
+
−This theory specification contains a {\tt consts} section with mixfix
+
−declarations encoding the priority grammar from
+
−\S\ref{sec:priority_grammars}:
+
−\begin{ttbox}
+
−EXP = Pure +
+
−types
+
−  exp
+
−arities
+
−  exp :: logic
+
−consts
+
−  "0" :: "exp"                ("0"      9)
+
−  "+" :: "[exp, exp] => exp"  ("_ + _"  [0, 1] 0)
+
−  "*" :: "[exp, exp] => exp"  ("_ * _"  [3, 2] 2)
+
−  "-" :: "exp => exp"         ("- _"    [3] 3)
+
−end
+
−\end{ttbox}
+
−Note that the {\tt arities} declaration causes {\tt exp} to be added to the
+
−syntax' roots.  If you put the text above into a file {\tt exp.thy} and load
+
−it via {\tt use_thy "EXP"}, you can run some tests:
+
−\begin{ttbox}
+
−val read_exp = Syntax.test_read (syn_of EXP.thy) "exp";
+
−{\out val it = fn : string -> unit}
+
−read_exp "0 * 0 * 0 * 0 + 0 + 0 + 0";
+
−{\out tokens: "0" "*" "0" "*" "0" "*" "0" "+" "0" "+" "0" "+" "0"}
+
−{\out raw: ("+" ("+" ("+" ("*" "0" ("*" "0" ("*" "0" "0"))) "0") "0") "0")}
+
−{\out \vdots}
+
−read_exp "0 + - 0 + 0";
+
−{\out tokens: "0" "+" "-" "0" "+" "0"}
+
−{\out raw: ("+" ("+" "0" ("-" "0")) "0")}
+
−{\out \vdots}
+
−\end{ttbox}
+
−The output of \ttindex{Syntax.test_read} includes the token list ({\tt
+
−  tokens}) and the raw \AST{} directly derived from the parse tree,
+
−ignoring parse \AST{} translations.  The rest is tracing information
+
−provided by the macro expander (see \S\ref{sec:macros}).
+
−
+
−Executing {\tt Syntax.print_gram} reveals the productions derived
+
−from our mixfix declarations (lots of additional information deleted):
+
−\begin{ttbox}
+
−Syntax.print_gram (syn_of EXP.thy);
+
−{\out exp = "0"  => "0" (9)}
+
−{\out exp = exp[0] "+" exp[1]  => "+" (0)}
+
−{\out exp = exp[3] "*" exp[2]  => "*" (2)}
+
−{\out exp = "-" exp[3]  => "-" (3)}
+
−\end{ttbox}
+
−
+
−
+
−\subsection{The mixfix template}
+
−Let us take a closer look at the string $template$ appearing in mixfix
+
−annotations.  This string specifies a list of parsing and printing
+
−directives: delimiters\index{delimiter}, arguments\index{argument!mixfix},
+
−spaces, blocks of indentation and line breaks.  These are encoded via the
+
−following character sequences:
+
−
+
−\index{pretty printing|(}
+
−\begin{description}
+
−  \item[~\ttindex_~] An argument\index{argument!mixfix} position, which
+
−    stands for a nonterminal symbol or name token.
+
−
+
−  \item[~$d$~] A \rmindex{delimiter}, namely a non-empty sequence of
+
−    non-special or escaped characters.  Escaping a character\index{escape
+
−      character} means preceding it with a {\tt '} (single quote).  Thus
+
−    you have to write {\tt ''} if you really want a single quote.  You must
+
−    also escape {\tt _}, {\tt (}, {\tt )} and {\tt /}.  Delimiters may
+
−    never contain white space, though.
+
−
+
−  \item[~$s$~] A non-empty sequence of spaces for printing.  This
+
−    and the following specifications do not affect parsing at all.
+
−
+
−  \item[~{\ttindex($n$}~] Open a pretty printing block.  The optional
+
−    number $n$ specifies how much indentation to add when a line break
+
−    occurs within the block.  If {\tt(} is not followed by digits, the
+
−    indentation defaults to~$0$.
+
−
+
−  \item[~\ttindex)~] Close a pretty printing block.
+
−
+
−  \item[~\ttindex{//}~] Force a line break.
+
−
+
−  \item[~\ttindex/$s$~] Allow a line break.  Here $s$ stands for the string
+
−    of spaces (zero or more) right after the {\tt /} character.  These
+
−    spaces are printed if the break is not taken.
+
−\end{description}
+
−Isabelle's pretty printer resembles the one described in
+
−Paulson~\cite{paulson91}.  \index{pretty printing|)}
+
−
+
−
+
−\subsection{Infixes}
+
−\indexbold{infix operators}
+
−Infix operators associating to the left or right can be declared
+
−using {\tt infixl} or {\tt infixr}.
+
−Roughly speaking, the form {\tt $c$ ::\ "$\sigma$" (infixl $p$)}
+
−abbreviates the declarations
+
−\begin{ttbox}
+
−"op \(c\)" :: "\(\sigma\)"   ("op \(c\)")
+
−"op \(c\)" :: "\(\sigma\)"   ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\))
+
−\end{ttbox}
+
−and {\tt $c$ ::\ "$\sigma$" (infixr $p$)} abbreviates the declarations
+
−\begin{ttbox}
+
−"op \(c\)" :: "\(\sigma\)"   ("op \(c\)")
+
−"op \(c\)" :: "\(\sigma\)"   ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\))
+
−\end{ttbox}
+
−The infix operator is declared as a constant with the prefix {\tt op}.
+
−Thus, prefixing infixes with \ttindex{op} makes them behave like ordinary
+
−function symbols, as in \ML.  Special characters occurring in~$c$ must be
+
−escaped, as in delimiters, using a single quote.
+
−
+
−The expanded forms above would be actually illegal in a {\tt .thy} file
+
−because they declare the constant \hbox{\tt"op \(c\)"} twice.
+
−
+
−
+
−\subsection{Binders}
+
−\indexbold{binders}
+
−\begingroup
+
−\def\Q{{\cal Q}}
+
−A {\bf binder} is a variable-binding construct such as a quantifier.  The
+
−binder declaration \indexbold{*binder}
+
−\begin{ttbox}
+
−\(c\) :: "\(\sigma\)"   (binder "\(\Q\)" \(p\))
+
−\end{ttbox}
+
−introduces a constant~$c$ of type~$\sigma$, which must have the form
+
−$(\tau@1 \To \tau@2) \To \tau@3$.  Its concrete syntax is $\Q~x.P$, where
+
−$x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$
+
−and the whole term has type~$\tau@3$.  Special characters in $\Q$ must be
+
−escaped using a single quote.
+
−
+
−Let us declare the quantifier~$\forall$:
+
−\begin{ttbox}
+
−All :: "('a => o) => o"   (binder "ALL " 10)
+
−\end{ttbox}
+
−This let us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL
+
−  $x$.$P$}.  When printing, Isabelle prefers the latter form, but must fall
+
−back on $\mtt{All}(P)$ if $P$ is not an abstraction.  Both $P$ and {\tt ALL
+
−  $x$.$P$} have type~$o$, the type of formulae, while the bound variable
+
−can be polymorphic.
+
−
+
−The binder~$c$ of type $(\sigma \To \tau) \To \tau$ can be nested.  The
+
−external form $\Q~x@1~x@2 \ldots x@n. P$ corresponds to the internal form
+
−\[ c(\lambda x@1. c(\lambda x@2. \ldots c(\lambda x@n. P) \ldots)) \]
+
−
+
−\medskip
+
−The general binder declaration
+
−\begin{ttbox}
+
−\(c\)    :: "(\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)"   (binder "\(\Q\)" \(p\))
+
−\end{ttbox}
+
−is internally expanded to
+
−\begin{ttbox}
+
−\(c\)    :: "(\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)"
+
−"\(\Q\)"\hskip-3pt  :: "[idts, \(\tau@2\)] => \(\tau@3\)"   ("(3\(\Q\)_./ _)" \(p\))
+
−\end{ttbox}
+
−with $idts$ being the nonterminal symbol for a list of $id$s optionally
+
−constrained (see Fig.\ts\ref{fig:pure_gram}).  The declaration also
+
−installs a parse translation\index{translations!parse} for~$\Q$ and a print
+
−translation\index{translations!print} for~$c$ to translate between the
+
−internal and external forms.
+
−\endgroup
+
−
+
−\index{mixfix declaration|)}
+
−
+
−
+
−\section{Example: some minimal logics} \label{sec:min_logics}
+
−This section presents some examples that have a simple syntax.  They
+
−demonstrate how to define new object-logics from scratch.
+
−
+
−First we must define how an object-logic syntax embedded into the
+
−meta-logic.  Since all theorems must conform to the syntax for~$prop$ (see
+
−Fig.\ts\ref{fig:pure_gram}), that syntax has to be extended with the
+
−object-level syntax.  Assume that the syntax of your object-logic defines a
+
−nonterminal symbol~$o$ of formulae.  These formulae can now appear in
+
−axioms and theorems wherever $prop$ does if you add the production
+
−\[ prop ~=~ o. \]
+
−This is not a copy production but a coercion from formulae to propositions:
+
−\begin{ttbox}
+
−Base = Pure +
+
−types
+
−  o
+
−arities
+
−  o :: logic
+
−consts
+
−  Trueprop :: "o => prop"   ("_" 5)
+
−end
+
−\end{ttbox}
+
−The constant {\tt Trueprop} (the name is arbitrary) acts as an invisible
+
−coercion function.  Assuming this definition resides in a file {\tt base.thy},
+
−you have to load it with the command {\tt use_thy "Base"}.
+
−
+
−One of the simplest nontrivial logics is {\bf minimal logic} of
+
−implication.  Its definition in Isabelle needs no advanced features but
+
−illustrates the overall mechanism nicely:
+
−\begin{ttbox}
+
−Hilbert = Base +
+
−consts
+
−  "-->" :: "[o, o] => o"   (infixr 10)
+
−rules
+
−  K     "P --> Q --> P"
+
−  S     "(P --> Q --> R) --> (P --> Q) --> P --> R"
+
−  MP    "[| P --> Q; P |] ==> Q"
+
−end
+
−\end{ttbox}
+
−After loading this definition from the file {\tt hilbert.thy}, you can
+
−start to prove theorems in the logic:
+
−\begin{ttbox}
+
−goal Hilbert.thy "P --> P";
+
−{\out Level 0}
+
−{\out P --> P}
+
−{\out  1.  P --> P}
+
−\ttbreak
+
−by (resolve_tac [Hilbert.MP] 1);
+
−{\out Level 1}
+
−{\out P --> P}
+
−{\out  1.  ?P --> P --> P}
+
−{\out  2.  ?P}
+
−\ttbreak
+
−by (resolve_tac [Hilbert.MP] 1);
+
−{\out Level 2}
+
−{\out P --> P}
+
−{\out  1.  ?P1 --> ?P --> P --> P}
+
−{\out  2.  ?P1}
+
−{\out  3.  ?P}
+
−\ttbreak
+
−by (resolve_tac [Hilbert.S] 1);
+
−{\out Level 3}
+
−{\out P --> P}
+
−{\out  1.  P --> ?Q2 --> P}
+
−{\out  2.  P --> ?Q2}
+
−\ttbreak
+
−by (resolve_tac [Hilbert.K] 1);
+
−{\out Level 4}
+
−{\out P --> P}
+
−{\out  1.  P --> ?Q2}
+
−\ttbreak
+
−by (resolve_tac [Hilbert.K] 1);
+
−{\out Level 5}
+
−{\out P --> P}
+
−{\out No subgoals!}
+
−\end{ttbox}
+
−As we can see, this Hilbert-style formulation of minimal logic is easy to
+
−define but difficult to use.  The following natural deduction formulation is
+
−better:
+
−\begin{ttbox}
+
−MinI = Base +
+
−consts
+
−  "-->" :: "[o, o] => o"   (infixr 10)
+
−rules
+
−  impI  "(P ==> Q) ==> P --> Q"
+
−  impE  "[| P --> Q; P |] ==> Q"
+
−end
+
−\end{ttbox}
+
−Note, however, that although the two systems are equivalent, this fact
+
−cannot be proved within Isabelle.  Axioms {\tt S} and {\tt K} can be
+
−derived in {\tt MinI} (exercise!), but {\tt impI} cannot be derived in {\tt
+
−  Hilbert}.  The reason is that {\tt impI} is only an {\bf admissible} rule
+
−in {\tt Hilbert}, something that can only be shown by induction over all
+
−possible proofs in {\tt Hilbert}.
+
−
+
−We may easily extend minimal logic with falsity:
+
−\begin{ttbox}
+
−MinIF = MinI +
+
−consts
+
−  False :: "o"
+
−rules
+
−  FalseE "False ==> P"
+
−end
+
−\end{ttbox}
+
−On the other hand, we may wish to introduce conjunction only:
+
−\begin{ttbox}
+
−MinC = Base +
+
−consts
+
−  "&" :: "[o, o] => o"   (infixr 30)
+
−\ttbreak
+
−rules
+
−  conjI  "[| P; Q |] ==> P & Q"
+
−  conjE1 "P & Q ==> P"
+
−  conjE2 "P & Q ==> Q"
+
−end
+
−\end{ttbox}
+
−And if we want to have all three connectives together, we create and load a
+
−theory file consisting of a single line:\footnote{We can combine the
+
−  theories without creating a theory file using the ML declaration
+
−\begin{ttbox}
+
−val MinIFC_thy = merge_theories(MinIF,MinC)
+
−\end{ttbox}
+
−\index{*merge_theories|fnote}}
+
−\begin{ttbox}
+
−MinIFC = MinIF + MinC
+
−\end{ttbox}
+
−Now we can prove mixed theorems like
+
−\begin{ttbox}
+
−goal MinIFC.thy "P & False --> Q";
+
−by (resolve_tac [MinI.impI] 1);
+
−by (dresolve_tac [MinC.conjE2] 1);
+
−by (eresolve_tac [MinIF.FalseE] 1);
+
−\end{ttbox}
+
−Try this as an exercise!
+
−
+
−\medskip
+
−Unless you need to define macros or syntax translation functions, you may
+
−skip the rest of this chapter.
+
−
+
−
+
−\section{*Abstract syntax trees} \label{sec:asts}
+
−\index{trees!abstract syntax|(} The parser, given a token list from the
+
−lexer, applies productions to yield a parse tree\index{trees!parse}.  By
+
−applying some internal transformations the parse tree becomes an abstract
+
−syntax tree, or \AST{}.  Macro expansion, further translations and finally
+
−type inference yields a well-typed term\index{terms!obtained from ASTs}.
+
−The printing process is the reverse, except for some subtleties to be
+
−discussed later.
+
−
+
−Figure~\ref{fig:parse_print} outlines the parsing and printing process.
+
−Much of the complexity is due to the macro mechanism.  Using macros, you
+
−can specify most forms of concrete syntax without writing any \ML{} code.
+
−
+
−\begin{figure}
+
−\begin{center}
+
−\begin{tabular}{cl}
+
−string          & \\
+
−$\downarrow$    & parser \\
+
−parse tree      & \\
+
−$\downarrow$    & parse \AST{} translation \\
+
−\AST{}             & \\
+
−$\downarrow$    & \AST{} rewriting (macros) \\
+
−\AST{}             & \\
+
−$\downarrow$    & parse translation, type inference \\
+
−--- well-typed term --- & \\
+
−$\downarrow$    & print translation \\
+
−\AST{}             & \\
+
−$\downarrow$    & \AST{} rewriting (macros) \\
+
−\AST{}             & \\
+
−$\downarrow$    & print \AST{} translation, printer \\
+
−string          &
+
−\end{tabular}
+
−\index{translations!parse}\index{translations!parse AST}
+
−\index{translations!print}\index{translations!print AST}
+
−
+
−\end{center}
+
−\caption{Parsing and printing}\label{fig:parse_print}
+
−\end{figure}
+
−
+
−Abstract syntax trees are an intermediate form between the raw parse trees
+
−and the typed $\lambda$-terms.  An \AST{} is either an atom (constant or
+
−variable) or a list of {\em at least two\/} subtrees.  Internally, they
+
−have type \ttindex{Syntax.ast}: \index{*Constant} \index{*Variable}
+
−\index{*Appl}
+
−\begin{ttbox}
+
−datatype ast = Constant of string
+
−             | Variable of string
+
−             | Appl of ast list
+
−\end{ttbox}
+
−
+
−Isabelle uses an S-expression syntax for abstract syntax trees.  Constant
+
−atoms are shown as quoted strings, variable atoms as non-quoted strings and
+
−applications as a parenthesized list of subtrees.  For example, the \AST
+
−\begin{ttbox}
+
−Appl [Constant "_constrain",
+
−  Appl [Constant "_abs", Variable "x", Variable "t"],
+
−  Appl [Constant "fun", Variable "'a", Variable "'b"]]
+
−\end{ttbox}
+
−is shown as {\tt ("_constrain" ("_abs" x t) ("fun" 'a 'b))}.
+
−Both {\tt ()} and {\tt (f)} are illegal because they have too few
+
−subtrees. 
+
−
+
−The resemblance of Lisp's S-expressions is intentional, but there are two
+
−kinds of atomic symbols: $\Constant x$ and $\Variable x$.  Do not take the
+
−names ``{\tt Constant}'' and ``{\tt Variable}'' too literally; in the later
+
−translation to terms, $\Variable x$ may become a constant, free or bound
+
−variable, even a type constructor or class name; the actual outcome depends
+
−on the context.
+
−
+
−Similarly, you can think of ${\tt (} f~x@1~\ldots~x@n{\tt )}$ as the
+
−application of~$f$ to the arguments $x@1, \ldots, x@n$.  But the kind of
+
−application is determined later by context; it could be a type constructor
+
−applied to types.
+
−
+
−Forms like {\tt (("_abs" x $t$) $u$)} are legal, but \AST{}s are
+
−first-order: the {\tt "_abs"} does not bind the {\tt x} in any way.  Later
+
−at the term level, {\tt ("_abs" x $t$)} will become an {\tt Abs} node and
+
−occurrences of {\tt x} in $t$ will be replaced by bound variables (the term
+
−constructor \ttindex{Bound}).
+
−
+
−
+
−\subsection{Transforming parse trees to \AST{}s}
+
−The parse tree is the raw output of the parser.  Translation functions,
+
−called {\bf parse AST translations}\indexbold{translations!parse AST},
+
−transform the parse tree into an abstract syntax tree.
+
−
+
−The parse tree is constructed by nesting the right-hand sides of the
+
−productions used to recognize the input.  Such parse trees are simply lists
+
−of tokens and constituent parse trees, the latter representing the
+
−nonterminals of the productions.  Let us refer to the actual productions in
+
−the form displayed by {\tt Syntax.print_syntax}.
+
−
+
−Ignoring parse \AST{} translations, parse trees are transformed to \AST{}s
+
−by stripping out delimiters and copy productions.  More precisely, the
+
−mapping $ast_of_pt$\index{ast_of_pt@$ast_of_pt$} is derived from the
+
−productions as follows:
+
−\begin{itemize}
+
−  \item Name tokens: $ast_of_pt(t) = \Variable s$, where $t$ is an $id$,
+
−    $var$, $tid$ or $tvar$ token, and $s$ its associated string.
+
−
+
−  \item Copy productions: $ast_of_pt(\ldots P \ldots) = ast_of_pt(P)$.
+
−    Here $\ldots$ stands for strings of delimiters, which are
+
−    discarded.  $P$ stands for the single constituent that is not a
+
−    delimiter; it is either a nonterminal symbol or a name token.
+
−
+
−  \item $0$-ary productions: $ast_of_pt(\ldots \mtt{=>} c) = \Constant c$.
+
−    Here there are no constituents other than delimiters, which are
+
−    discarded. 
+
−
+
−  \item $n$-ary productions, where $n \ge 1$: delimiters are discarded and
+
−    the remaining constituents $P@1$, \ldots, $P@n$ are built into an
+
−    application whose head constant is~$c$:
+
−    \begin{eqnarray*}
+
−      \lefteqn{ast_of_pt(\ldots P@1 \ldots P@n \ldots \mtt{=>} c)} \\
+
−      &&\qquad{}= \Appl{\Constant c, ast_of_pt(P@1), \ldots, ast_of_pt(P@n)}
+
−    \end{eqnarray*}
+
−\end{itemize}
+
−Figure~\ref{fig:parse_ast} presents some simple examples, where {\tt ==},
+
−{\tt _appl}, {\tt _args}, and so forth name productions of the Pure syntax.
+
−These examples illustrate the need for further translations to make \AST{}s
+
−closer to the typed $\lambda$-calculus.  The Pure syntax provides
+
−predefined parse \AST{} translations\index{translations!parse AST} for
+
−ordinary applications, type applications, nested abstractions, meta
+
−implications and function types.  Figure~\ref{fig:parse_ast_tr} shows their
+
−effect on some representative input strings.
+
−
+
−
+
−\begin{figure}
+
−\begin{center}
+
−\tt\begin{tabular}{ll}
+
−\rm input string    & \rm \AST \\\hline
+
−"f"                 & f \\
+
−"'a"                & 'a \\
+
−"t == u"            & ("==" t u) \\
+
−"f(x)"              & ("_appl" f x) \\
+
−"f(x, y)"           & ("_appl" f ("_args" x y)) \\
+
−"f(x, y, z)"        & ("_appl" f ("_args" x ("_args" y z))) \\
+
−"\%x y.\ t"         & ("_lambda" ("_idts" x y) t) \\
+
−\end{tabular}
+
−\end{center}
+
−\caption{Parsing examples using the Pure syntax}\label{fig:parse_ast} 
+
−\end{figure}
+
−
+
−\begin{figure}
+
−\begin{center}
+
−\tt\begin{tabular}{ll}
+
−\rm input string            & \rm \AST{} \\\hline
+
−"f(x, y, z)"                & (f x y z) \\
+
−"'a ty"                     & (ty 'a) \\
+
−"('a, 'b) ty"               & (ty 'a 'b) \\
+
−"\%x y z.\ t"               & ("_abs" x ("_abs" y ("_abs" z t))) \\
+
−"\%x ::\ 'a.\ t"            & ("_abs" ("_constrain" x 'a) t) \\
+
−"[| P; Q; R |] => S"        & ("==>" P ("==>" Q ("==>" R S))) \\
+
−"['a, 'b, 'c] => 'd"        & ("fun" 'a ("fun" 'b ("fun" 'c 'd)))
+
−\end{tabular}
+
−\end{center}
+
−\caption{Built-in parse \AST{} translations}\label{fig:parse_ast_tr}
+
−\end{figure}
+
−
+
−The names of constant heads in the \AST{} control the translation process.
+
−The list of constants invoking parse \AST{} translations appears in the
+
−output of {\tt Syntax.print_syntax} under {\tt parse_ast_translation}.
+
−
+
−
+
−\subsection{Transforming \AST{}s to terms}
+
−The \AST{}, after application of macros (see \S\ref{sec:macros}), is
+
−transformed into a term.  This term is probably ill-typed since type
+
−inference has not occurred yet.  The term may contain type constraints
+
−consisting of applications with head {\tt "_constrain"}; the second
+
−argument is a type encoded as a term.  Type inference later introduces
+
−correct types or rejects the input.
+
−
+
−Another set of translation functions, namely parse
+
−translations,\index{translations!parse}, may affect this process.  If we
+
−ignore parse translations for the time being, then \AST{}s are transformed
+
−to terms by mapping \AST{} constants to constants, \AST{} variables to
+
−schematic or free variables and \AST{} applications to applications.
+
−
+
−More precisely, the mapping $term_of_ast$\index{term_of_ast@$term_of_ast$}
+
−is defined by
+
−\begin{itemize}
+
−\item Constants: $term_of_ast(\Constant x) = \ttfct{Const} (x,
+
−  \mtt{dummyT})$.
+
−
+
−\item Schematic variables: $term_of_ast(\Variable \mtt{"?}xi\mtt") =
+
−  \ttfct{Var} ((x, i), \mtt{dummyT})$, where $x$ is the base name and $i$
+
−  the index extracted from $xi$.
+
−
+
−\item Free variables: $term_of_ast(\Variable x) = \ttfct{Free} (x,
+
−  \mtt{dummyT})$.
+
−
+
−\item Function applications with $n$ arguments:
+
−    \begin{eqnarray*}
+
−      \lefteqn{term_of_ast(\Appl{f, x@1, \ldots, x@n})} \\
+
−      &&\qquad{}= term_of_ast(f) \ttapp
+
−         term_of_ast(x@1) \ttapp \ldots \ttapp term_of_ast(x@n)
+
−    \end{eqnarray*}
+
−\end{itemize}
+
−Here \ttindex{Const}, \ttindex{Var}, \ttindex{Free} and
+
−\verb|$|\index{$@{\tt\$}} are constructors of the datatype {\tt term},
+
−while \ttindex{dummyT} stands for some dummy type that is ignored during
+
−type inference.
+
−
+
−So far the outcome is still a first-order term.  Abstractions and bound
+
−variables (constructors \ttindex{Abs} and \ttindex{Bound}) are introduced
+
−by parse translations.  Such translations are attached to {\tt "_abs"},
+
−{\tt "!!"} and user-defined binders.
+
−
+
−
+
−\subsection{Printing of terms}
+
−The output phase is essentially the inverse of the input phase.  Terms are
+
−translated via abstract syntax trees into strings.  Finally the strings are
+
−pretty printed.
+
−
+
−Print translations (\S\ref{sec:tr_funs}) may affect the transformation of
+
−terms into \AST{}s.  Ignoring those, the transformation maps
+
−term constants, variables and applications to the corresponding constructs
+
−on \AST{}s.  Abstractions are mapped to applications of the special
+
−constant {\tt _abs}.
+
−
+
−More precisely, the mapping $ast_of_term$\index{ast_of_term@$ast_of_term$}
+
−is defined as follows:
+
−\begin{itemize}
+
−  \item $ast_of_term(\ttfct{Const} (x, \tau)) = \Constant x$.
+
−
+
−  \item $ast_of_term(\ttfct{Free} (x, \tau)) = constrain (\Variable x,
+
−    \tau)$.
+
−
+
−  \item $ast_of_term(\ttfct{Var} ((x, i), \tau)) = constrain (\Variable
+
−    \mtt{"?}xi\mtt", \tau)$, where $\mtt?xi$ is the string representation of
+
−    the {\tt indexname} $(x, i)$.
+
−
+
−  \item For the abstraction $\lambda x::\tau.t$, let $x'$ be a variant
+
−    of~$x$ renamed to differ from all names occurring in~$t$, and let $t'$
+
−    be obtained from~$t$ by replacing all bound occurrences of~$x$ by
+
−    the free variable $x'$.  This replaces corresponding occurrences of the
+
−    constructor \ttindex{Bound} by the term $\ttfct{Free} (x',
+
−    \mtt{dummyT})$:
+
−   \begin{eqnarray*}
+
−      \lefteqn{ast_of_term(\ttfct{Abs} (x, \tau, t))} \\
+
−      &&\qquad{}=   \ttfct{Appl}
+
−                  \mathopen{\mtt[} 
+
−                  \Constant \mtt{"_abs"}, constrain(\Variable x', \tau), \\
+
−      &&\qquad\qquad\qquad ast_of_term(t') \mathclose{\mtt]}.
+
−    \end{eqnarray*}
+
−
+
−  \item $ast_of_term(\ttfct{Bound} i) = \Variable \mtt{"B.}i\mtt"$.  
+
−    The occurrence of constructor \ttindex{Bound} should never happen
+
−    when printing well-typed terms; it indicates a de Bruijn index with no
+
−    matching abstraction.
+
−
+
−  \item Where $f$ is not an application,
+
−    \begin{eqnarray*}
+
−      \lefteqn{ast_of_term(f \ttapp x@1 \ttapp \ldots \ttapp x@n)} \\
+
−      &&\qquad{}= \ttfct{Appl} 
+
−                  \mathopen{\mtt[} ast_of_term(f), 
+
−                  ast_of_term(x@1), \ldots,ast_of_term(x@n) 
+
−                  \mathclose{\mtt]}
+
−    \end{eqnarray*}
+
−\end{itemize}
+
−
+
−Type constraints are inserted to allow the printing of types, which is
+
−governed by the boolean variable \ttindex{show_types}.  Constraints are
+
−treated as follows:
+
−\begin{itemize}
+
−  \item $constrain(x, \tau) = x$, if $\tau = \mtt{dummyT}$ \index{*dummyT} or
+
−    \ttindex{show_types} not set to {\tt true}.
+
−
+
−  \item $constrain(x, \tau) = \Appl{\Constant \mtt{"_constrain"}, x, ty}$,
+
−    where $ty$ is the \AST{} encoding of $\tau$.  That is, type constructors as
+
−    {\tt Constant}s, type identifiers as {\tt Variable}s and type applications
+
−    as {\tt Appl}s with the head type constructor as first element.
+
−    Additionally, if \ttindex{show_sorts} is set to {\tt true}, some type
+
−    variables are decorated with an \AST{} encoding of their sort.
+
−\end{itemize}
+
−
+
−The \AST{}, after application of macros (see \S\ref{sec:macros}), is
+
−transformed into the final output string.  The built-in {\bf print AST
+
−  translations}\indexbold{translations!print AST} effectively reverse the
+
−parse \AST{} translations of Fig.\ts\ref{fig:parse_ast_tr}.
+
−
+
−For the actual printing process, the names attached to productions
+
−of the form $\ldots A^{(p@1)}@1 \ldots A^{(p@n)}@n \ldots \mtt{=>} c$ play
+
−a vital role.  Each \AST{} with constant head $c$, namely $\mtt"c\mtt"$ or
+
−$(\mtt"c\mtt"~ x@1 \ldots x@n)$, is printed according to the production
+
−for~$c$.  Each argument~$x@i$ is converted to a string, and put in
+
−parentheses if its priority~$(p@i)$ requires this.  The resulting strings
+
−and their syntactic sugar (denoted by ``\dots'' above) are joined to make a
+
−single string.
+
−
+
−If an application $(\mtt"c\mtt"~ x@1 \ldots x@m)$ has more arguments than the
+
−corresponding production, it is first split into $((\mtt"c\mtt"~ x@1 \ldots
+
−x@n) ~ x@{n+1} \ldots x@m)$. Applications with too few arguments or with
+
−non-constant head or without a corresponding production are printed as
+
−$f(x@1, \ldots, x@l)$ or $(\alpha@1, \ldots, \alpha@l) ty$.  An occurrence of
+
−$\Variable x$ is simply printed as~$x$.
+
−
+
−Blanks are {\em not\/} inserted automatically.  If blanks are required to
+
−separate tokens, specify them in the mixfix declaration, possibly preceeded
+
−by a slash~({\tt/}) to allow a line break.
+
−\index{trees!abstract syntax|)}
+
−
+
−
+
−
+
−\section{*Macros: Syntactic rewriting} \label{sec:macros}
+
−\index{macros|(}\index{rewriting!syntactic|(} 
+
−
+
−Mixfix declarations alone can handle situations where there is a direct
+
−connection between the concrete syntax and the underlying term.  Sometimes
+
−we require a more elaborate concrete syntax, such as quantifiers and list
+
−notation.  Isabelle's {\bf macros} and {\bf translation functions} can
+
−perform translations such as
+
−\begin{center}\tt
+
−  \begin{tabular}{r@{$\quad\protect\rightleftharpoons\quad$}l}
+
−    ALL x:A.P   & Ball(A, \%x.P)        \\ \relax
+
−    [x, y, z]   & Cons(x, Cons(y, Cons(z, Nil)))
+
−  \end{tabular}
+
−\end{center}
+
−Translation functions (see \S\ref{sec:tr_funs}) must be coded in ML; they
+
−are the most powerful translation mechanism but are difficult to read or
+
−write.  Macros are specified by first-order rewriting systems that operate
+
−on abstract syntax trees.  They are usually easy to read and write, and can
+
−express all but the most obscure translations.
+
−
+
−Figure~\ref{fig:set_trans} defines a fragment of first-order logic and set
+
−theory.\footnote{This and the following theories are complete working
+
−  examples, though they specify only syntax, no axioms.  The file {\tt
+
−    ZF/zf.thy} presents the full set theory definition, including many
+
−  macro rules.}  Theory {\tt SET} defines constants for set comprehension
+
−({\tt Collect}), replacement ({\tt Replace}) and bounded universal
+
−quantification ({\tt Ball}).  Each of these binds some variables.  Without
+
−additional syntax we should have to express $\forall x \in A.  P$ as {\tt
+
−  Ball(A,\%x.P)}, and similarly for the others.
+
−
+
−\begin{figure}
+
−\begin{ttbox}
+
−SET = Pure +
+
−types
+
−  i, o
+
−arities
+
−  i, o :: logic
+
−consts
+
−  Trueprop      :: "o => prop"              ("_" 5)
+
−  Collect       :: "[i, i => o] => i"
+
−  "{\at}Collect"    :: "[idt, i, o] => i"       ("(1{\ttlbrace}_:_./ _{\ttrbrace})")
+
−  Replace       :: "[i, [i, i] => o] => i"
+
−  "{\at}Replace"    :: "[idt, idt, i, o] => i"  ("(1{\ttlbrace}_./ _:_, _{\ttrbrace})")
+
−  Ball          :: "[i, i => o] => o"
+
−  "{\at}Ball"       :: "[idt, i, o] => o"       ("(3ALL _:_./ _)" 10)
+
−translations
+
−  "{\ttlbrace}x:A. P{\ttrbrace}"    == "Collect(A, \%x. P)"
+
−  "{\ttlbrace}y. x:A, Q{\ttrbrace}" == "Replace(A, \%x y. Q)"
+
−  "ALL x:A. P"  == "Ball(A, \%x. P)"
+
−end
+
−\end{ttbox}
+
−\caption{Macro example: set theory}\label{fig:set_trans}
+
−\end{figure}
+
−
+
−The theory specifies a variable-binding syntax through additional
+
−productions that have mixfix declarations.  Each non-copy production must
+
−specify some constant, which is used for building \AST{}s.  The additional
+
−constants are decorated with {\tt\at} to stress their purely syntactic
+
−purpose; they should never occur within the final well-typed terms.
+
−Furthermore, they cannot be written in formulae because they are not legal
+
−identifiers.
+
−
+
−The translations cause the replacement of external forms by internal forms
+
−after parsing, and vice versa before printing of terms.  As a specification
+
−of the set theory notation, they should be largely self-explanatory.  The
+
−syntactic constants, {\tt\at Collect}, {\tt\at Replace} and {\tt\at Ball},
+
−appear implicitly in the macro rules via their mixfix forms.
+
−
+
−Macros can define variable-binding syntax because they operate on \AST{}s,
+
−which have no inbuilt notion of bound variable.  The macro variables {\tt
+
−  x} and~{\tt y} have type~{\tt idt} and therefore range over identifiers,
+
−in this case bound variables.  The macro variables {\tt P} and~{\tt Q}
+
−range over formulae containing bound variable occurrences.
+
−
+
−Other applications of the macro system can be less straightforward, and
+
−there are peculiarities.  The rest of this section will describe in detail
+
−how Isabelle macros are preprocessed and applied.
+
−
+
−
+
−\subsection{Specifying macros}
+
−Macros are basically rewrite rules on \AST{}s.  But unlike other macro
+
−systems found in programming languages, Isabelle's macros work in both
+
−directions.  Therefore a syntax contains two lists of rewrites: one for
+
−parsing and one for printing.
+
−
+
−The {\tt translations} section\index{translations section@{\tt translations}
+
−section} specifies macros.  The syntax for a macro is
+
−\[ (root)\; string \quad
+
−   \left\{\begin{array}[c]{c} \mtt{=>} \\ \mtt{<=} \\ \mtt{==} \end{array}
+
−   \right\} \quad
+
−   (root)\; string 
+
−\]
+
−%
+
−This specifies a parse rule ({\tt =>}), a print rule ({\tt <=}), or both
+
−({\tt ==}).  The two strings specify the left and right-hand sides of the
+
−macro rule.  The $(root)$ specification is optional; it specifies the
+
−nonterminal for parsing the $string$ and if omitted defaults to {\tt
+
−  logic}.  \AST{} rewrite rules $(l, r)$ must obey certain conditions:
+
−\begin{itemize}
+
−\item Rules must be left linear: $l$ must not contain repeated variables.
+
−
+
−\item Rules must have constant heads, namely $l = \mtt"c\mtt"$ or $l =
+
−  (\mtt"c\mtt" ~ x@1 \ldots x@n)$.
+
−
+
−\item Every variable in~$r$ must also occur in~$l$.
+
−\end{itemize}
+
−
+
−Macro rules may refer to any syntax from the parent theories.  They may
+
−also refer to anything defined before the the {\tt .thy} file's {\tt
+
−  translations} section --- including any mixfix declarations.
+
−
+
−Upon declaration, both sides of the macro rule undergo parsing and parse
+
−\AST{} translations (see \S\ref{sec:asts}), but do not themselves undergo
+
−macro expansion.  The lexer runs in a different mode that additionally
+
−accepts identifiers of the form $\_~letter~quasiletter^*$ (like {\tt _idt},
+
−{\tt _K}).  Thus, a constant whose name starts with an underscore can
+
−appear in macro rules but not in ordinary terms.
+
−
+
−Some atoms of the macro rule's \AST{} are designated as constants for
+
−matching.  These are all names that have been declared as classes, types or
+
−constants.
+
−
+
−The result of this preprocessing is two lists of macro rules, each stored
+
−as a pair of \AST{}s.  They can be viewed using {\tt Syntax.print_syntax}
+
−(sections \ttindex{parse_rules} and \ttindex{print_rules}).  For
+
−theory~{\tt SET} of Fig.~\ref{fig:set_trans} these are
+
−\begin{ttbox}
+
−parse_rules:
+
−  ("{\at}Collect" x A P)  ->  ("Collect" A ("_abs" x P))
+
−  ("{\at}Replace" y x A Q)  ->  ("Replace" A ("_abs" x ("_abs" y Q)))
+
−  ("{\at}Ball" x A P)  ->  ("Ball" A ("_abs" x P))
+
−print_rules:
+
−  ("Collect" A ("_abs" x P))  ->  ("{\at}Collect" x A P)
+
−  ("Replace" A ("_abs" x ("_abs" y Q)))  ->  ("{\at}Replace" y x A Q)
+
−  ("Ball" A ("_abs" x P))  ->  ("{\at}Ball" x A P)
+
−\end{ttbox}
+
−
+
−\begin{warn}
+
−  Avoid choosing variable names that have previously been used as
+
−  constants, types or type classes; the {\tt consts} section in the output
+
−  of {\tt Syntax.print_syntax} lists all such names.  If a macro rule works
+
−  incorrectly, inspect its internal form as shown above, recalling that
+
−  constants appear as quoted strings and variables without quotes.
+
−\end{warn}
+
−
+
−\begin{warn}
+
−If \ttindex{eta_contract} is set to {\tt true}, terms will be
+
−$\eta$-contracted {\em before\/} the \AST{} rewriter sees them.  Thus some
+
−abstraction nodes needed for print rules to match may vanish.  For example,
+
−\verb|Ball(A, %x. P(x))| contracts {\tt Ball(A, P)}; the print rule does
+
−not apply and the output will be {\tt Ball(A, P)}.  This problem would not
+
−occur if \ML{} translation functions were used instead of macros (as is
+
−done for binder declarations).
+
−\end{warn}
+
−
+
−
+
−\begin{warn}
+
−Another trap concerns type constraints.  If \ttindex{show_types} is set to
+
−{\tt true}, bound variables will be decorated by their meta types at the
+
−binding place (but not at occurrences in the body).  Matching with
+
−\verb|Collect(A, %x. P)| binds {\tt x} to something like {\tt ("_constrain" y
+
−"i")} rather than only {\tt y}.  \AST{} rewriting will cause the constraint to
+
−appear in the external form, say \verb|{y::i:A::i. P::o}|.  
+
−
+
−To allow such constraints to be re-read, your syntax should specify bound
+
−variables using the nonterminal~\ttindex{idt}.  This is the case in our
+
−example.  Choosing {\tt id} instead of {\tt idt} is a common error,
+
−especially since it appears in former versions of most of Isabelle's
+
−object-logics.
+
−\end{warn}
+
−
+
−
+
−
+
−\subsection{Applying rules}
+
−As a term is being parsed or printed, an \AST{} is generated as an
+
−intermediate form (recall Fig.\ts\ref{fig:parse_print}).  The \AST{} is
+
−normalized by applying macro rules in the manner of a traditional term
+
−rewriting system.  We first examine how a single rule is applied.
+
−
+
−Let $t$ be the abstract syntax tree to be normalized and $(l, r)$ some
+
−translation rule.  A subtree~$u$ of $t$ is a {\bf redex} if it is an
+
−instance of~$l$; in this case $l$ is said to {\bf match}~$u$.  A redex
+
−matched by $l$ may be replaced by the corresponding instance of~$r$, thus
+
−{\bf rewriting} the \AST~$t$.  Matching requires some notion of {\bf
+
−  place-holders} that may occur in rule patterns but not in ordinary
+
−\AST{}s; {\tt Variable} atoms serve this purpose.
+
−
+
−The matching of the object~$u$ by the pattern~$l$ is performed as follows:
+
−\begin{itemize}
+
−  \item Every constant matches itself.
+
−
+
−  \item $\Variable x$ in the object matches $\Constant x$ in the pattern.
+
−    This point is discussed further below.
+
−
+
−  \item Every \AST{} in the object matches $\Variable x$ in the pattern,
+
−    binding~$x$ to~$u$.
+
−
+
−  \item One application matches another if they have the same number of
+
−    subtrees and corresponding subtrees match.
+
−
+
−  \item In every other case, matching fails.  In particular, {\tt
+
−      Constant}~$x$ can only match itself.
+
−\end{itemize}
+
−A successful match yields a substitution that is applied to~$r$, generating
+
−the instance that replaces~$u$.
+
−
+
−The second case above may look odd.  This is where {\tt Variable}s of
+
−non-rule \AST{}s behave like {\tt Constant}s.  Recall that \AST{}s are not
+
−far removed from parse trees; at this level it is not yet known which
+
−identifiers will become constants, bounds, frees, types or classes.  As
+
−\S\ref{sec:asts} describes, former parse tree heads appear in \AST{}s as
+
−{\tt Constant}s, while $id$s, $var$s, $tid$s and $tvar$s become {\tt
+
−  Variable}s.  On the other hand, when \AST{}s generated from terms for
+
−printing, all constants and type constructors become {\tt Constant}s; see
+
−\S\ref{sec:asts}.  Thus \AST{}s may contain a messy mixture of {\tt
+
−  Variable}s and {\tt Constant}s.  This is insignificant at macro level
+
−because matching treats them alike.
+
−
+
−Because of this behaviour, different kinds of atoms with the same name are
+
−indistinguishable, which may make some rules prone to misbehaviour.  Example:
+
−\begin{ttbox}
+
−types
+
−  Nil
+
−consts
+
−  Nil     :: "'a list"
+
−  "[]"    :: "'a list"    ("[]")
+
−translations
+
−  "[]"    == "Nil"
+
−\end{ttbox}
+
−The term {\tt Nil} will be printed as {\tt []}, just as expected.  What
+
−happens with \verb|%Nil.t| or {\tt x::Nil} is left as an exercise.
+
−
+
−Normalizing an \AST{} involves repeatedly applying macro rules until none
+
−is applicable.  Macro rules are chosen in the order that they appear in the
+
−{\tt translations} section.  You can watch the normalization of \AST{}s
+
−during parsing and printing by setting \ttindex{Syntax.trace_norm_ast} to
+
−{\tt true}.\index{tracing!of macros} Alternatively, use
+
−\ttindex{Syntax.test_read}.  The information displayed when tracing
+
−includes the \AST{} before normalization ({\tt pre}), redexes with results
+
−({\tt rewrote}), the normal form finally reached ({\tt post}) and some
+
−statistics ({\tt normalize}).  If tracing is off,
+
−\ttindex{Syntax.stat_norm_ast} can be set to {\tt true} in order to enable
+
−printing of the normal form and statistics only.
+
−
+
−
+
−\subsection{Example: the syntax of finite sets}
+
−This example demonstrates the use of recursive macros to implement a
+
−convenient notation for finite sets.
+
−\begin{ttbox}
+
−FINSET = SET +
+
−types
+
−  is
+
−consts
+
−  ""            :: "i => is"                ("_")
+
−  "{\at}Enum"       :: "[i, is] => is"          ("_,/ _")
+
−  empty         :: "i"                      ("{\ttlbrace}{\ttrbrace}")
+
−  insert        :: "[i, i] => i"
+
−  "{\at}Finset"     :: "is => i"                ("{\ttlbrace}(_){\ttrbrace}")
+
−translations
+
−  "{\ttlbrace}x, xs{\ttrbrace}"     == "insert(x, {\ttlbrace}xs{\ttrbrace})"
+
−  "{\ttlbrace}x{\ttrbrace}"         == "insert(x, {\ttlbrace}{\ttrbrace})"
+
−end
+
−\end{ttbox}
+
−Finite sets are internally built up by {\tt empty} and {\tt insert}.  The
+
−declarations above specify \verb|{x, y, z}| as the external representation
+
−of
+
−\begin{ttbox}
+
−insert(x, insert(y, insert(z, empty)))
+
−\end{ttbox}
+
−
+
−The nonterminal symbol~{\tt is} stands for one or more objects of type~{\tt
+
−  i} separated by commas.  The mixfix declaration \hbox{\verb|"_,/ _"|}
+
−allows a line break after the comma for pretty printing; if no line break
+
−is required then a space is printed instead.
+
−
+
−The nonterminal is declared as the type~{\tt is}, but with no {\tt arities}
+
−declaration.  Hence {\tt is} is not a logical type and no default
+
−productions are added.  If we had needed enumerations of the nonterminal
+
−{\tt logic}, which would include all the logical types, we could have used
+
−the predefined nonterminal symbol \ttindex{args} and skipped this part
+
−altogether.  The nonterminal~{\tt is} can later be reused for other
+
−enumerations of type~{\tt i} like lists or tuples.
+
−
+
−Next follows {\tt empty}, which is already equipped with its syntax
+
−\verb|{}|, and {\tt insert} without concrete syntax.  The syntactic
+
−constant {\tt\at Finset} provides concrete syntax for enumerations of~{\tt
+
−  i} enclosed in curly braces.  Remember that a pair of parentheses, as in
+
−\verb|"{(_)}"|, specifies a block of indentation for pretty printing.
+
−
+
−The translations may look strange at first.  Macro rules are best
+
−understood in their internal forms:
+
−\begin{ttbox}
+
−parse_rules:
+
−  ("{\at}Finset" ("{\at}Enum" x xs))  ->  ("insert" x ("{\at}Finset" xs))
+
−  ("{\at}Finset" x)  ->  ("insert" x "empty")
+
−print_rules:
+
−  ("insert" x ("{\at}Finset" xs))  ->  ("{\at}Finset" ("{\at}Enum" x xs))
+
−  ("insert" x "empty")  ->  ("{\at}Finset" x)
+
−\end{ttbox}
+
−This shows that \verb|{x, xs}| indeed matches any set enumeration of at least
+
−two elements, binding the first to {\tt x} and the rest to {\tt xs}.
+
−Likewise, \verb|{xs}| and \verb|{x}| represent any set enumeration.  
+
−The parse rules only work in the order given.
+
−
+
−\begin{warn}
+
−  The \AST{} rewriter cannot discern constants from variables and looks
+
−  only for names of atoms.  Thus the names of {\tt Constant}s occurring in
+
−  the (internal) left-hand side of translation rules should be regarded as
+
−  reserved keywords.  Choose non-identifiers like {\tt\at Finset} or
+
−  sufficiently long and strange names.  If a bound variable's name gets
+
−  rewritten, the result will be incorrect; for example, the term
+
−\begin{ttbox}
+
−\%empty insert. insert(x, empty)
+
−\end{ttbox}
+
−  gets printed as \verb|%empty insert. {x}|.
+
−\end{warn}
+
−
+
−
+
−\subsection{Example: a parse macro for dependent types}\label{prod_trans}
+
−As stated earlier, a macro rule may not introduce new {\tt Variable}s on
+
−the right-hand side.  Something like \verb|"K(B)" => "%x. B"| is illegal;
+
−it allowed, it could cause variable capture.  In such cases you usually
+
−must fall back on translation functions.  But a trick can make things
+
−readable in some cases: {\em calling translation functions by parse
+
−  macros}:
+
−\begin{ttbox}
+
−PROD = FINSET +
+
−consts
+
−  Pi            :: "[i, i => i] => i"
+
−  "{\at}PROD"       :: "[idt, i, i] => i"     ("(3PROD _:_./ _)" 10)
+
−  "{\at}->"         :: "[i, i] => i"          ("(_ ->/ _)" [51, 50] 50)
+
−\ttbreak
+
−translations
+
−  "PROD x:A. B" => "Pi(A, \%x. B)"
+
−  "A -> B"      => "Pi(A, _K(B))"
+
−end
+
−ML
+
−  val print_translation = [("Pi", dependent_tr' ("{\at}PROD", "{\at}->"))];
+
−\end{ttbox}
+
−
+
−Here {\tt Pi} is an internal constant for constructing general products.
+
−Two external forms exist: the general case {\tt PROD x:A.B} and the
+
−function space {\tt A -> B}, which abbreviates \verb|Pi(A, %x.B)| when {\tt B}
+
−does not depend on~{\tt x}.
+
−
+
−The second parse macro introduces {\tt _K(B)}, which later becomes \verb|%x.B|
+
−due to a parse translation associated with \ttindex{_K}.  The order of the
+
−parse rules is critical.  Unfortunately there is no such trick for
+
−printing, so we have to add a {\tt ML} section for the print translation
+
−\ttindex{dependent_tr'}.
+
−
+
−Recall that identifiers with a leading {\tt _} are allowed in translation
+
−rules, but not in ordinary terms.  Thus we can create \AST{}s containing
+
−names that are not directly expressible.
+
−
+
−The parse translation for {\tt _K} is already installed in Pure, and {\tt
+
−dependent_tr'} is exported by the syntax module for public use.  See
+
−\S\ref{sec:tr_funs} below for more of the arcane lore of translation functions.
+
−\index{macros|)}\index{rewriting!syntactic|)}
+
−
+
−
+
−
+
−\section{*Translation functions} \label{sec:tr_funs}
+
−\index{translations|(} 
+
−%
+
−This section describes the translation function mechanism.  By writing
+
−\ML{} functions, you can do almost everything with terms or \AST{}s during
+
−parsing and printing.  The logic \LK\ is a good example of sophisticated
+
−transformations between internal and external representations of
+
−associative sequences; here, macros would be useless.
+
−
+
−A full understanding of translations requires some familiarity
+
−with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ},
+
−{\tt Syntax.ast} and the encodings of types and terms as such at the various
+
−stages of the parsing or printing process.  Most users should never need to
+
−use translation functions.
+
−
+
−\subsection{Declaring translation functions}
+
−There are four kinds of translation functions.  Each such function is
+
−associated with a name, which triggers calls to it.  Such names can be
+
−constants (logical or syntactic) or type constructors.
+
−
+
−{\tt Syntax.print_syntax} displays the sets of names associated with the
+
−translation functions of a {\tt Syntax.syntax} under
+
−\ttindex{parse_ast_translation}, \ttindex{parse_translation},
+
−\ttindex{print_translation} and \ttindex{print_ast_translation}.  You can
+
−add new ones via the {\tt ML} section\index{ML section@{\tt ML} section} of
+
−a {\tt .thy} file.  There may never be more than one function of the same
+
−kind per name.  Conceptually, the {\tt ML} section should appear between
+
−{\tt consts} and {\tt translations}; newly installed translation functions
+
−are already effective when macros and logical rules are parsed.
+
−
+
−The {\tt ML} section is copied verbatim into the \ML\ file generated from a
+
−{\tt .thy} file.  Definitions made here are accessible as components of an
+
−\ML\ structure; to make some definitions private, use an \ML{} {\tt local}
+
−declaration.  The {\tt ML} section may install translation functions by
+
−declaring any of the following identifiers:
+
−\begin{ttbox}
+
−val parse_ast_translation : (string * (ast list -> ast)) list
+
−val print_ast_translation : (string * (ast list -> ast)) list
+
−val parse_translation     : (string * (term list -> term)) list
+
−val print_translation     : (string * (term list -> term)) list
+
−\end{ttbox}
+
−
+
−\subsection{The translation strategy}
+
−All four kinds of translation functions are treated similarly.  They are
+
−called during the transformations between parse trees, \AST{}s and terms
+
−(recall Fig.\ts\ref{fig:parse_print}).  Whenever a combination of the form
+
−$(\mtt"c\mtt"~x@1 \ldots x@n)$ is encountered, and a translation function
+
−$f$ of appropriate kind exists for $c$, the result is computed by the \ML{}
+
−function call $f \mtt[ x@1, \ldots, x@n \mtt]$.
+
−
+
−For \AST{} translations, the arguments $x@1, \ldots, x@n$ are \AST{}s.  A
+
−combination has the form $\Constant c$ or $\Appl{\Constant c, x@1, \ldots,
+
−  x@n}$.  For term translations, the arguments are terms and a combination
+
−has the form $\ttfct{Const} (c, \tau)$ or $\ttfct{Const} (c, \tau) \ttapp
+
−x@1 \ttapp \ldots \ttapp x@n$.  Terms allow more sophisticated
+
−transformations than \AST{}s do, typically involving abstractions and bound
+
−variables.
+
−
+
−Regardless of whether they act on terms or \AST{}s,
+
−parse translations differ from print translations fundamentally:
+
−\begin{description}
+
−\item[Parse translations] are applied bottom-up.  The arguments are already
+
−  in translated form.  The translations must not fail; exceptions trigger
+
−  an error message.
+
−
+
−\item[Print translations] are applied top-down.  They are supplied with
+
−  arguments that are partly still in internal form.  The result again
+
−  undergoes translation; therefore a print translation should not introduce
+
−  as head the very constant that invoked it.  The function may raise
+
−  exception \ttindex{Match} to indicate failure; in this event it has no
+
−  effect.
+
−\end{description}
+
−
+
−Only constant atoms --- constructor \ttindex{Constant} for \AST{}s and
+
−\ttindex{Const} for terms --- can invoke translation functions.  This
+
−causes another difference between parsing and printing.
+
−
+
−Parsing starts with a string and the constants are not yet identified.
+
−Only parse tree heads create {\tt Constant}s in the resulting \AST; recall
+
−$ast_of_pt$ in \S\ref{sec:asts}.  Macros and parse \AST{} translations may
+
−introduce further {\tt Constant}s.  When the final \AST{} is converted to a
+
−term, all {\tt Constant}s become {\tt Const}s; recall $term_of_ast$ in
+
−\S\ref{sec:asts}.
+
−
+
−Printing starts with a well-typed term and all the constants are known.  So
+
−all logical constants and type constructors may invoke print translations.
+
−These, and macros, may introduce further constants.
+
−
+
−
+
−\subsection{Example: a print translation for dependent types}
+
−\indexbold{*_K}\indexbold{*dependent_tr'}
+
−Let us continue the dependent type example (page~\pageref{prod_trans}) by
+
−examining the parse translation for {\tt _K} and the print translation
+
−{\tt dependent_tr'}, which are both built-in.  By convention, parse
+
−translations have names ending with {\tt _tr} and print translations have
+
−names ending with {\tt _tr'}.  Search for such names in the Isabelle
+
−sources to locate more examples.
+
−
+
−Here is the parse translation for {\tt _K}:
+
−\begin{ttbox}
+
−fun k_tr [t] = Abs ("x", dummyT, incr_boundvars 1 t)
+
−  | k_tr ts = raise TERM("k_tr",ts);
+
−\end{ttbox}
+
−If {\tt k_tr} is called with exactly one argument~$t$, it creates a new
+
−{\tt Abs} node with a body derived from $t$.  Since terms given to parse
+
−translations are not yet typed, the type of the bound variable in the new
+
−{\tt Abs} is simply {\tt dummyT}.  The function increments all {\tt Bound}
+
−nodes referring to outer abstractions by calling \ttindex{incr_boundvars},
+
−a basic term manipulation function defined in {\tt Pure/term.ML}.
+
−
+
−Here is the print translation for dependent types:
+
−\begin{ttbox}
+
−fun dependent_tr' (q,r) (A :: Abs (x, T, B) :: ts) =
+
−      if 0 mem (loose_bnos B) then
+
−        let val (x', B') = variant_abs (x, dummyT, B);
+
−        in list_comb (Const (q, dummyT) $ Free (x', T) $ A $ B', ts)
+
−        end
+
−      else list_comb (Const (r, dummyT) $ A $ B, ts)
+
−  | dependent_tr' _ _ = raise Match;
+
−\end{ttbox}
+
−The argument {\tt (q,r)} is supplied to {\tt dependent_tr'} by a curried
+
−function application during its installation.  We could set up print
+
−translations for both {\tt Pi} and {\tt Sigma} by including
+
−\begin{ttbox}
+
−val print_translation =
+
−  [("Pi",    dependent_tr' ("{\at}PROD", "{\at}->")),
+
−   ("Sigma", dependent_tr' ("{\at}SUM", "{\at}*"))];
+
−\end{ttbox}
+
−within the {\tt ML} section.  The first of these transforms ${\tt Pi}(A,
+
−\mtt{Abs}(x, T, B))$ into $\hbox{\tt{\at}PROD}(x', A, B')$ or
+
−$\hbox{\tt{\at}->}r(A, B)$, choosing the latter form if $B$ does not depend
+
−on~$x$.  It checks this using \ttindex{loose_bnos}, yet another function
+
−from {\tt Pure/term.ML}.  Note that $x'$ is a version of $x$ renamed away
+
−from all names in $B$, and $B'$ the body $B$ with {\tt Bound} nodes
+
−referring to our {\tt Abs} node replaced by $\ttfct{Free} (x',
+
−\mtt{dummyT})$.
+
−
+
−We must be careful with types here.  While types of {\tt Const}s are
+
−ignored, type constraints may be printed for some {\tt Free}s and
+
−{\tt Var}s if \ttindex{show_types} is set to {\tt true}.  Variables of type
+
−\ttindex{dummyT} are never printed with constraint, though.  The line
+
−\begin{ttbox}
+
−        let val (x', B') = variant_abs (x, dummyT, B);
+
−\end{ttbox}\index{*variant_abs}
+
−replaces bound variable occurrences in~$B$ by the free variable $x'$ with
+
−type {\tt dummyT}.  Only the binding occurrence of~$x'$ is given the
+
−correct type~{\tt T}, so this is the only place where a type
+
−constraint might appear. 
+
−\index{translations|)}
+
−
+
−
+
−