--- a/doc-src/AxClass/generated/Group.tex Fri Aug 04 10:59:22 2000 +0200
+++ b/doc-src/AxClass/generated/Group.tex Fri Aug 04 10:59:28 2000 +0200
@@ -1,7 +1,7 @@
\begin{isabelle}%
%
\isamarkupheader{Basic group theory}
-\isacommand{theory}~Group~=~Main:%
+\isacommand{theory}\ Group\ =\ Main:%
\begin{isamarkuptext}%
\medskip\noindent The meta-type system of Isabelle supports
\emph{intersections} and \emph{inclusions} of type classes. These
@@ -19,9 +19,9 @@
signature parts of our structures.%
\end{isamarkuptext}%
\isacommand{consts}\isanewline
-~~times~::~{"}'a~=>~'a~=>~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)\isanewline
-~~inverse~::~{"}'a~=>~'a{"}~~~~~~~~({"}(\_{\isasyminv}){"}~[1000]~999)\isanewline
-~~one~::~'a~~~~~~~~~~~~~~~~~~~~({"}{\isasymunit}{"})%
+\ \ times\ ::\ {"}'a\ =>\ 'a\ =>\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOtimes}{"}\ 70)\isanewline
+\ \ inverse\ ::\ {"}'a\ =>\ 'a{"}\ \ \ \ \ \ \ \ ({"}(\_{\isasyminv}){"}\ [1000]\ 999)\isanewline
+\ \ one\ ::\ 'a\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ ({"}{\isasymunit}{"})%
\begin{isamarkuptext}%
\noindent Next we define class $monoid$ of monoids with operations
$\TIMES$ and $1$. Note that multiple class axioms are allowed for
@@ -29,15 +29,15 @@
respective universal closures.%
\end{isamarkuptext}%
\isacommand{axclass}\isanewline
-~~monoid~<~{"}term{"}\isanewline
-~~assoc:~~~~~~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
-~~left\_unit:~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
-~~right\_unit:~{"}x~{\isasymOtimes}~{\isasymunit}~=~x{"}%
+\ \ monoid\ <\ {"}term{"}\isanewline
+\ \ assoc:\ \ \ \ \ \ {"}(x\ {\isasymOtimes}\ y)\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline
+\ \ left\_unit:\ \ {"}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{"}\isanewline
+\ \ right\_unit:\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{"}%
\begin{isamarkuptext}%
\noindent So class $monoid$ contains exactly those types $\tau$ where
$\TIMES :: \tau \To \tau \To \tau$ and $1 :: \tau$ are specified
appropriately, such that $\TIMES$ is associative and $1$ is a left
- and right unit element for $\TIMES$.%
+ and right unit element for the $\TIMES$ operation.%
\end{isamarkuptext}%
%
\begin{isamarkuptext}%
@@ -47,17 +47,17 @@
name, so we may re-use common names such as $assoc$.%
\end{isamarkuptext}%
\isacommand{axclass}\isanewline
-~~semigroup~<~{"}term{"}\isanewline
-~~assoc:~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
+\ \ semigroup\ <\ {"}term{"}\isanewline
+\ \ assoc:\ {"}(x\ {\isasymOtimes}\ y)\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline
\isanewline
\isacommand{axclass}\isanewline
-~~group~<~semigroup\isanewline
-~~left\_unit:~~~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
-~~left\_inverse:~{"}x{\isasyminv}~{\isasymOtimes}~x~=~{\isasymunit}{"}\isanewline
+\ \ group\ <\ semigroup\isanewline
+\ \ left\_unit:\ \ \ \ {"}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{"}\isanewline
+\ \ left\_inverse:\ {"}x{\isasyminv}\ {\isasymOtimes}\ x\ =\ {\isasymunit}{"}\isanewline
\isanewline
\isacommand{axclass}\isanewline
-~~agroup~<~group\isanewline
-~~commute:~{"}x~{\isasymOtimes}~y~=~y~{\isasymOtimes}~x{"}%
+\ \ agroup\ <\ group\isanewline
+\ \ commute:\ {"}x\ {\isasymOtimes}\ y\ =\ y\ {\isasymOtimes}\ x{"}%
\begin{isamarkuptext}%
\noindent Class $group$ inherits associativity of $\TIMES$ from
$semigroup$ and adds two further group axioms. Similarly, $agroup$
@@ -85,42 +85,42 @@
``abstract theorems''. For example, we may now derive the following
well-known laws of general groups.%
\end{isamarkuptext}%
-\isacommand{theorem}~group\_right\_inverse:~{"}x~{\isasymOtimes}~x{\isasyminv}~=~({\isasymunit}{\isasymColon}'a{\isasymColon}group){"}\isanewline
-\isacommand{proof}~-\isanewline
-~~\isacommand{have}~{"}x~{\isasymOtimes}~x{\isasyminv}~=~{\isasymunit}~{\isasymOtimes}~(x~{\isasymOtimes}~x{\isasyminv}){"}\isanewline
-~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}~{\isasymOtimes}~x~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~x{\isasyminv}~{\isasymOtimes}~x~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~(x{\isasyminv}~{\isasymOtimes}~x)~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~{\isasymunit}~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~({\isasymunit}~{\isasymOtimes}~x{\isasyminv}){"}\isanewline
-~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
-~~\isacommand{finally}~\isacommand{show}~?thesis~\isacommand{.}\isanewline
+\isacommand{theorem}\ group\_right\_inverse:\ {"}x\ {\isasymOtimes}\ x{\isasyminv}\ =\ ({\isasymunit}{\isasymColon}'a{\isasymColon}group){"}\isanewline
+\isacommand{proof}\ -\isanewline
+\ \ \isacommand{have}\ {"}x\ {\isasymOtimes}\ x{\isasyminv}\ =\ {\isasymunit}\ {\isasymOtimes}\ (x\ {\isasymOtimes}\ x{\isasyminv}){"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_unit)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ (x{\isasyminv}\ {\isasymOtimes}\ x)\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ {\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ ({\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}){"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_unit)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ {\isasymunit}{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline
+\ \ \isacommand{finally}\ \isacommand{show}\ ?thesis\ \isacommand{.}\isanewline
\isacommand{qed}%
\begin{isamarkuptext}%
\noindent With $group_right_inverse$ already available,
$group_right_unit$\label{thm:group-right-unit} is now established
much easier.%
\end{isamarkuptext}%
-\isacommand{theorem}~group\_right\_unit:~{"}x~{\isasymOtimes}~{\isasymunit}~=~(x{\isasymColon}'a{\isasymColon}group){"}\isanewline
-\isacommand{proof}~-\isanewline
-~~\isacommand{have}~{"}x~{\isasymOtimes}~{\isasymunit}~=~x~{\isasymOtimes}~(x{\isasyminv}~{\isasymOtimes}~x){"}\isanewline
-~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~x~{\isasymOtimes}~x{\isasyminv}~{\isasymOtimes}~x{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}~{\isasymOtimes}~x{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~group\_right\_inverse)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~x{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline
-~~\isacommand{finally}~\isacommand{show}~?thesis~\isacommand{.}\isanewline
+\isacommand{theorem}\ group\_right\_unit:\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ (x{\isasymColon}'a{\isasymColon}group){"}\isanewline
+\isacommand{proof}\ -\isanewline
+\ \ \isacommand{have}\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x\ {\isasymOtimes}\ (x{\isasyminv}\ {\isasymOtimes}\ x){"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ x\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ group\_right\_inverse)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ x{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_unit)\isanewline
+\ \ \isacommand{finally}\ \isacommand{show}\ ?thesis\ \isacommand{.}\isanewline
\isacommand{qed}%
\begin{isamarkuptext}%
\medskip Abstract theorems may be instantiated to only those types
@@ -169,22 +169,22 @@
\end{center}
\end{figure}%
\end{isamarkuptext}%
-\isacommand{instance}~monoid~<~semigroup\isanewline
-\isacommand{proof}~intro\_classes\isanewline
-~~\isacommand{fix}~x~y~z~::~{"}'a{\isasymColon}monoid{"}\isanewline
-~~\isacommand{show}~{"}x~{\isasymOtimes}~y~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
-~~~~\isacommand{by}~(rule~monoid.assoc)\isanewline
+\isacommand{instance}\ monoid\ <\ semigroup\isanewline
+\isacommand{proof}\ intro\_classes\isanewline
+\ \ \isacommand{fix}\ x\ y\ z\ ::\ {"}'a{\isasymColon}monoid{"}\isanewline
+\ \ \isacommand{show}\ {"}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline
+\ \ \ \ \isacommand{by}\ (rule\ monoid.assoc)\isanewline
\isacommand{qed}\isanewline
\isanewline
-\isacommand{instance}~group~<~monoid\isanewline
-\isacommand{proof}~intro\_classes\isanewline
-~~\isacommand{fix}~x~y~z~::~{"}'a{\isasymColon}group{"}\isanewline
-~~\isacommand{show}~{"}x~{\isasymOtimes}~y~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
-~~~~\isacommand{by}~(rule~semigroup.assoc)\isanewline
-~~\isacommand{show}~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
-~~~~\isacommand{by}~(rule~group.left\_unit)\isanewline
-~~\isacommand{show}~{"}x~{\isasymOtimes}~{\isasymunit}~=~x{"}\isanewline
-~~~~\isacommand{by}~(rule~group\_right\_unit)\isanewline
+\isacommand{instance}\ group\ <\ monoid\isanewline
+\isacommand{proof}\ intro\_classes\isanewline
+\ \ \isacommand{fix}\ x\ y\ z\ ::\ {"}'a{\isasymColon}group{"}\isanewline
+\ \ \isacommand{show}\ {"}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline
+\ \ \ \ \isacommand{by}\ (rule\ semigroup.assoc)\isanewline
+\ \ \isacommand{show}\ {"}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{"}\isanewline
+\ \ \ \ \isacommand{by}\ (rule\ group.left\_unit)\isanewline
+\ \ \isacommand{show}\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{"}\isanewline
+\ \ \ \ \isacommand{by}\ (rule\ group\_right\_unit)\isanewline
\isacommand{qed}%
\begin{isamarkuptext}%
\medskip The $\isakeyword{instance}$ command sets up an appropriate
@@ -211,13 +211,13 @@
transferred to Isabelle's type signature level.
\medskip As a typical example, we show that type $bool$ with
- exclusive-or as operation $\TIMES$, identity as $\isasyminv$, and
+ exclusive-or as $\TIMES$ operation, identity as $\isasyminv$, and
$False$ as $1$ forms an Abelian group.%
\end{isamarkuptext}%
-\isacommand{defs}~(\isakeyword{overloaded})\isanewline
-~~times\_bool\_def:~~~{"}x~{\isasymOtimes}~y~{\isasymequiv}~x~{\isasymnoteq}~(y{\isasymColon}bool){"}\isanewline
-~~inverse\_bool\_def:~{"}x{\isasyminv}~{\isasymequiv}~x{\isasymColon}bool{"}\isanewline
-~~unit\_bool\_def:~~~~{"}{\isasymunit}~{\isasymequiv}~False{"}%
+\isacommand{defs}\ (\isakeyword{overloaded})\isanewline
+\ \ times\_bool\_def:\ \ \ {"}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ (y{\isasymColon}bool){"}\isanewline
+\ \ inverse\_bool\_def:\ {"}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{"}\isanewline
+\ \ unit\_bool\_def:\ \ \ \ {"}{\isasymunit}\ {\isasymequiv}\ False{"}%
\begin{isamarkuptext}%
\medskip It is important to note that above $\DEFS$ are just
overloaded meta-level constant definitions, where type classes are
@@ -232,14 +232,14 @@
operations on type $bool$ appropriately, the class membership $bool
:: agroup$ may be now derived as follows.%
\end{isamarkuptext}%
-\isacommand{instance}~bool~::~agroup\isanewline
-\isacommand{proof}~(intro\_classes,\isanewline
-~~~~unfold~times\_bool\_def~inverse\_bool\_def~unit\_bool\_def)\isanewline
-~~\isacommand{fix}~x~y~z\isanewline
-~~\isacommand{show}~{"}((x~{\isasymnoteq}~y)~{\isasymnoteq}~z)~=~(x~{\isasymnoteq}~(y~{\isasymnoteq}~z)){"}~\isacommand{by}~blast\isanewline
-~~\isacommand{show}~{"}(False~{\isasymnoteq}~x)~=~x{"}~\isacommand{by}~blast\isanewline
-~~\isacommand{show}~{"}(x~{\isasymnoteq}~x)~=~False{"}~\isacommand{by}~blast\isanewline
-~~\isacommand{show}~{"}(x~{\isasymnoteq}~y)~=~(y~{\isasymnoteq}~x){"}~\isacommand{by}~blast\isanewline
+\isacommand{instance}\ bool\ ::\ agroup\isanewline
+\isacommand{proof}\ (intro\_classes,\isanewline
+\ \ \ \ unfold\ times\_bool\_def\ inverse\_bool\_def\ unit\_bool\_def)\isanewline
+\ \ \isacommand{fix}\ x\ y\ z\isanewline
+\ \ \isacommand{show}\ {"}((x\ {\isasymnoteq}\ y)\ {\isasymnoteq}\ z)\ =\ (x\ {\isasymnoteq}\ (y\ {\isasymnoteq}\ z)){"}\ \isacommand{by}\ blast\isanewline
+\ \ \isacommand{show}\ {"}(False\ {\isasymnoteq}\ x)\ =\ x{"}\ \isacommand{by}\ blast\isanewline
+\ \ \isacommand{show}\ {"}(x\ {\isasymnoteq}\ x)\ =\ False{"}\ \isacommand{by}\ blast\isanewline
+\ \ \isacommand{show}\ {"}(x\ {\isasymnoteq}\ y)\ =\ (y\ {\isasymnoteq}\ x){"}\ \isacommand{by}\ blast\isanewline
\isacommand{qed}%
\begin{isamarkuptext}%
The result of an $\isakeyword{instance}$ statement is both expressed
@@ -269,23 +269,23 @@
products, direct sums or function spaces. Subsequently we lift
$\TIMES$ component-wise to binary products $\alpha \times \beta$.%
\end{isamarkuptext}%
-\isacommand{defs}~(\isakeyword{overloaded})\isanewline
-~~times\_prod\_def:~{"}p~{\isasymOtimes}~q~{\isasymequiv}~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q){"}%
+\isacommand{defs}\ (\isakeyword{overloaded})\isanewline
+\ \ times\_prod\_def:\ {"}p\ {\isasymOtimes}\ q\ {\isasymequiv}\ (fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q){"}%
\begin{isamarkuptext}%
It is very easy to see that associativity of $\TIMES^\alpha$ and
$\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence
the binary type constructor $\times$ maps semigroups to semigroups.
This may be established formally as follows.%
\end{isamarkuptext}%
-\isacommand{instance}~*~::~(semigroup,~semigroup)~semigroup\isanewline
-\isacommand{proof}~(intro\_classes,~unfold~times\_prod\_def)\isanewline
-~~\isacommand{fix}~p~q~r~::~{"}'a{\isasymColon}semigroup~{\isasymtimes}~'b{\isasymColon}semigroup{"}\isanewline
-~~\isacommand{show}\isanewline
-~~~~{"}(fst~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q)~{\isasymOtimes}~fst~r,\isanewline
-~~~~~~snd~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q)~{\isasymOtimes}~snd~r)~=\isanewline
-~~~~~~~(fst~p~{\isasymOtimes}~fst~(fst~q~{\isasymOtimes}~fst~r,~snd~q~{\isasymOtimes}~snd~r),\isanewline
-~~~~~~~~snd~p~{\isasymOtimes}~snd~(fst~q~{\isasymOtimes}~fst~r,~snd~q~{\isasymOtimes}~snd~r)){"}\isanewline
-~~~~\isacommand{by}~(simp~add:~semigroup.assoc)\isanewline
+\isacommand{instance}\ *\ ::\ (semigroup,\ semigroup)\ semigroup\isanewline
+\isacommand{proof}\ (intro\_classes,\ unfold\ times\_prod\_def)\isanewline
+\ \ \isacommand{fix}\ p\ q\ r\ ::\ {"}'a{\isasymColon}semigroup\ {\isasymtimes}\ 'b{\isasymColon}semigroup{"}\isanewline
+\ \ \isacommand{show}\isanewline
+\ \ \ \ {"}(fst\ (fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q)\ {\isasymOtimes}\ fst\ r,\isanewline
+\ \ \ \ \ \ snd\ (fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q)\ {\isasymOtimes}\ snd\ r)\ =\isanewline
+\ \ \ \ \ \ \ (fst\ p\ {\isasymOtimes}\ fst\ (fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r),\isanewline
+\ \ \ \ \ \ \ \ snd\ p\ {\isasymOtimes}\ snd\ (fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r)){"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ add:\ semigroup.assoc)\isanewline
\isacommand{qed}%
\begin{isamarkuptext}%
Thus, if we view class instances as ``structures'', then overloaded