1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Classes}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 \isacommand{theory}\isamarkupfalse% |
|
11 \ Classes\isanewline |
|
12 \isakeyword{imports}\ Main\ Setup\isanewline |
|
13 \isakeyword{begin}% |
|
14 \endisatagtheory |
|
15 {\isafoldtheory}% |
|
16 % |
|
17 \isadelimtheory |
|
18 % |
|
19 \endisadelimtheory |
|
20 % |
|
21 \isamarkupsection{Introduction% |
|
22 } |
|
23 \isamarkuptrue% |
|
24 % |
|
25 \begin{isamarkuptext}% |
|
26 Type classes were introduced by Wadler and Blott \cite{wadler89how} |
|
27 into the Haskell language to allow for a reasonable implementation |
|
28 of overloading\footnote{throughout this tutorial, we are referring |
|
29 to classical Haskell 1.0 type classes, not considering later |
|
30 additions in expressiveness}. As a canonical example, a polymorphic |
|
31 equality function \isa{eq\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} which is overloaded on |
|
32 different types for \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}, which is achieved by splitting |
|
33 introduction of the \isa{eq} function from its overloaded |
|
34 definitions by means of \isa{class} and \isa{instance} |
|
35 declarations: \footnote{syntax here is a kind of isabellized |
|
36 Haskell} |
|
37 |
|
38 \begin{quote} |
|
39 |
|
40 \noindent\isa{class\ eq\ where} \\ |
|
41 \hspace*{2ex}\isa{eq\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} |
|
42 |
|
43 \medskip\noindent\isa{instance\ nat\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ eq\ where} \\ |
|
44 \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ True} \\ |
|
45 \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ False} \\ |
|
46 \hspace*{2ex}\isa{eq\ {\isaliteral{5F}{\isacharunderscore}}\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ False} \\ |
|
47 \hspace*{2ex}\isa{eq\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ eq\ n\ m} |
|
48 |
|
49 \medskip\noindent\isa{instance\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}eq{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}eq{\isaliteral{29}{\isacharparenright}}\ pair\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ eq\ where} \\ |
|
50 \hspace*{2ex}\isa{eq\ {\isaliteral{28}{\isacharparenleft}}x{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ y{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}x{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ y{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}} |
|
51 |
|
52 \medskip\noindent\isa{class\ ord\ extends\ eq\ where} \\ |
|
53 \hspace*{2ex}\isa{less{\isaliteral{5F}{\isacharunderscore}}eq\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} \\ |
|
54 \hspace*{2ex}\isa{less\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} |
|
55 |
|
56 \end{quote} |
|
57 |
|
58 \noindent Type variables are annotated with (finitely many) classes; |
|
59 these annotations are assertions that a particular polymorphic type |
|
60 provides definitions for overloaded functions. |
|
61 |
|
62 Indeed, type classes not only allow for simple overloading but form |
|
63 a generic calculus, an instance of order-sorted algebra |
|
64 \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}. |
|
65 |
|
66 From a software engineering point of view, type classes roughly |
|
67 correspond to interfaces in object-oriented languages like Java; so, |
|
68 it is naturally desirable that type classes do not only provide |
|
69 functions (class parameters) but also state specifications |
|
70 implementations must obey. For example, the \isa{class\ eq} |
|
71 above could be given the following specification, demanding that |
|
72 \isa{class\ eq} is an equivalence relation obeying reflexivity, |
|
73 symmetry and transitivity: |
|
74 |
|
75 \begin{quote} |
|
76 |
|
77 \noindent\isa{class\ eq\ where} \\ |
|
78 \hspace*{2ex}\isa{eq\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} \\ |
|
79 \isa{satisfying} \\ |
|
80 \hspace*{2ex}\isa{refl{\isaliteral{3A}{\isacharcolon}}\ eq\ x\ x} \\ |
|
81 \hspace*{2ex}\isa{sym{\isaliteral{3A}{\isacharcolon}}\ eq\ x\ y\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ eq\ x\ y} \\ |
|
82 \hspace*{2ex}\isa{trans{\isaliteral{3A}{\isacharcolon}}\ eq\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ eq\ y\ z\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ eq\ x\ z} |
|
83 |
|
84 \end{quote} |
|
85 |
|
86 \noindent From a theoretical point of view, type classes are |
|
87 lightweight modules; Haskell type classes may be emulated by SML |
|
88 functors \cite{classes_modules}. Isabelle/Isar offers a discipline |
|
89 of type classes which brings all those aspects together: |
|
90 |
|
91 \begin{enumerate} |
|
92 \item specifying abstract parameters together with |
|
93 corresponding specifications, |
|
94 \item instantiating those abstract parameters by a particular |
|
95 type |
|
96 \item in connection with a ``less ad-hoc'' approach to overloading, |
|
97 \item with a direct link to the Isabelle module system: |
|
98 locales \cite{kammueller-locales}. |
|
99 \end{enumerate} |
|
100 |
|
101 \noindent Isar type classes also directly support code generation in |
|
102 a Haskell like fashion. Internally, they are mapped to more |
|
103 primitive Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}. |
|
104 |
|
105 This tutorial demonstrates common elements of structured |
|
106 specifications and abstract reasoning with type classes by the |
|
107 algebraic hierarchy of semigroups, monoids and groups. Our |
|
108 background theory is that of Isabelle/HOL \cite{isa-tutorial}, for |
|
109 which some familiarity is assumed.% |
|
110 \end{isamarkuptext}% |
|
111 \isamarkuptrue% |
|
112 % |
|
113 \isamarkupsection{A simple algebra example \label{sec:example}% |
|
114 } |
|
115 \isamarkuptrue% |
|
116 % |
|
117 \isamarkupsubsection{Class definition% |
|
118 } |
|
119 \isamarkuptrue% |
|
120 % |
|
121 \begin{isamarkuptext}% |
|
122 Depending on an arbitrary type \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}, class \isa{semigroup} introduces a binary operator \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}{\isaliteral{29}{\isacharparenright}}} that is |
|
123 assumed to be associative:% |
|
124 \end{isamarkuptext}% |
|
125 \isamarkuptrue% |
|
126 % |
|
127 \isadelimquote |
|
128 % |
|
129 \endisadelimquote |
|
130 % |
|
131 \isatagquote |
|
132 \isacommand{class}\isamarkupfalse% |
|
133 \ semigroup\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
134 \ \ \isakeyword{fixes}\ mult\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{7}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
135 \ \ \isakeyword{assumes}\ assoc{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
136 \endisatagquote |
|
137 {\isafoldquote}% |
|
138 % |
|
139 \isadelimquote |
|
140 % |
|
141 \endisadelimquote |
|
142 % |
|
143 \begin{isamarkuptext}% |
|
144 \noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two parts: |
|
145 the \qn{operational} part names the class parameter (\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them |
|
146 (\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}). The local \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} and \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} are lifted to the theory toplevel, yielding the global |
|
147 parameter \isa{{\isaliteral{22}{\isachardoublequote}}mult\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequote}}} and the |
|
148 global theorem \hyperlink{fact.semigroup.assoc:}{\mbox{\isa{semigroup{\isaliteral{2E}{\isachardot}}assoc{\isaliteral{3A}{\isacharcolon}}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ z\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.% |
|
149 \end{isamarkuptext}% |
|
150 \isamarkuptrue% |
|
151 % |
|
152 \isamarkupsubsection{Class instantiation \label{sec:class_inst}% |
|
153 } |
|
154 \isamarkuptrue% |
|
155 % |
|
156 \begin{isamarkuptext}% |
|
157 The concrete type \isa{int} is made a \isa{semigroup} instance |
|
158 by providing a suitable definition for the class parameter \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}{\isaliteral{29}{\isacharparenright}}} and a proof for the specification of \hyperlink{fact.assoc}{\mbox{\isa{assoc}}}. This is |
|
159 accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:% |
|
160 \end{isamarkuptext}% |
|
161 \isamarkuptrue% |
|
162 % |
|
163 \isadelimquote |
|
164 % |
|
165 \endisadelimquote |
|
166 % |
|
167 \isatagquote |
|
168 \isacommand{instantiation}\isamarkupfalse% |
|
169 \ int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ semigroup\isanewline |
|
170 \isakeyword{begin}\isanewline |
|
171 \isanewline |
|
172 \isacommand{definition}\isamarkupfalse% |
|
173 \isanewline |
|
174 \ \ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}i\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ j\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}j{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
175 \isanewline |
|
176 \isacommand{instance}\isamarkupfalse% |
|
177 \ \isacommand{proof}\isamarkupfalse% |
|
178 \isanewline |
|
179 \ \ \isacommand{fix}\isamarkupfalse% |
|
180 \ i\ j\ k\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ \isacommand{have}\isamarkupfalse% |
|
181 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ j{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ k\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}j\ {\isaliteral{2B}{\isacharplus}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
182 \ simp\isanewline |
|
183 \ \ \isacommand{then}\isamarkupfalse% |
|
184 \ \isacommand{show}\isamarkupfalse% |
|
185 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ j{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ k\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}j\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
186 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
187 \ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
188 \isanewline |
|
189 \isacommand{qed}\isamarkupfalse% |
|
190 \isanewline |
|
191 \isanewline |
|
192 \isacommand{end}\isamarkupfalse% |
|
193 % |
|
194 \endisatagquote |
|
195 {\isafoldquote}% |
|
196 % |
|
197 \isadelimquote |
|
198 % |
|
199 \endisadelimquote |
|
200 % |
|
201 \begin{isamarkuptext}% |
|
202 \noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} defines class parameters at a |
|
203 particular instance using common specification tools (here, |
|
204 \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}). The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} opens a |
|
205 proof that the given parameters actually conform to the class |
|
206 specification. Note that the first proof step is the \hyperlink{method.default}{\mbox{\isa{default}}} method, which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}classes}}} method. This reduces an instance judgement to the |
|
207 relevant primitive proof goals; typically it is the first method |
|
208 applied in an instantiation proof. |
|
209 |
|
210 From now on, the type-checker will consider \isa{int} as a \isa{semigroup} automatically, i.e.\ any general results are immediately |
|
211 available on concrete instances. |
|
212 |
|
213 \medskip Another instance of \isa{semigroup} yields the natural |
|
214 numbers:% |
|
215 \end{isamarkuptext}% |
|
216 \isamarkuptrue% |
|
217 % |
|
218 \isadelimquote |
|
219 % |
|
220 \endisadelimquote |
|
221 % |
|
222 \isatagquote |
|
223 \isacommand{instantiation}\isamarkupfalse% |
|
224 \ nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ semigroup\isanewline |
|
225 \isakeyword{begin}\isanewline |
|
226 \isanewline |
|
227 \isacommand{primrec}\isamarkupfalse% |
|
228 \ mult{\isaliteral{5F}{\isacharunderscore}}nat\ \isakeyword{where}\isanewline |
|
229 \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
230 \ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}Suc\ m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
231 \isanewline |
|
232 \isacommand{instance}\isamarkupfalse% |
|
233 \ \isacommand{proof}\isamarkupfalse% |
|
234 \isanewline |
|
235 \ \ \isacommand{fix}\isamarkupfalse% |
|
236 \ m\ n\ q\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\ \isanewline |
|
237 \ \ \isacommand{show}\isamarkupfalse% |
|
238 \ {\isaliteral{22}{\isachardoublequoteopen}}m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ q\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ q{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
239 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
240 \ {\isaliteral{28}{\isacharparenleft}}induct\ m{\isaliteral{29}{\isacharparenright}}\ auto\isanewline |
|
241 \isacommand{qed}\isamarkupfalse% |
|
242 \isanewline |
|
243 \isanewline |
|
244 \isacommand{end}\isamarkupfalse% |
|
245 % |
|
246 \endisatagquote |
|
247 {\isafoldquote}% |
|
248 % |
|
249 \isadelimquote |
|
250 % |
|
251 \endisadelimquote |
|
252 % |
|
253 \begin{isamarkuptext}% |
|
254 \noindent Note the occurence of the name \isa{mult{\isaliteral{5F}{\isacharunderscore}}nat} in the |
|
255 primrec declaration; by default, the local name of a class operation |
|
256 \isa{f} to be instantiated on type constructor \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} is |
|
257 mangled as \isa{f{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}}. In case of uncertainty, these names may be |
|
258 inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}context}}}} command or the |
|
259 corresponding ProofGeneral button.% |
|
260 \end{isamarkuptext}% |
|
261 \isamarkuptrue% |
|
262 % |
|
263 \isamarkupsubsection{Lifting and parametric types% |
|
264 } |
|
265 \isamarkuptrue% |
|
266 % |
|
267 \begin{isamarkuptext}% |
|
268 Overloaded definitions given at a class instantiation may include |
|
269 recursion over the syntactic structure of types. As a canonical |
|
270 example, we model product semigroups using our simple algebra:% |
|
271 \end{isamarkuptext}% |
|
272 \isamarkuptrue% |
|
273 % |
|
274 \isadelimquote |
|
275 % |
|
276 \endisadelimquote |
|
277 % |
|
278 \isatagquote |
|
279 \isacommand{instantiation}\isamarkupfalse% |
|
280 \ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}semigroup{\isaliteral{2C}{\isacharcomma}}\ semigroup{\isaliteral{29}{\isacharparenright}}\ semigroup\isanewline |
|
281 \isakeyword{begin}\isanewline |
|
282 \isanewline |
|
283 \isacommand{definition}\isamarkupfalse% |
|
284 \isanewline |
|
285 \ \ mult{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}fst\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ fst\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ snd\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ snd\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
286 \isanewline |
|
287 \isacommand{instance}\isamarkupfalse% |
|
288 \ \isacommand{proof}\isamarkupfalse% |
|
289 \isanewline |
|
290 \ \ \isacommand{fix}\isamarkupfalse% |
|
291 \ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
292 \ \ \isacommand{show}\isamarkupfalse% |
|
293 \ {\isaliteral{22}{\isachardoublequoteopen}}p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
294 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
295 \ mult{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
|
296 \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ assoc{\isaliteral{29}{\isacharparenright}}\isanewline |
|
297 \isacommand{qed}\isamarkupfalse% |
|
298 \ \ \ \ \ \ \isanewline |
|
299 \isanewline |
|
300 \isacommand{end}\isamarkupfalse% |
|
301 % |
|
302 \endisatagquote |
|
303 {\isafoldquote}% |
|
304 % |
|
305 \isadelimquote |
|
306 % |
|
307 \endisadelimquote |
|
308 % |
|
309 \begin{isamarkuptext}% |
|
310 \noindent Associativity of product semigroups is established using |
|
311 the definition of \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}{\isaliteral{29}{\isacharparenright}}} on products and the hypothetical |
|
312 associativity of the type components; these hypotheses are |
|
313 legitimate due to the \isa{semigroup} constraints imposed on the |
|
314 type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition. Indeed, |
|
315 this pattern often occurs with parametric types and type classes.% |
|
316 \end{isamarkuptext}% |
|
317 \isamarkuptrue% |
|
318 % |
|
319 \isamarkupsubsection{Subclassing% |
|
320 } |
|
321 \isamarkuptrue% |
|
322 % |
|
323 \begin{isamarkuptext}% |
|
324 We define a subclass \isa{monoidl} (a semigroup with a left-hand |
|
325 neutral) by extending \isa{semigroup} with one additional |
|
326 parameter \isa{neutral} together with its characteristic property:% |
|
327 \end{isamarkuptext}% |
|
328 \isamarkuptrue% |
|
329 % |
|
330 \isadelimquote |
|
331 % |
|
332 \endisadelimquote |
|
333 % |
|
334 \isatagquote |
|
335 \isacommand{class}\isamarkupfalse% |
|
336 \ monoidl\ {\isaliteral{3D}{\isacharequal}}\ semigroup\ {\isaliteral{2B}{\isacharplus}}\isanewline |
|
337 \ \ \isakeyword{fixes}\ neutral\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
338 \ \ \isakeyword{assumes}\ neutl{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}% |
|
339 \endisatagquote |
|
340 {\isafoldquote}% |
|
341 % |
|
342 \isadelimquote |
|
343 % |
|
344 \endisadelimquote |
|
345 % |
|
346 \begin{isamarkuptext}% |
|
347 \noindent Again, we prove some instances, by providing suitable |
|
348 parameter definitions and proofs for the additional specifications. |
|
349 Observe that instantiations for types with the same arity may be |
|
350 simultaneous:% |
|
351 \end{isamarkuptext}% |
|
352 \isamarkuptrue% |
|
353 % |
|
354 \isadelimquote |
|
355 % |
|
356 \endisadelimquote |
|
357 % |
|
358 \isatagquote |
|
359 \isacommand{instantiation}\isamarkupfalse% |
|
360 \ nat\ \isakeyword{and}\ int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ monoidl\isanewline |
|
361 \isakeyword{begin}\isanewline |
|
362 \isanewline |
|
363 \isacommand{definition}\isamarkupfalse% |
|
364 \isanewline |
|
365 \ \ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
366 \isanewline |
|
367 \isacommand{definition}\isamarkupfalse% |
|
368 \isanewline |
|
369 \ \ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
370 \isanewline |
|
371 \isacommand{instance}\isamarkupfalse% |
|
372 \ \isacommand{proof}\isamarkupfalse% |
|
373 \isanewline |
|
374 \ \ \isacommand{fix}\isamarkupfalse% |
|
375 \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline |
|
376 \ \ \isacommand{show}\isamarkupfalse% |
|
377 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
378 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
379 \ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
|
380 \ simp\isanewline |
|
381 \isacommand{next}\isamarkupfalse% |
|
382 \isanewline |
|
383 \ \ \isacommand{fix}\isamarkupfalse% |
|
384 \ k\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\isanewline |
|
385 \ \ \isacommand{show}\isamarkupfalse% |
|
386 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ k\ {\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
387 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
388 \ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
|
389 \ simp\isanewline |
|
390 \isacommand{qed}\isamarkupfalse% |
|
391 \isanewline |
|
392 \isanewline |
|
393 \isacommand{end}\isamarkupfalse% |
|
394 \isanewline |
|
395 \isanewline |
|
396 \isacommand{instantiation}\isamarkupfalse% |
|
397 \ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}monoidl{\isaliteral{2C}{\isacharcomma}}\ monoidl{\isaliteral{29}{\isacharparenright}}\ monoidl\isanewline |
|
398 \isakeyword{begin}\isanewline |
|
399 \isanewline |
|
400 \isacommand{definition}\isamarkupfalse% |
|
401 \isanewline |
|
402 \ \ neutral{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
403 \isanewline |
|
404 \isacommand{instance}\isamarkupfalse% |
|
405 \ \isacommand{proof}\isamarkupfalse% |
|
406 \isanewline |
|
407 \ \ \isacommand{fix}\isamarkupfalse% |
|
408 \ p\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoidl\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoidl{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
409 \ \ \isacommand{show}\isamarkupfalse% |
|
410 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ p\ {\isaliteral{3D}{\isacharequal}}\ p{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
411 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
412 \ neutral{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ mult{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
|
413 \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ neutl{\isaliteral{29}{\isacharparenright}}\isanewline |
|
414 \isacommand{qed}\isamarkupfalse% |
|
415 \isanewline |
|
416 \isanewline |
|
417 \isacommand{end}\isamarkupfalse% |
|
418 % |
|
419 \endisatagquote |
|
420 {\isafoldquote}% |
|
421 % |
|
422 \isadelimquote |
|
423 % |
|
424 \endisadelimquote |
|
425 % |
|
426 \begin{isamarkuptext}% |
|
427 \noindent Fully-fledged monoids are modelled by another subclass, |
|
428 which does not add new parameters but tightens the specification:% |
|
429 \end{isamarkuptext}% |
|
430 \isamarkuptrue% |
|
431 % |
|
432 \isadelimquote |
|
433 % |
|
434 \endisadelimquote |
|
435 % |
|
436 \isatagquote |
|
437 \isacommand{class}\isamarkupfalse% |
|
438 \ monoid\ {\isaliteral{3D}{\isacharequal}}\ monoidl\ {\isaliteral{2B}{\isacharplus}}\isanewline |
|
439 \ \ \isakeyword{assumes}\ neutr{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
440 \isanewline |
|
441 \isacommand{instantiation}\isamarkupfalse% |
|
442 \ nat\ \isakeyword{and}\ int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ monoid\ \isanewline |
|
443 \isakeyword{begin}\isanewline |
|
444 \isanewline |
|
445 \isacommand{instance}\isamarkupfalse% |
|
446 \ \isacommand{proof}\isamarkupfalse% |
|
447 \isanewline |
|
448 \ \ \isacommand{fix}\isamarkupfalse% |
|
449 \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline |
|
450 \ \ \isacommand{show}\isamarkupfalse% |
|
451 \ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
452 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
453 \ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
|
454 \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all\isanewline |
|
455 \isacommand{next}\isamarkupfalse% |
|
456 \isanewline |
|
457 \ \ \isacommand{fix}\isamarkupfalse% |
|
458 \ k\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\isanewline |
|
459 \ \ \isacommand{show}\isamarkupfalse% |
|
460 \ {\isaliteral{22}{\isachardoublequoteopen}}k\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
461 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
462 \ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
|
463 \ simp\isanewline |
|
464 \isacommand{qed}\isamarkupfalse% |
|
465 \isanewline |
|
466 \isanewline |
|
467 \isacommand{end}\isamarkupfalse% |
|
468 \isanewline |
|
469 \isanewline |
|
470 \isacommand{instantiation}\isamarkupfalse% |
|
471 \ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}monoid{\isaliteral{2C}{\isacharcomma}}\ monoid{\isaliteral{29}{\isacharparenright}}\ monoid\isanewline |
|
472 \isakeyword{begin}\isanewline |
|
473 \isanewline |
|
474 \isacommand{instance}\isamarkupfalse% |
|
475 \ \isacommand{proof}\isamarkupfalse% |
|
476 \ \isanewline |
|
477 \ \ \isacommand{fix}\isamarkupfalse% |
|
478 \ p\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoid\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoid{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
479 \ \ \isacommand{show}\isamarkupfalse% |
|
480 \ {\isaliteral{22}{\isachardoublequoteopen}}p\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ p{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
481 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
482 \ neutral{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ mult{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
|
483 \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ neutr{\isaliteral{29}{\isacharparenright}}\isanewline |
|
484 \isacommand{qed}\isamarkupfalse% |
|
485 \isanewline |
|
486 \isanewline |
|
487 \isacommand{end}\isamarkupfalse% |
|
488 % |
|
489 \endisatagquote |
|
490 {\isafoldquote}% |
|
491 % |
|
492 \isadelimquote |
|
493 % |
|
494 \endisadelimquote |
|
495 % |
|
496 \begin{isamarkuptext}% |
|
497 \noindent To finish our small algebra example, we add a \isa{group} class with a corresponding instance:% |
|
498 \end{isamarkuptext}% |
|
499 \isamarkuptrue% |
|
500 % |
|
501 \isadelimquote |
|
502 % |
|
503 \endisadelimquote |
|
504 % |
|
505 \isatagquote |
|
506 \isacommand{class}\isamarkupfalse% |
|
507 \ group\ {\isaliteral{3D}{\isacharequal}}\ monoidl\ {\isaliteral{2B}{\isacharplus}}\isanewline |
|
508 \ \ \isakeyword{fixes}\ inverse\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5C3C6469763E}{\isasymdiv}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
509 \ \ \isakeyword{assumes}\ invl{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
510 \isanewline |
|
511 \isacommand{instantiation}\isamarkupfalse% |
|
512 \ int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ group\isanewline |
|
513 \isakeyword{begin}\isanewline |
|
514 \isanewline |
|
515 \isacommand{definition}\isamarkupfalse% |
|
516 \isanewline |
|
517 \ \ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}i{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
518 \isanewline |
|
519 \isacommand{instance}\isamarkupfalse% |
|
520 \ \isacommand{proof}\isamarkupfalse% |
|
521 \isanewline |
|
522 \ \ \isacommand{fix}\isamarkupfalse% |
|
523 \ i\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\isanewline |
|
524 \ \ \isacommand{have}\isamarkupfalse% |
|
525 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2D}{\isacharminus}}i\ {\isaliteral{2B}{\isacharplus}}\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
526 \ simp\isanewline |
|
527 \ \ \isacommand{then}\isamarkupfalse% |
|
528 \ \isacommand{show}\isamarkupfalse% |
|
529 \ {\isaliteral{22}{\isachardoublequoteopen}}i{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
530 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
531 \ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
532 \isanewline |
|
533 \isacommand{qed}\isamarkupfalse% |
|
534 \isanewline |
|
535 \isanewline |
|
536 \isacommand{end}\isamarkupfalse% |
|
537 % |
|
538 \endisatagquote |
|
539 {\isafoldquote}% |
|
540 % |
|
541 \isadelimquote |
|
542 % |
|
543 \endisadelimquote |
|
544 % |
|
545 \isamarkupsection{Type classes as locales% |
|
546 } |
|
547 \isamarkuptrue% |
|
548 % |
|
549 \isamarkupsubsection{A look behind the scenes% |
|
550 } |
|
551 \isamarkuptrue% |
|
552 % |
|
553 \begin{isamarkuptext}% |
|
554 The example above gives an impression how Isar type classes work in |
|
555 practice. As stated in the introduction, classes also provide a |
|
556 link to Isar's locale system. Indeed, the logical core of a class |
|
557 is nothing other than a locale:% |
|
558 \end{isamarkuptext}% |
|
559 \isamarkuptrue% |
|
560 % |
|
561 \isadelimquote |
|
562 % |
|
563 \endisadelimquote |
|
564 % |
|
565 \isatagquote |
|
566 \isacommand{class}\isamarkupfalse% |
|
567 \ idem\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
568 \ \ \isakeyword{fixes}\ f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
569 \ \ \isakeyword{assumes}\ idem{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}f\ {\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ x{\isaliteral{22}{\isachardoublequoteclose}}% |
|
570 \endisatagquote |
|
571 {\isafoldquote}% |
|
572 % |
|
573 \isadelimquote |
|
574 % |
|
575 \endisadelimquote |
|
576 % |
|
577 \begin{isamarkuptext}% |
|
578 \noindent essentially introduces the locale% |
|
579 \end{isamarkuptext}% |
|
580 \isamarkuptrue% |
|
581 \ % |
|
582 \isadeliminvisible |
|
583 % |
|
584 \endisadeliminvisible |
|
585 % |
|
586 \isataginvisible |
|
587 % |
|
588 \endisataginvisible |
|
589 {\isafoldinvisible}% |
|
590 % |
|
591 \isadeliminvisible |
|
592 % |
|
593 \endisadeliminvisible |
|
594 % |
|
595 \isadelimquote |
|
596 % |
|
597 \endisadelimquote |
|
598 % |
|
599 \isatagquote |
|
600 \isacommand{locale}\isamarkupfalse% |
|
601 \ idem\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
602 \ \ \isakeyword{fixes}\ f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
603 \ \ \isakeyword{assumes}\ idem{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}f\ {\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ x{\isaliteral{22}{\isachardoublequoteclose}}% |
|
604 \endisatagquote |
|
605 {\isafoldquote}% |
|
606 % |
|
607 \isadelimquote |
|
608 % |
|
609 \endisadelimquote |
|
610 % |
|
611 \begin{isamarkuptext}% |
|
612 \noindent together with corresponding constant(s):% |
|
613 \end{isamarkuptext}% |
|
614 \isamarkuptrue% |
|
615 % |
|
616 \isadelimquote |
|
617 % |
|
618 \endisadelimquote |
|
619 % |
|
620 \isatagquote |
|
621 \isacommand{consts}\isamarkupfalse% |
|
622 \ f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
623 \endisatagquote |
|
624 {\isafoldquote}% |
|
625 % |
|
626 \isadelimquote |
|
627 % |
|
628 \endisadelimquote |
|
629 % |
|
630 \begin{isamarkuptext}% |
|
631 \noindent The connection to the type system is done by means |
|
632 of a primitive type class% |
|
633 \end{isamarkuptext}% |
|
634 \isamarkuptrue% |
|
635 \ % |
|
636 \isadeliminvisible |
|
637 % |
|
638 \endisadeliminvisible |
|
639 % |
|
640 \isataginvisible |
|
641 % |
|
642 \endisataginvisible |
|
643 {\isafoldinvisible}% |
|
644 % |
|
645 \isadeliminvisible |
|
646 % |
|
647 \endisadeliminvisible |
|
648 % |
|
649 \isadelimquote |
|
650 % |
|
651 \endisadelimquote |
|
652 % |
|
653 \isatagquote |
|
654 \isacommand{classes}\isamarkupfalse% |
|
655 \ idem\ {\isaliteral{3C}{\isacharless}}\ type% |
|
656 \endisatagquote |
|
657 {\isafoldquote}% |
|
658 % |
|
659 \isadelimquote |
|
660 % |
|
661 \endisadelimquote |
|
662 % |
|
663 \isadeliminvisible |
|
664 % |
|
665 \endisadeliminvisible |
|
666 % |
|
667 \isataginvisible |
|
668 % |
|
669 \endisataginvisible |
|
670 {\isafoldinvisible}% |
|
671 % |
|
672 \isadeliminvisible |
|
673 % |
|
674 \endisadeliminvisible |
|
675 % |
|
676 \begin{isamarkuptext}% |
|
677 \noindent together with a corresponding interpretation:% |
|
678 \end{isamarkuptext}% |
|
679 \isamarkuptrue% |
|
680 % |
|
681 \isadelimquote |
|
682 % |
|
683 \endisadelimquote |
|
684 % |
|
685 \isatagquote |
|
686 \isacommand{interpretation}\isamarkupfalse% |
|
687 \ idem{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{3A}{\isacharcolon}}\isanewline |
|
688 \ \ idem\ {\isaliteral{22}{\isachardoublequoteopen}}f\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}idem{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
689 \endisatagquote |
|
690 {\isafoldquote}% |
|
691 % |
|
692 \isadelimquote |
|
693 % |
|
694 \endisadelimquote |
|
695 % |
|
696 \begin{isamarkuptext}% |
|
697 \noindent This gives you the full power of the Isabelle module system; |
|
698 conclusions in locale \isa{idem} are implicitly propagated |
|
699 to class \isa{idem}.% |
|
700 \end{isamarkuptext}% |
|
701 \isamarkuptrue% |
|
702 \ % |
|
703 \isadeliminvisible |
|
704 % |
|
705 \endisadeliminvisible |
|
706 % |
|
707 \isataginvisible |
|
708 % |
|
709 \endisataginvisible |
|
710 {\isafoldinvisible}% |
|
711 % |
|
712 \isadeliminvisible |
|
713 % |
|
714 \endisadeliminvisible |
|
715 % |
|
716 \isamarkupsubsection{Abstract reasoning% |
|
717 } |
|
718 \isamarkuptrue% |
|
719 % |
|
720 \begin{isamarkuptext}% |
|
721 Isabelle locales enable reasoning at a general level, while results |
|
722 are implicitly transferred to all instances. For example, we can |
|
723 now establish the \isa{left{\isaliteral{5F}{\isacharunderscore}}cancel} lemma for groups, which |
|
724 states that the function \isa{{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}{\isaliteral{29}{\isacharparenright}}} is injective:% |
|
725 \end{isamarkuptext}% |
|
726 \isamarkuptrue% |
|
727 % |
|
728 \isadelimquote |
|
729 % |
|
730 \endisadelimquote |
|
731 % |
|
732 \isatagquote |
|
733 \isacommand{lemma}\isamarkupfalse% |
|
734 \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{in}\ group{\isaliteral{29}{\isacharparenright}}\ left{\isaliteral{5F}{\isacharunderscore}}cancel{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
735 \isacommand{proof}\isamarkupfalse% |
|
736 \isanewline |
|
737 \ \ \isacommand{assume}\isamarkupfalse% |
|
738 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
739 \ \ \isacommand{then}\isamarkupfalse% |
|
740 \ \isacommand{have}\isamarkupfalse% |
|
741 \ {\isaliteral{22}{\isachardoublequoteopen}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
742 \ simp\isanewline |
|
743 \ \ \isacommand{then}\isamarkupfalse% |
|
744 \ \isacommand{have}\isamarkupfalse% |
|
745 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{using}\isamarkupfalse% |
|
746 \ assoc\ \isacommand{by}\isamarkupfalse% |
|
747 \ simp\isanewline |
|
748 \ \ \isacommand{then}\isamarkupfalse% |
|
749 \ \isacommand{show}\isamarkupfalse% |
|
750 \ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{using}\isamarkupfalse% |
|
751 \ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse% |
|
752 \ simp\isanewline |
|
753 \isacommand{next}\isamarkupfalse% |
|
754 \isanewline |
|
755 \ \ \isacommand{assume}\isamarkupfalse% |
|
756 \ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
757 \ \ \isacommand{then}\isamarkupfalse% |
|
758 \ \isacommand{show}\isamarkupfalse% |
|
759 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
760 \ simp\isanewline |
|
761 \isacommand{qed}\isamarkupfalse% |
|
762 % |
|
763 \endisatagquote |
|
764 {\isafoldquote}% |
|
765 % |
|
766 \isadelimquote |
|
767 % |
|
768 \endisadelimquote |
|
769 % |
|
770 \begin{isamarkuptext}% |
|
771 \noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target |
|
772 specification indicates that the result is recorded within that |
|
773 context for later use. This local theorem is also lifted to the |
|
774 global one \hyperlink{fact.group.left-cancel:}{\mbox{\isa{group{\isaliteral{2E}{\isachardot}}left{\isaliteral{5F}{\isacharunderscore}}cancel{\isaliteral{3A}{\isacharcolon}}}}} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ z\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}group{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequote}}}. Since type \isa{int} has been |
|
775 made an instance of \isa{group} before, we may refer to that |
|
776 fact as well: \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ z\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ int{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequote}}}.% |
|
777 \end{isamarkuptext}% |
|
778 \isamarkuptrue% |
|
779 % |
|
780 \isamarkupsubsection{Derived definitions% |
|
781 } |
|
782 \isamarkuptrue% |
|
783 % |
|
784 \begin{isamarkuptext}% |
|
785 Isabelle locales are targets which support local definitions:% |
|
786 \end{isamarkuptext}% |
|
787 \isamarkuptrue% |
|
788 % |
|
789 \isadelimquote |
|
790 % |
|
791 \endisadelimquote |
|
792 % |
|
793 \isatagquote |
|
794 \isacommand{primrec}\isamarkupfalse% |
|
795 \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{in}\ monoid{\isaliteral{29}{\isacharparenright}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
796 \ \ {\isaliteral{22}{\isachardoublequoteopen}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isadigit{0}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
797 \ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ n\ x{\isaliteral{22}{\isachardoublequoteclose}}% |
|
798 \endisatagquote |
|
799 {\isafoldquote}% |
|
800 % |
|
801 \isadelimquote |
|
802 % |
|
803 \endisadelimquote |
|
804 % |
|
805 \begin{isamarkuptext}% |
|
806 \noindent If the locale \isa{group} is also a class, this local |
|
807 definition is propagated onto a global definition of \isa{{\isaliteral{22}{\isachardoublequote}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoid\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoid{\isaliteral{22}{\isachardoublequote}}} with corresponding theorems |
|
808 |
|
809 \isa{pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isadigit{0}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\isasep\isanewline% |
|
810 pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ n\ x}. |
|
811 |
|
812 \noindent As you can see from this example, for local definitions |
|
813 you may use any specification tool which works together with |
|
814 locales, such as Krauss's recursive function package |
|
815 \cite{krauss2006}.% |
|
816 \end{isamarkuptext}% |
|
817 \isamarkuptrue% |
|
818 % |
|
819 \isamarkupsubsection{A functor analogy% |
|
820 } |
|
821 \isamarkuptrue% |
|
822 % |
|
823 \begin{isamarkuptext}% |
|
824 We introduced Isar classes by analogy to type classes in functional |
|
825 programming; if we reconsider this in the context of what has been |
|
826 said about type classes and locales, we can drive this analogy |
|
827 further by stating that type classes essentially correspond to |
|
828 functors that have a canonical interpretation as type classes. |
|
829 There is also the possibility of other interpretations. For |
|
830 example, \isa{list}s also form a monoid with \isa{append} and |
|
831 \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} as operations, but it seems inappropriate to apply to |
|
832 lists the same operations as for genuinely algebraic types. In such |
|
833 a case, we can simply make a particular interpretation of monoids |
|
834 for lists:% |
|
835 \end{isamarkuptext}% |
|
836 \isamarkuptrue% |
|
837 % |
|
838 \isadelimquote |
|
839 % |
|
840 \endisadelimquote |
|
841 % |
|
842 \isatagquote |
|
843 \isacommand{interpretation}\isamarkupfalse% |
|
844 \ list{\isaliteral{5F}{\isacharunderscore}}monoid{\isaliteral{3A}{\isacharcolon}}\ monoid\ append\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
845 \ \ \isacommand{proof}\isamarkupfalse% |
|
846 \ \isacommand{qed}\isamarkupfalse% |
|
847 \ auto% |
|
848 \endisatagquote |
|
849 {\isafoldquote}% |
|
850 % |
|
851 \isadelimquote |
|
852 % |
|
853 \endisadelimquote |
|
854 % |
|
855 \begin{isamarkuptext}% |
|
856 \noindent This enables us to apply facts on monoids |
|
857 to lists, e.g. \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{40}{\isacharat}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x}. |
|
858 |
|
859 When using this interpretation pattern, it may also |
|
860 be appropriate to map derived definitions accordingly:% |
|
861 \end{isamarkuptext}% |
|
862 \isamarkuptrue% |
|
863 % |
|
864 \isadelimquote |
|
865 % |
|
866 \endisadelimquote |
|
867 % |
|
868 \isatagquote |
|
869 \isacommand{primrec}\isamarkupfalse% |
|
870 \ replicate\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
871 \ \ {\isaliteral{22}{\isachardoublequoteopen}}replicate\ {\isadigit{0}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
872 \ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}replicate\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs\ {\isaliteral{40}{\isacharat}}\ replicate\ n\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
873 \isanewline |
|
874 \isacommand{interpretation}\isamarkupfalse% |
|
875 \ list{\isaliteral{5F}{\isacharunderscore}}monoid{\isaliteral{3A}{\isacharcolon}}\ monoid\ append\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
876 \ \ {\isaliteral{22}{\isachardoublequoteopen}}monoid{\isaliteral{2E}{\isachardot}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ append\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ replicate{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
877 \isacommand{proof}\isamarkupfalse% |
|
878 \ {\isaliteral{2D}{\isacharminus}}\isanewline |
|
879 \ \ \isacommand{interpret}\isamarkupfalse% |
|
880 \ monoid\ append\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
881 \isanewline |
|
882 \ \ \isacommand{show}\isamarkupfalse% |
|
883 \ {\isaliteral{22}{\isachardoublequoteopen}}monoid{\isaliteral{2E}{\isachardot}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ append\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ replicate{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
884 \ \ \isacommand{proof}\isamarkupfalse% |
|
885 \isanewline |
|
886 \ \ \ \ \isacommand{fix}\isamarkupfalse% |
|
887 \ n\isanewline |
|
888 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
889 \ {\isaliteral{22}{\isachardoublequoteopen}}monoid{\isaliteral{2E}{\isachardot}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ append\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ replicate\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
890 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
891 \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\ auto\isanewline |
|
892 \ \ \isacommand{qed}\isamarkupfalse% |
|
893 \isanewline |
|
894 \isacommand{qed}\isamarkupfalse% |
|
895 \ intro{\isaliteral{5F}{\isacharunderscore}}locales% |
|
896 \endisatagquote |
|
897 {\isafoldquote}% |
|
898 % |
|
899 \isadelimquote |
|
900 % |
|
901 \endisadelimquote |
|
902 % |
|
903 \begin{isamarkuptext}% |
|
904 \noindent This pattern is also helpful to reuse abstract |
|
905 specifications on the \emph{same} type. For example, think of a |
|
906 class \isa{preorder}; for type \isa{nat}, there are at least two |
|
907 possible instances: the natural order or the order induced by the |
|
908 divides relation. But only one of these instances can be used for |
|
909 \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}; using the locale behind the class \isa{preorder}, it is still possible to utilise the same abstract |
|
910 specification again using \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}.% |
|
911 \end{isamarkuptext}% |
|
912 \isamarkuptrue% |
|
913 % |
|
914 \isamarkupsubsection{Additional subclass relations% |
|
915 } |
|
916 \isamarkuptrue% |
|
917 % |
|
918 \begin{isamarkuptext}% |
|
919 Any \isa{group} is also a \isa{monoid}; this can be made |
|
920 explicit by claiming an additional subclass relation, together with |
|
921 a proof of the logical difference:% |
|
922 \end{isamarkuptext}% |
|
923 \isamarkuptrue% |
|
924 % |
|
925 \isadelimquote |
|
926 % |
|
927 \endisadelimquote |
|
928 % |
|
929 \isatagquote |
|
930 \isacommand{subclass}\isamarkupfalse% |
|
931 \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{in}\ group{\isaliteral{29}{\isacharparenright}}\ monoid\isanewline |
|
932 \isacommand{proof}\isamarkupfalse% |
|
933 \isanewline |
|
934 \ \ \isacommand{fix}\isamarkupfalse% |
|
935 \ x\isanewline |
|
936 \ \ \isacommand{from}\isamarkupfalse% |
|
937 \ invl\ \isacommand{have}\isamarkupfalse% |
|
938 \ {\isaliteral{22}{\isachardoublequoteopen}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
939 \ simp\isanewline |
|
940 \ \ \isacommand{with}\isamarkupfalse% |
|
941 \ assoc\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}\ neutl\ invl\ \isacommand{have}\isamarkupfalse% |
|
942 \ {\isaliteral{22}{\isachardoublequoteopen}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
943 \ simp\isanewline |
|
944 \ \ \isacommand{with}\isamarkupfalse% |
|
945 \ left{\isaliteral{5F}{\isacharunderscore}}cancel\ \isacommand{show}\isamarkupfalse% |
|
946 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
947 \ simp\isanewline |
|
948 \isacommand{qed}\isamarkupfalse% |
|
949 % |
|
950 \endisatagquote |
|
951 {\isafoldquote}% |
|
952 % |
|
953 \isadelimquote |
|
954 % |
|
955 \endisadelimquote |
|
956 % |
|
957 \begin{isamarkuptext}% |
|
958 The logical proof is carried out on the locale level. Afterwards it |
|
959 is propagated to the type system, making \isa{group} an instance |
|
960 of \isa{monoid} by adding an additional edge to the graph of |
|
961 subclass relations (\figref{fig:subclass}). |
|
962 |
|
963 \begin{figure}[htbp] |
|
964 \begin{center} |
|
965 \small |
|
966 \unitlength 0.6mm |
|
967 \begin{picture}(40,60)(0,0) |
|
968 \put(20,60){\makebox(0,0){\isa{semigroup}}} |
|
969 \put(20,40){\makebox(0,0){\isa{monoidl}}} |
|
970 \put(00,20){\makebox(0,0){\isa{monoid}}} |
|
971 \put(40,00){\makebox(0,0){\isa{group}}} |
|
972 \put(20,55){\vector(0,-1){10}} |
|
973 \put(15,35){\vector(-1,-1){10}} |
|
974 \put(25,35){\vector(1,-3){10}} |
|
975 \end{picture} |
|
976 \hspace{8em} |
|
977 \begin{picture}(40,60)(0,0) |
|
978 \put(20,60){\makebox(0,0){\isa{semigroup}}} |
|
979 \put(20,40){\makebox(0,0){\isa{monoidl}}} |
|
980 \put(00,20){\makebox(0,0){\isa{monoid}}} |
|
981 \put(40,00){\makebox(0,0){\isa{group}}} |
|
982 \put(20,55){\vector(0,-1){10}} |
|
983 \put(15,35){\vector(-1,-1){10}} |
|
984 \put(05,15){\vector(3,-1){30}} |
|
985 \end{picture} |
|
986 \caption{Subclass relationship of monoids and groups: |
|
987 before and after establishing the relationship |
|
988 \isa{group\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ monoid}; transitive edges are left out.} |
|
989 \label{fig:subclass} |
|
990 \end{center} |
|
991 \end{figure} |
|
992 |
|
993 For illustration, a derived definition in \isa{group} using \isa{pow{\isaliteral{5F}{\isacharunderscore}}nat}% |
|
994 \end{isamarkuptext}% |
|
995 \isamarkuptrue% |
|
996 % |
|
997 \isadelimquote |
|
998 % |
|
999 \endisadelimquote |
|
1000 % |
|
1001 \isatagquote |
|
1002 \isacommand{definition}\isamarkupfalse% |
|
1003 \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{in}\ group{\isaliteral{29}{\isacharparenright}}\ pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
1004 \ \ {\isaliteral{22}{\isachardoublequoteopen}}pow{\isaliteral{5F}{\isacharunderscore}}int\ k\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ k\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\isanewline |
|
1005 \ \ \ \ then\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ k{\isaliteral{29}{\isacharparenright}}\ x\isanewline |
|
1006 \ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6469763E}{\isasymdiv}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
1007 \endisatagquote |
|
1008 {\isafoldquote}% |
|
1009 % |
|
1010 \isadelimquote |
|
1011 % |
|
1012 \endisadelimquote |
|
1013 % |
|
1014 \begin{isamarkuptext}% |
|
1015 \noindent yields the global definition of \isa{{\isaliteral{22}{\isachardoublequote}}pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}group\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}group{\isaliteral{22}{\isachardoublequote}}} with the corresponding theorem \isa{pow{\isaliteral{5F}{\isacharunderscore}}int\ k\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isadigit{0}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ k\ then\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ k{\isaliteral{29}{\isacharparenright}}\ x\ else\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6469763E}{\isasymdiv}}{\isaliteral{29}{\isacharparenright}}}.% |
|
1016 \end{isamarkuptext}% |
|
1017 \isamarkuptrue% |
|
1018 % |
|
1019 \isamarkupsubsection{A note on syntax% |
|
1020 } |
|
1021 \isamarkuptrue% |
|
1022 % |
|
1023 \begin{isamarkuptext}% |
|
1024 As a convenience, class context syntax allows references to local |
|
1025 class operations and their global counterparts uniformly; type |
|
1026 inference resolves ambiguities. For example:% |
|
1027 \end{isamarkuptext}% |
|
1028 \isamarkuptrue% |
|
1029 % |
|
1030 \isadelimquote |
|
1031 % |
|
1032 \endisadelimquote |
|
1033 % |
|
1034 \isatagquote |
|
1035 \isacommand{context}\isamarkupfalse% |
|
1036 \ semigroup\isanewline |
|
1037 \isakeyword{begin}\isanewline |
|
1038 \isanewline |
|
1039 \isacommand{term}\isamarkupfalse% |
|
1040 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\ % |
|
1041 \isamarkupcmt{example 1% |
|
1042 } |
|
1043 \isanewline |
|
1044 \isacommand{term}\isamarkupfalse% |
|
1045 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\ % |
|
1046 \isamarkupcmt{example 2% |
|
1047 } |
|
1048 \isanewline |
|
1049 \isanewline |
|
1050 \isacommand{end}\isamarkupfalse% |
|
1051 \isanewline |
|
1052 \isanewline |
|
1053 \isacommand{term}\isamarkupfalse% |
|
1054 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\ % |
|
1055 \isamarkupcmt{example 3% |
|
1056 } |
|
1057 % |
|
1058 \endisatagquote |
|
1059 {\isafoldquote}% |
|
1060 % |
|
1061 \isadelimquote |
|
1062 % |
|
1063 \endisadelimquote |
|
1064 % |
|
1065 \begin{isamarkuptext}% |
|
1066 \noindent Here in example 1, the term refers to the local class |
|
1067 operation \isa{mult\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}}, whereas in example 2 the type |
|
1068 constraint enforces the global class operation \isa{mult\ {\isaliteral{5B}{\isacharbrackleft}}nat{\isaliteral{5D}{\isacharbrackright}}}. |
|
1069 In the global context in example 3, the reference is to the |
|
1070 polymorphic global class operation \isa{mult\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ semigroup{\isaliteral{5D}{\isacharbrackright}}}.% |
|
1071 \end{isamarkuptext}% |
|
1072 \isamarkuptrue% |
|
1073 % |
|
1074 \isamarkupsection{Further issues% |
|
1075 } |
|
1076 \isamarkuptrue% |
|
1077 % |
|
1078 \isamarkupsubsection{Type classes and code generation% |
|
1079 } |
|
1080 \isamarkuptrue% |
|
1081 % |
|
1082 \begin{isamarkuptext}% |
|
1083 Turning back to the first motivation for type classes, namely |
|
1084 overloading, it is obvious that overloading stemming from \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} statements and \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} targets naturally |
|
1085 maps to Haskell type classes. The code generator framework |
|
1086 \cite{isabelle-codegen} takes this into account. If the target |
|
1087 language (e.g.~SML) lacks type classes, then they are implemented by |
|
1088 an explicit dictionary construction. As example, let's go back to |
|
1089 the power function:% |
|
1090 \end{isamarkuptext}% |
|
1091 \isamarkuptrue% |
|
1092 % |
|
1093 \isadelimquote |
|
1094 % |
|
1095 \endisadelimquote |
|
1096 % |
|
1097 \isatagquote |
|
1098 \isacommand{definition}\isamarkupfalse% |
|
1099 \ example\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ \isakeyword{where}\isanewline |
|
1100 \ \ {\isaliteral{22}{\isachardoublequoteopen}}example\ {\isaliteral{3D}{\isacharequal}}\ pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isadigit{1}}{\isadigit{0}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
1101 \endisatagquote |
|
1102 {\isafoldquote}% |
|
1103 % |
|
1104 \isadelimquote |
|
1105 % |
|
1106 \endisadelimquote |
|
1107 % |
|
1108 \begin{isamarkuptext}% |
|
1109 \noindent This maps to Haskell as follows:% |
|
1110 \end{isamarkuptext}% |
|
1111 \isamarkuptrue% |
|
1112 % |
|
1113 \isadeliminvisible |
|
1114 % |
|
1115 \endisadeliminvisible |
|
1116 % |
|
1117 \isataginvisible |
|
1118 % |
|
1119 \endisataginvisible |
|
1120 {\isafoldinvisible}% |
|
1121 % |
|
1122 \isadeliminvisible |
|
1123 % |
|
1124 \endisadeliminvisible |
|
1125 % |
|
1126 \isadelimquotetypewriter |
|
1127 % |
|
1128 \endisadelimquotetypewriter |
|
1129 % |
|
1130 \isatagquotetypewriter |
|
1131 % |
|
1132 \begin{isamarkuptext}% |
|
1133 module\ Example\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1134 \isanewline |
|
1135 import\ Prelude\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3C}{\isacharless}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
|
1136 \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3C}{\isacharless}}{\isaliteral{3C}{\isacharless}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2E}{\isachardot}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{24}{\isachardollar}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{24}{\isachardollar}}{\isaliteral{21}{\isacharbang}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
|
1137 \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ Eq{\isaliteral{2C}{\isacharcomma}}\ error{\isaliteral{2C}{\isacharcomma}}\ id{\isaliteral{2C}{\isacharcomma}}\ return{\isaliteral{2C}{\isacharcomma}}\ not{\isaliteral{2C}{\isacharcomma}}\ fst{\isaliteral{2C}{\isacharcomma}}\ snd{\isaliteral{2C}{\isacharcomma}}\ map{\isaliteral{2C}{\isacharcomma}}\ filter{\isaliteral{2C}{\isacharcomma}}\ concat{\isaliteral{2C}{\isacharcomma}}\isanewline |
|
1138 \ \ concatMap{\isaliteral{2C}{\isacharcomma}}\ reverse{\isaliteral{2C}{\isacharcomma}}\ zip{\isaliteral{2C}{\isacharcomma}}\ null{\isaliteral{2C}{\isacharcomma}}\ takeWhile{\isaliteral{2C}{\isacharcomma}}\ dropWhile{\isaliteral{2C}{\isacharcomma}}\ all{\isaliteral{2C}{\isacharcomma}}\ any{\isaliteral{2C}{\isacharcomma}}\ Integer{\isaliteral{2C}{\isacharcomma}}\isanewline |
|
1139 \ \ negate{\isaliteral{2C}{\isacharcomma}}\ abs{\isaliteral{2C}{\isacharcomma}}\ divMod{\isaliteral{2C}{\isacharcomma}}\ String{\isaliteral{2C}{\isacharcomma}}\ Bool{\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ False{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ Maybe{\isaliteral{28}{\isacharparenleft}}Nothing{\isaliteral{2C}{\isacharcomma}}\ Just{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1140 import\ qualified\ Prelude{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1141 \isanewline |
|
1142 data\ Nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1143 \isanewline |
|
1144 data\ Num\ {\isaliteral{3D}{\isacharequal}}\ One\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{0}}\ Num\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{1}}\ Num{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1145 \isanewline |
|
1146 apsnd\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a\ b\ c{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1147 apsnd\ f\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ f\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1148 \isanewline |
|
1149 sgn{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1150 sgn{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ i\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ {\isadigit{0}}\ else\ {\isaliteral{28}{\isacharparenleft}}if\ {\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ i\ then\ {\isadigit{1}}\ else\ negate\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1151 \isanewline |
|
1152 abs{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1153 abs{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ i\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{0}}\ then\ negate\ i\ else\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1154 \isanewline |
|
1155 divmod{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}Integer{\isaliteral{2C}{\isacharcomma}}\ Integer{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1156 divmod{\isaliteral{5F}{\isacharunderscore}}int\ k\ l\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1157 \ \ {\isaliteral{28}{\isacharparenleft}}if\ k\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1158 \ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}if\ l\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1159 \ \ \ \ \ \ \ \ \ \ \ else\ apsnd\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C}{\isacharbackslash}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ sgn{\isaliteral{5F}{\isacharunderscore}}int\ l\ {\isaliteral{2A}{\isacharasterisk}}\ a{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1160 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ sgn{\isaliteral{5F}{\isacharunderscore}}int\ k\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ sgn{\isaliteral{5F}{\isacharunderscore}}int\ l\ then\ divMod\ {\isaliteral{28}{\isacharparenleft}}abs\ k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}abs\ l{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1161 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ let\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1162 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}r{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ divMod\ {\isaliteral{28}{\isacharparenleft}}abs\ k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}abs\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1163 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7D}{\isacharbraceright}}\ in\ {\isaliteral{28}{\isacharparenleft}}if\ s\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ {\isaliteral{28}{\isacharparenleft}}negate\ r{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1164 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}negate\ r\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ abs{\isaliteral{5F}{\isacharunderscore}}int\ l\ {\isaliteral{2D}{\isacharminus}}\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1165 \isanewline |
|
1166 plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1167 plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ m\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1168 plus{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1169 \isanewline |
|
1170 nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1171 nat\ k\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1172 \ \ {\isaliteral{28}{\isacharparenleft}}if\ k\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\isanewline |
|
1173 \ \ \ \ else\ let\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1174 \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ divmod{\isaliteral{5F}{\isacharunderscore}}int\ k\ {\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1175 \ \ \ \ \ \ \ \ \ \ \ n\ {\isaliteral{3D}{\isacharequal}}\ nat\ l{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1176 \ \ \ \ \ \ \ \ \ \ \ la\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ n\ n{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1177 \ \ \ \ \ \ \ \ \ {\isaliteral{7D}{\isacharbraceright}}\ in\ {\isaliteral{28}{\isacharparenleft}}if\ j\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ la\ else\ Suc\ la{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1178 \isanewline |
|
1179 class\ Semigroup\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1180 \ \ mult\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1181 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1182 \isanewline |
|
1183 class\ {\isaliteral{28}{\isacharparenleft}}Semigroup\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Monoidl\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1184 \ \ neutral\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1185 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1186 \isanewline |
|
1187 class\ {\isaliteral{28}{\isacharparenleft}}Monoidl\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Monoid\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1188 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1189 \isanewline |
|
1190 class\ {\isaliteral{28}{\isacharparenleft}}Monoid\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Group\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1191 \ \ inverse\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1192 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1193 \isanewline |
|
1194 neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1195 neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1196 \isanewline |
|
1197 inverse{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1198 inverse{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\ negate\ i{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1199 \isanewline |
|
1200 mult{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1201 mult{\isaliteral{5F}{\isacharunderscore}}int\ i\ j\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{2B}{\isacharplus}}\ j{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1202 \isanewline |
|
1203 instance\ Semigroup\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1204 \ \ mult\ {\isaliteral{3D}{\isacharequal}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1205 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1206 \isanewline |
|
1207 instance\ Monoidl\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1208 \ \ neutral\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1209 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1210 \isanewline |
|
1211 instance\ Monoid\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1212 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1213 \isanewline |
|
1214 instance\ Group\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1215 \ \ inverse\ {\isaliteral{3D}{\isacharequal}}\ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1216 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1217 \isanewline |
|
1218 pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Monoid\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1219 pow{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ x\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1220 pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ mult\ x\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ n\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1221 \isanewline |
|
1222 pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Group\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1223 pow{\isaliteral{5F}{\isacharunderscore}}int\ k\ x\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1224 \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ k\ then\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ k{\isaliteral{29}{\isacharparenright}}\ x\isanewline |
|
1225 \ \ \ \ else\ inverse\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{28}{\isacharparenleft}}negate\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1226 \isanewline |
|
1227 example\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1228 example\ {\isaliteral{3D}{\isacharequal}}\ pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isadigit{1}}{\isadigit{0}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1229 \isanewline |
|
1230 {\isaliteral{7D}{\isacharbraceright}}\isanewline% |
|
1231 \end{isamarkuptext}% |
|
1232 \isamarkuptrue% |
|
1233 % |
|
1234 \endisatagquotetypewriter |
|
1235 {\isafoldquotetypewriter}% |
|
1236 % |
|
1237 \isadelimquotetypewriter |
|
1238 % |
|
1239 \endisadelimquotetypewriter |
|
1240 % |
|
1241 \begin{isamarkuptext}% |
|
1242 \noindent The code in SML has explicit dictionary passing:% |
|
1243 \end{isamarkuptext}% |
|
1244 \isamarkuptrue% |
|
1245 % |
|
1246 \isadelimquotetypewriter |
|
1247 % |
|
1248 \endisadelimquotetypewriter |
|
1249 % |
|
1250 \isatagquotetypewriter |
|
1251 % |
|
1252 \begin{isamarkuptext}% |
|
1253 structure\ Example\ {\isaliteral{3A}{\isacharcolon}}\ sig\isanewline |
|
1254 \ \ datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat\isanewline |
|
1255 \ \ datatype\ num\ {\isaliteral{3D}{\isacharequal}}\ One\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{0}}\ of\ num\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{1}}\ of\ num\isanewline |
|
1256 \ \ val\ apsnd\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}c\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}c\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}b\isanewline |
|
1257 \ \ val\ sgn{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline |
|
1258 \ \ val\ abs{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline |
|
1259 \ \ val\ divmod{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2A}{\isacharasterisk}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline |
|
1260 \ \ val\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\isanewline |
|
1261 \ \ val\ nat\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\isanewline |
|
1262 \ \ type\ {\isaliteral{27}{\isacharprime}}a\ semigroup\isanewline |
|
1263 \ \ val\ mult\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline |
|
1264 \ \ type\ {\isaliteral{27}{\isacharprime}}a\ monoidl\isanewline |
|
1265 \ \ val\ semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup\isanewline |
|
1266 \ \ val\ neutral\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline |
|
1267 \ \ type\ {\isaliteral{27}{\isacharprime}}a\ monoid\isanewline |
|
1268 \ \ val\ monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl\isanewline |
|
1269 \ \ type\ {\isaliteral{27}{\isacharprime}}a\ group\isanewline |
|
1270 \ \ val\ monoid{\isaliteral{5F}{\isacharunderscore}}group\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\isanewline |
|
1271 \ \ val\ inverse\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline |
|
1272 \ \ val\ neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline |
|
1273 \ \ val\ inverse{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline |
|
1274 \ \ val\ mult{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline |
|
1275 \ \ val\ semigroup{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ semigroup\isanewline |
|
1276 \ \ val\ monoidl{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ monoidl\isanewline |
|
1277 \ \ val\ monoid{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ monoid\isanewline |
|
1278 \ \ val\ group{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ group\isanewline |
|
1279 \ \ val\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline |
|
1280 \ \ val\ pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline |
|
1281 \ \ val\ example\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline |
|
1282 end\ {\isaliteral{3D}{\isacharequal}}\ struct\isanewline |
|
1283 \isanewline |
|
1284 datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1285 \isanewline |
|
1286 datatype\ num\ {\isaliteral{3D}{\isacharequal}}\ One\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{0}}\ of\ num\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{1}}\ of\ num{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1287 \isanewline |
|
1288 fun\ apsnd\ f\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ f\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1289 \isanewline |
|
1290 fun\ sgn{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1291 \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ {\isadigit{0}}\isanewline |
|
1292 \ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}if\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ i{\isaliteral{29}{\isacharparenright}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1293 \ \ \ \ \ \ \ \ \ \ \ else\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1294 \isanewline |
|
1295 fun\ abs{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\ i\ else\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1296 \isanewline |
|
1297 fun\ divmod{\isaliteral{5F}{\isacharunderscore}}int\ k\ l\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1298 \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1299 \ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}l\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1300 \ \ \ \ \ \ \ \ \ \ \ else\ apsnd\ {\isaliteral{28}{\isacharparenleft}}fn\ a\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}sgn{\isaliteral{5F}{\isacharunderscore}}int\ l{\isaliteral{2C}{\isacharcomma}}\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1301 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}sgn{\isaliteral{5F}{\isacharunderscore}}int\ k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}sgn{\isaliteral{5F}{\isacharunderscore}}int\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1302 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ then\ IntInf{\isaliteral{2E}{\isachardot}}divMod\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}abs\ k{\isaliteral{2C}{\isacharcomma}}\ IntInf{\isaliteral{2E}{\isachardot}}abs\ l{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1303 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ let\isanewline |
|
1304 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}r{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1305 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ IntInf{\isaliteral{2E}{\isachardot}}divMod\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}abs\ k{\isaliteral{2C}{\isacharcomma}}\ IntInf{\isaliteral{2E}{\isachardot}}abs\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1306 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ in\isanewline |
|
1307 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\ r{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1308 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\isanewline |
|
1309 \ \ \ \ \ \ \ \ \ \ r{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
|
1310 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}abs{\isaliteral{5F}{\isacharunderscore}}int\ l{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1311 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ end{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1312 \isanewline |
|
1313 fun\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ m\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1314 \ \ {\isaliteral{7C}{\isacharbar}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1315 \isanewline |
|
1316 fun\ nat\ k\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1317 \ \ {\isaliteral{28}{\isacharparenleft}}if\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\isanewline |
|
1318 \ \ \ \ else\ let\isanewline |
|
1319 \ \ \ \ \ \ \ \ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ divmod{\isaliteral{5F}{\isacharunderscore}}int\ k\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1320 \ \ \ \ \ \ \ \ \ \ \ val\ n\ {\isaliteral{3D}{\isacharequal}}\ nat\ l{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1321 \ \ \ \ \ \ \ \ \ \ \ val\ la\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ n\ n{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1322 \ \ \ \ \ \ \ \ \ in\isanewline |
|
1323 \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}j\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ la\ else\ Suc\ la{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1324 \ \ \ \ \ \ \ \ \ end{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1325 \isanewline |
|
1326 type\ {\isaliteral{27}{\isacharprime}}a\ semigroup\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}mult\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1327 val\ mult\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}mult\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1328 \isanewline |
|
1329 type\ {\isaliteral{27}{\isacharprime}}a\ monoidl\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup{\isaliteral{2C}{\isacharcomma}}\ neutral\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1330 val\ semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1331 val\ neutral\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}neutral\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1332 \isanewline |
|
1333 type\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1334 val\ monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1335 \isanewline |
|
1336 type\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid{\isaliteral{2C}{\isacharcomma}}\ inverse\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1337 val\ monoid{\isaliteral{5F}{\isacharunderscore}}group\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ monoid{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1338 val\ inverse\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}inverse\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1339 \isanewline |
|
1340 val\ neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1341 \isanewline |
|
1342 fun\ inverse{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\ i{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1343 \isanewline |
|
1344 fun\ mult{\isaliteral{5F}{\isacharunderscore}}int\ i\ j\ {\isaliteral{3D}{\isacharequal}}\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1345 \isanewline |
|
1346 val\ semigroup{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}mult\ {\isaliteral{3D}{\isacharequal}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ semigroup{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1347 \isanewline |
|
1348 val\ monoidl{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1349 \ \ {\isaliteral{7B}{\isacharbraceleft}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ {\isaliteral{3D}{\isacharequal}}\ semigroup{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{2C}{\isacharcomma}}\ neutral\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\isanewline |
|
1350 \ \ IntInf{\isaliteral{2E}{\isachardot}}int\ monoidl{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1351 \isanewline |
|
1352 val\ monoid{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3D}{\isacharequal}}\ monoidl{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ monoid{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1353 \isanewline |
|
1354 val\ group{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ {\isaliteral{3D}{\isacharequal}}\ monoid{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{2C}{\isacharcomma}}\ inverse\ {\isaliteral{3D}{\isacharequal}}\ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\isanewline |
|
1355 \ \ IntInf{\isaliteral{2E}{\isachardot}}int\ group{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1356 \isanewline |
|
1357 fun\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ A{\isaliteral{5F}{\isacharunderscore}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ x\ {\isaliteral{3D}{\isacharequal}}\ neutral\ {\isaliteral{28}{\isacharparenleft}}monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ A{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1358 \ \ {\isaliteral{7C}{\isacharbar}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ A{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1359 \ \ \ \ mult\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ o\ monoidl{\isaliteral{5F}{\isacharunderscore}}monoid{\isaliteral{29}{\isacharparenright}}\ A{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ A{\isaliteral{5F}{\isacharunderscore}}\ n\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1360 \isanewline |
|
1361 fun\ pow{\isaliteral{5F}{\isacharunderscore}}int\ A{\isaliteral{5F}{\isacharunderscore}}\ k\ x\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1362 \ \ {\isaliteral{28}{\isacharparenleft}}if\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\ then\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ A{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}nat\ k{\isaliteral{29}{\isacharparenright}}\ x\isanewline |
|
1363 \ \ \ \ else\ inverse\ A{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ A{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1364 \isanewline |
|
1365 val\ example\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1366 \ \ pow{\isaliteral{5F}{\isacharunderscore}}int\ group{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{7E}{\isachartilde}}{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1367 \isanewline |
|
1368 end{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}struct\ Example{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline% |
|
1369 \end{isamarkuptext}% |
|
1370 \isamarkuptrue% |
|
1371 % |
|
1372 \endisatagquotetypewriter |
|
1373 {\isafoldquotetypewriter}% |
|
1374 % |
|
1375 \isadelimquotetypewriter |
|
1376 % |
|
1377 \endisadelimquotetypewriter |
|
1378 % |
|
1379 \begin{isamarkuptext}% |
|
1380 \noindent In Scala, implicts are used as dictionaries:% |
|
1381 \end{isamarkuptext}% |
|
1382 \isamarkuptrue% |
|
1383 % |
|
1384 \isadeliminvisible |
|
1385 % |
|
1386 \endisadeliminvisible |
|
1387 % |
|
1388 \isataginvisible |
|
1389 % |
|
1390 \endisataginvisible |
|
1391 {\isafoldinvisible}% |
|
1392 % |
|
1393 \isadeliminvisible |
|
1394 % |
|
1395 \endisadeliminvisible |
|
1396 % |
|
1397 \isadelimquotetypewriter |
|
1398 % |
|
1399 \endisadelimquotetypewriter |
|
1400 % |
|
1401 \isatagquotetypewriter |
|
1402 % |
|
1403 \begin{isamarkuptext}% |
|
1404 object\ Example\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1405 \isanewline |
|
1406 abstract\ sealed\ class\ nat\isanewline |
|
1407 final\ case\ object\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ extends\ nat\isanewline |
|
1408 final\ case\ class\ Suc{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{29}{\isacharparenright}}\ extends\ nat\isanewline |
|
1409 \isanewline |
|
1410 abstract\ sealed\ class\ num\isanewline |
|
1411 final\ case\ object\ One\ extends\ num\isanewline |
|
1412 final\ case\ class\ Bit{\isadigit{0}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ num{\isaliteral{29}{\isacharparenright}}\ extends\ num\isanewline |
|
1413 final\ case\ class\ Bit{\isadigit{1}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ num{\isaliteral{29}{\isacharparenright}}\ extends\ num\isanewline |
|
1414 \isanewline |
|
1415 def\ apsnd{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{2C}{\isacharcomma}}\ B{\isaliteral{2C}{\isacharcomma}}\ C{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}f{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ B{\isaliteral{2C}{\isacharcomma}}\ x{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}C{\isaliteral{2C}{\isacharcomma}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}C{\isaliteral{2C}{\isacharcomma}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}f{\isaliteral{2C}{\isacharcomma}}\ x{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ match\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1416 \ \ case\ {\isaliteral{28}{\isacharparenleft}}f{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ f{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1417 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
|
1418 \isanewline |
|
1419 def\ sgn{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1420 \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1421 \ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ i{\isaliteral{29}{\isacharparenright}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ else\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1422 \isanewline |
|
1423 def\ abs{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{3C}{\isacharless}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ i{\isaliteral{29}{\isacharparenright}}\ else\ i{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1424 \isanewline |
|
1425 def\ divmod{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ l{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1426 \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1427 \ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}l\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1428 \ \ \ \ \ \ \ \ \ \ \ else\ apsnd{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\isanewline |
|
1429 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ BigInt{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ sgn{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ a{\isaliteral{2C}{\isacharcomma}}\isanewline |
|
1430 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}sgn{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ sgn{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1431 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline |
|
1432 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ if\ {\isaliteral{28}{\isacharparenleft}}l\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\ else\isanewline |
|
1433 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2E}{\isachardot}}abs\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{25}{\isacharpercent}}\ l{\isaliteral{2E}{\isachardot}}abs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}apply{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}apply{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1434 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1435 \ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}r{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1436 \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ if\ {\isaliteral{28}{\isacharparenleft}}l\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\ else\isanewline |
|
1437 \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2E}{\isachardot}}abs\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{25}{\isacharpercent}}\ l{\isaliteral{2E}{\isachardot}}abs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}apply{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}apply{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1438 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ r{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1439 \ \ \ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ r{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ abs{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1440 \ \ {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1441 \isanewline |
|
1442 def\ plus{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{28}{\isacharparenleft}}x{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{29}{\isacharparenright}}\ match\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1443 \ \ case\ {\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}m{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{28}{\isacharparenleft}}m{\isaliteral{2C}{\isacharcomma}}\ Suc{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1444 \ \ case\ {\isaliteral{28}{\isacharparenleft}}Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ n\isanewline |
|
1445 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
|
1446 \isanewline |
|
1447 def\ nat{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1448 \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\isanewline |
|
1449 \ \ \ \ else\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1450 \ \ \ \ \ \ \ \ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ divmod{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1451 \ \ \ \ \ \ \ \ \ \ \ val\ n{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\ nat{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1452 \ \ \ \ \ \ \ \ \ \ \ val\ la{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
1453 \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}j\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ la\ else\ Suc{\isaliteral{28}{\isacharparenleft}}la{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1454 \ \ \ \ \ \ \ \ \ {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1455 \isanewline |
|
1456 trait\ semigroup{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1457 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}A{\isaliteral{2C}{\isacharcomma}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ A\isanewline |
|
1458 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
|
1459 def\ mult{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{28}{\isacharparenleft}}implicit\ A{\isaliteral{3A}{\isacharcolon}}\ semigroup{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1460 \ \ A{\isaliteral{2E}{\isachardot}}{\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1461 \isanewline |
|
1462 trait\ monoidl{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ semigroup{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1463 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}{\isaliteral{3A}{\isacharcolon}}\ A\isanewline |
|
1464 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
|
1465 def\ neutral{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}implicit\ A{\isaliteral{3A}{\isacharcolon}}\ monoidl{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2E}{\isachardot}}{\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}\isanewline |
|
1466 \isanewline |
|
1467 trait\ monoid{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ monoidl{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1468 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
|
1469 \isanewline |
|
1470 trait\ group{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ monoid{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1471 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{60}{\isacharbackquote}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ A\isanewline |
|
1472 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
|
1473 def\ inverse{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{28}{\isacharparenleft}}implicit\ A{\isaliteral{3A}{\isacharcolon}}\ group{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2E}{\isachardot}}{\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{60}{\isacharbackquote}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1474 \isanewline |
|
1475 def\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1476 \isanewline |
|
1477 def\ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ i{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1478 \isanewline |
|
1479 def\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{2B}{\isacharplus}}\ j\isanewline |
|
1480 \isanewline |
|
1481 implicit\ def\ semigroup{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ semigroup{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ new\ semigroup{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1482 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1483 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
|
1484 \isanewline |
|
1485 implicit\ def\ monoidl{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ monoidl{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ new\ monoidl{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1486 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int\isanewline |
|
1487 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1488 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
|
1489 \isanewline |
|
1490 implicit\ def\ monoid{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ monoid{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ new\ monoid{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1491 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int\isanewline |
|
1492 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1493 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
|
1494 \isanewline |
|
1495 implicit\ def\ group{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ group{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ new\ group{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1496 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1497 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int\isanewline |
|
1498 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1499 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
|
1500 \isanewline |
|
1501 def\ pow{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5B}{\isacharbrackleft}}A\ {\isaliteral{3A}{\isacharcolon}}\ monoid{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}xa{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}xa{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ match\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
1502 \ \ case\ {\isaliteral{28}{\isacharparenleft}}Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ neutral{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\isanewline |
|
1503 \ \ case\ {\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1504 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
|
1505 \isanewline |
|
1506 def\ pow{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5B}{\isacharbrackleft}}A\ {\isaliteral{3A}{\isacharcolon}}\ group{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1507 \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{29}{\isacharparenright}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}nat{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1508 \ \ \ \ else\ inverse{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}nat{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1509 \isanewline |
|
1510 def\ example{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ pow{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1511 \isanewline |
|
1512 {\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{2A}{\isacharasterisk}}\ object\ Example\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2F}{\isacharslash}}\isanewline% |
|
1513 \end{isamarkuptext}% |
|
1514 \isamarkuptrue% |
|
1515 % |
|
1516 \endisatagquotetypewriter |
|
1517 {\isafoldquotetypewriter}% |
|
1518 % |
|
1519 \isadelimquotetypewriter |
|
1520 % |
|
1521 \endisadelimquotetypewriter |
|
1522 % |
|
1523 \isamarkupsubsection{Inspecting the type class universe% |
|
1524 } |
|
1525 \isamarkuptrue% |
|
1526 % |
|
1527 \begin{isamarkuptext}% |
|
1528 To facilitate orientation in complex subclass structures, two |
|
1529 diagnostics commands are provided: |
|
1530 |
|
1531 \begin{description} |
|
1532 |
|
1533 \item[\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}classes}}}}] print a list of all classes |
|
1534 together with associated operations etc. |
|
1535 |
|
1536 \item[\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}}] visualizes the subclass relation |
|
1537 between all classes as a Hasse diagram. |
|
1538 |
|
1539 \end{description}% |
|
1540 \end{isamarkuptext}% |
|
1541 \isamarkuptrue% |
|
1542 % |
|
1543 \isadelimtheory |
|
1544 % |
|
1545 \endisadelimtheory |
|
1546 % |
|
1547 \isatagtheory |
|
1548 \isacommand{end}\isamarkupfalse% |
|
1549 % |
|
1550 \endisatagtheory |
|
1551 {\isafoldtheory}% |
|
1552 % |
|
1553 \isadelimtheory |
|
1554 % |
|
1555 \endisadelimtheory |
|
1556 \isanewline |
|
1557 \end{isabellebody}% |
|
1558 %%% Local Variables: |
|
1559 %%% mode: latex |
|
1560 %%% TeX-master: "root" |
|
1561 %%% End: |
|