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