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