11 (*>*) |
11 (*>*) |
12 |
12 |
13 chapter {* How to Write a Definitional Package\label{chp:package} *} |
13 chapter {* How to Write a Definitional Package\label{chp:package} *} |
14 |
14 |
15 text {* |
15 text {* |
|
16 \begin{flushright} |
|
17 {\em |
|
18 ``We will most likely never realize the full importance of painting the Tower,\\ |
|
19 that it is the essential element in the conservation of metal works and the\\ |
|
20 more meticulous the paint job, the longer the tower shall endure.''} \\[1ex] |
|
21 Gustave Eiffel, in his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been |
|
22 re-painted 18 times since its initial construction, an average of once every |
|
23 seven years. It takes more than one year for a team of 25 painters to paint the tower |
|
24 from top to bottom.} |
|
25 \end{flushright} |
|
26 |
|
27 \medskip |
16 HOL is based on just a few primitive constants, like equality and |
28 HOL is based on just a few primitive constants, like equality and |
17 implication, whose properties are described by axioms. All other concepts, |
29 implication, whose properties are described by axioms. All other concepts, |
18 such as inductive predicates, datatypes or recursive functions, are defined |
30 such as inductive predicates, datatypes or recursive functions, are defined |
19 in terms of those primitives, and the desired properties, for example |
31 in terms of those primitives, and the desired properties, for example |
20 induction theorems or recursion equations, are derived from the definitions |
32 induction theorems or recursion equations, are derived from the definitions |