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.59 +\medskip Do not read this manual before reading \emph{Introduction to 1.60 + Isabelle} and performing some Isabelle proofs. Consult the {\em Reference 1.61 + Manual} for more information on tactics, packages, etc. 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 +