doc-src/TutorialI/Types/Overloading.thy
author nipkow
Wed Mar 07 15:54:11 2001 +0100 (2001-03-07)
changeset 11196 bb4ede27fcb7
parent 10328 bf33cbd76c05
child 11494 23a118849801
permissions -rw-r--r--
*** empty log message ***
nipkow@10305
     1
(*<*)theory Overloading = Overloading1:(*>*)
nipkow@10305
     2
instance list :: ("term")ordrel
nipkow@10305
     3
by intro_classes
nipkow@10305
     4
nipkow@10305
     5
text{*\noindent
nipkow@10328
     6
This \isacommand{instance} declaration can be read like the declaration of
nipkow@10328
     7
a function on types: the constructor @{text list} maps types of class @{text
nipkow@10328
     8
term}, i.e.\ all HOL types, to types of class @{text ordrel}, i.e.\
nipkow@10328
     9
if @{text"ty :: term"} then @{text"ty list :: ordrel"}.
nipkow@10328
    10
Of course we should also define the meaning of @{text <<=} and
nipkow@10328
    11
@{text <<} on lists:
nipkow@10305
    12
*}
nipkow@10305
    13
nipkow@10305
    14
defs (overloaded)
nipkow@10305
    15
prefix_def:
nipkow@10305
    16
  "xs <<= (ys::'a::ordrel list)  \<equiv>  \<exists>zs. ys = xs@zs"
nipkow@10305
    17
strict_prefix_def:
nipkow@10305
    18
  "xs << (ys::'a::ordrel list)   \<equiv>  xs <<= ys \<and> xs \<noteq> ys"
nipkow@10305
    19
(*<*)end(*>*)