1 theory Ind_Intro

     2 imports Main 

     3 begin

     4 

     5 chapter {* How to Write a Definitional Package\label{chp:package} (TBD) *}

     6 

     7 text {*

     8   \begin{flushright}

     9   {\em

    10   ``My thesis is that programming is not at the bottom of the intellectual \\

    11   pyramid, but at the top. It's creative design of the highest order. It \\

    12   isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\

    13   claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex]

    14   Richard Bornat, In Defence of Programming \cite{Bornat-lecture}

    15   \end{flushright}

    16 

    17   \medskip

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

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

    20   such as inductive predicates, datatypes, or recursive functions have to be defined

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

    22   induction theorems, or recursion equations have to be derived from the definitions

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

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

    25   primitive operators of higher order logic, \emph{definitional packages} have

    26   been implemented automating such work. Thanks to those packages, the user

    27   can give a high-level specification, for example a list of introduction

    28   rules or constructors, and the package then does all the low-level

    29   definitions and proofs behind the scenes. In this chapter we explain how

    30   such a package can be implemented.

    31 

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

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

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

    35   the basis of Isabelle's standard inductive definition package.  Instead, we

    36   will use a simpler \emph{impredicative} (i.e.\ involving quantification on

    37   predicate variables) encoding of inductive predicates. Due to its

    38   simplicity, this package will necessarily have a reduced functionality. It

    39   does neither support introduction rules involving arbitrary monotone

    40   operators, nor does it prove case analysis (or inversion) rules. Moreover,

    41   it only proves a weaker form of the induction principle for inductive

    42   predicates.

    43 *}

    44 

    45 end