author | Christian Urban <urbanc@in.tum.de> |
Tue, 11 Jun 2019 23:31:09 +0100 | |
changeset 578 | 69c78980c8a4 |
parent 565 | cecd7a941885 |
permissions | -rw-r--r-- |
32 | 1 |
theory Ind_Intro |
346
0fea8b7a14a1
tuned the ML-output mechanism; tuned slightly the text
Christian Urban <urbanc@in.tum.de>
parents:
295
diff
changeset
|
2 |
imports "../Base" |
32 | 3 |
begin |
4 |
||
346
0fea8b7a14a1
tuned the ML-output mechanism; tuned slightly the text
Christian Urban <urbanc@in.tum.de>
parents:
295
diff
changeset
|
5 |
|
565
cecd7a941885
isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents:
517
diff
changeset
|
6 |
chapter \<open>How to Write a Definitional Package\label{chp:package}\<close> |
32 | 7 |
|
565
cecd7a941885
isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents:
517
diff
changeset
|
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
c9ff326e3ce5
more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents:
115
diff
changeset
|
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
c9ff326e3ce5
more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents:
115
diff
changeset
|
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>
parents:
243
diff
changeset
|
27 |
inductive predicates or datatypes ``by hand'' just using the |
116
c9ff326e3ce5
more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents:
115
diff
changeset
|
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
c9ff326e3ce5
more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents:
115
diff
changeset
|
30 |
can give a high-level specification, for example a list of introduction |
c9ff326e3ce5
more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents:
115
diff
changeset
|
31 |
rules or constructors, and the package then does all the low-level |
c9ff326e3ce5
more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents:
115
diff
changeset
|
32 |
definitions and proofs behind the scenes. In this chapter we explain how |
c9ff326e3ce5
more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents:
115
diff
changeset
|
33 |
such a package can be implemented. |
32 | 34 |
|
219
98d43270024f
more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents:
217
diff
changeset
|
35 |
As the running example we have chosen a rather simple package for defining |
127
74846cb0fff9
updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
121
diff
changeset
|
36 |
inductive predicates. To keep things really simple, we will not use the |
74846cb0fff9
updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
121
diff
changeset
|
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
74846cb0fff9
updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
121
diff
changeset
|
40 |
predicate variables) encoding of inductive predicates. Due to its |
74846cb0fff9
updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
121
diff
changeset
|
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>
parents:
243
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>
parents:
243
diff
changeset
|
46 |
Isabelle. |
565
cecd7a941885
isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents:
517
diff
changeset
|
47 |
\<close> |
32 | 48 |
|
49 |
end |