doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
author haftmann
Wed Oct 11 08:57:47 2006 +0200 (2006-10-11)
changeset 20967 1df105407f87
child 22317 b550d2c6ca90
permissions -rw-r--r--
added tex files to CVS
haftmann@20967
     1
%
haftmann@20967
     2
\begin{isabellebody}%
haftmann@20967
     3
\def\isabellecontext{Classes}%
haftmann@20967
     4
%
haftmann@20967
     5
\isadelimtheory
haftmann@20967
     6
\isanewline
haftmann@20967
     7
\isanewline
haftmann@20967
     8
\isanewline
haftmann@20967
     9
%
haftmann@20967
    10
\endisadelimtheory
haftmann@20967
    11
%
haftmann@20967
    12
\isatagtheory
haftmann@20967
    13
\isacommand{theory}\isamarkupfalse%
haftmann@20967
    14
\ Classes\isanewline
haftmann@20967
    15
\isakeyword{imports}\ Main\isanewline
haftmann@20967
    16
\isakeyword{begin}\isanewline
haftmann@20967
    17
%
haftmann@20967
    18
\endisatagtheory
haftmann@20967
    19
{\isafoldtheory}%
haftmann@20967
    20
%
haftmann@20967
    21
\isadelimtheory
haftmann@20967
    22
%
haftmann@20967
    23
\endisadelimtheory
haftmann@20967
    24
%
haftmann@20967
    25
\isadelimML
haftmann@20967
    26
%
haftmann@20967
    27
\endisadelimML
haftmann@20967
    28
%
haftmann@20967
    29
\isatagML
haftmann@20967
    30
%
haftmann@20967
    31
\endisatagML
haftmann@20967
    32
{\isafoldML}%
haftmann@20967
    33
%
haftmann@20967
    34
\isadelimML
haftmann@20967
    35
%
haftmann@20967
    36
\endisadelimML
haftmann@20967
    37
%
haftmann@20967
    38
\isamarkupchapter{Haskell-style classes with Isabelle/Isar%
haftmann@20967
    39
}
haftmann@20967
    40
\isamarkuptrue%
haftmann@20967
    41
%
haftmann@20967
    42
\isamarkupsection{Introduction%
haftmann@20967
    43
}
haftmann@20967
    44
\isamarkuptrue%
haftmann@20967
    45
%
haftmann@20967
    46
\begin{isamarkuptext}%
haftmann@20967
    47
The well-known concept of type classes
haftmann@20967
    48
  \cite{wadler89how,peterson93implementing,hall96type,Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}
haftmann@20967
    49
  offers a useful structuring mechanism for programs and proofs, which
haftmann@20967
    50
  is more light-weight than a fully featured module mechanism.  Type
haftmann@20967
    51
  classes are able to qualify types by associating operations and
haftmann@20967
    52
  logical properties.  For example, class \isa{eq} could provide
haftmann@20967
    53
  an equivalence relation \isa{{\isacharequal}} on type \isa{{\isasymalpha}}, and class
haftmann@20967
    54
  \isa{ord} could extend \isa{eq} by providing a strict order
haftmann@20967
    55
  \isa{{\isacharless}} etc.
haftmann@20967
    56
haftmann@20967
    57
  Isabelle/Isar offers Haskell-style type classes, combining operational
haftmann@20967
    58
  and logical specifications.%
haftmann@20967
    59
\end{isamarkuptext}%
haftmann@20967
    60
\isamarkuptrue%
haftmann@20967
    61
%
haftmann@20967
    62
\isamarkupsection{A simple algebra example \label{sec:example}%
haftmann@20967
    63
}
haftmann@20967
    64
\isamarkuptrue%
haftmann@20967
    65
%
haftmann@20967
    66
\begin{isamarkuptext}%
haftmann@20967
    67
We demonstrate common elements of structured specifications and
haftmann@20967
    68
  abstract reasoning with type classes by the algebraic hierarchy of
haftmann@20967
    69
  semigroups, monoids and groups.  Our background theory is that of
haftmann@20967
    70
  Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, which uses fairly
haftmann@20967
    71
  standard notation from mathematics and functional programming.  We
haftmann@20967
    72
  also refer to basic vernacular commands for definitions and
haftmann@20967
    73
  statements, e.g.\ \isa{{\isasymDEFINITION}} and \isa{{\isasymLEMMA}};
haftmann@20967
    74
  proofs will be recorded using structured elements of Isabelle/Isar
haftmann@20967
    75
  \cite{Wenzel-PhD,Nipkow:2002}, notably \isa{{\isasymPROOF}}/\isa{{\isasymQED}} and \isa{{\isasymFIX}}/\isa{{\isasymASSUME}}/\isa{{\isasymSHOW}}.
haftmann@20967
    76
haftmann@20967
    77
  Our main concern are the new \isa{{\isasymCLASS}}
haftmann@20967
    78
  and \isa{{\isasymINSTANCE}} elements used below.
haftmann@20967
    79
  Here we merely present the
haftmann@20967
    80
  look-and-feel for end users, which is quite similar to Haskell's
haftmann@20967
    81
  \texttt{class} and \texttt{instance} \cite{hall96type}, but
haftmann@20967
    82
  augmented by logical specifications and proofs;
haftmann@20967
    83
  Internally, those are mapped to more primitive Isabelle concepts.
haftmann@20967
    84
  See \cite{haftmann_wenzel2006classes} for more detail.%
haftmann@20967
    85
\end{isamarkuptext}%
haftmann@20967
    86
\isamarkuptrue%
haftmann@20967
    87
%
haftmann@20967
    88
\isamarkupsubsection{Class definition%
haftmann@20967
    89
}
haftmann@20967
    90
\isamarkuptrue%
haftmann@20967
    91
%
haftmann@20967
    92
\begin{isamarkuptext}%
haftmann@20967
    93
Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operation \isa{{\isasymcirc}} that is
haftmann@20967
    94
  assumed to be associative:%
haftmann@20967
    95
\end{isamarkuptext}%
haftmann@20967
    96
\isamarkuptrue%
haftmann@20967
    97
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@20967
    98
\ semigroup\ {\isacharequal}\isanewline
haftmann@20967
    99
\ \ \ \ \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}\isactrlloc {\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
haftmann@20967
   100
\ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}y\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
haftmann@20967
   101
\begin{isamarkuptext}%
haftmann@20967
   102
\noindent This \isa{{\isasymCLASS}} specification consists of two
haftmann@20967
   103
  parts: the \qn{operational} part names the class operation (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them
haftmann@20967
   104
  (\isa{{\isasymASSUMES}}).  The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global
haftmann@20967
   105
  operation \isa{{\isachardoublequote}mult\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isacharcolon}{\isacharcolon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
haftmann@20967
   106
  global theorem \isa{semigroup{\isachardot}assoc{\isacharcolon}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isasymalpha}{\isacharcolon}{\isacharcolon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
haftmann@20967
   107
\end{isamarkuptext}%
haftmann@20967
   108
\isamarkuptrue%
haftmann@20967
   109
%
haftmann@20967
   110
\isamarkupsubsection{Class instantiation \label{sec:class_inst}%
haftmann@20967
   111
}
haftmann@20967
   112
\isamarkuptrue%
haftmann@20967
   113
%
haftmann@20967
   114
\begin{isamarkuptext}%
haftmann@20967
   115
The concrete type \isa{int} is made a \isa{semigroup}
haftmann@20967
   116
  instance by providing a suitable definition for the class operation
haftmann@20967
   117
  \isa{mult} and a proof for the specification of \isa{assoc}.%
haftmann@20967
   118
\end{isamarkuptext}%
haftmann@20967
   119
\isamarkuptrue%
haftmann@20967
   120
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   121
\ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
haftmann@20967
   122
\ \ \ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isacharcolon}{\isacharcolon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
haftmann@20967
   123
%
haftmann@20967
   124
\isadelimproof
haftmann@20967
   125
\ \ \ \ %
haftmann@20967
   126
\endisadelimproof
haftmann@20967
   127
%
haftmann@20967
   128
\isatagproof
haftmann@20967
   129
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   130
\isanewline
haftmann@20967
   131
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   132
\ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   133
\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   134
\ simp\isanewline
haftmann@20967
   135
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   136
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   137
\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   138
\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   139
\isanewline
haftmann@20967
   140
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   141
%
haftmann@20967
   142
\endisatagproof
haftmann@20967
   143
{\isafoldproof}%
haftmann@20967
   144
%
haftmann@20967
   145
\isadelimproof
haftmann@20967
   146
%
haftmann@20967
   147
\endisadelimproof
haftmann@20967
   148
%
haftmann@20967
   149
\begin{isamarkuptext}%
haftmann@20967
   150
\noindent From now on, the type-checker will consider \isa{int}
haftmann@20967
   151
  as a \isa{semigroup} automatically, i.e.\ any general results
haftmann@20967
   152
  are immediately available on concrete instances.
haftmann@20967
   153
haftmann@20967
   154
  Another instance of \isa{semigroup} are the natural numbers:%
haftmann@20967
   155
\end{isamarkuptext}%
haftmann@20967
   156
\isamarkuptrue%
haftmann@20967
   157
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   158
\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
haftmann@20967
   159
\ \ \ \ \ \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymequiv}\ m\ {\isacharplus}\ n{\isachardoublequoteclose}\isanewline
haftmann@20967
   160
%
haftmann@20967
   161
\isadelimproof
haftmann@20967
   162
\ \ \ \ %
haftmann@20967
   163
\endisadelimproof
haftmann@20967
   164
%
haftmann@20967
   165
\isatagproof
haftmann@20967
   166
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   167
\isanewline
haftmann@20967
   168
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   169
\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
haftmann@20967
   170
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   171
\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   172
\ semigroup{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   173
\ simp\isanewline
haftmann@20967
   174
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   175
%
haftmann@20967
   176
\endisatagproof
haftmann@20967
   177
{\isafoldproof}%
haftmann@20967
   178
%
haftmann@20967
   179
\isadelimproof
haftmann@20967
   180
%
haftmann@20967
   181
\endisadelimproof
haftmann@20967
   182
%
haftmann@20967
   183
\begin{isamarkuptext}%
haftmann@20967
   184
Also \isa{list}s form a semigroup with \isa{op\ {\isacharat}} as
haftmann@20967
   185
  operation:%
haftmann@20967
   186
\end{isamarkuptext}%
haftmann@20967
   187
\isamarkuptrue%
haftmann@20967
   188
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   189
\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup\isanewline
haftmann@20967
   190
\ \ \ \ \ \ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline
haftmann@20967
   191
%
haftmann@20967
   192
\isadelimproof
haftmann@20967
   193
\ \ \ \ %
haftmann@20967
   194
\endisadelimproof
haftmann@20967
   195
%
haftmann@20967
   196
\isatagproof
haftmann@20967
   197
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   198
\isanewline
haftmann@20967
   199
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   200
\ xs\ ys\ zs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
haftmann@20967
   201
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   202
\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymotimes}\ zs\ {\isacharequal}\ xs\ {\isasymotimes}\ {\isacharparenleft}ys\ {\isasymotimes}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@20967
   203
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
haftmann@20967
   204
\ {\isacharminus}\isanewline
haftmann@20967
   205
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
haftmann@20967
   206
\ semigroup{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   207
\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   208
\isanewline
haftmann@20967
   209
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
haftmann@20967
   210
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   211
\ simp\isanewline
haftmann@20967
   212
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   213
\isanewline
haftmann@20967
   214
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   215
%
haftmann@20967
   216
\endisatagproof
haftmann@20967
   217
{\isafoldproof}%
haftmann@20967
   218
%
haftmann@20967
   219
\isadelimproof
haftmann@20967
   220
%
haftmann@20967
   221
\endisadelimproof
haftmann@20967
   222
%
haftmann@20967
   223
\isamarkupsubsection{Subclasses%
haftmann@20967
   224
}
haftmann@20967
   225
\isamarkuptrue%
haftmann@20967
   226
%
haftmann@20967
   227
\begin{isamarkuptext}%
haftmann@20967
   228
We define a subclass \isa{monoidl} (a semigroup with an left-hand neutral)
haftmann@20967
   229
  by extending \isa{semigroup}
haftmann@20967
   230
  with one additional operation \isa{neutral} together
haftmann@20967
   231
  with its property:%
haftmann@20967
   232
\end{isamarkuptext}%
haftmann@20967
   233
\isamarkuptrue%
haftmann@20967
   234
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@20967
   235
\ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
haftmann@20967
   236
\ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}\isactrlloc {\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
haftmann@20967
   237
\ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}\isactrlloc {\isasymone}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
haftmann@20967
   238
\begin{isamarkuptext}%
haftmann@20967
   239
\noindent Again, we make some instances, by
haftmann@20967
   240
  providing suitable operation definitions and proofs for the
haftmann@20967
   241
  additional specifications.%
haftmann@20967
   242
\end{isamarkuptext}%
haftmann@20967
   243
\isamarkuptrue%
haftmann@20967
   244
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   245
\ nat\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
haftmann@20967
   246
\ \ \ \ \ \ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
haftmann@20967
   247
%
haftmann@20967
   248
\isadelimproof
haftmann@20967
   249
\ \ \ \ %
haftmann@20967
   250
\endisadelimproof
haftmann@20967
   251
%
haftmann@20967
   252
\isatagproof
haftmann@20967
   253
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   254
\isanewline
haftmann@20967
   255
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   256
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
haftmann@20967
   257
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   258
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   259
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   260
\ simp\isanewline
haftmann@20967
   261
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   262
%
haftmann@20967
   263
\endisatagproof
haftmann@20967
   264
{\isafoldproof}%
haftmann@20967
   265
%
haftmann@20967
   266
\isadelimproof
haftmann@20967
   267
\isanewline
haftmann@20967
   268
%
haftmann@20967
   269
\endisadelimproof
haftmann@20967
   270
\isanewline
haftmann@20967
   271
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   272
\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
haftmann@20967
   273
\ \ \ \ \ \ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
haftmann@20967
   274
%
haftmann@20967
   275
\isadelimproof
haftmann@20967
   276
\ \ \ \ %
haftmann@20967
   277
\endisadelimproof
haftmann@20967
   278
%
haftmann@20967
   279
\isatagproof
haftmann@20967
   280
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   281
\isanewline
haftmann@20967
   282
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   283
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
haftmann@20967
   284
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   285
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   286
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   287
\ simp\isanewline
haftmann@20967
   288
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   289
%
haftmann@20967
   290
\endisatagproof
haftmann@20967
   291
{\isafoldproof}%
haftmann@20967
   292
%
haftmann@20967
   293
\isadelimproof
haftmann@20967
   294
\isanewline
haftmann@20967
   295
%
haftmann@20967
   296
\endisadelimproof
haftmann@20967
   297
\isanewline
haftmann@20967
   298
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   299
\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoidl\isanewline
haftmann@20967
   300
\ \ \ \ \ \ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
haftmann@20967
   301
%
haftmann@20967
   302
\isadelimproof
haftmann@20967
   303
\ \ \ \ %
haftmann@20967
   304
\endisadelimproof
haftmann@20967
   305
%
haftmann@20967
   306
\isatagproof
haftmann@20967
   307
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   308
\isanewline
haftmann@20967
   309
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   310
\ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
haftmann@20967
   311
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   312
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ xs\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
haftmann@20967
   313
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
haftmann@20967
   314
\ {\isacharminus}\isanewline
haftmann@20967
   315
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
haftmann@20967
   316
\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   317
\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isacharprime}a\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   318
\isanewline
haftmann@20967
   319
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
haftmann@20967
   320
\ \isacommand{from}\isamarkupfalse%
haftmann@20967
   321
\ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   322
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   323
\ simp\isanewline
haftmann@20967
   324
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
haftmann@20967
   325
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   326
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   327
\ simp\isanewline
haftmann@20967
   328
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   329
\isanewline
haftmann@20967
   330
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   331
%
haftmann@20967
   332
\endisatagproof
haftmann@20967
   333
{\isafoldproof}%
haftmann@20967
   334
%
haftmann@20967
   335
\isadelimproof
haftmann@20967
   336
%
haftmann@20967
   337
\endisadelimproof
haftmann@20967
   338
%
haftmann@20967
   339
\begin{isamarkuptext}%
haftmann@20967
   340
To finish our small algebra example, we add \isa{monoid}
haftmann@20967
   341
  and \isa{group} classes with corresponding instances%
haftmann@20967
   342
\end{isamarkuptext}%
haftmann@20967
   343
\isamarkuptrue%
haftmann@20967
   344
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@20967
   345
\ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
haftmann@20967
   346
\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
haftmann@20967
   347
\isanewline
haftmann@20967
   348
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   349
\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
haftmann@20967
   350
%
haftmann@20967
   351
\isadelimproof
haftmann@20967
   352
\ \ \ \ %
haftmann@20967
   353
\endisadelimproof
haftmann@20967
   354
%
haftmann@20967
   355
\isatagproof
haftmann@20967
   356
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   357
\isanewline
haftmann@20967
   358
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   359
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
haftmann@20967
   360
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   361
\ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   362
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   363
\ simp\isanewline
haftmann@20967
   364
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   365
%
haftmann@20967
   366
\endisatagproof
haftmann@20967
   367
{\isafoldproof}%
haftmann@20967
   368
%
haftmann@20967
   369
\isadelimproof
haftmann@20967
   370
\isanewline
haftmann@20967
   371
%
haftmann@20967
   372
\endisadelimproof
haftmann@20967
   373
\isanewline
haftmann@20967
   374
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   375
\ int\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
haftmann@20967
   376
%
haftmann@20967
   377
\isadelimproof
haftmann@20967
   378
\ \ \ \ %
haftmann@20967
   379
\endisadelimproof
haftmann@20967
   380
%
haftmann@20967
   381
\isatagproof
haftmann@20967
   382
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   383
\isanewline
haftmann@20967
   384
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   385
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
haftmann@20967
   386
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   387
\ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   388
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   389
\ simp\isanewline
haftmann@20967
   390
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   391
%
haftmann@20967
   392
\endisatagproof
haftmann@20967
   393
{\isafoldproof}%
haftmann@20967
   394
%
haftmann@20967
   395
\isadelimproof
haftmann@20967
   396
\isanewline
haftmann@20967
   397
%
haftmann@20967
   398
\endisadelimproof
haftmann@20967
   399
\isanewline
haftmann@20967
   400
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   401
\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoid\isanewline
haftmann@20967
   402
%
haftmann@20967
   403
\isadelimproof
haftmann@20967
   404
\ \ \ \ %
haftmann@20967
   405
\endisadelimproof
haftmann@20967
   406
%
haftmann@20967
   407
\isatagproof
haftmann@20967
   408
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   409
\isanewline
haftmann@20967
   410
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   411
\ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
haftmann@20967
   412
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
haftmann@20967
   413
\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
haftmann@20967
   414
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
haftmann@20967
   415
\ {\isacharminus}\isanewline
haftmann@20967
   416
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
haftmann@20967
   417
\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   418
\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   419
\isanewline
haftmann@20967
   420
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
haftmann@20967
   421
\ \isacommand{from}\isamarkupfalse%
haftmann@20967
   422
\ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   423
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isacharprime}a\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   424
\ simp\isanewline
haftmann@20967
   425
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
haftmann@20967
   426
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   427
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   428
\ simp\isanewline
haftmann@20967
   429
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   430
\isanewline
haftmann@20967
   431
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   432
%
haftmann@20967
   433
\endisatagproof
haftmann@20967
   434
{\isafoldproof}%
haftmann@20967
   435
%
haftmann@20967
   436
\isadelimproof
haftmann@20967
   437
\ \ \isanewline
haftmann@20967
   438
%
haftmann@20967
   439
\endisadelimproof
haftmann@20967
   440
\isanewline
haftmann@20967
   441
\ \ \ \ \isacommand{class}\isamarkupfalse%
haftmann@20967
   442
\ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
haftmann@20967
   443
\ \ \ \ \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}\isactrlloc {\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
haftmann@20967
   444
\ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\isanewline
haftmann@20967
   445
\isanewline
haftmann@20967
   446
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   447
\ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
haftmann@20967
   448
\ \ \ \ \ \ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymequiv}\ {\isacharminus}\ i{\isachardoublequoteclose}\isanewline
haftmann@20967
   449
%
haftmann@20967
   450
\isadelimproof
haftmann@20967
   451
\ \ \ \ %
haftmann@20967
   452
\endisadelimproof
haftmann@20967
   453
%
haftmann@20967
   454
\isatagproof
haftmann@20967
   455
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   456
\isanewline
haftmann@20967
   457
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   458
\ i\ {\isacharcolon}{\isacharcolon}\ int\isanewline
haftmann@20967
   459
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
haftmann@20967
   460
\ {\isachardoublequoteopen}{\isacharminus}i\ {\isacharplus}\ i\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   461
\ simp\isanewline
haftmann@20967
   462
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   463
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   464
\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
haftmann@20967
   465
\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ neutral{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
haftmann@20967
   466
\isanewline
haftmann@20967
   467
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   468
%
haftmann@20967
   469
\endisatagproof
haftmann@20967
   470
{\isafoldproof}%
haftmann@20967
   471
%
haftmann@20967
   472
\isadelimproof
haftmann@20967
   473
%
haftmann@20967
   474
\endisadelimproof
haftmann@20967
   475
%
haftmann@20967
   476
\isamarkupsubsection{Abstract reasoning%
haftmann@20967
   477
}
haftmann@20967
   478
\isamarkuptrue%
haftmann@20967
   479
%
haftmann@20967
   480
\begin{isamarkuptext}%
haftmann@20967
   481
Abstract theories enable reasoning at a general level, while results
haftmann@20967
   482
  are implicitly transferred to all instances.  For example, we can
haftmann@20967
   483
  now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which
haftmann@20967
   484
  states that the function \isa{{\isacharparenleft}x\ {\isasymcirc}{\isacharparenright}} is injective:%
haftmann@20967
   485
\end{isamarkuptext}%
haftmann@20967
   486
\isamarkuptrue%
haftmann@20967
   487
\ \ \ \ \isacommand{lemma}\isamarkupfalse%
haftmann@20967
   488
\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
haftmann@20967
   489
%
haftmann@20967
   490
\isadelimproof
haftmann@20967
   491
\ \ \ \ %
haftmann@20967
   492
\endisadelimproof
haftmann@20967
   493
%
haftmann@20967
   494
\isatagproof
haftmann@20967
   495
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   496
\isanewline
haftmann@20967
   497
\ \ \ \ \isacommand{assume}\isamarkupfalse%
haftmann@20967
   498
\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
haftmann@20967
   499
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   500
\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   501
\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   502
\ simp\isanewline
haftmann@20967
   503
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   504
\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   505
\ {\isachardoublequoteopen}{\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
haftmann@20967
   506
\ assoc\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   507
\ simp\isanewline
haftmann@20967
   508
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   509
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   510
\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
haftmann@20967
   511
\ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   512
\ simp\isanewline
haftmann@20967
   513
\ \ \ \ \isacommand{next}\isamarkupfalse%
haftmann@20967
   514
\isanewline
haftmann@20967
   515
\ \ \ \ \isacommand{assume}\isamarkupfalse%
haftmann@20967
   516
\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
haftmann@20967
   517
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
haftmann@20967
   518
\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   519
\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   520
\ simp\isanewline
haftmann@20967
   521
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   522
%
haftmann@20967
   523
\endisatagproof
haftmann@20967
   524
{\isafoldproof}%
haftmann@20967
   525
%
haftmann@20967
   526
\isadelimproof
haftmann@20967
   527
%
haftmann@20967
   528
\endisadelimproof
haftmann@20967
   529
%
haftmann@20967
   530
\begin{isamarkuptext}%
haftmann@20967
   531
\noindent Here the \qt{\isa{{\isasymIN}\ group}} target specification
haftmann@20967
   532
  indicates that the result is recorded within that context for later
haftmann@20967
   533
  use.  This local theorem is also lifted to the global one \isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isasymalpha}{\isacharcolon}{\isacharcolon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.  Since type \isa{int} has been made an instance of
haftmann@20967
   534
  \isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.%
haftmann@20967
   535
\end{isamarkuptext}%
haftmann@20967
   536
\isamarkuptrue%
haftmann@20967
   537
%
haftmann@20967
   538
\isamarkupsubsection{Additional subclass relations%
haftmann@20967
   539
}
haftmann@20967
   540
\isamarkuptrue%
haftmann@20967
   541
%
haftmann@20967
   542
\begin{isamarkuptext}%
haftmann@20967
   543
Any \isa{group} is also a \isa{monoid};  this
haftmann@20967
   544
  can be made explicit by claiming an additional subclass relation,
haftmann@20967
   545
  together with a proof of the logical difference:%
haftmann@20967
   546
\end{isamarkuptext}%
haftmann@20967
   547
\isamarkuptrue%
haftmann@20967
   548
\ \ \ \ \isacommand{instance}\isamarkupfalse%
haftmann@20967
   549
\ group\ {\isacharless}\ monoid\isanewline
haftmann@20967
   550
%
haftmann@20967
   551
\isadelimproof
haftmann@20967
   552
\ \ \ \ %
haftmann@20967
   553
\endisadelimproof
haftmann@20967
   554
%
haftmann@20967
   555
\isatagproof
haftmann@20967
   556
\isacommand{proof}\isamarkupfalse%
haftmann@20967
   557
\ {\isacharminus}\isanewline
haftmann@20967
   558
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
haftmann@20967
   559
\ x\isanewline
haftmann@20967
   560
\ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
haftmann@20967
   561
\ invl\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   562
\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   563
\ simp\isanewline
haftmann@20967
   564
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
haftmann@20967
   565
\ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
haftmann@20967
   566
\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   567
\ simp\isanewline
haftmann@20967
   568
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
haftmann@20967
   569
\ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse%
haftmann@20967
   570
\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@20967
   571
\ simp\isanewline
haftmann@20967
   572
\ \ \ \ \isacommand{qed}\isamarkupfalse%
haftmann@20967
   573
%
haftmann@20967
   574
\endisatagproof
haftmann@20967
   575
{\isafoldproof}%
haftmann@20967
   576
%
haftmann@20967
   577
\isadelimproof
haftmann@20967
   578
%
haftmann@20967
   579
\endisadelimproof
haftmann@20967
   580
%
haftmann@20967
   581
\isamarkupsection{Code generation%
haftmann@20967
   582
}
haftmann@20967
   583
\isamarkuptrue%
haftmann@20967
   584
%
haftmann@20967
   585
\begin{isamarkuptext}%
haftmann@20967
   586
Code generation takes account of type classes,
haftmann@20967
   587
  resulting either in Haskell type classes or SML dictionaries.
haftmann@20967
   588
  As example, we define the natural power function on groups:%
haftmann@20967
   589
\end{isamarkuptext}%
haftmann@20967
   590
\isamarkuptrue%
haftmann@20967
   591
\ \ \ \ \isacommand{function}\isamarkupfalse%
haftmann@20967
   592
\isanewline
haftmann@20967
   593
\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}monoidl\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}monoidl{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@20967
   594
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
haftmann@20967
   595
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline
haftmann@20967
   596
%
haftmann@20967
   597
\isadelimproof
haftmann@20967
   598
\ \ \ \ \ \ %
haftmann@20967
   599
\endisadelimproof
haftmann@20967
   600
%
haftmann@20967
   601
\isatagproof
haftmann@20967
   602
\isacommand{by}\isamarkupfalse%
haftmann@20967
   603
\ pat{\isacharunderscore}completeness\ auto%
haftmann@20967
   604
\endisatagproof
haftmann@20967
   605
{\isafoldproof}%
haftmann@20967
   606
%
haftmann@20967
   607
\isadelimproof
haftmann@20967
   608
\isanewline
haftmann@20967
   609
%
haftmann@20967
   610
\endisadelimproof
haftmann@20967
   611
\ \ \ \ \isacommand{termination}\isamarkupfalse%
haftmann@20967
   612
\ pow{\isacharunderscore}nat%
haftmann@20967
   613
\isadelimproof
haftmann@20967
   614
\ %
haftmann@20967
   615
\endisadelimproof
haftmann@20967
   616
%
haftmann@20967
   617
\isatagproof
haftmann@20967
   618
\isacommand{by}\isamarkupfalse%
haftmann@20967
   619
\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}measure\ fst{\isachardoublequoteclose}{\isacharparenright}%
haftmann@20967
   620
\endisatagproof
haftmann@20967
   621
{\isafoldproof}%
haftmann@20967
   622
%
haftmann@20967
   623
\isadelimproof
haftmann@20967
   624
%
haftmann@20967
   625
\endisadelimproof
haftmann@20967
   626
\isanewline
haftmann@20967
   627
\ \ \ \ \isacommand{declare}\isamarkupfalse%
haftmann@20967
   628
\ pow{\isacharunderscore}nat{\isachardot}simps\ {\isacharbrackleft}code\ func{\isacharbrackright}\isanewline
haftmann@20967
   629
\isanewline
haftmann@20967
   630
\ \ \ \ \isacommand{definition}\isamarkupfalse%
haftmann@20967
   631
\isanewline
haftmann@20967
   632
\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\isanewline
haftmann@20967
   633
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
haftmann@20967
   634
\ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
haftmann@20967
   635
\ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@20967
   636
\isanewline
haftmann@20967
   637
\ \ \ \ \isacommand{definition}\isamarkupfalse%
haftmann@20967
   638
\isanewline
haftmann@20967
   639
\ \ \ \ \ \ example\ {\isacharcolon}{\isacharcolon}\ int\isanewline
haftmann@20967
   640
\ \ \ \ \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
haftmann@20967
   641
\begin{isamarkuptext}%
haftmann@20967
   642
\noindent Now we generate and compile code for SML:%
haftmann@20967
   643
\end{isamarkuptext}%
haftmann@20967
   644
\isamarkuptrue%
haftmann@20967
   645
\ \ \ \ \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
haftmann@20967
   646
\ example\ {\isacharparenleft}SML\ {\isacharminus}{\isacharparenright}%
haftmann@20967
   647
\begin{isamarkuptext}%
haftmann@20967
   648
\noindent The result is as expected:%
haftmann@20967
   649
\end{isamarkuptext}%
haftmann@20967
   650
\isamarkuptrue%
haftmann@20967
   651
%
haftmann@20967
   652
\isadelimML
haftmann@20967
   653
\ \ \ \ %
haftmann@20967
   654
\endisadelimML
haftmann@20967
   655
%
haftmann@20967
   656
\isatagML
haftmann@20967
   657
\isacommand{ML}\isamarkupfalse%
haftmann@20967
   658
\ {\isacharverbatimopen}\isanewline
haftmann@20967
   659
\ \ \ \ \ \ if\ ROOT{\isachardot}Classes{\isachardot}example\ {\isacharequal}\ {\isachartilde}{\isadigit{2}}{\isadigit{0}}\ then\ {\isacharparenleft}{\isacharparenright}\ else\ error\ {\isachardoublequote}Wrong\ result{\isachardoublequote}\isanewline
haftmann@20967
   660
\ \ \ \ {\isacharverbatimclose}%
haftmann@20967
   661
\endisatagML
haftmann@20967
   662
{\isafoldML}%
haftmann@20967
   663
%
haftmann@20967
   664
\isadelimML
haftmann@20967
   665
%
haftmann@20967
   666
\endisadelimML
haftmann@20967
   667
\isanewline
haftmann@20967
   668
%
haftmann@20967
   669
\isadelimtheory
haftmann@20967
   670
\isanewline
haftmann@20967
   671
%
haftmann@20967
   672
\endisadelimtheory
haftmann@20967
   673
%
haftmann@20967
   674
\isatagtheory
haftmann@20967
   675
\isacommand{end}\isamarkupfalse%
haftmann@20967
   676
%
haftmann@20967
   677
\endisatagtheory
haftmann@20967
   678
{\isafoldtheory}%
haftmann@20967
   679
%
haftmann@20967
   680
\isadelimtheory
haftmann@20967
   681
%
haftmann@20967
   682
\endisadelimtheory
haftmann@20967
   683
\isanewline
haftmann@20967
   684
\end{isabellebody}%
haftmann@20967
   685
%%% Local Variables:
haftmann@20967
   686
%%% mode: latex
haftmann@20967
   687
%%% TeX-master: "root"
haftmann@20967
   688
%%% End: