3 begin |
3 begin |
4 |
4 |
5 chapter {* How to Write a Definitional Package\label{chp:package} *} |
5 chapter {* How to Write a Definitional Package\label{chp:package} *} |
6 |
6 |
7 text {* |
7 text {* |
8 \begin{flushright} |
|
9 {\em |
|
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] |
|
14 Richard Bornat, In Defence of Programming \cite{Bornat-lecture} |
|
15 \end{flushright} |
|
16 |
|
17 \medskip |
|
18 HOL is based on just a few primitive constants, like equality and |
8 HOL is based on just a few primitive constants, like equality and |
19 implication, whose properties are described by axioms. All other concepts, |
9 implication, whose properties are described by axioms. All other concepts, |
20 such as inductive predicates, datatypes or recursive functions, are defined |
10 such as inductive predicates, datatypes or recursive functions, are defined |
21 in terms of those primitives, and the desired properties, for example |
11 in terms of those primitives, and the desired properties, for example |
22 induction theorems or recursion equations, are derived from the definitions |
12 induction theorems or recursion equations, are derived from the definitions |
23 by a formal proof. Since it would be very tedious for a user to define |
13 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 |
14 inductive predicates or datatypes ``by hand'' just using the |
25 primitive operators of higher order logic, \emph{definitional packages} have |
15 primitive operators of higher order logic, \emph{definitional packages} have |
26 been implemented to automate such work. Thanks to those packages, the user |
16 been implemented to automate such work. Thanks to those packages, the user |
27 can give a high-level specification, for example a list of introduction |
17 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 |
18 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 |
19 definitions and proofs behind the scenes. In this chapter we explain how |
37 predicate variables) encoding of inductive predicates. Due to its |
27 predicate variables) encoding of inductive predicates. Due to its |
38 simplicity, this package will necessarily have a reduced functionality. It |
28 simplicity, this package will necessarily have a reduced functionality. It |
39 does neither support introduction rules involving arbitrary monotonic |
29 does neither support introduction rules involving arbitrary monotonic |
40 operators, nor does it prove case analysis rules (also called inversion rules). |
30 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 |
31 Moreover, it only proves a weaker form of the induction principle for inductive |
42 predicates. |
32 predicates. But it illustrates the implementation pf a typical package in |
|
33 Isabelle. |
43 *} |
34 *} |
44 |
35 |
45 end |
36 end |