doc-src/TutorialI/Types/Overloading.thy
author nipkow
Wed Dec 06 13:22:58 2000 +0100 (2000-12-06)
changeset 10608 620647438780
parent 10328 bf33cbd76c05
child 11196 bb4ede27fcb7
permissions -rw-r--r--
*** empty log message ***
     1 (*<*)theory Overloading = Overloading1:(*>*)
     2 instance list :: ("term")ordrel
     3 by intro_classes
     4 
     5 text{*\noindent
     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:
    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(*>*)