theory Ind_Intro+
−
imports Main +
−
begin+
−
+
−
chapter {* How to Write a Definitional Package *}+
−
+
−
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 \cite{Bornat-lecture}+
−
  \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}.+
−
+
−
  %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}.+
−
+
−
*}+
−
+
−
end+
−