doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
author haftmann
Fri Oct 10 15:52:45 2008 +0200 (2008-10-10)
changeset 28565 519b17118926
parent 28540 541366e3c1b3
child 28566 be2a72b421ae
permissions -rw-r--r--
tuned
     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 \ \ \ \ \isacommand{instantiation}\isamarkupfalse%
   372 \ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
   373 \ \ \ \ \isakeyword{begin}\isanewline
   374 \isanewline
   375 \ \ \ \ \isacommand{definition}\isamarkupfalse%
   376 \isanewline
   377 \ \ \ \ \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
   378 \isanewline
   379 \ \ \ \ \isacommand{definition}\isamarkupfalse%
   380 \isanewline
   381 \ \ \ \ \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
   382 \isanewline
   383 \ \ \ \ \isacommand{instance}\isamarkupfalse%
   384 %
   385 \isadelimproof
   386 \ %
   387 \endisadelimproof
   388 %
   389 \isatagproof
   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 %
   410 \endisatagproof
   411 {\isafoldproof}%
   412 %
   413 \isadelimproof
   414 %
   415 \endisadelimproof
   416 \isanewline
   417 \isanewline
   418 \ \ \ \ \isacommand{end}\isamarkupfalse%
   419 \isanewline
   420 \isanewline
   421 \ \ \ \ \isacommand{instantiation}\isamarkupfalse%
   422 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
   423 \ \ \ \ \isakeyword{begin}\isanewline
   424 \isanewline
   425 \ \ \ \ \isacommand{definition}\isamarkupfalse%
   426 \isanewline
   427 \ \ \ \ \ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   428 \isanewline
   429 \ \ \ \ \isacommand{instance}\isamarkupfalse%
   430 %
   431 \isadelimproof
   432 \ %
   433 \endisadelimproof
   434 %
   435 \isatagproof
   436 \isacommand{proof}\isamarkupfalse%
   437 \isanewline
   438 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
   439 \ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoidl\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline
   440 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
   441 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
   442 \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
   443 \ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
   444 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutl{\isacharparenright}\isanewline
   445 \ \ \ \ \isacommand{qed}\isamarkupfalse%
   446 %
   447 \endisatagproof
   448 {\isafoldproof}%
   449 %
   450 \isadelimproof
   451 %
   452 \endisadelimproof
   453 \isanewline
   454 \isanewline
   455 \ \ \ \isacommand{end}\isamarkupfalse%
   456 %
   457 \begin{isamarkuptext}%
   458 \noindent Fully-fledged monoids are modelled by another subclass
   459   which does not add new parameters but tightens the specification:%
   460 \end{isamarkuptext}%
   461 \isamarkuptrue%
   462 \ \ \ \ \isacommand{class}\isamarkupfalse%
   463 \ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
   464 \ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
   465 \isanewline
   466 \ \ \ \ \isacommand{instantiation}\isamarkupfalse%
   467 \ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline
   468 \ \ \ \ \isakeyword{begin}\isanewline
   469 \isanewline
   470 \ \ \ \ \isacommand{instance}\isamarkupfalse%
   471 %
   472 \isadelimproof
   473 \ %
   474 \endisadelimproof
   475 %
   476 \isatagproof
   477 \isacommand{proof}\isamarkupfalse%
   478 \isanewline
   479 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
   480 \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
   481 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
   482 \ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
   483 \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
   484 \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
   485 \ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
   486 \ \ \ \ \isacommand{next}\isamarkupfalse%
   487 \isanewline
   488 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
   489 \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
   490 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
   491 \ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
   492 \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
   493 \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
   494 \ simp\isanewline
   495 \ \ \ \ \isacommand{qed}\isamarkupfalse%
   496 %
   497 \endisatagproof
   498 {\isafoldproof}%
   499 %
   500 \isadelimproof
   501 %
   502 \endisadelimproof
   503 \isanewline
   504 \isanewline
   505 \ \ \ \ \isacommand{end}\isamarkupfalse%
   506 \isanewline
   507 \isanewline
   508 \ \ \ \ \isacommand{instantiation}\isamarkupfalse%
   509 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
   510 \ \ \ \ \isakeyword{begin}\isanewline
   511 \isanewline
   512 \ \ \ \ \isacommand{instance}\isamarkupfalse%
   513 %
   514 \isadelimproof
   515 \ %
   516 \endisadelimproof
   517 %
   518 \isatagproof
   519 \isacommand{proof}\isamarkupfalse%
   520 \ \isanewline
   521 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
   522 \ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoid\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoid{\isachardoublequoteclose}\isanewline
   523 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
   524 \ {\isachardoublequoteopen}p\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
   525 \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
   526 \ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
   527 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutr{\isacharparenright}\isanewline
   528 \ \ \ \ \isacommand{qed}\isamarkupfalse%
   529 %
   530 \endisatagproof
   531 {\isafoldproof}%
   532 %
   533 \isadelimproof
   534 %
   535 \endisadelimproof
   536 \isanewline
   537 \isanewline
   538 \ \ \ \ \isacommand{end}\isamarkupfalse%
   539 %
   540 \begin{isamarkuptext}%
   541 \noindent To finish our small algebra example, we add a \isa{group} class
   542   with a corresponding instance:%
   543 \end{isamarkuptext}%
   544 \isamarkuptrue%
   545 \ \ \ \ \isacommand{class}\isamarkupfalse%
   546 \ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
   547 \ \ \ \ \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
   548 \ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
   549 \isanewline
   550 \ \ \ \ \isacommand{instantiation}\isamarkupfalse%
   551 \ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
   552 \ \ \ \ \isakeyword{begin}\isanewline
   553 \isanewline
   554 \ \ \ \ \isacommand{definition}\isamarkupfalse%
   555 \isanewline
   556 \ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}i{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
   557 \isanewline
   558 \ \ \ \ \isacommand{instance}\isamarkupfalse%
   559 %
   560 \isadelimproof
   561 \ %
   562 \endisadelimproof
   563 %
   564 \isatagproof
   565 \isacommand{proof}\isamarkupfalse%
   566 \isanewline
   567 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
   568 \ i\ {\isacharcolon}{\isacharcolon}\ int\isanewline
   569 \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
   570 \ {\isachardoublequoteopen}{\isacharminus}i\ {\isacharplus}\ i\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   571 \ simp\isanewline
   572 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
   573 \ \isacommand{show}\isamarkupfalse%
   574 \ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
   575 \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
   576 \ mult{\isacharunderscore}int{\isacharunderscore}def\ neutral{\isacharunderscore}int{\isacharunderscore}def\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
   577 \isanewline
   578 \ \ \ \ \isacommand{qed}\isamarkupfalse%
   579 %
   580 \endisatagproof
   581 {\isafoldproof}%
   582 %
   583 \isadelimproof
   584 %
   585 \endisadelimproof
   586 \isanewline
   587 \isanewline
   588 \ \ \ \ \isacommand{end}\isamarkupfalse%
   589 %
   590 \isamarkupsection{Type classes as locales%
   591 }
   592 \isamarkuptrue%
   593 %
   594 \isamarkupsubsection{A look behind the scene%
   595 }
   596 \isamarkuptrue%
   597 %
   598 \begin{isamarkuptext}%
   599 The example above gives an impression how Isar type classes work
   600   in practice.  As stated in the introduction, classes also provide
   601   a link to Isar's locale system.  Indeed, the logical core of a class
   602   is nothing else than a locale:%
   603 \end{isamarkuptext}%
   604 \isamarkuptrue%
   605 \isacommand{class}\isamarkupfalse%
   606 \ idem\ {\isacharequal}\ type\ {\isacharplus}\isanewline
   607 \ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
   608 \ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
   609 \begin{isamarkuptext}%
   610 \noindent essentially introduces the locale%
   611 \end{isamarkuptext}%
   612 \isamarkuptrue%
   613 %
   614 \isadeliminvisible
   615 %
   616 \endisadeliminvisible
   617 %
   618 \isataginvisible
   619 \isacommand{setup}\isamarkupfalse%
   620 \ {\isacharverbatimopen}\ Sign{\isachardot}add{\isacharunderscore}path\ {\isachardoublequote}foo{\isachardoublequote}\ {\isacharverbatimclose}%
   621 \endisataginvisible
   622 {\isafoldinvisible}%
   623 %
   624 \isadeliminvisible
   625 %
   626 \endisadeliminvisible
   627 \isanewline
   628 \isanewline
   629 \isacommand{locale}\isamarkupfalse%
   630 \ idem\ {\isacharequal}\isanewline
   631 \ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
   632 \ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
   633 \begin{isamarkuptext}%
   634 \noindent together with corresponding constant(s):%
   635 \end{isamarkuptext}%
   636 \isamarkuptrue%
   637 \isacommand{consts}\isamarkupfalse%
   638 \ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
   639 \begin{isamarkuptext}%
   640 \noindent The connection to the type system is done by means
   641   of a primitive axclass%
   642 \end{isamarkuptext}%
   643 \isamarkuptrue%
   644 \isacommand{axclass}\isamarkupfalse%
   645 \ idem\ {\isacharless}\ type\isanewline
   646 \ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
   647 \begin{isamarkuptext}%
   648 \noindent together with a corresponding interpretation:%
   649 \end{isamarkuptext}%
   650 \isamarkuptrue%
   651 \isacommand{interpretation}\isamarkupfalse%
   652 \ idem{\isacharunderscore}class{\isacharcolon}\isanewline
   653 \ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
   654 %
   655 \isadelimproof
   656 %
   657 \endisadelimproof
   658 %
   659 \isatagproof
   660 \isacommand{by}\isamarkupfalse%
   661 \ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ idem{\isacharparenright}%
   662 \endisatagproof
   663 {\isafoldproof}%
   664 %
   665 \isadelimproof
   666 \isanewline
   667 %
   668 \endisadelimproof
   669 %
   670 \isadeliminvisible
   671 \isanewline
   672 %
   673 \endisadeliminvisible
   674 %
   675 \isataginvisible
   676 \isacommand{setup}\isamarkupfalse%
   677 \ {\isacharverbatimopen}\ Sign{\isachardot}parent{\isacharunderscore}path\ {\isacharverbatimclose}%
   678 \endisataginvisible
   679 {\isafoldinvisible}%
   680 %
   681 \isadeliminvisible
   682 %
   683 \endisadeliminvisible
   684 %
   685 \begin{isamarkuptext}%
   686 This give you at hand the full power of the Isabelle module system;
   687   conclusions in locale \isa{idem} are implicitly propagated
   688   to class \isa{idem}.%
   689 \end{isamarkuptext}%
   690 \isamarkuptrue%
   691 %
   692 \isamarkupsubsection{Abstract reasoning%
   693 }
   694 \isamarkuptrue%
   695 %
   696 \begin{isamarkuptext}%
   697 Isabelle locales enable reasoning at a general level, while results
   698   are implicitly transferred to all instances.  For example, we can
   699   now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which
   700   states that the function \isa{{\isacharparenleft}x\ {\isasymotimes}{\isacharparenright}} is injective:%
   701 \end{isamarkuptext}%
   702 \isamarkuptrue%
   703 \ \ \ \ \isacommand{lemma}\isamarkupfalse%
   704 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
   705 %
   706 \isadelimproof
   707 \ \ \ \ %
   708 \endisadelimproof
   709 %
   710 \isatagproof
   711 \isacommand{proof}\isamarkupfalse%
   712 \isanewline
   713 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
   714 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
   715 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
   716 \ \isacommand{have}\isamarkupfalse%
   717 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   718 \ simp\isanewline
   719 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
   720 \ \isacommand{have}\isamarkupfalse%
   721 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
   722 \ assoc\ \isacommand{by}\isamarkupfalse%
   723 \ simp\isanewline
   724 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
   725 \ \isacommand{show}\isamarkupfalse%
   726 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
   727 \ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%
   728 \ simp\isanewline
   729 \ \ \ \ \isacommand{next}\isamarkupfalse%
   730 \isanewline
   731 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
   732 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
   733 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
   734 \ \isacommand{show}\isamarkupfalse%
   735 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   736 \ simp\isanewline
   737 \ \ \ \ \isacommand{qed}\isamarkupfalse%
   738 %
   739 \endisatagproof
   740 {\isafoldproof}%
   741 %
   742 \isadelimproof
   743 %
   744 \endisadelimproof
   745 %
   746 \begin{isamarkuptext}%
   747 \noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target specification
   748   indicates that the result is recorded within that context for later
   749   use.  This local theorem is also lifted to the global one \hyperlink{fact.group.left-cancel:}{\mbox{\isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}}}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.  Since type \isa{int} has been made an instance of
   750   \isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.%
   751 \end{isamarkuptext}%
   752 \isamarkuptrue%
   753 %
   754 \isamarkupsubsection{Derived definitions%
   755 }
   756 \isamarkuptrue%
   757 %
   758 \begin{isamarkuptext}%
   759 Isabelle locales support a concept of local definitions
   760   in locales:%
   761 \end{isamarkuptext}%
   762 \isamarkuptrue%
   763 \ \ \ \ \isacommand{primrec}\isamarkupfalse%
   764 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   765 \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
   766 \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}%
   767 \begin{isamarkuptext}%
   768 \noindent If the locale \isa{group} is also a class, this local
   769   definition is propagated onto a global definition of
   770   \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}}
   771   with corresponding theorems
   772 
   773   \isa{pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}\isasep\isanewline%
   774 pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x}.
   775 
   776   \noindent As you can see from this example, for local
   777   definitions you may use any specification tool
   778   which works together with locales (e.g. \cite{krauss2006}).%
   779 \end{isamarkuptext}%
   780 \isamarkuptrue%
   781 %
   782 \isamarkupsubsection{A functor analogy%
   783 }
   784 \isamarkuptrue%
   785 %
   786 \begin{isamarkuptext}%
   787 We introduced Isar classes by analogy to type classes
   788   functional programming;  if we reconsider this in the
   789   context of what has been said about type classes and locales,
   790   we can drive this analogy further by stating that type
   791   classes essentially correspond to functors which have
   792   a canonical interpretation as type classes.
   793   Anyway, there is also the possibility of other interpretations.
   794   For example, also \isa{list}s form a monoid with
   795   \isa{append} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
   796   seems inappropriate to apply to lists
   797   the same operations as for genuinely algebraic types.
   798   In such a case, we simply can do a particular interpretation
   799   of monoids for lists:%
   800 \end{isamarkuptext}%
   801 \isamarkuptrue%
   802 \ \ \ \ \isacommand{interpretation}\isamarkupfalse%
   803 \ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
   804 %
   805 \isadelimproof
   806 \ \ \ \ \ \ %
   807 \endisadelimproof
   808 %
   809 \isatagproof
   810 \isacommand{by}\isamarkupfalse%
   811 \ unfold{\isacharunderscore}locales\ auto%
   812 \endisatagproof
   813 {\isafoldproof}%
   814 %
   815 \isadelimproof
   816 %
   817 \endisadelimproof
   818 %
   819 \begin{isamarkuptext}%
   820 \noindent This enables us to apply facts on monoids
   821   to lists, e.g. \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ x\ {\isacharequal}\ x}.
   822 
   823   When using this interpretation pattern, it may also
   824   be appropriate to map derived definitions accordingly:%
   825 \end{isamarkuptext}%
   826 \isamarkuptrue%
   827 \ \ \ \ \isacommand{fun}\isamarkupfalse%
   828 \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   829 \ \ \ \ \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
   830 \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
   831 \isanewline
   832 \ \ \ \ \isacommand{interpretation}\isamarkupfalse%
   833 \ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline
   834 \ \ \ \ \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
   835 %
   836 \isadelimproof
   837 \ \ \ \ %
   838 \endisadelimproof
   839 %
   840 \isatagproof
   841 \isacommand{proof}\isamarkupfalse%
   842 \ {\isacharminus}\isanewline
   843 \ \ \ \ \ \ \isacommand{interpret}\isamarkupfalse%
   844 \ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
   845 \isanewline
   846 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
   847 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
   848 \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
   849 \isanewline
   850 \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
   851 \ n\isanewline
   852 \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
   853 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
   854 \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
   855 \ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline
   856 \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
   857 \isanewline
   858 \ \ \ \ \isacommand{qed}\isamarkupfalse%
   859 \ intro{\isacharunderscore}locales%
   860 \endisatagproof
   861 {\isafoldproof}%
   862 %
   863 \isadelimproof
   864 %
   865 \endisadelimproof
   866 %
   867 \isamarkupsubsection{Additional subclass relations%
   868 }
   869 \isamarkuptrue%
   870 %
   871 \begin{isamarkuptext}%
   872 Any \isa{group} is also a \isa{monoid};  this
   873   can be made explicit by claiming an additional
   874   subclass relation,
   875   together with a proof of the logical difference:%
   876 \end{isamarkuptext}%
   877 \isamarkuptrue%
   878 \ \ \ \ \isacommand{subclass}\isamarkupfalse%
   879 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ monoid\isanewline
   880 %
   881 \isadelimproof
   882 \ \ \ \ %
   883 \endisadelimproof
   884 %
   885 \isatagproof
   886 \isacommand{proof}\isamarkupfalse%
   887 \ unfold{\isacharunderscore}locales\isanewline
   888 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
   889 \ x\isanewline
   890 \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
   891 \ invl\ \isacommand{have}\isamarkupfalse%
   892 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   893 \ simp\isanewline
   894 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
   895 \ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
   896 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ {\isasymone}{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   897 \ simp\isanewline
   898 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
   899 \ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse%
   900 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   901 \ simp\isanewline
   902 \ \ \ \ \isacommand{qed}\isamarkupfalse%
   903 %
   904 \endisatagproof
   905 {\isafoldproof}%
   906 %
   907 \isadelimproof
   908 %
   909 \endisadelimproof
   910 %
   911 \begin{isamarkuptext}%
   912 \noindent The logical proof is carried out on the locale level
   913   and thus conveniently is opened using the \isa{unfold{\isacharunderscore}locales}
   914   method which only leaves the logical differences still
   915   open to proof to the user.  Afterwards it is propagated
   916   to the type system, making \isa{group} an instance of
   917   \isa{monoid} by adding an additional edge
   918   to the graph of subclass relations
   919   (cf.\ \figref{fig:subclass}).
   920 
   921   \begin{figure}[htbp]
   922    \begin{center}
   923      \small
   924      \unitlength 0.6mm
   925      \begin{picture}(40,60)(0,0)
   926        \put(20,60){\makebox(0,0){\isa{semigroup}}}
   927        \put(20,40){\makebox(0,0){\isa{monoidl}}}
   928        \put(00,20){\makebox(0,0){\isa{monoid}}}
   929        \put(40,00){\makebox(0,0){\isa{group}}}
   930        \put(20,55){\vector(0,-1){10}}
   931        \put(15,35){\vector(-1,-1){10}}
   932        \put(25,35){\vector(1,-3){10}}
   933      \end{picture}
   934      \hspace{8em}
   935      \begin{picture}(40,60)(0,0)
   936        \put(20,60){\makebox(0,0){\isa{semigroup}}}
   937        \put(20,40){\makebox(0,0){\isa{monoidl}}}
   938        \put(00,20){\makebox(0,0){\isa{monoid}}}
   939        \put(40,00){\makebox(0,0){\isa{group}}}
   940        \put(20,55){\vector(0,-1){10}}
   941        \put(15,35){\vector(-1,-1){10}}
   942        \put(05,15){\vector(3,-1){30}}
   943      \end{picture}
   944      \caption{Subclass relationship of monoids and groups:
   945         before and after establishing the relationship
   946         \isa{group\ {\isasymsubseteq}\ monoid};  transitive edges left out.}
   947      \label{fig:subclass}
   948    \end{center}
   949   \end{figure}
   950 
   951   For illustration, a derived definition
   952   in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
   953 \end{isamarkuptext}%
   954 \isamarkuptrue%
   955 %
   956 \isadelimquote
   957 %
   958 \endisadelimquote
   959 %
   960 \isatagquote
   961 \isacommand{definition}\isamarkupfalse%
   962 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   963 \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
   964 \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
   965 \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
   966 \endisatagquote
   967 {\isafoldquote}%
   968 %
   969 \isadelimquote
   970 %
   971 \endisadelimquote
   972 %
   973 \begin{isamarkuptext}%
   974 \noindent yields the global definition of
   975   \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
   976   with the corresponding theorem \isa{pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{0}}\ {\isasymle}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}}.%
   977 \end{isamarkuptext}%
   978 \isamarkuptrue%
   979 %
   980 \isamarkupsubsection{A note on syntax%
   981 }
   982 \isamarkuptrue%
   983 %
   984 \begin{isamarkuptext}%
   985 As a commodity, class context syntax allows to refer
   986   to local class operations and their global counterparts
   987   uniformly;  type inference resolves ambiguities.  For example:%
   988 \end{isamarkuptext}%
   989 \isamarkuptrue%
   990 %
   991 \isadelimquote
   992 %
   993 \endisadelimquote
   994 %
   995 \isatagquote
   996 \isacommand{context}\isamarkupfalse%
   997 \ semigroup\isanewline
   998 \isakeyword{begin}\isanewline
   999 \isanewline
  1000 \isacommand{term}\isamarkupfalse%
  1001 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
  1002 \isamarkupcmt{example 1%
  1003 }
  1004 \isanewline
  1005 \isacommand{term}\isamarkupfalse%
  1006 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
  1007 \isamarkupcmt{example 2%
  1008 }
  1009 %
  1010 \endisatagquote
  1011 {\isafoldquote}%
  1012 %
  1013 \isadelimquote
  1014 %
  1015 \endisadelimquote
  1016 \isanewline
  1017 \isanewline
  1018 \isacommand{end}\isamarkupfalse%
  1019 \isanewline
  1020 %
  1021 \isadelimquote
  1022 \isanewline
  1023 %
  1024 \endisadelimquote
  1025 %
  1026 \isatagquote
  1027 \isacommand{term}\isamarkupfalse%
  1028 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
  1029 \isamarkupcmt{example 3%
  1030 }
  1031 %
  1032 \endisatagquote
  1033 {\isafoldquote}%
  1034 %
  1035 \isadelimquote
  1036 %
  1037 \endisadelimquote
  1038 %
  1039 \begin{isamarkuptext}%
  1040 \noindent Here in example 1, the term refers to the local class operation
  1041   \isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type constraint
  1042   enforces the global class operation \isa{mult\ {\isacharbrackleft}nat{\isacharbrackright}}.
  1043   In the global context in example 3, the reference is
  1044   to the polymorphic global class operation \isa{mult\ {\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isasymColon}\ semigroup{\isacharbrackright}}.%
  1045 \end{isamarkuptext}%
  1046 \isamarkuptrue%
  1047 %
  1048 \isamarkupsection{Type classes and code generation%
  1049 }
  1050 \isamarkuptrue%
  1051 %
  1052 \begin{isamarkuptext}%
  1053 Turning back to the first motivation for type classes,
  1054   namely overloading, it is obvious that overloading
  1055   stemming from \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} statements and
  1056   \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
  1057   targets naturally maps to Haskell type classes.
  1058   The code generator framework \cite{isabelle-codegen} 
  1059   takes this into account.  Concerning target languages
  1060   lacking type classes (e.g.~SML), type classes
  1061   are implemented by explicit dictionary construction.
  1062   As example, let's go back to the power function:%
  1063 \end{isamarkuptext}%
  1064 \isamarkuptrue%
  1065 %
  1066 \isadelimquote
  1067 %
  1068 \endisadelimquote
  1069 %
  1070 \isatagquote
  1071 \isacommand{definition}\isamarkupfalse%
  1072 \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
  1073 \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
  1074 \endisatagquote
  1075 {\isafoldquote}%
  1076 %
  1077 \isadelimquote
  1078 %
  1079 \endisadelimquote
  1080 %
  1081 \begin{isamarkuptext}%
  1082 \noindent This maps to Haskell as:%
  1083 \end{isamarkuptext}%
  1084 \isamarkuptrue%
  1085 %
  1086 \isadelimquote
  1087 %
  1088 \endisadelimquote
  1089 %
  1090 \isatagquote
  1091 %
  1092 \begin{isamarkuptext}%
  1093 \isaverbatim%
  1094 \noindent%
  1095 \verb|module Example where {|\newline%
  1096 \newline%
  1097 \newline%
  1098 \verb|data Nat = Suc Nat |\verb,|,\verb| Zero_nat;|\newline%
  1099 \newline%
  1100 \verb|nat_aux :: Integer -> Nat -> Nat;|\newline%
  1101 \verb|nat_aux i n = (if i <= 0 then n else nat_aux (i - 1) (Suc n));|\newline%
  1102 \newline%
  1103 \verb|nat :: Integer -> Nat;|\newline%
  1104 \verb|nat i = nat_aux i Zero_nat;|\newline%
  1105 \newline%
  1106 \verb|class Semigroup a where {|\newline%
  1107 \verb|  mult :: a -> a -> a;|\newline%
  1108 \verb|};|\newline%
  1109 \newline%
  1110 \verb|class (Semigroup a) => Monoidl a where {|\newline%
  1111 \verb|  neutral :: a;|\newline%
  1112 \verb|};|\newline%
  1113 \newline%
  1114 \verb|class (Monoidl a) => Monoid a where {|\newline%
  1115 \verb|};|\newline%
  1116 \newline%
  1117 \verb|class (Monoid a) => Group a where {|\newline%
  1118 \verb|  inverse :: a -> a;|\newline%
  1119 \verb|};|\newline%
  1120 \newline%
  1121 \verb|inverse_int :: Integer -> Integer;|\newline%
  1122 \verb|inverse_int i = negate i;|\newline%
  1123 \newline%
  1124 \verb|neutral_int :: Integer;|\newline%
  1125 \verb|neutral_int = 0;|\newline%
  1126 \newline%
  1127 \verb|mult_int :: Integer -> Integer -> Integer;|\newline%
  1128 \verb|mult_int i j = i + j;|\newline%
  1129 \newline%
  1130 \verb|instance Semigroup Integer where {|\newline%
  1131 \verb|  mult = mult_int;|\newline%
  1132 \verb|};|\newline%
  1133 \newline%
  1134 \verb|instance Monoidl Integer where {|\newline%
  1135 \verb|  neutral = neutral_int;|\newline%
  1136 \verb|};|\newline%
  1137 \newline%
  1138 \verb|instance Monoid Integer where {|\newline%
  1139 \verb|};|\newline%
  1140 \newline%
  1141 \verb|instance Group Integer where {|\newline%
  1142 \verb|  inverse = inverse_int;|\newline%
  1143 \verb|};|\newline%
  1144 \newline%
  1145 \verb|pow_nat :: forall a. (Monoid a) => Nat -> a -> a;|\newline%
  1146 \verb|pow_nat Zero_nat x = neutral;|\newline%
  1147 \verb|pow_nat (Suc n) x = mult x (pow_nat n x);|\newline%
  1148 \newline%
  1149 \verb|pow_int :: forall a. (Group a) => Integer -> a -> a;|\newline%
  1150 \verb|pow_int k x =|\newline%
  1151 \verb|  (if 0 <= k then pow_nat (nat k) x|\newline%
  1152 \verb|    else inverse (pow_nat (nat (negate k)) x));|\newline%
  1153 \newline%
  1154 \verb|example :: Integer;|\newline%
  1155 \verb|example = pow_int 10 (-2);|\newline%
  1156 \newline%
  1157 \verb|}|%
  1158 \end{isamarkuptext}%
  1159 \isamarkuptrue%
  1160 %
  1161 \endisatagquote
  1162 {\isafoldquote}%
  1163 %
  1164 \isadelimquote
  1165 %
  1166 \endisadelimquote
  1167 %
  1168 \begin{isamarkuptext}%
  1169 \noindent The whole code in SML with explicit dictionary passing:%
  1170 \end{isamarkuptext}%
  1171 \isamarkuptrue%
  1172 %
  1173 \isadelimquote
  1174 %
  1175 \endisadelimquote
  1176 %
  1177 \isatagquote
  1178 %
  1179 \begin{isamarkuptext}%
  1180 \isaverbatim%
  1181 \noindent%
  1182 \verb|structure Example = |\newline%
  1183 \verb|struct|\newline%
  1184 \newline%
  1185 \verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
  1186 \newline%
  1187 \verb|fun nat_aux i n =|\newline%
  1188 \verb|  (if IntInf.<= (i, (0 : IntInf.int)) then n|\newline%
  1189 \verb|    else nat_aux (IntInf.- (i, (1 : IntInf.int))) (Suc n));|\newline%
  1190 \newline%
  1191 \verb|fun nat i = nat_aux i Zero_nat;|\newline%
  1192 \newline%
  1193 \verb|type 'a semigroup = {mult : 'a -> 'a -> 'a};|\newline%
  1194 \verb|fun mult (A_:'a semigroup) = #mult A_;|\newline%
  1195 \newline%
  1196 \verb|type 'a monoidl =|\newline%
  1197 \verb|  {Classes__semigroup_monoidl : 'a semigroup, neutral : 'a};|\newline%
  1198 \verb|fun semigroup_monoidl (A_:'a monoidl) = #Classes__semigroup_monoidl A_;|\newline%
  1199 \verb|fun neutral (A_:'a monoidl) = #neutral A_;|\newline%
  1200 \newline%
  1201 \verb|type 'a monoid = {Classes__monoidl_monoid : 'a monoidl};|\newline%
  1202 \verb|fun monoidl_monoid (A_:'a monoid) = #Classes__monoidl_monoid A_;|\newline%
  1203 \newline%
  1204 \verb|type 'a group = {Classes__monoid_group : 'a monoid, inverse : 'a -> 'a};|\newline%
  1205 \verb|fun monoid_group (A_:'a group) = #Classes__monoid_group A_;|\newline%
  1206 \verb|fun inverse (A_:'a group) = #inverse A_;|\newline%
  1207 \newline%
  1208 \verb|fun inverse_int i = IntInf.~ i;|\newline%
  1209 \newline%
  1210 \verb|val neutral_int : IntInf.int = (0 : IntInf.int);|\newline%
  1211 \newline%
  1212 \verb|fun mult_int i j = IntInf.+ (i, j);|\newline%
  1213 \newline%
  1214 \verb|val semigroup_int = {mult = mult_int} : IntInf.int semigroup;|\newline%
  1215 \newline%
  1216 \verb|val monoidl_int =|\newline%
  1217 \verb|  {Classes__semigroup_monoidl = semigroup_int, neutral = neutral_int} :|\newline%
  1218 \verb|  IntInf.int monoidl;|\newline%
  1219 \newline%
  1220 \verb|val monoid_int = {Classes__monoidl_monoid = monoidl_int} :|\newline%
  1221 \verb|  IntInf.int monoid;|\newline%
  1222 \newline%
  1223 \verb|val group_int =|\newline%
  1224 \verb|  {Classes__monoid_group = monoid_int, inverse = inverse_int} :|\newline%
  1225 \verb|  IntInf.int group;|\newline%
  1226 \newline%
  1227 \verb|fun pow_nat A_ Zero_nat x = neutral (monoidl_monoid A_)|\newline%
  1228 \verb|  |\verb,|,\verb| pow_nat A_ (Suc n) x =|\newline%
  1229 \verb|    mult ((semigroup_monoidl o monoidl_monoid) A_) x (pow_nat A_ n x);|\newline%
  1230 \newline%
  1231 \verb|fun pow_int A_ k x =|\newline%
  1232 \verb|  (if IntInf.<= ((0 : IntInf.int), k)|\newline%
  1233 \verb|    then pow_nat (monoid_group A_) (nat k) x|\newline%
  1234 \verb|    else inverse A_ (pow_nat (monoid_group A_) (nat (IntInf.~ k)) x));|\newline%
  1235 \newline%
  1236 \verb|val example : IntInf.int =|\newline%
  1237 \verb|  pow_int group_int (10 : IntInf.int) (~2 : IntInf.int);|\newline%
  1238 \newline%
  1239 \verb|end; (*struct Example*)|%
  1240 \end{isamarkuptext}%
  1241 \isamarkuptrue%
  1242 %
  1243 \endisatagquote
  1244 {\isafoldquote}%
  1245 %
  1246 \isadelimquote
  1247 %
  1248 \endisadelimquote
  1249 %
  1250 \isadelimtheory
  1251 %
  1252 \endisadelimtheory
  1253 %
  1254 \isatagtheory
  1255 \isacommand{end}\isamarkupfalse%
  1256 %
  1257 \endisatagtheory
  1258 {\isafoldtheory}%
  1259 %
  1260 \isadelimtheory
  1261 %
  1262 \endisadelimtheory
  1263 \isanewline
  1264 \end{isabellebody}%
  1265 %%% Local Variables:
  1266 %%% mode: latex
  1267 %%% TeX-master: "root"
  1268 %%% End: