--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Ref/defining.tex Fri Apr 15 16:37:59 1994 +0200
@@ -0,0 +1,772 @@
+%% $Id$
+\chapter{Defining Logics} \label{Defining-Logics}
+This chapter explains how to define new formal systems --- in particular,
+their concrete syntax. While Isabelle can be regarded as a theorem prover
+for set theory, higher-order logic or the sequent calculus, its
+distinguishing feature is support for the definition of new logics.
+
+Isabelle logics are hierarchies of theories, which are described and
+illustrated in
+\iflabelundefined{sec:defining-theories}{{\em Introduction to Isabelle}}%
+{\S\ref{sec:defining-theories}}. That material, together with the theory
+files provided in the examples directories, should suffice for all simple
+applications. The easiest way to define a new theory is by modifying a
+copy of an existing theory.
+
+This chapter documents the meta-logic syntax, mixfix declarations and
+pretty printing. The extended examples in \S\ref{sec:min_logics}
+demonstrate the logical aspects of the definition of theories.
+
+
+\section{Priority grammars} \label{sec:priority_grammars}
+\index{priority grammars|(}
+
+A context-free grammar contains a set of {\bf nonterminal symbols}, a set of
+{\bf terminal symbols} and a set of {\bf productions}\index{productions}.
+Productions have the form ${A=\gamma}$, where $A$ is a nonterminal and
+$\gamma$ is a string of terminals and nonterminals. One designated
+nonterminal is called the {\bf start symbol}. The language defined by the
+grammar consists of all strings of terminals that can be derived from the
+start symbol by applying productions as rewrite rules.
+
+The syntax of an Isabelle logic is specified by a {\bf priority
+ grammar}.\index{priorities} Each nonterminal is decorated by an integer
+priority, as in~$A^{(p)}$. A nonterminal $A^{(p)}$ in a derivation may be
+rewritten using a production $A^{(q)} = \gamma$ only if~$p \le q$. Any
+priority grammar can be translated into a normal context free grammar by
+introducing new nonterminals and productions.
+
+Formally, a set of context free productions $G$ induces a derivation
+relation $\longrightarrow@G$. Let $\alpha$ and $\beta$ denote strings of
+terminal or nonterminal symbols. Then
+\[ \alpha\, A^{(p)}\, \beta ~\longrightarrow@G~ \alpha\,\gamma\,\beta \]
+if and only if $G$ contains some production $A^{(q)}=\gamma$ for~$p \le q$.
+
+The following simple grammar for arithmetic expressions demonstrates how
+binding power and associativity of operators can be enforced by priorities.
+\begin{center}
+\begin{tabular}{rclr}
+ $A^{(9)}$ & = & {\tt0} \\
+ $A^{(9)}$ & = & {\tt(} $A^{(0)}$ {\tt)} \\
+ $A^{(0)}$ & = & $A^{(0)}$ {\tt+} $A^{(1)}$ \\
+ $A^{(2)}$ & = & $A^{(3)}$ {\tt*} $A^{(2)}$ \\
+ $A^{(3)}$ & = & {\tt-} $A^{(3)}$
+\end{tabular}
+\end{center}
+The choice of priorities determines that {\tt -} binds tighter than {\tt *},
+which binds tighter than {\tt +}. Furthermore {\tt +} associates to the
+left and {\tt *} to the right.
+
+For clarity, grammars obey these conventions:
+\begin{itemize}
+\item All priorities must lie between~0 and \ttindex{max_pri}, which is a
+ some fixed integer. Sometimes {\tt max_pri} is written as $\infty$.
+\item Priority 0 on the right-hand side and priority \ttindex{max_pri} on
+ the left-hand side may be omitted.
+\item The production $A^{(p)} = \alpha$ is written as $A = \alpha~(p)$; the
+ priority of the left-hand side actually appears in a column on the far
+ right.
+\item Alternatives are separated by~$|$.
+\item Repetition is indicated by dots~(\dots) in an informal but obvious
+ way.
+\end{itemize}
+
+Using these conventions and assuming $\infty=9$, the grammar
+takes the form
+\begin{center}
+\begin{tabular}{rclc}
+$A$ & = & {\tt0} & \hspace*{4em} \\
+ & $|$ & {\tt(} $A$ {\tt)} \\
+ & $|$ & $A$ {\tt+} $A^{(1)}$ & (0) \\
+ & $|$ & $A^{(3)}$ {\tt*} $A^{(2)}$ & (2) \\
+ & $|$ & {\tt-} $A^{(3)}$ & (3)
+\end{tabular}
+\end{center}
+\index{priority grammars|)}
+
+
+\begin{figure}
+\begin{center}
+\begin{tabular}{rclc}
+$prop$ &=& {\tt PROP} $aprop$ ~~$|$~~ {\tt(} $prop$ {\tt)} \\
+ &$|$& $logic^{(3)}$ {\tt ==} $logic^{(2)}$ & (2) \\
+ &$|$& $logic^{(3)}$ {\tt =?=} $logic^{(2)}$ & (2) \\
+ &$|$& $prop^{(2)}$ {\tt ==>} $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^{(\infty)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\\\
+$fun$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $fun$ {\tt)} \\
+ &$|$& $fun^{(\infty)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\
+ &$|$& $fun^{(\infty)}$ {\tt::} $type$ \\
+ &$|$& {\tt \%} $idts$ {\tt.} $logic$ & (0) \\\\
+$idts$ &=& $idt$ ~~$|$~~ $idt^{(1)}$ $idts$ \\\\
+$idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\
+ &$|$& $id$ {\tt ::} $type$ & (0) \\\\
+$type$ &=& $tid$ ~~$|$~~ $tvar$ ~~$|$~~ $tid$ {\tt::} $sort$
+ ~~$|$~~ $tvar$ {\tt::} $sort$ \\
+ &$|$& $id$ ~~$|$~~ $type^{(\infty)}$ $id$
+ ~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $id$ \\
+ &$|$& $type^{(1)}$ {\tt =>} $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{*PROP symbol}
+\index{*== symbol}\index{*=?= symbol}\index{*==> symbol}
+\index{*:: symbol}\index{*=> symbol}
+%index command: percent is permitted, but braces must match!
+\index{%@{\tt\%} symbol}
+\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}
+\index{*[ symbol}\index{*] symbol}
+\index{*"!"! symbol}
+\index{*"["| symbol}
+\index{*"|"] symbol}
+\end{center}
+\caption{Meta-logic syntax}\label{fig:pure_gram}
+\end{figure}
+
+
+\section{The Pure syntax} \label{sec:basic_syntax}
+\index{syntax!Pure|(}
+
+At the root of all object-logics lies the theory \thydx{Pure}. It
+contains, among many other things, the Pure syntax. An informal account of
+this basic syntax (types, terms and formulae) appears in
+\iflabelundefined{sec:forward}{{\em Introduction to Isabelle}}%
+{\S\ref{sec:forward}}. A more precise description using a priority grammar
+appears in Fig.\ts\ref{fig:pure_gram}. It defines the following
+nonterminals:
+\begin{ttdescription}
+\item[\ndxbold{prop}] denotes terms of type {\tt prop}. These are formulae
+ of the meta-logic.
+
+\item[\ndxbold{aprop}] denotes atomic propositions. These typically
+ include the judgement forms of the object-logic; its definition
+ introduces a meta-level predicate for each judgement form.
+
+\item[\ndxbold{logic}] denotes terms whose type belongs to class
+ \cldx{logic}. As the syntax is extended by new object-logics, more
+ productions for {\tt logic} are added automatically (see below).
+
+ \item[\ndxbold{fun}] denotes terms potentially of function type.
+
+ \item[\ndxbold{type}] denotes types of the meta-logic.
+
+ \item[\ndxbold{idts}] denotes a list of identifiers, possibly constrained
+ by types.
+\end{ttdescription}
+
+\begin{warn}
+ In {\tt idts}, note that \verb|x::nat y| is parsed as \verb|x::(nat y)|,
+ treating {\tt y} like a type constructor applied to {\tt nat}. The
+ likely result is an error message. To avoid this interpretation, use
+ parentheses and write \verb|(x::nat) y|.
+
+ Similarly, \verb|x::nat y::nat| is parsed as \verb|x::(nat y::nat)| and
+ yields an error. The correct form is \verb|(x::nat) (y::nat)|.
+\end{warn}
+
+\subsection{Logical types and default syntax}\label{logical-types}
+\index{lambda calc@$\lambda$-calculus}
+
+Isabelle's representation of mathematical languages is based on the simply
+typed $\lambda$-calculus. All logical types, namely those of class
+\cldx{logic}, are automatically equipped with a basic syntax of types,
+identifiers, variables, parentheses, $\lambda$-abstractions and
+applications.
+
+More precisely, for each type constructor $ty$ with arity $(\vec{s})c$,
+where $c$ is a subclass of \cldx{logic}, several productions are added:
+\begin{center}
+\begin{tabular}{rclc}
+$ty$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $ty$ {\tt)} \\
+ &$|$& $fun^{(\infty)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)}\\
+ &$|$& $ty^{(\infty)}$ {\tt::} $type$\\\\
+$logic$ &=& $ty$
+\end{tabular}
+\end{center}
+
+
+\subsection{Lexical matters}
+The parser does not process input strings directly. It operates on token
+lists provided by Isabelle's \bfindex{lexer}. There are two kinds of
+tokens: \bfindex{delimiters} and \bfindex{name tokens}.
+
+\index{reserved words}
+Delimiters can be regarded as reserved words of the syntax. You can
+add new ones when extending theories. In Fig.\ts\ref{fig:pure_gram} they
+appear in typewriter font, for example {\tt ==}, {\tt =?=} and
+{\tt PROP}\@.
+
+Name tokens have a predefined syntax. The lexer distinguishes four
+disjoint classes of names: \rmindex{identifiers}, \rmindex{unknowns}, type
+identifiers\index{type identifiers}, type unknowns\index{type unknowns}.
+They are denoted by \ndxbold{id}, \ndxbold{var}, \ndxbold{tid},
+\ndxbold{tvar}, respectively. Typical examples are {\tt x}, {\tt ?x7},
+{\tt 'a}, {\tt ?'a3}. Here is the precise syntax:
+\begin{eqnarray*}
+id & = & letter~quasiletter^* \\
+var & = & \mbox{\tt ?}id ~~|~~ \mbox{\tt ?}id\mbox{\tt .}nat \\
+tid & = & \mbox{\tt '}id \\
+tvar & = & \mbox{\tt ?}tid ~~|~~
+ \mbox{\tt ?}tid\mbox{\tt .}nat \\[1ex]
+letter & = & \mbox{one of {\tt a}\dots {\tt z} {\tt A}\dots {\tt Z}} \\
+digit & = & \mbox{one of {\tt 0}\dots {\tt 9}} \\
+quasiletter & = & letter ~~|~~ digit ~~|~~ \mbox{\tt _} ~~|~~ \mbox{\tt '} \\
+nat & = & digit^+
+\end{eqnarray*}
+A \ndxbold{var} or \ndxbold{tvar} describes an unknown, which is internally
+a pair of base name and index (\ML\ type \mltydx{indexname}). These
+components are either separated by a dot as in {\tt ?x.1} or {\tt ?x7.3} or
+run together as in {\tt ?x1}. The latter form is possible if the base name
+does not end with digits. If the index is 0, it may be dropped altogether:
+{\tt ?x} abbreviates both {\tt ?x0} and {\tt ?x.0}.
+
+The lexer repeatedly takes the maximal prefix of the input string that
+forms a valid token. A maximal prefix that is both a delimiter and a name
+is treated as a delimiter. Spaces, tabs and newlines are separators; they
+never occur within tokens.
+
+Delimiters need not be separated by white space. For example, if {\tt -}
+is a delimiter but {\tt --} is not, then the string {\tt --} is treated as
+two consecutive occurrences of the token~{\tt -}. In contrast, \ML\
+treats {\tt --} as a single symbolic name. The consequence of Isabelle's
+more liberal scheme is that the same string may be parsed in different ways
+after extending the syntax: after adding {\tt --} as a delimiter, the input
+{\tt --} is treated as a single token.
+
+Although name tokens are returned from the lexer rather than the parser, it
+is more logical to regard them as nonterminals. Delimiters, however, are
+terminals; they are just syntactic sugar and contribute nothing to the
+abstract syntax tree.
+
+
+\subsection{*Inspecting the syntax}
+\begin{ttbox}
+syn_of : theory -> Syntax.syntax
+Syntax.print_syntax : Syntax.syntax -> unit
+Syntax.print_gram : Syntax.syntax -> unit
+Syntax.print_trans : Syntax.syntax -> unit
+\end{ttbox}
+The abstract type \mltydx{Syntax.syntax} allows manipulation of syntaxes
+in \ML. You can display values of this type by calling the following
+functions:
+\begin{ttdescription}
+\item[\ttindexbold{syn_of} {\it thy}] returns the syntax of the Isabelle
+ theory~{\it thy} as an \ML\ value.
+
+\item[\ttindexbold{Syntax.print_syntax} {\it syn}] shows virtually all
+ information contained in the syntax {\it syn}. The displayed output can
+ be large. The following two functions are more selective.
+
+\item[\ttindexbold{Syntax.print_gram} {\it syn}] shows the grammar part
+ of~{\it syn}, namely the lexicon, roots and productions. These are
+ discussed below.
+
+\item[\ttindexbold{Syntax.print_trans} {\it syn}] shows the translation
+ part of~{\it syn}, namely the constants, parse/print macros and
+ parse/print translations.
+\end{ttdescription}
+
+Let us demonstrate these functions by inspecting Pure's syntax. Even that
+is too verbose to display in full.
+\begin{ttbox}\index{*Pure theory}
+Syntax.print_syntax (syn_of Pure.thy);
+{\out lexicon: "!!" "\%" "(" ")" "," "." "::" ";" "==" "==>" \dots}
+{\out roots: logic type fun prop}
+{\out prods:}
+{\out type = tid (1000)}
+{\out type = tvar (1000)}
+{\out type = id (1000)}
+{\out type = tid "::" sort[0] => "_ofsort" (1000)}
+{\out type = tvar "::" sort[0] => "_ofsort" (1000)}
+{\out \vdots}
+\ttbreak
+{\out consts: "_K" "_appl" "_aprop" "_args" "_asms" "_bigimpl" \dots}
+{\out parse_ast_translation: "_appl" "_bigimpl" "_bracket"}
+{\out "_idtyp" "_lambda" "_tapp" "_tappl"}
+{\out parse_rules:}
+{\out parse_translation: "!!" "_K" "_abs" "_aprop"}
+{\out print_translation: "all"}
+{\out print_rules:}
+{\out print_ast_translation: "==>" "_abs" "_idts" "fun"}
+\end{ttbox}
+
+As you can see, the output is divided into labeled sections. The grammar
+is represented by {\tt lexicon}, {\tt roots} and {\tt prods}. The rest
+refers to syntactic translations and macro expansion. Here is an
+explanation of the various sections.
+\begin{description}
+ \item[{\tt lexicon}] lists the delimiters used for lexical
+ analysis.\index{delimiters}
+
+ \item[{\tt roots}] lists the grammar's nonterminal symbols. You must
+ name the desired root when calling lower level functions or specifying
+ macros. Higher level functions usually expect a type and derive the
+ actual root as described in~\S\ref{sec:grammar}.
+
+ \item[{\tt prods}] lists the \rmindex{productions} of the priority grammar.
+ The nonterminal $A^{(n)}$ is rendered in {\sc ascii} as {\tt $A$[$n$]}.
+ Each delimiter is quoted. Some productions are shown with {\tt =>} and
+ an attached string. These strings later become the heads of parse
+ trees; they also play a vital role when terms are printed (see
+ \S\ref{sec:asts}).
+
+ Productions with no strings attached are called {\bf copy
+ productions}\indexbold{productions!copy}. Their right-hand side must
+ have exactly one nonterminal symbol (or name token). The parser does
+ not create a new parse tree node for copy productions, but simply
+ returns the parse tree of the right-hand symbol.
+
+ If the right-hand side consists of a single nonterminal with no
+ delimiters, then the copy production is called a {\bf chain
+ production}. Chain productions act as abbreviations:
+ conceptually, they are removed from the grammar by adding new
+ productions. Priority information attached to chain productions is
+ ignored; only the dummy value $-1$ is displayed.
+
+ \item[{\tt consts}, {\tt parse_rules}, {\tt print_rules}]
+ relate to macros (see \S\ref{sec:macros}).
+
+ \item[{\tt parse_ast_translation}, {\tt print_ast_translation}]
+ list sets of constants that invoke translation functions for abstract
+ syntax trees. Section \S\ref{sec:asts} below discusses this obscure
+ matter.\index{constants!for translations}
+
+ \item[{\tt parse_translation}, {\tt print_translation}] list sets
+ of constants that invoke translation functions for terms (see
+ \S\ref{sec:tr_funs}).
+\end{description}
+\index{syntax!Pure|)}
+
+
+\section{Mixfix declarations} \label{sec:mixfix}
+\index{mixfix declarations|(}
+
+When defining a theory, you declare new constants by giving their names,
+their type, and an optional {\bf mixfix annotation}. Mixfix annotations
+allow you to extend Isabelle's basic $\lambda$-calculus syntax with
+readable notation. They can express any context-free priority grammar.
+Isabelle syntax definitions are inspired by \OBJ~\cite{OBJ}; they are more
+general than the priority declarations of \ML\ and Prolog.
+
+A mixfix annotation defines a production of the priority grammar. It
+describes the concrete syntax, the translation to abstract syntax, and the
+pretty printing. Special case annotations provide a simple means of
+specifying infix operators, binders and so forth.
+
+\subsection{Grammar productions}\label{sec:grammar}\index{productions}
+
+Let us examine the treatment of the production
+\[ A^{(p)}= w@0\, A@1^{(p@1)}\, w@1\, A@2^{(p@2)}\, \ldots\,
+ A@n^{(p@n)}\, w@n. \]
+Here $A@i^{(p@i)}$ is a nonterminal with priority~$p@i$ for $i=1$,
+\ldots,~$n$, while $w@0$, \ldots,~$w@n$ are strings of terminals.
+In the corresponding mixfix annotation, the priorities are given separately
+as $[p@1,\ldots,p@n]$ and~$p$. The nonterminal symbols are identified with
+types~$\tau$, $\tau@1$, \ldots,~$\tau@n$ respectively, and the production's
+effect on nonterminals is expressed as the function type
+\[ [\tau@1, \ldots, \tau@n]\To \tau. \]
+Finally, the template
+\[ w@0 \;_\; w@1 \;_\; \ldots \;_\; w@n \]
+describes the strings of terminals.
+
+A simple type is typically declared for each nonterminal symbol. In
+first-order logic, type~$i$ stands for terms and~$o$ for formulae. Only
+the outermost type constructor is taken into account. For example, any
+type of the form $\sigma list$ stands for a list; productions may refer
+to the symbol {\tt list} and will apply lists of any type.
+
+The symbol associated with a type is called its {\bf root} since it may
+serve as the root of a parse tree. Precisely, the root of $(\tau@1, \dots,
+\tau@n)ty$ is $ty$, where $\tau@1$, \ldots, $\tau@n$ are types and $ty$ is
+a type constructor. Type infixes are a special case of this; in
+particular, the root of $\tau@1 \To \tau@2$ is {\tt fun}. Finally, the
+root of a type variable is {\tt logic}; general productions might
+refer to this nonterminal.
+
+Identifying nonterminals with types allows a constant's type to specify
+syntax as well. We can declare the function~$f$ to have type $[\tau@1,
+\ldots, \tau@n]\To \tau$ and, through a mixfix annotation, specify the
+layout of the function's $n$ arguments. The constant's name, in this
+case~$f$, will also serve as the label in the abstract syntax tree. There
+are two exceptions to this treatment of constants:
+\begin{enumerate}\index{constants!syntactic}
+ \item A production need not map directly to a logical function. In this
+ case, you must declare a constant whose purpose is purely syntactic.
+ By convention such constants begin with the symbol~{\tt\at},
+ ensuring that they can never be written in formulae.
+
+ \item A copy production has no associated constant.\index{productions!copy}
+\end{enumerate}
+There is something artificial about this representation of productions,
+but it is convenient, particularly for simple theory extensions.
+
+\subsection{The general mixfix form}
+Here is a detailed account of mixfix declarations. Suppose the following
+line occurs within the {\tt consts} section of a {\tt .thy} file:
+\begin{center}
+ {\tt $c$ ::\ "$\sigma$" ("$template$" $ps$ $p$)}
+\end{center}
+This constant declaration and mixfix annotation is interpreted as follows:
+\begin{itemize}\index{productions}
+\item The string {\tt $c$} is the name of the constant associated with the
+ production; unless it is a valid identifier, it must be enclosed in
+ quotes. If $c$ is empty (given as~{\tt ""}) then this is a copy
+ production.\index{productions!copy} Otherwise, parsing an instance of the
+ phrase $template$ generates the \AST{} {\tt ("$c$" $a@1$ $\ldots$
+ $a@n$)}, where $a@i$ is the \AST{} generated by parsing the $i$-th
+ argument.
+
+ \item The constant $c$, if non-empty, is declared to have type $\sigma$.
+
+ \item The string $template$ specifies the right-hand side of
+ the production. It has the form
+ \[ w@0 \;_\; w@1 \;_\; \ldots \;_\; w@n, \]
+ where each occurrence of {\tt_} denotes an argument position and
+ the~$w@i$ do not contain~{\tt _}. (If you want a literal~{\tt _} in
+ the concrete syntax, you must escape it as described below.) The $w@i$
+ may consist of \rmindex{delimiters}, spaces or
+ \rmindex{pretty printing} annotations (see below).
+
+ \item The type $\sigma$ specifies the production's nonterminal symbols
+ (or name tokens). If $template$ is of the form above then $\sigma$
+ must be a function type with at least~$n$ argument positions, say
+ $\sigma = [\tau@1, \dots, \tau@n] \To \tau$. Nonterminal symbols are
+ derived from the types $\tau@1$, \ldots,~$\tau@n$, $\tau$ as described
+ above. Any of these may be function types; the corresponding root is
+ then \tydx{fun}.
+
+ \item The optional list~$ps$ may contain at most $n$ integers, say {\tt
+ [$p@1$, $\ldots$, $p@m$]}, where $p@i$ is the minimal
+ priority\indexbold{priorities} required of any phrase that may appear
+ as the $i$-th argument. Missing priorities default to~0.
+
+ \item The integer $p$ is the priority of this production. If omitted, it
+ defaults to the maximal priority.
+ Priorities range between 0 and \ttindexbold{max_pri} (= 1000).
+\end{itemize}
+%
+The declaration {\tt $c$ ::\ "$\sigma$" ("$template$")} specifies no
+priorities. The resulting production puts no priority constraints on any
+of its arguments and has maximal priority itself. Omitting priorities in
+this manner will introduce syntactic ambiguities unless the production's
+right-hand side is fully bracketed, as in \verb|"if _ then _ else _ fi"|.
+
+Omitting the mixfix annotation completely, as in {\tt $c$ ::\ "$\sigma$"},
+is sensible only if~$c$ is an identifier. Otherwise you will be unable to
+write terms involving~$c$.
+
+\begin{warn}
+ Theories must sometimes declare types for purely syntactic purposes. One
+ example is \tydx{type}, the built-in type of types. This is a `type of
+ all types' in the syntactic sense only. Do not declare such types under
+ {\tt arities} as belonging to class {\tt logic}\index{*logic class}, for
+ that would allow their use in arbitrary Isabelle
+ expressions~(\S\ref{logical-types}).
+\end{warn}
+
+\subsection{Example: arithmetic expressions}
+\index{examples!of mixfix declarations}
+This theory specification contains a {\tt consts} section with mixfix
+declarations encoding the priority grammar from
+\S\ref{sec:priority_grammars}:
+\begin{ttbox}
+EXP = Pure +
+types
+ exp
+arities
+ exp :: logic
+consts
+ "0" :: "exp" ("0" 9)
+ "+" :: "[exp, exp] => exp" ("_ + _" [0, 1] 0)
+ "*" :: "[exp, exp] => exp" ("_ * _" [3, 2] 2)
+ "-" :: "exp => exp" ("- _" [3] 3)
+end
+\end{ttbox}
+The {\tt arities} declaration causes {\tt exp} to be added as a new root.
+If you put this into a file {\tt exp.thy} and load it via {\tt
+ use_thy "EXP"}, you can run some tests:
+\begin{ttbox}
+val read_exp = Syntax.test_read (syn_of EXP.thy) "exp";
+{\out val it = fn : string -> unit}
+read_exp "0 * 0 * 0 * 0 + 0 + 0 + 0";
+{\out tokens: "0" "*" "0" "*" "0" "*" "0" "+" "0" "+" "0" "+" "0"}
+{\out raw: ("+" ("+" ("+" ("*" "0" ("*" "0" ("*" "0" "0"))) "0") "0") "0")}
+{\out \vdots}
+read_exp "0 + - 0 + 0";
+{\out tokens: "0" "+" "-" "0" "+" "0"}
+{\out raw: ("+" ("+" "0" ("-" "0")) "0")}
+{\out \vdots}
+\end{ttbox}
+The output of \ttindex{Syntax.test_read} includes the token list ({\tt
+ tokens}) and the raw \AST{} directly derived from the parse tree,
+ignoring parse \AST{} translations. The rest is tracing information
+provided by the macro expander (see \S\ref{sec:macros}).
+
+Executing {\tt Syntax.print_gram} reveals the productions derived
+from our mixfix declarations (lots of additional information deleted):
+\begin{ttbox}
+Syntax.print_gram (syn_of EXP.thy);
+{\out exp = "0" => "0" (9)}
+{\out exp = exp[0] "+" exp[1] => "+" (0)}
+{\out exp = exp[3] "*" exp[2] => "*" (2)}
+{\out exp = "-" exp[3] => "-" (3)}
+\end{ttbox}
+
+
+\subsection{The mixfix template}
+Let us take a closer look at the string $template$ appearing in mixfix
+annotations. This string specifies a list of parsing and printing
+directives: delimiters\index{delimiters}, arguments, spaces, blocks of
+indentation and line breaks. These are encoded by the following character
+sequences:
+\index{pretty printing|(}
+\begin{description}
+\item[~$d$~] is a delimiter, namely a non-empty sequence of characters
+ other than the special characters {\tt _}, {\tt(}, {\tt)} and~{\tt/}.
+ Even these characters may appear if escaped; this means preceding it with
+ a~{\tt '} (single quote). Thus you have to write {\tt ''} if you really
+ want a single quote. Delimiters may never contain spaces.
+
+\item[~{\tt_}~] is an argument position, which stands for a nonterminal symbol
+ or name token.
+
+\item[~$s$~] is a non-empty sequence of spaces for printing. This and the
+ following specifications do not affect parsing at all.
+
+\item[~{\tt(}$n$~] opens a pretty printing block. The optional number $n$
+ specifies how much indentation to add when a line break occurs within the
+ block. If {\tt(} is not followed by digits, the indentation defaults
+ to~0.
+
+\item[~{\tt)}~] closes a pretty printing block.
+
+\item[~{\tt//}~] forces a line break.
+
+\item[~{\tt/}$s$~] allows a line break. Here $s$ stands for the string of
+ spaces (zero or more) right after the {\tt /} character. These spaces
+ are printed if the break is not taken.
+\end{description}
+For example, the template {\tt"(_ +/ _)"} specifies an infix operator.
+There are two argument positions; the delimiter~{\tt+} is preceded by a
+space and followed by a space or line break; the entire phrase is a pretty
+printing block. Other examples appear in Fig.\ts\ref{fig:set_trans} below.
+Isabelle's pretty printer resembles the one described in
+Paulson~\cite{paulson91}.
+
+\index{pretty printing|)}
+
+
+\subsection{Infixes}
+\indexbold{infixes}
+
+Infix operators associating to the left or right can be declared
+using {\tt infixl} or {\tt infixr}.
+Roughly speaking, the form {\tt $c$ ::\ "$\sigma$" (infixl $p$)}
+abbreviates the constant declarations
+\begin{ttbox}
+"op \(c\)" :: "\(\sigma\)" ("op \(c\)")
+"op \(c\)" :: "\(\sigma\)" ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\))
+\end{ttbox}
+and {\tt $c$ ::\ "$\sigma$" (infixr $p$)} abbreviates the constant declarations
+\begin{ttbox}
+"op \(c\)" :: "\(\sigma\)" ("op \(c\)")
+"op \(c\)" :: "\(\sigma\)" ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\))
+\end{ttbox}
+The infix operator is declared as a constant with the prefix {\tt op}.
+Thus, prefixing infixes with \sdx{op} makes them behave like ordinary
+function symbols, as in \ML. Special characters occurring in~$c$ must be
+escaped, as in delimiters, using a single quote.
+
+The expanded forms above would be actually illegal in a {\tt .thy} file
+because they declare the constant \hbox{\tt"op \(c\)"} twice.
+
+
+\subsection{Binders}
+\indexbold{binders}
+\begingroup
+\def\Q{{\cal Q}}
+A {\bf binder} is a variable-binding construct such as a quantifier. The
+constant declaration
+\begin{ttbox}
+\(c\) :: "\(\sigma\)" (binder "\(\Q\)" \(p\))
+\end{ttbox}
+introduces a constant~$c$ of type~$\sigma$, which must have the form
+$(\tau@1 \To \tau@2) \To \tau@3$. Its concrete syntax is $\Q~x.P$, where
+$x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$
+and the whole term has type~$\tau@3$. Special characters in $\Q$ must be
+escaped using a single quote.
+
+The declaration is expanded internally to
+\begin{ttbox}
+\(c\) :: "(\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)"
+"\(\Q\)"\hskip-3pt :: "[idts, \(\tau@2\)] => \(\tau@3\)" ("(3\(\Q\)_./ _)" \(p\))
+\end{ttbox}
+Here \ndx{idts} is the nonterminal symbol for a list of identifiers with
+optional type constraints (see Fig.\ts\ref{fig:pure_gram}). The
+declaration also installs a parse translation\index{translations!parse}
+for~$\Q$ and a print translation\index{translations!print} for~$c$ to
+translate between the internal and external forms.
+
+A binder of type $(\sigma \To \tau) \To \tau$ can be nested by giving a
+list of variables. The external form $\Q~x@1~x@2 \ldots x@n. P$
+corresponds to the internal form
+\[ c(\lambda x@1. c(\lambda x@2. \ldots c(\lambda x@n. P) \ldots)). \]
+
+\medskip
+For example, let us declare the quantifier~$\forall$:\index{quantifiers}
+\begin{ttbox}
+All :: "('a => o) => o" (binder "ALL " 10)
+\end{ttbox}
+This lets us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL
+ $x$.$P$}. When printing, Isabelle prefers the latter form, but must fall
+back on ${\tt All}(P)$ if $P$ is not an abstraction. Both $P$ and {\tt ALL
+ $x$.$P$} have type~$o$, the type of formulae, while the bound variable
+can be polymorphic.
+\endgroup
+
+\index{mixfix declarations|)}
+
+
+\section{Example: some minimal logics} \label{sec:min_logics}
+\index{examples!of logic definitions}
+
+This section presents some examples that have a simple syntax. They
+demonstrate how to define new object-logics from scratch.
+
+First we must define how an object-logic syntax embedded into the
+meta-logic. Since all theorems must conform to the syntax for~\ndx{prop} (see
+Fig.\ts\ref{fig:pure_gram}), that syntax has to be extended with the
+object-level syntax. Assume that the syntax of your object-logic defines a
+nonterminal symbol~\ndx{o} of formulae. These formulae can now appear in
+axioms and theorems wherever \ndx{prop} does if you add the production
+\[ prop ~=~ o. \]
+This is not a copy production but a coercion from formulae to propositions:
+\begin{ttbox}
+Base = Pure +
+types
+ o
+arities
+ o :: logic
+consts
+ Trueprop :: "o => prop" ("_" 5)
+end
+\end{ttbox}
+The constant \cdx{Trueprop} (the name is arbitrary) acts as an invisible
+coercion function. Assuming this definition resides in a file {\tt base.thy},
+you have to load it with the command {\tt use_thy "Base"}.
+
+One of the simplest nontrivial logics is {\bf minimal logic} of
+implication. Its definition in Isabelle needs no advanced features but
+illustrates the overall mechanism nicely:
+\begin{ttbox}
+Hilbert = Base +
+consts
+ "-->" :: "[o, o] => o" (infixr 10)
+rules
+ K "P --> Q --> P"
+ S "(P --> Q --> R) --> (P --> Q) --> P --> R"
+ MP "[| P --> Q; P |] ==> Q"
+end
+\end{ttbox}
+After loading this definition from the file {\tt hilbert.thy}, you can
+start to prove theorems in the logic:
+\begin{ttbox}
+goal Hilbert.thy "P --> P";
+{\out Level 0}
+{\out P --> P}
+{\out 1. P --> P}
+\ttbreak
+by (resolve_tac [Hilbert.MP] 1);
+{\out Level 1}
+{\out P --> P}
+{\out 1. ?P --> P --> P}
+{\out 2. ?P}
+\ttbreak
+by (resolve_tac [Hilbert.MP] 1);
+{\out Level 2}
+{\out P --> P}
+{\out 1. ?P1 --> ?P --> P --> P}
+{\out 2. ?P1}
+{\out 3. ?P}
+\ttbreak
+by (resolve_tac [Hilbert.S] 1);
+{\out Level 3}
+{\out P --> P}
+{\out 1. P --> ?Q2 --> P}
+{\out 2. P --> ?Q2}
+\ttbreak
+by (resolve_tac [Hilbert.K] 1);
+{\out Level 4}
+{\out P --> P}
+{\out 1. P --> ?Q2}
+\ttbreak
+by (resolve_tac [Hilbert.K] 1);
+{\out Level 5}
+{\out P --> P}
+{\out No subgoals!}
+\end{ttbox}
+As we can see, this Hilbert-style formulation of minimal logic is easy to
+define but difficult to use. The following natural deduction formulation is
+better:
+\begin{ttbox}
+MinI = Base +
+consts
+ "-->" :: "[o, o] => o" (infixr 10)
+rules
+ impI "(P ==> Q) ==> P --> Q"
+ impE "[| P --> Q; P |] ==> Q"
+end
+\end{ttbox}
+Note, however, that although the two systems are equivalent, this fact
+cannot be proved within Isabelle. Axioms {\tt S} and {\tt K} can be
+derived in {\tt MinI} (exercise!), but {\tt impI} cannot be derived in {\tt
+ Hilbert}. The reason is that {\tt impI} is only an {\bf admissible} rule
+in {\tt Hilbert}, something that can only be shown by induction over all
+possible proofs in {\tt Hilbert}.
+
+We may easily extend minimal logic with falsity:
+\begin{ttbox}
+MinIF = MinI +
+consts
+ False :: "o"
+rules
+ FalseE "False ==> P"
+end
+\end{ttbox}
+On the other hand, we may wish to introduce conjunction only:
+\begin{ttbox}
+MinC = Base +
+consts
+ "&" :: "[o, o] => o" (infixr 30)
+\ttbreak
+rules
+ conjI "[| P; Q |] ==> P & Q"
+ conjE1 "P & Q ==> P"
+ conjE2 "P & Q ==> Q"
+end
+\end{ttbox}
+And if we want to have all three connectives together, we create and load a
+theory file consisting of a single line:\footnote{We can combine the
+ theories without creating a theory file using the ML declaration
+\begin{ttbox}
+val MinIFC_thy = merge_theories(MinIF,MinC)
+\end{ttbox}
+\index{*merge_theories|fnote}}
+\begin{ttbox}
+MinIFC = MinIF + MinC
+\end{ttbox}
+Now we can prove mixed theorems like
+\begin{ttbox}
+goal MinIFC.thy "P & False --> Q";
+by (resolve_tac [MinI.impI] 1);
+by (dresolve_tac [MinC.conjE2] 1);
+by (eresolve_tac [MinIF.FalseE] 1);
+\end{ttbox}
+Try this as an exercise!
+
+