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