--- a/CookBook/Package/Ind_Intro.thy Wed Jan 28 06:43:51 2009 +0000
+++ b/CookBook/Package/Ind_Intro.thy Thu Jan 29 09:46:17 2009 +0000
@@ -1,104 +1,103 @@
theory Ind_Intro
-imports Main
+imports Main
begin
-chapter {* How to write a definitional package *}
-
-section{* Introduction *}
+chapter {* How to Write a Definitional Package *}
text {*
-\begin{flushright}
+ \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
+ ``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 \cite{Bornat-lecture}
+ \end{flushright}
-\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}.
+ \medskip
+ 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 defined in
+ terms of those constants, and the desired properties, for example induction
+ theorems, or recursion equations are derived from the definitions by a
+ formal proof. Since it would be very tedious for a 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
+ packages automating such 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. In this chapter we explain how such a package can be
+ implemented.
+
+ %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.
+ %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.
+ 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.
+ %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}.
+ %The rest of this chapter 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