theory Ind_Introimports Mainbeginchapter {* 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\noindentHigher order logic, as implemented in Isabelle/HOL, is based on just a few primitiveconstants, like equality, implication, and the description operator, whose properties aredescribed as axioms. All other concepts, such as inductive predicates, datatypes, orrecursive functions are \emph{defined} using these constants, and the desiredproperties, for example induction theorems, or recursion equations are \emph{derived}from the definitions by a \emph{formal proof}. Since it would be very tediousfor the average user to define complex inductive predicates or datatypes ``by hand''just using the primitive operators of higher order logic, Isabelle/HOL already containsa 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 orconstructors, and the package then does all the low-level definitions and proofsbehind the scenes. The packages are written in Standard ML, the implementationlanguage of Isabelle, and can be invoked by the user from within theory documentswritten 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 innerworkings of packages, since they can just use the packages that are already partof the Isabelle distribution. However, when developing a general theory that isintended to be applied by other users, one may need to write a new package fromscratch. Recent examples of such packages include the verification environmentfor sequential imperative programs by Schirmer \cite{Schirmer-LPAR04}, thepackage 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 scientificresults. Of course, a carefully-developed theory on paper is indispensableas a basis. However, without an implementation, such a theory will only be ofvery limited practical use, since only an implementation enables other usersto 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 theoremprover. In the literature, there are many examples of paper proofs thatturned out to be incomplete or even faulty, and doing a formalization isa good way of uncovering such errors and ensuring that a proof is reallycorrect. The same applies to the theory underlying definitional packages.For example, the general form of some complicated induction rules for nominaldatatypes turned out to be quite hard to get right on the first try, soan implementation is an excellent way to find out whether the rules reallywork in practice.Writing a package is a particularly difficult task for users that are newto Isabelle, since its programming interface consists of thousands of functions.Rather than just listing all those functions, we give a step-by-step tutorialfor writing a package, using an example that is still simple enough to beeasily understandable, but at the same time sufficiently complex to demonstrateenough of Isabelle's interesting features. As a running example, we havechosen a rather simple package for defining inductive predicates. To keepthings simple, we will not use the general Knaster-Tarski fixpointtheorem on complete lattices, which forms the basis of Isabelle's standardinductive definition package originally due to Paulson \cite{Paulson-ind-defs}.Instead, we will use a simpler \emph{impredicative} (i.e.\ involvingquantification on predicate variables) encoding of inductive predicatessuggested by Melham \cite{Melham:1992:PIR}. Due to its simplicity, thispackage will necessarily have a reduced functionality. It does neithersupport introduction rules involving arbitrary monotone operators, nor doesit prove case analysis (or inversion) rules. Moreover, it only proves a weakerform of the rule induction theorem.Reading this article does not require any prior knowledge of Isabelle's programminginterface. However, we assume the reader to already be familiar with writingproofs in Isabelle/HOL using the Isar language. For further information onthis topic, consult the book by Nipkow, Paulson, and Wenzel\cite{isa-tutorial}. Moreover, in order to understand the pieces ofcode given in this tutorial, some familiarity with the basic concepts of the StandardML 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 usingsome 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 apackage that carries out the construction of such inductive predicates.First of all, a parser for a high-level notation for specifying inductivepredicates via a list of introduction rules is developed in \S\ref{sec:ind-interface}.Having parsed the specification, a suitable primitive definition must beadded 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 introductionand induction rules from the definitions introduced in \S\ref{sec:ind-definition}.\nocite{Bornat-lecture}*}end