doc-src/Logics/old.defining.tex
 author paulson Fri Feb 16 18:00:47 1996 +0100 (1996-02-16) changeset 1512 ce37c64244c0 parent 104 d8205bb279a7 permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     1 \chapter{Defining Logics} \label{Defining-Logics}

     2 This chapter is intended for Isabelle experts.  It explains how to define new

     3 logical systems, Isabelle's {\it raison d'\^etre}.  Isabelle logics are

     4 hierarchies of theories.  A number of simple examples are contained in the

     5 introductory manual; the full syntax of theory definitions is shown in the

     6 {\em Reference Manual}.  The purpose of this chapter is to explain the

     7 remaining subtleties, especially some context conditions on the class

     8 structure and the definition of new mixfix syntax.  A full understanding of

     9 the material requires knowledge of the internal representation of terms (data

    10 type {\tt term}) as detailed in the {\em Reference Manual}.  Sections marked

    11 with a * can be skipped on first reading.

    12

    13

    14 \section{Classes and Types *}

    15 \index{*arities!context conditions}

    16

    17 Type declarations are subject to the following two well-formedness

    18 conditions:

    19 \begin{itemize}

    20 \item There are no two declarations $ty :: (\vec{r})c$ and $ty :: (\vec{s})c$

    21   with $\vec{r} \neq \vec{s}$.  For example

    22 \begin{ttbox}

    23 types ty 1

    24 arities ty :: (\{logic\}) logic

    25         ty :: (\{\})logic

    26 \end{ttbox}

    27 leads to an error message and fails.

    28 \item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::   29 (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold

    30   for $i=1,\dots,n$.  The relationship $\preceq$, defined as

    31 $s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c,$

    32 expresses that the set of types represented by $s'$ is a subset of the set of

    33 types represented by $s$.  For example

    34 \begin{ttbox}

    35 classes term < logic

    36 types ty 1

    37 arities ty :: (\{logic\})logic

    38         ty :: (\{\})term

    39 \end{ttbox}

    40 leads to an error message and fails.

    41 \end{itemize}

    42 These conditions guarantee principal types~\cite{nipkow-prehofer}.

    43

    44 \section{Precedence Grammars}

    45 \label{PrecedenceGrammars}

    46 \index{precedence grammar|(}

    47

    48 The precise syntax of a logic is best defined by a context-free grammar.

    49 These grammars obey the following conventions: identifiers denote

    50 nonterminals, {\tt typewriter} fount denotes terminals, repetition is

    51 indicated by \dots, and alternatives are separated by $|$.

    52

    53 In order to simplify the description of mathematical languages, we introduce

    54 an extended format which permits {\bf precedences}\index{precedence}.  This

    55 scheme generalizes precedence declarations in \ML\ and {\sc prolog}.  In this

    56 extended grammar format, nonterminals are decorated by integers, their

    57 precedence.  In the sequel, precedences are shown as subscripts.  A nonterminal

    58 $A@p$ on the right-hand side of a production may only be replaced using a

    59 production $A@q = \gamma$ where $p \le q$.

    60

    61 Formally, a set of context free productions $G$ induces a derivation

    62 relation $\rew@G$ on strings as follows:

    63 $\alpha A@p \beta ~\rew@G~ \alpha\gamma\beta ~~~iff~~~   64 \exists q \ge p.~(A@q=\gamma) \in G   65$

    66 Any extended grammar of this kind can be translated into a normal context

    67 free grammar.  However, this translation may require the introduction of a

    68 large number of new nonterminals and productions.

    69

    70 \begin{example}

    71 \label{PrecedenceEx}

    72 The following simple grammar for arithmetic expressions demonstrates how

    73 binding power and associativity of operators can be enforced by precedences.

    74 \begin{center}

    75 \begin{tabular}{rclr}

    76 $A@9$ & = & {\tt0} \\

    77 $A@9$ & = & {\tt(} $A@0$ {\tt)} \\

    78 $A@0$ & = & $A@0$ {\tt+} $A@1$ \\

    79 $A@2$ & = & $A@3$ {\tt*} $A@2$ \\

    80 $A@3$ & = & {\tt-} $A@3$

    81 \end{tabular}

    82 \end{center}

    83 The choice of precedences determines that \verb$-$ binds tighter than

    84 \verb$*$ which binds tighter than \verb$+$, and that \verb$+$ and \verb$*$

    85 associate to the left and right, respectively.

    86 \end{example}

    87

    88 To minimize the number of subscripts, we adopt the following conventions:

    89 \begin{itemize}

    90 \item all precedences $p$ must be in the range $0 \leq p \leq max_pri$ for

    91   some fixed $max_pri$.

    92 \item precedence $0$ on the right-hand side and precedence $max_pri$ on the

    93   left-hand side may be omitted.

    94 \end{itemize}

    95 In addition, we write the production $A@p = \alpha$ as $A = \alpha~(p)$.

    96

    97 Using these conventions and assuming $max_pri=9$, the grammar in

    98 Example~\ref{PrecedenceEx} becomes

    99 \begin{center}

   100 \begin{tabular}{rclc}

   101 $A$ & = & {\tt0} & \hspace*{4em} \\

   102  & $|$ & {\tt(} $A$ {\tt)} \\

   103  & $|$ & $A$ {\tt+} $A@1$ & (0) \\

   104  & $|$ & $A@3$ {\tt*} $A@2$ & (2) \\

   105  & $|$ & {\tt-} $A@3$ & (3)

   106 \end{tabular}

   107 \end{center}

   108

   109 \index{precedence grammar|)}

   110

   111 \section{Basic syntax *}

   112

   113 An informal account of most of Isabelle's syntax (meta-logic, types etc) is

   114 contained in {\em Introduction to Isabelle}.  A precise description using a

   115 precedence grammar is shown in Figure~\ref{MetaLogicSyntax}.  This description

   116 is the basis of all extensions by object-logics.

   117 \begin{figure}[htb]

   118 \begin{center}

   119 \begin{tabular}{rclc}

   120 $prop$ &=& \ttindex{PROP} $aprop$ ~~$|$~~ {\tt(} $prop$ {\tt)} \\

   121      &$|$& $logic@3$ \ttindex{==} $logic@2$ & (2) \\

   122      &$|$& $prop@2$ \ttindex{==>} $prop@1$ & (1) \\

   123      &$|$& {\tt[|} $prop$ {\tt;} \dots {\tt;} $prop$ {\tt|]} {\tt==>} $prop@1$ & (1) \\

   124      &$|$& {\tt!!} $idts$ {\tt.} $prop$ & (0) \\\\

   125 $logic$ &=& $prop$ ~~$|$~~ $fun$ \\\\

   126 $aprop$ &=& $id$ ~~$|$~~ $var$

   127     ~~$|$~~ $fun@{max_pri}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\\\

   128 $fun$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $fun$ {\tt)} \\

   129     &$|$& \ttindex{\%} $idts$ {\tt.} $logic$ & (0) \\\\

   130 $idts$ &=& $idt$ ~~$|$~~ $idt@1$ $idts$ \\\\

   131 $idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\

   132     &$|$& $id$ \ttindex{::} $type$ & (0) \\\\

   133 $type$ &=& $tfree$ ~~$|$~~ $tvar$ \\

   134      &$|$& $tfree$ {\tt::} $sort$ ~~$|$~~ $tvar$ {\tt::} $sort$ \\

   135      &$|$& $id$ ~~$|$~~ $type@{max_pri}$ $id$

   136                 ~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $id$ \\

   137      &$|$& $type@1$ \ttindex{=>} $type$ & (0) \\

   138      &$|$& {\tt[}  $type$ {\tt,} \dots {\tt,} $type$ {\tt]} {\tt=>} $type$&(0)\\

   139      &$|$& {\tt(} $type$ {\tt)} \\\\

   140 $sort$ &=& $id$ ~~$|$~~ {\tt\{\}}

   141                 ~~$|$~~ {\tt\{} $id$ {\tt,} \dots {\tt,} $id$ {\tt\}}

   142 \end{tabular}\index{*"!"!}\index{*"["|}\index{*"|"]}

   143 \indexbold{type@$type$}\indexbold{sort@$sort$}\indexbold{idts@$idts$}

   144 \indexbold{logic@$logic$}\indexbold{prop@$prop$}\indexbold{fun@$fun$}

   145 \end{center}

   146 \caption{Meta-Logic Syntax}

   147 \label{MetaLogicSyntax}

   148 \end{figure}

   149 The following main categories are defined:

   150 \begin{description}

   151 \item[$prop$] Terms of type $prop$, i.e.\ formulae of the meta-logic.

   152 \item[$aprop$] Atomic propositions.

   153 \item[$logic$] Terms of types in class $logic$.  Initially, $logic$ contains

   154   merely $prop$.  As the syntax is extended by new object-logics, more

   155   productions for $logic$ are added (see below).

   156 \item[$fun$] Terms potentially of function type.

   157 \item[$type$] Types.

   158 \item[$idts$] a list of identifiers, possibly constrained by types.  Note

   159   that $x::nat~y$ is parsed as $x::(nat~y)$, i.e.\ $y$ is treated like a

   160   type constructor applied to $nat$.

   161 \end{description}

   162

   163 The predefined types $id$, $var$, $tfree$ and $tvar$ represent identifiers

   164 ({\tt f}), unknowns ({\tt ?f}), type variables ({\tt 'a}), and type unknowns

   165 ({\tt ?'a}) respectively.  If we think of them as nonterminals with

   166 predefined syntax, we may assume that all their productions have precedence

   167 $max_pri$.

   168

   169 \subsection{Logical types and default syntax}

   170

   171 Isabelle is concerned with mathematical languages which have a certain

   172 minimal vocabulary: identifiers, variables, parentheses, and the lambda

   173 calculus.  Logical types, i.e.\ those of class $logic$, are automatically

   174 equipped with this basic syntax.  More precisely, for any type constructor

   175 $ty$ with arity $(\dots)c$, where $c$ is a subclass of $logic$, the following

   176 productions are added:

   177 \begin{center}

   178 \begin{tabular}{rclc}

   179 $ty$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $ty$ {\tt)} \\

   180   &$|$& $fun@{max_pri}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)}\\

   181   &$|$& $ty@{max_pri}$ {\tt::} $type$\\\\

   182 $logic$ &=& $ty$

   183 \end{tabular}

   184 \end{center}

   185

   186

   187 \section{Mixfix syntax}

   188 \index{mixfix|(}

   189

   190 We distinguish between abstract and concrete syntax.  The {\em abstract}

   191 syntax is given by the typed constants of a theory.  Abstract syntax trees are

   192 well-typed terms, i.e.\ values of \ML\ type {\tt term}.  If none of the

   193 constants are introduced with mixfix annotations, there is no concrete syntax

   194 to speak of: terms can only be abstractions or applications of the form

   195 $f(t@1,\dots,t@n)$, where $f$ is a constant or variable.  Since this notation

   196 quickly becomes unreadable, Isabelle supports syntax definitions in the form

   197 of unrestricted context-free grammars using mixfix annotations.

   198

   199 Mixfix annotations describe the {\em concrete} syntax, its translation into

   200 the abstract syntax, and a pretty-printing scheme, all in one.  Isabelle

   201 syntax definitions are inspired by \OBJ's~\cite{OBJ} {\em mixfix\/} syntax.

   202 Each mixfix annotation defines a precedence grammar production and associates

   203 an Isabelle constant with it.

   204

   205 A {\em mixfix declaration} {\tt consts $c$ ::\ $\tau$ ($sy$ $ps$ $p$)} is

   206 interpreted as a grammar pro\-duction as follows:

   207 \begin{itemize}

   208 \item $sy$ is the right-hand side of this production, specified as a {\em

   209     mixfix annotation}.  In general, $sy$ is of the form

   210   $\alpha@0\_\alpha@1\dots\alpha@{n-1}\_\alpha@n$, where each occurrence of

   211   \ttindex{_}'' denotes an argument/nonterminal and the strings

   212   $\alpha@i$ do not contain {\tt_}''.

   213 \item $\tau$ specifies the types of the nonterminals on the left and right

   214   hand side. If $sy$ is of the form above, $\tau$ must be of the form

   215   $[\tau@1,\dots,\tau@n] \To \tau'$.  Then argument $i$ is of type $\tau@i$

   216   and the result, i.e.\ the left-hand side of the production, is of type

   217   $\tau'$.  Both the $\tau@i$ and $\tau'$ may be function types.

   218 \item $c$ is the name of the Isabelle constant associated with this production.

   219   Parsing an instance of the phrase $sy$ generates the {\tt term} {\tt

   220     Const($c$,dummyT\footnote{Proper types are inserted later on.  See

   221       \S\ref{Typing}})\$$a@1\$$\dots$\$$a@n}\index{*dummyT}, where a@i is   222 the term generated by parsing the i^{th} argument.   223 \item ps must be of the form [p@1,\dots,p@n], where p@i is the   224 minimal precedence\index{precedence} required of any phrase that may appear   225 as the i^{th} argument. The null list is interpreted as a list of 0's of   226 the appropriate length.   227 \item p is the precedence of this production.   228 \end{itemize}   229 Notice that there is a close connection between abstract and concrete syntax:   230 each production has an associated constant, and types act as {\bf syntactic   231 categories} in the concrete syntax. To emphasize this connection, we   232 sometimes refer to the nonterminals on the right-hand side of a production as   233 its arguments and to the nonterminal on the left-hand side as its result.   234   235 The maximal legal precedence is called \ttindexbold{max_pri}, which is   236 currently 1000. If you want to ignore precedences, the safest way to do so is   237 to use the annotation {\tt(sy)}: this production puts no precedence   238 constraints on any of its arguments and has maximal precedence itself, i.e.\   239 it is always applicable and does not exclude any productions of its   240 arguments.   241   242 \begin{example}   243 In mixfix notation the grammar in Example~\ref{PrecedenceEx} can be written   244 as follows:   245 \begin{ttbox}   246 types exp 0   247 consts "0" :: "exp" ("0" 9)   248 "+" :: "[exp,exp] => exp" ("_ + _" [0,1] 0)   249 "*" :: "[exp,exp] => exp" ("_ * _" [3,2] 2)   250 "-" :: "exp => exp" ("- _"  3)   251 \end{ttbox}   252 Parsing the string \verb!"0 + - 0 + 0"! produces the term {\tt   253 p\(p\(m\$$z$)\$$z)\$$z$} where {\tt$p =$Const("+",dummyT)},   254 {\tt$m =$Const("-",dummyT)}, and {\tt$z =$Const("0",dummyT)}.   255 \end{example}   256   257 The interpretation of \ttindex{_} in a mixfix annotation is always as a {\bf   258 meta-character}\index{meta-character} which does not represent itself but   259 an argument position. The following characters are also meta-characters:   260 \begin{ttbox}   261 ' ( ) /   262 \end{ttbox}   263 Preceding any character with a quote (\verb$'$) turns it into an ordinary   264 character. Thus you can write \verb!''! if you really want a single quote.   265 The purpose of the other meta-characters is explained in   266 \S\ref{PrettyPrinting}. Remember that in \ML\ strings \verb$\$is already a   267 (different kind of) meta-character.   268   269   270 \subsection{Types and syntactic categories *}   271   272 The precise mapping from types to syntactic categories is defined by the   273 following function:   274 \begin{eqnarray*}   275 N(\tau@1\To\tau@2) &=& fun \\   276 N((\tau@1,\dots,\tau@n)ty) &=& ty \\   277 N(\alpha) &=& logic   278 \end{eqnarray*}   279 Only the outermost type constructor is taken into account and type variables   280 can range over all logical types. This catches some ill-typed terms (like   281$Cons(x,0)$, where$Cons :: [\alpha,\alpha list] \To \alpha list$and$0 ::

   282 nat$) but leaves the real work to the type checker.   283   284 In terms of the precedence grammar format introduced in   285 \S\ref{PrecedenceGrammars}, the declaration   286 \begin{ttbox}   287 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$$)   288 \end{ttbox}   289 defines the production   290 $N(\tau)@p ~~=~~ \alpha@0 ~N(\tau@1)@{p@1}~ \alpha@1~ \dots   291 ~\alpha@{n-1} ~N(\tau@n)@{p@n}~ \alpha@n   292$   293   294 \subsection{Copy productions *}   295   296 Productions which do not create a new node in the abstract syntax tree are   297 called {\bf copy productions}. They must have exactly one nonterminal on   298 the right hand side. The term generated when parsing that nonterminal is   299 simply passed up as the result of parsing the whole copy production. In   300 Isabelle a copy production is indicated by an empty constant name, i.e.\ by   301 \begin{ttbox}   302 consts "" :: $$\tau$$ ($$sy$$ $$ps$$ $$p$$)   303 \end{ttbox}   304   305 A special kind of copy production is one where, modulo white space,$sy$is   306 {\tt"_"}. It is called a {\bf chain production}. Chain productions should be   307 seen as an abbreviation mechanism. Conceptually, they are removed from the   308 grammar by adding appropriate new rules. Precedence information attached to   309 chain productions is ignored. The following example demonstrates the effect:   310 the grammar defined by   311 \begin{ttbox}   312 types A,B,C 0   313 consts AB :: "B => A" ("A _"  517)   314 "" :: "C => B" ("_"  100)   315 x :: "C" ("x" 5)   316 y :: "C" ("y" 15)   317 \end{ttbox}   318 admits {\tt"A y"} but not {\tt"A x"}. Had the constant in the second   319 production been some non-empty string, both {\tt"A y"} and {\tt"A x"} would   320 be legal.   321   322 \index{mixfix|)}   323   324 \section{Lexical conventions}   325   326 The lexical analyzer distinguishes the following kinds of tokens: delimiters,   327 identifiers, unknowns, type variables and type unknowns.   328   329 Delimiters are user-defined, i.e.\ they are extracted from the syntax   330 definition. If$\alpha@0\_\alpha@1\dots\alpha@{n-1}\_\alpha@n$is a mixfix   331 annotation, each$\alpha@i$is decomposed into substrings   332$\beta@1~\dots~\beta@k$which are separated by and do not contain   333 \bfindex{white space} ( = blanks, tabs, newlines). Each$\beta@j$becomes a   334 delimiter. Thus a delimiter can be an arbitrary string not containing white   335 space.   336   337 The lexical syntax of identifiers and variables ( = unknowns) is defined in   338 the introductory manual. Parsing an identifier$f$generates {\tt   339 Free($f$,dummyT)}\index{*dummyT}. Parsing a variable {\tt?}$v$generates   340 {\tt Var(($u$,$i$),dummyT)} where$i$is the integer value of the longest   341 numeric suffix of$v$(possibly$0$), and$u$is the remaining prefix.   342 Parsing a variable {\tt?}$v{.}i$generates {\tt Var(($v$,$i$),dummyT)}. The   343 following table covers the four different cases that can arise:   344 \begin{center}\tt   345 \begin{tabular}{cccc}   346 "?v" & "?v.7" & "?v5" & "?v7.5" \\   347 Var(("v",0),$d$) & Var(("v",7),$d$) & Var(("v",5),$d$) & Var(("v7",5),$d$)   348 \end{tabular}   349 \end{center}   350 where$d = {\tt dummyT}$.   351   352 In mixfix annotations, \ttindexbold{id}, \ttindexbold{var},   353 \ttindexbold{tfree} and \ttindexbold{tvar} are the predefined categories of   354 identifiers, unknowns, type variables and type unknowns, respectively.   355   356   357 The lexical analyzer translates input strings to token lists by repeatedly   358 taking the maximal prefix of the input string that forms a valid token. A   359 maximal prefix that is both a delimiter and an identifier or variable (like   360 {\tt ALL}) is treated as a delimiter. White spaces are separators.   361   362 An important consequence of this translation scheme is that delimiters need   363 not be separated by white space to be recognized as separate. If \verb$"-"$  364 is a delimiter but \verb$"--"$is not, the string \verb$"--"$is treated as   365 two consecutive occurrences of \verb$"-"$. This is in contrast to \ML\ which   366 would treat \verb$"--"$as a single (undeclared) identifier. The   367 consequence of Isabelle's more liberal scheme is that the same string may be   368 parsed in a different way after extending the syntax: after adding   369 \verb$"--"$as a delimiter, the input \verb$"--"$is treated as   370 a single occurrence of \verb$"--"$.   371   372 \section{Infix operators}   373   374 {\tt Infixl} and {\tt infixr} declare infix operators which associate to the   375 left and right respectively. As in \ML, prefixing infix operators with   376 \ttindexbold{op} turns them into curried functions. Infix declarations can   377 be reduced to mixfix ones as follows:   378 \begin{center}\tt   379 \begin{tabular}{l@{~~$\Longrightarrow$~~}l}   380 "$c$" ::~$\tau$(\ttindexbold{infixl}$p$) &   381 "op$c$" ::~$\tau$("_$c$_" [$p$,$p+1$]$p$) \\   382 "$c$" ::~$\tau$(\ttindexbold{infixr}$p$) &   383 "op$c$" ::~$\tau$("_$c$_" [$p+1$,$p$]$p$)   384 \end{tabular}   385 \end{center}   386   387   388 \section{Binders}   389 A {\bf binder} is a variable-binding constant, such as a quantifier.   390 The declaration   391 \begin{ttbox}   392 consts $$c$$ :: $$\tau$$ (binder $$Q$$ $$p$$)   393 \end{ttbox}\indexbold{*binder}   394 introduces a binder$c$of type$\tau$,   395 which must have the form$(\tau@1\To\tau@2)\To\tau@3$. Its concrete syntax   396 is$Q~x.t$. A binder is like a generalized quantifier where$\tau@1$is the   397 type of the bound variable$x$,$\tau@2$the type of the body$t$, and   398$\tau@3$the type of the whole term. For example$\forall$can be declared   399 like this:   400 \begin{ttbox}   401 consts All :: "('a => o) => o" (binder "ALL " 10)   402 \end{ttbox}   403 This allows us to write$\forall x.P$either as {\tt ALL$x$.$P$} or {\tt   404 All(\%$x$.$P$)}; the latter form is for purists only.   405   406 In case$\tau@2 = \tau@3$, nested quantifications can be written as$Q~x@1

   407 \dots x@n.t$. From a syntactic point of view,   408 \begin{ttbox}   409 consts $$c$$ :: "$$(\tau@1\To\tau@2)\To\tau@3$$" (binder "$$Q$$" $$p$$)   410 \end{ttbox}   411 is equivalent to   412 \begin{ttbox}   413 consts $$c$$ :: "$$(\tau@1\To\tau@2)\To\tau@3$$"   414 "$$Q$$" :: "[idts,$$\tau@2$$] => $$\tau@3$$" ("$$Q$$_. _" $$p$$)   415 \end{ttbox}   416 where {\tt idts} is the syntactic category$idts$defined in   417 Figure~\ref{MetaLogicSyntax}.   418   419 However, there is more to binders than concrete syntax: behind the scenes the   420 body of the quantified expression has to be converted into a   421$\lambda$-abstraction (when parsing) and back again (when printing). This   422 is performed by the translation mechanism, which is discussed below. For   423 binders, the definition of the required translation functions has been   424 automated. Many other syntactic forms, such as set comprehension, require   425 special treatment.   426   427   428 \section{Parse translations *}   429 \label{Parse-translations}   430 \index{parse translation|(}   431   432 So far we have pretended that there is a close enough relationship between   433 concrete and abstract syntax to allow an automatic translation from one to   434 the other using the constant name supplied with each production. In many   435 cases this scheme is not powerful enough, especially for constructs involving   436 variable bindings. Therefore the$ML$-section of a theory definition can   437 associate constant names with user-defined translation functions by including   438 a line   439 \begin{ttbox}   440 val parse_translation = \dots   441 \end{ttbox}   442 where the right-hand side of this binding must be an \ML-expression of type   443 \verb$(string * (term list -> term))list$.   444   445 After the input string has been translated into a term according to the   446 syntax definition, there is a second phase in which the term is translated   447 using the user-supplied functions in a bottom-up manner. Given a list$tab$  448 of the above type, a term$t$is translated as follows. If$t$is not of the   449 form {\tt Const($c$,$\tau$)\$$t@1\\dots\$$t@n$}, then $t$ is returned

   450 unchanged.  Otherwise all $t@i$ are translated into $t@i'$.  Let {\tt $t' =$

   451   Const($c$,$\tau$)\$$t@1'\\dots\$$t@n'$}. If there is no pair$(c,f)$in   452$tab$, return$t'$. Otherwise apply$f$to$[t@1',\dots,t@n']$. If that   453 raises an exception, return$t'$, otherwise return the result.   454 \begin{example}\label{list-enum}   455 \ML-lists are constructed by {\tt[]} and {\tt::}. For readability the   456 list \hbox{\tt$x$::$y$::$z$::[]} can be written \hbox{\tt[$x$,$y$,$z$]}.   457 In Isabelle the two forms of lists are declared as follows:   458 \begin{ttbox}   459 types list 1   460 enum 0   461 arities list :: (term)term   462 consts "[]" :: "'a list" ("[]")   463 ":" :: "['a, 'a list] => 'a list" (infixr 50)   464 enum :: "enum => 'a list" ("[_]")   465 sing :: "'a => enum" ("_")   466 cons :: "['a,enum] => enum" ("_, _")   467 end   468 \end{ttbox}   469 Because \verb$::$is already used for type constraints, it is replaced by   470 \verb$:$as the infix list constructor.   471   472 In order to allow list enumeration, the new type {\tt enum} is introduced.   473 Its only purpose is syntactic and hence it does not need an arity, in   474 contrast to the logical type {\tt list}. Although \hbox{\tt[$x$,$y$,$z$]} is   475 syntactically legal, it needs to be translated into a term built up from   476 \verb$[]$and \verb$:$. This is what \verb$make_list$accomplishes:   477 \begin{ttbox}   478 val cons = Const("op :", dummyT);   479   480 fun make_list (Const("sing",_)$e) = cons $e$ Const("[]", dummyT)

   481   | make_list (Const("cons",_)$e$es) = cons $e$ make_list es;

   482 \end{ttbox}

   483 To hook this translation up to Isabelle's parser, the theory definition needs

   484 to contain the following $ML$-section:

   485 \begin{ttbox}

   486 ML

   487 fun enum_tr[enum] = make_list enum;

   488 val parse_translation = [("enum",enum_tr)]

   489 \end{ttbox}

   490 This causes \verb!Const("enum",_)$!$t$to be replaced by   491 \verb$enum_tr[$$t\verb].   492   493 Of course the definition of \verbmake_list should be included in the   494 ML-section.   495 \end{example}   496 \begin{example}\label{SET}   497 Isabelle represents the set \{ x \mid P(x) \} internally by Set(\lambda   498 x.P(x)). The internal and external forms need separate   499 constants:\footnote{In practice, the external form typically has a name   500 beginning with an {\at} sign, such as {\tt {\at}SET}. This emphasizes that   501 the constant should be used only for parsing/printing.}   502 \begin{ttbox}   503 types set 1   504 arities set :: (term)term   505 consts Set :: "('a => o) => 'a set"   506 SET :: "[id,o] => 'a set" ("\{_ | _\}")   507 \end{ttbox}   508 Parsing {\tt"\{x | P\}"} according to this syntax yields the term {\tt   509 Const("SET",dummyT) \ Free("$$x$$",dummyT) \ $$p$$}, where p is the   510 result of parsing P. What we need is the term {\tt   511 Const("Set",dummyT)\Abs("x",dummyT,p')}, where p' is some   512 abstracted'' version of p. Therefore we define a function   513 \begin{ttbox}   514 fun set_tr[Free(s,T), p] = Const("Set", dummyT)    515 Abs(s, T, abstract_over(Free(s,T), p));   516 \end{ttbox}   517 where \verbabstract_over: term*term -> term is a predefined function such   518 that {\tt abstract_over(u,t)} replaces every occurrence of u in t by   519 a {\tt Bound} variable of the correct index (i.e.\ 0 at top level). Remember   520 that {\tt dummyT} is replaced by the correct types at a later stage (see   521 \S\ref{Typing}). Function {\tt set_tr} is associated with {\tt SET} by   522 including the \ML-text   523 \begin{ttbox}   524 val parse_translation = [("SET", set_tr)];   525 \end{ttbox}   526 \end{example}   527   528 If you want to run the above examples in Isabelle, you should note that an   529 ML-section needs to contain not just a definition of   530 \verbparse_translation but also of a variable \verbprint_translation. The   531 purpose of the latter is to reverse the effect of the former during printing;   532 details are found in \S\ref{Print-translations}. Hence you need to include   533 the line   534 \begin{ttbox}   535 val print_translation = [];   536 \end{ttbox}   537 This is instructive because the terms are then printed out in their internal   538 form. For example the input \hbox{\tt[x,y,z]} is echoed as   539 \hbox{\ttx:y:z:[]}. This helps to check that your parse translation is   540 working correctly.   541   542 %\begin{warn}   543 %Explicit type constraints disappear with type checking but are still   544 %visible to the parse translation functions.   545 %\end{warn}   546   547 \index{parse translation|)}   548   549 \section{Printing}   550   551 Syntax definitions provide printing information in three distinct ways:   552 through   553 \begin{itemize}   554 \item the syntax of the language (as used for parsing),   555 \item pretty printing information, and   556 \item print translation functions.   557 \end{itemize}   558 The bare mixfix declarations enable Isabelle to print terms, but the result   559 will not necessarily be pretty and may look different from what you expected.   560 To produce a pleasing layout, you need to read the following sections.   561   562 \subsection{Printing with mixfix declarations}   563   564 Let {\ttt = Const(c,_)\$$t@1$\$\dots\$$t@n} be a term and let   565 \begin{ttbox}   566 consts $$c$$ :: $$\tau$$ ($$sy$$)   567 \end{ttbox}   568 be a mixfix declaration where sy is of the form   569 \alpha@0\_\alpha@1\dots\alpha@{n-1}\_\alpha@n. Printing t according to   570 sy means printing the string   571 \alpha@0\beta@1\alpha@1\ldots\alpha@{n-1}\beta@n\alpha@n, where \beta@i   572 is the result of printing t@i.   573   574 Note that the system does {\em not\/} insert blanks. They should be part of   575 the mixfix syntax if they are required to separate tokens or achieve a   576 certain layout.   577   578 \subsection{Pretty printing}   579 \label{PrettyPrinting}   580 \index{pretty printing}   581   582 In order to format the output, it is possible to embed pretty printing   583 directives in mixfix annotations. These directives are ignored during parsing   584 and affect only printing. The characters {\tt(}, {\tt)} and {\tt/} are   585 interpreted as meta-characters\index{meta-character} when found in a mixfix   586 annotation. Their meaning is   587 \begin{description}   588 \item[~{\tt(}~] Open a block. A sequence of digits following it is   589 interpreted as the \bfindex{indentation} of this block. It causes the   590 output to be indented by n positions if a line break occurs within the   591 block. If {\tt(} is not followed by a digit, the indentation defaults to   592 0.   593 \item[~{\tt)}~] Close a block.   594 \item[~\ttindex{/}~] Allow a \bfindex{line break}. White space immediately   595 following {\tt/} is not printed if the line is broken at this point.   596 \end{description}   597   598 \subsection{Print translations *}   599 \label{Print-translations}   600 \index{print translation|(}   601   602 Since terms are translated after parsing (see \S\ref{Parse-translations}),   603 there is a similar mechanism to translate them back before printing.   604 Therefore the ML-section of a theory definition can associate constant   605 names with user-defined translation functions by including a line   606 \begin{ttbox}   607 val print_translation = \dots   608 \end{ttbox}   609 where the right-hand side of this binding is again an \ML-expression of type   610 \verb(string * (term list -> term))list.   611 Including a pair (c,f) in this list causes the printer to print   612 f[t@1,\dots,t@n] whenever it finds {\tt Const(c,_)\$$t@1$\$\dots\$$t@n}.   613 \begin{example}   614 Reversing the effect of the parse translation in Example~\ref{list-enum} is   615 accomplished by the following function:   616 \begin{ttbox}   617 fun make_enum (Const("op :",_)  e  es) = case es of   618 Const("[]",_) => Const("sing",dummyT)  e   619 | _ => Const("enum",dummyT)  e  make_enum es;   620 \end{ttbox}   621 It translates \hbox{\ttx:y:z:[]} to \hbox{\tt[x,y,z]}. However,   622 if the input does not terminate with an empty list, e.g.\ \hbox{\ttx:xs},   623 \verbmake_enum raises exception {\tt Match}. This signals that the   624 attempted translation has failed and the term should be printed as is.   625 The connection with Isabelle's pretty printer is established as follows:   626 \begin{ttbox}   627 fun enum_tr'[x,xs] = Const("enum",dummyT)    628 make_enum(Const("op :",dummyT)xxs);   629 val print_translation = [("op :", enum_tr')];   630 \end{ttbox}   631 This declaration causes the printer to print \hbox{\tt enum_tr'[x,y]}   632 whenever it finds \verb!Const("op :",_)!x\verb!!y.   633 \end{example}   634 \begin{example}   635 In Example~\ref{SET} we showed how to translate the concrete syntax for set   636 comprehension into the proper internal form. The string {\tt"\{x |   637 P\}"} now becomes {\tt Const("Set",_)\Abs("x",_,p)}. If, however,   638 the latter term were printed without translating it back, it would result   639 in {\tt"Set(\%x.P)"}. Therefore the abstraction has to be turned back   640 into a term that matches the concrete mixfix syntax:   641 \begin{ttbox}   642 fun set_tr'[Abs(x,T,P)] =   643 let val (x',P') = variant_abs(x,T,P)   644 in Const("SET",dummyT)  Free(x',T)  P' end;   645 \end{ttbox}   646 The function \verbvariant_abs, a basic term manipulation function, replaces   647 the bound variable x by a {\tt Free} variable x' having a unique name. A   648 term produced by {\tt set_tr'} can now be printed according to the concrete   649 syntax defined in Example~\ref{SET} above.   650   651 Notice that the application of {\tt set_tr'} fails if the second component of   652 the argument is not an abstraction, but for example just a {\tt Free}   653 variable. This is intentional because it signals to the caller that the   654 translation is inapplicable. As a result {\tt Const("Set",_)\Free("P",_)}   655 prints as {\tt"Set(P)"}.   656   657 The full theory extension, including concrete syntax and both translation   658 functions, has the following form:   659 \begin{ttbox}   660 types set 1   661 arities set :: (term)term   662 consts Set :: "('a => o) => 'a set"   663 SET :: "[id,o] => 'a set" ("\{_ | _\}")   664 end   665 ML   666 fun set_tr[Free(s,T), p] = \dots;   667 val parse_translation = [("SET", set_tr)];   668 fun set_tr'[Abs(x,T,P)] = \dots;   669 val print_translation = [("Set", set_tr')];   670 \end{ttbox}   671 \end{example}   672 As during the parse translation process, the types attached to constants   673 during print translation are ignored. Thus {\tt Const("SET",dummyT)} in   674 {\tt set_tr'} above is acceptable. The types of {\tt Free}s and {\tt Var}s   675 however must be preserved because they may get printed (see {\tt   676 show_types}).   677   678 \index{print translation|)}   679   680 \subsection{Printing a term}   681   682 Let tab be the set of all string-function pairs of print translations in the   683 current syntax.   684   685 Terms are printed recursively; print translations are applied top down:   686 \begin{itemize}   687 \item {\tt Free(x,_)} is printed as x.   688 \item {\tt Var((x,i),_)} is printed as x, if i = 0 and x does not   689 end with a digit, as x followed by i, if i \neq 0 and x does not   690 end with a digit, and as {\tt x.i}, if x ends with a digit. Thus the   691 following cases can arise:   692 \begin{center}   693 {\tt\begin{tabular}{cccc}   694 \verbVar(("v",0),_) & \verbVar(("v",7),_) & \verbVar(("v5",0),_) \\   695 "?v" & "?v7" & "?v5.0"   696 \end{tabular}}   697 \end{center}   698 \item {\tt Abs(x@1,_,Abs(x@2,_,\dots Abs(x@n,_,p)\dots))}, where p   699 is not an abstraction, is printed as {\tt \%y@1\dots y@n.P}, where P   700 is the result of printing p, and the x@i are replaced by y@i. The   701 latter are (possibly new) unique names.   702 \item {\tt Bound(i)} is printed as {\tt B.i} \footnote{The occurrence of   703 such loose'' bound variables indicates that either you are trying to   704 print a subterm of an abstraction, or there is something wrong with your   705 print translations.}.   706 \item The application {\ttt = Const(c,_)\$$t@1$\$\dots\$$t@n} (where   707 n may be 0!) is printed as follows:   708   709 If there is a pair (c,f) in tab, print f[t@1,\dots,t@n]. If this   710 application raises exception {\tt Match} or there is no pair (c,f) in   711 tab, let sy be the mixfix annotation associated with c. If there is   712 no such sy, or if sy does not have exactly n argument positions, t   713 is printed as an application; otherwise t is printed according to sy.   714   715 All other applications are printed as applications.   716 \end{itemize}   717 Printing a term {\tt c\$$t@1$\$\dots\t@n$} as an application means   718 printing it as {\tt$s$($s@1$,\dots,$s@n$)}, where$s@i$is the result of   719 printing$t@i$. If$c$is a {\tt Const},$s$is its first argument;   720 otherwise$s$is the result of printing$c$as described above.   721 \medskip   722   723 The printer also inserts parentheses where they are necessary for reasons   724 of precedence.   725   726 \section{Identifiers, constants, and type inference *}   727 \label{Typing}   728   729 There is one final step in the translation from strings to terms that we have   730 not covered yet. It explains how constants are distinguished from {\tt Free}s   731 and how {\tt Free}s and {\tt Var}s are typed. Both issues arise because {\tt   732 Free}s and {\tt Var}s are not declared.   733   734 An identifier$f$that does not appear as a delimiter in the concrete syntax   735 can be either a free variable or a constant. Since the parser knows only   736 about those constants which appear in mixfix annotations, it parses$f$as   737 {\tt Free("$f$",dummyT)}, where \ttindex{dummyT} is the predefined dummy {\tt   738 typ}. Although the parser produces these very raw terms, most user   739 interface level functions like {\tt goal} type terms according to the given   740 theory, say$T$. In a first step, every occurrence of {\tt Free($f$,_)} or   741 {\tt Const($f$,_)} is replaced by {\tt Const($f$,$\tau$)}, provided there is   742 a constant$f$of {\tt typ}$\tau$in$T$. This means that identifiers are   743 treated as {\tt Free}s iff they are not declared in the theory. The types of   744 the remaining {\tt Free}s (and {\tt Var}s) are inferred as in \ML. Type   745 constraints can be used to remove ambiguities.   746   747 One peculiarity of the current type inference algorithm is that variables   748 with the same name must have the same type, irrespective of whether they are   749 schematic, free or bound. For example, take the first-order formula$f(x) = x

   750 \land (\forall f.~ f=f)$where${=} :: [\alpha{::}term,\alpha]\To o$and   751$\forall :: (\alpha{::}term\To o)\To o$. The first conjunct forces   752$x::\alpha{::}term$and$f::\alpha\To\alpha$, the second one   753$f::\beta{::}term$. Although the two$f$'s are distinct, they are required to   754 have the same type. Unifying$\alpha\To\alpha$and$\beta{::}term$fails   755 because, in first-order logic, function types are not in class$term$.   756   757   758 \section{Putting it all together}   759   760 Having discussed the individual building blocks of a logic definition, it   761 remains to be shown how they fit together. In particular we need to say how   762 an object-logic syntax is hooked up to the meta-logic. Since all theorems   763 must conform to the syntax for$prop$(see Figure~\ref{MetaLogicSyntax}),   764 that syntax has to be extended with the object-level syntax. Assume that the   765 syntax of your object-logic defines a category$o$of formulae. These   766 formulae can now appear in axioms and theorems wherever$prop$does if you   767 add the production   768 $prop ~=~ form.$   769 More precisely, you need a coercion from formulae to propositions:   770 \begin{ttbox}   771 Base = Pure +   772 types o 0   773 arities o :: logic   774 consts Trueprop :: "o => prop" ("_" 5)   775 end   776 \end{ttbox}   777 The constant {\tt Trueprop} (the name is arbitrary) acts as an invisible   778 coercion function. Assuming this definition resides in a file {\tt base.thy},   779 you have to load it with the command {\tt use_thy"base"}.   780   781 One of the simplest nontrivial logics is {\em minimal logic} of   782 implication. Its definition in Isabelle needs no advanced features but   783 illustrates the overall mechanism quite nicely:   784 \begin{ttbox}   785 Hilbert = Base +   786 consts "-->" :: "[o,o] => o" (infixr 10)   787 rules   788 K "P --> Q --> P"   789 S "(P --> Q --> R) --> (P --> Q) --> P --> R"   790 MP "[| P --> Q; P |] ==> Q"   791 end   792 \end{ttbox}   793 After loading this definition you can start to prove theorems in this logic:   794 \begin{ttbox}   795 goal Hilbert.thy "P --> P";   796 {\out Level 0}   797 {\out P --> P}   798 {\out 1. P --> P}   799 by (resolve_tac [Hilbert.MP] 1);   800 {\out Level 1}   801 {\out P --> P}   802 {\out 1. ?P --> P --> P}   803 {\out 2. ?P}   804 by (resolve_tac [Hilbert.MP] 1);   805 {\out Level 2}   806 {\out P --> P}   807 {\out 1. ?P1 --> ?P --> P --> P}   808 {\out 2. ?P1}   809 {\out 3. ?P}   810 by (resolve_tac [Hilbert.S] 1);   811 {\out Level 3}   812 {\out P --> P}   813 {\out 1. P --> ?Q2 --> P}   814 {\out 2. P --> ?Q2}   815 by (resolve_tac [Hilbert.K] 1);   816 {\out Level 4}   817 {\out P --> P}   818 {\out 1. P --> ?Q2}   819 by (resolve_tac [Hilbert.K] 1);   820 {\out Level 5}   821 {\out P --> P}   822 {\out No subgoals!}   823 \end{ttbox}   824 As you can see, this Hilbert-style formulation of minimal logic is easy to   825 define but difficult to use. The following natural deduction formulation is   826 far preferable:   827 \begin{ttbox}   828 MinI = Base +   829 consts "-->" :: "[o,o] => o" (infixr 10)   830 rules   831 impI "(P ==> Q) ==> P --> Q"   832 impE "[| P --> Q; P |] ==> Q"   833 end   834 \end{ttbox}   835 Note, however, that although the two systems are equivalent, this fact cannot   836 be proved within Isabelle: {\tt S} and {\tt K} can be derived in \verb$MinI\$

   837 (exercise!), but {\tt impI} cannot be derived in \verb!Hilbert!.  The reason

   838 is that {\tt impI} is only an {\em admissible} rule in \verb!Hilbert!,

   839 something that can only be shown by induction over all possible proofs in

   840 \verb!Hilbert!.

   841

   842 It is a very simple matter to extend minimal logic with falsity:

   843 \begin{ttbox}

   844 MinIF = MinI +

   845 consts False :: "o"

   846 rules

   847 FalseE  "False ==> P"

   848 end

   849 \end{ttbox}

   850 On the other hand, we may wish to introduce conjunction only:

   851 \begin{ttbox}

   852 MinC = Base +

   853 consts "&" :: "[o,o] => o"  (infixr 30)

   854 rules

   855 conjI  "[| P; Q |] ==> P & Q"

   856 conjE1 "P & Q ==> P"

   857 conjE2 "P & Q ==> Q"

   858 end

   859 \end{ttbox}

   860 And if we want to have all three connectives together, we define:

   861 \begin{ttbox}

   862 MinIFC = MinIF + MinC

   863 \end{ttbox}

   864 Now we can prove mixed theorems like

   865 \begin{ttbox}

   866 goal MinIFC.thy "P & False --> Q";

   867 by (resolve_tac [MinI.impI] 1);

   868 by (dresolve_tac [MinC.conjE2] 1);

   869 by (eresolve_tac [MinIF.FalseE] 1);

   870 \end{ttbox}

   871 Try this as an exercise!