10305
|
1 |
(*<*)theory Overloading1 = Main:(*>*)
|
|
2 |
|
10885
|
3 |
subsubsection{*Controlled Overloading with Type Classes*}
|
10305
|
4 |
|
|
5 |
text{*
|
11494
|
6 |
We now start with the theory of ordering relations, which we shall phrase
|
11277
|
7 |
in terms of the two binary symbols @{text"<<"} and @{text"<<="}
|
|
8 |
to avoid clashes with @{text"<"} and @{text"\<le>"} in theory @{text
|
10305
|
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
|
10328
|
16 |
This introduces a new class @{text ordrel} and makes it a subclass of
|
11494
|
17 |
the predefined class @{text term}, which
|
|
18 |
is the class of all HOL types.\footnote{The quotes around @{text term}
|
|
19 |
simply avoid the clash with the command \isacommand{term}.}
|
10305
|
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
|
|
22 |
instances:
|
|
23 |
*}
|
|
24 |
|
10328
|
25 |
consts less :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool" (infixl "<<" 50)
|
|
26 |
le :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool" (infixl "<<=" 50)
|
|
27 |
|
|
28 |
text{*\noindent
|
10396
|
29 |
Note that only one occurrence of a type variable in a type needs to be
|
|
30 |
constrained with a class; the constraint is propagated to the other
|
|
31 |
occurrences automatically.
|
|
32 |
|
11494
|
33 |
So far there are no types of class @{text ordrel}. To breathe life
|
10328
|
34 |
into @{text ordrel} we need to declare a type to be an \bfindex{instance} of
|
|
35 |
@{text ordrel}:
|
|
36 |
*}
|
10305
|
37 |
|
|
38 |
instance bool :: ordrel
|
10328
|
39 |
|
|
40 |
txt{*\noindent
|
|
41 |
Command \isacommand{instance} actually starts a proof, namely that
|
|
42 |
@{typ bool} satisfies all axioms of @{text ordrel}.
|
|
43 |
There are none, but we still need to finish that proof, which we do
|
11494
|
44 |
by invoking the \methdx{intro_classes} method:
|
10328
|
45 |
*}
|
|
46 |
|
10305
|
47 |
by intro_classes
|
|
48 |
|
10328
|
49 |
text{*\noindent
|
|
50 |
More interesting \isacommand{instance} proofs will arise below
|
|
51 |
in the context of proper axiomatic type classes.
|
|
52 |
|
11161
|
53 |
Although terms like @{prop"False <<= P"} are now legal, we still need to say
|
10328
|
54 |
what the relation symbols actually mean at type @{typ bool}:
|
|
55 |
*}
|
|
56 |
|
10305
|
57 |
defs (overloaded)
|
|
58 |
le_bool_def: "P <<= Q \<equiv> P \<longrightarrow> Q"
|
|
59 |
less_bool_def: "P << Q \<equiv> \<not>P \<and> Q"
|
|
60 |
|
10328
|
61 |
text{*\noindent
|
11494
|
62 |
Now @{prop"False <<= P"} is provable:
|
10305
|
63 |
*}
|
|
64 |
|
10328
|
65 |
lemma "False <<= P"
|
10305
|
66 |
by(simp add: le_bool_def)
|
|
67 |
|
|
68 |
text{*\noindent
|
11494
|
69 |
At this point, @{text"[] <<= []"} is not even well-typed.
|
|
70 |
To make it well-typed,
|
10305
|
71 |
we need to make lists a type of class @{text ordrel}:*}(*<*)end(*>*)
|