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(*>*)