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