summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/Logics/syntax.tex

author | wenzelm |

Wed Jul 25 12:38:54 2012 +0200 (2012-07-25) | |

changeset 48497 | ba61aceaa18a |

parent 42637 | 381fdcab0f36 |

permissions | -rw-r--r-- |

some updates on "Building a repository version of Isabelle";

1 %% THIS FILE IS COMMON TO ALL LOGIC MANUALS

3 \chapter{Syntax definitions}

4 The syntax of each logic is presented using a context-free grammar.

5 These 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)^*$

11 can 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}

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

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

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

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

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

21 as prefix and binding operators.

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

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

25 first-order logic, where $\exists$ has lower priority than $\disj$,

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

27 abbreviates $(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)$

30 becomes syntactically invalid if the brackets are removed.

32 A {\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

34 for the constant~$All$, which has type $(\alpha\To o)\To o$. This defines the

35 syntax $\forall x.t$ to mean $All(\lambda x.t)$. We can also write $\forall

36 x@1\ldots x@m.t$ to abbreviate $\forall x@1. \ldots \forall x@m.t$; this is

37 possible for any constant provided that $\tau$ and $\tau'$ are the same type.

38 The Hilbert description operator $\varepsilon x.P\,x$ has type $(\alpha\To

39 bool)\To\alpha$ and normally binds only one variable.

40 ZF's bounded quantifier $\forall x\in A.P(x)$ cannot be declared as a

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

42 type constraints on bound variables, as in

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

45 To avoid excess detail, the logic descriptions adopt a semi-formal style.

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

47 include their priorities. Grammar descriptions do not include numeric

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

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

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

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

53 example, the formulae of first-order logic have type~$o$. Every

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

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

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

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

58 separate possibility in the grammar for formulae.