summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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

3 subsubsection{*Controlled overloading with type classes*}

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 *}

13 axclass ordrel < "term"

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 *}

25 consts less :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool" (infixl "<<" 50)

26 le :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool" (infixl "<<=" 50)

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.

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 *}

38 instance bool :: ordrel

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 *}

47 by intro_classes

49 text{*\noindent

50 More interesting \isacommand{instance} proofs will arise below

51 in the context of proper axiomatic type classes.

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 *}

57 defs (overloaded)

58 le_bool_def: "P <<= Q \<equiv> P \<longrightarrow> Q"

59 less_bool_def: "P << Q \<equiv> \<not>P \<and> Q"

61 text{*\noindent

62 Now @{prop"False <<= P"} is provable

63 *}

65 lemma "False <<= P"

66 by(simp add: le_bool_def)

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