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 a few axioms. All other |
19 implication, whose properties are described by axioms. All other |
20 concepts, such as inductive predicates, datatypes, or recursive functions |
20 concepts, such as inductive predicates, datatypes, or recursive functions |
21 are defined in terms of those constants, and the desired properties, for |
21 are defined in terms of those constants, and the desired properties, for |
22 example induction theorems, or recursion equations are derived from the |
22 example induction theorems, or recursion equations are derived from the |
23 definitions by a formal proof. Since it would be very tedious for a user to |
23 definitions by a formal proof. Since it would be very tedious for a user to |
24 define complex inductive predicates or datatypes ``by hand'' just using the |
24 define complex inductive predicates or datatypes ``by hand'' just using the |
28 and the package then does all the low-level definitions and proofs behind |
28 and the package then does all the low-level definitions and proofs behind |
29 the scenes. In this chapter we explain how such a package can be |
29 the scenes. In this chapter we explain how such a package can be |
30 implemented. |
30 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 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 |
36 simpler \emph{impredicative} (i.e.\ involving quantification on predicate |
36 simpler \emph{impredicative} (i.e.\ involving quantification on predicate |
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 rule |
41 inversion) rules. Moreover, it only proves a weaker form of the |
42 induction theorem. |
42 induction theorem. |
43 *} |
43 *} |
44 |
44 |
45 end |
45 end |