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+
−