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]

  \end{flushright}

  \medskip

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

  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

*}

end