author | paulson |
Fri, 13 Dec 2002 16:48:20 +0100 | |
changeset 13750 | b5cd10cb106b |
parent 12338 | de0f4a63baa5 |
child 13778 | 61272514e3b5 |
permissions | -rw-r--r-- |
10305 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Overloading}% |
|
13750 | 4 |
\isanewline |
11866 | 5 |
\isamarkupfalse% |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11866
diff
changeset
|
6 |
\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}ordrel\isanewline |
11866 | 7 |
\isamarkupfalse% |
8 |
\isacommand{by}\ intro{\isacharunderscore}classes\isamarkupfalse% |
|
9 |
% |
|
10305 | 10 |
\begin{isamarkuptext}% |
11 |
\noindent |
|
10328 | 12 |
This \isacommand{instance} declaration can be read like the declaration of |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11866
diff
changeset
|
13 |
a function on types. The constructor \isa{list} maps types of class \isa{type} (all HOL types), to types of class \isa{ordrel}; |
11494 | 14 |
in other words, |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11866
diff
changeset
|
15 |
if \isa{ty\ {\isacharcolon}{\isacharcolon}\ type} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}. |
10328 | 16 |
Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and |
17 |
\isa{{\isacharless}{\isacharless}} on lists:% |
|
10305 | 18 |
\end{isamarkuptext}% |
11866 | 19 |
\isamarkuptrue% |
10305 | 20 |
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
21 |
prefix{\isacharunderscore}def{\isacharcolon}\isanewline |
|
22 |
\ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ {\isasymequiv}\ \ {\isasymexists}zs{\isachardot}\ ys\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline |
|
23 |
strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharcolon}\isanewline |
|
11866 | 24 |
\ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequote}\isamarkupfalse% |
13750 | 25 |
\isanewline |
11866 | 26 |
\isamarkupfalse% |
27 |
\end{isabellebody}% |
|
10305 | 28 |
%%% Local Variables: |
29 |
%%% mode: latex |
|
30 |
%%% TeX-master: "root" |
|
31 |
%%% End: |