author | wenzelm |
Sat, 18 Mar 2006 18:33:49 +0100 | |
changeset 19288 | 85b684d3fdbd |
parent 17187 | 45bee2f6e61f |
permissions | -rw-r--r-- |
10305 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Overloading{\isadigit{1}}}% |
|
17056 | 4 |
% |
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
% |
|
11 |
\endisatagtheory |
|
12 |
{\isafoldtheory}% |
|
13 |
% |
|
14 |
\isadelimtheory |
|
15 |
% |
|
16 |
\endisadelimtheory |
|
10305 | 17 |
% |
10878 | 18 |
\isamarkupsubsubsection{Controlled Overloading with Type Classes% |
10397 | 19 |
} |
11866 | 20 |
\isamarkuptrue% |
10305 | 21 |
% |
22 |
\begin{isamarkuptext}% |
|
11494 | 23 |
We now start with the theory of ordering relations, which we shall phrase |
11277 | 24 |
in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} |
12815 | 25 |
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 | 26 |
introduce the class \isa{ordrel}:% |
27 |
\end{isamarkuptext}% |
|
17175 | 28 |
\isamarkuptrue% |
29 |
\isacommand{axclass}\isamarkupfalse% |
|
30 |
\ ordrel\ {\isacharless}\ type% |
|
10305 | 31 |
\begin{isamarkuptext}% |
32 |
\noindent |
|
10328 | 33 |
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
|
34 |
the predefined class \isa{type}, which |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11866
diff
changeset
|
35 |
is the class of all HOL types. |
10305 | 36 |
This is a degenerate form of axiomatic type class without any axioms. |
37 |
Its sole purpose is to restrict the use of overloaded constants to meaningful |
|
38 |
instances:% |
|
39 |
\end{isamarkuptext}% |
|
17175 | 40 |
\isamarkuptrue% |
41 |
\isacommand{consts}\isamarkupfalse% |
|
19288 | 42 |
\ lt\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharless}{\isacharless}{\isachardoublequoteclose}\ \ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline |
43 |
\ \ \ \ \ \ \ le\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharless}{\isacharless}{\isacharequal}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}% |
|
10328 | 44 |
\begin{isamarkuptext}% |
45 |
\noindent |
|
10396 | 46 |
Note that only one occurrence of a type variable in a type needs to be |
47 |
constrained with a class; the constraint is propagated to the other |
|
48 |
occurrences automatically. |
|
49 |
||
11494 | 50 |
So far there are no types of class \isa{ordrel}. To breathe life |
10328 | 51 |
into \isa{ordrel} we need to declare a type to be an \bfindex{instance} of |
52 |
\isa{ordrel}:% |
|
53 |
\end{isamarkuptext}% |
|
17175 | 54 |
\isamarkuptrue% |
55 |
\isacommand{instance}\isamarkupfalse% |
|
56 |
\ bool\ {\isacharcolon}{\isacharcolon}\ ordrel% |
|
17056 | 57 |
\isadelimproof |
58 |
% |
|
59 |
\endisadelimproof |
|
60 |
% |
|
61 |
\isatagproof |
|
16353 | 62 |
% |
63 |
\begin{isamarkuptxt}% |
|
64 |
\noindent |
|
65 |
Command \isacommand{instance} actually starts a proof, namely that |
|
66 |
\isa{bool} satisfies all axioms of \isa{ordrel}. |
|
67 |
There are none, but we still need to finish that proof, which we do |
|
68 |
by invoking the \methdx{intro_classes} method:% |
|
69 |
\end{isamarkuptxt}% |
|
17175 | 70 |
\isamarkuptrue% |
71 |
\isacommand{by}\isamarkupfalse% |
|
72 |
\ intro{\isacharunderscore}classes% |
|
17056 | 73 |
\endisatagproof |
74 |
{\isafoldproof}% |
|
75 |
% |
|
76 |
\isadelimproof |
|
77 |
% |
|
78 |
\endisadelimproof |
|
11866 | 79 |
% |
10328 | 80 |
\begin{isamarkuptext}% |
81 |
\noindent |
|
82 |
More interesting \isacommand{instance} proofs will arise below |
|
83 |
in the context of proper axiomatic type classes. |
|
84 |
||
11161 | 85 |
Although terms like \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} are now legal, we still need to say |
10328 | 86 |
what the relation symbols actually mean at type \isa{bool}:% |
87 |
\end{isamarkuptext}% |
|
17175 | 88 |
\isamarkuptrue% |
89 |
\isacommand{defs}\isamarkupfalse% |
|
90 |
\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
|
19288 | 91 |
le{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}P\ {\isacharless}{\isacharless}{\isacharequal}\ Q\ {\isasymequiv}\ P\ {\isasymlongrightarrow}\ Q{\isachardoublequoteclose}\isanewline |
92 |
lt{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}P\ {\isacharless}{\isacharless}\ Q\ {\isasymequiv}\ {\isasymnot}P\ {\isasymand}\ Q{\isachardoublequoteclose}% |
|
10305 | 93 |
\begin{isamarkuptext}% |
10328 | 94 |
\noindent |
11494 | 95 |
Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} is provable:% |
10305 | 96 |
\end{isamarkuptext}% |
17175 | 97 |
\isamarkuptrue% |
98 |
\isacommand{lemma}\isamarkupfalse% |
|
99 |
\ {\isachardoublequoteopen}False\ {\isacharless}{\isacharless}{\isacharequal}\ P{\isachardoublequoteclose}\isanewline |
|
17056 | 100 |
% |
101 |
\isadelimproof |
|
102 |
% |
|
103 |
\endisadelimproof |
|
104 |
% |
|
105 |
\isatagproof |
|
17175 | 106 |
\isacommand{by}\isamarkupfalse% |
107 |
{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}% |
|
17056 | 108 |
\endisatagproof |
109 |
{\isafoldproof}% |
|
110 |
% |
|
111 |
\isadelimproof |
|
112 |
% |
|
113 |
\endisadelimproof |
|
11866 | 114 |
% |
10305 | 115 |
\begin{isamarkuptext}% |
116 |
\noindent |
|
11494 | 117 |
At this point, \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even well-typed. |
118 |
To make it well-typed, |
|
10305 | 119 |
we need to make lists a type of class \isa{ordrel}:% |
120 |
\end{isamarkuptext}% |
|
17175 | 121 |
\isamarkuptrue% |
17056 | 122 |
% |
123 |
\isadelimtheory |
|
124 |
% |
|
125 |
\endisadelimtheory |
|
126 |
% |
|
127 |
\isatagtheory |
|
128 |
% |
|
129 |
\endisatagtheory |
|
130 |
{\isafoldtheory}% |
|
131 |
% |
|
132 |
\isadelimtheory |
|
133 |
% |
|
134 |
\endisadelimtheory |
|
10305 | 135 |
\end{isabellebody}% |
136 |
%%% Local Variables: |
|
137 |
%%% mode: latex |
|
138 |
%%% TeX-master: "root" |
|
139 |
%%% End: |