doc-src/Logics/syntax.tex
changeset 6120 f40d61cd6b32
child 9695 ec7d7f877712
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/Logics/syntax.tex	Wed Jan 13 16:30:53 1999 +0100
     1.3 @@ -0,0 +1,62 @@
     1.4 +%% $Id$
     1.5 +%% THIS FILE IS COMMON TO ALL LOGIC MANUALS
     1.6 +
     1.7 +\chapter{Syntax definitions}
     1.8 +The syntax of each logic is presented using a context-free grammar.
     1.9 +These grammars obey the following conventions:
    1.10 +\begin{itemize}
    1.11 +\item identifiers denote nonterminal symbols
    1.12 +\item \texttt{typewriter} font denotes terminal symbols
    1.13 +\item parentheses $(\ldots)$ express grouping
    1.14 +\item constructs followed by a Kleene star, such as $id^*$ and $(\ldots)^*$
    1.15 +can be repeated~0 or more times 
    1.16 +\item alternatives are separated by a vertical bar,~$|$
    1.17 +\item the symbol for alphanumeric identifiers is~{\it id\/} 
    1.18 +\item the symbol for scheme variables is~{\it var}
    1.19 +\end{itemize}
    1.20 +To reduce the number of nonterminals and grammar rules required, Isabelle's
    1.21 +syntax module employs {\bf priorities},\index{priorities} or precedences.
    1.22 +Each grammar rule is given by a mixfix declaration, which has a priority,
    1.23 +and each argument place has a priority.  This general approach handles
    1.24 +infix operators that associate either to the left or to the right, as well
    1.25 +as prefix and binding operators.
    1.26 +
    1.27 +In a syntactically valid expression, an operator's arguments never involve
    1.28 +an operator of lower priority unless brackets are used.  Consider
    1.29 +first-order logic, where $\exists$ has lower priority than $\disj$,
    1.30 +which has lower priority than $\conj$.  There, $P\conj Q \disj R$
    1.31 +abbreviates $(P\conj Q) \disj R$ rather than $P\conj (Q\disj R)$.  Also,
    1.32 +$\exists x.P\disj Q$ abbreviates $\exists x.(P\disj Q)$ rather than
    1.33 +$(\exists x.P)\disj Q$.  Note especially that $P\disj(\exists x.Q)$
    1.34 +becomes syntactically invalid if the brackets are removed.
    1.35 +
    1.36 +A {\bf binder} is a symbol associated with a constant of type
    1.37 +$(\sigma\To\tau)\To\tau'$.  For instance, we may declare~$\forall$ as
    1.38 +a binder for the constant~$All$, which has type $(\alpha\To o)\To o$.
    1.39 +This defines the syntax $\forall x.t$ to mean $All(\lambda x.t)$.  We
    1.40 +can also write $\forall x@1\ldots x@m.t$ to abbreviate $\forall x@1.
    1.41 +\ldots \forall x@m.t$; this is possible for any constant provided that
    1.42 +$\tau$ and $\tau'$ are the same type.  \HOL's description operator
    1.43 +$\varepsilon x.P\,x$ has type $(\alpha\To bool)\To\alpha$ and can bind
    1.44 +only one variable, except when $\alpha$ is $bool$.  \ZF's bounded
    1.45 +quantifier $\forall x\in A.P(x)$ cannot be declared as a binder
    1.46 +because it has type $[i, i\To o]\To o$.  The syntax for binders allows
    1.47 +type constraints on bound variables, as in
    1.48 +\[ \forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z) \]
    1.49 +
    1.50 +To avoid excess detail, the logic descriptions adopt a semi-formal style.
    1.51 +Infix operators and binding operators are listed in separate tables, which
    1.52 +include their priorities.  Grammar descriptions do not include numeric
    1.53 +priorities; instead, the rules appear in order of decreasing priority.
    1.54 +This should suffice for most purposes; for full details, please consult the
    1.55 +actual syntax definitions in the {\tt.thy} files.
    1.56 +
    1.57 +Each nonterminal symbol is associated with some Isabelle type.  For
    1.58 +example, the formulae of first-order logic have type~$o$.  Every
    1.59 +Isabelle expression of type~$o$ is therefore a formula.  These include
    1.60 +atomic formulae such as $P$, where $P$ is a variable of type~$o$, and more
    1.61 +generally expressions such as $P(t,u)$, where $P$, $t$ and~$u$ have
    1.62 +suitable types.  Therefore, `expression of type~$o$' is listed as a
    1.63 +separate possibility in the grammar for formulae.
    1.64 +
    1.65 +