summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Wed, 13 Jan 1999 16:30:53 +0100 | |

changeset 6120 | f40d61cd6b32 |

parent 6119 | 7e3eb9b4df8e |

child 6121 | 5fe77b9b5185 |

removal of FOL and ZF

doc-src/Logics/preface.tex | file | annotate | diff | comparison | revisions | |

doc-src/Logics/syntax.tex | file | annotate | diff | comparison | revisions |

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Logics/preface.tex Wed Jan 13 16:30:53 1999 +0100 @@ -0,0 +1,60 @@ +%% $Id$ +\chapter*{Preface} +Several logics come with Isabelle. Many of them are sufficiently developed +to serve as comfortable reasoning environments. They are also good +starting points for defining new logics. Each logic is distributed with +sample proofs, some of which are described in this document. + +The logics \texttt{FOL} (first-order logic) and \texttt{ZF} (axiomatic set +theory) are described in a separate manual~\cite{isabelle-ZF}. Here are the +others: + +\begin{ttdescription} +\item[\thydx{CCL}] is Martin Coen's Classical Computational Logic, + which is the basis of a preliminary method for deriving programs from + proofs~\cite{coen92}. It is built upon classical~\FOL{}. + +\item[\thydx{LCF}] is a version of Scott's Logic for Computable + Functions, which is also implemented by the~{\sc lcf} + system~\cite{paulson87}. It is built upon classical~\FOL{}. + +\item[\thydx{HOL}] is the higher-order logic of Church~\cite{church40}, +which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon-hol}. +This object-logic should not be confused with Isabelle's meta-logic, which is +also a form of higher-order logic. + +\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an + extension of \texttt{HOL}\@. + +\item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type +Theory~\cite{nordstrom90}, with extensional equality. Universes are not +included. + +\item[\thydx{Cube}] is Barendregt's $\lambda$-cube. + \end{ttdescription} + +The directory \texttt{Sequents} contains several logics based + upon the sequent calculus. Sequents have the form $A@1,\ldots,A@m\turn +B@1,\ldots,B@n$; rules are applied using associative matching. +\begin{ttdescription} +\item[\thydx{LK}] is classical first-order logic as a sequent calculus. + +\item[\thydx{Modal}] implements the modal logics $T$, $S4$, and~$S43$. + +\item[\thydx{ILL}] implements intuitionistic linear logic. +\end{ttdescription} + +The logics \texttt{CCL}, \texttt{LCF}, \texttt{HOLCF}, \texttt{Modal}, \texttt{ILL} and {\tt + Cube} are undocumented. All object-logics' sources are +distributed with Isabelle (see the directory \texttt{src}). They are +also available for browsing on the WWW at +\begin{ttbox} +http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/ +\end{ttbox} +Note that this is not necessarily consistent with your local sources! + +\medskip Do not read this manual before reading \emph{Introduction to + Isabelle} and performing some Isabelle proofs. Consult the {\em Reference + Manual} for more information on tactics, packages, etc. + +

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