doc-src/Logics/syntax.tex
 author wenzelm Mon Aug 28 13:52:38 2000 +0200 (2000-08-28) changeset 9695 ec7d7f877712 parent 6120 f40d61cd6b32 child 14209 180cd69a5dbb permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
 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 context-free 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 first-order 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  wenzelm@9695  34 $(\sigma\To\tau)\To\tau'$. For instance, we may declare~$\forall$ as a binder  wenzelm@9695  35 for the constant~$All$, which has type $(\alpha\To o)\To o$. This defines the  wenzelm@9695  36 syntax $\forall x.t$ to mean $All(\lambda x.t)$. We can also write $\forall  wenzelm@9695  37 x@1\ldots x@m.t$ to abbreviate $\forall x@1. \ldots \forall x@m.t$; this is  wenzelm@9695  38 possible for any constant provided that $\tau$ and $\tau'$ are the same type.  wenzelm@9695  39 HOL's description operator $\varepsilon x.P\,x$ has type $(\alpha\To  wenzelm@9695  40 bool)\To\alpha$ and can bind only one variable, except when $\alpha$ is  wenzelm@9695  41 $bool$. ZF's bounded quantifier $\forall x\in A.P(x)$ cannot be declared as a  wenzelm@9695  42 binder because it has type $[i, i\To o]\To o$. The syntax for binders allows  paulson@6120  43 type constraints on bound variables, as in  paulson@6120  44 $\forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z)$  paulson@6120  45 paulson@6120  46 To avoid excess detail, the logic descriptions adopt a semi-formal style.  paulson@6120  47 Infix operators and binding operators are listed in separate tables, which  paulson@6120  48 include their priorities. Grammar descriptions do not include numeric  paulson@6120  49 priorities; instead, the rules appear in order of decreasing priority.  paulson@6120  50 This should suffice for most purposes; for full details, please consult the  paulson@6120  51 actual syntax definitions in the {\tt.thy} files.  paulson@6120  52 paulson@6120  53 Each nonterminal symbol is associated with some Isabelle type. For  paulson@6120  54 example, the formulae of first-order logic have type~$o$. Every  paulson@6120  55 Isabelle expression of type~$o$ is therefore a formula. These include  paulson@6120  56 atomic formulae such as $P$, where $P$ is a variable of type~$o$, and more  paulson@6120  57 generally expressions such as $P(t,u)$, where $P$, $t$ and~$u$ have  paulson@6120  58 suitable types. Therefore, expression of type~$o$' is listed as a  paulson@6120  59 separate possibility in the grammar for formulae.  paulson@6120  60 paulson@6120  61`