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, have to be defined |
21 in terms of those constants, and the desired properties, for example |
21 in terms of those constants, 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, have to be 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 automating 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 a 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'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 |