author paulson Wed Jan 13 16:30:53 1999 +0100 (1999-01-13) changeset 6120 f40d61cd6b32 parent 6119 7e3eb9b4df8e child 6121 5fe77b9b5185
removal of FOL and ZF
 doc-src/Logics/preface.tex file | annotate | diff | revisions doc-src/Logics/syntax.tex file | annotate | diff | revisions
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/Logics/preface.tex	Wed Jan 13 16:30:53 1999 +0100
1.3 @@ -0,0 +1,60 @@
1.4 +%% $Id$
1.5 +\chapter*{Preface}
1.6 +Several logics come with Isabelle.  Many of them are sufficiently developed
1.7 +to serve as comfortable reasoning environments.  They are also good
1.8 +starting points for defining new logics.  Each logic is distributed with
1.9 +sample proofs, some of which are described in this document.
1.10 +
1.11 +The logics \texttt{FOL} (first-order logic) and \texttt{ZF} (axiomatic set
1.12 +theory) are described in a separate manual~\cite{isabelle-ZF}.  Here are the
1.13 +others:
1.14 +
1.15 +\begin{ttdescription}
1.16 +\item[\thydx{CCL}] is Martin Coen's Classical Computational Logic,
1.17 +  which is the basis of a preliminary method for deriving programs from
1.18 +  proofs~\cite{coen92}.  It is built upon classical~\FOL{}.
1.19 +
1.20 +\item[\thydx{LCF}] is a version of Scott's Logic for Computable
1.21 +  Functions, which is also implemented by the~{\sc lcf}
1.22 +  system~\cite{paulson87}.  It is built upon classical~\FOL{}.
1.23 +
1.24 +\item[\thydx{HOL}] is the higher-order logic of Church~\cite{church40},
1.25 +which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon-hol}.
1.26 +This object-logic should not be confused with Isabelle's meta-logic, which is
1.27 +also a form of higher-order logic.
1.28 +
1.29 +\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an
1.30 +  extension of \texttt{HOL}\@.
1.31 +
1.32 +\item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type
1.33 +Theory~\cite{nordstrom90}, with extensional equality.  Universes are not
1.34 +included.
1.35 +
1.36 +\item[\thydx{Cube}] is Barendregt's $\lambda$-cube.
1.37 + \end{ttdescription}
1.38 +
1.39 +The directory \texttt{Sequents} contains several logics based
1.40 +  upon the sequent calculus.  Sequents have the form $A@1,\ldots,A@m\turn 1.41 +B@1,\ldots,B@n$; rules are applied using associative matching.
1.42 +\begin{ttdescription}
1.43 +\item[\thydx{LK}] is classical first-order logic as a sequent calculus.
1.44 +
1.45 +\item[\thydx{Modal}] implements the modal logics $T$, $S4$, and~$S43$.
1.46 +
1.47 +\item[\thydx{ILL}] implements intuitionistic linear logic.
1.48 +\end{ttdescription}
1.49 +
1.50 +The logics \texttt{CCL}, \texttt{LCF}, \texttt{HOLCF}, \texttt{Modal}, \texttt{ILL} and {\tt
1.51 +  Cube} are undocumented.  All object-logics' sources are
1.52 +distributed with Isabelle (see the directory \texttt{src}).  They are
1.53 +also available for browsing on the WWW at
1.54 +\begin{ttbox}
1.55 +http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
1.56 +\end{ttbox}
1.57 +Note that this is not necessarily consistent with your local sources!
1.58 +
1.60 +  Isabelle} and performing some Isabelle proofs.  Consult the {\em Reference
1.62 +
1.63 +

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/Logics/syntax.tex	Wed Jan 13 16:30:53 1999 +0100
2.3 @@ -0,0 +1,62 @@
2.4 +%% $Id$
2.5 +%% THIS FILE IS COMMON TO ALL LOGIC MANUALS
2.6 +
2.7 +\chapter{Syntax definitions}
2.8 +The syntax of each logic is presented using a context-free grammar.
2.9 +These grammars obey the following conventions:
2.10 +\begin{itemize}
2.11 +\item identifiers denote nonterminal symbols
2.12 +\item \texttt{typewriter} font denotes terminal symbols
2.13 +\item parentheses $(\ldots)$ express grouping
2.14 +\item constructs followed by a Kleene star, such as $id^*$ and $(\ldots)^*$
2.15 +can be repeated~0 or more times
2.16 +\item alternatives are separated by a vertical bar,~$|$
2.17 +\item the symbol for alphanumeric identifiers is~{\it id\/}
2.18 +\item the symbol for scheme variables is~{\it var}
2.19 +\end{itemize}
2.20 +To reduce the number of nonterminals and grammar rules required, Isabelle's
2.21 +syntax module employs {\bf priorities},\index{priorities} or precedences.
2.22 +Each grammar rule is given by a mixfix declaration, which has a priority,
2.23 +and each argument place has a priority.  This general approach handles
2.24 +infix operators that associate either to the left or to the right, as well
2.25 +as prefix and binding operators.
2.26 +
2.27 +In a syntactically valid expression, an operator's arguments never involve
2.28 +an operator of lower priority unless brackets are used.  Consider
2.29 +first-order logic, where $\exists$ has lower priority than $\disj$,
2.30 +which has lower priority than $\conj$.  There, $P\conj Q \disj R$
2.31 +abbreviates $(P\conj Q) \disj R$ rather than $P\conj (Q\disj R)$.  Also,
2.32 +$\exists x.P\disj Q$ abbreviates $\exists x.(P\disj Q)$ rather than
2.33 +$(\exists x.P)\disj Q$.  Note especially that $P\disj(\exists x.Q)$
2.34 +becomes syntactically invalid if the brackets are removed.
2.35 +
2.36 +A {\bf binder} is a symbol associated with a constant of type
2.37 +$(\sigma\To\tau)\To\tau'$.  For instance, we may declare~$\forall$ as
2.38 +a binder for the constant~$All$, which has type $(\alpha\To o)\To o$.
2.39 +This defines the syntax $\forall x.t$ to mean $All(\lambda x.t)$.  We
2.40 +can also write $\forall x@1\ldots x@m.t$ to abbreviate $\forall x@1. 2.41 +\ldots \forall x@m.t$; this is possible for any constant provided that
2.42 +$\tau$ and $\tau'$ are the same type.  \HOL's description operator
2.43 +$\varepsilon x.P\,x$ has type $(\alpha\To bool)\To\alpha$ and can bind
2.44 +only one variable, except when $\alpha$ is $bool$.  \ZF's bounded
2.45 +quantifier $\forall x\in A.P(x)$ cannot be declared as a binder
2.46 +because it has type $[i, i\To o]\To o$.  The syntax for binders allows
2.47 +type constraints on bound variables, as in
2.48 +$\forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z)$
2.49 +
2.50 +To avoid excess detail, the logic descriptions adopt a semi-formal style.
2.51 +Infix operators and binding operators are listed in separate tables, which
2.52 +include their priorities.  Grammar descriptions do not include numeric
2.53 +priorities; instead, the rules appear in order of decreasing priority.
2.54 +This should suffice for most purposes; for full details, please consult the
2.55 +actual syntax definitions in the {\tt.thy} files.
2.56 +
2.57 +Each nonterminal symbol is associated with some Isabelle type.  For
2.58 +example, the formulae of first-order logic have type~$o$.  Every
2.59 +Isabelle expression of type~$o$ is therefore a formula.  These include
2.60 +atomic formulae such as $P$, where $P$ is a variable of type~$o$, and more
2.61 +generally expressions such as $P(t,u)$, where $P$, $t$ and~$u$ have
2.62 +suitable types.  Therefore, expression of type~$o$' is listed as a
2.63 +separate possibility in the grammar for formulae.
2.64 +
2.65 +
`