1%% THIS FILE IS COMMON TO ALL LOGIC MANUALS 2 3\chapter{Syntax definitions} 4The syntax of each logic is presented using a context-free grammar. 5These grammars obey the following conventions: 6\begin{itemize} 7\item identifiers denote nonterminal symbols 8\item \texttt{typewriter} font denotes terminal symbols 9\item parentheses $(\ldots)$ express grouping 10\item constructs followed by a Kleene star, such as $id^*$ and $(\ldots)^*$ 11can be repeated~0 or more times 12\item alternatives are separated by a vertical bar,~$|$ 13\item the symbol for alphanumeric identifiers is~{\it id\/} 14\item the symbol for scheme variables is~{\it var} 15\end{itemize} 16To reduce the number of nonterminals and grammar rules required, Isabelle's 17syntax module employs {\bf priorities},\index{priorities} or precedences. 18Each grammar rule is given by a mixfix declaration, which has a priority, 19and each argument place has a priority. This general approach handles 20infix operators that associate either to the left or to the right, as well 21as prefix and binding operators. 22 23In a syntactically valid expression, an operator's arguments never involve 24an operator of lower priority unless brackets are used. Consider 25first-order logic, where $\exists$ has lower priority than $\disj$, 26which has lower priority than $\conj$. There, $P\conj Q \disj R$ 27abbreviates $(P\conj Q) \disj R$ rather than $P\conj (Q\disj R)$. Also, 28$\exists x.P\disj Q$ abbreviates $\exists x.(P\disj Q)$ rather than 29$(\exists x.P)\disj Q$. Note especially that $P\disj(\exists x.Q)$ 30becomes syntactically invalid if the brackets are removed. 31 32A {\bf binder} is a symbol associated with a constant of type 33$(\sigma\To\tau)\To\tau'$. For instance, we may declare~$\forall$ as a binder 34for the constant~$All$, which has type $(\alpha\To o)\To o$. This defines the 35syntax $\forall x.t$ to mean $All(\lambda x.t)$. We can also write $\forall 36x@1\ldots x@m.t$ to abbreviate $\forall x@1. \ldots \forall x@m.t$; this is 37possible for any constant provided that $\tau$ and $\tau'$ are the same type. 38The Hilbert description operator $\varepsilon x.P\,x$ has type $(\alpha\To 39bool)\To\alpha$ and normally binds only one variable. 40ZF's bounded quantifier $\forall x\in A.P(x)$ cannot be declared as a 41binder because it has type $[i, i\To o]\To o$. The syntax for binders allows 42type constraints on bound variables, as in 43\[ \forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z) \] 44 45To avoid excess detail, the logic descriptions adopt a semi-formal style. 46Infix operators and binding operators are listed in separate tables, which 47include their priorities. Grammar descriptions do not include numeric 48priorities; instead, the rules appear in order of decreasing priority. 49This should suffice for most purposes; for full details, please consult the 50actual syntax definitions in the {\tt.thy} files. 51 52Each nonterminal symbol is associated with some Isabelle type. For 53example, the formulae of first-order logic have type~$o$. Every 54Isabelle expression of type~$o$ is therefore a formula. These include 55atomic formulae such as $P$, where $P$ is a variable of type~$o$, and more 56generally expressions such as $P(t,u)$, where $P$, $t$ and~$u$ have 57suitable types. Therefore, `expression of type~$o$' is listed as a 58separate possibility in the grammar for formulae. 59 60 61