10305
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{Overloading{\isadigit{1}}}%
|
|
4 |
%
|
10878
|
5 |
\isamarkupsubsubsection{Controlled Overloading with Type Classes%
|
10397
|
6 |
}
|
10305
|
7 |
%
|
|
8 |
\begin{isamarkuptext}%
|
|
9 |
We now start with the theory of ordering relations, which we want to phrase
|
|
10 |
in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}}: they have
|
10328
|
11 |
been chosen to avoid clashes with \isa{{\isacharless}} and \isa{{\isasymle}} in theory \isa{Main}. To restrict the application of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} we
|
10305
|
12 |
introduce the class \isa{ordrel}:%
|
|
13 |
\end{isamarkuptext}%
|
|
14 |
\isacommand{axclass}\ ordrel\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}%
|
|
15 |
\begin{isamarkuptext}%
|
|
16 |
\noindent
|
10328
|
17 |
This introduces a new class \isa{ordrel} and makes it a subclass of
|
|
18 |
the predefined class \isa{term}\footnote{The quotes around \isa{term}
|
|
19 |
simply avoid the clash with the command \isacommand{term}.}; \isa{term}
|
|
20 |
is the class of all HOL types, like ``Object'' in Java.
|
10305
|
21 |
This is a degenerate form of axiomatic type class without any axioms.
|
|
22 |
Its sole purpose is to restrict the use of overloaded constants to meaningful
|
|
23 |
instances:%
|
|
24 |
\end{isamarkuptext}%
|
10328
|
25 |
\isacommand{consts}\ less\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharless}{\isacharless}{\isachardoublequote}\ \ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
|
|
26 |
\ \ \ \ \ \ \ le\ \ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharless}{\isacharless}{\isacharequal}{\isachardoublequote}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}%
|
|
27 |
\begin{isamarkuptext}%
|
|
28 |
\noindent
|
10396
|
29 |
Note that only one occurrence of a type variable in a type needs to be
|
|
30 |
constrained with a class; the constraint is propagated to the other
|
|
31 |
occurrences automatically.
|
|
32 |
|
10328
|
33 |
So far there is not a single type of class \isa{ordrel}. To breathe life
|
|
34 |
into \isa{ordrel} we need to declare a type to be an \bfindex{instance} of
|
|
35 |
\isa{ordrel}:%
|
|
36 |
\end{isamarkuptext}%
|
|
37 |
\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ ordrel%
|
|
38 |
\begin{isamarkuptxt}%
|
|
39 |
\noindent
|
|
40 |
Command \isacommand{instance} actually starts a proof, namely that
|
|
41 |
\isa{bool} satisfies all axioms of \isa{ordrel}.
|
|
42 |
There are none, but we still need to finish that proof, which we do
|
|
43 |
by invoking a fixed predefined method:%
|
|
44 |
\end{isamarkuptxt}%
|
|
45 |
\isacommand{by}\ intro{\isacharunderscore}classes%
|
|
46 |
\begin{isamarkuptext}%
|
|
47 |
\noindent
|
|
48 |
More interesting \isacommand{instance} proofs will arise below
|
|
49 |
in the context of proper axiomatic type classes.
|
|
50 |
|
11161
|
51 |
Although terms like \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} are now legal, we still need to say
|
10328
|
52 |
what the relation symbols actually mean at type \isa{bool}:%
|
|
53 |
\end{isamarkuptext}%
|
10305
|
54 |
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
|
|
55 |
le{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}P\ {\isacharless}{\isacharless}{\isacharequal}\ Q\ {\isasymequiv}\ P\ {\isasymlongrightarrow}\ Q{\isachardoublequote}\isanewline
|
|
56 |
less{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}P\ {\isacharless}{\isacharless}\ Q\ {\isasymequiv}\ {\isasymnot}P\ {\isasymand}\ Q{\isachardoublequote}%
|
|
57 |
\begin{isamarkuptext}%
|
10328
|
58 |
\noindent
|
|
59 |
Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} is provable%
|
10305
|
60 |
\end{isamarkuptext}%
|
10328
|
61 |
\isacommand{lemma}\ {\isachardoublequote}False\ {\isacharless}{\isacharless}{\isacharequal}\ P{\isachardoublequote}\isanewline
|
10305
|
62 |
\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}%
|
|
63 |
\begin{isamarkuptext}%
|
|
64 |
\noindent
|
|
65 |
whereas \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even welltyped. In order to make it welltyped
|
|
66 |
we need to make lists a type of class \isa{ordrel}:%
|
|
67 |
\end{isamarkuptext}%
|
|
68 |
\end{isabellebody}%
|
|
69 |
%%% Local Variables:
|
|
70 |
%%% mode: latex
|
|
71 |
%%% TeX-master: "root"
|
|
72 |
%%% End:
|