doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
author haftmann
Wed Oct 31 10:10:50 2007 +0100 (2007-10-31)
changeset 25247 7bacd1798fc4
parent 25200 f1d2e106f2fe
child 25533 0140cc7b26ad
permissions -rw-r--r--
tuned
haftmann@20967
     1
%
haftmann@20967
     2
\begin{isabellebody}%
haftmann@20967
     3
\def\isabellecontext{Classes}%
haftmann@20967
     4
%
haftmann@20967
     5
\isadelimtheory
haftmann@20967
     6
\isanewline
haftmann@20967
     7
%
haftmann@20967
     8
\endisadelimtheory
haftmann@20967
     9
%
haftmann@20967
    10
\isatagtheory
haftmann@22479
    11
%
haftmann@20967
    12
\endisatagtheory
haftmann@20967
    13
{\isafoldtheory}%
haftmann@20967
    14
%
haftmann@20967
    15
\isadelimtheory
haftmann@20967
    16
%
haftmann@20967
    17
\endisadelimtheory
haftmann@20967
    18
%
haftmann@20967
    19
\isadelimML
haftmann@22317
    20
%
haftmann@22317
    21
\endisadelimML
haftmann@22317
    22
%
haftmann@22317
    23
\isatagML
haftmann@22317
    24
%
haftmann@22317
    25
\endisatagML
haftmann@22317
    26
{\isafoldML}%
haftmann@22317
    27
%
haftmann@22317
    28
\isadelimML
haftmann@22317
    29
%
haftmann@22317
    30
\endisadelimML
haftmann@22317
    31
%
haftmann@22317
    32
\isadelimML
haftmann@20967
    33
%
haftmann@20967
    34
\endisadelimML
haftmann@20967
    35
%
haftmann@20967
    36
\isatagML
haftmann@20967
    37
%
haftmann@20967
    38
\endisatagML
haftmann@20967
    39
{\isafoldML}%
haftmann@20967
    40
%
haftmann@20967
    41
\isadelimML
haftmann@20967
    42
%
haftmann@20967
    43
\endisadelimML
haftmann@20967
    44
%
haftmann@20967
    45
\isamarkupchapter{Haskell-style classes with Isabelle/Isar%
haftmann@20967
    46
}
haftmann@20967
    47
\isamarkuptrue%
haftmann@20967
    48
%
haftmann@20967
    49
\isamarkupsection{Introduction%
haftmann@20967
    50
}
haftmann@20967
    51
\isamarkuptrue%
haftmann@20967
    52
%
haftmann@20967
    53
\begin{isamarkuptext}%
haftmann@22317
    54
Type classes were introduces by Wadler and Blott \cite{wadler89how}
haftmann@22317
    55
  into the Haskell language, to allow for a reasonable implementation
haftmann@22317
    56
  of overloading\footnote{throughout this tutorial, we are referring
haftmann@22317
    57
  to classical Haskell 1.0 type classes, not considering
haftmann@22317
    58
  later additions in expressiveness}.
haftmann@22317
    59
  As a canonical example, a polymorphic equality function
haftmann@22317
    60
  \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on different
haftmann@22550
    61
  types for \isa{{\isasymalpha}}, which is achieved by splitting introduction
haftmann@22317
    62
  of the \isa{eq} function from its overloaded definitions by means
haftmann@22317
    63
  of \isa{class} and \isa{instance} declarations:
haftmann@22317
    64
haftmann@22317
    65
  \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\
haftmann@22317
    66
  \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
haftmann@22317
    67
haftmann@22317
    68
  \medskip\noindent\hspace*{2ex}\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
haftmann@22317
    69
  \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\
haftmann@22317
    70
  \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\
haftmann@22317
    71
  \hspace*{4ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
haftmann@22317
    72
  \hspace*{4ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
haftmann@22317
    73
haftmann@22317
    74
  \medskip\noindent\hspace*{2ex}\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
haftmann@22550
    75
  \hspace*{4ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
haftmann@22317
    76
haftmann@22317
    77
  \medskip\noindent\hspace*{2ex}\isa{class\ ord\ extends\ eq\ where} \\
haftmann@22317
    78
  \hspace*{4ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
haftmann@22317
    79
  \hspace*{4ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
haftmann@22317
    80
haftmann@22550
    81
  \medskip\noindent Type variables are annotated with (finitly many) classes;
haftmann@22317
    82
  these annotations are assertions that a particular polymorphic type
haftmann@22317
    83
  provides definitions for overloaded functions.
haftmann@22317
    84
haftmann@22317
    85
  Indeed, type classes not only allow for simple overloading
haftmann@22317
    86
  but form a generic calculus, an instance of order-sorted
haftmann@23956
    87
  algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
haftmann@20967
    88
haftmann@22317
    89
  From a software enigineering point of view, type classes
haftmann@22317
    90
  correspond to interfaces in object-oriented languages like Java;
haftmann@22317
    91
  so, it is naturally desirable that type classes do not only
haftmann@24991
    92
  provide functions (class parameters) but also state specifications
haftmann@22317
    93
  implementations must obey.  For example, the \isa{class\ eq}
haftmann@22550
    94
  above could be given the following specification, demanding that
haftmann@22550
    95
  \isa{class\ eq} is an equivalence relation obeying reflexivity,
haftmann@22550
    96
  symmetry and transitivity:
haftmann@22317
    97
haftmann@22317
    98
  \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where} \\
haftmann@22317
    99
  \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
haftmann@22317
   100
  \hspace*{2ex}\isa{satisfying} \\
haftmann@22317
   101
  \hspace*{4ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
haftmann@22317
   102
  \hspace*{4ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
haftmann@22317
   103
  \hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
haftmann@22317
   104
haftmann@22550
   105
  \medskip\noindent From a theoretic point of view, type classes are leightweight
haftmann@22479
   106
  modules; Haskell type classes may be emulated by
haftmann@22317
   107
  SML functors \cite{classes_modules}. 
haftmann@22317
   108
  Isabelle/Isar offers a discipline of type classes which brings
haftmann@22317
   109
  all those aspects together:
haftmann@22317
   110
haftmann@22317
   111
  \begin{enumerate}
haftmann@25004
   112
    \item specifying abstract parameters together with
haftmann@22317
   113
       corresponding specifications,
haftmann@24991
   114
    \item instantating those abstract parameters by a particular
haftmann@22317
   115
       type
haftmann@22317
   116
    \item in connection with a ``less ad-hoc'' approach to overloading,
haftmann@23956
   117
    \item with a direct link to the Isabelle module system
haftmann@23956
   118
      (aka locales \cite{kammueller-locales}).
haftmann@22317
   119
  \end{enumerate}
haftmann@22317
   120
haftmann@22550
   121
  \noindent Isar type classes also directly support code generation
haftmann@22550
   122
  in a Haskell like fashion.
haftmann@22317
   123
haftmann@22317
   124
  This tutorial demonstrates common elements of structured specifications
haftmann@22317
   125
  and abstract reasoning with type classes by the algebraic hierarchy of
haftmann@22317
   126
  semigroups, monoids and groups.  Our background theory is that of
haftmann@23956
   127
  Isabelle/HOL \cite{isa-tutorial}, for which some
haftmann@22317
   128
  familiarity is assumed.
haftmann@22317
   129
haftmann@22317
   130
  Here we merely present the look-and-feel for end users.
haftmann@22317
   131
  Internally, those are mapped to more primitive Isabelle concepts.
haftmann@23956
   132
  See \cite{Haftmann-Wenzel:2006:classes} for more detail.%
haftmann@20967
   133
\end{isamarkuptext}%
haftmann@20967
   134
\isamarkuptrue%
haftmann@20967
   135
%
haftmann@20967
   136
\isamarkupsection{A simple algebra example \label{sec:example}%
haftmann@20967
   137
}
haftmann@20967
   138
\isamarkuptrue%
haftmann@20967
   139
%
haftmann@20967
   140
\isamarkupsubsection{Class definition%
haftmann@20967
   141
}
haftmann@20967
   142
\isamarkuptrue%
haftmann@20967
   143
%
haftmann@20967
   144
\begin{isamarkuptext}%
haftmann@24991
   145
Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operator \isa{{\isasymotimes}} that is
haftmann@20967
   146
  assumed to be associative:%
haftmann@20967
   147
\end{isamarkuptext}%
haftmann@20967
   148
\isamarkuptrue%
haftmann@20967
   149
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@22479
   150
\ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
haftmann@25200
   151
\ \ \ \ \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
haftmann@25200
   152
\ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
haftmann@20967
   153
\begin{isamarkuptext}%
haftmann@20967
   154
\noindent This \isa{{\isasymCLASS}} specification consists of two
haftmann@24991
   155
  parts: the \qn{operational} part names the class parameter (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them
haftmann@20967
   156
  (\isa{{\isasymASSUMES}}).  The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global
haftmann@24991
   157
  parameter \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
haftmann@22479
   158
  global theorem \isa{semigroup{\isachardot}assoc{\isacharcolon}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
haftmann@20967
   159
\end{isamarkuptext}%
haftmann@20967
   160
\isamarkuptrue%
haftmann@20967
   161
%
haftmann@20967
   162
\isamarkupsubsection{Class instantiation \label{sec:class_inst}%
haftmann@20967
   163
}
haftmann@20967
   164
\isamarkuptrue%
haftmann@20967
   165
%
haftmann@20967
   166
\begin{isamarkuptext}%
haftmann@20967
   167
The concrete type \isa{int} is made a \isa{semigroup}
haftmann@24991
   168
  instance by providing a suitable definition for the class parameter
haftmann@20967
   169
  \isa{mult} and a proof for the specification of \isa{assoc}.%
haftmann@20967
   170
\end{isamarkuptext}%
haftmann@20967
   171
\isamarkuptrue%
haftmann@20967
   172
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   173
\ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
haftmann@24628
   174
\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
haftmann@20967
   175
%
haftmann@20967
   176
\isadelimproof
haftmann@20967
   177
\ \ \ \ %
haftmann@20967
   178
\endisadelimproof
haftmann@20967
   179
%
haftmann@20967
   180
\isatagproof
haftmann@20967
   181
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   182
\isanewline
haftmann@22317
   183
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   184
\ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   185
\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   186
\ simp\isanewline
haftmann@22317
   187
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   188
\ \isacommand{show}\isamarkupfalse%
haftmann@25247
   189
\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@25247
   190
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   191
\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   192
\isanewline
haftmann@20967
   193
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   194
%
haftmann@20967
   195
\endisatagproof
haftmann@20967
   196
{\isafoldproof}%
haftmann@20967
   197
%
haftmann@20967
   198
\isadelimproof
haftmann@20967
   199
%
haftmann@20967
   200
\endisadelimproof
haftmann@20967
   201
%
haftmann@20967
   202
\begin{isamarkuptext}%
haftmann@20967
   203
\noindent From now on, the type-checker will consider \isa{int}
haftmann@20967
   204
  as a \isa{semigroup} automatically, i.e.\ any general results
haftmann@20967
   205
  are immediately available on concrete instances.
haftmann@20967
   206
haftmann@22317
   207
  Note that the first proof step is the \isa{default} method,
haftmann@22317
   208
  which for instantiation proofs maps to the \isa{intro{\isacharunderscore}classes} method.
haftmann@22317
   209
  This boils down an instantiation judgement to the relevant primitive
haftmann@22317
   210
  proof goals and should conveniently always be the first method applied
haftmann@22317
   211
  in an instantiation proof.
haftmann@22317
   212
haftmann@22550
   213
  \medskip Another instance of \isa{semigroup} are the natural numbers:%
haftmann@20967
   214
\end{isamarkuptext}%
haftmann@20967
   215
\isamarkuptrue%
haftmann@20967
   216
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   217
\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
haftmann@22317
   218
\ \ \ \ \ \ mult{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymequiv}\ m\ {\isacharplus}\ n{\isachardoublequoteclose}\isanewline
haftmann@20967
   219
%
haftmann@20967
   220
\isadelimproof
haftmann@20967
   221
\ \ \ \ %
haftmann@20967
   222
\endisadelimproof
haftmann@20967
   223
%
haftmann@20967
   224
\isatagproof
haftmann@20967
   225
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   226
\isanewline
haftmann@20967
   227
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   228
\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
haftmann@20967
   229
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@25247
   230
\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@25247
   231
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@22317
   232
\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   233
\ simp\isanewline
haftmann@20967
   234
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   235
%
haftmann@20967
   236
\endisatagproof
haftmann@20967
   237
{\isafoldproof}%
haftmann@20967
   238
%
haftmann@20967
   239
\isadelimproof
haftmann@20967
   240
%
haftmann@20967
   241
\endisadelimproof
haftmann@20967
   242
%
haftmann@25247
   243
\isamarkupsubsection{Lifting and parametric types%
haftmann@25247
   244
}
haftmann@25247
   245
\isamarkuptrue%
haftmann@25247
   246
%
haftmann@20967
   247
\begin{isamarkuptext}%
haftmann@25247
   248
Overloaded definitions giving on class instantiation
haftmann@25247
   249
  may include recursion over the syntactic structure of types.
haftmann@25247
   250
  As a canonical example, we model product semigroups
haftmann@25247
   251
  using our simple algebra:%
haftmann@20967
   252
\end{isamarkuptext}%
haftmann@20967
   253
\isamarkuptrue%
haftmann@20967
   254
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@25247
   255
\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
haftmann@25247
   256
\ \ \ \ \ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymequiv}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@20967
   257
%
haftmann@20967
   258
\isadelimproof
haftmann@20967
   259
\ \ \ \ %
haftmann@20967
   260
\endisadelimproof
haftmann@20967
   261
%
haftmann@20967
   262
\isatagproof
haftmann@20967
   263
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   264
\isanewline
haftmann@20967
   265
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@25247
   266
\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
haftmann@20967
   267
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@25247
   268
\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@25247
   269
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@25247
   270
\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@25247
   271
\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
haftmann@20967
   272
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   273
%
haftmann@20967
   274
\endisatagproof
haftmann@20967
   275
{\isafoldproof}%
haftmann@20967
   276
%
haftmann@20967
   277
\isadelimproof
haftmann@20967
   278
%
haftmann@20967
   279
\endisadelimproof
haftmann@20967
   280
%
haftmann@25247
   281
\begin{isamarkuptext}%
haftmann@25247
   282
\noindent Associativity from product semigroups is
haftmann@25247
   283
  established using
haftmann@25247
   284
  the definition of \isa{{\isasymotimes}} on products and the hypothetical
haftmann@25247
   285
  associativety of the type components;  these hypothesis
haftmann@25247
   286
  are facts due to the \isa{semigroup} constraints imposed
haftmann@25247
   287
  on the type components by the \isa{instance} proposition.
haftmann@25247
   288
  Indeed, this pattern often occurs with parametric types
haftmann@25247
   289
  and type classes.%
haftmann@25247
   290
\end{isamarkuptext}%
haftmann@25247
   291
\isamarkuptrue%
haftmann@25247
   292
%
haftmann@25247
   293
\isamarkupsubsection{Subclassing%
haftmann@20967
   294
}
haftmann@20967
   295
\isamarkuptrue%
haftmann@20967
   296
%
haftmann@20967
   297
\begin{isamarkuptext}%
haftmann@22317
   298
We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral)
haftmann@20967
   299
  by extending \isa{semigroup}
haftmann@24991
   300
  with one additional parameter \isa{neutral} together
haftmann@20967
   301
  with its property:%
haftmann@20967
   302
\end{isamarkuptext}%
haftmann@20967
   303
\isamarkuptrue%
haftmann@20967
   304
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@20967
   305
\ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
haftmann@25200
   306
\ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
haftmann@25200
   307
\ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
haftmann@20967
   308
\begin{isamarkuptext}%
haftmann@25247
   309
\noindent Again, we prove some instances, by
haftmann@24991
   310
  providing suitable parameter definitions and proofs for the
haftmann@25247
   311
  additional specifications:%
haftmann@20967
   312
\end{isamarkuptext}%
haftmann@20967
   313
\isamarkuptrue%
haftmann@20967
   314
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   315
\ nat\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
haftmann@22317
   316
\ \ \ \ \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
haftmann@20967
   317
%
haftmann@20967
   318
\isadelimproof
haftmann@20967
   319
\ \ \ \ %
haftmann@20967
   320
\endisadelimproof
haftmann@20967
   321
%
haftmann@20967
   322
\isatagproof
haftmann@20967
   323
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   324
\isanewline
haftmann@20967
   325
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   326
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
haftmann@20967
   327
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@25247
   328
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
haftmann@25247
   329
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   330
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   331
\ simp\isanewline
haftmann@20967
   332
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   333
%
haftmann@20967
   334
\endisatagproof
haftmann@20967
   335
{\isafoldproof}%
haftmann@20967
   336
%
haftmann@20967
   337
\isadelimproof
haftmann@20967
   338
\isanewline
haftmann@20967
   339
%
haftmann@20967
   340
\endisadelimproof
haftmann@20967
   341
\isanewline
haftmann@20967
   342
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   343
\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
haftmann@22317
   344
\ \ \ \ \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
haftmann@20967
   345
%
haftmann@20967
   346
\isadelimproof
haftmann@20967
   347
\ \ \ \ %
haftmann@20967
   348
\endisadelimproof
haftmann@20967
   349
%
haftmann@20967
   350
\isatagproof
haftmann@20967
   351
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   352
\isanewline
haftmann@20967
   353
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   354
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
haftmann@20967
   355
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@25247
   356
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
haftmann@25247
   357
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   358
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   359
\ simp\isanewline
haftmann@20967
   360
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   361
%
haftmann@20967
   362
\endisatagproof
haftmann@20967
   363
{\isafoldproof}%
haftmann@20967
   364
%
haftmann@20967
   365
\isadelimproof
haftmann@20967
   366
\isanewline
haftmann@20967
   367
%
haftmann@20967
   368
\endisadelimproof
haftmann@20967
   369
\isanewline
haftmann@20967
   370
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@25247
   371
\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
haftmann@25247
   372
\ \ \ \ \ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@20967
   373
%
haftmann@20967
   374
\isadelimproof
haftmann@20967
   375
\ \ \ \ %
haftmann@20967
   376
\endisadelimproof
haftmann@20967
   377
%
haftmann@20967
   378
\isatagproof
haftmann@20967
   379
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   380
\isanewline
haftmann@20967
   381
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@25247
   382
\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoidl\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline
haftmann@20967
   383
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@25247
   384
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
haftmann@25247
   385
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@25247
   386
\ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@25247
   387
\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutl{\isacharparenright}\isanewline
haftmann@20967
   388
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   389
%
haftmann@20967
   390
\endisatagproof
haftmann@20967
   391
{\isafoldproof}%
haftmann@20967
   392
%
haftmann@20967
   393
\isadelimproof
haftmann@20967
   394
%
haftmann@20967
   395
\endisadelimproof
haftmann@20967
   396
%
haftmann@20967
   397
\begin{isamarkuptext}%
haftmann@22317
   398
\noindent Fully-fledged monoids are modelled by another subclass
haftmann@24991
   399
  which does not add new parameters but tightens the specification:%
haftmann@20967
   400
\end{isamarkuptext}%
haftmann@20967
   401
\isamarkuptrue%
haftmann@20967
   402
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@20967
   403
\ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
haftmann@25247
   404
\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
haftmann@25247
   405
\isanewline
haftmann@20967
   406
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@25247
   407
\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline
haftmann@20967
   408
%
haftmann@20967
   409
\isadelimproof
haftmann@20967
   410
\ \ \ \ %
haftmann@20967
   411
\endisadelimproof
haftmann@20967
   412
%
haftmann@20967
   413
\isatagproof
haftmann@20967
   414
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   415
\isanewline
haftmann@20967
   416
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   417
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
haftmann@20967
   418
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@25247
   419
\ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
haftmann@25247
   420
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   421
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   422
\ simp\isanewline
haftmann@25247
   423
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@25247
   424
%
haftmann@25247
   425
\endisatagproof
haftmann@25247
   426
{\isafoldproof}%
haftmann@25247
   427
%
haftmann@25247
   428
\isadelimproof
haftmann@25247
   429
\isanewline
haftmann@25247
   430
%
haftmann@25247
   431
\endisadelimproof
haftmann@25247
   432
\isanewline
haftmann@25247
   433
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@25247
   434
\ int\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
haftmann@25247
   435
%
haftmann@25247
   436
\isadelimproof
haftmann@25247
   437
\ \ \ \ %
haftmann@25247
   438
\endisadelimproof
haftmann@25247
   439
%
haftmann@25247
   440
\isatagproof
haftmann@25247
   441
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   442
\isanewline
haftmann@20967
   443
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   444
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
haftmann@20967
   445
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@25247
   446
\ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
haftmann@25247
   447
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   448
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   449
\ simp\isanewline
haftmann@25247
   450
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@25247
   451
%
haftmann@25247
   452
\endisatagproof
haftmann@25247
   453
{\isafoldproof}%
haftmann@25247
   454
%
haftmann@25247
   455
\isadelimproof
haftmann@20967
   456
\isanewline
haftmann@25247
   457
%
haftmann@25247
   458
\endisadelimproof
haftmann@20967
   459
\isanewline
haftmann@25247
   460
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@25247
   461
\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
haftmann@25247
   462
%
haftmann@25247
   463
\isadelimproof
haftmann@25247
   464
\ \ \ \ %
haftmann@25247
   465
\endisadelimproof
haftmann@25247
   466
%
haftmann@25247
   467
\isatagproof
haftmann@25247
   468
\isacommand{proof}\isamarkupfalse%
haftmann@25247
   469
\ \isanewline
haftmann@25247
   470
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@25247
   471
\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoid\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}monoid{\isachardoublequoteclose}\isanewline
haftmann@25247
   472
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@25247
   473
\ {\isachardoublequoteopen}p\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
haftmann@25247
   474
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@25247
   475
\ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@25247
   476
\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutr{\isacharparenright}\isanewline
haftmann@20967
   477
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   478
%
haftmann@20967
   479
\endisatagproof
haftmann@20967
   480
{\isafoldproof}%
haftmann@20967
   481
%
haftmann@20967
   482
\isadelimproof
haftmann@20967
   483
%
haftmann@20967
   484
\endisadelimproof
haftmann@22317
   485
%
haftmann@22317
   486
\begin{isamarkuptext}%
haftmann@22317
   487
\noindent To finish our small algebra example, we add a \isa{group} class
haftmann@22317
   488
  with a corresponding instance:%
haftmann@22317
   489
\end{isamarkuptext}%
haftmann@22317
   490
\isamarkuptrue%
haftmann@20967
   491
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@20967
   492
\ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
haftmann@25200
   493
\ \ \ \ \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
haftmann@25200
   494
\ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
haftmann@20967
   495
\isanewline
haftmann@20967
   496
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   497
\ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
haftmann@22317
   498
\ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymequiv}\ {\isacharminus}\ i{\isachardoublequoteclose}\isanewline
haftmann@20967
   499
%
haftmann@20967
   500
\isadelimproof
haftmann@20967
   501
\ \ \ \ %
haftmann@20967
   502
\endisadelimproof
haftmann@20967
   503
%
haftmann@20967
   504
\isatagproof
haftmann@20967
   505
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   506
\isanewline
haftmann@20967
   507
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   508
\ i\ {\isacharcolon}{\isacharcolon}\ int\isanewline
haftmann@20967
   509
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
haftmann@20967
   510
\ {\isachardoublequoteopen}{\isacharminus}i\ {\isacharplus}\ i\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   511
\ simp\isanewline
haftmann@20967
   512
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   513
\ \isacommand{show}\isamarkupfalse%
haftmann@22550
   514
\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
haftmann@25247
   515
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@25247
   516
\ mult{\isacharunderscore}int{\isacharunderscore}def\ neutral{\isacharunderscore}int{\isacharunderscore}def\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   517
\isanewline
haftmann@20967
   518
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   519
%
haftmann@20967
   520
\endisatagproof
haftmann@20967
   521
{\isafoldproof}%
haftmann@20967
   522
%
haftmann@20967
   523
\isadelimproof
haftmann@20967
   524
%
haftmann@20967
   525
\endisadelimproof
haftmann@20967
   526
%
haftmann@22317
   527
\isamarkupsection{Type classes as locales%
haftmann@22317
   528
}
haftmann@22317
   529
\isamarkuptrue%
haftmann@22317
   530
%
haftmann@22317
   531
\isamarkupsubsection{A look behind the scene%
haftmann@22317
   532
}
haftmann@22317
   533
\isamarkuptrue%
haftmann@22317
   534
%
haftmann@22317
   535
\begin{isamarkuptext}%
haftmann@22479
   536
The example above gives an impression how Isar type classes work
haftmann@22479
   537
  in practice.  As stated in the introduction, classes also provide
haftmann@22479
   538
  a link to Isar's locale system.  Indeed, the logical core of a class
haftmann@22479
   539
  is nothing else than a locale:%
haftmann@22479
   540
\end{isamarkuptext}%
haftmann@22479
   541
\isamarkuptrue%
haftmann@22479
   542
\isacommand{class}\isamarkupfalse%
haftmann@22479
   543
\ idem\ {\isacharequal}\ type\ {\isacharplus}\isanewline
haftmann@22479
   544
\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
haftmann@22479
   545
\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
haftmann@22479
   546
\begin{isamarkuptext}%
haftmann@22479
   547
\noindent essentially introduces the locale%
haftmann@22479
   548
\end{isamarkuptext}%
haftmann@22479
   549
\isamarkuptrue%
haftmann@22317
   550
%
haftmann@22479
   551
\isadelimML
haftmann@22479
   552
%
haftmann@22479
   553
\endisadelimML
haftmann@22479
   554
%
haftmann@22479
   555
\isatagML
haftmann@22479
   556
%
haftmann@22479
   557
\endisatagML
haftmann@22479
   558
{\isafoldML}%
haftmann@22479
   559
%
haftmann@22479
   560
\isadelimML
haftmann@22479
   561
%
haftmann@22479
   562
\endisadelimML
haftmann@22479
   563
\isacommand{locale}\isamarkupfalse%
haftmann@22479
   564
\ idem\ {\isacharequal}\isanewline
haftmann@22479
   565
\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
haftmann@22479
   566
\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
haftmann@22479
   567
\begin{isamarkuptext}%
haftmann@22550
   568
\noindent together with corresponding constant(s):%
haftmann@22479
   569
\end{isamarkuptext}%
haftmann@22479
   570
\isamarkuptrue%
haftmann@22479
   571
\isacommand{consts}\isamarkupfalse%
haftmann@22550
   572
\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
haftmann@22550
   573
\begin{isamarkuptext}%
haftmann@22550
   574
\noindent The connection to the type system is done by means
haftmann@22550
   575
  of a primitive axclass%
haftmann@22550
   576
\end{isamarkuptext}%
haftmann@22550
   577
\isamarkuptrue%
haftmann@22479
   578
\isacommand{axclass}\isamarkupfalse%
haftmann@22479
   579
\ idem\ {\isacharless}\ type\isanewline
haftmann@22479
   580
\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
haftmann@22479
   581
\begin{isamarkuptext}%
wenzelm@22649
   582
\noindent together with a corresponding interpretation:%
haftmann@22479
   583
\end{isamarkuptext}%
haftmann@22479
   584
\isamarkuptrue%
haftmann@22479
   585
\isacommand{interpretation}\isamarkupfalse%
haftmann@22479
   586
\ idem{\isacharunderscore}class{\isacharcolon}\isanewline
haftmann@22479
   587
\ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isacharprime}a{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
haftmann@22479
   588
%
haftmann@22479
   589
\isadelimproof
haftmann@22479
   590
%
haftmann@22479
   591
\endisadelimproof
haftmann@22479
   592
%
haftmann@22479
   593
\isatagproof
haftmann@22479
   594
\isacommand{by}\isamarkupfalse%
haftmann@22550
   595
\ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ idem{\isacharparenright}%
haftmann@22479
   596
\endisatagproof
haftmann@22479
   597
{\isafoldproof}%
haftmann@22479
   598
%
haftmann@22479
   599
\isadelimproof
haftmann@22479
   600
%
haftmann@22479
   601
\endisadelimproof
haftmann@22479
   602
%
haftmann@22479
   603
\isadelimML
haftmann@22479
   604
%
haftmann@22479
   605
\endisadelimML
haftmann@22479
   606
%
haftmann@22479
   607
\isatagML
haftmann@22479
   608
%
haftmann@22479
   609
\endisatagML
haftmann@22479
   610
{\isafoldML}%
haftmann@22479
   611
%
haftmann@22479
   612
\isadelimML
haftmann@22479
   613
%
haftmann@22479
   614
\endisadelimML
haftmann@22479
   615
%
haftmann@22479
   616
\begin{isamarkuptext}%
haftmann@22479
   617
This give you at hand the full power of the Isabelle module system;
haftmann@22479
   618
  conclusions in locale \isa{idem} are implicitly propagated
haftmann@22479
   619
  to class \isa{idem}.%
haftmann@22317
   620
\end{isamarkuptext}%
haftmann@22317
   621
\isamarkuptrue%
haftmann@22317
   622
%
haftmann@20967
   623
\isamarkupsubsection{Abstract reasoning%
haftmann@20967
   624
}
haftmann@20967
   625
\isamarkuptrue%
haftmann@20967
   626
%
haftmann@20967
   627
\begin{isamarkuptext}%
haftmann@22479
   628
Isabelle locales enable reasoning at a general level, while results
haftmann@20967
   629
  are implicitly transferred to all instances.  For example, we can
haftmann@20967
   630
  now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which
haftmann@25247
   631
  states that the function \isa{{\isacharparenleft}x\ {\isasymotimes}{\isacharparenright}} is injective:%
haftmann@20967
   632
\end{isamarkuptext}%
haftmann@20967
   633
\isamarkuptrue%
haftmann@20967
   634
\ \ \ \ \isacommand{lemma}\isamarkupfalse%
haftmann@25200
   635
\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
haftmann@20967
   636
%
haftmann@20967
   637
\isadelimproof
haftmann@20967
   638
\ \ \ \ %
haftmann@20967
   639
\endisadelimproof
haftmann@20967
   640
%
haftmann@20967
   641
\isatagproof
haftmann@20967
   642
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   643
\isanewline
haftmann@25247
   644
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
haftmann@25200
   645
\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
haftmann@22479
   646
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   647
\ \isacommand{have}\isamarkupfalse%
haftmann@25200
   648
\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   649
\ simp\isanewline
haftmann@22479
   650
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   651
\ \isacommand{have}\isamarkupfalse%
haftmann@25200
   652
\ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
haftmann@20967
   653
\ assoc\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   654
\ simp\isanewline
haftmann@22479
   655
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   656
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   657
\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
haftmann@20967
   658
\ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   659
\ simp\isanewline
haftmann@20967
   660
\ \ \ \ \isacommand{next}\isamarkupfalse%
haftmann@20967
   661
\isanewline
haftmann@25247
   662
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
haftmann@20967
   663
\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
haftmann@22479
   664
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   665
\ \isacommand{show}\isamarkupfalse%
haftmann@25200
   666
\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   667
\ simp\isanewline
haftmann@20967
   668
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   669
%
haftmann@20967
   670
\endisatagproof
haftmann@20967
   671
{\isafoldproof}%
haftmann@20967
   672
%
haftmann@20967
   673
\isadelimproof
haftmann@20967
   674
%
haftmann@20967
   675
\endisadelimproof
haftmann@20967
   676
%
haftmann@20967
   677
\begin{isamarkuptext}%
haftmann@20967
   678
\noindent Here the \qt{\isa{{\isasymIN}\ group}} target specification
haftmann@20967
   679
  indicates that the result is recorded within that context for later
haftmann@22479
   680
  use.  This local theorem is also lifted to the global one \isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.  Since type \isa{int} has been made an instance of
haftmann@22479
   681
  \isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.%
haftmann@20967
   682
\end{isamarkuptext}%
haftmann@20967
   683
\isamarkuptrue%
haftmann@20967
   684
%
haftmann@23956
   685
\isamarkupsubsection{Derived definitions%
haftmann@23956
   686
}
haftmann@23956
   687
\isamarkuptrue%
haftmann@23956
   688
%
haftmann@23956
   689
\begin{isamarkuptext}%
haftmann@23956
   690
Isabelle locales support a concept of local definitions
haftmann@23956
   691
  in locales:%
haftmann@23956
   692
\end{isamarkuptext}%
haftmann@23956
   693
\isamarkuptrue%
haftmann@23956
   694
\ \ \ \ \isacommand{fun}\isamarkupfalse%
haftmann@23956
   695
\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\isanewline
haftmann@23956
   696
\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@25200
   697
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
haftmann@25200
   698
\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}%
haftmann@23956
   699
\begin{isamarkuptext}%
haftmann@23956
   700
\noindent If the locale \isa{group} is also a class, this local
haftmann@23956
   701
  definition is propagated onto a global definition of
haftmann@23956
   702
  \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}}
haftmann@23956
   703
  with corresponding theorems
haftmann@23956
   704
haftmann@23956
   705
  \isa{pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}\isasep\isanewline%
haftmann@23956
   706
pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x}.
haftmann@23956
   707
haftmann@23956
   708
  \noindent As you can see from this example, for local
haftmann@23956
   709
  definitions you may use any specification tool
haftmann@23956
   710
  which works together with locales (e.g. \cite{krauss2006}).%
haftmann@23956
   711
\end{isamarkuptext}%
haftmann@23956
   712
\isamarkuptrue%
haftmann@23956
   713
%
haftmann@25247
   714
\isamarkupsubsection{A functor analogy%
haftmann@25247
   715
}
haftmann@25247
   716
\isamarkuptrue%
haftmann@25247
   717
%
haftmann@25247
   718
\begin{isamarkuptext}%
haftmann@25247
   719
We introduced Isar classes by analogy to type classes
haftmann@25247
   720
  functional programming;  if we reconsider this in the
haftmann@25247
   721
  context of what has been said about type classes and locales,
haftmann@25247
   722
  we can drive this analogy further by stating that type
haftmann@25247
   723
  classes essentially correspond to functors which have
haftmann@25247
   724
  a canonical interpretation as type classes.
haftmann@25247
   725
  Anyway, there is also the possibility of other interpretations.
haftmann@25247
   726
  For example, also \isa{list}s form a monoid with
haftmann@25247
   727
  \isa{op\ {\isacharat}} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
haftmann@25247
   728
  seems inappropriate to apply to lists
haftmann@25247
   729
  the same operations as for genuinly algebraic types.
haftmann@25247
   730
  In such a case, we simply can do a particular interpretation
haftmann@25247
   731
  of monoids for lists:%
haftmann@25247
   732
\end{isamarkuptext}%
haftmann@25247
   733
\isamarkuptrue%
haftmann@25247
   734
\ \ \ \ \isacommand{interpretation}\isamarkupfalse%
haftmann@25247
   735
\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
haftmann@25247
   736
%
haftmann@25247
   737
\isadelimproof
haftmann@25247
   738
\ \ \ \ \ \ %
haftmann@25247
   739
\endisadelimproof
haftmann@25247
   740
%
haftmann@25247
   741
\isatagproof
haftmann@25247
   742
\isacommand{by}\isamarkupfalse%
haftmann@25247
   743
\ unfold{\isacharunderscore}locales\ auto%
haftmann@25247
   744
\endisatagproof
haftmann@25247
   745
{\isafoldproof}%
haftmann@25247
   746
%
haftmann@25247
   747
\isadelimproof
haftmann@25247
   748
%
haftmann@25247
   749
\endisadelimproof
haftmann@25247
   750
%
haftmann@25247
   751
\begin{isamarkuptext}%
haftmann@25247
   752
\noindent This enables us to apply facts on monoids
haftmann@25247
   753
  to lists, e.g. \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ x\ {\isacharequal}\ x}.
haftmann@25247
   754
haftmann@25247
   755
  When using this interpretation pattern, it may also
haftmann@25247
   756
  be appropriate to map derived definitions accordingly:%
haftmann@25247
   757
\end{isamarkuptext}%
haftmann@25247
   758
\isamarkuptrue%
haftmann@25247
   759
\ \ \ \ \isacommand{fun}\isamarkupfalse%
haftmann@25247
   760
\isanewline
haftmann@25247
   761
\ \ \ \ \ \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
haftmann@25247
   762
\ \ \ \ \isakeyword{where}\isanewline
haftmann@25247
   763
\ \ \ \ \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
haftmann@25247
   764
\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
haftmann@25247
   765
\isanewline
haftmann@25247
   766
\ \ \ \ \isacommand{interpretation}\isamarkupfalse%
haftmann@25247
   767
\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline
haftmann@25247
   768
\ \ \ \ \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
haftmann@25247
   769
%
haftmann@25247
   770
\isadelimproof
haftmann@25247
   771
\ \ \ \ %
haftmann@25247
   772
\endisadelimproof
haftmann@25247
   773
%
haftmann@25247
   774
\isatagproof
haftmann@25247
   775
\isacommand{proof}\isamarkupfalse%
haftmann@25247
   776
\isanewline
haftmann@25247
   777
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@25247
   778
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
haftmann@25247
   779
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@25247
   780
\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
haftmann@25247
   781
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
haftmann@25247
   782
\ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline
haftmann@25247
   783
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@25247
   784
%
haftmann@25247
   785
\endisatagproof
haftmann@25247
   786
{\isafoldproof}%
haftmann@25247
   787
%
haftmann@25247
   788
\isadelimproof
haftmann@25247
   789
%
haftmann@25247
   790
\endisadelimproof
haftmann@25247
   791
%
haftmann@24991
   792
\isamarkupsubsection{Additional subclass relations%
haftmann@24991
   793
}
haftmann@24991
   794
\isamarkuptrue%
haftmann@24991
   795
%
haftmann@24991
   796
\begin{isamarkuptext}%
haftmann@24991
   797
Any \isa{group} is also a \isa{monoid};  this
haftmann@25247
   798
  can be made explicit by claiming an additional
haftmann@25247
   799
  subclass relation,
haftmann@24991
   800
  together with a proof of the logical difference:%
haftmann@24991
   801
\end{isamarkuptext}%
haftmann@24991
   802
\isamarkuptrue%
haftmann@24991
   803
\ \ \ \ \isacommand{subclass}\isamarkupfalse%
haftmann@24991
   804
\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ monoid\isanewline
haftmann@24991
   805
%
haftmann@24991
   806
\isadelimproof
haftmann@24991
   807
\ \ \ \ %
haftmann@24991
   808
\endisadelimproof
haftmann@24991
   809
%
haftmann@24991
   810
\isatagproof
haftmann@24991
   811
\isacommand{proof}\isamarkupfalse%
haftmann@24991
   812
\ unfold{\isacharunderscore}locales\isanewline
haftmann@24991
   813
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@24991
   814
\ x\isanewline
haftmann@24991
   815
\ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
haftmann@24991
   816
\ invl\ \isacommand{have}\isamarkupfalse%
haftmann@25200
   817
\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@24991
   818
\ simp\isanewline
haftmann@24991
   819
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
haftmann@24991
   820
\ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
haftmann@25200
   821
\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ {\isasymone}{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@24991
   822
\ simp\isanewline
haftmann@24991
   823
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
haftmann@24991
   824
\ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse%
haftmann@25200
   825
\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@24991
   826
\ simp\isanewline
haftmann@24991
   827
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@24991
   828
%
haftmann@24991
   829
\endisatagproof
haftmann@24991
   830
{\isafoldproof}%
haftmann@24991
   831
%
haftmann@24991
   832
\isadelimproof
haftmann@24991
   833
%
haftmann@24991
   834
\endisadelimproof
haftmann@24991
   835
%
haftmann@24991
   836
\begin{isamarkuptext}%
haftmann@25200
   837
\noindent The logical proof is carried out on the locale level
haftmann@24991
   838
  and thus conveniently is opened using the \isa{unfold{\isacharunderscore}locales}
haftmann@24991
   839
  method which only leaves the logical differences still
haftmann@25200
   840
  open to proof to the user.  Afterwards it is propagated
haftmann@24991
   841
  to the type system, making \isa{group} an instance of
haftmann@25247
   842
  \isa{monoid} by adding an additional edge
haftmann@25247
   843
  to the graph of subclass relations
haftmann@25247
   844
  (cf.\ \figref{fig:subclass}).
haftmann@25247
   845
haftmann@25247
   846
  \begin{figure}[htbp]
haftmann@25247
   847
   \begin{center}
haftmann@25247
   848
     \small
haftmann@25247
   849
     \unitlength 0.6mm
haftmann@25247
   850
     \begin{picture}(40,60)(0,0)
haftmann@25247
   851
       \put(20,60){\makebox(0,0){\isa{semigroup}}}
haftmann@25247
   852
       \put(20,40){\makebox(0,0){\isa{monoidl}}}
haftmann@25247
   853
       \put(00,20){\makebox(0,0){\isa{monoid}}}
haftmann@25247
   854
       \put(40,00){\makebox(0,0){\isa{group}}}
haftmann@25247
   855
       \put(20,55){\vector(0,-1){10}}
haftmann@25247
   856
       \put(15,35){\vector(-1,-1){10}}
haftmann@25247
   857
       \put(25,35){\vector(1,-3){10}}
haftmann@25247
   858
     \end{picture}
haftmann@25247
   859
     \hspace{8em}
haftmann@25247
   860
     \begin{picture}(40,60)(0,0)
haftmann@25247
   861
       \put(20,60){\makebox(0,0){\isa{semigroup}}}
haftmann@25247
   862
       \put(20,40){\makebox(0,0){\isa{monoidl}}}
haftmann@25247
   863
       \put(00,20){\makebox(0,0){\isa{monoid}}}
haftmann@25247
   864
       \put(40,00){\makebox(0,0){\isa{group}}}
haftmann@25247
   865
       \put(20,55){\vector(0,-1){10}}
haftmann@25247
   866
       \put(15,35){\vector(-1,-1){10}}
haftmann@25247
   867
       \put(05,15){\vector(3,-1){30}}
haftmann@25247
   868
     \end{picture}
haftmann@25247
   869
     \caption{Subclass relationship of monoids and groups:
haftmann@25247
   870
        before and after establishing the relationship
haftmann@25247
   871
        \isa{group\ {\isasymsubseteq}\ monoid};  transitive edges left out.}
haftmann@25247
   872
     \label{fig:subclass}
haftmann@25247
   873
   \end{center}
haftmann@25247
   874
  \end{figure}
haftmann@25247
   875
haftmann@25247
   876
  For illustration, a derived definition
haftmann@24991
   877
  in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
haftmann@24991
   878
\end{isamarkuptext}%
haftmann@24991
   879
\isamarkuptrue%
haftmann@24991
   880
\ \ \ \ \isacommand{definition}\isamarkupfalse%
haftmann@24991
   881
\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\isanewline
haftmann@24991
   882
\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@24991
   883
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
haftmann@24991
   884
\ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
haftmann@25200
   885
\ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
haftmann@24991
   886
\begin{isamarkuptext}%
haftmann@25247
   887
\noindent yields the global definition of
haftmann@24991
   888
  \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
haftmann@24991
   889
  with the corresponding theorem \isa{pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{0}}\ {\isasymle}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}}.%
haftmann@24991
   890
\end{isamarkuptext}%
haftmann@24991
   891
\isamarkuptrue%
haftmann@24991
   892
%
haftmann@25247
   893
\isamarkupsection{Type classes and code generation%
haftmann@20967
   894
}
haftmann@20967
   895
\isamarkuptrue%
haftmann@20967
   896
%
haftmann@20967
   897
\begin{isamarkuptext}%
haftmann@22317
   898
Turning back to the first motivation for type classes,
haftmann@22317
   899
  namely overloading, it is obvious that overloading
haftmann@22317
   900
  stemming from \isa{{\isasymCLASS}} and \isa{{\isasymINSTANCE}}
haftmann@22317
   901
  statements naturally maps to Haskell type classes.
haftmann@22317
   902
  The code generator framework \cite{isabelle-codegen} 
haftmann@22317
   903
  takes this into account.  Concerning target languages
haftmann@22317
   904
  lacking type classes (e.g.~SML), type classes
haftmann@22317
   905
  are implemented by explicit dictionary construction.
haftmann@23956
   906
  For example, lets go back to the power function:%
haftmann@20967
   907
\end{isamarkuptext}%
haftmann@20967
   908
\isamarkuptrue%
haftmann@20967
   909
\ \ \ \ \isacommand{definition}\isamarkupfalse%
haftmann@20967
   910
\isanewline
haftmann@22317
   911
\ \ \ \ \ \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
haftmann@20967
   912
\ \ \ \ \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
haftmann@20967
   913
\begin{isamarkuptext}%
haftmann@22317
   914
\noindent This maps to Haskell as:%
haftmann@20967
   915
\end{isamarkuptext}%
haftmann@20967
   916
\isamarkuptrue%
haftmann@24628
   917
\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
haftmann@24628
   918
\ example\ \isakeyword{in}\ Haskell\ \isakeyword{module{\isacharunderscore}name}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}%
haftmann@20967
   919
\begin{isamarkuptext}%
haftmann@22317
   920
\lsthaskell{Thy/code_examples/Classes.hs}
haftmann@22317
   921
haftmann@22317
   922
  \noindent The whole code in SML with explicit dictionary passing:%
haftmann@22317
   923
\end{isamarkuptext}%
haftmann@22317
   924
\isamarkuptrue%
haftmann@24628
   925
\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
haftmann@24628
   926
\ example\ \isakeyword{in}\ SML\ \isakeyword{module{\isacharunderscore}name}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}%
haftmann@22317
   927
\begin{isamarkuptext}%
haftmann@22317
   928
\lstsml{Thy/code_examples/classes.ML}%
haftmann@20967
   929
\end{isamarkuptext}%
haftmann@20967
   930
\isamarkuptrue%
haftmann@20967
   931
%
haftmann@20967
   932
\isadelimtheory
haftmann@20967
   933
%
haftmann@20967
   934
\endisadelimtheory
haftmann@20967
   935
%
haftmann@20967
   936
\isatagtheory
haftmann@20967
   937
\isacommand{end}\isamarkupfalse%
haftmann@20967
   938
%
haftmann@20967
   939
\endisatagtheory
haftmann@20967
   940
{\isafoldtheory}%
haftmann@20967
   941
%
haftmann@20967
   942
\isadelimtheory
haftmann@20967
   943
%
haftmann@20967
   944
\endisadelimtheory
haftmann@20967
   945
\isanewline
haftmann@20967
   946
\end{isabellebody}%
haftmann@20967
   947
%%% Local Variables:
haftmann@20967
   948
%%% mode: latex
haftmann@20967
   949
%%% TeX-master: "root"
haftmann@20967
   950
%%% End: