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