\chapter{Defining Logics} \label{Defining-Logics}This chapter is intended for Isabelle experts. It explains how to define newlogical systems, Isabelle's {\it raison d'\^etre}. Isabelle logics arehierarchies of theories. A number of simple examples are contained in theintroductory manual; the full syntax of theory definitions is shown in the{\em Reference Manual}. The purpose of this chapter is to explain theremaining subtleties, especially some context conditions on the classstructure and the definition of new mixfix syntax. A full understanding ofthe material requires knowledge of the internal representation of terms (datatype {\tt term}) as detailed in the {\em Reference Manual}. Sections markedwith a * can be skipped on first reading.\section{Classes and Types *}\index{*arities!context conditions}Type declarations are subject to the following two well-formednessconditions:\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 1arities ty :: (\{logic\}) logic ty :: (\{\})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 oftypes represented by $s$. For example\begin{ttbox}classes term < logictypes ty 1arities ty :: (\{logic\})logic ty :: (\{\})term\end{ttbox}leads to an error message and fails.\end{itemize}These conditions guarantee principal types~\cite{nipkow-prehofer}.\section{Precedence Grammars}\label{PrecedenceGrammars}\index{precedence grammar|(}The precise syntax of a logic is best defined by a context-free grammar.These grammars obey the following conventions: identifiers denotenonterminals, {\tt typewriter} fount denotes terminals, repetition isindicated by \dots, and alternatives are separated by $|$.In order to simplify the description of mathematical languages, we introducean extended format which permits {\bf precedences}\index{precedence}. Thisscheme generalizes precedence declarations in \ML\ and {\sc prolog}. In thisextended grammar format, nonterminals are decorated by integers, theirprecedence. 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 aproduction $A@q = \gamma$ where $p \le q$.Formally, a set of context free productions $G$ induces a derivationrelation $\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 contextfree grammar. However, this translation may require the introduction of alarge number of new nonterminals and productions.\begin{example}\label{PrecedenceEx}The following simple grammar for arithmetic expressions demonstrates howbinding 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 \verb$-$ binds tighter than\verb$*$ which binds tighter than \verb$+$, and that \verb$+$ and \verb$*$associate to the left and right, respectively.\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)$.Using these conventions and assuming $max_pri=9$, the grammar inExample~\ref{PrecedenceEx} 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}\index{precedence grammar|)}\section{Basic syntax *}An informal account of most of Isabelle's syntax (meta-logic, types etc) iscontained in {\em Introduction to Isabelle}. A precise description using aprecedence grammar is shown in Figure~\ref{MetaLogicSyntax}. This descriptionis the basis of all extensions by object-logics.\begin{figure}[htb]\begin{center}\begin{tabular}{rclc}$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\}} \end{tabular}\index{*"!"!}\index{*"["|}\index{*"|"]}\indexbold{type@$type$}\indexbold{sort@$sort$}\indexbold{idts@$idts$}\indexbold{logic@$logic$}\indexbold{prop@$prop$}\indexbold{fun@$fun$}\end{center}\caption{Meta-Logic Syntax}\label{MetaLogicSyntax}\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 (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$.\end{description}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 withpredefined syntax, we may assume that all their productions have precedence$max_pri$.\subsection{Logical types and default syntax}Isabelle is concerned with mathematical languages which have a certainminimal vocabulary: identifiers, variables, parentheses, and the lambdacalculus. Logical types, i.e.\ those of class $logic$, are automaticallyequipped with this basic syntax. More precisely, for any type constructor$ty$ with arity $(\dots)c$, where $c$ is a subclass of $logic$, the followingproductions are added:\begin{center}\begin{tabular}{rclc}$ty$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $ty$ {\tt)} \\ &$|$& $fun@{max_pri}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)}\\ &$|$& $ty@{max_pri}$ {\tt::} $type$\\\\$logic$ &=& $ty$\end{tabular}\end{center}\section{Mixfix syntax}\index{mixfix|(}We distinguish between abstract and concrete syntax. The {\em abstract}syntax is given by the typed constants of a theory. Abstract syntax trees arewell-typed terms, i.e.\ values of \ML\ type {\tt term}. If none of theconstants are introduced with mixfix annotations, there is no concrete syntaxto 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 notationquickly becomes unreadable, Isabelle supports syntax definitions in the formof unrestricted context-free grammars using mixfix annotations.Mixfix annotations describe the {\em concrete} syntax, its translation intothe abstract syntax, and a pretty-printing scheme, all in one. Isabellesyntax definitions are inspired by \OBJ's~\cite{OBJ} {\em mixfix\/} syntax.Each mixfix annotation defines a precedence grammar production and associatesan Isabelle constant with it.A {\em mixfix declaration} {\tt consts $c$ ::\ $\tau$ ($sy$ $ps$ $p$)} isinterpreted as a grammar pro\-duction as follows:\begin{itemize}\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.\end{itemize}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, wesometimes refer to the nonterminals on the right-hand side of a production asits arguments and to the nonterminal on the left-hand side as its result.The maximal legal precedence is called \ttindexbold{max_pri}, which iscurrently 1000. If you want to ignore precedences, the safest way to do so isto use the annotation {\tt($sy$)}: this production puts no precedenceconstraints on any of its arguments and has maximal precedence itself, i.e.\ it is always applicable and does not exclude any productions of itsarguments.\begin{example}In mixfix notation the grammar in Example~\ref{PrecedenceEx} can be writtenas follows:\begin{ttbox}types exp 0consts "0" :: "exp" ("0" 9) "+" :: "[exp,exp] => exp" ("_ + _" [0,1] 0) "*" :: "[exp,exp] => exp" ("_ * _" [3,2] 2) "-" :: "exp => exp" ("- _" [3] 3)\end{ttbox}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)}.\end{example}The interpretation of \ttindex{_} in a mixfix annotation is always as a {\bf meta-character}\index{meta-character} which does not represent itself butan argument position. The following characters are also meta-characters:\begin{ttbox}' ( ) /\end{ttbox}Preceding any character with a quote (\verb$'$) turns it into an ordinarycharacter. 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 thefollowing function:\begin{eqnarray*}N(\tau@1\To\tau@2) &=& fun \\N((\tau@1,\dots,\tau@n)ty) &=& ty \\N(\alpha) &=& logic\end{eqnarray*}Only the outermost type constructor is taken into account and type variablescan 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\begin{ttbox}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\))\end{ttbox}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 arecalled {\bf copy productions}. They must have exactly one nonterminal onthe right hand side. The term generated when parsing that nonterminal issimply passed up as the result of parsing the whole copy production. InIsabelle a copy production is indicated by an empty constant name, i.e.\ by\begin{ttbox}consts "" :: \(\tau\) (\(sy\) \(ps\) \(p\))\end{ttbox}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 beseen as an abbreviation mechanism. Conceptually, they are removed from thegrammar by adding appropriate new rules. Precedence information attached tochain productions is ignored. The following example demonstrates the effect:the grammar defined by\begin{ttbox}types A,B,C 0consts AB :: "B => A" ("A _" [10] 517) "" :: "C => B" ("_" [0] 100) x :: "C" ("x" 5) y :: "C" ("y" 15)\end{ttbox}admits {\tt"A y"} but not {\tt"A x"}. Had the constant in the secondproduction been some non-empty string, both {\tt"A y"} and {\tt"A x"} wouldbe legal.\index{mixfix|)}\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 syntaxdefinition. If $\alpha@0\_\alpha@1\dots\alpha@{n-1}\_\alpha@n$ is a mixfixannotation, 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 adelimiter. Thus a delimiter can be an arbitrary string not containing whitespace.The lexical syntax of identifiers and variables ( = unknowns) is defined inthe 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 longestnumeric suffix of $v$ (possibly $0$), and $u$ is the remaining prefix.Parsing a variable {\tt?}$v{.}i$ generates {\tt Var(($v$,$i$),dummyT)}. Thefollowing table covers the four different cases that can arise:\begin{center}\tt\begin{tabular}{cccc}"?v" & "?v.7" & "?v5" & "?v7.5" \\Var(("v",0),$d$) & Var(("v",7),$d$) & Var(("v",5),$d$) & Var(("v7",5),$d$)\end{tabular}\end{center}where $d = {\tt dummyT}$.In mixfix annotations, \ttindexbold{id}, \ttindexbold{var},\ttindexbold{tfree} and \ttindexbold{tvar} are the predefined categories ofidentifiers, unknowns, type variables and type unknowns, respectively.The lexical analyzer translates input strings to token lists by repeatedlytaking the maximal prefix of the input string that forms a valid token. Amaximal 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 neednot be separated by white space to be recognized as separate. If \verb$"-"$is a delimiter but \verb$"--"$ is not, the string \verb$"--"$ is treated astwo consecutive occurrences of \verb$"-"$. This is in contrast to \ML\ whichwould treat \verb$"--"$ as a single (undeclared) identifier. Theconsequence of Isabelle's more liberal scheme is that the same string may beparsed in a different way after extending the syntax: after adding\verb$"--"$ as a delimiter, the input \verb$"--"$ is treated asa single occurrence of \verb$"--"$.\section{Infix operators}{\tt Infixl} and {\tt infixr} declare infix operators which associate to theleft and right respectively. As in \ML, prefixing infix operators with\ttindexbold{op} turns them into curried functions. Infix declarations canbe reduced to mixfix ones as follows:\begin{center}\tt\begin{tabular}{l@{~~$\Longrightarrow$~~}l}"$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$)\end{tabular}\end{center}\section{Binders}A {\bf binder} is a variable-binding constant, such as a quantifier.The declaration\begin{ttbox}consts \(c\) :: \(\tau\) (binder \(Q\) \(p\))\end{ttbox}\indexbold{*binder}introduces a binder $c$ of type $\tau$,which must have the form $(\tau@1\To\tau@2)\To\tau@3$. Its concrete syntaxis $Q~x.t$. A binder is like a generalized quantifier where $\tau@1$ is thetype 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 declaredlike this:\begin{ttbox}consts 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$)}; 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,\begin{ttbox}consts \(c\) :: "\((\tau@1\To\tau@2)\To\tau@3\)" (binder "\(Q\)" \(p\))\end{ttbox}is equivalent to\begin{ttbox}consts \(c\) :: "\((\tau@1\To\tau@2)\To\tau@3\)" "\(Q\)" :: "[idts,\(\tau@2\)] => \(\tau@3\)" ("\(Q\)_. _" \(p\))\end{ttbox}where {\tt idts} is the syntactic category $idts$ defined inFigure~\ref{MetaLogicSyntax}.However, there is more to binders than concrete syntax: behind the scenes thebody of the quantified expression has to be converted into a$\lambda$-abstraction (when parsing) and back again (when printing). Thisis performed by the translation mechanism, which is discussed below. Forbinders, the definition of the required translation functions has beenautomated. Many other syntactic forms, such as set comprehension, requirespecial treatment.\section{Parse translations *}\label{Parse-translations}\index{parse translation|(}So far we have pretended that there is a close enough relationship betweenconcrete and abstract syntax to allow an automatic translation from one tothe other using the constant name supplied with each production. In manycases this scheme is not powerful enough, especially for constructs involvingvariable bindings. Therefore the $ML$-section of a theory definition canassociate constant names with user-defined translation functions by includinga line\begin{ttbox}val parse_translation = \dots\end{ttbox}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 thesyntax definition, there is a second phase in which the term is translatedusing 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 theform {\tt Const($c$,$\tau$)\$$t@1$\$\dots\$$t@n$}, then $t$ is returnedunchanged. 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 thatraises an exception, return $t'$, otherwise return the result.\begin{example}\label{list-enum}\ML-lists are constructed by {\tt[]} and {\tt::}. For readability thelist \hbox{\tt$x$::$y$::$z$::[]} can be written \hbox{\tt[$x$,$y$,$z$]}.In Isabelle the two forms of lists are declared as follows:\begin{ttbox}types list 1 enum 0arities list :: (term)termconsts "[]" :: "'a list" ("[]") ":" :: "['a, 'a list] => 'a list" (infixr 50) enum :: "enum => 'a list" ("[_]") sing :: "'a => enum" ("_") cons :: "['a,enum] => enum" ("_, _")end\end{ttbox}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, incontrast to the logical type {\tt list}. Although \hbox{\tt[$x$,$y$,$z$]} issyntactically legal, it needs to be translated into a term built up from\verb$[]$ and \verb$:$. This is what \verb$make_list$ accomplishes:\begin{ttbox}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;\end{ttbox}To hook this translation up to Isabelle's parser, the theory definition needsto contain the following $ML$-section:\begin{ttbox}MLfun enum_tr[enum] = make_list enum;val parse_translation = [("enum",enum_tr)]\end{ttbox}This causes \verb!Const("enum",_)$!$t$ to be replaced by\verb$enum_tr[$$t$\verb$]$.Of course the definition of \verb$make_list$ should be included in the$ML$-section.\end{example}\begin{example}\label{SET} Isabelle represents the set $\{ x \mid P(x) \}$ internally by $Set(\lambda x.P(x))$. The internal and external forms need separateconstants:\footnote{In practice, the external form typically has a namebeginning with an {\at} sign, such as {\tt {\at}SET}. This emphasizes thatthe constant should be used only for parsing/printing.}\begin{ttbox}types set 1arities set :: (term)termconsts Set :: "('a => o) => 'a set" SET :: "[id,o] => 'a set" ("\{_ | _\}")\end{ttbox}Parsing {\tt"\{$x$ | $P$\}"} according to this syntax yields the term {\tt Const("SET",dummyT) \$ Free("\(x\)",dummyT) \$ \(p\)}, where $p$ is theresult 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\begin{ttbox}fun set_tr[Free(s,T), p] = Const("Set", dummyT) $ Abs(s, T, abstract_over(Free(s,T), p));\end{ttbox}where \verb$abstract_over: term*term -> term$ is a predefined function suchthat {\tt abstract_over($u$,$t$)} replaces every occurrence of $u$ in $t$ bya {\tt Bound} variable of the correct index (i.e.\ 0 at top level). Rememberthat {\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} byincluding the \ML-text\begin{ttbox}val parse_translation = [("SET", set_tr)];\end{ttbox}\end{example}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$. Thepurpose 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 includethe line\begin{ttbox}val print_translation = [];\end{ttbox}This is instructive because the terms are then printed out in their internalform. 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 isworking correctly.%\begin{warn}%Explicit type constraints disappear with type checking but are still%visible to the parse translation functions.%\end{warn}\index{parse translation|)}\section{Printing}Syntax definitions provide printing information in three distinct ways:through\begin{itemize}\item the syntax of the language (as used for parsing),\item pretty printing information, and\item print translation functions.\end{itemize}The bare mixfix declarations enable Isabelle to print terms, but the resultwill 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\begin{ttbox}consts \(c\) :: \(\tau\) (\(sy\))\end{ttbox}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 ofthe mixfix syntax if they are required to separate tokens or achieve acertain layout.\subsection{Pretty printing}\label{PrettyPrinting}\index{pretty printing}In order to format the output, it is possible to embed pretty printingdirectives in mixfix annotations. These directives are ignored during parsingand affect only printing. The characters {\tt(}, {\tt)} and {\tt/} areinterpreted as meta-characters\index{meta-character} when found in a mixfixannotation. Their meaning is\begin{description}\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.\end{description}\subsection{Print translations *}\label{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 constantnames with user-defined translation functions by including a line\begin{ttbox}val print_translation = \dots\end{ttbox}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$}.\begin{example}Reversing the effect of the parse translation in Example~\ref{list-enum} isaccomplished by the following function:\begin{ttbox}fun make_enum (Const("op :",_) $ e $ es) = case es of Const("[]",_) => Const("sing",dummyT) $ e | _ => Const("enum",dummyT) $ e $ make_enum es;\end{ttbox}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 theattempted translation has failed and the term should be printed as is.The connection with Isabelle's pretty printer is established as follows:\begin{ttbox}fun enum_tr'[x,xs] = Const("enum",dummyT) $ make_enum(Const("op :",dummyT)$x$xs);val print_translation = [("op :", enum_tr')];\end{ttbox}This declaration causes the printer to print \hbox{\tt enum_tr'[$x$,$y$]}whenever it finds \verb!Const("op :",_)$!$x$\verb!$!$y$.\end{example}\begin{example} 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:\begin{ttbox}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;\end{ttbox}The function \verb$variant_abs$, a basic term manipulation function, replacesthe bound variable $x$ by a {\tt Free} variable $x'$ having a unique name. Aterm produced by {\tt set_tr'} can now be printed according to the concretesyntax defined in Example~\ref{SET} above.Notice that the application of {\tt set_tr'} fails if the second component ofthe argument is not an abstraction, but for example just a {\tt Free}variable. This is intentional because it signals to the caller that thetranslation is inapplicable. As a result {\tt Const("Set",_)\$Free("P",_)}prints as {\tt"Set(P)"}.The full theory extension, including concrete syntax and both translationfunctions, has the following form:\begin{ttbox}types set 1arities set :: (term)termconsts Set :: "('a => o) => 'a set" SET :: "[id,o] => 'a set" ("\{_ | _\}")endMLfun 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')];\end{ttbox}\end{example}As during the parse translation process, the types attached to constantsduring 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}showever must be preserved because they may get printed (see {\ttshow_types}).\index{print translation|)}\subsection{Printing a term}Let $tab$ be the set of all string-function pairs of print translations in thecurrent syntax.Terms are printed recursively; print translations are applied top down:\begin{itemize}\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:\begin{center}{\tt\begin{tabular}{cccc}\verb$Var(("v",0),_)$ & \verb$Var(("v",7),_)$ & \verb$Var(("v5",0),_)$ \\"?v" & "?v7" & "?v5.0"\end{tabular}}\end{center}\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.\end{itemize}Printing a term {\tt $c$\$$t@1$\$\dots\$$t@n$} as an application meansprinting it as {\tt $s$($s@1$,\dots,$s@n$)}, where $s@i$ is the result ofprinting $t@i$. If $c$ is a {\tt Const}, $s$ is its first argument;otherwise $s$ is the result of printing $c$ as described above.\medskipThe printer also inserts parentheses where they are necessary for reasonsof precedence.\section{Identifiers, constants, and type inference *}\label{Typing}There is one final step in the translation from strings to terms that we havenot covered yet. It explains how constants are distinguished from {\tt Free}sand 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 syntaxcan be either a free variable or a constant. Since the parser knows onlyabout 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 userinterface level functions like {\tt goal} type terms according to the giventheory, 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 isa constant $f$ of {\tt typ} $\tau$ in $T$. This means that identifiers aretreated as {\tt Free}s iff they are not declared in the theory. The types ofthe remaining {\tt Free}s (and {\tt Var}s) are inferred as in \ML. Typeconstraints can be used to remove ambiguities.One peculiarity of the current type inference algorithm is that variableswith the same name must have the same type, irrespective of whether they areschematic, 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 tohave the same type. Unifying $\alpha\To\alpha$ and $\beta{::}term$ failsbecause, 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, itremains to be shown how they fit together. In particular we need to say howan object-logic syntax is hooked up to the meta-logic. Since all theoremsmust conform to the syntax for $prop$ (see Figure~\ref{MetaLogicSyntax}),that syntax has to be extended with the object-level syntax. Assume that thesyntax of your object-logic defines a category $o$ of formulae. Theseformulae can now appear in axioms and theorems wherever $prop$ does if youadd the production\[ prop ~=~ form. \]More precisely, you need a coercion from formulae to propositions:\begin{ttbox}Base = Pure +types o 0arities o :: logicconsts Trueprop :: "o => prop" ("_" 5)end\end{ttbox}The constant {\tt Trueprop} (the name is arbitrary) acts as an invisiblecoercion 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} ofimplication. Its definition in Isabelle needs no advanced features butillustrates the overall mechanism quite nicely:\begin{ttbox}Hilbert = Base +consts "-->" :: "[o,o] => o" (infixr 10)rulesK "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 todefine but difficult to use. The following natural deduction formulation isfar preferable:\begin{ttbox}MinI = Base +consts "-->" :: "[o,o] => o" (infixr 10)rulesimpI "(P ==> Q) ==> P --> Q"impE "[| P --> Q; P |] ==> Q"end\end{ttbox}Note, however, that although the two systems are equivalent, this fact cannotbe 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 reasonis 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\verb!Hilbert!.It is a very simple matter to extend minimal logic with falsity:\begin{ttbox}MinIF = MinI +consts False :: "o"rulesFalseE "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)rulesconjI "[| 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!