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