theory Ind_Introimports "../Base"begin(*<*)setup{*open_file_with_prelude "Ind_Package_Code.thy" ["theory Ind_Package", "imports Main", "begin"]*}(*>*)chapter {* How to Write a Definitional Package\label{chp:package} *}text {* 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.*}end