doc-src/TutorialI/Types/Overloading1.thy
author nipkow
Wed Dec 06 13:22:58 2000 +0100 (2000-12-06)
changeset 10608 620647438780
parent 10396 5ab08609e6c8
child 10885 90695f46440b
permissions -rw-r--r--
*** empty log message ***
nipkow@10305
     1
(*<*)theory Overloading1 = Main:(*>*)
nipkow@10305
     2
nipkow@10305
     3
subsubsection{*Controlled overloading with type classes*}
nipkow@10305
     4
nipkow@10305
     5
text{*
nipkow@10305
     6
We now start with the theory of ordering relations, which we want to phrase
nipkow@10305
     7
in terms of the two binary symbols @{text"<<"} and @{text"<<="}: they have
nipkow@10328
     8
been chosen to avoid clashes with @{text"<"} and @{text"\<le>"} in theory @{text
nipkow@10305
     9
Main}. To restrict the application of @{text"<<"} and @{text"<<="} we
nipkow@10305
    10
introduce the class @{text ordrel}:
nipkow@10305
    11
*}
nipkow@10305
    12
nipkow@10305
    13
axclass ordrel < "term"
nipkow@10305
    14
nipkow@10305
    15
text{*\noindent
nipkow@10328
    16
This introduces a new class @{text ordrel} and makes it a subclass of
nipkow@10328
    17
the predefined class @{text term}\footnote{The quotes around @{text term}
nipkow@10328
    18
simply avoid the clash with the command \isacommand{term}.}; @{text term}
nipkow@10328
    19
is the class of all HOL types, like ``Object'' in Java.
nipkow@10305
    20
This is a degenerate form of axiomatic type class without any axioms.
nipkow@10305
    21
Its sole purpose is to restrict the use of overloaded constants to meaningful
nipkow@10305
    22
instances:
nipkow@10305
    23
*}
nipkow@10305
    24
nipkow@10328
    25
consts less :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"     (infixl "<<"  50)
nipkow@10328
    26
       le   :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"     (infixl "<<=" 50)
nipkow@10328
    27
nipkow@10328
    28
text{*\noindent
nipkow@10396
    29
Note that only one occurrence of a type variable in a type needs to be
nipkow@10396
    30
constrained with a class; the constraint is propagated to the other
nipkow@10396
    31
occurrences automatically.
nipkow@10396
    32
nipkow@10328
    33
So far there is not a single type of class @{text ordrel}. To breathe life
nipkow@10328
    34
into @{text ordrel} we need to declare a type to be an \bfindex{instance} of
nipkow@10328
    35
@{text ordrel}:
nipkow@10328
    36
*}
nipkow@10305
    37
nipkow@10305
    38
instance bool :: ordrel
nipkow@10328
    39
nipkow@10328
    40
txt{*\noindent
nipkow@10328
    41
Command \isacommand{instance} actually starts a proof, namely that
nipkow@10328
    42
@{typ bool} satisfies all axioms of @{text ordrel}.
nipkow@10328
    43
There are none, but we still need to finish that proof, which we do
nipkow@10328
    44
by invoking a fixed predefined method:
nipkow@10328
    45
*}
nipkow@10328
    46
nipkow@10305
    47
by intro_classes
nipkow@10305
    48
nipkow@10328
    49
text{*\noindent
nipkow@10328
    50
More interesting \isacommand{instance} proofs will arise below
nipkow@10328
    51
in the context of proper axiomatic type classes.
nipkow@10328
    52
nipkow@10328
    53
Althoug terms like @{prop"False <<= P"} are now legal, we still need to say
nipkow@10328
    54
what the relation symbols actually mean at type @{typ bool}:
nipkow@10328
    55
*}
nipkow@10328
    56
nipkow@10305
    57
defs (overloaded)
nipkow@10305
    58
le_bool_def:  "P <<= Q \<equiv> P \<longrightarrow> Q"
nipkow@10305
    59
less_bool_def: "P << Q \<equiv> \<not>P \<and> Q"
nipkow@10305
    60
nipkow@10328
    61
text{*\noindent
nipkow@10328
    62
Now @{prop"False <<= P"} is provable
nipkow@10305
    63
*}
nipkow@10305
    64
nipkow@10328
    65
lemma "False <<= P"
nipkow@10305
    66
by(simp add: le_bool_def)
nipkow@10305
    67
nipkow@10305
    68
text{*\noindent
nipkow@10305
    69
whereas @{text"[] <<= []"} is not even welltyped. In order to make it welltyped
nipkow@10305
    70
we need to make lists a type of class @{text ordrel}:*}(*<*)end(*>*)