%

\begin{isabellebody}%

\def\isabellecontext{Overloading{\isadigit{1}}}%

%

\isamarkupsubsubsection{Controlled Overloading with Type Classes%

}

%

\begin{isamarkuptext}%

We now start with the theory of ordering relations, which we want to phrase

in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}}

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

introduce the class \isa{ordrel}:%

\end{isamarkuptext}%

\isacommand{axclass}\ ordrel\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}%

\begin{isamarkuptext}%

\noindent

This introduces a new class \isa{ordrel} and makes it a subclass of

the predefined class \isa{term}\footnote{The quotes around \isa{term}

simply avoid the clash with the command \isacommand{term}.} --- \isa{term}

is the class of all HOL types, like ``Object'' in Java.

This is a degenerate form of axiomatic type class without any axioms.

Its sole purpose is to restrict the use of overloaded constants to meaningful

instances:%

\end{isamarkuptext}%

\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

\ \ \ \ \ \ \ 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}%

\begin{isamarkuptext}%

\noindent

Note that only one occurrence of a type variable in a type needs to be

constrained with a class; the constraint is propagated to the other

occurrences automatically.

So far there is not a single type of class \isa{ordrel}. To breathe life

into \isa{ordrel} we need to declare a type to be an \bfindex{instance} of

\isa{ordrel}:%

\end{isamarkuptext}%

\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ ordrel%

\begin{isamarkuptxt}%

\noindent

Command \isacommand{instance} actually starts a proof, namely that

\isa{bool} satisfies all axioms of \isa{ordrel}.

There are none, but we still need to finish that proof, which we do

by invoking a fixed predefined method:%

\end{isamarkuptxt}%

\isacommand{by}\ intro{\isacharunderscore}classes%

\begin{isamarkuptext}%

\noindent

More interesting \isacommand{instance} proofs will arise below

in the context of proper axiomatic type classes.

Although terms like \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} are now legal, we still need to say

what the relation symbols actually mean at type \isa{bool}:%

\end{isamarkuptext}%

\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline

le{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}P\ {\isacharless}{\isacharless}{\isacharequal}\ Q\ {\isasymequiv}\ P\ {\isasymlongrightarrow}\ Q{\isachardoublequote}\isanewline

less{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}P\ {\isacharless}{\isacharless}\ Q\ {\isasymequiv}\ {\isasymnot}P\ {\isasymand}\ Q{\isachardoublequote}%

\begin{isamarkuptext}%

\noindent

Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} is provable%

\end{isamarkuptext}%

\isacommand{lemma}\ {\isachardoublequote}False\ {\isacharless}{\isacharless}{\isacharequal}\ P{\isachardoublequote}\isanewline

\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}%

\begin{isamarkuptext}%

\noindent

whereas \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even welltyped. In order to make it welltyped

we need to make lists a type of class \isa{ordrel}:%

\end{isamarkuptext}%

\end{isabellebody}%

%%% Local Variables:

%%% mode: latex

%%% TeX-master: "root"

%%% End: