equal
deleted
inserted
replaced
|
1 (*<*)theory Overloading1 = Main:(*>*) |
|
2 |
|
3 subsubsection{*Controlled overloading with type classes*} |
|
4 |
|
5 text{* |
|
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 |
|
8 been chosen to avoid clashes with @{text"\<le>"} and @{text"<"} in theory @{text |
|
9 Main}. To restrict the application of @{text"<<"} and @{text"<<="} we |
|
10 introduce the class @{text ordrel}: |
|
11 *} |
|
12 |
|
13 axclass ordrel < "term" |
|
14 |
|
15 text{*\noindent |
|
16 This is a degenerate form of axiomatic type class without any axioms. |
|
17 Its sole purpose is to restrict the use of overloaded constants to meaningful |
|
18 instances: |
|
19 *} |
|
20 |
|
21 consts |
|
22 "<<" :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool" (infixl 50) |
|
23 "<<=" :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool" (infixl 50) |
|
24 |
|
25 instance bool :: ordrel |
|
26 by intro_classes |
|
27 |
|
28 defs (overloaded) |
|
29 le_bool_def: "P <<= Q \<equiv> P \<longrightarrow> Q" |
|
30 less_bool_def: "P << Q \<equiv> \<not>P \<and> Q" |
|
31 |
|
32 text{* |
|
33 Now @{prop"False <<= False"} is provable |
|
34 *} |
|
35 |
|
36 lemma "False <<= False" |
|
37 by(simp add: le_bool_def) |
|
38 |
|
39 text{*\noindent |
|
40 whereas @{text"[] <<= []"} is not even welltyped. In order to make it welltyped |
|
41 we need to make lists a type of class @{text ordrel}:*}(*<*)end(*>*) |