author | wenzelm |
Thu, 09 Jun 2005 12:06:38 +0200 | |
changeset 16353 | 94e565ded526 |
parent 15481 | fc075ae929e4 |
child 17056 | 05fc32a23b8b |
permissions | -rw-r--r-- |
10305 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Overloading{\isadigit{1}}}% |
|
11866 | 4 |
\isamarkupfalse% |
10305 | 5 |
% |
10878 | 6 |
\isamarkupsubsubsection{Controlled Overloading with Type Classes% |
10397 | 7 |
} |
11866 | 8 |
\isamarkuptrue% |
10305 | 9 |
% |
10 |
\begin{isamarkuptext}% |
|
11494 | 11 |
We now start with the theory of ordering relations, which we shall phrase |
11277 | 12 |
in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} |
12815 | 13 |
to avoid clashes with \isa{{\isacharless}} and \isa{{\isacharless}{\isacharequal}} in theory \isa{Main}. To restrict the application of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} we |
10305 | 14 |
introduce the class \isa{ordrel}:% |
15 |
\end{isamarkuptext}% |
|
11866 | 16 |
\isamarkuptrue% |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11866
diff
changeset
|
17 |
\isacommand{axclass}\ ordrel\ {\isacharless}\ type\isamarkupfalse% |
11866 | 18 |
% |
10305 | 19 |
\begin{isamarkuptext}% |
20 |
\noindent |
|
10328 | 21 |
This introduces a new class \isa{ordrel} and makes it a subclass of |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11866
diff
changeset
|
22 |
the predefined class \isa{type}, which |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11866
diff
changeset
|
23 |
is the class of all HOL types. |
10305 | 24 |
This is a degenerate form of axiomatic type class without any axioms. |
25 |
Its sole purpose is to restrict the use of overloaded constants to meaningful |
|
26 |
instances:% |
|
27 |
\end{isamarkuptext}% |
|
11866 | 28 |
\isamarkuptrue% |
10328 | 29 |
\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 |
11866 | 30 |
\ \ \ \ \ \ \ 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}\isamarkupfalse% |
31 |
% |
|
10328 | 32 |
\begin{isamarkuptext}% |
33 |
\noindent |
|
10396 | 34 |
Note that only one occurrence of a type variable in a type needs to be |
35 |
constrained with a class; the constraint is propagated to the other |
|
36 |
occurrences automatically. |
|
37 |
||
11494 | 38 |
So far there are no types of class \isa{ordrel}. To breathe life |
10328 | 39 |
into \isa{ordrel} we need to declare a type to be an \bfindex{instance} of |
40 |
\isa{ordrel}:% |
|
41 |
\end{isamarkuptext}% |
|
11866 | 42 |
\isamarkuptrue% |
43 |
\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ ordrel\isamarkupfalse% |
|
16353 | 44 |
% |
45 |
\begin{isamarkuptxt}% |
|
46 |
\noindent |
|
47 |
Command \isacommand{instance} actually starts a proof, namely that |
|
48 |
\isa{bool} satisfies all axioms of \isa{ordrel}. |
|
49 |
There are none, but we still need to finish that proof, which we do |
|
50 |
by invoking the \methdx{intro_classes} method:% |
|
51 |
\end{isamarkuptxt}% |
|
11866 | 52 |
\isamarkuptrue% |
16353 | 53 |
\isacommand{by}\ intro{\isacharunderscore}classes\isamarkupfalse% |
11866 | 54 |
% |
10328 | 55 |
\begin{isamarkuptext}% |
56 |
\noindent |
|
57 |
More interesting \isacommand{instance} proofs will arise below |
|
58 |
in the context of proper axiomatic type classes. |
|
59 |
||
11161 | 60 |
Although terms like \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} are now legal, we still need to say |
10328 | 61 |
what the relation symbols actually mean at type \isa{bool}:% |
62 |
\end{isamarkuptext}% |
|
11866 | 63 |
\isamarkuptrue% |
10305 | 64 |
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
65 |
le{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}P\ {\isacharless}{\isacharless}{\isacharequal}\ Q\ {\isasymequiv}\ P\ {\isasymlongrightarrow}\ Q{\isachardoublequote}\isanewline |
|
11866 | 66 |
less{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}P\ {\isacharless}{\isacharless}\ Q\ {\isasymequiv}\ {\isasymnot}P\ {\isasymand}\ Q{\isachardoublequote}\isamarkupfalse% |
67 |
% |
|
10305 | 68 |
\begin{isamarkuptext}% |
10328 | 69 |
\noindent |
11494 | 70 |
Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} is provable:% |
10305 | 71 |
\end{isamarkuptext}% |
11866 | 72 |
\isamarkuptrue% |
10328 | 73 |
\isacommand{lemma}\ {\isachardoublequote}False\ {\isacharless}{\isacharless}{\isacharequal}\ P{\isachardoublequote}\isanewline |
11866 | 74 |
\isamarkupfalse% |
16353 | 75 |
\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% |
11866 | 76 |
% |
10305 | 77 |
\begin{isamarkuptext}% |
78 |
\noindent |
|
11494 | 79 |
At this point, \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even well-typed. |
80 |
To make it well-typed, |
|
10305 | 81 |
we need to make lists a type of class \isa{ordrel}:% |
82 |
\end{isamarkuptext}% |
|
11866 | 83 |
\isamarkuptrue% |
84 |
\isamarkupfalse% |
|
10305 | 85 |
\end{isabellebody}% |
86 |
%%% Local Variables: |
|
87 |
%%% mode: latex |
|
88 |
%%% TeX-master: "root" |
|
89 |
%%% End: |