tuned;

--- a/doc-src/AxClass/Group/Group.thy	Mon May 22 10:31:44 2000 +0200
+++ b/doc-src/AxClass/Group/Group.thy	Mon May 22 11:56:55 2000 +0200
@@ -4,13 +4,13 @@
 theory Group = Main:;
 
 text {*
- \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.
 *};
 
 subsection {* Monoids and Groups *};
@@ -47,9 +47,9 @@
 
 text {*
  \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$.
 *};
 
 axclass
@@ -59,7 +59,7 @@
 axclass
   group < semigroup
   left_unit:    "\<unit> \<Otimes> x = x"
-  left_inverse: "inverse x \<Otimes> x = \<unit>";
+  left_inverse: "x\<inv> \<Otimes> x = \<unit>";
 
 axclass
   agroup < group
@@ -67,7 +67,7 @@
 
 text {*
  \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.
@@ -79,8 +79,8 @@
 text {*
  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 ::
@@ -91,14 +91,14 @@
  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.
 *};
 
-theorem group_right_inverse: "x \<Otimes> x\<inv> = (\<unit>\<Colon>'a\<Colon>group)";
+theorem group_right_inverse: "x \<Otimes> x\<inv> = (\<unit>\\<Colon>'a\\<Colon>group)";
 proof -;
   have "x \<Otimes> x\<inv> = \<unit> \<Otimes> (x \<Otimes> x\<inv>)";
     by (simp only: group.left_unit);
-  also; have "... = (\<unit> \<Otimes> x) \<Otimes> x\<inv>";
+  also; have "... = \<unit> \<Otimes> x \<Otimes> x\<inv>";
     by (simp only: semigroup.assoc);
   also; have "... = (x\<inv>)\<inv> \<Otimes> x\<inv> \<Otimes> x \<Otimes> x\<inv>";
     by (simp only: group.left_inverse);
@@ -121,7 +121,7 @@
  much easier.
 *};
 
-theorem group_right_unit: "x \<Otimes> \<unit> = (x\<Colon>'a\<Colon>group)";
+theorem group_right_unit: "x \<Otimes> \<unit> = (x\\<Colon>'a\\<Colon>group)";
 proof -;
   have "x \<Otimes> \<unit> = x \<Otimes> (x\<inv> \<Otimes> x)";
     by (simp only: group.left_inverse);
@@ -151,7 +151,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]
@@ -180,24 +181,18 @@
      \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.
 *};
 
 instance monoid < semigroup;
 proof intro_classes;
-  fix x y z :: "'a\<Colon>monoid";
+  fix x y z :: "'a\\<Colon>monoid";
   show "x \<Otimes> y \<Otimes> z = x \<Otimes> (y \<Otimes> z)";
     by (rule monoid.assoc);
 qed;
 
 instance group < monoid;
 proof intro_classes;
-  fix x y z :: "'a\<Colon>group";
+  fix x y z :: "'a\\<Colon>group";
   show "x \<Otimes> y \<Otimes> z = x \<Otimes> (y \<Otimes> z)";
     by (rule semigroup.assoc);
   show "\<unit> \<Otimes> x = x";
@@ -208,15 +203,18 @@
 
 text {*
  \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.
 *};
 
 
-subsection {* Concrete instantiation *};
+subsection {* Concrete instantiation \label{sec:inst-arity} *};
 
 text {*
  So far we have covered the case of the form
@@ -228,11 +226,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.
 *};
 
 defs
@@ -242,12 +238,12 @@
 
 text {*
  \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
@@ -258,7 +254,7 @@
 instance bool :: agroup;
 proof (intro_classes,
     unfold times_bool_def inverse_bool_def unit_bool_def);
-  fix x y z :: bool;
+  fix x y z;
   show "((x \\<noteq> y) \\<noteq> z) = (x \\<noteq> (y \\<noteq> z))"; by blast;
   show "(False \\<noteq> x) = x"; by blast;
   show "(x \\<noteq> x) = False"; by blast;
@@ -266,18 +262,18 @@
 qed;
 
 text {*
- 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.
 *};
 
 
@@ -292,23 +288,22 @@
 
  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$.
 *};
 
 defs
-  prod_prod_def: "p \<Otimes> q \\<equiv> (fst p \<Otimes> fst q, snd p \<Otimes> snd q)";
+  times_prod_def: "p \<Otimes> q \\<equiv> (fst p \<Otimes> fst q, snd p \<Otimes> snd q)";
 
 text {*
- 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.
 *};
 
 instance * :: (semigroup, semigroup) semigroup;
-proof (intro_classes, unfold prod_prod_def);
-  fix p q r :: "'a\<Colon>semigroup * 'b\<Colon>semigroup";
+proof (intro_classes, unfold times_prod_def);
+  fix p q r :: "'a\\<Colon>semigroup \\<times> 'b\\<Colon>semigroup";
   show
     "(fst (fst p \<Otimes> fst q, snd p \<Otimes> snd q) \<Otimes> fst r,
       snd (fst p \<Otimes> fst q, snd p \<Otimes> snd q) \<Otimes> snd r) =
@@ -319,8 +314,8 @@
 
 text {*
  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.
 *};
 

--- a/doc-src/AxClass/Group/Product.thy	Mon May 22 10:31:44 2000 +0200
+++ b/doc-src/AxClass/Group/Product.thy	Mon May 22 11:56:55 2000 +0200
@@ -5,14 +5,14 @@
 
 text {*
  \medskip\noindent There is still a feature of Isabelle's type system
- left that we have not yet used: when declaring polymorphic constants
- $c :: \sigma$, the type variables occurring in $\sigma$ may be
- constrained by type classes (or even general sorts) in an arbitrary
- way.  Note that by default, in Isabelle/HOL the declaration $\TIMES
- :: \alpha \To \alpha \To \alpha$ is actually an abbreviation for
- $\TIMES :: (\alpha::term) \To \alpha \To \alpha$.  Since class $term$
- is the universal class of HOL, this is not really a restriction at
- all.
+ left that we have not yet discussed.  When declaring polymorphic
+ constants $c :: \sigma$, the type variables occurring in $\sigma$ may
+ be constrained by type classes (or even general sorts) in an
+ arbitrary way.  Note that by default, in Isabelle/HOL the declaration
+ $\TIMES :: \alpha \To \alpha \To \alpha$ is actually an abbreviation
+ for $\TIMES :: (\alpha::term) \To \alpha \To \alpha$.  Since class
+ $term$ is the universal class of HOL, this is not really a constraint
+ at all.
 
  The $product$ class below provides a less degenerate example of
  syntactic type classes.
@@ -21,7 +21,7 @@
 axclass
   product < "term";
 consts
-  product :: "'a::product \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\\<otimes>" 70);
+  product :: "'a::product \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\\<Otimes>" 70);
 
 text {*
  Here class $product$ is defined as subclass of $term$ without any
@@ -55,7 +55,7 @@
 instance bool :: product;
   by intro_classes;
 defs
-  product_bool_def: "x \\<otimes> y \\<equiv> x \\<and> y";
+  product_bool_def: "x \\<Otimes> y \\<equiv> x \\<and> y";
 
 text {*
  The definition $prod_bool_def$ becomes syntactically well-formed only
@@ -70,14 +70,14 @@
 
  \medskip While Isabelle type classes and those of Haskell are almost
  the same as far as type-checking and type inference are concerned,
- there are major semantic differences.  Haskell classes require their
- instances to \emph{provide operations} of certain \emph{names}.
+ there are important semantic differences.  Haskell classes require
+ their instances to \emph{provide operations} of certain \emph{names}.
  Therefore, its \texttt{instance} has a \texttt{where} part that tells
  the system what these ``member functions'' should be.
 
- This style of \texttt{instance} won't make much sense in Isabelle,
- because its meta-logic has no corresponding notion of ``providing
- operations'' or ``names''.
+ This style of \texttt{instance} won't make much sense in Isabelle's
+ meta-logic, because there is no internal notion of ``providing
+ operations'' or even ``names of functions''.
 *};
 
 end;
\ No newline at end of file

--- a/doc-src/AxClass/Group/Semigroups.thy	Mon May 22 10:31:44 2000 +0200
+++ b/doc-src/AxClass/Group/Semigroups.thy	Mon May 22 11:56:55 2000 +0200
@@ -5,12 +5,12 @@
 
 text {*
  \medskip\noindent An axiomatic type class is simply a class of types
- that all meet certain \emph{axioms}. Thus, type classes may be also
- understood as type predicates --- i.e.\ abstractions over a single
- type argument $\alpha$.  Class axioms typically contain polymorphic
- constants that depend on this type $\alpha$.  These
- \emph{characteristic constants} behave like operations associated
- with the ``carrier'' type $\alpha$.
+ that all meet certain properties, which are also called \emph{class
+ axioms}. Thus, type classes may be also understood as type predicates
+ --- i.e.\ abstractions over a single type argument $\alpha$.  Class
+ axioms typically contain polymorphic constants that depend on this
+ type $\alpha$.  These \emph{characteristic constants} behave like
+ operations associated with the ``carrier'' type $\alpha$.
 
  We illustrate these basic concepts by the following formulation of
  semigroups.
@@ -35,8 +35,8 @@
  \medskip In general, type classes may be used to describe
  \emph{structures} with exactly one carrier $\alpha$ and a fixed
  \emph{signature}.  Different signatures require different classes.
- Subsequently, class $plus_semigroup$ represents semigroups of the
- form $(\tau, \PLUS^\tau)$, while $semigroup$ above would correspond
+ Below, class $plus_semigroup$ represents semigroups of the form
+ $(\tau, \PLUS^\tau)$, while the original $semigroup$ would correspond
  to semigroups $(\tau, \TIMES^\tau)$.
 *};
 
@@ -47,8 +47,9 @@
   assoc: "(x \<Oplus> y) \<Oplus> z = x \<Oplus> (y \<Oplus> z)";
 
 text {*
- \noindent Even if classes $plus_semigroup$ and $times_semigroup$ both
- represent semigroups in a sense, they are certainly not the same!
+ \noindent Even if classes $plus_semigroup$ and $semigroup$ both
+ represent semigroups in a sense, they are certainly not quite the
+ same.
 *};
 
 end;
\ No newline at end of file

--- a/doc-src/AxClass/Nat/NatClass.thy	Mon May 22 10:31:44 2000 +0200
+++ b/doc-src/AxClass/Nat/NatClass.thy	Mon May 22 11:56:55 2000 +0200
@@ -34,26 +34,28 @@
 text {*
  This is an abstract version of the plain $Nat$ theory in
  FOL.\footnote{See
- \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}}
+ \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}} Basically,
+ we have just replaced all occurrences of type $nat$ by $\alpha$ and
+ used the natural number axioms to define class $nat$.  There is only
+ a minor snag, that the original recursion operator $rec$ had to be
+ made monomorphic.
 
- Basically, we have just replaced all occurrences of type $nat$ by
- $\alpha$ and used the natural number axioms to define class $nat$.
- There is only a minor snag, that the original recursion operator
- $rec$ had to be made monomorphic, in a sense.  Thus class $nat$
- contains exactly those types $\tau$ that are isomorphic to ``the''
- natural numbers (with signature $0$, $Suc$, $rec$).
+ Thus class $nat$ contains exactly those types $\tau$ that are
+ isomorphic to ``the'' natural numbers (with signature $0$, $Suc$,
+ $rec$).
 
  \medskip What we have done here can be also viewed as \emph{type
  specification}.  Of course, it still remains open if there is some
  type at all that meets the class axioms.  Now a very nice property of
- axiomatic type classes is, that abstract reasoning is always possible
+ axiomatic type classes is that abstract reasoning is always possible
  --- independent of satisfiability.  The meta-logic won't break, even
- if some classes (or general sorts) turns out to be empty
- (``inconsistent'') later.
+ if some classes (or general sorts) turns out to be empty later ---
+ ``inconsistent'' class definitions may be useless, but do not cause
+ any harm.
 
  Theorems of the abstract natural numbers may be derived in the same
  way as for the concrete version.  The original proof scripts may be
- used with some trivial changes only (mostly adding some type
+ re-used with some trivial changes only (mostly adding some type
  constraints).
 *};
 

--- a/doc-src/AxClass/axclass.tex	Mon May 22 10:31:44 2000 +0200
+++ b/doc-src/AxClass/axclass.tex	Mon May 22 11:56:55 2000 +0200
@@ -3,12 +3,12 @@
 \usepackage{graphicx,../iman,../extra,../isar,../pdfsetup}
 \usepackage{generated/isabelle,generated/isabellesym}
 
-\newcommand{\isasymOtimes}{\emph{$\odot$}}
+\newcommand{\TIMES}{\cdot}
+\newcommand{\PLUS}{\oplus}
+\newcommand{\isasymOtimes}{\emph{$\cdot$}}
 \newcommand{\isasymOplus}{\emph{$\oplus$}}
 \newcommand{\isasyminv}{\emph{${}^{-1}$}}
 \newcommand{\isasymunit}{\emph{$1$}}
-\newcommand{\TIMES}{\odot}
-\newcommand{\PLUS}{\oplus}
 
 
 \newcommand{\secref}[1]{\S\ref{#1}}
@@ -46,12 +46,12 @@
   abstract theories. Subsequently, we demonstrate typical uses of Isabelle's
   axiomatic type classes to model basic algebraic structures.
   
-  Note that this document describes axiomatic type classes using Isabelle/Isar
-  theories, with proofs expressed via Isar proof language elements.  The new
-  theory format greatly simplifies the arrangement of the overall development,
-  since definitions and proofs may be freely intermixed.  Users who prefer
-  tactic scripts over structured proofs do not need to fall back on separate
-  ML scripts, but may refer to Isar's tactic emulation commands.
+  This document describes axiomatic type classes using Isabelle/Isar theories,
+  with proofs expressed via Isar proof language elements.  The new theory
+  format greatly simplifies the arrangement of the overall development, since
+  definitions and proofs may be freely intermixed.  Users who prefer tactic
+  scripts over structured proofs do not need to fall back on separate ML
+  scripts, though, but may refer to Isar's tactic emulation commands.
 \end{abstract}
 
 

--- a/doc-src/AxClass/body.tex	Mon May 22 10:31:44 2000 +0200
+++ b/doc-src/AxClass/body.tex	Mon May 22 11:56:55 2000 +0200
@@ -2,25 +2,25 @@
 \chapter{Introduction}
 
 A Haskell-style type-system \cite{haskell-report} with ordered type-classes
-has been present in Isabelle since 1991 \cite{nipkow-sorts93}.  Initially,
-classes have mainly served as a \emph{purely syntactic} tool to formulate
-polymorphic object-logics in a clean way, such as the standard Isabelle
-formulation of many-sorted FOL \cite{paulson-isa-book}.
+has been present in Isabelle since 1991 already \cite{nipkow-sorts93}.
+Initially, classes have mainly served as a \emph{purely syntactic} tool to
+formulate polymorphic object-logics in a clean way, such as the standard
+Isabelle formulation of many-sorted FOL \cite{paulson-isa-book}.
 
 Applying classes at the \emph{logical level} to provide a simple notion of
 abstract theories and instantiations to concrete ones, has been long proposed
-as well \cite{nipkow-types93,nipkow-sorts93}).  At that time, Isabelle still
+as well \cite{nipkow-types93,nipkow-sorts93}.  At that time, Isabelle still
 lacked built-in support for these \emph{axiomatic type classes}. More
 importantly, their semantics was not yet fully fleshed out (and unnecessarily
 complicated, too).
 
-Since the Isabelle94 releases, actual axiomatic type classes have been an
-integral part of Isabelle's meta-logic.  This very simple implementation is
-based on a straight-forward extension of traditional simple-typed Higher-Order
-Logic, including types qualified by logical predicates and overloaded constant
-definitions; see \cite{Wenzel:1997:TPHOL} for further details.
+Since Isabelle94, actual axiomatic type classes have been an integral part of
+Isabelle's meta-logic.  This very simple implementation is based on a
+straight-forward extension of traditional simply-typed Higher-Order Logic, by
+including types qualified by logical predicates and overloaded constant
+definitions (see \cite{Wenzel:1997:TPHOL} for further details).
 
-Yet until Isabelle99, there used to be still a fundamental methodological
+Yet even until Isabelle99, there used to be still a fundamental methodological
 problem in using axiomatic type classes conveniently, due to the traditional
 distinction of Isabelle theory files vs.\ ML proof scripts.  This has been
 finally overcome with the advent of Isabelle/Isar theories
@@ -32,9 +32,9 @@
 \medskip
 
 So to cut a long story short, the present version of axiomatic type classes
-(Isabelle99 or later) now provides an even more useful and convenient
-mechanism for light-weight abstract theories, without any special provisions
-to be observed by the user.
+now provides an even more useful and convenient mechanism for light-weight
+abstract theories, without any special technical provisions to be observed by
+the user.
 
 
 \chapter{Examples}\label{sec:ex}

--- 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}%

--- a/doc-src/AxClass/generated/NatClass.tex	Mon May 22 10:31:44 2000 +0200
+++ b/doc-src/AxClass/generated/NatClass.tex	Mon May 22 11:56:55 2000 +0200
@@ -31,26 +31,28 @@
 \begin{isamarkuptext}%
 This is an abstract version of the plain $Nat$ theory in
  FOL.\footnote{See
- \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}}
+ \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}} Basically,
+ we have just replaced all occurrences of type $nat$ by $\alpha$ and
+ used the natural number axioms to define class $nat$.  There is only
+ a minor snag, that the original recursion operator $rec$ had to be
+ made monomorphic.
 
- Basically, we have just replaced all occurrences of type $nat$ by
- $\alpha$ and used the natural number axioms to define class $nat$.
- There is only a minor snag, that the original recursion operator
- $rec$ had to be made monomorphic, in a sense.  Thus class $nat$
- contains exactly those types $\tau$ that are isomorphic to ``the''
- natural numbers (with signature $0$, $Suc$, $rec$).
+ Thus class $nat$ contains exactly those types $\tau$ that are
+ isomorphic to ``the'' natural numbers (with signature $0$, $Suc$,
+ $rec$).
 
  \medskip What we have done here can be also viewed as \emph{type
  specification}.  Of course, it still remains open if there is some
  type at all that meets the class axioms.  Now a very nice property of
- axiomatic type classes is, that abstract reasoning is always possible
+ axiomatic type classes is that abstract reasoning is always possible
  --- independent of satisfiability.  The meta-logic won't break, even
- if some classes (or general sorts) turns out to be empty
- (``inconsistent'') later.
+ if some classes (or general sorts) turns out to be empty later ---
+ ``inconsistent'' class definitions may be useless, but do not cause
+ any harm.
 
  Theorems of the abstract natural numbers may be derived in the same
  way as for the concrete version.  The original proof scripts may be
- used with some trivial changes only (mostly adding some type
+ re-used with some trivial changes only (mostly adding some type
  constraints).%
 \end{isamarkuptext}%
 \isacommand{end}\end{isabelle}%

--- a/doc-src/AxClass/generated/Product.tex	Mon May 22 10:31:44 2000 +0200
+++ b/doc-src/AxClass/generated/Product.tex	Mon May 22 11:56:55 2000 +0200
@@ -4,14 +4,14 @@
 \isacommand{theory}~Product~=~Main:%
 \begin{isamarkuptext}%
 \medskip\noindent There is still a feature of Isabelle's type system
- left that we have not yet used: when declaring polymorphic constants
- $c :: \sigma$, the type variables occurring in $\sigma$ may be
- constrained by type classes (or even general sorts) in an arbitrary
- way.  Note that by default, in Isabelle/HOL the declaration $\TIMES
- :: \alpha \To \alpha \To \alpha$ is actually an abbreviation for
- $\TIMES :: (\alpha::term) \To \alpha \To \alpha$.  Since class $term$
- is the universal class of HOL, this is not really a restriction at
- all.
+ left that we have not yet discussed.  When declaring polymorphic
+ constants $c :: \sigma$, the type variables occurring in $\sigma$ may
+ be constrained by type classes (or even general sorts) in an
+ arbitrary way.  Note that by default, in Isabelle/HOL the declaration
+ $\TIMES :: \alpha \To \alpha \To \alpha$ is actually an abbreviation
+ for $\TIMES :: (\alpha::term) \To \alpha \To \alpha$.  Since class
+ $term$ is the universal class of HOL, this is not really a constraint
+ at all.
 
  The $product$ class below provides a less degenerate example of
  syntactic type classes.%
@@ -19,7 +19,7 @@
 \isacommand{axclass}\isanewline
 ~~product~<~{"}term{"}\isanewline
 \isacommand{consts}\isanewline
-~~product~::~{"}'a::product~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymotimes}{"}~70)%
+~~product~::~{"}'a::product~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)%
 \begin{isamarkuptext}%
 Here class $product$ is defined as subclass of $term$ without any
  additional axioms.  This effects in logical equivalence of $product$
@@ -51,7 +51,7 @@
 \isacommand{instance}~bool~::~product\isanewline
 ~~\isacommand{by}~intro\_classes\isanewline
 \isacommand{defs}\isanewline
-~~product\_bool\_def:~{"}x~{\isasymotimes}~y~{\isasymequiv}~x~{\isasymand}~y{"}%
+~~product\_bool\_def:~{"}x~{\isasymOtimes}~y~{\isasymequiv}~x~{\isasymand}~y{"}%
 \begin{isamarkuptext}%
 The definition $prod_bool_def$ becomes syntactically well-formed only
  after the arity $bool :: product$ is made known to the type checker.
@@ -65,13 +65,13 @@
 
  \medskip While Isabelle type classes and those of Haskell are almost
  the same as far as type-checking and type inference are concerned,
- there are major semantic differences.  Haskell classes require their
- instances to \emph{provide operations} of certain \emph{names}.
+ there are important semantic differences.  Haskell classes require
+ their instances to \emph{provide operations} of certain \emph{names}.
  Therefore, its \texttt{instance} has a \texttt{where} part that tells
  the system what these ``member functions'' should be.
 
- This style of \texttt{instance} won't make much sense in Isabelle,
- because its meta-logic has no corresponding notion of ``providing
- operations'' or ``names''.%
+ This style of \texttt{instance} won't make much sense in Isabelle's
+ meta-logic, because there is no internal notion of ``providing
+ operations'' or even ``names of functions''.%
 \end{isamarkuptext}%
 \isacommand{end}\end{isabelle}%

--- a/doc-src/AxClass/generated/Semigroups.tex	Mon May 22 10:31:44 2000 +0200
+++ b/doc-src/AxClass/generated/Semigroups.tex	Mon May 22 11:56:55 2000 +0200
@@ -4,12 +4,12 @@
 \isacommand{theory}~Semigroups~=~Main:%
 \begin{isamarkuptext}%
 \medskip\noindent An axiomatic type class is simply a class of types
- that all meet certain \emph{axioms}. Thus, type classes may be also
- understood as type predicates --- i.e.\ abstractions over a single
- type argument $\alpha$.  Class axioms typically contain polymorphic
- constants that depend on this type $\alpha$.  These
- \emph{characteristic constants} behave like operations associated
- with the ``carrier'' type $\alpha$.
+ that all meet certain properties, which are also called \emph{class
+ axioms}. Thus, type classes may be also understood as type predicates
+ --- i.e.\ abstractions over a single type argument $\alpha$.  Class
+ axioms typically contain polymorphic constants that depend on this
+ type $\alpha$.  These \emph{characteristic constants} behave like
+ operations associated with the ``carrier'' type $\alpha$.
 
  We illustrate these basic concepts by the following formulation of
  semigroups.%
@@ -32,8 +32,8 @@
  \medskip In general, type classes may be used to describe
  \emph{structures} with exactly one carrier $\alpha$ and a fixed
  \emph{signature}.  Different signatures require different classes.
- Subsequently, class $plus_semigroup$ represents semigroups of the
- form $(\tau, \PLUS^\tau)$, while $semigroup$ above would correspond
+ Below, class $plus_semigroup$ represents semigroups of the form
+ $(\tau, \PLUS^\tau)$, while the original $semigroup$ would correspond
  to semigroups $(\tau, \TIMES^\tau)$.%
 \end{isamarkuptext}%
 \isacommand{consts}\isanewline
@@ -42,7 +42,8 @@
 ~~plus\_semigroup~<~{"}term{"}\isanewline
 ~~assoc:~{"}(x~{\isasymOplus}~y)~{\isasymOplus}~z~=~x~{\isasymOplus}~(y~{\isasymOplus}~z){"}%
 \begin{isamarkuptext}%
-\noindent Even if classes $plus_semigroup$ and $times_semigroup$ both
- represent semigroups in a sense, they are certainly not the same!%
+\noindent Even if classes $plus_semigroup$ and $semigroup$ both
+ represent semigroups in a sense, they are certainly not quite the
+ same.%
 \end{isamarkuptext}%
 \isacommand{end}\end{isabelle}%