doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
author wenzelm
Thu, 12 Apr 2007 15:35:29 +0200
changeset 22649 6cf96b9f7b9e
parent 22550 c5039bee2602
child 23015 e67f05cc0ac5
permissions -rw-r--r--
updated;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
     1
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
     2
\begin{isabellebody}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
     3
\def\isabellecontext{Classes}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
     4
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
     5
\isadelimtheory
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
     6
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
     7
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
     8
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
     9
\endisadelimtheory
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    10
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    11
\isatagtheory
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
    12
%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    13
\endisatagtheory
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    14
{\isafoldtheory}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    15
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    16
\isadelimtheory
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    17
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    18
\endisadelimtheory
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    19
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    20
\isadelimML
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    21
%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    22
\endisadelimML
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    23
%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    24
\isatagML
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    25
%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    26
\endisatagML
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    27
{\isafoldML}%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    28
%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    29
\isadelimML
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    30
%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    31
\endisadelimML
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    32
%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    33
\isadelimML
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    34
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    35
\endisadelimML
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    36
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    37
\isatagML
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    38
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    39
\endisatagML
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    40
{\isafoldML}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    41
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    42
\isadelimML
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    43
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    44
\endisadelimML
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    45
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    46
\isamarkupchapter{Haskell-style classes with Isabelle/Isar%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    47
}
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    48
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    49
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    50
\isamarkupsection{Introduction%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    51
}
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    52
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    53
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    54
\begin{isamarkuptext}%
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    55
Type classes were introduces by Wadler and Blott \cite{wadler89how}
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    56
  into the Haskell language, to allow for a reasonable implementation
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    57
  of overloading\footnote{throughout this tutorial, we are referring
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    58
  to classical Haskell 1.0 type classes, not considering
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    59
  later additions in expressiveness}.
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    60
  As a canonical example, a polymorphic equality function
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    61
  \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on different
22550
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
    62
  types for \isa{{\isasymalpha}}, which is achieved by splitting introduction
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    63
  of the \isa{eq} function from its overloaded definitions by means
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    64
  of \isa{class} and \isa{instance} declarations:
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    65
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    66
  \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    67
  \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    68
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    69
  \medskip\noindent\hspace*{2ex}\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    70
  \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    71
  \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    72
  \hspace*{4ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    73
  \hspace*{4ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    74
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    75
  \medskip\noindent\hspace*{2ex}\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
22550
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
    76
  \hspace*{4ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    77
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    78
  \medskip\noindent\hspace*{2ex}\isa{class\ ord\ extends\ eq\ where} \\
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    79
  \hspace*{4ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    80
  \hspace*{4ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    81
22550
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
    82
  \medskip\noindent Type variables are annotated with (finitly many) classes;
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    83
  these annotations are assertions that a particular polymorphic type
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    84
  provides definitions for overloaded functions.
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    85
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    86
  Indeed, type classes not only allow for simple overloading
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    87
  but form a generic calculus, an instance of order-sorted
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    88
  algebra \cite{Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}.
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
    89
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    90
  From a software enigineering point of view, type classes
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    91
  correspond to interfaces in object-oriented languages like Java;
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    92
  so, it is naturally desirable that type classes do not only
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    93
  provide functions (class operations) but also state specifications
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    94
  implementations must obey.  For example, the \isa{class\ eq}
22550
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
    95
  above could be given the following specification, demanding that
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
    96
  \isa{class\ eq} is an equivalence relation obeying reflexivity,
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
    97
  symmetry and transitivity:
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    98
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
    99
  \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where} \\
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   100
  \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   101
  \hspace*{2ex}\isa{satisfying} \\
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   102
  \hspace*{4ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   103
  \hspace*{4ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   104
  \hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   105
22550
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   106
  \medskip\noindent From a theoretic point of view, type classes are leightweight
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   107
  modules; Haskell type classes may be emulated by
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   108
  SML functors \cite{classes_modules}. 
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   109
  Isabelle/Isar offers a discipline of type classes which brings
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   110
  all those aspects together:
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   111
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   112
  \begin{enumerate}
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   113
    \item specifying abstract operations togehter with
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   114
       corresponding specifications,
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   115
    \item instantating those abstract operations by a particular
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   116
       type
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   117
    \item in connection with a ``less ad-hoc'' approach to overloading,
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   118
    \item with a direct link to the Isabelle module system (aka locales).
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   119
  \end{enumerate}
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   120
22550
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   121
  \noindent Isar type classes also directly support code generation
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   122
  in a Haskell like fashion.
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   123
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   124
  This tutorial demonstrates common elements of structured specifications
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   125
  and abstract reasoning with type classes by the algebraic hierarchy of
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   126
  semigroups, monoids and groups.  Our background theory is that of
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   127
  Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, for which some
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   128
  familiarity is assumed.
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   129
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   130
  Here we merely present the look-and-feel for end users.
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   131
  Internally, those are mapped to more primitive Isabelle concepts.
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   132
  See \cite{haftmann_wenzel2006classes} for more detail.%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   133
\end{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   134
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   135
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   136
\isamarkupsection{A simple algebra example \label{sec:example}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   137
}
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   138
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   139
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   140
\isamarkupsubsection{Class definition%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   141
}
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   142
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   143
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   144
\begin{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   145
Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operation \isa{{\isasymcirc}} that is
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   146
  assumed to be associative:%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   147
\end{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   148
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   149
\ \ \ \ \isacommand{class}\isamarkupfalse%
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   150
\ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   151
\ \ \ \ \ \ \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
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   152
\ \ \ \ \ \ \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}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   153
\begin{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   154
\noindent This \isa{{\isasymCLASS}} specification consists of two
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   155
  parts: the \qn{operational} part names the class operation (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   156
  (\isa{{\isasymASSUMES}}).  The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   157
  operation \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   158
  global theorem \isa{semigroup{\isachardot}assoc{\isacharcolon}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   159
\end{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   160
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   161
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   162
\isamarkupsubsection{Class instantiation \label{sec:class_inst}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   163
}
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   164
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   165
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   166
\begin{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   167
The concrete type \isa{int} is made a \isa{semigroup}
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   168
  instance by providing a suitable definition for the class operation
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   169
  \isa{mult} and a proof for the specification of \isa{assoc}.%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   170
\end{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   171
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   172
\ \ \ \ \isacommand{instance}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   173
\ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   174
\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isasymColon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   175
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   176
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   177
\ \ \ \ %
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   178
\endisadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   179
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   180
\isatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   181
\isacommand{proof}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   182
\isanewline
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   183
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   184
\ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   185
\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   186
\ simp\isanewline
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   187
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   188
\ \isacommand{show}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   189
\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   190
\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   191
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   192
\ \ \ \ \isacommand{qed}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   193
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   194
\endisatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   195
{\isafoldproof}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   196
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   197
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   198
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   199
\endisadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   200
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   201
\begin{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   202
\noindent From now on, the type-checker will consider \isa{int}
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   203
  as a \isa{semigroup} automatically, i.e.\ any general results
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   204
  are immediately available on concrete instances.
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   205
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   206
  Note that the first proof step is the \isa{default} method,
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   207
  which for instantiation proofs maps to the \isa{intro{\isacharunderscore}classes} method.
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   208
  This boils down an instantiation judgement to the relevant primitive
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   209
  proof goals and should conveniently always be the first method applied
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   210
  in an instantiation proof.
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   211
22550
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   212
  \medskip Another instance of \isa{semigroup} are the natural numbers:%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   213
\end{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   214
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   215
\ \ \ \ \isacommand{instance}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   216
\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   217
\ \ \ \ \ \ mult{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymequiv}\ m\ {\isacharplus}\ n{\isachardoublequoteclose}\isanewline
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   218
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   219
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   220
\ \ \ \ %
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   221
\endisadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   222
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   223
\isatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   224
\isacommand{proof}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   225
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   226
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   227
\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   228
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   229
\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   230
\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   231
\ simp\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   232
\ \ \ \ \isacommand{qed}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   233
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   234
\endisatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   235
{\isafoldproof}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   236
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   237
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   238
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   239
\endisadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   240
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   241
\begin{isamarkuptext}%
22550
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   242
\noindent Also \isa{list}s form a semigroup with \isa{op\ {\isacharat}} as
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   243
  operation:%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   244
\end{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   245
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   246
\ \ \ \ \isacommand{instance}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   247
\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup\isanewline
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   248
\ \ \ \ \ \ mult{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   249
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   250
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   251
\ \ \ \ %
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   252
\endisadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   253
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   254
\isatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   255
\isacommand{proof}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   256
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   257
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   258
\ xs\ ys\ zs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   259
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   260
\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymotimes}\ zs\ {\isacharequal}\ xs\ {\isasymotimes}\ {\isacharparenleft}ys\ {\isasymotimes}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   261
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   262
\ {\isacharminus}\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   263
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   264
\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   265
\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   266
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   267
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   268
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   269
\ simp\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   270
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   271
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   272
\ \ \ \ \isacommand{qed}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   273
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   274
\endisatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   275
{\isafoldproof}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   276
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   277
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   278
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   279
\endisadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   280
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   281
\isamarkupsubsection{Subclasses%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   282
}
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   283
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   284
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   285
\begin{isamarkuptext}%
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   286
We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral)
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   287
  by extending \isa{semigroup}
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   288
  with one additional operation \isa{neutral} together
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   289
  with its property:%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   290
\end{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   291
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   292
\ \ \ \ \isacommand{class}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   293
\ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   294
\ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}\isactrlloc {\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   295
\ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}\isactrlloc {\isasymone}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   296
\begin{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   297
\noindent Again, we make some instances, by
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   298
  providing suitable operation definitions and proofs for the
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   299
  additional specifications.%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   300
\end{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   301
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   302
\ \ \ \ \isacommand{instance}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   303
\ nat\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   304
\ \ \ \ \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   305
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   306
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   307
\ \ \ \ %
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   308
\endisadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   309
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   310
\isatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   311
\isacommand{proof}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   312
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   313
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   314
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   315
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   316
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   317
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   318
\ simp\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   319
\ \ \ \ \isacommand{qed}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   320
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   321
\endisatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   322
{\isafoldproof}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   323
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   324
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   325
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   326
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   327
\endisadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   328
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   329
\ \ \ \ \isacommand{instance}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   330
\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   331
\ \ \ \ \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   332
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   333
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   334
\ \ \ \ %
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   335
\endisadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   336
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   337
\isatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   338
\isacommand{proof}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   339
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   340
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   341
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   342
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   343
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   344
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   345
\ simp\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   346
\ \ \ \ \isacommand{qed}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   347
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   348
\endisatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   349
{\isafoldproof}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   350
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   351
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   352
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   353
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   354
\endisadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   355
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   356
\ \ \ \ \isacommand{instance}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   357
\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoidl\isanewline
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   358
\ \ \ \ \ \ neutral{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   359
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   360
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   361
\ \ \ \ %
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   362
\endisadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   363
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   364
\isatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   365
\isacommand{proof}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   366
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   367
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   368
\ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   369
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   370
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ xs\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   371
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   372
\ {\isacharminus}\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   373
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   374
\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   375
\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   376
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   377
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   378
\ \isacommand{from}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   379
\ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   380
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   381
\ simp\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   382
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   383
\ \isacommand{show}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   384
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   385
\ simp\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   386
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   387
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   388
\ \ \ \ \isacommand{qed}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   389
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   390
\endisatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   391
{\isafoldproof}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   392
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   393
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   394
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   395
\endisadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   396
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   397
\begin{isamarkuptext}%
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   398
\noindent Fully-fledged monoids are modelled by another subclass
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   399
  which does not add new operations but tightens the specification:%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   400
\end{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   401
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   402
\ \ \ \ \isacommand{class}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   403
\ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   404
\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   405
\begin{isamarkuptext}%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   406
\noindent Instantiations may also be given simultaneously for different
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   407
  type constructors:%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   408
\end{isamarkuptext}%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   409
\isamarkuptrue%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   410
\ \ \ \ \isacommand{instance}\isamarkupfalse%
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   411
\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoid\isanewline
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   412
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   413
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   414
\ \ \ \ %
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   415
\endisadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   416
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   417
\isatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   418
\isacommand{proof}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   419
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   420
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   421
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   422
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   423
\ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   424
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   425
\ simp\isanewline
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   426
\ \ \ \ \isacommand{next}\isamarkupfalse%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   427
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   428
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   429
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   430
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   431
\ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   432
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   433
\ simp\isanewline
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   434
\ \ \ \ \isacommand{next}\isamarkupfalse%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   435
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   436
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   437
\ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   438
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   439
\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   440
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   441
\ {\isacharminus}\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   442
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   443
\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   444
\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   445
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   446
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   447
\ \isacommand{from}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   448
\ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   449
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   450
\ simp\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   451
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   452
\ \isacommand{show}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   453
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   454
\ simp\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   455
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   456
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   457
\ \ \ \ \isacommand{qed}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   458
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   459
\endisatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   460
{\isafoldproof}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   461
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   462
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   463
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   464
\endisadelimproof
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   465
%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   466
\begin{isamarkuptext}%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   467
\noindent To finish our small algebra example, we add a \isa{group} class
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   468
  with a corresponding instance:%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   469
\end{isamarkuptext}%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   470
\isamarkuptrue%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   471
\ \ \ \ \isacommand{class}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   472
\ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   473
\ \ \ \ \ \ \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
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   474
\ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   475
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   476
\ \ \ \ \isacommand{instance}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   477
\ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   478
\ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymequiv}\ {\isacharminus}\ i{\isachardoublequoteclose}\isanewline
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   479
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   480
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   481
\ \ \ \ %
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   482
\endisadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   483
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   484
\isatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   485
\isacommand{proof}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   486
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   487
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   488
\ i\ {\isacharcolon}{\isacharcolon}\ int\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   489
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   490
\ {\isachardoublequoteopen}{\isacharminus}i\ {\isacharplus}\ i\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   491
\ simp\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   492
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   493
\ \isacommand{show}\isamarkupfalse%
22550
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   494
\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   495
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   496
\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ neutral{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   497
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   498
\ \ \ \ \isacommand{qed}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   499
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   500
\endisatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   501
{\isafoldproof}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   502
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   503
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   504
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   505
\endisadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   506
%
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   507
\isamarkupsection{Type classes as locales%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   508
}
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   509
\isamarkuptrue%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   510
%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   511
\isamarkupsubsection{A look behind the scene%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   512
}
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   513
\isamarkuptrue%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   514
%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   515
\begin{isamarkuptext}%
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   516
The example above gives an impression how Isar type classes work
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   517
  in practice.  As stated in the introduction, classes also provide
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   518
  a link to Isar's locale system.  Indeed, the logical core of a class
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   519
  is nothing else than a locale:%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   520
\end{isamarkuptext}%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   521
\isamarkuptrue%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   522
\isacommand{class}\isamarkupfalse%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   523
\ idem\ {\isacharequal}\ type\ {\isacharplus}\isanewline
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   524
\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   525
\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   526
\begin{isamarkuptext}%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   527
\noindent essentially introduces the locale%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   528
\end{isamarkuptext}%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   529
\isamarkuptrue%
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   530
%
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   531
\isadelimML
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   532
%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   533
\endisadelimML
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   534
%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   535
\isatagML
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   536
%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   537
\endisatagML
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   538
{\isafoldML}%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   539
%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   540
\isadelimML
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   541
%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   542
\endisadelimML
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   543
\isacommand{locale}\isamarkupfalse%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   544
\ idem\ {\isacharequal}\isanewline
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   545
\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   546
\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   547
\begin{isamarkuptext}%
22550
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   548
\noindent together with corresponding constant(s):%
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   549
\end{isamarkuptext}%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   550
\isamarkuptrue%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   551
\isacommand{consts}\isamarkupfalse%
22550
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   552
\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   553
\begin{isamarkuptext}%
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   554
\noindent The connection to the type system is done by means
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   555
  of a primitive axclass%
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   556
\end{isamarkuptext}%
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   557
\isamarkuptrue%
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   558
\isacommand{axclass}\isamarkupfalse%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   559
\ idem\ {\isacharless}\ type\isanewline
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   560
\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   561
\begin{isamarkuptext}%
22649
6cf96b9f7b9e updated;
wenzelm
parents: 22550
diff changeset
   562
\noindent together with a corresponding interpretation:%
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   563
\end{isamarkuptext}%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   564
\isamarkuptrue%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   565
\isacommand{interpretation}\isamarkupfalse%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   566
\ idem{\isacharunderscore}class{\isacharcolon}\isanewline
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   567
\ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isacharprime}a{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   568
%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   569
\isadelimproof
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   570
%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   571
\endisadelimproof
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   572
%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   573
\isatagproof
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   574
\isacommand{by}\isamarkupfalse%
22550
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   575
\ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ idem{\isacharparenright}%
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   576
\endisatagproof
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   577
{\isafoldproof}%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   578
%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   579
\isadelimproof
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   580
%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   581
\endisadelimproof
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   582
%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   583
\isadelimML
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   584
%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   585
\endisadelimML
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   586
%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   587
\isatagML
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   588
%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   589
\endisatagML
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   590
{\isafoldML}%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   591
%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   592
\isadelimML
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   593
%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   594
\endisadelimML
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   595
%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   596
\begin{isamarkuptext}%
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   597
This give you at hand the full power of the Isabelle module system;
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   598
  conclusions in locale \isa{idem} are implicitly propagated
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   599
  to class \isa{idem}.%
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   600
\end{isamarkuptext}%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   601
\isamarkuptrue%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   602
%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   603
\isamarkupsubsection{Abstract reasoning%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   604
}
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   605
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   606
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   607
\begin{isamarkuptext}%
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   608
Isabelle locales enable reasoning at a general level, while results
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   609
  are implicitly transferred to all instances.  For example, we can
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   610
  now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   611
  states that the function \isa{{\isacharparenleft}x\ {\isasymcirc}{\isacharparenright}} is injective:%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   612
\end{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   613
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   614
\ \ \ \ \isacommand{lemma}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   615
\ {\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
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   616
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   617
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   618
\ \ \ \ %
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   619
\endisadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   620
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   621
\isatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   622
\isacommand{proof}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   623
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   624
\ \ \ \ \isacommand{assume}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   625
\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   626
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   627
\ \isacommand{have}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   628
\ {\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%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   629
\ simp\isanewline
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   630
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   631
\ \isacommand{have}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   632
\ {\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%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   633
\ assoc\ \isacommand{by}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   634
\ simp\isanewline
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   635
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   636
\ \isacommand{show}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   637
\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   638
\ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   639
\ simp\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   640
\ \ \ \ \isacommand{next}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   641
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   642
\ \ \ \ \isacommand{assume}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   643
\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   644
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   645
\ \isacommand{show}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   646
\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   647
\ simp\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   648
\ \ \ \ \isacommand{qed}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   649
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   650
\endisatagproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   651
{\isafoldproof}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   652
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   653
\isadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   654
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   655
\endisadelimproof
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   656
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   657
\begin{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   658
\noindent Here the \qt{\isa{{\isasymIN}\ group}} target specification
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   659
  indicates that the result is recorded within that context for later
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   660
  use.  This local theorem is also lifted to the global one \isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.  Since type \isa{int} has been made an instance of
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   661
  \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}}.%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   662
\end{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   663
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   664
%
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   665
\isamarkupsection{Further issues%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   666
}
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   667
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   668
%
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   669
\isamarkupsubsection{Code generation%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   670
}
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   671
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   672
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   673
\begin{isamarkuptext}%
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   674
Turning back to the first motivation for type classes,
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   675
  namely overloading, it is obvious that overloading
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   676
  stemming from \isa{{\isasymCLASS}} and \isa{{\isasymINSTANCE}}
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   677
  statements naturally maps to Haskell type classes.
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   678
  The code generator framework \cite{isabelle-codegen} 
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   679
  takes this into account.  Concerning target languages
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   680
  lacking type classes (e.g.~SML), type classes
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   681
  are implemented by explicit dictionary construction.
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   682
  As example, the natural power function on groups:%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   683
\end{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   684
\isamarkuptrue%
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   685
\ \ \ \ \isacommand{fun}\isamarkupfalse%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   686
\isanewline
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   687
\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   688
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   689
\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   690
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   691
\ \ \ \ \isacommand{definition}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   692
\isanewline
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22317
diff changeset
   693
\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   694
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   695
\ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   696
\ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   697
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   698
\ \ \ \ \isacommand{definition}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   699
\isanewline
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   700
\ \ \ \ \ \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   701
\ \ \ \ \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   702
\begin{isamarkuptext}%
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   703
\noindent This maps to Haskell as:%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   704
\end{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   705
\isamarkuptrue%
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   706
\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   707
\ example\ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}{\isacharparenright}%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   708
\begin{isamarkuptext}%
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   709
\lsthaskell{Thy/code_examples/Classes.hs}
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   710
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   711
  \noindent (we have left out all other modules).
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   712
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   713
  \noindent The whole code in SML with explicit dictionary passing:%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   714
\end{isamarkuptext}%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   715
\isamarkuptrue%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   716
\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   717
\ example\ {\isacharparenleft}SML\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   718
\begin{isamarkuptext}%
b550d2c6ca90 continued class tutorial
haftmann
parents: 20967
diff changeset
   719
\lstsml{Thy/code_examples/classes.ML}%
20967
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   720
\end{isamarkuptext}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   721
\isamarkuptrue%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   722
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   723
\isadelimtheory
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   724
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   725
\endisadelimtheory
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   726
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   727
\isatagtheory
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   728
\isacommand{end}\isamarkupfalse%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   729
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   730
\endisatagtheory
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   731
{\isafoldtheory}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   732
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   733
\isadelimtheory
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   734
%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   735
\endisadelimtheory
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   736
\isanewline
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   737
\end{isabellebody}%
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   738
%%% Local Variables:
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   739
%%% mode: latex
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   740
%%% TeX-master: "root"
1df105407f87 added tex files to CVS
haftmann
parents:
diff changeset
   741
%%% End: