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

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 +