1 theory Ind_Intro |
1 theory Ind_Intro |
2 imports Main |
2 imports Main |
3 begin |
3 begin |
4 |
4 |
5 chapter {* How to write a definitional package *} |
5 chapter {* How to Write a Definitional Package *} |
6 |
|
7 section{* Introduction *} |
|
8 |
6 |
9 text {* |
7 text {* |
10 \begin{flushright} |
8 \begin{flushright} |
11 {\em |
9 {\em |
12 ``My thesis is that programming is not at the bottom of the intellectual \\ |
10 ``My thesis is that programming is not at the bottom of the intellectual \\ |
13 pyramid, but at the top. It's creative design of the highest order. It \\ |
11 pyramid, but at the top. It's creative design of the highest order. It \\ |
14 isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\ |
12 isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\ |
15 claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex] |
13 claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex] |
16 Richard Bornat, In defence of programming |
14 Richard Bornat, In defence of programming \cite{Bornat-lecture} |
17 \end{flushright} |
15 \end{flushright} |
18 |
16 |
19 \medskip |
17 \medskip |
|
18 Higher order logic, as implemented in Isabelle/HOL, is based on just a few |
|
19 primitive constants, like equality, implication, and the description |
|
20 operator, whose properties are described as axioms. All other concepts, such |
|
21 as inductive predicates, datatypes, or recursive functions are defined in |
|
22 terms of those constants, and the desired properties, for example induction |
|
23 theorems, or recursion equations are derived from the definitions by a |
|
24 formal proof. Since it would be very tedious for a user to define complex |
|
25 inductive predicates or datatypes ``by hand'' just using the primitive |
|
26 operators of higher order logic, Isabelle/HOL already contains a number of |
|
27 packages automating such work. Thanks to those packages, the user can give a |
|
28 high-level specification, like a list of introduction rules or constructors, |
|
29 and the package then does all the low-level definitions and proofs behind |
|
30 the scenes. In this chapter we explain how such a package can be |
|
31 implemented. |
20 |
32 |
21 \noindent |
33 %The packages are written in Standard ML, the implementation |
22 Higher order logic, as implemented in Isabelle/HOL, is based on just a few primitive |
34 %language of Isabelle, and can be invoked by the user from within theory documents |
23 constants, like equality, implication, and the description operator, whose properties are |
35 %written in the Isabelle/Isar language via specific commands. Most of the time, |
24 described as axioms. All other concepts, such as inductive predicates, datatypes, or |
36 %when using Isabelle for applications, users do not have to worry about the inner |
25 recursive functions are \emph{defined} using these constants, and the desired |
37 %workings of packages, since they can just use the packages that are already part |
26 properties, for example induction theorems, or recursion equations are \emph{derived} |
38 %of the Isabelle distribution. However, when developing a general theory that is |
27 from the definitions by a \emph{formal proof}. Since it would be very tedious |
39 %intended to be applied by other users, one may need to write a new package from |
28 for the average user to define complex inductive predicates or datatypes ``by hand'' |
40 %scratch. Recent examples of such packages include the verification environment |
29 just using the primitive operators of higher order logic, Isabelle/HOL already contains |
41 %for sequential imperative programs by Schirmer \cite{Schirmer-LPAR04}, the |
30 a number of \emph{packages} automating such tedious work. Thanks to those packages, |
42 %package for defining general recursive functions by Krauss \cite{Krauss-IJCAR06}, |
31 the user can give a high-level specification, like a list of introduction rules or |
43 %as well as the nominal datatype package by Berghofer and Urban \cite{Urban-Berghofer06}. |
32 constructors, and the package then does all the low-level definitions and proofs |
|
33 behind the scenes. The packages are written in Standard ML, the implementation |
|
34 language of Isabelle, and can be invoked by the user from within theory documents |
|
35 written in the Isabelle/Isar language via specific commands. Most of the time, |
|
36 when using Isabelle for applications, users do not have to worry about the inner |
|
37 workings of packages, since they can just use the packages that are already part |
|
38 of the Isabelle distribution. However, when developing a general theory that is |
|
39 intended to be applied by other users, one may need to write a new package from |
|
40 scratch. Recent examples of such packages include the verification environment |
|
41 for sequential imperative programs by Schirmer \cite{Schirmer-LPAR04}, the |
|
42 package for defining general recursive functions by Krauss \cite{Krauss-IJCAR06}, |
|
43 as well as the nominal datatype package by Berghofer and Urban \cite{Urban-Berghofer06}. |
|
44 |
44 |
45 The scientific value of implementing a package should not be underestimated: |
45 %The scientific value of implementing a package should not be underestimated: |
46 it is often more than just the automation of long-established scientific |
46 %it is often more than just the automation of long-established scientific |
47 results. Of course, a carefully-developed theory on paper is indispensable |
47 %results. Of course, a carefully-developed theory on paper is indispensable |
48 as a basis. However, without an implementation, such a theory will only be of |
48 %as a basis. However, without an implementation, such a theory will only be of |
49 very limited practical use, since only an implementation enables other users |
49 %very limited practical use, since only an implementation enables other users |
50 to apply the theory on a larger scale without too much effort. Moreover, |
50 %to apply the theory on a larger scale without too much effort. Moreover, |
51 implementing a package is a bit like formalizing a paper proof in a theorem |
51 %implementing a package is a bit like formalizing a paper proof in a theorem |
52 prover. In the literature, there are many examples of paper proofs that |
52 %prover. In the literature, there are many examples of paper proofs that |
53 turned out to be incomplete or even faulty, and doing a formalization is |
53 %turned out to be incomplete or even faulty, and doing a formalization is |
54 a good way of uncovering such errors and ensuring that a proof is really |
54 %a good way of uncovering such errors and ensuring that a proof is really |
55 correct. The same applies to the theory underlying definitional packages. |
55 %correct. The same applies to the theory underlying definitional packages. |
56 For example, the general form of some complicated induction rules for nominal |
56 %For example, the general form of some complicated induction rules for nominal |
57 datatypes turned out to be quite hard to get right on the first try, so |
57 %datatypes turned out to be quite hard to get right on the first try, so |
58 an implementation is an excellent way to find out whether the rules really |
58 %an implementation is an excellent way to find out whether the rules really |
59 work in practice. |
59 %work in practice. |
60 |
60 |
61 Writing a package is a particularly difficult task for users that are new |
61 Writing a package is a particularly difficult task for users that are new |
62 to Isabelle, since its programming interface consists of thousands of functions. |
62 to Isabelle, since its programming interface consists of thousands of functions. |
63 Rather than just listing all those functions, we give a step-by-step tutorial |
63 Rather than just listing all those functions, we give a step-by-step tutorial |
64 for writing a package, using an example that is still simple enough to be |
64 for writing a package, using an example that is still simple enough to be |
65 easily understandable, but at the same time sufficiently complex to demonstrate |
65 easily understandable, but at the same time sufficiently complex to demonstrate |
66 enough of Isabelle's interesting features. As a running example, we have |
66 enough of Isabelle's interesting features. As a running example, we have |
67 chosen a rather simple package for defining inductive predicates. To keep |
67 chosen a rather simple package for defining inductive predicates. To keep |
68 things simple, we will not use the general Knaster-Tarski fixpoint |
68 things simple, we will not use the general Knaster-Tarski fixpoint |
69 theorem on complete lattices, which forms the basis of Isabelle's standard |
69 theorem on complete lattices, which forms the basis of Isabelle's standard |
70 inductive definition package originally due to Paulson \cite{Paulson-ind-defs}. |
70 inductive definition package originally due to Paulson \cite{Paulson-ind-defs}. |
71 Instead, we will use a simpler \emph{impredicative} (i.e.\ involving |
71 Instead, we will use a simpler \emph{impredicative} (i.e.\ involving |
72 quantification on predicate variables) encoding of inductive predicates |
72 quantification on predicate variables) encoding of inductive predicates |
73 suggested by Melham \cite{Melham:1992:PIR}. Due to its simplicity, this |
73 suggested by Melham \cite{Melham:1992:PIR}. Due to its simplicity, this |
74 package will necessarily have a reduced functionality. It does neither |
74 package will necessarily have a reduced functionality. It does neither |
75 support introduction rules involving arbitrary monotone operators, nor does |
75 support introduction rules involving arbitrary monotone operators, nor does |
76 it prove case analysis (or inversion) rules. Moreover, it only proves a weaker |
76 it prove case analysis (or inversion) rules. Moreover, it only proves a weaker |
77 form of the rule induction theorem. |
77 form of the rule induction theorem. |
78 |
78 |
79 Reading this article does not require any prior knowledge of Isabelle's programming |
79 %Reading this article does not require any prior knowledge of Isabelle's programming |
80 interface. However, we assume the reader to already be familiar with writing |
80 %interface. However, we assume the reader to already be familiar with writing |
81 proofs in Isabelle/HOL using the Isar language. For further information on |
81 %proofs in Isabelle/HOL using the Isar language. For further information on |
82 this topic, consult the book by Nipkow, Paulson, and Wenzel |
82 %this topic, consult the book by Nipkow, Paulson, and Wenzel |
83 \cite{isa-tutorial}. Moreover, in order to understand the pieces of |
83 %\cite{isa-tutorial}. Moreover, in order to understand the pieces of |
84 code given in this tutorial, some familiarity with the basic concepts of the Standard |
84 %code given in this tutorial, some familiarity with the basic concepts of the Standard |
85 ML programming language, as described for example in the textbook by Paulson |
85 %ML programming language, as described for example in the textbook by Paulson |
86 \cite{paulson-ml2}, is required as well. |
86 %\cite{paulson-ml2}, is required as well. |
87 |
87 |
88 The rest of this article is structured as follows. In \S\ref{sec:ind-examples}, |
88 %The rest of this chapter is structured as follows. In \S\ref{sec:ind-examples}, |
89 we will illustrate the ``manual'' definition of inductive predicates using |
89 %we will illustrate the ``manual'' definition of inductive predicates using |
90 some examples. Starting from these examples, we will describe in |
90 %some examples. Starting from these examples, we will describe in |
91 \S\ref{sec:ind-general-method} how the construction works in general. |
91 %\S\ref{sec:ind-general-method} how the construction works in general. |
92 The following sections are then dedicated to the implementation of a |
92 %The following sections are then dedicated to the implementation of a |
93 package that carries out the construction of such inductive predicates. |
93 %package that carries out the construction of such inductive predicates. |
94 First of all, a parser for a high-level notation for specifying inductive |
94 %First of all, a parser for a high-level notation for specifying inductive |
95 predicates via a list of introduction rules is developed in \S\ref{sec:ind-interface}. |
95 %predicates via a list of introduction rules is developed in \S\ref{sec:ind-interface}. |
96 Having parsed the specification, a suitable primitive definition must be |
96 %Having parsed the specification, a suitable primitive definition must be |
97 added to the theory, which will be explained in \S\ref{sec:ind-definition}. |
97 %added to the theory, which will be explained in \S\ref{sec:ind-definition}. |
98 Finally, \S\ref{sec:ind-proofs} will focus on methods for proving introduction |
98 %Finally, \S\ref{sec:ind-proofs} will focus on methods for proving introduction |
99 and induction rules from the definitions introduced in \S\ref{sec:ind-definition}. |
99 %and induction rules from the definitions introduced in \S\ref{sec:ind-definition}. |
100 |
100 |
101 \nocite{Bornat-lecture} |
|
102 *} |
101 *} |
103 |
102 |
104 end |
103 end |