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