\begin{isabelle}%
%
\isamarkupheader{Basic group theory}
\isacommand{theory}~Group~=~Main:%
\begin{isamarkuptext}%
\medskip\noindent The meta type system of Isabelle supports
\emph{intersections} and \emph{inclusions} of type classes. These
directly correspond to intersections and inclusions of type
predicates in a purely set theoretic sense. This is sufficient as a
means to describe simple hierarchies of structures. As an
illustration, we use the well-known example of semigroups, monoids,
general groups and abelian groups.%
\end{isamarkuptext}%
%
\isamarkupsubsection{Monoids and Groups}
%
\begin{isamarkuptext}%
First we declare some polymorphic constants required later for the
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}{"})%
\begin{isamarkuptext}%
\noindent Next we define class $monoid$ of monoids with operations
$\TIMES$ and $1$. Note that multiple class axioms are allowed for
user convenience --- they simply represent the conjunction of their
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{"}%
\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$.%
\end{isamarkuptext}%
%
\begin{isamarkuptext}%
\medskip Independently of $monoid$, we now define a linear hierarchy
of semigroups, general groups and abelian groups. Note that the
names of class axioms are automatically qualified with the class
name; thus 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
\isanewline
\isacommand{axclass}\isanewline
~~group~<~semigroup\isanewline
~~left\_unit:~~~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
~~left\_inverse:~{"}inverse~x~{\isasymOtimes}~x~=~{\isasymunit}{"}\isanewline
\isanewline
\isacommand{axclass}\isanewline
~~agroup~<~group\isanewline
~~commute:~{"}x~{\isasymOtimes}~y~=~y~{\isasymOtimes}~x{"}%
\begin{isamarkuptext}%
\noindent Class $group$ inherits associativity of $\TIMES$ from
$semigroup$ and adds the other two group axioms. Similarly, $agroup$
is defined as the subset of $group$ such that for all of its elements
$\tau$, the operation $\TIMES :: \tau \To \tau \To \tau$ is even
commutative.%
\end{isamarkuptext}%
%
\isamarkupsubsection{Abstract reasoning}
%
\begin{isamarkuptext}%
In a sense, axiomatic type classes may be viewed as \emph{abstract
theories}. Above class definitions gives rise to abstract axioms
$assoc$, $left_unit$, $left_inverse$, $commute$, where all of these
contain type a variable $\alpha :: c$ that is restricted to types of
the corresponding class $c$. \emph{Sort constraints} like this
express a logical precondition for the whole formula. For example,
$assoc$ states that for all $\tau$, provided that $\tau ::
semigroup$, the operation $\TIMES :: \tau \To \tau \To \tau$ is
associative.
\medskip From a technical point of view, abstract axioms are just
ordinary Isabelle theorems, which may be used in proofs without
special treatment. Such ``abstract proofs'' usually yield new
``abstract theorems''. For example, we may now derive the following
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{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{qed}%
\begin{isamarkuptext}%
\medskip Abstract theorems may be instantiated to only those types
$\tau$ where the appropriate class membership $\tau :: c$ is known at
Isabelle's type signature level. Since we have $agroup \subseteq
group \subseteq semigroup$ by definition, all theorems of $semigroup$
and $group$ are automatically inherited by $group$ and $agroup$.%
\end{isamarkuptext}%
%
\isamarkupsubsection{Abstract instantiation}
%
\begin{isamarkuptext}%
From the definition, the $monoid$ and $group$ classes have been
independent. Note that for monoids, $right_unit$ had to be included
as an axiom, but for groups both $right_unit$ and $right_inverse$ are
derivable from the other axioms. With $group_right_unit$ derived as
a theorem of group theory (see page~\pageref{thm:group-right-unit}),
we may now instantiate $group \subseteq monoid$ properly as follows
(cf.\ \figref{fig:monoid-group}).
\begin{figure}[htbp]
\begin{center}
\small
\unitlength 0.6mm
\begin{picture}(65,90)(0,-10)
\put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
\put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}}
\put(15,5){\makebox(0,0){$agroup$}}
\put(15,25){\makebox(0,0){$group$}}
\put(15,45){\makebox(0,0){$semigroup$}}
\put(30,65){\makebox(0,0){$term$}} \put(50,45){\makebox(0,0){$monoid$}}
\end{picture}
\hspace{4em}
\begin{picture}(30,90)(0,0)
\put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
\put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}}
\put(15,5){\makebox(0,0){$agroup$}}
\put(15,25){\makebox(0,0){$group$}}
\put(15,45){\makebox(0,0){$monoid$}}
\put(15,65){\makebox(0,0){$semigroup$}}
\put(15,85){\makebox(0,0){$term$}}
\end{picture}
\caption{Monoids and groups: according to definition, and by proof}
\label{fig:monoid-group}
\end{center}
\end{figure}
We know by definition that $\TIMES$ is associative for monoids, i.e.\
$monoid \subseteq semigroup$. Furthermore we have $assoc$,
$left_unit$ and $right_unit$ for groups (where $right_unit$ is
derivable from the group axioms), that is $group \subseteq monoid$.
Thus we may establish the following class instantiations.%
\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{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{qed}%
\begin{isamarkuptext}%
\medskip The $\isakeyword{instance}$ command sets up an appropriate
goal that represents the class inclusion (or type arity) to be proven
(see also \cite{isabelle-isar-ref}). The $intro_classes$ proof
method does back-chaining of class membership statements wrt.\ the
hierarchy of any classes defined in the current theory; the effect is
to reduce to any logical class axioms as subgoals.%
\end{isamarkuptext}%
%
\isamarkupsubsection{Concrete instantiation}
%
\begin{isamarkuptext}%
So far we have covered the case of the form
$\isakeyword{instance}~c@1 < c@2$, namely \emph{abstract
instantiation} --- $c@1$ is more special than $c@2$ and thus an
instance of $c@2$. Even more interesting for practical applications
are \emph{concrete instantiations} of axiomatic type classes. That
is, certain simple schemes $(\alpha@1, \ldots, \alpha@n)t :: c$ of
class membership may be established at the logical level and then
transferred to Isabelle's type signature level.
\medskip
As an typical example, we show that type $bool$ with exclusive-or as
operation $\TIMES$, identity as $\isasyminv$, and $False$ as $1$
forms an Abelian group.%
\end{isamarkuptext}%
\isacommand{defs}\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. In particular, type
classes are not yet involved at all! This form of constant
definition with overloading (and optional recursion over the
syntactic structure of simple types) are admissible of proper
definitional extensions in any version of HOL
\cite{Wenzel:1997:TPHOL}. Nevertheless, overloaded definitions are
best applied in the context of type classes.
\medskip Since we have chosen above $\DEFS$ of the generic group
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~::~bool\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 $\isakeyword{instance}$ is both expressed as a theorem
of Isabelle's meta-logic, and a type arity statement of the type
signature. The latter enables the type-inference system to take care
of this new instance automatically.
\medskip In a similarly fashion, we could also instantiate our group
theory classes to many other concrete types. For example, $int ::
agroup$ (e.g.\ by defining $\TIMES$ as addition, $\isasyminv$ as
negation and $1$ as zero) or $list :: (term)semigroup$ (e.g.\ if
$\TIMES$ is defined as list append). Thus, the characteristic
constants $\TIMES$, $\isasyminv$, $1$ really become overloaded, i.e.\
have different meanings on different types.%
\end{isamarkuptext}%
%
\isamarkupsubsection{Lifting and Functors}
%
\begin{isamarkuptext}%
As already mentioned above, overloading in the simply-typed HOL
systems may include recursion over the syntactic structure of types.
That is, definitional equations $c^\tau \equiv t$ may also contain
constants of name $c$ on the right-hand side --- if these have types
that are structurally simpler than $\tau$.
This feature enables us to \emph{lift operations}, say to Cartesian
products, direct sums or function spaces. Subsequently we lift
$\TIMES$ component-wise to binary Cartesian products $\alpha \times
\beta$.%
\end{isamarkuptext}%
\isacommand{defs}\isanewline
~~prod\_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$,
$\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~prod\_prod\_def)\isanewline
~~\isacommand{fix}~p~q~r~::~{"}'a{\isasymColon}semigroup~*~'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
constant definitions with primitive recursion over types indirectly
provide some kind of ``functors'' --- i.e.\ mappings between abstract
theories.%
\end{isamarkuptext}%
\isacommand{end}\end{isabelle}%