doc-src/Logics/defining.tex

various minor changes;

%% $Id$

\newcommand{\rmindex}[1]{{#1}\index{#1}\@}
\newcommand{\mtt}[1]{\mbox{\tt #1}}
\newcommand{\ttfct}[1]{\mathop{\mtt{#1}}\nolimits}
\newcommand{\ttrel}[1]{\mathrel{\mtt{#1}}}
\newcommand{\Constant}{\ttfct{Constant}}
\newcommand{\Variable}{\ttfct{Variable}}
\newcommand{\Appl}[1]{\ttfct{Appl}\mathopen{\mtt[}#1\mathclose{\mtt]}}



\chapter{Defining Logics} \label{Defining-Logics}

This chapter is intended for Isabelle experts. It explains how to define new
logical systems, Isabelle's {\em raison d'\^etre}. Isabelle logics are
hierarchies of theories. A number of simple examples are contained in {\em
Introduction to Isabelle}; the full syntax of theory definition files ({\tt
.thy} files) is shown in {\em The Isabelle Reference Manual}. This chapter's
chief purpose is a thorough description of all syntax related matters
concerning theories. The most important sections are \S\ref{sec:mixfix} about
mixfix declarations and \S\ref{sec:macros} describing the macro system. The
concluding examples of \S\ref{sec:min_logics} are more concerned with the
logical aspects of the definition of theories. Sections marked with * can be
skipped on the first reading.


%% FIXME move to Refman
% \section{Classes and types *}
% \index{*arities!context conditions}
%
% Type declarations are subject to the following two well-formedness
% conditions:
% \begin{itemize}
% \item There are no two declarations $ty :: (\vec{r})c$ and $ty :: (\vec{s})c$
%   with $\vec{r} \neq \vec{s}$.  For example
% \begin{ttbox}
% types ty 1
% arities ty :: ({\ttlbrace}logic{\ttrbrace}) logic
%         ty :: ({\ttlbrace}{\ttrbrace})logic
% \end{ttbox}
% leads to an error message and fails.
% \item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::
%   (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold
%   for $i=1,\dots,n$.  The relationship $\preceq$, defined as
% \[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
% expresses that the set of types represented by $s'$ is a subset of the set of
% types represented by $s$.  For example
% \begin{ttbox}
% classes term < logic
% types ty 1
% arities ty :: ({\ttlbrace}logic{\ttrbrace})logic
%         ty :: ({\ttlbrace}{\ttrbrace})term
% \end{ttbox}
% leads to an error message and fails.
% \end{itemize}
% These conditions guarantee principal types~\cite{nipkow-prehofer}.



\section{Precedence grammars} \label{sec:precedence_grammars}

The precise syntax of a logic is best defined by a \rmindex{context-free
grammar}. In order to simplify the description of mathematical languages, we
introduce an extended format which permits {\bf
precedences}\indexbold{precedence}. This scheme generalizes precedence
declarations in \ML\ and {\sc prolog}. In this extended grammar format,
nonterminals are decorated by integers, their precedence. In the sequel,
precedences are shown as subscripts. A nonterminal $A@p$ on the right-hand
side of a production may only be replaced using a production $A@q = \gamma$
where $p \le q$.

Formally, a set of context free productions $G$ induces a derivation
relation $\rew@G$ on strings as follows:
\[ \alpha A@p \beta ~\rew@G~ \alpha\gamma\beta ~~~iff~~~
   \exists (A@q=\gamma) \in G.~q \ge p
\]
Any extended grammar of this kind can be translated into a normal context
free grammar. However, this translation may require the introduction of a
large number of new nonterminals and productions.

\begin{example} \label{ex:precedence}
The following simple grammar for arithmetic expressions demonstrates how
binding power and associativity of operators can be enforced by precedences.
\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 precedences determines that {\tt -} binds tighter than {\tt *}
which binds tighter than {\tt +}, and that {\tt +} associates to the left and
{\tt *} to the right.
\end{example}

To minimize the number of subscripts, we adopt the following conventions:
\begin{itemize}
\item All precedences $p$ must be in the range $0 \leq p \leq max_pri$ for
  some fixed $max_pri$.
\item Precedence $0$ on the right-hand side and precedence $max_pri$ on the
  left-hand side may be omitted.
\end{itemize}
In addition, we write the production $A@p = \alpha$ as $A = \alpha~(p)$,
i.e.\ the precedence of the left-hand side actually appears in the uttermost
right. Finally, alternatives may be separated by $|$, and repetition
indicated by \dots.

Using these conventions and assuming $max_pri=9$, the grammar in
Example~\ref{ex:precedence} becomes
\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}



\section{Basic syntax} \label{sec:basic_syntax}

The basis of all extensions by object-logics is the \rmindex{Pure theory},
bound to the \ML-identifier \ttindex{Pure.thy}. It contains, among many other
things, the \rmindex{Pure syntax}. An informal account of this basic syntax
(meta-logic, types etc.) may be found in {\em Introduction to Isabelle}. A
more precise description using a precedence grammar is shown in
Figure~\ref{fig:pure_gram}.

\begin{figure}[htb]
\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$ &=& $tfree$ ~~$|$~~ $tvar$ ~~$|$~~ $tfree$ {\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}

The following main categories are defined:
\begin{description}
  \item[$prop$] Terms of type $prop$, i.e.\ formulae of the meta-logic.

  \item[$aprop$] Atomic propositions.

  \item[$logic$] Terms of types in class $logic$. Initially, $logic$ contains
    merely $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$] Meta-types.

  \item[$idts$] A list of identifiers, possibly constrained by types. Note
    that \verb|x :: nat y| is parsed as \verb|x :: (nat y)|, i.e.\ {\tt y}
    would be treated like a type constructor applied to {\tt nat}.
\end{description}


\subsection{Logical types and default syntax}

Isabelle is concerned with mathematical languages which have a certain
minimal vocabulary: identifiers, variables, parentheses, and the lambda
calculus. Logical types, i.e.\ those of class $logic$, are automatically
equipped with this basic syntax. More precisely, for any type constructor
$ty$ with arity $(\vec{s})c$, where $c$ is a subclass of $logic$, the
following 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 rather operates on
token lists provided by Isabelle's \rmindex{lexical analyzer} (the
\bfindex{lexer}). There are two different kinds of tokens: {\bf
literals}\indexbold{literal token}\indexbold{token!literal} and {\bf valued
tokens}\indexbold{valued token}\indexbold{token!valued}.

Literals can be regarded as reserved words\index{reserved word} of the syntax
and the user can add new ones, when extending theories. In
Figure~\ref{fig:pure_gram} they appear in typewriter type, e.g.\ {\tt PROP},
{\tt ==}, {\tt =?=}, {\tt ;}.

Valued tokens on the other hand have a fixed predefined syntax. The lexer
distinguishes four kinds of them: identifiers\index{identifier},
unknowns\index{unknown}\index{scheme variable|see{unknown}}, type
variables\index{type variable}, type unknowns\index{type unknown}\index{type
scheme variable|see{type unknown}}; they are denoted by $id$\index{id@$id$},
$var$\index{var@$var$}, $tfree$\index{tfree@$tfree$},
$tvar$\index{tvar@$tvar$}, respectively. Typical examples are {\tt x}, {\tt
?x7}, {\tt 'a}, {\tt ?'a3}, the exact syntax is:

\begin{tabular}{rcl}
$id$        & =   & $letter~quasiletter^*$ \\
$var$       & =   & ${\tt ?}id ~~|~~ {\tt ?}id{\tt .}nat$ \\
$tfree$     & =   & ${\tt '}id$ \\
$tvar$      & =   & ${\tt ?}tfree ~~|~~ {\tt ?}tfree{\tt .}nat$ \\[1ex]

$letter$    & =   & one of {\tt a}\dots {\tt z} {\tt A}\dots {\tt Z} \\
$digit$     & =   & one of {\tt 0}\dots {\tt 9} \\
$quasiletter$ & =  & $letter ~~|~~ digit ~~|~~ {\tt _} ~~|~~ {\tt '}$ \\
$nat$       & =   & $digit^+$
\end{tabular}

A string of $var$ or $tvar$ describes an \rmindex{unknown} which is
internally a pair of base name and index (\ML\ type \ttindex{indexname}).
These components are either explicitly separated by a dot as in {\tt ?x.1} or
{\tt ?x7.3} or directly run together as in {\tt ?x1}. The latter form is
possible, if the base name does not end with digits. And if the index is 0,
it may be dropped altogether: {\tt ?x} abbreviates {\tt ?x0} or {\tt ?x.0}.

Note that $id$, $var$, $tfree$, $tvar$ are mutually disjoint, but it is
perfectly legal that they overlap with the set of literal tokens (e.g.\ {\tt
PROP}, {\tt ALL}, {\tt EX}).

The lexical analyzer translates input strings to token lists by repeatedly
taking the maximal prefix of the input string that forms a valid token. A
maximal prefix that is both a literal and a valued token is treated as a
literal. Spaces, tabs and newlines are separators; they never occur within
tokens.

Note that literals need not necessarily be surrounded by white space to be
recognized as separate. For example, if {\tt -} is a literal but {\tt --} is
not, then the string {\tt --} is treated as two consecutive occurrences of
{\tt -}. This is in contrast to \ML\ which would treat {\tt --} always 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 literal, the input {\tt --} is treated as
a single token.


\subsection{Inspecting syntax *}

You may get the \ML\ representation of the syntax of any Isabelle theory by
applying \index{*syn_of}
\begin{ttbox}
  syn_of: theory -> Syntax.syntax
\end{ttbox}
\ttindex{Syntax.syntax} is an abstract type. Values of this type can be
displayed by the following functions: \index{*Syntax.print_syntax}
\index{*Syntax.print_gram} \index{*Syntax.print_trans}
\begin{ttbox}
  Syntax.print_syntax: Syntax.syntax -> unit
  Syntax.print_gram: Syntax.syntax -> unit
  Syntax.print_trans: Syntax.syntax -> unit
\end{ttbox}
{\tt Syntax.print_syntax} shows virtually all information contained in a
syntax, therefore being quite verbose. Its output is divided into labeled
sections. The syntax proper is represented by {\tt lexicon}, {\tt roots} and
{\tt prods}. The rest refers to the manifold facilities to apply syntactic
translations (macro expansion etc.).

To simplify coping with the verbosity of {\tt Syntax.print_syntax}, there are
\ttindex{Syntax.print_gram} to print the syntax proper only and
\ttindex{Syntax.print_trans} to print the translation related information
only.

Let's have a closer look at part of Pure's syntax:
\begin{ttbox}
Syntax.print_syntax (syn_of Pure.thy);
{\out lexicon: "!!" "%" "(" ")" "," "." "::" ";" "==" "==>" \dots}
{\out roots: logic type fun prop}
{\out prods:}
{\out   type = tfree  (1000)}
{\out   type = tvar  (1000)}
{\out   type = id  (1000)}
{\out   type = tfree "::" sort[0]  => "_ofsort" (1000)}
{\out   type = tvar "::" sort[0]  => "_ofsort" (1000)}
{\out   \vdots}
{\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}

\begin{description}
  \item[\ttindex{lexicon}]
    The set of literal tokens (i.e.\ reserved words, delimiters) used for
    lexical analysis.

  \item[\ttindex{roots}]
    The legal syntactic categories to start parsing with. You name the
    desired root directly as a string when calling lower level functions or
    specifying macros. Higher level functions usually expect a type and
    derive the actual root as follows:\index{root_of_type@$root_of_type$}
    \begin{itemize}
      \item $root_of_type(\tau@1 \To \tau@2) = \mtt{fun}$.

      \item $root_of_type(\tau@1 \mathrel{ty} \tau@2) = ty$.

      \item $root_of_type((\tau@1, \dots, \tau@n)ty) = ty$.

      \item $root_of_type(\alpha) = \mtt{logic}$.
    \end{itemize}
    Thereby $\tau@1, \dots, \tau@n$ are types, $ty$ an infix or ordinary type
    constructor and $\alpha$ a type variable or unknown. Note that only the
    outermost type constructor is taken into account.

  \item[\ttindex{prods}]
    The list of productions describing the precedence grammar. Nonterminals
    $A@n$ are rendered in {\sc ascii} as {\tt $A$[$n$]}, literal tokens are
    quoted. Some productions have strings attached after an {\tt =>}. These
    strings later become the heads of parse trees, but they also play a vital
    role when terms are printed (see \S\ref{sec:asts}).

    Productions which do not have string attached and thus do not create a
    new parse tree node are called {\bf copy productions}\indexbold{copy
    production}. They must have exactly one
    argument\index{argument!production} (i.e.\ nonterminal or valued token)
    on the right-hand side. The parse tree generated when parsing that
    argument is simply passed up as the result of parsing the whole copy
    production.

    A special kind of copy production is one where the argument is a
    nonterminal and no additional syntactic sugar (literals) exists. It is
    called a \bfindex{chain production}. Chain productions should be seen as
    an abbreviation mechanism: conceptually, they are removed from the
    grammar by adding appropriate new rules. Precedence information attached
    to chain productions is ignored, only the dummy value $-1$ is displayed.

  \item[\ttindex{consts}, \ttindex{parse_rules}, \ttindex{print_rules}]
    This is macro related information (see \S\ref{sec:macros}).

  \item[\tt *_translation]
    \index{*parse_ast_translation} \index{*parse_translation}
    \index{*print_translation} \index{*print_ast_translation}
    The sets of constants that invoke translation functions. These are more
    arcane matters (see \S\ref{sec:asts} and \S\ref{sec:tr_funs}).
\end{description}

Of course you may inspect the syntax of any theory using the above calling
sequence. Beware that, as more and more material accumulates, the output
becomes even more verbose. When extending syntaxes, new {\tt roots}, {\tt
prods}, {\tt parse_rules} and {\tt print_rules} are appended to the end. The
other lists are displayed sorted.



\section{Abstract syntax trees} \label{sec:asts}

Figure~\ref{fig:parse_print} shows a simplified model of the parsing and
printing process.

\begin{figure}[htb]
\begin{center}
\begin{tabular}{cl}
string          & \\
$\downarrow$    & parser \\
parse tree      & \\
$\downarrow$    & \rmindex{parse ast translation} \\
ast             & \\
$\downarrow$    & ast rewriting (macros) \\
ast             & \\
$\downarrow$    & \rmindex{parse translation}, type-inference \\
--- well-typed term --- & \\
$\downarrow$    & \rmindex{print translation} \\
ast             & \\
$\downarrow$    & ast rewriting (macros) \\
ast             & \\
$\downarrow$    & \rmindex{print ast translation}, printer \\
string          &
\end{tabular}
\end{center}
\caption{Parsing and Printing}
\label{fig:parse_print}
\end{figure}

The parser takes an input string (more precisely the token list produced by
the lexer) and produces a \rmin«ôx{parse tree}, which is directly derived
from the productions involved. By applying some internal transformations the
parse tree becomes an \bfindex{abstract syntax tree} (\bfindex{ast}). Macro
expansion, further translations and finally type inference yields a
well-typed term\index{term!well-typed}.

The printing process is the reverse, except for some subtleties to be
discussed later.

Asts are an intermediate form between the very 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\/} subasts. Internally, they have type \ttindex{Syntax.ast}
which is defined as: \index{*Constant} \index{*Variable} \index{*Appl}
\begin{ttbox}
datatype ast =
  Constant of string |
  Variable of string |
  Appl of ast list
\end{ttbox}

Notation: We write constant atoms as quoted strings, variable atoms as
non-quoted strings and applications as list of subasts separated by space and
enclosed in parentheses. For example:
\begin{ttbox}
  Appl [Constant "_constrain",
    Appl [Constant "_abs", Variable "x", Variable "t"],
    Appl [Constant "fun", Variable "'a", Variable "'b"]]
  {\rm is written as} ("_constrain" ("_abs" x t) ("fun" 'a 'b))
\end{ttbox}

Note that {\tt ()} and {\tt (f)} are both illegal.

The resemblance of Lisp's S-expressions is intentional, but notice the two
kinds of atomic symbols: $\Constant x$ and $\Variable x$. This distinction
has some more obscure reasons and you can ignore it about half of the time.
You should 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 some sort of
application of $f$ to the arguments $x@1, \ldots, x@n$. But the actual kind
of application (say a type constructor $f$ applied to types $x@1, \ldots,
x@n$) is determined later by context, too.

Forms like {\tt (("_abs" x $t$) $u$)} are perfectly legal, but asts are not
higher-order: the {\tt "_abs"} does not yet bind the {\tt x} in any way,
though 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 {\tt Bound}s. Even
if non-constant heads of applications may seem unusual, asts should be
regarded as first-order. Purists may think of ${\tt (} f~x@1~\ldots~x@n{\tt
)}$ as a first-order application of some invisible $(n+1)$-ary constant.


\subsection{Parse trees to asts}

Asts are generated from parse trees by applying some translation functions,
which are internally called {\bf parse ast translations}\indexbold{parse ast
translation}.

We can think of the raw output of the parser as trees built up by nesting the
right-hand sides of those productions that were used to derive a word that
matches the input token list. Then parse trees are simply lists of tokens and
sub parse trees, the latter replacing the nonterminals of the productions.
Note that we refer here to the actual productions in their internal form as
displayed by {\tt Syntax.print_syntax}.

Ignoring parse ast translations, the mapping
$ast_of_pt$\index{ast_of_pt@$ast_of_pt$} from parse trees to asts is derived
from the productions involved as follows:
\begin{itemize}
  \item Valued tokens: $ast_of_pt(t) = \Variable s$, where $t$ is an $id$,
    $var$, $tfree$ or $tvar$ token, and $s$ its value.

  \item Copy productions: $ast_of_pt(\ldots P \ldots) = ast_of_pt(P)$.

  \item $0$-ary productions: $ast_of_pt(\ldots \mtt{=>} c) = \Constant c$.

  \item $n$-ary productions: $ast_of_pt(\ldots P@1 \ldots P@n \ldots \mtt{=>}
    c) = \Appl{\Constant c,$ $ast_of_pt(P@1),$ $\ldots,$ $ast_of_pt(P@n)}$,
    where $n \ge 1$.
\end{itemize}
Thereby $P, P@1, \ldots, P@n$ denote sub parse trees or valued tokens and
``\dots'' zero or more literal tokens. That means literal tokens are stripped
and do not appear in asts.

The following table presents some simple examples:

{\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}}

Some of these examples illustrate why further translations are desirable in
order to provide some nice standard form of asts before macro expansion takes
place. Hence the Pure syntax provides predefined parse ast
translations\index{parse ast translation!of Pure} for ordinary applications,
type applications, nested abstractions, meta implications and function types.
Their net effect on some representative input strings is shown in
Figure~\ref{fig:parse_ast_tr}.

\begin{figure}[htb]
\begin{center}
{\tt\begin{tabular}{ll}
\rm 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}

This translation process is guided by names of constant heads of asts. The
list of constants invoking parse ast translations is shown in the output of
{\tt Syntax.print_syntax} under {\tt parse_ast_translation}.


\subsection{Asts to terms *}

After the ast has been normalized by the macro expander (see
\S\ref{sec:macros}), it is transformed into a term with yet another set of
translation functions interspersed: {\bf parse translations}\indexbold{parse
translation}. The result is a non-typed term\index{term!non-typed} which may
contain type constraints, that is 2-place applications with head {\tt
"_constrain"}. The second argument of a constraint is a type encoded as term.
Real types will be introduced later during type inference, which is not
discussed here.

If we ignore the built-in parse translations of Pure first, then the mapping
$term_of_ast$\index{term_of_ast@$term_of_ast$} from asts to (non-typed) terms
is defined by:
\begin{itemize}
  \item $term_of_ast(\Constant x) = \ttfct{Const} (x, \mtt{dummyT})$.

  \item $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 $term_of_ast(\Variable x) = \ttfct{Free} (x, \mtt{dummyT})$.

  \item $term_of_ast(\Appl{f, x@1, \ldots, x@n}) = term_of_ast(f) ~{\tt\$}~
    term_of_ast(x@1)$ {\tt\$} \dots\ {\tt\$} $term_of_ast(x@n)$.
\end{itemize}
Note that {\tt Const}, {\tt Var}, {\tt Free} belong to the datatype {\tt
term} and \ttindex{dummyT} is bound to some dummy {\tt typ}, which is ignored
during type-inference.

So far the outcome is still a first-order term. {\tt Abs}s and {\tt Bound}s
are introduced by parse translations associated with {\tt "_abs"} and {\tt
"!!"} (and any other user defined binder).


\subsection{Printing of terms *}

When terms are prepared for printing, they are first transformed into asts
via $ast_of_term$\index{ast_of_term@$ast_of_term$} (ignoring {\bf print
translations}\indexbold{print translation}):
\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 $ast_of_term(\ttfct{Abs} (x, \tau, t)) = \ttfct{Appl}
    \mathopen{\mtt[} \Constant \mtt{"_abs"}, constrain(\Variable x', \tau),$
    $ast_of_term(t') \mathclose{\mtt]}$, where $x'$ is a version of $x$
    renamed away from all names occurring in $t$, and $t'$ the body $t$ with
    all {\tt Bound}s referring to this {\tt Abs} replaced by $\ttfct{Free}
    (x', \mtt{dummyT})$.

  \item $ast_of_term(\ttfct{Bound} i) = \Variable \mtt{"B.}i\mtt"$. Note that
    the occurrence of loose bound variables is abnormal and should never
    happen when printing well-typed terms.

  \item $ast_of_term(f \ttrel{\$} x@1 \ttrel{\$} \ldots \ttrel{\$} x@n) =
    \ttfct{Appl} \mathopen{\mtt[} ast_of_term(f), ast_of_term(x@1), \ldots,$
    $ast_of_term(x@n) \mathclose{\mtt]}$, where $f$ is not an application.

  \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 variables 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}

\medskip
After an ast has been normalized wrt.\ the print macros, it is transformed
into the final output string. The built-in {\bf print ast
translations}\indexbold{print ast translation} are essentially the reverse
ones of the parse ast translations of Figure~\ref{fig:parse_ast_tr}.

For the actual printing process, the names attached to grammar productions of
the form $\ldots A@{p@1}^1 \ldots A@{p@n}^n \ldots \mtt{=>} c$ play a vital
role. Whenever an ast with constant head $c$, i.e.\ $\mtt"c\mtt"$ or
$(\mtt"c\mtt"~ x@1 \ldots x@n)$, is encountered it is printed according to
the production for $c$. This means that first the arguments $x@1$ \dots $x@n$
are printed, then put in parentheses if necessary for reasons of precedence,
and finally joined to a single string, separated by the syntactic sugar of
the production (denoted by ``\dots'' above).

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$. A single
$\Variable x$ is simply printed as $x$.

Note that the system does {\em not\/} insert blanks automatically. They
should be part of the mixfix declaration the production has been derived
from, if they are required to separate tokens. Mixfix declarations may also
contain pretty printing annotations.



\section{Mixfix declarations} \label{sec:mixfix}

When defining theories, the user usually declares new constants as names
associated with a type followed by an optional \bfindex{mixfix annotation}.
If none of the constants are introduced with mixfix annotations, there is no
concrete syntax to speak of: terms can only be abstractions or applications
of the form $f(t@1, \dots, t@n)$. Since this notation quickly becomes
unreadable, Isabelle supports syntax definitions in the form of unrestricted
context-free \index{context-free grammar} \index{precedence grammar}
precedence grammars using mixfix annotations.

Mixfix annotations describe the {\em concrete\/} syntax, a standard
translation into the abstract syntax and a pretty printing scheme, all in
one. Isabelle syntax definitions are inspired by \OBJ's~\cite{OBJ} {\em
mixfix\/} syntax. Each mixfix annotation defines a precedence grammar
production and optionally associates a constant with it.

There is a general form of mixfix annotation and some shortcuts for common
cases like infix operators.

The general \bfindex{mixfix declaration} as it may occur within the {\tt
consts} section\index{consts section@{\tt consts} section} of a {\tt .thy}
file, specifies a constant declaration and a grammar production at the same
time. It has the form {\tt $c$ ::\ "$\tau$" ("$sy$" $ps$ $p$)} and is
interpreted as follows:
\begin{itemize}
  \item {\tt $c$ ::\ "$\tau$"} is the actual constant declaration without any
    syntactic significance.

  \item $sy$ is the right-hand side of the production, specified as a
    symbolic string. In general, $sy$ is of the form $\alpha@0 \_ \alpha@1
    \dots \alpha@{n-1} \_ \alpha@n$, where each occurrence of \ttindex{_}
    denotes an argument\index{argument!mixfix} position and the strings
    $\alpha@i$ do not contain (non-escaped) {\tt _}. The $\alpha@i$ may
    consist of delimiters\index{delimiter},
    spaces\index{space (pretty printing)} or \rmindex{pretty printing}
    annotations (see below).

  \item $\tau$ specifies the syntactic categories of the arguments on the
    left-hand and of the right-hand side. Arguments may be nonterminals or
    valued tokens. If $sy$ is of the form above, $\tau$ must be a nested
    function type with at least $n$ argument positions, say $\tau = [\tau@1,
    \dots, \tau@n] \To \tau'$. The syntactic category of argument $i$ is
    derived from type $\tau@i$ (see $root_of_type$ in
    \S\ref{sec:basic_syntax}). The result, i.e.\ the left-hand side of the
    production, is derived from type $\tau'$. Note that the $\tau@i$ and
    $\tau'$ may be function types.

  \item $c$ is the name of the constant associated with the production. If
    $c$ is the empty string {\tt ""} then this is a \rmindex{copy
    production}. Otherwise, parsing an instance of the phrase $sy$ generates
    the ast {\tt ("$c$" $a@1$ $\ldots$ $a@n$)}, where $a@i$ is the ast
    generated by parsing the $i$-th argument.

  \item $ps$ is an optional list of at most $n$ integers, say {\tt [$p@1$,
    $\ldots$, $p@m$]}, where $p@i$ is the minimal \rmindex{precedence}
    required of any phrase that may appear as the $i$-th argument. Missing
    precedences default to $0$.

  \item $p$ is the \rmindex{precedence} the of this production.
\end{itemize}

Precedences\index{precedence!range of} may range between $0$ and
$max_pri$\indexbold{max_pri@$max_pri$} (= 1000). If you want to ignore them,
the safest way to do so is to use the declaration {\tt $c$ ::\ "$\tau$"
("$sy$")}. The resulting production puts no precedence constraints on any of
its arguments and has maximal precedence itself.

\begin{example}
The following theory specification contains a {\tt consts} section that
encodes the precedence grammar of Example~\ref{ex:precedence} as mixfix
declarations:
\begin{ttbox}
EXP = Pure +
types
  exp 0
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 above text 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";
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 (syn_of EXP.thy)} reveals the actual grammar
productions derived from the above mixfix declarations (lots of additional
information deleted):
\begin{ttbox}
exp = "0"  => "0" (9)
exp = exp[0] "+" exp[1]  => "+" (0)
exp = exp[3] "*" exp[2]  => "*" (2)
exp = "-" exp[3]  => "-" (3)
\end{ttbox}
\end{example}

Let us now have a closer look at the structure of the string $sy$ appearing
in mixfix annotations. This string specifies a list of parsing and printing
directives, namely delimiters\index{delimiter},
arguments\index{argument!mixfix}, spaces\index{space (pretty printing)},
blocks of indentation\index{block (pretty printing)} and optional or forced
line breaks\index{break (pretty printing)}. These are encoded via the
following character sequences:

\begin{description}
  \item[~\ttindex_~] An argument\index{argument!mixfix} position.

  \item[~$d$~] A \rmindex{delimiter}, i.e.\ a non-empty sequence of
    non-special or escaped characters. Escaping a
    character\index{escape character} means preceding it with a {\tt '}
    (quote). Thus you have to write {\tt ''} if you really want a single
    quote. Delimiters may never contain white space, though.

  \item[~$s$~] A non-empty sequence of spaces\index{space (pretty printing)}
    for printing.

  \item[~{\ttindex($n$}~] Open a block\index{block (pretty printing)}. $n$ is
    an optional sequence of digits that specifies the amount of indentation
    to be added when a line break occurs within the block. If {\tt(} is not
    followed by a digit, the indentation defaults to $0$.

  \item[~\ttindex)~] Close a block.

  \item[~\ttindex{//}~] Force a line break\index{break (pretty printing)}.

  \item[~\ttindex/$s$~] Allow a line break\index{break (pretty printing)}.
    Spaces $s$ right after {\tt /} are only printed if the break is not
    taken.
\end{description}

In terms of parsing, arguments are nonterminals or valued tokens, while
delimiters are literal tokens. The other directives have only significance
for printing. The \rmindex{pretty printing} mechanisms of Isabelle is
essentially the one described in \cite{paulson91}.


\subsection{Infixes}

Infix\index{infix} operators associating to the left or right can be declared
conveniently using \ttindex{infixl} or \ttindex{infixr}.

Roughly speaking, the form {\tt $c$ ::\ "$\tau$" (infixl $p$)} abbreviates:
\begin{ttbox}
"op \(c\)" ::\ "\(\tau\)"   ("op \(c\)")
"op \(c\)" ::\ "\(\tau\)"   ("(_ \(c\)/ _)" [\(p\), \(p + 1\)] \(p\))
\end{ttbox}
and {\tt $c$ ::\ "$\tau$" (infixr $p$)} abbreviates:
\begin{ttbox}
"op \(c\)" ::\ "\(\tau\)"   ("op \(c\)")
"op \(c\)" ::\ "\(\tau\)"   ("(_ \(c\)/ _)" [\(p + 1\), \(p\)] \(p\))
\end{ttbox}

Thus, prefixing infixes with \ttindex{op} makes them behave like ordinary
function symbols. Special characters occurring in $c$ have to be escaped as
in delimiters. Also note that the expanded forms above would be actually
illegal at the user level because of duplicate declarations of constants.


\subsection{Binders}

A \bfindex{binder} is a variable-binding construct, such as a
\rmindex{quantifier}. The constant declaration \indexbold{*binder}
\begin{ttbox}
\(c\) ::\ "\(\tau\)"   (binder "\(Q\)" \(p\))
\end{ttbox}
introduces a binder $c$ of type $\tau$, which must have the form $(\tau@1 \To
\tau@2) \To \tau@3$. Its concrete syntax is $Q~x.P$. A binder is like a
generalized quantifier where $\tau@1$ is the type of the bound variable $x$,
$\tau@2$ the type of the body $P$, and $\tau@3$ the type of the whole term.
For example $\forall$ can be declared like this:
\begin{ttbox}
All :: "('a => o) => o"   (binder "ALL " 10)
\end{ttbox}
This allows us to write $\forall x.P$ either as {\tt All(\%$x$.$P$)} or {\tt
ALL $x$.$P$}. When printing terms, Isabelle usually uses the latter form, but
has to fall back on $\mtt{All}(P)$, if $P$ is not an abstraction.

Binders $c$ of type $(\sigma \To \tau) \To \tau$ can be nested; then the
internal form $c(\lambda x@1. c(\lambda x@2. \ldots c(\lambda x@n. P)
\ldots))$ corresponds to external $Q~x@1~x@2 \ldots x@n. P$.

\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\)" ::\ "[idts, \(\tau@2\)] => \(\tau@3\)"   ("(3\(Q\)_./ _)" \(p\))
\end{ttbox}
with $idts$ being the syntactic category for a list of $id$s optionally
constrained (see Figure~\ref{fig:pure_gram}). Note that special characters in
$Q$ have to be escaped as in delimiters.

Additionally, a parse translation\index{parse translation!for binder} for $Q$
and a print translation\index{print translation!for binder} for $c$ is
installed. These perform behind the scenes the translation between the
internal and external forms.



\section{Syntactic translations (macros)} \label{sec:macros}

So far we have pretended that there is a close enough relationship between
concrete and abstract syntax to allow an automatic translation from one to
the other using the constant name supplied with each non-copy production. In
many cases this scheme is not powerful enough. Some typical examples involve
variable binding constructs (e.g.\ {\tt ALL x:A.P} vs.\ {\tt Ball(A, \%x.P)}
or convenient notations for enumerations like finite sets, lists etc.\ (e.g.\
{\tt [x, y, z]} vs.\ {\tt Cons(x, Cons(y, Cons(z, Nil)))}).

Isabelle offers such translation facilities at two different levels, namely
{\bf macros}\indexbold{macro} and {\bf translation functions}.

Macros are specified by first-order rewriting systems that operate on asts.
They are usually easy to read and in most cases not very difficult to write.
Unfortunately, some more obscure translations cannot be expressed as macros
and you have to fall back on the more powerful mechanism of translation
functions written in \ML. These are quite unreadable and hard to write (see
\S\ref{sec:tr_funs}).

\medskip
Let us now get started with the macro system by a simple example:

\begin{example}~ \label{ex:set_trans}

\begin{ttbox}
SET = Pure +
types
  i, o 0
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}

This and the following theories are complete working examples, though they
are fragmentary as they contain merely syntax. They are somewhat fashioned
after {\tt ZF/zf.thy}, where you should look for a good real-world example.

{\tt SET} defines constants for set comprehension ({\tt Collect}),
replacement ({\tt Replace}) and bounded universal quantification ({\tt
Ball}). Without additional syntax you would have to express $\forall x \in A.
P(x)$ as {\tt Ball(A, P)}. Since this is quite awkward, we define additional
constants with appropriate concrete syntax. These constants are decorated
with {\tt\at} to stress their pure syntactic purpose; they should never occur
within the final well-typed terms. Another consequence is that the user
cannot refer to such names directly, since 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.
\end{example}

This is only a very simple but common instance of a more powerful mechanism.
As a specification of what is to be translated, it should be comprehensible
without further explanations. But there are also some snags and other
peculiarities that are typical for macro systems in general. The purpose of
this section is to explain how Isabelle's macro system really works.


\subsection{Specifying macros}

Basically macros are rewrite rules on asts. But unlike other macro systems of
various programming languages, Isabelle's macros work two way. Therefore a
syntax contains two lists of rules: one for parsing and one for printing.

The {\tt translations} section\index{translations section@{\tt translations}
section} consists of a list of rule specifications of the form:

\begin{center}
{\tt $[$ ($root$) $]$ $string$ $[$ => $|$ <= $|$ == $]$ $[$ ($root$) $]$
$string$}.
\end{center}

This specifies a \rmindex{parse rule} ({\tt =>}) a \rmindex{print rule} ({\tt
<=}) or both ({\tt ==}). The two $string$s preceded by optional parenthesized
$root$s denote the left-hand and right-hand side of the rule as `source
code', i.e.\ in the usual syntax of terms.

Rules are internalized wrt.\ an intermediate signature that is obtained from
the parent theories' ones by adding all material of all sections preceding
{\tt translations} in the {\tt .thy} file. Especially, new syntax defined in
{\tt consts} is already effective.

Then part of the process that transforms input strings into terms is applied:
lexing, parsing and parse ast translations (see \S\ref{sec:asts}). Macros
specified in the parents are {\em not\/} expanded. Also note that the lexer
runs in a different mode that additionally accepts identifiers of the form
$\_~letter~quasiletter^*$ (like {\tt _idt}, {\tt _K}). The syntactic category
to parse is specified by $root$, which defaults to {\tt logic}.

Finally, Isabelle tries to guess which atoms of the resulting ast of the rule
should be treated as constants during matching (see below). These names are
extracted from all class, type and constant declarations made so far.

\medskip
The result are two lists of translation rules in internal form, that is pairs
of asts. They can be viewed using {\tt Syntax.print_syntax} (sections
\ttindex{parse_rules} and \ttindex{print_rules}). For {\tt SET} of
Example~\ref{ex: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}

Note that in this notation all rules are oriented left to right. In the {\tt
translations} section, which has been split into two parts, print rules
appeared right to left.

\begin{warn}
Be careful not to choose names for variables in rules that are actually
treated as constant. If in doubt, check the rules in their internal form or
the section labeled {\tt consts} in the output of {\tt Syntax.print_syntax}.
\end{warn}


\subsection{Applying rules}

In the course of parsing and printing terms, asts are generated as an
intermediate form as pictured in Figure~\ref{fig:parse_print}. These asts are
normalized wrt.\ the given lists of translation rules in a uniform manner. As
stated earlier, asts are supposed to be first-order `terms'. The rewriting
systems derived from {\tt translations} sections essentially resemble
traditional first-order term rewriting systems. We first examine how a single
rule is applied.

Let $t$ be the ast to be normalized and $(l, r)$ some translation rule. A
subast $u$ of $t$ is called {\bf redex}\indexbold{redex (ast)} (reducible
expression), if it is an instance of $l$. In this case $l$ is said to {\bf
match}\indexbold{match (ast)} $u$. A redex matched by $l$ may be replaced by
the corresponding instance of $r$, thus {\bf rewriting}\index{rewrite (ast)}
the ast $t$.

Matching requires some notion of {\bf place-holders}\indexbold{place-holder
(ast)} that may occur in rule patterns but not in ordinary asts, which are
considered ground. Here we simply use {\tt Variable}s for this purpose.

More formally, the matching of $u$ by $l$ is performed as follows (the rule
pattern is the second argument): \index{match (ast)@$match$ (ast)}
\begin{itemize}
  \item $match(\Constant x, \Constant x) = \mbox{OK}$.

  \item $match(\Variable x, \Constant x) = \mbox{OK}$.

  \item $match(u, \Variable x) = \mbox{OK, bind}~x~\mbox{to}~u$.

  \item $match(\Appl{u@1, \ldots, u@n}, \Appl{l@1, \ldots, l@n}) = match(u@1,
    l@1), \ldots, match(u@n, l@n)$.

  \item $match(u, l) = \mbox{FAIL}$ in any other case.
\end{itemize}

This means that a {\tt Constant} pattern matches any atomic asts of the same
name, while a {\tt Variable} matches any ast. If successful, $match$ yields a
substitution $\sigma$ that is applied to $r$, generating the appropriate
instance that replaces $u$.

\medskip
In order to make things simple and fast, ast rewrite rules $(l, r)$ are
restricted by the following conditions:
\begin{itemize}
  \item Rules have to be left linear, i.e.\ $l$ must not contain any {\tt
    Variable} more than once.

  \item Rules must have constant heads, i.e.\ $l = \mtt"c\mtt"$ or $l =
    (\mtt"c\mtt" ~ x@1 \ldots x@n)$.

  \item The set of variables contained in $r$ has to be a subset of those of
    $l$.
\end{itemize}

\medskip
Having first-order matching in mind, the second case of $match$ may look a
bit odd. But this is exactly the place, where {\tt Variable}s of non-rule
asts behave like {\tt Constant}s. The deeper meaning of this is related with
asts being very `primitive' in some sense, ignorant of the underlying
`semantics', not far removed from parse trees. At this level it is not yet
known, which $id$s will become constants, bounds, frees, types or classes. As
$ast_of_pt$ (see \S\ref{sec:asts}) shows, former parse tree heads appear in
asts as {\tt Constant}s, while $id$s, $var$s, $tfree$s and $tvar$s become
{\tt Variable}s.

This is at variance with asts generated from terms before printing (see
$ast_of_term$ in \S\ref{sec:asts}), where all constants and type constructors
become {\tt Constant}s.

\begin{warn}
This means asts may contain quite a messy mixture of {\tt Variable}s and {\tt
Constant}s, which is insignificant at macro level because $match$ treats them
alike.
\end{warn}

Because of this behaviour, different kinds of atoms with the same name are
indistinguishable, which may make some rules prone to misbehaviour. Regard
the following fragmentary example:
\begin{ttbox}
types
  Nil 0
consts
  Nil     :: "'a list"
  "[]"    :: "'a list"    ("[]")
translations
  "[]"    == "Nil"
\end{ttbox}
Then 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.


\subsection{Rewriting strategy}

When normalizing an ast by repeatedly applying translation rules until no
more rule is applicable, there are in each step two choices: which rule to
apply next, and which redex to reduce.

We could assume that the user always supplies terminating and confluent
rewriting systems, but this would often complicate things unnecessarily.
Therefore, we reveal part of the actual rewriting strategy: The normalizer
always applies the first matching rule reducing an unspecified redex chosen
first.

Thereby, `first rule' is roughly speaking meant wrt.\ the appearance of the
rules in the {\tt translations} sections. But this is more tricky than it
seems: If a given theory is {\em extended}, new rules are simply appended to
the end. But if theories are {\em merged}, it is not clear which list of
rules has priority over the other. In fact the merge order is left
unspecified. This shouldn't cause any problems in practice, since
translations of different theories usually do not overlap. {\tt
Syntax.print_syntax} shows the rules in their internal order.

\medskip
You can watch the normalization of asts during parsing and printing by
setting \ttindex{Syntax.trace_norm_ast} to {\tt true}. An alternative is the
use of \ttindex{Syntax.test_read}, which is always in trace mode. The
information displayed when tracing\index{tracing (ast)} 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{More examples}

Let us first reconsider Example~\ref{ex:set_trans}, which is concerned with
variable binding constructs.

There is a minor disadvantage over an implementation via translation
functions (as done for binders):

\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 get lost. E.g.\
\verb|Ball(A, %x. P(x))| is contracted to {\tt Ball(A, P)}, the print rule is
no longer applicable and the output will be {\tt Ball(A, P)}. Note that
$\eta$-expansion via macros is {\em not\/} possible.
\end{warn}

\medskip
Another common trap are meta 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). E.g.\ 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}|. Therefore your
syntax should be ready for such constraints to be re-read. This is the case
in our example, because of the category {\tt idt} of the first argument.

\begin{warn}
Choosing {\tt id} instead of {\tt idt} is a very common error, especially
since it appears in former versions of most of Isabelle's object-logics.
\end{warn}

\begin{example} \label{ex:finset_trans}
This example demonstrates the use of recursive macros to implement a
convenient notation for finite sets.
\begin{ttbox}
FINSET = SET +
types
  is 0
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}.
Externally we would like to see \verb|{x, y, z}| rather than {\tt insert(x,
insert(y, insert(z, empty)))}.

First we define the generic syntactic category {\tt is} for one or more
objects of type {\tt i} separated by commas (including breaks for pretty
printing). The category has to be declared as a 0-place type constructor, but
without {\tt arities} declaration. Hence {\tt is} is not a logical type, no
default productions will be added, and we can cook our own syntax for {\tt
is} (first two lines of {\tt consts} section). If we had needed generic
enumerations of type $\alpha$ (i.e.\ {\tt logic}), we could have used the
predefined category \ttindex{args} and skipped this part altogether.

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 specifies a block of
indentation for pretty printing. The category {\tt is} can later be reused
for other enumerations like lists or tuples.

The translations may look a bit odd at first sight, but rules can only be
fully understood in their internal forms, which are:
\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. Note that
the parse rules only work in this order.

\medskip
Some rules are prone to misbehaviour, as
\verb|%empty insert. insert(x, empty)| shows, which is printed as
\verb|%empty insert. {x}|. This problem arises, because the ast rewriter
cannot discern constants, frees, bounds etc.\ 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'. It is good
practice to choose non-identifiers here like {\tt\at Finset} or sufficiently
long and strange names.
\end{example}

\begin{example} \label{ex:prod_trans}
One of the well-formedness conditions for ast rewrite rules stated earlier
implies that you can never introduce new {\tt Variable}s on the right-hand
side. Something like \verb|"K(B)" => "%x. B"| is illegal and could cause
variable capturing, if it were allowed. In such cases you usually have to
fall back on translation functions. But there is a trick that makes things
quite readable in some cases: {\em calling parse translations by parse
rules}. This is demonstrated here.
\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)
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}

{\tt Pi} is an internal constant for constructing dependent products. Two
external forms exist: {\tt PROD x:A.B}, the general case, and {\tt A -> B},
an abbreviation for \verb|Pi(A, %x.B)| with {\tt B} not actually depending on
{\tt x}.

Now the second parse rule is where the trick comes in: {\tt _K(B)} is
introduced during ast rewriting, which later becomes \verb|%x.B| due to a
parse translation associated with \ttindex{_K}. Note that a leading {\tt _}
in $id$s is allowed in translation rules, but not in ordinary terms. This
special behaviour of the lexer is very useful for `forging' asts containing
names that are not directly accessible normally.

Unfortunately, there is no such trick for printing, so we have to add a {\tt
ML} section for the print translation \ttindex{dependent_tr'}.

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} for more of the arcane lore of translation functions.
\end{example}



\section{Translation functions *} \label{sec:tr_funs}

This section is about the remaining translation mechanism which enables the
designer of theories to do almost everything with terms or asts during the
parsing or printing process, by writing \ML-functions. The logic \LK\ is a
good example of a quite sophisticated use of this to transform between
internal and external representations of associative sequences. The high
level macro system described in \S\ref{sec:macros} fails here completely.

\begin{warn}
A full understanding of the matters presented here 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. You probably do not really want to
use translation functions at all!
\end{warn}

As already mentioned in \S\ref{sec:asts}, there are four kinds of translation
functions. All such functions are associated with a name which specifies an
ast's or term's head invoking that function. Such names can be (logical or
syntactic) constants 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}. The user can
add new ones via the {\tt ML} section\index{ML section@{\tt ML} section} of a
{\tt .thy} file. But there may never be more than one function of the same
kind per name.

\begin{warn}
Conceptually, the {\tt ML} section should appear between {\tt consts} and
{\tt translations}, i.e.\ newly installed translation functions are already
effective when macros and logical rules are parsed. {\tt ML} has to be the
last section because the {\tt .thy} file parser is unable to detect the end
of \ML\ code in another way than by end-of-file.
\end{warn}

All text of the {\tt ML} section is simply copied verbatim into the \ML\ file
generated from a {\tt .thy} file. Definitions made here by the user become
components of a \ML\ structure of the same name as the theory to be created.
Therefore local things should be declared within {\tt local}. The following
special \ML\ values, which are all optional, serve as the interface for the
installation of user defined translation functions.

\begin{ttbox}
val parse_ast_translation: (string * (ast list -> ast)) list
val parse_translation: (string * (term list -> term)) list
val print_translation: (string * (term list -> term)) list
val print_ast_translation: (string * (ast list -> ast)) list
\end{ttbox}

The basic idea behind all four kinds of functions is relatively simple (see
also Figure~\ref{fig:parse_print}): Whenever --- during the transformations
between parse trees, asts and terms --- 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 will be $f \mtt[ x@1, \ldots,
x@n \mtt]$. Thereby, $x@1, \ldots, x@n$ (with $n \ge 0$) are asts for ast
translations and terms for term translations. A `combination' at ast level is
of the form $\Constant c$ or $\Appl{\Constant c, x@1, \ldots, x@n}$, and at
term level $\ttfct{Const} (c, \tau)$ or $\ttfct{Const} (c, \tau) \ttrel{\$}
x@1 \ttrel{\$} \dots \ttrel{\$} x@n$.

\medskip
Translation functions at ast level differ from those at term level only in
the same way, as asts and terms differ. Terms, being more complex and more
specific, allow more sophisticated transformations (typically involving
abstractions and bound variables).

On the other hand, {\em parse\/} (ast) translations differ from {\em print\/}
(ast) translations more fundamentally:
\begin{description}
  \item[Parse (ast) translations] are applied bottom-up, i.e.\ the arguments
    supplied ($x@1, \ldots, x@n$ above) are already in translated form.
    Additionally, they may not fail, exceptions are re-raised after printing
    an error message.

  \item[Print (ast) translations] are applied top-down, i.e.\ supplied with
    arguments that are partly still in internal form. The result is again fed
    into the translation machinery as a whole. Therefore a print (ast)
    translation should not introduce as head a constant of the same name that
    invoked it in the first place. Alternatively, exception \ttindex{Match}
    may be raised, indicating failure of translation.
\end{description}

Another difference between the parsing and the printing process is, which
atoms are {\tt Constant}s or {\tt Const}s, i.e.\ able to invoke translation
functions.

For parse ast translations only former parse tree heads are {\tt Constant}s
(see also $ast_of_pt$ in \S\ref{sec:asts}). These and additionally introduced
{\tt Constant}s (e.g.\ by macros), become {\tt Const}s for parse translations
(see also $term_of_ast$ in \S\ref{sec:asts}).

The situation is slightly different, when terms are prepared for printing,
since the role of atoms is known. Initially, all logical constants and type
constructors may invoke print translations. New constants may be introduced
by these or by macros, able to invoke parse ast translations.


\subsection{A simple example *}

Presenting a simple and useful example of translation functions is not that
easy, since the macro system is sufficient for most simple applications. By
convention, translation functions always have names ending with {\tt
_ast_tr}, {\tt _tr}, {\tt _tr'} or {\tt _ast_tr'}. You may look for such
names in the sources of Pure Isabelle for more examples.

\begin{example} \label{ex:tr_funs}

We continue Example~\ref{ex:prod_trans} by presenting the \ML\ sources of the
parse translation for \ttindex{_K} and the print translation
\ttindex{dependent_tr'}:

\begin{ttbox}
(* nondependent abstraction *)

fun k_tr (*"_K"*) [t] = Abs ("x", dummyT, incr_boundvars 1 t)
  | k_tr (*"_K"*) ts = raise_term "k_tr" ts;

(* dependent / nondependent quantifiers *)

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}

This text is taken from the Pure sources, ordinary user translations would
typically appear within the {\tt ML} section of the {\tt .thy} file.

\medskip
If {\tt k_tr} is called with exactly one argument $t$, it creates a new {\tt
Abs} node with a body derived from $t$: loose {\tt Bound}s, i.e.\ those
referring to outer {\tt Abs}s, are incremented using
\ttindex{incr_boundvars}. This and many other basic term manipulation
functions are defined in {\tt Pure/term.ML}, the comments there being in most
cases the only documentation.

Since terms fed into parse translations are not yet typed, the type of the
bound variable in the new {\tt Abs} is simply {\tt dummyT}.

\medskip
The argument $(q, r)$ for {\tt dependent_tr'} is supplied already during the
installation within an {\tt ML} section. This yields a parse translation that
transforms something like $c(A, \mtt{Abs}(x, T, B), t@1, \ldots, t@n)$ into
$q(x', A, B', t@1, \ldots, t@n)$ or $r(A, B, t@1, \ldots, t@n)$. The latter
form, if $B$ does not actually depend on $x$. This is checked using
\ttindex{loose_bnos}, yet another function of {\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}s referring to our {\tt Abs} node replaced by
$\ttfct{Free} (x', \mtt{dummyT})$.

We have to be more careful with types here. While types of {\tt Const}s are
completely 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. Thus, a
constraint of $x'$ may only appear at its binding place, since {\tt Free}s of
$B'$ replacing the appropriate {\tt Bound}s of $B$ via \ttindex{variant_abs}
have all type {\tt dummyT}. \end{example}



\section{Example: some minimal logics} \label{sec:min_logics}

This concluding section presents some examples that are very simple from a
syntactic point of view. They should rather demonstrate how to define new
object-logics from scratch. In particular we need to say how an object-logic
syntax is hooked up to the meta-logic. Since all theorems must conform to the
syntax for $prop$ (see Figure~\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 category $o$ of formulae. These formulae can now
appear in axioms and theorems wherever $prop$ does if you add the production
\[ prop ~=~ o. \]
More precisely, you need a coercion from formulae to propositions:
\begin{ttbox}
Base = Pure +
types
  o 0
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 {\em minimal logic\/} of
implication. Its definition in Isabelle needs no advanced features but
illustrates the overall mechanism quite 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 you can start to prove theorems in this logic:
\begin{ttbox}
goal Hilbert.thy "P --> P";
{\out Level 0}
{\out P --> P}
{\out  1.  P --> P}
by (resolve_tac [Hilbert.MP] 1);
{\out Level 1}
{\out P --> P}
{\out  1.  ?P --> P --> P}
{\out  2.  ?P}
by (resolve_tac [Hilbert.MP] 1);
{\out Level 2}
{\out P --> P}
{\out  1.  ?P1 --> ?P --> P --> P}
{\out  2.  ?P1}
{\out  3.  ?P}
by (resolve_tac [Hilbert.S] 1);
{\out Level 3}
{\out P --> P}
{\out  1.  P --> ?Q2 --> P}
{\out  2.  P --> ?Q2}
by (resolve_tac [Hilbert.K] 1);
{\out Level 4}
{\out P --> P}
{\out  1.  P --> ?Q2}
by (resolve_tac [Hilbert.K] 1);
{\out Level 5}
{\out P --> P}
{\out No subgoals!}
\end{ttbox}
As you can see, this Hilbert-style formulation of minimal logic is easy to
define but difficult to use. The following natural deduction formulation is
far preferable:
\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: {\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 {\em admissible\/} rule in {\tt Hilbert},
something that can only be shown by induction over all possible proofs in
{\tt Hilbert}.

It is a very simple matter to 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)
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 define:
\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!