--- 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
--- 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
--- 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
--- 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
--- 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
--- 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$}}
--- 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 (!?);
--- 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}%
--- 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
--- 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}%
--- 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
--- 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}