diff -r 53460ac408b5 -r 5bb2d29553c2 CookBook/Package/Ind_Intro.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Package/Ind_Intro.thy	Fri Oct 10 17:13:21 2008 +0200
@@ -0,0 +1,104 @@
+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