doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
author haftmann
Tue Jul 24 15:21:54 2007 +0200 (2007-07-24)
changeset 23956 48494ccfabaf
parent 23015 e67f05cc0ac5
child 24628 33137422d7fd
permissions -rw-r--r--
updated
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
\isanewline
haftmann@20967
     8
%
haftmann@20967
     9
\endisadelimtheory
haftmann@20967
    10
%
haftmann@20967
    11
\isatagtheory
haftmann@22479
    12
%
haftmann@20967
    13
\endisatagtheory
haftmann@20967
    14
{\isafoldtheory}%
haftmann@20967
    15
%
haftmann@20967
    16
\isadelimtheory
haftmann@20967
    17
%
haftmann@20967
    18
\endisadelimtheory
haftmann@20967
    19
%
haftmann@20967
    20
\isadelimML
haftmann@22317
    21
%
haftmann@22317
    22
\endisadelimML
haftmann@22317
    23
%
haftmann@22317
    24
\isatagML
haftmann@22317
    25
%
haftmann@22317
    26
\endisatagML
haftmann@22317
    27
{\isafoldML}%
haftmann@22317
    28
%
haftmann@22317
    29
\isadelimML
haftmann@22317
    30
%
haftmann@22317
    31
\endisadelimML
haftmann@22317
    32
%
haftmann@22317
    33
\isadelimML
haftmann@20967
    34
%
haftmann@20967
    35
\endisadelimML
haftmann@20967
    36
%
haftmann@20967
    37
\isatagML
haftmann@20967
    38
%
haftmann@20967
    39
\endisatagML
haftmann@20967
    40
{\isafoldML}%
haftmann@20967
    41
%
haftmann@20967
    42
\isadelimML
haftmann@20967
    43
%
haftmann@20967
    44
\endisadelimML
haftmann@20967
    45
%
haftmann@20967
    46
\isamarkupchapter{Haskell-style classes with Isabelle/Isar%
haftmann@20967
    47
}
haftmann@20967
    48
\isamarkuptrue%
haftmann@20967
    49
%
haftmann@20967
    50
\isamarkupsection{Introduction%
haftmann@20967
    51
}
haftmann@20967
    52
\isamarkuptrue%
haftmann@20967
    53
%
haftmann@20967
    54
\begin{isamarkuptext}%
haftmann@22317
    55
Type classes were introduces by Wadler and Blott \cite{wadler89how}
haftmann@22317
    56
  into the Haskell language, to allow for a reasonable implementation
haftmann@22317
    57
  of overloading\footnote{throughout this tutorial, we are referring
haftmann@22317
    58
  to classical Haskell 1.0 type classes, not considering
haftmann@22317
    59
  later additions in expressiveness}.
haftmann@22317
    60
  As a canonical example, a polymorphic equality function
haftmann@22317
    61
  \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on different
haftmann@22550
    62
  types for \isa{{\isasymalpha}}, which is achieved by splitting introduction
haftmann@22317
    63
  of the \isa{eq} function from its overloaded definitions by means
haftmann@22317
    64
  of \isa{class} and \isa{instance} declarations:
haftmann@22317
    65
haftmann@22317
    66
  \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\
haftmann@22317
    67
  \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
haftmann@22317
    68
haftmann@22317
    69
  \medskip\noindent\hspace*{2ex}\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
haftmann@22317
    70
  \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\
haftmann@22317
    71
  \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\
haftmann@22317
    72
  \hspace*{4ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
haftmann@22317
    73
  \hspace*{4ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
haftmann@22317
    74
haftmann@22317
    75
  \medskip\noindent\hspace*{2ex}\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
haftmann@22550
    76
  \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
    77
haftmann@22317
    78
  \medskip\noindent\hspace*{2ex}\isa{class\ ord\ extends\ eq\ where} \\
haftmann@22317
    79
  \hspace*{4ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
haftmann@22317
    80
  \hspace*{4ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
haftmann@22317
    81
haftmann@22550
    82
  \medskip\noindent Type variables are annotated with (finitly many) classes;
haftmann@22317
    83
  these annotations are assertions that a particular polymorphic type
haftmann@22317
    84
  provides definitions for overloaded functions.
haftmann@22317
    85
haftmann@22317
    86
  Indeed, type classes not only allow for simple overloading
haftmann@22317
    87
  but form a generic calculus, an instance of order-sorted
haftmann@23956
    88
  algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
haftmann@20967
    89
haftmann@22317
    90
  From a software enigineering point of view, type classes
haftmann@22317
    91
  correspond to interfaces in object-oriented languages like Java;
haftmann@22317
    92
  so, it is naturally desirable that type classes do not only
haftmann@22317
    93
  provide functions (class operations) but also state specifications
haftmann@22317
    94
  implementations must obey.  For example, the \isa{class\ eq}
haftmann@22550
    95
  above could be given the following specification, demanding that
haftmann@22550
    96
  \isa{class\ eq} is an equivalence relation obeying reflexivity,
haftmann@22550
    97
  symmetry and transitivity:
haftmann@22317
    98
haftmann@22317
    99
  \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where} \\
haftmann@22317
   100
  \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
haftmann@22317
   101
  \hspace*{2ex}\isa{satisfying} \\
haftmann@22317
   102
  \hspace*{4ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
haftmann@22317
   103
  \hspace*{4ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
haftmann@22317
   104
  \hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
haftmann@22317
   105
haftmann@22550
   106
  \medskip\noindent From a theoretic point of view, type classes are leightweight
haftmann@22479
   107
  modules; Haskell type classes may be emulated by
haftmann@22317
   108
  SML functors \cite{classes_modules}. 
haftmann@22317
   109
  Isabelle/Isar offers a discipline of type classes which brings
haftmann@22317
   110
  all those aspects together:
haftmann@22317
   111
haftmann@22317
   112
  \begin{enumerate}
haftmann@22317
   113
    \item specifying abstract operations togehter with
haftmann@22317
   114
       corresponding specifications,
haftmann@22317
   115
    \item instantating those abstract operations by a particular
haftmann@22317
   116
       type
haftmann@22317
   117
    \item in connection with a ``less ad-hoc'' approach to overloading,
haftmann@23956
   118
    \item with a direct link to the Isabelle module system
haftmann@23956
   119
      (aka locales \cite{kammueller-locales}).
haftmann@22317
   120
  \end{enumerate}
haftmann@22317
   121
haftmann@22550
   122
  \noindent Isar type classes also directly support code generation
haftmann@22550
   123
  in a Haskell like fashion.
haftmann@22317
   124
haftmann@22317
   125
  This tutorial demonstrates common elements of structured specifications
haftmann@22317
   126
  and abstract reasoning with type classes by the algebraic hierarchy of
haftmann@22317
   127
  semigroups, monoids and groups.  Our background theory is that of
haftmann@23956
   128
  Isabelle/HOL \cite{isa-tutorial}, for which some
haftmann@22317
   129
  familiarity is assumed.
haftmann@22317
   130
haftmann@22317
   131
  Here we merely present the look-and-feel for end users.
haftmann@22317
   132
  Internally, those are mapped to more primitive Isabelle concepts.
haftmann@23956
   133
  See \cite{Haftmann-Wenzel:2006:classes} for more detail.%
haftmann@20967
   134
\end{isamarkuptext}%
haftmann@20967
   135
\isamarkuptrue%
haftmann@20967
   136
%
haftmann@20967
   137
\isamarkupsection{A simple algebra example \label{sec:example}%
haftmann@20967
   138
}
haftmann@20967
   139
\isamarkuptrue%
haftmann@20967
   140
%
haftmann@20967
   141
\isamarkupsubsection{Class definition%
haftmann@20967
   142
}
haftmann@20967
   143
\isamarkuptrue%
haftmann@20967
   144
%
haftmann@20967
   145
\begin{isamarkuptext}%
haftmann@20967
   146
Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operation \isa{{\isasymcirc}} that is
haftmann@20967
   147
  assumed to be associative:%
haftmann@20967
   148
\end{isamarkuptext}%
haftmann@20967
   149
\isamarkuptrue%
haftmann@20967
   150
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@22479
   151
\ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
haftmann@20967
   152
\ \ \ \ \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}\isactrlloc {\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
haftmann@20967
   153
\ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}y\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
haftmann@20967
   154
\begin{isamarkuptext}%
haftmann@20967
   155
\noindent This \isa{{\isasymCLASS}} specification consists of two
haftmann@20967
   156
  parts: the \qn{operational} part names the class operation (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them
haftmann@20967
   157
  (\isa{{\isasymASSUMES}}).  The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global
haftmann@22479
   158
  operation \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
haftmann@22479
   159
  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
   160
\end{isamarkuptext}%
haftmann@20967
   161
\isamarkuptrue%
haftmann@20967
   162
%
haftmann@20967
   163
\isamarkupsubsection{Class instantiation \label{sec:class_inst}%
haftmann@20967
   164
}
haftmann@20967
   165
\isamarkuptrue%
haftmann@20967
   166
%
haftmann@20967
   167
\begin{isamarkuptext}%
haftmann@20967
   168
The concrete type \isa{int} is made a \isa{semigroup}
haftmann@20967
   169
  instance by providing a suitable definition for the class operation
haftmann@20967
   170
  \isa{mult} and a proof for the specification of \isa{assoc}.%
haftmann@20967
   171
\end{isamarkuptext}%
haftmann@20967
   172
\isamarkuptrue%
haftmann@20967
   173
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   174
\ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
haftmann@22479
   175
\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isasymColon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
haftmann@20967
   176
%
haftmann@20967
   177
\isadelimproof
haftmann@20967
   178
\ \ \ \ %
haftmann@20967
   179
\endisadelimproof
haftmann@20967
   180
%
haftmann@20967
   181
\isatagproof
haftmann@20967
   182
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   183
\isanewline
haftmann@22317
   184
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   185
\ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   186
\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   187
\ simp\isanewline
haftmann@22317
   188
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   189
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   190
\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\ \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@20967
   230
\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@22317
   231
\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   232
\ simp\isanewline
haftmann@20967
   233
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   234
%
haftmann@20967
   235
\endisatagproof
haftmann@20967
   236
{\isafoldproof}%
haftmann@20967
   237
%
haftmann@20967
   238
\isadelimproof
haftmann@20967
   239
%
haftmann@20967
   240
\endisadelimproof
haftmann@20967
   241
%
haftmann@20967
   242
\begin{isamarkuptext}%
haftmann@22550
   243
\noindent Also \isa{list}s form a semigroup with \isa{op\ {\isacharat}} as
haftmann@20967
   244
  operation:%
haftmann@20967
   245
\end{isamarkuptext}%
haftmann@20967
   246
\isamarkuptrue%
haftmann@20967
   247
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   248
\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup\isanewline
haftmann@22317
   249
\ \ \ \ \ \ mult{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline
haftmann@20967
   250
%
haftmann@20967
   251
\isadelimproof
haftmann@20967
   252
\ \ \ \ %
haftmann@20967
   253
\endisadelimproof
haftmann@20967
   254
%
haftmann@20967
   255
\isatagproof
haftmann@20967
   256
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   257
\isanewline
haftmann@20967
   258
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   259
\ xs\ ys\ zs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
haftmann@20967
   260
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   261
\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymotimes}\ zs\ {\isacharequal}\ xs\ {\isasymotimes}\ {\isacharparenleft}ys\ {\isasymotimes}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@20967
   262
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
haftmann@20967
   263
\ {\isacharminus}\isanewline
haftmann@20967
   264
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
haftmann@22317
   265
\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   266
\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   267
\isanewline
haftmann@20967
   268
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
haftmann@20967
   269
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   270
\ simp\isanewline
haftmann@20967
   271
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   272
\isanewline
haftmann@20967
   273
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   274
%
haftmann@20967
   275
\endisatagproof
haftmann@20967
   276
{\isafoldproof}%
haftmann@20967
   277
%
haftmann@20967
   278
\isadelimproof
haftmann@20967
   279
%
haftmann@20967
   280
\endisadelimproof
haftmann@20967
   281
%
haftmann@20967
   282
\isamarkupsubsection{Subclasses%
haftmann@20967
   283
}
haftmann@20967
   284
\isamarkuptrue%
haftmann@20967
   285
%
haftmann@20967
   286
\begin{isamarkuptext}%
haftmann@22317
   287
We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral)
haftmann@20967
   288
  by extending \isa{semigroup}
haftmann@20967
   289
  with one additional operation \isa{neutral} together
haftmann@20967
   290
  with its property:%
haftmann@20967
   291
\end{isamarkuptext}%
haftmann@20967
   292
\isamarkuptrue%
haftmann@20967
   293
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@20967
   294
\ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
haftmann@20967
   295
\ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}\isactrlloc {\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
haftmann@20967
   296
\ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}\isactrlloc {\isasymone}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
haftmann@20967
   297
\begin{isamarkuptext}%
haftmann@20967
   298
\noindent Again, we make some instances, by
haftmann@20967
   299
  providing suitable operation definitions and proofs for the
haftmann@20967
   300
  additional specifications.%
haftmann@20967
   301
\end{isamarkuptext}%
haftmann@20967
   302
\isamarkuptrue%
haftmann@20967
   303
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   304
\ nat\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
haftmann@22317
   305
\ \ \ \ \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
haftmann@20967
   306
%
haftmann@20967
   307
\isadelimproof
haftmann@20967
   308
\ \ \ \ %
haftmann@20967
   309
\endisadelimproof
haftmann@20967
   310
%
haftmann@20967
   311
\isatagproof
haftmann@20967
   312
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   313
\isanewline
haftmann@20967
   314
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   315
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
haftmann@20967
   316
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   317
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   318
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   319
\ simp\isanewline
haftmann@20967
   320
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   321
%
haftmann@20967
   322
\endisatagproof
haftmann@20967
   323
{\isafoldproof}%
haftmann@20967
   324
%
haftmann@20967
   325
\isadelimproof
haftmann@20967
   326
\isanewline
haftmann@20967
   327
%
haftmann@20967
   328
\endisadelimproof
haftmann@20967
   329
\isanewline
haftmann@20967
   330
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   331
\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
haftmann@22317
   332
\ \ \ \ \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
haftmann@20967
   333
%
haftmann@20967
   334
\isadelimproof
haftmann@20967
   335
\ \ \ \ %
haftmann@20967
   336
\endisadelimproof
haftmann@20967
   337
%
haftmann@20967
   338
\isatagproof
haftmann@20967
   339
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   340
\isanewline
haftmann@20967
   341
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   342
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
haftmann@20967
   343
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   344
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   345
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   346
\ simp\isanewline
haftmann@20967
   347
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   348
%
haftmann@20967
   349
\endisatagproof
haftmann@20967
   350
{\isafoldproof}%
haftmann@20967
   351
%
haftmann@20967
   352
\isadelimproof
haftmann@20967
   353
\isanewline
haftmann@20967
   354
%
haftmann@20967
   355
\endisadelimproof
haftmann@20967
   356
\isanewline
haftmann@20967
   357
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   358
\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoidl\isanewline
haftmann@22317
   359
\ \ \ \ \ \ neutral{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
haftmann@20967
   360
%
haftmann@20967
   361
\isadelimproof
haftmann@20967
   362
\ \ \ \ %
haftmann@20967
   363
\endisadelimproof
haftmann@20967
   364
%
haftmann@20967
   365
\isatagproof
haftmann@20967
   366
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   367
\isanewline
haftmann@20967
   368
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   369
\ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
haftmann@20967
   370
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   371
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ xs\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
haftmann@20967
   372
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
haftmann@20967
   373
\ {\isacharminus}\isanewline
haftmann@20967
   374
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
haftmann@20967
   375
\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
haftmann@22479
   376
\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   377
\isanewline
haftmann@20967
   378
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
haftmann@20967
   379
\ \isacommand{from}\isamarkupfalse%
haftmann@20967
   380
\ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   381
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   382
\ simp\isanewline
haftmann@20967
   383
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
haftmann@20967
   384
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   385
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   386
\ simp\isanewline
haftmann@20967
   387
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   388
\isanewline
haftmann@20967
   389
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   390
%
haftmann@20967
   391
\endisatagproof
haftmann@20967
   392
{\isafoldproof}%
haftmann@20967
   393
%
haftmann@20967
   394
\isadelimproof
haftmann@20967
   395
%
haftmann@20967
   396
\endisadelimproof
haftmann@20967
   397
%
haftmann@20967
   398
\begin{isamarkuptext}%
haftmann@22317
   399
\noindent Fully-fledged monoids are modelled by another subclass
haftmann@22317
   400
  which does not add new operations but tightens the specification:%
haftmann@20967
   401
\end{isamarkuptext}%
haftmann@20967
   402
\isamarkuptrue%
haftmann@20967
   403
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@20967
   404
\ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
haftmann@22317
   405
\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}%
haftmann@22317
   406
\begin{isamarkuptext}%
haftmann@22317
   407
\noindent Instantiations may also be given simultaneously for different
haftmann@22317
   408
  type constructors:%
haftmann@22317
   409
\end{isamarkuptext}%
haftmann@22317
   410
\isamarkuptrue%
haftmann@20967
   411
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@22317
   412
\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoid\isanewline
haftmann@20967
   413
%
haftmann@20967
   414
\isadelimproof
haftmann@20967
   415
\ \ \ \ %
haftmann@20967
   416
\endisadelimproof
haftmann@20967
   417
%
haftmann@20967
   418
\isatagproof
haftmann@20967
   419
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   420
\isanewline
haftmann@20967
   421
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   422
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
haftmann@20967
   423
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   424
\ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   425
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   426
\ simp\isanewline
haftmann@22317
   427
\ \ \ \ \isacommand{next}\isamarkupfalse%
haftmann@20967
   428
\isanewline
haftmann@20967
   429
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   430
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
haftmann@20967
   431
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   432
\ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   433
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   434
\ simp\isanewline
haftmann@22317
   435
\ \ \ \ \isacommand{next}\isamarkupfalse%
haftmann@20967
   436
\isanewline
haftmann@20967
   437
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   438
\ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
haftmann@20967
   439
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   440
\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
haftmann@20967
   441
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
haftmann@20967
   442
\ {\isacharminus}\isanewline
haftmann@20967
   443
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
haftmann@20967
   444
\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   445
\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   446
\isanewline
haftmann@20967
   447
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
haftmann@20967
   448
\ \isacommand{from}\isamarkupfalse%
haftmann@20967
   449
\ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
haftmann@22479
   450
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   451
\ simp\isanewline
haftmann@20967
   452
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
haftmann@20967
   453
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   454
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   455
\ simp\isanewline
haftmann@20967
   456
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   457
\isanewline
haftmann@20967
   458
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   459
%
haftmann@20967
   460
\endisatagproof
haftmann@20967
   461
{\isafoldproof}%
haftmann@20967
   462
%
haftmann@20967
   463
\isadelimproof
haftmann@20967
   464
%
haftmann@20967
   465
\endisadelimproof
haftmann@22317
   466
%
haftmann@22317
   467
\begin{isamarkuptext}%
haftmann@22317
   468
\noindent To finish our small algebra example, we add a \isa{group} class
haftmann@22317
   469
  with a corresponding instance:%
haftmann@22317
   470
\end{isamarkuptext}%
haftmann@22317
   471
\isamarkuptrue%
haftmann@20967
   472
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@20967
   473
\ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
haftmann@20967
   474
\ \ \ \ \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}\isactrlloc {\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
haftmann@20967
   475
\ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\isanewline
haftmann@20967
   476
\isanewline
haftmann@20967
   477
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   478
\ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
haftmann@22317
   479
\ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymequiv}\ {\isacharminus}\ i{\isachardoublequoteclose}\isanewline
haftmann@20967
   480
%
haftmann@20967
   481
\isadelimproof
haftmann@20967
   482
\ \ \ \ %
haftmann@20967
   483
\endisadelimproof
haftmann@20967
   484
%
haftmann@20967
   485
\isatagproof
haftmann@20967
   486
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   487
\isanewline
haftmann@20967
   488
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   489
\ i\ {\isacharcolon}{\isacharcolon}\ int\isanewline
haftmann@20967
   490
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
haftmann@20967
   491
\ {\isachardoublequoteopen}{\isacharminus}i\ {\isacharplus}\ i\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   492
\ simp\isanewline
haftmann@20967
   493
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   494
\ \isacommand{show}\isamarkupfalse%
haftmann@22550
   495
\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
haftmann@22550
   496
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   497
\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ neutral{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   498
\isanewline
haftmann@20967
   499
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   500
%
haftmann@20967
   501
\endisatagproof
haftmann@20967
   502
{\isafoldproof}%
haftmann@20967
   503
%
haftmann@20967
   504
\isadelimproof
haftmann@20967
   505
%
haftmann@20967
   506
\endisadelimproof
haftmann@20967
   507
%
haftmann@22317
   508
\isamarkupsection{Type classes as locales%
haftmann@22317
   509
}
haftmann@22317
   510
\isamarkuptrue%
haftmann@22317
   511
%
haftmann@22317
   512
\isamarkupsubsection{A look behind the scene%
haftmann@22317
   513
}
haftmann@22317
   514
\isamarkuptrue%
haftmann@22317
   515
%
haftmann@22317
   516
\begin{isamarkuptext}%
haftmann@22479
   517
The example above gives an impression how Isar type classes work
haftmann@22479
   518
  in practice.  As stated in the introduction, classes also provide
haftmann@22479
   519
  a link to Isar's locale system.  Indeed, the logical core of a class
haftmann@22479
   520
  is nothing else than a locale:%
haftmann@22479
   521
\end{isamarkuptext}%
haftmann@22479
   522
\isamarkuptrue%
haftmann@22479
   523
\isacommand{class}\isamarkupfalse%
haftmann@22479
   524
\ idem\ {\isacharequal}\ type\ {\isacharplus}\isanewline
haftmann@22479
   525
\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
haftmann@22479
   526
\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
haftmann@22479
   527
\begin{isamarkuptext}%
haftmann@22479
   528
\noindent essentially introduces the locale%
haftmann@22479
   529
\end{isamarkuptext}%
haftmann@22479
   530
\isamarkuptrue%
haftmann@22317
   531
%
haftmann@22479
   532
\isadelimML
haftmann@22479
   533
%
haftmann@22479
   534
\endisadelimML
haftmann@22479
   535
%
haftmann@22479
   536
\isatagML
haftmann@22479
   537
%
haftmann@22479
   538
\endisatagML
haftmann@22479
   539
{\isafoldML}%
haftmann@22479
   540
%
haftmann@22479
   541
\isadelimML
haftmann@22479
   542
%
haftmann@22479
   543
\endisadelimML
haftmann@22479
   544
\isacommand{locale}\isamarkupfalse%
haftmann@22479
   545
\ idem\ {\isacharequal}\isanewline
haftmann@22479
   546
\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
haftmann@22479
   547
\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
haftmann@22479
   548
\begin{isamarkuptext}%
haftmann@22550
   549
\noindent together with corresponding constant(s):%
haftmann@22479
   550
\end{isamarkuptext}%
haftmann@22479
   551
\isamarkuptrue%
haftmann@22479
   552
\isacommand{consts}\isamarkupfalse%
haftmann@22550
   553
\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
haftmann@22550
   554
\begin{isamarkuptext}%
haftmann@22550
   555
\noindent The connection to the type system is done by means
haftmann@22550
   556
  of a primitive axclass%
haftmann@22550
   557
\end{isamarkuptext}%
haftmann@22550
   558
\isamarkuptrue%
haftmann@22479
   559
\isacommand{axclass}\isamarkupfalse%
haftmann@22479
   560
\ idem\ {\isacharless}\ type\isanewline
haftmann@22479
   561
\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
haftmann@22479
   562
\begin{isamarkuptext}%
wenzelm@22649
   563
\noindent together with a corresponding interpretation:%
haftmann@22479
   564
\end{isamarkuptext}%
haftmann@22479
   565
\isamarkuptrue%
haftmann@22479
   566
\isacommand{interpretation}\isamarkupfalse%
haftmann@22479
   567
\ idem{\isacharunderscore}class{\isacharcolon}\isanewline
haftmann@22479
   568
\ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isacharprime}a{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
haftmann@22479
   569
%
haftmann@22479
   570
\isadelimproof
haftmann@22479
   571
%
haftmann@22479
   572
\endisadelimproof
haftmann@22479
   573
%
haftmann@22479
   574
\isatagproof
haftmann@22479
   575
\isacommand{by}\isamarkupfalse%
haftmann@22550
   576
\ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ idem{\isacharparenright}%
haftmann@22479
   577
\endisatagproof
haftmann@22479
   578
{\isafoldproof}%
haftmann@22479
   579
%
haftmann@22479
   580
\isadelimproof
haftmann@22479
   581
%
haftmann@22479
   582
\endisadelimproof
haftmann@22479
   583
%
haftmann@22479
   584
\isadelimML
haftmann@22479
   585
%
haftmann@22479
   586
\endisadelimML
haftmann@22479
   587
%
haftmann@22479
   588
\isatagML
haftmann@22479
   589
%
haftmann@22479
   590
\endisatagML
haftmann@22479
   591
{\isafoldML}%
haftmann@22479
   592
%
haftmann@22479
   593
\isadelimML
haftmann@22479
   594
%
haftmann@22479
   595
\endisadelimML
haftmann@22479
   596
%
haftmann@22479
   597
\begin{isamarkuptext}%
haftmann@22479
   598
This give you at hand the full power of the Isabelle module system;
haftmann@22479
   599
  conclusions in locale \isa{idem} are implicitly propagated
haftmann@22479
   600
  to class \isa{idem}.%
haftmann@22317
   601
\end{isamarkuptext}%
haftmann@22317
   602
\isamarkuptrue%
haftmann@22317
   603
%
haftmann@20967
   604
\isamarkupsubsection{Abstract reasoning%
haftmann@20967
   605
}
haftmann@20967
   606
\isamarkuptrue%
haftmann@20967
   607
%
haftmann@20967
   608
\begin{isamarkuptext}%
haftmann@22479
   609
Isabelle locales enable reasoning at a general level, while results
haftmann@20967
   610
  are implicitly transferred to all instances.  For example, we can
haftmann@20967
   611
  now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which
haftmann@20967
   612
  states that the function \isa{{\isacharparenleft}x\ {\isasymcirc}{\isacharparenright}} is injective:%
haftmann@20967
   613
\end{isamarkuptext}%
haftmann@20967
   614
\isamarkuptrue%
haftmann@20967
   615
\ \ \ \ \isacommand{lemma}\isamarkupfalse%
haftmann@20967
   616
\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
haftmann@20967
   617
%
haftmann@20967
   618
\isadelimproof
haftmann@20967
   619
\ \ \ \ %
haftmann@20967
   620
\endisadelimproof
haftmann@20967
   621
%
haftmann@20967
   622
\isatagproof
haftmann@20967
   623
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   624
\isanewline
haftmann@20967
   625
\ \ \ \ \isacommand{assume}\isamarkupfalse%
haftmann@20967
   626
\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
haftmann@22479
   627
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   628
\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   629
\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   630
\ simp\isanewline
haftmann@22479
   631
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   632
\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   633
\ {\isachardoublequoteopen}{\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
haftmann@20967
   634
\ assoc\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   635
\ simp\isanewline
haftmann@22479
   636
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   637
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   638
\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
haftmann@20967
   639
\ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   640
\ simp\isanewline
haftmann@20967
   641
\ \ \ \ \isacommand{next}\isamarkupfalse%
haftmann@20967
   642
\isanewline
haftmann@20967
   643
\ \ \ \ \isacommand{assume}\isamarkupfalse%
haftmann@20967
   644
\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
haftmann@22479
   645
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   646
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   647
\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   648
\ simp\isanewline
haftmann@20967
   649
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   650
%
haftmann@20967
   651
\endisatagproof
haftmann@20967
   652
{\isafoldproof}%
haftmann@20967
   653
%
haftmann@20967
   654
\isadelimproof
haftmann@20967
   655
%
haftmann@20967
   656
\endisadelimproof
haftmann@20967
   657
%
haftmann@20967
   658
\begin{isamarkuptext}%
haftmann@20967
   659
\noindent Here the \qt{\isa{{\isasymIN}\ group}} target specification
haftmann@20967
   660
  indicates that the result is recorded within that context for later
haftmann@22479
   661
  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
   662
  \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
   663
\end{isamarkuptext}%
haftmann@20967
   664
\isamarkuptrue%
haftmann@20967
   665
%
haftmann@23956
   666
\isamarkupsubsection{Derived definitions%
haftmann@23956
   667
}
haftmann@23956
   668
\isamarkuptrue%
haftmann@23956
   669
%
haftmann@23956
   670
\begin{isamarkuptext}%
haftmann@23956
   671
Isabelle locales support a concept of local definitions
haftmann@23956
   672
  in locales:%
haftmann@23956
   673
\end{isamarkuptext}%
haftmann@23956
   674
\isamarkuptrue%
haftmann@23956
   675
\ \ \ \ \isacommand{fun}\isamarkupfalse%
haftmann@23956
   676
\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\isanewline
haftmann@23956
   677
\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@23956
   678
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\isanewline
haftmann@23956
   679
\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}%
haftmann@23956
   680
\begin{isamarkuptext}%
haftmann@23956
   681
\noindent If the locale \isa{group} is also a class, this local
haftmann@23956
   682
  definition is propagated onto a global definition of
haftmann@23956
   683
  \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}}
haftmann@23956
   684
  with corresponding theorems
haftmann@23956
   685
haftmann@23956
   686
  \isa{pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}\isasep\isanewline%
haftmann@23956
   687
pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x}.
haftmann@23956
   688
haftmann@23956
   689
  \noindent As you can see from this example, for local
haftmann@23956
   690
  definitions you may use any specification tool
haftmann@23956
   691
  which works together with locales (e.g. \cite{krauss2006}).%
haftmann@23956
   692
\end{isamarkuptext}%
haftmann@23956
   693
\isamarkuptrue%
haftmann@23956
   694
%
haftmann@22317
   695
\isamarkupsection{Further issues%
haftmann@20967
   696
}
haftmann@20967
   697
\isamarkuptrue%
haftmann@20967
   698
%
haftmann@22317
   699
\isamarkupsubsection{Code generation%
haftmann@20967
   700
}
haftmann@20967
   701
\isamarkuptrue%
haftmann@20967
   702
%
haftmann@20967
   703
\begin{isamarkuptext}%
haftmann@22317
   704
Turning back to the first motivation for type classes,
haftmann@22317
   705
  namely overloading, it is obvious that overloading
haftmann@22317
   706
  stemming from \isa{{\isasymCLASS}} and \isa{{\isasymINSTANCE}}
haftmann@22317
   707
  statements naturally maps to Haskell type classes.
haftmann@22317
   708
  The code generator framework \cite{isabelle-codegen} 
haftmann@22317
   709
  takes this into account.  Concerning target languages
haftmann@22317
   710
  lacking type classes (e.g.~SML), type classes
haftmann@22317
   711
  are implemented by explicit dictionary construction.
haftmann@23956
   712
  For example, lets go back to the power function:%
haftmann@20967
   713
\end{isamarkuptext}%
haftmann@20967
   714
\isamarkuptrue%
haftmann@22317
   715
\ \ \ \ \isacommand{fun}\isamarkupfalse%
haftmann@20967
   716
\isanewline
haftmann@23956
   717
\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@20967
   718
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
haftmann@22479
   719
\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline
haftmann@20967
   720
\isanewline
haftmann@20967
   721
\ \ \ \ \isacommand{definition}\isamarkupfalse%
haftmann@20967
   722
\isanewline
haftmann@22479
   723
\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@20967
   724
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
haftmann@20967
   725
\ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
haftmann@20967
   726
\ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@20967
   727
\isanewline
haftmann@20967
   728
\ \ \ \ \isacommand{definition}\isamarkupfalse%
haftmann@20967
   729
\isanewline
haftmann@22317
   730
\ \ \ \ \ \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
haftmann@20967
   731
\ \ \ \ \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
haftmann@20967
   732
\begin{isamarkuptext}%
haftmann@22317
   733
\noindent This maps to Haskell as:%
haftmann@20967
   734
\end{isamarkuptext}%
haftmann@20967
   735
\isamarkuptrue%
haftmann@22317
   736
\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
haftmann@23956
   737
\ example\ \isakeyword{in}\ Haskell\ \isakeyword{to}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}%
haftmann@20967
   738
\begin{isamarkuptext}%
haftmann@22317
   739
\lsthaskell{Thy/code_examples/Classes.hs}
haftmann@22317
   740
haftmann@22317
   741
  \noindent The whole code in SML with explicit dictionary passing:%
haftmann@22317
   742
\end{isamarkuptext}%
haftmann@22317
   743
\isamarkuptrue%
haftmann@22317
   744
\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
haftmann@23956
   745
\ example\ \isakeyword{in}\ SML\ \isakeyword{to}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}%
haftmann@22317
   746
\begin{isamarkuptext}%
haftmann@22317
   747
\lstsml{Thy/code_examples/classes.ML}%
haftmann@20967
   748
\end{isamarkuptext}%
haftmann@20967
   749
\isamarkuptrue%
haftmann@20967
   750
%
haftmann@20967
   751
\isadelimtheory
haftmann@20967
   752
%
haftmann@20967
   753
\endisadelimtheory
haftmann@20967
   754
%
haftmann@20967
   755
\isatagtheory
haftmann@20967
   756
\isacommand{end}\isamarkupfalse%
haftmann@20967
   757
%
haftmann@20967
   758
\endisatagtheory
haftmann@20967
   759
{\isafoldtheory}%
haftmann@20967
   760
%
haftmann@20967
   761
\isadelimtheory
haftmann@20967
   762
%
haftmann@20967
   763
\endisadelimtheory
haftmann@20967
   764
\isanewline
haftmann@20967
   765
\end{isabellebody}%
haftmann@20967
   766
%%% Local Variables:
haftmann@20967
   767
%%% mode: latex
haftmann@20967
   768
%%% TeX-master: "root"
haftmann@20967
   769
%%% End: