diff -r a90d0fb24e75 -r 9b6c9d172378 CookBook/Package/Ind_Intro.thy --- 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