--- a/CookBook/Package/Ind_Intro.thy Fri Feb 13 01:05:09 2009 +0000
+++ b/CookBook/Package/Ind_Intro.thy Fri Feb 13 01:05:31 2009 +0000
@@ -15,89 +15,31 @@
\end{flushright}
\medskip
- 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}.
+ HOL is based on just a few primitive constants, like equality and
+ implication, whose properties are described by a few 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, packages have been implemented
+ 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 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 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}.
-
+ 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. 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.
*}
end