18   HOL is based on just a few primitive constants, like equality, implication,

    18   HOL is based on just a few primitive constants, like equality and

    19   and the description operator, whose properties are described as axioms. All

    19   implication, whose properties are described by a few axioms. All other

    20   other concepts, such as inductive predicates, datatypes, or recursive

    20   concepts, such as inductive predicates, datatypes, or recursive functions

    21   functions are defined in terms of those constants, and the desired

    21   are defined in terms of those constants, and the desired properties, for

    22   properties, for example induction theorems, or recursion equations are

    22   example induction theorems, or recursion equations are derived from the

    23   derived from the definitions by a formal proof. Since it would be very

    23   definitions by a formal proof. Since it would be very tedious for a user to

    24   tedious for a user to define complex inductive predicates or datatypes ``by

    24   define complex inductive predicates or datatypes ``by hand'' just using the

    25   hand'' just using the primitive operators of higher order logic,

    25   primitive operators of higher order logic, packages have been implemented

    26   Isabelle/HOL already contains a number of packages automating such

    26   automating such work. Thanks to those packages, the user can give a

    27   work. Thanks to those packages, the user can give a high-level

    27   high-level specification, like a list of introduction rules or constructors,

    28   specification, like a list of introduction rules or constructors, and the

    28   and the package then does all the low-level definitions and proofs behind

    29   package then does all the low-level definitions and proofs behind the

    29   the scenes. In this chapter we explain how such a package can be

    30   scenes. In this chapter we explain how such a package can be implemented.

    30   implemented.

    32 

    32   As a running example, we have chosen a rather simple package for defining

    33   %The packages are written in Standard ML, the implementation

    33   inductive predicates. To keep things simple, we will not use the general

    34   %language of Isabelle, and can be invoked by the user from within theory documents

    34   Knaster-Tarski fixpoint theorem on complete lattices, which forms the basis

    35   %written in the Isabelle/Isar language via specific commands. Most of the time,

    35   of Isabelle's standard inductive definition package.  Instead, we will use a

    36   %when using Isabelle for applications, users do not have to worry about the inner

    36   simpler \emph{impredicative} (i.e.\ involving quantification on predicate

    37   %workings of packages, since they can just use the packages that are already part

    37   variables) encoding of inductive predicates suggested by Melham

    38   %of the Isabelle distribution. However, when developing a general theory that is

    38   \cite{Melham:1992:PIR}. Due to its simplicity, this package will necessarily

    39   %intended to be applied by other users, one may need to write a new package from

    39   have a reduced functionality. It does neither support introduction rules

    40   %scratch. Recent examples of such packages include the verification environment

    40   involving arbitrary monotone operators, nor does it prove case analysis (or

    41   %for sequential imperative programs by Schirmer \cite{Schirmer-LPAR04}, the

    41   inversion) rules. Moreover, it only proves a weaker form of the rule

    42   %package for defining general recursive functions by Krauss \cite{Krauss-IJCAR06},

    42   induction theorem.

    43   %as well as the nominal datatype package by Berghofer and Urban \cite{Urban-Berghofer06}.

    44 

    45   %The scientific value of implementing a package should not be underestimated:

    46   %it is often more than just the automation of long-established scientific

    47   %results. Of course, a carefully-developed theory on paper is indispensable

    48   %as a basis. However, without an implementation, such a theory will only be of

    49   %very limited practical use, since only an implementation enables other users

    50   %to apply the theory on a larger scale without too much effort. Moreover,

    51   %implementing a package is a bit like formalizing a paper proof in a theorem

    52   %prover. In the literature, there are many examples of paper proofs that

    53   %turned out to be incomplete or even faulty, and doing a formalization is

    54   %a good way of uncovering such errors and ensuring that a proof is really

    55   %correct. The same applies to the theory underlying definitional packages.

    56   %For example, the general form of some complicated induction rules for nominal

    57   %datatypes turned out to be quite hard to get right on the first try, so

    58   %an implementation is an excellent way to find out whether the rules really

    59   %work in practice.

    60 

    61   Writing a package is a particularly difficult task for users that are new

    62   to Isabelle, since its programming interface consists of thousands of functions.

    63   Rather than just listing all those functions, we give a step-by-step tutorial

    64   for writing a package, using an example that is still simple enough to be

    65   easily understandable, but at the same time sufficiently complex to demonstrate

    66   enough of Isabelle's interesting features. As a running example, we have

    67   chosen a rather simple package for defining inductive predicates. To keep

    68   things simple, we will not use the general Knaster-Tarski fixpoint

    69   theorem on complete lattices, which forms the basis of Isabelle's standard

    70   inductive definition package originally due to Paulson \cite{Paulson-ind-defs}.

    71   Instead, we will use a simpler \emph{impredicative} (i.e.\ involving

    72   quantification on predicate variables) encoding of inductive predicates

    73   suggested by Melham \cite{Melham:1992:PIR}. Due to its simplicity, this

    74   package will necessarily have a reduced functionality. It does neither

    75   support introduction rules involving arbitrary monotone operators, nor does

    76   it prove case analysis (or inversion) rules. Moreover, it only proves a weaker

    77   form of the rule induction theorem.

    78 

    79   %Reading this article does not require any prior knowledge of Isabelle's programming

    80   %interface. However, we assume the reader to already be familiar with writing

    81   %proofs in Isabelle/HOL using the Isar language. For further information on

    82   %this topic, consult the book by Nipkow, Paulson, and Wenzel

    83   %\cite{isa-tutorial}. Moreover, in order to understand the pieces of

    84   %code given in this tutorial, some familiarity with the basic concepts of the Standard

    85   %ML programming language, as described for example in the textbook by Paulson

    86   %\cite{paulson-ml2}, is required as well.

    87 

    88   %The rest of this chapter is structured as follows. In \S\ref{sec:ind-examples},

    89   %we will illustrate the ``manual'' definition of inductive predicates using

    90   %some examples. Starting from these examples, we will describe in

    91   %\S\ref{sec:ind-general-method} how the construction works in general.

    92   %The following sections are then dedicated to the implementation of a

    93   %package that carries out the construction of such inductive predicates.

    94   %First of all, a parser for a high-level notation for specifying inductive

    95   %predicates via a list of introduction rules is developed in \S\ref{sec:ind-interface}.

    96   %Having parsed the specification, a suitable primitive definition must be

    97   %added to the theory, which will be explained in \S\ref{sec:ind-definition}.

    98   %Finally, \S\ref{sec:ind-proofs} will focus on methods for proving introduction

    99   %and induction rules from the definitions introduced in \S\ref{sec:ind-definition}.

   100