4 |
4 |
5 \index{Isabelle!object-logics supported} |
5 \index{Isabelle!object-logics supported} |
6 |
6 |
7 Most theorem provers support a fixed logic, such as first-order or |
7 Most theorem provers support a fixed logic, such as first-order or |
8 equational logic. They bring sophisticated proof procedures to bear upon |
8 equational logic. They bring sophisticated proof procedures to bear upon |
9 the conjectured formula. An impressive example is the resolution prover |
9 the conjectured formula. The resolution prover Otter~\cite{wos-bledsoe} is |
10 Otter, which Quaife~\cite{quaife-book} has used to formalize a body of |
10 an impressive example. ALF~\cite{alf}, Coq~\cite{coq} and |
11 mathematics. |
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. |
12 |
17 |
13 ALF~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each support a |
18 A {\bf generic} theorem prover is one that can support a variety of logics. |
14 fixed logic too, but one far removed from first-order logic. They are |
19 Some generic provers are noteworthy for their user interfaces |
15 explicitly concerned with computation. A diverse collection of logics --- |
20 \cite{dawson90,mural,sawamura92}. Most of them work by implementing a |
16 type theories, process calculi, $\lambda$-calculi --- may be found in the |
21 syntactic framework that can express typical inference rules. Isabelle's |
17 Computer Science literature. Such logics require proof support. Few proof |
22 distinctive feature is its representation of logics within a fragment of |
18 procedures exist, but the theorem prover can at least check that each |
23 higher-order logic, called the meta-logic. The proof theory of |
19 inference is valid. |
24 higher-order logic may be used to demonstrate that the representation is |
20 |
25 correct~\cite{paulson89}. The approach has much in common with the |
21 A {\bf generic} theorem prover is one that can support many different |
26 Edinburgh Logical Framework~\cite{harper-jacm} and with |
22 logics. Most of these \cite{dawson90,mural,sawamura92} work by |
|
23 implementing a syntactic framework that can express the features of typical |
|
24 inference rules. Isabelle's distinctive feature is its representation of |
|
25 logics using a meta-logic. This meta-logic is just a fragment of |
|
26 higher-order logic; known proof theory may be used to demonstrate that the |
|
27 representation is correct~\cite{paulson89}. The representation has much in |
|
28 common with the Edinburgh Logical Framework~\cite{harper-jacm} and with |
|
29 Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics. |
27 Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics. |
30 |
28 |
31 An inference rule in Isabelle is a generalized Horn clause. Rules are |
29 An inference rule in Isabelle is a generalized Horn clause. Rules are |
32 joined to make proofs by resolving such clauses. Logical variables in |
30 joined to make proofs by resolving such clauses. Logical variables in |
33 goals can be instantiated incrementally. But Isabelle is not a resolution |
31 goals can be instantiated incrementally. But Isabelle is not a resolution |
34 theorem prover like Otter. Isabelle's clauses are drawn from a richer, |
32 theorem prover like Otter. Isabelle's clauses are drawn from a richer |
35 higher-order language and a fully automatic search would be impractical. |
33 language and a fully automatic search would be impractical. Isabelle does |
36 Isabelle does not join clauses automatically, but under strict user |
34 not resolve clauses automatically, but under user direction. You can |
37 control. You can conduct single-step proofs, use Isabelle's built-in proof |
35 conduct single-step proofs, use Isabelle's built-in proof procedures, or |
38 procedures, or develop new proof procedures using tactics and tacticals. |
36 develop new proof procedures using tactics and tacticals. |
39 |
37 |
40 Isabelle's meta-logic is higher-order, based on the typed |
38 Isabelle's meta-logic is higher-order, based on the typed |
41 $\lambda$-calculus. So resolution cannot use ordinary unification, but |
39 $\lambda$-calculus. So resolution cannot use ordinary unification, but |
42 higher-order unification~\cite{huet75}. This complicated procedure gives |
40 higher-order unification~\cite{huet75}. This complicated procedure gives |
43 Isabelle strong support for many logical formalisms involving variable |
41 Isabelle strong support for many logical formalisms involving variable |
53 |
51 |
54 \centerline{\epsfbox{Isa-logics.eps}} |
52 \centerline{\epsfbox{Isa-logics.eps}} |
55 |
53 |
56 |
54 |
57 \section*{How to read this book} |
55 \section*{How to read this book} |
58 Isabelle is a large system, but beginners can get by with a few commands |
56 Isabelle is a complex system, but beginners can get by with a few commands |
59 and a basic knowledge of how Isabelle works. Some knowledge of |
57 and a basic knowledge of how Isabelle works. Some knowledge of |
60 Standard~\ML{} is essential because \ML{} is Isabelle's user interface. |
58 Standard~\ML{} is essential because \ML{} is Isabelle's user interface. |
61 Advanced Isabelle theorem proving can involve writing \ML{} code, possibly |
59 Advanced Isabelle theorem proving can involve writing \ML{} code, possibly |
62 with Isabelle's sources at hand. My book on~\ML{}~\cite{paulson91} covers |
60 with Isabelle's sources at hand. My book on~\ML{}~\cite{paulson91} covers |
63 much material connected with Isabelle, including a simple theorem prover. |
61 much material connected with Isabelle, including a simple theorem prover. |
71 describes Isabelle's meta-logic in some detail. The other chapters |
69 describes Isabelle's meta-logic in some detail. The other chapters |
72 present on-line sessions of increasing difficulty. It also explains how |
70 present on-line sessions of increasing difficulty. It also explains how |
73 to derive rules define theories, and concludes with an extended example: |
71 to derive rules define theories, and concludes with an extended example: |
74 a Prolog interpreter. |
72 a Prolog interpreter. |
75 |
73 |
76 \item {\em The Isabelle Reference Manual\/} contains information about most |
74 \item {\em The Isabelle Reference Manual\/} provides detailed information |
77 of the facilities of Isabelle, apart from particular object-logics. This |
75 about Isabelle's facilities, excluding the object-logics. This part |
78 part would make boring reading, though browsing might be useful. Mostly |
76 would make boring reading, though browsing might be useful. Mostly you |
79 you should use it to locate facts quickly. |
77 should use it to locate facts quickly. |
80 |
78 |
81 \item {\em Isabelle's Object-Logics\/} describes the various logics |
79 \item {\em Isabelle's Object-Logics\/} describes the various logics |
82 distributed with Isabelle. Its final chapter explains how to define new |
80 distributed with Isabelle. Its final chapter explains how to define new |
83 logics. The other chapters are intended for reference only. |
81 logics. The other chapters are intended for reference only. |
84 \end{itemize} |
82 \end{itemize} |
116 \end{itemize} |
114 \end{itemize} |
117 My electronic mail address is {\tt lcp\at cl.cam.ac.uk}. Please report any |
115 My electronic mail address is {\tt lcp\at cl.cam.ac.uk}. Please report any |
118 errors you find in this book and your problems or successes with Isabelle. |
116 errors you find in this book and your problems or successes with Isabelle. |
119 |
117 |
120 |
118 |
121 \subsection*{Acknowledgements} |
119 \section*{Acknowledgements} |
122 Tobias Nipkow has made immense contributions to Isabelle, including the |
120 Tobias Nipkow has made immense contributions to Isabelle, including the |
123 parser generator, type classes, the simplifier, and several object-logics. |
121 parser generator, type classes, the simplifier, and several object-logics. |
124 He also arranged for several of his students to help. Carsten Clasohm |
122 He also arranged for several of his students to help. Carsten Clasohm |
125 implemented the theory database; Markus Wenzel implemented macros; Sonia |
123 implemented the theory database; Markus Wenzel implemented macros; Sonia |
126 Mahjoub and Karin Nimmermann also contributed. |
124 Mahjoub and Karin Nimmermann also contributed. |
127 |
125 |
128 Nipkow and his students wrote much of the documentation underlying this |
126 Nipkow and his students wrote much of the documentation underlying this |
129 book. Nipkow wrote the first versions of \S\ref{sec:defining-theories}, |
127 book. Nipkow wrote the first versions of \S\ref{sec:defining-theories}, |
130 Chap.\ts\ref{simp-chap}, Chap.\ts\ref{Defining-Logics} and part of |
128 \S\ref{sec:ref-defining-theories}, Chap.\ts\ref{simp-chap}, |
131 Chap.\ts\ref{theories}, and App.\ts\ref{app:TheorySyntax}. Carsten Clasohm |
129 Chap.\ts\ref{Defining-Logics} and App.\ts\ref{app:TheorySyntax}\@. Carsten |
132 contributed to Chap.\ts\ref{theories}. Markus Wenzel contributed to |
130 Clasohm contributed to Chap.\ts\ref{theories}. Markus Wenzel contributed |
133 Chap.\ts\ref{Defining-Logics}. |
131 to Chap.\ts\ref{Defining-Logics}. |
134 |
132 |
135 David Aspinall, Sara Kalvala, Ina Kraan, Zhenyu Qian, Norbert Voelker and |
133 David Aspinall, Sara Kalvala, Ina Kraan, Zhenyu Qian, Norbert V{\"o}lker and |
136 Markus Wenzel suggested changes and corrections to the documentation. |
134 Markus Wenzel suggested changes and corrections to the documentation. |
137 |
135 |
138 Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped |
136 Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped |
139 to develop Isabelle's standard object-logics. David Aspinall performed |
137 to develop Isabelle's standard object-logics. David Aspinall performed |
140 some useful research into theories and implemented an Isabelle Emacs mode. |
138 some useful research into theories and implemented an Isabelle Emacs mode. |