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 concepts, |
19 implication, whose properties are described by axioms. All other concepts, |
20 such as inductive predicates, datatypes or recursive functions, have to be defined |
20 such as inductive predicates, datatypes or recursive functions, are defined |
21 in terms of those constants, and the desired properties, for example |
21 in terms of those primitives, and the desired properties, for example |
22 induction theorems or recursion equations, have to be derived from the definitions |
22 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 |
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 |
24 complex inductive predicates or datatypes ``by hand'' just using the |
25 primitive operators of higher order logic, \emph{definitional packages} have |
25 primitive operators of higher order logic, \emph{definitional packages} have |
26 been implemented automating such work. Thanks to those packages, the user |
26 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 |
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 |
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 |
29 definitions and proofs behind the scenes. In this chapter we explain how |
30 such a package can be implemented. |
30 such a package can be implemented. |
31 |
31 |
32 As the running example we have chosen a rather simple package for defining |
32 As the running example we have chosen a rather simple package for defining |
33 inductive predicates. To keep things really simple, we will not use the |
33 inductive predicates. To keep things really simple, we will not use the |
34 general Knaster-Tarski fixpoint theorem on complete lattices, which forms |
34 general Knaster-Tarski fixpoint theorem on complete lattices, which forms |
35 the basis of Isabelle's standard inductive definition package. Instead, we |
35 the basis of Isabelle/HOL's standard inductive definition package. Instead, we |
36 will describe a simpler \emph{impredicative} (i.e.\ involving quantification on |
36 will describe a simpler \emph{impredicative} (i.e.\ involving quantification on |
37 predicate variables) encoding of inductive predicates. Due to its |
37 predicate variables) encoding of inductive predicates. Due to its |
38 simplicity, this package will necessarily have a reduced functionality. It |
38 simplicity, this package will necessarily have a reduced functionality. It |
39 does neither support introduction rules involving arbitrary monotone |
39 does neither support introduction rules involving arbitrary monotonic |
40 operators, nor does it prove case analysis rules (also called inversion rules). |
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 |
41 Moreover, it only proves a weaker form of the induction principle for inductive |
42 predicates. |
42 predicates. |
43 *} |
43 *} |
44 |
44 |