doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
author haftmann
Tue Mar 20 10:23:31 2007 +0100 (2007-03-20)
changeset 22479 de15ea8fb348
parent 22317 b550d2c6ca90
child 22550 c5039bee2602
permissions -rw-r--r--
updated code generation sections
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@22317
    62
  types for \isa{{\isasymalpha}}, which is achieves 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@22317
    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}}\ {\isacharampersand}{\isacharampersand}\ 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@22317
    82
  \medskip 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@22317
    88
  algebra \cite{Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}.
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@22317
    95
  above could be given the following specification:
haftmann@22317
    96
haftmann@22317
    97
  \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where} \\
haftmann@22317
    98
  \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
haftmann@22317
    99
  \hspace*{2ex}\isa{satisfying} \\
haftmann@22317
   100
  \hspace*{4ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
haftmann@22317
   101
  \hspace*{4ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
haftmann@22317
   102
  \hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
haftmann@22317
   103
haftmann@22317
   104
  \medskip From a theoretic point of view, type classes are leightweight
haftmann@22479
   105
  modules; Haskell type classes may be emulated by
haftmann@22317
   106
  SML functors \cite{classes_modules}. 
haftmann@22317
   107
  Isabelle/Isar offers a discipline of type classes which brings
haftmann@22317
   108
  all those aspects together:
haftmann@22317
   109
haftmann@22317
   110
  \begin{enumerate}
haftmann@22317
   111
    \item specifying abstract operations togehter with
haftmann@22317
   112
       corresponding specifications,
haftmann@22317
   113
    \item instantating those abstract operations by a particular
haftmann@22317
   114
       type
haftmann@22317
   115
    \item in connection with a ``less ad-hoc'' approach to overloading,
haftmann@22317
   116
    \item with a direct link to the Isabelle module system (aka locales).
haftmann@22317
   117
  \end{enumerate}
haftmann@22317
   118
haftmann@22317
   119
  Isar type classes also directly support code generation
haftmann@22317
   120
  in as Haskell like fashion.
haftmann@22317
   121
haftmann@22317
   122
  This tutorial demonstrates common elements of structured specifications
haftmann@22317
   123
  and abstract reasoning with type classes by the algebraic hierarchy of
haftmann@22317
   124
  semigroups, monoids and groups.  Our background theory is that of
haftmann@22317
   125
  Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, for which some
haftmann@22317
   126
  familiarity is assumed.
haftmann@22317
   127
haftmann@22317
   128
  Here we merely present the look-and-feel for end users.
haftmann@22317
   129
  Internally, those are mapped to more primitive Isabelle concepts.
haftmann@22317
   130
  See \cite{haftmann_wenzel2006classes} for more detail.%
haftmann@20967
   131
\end{isamarkuptext}%
haftmann@20967
   132
\isamarkuptrue%
haftmann@20967
   133
%
haftmann@20967
   134
\isamarkupsection{A simple algebra example \label{sec:example}%
haftmann@20967
   135
}
haftmann@20967
   136
\isamarkuptrue%
haftmann@20967
   137
%
haftmann@20967
   138
\isamarkupsubsection{Class definition%
haftmann@20967
   139
}
haftmann@20967
   140
\isamarkuptrue%
haftmann@20967
   141
%
haftmann@20967
   142
\begin{isamarkuptext}%
haftmann@20967
   143
Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operation \isa{{\isasymcirc}} that is
haftmann@20967
   144
  assumed to be associative:%
haftmann@20967
   145
\end{isamarkuptext}%
haftmann@20967
   146
\isamarkuptrue%
haftmann@20967
   147
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@22479
   148
\ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
haftmann@20967
   149
\ \ \ \ \ \ \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
   150
\ \ \ \ \ \ \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
   151
\begin{isamarkuptext}%
haftmann@20967
   152
\noindent This \isa{{\isasymCLASS}} specification consists of two
haftmann@20967
   153
  parts: the \qn{operational} part names the class operation (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them
haftmann@20967
   154
  (\isa{{\isasymASSUMES}}).  The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global
haftmann@22479
   155
  operation \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
haftmann@22479
   156
  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
   157
\end{isamarkuptext}%
haftmann@20967
   158
\isamarkuptrue%
haftmann@20967
   159
%
haftmann@20967
   160
\isamarkupsubsection{Class instantiation \label{sec:class_inst}%
haftmann@20967
   161
}
haftmann@20967
   162
\isamarkuptrue%
haftmann@20967
   163
%
haftmann@20967
   164
\begin{isamarkuptext}%
haftmann@20967
   165
The concrete type \isa{int} is made a \isa{semigroup}
haftmann@20967
   166
  instance by providing a suitable definition for the class operation
haftmann@20967
   167
  \isa{mult} and a proof for the specification of \isa{assoc}.%
haftmann@20967
   168
\end{isamarkuptext}%
haftmann@20967
   169
\isamarkuptrue%
haftmann@20967
   170
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   171
\ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
haftmann@22479
   172
\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isasymColon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
haftmann@20967
   173
%
haftmann@20967
   174
\isadelimproof
haftmann@20967
   175
\ \ \ \ %
haftmann@20967
   176
\endisadelimproof
haftmann@20967
   177
%
haftmann@20967
   178
\isatagproof
haftmann@20967
   179
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   180
\isanewline
haftmann@22317
   181
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   182
\ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   183
\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   184
\ simp\isanewline
haftmann@22317
   185
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   186
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   187
\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   188
\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   189
\isanewline
haftmann@20967
   190
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   191
%
haftmann@20967
   192
\endisatagproof
haftmann@20967
   193
{\isafoldproof}%
haftmann@20967
   194
%
haftmann@20967
   195
\isadelimproof
haftmann@20967
   196
%
haftmann@20967
   197
\endisadelimproof
haftmann@20967
   198
%
haftmann@20967
   199
\begin{isamarkuptext}%
haftmann@20967
   200
\noindent From now on, the type-checker will consider \isa{int}
haftmann@20967
   201
  as a \isa{semigroup} automatically, i.e.\ any general results
haftmann@20967
   202
  are immediately available on concrete instances.
haftmann@20967
   203
haftmann@22317
   204
  Note that the first proof step is the \isa{default} method,
haftmann@22317
   205
  which for instantiation proofs maps to the \isa{intro{\isacharunderscore}classes} method.
haftmann@22317
   206
  This boils down an instantiation judgement to the relevant primitive
haftmann@22317
   207
  proof goals and should conveniently always be the first method applied
haftmann@22317
   208
  in an instantiation proof.
haftmann@22317
   209
haftmann@20967
   210
  Another instance of \isa{semigroup} are the natural numbers:%
haftmann@20967
   211
\end{isamarkuptext}%
haftmann@20967
   212
\isamarkuptrue%
haftmann@20967
   213
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   214
\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
haftmann@22317
   215
\ \ \ \ \ \ mult{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymequiv}\ m\ {\isacharplus}\ n{\isachardoublequoteclose}\isanewline
haftmann@20967
   216
%
haftmann@20967
   217
\isadelimproof
haftmann@20967
   218
\ \ \ \ %
haftmann@20967
   219
\endisadelimproof
haftmann@20967
   220
%
haftmann@20967
   221
\isatagproof
haftmann@20967
   222
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   223
\isanewline
haftmann@20967
   224
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   225
\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
haftmann@20967
   226
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   227
\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@22317
   228
\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   229
\ simp\isanewline
haftmann@20967
   230
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   231
%
haftmann@20967
   232
\endisatagproof
haftmann@20967
   233
{\isafoldproof}%
haftmann@20967
   234
%
haftmann@20967
   235
\isadelimproof
haftmann@20967
   236
%
haftmann@20967
   237
\endisadelimproof
haftmann@20967
   238
%
haftmann@20967
   239
\begin{isamarkuptext}%
haftmann@20967
   240
Also \isa{list}s form a semigroup with \isa{op\ {\isacharat}} as
haftmann@20967
   241
  operation:%
haftmann@20967
   242
\end{isamarkuptext}%
haftmann@20967
   243
\isamarkuptrue%
haftmann@20967
   244
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   245
\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup\isanewline
haftmann@22317
   246
\ \ \ \ \ \ mult{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline
haftmann@20967
   247
%
haftmann@20967
   248
\isadelimproof
haftmann@20967
   249
\ \ \ \ %
haftmann@20967
   250
\endisadelimproof
haftmann@20967
   251
%
haftmann@20967
   252
\isatagproof
haftmann@20967
   253
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   254
\isanewline
haftmann@20967
   255
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   256
\ xs\ ys\ zs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
haftmann@20967
   257
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   258
\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymotimes}\ zs\ {\isacharequal}\ xs\ {\isasymotimes}\ {\isacharparenleft}ys\ {\isasymotimes}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@20967
   259
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
haftmann@20967
   260
\ {\isacharminus}\isanewline
haftmann@20967
   261
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
haftmann@22317
   262
\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   263
\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   264
\isanewline
haftmann@20967
   265
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
haftmann@20967
   266
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   267
\ simp\isanewline
haftmann@20967
   268
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   269
\isanewline
haftmann@20967
   270
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   271
%
haftmann@20967
   272
\endisatagproof
haftmann@20967
   273
{\isafoldproof}%
haftmann@20967
   274
%
haftmann@20967
   275
\isadelimproof
haftmann@20967
   276
%
haftmann@20967
   277
\endisadelimproof
haftmann@20967
   278
%
haftmann@20967
   279
\isamarkupsubsection{Subclasses%
haftmann@20967
   280
}
haftmann@20967
   281
\isamarkuptrue%
haftmann@20967
   282
%
haftmann@20967
   283
\begin{isamarkuptext}%
haftmann@22317
   284
We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral)
haftmann@20967
   285
  by extending \isa{semigroup}
haftmann@20967
   286
  with one additional operation \isa{neutral} together
haftmann@20967
   287
  with its property:%
haftmann@20967
   288
\end{isamarkuptext}%
haftmann@20967
   289
\isamarkuptrue%
haftmann@20967
   290
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@20967
   291
\ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
haftmann@20967
   292
\ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}\isactrlloc {\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
haftmann@20967
   293
\ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}\isactrlloc {\isasymone}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
haftmann@20967
   294
\begin{isamarkuptext}%
haftmann@20967
   295
\noindent Again, we make some instances, by
haftmann@20967
   296
  providing suitable operation definitions and proofs for the
haftmann@20967
   297
  additional specifications.%
haftmann@20967
   298
\end{isamarkuptext}%
haftmann@20967
   299
\isamarkuptrue%
haftmann@20967
   300
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   301
\ nat\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
haftmann@22317
   302
\ \ \ \ \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
haftmann@20967
   303
%
haftmann@20967
   304
\isadelimproof
haftmann@20967
   305
\ \ \ \ %
haftmann@20967
   306
\endisadelimproof
haftmann@20967
   307
%
haftmann@20967
   308
\isatagproof
haftmann@20967
   309
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   310
\isanewline
haftmann@20967
   311
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   312
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
haftmann@20967
   313
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   314
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   315
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   316
\ simp\isanewline
haftmann@20967
   317
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   318
%
haftmann@20967
   319
\endisatagproof
haftmann@20967
   320
{\isafoldproof}%
haftmann@20967
   321
%
haftmann@20967
   322
\isadelimproof
haftmann@20967
   323
\isanewline
haftmann@20967
   324
%
haftmann@20967
   325
\endisadelimproof
haftmann@20967
   326
\isanewline
haftmann@20967
   327
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   328
\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
haftmann@22317
   329
\ \ \ \ \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
haftmann@20967
   330
%
haftmann@20967
   331
\isadelimproof
haftmann@20967
   332
\ \ \ \ %
haftmann@20967
   333
\endisadelimproof
haftmann@20967
   334
%
haftmann@20967
   335
\isatagproof
haftmann@20967
   336
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   337
\isanewline
haftmann@20967
   338
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   339
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
haftmann@20967
   340
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   341
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   342
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   343
\ simp\isanewline
haftmann@20967
   344
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   345
%
haftmann@20967
   346
\endisatagproof
haftmann@20967
   347
{\isafoldproof}%
haftmann@20967
   348
%
haftmann@20967
   349
\isadelimproof
haftmann@20967
   350
\isanewline
haftmann@20967
   351
%
haftmann@20967
   352
\endisadelimproof
haftmann@20967
   353
\isanewline
haftmann@20967
   354
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   355
\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoidl\isanewline
haftmann@22317
   356
\ \ \ \ \ \ neutral{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
haftmann@20967
   357
%
haftmann@20967
   358
\isadelimproof
haftmann@20967
   359
\ \ \ \ %
haftmann@20967
   360
\endisadelimproof
haftmann@20967
   361
%
haftmann@20967
   362
\isatagproof
haftmann@20967
   363
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   364
\isanewline
haftmann@20967
   365
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   366
\ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
haftmann@20967
   367
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   368
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ xs\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
haftmann@20967
   369
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
haftmann@20967
   370
\ {\isacharminus}\isanewline
haftmann@20967
   371
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
haftmann@20967
   372
\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
haftmann@22479
   373
\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   374
\isanewline
haftmann@20967
   375
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
haftmann@20967
   376
\ \isacommand{from}\isamarkupfalse%
haftmann@20967
   377
\ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   378
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   379
\ simp\isanewline
haftmann@20967
   380
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
haftmann@20967
   381
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   382
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   383
\ simp\isanewline
haftmann@20967
   384
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   385
\isanewline
haftmann@20967
   386
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   387
%
haftmann@20967
   388
\endisatagproof
haftmann@20967
   389
{\isafoldproof}%
haftmann@20967
   390
%
haftmann@20967
   391
\isadelimproof
haftmann@20967
   392
%
haftmann@20967
   393
\endisadelimproof
haftmann@20967
   394
%
haftmann@20967
   395
\begin{isamarkuptext}%
haftmann@22317
   396
\noindent Fully-fledged monoids are modelled by another subclass
haftmann@22317
   397
  which does not add new operations but tightens the specification:%
haftmann@20967
   398
\end{isamarkuptext}%
haftmann@20967
   399
\isamarkuptrue%
haftmann@20967
   400
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@20967
   401
\ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
haftmann@22317
   402
\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}%
haftmann@22317
   403
\begin{isamarkuptext}%
haftmann@22317
   404
\noindent Instantiations may also be given simultaneously for different
haftmann@22317
   405
  type constructors:%
haftmann@22317
   406
\end{isamarkuptext}%
haftmann@22317
   407
\isamarkuptrue%
haftmann@20967
   408
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@22317
   409
\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoid\isanewline
haftmann@20967
   410
%
haftmann@20967
   411
\isadelimproof
haftmann@20967
   412
\ \ \ \ %
haftmann@20967
   413
\endisadelimproof
haftmann@20967
   414
%
haftmann@20967
   415
\isatagproof
haftmann@20967
   416
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   417
\isanewline
haftmann@20967
   418
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   419
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
haftmann@20967
   420
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   421
\ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   422
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   423
\ simp\isanewline
haftmann@22317
   424
\ \ \ \ \isacommand{next}\isamarkupfalse%
haftmann@20967
   425
\isanewline
haftmann@20967
   426
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   427
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
haftmann@20967
   428
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   429
\ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   430
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   431
\ simp\isanewline
haftmann@22317
   432
\ \ \ \ \isacommand{next}\isamarkupfalse%
haftmann@20967
   433
\isanewline
haftmann@20967
   434
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   435
\ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
haftmann@20967
   436
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   437
\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
haftmann@20967
   438
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
haftmann@20967
   439
\ {\isacharminus}\isanewline
haftmann@20967
   440
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
haftmann@20967
   441
\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   442
\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   443
\isanewline
haftmann@20967
   444
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
haftmann@20967
   445
\ \isacommand{from}\isamarkupfalse%
haftmann@20967
   446
\ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
haftmann@22479
   447
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   448
\ simp\isanewline
haftmann@20967
   449
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
haftmann@20967
   450
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   451
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   452
\ simp\isanewline
haftmann@20967
   453
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   454
\isanewline
haftmann@20967
   455
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   456
%
haftmann@20967
   457
\endisatagproof
haftmann@20967
   458
{\isafoldproof}%
haftmann@20967
   459
%
haftmann@20967
   460
\isadelimproof
haftmann@20967
   461
%
haftmann@20967
   462
\endisadelimproof
haftmann@22317
   463
%
haftmann@22317
   464
\begin{isamarkuptext}%
haftmann@22317
   465
\noindent To finish our small algebra example, we add a \isa{group} class
haftmann@22317
   466
  with a corresponding instance:%
haftmann@22317
   467
\end{isamarkuptext}%
haftmann@22317
   468
\isamarkuptrue%
haftmann@20967
   469
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@20967
   470
\ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
haftmann@20967
   471
\ \ \ \ \ \ \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
   472
\ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\isanewline
haftmann@20967
   473
\isanewline
haftmann@20967
   474
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   475
\ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
haftmann@22317
   476
\ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymequiv}\ {\isacharminus}\ i{\isachardoublequoteclose}\isanewline
haftmann@20967
   477
%
haftmann@20967
   478
\isadelimproof
haftmann@20967
   479
\ \ \ \ %
haftmann@20967
   480
\endisadelimproof
haftmann@20967
   481
%
haftmann@20967
   482
\isatagproof
haftmann@20967
   483
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   484
\isanewline
haftmann@20967
   485
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   486
\ i\ {\isacharcolon}{\isacharcolon}\ int\isanewline
haftmann@20967
   487
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
haftmann@20967
   488
\ {\isachardoublequoteopen}{\isacharminus}i\ {\isacharplus}\ i\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   489
\ simp\isanewline
haftmann@20967
   490
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   491
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   492
\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   493
\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ neutral{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   494
\isanewline
haftmann@20967
   495
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   496
%
haftmann@20967
   497
\endisatagproof
haftmann@20967
   498
{\isafoldproof}%
haftmann@20967
   499
%
haftmann@20967
   500
\isadelimproof
haftmann@20967
   501
%
haftmann@20967
   502
\endisadelimproof
haftmann@20967
   503
%
haftmann@22317
   504
\isamarkupsection{Type classes as locales%
haftmann@22317
   505
}
haftmann@22317
   506
\isamarkuptrue%
haftmann@22317
   507
%
haftmann@22317
   508
\isamarkupsubsection{A look behind the scene%
haftmann@22317
   509
}
haftmann@22317
   510
\isamarkuptrue%
haftmann@22317
   511
%
haftmann@22317
   512
\begin{isamarkuptext}%
haftmann@22479
   513
The example above gives an impression how Isar type classes work
haftmann@22479
   514
  in practice.  As stated in the introduction, classes also provide
haftmann@22479
   515
  a link to Isar's locale system.  Indeed, the logical core of a class
haftmann@22479
   516
  is nothing else than a locale:%
haftmann@22479
   517
\end{isamarkuptext}%
haftmann@22479
   518
\isamarkuptrue%
haftmann@22479
   519
\isacommand{class}\isamarkupfalse%
haftmann@22479
   520
\ idem\ {\isacharequal}\ type\ {\isacharplus}\isanewline
haftmann@22479
   521
\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
haftmann@22479
   522
\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
haftmann@22479
   523
\begin{isamarkuptext}%
haftmann@22479
   524
\noindent essentially introduces the locale%
haftmann@22479
   525
\end{isamarkuptext}%
haftmann@22479
   526
\isamarkuptrue%
haftmann@22317
   527
%
haftmann@22479
   528
\isadelimML
haftmann@22479
   529
%
haftmann@22479
   530
\endisadelimML
haftmann@22479
   531
%
haftmann@22479
   532
\isatagML
haftmann@22479
   533
%
haftmann@22479
   534
\endisatagML
haftmann@22479
   535
{\isafoldML}%
haftmann@22479
   536
%
haftmann@22479
   537
\isadelimML
haftmann@22479
   538
%
haftmann@22479
   539
\endisadelimML
haftmann@22479
   540
\isanewline
haftmann@22479
   541
\isacommand{locale}\isamarkupfalse%
haftmann@22479
   542
\ idem\ {\isacharequal}\isanewline
haftmann@22479
   543
\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
haftmann@22479
   544
\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
haftmann@22479
   545
\begin{isamarkuptext}%
haftmann@22479
   546
\noindent together with corresponding constant(s) and axclass%
haftmann@22479
   547
\end{isamarkuptext}%
haftmann@22479
   548
\isamarkuptrue%
haftmann@22479
   549
\isacommand{consts}\isamarkupfalse%
haftmann@22479
   550
\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
haftmann@22479
   551
\isanewline
haftmann@22479
   552
\isacommand{axclass}\isamarkupfalse%
haftmann@22479
   553
\ idem\ {\isacharless}\ type\isanewline
haftmann@22479
   554
\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
haftmann@22479
   555
\begin{isamarkuptext}%
haftmann@22479
   556
This axclass is coupled to the locale by means of an interpretation:%
haftmann@22479
   557
\end{isamarkuptext}%
haftmann@22479
   558
\isamarkuptrue%
haftmann@22479
   559
\isacommand{interpretation}\isamarkupfalse%
haftmann@22479
   560
\ idem{\isacharunderscore}class{\isacharcolon}\isanewline
haftmann@22479
   561
\ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isacharprime}a{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
haftmann@22479
   562
%
haftmann@22479
   563
\isadelimproof
haftmann@22479
   564
%
haftmann@22479
   565
\endisadelimproof
haftmann@22479
   566
%
haftmann@22479
   567
\isatagproof
haftmann@22479
   568
\isacommand{by}\isamarkupfalse%
haftmann@22479
   569
\ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ idem{\isacharparenright}\isanewline
haftmann@22479
   570
%
haftmann@22479
   571
\endisatagproof
haftmann@22479
   572
{\isafoldproof}%
haftmann@22479
   573
%
haftmann@22479
   574
\isadelimproof
haftmann@22479
   575
%
haftmann@22479
   576
\endisadelimproof
haftmann@22479
   577
%
haftmann@22479
   578
\isadelimML
haftmann@22479
   579
%
haftmann@22479
   580
\endisadelimML
haftmann@22479
   581
%
haftmann@22479
   582
\isatagML
haftmann@22479
   583
%
haftmann@22479
   584
\endisatagML
haftmann@22479
   585
{\isafoldML}%
haftmann@22479
   586
%
haftmann@22479
   587
\isadelimML
haftmann@22479
   588
%
haftmann@22479
   589
\endisadelimML
haftmann@22479
   590
%
haftmann@22479
   591
\begin{isamarkuptext}%
haftmann@22479
   592
This give you at hand the full power of the Isabelle module system;
haftmann@22479
   593
  conclusions in locale \isa{idem} are implicitly propagated
haftmann@22479
   594
  to class \isa{idem}.%
haftmann@22317
   595
\end{isamarkuptext}%
haftmann@22317
   596
\isamarkuptrue%
haftmann@22317
   597
%
haftmann@20967
   598
\isamarkupsubsection{Abstract reasoning%
haftmann@20967
   599
}
haftmann@20967
   600
\isamarkuptrue%
haftmann@20967
   601
%
haftmann@20967
   602
\begin{isamarkuptext}%
haftmann@22479
   603
Isabelle locales enable reasoning at a general level, while results
haftmann@20967
   604
  are implicitly transferred to all instances.  For example, we can
haftmann@20967
   605
  now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which
haftmann@20967
   606
  states that the function \isa{{\isacharparenleft}x\ {\isasymcirc}{\isacharparenright}} is injective:%
haftmann@20967
   607
\end{isamarkuptext}%
haftmann@20967
   608
\isamarkuptrue%
haftmann@20967
   609
\ \ \ \ \isacommand{lemma}\isamarkupfalse%
haftmann@20967
   610
\ {\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
   611
%
haftmann@20967
   612
\isadelimproof
haftmann@20967
   613
\ \ \ \ %
haftmann@20967
   614
\endisadelimproof
haftmann@20967
   615
%
haftmann@20967
   616
\isatagproof
haftmann@20967
   617
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   618
\isanewline
haftmann@20967
   619
\ \ \ \ \isacommand{assume}\isamarkupfalse%
haftmann@20967
   620
\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
haftmann@22479
   621
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   622
\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   623
\ {\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
   624
\ simp\isanewline
haftmann@22479
   625
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   626
\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   627
\ {\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
   628
\ assoc\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   629
\ simp\isanewline
haftmann@22479
   630
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   631
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   632
\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
haftmann@20967
   633
\ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   634
\ simp\isanewline
haftmann@20967
   635
\ \ \ \ \isacommand{next}\isamarkupfalse%
haftmann@20967
   636
\isanewline
haftmann@20967
   637
\ \ \ \ \isacommand{assume}\isamarkupfalse%
haftmann@20967
   638
\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
haftmann@22479
   639
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   640
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   641
\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   642
\ simp\isanewline
haftmann@20967
   643
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   644
%
haftmann@20967
   645
\endisatagproof
haftmann@20967
   646
{\isafoldproof}%
haftmann@20967
   647
%
haftmann@20967
   648
\isadelimproof
haftmann@20967
   649
%
haftmann@20967
   650
\endisadelimproof
haftmann@20967
   651
%
haftmann@20967
   652
\begin{isamarkuptext}%
haftmann@20967
   653
\noindent Here the \qt{\isa{{\isasymIN}\ group}} target specification
haftmann@20967
   654
  indicates that the result is recorded within that context for later
haftmann@22479
   655
  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
   656
  \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
   657
\end{isamarkuptext}%
haftmann@20967
   658
\isamarkuptrue%
haftmann@20967
   659
%
haftmann@22317
   660
\isamarkupsection{Further issues%
haftmann@20967
   661
}
haftmann@20967
   662
\isamarkuptrue%
haftmann@20967
   663
%
haftmann@22317
   664
\isamarkupsubsection{Code generation%
haftmann@20967
   665
}
haftmann@20967
   666
\isamarkuptrue%
haftmann@20967
   667
%
haftmann@20967
   668
\begin{isamarkuptext}%
haftmann@22317
   669
Turning back to the first motivation for type classes,
haftmann@22317
   670
  namely overloading, it is obvious that overloading
haftmann@22317
   671
  stemming from \isa{{\isasymCLASS}} and \isa{{\isasymINSTANCE}}
haftmann@22317
   672
  statements naturally maps to Haskell type classes.
haftmann@22317
   673
  The code generator framework \cite{isabelle-codegen} 
haftmann@22317
   674
  takes this into account.  Concerning target languages
haftmann@22317
   675
  lacking type classes (e.g.~SML), type classes
haftmann@22317
   676
  are implemented by explicit dictionary construction.
haftmann@22317
   677
  As example, the natural power function on groups:%
haftmann@20967
   678
\end{isamarkuptext}%
haftmann@20967
   679
\isamarkuptrue%
haftmann@22317
   680
\ \ \ \ \isacommand{fun}\isamarkupfalse%
haftmann@20967
   681
\isanewline
haftmann@22479
   682
\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@20967
   683
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
haftmann@22479
   684
\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline
haftmann@20967
   685
\isanewline
haftmann@20967
   686
\ \ \ \ \isacommand{definition}\isamarkupfalse%
haftmann@20967
   687
\isanewline
haftmann@22479
   688
\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@20967
   689
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
haftmann@20967
   690
\ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
haftmann@20967
   691
\ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@20967
   692
\isanewline
haftmann@20967
   693
\ \ \ \ \isacommand{definition}\isamarkupfalse%
haftmann@20967
   694
\isanewline
haftmann@22317
   695
\ \ \ \ \ \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
haftmann@20967
   696
\ \ \ \ \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
haftmann@20967
   697
\begin{isamarkuptext}%
haftmann@22317
   698
\noindent This maps to Haskell as:%
haftmann@20967
   699
\end{isamarkuptext}%
haftmann@20967
   700
\isamarkuptrue%
haftmann@22317
   701
\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
haftmann@22317
   702
\ example\ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}{\isacharparenright}%
haftmann@20967
   703
\begin{isamarkuptext}%
haftmann@22317
   704
\lsthaskell{Thy/code_examples/Classes.hs}
haftmann@22317
   705
haftmann@22317
   706
  \noindent (we have left out all other modules).
haftmann@22317
   707
haftmann@22317
   708
  \noindent The whole code in SML with explicit dictionary passing:%
haftmann@22317
   709
\end{isamarkuptext}%
haftmann@22317
   710
\isamarkuptrue%
haftmann@22317
   711
\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
haftmann@22317
   712
\ example\ {\isacharparenleft}SML\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
haftmann@22317
   713
\begin{isamarkuptext}%
haftmann@22317
   714
\lstsml{Thy/code_examples/classes.ML}%
haftmann@20967
   715
\end{isamarkuptext}%
haftmann@20967
   716
\isamarkuptrue%
haftmann@20967
   717
%
haftmann@20967
   718
\isadelimtheory
haftmann@20967
   719
%
haftmann@20967
   720
\endisadelimtheory
haftmann@20967
   721
%
haftmann@20967
   722
\isatagtheory
haftmann@20967
   723
\isacommand{end}\isamarkupfalse%
haftmann@20967
   724
%
haftmann@20967
   725
\endisatagtheory
haftmann@20967
   726
{\isafoldtheory}%
haftmann@20967
   727
%
haftmann@20967
   728
\isadelimtheory
haftmann@20967
   729
%
haftmann@20967
   730
\endisadelimtheory
haftmann@20967
   731
\isanewline
haftmann@20967
   732
\end{isabellebody}%
haftmann@20967
   733
%%% Local Variables:
haftmann@20967
   734
%%% mode: latex
haftmann@20967
   735
%%% TeX-master: "root"
haftmann@20967
   736
%%% End: