2 |
2 |
3 subsubsection{*Controlled Overloading with Type Classes*} |
3 subsubsection{*Controlled Overloading with Type Classes*} |
4 |
4 |
5 text{* |
5 text{* |
6 We now start with the theory of ordering relations, which we want to phrase |
6 We now start with the theory of ordering relations, which we want to phrase |
7 in terms of the two binary symbols @{text"<<"} and @{text"<<="}: they have |
7 in terms of the two binary symbols @{text"<<"} and @{text"<<="} |
8 been chosen to avoid clashes with @{text"<"} and @{text"\<le>"} in theory @{text |
8 to avoid clashes with @{text"<"} and @{text"\<le>"} in theory @{text |
9 Main}. To restrict the application of @{text"<<"} and @{text"<<="} we |
9 Main}. To restrict the application of @{text"<<"} and @{text"<<="} we |
10 introduce the class @{text ordrel}: |
10 introduce the class @{text ordrel}: |
11 *} |
11 *} |
12 |
12 |
13 axclass ordrel < "term" |
13 axclass ordrel < "term" |
14 |
14 |
15 text{*\noindent |
15 text{*\noindent |
16 This introduces a new class @{text ordrel} and makes it a subclass of |
16 This introduces a new class @{text ordrel} and makes it a subclass of |
17 the predefined class @{text term}\footnote{The quotes around @{text term} |
17 the predefined class @{text term}\footnote{The quotes around @{text term} |
18 simply avoid the clash with the command \isacommand{term}.}; @{text term} |
18 simply avoid the clash with the command \isacommand{term}.} --- @{text term} |
19 is the class of all HOL types, like ``Object'' in Java. |
19 is the class of all HOL types, like ``Object'' in Java. |
20 This is a degenerate form of axiomatic type class without any axioms. |
20 This is a degenerate form of axiomatic type class without any axioms. |
21 Its sole purpose is to restrict the use of overloaded constants to meaningful |
21 Its sole purpose is to restrict the use of overloaded constants to meaningful |
22 instances: |
22 instances: |
23 *} |
23 *} |