|
1 theory Ind_Intro |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 chapter {* How to write a definitional package *} |
|
6 |
|
7 section{* Introduction *} |
|
8 |
|
9 text {* |
|
10 \begin{flushright} |
|
11 {\em |
|
12 ``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 \\ |
|
14 isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\ |
|
15 claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex] |
|
16 Richard Bornat, In defence of programming |
|
17 \end{flushright} |
|
18 |
|
19 \medskip |
|
20 |
|
21 \noindent |
|
22 Higher order logic, as implemented in Isabelle/HOL, is based on just a few primitive |
|
23 constants, like equality, implication, and the description operator, whose properties are |
|
24 described as axioms. All other concepts, such as inductive predicates, datatypes, or |
|
25 recursive functions are \emph{defined} using these constants, and the desired |
|
26 properties, for example induction theorems, or recursion equations are \emph{derived} |
|
27 from the definitions by a \emph{formal proof}. Since it would be very tedious |
|
28 for the average user to define complex inductive predicates or datatypes ``by hand'' |
|
29 just using the primitive operators of higher order logic, Isabelle/HOL already contains |
|
30 a number of \emph{packages} automating such tedious work. Thanks to those packages, |
|
31 the user can give a high-level specification, like a list of introduction rules or |
|
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 |
|
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 |
|
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 |
|
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, |
|
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 |
|
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 |
|
55 correct. The same applies to the theory underlying definitional packages. |
|
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 |
|
58 an implementation is an excellent way to find out whether the rules really |
|
59 work in practice. |
|
60 |
|
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. |
|
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 |
|
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 |
|
67 chosen a rather simple package for defining inductive predicates. To keep |
|
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 |
|
70 inductive definition package originally due to Paulson \cite{Paulson-ind-defs}. |
|
71 Instead, we will use a simpler \emph{impredicative} (i.e.\ involving |
|
72 quantification on predicate variables) encoding of inductive predicates |
|
73 suggested by Melham \cite{Melham:1992:PIR}. Due to its simplicity, this |
|
74 package will necessarily have a reduced functionality. It does neither |
|
75 support introduction rules involving arbitrary monotone operators, nor does |
|
76 it prove case analysis (or inversion) rules. Moreover, it only proves a weaker |
|
77 form of the rule induction theorem. |
|
78 |
|
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 |
|
81 proofs in Isabelle/HOL using the Isar language. For further information on |
|
82 this topic, consult the book by Nipkow, Paulson, and Wenzel |
|
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 |
|
85 ML programming language, as described for example in the textbook by Paulson |
|
86 \cite{paulson-ml2}, is required as well. |
|
87 |
|
88 The rest of this article is structured as follows. In \S\ref{sec:ind-examples}, |
|
89 we will illustrate the ``manual'' definition of inductive predicates using |
|
90 some examples. Starting from these examples, we will describe in |
|
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 |
|
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 |
|
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 |
|
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 |
|
99 and induction rules from the definitions introduced in \S\ref{sec:ind-definition}. |
|
100 |
|
101 \nocite{Bornat-lecture} |
|
102 *} |
|
103 |
|
104 end |