# HG changeset patch
# User wenzelm
# Date 958938519 -7200
# Node ID 78d6e47469e4667519858ada5381bf0914165966
# Parent  a705822f4e2a05bf2f7cfd5d92b4747d1f377eed
new Isar version;

diff -r a705822f4e2a -r 78d6e47469e4 doc-src/AxClass/Group/Group.thy
--- a/doc-src/AxClass/Group/Group.thy	Sun May 21 14:49:28 2000 +0200
+++ b/doc-src/AxClass/Group/Group.thy	Sun May 21 21:48:39 2000 +0200
@@ -1,12 +1,36 @@
+
+header {* Basic group theory *};
 
 theory Group = Main:;
 
+text {*
+ \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.
+*};
+
+subsection {* Monoids and Groups *};
+
+text {*
+ First we declare some polymorphic constants required later for the
+ signature parts of our structures.
+*};
 
 consts
   times :: "'a => 'a => 'a"    (infixl "\<Otimes>" 70)
   inverse :: "'a => 'a"        ("(_\<inv>)" [1000] 999)
   one :: 'a                    ("\<unit>");
 
+text {*
+ \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.
+*};
 
 axclass
   monoid < "term"
@@ -14,6 +38,19 @@
   left_unit:  "\<unit> \<Otimes> x = x"
   right_unit: "x \<Otimes> \<unit> = x";
 
+text {*
+ \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$.
+*};
+
+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$.
+*};
 
 axclass
   semigroup < "term"
@@ -24,13 +61,40 @@
   left_unit:    "\<unit> \<Otimes> x = x"
   left_inverse: "inverse x \<Otimes> x = \<unit>";
 
+axclass
+  agroup < group
+  commute: "x \<Otimes> y = y \<Otimes> x";
+
+text {*
+ \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.
+*};
+
+
+subsection {* Abstract reasoning *};
 
 text {*
- 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.
 *};
 
-theorem group_right_inverse: "x \<Otimes> x\<inv> = (\<unit>::'a::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);
@@ -52,12 +116,12 @@
 qed;
 
 text {*
- 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.
 *};
 
-theorem group_right_unit: "x \<Otimes> \<unit> = (x::'a::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);
@@ -70,24 +134,70 @@
   finally; show ?thesis; .;
 qed;
 
-
-axclass
-  agroup < group
-  commute: "x \<Otimes> y = y \<Otimes> x";
+text {*
+ \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$.
+*};
 
 
+subsection {* Abstract instantiation *};
+
+text {*
+ 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.
+*};
 
 instance monoid < semigroup;
 proof intro_classes;
-  fix x y z :: "'a::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::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";
@@ -96,13 +206,55 @@
     by (rule group_right_unit);
 qed;
 
+text {*
+ \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.
+*};
 
 
+subsection {* Concrete instantiation *};
+
+text {*
+ 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.
+*};
+
 defs
   times_bool_def:   "x \<Otimes> y \\<equiv> x \\<noteq> (y\\<Colon>bool)"
   inverse_bool_def: "x\<inv> \\<equiv> x\\<Colon>bool"
   unit_bool_def:    "\<unit> \\<equiv> False";
 
+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
+ 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.
+*};
+
 instance bool :: agroup;
 proof (intro_classes,
     unfold times_bool_def inverse_bool_def unit_bool_def);
@@ -113,13 +265,50 @@
   show "(x \\<noteq> y) = (y \\<noteq> x)"; by blast;
 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.
+
+ \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.
+*};
+
+
+subsection {* Lifting and Functors *};
+
+text {*
+ 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$.
+*};
 
 defs
   prod_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$,
+ $\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::semigroup * 'b::semigroup";
+  fix p q r :: "'a\<Colon>semigroup * '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) =
@@ -128,4 +317,11 @@
     by (simp add: semigroup.assoc);
 qed;
 
+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
+ theories.
+*};
+
 end;
\ No newline at end of file
diff -r a705822f4e2a -r 78d6e47469e4 doc-src/AxClass/Group/Product.thy
--- a/doc-src/AxClass/Group/Product.thy	Sun May 21 14:49:28 2000 +0200
+++ b/doc-src/AxClass/Group/Product.thy	Sun May 21 21:48:39 2000 +0200
@@ -1,22 +1,83 @@
-(*  Title:      HOL/AxClasses/Tutorial/Product.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
 
-Example 'syntactic' class "product", instantiated on type "bool".  At
-first sight this may look like instance in Haskell, but is not quite
-the same!
-*)
+header {* Syntactic classes *};
 
 theory Product = Main:;
 
+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.
+
+ The $product$ class below provides a less degenerate example of
+ syntactic type classes.
+*};
+
 axclass
   product < "term";
 consts
   product :: "'a::product \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\\<otimes>" 70);
 
+text {*
+ Here class $product$ is defined as subclass of $term$ without any
+ additional axioms.  This effects in logical equivalence of $product$
+ and $term$, as is reflected by the trivial introduction rule
+ generated for this definition.
+
+ \medskip So what is the difference of declaring $\TIMES :: (\alpha ::
+ product) \To \alpha \To \alpha$ vs.\ declaring $\TIMES :: (\alpha ::
+ term) \To \alpha \To \alpha$ anyway?  In this particular case where
+ $product \equiv term$, it should be obvious that both declarations
+ are the same from the logic's point of view.  It even makes the most
+ sense to remove sort constraints from constant declarations, as far
+ as the purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}.
+
+ On the other hand there are syntactic differences, of course.
+ Constants $\TIMES^\tau$ are rejected by the type-checker, unless the
+ arity $\tau :: product$ is part of the type signature.  In our
+ example, this arity may be always added when required by means of an
+ $\isarkeyword{instance}$ with the trivial proof $\BY{intro_classes}$.
+
+ \medskip Thus, we may observe the following discipline of using
+ syntactic classes.  Overloaded polymorphic constants have their type
+ arguments restricted to an associated (logically trivial) class $c$.
+ Only immediately before \emph{specifying} these constants on a
+ certain type $\tau$ do we instantiate $\tau :: c$.
+
+ This is done for class $product$ and type $bool$ as follows.
+*};
+
 instance bool :: product;
   by intro_classes;
 defs
   product_bool_def: "x \\<otimes> y \\<equiv> x \\<and> y";
 
+text {*
+ The definition $prod_bool_def$ becomes syntactically well-formed only
+ after the arity $bool :: product$ is made known to the type checker.
+
+ \medskip It is very important to see that above $\DEFS$ are not
+ directly connected with $\isarkeyword{instance}$ at all!  We were
+ just following our convention to specify $\TIMES$ on $bool$ after
+ having instantiated $bool :: product$.  Isabelle does not require
+ these definitions, which is in contrast to programming languages like
+ Haskell \cite{haskell-report}.
+
+ \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}.
+ 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''.
+*};
+
 end;
\ No newline at end of file
diff -r a705822f4e2a -r 78d6e47469e4 doc-src/AxClass/Group/Semigroups.thy
--- a/doc-src/AxClass/Group/Semigroups.thy	Sun May 21 14:49:28 2000 +0200
+++ b/doc-src/AxClass/Group/Semigroups.thy	Sun May 21 21:48:39 2000 +0200
@@ -1,16 +1,8 @@
 theory Semigroups = Main:;
 
-text {*
- \noindent Associativity of binary operations:
-*};
 constdefs
   is_assoc :: "('a \\<Rightarrow> 'a \\<Rightarrow> 'a) \\<Rightarrow> bool"
-  "is_assoc f == \\<forall>x y z. f (f x y) z = f x (f y z)";
-
-text {*
- \medskip\noindent Semigroups over \isa{(op~{\isasymOplus})}:
- %term (latex xsymbols symbols) "op \<Oplus>";
-*};
+  "is_assoc f \\<equiv> \\<forall>x y z. f (f x y) z = f x (f y z)";
 
 consts
   plus :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\<Oplus>" 65);
@@ -18,11 +10,6 @@
   plus_semigroup < "term"
   assoc: "is_assoc (op \<Oplus>)";
 
-text {*
- \medskip\noindent Semigroups over \isa{(op~{\isasymOtimes})}:
- %term (latex xsymbols symbols) "op \<Otimes>";
-*};
-
 consts
   times :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\<Otimes>" 65);
 axclass
diff -r a705822f4e2a -r 78d6e47469e4 doc-src/AxClass/Makefile
--- a/doc-src/AxClass/Makefile	Sun May 21 14:49:28 2000 +0200
+++ b/doc-src/AxClass/Makefile	Sun May 21 21:48:39 2000 +0200
@@ -13,7 +13,10 @@
 
 NAME = axclass
 
-FILES = axclass.tex body.tex ../iman.sty ../extra.sty ../pdfsetup.sty
+FILES = axclass.tex body.tex ../iman.sty ../extra.sty ../isar.sty \
+  ../pdfsetup.sty generated/Group.tex generated/NatClass.tex \
+  generated/Product.tex generated/Semigroup.tex generated/Semigroups.tex \
+  generated/session.tex
 
 dvi: $(NAME).dvi
 
diff -r a705822f4e2a -r 78d6e47469e4 doc-src/AxClass/Nat/NatClass.thy
--- a/doc-src/AxClass/Nat/NatClass.thy	Sun May 21 14:49:28 2000 +0200
+++ b/doc-src/AxClass/Nat/NatClass.thy	Sun May 21 21:48:39 2000 +0200
@@ -1,15 +1,3 @@
-(*  Title:      FOL/ex/NatClass.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-This is an abstract version of Nat.thy. Instead of axiomatizing a
-single type "nat" we define the class of all these types (up to
-isomorphism).
-
-Note: The "rec" operator had to be made 'monomorphic', because class
-axioms may not contain more than one type variable.
-*)
-
 theory NatClass = FOL:;
 
 consts
diff -r a705822f4e2a -r 78d6e47469e4 doc-src/AxClass/axclass.tex
--- a/doc-src/AxClass/axclass.tex	Sun May 21 14:49:28 2000 +0200
+++ b/doc-src/AxClass/axclass.tex	Sun May 21 21:48:39 2000 +0200
@@ -1,6 +1,6 @@
 
 \documentclass[12pt,a4paper,fleqn]{report}
-\usepackage{graphicx,../iman,../extra,../pdfsetup}
+\usepackage{graphicx,../iman,../extra,../isar,../pdfsetup}
 \usepackage{generated/isabelle,generated/isabellesym}
 
 \newcommand{\isasymOtimes}{\emph{$\odot$}}
diff -r a705822f4e2a -r 78d6e47469e4 doc-src/AxClass/body.tex
--- a/doc-src/AxClass/body.tex	Sun May 21 14:49:28 2000 +0200
+++ b/doc-src/AxClass/body.tex	Sun May 21 21:48:39 2000 +0200
@@ -55,7 +55,7 @@
 These \emph{characteristic constants} behave like operations associated with
 the ``carrier'' type $\alpha$.
 
-We illustrate these basic concepts by the following theory of semi-groups.
+We illustrate these basic concepts by the following theory of semigroups.
 
 \bigskip
 \input{generated/Semigroup}
@@ -86,496 +86,44 @@
 semigroups in a sense, they are not the same!
 
 
-\section{Basic group theory}
-
 \input{generated/Group}
 
-
-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.
-
-
-\subsection{Monoids and Groups}
-
-First we declare some polymorphic constants required later for the signature
-parts of our structures.
-
-
-Next we define class $monoid$ of monoids of the form $(\alpha,
-{\TIMES}^\alpha)$.  Note that multiple class axioms are allowed for user
-convenience --- they simply represent the conjunction of their respective
-universal closures.
-
-
-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 for $\TIMES$.
-
-
-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$.
-
-
-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.
-
-
-\subsection{Abstract reasoning}
-
-In a sense, axiomatic type classes may be viewed as \emph{abstract theories}.
-Above class definitions internally generate the following abstract axioms:
-
-%FIXME
-% \begin{ascbox}
-% assoc:        (?x::?'a::semigroup) <*> (?y::?'a::semigroup)
-%                 <*> (?z::?'a::semigroup) = ?x <*> (?y <*> ?z)\medskip
-% left@unit:    1 <*> (?x::?'a::group) = ?x
-% left@inverse: inverse (?x::?'a::group) <*> ?x = 1\medskip
-% commut:       (?x::?'a::agroup) <*> (?y::?'a::agroup) = ?y <*> ?x
-% \emphnd{ascbox}
-
-All of these contain type variables $\alpha :: c$ that are restricted to types
-of some class $c$. These \emph{sort constraints} 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 purely technical point of view, abstract axioms are just ordinary
-Isabelle theorems; they may be used for proofs without special treatment.
-Such ``abstract proofs'' usually yield new abstract theorems.  For example, we
-may now derive the following laws of general groups.
-
-
-
-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$.
+\input{generated/Product}
 
 
-\subsection{Abstract instantiation}
-
-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 \subset
-monoid$ properly as follows (cf.\ \figref{fig:monoid-group}).
-
-\begin{figure}[htbp]
-  \begin{center}
-    \small
-%    \unitlength 0.75mm
-    \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}
+\section{Defining natural numbers in FOL}\label{sec:ex-natclass}
 
-
-\endinput
-
-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.
-
-\endinput
-
-The \texttt{instance} section does really check that the class inclusions
-(or type arities) to be added are derivable. To this end, it sets up a
-suitable goal and attempts a proof with the help of some internal
-axioms and user supplied theorems. These latter \emph{witnesses} usually
-should be appropriate type instances of the class axioms (as are
-\texttt{Monoid.assoc} and \texttt{assoc}, \texttt{left_unit}, \texttt{right_unit}
-above).
+Axiomatic type classes abstract over exactly one type argument. Thus, any
+\emph{axiomatic} theory extension where each axiom refers to at most one type
+variable, may be trivially turned into a \emph{definitional} one.
 
-The most important internal tool for instantiation proofs is the class
-introduction rule that is automatically generated by \texttt{axclass}. For
-class \texttt{group} this is axiom \texttt{groupI}:
-
-\begin{ascbox}
-groupI:   [| OFCLASS(?'a::term, semigroup@class);
-             !!x::?'a::term. 1 <*> x = x;
-             !!x::?'a::term. inverse x <*> x = 1 |]
-          ==> OFCLASS(?'a::term, group@class)
-\emphnd{ascbox}
-
-There are also axioms \texttt{monoidI}, \texttt{semigroupI} and \texttt{agroupI}
-of a similar form.  Note that $\texttt{OFCLASS}(\tau, c \texttt{_class})$
-expresses class membership $\tau :: c$ as a proposition of the
-meta-logic.
-
-
-\subsection{Concrete instantiation}
+We illustrate this with the natural numbers in Isabelle/FOL.
 
-So far we have covered the case of \texttt{instance $c@1$ < $c@2$} that
-could be described as \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 transferred to
-Isabelle's type signature level. This form of \texttt{instance} is a ``safe''
-variant of the old-style \texttt{arities} theory section.
-
-As an example, we show that type \texttt{bool} with exclusive-or as
-operation $\TIMES$, identity as \texttt{inverse}, and \texttt{False} as \texttt{1}
-forms an abelian group. We first define theory \texttt{Xor}:
-
-\begin{ascbox}
-Xor = Group +\medskip
-defs
-  prod@bool@def     "x <*> y   == x ~= (y::bool)"
-  inverse@bool@def  "inverse x == x::bool"
-  unit@bool@def     "1         == False"\medskip
-end
-\emphnd{ascbox}
-
-It is important to note that above \texttt{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 primitive recursion over types) would be also possible
-in traditional versions of \HOL\ that lack type classes.
-% (see FIXME <foundation> for more details)
-Nonetheless, such definitions are best applied in the context of
-classes.
-
-\medskip
-
-Since we chose the \texttt{defs} of theory \texttt{Xor} suitably, the class
-membership $\texttt{bool} :: \texttt{agroup}$ is now derivable as follows:
+\bigskip
+\input{generated/NatClass}
+\bigskip
 
-\begin{ascbox}
-open AxClass;
-goal@arity Xor.thy ("bool", [], "agroup");
-\out{Level 0}
-\out{OFCLASS(bool, agroup@class)}
-\out{ 1. OFCLASS(bool, agroup@class)}\brk
-by (axclass@tac []);
-\out{Level 1}
-\out{OFCLASS(bool, agroup@class)}
-\out{ 1. !!(x::bool) (y::bool) z::bool. x <*> y <*> z = x <*> (y <*> z)}
-\out{ 2. !!x::bool. 1 <*> x = x}
-\out{ 3. !!x::bool. inverse x <*> x = 1}
-\out{ 4. !!(x::bool) y::bool. x <*> y = y <*> x}
-\emphnd{ascbox}
-
-The tactic \texttt{axclass_tac} has applied \texttt{agroupI} internally to
-expand the class definition. It now remains to be shown that the
-\texttt{agroup} axioms hold for bool. To this end, we expand the
-definitions of \texttt{Xor} and solve the new subgoals by \texttt{fast_tac}
-of \HOL:
+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}}
 
-\begin{ascbox}
-by (rewrite@goals@tac [Xor.prod@bool@def, Xor.inverse@bool@def,
-        Xor.unit@bool@def]);
-\out{Level 2}
-\out{OFCLASS(bool, agroup@class)}
-\out{ 1. !!(x::bool) (y::bool) z::bool. x ~= y ~= z = (x ~= (y ~= z))}
-\out{ 2. !!x::bool. False ~= x = x}
-\out{ 3. !!x::bool. x ~= x = False}
-\out{ 4. !!(x::bool) y::bool. x ~= y = (y ~= x)}
-by (ALLGOALS (fast@tac HOL@cs));
-\out{Level 3}
-\out{OFCLASS(bool, agroup@class)}
-\out{No subgoals!}
-qed "bool@in@agroup";
-\out{val bool@in@agroup = "OFCLASS(bool, agroup@class)"}
-\emphnd{ascbox}
-
-The result is theorem $\texttt{OFCLASS}(\texttt{bool}, \texttt{agroup_class})$
-which expresses $\texttt{bool} :: \texttt{agroup}$ as a meta-proposition. This
-is not yet known at the type signature level, though.
+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$).
 
 \medskip
 
-What we have done here by hand, can be also performed via
-\texttt{instance} in a similar way behind the scenes. This may look as
-follows\footnote{Subsequently, theory \texttt{Xor} is no longer
-  required.}:
-
-\begin{ascbox}
-BoolGroupInsts = Group +\medskip
-defs
-  prod@bool@def     "x <*> y   == x ~= (y::bool)"
-  inverse@bool@def  "inverse x == x::bool"
-  unit@bool@def     "1         == False"\medskip
-instance
-  bool :: agroup                \{| ALLGOALS (fast@tac HOL@cs) |\}\medskip
-end
-\emphnd{ascbox}
-
-This way, we have $\texttt{bool} :: \texttt{agroup}$ in the type signature of
-\texttt{BoolGroupInsts}, and all abstract group theorems are transferred
-to \texttt{bool} for free.
-
-Similarly, we could now also instantiate our group theory classes to
-many other concrete types. For example, $\texttt{int} :: \texttt{agroup}$ (by
-defining $\TIMES$ as addition, \texttt{inverse} as negation and \texttt{1} as
-zero, say) or $\texttt{list} :: (\texttt{term})\texttt{semigroup}$ (e.g.\ if
-$\TIMES$ is list append). Thus, the characteristic constants $\TIMES$,
-\texttt{inverse}, \texttt{1} really become overloaded, i.e.\ have different
-meanings on different types.
-
-
-\subsection{Lifting and Functors}
-
-As already mentioned above, \HOL-like systems not only support
-overloaded definitions of polymorphic constants (without requiring
-type classes), but even primitive recursion over types. That is,
-definitional equations $c^\tau \emphq t$ may also contain constants of
-name $c$ on the RHS --- provided that these have types that are
-strictly simpler (structurally) than $\tau$.
-
-This feature enables us to \emph{lift operations}, e.g.\ to Cartesian
-products, direct sums or function spaces. Below, theory
-\texttt{ProdGroupInsts} lifts $\TIMES$ componentwise to two-place
-Cartesian products $\alpha \times \beta$:
-
-\begin{ascbox}
-ProdGroupInsts = Prod + Group +\medskip
-defs
-  prod@prod@def "p <*> q == (fst p <*> fst q, snd p <*> snd q)"\medskip
-instance
-  "*" :: (semigroup, semigroup) semigroup
-    \{| simp@tac (prod@ss addsimps [assoc]) 1 |\}
-end
-\emphnd{ascbox}
-
-Note that \texttt{prod_prod_def} basically has the form $\emphdrv
-{\TIMES}^{\alpha \times \beta} \emphq \ldots {\TIMES}^\alpha \ldots
-{\TIMES}^\beta \ldots$, i.e.\ the recursive occurrences
-$\TIMES^\alpha$ and $\TIMES^\beta$ are really at ``simpler'' types.
-
-It is very easy to see that associativity of $\TIMES^\alpha$,
-$\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence
-the two-place type constructor $\times$ maps semigroups into
-semigroups. This fact is proven and put into Isabelle's type signature by
-above \texttt{instance} section.
-
-\medskip
-
-Thus, if we view class instances as ``structures'', overloaded
-constant definitions with primitive recursion over types indirectly
-provide some kind of ``functors'' (mappings between abstract theories,
-that is).
-
-
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "axclass"
-%%% End: 
-
-
-\section{Syntactic classes}
-
-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:  FIXME
-
-\input{generated/Product}
-\input{generated/NatClass}
-
-
-
-\endinput
-
-
-%\section
-
-\begin{ascbox}
-  <*> :: ['a, 'a] => 'a
-\emphnd{ascbox}
-
-is actually an abbreviation for:
-
-\begin{ascbox}
-  <*> :: ['a::term, 'a::term] => 'a::term
-\emphnd{ascbox}
-
-Since class \texttt{term} is the universal class of \HOL, this is not
-really a restriction at all. A less trivial example is the following
-theory \texttt{Product}:
-
-\begin{ascbox}
-Product = HOL +\medskip
-axclass
-  product < term\medskip
-consts
-  "<*>" :: "['a::product, 'a] => 'a"      (infixl 70)\medskip
-end
-\emphnd{ascbox}
-
-Here class \texttt{product} is defined as subclass of \texttt{term}, but
-without any additional axioms. This effects in logical equivalence of
-\texttt{product} and \texttt{term}, since \texttt{productI} is as follows:
+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 --- independent of satisfiability.  The
+meta-logic won't break, even if some classes (or general sorts) turns out to
+be empty (``inconsistent'') later.
 
-\begin{ascbox}
-productI: OFCLASS(?'a::logic, term@class) ==>
-            OFCLASS(?'a::logic, product@class)
-\emphnd{ascbox}
-
-I.e.\ $\texttt{term} \subseteq \texttt{product}$. The converse inclusion is
-already contained in the type signature of theory \texttt{Product}.
-
-Now, what is the difference of declaring $\TIMES :: [\alpha ::
-\texttt{product}, \alpha] \To \alpha$ vs.\ declaring $\TIMES :: [\alpha ::
-\texttt{term}, \alpha] \To \alpha$? In this special case (where
-$\texttt{product} \emphq \texttt{term}$), it should be obvious that both
-declarations are the same from the logic's point of view.  It is even
-most sensible in the general case not to attach any \emph{logical}
-meaning to sort constraints occurring in constant \emph{declarations}
-(see \cite[page 79]{Wenzel94} for more details).
-
-On the other hand there are syntactic differences, of course.
-Constants $\TIMES^\tau$ are rejected by the type-checker, unless $\tau
-:: \texttt{product}$ is part of the type signature.  In our example, this
-arity may be always added when required by means of a trivial
-\texttt{instance}.
-
-Thus, we can follow this discipline: Overloaded polymorphic constants
-have their type arguments restricted to an associated (logically
-trivial) class $c$. Only immediately before \emph{specifying} these
-constants on a certain type $\tau$ do we instantiate $\tau :: c$.
-
-This is done for class \texttt{product} and type \texttt{bool} in theory
-\texttt{ProductInsts} below:
-
-\begin{ascbox}
-ProductInsts = Product +\medskip
-instance
-  bool :: product\medskip
-defs
-  prod@bool@def "x <*> y  == x & y::bool"\medskip
-end
-\emphnd{ascbox}
-
-Note that \texttt{instance bool ::\ product} does not require any
-witnesses, since this statement is logically trivial. Nonetheless,
-\texttt{instance} really performs a proof.
-
-Only after $\texttt{bool} :: \texttt{product}$ is made known to the type
-checker, does \texttt{prod_bool_def} become syntactically well-formed.
-
-\medskip
-
-It is very important to see that above \texttt{defs} are not directly
-connected with \texttt{instance} at all! We were just following our
-convention to specify $\TIMES$ on \texttt{bool} after having instantiated
-$\texttt{bool} :: \texttt{product}$. Isabelle does not require these definitions,
-which is in contrast to programming languages like Haskell.
-
-\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}. 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''.
-
-
-\section{Defining natural numbers in FOL}
-\label{sec:ex-natclass}
-
-Axiomatic type classes abstract over exactly one type argument. Thus,
-any \emph{axiomatic} theory extension where each axiom refers to at most
-one type variable, may be trivially turned into a \emph{definitional}
-one.
-
-We illustrate this with the natural numbers in Isabelle/FOL:
-
-\begin{ascbox}
-NatClass = FOL +\medskip
-consts
-  "0"           :: "'a"                                 ("0")
-  Suc           :: "'a => 'a"
-  rec           :: "['a, 'a, ['a, 'a] => 'a] => 'a"\medskip
-axclass
-  nat < term
-  induct        "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
-  Suc@inject    "Suc(m) = Suc(n) ==> m = n"
-  Suc@neq@0     "Suc(m) = 0 ==> R"
-  rec@0         "rec(0, a, f) = a"
-  rec@Suc       "rec(Suc(m), a, f) = f(m, rec(m, a, f))"\medskip
-consts
-  "+"           :: "['a::nat, 'a] => 'a"                (infixl 60)\medskip
-defs
-  add@def       "m + n == rec(m, n, %x y. Suc(y))"\medskip
-end
-\emphnd{ascbox}
-
-\texttt{NatClass} is an abstract version of \texttt{Nat}\footnote{See
-  directory \texttt{FOL/ex}.}. Basically, we have just replaced all
-occurrences of \emph{type} \texttt{nat} by $\alpha$ and used the natural
-number axioms to define \emph{class} \texttt{nat}\footnote{There's a snag:
-  The original recursion operator \texttt{rec} had to be made monomorphic,
-  in a sense.}. Thus class \texttt{nat} contains exactly those types
-$\tau$ that are isomorphic to ``the'' natural numbers (with signature
-\texttt{0}, \texttt{Suc}, \texttt{rec}).
-
-Furthermore, theory \texttt{NatClass} defines an ``abstract constant'' $+$
-based on class \texttt{nat}.
-
-\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 --- independent
-of satisfiability. The meta-logic won't break, even if some class (or
-general sort) turns out to be empty (``inconsistent'')
-later\footnote{As a consequence of an old bug, this is \emph{not} true
-  for pre-Isabelle94-2 versions.}.
-
-For example, we may derive the following abstract natural numbers
-theorems:
-
-\begin{ascbox}
-add@0:    0 + (?n::?'a::nat) = ?n
-add@Suc:  Suc(?m::?'a::nat) + (?n::?'a::nat) = Suc(?m + ?n)
-\emphnd{ascbox}
-
-See also file \texttt{FOL/ex/NatClass.ML}. Note that this required only
-some trivial modifications of the original \texttt{Nat.ML}.
+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 constraints).
 
 
 %% FIXME move some parts to ref or isar-ref manual (!?);
diff -r a705822f4e2a -r 78d6e47469e4 doc-src/AxClass/generated/Group.tex
--- 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}%
diff -r a705822f4e2a -r 78d6e47469e4 doc-src/AxClass/generated/NatClass.tex
--- a/doc-src/AxClass/generated/NatClass.tex	Sun May 21 14:49:28 2000 +0200
+++ b/doc-src/AxClass/generated/NatClass.tex	Sun May 21 21:48:39 2000 +0200
@@ -1,6 +1,4 @@
 \begin{isabelle}%
-\isanewline
-\isanewline
 \isacommand{theory}~NatClass~=~FOL:\isanewline
 \isanewline
 \isacommand{consts}\isanewline
diff -r a705822f4e2a -r 78d6e47469e4 doc-src/AxClass/generated/Product.tex
--- a/doc-src/AxClass/generated/Product.tex	Sun May 21 14:49:28 2000 +0200
+++ b/doc-src/AxClass/generated/Product.tex	Sun May 21 21:48:39 2000 +0200
@@ -1,16 +1,77 @@
 \begin{isabelle}%
-\isanewline
-\isanewline
-\isacommand{theory}~Product~=~Main:\isanewline
-\isanewline
+%
+\isamarkupheader{Syntactic classes}
+\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.
+
+ The $product$ class below provides a less degenerate example of
+ syntactic type classes.%
+\end{isamarkuptext}%
 \isacommand{axclass}\isanewline
 ~~product~<~{"}term{"}\isanewline
 \isacommand{consts}\isanewline
-~~product~::~{"}'a::product~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymotimes}{"}~70)\isanewline
-\isanewline
+~~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$
+ and $term$, as is reflected by the trivial introduction rule
+ generated for this definition.
+
+ \medskip So what is the difference of declaring $\TIMES :: (\alpha ::
+ product) \To \alpha \To \alpha$ vs.\ declaring $\TIMES :: (\alpha ::
+ term) \To \alpha \To \alpha$ anyway?  In this particular case where
+ $product \equiv term$, it should be obvious that both declarations
+ are the same from the logic's point of view.  It even makes the most
+ sense to remove sort constraints from constant declarations, as far
+ as the purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}.
+
+ On the other hand there are syntactic differences, of course.
+ Constants $\TIMES^\tau$ are rejected by the type-checker, unless the
+ arity $\tau :: product$ is part of the type signature.  In our
+ example, this arity may be always added when required by means of an
+ $\isarkeyword{instance}$ with the trivial proof $\BY{intro_classes}$.
+
+ \medskip Thus, we may observe the following discipline of using
+ syntactic classes.  Overloaded polymorphic constants have their type
+ arguments restricted to an associated (logically trivial) class $c$.
+ Only immediately before \emph{specifying} these constants on a
+ certain type $\tau$ do we instantiate $\tau :: c$.
+
+ This is done for class $product$ and type $bool$ as follows.%
+\end{isamarkuptext}%
 \isacommand{instance}~bool~::~product\isanewline
 ~~\isacommand{by}~intro\_classes\isanewline
 \isacommand{defs}\isanewline
-~~product\_bool\_def:~{"}x~{\isasymotimes}~y~{\isasymequiv}~x~{\isasymand}~y{"}\isanewline
-\isanewline
+~~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.
+
+ \medskip It is very important to see that above $\DEFS$ are not
+ directly connected with $\isarkeyword{instance}$ at all!  We were
+ just following our convention to specify $\TIMES$ on $bool$ after
+ having instantiated $bool :: product$.  Isabelle does not require
+ these definitions, which is in contrast to programming languages like
+ Haskell \cite{haskell-report}.
+
+ \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}.
+ 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''.%
+\end{isamarkuptext}%
 \isacommand{end}\end{isabelle}%
diff -r a705822f4e2a -r 78d6e47469e4 doc-src/AxClass/generated/Semigroups.tex
--- a/doc-src/AxClass/generated/Semigroups.tex	Sun May 21 14:49:28 2000 +0200
+++ b/doc-src/AxClass/generated/Semigroups.tex	Sun May 21 21:48:39 2000 +0200
@@ -1,24 +1,16 @@
 \begin{isabelle}%
-\isacommand{theory}~Semigroups~=~Main:%
-\begin{isamarkuptext}%
-\noindent Associativity of binary operations:%
-\end{isamarkuptext}%
+\isacommand{theory}~Semigroups~=~Main:\isanewline
+\isanewline
 \isacommand{constdefs}\isanewline
 ~~is\_assoc~::~{"}('a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a)~{\isasymRightarrow}~bool{"}\isanewline
-~~{"}is\_assoc~f~==~{\isasymforall}x~y~z.~f~(f~x~y)~z~=~f~x~(f~y~z){"}%
-\begin{isamarkuptext}%
-\medskip\noindent Semigroups over \isa{(op~{\isasymOplus})}:
- %term (latex xsymbols symbols) "op \<Oplus>";%
-\end{isamarkuptext}%
+~~{"}is\_assoc~f~{\isasymequiv}~{\isasymforall}x~y~z.~f~(f~x~y)~z~=~f~x~(f~y~z){"}\isanewline
+\isanewline
 \isacommand{consts}\isanewline
 ~~plus~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOplus}{"}~65)\isanewline
 \isacommand{axclass}\isanewline
 ~~plus\_semigroup~<~{"}term{"}\isanewline
-~~assoc:~{"}is\_assoc~(op~{\isasymOplus}){"}%
-\begin{isamarkuptext}%
-\medskip\noindent Semigroups over \isa{(op~{\isasymOtimes})}:
- %term (latex xsymbols symbols) "op \<Otimes>";%
-\end{isamarkuptext}%
+~~assoc:~{"}is\_assoc~(op~{\isasymOplus}){"}\isanewline
+\isanewline
 \isacommand{consts}\isanewline
 ~~times~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~65)\isanewline
 \isacommand{axclass}\isanewline
diff -r a705822f4e2a -r 78d6e47469e4 doc-src/AxClass/generated/session.tex
--- a/doc-src/AxClass/generated/session.tex	Sun May 21 14:49:28 2000 +0200
+++ b/doc-src/AxClass/generated/session.tex	Sun May 21 21:48:39 2000 +0200
@@ -1,4 +1,1 @@
-\input{Semigroup.tex}
-\input{Semigroups.tex}
-\input{Group.tex}
-\input{Product.tex}
+\input{NatClass.tex}