changeset 104 d8205bb279a7
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Logics/old.defining.tex	Wed Nov 10 05:00:57 1993 +0100
@@ -0,0 +1,871 @@
+\chapter{Defining Logics} \label{Defining-Logics}
+This chapter is intended for Isabelle experts.  It explains how to define new
+logical systems, Isabelle's {\it raison d'\^etre}.  Isabelle logics are
+hierarchies of theories.  A number of simple examples are contained in the
+introductory manual; the full syntax of theory definitions is shown in the
+{\em Reference Manual}.  The purpose of this chapter is to explain the
+remaining subtleties, especially some context conditions on the class
+structure and the definition of new mixfix syntax.  A full understanding of
+the material requires knowledge of the internal representation of terms (data
+type {\tt term}) as detailed in the {\em Reference Manual}.  Sections marked
+with a * can be skipped on first reading.
+\section{Classes and Types *}
+\index{*arities!context conditions}
+Type declarations are subject to the following two well-formedness
+\item There are no two declarations $ty :: (\vec{r})c$ and $ty :: (\vec{s})c$
+  with $\vec{r} \neq \vec{s}$.  For example
+types ty 1
+arities ty :: (\{logic\}) logic
+        ty :: (\{\})logic
+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
+classes term < logic
+types ty 1
+arities ty :: (\{logic\})logic
+        ty :: (\{\})term
+leads to an error message and fails.
+These conditions guarantee principal types~\cite{nipkow-prehofer}.
+\section{Precedence Grammars}
+\index{precedence grammar|(}
+The precise syntax of a logic is best defined by a context-free grammar.
+These grammars obey the following conventions: identifiers denote
+nonterminals, {\tt typewriter} fount denotes terminals, repetition is
+indicated by \dots, and alternatives are separated by $|$.
+In order to simplify the description of mathematical languages, we introduce
+an extended format which permits {\bf precedences}\index{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 q \ge p.~(A@q=\gamma) \in G
+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.
+The following simple grammar for arithmetic expressions demonstrates how
+binding power and associativity of operators can be enforced by precedences.
+$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$
+The choice of precedences determines that \verb$-$ binds tighter than
+\verb$*$ which binds tighter than \verb$+$, and that \verb$+$ and \verb$*$
+associate to the left and right, respectively.
+To minimize the number of subscripts, we adopt the following conventions:
+\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.
+In addition, we write the production $A@p = \alpha$ as $A = \alpha~(p)$.
+Using these conventions and assuming $max_pri=9$, the grammar in
+Example~\ref{PrecedenceEx} becomes
+$A$ & = & {\tt0} & \hspace*{4em} \\
+ & $|$ & {\tt(} $A$ {\tt)} \\
+ & $|$ & $A$ {\tt+} $A@1$ & (0) \\
+ & $|$ & $A@3$ {\tt*} $A@2$ & (2) \\
+ & $|$ & {\tt-} $A@3$ & (3)
+\index{precedence grammar|)}
+\section{Basic syntax *}
+An informal account of most of Isabelle's syntax (meta-logic, types etc) is
+contained in {\em Introduction to Isabelle}.  A precise description using a
+precedence grammar is shown in Figure~\ref{MetaLogicSyntax}.  This description
+is the basis of all extensions by object-logics.
+$prop$ &=& \ttindex{PROP} $aprop$ ~~$|$~~ {\tt(} $prop$ {\tt)} \\
+     &$|$& $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\{\}}
+                ~~$|$~~ {\tt\{} $id$ {\tt,} \dots {\tt,} $id$ {\tt\}} 
+\caption{Meta-Logic Syntax}
+The following main categories are defined:
+\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 (see below).
+\item[$fun$] Terms potentially of function type.
+\item[$type$] Types.
+\item[$idts$] a list of identifiers, possibly constrained by types.  Note
+  that $x::nat~y$ is parsed as $x::(nat~y)$, i.e.\ $y$ is treated like a
+  type constructor applied to $nat$.
+The predefined types $id$, $var$, $tfree$ and $tvar$ represent identifiers
+({\tt f}), unknowns ({\tt ?f}), type variables ({\tt 'a}), and type unknowns
+({\tt ?'a}) respectively.  If we think of them as nonterminals with
+predefined syntax, we may assume that all their productions have precedence
+\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
+productions are added:
+$ty$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $ty$ {\tt)} \\
+  &$|$& $fun@{max_pri}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)}\\
+  &$|$& $ty@{max_pri}$ {\tt::} $type$\\\\
+$logic$ &=& $ty$
+\section{Mixfix syntax}
+We distinguish between abstract and concrete syntax.  The {\em abstract}
+syntax is given by the typed constants of a theory.  Abstract syntax trees are
+well-typed terms, i.e.\ values of \ML\ type {\tt term}.  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)$, where $f$ is a constant or variable.  Since this notation
+quickly becomes unreadable, Isabelle supports syntax definitions in the form
+of unrestricted context-free grammars using mixfix annotations.
+Mixfix annotations describe the {\em concrete} syntax, its 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 associates
+an Isabelle constant with it.
+A {\em mixfix declaration} {\tt consts $c$ ::\ $\tau$ ($sy$ $ps$ $p$)} is
+interpreted as a grammar pro\-duction as follows:
+\item $sy$ is the right-hand side of this production, specified as a {\em
+    mixfix annotation}.  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/nonterminal and the strings
+  $\alpha@i$ do not contain ``{\tt_}''.
+\item $\tau$ specifies the types of the nonterminals on the left and right
+  hand side. If $sy$ is of the form above, $\tau$ must be of the form
+  $[\tau@1,\dots,\tau@n] \To \tau'$.  Then argument $i$ is of type $\tau@i$
+  and the result, i.e.\ the left-hand side of the production, is of type
+  $\tau'$.  Both the $\tau@i$ and $\tau'$ may be function types.
+\item $c$ is the name of the Isabelle constant associated with this production.
+  Parsing an instance of the phrase $sy$ generates the {\tt term} {\tt
+    Const($c$,dummyT\footnote{Proper types are inserted later on.  See
+      \S\ref{Typing}})\$$a@1$\$$\dots$\$$a@n$}\index{*dummyT}, where $a@i$ is
+  the term generated by parsing the $i^{th}$ argument.
+\item $ps$ must be of the form $[p@1,\dots,p@n]$, where $p@i$ is the
+  minimal precedence\index{precedence} required of any phrase that may appear
+  as the $i^{th}$ argument.  The null list is interpreted as a list of 0's of
+  the appropriate length.
+\item $p$ is the precedence of this production.
+Notice that there is a close connection between abstract and concrete syntax:
+each production has an associated constant, and types act as {\bf syntactic
+  categories} in the concrete syntax.  To emphasize this connection, we
+sometimes refer to the nonterminals on the right-hand side of a production as
+its arguments and to the nonterminal on the left-hand side as its result.
+The maximal legal precedence is called \ttindexbold{max_pri}, which is
+currently 1000.  If you want to ignore precedences, the safest way to do so is
+to use the annotation {\tt($sy$)}: this production puts no precedence
+constraints on any of its arguments and has maximal precedence itself, i.e.\ 
+it is always applicable and does not exclude any productions of its
+In mixfix notation the grammar in Example~\ref{PrecedenceEx} can be written
+as follows:
+types exp 0
+consts "0"  ::              "exp"  ("0" 9)
+       "+"  :: "[exp,exp] => exp"  ("_ + _" [0,1] 0)
+       "*"  :: "[exp,exp] => exp"  ("_ * _" [3,2] 2)
+       "-"  ::       "exp => exp"  ("- _"   [3]   3)
+Parsing the string \verb!"0 + - 0 + 0"! produces the term {\tt
+  $p$\$($p$\$($m$\$$z$)\$$z$)\$$z$} where {\tt$p =$ Const("+",dummyT)},
+{\tt$m =$ Const("-",dummyT)}, and {\tt$z =$ Const("0",dummyT)}.
+The interpretation of \ttindex{_} in a mixfix annotation is always as a {\bf
+  meta-character}\index{meta-character} which does not represent itself but
+an argument position.  The following characters are also meta-characters:
+'   (   )   /
+Preceding any character with a quote (\verb$'$) turns it into an ordinary
+character.  Thus you can write \verb!''! if you really want a single quote.
+The purpose of the other meta-characters is explained in
+\S\ref{PrettyPrinting}.  Remember that in \ML\ strings \verb$\$ is already a
+(different kind of) meta-character.
+\subsection{Types and syntactic categories *}
+The precise mapping from types to syntactic categories is defined by the
+following function:
+N(\tau@1\To\tau@2) &=& fun \\
+N((\tau@1,\dots,\tau@n)ty) &=& ty \\
+N(\alpha) &=& logic
+Only the outermost type constructor is taken into account and type variables
+can range over all logical types.  This catches some ill-typed terms (like
+$Cons(x,0)$, where $Cons :: [\alpha,\alpha list] \To \alpha list$ and $0 ::
+nat$) but leaves the real work to the type checker.
+In terms of the precedence grammar format introduced in
+\S\ref{PrecedenceGrammars}, the declaration
+consts \(c\) :: "[\(\tau@1\),\dots,\(\tau@n\)]\(\To\tau\)" ("\(\alpha@0\_\alpha@1\dots\alpha@{n-1}\_\alpha@n\)") [\(p@1\),\dots,\(p@n\)] \(p\))
+defines the production
+\[ N(\tau)@p ~~=~~ \alpha@0 ~N(\tau@1)@{p@1}~ \alpha@1~ \dots
+                  ~\alpha@{n-1} ~N(\tau@n)@{p@n}~ \alpha@n
+\subsection{Copy productions *}
+Productions which do not create a new node in the abstract syntax tree are
+called {\bf copy productions}.  They must have exactly one nonterminal on
+the right hand side.  The term generated when parsing that nonterminal is
+simply passed up as the result of parsing the whole copy production.  In
+Isabelle a copy production is indicated by an empty constant name, i.e.\ by
+consts "" :: \(\tau\)  (\(sy\) \(ps\) \(p\))
+A special kind of copy production is one where, modulo white space, $sy$ is
+{\tt"_"}.  It is called a {\bf 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.  The following example demonstrates the effect:
+the grammar defined by
+types A,B,C 0
+consts AB :: "B => A"  ("A _" [10] 517)
+       "" :: "C => B"  ("_"   [0]  100)
+       x  :: "C"       ("x"          5)
+       y  :: "C"       ("y"         15)
+admits {\tt"A y"} but not {\tt"A x"}.  Had the constant in the second
+production been some non-empty string, both {\tt"A y"} and {\tt"A x"} would
+be legal.
+\section{Lexical conventions}
+The lexical analyzer distinguishes the following kinds of tokens: delimiters,
+identifiers, unknowns, type variables and type unknowns.
+Delimiters are user-defined, i.e.\ they are extracted from the syntax
+definition.  If $\alpha@0\_\alpha@1\dots\alpha@{n-1}\_\alpha@n$ is a mixfix
+annotation, each $\alpha@i$ is decomposed into substrings
+$\beta@1~\dots~\beta@k$ which are separated by and do not contain
+\bfindex{white space} ( = blanks, tabs, newlines).  Each $\beta@j$ becomes a
+delimiter.  Thus a delimiter can be an arbitrary string not containing white
+The lexical syntax of identifiers and variables ( = unknowns) is defined in
+the introductory manual.  Parsing an identifier $f$ generates {\tt
+  Free($f$,dummyT)}\index{*dummyT}.  Parsing a variable {\tt?}$v$ generates
+{\tt Var(($u$,$i$),dummyT)} where $i$ is the integer value of the longest
+numeric suffix of $v$ (possibly $0$), and $u$ is the remaining prefix.
+Parsing a variable {\tt?}$v{.}i$ generates {\tt Var(($v$,$i$),dummyT)}.  The
+following table covers the four different cases that can arise:
+"?v" & "?v.7" & "?v5" & "?v7.5" \\
+Var(("v",0),$d$) & Var(("v",7),$d$) & Var(("v",5),$d$) & Var(("v7",5),$d$)
+where $d = {\tt dummyT}$.
+In mixfix annotations, \ttindexbold{id}, \ttindexbold{var},
+\ttindexbold{tfree} and \ttindexbold{tvar} are the predefined categories of
+identifiers, unknowns, type variables and type unknowns, respectively.
+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 delimiter and an identifier or variable (like
+{\tt ALL}) is treated as a delimiter.  White spaces are separators.
+An important consequence of this translation scheme is that delimiters need
+not be separated by white space to be recognized as separate.  If \verb$"-"$
+is a delimiter but \verb$"--"$ is not, the string \verb$"--"$ is treated as
+two consecutive occurrences of \verb$"-"$.  This is in contrast to \ML\ which
+would treat \verb$"--"$ as a single (undeclared) identifier.  The
+consequence of Isabelle's more liberal scheme is that the same string may be
+parsed in a different way after extending the syntax: after adding
+\verb$"--"$ as a delimiter, the input \verb$"--"$ is treated as
+a single occurrence of \verb$"--"$.
+\section{Infix operators}
+{\tt Infixl} and {\tt infixr} declare infix operators which associate to the
+left and right respectively.  As in \ML, prefixing infix operators with
+\ttindexbold{op} turns them into curried functions.  Infix declarations can
+be reduced to mixfix ones as follows:
+"$c$" ::~$\tau$ (\ttindexbold{infixl} $p$) &
+"op $c$" ::~$\tau$ ("_ $c$ _" [$p$,$p+1$] $p$) \\
+"$c$" ::~$\tau$ (\ttindexbold{infixr} $p$) &
+"op $c$" ::~$\tau$ ("_ $c$ _" [$p+1$,$p$] $p$)
+A {\bf binder} is a variable-binding constant, such as a quantifier.
+The declaration
+consts \(c\) :: \(\tau\)  (binder \(Q\) \(p\))
+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.t$.  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 $t$, and
+$\tau@3$ the type of the whole term.  For example $\forall$ can be declared
+like this:
+consts All :: "('a => o) => o"  (binder "ALL " 10)
+This allows us to write $\forall x.P$ either as {\tt ALL $x$.$P$} or {\tt
+  All(\%$x$.$P$)}; the latter form is for purists only.
+In case $\tau@2 = \tau@3$, nested quantifications can be written as $Q~x@1
+\dots x@n.t$.  From a syntactic point of view,
+consts \(c\) :: "\((\tau@1\To\tau@2)\To\tau@3\)"  (binder "\(Q\)" \(p\))
+is equivalent to
+consts \(c\)   :: "\((\tau@1\To\tau@2)\To\tau@3\)"
+       "\(Q\)" :: "[idts,\(\tau@2\)] => \(\tau@3\)"  ("\(Q\)_.  _" \(p\))
+where {\tt idts} is the syntactic category $idts$ defined in
+However, there is more to binders than concrete syntax: behind the scenes the
+body of the quantified expression has to be converted into a
+$\lambda$-abstraction (when parsing) and back again (when printing).  This
+is performed by the translation mechanism, which is discussed below.  For
+binders, the definition of the required translation functions has been
+automated.  Many other syntactic forms, such as set comprehension, require
+special treatment.
+\section{Parse translations *}
+\index{parse translation|(}
+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 production.  In many
+cases this scheme is not powerful enough, especially for constructs involving
+variable bindings.  Therefore the $ML$-section of a theory definition can
+associate constant names with user-defined translation functions by including
+a line
+val parse_translation = \dots
+where the right-hand side of this binding must be an \ML-expression of type
+\verb$(string * (term list -> term))list$.
+After the input string has been translated into a term according to the
+syntax definition, there is a second phase in which the term is translated
+using the user-supplied functions in a bottom-up manner.  Given a list $tab$
+of the above type, a term $t$ is translated as follows.  If $t$ is not of the
+form {\tt Const($c$,$\tau$)\$$t@1$\$\dots\$$t@n$}, then $t$ is returned
+unchanged.  Otherwise all $t@i$ are translated into $t@i'$.  Let {\tt $t' =$
+  Const($c$,$\tau$)\$$t@1'$\$\dots\$$t@n'$}.  If there is no pair $(c,f)$ in
+$tab$, return $t'$.  Otherwise apply $f$ to $[t@1',\dots,t@n']$.  If that
+raises an exception, return $t'$, otherwise return the result.
+\ML-lists are constructed by {\tt[]} and {\tt::}.  For readability the
+list \hbox{\tt$x$::$y$::$z$::[]} can be written \hbox{\tt[$x$,$y$,$z$]}.
+In Isabelle the two forms of lists are declared as follows:
+types list 1
+      enum 0
+arities list :: (term)term
+consts "[]" :: "'a list"                   ("[]")
+       ":"  :: "['a, 'a list] => 'a list"  (infixr 50)
+       enum :: "enum => 'a list"           ("[_]")
+       sing :: "'a => enum"                ("_")
+       cons :: "['a,enum] => enum"         ("_, _")
+Because \verb$::$ is already used for type constraints, it is replaced by
+\verb$:$ as the infix list constructor.
+In order to allow list enumeration, the new type {\tt enum} is introduced.
+Its only purpose is syntactic and hence it does not need an arity, in
+contrast to the logical type {\tt list}.  Although \hbox{\tt[$x$,$y$,$z$]} is
+syntactically legal, it needs to be translated into a term built up from
+\verb$[]$ and \verb$:$.  This is what \verb$make_list$ accomplishes:
+val cons = Const("op :", dummyT);
+fun make_list (Const("sing",_)$e) = cons $ e $ Const("[]", dummyT)
+  | make_list (Const("cons",_)$e$es) = cons $ e $ make_list es;
+To hook this translation up to Isabelle's parser, the theory definition needs
+to contain the following $ML$-section:
+fun enum_tr[enum] = make_list enum;
+val parse_translation = [("enum",enum_tr)]
+This causes \verb!Const("enum",_)$!$t$ to be replaced by
+Of course the definition of \verb$make_list$ should be included in the
+  Isabelle represents the set $\{ x \mid P(x) \}$ internally by $Set(\lambda
+  x.P(x))$.  The internal and external forms need separate
+constants:\footnote{In practice, the external form typically has a name
+beginning with an {\at} sign, such as {\tt {\at}SET}.  This emphasizes that
+the constant should be used only for parsing/printing.}
+types set 1
+arities set :: (term)term
+consts Set :: "('a => o) => 'a set"
+       SET :: "[id,o] => 'a set"  ("\{_ | _\}")
+Parsing {\tt"\{$x$ | $P$\}"} according to this syntax yields the term {\tt
+  Const("SET",dummyT) \$ Free("\(x\)",dummyT) \$ \(p\)}, where $p$ is the
+result of parsing $P$.  What we need is the term {\tt
+  Const("Set",dummyT)\$Abs("$x$",dummyT,$p'$)}, where $p'$ is some
+``abstracted'' version of $p$.  Therefore we define a function
+fun set_tr[Free(s,T), p] = Const("Set", dummyT) $
+                           Abs(s, T, abstract_over(Free(s,T), p));
+where \verb$abstract_over: term*term -> term$ is a predefined function such
+that {\tt abstract_over($u$,$t$)} replaces every occurrence of $u$ in $t$ by
+a {\tt Bound} variable of the correct index (i.e.\ 0 at top level).  Remember
+that {\tt dummyT} is replaced by the correct types at a later stage (see
+\S\ref{Typing}).  Function {\tt set_tr} is associated with {\tt SET} by
+including the \ML-text
+val parse_translation = [("SET", set_tr)];
+If you want to run the above examples in Isabelle, you should note that an
+$ML$-section needs to contain not just a definition of
+\verb$parse_translation$ but also of a variable \verb$print_translation$.  The
+purpose of the latter is to reverse the effect of the former during printing;
+details are found in \S\ref{Print-translations}.  Hence you need to include
+the line
+val print_translation = [];
+This is instructive because the terms are then printed out in their internal
+form.  For example the input \hbox{\tt[$x$,$y$,$z$]} is echoed as
+\hbox{\tt$x$:$y$:$z$:[]}.  This helps to check that your parse translation is
+working correctly.
+%Explicit type constraints disappear with type checking but are still
+%visible to the parse translation functions.
+\index{parse translation|)}
+Syntax definitions provide printing information in three distinct ways:
+\item the syntax of the language (as used for parsing),
+\item pretty printing information, and
+\item print translation functions.
+The bare mixfix declarations enable Isabelle to print terms, but the result
+will not necessarily be pretty and may look different from what you expected.
+To produce a pleasing layout, you need to read the following sections.
+\subsection{Printing with mixfix declarations}
+Let {\tt$t =$ Const($c$,_)\$$t@1$\$\dots\$$t@n$} be a term and let
+consts \(c\) :: \(\tau\) (\(sy\))
+be a mixfix declaration where $sy$ is of the form
+$\alpha@0\_\alpha@1\dots\alpha@{n-1}\_\alpha@n$.  Printing $t$ according to
+$sy$ means printing the string
+$\alpha@0\beta@1\alpha@1\ldots\alpha@{n-1}\beta@n\alpha@n$, where $\beta@i$
+is the result of printing $t@i$.
+Note that the system does {\em not\/} insert blanks.  They should be part of
+the mixfix syntax if they are required to separate tokens or achieve a
+certain layout.
+\subsection{Pretty printing}
+\index{pretty printing}
+In order to format the output, it is possible to embed pretty printing
+directives in mixfix annotations.  These directives are ignored during parsing
+and affect only printing.  The characters {\tt(}, {\tt)} and {\tt/} are
+interpreted as meta-characters\index{meta-character} when found in a mixfix
+annotation.  Their meaning is
+\item[~{\tt(}~] Open a block.  A sequence of digits following it is
+  interpreted as the \bfindex{indentation} of this block.  It causes the
+  output to be indented by $n$ positions if a line break occurs within the
+  block.  If {\tt(} is not followed by a digit, the indentation defaults to
+  $0$.
+\item[~{\tt)}~] Close a block.
+\item[~\ttindex{/}~] Allow a \bfindex{line break}.  White space immediately
+  following {\tt/} is not printed if the line is broken at this point.
+\subsection{Print translations *}
+\index{print translation|(}
+Since terms are translated after parsing (see \S\ref{Parse-translations}),
+there is a similar mechanism to translate them back before printing.
+Therefore the $ML$-section of a theory definition can associate constant
+names with user-defined translation functions by including a line
+val print_translation = \dots
+where the right-hand side of this binding is again an \ML-expression of type
+\verb$(string * (term list -> term))list$.
+Including a pair $(c,f)$ in this list causes the printer to print
+$f[t@1,\dots,t@n]$ whenever it finds {\tt Const($c$,_)\$$t@1$\$\dots\$$t@n$}.
+Reversing the effect of the parse translation in Example~\ref{list-enum} is
+accomplished by the following function:
+fun make_enum (Const("op :",_) $ e $ es) = case es of
+        Const("[]",_)  =>  Const("sing",dummyT) $ e
+      | _  =>  Const("enum",dummyT) $ e $ make_enum es;
+It translates \hbox{\tt$x$:$y$:$z$:[]} to \hbox{\tt[$x$,$y$,$z$]}.  However,
+if the input does not terminate with an empty list, e.g.\ \hbox{\tt$x$:$xs$},
+\verb$make_enum$ raises exception {\tt Match}.  This signals that the
+attempted translation has failed and the term should be printed as is.
+The connection with Isabelle's pretty printer is established as follows:
+fun enum_tr'[x,xs] = Const("enum",dummyT) $
+                     make_enum(Const("op :",dummyT)$x$xs);
+val print_translation = [("op :", enum_tr')];
+This declaration causes the printer to print \hbox{\tt enum_tr'[$x$,$y$]}
+whenever it finds \verb!Const("op :",_)$!$x$\verb!$!$y$.
+  In Example~\ref{SET} we showed how to translate the concrete syntax for set
+  comprehension into the proper internal form.  The string {\tt"\{$x$ |
+    $P$\}"} now becomes {\tt Const("Set",_)\$Abs("$x$",_,$p$)}.  If, however,
+  the latter term were printed without translating it back, it would result
+  in {\tt"Set(\%$x$.$P$)"}.  Therefore the abstraction has to be turned back
+  into a term that matches the concrete mixfix syntax:
+fun set_tr'[Abs(x,T,P)] =
+      let val (x',P') = variant_abs(x,T,P)
+      in Const("SET",dummyT) $ Free(x',T) $ P' end;
+The function \verb$variant_abs$, a basic term manipulation function, replaces
+the bound variable $x$ by a {\tt Free} variable $x'$ having a unique name.  A
+term produced by {\tt set_tr'} can now be printed according to the concrete
+syntax defined in Example~\ref{SET} above.
+Notice that the application of {\tt set_tr'} fails if the second component of
+the argument is not an abstraction, but for example just a {\tt Free}
+variable.  This is intentional because it signals to the caller that the
+translation is inapplicable.  As a result {\tt Const("Set",_)\$Free("P",_)}
+prints as {\tt"Set(P)"}.
+The full theory extension, including concrete syntax and both translation
+functions, has the following form:
+types set 1
+arities set :: (term)term
+consts Set :: "('a => o) => 'a set"
+       SET :: "[id,o] => 'a set"  ("\{_ | _\}")
+fun set_tr[Free(s,T), p] = \dots;
+val parse_translation = [("SET", set_tr)];
+fun set_tr'[Abs(x,T,P)] = \dots;
+val print_translation = [("Set", set_tr')];
+As during the parse translation process, the types attached to constants
+during print translation are ignored.  Thus {\tt Const("SET",dummyT)} in
+{\tt set_tr'} above is acceptable.  The types of {\tt Free}s and {\tt Var}s
+however must be preserved because they may get printed (see {\tt
+\index{print translation|)}
+\subsection{Printing a term}
+Let $tab$ be the set of all string-function pairs of print translations in the
+current syntax.
+Terms are printed recursively; print translations are applied top down:
+\item {\tt Free($x$,_)} is printed as $x$.
+\item {\tt Var(($x$,$i$),_)} is printed as $x$, if $i = 0$ and $x$ does not
+  end with a digit, as $x$ followed by $i$, if $i \neq 0$ and $x$ does not
+  end with a digit, and as {\tt $x$.$i$}, if $x$ ends with a digit.  Thus the
+  following cases can arise:
+\verb$Var(("v",0),_)$ & \verb$Var(("v",7),_)$ & \verb$Var(("v5",0),_)$ \\
+"?v" & "?v7" & "?v5.0"
+\item {\tt Abs($x@1$,_,Abs($x@2$,_,\dots Abs($x@n$,_,$p$)\dots))}, where $p$
+  is not an abstraction, is printed as {\tt \%$y@1\dots y@n$.$P$}, where $P$
+  is the result of printing $p$, and the $x@i$ are replaced by $y@i$.  The
+  latter are (possibly new) unique names.
+\item {\tt Bound($i$)} is printed as {\tt B.$i$} \footnote{The occurrence of
+    such ``loose'' bound variables indicates that either you are trying to
+    print a subterm of an abstraction, or there is something wrong with your
+    print translations.}.
+\item The application {\tt$t =$ Const($c$,_)\$$t@1$\$\dots\$$t@n$} (where
+  $n$ may be $0$!) is printed as follows:
+  If there is a pair $(c,f)$ in $tab$, print $f[t@1,\dots,t@n]$.  If this
+  application raises exception {\tt Match} or there is no pair $(c,f)$ in
+  $tab$, let $sy$ be the mixfix annotation associated with $c$.  If there is
+  no such $sy$, or if $sy$ does not have exactly $n$ argument positions, $t$
+  is printed as an application; otherwise $t$ is printed according to $sy$.
+  All other applications are printed as applications.
+Printing a term {\tt $c$\$$t@1$\$\dots\$$t@n$} as an application means
+printing it as {\tt $s$($s@1$,\dots,$s@n$)}, where $s@i$ is the result of
+printing $t@i$.  If $c$ is a {\tt Const}, $s$ is its first argument;
+otherwise $s$ is the result of printing $c$ as described above.
+The printer also inserts parentheses where they are necessary for reasons
+of precedence.
+\section{Identifiers, constants, and type inference *}
+There is one final step in the translation from strings to terms that we have
+not covered yet.  It explains how constants are distinguished from {\tt Free}s
+and how {\tt Free}s and {\tt Var}s are typed.  Both issues arise because {\tt
+  Free}s and {\tt Var}s are not declared.
+An identifier $f$ that does not appear as a delimiter in the concrete syntax
+can be either a free variable or a constant.  Since the parser knows only
+about those constants which appear in mixfix annotations, it parses $f$ as
+{\tt Free("$f$",dummyT)}, where \ttindex{dummyT} is the predefined dummy {\tt
+  typ}.  Although the parser produces these very raw terms, most user
+interface level functions like {\tt goal} type terms according to the given
+theory, say $T$.  In a first step, every occurrence of {\tt Free($f$,_)} or
+{\tt Const($f$,_)} is replaced by {\tt Const($f$,$\tau$)}, provided there is
+a constant $f$ of {\tt typ} $\tau$ in $T$.  This means that identifiers are
+treated as {\tt Free}s iff they are not declared in the theory.  The types of
+the remaining {\tt Free}s (and {\tt Var}s) are inferred as in \ML.  Type
+constraints can be used to remove ambiguities.
+One peculiarity of the current type inference algorithm is that variables
+with the same name must have the same type, irrespective of whether they are
+schematic, free or bound.  For example, take the first-order formula $f(x) = x
+\land (\forall f.~ f=f)$ where ${=} :: [\alpha{::}term,\alpha]\To o$ and
+$\forall :: (\alpha{::}term\To o)\To o$.  The first conjunct forces
+$x::\alpha{::}term$ and $f::\alpha\To\alpha$, the second one
+$f::\beta{::}term$.  Although the two $f$'s are distinct, they are required to
+have the same type.  Unifying $\alpha\To\alpha$ and $\beta{::}term$ fails
+because, in first-order logic, function types are not in class $term$.
+\section{Putting it all together}
+Having discussed the individual building blocks of a logic definition, it
+remains to be shown how they fit together.  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{MetaLogicSyntax}),
+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 ~=~ form.  \]
+More precisely, you need a coercion from formulae to propositions:
+Base = Pure +
+types o 0
+arities o :: logic
+consts Trueprop :: "o => prop"  ("_"  5)
+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:
+Hilbert = Base +
+consts "-->" :: "[o,o] => o"  (infixr 10)
+K   "P --> Q --> P"
+S   "(P --> Q --> R) --> (P --> Q) --> P --> R"
+MP  "[| P --> Q; P |] ==> Q"
+After loading this definition you can start to prove theorems in this logic:
+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!}
+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:
+MinI = Base +
+consts "-->" :: "[o,o] => o"  (infixr 10)
+impI  "(P ==> Q) ==> P --> Q"
+impE  "[| P --> Q; P |] ==> Q"
+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 \verb$MinI$
+(exercise!), but {\tt impI} cannot be derived in \verb!Hilbert!.  The reason
+is that {\tt impI} is only an {\em admissible} rule in \verb!Hilbert!,
+something that can only be shown by induction over all possible proofs in
+It is a very simple matter to extend minimal logic with falsity:
+MinIF = MinI +
+consts False :: "o"
+FalseE  "False ==> P"
+On the other hand, we may wish to introduce conjunction only:
+MinC = Base +
+consts "&" :: "[o,o] => o"  (infixr 30)
+conjI  "[| P; Q |] ==> P & Q"
+conjE1 "P & Q ==> P"
+conjE2 "P & Q ==> Q"
+And if we want to have all three connectives together, we define:
+MinIFC = MinIF + MinC
+Now we can prove mixed theorems like
+goal MinIFC.thy "P & False --> Q";
+by (resolve_tac [MinI.impI] 1);
+by (dresolve_tac [MinC.conjE2] 1);
+by (eresolve_tac [MinIF.FalseE] 1);
+Try this as an exercise!