1 %% $Id$ |
1 %% $Id$ |
2 \chapter{Introduction} |
2 \chapter{Basic Concepts} |
3 Several logics come with Isabelle. Many of them are sufficiently developed |
3 Several logics come with Isabelle. Many of them are sufficiently developed |
4 to serve as comfortable reasoning environments. They are also good |
4 to serve as comfortable reasoning environments. They are also good |
5 starting points for defining new logics. Each logic is distributed with |
5 starting points for defining new logics. Each logic is distributed with |
6 sample proofs, some of which are described in this document. |
6 sample proofs, some of which are described in this document. |
7 |
7 |
33 {\ttindexbold{LCF}} is a version of Scott's Logic for Computable Functions, |
33 {\ttindexbold{LCF}} is a version of Scott's Logic for Computable Functions, |
34 which is also implemented by the~{\sc lcf} system~\cite{paulson87}. |
34 which is also implemented by the~{\sc lcf} system~\cite{paulson87}. |
35 \end{quote} |
35 \end{quote} |
36 The logics {\tt Modal}, {\tt Cube} and {\tt LCF} are currently undocumented. |
36 The logics {\tt Modal}, {\tt Cube} and {\tt LCF} are currently undocumented. |
37 |
37 |
38 This manual assumes that you have read the {\em Introduction to Isabelle\/} |
38 You should not read this before reading {\em Introduction to Isabelle\/} |
39 and have some experience of using Isabelle to perform interactive proofs. |
39 and performing some Isabelle proofs. Consult the {\em Reference Manual} |
40 It refers to packages defined in the {\em Reference Manual}, which you |
40 for more information on tactics, packages, etc. |
41 should keep at hand. |
|
42 |
41 |
43 |
42 |
44 \section{Syntax definitions} |
43 \section{Syntax definitions} |
45 This manual defines each logic's syntax using a context-free grammar. |
44 The syntax of each logic syntax is defined using a context-free grammar. |
46 These grammars obey the following conventions: |
45 These grammars obey the following conventions: |
47 \begin{itemize} |
46 \begin{itemize} |
48 \item identifiers denote nonterminal symbols |
47 \item identifiers denote nonterminal symbols |
49 \item {\tt typewriter} font denotes terminal symbols |
48 \item {\tt typewriter} font denotes terminal symbols |
50 \item parentheses $(\ldots)$ express grouping |
49 \item parentheses $(\ldots)$ express grouping |