
diff -r fc7841f31388 -r 813fabceec00 doc-src/AxClass/generated/Group.tex
--- 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}%




