theory Ind_Intro
imports Main 
begin

chapter {* How to Write a Definitional Package\label{chp: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 primitives, 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, \emph{definitional packages} have
  been implemented to automate such work. Thanks to those packages, the user
  can give a high-level specification, for example 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 the 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/HOL's standard inductive definition package.  Instead, we
  will describe a simpler \emph{impredicative} (i.e.\ involving quantification on
  predicate variables) encoding of inductive predicates. Due to its
  simplicity, this package will necessarily have a reduced functionality. It
  does neither support introduction rules involving arbitrary monotonic
  operators, nor does it prove case analysis rules (also called inversion rules). 
  Moreover, it only proves a weaker form of the induction principle for inductive
  predicates.
*}

end