--- a/doc-src/AxClass/generated/Group.tex Sun May 21 14:49:28 2000 +0200
+++ b/doc-src/AxClass/generated/Group.tex Sun May 21 21:48:39 2000 +0200
@@ -1,21 +1,51 @@
\begin{isabelle}%
-\isanewline
-\isacommand{theory}~Group~=~Main:\isanewline
-\isanewline
-\isanewline
+%
+\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}{"})\isanewline
-\isanewline
-\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{"}\isanewline
-\isanewline
-\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
@@ -23,12 +53,39 @@
\isacommand{axclass}\isanewline
~~group~<~semigroup\isanewline
~~left\_unit:~~~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
-~~left\_inverse:~{"}inverse~x~{\isasymOtimes}~x~=~{\isasymunit}{"}%
+~~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}%
-The group axioms only state the properties of left unit and inverse,
- the right versions may be derived as follows.%
+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}::'a::group){"}\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
@@ -49,11 +106,11 @@
~~\isacommand{finally}~\isacommand{show}~?thesis~\isacommand{.}\isanewline
\isacommand{qed}%
\begin{isamarkuptext}%
-With $group_right_inverse$ already available,
+\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::'a::group){"}\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
@@ -64,41 +121,121 @@
~~\isacommand{also}~\isacommand{have}~{"}...~=~x{"}\isanewline
~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline
~~\isacommand{finally}~\isacommand{show}~?thesis~\isacommand{.}\isanewline
-\isacommand{qed}\isanewline
-\isanewline
-\isanewline
-\isacommand{axclass}\isanewline
-~~agroup~<~group\isanewline
-~~commute:~{"}x~{\isasymOtimes}~y~=~y~{\isasymOtimes}~x{"}\isanewline
-\isanewline
-\isanewline
-\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::monoid{"}\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
-\isanewline
\isacommand{instance}~group~<~monoid\isanewline
\isacommand{proof}~intro\_classes\isanewline
-~~\isacommand{fix}~x~y~z~::~{"}'a::group{"}\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}\isanewline
-\isanewline
-\isanewline
-\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{"}\isanewline
-\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
@@ -107,21 +244,58 @@
~~\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}\isanewline
-\isanewline
-\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){"}\isanewline
-\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::semigroup~*~'b::semigroup{"}\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}\isanewline
-\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}%