8890
|
1 |
\begin{isabelle}%
|
8903
|
2 |
%
|
|
3 |
\isamarkupheader{Basic group theory}
|
|
4 |
\isacommand{theory}~Group~=~Main:%
|
|
5 |
\begin{isamarkuptext}%
|
8907
|
6 |
\medskip\noindent The meta-type system of Isabelle supports
|
8903
|
7 |
\emph{intersections} and \emph{inclusions} of type classes. These
|
|
8 |
directly correspond to intersections and inclusions of type
|
|
9 |
predicates in a purely set theoretic sense. This is sufficient as a
|
|
10 |
means to describe simple hierarchies of structures. As an
|
|
11 |
illustration, we use the well-known example of semigroups, monoids,
|
8907
|
12 |
general groups and Abelian groups.%
|
8903
|
13 |
\end{isamarkuptext}%
|
|
14 |
%
|
|
15 |
\isamarkupsubsection{Monoids and Groups}
|
|
16 |
%
|
|
17 |
\begin{isamarkuptext}%
|
|
18 |
First we declare some polymorphic constants required later for the
|
|
19 |
signature parts of our structures.%
|
|
20 |
\end{isamarkuptext}%
|
8890
|
21 |
\isacommand{consts}\isanewline
|
|
22 |
~~times~::~{"}'a~=>~'a~=>~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)\isanewline
|
|
23 |
~~inverse~::~{"}'a~=>~'a{"}~~~~~~~~({"}(\_{\isasyminv}){"}~[1000]~999)\isanewline
|
8903
|
24 |
~~one~::~'a~~~~~~~~~~~~~~~~~~~~({"}{\isasymunit}{"})%
|
|
25 |
\begin{isamarkuptext}%
|
|
26 |
\noindent Next we define class $monoid$ of monoids with operations
|
|
27 |
$\TIMES$ and $1$. Note that multiple class axioms are allowed for
|
|
28 |
user convenience --- they simply represent the conjunction of their
|
|
29 |
respective universal closures.%
|
|
30 |
\end{isamarkuptext}%
|
8890
|
31 |
\isacommand{axclass}\isanewline
|
|
32 |
~~monoid~<~{"}term{"}\isanewline
|
|
33 |
~~assoc:~~~~~~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
|
|
34 |
~~left\_unit:~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
|
8903
|
35 |
~~right\_unit:~{"}x~{\isasymOtimes}~{\isasymunit}~=~x{"}%
|
|
36 |
\begin{isamarkuptext}%
|
|
37 |
\noindent So class $monoid$ contains exactly those types $\tau$ where
|
|
38 |
$\TIMES :: \tau \To \tau \To \tau$ and $1 :: \tau$ are specified
|
|
39 |
appropriately, such that $\TIMES$ is associative and $1$ is a left
|
|
40 |
and right unit element for $\TIMES$.%
|
|
41 |
\end{isamarkuptext}%
|
|
42 |
%
|
|
43 |
\begin{isamarkuptext}%
|
|
44 |
\medskip Independently of $monoid$, we now define a linear hierarchy
|
8907
|
45 |
of semigroups, general groups and Abelian groups. Note that the
|
|
46 |
names of class axioms are automatically qualified with each class
|
|
47 |
name, so we may re-use common names such as $assoc$.%
|
8903
|
48 |
\end{isamarkuptext}%
|
8890
|
49 |
\isacommand{axclass}\isanewline
|
|
50 |
~~semigroup~<~{"}term{"}\isanewline
|
|
51 |
~~assoc:~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
|
|
52 |
\isanewline
|
|
53 |
\isacommand{axclass}\isanewline
|
|
54 |
~~group~<~semigroup\isanewline
|
|
55 |
~~left\_unit:~~~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
|
8907
|
56 |
~~left\_inverse:~{"}x{\isasyminv}~{\isasymOtimes}~x~=~{\isasymunit}{"}\isanewline
|
8903
|
57 |
\isanewline
|
|
58 |
\isacommand{axclass}\isanewline
|
|
59 |
~~agroup~<~group\isanewline
|
|
60 |
~~commute:~{"}x~{\isasymOtimes}~y~=~y~{\isasymOtimes}~x{"}%
|
|
61 |
\begin{isamarkuptext}%
|
|
62 |
\noindent Class $group$ inherits associativity of $\TIMES$ from
|
8907
|
63 |
$semigroup$ and adds two further group axioms. Similarly, $agroup$
|
8903
|
64 |
is defined as the subset of $group$ such that for all of its elements
|
|
65 |
$\tau$, the operation $\TIMES :: \tau \To \tau \To \tau$ is even
|
|
66 |
commutative.%
|
|
67 |
\end{isamarkuptext}%
|
|
68 |
%
|
|
69 |
\isamarkupsubsection{Abstract reasoning}
|
|
70 |
%
|
8890
|
71 |
\begin{isamarkuptext}%
|
8903
|
72 |
In a sense, axiomatic type classes may be viewed as \emph{abstract
|
|
73 |
theories}. Above class definitions gives rise to abstract axioms
|
8907
|
74 |
$assoc$, $left_unit$, $left_inverse$, $commute$, where any of these
|
|
75 |
contain a type variable $\alpha :: c$ that is restricted to types of
|
8903
|
76 |
the corresponding class $c$. \emph{Sort constraints} like this
|
|
77 |
express a logical precondition for the whole formula. For example,
|
|
78 |
$assoc$ states that for all $\tau$, provided that $\tau ::
|
|
79 |
semigroup$, the operation $\TIMES :: \tau \To \tau \To \tau$ is
|
|
80 |
associative.
|
|
81 |
|
|
82 |
\medskip From a technical point of view, abstract axioms are just
|
|
83 |
ordinary Isabelle theorems, which may be used in proofs without
|
|
84 |
special treatment. Such ``abstract proofs'' usually yield new
|
|
85 |
``abstract theorems''. For example, we may now derive the following
|
8907
|
86 |
well-known laws of general groups.%
|
8890
|
87 |
\end{isamarkuptext}%
|
8903
|
88 |
\isacommand{theorem}~group\_right\_inverse:~{"}x~{\isasymOtimes}~x{\isasyminv}~=~({\isasymunit}{\isasymColon}'a{\isasymColon}group){"}\isanewline
|
8890
|
89 |
\isacommand{proof}~-\isanewline
|
|
90 |
~~\isacommand{have}~{"}x~{\isasymOtimes}~x{\isasyminv}~=~{\isasymunit}~{\isasymOtimes}~(x~{\isasymOtimes}~x{\isasyminv}){"}\isanewline
|
|
91 |
~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline
|
8907
|
92 |
~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}~{\isasymOtimes}~x~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
|
8890
|
93 |
~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
|
|
94 |
~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~x{\isasyminv}~{\isasymOtimes}~x~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
|
|
95 |
~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
|
|
96 |
~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~(x{\isasyminv}~{\isasymOtimes}~x)~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
|
|
97 |
~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
|
|
98 |
~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~{\isasymunit}~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
|
|
99 |
~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
|
|
100 |
~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~({\isasymunit}~{\isasymOtimes}~x{\isasyminv}){"}\isanewline
|
|
101 |
~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
|
|
102 |
~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
|
|
103 |
~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline
|
|
104 |
~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}{"}\isanewline
|
|
105 |
~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
|
|
106 |
~~\isacommand{finally}~\isacommand{show}~?thesis~\isacommand{.}\isanewline
|
|
107 |
\isacommand{qed}%
|
|
108 |
\begin{isamarkuptext}%
|
8903
|
109 |
\noindent With $group_right_inverse$ already available,
|
8890
|
110 |
$group_right_unit$\label{thm:group-right-unit} is now established
|
|
111 |
much easier.%
|
|
112 |
\end{isamarkuptext}%
|
8903
|
113 |
\isacommand{theorem}~group\_right\_unit:~{"}x~{\isasymOtimes}~{\isasymunit}~=~(x{\isasymColon}'a{\isasymColon}group){"}\isanewline
|
8890
|
114 |
\isacommand{proof}~-\isanewline
|
|
115 |
~~\isacommand{have}~{"}x~{\isasymOtimes}~{\isasymunit}~=~x~{\isasymOtimes}~(x{\isasyminv}~{\isasymOtimes}~x){"}\isanewline
|
|
116 |
~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
|
|
117 |
~~\isacommand{also}~\isacommand{have}~{"}...~=~x~{\isasymOtimes}~x{\isasyminv}~{\isasymOtimes}~x{"}\isanewline
|
|
118 |
~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
|
|
119 |
~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}~{\isasymOtimes}~x{"}\isanewline
|
|
120 |
~~~~\isacommand{by}~(simp~only:~group\_right\_inverse)\isanewline
|
|
121 |
~~\isacommand{also}~\isacommand{have}~{"}...~=~x{"}\isanewline
|
|
122 |
~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline
|
|
123 |
~~\isacommand{finally}~\isacommand{show}~?thesis~\isacommand{.}\isanewline
|
8903
|
124 |
\isacommand{qed}%
|
|
125 |
\begin{isamarkuptext}%
|
|
126 |
\medskip Abstract theorems may be instantiated to only those types
|
|
127 |
$\tau$ where the appropriate class membership $\tau :: c$ is known at
|
|
128 |
Isabelle's type signature level. Since we have $agroup \subseteq
|
|
129 |
group \subseteq semigroup$ by definition, all theorems of $semigroup$
|
|
130 |
and $group$ are automatically inherited by $group$ and $agroup$.%
|
|
131 |
\end{isamarkuptext}%
|
|
132 |
%
|
|
133 |
\isamarkupsubsection{Abstract instantiation}
|
|
134 |
%
|
|
135 |
\begin{isamarkuptext}%
|
|
136 |
From the definition, the $monoid$ and $group$ classes have been
|
|
137 |
independent. Note that for monoids, $right_unit$ had to be included
|
|
138 |
as an axiom, but for groups both $right_unit$ and $right_inverse$ are
|
|
139 |
derivable from the other axioms. With $group_right_unit$ derived as
|
|
140 |
a theorem of group theory (see page~\pageref{thm:group-right-unit}),
|
8907
|
141 |
we may now instantiate $monoid \subseteq semigroup$ and $group
|
|
142 |
\subseteq monoid$ properly as follows
|
8903
|
143 |
(cf.\ \figref{fig:monoid-group}).
|
|
144 |
|
|
145 |
\begin{figure}[htbp]
|
|
146 |
\begin{center}
|
|
147 |
\small
|
|
148 |
\unitlength 0.6mm
|
|
149 |
\begin{picture}(65,90)(0,-10)
|
|
150 |
\put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
|
|
151 |
\put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}}
|
|
152 |
\put(15,5){\makebox(0,0){$agroup$}}
|
|
153 |
\put(15,25){\makebox(0,0){$group$}}
|
|
154 |
\put(15,45){\makebox(0,0){$semigroup$}}
|
|
155 |
\put(30,65){\makebox(0,0){$term$}} \put(50,45){\makebox(0,0){$monoid$}}
|
|
156 |
\end{picture}
|
|
157 |
\hspace{4em}
|
|
158 |
\begin{picture}(30,90)(0,0)
|
|
159 |
\put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
|
|
160 |
\put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}}
|
|
161 |
\put(15,5){\makebox(0,0){$agroup$}}
|
|
162 |
\put(15,25){\makebox(0,0){$group$}}
|
|
163 |
\put(15,45){\makebox(0,0){$monoid$}}
|
|
164 |
\put(15,65){\makebox(0,0){$semigroup$}}
|
|
165 |
\put(15,85){\makebox(0,0){$term$}}
|
|
166 |
\end{picture}
|
|
167 |
\caption{Monoids and groups: according to definition, and by proof}
|
|
168 |
\label{fig:monoid-group}
|
|
169 |
\end{center}
|
8907
|
170 |
\end{figure}%
|
8903
|
171 |
\end{isamarkuptext}%
|
8890
|
172 |
\isacommand{instance}~monoid~<~semigroup\isanewline
|
|
173 |
\isacommand{proof}~intro\_classes\isanewline
|
8903
|
174 |
~~\isacommand{fix}~x~y~z~::~{"}'a{\isasymColon}monoid{"}\isanewline
|
8890
|
175 |
~~\isacommand{show}~{"}x~{\isasymOtimes}~y~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
|
|
176 |
~~~~\isacommand{by}~(rule~monoid.assoc)\isanewline
|
|
177 |
\isacommand{qed}\isanewline
|
|
178 |
\isanewline
|
|
179 |
\isacommand{instance}~group~<~monoid\isanewline
|
|
180 |
\isacommand{proof}~intro\_classes\isanewline
|
8903
|
181 |
~~\isacommand{fix}~x~y~z~::~{"}'a{\isasymColon}group{"}\isanewline
|
8890
|
182 |
~~\isacommand{show}~{"}x~{\isasymOtimes}~y~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
|
|
183 |
~~~~\isacommand{by}~(rule~semigroup.assoc)\isanewline
|
|
184 |
~~\isacommand{show}~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
|
|
185 |
~~~~\isacommand{by}~(rule~group.left\_unit)\isanewline
|
|
186 |
~~\isacommand{show}~{"}x~{\isasymOtimes}~{\isasymunit}~=~x{"}\isanewline
|
|
187 |
~~~~\isacommand{by}~(rule~group\_right\_unit)\isanewline
|
8903
|
188 |
\isacommand{qed}%
|
|
189 |
\begin{isamarkuptext}%
|
|
190 |
\medskip The $\isakeyword{instance}$ command sets up an appropriate
|
8907
|
191 |
goal that represents the class inclusion (or type arity, see
|
|
192 |
\secref{sec:inst-arity}) to be proven
|
8903
|
193 |
(see also \cite{isabelle-isar-ref}). The $intro_classes$ proof
|
|
194 |
method does back-chaining of class membership statements wrt.\ the
|
|
195 |
hierarchy of any classes defined in the current theory; the effect is
|
8907
|
196 |
to reduce to the initial statement to a number of goals that directly
|
|
197 |
correspond to any class axioms encountered on the path upwards
|
|
198 |
through the class hierarchy.
|
|
199 |
|
|
200 |
any logical class axioms as subgoals.%
|
8903
|
201 |
\end{isamarkuptext}%
|
|
202 |
%
|
8907
|
203 |
\isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}}
|
8903
|
204 |
%
|
|
205 |
\begin{isamarkuptext}%
|
|
206 |
So far we have covered the case of the form
|
|
207 |
$\isakeyword{instance}~c@1 < c@2$, namely \emph{abstract
|
|
208 |
instantiation} --- $c@1$ is more special than $c@2$ and thus an
|
|
209 |
instance of $c@2$. Even more interesting for practical applications
|
|
210 |
are \emph{concrete instantiations} of axiomatic type classes. That
|
|
211 |
is, certain simple schemes $(\alpha@1, \ldots, \alpha@n)t :: c$ of
|
|
212 |
class membership may be established at the logical level and then
|
|
213 |
transferred to Isabelle's type signature level.
|
|
214 |
|
8907
|
215 |
\medskip As a typical example, we show that type $bool$ with
|
|
216 |
exclusive-or as operation $\TIMES$, identity as $\isasyminv$, and
|
|
217 |
$False$ as $1$ forms an Abelian group.%
|
8903
|
218 |
\end{isamarkuptext}%
|
8890
|
219 |
\isacommand{defs}\isanewline
|
|
220 |
~~times\_bool\_def:~~~{"}x~{\isasymOtimes}~y~{\isasymequiv}~x~{\isasymnoteq}~(y{\isasymColon}bool){"}\isanewline
|
|
221 |
~~inverse\_bool\_def:~{"}x{\isasyminv}~{\isasymequiv}~x{\isasymColon}bool{"}\isanewline
|
8903
|
222 |
~~unit\_bool\_def:~~~~{"}{\isasymunit}~{\isasymequiv}~False{"}%
|
|
223 |
\begin{isamarkuptext}%
|
|
224 |
\medskip It is important to note that above $\DEFS$ are just
|
8907
|
225 |
overloaded meta-level constant definitions, where type classes are
|
|
226 |
not yet involved at all. This form of constant definition with
|
|
227 |
overloading (and optional recursion over the syntactic structure of
|
|
228 |
simple types) are admissible as definitional extensions of plain HOL
|
|
229 |
\cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not
|
|
230 |
required for overloading. Nevertheless, overloaded definitions are
|
8903
|
231 |
best applied in the context of type classes.
|
|
232 |
|
|
233 |
\medskip Since we have chosen above $\DEFS$ of the generic group
|
|
234 |
operations on type $bool$ appropriately, the class membership $bool
|
|
235 |
:: agroup$ may be now derived as follows.%
|
|
236 |
\end{isamarkuptext}%
|
8890
|
237 |
\isacommand{instance}~bool~::~agroup\isanewline
|
|
238 |
\isacommand{proof}~(intro\_classes,\isanewline
|
|
239 |
~~~~unfold~times\_bool\_def~inverse\_bool\_def~unit\_bool\_def)\isanewline
|
8907
|
240 |
~~\isacommand{fix}~x~y~z\isanewline
|
8890
|
241 |
~~\isacommand{show}~{"}((x~{\isasymnoteq}~y)~{\isasymnoteq}~z)~=~(x~{\isasymnoteq}~(y~{\isasymnoteq}~z)){"}~\isacommand{by}~blast\isanewline
|
|
242 |
~~\isacommand{show}~{"}(False~{\isasymnoteq}~x)~=~x{"}~\isacommand{by}~blast\isanewline
|
|
243 |
~~\isacommand{show}~{"}(x~{\isasymnoteq}~x)~=~False{"}~\isacommand{by}~blast\isanewline
|
|
244 |
~~\isacommand{show}~{"}(x~{\isasymnoteq}~y)~=~(y~{\isasymnoteq}~x){"}~\isacommand{by}~blast\isanewline
|
8903
|
245 |
\isacommand{qed}%
|
|
246 |
\begin{isamarkuptext}%
|
8907
|
247 |
The result of an $\isakeyword{instance}$ statement is both expressed
|
|
248 |
as a theorem of Isabelle's meta-logic, and as a type arity of the
|
|
249 |
type signature. The latter enables type-inference system to take
|
|
250 |
care of this new instance automatically.
|
8903
|
251 |
|
8907
|
252 |
\medskip We could now also instantiate our group theory classes to
|
|
253 |
many other concrete types. For example, $int :: agroup$ (e.g.\ by
|
|
254 |
defining $\TIMES$ as addition, $\isasyminv$ as negation and $1$ as
|
|
255 |
zero) or $list :: (term)semigroup$ (e.g.\ if $\TIMES$ is defined as
|
|
256 |
list append). Thus, the characteristic constants $\TIMES$,
|
|
257 |
$\isasyminv$, $1$ really become overloaded, i.e.\ have different
|
|
258 |
meanings on different types.%
|
8903
|
259 |
\end{isamarkuptext}%
|
|
260 |
%
|
|
261 |
\isamarkupsubsection{Lifting and Functors}
|
|
262 |
%
|
|
263 |
\begin{isamarkuptext}%
|
|
264 |
As already mentioned above, overloading in the simply-typed HOL
|
|
265 |
systems may include recursion over the syntactic structure of types.
|
|
266 |
That is, definitional equations $c^\tau \equiv t$ may also contain
|
|
267 |
constants of name $c$ on the right-hand side --- if these have types
|
|
268 |
that are structurally simpler than $\tau$.
|
|
269 |
|
|
270 |
This feature enables us to \emph{lift operations}, say to Cartesian
|
|
271 |
products, direct sums or function spaces. Subsequently we lift
|
8907
|
272 |
$\TIMES$ component-wise to binary products $\alpha \times \beta$.%
|
8903
|
273 |
\end{isamarkuptext}%
|
8890
|
274 |
\isacommand{defs}\isanewline
|
8907
|
275 |
~~times\_prod\_def:~{"}p~{\isasymOtimes}~q~{\isasymequiv}~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q){"}%
|
8903
|
276 |
\begin{isamarkuptext}%
|
8907
|
277 |
It is very easy to see that associativity of $\TIMES^\alpha$ and
|
8903
|
278 |
$\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence
|
|
279 |
the binary type constructor $\times$ maps semigroups to semigroups.
|
|
280 |
This may be established formally as follows.%
|
|
281 |
\end{isamarkuptext}%
|
8890
|
282 |
\isacommand{instance}~*~::~(semigroup,~semigroup)~semigroup\isanewline
|
8907
|
283 |
\isacommand{proof}~(intro\_classes,~unfold~times\_prod\_def)\isanewline
|
|
284 |
~~\isacommand{fix}~p~q~r~::~{"}'a{\isasymColon}semigroup~{\isasymtimes}~'b{\isasymColon}semigroup{"}\isanewline
|
8890
|
285 |
~~\isacommand{show}\isanewline
|
|
286 |
~~~~{"}(fst~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q)~{\isasymOtimes}~fst~r,\isanewline
|
|
287 |
~~~~~~snd~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q)~{\isasymOtimes}~snd~r)~=\isanewline
|
|
288 |
~~~~~~~(fst~p~{\isasymOtimes}~fst~(fst~q~{\isasymOtimes}~fst~r,~snd~q~{\isasymOtimes}~snd~r),\isanewline
|
|
289 |
~~~~~~~~snd~p~{\isasymOtimes}~snd~(fst~q~{\isasymOtimes}~fst~r,~snd~q~{\isasymOtimes}~snd~r)){"}\isanewline
|
|
290 |
~~~~\isacommand{by}~(simp~add:~semigroup.assoc)\isanewline
|
8903
|
291 |
\isacommand{qed}%
|
|
292 |
\begin{isamarkuptext}%
|
|
293 |
Thus, if we view class instances as ``structures'', then overloaded
|
8907
|
294 |
constant definitions with recursion over types indirectly provide
|
|
295 |
some kind of ``functors'' --- i.e.\ mappings between abstract
|
8903
|
296 |
theories.%
|
|
297 |
\end{isamarkuptext}%
|
8890
|
298 |
\isacommand{end}\end{isabelle}%
|