32
|
1 |
theory Ind_Intro
|
346
|
2 |
imports "../Base"
|
32
|
3 |
begin
|
|
4 |
|
346
|
5 |
|
565
|
6 |
chapter \<open>How to Write a Definitional Package\label{chp:package}\<close>
|
32
|
7 |
|
565
|
8 |
text \<open>
|
489
|
9 |
\begin{flushright}
|
|
10 |
{\em
|
|
11 |
``We will most likely never realize the full importance of painting the Tower,\\
|
|
12 |
that it is the essential element in the conservation of metal works and the\\
|
|
13 |
more meticulous the paint job, the longer the tower shall endure.''} \\[1ex]
|
|
14 |
Gustave Eiffel, in his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been
|
|
15 |
re-painted 18 times since its initial construction, an average of once every
|
|
16 |
seven years. It takes more than one year for a team of 25 painters to paint the tower
|
|
17 |
from top to bottom.}
|
|
18 |
\end{flushright}
|
|
19 |
|
|
20 |
\medskip
|
113
|
21 |
HOL is based on just a few primitive constants, like equality and
|
116
|
22 |
implication, whose properties are described by axioms. All other concepts,
|
243
|
23 |
such as inductive predicates, datatypes or recursive functions, are defined
|
|
24 |
in terms of those primitives, and the desired properties, for example
|
|
25 |
induction theorems or recursion equations, are derived from the definitions
|
116
|
26 |
by a formal proof. Since it would be very tedious for a user to define
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
27 |
inductive predicates or datatypes ``by hand'' just using the
|
116
|
28 |
primitive operators of higher order logic, \emph{definitional packages} have
|
243
|
29 |
been implemented to automate such work. Thanks to those packages, the user
|
116
|
30 |
can give a high-level specification, for example a list of introduction
|
|
31 |
rules or constructors, and the package then does all the low-level
|
|
32 |
definitions and proofs behind the scenes. In this chapter we explain how
|
|
33 |
such a package can be implemented.
|
32
|
34 |
|
219
|
35 |
As the running example we have chosen a rather simple package for defining
|
127
|
36 |
inductive predicates. To keep things really simple, we will not use the
|
|
37 |
general Knaster-Tarski fixpoint theorem on complete lattices, which forms
|
243
|
38 |
the basis of Isabelle/HOL's standard inductive definition package. Instead, we
|
212
|
39 |
will describe a simpler \emph{impredicative} (i.e.\ involving quantification on
|
127
|
40 |
predicate variables) encoding of inductive predicates. Due to its
|
|
41 |
simplicity, this package will necessarily have a reduced functionality. It
|
243
|
42 |
does neither support introduction rules involving arbitrary monotonic
|
212
|
43 |
operators, nor does it prove case analysis rules (also called inversion rules).
|
|
44 |
Moreover, it only proves a weaker form of the induction principle for inductive
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
45 |
predicates. But it illustrates the implementation pf a typical package in
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
46 |
Isabelle.
|
565
|
47 |
\<close>
|
32
|
48 |
|
|
49 |
end
|