theory Ind_Intro

imports "../Base"

begin

chapter \<open>How to Write a Definitional Package\label{chp:package}\<close>

text \<open>

   \begin{flushright}

  {\em

  ``We will most likely never realize the full importance of painting the Tower,\\ 

  that it is the essential element in the conservation of metal works and the\\ 

  more meticulous the paint job, the longer the tower shall endure.''} \\[1ex]

  Gustave Eiffel, in his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been 

  re-painted 18 times since its initial construction, an average of once every 

  seven years. It takes more than one year for a team of 25 painters to paint the tower 

  from top to bottom.}

  \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

  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. But it illustrates the implementation pf a typical package in

  Isabelle.

\<close>

end