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