9 {\em |
9 {\em |
10 ``My thesis is that programming is not at the bottom of the intellectual \\ |
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 \\ |
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 \\ |
12 isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\ |
13 claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex] |
13 claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex] |
14 Richard Bornat, In defence of programming \cite{Bornat-lecture} |
14 Richard Bornat, In Defence of Programming \cite{Bornat-lecture} |
15 \end{flushright} |
15 \end{flushright} |
16 |
16 |
17 \medskip |
17 \medskip |
18 HOL is based on just a few primitive constants, like equality and |
18 HOL is based on just a few primitive constants, like equality and |
19 implication, whose properties are described by axioms. All other |
19 implication, whose properties are described by axioms. All other concepts, |
20 concepts, such as inductive predicates, datatypes, or recursive functions |
20 such as inductive predicates, datatypes, or recursive functions are defined |
21 are defined in terms of those constants, and the desired properties, for |
21 in terms of those constants, and the desired properties, for example |
22 example induction theorems, or recursion equations are derived from the |
22 induction theorems, or recursion equations are derived from the definitions |
23 definitions by a formal proof. Since it would be very tedious for a user to |
23 by a formal proof. Since it would be very tedious for a user to define |
24 define complex inductive predicates or datatypes ``by hand'' just using the |
24 complex inductive predicates or datatypes ``by hand'' just using the |
25 primitive operators of higher order logic, packages have been implemented |
25 primitive operators of higher order logic, \emph{definitional packages} have |
26 automating such work. Thanks to those packages, the user can give a |
26 been implemented automating such work. Thanks to those packages, the user |
27 high-level specification, like a list of introduction rules or constructors, |
27 can give a high-level specification, for example a list of introduction |
28 and the package then does all the low-level definitions and proofs behind |
28 rules or constructors, and the package then does all the low-level |
29 the scenes. In this chapter we explain how such a package can be |
29 definitions and proofs behind the scenes. In this chapter we explain how |
30 implemented. |
30 such a package can be implemented. |
31 |
31 |
32 As a running example, we have chosen a rather simple package for defining |
32 As a running example, we have chosen a rather simple package for defining |
33 inductive predicates. To keep things really simple, we will not use the general |
33 inductive predicates. To keep things really simple, we will not use the general |
34 Knaster-Tarski fixpoint theorem on complete lattices, which forms the basis |
34 Knaster-Tarski fixpoint theorem on complete lattices, which forms the basis |
35 of Isabelle's standard inductive definition package. Instead, we will use a |
35 of Isabelle's standard inductive definition package. Instead, we will use a |
37 variables) encoding of inductive predicates suggested by Melham |
37 variables) encoding of inductive predicates suggested by Melham |
38 \cite{Melham:1992:PIR}. Due to its simplicity, this package will necessarily |
38 \cite{Melham:1992:PIR}. Due to its simplicity, this package will necessarily |
39 have a reduced functionality. It does neither support introduction rules |
39 have a reduced functionality. It does neither support introduction rules |
40 involving arbitrary monotone operators, nor does it prove case analysis (or |
40 involving arbitrary monotone operators, nor does it prove case analysis (or |
41 inversion) rules. Moreover, it only proves a weaker form of the |
41 inversion) rules. Moreover, it only proves a weaker form of the |
42 induction theorem. |
42 induction principle for inductive predicates. |
43 *} |
43 *} |
44 |
44 |
45 end |
45 end |