--- a/doc-src/AxClass/generated/Group.tex Mon May 22 10:31:44 2000 +0200
+++ b/doc-src/AxClass/generated/Group.tex Mon May 22 11:56:55 2000 +0200
@@ -3,13 +3,13 @@
\isamarkupheader{Basic group theory}
\isacommand{theory}~Group~=~Main:%
\begin{isamarkuptext}%
-\medskip\noindent The meta type system of Isabelle supports
+\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.%
+ general groups and Abelian groups.%
\end{isamarkuptext}%
%
\isamarkupsubsection{Monoids and Groups}
@@ -42,9 +42,9 @@
%
\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$.%
+ of semigroups, general groups and Abelian groups. Note that the
+ names of class axioms are automatically qualified with each class
+ name, so we may re-use common names such as $assoc$.%
\end{isamarkuptext}%
\isacommand{axclass}\isanewline
~~semigroup~<~{"}term{"}\isanewline
@@ -53,14 +53,14 @@
\isacommand{axclass}\isanewline
~~group~<~semigroup\isanewline
~~left\_unit:~~~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
-~~left\_inverse:~{"}inverse~x~{\isasymOtimes}~x~=~{\isasymunit}{"}\isanewline
+~~left\_inverse:~{"}x{\isasyminv}~{\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$
+ $semigroup$ and adds two further 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.%
@@ -71,8 +71,8 @@
\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
+ $assoc$, $left_unit$, $left_inverse$, $commute$, where any of these
+ contain a type 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 ::
@@ -83,13 +83,13 @@
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.%
+ 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{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
@@ -138,7 +138,8 @@
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
+ we may now instantiate $monoid \subseteq semigroup$ and $group
+ \subseteq monoid$ properly as follows
(cf.\ \figref{fig:monoid-group}).
\begin{figure}[htbp]
@@ -166,13 +167,7 @@
\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{figure}%
\end{isamarkuptext}%
\isacommand{instance}~monoid~<~semigroup\isanewline
\isacommand{proof}~intro\_classes\isanewline
@@ -193,14 +188,19 @@
\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
+ goal that represents the class inclusion (or type arity, see
+ \secref{sec:inst-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.%
+ to reduce to the initial statement to a number of goals that directly
+ correspond to any class axioms encountered on the path upwards
+ through the class hierarchy.
+
+ any logical class axioms as subgoals.%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Concrete instantiation}
+\isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}}
%
\begin{isamarkuptext}%
So far we have covered the case of the form
@@ -212,11 +212,9 @@
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.%
+ \medskip As a 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
@@ -224,12 +222,12 @@
~~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
+ overloaded meta-level constant definitions, where 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 as definitional extensions of plain HOL
+ \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not
+ required for overloading. Nevertheless, overloaded definitions are
best applied in the context of type classes.
\medskip Since we have chosen above $\DEFS$ of the generic group
@@ -239,25 +237,25 @@
\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{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 $\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.
+The result of an $\isakeyword{instance}$ statement is both expressed
+ as a theorem of Isabelle's meta-logic, and as a type arity of the
+ type signature. The latter enables 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.%
+ \medskip We could now 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}
@@ -271,20 +269,19 @@
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$.%
+ $\TIMES$ component-wise to binary 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){"}%
+~~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$,
+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~prod\_prod\_def)\isanewline
-~~\isacommand{fix}~p~q~r~::~{"}'a{\isasymColon}semigroup~*~'b{\isasymColon}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
@@ -294,8 +291,8 @@
\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
+ constant definitions with recursion over types indirectly provide
+ some kind of ``functors'' --- i.e.\ mappings between abstract
theories.%
\end{isamarkuptext}%
\isacommand{end}\end{isabelle}%