theory Ind_Intro+ −
imports Main+ −
begin+ −
+ −
chapter {* How to write a definitional package *}+ −
+ −
section{* Introduction *}+ −
+ −
text {*+ −
\begin{flushright}+ −
{\em+ −
``My thesis is that programming is not at the bottom of the intellectual \\+ −
pyramid, but at the top. It's creative design of the highest order. It \\+ −
isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\+ −
claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex]+ −
Richard Bornat, In defence of programming+ −
\end{flushright}+ −
+ −
\medskip+ −
+ −
\noindent+ −
Higher order logic, as implemented in Isabelle/HOL, is based on just a few primitive+ −
constants, like equality, implication, and the description operator, whose properties are+ −
described as axioms. All other concepts, such as inductive predicates, datatypes, or+ −
recursive functions are \emph{defined} using these constants, and the desired+ −
properties, for example induction theorems, or recursion equations are \emph{derived}+ −
from the definitions by a \emph{formal proof}. Since it would be very tedious+ −
for the average user to define complex inductive predicates or datatypes ``by hand''+ −
just using the primitive operators of higher order logic, Isabelle/HOL already contains+ −
a number of \emph{packages} automating such tedious work. Thanks to those packages,+ −
the user can give a high-level specification, like a list of introduction rules or+ −
constructors, and the package then does all the low-level definitions and proofs+ −
behind the scenes. The packages are written in Standard ML, the implementation+ −
language of Isabelle, and can be invoked by the user from within theory documents+ −
written in the Isabelle/Isar language via specific commands. Most of the time,+ −
when using Isabelle for applications, users do not have to worry about the inner+ −
workings of packages, since they can just use the packages that are already part+ −
of the Isabelle distribution. However, when developing a general theory that is+ −
intended to be applied by other users, one may need to write a new package from+ −
scratch. Recent examples of such packages include the verification environment+ −
for sequential imperative programs by Schirmer \cite{Schirmer-LPAR04}, the+ −
package for defining general recursive functions by Krauss \cite{Krauss-IJCAR06},+ −
as well as the nominal datatype package by Berghofer and Urban \cite{Urban-Berghofer06}.+ −
+ −
The scientific value of implementing a package should not be underestimated:+ −
it is often more than just the automation of long-established scientific+ −
results. Of course, a carefully-developed theory on paper is indispensable+ −
as a basis. However, without an implementation, such a theory will only be of+ −
very limited practical use, since only an implementation enables other users+ −
to apply the theory on a larger scale without too much effort. Moreover,+ −
implementing a package is a bit like formalizing a paper proof in a theorem+ −
prover. In the literature, there are many examples of paper proofs that+ −
turned out to be incomplete or even faulty, and doing a formalization is+ −
a good way of uncovering such errors and ensuring that a proof is really+ −
correct. The same applies to the theory underlying definitional packages.+ −
For example, the general form of some complicated induction rules for nominal+ −
datatypes turned out to be quite hard to get right on the first try, so+ −
an implementation is an excellent way to find out whether the rules really+ −
work in practice.+ −
+ −
Writing a package is a particularly difficult task for users that are new+ −
to Isabelle, since its programming interface consists of thousands of functions.+ −
Rather than just listing all those functions, we give a step-by-step tutorial+ −
for writing a package, using an example that is still simple enough to be+ −
easily understandable, but at the same time sufficiently complex to demonstrate+ −
enough of Isabelle's interesting features. As a running example, we have+ −
chosen a rather simple package for defining inductive predicates. To keep+ −
things simple, we will not use the general Knaster-Tarski fixpoint+ −
theorem on complete lattices, which forms the basis of Isabelle's standard+ −
inductive definition package originally due to Paulson \cite{Paulson-ind-defs}.+ −
Instead, we will use a simpler \emph{impredicative} (i.e.\ involving+ −
quantification on predicate variables) encoding of inductive predicates+ −
suggested by Melham \cite{Melham:1992:PIR}. Due to its simplicity, this+ −
package will necessarily have a reduced functionality. It does neither+ −
support introduction rules involving arbitrary monotone operators, nor does+ −
it prove case analysis (or inversion) rules. Moreover, it only proves a weaker+ −
form of the rule induction theorem.+ −
+ −
Reading this article does not require any prior knowledge of Isabelle's programming+ −
interface. However, we assume the reader to already be familiar with writing+ −
proofs in Isabelle/HOL using the Isar language. For further information on+ −
this topic, consult the book by Nipkow, Paulson, and Wenzel+ −
\cite{isa-tutorial}. Moreover, in order to understand the pieces of+ −
code given in this tutorial, some familiarity with the basic concepts of the Standard+ −
ML programming language, as described for example in the textbook by Paulson+ −
\cite{paulson-ml2}, is required as well.+ −
+ −
The rest of this article is structured as follows. In \S\ref{sec:ind-examples},+ −
we will illustrate the ``manual'' definition of inductive predicates using+ −
some examples. Starting from these examples, we will describe in+ −
\S\ref{sec:ind-general-method} how the construction works in general.+ −
The following sections are then dedicated to the implementation of a+ −
package that carries out the construction of such inductive predicates.+ −
First of all, a parser for a high-level notation for specifying inductive+ −
predicates via a list of introduction rules is developed in \S\ref{sec:ind-interface}.+ −
Having parsed the specification, a suitable primitive definition must be+ −
added to the theory, which will be explained in \S\ref{sec:ind-definition}.+ −
Finally, \S\ref{sec:ind-proofs} will focus on methods for proving introduction+ −
and induction rules from the definitions introduced in \S\ref{sec:ind-definition}.+ −
+ −
\nocite{Bornat-lecture}+ −
*}+ −
+ −
end+ −