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 and
  implication, whose properties are described by 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.

  As a running example, we have chosen a rather simple package for defining
  inductive predicates. To keep things really 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
  induction theorem.
*}

end