10305
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{Overloading}%
|
|
4 |
\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isachardoublequote}term{\isachardoublequote}{\isacharparenright}ordrel\isanewline
|
|
5 |
\isacommand{by}\ intro{\isacharunderscore}classes%
|
|
6 |
\begin{isamarkuptext}%
|
|
7 |
\noindent
|
10328
|
8 |
This \isacommand{instance} declaration can be read like the declaration of
|
|
9 |
a function on types: the constructor \isa{list} maps types of class \isa{term}, i.e.\ all HOL types, to types of class \isa{ordrel}, i.e.\
|
|
10 |
if \isa{ty\ {\isacharcolon}{\isacharcolon}\ term} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}.
|
|
11 |
Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
|
|
12 |
\isa{{\isacharless}{\isacharless}} on lists:%
|
10305
|
13 |
\end{isamarkuptext}%
|
|
14 |
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
|
|
15 |
prefix{\isacharunderscore}def{\isacharcolon}\isanewline
|
|
16 |
\ \ {\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
|
|
17 |
strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharcolon}\isanewline
|
11196
|
18 |
\ \ {\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}\end{isabellebody}%
|
10305
|
19 |
%%% Local Variables:
|
|
20 |
%%% mode: latex
|
|
21 |
%%% TeX-master: "root"
|
|
22 |
%%% End:
|