10305
|
1 |
(*<*)theory Overloading = Overloading1:(*>*)
|
|
2 |
instance list :: ("term")ordrel
|
|
3 |
by intro_classes
|
|
4 |
|
|
5 |
text{*\noindent
|
10328
|
6 |
This \isacommand{instance} declaration can be read like the declaration of
|
|
7 |
a function on types: the constructor @{text list} maps types of class @{text
|
|
8 |
term}, i.e.\ all HOL types, to types of class @{text ordrel}, i.e.\
|
|
9 |
if @{text"ty :: term"} then @{text"ty list :: ordrel"}.
|
|
10 |
Of course we should also define the meaning of @{text <<=} and
|
|
11 |
@{text <<} on lists:
|
10305
|
12 |
*}
|
|
13 |
|
|
14 |
defs (overloaded)
|
|
15 |
prefix_def:
|
|
16 |
"xs <<= (ys::'a::ordrel list) \<equiv> \<exists>zs. ys = xs@zs"
|
|
17 |
strict_prefix_def:
|
|
18 |
"xs << (ys::'a::ordrel list) \<equiv> xs <<= ys \<and> xs \<noteq> ys"
|
|
19 |
|
|
20 |
text{*
|
|
21 |
We could also have made the second definition non-overloaded once and for
|
|
22 |
all: @{prop"x << y \<equiv> x <<= y \<and> x \<noteq> y"}. This would have saved us writing
|
|
23 |
many similar definitions at different types, but it would also have fixed
|
|
24 |
that @{text <<} is defined in terms of @{text <<=} and never the other way
|
|
25 |
around. Below you will see why we want to avoid this asymmetry.
|
|
26 |
*}
|
|
27 |
(*<*)end(*>*)
|