doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
author haftmann
Fri Oct 10 15:52:45 2008 +0200 (2008-10-10)
changeset 28565 519b17118926
parent 28540 541366e3c1b3
child 28566 be2a72b421ae
permissions -rw-r--r--
tuned
haftmann@20967
     1
%
haftmann@20967
     2
\begin{isabellebody}%
haftmann@20967
     3
\def\isabellecontext{Classes}%
haftmann@20967
     4
%
haftmann@20967
     5
\isadelimtheory
haftmann@20967
     6
%
haftmann@20967
     7
\endisadelimtheory
haftmann@20967
     8
%
haftmann@20967
     9
\isatagtheory
haftmann@28565
    10
\isacommand{theory}\isamarkupfalse%
haftmann@28565
    11
\ Classes\isanewline
haftmann@28565
    12
\isakeyword{imports}\ Main\ Setup\isanewline
haftmann@28565
    13
\isakeyword{begin}%
haftmann@20967
    14
\endisatagtheory
haftmann@20967
    15
{\isafoldtheory}%
haftmann@20967
    16
%
haftmann@20967
    17
\isadelimtheory
haftmann@20967
    18
%
haftmann@20967
    19
\endisadelimtheory
haftmann@20967
    20
%
haftmann@20967
    21
\isamarkupchapter{Haskell-style classes with Isabelle/Isar%
haftmann@20967
    22
}
haftmann@20967
    23
\isamarkuptrue%
haftmann@20967
    24
%
haftmann@20967
    25
\isamarkupsection{Introduction%
haftmann@20967
    26
}
haftmann@20967
    27
\isamarkuptrue%
haftmann@20967
    28
%
haftmann@20967
    29
\begin{isamarkuptext}%
haftmann@22317
    30
Type classes were introduces by Wadler and Blott \cite{wadler89how}
haftmann@22317
    31
  into the Haskell language, to allow for a reasonable implementation
haftmann@22317
    32
  of overloading\footnote{throughout this tutorial, we are referring
haftmann@22317
    33
  to classical Haskell 1.0 type classes, not considering
haftmann@22317
    34
  later additions in expressiveness}.
haftmann@22317
    35
  As a canonical example, a polymorphic equality function
haftmann@22317
    36
  \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on different
haftmann@22550
    37
  types for \isa{{\isasymalpha}}, which is achieved by splitting introduction
haftmann@22317
    38
  of the \isa{eq} function from its overloaded definitions by means
haftmann@22317
    39
  of \isa{class} and \isa{instance} declarations:
haftmann@22317
    40
haftmann@28565
    41
  \begin{quote}
haftmann@28565
    42
haftmann@28565
    43
  \noindent\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\
haftmann@28565
    44
  \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
haftmann@22317
    45
haftmann@28565
    46
  \medskip\noindent\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
haftmann@28565
    47
  \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\
haftmann@28565
    48
  \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\
haftmann@28565
    49
  \hspace*{2ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
haftmann@28565
    50
  \hspace*{2ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
haftmann@22317
    51
haftmann@28565
    52
  \medskip\noindent\\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
haftmann@28565
    53
  \hspace*{2ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
haftmann@22317
    54
haftmann@28565
    55
  \medskip\noindent\isa{class\ ord\ extends\ eq\ where} \\
haftmann@28565
    56
  \hspace*{2ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
haftmann@28565
    57
  \hspace*{2ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
haftmann@22317
    58
haftmann@28565
    59
  \end{quote}
haftmann@28565
    60
haftmann@28565
    61
  \noindent Type variables are annotated with (finitely many) classes;
haftmann@22317
    62
  these annotations are assertions that a particular polymorphic type
haftmann@22317
    63
  provides definitions for overloaded functions.
haftmann@22317
    64
haftmann@22317
    65
  Indeed, type classes not only allow for simple overloading
haftmann@22317
    66
  but form a generic calculus, an instance of order-sorted
haftmann@23956
    67
  algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
haftmann@20967
    68
haftmann@28540
    69
  From a software engeneering point of view, type classes
haftmann@28540
    70
  roughly correspond to interfaces in object-oriented languages like Java;
haftmann@22317
    71
  so, it is naturally desirable that type classes do not only
haftmann@24991
    72
  provide functions (class parameters) but also state specifications
haftmann@22317
    73
  implementations must obey.  For example, the \isa{class\ eq}
haftmann@22550
    74
  above could be given the following specification, demanding that
haftmann@22550
    75
  \isa{class\ eq} is an equivalence relation obeying reflexivity,
haftmann@22550
    76
  symmetry and transitivity:
haftmann@22317
    77
haftmann@28565
    78
  \begin{quote}
haftmann@22317
    79
haftmann@28565
    80
  \noindent\isa{class\ eq\ where} \\
haftmann@28565
    81
  \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
haftmann@28565
    82
  \isa{satisfying} \\
haftmann@28565
    83
  \hspace*{2ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
haftmann@28565
    84
  \hspace*{2ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
haftmann@28565
    85
  \hspace*{2ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
haftmann@28565
    86
haftmann@28565
    87
  \end{quote}
haftmann@28565
    88
haftmann@28565
    89
  \noindent From a theoretic point of view, type classes are lightweight
haftmann@22479
    90
  modules; Haskell type classes may be emulated by
haftmann@22317
    91
  SML functors \cite{classes_modules}. 
haftmann@22317
    92
  Isabelle/Isar offers a discipline of type classes which brings
haftmann@22317
    93
  all those aspects together:
haftmann@22317
    94
haftmann@22317
    95
  \begin{enumerate}
haftmann@25004
    96
    \item specifying abstract parameters together with
haftmann@22317
    97
       corresponding specifications,
haftmann@28540
    98
    \item instantiating those abstract parameters by a particular
haftmann@22317
    99
       type
haftmann@22317
   100
    \item in connection with a ``less ad-hoc'' approach to overloading,
haftmann@23956
   101
    \item with a direct link to the Isabelle module system
haftmann@23956
   102
      (aka locales \cite{kammueller-locales}).
haftmann@22317
   103
  \end{enumerate}
haftmann@22317
   104
haftmann@22550
   105
  \noindent Isar type classes also directly support code generation
haftmann@22550
   106
  in a Haskell like fashion.
haftmann@22317
   107
haftmann@22317
   108
  This tutorial demonstrates common elements of structured specifications
haftmann@22317
   109
  and abstract reasoning with type classes by the algebraic hierarchy of
haftmann@22317
   110
  semigroups, monoids and groups.  Our background theory is that of
haftmann@23956
   111
  Isabelle/HOL \cite{isa-tutorial}, for which some
haftmann@22317
   112
  familiarity is assumed.
haftmann@22317
   113
haftmann@22317
   114
  Here we merely present the look-and-feel for end users.
haftmann@22317
   115
  Internally, those are mapped to more primitive Isabelle concepts.
haftmann@23956
   116
  See \cite{Haftmann-Wenzel:2006:classes} for more detail.%
haftmann@20967
   117
\end{isamarkuptext}%
haftmann@20967
   118
\isamarkuptrue%
haftmann@20967
   119
%
haftmann@20967
   120
\isamarkupsection{A simple algebra example \label{sec:example}%
haftmann@20967
   121
}
haftmann@20967
   122
\isamarkuptrue%
haftmann@20967
   123
%
haftmann@20967
   124
\isamarkupsubsection{Class definition%
haftmann@20967
   125
}
haftmann@20967
   126
\isamarkuptrue%
haftmann@20967
   127
%
haftmann@20967
   128
\begin{isamarkuptext}%
haftmann@28565
   129
Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operator \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} that is
haftmann@20967
   130
  assumed to be associative:%
haftmann@20967
   131
\end{isamarkuptext}%
haftmann@20967
   132
\isamarkuptrue%
haftmann@28565
   133
%
haftmann@28565
   134
\isadelimquote
haftmann@28565
   135
%
haftmann@28565
   136
\endisadelimquote
haftmann@28565
   137
%
haftmann@28565
   138
\isatagquote
haftmann@28565
   139
\isacommand{class}\isamarkupfalse%
haftmann@22479
   140
\ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
haftmann@28565
   141
\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
haftmann@28565
   142
\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
haftmann@28565
   143
\endisatagquote
haftmann@28565
   144
{\isafoldquote}%
haftmann@28565
   145
%
haftmann@28565
   146
\isadelimquote
haftmann@28565
   147
%
haftmann@28565
   148
\endisadelimquote
haftmann@28565
   149
%
haftmann@20967
   150
\begin{isamarkuptext}%
haftmann@28565
   151
\noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two
haftmann@28565
   152
  parts: the \qn{operational} part names the class parameter
haftmann@28565
   153
  (\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them
haftmann@28565
   154
  (\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}).  The local \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} and
haftmann@28565
   155
  \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} are lifted to the theory toplevel,
haftmann@28565
   156
  yielding the global
haftmann@24991
   157
  parameter \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
haftmann@28565
   158
  global theorem \hyperlink{fact.semigroup.assoc:}{\mbox{\isa{semigroup{\isachardot}assoc{\isacharcolon}}}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
haftmann@20967
   159
\end{isamarkuptext}%
haftmann@20967
   160
\isamarkuptrue%
haftmann@20967
   161
%
haftmann@20967
   162
\isamarkupsubsection{Class instantiation \label{sec:class_inst}%
haftmann@20967
   163
}
haftmann@20967
   164
\isamarkuptrue%
haftmann@20967
   165
%
haftmann@20967
   166
\begin{isamarkuptext}%
haftmann@20967
   167
The concrete type \isa{int} is made a \isa{semigroup}
haftmann@24991
   168
  instance by providing a suitable definition for the class parameter
haftmann@28565
   169
  \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} and a proof for the specification of \hyperlink{fact.assoc}{\mbox{\isa{assoc}}}.
haftmann@28565
   170
  This is accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:%
haftmann@20967
   171
\end{isamarkuptext}%
haftmann@20967
   172
\isamarkuptrue%
haftmann@28565
   173
%
haftmann@28565
   174
\isadelimquote
haftmann@28565
   175
%
haftmann@28565
   176
\endisadelimquote
haftmann@28565
   177
%
haftmann@28565
   178
\isatagquote
haftmann@28565
   179
\isacommand{instantiation}\isamarkupfalse%
haftmann@20967
   180
\ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
haftmann@28565
   181
\isakeyword{begin}\isanewline
haftmann@25533
   182
\isanewline
haftmann@28565
   183
\isacommand{definition}\isamarkupfalse%
haftmann@28565
   184
\isanewline
haftmann@28565
   185
\ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@20967
   186
\isanewline
haftmann@28565
   187
\isacommand{instance}\isamarkupfalse%
haftmann@28565
   188
\ \isacommand{proof}\isamarkupfalse%
haftmann@28565
   189
\isanewline
haftmann@28565
   190
\ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   191
\ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   192
\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   193
\ simp\isanewline
haftmann@28565
   194
\ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   195
\ \isacommand{show}\isamarkupfalse%
haftmann@25247
   196
\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@28565
   197
\ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   198
\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   199
\isanewline
haftmann@28565
   200
\isacommand{qed}\isamarkupfalse%
haftmann@25533
   201
\isanewline
haftmann@25533
   202
\isanewline
haftmann@28565
   203
\isacommand{end}\isamarkupfalse%
haftmann@28565
   204
%
haftmann@28565
   205
\endisatagquote
haftmann@28565
   206
{\isafoldquote}%
haftmann@28565
   207
%
haftmann@28565
   208
\isadelimquote
haftmann@28565
   209
%
haftmann@28565
   210
\endisadelimquote
haftmann@20967
   211
%
haftmann@20967
   212
\begin{isamarkuptext}%
haftmann@28565
   213
\noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} allows to define class parameters
haftmann@25533
   214
  at a particular instance using common specification tools (here,
haftmann@28565
   215
  \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}).  The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
haftmann@25533
   216
  opens a proof that the given parameters actually conform
haftmann@25533
   217
  to the class specification.  Note that the first proof step
haftmann@28565
   218
  is the \hyperlink{method.default}{\mbox{\isa{default}}} method,
haftmann@28565
   219
  which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method.
haftmann@25533
   220
  This boils down an instance judgement to the relevant primitive
haftmann@22317
   221
  proof goals and should conveniently always be the first method applied
haftmann@22317
   222
  in an instantiation proof.
haftmann@22317
   223
haftmann@25533
   224
  From now on, the type-checker will consider \isa{int}
haftmann@25533
   225
  as a \isa{semigroup} automatically, i.e.\ any general results
haftmann@25533
   226
  are immediately available on concrete instances.
haftmann@28565
   227
haftmann@22550
   228
  \medskip Another instance of \isa{semigroup} are the natural numbers:%
haftmann@20967
   229
\end{isamarkuptext}%
haftmann@20967
   230
\isamarkuptrue%
haftmann@20967
   231
%
haftmann@28565
   232
\isadelimquote
haftmann@28565
   233
%
haftmann@28565
   234
\endisadelimquote
haftmann@20967
   235
%
haftmann@28565
   236
\isatagquote
haftmann@28565
   237
\isacommand{instantiation}\isamarkupfalse%
haftmann@28565
   238
\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
haftmann@28565
   239
\isakeyword{begin}\isanewline
haftmann@20967
   240
\isanewline
haftmann@28565
   241
\isacommand{primrec}\isamarkupfalse%
haftmann@28565
   242
\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
haftmann@28565
   243
\ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
haftmann@28565
   244
\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymotimes}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@28565
   245
\isanewline
haftmann@28565
   246
\isacommand{instance}\isamarkupfalse%
haftmann@28565
   247
\ \isacommand{proof}\isamarkupfalse%
haftmann@28565
   248
\isanewline
haftmann@28565
   249
\ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   250
\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
haftmann@28565
   251
\ \ \isacommand{show}\isamarkupfalse%
haftmann@25247
   252
\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@28565
   253
\ \ \ \ \isacommand{by}\isamarkupfalse%
haftmann@25871
   254
\ {\isacharparenleft}induct\ m{\isacharparenright}\ auto\isanewline
haftmann@28565
   255
\isacommand{qed}\isamarkupfalse%
haftmann@25533
   256
\isanewline
haftmann@25533
   257
\isanewline
haftmann@28565
   258
\isacommand{end}\isamarkupfalse%
haftmann@28565
   259
%
haftmann@28565
   260
\endisatagquote
haftmann@28565
   261
{\isafoldquote}%
haftmann@28565
   262
%
haftmann@28565
   263
\isadelimquote
haftmann@28565
   264
%
haftmann@28565
   265
\endisadelimquote
haftmann@20967
   266
%
haftmann@25871
   267
\begin{isamarkuptext}%
haftmann@25871
   268
\noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat}
haftmann@25871
   269
  in the primrec declaration;  by default, the local name of
haftmann@25871
   270
  a class operation \isa{f} to instantiate on type constructor
haftmann@25871
   271
  \isa{{\isasymkappa}} are mangled as \isa{f{\isacharunderscore}{\isasymkappa}}.  In case of uncertainty,
haftmann@28565
   272
  these names may be inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command
haftmann@25871
   273
  or the corresponding ProofGeneral button.%
haftmann@25871
   274
\end{isamarkuptext}%
haftmann@25871
   275
\isamarkuptrue%
haftmann@25871
   276
%
haftmann@25247
   277
\isamarkupsubsection{Lifting and parametric types%
haftmann@25247
   278
}
haftmann@25247
   279
\isamarkuptrue%
haftmann@25247
   280
%
haftmann@20967
   281
\begin{isamarkuptext}%
haftmann@25247
   282
Overloaded definitions giving on class instantiation
haftmann@25247
   283
  may include recursion over the syntactic structure of types.
haftmann@25247
   284
  As a canonical example, we model product semigroups
haftmann@25247
   285
  using our simple algebra:%
haftmann@20967
   286
\end{isamarkuptext}%
haftmann@20967
   287
\isamarkuptrue%
haftmann@28565
   288
%
haftmann@28565
   289
\isadelimquote
haftmann@28565
   290
%
haftmann@28565
   291
\endisadelimquote
haftmann@20967
   292
%
haftmann@28565
   293
\isatagquote
haftmann@28565
   294
\isacommand{instantiation}\isamarkupfalse%
haftmann@28565
   295
\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
haftmann@28565
   296
\isakeyword{begin}\isanewline
haftmann@28565
   297
\isanewline
haftmann@28565
   298
\isacommand{definition}\isamarkupfalse%
haftmann@28565
   299
\isanewline
haftmann@28565
   300
\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@20967
   301
\isanewline
haftmann@28565
   302
\isacommand{instance}\isamarkupfalse%
haftmann@28565
   303
\ \isacommand{proof}\isamarkupfalse%
haftmann@28565
   304
\isanewline
haftmann@28565
   305
\ \ \isacommand{fix}\isamarkupfalse%
haftmann@25533
   306
\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
haftmann@28565
   307
\ \ \isacommand{show}\isamarkupfalse%
haftmann@25247
   308
\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@28565
   309
\ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@25247
   310
\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@25247
   311
\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
haftmann@28565
   312
\isacommand{qed}\isamarkupfalse%
haftmann@25533
   313
\ \ \ \ \ \ \isanewline
haftmann@25533
   314
\isanewline
haftmann@28565
   315
\isacommand{end}\isamarkupfalse%
haftmann@28565
   316
%
haftmann@28565
   317
\endisatagquote
haftmann@28565
   318
{\isafoldquote}%
haftmann@28565
   319
%
haftmann@28565
   320
\isadelimquote
haftmann@28565
   321
%
haftmann@28565
   322
\endisadelimquote
haftmann@20967
   323
%
haftmann@25247
   324
\begin{isamarkuptext}%
haftmann@25247
   325
\noindent Associativity from product semigroups is
haftmann@25247
   326
  established using
haftmann@28565
   327
  the definition of \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} on products and the hypothetical
wenzelm@27507
   328
  associativity of the type components;  these hypotheses
haftmann@25247
   329
  are facts due to the \isa{semigroup} constraints imposed
haftmann@28565
   330
  on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition.
haftmann@25247
   331
  Indeed, this pattern often occurs with parametric types
haftmann@25247
   332
  and type classes.%
haftmann@25247
   333
\end{isamarkuptext}%
haftmann@25247
   334
\isamarkuptrue%
haftmann@25247
   335
%
haftmann@25247
   336
\isamarkupsubsection{Subclassing%
haftmann@20967
   337
}
haftmann@20967
   338
\isamarkuptrue%
haftmann@20967
   339
%
haftmann@20967
   340
\begin{isamarkuptext}%
haftmann@22317
   341
We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral)
haftmann@20967
   342
  by extending \isa{semigroup}
haftmann@24991
   343
  with one additional parameter \isa{neutral} together
haftmann@20967
   344
  with its property:%
haftmann@20967
   345
\end{isamarkuptext}%
haftmann@20967
   346
\isamarkuptrue%
haftmann@28565
   347
%
haftmann@28565
   348
\isadelimquote
haftmann@28565
   349
%
haftmann@28565
   350
\endisadelimquote
haftmann@28565
   351
%
haftmann@28565
   352
\isatagquote
haftmann@28565
   353
\isacommand{class}\isamarkupfalse%
haftmann@20967
   354
\ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
haftmann@28565
   355
\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
haftmann@28565
   356
\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
haftmann@28565
   357
\endisatagquote
haftmann@28565
   358
{\isafoldquote}%
haftmann@28565
   359
%
haftmann@28565
   360
\isadelimquote
haftmann@28565
   361
%
haftmann@28565
   362
\endisadelimquote
haftmann@28565
   363
%
haftmann@20967
   364
\begin{isamarkuptext}%
haftmann@25247
   365
\noindent Again, we prove some instances, by
haftmann@24991
   366
  providing suitable parameter definitions and proofs for the
wenzelm@27507
   367
  additional specifications.  Observe that instantiations
haftmann@25533
   368
  for types with the same arity may be simultaneous:%
haftmann@20967
   369
\end{isamarkuptext}%
haftmann@20967
   370
\isamarkuptrue%
haftmann@25533
   371
\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
haftmann@25533
   372
\ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
haftmann@25533
   373
\ \ \ \ \isakeyword{begin}\isanewline
haftmann@25533
   374
\isanewline
haftmann@25533
   375
\ \ \ \ \isacommand{definition}\isamarkupfalse%
haftmann@25533
   376
\isanewline
haftmann@25533
   377
\ \ \ \ \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@25533
   378
\isanewline
haftmann@25533
   379
\ \ \ \ \isacommand{definition}\isamarkupfalse%
haftmann@25533
   380
\isanewline
haftmann@25533
   381
\ \ \ \ \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@25533
   382
\isanewline
haftmann@20967
   383
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   384
%
haftmann@20967
   385
\isadelimproof
haftmann@25533
   386
\ %
haftmann@20967
   387
\endisadelimproof
haftmann@20967
   388
%
haftmann@20967
   389
\isatagproof
haftmann@20967
   390
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   391
\isanewline
haftmann@20967
   392
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   393
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
haftmann@20967
   394
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@25247
   395
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
haftmann@25247
   396
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
wenzelm@26991
   397
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   398
\ simp\isanewline
haftmann@25533
   399
\ \ \ \ \isacommand{next}\isamarkupfalse%
haftmann@20967
   400
\isanewline
haftmann@20967
   401
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   402
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
haftmann@20967
   403
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@25247
   404
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
haftmann@25247
   405
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   406
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   407
\ simp\isanewline
haftmann@20967
   408
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   409
%
haftmann@20967
   410
\endisatagproof
haftmann@20967
   411
{\isafoldproof}%
haftmann@20967
   412
%
haftmann@20967
   413
\isadelimproof
haftmann@20967
   414
%
haftmann@20967
   415
\endisadelimproof
haftmann@20967
   416
\isanewline
haftmann@25533
   417
\isanewline
haftmann@25533
   418
\ \ \ \ \isacommand{end}\isamarkupfalse%
haftmann@25533
   419
\isanewline
haftmann@25533
   420
\isanewline
haftmann@25533
   421
\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
haftmann@25247
   422
\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
haftmann@25533
   423
\ \ \ \ \isakeyword{begin}\isanewline
haftmann@25533
   424
\isanewline
haftmann@25533
   425
\ \ \ \ \isacommand{definition}\isamarkupfalse%
haftmann@25533
   426
\isanewline
haftmann@25533
   427
\ \ \ \ \ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@25533
   428
\isanewline
haftmann@25533
   429
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   430
%
haftmann@20967
   431
\isadelimproof
haftmann@25533
   432
\ %
haftmann@20967
   433
\endisadelimproof
haftmann@20967
   434
%
haftmann@20967
   435
\isatagproof
haftmann@20967
   436
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   437
\isanewline
haftmann@20967
   438
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@25533
   439
\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoidl\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline
haftmann@20967
   440
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@25247
   441
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
haftmann@25247
   442
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@25247
   443
\ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@25247
   444
\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutl{\isacharparenright}\isanewline
haftmann@20967
   445
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   446
%
haftmann@20967
   447
\endisatagproof
haftmann@20967
   448
{\isafoldproof}%
haftmann@20967
   449
%
haftmann@20967
   450
\isadelimproof
haftmann@20967
   451
%
haftmann@20967
   452
\endisadelimproof
haftmann@25533
   453
\isanewline
haftmann@25533
   454
\isanewline
haftmann@25533
   455
\ \ \ \isacommand{end}\isamarkupfalse%
haftmann@20967
   456
%
haftmann@20967
   457
\begin{isamarkuptext}%
haftmann@22317
   458
\noindent Fully-fledged monoids are modelled by another subclass
haftmann@24991
   459
  which does not add new parameters but tightens the specification:%
haftmann@20967
   460
\end{isamarkuptext}%
haftmann@20967
   461
\isamarkuptrue%
haftmann@20967
   462
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@20967
   463
\ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
haftmann@25247
   464
\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
haftmann@25247
   465
\isanewline
haftmann@25533
   466
\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
haftmann@25533
   467
\ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline
haftmann@25533
   468
\ \ \ \ \isakeyword{begin}\isanewline
haftmann@25533
   469
\isanewline
haftmann@20967
   470
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   471
%
haftmann@20967
   472
\isadelimproof
haftmann@25533
   473
\ %
haftmann@20967
   474
\endisadelimproof
haftmann@20967
   475
%
haftmann@20967
   476
\isatagproof
haftmann@20967
   477
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   478
\isanewline
haftmann@20967
   479
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   480
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
haftmann@20967
   481
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@25247
   482
\ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
haftmann@25247
   483
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@25871
   484
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@25871
   485
\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
haftmann@25533
   486
\ \ \ \ \isacommand{next}\isamarkupfalse%
haftmann@20967
   487
\isanewline
haftmann@20967
   488
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   489
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
haftmann@20967
   490
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@25247
   491
\ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
haftmann@25247
   492
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   493
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   494
\ simp\isanewline
haftmann@25247
   495
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@25247
   496
%
haftmann@25247
   497
\endisatagproof
haftmann@25247
   498
{\isafoldproof}%
haftmann@25247
   499
%
haftmann@25247
   500
\isadelimproof
haftmann@25247
   501
%
haftmann@25247
   502
\endisadelimproof
haftmann@20967
   503
\isanewline
haftmann@25533
   504
\isanewline
haftmann@25533
   505
\ \ \ \ \isacommand{end}\isamarkupfalse%
haftmann@25533
   506
\isanewline
haftmann@25533
   507
\isanewline
haftmann@25533
   508
\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
haftmann@25533
   509
\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
haftmann@25533
   510
\ \ \ \ \isakeyword{begin}\isanewline
haftmann@25533
   511
\isanewline
haftmann@25247
   512
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@25247
   513
%
haftmann@25247
   514
\isadelimproof
haftmann@25533
   515
\ %
haftmann@25247
   516
\endisadelimproof
haftmann@25247
   517
%
haftmann@25247
   518
\isatagproof
haftmann@25247
   519
\isacommand{proof}\isamarkupfalse%
haftmann@25247
   520
\ \isanewline
haftmann@25247
   521
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@25533
   522
\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoid\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoid{\isachardoublequoteclose}\isanewline
haftmann@25247
   523
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@25247
   524
\ {\isachardoublequoteopen}p\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
haftmann@25247
   525
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@25247
   526
\ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@25247
   527
\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutr{\isacharparenright}\isanewline
haftmann@20967
   528
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   529
%
haftmann@20967
   530
\endisatagproof
haftmann@20967
   531
{\isafoldproof}%
haftmann@20967
   532
%
haftmann@20967
   533
\isadelimproof
haftmann@20967
   534
%
haftmann@20967
   535
\endisadelimproof
haftmann@25533
   536
\isanewline
haftmann@25533
   537
\isanewline
haftmann@25533
   538
\ \ \ \ \isacommand{end}\isamarkupfalse%
haftmann@22317
   539
%
haftmann@22317
   540
\begin{isamarkuptext}%
haftmann@22317
   541
\noindent To finish our small algebra example, we add a \isa{group} class
haftmann@22317
   542
  with a corresponding instance:%
haftmann@22317
   543
\end{isamarkuptext}%
haftmann@22317
   544
\isamarkuptrue%
haftmann@20967
   545
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@20967
   546
\ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
haftmann@25200
   547
\ \ \ \ \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
haftmann@25200
   548
\ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
haftmann@20967
   549
\isanewline
haftmann@25533
   550
\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
haftmann@20967
   551
\ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
haftmann@25533
   552
\ \ \ \ \isakeyword{begin}\isanewline
haftmann@25533
   553
\isanewline
haftmann@25533
   554
\ \ \ \ \isacommand{definition}\isamarkupfalse%
haftmann@25533
   555
\isanewline
haftmann@25533
   556
\ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}i{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@25533
   557
\isanewline
haftmann@25533
   558
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   559
%
haftmann@20967
   560
\isadelimproof
haftmann@25533
   561
\ %
haftmann@20967
   562
\endisadelimproof
haftmann@20967
   563
%
haftmann@20967
   564
\isatagproof
haftmann@20967
   565
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   566
\isanewline
haftmann@20967
   567
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   568
\ i\ {\isacharcolon}{\isacharcolon}\ int\isanewline
haftmann@20967
   569
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
haftmann@20967
   570
\ {\isachardoublequoteopen}{\isacharminus}i\ {\isacharplus}\ i\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   571
\ simp\isanewline
haftmann@20967
   572
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   573
\ \isacommand{show}\isamarkupfalse%
haftmann@22550
   574
\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
haftmann@25247
   575
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@25247
   576
\ mult{\isacharunderscore}int{\isacharunderscore}def\ neutral{\isacharunderscore}int{\isacharunderscore}def\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   577
\isanewline
haftmann@20967
   578
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   579
%
haftmann@20967
   580
\endisatagproof
haftmann@20967
   581
{\isafoldproof}%
haftmann@20967
   582
%
haftmann@20967
   583
\isadelimproof
haftmann@20967
   584
%
haftmann@20967
   585
\endisadelimproof
haftmann@25533
   586
\isanewline
haftmann@25533
   587
\isanewline
haftmann@25533
   588
\ \ \ \ \isacommand{end}\isamarkupfalse%
haftmann@20967
   589
%
haftmann@22317
   590
\isamarkupsection{Type classes as locales%
haftmann@22317
   591
}
haftmann@22317
   592
\isamarkuptrue%
haftmann@22317
   593
%
haftmann@22317
   594
\isamarkupsubsection{A look behind the scene%
haftmann@22317
   595
}
haftmann@22317
   596
\isamarkuptrue%
haftmann@22317
   597
%
haftmann@22317
   598
\begin{isamarkuptext}%
haftmann@22479
   599
The example above gives an impression how Isar type classes work
haftmann@22479
   600
  in practice.  As stated in the introduction, classes also provide
haftmann@22479
   601
  a link to Isar's locale system.  Indeed, the logical core of a class
haftmann@22479
   602
  is nothing else than a locale:%
haftmann@22479
   603
\end{isamarkuptext}%
haftmann@22479
   604
\isamarkuptrue%
haftmann@22479
   605
\isacommand{class}\isamarkupfalse%
haftmann@22479
   606
\ idem\ {\isacharequal}\ type\ {\isacharplus}\isanewline
haftmann@22479
   607
\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
haftmann@22479
   608
\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
haftmann@22479
   609
\begin{isamarkuptext}%
haftmann@22479
   610
\noindent essentially introduces the locale%
haftmann@22479
   611
\end{isamarkuptext}%
haftmann@22479
   612
\isamarkuptrue%
haftmann@22317
   613
%
haftmann@28565
   614
\isadeliminvisible
haftmann@22479
   615
%
haftmann@28565
   616
\endisadeliminvisible
haftmann@22479
   617
%
haftmann@28565
   618
\isataginvisible
haftmann@28565
   619
\isacommand{setup}\isamarkupfalse%
haftmann@28565
   620
\ {\isacharverbatimopen}\ Sign{\isachardot}add{\isacharunderscore}path\ {\isachardoublequote}foo{\isachardoublequote}\ {\isacharverbatimclose}%
haftmann@28565
   621
\endisataginvisible
haftmann@28565
   622
{\isafoldinvisible}%
haftmann@22479
   623
%
haftmann@28565
   624
\isadeliminvisible
haftmann@22479
   625
%
haftmann@28565
   626
\endisadeliminvisible
haftmann@28565
   627
\isanewline
haftmann@28565
   628
\isanewline
haftmann@22479
   629
\isacommand{locale}\isamarkupfalse%
haftmann@22479
   630
\ idem\ {\isacharequal}\isanewline
haftmann@22479
   631
\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
haftmann@22479
   632
\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
haftmann@22479
   633
\begin{isamarkuptext}%
haftmann@22550
   634
\noindent together with corresponding constant(s):%
haftmann@22479
   635
\end{isamarkuptext}%
haftmann@22479
   636
\isamarkuptrue%
haftmann@22479
   637
\isacommand{consts}\isamarkupfalse%
haftmann@22550
   638
\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
haftmann@22550
   639
\begin{isamarkuptext}%
haftmann@22550
   640
\noindent The connection to the type system is done by means
haftmann@22550
   641
  of a primitive axclass%
haftmann@22550
   642
\end{isamarkuptext}%
haftmann@22550
   643
\isamarkuptrue%
haftmann@22479
   644
\isacommand{axclass}\isamarkupfalse%
haftmann@22479
   645
\ idem\ {\isacharless}\ type\isanewline
haftmann@22479
   646
\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
haftmann@22479
   647
\begin{isamarkuptext}%
wenzelm@22649
   648
\noindent together with a corresponding interpretation:%
haftmann@22479
   649
\end{isamarkuptext}%
haftmann@22479
   650
\isamarkuptrue%
haftmann@22479
   651
\isacommand{interpretation}\isamarkupfalse%
haftmann@22479
   652
\ idem{\isacharunderscore}class{\isacharcolon}\isanewline
haftmann@25533
   653
\ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
haftmann@22479
   654
%
haftmann@22479
   655
\isadelimproof
haftmann@22479
   656
%
haftmann@22479
   657
\endisadelimproof
haftmann@22479
   658
%
haftmann@22479
   659
\isatagproof
haftmann@22479
   660
\isacommand{by}\isamarkupfalse%
haftmann@22550
   661
\ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ idem{\isacharparenright}%
haftmann@22479
   662
\endisatagproof
haftmann@22479
   663
{\isafoldproof}%
haftmann@22479
   664
%
haftmann@22479
   665
\isadelimproof
haftmann@28565
   666
\isanewline
haftmann@22479
   667
%
haftmann@22479
   668
\endisadelimproof
haftmann@22479
   669
%
haftmann@28565
   670
\isadeliminvisible
haftmann@28565
   671
\isanewline
haftmann@22479
   672
%
haftmann@28565
   673
\endisadeliminvisible
haftmann@22479
   674
%
haftmann@28565
   675
\isataginvisible
haftmann@28565
   676
\isacommand{setup}\isamarkupfalse%
haftmann@28565
   677
\ {\isacharverbatimopen}\ Sign{\isachardot}parent{\isacharunderscore}path\ {\isacharverbatimclose}%
haftmann@28565
   678
\endisataginvisible
haftmann@28565
   679
{\isafoldinvisible}%
haftmann@22479
   680
%
haftmann@28565
   681
\isadeliminvisible
haftmann@22479
   682
%
haftmann@28565
   683
\endisadeliminvisible
haftmann@22479
   684
%
haftmann@22479
   685
\begin{isamarkuptext}%
haftmann@22479
   686
This give you at hand the full power of the Isabelle module system;
haftmann@22479
   687
  conclusions in locale \isa{idem} are implicitly propagated
haftmann@22479
   688
  to class \isa{idem}.%
haftmann@22317
   689
\end{isamarkuptext}%
haftmann@22317
   690
\isamarkuptrue%
haftmann@22317
   691
%
haftmann@20967
   692
\isamarkupsubsection{Abstract reasoning%
haftmann@20967
   693
}
haftmann@20967
   694
\isamarkuptrue%
haftmann@20967
   695
%
haftmann@20967
   696
\begin{isamarkuptext}%
haftmann@22479
   697
Isabelle locales enable reasoning at a general level, while results
haftmann@20967
   698
  are implicitly transferred to all instances.  For example, we can
haftmann@20967
   699
  now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which
haftmann@25247
   700
  states that the function \isa{{\isacharparenleft}x\ {\isasymotimes}{\isacharparenright}} is injective:%
haftmann@20967
   701
\end{isamarkuptext}%
haftmann@20967
   702
\isamarkuptrue%
haftmann@20967
   703
\ \ \ \ \isacommand{lemma}\isamarkupfalse%
haftmann@25200
   704
\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
haftmann@20967
   705
%
haftmann@20967
   706
\isadelimproof
haftmann@20967
   707
\ \ \ \ %
haftmann@20967
   708
\endisadelimproof
haftmann@20967
   709
%
haftmann@20967
   710
\isatagproof
haftmann@20967
   711
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   712
\isanewline
haftmann@25247
   713
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
haftmann@25200
   714
\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
haftmann@22479
   715
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   716
\ \isacommand{have}\isamarkupfalse%
haftmann@25200
   717
\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   718
\ simp\isanewline
haftmann@22479
   719
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   720
\ \isacommand{have}\isamarkupfalse%
haftmann@25200
   721
\ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
haftmann@20967
   722
\ assoc\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   723
\ simp\isanewline
haftmann@22479
   724
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   725
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   726
\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
haftmann@20967
   727
\ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   728
\ simp\isanewline
haftmann@20967
   729
\ \ \ \ \isacommand{next}\isamarkupfalse%
haftmann@20967
   730
\isanewline
haftmann@25247
   731
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
haftmann@20967
   732
\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
haftmann@22479
   733
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   734
\ \isacommand{show}\isamarkupfalse%
haftmann@25200
   735
\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   736
\ simp\isanewline
haftmann@20967
   737
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   738
%
haftmann@20967
   739
\endisatagproof
haftmann@20967
   740
{\isafoldproof}%
haftmann@20967
   741
%
haftmann@20967
   742
\isadelimproof
haftmann@20967
   743
%
haftmann@20967
   744
\endisadelimproof
haftmann@20967
   745
%
haftmann@20967
   746
\begin{isamarkuptext}%
haftmann@28565
   747
\noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target specification
haftmann@20967
   748
  indicates that the result is recorded within that context for later
haftmann@28565
   749
  use.  This local theorem is also lifted to the global one \hyperlink{fact.group.left-cancel:}{\mbox{\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
   750
  \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
   751
\end{isamarkuptext}%
haftmann@20967
   752
\isamarkuptrue%
haftmann@20967
   753
%
haftmann@23956
   754
\isamarkupsubsection{Derived definitions%
haftmann@23956
   755
}
haftmann@23956
   756
\isamarkuptrue%
haftmann@23956
   757
%
haftmann@23956
   758
\begin{isamarkuptext}%
haftmann@23956
   759
Isabelle locales support a concept of local definitions
haftmann@23956
   760
  in locales:%
haftmann@23956
   761
\end{isamarkuptext}%
haftmann@23956
   762
\isamarkuptrue%
haftmann@25871
   763
\ \ \ \ \isacommand{primrec}\isamarkupfalse%
haftmann@28540
   764
\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@25200
   765
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
haftmann@25200
   766
\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}%
haftmann@23956
   767
\begin{isamarkuptext}%
haftmann@23956
   768
\noindent If the locale \isa{group} is also a class, this local
haftmann@23956
   769
  definition is propagated onto a global definition of
haftmann@23956
   770
  \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}}
haftmann@23956
   771
  with corresponding theorems
haftmann@23956
   772
haftmann@23956
   773
  \isa{pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}\isasep\isanewline%
haftmann@23956
   774
pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x}.
haftmann@23956
   775
haftmann@23956
   776
  \noindent As you can see from this example, for local
haftmann@23956
   777
  definitions you may use any specification tool
haftmann@23956
   778
  which works together with locales (e.g. \cite{krauss2006}).%
haftmann@23956
   779
\end{isamarkuptext}%
haftmann@23956
   780
\isamarkuptrue%
haftmann@23956
   781
%
haftmann@25247
   782
\isamarkupsubsection{A functor analogy%
haftmann@25247
   783
}
haftmann@25247
   784
\isamarkuptrue%
haftmann@25247
   785
%
haftmann@25247
   786
\begin{isamarkuptext}%
haftmann@25247
   787
We introduced Isar classes by analogy to type classes
haftmann@25247
   788
  functional programming;  if we reconsider this in the
haftmann@25247
   789
  context of what has been said about type classes and locales,
haftmann@25247
   790
  we can drive this analogy further by stating that type
haftmann@25247
   791
  classes essentially correspond to functors which have
haftmann@25247
   792
  a canonical interpretation as type classes.
haftmann@25247
   793
  Anyway, there is also the possibility of other interpretations.
haftmann@25247
   794
  For example, also \isa{list}s form a monoid with
haftmann@28565
   795
  \isa{append} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
haftmann@25247
   796
  seems inappropriate to apply to lists
wenzelm@27507
   797
  the same operations as for genuinely algebraic types.
haftmann@25247
   798
  In such a case, we simply can do a particular interpretation
haftmann@25247
   799
  of monoids for lists:%
haftmann@25247
   800
\end{isamarkuptext}%
haftmann@25247
   801
\isamarkuptrue%
haftmann@25247
   802
\ \ \ \ \isacommand{interpretation}\isamarkupfalse%
haftmann@28565
   803
\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
haftmann@25247
   804
%
haftmann@25247
   805
\isadelimproof
haftmann@25247
   806
\ \ \ \ \ \ %
haftmann@25247
   807
\endisadelimproof
haftmann@25247
   808
%
haftmann@25247
   809
\isatagproof
haftmann@25247
   810
\isacommand{by}\isamarkupfalse%
haftmann@25247
   811
\ unfold{\isacharunderscore}locales\ auto%
haftmann@25247
   812
\endisatagproof
haftmann@25247
   813
{\isafoldproof}%
haftmann@25247
   814
%
haftmann@25247
   815
\isadelimproof
haftmann@25247
   816
%
haftmann@25247
   817
\endisadelimproof
haftmann@25247
   818
%
haftmann@25247
   819
\begin{isamarkuptext}%
haftmann@25247
   820
\noindent This enables us to apply facts on monoids
haftmann@25247
   821
  to lists, e.g. \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ x\ {\isacharequal}\ x}.
haftmann@25247
   822
haftmann@25247
   823
  When using this interpretation pattern, it may also
haftmann@25247
   824
  be appropriate to map derived definitions accordingly:%
haftmann@25247
   825
\end{isamarkuptext}%
haftmann@25247
   826
\isamarkuptrue%
haftmann@25247
   827
\ \ \ \ \isacommand{fun}\isamarkupfalse%
haftmann@28540
   828
\ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@25247
   829
\ \ \ \ \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
haftmann@25247
   830
\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
haftmann@25247
   831
\isanewline
haftmann@25247
   832
\ \ \ \ \isacommand{interpretation}\isamarkupfalse%
haftmann@28565
   833
\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline
haftmann@28565
   834
\ \ \ \ \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
haftmann@25247
   835
%
haftmann@25247
   836
\isadelimproof
haftmann@25247
   837
\ \ \ \ %
haftmann@25247
   838
\endisadelimproof
haftmann@25247
   839
%
haftmann@25247
   840
\isatagproof
haftmann@25247
   841
\isacommand{proof}\isamarkupfalse%
haftmann@28540
   842
\ {\isacharminus}\isanewline
haftmann@28540
   843
\ \ \ \ \ \ \isacommand{interpret}\isamarkupfalse%
haftmann@28565
   844
\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
haftmann@25247
   845
\isanewline
haftmann@25247
   846
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@28565
   847
\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
haftmann@28540
   848
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
haftmann@28540
   849
\isanewline
haftmann@28540
   850
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@28540
   851
\ n\isanewline
haftmann@28540
   852
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@28565
   853
\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
haftmann@28540
   854
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
haftmann@25247
   855
\ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline
haftmann@28540
   856
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@28540
   857
\isanewline
haftmann@25247
   858
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@28540
   859
\ intro{\isacharunderscore}locales%
haftmann@25247
   860
\endisatagproof
haftmann@25247
   861
{\isafoldproof}%
haftmann@25247
   862
%
haftmann@25247
   863
\isadelimproof
haftmann@25247
   864
%
haftmann@25247
   865
\endisadelimproof
haftmann@25247
   866
%
haftmann@24991
   867
\isamarkupsubsection{Additional subclass relations%
haftmann@24991
   868
}
haftmann@24991
   869
\isamarkuptrue%
haftmann@24991
   870
%
haftmann@24991
   871
\begin{isamarkuptext}%
haftmann@24991
   872
Any \isa{group} is also a \isa{monoid};  this
haftmann@25247
   873
  can be made explicit by claiming an additional
haftmann@25247
   874
  subclass relation,
haftmann@24991
   875
  together with a proof of the logical difference:%
haftmann@24991
   876
\end{isamarkuptext}%
haftmann@24991
   877
\isamarkuptrue%
haftmann@24991
   878
\ \ \ \ \isacommand{subclass}\isamarkupfalse%
haftmann@24991
   879
\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ monoid\isanewline
haftmann@24991
   880
%
haftmann@24991
   881
\isadelimproof
haftmann@24991
   882
\ \ \ \ %
haftmann@24991
   883
\endisadelimproof
haftmann@24991
   884
%
haftmann@24991
   885
\isatagproof
haftmann@24991
   886
\isacommand{proof}\isamarkupfalse%
haftmann@24991
   887
\ unfold{\isacharunderscore}locales\isanewline
haftmann@24991
   888
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@24991
   889
\ x\isanewline
haftmann@24991
   890
\ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
haftmann@24991
   891
\ invl\ \isacommand{have}\isamarkupfalse%
haftmann@25200
   892
\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@24991
   893
\ simp\isanewline
haftmann@24991
   894
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
haftmann@24991
   895
\ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
haftmann@25200
   896
\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ {\isasymone}{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@24991
   897
\ simp\isanewline
haftmann@24991
   898
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
haftmann@24991
   899
\ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse%
haftmann@25200
   900
\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@24991
   901
\ simp\isanewline
haftmann@24991
   902
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@24991
   903
%
haftmann@24991
   904
\endisatagproof
haftmann@24991
   905
{\isafoldproof}%
haftmann@24991
   906
%
haftmann@24991
   907
\isadelimproof
haftmann@24991
   908
%
haftmann@24991
   909
\endisadelimproof
haftmann@24991
   910
%
haftmann@24991
   911
\begin{isamarkuptext}%
haftmann@25200
   912
\noindent The logical proof is carried out on the locale level
haftmann@24991
   913
  and thus conveniently is opened using the \isa{unfold{\isacharunderscore}locales}
haftmann@24991
   914
  method which only leaves the logical differences still
haftmann@25200
   915
  open to proof to the user.  Afterwards it is propagated
haftmann@24991
   916
  to the type system, making \isa{group} an instance of
haftmann@25247
   917
  \isa{monoid} by adding an additional edge
haftmann@25247
   918
  to the graph of subclass relations
haftmann@25247
   919
  (cf.\ \figref{fig:subclass}).
haftmann@25247
   920
haftmann@25247
   921
  \begin{figure}[htbp]
haftmann@25247
   922
   \begin{center}
haftmann@25247
   923
     \small
haftmann@25247
   924
     \unitlength 0.6mm
haftmann@25247
   925
     \begin{picture}(40,60)(0,0)
haftmann@25247
   926
       \put(20,60){\makebox(0,0){\isa{semigroup}}}
haftmann@25247
   927
       \put(20,40){\makebox(0,0){\isa{monoidl}}}
haftmann@25247
   928
       \put(00,20){\makebox(0,0){\isa{monoid}}}
haftmann@25247
   929
       \put(40,00){\makebox(0,0){\isa{group}}}
haftmann@25247
   930
       \put(20,55){\vector(0,-1){10}}
haftmann@25247
   931
       \put(15,35){\vector(-1,-1){10}}
haftmann@25247
   932
       \put(25,35){\vector(1,-3){10}}
haftmann@25247
   933
     \end{picture}
haftmann@25247
   934
     \hspace{8em}
haftmann@25247
   935
     \begin{picture}(40,60)(0,0)
haftmann@25247
   936
       \put(20,60){\makebox(0,0){\isa{semigroup}}}
haftmann@25247
   937
       \put(20,40){\makebox(0,0){\isa{monoidl}}}
haftmann@25247
   938
       \put(00,20){\makebox(0,0){\isa{monoid}}}
haftmann@25247
   939
       \put(40,00){\makebox(0,0){\isa{group}}}
haftmann@25247
   940
       \put(20,55){\vector(0,-1){10}}
haftmann@25247
   941
       \put(15,35){\vector(-1,-1){10}}
haftmann@25247
   942
       \put(05,15){\vector(3,-1){30}}
haftmann@25247
   943
     \end{picture}
haftmann@25247
   944
     \caption{Subclass relationship of monoids and groups:
haftmann@25247
   945
        before and after establishing the relationship
haftmann@25247
   946
        \isa{group\ {\isasymsubseteq}\ monoid};  transitive edges left out.}
haftmann@25247
   947
     \label{fig:subclass}
haftmann@25247
   948
   \end{center}
haftmann@25247
   949
  \end{figure}
haftmann@25247
   950
haftmann@25247
   951
  For illustration, a derived definition
haftmann@24991
   952
  in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
haftmann@24991
   953
\end{isamarkuptext}%
haftmann@24991
   954
\isamarkuptrue%
haftmann@28565
   955
%
haftmann@28565
   956
\isadelimquote
haftmann@28565
   957
%
haftmann@28565
   958
\endisadelimquote
haftmann@28565
   959
%
haftmann@28565
   960
\isatagquote
haftmann@28565
   961
\isacommand{definition}\isamarkupfalse%
haftmann@28565
   962
\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@28565
   963
\ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
haftmann@28565
   964
\ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
haftmann@28565
   965
\ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
haftmann@28565
   966
\endisatagquote
haftmann@28565
   967
{\isafoldquote}%
haftmann@28565
   968
%
haftmann@28565
   969
\isadelimquote
haftmann@28565
   970
%
haftmann@28565
   971
\endisadelimquote
haftmann@28565
   972
%
haftmann@24991
   973
\begin{isamarkuptext}%
haftmann@25247
   974
\noindent yields the global definition of
haftmann@24991
   975
  \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
haftmann@24991
   976
  with the corresponding theorem \isa{pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{0}}\ {\isasymle}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}}.%
haftmann@24991
   977
\end{isamarkuptext}%
haftmann@24991
   978
\isamarkuptrue%
haftmann@24991
   979
%
haftmann@25868
   980
\isamarkupsubsection{A note on syntax%
haftmann@25868
   981
}
haftmann@25868
   982
\isamarkuptrue%
haftmann@25868
   983
%
haftmann@25868
   984
\begin{isamarkuptext}%
haftmann@25868
   985
As a commodity, class context syntax allows to refer
wenzelm@27507
   986
  to local class operations and their global counterparts
haftmann@25868
   987
  uniformly;  type inference resolves ambiguities.  For example:%
haftmann@25868
   988
\end{isamarkuptext}%
haftmann@25868
   989
\isamarkuptrue%
haftmann@28565
   990
%
haftmann@28565
   991
\isadelimquote
haftmann@28565
   992
%
haftmann@28565
   993
\endisadelimquote
haftmann@28565
   994
%
haftmann@28565
   995
\isatagquote
haftmann@25868
   996
\isacommand{context}\isamarkupfalse%
haftmann@25868
   997
\ semigroup\isanewline
haftmann@25868
   998
\isakeyword{begin}\isanewline
haftmann@25868
   999
\isanewline
haftmann@25868
  1000
\isacommand{term}\isamarkupfalse%
haftmann@25868
  1001
\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
haftmann@25868
  1002
\isamarkupcmt{example 1%
haftmann@25868
  1003
}
haftmann@25868
  1004
\isanewline
haftmann@25868
  1005
\isacommand{term}\isamarkupfalse%
haftmann@25868
  1006
\ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
haftmann@25868
  1007
\isamarkupcmt{example 2%
haftmann@25868
  1008
}
haftmann@28565
  1009
%
haftmann@28565
  1010
\endisatagquote
haftmann@28565
  1011
{\isafoldquote}%
haftmann@28565
  1012
%
haftmann@28565
  1013
\isadelimquote
haftmann@28565
  1014
%
haftmann@28565
  1015
\endisadelimquote
haftmann@25868
  1016
\isanewline
haftmann@25868
  1017
\isanewline
haftmann@25868
  1018
\isacommand{end}\isamarkupfalse%
haftmann@25868
  1019
\isanewline
haftmann@28565
  1020
%
haftmann@28565
  1021
\isadelimquote
haftmann@25868
  1022
\isanewline
haftmann@28565
  1023
%
haftmann@28565
  1024
\endisadelimquote
haftmann@28565
  1025
%
haftmann@28565
  1026
\isatagquote
haftmann@25868
  1027
\isacommand{term}\isamarkupfalse%
haftmann@25868
  1028
\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
haftmann@25868
  1029
\isamarkupcmt{example 3%
haftmann@25868
  1030
}
haftmann@25868
  1031
%
haftmann@28565
  1032
\endisatagquote
haftmann@28565
  1033
{\isafoldquote}%
haftmann@28565
  1034
%
haftmann@28565
  1035
\isadelimquote
haftmann@28565
  1036
%
haftmann@28565
  1037
\endisadelimquote
haftmann@28565
  1038
%
haftmann@25868
  1039
\begin{isamarkuptext}%
haftmann@25868
  1040
\noindent Here in example 1, the term refers to the local class operation
haftmann@25868
  1041
  \isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type constraint
haftmann@25868
  1042
  enforces the global class operation \isa{mult\ {\isacharbrackleft}nat{\isacharbrackright}}.
haftmann@25868
  1043
  In the global context in example 3, the reference is
haftmann@25868
  1044
  to the polymorphic global class operation \isa{mult\ {\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isasymColon}\ semigroup{\isacharbrackright}}.%
haftmann@25868
  1045
\end{isamarkuptext}%
haftmann@25868
  1046
\isamarkuptrue%
haftmann@25868
  1047
%
haftmann@25247
  1048
\isamarkupsection{Type classes and code generation%
haftmann@20967
  1049
}
haftmann@20967
  1050
\isamarkuptrue%
haftmann@20967
  1051
%
haftmann@20967
  1052
\begin{isamarkuptext}%
haftmann@22317
  1053
Turning back to the first motivation for type classes,
haftmann@22317
  1054
  namely overloading, it is obvious that overloading
haftmann@28565
  1055
  stemming from \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} statements and
haftmann@28565
  1056
  \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
haftmann@25533
  1057
  targets naturally maps to Haskell type classes.
haftmann@22317
  1058
  The code generator framework \cite{isabelle-codegen} 
haftmann@22317
  1059
  takes this into account.  Concerning target languages
haftmann@22317
  1060
  lacking type classes (e.g.~SML), type classes
haftmann@22317
  1061
  are implemented by explicit dictionary construction.
haftmann@28565
  1062
  As example, let's go back to the power function:%
haftmann@20967
  1063
\end{isamarkuptext}%
haftmann@20967
  1064
\isamarkuptrue%
haftmann@28565
  1065
%
haftmann@28565
  1066
\isadelimquote
haftmann@28565
  1067
%
haftmann@28565
  1068
\endisadelimquote
haftmann@28565
  1069
%
haftmann@28565
  1070
\isatagquote
haftmann@28565
  1071
\isacommand{definition}\isamarkupfalse%
haftmann@28565
  1072
\ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
haftmann@28565
  1073
\ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
haftmann@28565
  1074
\endisatagquote
haftmann@28565
  1075
{\isafoldquote}%
haftmann@28565
  1076
%
haftmann@28565
  1077
\isadelimquote
haftmann@28565
  1078
%
haftmann@28565
  1079
\endisadelimquote
haftmann@28565
  1080
%
haftmann@20967
  1081
\begin{isamarkuptext}%
haftmann@22317
  1082
\noindent This maps to Haskell as:%
haftmann@20967
  1083
\end{isamarkuptext}%
haftmann@20967
  1084
\isamarkuptrue%
haftmann@28540
  1085
%
haftmann@28565
  1086
\isadelimquote
haftmann@28540
  1087
%
haftmann@28565
  1088
\endisadelimquote
haftmann@28540
  1089
%
haftmann@28565
  1090
\isatagquote
haftmann@28540
  1091
%
haftmann@20967
  1092
\begin{isamarkuptext}%
haftmann@28540
  1093
\isaverbatim%
haftmann@28540
  1094
\noindent%
haftmann@28540
  1095
\verb|module Example where {|\newline%
haftmann@28540
  1096
\newline%
haftmann@28540
  1097
\newline%
haftmann@28540
  1098
\verb|data Nat = Suc Nat |\verb,|,\verb| Zero_nat;|\newline%
haftmann@28540
  1099
\newline%
haftmann@28540
  1100
\verb|nat_aux :: Integer -> Nat -> Nat;|\newline%
haftmann@28540
  1101
\verb|nat_aux i n = (if i <= 0 then n else nat_aux (i - 1) (Suc n));|\newline%
haftmann@28540
  1102
\newline%
haftmann@28540
  1103
\verb|nat :: Integer -> Nat;|\newline%
haftmann@28540
  1104
\verb|nat i = nat_aux i Zero_nat;|\newline%
haftmann@28540
  1105
\newline%
haftmann@28540
  1106
\verb|class Semigroup a where {|\newline%
haftmann@28540
  1107
\verb|  mult :: a -> a -> a;|\newline%
haftmann@28540
  1108
\verb|};|\newline%
haftmann@28540
  1109
\newline%
haftmann@28540
  1110
\verb|class (Semigroup a) => Monoidl a where {|\newline%
haftmann@28540
  1111
\verb|  neutral :: a;|\newline%
haftmann@28540
  1112
\verb|};|\newline%
haftmann@28540
  1113
\newline%
haftmann@28540
  1114
\verb|class (Monoidl a) => Monoid a where {|\newline%
haftmann@28540
  1115
\verb|};|\newline%
haftmann@28540
  1116
\newline%
haftmann@28540
  1117
\verb|class (Monoid a) => Group a where {|\newline%
haftmann@28540
  1118
\verb|  inverse :: a -> a;|\newline%
haftmann@28540
  1119
\verb|};|\newline%
haftmann@28540
  1120
\newline%
haftmann@28540
  1121
\verb|inverse_int :: Integer -> Integer;|\newline%
haftmann@28540
  1122
\verb|inverse_int i = negate i;|\newline%
haftmann@28540
  1123
\newline%
haftmann@28540
  1124
\verb|neutral_int :: Integer;|\newline%
haftmann@28540
  1125
\verb|neutral_int = 0;|\newline%
haftmann@28540
  1126
\newline%
haftmann@28540
  1127
\verb|mult_int :: Integer -> Integer -> Integer;|\newline%
haftmann@28540
  1128
\verb|mult_int i j = i + j;|\newline%
haftmann@28540
  1129
\newline%
haftmann@28540
  1130
\verb|instance Semigroup Integer where {|\newline%
haftmann@28540
  1131
\verb|  mult = mult_int;|\newline%
haftmann@28540
  1132
\verb|};|\newline%
haftmann@28540
  1133
\newline%
haftmann@28540
  1134
\verb|instance Monoidl Integer where {|\newline%
haftmann@28540
  1135
\verb|  neutral = neutral_int;|\newline%
haftmann@28540
  1136
\verb|};|\newline%
haftmann@28540
  1137
\newline%
haftmann@28540
  1138
\verb|instance Monoid Integer where {|\newline%
haftmann@28540
  1139
\verb|};|\newline%
haftmann@28540
  1140
\newline%
haftmann@28540
  1141
\verb|instance Group Integer where {|\newline%
haftmann@28540
  1142
\verb|  inverse = inverse_int;|\newline%
haftmann@28540
  1143
\verb|};|\newline%
haftmann@28540
  1144
\newline%
haftmann@28540
  1145
\verb|pow_nat :: forall a. (Monoid a) => Nat -> a -> a;|\newline%
haftmann@28540
  1146
\verb|pow_nat Zero_nat x = neutral;|\newline%
haftmann@28540
  1147
\verb|pow_nat (Suc n) x = mult x (pow_nat n x);|\newline%
haftmann@28540
  1148
\newline%
haftmann@28540
  1149
\verb|pow_int :: forall a. (Group a) => Integer -> a -> a;|\newline%
haftmann@28540
  1150
\verb|pow_int k x =|\newline%
haftmann@28540
  1151
\verb|  (if 0 <= k then pow_nat (nat k) x|\newline%
haftmann@28540
  1152
\verb|    else inverse (pow_nat (nat (negate k)) x));|\newline%
haftmann@28540
  1153
\newline%
haftmann@28540
  1154
\verb|example :: Integer;|\newline%
haftmann@28540
  1155
\verb|example = pow_int 10 (-2);|\newline%
haftmann@28540
  1156
\newline%
haftmann@28540
  1157
\verb|}|%
haftmann@22317
  1158
\end{isamarkuptext}%
haftmann@22317
  1159
\isamarkuptrue%
haftmann@28540
  1160
%
haftmann@28565
  1161
\endisatagquote
haftmann@28565
  1162
{\isafoldquote}%
haftmann@28540
  1163
%
haftmann@28565
  1164
\isadelimquote
haftmann@28540
  1165
%
haftmann@28565
  1166
\endisadelimquote
haftmann@28540
  1167
%
haftmann@22317
  1168
\begin{isamarkuptext}%
haftmann@28540
  1169
\noindent The whole code in SML with explicit dictionary passing:%
haftmann@20967
  1170
\end{isamarkuptext}%
haftmann@20967
  1171
\isamarkuptrue%
haftmann@20967
  1172
%
haftmann@28565
  1173
\isadelimquote
haftmann@28540
  1174
%
haftmann@28565
  1175
\endisadelimquote
haftmann@28540
  1176
%
haftmann@28565
  1177
\isatagquote
haftmann@28540
  1178
%
haftmann@28540
  1179
\begin{isamarkuptext}%
haftmann@28540
  1180
\isaverbatim%
haftmann@28540
  1181
\noindent%
haftmann@28540
  1182
\verb|structure Example = |\newline%
haftmann@28540
  1183
\verb|struct|\newline%
haftmann@28540
  1184
\newline%
haftmann@28540
  1185
\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
haftmann@28540
  1186
\newline%
haftmann@28540
  1187
\verb|fun nat_aux i n =|\newline%
haftmann@28540
  1188
\verb|  (if IntInf.<= (i, (0 : IntInf.int)) then n|\newline%
haftmann@28540
  1189
\verb|    else nat_aux (IntInf.- (i, (1 : IntInf.int))) (Suc n));|\newline%
haftmann@28540
  1190
\newline%
haftmann@28540
  1191
\verb|fun nat i = nat_aux i Zero_nat;|\newline%
haftmann@28540
  1192
\newline%
haftmann@28540
  1193
\verb|type 'a semigroup = {mult : 'a -> 'a -> 'a};|\newline%
haftmann@28540
  1194
\verb|fun mult (A_:'a semigroup) = #mult A_;|\newline%
haftmann@28540
  1195
\newline%
haftmann@28540
  1196
\verb|type 'a monoidl =|\newline%
haftmann@28540
  1197
\verb|  {Classes__semigroup_monoidl : 'a semigroup, neutral : 'a};|\newline%
haftmann@28540
  1198
\verb|fun semigroup_monoidl (A_:'a monoidl) = #Classes__semigroup_monoidl A_;|\newline%
haftmann@28540
  1199
\verb|fun neutral (A_:'a monoidl) = #neutral A_;|\newline%
haftmann@28540
  1200
\newline%
haftmann@28540
  1201
\verb|type 'a monoid = {Classes__monoidl_monoid : 'a monoidl};|\newline%
haftmann@28540
  1202
\verb|fun monoidl_monoid (A_:'a monoid) = #Classes__monoidl_monoid A_;|\newline%
haftmann@28540
  1203
\newline%
haftmann@28540
  1204
\verb|type 'a group = {Classes__monoid_group : 'a monoid, inverse : 'a -> 'a};|\newline%
haftmann@28540
  1205
\verb|fun monoid_group (A_:'a group) = #Classes__monoid_group A_;|\newline%
haftmann@28540
  1206
\verb|fun inverse (A_:'a group) = #inverse A_;|\newline%
haftmann@28540
  1207
\newline%
haftmann@28540
  1208
\verb|fun inverse_int i = IntInf.~ i;|\newline%
haftmann@28540
  1209
\newline%
haftmann@28540
  1210
\verb|val neutral_int : IntInf.int = (0 : IntInf.int);|\newline%
haftmann@28540
  1211
\newline%
haftmann@28540
  1212
\verb|fun mult_int i j = IntInf.+ (i, j);|\newline%
haftmann@28540
  1213
\newline%
haftmann@28540
  1214
\verb|val semigroup_int = {mult = mult_int} : IntInf.int semigroup;|\newline%
haftmann@28540
  1215
\newline%
haftmann@28540
  1216
\verb|val monoidl_int =|\newline%
haftmann@28540
  1217
\verb|  {Classes__semigroup_monoidl = semigroup_int, neutral = neutral_int} :|\newline%
haftmann@28540
  1218
\verb|  IntInf.int monoidl;|\newline%
haftmann@28540
  1219
\newline%
haftmann@28540
  1220
\verb|val monoid_int = {Classes__monoidl_monoid = monoidl_int} :|\newline%
haftmann@28540
  1221
\verb|  IntInf.int monoid;|\newline%
haftmann@28540
  1222
\newline%
haftmann@28540
  1223
\verb|val group_int =|\newline%
haftmann@28540
  1224
\verb|  {Classes__monoid_group = monoid_int, inverse = inverse_int} :|\newline%
haftmann@28540
  1225
\verb|  IntInf.int group;|\newline%
haftmann@28540
  1226
\newline%
haftmann@28540
  1227
\verb|fun pow_nat A_ Zero_nat x = neutral (monoidl_monoid A_)|\newline%
haftmann@28540
  1228
\verb|  |\verb,|,\verb| pow_nat A_ (Suc n) x =|\newline%
haftmann@28540
  1229
\verb|    mult ((semigroup_monoidl o monoidl_monoid) A_) x (pow_nat A_ n x);|\newline%
haftmann@28540
  1230
\newline%
haftmann@28540
  1231
\verb|fun pow_int A_ k x =|\newline%
haftmann@28540
  1232
\verb|  (if IntInf.<= ((0 : IntInf.int), k)|\newline%
haftmann@28540
  1233
\verb|    then pow_nat (monoid_group A_) (nat k) x|\newline%
haftmann@28540
  1234
\verb|    else inverse A_ (pow_nat (monoid_group A_) (nat (IntInf.~ k)) x));|\newline%
haftmann@28540
  1235
\newline%
haftmann@28540
  1236
\verb|val example : IntInf.int =|\newline%
haftmann@28540
  1237
\verb|  pow_int group_int (10 : IntInf.int) (~2 : IntInf.int);|\newline%
haftmann@28540
  1238
\newline%
haftmann@28540
  1239
\verb|end; (*struct Example*)|%
haftmann@28540
  1240
\end{isamarkuptext}%
haftmann@28540
  1241
\isamarkuptrue%
haftmann@28540
  1242
%
haftmann@28565
  1243
\endisatagquote
haftmann@28565
  1244
{\isafoldquote}%
haftmann@28540
  1245
%
haftmann@28565
  1246
\isadelimquote
haftmann@28540
  1247
%
haftmann@28565
  1248
\endisadelimquote
haftmann@28540
  1249
%
haftmann@20967
  1250
\isadelimtheory
haftmann@20967
  1251
%
haftmann@20967
  1252
\endisadelimtheory
haftmann@20967
  1253
%
haftmann@20967
  1254
\isatagtheory
haftmann@20967
  1255
\isacommand{end}\isamarkupfalse%
haftmann@20967
  1256
%
haftmann@20967
  1257
\endisatagtheory
haftmann@20967
  1258
{\isafoldtheory}%
haftmann@20967
  1259
%
haftmann@20967
  1260
\isadelimtheory
haftmann@20967
  1261
%
haftmann@20967
  1262
\endisadelimtheory
haftmann@20967
  1263
\isanewline
haftmann@20967
  1264
\end{isabellebody}%
haftmann@20967
  1265
%%% Local Variables:
haftmann@20967
  1266
%%% mode: latex
haftmann@20967
  1267
%%% TeX-master: "root"
haftmann@20967
  1268
%%% End: