summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Logics/old.defining.tex

author | wenzelm |

Fri, 10 Nov 2000 19:02:37 +0100 | |

changeset 10432 | 3dfbc913d184 |

parent 104 | d8205bb279a7 |

permissions | -rw-r--r-- |

added axclass inverse and consts inverse, divide (infix "/");
moved axclass power to Nat.thy;

\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 conditions: \begin{itemize} \item There are no two declarations $ty :: (\vec{r})c$ and $ty :: (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example \begin{ttbox} types ty 1 arities ty :: (\{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 of types represented by $s$. For example \begin{ttbox} classes term < logic types ty 1 arities 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 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. \begin{example} \label{PrecedenceEx} The following simple grammar for arithmetic expressions demonstrates how binding power and associativity of operators can be enforced by precedences. \begin{center} \begin{tabular}{rclr} $A@9$ & = & {\tt0} \\ $A@9$ & = & {\tt(} $A@0$ {\tt)} \\ $A@0$ & = & $A@0$ {\tt+} $A@1$ \\ $A@2$ & = & $A@3$ {\tt*} $A@2$ \\ $A@3$ & = & {\tt-} $A@3$ \end{tabular} \end{center} The choice of precedences determines that \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 in Example~\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) 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. \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 with predefined 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 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: \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 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: \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, 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 arguments. \begin{example} In mixfix notation the grammar in Example~\ref{PrecedenceEx} can be written as follows: \begin{ttbox} types exp 0 consts "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 but an argument position. The following characters are also meta-characters: \begin{ttbox} ' ( ) / \end{ttbox} 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: \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 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 \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 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 \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 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 \begin{ttbox} types A,B,C 0 consts 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 second production been some non-empty string, both {\tt"A y"} and {\tt"A x"} would be 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 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 space. 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: \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 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: \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 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: \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 in Figure~\ref{MetaLogicSyntax}. 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 *} \label{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 \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 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. \begin{example}\label{list-enum} \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: \begin{ttbox} 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" ("_, _") 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, 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: \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 needs to contain the following $ML$-section: \begin{ttbox} ML fun 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 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.} \begin{ttbox} types set 1 arities set :: (term)term consts 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 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 \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 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 \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$. 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 \begin{ttbox} val print_translation = []; \end{ttbox} 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. %\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 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 \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 of the mixfix syntax if they are required to separate tokens or achieve a certain layout. \subsection{Pretty printing} \label{PrettyPrinting} \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 \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 constant names 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} is accomplished 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 the attempted 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, 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: \begin{ttbox} types set 1 arities set :: (term)term consts Set :: "('a => o) => 'a set" SET :: "[id,o] => 'a set" ("\{_ | _\}") end ML 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')]; \end{ttbox} \end{example} 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 show_types}). \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: \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 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. \medskip The printer also inserts parentheses where they are necessary for reasons of precedence. \section{Identifiers, constants, and type inference *} \label{Typing} 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: \begin{ttbox} Base = Pure + types o 0 arities o :: logic consts Trueprop :: "o => prop" ("_" 5) end \end{ttbox} The constant {\tt Trueprop} (the name is arbitrary) acts as an invisible coercion function. Assuming this definition resides in a file {\tt base.thy}, you have to load it with the command {\tt use_thy"base"}. One of the simplest nontrivial logics is {\em minimal logic} of implication. Its definition in Isabelle needs no advanced features but illustrates the overall mechanism quite nicely: \begin{ttbox} Hilbert = Base + consts "-->" :: "[o,o] => o" (infixr 10) rules K "P --> Q --> P" S "(P --> Q --> R) --> (P --> Q) --> P --> R" MP "[| P --> Q; P |] ==> Q" end \end{ttbox} After loading this definition you can start to prove theorems in this logic: \begin{ttbox} goal Hilbert.thy "P --> P"; {\out Level 0} {\out P --> P} {\out 1. P --> P} by (resolve_tac [Hilbert.MP] 1); {\out Level 1} {\out P --> P} {\out 1. ?P --> P --> P} {\out 2. ?P} by (resolve_tac [Hilbert.MP] 1); {\out Level 2} {\out P --> P} {\out 1. ?P1 --> ?P --> P --> P} {\out 2. ?P1} {\out 3. ?P} by (resolve_tac [Hilbert.S] 1); {\out Level 3} {\out P --> P} {\out 1. P --> ?Q2 --> P} {\out 2. P --> ?Q2} by (resolve_tac [Hilbert.K] 1); {\out Level 4} {\out P --> P} {\out 1. P --> ?Q2} by (resolve_tac [Hilbert.K] 1); {\out Level 5} {\out P --> P} {\out No subgoals!} \end{ttbox} As you can see, this Hilbert-style formulation of minimal logic is easy to define but difficult to use. The following natural deduction formulation is far preferable: \begin{ttbox} MinI = Base + consts "-->" :: "[o,o] => o" (infixr 10) rules impI "(P ==> Q) ==> P --> Q" impE "[| P --> Q; P |] ==> Q" end \end{ttbox} Note, however, that although the two systems are equivalent, this fact cannot be proved within Isabelle: {\tt S} and {\tt K} can be derived in \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 \verb!Hilbert!. It is a very simple matter to extend minimal logic with falsity: \begin{ttbox} MinIF = MinI + consts False :: "o" rules FalseE "False ==> P" end \end{ttbox} On the other hand, we may wish to introduce conjunction only: \begin{ttbox} MinC = Base + consts "&" :: "[o,o] => o" (infixr 30) rules conjI "[| P; Q |] ==> P & Q" conjE1 "P & Q ==> P" conjE2 "P & Q ==> Q" end \end{ttbox} And if we want to have all three connectives together, we define: \begin{ttbox} MinIFC = MinIF + MinC \end{ttbox} Now we can prove mixed theorems like \begin{ttbox} goal MinIFC.thy "P & False --> Q"; by (resolve_tac [MinI.impI] 1); by (dresolve_tac [MinC.conjE2] 1); by (eresolve_tac [MinIF.FalseE] 1); \end{ttbox} Try this as an exercise!