--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Package/Ind_Intro.thy	Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,45 @@
+theory Ind_Intro
+imports Main 
+begin
+
+chapter {* How to Write a Definitional Package\label{chp:package} (TBD) *}
+
+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 have to be defined
+  in terms of those constants, and the desired properties, for example
+  induction theorems, or recursion equations have to be 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 automating 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 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. 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 principle for inductive
+  predicates.
+*}
+
+end