32
|
1 |
theory Ind_Intro
|
88
|
2 |
imports Main
|
32
|
3 |
begin
|
|
4 |
|
217
|
5 |
chapter {* How to Write a Definitional Package\label{chp:package} *}
|
32
|
6 |
|
|
7 |
text {*
|
88
|
8 |
\begin{flushright}
|
32
|
9 |
{\em
|
88
|
10 |
``My thesis is that programming is not at the bottom of the intellectual \\
|
|
11 |
pyramid, but at the top. It's creative design of the highest order. It \\
|
|
12 |
isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\
|
|
13 |
claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex]
|
116
|
14 |
Richard Bornat, In Defence of Programming \cite{Bornat-lecture}
|
88
|
15 |
\end{flushright}
|
32
|
16 |
|
88
|
17 |
\medskip
|
113
|
18 |
HOL is based on just a few primitive constants, like equality and
|
116
|
19 |
implication, whose properties are described by axioms. All other concepts,
|
243
|
20 |
such as inductive predicates, datatypes or recursive functions, are defined
|
|
21 |
in terms of those primitives, and the desired properties, for example
|
|
22 |
induction theorems or recursion equations, are derived from the definitions
|
116
|
23 |
by a formal proof. Since it would be very tedious for a user to define
|
|
24 |
complex inductive predicates or datatypes ``by hand'' just using the
|
|
25 |
primitive operators of higher order logic, \emph{definitional packages} have
|
243
|
26 |
been implemented to automate such work. Thanks to those packages, the user
|
116
|
27 |
can give a high-level specification, for example a list of introduction
|
|
28 |
rules or constructors, and the package then does all the low-level
|
|
29 |
definitions and proofs behind the scenes. In this chapter we explain how
|
|
30 |
such a package can be implemented.
|
32
|
31 |
|
219
|
32 |
As the running example we have chosen a rather simple package for defining
|
127
|
33 |
inductive predicates. To keep things really simple, we will not use the
|
|
34 |
general Knaster-Tarski fixpoint theorem on complete lattices, which forms
|
243
|
35 |
the basis of Isabelle/HOL's standard inductive definition package. Instead, we
|
212
|
36 |
will describe a simpler \emph{impredicative} (i.e.\ involving quantification on
|
127
|
37 |
predicate variables) encoding of inductive predicates. Due to its
|
|
38 |
simplicity, this package will necessarily have a reduced functionality. It
|
243
|
39 |
does neither support introduction rules involving arbitrary monotonic
|
212
|
40 |
operators, nor does it prove case analysis rules (also called inversion rules).
|
|
41 |
Moreover, it only proves a weaker form of the induction principle for inductive
|
127
|
42 |
predicates.
|
32
|
43 |
*}
|
|
44 |
|
|
45 |
end
|