paulson@6120

1 
%% $Id$

paulson@6120

2 
%% THIS FILE IS COMMON TO ALL LOGIC MANUALS

paulson@6120

3 

paulson@6120

4 
\chapter{Syntax definitions}

paulson@6120

5 
The syntax of each logic is presented using a contextfree grammar.

paulson@6120

6 
These grammars obey the following conventions:

paulson@6120

7 
\begin{itemize}

paulson@6120

8 
\item identifiers denote nonterminal symbols

paulson@6120

9 
\item \texttt{typewriter} font denotes terminal symbols

paulson@6120

10 
\item parentheses $(\ldots)$ express grouping

paulson@6120

11 
\item constructs followed by a Kleene star, such as $id^*$ and $(\ldots)^*$

paulson@6120

12 
can be repeated~0 or more times

paulson@6120

13 
\item alternatives are separated by a vertical bar,~$$

paulson@6120

14 
\item the symbol for alphanumeric identifiers is~{\it id\/}

paulson@6120

15 
\item the symbol for scheme variables is~{\it var}

paulson@6120

16 
\end{itemize}

paulson@6120

17 
To reduce the number of nonterminals and grammar rules required, Isabelle's

paulson@6120

18 
syntax module employs {\bf priorities},\index{priorities} or precedences.

paulson@6120

19 
Each grammar rule is given by a mixfix declaration, which has a priority,

paulson@6120

20 
and each argument place has a priority. This general approach handles

paulson@6120

21 
infix operators that associate either to the left or to the right, as well

paulson@6120

22 
as prefix and binding operators.

paulson@6120

23 

paulson@6120

24 
In a syntactically valid expression, an operator's arguments never involve

paulson@6120

25 
an operator of lower priority unless brackets are used. Consider

paulson@6120

26 
firstorder logic, where $\exists$ has lower priority than $\disj$,

paulson@6120

27 
which has lower priority than $\conj$. There, $P\conj Q \disj R$

paulson@6120

28 
abbreviates $(P\conj Q) \disj R$ rather than $P\conj (Q\disj R)$. Also,

paulson@6120

29 
$\exists x.P\disj Q$ abbreviates $\exists x.(P\disj Q)$ rather than

paulson@6120

30 
$(\exists x.P)\disj Q$. Note especially that $P\disj(\exists x.Q)$

paulson@6120

31 
becomes syntactically invalid if the brackets are removed.

paulson@6120

32 

paulson@6120

33 
A {\bf binder} is a symbol associated with a constant of type

paulson@6120

34 
$(\sigma\To\tau)\To\tau'$. For instance, we may declare~$\forall$ as

paulson@6120

35 
a binder for the constant~$All$, which has type $(\alpha\To o)\To o$.

paulson@6120

36 
This defines the syntax $\forall x.t$ to mean $All(\lambda x.t)$. We

paulson@6120

37 
can also write $\forall x@1\ldots x@m.t$ to abbreviate $\forall x@1.

paulson@6120

38 
\ldots \forall x@m.t$; this is possible for any constant provided that

paulson@6120

39 
$\tau$ and $\tau'$ are the same type. \HOL's description operator

paulson@6120

40 
$\varepsilon x.P\,x$ has type $(\alpha\To bool)\To\alpha$ and can bind

paulson@6120

41 
only one variable, except when $\alpha$ is $bool$. \ZF's bounded

paulson@6120

42 
quantifier $\forall x\in A.P(x)$ cannot be declared as a binder

paulson@6120

43 
because it has type $[i, i\To o]\To o$. The syntax for binders allows

paulson@6120

44 
type constraints on bound variables, as in

paulson@6120

45 
\[ \forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z) \]

paulson@6120

46 

paulson@6120

47 
To avoid excess detail, the logic descriptions adopt a semiformal style.

paulson@6120

48 
Infix operators and binding operators are listed in separate tables, which

paulson@6120

49 
include their priorities. Grammar descriptions do not include numeric

paulson@6120

50 
priorities; instead, the rules appear in order of decreasing priority.

paulson@6120

51 
This should suffice for most purposes; for full details, please consult the

paulson@6120

52 
actual syntax definitions in the {\tt.thy} files.

paulson@6120

53 

paulson@6120

54 
Each nonterminal symbol is associated with some Isabelle type. For

paulson@6120

55 
example, the formulae of firstorder logic have type~$o$. Every

paulson@6120

56 
Isabelle expression of type~$o$ is therefore a formula. These include

paulson@6120

57 
atomic formulae such as $P$, where $P$ is a variable of type~$o$, and more

paulson@6120

58 
generally expressions such as $P(t,u)$, where $P$, $t$ and~$u$ have

paulson@6120

59 
suitable types. Therefore, `expression of type~$o$' is listed as a

paulson@6120

60 
separate possibility in the grammar for formulae.

paulson@6120

61 

paulson@6120

62 
