author wenzelm Mon, 22 May 2000 11:56:55 +0200 changeset 8907 813fabceec00 parent 8906 fc7841f31388 child 8908 25f2bdc02123
tuned;
 doc-src/AxClass/Group/Group.thy file | annotate | diff | comparison | revisions doc-src/AxClass/Group/Product.thy file | annotate | diff | comparison | revisions doc-src/AxClass/Group/Semigroups.thy file | annotate | diff | comparison | revisions doc-src/AxClass/Nat/NatClass.thy file | annotate | diff | comparison | revisions doc-src/AxClass/axclass.tex file | annotate | diff | comparison | revisions doc-src/AxClass/body.tex file | annotate | diff | comparison | revisions doc-src/AxClass/generated/Group.tex file | annotate | diff | comparison | revisions doc-src/AxClass/generated/NatClass.tex file | annotate | diff | comparison | revisions doc-src/AxClass/generated/Product.tex file | annotate | diff | comparison | revisions doc-src/AxClass/generated/Semigroups.tex file | annotate | diff | comparison | revisions
--- 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
@@ -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
- 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
+ simple types) are admissible as definitional extensions of plain HOL
+ \cite{Wenzel:1997:TPHOL}.  The Haskell-style type system is not
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

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