author | wenzelm |
Sun, 31 May 2009 15:29:43 +0200 | |
changeset 31316 | 39fe8093b1df |
parent 27169 | 89d5f117add3 |
child 31707 | 678d294a563c |
permissions | -rw-r--r-- |
17914 | 1 |
(*<*)theory Overloading imports Overloading1 begin(*>*) |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11494
diff
changeset
|
2 |
instance list :: (type)ordrel |
10305 | 3 |
by intro_classes |
4 |
||
5 |
text{*\noindent |
|
10328 | 6 |
This \isacommand{instance} declaration can be read like the declaration of |
11494 | 7 |
a function on types. The constructor @{text list} maps types of class @{text |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11494
diff
changeset
|
8 |
type} (all HOL types), to types of class @{text ordrel}; |
11494 | 9 |
in other words, |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11494
diff
changeset
|
10 |
if @{text"ty :: type"} then @{text"ty list :: ordrel"}. |
10328 | 11 |
Of course we should also define the meaning of @{text <<=} and |
12 |
@{text <<} on lists: |
|
10305 | 13 |
*} |
14 |
||
15 |
defs (overloaded) |
|
16 |
prefix_def: |
|
27169 | 17 |
"xs <<= (ys::'a list) \<equiv> \<exists>zs. ys = xs@zs" |
10305 | 18 |
strict_prefix_def: |
27169 | 19 |
"xs << (ys::'a list) \<equiv> xs <<= ys \<and> xs \<noteq> ys" |
20 |
||
10305 | 21 |
(*<*)end(*>*) |