doc-src/AxClass/Group/Semigroups.thy

+
+header {* Semigroups *};
+
 theory Semigroups = Main:;
 
-constdefs
-  is_assoc :: "('a \\<Rightarrow> 'a \\<Rightarrow> 'a) \\<Rightarrow> bool"
-  "is_assoc f \\<equiv> \\<forall>x y z. f (f x y) z = f x (f y z)";
+text {*
+ \medskip\noindent An axiomatic type class is simply a class of types
+ that all meet certain \emph{axioms}. Thus, type classes may be also
+ understood as type predicates --- i.e.\ abstractions over a single
+ type argument $\alpha$.  Class axioms typically contain polymorphic
+ constants that depend on this type $\alpha$.  These
+ \emph{characteristic constants} behave like operations associated
+ with the ``carrier'' type $\alpha$.
+
+ We illustrate these basic concepts by the following formulation of
+ semigroups.
+*};
 
 consts
-  plus :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\<Oplus>" 65);
+  times :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\<Otimes>" 70);
+axclass
+  semigroup < "term"
+  assoc: "(x \<Otimes> y) \<Otimes> z = x \<Otimes> (y \<Otimes> z)";
+
+text {*
+ \noindent Above we have first declared a polymorphic constant $\TIMES
+ :: \alpha \To \alpha \To \alpha$ and then defined the class
+ $semigroup$ of all types $\tau$ such that $\TIMES :: \tau \To \tau
+ \To \tau$ is indeed an associative operator.  The $assoc$ axiom
+ contains exactly one type variable, which is invisible in the above
+ presentation, though.  Also note that free term variables (like $x$,
+ $y$, $z$) are allowed for user convenience --- conceptually all of
+ these are bound by outermost universal quantifiers.
+
+ \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
+ to semigroups $(\tau, \TIMES^\tau)$.
+*};
+
+consts
+  plus :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\<Oplus>" 70);
 axclass
   plus_semigroup < "term"
-  assoc: "is_assoc (op \<Oplus>)";
+  assoc: "(x \<Oplus> y) \<Oplus> z = x \<Oplus> (y \<Oplus> z)";
 
-consts
-  times :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\<Otimes>" 65);
-axclass
-  times_semigroup < "term"
-  assoc: "is_assoc (op \<Otimes>)";
+text {*
+ \noindent Even if classes $plus_semigroup$ and $times_semigroup$ both
+ represent semigroups in a sense, they are certainly not the same!
+*};
 
 end;