1 \chapter*{Preface} |
1 \chapter*{Preface} |
2 \markboth{Preface}{Preface} %or Preface ? |
2 \markboth{Preface}{Preface} %or Preface ? |
3 \addcontentsline{toc}{chapter}{Preface} |
3 \addcontentsline{toc}{chapter}{Preface} |
4 |
4 |
5 \index{Isabelle!object-logics supported} |
|
6 |
|
7 Most theorem provers support a fixed logic, such as first-order or |
5 Most theorem provers support a fixed logic, such as first-order or |
8 equational logic. They bring sophisticated proof procedures to bear upon |
6 equational logic. They bring sophisticated proof procedures to bear upon |
9 the conjectured formula. The resolution prover Otter~\cite{wos-bledsoe} is |
7 the conjectured formula. The resolution prover Otter~\cite{wos-bledsoe} is |
10 an impressive example. ALF~\cite{alf}, Coq~\cite{coq} and |
8 an impressive example. |
11 Nuprl~\cite{constable86} each support a fixed logic too, but one far |
|
12 removed from first-order logic. They are explicitly concerned with |
|
13 computation. A diverse collection of logics --- type theories, process |
|
14 calculi, $\lambda$-calculi --- may be found in the Computer Science |
|
15 literature. Such logics require proof support. Few proof procedures are |
|
16 known for them, but the theorem prover can at least automate routine steps. |
|
17 |
9 |
18 A {\bf generic} theorem prover is one that can support a variety of logics. |
10 {\sc alf}~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each |
|
11 support a fixed logic too. These are higher-order type theories, |
|
12 explicitly concerned with computation and capable of expressing |
|
13 developments in constructive mathematics. They are far removed from |
|
14 classical first-order logic. |
|
15 |
|
16 A diverse collection of logics --- type theories, process calculi, |
|
17 $\lambda$-calculi --- may be found in the Computer Science literature. |
|
18 Such logics require proof support. Few proof procedures are known for |
|
19 them, but the theorem prover can at least automate routine steps. |
|
20 |
|
21 A {\bf generic} theorem prover is one that supports a variety of logics. |
19 Some generic provers are noteworthy for their user interfaces |
22 Some generic provers are noteworthy for their user interfaces |
20 \cite{dawson90,mural,sawamura92}. Most of them work by implementing a |
23 \cite{dawson90,mural,sawamura92}. Most of them work by implementing a |
21 syntactic framework that can express typical inference rules. Isabelle's |
24 syntactic framework that can express typical inference rules. Isabelle's |
22 distinctive feature is its representation of logics within a fragment of |
25 distinctive feature is its representation of logics within a fragment of |
23 higher-order logic, called the meta-logic. The proof theory of |
26 higher-order logic, called the meta-logic. The proof theory of |
33 language and a fully automatic search would be impractical. Isabelle does |
36 language and a fully automatic search would be impractical. Isabelle does |
34 not resolve clauses automatically, but under user direction. You can |
37 not resolve clauses automatically, but under user direction. You can |
35 conduct single-step proofs, use Isabelle's built-in proof procedures, or |
38 conduct single-step proofs, use Isabelle's built-in proof procedures, or |
36 develop new proof procedures using tactics and tacticals. |
39 develop new proof procedures using tactics and tacticals. |
37 |
40 |
38 Isabelle's meta-logic is higher-order, based on the typed |
41 Isabelle's meta-logic is higher-order, based on the simply typed |
39 $\lambda$-calculus. So resolution cannot use ordinary unification, but |
42 $\lambda$-calculus. So resolution cannot use ordinary unification, but |
40 higher-order unification~\cite{huet75}. This complicated procedure gives |
43 higher-order unification~\cite{huet75}. This complicated procedure gives |
41 Isabelle strong support for many logical formalisms involving variable |
44 Isabelle strong support for many logical formalisms involving variable |
42 binding. |
45 binding. |
43 |
46 |
44 The diagram below illustrates some of the logics distributed with Isabelle. |
47 The diagram below illustrates some of the logics distributed with Isabelle. |
45 These include first-order logic (intuitionistic and classical), the sequent |
48 These include first-order logic (intuitionistic and classical), the sequent |
46 calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72}, |
49 calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72}, |
47 a version of Constructive Type Theory~\cite{nordstrom90}, several modal |
50 a version of Constructive Type Theory~\cite{nordstrom90}, several modal |
48 logics, and a Logic for Computable Functions. Several experimental |
51 logics, and a Logic for Computable Functions. Several experimental logics |
49 logics are also available, such a term assignment calculus for linear |
52 are being developed, such as linear logic. |
50 logic. |
|
51 |
53 |
52 \centerline{\epsfbox{Isa-logics.eps}} |
54 \centerline{\epsfbox{Isa-logics.eps}} |
53 |
55 |
54 |
56 |
55 \section*{How to read this book} |
57 \section*{How to read this book} |
75 about Isabelle's facilities, excluding the object-logics. This part |
77 about Isabelle's facilities, excluding the object-logics. This part |
76 would make boring reading, though browsing might be useful. Mostly you |
78 would make boring reading, though browsing might be useful. Mostly you |
77 should use it to locate facts quickly. |
79 should use it to locate facts quickly. |
78 |
80 |
79 \item {\em Isabelle's Object-Logics\/} describes the various logics |
81 \item {\em Isabelle's Object-Logics\/} describes the various logics |
80 distributed with Isabelle. Its final chapter explains how to define new |
82 distributed with Isabelle. The chapters are intended for reference only; |
81 logics. The other chapters are intended for reference only. |
83 they overlap somewhat so that each chapter can be read in isolation. |
82 \end{itemize} |
84 \end{itemize} |
83 This book should not be read from start to finish. Instead you might read |
85 This book should not be read from start to finish. Instead you might read |
84 a couple of chapters from {\em Introduction to Isabelle}, then try some |
86 a couple of chapters from {\em Introduction to Isabelle}, then try some |
85 examples referring to the other parts, return to the {\em Introduction}, |
87 examples referring to the other parts, return to the {\em Introduction}, |
86 and so forth. Starred sections discuss obscure matters and may be skipped |
88 and so forth. Starred sections discuss obscure matters and may be skipped |
87 on a first reading. |
89 on a first reading. |
88 |
90 |
89 |
91 |
90 |
92 |
91 \section*{Releases of Isabelle}\index{Isabelle!release history} |
93 \section*{Releases of Isabelle} |
92 Isabelle was first distributed in 1986. The 1987 version introduced a |
94 Isabelle was first distributed in 1986. The 1987 version introduced a |
93 higher-order meta-logic with an improved treatment of quantifiers. The |
95 higher-order meta-logic with an improved treatment of quantifiers. The |
94 1988 version added limited polymorphism and support for natural deduction. |
96 1988 version added limited polymorphism and support for natural deduction. |
95 The 1989 version included a parser and pretty printer generator. The 1992 |
97 The 1989 version included a parser and pretty printer generator. The 1992 |
96 version introduced type classes, to support many-sorted and higher-order |
98 version introduced type classes, to support many-sorted and higher-order |
123 implemented the theory database; Markus Wenzel implemented macros; Sonia |
125 implemented the theory database; Markus Wenzel implemented macros; Sonia |
124 Mahjoub and Karin Nimmermann also contributed. |
126 Mahjoub and Karin Nimmermann also contributed. |
125 |
127 |
126 Nipkow and his students wrote much of the documentation underlying this |
128 Nipkow and his students wrote much of the documentation underlying this |
127 book. Nipkow wrote the first versions of \S\ref{sec:defining-theories}, |
129 book. Nipkow wrote the first versions of \S\ref{sec:defining-theories}, |
128 \S\ref{sec:ref-defining-theories}, Chap.\ts\ref{simp-chap}, |
130 \S\ref{sec:ref-defining-theories}, Chap.\ts\ref{Defining-Logics}, |
129 Chap.\ts\ref{Defining-Logics} and App.\ts\ref{app:TheorySyntax}\@. Carsten |
131 Chap.\ts\ref{simp-chap} and App.\ts\ref{app:TheorySyntax}\@. Carsten |
130 Clasohm contributed to Chap.\ts\ref{theories}. Markus Wenzel contributed |
132 Clasohm contributed to Chap.\ts\ref{theories}. Markus Wenzel contributed |
131 to Chap.\ts\ref{Defining-Logics}. |
133 to Chap.\ts\ref{chap:syntax}. Nipkow also provided the quotation at |
|
134 the front. |
132 |
135 |
133 David Aspinall, Sara Kalvala, Ina Kraan, Zhenyu Qian, Norbert V{\"o}lker and |
136 David Aspinall, Sara Kalvala, Ina Kraan, Chris Owens, Zhenyu Qian, Norbert |
134 Markus Wenzel suggested changes and corrections to the documentation. |
137 V{\"o}lker and Markus Wenzel suggested changes and corrections to the |
|
138 documentation. |
135 |
139 |
136 Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped |
140 Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped |
137 to develop Isabelle's standard object-logics. David Aspinall performed |
141 to develop Isabelle's standard object-logics. David Aspinall performed |
138 some useful research into theories and implemented an Isabelle Emacs mode. |
142 some useful research into theories and implemented an Isabelle Emacs mode. |
139 Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler, |
143 Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler, |
140 Poly/{\sc ml}. |
144 Poly/{\sc ml}. |
141 |
145 |
142 The research has been funded by numerous SERC grants dating from the Alvey |
146 The research has been funded by numerous SERC grants dating from the Alvey |
143 programme (grants GR/E0355.7, GR/G53279, GR/H40570) and by ESPRIT (projects |
147 programme (grants GR/E0355.7, GR/G53279, GR/H40570) and by ESPRIT (projects |
144 3245: Logical Frameworks and 6453: Types). |
148 3245: Logical Frameworks and 6453: Types). |
145 |
|
146 |
|
147 \index{ML} |
|