doc-src/Logics/defining.tex
 changeset 104 d8205bb279a7 child 108 e332c5bf9e1f
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Logics/defining.tex	Wed Nov 10 05:00:57 1993 +0100
@@ -0,0 +1,1557 @@
+%% $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
+
+
+%% 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)} \\
+    &$|$& \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 for (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} here.
+\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 $(\dots)c$, where $c$ is a subclass of $logic$, the following
+\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 (or delimiters \index{delimiter}) 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. Additionally, if the +index is 0, it may be dropped altogether, e.g.\ {\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 containing quite a lot of +material, wherefore there is no toplevel pretty printer set up for displaying +it automatically. You have to call one of the following functions instead: +\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} +where {\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 to parse trees (macro expansion etc.). See \S\ref{sec:macros} +and \S\ref{sec:tr_funs} for more details on translations. + +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 stuff 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 a type 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 ASCII as {\tt A[n]}, literal tokens are quoted. + Note that 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 stuff (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. But unfortunately, as more and more material accumulates, the +output becomes even more verbose. Note that 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 (well, actually a token list produced by the +lexer) and produces a \rmindex{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 at about half of the +time. By now you shouldn't 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 abstraction, meta implication 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 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 (which provide the user interface for +defining syntax) if they are required to separate tokens. Mixfix declarations +may also contain pretty printing annotations. See \S\ref{sec:mixfix} for +details. + + + +\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 exhibiting the full power of +extending a theory's syntax, and some shortcuts for common cases like infix +operators. + +The general \bfindex{mixfix declaration} as it may occur within a {\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 do 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}). + +Issuing {\tt Syntax.print_gram (syn_of EXP.thy)} will reveal the actual +grammar productions derived from the above mixfix declarations (lots of +additional stuff 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 that described in \cite{FIXME:ML_for_the_Working_Programmer}. + + +\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 ids 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 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 enumeration 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. +But 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 hard to write and nearly unreadable by the casual +user (see \S\ref{sec:tr_funs}). + +\medskip +Let us now getting 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 'forge' terms containing such names, like {\tt\at Collect(x)}, for +being syntactically incorrect. + +The included 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, whose general form is: +{\tt [ (root) ] string [ => | <= | == ] [ (root) ] +string}. + +This specifies a \rmindex{parse rule} ({\tt =>}) a \rmindex{print rule} ({\tt +<=}) or both ({\tt ==}). The two strings preceded by optional parenthesized +roots denote the left-hand and right-hand side of the rule as 'source +code'. + +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 as +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} +(\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 sort of first order terms. The +rewriting systems derived from {\tt translations} sections essentially +resemble traditional first order term rewriting systems. We'll first examine +how a single rule is applied. + +Let t be the ast to be normalized and (l, r) some translation rule. A +(improper) 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 for all place-holders in l, equalling it with the +redex u. Then \sigma 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', only short way from parse trees. At this level it is not yet +known, which ids 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 ids, vars, tfrees and tvars 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 +issuing: \index{*Syntax.trace_norm_ast} +\begin{ttbox} +Syntax.trace_norm_ast := true; +\end{ttbox} +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 be later reused +for other enumerations like lists or tuples. + +The translations might look a bit odd at the first glance. But rules can be +only 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 print translations by print +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 ids 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 some \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 + of 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 a {\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 undocumented 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 (only 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!
+